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

Merge branch 'master' into allocations_logement

Browse Source
This commit is contained in:
Denis Merigoux 2022-05-05 14:27:48 +02:00
commit a72944a3ec
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
30 changed files with 3256 additions and 2680 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Makefile
View File

@ -243,7 +243,7 @@ run_french_law_library_benchmark_python: type_french_law_library_python
##########################################
CATALA_OPTS?=
CLERK_OPTS?=
CLERK_OPTS?=--makeflags="$(MAKEFLAGS)"
CATALA_BIN=_build/default/compiler/catala.exe
CLERK_BIN=_build/default/build_system/clerk.exe
@ -255,10 +255,10 @@ CLERK=$(CLERK_BIN) --exe $(CATALA_BIN) \
.FORCE:
test_suite: .FORCE
@$(CLERK) test tests
$(CLERK) test tests
test_examples: .FORCE
@$(CLERK) test examples
$(CLERK) test examples
test_clerk: .FORCE
cd $(BUILD_SYSTEM_DIR) && dune test

34
build_system/clerk_driver.ml
View File

@ -70,6 +70,15 @@ let scope =
"Used with the `run` command, selects which scope of a given Catala \
file to run.")
let makeflags =
Arg.(
value
& opt (some string) None
& 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.")
let catala_opts =
Arg.(
value
@ -79,8 +88,8 @@ let catala_opts =
let clerk_t f =
Term.(
const f $ files_or_folders $ command $ catalac $ catala_opts $ debug $ scope
$ reset_test_outputs $ ninja_output)
const f $ files_or_folders $ command $ catalac $ catala_opts $ makeflags
$ debug $ scope $ reset_test_outputs $ ninja_output)
let version = "0.5.0"
@ -701,16 +710,35 @@ let add_test_builds
else collect_in_file ctx file_or_folder curr_ninja reset_test_outputs)
ctx
let makeflags_to_ninja_flags (makeflags : string option) =
match makeflags with
| None -> ""
| 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 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;
]
let driver
(files_or_folders : string list)
(command : string)
(catala_exe : string option)
(catala_opts : string option)
(makeflags : string option)
(debug : bool)
(scope : string option)
(reset_test_outputs : bool)
(ninja_output : string option) : int =
if debug then Cli.debug_flag := true;
let ninja_flags = makeflags_to_ninja_flags makeflags in
let files_or_folders = List.sort_uniq String.compare files_or_folders
and catala_exe = Option.fold ~none:"catala" ~some:Fun.id catala_exe
and catala_opts = Option.fold ~none:"" ~some:Fun.id catala_opts
@ -750,7 +778,7 @@ let driver
(Format.formatter_of_out_channel out)
(add_root_test_build ninja ctx.all_file_names ctx.all_test_builds);
close_out out;
let ninja_cmd = "ninja test -f " ^ ninja_output in
let ninja_cmd = "ninja " ^ ninja_flags ^ " test -f " ^ ninja_output in
Cli.debug_print "executing '%s'..." ninja_cmd;
Sys.command ninja_cmd
with Sys_error e ->

376
compiler/dcalc/ast.ml
View File

