Formatting: some other personal preferences

This commit is contained in:
Louis Gesbert 2022-05-04 15:48:03 +02:00
parent 74c5629153
commit f17875f90e
44 changed files with 1038 additions and 1130 deletions

View File

@ -6,3 +6,6 @@ wrap-comments
parse-docstrings
version=0.21.0
cases-exp-indent=2
indicate-multiline-delimiters=no
parens-tuple=multi-line-only
space-around-lists=false

View File

@ -34,12 +34,12 @@ let command =
& info [] ~docv:"COMMAND" ~doc:"Command selection among: test, run")
let debug =
Arg.(value & flag & info [ "debug"; "d" ] ~doc:"Prints debug information")
Arg.(value & flag & info ["debug"; "d"] ~doc:"Prints debug information")
let reset_test_outputs =
Arg.(
value & flag
& info [ "r"; "reset" ]
& info ["r"; "reset"]
~doc:
"Used with the `test` command, resets the test output to whatever is \
output by the Catala compiler.")
@ -48,14 +48,14 @@ let catalac =
Arg.(
value
& opt (some string) None
& info [ "e"; "exe" ] ~docv:"EXE"
& info ["e"; "exe"] ~docv:"EXE"
~doc:"Catala compiler executable, defaults to `catala`")
let ninja_output =
Arg.(
value
& opt (some string) None
& info [ "o"; "output" ] ~docv:"OUTPUT"
& info ["o"; "output"] ~docv:"OUTPUT"
~doc:
"$(i, OUTPUT) is the file that will contain the build.ninja file \
output. If not specified, the build.ninja file will be outputed in \
@ -65,7 +65,7 @@ let scope =
Arg.(
value
& opt (some string) None
& info [ "s"; "scope" ] ~docv:"SCOPE"
& info ["s"; "scope"] ~docv:"SCOPE"
~doc:
"Used with the `run` command, selects which scope of a given Catala \
file to run.")
@ -74,7 +74,7 @@ let makeflags =
Arg.(
value
& opt (some string) None
& info [ "makeflags" ] ~docv:"LANG"
& info ["makeflags"] ~docv:"LANG"
~doc:
"Provides the contents of a $(i, MAKEFLAGS) variable to pass on to \
Ninja. Currently recognizes the -i and -j options.")
@ -83,7 +83,7 @@ let catala_opts =
Arg.(
value
& opt (some string) None
& info [ "c"; "catala-opts" ] ~docv:"LANG"
& info ["c"; "catala-opts"] ~docv:"LANG"
~doc:"Options to pass to the Catala compiler")
let clerk_t f =
@ -134,7 +134,7 @@ let info =
"Please file bug reports at https://github.com/CatalaLang/catala/issues";
]
in
let exits = Cmd.Exit.defaults @ [ Cmd.Exit.info ~doc:"on error." 1 ] in
let exits = Cmd.Exit.defaults @ [Cmd.Exit.info ~doc:"on error." 1] in
Cmd.info "clerk" ~version ~doc ~exits ~man
(**{1 Testing}*)
@ -176,13 +176,13 @@ let filename_to_expected_output_descr (output_dir : string) (filename : string)
let second_extension = Filename.extension filename in
let base_filename, scope =
if Re.Pcre.pmatch ~rex:catala_suffix_regex second_extension then
(filename, None)
filename, None
else
let scope_name_regex = Re.Pcre.regexp "\\.(.+)" in
let scope_name =
(Re.Pcre.extract ~rex:scope_name_regex second_extension).(1)
in
(Filename.remove_extension filename, Some scope_name)
Filename.remove_extension filename, Some scope_name
in
Some { output_dir; complete_filename; base_filename; backend; scope }
@ -234,7 +234,7 @@ let add_reset_rules_aux
~command:
Nj.Expr.(
Seq
([ Lit catala_exe_opts; Lit "-s"; Var "scope" ]
([Lit catala_exe_opts; Lit "-s"; Var "scope"]
@ reset_common_cmd_exprs))
~description:
Nj.Expr.(
@ -280,7 +280,7 @@ let add_test_rules_aux
~command:
Nj.Expr.(
Seq
([ Lit catala_exe_opts; Lit "-s"; Var "scope" ]
([Lit catala_exe_opts; Lit "-s"; Var "scope"]
@ test_common_cmd_exprs))
~description:
Nj.Expr.(
@ -381,10 +381,10 @@ let ninja_start (catala_exe : string) (catala_opts : string) : ninja =
let catala_exe_opts = catala_exe ^ " " ^ catala_opts in
let run_and_display_final_message =
Nj.Rule.make "run_and_display_final_message"
~command:Nj.Expr.(Seq [ Lit ":" ])
~command:Nj.Expr.(Seq [Lit ":"])
~description:
Nj.Expr.(
Seq [ Lit "All tests"; Var "test_file_or_folder"; Lit "passed!" ])
Seq [Lit "All tests"; Var "test_file_or_folder"; Lit "passed!"])
in
{
rules =
@ -420,7 +420,7 @@ let collect_all_ninja_build
Nj.Expr.Lit
(Cli.catala_backend_option_to_string expected_output.backend)
);
("tested_file", Nj.Expr.Lit tested_file);
"tested_file", Nj.Expr.Lit tested_file;
( "expected_output",
Nj.Expr.Lit
(expected_output.output_dir
@ -457,8 +457,7 @@ let collect_all_ninja_build
ninja with
builds =
Nj.BuildMap.add rule_output
(Nj.Build.make_with_vars
~outputs:[ Nj.Expr.Lit rule_output ]
(Nj.Build.make_with_vars ~outputs:[Nj.Expr.Lit rule_output]
~rule ~vars)
ninja.builds;
}
@ -505,8 +504,8 @@ let collect_all_ninja_build
ninja with
builds =
Nj.BuildMap.add test_name
(Nj.Build.make_with_inputs ~outputs:[ Nj.Expr.Lit test_name ]
~rule:"phony" ~inputs:[ Nj.Expr.Lit test_names ])
(Nj.Build.make_with_inputs ~outputs:[Nj.Expr.Lit test_name]
~rule:"phony" ~inputs:[Nj.Expr.Lit test_names])
ninja.builds;
} )
@ -527,9 +526,9 @@ let add_root_test_build
ninja with
builds =
Nj.BuildMap.add "test"
(Nj.Build.make_with_vars_and_inputs ~outputs:[ Nj.Expr.Lit "test" ]
(Nj.Build.make_with_vars_and_inputs ~outputs:[Nj.Expr.Lit "test"]
~rule:"run_and_display_final_message"
~inputs:[ Nj.Expr.Lit all_test_builds ]
~inputs:[Nj.Expr.Lit all_test_builds]
~vars:
[
( "test_file_or_folder",
@ -549,7 +548,7 @@ let run_file
String.concat " "
(List.filter
(fun s -> s <> "")
[ catala_exe; catala_opts; "-s " ^ scope; "Interpret"; file ])
[catala_exe; catala_opts; "-s " ^ scope; "Interpret"; file])
in
Cli.debug_print "Running: %s" command;
Sys.command command
@ -572,7 +571,7 @@ let get_catala_files_in_folder (dir : string) : string list =
else loop (f :: result) fs
| [] -> result
in
let all_files_in_folder = loop [] [ dir ] in
let all_files_in_folder = loop [] [dir] in
List.filter (Re.Pcre.pmatch ~rex:catala_suffix_regex) all_files_in_folder
type ninja_building_context = {
@ -611,9 +610,9 @@ let collect_in_folder
match collect_all_ninja_build ninja file reset_test_outputs with
| None ->
(* Skips none Catala file. *)
(ninja, test_file_names)
ninja, test_file_names
| Some (test_file_name, ninja) ->
(ninja, test_file_names ^ " $\n " ^ test_file_name))
ninja, test_file_names ^ " $\n " ^ test_file_name)
(ninja_start, "")
(get_catala_files_in_folder folder)
in
@ -629,9 +628,9 @@ let collect_in_folder
builds =
Nj.BuildMap.add test_dir_name
(Nj.Build.make_with_vars_and_inputs
~outputs:[ Nj.Expr.Lit test_dir_name ]
~outputs:[Nj.Expr.Lit test_dir_name]
~rule:"run_and_display_final_message"
~inputs:[ Nj.Expr.Lit test_file_names ]
~inputs:[Nj.Expr.Lit test_file_names]
~vars:
[
( "test_file_or_folder",
@ -714,15 +713,13 @@ let makeflags_to_ninja_flags (makeflags : string option) =
| Some makeflags ->
let ignore_rex = Re.(compile @@ word (char 'i')) in
let has_ignore = Re.execp ignore_rex makeflags in
let jobs_rex = Re.(compile @@ seq [ str "-j"; group (rep digit) ]) in
let jobs_rex = Re.(compile @@ seq [str "-j"; group (rep digit)]) in
let number_of_jobs =
try int_of_string (Re.Group.get (Re.exec jobs_rex makeflags) 1)
with _ -> 0
in
String.concat " "
[
(if has_ignore then "-k0" else ""); "-j" ^ string_of_int number_of_jobs;
]
[(if has_ignore then "-k0" else ""); "-j" ^ string_of_int number_of_jobs]
let driver
(files_or_folders : string list)
@ -762,7 +759,7 @@ let driver
List.iter
(fun f ->
f
|> Cli.with_style [ ANSITerminal.magenta ] "%s"
|> Cli.with_style [ANSITerminal.magenta] "%s"
|> Cli.warning_print "No test case found for %s")
ctx.all_failed_names;
if 0 = List.compare_lengths ctx.all_failed_names files_or_folders then

View File

@ -65,7 +65,7 @@ module Build = struct
let make_with_vars_and_inputs ~outputs ~rule ~inputs ~vars =
{ outputs; rule; inputs = Option.some inputs; vars }
let empty = make ~outputs:[ Expr.Lit "empty" ] ~rule:"phony"
let empty = make ~outputs:[Expr.Lit "empty"] ~rule:"phony"
let unpath ?(sep = "-") path =
Re.Pcre.(substitute ~rex:(regexp "/") ~subst:(fun _ -> sep)) path

View File

@ -25,7 +25,7 @@ let test_ninja_start () =
let test_add_test_builds_for_folder () =
let ctx = D.ninja_building_context_init ninja_start in
let nj_building_ctx =
To_test.add_test_builds ctx [ test_files_dir ^ "folder" ] false
To_test.add_test_builds ctx [test_files_dir ^ "folder"] false
in
al_assert "a test case should be found"
(Option.is_some nj_building_ctx.curr_ninja);
@ -47,7 +47,7 @@ let test_add_test_builds_for_folder () =
let test_add_test_builds_for_untested_file () =
let untested_file = test_files_dir ^ "untested_file.catala_en" in
let ctx = D.ninja_building_context_init Nj.empty in
let nj_building_ctx = To_test.add_test_builds ctx [ untested_file ] false in
let nj_building_ctx = To_test.add_test_builds ctx [untested_file] false in
al_assert "no test cases should be found"
(Option.is_none nj_building_ctx.curr_ninja);
@ -61,7 +61,7 @@ let test_add_test_builds_for_simple_interpret_scope_file () =
in
let ctx = D.ninja_building_context_init ninja_start in
let nj_building_ctx =
To_test.add_test_builds ctx [ simple_interpret_scope_file ] false
To_test.add_test_builds ctx [simple_interpret_scope_file] false
in
al_assert "a test case should be found"
(Option.is_some nj_building_ctx.curr_ninja);
@ -76,13 +76,13 @@ let test_add_test_builds_for_simple_interpret_scope_file () =
in
let test_A_file =
Build.make_with_vars
~outputs:[ Expr.Lit test_A_file_output ]
~outputs:[Expr.Lit test_A_file_output]
~rule:"test_with_scope"
~vars:
[
("scope", Lit "A");
("catala_cmd", Lit "Interpret");
("tested_file", Lit simple_interpret_scope_file);
"scope", Lit "A";
"catala_cmd", Lit "Interpret";
"tested_file", Lit simple_interpret_scope_file;
( "expected_output",
Lit
(test_files_dir
@ -91,9 +91,9 @@ let test_add_test_builds_for_simple_interpret_scope_file () =
in
let test_file =
Build.make_with_inputs
~outputs:[ Expr.Lit test_file_output ]
~outputs:[Expr.Lit test_file_output]
~rule:"phony"
~inputs:[ Expr.Lit (" $\n " ^ test_A_file_output) ]
~inputs:[Expr.Lit (" $\n " ^ test_A_file_output)]
in
BuildMap.empty
|> BuildMap.add test_file_output test_file

View File

@ -163,15 +163,13 @@ and 'expr scopes = Nil | ScopeDef of 'expr scope_def
type program = { decl_ctx : decl_ctx; scopes : expr scopes }
let evar (v : expr Bindlib.var) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun v' -> (v', pos)) (Bindlib.box_var v)
Bindlib.box_apply (fun v' -> v', pos) (Bindlib.box_var v)
let etuple
(args : expr Pos.marked Bindlib.box list)
(s : StructName.t option)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun args -> (ETuple (args, s), pos))
(Bindlib.box_list args)
Bindlib.box_apply (fun args -> ETuple (args, s), pos) (Bindlib.box_list args)
let etupleaccess
(e1 : expr Pos.marked Bindlib.box)
@ -179,7 +177,7 @@ let etupleaccess
(s : StructName.t option)
(typs : typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (ETupleAccess (e1, i, s, typs), pos)) e1
Bindlib.box_apply (fun e1 -> ETupleAccess (e1, i, s, typs), pos) e1
let einj
(e1 : expr Pos.marked Bindlib.box)
@ -187,7 +185,7 @@ let einj
(e_name : EnumName.t)
(typs : typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (EInj (e1, i, e_name, typs), pos)) e1
Bindlib.box_apply (fun e1 -> EInj (e1, i, e_name, typs), pos) e1
let ematch
(arg : expr Pos.marked Bindlib.box)
@ -195,12 +193,12 @@ let ematch
(e_name : EnumName.t)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun arg arms -> (EMatch (arg, arms, e_name), pos))
(fun arg arms -> EMatch (arg, arms, e_name), pos)
arg (Bindlib.box_list arms)
let earray (args : expr Pos.marked Bindlib.box list) (pos : Pos.t) :
expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun args -> (EArray args, pos)) (Bindlib.box_list args)
Bindlib.box_apply (fun args -> EArray args, pos) (Bindlib.box_list args)
let elit (l : lit) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (ELit l, pos)
@ -211,7 +209,7 @@ let eabs
(typs : typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun binder -> (EAbs ((binder, pos_binder), typs), pos))
(fun binder -> EAbs ((binder, pos_binder), typs), pos)
binder
let eapp
@ -219,12 +217,12 @@ let eapp
(args : expr Pos.marked Bindlib.box list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun e1 args -> (EApp (e1, args), pos))
(fun e1 args -> EApp (e1, args), pos)
e1 (Bindlib.box_list args)
let eassert (e1 : expr Pos.marked Bindlib.box) (pos : Pos.t) :
expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (EAssert e1, pos)) e1
Bindlib.box_apply (fun e1 -> EAssert e1, pos) e1
let eop (op : operator) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (EOp op, pos)
@ -235,7 +233,7 @@ let edefault
(cons : expr Pos.marked Bindlib.box)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply3
(fun excepts just cons -> (EDefault (excepts, just, cons), pos))
(fun excepts just cons -> EDefault (excepts, just, cons), pos)
(Bindlib.box_list excepts) just cons
let eifthenelse
@ -243,11 +241,11 @@ let eifthenelse
(e2 : expr Pos.marked Bindlib.box)
(e3 : expr Pos.marked Bindlib.box)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply3 (fun e1 e2 e3 -> (EIfThenElse (e1, e2, e3), pos)) e1 e2 e3
Bindlib.box_apply3 (fun e1 e2 e3 -> EIfThenElse (e1, e2, e3), pos) e1 e2 e3
let eerroronempty (e1 : expr Pos.marked Bindlib.box) (pos : Pos.t) :
expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (ErrorOnEmpty e1, pos)) e1
Bindlib.box_apply (fun e1 -> ErrorOnEmpty e1, pos) e1
let map_expr
(ctx : 'a)
@ -420,7 +418,7 @@ let rec free_vars_expr (e : expr Pos.marked) : VarSet.t =
|> List.fold_left VarSet.union VarSet.empty
| EOp _ | ELit _ -> VarSet.empty
| EIfThenElse (e1, e2, e3) ->
[ e1; e2; e3 ] |> List.map free_vars_expr
[e1; e2; e3] |> List.map free_vars_expr
|> List.fold_left VarSet.union VarSet.empty
| EAbs ((binder, _), _) ->
let vs, body = Bindlib.unmbind binder in
@ -452,7 +450,7 @@ let rec free_vars_scopes (scopes : expr scopes) : VarSet.t =
type vars = expr Bindlib.mvar
let make_var ((x, pos) : Var.t Pos.marked) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun x -> (x, pos)) (Bindlib.box_var x)
Bindlib.box_apply (fun x -> x, pos) (Bindlib.box_var x)
let make_abs
(xs : vars)
@ -461,14 +459,14 @@ let make_abs
(taus : typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun b -> (EAbs ((b, pos_binder), taus), pos))
(fun b -> EAbs ((b, pos_binder), taus), pos)
(Bindlib.bind_mvar xs e)
let make_app
(e : expr Pos.marked Bindlib.box)
(u : expr Pos.marked Bindlib.box list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2 (fun e u -> (EApp (e, u), pos)) e (Bindlib.box_list u)
Bindlib.box_apply2 (fun e u -> EApp (e, u), pos) e (Bindlib.box_list u)
let make_let_in
(x : Var.t)
@ -476,22 +474,22 @@ let make_let_in
(e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
make_app (make_abs (Array.of_list [ x ]) e2 pos [ tau ] pos) [ e1 ] pos
make_app (make_abs (Array.of_list [x]) e2 pos [tau] pos) [e1] pos
let empty_thunked_term : expr Pos.marked =
let silent = Var.make ("_", Pos.no_pos) in
Bindlib.unbox
(make_abs (Array.of_list [ silent ])
(make_abs (Array.of_list [silent])
(Bindlib.box (ELit LEmptyError, Pos.no_pos))
Pos.no_pos
[ (TLit TUnit, Pos.no_pos) ]
[TLit TUnit, Pos.no_pos]
Pos.no_pos)
let is_value (e : expr Pos.marked) : bool =
match Pos.unmark e with ELit _ | EAbs _ | EOp _ -> true | _ -> false
let rec equal_typs (ty1 : typ Pos.marked) (ty2 : typ Pos.marked) : bool =
match (Pos.unmark ty1, Pos.unmark ty2) with
match Pos.unmark ty1, Pos.unmark ty2 with
| TLit l1, TLit l2 -> l1 = l2
| TTuple (tys1, n1), TTuple (tys2, n2) -> n1 = n2 && equal_typs_list tys1 tys2
| TEnum (tys1, n1), TEnum (tys2, n2) -> n1 = n2 && equal_typs_list tys1 tys2
@ -508,12 +506,12 @@ and equal_typs_list (tys1 : typ Pos.marked list) (tys2 : typ Pos.marked list) :
List.for_all (fun (x, y) -> equal_typs x y) (List.combine tys1 tys2)
let equal_log_entries (l1 : log_entry) (l2 : log_entry) : bool =
match (l1, l2) with
match l1, l2 with
| VarDef t1, VarDef t2 -> equal_typs (t1, Pos.no_pos) (t2, Pos.no_pos)
| x, y -> x = y
let equal_unops (op1 : unop) (op2 : unop) : bool =
match (op1, op2) with
match op1, op2 with
(* Log entries contain a typ which contain position information, we thus need
to descend into them *)
| Log (l1, info1), Log (l2, info2) -> equal_log_entries l1 l2 && info1 = info2
@ -521,14 +519,14 @@ let equal_unops (op1 : unop) (op2 : unop) : bool =
| _ -> op1 = op2
let equal_ops (op1 : operator) (op2 : operator) : bool =
match (op1, op2) with
match op1, op2 with
| Ternop op1, Ternop op2 -> op1 = op2
| Binop op1, Binop op2 -> op1 = op2
| Unop op1, Unop op2 -> equal_unops op1 op2
| _, _ -> false
let rec equal_exprs (e1 : expr Pos.marked) (e2 : expr Pos.marked) : bool =
match (Pos.unmark e1, Pos.unmark e2) with
match Pos.unmark e1, Pos.unmark e2 with
| EVar v1, EVar v2 -> Pos.unmark v1 = Pos.unmark v2
| ETuple (es1, n1), ETuple (es2, n2) -> n1 = n2 && equal_exprs_list es1 es2
| ETupleAccess (e1, id1, n1, tys1), ETupleAccess (e2, id2, n2, tys2) ->
@ -610,7 +608,7 @@ let build_whole_scope_expr
(pos_scope : Pos.t) : 'expr Pos.marked Bindlib.box =
let var, body_expr = Bindlib.unbind body.scope_body_expr in
let body_expr = unfold_scope_body_expr ~box_expr ~make_let_in ctx body_expr in
make_abs (Array.of_list [ var ]) body_expr pos_scope
make_abs (Array.of_list [var]) body_expr pos_scope
[
( TTuple
( List.map snd
@ -630,12 +628,12 @@ let build_scope_typ_from_sig
StructMap.find scope_return_struct_name ctx.ctx_structs
in
let result_typ =
(TTuple (List.map snd scope_return_typ, Some scope_return_struct_name), pos)
TTuple (List.map snd scope_return_typ, Some scope_return_struct_name), pos
in
let input_typ =
(TTuple (List.map snd scope_sig, Some scope_input_struct_name), pos)
TTuple (List.map snd scope_sig, Some scope_input_struct_name), pos
in
(TArrow (input_typ, result_typ), pos)
TArrow (input_typ, result_typ), pos
type 'expr scope_name_or_var =
| ScopeName of ScopeName.t
@ -652,7 +650,7 @@ let rec unfold_scopes
| Nil -> (
match main_scope with
| ScopeVar v ->
Bindlib.box_apply (fun v -> (v, Pos.no_pos)) (Bindlib.box_var v)
Bindlib.box_apply (fun v -> v, Pos.no_pos) (Bindlib.box_var v)
| ScopeName _ -> failwith "should not happen")
| ScopeDef { scope_name; scope_body; scope_next } ->
let scope_var, scope_next = Bindlib.unbind scope_next in
@ -701,7 +699,7 @@ let rec expr_size (e : expr Pos.marked) : int =
let remove_logging_calls (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let rec f () e =
match Pos.unmark e with
| EApp ((EOp (Unop (Log _)), _), [ arg ]) -> map_expr () ~f arg
| EApp ((EOp (Unop (Log _)), _), [arg]) -> map_expr () ~f arg
| _ -> map_expr () ~f e
in
f () e

View File

@ -40,16 +40,16 @@ let rec evaluate_operator
with Division_by_zero ->
Errors.raise_multispanned_error
[
(Some "The division operator:", Pos.get_position op);
(Some "The null denominator:", Pos.get_position (List.nth args 1));
Some "The division operator:", Pos.get_position op;
Some "The null denominator:", Pos.get_position (List.nth args 1);
]
"division by zero at runtime"
in
let get_binop_args_pos (args : (A.expr * Pos.t) list) :
(string option * Pos.t) list =
[
(None, Pos.get_position (List.nth args 0));
(None, Pos.get_position (List.nth args 1));
None, Pos.get_position (List.nth args 0);
None, Pos.get_position (List.nth args 1);
]
in
(* Try to apply [cmp] and if a [UncomparableDurations] exceptions is catched,
@ -64,53 +64,53 @@ let rec evaluate_operator
precise number of days"
in
Pos.same_pos_as
(match (Pos.unmark op, List.map Pos.unmark args) with
| A.Ternop A.Fold, [ _f; _init; EArray es ] ->
(match Pos.unmark op, List.map Pos.unmark args with
| A.Ternop A.Fold, [_f; _init; EArray es] ->
Pos.unmark
(List.fold_left
(fun acc e' ->
evaluate_expr ctx
(Pos.same_pos_as (A.EApp (List.nth args 0, [ acc; e' ])) e'))
(Pos.same_pos_as (A.EApp (List.nth args 0, [acc; e'])) e'))
(List.nth args 1) es)
| A.Binop A.And, [ ELit (LBool b1); ELit (LBool b2) ] ->
| A.Binop A.And, [ELit (LBool b1); ELit (LBool b2)] ->
A.ELit (LBool (b1 && b2))
| A.Binop A.Or, [ ELit (LBool b1); ELit (LBool b2) ] ->
| A.Binop A.Or, [ELit (LBool b1); ELit (LBool b2)] ->
A.ELit (LBool (b1 || b2))
| A.Binop A.Xor, [ ELit (LBool b1); ELit (LBool b2) ] ->
| A.Binop A.Xor, [ELit (LBool b1); ELit (LBool b2)] ->
A.ELit (LBool (b1 <> b2))
| A.Binop (A.Add KInt), [ ELit (LInt i1); ELit (LInt i2) ] ->
| A.Binop (A.Add KInt), [ELit (LInt i1); ELit (LInt i2)] ->
A.ELit (LInt Runtime.(i1 +! i2))
| A.Binop (A.Sub KInt), [ ELit (LInt i1); ELit (LInt i2) ] ->
| A.Binop (A.Sub KInt), [ELit (LInt i1); ELit (LInt i2)] ->
A.ELit (LInt Runtime.(i1 -! i2))
| A.Binop (A.Mult KInt), [ ELit (LInt i1); ELit (LInt i2) ] ->
| A.Binop (A.Mult KInt), [ELit (LInt i1); ELit (LInt i2)] ->
A.ELit (LInt Runtime.(i1 *! i2))
| A.Binop (A.Div KInt), [ ELit (LInt i1); ELit (LInt i2) ] ->
| A.Binop (A.Div KInt), [ELit (LInt i1); ELit (LInt i2)] ->
apply_div_or_raise_err (fun _ -> A.ELit (LInt Runtime.(i1 /! i2))) op
| A.Binop (A.Add KRat), [ ELit (LRat i1); ELit (LRat i2) ] ->
| A.Binop (A.Add KRat), [ELit (LRat i1); ELit (LRat i2)] ->
A.ELit (LRat Runtime.(i1 +& i2))
| A.Binop (A.Sub KRat), [ ELit (LRat i1); ELit (LRat i2) ] ->
| A.Binop (A.Sub KRat), [ELit (LRat i1); ELit (LRat i2)] ->
A.ELit (LRat Runtime.(i1 -& i2))
| A.Binop (A.Mult KRat), [ ELit (LRat i1); ELit (LRat i2) ] ->
| A.Binop (A.Mult KRat), [ELit (LRat i1); ELit (LRat i2)] ->
A.ELit (LRat Runtime.(i1 *& i2))
| A.Binop (A.Div KRat), [ ELit (LRat i1); ELit (LRat i2) ] ->
| A.Binop (A.Div KRat), [ELit (LRat i1); ELit (LRat i2)] ->
apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(i1 /& i2))) op
| A.Binop (A.Add KMoney), [ ELit (LMoney m1); ELit (LMoney m2) ] ->
| A.Binop (A.Add KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
A.ELit (LMoney Runtime.(m1 +$ m2))
| A.Binop (A.Sub KMoney), [ ELit (LMoney m1); ELit (LMoney m2) ] ->
| A.Binop (A.Sub KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
A.ELit (LMoney Runtime.(m1 -$ m2))
| A.Binop (A.Mult KMoney), [ ELit (LMoney m1); ELit (LRat m2) ] ->
| A.Binop (A.Mult KMoney), [ELit (LMoney m1); ELit (LRat m2)] ->
A.ELit (LMoney Runtime.(m1 *$ m2))
| A.Binop (A.Div KMoney), [ ELit (LMoney m1); ELit (LMoney m2) ] ->
| A.Binop (A.Div KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(m1 /$ m2))) op
| A.Binop (A.Add KDuration), [ ELit (LDuration d1); ELit (LDuration d2) ] ->
| A.Binop (A.Add KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
A.ELit (LDuration Runtime.(d1 +^ d2))
| A.Binop (A.Sub KDuration), [ ELit (LDuration d1); ELit (LDuration d2) ] ->
| A.Binop (A.Sub KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
A.ELit (LDuration Runtime.(d1 -^ d2))
| A.Binop (A.Sub KDate), [ ELit (LDate d1); ELit (LDate d2) ] ->
| A.Binop (A.Sub KDate), [ELit (LDate d1); ELit (LDate d2)] ->
A.ELit (LDuration Runtime.(d1 -@ d2))
| A.Binop (A.Add KDate), [ ELit (LDate d1); ELit (LDuration d2) ] ->
| A.Binop (A.Add KDate), [ELit (LDate d1); ELit (LDuration d2)] ->
A.ELit (LDate Runtime.(d1 +@ d2))
| A.Binop (A.Div KDuration), [ ELit (LDuration d1); ELit (LDuration d2) ] ->
| A.Binop (A.Div KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
apply_div_or_raise_err
(fun _ ->
try A.ELit (LRat Runtime.(d1 /^ d2))
@ -119,119 +119,119 @@ let rec evaluate_operator
"Cannot divide durations that cannot be converted to a precise \
number of days")
op
| A.Binop (A.Lt KInt), [ ELit (LInt i1); ELit (LInt i2) ] ->
| A.Binop (A.Lt KInt), [ELit (LInt i1); ELit (LInt i2)] ->
A.ELit (LBool Runtime.(i1 <! i2))
| A.Binop (A.Lte KInt), [ ELit (LInt i1); ELit (LInt i2) ] ->
| A.Binop (A.Lte KInt), [ELit (LInt i1); ELit (LInt i2)] ->
A.ELit (LBool Runtime.(i1 <=! i2))
| A.Binop (A.Gt KInt), [ ELit (LInt i1); ELit (LInt i2) ] ->
| A.Binop (A.Gt KInt), [ELit (LInt i1); ELit (LInt i2)] ->
A.ELit (LBool Runtime.(i1 >! i2))
| A.Binop (A.Gte KInt), [ ELit (LInt i1); ELit (LInt i2) ] ->
| A.Binop (A.Gte KInt), [ELit (LInt i1); ELit (LInt i2)] ->
A.ELit (LBool Runtime.(i1 >=! i2))
| A.Binop (A.Lt KRat), [ ELit (LRat i1); ELit (LRat i2) ] ->
| A.Binop (A.Lt KRat), [ELit (LRat i1); ELit (LRat i2)] ->
A.ELit (LBool Runtime.(i1 <& i2))
| A.Binop (A.Lte KRat), [ ELit (LRat i1); ELit (LRat i2) ] ->
| A.Binop (A.Lte KRat), [ELit (LRat i1); ELit (LRat i2)] ->
A.ELit (LBool Runtime.(i1 <=& i2))
| A.Binop (A.Gt KRat), [ ELit (LRat i1); ELit (LRat i2) ] ->
| A.Binop (A.Gt KRat), [ELit (LRat i1); ELit (LRat i2)] ->
A.ELit (LBool Runtime.(i1 >& i2))
| A.Binop (A.Gte KRat), [ ELit (LRat i1); ELit (LRat i2) ] ->
| A.Binop (A.Gte KRat), [ELit (LRat i1); ELit (LRat i2)] ->
A.ELit (LBool Runtime.(i1 >=& i2))
| A.Binop (A.Lt KMoney), [ ELit (LMoney m1); ELit (LMoney m2) ] ->
| A.Binop (A.Lt KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
A.ELit (LBool Runtime.(m1 <$ m2))
| A.Binop (A.Lte KMoney), [ ELit (LMoney m1); ELit (LMoney m2) ] ->
| A.Binop (A.Lte KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
A.ELit (LBool Runtime.(m1 <=$ m2))
| A.Binop (A.Gt KMoney), [ ELit (LMoney m1); ELit (LMoney m2) ] ->
| A.Binop (A.Gt KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
A.ELit (LBool Runtime.(m1 >$ m2))
| A.Binop (A.Gte KMoney), [ ELit (LMoney m1); ELit (LMoney m2) ] ->
| A.Binop (A.Gte KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
A.ELit (LBool Runtime.(m1 >=$ m2))
| A.Binop (A.Lt KDuration), [ ELit (LDuration d1); ELit (LDuration d2) ] ->
| A.Binop (A.Lt KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
apply_cmp_or_raise_err (fun _ -> A.ELit (LBool Runtime.(d1 <^ d2))) args
| A.Binop (A.Lte KDuration), [ ELit (LDuration d1); ELit (LDuration d2) ] ->
| A.Binop (A.Lte KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
apply_cmp_or_raise_err (fun _ -> A.ELit (LBool Runtime.(d1 <=^ d2))) args
| A.Binop (A.Gt KDuration), [ ELit (LDuration d1); ELit (LDuration d2) ] ->
| A.Binop (A.Gt KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
apply_cmp_or_raise_err (fun _ -> A.ELit (LBool Runtime.(d1 >^ d2))) args
| A.Binop (A.Gte KDuration), [ ELit (LDuration d1); ELit (LDuration d2) ] ->
| A.Binop (A.Gte KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
apply_cmp_or_raise_err (fun _ -> A.ELit (LBool Runtime.(d1 >=^ d2))) args
| A.Binop (A.Lt KDate), [ ELit (LDate d1); ELit (LDate d2) ] ->
| A.Binop (A.Lt KDate), [ELit (LDate d1); ELit (LDate d2)] ->
A.ELit (LBool Runtime.(d1 <@ d2))
| A.Binop (A.Lte KDate), [ ELit (LDate d1); ELit (LDate d2) ] ->
| A.Binop (A.Lte KDate), [ELit (LDate d1); ELit (LDate d2)] ->
A.ELit (LBool Runtime.(d1 <=@ d2))
| A.Binop (A.Gt KDate), [ ELit (LDate d1); ELit (LDate d2) ] ->
| A.Binop (A.Gt KDate), [ELit (LDate d1); ELit (LDate d2)] ->
A.ELit (LBool Runtime.(d1 >@ d2))
| A.Binop (A.Gte KDate), [ ELit (LDate d1); ELit (LDate d2) ] ->
| A.Binop (A.Gte KDate), [ELit (LDate d1); ELit (LDate d2)] ->
A.ELit (LBool Runtime.(d1 >=@ d2))
| A.Binop A.Eq, [ ELit LUnit; ELit LUnit ] -> A.ELit (LBool true)
| A.Binop A.Eq, [ ELit (LDuration d1); ELit (LDuration d2) ] ->
| A.Binop A.Eq, [ELit LUnit; ELit LUnit] -> A.ELit (LBool true)
| A.Binop A.Eq, [ELit (LDuration d1); ELit (LDuration d2)] ->
A.ELit (LBool Runtime.(d1 =^ d2))
| A.Binop A.Eq, [ ELit (LDate d1); ELit (LDate d2) ] ->
| A.Binop A.Eq, [ELit (LDate d1); ELit (LDate d2)] ->
A.ELit (LBool Runtime.(d1 =@ d2))
| A.Binop A.Eq, [ ELit (LMoney m1); ELit (LMoney m2) ] ->
| A.Binop A.Eq, [ELit (LMoney m1); ELit (LMoney m2)] ->
A.ELit (LBool Runtime.(m1 =$ m2))
| A.Binop A.Eq, [ ELit (LRat i1); ELit (LRat i2) ] ->
| A.Binop A.Eq, [ELit (LRat i1); ELit (LRat i2)] ->
A.ELit (LBool Runtime.(i1 =& i2))
| A.Binop A.Eq, [ ELit (LInt i1); ELit (LInt i2) ] ->
| A.Binop A.Eq, [ELit (LInt i1); ELit (LInt i2)] ->
A.ELit (LBool Runtime.(i1 =! i2))
| A.Binop A.Eq, [ ELit (LBool b1); ELit (LBool b2) ] ->
| A.Binop A.Eq, [ELit (LBool b1); ELit (LBool b2)] ->
A.ELit (LBool (b1 = b2))
| A.Binop A.Eq, [ EArray es1; EArray es2 ] ->
| A.Binop A.Eq, [EArray es1; EArray es2] ->
A.ELit
(LBool
(try
List.for_all2
(fun e1 e2 ->
match Pos.unmark (evaluate_operator ctx op [ e1; e2 ]) with
match Pos.unmark (evaluate_operator ctx op [e1; e2]) with
| A.ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
es1 es2
with Invalid_argument _ -> false))
| A.Binop A.Eq, [ ETuple (es1, s1); ETuple (es2, s2) ] ->
| A.Binop A.Eq, [ETuple (es1, s1); ETuple (es2, s2)] ->
A.ELit
(LBool
(try
s1 = s2
&& List.for_all2
(fun e1 e2 ->
match Pos.unmark (evaluate_operator ctx op [ e1; e2 ]) with
match Pos.unmark (evaluate_operator ctx op [e1; e2]) with
| A.ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
es1 es2
with Invalid_argument _ -> false))
| A.Binop A.Eq, [ EInj (e1, i1, en1, _ts1); EInj (e2, i2, en2, _ts2) ] ->
| A.Binop A.Eq, [EInj (e1, i1, en1, _ts1); EInj (e2, i2, en2, _ts2)] ->
A.ELit
(LBool
(try
en1 = en2 && i1 = i2
&&
match Pos.unmark (evaluate_operator ctx op [ e1; e2 ]) with
match Pos.unmark (evaluate_operator ctx op [e1; e2]) with
| A.ELit (LBool b) -> b
| _ -> assert false
(* should not happen *)
with Invalid_argument _ -> false))
| A.Binop A.Eq, [ _; _ ] ->
| A.Binop A.Eq, [_; _] ->
A.ELit (LBool false) (* comparing anything else return false *)
| A.Binop A.Neq, [ _; _ ] -> (
| A.Binop A.Neq, [_; _] -> (
match
Pos.unmark
(evaluate_operator ctx (Pos.same_pos_as (A.Binop A.Eq) op) args)
with
| A.ELit (A.LBool b) -> A.ELit (A.LBool (not b))
| _ -> assert false (*should not happen *))
| A.Binop A.Concat, [ A.EArray es1; A.EArray es2 ] -> A.EArray (es1 @ es2)
| A.Binop A.Map, [ _; A.EArray es ] ->
| A.Binop A.Concat, [A.EArray es1; A.EArray es2] -> A.EArray (es1 @ es2)
| A.Binop A.Map, [_; A.EArray es] ->
A.EArray
(List.map
(fun e' ->
evaluate_expr ctx
(Pos.same_pos_as (A.EApp (List.nth args 0, [ e' ])) e'))
(Pos.same_pos_as (A.EApp (List.nth args 0, [e'])) e'))
es)
| A.Binop A.Filter, [ _; A.EArray es ] ->
| A.Binop A.Filter, [_; A.EArray es] ->
A.EArray
(List.filter
(fun e' ->
match
evaluate_expr ctx
(Pos.same_pos_as (A.EApp (List.nth args 0, [ e' ])) e')
(Pos.same_pos_as (A.EApp (List.nth args 0, [e'])) e')
with
| A.ELit (A.LBool b), _ -> b
| _ ->
@ -240,32 +240,32 @@ let rec evaluate_operator
"This predicate evaluated to something else than a boolean \
(should not happen if the term was well-typed)")
es)
| A.Binop _, ([ ELit LEmptyError; _ ] | [ _; ELit LEmptyError ]) ->
| A.Binop _, ([ELit LEmptyError; _] | [_; ELit LEmptyError]) ->
A.ELit LEmptyError
| A.Unop (A.Minus KInt), [ ELit (LInt i) ] ->
| A.Unop (A.Minus KInt), [ELit (LInt i)] ->
A.ELit (LInt Runtime.(integer_of_int 0 -! i))
| A.Unop (A.Minus KRat), [ ELit (LRat i) ] ->
| A.Unop (A.Minus KRat), [ELit (LRat i)] ->
A.ELit (LRat Runtime.(decimal_of_string "0" -& i))
| A.Unop (A.Minus KMoney), [ ELit (LMoney i) ] ->
| A.Unop (A.Minus KMoney), [ELit (LMoney i)] ->
A.ELit (LMoney Runtime.(money_of_units_int 0 -$ i))
| A.Unop (A.Minus KDuration), [ ELit (LDuration i) ] ->
| A.Unop (A.Minus KDuration), [ELit (LDuration i)] ->
A.ELit (LDuration Runtime.(~-^i))
| A.Unop A.Not, [ ELit (LBool b) ] -> A.ELit (LBool (not b))
| A.Unop A.Length, [ EArray es ] ->
| A.Unop A.Not, [ELit (LBool b)] -> A.ELit (LBool (not b))
| A.Unop A.Length, [EArray es] ->
A.ELit (LInt (Runtime.integer_of_int (List.length es)))
| A.Unop A.GetDay, [ ELit (LDate d) ] ->
| A.Unop A.GetDay, [ELit (LDate d)] ->
A.ELit (LInt Runtime.(day_of_month_of_date d))
| A.Unop A.GetMonth, [ ELit (LDate d) ] ->
| A.Unop A.GetMonth, [ELit (LDate d)] ->
A.ELit (LInt Runtime.(month_number_of_date d))
| A.Unop A.GetYear, [ ELit (LDate d) ] ->
| A.Unop A.GetYear, [ELit (LDate d)] ->
A.ELit (LInt Runtime.(year_of_date d))
| A.Unop A.IntToRat, [ ELit (LInt i) ] ->
| A.Unop A.IntToRat, [ELit (LInt i)] ->
A.ELit (LRat Runtime.(decimal_of_integer i))
| A.Unop A.RoundMoney, [ ELit (LMoney m) ] ->
| A.Unop A.RoundMoney, [ELit (LMoney m)] ->
A.ELit (LMoney Runtime.(money_round m))
| A.Unop A.RoundDecimal, [ ELit (LRat m) ] ->
| A.Unop A.RoundDecimal, [ELit (LRat m)] ->
A.ELit (LRat Runtime.(decimal_round m))
| A.Unop (A.Log (entry, infos)), [ e' ] ->
| A.Unop (A.Log (entry, infos)), [e'] ->
if !Cli.trace_flag then (
match entry with
| VarDef _ ->
@ -288,14 +288,14 @@ let rec evaluate_operator
~subst:(fun _ -> " ")
expr_str
in
Cli.with_style [ ANSITerminal.green ] "%s" expr_str)
Cli.with_style [ANSITerminal.green] "%s" expr_str)
| PosRecordIfTrueBool -> (
let pos = Pos.get_position op in
match (pos <> Pos.no_pos, e') with
match pos <> Pos.no_pos, e' with
| true, ELit (LBool true) ->
Cli.log_format "%*s%a%s:\n%s" (!log_indent * 2) ""
Print.format_log_entry entry
(Cli.with_style [ ANSITerminal.green ] "Definition applied")
(Cli.with_style [ANSITerminal.green] "Definition applied")
(Cli.add_prefix_to_each_line (Pos.retrieve_loc_text pos) (fun _ ->
Format.asprintf "%*s" (!log_indent * 2) ""))
| _ -> ())
@ -309,10 +309,10 @@ let rec evaluate_operator
entry Print.format_uid_list infos)
else ();
e'
| A.Unop _, [ ELit LEmptyError ] -> A.ELit LEmptyError
| A.Unop _, [ELit LEmptyError] -> A.ELit LEmptyError
| _ ->
Errors.raise_multispanned_error
([ (Some "Operator:", Pos.get_position op) ]
([Some "Operator:", Pos.get_position op]
@ List.mapi
(fun i arg ->
( Some
@ -364,12 +364,12 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) :
let e1 = evaluate_expr ctx e1 in
match Pos.unmark e1 with
| ETuple (es, s') -> (
(match (s, s') with
(match s, s' with
| None, None -> ()
| Some s, Some s' when s = s' -> ()
| _ ->
Errors.raise_multispanned_error
[ (None, Pos.get_position e); (None, Pos.get_position e1) ]
[None, Pos.get_position e; None, Pos.get_position e1]
"Error during tuple access: not the same structs (should not happen \
if the term was well-typed)");
match List.nth_opt es n with
@ -396,7 +396,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) :
| A.EInj (e1, n, e_name', _) ->
if e_name <> e_name' then
Errors.raise_multispanned_error
[ (None, Pos.get_position e); (None, Pos.get_position e1) ]
[None, Pos.get_position e; None, Pos.get_position e1]
"Error during match: two different enums found (should not happend \
if the term was well-typed)";
let es_n =
@ -407,7 +407,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) :
"sum type index error (should not happend if the term was \
well-typed)"
in
let new_e = Pos.same_pos_as (A.EApp (es_n, [ e1 ])) e in
let new_e = Pos.same_pos_as (A.EApp (es_n, [e1])) e in
evaluate_expr ctx new_e
| A.ELit A.LEmptyError -> Pos.same_pos_as (A.ELit A.LEmptyError) e
| _ ->
@ -466,7 +466,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) :
match Pos.unmark e' with
| EApp
( (Ast.EOp (Binop op), pos_op),
[ ((ELit _, _) as e1); ((ELit _, _) as e2) ] ) ->
[((ELit _, _) as e1); ((ELit _, _) as e2)] ) ->
Errors.raise_spanned_error (Pos.get_position e')
"Assertion failed: %a %a %a"
(Print.format_expr ctx ~debug:false)
@ -486,10 +486,10 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) :
let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Pos.marked) :
(Uid.MarkedString.info * Ast.expr Pos.marked) list =
match Pos.unmark (evaluate_expr ctx e) with
| Ast.EAbs (_, [ (Ast.TTuple (taus, Some s_in), _) ]) -> (
| Ast.EAbs (_, [(Ast.TTuple (taus, Some s_in), _)]) -> (
let application_term = List.map (fun _ -> Ast.empty_thunked_term) taus in
let to_interpret =
( Ast.EApp (e, [ (Ast.ETuple (application_term, Some s_in), Pos.no_pos) ]),
( Ast.EApp (e, [Ast.ETuple (application_term, Some s_in), Pos.no_pos]),
Pos.no_pos )
in
match Pos.unmark (evaluate_expr ctx to_interpret) with
@ -499,7 +499,7 @@ let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Pos.marked) :
(fun (f, _) -> Ast.StructFieldName.get_info f)
(Ast.StructMap.find s_out ctx.ctx_structs)
in
List.map2 (fun arg var -> (var, arg)) args s_out_fields
List.map2 (fun arg var -> var, arg) args s_out_fields
| _ ->
Errors.raise_spanned_error (Pos.get_position e)
"The interpretation of a program should always yield a struct \

View File

@ -29,68 +29,68 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked)
match Pos.unmark e with
| EApp
( (( EOp (Unop Not), _
| EApp ((EOp (Unop (Log _)), _), [ (EOp (Unop Not), _) ]), _ ) as op),
[ e1 ] ) ->
| EApp ((EOp (Unop (Log _)), _), [(EOp (Unop Not), _)]), _ ) as op),
[e1] ) ->
(* reduction of logical not *)
(Bindlib.box_apply (fun e1 ->
match e1 with
| ELit (LBool false), _ -> (ELit (LBool true), pos)
| ELit (LBool true), _ -> (ELit (LBool false), pos)
| _ -> (EApp (op, [ e1 ]), pos)))
| ELit (LBool false), _ -> ELit (LBool true), pos
| ELit (LBool true), _ -> ELit (LBool false), pos
| _ -> EApp (op, [e1]), pos))
(rec_helper e1)
| EApp
( (( EOp (Binop Or), _
| EApp ((EOp (Unop (Log _)), _), [ (EOp (Binop Or), _) ]), _ ) as op),
[ e1; e2 ] ) ->
| EApp ((EOp (Unop (Log _)), _), [(EOp (Binop Or), _)]), _ ) as op),
[e1; e2] ) ->
(* reduction of logical or *)
(Bindlib.box_apply2 (fun e1 e2 ->
match (e1, e2) with
match e1, e2 with
| (ELit (LBool false), _), new_e | new_e, (ELit (LBool false), _) ->
new_e
| (ELit (LBool true), _), _ | _, (ELit (LBool true), _) ->
(ELit (LBool true), pos)
| _ -> (EApp (op, [ e1; e2 ]), pos)))
ELit (LBool true), pos
| _ -> EApp (op, [e1; e2]), pos))
(rec_helper e1) (rec_helper e2)
| EApp
( (( EOp (Binop And), _
| EApp ((EOp (Unop (Log _)), _), [ (EOp (Binop And), _) ]), _ ) as op),
[ e1; e2 ] ) ->
| EApp ((EOp (Unop (Log _)), _), [(EOp (Binop And), _)]), _ ) as op),
[e1; e2] ) ->
(* reduction of logical and *)
(Bindlib.box_apply2 (fun e1 e2 ->
match (e1, e2) with
match e1, e2 with
| (ELit (LBool true), _), new_e | new_e, (ELit (LBool true), _) ->
new_e
| (ELit (LBool false), _), _ | _, (ELit (LBool false), _) ->
(ELit (LBool false), pos)
| _ -> (EApp (op, [ e1; e2 ]), pos)))
ELit (LBool false), pos
| _ -> EApp (op, [e1; e2]), pos))
(rec_helper e1) (rec_helper e2)
| EVar (x, _) -> Bindlib.box_apply (fun x -> (x, pos)) (Bindlib.box_var x)
| EVar (x, _) -> Bindlib.box_apply (fun x -> x, pos) (Bindlib.box_var x)
| ETuple (args, s_name) ->
Bindlib.box_apply
(fun args -> (ETuple (args, s_name), pos))
(fun args -> ETuple (args, s_name), pos)
(List.map rec_helper args |> Bindlib.box_list)
| ETupleAccess (arg, i, s_name, typs) ->
Bindlib.box_apply
(fun arg -> (ETupleAccess (arg, i, s_name, typs), pos))
(fun arg -> ETupleAccess (arg, i, s_name, typs), pos)
(rec_helper arg)
| EInj (arg, i, e_name, typs) ->
Bindlib.box_apply
(fun arg -> (EInj (arg, i, e_name, typs), pos))
(fun arg -> EInj (arg, i, e_name, typs), pos)
(rec_helper arg)
| EMatch (arg, arms, e_name) ->
Bindlib.box_apply2
(fun arg arms ->
match (arg, arms) with
match arg, arms with
| (EInj (e1, i, e_name', _ts), _), _
when Ast.EnumName.compare e_name e_name' = 0 ->
(* iota reduction *)
(EApp (List.nth arms i, [ e1 ]), pos)
| _ -> (EMatch (arg, arms, e_name), pos))
EApp (List.nth arms i, [e1]), pos
| _ -> EMatch (arg, arms, e_name), pos)
(rec_helper arg)
(List.map rec_helper arms |> Bindlib.box_list)
| EArray args ->
Bindlib.box_apply
(fun args -> (EArray args, pos))
(fun args -> EArray args, pos)
(List.map rec_helper args |> Bindlib.box_list)
| ELit l -> Bindlib.box (ELit l, pos)
| EAbs ((binder, binder_pos), typs) ->
@ -98,7 +98,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked)
let new_body = rec_helper body in
let new_binder = Bindlib.bind_mvar vars new_body in
Bindlib.box_apply
(fun binder -> (EAbs ((binder, binder_pos), typs), pos))
(fun binder -> EAbs ((binder, binder_pos), typs), pos)
new_binder
| EApp (f, args) ->
Bindlib.box_apply2
@ -107,11 +107,10 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked)
| EAbs ((binder, _pos_binder), _ts) ->
(* beta reduction *)
Bindlib.msubst binder (List.map fst args |> Array.of_list)
| _ -> (EApp (f, args), pos))
| _ -> EApp (f, args), pos)
(rec_helper f)
(List.map rec_helper args |> Bindlib.box_list)
| EAssert e1 ->
Bindlib.box_apply (fun e1 -> (EAssert e1, pos)) (rec_helper e1)
| EAssert e1 -> Bindlib.box_apply (fun e1 -> EAssert e1, pos) (rec_helper e1)
| EOp op -> Bindlib.box (EOp op, pos)
| EDefault (exceptions, just, cons) ->
Bindlib.box_apply3
@ -138,53 +137,53 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked)
beautiful right error message *)
Interpreter.evaluate_expr ctx.decl_ctx
(EDefault (exceptions, just, cons), pos)
| [ except ], _, _ when is_value except ->
| [except], _, _ when is_value except ->
(* if there is only one exception and it is a non-empty value it is
always chosen *)
except
| ( [],
( ( ELit (LBool true)
| EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ]) ),
| EApp ((EOp (Unop (Log _)), _), [(ELit (LBool true), _)]) ),
_ ),
cons ) ->
cons
| ( [],
( ( ELit (LBool false)
| EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ]) ),
| EApp ((EOp (Unop (Log _)), _), [(ELit (LBool false), _)]) ),
_ ),
_ ) ->
(ELit LEmptyError, pos)
ELit LEmptyError, pos
| [], just, cons when not !Cli.avoid_exceptions_flag ->
(* without exceptions, a default is just an [if then else] raising an
error in the else case. This exception is only valid in the context
of compilation_with_exceptions, so we desactivate with a global
flag to know if we will be compiling using exceptions or the option
monad. *)
(EIfThenElse (just, cons, (ELit LEmptyError, pos)), pos)
| exceptions, just, cons -> (EDefault (exceptions, just, cons), pos))
EIfThenElse (just, cons, (ELit LEmptyError, pos)), pos
| exceptions, just, cons -> EDefault (exceptions, just, cons), pos)
(List.map rec_helper exceptions |> Bindlib.box_list)
(rec_helper just) (rec_helper cons)
| EIfThenElse (e1, e2, e3) ->
Bindlib.box_apply3
(fun e1 e2 e3 ->
match (Pos.unmark e1, Pos.unmark e2, Pos.unmark e3) with
match Pos.unmark e1, Pos.unmark e2, Pos.unmark e3 with
| ELit (LBool true), _, _
| EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ]), _, _ ->
| EApp ((EOp (Unop (Log _)), _), [(ELit (LBool true), _)]), _, _ ->
e2
| ELit (LBool false), _, _
| EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ]), _, _ ->
| EApp ((EOp (Unop (Log _)), _), [(ELit (LBool false), _)]), _, _ ->
e3
| ( _,
( ELit (LBool true)
| EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ]) ),
| EApp ((EOp (Unop (Log _)), _), [(ELit (LBool true), _)]) ),
( ELit (LBool false)
| EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ]) ) ) ->
| EApp ((EOp (Unop (Log _)), _), [(ELit (LBool false), _)]) ) ) ->
e1
| _ when equal_exprs e2 e3 -> e2
| _ -> (EIfThenElse (e1, e2, e3), pos))
| _ -> EIfThenElse (e1, e2, e3), pos)
(rec_helper e1) (rec_helper e2) (rec_helper e3)
| ErrorOnEmpty e1 ->
Bindlib.box_apply (fun e1 -> (ErrorOnEmpty e1, pos)) (rec_helper e1)
Bindlib.box_apply (fun e1 -> ErrorOnEmpty e1, pos) (rec_helper e1)
let optimize_expr (decl_ctx : decl_ctx) (e : expr Pos.marked) =
partial_evaluation { var_values = VarMap.empty; decl_ctx } e

View File

@ -42,29 +42,25 @@ let format_uid_list
Format.fprintf fmt "%a"
(Utils.Cli.format_with_style
(if begins_with_uppercase (Pos.unmark info) then
[ ANSITerminal.red ]
[ANSITerminal.red]
else []))
(Format.asprintf "%a" Utils.Uid.MarkedString.format_info info)))
infos
let format_keyword (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ ANSITerminal.red ]) s
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ANSITerminal.red]) s
let format_base_type (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%a"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
s
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ANSITerminal.yellow]) s
let format_punctuation (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ ANSITerminal.cyan ]) s
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ANSITerminal.cyan]) s
let format_operator (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ ANSITerminal.green ]) s
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ANSITerminal.green]) s
let format_lit_style (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%a"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
s
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ANSITerminal.yellow]) s
let format_tlit (fmt : Format.formatter) (l : typ_lit) : unit =
format_base_type fmt
@ -80,7 +76,7 @@ let format_tlit (fmt : Format.formatter) (l : typ_lit) : unit =
let format_enum_constructor (fmt : Format.formatter) (c : EnumConstructor.t) :
unit =
Format.fprintf fmt "%a"
(Utils.Cli.format_with_style [ ANSITerminal.magenta ])
(Utils.Cli.format_with_style [ANSITerminal.magenta])
(Format.asprintf "%a" EnumConstructor.format_t c)
let rec format_typ
@ -188,10 +184,10 @@ let format_ternop (fmt : Format.formatter) (op : ternop Pos.marked) : unit =
let format_log_entry (fmt : Format.formatter) (entry : log_entry) : unit =
Format.fprintf fmt "@<2>%s"
(match entry with
| VarDef _ -> Utils.Cli.with_style [ ANSITerminal.blue ] ""
| BeginCall -> Utils.Cli.with_style [ ANSITerminal.yellow ] ""
| EndCall -> Utils.Cli.with_style [ ANSITerminal.yellow ] ""
| PosRecordIfTrueBool -> Utils.Cli.with_style [ ANSITerminal.green ] "")
| VarDef _ -> Utils.Cli.with_style [ANSITerminal.blue] ""
| BeginCall -> Utils.Cli.with_style [ANSITerminal.yellow] ""
| EndCall -> Utils.Cli.with_style [ANSITerminal.yellow] ""
| PosRecordIfTrueBool -> Utils.Cli.with_style [ANSITerminal.green] "")
let format_unop (fmt : Format.formatter) (op : unop Pos.marked) : unit =
Format.fprintf fmt "%s"
@ -281,10 +277,8 @@ let rec format_expr
| ELit l -> format_lit fmt (Pos.same_pos_as l e)
| EApp ((EAbs ((binder, _), taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
let xs_tau_arg =
List.map2 (fun (x, tau) arg -> (x, tau, arg)) xs_tau args
in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in
Format.fprintf fmt "%a%a"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "")
@ -296,7 +290,7 @@ let rec format_expr
xs_tau_arg format_expr body
| EAbs ((binder, _), taus) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
Format.fprintf fmt "@[<hov 2>%a @[<hov 2>%a@] %a@ %a@]" format_punctuation
"λ"
(Format.pp_print_list
@ -305,15 +299,15 @@ let rec format_expr
Format.fprintf fmt "%a%a%a %a%a" format_punctuation "(" format_var x
format_punctuation ":" (format_typ ctx) tau format_punctuation ")"))
xs_tau format_punctuation "" format_expr body
| EApp ((EOp (Binop ((Ast.Map | Ast.Filter) as op)), _), [ arg1; arg2 ]) ->
| EApp ((EOp (Binop ((Ast.Map | Ast.Filter) as op)), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_binop (op, Pos.no_pos)
format_with_parens arg1 format_with_parens arg2
| EApp ((EOp (Binop op), _), [ arg1; arg2 ]) ->
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1
format_binop (op, Pos.no_pos) format_with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [ arg1 ]) when not debug ->
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug ->
format_expr fmt arg1
| EApp ((EOp (Unop op), _), [ arg1 ]) ->
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_unop (op, Pos.no_pos)
format_with_parens arg1
| EApp (f, args) ->

View File

@ -88,30 +88,30 @@ let rec unify
(* TODO: if we get weird error messages, then it means that we should use
the persistent version of the union-find data structure. *)
let t1_s =
Cli.with_style [ ANSITerminal.yellow ] "%s"
Cli.with_style [ANSITerminal.yellow] "%s"
(Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
~subst:(fun _ -> " ")
(Format.asprintf "%a" (format_typ ctx) t1))
in
let t2_s =
Cli.with_style [ ANSITerminal.yellow ] "%s"
Cli.with_style [ANSITerminal.yellow] "%s"
(Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
~subst:(fun _ -> " ")
(Format.asprintf "%a" (format_typ ctx) t2))
in
Errors.raise_multispanned_error
[
(Some (Format.asprintf "Type %s coming from expression:" t1_s), t1_pos);
(Some (Format.asprintf "Type %s coming from expression:" t2_s), t2_pos);
Some (Format.asprintf "Type %s coming from expression:" t1_s), t1_pos;
Some (Format.asprintf "Type %s coming from expression:" t2_s), t2_pos;
]
"Error during typechecking, incompatible types:\n%a %s\n%a %s"
(Cli.format_with_style [ ANSITerminal.blue; ANSITerminal.Bold ])
(Cli.format_with_style [ANSITerminal.blue; ANSITerminal.Bold])
"-->" t1_s
(Cli.format_with_style [ ANSITerminal.blue; ANSITerminal.Bold ])
(Cli.format_with_style [ANSITerminal.blue; ANSITerminal.Bold])
"-->" t2_s
in
let repr =
match (t1_repr, t2_repr) with
match t1_repr, t2_repr with
| (TLit tl1, _), (TLit tl2, _) when tl1 = tl2 -> None
| (TArrow (t11, t12), _), (TArrow (t21, t22), _) ->
unify t11 t21;
@ -493,7 +493,7 @@ and typecheck_expr_top_down
let xstaus =
List.map2
(fun x t_arg ->
(x, UnionFind.make (Pos.map_under_mark ast_to_typ t_arg)))
x, UnionFind.make (Pos.map_under_mark ast_to_typ t_arg))
(Array.to_list xs) t_args
in
let env =

View File

@ -53,7 +53,7 @@ module ScopeDef = struct
subscope's original declaration *)
let compare x y =
match (x, y) with
match x, y with
| Var (x, None), Var (y, None)
| Var (x, Some _), Var (y, None)
| Var (x, None), Var (y, Some _)
@ -108,7 +108,7 @@ Set.Make (struct
type t = location Pos.marked
let compare x y =
match (Pos.unmark x, Pos.unmark y) with
match Pos.unmark x, Pos.unmark y with
| ScopeVar (vx, None), ScopeVar (vy, None)
| ScopeVar (vx, Some _), ScopeVar (vy, None)
| ScopeVar (vx, None), ScopeVar (vy, Some _) ->
@ -186,7 +186,7 @@ let empty_rule
(match have_parameter with
| Some typ -> Some (Var.make ("dummy", pos), typ)
| None -> None);
rule_exception_to_rules = (RuleSet.empty, pos);
rule_exception_to_rules = RuleSet.empty, pos;
rule_id = RuleName.fresh ("empty", pos);
}
@ -200,7 +200,7 @@ let always_false_rule
(match have_parameter with
| Some typ -> Some (Var.make ("dummy", pos), typ)
| None -> None);
rule_exception_to_rules = (RuleSet.empty, pos);
rule_exception_to_rules = RuleSet.empty, pos;
rule_id = RuleName.fresh ("always_false", pos);
}
@ -296,7 +296,7 @@ let free_variables (def : rule RuleMap.t) : Pos.t ScopeDefMap.t =
def ScopeDefMap.empty
let make_var ((x, pos) : Var.t Pos.marked) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun v -> (v, pos)) (Bindlib.box_var x)
Bindlib.box_apply (fun v -> v, pos) (Bindlib.box_var x)
let make_abs
(xs : vars)
@ -305,14 +305,14 @@ let make_abs
(taus : Scopelang.Ast.typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun b -> (EAbs ((b, pos_binder), taus), pos))
(fun b -> EAbs ((b, pos_binder), taus), pos)
(Bindlib.bind_mvar xs e)
let make_app
(e : expr Pos.marked Bindlib.box)
(u : expr Pos.marked Bindlib.box list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2 (fun e u -> (EApp (e, u), pos)) e (Bindlib.box_list u)
Bindlib.box_apply2 (fun e u -> EApp (e, u), pos) e (Bindlib.box_list u)
let make_let_in
(x : Var.t)
@ -320,11 +320,11 @@ let make_let_in
(e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun e u -> (EApp (e, u), Pos.get_position (Bindlib.unbox e2)))
(make_abs (Array.of_list [ x ]) e2
(fun e u -> EApp (e, u), Pos.get_position (Bindlib.unbox e2))
(make_abs (Array.of_list [x]) e2
(Pos.get_position (Bindlib.unbox e2))
[ tau ]
[tau]
(Pos.get_position (Bindlib.unbox e2)))
(Bindlib.box_list [ e1 ])
(Bindlib.box_list [e1])
module VarMap = Map.Make (Var)

View File

@ -46,7 +46,7 @@ module Vertex = struct
let compare = compare
let equal x y =
match (x, y) with
match x, y with
| Var (x, None), Var (y, None) -> Ast.ScopeVar.compare x y = 0
| Var (x, Some sx), Var (y, Some sy) ->
Ast.ScopeVar.compare x y = 0 && Ast.StateName.compare sx sy = 0
@ -170,7 +170,7 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
let fv = Ast.free_variables def in
Ast.ScopeDefMap.fold
(fun fv_def fv_def_pos g ->
match (def_key, fv_def) with
match def_key, fv_def with
| ( Ast.ScopeDef.Var (v_defined, s_defined),
Ast.ScopeDef.Var (v_used, s_used) ) ->
(* simple case *)

View File

@ -37,7 +37,7 @@ let tag_with_log_entry
( Scopelang.Ast.EApp
( ( Scopelang.Ast.EOp (Dcalc.Ast.Unop (Dcalc.Ast.Log (l, markings))),
Pos.get_position e ),
[ e ] ),
[e] ),
Pos.get_position e )
let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
@ -81,24 +81,23 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
| EStruct (s_name, fields) ->
Bindlib.box_apply
(fun new_fields ->
(Scopelang.Ast.EStruct (s_name, new_fields), Pos.get_position e))
Scopelang.Ast.EStruct (s_name, new_fields), Pos.get_position e)
(Scopelang.Ast.StructFieldMapLift.lift_box
(Scopelang.Ast.StructFieldMap.map (translate_expr ctx) fields))
| EStructAccess (e1, s_name, f_name) ->
Bindlib.box_apply
(fun new_e1 ->
( Scopelang.Ast.EStructAccess (new_e1, s_name, f_name),
Pos.get_position e ))
Scopelang.Ast.EStructAccess (new_e1, s_name, f_name), Pos.get_position e)
(translate_expr ctx e1)
| EEnumInj (e1, cons, e_name) ->
Bindlib.box_apply
(fun new_e1 ->
(Scopelang.Ast.EEnumInj (new_e1, cons, e_name), Pos.get_position e))
Scopelang.Ast.EEnumInj (new_e1, cons, e_name), Pos.get_position e)
(translate_expr ctx e1)
| EMatch (e1, e_name, arms) ->
Bindlib.box_apply2
(fun new_e1 new_arms ->
(Scopelang.Ast.EMatch (new_e1, e_name, new_arms), Pos.get_position e))
Scopelang.Ast.EMatch (new_e1, e_name, new_arms), Pos.get_position e)
(translate_expr ctx e1)
(Scopelang.Ast.EnumConstructorMapLift.lift_box
(Scopelang.Ast.EnumConstructorMap.map (translate_expr ctx) arms))
@ -118,12 +117,12 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
in
Bindlib.box_apply
(fun new_binder ->
(Scopelang.Ast.EAbs ((new_binder, binder_pos), typs), Pos.get_position e))
Scopelang.Ast.EAbs ((new_binder, binder_pos), typs), Pos.get_position e)
(Bindlib.bind_mvar new_vars (translate_expr ctx body))
| EApp (e1, args) ->
Bindlib.box_apply2
(fun new_e1 new_args ->
(Scopelang.Ast.EApp (new_e1, new_args), Pos.get_position e))
Scopelang.Ast.EApp (new_e1, new_args), Pos.get_position e)
(translate_expr ctx e1)
(Bindlib.box_list (List.map (translate_expr ctx) args))
| EOp op -> Bindlib.box (Scopelang.Ast.EOp op, Pos.get_position e)
@ -137,15 +136,15 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
| EIfThenElse (e1, e2, e3) ->
Bindlib.box_apply3
(fun new_e1 new_e2 new_e3 ->
(Scopelang.Ast.EIfThenElse (new_e1, new_e2, new_e3), Pos.get_position e))
Scopelang.Ast.EIfThenElse (new_e1, new_e2, new_e3), Pos.get_position e)
(translate_expr ctx e1) (translate_expr ctx e2) (translate_expr ctx e3)
| EArray args ->
Bindlib.box_apply
(fun new_args -> (Scopelang.Ast.EArray new_args, Pos.get_position e))
(fun new_args -> Scopelang.Ast.EArray new_args, Pos.get_position e)
(Bindlib.box_list (List.map (translate_expr ctx) args))
| ErrorOnEmpty e1 ->
Bindlib.box_apply
(fun new_e1 -> (Scopelang.Ast.ErrorOnEmpty new_e1, Pos.get_position e))
(fun new_e1 -> Scopelang.Ast.ErrorOnEmpty new_e1, Pos.get_position e)
(translate_expr ctx e1)
(** {1 Rule tree construction} *)
@ -200,7 +199,7 @@ let rec rule_tree_to_expr
(is_func : Ast.Var.t option)
(tree : rule_tree) : Scopelang.Ast.expr Pos.marked Bindlib.box =
let exceptions, base_rules =
match tree with Leaf r -> ([], r) | Node (exceptions, r) -> (exceptions, r)
match tree with Leaf r -> [], r | Node (exceptions, r) -> exceptions, r
in
(* because each rule has its own variable parameter and we want to convert the
whole rule tree into a function, we need to perform some alpha-renaming of
@ -208,7 +207,7 @@ let rec rule_tree_to_expr
let substitute_parameter
(e : Ast.expr Pos.marked Bindlib.box)
(rule : Ast.rule) : Ast.expr Pos.marked Bindlib.box =
match (is_func, rule.Ast.rule_parameter) with
match is_func, rule.Ast.rule_parameter with
| Some new_param, Some (old_param, _) ->
let binder = Bindlib.bind_var old_param e in
Bindlib.box_apply2
@ -296,7 +295,7 @@ let rec rule_tree_to_expr
def_pos ))
exceptions default_containing_base_cases
in
match (is_func, (List.hd base_rules).Ast.rule_parameter) with
match is_func, (List.hd base_rules).Ast.rule_parameter with
| None, None -> default
| Some new_param, Some (_, typ) ->
if toplevel then
@ -305,12 +304,12 @@ let rec rule_tree_to_expr
let default =
Bindlib.box_apply
(fun (default : Scopelang.Ast.expr * Pos.t) ->
(Scopelang.Ast.ErrorOnEmpty default, def_pos))
Scopelang.Ast.ErrorOnEmpty default, def_pos)
default
in
Scopelang.Ast.make_abs
(Array.of_list [ Ast.VarMap.find new_param ctx.var_mapping ])
default def_pos [ typ ] def_pos
(Array.of_list [Ast.VarMap.find new_param ctx.var_mapping])
default def_pos [typ] def_pos
else default
| _ -> (* should not happen *) assert false
@ -400,7 +399,7 @@ let translate_def
defined as an OnlyInput to a subscope, since the [false] default value
will not be provided by the calee scope, it has to be placed in the
caller. *)
then (ELit LEmptyError, Pos.no_pos)
then ELit LEmptyError, Pos.no_pos
else
Bindlib.unbox
(rule_tree_to_expr ~toplevel:true ctx
@ -412,8 +411,8 @@ let translate_def
(match top_list with
| [] ->
(* In this case, there are no rules to define the expression *)
Leaf [ top_value ]
| _ -> Node (top_list, [ top_value ])))
Leaf [top_value]
| _ -> Node (top_list, [top_value])))
(** Translates a scope *)
let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
@ -462,7 +461,7 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
in
let scope_var =
match
(Ast.ScopeVarMap.find var ctx.scope_var_mapping, state)
Ast.ScopeVarMap.find var ctx.scope_var_mapping, state
with
| WholeVar v, None -> v
| States states, Some state -> List.assoc state states
@ -571,12 +570,12 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
Ast.ScopeVarMap.find sub_scope_var
ctx.scope_var_mapping
with
| WholeVar v -> (v, var_pos)
| WholeVar v -> v, var_pos
| States states ->
(* When defining a sub-scope variable, we
always define its first state in the
sub-scope. *)
(snd (List.hd states), var_pos) ),
snd (List.hd states), var_pos ),
var_pos ),
def_typ,
scope_def.Ast.scope_def_io,
@ -587,7 +586,7 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
List.map snd (Ast.ScopeDefMap.bindings sub_scope_vars_redefs)
in
sub_scope_vars_redefs
@ [ Scopelang.Ast.Call (sub_scope, sub_scope_index) ])
@ [Scopelang.Ast.Call (sub_scope, sub_scope_index)])
scope_ordering)
in
(* Then, after having computed all the scopes variables, we add the

View File

@ -20,12 +20,11 @@ module Errors = Utils.Errors
module Pos = Utils.Pos
(** Associates a {!type: Cli.backend_lang} with its string represtation. *)
let languages = [ ("en", Cli.En); ("fr", Cli.Fr); ("pl", Cli.Pl) ]
let languages = ["en", Cli.En; "fr", Cli.Fr; "pl", Cli.Pl]
(** Associates a file extension with its corresponding {!type: Cli.backend_lang}
string representation. *)
let extensions =
[ (".catala_fr", "fr"); (".catala_en", "en"); (".catala_pl", "pl") ]
let extensions = [".catala_fr", "fr"; ".catala_en", "en"; ".catala_pl", "pl"]
(** Entry function for the executable. Returns a negative number in case of
error. Usage: [driver source_file options]*)
@ -74,7 +73,7 @@ let driver source_file (options : Cli.options) : int =
let prgm = Surface.Fill_positions.fill_pos_with_legislative_info prgm in
match backend with
| Cli.Makefile ->
let backend_extensions_list = [ ".tex" ] in
let backend_extensions_list = [".tex"] in
let source_file =
match source_file with
| FileName f -> f
@ -150,7 +149,7 @@ let driver source_file (options : Cli.options) : int =
Cli.debug_print "Name resolution...";
let ctxt = Surface.Name_resolution.form_context prgm in
let scope_uid =
match (options.ex_scope, backend) with
match options.ex_scope, backend with
| None, Cli.Interpret ->
Errors.raise_error "No scope was provided for execution."
| None, _ ->
@ -174,8 +173,8 @@ let driver source_file (options : Cli.options) : int =
match options.output_file with
| Some f ->
let oc = open_out f in
(Format.formatter_of_out_channel oc, fun _ -> close_out oc)
| None -> (Format.std_formatter, fun _ -> ())
Format.formatter_of_out_channel oc, fun _ -> close_out oc
| None -> Format.std_formatter, fun _ -> ()
in
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
@ -208,8 +207,8 @@ let driver source_file (options : Cli.options) : int =
match options.output_file with
| Some f ->
let oc = open_out f in
(Format.formatter_of_out_channel oc, fun _ -> close_out oc)
| None -> (Format.std_formatter, fun _ -> ())
Format.formatter_of_out_channel oc, fun _ -> close_out oc
| None -> Format.std_formatter, fun _ -> ()
in
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
@ -262,7 +261,7 @@ let driver source_file (options : Cli.options) : int =
let v1 =
Re.Pcre.substitute ~rex:out_regex ~subst:(fun _ -> "") v1
in
((v1, v1_pos), e1))
(v1, v1_pos), e1)
results
in
let results =
@ -307,8 +306,8 @@ let driver source_file (options : Cli.options) : int =
match options.output_file with
| Some f ->
let oc = open_out f in
(Format.formatter_of_out_channel oc, fun _ -> close_out oc)
| None -> (Format.std_formatter, fun _ -> ())
Format.formatter_of_out_channel oc, fun _ -> close_out oc
| None -> Format.std_formatter, fun _ -> ()
in
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
@ -365,8 +364,8 @@ let driver source_file (options : Cli.options) : int =
match options.output_file with
| Some f ->
let oc = open_out f in
(Format.formatter_of_out_channel oc, fun _ -> close_out oc)
| None -> (Format.std_formatter, fun _ -> ())
Format.formatter_of_out_channel oc, fun _ -> close_out oc
| None -> Format.std_formatter, fun _ -> ()
in
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"

