The generic type of AST markings. Using a GADT allows functions to be polymorphic in the marking, but still do transformations on types when appropriate. The Custom case can be used within passes that need to store specific information, e.g. typing
General expressions: groups all expression cases of the different ASTs, and uses a GADT to eliminate irrelevant cases for each one. The 't annotations are also totally unconstrained at this point. The dcalc exprs, for ex ample, are then defined with type naked_expr = dcalc naked_gexpr plus the annotations.
A few tips on using this GADT:
To write a function that handles cases from different ASTs, explicit the type variables: fun (type a) (x: a naked_gexpr) -> ...
For recursive functions, you may need to additionally explicit the generalisation of the variable: let rec f: type a . a naked_gexpr -> ...
Always think of using the pre-defined map/fold functions in Expr rather than completely defining your recursion manually.
The first argument of the base_gexpr type caracterises the "deep" type of the AST, while the second is the shallow type. They are always equal for well-formed AST types, but differentiating them ephemerally allows us to do well-typed recursive transformations on the AST that change its type
A function of the given type, as a runtime OCaml object. The specified types for arguments and result must be the Catala types corresponding to the runtime types of the function.
('a, 'm) gexpr boxed is ('a, 'm) boxed_gexpr. The difference with ('a, 'm) gexpr Bindlib.box is that the annotations is outside of the box, and can therefore be accessed without the need to resolve the box
Constructs scopes and programs on top of expressions. The 'e type parameter throughout is expected to match instances of the gexpr type defined above. Markings are constrained to the mark GADT defined above. Note that this structure is at the moment only relevant for dcalc and lcalc, as scopelang has its own scope structure, as the name implies.
type scope_let_kind =
| DestructuringInputStruct
(*
let x = input.field
*)
| ScopeVarDefinition
(*
let x = error_on_empty e
*)
| SubScopeVarDefinition
(*
let s.x = fun _ -> e or let s.x = error_on_empty e for input-only subscope variables.
*)
| CallingSubScope
(*
let result = s ({ x = s.x; y = s.x; ...})
*)
| DestructuringSubScopeResults
(*
let s.x = result.x *
*)
| Assertion
(*
let () = assert e
*)
This kind annotation signals that the let-binding respects a structural invariant. These invariants concern the shape of the expression in the let-binding, and are documented below.
A scope let-binding has all the information necessary to make a proper let-binding expression, plus an annotation for the kind of the let-binding that comes from the compilation of a Scopelang.Ast statement.
Instead of being a single expression, we give a little more ad-hoc structure to the scope body by decomposing it in an ordered list of let-bindings, and a result expression that uses the let-binded variables. The first binder is the argument of type scope_body_input_struct.