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

Unify runtime error handling (#611)

Browse Source
This commit is contained in:
Denis Merigoux 2024-05-03 10:11:36 +02:00 committed by GitHub
commit 0f425dc408
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
65 changed files with 1244 additions and 1199 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Makefile
View File

@ -194,14 +194,14 @@ syntax:
# High-level test and benchmarks commands
##########################################
CATALA_OPTS ?=
CATALAOPTS ?=
CLERK_OPTS ?=
CATALA_BIN=_build/default/$(COMPILER_DIR)/catala.exe
CLERK_BIN=_build/default/$(BUILD_SYSTEM_DIR)/clerk.exe
CLERK_TEST=$(CLERK_BIN) test --exe $(CATALA_BIN) \
$(CLERK_OPTS) $(if $(CATALA_OPTS),--catala-opts=$(CATALA_OPTS),)
$(CLERK_OPTS) $(if $(CATALAOPTS),--catala-opts=$(CATALAOPTS),)
.FORCE:
@ -234,7 +234,7 @@ testsuite: unit-tests
#> reset-tests : Update the expected test results from current run
reset-tests: .FORCE $(CLERK_BIN)
$(CLERK_TEST) tests --reset
$(CLERK_TEST) tests doc --reset
tests/%: .FORCE
$(CLERK_TEST) test $@

2
compiler/catala_utils/dune
View File

@ -3,7 +3,7 @@
(public_name catala.catala_utils)
(modules
(:standard \ get_version))
(libraries unix cmdliner ubase ocolor re bindlib catala.runtime_ocaml))
(libraries unix cmdliner ubase ocolor re))
(executable
(name get_version)

36
compiler/catala_utils/file.ml
View File

@ -180,6 +180,42 @@ let process_out ?check_exit cmd args =
assert false
with End_of_file -> Buffer.contents buf
(* SIDE EFFECT AT MODULE LOAD: sets up a signal handler on SIGWINCH (window
resize) *)
let () =
let default = 80 in
let get_terminal_cols () =
let count =
try (* terminfo *)
process_out "tput" ["cols"] |> int_of_string
with Failure _ -> (
try
(* stty *)
process_out "stty" ["size"]
|> fun s ->
let i = String.rindex s ' ' + 1 in
String.sub s (i + 1) (String.length s - i) |> int_of_string
with Failure _ | Not_found | Invalid_argument _ -> (
try int_of_string (Sys.getenv "COLUMNS")
with Not_found | Failure _ -> 0))
in
if count > 0 then count else default
in
let width = ref None in
let () =
try
Sys.set_signal 28 (* SIGWINCH *)
(Sys.Signal_handle (fun _ -> width := None))
with Invalid_argument _ -> ()
in
Message.set_terminal_width_function (fun () ->
match !width with
| Some n -> n
| None ->
let r = get_terminal_cols () in
width := Some r;
r)
let check_directory d =
try
let d = Unix.realpath d in

40
compiler/catala_utils/message.ml
View File

@ -34,22 +34,39 @@ let unstyle_formatter ppf =
[Format.sprintf] etc. functions (ignoring them) *)
let () = ignore (unstyle_formatter Format.str_formatter)
let terminal_columns, set_terminal_width_function =
let get_cols = ref (fun () -> 80) in
(fun () -> !get_cols ()), fun f -> get_cols := f
(* Note: we could do the same for std_formatter, err_formatter... but we'd
rather promote the use of the formatting functions of this module and the
below std_ppf / err_ppf *)
let has_color oc =
let has_color_raw ~(tty : bool Lazy.t) =
match Global.options.color with
| Global.Never -> false
| Always -> true
| Auto -> Unix.(isatty (descr_of_out_channel oc))
| Auto -> Lazy.force tty
let has_color oc =
has_color_raw ~tty:(lazy Unix.(isatty (descr_of_out_channel oc)))
(* Here we create new formatters to stderr/stdout that remain separate from the
ones used by [Format.printf] / [Format.eprintf] (which remain unchanged) *)
let formatter_of_out_channel oc =
let tty = lazy Unix.(isatty (descr_of_out_channel oc)) in
let ppf = Format.formatter_of_out_channel oc in
if has_color oc then color_formatter ppf else unstyle_formatter ppf
let ppf =
if has_color_raw ~tty then color_formatter ppf else unstyle_formatter ppf
in
let out, flush = Format.pp_get_formatter_output_functions ppf () in
let flush () =
if Lazy.force tty then Format.pp_set_margin ppf (terminal_columns ());
flush ()
in
Format.pp_set_formatter_output_functions ppf out flush;
ppf
let std_ppf = lazy (formatter_of_out_channel stdout)
let err_ppf = lazy (formatter_of_out_channel stderr)
@ -196,22 +213,21 @@ module Content = struct
content
| some -> some
in
pos, m
| Position { pos_message; pos } ->
let message =
match pos_message with Some m -> m | None -> fun _ -> ()
in
Some pos, message
| Outcome m -> None, m
| Suggestion sl -> None, fun ppf -> Suggestions.format ppf sl
pos, Some m
| Position { pos_message; pos } -> Some pos, pos_message
| Outcome m -> None, Some m
| Suggestion sl -> None, Some (fun ppf -> Suggestions.format ppf sl)
in
Option.iter
(fun pos ->
Format.fprintf ppf "@{<blue>%s@}: " (Pos.to_string_short pos))
pos;
pp_marker target ppf;
match message with
| Some message ->
Format.pp_print_char ppf ' ';
Format.pp_print_string ppf (unformat message))
Format.pp_print_string ppf (unformat message)
| None -> ())
ppf content;
Format.pp_print_newline ppf ()
end

1
compiler/catala_utils/message.mli
View File

@ -71,6 +71,7 @@ val unformat : (Format.formatter -> unit) -> string
indents *)
val has_color : out_channel -> bool
val set_terminal_width_function : (unit -> int) -> unit
(* {1 More general color-enabled formatting helpers}*)

13
compiler/dcalc/from_scopelang.ml
View File