View File

@ -53,15 +53,13 @@ type expr =
type program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : expr Dcalc.Ast.scopes }
let evar (v : expr Bindlib.var) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun v' -> (v', pos)) (Bindlib.box_var v)
Bindlib.box_apply (fun v' -> v', pos) (Bindlib.box_var v)
let etuple
(args : expr Pos.marked Bindlib.box list)
(s : Dcalc.Ast.StructName.t option)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun args -> (ETuple (args, s), pos))
(Bindlib.box_list args)
Bindlib.box_apply (fun args -> ETuple (args, s), pos) (Bindlib.box_list args)
let etupleaccess
(e1 : expr Pos.marked Bindlib.box)
@ -69,7 +67,7 @@ let etupleaccess
(s : Dcalc.Ast.StructName.t option)
(typs : Dcalc.Ast.typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (ETupleAccess (e1, i, s, typs), pos)) e1
Bindlib.box_apply (fun e1 -> ETupleAccess (e1, i, s, typs), pos) e1
let einj
(e1 : expr Pos.marked Bindlib.box)
@ -77,7 +75,7 @@ let einj
(e_name : Dcalc.Ast.EnumName.t)
(typs : Dcalc.Ast.typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (EInj (e1, i, e_name, typs), pos)) e1
Bindlib.box_apply (fun e1 -> EInj (e1, i, e_name, typs), pos) e1
let ematch
(arg : expr Pos.marked Bindlib.box)
@ -85,12 +83,12 @@ let ematch
(e_name : Dcalc.Ast.EnumName.t)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun arg arms -> (EMatch (arg, arms, e_name), pos))
(fun arg arms -> EMatch (arg, arms, e_name), pos)
arg (Bindlib.box_list arms)
let earray (args : expr Pos.marked Bindlib.box list) (pos : Pos.t) :
expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun args -> (EArray args, pos)) (Bindlib.box_list args)
Bindlib.box_apply (fun args -> EArray args, pos) (Bindlib.box_list args)
let elit (l : lit) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (ELit l, pos)
@ -101,7 +99,7 @@ let eabs
(typs : Dcalc.Ast.typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun binder -> (EAbs ((binder, pos_binder), typs), pos))
(fun binder -> EAbs ((binder, pos_binder), typs), pos)
binder
let eapp
@ -109,12 +107,12 @@ let eapp
(args : expr Pos.marked Bindlib.box list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun e1 args -> (EApp (e1, args), pos))
(fun e1 args -> EApp (e1, args), pos)
e1 (Bindlib.box_list args)
let eassert (e1 : expr Pos.marked Bindlib.box) (pos : Pos.t) :
expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (EAssert e1, pos)) e1
Bindlib.box_apply (fun e1 -> EAssert e1, pos) e1
let eop (op : Dcalc.Ast.operator) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (EOp op, pos)
@ -127,14 +125,14 @@ let ecatch
(exn : except)
(e2 : expr Pos.marked Bindlib.box)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2 (fun e1 e2 -> (ECatch (e1, exn, e2), pos)) e1 e2
Bindlib.box_apply2 (fun e1 e2 -> ECatch (e1, exn, e2), pos) e1 e2
let eifthenelse
(e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box)
(e3 : expr Pos.marked Bindlib.box)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply3 (fun e1 e2 e3 -> (EIfThenElse (e1, e2, e3), pos)) e1 e2 e3
Bindlib.box_apply3 (fun e1 e2 e3 -> EIfThenElse (e1, e2, e3), pos) e1 e2 e3
module Var = struct
type t = expr Bindlib.var
@ -187,7 +185,7 @@ let box_expr (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
id_t () e
let make_var ((x, pos) : Var.t Pos.marked) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun x -> (x, pos)) (Bindlib.box_var x)
Bindlib.box_apply (fun x -> x, pos) (Bindlib.box_var x)
let make_abs
(xs : vars)
@ -196,14 +194,14 @@ let make_abs
(taus : D.typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun b -> (EAbs ((b, pos_binder), taus), pos))
(fun b -> EAbs ((b, pos_binder), taus), pos)
(Bindlib.bind_mvar xs e)
let make_app
(e : expr Pos.marked Bindlib.box)
(u : expr Pos.marked Bindlib.box list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2 (fun e u -> (EApp (e, u), pos)) e (Bindlib.box_list u)
Bindlib.box_apply2 (fun e u -> EApp (e, u), pos) e (Bindlib.box_list u)
let make_let_in
(x : Var.t)
@ -211,7 +209,7 @@ let make_let_in
(e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
make_app (make_abs (Array.of_list [ x ]) e2 pos [ tau ] pos) [ e1 ] pos
make_app (make_abs (Array.of_list [x]) e2 pos [tau] pos) [e1] pos
let make_multiple_let_in
(xs : Var.t array)
@ -232,19 +230,13 @@ let some_constr : D.EnumConstructor.t =
D.EnumConstructor.fresh ("ESome", Pos.no_pos)
let option_enum_config : (D.EnumConstructor.t * D.typ Pos.marked) list =
[
(none_constr, (D.TLit D.TUnit, Pos.no_pos));
(some_constr, (D.TAny, Pos.no_pos));
]
[none_constr, (D.TLit D.TUnit, Pos.no_pos); some_constr, (D.TAny, Pos.no_pos)]
let make_none (pos : Pos.t) : expr Pos.marked Bindlib.box =
let mark : 'a -> 'a Pos.marked = Pos.mark pos in
Bindlib.box @@ mark
@@ EInj
( mark @@ ELit LUnit,
0,
option_enum,
[ (D.TLit D.TUnit, pos); (D.TAny, pos) ] )
(mark @@ ELit LUnit, 0, option_enum, [D.TLit D.TUnit, pos; D.TAny, pos])
let make_some (e : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position @@ Bindlib.unbox e in
@ -284,8 +276,8 @@ let make_matchopt
let x = Var.make ("_", pos) in
make_matchopt_with_abs_arms arg
(make_abs (Array.of_list [ x ]) e_none pos [ (D.TLit D.TUnit, pos) ] pos)
(make_abs (Array.of_list [ v ]) e_some pos [ tau ] pos)
(make_abs (Array.of_list [x]) e_none pos [D.TLit D.TUnit, pos] pos)
(make_abs (Array.of_list [v]) e_some pos [tau] pos)
let handle_default = Var.make ("handle_default", Pos.no_pos)
let handle_default_opt = Var.make ("handle_default_opt", Pos.no_pos)

View File

@ -32,7 +32,7 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
match Pos.unmark e with
| EVar v ->
( Bindlib.box_apply
(fun new_v -> (new_v, Pos.get_position v))
(fun new_v -> new_v, Pos.get_position v)
(Bindlib.box_var (Pos.unmark v)),
VarSet.diff (VarSet.singleton (Pos.unmark v)) ctx.globally_bound_vars )
| ETuple (args, s) ->
@ -40,23 +40,23 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
List.fold_left
(fun (new_args, free_vars) arg ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
(new_arg :: new_args, VarSet.union new_free_vars free_vars))
new_arg :: new_args, VarSet.union new_free_vars free_vars)
([], VarSet.empty) args
in
( Bindlib.box_apply
(fun new_args -> (ETuple (List.rev new_args, s), Pos.get_position e))
(fun new_args -> ETuple (List.rev new_args, s), Pos.get_position e)
(Bindlib.box_list new_args),
free_vars )
| ETupleAccess (e1, n, s, typs) ->
let new_e1, free_vars = closure_conversion_expr ctx e1 in
( Bindlib.box_apply
(fun new_e1 -> (ETupleAccess (new_e1, n, s, typs), Pos.get_position e))
(fun new_e1 -> ETupleAccess (new_e1, n, s, typs), Pos.get_position e)
new_e1,
free_vars )
| EInj (e1, n, e_name, typs) ->
let new_e1, free_vars = closure_conversion_expr ctx e1 in
( Bindlib.box_apply
(fun new_e1 -> (EInj (new_e1, n, e_name, typs), Pos.get_position e))
(fun new_e1 -> EInj (new_e1, n, e_name, typs), Pos.get_position e)
new_e1,
free_vars )
| EMatch (e1, arms, e_name) ->
@ -73,7 +73,7 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
let new_binder = Bindlib.bind_mvar vars new_body in
( Bindlib.box_apply
(fun new_binder ->
(EAbs ((new_binder, binder_pos), typs), Pos.get_position arm))
EAbs ((new_binder, binder_pos), typs), Pos.get_position arm)
new_binder
:: new_arms,
VarSet.union free_vars new_free_vars )
@ -82,7 +82,7 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
in
( Bindlib.box_apply2
(fun new_e1 new_arms ->
(EMatch (new_e1, new_arms, e_name), Pos.get_position e))
EMatch (new_e1, new_arms, e_name), Pos.get_position e)
new_e1
(Bindlib.box_list new_arms),
free_vars )
@ -91,14 +91,14 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
List.fold_right
(fun arg (new_args, free_vars) ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
(new_arg :: new_args, VarSet.union free_vars new_free_vars))
new_arg :: new_args, VarSet.union free_vars new_free_vars)
args ([], VarSet.empty)
in
( Bindlib.box_apply
(fun new_args -> (EArray new_args, Pos.get_position e))
(fun new_args -> EArray new_args, Pos.get_position e)
(Bindlib.box_list new_args),
free_vars )
| ELit l -> (Bindlib.box (ELit l, Pos.get_position e), VarSet.empty)
| ELit l -> Bindlib.box (ELit l, Pos.get_position e), VarSet.empty
| EApp ((EAbs ((binder, binder_pos), typs_abs), e1_pos), args) ->
(* let-binding, we should not close these *)
let vars, body = Bindlib.unmbind binder in
@ -108,7 +108,7 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
List.fold_right
(fun arg (new_args, free_vars) ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
(new_arg :: new_args, VarSet.union free_vars new_free_vars))
new_arg :: new_args, VarSet.union free_vars new_free_vars)
args ([], free_vars)
in
( Bindlib.box_apply2
@ -137,7 +137,7 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
make_multiple_let_in
(Array.of_list extra_vars_list)
(List.init (List.length extra_vars_list) (fun _ ->
(Dcalc.Ast.TAny, binder_pos)))
Dcalc.Ast.TAny, binder_pos))
(List.mapi
(fun i _ ->
Bindlib.box_apply
@ -148,7 +148,7 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
None,
List.init
(List.length extra_vars_list + 1)
(fun _ -> (Dcalc.Ast.TAny, binder_pos)) ),
(fun _ -> Dcalc.Ast.TAny, binder_pos) ),
binder_pos ))
(Bindlib.box_var inner_c_var))
extra_vars_list)
@ -156,7 +156,7 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
in
let new_closure =
make_abs
(Array.concat [ Array.make 1 inner_c_var; vars ])
(Array.concat [Array.make 1 inner_c_var; vars])
new_closure_body binder_pos
((Dcalc.Ast.TAny, binder_pos) :: typs)
(Pos.get_position e)
@ -169,7 +169,7 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
( ETuple
( (code_var, binder_pos)
:: List.map
(fun extra_var -> (extra_var, binder_pos))
(fun extra_var -> extra_var, binder_pos)
extra_vars,
None ),
Pos.get_position e ))
@ -186,11 +186,11 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
List.fold_right
(fun arg (new_args, free_vars) ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
(new_arg :: new_args, VarSet.union free_vars new_free_vars))
new_arg :: new_args, VarSet.union free_vars new_free_vars)
args ([], VarSet.empty)
in
( Bindlib.box_apply
(fun new_e2 -> (EApp ((EOp op, pos_op), new_e2), Pos.get_position e))
(fun new_e2 -> EApp ((EOp op, pos_op), new_e2), Pos.get_position e)
(Bindlib.box_list new_args),
free_vars )
| EApp ((EVar (v, _), v_pos), args) when VarSet.mem v ctx.globally_bound_vars
@ -200,12 +200,11 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
List.fold_right
(fun arg (new_args, free_vars) ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
(new_arg :: new_args, VarSet.union free_vars new_free_vars))
new_arg :: new_args, VarSet.union free_vars new_free_vars)
args ([], VarSet.empty)
in
( Bindlib.box_apply2
(fun new_v new_e2 ->
(EApp ((new_v, v_pos), new_e2), Pos.get_position e))
(fun new_v new_e2 -> EApp ((new_v, v_pos), new_e2), Pos.get_position e)
(Bindlib.box_var v)
(Bindlib.box_list new_args),
free_vars )
@ -217,7 +216,7 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
List.fold_right
(fun arg (new_args, free_vars) ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
(new_arg :: new_args, VarSet.union free_vars new_free_vars))
new_arg :: new_args, VarSet.union free_vars new_free_vars)
args ([], free_vars)
in
let call_expr =
@ -245,28 +244,26 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
free_vars )
| EAssert e1 ->
let new_e1, free_vars = closure_conversion_expr ctx e1 in
( Bindlib.box_apply
(fun new_e1 -> (EAssert new_e1, Pos.get_position e))
new_e1,
( Bindlib.box_apply (fun new_e1 -> EAssert new_e1, Pos.get_position e) new_e1,
free_vars )
| EOp op -> (Bindlib.box (EOp op, Pos.get_position e), VarSet.empty)
| EOp op -> Bindlib.box (EOp op, Pos.get_position e), VarSet.empty
| EIfThenElse (e1, e2, e3) ->
let new_e1, free_vars1 = closure_conversion_expr ctx e1 in
let new_e2, free_vars2 = closure_conversion_expr ctx e2 in
let new_e3, free_vars3 = closure_conversion_expr ctx e3 in
( Bindlib.box_apply3
(fun new_e1 new_e2 new_e3 ->
(EIfThenElse (new_e1, new_e2, new_e3), Pos.get_position e))
EIfThenElse (new_e1, new_e2, new_e3), Pos.get_position e)
new_e1 new_e2 new_e3,
VarSet.union (VarSet.union free_vars1 free_vars2) free_vars3 )
| ERaise except ->
(Bindlib.box (ERaise except, Pos.get_position e), VarSet.empty)
Bindlib.box (ERaise except, Pos.get_position e), VarSet.empty
| ECatch (e1, except, e2) ->
let new_e1, free_vars1 = closure_conversion_expr ctx e1 in
let new_e2, free_vars2 = closure_conversion_expr ctx e2 in
( Bindlib.box_apply2
(fun new_e1 new_e2 ->
(ECatch (new_e1, except, new_e2), Pos.get_position e))
ECatch (new_e1, except, new_e2), Pos.get_position e)
new_e1 new_e2,
VarSet.union free_vars1 free_vars2 )
@ -315,7 +312,7 @@ let closure_conversion (p : program) : program Bindlib.box =
new_scope_body_expr
(Bindlib.bind_var scope_var next))),
global_vars ))
~init:(Fun.id, VarSet.of_list [ handle_default; handle_default_opt ])
~init:(Fun.id, VarSet.of_list [handle_default; handle_default_opt])
p.scopes
in
Bindlib.box_apply