@ -134,49 +134,259 @@ type scope_let_kind =
| DestructuringSubScopeResults
| Assertion
type scope_let = {
type 'expr scope_let = {
scope_let_kind : scope_let_kind;
scope_let_typ : typ Utils.Pos.marked;
scope_let_expr : expr Utils.Pos.marked;
scope_let_next : (expr, scope_body_expr) Bindlib.binder;
scope_let_expr : 'expr Utils.Pos.marked;
scope_let_next : ('expr, 'expr scope_body_expr) Bindlib.binder;
scope_let_pos : Utils.Pos.t;
}
and scope_body_expr = Result of expr Utils.Pos.marked | ScopeLet of scope_let
and 'expr scope_body_expr =
| Result of 'expr Utils.Pos.marked
| ScopeLet of 'expr scope_let
type scope_body = {
type 'expr scope_body = {
scope_body_input_struct : StructName.t;
scope_body_output_struct : StructName.t;
scope_body_expr : (expr, scope_body_expr) Bindlib.binder;
scope_body_expr : ('expr, 'expr scope_body_expr) Bindlib.binder;
}
type scope_def = {
type 'expr scope_def = {
scope_name : ScopeName.t;
scope_body : scope_body;
scope_next : (expr, scopes) Bindlib.binder;
scope_body : 'expr scope_body;
scope_next : ('expr, 'expr scopes) Bindlib.binder;
}
and scopes = Nil | ScopeDef of scope_def
and 'expr scopes = Nil | ScopeDef of 'expr scope_def
type program = { decl_ctx : decl_ctx; scopes : scopes }
type program = { decl_ctx : decl_ctx; scopes : expr scopes }
let rec fold_scope_lets
~(f : 'a -> scope_let -> 'a)
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)
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)
let etupleaccess
(e1 : expr Pos.marked Bindlib.box)
(i : int)
(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
let einj
(e1 : expr Pos.marked Bindlib.box)
(i : int)
(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
let ematch
(arg : expr Pos.marked Bindlib.box)
(arms : expr Pos.marked Bindlib.box list)
(e_name : EnumName.t)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(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)
let elit (l : lit) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (ELit l, pos)
let eabs
(binder : (expr, expr Pos.marked) Bindlib.mbinder Bindlib.box)
(pos_binder : Pos.t)
(typs : typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun binder -> (EAbs ((binder, pos_binder), typs), pos))
binder
let eapp
(e1 : expr Pos.marked Bindlib.box)
(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))
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
let eop (op : operator) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (EOp op, pos)
let edefault
(excepts : expr Pos.marked Bindlib.box list)
(just : expr Pos.marked Bindlib.box)
(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))
(Bindlib.box_list excepts) just cons
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
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
let map_expr
(ctx : 'a)
~(f : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box)
(e : expr Pos.marked) : expr Pos.marked Bindlib.box =
match Pos.unmark e with
| EVar (v, _pos) -> evar v (Pos.get_position e)
| EApp (e1, args) ->
eapp (f ctx e1) (List.map (f ctx) args) (Pos.get_position e)
| EAbs ((binder, binder_pos), typs) ->
eabs
(Bindlib.box_mbinder (f ctx) binder)
binder_pos typs (Pos.get_position e)
| ETuple (args, s) -> etuple (List.map (f ctx) args) s (Pos.get_position e)
| ETupleAccess (e1, n, s_name, typs) ->
etupleaccess ((f ctx) e1) n s_name typs (Pos.get_position e)
| EInj (e1, i, e_name, typs) ->
einj ((f ctx) e1) i e_name typs (Pos.get_position e)
| EMatch (arg, arms, e_name) ->
ematch ((f ctx) arg) (List.map (f ctx) arms) e_name (Pos.get_position e)
| EArray args -> earray (List.map (f ctx) args) (Pos.get_position e)
| ELit l -> elit l (Pos.get_position e)
| EAssert e1 -> eassert ((f ctx) e1) (Pos.get_position e)
| EOp op -> Bindlib.box (EOp op, Pos.get_position e)
| EDefault (excepts, just, cons) ->
edefault
(List.map (f ctx) excepts)
((f ctx) just)
((f ctx) cons)
(Pos.get_position e)
| EIfThenElse (e1, e2, e3) ->
eifthenelse ((f ctx) e1) ((f ctx) e2) ((f ctx) e3) (Pos.get_position e)
| ErrorOnEmpty e1 -> eerroronempty ((f ctx) e1) (Pos.get_position e)
(** See [Bindlib.box_term] documentation for why we are doing that. *)
let box_expr (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let rec id_t () e = map_expr () ~f:id_t e in
id_t () e
type 'expr box_expr_sig = 'expr Pos.marked -> 'expr Pos.marked Bindlib.box
let rec fold_left_scope_lets
~(f : 'a -> 'expr scope_let -> 'expr Bindlib.var -> 'a)
~(init : 'a)
(scope_body_expr : scope_body_expr) : 'a =
(scope_body_expr : 'expr scope_body_expr) : 'a =
match scope_body_expr with
| Result _ -> init
| ScopeLet scope_let ->
let _, next = Bindlib.unbind scope_let.scope_let_next in
fold_scope_lets ~f ~init:(f init scope_let) next
let var, next = Bindlib.unbind scope_let.scope_let_next in
fold_left_scope_lets ~f ~init:(f init scope_let var) next
let rec fold_scope_defs
~(f : 'a -> scope_def -> 'a) ~(init : 'a) (scopes : scopes) : 'a =
let rec fold_right_scope_lets
~(f : 'expr scope_let -> 'expr Bindlib.var -> 'a -> 'a)
~(init : 'expr Pos.marked -> 'a)
(scope_body_expr : 'expr scope_body_expr) : 'a =
match scope_body_expr with
| Result result -> init result
| ScopeLet scope_let ->
let var, next = Bindlib.unbind scope_let.scope_let_next in
let next_result = fold_right_scope_lets ~f ~init next in
f scope_let var next_result
let map_exprs_in_scope_lets
~(f : 'expr Pos.marked -> 'expr Pos.marked Bindlib.box)
(scope_body_expr : 'expr scope_body_expr) :
'expr scope_body_expr Bindlib.box =
fold_right_scope_lets
~f:(fun scope_let var_next (acc : 'expr scope_body_expr Bindlib.box) ->
let new_scope_let =
Bindlib.box_apply
(fun new_expr -> { scope_let with scope_let_expr = new_expr })
(f scope_let.scope_let_expr)
in
let new_next = Bindlib.bind_var var_next acc in
Bindlib.box_apply2
(fun new_next new_scope_let ->
ScopeLet { new_scope_let with scope_let_next = new_next })
new_next new_scope_let)
~init:(fun res -> Bindlib.box_apply (fun res -> Result res) (f res))
scope_body_expr
let rec fold_left_scope_defs
~(f : 'a -> 'expr scope_def -> 'expr Bindlib.var -> 'a)
~(init : 'a)
(scopes : 'expr scopes) : 'a =
match scopes with
| Nil -> init
| ScopeDef scope_def ->
let _, next = Bindlib.unbind scope_def.scope_next in
fold_scope_defs ~f ~init:(f init scope_def) next
let var, next = Bindlib.unbind scope_def.scope_next in
fold_left_scope_defs ~f ~init:(f init scope_def var) next
let rec fold_right_scope_defs
~(f : 'expr scope_def -> 'expr Bindlib.var -> 'a -> 'a)
~(init : 'a)
(scopes : 'expr scopes) : 'a =
match scopes with
| Nil -> init
| ScopeDef scope_def ->
let var_next, next = Bindlib.unbind scope_def.scope_next in
let result_next = fold_right_scope_defs ~f ~init next in
f scope_def var_next result_next
let map_scope_defs
~(f : 'expr scope_def -> 'expr scope_def Bindlib.box)
(scopes : 'expr scopes) : 'expr scopes Bindlib.box =
fold_right_scope_defs
~f:(fun scope_def var_next acc ->
let new_scope_def = f scope_def in
let new_next = Bindlib.bind_var var_next acc in
Bindlib.box_apply2
(fun new_scope_def new_next ->
ScopeDef { new_scope_def with scope_next = new_next })
new_scope_def new_next)
~init:(Bindlib.box Nil) scopes
let map_exprs_in_scopes
~(f : 'expr Pos.marked -> 'expr Pos.marked Bindlib.box)
(scopes : 'expr scopes) : 'expr scopes Bindlib.box =
map_scope_defs
~f:(fun scope_def ->
let scope_input_var, scope_lets =
Bindlib.unbind scope_def.scope_body.scope_body_expr
in
let new_scope_body_expr = map_exprs_in_scope_lets ~f scope_lets in
let new_scope_body_expr =
Bindlib.bind_var scope_input_var new_scope_body_expr
in
Bindlib.box_apply
(fun new_scope_body_expr ->
{
scope_def with
scope_body =
{
scope_def.scope_body with
scope_body_expr = new_scope_body_expr;
};
})
new_scope_body_expr)
scopes
module Var = struct
type t = expr Bindlib.var
@ -189,62 +399,6 @@ module Var = struct
let compare x y = Bindlib.compare_vars x y
end
(** See [Bindlib.box_term] documentation for why we are doing that. *)
let rec box_expr (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
match Pos.unmark e with
| EVar (v, _pos) ->
Bindlib.box_apply (fun v -> (v, Pos.get_position e)) (Bindlib.box_var v)
| EApp (f, args) ->
Bindlib.box_apply2
(fun f args -> (EApp (f, args), Pos.get_position e))
(box_expr f)
(Bindlib.box_list (List.map box_expr args))
| EAbs ((binder, binder_pos), typs) ->
Bindlib.box_apply
(fun binder -> (EAbs ((binder, binder_pos), typs), Pos.get_position e))
(Bindlib.box_mbinder box_expr binder)
| ETuple (args, s) ->
Bindlib.box_apply
(fun args -> (ETuple (args, s), Pos.get_position e))
(Bindlib.box_list (List.map box_expr args))
| ETupleAccess (e1, n, s_name, typs) ->
Bindlib.box_apply
(fun e1 -> (ETupleAccess (e1, n, s_name, typs), Pos.get_position e))
(box_expr e1)
| EInj (e1, i, e_name, typ) ->
Bindlib.box_apply
(fun e1 -> (EInj (e1, i, e_name, typ), Pos.get_position e))
(box_expr e1)
| EMatch (arg, arms, e_name) ->
Bindlib.box_apply2
(fun arg arms -> (EMatch (arg, arms, e_name), Pos.get_position e))
(box_expr arg)
(Bindlib.box_list (List.map box_expr arms))
| EArray args ->
Bindlib.box_apply
(fun args -> (EArray args, Pos.get_position e))
(Bindlib.box_list (List.map box_expr args))
| ELit l -> Bindlib.box (ELit l, Pos.get_position e)
| EAssert e1 ->
Bindlib.box_apply
(fun e1 -> (EAssert e1, Pos.get_position e))
(box_expr e1)
| EOp op -> Bindlib.box (EOp op, Pos.get_position e)
| EDefault (excepts, just, cons) ->
Bindlib.box_apply3
(fun excepts just cons ->
(EDefault (excepts, just, cons), Pos.get_position e))
(Bindlib.box_list (List.map box_expr excepts))
(box_expr just) (box_expr cons)
| EIfThenElse (e1, e2, e3) ->
Bindlib.box_apply3
(fun e1 e2 e3 -> (EIfThenElse (e1, e2, e3), Pos.get_position e))
(box_expr e1) (box_expr e2) (box_expr e3)
| ErrorOnEmpty e1 ->
Bindlib.box_apply
(fun e1 -> (ErrorOnEmpty e1, Pos.get_position e1))
(box_expr e1)
module VarMap = Map.Make (Var)
module VarSet = Set.Make (Var)
@ -272,7 +426,8 @@ let rec free_vars_expr (e : expr Pos.marked) : VarSet.t =
let vs, body = Bindlib.unmbind binder in
Array.fold_right VarSet.remove vs (free_vars_expr body)
let rec free_vars_scope_body_expr (scope_lets : scope_body_expr) : VarSet.t =
let rec free_vars_scope_body_expr (scope_lets : expr scope_body_expr) : VarSet.t
=
match scope_lets with
| Result e -> free_vars_expr e
| ScopeLet { scope_let_expr = e; scope_let_next = next; _ } ->
@ -280,12 +435,12 @@ let rec free_vars_scope_body_expr (scope_lets : scope_body_expr) : VarSet.t =
VarSet.union (free_vars_expr e)
(VarSet.remove v (free_vars_scope_body_expr body))
let free_vars_scope_body (scope_body : scope_body) : VarSet.t =
let free_vars_scope_body (scope_body : expr scope_body) : VarSet.t =
let { scope_body_expr = binder; _ } = scope_body in
let v, body = Bindlib.unbind binder in
VarSet.remove v (free_vars_scope_body_expr body)
let rec free_vars_scopes (scopes : scopes) : VarSet.t =
let rec free_vars_scopes (scopes : expr scopes) : VarSet.t =
match scopes with
| Nil -> VarSet.empty
| ScopeDef { scope_body = body; scope_next = next; _ } ->
@ -411,8 +566,27 @@ and equal_exprs_list (es1 : expr Pos.marked list) (es2 : expr Pos.marked list) :
assume here that both lists have equal length *)
List.for_all (fun (x, y) -> equal_exprs x y) (List.combine es1 es2)
let rec unfold_scope_body_expr (ctx : decl_ctx) (scope_let : scope_body_expr) :
expr Pos.marked Bindlib.box =
type 'expr make_let_in_sig =
'expr Bindlib.var ->
typ Pos.marked ->
'expr Pos.marked Bindlib.box ->
'expr Pos.marked Bindlib.box ->
Pos.t ->
'expr Pos.marked Bindlib.box
type 'expr make_abs_sig =
'expr Bindlib.mvar ->
'expr Pos.marked Bindlib.box ->
Pos.t ->
typ Pos.marked list ->
Pos.t ->
'expr Pos.marked Bindlib.box
let rec unfold_scope_body_expr
~(box_expr : 'expr box_expr_sig)
~(make_let_in : 'expr make_let_in_sig)
(ctx : decl_ctx)
(scope_let : 'expr scope_body_expr) : 'expr Pos.marked Bindlib.box =
match scope_let with
| Result e -> box_expr e
| ScopeLet
@ -425,13 +599,18 @@ let rec unfold_scope_body_expr (ctx : decl_ctx) (scope_let : scope_body_expr) :
} ->
let var, next = Bindlib.unbind scope_let_next in
make_let_in var scope_let_typ (box_expr scope_let_expr)
(unfold_scope_body_expr ctx next)
(unfold_scope_body_expr ~box_expr ~make_let_in ctx next)
scope_let_pos
let build_whole_scope_expr
(ctx : decl_ctx) (body : scope_body) (pos_scope : Pos.t) =
~(box_expr : 'expr box_expr_sig)
~(make_abs : 'expr make_abs_sig)
~(make_let_in : 'expr make_let_in_sig)
(ctx : decl_ctx)
(body : 'expr scope_body)
(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 ctx 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
@ -461,11 +640,17 @@ let build_scope_typ_from_sig
in
(TArrow (input_typ, result_typ), pos)
type scope_name_or_var = ScopeName of ScopeName.t | ScopeVar of Var.t
type 'expr scope_name_or_var =
| ScopeName of ScopeName.t
| ScopeVar of 'expr Bindlib.var
let rec unfold_scopes
(ctx : decl_ctx) (s : scopes) (main_scope : scope_name_or_var) :
expr Pos.marked Bindlib.box =
~(box_expr : 'expr box_expr_sig)
~(make_abs : 'expr make_abs_sig)
~(make_let_in : 'expr make_let_in_sig)
(ctx : decl_ctx)
(s : 'expr scopes)
(main_scope : 'expr scope_name_or_var) : 'expr Pos.marked Bindlib.box =
match s with
| Nil -> (
match main_scope with
@ -485,12 +670,15 @@ let rec unfold_scopes
make_let_in scope_var
(build_scope_typ_from_sig ctx scope_body.scope_body_input_struct
scope_body.scope_body_output_struct scope_pos)
(build_whole_scope_expr ctx scope_body scope_pos)
(unfold_scopes ctx scope_next main_scope)
(build_whole_scope_expr ~box_expr ~make_abs ~make_let_in ctx scope_body
scope_pos)
(unfold_scopes ~box_expr ~make_abs ~make_let_in ctx scope_next
main_scope)
scope_pos
let build_whole_program_expr (p : program) (main_scope : ScopeName.t) =
unfold_scopes p.decl_ctx p.scopes (ScopeName main_scope)
unfold_scopes ~box_expr ~make_abs ~make_let_in p.decl_ctx p.scopes
(ScopeName main_scope)
let rec expr_size (e : expr Pos.marked) : int =
match Pos.unmark e with
@ -516,3 +704,11 @@ let rec expr_size (e : expr Pos.marked) : int =
(fun acc except -> acc + expr_size except)
(1 + expr_size just + expr_size cons)
exceptions
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
| _ -> map_expr () ~f e
in
f () e

232
compiler/dcalc/ast.mli
View File

@ -145,52 +145,207 @@ type scope_let_kind =
| DestructuringSubScopeResults (** [let s.x = result.x ]**)
| Assertion (** [let _ = assert e]*)
type scope_let = {
type 'expr scope_let = {
scope_let_kind : scope_let_kind;
scope_let_typ : typ Utils.Pos.marked;
scope_let_expr : expr Utils.Pos.marked;
scope_let_next : (expr, scope_body_expr) Bindlib.binder;
scope_let_expr : 'expr Utils.Pos.marked;
scope_let_next : ('expr, 'expr scope_body_expr) Bindlib.binder;
scope_let_pos : Utils.Pos.t;
}
(** This type is parametrized by the expression type so it can be reused in
later intermediate representations. *)
(** A scope let-binding has all the information necessary to make a proper
let-binding expression, plus an annotation for the kind of the let-binding
that comes from the compilation of a {!module: Scopelang.Ast} statement. *)
and scope_body_expr = Result of expr Utils.Pos.marked | ScopeLet of scope_let
and 'expr scope_body_expr =
| Result of 'expr Utils.Pos.marked
| ScopeLet of 'expr scope_let
type scope_body = {
type 'expr scope_body = {
scope_body_input_struct : StructName.t;
scope_body_output_struct : StructName.t;
scope_body_expr : (expr, scope_body_expr) Bindlib.binder;
scope_body_expr : ('expr, 'expr scope_body_expr) Bindlib.binder;
}
(** Instead of being a single expression, we give a little more ad-hoc structure
to the scope body by decomposing it in an ordered list of let-bindings, and
a result expression that uses the let-binded variables. The first binder is
the argument of type [scope_body_input_struct]. *)
type scope_def = {
type 'expr scope_def = {
scope_name : ScopeName.t;
scope_body : scope_body;
scope_next : (expr, scopes) Bindlib.binder;
scope_body : 'expr scope_body;
scope_next : ('expr, 'expr scopes) Bindlib.binder;
}
(** Finally, we do the same transformation for the whole program for the kinded
lets. This permit us to use bindlib variables for scopes names. *)
and scopes = Nil | ScopeDef of scope_def
and 'a scopes = Nil | ScopeDef of 'a scope_def
type program = { decl_ctx : decl_ctx; scopes : scopes }
type program = { decl_ctx : decl_ctx; scopes : expr scopes }
(** {1 Helpers} *)
(** {2 Boxed constructors}*)
val evar : expr Bindlib.var -> Pos.t -> expr Pos.marked Bindlib.box
val etuple :
expr Pos.marked Bindlib.box list ->
StructName.t option ->
Pos.t ->
expr Pos.marked Bindlib.box
val etupleaccess :
expr Pos.marked Bindlib.box ->
int ->
StructName.t option ->
typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val einj :
expr Pos.marked Bindlib.box ->
int ->
EnumName.t ->
typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val ematch :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box list ->
EnumName.t ->
Pos.t ->
expr Pos.marked Bindlib.box
val earray :
expr Pos.marked Bindlib.box list -> Pos.t -> expr Pos.marked Bindlib.box
val elit : lit -> Pos.t -> expr Pos.marked Bindlib.box
val eabs :
(expr, expr Pos.marked) Bindlib.mbinder Bindlib.box ->
Pos.t ->
typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val eapp :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box list ->
Pos.t ->
expr Pos.marked Bindlib.box
val eassert :
expr Pos.marked Bindlib.box -> Pos.t -> expr Pos.marked Bindlib.box
val eop : operator -> Pos.t -> expr Pos.marked Bindlib.box
val edefault :
expr Pos.marked Bindlib.box list ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
Pos.t ->
expr Pos.marked Bindlib.box
val eifthenelse :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
Pos.t ->
expr Pos.marked Bindlib.box
val eerroronempty :
expr Pos.marked Bindlib.box -> Pos.t -> expr Pos.marked Bindlib.box
val box_expr : expr Pos.marked -> expr Pos.marked Bindlib.box
type 'expr box_expr_sig = 'expr Pos.marked -> 'expr Pos.marked Bindlib.box
(**{2 Program traversal}*)
(** Be careful when using these traversal functions, as the bound variables they
open will be different at each traversal. *)
val fold_scope_lets :
f:('a -> scope_let -> 'a) -> init:'a -> scope_body_expr -> 'a
val map_expr :
'a ->
f:('a -> expr Pos.marked -> expr Pos.marked Bindlib.box) ->
expr Pos.marked ->
expr Pos.marked Bindlib.box
(** If you want to apply a map transform to an expression, you can save up
writing a painful match over all the cases of the AST. For instance, if you
want to remove all errors on empty, you can write
val fold_scope_defs : f:('a -> scope_def -> 'a) -> init:'a -> scopes -> 'a
{[
let remove_error_empty =
let rec f () e =
match Pos.unmark e with
| ErrorOnEmpty e1 -> map_expr () f e1
| _ -> map_expr () f e
in
f () e
]}
The first argument of map_expr is an optional context that you can carry
around during your map traversal. *)
val fold_left_scope_lets :
f:('a -> 'expr scope_let -> 'expr Bindlib.var -> 'a) ->
init:'a ->
'expr scope_body_expr ->
'a
(** Usage:
[fold_left_scope_lets ~f:(fun acc scope_let scope_let_var -> ...) ~init scope_lets],
where [scope_let_var] is the variable bound to the scope let in the next
scope lets to be examined. *)
val fold_right_scope_lets :
f:('expr scope_let -> 'expr Bindlib.var -> 'a -> 'a) ->
init:('expr Pos.marked -> 'a) ->
'expr scope_body_expr ->
'a
(** Usage:
[fold_right_scope_lets ~f:(fun scope_let scope_let_var acc -> ...) ~init scope_lets],
where [scope_let_var] is the variable bound to the scope let in the next
scope lets to be examined (which are before in the program order). *)
val map_exprs_in_scope_lets :
f:('expr Pos.marked -> 'expr Pos.marked Bindlib.box) ->
'expr scope_body_expr ->
'expr scope_body_expr Bindlib.box
val fold_left_scope_defs :
f:('a -> 'expr scope_def -> 'expr Bindlib.var -> 'a) ->
init:'a ->
'expr scopes ->
'a
(** Usage:
[fold_left_scope_defs ~f:(fun acc scope_def scope_var -> ...) ~init scope_def],
where [scope_var] is the variable bound to the scope in the next scopes to
be examined. *)
val fold_right_scope_defs :
f:('expr scope_def -> 'expr Bindlib.var -> 'a -> 'a) ->
init:'a ->
'expr scopes ->
'a
(** Usage:
[fold_right_scope_defs ~f:(fun scope_def scope_var acc -> ...) ~init scope_def],
where [scope_var] is the variable bound to the scope in the next scopes to
be examined (which are before in the program order). *)
val map_scope_defs :
f:('expr scope_def -> 'expr scope_def Bindlib.box) ->
'expr scopes ->
'expr scopes Bindlib.box
val map_exprs_in_scopes :
f:('expr Pos.marked -> 'expr Pos.marked Bindlib.box) ->
'expr scopes ->
'expr scopes Bindlib.box
(** This is the main map visitor for all the expressions inside all the scopes
of the program. *)
(** {2 Variables}*)
@ -205,12 +360,14 @@ module VarMap : Map.S with type key = Var.t
module VarSet : Set.S with type elt = Var.t
val free_vars_expr : expr Pos.marked -> VarSet.t
val free_vars_scope_body_expr : scope_body_expr -> VarSet.t
val free_vars_scope_body : scope_body -> VarSet.t
val free_vars_scopes : scopes -> VarSet.t
val free_vars_scope_body_expr : expr scope_body_expr -> VarSet.t
val free_vars_scope_body : expr scope_body -> VarSet.t
val free_vars_scopes : expr scopes -> VarSet.t
type vars = expr Bindlib.mvar
(** {2 Boxed term constructors}*)
val make_var : Var.t Pos.marked -> expr Pos.marked Bindlib.box
val make_abs :
@ -245,12 +402,47 @@ val equal_exprs : expr Pos.marked -> expr Pos.marked -> bool
(** {1 AST manipulation helpers}*)
type 'expr make_let_in_sig =
'expr Bindlib.var ->
typ Pos.marked ->
'expr Pos.marked Bindlib.box ->
'expr Pos.marked Bindlib.box ->
Pos.t ->
'expr Pos.marked Bindlib.box
type 'expr make_abs_sig =
'expr Bindlib.mvar ->
'expr Pos.marked Bindlib.box ->
Pos.t ->
typ Pos.marked list ->
Pos.t ->
'expr Pos.marked Bindlib.box
val build_whole_scope_expr :
decl_ctx -> scope_body -> Pos.t -> expr Pos.marked Bindlib.box
box_expr:'expr box_expr_sig ->
make_abs:'expr make_abs_sig ->
make_let_in:'expr make_let_in_sig ->
decl_ctx ->
'expr scope_body ->
Pos.t ->
'expr Pos.marked Bindlib.box
(** Usage: [build_whole_scope_expr ctx body scope_position] where
[scope_position] corresponds to the line of the scope declaration for
instance. *)
type 'expr scope_name_or_var =
| ScopeName of ScopeName.t
| ScopeVar of 'expr Bindlib.var
val unfold_scopes :
box_expr:'expr box_expr_sig ->
make_abs:'expr make_abs_sig ->
make_let_in:'expr make_let_in_sig ->
decl_ctx ->
'expr scopes ->
'expr scope_name_or_var ->
'expr Pos.marked Bindlib.box
val build_whole_program_expr :
program -> ScopeName.t -> expr Pos.marked Bindlib.box
(** Usage: [build_whole_program_expr program main_scope] builds an expression
@ -259,3 +451,7 @@ val build_whole_program_expr :
val expr_size : expr Pos.marked -> int
(** Used by the optimizer to know when to stop *)
val remove_logging_calls : expr Pos.marked -> expr Pos.marked Bindlib.box
(** Removes all calls to [Log] unary operators in the AST, replacing them by
their argument. *)

62
compiler/dcalc/optimizations.ml
View File

@ -193,7 +193,8 @@ let optimize_expr (decl_ctx : decl_ctx) (e : expr Pos.marked) =
let rec scope_lets_map
(t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box)
(ctx : 'a)
(scope_body_expr : scope_body_expr) : scope_body_expr Bindlib.box =
(scope_body_expr : expr scope_body_expr) : expr scope_body_expr Bindlib.box
=
match scope_body_expr with
| Result e -> Bindlib.box_apply (fun e' -> Result e') (t ctx e)
| ScopeLet scope_let ->
@ -214,7 +215,7 @@ let rec scope_lets_map
let rec scopes_map
(t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box)
(ctx : 'a)
(scopes : scopes) : scopes Bindlib.box =
(scopes : expr scopes) : expr scopes Bindlib.box =
match scopes with
| Nil -> Bindlib.box Nil
| ScopeDef scope_def ->
@ -255,60 +256,3 @@ let optimize_program (p : program) : program =
(program_map partial_evaluation
{ var_values = VarMap.empty; decl_ctx = p.decl_ctx }
p)
let rec remove_all_logs (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position e in
let rec_helper = remove_all_logs in
match Pos.unmark e with
| 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))
(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))
(rec_helper arg)
| EInj (arg, i, e_name, typs) ->
Bindlib.box_apply
(fun arg -> (EInj (arg, i, e_name, typs), pos))
(rec_helper arg)
| EMatch (arg, arms, e_name) ->
Bindlib.box_apply2
(fun arg arms -> (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))
(List.map rec_helper args |> Bindlib.box_list)
| ELit l -> Bindlib.box (ELit l, pos)
| EAbs ((binder, binder_pos), typs) ->
let vars, body = Bindlib.unmbind binder in
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))
new_binder
| EApp (f, args) ->
Bindlib.box_apply2
(fun f args ->
match (Pos.unmark f, args) with
| EOp (Unop (Log _)), [ arg ] -> arg
| _ -> (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)
| EOp op -> Bindlib.box (EOp op, pos)
| EDefault (exceptions, just, cons) ->
Bindlib.box_apply3
(fun 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 -> (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)

1
compiler/dcalc/optimizations.mli
View File

@ -22,4 +22,3 @@ open Ast
val optimize_expr : decl_ctx -> expr Pos.marked -> expr Pos.marked Bindlib.box
val optimize_program : program -> program
val remove_all_logs : expr Pos.marked -> expr Pos.marked Bindlib.box

5
compiler/dcalc/print.ml
View File

@ -356,9 +356,10 @@ let format_scope
?(debug : bool = false)
(ctx : decl_ctx)
(fmt : Format.formatter)
((n, s) : Ast.ScopeName.t * scope_body) =
((n, s) : Ast.ScopeName.t * Ast.expr scope_body) =
Format.fprintf fmt "@[<hov 2>%a %a =@ %a@]" format_keyword "let"
Ast.ScopeName.format_t n (format_expr ctx ~debug)
(Bindlib.unbox
(Ast.build_whole_scope_expr ctx s
(Ast.build_whole_scope_expr ~make_abs:Ast.make_abs
~make_let_in:Ast.make_let_in ~box_expr:Ast.box_expr ctx s
(Pos.get_position (Ast.ScopeName.get_info n))))

2
compiler/dcalc/print.mli
View File

@ -56,5 +56,5 @@ val format_scope :
?debug:bool (** [true] for debug printing *) ->
Ast.decl_ctx ->
Format.formatter ->
Ast.ScopeName.t * Ast.scope_body ->
Ast.ScopeName.t * Ast.expr Ast.scope_body ->
unit

47
compiler/driver.ml
View File

@ -217,8 +217,8 @@ let driver source_file (options : Cli.options) : int =
(Dcalc.Print.format_scope ~debug:options.debug prgm.decl_ctx)
( scope_uid,
Option.get
(Dcalc.Ast.fold_scope_defs ~init:None
~f:(fun acc scope_def ->
(Dcalc.Ast.fold_left_scope_defs ~init:None
~f:(fun acc scope_def _ ->
if
Dcalc.Ast.ScopeName.compare scope_def.scope_name
scope_uid
@ -298,17 +298,8 @@ let driver source_file (options : Cli.options) : int =
let prgm =
if options.closure_conversion then (
Cli.debug_print "Performing closure conversion...";
let prgm, closures =
Lcalc.Closure_conversion.closure_conversion prgm
in
let prgm = Lcalc.Closure_conversion.closure_conversion prgm in
let prgm = Bindlib.unbox prgm in
List.iter
(fun closure ->
Cli.debug_format "Closure found:\n%a"
(Lcalc.Print.format_expr ~debug:options.debug
prgm.decl_ctx)
(Bindlib.unbox closure.Lcalc.Closure_conversion.expr))
closures;
prgm)
else prgm
in
@ -323,19 +314,27 @@ let driver source_file (options : Cli.options) : int =
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
(Lcalc.Print.format_scope ~debug:options.debug prgm.decl_ctx)
(let body =
List.find
(fun body -> body.Lcalc.Ast.scope_body_name = scope_uid)
prgm.scopes
in
body)
( scope_uid,
Option.get
(Dcalc.Ast.fold_left_scope_defs ~init:None
~f:(fun acc scope_def _ ->
if
Dcalc.Ast.ScopeName.compare scope_def.scope_name
scope_uid
= 0
then Some scope_def.scope_body
else acc)
prgm.scopes) )
else
Format.fprintf fmt "%a\n"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n\n")
(fun fmt scope ->
(Lcalc.Print.format_scope prgm.decl_ctx) fmt scope))
prgm.scopes;
ignore
(Dcalc.Ast.fold_left_scope_defs ~init:0
~f:(fun i scope_def _ ->
Format.fprintf fmt "%s%a"
(if i = 0 then "" else "\n")
(Lcalc.Print.format_scope prgm.decl_ctx)
(scope_uid, scope_def.scope_body);
i + 1)
prgm.scopes);
at_end ();
exit 0
end;

132
compiler/lcalc/ast.ml
View File

@ -50,6 +50,92 @@ type expr =
| ERaise of except
| ECatch of expr Pos.marked * except * expr Pos.marked
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)
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)
let etupleaccess
(e1 : expr Pos.marked Bindlib.box)
(i : int)
(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
let einj
(e1 : expr Pos.marked Bindlib.box)
(i : int)
(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
let ematch
(arg : expr Pos.marked Bindlib.box)
(arms : expr Pos.marked Bindlib.box list)
(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))
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)
let elit (l : lit) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (ELit l, pos)
let eabs
(binder : (expr, expr Pos.marked) Bindlib.mbinder Bindlib.box)
(pos_binder : Pos.t)
(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))
binder
let eapp
(e1 : expr Pos.marked Bindlib.box)
(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))
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
let eop (op : Dcalc.Ast.operator) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (EOp op, pos)
let eraise (e1 : except) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (ERaise e1, pos)
let ecatch
(e1 : expr Pos.marked Bindlib.box)
(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
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
module Var = struct
type t = expr Bindlib.var
@ -66,6 +152,40 @@ module VarSet = Set.Make (Var)
type vars = expr Bindlib.mvar
let map_expr
(ctx : 'a)
~(f : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box)
(e : expr Pos.marked) : expr Pos.marked Bindlib.box =
match Pos.unmark e with
| EVar (v, _pos) -> evar v (Pos.get_position e)
| EApp (e1, args) ->
eapp (f ctx e1) (List.map (f ctx) args) (Pos.get_position e)
| EAbs ((binder, binder_pos), typs) ->
eabs
(Bindlib.box_mbinder (f ctx) binder)
binder_pos typs (Pos.get_position e)
| ETuple (args, s) -> etuple (List.map (f ctx) args) s (Pos.get_position e)
| ETupleAccess (e1, n, s_name, typs) ->
etupleaccess ((f ctx) e1) n s_name typs (Pos.get_position e)
| EInj (e1, i, e_name, typs) ->
einj ((f ctx) e1) i e_name typs (Pos.get_position e)
| EMatch (arg, arms, e_name) ->
ematch ((f ctx) arg) (List.map (f ctx) arms) e_name (Pos.get_position e)
| EArray args -> earray (List.map (f ctx) args) (Pos.get_position e)
| ELit l -> elit l (Pos.get_position e)
| EAssert e1 -> eassert ((f ctx) e1) (Pos.get_position e)
| EOp op -> Bindlib.box (EOp op, Pos.get_position e)
| ERaise exn -> eraise exn (Pos.get_position e)
| EIfThenElse (e1, e2, e3) ->
eifthenelse ((f ctx) e1) ((f ctx) e2) ((f ctx) e3) (Pos.get_position e)
| ECatch (e1, exn, e2) ->
ecatch (f ctx e1) exn (f ctx e2) (Pos.get_position e)
(** See [Bindlib.box_term] documentation for why we are doing that. *)
let box_expr (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let rec id_t () e = map_expr () ~f:id_t e in
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)
@ -89,8 +209,8 @@ let make_let_in
(x : Var.t)
(tau : D.typ Pos.marked)
(e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position (Bindlib.unbox e2) in
(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
let make_multiple_let_in
@ -169,11 +289,3 @@ let handle_default = Var.make ("handle_default", Pos.no_pos)
let handle_default_opt = Var.make ("handle_default_opt", Pos.no_pos)
type binder = (expr, expr Pos.marked) Bindlib.binder
type scope_body = {
scope_body_name : Dcalc.Ast.ScopeName.t;
scope_body_var : Var.t;
scope_body_expr : expr Pos.marked;
}
type program = { decl_ctx : D.decl_ctx; scopes : scope_body list }

92
compiler/lcalc/ast.mli
View File

@ -64,6 +64,8 @@ type expr =
| ERaise of except
| ECatch of expr Pos.marked * except * expr Pos.marked
type program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : expr Dcalc.Ast.scopes }
(** {1 Variable helpers} *)
module Var : sig
@ -77,6 +79,81 @@ module VarMap : Map.S with type key = Var.t
module VarSet : Set.S with type elt = Var.t
type vars = expr Bindlib.mvar
type binder = (expr, expr Pos.marked) Bindlib.binder
(** {1 Boxed constructors}*)
val evar : expr Bindlib.var -> Pos.t -> expr Pos.marked Bindlib.box
val etuple :
expr Pos.marked Bindlib.box list ->
Dcalc.Ast.StructName.t option ->
Pos.t ->
expr Pos.marked Bindlib.box
val etupleaccess :
expr Pos.marked Bindlib.box ->
int ->
Dcalc.Ast.StructName.t option ->
Dcalc.Ast.typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val einj :
expr Pos.marked Bindlib.box ->
int ->
Dcalc.Ast.EnumName.t ->
Dcalc.Ast.typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val ematch :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box list ->
Dcalc.Ast.EnumName.t ->
Pos.t ->
expr Pos.marked Bindlib.box
val earray :
expr Pos.marked Bindlib.box list -> Pos.t -> expr Pos.marked Bindlib.box
val elit : lit -> Pos.t -> expr Pos.marked Bindlib.box
val eabs :
(expr, expr Pos.marked) Bindlib.mbinder Bindlib.box ->
Pos.t ->
Dcalc.Ast.typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val eapp :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box list ->
Pos.t ->
expr Pos.marked Bindlib.box
val eassert :
expr Pos.marked Bindlib.box -> Pos.t -> expr Pos.marked Bindlib.box
val eop : Dcalc.Ast.operator -> Pos.t -> expr Pos.marked Bindlib.box
val eifthenelse :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
Pos.t ->
expr Pos.marked Bindlib.box
val ecatch :
expr Pos.marked Bindlib.box ->
except ->
expr Pos.marked Bindlib.box ->
Pos.t ->
expr Pos.marked Bindlib.box
val eraise : except -> Pos.t -> expr Pos.marked Bindlib.box
(** {1 Language terms construction}*)
val make_var : Var.t Pos.marked -> expr Pos.marked Bindlib.box
@ -99,6 +176,7 @@ val make_let_in :
Dcalc.Ast.typ Pos.marked ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
Pos.t ->
expr Pos.marked Bindlib.box
val make_multiple_let_in :
@ -136,15 +214,9 @@ val make_matchopt :
(** [e' = make_matchopt'' pos v e e_none e_some] Builds the term corresponding
to [match e with | None -> fun () -> e_none |Some -> fun v -> e_some]. *)
val box_expr : expr Pos.marked -> expr Pos.marked Bindlib.box
(** {1 Special symbols}*)
val handle_default : Var.t
val handle_default_opt : Var.t
type binder = (expr, expr Pos.marked) Bindlib.binder
type scope_body = {
scope_body_name : Dcalc.Ast.ScopeName.t;
scope_body_var : Var.t;
scope_body_expr : expr Pos.marked;
}
type program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : scope_body list }

103
compiler/lcalc/closure_conversion.ml
View File

@ -16,6 +16,7 @@
open Ast
open Utils
module D = Dcalc.Ast
(** TODO: This version is not yet debugged and ought to be specialized when
Lcalc has more structure. *)
@ -181,7 +182,8 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
(Bindlib.box_list
(List.map
(fun extra_var -> Bindlib.box_var extra_var)
extra_vars_list))),
extra_vars_list)))
(Pos.get_position e),
extra_vars )
| EApp ((EOp op, pos_op), args) ->
(* This corresponds to an operator call, which we don't want to
@ -241,8 +243,11 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
Pos.get_position e ))
(Bindlib.box_var code_var) (Bindlib.box_var env_var)
(Bindlib.box_list new_args))
(Pos.get_position e)
in
( make_let_in env_var (Dcalc.Ast.TAny, Pos.get_position e) new_e1 call_expr,
( make_let_in env_var
(Dcalc.Ast.TAny, Pos.get_position e)
new_e1 call_expr (Pos.get_position e),
free_vars )
| EAssert e1 ->
let new_e1, free_vars = closure_conversion_expr ctx e1 in
@ -271,48 +276,54 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
new_e1 new_e2,
VarSet.union free_vars1 free_vars2 )
let closure_conversion (p : program) : program Bindlib.box * closure list =
let all_scope_variables =
List.fold_left
(fun acc scope -> VarSet.add scope.scope_body_var acc)
VarSet.empty p.scopes
let closure_conversion (p : program) : program Bindlib.box =
let new_scopes, _ =
D.fold_left_scope_defs
~f:
(fun ((acc_new_scopes, global_vars) :
(expr D.scopes Bindlib.box -> expr D.scopes Bindlib.box)
* VarSet.t) (scope : expr D.scope_def) (scope_var : Var.t) ->
(* [acc_new_scopes] represents what has been translated in the past, it
needs a continuation to attach the rest of the translated scopes. *)
let scope_input_var, scope_body_expr =
Bindlib.unbind scope.scope_body.scope_body_expr
in
let global_vars = VarSet.add scope_var global_vars in
let ctx =
{
name_context =
Pos.unmark (Dcalc.Ast.ScopeName.get_info scope.scope_name);
globally_bound_vars = global_vars;
}
in
let new_scope_lets =
D.map_exprs_in_scope_lets
~f:(fun e -> fst (closure_conversion_expr ctx e))
scope_body_expr
in
let new_scope_body_expr =
Bindlib.bind_var scope_input_var new_scope_lets
in
( (fun next ->
acc_new_scopes
(Bindlib.box_apply2
(fun new_scope_body_expr next ->
D.ScopeDef
{
scope with
scope_body =
{
scope.scope_body with
scope_body_expr = new_scope_body_expr;
};
scope_next = next;
})
new_scope_body_expr
(Bindlib.bind_var scope_var next))),
global_vars ))
~init:(Fun.id, VarSet.of_list [ handle_default; handle_default_opt ])
p.scopes
in
let new_scopes, closures =
List.fold_left
(fun ((acc_new_scopes, acc_closures) :
scope_body Bindlib.box list * closure list) (scope : scope_body) ->
match Pos.unmark scope.scope_body_expr with
| EAbs ((binder, binder_pos), typs) ->
(* We do not hoist the outer-most EAbs which is the scope function
itself *)
let vars, body = Bindlib.unmbind binder in
let ctx =
{
name_context =
Pos.unmark
(Dcalc.Ast.ScopeName.get_info scope.scope_body_name);
globally_bound_vars =
VarSet.union all_scope_variables
(VarSet.of_list [ handle_default; handle_default_opt ]);
}
in
let new_body_expr, _ = closure_conversion_expr ctx body in
let new_binder = Bindlib.bind_mvar vars new_body_expr in
( Bindlib.box_apply
(fun new_binder ->
{
scope with
scope_body_expr =
( EAbs ((new_binder, binder_pos), typs),
Pos.get_position scope.scope_body_expr );
})
new_binder
:: acc_new_scopes,
[] @ acc_closures )
| _ -> failwith "should not happen")
([], []) p.scopes
in
( Bindlib.box_apply
(fun new_scopes -> { p with scopes = List.rev new_scopes })
(Bindlib.box_list new_scopes),
closures )
Bindlib.box_apply
(fun new_scopes -> { p with scopes = new_scopes })
(new_scopes (Bindlib.box D.Nil))

192
compiler/lcalc/compile_with_exceptions.ml
View File

@ -18,7 +18,7 @@ open Utils
module D = Dcalc.Ast
module A = Ast
type ctx = A.expr Pos.marked Bindlib.box D.VarMap.t
type ctx = A.Var.t D.VarMap.t
(** This environment contains a mapping between the variables in Dcalc and their
correspondance in Lcalc. *)
@ -53,9 +53,7 @@ let rec translate_default
A.make_app
(A.make_var (A.handle_default, pos_default))
[
Bindlib.box_apply
(fun exceptions -> (A.EArray exceptions, pos_default))
(Bindlib.box_list exceptions);
A.earray exceptions pos_default;
thunk_expr (translate_expr ctx just) pos_default;
thunk_expr (translate_expr ctx cons) pos_default;
]
@ -66,61 +64,40 @@ let rec translate_default
and translate_expr (ctx : ctx) (e : D.expr Pos.marked) :
A.expr Pos.marked Bindlib.box =
match Pos.unmark e with
| D.EVar v -> D.VarMap.find (Pos.unmark v) ctx
| D.EVar v -> A.make_var (D.VarMap.find (Pos.unmark v) ctx, Pos.get_position e)
| D.ETuple (args, s) ->
Bindlib.box_apply
(fun args -> Pos.same_pos_as (A.ETuple (args, s)) e)
(Bindlib.box_list (List.map (translate_expr ctx) args))
A.etuple (List.map (translate_expr ctx) args) s (Pos.get_position e)
| D.ETupleAccess (e1, i, s, ts) ->
Bindlib.box_apply
(fun e1 -> Pos.same_pos_as (A.ETupleAccess (e1, i, s, ts)) e)
(translate_expr ctx e1)
A.etupleaccess (translate_expr ctx e1) i s ts (Pos.get_position e)
| D.EInj (e1, i, en, ts) ->
Bindlib.box_apply
(fun e1 -> Pos.same_pos_as (A.EInj (e1, i, en, ts)) e)
(translate_expr ctx e1)
A.einj (translate_expr ctx e1) i en ts (Pos.get_position e)
| D.EMatch (e1, cases, en) ->
Bindlib.box_apply2
(fun e1 cases -> Pos.same_pos_as (A.EMatch (e1, cases, en)) e)
(translate_expr ctx e1)
(Bindlib.box_list (List.map (translate_expr ctx) cases))
A.ematch (translate_expr ctx e1)
(List.map (translate_expr ctx) cases)
en (Pos.get_position e)
| D.EArray es ->
Bindlib.box_apply
(fun es -> Pos.same_pos_as (A.EArray es) e)
(Bindlib.box_list (List.map (translate_expr ctx) es))
A.earray (List.map (translate_expr ctx) es) (Pos.get_position e)
| D.ELit l -> Bindlib.box (Pos.same_pos_as (translate_lit l) e)
| D.EOp op -> Bindlib.box (Pos.same_pos_as (A.EOp op) e)
| D.EOp op -> A.eop op (Pos.get_position e)
| D.EIfThenElse (e1, e2, e3) ->
Bindlib.box_apply3
(fun e1 e2 e3 -> Pos.same_pos_as (A.EIfThenElse (e1, e2, e3)) e)
(translate_expr ctx e1) (translate_expr ctx e2) (translate_expr ctx e3)
| D.EAssert e1 ->
Bindlib.box_apply
(fun e1 -> Pos.same_pos_as (A.EAssert e1) e)
(translate_expr ctx e1)
A.eifthenelse (translate_expr ctx e1) (translate_expr ctx e2)
(translate_expr ctx e3) (Pos.get_position e)
| D.EAssert e1 -> A.eassert (translate_expr ctx e1) (Pos.get_position e)
| D.ErrorOnEmpty arg ->
Bindlib.box_apply
(fun arg ->
Pos.same_pos_as
(A.ECatch
( arg,
A.EmptyError,
Pos.same_pos_as (A.ERaise A.NoValueProvided) e ))
e)
(translate_expr ctx arg)
A.ecatch (translate_expr ctx arg) A.EmptyError
(Bindlib.box (Pos.same_pos_as (A.ERaise A.NoValueProvided) e))
(Pos.get_position e)
| D.EApp (e1, args) ->
Bindlib.box_apply2
(fun e1 args -> Pos.same_pos_as (A.EApp (e1, args)) e)
(translate_expr ctx e1)
(Bindlib.box_list (List.map (translate_expr ctx) args))
A.eapp (translate_expr ctx e1)
(List.map (translate_expr ctx) args)
(Pos.get_position e)
| D.EAbs ((binder, pos_binder), ts) ->
let vars, body = Bindlib.unmbind binder in
let ctx, lc_vars =
Array.fold_right
(fun var (ctx, lc_vars) ->
let lc_var = A.Var.make (Bindlib.name_of var, pos_binder) in
let lc_var_expr = A.make_var (lc_var, pos_binder) in
(D.VarMap.add var lc_var_expr 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
@ -131,49 +108,102 @@ and translate_expr (ctx : ctx) (e : D.expr Pos.marked) :
Pos.same_pos_as (A.EAbs ((new_binder, pos_binder), ts)) e)
new_binder
| D.EDefault ([ exn ], just, cons) when !Cli.optimize_flag ->
Bindlib.box_apply3
(fun exn just cons ->
Pos.same_pos_as
(A.ECatch
( exn,
A.EmptyError,
Pos.same_pos_as
(A.EIfThenElse
(just, cons, Pos.same_pos_as (A.ERaise A.EmptyError) e))
e ))
e)
(translate_expr ctx exn) (translate_expr ctx just)
(translate_expr ctx cons)
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))
(Pos.get_position e))
(Pos.get_position e)
| D.EDefault (exceptions, just, cons) ->
translate_default ctx exceptions just cons (Pos.get_position e)
let rec translate_scopes
(decl_ctx : D.decl_ctx) (ctx : A.Var.t D.VarMap.t) (scopes : D.scopes) :
A.scope_body list =
match scopes with
| Nil -> []
| ScopeDef scope_def ->
let scope_var, scope_next = Bindlib.unbind scope_def.scope_next in
let new_n = A.Var.make (Bindlib.name_of scope_var, Pos.no_pos) in
let new_scope =
{
Ast.scope_body_name = scope_def.scope_name;
scope_body_var = new_n;
scope_body_expr =
Bindlib.unbox
(translate_expr
(D.VarMap.map (fun v -> A.make_var (v, Pos.no_pos)) ctx)
(Bindlib.unbox
(D.build_whole_scope_expr decl_ctx scope_def.scope_body
(Pos.get_position
(Dcalc.Ast.ScopeName.get_info scope_def.scope_name)))));
}
let rec translate_scope_lets
(decl_ctx : D.decl_ctx)
(ctx : A.Var.t D.VarMap.t)
(scope_lets : D.expr D.scope_body_expr) :
A.expr D.scope_body_expr Bindlib.box =
match scope_lets with
| Result e -> Bindlib.box_apply (fun e -> D.Result e) (translate_expr ctx e)
| ScopeLet scope_let ->
let old_scope_let_var, scope_let_next =
Bindlib.unbind scope_let.scope_let_next
in
let new_ctx = D.VarMap.add scope_var new_n ctx in
new_scope :: translate_scopes decl_ctx new_ctx scope_next
let new_scope_let_var =
A.Var.make (Bindlib.name_of old_scope_let_var, scope_let.scope_let_pos)
in
let new_scope_let_expr = translate_expr ctx scope_let.scope_let_expr in
let new_ctx = D.VarMap.add old_scope_let_var new_scope_let_var ctx in
let new_scope_next =
translate_scope_lets decl_ctx new_ctx scope_let_next
in
let new_scope_next = Bindlib.bind_var new_scope_let_var new_scope_next in
Bindlib.box_apply2
(fun new_scope_next new_scope_let_expr ->
D.ScopeLet
{
scope_let_typ = scope_let.D.scope_let_typ;
scope_let_kind = scope_let.D.scope_let_kind;
scope_let_pos = scope_let.D.scope_let_pos;
scope_let_next = new_scope_next;
scope_let_expr = new_scope_let_expr;
})
new_scope_next new_scope_let_expr
let rec translate_scopes
(decl_ctx : D.decl_ctx)
(ctx : A.Var.t D.VarMap.t)
(scopes : D.expr D.scopes) : A.expr D.scopes Bindlib.box =
match scopes with
| Nil -> Bindlib.box D.Nil
| ScopeDef scope_def ->
let old_scope_var, scope_next = Bindlib.unbind scope_def.scope_next in
let new_scope_var =
A.Var.make (D.ScopeName.get_info scope_def.scope_name)
in
let old_scope_input_var, scope_body_expr =
Bindlib.unbind scope_def.scope_body.scope_body_expr
in
let new_scope_input_var =
A.Var.make
( Bindlib.name_of old_scope_input_var,
Pos.get_position (D.ScopeName.get_info scope_def.scope_name) )
in
let new_ctx = D.VarMap.add old_scope_input_var new_scope_input_var ctx in
let new_scope_body_expr =
translate_scope_lets decl_ctx new_ctx scope_body_expr
in
let new_scope_body_expr =
Bindlib.bind_var new_scope_input_var new_scope_body_expr
in
let new_scope : A.expr D.scope_body Bindlib.box =
Bindlib.box_apply
(fun new_scope_body_expr ->
{
D.scope_body_input_struct =
scope_def.scope_body.scope_body_input_struct;
scope_body_output_struct =
scope_def.scope_body.scope_body_output_struct;
scope_body_expr = new_scope_body_expr;
})
new_scope_body_expr
in
let new_ctx = D.VarMap.add old_scope_var new_scope_var new_ctx in
let scope_next =
Bindlib.bind_var new_scope_var
(translate_scopes decl_ctx new_ctx scope_next)
in
Bindlib.box_apply2
(fun new_scope scope_next ->
D.ScopeDef
{
scope_name = scope_def.scope_name;
scope_body = new_scope;
scope_next;
})
new_scope scope_next
let translate_program (prgm : D.program) : A.program =
{
scopes = translate_scopes prgm.decl_ctx D.VarMap.empty prgm.scopes;
scopes =
Bindlib.unbox (translate_scopes prgm.decl_ctx D.VarMap.empty prgm.scopes);
decl_ctx = prgm.decl_ctx;
}

133
compiler/lcalc/compile_without_exceptions.ml
View File

@ -216,17 +216,13 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
(A.make_abs [| x |] (A.make_var (x, pos)) pos [ (D.TAny, pos) ] pos),
A.VarMap.empty )
(* pure terms *)
| D.ELit l -> (Bindlib.box (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
let e3', h3 = translate_and_hoist ctx e3 in
let e' =
Bindlib.box_apply3
(fun e1' e2' e3' -> (A.EIfThenElse (e1', e2', e3'), pos))
e1' e2' e3'
in
let e' = A.eifthenelse e1' e2' e3' pos in
(*(* equivalent code : *) let e' = let+ e1' = e1' and+ e2' = e2' and+ e3'
= e3' in (A.EIfThenElse (e1', e2', e3'), pos) in *)
@ -235,7 +231,7 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
(* 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
(Bindlib.box_apply (fun e1' -> (A.EAssert e1', pos)) e1', h1)
(A.eassert e1' pos, h1)
| D.EAbs ((binder, pos_binder), ts) ->
let vars, body = Bindlib.unmbind binder in
let ctx, lc_vars =
@ -270,11 +266,7 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
in
let hoists = disjoint_union_maps pos (h1 :: h_args) in
let e' =
Bindlib.box_apply2
(fun e1' args' -> (A.EApp (e1', args'), pos))
e1' (Bindlib.box_list args')
in
let e' = A.eapp e1' args' pos in
(e', hoists)
| ETuple (args, s) ->
let args', h_args =
@ -282,21 +274,14 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
in
let hoists = disjoint_union_maps pos h_args in
( Bindlib.box_apply
(fun args' -> (A.ETuple (args', s), pos))
(Bindlib.box_list args'),
hoists )
(A.etuple args' s pos, hoists)
| ETupleAccess (e1, i, s, ts) ->
let e1', hoists = translate_and_hoist ctx e1 in
let e1' =
Bindlib.box_apply (fun e1' -> (A.ETupleAccess (e1', i, s, ts), pos)) e1'
in
let e1' = A.etupleaccess e1' i s ts pos in
(e1', hoists)
| EInj (e1, i, en, ts) ->
let e1', hoists = translate_and_hoist ctx e1 in
let e1' =
Bindlib.box_apply (fun e1' -> (A.EInj (e1', i, en, ts), pos)) e1'
in
let e1' = A.einj e1' i en ts pos in
(e1', hoists)
| EMatch (e1, cases, en) ->
let e1', h1 = translate_and_hoist ctx e1 in
@ -305,19 +290,14 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
in
let hoists = disjoint_union_maps pos (h1 :: h_cases) in
let e' =
Bindlib.box_apply2
(fun e1' cases' -> (A.EMatch (e1', cases', en), pos))
e1' (Bindlib.box_list cases')
in
let e' = A.ematch e1' cases' en pos in
(e', hoists)
| EArray es ->
let es', hoists =
es |> List.map (translate_and_hoist ctx) |> List.split
in
( Bindlib.box_apply (fun es' -> (A.EArray es', pos)) (Bindlib.box_list es'),
disjoint_union_maps pos hoists )
(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) :
@ -391,14 +371,18 @@ and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Pos.marked) :
A.make_matchopt pos_hoist v (D.TAny, pos_hoist) c' (A.make_none pos_hoist)
acc)
let rec translate_scope_let (ctx : ctx) (lets : D.scope_body_expr) =
let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) :
A.expr D.scope_body_expr Bindlib.box =
match lets with
| Result e -> translate_expr ~append_esome:false ctx e
| Result e ->
Bindlib.box_apply
(fun e -> D.Result e)
(translate_expr ~append_esome:false ctx e)
| ScopeLet
{
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = typ;
scope_let_expr = D.EAbs ((binder, _), _), _pos;
scope_let_expr = D.EAbs ((binder, _), _), _;
scope_let_next = next;
scope_let_pos = pos;
} ->
@ -414,9 +398,19 @@ let rec translate_scope_let (ctx : ctx) (lets : D.scope_body_expr) =
let new_var =
(find ~info:"variable that was just created" var ctx').var
in
A.make_let_in new_var (translate_typ typ)
let new_next = translate_scope_let ctx' next in
Bindlib.box_apply2
(fun new_expr new_next ->
D.ScopeLet
{
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = translate_typ typ;
scope_let_expr = new_expr;
scope_let_next = new_next;
scope_let_pos = pos;
})
(translate_expr ctx ~append_esome:false expr)
(translate_scope_let ctx' next)
(Bindlib.bind_var new_var new_next)
| ScopeLet
{
scope_let_kind = SubScopeVarDefinition;
@ -434,9 +428,18 @@ let rec translate_scope_let (ctx : ctx) (lets : D.scope_body_expr) =
let new_var =
(find ~info:"variable that was just created" var ctx').var
in
A.make_let_in new_var (translate_typ typ)
Bindlib.box_apply2
(fun new_expr new_next ->
D.ScopeLet
{
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = translate_typ typ;
scope_let_expr = new_expr;
scope_let_next = new_next;
scope_let_pos = pos;
})
(translate_expr ctx ~append_esome:false expr)
(translate_scope_let ctx' next)
(Bindlib.bind_var new_var (translate_scope_let ctx' next))
| ScopeLet
{
scope_let_kind = SubScopeVarDefinition;
@ -479,32 +482,44 @@ let rec translate_scope_let (ctx : ctx) (lets : D.scope_body_expr) =
let new_var =
(find ~info:"variable that was just created" var ctx').var
in
A.make_let_in new_var (translate_typ typ)
Bindlib.box_apply2
(fun new_expr new_next ->
D.ScopeLet
{
scope_let_kind = kind;
scope_let_typ = translate_typ typ;
scope_let_expr = new_expr;
scope_let_next = new_next;
scope_let_pos = pos;
})
(translate_expr ctx ~append_esome:false expr)
(translate_scope_let ctx' next)
(Bindlib.bind_var new_var (translate_scope_let ctx' next))
let translate_scope_body (scope_pos : Pos.t) (ctx : ctx) (body : D.scope_body) :
A.expr Pos.marked Bindlib.box =
let translate_scope_body
(scope_pos : Pos.t) (ctx : ctx) (body : D.expr D.scope_body) :
A.expr D.scope_body Bindlib.box =
match body with
| {
scope_body_expr = result;
scope_body_input_struct = input_struct;
scope_body_output_struct = _output_struct;
scope_body_output_struct = output_struct;
} ->
let v, lets = Bindlib.unbind result in
let ctx' = add_var scope_pos v true ctx in
let v' = (find ~info:"variable that was just created" v ctx').var in
Bindlib.box_apply
(fun new_expr ->
{
D.scope_body_expr = new_expr;
scope_body_input_struct = input_struct;
scope_body_output_struct = output_struct;
})
(Bindlib.bind_var v' (translate_scope_let ctx' lets))
A.make_abs [| v' |]
(translate_scope_let ctx' lets)
Pos.no_pos
[ (D.TTuple ([], Some input_struct), Pos.no_pos) ]
Pos.no_pos
let rec translate_scopes (ctx : ctx) (scopes : D.scopes) :
Ast.scope_body list Bindlib.box =
let rec translate_scopes (ctx : ctx) (scopes : D.expr D.scopes) :
A.expr D.scopes Bindlib.box =
match scopes with
| Nil -> Bindlib.box []
| Nil -> Bindlib.box D.Nil
| ScopeDef { scope_name; scope_body; scope_next } ->
let scope_var, next = Bindlib.unbind scope_next in
let new_ctx = add_var Pos.no_pos scope_var true ctx in
@ -519,20 +534,13 @@ let rec translate_scopes (ctx : ctx) (scopes : D.scopes) :
Bindlib.box_apply2
(fun body tail ->
{
Ast.scope_body_var = new_scope_name;
scope_body_name = scope_name;
scope_body_expr = body;
}
:: tail)
new_body tail
let translate_scopes (ctx : ctx) (scopes : D.scopes) : Ast.scope_body list =
Bindlib.unbox (translate_scopes ctx scopes)
D.ScopeDef { scope_name; scope_body = body; scope_next = tail })
new_body
(Bindlib.bind_var new_scope_name tail)
let translate_program (prgm : D.program) : A.program =
let inputs_structs =
D.fold_scope_defs prgm.scopes ~init:[] ~f:(fun acc scope_def ->
D.fold_left_scope_defs prgm.scopes ~init:[] ~f:(fun acc scope_def _ ->
scope_def.D.scope_body.scope_body_input_struct :: acc)
in
@ -565,7 +573,8 @@ let translate_program (prgm : D.program) : A.program =
in
let scopes =
prgm.scopes |> translate_scopes { decl_ctx; vars = D.VarMap.empty }
Bindlib.unbox
(translate_scopes { decl_ctx; vars = D.VarMap.empty } prgm.scopes)
in
{ scopes; decl_ctx }

48
compiler/lcalc/optimizations.ml
View File

@ -27,9 +27,9 @@ let visitor_map
syntax tree modified. Used in other transformations. *)
let default_mark e' = Pos.same_pos_as e' e in
match Pos.unmark e with
| EVar (v, pos) ->
| EVar (v, _pos) ->
let+ v = Bindlib.box_var v in
(v, pos)
default_mark @@ v
| ETuple (args, n) ->
let+ args = args |> List.map (t ctx) |> Bindlib.box_list in
default_mark @@ ETuple (args, n)
@ -101,36 +101,16 @@ let rec beta_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box
| _ -> visitor_map beta_expr () e
let iota_optimizations (p : program) : program =
{
p with
scopes =
List.map
(fun scope_body ->
{
scope_body with
scope_body_expr =
Bindlib.unbox (iota_expr () scope_body.scope_body_expr);
})
p.scopes;
}
let new_scopes = Dcalc.Ast.map_exprs_in_scopes ~f:(iota_expr ()) p.scopes in
{ p with scopes = Bindlib.unbox new_scopes }
(* TODO: beta optimizations apply inlining of the program. We left the inclusion
of beta-optimization as future work since its produce code that is harder to
read, and can produce exponential blowup of the size of the generated
program. *)
let _beta_optimizations (p : program) : program =
{
p with
scopes =
List.map
(fun scope_body ->
{
scope_body with
scope_body_expr =
Bindlib.unbox (beta_expr () scope_body.scope_body_expr);
})
p.scopes;
}
let new_scopes = Dcalc.Ast.map_exprs_in_scopes ~f:(beta_expr ()) p.scopes in
{ p with scopes = Bindlib.unbox new_scopes }
let rec peephole_expr (_ : unit) (e : expr Pos.marked) :
expr Pos.marked Bindlib.box =
@ -161,18 +141,10 @@ let rec peephole_expr (_ : unit) (e : expr Pos.marked) :
| _ -> visitor_map peephole_expr () e
let peephole_optimizations (p : program) : program =
{
p with
scopes =
List.map
(fun scope_body ->
{
scope_body with
scope_body_expr =
Bindlib.unbox (peephole_expr () scope_body.scope_body_expr);
})
p.scopes;
}
let new_scopes =
Dcalc.Ast.map_exprs_in_scopes ~f:(peephole_expr ()) p.scopes
in
{ p with scopes = Bindlib.unbox new_scopes }
let optimize_program (p : program) : program =
p |> iota_optimizations |> peephole_optimizations

16
compiler/lcalc/print.ml
View File

@ -74,8 +74,8 @@ let format_var (fmt : Format.formatter) (v : Var.t) : unit =
Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
let rec format_expr
(ctx : Dcalc.Ast.decl_ctx)
?(debug : bool = false)
(ctx : Dcalc.Ast.decl_ctx)
(fmt : Format.formatter)
(e : expr Pos.marked) : unit =
let format_expr = format_expr ctx ~debug in
@ -204,11 +204,13 @@ let rec format_expr
format_punctuation "(" format_expr e' format_punctuation ")"
let format_scope
(decl_ctx : Dcalc.Ast.decl_ctx)
?(debug : bool = false)
(ctx : Dcalc.Ast.decl_ctx)
(fmt : Format.formatter)
(body : scope_body) : unit =
Format.fprintf fmt "@[<hov 2>%a %a %a@ %a@]" format_keyword "let" format_var
body.scope_body_var format_punctuation "="
(format_expr decl_ctx ~debug)
body.scope_body_expr
((n, s) : Dcalc.Ast.ScopeName.t * Ast.expr Dcalc.Ast.scope_body) : unit =
Format.fprintf fmt "@[<hov 2>%a %a =@ %a@]" format_keyword "let"
Dcalc.Ast.ScopeName.format_t n (format_expr ctx ~debug)
(Bindlib.unbox
(Dcalc.Ast.build_whole_scope_expr ~make_abs:Ast.make_abs
~make_let_in:Ast.make_let_in ~box_expr:Ast.box_expr ctx s
(Pos.get_position (Dcalc.Ast.ScopeName.get_info n))))

6
compiler/lcalc/print.mli
View File

@ -28,15 +28,15 @@ val format_var : Format.formatter -> Ast.Var.t -> unit
val format_exception : Format.formatter -> Ast.except -> unit
val format_expr :
Dcalc.Ast.decl_ctx ->
?debug:bool ->
Dcalc.Ast.decl_ctx ->
Format.formatter ->
Ast.expr Pos.marked ->
unit
val format_scope :
Dcalc.Ast.decl_ctx ->
?debug:bool ->
Dcalc.Ast.decl_ctx ->
Format.formatter ->
Ast.scope_body ->
Dcalc.Ast.ScopeName.t * Ast.expr Dcalc.Ast.scope_body ->
unit

46
compiler/lcalc/to_ocaml.ml
View File

@ -513,6 +513,40 @@ let format_ctx
Format.fprintf fmt "%a@\n@\n" format_enum_decl (e, find_enum e ctx))
(type_ordering @ scope_structs)
let rec format_scope_body_expr
(ctx : Dcalc.Ast.decl_ctx)
(fmt : Format.formatter)
(scope_lets : Ast.expr Dcalc.Ast.scope_body_expr) : unit =
match scope_lets with
| Dcalc.Ast.Result e -> format_expr ctx fmt e
| Dcalc.Ast.ScopeLet scope_let ->
let scope_let_var, scope_let_next =
Bindlib.unbind scope_let.scope_let_next
in
Format.fprintf fmt "@[<hov 2>let %a: %a = %a in@]@\n%a" format_var
scope_let_var format_typ scope_let.scope_let_typ (format_expr ctx)
scope_let.scope_let_expr
(format_scope_body_expr ctx)
scope_let_next
let rec format_scopes
(ctx : Dcalc.Ast.decl_ctx)
(fmt : Format.formatter)
(scopes : Ast.expr Dcalc.Ast.scopes) : unit =
match scopes with
| Dcalc.Ast.Nil -> ()
| Dcalc.Ast.ScopeDef scope_def ->
let scope_input_var, scope_body_expr =
Bindlib.unbind scope_def.scope_body.scope_body_expr
in
let scope_var, scope_next = Bindlib.unbind scope_def.scope_next in
Format.fprintf fmt "@\n@\n@[<hov 2>let %a (%a: %a) : %a =@\n%a@]%a"
format_var scope_var format_var scope_input_var format_struct_name
scope_def.scope_body.scope_body_input_struct format_struct_name
scope_def.scope_body.scope_body_output_struct
(format_scope_body_expr ctx)
scope_body_expr (format_scopes ctx) scope_next
let format_program
(fmt : Format.formatter)
(p : Ast.program)
@ -525,13 +559,5 @@ let format_program
@\n\
[@@@@@@ocaml.warning \"-4-26-27-32-41-42\"]@\n\
@\n\
%a@\n\
@\n\
%a@?"
(format_ctx type_ordering) p.decl_ctx
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n@\n")
(fun fmt body ->
Format.fprintf fmt "@[<hov 2>let@ %a@ =@ %a@]" format_var
body.scope_body_var (format_expr p.decl_ctx) body.scope_body_expr))
p.scopes
%a%a@?"
(format_ctx type_ordering) p.decl_ctx (format_scopes p.decl_ctx) p.scopes

20
compiler/literate/literate_common.mli
View File

@ -17,16 +17,16 @@
open Utils
val literal_title : Cli.backend_lang -> string
(** Return the title traduction according the given {!type:
Utils.Cli.backend_lang}. *)
(** Return the title traduction according the given
{!type:Utils.Cli.backend_lang}. *)
val literal_generated_by : Cli.backend_lang -> string
(** Return the 'generated by' traduction according the given {!type:
Utils.Cli.backend_lang}. *)
(** Return the 'generated by' traduction according the given
{!type:Utils.Cli.backend_lang}. *)
val literal_source_files : Cli.backend_lang -> string
(** Return the 'source files weaved' traduction according the given {!type:
Utils.Cli.backend_lang}. *)
(** Return the 'source files weaved' traduction according the given
{!type:Utils.Cli.backend_lang}. *)
val literal_disclaimer_and_link : Cli.backend_lang -> string
(** Return the traduction of a paragraph giving a basic disclaimer about Catala
@ -34,12 +34,12 @@ val literal_disclaimer_and_link : Cli.backend_lang -> string
Utils.Cli.backend_lang}. *)
val literal_last_modification : Cli.backend_lang -> string
(** Return the 'last modification' traduction according the given {!type:
Utils.Cli.backend_lang}. *)
(** Return the 'last modification' traduction according the given
{!type:Utils.Cli.backend_lang}. *)
val get_language_extension : Cli.backend_lang -> string
(** Return the file extension corresponding to the given {!type:
Utils.Cli.backend_lang}. *)
(** Return the file extension corresponding to the given
{!type:Utils.Cli.backend_lang}. *)
val run_pandoc : string -> Cli.backend_option -> string
(** Runs the [pandoc] on a string to pretty-print markdown features into the

144
compiler/scalc/compile_from_lambda.ml
View File

@ -125,15 +125,10 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Pos.marked) :
and translate_statements (ctxt : ctxt) (block_expr : L.expr Pos.marked) :
A.block =
match Pos.unmark block_expr with
| L.EApp
((L.EAbs ((binder, _), [ (D.TLit D.TUnit, _) ]), _), [ (L.EAssert e, _) ])
->
| L.EAssert e ->
(* Assertions are always encapsulated in a unit-typed let binding *)
let _, body = Bindlib.unmbind binder in
let e_stmts, new_e = translate_expr ctxt e in
e_stmts
@ (A.SAssert (Pos.unmark new_e), Pos.get_position block_expr)
:: translate_statements ctxt body
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
@ -281,30 +276,16 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Pos.marked) :
Pos.get_position block_expr );
])
let translate_scope
let rec translate_scope_body_expr
(scope_name : D.ScopeName.t)
(decl_ctx : D.decl_ctx)
(var_dict : A.LocalName.t L.VarMap.t)
(func_dict : A.TopLevelName.t L.VarMap.t)
(scope_expr : L.expr Pos.marked) :
(A.LocalName.t Pos.marked * D.typ Pos.marked) list * A.block =
match Pos.unmark scope_expr with
| L.EAbs ((binder, binder_pos), typs) ->
let vars, body = Bindlib.unmbind binder in
let var_dict =
Array.fold_left
(fun var_dict var ->
L.VarMap.add var
(A.LocalName.fresh (Bindlib.name_of var, binder_pos))
var_dict)
L.VarMap.empty vars
in
let param_list =
List.map2
(fun var typ -> ((L.VarMap.find var var_dict, binder_pos), typ))
(Array.to_list vars) typs
in
let new_body =
translate_statements
(scope_expr : L.expr D.scope_body_expr) : A.block =
match scope_expr with
| Result e ->
let block, new_e =
translate_expr
{
decl_ctx;
func_dict;
@ -312,48 +293,109 @@ let translate_scope
inside_definition_of = None;
context_name = Pos.unmark (D.ScopeName.get_info scope_name);
}
body
e
in
(param_list, new_body)
| _ -> assert false
(* should not happen *)
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 =
A.LocalName.fresh (Bindlib.name_of let_var, scope_let.scope_let_pos)
in
let new_var_dict = L.VarMap.add let_var let_var_id var_dict in
(match scope_let.scope_let_kind with
| D.Assertion ->
translate_statements
{
decl_ctx;
func_dict;
var_dict;
inside_definition_of = Some let_var_id;
context_name = Pos.unmark (D.ScopeName.get_info scope_name);
}
scope_let.scope_let_expr
| _ ->
let let_expr_stmts, new_let_expr =
translate_expr
{
decl_ctx;
func_dict;
var_dict;
inside_definition_of = Some let_var_id;
context_name = Pos.unmark (D.ScopeName.get_info scope_name);
}
scope_let.scope_let_expr
in
let_expr_stmts
@ [
( A.SLocalDecl
( (let_var_id, scope_let.scope_let_pos),
scope_let.scope_let_typ ),
scope_let.scope_let_pos );
( A.SLocalDef ((let_var_id, scope_let.scope_let_pos), new_let_expr),
scope_let.scope_let_pos );
])
@ translate_scope_body_expr scope_name decl_ctx new_var_dict func_dict
scope_let_next
let translate_program (p : L.program) : A.program =
{
decl_ctx = p.L.decl_ctx;
scopes =
(let _, new_scopes =
List.fold_left
(fun (func_dict, new_scopes) body ->
let new_scope_params, new_scope_body =
translate_scope body.L.scope_body_name p.decl_ctx func_dict
body.L.scope_body_expr
D.fold_left_scope_defs
~f:(fun (func_dict, new_scopes) scope_def scope_var ->
let scope_input_var, scope_body_expr =
Bindlib.unbind scope_def.scope_body.scope_body_expr
in
let input_pos =
Pos.get_position (D.ScopeName.get_info scope_def.scope_name)
in
let scope_input_var_id =
A.LocalName.fresh (Bindlib.name_of scope_input_var, input_pos)
in
let var_dict =
L.VarMap.singleton scope_input_var scope_input_var_id
in
let new_scope_body =
translate_scope_body_expr scope_def.D.scope_name p.decl_ctx
var_dict func_dict scope_body_expr
in
let func_id =
A.TopLevelName.fresh
(Bindlib.name_of body.Lcalc.Ast.scope_body_var, Pos.no_pos)
in
let func_dict =
L.VarMap.add body.Lcalc.Ast.scope_body_var func_id func_dict
A.TopLevelName.fresh (Bindlib.name_of scope_var, Pos.no_pos)
in
let func_dict = L.VarMap.add scope_var func_id func_dict in
( func_dict,
{
Ast.scope_body_name = body.Lcalc.Ast.scope_body_name;
Ast.scope_body_name = scope_def.D.scope_name;
Ast.scope_body_var = func_id;
scope_body_func =
{
A.func_params = new_scope_params;
A.func_params =
[
( (scope_input_var_id, input_pos),
( D.TTuple
( List.map snd
(D.StructMap.find
scope_def.D.scope_body
.D.scope_body_input_struct
p.L.decl_ctx.ctx_structs),
Some
scope_def.D.scope_body
.D.scope_body_input_struct ),
input_pos ) );
];
A.func_body = new_scope_body;
};
}
:: new_scopes ))
( (if !Cli.avoid_exceptions_flag then
L.VarMap.singleton L.handle_default_opt
(A.TopLevelName.fresh ("handle_default_opt", Pos.no_pos))
else
L.VarMap.singleton L.handle_default
(A.TopLevelName.fresh ("handle_default", Pos.no_pos))),
[] )
~init:
( (if !Cli.avoid_exceptions_flag then
L.VarMap.singleton L.handle_default_opt
(A.TopLevelName.fresh ("handle_default_opt", Pos.no_pos))
else
L.VarMap.singleton L.handle_default
(A.TopLevelName.fresh ("handle_default", Pos.no_pos))),
[] )
p.L.scopes
in
List.rev new_scopes);

19
compiler/scopelang/scope_to_dcalc.ml
View File

@ -342,8 +342,8 @@ let translate_rule
(ctx : ctx)
(rule : Ast.rule)
((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info) :
(Dcalc.Ast.scope_body_expr Bindlib.box ->
Dcalc.Ast.scope_body_expr Bindlib.box)
(Dcalc.Ast.expr Dcalc.Ast.scope_body_expr Bindlib.box ->
Dcalc.Ast.expr Dcalc.Ast.scope_body_expr Bindlib.box)
* ctx =
match rule with
| Definition ((ScopeVar a, var_def_pos), tau, a_io, e) ->
@ -555,7 +555,8 @@ let translate_rule
Some called_scope_return_struct ),
pos_sigma )
in
let call_scope_let (next : Dcalc.Ast.scope_body_expr Bindlib.box) =
let call_scope_let
(next : Dcalc.Ast.expr Dcalc.Ast.scope_body_expr Bindlib.box) =
Bindlib.box_apply2
(fun next call_expr ->
Dcalc.Ast.ScopeLet
@ -569,7 +570,8 @@ let translate_rule
(Bindlib.bind_var result_tuple_var next)
call_expr
in
let result_bindings_lets (next : Dcalc.Ast.scope_body_expr Bindlib.box) =
let result_bindings_lets
(next : Dcalc.Ast.expr Dcalc.Ast.scope_body_expr Bindlib.box) =
List.fold_right
(fun (var_ctx, v) (next, i) ->
( Bindlib.box_apply2
@ -643,7 +645,7 @@ let translate_rules
(rules : Ast.rule list)
((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info)
(sigma_return_struct_name : Ast.StructName.t) :
Dcalc.Ast.scope_body_expr Bindlib.box * ctx =
Dcalc.Ast.expr Dcalc.Ast.scope_body_expr Bindlib.box * ctx =
let scope_lets, new_ctx =
List.fold_left
(fun (scope_lets, ctx) rule ->
@ -682,7 +684,7 @@ let translate_scope_decl
(sctx : scope_sigs_ctx)
(scope_name : Ast.ScopeName.t)
(sigma : Ast.scope_decl) :
Dcalc.Ast.scope_body Bindlib.box * Dcalc.Ast.struct_ctx =
Dcalc.Ast.expr Dcalc.Ast.scope_body Bindlib.box * Dcalc.Ast.struct_ctx =
let sigma_info = Ast.ScopeName.get_info sigma.scope_decl_name in
let scope_sig = Ast.ScopeMap.find sigma.scope_decl_name sctx in
let scope_variables = scope_sig.scope_sig_local_vars in
@ -751,7 +753,8 @@ let translate_scope_decl
pos_sigma )
| NoInput -> failwith "should not happen"
in
let input_destructurings (next : Dcalc.Ast.scope_body_expr Bindlib.box) =
let input_destructurings
(next : Dcalc.Ast.expr Dcalc.Ast.scope_body_expr Bindlib.box) =
fst
(List.fold_right
(fun (var_ctx, v) (next, i) ->
@ -888,7 +891,7 @@ let translate_program (prgm : Ast.program) :
in
(* the resulting expression is the list of definitions of all the scopes,
ending with the top-level scope. *)
let (scopes, decl_ctx) : Dcalc.Ast.scopes Bindlib.box * _ =
let (scopes, decl_ctx) : Dcalc.Ast.expr Dcalc.Ast.scopes Bindlib.box * _ =
List.fold_right
(fun scope_name (scopes, decl_ctx) ->
let scope = Ast.ScopeMap.find scope_name prgm.program_scopes in

9
compiler/surface/lexer_common.mli
View File

@ -47,8 +47,8 @@ val get_law_heading : Sedlexing.lexbuf -> Tokens.token
module type LocalisedLexer = sig
val token_list : (string * Tokens.token) list
(** Same as {!val: Surface.Lexer_common.token_list_language_agnostic}, but
with tokens whose string varies with the input language. *)
(** Same as {!val:Surface.Lexer_common.token_list_language_agnostic}, but with
tokens whose string varies with the input language. *)
val lex_builtin : string -> Ast.builtin_expression option
(** Simple lexer for builtins *)
@ -60,7 +60,6 @@ module type LocalisedLexer = sig
(** Main lexing function used outside code blocks *)
val lexer : Sedlexing.lexbuf -> Tokens.token
(** Entry point of the lexer, distributes to {!val: lex_code} or
{!val:lex_law} depending of the current {!val:
Surface.Lexer_common.context}. *)
(** Entry point of the lexer, distributes to {!val:lex_code} or {!val:lex_law}
depending of the current {!val:Surface.Lexer_common.context}. *)
end

4
compiler/utils/cli.mli
View File

@ -36,8 +36,8 @@ val catala_backend_option_to_string : backend_option -> string
given [backend].*)
val catala_backend_option_of_string : string -> backend_option option
(** [catala_backend_option_of_string backend] returns the {!type:
backend_option} corresponding to the [backend] string. *)
(** [catala_backend_option_of_string backend] returns the {!type:backend_option}
corresponding to the [backend] string. *)
(** {2 Configuration globals} *)

40
compiler/verification/conditions.ml
View File

@ -76,34 +76,20 @@ let half_product (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list =
let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Pos.marked) :
expr Pos.marked =
match Pos.unmark e with
| EApp
( (EOp (Unop (Log _)), _),
[
( ErrorOnEmpty
( EDefault
( [ (EApp ((EVar (x, _), _), [ (ELit LUnit, _) ]), _) ],
(ELit (LBool true), _),
cons ),
_ ),
_ );
] )
| ErrorOnEmpty
( EDefault
( [ (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
match Pos.unmark body with
| EApp ((EOp (Unop (Log _)), _), [ arg ]) -> arg
| _ ->
Errors.raise_spanned_error (Pos.get_position e)
"Internal error: this expression does not have the structure \
expected by the VC generator:\n\
%a"
(Print.format_expr ~debug:true ctx.decl)
e)
| ErrorOnEmpty (EApp ((EOp (Unop (Log _)), _), [ d ]), _)
| EApp ((EOp (Unop (Log _)), _), [ (ErrorOnEmpty d, _) ]) ->
body
| ErrorOnEmpty d ->
d (* input subscope variables and non-input scope variable *)
| _ ->
Errors.raise_spanned_error (Pos.get_position e)
@ -304,7 +290,7 @@ type verification_condition = {
}
let rec generate_verification_conditions_scope_body_expr
(ctx : ctx) (scope_body_expr : scope_body_expr) :
(ctx : ctx) (scope_body_expr : expr scope_body_expr) :
ctx * verification_condition list =
match scope_body_expr with
| Result _ -> (ctx, [])
@ -323,9 +309,9 @@ let rec generate_verification_conditions_scope_body_expr
exceptions to something defined in the subscope so we just ought
to verify only that the exceptions overlap. *)
let e =
match_and_ignore_outer_reentrant_default ctx
scope_let.scope_let_expr
Bindlib.unbox (remove_logging_calls scope_let.scope_let_expr)
in
let e = match_and_ignore_outer_reentrant_default ctx e in
let vc_confl, vc_confl_typs =
generate_vs_must_not_return_confict ctx e
in
@ -389,7 +375,7 @@ let rec generate_verification_conditions_scope_body_expr
(new_ctx, vc_list @ new_vcs)
let rec generate_verification_conditions_scopes
(decl_ctx : decl_ctx) (scopes : scopes) (s : ScopeName.t option) :
(decl_ctx : decl_ctx) (scopes : expr scopes) (s : ScopeName.t option) :
verification_condition list =
match scopes with
| Nil -> []

3
compiler/verification/solver.ml
View File

@ -34,8 +34,7 @@ let solve_vc
Z3backend.Io.translate_expr
(Z3backend.Io.make_context decl_ctx
vc.Conditions.vc_free_vars_typ)
(Bindlib.unbox
(Dcalc.Optimizations.remove_all_logs vc.Conditions.vc_guard))
vc.Conditions.vc_guard
in
Z3backend.Io.Success (z3_vc, ctx)
with Failure msg -> Fail msg ))

2
examples/Makefile
View File

@ -1,5 +1,5 @@
CATALA_OPTS?=
CLERK_OPTS?=
CLERK_OPTS?=--makeflags="$(MAKEFLAGS)"
CLERK=_build/default/build_system/clerk.exe --exe "_build/default/compiler/catala.exe" \
$(CLERK_OPTS) $(if $(CATALA_OPTS),--catala-opts=$(CATALA_OPTS),) test

3672
french_law/js/french_law.js generated
View File

File diff suppressed because one or more lines are too long

282
french_law/ocaml/law_source/allocations_familiales.ml generated
View File

@ -339,7 +339,8 @@ let embed_interface_allocations_familiales_in
] )
let allocation_familiales_avril2008
(allocation_familiales_avril2008_in : allocation_familiales_avril2008_in) =
(allocation_familiales_avril2008_in : allocation_familiales_avril2008_in) :
allocation_familiales_avril2008_out =
let age_minimum_alinea_1_l521_3_ : integer =
log_variable_definition
[ "AllocationFamilialesAvril2008"; "âge_minimum_alinéa_1_l521_3" ]
@ -349,25 +350,23 @@ let allocation_familiales_avril2008
raise
(NoValueProvided
{
filename = "./securite_sociale_R.catala_fr";
start_line = 78;
start_column = 49;
end_line = 78;
end_column = 51;
filename = "./prologue.catala_fr";
start_line = 77;
start_column = 10;
end_line = 77;
end_column = 37;
law_headings =
[
"Article R521-1";
"Chapitre 1er : Allocations familiales";
"Titre 2 : Prestations générales d'entretien";
"Livre 5 : Prestations familiales et prestations assimilées";
"Partie réglementaire - Décrets en Conseil d'Etat";
"Code de la sécurité sociale";
"Allocations familiales";
"Champs d'applications";
"Prologue";
];
}))
in
{ age_minimum_alinea_1_l521_3_out = age_minimum_alinea_1_l521_3_ }
let enfant_le_plus_age (enfant_le_plus_age_in : enfant_le_plus_age_in) =
let enfant_le_plus_age (enfant_le_plus_age_in : enfant_le_plus_age_in) :
enfant_le_plus_age_out =
let enfants_ : enfant array = enfant_le_plus_age_in.enfants_in in
let le_plus_age_ : enfant =
log_variable_definition
@ -407,7 +406,7 @@ let enfant_le_plus_age (enfant_le_plus_age_in : enfant_le_plus_age_in) =
in
{ le_plus_age_out = le_plus_age_ }
let smic (smic_in : smic_in) =
let smic (smic_in : smic_in) : smic_out =
let date_courante_ : date = smic_in.date_courante_in in
let residence_ : collectivite = smic_in.residence_in in
let brut_horaire_ : money =
@ -582,7 +581,8 @@ let smic (smic_in : smic_in) =
let base_mensuelle_allocations_familiales
(base_mensuelle_allocations_familiales_in :
base_mensuelle_allocations_familiales_in) =
base_mensuelle_allocations_familiales_in) :
base_mensuelle_allocations_familiales_out =
let date_courante_ : date =
base_mensuelle_allocations_familiales_in.date_courante_in
in
@ -714,7 +714,8 @@ let base_mensuelle_allocations_familiales
{ montant_out = montant_ }
let prestations_familiales
(prestations_familiales_in : prestations_familiales_in) =
(prestations_familiales_in : prestations_familiales_in) :
prestations_familiales_out =
let date_courante_ : date = prestations_familiales_in.date_courante_in in
let prestation_courante_ : element_prestations_familiales =
prestations_familiales_in.prestation_courante_in
@ -729,19 +730,16 @@ let prestations_familiales
raise
(NoValueProvided
{
filename = "./securite_sociale_R.catala_fr";
start_line = 21;
start_column = 34;
end_line = 21;
end_column = 36;
filename = "./prologue.catala_fr";
start_line = 61;
start_column = 10;
end_line = 61;
end_column = 22;
law_headings =
[
"Article R512-2";
"Chapitre 2 : Champ d'application.";
"Titre 1 : Champ d'application - Généralités";
"Livre 5 : Prestations familiales et prestations assimilées";
"Partie réglementaire - Décrets en Conseil d'Etat";
"Code de la sécurité sociale";
"Prestations familiales";
"Champs d'applications";
"Prologue";
];
}))
in
@ -754,13 +752,13 @@ let prestations_familiales
raise
(NoValueProvided
{
filename = "./prologue.catala_fr";
start_line = 66;
start_column = 3;
end_line = 66;
end_column = 7;
filename = "./../smic/smic.catala_fr";
start_line = 9;
start_column = 10;
end_line = 9;
end_column = 23;
law_headings =
[ "Prestations familiales"; "Champs d'applications"; "Prologue" ];
[ "Prologue"; "Montant du salaire minimum de croissance" ];
})
in
let smic_dot_residence_ : collectivite =
@ -772,13 +770,13 @@ let prestations_familiales
raise
(NoValueProvided
{
filename = "./prologue.catala_fr";
start_line = 66;
start_column = 3;
end_line = 66;
end_column = 7;
filename = "./../smic/smic.catala_fr";
start_line = 10;
start_column = 10;
end_line = 10;
end_column = 19;
law_headings =
[ "Prestations familiales"; "Champs d'applications"; "Prologue" ];
[ "Prologue"; "Montant du salaire minimum de croissance" ];
})
in
let result_ : smic_out =
@ -1111,7 +1109,8 @@ let prestations_familiales
}
let allocations_familiales
(allocations_familiales_in : allocations_familiales_in) =
(allocations_familiales_in : allocations_familiales_in) :
allocations_familiales_out =
let personne_charge_effective_permanente_est_parent_ : bool =
allocations_familiales_in.personne_charge_effective_permanente_est_parent_in
in
@ -1519,19 +1518,16 @@ let allocations_familiales
raise
(NoValueProvided
{
filename = "./securite_sociale_D.catala_fr";
start_line = 291;
start_column = 43;
end_line = 291;
end_column = 44;
filename = "./prologue.catala_fr";
start_line = 146;
start_column = 11;
end_line = 146;
end_column = 32;
law_headings =
[
"Article D521-2";
"Chapitre 1er : Allocations familiales";
"Titre 2 : Prestations générales d'entretien";
"Livre 5 : Prestations familiales et prestations assimilées";
"Partie réglementaire - Décrets simples";
"Code de la sécurité sociale";
"Allocations familiales";
"Champs d'applications";
"Prologue";
];
}))
in
@ -1544,19 +1540,16 @@ let allocations_familiales
raise
(NoValueProvided
{
filename = "./securite_sociale_R.catala_fr";
start_line = 64;
start_column = 52;
end_line = 64;
end_column = 53;
filename = "./prologue.catala_fr";
start_line = 148;
start_column = 11;
end_line = 148;
end_column = 41;
law_headings =
[
"Article R521-1";
"Chapitre 1er : Allocations familiales";
"Titre 2 : Prestations générales d'entretien";
"Livre 5 : Prestations familiales et prestations assimilées";
"Partie réglementaire - Décrets en Conseil d'Etat";
"Code de la sécurité sociale";
"Allocations familiales";
"Champs d'applications";
"Prologue";
];
}))
in
@ -1587,13 +1580,14 @@ let allocations_familiales
raise
(NoValueProvided
{
filename = "./prologue.catala_fr";
start_line = 143;
start_column = 3;
end_line = 143;
end_column = 7;
filename =
"./../base_mensuelle_allocations_familiales/bmaf.catala_fr";
start_line = 5;
start_column = 10;
end_line = 5;
end_column = 23;
law_headings =
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
[ "Montant de la base mensuelle des allocations familiales" ];
})
in
let result_ : base_mensuelle_allocations_familiales_out =
@ -1617,12 +1611,12 @@ let allocations_familiales
(NoValueProvided
{
filename = "./prologue.catala_fr";
start_line = 140;
start_column = 3;
end_line = 140;
end_column = 25;
start_line = 63;
start_column = 10;
end_line = 63;
end_column = 23;
law_headings =
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
[ "Prestations familiales"; "Champs d'applications"; "Prologue" ];
})
in
let prestations_familiales_dot_prestation_courante_ :
@ -1638,12 +1632,12 @@ let allocations_familiales
(NoValueProvided
{
filename = "./prologue.catala_fr";
start_line = 140;
start_column = 3;
end_line = 140;
end_column = 25;
start_line = 64;
start_column = 10;
end_line = 64;
end_column = 29;
law_headings =
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
[ "Prestations familiales"; "Champs d'applications"; "Prologue" ];
})
in
let prestations_familiales_dot_residence_ : collectivite =
@ -1656,12 +1650,12 @@ let allocations_familiales
(NoValueProvided
{
filename = "./prologue.catala_fr";
start_line = 140;
start_column = 3;
end_line = 140;
end_column = 25;
start_line = 65;
start_column = 10;
end_line = 65;
end_column = 19;
law_headings =
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
[ "Prestations familiales"; "Champs d'applications"; "Prologue" ];
})
in
let result_ : prestations_familiales_out =
@ -1707,10 +1701,10 @@ let allocations_familiales
(NoValueProvided
{
filename = "./prologue.catala_fr";
start_line = 142;
start_column = 3;
end_line = 142;
end_column = 21;
start_line = 80;
start_column = 10;
end_line = 80;
end_column = 17;
law_headings =
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
})
@ -5142,7 +5136,7 @@ let allocations_familiales
let interface_allocations_familiales
(interface_allocations_familiales_in : interface_allocations_familiales_in)
=
: interface_allocations_familiales_out =
let i_date_courante_ : date =
interface_allocations_familiales_in.i_date_courante_in
in
@ -5249,17 +5243,13 @@ let interface_allocations_familiales
raise
(NoValueProvided
{
filename = "./epilogue.catala_fr";
start_line = 77;
start_column = 3;
end_line = 77;
end_column = 25;
filename = "./prologue.catala_fr";
start_line = 86;
start_column = 10;
end_line = 86;
end_column = 57;
law_headings =
[
"Interface du programme";
"Épilogue";
"Dispositions spéciales relatives à Mayotte";
];
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
})
in
let allocations_familiales_dot_personne_charge_effective_permanente_remplit_titre__i_
@ -5295,17 +5285,13 @@ let interface_allocations_familiales
raise
(NoValueProvided
{
filename = "./epilogue.catala_fr";
start_line = 77;
start_column = 3;
end_line = 77;
end_column = 25;
filename = "./prologue.catala_fr";
start_line = 87;
start_column = 10;
end_line = 87;
end_column = 62;
law_headings =
[
"Interface du programme";
"Épilogue";
"Dispositions spéciales relatives à Mayotte";
];
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
})
in
let allocations_familiales_dot_ressources_menage_ : money =
@ -5320,17 +5306,13 @@ let interface_allocations_familiales
raise
(NoValueProvided
{
filename = "./epilogue.catala_fr";
start_line = 77;
start_column = 3;
end_line = 77;
end_column = 25;
filename = "./prologue.catala_fr";
start_line = 88;
start_column = 10;
end_line = 88;
end_column = 27;
law_headings =
[
"Interface du programme";
"Épilogue";
"Dispositions spéciales relatives à Mayotte";
];
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
})
in
let allocations_familiales_dot_residence_ : collectivite =
@ -5342,17 +5324,13 @@ let interface_allocations_familiales
raise
(NoValueProvided
{
filename = "./epilogue.catala_fr";
start_line = 77;
start_column = 3;
end_line = 77;
end_column = 25;
filename = "./prologue.catala_fr";
start_line = 89;
start_column = 10;
end_line = 89;
end_column = 19;
law_headings =
[
"Interface du programme";
"Épilogue";
"Dispositions spéciales relatives à Mayotte";
];
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
})
in
let allocations_familiales_dot_date_courante_ : date =
@ -5367,17 +5345,13 @@ let interface_allocations_familiales
raise
(NoValueProvided
{
filename = "./epilogue.catala_fr";
start_line = 77;
start_column = 3;
end_line = 77;
end_column = 25;
filename = "./prologue.catala_fr";
start_line = 92;
start_column = 10;
end_line = 92;
end_column = 23;
law_headings =
[
"Interface du programme";
"Épilogue";
"Dispositions spéciales relatives à Mayotte";
];
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
})
in
let allocations_familiales_dot_enfants_a_charge_ : enfant array =
@ -5392,17 +5366,13 @@ let interface_allocations_familiales
raise
(NoValueProvided
{
filename = "./epilogue.catala_fr";
start_line = 77;
start_column = 3;
end_line = 77;
end_column = 25;
filename = "./prologue.catala_fr";
start_line = 95;
start_column = 10;
end_line = 95;
end_column = 26;
law_headings =
[
"Interface du programme";
"Épilogue";
"Dispositions spéciales relatives à Mayotte";
];
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
})
in
let allocations_familiales_dot_avait_enfant_a_charge_avant_1er_janvier_2012_ :
@ -5438,17 +5408,13 @@ let interface_allocations_familiales
raise
(NoValueProvided
{
filename = "./epilogue.catala_fr";
start_line = 77;
start_column = 3;
end_line = 77;
end_column = 25;
filename = "./prologue.catala_fr";
start_line = 116;
start_column = 10;
end_line = 116;
end_column = 54;
law_headings =
[
"Interface du programme";
"Épilogue";
"Dispositions spéciales relatives à Mayotte";
];
[ "Allocations familiales"; "Champs d'applications"; "Prologue" ];
})
in
let result_ : allocations_familiales_out =

206
french_law/python/src/allocations_familiales.py generated
View File

@ -517,15 +517,12 @@ def allocation_familiales_avril2008(allocation_familiales_avril2008_in: Allocati
try:
temp_age_minimum_alinea_1_l521_3 = integer_of_string("16")
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./securite_sociale_R.catala_fr",
start_line=78, start_column=49,
end_line=78, end_column=51,
law_headings=["Article R521-1",
"Chapitre 1er : Allocations familiales",
"Titre 2 : Prestations générales d'entretien",
"Livre 5 : Prestations familiales et prestations assimilées",
"Partie réglementaire - Décrets en Conseil d'Etat",
"Code de la sécurité sociale"]))
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=77, start_column=10,
end_line=77, end_column=37,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
age_minimum_alinea_1_l521_3 = log_variable_definition(["AllocationFamilialesAvril2008",
"âge_minimum_alinéa_1_l521_3"], temp_age_minimum_alinea_1_l521_3)
return AllocationFamilialesAvril2008Out(age_minimum_alinea_1_l521_3_out=age_minimum_alinea_1_l521_3)
@ -782,38 +779,33 @@ def prestations_familiales(prestations_familiales_in: PrestationsFamilialesIn):
try:
temp_age_l512_3_2 = integer_of_string("20")
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./securite_sociale_R.catala_fr",
start_line=21, start_column=34,
end_line=21, end_column=36,
law_headings=["Article R512-2",
"Chapitre 2 : Champ d'application.",
"Titre 1 : Champ d'application - Généralités",
"Livre 5 : Prestations familiales et prestations assimilées",
"Partie réglementaire - Décrets en Conseil d'Etat",
"Code de la sécurité sociale"]))
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=61, start_column=10,
end_line=61, end_column=22,
law_headings=["Prestations familiales",
"Champs d'applications",
"Prologue"]))
age_l512_3_2 = log_variable_definition(["PrestationsFamiliales",
"âge_l512_3_2"], temp_age_l512_3_2)
try:
temp_smic_dot_date_courante = log_variable_definition(["PrestationsFamiliales",
"smic.date_courante"], date_courante_2)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=66, start_column=3,
end_line=66, end_column=7,
law_headings=["Prestations familiales",
"Champs d'applications",
"Prologue"]))
raise NoValueProvided(SourcePosition(filename="./../smic/smic.catala_fr",
start_line=9, start_column=10,
end_line=9, end_column=23,
law_headings=["Prologue",
"Montant du salaire minimum de croissance"]))
smic_dot_date_courante = temp_smic_dot_date_courante
try:
temp_smic_dot_residence = log_variable_definition(["PrestationsFamiliales",
"smic.résidence"], residence_1)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=66, start_column=3,
end_line=66, end_column=7,
law_headings=["Prestations familiales",
"Champs d'applications",
"Prologue"]))
raise NoValueProvided(SourcePosition(filename="./../smic/smic.catala_fr",
start_line=10, start_column=10,
end_line=10, end_column=19,
law_headings=["Prologue",
"Montant du salaire minimum de croissance"]))
smic_dot_residence = temp_smic_dot_residence
result = log_end_call(["PrestationsFamiliales", "smic", "Smic"],
log_begin_call(["PrestationsFamiliales", "smic", "Smic"], smic,
@ -1449,29 +1441,23 @@ def allocations_familiales(allocations_familiales_in: AllocationsFamilialesIn):
try:
temp_nombre_enfants_l521_1 = integer_of_string("3")
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./securite_sociale_D.catala_fr",
start_line=291, start_column=43,
end_line=291, end_column=44,
law_headings=["Article D521-2",
"Chapitre 1er : Allocations familiales",
"Titre 2 : Prestations générales d'entretien",
"Livre 5 : Prestations familiales et prestations assimilées",
"Partie réglementaire - Décrets simples",
"Code de la sécurité sociale"]))
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=146, start_column=11,
end_line=146, end_column=32,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
nombre_enfants_l521_1 = log_variable_definition(["AllocationsFamiliales",
"nombre_enfants_l521_1"], temp_nombre_enfants_l521_1)
try:
temp_nombre_enfants_alinea_2_l521_3 = integer_of_string("3")
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./securite_sociale_R.catala_fr",
start_line=64, start_column=52,
end_line=64, end_column=53,
law_headings=["Article R521-1",
"Chapitre 1er : Allocations familiales",
"Titre 2 : Prestations générales d'entretien",
"Livre 5 : Prestations familiales et prestations assimilées",
"Partie réglementaire - Décrets en Conseil d'Etat",
"Code de la sécurité sociale"]))
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=148, start_column=11,
end_line=148, end_column=41,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
nombre_enfants_alinea_2_l521_3 = log_variable_definition(["AllocationsFamiliales",
"nombre_enfants_alinéa_2_l521_3"],
temp_nombre_enfants_alinea_2_l521_3)
@ -1485,12 +1471,10 @@ def allocations_familiales(allocations_familiales_in: AllocationsFamilialesIn):
temp_bmaf_dot_date_courante = log_variable_definition(["AllocationsFamiliales",
"bmaf.date_courante"], date_courante_3)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=143, start_column=3,
end_line=143, end_column=7,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
raise NoValueProvided(SourcePosition(filename="./../base_mensuelle_allocations_familiales/bmaf.catala_fr",
start_line=5, start_column=10,
end_line=5, end_column=23,
law_headings=["Montant de la base mensuelle des allocations familiales"]))
bmaf_dot_date_courante = temp_bmaf_dot_date_courante
result_2 = log_end_call(["AllocationsFamiliales", "bmaf",
"BaseMensuelleAllocationsFamiliales"],
@ -1504,9 +1488,9 @@ def allocations_familiales(allocations_familiales_in: AllocationsFamilialesIn):
"prestations_familiales.date_courante"], date_courante_3)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=140, start_column=3,
end_line=140, end_column=25,
law_headings=["Allocations familiales",
start_line=63, start_column=10,
end_line=63, end_column=23,
law_headings=["Prestations familiales",
"Champs d'applications",
"Prologue"]))
prestations_familiales_dot_date_courante = temp_prestations_familiales_dot_date_courante
@ -1517,9 +1501,9 @@ def allocations_familiales(allocations_familiales_in: AllocationsFamilialesIn):
Unit()))
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=140, start_column=3,
end_line=140, end_column=25,
law_headings=["Allocations familiales",
start_line=64, start_column=10,
end_line=64, end_column=29,
law_headings=["Prestations familiales",
"Champs d'applications",
"Prologue"]))
prestations_familiales_dot_prestation_courante = temp_prestations_familiales_dot_prestation_courante
@ -1528,9 +1512,9 @@ def allocations_familiales(allocations_familiales_in: AllocationsFamilialesIn):
"prestations_familiales.résidence"], residence_2)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=140, start_column=3,
end_line=140, end_column=25,
law_headings=["Allocations familiales",
start_line=65, start_column=10,
end_line=65, end_column=19,
law_headings=["Prestations familiales",
"Champs d'applications",
"Prologue"]))
prestations_familiales_dot_residence = temp_prestations_familiales_dot_residence
@ -1550,8 +1534,8 @@ def allocations_familiales(allocations_familiales_in: AllocationsFamilialesIn):
"enfant_le_plus_âgé.enfants"], enfants_a_charge)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=142, start_column=3,
end_line=142, end_column=21,
start_line=80, start_column=10,
end_line=80, end_column=17,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
@ -3640,9 +3624,9 @@ def allocations_familiales(allocations_familiales_in: AllocationsFamilialesIn):
montant_verse = log_variable_definition(["AllocationsFamiliales",
"montant_versé"], temp_montant_verse)
try:
allocations_familiales = (personne_charge_effective_permanente_est_parent or
(not personne_charge_effective_permanente_est_parent and
personne_charge_effective_permanente_remplit_titre__i))
temp__ = (personne_charge_effective_permanente_est_parent or
(not personne_charge_effective_permanente_est_parent and
personne_charge_effective_permanente_remplit_titre__i))
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./securite_sociale_L.catala_fr",
start_line=230, start_column=5,
@ -3653,7 +3637,7 @@ def allocations_familiales(allocations_familiales_in: AllocationsFamilialesIn):
"Livre 5 : Prestations familiales et prestations assimilées",
"Partie législative",
"Code de la sécurité sociale"]))
assert allocations_familiales
assert temp__
return AllocationsFamilialesOut(montant_verse_out=montant_verse)
@ -3715,12 +3699,12 @@ def interface_allocations_familiales(interface_allocations_familiales_in: Interf
"allocations_familiales.personne_charge_effective_permanente_est_parent"],
temp_allocations_familiales_dot_personne_charge_effective_permanente_est_parent)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./epilogue.catala_fr",
start_line=77, start_column=3,
end_line=77, end_column=25,
law_headings=["Interface du programme",
"Épilogue",
"Dispositions spéciales relatives à Mayotte"]))
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=86, start_column=10,
end_line=86, end_column=57,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
allocations_familiales_dot_personne_charge_effective_permanente_est_parent = temp_allocations_familiales_dot_personne_charge_effective_permanente_est_parent_1
try:
try:
@ -3737,57 +3721,57 @@ def interface_allocations_familiales(interface_allocations_familiales_in: Interf
"allocations_familiales.personne_charge_effective_permanente_remplit_titre_I"],
temp_allocations_familiales_dot_personne_charge_effective_permanente_remplit_titre__i)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./epilogue.catala_fr",
start_line=77, start_column=3,
end_line=77, end_column=25,
law_headings=["Interface du programme",
"Épilogue",
"Dispositions spéciales relatives à Mayotte"]))
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=87, start_column=10,
end_line=87, end_column=62,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
allocations_familiales_dot_personne_charge_effective_permanente_remplit_titre__i = temp_allocations_familiales_dot_personne_charge_effective_permanente_remplit_titre__i_1
try:
temp_allocations_familiales_dot_ressources_menage = log_variable_definition(["InterfaceAllocationsFamiliales",
"allocations_familiales.ressources_ménage"],
i_ressources_menage)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./epilogue.catala_fr",
start_line=77, start_column=3,
end_line=77, end_column=25,
law_headings=["Interface du programme",
"Épilogue",
"Dispositions spéciales relatives à Mayotte"]))
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=88, start_column=10,
end_line=88, end_column=27,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
allocations_familiales_dot_ressources_menage = temp_allocations_familiales_dot_ressources_menage
try:
temp_allocations_familiales_dot_residence = log_variable_definition(["InterfaceAllocationsFamiliales",
"allocations_familiales.résidence"], i_residence)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./epilogue.catala_fr",
start_line=77, start_column=3,
end_line=77, end_column=25,
law_headings=["Interface du programme",
"Épilogue",
"Dispositions spéciales relatives à Mayotte"]))
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=89, start_column=10,
end_line=89, end_column=19,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
allocations_familiales_dot_residence = temp_allocations_familiales_dot_residence
try:
temp_allocations_familiales_dot_date_courante = log_variable_definition(["InterfaceAllocationsFamiliales",
"allocations_familiales.date_courante"], i_date_courante)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./epilogue.catala_fr",
start_line=77, start_column=3,
end_line=77, end_column=25,
law_headings=["Interface du programme",
"Épilogue",
"Dispositions spéciales relatives à Mayotte"]))
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=92, start_column=10,
end_line=92, end_column=23,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
allocations_familiales_dot_date_courante = temp_allocations_familiales_dot_date_courante
try:
temp_allocations_familiales_dot_enfants_a_charge = log_variable_definition(["InterfaceAllocationsFamiliales",
"allocations_familiales.enfants_à_charge"], enfants_a_charge_1)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./epilogue.catala_fr",
start_line=77, start_column=3,
end_line=77, end_column=25,
law_headings=["Interface du programme",
"Épilogue",
"Dispositions spéciales relatives à Mayotte"]))
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=95, start_column=10,
end_line=95, end_column=26,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
allocations_familiales_dot_enfants_a_charge = temp_allocations_familiales_dot_enfants_a_charge
try:
try:
@ -3804,12 +3788,12 @@ def interface_allocations_familiales(interface_allocations_familiales_in: Interf
"allocations_familiales.avait_enfant_à_charge_avant_1er_janvier_2012"],
temp_allocations_familiales_dot_avait_enfant_a_charge_avant_1er_janvier_2012)
except EmptyError:
raise NoValueProvided(SourcePosition(filename="./epilogue.catala_fr",
start_line=77, start_column=3,
end_line=77, end_column=25,
law_headings=["Interface du programme",
"Épilogue",
"Dispositions spéciales relatives à Mayotte"]))
raise NoValueProvided(SourcePosition(filename="./prologue.catala_fr",
start_line=116, start_column=10,
end_line=116, end_column=54,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
allocations_familiales_dot_avait_enfant_a_charge_avant_1er_janvier_2012 = temp_allocations_familiales_dot_avait_enfant_a_charge_avant_1er_janvier_2012_1
result_5 = log_end_call(["InterfaceAllocationsFamiliales",
"allocations_familiales", "AllocationsFamiliales"],

2
tests/Makefile
View File

@ -3,7 +3,7 @@
############################################
CATALA_OPTS?=
CLERK_OPTS?=
CLERK_OPTS?=--makeflags="$(MAKEFLAGS)"
CLERK=_build/default/build_system/clerk.exe --exe "_build/default/compiler/catala.exe" \
$(CLERK_OPTS) $(if $(CATALA_OPTS),--catala-opts=$(CATALA_OPTS),) test