@ -139,7 +139,8 @@ let tag_with_log_entry
let m = mark_tany (Mark.get e) (Expr.pos e) in
if Global.options.trace then
Expr.eappop ~op:(Log (l, markings)) ~tys:[TAny, Expr.pos e] ~args:[e] m
let pos = Expr.pos e in
Expr.eappop ~op:(Log (l, markings), pos) ~tys:[TAny, pos] ~args:[e] m
else e
(* In a list of exceptions, it is normally an error if more than a single one
@ -264,7 +265,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm S.expr) : 'm Ast.expr boxed =
( var_ctx.scope_input_name,
Expr.make_abs
[| Var.make "_" |]
(Expr.eemptyerror (Expr.with_ty m ty0))
(Expr.eempty (Expr.with_ty m ty0))
[TAny, iopos]
pos )
| Some var_ctx, Some e ->
@ -565,12 +566,12 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm S.expr) : 'm Ast.expr boxed =
let v, _ = TopdefName.Map.find (Mark.remove name) ctx.toplevel_vars in
Expr.evar v m
else Expr.eexternal ~name:(Mark.map (fun n -> External_value n) name) m
| EAppOp { op = Add_dat_dur _; args; tys } ->
| EAppOp { op = Add_dat_dur _, opos; args; tys } ->
let args = List.map (translate_expr ctx) args in
Expr.eappop ~op:(Add_dat_dur ctx.date_rounding) ~args ~tys m
Expr.eappop ~op:(Add_dat_dur ctx.date_rounding, opos) ~args ~tys m
| ( EVar _ | EAbs _ | ELit _ | EStruct _ | EStructAccess _ | ETuple _
| ETupleAccess _ | EInj _ | EEmptyError | EErrorOnEmpty _ | EArray _
| EIfThenElse _ | EAppOp _ ) as e ->
| ETupleAccess _ | EInj _ | EFatalError _ | EEmpty | EErrorOnEmpty _
| EArray _ | EIfThenElse _ | EAppOp _ ) as e ->
Expr.map ~f:(translate_expr ctx) ~op:Operator.translate (e, m)
(** The result of a rule translation is a list of assignments, with variables

2
compiler/desugared/ast.ml
View File

@ -187,7 +187,7 @@ let empty_rule
(parameters : (Uid.MarkedString.info * typ) list Mark.pos option) : rule =
{
rule_just = Expr.box (ELit (LBool false), Untyped { pos });
rule_cons = Expr.box (EEmptyError, Untyped { pos });
rule_cons = Expr.box (EEmpty, Untyped { pos });
rule_parameter =
Option.map
(Mark.map (List.map (fun (lbl, typ) -> Mark.map Var.make lbl, typ)))

93
compiler/desugared/from_surface.ml
View File

@ -42,7 +42,7 @@ let translate_binop :
Ast.expr boxed =
fun (op, op_pos) pos lhs rhs ->
let op_expr op tys =
Expr.eappop ~op
Expr.eappop ~op:(op, op_pos)
~tys:(List.map (Mark.add op_pos) tys)
~args:[lhs; rhs]
(Untyped { pos })
@ -114,7 +114,10 @@ let translate_binop :
let translate_unop ((op, op_pos) : S.unop Mark.pos) pos arg : Ast.expr boxed =
let op_expr op ty =
Expr.eappop ~op ~tys:[Mark.add op_pos ty] ~args:[arg] (Untyped { pos })
Expr.eappop ~op:(op, op_pos)
~tys:[Mark.add op_pos ty]
~args:[arg]
(Untyped { pos })
in
match op with
| S.Not -> op_expr Not (TLit TBool)
@ -238,12 +241,12 @@ let rec translate_expr
let rec_helper ?(local_vars = local_vars) e =
translate_expr scope inside_definition_of ctxt local_vars e
in
let rec detuplify_list names = function
let rec detuplify_list opos names = function
(* Where a list is expected (e.g. after [among]), as syntactic sugar, if a
tuple is found instead we transpose it into a list of tuples *)
| S.Tuple ls, pos ->
let m = Untyped { pos } in
let ls = List.map (detuplify_list []) ls in
let ls = List.map (detuplify_list opos []) ls in
let rec zip names = function
| [] -> assert false
| [l] -> l
@ -272,7 +275,7 @@ let rec translate_expr
(Expr.make_tuple (Expr.evar x1 m :: explode (Expr.evar x2 m)) m)
tys pos
in
Expr.eappop ~op:Map2 ~args:[f_join; l1; rhs]
Expr.eappop ~op:(Map2, opos) ~args:[f_join; l1; rhs]
~tys:((TAny, pos) :: List.map (fun ty -> TArray ty, pos) tys)
m
in
@ -286,7 +289,7 @@ let rec translate_expr
match Mark.remove expr with
| Paren e -> rec_helper e
| Binop
( (S.And, _pos_op),
( (S.And, pos_op),
( TestMatchCase (e1_sub, ((constructors, Some binding), pos_pattern)),
_pos_e1 ),
e2 ) ->
@ -302,14 +305,14 @@ let rec translate_expr
let nop_var = Var.make "_" in
Expr.make_abs [| nop_var |]
(Expr.elit (LBool false) emark)
[tau] pos
[tau] pos_op
else
let binding_var = Var.make (Mark.remove binding) in
let local_vars =
Ident.Map.add (Mark.remove binding) binding_var local_vars
in
let e2 = rec_helper ~local_vars e2 in
Expr.make_abs [| binding_var |] e2 [tau] pos)
Expr.make_abs [| binding_var |] e2 [tau] pos_op)
(EnumName.Map.find enum_uid ctxt.enums)
in
Expr.ematch ~e:(rec_helper e1_sub) ~name:enum_uid ~cases emark
@ -330,12 +333,18 @@ let rec translate_expr
match l with
| LNumber ((Int i, _), None) -> LInt (Runtime.integer_of_string i)
| LNumber ((Int i, _), Some (Percent, _)) ->
LRat Runtime.(Oper.o_div_rat_rat (decimal_of_string i) rat100)
LRat
Runtime.(
Oper.o_div_rat_rat (Expr.pos_to_runtime pos) (decimal_of_string i)
rat100)
| LNumber ((Dec (i, f), _), None) ->
LRat Runtime.(decimal_of_string (i ^ "." ^ f))
| LNumber ((Dec (i, f), _), Some (Percent, _)) ->
LRat
Runtime.(Oper.o_div_rat_rat (decimal_of_string (i ^ "." ^ f)) rat100)
Runtime.(
Oper.o_div_rat_rat (Expr.pos_to_runtime pos)
(decimal_of_string (i ^ "." ^ f))
rat100)
| LBool b -> LBool b
| LMoneyAmount i ->
LMoney
@ -366,7 +375,7 @@ let rec translate_expr
(try
Runtime.date_of_numbers date.literal_date_year
date.literal_date_month date.literal_date_day
with Runtime.ImpossibleDate ->
with Failure _ ->
Message.error ~pos
"There is an error in this date, it does not correspond to a \
correct calendar day")
@ -487,7 +496,7 @@ let rec translate_expr
in
Expr.edstructaccess ~e ~field:(Mark.remove x) ~name_opt:(get_str ctxt path)
emark
| FunCall ((Builtin b, _), [arg]) ->
| FunCall ((Builtin b, pos), [arg]) ->
let op, ty =
match b with
| S.ToDecimal -> Op.ToRat, TAny
@ -500,7 +509,7 @@ let rec translate_expr
| S.FirstDayOfMonth -> Op.FirstDayOfMonth, TLit TDate
| S.LastDayOfMonth -> Op.LastDayOfMonth, TLit TDate
in
Expr.eappop ~op ~tys:[ty, pos] ~args:[rec_helper arg] emark
Expr.eappop ~op:(op, pos) ~tys:[ty, pos] ~args:[rec_helper arg] emark
| S.Builtin _ ->
Message.error ~pos "Invalid use of built-in: needs one operand"
| FunCall (f, args) ->
@ -717,10 +726,10 @@ let rec translate_expr
| Tuple es -> Expr.etuple (List.map rec_helper es) emark
| TupleAccess (e, n) ->
Expr.etupleaccess ~e:(rec_helper e) ~index:(Mark.remove n - 1) ~size:0 emark
| CollectionOp (((S.Filter { f } | S.Map { f }) as op), collection) ->
| CollectionOp ((((S.Filter { f } | S.Map { f }), opos) as op), collection) ->
let param_names, predicate = f in
let collection =
detuplify_list (List.map Mark.remove param_names) collection
detuplify_list opos (List.map Mark.remove param_names) collection
in
let params = List.map (fun n -> Var.make (Mark.remove n)) param_names in
let local_vars =
@ -756,18 +765,19 @@ let rec translate_expr
Expr.eappop
~op:
(match op with
| S.Map _ -> Map
| S.Filter _ -> Filter
| S.Map _, pos -> Map, pos
| S.Filter _, pos -> Filter, pos
| _ -> assert false)
~tys:[TAny, pos; TAny, pos]
~args:[f_pred; collection] emark
| CollectionOp
( S.AggregateArgExtremum { max; default; f = param_names, predicate },
( ( S.AggregateArgExtremum { max; default; f = param_names, predicate },
opos ),
collection ) ->
let default = rec_helper default in
let pos_dft = Expr.pos default in
let collection =
detuplify_list (List.map Mark.remove param_names) collection
detuplify_list opos (List.map Mark.remove param_names) collection
in
let params = List.map (fun n -> Var.make (Mark.remove n)) param_names in
let local_vars =
@ -775,7 +785,7 @@ let rec translate_expr
(fun vars n p -> Ident.Map.add (Mark.remove n) p vars)
local_vars param_names params
in
let cmp_op = if max then Op.Gt else Op.Lt in
let cmp_op = if max then Op.Gt, opos else Op.Lt, opos in
let f_pred =
Expr.make_abs (Array.of_list params)
(rec_helper ~local_vars predicate)
@ -814,10 +824,10 @@ let rec translate_expr
let weighted_result =
Expr.make_let_in weights_var
(TArray (TTuple [TAny, pos; TAny, pos], pos), pos)
(Expr.eappop ~op:Map
(Expr.eappop ~op:(Map, opos)
~tys:[TAny, pos; TArray (TAny, pos), pos]
~args:[add_weight_f; collection] emark)
(Expr.eappop ~op:Reduce
(Expr.eappop ~op:(Reduce, opos)
~tys:[TAny, pos; TAny, pos; TAny, pos]
~args:[reduce_f; default; Expr.evar weights_var emark]
emark)
@ -825,14 +835,15 @@ let rec translate_expr
in
Expr.etupleaccess ~e:weighted_result ~index:0 ~size:2 emark
| CollectionOp
(((Exists { predicate } | Forall { predicate }) as op), collection) ->
((((Exists { predicate } | Forall { predicate }), opos) as op), collection)
->
let collection =
detuplify_list (List.map Mark.remove (fst predicate)) collection
detuplify_list opos (List.map Mark.remove (fst predicate)) collection
in
let init, op =
match op with
| Exists _ -> false, S.Or
| Forall _ -> true, S.And
| Exists _, pos -> false, (S.Or, pos)
| Forall _, pos -> true, (S.And, pos)
| _ -> assert false
in
let init = Expr.elit (LBool init) emark in
@ -851,15 +862,14 @@ let rec translate_expr
Expr.eabs
(Expr.bind
(Array.of_list (acc_var :: params))
(translate_binop (op, pos) pos acc
(rec_helper ~local_vars predicate)))
(translate_binop op pos acc (rec_helper ~local_vars predicate)))
[TAny, pos; TAny, pos]
emark
in
Expr.eappop ~op:Fold
Expr.eappop ~op:(Fold, opos)
~tys:[TAny, pos; TAny, pos; TAny, pos]
~args:[f; init; collection] emark
| CollectionOp (AggregateExtremum { max; default }, collection) ->
| CollectionOp ((AggregateExtremum { max; default }, opos), collection) ->
let collection = rec_helper collection in
let default = rec_helper default in
let op = if max then S.Gt KPoly else S.Lt KPoly in
@ -874,11 +884,11 @@ let rec translate_expr
[TAny, pos; TAny, pos]
pos
in
Expr.eappop ~op:Reduce
Expr.eappop ~op:(Reduce, opos)
~tys:[TAny, pos; TAny, pos; TAny, pos]
~args:[op_f; default; collection]
emark
| CollectionOp (AggregateSum { typ }, collection) ->
| CollectionOp ((AggregateSum { typ }, opos), collection) ->
let collection = rec_helper collection in
let default_lit =
let i0 = Runtime.integer_of_int 0 in
@ -888,7 +898,8 @@ let rec translate_expr
| S.Money -> LMoney (Runtime.money_of_cents_integer i0)
| S.Duration -> LDuration (Runtime.duration_of_numbers 0 0 0)
| t ->
Message.error ~pos "It is impossible to sum values of type %a together"
Message.error ~pos:opos
"It is impossible to sum values of type %a together"
SurfacePrint.format_primitive_typ t
in
let op_f =
@ -899,28 +910,28 @@ let rec translate_expr
let x1 = Expr.make_var v1 emark in
let x2 = Expr.make_var v2 emark in
Expr.make_abs [| v1; v2 |]
(translate_binop (S.Add KPoly, pos) pos x1 x2)
(translate_binop (S.Add KPoly, opos) pos x1 x2)
[TAny, pos; TAny, pos]
pos
in
Expr.eappop ~op:Reduce
Expr.eappop ~op:(Reduce, opos)
~tys:[TAny, pos; TAny, pos; TAny, pos]
~args:[op_f; Expr.elit default_lit emark; collection]
emark
| MemCollection (member, collection) ->
| CollectionOp ((Member { element = member }, opos), collection) ->
let param_var = Var.make "collection_member" in
let param = Expr.make_var param_var emark in
let collection = detuplify_list ["collection_member"] collection in
let collection = detuplify_list opos ["collection_member"] collection in
let init = Expr.elit (LBool false) emark in
let acc_var = Var.make "acc" in
let acc = Expr.make_var acc_var emark in
let f_body =
let member = rec_helper member in
Expr.eappop ~op:Or
Expr.eappop ~op:(Or, opos)
~tys:[TLit TBool, pos; TLit TBool, pos]
~args:
[
Expr.eappop ~op:Eq
Expr.eappop ~op:(Eq, opos)
~tys:[TAny, pos; TAny, pos]
~args:[member; param] emark;
acc;
@ -933,7 +944,7 @@ let rec translate_expr
[TLit TBool, pos; TAny, pos]
emark
in
Expr.eappop ~op:Fold
Expr.eappop ~op:(Fold, opos)
~tys:[TAny, pos; TAny, pos; TAny, pos]
~args:[f; init; collection] emark
@ -1084,7 +1095,7 @@ let merge_conditions
(default_pos : Pos.t) : Ast.expr boxed =
match precond, cond with
| Some precond, Some cond ->
Expr.eappop ~op:And
Expr.eappop ~op:(And, default_pos)
~tys:[TLit TBool, default_pos; TLit TBool, default_pos]
~args:[precond; cond] (Mark.get cond)
| Some precond, None -> Mark.remove precond, Untyped { pos = default_pos }

38
compiler/driver.ml
View File

@ -330,6 +330,27 @@ module Commands = struct
Message.error "There is no scope \"@{<yellow>%s@}\" inside the program."
scope
let get_scopeopt_uid (ctx : decl_ctx) (scope_opt : string option) :
ScopeName.t =
match scope_opt with
| Some s -> get_scope_uid ctx s
| None -> (
match ScopeName.Map.cardinal ctx.ctx_scopes with
| 0 -> Message.error "The program defines no scopes"
| 1 ->
let s, _ = ScopeName.Map.choose ctx.ctx_scopes in
Message.warning
"No scope was specified, using the only one defined by the program:@ \
%a"
ScopeName.format s;
s
| _ ->
Message.error
"Please specify option @{<yellow>--scope@} or @{<yellow>-s@}.@ The \
program defines the following scopes:@ @[<hv 4>%a@]"
(ScopeName.Map.format_keys ~pp_sep:Format.pp_print_space)
ctx.ctx_scopes)
(* TODO: this is very weird but I'm trying to maintain the current behaviour
for now *)
let get_random_scope_uid (ctx : decl_ctx) : ScopeName.t =
@ -680,14 +701,19 @@ module Commands = struct
result)
results
let interpret_dcalc typed options includes optimize check_invariants ex_scope
=
let interpret_dcalc
typed
options
includes
optimize
check_invariants
ex_scope_opt =
let prg, _ =
Passes.dcalc options ~includes ~optimize ~check_invariants ~typed
in
Interpreter.load_runtime_modules prg;
print_interpretation_results options Interpreter.interpret_program_dcalc prg
(get_scope_uid prg.decl_ctx ex_scope)
(get_scopeopt_uid prg.decl_ctx ex_scope_opt)
let lcalc
typed
@ -749,14 +775,14 @@ module Commands = struct
includes
optimize
check_invariants
ex_scope =
ex_scope_opt =
let prg, _ =
Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion ~monomorphize_types ~typed
in
Interpreter.load_runtime_modules prg;
print_interpretation_results options Interpreter.interpret_program_lcalc prg
(get_scope_uid prg.decl_ctx ex_scope)
(get_scopeopt_uid prg.decl_ctx ex_scope_opt)
let interpret_cmd =
let f lcalc avoid_exceptions closure_conversion monomorphize_types no_typing
@ -793,7 +819,7 @@ module Commands = struct
$ Cli.Flags.include_dirs
$ Cli.Flags.optimize
$ Cli.Flags.check_invariants
$ Cli.Flags.ex_scope)
$ Cli.Flags.ex_scope_opt)
let ocaml
options

17
compiler/lcalc/closure_conversion.ml
View File

@ -38,7 +38,8 @@ let rec transform_closures_expr :
let m = Mark.get e in
match Mark.remove e with
| EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ | EArray _
| ELit _ | EExternal _ | EAssert _ | EIfThenElse _ | ERaise _ | ECatch _ ->
| ELit _ | EExternal _ | EAssert _ | EFatalError _ | EIfThenElse _
| ERaiseEmpty | ECatchEmpty _ ->
Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union
~f:(transform_closures_expr ctx)
e
@ -144,7 +145,8 @@ let rec transform_closures_expr :
(* let env = from_closure_env env in let arg0 = env.0 in ... *)
let new_closure_body =
Expr.make_let_in closure_env_var any_ty
(Expr.eappop ~op:Operator.FromClosureEnv
(Expr.eappop
~op:(Operator.FromClosureEnv, binder_pos)
~tys:[TClosureEnv, binder_pos]
~args:[Expr.evar closure_env_arg_var binder_mark]
binder_mark)
@ -177,7 +179,8 @@ let rec transform_closures_expr :
(Expr.make_tuple
((Bindlib.box_var code_var, binder_mark)
:: [
Expr.eappop ~op:Operator.ToClosureEnv
Expr.eappop
~op:(Operator.ToClosureEnv, binder_pos)
~tys:[TAny, Expr.pos e]
~args:
[
@ -196,7 +199,7 @@ let rec transform_closures_expr :
(Expr.pos e) )
| EAppOp
{
op = (HandleDefaultOpt | Fold | Map | Filter | Reduce) as op;
op = ((HandleDefaultOpt | Fold | Map | Filter | Reduce), _) as op;
tys;
args;
} ->
@ -491,7 +494,7 @@ let rec hoist_closures_expr :
~args:new_args ~tys m )
| EAppOp
{
op = (HandleDefaultOpt | Fold | Map | Filter | Reduce) as op;
op = ((HandleDefaultOpt | Fold | Map | Filter | Reduce), _) as op;
tys;
args;
} ->
@ -538,8 +541,8 @@ let rec hoist_closures_expr :
],
Expr.make_var closure_var m )
| EApp _ | EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _
| EArray _ | ELit _ | EAssert _ | EAppOp _ | EIfThenElse _ | ERaise _
| ECatch _ | EVar _ ->
| EArray _ | ELit _ | EAssert _ | EFatalError _ | EAppOp _ | EIfThenElse _
| ERaiseEmpty | ECatchEmpty _ | EVar _ ->
Expr.map_gather ~acc:[] ~join:( @ ) ~f:(hoist_closures_expr name_context) e
| EExternal _ -> failwith "unimplemented"
| _ -> .

11
compiler/lcalc/compile_with_exceptions.ml
View File

@ -51,7 +51,8 @@ let rec translate_default
let exceptions =
List.map (fun except -> Expr.thunk_term (translate_expr except)) exceptions
in
Expr.eappop ~op:Op.HandleDefault
Expr.eappop
~op:(Op.HandleDefault, Expr.pos cons)
~tys:
[
TArray (TArrow ([TLit TUnit, pos], (TAny, pos)), pos), pos;
@ -71,12 +72,10 @@ let rec translate_default
and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
match e with
| EEmptyError, m -> Expr.eraise EmptyError (translate_mark m)
| EEmpty, m -> Expr.eraiseempty (translate_mark m)
| EErrorOnEmpty arg, m ->
let m = translate_mark m in
Expr.ecatch (translate_expr arg) EmptyError
(Expr.eraise NoValueProvided m)
m
Expr.ecatchempty (translate_expr arg) (Expr.efatalerror Runtime.NoValue m) m
| EDefault { excepts; just; cons }, m ->
translate_default excepts just cons (translate_mark m)
| EPureDefault e, _ -> translate_expr e
@ -87,7 +86,7 @@ and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
(translate_mark m)
| ( ( ELit _ | EArray _ | EVar _ | EAbs _ | EApp _ | EExternal _
| EIfThenElse _ | ETuple _ | ETupleAccess _ | EInj _ | EAssert _
| EStruct _ | EStructAccess _ | EMatch _ ),
| EFatalError _ | EStruct _ | EStructAccess _ | EMatch _ ),
_ ) as e ->
Expr.map ~f:translate_expr ~typ:translate_typ e
| _ -> .

13
compiler/lcalc/compile_without_exceptions.ml
View File

@ -61,7 +61,8 @@ let rec translate_default
let pos = Expr.mark_pos mark_default in
let exceptions = List.map translate_expr exceptions in
let exceptions_and_cons_ty = Expr.maybe_ty mark_default in
Expr.eappop ~op:Op.HandleDefaultOpt
Expr.eappop
~op:(Op.HandleDefaultOpt, Expr.pos cons)
~tys:
[
TArray exceptions_and_cons_ty, pos;
@ -83,7 +84,7 @@ let rec translate_default
and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
match e with
| EEmptyError, m ->
| EEmpty, m ->
let m = translate_mark m in
let pos = Expr.mark_pos m in
Expr.einj
@ -97,10 +98,8 @@ and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
[
( Expr.none_constr,
let x = Var.make "_" in
Expr.make_abs [| x |]
(Expr.eraise NoValueProvided m)
[TAny, pos]
pos );
Expr.make_abs [| x |] (Expr.efatalerror NoValue m) [TAny, pos] pos
);
(* | None x -> raise NoValueProvided *)
Expr.some_constr, Expr.fun_id ~var_name:"arg" m (* | Some x -> x *);
]
@ -118,7 +117,7 @@ and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
(translate_mark m)
| ( ( ELit _ | EArray _ | EVar _ | EApp _ | EAbs _ | EExternal _
| EIfThenElse _ | ETuple _ | ETupleAccess _ | EInj _ | EAssert _
| EStruct _ | EStructAccess _ | EMatch _ ),
| EFatalError _ | EStruct _ | EStructAccess _ | EMatch _ ),
_ ) as e ->
Expr.map ~f:translate_expr ~typ:translate_typ e
| _ -> .

121
compiler/lcalc/to_ocaml.ml
View File

@ -19,6 +19,24 @@ open Shared_ast
open Ast
module D = Dcalc.Ast
let format_string_list (fmt : Format.formatter) (uids : string list) : unit =
let sanitize_quotes = Re.compile (Re.char '"') in
Format.fprintf fmt "@[<hov 2>[%a]@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ";@ ")
(fun fmt info ->
Format.fprintf fmt "\"%s\""
(Re.replace sanitize_quotes ~f:(fun _ -> "\\\"") info)))
uids
let format_pos ppf pos =
Format.fprintf ppf
"@[<hov 1>{filename=%S;@ start_line=%d; start_column=%d;@ end_line=%d; \
end_column=%d;@ law_headings=%a}@]"
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos)
let format_lit (fmt : Format.formatter) (l : lit Mark.pos) : unit =
match Mark.remove l with
| LBool b -> Print.lit fmt (LBool b)
@ -47,16 +65,6 @@ let format_uid_list (fmt : Format.formatter) (uids : Uid.MarkedString.info list)
Format.fprintf fmt "\"%a\"" Uid.MarkedString.format info))
uids
let format_string_list (fmt : Format.formatter) (uids : string list) : unit =
let sanitize_quotes = Re.compile (Re.char '"') in
Format.fprintf fmt "@[<hov 2>[%a]@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ";@ ")
(fun fmt info ->
Format.fprintf fmt "\"%s\""
(Re.replace sanitize_quotes ~f:(fun _ -> "\\\"") info)))
uids
(* list taken from
http://caml.inria.fr/pub/docs/manual-ocaml/lex.html#sss:keywords *)
let ocaml_keywords =
@ -258,28 +266,6 @@ let needs_parens (e : 'm expr) : bool =
false
| _ -> true
let format_exception (fmt : Format.formatter) (exc : except Mark.pos) : unit =
match Mark.remove exc with
| ConflictError _ ->
let pos = Mark.get exc in
Format.fprintf fmt
"(ConflictError@ @[<hov 2>{filename = \"%s\";@\n\
start_line=%d;@ start_column=%d;@ end_line=%d; end_column=%d;@ \
law_headings=%a}@])"
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos)
| EmptyError -> Format.fprintf fmt "EmptyError"
| Crash s -> Format.fprintf fmt "(Crash %S)" s
| NoValueProvided ->
let pos = Mark.get exc in
Format.fprintf fmt
"(NoValueProvided@ @[<hov 2>{filename = \"%s\";@ start_line=%d;@ \
start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@])"
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos)
let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
unit =
let format_expr = format_expr ctx in
@ -388,14 +374,14 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
xs_tau format_expr body
| EApp
{
f = EAppOp { op = Log (BeginCall, info); args = [f]; _ }, _;
f = EAppOp { op = Log (BeginCall, info), _; args = [f]; _ }, _;
args = [arg];
_;
}
when Global.options.trace ->
Format.fprintf fmt "(log_begin_call@ %a@ %a)@ %a" format_uid_list info
format_with_parens f format_with_parens arg
| EAppOp { op = Log (VarDef var_def_info, info); args = [arg1]; _ }
| EAppOp { op = Log (VarDef var_def_info, info), _; args = [arg1]; _ }
when Global.options.trace ->
Format.fprintf fmt
"(log_variable_definition@ %a@ {io_input=%s;@ io_output=%b}@ (%a)@ %a)"
@ -407,7 +393,7 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
var_def_info.log_io_output typ_embedding_name
(var_def_info.log_typ, Pos.no_pos)
format_with_parens arg1
| EAppOp { op = Log (PosRecordIfTrueBool, _); args = [arg1]; _ }
| EAppOp { op = Log (PosRecordIfTrueBool, _), _; args = [arg1]; _ }
when Global.options.trace ->
let pos = Expr.pos e in
Format.fprintf fmt
@ -416,24 +402,26 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos) format_with_parens arg1
| EAppOp { op = Log (EndCall, info); args = [arg1]; _ }
| EAppOp { op = Log (EndCall, info), _; args = [arg1]; _ }
when Global.options.trace ->
Format.fprintf fmt "(log_end_call@ %a@ %a)" format_uid_list info
format_with_parens arg1
| EAppOp { op = Log _; args = [arg1]; _ } ->
| EAppOp { op = Log _, _; args = [arg1]; _ } ->
Format.fprintf fmt "%a" format_with_parens arg1
| EAppOp { op = (HandleDefault | HandleDefaultOpt) as op; args; _ } ->
let pos = Expr.pos e in
Format.fprintf fmt
"@[<hov 2>%s@ @[<hov 2>{filename = \"%s\";@ start_line=%d;@ \
start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@]@ %a@]"
| EAppOp
{
op = ((HandleDefault | HandleDefaultOpt) as op), _;
args = (EArray excs, _) :: _ as args;
_;
} ->
let pos = List.map Expr.pos excs in
Format.fprintf fmt "@[<hov 2>%s@ [|%a|]@ %a@]"
(Print.operator_to_string op)
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos)
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
format_with_parens)
~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ")
format_pos)
pos
(Format.pp_print_list ~pp_sep:Format.pp_print_space format_with_parens)
args
| EApp { f; args; _ } ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_with_parens f
@ -445,32 +433,33 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
Format.fprintf fmt
"@[<hov 2> if@ @[<hov 2>%a@]@ then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@]"
format_with_parens cond format_with_parens etrue format_with_parens efalse
| EAppOp { op; args; _ } ->
Format.fprintf fmt "@[<hov 2>%s@ %a@]" (Operator.name op)
| EAppOp { op = op, pos; args; _ } ->
Format.fprintf fmt "@[<hov 2>%s@ %t%a@]" (Operator.name op)
(fun ppf ->
match op with
| Map2 | Lt_dur_dur | Lte_dur_dur | Gt_dur_dur | Gte_dur_dur
| Eq_dur_dur ->
Format.fprintf ppf "%a@ " format_pos pos
| Div_int_int | Div_rat_rat | Div_mon_mon | Div_mon_rat | Div_dur_dur ->
Format.fprintf ppf "%a@ " format_pos (Expr.pos (List.nth args 1))
| _ -> ())
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
format_with_parens)
args
| EAssert e' ->
Format.fprintf fmt
"@[<hov 2>if@ %a@ then@ ()@ else@ raise (AssertionFailed @[<hov \
2>{filename = \"%s\";@ start_line=%d;@ start_column=%d;@ end_line=%d; \
end_column=%d;@ law_headings=%a}@])@]"
"@[<hov 2>if@ %a@ then@ ()@ else@ raise (Error (%s, [%a]))@]"
format_with_parens e'
(Pos.get_file (Expr.pos e'))
(Pos.get_start_line (Expr.pos e'))
(Pos.get_start_column (Expr.pos e'))
(Pos.get_end_line (Expr.pos e'))
(Pos.get_end_column (Expr.pos e'))
format_string_list
(Pos.get_law_info (Expr.pos e'))
| ERaise exc ->
Format.fprintf fmt "raise@ %a" format_exception (exc, Expr.pos e)
| ECatch { body; exn; handler } ->
Format.fprintf fmt "@[<hv>@[<hov 2>try@ %a@]@ with@]@ @[<hov 2>%a@ ->@ %a@]"
format_with_parens body format_exception
(exn, Expr.pos e)
format_with_parens handler
Runtime.(error_to_string AssertionFailed)
format_pos (Expr.pos e')
| EFatalError er ->
Format.fprintf fmt "raise@ (Runtime_ocaml.Runtime.Error (%a, [%a]))"
Print.runtime_error er format_pos (Expr.pos e)
| ERaiseEmpty -> Format.fprintf fmt "raise Empty"
| ECatchEmpty { body; handler } ->
Format.fprintf fmt "@[<hv>@[<hov 2>try@ %a@]@ with Empty ->@]@ @[%a@]"
format_with_parens body format_with_parens handler
| _ -> .
let format_struct_embedding

81
compiler/plugins/explain.ml
View File

@ -126,26 +126,44 @@ let neg_op = function
| Op.Gte_dur_dur -> Some Op.Lt_dur_dur
| _ -> None
let rec bool_negation e =
let rec bool_negation pos e =
match Expr.skip_wrappers e with
| ELit (LBool true), m -> ELit (LBool false), m
| ELit (LBool false), m -> ELit (LBool true), m
| EAppOp { op = Op.Not; args = [(e, _)] }, m -> e, m
| (EAppOp { op; tys; args = [e1; e2] }, m) as e -> (
| EAppOp { op = Op.Not, _; args = [(e, _)] }, m -> e, m
| (EAppOp { op = op, opos; tys; args = [e1; e2] }, m) as e -> (
match op with
| Op.And ->
EAppOp { op = Op.Or; tys; args = [bool_negation e1; bool_negation e2] }, m
( EAppOp
{
op = Op.Or, opos;
tys;
args = [bool_negation pos e1; bool_negation pos e2];
},
m )
| Op.Or ->
( EAppOp { op = Op.And; tys; args = [bool_negation e1; bool_negation e2] },
( EAppOp
{
op = Op.And, opos;
tys;
args = [bool_negation pos e1; bool_negation pos e2];
},
m )
| op -> (
match neg_op op with
| Some op -> EAppOp { op; tys; args = [e1; e2] }, m
| Some op -> EAppOp { op = op, opos; tys; args = [e1; e2] }, m
| None ->
( EAppOp { op = Op.Not; tys = [TLit TBool, Expr.mark_pos m]; args = [e] },
( EAppOp
{
op = Op.Not, opos;
tys = [TLit TBool, Expr.mark_pos m];
args = [e];
},
m )))
| (_, m) as e ->
EAppOp { op = Op.Not; tys = [TLit TBool, Expr.mark_pos m]; args = [e] }, m
( EAppOp
{ op = Op.Not, pos; tys = [TLit TBool, Expr.mark_pos m]; args = [e] },
m )
let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
=
@ -169,7 +187,7 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
let r, env1 = lazy_eval ctx env1 llevel e in
env_elt.reduced <- r, env1;
r, Env.join env env1
| EAppOp { op; args; tys }, m -> (
| EAppOp { op = op, opos; args; tys }, m -> (
if
(not llevel.eval_default)
&& not (List.equal Expr.equal args [ELit LUnit, m])
@ -192,11 +210,13 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
let pos = Expr.mark_pos m in
( EAppOp
{
op = Op.Eq_int_int;
op = Op.Eq_int_int, opos;
tys = [TLit TInt, pos; TLit TInt, pos];
args =
[
EAppOp { op = Op.Length; tys = [aty]; args = [arr] }, m;
( EAppOp
{ op = Op.Length, opos; tys = [aty]; args = [arr] },
m );
ELit (LInt (Runtime.integer_of_int 0)), m;
];
},
@ -245,7 +265,7 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
(* We did a transformation (removing the outer operator), but further
evaluation may be needed to guarantee that [llevel] is reached *)
lazy_eval ctx env { llevel with eval_match = true } e
| _ -> (EAppOp { op; args; tys }, m), env)
| _ -> (EAppOp { op = op, opos; args; tys }, m), env)
| _ ->
let env, args =
List.fold_left_map
@ -254,7 +274,7 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
env, e)
env args
in
if not llevel.eval_op then (EAppOp { op; args; tys }, m), env
if not llevel.eval_op then (EAppOp { op = op, opos; args; tys }, m), env
else
let renv = ref env in
(* Dirty workaround returning env and conds from evaluate_operator *)
@ -264,7 +284,7 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
e
in
let e =
Interpreter.evaluate_operator eval op m Global.En
Interpreter.evaluate_operator eval (op, opos) m Global.En
(* Default language to English but this should not raise any error
messages so we don't care. *)
args
@ -294,7 +314,7 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
log "@]}";
e, env
| e, _ -> error e "Invalid apply on %a" Expr.format e)
| (EAbs _ | ELit _ | EEmptyError), _ -> e0, env (* these are values *)
| (EAbs _ | ELit _ | EEmpty), _ -> e0, env (* these are values *)
| (EStruct _ | ETuple _ | EInj _ | EArray _), _ ->
if not llevel.eval_struct then e0, env
else
@ -348,7 +368,7 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
List.filter_map
(fun e ->
match eval_to_value env e ~eval_default:false with
| (EEmptyError, _), _ -> None
| (EEmpty, _), _ -> None
| e -> Some e)
excepts
in
@ -359,7 +379,7 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
let condition = just, env in
let e, env = lazy_eval ctx env llevel cons in
add_condition ~condition e, env
| (ELit (LBool false), _), _ -> (EEmptyError, m), env
| (ELit (LBool false), _), _ -> (EEmpty, m), env
(* Note: conditions for empty are skipped *)
| e, _ -> error e "Invalid exception justification %a" Expr.format e)
| [(e, env)] ->
@ -370,14 +390,14 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
~extra_pos:(List.map (fun (e, _) -> "", Expr.pos e) excs)
"Conflicting exceptions")
| EPureDefault e, _ -> lazy_eval ctx env llevel e
| EIfThenElse { cond; etrue; efalse }, _ -> (
| EIfThenElse { cond; etrue; efalse }, m -> (
match eval_to_value env cond with
| (ELit (LBool true), _), _ ->
let condition = cond, env in
let e, env = lazy_eval ctx env llevel etrue in
add_condition ~condition e, env
| (ELit (LBool false), m), _ -> (
let condition = bool_negation cond, env in
let condition = bool_negation (Expr.mark_pos m) cond, env in
let e, env = lazy_eval ctx env llevel efalse in
match efalse with
(* The negated condition is not added for nested [else if] to reduce
@ -387,7 +407,7 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
| e, _ -> error e "Invalid condition %a" Expr.format e)
| EErrorOnEmpty e, _ -> (
match eval_to_value env e ~eval_default:false with
| ((EEmptyError, _) as e'), _ ->
| ((EEmpty, _) as e'), _ ->
(* This does _not_ match the eager semantics ! *)
error e' "This value is undefined %a" Expr.format e
| e, env -> lazy_eval ctx env llevel e)
@ -400,6 +420,8 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
error e "Assert failure (%a)" Expr.format e error e
"Assert failure (%a)" Expr.format e
| _ -> error e "Invalid assertion condition %a" Expr.format e)
| EFatalError err, _ ->
error e0 "%a" Format.pp_print_text (Runtime.error_message err)
| EExternal _, _ -> assert false (* todo *)
| _ -> .
@ -539,7 +561,8 @@ let to_graph ctx env expr =
let rec aux env g e =
(* lazy_eval ctx env (result_level base_vars) e *)
match Expr.skip_wrappers e with
| EAppOp { op = ToRat_int | ToRat_mon | ToMoney_rat; args = [arg]; _ }, _ ->
| ( EAppOp { op = (ToRat_int | ToRat_mon | ToMoney_rat), _; args = [arg]; _ },
_ ) ->
aux env g arg
(* we skip conversions *)
| ELit l, _ ->
@ -657,8 +680,9 @@ let program_to_graph
in
let e = Mark.set m (Expr.skip_wrappers e) in
match e with
| EAppOp { op = ToRat_int | ToRat_mon | ToMoney_rat; args = [arg]; tys }, _
->
| ( EAppOp
{ op = (ToRat_int | ToRat_mon | ToMoney_rat), _; args = [arg]; tys },
_ ) ->
aux parent (g, var_vertices, env0) (Mark.set m arg)
(* we skip conversions *)
| ELit l, _ ->
@ -696,7 +720,8 @@ let program_to_graph
let v = G.V.create e in
let g = G.add_vertex g v in
(g, var_vertices, env), v))
| EAppOp { op = Map | Filter | Reduce | Fold; args = _ :: args; _ }, _ ->
| EAppOp { op = (Map | Filter | Reduce | Fold), _; args = _ :: args; _ }, _
->
(* First argument (which is a function) is ignored *)
let v = G.V.create e in
let g = G.add_vertex g v in
@ -705,7 +730,7 @@ let program_to_graph
in
( (List.fold_left (fun g -> G.add_edge g v) g children, var_vertices, env),
v )
| EAppOp { op; args = [lhs; rhs]; _ }, _ ->
| EAppOp { op = op, _; args = [lhs; rhs]; _ }, _ ->
let v = G.V.create e in
let g = G.add_vertex g v in
let (g, var_vertices, env), lhs =
@ -1072,8 +1097,8 @@ let expr_to_dot_label0 :
let bypass : type a t. Format.formatter -> (a, t) gexpr -> bool =
fun ppf e ->
match Mark.remove e with
| ELit _ | EArray _ | ETuple _ | EStruct _ | EInj _ | EEmptyError
| EAbs _ | EExternal _ ->
| ELit _ | EArray _ | ETuple _ | EStruct _ | EInj _ | EEmpty | EAbs _
| EExternal _ ->
aux_value ppf e;
true
| EMatch { e; cases; _ } ->
@ -1219,7 +1244,7 @@ let to_dot lang ppf ctx env base_vars g ~base_src_url =
else (* Constants *)
[`Style `Filled; `Fillcolor 0x77aaff; `Shape `Note]
| EStruct _, _ | EArray _, _ -> [`Shape `Record]
| EAppOp { op; _ }, _ -> (
| EAppOp { op = op, _; _ }, _ -> (
match op_kind op with
| `Sum | `Product | _ -> [`Shape `Box] (* | _ -> [] *))
| _ -> [])

12
compiler/plugins/lazy_interp.ml
View File

@ -142,7 +142,7 @@ let rec lazy_eval :
log "@]}";
e, env
| e, _ -> error e "Invalid apply on %a" Expr.format e)
| (EAbs _ | ELit _ | EEmptyError), _ -> e0, env (* these are values *)
| (EAbs _ | ELit _ | EEmpty), _ -> e0, env (* these are values *)
| (EStruct _ | ETuple _ | EInj _ | EArray _), _ ->
if not llevel.eval_struct then e0, env
else
@ -183,7 +183,7 @@ let rec lazy_eval :
List.filter_map
(fun e ->
match eval_to_value env e ~eval_default:false with
| (EEmptyError, _), _ -> None
| (EEmpty, _), _ -> None
| e -> Some e)
excepts
in
@ -191,7 +191,7 @@ let rec lazy_eval :
| [] -> (
match eval_to_value env just with
| (ELit (LBool true), _), _ -> lazy_eval ctx env llevel cons
| (ELit (LBool false), _), _ -> (EEmptyError, m), env
| (ELit (LBool false), _), _ -> (EEmpty, m), env
| e, _ -> error e "Invalid exception justification %a" Expr.format e)
| [(e, env)] ->
log "@[<hov 5>EVAL %a@]" Expr.format e;
@ -208,7 +208,7 @@ let rec lazy_eval :
| e, _ -> error e "Invalid condition %a" Expr.format e)
| EErrorOnEmpty e, _ -> (
match eval_to_value env e ~eval_default:false with
| ((EEmptyError, _) as e'), _ ->
| ((EEmpty, _) as e'), _ ->
(* This does _not_ match the eager semantics ! *)
error e' "This value is undefined %a" Expr.format e
| e, env -> lazy_eval ctx env llevel e)
@ -220,6 +220,8 @@ let rec lazy_eval :
| (ELit (LBool false), _), _ ->
error e "Assert failure (%a)" Expr.format e
| _ -> error e "Invalid assertion condition %a" Expr.format e)
| EFatalError err, m ->
error e0 "%a" Format.pp_print_text (Runtime.error_message err)
| EExternal _, _ -> assert false (* todo *)
| _ -> .
@ -251,7 +253,7 @@ let interpret_program (prg : ('dcalc, 'm) gexpr program) (scope : ScopeName.t) :
| TArrow (ty_in, ty_out), _ ->
Expr.make_abs
[| Var.make "_" |]
(Bindlib.box EEmptyError, Expr.with_ty m ty_out)
(Bindlib.box EEmpty, Expr.with_ty m ty_out)
ty_in (Expr.mark_pos m)
| ty -> Expr.evar (Var.make "undefined_input") (Expr.with_ty m ty))
(StructName.Map.find scope_arg_struct ctx.ctx_structs))

7
compiler/scalc/ast.ml
View File

@ -61,7 +61,7 @@ and naked_expr =
| EArray of expr list
| ELit of lit
| EApp of { f : expr; args : expr list }
| EAppOp of { op : operator; args : expr list }
| EAppOp of { op : operator Mark.pos; args : expr list }
| EExternal of { modname : VarName.t Mark.pos; name : string Mark.pos }
type stmt =
@ -69,8 +69,9 @@ type stmt =
| SLocalDecl of { name : VarName.t Mark.pos; typ : typ }
| SLocalInit of { name : VarName.t Mark.pos; typ : typ; expr : expr }
| SLocalDef of { name : VarName.t Mark.pos; expr : expr; typ : typ }
| STryExcept of { try_block : block; except : except; with_block : block }
| SRaise of except
| STryWEmpty of { try_block : block; with_block : block }
| SRaiseEmpty
| SFatalError of Runtime.error
| SIfThenElse of { if_expr : expr; then_block : block; else_block : block }
| SSwitch of {
switch_expr : expr;

19
compiler/scalc/from_lcalc.ml
View File

@ -140,7 +140,7 @@ and translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : RevBlock.t * A.expr =
e1_stmts, (A.ETupleAccess { e1 = new_e1; index }, Expr.pos expr)
| EAppOp
{
op = Op.HandleDefaultOpt;
op = Op.HandleDefaultOpt, _;
args = [_exceptions; _just; _cons];
tys = _;
}
@ -227,7 +227,8 @@ and translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : RevBlock.t * A.expr =
Expr.pos expr )
in
RevBlock.empty, (EExternal { modname; name }, Expr.pos expr)
| ECatch _ | EAbs _ | EIfThenElse _ | EMatch _ | EAssert _ | ERaise _ ->
| ECatchEmpty _ | EAbs _ | EIfThenElse _ | EMatch _ | EAssert _
| EFatalError _ | ERaiseEmpty ->
raise (NotAnExpr { needs_a_local_decl = true })
| _ -> .
with NotAnExpr { needs_a_local_decl } ->
@ -272,8 +273,9 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
RevBlock.rebuild
~tail:[A.SAssert (Mark.remove new_e), Expr.pos block_expr]
e_stmts
| EFatalError err -> [SFatalError err, Expr.pos block_expr]
| EAppOp
{ op = Op.HandleDefaultOpt; tys = _; args = [exceptions; just; cons] }
{ op = Op.HandleDefaultOpt, _; tys = _; args = [exceptions; just; cons] }
when ctxt.config.keep_special_ops ->
let exceptions =
match Mark.remove exceptions with
@ -481,15 +483,14 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
},
Expr.pos block_expr );
]
| ECatch { body; exn; handler } ->
| ECatchEmpty { body; handler } ->
let s_e_try = translate_statements ctxt body in
let s_e_catch = translate_statements ctxt handler in
[
( A.STryExcept
{ try_block = s_e_try; except = exn; with_block = s_e_catch },
( A.STryWEmpty { try_block = s_e_try; with_block = s_e_catch },
Expr.pos block_expr );
]
| ERaise except ->
| ERaiseEmpty ->
(* Before raising the exception, we still give a dummy definition to the
current variable so that tools like mypy don't complain. *)
(match ctxt.inside_definition_of with
@ -504,7 +505,7 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
Expr.pos block_expr );
]
| _ -> [])
@ [A.SRaise except, Expr.pos block_expr]
@ [A.SRaiseEmpty, Expr.pos block_expr]
| EInj { e = e1; cons; name } when ctxt.config.no_struct_literals ->
let e1_stmts, new_e1 = translate_expr ctxt e1 in
let tmp_struct_var_name =
@ -572,7 +573,7 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
let e_stmts, new_e = translate_expr ctxt block_expr in
let tail =
match (e_stmts :> (A.stmt * Pos.t) list) with
| (A.SRaise _, _) :: _ ->
| (A.SRaiseEmpty, _) :: _ ->
(* if the last statement raises an exception, then we don't need to
return or to define the current variable since this code will be
unreachable *)

23
compiler/scalc/print.ml
View File

@ -74,15 +74,15 @@ let rec format_expr
Format.fprintf fmt "@[<hov 2>%a@ %a@]" EnumConstructor.format cons
format_expr e
| ELit l -> Print.lit fmt l
| EAppOp { op = (Map | Filter) as op; args = [arg1; arg2] } ->
| EAppOp { op = ((Map | Filter) as op), _; args = [arg1; arg2] } ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" (Print.operator ~debug) op
format_with_parens arg1 format_with_parens arg2
| EAppOp { op; args = [arg1; arg2] } ->
| EAppOp { op = op, _; args = [arg1; arg2] } ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1
(Print.operator ~debug) op format_with_parens arg2
| EAppOp { op = Log _; args = [arg1] } when not debug ->
| EAppOp { op = Log _, _; args = [arg1] } when not debug ->
Format.fprintf fmt "%a" format_with_parens arg1
| EAppOp { op; args = [arg1] } ->
| EAppOp { op = op, _; args = [arg1] } ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" (Print.operator ~debug) op
format_with_parens arg1
| EApp { f; args = [] } ->
@ -93,7 +93,7 @@ let rec format_expr
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
format_with_parens)
args
| EAppOp { op; args } ->
| EAppOp { op = op, _; args } ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" (Print.operator ~debug) op
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
@ -137,16 +137,19 @@ let rec format_statement
Print.punctuation "="
(format_expr decl_ctx ~debug)
naked_expr
| STryExcept { try_block = b_try; except; with_block = b_with } ->
| STryWEmpty { try_block = b_try; with_block = b_with } ->
Format.fprintf fmt "@[<v 2>%a%a@ %a@]@\n@[<v 2>%a %a%a@ %a@]" Print.keyword
"try" Print.punctuation ":"
(format_block decl_ctx ~debug)
b_try Print.keyword "with" Print.except except Print.punctuation ":"
b_try Print.keyword "with" Print.op_style "Empty" Print.punctuation ":"
(format_block decl_ctx ~debug)
b_with
| SRaise except ->
Format.fprintf fmt "@[<hov 2>%a %a@]" Print.keyword "raise" Print.except
except
| SRaiseEmpty ->
Format.fprintf fmt "@[<hov 2>%a %a@]" Print.keyword "raise" Print.op_style
"Empty"
| SFatalError err ->
Format.fprintf fmt "@[<hov 2>%a %a@]" Print.keyword "fatal"
Print.runtime_error err
| SIfThenElse { if_expr = e_if; then_block = b_true; else_block = b_false } ->
Format.fprintf fmt "@[<v 2>%a @[<hov 2>%a@]%a@ %a@ @]@[<v 2>%a%a@ %a@]"
Print.keyword "if"

43
compiler/scalc/to_c.ml
View File

@ -350,26 +350,23 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) :
failwith
"should not happen, array initialization is caught at the statement level"
| ELit l -> Format.fprintf fmt "%a" format_lit (Mark.copy e l)
| EAppOp { op = (Map | Filter) as op; args = [arg1; arg2] } ->
Format.fprintf fmt "%a(%a,@ %a)" format_op (op, Pos.no_pos)
(format_expression ctx) arg1 (format_expression ctx) arg2
| EAppOp { op = ((Map | Filter), _) as op; args = [arg1; arg2] } ->
Format.fprintf fmt "%a(%a,@ %a)" format_op op (format_expression ctx) arg1
(format_expression ctx) arg2
| EAppOp { op; args = [arg1; arg2] } ->
Format.fprintf fmt "(%a %a@ %a)" (format_expression ctx) arg1 format_op
(op, Pos.no_pos) (format_expression ctx) arg2
| EAppOp { op = Not; args = [arg1] } ->
Format.fprintf fmt "%a %a" format_op (Not, Pos.no_pos)
(format_expression ctx) arg1
Format.fprintf fmt "(%a %a@ %a)" (format_expression ctx) arg1 format_op op
(format_expression ctx) arg2
| EAppOp { op = (Not, _) as op; args = [arg1] } ->
Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1
| EAppOp
{
op = (Minus_int | Minus_rat | Minus_mon | Minus_dur) as op;
op = ((Minus_int | Minus_rat | Minus_mon | Minus_dur), _) as op;
args = [arg1];
} ->
Format.fprintf fmt "%a %a" format_op (op, Pos.no_pos)
(format_expression ctx) arg1
Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1
| EAppOp { op; args = [arg1] } ->
Format.fprintf fmt "%a(%a)" format_op (op, Pos.no_pos)
(format_expression ctx) arg1
| EAppOp { op = HandleDefaultOpt | HandleDefault; args = _ } ->
Format.fprintf fmt "%a(%a)" format_op op (format_expression ctx) arg1
| EAppOp { op = (HandleDefaultOpt | HandleDefault), _; args = _ } ->
failwith "should not happen because of keep_special_ops"
| EApp { f; args } ->
Format.fprintf fmt "%a(@[<hov 0>%a)@]" (format_expression ctx) f
@ -378,7 +375,7 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) :
(format_expression ctx))
args
| EAppOp { op; args } ->
Format.fprintf fmt "%a(@[<hov 0>%a)@]" format_op (op, Pos.no_pos)
Format.fprintf fmt "%a(@[<hov 0>%a)@]" format_op op
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(format_expression ctx))
@ -402,8 +399,8 @@ let rec format_statement
(s : stmt Mark.pos) : unit =
match Mark.remove s with
| SInnerFuncDef _ ->
Message.error ~pos:(Mark.get s)
"Internal error: this inner functions should have been hoisted in Scalc"
Message.error ~pos:(Mark.get s) ~internal:true
"This inner functions should have been hoisted in Scalc"
| SLocalDecl { name = v; typ = ty } ->
Format.fprintf fmt "@[<hov 2>%a@];"
(format_typ ctx (fun fmt -> format_var fmt (Mark.remove v)))
@ -440,22 +437,18 @@ let rec format_statement
| SLocalDef { name = v; expr = e; _ } ->
Format.fprintf fmt "@[<hov 2>%a = %a;@]" format_var (Mark.remove v)
(format_expression ctx) e
| STryExcept _ -> failwith "should not happen"
| SRaise e ->
| SRaiseEmpty | STryWEmpty _ -> assert false
| SFatalError err ->
let pos = Mark.get s in
Format.fprintf fmt
"catala_fatal_error_raised.code = %s;@,\
"catala_fatal_error_raised.code = catala_%s;@,\
catala_fatal_error_raised.position.filename = \"%s\";@,\
catala_fatal_error_raised.position.start_line = %d;@,\
catala_fatal_error_raised.position.start_column = %d;@,\
catala_fatal_error_raised.position.end_line = %d;@,\
catala_fatal_error_raised.position.end_column = %d;@,\
longjmp(catala_fatal_error_jump_buffer, 0);"
(match e with
| ConflictError _ -> "catala_conflict"
| EmptyError -> "catala_empty"
| NoValueProvided -> "catala_no_value_provided"
| Crash _ -> "catala_crash")
(String.to_snake_case (Runtime.error_to_string err))
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos)
| SIfThenElse { if_expr = cond; then_block = b1; else_block = b2 } ->

92
compiler/scalc/to_python.ml
View File

@ -247,27 +247,20 @@ let format_func_name (fmt : Format.formatter) (v : FuncName.t) : unit =
let v_str = Mark.remove (FuncName.get_info v) in
format_name_cleaned fmt v_str
let format_exception (fmt : Format.formatter) (exc : except Mark.pos) : unit =
let pos = Mark.get exc in
match Mark.remove exc with
| ConflictError _ ->
Format.fprintf fmt
"ConflictError(@[<hov 0>SourcePosition(@[<hov 0>filename=\"%s\",@ \
start_line=%d,@ start_column=%d,@ end_line=%d,@ end_column=%d,@ \
law_headings=%a)@])@]"
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos)
| EmptyError -> Format.fprintf fmt "EmptyError"
| Crash _ -> Format.fprintf fmt "Crash"
| NoValueProvided ->
Format.fprintf fmt
"NoValueProvided(@[<hov 0>SourcePosition(@[<hov 0>filename=\"%s\",@ \
start_line=%d,@ start_column=%d,@ end_line=%d,@ end_column=%d,@ \
law_headings=%a)@])@]"
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos)
let format_position ppf pos =
Format.fprintf ppf
"@[<hov 4>SourcePosition(@,\
filename=\"%s\",@ start_line=%d, start_column=%d,@ end_line=%d, \
end_column=%d,@ law_headings=%a@;\
<0 -4>)@]" (Pos.get_file pos) (Pos.get_start_line pos)
(Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)
format_string_list (Pos.get_law_info pos)
let format_error (ppf : Format.formatter) (err : Runtime.error Mark.pos) : unit
=
let pos = Mark.get err in
let tag = Runtime.error_to_string (Mark.remove err) in
Format.fprintf ppf "%s(%a)" tag format_position pos
let rec format_expression ctx (fmt : Format.formatter) (e : expr) : unit =
match Mark.remove e with
@ -305,18 +298,21 @@ let rec format_expression ctx (fmt : Format.formatter) (e : expr) : unit =
(fun fmt e -> Format.fprintf fmt "%a" (format_expression ctx) e))
es
| ELit l -> Format.fprintf fmt "%a" format_lit (Mark.copy e l)
| EAppOp { op = (Map | Filter) as op; args = [arg1; arg2] } ->
Format.fprintf fmt "%a(%a,@ %a)" format_op (op, Pos.no_pos)
(format_expression ctx) arg1 (format_expression ctx) arg2
| EAppOp { op = ((Map | Filter), _) as op; args = [arg1; arg2] } ->
Format.fprintf fmt "%a(%a,@ %a)" format_op op (format_expression ctx) arg1
(format_expression ctx) arg2
| EAppOp { op; args = [arg1; arg2] } ->
Format.fprintf fmt "(%a %a@ %a)" (format_expression ctx) arg1 format_op
(op, Pos.no_pos) (format_expression ctx) arg2
Format.fprintf fmt "(%a %a@ %a)" (format_expression ctx) arg1 format_op op
(format_expression ctx) arg2
| EApp
{ f = EAppOp { op = Log (BeginCall, info); args = [f] }, _; args = [arg] }
{
f = EAppOp { op = Log (BeginCall, info), _; args = [f] }, _;
args = [arg];
}
when Global.options.trace ->
Format.fprintf fmt "log_begin_call(%a,@ %a,@ %a)" format_uid_list info
(format_expression ctx) f (format_expression ctx) arg
| EAppOp { op = Log (VarDef var_def_info, info); args = [arg1] }
| EAppOp { op = Log (VarDef var_def_info, info), _; args = [arg1] }
when Global.options.trace ->
Format.fprintf fmt
"log_variable_definition(%a,@ LogIO(input_io=InputIO.%s,@ \
@ -328,7 +324,7 @@ let rec format_expression ctx (fmt : Format.formatter) (e : expr) : unit =
| Runtime.Reentrant -> "Reentrant")
(if var_def_info.log_io_output then "True" else "False")
(format_expression ctx) arg1
| EAppOp { op = Log (PosRecordIfTrueBool, _); args = [arg1] }
| EAppOp { op = Log (PosRecordIfTrueBool, _), _; args = [arg1] }
when Global.options.trace ->
let pos = Mark.get e in
Format.fprintf fmt
@ -337,31 +333,28 @@ let rec format_expression ctx (fmt : Format.formatter) (e : expr) : unit =
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos) (format_expression ctx) arg1
| EAppOp { op = Log (EndCall, info); args = [arg1] } when Global.options.trace
->
| EAppOp { op = Log (EndCall, info), _; args = [arg1] }
when Global.options.trace ->
Format.fprintf fmt "log_end_call(%a,@ %a)" format_uid_list info
(format_expression ctx) arg1
| EAppOp { op = Log _; args = [arg1] } ->
| EAppOp { op = Log _, _; args = [arg1] } ->
Format.fprintf fmt "%a" (format_expression ctx) arg1
| EAppOp { op = Not; args = [arg1] } ->
Format.fprintf fmt "%a %a" format_op (Not, Pos.no_pos)
(format_expression ctx) arg1
| EAppOp { op = (Not, _) as op; args = [arg1] } ->
Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1
| EAppOp
{
op = (Minus_int | Minus_rat | Minus_mon | Minus_dur) as op;
op = ((Minus_int | Minus_rat | Minus_mon | Minus_dur), _) as op;
args = [arg1];
} ->
Format.fprintf fmt "%a %a" format_op (op, Pos.no_pos)
(format_expression ctx) arg1
Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1
| EAppOp { op; args = [arg1] } ->
Format.fprintf fmt "%a(%a)" format_op (op, Pos.no_pos)
(format_expression ctx) arg1
| EAppOp { op = (HandleDefault | HandleDefaultOpt) as op; args } ->
Format.fprintf fmt "%a(%a)" format_op op (format_expression ctx) arg1
| EAppOp { op = ((HandleDefault | HandleDefaultOpt), _) as op; args } ->
let pos = Mark.get e in
Format.fprintf fmt
"%a(@[<hov 0>SourcePosition(filename=\"%s\",@ start_line=%d,@ \
start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)@]"
format_op (op, pos) (Pos.get_file pos) (Pos.get_start_line pos)
format_op op (Pos.get_file pos) (Pos.get_start_line pos)
(Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)
format_string_list (Pos.get_law_info pos)
(Format.pp_print_list
@ -388,7 +381,7 @@ let rec format_expression ctx (fmt : Format.formatter) (e : expr) : unit =
(format_expression ctx))
args
| EAppOp { op; args } ->
Format.fprintf fmt "%a(@[<hov 0>%a)@]" format_op (op, Pos.no_pos)
Format.fprintf fmt "%a(@[<hov 0>%a)@]" format_op op
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(format_expression ctx))
@ -423,13 +416,12 @@ let rec format_statement ctx (fmt : Format.formatter) (s : stmt Mark.pos) : unit
->
Format.fprintf fmt "@[<hov 4>%a = %a@]" format_var (Mark.remove v)
(format_expression ctx) e
| STryExcept { try_block = try_b; except; with_block = catch_b } ->
Format.fprintf fmt "@[<hov 4>try:@\n%a@]@\n@[<hov 4>except %a:@\n%a@]"
(format_block ctx) try_b format_exception (except, Pos.no_pos)
(format_block ctx) catch_b
| SRaise except ->
Format.fprintf fmt "@[<hov 4>raise %a@]" format_exception
(except, Mark.get s)
| STryWEmpty { try_block = try_b; with_block = catch_b } ->
Format.fprintf fmt "@[<v 4>try:@,%a@]@\n@[<v 4>except Empty:@,%a@]"
(format_block ctx) try_b (format_block ctx) catch_b
| SRaiseEmpty -> Format.fprintf fmt "raise Empty"
| SFatalError err ->
Format.fprintf fmt "@[<hov 4>raise %a@]" format_error (err, Mark.get s)
| SIfThenElse { if_expr = cond; then_block = b1; else_block = b2 } ->
Format.fprintf fmt "@[<hov 4>if %a:@\n%a@]@\n@[<hov 4>else:@\n%a@]"
(format_expression ctx) cond (format_block ctx) b1 (format_block ctx) b2

82
compiler/scalc/to_r.ml
View File

@ -253,34 +253,20 @@ let format_func_name (fmt : Format.formatter) (v : FuncName.t) : unit =
let v_str = Mark.remove (FuncName.get_info v) in
format_name_cleaned fmt v_str
let format_exception (fmt : Format.formatter) (exc : except Mark.pos) : unit =
let pos = Mark.get exc in
match Mark.remove exc with
| ConflictError _ ->
Format.fprintf fmt
"catala_conflict_error(@[<hov 0>catala_position(@[<hov \
0>filename=\"%s\",@ start_line=%d,@ start_column=%d,@ end_line=%d,@ \
end_column=%d,@ law_headings=%a)@])@]"
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos)
| EmptyError -> Format.fprintf fmt "catala_empty_error()"
| Crash _ -> Format.fprintf fmt "catala_crash()"
| NoValueProvided ->
Format.fprintf fmt
"catala_no_value_provided_error(@[<hov 0>catala_position(@[<hov \
0>filename=\"%s\",@ start_line=%d,@ start_column=%d,@ end_line=%d,@ \
end_column=%d,@ law_headings=%a)@])@]"
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos)
let format_position ppf pos =
Format.fprintf ppf
"@[<hov 2>catala_position(@,\
filename=\"%s\",@ start_line=%d, start_column=%d,@ end_line=%d, \
end_column=%d,@ law_headings=%a@;\
<0 -2>)@]" (Pos.get_file pos) (Pos.get_start_line pos)
(Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)
format_string_list (Pos.get_law_info pos)
let format_exception_name (fmt : Format.formatter) (exc : except) : unit =
match exc with
| ConflictError _ -> Format.fprintf fmt "catala_conflict_error"
| EmptyError -> Format.fprintf fmt "catala_empty_error"
| Crash _ -> Format.fprintf fmt "catala_crash"
| NoValueProvided -> Format.fprintf fmt "catala_no_value_provided_error"
let format_error (ppf : Format.formatter) (err : Runtime.error Mark.pos) : unit
=
let pos = Mark.get err in
let tag = String.to_snake_case (Runtime.error_to_string (Mark.remove err)) in
Format.fprintf ppf "%s(%a)" tag format_position pos
let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) :
unit =
@ -319,29 +305,26 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) :
(fun fmt e -> Format.fprintf fmt "%a" (format_expression ctx) e))
es
| ELit l -> Format.fprintf fmt "%a" format_lit (Mark.copy e l)
| EAppOp { op = (Map | Filter) as op; args = [arg1; arg2] } ->
Format.fprintf fmt "%a(%a,@ %a)" format_op (op, Pos.no_pos)
(format_expression ctx) arg1 (format_expression ctx) arg2
| EAppOp { op = ((Map | Filter), _) as op; args = [arg1; arg2] } ->
Format.fprintf fmt "%a(%a,@ %a)" format_op op (format_expression ctx) arg1
(format_expression ctx) arg2
| EAppOp { op; args = [arg1; arg2] } ->
Format.fprintf fmt "(%a %a@ %a)" (format_expression ctx) arg1 format_op
(op, Pos.no_pos) (format_expression ctx) arg2
| EAppOp { op = Not; args = [arg1] } ->
Format.fprintf fmt "%a %a" format_op (Not, Pos.no_pos)
(format_expression ctx) arg1
Format.fprintf fmt "(%a %a@ %a)" (format_expression ctx) arg1 format_op op
(format_expression ctx) arg2
| EAppOp { op = (Not, _) as op; args = [arg1] } ->
Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1
| EAppOp
{
op = (Minus_int | Minus_rat | Minus_mon | Minus_dur) as op;
op = ((Minus_int | Minus_rat | Minus_mon | Minus_dur), _) as op;
args = [arg1];
} ->
Format.fprintf fmt "%a %a" format_op (op, Pos.no_pos)
(format_expression ctx) arg1
Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1
| EAppOp { op; args = [arg1] } ->
Format.fprintf fmt "%a(%a)" format_op (op, Pos.no_pos)
(format_expression ctx) arg1
| EAppOp { op = HandleDefaultOpt; _ } ->
Format.fprintf fmt "%a(%a)" format_op op (format_expression ctx) arg1
| EAppOp { op = HandleDefaultOpt, _; _ } ->
Message.error ~internal:true
"R compilation does not currently support the avoiding of exceptions"
| EAppOp { op = HandleDefault as op; args; _ } ->
| EAppOp { op = (HandleDefault as op), _; args; _ } ->
let pos = Mark.get e in
Format.fprintf fmt
"%a(@[<hov 0>catala_position(filename=\"%s\",@ start_line=%d,@ \
@ -373,7 +356,7 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) :
(format_expression ctx))
args
| EAppOp { op; args } ->
Format.fprintf fmt "%a(@[<hov 0>%a)@]" format_op (op, Pos.no_pos)
Format.fprintf fmt "%a(@[<hov 0>%a)@]" format_op op
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(format_expression ctx))
@ -409,20 +392,19 @@ let rec format_statement
->
Format.fprintf fmt "@[<hov 2>%a <- %a@]" format_var (Mark.remove v)
(format_expression ctx) e
| STryExcept { try_block = try_b; except; with_block = catch_b } ->
| STryWEmpty { try_block = try_b; with_block = catch_b } ->
Format.fprintf fmt
(* TODO escape dummy__arg*)
"@[<hov 2>tryCatch(@[<hov 2>{@;\
%a@;\
}@],@;\
%a = function(dummy__arg) @[<hov 2>{@;\
catala_empty_error() = function(dummy__arg) @[<hov 2>{@;\
%a@;\
}@])@]"
(format_block ctx) try_b format_exception_name except (format_block ctx)
catch_b
| SRaise except ->
Format.fprintf fmt "@[<hov 2>stop(%a)@]" format_exception
(except, Mark.get s)
(format_block ctx) try_b (format_block ctx) catch_b
| SRaiseEmpty -> Format.pp_print_string fmt "stop(catala_empty_error())"
| SFatalError err ->
Format.fprintf fmt "@[<hov 2>stop(%a)@]" format_error (err, Mark.get s)
| SIfThenElse { if_expr = cond; then_block = b1; else_block = b2 } ->
Format.fprintf fmt
"@[<hov 2>if (%a) {@\n%a@]@\n@[<hov 2>} else {@\n%a@]@\n}"

22
compiler/scopelang/from_desugared.ml
View File

@ -39,7 +39,7 @@ let tag_with_log_entry
(markings : Uid.MarkedString.info list) : untyped Ast.expr boxed =
if Global.options.trace then
Expr.eappop
~op:(Log (l, markings))
~op:(Log (l, markings), Expr.pos e)
~tys:[TAny, Expr.pos e]
~args:[e] (Mark.get e)
else e
@ -200,15 +200,13 @@ let rec translate_expr (ctx : ctx) (e : D.expr) : untyped Ast.expr boxed =
~monomorphic:(fun op -> Expr.eappop ~op ~tys ~args m)
~polymorphic:(fun op -> Expr.eappop ~op ~tys ~args m)
~overloaded:(fun op ->
match
Operator.resolve_overload ctx.decl_ctx (Mark.add (Expr.pos e) op) tys
with
match Operator.resolve_overload ctx.decl_ctx op tys with
| op, `Straight -> Expr.eappop ~op ~tys ~args m
| op, `Reversed ->
Expr.eappop ~op ~tys:(List.rev tys) ~args:(List.rev args) m)
| ( EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _
| EMatch _ | ELit _ | EDefault _ | EPureDefault _ | EIfThenElse _ | EArray _
| EEmptyError | EErrorOnEmpty _ ) as e ->
| EMatch _ | ELit _ | EDefault _ | EPureDefault _ | EFatalError _
| EIfThenElse _ | EArray _ | EEmpty | EErrorOnEmpty _ ) as e ->
Expr.map ~f:(translate_expr ctx) (e, m)
(** {1 Rule tree construction} *)
@ -450,19 +448,19 @@ let rec rule_tree_to_expr
match Expr.unbox base_just with
| ELit (LBool false), _ -> acc
| _ ->
let cons = Expr.make_puredefault base_cons in
Expr.edefault
~excepts:[]
(* Here we insert the logging command that records when a
decision is taken for the value of a variable. *)
~just:(tag_with_log_entry base_just PosRecordIfTrueBool [])
~cons:(Expr.epuredefault base_cons emark)
emark
~cons (Mark.get cons)
:: acc)
(translate_and_unbox_list base_just_list)
(translate_and_unbox_list base_cons_list)
[])
~just:(Expr.elit (LBool false) emark)
~cons:(Expr.eemptyerror emark) emark
~cons:(Expr.eempty emark) emark
in
let exceptions =
List.map
@ -561,15 +559,15 @@ let translate_def
caller. *)
then
let m = Untyped { pos = D.ScopeDef.get_position def_info } in
let empty_error = Expr.eemptyerror m in
let empty = Expr.eempty m in
match params with
| Some (ps, _) ->
let labels, tys = List.split ps in
Expr.make_abs
(Array.of_list
(List.map (fun lbl -> Var.make (Mark.remove lbl)) labels))
empty_error tys (Expr.mark_pos m)
| _ -> empty_error
empty tys (Expr.mark_pos m)
| _ -> empty
else
rule_tree_to_expr ~toplevel:true ~is_reentrant_var:is_reentrant
~subscope:is_subscope_var ctx

16
compiler/shared_ast/definitions.ml
View File

@ -378,12 +378,6 @@ end
type 'a operator = 'a Op.t
type except =
| ConflictError of Pos.t list
| EmptyError
| NoValueProvided
| Crash of string
(** {2 Markings} *)
type untyped = { pos : Pos.t } [@@caml.unboxed]
@ -478,7 +472,7 @@ and ('a, 'b, 'm) base_gexpr =
}
-> ('a, < .. >, 'm) base_gexpr
| EAppOp : {
op : 'a operator;
op : 'a operator Mark.pos;
args : ('a, 'm) gexpr list;
tys : typ list;
}
@ -553,6 +547,7 @@ and ('a, 'b, 'm) base_gexpr =
}
-> ('a, < explicitScopes : no ; .. >, 't) base_gexpr
| EAssert : ('a, 'm) gexpr -> ('a, < assertions : yes ; .. >, 'm) base_gexpr
| EFatalError : Runtime.error -> ('a, < .. >, 'm) base_gexpr
(* Default terms *)
| EDefault : {
excepts : ('a, 'm) gexpr list;
@ -564,15 +559,14 @@ and ('a, 'b, 'm) base_gexpr =
('a, 'm) gexpr
-> ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr
(** "return" of a pure term, so that it can be typed as [default] *)
| EEmptyError : ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr
| EEmpty : ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr
| EErrorOnEmpty :
('a, 'm) gexpr
-> ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr
(* Lambda calculus with exceptions *)
| ERaise : except -> ('a, < exceptions : yes ; .. >, 'm) base_gexpr
| ECatch : {
| ERaiseEmpty : ('a, < exceptions : yes ; .. >, 'm) base_gexpr
| ECatchEmpty : {
body : ('a, 'm) gexpr;
exn : except;
handler : ('a, 'm) gexpr;
}
-> ('a, < exceptions : yes ; .. >, 'm) base_gexpr

131
compiler/shared_ast/expr.ml
View File

@ -128,6 +128,7 @@ let eabs binder tys mark =
let eapp ~f ~args ~tys = Box.app1n f args @@ fun f args -> EApp { f; args; tys }
let eassert e1 = Box.app1 e1 @@ fun e1 -> EAssert e1
let efatalerror e1 = Box.app0 @@ EFatalError e1
let eappop ~op ~args ~tys =
Box.appn args @@ fun args -> EAppOp { op; args; tys }
@ -143,11 +144,11 @@ 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 = Mark.add mark (Bindlib.box EEmptyError)
let eraise e1 = Box.app0 @@ ERaise e1
let eempty mark = Mark.add mark (Bindlib.box EEmpty)
let eraiseempty mark = Mark.add mark (Bindlib.box ERaiseEmpty)
let ecatch body exn handler =
Box.app2 body handler @@ fun body handler -> ECatch { body; exn; handler }
let ecatchempty body handler =
Box.app2 body handler @@ fun body handler -> ECatchEmpty { body; handler }
let ecustom obj targs tret mark =
Mark.add mark (Bindlib.box (ECustom { obj; targs; tret }))
@ -275,13 +276,33 @@ let option_enum_config =
EnumConstructor.Map.of_list
[none_constr, (TLit TUnit, Pos.no_pos); some_constr, (TAny, Pos.no_pos)]
let pos_to_runtime pos =
{
Runtime.filename = Pos.get_file pos;
start_line = Pos.get_start_line pos;
start_column = Pos.get_start_column pos;
end_line = Pos.get_end_line pos;
end_column = Pos.get_end_column pos;
law_headings = Pos.get_law_info pos;
}
let runtime_to_pos rpos =
let pos =
let open Runtime in
Pos.from_info rpos.filename rpos.start_line rpos.start_column rpos.end_line
rpos.end_column
in
Pos.overwrite_law_info pos rpos.law_headings
(* - Traversal functions - *)
(* shallow map *)
let map
(type a b)
?(typ : typ -> typ = Fun.id)
?op:(fop = (fun _ -> invalid_arg "Expr.map" : a Operator.t -> b Operator.t))
?op:(fop =
(fun _ -> invalid_arg "Expr.map"
: a Operator.t Mark.pos -> b Operator.t Mark.pos))
~(f : (a, 'm1) gexpr -> (b, 'm2) boxed_gexpr)
(e : ((a, b, 'm1) base_gexpr, 'm2) marked) : (b, 'm2) boxed_gexpr =
let m = map_ty typ (Mark.get e) in
@ -306,13 +327,14 @@ let map
| ETupleAccess { e; index; size } -> etupleaccess ~e:(f e) ~index ~size m
| EInj { name; cons; e } -> einj ~name ~cons ~e:(f e) m
| EAssert e1 -> eassert (f e1) m
| EFatalError e1 -> efatalerror e1 m
| EDefault { excepts; just; cons } ->
edefault ~excepts:(List.map f excepts) ~just:(f just) ~cons:(f cons) m
| EPureDefault e1 -> epuredefault (f e1) m
| EEmptyError -> eemptyerror m
| EEmpty -> eempty m
| EErrorOnEmpty e1 -> eerroronempty (f e1) m
| ECatch { body; exn; handler } -> ecatch (f body) exn (f handler) m
| ERaise exn -> eraise exn m
| ECatchEmpty { body; handler } -> ecatchempty (f body) (f handler) m
| ERaiseEmpty -> eraiseempty m
| ELocation loc -> elocation loc m
| EStruct { name; fields } ->
let fields = StructField.Map.map f fields in
@ -343,7 +365,9 @@ let shallow_fold
(acc : 'acc) : 'acc =
let lfold x acc = List.fold_left (fun acc x -> f x acc) acc x in
match Mark.remove e with
| ELit _ | EVar _ | EExternal _ | ERaise _ | ELocation _ | EEmptyError -> acc
| ELit _ | EVar _ | EFatalError _ | EExternal _ | ERaiseEmpty | ELocation _
| EEmpty ->
acc
| EApp { f = e; args; _ } -> acc |> f e |> lfold args
| EAppOp { args; _ } -> acc |> lfold args
| EArray args -> acc |> lfold args
@ -358,7 +382,7 @@ let shallow_fold
| EDefault { excepts; just; cons } -> acc |> lfold excepts |> f just |> f cons
| EPureDefault e -> acc |> f e
| EErrorOnEmpty e -> acc |> f e
| ECatch { body; handler; _ } -> acc |> f body |> f handler
| ECatchEmpty { body; handler } -> acc |> f body |> f handler
| EStruct { fields; _ } -> acc |> StructField.Map.fold (fun _ -> f) fields
| EDStructAmend { e; fields; _ } ->
acc |> f e |> Ident.Map.fold (fun _ -> f) fields
@ -423,6 +447,7 @@ let map_gather
| EAssert e ->
let acc, e = f e in
acc, eassert e m
| EFatalError e -> acc, efatalerror e m
| EDefault { excepts; just; cons } ->
let acc1, excepts = lfoldmap excepts in
let acc2, just = f just in
@ -431,15 +456,15 @@ let map_gather
| EPureDefault e ->
let acc, e = f e in
acc, epuredefault e m
| EEmptyError -> acc, eemptyerror m
| EEmpty -> acc, eempty m
| EErrorOnEmpty e ->
let acc, e = f e in
acc, eerroronempty e m
| ECatch { body; exn; handler } ->
| ECatchEmpty { body; handler } ->
let acc1, body = f body in
let acc2, handler = f handler in
join acc1 acc2, ecatch body exn handler m
| ERaise exn -> acc, eraise exn m
join acc1 acc2, ecatchempty body handler m
| ERaiseEmpty -> acc, eraiseempty m
| ELocation loc -> acc, elocation loc m
| EStruct { name; fields } ->
let acc, fields =
@ -507,7 +532,7 @@ let untype e = map_marks ~f:(fun m -> Untyped { pos = mark_pos m }) e
let is_value (type a) (e : (a, _) gexpr) =
match Mark.remove e with
| ELit _ | EAbs _ | ERaise _ | ECustom _ | EExternal _ -> true
| ELit _ | EAbs _ | ERaiseEmpty | ECustom _ | EExternal _ -> true
| _ -> false
let equal_lit (l1 : lit) (l2 : lit) =
@ -519,7 +544,9 @@ let equal_lit (l1 : lit) (l2 : lit) =
| 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
| LDuration d1, LDuration d2 -> (
try o_eq_dur_dur (pos_to_runtime Pos.no_pos) d1 d2
with Runtime.(Error (UncomparableDurations, _)) -> false)
| (LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _), _ ->
false
@ -581,8 +608,8 @@ let compare_location
| _, ToplevelVar _ -> .
let equal_location a b = compare_location a b = 0
let equal_except ex1 ex2 = ex1 = ex2
let compare_except ex1 ex2 = Stdlib.compare ex1 ex2
let equal_error er1 er2 = er1 = er2
let compare_error er1 er2 = Stdlib.compare er1 er2
let equal_external_ref ref1 ref2 =
match ref1, ref2 with
@ -623,10 +650,11 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
equal e1 e2 && equal_list args1 args2 && Type.equal_list tys1 tys2
| ( EAppOp { op = op1; args = args1; tys = tys1 },
EAppOp { op = op2; args = args2; tys = tys2 } ) ->
Operator.equal op1 op2
Mark.equal Operator.equal op1 op2
&& equal_list args1 args2
&& Type.equal_list tys1 tys2
| EAssert e1, EAssert e2 -> equal e1 e2
| EFatalError e1, EFatalError e2 -> equal_error e1 e2
| ( EDefault { excepts = exc1; just = def1; cons = cons1 },
EDefault { excepts = exc2; just = def2; cons = cons2 } ) ->
equal def1 def2 && equal cons1 cons2 && equal_list exc1 exc2
@ -634,12 +662,12 @@ 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
| EEmpty, EEmpty -> true
| EErrorOnEmpty e1, EErrorOnEmpty e2 -> equal e1 e2
| ERaise ex1, ERaise ex2 -> equal_except ex1 ex2
| ( ECatch { body = etry1; exn = ex1; handler = ewith1 },
ECatch { body = etry2; exn = ex2; handler = ewith2 } ) ->
equal etry1 etry2 && equal_except ex1 ex2 && equal ewith1 ewith2
| ERaiseEmpty, ERaiseEmpty -> true
| ( ECatchEmpty { body = etry1; handler = ewith1 },
ECatchEmpty { body = etry2; handler = ewith2 } ) ->
equal etry1 etry2 && equal ewith1 ewith2
| ELocation l1, ELocation l2 ->
equal_location (Mark.add Pos.no_pos l1) (Mark.add Pos.no_pos l2)
| ( EStruct { name = s1; fields = fields1 },
@ -671,10 +699,11 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
ECustom { obj = obj2; targs = targs2; tret = tret2 } ) ->
Type.equal_list targs1 targs2 && Type.equal tret1 tret2 && obj1 == obj2
| ( ( EVar _ | EExternal _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _
| EAbs _ | EApp _ | EAppOp _ | EAssert _ | EDefault _ | EPureDefault _
| EIfThenElse _ | EEmptyError | EErrorOnEmpty _ | ERaise _ | ECatch _
| ELocation _ | EStruct _ | EDStructAmend _ | EDStructAccess _
| EStructAccess _ | EInj _ | EMatch _ | EScopeCall _ | ECustom _ ),
| EAbs _ | EApp _ | EAppOp _ | EAssert _ | EFatalError _ | EDefault _
| EPureDefault _ | EIfThenElse _ | EEmpty | EErrorOnEmpty _ | ERaiseEmpty
| ECatchEmpty _ | ELocation _ | EStruct _ | EDStructAmend _
| EDStructAccess _ | EStructAccess _ | EInj _ | EMatch _ | EScopeCall _
| ECustom _ ),
_ ) ->
false
@ -692,7 +721,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
List.compare compare args1 args2 @@< fun () ->
List.compare Type.compare tys1 tys2
| EAppOp {op=op1; args=args1; tys=tys1}, EAppOp {op=op2; args=args2; tys=tys2} ->
Operator.compare op1 op2 @@< fun () ->
Mark.compare Operator.compare op1 op2 @@< fun () ->
List.compare compare args1 args2 @@< fun () ->
List.compare Type.compare tys1 tys2
| EArray a1, EArray a2 ->
@ -755,6 +784,8 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
compare e1 e2
| EAssert e1, EAssert e2 ->
compare e1 e2
| EFatalError e1, EFatalError e2 ->
compare_error e1 e2
| EDefault {excepts=exs1; just=just1; cons=cons1},
EDefault {excepts=exs2; just=just2; cons=cons2} ->
compare just1 just2 @@< fun () ->
@ -762,14 +793,12 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
List.compare compare exs1 exs2
| EPureDefault e1, EPureDefault e2 ->
compare e1 e2
| EEmptyError, EEmptyError -> 0
| EEmpty, EEmpty -> 0
| EErrorOnEmpty e1, EErrorOnEmpty e2 ->
compare e1 e2
| ERaise ex1, ERaise ex2 ->
compare_except ex1 ex2
| ECatch {body=etry1; exn=ex1; handler=ewith1},
ECatch {body=etry2; exn=ex2; handler=ewith2} ->
compare_except ex1 ex2 @@< fun () ->
| ERaiseEmpty, ERaiseEmpty -> 0
| ECatchEmpty {body=etry1; handler=ewith1},
ECatchEmpty {body=etry2; handler=ewith2} ->
compare etry1 etry2 @@< fun () ->
compare ewith1 ewith2
| ECustom _, _ | _, ECustom _ ->
@ -794,12 +823,13 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
| ETupleAccess _, _ -> -1 | _, ETupleAccess _ -> 1
| EInj _, _ -> -1 | _, EInj _ -> 1
| EAssert _, _ -> -1 | _, EAssert _ -> 1
| EFatalError _, _ -> -1 | _, EFatalError _ -> 1
| EDefault _, _ -> -1 | _, EDefault _ -> 1
| EPureDefault _, _ -> -1 | _, EPureDefault _ -> 1
| EEmptyError , _ -> -1 | _, EEmptyError -> 1
| EEmpty , _ -> -1 | _, EEmpty -> 1
| EErrorOnEmpty _, _ -> -1 | _, EErrorOnEmpty _ -> 1
| ERaise _, _ -> -1 | _, ERaise _ -> 1
| ECatch _, _ -> . | _, ECatch _ -> .
| ERaiseEmpty, _ -> -1 | _, ERaiseEmpty -> 1
| ECatchEmpty _, _ -> . | _, ECatchEmpty _ -> .
let rec free_vars : ('a, 't) gexpr -> ('a, 't) gexpr Var.Set.t = function
| EVar v, _ -> Var.Set.singleton v
@ -817,7 +847,8 @@ let remove_logging_calls e =
let rec f e =
let e, m = map ~f ~op:Fun.id e in
( Bindlib.box_apply
(function EAppOp { op = Log _; args = [(arg, _)]; _ } -> arg | e -> e)
(function
| EAppOp { op = Log _, _; args = [(arg, _)]; _ } -> arg | e -> e)
e,
m )
in
@ -907,12 +938,13 @@ let format ppf e = Print.expr ~debug:false () ppf e
let rec size : type a. (a, 't) gexpr -> int =
fun e ->
match Mark.remove e with
| EVar _ | EExternal _ | ELit _ | EEmptyError | ECustom _ -> 1
| EVar _ | EExternal _ | ELit _ | EEmpty | ECustom _ -> 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
| EInj { e; _ } -> size e + 1
| EAssert e -> size e + 1
| EFatalError _ -> 1
| EErrorOnEmpty e -> size e + 1
| EPureDefault e -> size e + 1
| EApp { f; args; _ } ->
@ -928,8 +960,8 @@ let rec size : type a. (a, 't) gexpr -> int =
(fun acc except -> acc + size except)
(1 + size just + size cons)
excepts
| ERaise _ -> 1
| ECatch { body; handler; _ } -> 1 + size body + size handler
| ERaiseEmpty -> 1
| ECatchEmpty { body; handler } -> 1 + size body + size handler
| ELocation _ -> 1
| EStruct { fields; _ } ->
StructField.Map.fold (fun _ e acc -> acc + 1 + size e) fields 0
@ -1024,16 +1056,13 @@ let thunk_term term =
let pos = mark_pos (Mark.get term) in
make_abs [| silent |] term [TLit TUnit, pos] pos
let empty_thunked_term mark = thunk_term (Bindlib.box EEmptyError, mark)
let empty_thunked_term mark = thunk_term (Bindlib.box EEmpty, mark)
let unthunk_term_nobox term mark =
Mark.add mark
(EApp
{
f = term;
args = [ELit LUnit, mark];
tys = [TLit TUnit, mark_pos mark];
})
let unthunk_term_nobox = function
| EAbs { binder; tys = [(TLit TUnit, _)] }, _ ->
let _v, e = Bindlib.unmbind binder in
e
| _ -> invalid_arg "unthunk_term_nobox"
let make_let_in x tau e1 e2 mpos =
make_app (make_abs [| x |] e2 [tau] mpos) [e1] [tau] (pos e2)

23
compiler/shared_ast/expr.mli
View File

@ -82,8 +82,10 @@ val eassert :
'm mark ->
((< assertions : yes ; .. > as 'a), 'm) boxed_gexpr
val efatalerror : Runtime.error -> 'm mark -> (< .. >, 'm) boxed_gexpr
val eappop :
op:'a operator ->
op:'a operator Mark.pos ->
args:('a, 'm) boxed_gexpr list ->
tys:typ list ->
'm mark ->
@ -108,22 +110,20 @@ val eifthenelse :
'm mark ->
('a any, 'm) boxed_gexpr
val eemptyerror :
'm mark -> ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
val eempty : 'm mark -> ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
val eerroronempty :
('a, 'm) boxed_gexpr ->
'm mark ->
((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
val ecatch :
val ecatchempty :
('a, 'm) boxed_gexpr ->
except ->
('a, 'm) boxed_gexpr ->
'm mark ->
((< exceptions : yes ; .. > as 'a), 'm) boxed_gexpr
val eraise : except -> 'm mark -> (< exceptions : yes ; .. >, 'm) boxed_gexpr
val eraiseempty : 'm mark -> (< exceptions : yes ; .. >, 'm) boxed_gexpr
val elocation : 'a glocation -> 'm mark -> ((< .. > as 'a), 'm) boxed_gexpr
val estruct :
@ -229,6 +229,8 @@ val option_enum : EnumName.t
val none_constr : EnumConstructor.t
val some_constr : EnumConstructor.t
val option_enum_config : typ EnumConstructor.Map.t
val pos_to_runtime : Pos.t -> Runtime.source_position
val runtime_to_pos : Runtime.source_position -> Pos.t
(** Manipulation of marked expressions *)
@ -241,7 +243,7 @@ val untype : ('a, 'm) gexpr -> ('a, untyped) boxed_gexpr
val map :
?typ:(typ -> typ) ->
?op:('a operator -> 'b operator) ->
?op:('a operator Mark.pos -> 'b operator Mark.pos) ->
f:(('a, 'm1) gexpr -> ('b, 'm2) boxed_gexpr) ->
(('a, 'b, 'm1) base_gexpr, 'm2) marked ->
('b, 'm2) boxed_gexpr
@ -359,7 +361,10 @@ val empty_thunked_term :
'm mark -> (< defaultTerms : yes ; .. >, 'm) boxed_gexpr
val thunk_term : ('a any, 'b) boxed_gexpr -> ('a, 'b) boxed_gexpr
val unthunk_term_nobox : ('a any, 'm) gexpr -> 'm mark -> ('a, 'm) gexpr
val unthunk_term_nobox : ('a any, 'm) gexpr -> ('a, 'm) gexpr
(** Remove thunking around an expression (this assumes it's the right form,
raises Invalid_argument otherwise) *)
val make_let_in :
('a, 'm) gexpr Var.t ->
@ -416,8 +421,6 @@ val equal_lit : lit -> lit -> bool
val compare_lit : lit -> lit -> int
val equal_location : 'a glocation Mark.pos -> 'a glocation Mark.pos -> bool
val compare_location : 'a glocation Mark.pos -> 'a glocation Mark.pos -> int
val equal_except : except -> except -> bool
val compare_except : except -> except -> int
val equal : ('a, 'm) gexpr -> ('a, 'm) gexpr -> bool
(** Determines if two expressions are equal, omitting their position information *)

246
compiler/shared_ast/interpreter.ml
View File

@ -26,7 +26,7 @@ module Runtime = Runtime_ocaml.Runtime
(** {1 Helpers} *)
let is_empty_error : type a. (a, 'm) gexpr -> bool =
fun e -> match Mark.remove e with EEmptyError -> true | _ -> false
fun e -> match Mark.remove e with EEmpty -> true | _ -> false
(* TODO: we should provide a generic way to print logs, that work across the
different backends: python, ocaml, javascript, and interpreter *)
@ -59,20 +59,11 @@ let print_log lang entry infos pos e =
Message.log "%s%a %a" !indent_str Print.log_entry entry Print.uid_list
infos
exception CatalaException of except * Pos.t
let () =
Printexc.register_printer (function
| CatalaException (e, _pos) ->
Some
(Format.asprintf "uncaught exception %a raised during interpretation"
Print.except e)
| _ -> None)
(* Todo: this should be handled early when resolving overloads. Here we have
proper structural equality, but the OCaml backend for example uses the
builtin equality function instead of this. *)
let handle_eq evaluate_operator pos lang e1 e2 =
let handle_eq pos evaluate_operator m lang e1 e2 =
let eq_eval = evaluate_operator (Eq, pos) m lang in
let open Runtime.Oper in
match e1, e2 with
| ELit LUnit, ELit LUnit -> true
@ -80,13 +71,14 @@ let handle_eq evaluate_operator pos lang e1 e2 =
| ELit (LInt x1), ELit (LInt x2) -> o_eq_int_int x1 x2
| ELit (LRat x1), ELit (LRat x2) -> o_eq_rat_rat x1 x2
| ELit (LMoney x1), ELit (LMoney x2) -> o_eq_mon_mon x1 x2
| ELit (LDuration x1), ELit (LDuration x2) -> o_eq_dur_dur x1 x2
| ELit (LDuration x1), ELit (LDuration x2) ->
o_eq_dur_dur (Expr.pos_to_runtime (Expr.mark_pos m)) x1 x2
| ELit (LDate x1), ELit (LDate x2) -> o_eq_dat_dat x1 x2
| EArray es1, EArray es2 -> (
try
List.for_all2
(fun e1 e2 ->
match Mark.remove (evaluate_operator Eq pos lang [e1; e2]) with
match Mark.remove (eq_eval [e1; e2]) with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
@ -96,7 +88,7 @@ let handle_eq evaluate_operator pos lang e1 e2 =
StructName.equal s1 s2
&& StructField.Map.equal
(fun e1 e2 ->
match Mark.remove (evaluate_operator Eq pos lang [e1; e2]) with
match Mark.remove (eq_eval [e1; e2]) with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
@ -107,7 +99,7 @@ let handle_eq evaluate_operator pos lang e1 e2 =
EnumName.equal en1 en2
&& EnumConstructor.equal i1 i2
&&
match Mark.remove (evaluate_operator Eq pos lang [e1; e2]) with
match Mark.remove (eq_eval [e1; e2]) with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *)
@ -117,31 +109,16 @@ let handle_eq evaluate_operator pos lang e1 e2 =
(* Call-by-value: the arguments are expected to be already evaluated here *)
let rec evaluate_operator
evaluate_expr
(op : < overloaded : no ; .. > operator)
((op, opos) : < overloaded : no ; .. > operator Mark.pos)
m
lang
args =
let pos = Expr.mark_pos m in
let protect f x y =
let get_binop_args_pos = function
| (arg0 :: arg1 :: _ : ('t, 'm) gexpr list) ->
["", Expr.pos arg0; "", Expr.pos arg1]
| _ -> assert false
in
try f x y with
| Runtime.Division_by_zero ->
Message.error
~extra_pos:
[
"The division operator:", pos;
"The null denominator:", Expr.pos (List.nth args 1);
]
"division by zero at runtime"
| Runtime.UncomparableDurations ->
Message.error ~extra_pos:(get_binop_args_pos args) "%a"
Format.pp_print_text
"Cannot compare together durations that cannot be converted to a \
precise number of days"
let rpos () = Expr.pos_to_runtime opos in
let div_pos () =
(* Division by 0 errors point to their 2nd operand *)
Expr.pos_to_runtime
@@ match args with _ :: denom :: _ -> Expr.pos denom | _ -> opos
in
let err () =
Message.error
@ -150,7 +127,7 @@ let rec evaluate_operator
( Format.asprintf "Operator (value %a):"
(Print.operator ~debug:true)
op,
pos );
opos );
]
@ List.mapi
(fun i arg ->
@ -180,7 +157,7 @@ let rec evaluate_operator
Mark.remove e'
| (ToClosureEnv | FromClosureEnv), _ -> err ()
| Eq, [(e1, _); (e2, _)] ->
ELit (LBool (handle_eq (evaluate_operator evaluate_expr) m lang e1 e2))
ELit (LBool (handle_eq opos (evaluate_operator evaluate_expr) m lang e1 e2))
| Map, [f; (EArray es, _)] ->
EArray
(List.map
@ -315,15 +292,15 @@ let rec evaluate_operator
| 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))
ELit (LRat (o_div_int_int (div_pos ()) x y))
| Div_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (protect o_div_rat_rat x y))
ELit (LRat (o_div_rat_rat (div_pos ()) x y))
| Div_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LRat (protect o_div_mon_mon x y))
ELit (LRat (o_div_mon_mon (div_pos ()) x y))
| Div_mon_rat, [(ELit (LMoney x), _); (ELit (LRat y), _)] ->
ELit (LMoney (protect o_div_mon_rat x y))
ELit (LMoney (o_div_mon_rat (div_pos ()) x y))
| Div_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LRat (protect o_div_dur_dur x y))
ELit (LRat (o_div_dur_dur (div_pos ()) 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), _)] ->
@ -333,7 +310,7 @@ let rec evaluate_operator
| 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))
ELit (LBool (o_lt_dur_dur (rpos ()) 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), _)] ->
@ -343,7 +320,7 @@ let rec evaluate_operator
| 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))
ELit (LBool (o_lte_dur_dur (rpos ()) 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), _)] ->
@ -353,7 +330,7 @@ let rec evaluate_operator
| 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))
ELit (LBool (o_gt_dur_dur (rpos ()) 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), _)] ->
@ -363,7 +340,7 @@ let rec evaluate_operator
| 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))
ELit (LBool (o_gte_dur_dur (rpos ()) 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), _)] ->
@ -373,24 +350,23 @@ let rec evaluate_operator
| 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))
ELit (LBool (o_eq_dur_dur (rpos ()) x y))
| HandleDefault, [(EArray excepts, _); just; cons] -> (
(* This case is for lcalc with exceptions: we rely OCaml exception handling
here *)
match
List.filter_map
(fun e ->
try Some (evaluate_expr (Expr.unthunk_term_nobox e m))
with CatalaException (EmptyError, _) -> None)
try Some (evaluate_expr (Expr.unthunk_term_nobox e))
with Runtime.Empty -> None)
excepts
with
| [] -> (
let just = evaluate_expr (Expr.unthunk_term_nobox just m) in
let just = evaluate_expr (Expr.unthunk_term_nobox just) in
match Mark.remove just with
| ELit (LBool true) ->
Mark.remove
(evaluate_expr (Expr.unthunk_term_nobox cons (Mark.get cons)))
| ELit (LBool false) -> raise (CatalaException (EmptyError, pos))
Mark.remove (evaluate_expr (Expr.unthunk_term_nobox cons))
| ELit (LBool false) -> raise Runtime.Empty
| _ ->
Message.error ~pos
"Default justification has not been reduced to a boolean at@ \
@ -398,7 +374,12 @@ let rec evaluate_operator
%a@."
Expr.format just)
| [e] -> Mark.remove e
| es -> raise (CatalaException (ConflictError (List.map Expr.pos es), pos)))
| es ->
raise
Runtime.(
Error
(Conflict, List.map (fun e -> Expr.pos_to_runtime (Expr.pos e)) es))
)
| HandleDefaultOpt, [(EArray exps, _); justification; conclusion] -> (
let valid_exceptions =
ListLabels.filter exps ~f:(function
@ -408,10 +389,10 @@ let rec evaluate_operator
in
match valid_exceptions with
| [] -> (
let e = evaluate_expr (Expr.unthunk_term_nobox justification m) in
let e = evaluate_expr (Expr.unthunk_term_nobox justification) in
match Mark.remove e with
| ELit (LBool true) ->
Mark.remove (evaluate_expr (Expr.unthunk_term_nobox conclusion m))
Mark.remove (evaluate_expr (Expr.unthunk_term_nobox conclusion))
| ELit (LBool false) ->
EInj
{
@ -435,7 +416,10 @@ let rec evaluate_operator
e
| [_] -> err ()
| excs ->
raise (CatalaException (ConflictError (List.map Expr.pos excs), pos)))
raise
Runtime.(
Error (Conflict, List.map Expr.(fun e -> pos_to_runtime (pos e)) excs))
)
| ( ( 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
@ -533,7 +517,7 @@ and val_to_runtime :
Obj.t =
fun eval_expr ctx ty v ->
match Mark.remove ty, Mark.remove v with
| _, EEmptyError -> raise Runtime.EmptyError
| _, EEmpty -> raise Runtime.Empty
| TLit TBool, ELit (LBool b) -> Obj.repr b
| TLit TUnit, ELit LUnit -> Obj.repr ()
| TLit TInt, ELit (LInt i) -> Obj.repr i
@ -594,8 +578,7 @@ and val_to_runtime :
let args = List.rev acc in
let tys = List.map (fun a -> Expr.maybe_ty (Mark.get a)) args in
val_to_runtime eval_expr ctx tret
(try eval_expr ctx (EApp { f = v; args; tys }, m)
with CatalaException (EmptyError, _) -> raise Runtime.EmptyError)
(eval_expr ctx (EApp { f = v; args; tys }, m))
| targ :: targs ->
Obj.repr (fun x ->
curry (runtime_to_val eval_expr ctx m targ x :: acc) targs)
@ -663,29 +646,24 @@ let rec evaluate_expr :
Message.error ~pos "wrong function call, expected %d arguments, got %d"
(Bindlib.mbinder_arity binder)
(List.length args)
| ECustom { obj; targs; tret } -> (
| ECustom { obj; targs; tret } ->
(* Applies the arguments one by one to the curried form *)
match
let o =
List.fold_left2
(fun fobj targ arg ->
(Obj.obj fobj : Obj.t -> Obj.t)
(val_to_runtime (fun ctx -> evaluate_expr ctx lang) ctx targ arg))
obj targs args
with
| exception e ->
Format.ksprintf
(fun s -> raise (CatalaException (Crash s, pos)))
"@[<hv 2>This call to code from a module failed with:@ %s@]"
(Printexc.to_string e)
| o -> runtime_to_val (fun ctx -> evaluate_expr ctx lang) ctx m tret o)
in
runtime_to_val (fun ctx -> evaluate_expr ctx lang) ctx m tret o
| _ ->
Message.error ~pos "%a" Format.pp_print_text
Message.error ~pos ~internal:true "%a" Format.pp_print_text
"function has not been reduced to a lambda at evaluation (should not \
happen if the term was well-typed")
| EAppOp { op; args; _ } ->
let args = List.map (evaluate_expr ctx lang) args in
evaluate_operator (evaluate_expr ctx lang) op m lang args
| EAbs _ | ELit _ | ECustom _ | EEmptyError -> e (* these are values *)
| EAbs _ | ELit _ | ECustom _ | EEmpty -> e (* these are values *)
| EStruct { fields = es; name } ->
let fields, es = List.split (StructField.Map.bindings es) in
let es = List.map (evaluate_expr ctx lang) es in
@ -777,20 +755,21 @@ let rec evaluate_expr :
match Mark.remove e with
| ELit (LBool true) -> Mark.add m (ELit LUnit)
| ELit (LBool false) ->
Message.error ~pos:(Expr.pos e') "Assertion failed:@\n%a"
Message.warning "Assertion failed:@ %a"
(Print.UserFacing.expr lang)
(partially_evaluate_expr_for_assertion_failure_message ctx lang
(Expr.skip_wrappers e'))
(Expr.skip_wrappers e'));
raise Runtime.(Error (AssertionFailed, [Expr.pos_to_runtime pos]))
| _ ->
Message.error ~pos:(Expr.pos e') "%a" Format.pp_print_text
"Expected a boolean literal for the result of this assertion (should \
not happen if the term was well-typed)")
| EFatalError err -> raise (Runtime.Error (err, [Expr.pos_to_runtime pos]))
| EErrorOnEmpty e' -> (
match evaluate_expr ctx lang e' with
| EEmptyError, _ ->
Message.error ~pos:(Expr.pos e') "%a" Format.pp_print_text
"This variable evaluated to an empty term (no rule that defined it \
applied in this situation)"
| EEmpty, _ -> raise Runtime.(Error (NoValue, [Expr.pos_to_runtime pos]))
| exception Runtime.Empty ->
raise Runtime.(Error (NoValue, [Expr.pos_to_runtime pos]))
| e -> e)
| EDefault { excepts; just; cons } -> (
let excepts = List.map (evaluate_expr ctx lang) excepts in
@ -800,7 +779,7 @@ let rec evaluate_expr :
let just = evaluate_expr ctx lang just in
match Mark.remove just with
| ELit (LBool true) -> evaluate_expr ctx lang cons
| ELit (LBool false) -> Mark.copy e EEmptyError
| ELit (LBool false) -> Mark.copy e EEmpty
| _ ->
Message.error ~pos:(Expr.pos e) "%a" Format.pp_print_text
"Default justification has not been reduced to a boolean at \
@ -809,16 +788,17 @@ let rec evaluate_expr :
| _ ->
let poslist =
List.filter_map
(fun ex -> if is_empty_error ex then None else Some (Expr.pos ex))
(fun ex ->
if is_empty_error ex then None
else Some Expr.(pos_to_runtime (pos ex)))
excepts
in
raise (CatalaException (ConflictError poslist, pos)))
raise Runtime.(Error (Conflict, poslist)))
| EPureDefault e -> evaluate_expr ctx lang e
| ERaise exn -> raise (CatalaException (exn, pos))
| ECatch { body; exn; handler } -> (
| ERaiseEmpty -> raise Runtime.Empty
| ECatchEmpty { body; handler } -> (
try evaluate_expr ctx lang body
with CatalaException (caught, _) when Expr.equal_except caught exn ->
evaluate_expr ctx lang handler)
with Runtime.Empty -> evaluate_expr ctx lang handler)
| _ -> .
and partially_evaluate_expr_for_assertion_failure_message :
@ -839,12 +819,13 @@ and partially_evaluate_expr_for_assertion_failure_message :
args = [e1; e2];
tys;
op =
( And | Or | Xor | Eq | Lt_int_int | Lt_rat_rat | Lt_mon_mon
( ( And | Or | Xor | Eq | 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_dur_dur | Eq_dat_dat ) as op;
| Eq_dur_dur | Eq_dat_dat ),
_ ) as op;
} ->
( EAppOp
{
@ -859,6 +840,20 @@ and partially_evaluate_expr_for_assertion_failure_message :
Mark.get e )
| _ -> evaluate_expr ctx lang e
let evaluate_expr_safe :
type d e.
decl_ctx ->
Global.backend_lang ->
((d, e, yes) interpr_kind, 't) gexpr ->
((d, e, yes) interpr_kind, 't) gexpr =
fun ctx lang e ->
try evaluate_expr ctx lang e
with Runtime.Error (err, rpos) ->
Message.error
~extra_pos:(List.map (fun rp -> "", Expr.runtime_to_pos rp) rpos)
"During evaluation: %a." Format.pp_print_text
(Runtime.error_message err)
(* Typing shenanigan to add custom terms to the AST type. *)
let addcustom e =
let rec f :
@ -870,13 +865,13 @@ let addcustom e =
Expr.eappop ~tys ~args:(List.map f args) ~op:(Operator.translate op) m
| (EDefault _, _) as e -> Expr.map ~f e
| (EPureDefault _, _) as e -> Expr.map ~f e
| (EEmptyError, _) as e -> Expr.map ~f e
| (EEmpty, _) as e -> Expr.map ~f e
| (EErrorOnEmpty _, _) as e -> Expr.map ~f e
| (ECatch _, _) as e -> Expr.map ~f e
| (ERaise _, _) as e -> Expr.map ~f e
| ( ( EAssert _ | ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EAbs _
| EIfThenElse _ | ETuple _ | ETupleAccess _ | EInj _ | EStruct _
| EStructAccess _ | EMatch _ ),
| (ECatchEmpty _, _) as e -> Expr.map ~f e
| (ERaiseEmpty, _) as e -> Expr.map ~f e
| ( ( EAssert _ | EFatalError _ | ELit _ | EApp _ | EArray _ | EVar _
| EExternal _ | EAbs _ | EIfThenElse _ | ETuple _ | ETupleAccess _
| EInj _ | EStruct _ | EStructAccess _ | EMatch _ ),
_ ) as e ->
Expr.map ~f e
| _ -> .
@ -902,13 +897,13 @@ let delcustom e =
Expr.eappop ~tys ~args:(List.map f args) ~op:(Operator.translate op) m
| (EDefault _, _) as e -> Expr.map ~f e
| (EPureDefault _, _) as e -> Expr.map ~f e
| (EEmptyError, _) as e -> Expr.map ~f e
| (EEmpty, _) as e -> Expr.map ~f e
| (EErrorOnEmpty _, _) as e -> Expr.map ~f e
| (ECatch _, _) as e -> Expr.map ~f e
| (ERaise _, _) as e -> Expr.map ~f e
| ( ( EAssert _ | ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EAbs _
| EIfThenElse _ | ETuple _ | ETupleAccess _ | EInj _ | EStruct _
| EStructAccess _ | EMatch _ ),
| (ECatchEmpty _, _) as e -> Expr.map ~f e
| (ERaiseEmpty, _) as e -> Expr.map ~f e
| ( ( EAssert _ | EFatalError _ | ELit _ | EApp _ | EArray _ | EVar _
| EExternal _ | EAbs _ | EIfThenElse _ | ETuple _ | ETupleAccess _
| EInj _ | EStruct _ | EStructAccess _ | EMatch _ ),
_ ) as e ->
Expr.map ~f e
| _ -> .
@ -918,30 +913,11 @@ let delcustom e =
nodes. *)
Expr.unbox (f e)
let interp_failure_message ~pos = function
| NoValueProvided ->
Message.error ~pos "%a" Format.pp_print_text
"This variable evaluated to an empty term (no rule that defined it \
applied in this situation)"
| ConflictError cpos ->
Message.error
~extra_pos:
(List.map
(fun pos -> "This consequence has a valid justification:", pos)
cpos)
"%a" Format.pp_print_text
"There is a conflict between multiple valid consequences for assigning \
the same variable."
| Crash s -> Message.error ~pos "%s" s
| EmptyError ->
Message.error ~pos ~internal:true
"A variable without valid definition escaped"
let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
=
let e = Expr.unbox @@ Program.to_expr p s in
let ctx = p.decl_ctx in
match evaluate_expr ctx p.lang (addcustom e) with
match evaluate_expr_safe ctx p.lang (addcustom e) with
| (EAbs { tys = [((TStruct s_in, _) as _targs)]; _ }, mark_e) as e -> begin
(* At this point, the interpreter seeks to execute the scope but does not
have a way to retrieve input values from the command line. [taus] contain
@ -969,7 +945,7 @@ let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
tell with just this info. *)
Expr.make_abs
(Array.of_list @@ List.map (fun _ -> Var.make "_") ty_in)
(Expr.eraise EmptyError (Expr.with_ty mark_e ty_out))
(Expr.eraiseempty (Expr.with_ty mark_e ty_out))
ty_in (Expr.mark_pos mark_e)
| TTuple ((TArrow (ty_in, (TOption _, _)), _) :: _) ->
(* ... or a closure if closure conversion is enabled *)
@ -980,7 +956,8 @@ let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
(Expr.einj ~e:(Expr.elit LUnit mark_e) ~cons:Expr.none_constr
~name:Expr.option_enum mark_e)
ty_in (Expr.mark_pos mark_e);
Expr.eappop ~op:Operator.ToClosureEnv
Expr.eappop
~op:(Operator.ToClosureEnv, pos)
~args:[Expr.etuple [] mark_e]
~tys:[TClosureEnv, pos]
mark_e;
@ -1006,16 +983,21 @@ let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
[TStruct s_in, Expr.pos e]
(Expr.pos e)
in
match Mark.remove (evaluate_expr ctx p.lang (Expr.unbox to_interpret)) with
match
Mark.remove (evaluate_expr_safe ctx p.lang (Expr.unbox to_interpret))
with
| EStruct { fields; _ } ->
List.map
(fun (fld, e) -> StructField.get_info fld, e)
(StructField.Map.bindings fields)
| exception CatalaException (except, pos) ->
interp_failure_message ~pos except
| exception Runtime.Error (err, rpos) ->
Message.error
~extra_pos:(List.map (fun rp -> "", Expr.runtime_to_pos rp) rpos)
"%a" Format.pp_print_text
(Runtime.error_message err)
| _ ->
Message.error ~pos:(Expr.pos e) "%a" Format.pp_print_text
"The interpretation of a program should always yield a struct \
Message.error ~pos:(Expr.pos e) ~internal:true "%a" Format.pp_print_text
"The interpretation of the program doesn't yield a struct \
corresponding to the scope variables"
end
| _ ->
@ -1028,7 +1010,7 @@ let interpret_program_dcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
=
let ctx = p.decl_ctx in
let e = Expr.unbox (Program.to_expr p s) in
match evaluate_expr p.decl_ctx p.lang (addcustom e) with
match evaluate_expr_safe p.decl_ctx p.lang (addcustom e) with
| (EAbs { tys = [((TStruct s_in, _) as _targs)]; _ }, mark_e) as e -> begin
(* At this point, the interpreter seeks to execute the scope but does not
have a way to retrieve input values from the command line. [taus] contain
@ -1043,7 +1025,7 @@ let interpret_program_dcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
| TArrow (ty_in, ty_out) ->
Expr.make_abs
(Array.of_list @@ List.map (fun _ -> Var.make "_") ty_in)
(Bindlib.box EEmptyError, Expr.with_ty mark_e ty_out)
(Bindlib.box EEmpty, Expr.with_ty mark_e ty_out)
ty_in (Expr.mark_pos mark_e)
| _ ->
Message.error ~pos:(Mark.get ty) "%a" Format.pp_print_text
@ -1063,13 +1045,13 @@ let interpret_program_dcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
[TStruct s_in, Expr.pos e]
(Expr.pos e)
in
match Mark.remove (evaluate_expr ctx p.lang (Expr.unbox to_interpret)) with
match
Mark.remove (evaluate_expr_safe ctx p.lang (Expr.unbox to_interpret))
with
| EStruct { fields; _ } ->
List.map
(fun (fld, e) -> StructField.get_info fld, e)
(StructField.Map.bindings fields)
| exception CatalaException (except, pos) ->
interp_failure_message ~pos except
| _ ->
Message.error ~pos:(Expr.pos e) "%a" Format.pp_print_text
"The interpretation of a program should always yield a struct \

4
compiler/shared_ast/interpreter.mli
View File

@ -20,11 +20,9 @@
open Catala_utils
open Definitions
exception CatalaException of except * Pos.t
val evaluate_operator :
((((_, _, _) interpr_kind as 'a), 'm) gexpr -> ('a, 'm) gexpr) ->
'a operator ->
'a operator Mark.pos ->
'm mark ->
Global.backend_lang ->
('a, 'm) gexpr list ->

78
compiler/shared_ast/operator.ml
View File

@ -330,26 +330,28 @@ let equal t1 t2 = compare t1 t2 = 0
let kind_dispatch :
type a.
polymorphic:(< polymorphic : yes ; .. > t -> 'b) ->
monomorphic:(< monomorphic : yes ; .. > t -> 'b) ->
?overloaded:(< overloaded : yes ; .. > t -> 'b) ->
?resolved:(< resolved : yes ; .. > t -> 'b) ->
a t ->
polymorphic:(< polymorphic : yes ; .. > t Mark.pos -> 'b) ->
monomorphic:(< monomorphic : yes ; .. > t Mark.pos -> 'b) ->
?overloaded:(< overloaded : yes ; .. > t Mark.pos -> 'b) ->
?resolved:(< resolved : yes ; .. > t Mark.pos -> 'b) ->
a t Mark.pos ->
'b =
fun ~polymorphic ~monomorphic ?(overloaded = fun _ -> assert false)
?(resolved = fun _ -> assert false) op ->
match op with
| ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth | And
| Or | Xor ) as op ->
| ( ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth
| And | Or | Xor ),
_ ) as op ->
monomorphic op
| ( Log _ | Length | Eq | Map | Map2 | Concat | Filter | Reduce | Fold
| HandleDefault | HandleDefaultOpt | FromClosureEnv | ToClosureEnv ) as op
->
| ( ( Log _ | Length | Eq | Map | Map2 | Concat | Filter | Reduce | Fold
| HandleDefault | HandleDefaultOpt | FromClosureEnv | ToClosureEnv ),
_ ) as op ->
polymorphic op
| ( Minus | ToRat | ToMoney | Round | Add | Sub | Mult | Div | Lt | Lte | Gt
| Gte ) as op ->
| ( ( Minus | ToRat | ToMoney | Round | Add | Sub | Mult | Div | Lt | Lte | Gt
| Gte ),
_ ) as op ->
overloaded op
| ( Minus_int | Minus_rat | Minus_mon | Minus_dur | ToRat_int | ToRat_mon
| ( ( 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
@ -359,7 +361,8 @@ let kind_dispatch :
| 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 ->
| Eq_mon_mon | Eq_dat_dat | Eq_dur_dur ),
_ ) as op ->
resolved op
type 'a no_overloads =
@ -371,22 +374,23 @@ type 'a no_overloads =
as
'a
let translate (t : 'a no_overloads t) : 'b no_overloads t =
let translate (t : 'a no_overloads t Mark.pos) : 'b no_overloads t Mark.pos =
match t with
| ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth | And
| Or | Xor | HandleDefault | HandleDefaultOpt | Log _ | Length | Eq | Map
| Map2 | Concat | Filter | Reduce | Fold | 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
| FromClosureEnv | ToClosureEnv ) as op ->
| ( ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth
| And | Or | Xor | HandleDefault | HandleDefaultOpt | Log _ | Length | Eq
| Map | Map2 | Concat | Filter | Reduce | Fold | 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 | FromClosureEnv | ToClosureEnv ),
_ ) as op ->
op
let monomorphic_type ((op : monomorphic t), pos) =
@ -537,8 +541,11 @@ let resolve_overload_aux (op : overloaded t) (operands : typ_lit list) :
_ ) ->
raise Not_found
let resolve_overload ctx (op : overloaded t Mark.pos) (operands : typ list) :
< resolved : yes ; .. > t * [ `Straight | `Reversed ] =
let resolve_overload
ctx
((op, pos) : overloaded t Mark.pos)
(operands : typ list) :
< resolved : yes ; .. > t Mark.pos * [ `Straight | `Reversed ] =
try
let operands =
List.map
@ -546,11 +553,12 @@ let resolve_overload ctx (op : overloaded t Mark.pos) (operands : typ list) :
match Mark.remove t with TLit tl -> tl | _ -> raise Not_found)
operands
in
resolve_overload_aux (Mark.remove op) operands
let op, direction = resolve_overload_aux op operands in
(op, pos), direction
with Not_found ->
Message.error
~extra_pos:
(("", Mark.get op)
(("", pos)
:: List.map
(fun ty ->
( Format.asprintf "Type %a coming from expression:"
@ -559,7 +567,7 @@ let resolve_overload ctx (op : overloaded t Mark.pos) (operands : typ list) :
operands)
"I don't know how to apply operator %a on types %a"
(Print.operator ~debug:true)
(Mark.remove op)
op
(Format.pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf " and@ ")
(Print.typ ctx))
@ -567,4 +575,4 @@ let resolve_overload ctx (op : overloaded t Mark.pos) (operands : typ list) :
let overload_type ctx (op : overloaded t Mark.pos) (operands : typ list) : typ =
let rop = fst (resolve_overload ctx op operands) in
resolved_type (Mark.copy op rop)
resolved_type rop

14
compiler/shared_ast/operator.mli
View File

@ -43,11 +43,11 @@ val name : 'a t -> string
symbols, e.g. [+$]. *)
val kind_dispatch :
polymorphic:(< polymorphic : yes ; .. > t -> 'b) ->
monomorphic:(< monomorphic : yes ; .. > t -> 'b) ->
?overloaded:(< overloaded : yes ; .. > t -> 'b) ->
?resolved:(< resolved : yes ; .. > t -> 'b) ->
'a t ->
polymorphic:(< polymorphic : yes ; .. > t Mark.pos -> 'b) ->
monomorphic:(< monomorphic : yes ; .. > t Mark.pos -> 'b) ->
?overloaded:(< overloaded : yes ; .. > t Mark.pos -> 'b) ->
?resolved:(< resolved : yes ; .. > t Mark.pos -> 'b) ->
'a t Mark.pos ->
'b
(** Calls one of the supplied functions depending on the kind of the operator *)
@ -60,7 +60,7 @@ type 'a no_overloads =
as
'a
val translate : 'a no_overloads t -> 'b no_overloads t
val translate : 'a no_overloads t Mark.pos -> 'b no_overloads t Mark.pos
(** An identity function that allows translating an operator between different
passes that don't change operator types *)
@ -84,7 +84,7 @@ val resolve_overload :
decl_ctx ->
overloaded t Mark.pos ->
typ list ->
< resolved : yes ; .. > t * [ `Straight | `Reversed ]
< resolved : yes ; .. > t Mark.pos * [ `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. *)

67
compiler/shared_ast/optimizations.ml
View File

@ -97,15 +97,15 @@ let rec optimize_expr :
the matches and the log calls are not preserved, which would be a good
property *)
match Mark.remove e with
| EAppOp { op = Not; args = [(ELit (LBool b), _)]; _ } ->
| EAppOp { op = Not, _; args = [(ELit (LBool b), _)]; _ } ->
(* reduction of logical not *)
ELit (LBool (not b))
| EAppOp { op = Or; args = [(ELit (LBool b), _); (e, _)]; _ }
| EAppOp { op = Or; args = [(e, _); (ELit (LBool b), _)]; _ } ->
| EAppOp { op = Or, _; args = [(ELit (LBool b), _); (e, _)]; _ }
| EAppOp { op = Or, _; args = [(e, _); (ELit (LBool b), _)]; _ } ->
(* reduction of logical or *)
if b then ELit (LBool true) else e
| EAppOp { op = And; args = [(ELit (LBool b), _); (e, _)]; _ }
| EAppOp { op = And; args = [(e, _); (ELit (LBool b), _)]; _ } ->
| EAppOp { op = And, _; args = [(ELit (LBool b), _); (e, _)]; _ }
| EAppOp { op = And, _; args = [(e, _); (ELit (LBool b), _)]; _ } ->
(* reduction of logical and *)
if b then e else ELit (LBool false)
| EMatch { e = EInj { e = e'; cons; name = n' }, _; cases; name = n }
@ -140,15 +140,12 @@ let rec optimize_expr :
match Mark.remove b1, Mark.remove e2 with
| EAbs { binder = b1; _ }, EAbs { binder = b2; tys } -> (
let v1, e1 = Bindlib.unmbind b1 in
let[@warning "-8"] [| v1 |] = v1 in
match Mark.remove e1 with
| EInj { e = e1; _ } ->
| EInj { e = e1, _; _ } ->
Some
(Expr.unbox
(Expr.make_abs [| v1 |]
(Expr.rebox
(Bindlib.msubst b2
([e1] |> List.map fst |> Array.of_list)))
(Expr.make_abs v1
(Expr.rebox (Bindlib.msubst b2 [| e1 |]))
tys (Expr.pos e2)))
| _ -> assert false)
| _ -> assert false)
@ -171,7 +168,7 @@ let rec optimize_expr :
| EDefault { excepts; just; cons } -> (
(* TODO: mechanically prove each of these optimizations correct *)
let excepts =
List.filter (fun except -> Mark.remove except <> EEmptyError) excepts
List.filter (fun except -> Mark.remove except <> EEmpty) excepts
(* we can discard the exceptions that are always empty error *)
in
let value_except_count =
@ -198,13 +195,13 @@ let rec optimize_expr :
Mark.remove cons
| ( [],
( ( ELit (LBool false)
| EAppOp { op = Log _; args = [(ELit (LBool false), _)]; _ } ),
| EAppOp { op = Log _, _; args = [(ELit (LBool false), _)]; _ } ),
_ ) ) ->
(* No exceptions and condition false *)
EEmptyError
EEmpty
| ( [except],
( ( ELit (LBool false)
| EAppOp { op = Log _; args = [(ELit (LBool false), _)]; _ } ),
| EAppOp { op = Log _, _; args = [(ELit (LBool false), _)]; _ } ),
_ ) ) ->
(* Single exception and condition false *)
Mark.remove except
@ -213,7 +210,7 @@ let rec optimize_expr :
{
cond =
( ELit (LBool true), _
| EAppOp { op = Log _; args = [(ELit (LBool true), _)]; _ }, _ );
| EAppOp { op = Log _, _; args = [(ELit (LBool true), _)]; _ }, _ );
etrue;
_;
} ->
@ -222,7 +219,7 @@ let rec optimize_expr :
{
cond =
( ( ELit (LBool false)
| EAppOp { op = Log _; args = [(ELit (LBool false), _)]; _ } ),
| EAppOp { op = Log _, _; args = [(ELit (LBool false), _)]; _ } ),
_ );
efalse;
_;
@ -233,32 +230,37 @@ let rec optimize_expr :
cond;
etrue =
( ( ELit (LBool btrue)
| EAppOp { op = Log _; args = [(ELit (LBool btrue), _)]; _ } ),
| EAppOp { op = Log _, _; args = [(ELit (LBool btrue), _)]; _ } ),
_ );
efalse =
( ( ELit (LBool bfalse)
| EAppOp { op = Log _; args = [(ELit (LBool bfalse), _)]; _ } ),
| EAppOp { op = Log _, _; args = [(ELit (LBool bfalse), _)]; _ }
),
_ );
} ->
if btrue && not bfalse then Mark.remove cond
else if (not btrue) && bfalse then
EAppOp
{ op = Not; tys = [TLit TBool, Expr.mark_pos mark]; args = [cond] }
{
op = Not, Expr.mark_pos mark;
tys = [TLit TBool, Expr.mark_pos mark];
args = [cond];
}
(* note: this last call eliminates the condition & might skip log calls
as well *)
else (* btrue = bfalse *) ELit (LBool btrue)
| EAppOp { op = Op.Fold; args = [_f; init; (EArray [], _)]; _ } ->
| EAppOp { op = Op.Fold, _; args = [_f; init; (EArray [], _)]; _ } ->
(*reduces a fold with an empty list *)
Mark.remove init
| EAppOp
{
op = Map;
op = (Map, _) as op;
args =
[
f1;
( EAppOp
{
op = Map;
op = Map, _;
args = [f2; ls];
tys = [_; ((TArray xty, _) as lsty)];
},
@ -286,7 +288,7 @@ let rec optimize_expr :
in
let fg = optimize_expr ctx (Expr.unbox fg) in
let mapl =
Expr.eappop ~op:Map
Expr.eappop ~op
~args:[fg; Expr.box ls]
~tys:[Expr.maybe_ty (Mark.get fg); lsty]
mark
@ -294,13 +296,13 @@ let rec optimize_expr :
Mark.remove (Expr.unbox mapl)
| EAppOp
{
op = Map;
op = Map, _;
args =
[
f1;
( EAppOp
{
op = Map2;
op = (Map2, _) as op;
args = [f2; ls1; ls2];
tys =
[
@ -339,7 +341,7 @@ let rec optimize_expr :
in
let fg = optimize_expr ctx (Expr.unbox fg) in
let mapl =
Expr.eappop ~op:Map2
Expr.eappop ~op
~args:[fg; Expr.box ls1; Expr.box ls2]
~tys:[Expr.maybe_ty (Mark.get fg); ls1ty; ls2ty]
mark
@ -347,7 +349,7 @@ let rec optimize_expr :
Mark.remove (Expr.unbox mapl)
| EAppOp
{
op = Op.Fold;
op = Op.Fold, _;
args = [f; init; (EArray [e'], _)];
tys = [_; tinit; (TArray tx, _)];
} ->
@ -363,13 +365,12 @@ let rec optimize_expr :
el) ->
(* identity tuple reconstruction *)
Mark.remove e
| ECatch { body; exn; handler } -> (
| ECatchEmpty { body; handler } -> (
(* peephole exception catching reductions *)
match Mark.remove body, Mark.remove handler with
| ERaise exn', ERaise exn'' when exn' = exn && exn = exn'' -> ERaise exn
| ERaise exn', _ when exn' = exn -> Mark.remove handler
| _, ERaise exn' when exn' = exn -> Mark.remove body
| _ -> ECatch { body; exn; handler })
| ERaiseEmpty, _ -> Mark.remove handler
| _, ERaiseEmpty -> Mark.remove body
| _ -> ECatchEmpty { body; handler })
| e -> e
in
Expr.Box.app1 e reduce mark

61
compiler/shared_ast/print.ml
View File

@ -345,13 +345,8 @@ let operator : type a. ?debug:bool -> Format.formatter -> a operator -> unit =
op_style fmt
(if debug then operator_to_string op else operator_to_shorter_string op)
let except (fmt : Format.formatter) (exn : except) : unit =
op_style fmt
(match exn with
| EmptyError -> "EmptyError"
| ConflictError _ -> "ConflictError"
| Crash s -> Printf.sprintf "Crash %S" s
| NoValueProvided -> "NoValueProvided")
let runtime_error ppf err =
Format.fprintf ppf "@{<red>%s@}" (Runtime.error_to_string err)
let var_debug fmt v =
Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
@ -375,7 +370,7 @@ module Precedence = struct
match Mark.remove e with
| ELit _ -> Contained (* Todo: unop if < 0 *)
| EAppOp { op; _ } -> (
match op with
match Mark.remove op with
| Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth
| Length | Log _ | Minus | Minus_int | Minus_rat | Minus_mon | Minus_dur
| ToRat | ToRat_int | ToRat_mon | ToMoney | ToMoney_rat | Round
@ -426,12 +421,13 @@ module Precedence = struct
| EDStructAmend _ -> App
| EDStructAccess _ | EStructAccess _ -> Dot
| EAssert _ -> App
| EFatalError _ -> App
| EDefault _ -> Contained
| EPureDefault _ -> Contained
| EEmptyError -> Contained
| EEmpty -> Contained
| EErrorOnEmpty _ -> App
| ERaise _ -> App
| ECatch _ -> App
| ERaiseEmpty -> App
| ECatchEmpty _ -> App
| ECustom _ -> Contained
let needs_parens ~context ?(rhs = false) e =
@ -575,16 +571,16 @@ module ExprGen (C : EXPR_PARAM) = struct
Format.pp_close_box fmt ();
punctuation fmt ")"))
xs_tau punctuation "→" (rhs expr) body
| EAppOp { op = (Map | Filter) as op; args = [arg1; arg2]; _ } ->
| EAppOp { op = ((Map | Filter) as op), _; args = [arg1; arg2]; _ } ->
Format.fprintf fmt "@[<hv 2>%a %a@ %a@]" operator op (lhs exprc) arg1
(rhs exprc) arg2
| EAppOp { op = Log _ as op; args = [arg1]; _ } ->
| EAppOp { op = (Log _ as op), _; args = [arg1]; _ } ->
Format.fprintf fmt "@[<hv 0>%a@ %a@]" operator op (rhs exprc) arg1
| EAppOp { op = op0; args = [_; _]; _ } ->
| EAppOp { op = op0, _; args = [_; _]; _ } ->
let prec = Precedence.expr e in
let rec pr colors fmt = function
(* Flatten sequences of the same associative op *)
| EAppOp { op; args = [arg1; arg2]; _ }, _ when op = op0 -> (
| EAppOp { op = op, _; args = [arg1; arg2]; _ }, _ when op = op0 -> (
(match prec with
| Op (And | Or | Mul | Add | Div | Sub) -> lhs pr fmt arg1
| _ -> lhs exprc fmt arg1);
@ -599,9 +595,9 @@ module ExprGen (C : EXPR_PARAM) = struct
Format.pp_open_hvbox fmt 0;
pr colors fmt e;
Format.pp_close_box fmt ()
| EAppOp { op; args = [arg1]; _ } ->
| EAppOp { op = op, _; args = [arg1]; _ } ->
Format.fprintf fmt "@[<hv 2>%a@ %a@]" operator op (rhs exprc) arg1
| EAppOp { op; args; _ } ->
| EAppOp { op = op, _; args; _ } ->
Format.fprintf fmt "@[<hv 2>%a@ %a@]" operator op
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
@ -665,19 +661,22 @@ module ExprGen (C : EXPR_PARAM) = struct
"⟨" expr e
(default_punct (List.hd colors))
"⟩"
| EEmptyError -> lit_style fmt "∅"
| EEmpty -> lit_style fmt "∅"
| EErrorOnEmpty e' ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" op_style "error_empty"
(rhs exprc) e'
| EAssert e' ->
Format.fprintf fmt "@[<hov 2>%a@ %a%a%a@]" keyword "assert" punctuation
"(" (rhs exprc) e' punctuation ")"
| ECatch { body; exn; handler } ->
| EFatalError err ->
Format.fprintf fmt "@[<hov 2>%a@ @{<red>%s@}@]" keyword "error"
(Runtime.error_to_string err)
| ECatchEmpty { body; handler } ->
Format.fprintf fmt
"@[<hv 0>@[<hov 2>%a@ %a@]@ @[<hov 2>%a@ %a ->@ %a@]@]" keyword "try"
expr body keyword "with" except exn (rhs exprc) handler
| ERaise exn ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" keyword "raise" except exn
expr body keyword "with" op_style "Empty" (rhs exprc) handler
| ERaiseEmpty ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" keyword "raise" op_style "Empty"
| ELocation loc -> location fmt loc
| EDStructAccess { e; field; _ } ->
Format.fprintf fmt "@[<hv 2>%a%a@,%a%a%a@]" (lhs exprc) e punctuation
@ -762,7 +761,7 @@ module ExprConciseParam = struct
let lit = lit
let rec pre_map : type a. (a, 't) gexpr -> (a, 't) gexpr = function
| EAppOp { op = Log _; args = [e]; _ }, _ -> pre_map e
| EAppOp { op = Log _, _; args = [e]; _ }, _ -> pre_map e
| e -> e
end
@ -952,8 +951,8 @@ let program ?(debug = false) fmt p =
(* This function is re-exported from module [Expr], but defined here where it's
first needed *)
let rec skip_wrappers : type a. (a, 'm) gexpr -> (a, 'm) gexpr = function
| EAppOp { op = Log _; args = [e]; tys = _ }, _ -> skip_wrappers e
| EApp { f = EAppOp { op = Log _; args = [f]; _ }, _; args; tys }, m ->
| EAppOp { op = Log _, _; args = [e]; tys = _ }, _ -> skip_wrappers e
| EApp { f = EAppOp { op = Log _, _; args = [f]; _ }, _; args; tys }, m ->
skip_wrappers (EApp { f; args; tys }, m)
| EErrorOnEmpty e, _ -> skip_wrappers e
| EDefault { excepts = []; just = ELit (LBool true), _; cons = e }, _ ->
@ -1052,13 +1051,13 @@ module UserFacing = struct
and some others not, adding confusion. *)
let date (lang : Global.backend_lang) ppf d =
let y, m, d = Dates_calc.Dates.date_to_ymd d in
let y, m, d = Runtime.date_to_years_months_days d in
match lang with
| En | Pl -> Format.fprintf ppf "%04d-%02d-%02d" y m d
| Fr -> Format.fprintf ppf "%02d/%02d/%04d" d m y
let duration (lang : Global.backend_lang) ppf dr =
let y, m, d = Dates_calc.Dates.period_to_ymds dr in
let y, m, d = Runtime.duration_to_years_months_days dr in
let rec filter0 = function
| (0, _) :: (_ :: _ as r) -> filter0 r
| x :: r -> x :: List.filter (fun (n, _) -> n <> 0) r
@ -1130,12 +1129,12 @@ module UserFacing = struct
| EInj { name = _; cons; e } ->
Format.fprintf ppf "@[<hov 2>%a@ %a@]" EnumConstructor.format cons
(value ~fallback lang) e
| EEmptyError -> Format.pp_print_string ppf "ø"
| EEmpty -> Format.pp_print_string ppf "ø"
| EAbs _ -> Format.pp_print_string ppf "<function>"
| EExternal _ -> Format.pp_print_string ppf "<external>"
| EApp _ | EAppOp _ | EVar _ | EIfThenElse _ | EMatch _ | ETupleAccess _
| EStructAccess _ | EAssert _ | EDefault _ | EPureDefault _
| EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EScopeCall _
| EStructAccess _ | EAssert _ | EFatalError _ | EDefault _ | EPureDefault _
| EErrorOnEmpty _ | ERaiseEmpty | ECatchEmpty _ | ELocation _ | EScopeCall _
| EDStructAmend _ | EDStructAccess _ | ECustom _ ->
fallback ppf e
@ -1150,7 +1149,7 @@ module UserFacing = struct
let bypass : type a t. Format.formatter -> (a, t) gexpr -> bool =
fun ppf e ->
match Mark.remove e with
| EArray _ | ETuple _ | EStruct _ | EInj _ | EEmptyError | EAbs _
| EArray _ | ETuple _ | EStruct _ | EInj _ | EEmpty | EAbs _
| EExternal _ ->
aux_value ppf e;
true

2
compiler/shared_ast/print.mli
View File

@ -47,7 +47,7 @@ val typ : decl_ctx -> Format.formatter -> typ -> unit
val lit : Format.formatter -> lit -> unit
val operator : ?debug:bool -> Format.formatter -> 'a operator -> unit
val log_entry : Format.formatter -> log_entry -> unit
val except : Format.formatter -> except -> unit
val runtime_error : Format.formatter -> Runtime.error -> unit
val var : Format.formatter -> 'e Var.t -> unit
val var_debug : Format.formatter -> 'e Var.t -> unit

36
compiler/shared_ast/typing.ml
View File

@ -354,13 +354,11 @@ let polymorphic_op_return_type
let resolve_overload_ret_type
~flags
(ctx : A.decl_ctx)
e
(op : Operator.overloaded A.operator)
_e
(op : Operator.overloaded A.operator Mark.pos)
tys : unionfind_typ =
let op_ty =
Operator.overload_type ctx
(Mark.add (Expr.pos e) op)
(List.map (typ_to_ast ~flags) tys)
Operator.overload_type ctx op (List.map (typ_to_ast ~flags) tys)
in
ast_to_typ (Type.arrow_return op_ty)
@ -754,11 +752,11 @@ and typecheck_expr_top_down :
args
in
Expr.escopecall ~scope ~args:args' mark
| A.ERaise ex -> Expr.eraise ex context_mark
| A.ECatch { body; exn; handler } ->
| A.ERaiseEmpty -> Expr.eraiseempty context_mark
| A.ECatchEmpty { body; handler } ->
let body' = typecheck_expr_top_down ctx env tau body in
let handler' = typecheck_expr_top_down ctx env tau handler in
Expr.ecatch body' exn handler' context_mark
Expr.ecatchempty body' handler' context_mark
| A.EVar v ->
let tau' =
match Env.get env v with
@ -887,17 +885,14 @@ and typecheck_expr_top_down :
let t_args = List.map ast_to_typ tys in
let t_func = unionfind (TArrow (t_args, tau)) in
let args =
Operator.kind_dispatch op
Operator.kind_dispatch (Mark.set pos_e op)
~polymorphic:(fun op ->
(* Type the operator first, then right-to-left: polymorphic operators
are required to allow the resolution of all type variables this
way *)
if not env.flags.assume_op_types then
unify ctx e (polymorphic_op_type (Mark.add pos_e op)) t_func
else
unify ctx e
(polymorphic_op_return_type ctx e (Mark.add pos_e op) t_args)
tau;
unify ctx e (polymorphic_op_type op) t_func
else unify ctx e (polymorphic_op_return_type ctx e op t_args) tau;
List.rev_map2
(typecheck_expr_top_down ctx env)
(List.rev t_args) (List.rev args))
@ -908,15 +903,11 @@ and typecheck_expr_top_down :
args')
~monomorphic:(fun op ->
(* Here it doesn't matter but may affect the error messages *)
unify ctx e
(ast_to_typ (Operator.monomorphic_type (Mark.add pos_e op)))
t_func;
unify ctx e (ast_to_typ (Operator.monomorphic_type op)) t_func;
List.map2 (typecheck_expr_top_down ctx env) t_args args)
~resolved:(fun op ->
(* This case should not fail *)
unify ctx e
(ast_to_typ (Operator.resolved_type (Mark.add pos_e op)))
t_func;
unify ctx e (ast_to_typ (Operator.resolved_type op)) t_func;
List.map2 (typecheck_expr_top_down ctx env) t_args args)
in
(* All operator applications are monomorphised at this point *)
@ -949,8 +940,9 @@ and typecheck_expr_top_down :
typecheck_expr_top_down ctx env (unionfind ~pos:e1 (TLit TBool)) e1
in
Expr.eassert e1' mark
| A.EEmptyError ->
Expr.eemptyerror (ty_mark (TDefault (unionfind (TAny (Any.fresh ())))))
| A.EFatalError err -> Expr.efatalerror err context_mark
| A.EEmpty ->
Expr.eempty (ty_mark (TDefault (unionfind (TAny (Any.fresh ())))))
| A.EErrorOnEmpty e1 ->
let tau' = unionfind (TDefault tau) in
let e1' = typecheck_expr_top_down ctx env tau' e1 in

4
compiler/surface/ast.ml
View File

@ -145,6 +145,7 @@ and literal =
| LDate of literal_date
and collection_op =
| Member of { element : expression }
| Exists of { predicate : lident Mark.pos list * expression }
| Forall of { predicate : lident Mark.pos list * expression }
| Map of { f : lident Mark.pos list * expression }
@ -175,8 +176,7 @@ and naked_expression =
| IfThenElse of expression * expression * expression
| Binop of binop Mark.pos * expression * expression
| Unop of unop Mark.pos * expression
| CollectionOp of collection_op * expression
| MemCollection of expression * expression
| CollectionOp of collection_op Mark.pos * expression
| TestMatchCase of expression * match_case_pattern Mark.pos
| FunCall of expression * expression list
| ScopeCall of

1
compiler/surface/dune
View File

@ -8,7 +8,6 @@
re
zarith
zarith_stubs_js
dates_calc
shared_ast)
(preprocess
(pps sedlex.ppx visitors.ppx)))

43
compiler/surface/parser.mly
View File

@ -232,25 +232,26 @@ let naked_expression ==
RBRACE ; {
StructReplace (e, fields)
}
| e1 = expression ;
CONTAINS ;
e2 = expression ; {
MemCollection (e2, e1)
| coll = expression ;
pos = pos(CONTAINS) ;
element = expression ; {
CollectionOp ((Member { element }, pos), coll)
} %prec apply
| SUM ; typ = addpos(primitive_typ) ;
| pos = pos(SUM) ; typ = addpos(primitive_typ) ;
OF ; coll = expression ; {
CollectionOp (AggregateSum { typ = Mark.remove typ }, coll)
CollectionOp ((AggregateSum { typ = Mark.remove typ }, pos), coll)
} %prec apply
| f = expression ;
FOR ; i = mbinder ;
pos = pos(FOR) ; i = mbinder ;
AMONG ; coll = expression ; {
CollectionOp (Map {f = i, f}, coll)
CollectionOp ((Map {f = i, f}, pos), coll)
} %prec apply
| max = minmax ;
| maxp = addpos(minmax) ;
OF ; coll = expression ;
OR ; IF ; LIST_EMPTY ; THEN ;
default = expression ; {
CollectionOp (AggregateExtremum { max; default }, coll)
let max, pos = maxp in
CollectionOp ((AggregateExtremum { max; default }, pos), coll)
} %prec apply
| op = addpos(unop) ; e = expression ; {
Unop (op, e)
@ -260,15 +261,15 @@ let naked_expression ==
e2 = expression ; {
Binop (binop, e1, e2)
}
| EXISTS ; i = mbinder ;
| pos = pos(EXISTS) ; i = mbinder ;
AMONG ; coll = expression ;
SUCH ; THAT ; predicate = expression ; {
CollectionOp (Exists {predicate = i, predicate}, coll)
CollectionOp ((Exists {predicate = i, predicate}, pos), coll)
} %prec let_expr
| FOR ; ALL ; i = mbinder ;
| pos = pos(FOR) ; ALL ; i = mbinder ;
AMONG ; coll = expression ;
WE_HAVE ; predicate = expression ; {
CollectionOp (Forall {predicate = i, predicate}, coll)
CollectionOp ((Forall {predicate = i, predicate}, pos), coll)
} %prec let_expr
| MATCH ; e = expression ;
WITH ;
@ -285,23 +286,23 @@ let naked_expression ==
IN ; e2 = expression ; {
LetIn (ids, e1, e2)
} %prec let_expr
| LIST; ids = mbinder ;
| pos = pos(LIST); ids = mbinder ;
AMONG ; coll = expression ;
SUCH ; THAT ; f = expression ; {
CollectionOp (Filter {f = ids, f}, coll)
CollectionOp ((Filter {f = ids, f}, pos), coll)
} %prec top_expr
| fmap = expression ;
FOR ; i = mbinder ;
pfor = pos(FOR) ; i = mbinder ;
AMONG ; coll = expression ;
SUCH ; THAT ; ffilt = expression ; {
CollectionOp (Map {f = i, fmap}, (CollectionOp (Filter {f = i, ffilt}, coll), Pos.from_lpos $loc))
psuch = pos(SUCH) ; THAT ; ffilt = expression ; {
CollectionOp ((Map {f = i, fmap}, pfor), (CollectionOp ((Filter {f = i, ffilt}, psuch), coll), Pos.from_lpos $loc))
} %prec top_expr
| CONTENT; OF; ids = mbinder ;
| pos = pos(CONTENT); OF; ids = mbinder ;
AMONG ; coll = expression ;
SUCH ; THAT ; f = expression ;
IS ; max = minmax ;
OR ; IF ; LIST_EMPTY ; THEN ; default = expression ; {
CollectionOp (AggregateArgExtremum { max; default; f = ids, f }, coll)
CollectionOp ((AggregateArgExtremum { max; default; f = ids, f }, pos), coll)
} %prec top_expr

18
compiler/verification/conditions.ml
View File

@ -40,7 +40,7 @@ let rec conjunction_exprs (exprs : typed expr list) (mark : typed mark) :
| hd :: tl ->
( EAppOp
{
op = And;
op = And, Expr.mark_pos mark;
tys = [TLit TBool, Expr.pos hd; TLit TBool, Expr.pos hd];
args = [hd; conjunction_exprs tl mark];
},
@ -54,7 +54,7 @@ let conjunction (args : vc_return list) (mark : typed mark) : vc_return =
(fun acc arg ->
( EAppOp
{
op = And;
op = And, Expr.mark_pos mark;
tys = [TLit TBool, Expr.pos acc; TLit TBool, Expr.pos arg];
args = [arg; acc];
},
@ -62,7 +62,13 @@ let conjunction (args : vc_return list) (mark : typed mark) : vc_return =
acc list
let negation (arg : vc_return) (mark : typed mark) : vc_return =
EAppOp { op = Not; tys = [TLit TBool, Expr.pos arg]; args = [arg] }, mark
( EAppOp
{
op = Not, Expr.mark_pos mark;
tys = [TLit TBool, Expr.pos arg];
args = [arg];
},
mark )
let disjunction (args : vc_return list) (mark : typed mark) : vc_return =
let acc, list =
@ -72,7 +78,7 @@ let disjunction (args : vc_return list) (mark : typed mark) : vc_return =
(fun (acc : vc_return) arg ->
( EAppOp
{
op = Or;
op = Or, Expr.mark_pos mark;
tys = [TLit TBool, Expr.pos acc; TLit TBool, Expr.pos arg];
args = [arg; acc];
},
@ -171,7 +177,7 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) :
(Mark.get e);
])
(Mark.get e)
| EEmptyError -> Mark.copy e (ELit (LBool false))
| EEmpty -> Mark.copy e (ELit (LBool false))
| EVar _
(* Per default calculus semantics, you cannot call a function with an argument
that evaluates to the empty error. Thus, all variable evaluate to
@ -202,7 +208,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 Mark.remove body with
| EEmptyError -> Mark.copy field (ELit (LBool true))
| EEmpty -> Mark.copy field (ELit (LBool true))
| _ ->
(* same as basic [EAbs case]*)
generate_vc_must_not_return_empty ctx field)

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

@ -19,7 +19,7 @@ open Shared_ast
open Dcalc
open Ast
open Z3
module StringMap : Map.S with type key = String.t = Map.Make (String)
module StringMap = String.Map
module Runtime = Runtime_ocaml.Runtime
type context = {
@ -432,15 +432,15 @@ 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 :
context -> dcalc operator -> 'm expr list -> context * Expr.expr =
fun ctx op args ->
context -> dcalc operator Mark.pos -> 'm expr list -> context * Expr.expr =
fun ctx (op, pos) args ->
let ill_formed () =
Format.kasprintf failwith
"[Z3 encoding] Ill-formed operator application: %a" Shared_ast.Expr.format
(Shared_ast.Expr.eappop ~op
(Shared_ast.Expr.eappop ~op:(op, pos)
~args:(List.map Shared_ast.Expr.untype args)
~tys:[]
(Untyped { pos = Pos.no_pos })
(Untyped { pos })
|> Shared_ast.Expr.unbox)
in
let app f =
@ -458,7 +458,7 @@ let rec translate_op :
failwith "[Z3 encoding] ternary operator application not supported"
(* Special case for GetYear comparisons *)
| ( Lt_int_int,
[(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
[(EAppOp { op = GetYear, _; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let e2 =
@ -469,7 +469,7 @@ let rec translate_op :
days *)
ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2
| ( Lte_int_int,
[(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
[(EAppOp { op = GetYear, _; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
let ctx, e1 = translate_expr ctx e1 in
let nb_days = if is_leap_year n then 365 else 364 in
let n = Runtime.integer_to_int n in
@ -483,7 +483,7 @@ let rec translate_op :
in
ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2
| ( Gt_int_int,
[(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
[(EAppOp { op = GetYear, _; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
let ctx, e1 = translate_expr ctx e1 in
let nb_days = if is_leap_year n then 365 else 364 in
let n = Runtime.integer_to_int n in
@ -497,7 +497,7 @@ let rec translate_op :
in
ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2
| ( Gte_int_int,
[(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
[(EAppOp { op = GetYear, _; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let e2 =
@ -507,7 +507,7 @@ let rec translate_op :
be directly translated as >= in the Z3 encoding using the number of
days *)
ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2
| Eq, [(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ->
| Eq, [(EAppOp { op = GetYear, _; args = [e1]; _ }, _); (ELit (LInt n), _)] ->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let min_date =
@ -746,6 +746,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
"[Z3 encoding] EApp node: Catala function calls should only include \
operators or function names")
| EAssert e -> translate_expr ctx e
| EFatalError _ -> failwith "[Z3 encoding] EFatalError unsupported"
| EDefault _ -> failwith "[Z3 encoding] EDefault unsupported"
| EPureDefault _ -> failwith "[Z3 encoding] EPureDefault unsupported"
| EIfThenElse { cond = e_if; etrue = e_then; efalse = e_else } ->
@ -756,7 +757,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
let ctx, z3_then = translate_expr ctx e_then in
let ctx, z3_else = translate_expr ctx e_else in
ctx, Boolean.mk_ite ctx.ctx_z3 z3_if z3_then z3_else
| EEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
| EEmpty -> failwith "[Z3 encoding] 'Empty' literals not supported"
| EErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"
| _ -> .

15
doc/syntax/syntax_en.catala_en
View File

@ -65,9 +65,8 @@ declaration x content integer equals
round of $9.99
) in
let x equals (
get_day of 0,
get_month of 0,
get_year of 0
get_month of |2003-01-02|,
first_day_of_month of |2003-01-02|
) in
let x equals (
a +! b, # integer
@ -214,17 +213,17 @@ declaration x content integer equals
for all x among lst we have x > 2
in
let x equals
x + 2 for x among lst
(x + 2) for x among lst
in
let x equals
list of x among lst such that x > 2
in
let x equals
x - 2 for x among lst
(x - 2) for x among lst
such that x > 2
in
let x equals
x + y for (x, y) among (lst1, lst2)
(x + y) for (x, y) among (lst1, lst2)
in
let x equals
lst1 ++ lst2
@ -255,9 +254,9 @@ to ensure that the *syntax* is correct.
$ catala typecheck
[ERROR] No scope named Scope0 found
┌─⯈ doc/syntax/syntax_en.catala_en:95.14-95.20:
┌─⯈ doc/syntax/syntax_en.catala_en:94.14-94.20:
└──┐
95 │ sub1 scope Scope0
94 │ sub1 scope Scope0
│ ‾‾‾‾‾‾
└─ Metadata declaration
#return code 123#

10
doc/syntax/syntax_en.tex
View File

@ -378,8 +378,8 @@
\\
\begin{catala}
```catala
get_day of ... get_month of ...
get_year of ...
get_month of ...
first_day_of_month of ...
```
\end{catala}
& Date parts
@ -674,7 +674,7 @@
\\
\begin{catala}
```catala
x + 2 for x among lst
(x + 2) for x among lst
```
\end{catala}
& Mapping
@ -688,7 +688,7 @@
\\
\begin{catala}
```catala
x - 2 for x among lst
(x - 2) for x among lst
such that x > 2
```
\end{catala}
@ -696,7 +696,7 @@
\\
\begin{catala}
```catala
x + y for (x, y) among (lst1, lst2)
(x + y) for (x, y) among (lst1, lst2)
```
\end{catala}
& Multiple mapping

15
doc/syntax/syntax_fr.catala_fr
View File

@ -63,9 +63,8 @@ déclaration x contenu entier égal à
arrondi de 9,99€
) dans
soit x égal à (
accès_jour de 0 ,
accès_mois de 0 ,
accès_année de 0
accès_année de |2003-01-02|,
premier_jour_du_mois de |2003-01-02|
) dans
soit x égal à (
a +! b, # entier
@ -212,17 +211,17 @@ déclaration x contenu entier égal à
pour tout x parmi lst on a x >= 2
dans
soit x égal à
x + 2 pour x parmi lst
(x + 2) pour x parmi lst
dans
soit x égal à
liste de x parmi lst tel que x > 2
dans
soit x égal à
x - 2 pour x parmi lst
(x - 2) pour x parmi lst
tel que x > 2
dans
soit x égal à
x + y pour (x, y) parmi (lst1, lst2)
(x + y) pour (x, y) parmi (lst1, lst2)
dans
soit x égal à
lst1 ++ lst2
@ -253,9 +252,9 @@ to ensure that the *syntax* is correct.
$ catala typecheck
[ERROR] No scope named Scope0 found
┌─⯈ doc/syntax/syntax_fr.catala_fr:93.28-93.34:
┌─⯈ doc/syntax/syntax_fr.catala_fr:92.28-92.34:
└──┐
93 │ sub1 champ d'application Scope0
92 │ sub1 champ d'application Scope0
│ ‾‾‾‾‾‾
└─ Déclaration des métadonnées
#return code 123#

8
doc/syntax/syntax_fr.tex
View File

@ -380,8 +380,8 @@
\\
\begin{catala}
```catala
accès_jour de ... accès_mois de ...
accès_année de ...
premier_jour_du_mois de ...
```
\end{catala}
& Éléments de dates
@ -679,7 +679,7 @@
\\
\begin{catala}
```catala
x + 2 pour x parmi lst
(x + 2) pour x parmi lst
```
\end{catala}
& Application un-à-un
@ -693,7 +693,7 @@
\\
\begin{catala}
```catala
x - 2 pour x parmi lst
(x - 2) pour x parmi lst
tel que x > 2
```
\end{catala}
@ -701,7 +701,7 @@
\\
\begin{catala}
```catala
x + y pour (x, y) parmi (lst1, lst2)
(x + y) pour (x, y) parmi (lst1, lst2)
```
\end{catala}
& Multiple mapping

10
runtimes/c/runtime.c
View File

@ -4,11 +4,13 @@
typedef enum catala_fatal_error_code
{
catala_no_value_provided,
catala_assertion_failed,
catala_no_value,
catala_conflict,
catala_crash,
catala_empty,
catala_assertion_failure,
catala_division_by_zero,
catala_not_same_length,
catala_uncomparable_durations,
catala_indivisible_durations,
catala_malloc_error,
} catala_fatal_error_code;

27
runtimes/jsoo/runtime.ml
View File

@ -60,11 +60,14 @@ let date_of_js d =
if String.contains d 'T' then d |> String.split_on_char 'T' |> List.hd
else d
in
let fail () = failwith "date_of_js: invalid date" in
match String.split_on_char '-' d with
| [year; month; day] ->
| [year; month; day] -> (
try
R_ocaml.date_of_numbers (int_of_string year) (int_of_string month)
(int_of_string day)
| _ -> failwith "date_of_js: invalid date"
with Failure _ -> fail ())
| _ -> fail ()
let date_to_js d = Js.string @@ R_ocaml.date_to_string d
@ -147,13 +150,9 @@ let event_manager : event_manager Js.t =
end
let execute_or_throw_error f =
let throw_error (descr : string) (pos : R_ocaml.source_position) =
let msg =
Js.string
(Format.asprintf "%s in file %s, position %d:%d--%d:%d." descr
pos.filename pos.start_line pos.start_column pos.end_line
pos.end_column)
in
try f ()
with R_ocaml.Error _ as exc ->
let msg = Js.string (Printexc.to_string exc) in
Js.Js_error.raise_
(Js.Js_error.of_error
(object%js
@ -162,16 +161,6 @@ let execute_or_throw_error f =
val mutable stack = Js.Optdef.empty
method toString = msg
end))
in
try f () with
| R_ocaml.NoValueProvided pos ->
throw_error
"No rule applies in the given context to give a value to the variable" pos
| R_ocaml.ConflictError pos ->
throw_error
"A conflict happened between two rules giving a value to the variable" pos
| R_ocaml.AssertionFailed pos ->
throw_error "A failure happened in the assertion" pos
let () =
Js.export_all

186
runtimes/ocaml/runtime.ml
View File

@ -45,35 +45,54 @@ type source_position = {
law_headings : string list;
}
exception EmptyError
exception AssertionFailed of source_position
exception ConflictError of source_position
exception UncomparableDurations
exception IndivisibleDurations
exception ImpossibleDate
exception NoValueProvided of source_position
exception NotSameLength
exception Division_by_zero (* Shadows the stdlib definition *)
type error =
| AssertionFailed
| NoValue
| Conflict
| DivisionByZero
| NotSameLength
| UncomparableDurations
| IndivisibleDurations
(* Register exceptions printers *)
let error_to_string = function
| AssertionFailed -> "AssertionFailed"
| NoValue -> "NoValue"
| Conflict -> "Conflict"
| DivisionByZero -> "DivisionByZero"
| NotSameLength -> "NotSameLength"
| UncomparableDurations -> "UncomparableDurations"
| IndivisibleDurations -> "IndivisibleDurations"
let error_message = function
| AssertionFailed -> "an assertion doesn't hold"
| NoValue -> "no applicable rule to define this variable in this situation"
| Conflict ->
"conflict between multiple valid consequences for assigning the same \
variable"
| DivisionByZero ->
"a value is being used as denominator in a division and it computed to zero"
| NotSameLength -> "traversing multiple lists of different lengths"
| UncomparableDurations ->
"ambiguous comparison between durations in different units (e.g. months \
vs. days)"
| IndivisibleDurations -> "dividing durations that are not in days"
exception Error of error * source_position list
exception Empty
let error err pos = raise (Error (err, pos))
(* Register (fallback) exception printers *)
let () =
let pos () p =
let ppos () p =
Printf.sprintf "%s:%d.%d-%d.%d" p.filename p.start_line p.start_column
p.end_line p.end_column
in
let pr fmt = Printf.ksprintf (fun s -> Some s) fmt in
let pposl () pl = String.concat ", " (List.map (ppos ()) pl) in
Printexc.register_printer
@@ function
| EmptyError -> pr "A variable couldn't be resolved"
| AssertionFailed p -> pr "At %a: Assertion failed" pos p
| ConflictError p -> pr "At %a: Conflicting exceptions" pos p
| UncomparableDurations -> pr "Ambiguous comparison between durations"
| IndivisibleDurations -> pr "Ambiguous division between durations"
| ImpossibleDate -> pr "Invalid date"
| NoValueProvided p ->
pr "At %a: No definition applied to this variable" pos p
| NotSameLength -> pr "Attempt to traverse lists of different lengths"
| Division_by_zero -> pr "Division by zero"
| Error (err, pos) ->
Some (Printf.sprintf "At %a: %s" pposl pos (error_message err))
| _ -> None
let () =
@ -81,6 +100,9 @@ let () =
@@ fun exc bt ->
Printf.eprintf "[ERROR] %s\n%!" (Printexc.to_string exc);
if Printexc.backtrace_status () then Printexc.print_raw_backtrace stderr bt
(* TODO: the backtrace will point to the OCaml code; but we could make it point
to the Catala code if we add #line directives everywhere in the generated
code. *)
let round (q : Q.t) : Z.t =
(* The mathematical formula is [round(q) = sgn(q) * floor(abs(q) + 0.5)].
@ -185,13 +207,19 @@ let day_of_month_of_date (d : date) : integer =
let _, _, d = Dates_calc.Dates.date_to_ymd d in
Z.of_int d
(* This could fail, but is expected to only be called with known, already
validated arguments by the generated code *)
let date_of_numbers (year : int) (month : int) (day : int) : date =
try Dates_calc.Dates.make_date ~year ~month ~day
with _ -> raise ImpossibleDate
with Dates_calc.Dates.InvalidDate ->
failwith "date_of_numbers: invalid date"
let date_to_string (d : date) : string =
Format.asprintf "%a" Dates_calc.Dates.format_date d
let date_to_years_months_days (d : date) : int * int * int =
Dates_calc.Dates.date_to_ymd d
let first_day_of_month = Dates_calc.Dates.first_day_of_month
let last_day_of_month = Dates_calc.Dates.last_day_of_month
@ -200,19 +228,6 @@ let duration_of_numbers (year : int) (month : int) (day : int) : duration =
let duration_to_string (d : duration) : string =
Format.asprintf "%a" Dates_calc.Dates.format_period d
(* breaks previous format *)
(* let x, y, z = CalendarLib.Date.Period.ymd d in
* let to_print =
* List.filter (fun (a, _) -> a <> 0) [x, "years"; y, "months"; z, "days"]
* in
* match to_print with
* | [] -> "empty duration"
* | _ ->
* Format.asprintf "%a"
* (Format.pp_print_list
* ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
* (fun fmt (d, l) -> Format.fprintf fmt "%d %s" d l))
* to_print *)
let duration_to_years_months_days (d : duration) : int * int * int =
Dates_calc.Dates.period_to_ymds d
@ -703,61 +718,60 @@ end
let handle_default :
'a.
source_position ->
source_position array ->
(unit -> 'a) array ->
(unit -> bool) ->
(unit -> 'a) ->
'a =
fun pos exceptions just cons ->
let except =
Array.fold_left
(fun acc except ->
let new_val = try Some (except ()) with EmptyError -> None in
match acc, new_val with
| None, _ -> new_val
| Some _, None -> acc
| Some _, Some _ -> raise (ConflictError pos))
None exceptions
let len = Array.length exceptions in
let rec filt_except i =
if i < len then
match exceptions.(i) () with
| new_val -> (new_val, i) :: filt_except (i + 1)
| exception Empty -> filt_except (i + 1)
else []
in
match except with
| Some x -> x
| None -> if just () then cons () else raise EmptyError
match filt_except 0 with
| [] -> if just () then cons () else raise Empty
| [(res, _)] -> res
| res -> error Conflict (List.map (fun (_, i) -> pos.(i)) res)
let handle_default_opt
(pos : source_position)
(pos : source_position array)
(exceptions : 'a Eoption.t array)
(just : unit -> bool)
(cons : unit -> 'a Eoption.t) : 'a Eoption.t =
let except =
Array.fold_left
(fun acc except ->
match acc, except with
| Eoption.ENone _, _ -> except
| Eoption.ESome _, Eoption.ENone _ -> acc
| Eoption.ESome _, Eoption.ESome _ -> raise (ConflictError pos))
(Eoption.ENone ()) exceptions
let len = Array.length exceptions in
let rec filt_except i =
if i < len then
match exceptions.(i) with
| Eoption.ESome _ as new_val -> (new_val, i) :: filt_except (i + 1)
| Eoption.ENone () -> filt_except (i + 1)
else []
in
match except with
| Eoption.ESome _ -> except
| Eoption.ENone _ -> if just () then cons () else Eoption.ENone ()
let no_input : unit -> 'a = fun _ -> raise EmptyError
match filt_except 0 with
| [] -> if just () then cons () else Eoption.ENone ()
| [(res, _)] -> res
| res -> error Conflict (List.map (fun (_, i) -> pos.(i)) res)
(* TODO: add a compare built-in to dates_calc. At the moment this fails on e.g.
[3 months, 4 months] *)
let compare_periods (p1 : duration) (p2 : duration) : int =
let compare_periods pos (p1 : duration) (p2 : duration) : int =
try
let p1_days = Dates_calc.Dates.period_to_days p1 in
let p2_days = Dates_calc.Dates.period_to_days p2 in
compare p1_days p2_days
with Dates_calc.Dates.AmbiguousComputation -> raise UncomparableDurations
with Dates_calc.Dates.AmbiguousComputation ->
error UncomparableDurations [pos]
(* TODO: same here, although it was tweaked to never fail on equal dates.
Comparing the difference to duration_0 is not a good idea because we still
want to fail on [1 month, 30 days] rather than return [false] *)
let equal_periods (p1 : duration) (p2 : duration) : bool =
let equal_periods pos (p1 : duration) (p2 : duration) : bool =
try Dates_calc.Dates.period_to_days (Dates_calc.Dates.sub_periods p1 p2) = 0
with Dates_calc.Dates.AmbiguousComputation -> raise UncomparableDurations
with Dates_calc.Dates.AmbiguousComputation ->
error UncomparableDurations [pos]
module Oper = struct
let o_not = Stdlib.not
@ -782,8 +796,8 @@ module Oper = struct
let o_eq = ( = )
let o_map = Array.map
let o_map2 f a b =
try Array.map2 f a b with Invalid_argument _ -> raise NotSameLength
let o_map2 pos f a b =
try Array.map2 f a b with Invalid_argument _ -> error NotSameLength [pos]
let o_reduce f dft a =
let len = Array.length a in
@ -818,54 +832,56 @@ module Oper = struct
let o_mult_dur_int d m = Dates_calc.Dates.mul_period d (Z.to_int m)
let o_div_int_int i1 i2 =
let o_div_int_int pos i1 i2 =
(* It's not on the ocamldoc, but Q.div likely already raises this ? *)
if Z.zero = i2 then raise Division_by_zero
if Z.zero = i2 then error DivisionByZero [pos]
else Q.div (Q.of_bigint i1) (Q.of_bigint i2)
let o_div_rat_rat i1 i2 =
if Q.zero = i2 then raise Division_by_zero else Q.div i1 i2
let o_div_rat_rat pos i1 i2 =
if Q.zero = i2 then error DivisionByZero [pos] else Q.div i1 i2
let o_div_mon_mon m1 m2 =
if Z.zero = m2 then raise Division_by_zero
let o_div_mon_mon pos m1 m2 =
if Z.zero = m2 then error DivisionByZero [pos]
else Q.div (Q.of_bigint m1) (Q.of_bigint m2)
let o_div_mon_rat m1 r1 =
if Q.zero = r1 then raise Division_by_zero else o_mult_mon_rat m1 (Q.inv r1)
let o_div_mon_rat pos m1 r1 =
if Q.zero = r1 then error DivisionByZero [pos]
else o_mult_mon_rat m1 (Q.inv r1)
let o_div_dur_dur d1 d2 =
let o_div_dur_dur pos d1 d2 =
let i1, i2 =
try
( integer_of_int (Dates_calc.Dates.period_to_days d1),
integer_of_int (Dates_calc.Dates.period_to_days d2) )
with Dates_calc.Dates.AmbiguousComputation -> raise IndivisibleDurations
with Dates_calc.Dates.AmbiguousComputation ->
error IndivisibleDurations [pos]
in
o_div_int_int i1 i2
o_div_int_int pos i1 i2
let o_lt_int_int i1 i2 = Z.compare i1 i2 < 0
let o_lt_rat_rat i1 i2 = Q.compare i1 i2 < 0
let o_lt_mon_mon m1 m2 = Z.compare m1 m2 < 0
let o_lt_dur_dur d1 d2 = compare_periods d1 d2 < 0
let o_lt_dur_dur pos d1 d2 = compare_periods pos d1 d2 < 0
let o_lt_dat_dat d1 d2 = Dates_calc.Dates.compare_dates d1 d2 < 0
let o_lte_int_int i1 i2 = Z.compare i1 i2 <= 0
let o_lte_rat_rat i1 i2 = Q.compare i1 i2 <= 0
let o_lte_mon_mon m1 m2 = Z.compare m1 m2 <= 0
let o_lte_dur_dur d1 d2 = compare_periods d1 d2 <= 0
let o_lte_dur_dur pos d1 d2 = compare_periods pos d1 d2 <= 0
let o_lte_dat_dat d1 d2 = Dates_calc.Dates.compare_dates d1 d2 <= 0
let o_gt_int_int i1 i2 = Z.compare i1 i2 > 0
let o_gt_rat_rat i1 i2 = Q.compare i1 i2 > 0
let o_gt_mon_mon m1 m2 = Z.compare m1 m2 > 0
let o_gt_dur_dur d1 d2 = compare_periods d1 d2 > 0
let o_gt_dur_dur pos d1 d2 = compare_periods pos d1 d2 > 0
let o_gt_dat_dat d1 d2 = Dates_calc.Dates.compare_dates d1 d2 > 0
let o_gte_int_int i1 i2 = Z.compare i1 i2 >= 0
let o_gte_rat_rat i1 i2 = Q.compare i1 i2 >= 0
let o_gte_mon_mon m1 m2 = Z.compare m1 m2 >= 0
let o_gte_dur_dur d1 d2 = compare_periods d1 d2 >= 0
let o_gte_dur_dur pos d1 d2 = compare_periods pos d1 d2 >= 0
let o_gte_dat_dat d1 d2 = Dates_calc.Dates.compare_dates d1 d2 >= 0
let o_eq_int_int i1 i2 = Z.equal i1 i2
let o_eq_rat_rat i1 i2 = Q.equal i1 i2
let o_eq_mon_mon m1 m2 = Z.equal m1 m2
let o_eq_dur_dur d1 d2 = equal_periods d1 d2
let o_eq_dur_dur pos d1 d2 = equal_periods pos d1 d2
let o_eq_dat_dat d1 d2 = Dates_calc.Dates.compare_dates d1 d2 = 0
let o_fold = Array.fold_left
end

75
runtimes/ocaml/runtime.mli
View File

@ -69,14 +69,24 @@ type io_log = {
(** {1 Exceptions} *)
exception EmptyError
exception AssertionFailed of source_position
exception ConflictError of source_position
exception UncomparableDurations
exception IndivisibleDurations
exception ImpossibleDate
exception NoValueProvided of source_position
exception Division_by_zero (* Shadows the stdlib definition *)
type error =
| AssertionFailed (** An assertion in the program doesn't hold *)
| NoValue (** No computation with valid conditions found *)
| Conflict (** Two different valid computations at that point *)
| DivisionByZero (** The denominator happened to be 0 here *)
| NotSameLength (** Traversing multiple lists of different lengths *)
| UncomparableDurations
(** Comparing durations in different units (e.g. months vs. days) *)
| IndivisibleDurations (** Dividing durations that are not in days *)
val error_to_string : error -> string
(** Returns the capitalized tag of the error as a string *)
val error_message : error -> string
(** Returns a short explanation message about the error *)
exception Error of error * source_position list
exception Empty
(** {1 Value Embedding} *)
@ -305,12 +315,12 @@ val year_of_date : date -> integer
val date_to_string : date -> string
val date_of_numbers : int -> int -> int -> date
(** Usage: [date_of_numbers year month day]
@raise ImpossibleDate *)
(** Usage: [date_of_numbers year month day].
@raise Failure on invalid inputs *)
val first_day_of_month : date -> date
val last_day_of_month : date -> date
val date_to_years_months_days : date -> int * int * int
(**{2 Durations} *)
@ -318,6 +328,7 @@ val duration_of_numbers : int -> int -> int -> duration
(** Usage : [duration_of_numbers year mounth day]. *)
val duration_to_years_months_days : duration -> int * int * int
(**{2 Times} *)
val duration_to_string : duration -> string
@ -325,24 +336,27 @@ val duration_to_string : duration -> string
(**{1 Defaults} *)
val handle_default :
source_position -> (unit -> 'a) array -> (unit -> bool) -> (unit -> 'a) -> 'a
(** @raise EmptyError
@raise ConflictError *)
source_position array ->
(unit -> 'a) array ->
(unit -> bool) ->
(unit -> 'a) ->
'a
(** @raise Empty
@raise Error Conflict *)
val handle_default_opt :
source_position ->
source_position array ->
'a Eoption.t array ->
(unit -> bool) ->
(unit -> 'a Eoption.t) ->
'a Eoption.t
(** @raise ConflictError *)
val no_input : unit -> 'a
(** @raise Error Conflict *)
(**{1 Operators} *)
module Oper : sig
(* The types **must** match with Shared_ast.Operator.*_type *)
(* The types **must** match with Shared_ast.Operator.*_type ; but for the
added first argument [pos] for any operator that might trigger an error. *)
val o_not : bool -> bool
val o_length : 'a array -> integer
val o_torat_int : integer -> decimal
@ -365,7 +379,8 @@ module Oper : sig
val o_eq : 'a -> 'a -> bool
val o_map : ('a -> 'b) -> 'a array -> 'b array
val o_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
val o_map2 :
source_position -> ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
(** @raise [NotSameLength] *)
val o_reduce : ('a -> 'a -> 'a) -> 'a -> 'a array -> 'a
@ -386,35 +401,35 @@ module Oper : sig
val o_mult_rat_rat : decimal -> decimal -> decimal
val o_mult_mon_rat : money -> decimal -> money
val o_mult_dur_int : duration -> integer -> duration
val o_div_int_int : integer -> integer -> decimal
val o_div_rat_rat : decimal -> decimal -> decimal
val o_div_mon_mon : money -> money -> decimal
val o_div_mon_rat : money -> decimal -> money
val o_div_dur_dur : duration -> duration -> decimal
val o_div_int_int : source_position -> integer -> integer -> decimal
val o_div_rat_rat : source_position -> decimal -> decimal -> decimal
val o_div_mon_mon : source_position -> money -> money -> decimal
val o_div_mon_rat : source_position -> money -> decimal -> money
val o_div_dur_dur : source_position -> duration -> duration -> decimal
val o_lt_int_int : integer -> integer -> bool
val o_lt_rat_rat : decimal -> decimal -> bool
val o_lt_mon_mon : money -> money -> bool
val o_lt_dur_dur : duration -> duration -> bool
val o_lt_dur_dur : source_position -> duration -> duration -> bool
val o_lt_dat_dat : date -> date -> bool
val o_lte_int_int : integer -> integer -> bool
val o_lte_rat_rat : decimal -> decimal -> bool
val o_lte_mon_mon : money -> money -> bool
val o_lte_dur_dur : duration -> duration -> bool
val o_lte_dur_dur : source_position -> duration -> duration -> bool
val o_lte_dat_dat : date -> date -> bool
val o_gt_int_int : integer -> integer -> bool
val o_gt_rat_rat : decimal -> decimal -> bool
val o_gt_mon_mon : money -> money -> bool
val o_gt_dur_dur : duration -> duration -> bool
val o_gt_dur_dur : source_position -> duration -> duration -> bool
val o_gt_dat_dat : date -> date -> bool
val o_gte_int_int : integer -> integer -> bool
val o_gte_rat_rat : decimal -> decimal -> bool
val o_gte_mon_mon : money -> money -> bool
val o_gte_dur_dur : duration -> duration -> bool
val o_gte_dur_dur : source_position -> duration -> duration -> bool
val o_gte_dat_dat : date -> date -> bool
val o_eq_int_int : integer -> integer -> bool
val o_eq_rat_rat : decimal -> decimal -> bool
val o_eq_mon_mon : money -> money -> bool
val o_eq_dur_dur : duration -> duration -> bool
val o_eq_dur_dur : source_position -> duration -> duration -> bool
val o_eq_dat_dat : date -> date -> bool
val o_fold : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
end

65
runtimes/python/src/catala/runtime.py
View File

@ -355,37 +355,62 @@ class SourcePosition:
self.law_headings = law_headings
def __str__(self) -> str:
return "in file {}, from {}:{} to {}:{}".format(
self.filename, self.start_line, self.start_column, self.end_line, self.end_column)
return "{}:{}.{}-{}.{}".format(
self.filename,
self.start_line, self.start_column,
self.end_line, self.end_column)
# ==========
# Exceptions
# ==========
class EmptyError(Exception):
class Empty(Exception):
pass
class AssertionFailed(Exception):
def __init__(self, source_position: SourcePosition) -> None:
class CatalaError(Exception):
def __init__(self, message: str, source_position: SourcePosition) -> None:
self.message = message
self.source_position = source_position
# Prints in the same format as the OCaml runtime
def __str__(self) -> str:
return "[ERROR] At {}: {}".format(
self.source_position,
self.message)
class ConflictError(Exception):
class AssertionFailed(CatalaError):
def __init__(self, source_position: SourcePosition) -> None:
self.source_position = source_position
super().__init__("this assertion doesn't hold", source_position)
class NoValueProvided(Exception):
class NoValue(CatalaError):
def __init__(self, source_position: SourcePosition) -> None:
self.source_position = source_position
super().__init__("no computation with valid conditions found",
source_position)
class AssertionFailure(Exception):
class Conflict(CatalaError):
def __init__(self, source_position: SourcePosition) -> None:
self.source_position = source_position
super().__init__("two or more concurring valid computations",
source_position)
class DivisionByZero(CatalaError):
def __init__(self, source_position: SourcePosition) -> None:
super().__init__("division by zero", source_position)
class NotSameLength(CatalaError):
def __init__(self, source_position: SourcePosition) -> None:
super().__init__("traversing multiple lists of different lengths",
source_position)
class UncomparableDurations(CatalaError):
def __init__(self, source_position: SourcePosition) -> None:
super().__init__(
"comparing durations in different units (e.g. months vs. days)",
source_position)
class IndivisibleDurations(CatalaError):
def __init__(self, source_position: SourcePosition) -> None:
super().__init__("dividing durations that are not in days",
source_position)
# ============================
# Constructors and conversions
@ -601,19 +626,19 @@ def handle_default(
new_val: Optional[Alpha]
try:
new_val = exception(Unit())
except EmptyError:
except Empty:
new_val = None
if acc is None:
acc = new_val
elif not (acc is None) and new_val is None:
pass # acc stays the same
elif not (acc is None) and not (new_val is None):
raise ConflictError(pos)
raise Conflict(pos)
if acc is None:
if just(Unit()):
return cons(Unit())
else:
raise EmptyError
raise Empty
else:
return acc
@ -631,7 +656,7 @@ def handle_default_opt(
elif not (acc is None) and exception is None:
pass # acc stays the same
elif not (acc is None) and not (exception is None):
raise ConflictError(pos)
raise Conflict(pos)
if acc is None:
b = just(Unit())
if b:
@ -644,7 +669,7 @@ def handle_default_opt(
def no_input() -> Callable[[Unit], Alpha]:
def closure(_: Unit):
raise EmptyError
raise Empty
return closure

66
tests/arithmetic/bad/division_by_zero.catala_en
View File

@ -32,42 +32,10 @@ scope Money:
```catala-test-inline
$ catala Interpret -s Dec
[ERROR] division by zero at runtime
$ catala test-scope Dec
[ERROR] During evaluation: a value is being used as denominator in a division
and it computed to zero.
The division operator:
┌─⯈ tests/arithmetic/bad/division_by_zero.catala_en:20.23-20.30:
└──┐
20 │ definition i equals 1. / 0.
│ ‾‾‾‾‾‾‾
└┬ `Division_by_zero` exception management
└─ with decimals
The null denominator:
┌─⯈ tests/arithmetic/bad/division_by_zero.catala_en:20.28-20.30:
└──┐
20 │ definition i equals 1. / 0.
│ ‾‾
└┬ `Division_by_zero` exception management
└─ with decimals
#return code 123#
```
Fixme: the following should give the same result as above, but the optimisation pass propagates the position surrounding the `ErrorOnEmpty` and loses the position of the actual division expression which was in the `cons` of the default term. Unfortunately this is non-trivial due to the bindlib boxing tricks.
```catala-test-inline
$ catala Interpret -O -s Dec
[ERROR] division by zero at runtime
The division operator:
┌─⯈ tests/arithmetic/bad/division_by_zero.catala_en:17.10-17.11:
└──┐
17 │ output i content decimal
│ ‾
└┬ `Division_by_zero` exception management
└─ with decimals
The null denominator:
┌─⯈ tests/arithmetic/bad/division_by_zero.catala_en:20.28-20.30:
└──┐
20 │ definition i equals 1. / 0.
@ -78,18 +46,10 @@ The null denominator:
```
```catala-test-inline
$ catala interpret -s Int
[ERROR] division by zero at runtime
$ catala test-scope Int
[ERROR] During evaluation: a value is being used as denominator in a division
and it computed to zero.
The division operator:
┌─⯈ tests/arithmetic/bad/division_by_zero.catala_en:10.23-10.28:
└──┐
10 │ definition i equals 1 / 0
│ ‾‾‾‾‾
└┬ `Division_by_zero` exception management
└─ with integers
The null denominator:
┌─⯈ tests/arithmetic/bad/division_by_zero.catala_en:10.27-10.28:
└──┐
10 │ definition i equals 1 / 0
@ -100,18 +60,10 @@ The null denominator:
```
```catala-test-inline
$ catala Interpret -s Money
[ERROR] division by zero at runtime
$ catala test-scope Money
[ERROR] During evaluation: a value is being used as denominator in a division
and it computed to zero.
The division operator:
┌─⯈ tests/arithmetic/bad/division_by_zero.catala_en:30.23-30.35:
└──┐
30 │ definition i equals $10.0 / $0.0
│ ‾‾‾‾‾‾‾‾‾‾‾‾
└┬ `Division_by_zero` exception management
└─ with money
The null denominator:
┌─⯈ tests/arithmetic/bad/division_by_zero.catala_en:30.31-30.35:
└──┐
30 │ definition i equals $10.0 / $0.0

8
tests/backends/output/simple.c
View File

@ -180,7 +180,7 @@ baz_struct baz_func(baz_in_struct baz_in) {
option_1_enum match_arg = temp_a_3;
if (match_arg.code == option_1_enum_none_1_cons) {
void* /* unit */ dummy_var = match_arg.payload.none_1_cons;
catala_fatal_error_raised.code = catala_no_value_provided;
catala_fatal_error_raised.code = catala_no_value;
catala_fatal_error_raised.position.filename = "tests/backends/simple.catala_en";
catala_fatal_error_raised.position.start_line = 11;
catala_fatal_error_raised.position.start_column = 11;
@ -202,7 +202,7 @@ baz_struct baz_func(baz_in_struct baz_in) {
option_1_enum match_arg_1 = temp_a_1;
if (match_arg_1.code == option_1_enum_none_1_cons) {
void* /* unit */ dummy_var = match_arg_1.payload.none_1_cons;
catala_fatal_error_raised.code = catala_no_value_provided;
catala_fatal_error_raised.code = catala_no_value;
catala_fatal_error_raised.position.filename = "tests/backends/simple.catala_en";
catala_fatal_error_raised.position.start_line = 11;
catala_fatal_error_raised.position.start_column = 11;
@ -360,7 +360,7 @@ baz_struct baz_func(baz_in_struct baz_in) {
option_2_enum match_arg_4 = temp_b_1;
if (match_arg_4.code == option_2_enum_none_2_cons) {
void* /* unit */ dummy_var = match_arg_4.payload.none_2_cons;
catala_fatal_error_raised.code = catala_no_value_provided;
catala_fatal_error_raised.code = catala_no_value;
catala_fatal_error_raised.position.filename = "tests/backends/simple.catala_en";
catala_fatal_error_raised.position.start_line = 12;
catala_fatal_error_raised.position.start_column = 10;
@ -424,7 +424,7 @@ baz_struct baz_func(baz_in_struct baz_in) {
option_3_enum match_arg_5 = temp_c_1;
if (match_arg_5.code == option_3_enum_none_3_cons) {
void* /* unit */ dummy_var = match_arg_5.payload.none_3_cons;
catala_fatal_error_raised.code = catala_no_value_provided;
catala_fatal_error_raised.code = catala_no_value;
catala_fatal_error_raised.position.filename = "tests/backends/simple.catala_en";
catala_fatal_error_raised.position.start_line = 13;
catala_fatal_error_raised.position.start_column = 10;

30
tests/backends/python_name_clash.catala_en
View File

@ -98,24 +98,23 @@ def some_name(some_name_in:SomeNameIn):
def temp_o_2(_:Unit):
return (i + integer_of_string("1"))
return handle_default(SourcePosition(filename="tests/backends/python_name_clash.catala_en",
start_line=7, start_column=10,
end_line=7, end_column=11,
start_line=10, start_column=23,
end_line=10, end_column=28,
law_headings=[]), [], temp_o_1, temp_o_2)
def temp_o_3(_:Unit):
return False
def temp_o_4(_:Unit):
raise EmptyError
raise Empty
temp_o_5 = handle_default(SourcePosition(filename="tests/backends/python_name_clash.catala_en",
start_line=7, start_column=10,
end_line=7, end_column=11,
law_headings=[]), [temp_o], temp_o_3,
temp_o_4)
except EmptyError:
temp_o_5 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/backends/python_name_clash.catala_en",
except Empty:
raise NoValue(SourcePosition(
filename="tests/backends/python_name_clash.catala_en",
start_line=7, start_column=10,
end_line=7, end_column=11,
law_headings=[]))
end_line=7, end_column=11, law_headings=[]))
o = temp_o_5
return SomeName(o = o)
@ -127,25 +126,24 @@ def b(b_in:BIn):
def temp_result_2(_:Unit):
return integer_of_string("1")
return handle_default(SourcePosition(filename="tests/backends/python_name_clash.catala_en",
start_line=16, start_column=14,
end_line=16, end_column=25,
start_line=16, start_column=33,
end_line=16, end_column=34,
law_headings=[]), [], temp_result_1,
temp_result_2)
def temp_result_3(_:Unit):
return False
def temp_result_4(_:Unit):
raise EmptyError
raise Empty
temp_result_5 = handle_default(SourcePosition(filename="tests/backends/python_name_clash.catala_en",
start_line=16, start_column=14,
end_line=16, end_column=25,
law_headings=[]), [temp_result],
temp_result_3, temp_result_4)
except EmptyError:
temp_result_5 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/backends/python_name_clash.catala_en",
except Empty:
raise NoValue(SourcePosition(
filename="tests/backends/python_name_clash.catala_en",
start_line=16, start_column=14,
end_line=16, end_column=25,
law_headings=[]))
end_line=16, end_column=25, law_headings=[]))
result = some_name(SomeNameIn(i_in = temp_result_5))
result_1 = SomeName(o = result.o)
if True:

60
tests/date/bad/uncomparable_duration.catala_en
View File

@ -42,20 +42,13 @@ scope Ge:
```catala-test-inline
$ catala test-scope Ge
[ERROR] Cannot compare together durations that cannot be converted to a
precise number of days
[ERROR] During evaluation: ambiguous comparison between durations in
different units (e.g. months vs. days).
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:40.23-40.30:
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:40.31-40.33:
└──┐
40 │ definition d equals 1 month >= 2 day
│ ‾‾‾‾‾‾‾
└┬ `UncomparableDurations` exception management
└─ `>=` operator
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:40.34-40.39:
└──┐
40 │ definition d equals 1 month >= 2 day
│ ‾‾‾‾‾
│ ‾‾
└┬ `UncomparableDurations` exception management
└─ `>=` operator
#return code 123#
@ -63,20 +56,13 @@ $ catala test-scope Ge
```catala-test-inline
$ catala test-scope Gt
[ERROR] Cannot compare together durations that cannot be converted to a
precise number of days
[ERROR] During evaluation: ambiguous comparison between durations in
different units (e.g. months vs. days).
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:30.23-30.30:
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:30.31-30.32:
└──┐
30 │ definition d equals 1 month > 2 day
│ ‾‾‾‾‾‾‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:30.33-30.38:
└──┐
30 │ definition d equals 1 month > 2 day
│ ‾‾‾‾‾
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
#return code 123#
@ -84,20 +70,13 @@ $ catala test-scope Gt
```catala-test-inline
$ catala test-scope Le
[ERROR] Cannot compare together durations that cannot be converted to a
precise number of days
[ERROR] During evaluation: ambiguous comparison between durations in
different units (e.g. months vs. days).
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:20.23-20.30:
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:20.31-20.33:
└──┐
20 │ definition d equals 1 month <= 2 day
│ ‾‾‾‾‾‾‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:20.34-20.39:
└──┐
20 │ definition d equals 1 month <= 2 day
│ ‾‾‾‾‾
│ ‾‾
└┬ `UncomparableDurations` exception management
└─ `<=` operator
#return code 123#
@ -105,20 +84,13 @@ $ catala test-scope Le
```catala-test-inline
$ catala test-scope Lt
[ERROR] Cannot compare together durations that cannot be converted to a
precise number of days
[ERROR] During evaluation: ambiguous comparison between durations in
different units (e.g. months vs. days).
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:10.23-10.30:
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:10.31-10.32:
└──┐
10 │ definition d equals 1 month < 2 day
│ ‾‾‾‾‾‾‾
└┬ `UncomparableDurations` exception management
└─ `<` operator
┌─⯈ tests/date/bad/uncomparable_duration.catala_en:10.33-10.38:
└──┐
10 │ definition d equals 1 month < 2 day
│ ‾‾‾‾‾
│ ‾
└┬ `UncomparableDurations` exception management
└─ `<` operator
#return code 123#

6
tests/default/bad/conflict.catala_en
View File

@ -11,8 +11,8 @@ scope A:
```catala-test-inline
$ catala Interpret -s A --message=gnu
tests/default/bad/conflict.catala_en:8.56-8.57: [ERROR] There is a conflict between multiple valid consequences for assigning the same variable.
tests/default/bad/conflict.catala_en:8.56-8.57: [ERROR] This consequence has a valid justification:
tests/default/bad/conflict.catala_en:9.56-9.57: [ERROR] This consequence has a valid justification:
tests/default/bad/conflict.catala_en:8.56-8.57: [ERROR] During evaluation: conflict between multiple valid consequences for assigning the same variable.
tests/default/bad/conflict.catala_en:8.56-8.57: [ERROR]
tests/default/bad/conflict.catala_en:9.56-9.57: [ERROR]
#return code 123#
```

4
tests/default/bad/empty.catala_en
View File

@ -19,8 +19,8 @@ $ catala test-scope A
6 │ output y content boolean
│ ‾
└─ Article
[ERROR] This variable evaluated to an empty term (no rule that defined it
applied in this situation)
[ERROR] During evaluation: no applicable rule to define this variable in this
situation.
┌─⯈ tests/default/bad/empty.catala_en:6.10-6.11:
└─┐

6
tests/default/bad/empty_with_rules.catala_en
View File

@ -13,9 +13,9 @@ scope A:
```
```catala-test-inline
$ catala interpret -s A
[ERROR] This variable evaluated to an empty term (no rule that defined it
applied in this situation)
$ catala test-scope A
[ERROR] During evaluation: no applicable rule to define this variable in this
situation.
┌─⯈ tests/default/bad/empty_with_rules.catala_en:5.10-5.11:
└─┐

10
tests/exception/bad/two_exceptions.catala_en
View File

@ -15,21 +15,17 @@ scope A:
definition x equals 2
```
Note: ideally this could use test-scope but some positions are lost during translation to lcalc
```catala-test-inline
$ catala interpret -s A
[ERROR] There is a conflict between multiple valid consequences for assigning
the same variable.
$ catala test-scope A
[ERROR] During evaluation: conflict between multiple valid consequences for
assigning the same variable.
This consequence has a valid justification:
┌─⯈ tests/exception/bad/two_exceptions.catala_en:12.23-12.24:
└──┐
12 │ definition x equals 1
│ ‾
└─ Test
This consequence has a valid justification:
┌─⯈ tests/exception/bad/two_exceptions.catala_en:15.23-15.24:
└──┐
15 │ definition x equals 2

10
tests/func/bad/bad_func.catala_en
View File

@ -27,21 +27,17 @@ $ catala test-scope R
[RESULT] r = 30
```
Note: ideally this could use test-scope but some positions are lost during translation to lcalc
```catala-test-inline
$ catala interpret -s S
[ERROR] There is a conflict between multiple valid consequences for assigning
the same variable.
$ catala test-scope S
[ERROR] During evaluation: conflict between multiple valid consequences for
assigning the same variable.
This consequence has a valid justification:
┌─⯈ tests/func/bad/bad_func.catala_en:14.65-14.70:
└──┐
14 │ definition f of x under condition (x >= x) consequence equals x + x
│ ‾‾‾‾‾
└─ Article
This consequence has a valid justification:
┌─⯈ tests/func/bad/bad_func.catala_en:15.62-15.67:
└──┐
15 │ definition f of x under condition not b consequence equals x * x

2
tests/func/good/closure_conversion_reduce.catala_en
View File

@ -75,7 +75,7 @@ let scope S (S_in: S_in {x_in: list of integer}): S {y: integer} =
(λ () → false)
(λ () → ENone ()))
with
| ENone → raise NoValueProvided
| ENone → error NoValue
| ESome arg → arg
in
return { S y = y; }

2
tests/func/good/scope_call_func_struct_closure.catala_en
View File

@ -124,7 +124,7 @@ let scope Foo
match
(handle_default_opt [b.0 b.1 ()] (λ () → true) (λ () → ESome true))
with
| ENone → raise NoValueProvided
| ENone → error NoValue
| ESome arg → arg
in
let set r :

56
tests/modules/good/output/mod_def.ml
View File

@ -29,46 +29,46 @@ let s (s_in: S_in.t) : S.t =
let sr_: money =
try
(handle_default
{filename = "tests/modules/good/mod_def.catala_en"; start_line=16;
start_column=10; end_line=16; end_column=12;
law_headings=["Test modules + inclusions 1"]}
[|{filename="tests/modules/good/mod_def.catala_en";
start_line=26; start_column=24; end_line=26; end_column=30;
law_headings=["Test modules + inclusions 1"]}|]
([|(fun (_: unit) ->
handle_default
{filename = "tests/modules/good/mod_def.catala_en";
handle_default [||] ([||]) (fun (_: unit) -> true)
(fun (_: unit) -> money_of_cents_string "100000"))|])
(fun (_: unit) -> false) (fun (_: unit) -> raise Empty))
with Empty ->
(raise
(Runtime_ocaml.Runtime.Error (NoValue, [{filename="tests/modules/good/mod_def.catala_en";
start_line=16; start_column=10;
end_line=16; end_column=12;
law_headings=["Test modules + inclusions 1"]} ([||])
(fun (_: unit) -> true)
(fun (_: unit) -> money_of_cents_string "100000"))|])
(fun (_: unit) -> false) (fun (_: unit) -> raise EmptyError))
with
EmptyError -> (raise (NoValueProvided
{filename = "tests/modules/good/mod_def.catala_en"; start_line=16;
start_column=10; end_line=16; end_column=12;
law_headings=["Test modules + inclusions 1"]})) in
law_headings=["Test modules + inclusions 1"]}])))
in
let e1_: Enum1.t =
try
(handle_default
{filename = "tests/modules/good/mod_def.catala_en"; start_line=17;
start_column=10; end_line=17; end_column=12;
law_headings=["Test modules + inclusions 1"]}
[|{filename="tests/modules/good/mod_def.catala_en";
start_line=27; start_column=24; end_line=27; end_column=29;
law_headings=["Test modules + inclusions 1"]}|]
([|(fun (_: unit) ->
handle_default
{filename = "tests/modules/good/mod_def.catala_en";
handle_default [||] ([||]) (fun (_: unit) -> true)
(fun (_: unit) -> Enum1.Maybe ()))|])
(fun (_: unit) -> false) (fun (_: unit) -> raise Empty))
with Empty ->
(raise
(Runtime_ocaml.Runtime.Error (NoValue, [{filename="tests/modules/good/mod_def.catala_en";
start_line=17; start_column=10;
end_line=17; end_column=12;
law_headings=["Test modules + inclusions 1"]} ([||])
(fun (_: unit) -> true) (fun (_: unit) -> Enum1.Maybe ()))|])
(fun (_: unit) -> false) (fun (_: unit) -> raise EmptyError))
with
EmptyError -> (raise (NoValueProvided
{filename = "tests/modules/good/mod_def.catala_en"; start_line=17;
start_column=10; end_line=17; end_column=12;
law_headings=["Test modules + inclusions 1"]})) in
law_headings=["Test modules + inclusions 1"]}])))
in
{S.sr = sr_; S.e1 = e1_}
let half_ : integer -> decimal =
fun (x_: integer) -> o_div_int_int x_ (integer_of_string "2")
fun (x_: integer) ->
o_div_int_int
{filename="tests/modules/good/mod_def.catala_en";
start_line=21; start_column=14; end_line=21; end_column=15;
law_headings=["Test modules + inclusions 1"]} x_ (integer_of_string
"2")
let () =
Runtime_ocaml.Runtime.register_module "Mod_def"

6
tests/modules/good/prorata_external.ml
View File

@ -5,12 +5,14 @@ open Oper
let mzero = money_of_units_int 0
let pos = {filename=__FILE__; start_line=0; start_column=0; end_line=0; end_column=0; law_headings=[]}
let prorata_ : money -> (money array) -> (money array) =
fun (amount: money) (weights: money array) ->
let w_total = Array.fold_left o_add_mon_mon mzero weights in
let rem, a =
Array.fold_left_map (fun rem w ->
let r = o_mult_mon_rat amount (o_div_mon_mon w w_total) in
let r = o_mult_mon_rat amount (o_div_mon_mon pos w w_total) in
o_sub_mon_mon rem r, r)
amount weights
in
@ -25,7 +27,7 @@ let prorata2_ : money -> (money array) -> (money array) =
let r =
o_mult_mon_rat
rem_amount
(o_div_mon_mon w rem_weights) in
(o_div_mon_mon pos w rem_weights) in
(o_sub_mon_mon rem_amount r, o_sub_mon_mon rem_weights w), r)
(amount, w_total) weights
in

41
tests/name_resolution/good/let_in2.catala_en
View File

@ -51,38 +51,35 @@ let s (s_in: S_in.t) : S.t =
let a_: bool =
try
(handle_default
{filename = "tests/name_resolution/good/let_in2.catala_en";
[|{filename="tests/name_resolution/good/let_in2.catala_en";
start_line=7; start_column=18; end_line=7; end_column=19;
law_headings=["Article"]} ([|(fun (_: unit) -> a_ ())|])
law_headings=["Article"]}|] ([|(fun (_: unit) -> a_ ())|])
(fun (_: unit) -> true)
(fun (_: unit) ->
try
(handle_default
{filename = "tests/name_resolution/good/let_in2.catala_en";
start_line=7; start_column=18; end_line=7; end_column=19;
law_headings=["Article"]}
[|{filename="tests/name_resolution/good/let_in2.catala_en";
start_line=11; start_column=5; end_line=13; end_column=6;
law_headings=["Article"]}|]
([|(fun (_: unit) ->
handle_default
{filename = "tests/name_resolution/good/let_in2.catala_en";
start_line=7; start_column=18;
end_line=7; end_column=19;
law_headings=["Article"]} ([||])
(fun (_: unit) -> true)
handle_default [||] ([||]) (fun (_: unit) -> true)
(fun (_: unit) -> (let a_ : bool = false
in
(let a_ : bool = (o_or a_ true) in
a_))))|]) (fun (_: unit) -> false)
(fun (_: unit) -> raise EmptyError))
with
EmptyError -> (raise (NoValueProvided
{filename = "tests/name_resolution/good/let_in2.catala_en";
start_line=7; start_column=18; end_line=7; end_column=19;
law_headings=["Article"]}))))
with
EmptyError -> (raise (NoValueProvided
{filename = "tests/name_resolution/good/let_in2.catala_en";
start_line=7; start_column=18; end_line=7; end_column=19;
law_headings=["Article"]})) in
(fun (_: unit) -> raise Empty))
with Empty ->
(raise
(Runtime_ocaml.Runtime.Error (NoValue, [{filename="tests/name_resolution/good/let_in2.catala_en";
start_line=7; start_column=18;
end_line=7; end_column=19;
law_headings=["Article"]}])))))
with Empty ->
(raise
(Runtime_ocaml.Runtime.Error (NoValue, [{filename="tests/name_resolution/good/let_in2.catala_en";
start_line=7; start_column=18;
end_line=7; end_column=19;
law_headings=["Article"]}]))) in
{S.a = a_}
let () =

90
tests/name_resolution/good/toplevel_defs.catala_en
View File

@ -133,10 +133,10 @@ let S2_6 (S2_in_10: S2_in) =
return false;
decl temp_a_21 : unit → decimal;
let func temp_a_21 (__22 : unit) =
raise EmptyError;
raise Empty;
temp_a_12 = handle_default [temp_a_13] temp_a_19 temp_a_21
with EmptyError:
raise NoValueProvided;
with Empty:
fatal NoValue;
decl a_11 : decimal;
a_11 = temp_a_12;
return S2 {"a": a_11}
@ -158,10 +158,10 @@ let S3_7 (S3_in_23: S3_in) =
return false;
decl temp_a_34 : unit → decimal;
let func temp_a_34 (__35 : unit) =
raise EmptyError;
raise Empty;
temp_a_25 = handle_default [temp_a_26] temp_a_32 temp_a_34
with EmptyError:
raise NoValueProvided;
with Empty:
fatal NoValue;
decl a_24 : decimal;
a_24 = temp_a_25;
return S3 {"a": a_24}
@ -183,10 +183,10 @@ let S4_8 (S4_in_36: S4_in) =
return false;
decl temp_a_47 : unit → decimal;
let func temp_a_47 (__48 : unit) =
raise EmptyError;
raise Empty;
temp_a_38 = handle_default [temp_a_39] temp_a_45 temp_a_47
with EmptyError:
raise NoValueProvided;
with Empty:
fatal NoValue;
decl a_37 : decimal;
a_37 = temp_a_38;
return S4 {"a": a_37}
@ -208,10 +208,10 @@ let S_9 (S_in_49: S_in) =
return false;
decl temp_a_72 : unit → decimal;
let func temp_a_72 (__73 : unit) =
raise EmptyError;
raise Empty;
temp_a_63 = handle_default [temp_a_64] temp_a_70 temp_a_72
with EmptyError:
raise NoValueProvided;
with Empty:
fatal NoValue;
decl a_50 : decimal;
a_50 = temp_a_63;
decl temp_b_52 : A {y: bool; z: decimal};
@ -230,10 +230,10 @@ let S_9 (S_in_49: S_in) =
return false;
decl temp_b_61 : unit → A {y: bool; z: decimal};
let func temp_b_61 (__62 : unit) =
raise EmptyError;
raise Empty;
temp_b_52 = handle_default [temp_b_53] temp_b_59 temp_b_61
with EmptyError:
raise NoValueProvided;
with Empty:
fatal NoValue;
decl b_51 : A {y: bool; z: decimal};
b_51 = temp_b_52;
return S {"a": a_50, "b": b_51}
@ -426,22 +426,22 @@ def s2(s2_in:S2In):
return (glob3(money_of_cents_string("4400")) +
decimal_of_string("100."))
return handle_default(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=45, start_column=10,
end_line=45, end_column=11,
start_line=48, start_column=24,
end_line=48, end_column=43,
law_headings=["Test toplevel function defs"]), [],
temp_a_1, temp_a_2)
def temp_a_3(_:Unit):
return False
def temp_a_4(_:Unit):
raise EmptyError
raise Empty
temp_a_5 = handle_default(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=45, start_column=10,
end_line=45, end_column=11,
law_headings=["Test toplevel function defs"]), [temp_a],
temp_a_3, temp_a_4)
except EmptyError:
temp_a_5 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
except Empty:
raise NoValue(SourcePosition(
filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=45, start_column=10,
end_line=45, end_column=11,
law_headings=["Test toplevel function defs"]))
@ -458,22 +458,22 @@ def s3(s3_in:S3In):
glob4(money_of_cents_string("4400"),
decimal_of_string("55.")))
return handle_default(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=65, start_column=10,
end_line=65, end_column=11,
start_line=68, start_column=24,
end_line=68, end_column=47,
law_headings=["Test function def with two args"]), [],
temp_a_7, temp_a_8)
def temp_a_9(_:Unit):
return False
def temp_a_10(_:Unit):
raise EmptyError
raise Empty
temp_a_11 = handle_default(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=65, start_column=10,
end_line=65, end_column=11,
law_headings=["Test function def with two args"]), [temp_a_6],
temp_a_9, temp_a_10)
except EmptyError:
temp_a_11 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
except Empty:
raise NoValue(SourcePosition(
filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=65, start_column=10,
end_line=65, end_column=11,
law_headings=["Test function def with two args"]))
@ -488,22 +488,22 @@ def s4(s4_in:S4In):
def temp_a_14(_:Unit):
return (glob5 + decimal_of_string("1."))
return handle_default(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=88, start_column=10,
end_line=88, end_column=11,
start_line=91, start_column=24,
end_line=91, end_column=34,
law_headings=["Test inline defs in toplevel defs"]), [],
temp_a_13, temp_a_14)
def temp_a_15(_:Unit):
return False
def temp_a_16(_:Unit):
raise EmptyError
raise Empty
temp_a_17 = handle_default(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=88, start_column=10,
end_line=88, end_column=11,
law_headings=["Test inline defs in toplevel defs"]), [temp_a_12],
temp_a_15, temp_a_16)
except EmptyError:
temp_a_17 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
except Empty:
raise NoValue(SourcePosition(
filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=88, start_column=10,
end_line=88, end_column=11,
law_headings=["Test inline defs in toplevel defs"]))
@ -518,22 +518,22 @@ def s(s_in:SIn):
def temp_a_20(_:Unit):
return (glob1 * glob1)
return handle_default(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=7, start_column=10,
end_line=7, end_column=11,
start_line=18, start_column=24,
end_line=18, end_column=37,
law_headings=["Test basic toplevel values defs"]), [],
temp_a_19, temp_a_20)
def temp_a_21(_:Unit):
return False
def temp_a_22(_:Unit):
raise EmptyError
raise Empty
temp_a_23 = handle_default(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=7, start_column=10,
end_line=7, end_column=11,
law_headings=["Test basic toplevel values defs"]), [temp_a_18],
temp_a_21, temp_a_22)
except EmptyError:
temp_a_23 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
except Empty:
raise NoValue(SourcePosition(
filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=7, start_column=10,
end_line=7, end_column=11,
law_headings=["Test basic toplevel values defs"]))
@ -545,22 +545,22 @@ def s(s_in:SIn):
def temp_b_2(_:Unit):
return glob2
return handle_default(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=8, start_column=10,
end_line=8, end_column=11,
start_line=19, start_column=24,
end_line=19, end_column=29,
law_headings=["Test basic toplevel values defs"]), [],
temp_b_1, temp_b_2)
def temp_b_3(_:Unit):
return False
def temp_b_4(_:Unit):
raise EmptyError
raise Empty
temp_b_5 = handle_default(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=8, start_column=10,
end_line=8, end_column=11,
law_headings=["Test basic toplevel values defs"]), [temp_b],
temp_b_3, temp_b_4)
except EmptyError:
temp_b_5 = dead_value
raise NoValueProvided(SourcePosition(filename="tests/name_resolution/good/toplevel_defs.catala_en",
except Empty:
raise NoValue(SourcePosition(
filename="tests/name_resolution/good/toplevel_defs.catala_en",
start_line=8, start_column=10,
end_line=8, end_column=11,
law_headings=["Test basic toplevel values defs"]))

10
tests/scope/bad/scope.catala_en
View File

@ -14,21 +14,17 @@ scope A:
definition b under condition not c consequence equals 0
```
Note: ideally this could use test-scope but some positions are lost during translation to lcalc
```catala-test-inline
$ catala interpret -s A
[ERROR] There is a conflict between multiple valid consequences for assigning
the same variable.
$ catala test-scope A
[ERROR] During evaluation: conflict between multiple valid consequences for
assigning the same variable.
This consequence has a valid justification:
┌─⯈ tests/scope/bad/scope.catala_en:13.57-13.61:
└──┐
13 │ definition b under condition not c consequence equals 1337
│ ‾‾‾‾
└─ Article
This consequence has a valid justification:
┌─⯈ tests/scope/bad/scope.catala_en:14.57-14.58:
└──┐
14 │ definition b under condition not c consequence equals 0

2
tests/scope/good/nothing.catala_en
View File

@ -33,7 +33,7 @@ $ catala Scalc -s Foo2 -O -t
└─ Test
let Foo2_3 (Foo2_in_2: Foo2_in) =
decl temp_bar_4 : integer;
raise NoValueProvided;
fatal NoValue;
decl bar_3 : integer;
bar_3 = temp_bar_4;
return Foo2 {"bar": bar_3}

4
tests/scope/good/simple.catala_en
View File

@ -24,8 +24,8 @@ let scope Foo (Foo_in: Foo_in): Foo {bar: integer} =
handle_default
[λ () → handle_default [] (λ () → true) (λ () → 0)]
(λ () → false)
(λ () → raise EmptyError)
with EmptyError -> raise NoValueProvided
(λ () → raise Empty)
with Empty -> error NoValue
in
return { Foo bar = bar; }
```