View File

@ -36,7 +36,7 @@ let translate_lit (l : D.lit) : A.expr =
let thunk_expr (e : A.expr Pos.marked Bindlib.box) (pos : Pos.t) :
A.expr Pos.marked Bindlib.box =
let dummy_var = A.Var.make ("_", pos) in
A.make_abs [| dummy_var |] e pos [ (D.TAny, pos) ] pos
A.make_abs [| dummy_var |] e pos [D.TAny, pos] pos
let rec translate_default
(ctx : ctx)
@ -97,7 +97,7 @@ and translate_expr (ctx : ctx) (e : D.expr Pos.marked) :
Array.fold_right
(fun var (ctx, lc_vars) ->
let lc_var = A.Var.make (Bindlib.name_of var, pos_binder) in
(D.VarMap.add var lc_var ctx, lc_var :: lc_vars))
D.VarMap.add var lc_var ctx, lc_var :: lc_vars)
vars (ctx, [])
in
let lc_vars = Array.of_list lc_vars in
@ -107,7 +107,7 @@ and translate_expr (ctx : ctx) (e : D.expr Pos.marked) :
(fun new_binder ->
Pos.same_pos_as (A.EAbs ((new_binder, pos_binder), ts)) e)
new_binder
| D.EDefault ([ exn ], just, cons) when !Cli.optimize_flag ->
| D.EDefault ([exn], just, cons) when !Cli.optimize_flag ->
A.ecatch (translate_expr ctx exn) A.EmptyError
(A.eifthenelse (translate_expr ctx just) (translate_expr ctx cons)
(Bindlib.box (Pos.same_pos_as (A.ERaise A.EmptyError) e))

View File

@ -123,7 +123,7 @@ let rec translate_typ (tau : D.typ Pos.marked) : D.typ Pos.marked =
| D.TArray ts -> D.TArray (translate_typ ts)
(* catala is not polymorphic *)
| D.TArrow ((D.TLit D.TUnit, pos_unit), t2) ->
D.TEnum ([ (D.TLit D.TUnit, pos_unit); translate_typ t2 ], A.option_enum)
D.TEnum ([D.TLit D.TUnit, pos_unit; translate_typ t2], A.option_enum)
(* D.TAny *)
| D.TArrow (t1, t2) -> D.TArrow (translate_typ t1, translate_typ t2)
end
@ -178,24 +178,24 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
(* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a,
created a variable %a to replace it" Dcalc.Print.format_var v
Print.format_var v'; *)
(A.make_var (v', pos), A.VarMap.singleton v' e)
else ((find ~info:"should never happend" v ctx).expr, A.VarMap.empty)
| D.EApp ((D.EVar (v, pos_v), p), [ (D.ELit D.LUnit, _) ]) ->
A.make_var (v', pos), A.VarMap.singleton v' e
else (find ~info:"should never happend" v ctx).expr, A.VarMap.empty
| D.EApp ((D.EVar (v, pos_v), p), [(D.ELit D.LUnit, _)]) ->
if not (find ~info:"search for a variable" v ctx).is_pure then
let v' = A.Var.make (Bindlib.name_of v, pos_v) in
(* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a,
created a variable %a to replace it" Dcalc.Print.format_var v
Print.format_var v'; *)
(A.make_var (v', pos), A.VarMap.singleton v' (D.EVar (v, pos_v), p))
A.make_var (v', pos), A.VarMap.singleton v' (D.EVar (v, pos_v), p)
else
Errors.raise_spanned_error pos
"Internal error: an pure variable was found in an unpure environment."
| D.EDefault (_exceptions, _just, _cons) ->
let v' = A.Var.make ("default_term", pos) in
(A.make_var (v', pos), A.VarMap.singleton v' e)
A.make_var (v', pos), A.VarMap.singleton v' e
| D.ELit D.LEmptyError ->
let v' = A.Var.make ("empty_litteral", pos) in
(A.make_var (v', pos), A.VarMap.singleton v' e)
A.make_var (v', pos), A.VarMap.singleton v' e
(* This one is a very special case. It transform an unpure expression
environement to a pure expression. *)
| ErrorOnEmpty arg ->
@ -209,12 +209,12 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
(A.make_abs [| silent_var |]
(Bindlib.box (A.ERaise A.NoValueProvided, pos))
pos
[ (D.TAny, pos) ]
[D.TAny, pos]
pos)
(A.make_abs [| x |] (A.make_var (x, pos)) pos [ (D.TAny, pos) ] pos),
(A.make_abs [| x |] (A.make_var (x, pos)) pos [D.TAny, pos] pos),
A.VarMap.empty )
(* pure terms *)
| D.ELit l -> (A.elit (translate_lit l pos) pos, A.VarMap.empty)
| D.ELit l -> A.elit (translate_lit l pos) pos, A.VarMap.empty
| D.EIfThenElse (e1, e2, e3) ->
let e1', h1 = translate_and_hoist ctx e1 in
let e2', h2 = translate_and_hoist ctx e2 in
@ -224,12 +224,12 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
(*(* equivalent code : *) let e' = let+ e1' = e1' and+ e2' = e2' and+ e3' =
e3' in (A.EIfThenElse (e1', e2', e3'), pos) in *)
(e', disjoint_union_maps pos [ h1; h2; h3 ])
e', disjoint_union_maps pos [h1; h2; h3]
| D.EAssert e1 ->
(* same behavior as in the ICFP paper: if e1 is empty, then no error is
raised. *)
let e1', h1 = translate_and_hoist ctx e1 in
(A.eassert e1' pos, h1)
A.eassert e1' pos, h1
| D.EAbs ((binder, pos_binder), ts) ->
let vars, body = Bindlib.unmbind binder in
let ctx, lc_vars =
@ -242,7 +242,7 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
(unimplemented for now) *)
let ctx = add_var pos var true ctx in
let lc_var = (find var ctx).var in
(ctx, lc_var :: lc_vars))
ctx, lc_var :: lc_vars)
in
let lc_vars = Array.of_list lc_vars in
@ -253,7 +253,7 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
( Bindlib.box_apply
(fun new_binder ->
(A.EAbs ((new_binder, pos_binder), List.map translate_typ ts), pos))
A.EAbs ((new_binder, pos_binder), List.map translate_typ ts), pos)
new_binder,
hoists )
| EApp (e1, args) ->
@ -264,22 +264,22 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
let hoists = disjoint_union_maps pos (h1 :: h_args) in
let e' = A.eapp e1' args' pos in
(e', hoists)
e', hoists
| ETuple (args, s) ->
let args', h_args =
args |> List.map (translate_and_hoist ctx) |> List.split
in
let hoists = disjoint_union_maps pos h_args in
(A.etuple args' s pos, hoists)
A.etuple args' s pos, hoists
| ETupleAccess (e1, i, s, ts) ->
let e1', hoists = translate_and_hoist ctx e1 in
let e1' = A.etupleaccess e1' i s ts pos in
(e1', hoists)
e1', hoists
| EInj (e1, i, en, ts) ->
let e1', hoists = translate_and_hoist ctx e1 in
let e1' = A.einj e1' i en ts pos in
(e1', hoists)
e1', hoists
| EMatch (e1, cases, en) ->
let e1', h1 = translate_and_hoist ctx e1 in
let cases', h_cases =
@ -288,12 +288,12 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
let hoists = disjoint_union_maps pos (h1 :: h_cases) in
let e' = A.ematch e1' cases' en pos in
(e', hoists)
e', hoists
| EArray es ->
let es', hoists = es |> List.map (translate_and_hoist ctx) |> List.split in
(A.earray es' pos, disjoint_union_maps pos hoists)
| EOp op -> (Bindlib.box (A.EOp op, pos), A.VarMap.empty)
A.earray es' pos, disjoint_union_maps pos hoists
| EOp op -> Bindlib.box (A.EOp op, pos), A.VarMap.empty
and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Pos.marked) :
A.expr Pos.marked Bindlib.box =
@ -325,7 +325,7 @@ and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Pos.marked) :
(A.make_var (A.handle_default_opt, pos_hoist))
[
Bindlib.box_apply
(fun excep' -> (A.EArray excep', pos_hoist))
(fun excep' -> A.EArray excep', pos_hoist)
(Bindlib.box_list excep');
just';
cons';
@ -344,14 +344,14 @@ and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Pos.marked) :
(A.make_abs [| silent_var |]
(Bindlib.box (A.ERaise A.NoValueProvided, pos_hoist))
pos_hoist
[ (D.TAny, pos_hoist) ]
[D.TAny, pos_hoist]
pos_hoist)
(A.make_abs [| x |]
(Bindlib.box_apply
(fun arg -> (A.EAssert arg, pos_hoist))
(fun arg -> A.EAssert arg, pos_hoist)
(A.make_var (x, pos_hoist)))
pos_hoist
[ (D.TAny, pos_hoist) ]
[D.TAny, pos_hoist]
pos_hoist)
| _ ->
Errors.raise_spanned_error pos_hoist
@ -557,7 +557,7 @@ let translate_program (prgm : D.program) : A.program =
@@ Format.asprintf "Output type: %a"
(Dcalc.Print.format_typ decl_ctx) (translate_typ
tau); *)
(n, translate_typ tau))
n, translate_typ tau)
else l);
}
in

View File

@ -74,7 +74,7 @@ let rec iota_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box
when Dcalc.Ast.EnumName.compare n n' = 0 ->
let+ e1 = visitor_map iota_expr () e1
and+ case = visitor_map iota_expr () (List.nth cases i) in
default_mark @@ EApp (case, [ e1 ])
default_mark @@ EApp (case, [e1])
| EMatch (e', cases, n)
when cases
|> List.mapi (fun i (case, _pos) ->
@ -123,15 +123,15 @@ let rec peephole_expr (_ : unit) (e : expr Pos.marked) :
and+ e3 = peephole_expr () e3 in
match Pos.unmark e1 with
| ELit (LBool true)
| EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ]) ->
| EApp ((EOp (Unop (Log _)), _), [(ELit (LBool true), _)]) ->
e2
| ELit (LBool false)
| EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ]) ->
| EApp ((EOp (Unop (Log _)), _), [(ELit (LBool false), _)]) ->
e3
| _ -> default_mark @@ EIfThenElse (e1, e2, e3))
| ECatch (e1, except, e2) -> (
let+ e1 = peephole_expr () e1 and+ e2 = peephole_expr () e2 in
match (Pos.unmark e1, Pos.unmark e2) with
match Pos.unmark e1, Pos.unmark e2 with
| ERaise except', ERaise except'' when except' = except && except = except''
->
default_mark @@ ERaise except

View File

@ -63,10 +63,10 @@ let format_exception (fmt : Format.formatter) (exn : except) : unit =
| NoValueProvided -> "NoValueProvided")
let format_keyword (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ ANSITerminal.red ]) s
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ANSITerminal.red]) s
let format_punctuation (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ ANSITerminal.cyan ]) s
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ANSITerminal.cyan]) s
let needs_parens (e : expr Pos.marked) : bool =
match Pos.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false
@ -139,10 +139,8 @@ let rec format_expr
| ELit l -> Format.fprintf fmt "%a" format_lit (Pos.same_pos_as l e)
| EApp ((EAbs ((binder, _), taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
let xs_tau_arg =
List.map2 (fun (x, tau) arg -> (x, tau, arg)) xs_tau args
in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in
Format.fprintf fmt "%a%a"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "")
@ -154,7 +152,7 @@ let rec format_expr
xs_tau_arg format_expr body
| EAbs ((binder, _), taus) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
Format.fprintf fmt "@[<hov 2>%a %a %a@ %a@]" format_punctuation "λ"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
@ -165,16 +163,16 @@ let rec format_expr
tau format_punctuation ")"))
xs_tau format_punctuation "" format_expr body
| EApp
( (EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _),
[ arg1; arg2 ] ) ->
((EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _), [arg1; arg2])
->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" Dcalc.Print.format_binop
(op, Pos.no_pos) format_with_parens arg1 format_with_parens arg2
| EApp ((EOp (Binop op), _), [ arg1; arg2 ]) ->
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1
Dcalc.Print.format_binop (op, Pos.no_pos) format_with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [ arg1 ]) when not debug ->
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug ->
Format.fprintf fmt "%a" format_with_parens arg1
| EApp ((EOp (Unop op), _), [ arg1 ]) ->
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" Dcalc.Print.format_unop
(op, Pos.no_pos) format_with_parens arg1
| EApp (f, args) ->

