Feature request: Eliminate (U)LLBC AST Modules' Circular Dependencies

[ssyram]

Rust allows module circular dependencies but most of the mainstream languages not. This creates a potential gap in the auto-generation of (U)LLBC AST in other languages.

If the dependencies could be resolved at the Rust side, the auto-generation could be more direct and auto without the need of manually hard-coding to adjust the definitions.

Another obvious way would be to produce all the definitions at one file and making everything mutually recursive, but this is never an elegant way...

Yet, this is of rather low priority.

[Nadrieril]

What is the ask exactly? You would want to move the mutually-recursive definitions to all be in the same file? So we'd have all of Ty, ConstantExpr and related types together? Is it that you'd want to use the rust module names to generate the corresponding ocaml/haskell modules?

[sonmarcho]

I'm not sure I fully understand the ask either, but perhaps relatedly have you noticed that the TranslatedCrate has a field which lists the definitions following the dependency order (i.e., g appears before f if f depends on g) and while grouping together the mutually recursive definitions?

charon/charon/src/ast/krate.rs

Lines 205 to 207 in 69f63d6

	/// The re-ordered groups of declarations, initialized as empty.
	#[drive(skip)]
	pub ordered_decls: Option<DeclarationsGroups>,

[ssyram]

@sonmarcho Ah, thanks! This would be helpful!

[ssyram]

@Nadrieril I mean is it possible to resolve the modular circular dependencies in Rust so that when generating the codes, one can mimic exactly the same file / module structures, this is also helpful in confirming consistency between the ASTs expressed in different languages and also helpful in human understanding that one who is familiar with the Rust AST can instantly understand the OCaml / Haskell AST.

[Nadrieril]

Is that not the case today? I think the crate was designed with this in mind, though it's evolved a lot so I might have accidentaly broken that. As far as I can see though, making the modules be like (u)llbc_ast -> gast -> expressions -> ty -> values would work?

[ssyram]

Currently, gast and (u)llbc_ast at least is currently a circular dependency, and also expression will also depend on gast for the DeclRef things. But yes, this issue itself is not that urgent.

[Nadrieril]

Ah yes I see. If we find an organization that's idiomatic in Rust and also in ocaml/haskell I'm open to that change.