CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into aides_logement_outre_mer

Browse Source
This commit is contained in:
Denis Merigoux 2023-04-03 14:05:34 +02:00
commit ad02a0959d
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
123 changed files with 2103 additions and 702 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
compiler/catala_utils/cli.ml
View File

@ -86,6 +86,7 @@ let style_flag = ref true
(* Max number of digits to show for decimal results *)
let max_prec_digits = ref 20
let trace_flag = ref false
let disable_warnings_flag = ref false
let optimize_flag = ref false
let disable_counterexamples = ref false
let avoid_exceptions_flag = ref false
@ -135,19 +136,26 @@ let trace_opt =
"Displays a trace of the interpreter's computation or generates \
logging instructions in translate programs.")
let disable_warnings_opt =
Arg.(
value
& flag
& info ["disable_warnings"]
~doc:"Disable all the warnings emitted by the compiler.")
let avoid_exceptions =
Arg.(
value
& flag
& info ["avoid_exceptions"]
~doc:"Compiles the default calculus without exceptions")
~doc:"Compiles the default calculus without exceptions.")
let closure_conversion =
Arg.(
value
& flag
& info ["closure_conversion"]
~doc:"Performs closure conversion on the lambda calculus")
~doc:"Performs closure conversion on the lambda calculus.")
let wrap_weaved_output =
Arg.(
@ -243,6 +251,7 @@ type options = {
language : string option;
max_prec_digits : int option;
trace : bool;
disable_warnings : bool;
disable_counterexamples : bool;
optimize : bool;
ex_scope : string option;
@ -263,6 +272,7 @@ let options =
plugins_dirs
language
max_prec_digits
disable_warnings
trace
disable_counterexamples
optimize
@ -278,6 +288,7 @@ let options =
plugins_dirs;
language;
max_prec_digits;
disable_warnings;
trace;
disable_counterexamples;
optimize;
@ -299,6 +310,7 @@ let options =
$ plugins_dirs
$ language
$ max_prec_digits_opt
$ disable_warnings_opt
$ trace_opt
$ disable_counterexamples_opt
$ optimize
@ -315,6 +327,10 @@ let set_option_globals options : unit =
| Always -> true
| Never -> false
| Auto -> Unix.isatty Unix.stdout);
(match options.max_prec_digits with
| None -> ()
| Some i -> max_prec_digits := i);
disable_warnings_flag := options.disable_warnings;
trace_flag := options.trace;
optimize_flag := options.optimize;
disable_counterexamples := options.disable_counterexamples;
@ -495,7 +511,8 @@ let error_print (format : ('a, out_channel, unit) format) =
Printf.eprintf ("%s" ^^ format ^^ "\n%!") (error_marker ())
let warning_print (format : ('a, out_channel, unit) format) =
Printf.printf ("%s" ^^ format ^^ "\n%!") (warning_marker ())
if !disable_warnings_flag then Printf.ifprintf stdout format
else Printf.printf ("%s" ^^ format ^^ "\n%!") (warning_marker ())
let warning_format (format : ('a, Format.formatter, unit) format) =
Format.printf ("%s" ^^ format ^^ "\n%!") (warning_marker ())

2
compiler/catala_utils/cli.mli
View File

@ -64,6 +64,7 @@ val max_prec_digits : int ref
(** Max number of digits to show for decimal results *)
val trace_flag : bool ref
val disable_warnings_flag : bool ref
val disable_counterexamples : bool ref
(** Disables model-generated counterexamples for proofs that fail. *)
@ -99,6 +100,7 @@ type options = {
language : string option;
max_prec_digits : int option;
trace : bool;
disable_warnings : bool;
disable_counterexamples : bool;
optimize : bool;
ex_scope : string option;

1
compiler/catala_web_interpreter.ml
View File

@ -23,6 +23,7 @@ let _ =
max_prec_digits = None;
closure_conversion = false;
trace;
disable_warnings = true;
disable_counterexamples = false;
optimize = false;
ex_scope = Some (Js.to_string scope);

2
compiler/dcalc/ast.ml
View File

@ -17,8 +17,6 @@
open Shared_ast
type lit = dcalc glit
type 'm naked_expr = (dcalc, 'm mark) naked_gexpr
and 'm expr = (dcalc, 'm mark) gexpr

2
compiler/dcalc/ast.mli
View File

@ -19,8 +19,6 @@
open Shared_ast
type lit = dcalc glit
type 'm naked_expr = (dcalc, 'm mark) naked_gexpr
and 'm expr = (dcalc, 'm mark) gexpr

12
compiler/dcalc/from_scopelang.ml
View File

@ -201,8 +201,8 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
match Marked.unmark e with
| EVar v -> Expr.evar (Var.Map.find v ctx.local_vars) m
| ELit
(( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _
| LDuration _ ) as l) ->
((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
l) ->
Expr.elit l m
| EStruct { name; fields } ->
let fields = StructField.Map.map (translate_expr ctx) fields in
@ -254,7 +254,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
let expr =
match str_field, expr with
| Some { scope_input_io = Desugared.Ast.Reentrant, _; _ }, None ->
Some (Expr.unbox (Expr.elit LEmptyError (mark_tany m pos)))
Some (Expr.unbox (Expr.eemptyerror (mark_tany m pos)))
| _ -> expr
in
match str_field, expr with
@ -555,8 +555,10 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
Expr.eifthenelse (translate_expr ctx cond) (translate_expr ctx etrue)
(translate_expr ctx efalse)
m
| EOp { op; tys } ->
Expr.eop (Operator.translate (Some ctx.date_rounding) op) tys m
| EOp { op = Add_dat_dur _; tys } ->
Expr.eop (Add_dat_dur ctx.date_rounding) tys m
| EOp { op; tys } -> Expr.eop (Operator.translate op) tys m
| EEmptyError -> Expr.eemptyerror m
| EErrorOnEmpty e' -> Expr.eerroronempty (translate_expr ctx e') m
| EArray es -> Expr.earray (List.map (translate_expr ctx) es) m

368
compiler/dcalc/interpreter.ml
View File

@ -23,7 +23,7 @@ module Runtime = Runtime_ocaml.Runtime
(** {1 Helpers} *)
let is_empty_error (e : 'm Ast.expr) : bool =
match Marked.unmark e with ELit LEmptyError -> true | _ -> false
match Marked.unmark e with EEmptyError -> true | _ -> false
let log_indent = ref 0
@ -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
@ -154,162 +150,184 @@ and evaluate_operator :
(should not happen if the term was well-typed)"
in
let open Runtime.Oper in
if List.exists (function ELit LEmptyError, _ -> true | _ -> false) args then
ELit LEmptyError
if List.exists (function EEmptyError, _ -> true | _ -> false) args then
EEmptyError
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
@ -332,7 +350,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
(List.length args)
| EOp { op; _ } ->
Marked.same_mark_as (evaluate_operator ctx op (Expr.pos e) args) e
| ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
| EEmptyError -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"function has not been reduced to a lambda at evaluation (should not \
@ -341,7 +359,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
| EStruct { fields = es; name } ->
let new_es = StructField.Map.map (evaluate_expr ctx) es in
if StructField.Map.exists (fun _ e -> is_empty_error e) new_es then
Marked.same_mark_as (ELit LEmptyError) e
Marked.same_mark_as EEmptyError e
else Marked.same_mark_as (EStruct { fields = new_es; name }) e
| EStructAccess { e = e1; name = s; field } -> (
let e1 = evaluate_expr ctx e1 in
@ -359,7 +377,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
"Invalid field access %a in struct %a (should not happen if the term \
was well-typed)"
StructField.format_t field StructName.format_t s)
| ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
| EEmptyError -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos e1)
"The expression %a should be a struct %a but is not (should not happen \
@ -379,7 +397,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
e size)
| EInj { e = e1; name; cons } ->
let e1' = evaluate_expr ctx e1 in
if is_empty_error e then Marked.same_mark_as (ELit LEmptyError) e
if is_empty_error e then Marked.same_mark_as EEmptyError e
else Marked.same_mark_as (EInj { e = e1'; name; cons }) e
| EMatch { e = e1; cases = es; name } -> (
let e1 = evaluate_expr ctx e1 in
@ -400,7 +418,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
in
let new_e = Marked.same_mark_as (EApp { f = es_n; args = [e1] }) e in
evaluate_expr ctx new_e
| ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
| EEmptyError -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos e1)
"Expected a term having a sum type as an argument to a match (should \
@ -412,9 +430,9 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
| 0 -> (
let just = evaluate_expr ctx just in
match Marked.unmark just with
| ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
| EEmptyError -> Marked.same_mark_as EEmptyError e
| ELit (LBool true) -> evaluate_expr ctx cons
| ELit (LBool false) -> Marked.same_mark_as (ELit LEmptyError) e
| ELit (LBool false) -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"Default justification has not been reduced to a boolean at \
@ -432,19 +450,19 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
match Marked.unmark (evaluate_expr ctx cond) with
| ELit (LBool true) -> evaluate_expr ctx etrue
| ELit (LBool false) -> evaluate_expr ctx efalse
| ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
| EEmptyError -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos cond)
"Expected a boolean literal for the result of this condition (should \
not happen if the term was well-typed)")
| EArray es ->
let new_es = List.map (evaluate_expr ctx) es in
if List.exists is_empty_error new_es then
Marked.same_mark_as (ELit LEmptyError) e
if List.exists is_empty_error new_es then Marked.same_mark_as EEmptyError e
else Marked.same_mark_as (EArray new_es) e
| EEmptyError -> Marked.same_mark_as EEmptyError e
| EErrorOnEmpty e' ->
let e' = evaluate_expr ctx e' in
if Marked.unmark e' = ELit LEmptyError then
if Marked.unmark e' = EEmptyError then
Errors.raise_spanned_error (Expr.pos e')
"This variable evaluated to an empty term (no rule that defined it \
applied in this situation)"
@ -497,7 +515,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
| _ ->
Cli.debug_format "%a" (Expr.format ctx) e';
Errors.raise_spanned_error (Expr.pos e') "Assertion failed")
| ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e
| EEmptyError -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos e')
"Expected a boolean literal for the result of this assertion (should \
@ -525,7 +543,7 @@ let interpret_program :
| TArrow (ty_in, ty_out) ->
Expr.make_abs
(Array.of_list @@ List.map (fun _ -> Var.make "_") ty_in)
(Bindlib.box (ELit LEmptyError), Expr.with_ty mark_e ty_out)
(Bindlib.box EEmptyError, Expr.with_ty mark_e ty_out)
ty_in (Expr.mark_pos mark_e)
| _ ->
Errors.raise_spanned_error (Marked.get_mark ty)

11
compiler/dcalc/optimizations.ml
View File

@ -29,7 +29,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
let e = Expr.map ~f:(partial_evaluation ctx) e in
let mark = Marked.get_mark e in
(* Then reduce the parent node *)
let reduce e =
let reduce (e : 'm expr) =
(* Todo: improve the handling of eapp(log,elit) cases here, it obfuscates
the matches and the log calls are not preserved, which would be a good
property *)
@ -99,9 +99,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
| EDefault { excepts; just; cons } -> (
(* TODO: mechanically prove each of these optimizations correct :) *)
let excepts =
List.filter
(fun except -> Marked.unmark except <> ELit LEmptyError)
excepts
List.filter (fun except -> Marked.unmark except <> EEmptyError) excepts
(* we can discard the exceptions that are always empty error *)
in
let value_except_count =
@ -137,7 +135,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
args = [(ELit (LBool false), _)];
} ),
_ ) ) ->
ELit LEmptyError
EEmptyError
| [], just when not !Cli.avoid_exceptions_flag ->
(* without exceptions, a default is just an [if then else] raising an
error in the else case. This exception is only valid in the context
@ -145,8 +143,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
flag to know if we will be compiling using exceptions or the option
monad. FIXME: move this optimisation somewhere else to avoid this
check *)
EIfThenElse
{ cond = just; etrue = cons; efalse = ELit LEmptyError, mark }
EIfThenElse { cond = just; etrue = cons; efalse = EEmptyError, mark }
| excepts, just -> EDefault { excepts; just; cons })
| EIfThenElse
{

27
compiler/desugared/ast.ml
View File

@ -145,7 +145,7 @@ let empty_rule
(parameters : (Uid.MarkedString.info * typ) list Marked.pos option) : rule =
{
rule_just = Expr.box (ELit (LBool false), Untyped { pos });
rule_cons = Expr.box (ELit LEmptyError, Untyped { pos });
rule_cons = Expr.box (EEmptyError, Untyped { pos });
rule_parameter =
Option.map
(Marked.map_under_mark
@ -247,3 +247,28 @@ let free_variables (def : rule RuleName.Map.t) : Pos.t ScopeDefMap.t =
in
add_locs acc locs)
def ScopeDefMap.empty
let fold_exprs ~(f : 'a -> expr -> 'a) ~(init : 'a) (p : program) : 'a =
let acc =
ScopeName.Map.fold
(fun _ scope acc ->
let acc =
ScopeDefMap.fold
(fun _ scope_def acc ->
RuleName.Map.fold
(fun _ rule acc ->
f
(f acc (Expr.unbox rule.rule_just))
(Expr.unbox rule.rule_cons))
scope_def.scope_def_rules acc)
scope.scope_defs acc
in
let acc =
List.fold_left
(fun acc assertion -> f acc (Expr.unbox assertion))
acc scope.scope_assertions
in
acc)
p.program_scopes init
in
TopdefName.Map.fold (fun _ (e, _) acc -> f acc e) p.program_topdefs acc

6
compiler/desugared/ast.mli
View File

@ -134,3 +134,9 @@ type program = {
val locations_used : expr -> LocationSet.t
val free_variables : rule RuleName.Map.t -> Pos.t ScopeDefMap.t
val fold_exprs : f:('a -> expr -> 'a) -> init:'a -> program -> 'a
(** Usage: [fold_exprs ~f ~init program] applies ~f to all the expressions
inside rules (justifications and consequences), expressions and top-level
definitions of the program. Note that there may be free variables in these
expressions. *)

203
compiler/desugared/linting.ml Normal file
View File

@ -0,0 +1,203 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2023 Inria, contributor:
Denis Merigoux <denis.merigoux@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
open Shared_ast
open Ast
open Catala_utils
(** If the variable is not an input, then it should be defined somewhere. *)
let detect_empty_definitions (p : program) : unit =
ScopeName.Map.iter
(fun (scope_name : ScopeName.t) scope ->
ScopeDefMap.iter
(fun scope_def_key scope_def ->
if
(match scope_def_key with ScopeDef.Var _ -> true | _ -> false)
&& RuleName.Map.is_empty scope_def.scope_def_rules
&& (not scope_def.scope_def_is_condition)
&&
match Marked.unmark scope_def.scope_def_io.io_input with
| Ast.NoInput -> true
| _ -> false
then
Errors.format_spanned_warning
(ScopeDef.get_position scope_def_key)
"In scope %a, the variable %a is declared but never defined; did \
you forget something?"
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" ScopeName.format_t scope_name)
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" Ast.ScopeDef.format_t scope_def_key))
scope.scope_defs)
p.program_scopes
let detect_unused_scope_vars (p : program) : unit =
let used_scope_vars =
Ast.fold_exprs
~f:(fun used_scope_vars e ->
let rec used_scope_vars_expr e used_scope_vars =
match Marked.unmark e with
| ELocation (DesugaredScopeVar (v, _)) ->
ScopeVar.Set.add (Marked.unmark v) used_scope_vars
| _ -> Expr.shallow_fold used_scope_vars_expr e used_scope_vars
in
used_scope_vars_expr e used_scope_vars)
~init:ScopeVar.Set.empty p
in
ScopeName.Map.iter
(fun (scope_name : ScopeName.t) scope ->
ScopeDefMap.iter
(fun scope_def_key scope_def ->
match scope_def_key with
| ScopeDef.Var (v, _)
when (not (ScopeVar.Set.mem v used_scope_vars))
&& not (Marked.unmark scope_def.scope_def_io.io_output) ->
Errors.format_spanned_warning
(ScopeDef.get_position scope_def_key)
"In scope %a, the variable %a is never used anywhere; maybe it's \
unnecessary?"
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" ScopeName.format_t scope_name)
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" Ast.ScopeDef.format_t scope_def_key)
| _ -> ())
scope.scope_defs)
p.program_scopes
let detect_unused_struct_fields (p : program) : unit =
let struct_fields_used =
Ast.fold_exprs
~f:(fun struct_fields_used e ->
let rec structs_fields_used_expr e struct_fields_used =
match Marked.unmark e with
| EDStructAccess { name_opt = Some name; e = e_struct; field } ->
let field =
StructName.Map.find name
(IdentName.Map.find field p.program_ctx.ctx_struct_fields)
in
StructField.Set.add field
(structs_fields_used_expr e_struct struct_fields_used)
| EStruct { name = _; fields } ->
StructField.Map.fold
(fun field e_field struct_fields_used ->
StructField.Set.add field
(structs_fields_used_expr e_field struct_fields_used))
fields struct_fields_used
| _ -> Expr.shallow_fold structs_fields_used_expr e struct_fields_used
in
structs_fields_used_expr e struct_fields_used)
~init:StructField.Set.empty p
in
let scope_out_structs_fields =
ScopeName.Map.fold
(fun _ out_struct acc ->
ScopeVar.Map.fold
(fun _ field acc -> StructField.Set.add field acc)
out_struct.out_struct_fields acc)
p.program_ctx.ctx_scopes StructField.Set.empty
in
StructName.Map.iter
(fun s_name fields ->
if
(not (StructField.Map.is_empty fields))
&& StructField.Map.for_all
(fun field _ ->
(not (StructField.Set.mem field struct_fields_used))
&& not (StructField.Set.mem field scope_out_structs_fields))
fields
then
Errors.format_spanned_warning
(snd (StructName.get_info s_name))
"The structure %a is never used; maybe it's unnecessary?"
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" StructName.format_t s_name)
else
StructField.Map.iter
(fun field _ ->
if
(not (StructField.Set.mem field struct_fields_used))
&& not (StructField.Set.mem field scope_out_structs_fields)
then
Errors.format_spanned_warning
(snd (StructField.get_info field))
"The field %a of struct %a is never used; maybe it's \
unnecessary?"
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" StructField.format_t field)
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" StructName.format_t s_name))
fields)
p.program_ctx.ctx_structs
let detect_unused_enum_constructors (p : program) : unit =
let enum_constructors_used =
Ast.fold_exprs
~f:(fun enum_constructors_used e ->
let rec enum_constructors_used_expr e enum_constructors_used =
match Marked.unmark e with
| EInj { name = _; e = e_enum; cons } ->
EnumConstructor.Set.add cons
(enum_constructors_used_expr e_enum enum_constructors_used)
| EMatch { e = e_match; name = _; cases } ->
let enum_constructors_used =
enum_constructors_used_expr e_match enum_constructors_used
in
EnumConstructor.Map.fold
(fun cons e_cons enum_constructors_used ->
EnumConstructor.Set.add cons
(enum_constructors_used_expr e_cons enum_constructors_used))
cases enum_constructors_used
| _ ->
Expr.shallow_fold enum_constructors_used_expr e
enum_constructors_used
in
enum_constructors_used_expr e enum_constructors_used)
~init:EnumConstructor.Set.empty p
in
EnumName.Map.iter
(fun e_name constructors ->
if
EnumConstructor.Map.for_all
(fun cons _ ->
not (EnumConstructor.Set.mem cons enum_constructors_used))
constructors
then
Errors.format_spanned_warning
(snd (EnumName.get_info e_name))
"The enumeration %a is never used; maybe it's unnecessary?"
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" EnumName.format_t e_name)
else
EnumConstructor.Map.iter
(fun constructor _ ->
if not (EnumConstructor.Set.mem constructor enum_constructors_used)
then
Errors.format_spanned_warning
(snd (EnumConstructor.get_info constructor))
"The constructor %a of enumeration %a is never used; maybe \
it's unnecessary?"
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" EnumConstructor.format_t constructor)
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" EnumName.format_t e_name))
constructors)
p.program_ctx.ctx_enums
let lint_program (p : program) : unit =
detect_empty_definitions p;
detect_unused_scope_vars p;
detect_unused_struct_fields p;
detect_unused_enum_constructors p

19
compiler/desugared/linting.mli Normal file
View File

@ -0,0 +1,19 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2023 Inria, contributor:
Denis Merigoux <denis.merigoux@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
val lint_program : Ast.program -> unit
(** Performs various lints on the program, displaying warnings to help the
developer improve the code. *)

5
compiler/driver.ml
View File

@ -39,9 +39,6 @@ let driver source_file (options : Cli.options) : int =
(match source_file with
| Pos.FileName f -> filename := f
| Contents c -> Cli.contents := c);
(match options.max_prec_digits with
| None -> ()
| Some i -> Cli.max_prec_digits := i);
let l =
match options.language with
| Some l -> l
@ -174,6 +171,8 @@ let driver source_file (options : Cli.options) : int =
let prgm = Desugared.From_surface.translate_program ctxt prgm in
Cli.debug_print "Disambiguating...";
let prgm = Desugared.Disambiguate.program prgm in
Cli.debug_print "Linting...";
Desugared.Linting.lint_program prgm;
Cli.debug_print "Collecting rules...";
let prgm = Scopelang.From_desugared.translate_program prgm in
match backend with

2
compiler/lcalc/ast.ml
View File

@ -17,8 +17,6 @@
open Catala_utils
include Shared_ast
type lit = lcalc glit
type 'm naked_expr = (lcalc, 'm mark) naked_gexpr
and 'm expr = (lcalc, 'm mark) gexpr

2
compiler/lcalc/ast.mli
View File

@ -21,8 +21,6 @@ open Shared_ast
(** {1 Abstract syntax tree} *)
type lit = lcalc glit
type 'm naked_expr = (lcalc, 'm mark) naked_gexpr
and 'm expr = (lcalc, 'm mark) gexpr

41
compiler/lcalc/compile_with_exceptions.ml
View File

@ -59,44 +59,11 @@ let rec translate_default
and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr boxed =
let m = Marked.get_mark e in
match Marked.unmark e with
| EVar v -> Expr.make_var (translate_var v) m
| EStruct { name; fields } ->
Expr.estruct name (StructField.Map.map (translate_expr ctx) fields) m
| EStructAccess { name; e; field } ->
Expr.estructaccess (translate_expr ctx e) field name m
| ETuple es -> Expr.etuple (List.map (translate_expr ctx) es) m
| ETupleAccess { e; index; size } ->
Expr.etupleaccess (translate_expr ctx e) index size m
| EInj { name; e; cons } -> Expr.einj (translate_expr ctx e) cons name m
| EMatch { name; e; cases } ->
Expr.ematch (translate_expr ctx e) name
(EnumConstructor.Map.map (translate_expr ctx) cases)
m
| EArray es -> Expr.earray (List.map (translate_expr ctx) es) m
| ELit
((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
l) ->
Expr.elit l m
| ELit LEmptyError -> Expr.eraise EmptyError m
| EOp { op; tys } -> Expr.eop (Operator.translate None op) tys m
| EIfThenElse { cond; etrue; efalse } ->
Expr.eifthenelse (translate_expr ctx cond) (translate_expr ctx etrue)
(translate_expr ctx efalse)
m
| EAssert e1 -> Expr.eassert (translate_expr ctx e1) m
| EEmptyError -> Expr.eraise EmptyError m
| EErrorOnEmpty arg ->
Expr.ecatch (translate_expr ctx arg) EmptyError
(Expr.eraise NoValueProvided m)
m
| EApp { f; args } ->
Expr.eapp (translate_expr ctx f)
(List.map (translate_expr ctx) args)
(Marked.get_mark e)
| EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in
let new_body = translate_expr ctx body in
let new_binder = Expr.bind (Array.map translate_var vars) new_body in
Expr.eabs new_binder tys (Marked.get_mark e)
| EDefault { excepts = [exn]; just; cons } when !Cli.optimize_flag ->
(* FIXME: bad place to rely on a global flag *)
Expr.ecatch (translate_expr ctx exn) EmptyError
@ -106,6 +73,12 @@ and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr boxed =
(Marked.get_mark e)
| EDefault { excepts; just; cons } ->
translate_default ctx excepts just cons (Marked.get_mark e)
| ( ELit _ | EApp _ | EOp _ | EArray _ | EVar _ | EAbs _ | EIfThenElse _
| ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _
| EStructAccess _ | EMatch _ ) as e ->
Expr.map_raw ~fop:Operator.translate
~floc:(function _ -> .)
~f:(translate_expr ctx) (Marked.mark m e)
let rec translate_scope_lets
(decl_ctx : decl_ctx)

7
compiler/lcalc/compile_without_exceptions.ml
View File

@ -182,7 +182,7 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
| EDefault _ ->
let v' = Var.make "default_term" in
Expr.make_var v' mark, Var.Map.singleton v' e
| ELit LEmptyError ->
| EEmptyError ->
let v' = Var.make "empty_litteral" in
Expr.make_var v' mark, Var.Map.singleton v' e
(* This one is a very special case. It transform an unpure expression
@ -302,8 +302,7 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
let es', hoists = es |> List.map (translate_and_hoist ctx) |> List.split in
Expr.earray es' mark, disjoint_union_maps (Expr.pos e) hoists
| EOp { op; tys } ->
Expr.eop (Operator.translate None op) tys mark, Var.Map.empty
| EOp { op; tys } -> Expr.eop (Operator.translate op) tys mark, Var.Map.empty
and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
'm A.expr boxed =
@ -334,7 +333,7 @@ and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
(Expr.make_var (Var.translate A.handle_default_opt) mark_hoist)
[Expr.earray excepts' mark_hoist; just'; cons']
pos
| ELit LEmptyError -> A.make_none mark_hoist
| EEmptyError -> A.make_none mark_hoist
| EAssert arg ->
let arg' = translate_expr ctx arg in

6
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 =
@ -34,9 +36,9 @@ and naked_expr =
| EStructFieldAccess : expr * StructField.t * StructName.t -> naked_expr
| EInj : expr * EnumConstructor.t * EnumName.t -> naked_expr
| EArray : expr list -> naked_expr
| ELit : L.lit -> naked_expr
| ELit : 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 op), Expr.pos expr)
| ELit l -> [], (A.ELit l, Expr.pos expr)
| _ ->
let tmp_var =

7
compiler/scalc/to_python.ml
View File

@ -22,7 +22,7 @@ module Runtime = Runtime_ocaml.Runtime
module D = Dcalc.Ast
module L = Lcalc.Ast
let format_lit (fmt : Format.formatter) (l : L.lit Marked.pos) : unit =
let format_lit (fmt : Format.formatter) (l : lit Marked.pos) : unit =
match Marked.unmark l with
| LBool true -> Format.pp_print_string fmt "True"
| LBool false -> Format.pp_print_string fmt "False"
@ -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 ->

17
compiler/scopelang/from_desugared.ml
View File

@ -91,8 +91,11 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
with Not_found ->
(* Should not happen after disambiguation *)
Errors.raise_spanned_error (Expr.mark_pos m)
"Field %s does not belong to structure %a" field StructName.format_t
name
"Field %a does not belong to structure %a"
(Cli.format_with_style [ANSITerminal.yellow])
("\"" ^ field ^ "\"")
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" StructName.format_t name)
in
Expr.estructaccess e' field name m
| ETuple es -> Expr.etuple (List.map (translate_expr ctx) es) m
@ -120,8 +123,8 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
args ScopeVar.Map.empty)
m
| ELit
(( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _
| LDuration _ ) as l) ->
((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
l) ->
Expr.elit l m
| EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in
@ -159,6 +162,7 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
(translate_expr ctx efalse)
m
| EArray args -> Expr.earray (List.map (translate_expr ctx) args) m
| EEmptyError -> Expr.eemptyerror m
| EErrorOnEmpty e1 -> Expr.eerroronempty (translate_expr ctx e1) m
(** {1 Rule tree construction} *)
@ -292,8 +296,7 @@ let rec rule_tree_to_expr
(translate_and_unbox_list base_just_list)
(translate_and_unbox_list base_cons_list))
(Expr.elit (LBool false) emark)
(Expr.elit LEmptyError emark)
emark
(Expr.eemptyerror emark) emark
in
let exceptions =
List.map
@ -390,7 +393,7 @@ let translate_def
caller. *)
then
let m = Untyped { pos = Desugared.Ast.ScopeDef.get_position def_info } in
let empty_error = Expr.elit LEmptyError m in
let empty_error = Expr.eemptyerror m in
match params with
| Some (ps, _) ->
let labels, tys = List.split ps in

357
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,32 @@ 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 =
| 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
type lit =
| LBool of bool
| LInt of Runtime.integer
| LRat of Runtime.decimal
| LMoney of Runtime.money
| LUnit
| LDate of date
| LDuration of duration
(** 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
and ('a, 't) naked_gexpr = ('a, 'a, 't) base_gexpr
(** 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.
@ -268,97 +303,101 @@ type ('a, 't) gexpr = (('a, 't) naked_gexpr, 't) Marked.t
- 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. *)
than completely defining your recursion manually.
and ('a, 't) naked_gexpr =
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 *)
and ('a, 'b, 't) base_gexpr =
(* Constructors common to all ASTs *)
| ELit : 'a glit -> ('a any, 't) naked_gexpr
| ELit : lit -> ('a, [< all ], 't) base_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
-> ('a, [< all ], 't) base_gexpr
| EOp : { op : 'a operator; tys : typ list } -> ('a, [< all ], 't) base_gexpr
| EArray : ('a, 't) gexpr list -> ('a, [< all ], 't) base_gexpr
| EVar : ('a, 't) naked_gexpr Bindlib.var -> ('a, _, 't) base_gexpr
| EAbs : {
binder : (('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder;
binder : (('a, 'a, 't) base_gexpr, ('a, 't) gexpr) Bindlib.mbinder;
tys : typ list;
}
-> ('a any, 't) naked_gexpr
-> ('a, [< all ], 't) base_gexpr
| EIfThenElse : {
cond : ('a, 't) gexpr;
etrue : ('a, 't) gexpr;
efalse : ('a, 't) gexpr;
}
-> ('a any, 't) naked_gexpr
-> ('a, [< all ], 't) base_gexpr
| EStruct : {
name : StructName.t;
fields : ('a, 't) gexpr StructField.Map.t;
}
-> ('a any, 't) naked_gexpr
-> ('a, [< all ], 't) base_gexpr
| EInj : {
name : EnumName.t;
e : ('a, 't) gexpr;
cons : EnumConstructor.t;
}
-> ('a any, 't) naked_gexpr
-> ('a, [< all ], 't) base_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
-> ('a, [< all ], 't) base_gexpr
| ETuple : ('a, 't) gexpr list -> ('a, [< all ], 't) base_gexpr
| ETupleAccess : {
e : ('a, 't) gexpr;
index : int;
size : int;
}
-> ('a any, 't) naked_gexpr
-> ('a, [< all ], 't) base_gexpr
(* Early stages *)
| ELocation :
'a glocation
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
| ELocation : 'a glocation -> ('a, [< all > `ExplicitScopes ], 't) base_gexpr
| EScopeCall : {
scope : ScopeName.t;
args : ('a, 't) gexpr ScopeVar.Map.t;
}
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
-> ('a, [< all > `ExplicitScopes ], 't) base_gexpr
| EDStructAccess : {
name_opt : StructName.t option;
e : ('a, 't) gexpr;
field : IdentName.t;
}
-> ((desugared as 'a), 't) naked_gexpr
-> ('a, [< all > `SyntacticNames ], 't) base_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
-> ('a, [< all > `ResolvedNames ], 't) base_gexpr
(** Resolved struct/enums, after [desugared] *)
(* Lambda-like *)
| EAssert : ('a, 't) gexpr -> (([< dcalc | lcalc ] as 'a), 't) naked_gexpr
| EAssert : ('a, 't) gexpr -> ('a, [< all > `Assertions ], 't) base_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
-> ('a, [< all > `DefaultTerms ], 't) base_gexpr
| EEmptyError : ('a, [< all > `DefaultTerms ], 't) base_gexpr
| EErrorOnEmpty :
('a, 't) gexpr
-> (([< desugared | scopelang | dcalc ] as 'a), 't) naked_gexpr
-> ('a, [< all > `DefaultTerms ], 't) base_gexpr
(* Lambda calculus with exceptions *)
| ERaise : except -> ((lcalc as 'a), 't) naked_gexpr
| ERaise : except -> ('a, [< all > `Exceptions ], 't) base_gexpr
| ECatch : {
body : ('a, 't) gexpr;
exn : except;
handler : ('a, 't) gexpr;
}
-> ((lcalc as 'a), 't) naked_gexpr
-> ('a, [< all > `Exceptions ], 't) base_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 *)
@ -389,7 +428,7 @@ type typed = { pos : Pos.t; ty : typ }
type _ mark = Untyped : untyped -> untyped mark | Typed : typed -> typed mark
(** Useful for errors and printing, for example *)
type any_expr = AnyExpr : (_, _ mark) gexpr -> any_expr
type any_expr = AnyExpr : ('a, _ mark) gexpr -> any_expr
(** {2 Higher-level program structure} *)
@ -420,7 +459,7 @@ type 'e scope_let = {
(* todo ? Factorise the code_item _list type below and use it here *)
scope_let_pos : Pos.t;
}
constraint 'e = (_ any, _ mark) gexpr
constraint 'e = ('a any, _ mark) gexpr
(** This type is parametrized by the expression type so it can be reused in
later intermediate representations. *)
@ -430,14 +469,14 @@ type 'e scope_let = {
and 'e scope_body_expr =
| Result of 'e
| ScopeLet of 'e scope_let
constraint 'e = (_ any, _ mark) gexpr
constraint 'e = ('a any, _ mark) gexpr
type 'e scope_body = {
scope_body_input_struct : StructName.t;
scope_body_output_struct : StructName.t;
scope_body_expr : ('e, 'e scope_body_expr) binder;
}
constraint 'e = (_ any, _ mark) gexpr
constraint 'e = ('a any, _ mark) gexpr
(** 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

58
compiler/shared_ast/expr.ml
View File

@ -101,6 +101,7 @@ let eifthenelse cond etrue efalse =
@@ fun cond etrue efalse -> EIfThenElse { cond; etrue; efalse }
let eerroronempty e1 = Box.app1 e1 @@ fun e1 -> EErrorOnEmpty e1
let eemptyerror mark = Marked.mark mark (Bindlib.box EEmptyError)
let eraise e1 = Box.app0 @@ ERaise e1
let ecatch body exn handler =
@ -204,15 +205,17 @@ let maybe_ty (type m) ?(typ = TAny) (m : m mark) : typ =
(* - Traversal functions - *)
(* shallow map *)
let map
(type a)
~(f : (a, 'm1) gexpr -> (a, 'm2) boxed_gexpr)
(e : ((a, 'm1) naked_gexpr, 'm2) Marked.t) : (a, 'm2) boxed_gexpr =
let map_raw
(type a b)
~(f : (a, 'm1) gexpr -> (b, 'm2) boxed_gexpr)
~(fop : a Op.t -> b Op.t)
~(floc : a glocation -> b glocation)
(e : ((a, b, 'm1) base_gexpr, 'm2) Marked.t) : (b, 'm2) boxed_gexpr =
let m = Marked.get_mark e in
match Marked.unmark e with
| ELit l -> elit l m
| EApp { f = e1; args } -> eapp (f e1) (List.map f args) m
| EOp { op; tys } -> eop op tys m
| EOp { op; tys } -> eop (fop op) tys m
| EArray args -> earray (List.map f args) m
| EVar v -> evar (Var.translate v) m
| EAbs { binder; tys } ->
@ -228,10 +231,11 @@ let map
| EAssert e1 -> eassert (f e1) m
| EDefault { excepts; just; cons } ->
edefault (List.map f excepts) (f just) (f cons) m
| EEmptyError -> eemptyerror m
| EErrorOnEmpty e1 -> eerroronempty (f e1) m
| ECatch { body; exn; handler } -> ecatch (f body) exn (f handler) m
| ERaise exn -> eraise exn m
| ELocation loc -> elocation loc m
| ELocation loc -> elocation (floc loc) m
| EStruct { name; fields } ->
let fields = StructField.Map.map f fields in
estruct name fields m
@ -245,6 +249,7 @@ let map
let fields = ScopeVar.Map.map f args in
escopecall scope fields m
let map = map_raw ~fop:(fun op -> op) ~floc:(fun loc -> loc)
let rec map_top_down ~f e = map ~f:(map_top_down ~f) (f e)
let map_marks ~f e =
@ -259,10 +264,12 @@ let shallow_fold
(acc : 'acc) : 'acc =
let lfold x acc = List.fold_left (fun acc x -> f x acc) acc x in
match Marked.unmark e with
| ELit _ | EOp _ | EVar _ | ERaise _ | ELocation _ -> acc
| ELit _ | EOp _ | EVar _ | ERaise _ | ELocation _ | EEmptyError -> acc
| EApp { f = e; args } -> acc |> f e |> lfold args
| EArray args -> acc |> lfold args
| EAbs _ -> acc
| EAbs { binder; tys = _ } ->
let _, body = Bindlib.unmbind binder in
acc |> f body
| EIfThenElse { cond; etrue; efalse } -> acc |> f cond |> f etrue |> f efalse
| ETuple args -> acc |> lfold args
| ETupleAccess { e; _ } -> acc |> f e
@ -334,6 +341,7 @@ let map_gather
let acc2, just = f just in
let acc3, cons = f cons in
join (join acc1 acc2) acc3, edefault excepts just cons m
| EEmptyError -> acc, eemptyerror m
| EErrorOnEmpty e ->
let acc, e = f e in
acc, eerroronempty e m
@ -383,7 +391,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
@ -396,27 +404,23 @@ let is_value (type a) (e : (a, _) gexpr) =
| ELit _ | EAbs _ | EOp _ | ERaise _ -> true
| _ -> false
let equal_lit (type a) (l1 : a glit) (l2 : a glit) =
let equal_lit (l1 : lit) (l2 : lit) =
let open Runtime.Oper in
match l1, l2 with
| LBool b1, LBool b2 -> not (o_xor b1 b2)
| LEmptyError, LEmptyError -> true
| LInt n1, LInt n2 -> o_eq_int_int n1 n2
| LRat r1, LRat r2 -> o_eq_rat_rat r1 r2
| LMoney m1, LMoney m2 -> o_eq_mon_mon m1 m2
| LUnit, LUnit -> true
| LDate d1, LDate d2 -> o_eq_dat_dat d1 d2
| LDuration d1, LDuration d2 -> o_eq_dur_dur d1 d2
| ( ( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _
| LDuration _ ),
_ ) ->
| (LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _), _ ->
false
let compare_lit (type a) (l1 : a glit) (l2 : a glit) =
let compare_lit (l1 : lit) (l2 : lit) =
let open Runtime.Oper in
match l1, l2 with
| LBool b1, LBool b2 -> Bool.compare b1 b2
| LEmptyError, LEmptyError -> 0
| LInt n1, LInt n2 ->
if o_lt_int_int n1 n2 then -1 else if o_eq_int_int n1 n2 then 0 else 1
| LRat r1, LRat r2 ->
@ -436,8 +440,6 @@ let compare_lit (type a) (l1 : a glit) (l2 : a glit) =
| n -> n)
| LBool _, _ -> -1
| _, LBool _ -> 1
| LEmptyError, _ -> -1
| _, LEmptyError -> 1
| LInt _, _ -> -1
| _, LInt _ -> 1
| LRat _, _ -> -1
@ -516,6 +518,7 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
| ( EIfThenElse { cond = if1; etrue = then1; efalse = else1 },
EIfThenElse { cond = if2; etrue = then2; efalse = else2 } ) ->
equal if1 if2 && equal then1 then2 && equal else1 else2
| EEmptyError, EEmptyError -> true
| EErrorOnEmpty e1, EErrorOnEmpty e2 -> equal e1 e2
| ERaise ex1, ERaise ex2 -> equal_except ex1 ex2
| ( ECatch { body = etry1; exn = ex1; handler = ewith1 },
@ -544,9 +547,9 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
EScopeCall { scope = s2; args = fields2 } ) ->
ScopeName.equal s1 s2 && ScopeVar.Map.equal equal fields1 fields2
| ( ( EVar _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _ | EAbs _ | EApp _
| EAssert _ | EOp _ | EDefault _ | EIfThenElse _ | EErrorOnEmpty _
| ERaise _ | ECatch _ | ELocation _ | EStruct _ | EDStructAccess _
| EStructAccess _ | EInj _ | EMatch _ | EScopeCall _ ),
| EAssert _ | EOp _ | EDefault _ | EIfThenElse _ | EEmptyError
| EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EStruct _
| EDStructAccess _ | EStructAccess _ | EInj _ | EMatch _ | EScopeCall _ ),
_ ) ->
false
@ -623,6 +626,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
compare just1 just2 @@< fun () ->
compare cons1 cons2 @@< fun () ->
List.compare compare exs1 exs2
| EEmptyError, EEmptyError -> 0
| EErrorOnEmpty e1, EErrorOnEmpty e2 ->
compare e1 e2
| ERaise ex1, ERaise ex2 ->
@ -650,11 +654,12 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
| EInj _, _ -> -1 | _, EInj _ -> 1
| EAssert _, _ -> -1 | _, EAssert _ -> 1
| EDefault _, _ -> -1 | _, EDefault _ -> 1
| EErrorOnEmpty _, _ -> . | _, EErrorOnEmpty _ -> .
| EEmptyError , _ -> -1 | _, EEmptyError -> 1
| 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
@ -674,7 +679,7 @@ let format ?debug decl_ctx ppf e = Print.expr ?debug decl_ctx ppf e
let rec size : type a. (a, 't) gexpr -> int =
fun e ->
match Marked.unmark e with
| EVar _ | ELit _ | EOp _ -> 1
| EVar _ | ELit _ | EOp _ | EEmptyError -> 1
| ETuple args -> List.fold_left (fun acc arg -> acc + size arg) 1 args
| EArray args -> List.fold_left (fun acc arg -> acc + size arg) 1 args
| ETupleAccess { e; _ } -> size e + 1
@ -738,10 +743,7 @@ let make_app e args pos =
let empty_thunked_term mark =
let silent = Var.make "_" in
let pos = mark_pos mark in
make_abs [| silent |]
(Bindlib.box (ELit LEmptyError), mark)
[TLit TUnit, pos]
pos
make_abs [| silent |] (Bindlib.box EEmptyError, mark) [TLit TUnit, pos] pos
let make_let_in x tau e1 e2 mpos =
make_app (make_abs [| x |] e2 [tau] mpos) [e1] (pos e2)

123
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,103 @@ 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 : lit -> '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 eemptyerror : 't -> (([< all > `DefaultTerms ] as 'a), '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 *)
@ -197,6 +199,30 @@ val map :
f e
]} *)
val map_raw :
f:(('a, 'm1) gexpr -> ('b, 'm2) boxed_gexpr) ->
fop:('a Op.t -> 'b Op.t) ->
floc:('a glocation -> 'b glocation) ->
(('a, 'b, 'm1) base_gexpr, 'm2) Marked.t ->
('b, 'm2) boxed_gexpr
(** Lower-level version of shallow [map] that can be used for transforming the
type of the AST. See [Lcalc.Compile_without_exceptions] for an example. The
structure is like this:
{[
let rec translate = function
| SpecificCase e -> TargetCase (translate e)
| (All | Other | Common | Cases) as e -> map_raw ~f:translate e
]}
This function makes it very concise to transform only certain nodes of the
AST.
The [e] parameter passed to [map_raw] here needs to have only the common
cases in its shallow type, but can still contain any node from the starting
AST deeper inside: this is where the second type parameter to [base_gexpr]
becomes useful. *)
val map_top_down :
f:(('a, 't1) gexpr -> (('a, 't1) naked_gexpr, 't2) Marked.t) ->
('a, 't1) gexpr ->
@ -210,9 +236,9 @@ val map_marks : f:('t1 -> 't2) -> ('a, 't1) gexpr -> ('a, 't2) boxed_gexpr
val shallow_fold :
(('a, 't) gexpr -> 'acc -> 'acc) -> ('a, 't) gexpr -> 'acc -> 'acc
(** Applies a function on all sub-terms of the given expression. Does not
recurse, and doesn't open binders. Useful as helper for recursive calls
within traversal functions. This can be used to compute free variables with
e.g.:
recurse. It opens binders unless you avoid sending binders to the function
like the example below. Useful as helper for recursive calls within
traversal functions. This can be used to compute free variables with e.g.:
{[
let rec free_vars = function
@ -257,16 +283,16 @@ val make_abs :
('a, 'm mark) boxed_gexpr ->
typ list ->
Pos.t ->
('a, 'm mark) boxed_gexpr
('a any, 'm mark) boxed_gexpr
val make_app :
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr list ->
Pos.t ->
('a, 'm mark) boxed_gexpr
('a any, '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 ->
@ -274,7 +300,7 @@ val make_let_in :
('a, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr ->
Pos.t ->
('a, 'm mark) boxed_gexpr
('a any, 'm mark) boxed_gexpr
val make_multiple_let_in :
('a, 'm mark) gexpr Var.vars ->
@ -282,14 +308,14 @@ val make_multiple_let_in :
('a, 'm mark) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr ->
Pos.t ->
('a, 'm mark) boxed_gexpr
('a any, '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 +336,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. *)
@ -323,8 +350,8 @@ val format :
(** {2 Analysis and tests} *)
val equal_lit : 'a glit -> 'a glit -> bool
val compare_lit : 'a glit -> 'a glit -> int
val equal_lit : lit -> lit -> bool
val compare_lit : lit -> lit -> int
val equal_location : 'a glocation Marked.pos -> 'a glocation Marked.pos -> bool
val compare_location : 'a glocation Marked.pos -> 'a glocation Marked.pos -> int

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,28 @@ 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
| 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
let translate
(t : [< scopelang | dcalc | lcalc > `Monomorphic `Polymorphic `Resolved ] t)
=
match t with
| ( 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_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 ) 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 +381,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 +441,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 +501,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 +528,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)

34
compiler/shared_ast/operator.mli
View File

@ -33,39 +33,35 @@ 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 +74,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. *)

12
compiler/shared_ast/print.ml
View File

@ -126,11 +126,10 @@ let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit =
Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "collection" typ t1
| TAny -> base_type fmt "any"
let lit (type a) (fmt : Format.formatter) (l : a glit) : unit =
let lit (fmt : Format.formatter) (l : lit) : unit =
match l with
| LBool b -> lit_style fmt (string_of_bool b)
| LInt i -> lit_style fmt (Runtime.integer_to_string i)
| LEmptyError -> lit_style fmt "∅ "
| LUnit -> lit_style fmt "()"
| LRat i ->
lit_style fmt
@ -154,7 +153,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 +242,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
@ -360,6 +363,7 @@ let rec expr_aux :
expr)
excepts punctuation "|" expr just punctuation "⊢" expr cons punctuation
"⟩"
| EEmptyError -> lit_style fmt "∅ "
| EErrorOnEmpty e' ->
Format.fprintf fmt "%a@ %a" op_style "error_empty" with_parens e'
| EAssert e' ->

4
compiler/shared_ast/print.mli
View File

@ -34,8 +34,8 @@ val enum_constructor : Format.formatter -> EnumConstructor.t -> unit
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 lit : Format.formatter -> lit -> 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

6
compiler/shared_ast/program.ml
View File

@ -22,6 +22,12 @@ let map_exprs ~f ~varf { code_items; decl_ctx } =
(fun code_items -> { code_items; decl_ctx })
(Scope.map_exprs ~f ~varf code_items)
let fold_left_exprs ~f ~init { code_items; decl_ctx = _ } =
Scope.fold_left ~f:(fun acc e _ -> f acc e) ~init code_items
let fold_right_exprs ~f ~init { code_items; decl_ctx = _ } =
Scope.fold_right ~f:(fun e _ acc -> f e acc) ~init code_items
let get_scope_body { code_items; _ } scope =
match
Scope.fold_left ~init:None

15
compiler/shared_ast/program.mli
View File

@ -25,15 +25,18 @@ val map_exprs :
'expr1 program ->
'expr2 program Bindlib.box
val fold_left_exprs :
f:('a -> 'expr code_item -> 'a) -> init:'a -> 'expr program -> 'a
val fold_right_exprs :
f:('expr code_item -> 'a -> 'a) -> init:'a -> 'expr program -> 'a
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. *)

29
compiler/shared_ast/typing.ml
View File

@ -221,7 +221,7 @@ let handle_type_error ctx e t1 t2 =
(Cli.format_with_style [ANSITerminal.blue; ANSITerminal.Bold])
"-->" t2_s ()
let lit_type (type a) (lit : a A.glit) : naked_typ =
let lit_type (lit : A.lit) : naked_typ =
match lit with
| LBool _ -> TLit TBool
| LInt _ -> TLit TInt
@ -230,15 +230,14 @@ let lit_type (type a) (lit : a A.glit) : naked_typ =
| LDate _ -> TLit TDate
| LDuration _ -> TLit TDuration
| LUnit -> TLit TUnit
| LEmptyError -> TAny (Any.fresh ())
(** [op_type] and [resolve_overload] are a bit similar, and work on disjoint
sets of operators. However, their assumptions are different so we keep the
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 +266,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
@ -475,18 +474,27 @@ and typecheck_expr_top_down :
try A.IdentName.Map.find field ctx.ctx_struct_fields
with Not_found ->
Errors.raise_spanned_error context_mark.pos
"Field %s does not belong to structure %a (no structure defines \
"Field %a does not belong to structure %a (no structure defines \
it)"
field A.StructName.format_t name
(Cli.format_with_style [ANSITerminal.yellow])
("\"" ^ field ^ "\"")
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" A.StructName.format_t name)
in
try A.StructName.Map.find name candidate_structs
with Not_found ->
Errors.raise_spanned_error context_mark.pos
"Field %s does not belong to structure %a, but to %a" field
A.StructName.format_t name
"Field %a does not belong to structure %a, but to %a"
(Cli.format_with_style [ANSITerminal.yellow])
("\"" ^ field ^ "\"")
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" A.StructName.format_t name)
(Format.pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf "@ or@ ")
A.StructName.format_t)
(fun fmt s_name ->
Format.fprintf fmt "%a"
(Cli.format_with_style [ANSITerminal.yellow])
(Format.asprintf "\"%a\"" A.StructName.format_t s_name)))
(List.map fst (A.StructName.Map.bindings candidate_structs))
in
A.StructField.Map.find field str
@ -742,6 +750,7 @@ and typecheck_expr_top_down :
e1
in
Expr.eassert e1' mark
| A.EEmptyError -> Expr.eemptyerror (ty_mark (TAny (Any.fresh ())))
| A.EErrorOnEmpty e1 ->
let e1' = typecheck_expr_top_down ~leave_unresolved ctx env tau e1 in
Expr.eerroronempty e1' context_mark

6
compiler/shared_ast/var.ml
View File

@ -21,10 +21,8 @@ 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 vars = ('a, 't) naked_gexpr Bindlib.mvar
constraint 'e = ('a any, 't) gexpr
type 'e t = ('a, 't) naked_gexpr Bindlib.var constraint 'e = ('a, 't) gexpr
type 'e vars = ('a, 't) naked_gexpr Bindlib.mvar constraint 'e = ('a, 't) gexpr
let make (name : string) : 'e t = Bindlib.new_var (fun x -> EVar x) name
let compare = Bindlib.compare_vars

6
compiler/shared_ast/var.mli
View File

@ -21,10 +21,8 @@ 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 vars = ('a, 't) naked_gexpr Bindlib.mvar
constraint 'e = ('a any, 't) gexpr
type 'e t = ('a, 't) naked_gexpr Bindlib.var constraint 'e = ('a, 't) gexpr
type 'e vars = ('a, 't) naked_gexpr Bindlib.mvar constraint 'e = ('a, 't) gexpr
val make : string -> 'e t
val compare : 'e t -> 'e t -> int

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)

4
compiler/verification/conditions.ml
View File

@ -198,7 +198,7 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) :
(Marked.get_mark e);
])
(Marked.get_mark e)
| ELit LEmptyError -> Marked.same_mark_as (ELit (LBool false)) e
| EEmptyError -> Marked.same_mark_as (ELit (LBool false)) e
| EVar _
(* Per default calculus semantics, you cannot call a function with an argument
that evaluates to the empty error. Thus, all variable evaluate to
@ -229,7 +229,7 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) :
can be ignored *)
let _vars, body = Bindlib.unmbind binder in
match Marked.unmark body with
| ELit LEmptyError ->
| EEmptyError ->
Marked.same_mark_as (ELit (LBool true)) field
| _ ->
(* same as basic [EAbs case]*)

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

@ -374,7 +374,6 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr =
match l with
| LBool b ->
if b then Boolean.mk_true ctx.ctx_z3 else Boolean.mk_false ctx.ctx_z3
| LEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
| LInt n ->
Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (Runtime.integer_to_int n)
| LRat r ->
@ -430,8 +429,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
@ -786,6 +784,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
(Boolean.mk_not ctx.ctx_z3 z3_if)
z3_else;
] )
| EEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
| EErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"
(** [create_z3unit] creates a Z3 sort and expression corresponding to the unit

4
examples/aides_logement/tests/tests_calcul_al_locatif.catala_fr
View File

@ -90,13 +90,13 @@ champ d'application Exemple2 :
```
```catala-test-inline
$ catala Interpret -s Exemple1
$ catala Interpret -s Exemple1 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 345.73 €
```
```catala-test-inline
$ catala Interpret -s Exemple2
$ catala Interpret -s Exemple2 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 352.77 €
```

2
examples/aides_logement/tests/tests_calcul_al_logement_foyer.catala_fr
View File

@ -31,7 +31,7 @@ champ d'application CasTest1:
```
```catala-test-inline
$ catala Interpret -s CasTest1
$ catala Interpret -s CasTest1 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 76.38 €
```

8
examples/aides_logement/tests/tests_calcul_apl_accession_propriete.catala_fr
View File

@ -144,26 +144,26 @@ champ d'application Exemple4:
```
```catala-test-inline
$ catala Interpret -s Exemple1
$ catala Interpret -s Exemple1 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 181.91 €
```
```catala-test-inline
$ catala Interpret -s Exemple2
$ catala Interpret -s Exemple2 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 67.34 €
```
```catala-test-inline
$ catala Interpret -s Exemple3
$ catala Interpret -s Exemple3 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 181.91 €
```
```catala-test-inline
$ catala Interpret -s Exemple4
$ catala Interpret -s Exemple4 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 118.59 €
```

18
examples/aides_logement/tests/tests_calcul_apl_locatif.catala_fr
View File

@ -279,55 +279,55 @@ champ d'application Exemple9:
```
```catala-test-inline
$ catala Interpret -s Exemple1
$ catala Interpret -s Exemple1 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 0.00 €
```
```catala-test-inline
$ catala Interpret -s Exemple2
$ catala Interpret -s Exemple2 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 352.77 €
```
```catala-test-inline
$ catala Interpret -s Exemple3
$ catala Interpret -s Exemple3 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 321.61 €
```
```catala-test-inline
$ catala Interpret -s Exemple4
$ catala Interpret -s Exemple4 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 0.00 €
```
```catala-test-inline
$ catala Interpret -s Exemple5
$ catala Interpret -s Exemple5 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 311.56 €
```
```catala-test-inline
$ catala Interpret -s Exemple6
$ catala Interpret -s Exemple6 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 0.00 €
```
```catala-test-inline
$ catala Interpret -s Exemple7
$ catala Interpret -s Exemple7 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 153.77 €
```
```catala-test-inline
$ catala Interpret -s Exemple8
$ catala Interpret -s Exemple8 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 11.06 €
```
```catala-test-inline
$ catala Interpret -s Exemple9
$ catala Interpret -s Exemple9 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 210.06 €
```

10
examples/aides_logement/tests/tests_calcul_apl_logement_foyer.catala_fr
View File

@ -132,31 +132,31 @@ champ d'application CasTest5:
```
```catala-test-inline
$ catala Interpret -s CasTest1
$ catala Interpret -s CasTest1 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 12.06 €
```
```catala-test-inline
$ catala Interpret -s CasTest2
$ catala Interpret -s CasTest2 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 23.12 €
```
```catala-test-inline
$ catala Interpret -s CasTest3
$ catala Interpret -s CasTest3 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 154.78 €
```
```catala-test-inline
$ catala Interpret -s CasTest4
$ catala Interpret -s CasTest4 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 154.78 €
```
```catala-test-inline
$ catala Interpret -s CasTest5
$ catala Interpret -s CasTest5 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] montant = 129.65 €
```

230
examples/aides_logement/tests/tests_eligibilite_apl.catala_fr
View File

@ -260,12 +260,240 @@ champ d'application Exemple2 :
```
```catala-test-inline
$ catala Interpret -s Exemple1
$ catala Interpret -s Exemple1 --disable_warnings
[RESULT] Computation successful! Results:
[RESULT] éligible = true
```
```catala-test-inline
$ catala Typecheck
[WARNING] In scope "RessourcesAidesPersonnelleLogement", the variable "ressources_ménage_arrondies.seuil" is declared but never defined; did you forget something?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:496.9-14:
└───┐
496 │ état seuil
│ ‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Déclarations des champs d'application
└─ Prise en compte des ressources pour les aides personnelles au logement
[WARNING] In scope "RessourcesAidesPersonnelleLogement", the variable "ressources_forfaitaires_r822_20" is declared but never defined; did you forget something?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:504.10-41:
└───┐
504 │ interne ressources_forfaitaires_r822_20 contenu argent
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Déclarations des champs d'application
└─ Prise en compte des ressources pour les aides personnelles au logement
[WARNING] In scope "ÉligibilitéAidesPersonnelleLogement", the variable "condition_prêt" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:292.10-24:
└───┐
292 │ interne condition_prêt condition dépend de prêt contenu Prêt
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Déclarations des champs d'application
└─ Éligibilité aux aides personnelles au logement
[WARNING] In scope "ÉligibilitéAidesPersonnelleLogement", the variable "condition_peuplement_logement_l822_10" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:301.10-47:
└───┐
301 │ interne condition_peuplement_logement_l822_10 condition
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Déclarations des champs d'application
└─ Éligibilité aux aides personnelles au logement
[WARNING] In scope "ÉligibilitéAidesPersonnelleLogement", the variable "patrimoine_pris_en_compte" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:314.10-35:
└───┐
314 │ interne patrimoine_pris_en_compte contenu argent
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Déclarations des champs d'application
└─ Éligibilité aux aides personnelles au logement
[WARNING] In scope "ÉligibilitéPrimeDeDéménagement", the variable "éligibilité_logement" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:457.10-30:
└───┐
457 │ interne éligibilité_logement condition
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Déclarations des champs d'application
└─ Éligibilité à la prime de déménagement
[WARNING] In scope "RessourcesAidesPersonnelleLogement", the variable "ressources_ménage_arrondies.seuil" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:496.9-14:
└───┐
496 │ état seuil
│ ‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Déclarations des champs d'application
└─ Prise en compte des ressources pour les aides personnelles au logement
[WARNING] In scope "RessourcesAidesPersonnelleLogement", the variable "ressources_ménage_arrondies.base" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:495.9-13:
└───┐
495 │ état base
│ ‾‾‾‾
└┬ Prologue : aides au logement
└┬ Déclarations des champs d'application
└─ Prise en compte des ressources pour les aides personnelles au logement
[WARNING] In scope "RessourcesAidesPersonnelleLogement", the variable "abattement_r_822_8" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:499.10-28:
└───┐
499 │ interne abattement_r_822_8 contenu argent
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Déclarations des champs d'application
└─ Prise en compte des ressources pour les aides personnelles au logement
[WARNING] In scope "RessourcesAidesPersonnelleLogement", the variable "abattement_r_822_7" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:501.10-28:
└───┐
501 │ interne abattement_r_822_7 contenu argent
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Déclarations des champs d'application
└─ Prise en compte des ressources pour les aides personnelles au logement
[WARNING] In scope "RessourcesAidesPersonnelleLogement", the variable "abattement_r_822_10" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:503.10-29:
└───┐
503 │ interne abattement_r_822_10 contenu argent
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Déclarations des champs d'application
└─ Prise en compte des ressources pour les aides personnelles au logement
[WARNING] In scope "CalculAllocationLogement", the variable "catégorie_calcul_apl" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:1000.10-30:
└────┐
1000 │ interne catégorie_calcul_apl contenu CatégorieCalculAPL
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Calcul du montant de l'allocation logement
└┬ Secteur logement-foyer
└─ Tous secteurs
[WARNING] In scope "ÉligibilitéPrestationsFamiliales", the variable "prestation_courante" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../../prestations_familiales/prologue.catala_fr:48.9-28:
└──┐
48 │ entrée prestation_courante contenu ÉlémentPrestationsFamiliales
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─ Prologue : prestations familiales
[WARNING] The constructor "AllocationJeuneEnfant" of enumeration "PrestationReçue" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:132.5-26:
└───┐
132 │ -- AllocationJeuneEnfant
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Types de données manipulées par le programme
└┬ Calcul et éligibilité des aides personnelles au logement
└─ Calcul et éligibilité pour tous les secteurs
[WARNING] The constructor "Descendant" of enumeration "Parenté" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:185.5-15:
└───┐
185 │ -- Descendant
│ ‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Types de données manipulées par le programme
└┬ Calcul et éligibilité des aides personnelles au logement
└─ Calcul et éligibilité pour tous les secteurs
[WARNING] The constructor "CollatéralDeuxièmeTroisièmeDegré" of enumeration "Parenté" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../prologue.catala_fr:186.5-37:
└───┐
186 │ -- CollatéralDeuxièmeTroisièmeDegré
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue : aides au logement
└┬ Types de données manipulées par le programme
└┬ Calcul et éligibilité des aides personnelles au logement
└─ Calcul et éligibilité pour tous les secteurs
[WARNING] The enumeration "PriseEnCharge" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../code_construction_legislatif.catala_fr:444.24-37:
└───┐
444 │ déclaration énumération PriseEnCharge:
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Code de la construction et de l'habitation
└┬ Partie législative
└┬ Livre VIII : Aides personnelles au logement
└┬ Titre II : Dispositions communes aux aides personnelles au logement
└┬ Chapitre III : Modalités de liquidation et de versement
└─ Article L823-2
[WARNING] The constructor "GardeAlternéeAllocataireUnique" of enumeration "PriseEnChargeEnfant" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../../prestations_familiales/prologue.catala_fr:10.5-35:
└──┐
10 │ -- GardeAlternéeAllocataireUnique
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─ Prologue : prestations familiales
[WARNING] The constructor "ServicesSociauxAllocationVerséeÀLaFamille" of enumeration "PriseEnChargeEnfant" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../../prestations_familiales/prologue.catala_fr:12.5-46:
└──┐
12 │ -- ServicesSociauxAllocationVerséeÀLaFamille
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─ Prologue : prestations familiales
[WARNING] The constructor "ServicesSociauxAllocationVerséeAuxServicesSociaux" of enumeration "PriseEnChargeEnfant" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../../prestations_familiales/prologue.catala_fr:13.5-54:
└──┐
13 │ -- ServicesSociauxAllocationVerséeAuxServicesSociaux
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─ Prologue : prestations familiales
[WARNING] The constructor "PrestationAccueilJeuneEnfant" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../../prestations_familiales/prologue.catala_fr:30.5-33:
└──┐
30 │ -- PrestationAccueilJeuneEnfant
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─ Prologue : prestations familiales
[WARNING] The constructor "ComplémentFamilial" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../../prestations_familiales/prologue.catala_fr:32.5-23:
└──┐
32 │ -- ComplémentFamilial
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─ Prologue : prestations familiales
[WARNING] The constructor "AllocationLogement" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../../prestations_familiales/prologue.catala_fr:33.5-23:
└──┐
33 │ -- AllocationLogement
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─ Prologue : prestations familiales
[WARNING] The constructor "AllocationÉducationEnfantHandicapé" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../../prestations_familiales/prologue.catala_fr:34.5-39:
└──┐
34 │ -- AllocationÉducationEnfantHandicapé
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─ Prologue : prestations familiales
[WARNING] The constructor "AllocationSoutienFamilial" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../../prestations_familiales/prologue.catala_fr:35.5-30:
└──┐
35 │ -- AllocationSoutienFamilial
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─ Prologue : prestations familiales
[WARNING] The constructor "AllocationRentréeScolaire" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../../prestations_familiales/prologue.catala_fr:36.5-30:
└──┐
36 │ -- AllocationRentréeScolaire
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─ Prologue : prestations familiales
[WARNING] The constructor "AllocationJournalièrePresenceParentale" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/aides_logement/tests/../../prestations_familiales/prologue.catala_fr:37.5-43:
└──┐
37 │ -- AllocationJournalièrePresenceParentale
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└─ Prologue : prestations familiales
[RESULT] Typechecking successful!
```

116
examples/allocations_familiales/tests/tests_allocations_familiales.catala_fr
View File

@ -349,71 +349,159 @@ champ d'application Test14:
```
```catala-test-inline
$ catala Interpret -s Test1
$ catala Typecheck
[WARNING] In scope "PrestationsFamiliales", the variable "prestation_courante" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/allocations_familiales/tests/../prologue.catala_fr:63.9-28:
└──┐
63 │ entrée prestation_courante contenu ÉlémentPrestationsFamiliales
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue
└┬ Champs d'applications
└─ Prestations familiales
[WARNING] In scope "AllocationsFamiliales", the variable "versement" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/allocations_familiales/tests/../prologue.catala_fr:98.10-19:
└──┐
98 │ interne versement contenu VersementAllocations dépend de enfant contenu Enfant
│ ‾‾‾‾‾‾‾‾‾
└┬ Prologue
└┬ Champs d'applications
└─ Allocations familiales
[WARNING] In scope "AllocationsFamiliales", the variable "nombre_enfants_l521_1" is never used anywhere; maybe it's unnecessary?
┌─⯈ examples/allocations_familiales/tests/../prologue.catala_fr:151.10-31:
└───┐
151 │ interne nombre_enfants_l521_1 contenu entier
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue
└┬ Champs d'applications
└─ Allocations familiales
[WARNING] The constructor "PrestationAccueilJeuneEnfant" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/allocations_familiales/tests/../prologue.catala_fr:41.5-33:
└──┐
41 │ -- PrestationAccueilJeuneEnfant
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue
└─ Types de données manipulées par le programme
[WARNING] The constructor "ComplémentFamilial" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/allocations_familiales/tests/../prologue.catala_fr:43.5-23:
└──┐
43 │ -- ComplémentFamilial
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue
└─ Types de données manipulées par le programme
[WARNING] The constructor "AllocationLogement" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/allocations_familiales/tests/../prologue.catala_fr:44.5-23:
└──┐
44 │ -- AllocationLogement
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue
└─ Types de données manipulées par le programme
[WARNING] The constructor "AllocationÉducationEnfantHandicapé" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/allocations_familiales/tests/../prologue.catala_fr:45.5-39:
└──┐
45 │ -- AllocationÉducationEnfantHandicapé
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue
└─ Types de données manipulées par le programme
[WARNING] The constructor "AllocationSoutienFamilial" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/allocations_familiales/tests/../prologue.catala_fr:46.5-30:
└──┐
46 │ -- AllocationSoutienFamilial
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue
└─ Types de données manipulées par le programme
[WARNING] The constructor "AllocationRentréeScolaire" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/allocations_familiales/tests/../prologue.catala_fr:47.5-30:
└──┐
47 │ -- AllocationRentréeScolaire
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue
└─ Types de données manipulées par le programme
[WARNING] The constructor "AllocationJournalièrePresenceParentale" of enumeration "ÉlémentPrestationsFamiliales" is never used; maybe it's unnecessary?
┌─⯈ examples/allocations_familiales/tests/../prologue.catala_fr:48.5-43:
└──┐
48 │ -- AllocationJournalièrePresenceParentale
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ Prologue
└─ Types de données manipulées par le programme
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret -s Test1 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test2
$ catala Interpret -s Test2 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test3
$ catala Interpret -s Test3 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test4
$ catala Interpret -s Test4 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test5
$ catala Interpret -s Test5 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test6
$ catala Interpret -s Test6 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test7
$ catala Interpret -s Test7 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test8
$ catala Interpret -s Test8 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test9
$ catala Interpret -s Test9 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test10
$ catala Interpret -s Test10 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test11
$ catala Interpret -s Test11 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test12
$ catala Interpret -s Test12 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test13
$ catala Interpret -s Test13 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test13
$ catala Interpret -s Test13 --disable_warnings
[RESULT] Computation successful!
```

2
examples/allocations_familiales/tests/tests_ouverture_droits.catala_fr
View File

@ -62,6 +62,6 @@ champ d'application Test1:
```
```catala-test-inline
$ catala Interpret -s Test1
$ catala Interpret -s Test1 --disable_warnings
[RESULT] Computation successful!
```

4
examples/polish_taxes/tests/test_a7_u1_p1.catala_pl
View File

@ -23,11 +23,11 @@ zakres Test_A7_U1_P1_PPb:
```
```catala-test-inline
$ catala Interpret -s Test_A7_U1_P1_PPa
$ catala Interpret -s Test_A7_U1_P1_PPa --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test_A7_U1_P1_PPb
$ catala Interpret -s Test_A7_U1_P1_PPb --disable_warnings
[RESULT] Computation successful!
```

4
examples/polish_taxes/tests/test_a7_u1_p2.catala_pl
View File

@ -23,11 +23,11 @@ zakres Test_A7_U1_P2_PPb:
```
```catala-test-inline
$ catala Interpret -s Test_A7_U1_P2_PPa
$ catala Interpret -s Test_A7_U1_P2_PPa --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test_A7_U1_P2_PPb
$ catala Interpret -s Test_A7_U1_P2_PPb --disable_warnings
[RESULT] Computation successful!
```

2
examples/polish_taxes/tests/test_a7_u1_p3.catala_pl
View File

@ -12,6 +12,6 @@ zakres Test_A7_U1_P3:
asercja sprzedaz.podatek = 1 PLN
```
```catala-test-inline
$ catala Interpret -s Test_A7_U1_P3
$ catala Interpret -s Test_A7_U1_P3 --disable_warnings
[RESULT] Computation successful!
```

2
examples/polish_taxes/tests/test_a7_u1_p4.catala_pl
View File

@ -12,6 +12,6 @@ zakres Test_A7_U1_P4:
asercja sprzedaz.podatek = 1 PLN
```
```catala-test-inline
$ catala Interpret -s Test_A7_U1_P4
$ catala Interpret -s Test_A7_U1_P4 --disable_warnings
[RESULT] Computation successful!
```

2
examples/polish_taxes/tests/test_a7_u1_p7.catala_pl
View File

@ -12,6 +12,6 @@ zakres Test_A7_U1_P7:
asercja sprzedaz.podatek = 1 PLN
```
```catala-test-inline
$ catala Interpret -s Test_A7_U1_P7
$ catala Interpret -s Test_A7_U1_P7 --disable_warnings
[RESULT] Computation successful!
```

2
examples/polish_taxes/tests/test_a7_u1_p9.catala_pl
View File

@ -12,6 +12,6 @@ zakres Test_A7_U1_P9:
asercja sprzedaz.podatek = 5 PLN
```
```catala-test-inline
$ catala Interpret -s Test_A7_U1_P9
$ catala Interpret -s Test_A7_U1_P9 --disable_warnings
[RESULT] Computation successful!
```

2
examples/prestations_familiales/tests/tests_ouverture_droits.catala_fr
View File

@ -62,6 +62,6 @@ champ d'application Test1:
```
```catala-test-inline
$ catala Interpret -s Test1
$ catala Interpret -s Test1 --disable_warnings
[RESULT] Computation successful!
```

4
examples/tutorial_en/tests/test_tutorial.catala_en
View File

@ -29,11 +29,11 @@ scope UnitTest2:
```
```catala-test-inline
$ catala Interpret -s UnitTest1
$ catala Interpret -s UnitTest1 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s UnitTest2
$ catala Interpret -s UnitTest2 --disable_warnings
[RESULT] Computation successful!
```

4
examples/tutoriel_fr/tests/test_tutoriel.catala_fr
View File

@ -29,11 +29,11 @@ champ d'application TestUnitaire2:
```
```catala-test-inline
$ catala Interpret -s TestUnitaire1
$ catala Interpret -s TestUnitaire1 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s TestUnitaire2
$ catala Interpret -s TestUnitaire2 --disable_warnings
[RESULT] Computation successful!
```

12
examples/us_tax_code/tests/test_section_121.catala_en
View File

@ -146,31 +146,31 @@ scope Test6:
```
```catala-test-inline
$ catala Interpret -s Test1
$ catala Interpret -s Test1 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test2
$ catala Interpret -s Test2 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test3
$ catala Interpret -s Test3 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test4
$ catala Interpret -s Test4 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test5
$ catala Interpret -s Test5 --disable_warnings
[RESULT] Computation successful!
```
```catala-test-inline
$ catala Interpret -s Test6
$ catala Interpret -s Test6 --disable_warnings
[RESULT] Computation successful!
```

72
tests/test_arithmetic/bad/division_by_zero.catala_en
View File

@ -33,6 +33,30 @@ scope Money:
```catala-test-inline
$ catala Interpret -s Dec
[WARNING] In scope "Int", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:7.10-11:
└─┐
7 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with integers
[WARNING] In scope "Dec", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:17.10-11:
└──┐
17 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with decimals
[WARNING] In scope "Money", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:27.10-11:
└──┐
27 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with money
[ERROR] division by zero at runtime
The division operator:
@ -55,6 +79,30 @@ The null denominator:
```catala-test-inline
$ catala Interpret -s Int
[WARNING] In scope "Int", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:7.10-11:
└─┐
7 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with integers
[WARNING] In scope "Dec", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:17.10-11:
└──┐
17 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with decimals
[WARNING] In scope "Money", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:27.10-11:
└──┐
27 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with money
[ERROR] division by zero at runtime
The division operator:
@ -77,6 +125,30 @@ The null denominator:
```catala-test-inline
$ catala Interpret -s Money
[WARNING] In scope "Int", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:7.10-11:
└─┐
7 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with integers
[WARNING] In scope "Dec", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:17.10-11:
└──┐
17 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with decimals
[WARNING] In scope "Money", the variable "i" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:27.10-11:
└──┐
27 │ context i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with money
[ERROR] division by zero at runtime
The division operator:

7
tests/test_date/bad/rounding_option.catala_en
View File

@ -12,6 +12,13 @@ scope Test:
```catala-test-inline
$ catala Interpret -s Test
[WARNING] In scope "Test", the variable "ambiguous" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/rounding_option.catala_en:5.10-19:
└─┐
5 │ context ambiguous content boolean
│ ‾‾‾‾‾‾‾‾‾
catala: internal error, uncaught exception:
Dates_calc.Dates.AmbiguousComputation

7
tests/test_date/bad/rounding_option.catala_fr
View File

@ -12,6 +12,13 @@ champ d'application Test:
```catala-test-inline
$ catala Interpret -s Test
[WARNING] In scope "Test", the variable "ambiguité" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/rounding_option.catala_fr:5.11-20:
└─┐
5 │ contexte ambiguité contenu booléen
│ ‾‾‾‾‾‾‾‾‾
catala: internal error, uncaught exception:
Dates_calc.Dates.AmbiguousComputation

128
tests/test_date/bad/uncomparable_duration.catala_en
View File

@ -42,6 +42,38 @@ scope Ge:
```catala-test-inline
$ catala Interpret -s Ge
[WARNING] In scope "Lt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:7.10-11:
└─┐
7 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<` operator
[WARNING] In scope "Le", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:17.10-11:
└──┐
17 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Gt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:27.10-11:
└──┐
27 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Ge", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:37.10-11:
└──┐
37 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `>=` operator
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:40.22-29:
@ -62,6 +94,38 @@ $ catala Interpret -s Ge
```catala-test-inline
$ catala Interpret -s Gt
[WARNING] In scope "Lt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:7.10-11:
└─┐
7 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<` operator
[WARNING] In scope "Le", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:17.10-11:
└──┐
17 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Gt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:27.10-11:
└──┐
27 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Ge", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:37.10-11:
└──┐
37 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `>=` operator
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:30.22-29:
@ -82,6 +146,38 @@ $ catala Interpret -s Gt
```catala-test-inline
$ catala Interpret -s Le
[WARNING] In scope "Lt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:7.10-11:
└─┐
7 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<` operator
[WARNING] In scope "Le", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:17.10-11:
└──┐
17 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Gt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:27.10-11:
└──┐
27 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Ge", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:37.10-11:
└──┐
37 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `>=` operator
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:20.22-29:
@ -102,6 +198,38 @@ $ catala Interpret -s Le
```catala-test-inline
$ catala Interpret -s Lt
[WARNING] In scope "Lt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:7.10-11:
└─┐
7 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<` operator
[WARNING] In scope "Le", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:17.10-11:
└──┐
17 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Gt", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:27.10-11:
└──┐
27 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
[WARNING] In scope "Ge", the variable "d" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:37.10-11:
└──┐
37 │ context d content boolean
│ ‾
└┬ `UncomparableDurations` exception management
└─ `>=` operator
[ERROR] Cannot compare together durations that cannot be converted to a precise number of days
┌─⯈ tests/test_date/bad/uncomparable_duration.catala_en:10.22-29:

7
tests/test_default/bad/conflict.catala_en
View File

@ -11,6 +11,13 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_default/bad/conflict.catala_en:5.10-11:
└─┐
5 │ context x content integer
│ ‾
└─ Article
[ERROR] There is a conflict between multiple valid consequences for assigning the same variable.
This consequence has a valid justification:

14
tests/test_default/bad/empty.catala_en
View File

@ -11,6 +11,20 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_default/bad/empty.catala_en:5.10-11:
└─┐
5 │ context x content integer
│ ‾
└─ Article
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_default/bad/empty.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Article
[ERROR] This variable evaluated to an empty term (no rule that defined it applied in this situation)
┌─⯈ tests/test_default/bad/empty.catala_en:6.10-11:

7
tests/test_default/bad/empty_with_rules.catala_en
View File

@ -14,6 +14,13 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_default/bad/empty_with_rules.catala_en:5.10-11:
└─┐
5 │ context x content integer
│ ‾
└─ Article
[ERROR] This variable evaluated to an empty term (no rule that defined it applied in this situation)
┌─⯈ tests/test_default/bad/empty_with_rules.catala_en:5.10-11:

14
tests/test_enum/bad/missing_case.catala_en
View File

@ -18,6 +18,20 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "out" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_enum/bad/missing_case.catala_en:11.10-13:
└──┐
11 │ context out content boolean
│ ‾‾‾
└─ Article
[WARNING] The constructor "Case3" of enumeration "E" is never used; maybe it's unnecessary?
┌─⯈ tests/test_enum/bad/missing_case.catala_en:7.5-10:
└─┐
7 │ -- Case3
│ ‾‾‾‾‾
└─ Article
[ERROR] The constructor Case3 of enum E is missing from this pattern matching
┌─⯈ tests/test_enum/bad/missing_case.catala_en:14.24-16.21:

7
tests/test_exception/bad/exceptions_cycle.catala_en
View File

@ -20,6 +20,13 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_exception/bad/exceptions_cycle.catala_en:5.10-11:
└─┐
5 │ context x content integer
│ ‾
└─ Test
[ERROR] Exception cycle detected when defining x: each of these 3 exceptions applies over the previous one, and the first applies over the last
┌─⯈ tests/test_exception/bad/exceptions_cycle.catala_en:8.2-10.14:

7
tests/test_exception/bad/self_exception.catala_en
View File

@ -12,6 +12,13 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_exception/bad/self_exception.catala_en:5.10-11:
└─┐
5 │ context y content integer
│ ‾
└─ Test
[ERROR] Cannot define rule as an exception to itself
┌─⯈ tests/test_exception/bad/self_exception.catala_en:9.12-18:

7
tests/test_exception/bad/two_exceptions.catala_en
View File

@ -17,6 +17,13 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_exception/bad/two_exceptions.catala_en:5.10-11:
└─┐
5 │ context x content integer
│ ‾
└─ Test
[ERROR] There is a conflict between multiple valid consequences for assigning the same variable.
This consequence has a valid justification:

21
tests/test_func/good/context_func.catala_en
View File

@ -17,6 +17,13 @@ scope B:
```catala-test-inline
$ catala Scopelang -s B
[WARNING] In scope "A", the variable "f" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_func/good/context_func.catala_en:5.10-11:
└─┐
5 │ context f content integer depends on x content integer
│ ‾
└─ Test
let scope B (b: bool|input) =
let a.f : integer → integer =
λ (x: integer) → ⟨b && x >! 0 ⊢ x -! 1⟩;
@ -25,6 +32,13 @@ let scope B (b: bool|input) =
```catala-test-inline
$ catala Dcalc -s A
[WARNING] In scope "A", the variable "f" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_func/good/context_func.catala_en:5.10-11:
└─┐
5 │ context f content integer depends on x content integer
│ ‾
└─ Test
let A =
λ (A_in: A_in {"f_in": integer → integer}) →
let f : integer → integer = A_in."f_in" in
@ -36,6 +50,13 @@ let A =
```catala-test-inline
$ catala Dcalc -s B
[WARNING] In scope "A", the variable "f" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_func/good/context_func.catala_en:5.10-11:
└─┐
5 │ context f content integer depends on x content integer
│ ‾
└─ Test
let B =
λ (B_in: B_in {"b_in": bool}) →
let b : bool = B_in."b_in" in

7
tests/test_io/bad/redefining_input.catala_en
View File

@ -9,6 +9,13 @@ scope A:
```
```catala-test-inline
$ catala Typecheck
[WARNING] In scope "A", the variable "a" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_io/bad/redefining_input.catala_en:5.8-9:
└─┐
5 │ input a content integer
│ ‾
└─ Test
[ERROR] It is impossible to give a definition to a scope variable tagged as input.
Incriminated variable:

7
tests/test_io/bad/using_non_output.catala_en
View File

@ -15,6 +15,13 @@ scope B:
```
```catala-test-inline
$ catala Typecheck
[WARNING] In scope "A", the variable "a" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_io/bad/using_non_output.catala_en:5.11-12:
└─┐
5 │ internal a content integer
│ ‾
└─ Test
[ERROR] The variable a.a cannot be used here, as it is not part of subscope a's results. Maybe you forgot to qualify it as an output?
Incriminated variable usage:

7
tests/test_proof/bad/array_length-empty.catala_en
View File

@ -12,6 +12,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/array_length-empty.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/array_length-empty.catala_en:6.10-11:
└─┐

7
tests/test_proof/bad/array_length-overlap.catala_en
View File

@ -13,6 +13,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/array_length-overlap.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/array_length-overlap.catala_en:6.10-11:
└─┐

7
tests/test_proof/bad/dates_get_year-empty.catala_en
View File

@ -15,6 +15,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/dates_get_year-empty.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/dates_get_year-empty.catala_en:6.10-11:
└─┐

7
tests/test_proof/bad/dates_get_year-overlap.catala_en
View File

@ -15,6 +15,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/dates_get_year-overlap.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/dates_get_year-overlap.catala_en:6.10-11:
└─┐

7
tests/test_proof/bad/dates_simple-empty.catala_en
View File

@ -14,6 +14,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/dates_simple-empty.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/dates_simple-empty.catala_en:6.10-11:
└─┐

7
tests/test_proof/bad/dates_simple-overlap.catala_en
View File

@ -15,6 +15,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/dates_simple-overlap.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/dates_simple-overlap.catala_en:6.10-11:
└─┐

7
tests/test_proof/bad/duration-empty.catala_en
View File

@ -12,6 +12,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/duration-empty.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/duration-empty.catala_en:6.10-11:
└─┐

7
tests/test_proof/bad/duration-overlap.catala_en
View File

@ -13,6 +13,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/duration-overlap.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/duration-overlap.catala_en:6.10-11:
└─┐

14
tests/test_proof/bad/enums-empty.catala_en
View File

@ -23,6 +23,20 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-empty.catala_en:15.10-11:
└──┐
15 │ context x content integer
│ ‾
└─ Test
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-empty.catala_en:7.6-7:
└─┐
7 │ -- C content boolean
│ ‾
└─ Test
[ERROR] [A.x] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/enums-empty.catala_en:15.10-11:
└──┐

14
tests/test_proof/bad/enums-nonbool-empty.catala_en
View File

@ -21,6 +21,20 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-nonbool-empty.catala_en:13.10-11:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-nonbool-empty.catala_en:5.6-7:
└─┐
5 │ -- C content boolean
│ ‾
└─ Test
[ERROR] [A.x] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/enums-nonbool-empty.catala_en:13.10-11:
└──┐

14
tests/test_proof/bad/enums-nonbool-overlap.catala_en
View File

@ -21,6 +21,20 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-nonbool-overlap.catala_en:13.10-11:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-nonbool-overlap.catala_en:5.6-7:
└─┐
5 │ -- C content boolean
│ ‾
└─ Test
[ERROR] [A.x] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/enums-nonbool-overlap.catala_en:13.10-11:
└──┐

14
tests/test_proof/bad/enums-overlap.catala_en
View File

@ -23,6 +23,20 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-overlap.catala_en:15.10-11:
└──┐
15 │ context x content integer
│ ‾
└─ Test
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums-overlap.catala_en:7.6-7:
└─┐
7 │ -- C content boolean
│ ‾
└─ Test
[ERROR] [A.x] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/enums-overlap.catala_en:15.10-11:
└──┐

14
tests/test_proof/bad/enums_inj-empty.catala_en
View File

@ -16,6 +16,20 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums_inj-empty.catala_en:10.10-11:
└──┐
10 │ context y content integer
│ ‾
└─ Article
[WARNING] The constructor "C2" of enumeration "E" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums_inj-empty.catala_en:6.5-7:
└─┐
6 │ -- C2
│ ‾‾
└─ Article
[ERROR] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/enums_inj-empty.catala_en:10.10-11:
└──┐

7
tests/test_proof/bad/enums_inj-overlap.catala_en
View File

@ -18,6 +18,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums_inj-overlap.catala_en:10.10-11:
└──┐
10 │ context y content integer
│ ‾
└─ Article
[ERROR] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/enums_inj-overlap.catala_en:10.10-11:
└──┐

7
tests/test_proof/bad/enums_unit-empty.catala_en
View File

@ -21,6 +21,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums_unit-empty.catala_en:10.10-11:
└──┐
10 │ context y content integer
│ ‾
└─ Article
[ERROR] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/enums_unit-empty.catala_en:10.10-11:
└──┐

7
tests/test_proof/bad/enums_unit-overlap.catala_en
View File

@ -21,6 +21,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/enums_unit-overlap.catala_en:10.10-11:
└──┐
10 │ context y content integer
│ ‾
└─ Article
[ERROR] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/enums_unit-overlap.catala_en:10.10-11:
└──┐

7
tests/test_proof/bad/let_in_condition-empty.catala_en
View File

@ -13,6 +13,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/let_in_condition-empty.catala_en:5.10-11:
└─┐
5 │ context x content boolean
│ ‾
└─ Test
[ERROR] [A.x] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/let_in_condition-empty.catala_en:5.10-11:
└─┐

7
tests/test_proof/bad/money-empty.catala_en
View File

@ -16,6 +16,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/money-empty.catala_en:8.10-11:
└─┐
8 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/money-empty.catala_en:8.10-11:
└─┐

7
tests/test_proof/bad/money-overlap.catala_en
View File

@ -17,6 +17,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/money-overlap.catala_en:8.10-11:
└─┐
8 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/money-overlap.catala_en:8.10-11:
└─┐

7
tests/test_proof/bad/no_vars-conflict.catala_en
View File

@ -17,6 +17,13 @@ scope A:
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/no_vars-conflict.catala_en:8.10-11:
└─┐
8 │ context y content integer
│ ‾
└─ Test
[ERROR] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/no_vars-conflict.catala_en:8.10-11:
└─┐

7
tests/test_proof/bad/no_vars-empty.catala_en
View File

@ -16,6 +16,13 @@ scope A:
```
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/no_vars-empty.catala_en:7.10-11:
└─┐
7 │ context y content integer
│ ‾
└─ Test
[ERROR] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/no_vars-empty.catala_en:7.10-11:
└─┐

16
tests/test_proof/bad/prolala_motivating_example.catala_en
View File

@ -123,6 +123,22 @@ scope Amount:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "Amount", the variable "amount" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/prolala_motivating_example.catala_en:60.10-16:
└──┐
60 │ context amount content integer
│ ‾‾‾‾‾‾
└┬ ProLaLa 2022 Super Cash Bonus
└─ Amount
[WARNING] In scope "Amount", the variable "correct_amount" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/prolala_motivating_example.catala_en:61.10-24:
└──┐
61 │ context correct_amount content integer
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾
└┬ ProLaLa 2022 Super Cash Bonus
└─ Amount
[ERROR] [Amount.amount] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/prolala_motivating_example.catala_en:60.10-16:
└──┐

7
tests/test_proof/bad/rationals-empty.catala_en
View File

@ -12,6 +12,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/rationals-empty.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/rationals-empty.catala_en:6.10-11:
└─┐

7
tests/test_proof/bad/rationals-overlap.catala_en
View File

@ -13,6 +13,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/rationals-overlap.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[ERROR] [A.y] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/rationals-overlap.catala_en:6.10-11:
└─┐

7
tests/test_proof/bad/sat_solving.catala_en
View File

@ -40,6 +40,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x10" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/sat_solving.catala_en:15.10-13:
└──┐
15 │ context x10 content boolean
│ ‾‾‾
└─ Test
[ERROR] [A.x10] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/sat_solving.catala_en:15.10-13:
└──┐

7
tests/test_proof/bad/structs-empty.catala_en
View File

@ -21,6 +21,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/structs-empty.catala_en:13.10-11:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[ERROR] [A.x] This variable might return an empty error:
┌─⯈ tests/test_proof/bad/structs-empty.catala_en:13.10-11:
└──┐

7
tests/test_proof/bad/structs-overlap.catala_en
View File

@ -21,6 +21,13 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/bad/structs-overlap.catala_en:13.10-11:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[ERROR] [A.x] At least two exceptions overlap for this variable:
┌─⯈ tests/test_proof/bad/structs-overlap.catala_en:13.10-11:
└──┐

7
tests/test_proof/good/array_length.catala_en
View File

@ -13,5 +13,12 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/array_length.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

7
tests/test_proof/good/dates_get_year.catala_en
View File

@ -15,5 +15,12 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/dates_get_year.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

7
tests/test_proof/good/dates_simple.catala_en
View File

@ -15,5 +15,12 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/dates_simple.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

7
tests/test_proof/good/duration.catala_en
View File

@ -13,5 +13,12 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "y" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/duration.catala_en:6.10-11:
└─┐
6 │ context y content boolean
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

14
tests/test_proof/good/enums-arith.catala_en
View File

@ -21,5 +21,19 @@ scope A:
```catala-test-inline
$ catala Proof --disable_counterexamples
[WARNING] In scope "A", the variable "x" is never used anywhere; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/enums-arith.catala_en:13.10-11:
└──┐
13 │ context x content integer
│ ‾
└─ Test
[WARNING] The constructor "C" of enumeration "T" is never used; maybe it's unnecessary?
┌─⯈ tests/test_proof/good/enums-arith.catala_en:5.6-7:
└─┐
5 │ -- C content boolean
│ ‾
└─ Test
[RESULT] No errors found during the proof mode run.
```

Some files were not shown because too many files have changed in this diff Show More