View File

@ -207,7 +207,7 @@ let rec format_typ (fmt : Format.formatter) (typ : Dcalc.Ast.typ Pos.marked) :
format_typ_with_parens)
ts
| TTuple (_, Some s) -> Format.fprintf fmt "%a" format_struct_name s
| TEnum ([ t ], e) when D.EnumName.compare e Ast.option_enum = 0 ->
| TEnum ([t], e) when D.EnumName.compare e Ast.option_enum = 0 ->
Format.fprintf fmt "@[<hov 2>(%a)@] %a" format_typ_with_parens t
format_enum_name e
| TEnum (_, e) when D.EnumName.compare e Ast.option_enum = 0 ->
@ -230,7 +230,7 @@ let format_var (fmt : Format.formatter) (v : Var.t) : unit =
in
let lowercase_name = avoid_keywords (to_ascii lowercase_name) in
if
List.mem lowercase_name [ "handle_default"; "handle_default_opt" ]
List.mem lowercase_name ["handle_default"; "handle_default_opt"]
|| Dcalc.Print.begins_with_uppercase (Bindlib.name_of v)
then Format.fprintf fmt "%s" lowercase_name
else if lowercase_name = "_" then Format.fprintf fmt "%s" lowercase_name
@ -329,10 +329,8 @@ let rec format_expr
| ELit l -> Format.fprintf fmt "%a" format_lit (Pos.same_pos_as l e)
| EApp ((EAbs ((binder, _), taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
let xs_tau_arg =
List.map2 (fun (x, tau) arg -> (x, tau, arg)) xs_tau args
in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in
Format.fprintf fmt "(%a%a)"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "")
@ -342,7 +340,7 @@ let rec format_expr
xs_tau_arg format_with_parens body
| EAbs ((binder, _), taus) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
Format.fprintf fmt "@[<hov 2>fun@ %a ->@ %a@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
@ -350,23 +348,22 @@ let rec format_expr
Format.fprintf fmt "@[<hov 2>(%a:@ %a)@]" format_var x format_typ tau))
xs_tau format_expr body
| EApp
( (EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _),
[ arg1; arg2 ] ) ->
((EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _), [arg1; arg2])
->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_binop (op, Pos.no_pos)
format_with_parens arg1 format_with_parens arg2
| EApp ((EOp (Binop op), _), [ arg1; arg2 ]) ->
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1
format_binop (op, Pos.no_pos) format_with_parens arg2
| EApp
((EApp ((EOp (Unop (D.Log (D.BeginCall, info))), _), [ f ]), _), [ arg ])
| EApp ((EApp ((EOp (Unop (D.Log (D.BeginCall, info))), _), [f]), _), [arg])
when !Cli.trace_flag ->
Format.fprintf fmt "(log_begin_call@ %a@ %a@ %a)" format_uid_list info
format_with_parens f format_with_parens arg
| EApp ((EOp (Unop (D.Log (D.VarDef tau, info))), _), [ arg1 ])
| EApp ((EOp (Unop (D.Log (D.VarDef tau, info))), _), [arg1])
when !Cli.trace_flag ->
Format.fprintf fmt "(log_variable_definition@ %a@ (%a)@ %a)" format_uid_list
info typ_embedding_name (tau, Pos.no_pos) format_with_parens arg1
| EApp ((EOp (Unop (D.Log (D.PosRecordIfTrueBool, _))), pos), [ arg1 ])
| EApp ((EOp (Unop (D.Log (D.PosRecordIfTrueBool, _))), pos), [arg1])
when !Cli.trace_flag ->
Format.fprintf fmt
"(log_decision_taken@ @[<hov 2>{filename = \"%s\";@ start_line=%d;@ \
@ -374,13 +371,13 @@ let rec format_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
| EApp ((EOp (Unop (D.Log (D.EndCall, info))), _), [ arg1 ])
| EApp ((EOp (Unop (D.Log (D.EndCall, info))), _), [arg1])
when !Cli.trace_flag ->
Format.fprintf fmt "(log_end_call@ %a@ %a)" format_uid_list info
format_with_parens arg1
| EApp ((EOp (Unop (D.Log _)), _), [ arg1 ]) ->
| EApp ((EOp (Unop (D.Log _)), _), [arg1]) ->
Format.fprintf fmt "%a" format_with_parens arg1
| EApp ((EOp (Unop op), _), [ arg1 ]) ->
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_unop (op, Pos.no_pos)
format_with_parens arg1
| EApp (f, args) ->

View File

