catala/compiler/verification
Louis Gesbert 1efda5ca22 Typing defaults: support nested priorities
The way nested priorities are encoded use `< < excs | true :- nested > :- x >`,
which imply that `nested` can actually be ∅ ; to cope with this, the typing of
default terms is made more generic (the return type is now the same as the
`cons` type `'a`, rather than `<'a>`). For the general case, we add an explicit
`EPureDefault` node which just encapsulates its argument (a `return`, in monad
terminology).
2023-11-27 11:09:08 +01:00
..
conditions.ml Verification: support unboxed defaults 2023-11-27 11:06:33 +01:00
conditions.mli Rework and normalise the Marked interface 2023-05-17 17:37:00 +02:00
dune Rename utils to catala_utils 2022-11-28 16:38:09 +01:00
globals.ml Refacter the main Driver module 2023-07-03 16:42:54 +02:00
globals.mli Refacter the main Driver module 2023-07-03 16:42:54 +02:00
io.ml Add some helper functions in a wrapper Map module 2023-07-12 11:51:15 +02:00
io.mli Merge branch 'afromher_verif' into afromher_334 2022-11-16 22:16:11 +01:00
solver.ml Messages renamed to Message (lighter syntax) 2023-06-13 11:50:56 +02: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 Messages renamed to Message (lighter syntax) 2023-06-13 11:50:56 +02:00
z3backend.mli Big reformatting 2022-03-08 15:03:14 +01:00
z3backend.real.ml Typing defaults: support nested priorities 2023-11-27 11:09:08 +01:00