search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
132 stars 33 forks source link

Remove the Typed module #1258

Closed Halbaroth closed 1 week ago

Halbaroth commented 1 month ago

This PR removes the output AST of the legacy typechecker. This AST was still used by the compilation of match expressions in Expr.

Halbaroth commented 1 week ago

Overall looks good — I think the Expr module was a good boundary for the mk_match abstraction but I'm OK as is now that we have a single frontend.

I had the same concerns when I have done this modification. Expr is an internal AST of the library and Dolmen expressions will become the new input AST of the library. Moving this feature from Expr to Translate means we cannot use it directly on AE expressions as library developers, but we do not use it. Actually we could use it in models because it would be simpler to produce a match expression for model terms then compiles it. My opinion is that we do not need to focus on this detail now and we can move back a part of the code in Expr later if we want to produce match expressions from AE expressions. Keeping all the match compilation code in Translate now is just simpler in the current state of the code base.

bclement-ocp commented 1 week ago

I had the same concerns when I have done this modification. [..] My opinion is that we do not need to focus on this detail now and we can move back a part of the code in Expr later

This argument could have been made to avoid moving the code out of Expr in the first place ;)