@ -180,7 +180,7 @@ let rec law_structure_to_html
let h_number = heading.law_heading_precedence + 1 in
Format.fprintf fmt "<h%d class='law-heading'><a href='%s'>%s</a></h%d>\n"
h_number
(match (heading.law_heading_id, language) with
(match heading.law_heading_id, language with
| Some id, Fr ->
let ltime = Unix.localtime (Unix.time ()) in
P.sprintf "https://legifrance.gouv.fr/codes/id/%s/%d-%02d-%02d" id

View File

@ -32,12 +32,12 @@ let pre_latexify (s : string) : string =
R.substitute ~rex:(R.regexp old_s) ~subst:(fun _ -> new_s) s
in
[
("\\$", "\\$");
("%", "\\%");
("\\_", "\\_");
("\\#", "\\#");
("1er", "1\\textsuperscript{er}");
("\\^", "\\textasciicircum");
"\\$", "\\$";
"%", "\\%";
"\\_", "\\_";
"\\#", "\\#";
"1er", "1\\textsuperscript{er}";
"\\^", "\\textasciicircum";
]
|> List.fold_left substitute s

View File

@ -178,9 +178,7 @@ let duration_of_numbers (year : int) (month : int) (day : int) : duration =
let duration_to_string (d : duration) : string =
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") ]
List.filter (fun (a, _) -> a <> 0) [x, "years"; y, "months"; z, "days"]
in
match to_print with
| [] -> "empty duration"
@ -201,7 +199,7 @@ let handle_default :
Array.fold_left
(fun acc except ->
let new_val = try Some (except ()) with EmptyError -> None in
match (acc, new_val) with
match acc, new_val with
| None, _ -> new_val
| Some _, None -> acc
| Some _, Some _ -> raise ConflictError)
@ -218,7 +216,7 @@ let handle_default_opt
let except =
Array.fold_left
(fun acc except ->
match (acc, except) with
match acc, except with
| ENone _, _ -> except
| ESome _, ENone _ -> acc
| ESome _, ESome _ -> raise ConflictError)

View File

@ -37,18 +37,18 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Pos.marked) :
try A.EVar (L.VarMap.find (Pos.unmark v) ctxt.var_dict)
with Not_found -> A.EFunc (L.VarMap.find (Pos.unmark v) ctxt.func_dict)
in
([], (local_var, Pos.get_position v))
[], (local_var, Pos.get_position v)
| L.ETuple (args, Some s_name) ->
let args_stmts, new_args =
List.fold_left
(fun (args_stmts, new_args) arg ->
let arg_stmts, new_arg = translate_expr ctxt arg in
(arg_stmts @ args_stmts, new_arg :: new_args))
arg_stmts @ args_stmts, new_arg :: new_args)
([], []) args
in
let new_args = List.rev new_args in
let args_stmts = List.rev args_stmts in
(args_stmts, (A.EStruct (new_args, s_name), Pos.get_position expr))
args_stmts, (A.EStruct (new_args, s_name), Pos.get_position expr)
| L.ETuple (_, None) ->
failwith "Non-struct tuples cannot be compiled to scalc"
| L.ETupleAccess (e1, num_field, Some s_name, _) ->
@ -67,30 +67,30 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Pos.marked) :
let cons_name =
fst (List.nth (D.EnumMap.find e_name ctxt.decl_ctx.ctx_enums) num_cons)
in
(e1_stmts, (A.EInj (new_e1, cons_name, e_name), Pos.get_position expr))
e1_stmts, (A.EInj (new_e1, cons_name, e_name), Pos.get_position expr)
| L.EApp (f, args) ->
let f_stmts, new_f = translate_expr ctxt f in
let args_stmts, new_args =
List.fold_left
(fun (args_stmts, new_args) arg ->
let arg_stmts, new_arg = translate_expr ctxt arg in
(arg_stmts @ args_stmts, new_arg :: new_args))
arg_stmts @ args_stmts, new_arg :: new_args)
([], []) args
in
let new_args = List.rev new_args in
(f_stmts @ args_stmts, (A.EApp (new_f, new_args), Pos.get_position expr))
f_stmts @ args_stmts, (A.EApp (new_f, new_args), Pos.get_position expr)
| L.EArray args ->
let args_stmts, new_args =
List.fold_left
(fun (args_stmts, new_args) arg ->
let arg_stmts, new_arg = translate_expr ctxt arg in
(arg_stmts @ args_stmts, new_arg :: new_args))
arg_stmts @ args_stmts, new_arg :: new_args)
([], []) args
in
let new_args = List.rev new_args in
(args_stmts, (A.EArray new_args, Pos.get_position expr))
| L.EOp op -> ([], (A.EOp op, Pos.get_position expr))
| L.ELit l -> ([], (A.ELit l, Pos.get_position expr))
args_stmts, (A.EArray new_args, Pos.get_position expr)
| L.EOp op -> [], (A.EOp op, Pos.get_position expr)
| L.ELit l -> [], (A.ELit l, Pos.get_position expr)
| _ ->
let tmp_var =
A.LocalName.fresh
@ -125,13 +125,11 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Pos.marked) :
| L.EAssert e ->
(* Assertions are always encapsulated in a unit-typed let binding *)
let e_stmts, new_e = translate_expr ctxt e in
e_stmts @ [ (A.SAssert (Pos.unmark new_e), Pos.get_position block_expr) ]
e_stmts @ [A.SAssert (Pos.unmark new_e), Pos.get_position block_expr]
| L.EApp ((L.EAbs ((binder, binder_pos), taus), eabs_pos), args) ->
(* This defines multiple local variables at the time *)
let vars, body = Bindlib.unmbind binder in
let vars_tau =
List.map2 (fun x tau -> (x, tau)) (Array.to_list vars) taus
in
let vars_tau = List.map2 (fun x tau -> x, tau) (Array.to_list vars) taus in
let ctxt =
{
ctxt with
@ -154,7 +152,7 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Pos.marked) :
let vars_args =
List.map2
(fun (x, tau) arg ->
((L.VarMap.find x ctxt.var_dict, binder_pos), tau, arg))
(L.VarMap.find x ctxt.var_dict, binder_pos), tau, arg)
vars_tau args
in
let def_blocks =
@ -168,16 +166,14 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Pos.marked) :
}
in
let arg_stmts, new_arg = translate_expr ctxt arg in
arg_stmts @ [ (A.SLocalDef (x, new_arg), binder_pos) ])
arg_stmts @ [A.SLocalDef (x, new_arg), binder_pos])
vars_args
in
let rest_of_block = translate_statements ctxt body in
local_decls @ List.flatten def_blocks @ rest_of_block
| L.EAbs ((binder, binder_pos), taus) ->
let vars, body = Bindlib.unmbind binder in
let vars_tau =
List.map2 (fun x tau -> (x, tau)) (Array.to_list vars) taus
in
let vars_tau = List.map2 (fun x tau -> x, tau) (Array.to_list vars) taus in
let closure_name =
match ctxt.inside_definition_of with
| None ->
@ -205,7 +201,7 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Pos.marked) :
func_params =
List.map
(fun (var, tau) ->
((L.VarMap.find var ctxt.var_dict, binder_pos), tau))
(L.VarMap.find var ctxt.var_dict, binder_pos), tau)
vars_tau;
func_body = new_body;
} ),
@ -235,21 +231,18 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Pos.marked) :
in
let new_args = List.rev new_args in
e1_stmts
@ [ (A.SSwitch (new_e1, e_name, new_args), Pos.get_position block_expr) ]
@ [A.SSwitch (new_e1, e_name, new_args), Pos.get_position block_expr]
| L.EIfThenElse (cond, e_true, e_false) ->
let cond_stmts, s_cond = translate_expr ctxt cond in
let s_e_true = translate_statements ctxt e_true in
let s_e_false = translate_statements ctxt e_false in
cond_stmts
@ [
( A.SIfThenElse (s_cond, s_e_true, s_e_false),
Pos.get_position block_expr );
]
@ [A.SIfThenElse (s_cond, s_e_true, s_e_false), Pos.get_position block_expr]
| L.ECatch (e_try, except, e_catch) ->
let s_e_try = translate_statements ctxt e_try in
let s_e_catch = translate_statements ctxt e_catch in
[ (A.STryExcept (s_e_try, except, s_e_catch), Pos.get_position block_expr) ]
| L.ERaise except -> [ (A.SRaise except, Pos.get_position block_expr) ]
[A.STryExcept (s_e_try, except, s_e_catch), Pos.get_position block_expr]
| L.ERaise except -> [A.SRaise except, Pos.get_position block_expr]
| _ -> (
let e_stmts, new_e = translate_expr ctxt block_expr in
e_stmts
@ -287,7 +280,7 @@ let rec translate_scope_body_expr
}
e
in
block @ [ (A.SReturn (Pos.unmark new_e), Pos.get_position new_e) ]
block @ [A.SReturn (Pos.unmark new_e), Pos.get_position new_e]
| ScopeLet scope_let ->
let let_var, scope_let_next = Bindlib.unbind scope_let.scope_let_next in
let let_var_id =

View File

@ -77,16 +77,16 @@ let rec format_expr
| ELit l ->
Format.fprintf fmt "%a" Lcalc.Print.format_lit (Pos.same_pos_as l e)
| EApp
( (EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _),
[ arg1; arg2 ] ) ->
((EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _), [arg1; arg2])
->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" Dcalc.Print.format_binop
(op, Pos.no_pos) format_with_parens arg1 format_with_parens arg2
| EApp ((EOp (Binop op), _), [ arg1; arg2 ]) ->
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1
Dcalc.Print.format_binop (op, Pos.no_pos) format_with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [ arg1 ]) when not debug ->
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug ->
Format.fprintf fmt "%a" format_with_parens arg1
| EApp ((EOp (Unop op), _), [ arg1 ]) ->
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" Dcalc.Print.format_unop
(op, Pos.no_pos) format_with_parens arg1
| EApp (f, args) ->

View File

@ -174,7 +174,7 @@ let rec format_typ (fmt : Format.formatter) (typ : Dcalc.Ast.typ Pos.marked) :
(fun fmt t -> Format.fprintf fmt "%a" format_typ_with_parens t))
ts
| TTuple (_, Some s) -> Format.fprintf fmt "%a" format_struct_name s
| TEnum ([ _; some_typ ], e) when D.EnumName.compare e L.option_enum = 0 ->
| TEnum ([_; some_typ], e) when D.EnumName.compare e L.option_enum = 0 ->
(* We translate the option type with an overloading by Python's [None] *)
Format.fprintf fmt "Optional[%a]" format_typ some_typ
| TEnum (_, e) -> Format.fprintf fmt "%a" format_enum_name e
@ -301,23 +301,22 @@ let rec format_expression
es
| ELit l -> Format.fprintf fmt "%a" format_lit (Pos.same_pos_as l e)
| EApp
( (EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _),
[ arg1; arg2 ] ) ->
((EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _), [arg1; arg2])
->
Format.fprintf fmt "%a(%a,@ %a)" format_binop (op, Pos.no_pos)
(format_expression ctx) arg1 (format_expression ctx) arg2
| EApp ((EOp (Binop op), _), [ arg1; arg2 ]) ->
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "(%a %a@ %a)" (format_expression ctx) arg1 format_binop
(op, Pos.no_pos) (format_expression ctx) arg2
| EApp
((EApp ((EOp (Unop (D.Log (D.BeginCall, info))), _), [ f ]), _), [ arg ])
| EApp ((EApp ((EOp (Unop (D.Log (D.BeginCall, info))), _), [f]), _), [arg])
when !Cli.trace_flag ->
Format.fprintf fmt "log_begin_call(%a,@ %a,@ %a)" format_uid_list info
(format_expression ctx) f (format_expression ctx) arg
| EApp ((EOp (Unop (D.Log (D.VarDef tau, info))), _), [ arg1 ])
| EApp ((EOp (Unop (D.Log (D.VarDef tau, info))), _), [arg1])
when !Cli.trace_flag ->
Format.fprintf fmt "log_variable_definition(%a,@ %a)" format_uid_list info
(format_expression ctx) arg1
| EApp ((EOp (Unop (D.Log (D.PosRecordIfTrueBool, _))), pos), [ arg1 ])
| EApp ((EOp (Unop (D.Log (D.PosRecordIfTrueBool, _))), pos), [arg1])
when !Cli.trace_flag ->
Format.fprintf fmt
"log_decision_taken(SourcePosition(filename=\"%s\",@ start_line=%d,@ \
@ -325,16 +324,16 @@ let rec format_expression
(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
| EApp ((EOp (Unop (D.Log (D.EndCall, info))), _), [ arg1 ])
| EApp ((EOp (Unop (D.Log (D.EndCall, info))), _), [arg1])
when !Cli.trace_flag ->
Format.fprintf fmt "log_end_call(%a,@ %a)" format_uid_list info
(format_expression ctx) arg1
| EApp ((EOp (Unop (D.Log _)), _), [ arg1 ]) ->
| EApp ((EOp (Unop (D.Log _)), _), [arg1]) ->
Format.fprintf fmt "%a" (format_expression ctx) arg1
| EApp ((EOp (Unop ((Minus _ | Not) as op)), _), [ arg1 ]) ->
| EApp ((EOp (Unop ((Minus _ | Not) as op)), _), [arg1]) ->
Format.fprintf fmt "%a %a" format_unop (op, Pos.no_pos)
(format_expression ctx) arg1
| EApp ((EOp (Unop op), _), [ arg1 ]) ->
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "%a(%a)" format_unop (op, Pos.no_pos)
(format_expression ctx) arg1
| EApp (f, args) ->
@ -375,7 +374,7 @@ let rec format_statement
| SIfThenElse (cond, b1, 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
| SSwitch (e1, e_name, [ (case_none, _); (case_some, case_some_var) ])
| SSwitch (e1, e_name, [(case_none, _); (case_some, case_some_var)])
when D.EnumName.compare e_name L.option_enum = 0 ->
(* We translate the option type with an overloading by Python's [None] *)
let tmp_var = LocalName.fresh ("perhaps_none_arg", Pos.no_pos) in
@ -392,7 +391,7 @@ let rec format_statement
| SSwitch (e1, e_name, cases) ->
let cases =
List.map2
(fun (x, y) (cons, _) -> (x, y, cons))
(fun (x, y) (cons, _) -> x, y, cons)
cases
(D.EnumMap.find e_name ctx.ctx_enums)
in
@ -509,7 +508,7 @@ let format_ctx
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun _fmt (i, enum_cons, enum_cons_type) ->
Format.fprintf fmt "%a = %d" format_enum_cons_name enum_cons i))
(List.mapi (fun i (x, y) -> (i, x, y)) enum_cons)
(List.mapi (fun i (x, y) -> i, x, y) enum_cons)
format_enum_name enum_name format_enum_name enum_name format_enum_name
enum_name
in

View File

@ -60,7 +60,7 @@ Set.Make (struct
type t = location Pos.marked
let compare x y =
match (Pos.unmark x, Pos.unmark y) with
match Pos.unmark x, Pos.unmark y with
| ScopeVar (vx, _), ScopeVar (vy, _) -> ScopeVar.compare vx vy
| ( SubScopeVar (_, (xsubindex, _), (xsubvar, _)),
SubScopeVar (_, (ysubindex, _), (ysubvar, _)) ) ->
@ -168,7 +168,7 @@ end
type vars = expr Bindlib.mvar
let make_var ((x, pos) : Var.t Pos.marked) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun v -> (v, pos)) (Bindlib.box_var x)
Bindlib.box_apply (fun v -> v, pos) (Bindlib.box_var x)
let make_abs
(xs : vars)
@ -177,14 +177,14 @@ let make_abs
(taus : typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun b -> (EAbs ((b, pos_binder), taus), pos))
(fun b -> EAbs ((b, pos_binder), taus), pos)
(Bindlib.bind_mvar xs e)
let make_app
(e : expr Pos.marked Bindlib.box)
(u : expr Pos.marked Bindlib.box list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2 (fun e u -> (EApp (e, u), pos)) e (Bindlib.box_list u)
Bindlib.box_apply2 (fun e u -> EApp (e, u), pos) e (Bindlib.box_list u)
let make_let_in
(x : Var.t)
@ -192,11 +192,11 @@ let make_let_in
(e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun e u -> (EApp (e, u), Pos.get_position (Bindlib.unbox e2)))
(make_abs (Array.of_list [ x ]) e2
(fun e u -> EApp (e, u), Pos.get_position (Bindlib.unbox e2))
(make_abs (Array.of_list [x]) e2
(Pos.get_position (Bindlib.unbox e2))
[ tau ]
[tau]
(Pos.get_position (Bindlib.unbox e2)))
(Bindlib.box_list [ e1 ])
(Bindlib.box_list [e1])
module VarMap = Map.Make (Var)

View File

@ -123,14 +123,14 @@ module TVertex = struct
| Enum x -> Ast.EnumName.hash x
let compare x y =
match (x, y) with
match x, y with
| Struct x, Struct y -> Ast.StructName.compare x y
| Enum x, Enum y -> Ast.EnumName.compare x y
| Struct _, Enum _ -> 1
| Enum _, Struct _ -> -1
let equal x y =
match (x, y) with
match x, y with
| Struct x, Struct y -> Ast.StructName.compare x y = 0
| Enum x, Enum y -> Ast.EnumName.compare x y = 0
| _ -> false
@ -242,7 +242,7 @@ let check_type_cycles (structs : Ast.struct_ctx) (enums : Ast.enum_ctx) :
(List.map
(fun v ->
let var_str, var_info =
(Format.asprintf "%a" TVertex.format_t v, TVertex.get_info v)
Format.asprintf "%a" TVertex.format_t v, TVertex.get_info v
in
let succs = TDependencies.succ_e g v in
let _, edge_pos, succ =

View File

@ -99,10 +99,8 @@ let rec format_expr
(Ast.EnumConstructorMap.bindings cases)
| EApp ((EAbs ((binder, _), taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
let xs_tau_arg =
List.map2 (fun (x, tau) arg -> (x, tau, arg)) xs_tau args
in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in
Format.fprintf fmt "@[%a%a@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " ")
@ -115,7 +113,7 @@ let rec format_expr
xs_tau_arg format_expr body
| EAbs ((binder, _), taus) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@]"
Dcalc.Print.format_punctuation "λ"
(Format.pp_print_list
@ -125,12 +123,12 @@ let rec format_expr
"(" format_var x Dcalc.Print.format_punctuation ":" format_typ tau
Dcalc.Print.format_punctuation ")"))
xs_tau Dcalc.Print.format_punctuation "" format_expr body
| EApp ((EOp (Binop op), _), [ arg1; arg2 ]) ->
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[%a@ %a@ %a@]" format_with_parens arg1
Dcalc.Print.format_binop (op, Pos.no_pos) format_with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [ arg1 ]) when not debug ->
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug ->
format_expr fmt arg1
| EApp ((EOp (Unop op), _), [ arg1 ]) ->
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[%a@ %a@]" Dcalc.Print.format_unop (op, Pos.no_pos)
format_with_parens arg1
| EApp (f, args) ->

View File

@ -86,14 +86,14 @@ let merge_defaults
Dcalc.Ast.expr Pos.marked Bindlib.box =
let caller =
Dcalc.Ast.make_app caller
[ Bindlib.box (Dcalc.Ast.ELit Dcalc.Ast.LUnit, Pos.no_pos) ]
[Bindlib.box (Dcalc.Ast.ELit Dcalc.Ast.LUnit, Pos.no_pos)]
Pos.no_pos
in
let body =
Bindlib.box_apply2
(fun caller callee ->
( Dcalc.Ast.EDefault
( [ caller ],
( [caller],
(Dcalc.Ast.ELit (Dcalc.Ast.LBool true), Pos.no_pos),
callee ),
Pos.no_pos ))
@ -111,7 +111,7 @@ let tag_with_log_entry
( Dcalc.Ast.EApp
( ( Dcalc.Ast.EOp (Dcalc.Ast.Unop (Dcalc.Ast.Log (l, markings))),
Pos.get_position e ),
[ e ] ),
[e] ),
Pos.get_position e ))
e
@ -129,7 +129,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
(fun (field_name, _) (d_fields, e_fields) ->
let field_e = Ast.StructFieldMap.find field_name e_fields in
let field_d = translate_expr ctx field_e in
(field_d :: d_fields, Ast.StructFieldMap.remove field_name e_fields))
field_d :: d_fields, Ast.StructFieldMap.remove field_name e_fields)
struct_sig ([], e_fields)
in
if Ast.StructFieldMap.cardinal remaining_e_fields > 0 then
@ -150,7 +150,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
let _, field_index =
try
List.assoc field_name
(List.mapi (fun i (x, y) -> (x, (y, i))) struct_sig)
(List.mapi (fun i (x, y) -> x, (y, i)) struct_sig)
with Not_found ->
Errors.raise_spanned_error (Pos.get_position e)
"The field \"%a\" does not belong to the structure %a"
@ -171,7 +171,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
let _, constructor_index =
try
List.assoc constructor
(List.mapi (fun i (x, y) -> (x, (y, i))) enum_sig)
(List.mapi (fun i (x, y) -> x, (y, i)) enum_sig)
with Not_found ->
Errors.raise_spanned_error (Pos.get_position e)
"The constructor \"%a\" does not belong to the enum %a"
@ -202,8 +202,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
enum_name
in
let case_d = translate_expr ctx case_e in
( case_d :: d_cases,
Ast.EnumConstructorMap.remove constructor e_cases ))
case_d :: d_cases, Ast.EnumConstructorMap.remove constructor e_cases)
enum_sig ([], cases)
in
if Ast.EnumConstructorMap.cardinal remaining_e_cases > 0 then
@ -227,9 +226,9 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
let markings l =
match l with
| Ast.ScopeVar (v, _) ->
[ Ast.ScopeName.get_info ctx.scope_name; Ast.ScopeVar.get_info v ]
[Ast.ScopeName.get_info ctx.scope_name; Ast.ScopeVar.get_info v]
| Ast.SubScopeVar (s, _, (v, _)) ->
[ Ast.ScopeName.get_info s; Ast.ScopeVar.get_info v ]
[Ast.ScopeName.get_info s; Ast.ScopeVar.get_info v]
in
let e1_func =
match Pos.unmark e1 with
@ -239,17 +238,17 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
in
let new_args = List.map (translate_expr ctx) args in
let new_args =
match (Pos.unmark e1, new_args) with
| ELocation l, [ new_arg ] ->
match Pos.unmark e1, new_args with
| ELocation l, [new_arg] ->
[
tag_with_log_entry new_arg (Dcalc.Ast.VarDef Dcalc.Ast.TAny)
(markings l @ [ Pos.same_pos_as "input" e ]);
(markings l @ [Pos.same_pos_as "input" e]);
]
| _ -> new_args
in
let new_e =
Bindlib.box_apply2
(fun e' u -> (Dcalc.Ast.EApp (e', u), Pos.get_position e))
(fun e' u -> Dcalc.Ast.EApp (e', u), Pos.get_position e)
e1_func
(Bindlib.box_list new_args)
in
@ -258,7 +257,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
| ELocation l ->
tag_with_log_entry
(tag_with_log_entry new_e (Dcalc.Ast.VarDef Dcalc.Ast.TAny)
(markings l @ [ Pos.same_pos_as "output" e ]))
(markings l @ [Pos.same_pos_as "output" e]))
Dcalc.Ast.EndCall (markings l)
| _ -> new_e
in
@ -270,7 +269,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
(fun x -> Dcalc.Ast.Var.make (Bindlib.name_of x, Pos.no_pos))
xs
in
let both_xs = Array.map2 (fun x new_x -> (x, new_x)) xs new_xs in
let both_xs = Array.map2 (fun x new_x -> x, new_x) xs new_xs in
let body =
translate_expr
{
@ -305,7 +304,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
with Not_found ->
Errors.raise_multispanned_error
[
(Some "Incriminated variable usage:", Pos.get_position e);
Some "Incriminated variable usage:", Pos.get_position e;
( Some "Incriminated subscope variable declaration:",
Pos.get_position (Ast.ScopeVar.get_info (Pos.unmark a)) );
( Some "Incriminated subscope declaration:",
@ -352,7 +351,7 @@ let translate_rule
let merged_expr =
Bindlib.box_apply
(fun merged_expr ->
(Dcalc.Ast.ErrorOnEmpty merged_expr, Pos.get_position a_name))
Dcalc.Ast.ErrorOnEmpty merged_expr, Pos.get_position a_name)
(match Pos.unmark a_io.io_input with
| OnlyInput ->
failwith "should not happen"
@ -364,7 +363,7 @@ let translate_rule
let merged_expr =
tag_with_log_entry merged_expr
(Dcalc.Ast.VarDef (Pos.unmark tau))
[ (sigma_name, pos_sigma); a_name ]
[sigma_name, pos_sigma; a_name]
in
( (fun next ->
Bindlib.box_apply2
@ -402,7 +401,7 @@ let translate_rule
let new_e =
tag_with_log_entry (translate_expr ctx e)
(Dcalc.Ast.VarDef (Pos.unmark tau))
[ (sigma_name, pos_sigma); a_name ]
[sigma_name, pos_sigma; a_name]
in
let silent_var = Dcalc.Ast.Var.make ("_", Pos.no_pos) in
let thunked_or_nonempty_new_e =
@ -410,14 +409,13 @@ let translate_rule
| NoInput -> failwith "should not happen"
| OnlyInput ->
Bindlib.box_apply
(fun new_e ->
(Dcalc.Ast.ErrorOnEmpty new_e, Pos.get_position subs_var))
(fun new_e -> Dcalc.Ast.ErrorOnEmpty new_e, Pos.get_position subs_var)
new_e
| Reentrant ->
Dcalc.Ast.make_abs
(Array.of_list [ silent_var ])
(Array.of_list [silent_var])
new_e var_def_pos
[ (Dcalc.Ast.TLit TUnit, var_def_pos) ]
[Dcalc.Ast.TLit TUnit, var_def_pos]
var_def_pos
in
( (fun next ->
@ -516,7 +514,7 @@ let translate_rule
Pos.unmark (Ast.SubScopeName.get_info subindex) ^ "." ^ s)
(Ast.ScopeVar.get_info subvar.scope_var_name))
in
(subvar, sub_dcalc_var))
subvar, sub_dcalc_var)
all_subscope_output_vars
in
let subscope_func =
@ -526,7 +524,7 @@ let translate_rule
Pos.get_position (Ast.SubScopeName.get_info subindex) ))
Dcalc.Ast.BeginCall
[
(sigma_name, pos_sigma);
sigma_name, pos_sigma;
Ast.SubScopeName.get_info subindex;
Ast.ScopeName.get_info subname;
]
@ -534,11 +532,11 @@ let translate_rule
let call_expr =
tag_with_log_entry
(Bindlib.box_apply2
(fun e u -> (Dcalc.Ast.EApp (e, [ u ]), Pos.no_pos))
(fun e u -> Dcalc.Ast.EApp (e, [u]), Pos.no_pos)
subscope_func subscope_struct_arg)
Dcalc.Ast.EndCall
[
(sigma_name, pos_sigma);
sigma_name, pos_sigma;
Ast.SubScopeName.get_info subindex;
Ast.ScopeName.get_info subname;
]
@ -547,7 +545,7 @@ let translate_rule
let result_tuple_typ =
( Dcalc.Ast.TTuple
( List.map
(fun (subvar, _) -> (subvar.scope_var_typ, pos_sigma))
(fun (subvar, _) -> subvar.scope_var_typ, pos_sigma)
all_subscope_output_vars_dcalc,
Some called_scope_return_struct ),
pos_sigma )
@ -577,7 +575,7 @@ let translate_rule
{
Dcalc.Ast.scope_let_next = next;
Dcalc.Ast.scope_let_pos = pos_sigma;
Dcalc.Ast.scope_let_typ = (var_ctx.scope_var_typ, pos_sigma);
Dcalc.Ast.scope_let_typ = var_ctx.scope_var_typ, pos_sigma;
Dcalc.Ast.scope_let_kind =
Dcalc.Ast.DestructuringSubScopeResults;
Dcalc.Ast.scope_let_expr =
@ -587,7 +585,7 @@ let translate_rule
Some called_scope_return_struct,
List.map
(fun (var_ctx, _) ->
(var_ctx.scope_var_typ, pos_sigma))
var_ctx.scope_var_typ, pos_sigma)
all_subscope_output_vars_dcalc ),
pos_sigma );
})
@ -620,7 +618,7 @@ let translate_rule
Dcalc.Ast.scope_let_next = next;
Dcalc.Ast.scope_let_pos = Pos.get_position e;
Dcalc.Ast.scope_let_typ =
(Dcalc.Ast.TLit TUnit, Pos.get_position e);
Dcalc.Ast.TLit TUnit, Pos.get_position e;
Dcalc.Ast.scope_let_expr =
(* To ensure that we throw an error if the value is not
defined, we add an check "ErrorOnEmpty" here. *)
@ -646,7 +644,7 @@ let translate_rules
let new_scope_lets, new_ctx =
translate_rule ctx rule (sigma_name, pos_sigma)
in
((fun next -> scope_lets (new_scope_lets next)), new_ctx))
(fun next -> scope_lets (new_scope_lets next)), new_ctx)
((fun next -> next), ctx)
rules
in
@ -659,7 +657,7 @@ let translate_rules
let return_exp =
Bindlib.box_apply
(fun args ->
(Dcalc.Ast.ETuple (args, Some sigma_return_struct_name), pos_sigma))
Dcalc.Ast.ETuple (args, Some sigma_return_struct_name), pos_sigma)
(Bindlib.box_list
(List.map
(fun (_, (dcalc_var, _, _)) ->
@ -718,7 +716,7 @@ let translate_scope_decl
let dcalc_x, _, _ =
Ast.ScopeVarMap.find var_ctx.scope_var_name ctx.scope_vars
in
(var_ctx, dcalc_x))
var_ctx, dcalc_x)
scope_variables
in
(* first we create variables from the fields of the input struct *)
@ -737,7 +735,7 @@ let translate_scope_decl
in
let input_var_typ (var_ctx : scope_var_ctx) =
match Pos.unmark var_ctx.scope_var_io.io_input with
| OnlyInput -> (var_ctx.scope_var_typ, pos_sigma)
| OnlyInput -> var_ctx.scope_var_typ, pos_sigma
| Reentrant ->
( Dcalc.Ast.TArrow
((Dcalc.Ast.TLit TUnit, pos_sigma), (var_ctx.scope_var_typ, pos_sigma)),
@ -780,7 +778,7 @@ let translate_scope_decl
let struct_field_name =
Ast.StructFieldName.fresh (Bindlib.name_of dvar ^ "_out", pos_sigma)
in
(struct_field_name, (var_ctx.scope_var_typ, pos_sigma)))
struct_field_name, (var_ctx.scope_var_typ, pos_sigma))
scope_output_variables
in
let scope_input_struct_fields =
@ -789,7 +787,7 @@ let translate_scope_decl
let struct_field_name =
Ast.StructFieldName.fresh (Bindlib.name_of dvar ^ "_in", pos_sigma)
in
(struct_field_name, input_var_typ var_ctx))
struct_field_name, input_var_typ var_ctx)
scope_input_variables
in
let new_struct_ctx =
@ -827,12 +825,12 @@ let translate_program (prgm : Ast.program) :
Dcalc.Ast.ctx_structs =
Ast.StructMap.map
(List.map (fun (x, y) ->
(x, translate_typ (ctx_for_typ_translation dummy_scope) y)))
x, translate_typ (ctx_for_typ_translation dummy_scope) y))
struct_ctx;
Dcalc.Ast.ctx_enums =
Ast.EnumMap.map
(List.map (fun (x, y) ->
(x, (translate_typ (ctx_for_typ_translation dummy_scope)) y)))
x, (translate_typ (ctx_for_typ_translation dummy_scope)) y))
enum_ctx;
}
in
@ -906,8 +904,8 @@ let translate_program (prgm : Ast.program) :
Dcalc.Ast.ScopeDef { scope_name; scope_body; scope_next })
scope_body scope_next
in
(new_scopes, decl_ctx))
new_scopes, decl_ctx)
scope_ordering
(Bindlib.box Dcalc.Ast.Nil, decl_ctx)
in
({ scopes = Bindlib.unbox scopes; decl_ctx }, types_ordering)
{ scopes = Bindlib.unbox scopes; decl_ctx }, types_ordering

