CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 00:15:39 +03:00
Code Issues Projects Releases Wiki Activity

Rework the AST Gadt to allow merging of different ASTs

Browse Source 
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.
This commit is contained in:
Louis Gesbert 2023-03-30 15:30:08 +02:00
parent b85a199daa
commit a415355a39
18 changed files with 14574 additions and 13172 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

336
compiler/dcalc/interpreter.ml
View File

@ -113,12 +113,8 @@ let rec handle_eq ctx pos e1 e2 =
(* Call-by-value: the arguments are expected to be already evaluated here *)
and evaluate_operator :
type k.
decl_ctx ->
(dcalc, k) operator ->
Pos.t ->
'm Ast.expr list ->
'm Ast.naked_expr =
decl_ctx -> dcalc operator -> Pos.t -> 'm Ast.expr list -> 'm Ast.naked_expr
=
fun ctx op pos args ->
let protect f x y =
let get_binop_args_pos = function
@ -157,159 +153,181 @@ and evaluate_operator :
if List.exists (function ELit LEmptyError, _ -> true | _ -> false) args then
ELit LEmptyError
else
Operator.kind_dispatch op
~polymorphic:(fun op ->
match op, args with
| Length, [(EArray es, _)] ->
ELit (LInt (Runtime.integer_of_int (List.length es)))
| Log (entry, infos), [e'] ->
print_log ctx entry infos pos e';
Marked.unmark e'
| Eq, [(e1, _); (e2, _)] -> ELit (LBool (handle_eq ctx pos e1 e2))
| Map, [f; (EArray es, _)] ->
EArray
(List.map
(fun e' ->
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [e'] }) e'))
es)
| Reduce, [_; default; (EArray [], _)] -> Marked.unmark default
| Reduce, [f; _; (EArray (x0 :: xn), _)] ->
Marked.unmark
(List.fold_left
(fun acc x ->
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [acc; x] }) f))
x0 xn)
| Concat, [(EArray es1, _); (EArray es2, _)] -> EArray (es1 @ es2)
| Filter, [f; (EArray es, _)] ->
EArray
(List.filter
(fun e' ->
match
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [e'] }) e')
with
| ELit (LBool b), _ -> b
| _ ->
Errors.raise_spanned_error
(Expr.pos (List.nth args 0))
"This predicate evaluated to something else than a \
boolean (should not happen if the term was well-typed)")
es)
| Fold, [f; init; (EArray es, _)] ->
Marked.unmark
(List.fold_left
(fun acc e' ->
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [acc; e'] }) e'))
init es)
| (Length | Log _ | Eq | Map | Concat | Filter | Fold | Reduce), _ ->
err ())
~monomorphic:(fun op ->
let rlit =
match op, List.map (function ELit l, _ -> l | _ -> err ()) args with
| Not, [LBool b] -> LBool (o_not b)
| GetDay, [LDate d] -> LInt (o_getDay d)
| GetMonth, [LDate d] -> LInt (o_getMonth d)
| GetYear, [LDate d] -> LInt (o_getYear d)
| FirstDayOfMonth, [LDate d] -> LDate (o_firstDayOfMonth d)
| LastDayOfMonth, [LDate d] -> LDate (o_lastDayOfMonth d)
| And, [LBool b1; LBool b2] -> LBool (o_and b1 b2)
| Or, [LBool b1; LBool b2] -> LBool (o_or b1 b2)
| Xor, [LBool b1; LBool b2] -> LBool (o_xor b1 b2)
| ( ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth
| LastDayOfMonth | And | Or | Xor ),
_ ) ->
err ()
in
ELit rlit)
~resolved:(fun op ->
let rlit =
match op, List.map (function ELit l, _ -> l | _ -> err ()) args with
| Minus_int, [LInt x] -> LInt (o_minus_int x)
| Minus_rat, [LRat x] -> LRat (o_minus_rat x)
| Minus_mon, [LMoney x] -> LMoney (o_minus_mon x)
| Minus_dur, [LDuration x] -> LDuration (o_minus_dur x)
| ToRat_int, [LInt i] -> LRat (o_torat_int i)
| ToRat_mon, [LMoney i] -> LRat (o_torat_mon i)
| ToMoney_rat, [LRat i] -> LMoney (o_tomoney_rat i)
| Round_mon, [LMoney m] -> LMoney (o_round_mon m)
| Round_rat, [LRat m] -> LRat (o_round_rat m)
| Add_int_int, [LInt x; LInt y] -> LInt (o_add_int_int x y)
| Add_rat_rat, [LRat x; LRat y] -> LRat (o_add_rat_rat x y)
| Add_mon_mon, [LMoney x; LMoney y] -> LMoney (o_add_mon_mon x y)
| Add_dat_dur r, [LDate x; LDuration y] -> LDate (o_add_dat_dur r x y)
| Add_dur_dur, [LDuration x; LDuration y] ->
LDuration (o_add_dur_dur x y)
| Sub_int_int, [LInt x; LInt y] -> LInt (o_sub_int_int x y)
| Sub_rat_rat, [LRat x; LRat y] -> LRat (o_sub_rat_rat x y)
| Sub_mon_mon, [LMoney x; LMoney y] -> LMoney (o_sub_mon_mon x y)
| Sub_dat_dat, [LDate x; LDate y] -> LDuration (o_sub_dat_dat x y)
| Sub_dat_dur, [LDate x; LDuration y] -> LDate (o_sub_dat_dur x y)
| Sub_dur_dur, [LDuration x; LDuration y] ->
LDuration (o_sub_dur_dur x y)
| Mult_int_int, [LInt x; LInt y] -> LInt (o_mult_int_int x y)
| Mult_rat_rat, [LRat x; LRat y] -> LRat (o_mult_rat_rat x y)
| Mult_mon_rat, [LMoney x; LRat y] -> LMoney (o_mult_mon_rat x y)
| Mult_dur_int, [LDuration x; LInt y] ->
LDuration (o_mult_dur_int x y)
| Div_int_int, [LInt x; LInt y] -> LRat (protect o_div_int_int x y)
| Div_rat_rat, [LRat x; LRat y] -> LRat (protect o_div_rat_rat x y)
| Div_mon_mon, [LMoney x; LMoney y] ->
LRat (protect o_div_mon_mon x y)
| Div_mon_rat, [LMoney x; LRat y] ->
LMoney (protect o_div_mon_rat x y)
| Div_dur_dur, [LDuration x; LDuration y] ->
LRat (protect o_div_dur_dur x y)
| Lt_int_int, [LInt x; LInt y] -> LBool (o_lt_int_int x y)
| Lt_rat_rat, [LRat x; LRat y] -> LBool (o_lt_rat_rat x y)
| Lt_mon_mon, [LMoney x; LMoney y] -> LBool (o_lt_mon_mon x y)
| Lt_dat_dat, [LDate x; LDate y] -> LBool (o_lt_dat_dat x y)
| Lt_dur_dur, [LDuration x; LDuration y] ->
LBool (protect o_lt_dur_dur x y)
| Lte_int_int, [LInt x; LInt y] -> LBool (o_lte_int_int x y)
| Lte_rat_rat, [LRat x; LRat y] -> LBool (o_lte_rat_rat x y)
| Lte_mon_mon, [LMoney x; LMoney y] -> LBool (o_lte_mon_mon x y)
| Lte_dat_dat, [LDate x; LDate y] -> LBool (o_lte_dat_dat x y)
| Lte_dur_dur, [LDuration x; LDuration y] ->
LBool (protect o_lte_dur_dur x y)
| Gt_int_int, [LInt x; LInt y] -> LBool (o_gt_int_int x y)
| Gt_rat_rat, [LRat x; LRat y] -> LBool (o_gt_rat_rat x y)
| Gt_mon_mon, [LMoney x; LMoney y] -> LBool (o_gt_mon_mon x y)
| Gt_dat_dat, [LDate x; LDate y] -> LBool (o_gt_dat_dat x y)
| Gt_dur_dur, [LDuration x; LDuration y] ->
LBool (protect o_gt_dur_dur x y)
| Gte_int_int, [LInt x; LInt y] -> LBool (o_gte_int_int x y)
| Gte_rat_rat, [LRat x; LRat y] -> LBool (o_gte_rat_rat x y)
| Gte_mon_mon, [LMoney x; LMoney y] -> LBool (o_gte_mon_mon x y)
| Gte_dat_dat, [LDate x; LDate y] -> LBool (o_gte_dat_dat x y)
| Gte_dur_dur, [LDuration x; LDuration y] ->
LBool (protect o_gte_dur_dur x y)
| Eq_int_int, [LInt x; LInt y] -> LBool (o_eq_int_int x y)
| Eq_rat_rat, [LRat x; LRat y] -> LBool (o_eq_rat_rat x y)
| Eq_mon_mon, [LMoney x; LMoney y] -> LBool (o_eq_mon_mon x y)
| Eq_dat_dat, [LDate x; LDate y] -> LBool (o_eq_dat_dat x y)
| Eq_dur_dur, [LDuration x; LDuration y] ->
LBool (protect o_eq_dur_dur x y)
| ( ( Minus_int | Minus_rat | Minus_mon | Minus_dur | ToRat_int
| ToRat_mon | ToMoney_rat | Round_rat | Round_mon | Add_int_int
| Add_rat_rat | Add_mon_mon | Add_dat_dur _ | Add_dur_dur
| Sub_int_int | Sub_rat_rat | Sub_mon_mon | Sub_dat_dat
| Sub_dat_dur | Sub_dur_dur | Mult_int_int | Mult_rat_rat
| Mult_mon_rat | Mult_dur_int | Div_int_int | Div_rat_rat
| Div_mon_mon | Div_mon_rat | Div_dur_dur | Lt_int_int
| Lt_rat_rat | Lt_mon_mon | Lt_dat_dat | Lt_dur_dur | Lte_int_int
| Lte_rat_rat | Lte_mon_mon | Lte_dat_dat | Lte_dur_dur
| Gt_int_int | Gt_rat_rat | Gt_mon_mon | Gt_dat_dat | Gt_dur_dur
| Gte_int_int | Gte_rat_rat | Gte_mon_mon | Gte_dat_dat
| Gte_dur_dur | Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dat_dat
| Eq_dur_dur ),
_ ) ->
err ()
in
ELit rlit)
~overloaded:(fun _ -> assert false)
match op, args with
| Length, [(EArray es, _)] ->
ELit (LInt (Runtime.integer_of_int (List.length es)))
| Log (entry, infos), [e'] ->
print_log ctx entry infos pos e';
Marked.unmark e'
| Eq, [(e1, _); (e2, _)] -> ELit (LBool (handle_eq ctx pos e1 e2))
| Map, [f; (EArray es, _)] ->
EArray
(List.map
(fun e' ->
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [e'] }) e'))
es)
| Reduce, [_; default; (EArray [], _)] -> Marked.unmark default
| Reduce, [f; _; (EArray (x0 :: xn), _)] ->
Marked.unmark
(List.fold_left
(fun acc x ->
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [acc; x] }) f))
x0 xn)
| Concat, [(EArray es1, _); (EArray es2, _)] -> EArray (es1 @ es2)
| Filter, [f; (EArray es, _)] ->
EArray
(List.filter
(fun e' ->
match
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [e'] }) e')
with
| ELit (LBool b), _ -> b
| _ ->
Errors.raise_spanned_error
(Expr.pos (List.nth args 0))
"This predicate evaluated to something else than a boolean \
(should not happen if the term was well-typed)")
es)
| Fold, [f; init; (EArray es, _)] ->
Marked.unmark
(List.fold_left
(fun acc e' ->
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [acc; e'] }) e'))
init es)
| (Length | Log _ | Eq | Map | Concat | Filter | Fold | Reduce), _ -> err ()
| Not, [(ELit (LBool b), _)] -> ELit (LBool (o_not b))
| GetDay, [(ELit (LDate d), _)] -> ELit (LInt (o_getDay d))
| GetMonth, [(ELit (LDate d), _)] -> ELit (LInt (o_getMonth d))
| GetYear, [(ELit (LDate d), _)] -> ELit (LInt (o_getYear d))
| FirstDayOfMonth, [(ELit (LDate d), _)] ->
ELit (LDate (o_firstDayOfMonth d))
| LastDayOfMonth, [(ELit (LDate d), _)] -> ELit (LDate (o_lastDayOfMonth d))
| And, [(ELit (LBool b1), _); (ELit (LBool b2), _)] ->
ELit (LBool (o_and b1 b2))
| Or, [(ELit (LBool b1), _); (ELit (LBool b2), _)] ->
ELit (LBool (o_or b1 b2))
| Xor, [(ELit (LBool b1), _); (ELit (LBool b2), _)] ->
ELit (LBool (o_xor b1 b2))
| ( ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth
| And | Or | Xor ),
_ ) ->
err ()
| Minus_int, [(ELit (LInt x), _)] -> ELit (LInt (o_minus_int x))
| Minus_rat, [(ELit (LRat x), _)] -> ELit (LRat (o_minus_rat x))
| Minus_mon, [(ELit (LMoney x), _)] -> ELit (LMoney (o_minus_mon x))
| Minus_dur, [(ELit (LDuration x), _)] -> ELit (LDuration (o_minus_dur x))
| ToRat_int, [(ELit (LInt i), _)] -> ELit (LRat (o_torat_int i))
| ToRat_mon, [(ELit (LMoney i), _)] -> ELit (LRat (o_torat_mon i))
| ToMoney_rat, [(ELit (LRat i), _)] -> ELit (LMoney (o_tomoney_rat i))
| Round_mon, [(ELit (LMoney m), _)] -> ELit (LMoney (o_round_mon m))
| Round_rat, [(ELit (LRat m), _)] -> ELit (LRat (o_round_rat m))
| Add_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LInt (o_add_int_int x y))
| Add_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (o_add_rat_rat x y))
| Add_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LMoney (o_add_mon_mon x y))
| Add_dat_dur r, [(ELit (LDate x), _); (ELit (LDuration y), _)] ->
ELit (LDate (o_add_dat_dur r x y))
| Add_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LDuration (o_add_dur_dur x y))
| Sub_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LInt (o_sub_int_int x y))
| Sub_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (o_sub_rat_rat x y))
| Sub_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LMoney (o_sub_mon_mon x y))
| Sub_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LDuration (o_sub_dat_dat x y))
| Sub_dat_dur, [(ELit (LDate x), _); (ELit (LDuration y), _)] ->
ELit (LDate (o_sub_dat_dur x y))
| Sub_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LDuration (o_sub_dur_dur x y))
| Mult_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LInt (o_mult_int_int x y))
| Mult_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (o_mult_rat_rat x y))
| Mult_mon_rat, [(ELit (LMoney x), _); (ELit (LRat y), _)] ->
ELit (LMoney (o_mult_mon_rat x y))
| Mult_dur_int, [(ELit (LDuration x), _); (ELit (LInt y), _)] ->
ELit (LDuration (o_mult_dur_int x y))
| Div_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LRat (protect o_div_int_int x y))
| Div_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (protect o_div_rat_rat x y))
| Div_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LRat (protect o_div_mon_mon x y))
| Div_mon_rat, [(ELit (LMoney x), _); (ELit (LRat y), _)] ->
ELit (LMoney (protect o_div_mon_rat x y))
| Div_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LRat (protect o_div_dur_dur x y))
| Lt_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_lt_int_int x y))
| Lt_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_lt_rat_rat x y))
| Lt_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_lt_mon_mon x y))
| Lt_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_lt_dat_dat x y))
| Lt_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_lt_dur_dur x y))
| Lte_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_lte_int_int x y))
| Lte_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_lte_rat_rat x y))
| Lte_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_lte_mon_mon x y))
| Lte_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_lte_dat_dat x y))
| Lte_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_lte_dur_dur x y))
| Gt_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_gt_int_int x y))
| Gt_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_gt_rat_rat x y))
| Gt_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_gt_mon_mon x y))
| Gt_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_gt_dat_dat x y))
| Gt_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_gt_dur_dur x y))
| Gte_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_gte_int_int x y))
| Gte_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_gte_rat_rat x y))
| Gte_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_gte_mon_mon x y))
| Gte_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_gte_dat_dat x y))
| Gte_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_gte_dur_dur x y))
| Eq_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_eq_int_int x y))
| Eq_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_eq_rat_rat x y))
| Eq_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_eq_mon_mon x y))
| Eq_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_eq_dat_dat x y))
| Eq_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_eq_dur_dur x y))
| ( ( Minus_int | Minus_rat | Minus_mon | Minus_dur | ToRat_int | ToRat_mon
| ToMoney_rat | Round_rat | Round_mon | Add_int_int | Add_rat_rat
| Add_mon_mon | Add_dat_dur _ | Add_dur_dur | Sub_int_int | Sub_rat_rat
| Sub_mon_mon | Sub_dat_dat | Sub_dat_dur | Sub_dur_dur | Mult_int_int
| Mult_rat_rat | Mult_mon_rat | Mult_dur_int | Div_int_int | Div_rat_rat
| Div_mon_mon | Div_mon_rat | Div_dur_dur | Lt_int_int | Lt_rat_rat
| Lt_mon_mon | Lt_dat_dat | Lt_dur_dur | Lte_int_int | Lte_rat_rat
| Lte_mon_mon | Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_rat_rat
| Gt_mon_mon | Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat
| Gte_mon_mon | Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat
| Eq_mon_mon | Eq_dat_dat | Eq_dur_dur ),
_ ) ->
err ()
and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
match Marked.unmark e with

