catala/compiler/verification
Louis Gesbert a415355a39 Rework the AST Gadt to allow merging of different ASTs
The phantom polymorphic variant qualifying AST nodes is reversed:
- previously, we were explicitely restricting each AST node to the passes where it belonged using a closed type (e.g. `[< dcalc | lcalc]`)
- now, each node instead declares the "feature" it provides using an open type (e.g. `[> 'Exceptions ]`)
- then the AST for a specific pass limits the features it allows with a closed type

The result is that you can mix and match all features if you wish,
even if the result is not a valid AST for any given pass. More
interestingly, it's now easier to write a function that works on
different ASTs at once (it's the inferred default if you don't write a
type restriction).

The opportunity was also taken to simplify the encoding of the
operators, which don't need a second type parameter anymore.
2023-03-30 15:30:08 +02:00
..
conditions.ml Toplevel definitions: branch cleanup 2023-02-13 18:02:09 +01:00
conditions.mli Merge branch 'master' into afromher_334 2023-01-20 14:05:38 -05:00
dune Rename utils to catala_utils 2022-11-28 16:38:09 +01:00
io.ml Merge branch 'master' into afromher_334 2023-01-20 14:05:38 -05:00
io.mli Merge branch 'afromher_verif' into afromher_334 2022-11-16 22:16:11 +01:00
solver.ml Merge branch 'master' into afromher_334 2023-01-20 14:05:38 -05:00
solver.mli Leverage the shared AST: big cleanup (part I) 2022-08-22 19:28:21 +02:00
verification.mld Documentation pass 2022-01-19 10:54:16 +01:00
z3backend.dummy.ml Merge branch 'master' into afromher_334 2023-01-20 14:05:38 -05:00
z3backend.mli Big reformatting 2022-03-08 15:03:14 +01:00
z3backend.real.ml Rework the AST Gadt to allow merging of different ASTs 2023-03-30 15:30:08 +02:00