View File

@ -47,13 +47,13 @@ type qident = ident Pos.marked list
visitors
{
variety = "map";
ancestors = [ "Pos.marked_map"; "ident_map" ];
ancestors = ["Pos.marked_map"; "ident_map"];
name = "qident_map";
},
visitors
{
variety = "iter";
ancestors = [ "Pos.marked_iter"; "ident_iter" ];
ancestors = ["Pos.marked_iter"; "ident_iter"];
name = "qident_iter";
}]
@ -70,13 +70,13 @@ type primitive_typ =
visitors
{
variety = "map";
ancestors = [ "constructor_map" ];
ancestors = ["constructor_map"];
name = "primitive_typ_map";
},
visitors
{
variety = "iter";
ancestors = [ "constructor_iter" ];
ancestors = ["constructor_iter"];
name = "primitive_typ_iter";
}]
@ -87,13 +87,13 @@ type base_typ_data =
visitors
{
variety = "map";
ancestors = [ "Pos.marked_map"; "primitive_typ_map" ];
ancestors = ["Pos.marked_map"; "primitive_typ_map"];
name = "base_typ_data_map";
},
visitors
{
variety = "iter";
ancestors = [ "Pos.marked_iter"; "primitive_typ_iter" ];
ancestors = ["Pos.marked_iter"; "primitive_typ_iter"];
name = "base_typ_data_iter";
}]
@ -102,14 +102,14 @@ type base_typ = Condition | Data of base_typ_data
visitors
{
variety = "map";
ancestors = [ "base_typ_data_map" ];
ancestors = ["base_typ_data_map"];
name = "base_typ_map";
nude = true;
},
visitors
{
variety = "iter";
ancestors = [ "base_typ_data_iter" ];
ancestors = ["base_typ_data_iter"];
name = "base_typ_iter";
nude = true;
}]
@ -122,14 +122,14 @@ type func_typ = {
visitors
{
variety = "map";
ancestors = [ "base_typ_map" ];
ancestors = ["base_typ_map"];
name = "func_typ_map";
nude = true;
},
visitors
{
variety = "iter";
ancestors = [ "base_typ_iter" ];
ancestors = ["base_typ_iter"];
name = "func_typ_iter";
nude = true;
}]
@ -139,14 +139,14 @@ type typ = Base of base_typ | Func of func_typ
visitors
{
variety = "map";
ancestors = [ "func_typ_map" ];
ancestors = ["func_typ_map"];
name = "typ_map";
nude = true;
},
visitors
{
variety = "iter";
ancestors = [ "func_typ_iter" ];
ancestors = ["func_typ_iter"];
name = "typ_iter";
nude = true;
}]
@ -159,13 +159,13 @@ type struct_decl_field = {
visitors
{
variety = "map";
ancestors = [ "typ_map"; "ident_map" ];
ancestors = ["typ_map"; "ident_map"];
name = "struct_decl_field_map";
},
visitors
{
variety = "iter";
ancestors = [ "typ_iter"; "ident_iter" ];
ancestors = ["typ_iter"; "ident_iter"];
name = "struct_decl_field_iter";
}]
@ -177,13 +177,13 @@ type struct_decl = {
visitors
{
variety = "map";
ancestors = [ "struct_decl_field_map" ];
ancestors = ["struct_decl_field_map"];
name = "struct_decl_map";
},
visitors
{
variety = "iter";
ancestors = [ "struct_decl_field_iter" ];
ancestors = ["struct_decl_field_iter"];
name = "struct_decl_iter";
}]
@ -195,14 +195,14 @@ type enum_decl_case = {
visitors
{
variety = "map";
ancestors = [ "typ_map" ];
ancestors = ["typ_map"];
name = "enum_decl_case_map";
nude = true;
},
visitors
{
variety = "iter";
ancestors = [ "typ_iter" ];
ancestors = ["typ_iter"];
name = "enum_decl_case_iter";
nude = true;
}]
@ -215,14 +215,14 @@ type enum_decl = {
visitors
{
variety = "map";
ancestors = [ "enum_decl_case_map" ];
ancestors = ["enum_decl_case_map"];
name = "enum_decl_map";
nude = true;
},
visitors
{
variety = "iter";
ancestors = [ "enum_decl_case_iter" ];
ancestors = ["enum_decl_case_iter"];
name = "enum_decl_iter";
nude = true;
}]
@ -234,13 +234,13 @@ type match_case_pattern =
visitors
{
variety = "map";
ancestors = [ "ident_map"; "constructor_map"; "Pos.marked_map" ];
ancestors = ["ident_map"; "constructor_map"; "Pos.marked_map"];
name = "match_case_pattern_map";
},
visitors
{
variety = "iter";
ancestors = [ "ident_iter"; "constructor_iter"; "Pos.marked_iter" ];
ancestors = ["ident_iter"; "constructor_iter"; "Pos.marked_iter"];
name = "match_case_pattern_iter";
}]
@ -268,14 +268,14 @@ type binop =
visitors
{
variety = "map";
ancestors = [ "op_kind_map" ];
ancestors = ["op_kind_map"];
name = "binop_map";
nude = true;
},
visitors
{
variety = "iter";
ancestors = [ "op_kind_iter" ];
ancestors = ["op_kind_iter"];
name = "binop_iter";
nude = true;
}]
@ -285,14 +285,14 @@ type unop = Not | Minus of op_kind
visitors
{
variety = "map";
ancestors = [ "op_kind_map" ];
ancestors = ["op_kind_map"];
name = "unop_map";
nude = true;
},
visitors
{
variety = "iter";
ancestors = [ "op_kind_iter" ];
ancestors = ["op_kind_iter"];
name = "unop_iter";
nude = true;
}]
@ -318,13 +318,13 @@ type literal_date = {
visitors
{
variety = "map";
ancestors = [ "Pos.marked_map" ];
ancestors = ["Pos.marked_map"];
name = "literal_date_map";
},
visitors
{
variety = "iter";
ancestors = [ "Pos.marked_iter" ];
ancestors = ["Pos.marked_iter"];
name = "literal_date_iter";
}]
@ -468,13 +468,13 @@ type exception_to =
visitors
{
variety = "map";
ancestors = [ "ident_map"; "Pos.marked_map" ];
ancestors = ["ident_map"; "Pos.marked_map"];
name = "exception_to_map";
},
visitors
{
variety = "iter";
ancestors = [ "ident_iter"; "Pos.marked_iter" ];
ancestors = ["ident_iter"; "Pos.marked_iter"];
name = "exception_to_iter";
}]
@ -492,13 +492,13 @@ type rule = {
visitors
{
variety = "map";
ancestors = [ "expression_map"; "qident_map"; "exception_to_map" ];
ancestors = ["expression_map"; "qident_map"; "exception_to_map"];
name = "rule_map";
},
visitors
{
variety = "iter";
ancestors = [ "expression_iter"; "qident_iter"; "exception_to_iter" ];
ancestors = ["expression_iter"; "qident_iter"; "exception_to_iter"];
name = "rule_iter";
}]
@ -516,13 +516,13 @@ type definition = {
visitors
{
variety = "map";
ancestors = [ "expression_map"; "qident_map"; "exception_to_map" ];
ancestors = ["expression_map"; "qident_map"; "exception_to_map"];
name = "definition_map";
},
visitors
{
variety = "iter";
ancestors = [ "expression_iter"; "qident_iter"; "exception_to_iter" ];
ancestors = ["expression_iter"; "qident_iter"; "exception_to_iter"];
name = "definition_iter";
}]
@ -541,13 +541,13 @@ type meta_assertion =
visitors
{
variety = "map";
ancestors = [ "variation_typ_map"; "qident_map"; "expression_map" ];
ancestors = ["variation_typ_map"; "qident_map"; "expression_map"];
name = "meta_assertion_map";
},
visitors
{
variety = "iter";
ancestors = [ "variation_typ_iter"; "qident_iter"; "expression_iter" ];
ancestors = ["variation_typ_iter"; "qident_iter"; "expression_iter"];
name = "meta_assertion_iter";
}]
@ -557,15 +557,11 @@ type assertion = {
}
[@@deriving
visitors
{
variety = "map";
ancestors = [ "expression_map" ];
name = "assertion_map";
},
{ variety = "map"; ancestors = ["expression_map"]; name = "assertion_map" },
visitors
{
variety = "iter";
ancestors = [ "expression_iter" ];
ancestors = ["expression_iter"];
name = "assertion_iter";
}]
@ -579,7 +575,7 @@ type scope_use_item =
{
variety = "map";
ancestors =
[ "meta_assertion_map"; "definition_map"; "assertion_map"; "rule_map" ];
["meta_assertion_map"; "definition_map"; "assertion_map"; "rule_map"];
name = "scope_use_item_map";
},
visitors
@ -604,13 +600,13 @@ type scope_use = {
visitors
{
variety = "map";
ancestors = [ "expression_map"; "scope_use_item_map" ];
ancestors = ["expression_map"; "scope_use_item_map"];
name = "scope_use_map";
},
visitors
{
variety = "iter";
ancestors = [ "expression_iter"; "scope_use_item_iter" ];
ancestors = ["expression_iter"; "scope_use_item_iter"];
name = "scope_use_iter";
}]
@ -627,13 +623,13 @@ type scope_decl_context_io = {
visitors
{
variety = "map";
ancestors = [ "io_input_map"; "Pos.marked_map" ];
ancestors = ["io_input_map"; "Pos.marked_map"];
name = "scope_decl_context_io_map";
},
visitors
{
variety = "iter";
ancestors = [ "io_input_iter"; "Pos.marked_iter" ];
ancestors = ["io_input_iter"; "Pos.marked_iter"];
name = "scope_decl_context_io_iter";
}]
@ -678,13 +674,13 @@ type scope_decl_context_data = {
visitors
{
variety = "map";
ancestors = [ "typ_map"; "scope_decl_context_io_map"; "ident_map" ];
ancestors = ["typ_map"; "scope_decl_context_io_map"; "ident_map"];
name = "scope_decl_context_data_map";
},
visitors
{
variety = "iter";
ancestors = [ "typ_iter"; "scope_decl_context_io_iter"; "ident_iter" ];
ancestors = ["typ_iter"; "scope_decl_context_io_iter"; "ident_iter"];
name = "scope_decl_context_data_iter";
}]
@ -696,14 +692,14 @@ type scope_decl_context_item =
{
variety = "map";
ancestors =
[ "scope_decl_context_data_map"; "scope_decl_context_scope_map" ];
["scope_decl_context_data_map"; "scope_decl_context_scope_map"];
name = "scope_decl_context_item_map";
},
visitors
{
variety = "iter";
ancestors =
[ "scope_decl_context_data_iter"; "scope_decl_context_scope_iter" ];
["scope_decl_context_data_iter"; "scope_decl_context_scope_iter"];
name = "scope_decl_context_item_iter";
}]
@ -715,13 +711,13 @@ type scope_decl = {
visitors
{
variety = "map";
ancestors = [ "scope_decl_context_item_map" ];
ancestors = ["scope_decl_context_item_map"];
name = "scope_decl_map";
},
visitors
{
variety = "iter";
ancestors = [ "scope_decl_context_item_iter" ];
ancestors = ["scope_decl_context_item_iter"];
name = "scope_decl_iter";
}]
@ -735,9 +731,7 @@ type code_item =
{
variety = "map";
ancestors =
[
"scope_decl_map"; "enum_decl_map"; "struct_decl_map"; "scope_use_map";
];
["scope_decl_map"; "enum_decl_map"; "struct_decl_map"; "scope_use_map"];
name = "code_item_map";
},
visitors
@ -756,15 +750,11 @@ type code_item =
type code_block = code_item Pos.marked list
[@@deriving
visitors
{
variety = "map";
ancestors = [ "code_item_map" ];
name = "code_block_map";
},
{ variety = "map"; ancestors = ["code_item_map"]; name = "code_block_map" },
visitors
{
variety = "iter";
ancestors = [ "code_item_iter" ];
ancestors = ["code_item_iter"];
name = "code_block_iter";
}]
@ -773,13 +763,13 @@ type source_repr = (string[@opaque]) Pos.marked
visitors
{
variety = "map";
ancestors = [ "Pos.marked_map" ];
ancestors = ["Pos.marked_map"];
name = "source_repr_map";
},
visitors
{
variety = "iter";
ancestors = [ "Pos.marked_iter" ];
ancestors = ["Pos.marked_iter"];
name = "source_repr_iter";
}]
@ -793,13 +783,13 @@ type law_heading = {
visitors
{
variety = "map";
ancestors = [ "Pos.marked_map" ];
ancestors = ["Pos.marked_map"];
name = "law_heading_map";
},
visitors
{
variety = "iter";
ancestors = [ "Pos.marked_iter" ];
ancestors = ["Pos.marked_iter"];
name = "law_heading_iter";
}]
@ -811,13 +801,13 @@ type law_include =
visitors
{
variety = "map";
ancestors = [ "Pos.marked_map" ];
ancestors = ["Pos.marked_map"];
name = "law_include_map";
},
visitors
{
variety = "iter";
ancestors = [ "Pos.marked_iter" ];
ancestors = ["Pos.marked_iter"];
name = "law_include_iter";
}]
@ -858,15 +848,11 @@ type program = {
}
[@@deriving
visitors
{
variety = "map";
ancestors = [ "law_structure_map" ];
name = "program_map";
},
{ variety = "map"; ancestors = ["law_structure_map"]; name = "program_map" },
visitors
{
variety = "iter";
ancestors = [ "law_structure_iter" ];
ancestors = ["law_structure_iter"];
name = "program_iter";
}]
@ -884,6 +870,6 @@ let rule_to_def (rule : rule) : definition =
definition_parameter = rule.rule_parameter;
definition_condition = rule.rule_condition;
definition_id = rule.rule_id;
definition_expr = (consequence_expr, Pos.get_position rule.rule_consequence);
definition_expr = consequence_expr, Pos.get_position rule.rule_consequence;
definition_state = rule.rule_state;
}

View File

@ -66,7 +66,7 @@ let disambiguate_constructor
(pos : Pos.t) : Scopelang.Ast.EnumName.t * Scopelang.Ast.EnumConstructor.t =
let enum, constructor =
match constructor with
| [ c ] -> c
| [c] -> c
| _ ->
Errors.raise_spanned_error pos
"The deep pattern matching syntactic sugar is not yet supported"
@ -102,7 +102,7 @@ let disambiguate_constructor
in
try
let c_uid = Scopelang.Ast.EnumMap.find e_uid possible_c_uids in
(e_uid, c_uid)
e_uid, c_uid
with Not_found ->
Errors.raise_spanned_error pos "Enum %s does not contain case %s"
(Pos.unmark enum) (Pos.unmark constructor)
@ -141,23 +141,23 @@ let rec translate_expr
Bindlib.unbox
(Desugared.Ast.make_abs [| nop_var |]
(Bindlib.box (Desugared.Ast.ELit (Dcalc.Ast.LBool false), pos))
pos [ tau ] pos)
pos [tau] pos)
else
let ctxt, binding_var =
Name_resolution.add_def_local_var ctxt binding
in
let e2 = translate_expr scope inside_definition_of ctxt e2 in
Bindlib.unbox
(Desugared.Ast.make_abs [| binding_var |] e2 pos [ tau ] pos))
(Desugared.Ast.make_abs [| binding_var |] e2 pos [tau] pos))
(Scopelang.Ast.EnumMap.find enum_uid ctxt.enums)
in
Bindlib.box_apply
(fun e1_sub -> (Desugared.Ast.EMatch (e1_sub, enum_uid, cases), pos))
(fun e1_sub -> Desugared.Ast.EMatch (e1_sub, enum_uid, cases), pos)
(translate_expr scope inside_definition_of ctxt e1_sub)
| IfThenElse (e_if, e_then, e_else) ->
Bindlib.box_apply3
(fun e_if e_then e_else ->
(Desugared.Ast.EIfThenElse (e_if, e_then, e_else), pos))
Desugared.Ast.EIfThenElse (e_if, e_then, e_else), pos)
(rec_helper e_if) (rec_helper e_then) (rec_helper e_else)
| Binop (op, e1, e2) ->
let op_term =
@ -166,7 +166,7 @@ let rec translate_expr
op
in
Bindlib.box_apply2
(fun e1 e2 -> (Desugared.Ast.EApp (op_term, [ e1; e2 ]), pos))
(fun e1 e2 -> Desugared.Ast.EApp (op_term, [e1; e2]), pos)
(rec_helper e1) (rec_helper e2)
| Unop (op, e) ->
let op_term =
@ -175,7 +175,7 @@ let rec translate_expr
op
in
Bindlib.box_apply
(fun e -> (Desugared.Ast.EApp (op_term, [ e ]), pos))
(fun e -> Desugared.Ast.EApp (op_term, [e]), pos)
(rec_helper e)
| Literal l ->
let untyped_term =
@ -344,7 +344,7 @@ let rec translate_expr
Scopelang.Ast.StructMap.choose x_possible_structs
in
Bindlib.box_apply
(fun e -> (Desugared.Ast.EStructAccess (e, f_uid, s_uid), pos))
(fun e -> Desugared.Ast.EStructAccess (e, f_uid, s_uid), pos)
e
| Some c_name -> (
try
@ -354,7 +354,7 @@ let rec translate_expr
try
let f_uid = Scopelang.Ast.StructMap.find c_uid x_possible_structs in
Bindlib.box_apply
(fun e -> (Desugared.Ast.EStructAccess (e, f_uid, c_uid), pos))
(fun e -> Desugared.Ast.EStructAccess (e, f_uid, c_uid), pos)
e
with Not_found ->
Errors.raise_spanned_error pos "Struct %s does not contain field %s"
@ -364,7 +364,7 @@ let rec translate_expr
"Struct %s has not been defined before" (Pos.unmark c_name))))
| FunCall (f, arg) ->
Bindlib.box_apply2
(fun f arg -> (Desugared.Ast.EApp (f, [ arg ]), pos))
(fun f arg -> Desugared.Ast.EApp (f, [arg]), pos)
(rec_helper f) (rec_helper arg)
| StructLit (s_name, fields) ->
let s_uid =
@ -392,8 +392,8 @@ let rec translate_expr
| Some e_field ->
Errors.raise_multispanned_error
[
(None, Pos.get_position f_e);
(None, Pos.get_position (Bindlib.unbox e_field));
None, Pos.get_position f_e;
None, Pos.get_position (Bindlib.unbox e_field);
]
"The field %a has been defined twice:"
Scopelang.Ast.StructFieldName.format_t f_uid);
@ -412,7 +412,7 @@ let rec translate_expr
expected_s_fields;
Bindlib.box_apply
(fun s_fields -> (Desugared.Ast.EStruct (s_uid, s_fields), pos))
(fun s_fields -> Desugared.Ast.EStruct (s_uid, s_fields), pos)
(LiftStructFieldMap.lift_box s_fields)
| EnumInject (enum, constructor, payload) -> (
let possible_c_uids =
@ -494,7 +494,7 @@ let rec translate_expr
cases
in
Bindlib.box_apply2
(fun e1 cases_d -> (Desugared.Ast.EMatch (e1, e_uid, cases_d), pos))
(fun e1 cases_d -> Desugared.Ast.EMatch (e1, e_uid, cases_d), pos)
e1
(LiftEnumConstructorMap.lift_box cases_d)
| TestMatchCase (e1, pattern) ->
@ -519,15 +519,15 @@ let rec translate_expr
(Dcalc.Ast.LBool
(Scopelang.Ast.EnumConstructor.compare c_uid c_uid' = 0)),
pos ))
pos [ tau ] pos))
pos [tau] pos))
(Scopelang.Ast.EnumMap.find enum_uid ctxt.enums)
in
Bindlib.box_apply
(fun e -> (Desugared.Ast.EMatch (e, enum_uid, cases), pos))
(fun e -> Desugared.Ast.EMatch (e, enum_uid, cases), pos)
(translate_expr scope inside_definition_of ctxt e1)
| ArrayLit es ->
Bindlib.box_apply
(fun es -> (Desugared.Ast.EArray es, pos))
(fun es -> Desugared.Ast.EArray es, pos)
(Bindlib.box_list (List.map rec_helper es))
| CollectionOp
( (((Ast.Filter | Ast.Map) as op'), _pos_op'),
@ -540,7 +540,7 @@ let rec translate_expr
Desugared.Ast.make_abs [| param |]
(translate_expr scope inside_definition_of ctxt predicate)
pos
[ (Scopelang.Ast.TAny, pos) ]
[Scopelang.Ast.TAny, pos]
pos
in
Bindlib.box_apply2
@ -552,7 +552,7 @@ let rec translate_expr
| Ast.Filter -> Dcalc.Ast.Binop Dcalc.Ast.Filter
| _ -> assert false (* should not happen *)),
pos ),
[ f_pred; collection ] ),
[f_pred; collection] ),
pos ))
f_pred collection
| CollectionOp
@ -584,7 +584,7 @@ let rec translate_expr
Desugared.Ast.make_abs [| param |]
(translate_expr scope inside_definition_of ctxt predicate)
pos
[ (Scopelang.Ast.TAny, pos) ]
[Scopelang.Ast.TAny, pos]
pos
in
let f_pred_var =
@ -610,8 +610,8 @@ let rec translate_expr
( ( Desugared.Ast.EApp
( (Desugared.Ast.EOp (Dcalc.Ast.Binop cmp_op), pos_op'),
[
(Desugared.Ast.EApp (f_pred_var_e, [ acc_var_e ]), pos);
(Desugared.Ast.EApp (f_pred_var_e, [ item_var_e ]), pos);
Desugared.Ast.EApp (f_pred_var_e, [acc_var_e]), pos;
Desugared.Ast.EApp (f_pred_var_e, [item_var_e]), pos;
] ),
pos ),
acc_var_e,
@ -621,7 +621,7 @@ let rec translate_expr
in
let fold_f =
Desugared.Ast.make_abs [| acc_var; item_var |] fold_body pos
[ (Scopelang.Ast.TAny, pos); (Scopelang.Ast.TAny, pos) ]
[Scopelang.Ast.TAny, pos; Scopelang.Ast.TAny, pos]
pos
in
let fold =
@ -629,7 +629,7 @@ let rec translate_expr
(fun fold_f collection init ->
( Desugared.Ast.EApp
( (Desugared.Ast.EOp (Dcalc.Ast.Ternop Dcalc.Ast.Fold), pos),
[ fold_f; init; collection ] ),
[fold_f; init; collection] ),
pos ))
fold_f collection init
in
@ -684,7 +684,7 @@ let rec translate_expr
(fun predicate acc ->
( Desugared.Ast.EApp
( (Desugared.Ast.EOp (Dcalc.Ast.Binop op), Pos.get_position op'),
[ acc; predicate ] ),
[acc; predicate] ),
pos ))
(translate_expr scope inside_definition_of ctxt predicate)
acc
@ -702,7 +702,7 @@ let rec translate_expr
( ( Desugared.Ast.EApp
( ( Desugared.Ast.EOp (Dcalc.Ast.Binop cmp_op),
Pos.get_position op' ),
[ acc; tmp ] ),
[acc; tmp] ),
pos ),
acc,
tmp ),
@ -727,12 +727,12 @@ let rec translate_expr
| Ast.Aggregate (Ast.AggregateExtremum (max_or_min, t, _)) ->
let op_kind, typ =
match t with
| Ast.Integer -> (Dcalc.Ast.KInt, (Scopelang.Ast.TLit TInt, pos))
| Ast.Decimal -> (Dcalc.Ast.KRat, (Scopelang.Ast.TLit TRat, pos))
| Ast.Money -> (Dcalc.Ast.KMoney, (Scopelang.Ast.TLit TMoney, pos))
| Ast.Integer -> Dcalc.Ast.KInt, (Scopelang.Ast.TLit TInt, pos)
| Ast.Decimal -> Dcalc.Ast.KRat, (Scopelang.Ast.TLit TRat, pos)
| Ast.Money -> Dcalc.Ast.KMoney, (Scopelang.Ast.TLit TMoney, pos)
| Ast.Duration ->
(Dcalc.Ast.KDuration, (Scopelang.Ast.TLit TDuration, pos))
| Ast.Date -> (Dcalc.Ast.KDate, (Scopelang.Ast.TLit TDate, pos))
Dcalc.Ast.KDuration, (Scopelang.Ast.TLit TDuration, pos)
| Ast.Date -> Dcalc.Ast.KDate, (Scopelang.Ast.TLit TDate, pos)
| _ ->
Errors.raise_spanned_error pos
"It is impossible to compute the %s of two values of type %a"
@ -771,8 +771,8 @@ let rec translate_expr
( Desugared.Ast.EAbs
( (binder, pos),
[
(Scopelang.Ast.TLit t, Pos.get_position op');
(Scopelang.Ast.TAny, pos)
Scopelang.Ast.TLit t, Pos.get_position op';
Scopelang.Ast.TAny, pos
(* we put any here because the type of the elements of the
arrays is not always the type of the accumulator; for
instance in AggregateCount. *);
@ -806,7 +806,7 @@ let rec translate_expr
(fun f collection init ->
( Desugared.Ast.EApp
( (Desugared.Ast.EOp (Dcalc.Ast.Ternop Dcalc.Ast.Fold), pos),
[ f; init; collection ] ),
[f; init; collection] ),
pos ))
f collection init
| MemCollection (member, collection) ->
@ -824,7 +824,7 @@ let rec translate_expr
[
( Desugared.Ast.EApp
( (Desugared.Ast.EOp (Dcalc.Ast.Binop Dcalc.Ast.Eq), pos),
[ member; param ] ),
[member; param] ),
pos );
acc;
] ),
@ -838,8 +838,8 @@ let rec translate_expr
( Desugared.Ast.EAbs
( (binder, pos),
[
(Scopelang.Ast.TLit Dcalc.Ast.TBool, pos);
(Scopelang.Ast.TAny, pos);
Scopelang.Ast.TLit Dcalc.Ast.TBool, pos;
Scopelang.Ast.TAny, pos;
] ),
pos ))
(Bindlib.bind_mvar [| acc_var; param_var |] f_body)
@ -848,7 +848,7 @@ let rec translate_expr
(fun f collection init ->
( Desugared.Ast.EApp
( (Desugared.Ast.EOp (Dcalc.Ast.Ternop Dcalc.Ast.Fold), pos),
[ f; init; collection ] ),
[f; init; collection] ),
pos ))
f collection init
| Builtin IntToDec ->
@ -874,10 +874,10 @@ and disambiguate_match_and_build_expression
Desugared.Ast.expr Pos.marked Bindlib.box Scopelang.Ast.EnumConstructorMap.t
* Scopelang.Ast.EnumName.t =
let create_var = function
| None -> (ctxt, (Desugared.Ast.Var.make ("_", Pos.no_pos), Pos.no_pos))
| None -> ctxt, (Desugared.Ast.Var.make ("_", Pos.no_pos), Pos.no_pos)
| Some param ->
let ctxt, param_var = Name_resolution.add_def_local_var ctxt param in
(ctxt, (param_var, Pos.get_position param))
ctxt, (param_var, Pos.get_position param)
in
let bind_case_body
(c_uid : Dcalc.Ast.EnumConstructor.t)
@ -926,8 +926,8 @@ and disambiguate_match_and_build_expression
| Some e_case ->
Errors.raise_multispanned_error
[
(None, Pos.get_position case.match_case_expr);
(None, Pos.get_position (Bindlib.unbox e_case));
None, Pos.get_position case.match_case_expr;
None, Pos.get_position (Bindlib.unbox e_case);
]
"The constructor %a has been matched twice:"
Scopelang.Ast.EnumConstructor.format_t c_uid);
@ -935,9 +935,7 @@ and disambiguate_match_and_build_expression
let case_body =
translate_expr scope inside_definition_of ctxt case.Ast.match_case_expr
in
let e_binder =
Bindlib.bind_mvar (Array.of_list [ param_var ]) case_body
in
let e_binder = Bindlib.bind_mvar (Array.of_list [param_var]) case_body in
let case_expr =
bind_case_body c_uid e_uid ctxt param_pos case_body e_binder
in
@ -949,7 +947,7 @@ and disambiguate_match_and_build_expression
let raise_wildcard_not_last_case_err () =
Errors.raise_multispanned_error
[
(Some "Not ending wildcard:", case_pos);
Some "Not ending wildcard:", case_pos;
( Some "Next reachable case:",
curr_index + 1 |> List.nth cases |> Pos.get_position );
]
@ -995,7 +993,7 @@ and disambiguate_match_and_build_expression
translate_expr scope inside_definition_of ctxt match_case_expr
in
let e_binder =
Bindlib.bind_mvar (Array.of_list [ payload_var ]) case_body
Bindlib.bind_mvar (Array.of_list [payload_var]) case_body
in
(* For each missing cases, binds the wildcard payload. *)
@ -1015,7 +1013,7 @@ and disambiguate_match_and_build_expression
(Scopelang.Ast.EnumConstructorMap.empty, None, 0)
cases
in
(expr, Option.get e_name)
expr, Option.get e_name
[@@ocamlformat "wrap-comments=false"]
(** {1 Translating scope definitions} *)
@ -1027,7 +1025,7 @@ let merge_conditions
(precond : Desugared.Ast.expr Pos.marked Bindlib.box option)
(cond : Desugared.Ast.expr Pos.marked Bindlib.box option)
(default_pos : Pos.t) : Desugared.Ast.expr Pos.marked Bindlib.box =
match (precond, cond) with
match precond, cond with
| Some precond, Some cond ->
let op_term =
( Desugared.Ast.EOp (Dcalc.Ast.Binop Dcalc.Ast.And),
@ -1035,8 +1033,7 @@ let merge_conditions
in
Bindlib.box_apply2
(fun precond cond ->
( Desugared.Ast.EApp (op_term, [ precond; cond ]),
Pos.get_position precond ))
Desugared.Ast.EApp (op_term, [precond; cond]), Pos.get_position precond)
precond cond
| Some cond, None | None, Some cond -> cond
| None, None ->
@ -1068,7 +1065,7 @@ let process_default
(let def_key_typ =
Name_resolution.get_def_typ ctxt (Pos.unmark def_key)
in
match (Pos.unmark def_key_typ, param_uid) with
match Pos.unmark def_key_typ, param_uid with
| Scopelang.Ast.TArrow (t_in, _), Some param_uid ->
Some (Pos.unmark param_uid, t_in)
| Scopelang.Ast.TArrow _, None ->
@ -1108,10 +1105,10 @@ let process_def
(* We add to the name resolution context the name of the parameter variable *)
let param_uid, new_ctxt =
match def.definition_parameter with
| None -> (None, ctxt)
| None -> None, ctxt
| Some param ->
let ctxt, param_var = Name_resolution.add_def_local_var ctxt param in
(Some (Pos.same_pos_as param_var param), ctxt)
Some (Pos.same_pos_as param_var param), ctxt
in
let scope_updated =
let scope_def = Desugared.Ast.ScopeDefMap.find def_key scope.scope_defs in
@ -1119,7 +1116,7 @@ let process_def
let parent_rules =
match def.Ast.definition_exception_to with
| NotAnException ->
(Desugared.Ast.RuleSet.empty, Pos.get_position def.Ast.definition_name)
Desugared.Ast.RuleSet.empty, Pos.get_position def.Ast.definition_name
| UnlabeledException -> (
match scope_def_ctxt.default_exception_rulename with
(* This should have been caught previously by
@ -1127,7 +1124,7 @@ let process_def
| None | Some (Name_resolution.Ambiguous _) ->
assert false (* should not happen *)
| Some (Name_resolution.Unique (name, pos)) ->
(Desugared.Ast.RuleSet.singleton name, pos))
Desugared.Ast.RuleSet.singleton name, pos)
| ExceptionToLabel label -> (
try
let label_id =
@ -1275,8 +1272,8 @@ let check_unlabeled_exception
"This exception does not have a corresponding definition"
| Some (Ambiguous pos) ->
Errors.raise_multispanned_error
([ (Some "Ambiguous exception", Pos.get_position item) ]
@ List.map (fun p -> (Some "Candidate definition", p)) pos)
([Some "Ambiguous exception", Pos.get_position item]
@ List.map (fun p -> Some "Candidate definition", p) pos)
"This exception can refer to several definitions. Try using labels \
to disambiguate"
| Some (Unique _) -> ()))