4
compiler/scalc/ast.ml
View File

@ -25,6 +25,8 @@ let dead_value = VarName.fresh ("dead_value", Pos.no_pos)
let handle_default = FuncName.fresh ("handle_default", Pos.no_pos)
let handle_default_opt = FuncName.fresh ("handle_default_opt", Pos.no_pos)
type operator = [ `Monomorphic | `Polymorphic | `Resolved ] Shared_ast.operator
type expr = naked_expr Marked.pos
and naked_expr =
@ -36,7 +38,7 @@ and naked_expr =
| EArray : expr list -> naked_expr
| ELit : L.lit -> naked_expr
| EApp : expr * expr list -> naked_expr
| EOp : (lcalc, _) operator -> naked_expr
| EOp : operator -> naked_expr
type stmt =
| SInnerFuncDef of VarName.t Marked.pos * func

2
compiler/scalc/from_lcalc.ml
View File

@ -86,7 +86,7 @@ let rec translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : A.block * A.expr =
in
let new_args = List.rev new_args in
args_stmts, (A.EArray new_args, Expr.pos expr)
| EOp { op; _ } -> [], (A.EOp op, Expr.pos expr)
| EOp { op; _ } -> [], (A.EOp (Operator.translate None op), Expr.pos expr)
| ELit l -> [], (A.ELit l, Expr.pos expr)
| _ ->
let tmp_var =

5
compiler/scalc/to_python.ml
View File

@ -49,10 +49,7 @@ let format_log_entry (fmt : Format.formatter) (entry : log_entry) : unit =
| EndCall -> Format.fprintf fmt "%s" "← "
| PosRecordIfTrueBool -> Format.pp_print_string fmt "☛ "
let format_op
(type k)
(fmt : Format.formatter)
(op : (lcalc, k) operator Marked.pos) : unit =
let format_op (fmt : Format.formatter) (op : operator Marked.pos) : unit =
match Marked.unmark op with
| Log (entry, infos) -> assert false
| Minus_int | Minus_rat | Minus_mon | Minus_dur ->

326
compiler/shared_ast/definitions.ml
View File

@ -48,17 +48,63 @@ module StateName = Uid.Gen ()
(** Define a common base type for the expressions in most passes of the compiler *)
type desugared = [ `Desugared ]
(** {2 Phantom types used to select relevant cases on the generic AST}
we instantiate them with a polymorphic variant to take advantage of
sub-typing. The values aren't actually used. *)
type scopelang = [ `Scopelang ]
type dcalc = [ `Dcalc ]
type lcalc = [ `Lcalc ]
(** These types allow to select the features present in any given expression
type *)
type 'a any = [< desugared | scopelang | dcalc | lcalc ] as 'a
type op_kind = [ `Monomorphic | `Polymorphic | `Overloaded | `Resolved ]
type all_ast_features =
[ `SyntacticNames
| `ResolvedNames
| `ScopeVarStates
| `ScopeVarSimpl
| `ExplicitScopes
| `Assertions
| `DefaultTerms
| `Exceptions ]
type all = [ all_ast_features | op_kind ]
type desugared =
[ `Monomorphic
| `Polymorphic
| `Overloaded
| `SyntacticNames
| `ExplicitScopes
| `ScopeVarStates
| `DefaultTerms ]
type scopelang =
[ `Monomorphic
| `Polymorphic
| `Resolved
| `ResolvedNames
| `ExplicitScopes
| `ScopeVarSimpl
| `DefaultTerms ]
type dcalc =
[ `Monomorphic
| `Polymorphic
| `Resolved
| `ResolvedNames
| `Assertions
| `DefaultTerms ]
type lcalc =
[ `Monomorphic
| `Polymorphic
| `Resolved
| `ResolvedNames
| `Assertions
| `Exceptions ]
type 'a any = [< all ] as 'a
(** ['a any] is 'a, but adds the constraint that it should be restricted to
valid AST kinds *)
@ -95,134 +141,124 @@ type log_entry =
module Op = struct
(** Classification of operators on how they should be typed *)
type monomorphic =
| Monomorphic (** Operands and return types of the operator are fixed *)
type 'a any = [> op_kind ] as 'a
type polymorphic =
| Polymorphic
(** The operator is truly polymorphic: it's the same runtime function
that may work on multiple types. We require that resolving the
argument types from right to left trivially resolves all type
variables declared in the operator type. *)
type monomorphic = [ `Monomorphic ]
(** Operands and return types of the operator are fixed *)
type overloaded =
| Overloaded
(** The operator is ambiguous and requires the types of its arguments to
be known before it can be typed, using a pre-defined table *)
type polymorphic = [ `Polymorphic ]
(** The operator is truly polymorphic: it's the same runtime function that may
work on multiple types. We require that resolving the argument types from
right to left trivially resolves all type variables declared in the
operator type. *)
type resolved =
| Resolved (** Explicit monomorphic versions of the overloaded operators *)
type overloaded = [ `Overloaded ]
(** The operator is ambiguous and requires the types of its arguments to be
known before it can be typed, using a pre-defined table *)
(** Classification of operators. This could be inlined in the definition of
[t] but is more concise this way *)
type (_, _) kind =
| Monomorphic : ('a any, monomorphic) kind
| Polymorphic : ('a any, polymorphic) kind
| Overloaded : ([< desugared ], overloaded) kind
| Resolved : ([< scopelang | dcalc | lcalc ], resolved) kind
type resolved = [ `Resolved ]
(** Explicit monomorphic versions of the overloaded operators *)
type (_, _) t =
type _ t =
(* unary *)
(* * monomorphic *)
| Not : ('a any, monomorphic) t
| GetDay : ('a any, monomorphic) t
| GetMonth : ('a any, monomorphic) t
| GetYear : ('a any, monomorphic) t
| FirstDayOfMonth : ('a any, monomorphic) t
| LastDayOfMonth : ('a any, monomorphic) t
| Not : [> `Monomorphic ] t
| GetDay : [> `Monomorphic ] t
| GetMonth : [> `Monomorphic ] t
| GetYear : [> `Monomorphic ] t
| FirstDayOfMonth : [> `Monomorphic ] t
| LastDayOfMonth : [> `Monomorphic ] t
(* * polymorphic *)
| Length : ('a any, polymorphic) t
| Log : log_entry * Uid.MarkedString.info list -> ('a any, polymorphic) t
| Length : [> `Polymorphic ] t
| Log : log_entry * Uid.MarkedString.info list -> [> `Polymorphic ] t
(* * overloaded *)
| Minus : (desugared, overloaded) t
| Minus_int : ([< scopelang | dcalc | lcalc ], resolved) t
| Minus_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Minus_mon : ([< scopelang | dcalc | lcalc ], resolved) t
| Minus_dur : ([< scopelang | dcalc | lcalc ], resolved) t
| ToRat : (desugared, overloaded) t
| ToRat_int : ([< scopelang | dcalc | lcalc ], resolved) t
| ToRat_mon : ([< scopelang | dcalc | lcalc ], resolved) t
| ToMoney : (desugared, overloaded) t
| ToMoney_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Round : (desugared, overloaded) t
| Round_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Round_mon : ([< scopelang | dcalc | lcalc ], resolved) t
| Minus : [> `Overloaded ] t
| Minus_int : [> `Resolved ] t
| Minus_rat : [> `Resolved ] t
| Minus_mon : [> `Resolved ] t
| Minus_dur : [> `Resolved ] t
| ToRat : [> `Overloaded ] t
| ToRat_int : [> `Resolved ] t
| ToRat_mon : [> `Resolved ] t
| ToMoney : [> `Overloaded ] t
| ToMoney_rat : [> `Resolved ] t
| Round : [> `Overloaded ] t
| Round_rat : [> `Resolved ] t
| Round_mon : [> `Resolved ] t
(* binary *)
(* * monomorphic *)
| And : ('a any, monomorphic) t
| Or : ('a any, monomorphic) t
| Xor : ('a any, monomorphic) t
| And : [> `Monomorphic ] t
| Or : [> `Monomorphic ] t
| Xor : [> `Monomorphic ] t
(* * polymorphic *)
| Eq : ('a any, polymorphic) t
| Map : ('a any, polymorphic) t
| Concat : ('a any, polymorphic) t
| Filter : ('a any, polymorphic) t
| Reduce : ('a any, polymorphic) t
| Eq : [> `Polymorphic ] t
| Map : [> `Polymorphic ] t
| Concat : [> `Polymorphic ] t
| Filter : [> `Polymorphic ] t
| Reduce : [> `Polymorphic ] t
(* * overloaded *)
| Add : (desugared, overloaded) t
| Add_int_int : ([< scopelang | dcalc | lcalc ], resolved) t
| Add_rat_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Add_mon_mon : ([< scopelang | dcalc | lcalc ], resolved) t
| Add_dat_dur :
date_rounding
-> ([< scopelang | dcalc | lcalc ], resolved) t
| Add_dur_dur : ([< scopelang | dcalc | lcalc ], resolved) t
| Sub : (desugared, overloaded) t
| Sub_int_int : ([< scopelang | dcalc | lcalc ], resolved) t
| Sub_rat_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Sub_mon_mon : ([< scopelang | dcalc | lcalc ], resolved) t
| Sub_dat_dat : ([< scopelang | dcalc | lcalc ], resolved) t
| Sub_dat_dur : ([< scopelang | dcalc | lcalc ], resolved) t
| Sub_dur_dur : ([< scopelang | dcalc | lcalc ], resolved) t
| Mult : (desugared, overloaded) t
| Mult_int_int : ([< scopelang | dcalc | lcalc ], resolved) t
| Mult_rat_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Mult_mon_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Mult_dur_int : ([< scopelang | dcalc | lcalc ], resolved) t
| Div : (desugared, overloaded) t
| Div_int_int : ([< scopelang | dcalc | lcalc ], resolved) t
| Div_rat_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Div_mon_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Div_mon_mon : ([< scopelang | dcalc | lcalc ], resolved) t
| Div_dur_dur : ([< scopelang | dcalc | lcalc ], resolved) t
| Lt : (desugared, overloaded) t
| Lt_int_int : ([< scopelang | dcalc | lcalc ], resolved) t
| Lt_rat_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Lt_mon_mon : ([< scopelang | dcalc | lcalc ], resolved) t
| Lt_dat_dat : ([< scopelang | dcalc | lcalc ], resolved) t
| Lt_dur_dur : ([< scopelang | dcalc | lcalc ], resolved) t
| Lte : (desugared, overloaded) t
| Lte_int_int : ([< scopelang | dcalc | lcalc ], resolved) t
| Lte_rat_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Lte_mon_mon : ([< scopelang | dcalc | lcalc ], resolved) t
| Lte_dat_dat : ([< scopelang | dcalc | lcalc ], resolved) t
| Lte_dur_dur : ([< scopelang | dcalc | lcalc ], resolved) t
| Gt : (desugared, overloaded) t
| Gt_int_int : ([< scopelang | dcalc | lcalc ], resolved) t
| Gt_rat_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Gt_mon_mon : ([< scopelang | dcalc | lcalc ], resolved) t
| Gt_dat_dat : ([< scopelang | dcalc | lcalc ], resolved) t
| Gt_dur_dur : ([< scopelang | dcalc | lcalc ], resolved) t
| Gte : (desugared, overloaded) t
| Gte_int_int : ([< scopelang | dcalc | lcalc ], resolved) t
| Gte_rat_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Gte_mon_mon : ([< scopelang | dcalc | lcalc ], resolved) t
| Gte_dat_dat : ([< scopelang | dcalc | lcalc ], resolved) t
| Gte_dur_dur : ([< scopelang | dcalc | lcalc ], resolved) t
| Add : [> `Overloaded ] t
| Add_int_int : [> `Resolved ] t
| Add_rat_rat : [> `Resolved ] t
| Add_mon_mon : [> `Resolved ] t
| Add_dat_dur : date_rounding -> [> `Resolved ] t
| Add_dur_dur : [> `Resolved ] t
| Sub : [> `Overloaded ] t
| Sub_int_int : [> `Resolved ] t
| Sub_rat_rat : [> `Resolved ] t
| Sub_mon_mon : [> `Resolved ] t
| Sub_dat_dat : [> `Resolved ] t
| Sub_dat_dur : [> `Resolved ] t
| Sub_dur_dur : [> `Resolved ] t
| Mult : [> `Overloaded ] t
| Mult_int_int : [> `Resolved ] t
| Mult_rat_rat : [> `Resolved ] t
| Mult_mon_rat : [> `Resolved ] t
| Mult_dur_int : [> `Resolved ] t
| Div : [> `Overloaded ] t
| Div_int_int : [> `Resolved ] t
| Div_rat_rat : [> `Resolved ] t
| Div_mon_rat : [> `Resolved ] t
| Div_mon_mon : [> `Resolved ] t
| Div_dur_dur : [> `Resolved ] t
| Lt : [> `Overloaded ] t
| Lt_int_int : [> `Resolved ] t
| Lt_rat_rat : [> `Resolved ] t
| Lt_mon_mon : [> `Resolved ] t
| Lt_dat_dat : [> `Resolved ] t
| Lt_dur_dur : [> `Resolved ] t
| Lte : [> `Overloaded ] t
| Lte_int_int : [> `Resolved ] t
| Lte_rat_rat : [> `Resolved ] t
| Lte_mon_mon : [> `Resolved ] t
| Lte_dat_dat : [> `Resolved ] t
| Lte_dur_dur : [> `Resolved ] t
| Gt : [> `Overloaded ] t
| Gt_int_int : [> `Resolved ] t
| Gt_rat_rat : [> `Resolved ] t
| Gt_mon_mon : [> `Resolved ] t
| Gt_dat_dat : [> `Resolved ] t
| Gt_dur_dur : [> `Resolved ] t
| Gte : [> `Overloaded ] t
| Gte_int_int : [> `Resolved ] t
| Gte_rat_rat : [> `Resolved ] t
| Gte_mon_mon : [> `Resolved ] t
| Gte_dat_dat : [> `Resolved ] t
| Gte_dur_dur : [> `Resolved ] t
(* Todo: Eq is not an overload at the moment, but it should be one. The
trick is that it needs generation of specific code for arrays, every
struct and enum: operators [Eq_structs of StructName.t], etc. *)
| Eq_int_int : ([< scopelang | dcalc | lcalc ], resolved) t
| Eq_rat_rat : ([< scopelang | dcalc | lcalc ], resolved) t
| Eq_mon_mon : ([< scopelang | dcalc | lcalc ], resolved) t
| Eq_dur_dur : ([< scopelang | dcalc | lcalc ], resolved) t
| Eq_dat_dat : ([< scopelang | dcalc | lcalc ], resolved) t
| Eq_int_int : [> `Resolved ] t
| Eq_rat_rat : [> `Resolved ] t
| Eq_mon_mon : [> `Resolved ] t
| Eq_dur_dur : [> `Resolved ] t
| Eq_dat_dat : [> `Resolved ] t
(* ternary *)
(* * polymorphic *)
| Fold : ('a any, polymorphic) t
| Fold : [> `Polymorphic ] t
end
type ('a, 'k) operator = ('a any, 'k) Op.t
type 'a operator = 'a Op.t
type except = ConflictError | EmptyError | NoValueProvided | Crash
(** {2 Generic expressions} *)
@ -231,33 +267,31 @@ type except = ConflictError | EmptyError | NoValueProvided | Crash
(** Literals are the same throughout compilation except for the [LEmptyError]
case which is eliminated midway through. *)
type 'a glit =
type _ glit =
| LBool : bool -> 'a glit
| LEmptyError : [< desugared | scopelang | dcalc ] glit
| LInt : Runtime.integer -> 'a glit
| LRat : Runtime.decimal -> 'a glit
| LMoney : Runtime.money -> 'a glit
| LUnit : 'a glit
| LDate : date -> 'a glit
| LDuration : duration -> 'a glit
| LEmptyError : [> `DefaultTerms ] glit
(** Locations are handled differently in [desugared] and [scopelang] *)
type 'a glocation =
| DesugaredScopeVar :
ScopeVar.t Marked.pos * StateName.t option
-> desugared glocation
| ScopelangScopeVar : ScopeVar.t Marked.pos -> scopelang glocation
-> [> `ScopeVarStates ] glocation
| ScopelangScopeVar : ScopeVar.t Marked.pos -> [> `ScopeVarSimpl ] glocation
| SubScopeVar :
ScopeName.t * SubScopeName.t Marked.pos * ScopeVar.t Marked.pos
-> [< desugared | scopelang ] glocation
| ToplevelVar :
TopdefName.t Marked.pos
-> [< desugared | scopelang ] glocation
-> [> `ExplicitScopes ] glocation
| ToplevelVar : TopdefName.t Marked.pos -> [> `ExplicitScopes ] glocation
type ('a, 't) gexpr = (('a, 't) naked_gexpr, 't) Marked.t
(** 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 example,
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.
@ -272,93 +306,99 @@ type ('a, 't) gexpr = (('a, 't) naked_gexpr, 't) Marked.t
and ('a, 't) naked_gexpr =
(* Constructors common to all ASTs *)
| ELit : 'a glit -> ('a any, 't) naked_gexpr
| ELit : 'a glit -> (([< all ] as 'a), 't) naked_gexpr
| EApp : {
f : ('a, 't) gexpr;
args : ('a, 't) gexpr list;
}
-> ('a any, 't) naked_gexpr
| EOp : { op : ('a, _) operator; tys : typ list } -> ('a any, 't) naked_gexpr
| EArray : ('a, 't) gexpr list -> ('a any, 't) naked_gexpr
| EVar : ('a, 't) naked_gexpr Bindlib.var -> ('a any, 't) naked_gexpr
-> (([< all ] as 'a), 't) naked_gexpr
| EOp : {
op : 'a operator;
tys : typ list;
}
-> (([< all ] as 'a), 't) naked_gexpr
| EArray : ('a, 't) gexpr list -> (([< all ] as 'a), 't) naked_gexpr
| EVar :
('a, 't) naked_gexpr Bindlib.var
-> (([< all ] as 'a), 't) naked_gexpr
| EAbs : {
binder : (('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder;
tys : typ list;
}
-> ('a any, 't) naked_gexpr
-> (([< all ] as 'a), 't) naked_gexpr
| EIfThenElse : {
cond : ('a, 't) gexpr;
etrue : ('a, 't) gexpr;
efalse : ('a, 't) gexpr;
}
-> ('a any, 't) naked_gexpr
-> (([< all ] as 'a), 't) naked_gexpr
| EStruct : {
name : StructName.t;
fields : ('a, 't) gexpr StructField.Map.t;
}
-> ('a any, 't) naked_gexpr
-> (([< all ] as 'a), 't) naked_gexpr
| EInj : {
name : EnumName.t;
e : ('a, 't) gexpr;
cons : EnumConstructor.t;
}
-> ('a any, 't) naked_gexpr
-> (([< all ] as 'a), 't) naked_gexpr
| EMatch : {
name : EnumName.t;
e : ('a, 't) gexpr;
cases : ('a, 't) gexpr EnumConstructor.Map.t;
}
-> ('a any, 't) naked_gexpr
| ETuple : ('a, 't) gexpr list -> ('a any, 't) naked_gexpr
-> (([< all ] as 'a), 't) naked_gexpr
| ETuple : ('a, 't) gexpr list -> (([< all ] as 'a), 't) naked_gexpr
| ETupleAccess : {
e : ('a, 't) gexpr;
index : int;
size : int;
}
-> ('a any, 't) naked_gexpr
-> (([< all ] as 'a), 't) naked_gexpr
(* Early stages *)
| ELocation :
'a glocation
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
-> (([< all > `ExplicitScopes ] as 'a), 't) naked_gexpr
| EScopeCall : {
scope : ScopeName.t;
args : ('a, 't) gexpr ScopeVar.Map.t;
}
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
-> (([< all > `ExplicitScopes ] as 'a), 't) naked_gexpr
| EDStructAccess : {
name_opt : StructName.t option;
e : ('a, 't) gexpr;
field : IdentName.t;
}
-> ((desugared as 'a), 't) naked_gexpr
-> (([< all > `SyntacticNames ] as 'a), 't) naked_gexpr
(** [desugared] has ambiguous struct fields *)
| EStructAccess : {
name : StructName.t;
e : ('a, 't) gexpr;
field : StructField.t;
}
-> (([< scopelang | dcalc | lcalc ] as 'a), 't) naked_gexpr
-> (([< all > `ResolvedNames ] as 'a), 't) naked_gexpr
(** Resolved struct/enums, after [desugared] *)
(* Lambda-like *)
| EAssert : ('a, 't) gexpr -> (([< dcalc | lcalc ] as 'a), 't) naked_gexpr
| EAssert : ('a, 't) gexpr -> (([< all > `Assertions ] as 'a), 't) naked_gexpr
(* Default terms *)
| EDefault : {
excepts : ('a, 't) gexpr list;
just : ('a, 't) gexpr;
cons : ('a, 't) gexpr;
}
-> (([< desugared | scopelang | dcalc ] as 'a), 't) naked_gexpr
-> (([< all > `DefaultTerms ] as 'a), 't) naked_gexpr
| EErrorOnEmpty :
('a, 't) gexpr
-> (([< desugared | scopelang | dcalc ] as 'a), 't) naked_gexpr
-> (([< all > `DefaultTerms ] as 'a), 't) naked_gexpr
(* Lambda calculus with exceptions *)
| ERaise : except -> ((lcalc as 'a), 't) naked_gexpr
| ERaise : except -> (([< all > `Exceptions ] as 'a), 't) naked_gexpr
| ECatch : {
body : ('a, 't) gexpr;
exn : except;
handler : ('a, 't) gexpr;
}
-> ((lcalc as 'a), 't) naked_gexpr
-> (([< all > `Exceptions ] as 'a), 't) naked_gexpr
type ('a, 't) boxed_gexpr = (('a, 't) naked_gexpr Bindlib.box, 't) Marked.t
(** The annotation is lifted outside of the box for expressions *)

8
compiler/shared_ast/expr.ml
View File

@ -214,7 +214,7 @@ let map
| EApp { f = e1; args } -> eapp (f e1) (List.map f args) m
| EOp { op; tys } -> eop op tys m
| EArray args -> earray (List.map f args) m
| EVar v -> evar (Var.translate v) m
| EVar v -> evar (Var.translate_mark v) m
| EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in
let body = f body in
@ -383,7 +383,7 @@ let map_gather
(* - *)
(** See [Bindlib.box_term] documentation for why we are doing that. *)
let rec rebox e = map ~f:rebox e
let rec rebox (e : ('a any, 't) gexpr) = map ~f:rebox e
let box e = Marked.same_mark_as (Bindlib.box (Marked.unmark e)) e
let unbox (e, m) = Bindlib.unbox e, m
@ -650,11 +650,11 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
| EInj _, _ -> -1 | _, EInj _ -> 1
| EAssert _, _ -> -1 | _, EAssert _ -> 1
| EDefault _, _ -> -1 | _, EDefault _ -> 1
| EErrorOnEmpty _, _ -> . | _, EErrorOnEmpty _ -> .
| EErrorOnEmpty _, _ -> -1 | _, EErrorOnEmpty _ -> 1
| ERaise _, _ -> -1 | _, ERaise _ -> 1
| ECatch _, _ -> . | _, ECatch _ -> .
let rec free_vars : type a. (a, 't) gexpr -> (a, 't) gexpr Var.Set.t = function
let rec free_vars : ('a, 't) gexpr -> ('a, 't) gexpr Var.Set.t = function
| EVar v, _ -> Var.Set.singleton v
| EAbs { binder; _ }, _ ->
let vs, body = Bindlib.unmbind binder in

77
compiler/shared_ast/expr.mli
View File

@ -28,7 +28,7 @@ val box : ('a, 't) gexpr -> ('a, 't) boxed_gexpr
val unbox : ('a, 't) boxed_gexpr -> ('a, 't) gexpr
(** For closed expressions, similar to [Bindlib.unbox] *)
val rebox : ('a, 't) gexpr -> ('a, 't) boxed_gexpr
val rebox : ('a any, 't) gexpr -> ('a, 't) boxed_gexpr
(** Rebuild the whole term, re-binding all variables and exposing free variables *)
val evar : ('a, 't) gexpr Var.t -> 't -> ('a, 't) boxed_gexpr
@ -43,101 +43,101 @@ val subst :
('a, 't) gexpr list ->
('a, 't) gexpr
val etuple : ('a any, 't) boxed_gexpr list -> 't -> ('a, 't) boxed_gexpr
val etuple : ('a, 't) boxed_gexpr list -> 't -> ('a any, 't) boxed_gexpr
val etupleaccess :
('a any, 't) boxed_gexpr -> int -> int -> 't -> ('a, 't) boxed_gexpr
('a, 't) boxed_gexpr -> int -> int -> 't -> ('a any, 't) boxed_gexpr
val earray : ('a any, 't) boxed_gexpr list -> 't -> ('a, 't) boxed_gexpr
val elit : 'a any glit -> 't -> ('a, 't) boxed_gexpr
val earray : ('a, 't) boxed_gexpr list -> 't -> ('a any, 't) boxed_gexpr
val elit : 'a glit -> 't -> ('a any, 't) boxed_gexpr
val eabs :
(('a any, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder Bindlib.box ->
(('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder Bindlib.box ->
typ list ->
't ->
('a, 't) boxed_gexpr
('a any, 't) boxed_gexpr
val eapp :
('a any, 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
('a, 't) boxed_gexpr list ->
't ->
('a, 't) boxed_gexpr
('a any, 't) boxed_gexpr
val eassert :
(([< dcalc | lcalc ] as 'a), 't) boxed_gexpr -> 't -> ('a, 't) boxed_gexpr
('a, 't) boxed_gexpr -> 't -> (([< all > `Assertions ] as 'a), 't) boxed_gexpr
val eop : ('a any, 'k) operator -> typ list -> 't -> ('a, 't) boxed_gexpr
val eop : 'a operator -> typ list -> 't -> (([< all ] as 'a), 't) boxed_gexpr
val edefault :
(([< desugared | scopelang | dcalc ] as 'a), 't) boxed_gexpr list ->
('a, 't) boxed_gexpr list ->
('a, 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
't ->
('a, 't) boxed_gexpr
(([< all > `DefaultTerms ] as 'a), 't) boxed_gexpr
val eifthenelse :
('a any, 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
't ->
('a, 't) boxed_gexpr
('a any, 't) boxed_gexpr
val eerroronempty :
(([< desugared | scopelang | dcalc ] as 'a), 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
't ->
('a, 't) boxed_gexpr
(([< all > `DefaultTerms ] as 'a), 't) boxed_gexpr
val ecatch :
(lcalc, 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
except ->
(lcalc, 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
't ->
(lcalc, 't) boxed_gexpr
(([< all > `Exceptions ] as 'a), 't) boxed_gexpr
val eraise : except -> 't -> (lcalc, 't) boxed_gexpr
val eraise : except -> 't -> ([< all > `Exceptions ], 't) boxed_gexpr
val elocation :
([< desugared | scopelang ] as 'a) glocation -> 't -> ('a, 't) boxed_gexpr
'a glocation -> 't -> (([< all > `ExplicitScopes ] as 'a), 't) boxed_gexpr
val estruct :
StructName.t ->
('a any, 't) boxed_gexpr StructField.Map.t ->
('a, 't) boxed_gexpr StructField.Map.t ->
't ->
('a, 't) boxed_gexpr
('a any, 't) boxed_gexpr
val edstructaccess :
(desugared, 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
IdentName.t ->
StructName.t option ->
't ->
(desugared, 't) boxed_gexpr
(([< all > `SyntacticNames ] as 'a), 't) boxed_gexpr
val estructaccess :
(([< scopelang | dcalc | lcalc ] as 'a), 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
StructField.t ->
StructName.t ->
't ->
('a, 't) boxed_gexpr
(([< all > `ResolvedNames ] as 'a), 't) boxed_gexpr
val einj :
('a any, 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
EnumConstructor.t ->
EnumName.t ->
't ->
('a, 't) boxed_gexpr
('a any, 't) boxed_gexpr
val ematch :
('a any, 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
EnumName.t ->
('a, 't) boxed_gexpr EnumConstructor.Map.t ->
't ->
('a, 't) boxed_gexpr
('a any, 't) boxed_gexpr
val escopecall :
ScopeName.t ->
(([< desugared | scopelang ] as 'a), 't) boxed_gexpr ScopeVar.Map.t ->
('a, 't) boxed_gexpr ScopeVar.Map.t ->
't ->
('a, 't) boxed_gexpr
(([< all > `ExplicitScopes ] as 'a), 't) boxed_gexpr
(** Manipulation of marks *)
@ -266,7 +266,7 @@ val make_app :
('a, 'm mark) boxed_gexpr
val empty_thunked_term :
'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) boxed_gexpr
'm mark -> ([< all > `DefaultTerms ], 'm mark) boxed_gexpr
val make_let_in :
('a, 'm mark) gexpr Var.t ->
@ -285,11 +285,11 @@ val make_multiple_let_in :
('a, 'm mark) boxed_gexpr
val make_default :
(([< desugared | scopelang | dcalc ] as 'a), 't) boxed_gexpr list ->
('a, 't) boxed_gexpr list ->
('a, 't) boxed_gexpr ->
('a, 't) boxed_gexpr ->
't ->
('a, 't) boxed_gexpr
(([< all > `Polymorphic `DefaultTerms ] as 'a), 't) boxed_gexpr
(** [make_default ?pos exceptions just cons] builds a term semantically
equivalent to [<exceptions | just :- cons>] (the [EDefault] constructor)
while avoiding redundant nested constructions. The position is extracted
@ -310,7 +310,8 @@ val make_tuple :
(** {2 Transformations} *)
val remove_logging_calls : ('a any, 't) gexpr -> ('a, 't) boxed_gexpr
val remove_logging_calls :
(([< all > `Polymorphic ] as 'a), 't) gexpr -> ('a, 't) boxed_gexpr
(** Removes all calls to [Log] unary operators in the AST, replacing them by
their argument. *)

138
compiler/shared_ast/operator.ml
View File

@ -18,7 +18,7 @@ open Catala_utils
open Definitions
include Definitions.Op
let name : type a k. (a, k) t -> string = function
let name : type a. a t -> string = function
| Not -> "o_not"
| Length -> "o_length"
| GetDay -> "o_getDay"
@ -124,7 +124,7 @@ let compare_log_entries l1 l2 =
| PosRecordIfTrueBool, _ -> .
| _, PosRecordIfTrueBool -> .
let compare (type a k a2 k2) (t1 : (a, k) t) (t2 : (a2, k2) t) =
let compare (type a1 a2) (t1 : a1 t) (t2 : a2 t) =
match[@ocamlformat "disable"] t1, t2 with
| Log (l1, info1), Log (l2, info2) -> (
match compare_log_entries l1 l2 with
@ -296,18 +296,18 @@ let compare (type a k a2 k2) (t1 : (a, k) t) (t2 : (a2, k2) t) =
| Eq_dur_dur, _ -> -1 | _, Eq_dur_dur -> 1
| Fold, _ | _, Fold -> .
let equal (type a k a2 k2) (t1 : (a, k) t) (t2 : (a2, k2) t) = compare t1 t2 = 0
let equal t1 t2 = compare t1 t2 = 0
(* Classification of operators *)
let kind_dispatch :
type a b k.
polymorphic:((_, polymorphic) t -> b) ->
monomorphic:((_, monomorphic) t -> b) ->
?overloaded:((_, overloaded) t -> b) ->
?resolved:((_, resolved) t -> b) ->
(a, k) t ->
b =
type a.
polymorphic:([> polymorphic ] t -> 'b) ->
monomorphic:([> monomorphic ] t -> 'b) ->
?overloaded:([> overloaded ] t -> 'b) ->
?resolved:([> resolved ] t -> 'b) ->
a t ->
'b =
fun ~polymorphic ~monomorphic ?(overloaded = fun _ -> assert false)
?(resolved = fun _ -> assert false) op ->
match op with
@ -332,88 +332,30 @@ let kind_dispatch :
| Eq_mon_mon | Eq_dat_dat | Eq_dur_dur ) as op ->
resolved op
(* Glorified identity... allowed operators are the same in scopelang, dcalc,
lcalc *)
let translate :
type k.
date_rounding option ->
([< scopelang | dcalc | lcalc ], k) t ->
([< scopelang | dcalc | lcalc ], k) t =
fun r op ->
match op with
| Length -> Length
| Log (i, l) -> Log (i, l)
| Eq -> Eq
| Map -> Map
| Concat -> Concat
| Filter -> Filter
| Reduce -> Reduce
| Fold -> Fold
| Not -> Not
| GetDay -> GetDay
| GetMonth -> GetMonth
| GetYear -> GetYear
| FirstDayOfMonth -> FirstDayOfMonth
| LastDayOfMonth -> LastDayOfMonth
| And -> And
| Or -> Or
| Xor -> Xor
| Minus_int -> Minus_int
| Minus_rat -> Minus_rat
| Minus_mon -> Minus_mon
| Minus_dur -> Minus_dur
| ToRat_int -> ToRat_int
| ToRat_mon -> ToRat_mon
| ToMoney_rat -> ToMoney_rat
| Round_rat -> Round_rat
| Round_mon -> Round_mon
| Add_int_int -> Add_int_int
| Add_rat_rat -> Add_rat_rat
| Add_mon_mon -> Add_mon_mon
let translate
(r : date_rounding option)
(t : [< scopelang | dcalc | lcalc > `Monomorphic `Polymorphic `Resolved ] t)
=
match t with
| Add_dat_dur rmode -> Add_dat_dur (Option.value r ~default:rmode)
| Add_dur_dur -> Add_dur_dur
| Sub_int_int -> Sub_int_int
| Sub_rat_rat -> Sub_rat_rat
| Sub_mon_mon -> Sub_mon_mon
| Sub_dat_dat -> Sub_dat_dat
| Sub_dat_dur -> Sub_dat_dur
| Sub_dur_dur -> Sub_dur_dur
| Mult_int_int -> Mult_int_int
| Mult_rat_rat -> Mult_rat_rat
| Mult_mon_rat -> Mult_mon_rat
| Mult_dur_int -> Mult_dur_int
| Div_int_int -> Div_int_int
| Div_rat_rat -> Div_rat_rat
| Div_mon_mon -> Div_mon_mon
| Div_mon_rat -> Div_mon_rat
| Div_dur_dur -> Div_dur_dur
| Lt_int_int -> Lt_int_int
| Lt_rat_rat -> Lt_rat_rat
| Lt_mon_mon -> Lt_mon_mon
| Lt_dat_dat -> Lt_dat_dat
| Lt_dur_dur -> Lt_dur_dur
| Lte_int_int -> Lte_int_int
| Lte_rat_rat -> Lte_rat_rat
| Lte_mon_mon -> Lte_mon_mon
| Lte_dat_dat -> Lte_dat_dat
| Lte_dur_dur -> Lte_dur_dur
| Gt_int_int -> Gt_int_int
| Gt_rat_rat -> Gt_rat_rat
| Gt_mon_mon -> Gt_mon_mon
| Gt_dat_dat -> Gt_dat_dat
| Gt_dur_dur -> Gt_dur_dur
| Gte_int_int -> Gte_int_int
| Gte_rat_rat -> Gte_rat_rat
| Gte_mon_mon -> Gte_mon_mon
| Gte_dat_dat -> Gte_dat_dat
| Gte_dur_dur -> Gte_dur_dur
| Eq_int_int -> Eq_int_int
| Eq_rat_rat -> Eq_rat_rat
| Eq_mon_mon -> Eq_mon_mon
| Eq_dat_dat -> Eq_dat_dat
| Eq_dur_dur -> Eq_dur_dur
| ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth | And
| Or | Xor ) as op ->
op
| (Log _ | Length | Eq | Map | Concat | Filter | Reduce | Fold) as op -> op
| ( Minus_int | Minus_rat | Minus_mon | Minus_dur | ToRat_int | ToRat_mon
| ToMoney_rat | Round_rat | Round_mon | Add_int_int | Add_rat_rat
| Add_mon_mon | Add_dur_dur | Sub_int_int | Sub_rat_rat | Sub_mon_mon
| Sub_dat_dat | Sub_dat_dur | Sub_dur_dur | Mult_int_int | Mult_rat_rat
| Mult_mon_rat | Mult_dur_int | Div_int_int | Div_rat_rat | Div_mon_mon
| Div_mon_rat | Div_dur_dur | Lt_int_int | Lt_rat_rat | Lt_mon_mon
| Lt_dat_dat | Lt_dur_dur | Lte_int_int | Lte_rat_rat | Lte_mon_mon
| Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_rat_rat | Gt_mon_mon
| Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat | Gte_mon_mon
| Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat | Eq_mon_mon
| Eq_dat_dat | Eq_dur_dur ) as op ->
op
let monomorphic_type (op, pos) =
let monomorphic_type ((op : monomorphic t), pos) =
let args, ret =
match op with
| Not -> [TBool], TBool
@ -441,7 +383,7 @@ let monomorphic_type (op, pos) =
considering an operator with type ['a -> 'b -> 'c], for any given two among
['a], ['b] and ['c], there should be a unique solution for the third. *)
let resolved_type (op, pos) =
let resolved_type ((op : resolved t), pos) =
let args, ret =
match op with
| Minus_int -> [TInt], TInt
@ -501,8 +443,8 @@ let resolved_type (op, pos) =
in
TArrow (List.map (fun tau -> TLit tau, pos) args, (TLit ret, pos)), pos
let resolve_overload_aux (op : ('a, overloaded) t) (operands : typ_lit list) :
('b, resolved) t * [ `Straight | `Reversed ] =
let resolve_overload_aux (op : [< overloaded ] t) (operands : typ_lit list) :
[> resolved ] t * [ `Straight | `Reversed ] =
match op, operands with
| Minus, [TInt] -> Minus_int, `Straight
| Minus, [TRat] -> Minus_rat, `Straight
@ -561,10 +503,8 @@ let resolve_overload_aux (op : ('a, overloaded) t) (operands : typ_lit list) :
_ ) ->
raise Not_found
let resolve_overload
ctx
(op : ('a, overloaded) t Marked.pos)
(operands : typ list) : ('b, resolved) t * [ `Straight | `Reversed ] =
let resolve_overload ctx (op : overloaded t Marked.pos) (operands : typ list) :
[> resolved ] t * [ `Straight | `Reversed ] =
try
let operands =
List.map
@ -590,7 +530,7 @@ let resolve_overload
(Print.typ ctx))
operands
let overload_type ctx (op : ('a, overloaded) t Marked.pos) (operands : typ list)
: typ =
let overload_type ctx (op : overloaded t Marked.pos) (operands : typ list) : typ
=
let rop = fst (resolve_overload ctx op operands) in
resolved_type (Marked.same_mark_as rop op)

33
compiler/shared_ast/operator.mli
View File

@ -33,39 +33,36 @@ open Catala_utils
open Definitions
include module type of Definitions.Op
val equal : ('a1, 'k1) t -> ('a2, 'k2) t -> bool
val compare : ('a1, 'k1) t -> ('a2, 'k2) t -> int
val equal : 'a1 t -> 'a2 t -> bool
val compare : 'a1 t -> 'a2 t -> int
val name : ('a, 'k) t -> string
val name : 'a t -> string
(** Returns the operator name as a valid ident starting with a lowercase
character. This is different from Print.operator which returns operator
symbols, e.g. [+$]. *)
val kind_dispatch :
polymorphic:((_ any, polymorphic) t -> 'b) ->
monomorphic:((_ any, monomorphic) t -> 'b) ->
?overloaded:((desugared, overloaded) t -> 'b) ->
?resolved:(([< scopelang | dcalc | lcalc ], resolved) t -> 'b) ->
('a, 'k) t ->
polymorphic:([> polymorphic ] t -> 'b) ->
monomorphic:([> monomorphic ] t -> 'b) ->
?overloaded:([> overloaded ] t -> 'b) ->
?resolved:([> resolved ] t -> 'b) ->
'a t ->
'b
(** Calls one of the supplied functions depending on the kind of the operator *)
val translate :
date_rounding option ->
([< scopelang | dcalc | lcalc ], 'k) t ->
([< scopelang | dcalc | lcalc ], 'k) t
[< scopelang | dcalc | lcalc > `Monomorphic `Polymorphic `Resolved ] t ->
[> `Monomorphic | `Polymorphic | `Resolved ] t
(** An identity function that allows translating an operator between different
passes that don't change operator types *)
(** {2 Getting the types of operators} *)
val monomorphic_type : ('a any, monomorphic) t Marked.pos -> typ
val monomorphic_type : monomorphic t Marked.pos -> typ
val resolved_type : resolved t Marked.pos -> typ
val resolved_type :
([< scopelang | dcalc | lcalc ], resolved) t Marked.pos -> typ
val overload_type :
decl_ctx -> (desugared, overloaded) t Marked.pos -> typ list -> typ
val overload_type : decl_ctx -> overloaded t Marked.pos -> typ list -> typ
(** The type for typing overloads is different since the types of the operands
are required in advance.
@ -78,9 +75,9 @@ val overload_type :
val resolve_overload :
decl_ctx ->
(desugared, overloaded) t Marked.pos ->
overloaded t Marked.pos ->
typ list ->
([< scopelang | dcalc | lcalc ], resolved) t * [ `Straight | `Reversed ]
[> resolved ] t * [ `Straight | `Reversed ]
(** Some overloads are sugar for an operation with reversed operands, e.g.
[TRat * TMoney] is using [mult_mon_rat]. [`Reversed] is returned to signify
this case. *)

8
compiler/shared_ast/print.ml
View File

@ -154,7 +154,9 @@ let log_entry (fmt : Format.formatter) (entry : log_entry) : unit =
Cli.format_with_style [ANSITerminal.green] fmt "☛ ")
entry
let operator_to_string : type a k. (a, k) Op.t -> string = function
let operator_to_string : type a. a Op.t -> string =
let open Op in
function
| Not -> "~"
| Length -> "length"
| GetDay -> "get_day"
@ -241,7 +243,9 @@ let operator_to_string : type a k. (a, k) Op.t -> string = function
| Eq_dat_dat -> "=@"
| Fold -> "fold"
let operator (type k) (fmt : Format.formatter) (op : ('a, k) operator) : unit =
let operator : type a. Format.formatter -> a Op.t -> unit =
fun fmt op ->
let open Op in
match op with
| Log (entry, infos) ->
Format.fprintf fmt "%a@[<hov 2>[%a|%a]@]" op_style "log" log_entry entry

2
compiler/shared_ast/print.mli
View File

@ -35,7 +35,7 @@ val tlit : Format.formatter -> typ_lit -> unit
val location : Format.formatter -> 'a glocation -> unit
val typ : decl_ctx -> Format.formatter -> typ -> unit
val lit : Format.formatter -> 'a glit -> unit
val operator : Format.formatter -> ('a any, 'k) operator -> unit
val operator : Format.formatter -> 'a operator -> unit
val log_entry : Format.formatter -> log_entry -> unit
val except : Format.formatter -> except -> unit
val var : Format.formatter -> 'e Var.t -> unit

9
compiler/shared_ast/program.mli
View File

@ -26,14 +26,11 @@ val map_exprs :
'expr2 program Bindlib.box
val get_scope_body :
(([< dcalc | lcalc ], _) gexpr as 'e) program -> ScopeName.t -> 'e scope_body
((_ any, 't) gexpr as 'e) program -> ScopeName.t -> 'e scope_body
val untype :
(([< dcalc | lcalc ] as 'a), 'm mark) gexpr program ->
('a, untyped mark) gexpr program
val untype : ('a any, _ mark) gexpr program -> ('a, untyped mark) gexpr program
val to_expr :
(([< dcalc | lcalc ], _) gexpr as 'e) program -> ScopeName.t -> 'e boxed
val to_expr : ((_ any, _) gexpr as 'e) program -> ScopeName.t -> 'e boxed
(** Usage: [build_whole_program_expr program main_scope] builds an expression
corresponding to the main program and returning the main scope as a
function. *)

6
compiler/shared_ast/typing.ml
View File

@ -237,8 +237,8 @@ let lit_type (type a) (lit : a A.glit) : naked_typ =
functions separate. In particular [resolve_overloads] requires its argument
types to be known in advance. *)
let polymorphic_op_type (op : ('a, Operator.polymorphic) A.operator Marked.pos)
: unionfind_typ =
let polymorphic_op_type (op : Operator.polymorphic A.operator Marked.pos) :
unionfind_typ =
let open Operator in
let pos = Marked.get_mark op in
let any = lazy (UnionFind.make (TAny (Any.fresh ()), pos)) in
@ -267,7 +267,7 @@ let resolve_overload_ret_type
~leave_unresolved
(ctx : A.decl_ctx)
e
(op : ('a A.any, Operator.overloaded) A.operator)
(op : Operator.overloaded A.operator)
tys : unionfind_typ =
let op_ty =
Operator.overload_type ctx

3
compiler/shared_ast/var.ml
View File

@ -21,7 +21,7 @@ open Definitions
(** This module provides types and helpers for Bindlib variables on the [gexpr]
type *)
type 'e t = ('a, 't) naked_gexpr Bindlib.var constraint 'e = ('a any, 't) gexpr
type 'e t = ('a any, 't) naked_gexpr Bindlib.var constraint 'e = ('a, 't) gexpr
type 'e vars = ('a, 't) naked_gexpr Bindlib.mvar
constraint 'e = ('a any, 't) gexpr
@ -29,6 +29,7 @@ type 'e vars = ('a, 't) naked_gexpr Bindlib.mvar
let make (name : string) : 'e t = Bindlib.new_var (fun x -> EVar x) name
let compare = Bindlib.compare_vars
let eq = Bindlib.eq_vars
let translate_mark v = Bindlib.copy_var v (fun x -> EVar x) (Bindlib.name_of v)
let translate (v : 'e1 t) : 'e2 t =
Bindlib.copy_var v (fun x -> EVar x) (Bindlib.name_of v)

5
compiler/shared_ast/var.mli
View File

@ -21,7 +21,7 @@ open Definitions
(** This module provides types and helpers for Bindlib variables on the [gexpr]
type *)
type 'e t = ('a, 't) naked_gexpr Bindlib.var constraint 'e = ('a any, 't) gexpr
type 'e t = ('a any, 't) naked_gexpr Bindlib.var constraint 'e = ('a, 't) gexpr
type 'e vars = ('a, 't) naked_gexpr Bindlib.mvar
constraint 'e = ('a any, 't) gexpr
@ -30,6 +30,9 @@ val make : string -> 'e t
val compare : 'e t -> 'e t -> int
val eq : 'e t -> 'e t -> bool
val translate_mark :
('a any, 't1) naked_gexpr Bindlib.var -> ('a any, 't2) naked_gexpr Bindlib.var
val translate : 'e1 t -> 'e2 t
(** Needed when converting from one AST type to another. See the note of caution
on [Bindlib.copy_var]. *)

2
compiler/surface/dune
View File

@ -40,7 +40,7 @@
(rule
(target grammar.html)
(action
(run obelisk html -o %{target} %{dep:parser.mly})))
(run obelisk html -i -o %{target} %{dep:parser.mly})))
(documentation
(package catala)

3
compiler/verification/z3backend.real.ml
View File

@ -430,8 +430,7 @@ let is_leap_year = Runtime.is_leap_year
(** [translate_op] returns the Z3 expression corresponding to the application of
[op] to the arguments [args] **)
let rec translate_op :
type k.
context -> (dcalc, k) operator -> 'm expr list -> context * Expr.expr =
context -> dcalc operator -> 'm expr list -> context * Expr.expr =
fun ctx op args ->
let ill_formed () =
Format.kasprintf failwith

26779
french_law/js/french_law.js generated
View File

File diff suppressed because one or more lines are too long