Catala à la carte

[adelaett]

To simplify the internals of the Catala compiler, it should be possible to use the "a la carte" framework.

The main idea behind "a la carte" is to split the definition of an expression.

type expr =
| EVar of expr Bindlib.var Pos.marked
| ETuple of expr Pos.marked list * D.StructName.t option
| ETupleAccess of expr Pos.marked * int * D.StructName.t option * D.typ Pos.marked list
| EInj of expr Pos.marked * int * D.EnumName.t * D.typ Pos.marked list
| EMatch of expr Pos.marked * expr Pos.marked list * D.EnumName.t
| EArray of expr Pos.marked list
| ELit of lit
| EAbs of (expr, expr Pos.marked) Bindlib.mbinder Pos.marked * D.typ Pos.marked list
| EApp of expr Pos.marked * expr Pos.marked list
| EAssert of expr Pos.marked
| EOp of D.operator
| EIfThenElse of expr Pos.marked * expr Pos.marked * expr Pos.marked
| ERaise of except
| ECatch of expr Pos.marked * except * expr Pos.marked

In subparts

type 'expr expr_lambda =
| EVar of 'expr Bindlib.var Pos.marked
| EAbs of ('expr, 'expr Pos.marked) Bindlib.mbinder Pos.marked * D.typ Pos.marked list
| EApp of 'expr Pos.marked * 'expr Pos.marked list

type 'expr expr_constructors =
| EInj of 'expr Pos.marked * int * D.EnumName.t * D.typ Pos.marked list
| EMatch of 'expr Pos.marked * 'expr Pos.marked list * D.EnumName.t

type 'expr expr_firstorder =
| EOp of D.operator
| EIfThenElse of 'expr Pos.marked * 'expr Pos.marked * 'expr Pos.marked
| ELit of lit
| ETuple of 'expr Pos.marked list * D.StructName.t option
| ETupleAccess of 'expr Pos.marked * int * D.StructName.t option * D.typ Pos.marked list
| EArray of 'expr Pos.marked list

type 'expr expr_exceptions =
| EAssert of 'expr Pos.marked
| ERaise of except
| ECatch of 'expr Pos.marked * except * 'expr Pos.marked

type 'expr expr_default =
| EDefault of 'expr Pos.marked list * 'expr Pos.marked * 'expr Pos.marked
| ErrorOnEmpty of 'expr Pos.marked

type lcalc =
| LInjConstructors of lcalc expr_constructors
| LInjLambda of lcalc expr_lambda
| LInjFirstOrder of lcalc expr_firstorder
| LInjExceptions of lcalc expr_exceptions

type dcalc =
| DInjConstructors of dcalc expr_constructors
| DInjLambda of dcalc expr_lambda
| DInjFirstOrder of dcalc expr_firstorder
| DInjDefault of dcalc expr_default

One could then reuse components developed for a subpart of the calculus to other subparts. For instance, the type inference algorithm defined for dcalc could be reuse without duplicating the code in the lcalc; and the programs transformations could be simplified as most of the translation from dcalc to lcalc is identity.

It is not obvious that this approach is compatible with Bindlib.

Here are some pointers on this kind of definition

https://www.ps.uni-saarland.de/Publications/documents/ForsterStark_2020_Coq.pdf

http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf

[denismerigoux]

A factorization of all the AST definitions has been done with #320, #321 and predecessors. It's not à la carte but achieves similar objectives, so I can close this.