View File

@ -22,7 +22,7 @@ let fill_pos_with_legislative_info (p : Ast.program) : Ast.program =
inherit [_] Ast.program_map as super
method! visit_marked f env x =
(f env (Pos.unmark x), Pos.overwrite_law_info (Pos.get_position x) env)
f env (Pos.unmark x), Pos.overwrite_law_info (Pos.get_position x) env
method! visit_LawHeading
(env : string list)

View File

@ -73,27 +73,27 @@ let raise_lexer_error (loc : Pos.t) (token : string) =
(English, French, etc.) *)
let token_list_language_agnostic : (string * token) list =
[
(".", DOT);
("<=", LESSER_EQUAL);
(">=", GREATER_EQUAL);
(">", GREATER);
("!=", NOT_EQUAL);
("=", EQUAL);
("(", LPAREN);
(")", RPAREN);
("{", LBRACKET);
("}", RBRACKET);
("{", LSQUARE);
("}", RSQUARE);
("+", PLUS);
("-", MINUS);
("*", MULT);
("/", DIV);
("|", VERTICAL);
(":", COLON);
(";", SEMICOLON);
("--", ALT);
("++", PLUSPLUS);
".", DOT;
"<=", LESSER_EQUAL;
">=", GREATER_EQUAL;
">", GREATER;
"!=", NOT_EQUAL;
"=", EQUAL;
"(", LPAREN;
")", RPAREN;
"{", LBRACKET;
"}", RBRACKET;
"{", LSQUARE;
"}", RSQUARE;
"+", PLUS;
"-", MINUS;
"*", MULT;
"/", DIV;
"|", VERTICAL;
":", COLON;
";", SEMICOLON;
"--", ALT;
"++", PLUSPLUS;
]
module type LocalisedLexer = sig

View File

@ -104,7 +104,7 @@ let raise_unsupported_feature (msg : string) (pos : Pos.t) =
let raise_unknown_identifier (msg : string) (ident : ident Pos.marked) =
Errors.raise_spanned_error (Pos.get_position ident)
"\"%s\": unknown identifier %s"
(Utils.Cli.with_style [ ANSITerminal.yellow ] "%s" (Pos.unmark ident))
(Utils.Cli.with_style [ANSITerminal.yellow] "%s" (Pos.unmark ident))
msg
(** Gets the type associated to an uid *)
@ -209,10 +209,10 @@ let process_subscope_decl
[
( Some "first use",
Pos.get_position (Scopelang.Ast.SubScopeName.get_info use) );
(Some "second use", s_pos);
Some "second use", s_pos;
]
"Subscope name \"%a\" already used"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
(Utils.Cli.format_with_style [ANSITerminal.yellow])
subscope
| None ->
let sub_scope_uid = Scopelang.Ast.SubScopeName.fresh (name, name_pos) in
@ -249,7 +249,7 @@ let rec process_base_typ
(ctxt : context)
((typ, typ_pos) : Ast.base_typ Pos.marked) : Scopelang.Ast.typ Pos.marked =
match typ with
| Ast.Condition -> (Scopelang.Ast.TLit TBool, typ_pos)
| Ast.Condition -> Scopelang.Ast.TLit TBool, typ_pos
| Ast.Data (Ast.Collection t) ->
( Scopelang.Ast.TArray
(Pos.unmark
@ -257,23 +257,23 @@ let rec process_base_typ
typ_pos )
| Ast.Data (Ast.Primitive prim) -> (
match prim with
| Ast.Integer -> (Scopelang.Ast.TLit TInt, typ_pos)
| Ast.Decimal -> (Scopelang.Ast.TLit TRat, typ_pos)
| Ast.Money -> (Scopelang.Ast.TLit TMoney, typ_pos)
| Ast.Duration -> (Scopelang.Ast.TLit TDuration, typ_pos)
| Ast.Date -> (Scopelang.Ast.TLit TDate, typ_pos)
| Ast.Boolean -> (Scopelang.Ast.TLit TBool, typ_pos)
| Ast.Integer -> Scopelang.Ast.TLit TInt, typ_pos
| Ast.Decimal -> Scopelang.Ast.TLit TRat, typ_pos
| Ast.Money -> Scopelang.Ast.TLit TMoney, typ_pos
| Ast.Duration -> Scopelang.Ast.TLit TDuration, typ_pos
| Ast.Date -> Scopelang.Ast.TLit TDate, typ_pos
| Ast.Boolean -> Scopelang.Ast.TLit TBool, typ_pos
| Ast.Text -> raise_unsupported_feature "text type" typ_pos
| Ast.Named ident -> (
match Desugared.Ast.IdentMap.find_opt ident ctxt.struct_idmap with
| Some s_uid -> (Scopelang.Ast.TStruct s_uid, typ_pos)
| Some s_uid -> Scopelang.Ast.TStruct s_uid, typ_pos
| None -> (
match Desugared.Ast.IdentMap.find_opt ident ctxt.enum_idmap with
| Some e_uid -> (Scopelang.Ast.TEnum e_uid, typ_pos)
| Some e_uid -> Scopelang.Ast.TEnum e_uid, typ_pos
| None ->
Errors.raise_spanned_error typ_pos
"Unknown type \"%a\", not a struct or enum previously declared"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
(Utils.Cli.format_with_style [ANSITerminal.yellow])
ident)))
(** Process a type (function or not) *)
@ -300,12 +300,11 @@ let process_data_decl
| Some use ->
Errors.raise_multispanned_error
[
( Some "first use",
Pos.get_position (Desugared.Ast.ScopeVar.get_info use) );
(Some "second use", pos);
Some "first use", Pos.get_position (Desugared.Ast.ScopeVar.get_info use);
Some "second use", pos;
]
"var name \"%a\" already used"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
(Utils.Cli.format_with_style [ANSITerminal.yellow])
name
| None ->
let uid = Desugared.Ast.ScopeVar.fresh (name, pos) in
@ -361,7 +360,7 @@ let add_def_local_var (ctxt : context) (name : ident Pos.marked) :
ctxt.local_var_idmap;
}
in
(ctxt, local_var_uid)
ctxt, local_var_uid
(** Process a scope declaration *)
let process_scope_decl (ctxt : context) (decl : Ast.scope_decl) : context =
@ -456,7 +455,7 @@ let process_enum_decl (ctxt : context) (edecl : Ast.enum_decl) : context =
(fun cases ->
let typ =
match cdecl.Ast.enum_decl_case_typ with
| None -> (Scopelang.Ast.TLit TUnit, cdecl_pos)
| None -> Scopelang.Ast.TLit TUnit, cdecl_pos
| Some typ -> process_type ctxt typ
in
match cases with
@ -474,11 +473,11 @@ let process_name_item (ctxt : context) (item : Ast.code_item Pos.marked) :
let raise_already_defined_error (use : Uid.MarkedString.info) name pos msg =
Errors.raise_multispanned_error
[
(Some "First definition:", Pos.get_position use);
(Some "Second definition:", pos);
Some "First definition:", Pos.get_position use;
Some "Second definition:", pos;
]
"%s name \"%a\" already defined" msg
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
(Utils.Cli.format_with_style [ANSITerminal.yellow])
name
in
match Pos.unmark item with
@ -579,7 +578,7 @@ let get_def_key
(default_pos : Pos.t) : Desugared.Ast.ScopeDef.t =
let scope_ctxt = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
match name with
| [ x ] ->
| [x] ->
let x_uid = get_var_uid scope_uid ctxt x in
let var_sig = Desugared.Ast.ScopeVarMap.find x_uid ctxt.var_typs in
Desugared.Ast.ScopeDef.Var
@ -593,7 +592,7 @@ let get_def_key
with Not_found ->
Errors.raise_multispanned_error
[
(None, Pos.get_position state);
None, Pos.get_position state;
( Some "Variable declaration:",
Pos.get_position (Desugared.Ast.ScopeVar.get_info x_uid) );
]
@ -604,7 +603,7 @@ let get_def_key
then
Errors.raise_multispanned_error
[
(None, Pos.get_position x);
None, Pos.get_position x;
( Some "Variable declaration:",
Pos.get_position (Desugared.Ast.ScopeVar.get_info x_uid) );
]
@ -612,7 +611,7 @@ let get_def_key
considered for variable %a."
Desugared.Ast.ScopeVar.format_t x_uid
else None )
| [ y; x ] ->
| [y; x] ->
let subscope_uid : Scopelang.Ast.SubScopeName.t =
get_subscope_uid scope_uid ctxt y
in
@ -717,11 +716,11 @@ let process_definition
default_exception_rulename =
Some
(Ambiguous
([ Pos.get_position d.definition_name ]
([Pos.get_position d.definition_name]
@
match old with
| Ambiguous old -> old
| Unique (_, pos) -> [ pos ]));
| Unique (_, pos) -> [pos]));
}
(* No definition has been set yet for this key *)
| None -> (
@ -734,7 +733,7 @@ let process_definition
default_exception_rulename =
Some
(Ambiguous
[ Pos.get_position d.definition_name ]);
[Pos.get_position d.definition_name]);
}
(* This is a possible default definition for this
key. We create and store a fresh rulename *)
@ -773,7 +772,7 @@ let process_scope_use (ctxt : context) (suse : Ast.scope_use) : context =
Errors.raise_spanned_error
(Pos.get_position suse.Ast.scope_use_name)
"\"%a\": this scope has not been declared anywhere, is it a typo?"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
(Utils.Cli.format_with_style [ANSITerminal.yellow])
(Pos.unmark suse.Ast.scope_use_name)
in
List.fold_left (process_scope_use_item s_name) ctxt suse.Ast.scope_use_items

View File

@ -65,7 +65,7 @@ let rec law_struct_list_to_tree (f : Ast.law_structure list) :
Ast.law_structure list =
match f with
| [] -> []
| [ item ] -> [ item ]
| [item] -> [item]
| first_item :: rest -> (
let rest_tree = law_struct_list_to_tree rest in
match rest_tree with
@ -83,22 +83,22 @@ let rec law_struct_list_to_tree (f : Ast.law_structure list) :
let rec split_rest_tree (rest_tree : Ast.law_structure list) :
Ast.law_structure list * Ast.law_structure list =
match rest_tree with
| [] -> ([], [])
| [] -> [], []
| LawHeading (new_heading, _) :: _
when new_heading.law_heading_precedence
<= heading.law_heading_precedence ->
(* we stop gobbling *)
([], rest_tree)
[], rest_tree
| first :: after ->
(* we continue gobbling *)
let after_gobbled, after_out = split_rest_tree after in
(first :: after_gobbled, after_out)
first :: after_gobbled, after_out
in
let gobbled, rest_out = split_rest_tree rest_tree in
LawHeading (heading, gobbled) :: rest_out))
(** Style with which to display syntax hints in the terminal output *)
let syntax_hints_style = [ ANSITerminal.yellow ]
let syntax_hints_style = [ANSITerminal.yellow]
(** Usage: [raise_parser_error error_loc last_good_loc token msg]
@ -116,7 +116,7 @@ let raise_parser_error
::
(match last_good_loc with
| None -> []
| Some last_good_loc -> [ (Some "Last good token:", last_good_loc) ]))
| Some last_good_loc -> [Some "Last good token:", last_good_loc]))
"Syntax error at token %a\n%s"
(Cli.format_with_style syntax_hints_style)
(Printf.sprintf "\"%s\"" token)
@ -158,7 +158,7 @@ module ParserAux (LocalisedLexer : Lexer_common.LocalisedLexer) = struct
(fst (lexing_positions lexbuf)))
token_list,
Some (I.positions last_input_needed) )
| None -> (token_list, None)
| None -> token_list, None
in
let similar_acceptable_tokens =
List.sort
@ -277,9 +277,9 @@ let rec parse_source_file
| FileName source_file -> (
try
let input = open_in source_file in
(Sedlexing.Utf8.from_channel input, Some input)
Sedlexing.Utf8.from_channel input, Some input
with Sys_error msg -> Errors.raise_error "%s" msg)
| Contents contents -> (Sedlexing.Utf8.from_string contents, None)
| Contents contents -> Sedlexing.Utf8.from_string contents, None
in
let source_file_name =
match source_file with FileName s -> s | Contents _ -> "stdin"
@ -323,9 +323,9 @@ and expand_includes
{
Ast.program_source_files = acc.Ast.program_source_files @ new_sources;
Ast.program_items =
acc.Ast.program_items @ [ Ast.LawHeading (heading, commands') ];
acc.Ast.program_items @ [Ast.LawHeading (heading, commands')];
}
| i -> { acc with Ast.program_items = acc.Ast.program_items @ [ i ] })
| i -> { acc with Ast.program_items = acc.Ast.program_items @ [i] })
{ Ast.program_source_files = []; Ast.program_items = [] }
commands

View File

@ -89,22 +89,21 @@ let file =
& info [] ~docv:"FILE" ~doc:"Catala master file to be compiled.")
let debug =
Arg.(value & flag & info [ "debug"; "d" ] ~doc:"Prints debug information.")
Arg.(value & flag & info ["debug"; "d"] ~doc:"Prints debug information.")
let unstyled =
Arg.(
value & flag
& info [ "unstyled"; "u" ]
& info ["unstyled"; "u"]
~doc:"Removes styling (colors, etc.) from terminal output.")
let optimize =
Arg.(
value & flag & info [ "optimize"; "O" ] ~doc:"Run compiler optimizations.")
Arg.(value & flag & info ["optimize"; "O"] ~doc:"Run compiler optimizations.")
let trace_opt =
Arg.(
value & flag
& info [ "trace"; "t" ]
& info ["trace"; "t"]
~doc:
"Displays a trace of the interpreter's computation or generates \
logging instructions in translate programs.")
@ -112,19 +111,19 @@ let trace_opt =
let avoid_exceptions =
Arg.(
value & flag
& info [ "avoid_exceptions" ]
& info ["avoid_exceptions"]
~doc:"Compiles the default calculus without exceptions")
let closure_conversion =
Arg.(
value & flag
& info [ "closure_conversion" ]
& info ["closure_conversion"]
~doc:"Performs closure conversion on the lambda calculus")
let wrap_weaved_output =
Arg.(
value & flag
& info [ "wrap"; "w" ]
& info ["wrap"; "w"]
~doc:"Wraps literate programming output with a minimal preamble.")
let backend =
@ -139,7 +138,7 @@ let language =
Arg.(
value
& opt (some string) None
& info [ "l"; "language" ] ~docv:"LANG"
& info ["l"; "language"] ~docv:"LANG"
~doc:"Input language among: en, fr, pl.")
let max_prec_digits_opt =
@ -147,7 +146,7 @@ let max_prec_digits_opt =
value
& opt (some int) None
& info
[ "p"; "max_digits_printed" ]
["p"; "max_digits_printed"]
~docv:"DIGITS"
~doc:
"Maximum number of significant digits printed for decimal results \
@ -157,7 +156,7 @@ let disable_counterexamples_opt =
Arg.(
value & flag
& info
[ "disable_counterexamples" ]
["disable_counterexamples"]
~doc:
"Disables the search for counterexamples in proof mode. Useful when \
you want a deterministic output from the Catala compiler, since \
@ -167,13 +166,13 @@ let ex_scope =
Arg.(
value
& opt (some string) None
& info [ "s"; "scope" ] ~docv:"SCOPE" ~doc:"Scope to be focused on.")
& info ["s"; "scope"] ~docv:"SCOPE" ~doc:"Scope to be focused on.")
let output =
Arg.(
value
& opt (some string) None
& info [ "output"; "o" ] ~docv:"OUTPUT"
& info ["output"; "o"] ~docv:"OUTPUT"
~doc:
"$(i, OUTPUT) is the file that will contain the output of the \
compiler. Defaults to $(i,FILE).$(i,EXT) where $(i,EXT) depends on \
@ -315,7 +314,7 @@ let info =
"Please file bug reports at https://github.com/CatalaLang/catala/issues";
]
in
let exits = Cmd.Exit.defaults @ [ Cmd.Exit.info ~doc:"on error." 1 ] in
let exits = Cmd.Exit.defaults @ [Cmd.Exit.info ~doc:"on error." 1] in
Cmd.info "catala" ~version ~doc ~exits ~man
(**{1 Terminal formatting}*)
@ -343,29 +342,28 @@ let time_marker () =
if delta > 50. then
Printf.printf "%s"
(with_style
[ ANSITerminal.Bold; ANSITerminal.black ]
[ANSITerminal.Bold; ANSITerminal.black]
"[TIME] %.0f ms\n" delta)
(** Prints [\[DEBUG\]] in purple on the terminal standard output *)
let debug_marker () =
time_marker ();
with_style [ ANSITerminal.Bold; ANSITerminal.magenta ] "[DEBUG] "
with_style [ANSITerminal.Bold; ANSITerminal.magenta] "[DEBUG] "
(** Prints [\[ERROR\]] in red on the terminal error output *)
let error_marker () =
with_style [ ANSITerminal.Bold; ANSITerminal.red ] "[ERROR] "
with_style [ANSITerminal.Bold; ANSITerminal.red] "[ERROR] "
(** Prints [\[WARNING\]] in yellow on the terminal standard output *)
let warning_marker () =
with_style [ ANSITerminal.Bold; ANSITerminal.yellow ] "[WARNING] "
with_style [ANSITerminal.Bold; ANSITerminal.yellow] "[WARNING] "
(** Prints [\[RESULT\]] in green on the terminal standard output *)
let result_marker () =
with_style [ ANSITerminal.Bold; ANSITerminal.green ] "[RESULT] "
with_style [ANSITerminal.Bold; ANSITerminal.green] "[RESULT] "
(** Prints [\[LOG\]] in red on the terminal error output *)
let log_marker () =
with_style [ ANSITerminal.Bold; ANSITerminal.black ] "[LOG] "
let log_marker () = with_style [ANSITerminal.Bold; ANSITerminal.black] "[LOG] "
(**{2 Printers}*)

View File

@ -39,7 +39,7 @@ let print_structured_error (msg : string) (pos : (string option * Pos.t) list) :
let raise_spanned_error ?(span_msg : string option) (span : Pos.t) format =
Format.kasprintf
(fun msg -> raise (StructuredError (msg, [ (span_msg, span) ])))
(fun msg -> raise (StructuredError (msg, [span_msg, span])))
format
let raise_multispanned_error (spans : (string option * Pos.t) list) format =
@ -56,6 +56,6 @@ let format_multispanned_warning (pos : (string option * Pos.t) list) format =
format
let format_spanned_warning ?(span_msg : string option) (span : Pos.t) format =
format_multispanned_warning [ (span_msg, span) ] format
format_multispanned_warning [span_msg, span] format
let format_warning format = format_multispanned_warning [] format

View File

@ -41,7 +41,7 @@ let from_info
Lexing.pos_bol = 1;
}
in
{ code_pos = (spos, epos); law_pos = [] }
{ code_pos = spos, epos; law_pos = [] }
let overwrite_law_info (pos : t) (law_pos : string list) : t =
{ pos with law_pos }
@ -92,7 +92,7 @@ let indent_number (s : string) : int =
let retrieve_loc_text (pos : t) : string =
try
let filename = get_file pos in
let blue_style = [ ANSITerminal.Bold; ANSITerminal.blue ] in
let blue_style = [ANSITerminal.Bold; ANSITerminal.blue] in
if filename = "" then "No position information"
else
let sline = get_start_line pos in
@ -108,17 +108,17 @@ let retrieve_loc_text (pos : t) : string =
Some l
| None -> None
in
(None, input_line_opt)
None, input_line_opt
else
let oc = open_in filename in
let input_line_opt () : string option =
try Some (input_line oc) with End_of_file -> None
in
(Some oc, input_line_opt)
Some oc, input_line_opt
in
let print_matched_line (line : string) (line_no : int) : string =
let line_indent = indent_number line in
let error_indicator_style = [ ANSITerminal.red; ANSITerminal.Bold ] in
let error_indicator_style = [ANSITerminal.red; ANSITerminal.Bold] in
line
^
if line_no >= sline && line_no <= eline then
@ -214,13 +214,13 @@ let no_pos : t =
Lexing.pos_bol = 0;
}
in
{ code_pos = (zero_pos, zero_pos); law_pos = [] }
{ code_pos = zero_pos, zero_pos; law_pos = [] }
let mark pos e : 'a marked = (e, pos)
let mark pos e : 'a marked = e, pos
let unmark ((x, _) : 'a marked) : 'a = x
let get_position ((_, x) : 'a marked) : t = x
let map_under_mark (f : 'a -> 'b) ((x, y) : 'a marked) : 'b marked = (f x, y)
let same_pos_as (x : 'a) ((_, y) : 'b marked) : 'a marked = (x, y)
let map_under_mark (f : 'a -> 'b) ((x, y) : 'a marked) : 'b marked = f x, y
let same_pos_as (x : 'a) ((_, y) : 'b marked) : 'a marked = x, y
let unmark_option (x : 'a marked option) : 'a option =
match x with Some x -> Some (unmark x) | None -> None

View File

@ -35,37 +35,35 @@ type ctx = {
let conjunction (args : vc_return list) (pos : Pos.t) : vc_return =
let acc, list =
match args with
| hd :: tl -> (hd, tl)
| [] -> (((ELit (LBool true), pos), VarMap.empty), [])
| hd :: tl -> hd, tl
| [] -> ((ELit (LBool true), pos), VarMap.empty), []
in
List.fold_left
(fun (acc, acc_ty) (arg, arg_ty) ->
( (EApp ((EOp (Binop And), pos), [ arg; acc ]), pos),
VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty
))
( (EApp ((EOp (Binop And), pos), [arg; acc]), pos),
VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty ))
acc list
let negation ((arg, arg_ty) : vc_return) (pos : Pos.t) : vc_return =
((EApp ((EOp (Unop Not), pos), [ arg ]), pos), arg_ty)
(EApp ((EOp (Unop Not), pos), [arg]), pos), arg_ty
let disjunction (args : vc_return list) (pos : Pos.t) : vc_return =
let acc, list =
match args with
| hd :: tl -> (hd, tl)
| [] -> (((ELit (LBool false), pos), VarMap.empty), [])
| hd :: tl -> hd, tl
| [] -> ((ELit (LBool false), pos), VarMap.empty), []
in
List.fold_left
(fun ((acc, acc_ty) : vc_return) (arg, arg_ty) ->
( (EApp ((EOp (Binop Or), pos), [ arg; acc ]), pos),
VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty
))
( (EApp ((EOp (Binop Or), pos), [arg; acc]), pos),
VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty ))
acc list
(** [half_product \[a1,...,an\] \[b1,...,bm\] returns \[(a1,b1),...(a1,bn),...(an,b1),...(an,bm)\]] *)
let half_product (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list =
l1
|> List.mapi (fun i ei ->
List.filteri (fun j _ -> i < j) l2 |> List.map (fun ej -> (ei, ej)))
List.filteri (fun j _ -> i < j) l2 |> List.map (fun ej -> ei, ej))
|> List.concat
(** This code skims through the topmost layers of the terms like this:
@ -78,14 +76,14 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Pos.marked) :
match Pos.unmark e with
| ErrorOnEmpty
( EDefault
( [ (EApp ((EVar (x, _), _), [ (ELit LUnit, _) ]), _) ],
( [(EApp ((EVar (x, _), _), [(ELit LUnit, _)]), _)],
(ELit (LBool true), _),
cons ),
_ )
when List.exists (fun x' -> Bindlib.eq_vars x x') ctx.input_vars ->
(* scope variables*)
cons
| EAbs ((binder, _), [ (TLit TUnit, _) ]) ->
| EAbs ((binder, _), [(TLit TUnit, _)]) ->
(* context sub-scope variables *)
let _, body = Bindlib.unmbind binder in
body
@ -134,7 +132,7 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Pos.marked) :
List.fold_left
(fun acc (var, ty) -> VarMap.add var ty acc)
vc_body_ty
(List.map2 (fun x y -> (x, y)) (Array.to_list vars) typs) )
(List.map2 (fun x y -> x, y) (Array.to_list vars) typs) )
| EApp (f, args) ->
(* We assume here that function calls never return empty error, which implies
all functions have been checked never to return empty errors. *)
@ -147,19 +145,19 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Pos.marked) :
let e3_vc, vc_typ3 = generate_vc_must_not_return_empty ctx e3 in
conjunction
[
(e1_vc, vc_typ1);
e1_vc, vc_typ1;
( (EIfThenElse (e1, e2_vc, e3_vc), Pos.get_position e),
VarMap.union
(fun _ _ _ -> failwith "should not happen")
vc_typ2 vc_typ3 );
]
(Pos.get_position e)
| ELit LEmptyError -> (Pos.same_pos_as (ELit (LBool false)) e, VarMap.empty)
| ELit LEmptyError -> Pos.same_pos_as (ELit (LBool false)) e, VarMap.empty
| EVar _
(* Per default calculus semantics, you cannot call a function with an argument
that evaluates to the empty error. Thus, all variable evaluate to non-empty-error terms. *)
| ELit _ | EOp _ ->
(Pos.same_pos_as (ELit (LBool true)) e, VarMap.empty)
Pos.same_pos_as (ELit (LBool true)) e, VarMap.empty
| EDefault (exceptions, just, cons) ->
(* <e1 ... en | ejust :- econs > never returns empty if and only if:
- first we look if e1 .. en ejust can return empty;
@ -226,7 +224,7 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : expr Pos.marked) :
List.fold_left
(fun acc (var, ty) -> VarMap.add var ty acc)
vc_body_ty
(List.map2 (fun x y -> (x, y)) (Array.to_list vars) typs) )
(List.map2 (fun x y -> x, y) (Array.to_list vars) typs) )
| EApp (f, args) ->
conjunction
(List.map (generate_vs_must_not_return_confict ctx) (f :: args))
@ -237,7 +235,7 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : expr Pos.marked) :
let e3_vc, vc_typ3 = generate_vs_must_not_return_confict ctx e3 in
conjunction
[
(e1_vc, vc_typ1);
e1_vc, vc_typ1;
( (EIfThenElse (e1, e2_vc, e3_vc), Pos.get_position e),
VarMap.union
(fun _ _ _ -> failwith "should not happen")
@ -245,7 +243,7 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : expr Pos.marked) :
]
(Pos.get_position e)
| EVar _ | ELit _ | EOp _ ->
(Pos.same_pos_as (ELit (LBool true)) e, VarMap.empty)
Pos.same_pos_as (ELit (LBool true)) e, VarMap.empty
| EDefault (exceptions, just, cons) ->
(* <e1 ... en | ejust :- econs > never returns conflict if and only if:
- neither e1 nor ... nor en nor ejust nor econs return conflict
@ -294,7 +292,7 @@ let rec generate_verification_conditions_scope_body_expr
(scope_body_expr : expr scope_body_expr) : ctx * verification_condition list
=
match scope_body_expr with
| Result _ -> (ctx, [])
| Result _ -> ctx, []
| ScopeLet scope_let ->
let scope_let_var, scope_let_next =
Bindlib.unbind scope_let.scope_let_next
@ -302,7 +300,7 @@ let rec generate_verification_conditions_scope_body_expr
let new_ctx, vc_list =
match scope_let.scope_let_kind with
| DestructuringInputStruct ->
({ ctx with input_vars = scope_let_var :: ctx.input_vars }, [])
{ ctx with input_vars = scope_let_var :: ctx.input_vars }, []
| ScopeVarDefinition | SubScopeVarDefinition ->
(* For scope variables, we should check both that they never evaluate to
emptyError nor conflictError. But for subscope variable definitions,
@ -329,7 +327,7 @@ let rec generate_verification_conditions_scope_body_expr
(fun _ _ -> failwith "should not happen")
ctx.scope_variables_typs vc_confl_typs;
vc_scope = ctx.current_scope_name;
vc_variable = (scope_let_var, scope_let.scope_let_pos);
vc_variable = scope_let_var, scope_let.scope_let_pos;
};
]
in
@ -352,13 +350,13 @@ let rec generate_verification_conditions_scope_body_expr
(fun _ _ -> failwith "should not happen")
ctx.scope_variables_typs vc_empty_typs;
vc_scope = ctx.current_scope_name;
vc_variable = (scope_let_var, scope_let.scope_let_pos);
vc_variable = scope_let_var, scope_let.scope_let_pos;
}
:: vc_list
| _ -> vc_list
in
(ctx, vc_list)
| _ -> (ctx, [])
ctx, vc_list
| _ -> ctx, []
in
let new_ctx, new_vcs =
generate_verification_conditions_scope_body_expr
@ -370,7 +368,7 @@ let rec generate_verification_conditions_scope_body_expr
}
scope_let_next
in
(new_ctx, vc_list @ new_vcs)
new_ctx, vc_list @ new_vcs
let rec generate_verification_conditions_scopes
(decl_ctx : decl_ctx)

View File

@ -97,12 +97,12 @@ module MakeBackendIO (B : Backend) = struct
match vc.Conditions.vc_kind with
| Conditions.NoEmptyError ->
Format.asprintf "%s This variable never returns an empty error"
(Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
| Conditions.NoOverlappingExceptions ->
Format.asprintf "%s No two exceptions to ever overlap for this variable"
(Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
@ -114,14 +114,14 @@ module MakeBackendIO (B : Backend) = struct
match vc.Conditions.vc_kind with
| Conditions.NoEmptyError ->
Format.asprintf "%s This variable might return an empty error:\n%s"
(Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
(Pos.retrieve_loc_text (Pos.get_position vc.vc_variable))
| Conditions.NoOverlappingExceptions ->
Format.asprintf
"%s At least two exceptions overlap for this variable:\n%s"
(Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
(Pos.retrieve_loc_text (Pos.get_position vc.vc_variable))
@ -161,7 +161,7 @@ module MakeBackendIO (B : Backend) = struct
Cli.debug_print "For this variable:\n%s\n"
(Pos.retrieve_loc_text (Pos.get_position vc.Conditions.vc_guard));
Cli.debug_format "This verification condition was generated for %a:@\n%a"
(Cli.format_with_style [ ANSITerminal.yellow ])
(Cli.format_with_style [ANSITerminal.yellow])
(match vc.vc_kind with
| Conditions.NoEmptyError ->
"the variable definition never to return an empty error"
@ -180,7 +180,7 @@ module MakeBackendIO (B : Backend) = struct
| Unknown -> failwith "The solver failed at proving or disproving the VC")
| Fail msg ->
Cli.error_print "%s The translation to Z3 failed:\n%s"
(Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
msg

View File

@ -222,8 +222,8 @@ let print_model (ctx : context) (model : Model.model) : string =
let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
let v = StringMap.find symbol_name ctx.ctx_z3vars in
Format.fprintf fmt "%s %s : %s"
(Cli.with_style [ ANSITerminal.blue ] "%s" "-->")
(Cli.with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
(Cli.with_style [ANSITerminal.blue] "%s" "-->")
(Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v))
(print_z3model_expr ctx (VarMap.find v ctx.ctx_var) e)
else
(* Declaration d is a function *)
@ -237,8 +237,8 @@ let print_model (ctx : context) (model : Model.model) : string =
let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
let v = StringMap.find symbol_name ctx.ctx_z3vars in
Format.fprintf fmt "%s %s : %s"
(Cli.with_style [ ANSITerminal.blue ] "%s" "-->")
(Cli.with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
(Cli.with_style [ANSITerminal.blue] "%s" "-->")
(Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v))
(* TODO: Model of a Z3 function should be pretty-printed *)
(Model.FuncInterp.to_string f)))
decls
@ -260,7 +260,7 @@ let translate_typ_lit (ctx : context) (t : typ_lit) : Sort.sort =
(** [translate_typ] returns the Z3 sort correponding to the Catala type [t] **)
let rec translate_typ (ctx : context) (t : typ) : context * Sort.sort =
match t with
| TLit t -> (ctx, translate_typ_lit ctx t)
| TLit t -> ctx, translate_typ_lit ctx t
| TTuple (_, Some name) -> find_or_create_struct ctx name
| TTuple (_, None) ->
failwith "[Z3 encoding] TTuple type of unnamed struct not supported"
@ -269,7 +269,7 @@ let rec translate_typ (ctx : context) (t : typ) : context * Sort.sort =
| TArray _ ->
(* For now, we are only encoding the (symbolic) length of an array.
Ultimately, the type of an array should also contain its elements *)
(ctx, Arithmetic.Integer.mk_sort ctx.ctx_z3)
ctx, Arithmetic.Integer.mk_sort ctx.ctx_z3
| TAny -> failwith "[Z3 encoding] TAny type not supported"
(** [find_or_create_enum] attempts to retrieve the Z3 sort corresponding to the
@ -300,14 +300,14 @@ and find_or_create_enum (ctx : context) (enum : EnumName.t) :
(* We need a name for the argument of the constructor, we arbitrary pick
the name of the constructor to which we append the special character
"!" and the integer 0 *)
[ Symbol.mk_string ctx.ctx_z3 (name ^ "!0") ]
[Symbol.mk_string ctx.ctx_z3 (name ^ "!0")]
(* The type of the argument, translated to a Z3 sort *)
[ Some arg_z3_ty ]
[ Sort.get_id arg_z3_ty ] )
[Some arg_z3_ty]
[Sort.get_id arg_z3_ty] )
in
match EnumMap.find_opt enum ctx.ctx_z3datatypes with
| Some e -> (ctx, e)
| Some e -> ctx, e
| None ->
let ctrs = EnumMap.find enum ctx.ctx_decl.ctx_enums in
let ctx, z3_ctrs = List.fold_left_map create_constructor ctx ctrs in
@ -316,7 +316,7 @@ and find_or_create_enum (ctx : context) (enum : EnumName.t) :
(Pos.unmark (EnumName.get_info enum))
z3_ctrs
in
(add_z3enum enum z3_enum ctx, z3_enum)
add_z3enum enum z3_enum ctx, z3_enum
(** [find_or_create_struct] attemps to retrieve the Z3 sort corresponding to the
struct [s]. If no such sort exists yet, we construct it as a datatype with
@ -325,7 +325,7 @@ and find_or_create_enum (ctx : context) (enum : EnumName.t) :
and find_or_create_struct (ctx : context) (s : StructName.t) :
context * Sort.sort =
match StructMap.find_opt s ctx.ctx_z3structs with
| Some s -> (ctx, s)
| Some s -> ctx, s
| None ->
let s_name = Pos.unmark (StructName.get_info s) in
let fields = StructMap.find s ctx.ctx_decl.ctx_structs in
@ -351,8 +351,8 @@ and find_or_create_struct (ctx : context) (s : StructName.t) :
z3_sortrefs
in
let z3_struct = Datatype.mk_sort_s ctx.ctx_z3 s_name [ z3_mk_struct ] in
(add_z3struct s z3_struct ctx, z3_struct)
let z3_struct = Datatype.mk_sort_s ctx.ctx_z3 s_name [z3_mk_struct] in
add_z3struct s z3_struct ctx, z3_struct
(** [translate_lit] returns the Z3 expression as a literal corresponding to
[lit] **)
@ -388,7 +388,7 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr =
let find_or_create_funcdecl (ctx : context) (v : Var.t) :
context * FuncDecl.func_decl =
match VarMap.find_opt v ctx.ctx_funcdecl with
| Some fd -> (ctx, fd)
| Some fd -> ctx, fd
| None -> (
(* Retrieves the Catala type of the function [v] *)
let f_ty = VarMap.find v ctx.ctx_var in
@ -397,10 +397,10 @@ let find_or_create_funcdecl (ctx : context) (v : Var.t) :
let ctx, z3_t1 = translate_typ ctx (Pos.unmark t1) in
let ctx, z3_t2 = translate_typ ctx (Pos.unmark t2) in
let name = unique_name v in
let fd = FuncDecl.mk_func_decl_s ctx.ctx_z3 name [ z3_t1 ] z3_t2 in
let fd = FuncDecl.mk_func_decl_s ctx.ctx_z3 name [z3_t1] z3_t2 in
let ctx = add_funcdecl v fd ctx in
let ctx = add_z3var name v ctx in
(ctx, fd)
ctx, fd
| TAny ->
failwith
"[Z3 Encoding] A function being applied has type TAny, the type was \
@ -420,7 +420,7 @@ let rec translate_op
| Ternop _top ->
let _e1, _e2, _e3 =
match args with
| [ e1; e2; e3 ] -> (e1, e2, e3)
| [e1; e2; e3] -> e1, e2, e3
| _ ->
failwith
(Format.asprintf
@ -432,9 +432,9 @@ let rec translate_op
failwith "[Z3 encoding] ternary operator application not supported"
| Binop bop -> (
(* Special case for GetYear comparisons *)
match (bop, args) with
| ( Lt KInt,
[ (EApp ((EOp (Unop GetYear), _), [ e1 ]), _); (ELit (LInt n), _) ] ) ->
match bop, args with
| Lt KInt, [(EApp ((EOp (Unop GetYear), _), [e1]), _); (ELit (LInt n), _)]
->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let e2 =
@ -444,9 +444,9 @@ let rec translate_op
(* e2 corresponds to the first day of the year n. GetYear e1 < e2 can thus
be directly translated as < in the Z3 encoding using the number of
days *)
(ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2)
| ( Lte KInt,
[ (EApp ((EOp (Unop GetYear), _), [ e1 ]), _); (ELit (LInt n), _) ] ) ->
ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2
| Lte KInt, [(EApp ((EOp (Unop GetYear), _), [e1]), _); (ELit (LInt n), _)]
->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let nb_days = if CalendarLib.Date.is_leap_year n then 365 else 364 in
@ -458,9 +458,9 @@ let rec translate_op
Arithmetic.Integer.mk_numeral_i ctx.ctx_z3
(date_to_int (date_of_year n) + nb_days)
in
(ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2)
| ( Gt KInt,
[ (EApp ((EOp (Unop GetYear), _), [ e1 ]), _); (ELit (LInt n), _) ] ) ->
ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2
| Gt KInt, [(EApp ((EOp (Unop GetYear), _), [e1]), _); (ELit (LInt n), _)]
->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let nb_days = if CalendarLib.Date.is_leap_year n then 365 else 364 in
@ -472,9 +472,9 @@ let rec translate_op
Arithmetic.Integer.mk_numeral_i ctx.ctx_z3
(date_to_int (date_of_year n) + nb_days)
in
(ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2)
| ( Gte KInt,
[ (EApp ((EOp (Unop GetYear), _), [ e1 ]), _); (ELit (LInt n), _) ] ) ->
ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2
| Gte KInt, [(EApp ((EOp (Unop GetYear), _), [e1]), _); (ELit (LInt n), _)]
->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let e2 =
@ -484,8 +484,8 @@ let rec translate_op
(* e2 corresponds to the first day of the year n. GetYear e1 >= e2 can
thus be directly translated as >= in the Z3 encoding using the number
of days *)
(ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2)
| Eq, [ (EApp ((EOp (Unop GetYear), _), [ e1 ]), _); (ELit (LInt n), _) ] ->
ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2
| Eq, [(EApp ((EOp (Unop GetYear), _), [e1]), _); (ELit (LInt n), _)] ->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let min_date =
@ -505,10 +505,10 @@ let rec translate_op
| _ -> (
let ctx, e1, e2 =
match args with
| [ e1; e2 ] ->
| [e1; e2] ->
let ctx, e1 = translate_expr ctx e1 in
let ctx, e2 = translate_expr ctx e2 in
(ctx, e1, e2)
ctx, e1, e2
| _ ->
failwith
(Format.asprintf
@ -518,31 +518,31 @@ let rec translate_op
in
match bop with
| And -> (ctx, Boolean.mk_and ctx.ctx_z3 [ e1; e2 ])
| Or -> (ctx, Boolean.mk_or ctx.ctx_z3 [ e1; e2 ])
| Xor -> (ctx, Boolean.mk_xor ctx.ctx_z3 e1 e2)
| And -> ctx, Boolean.mk_and ctx.ctx_z3 [e1; e2]
| Or -> ctx, Boolean.mk_or ctx.ctx_z3 [e1; e2]
| Xor -> ctx, Boolean.mk_xor ctx.ctx_z3 e1 e2
| Add KInt | Add KRat | Add KMoney | Add KDate | Add KDuration ->
(ctx, Arithmetic.mk_add ctx.ctx_z3 [ e1; e2 ])
ctx, Arithmetic.mk_add ctx.ctx_z3 [e1; e2]
| Sub KInt | Sub KRat | Sub KMoney | Sub KDate | Sub KDuration ->
(ctx, Arithmetic.mk_sub ctx.ctx_z3 [ e1; e2 ])
ctx, Arithmetic.mk_sub ctx.ctx_z3 [e1; e2]
| Mult KInt | Mult KRat | Mult KMoney | Mult KDate | Mult KDuration ->
(ctx, Arithmetic.mk_mul ctx.ctx_z3 [ e1; e2 ])
ctx, Arithmetic.mk_mul ctx.ctx_z3 [e1; e2]
| Div KInt | Div KRat | Div KMoney ->
(ctx, Arithmetic.mk_div ctx.ctx_z3 e1 e2)
ctx, Arithmetic.mk_div ctx.ctx_z3 e1 e2
| Div _ ->
failwith
"[Z3 encoding] application of non-integer binary operator Div not \
supported"
| Lt KInt | Lt KRat | Lt KMoney | Lt KDate | Lt KDuration ->
(ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2)
ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2
| Lte KInt | Lte KRat | Lte KMoney | Lte KDate | Lte KDuration ->
(ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2)
ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2
| Gt KInt | Gt KRat | Gt KMoney | Gt KDate | Gt KDuration ->
(ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2)
ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2
| Gte KInt | Gte KRat | Gte KMoney | Gte KDate | Gte KDuration ->
(ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2)
| Eq -> (ctx, Boolean.mk_eq ctx.ctx_z3 e1 e2)
| Neq -> (ctx, Boolean.mk_not ctx.ctx_z3 (Boolean.mk_eq ctx.ctx_z3 e1 e2))
ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2
| Eq -> ctx, Boolean.mk_eq ctx.ctx_z3 e1 e2
| Neq -> ctx, Boolean.mk_not ctx.ctx_z3 (Boolean.mk_eq ctx.ctx_z3 e1 e2)
| Map ->
failwith
"[Z3 encoding] application of binary operator Map not supported"
@ -555,7 +555,7 @@ let rec translate_op
| Unop uop -> (
let ctx, e1 =
match args with
| [ e1 ] -> translate_expr ctx e1
| [e1] -> translate_expr ctx e1
| _ ->
failwith
(Format.asprintf
@ -565,14 +565,14 @@ let rec translate_op
in
match uop with
| Not -> (ctx, Boolean.mk_not ctx.ctx_z3 e1)
| Not -> ctx, Boolean.mk_not ctx.ctx_z3 e1
| Minus _ ->
failwith "[Z3 encoding] application of unary operator Minus not supported"
(* Omitting the log from the VC *)
| Log _ -> (ctx, e1)
| Log _ -> ctx, e1
| Length ->
(* For now, an array is only its symbolic length. We simply return it *)
(ctx, e1)
ctx, e1
| IntToRat ->
failwith
"[Z3 encoding] application of unary operator IntToRat not supported"
@ -608,7 +608,7 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr
(* Invariant: Catala enums always have exactly one argument *)
let accessor = List.hd accessors in
let proj = Expr.mk_app ctx.ctx_z3 accessor [ head ] in
let proj = Expr.mk_app ctx.ctx_z3 accessor [head] in
(* The fresh variable should be substituted by a projection into the enum
in the body, we add this to the context *)
let ctx = add_z3matchsubst fresh_v proj ctx in
@ -642,12 +642,12 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr
| _ -> ctx
in
(ctx, z3_var)
ctx, z3_var
| Some e ->
(* This variable is a temporary variable generated during VC translation
of a match. It actually corresponds to applying an accessor to an enum,
the corresponding Z3 expression was previously stored in the context *)
(ctx, e))
ctx, e)
| ETuple _ -> failwith "[Z3 encoding] ETuple unsupported"
| ETupleAccess (s, idx, oname, _tys) ->
let name =
@ -663,7 +663,7 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr
let accessors = List.hd (Datatype.get_accessors z3_struct) in
let accessor = List.nth accessors idx in
let ctx, s = translate_expr ctx s in
(ctx, Expr.mk_app ctx.ctx_z3 accessor [ s ])
ctx, Expr.mk_app ctx.ctx_z3 accessor [s]
| EInj (e, idx, en, _tys) ->
(* This node corresponds to creating a value for the enumeration [en], by
calling the [idx]-th constructor of enum [en], with argument [e] *)
@ -672,7 +672,7 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr
let ctrs = Datatype.get_constructors z3_enum in
(* This should always succeed if the expression is well-typed in dcalc *)
let ctr = List.nth ctrs idx in
(ctx, Expr.mk_app ctx.ctx_z3 ctr [ z3_arg ])
ctx, Expr.mk_app ctx.ctx_z3 ctr [z3_arg]
| EMatch (arg, arms, enum) ->
let ctx, z3_enum = find_or_create_enum ctx enum in
let ctx, z3_arg = translate_expr ctx arg in
@ -686,14 +686,14 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr
List.map2
(fun r arm ->
(* Encodes A? arg ==> body *)
let is_r = Expr.mk_app ctx.ctx_z3 r [ z3_arg ] in
let is_r = Expr.mk_app ctx.ctx_z3 r [z3_arg] in
Boolean.mk_implies ctx.ctx_z3 is_r arm)
(Datatype.get_recognizers z3_enum)
z3_arms
in
(ctx, Boolean.mk_and ctx.ctx_z3 z3_arms)
ctx, Boolean.mk_and ctx.ctx_z3 z3_arms
| EArray _ -> failwith "[Z3 encoding] EArray unsupported"
| ELit l -> (ctx, translate_lit ctx l)
| ELit l -> ctx, translate_lit ctx l
| EAbs _ -> failwith "[Z3 encoding] EAbs unsupported"
| EApp (head, args) -> (
match Pos.unmark head with
@ -706,10 +706,10 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr
List.fold_right
(fun arg (ctx, acc) ->
let ctx, z3_arg = translate_expr ctx arg in
(ctx, z3_arg :: acc))
ctx, z3_arg :: acc)
args (ctx, [])
in
(ctx, Expr.mk_app ctx.ctx_z3 fd z3_args)
ctx, Expr.mk_app ctx.ctx_z3 fd z3_args
| _ ->
failwith
"[Z3 encoding] EApp node: Catala function calls should only include \
@ -739,7 +739,7 @@ let create_z3unit (ctx : Z3.context) : Z3.context * (Sort.sort * Expr.expr) =
let unit_sort = Tuple.mk_sort ctx (Symbol.mk_string ctx "unit") [] [] in
let mk_unit = Tuple.get_mk_decl unit_sort in
let unit_val = Expr.mk_app ctx mk_unit [] in
(ctx, (unit_sort, unit_val))
ctx, (unit_sort, unit_val)
module Backend = struct
type backend_context = context
@ -779,8 +779,8 @@ module Backend = struct
(decl_ctx : decl_ctx)
(free_vars_typ : typ Pos.marked VarMap.t) : backend_context =
let cfg =
(if !Cli.disable_counterexamples then [] else [ ("model", "true") ])
@ [ ("proof", "false") ]
(if !Cli.disable_counterexamples then [] else ["model", "true"])
@ ["proof", "false"]
in
let z3_ctx = mk_context cfg in
let z3_ctx, z3unit = create_z3unit z3_ctx in

File diff suppressed because it is too large Load Diff

View File

@ -4,13 +4,13 @@ let try_test msg test =
try
test ();
Format.printf "%s %s\n"
(ANSITerminal.sprintf [ ANSITerminal.green ] "PASS")
(ANSITerminal.sprintf [ ANSITerminal.magenta ] msg)
(ANSITerminal.sprintf [ANSITerminal.green] "PASS")
(ANSITerminal.sprintf [ANSITerminal.magenta] msg)
with Runtime.AssertionFailed ->
failure := true;
Format.printf "%s %s\n"
(ANSITerminal.sprintf [ ANSITerminal.red ] "FAIL")
(ANSITerminal.sprintf [ ANSITerminal.magenta ] msg)
(ANSITerminal.sprintf [ANSITerminal.red] "FAIL")
(ANSITerminal.sprintf [ANSITerminal.magenta] msg)
let _ =
try_test "Allocations familiales #1" Tests_allocations_familiales.test1;