mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-20 00:41:05 +03:00
Merge pull request #235 from CatalaLang/c_backend
C backend : preparatory work
This commit is contained in:
commit
c4d031d7ef
@ -217,6 +217,7 @@ let add_reset_rules_aux
|
||||
Lit redirect;
|
||||
Var "expected_output";
|
||||
Lit "2>&1";
|
||||
Lit "| true";
|
||||
]
|
||||
in
|
||||
let reset_with_scope_rule =
|
||||
|
@ -16,7 +16,7 @@ let test_ninja_start () =
|
||||
Buffer.clear Format.stdbuf;
|
||||
Nj.format Format.str_formatter ninja_start;
|
||||
let expected_format =
|
||||
"rule reset_with_scope\n command = catala -s $scope $catala_cmd $tested_file $extra_flags --unstyled > $expected_output 2>&1\n description = RESET scope $scope of file $tested_file with the $catala_cmd command\n\nrule reset_with_scope_and_output\n command = catala -s $scope $catala_cmd $tested_file $extra_flags --unstyled -o $expected_output 2>&1\n description = RESET scope $scope of file $tested_file with the $catala_cmd command\n\nrule reset_without_scope\n command = catala $catala_cmd $tested_file $extra_flags --unstyled > $expected_output 2>&1\n description = RESET file $tested_file with the $catala_cmd command\n\nrule reset_without_scope_and_output\n command = catala $catala_cmd $tested_file $extra_flags --unstyled -o $expected_output 2>&1\n description = RESET file $tested_file with the $catala_cmd command\n\nrule run_and_display_final_message\n command = :\n description = All tests $test_file_or_folder passed!\n\nrule test_with_scope\n command = catala -s $scope $catala_cmd $tested_file $extra_flags --unstyled 2>&1 | colordiff -u -b $expected_output -\n description = TEST scope $scope of file $tested_file with the $catala_cmd command\n\nrule test_with_scope_and_output\n command = catala -s $scope $catala_cmd $tested_file $extra_flags --unstyled -o $tmp_file ; colordiff -u -b $expected_output $tmp_file\n description = TEST scope $scope of file $tested_file with the $catala_cmd command\n\nrule test_without_scope\n command = catala $catala_cmd $tested_file $extra_flags --unstyled 2>&1 | colordiff -u -b $expected_output -\n description = TEST on file $tested_file with the $catala_cmd command\n\nrule test_without_scope_and_output\n command = catala $catala_cmd $tested_file $extra_flags --unstyled -o $tmp_file ; colordiff -u -b $expected_output $tmp_file\n description = TEST on file $tested_file with the $catala_cmd command\n\n"[@ocamlformat "disable"]
|
||||
"rule reset_with_scope\n command = catala -s $scope $catala_cmd $tested_file $extra_flags --unstyled > $expected_output 2>&1 | true\n description = RESET scope $scope of file $tested_file with the $catala_cmd command\n\nrule reset_with_scope_and_output\n command = catala -s $scope $catala_cmd $tested_file $extra_flags --unstyled -o $expected_output 2>&1 | true\n description = RESET scope $scope of file $tested_file with the $catala_cmd command\n\nrule reset_without_scope\n command = catala $catala_cmd $tested_file $extra_flags --unstyled > $expected_output 2>&1 | true\n description = RESET file $tested_file with the $catala_cmd command\n\nrule reset_without_scope_and_output\n command = catala $catala_cmd $tested_file $extra_flags --unstyled -o $expected_output 2>&1 | true\n description = RESET file $tested_file with the $catala_cmd command\n\nrule run_and_display_final_message\n command = :\n description = All tests $test_file_or_folder passed!\n\nrule test_with_scope\n command = catala -s $scope $catala_cmd $tested_file $extra_flags --unstyled 2>&1 | colordiff -u -b $expected_output -\n description = TEST scope $scope of file $tested_file with the $catala_cmd command\n\nrule test_with_scope_and_output\n command = catala -s $scope $catala_cmd $tested_file $extra_flags --unstyled -o $tmp_file ; colordiff -u -b $expected_output $tmp_file\n description = TEST scope $scope of file $tested_file with the $catala_cmd command\n\nrule test_without_scope\n command = catala $catala_cmd $tested_file $extra_flags --unstyled 2>&1 | colordiff -u -b $expected_output -\n description = TEST on file $tested_file with the $catala_cmd command\n\nrule test_without_scope_and_output\n command = catala $catala_cmd $tested_file $extra_flags --unstyled -o $tmp_file ; colordiff -u -b $expected_output $tmp_file\n description = TEST on file $tested_file with the $catala_cmd command\n\n"[@ocamlformat "disable"]
|
||||
in
|
||||
let actual_format = Buffer.contents Format.stdbuf in
|
||||
Al.(check string)
|
||||
|
@ -1,6 +1,7 @@
|
||||
(* This file is part of the Catala compiler, a specification language for tax
|
||||
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
|
||||
Denis Merigoux <denis.merigoux@inria.fr>
|
||||
Denis Merigoux <denis.merigoux@inria.fr>, Alain Delaët-Tixeuil
|
||||
<alain.delaet--tixeuil@inria.fr>
|
||||
|
||||
Licensed under the Apache License, Version 2.0 (the "License"); you may not
|
||||
use this file except in compliance with the License. You may obtain a copy of
|
||||
@ -133,26 +134,49 @@ type scope_let_kind =
|
||||
| Assertion
|
||||
|
||||
type scope_let = {
|
||||
scope_let_var : expr Bindlib.var Pos.marked;
|
||||
scope_let_kind : scope_let_kind;
|
||||
scope_let_typ : typ Pos.marked;
|
||||
scope_let_expr : expr Pos.marked Bindlib.box;
|
||||
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_pos : Utils.Pos.t;
|
||||
}
|
||||
|
||||
and scope_body_expr = Result of expr Utils.Pos.marked | ScopeLet of scope_let
|
||||
|
||||
type scope_body = {
|
||||
scope_body_lets : scope_let list;
|
||||
scope_body_result : expr Pos.marked Bindlib.box;
|
||||
(** {x1 = x1; x2 = x2; x3 = x3; ... } *)
|
||||
scope_body_arg : expr Bindlib.var; (** x: input_struct *)
|
||||
scope_body_input_struct : StructName.t;
|
||||
scope_body_output_struct : StructName.t;
|
||||
scope_body_expr : (expr, scope_body_expr) Bindlib.binder;
|
||||
}
|
||||
|
||||
type program = {
|
||||
decl_ctx : decl_ctx;
|
||||
scopes : (ScopeName.t * expr Bindlib.var * scope_body) list;
|
||||
type scope_def = {
|
||||
scope_name : ScopeName.t;
|
||||
scope_body : scope_body;
|
||||
scope_next : (expr, scopes) Bindlib.binder;
|
||||
}
|
||||
|
||||
and scopes = Nil | ScopeDef of scope_def
|
||||
|
||||
type program = { decl_ctx : decl_ctx; scopes : scopes }
|
||||
|
||||
let rec fold_scope_lets
|
||||
~(f : 'a -> scope_let -> 'a)
|
||||
~(init : 'a)
|
||||
(scope_body_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 rec fold_scope_defs
|
||||
~(f : 'a -> scope_def -> 'a) ~(init : 'a) (scopes : 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
|
||||
|
||||
module Var = struct
|
||||
type t = expr Bindlib.var
|
||||
|
||||
@ -164,36 +188,110 @@ module Var = struct
|
||||
let compare x y = Bindlib.compare_vars x y
|
||||
end
|
||||
|
||||
module VarMap = Map.Make (Var)
|
||||
|
||||
let union : unit VarMap.t -> unit VarMap.t -> unit VarMap.t =
|
||||
VarMap.union (fun _ _ _ -> Some ())
|
||||
|
||||
let rec free_vars_set (e : expr Pos.marked) : unit VarMap.t =
|
||||
(** 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, _) -> VarMap.singleton v ()
|
||||
| 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)
|
||||
|
||||
let rec free_vars_expr (e : expr Pos.marked) : VarSet.t =
|
||||
match Pos.unmark e with
|
||||
| EVar (v, _) -> VarSet.singleton v
|
||||
| ETuple (es, _) | EArray es ->
|
||||
es |> List.map free_vars_set |> List.fold_left union VarMap.empty
|
||||
es |> List.map free_vars_expr |> List.fold_left VarSet.union VarSet.empty
|
||||
| ETupleAccess (e1, _, _, _)
|
||||
| EAssert e1
|
||||
| ErrorOnEmpty e1
|
||||
| EInj (e1, _, _, _) ->
|
||||
free_vars_set e1
|
||||
free_vars_expr e1
|
||||
| EApp (e1, es) | EMatch (e1, es, _) ->
|
||||
e1 :: es |> List.map free_vars_set |> List.fold_left union VarMap.empty
|
||||
e1 :: es |> List.map free_vars_expr
|
||||
|> List.fold_left VarSet.union VarSet.empty
|
||||
| EDefault (es, ejust, econs) ->
|
||||
ejust :: econs :: es |> List.map free_vars_set
|
||||
|> List.fold_left union VarMap.empty
|
||||
| EOp _ | ELit _ -> VarMap.empty
|
||||
ejust :: econs :: es |> List.map free_vars_expr
|
||||
|> List.fold_left VarSet.union VarSet.empty
|
||||
| EOp _ | ELit _ -> VarSet.empty
|
||||
| EIfThenElse (e1, e2, e3) ->
|
||||
[ e1; e2; e3 ] |> List.map free_vars_set
|
||||
|> List.fold_left union VarMap.empty
|
||||
[ e1; e2; e3 ] |> List.map free_vars_expr
|
||||
|> List.fold_left VarSet.union VarSet.empty
|
||||
| EAbs ((binder, _), _) ->
|
||||
let vs, body = Bindlib.unmbind binder in
|
||||
Array.fold_right VarMap.remove vs (free_vars_set body)
|
||||
Array.fold_right VarSet.remove vs (free_vars_expr body)
|
||||
|
||||
let free_vars_list (e : expr Pos.marked) : Var.t list =
|
||||
free_vars_set e |> VarMap.bindings |> List.map fst
|
||||
let rec free_vars_scope_body_expr (scope_lets : scope_body_expr) : VarSet.t =
|
||||
match scope_lets with
|
||||
| Result e -> free_vars_expr e
|
||||
| ScopeLet { scope_let_expr = e; scope_let_next = next; _ } ->
|
||||
let v, body = Bindlib.unbind next in
|
||||
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 { 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 =
|
||||
match scopes with
|
||||
| Nil -> VarSet.empty
|
||||
| ScopeDef { scope_body = body; scope_next = next; _ } ->
|
||||
let v, next = Bindlib.unbind next in
|
||||
VarSet.union
|
||||
(VarSet.remove v (free_vars_scopes next))
|
||||
(free_vars_scope_body body)
|
||||
|
||||
type vars = expr Bindlib.mvar
|
||||
|
||||
@ -312,19 +410,31 @@ 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 =
|
||||
match scope_let with
|
||||
| Result e -> box_expr e
|
||||
| ScopeLet
|
||||
{
|
||||
scope_let_kind = _;
|
||||
scope_let_typ;
|
||||
scope_let_expr;
|
||||
scope_let_next;
|
||||
scope_let_pos;
|
||||
} ->
|
||||
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)
|
||||
scope_let_pos
|
||||
|
||||
let build_whole_scope_expr
|
||||
(ctx : decl_ctx) (body : scope_body) (pos_scope : Pos.t) =
|
||||
let body_expr =
|
||||
List.fold_right
|
||||
(fun scope_let acc ->
|
||||
make_let_in
|
||||
(Pos.unmark scope_let.scope_let_var)
|
||||
scope_let.scope_let_typ scope_let.scope_let_expr acc
|
||||
(Pos.get_position scope_let.scope_let_var))
|
||||
body.scope_body_lets body.scope_body_result
|
||||
in
|
||||
let var, body_expr = Bindlib.unbind body.scope_body_expr in
|
||||
Cli.debug_format "Getting variable %s_%d" (Bindlib.name_of var)
|
||||
(Bindlib.uid_of var);
|
||||
let body_expr = unfold_scope_body_expr ctx body_expr in
|
||||
make_abs
|
||||
(Array.of_list [ body.scope_body_arg ])
|
||||
(Array.of_list [ var ])
|
||||
body_expr pos_scope
|
||||
[
|
||||
( TTuple
|
||||
@ -352,25 +462,36 @@ let build_scope_typ_from_sig
|
||||
in
|
||||
(TArrow (input_typ, result_typ), pos)
|
||||
|
||||
let build_whole_program_expr (p : program) (main_scope : ScopeName.t) =
|
||||
let end_result =
|
||||
make_var
|
||||
(let _, x, _ =
|
||||
List.find
|
||||
(fun (s_name, _, _) -> ScopeName.compare main_scope s_name = 0)
|
||||
p.scopes
|
||||
type scope_name_or_var = ScopeName of ScopeName.t | ScopeVar of Var.t
|
||||
|
||||
let rec unfold_scopes
|
||||
(ctx : decl_ctx) (s : scopes) (main_scope : scope_name_or_var) :
|
||||
expr Pos.marked Bindlib.box =
|
||||
match s with
|
||||
| Nil -> (
|
||||
match main_scope with
|
||||
| ScopeVar v ->
|
||||
Bindlib.box_apply (fun v -> (v, Pos.no_pos)) (Bindlib.box_var v)
|
||||
| ScopeName _ -> failwith "should not happen")
|
||||
| ScopeDef { scope_name; scope_body; scope_next } ->
|
||||
let scope_var, scope_next = Bindlib.unbind scope_next in
|
||||
let scope_pos = Pos.get_position (ScopeName.get_info scope_name) in
|
||||
let main_scope =
|
||||
match main_scope with
|
||||
| ScopeVar v -> ScopeVar v
|
||||
| ScopeName n ->
|
||||
if ScopeName.compare n scope_name = 0 then ScopeVar scope_var
|
||||
else ScopeName n
|
||||
in
|
||||
(x, Pos.no_pos))
|
||||
in
|
||||
List.fold_right
|
||||
(fun (scope_name, scope_var, scope_body) acc ->
|
||||
let pos = Pos.get_position (ScopeName.get_info scope_name) in
|
||||
make_let_in scope_var
|
||||
(build_scope_typ_from_sig p.decl_ctx scope_body.scope_body_input_struct
|
||||
scope_body.scope_body_output_struct pos)
|
||||
(build_whole_scope_expr p.decl_ctx scope_body pos)
|
||||
acc pos)
|
||||
p.scopes end_result
|
||||
(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)
|
||||
scope_pos
|
||||
|
||||
let build_whole_program_expr (p : program) (main_scope : ScopeName.t) =
|
||||
unfold_scopes p.decl_ctx p.scopes (ScopeName main_scope)
|
||||
|
||||
let rec expr_size (e : expr Pos.marked) : int =
|
||||
match Pos.unmark e with
|
||||
@ -396,14 +517,3 @@ 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 variable_types (p : program) : typ Pos.marked VarMap.t =
|
||||
List.fold_left
|
||||
(fun acc (_, _, scope) ->
|
||||
List.fold_left
|
||||
(fun acc scope_let ->
|
||||
VarMap.add
|
||||
(Pos.unmark scope_let.scope_let_var)
|
||||
scope_let.scope_let_typ acc)
|
||||
acc scope.scope_body_lets)
|
||||
VarMap.empty p.scopes
|
||||
|
@ -1,6 +1,7 @@
|
||||
(* This file is part of the Catala compiler, a specification language for tax
|
||||
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
|
||||
Denis Merigoux <denis.merigoux@inria.fr>
|
||||
Denis Merigoux <denis.merigoux@inria.fr>, Alain Delaët-Tixeuil
|
||||
<alain.delaet--tixeuil@inria.fr>
|
||||
|
||||
Licensed under the Apache License, Version 2.0 (the "License"); you may not
|
||||
use this file except in compliance with the License. You may obtain a copy of
|
||||
@ -144,33 +145,52 @@ type scope_let_kind =
|
||||
| Assertion (** [let _ = assert e]*)
|
||||
|
||||
type scope_let = {
|
||||
scope_let_var : expr Bindlib.var Pos.marked;
|
||||
scope_let_kind : scope_let_kind;
|
||||
scope_let_typ : typ Pos.marked;
|
||||
scope_let_expr : expr Pos.marked Bindlib.box;
|
||||
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_pos : Utils.Pos.t;
|
||||
}
|
||||
|
||||
(** 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
|
||||
|
||||
type scope_body = {
|
||||
scope_body_lets : scope_let list;
|
||||
scope_body_result : expr Pos.marked Bindlib.box;
|
||||
scope_body_arg : expr Bindlib.var;
|
||||
scope_body_input_struct : StructName.t;
|
||||
scope_body_output_struct : StructName.t;
|
||||
scope_body_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. *)
|
||||
a result expression that uses the let-binded variables. The first binder is
|
||||
the argument of type [scope_body_input_struct]. *)
|
||||
|
||||
type program = {
|
||||
decl_ctx : decl_ctx;
|
||||
scopes : (ScopeName.t * expr Bindlib.var * scope_body) list;
|
||||
type scope_def = {
|
||||
scope_name : ScopeName.t;
|
||||
scope_body : scope_body;
|
||||
scope_next : (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
|
||||
|
||||
type program = { decl_ctx : decl_ctx; scopes : scopes }
|
||||
|
||||
(** {1 Helpers} *)
|
||||
|
||||
(**{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 fold_scope_defs : f:('a -> scope_def -> 'a) -> init:'a -> scopes -> 'a
|
||||
|
||||
(** {2 Variables}*)
|
||||
|
||||
module Var : sig
|
||||
@ -181,9 +201,12 @@ module Var : sig
|
||||
end
|
||||
|
||||
module VarMap : Map.S with type key = Var.t
|
||||
module VarSet : Set.S with type elt = Var.t
|
||||
|
||||
val free_vars_set : expr Pos.marked -> unit VarMap.t
|
||||
val free_vars_list : expr Pos.marked -> Var.t list
|
||||
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
|
||||
|
||||
type vars = expr Bindlib.mvar
|
||||
|
||||
@ -235,8 +258,3 @@ val build_whole_program_expr :
|
||||
|
||||
val expr_size : expr Pos.marked -> int
|
||||
(** Used by the optimizer to know when to stop *)
|
||||
|
||||
val variable_types : program -> typ Pos.marked VarMap.t
|
||||
(** Traverses all the scopes and retrieves all the types for the variables that
|
||||
may appear in scope or subscope variable definitions, giving them as a big
|
||||
map. *)
|
||||
|
@ -1,146 +0,0 @@
|
||||
(* This file is part of the Catala compiler, a specification language for tax
|
||||
and social benefits computation rules. Copyright (C) 2020-2022 Inria,
|
||||
contributor: Alain Delaët-Tixeuil <alain.delaet--tixeuil@inria.fr>
|
||||
|
||||
Licensed under the Apache License, Version 2.0 (the "License"); you may not
|
||||
use this file except in compliance with the License. You may obtain a copy of
|
||||
the License at
|
||||
|
||||
http://www.apache.org/licenses/LICENSE-2.0
|
||||
|
||||
Unless required by applicable law or agreed to in writing, software
|
||||
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
|
||||
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
|
||||
License for the specific language governing permissions and limitations under
|
||||
the License. *)
|
||||
|
||||
open Utils
|
||||
module D = Ast
|
||||
|
||||
type scope_lets =
|
||||
| Result of D.expr Pos.marked
|
||||
| ScopeLet of {
|
||||
scope_let_kind : D.scope_let_kind;
|
||||
scope_let_typ : D.typ Pos.marked;
|
||||
scope_let_expr : D.expr Pos.marked;
|
||||
scope_let_next : (D.expr, scope_lets) Bindlib.binder;
|
||||
scope_let_pos : Pos.t;
|
||||
}
|
||||
|
||||
type scope_body = {
|
||||
scope_body_input_struct : D.StructName.t;
|
||||
scope_body_output_struct : D.StructName.t;
|
||||
scope_body_result : (D.expr, scope_lets) Bindlib.binder;
|
||||
}
|
||||
|
||||
type scopes =
|
||||
| Nil
|
||||
| ScopeDef of {
|
||||
scope_name : D.ScopeName.t;
|
||||
scope_body : scope_body;
|
||||
scope_next : (D.expr, scopes) Bindlib.binder;
|
||||
}
|
||||
|
||||
let union : unit D.VarMap.t -> unit D.VarMap.t -> unit D.VarMap.t =
|
||||
D.VarMap.union (fun _ _ _ -> Some ())
|
||||
|
||||
let rec free_vars_set_scope_lets (scope_lets : scope_lets) : unit D.VarMap.t =
|
||||
match scope_lets with
|
||||
| Result e -> D.free_vars_set e
|
||||
| ScopeLet { scope_let_expr = e; scope_let_next = next; _ } ->
|
||||
let v, body = Bindlib.unbind next in
|
||||
union (D.free_vars_set e)
|
||||
(D.VarMap.remove v (free_vars_set_scope_lets body))
|
||||
|
||||
let free_vars_set_scope_body (scope_body : scope_body) : unit D.VarMap.t =
|
||||
let { scope_body_result = binder; _ } = scope_body in
|
||||
let v, body = Bindlib.unbind binder in
|
||||
D.VarMap.remove v (free_vars_set_scope_lets body)
|
||||
|
||||
let rec free_vars_set_scopes (scopes : scopes) : unit D.VarMap.t =
|
||||
match scopes with
|
||||
| Nil -> D.VarMap.empty
|
||||
| ScopeDef { scope_body = body; scope_next = next; _ } ->
|
||||
let v, next = Bindlib.unbind next in
|
||||
|
||||
union
|
||||
(D.VarMap.remove v (free_vars_set_scopes next))
|
||||
(free_vars_set_scope_body body)
|
||||
|
||||
let free_vars_list_scope_lets (scope_lets : scope_lets) : D.Var.t list =
|
||||
free_vars_set_scope_lets scope_lets |> D.VarMap.bindings |> List.map fst
|
||||
|
||||
let free_vars_list_scope_body (scope_body : scope_body) : D.Var.t list =
|
||||
free_vars_set_scope_body scope_body |> D.VarMap.bindings |> List.map fst
|
||||
|
||||
let free_vars_list_scopes (scopes : scopes) : D.Var.t list =
|
||||
free_vars_set_scopes scopes |> D.VarMap.bindings |> List.map fst
|
||||
|
||||
(** Actual transformation for scopes. *)
|
||||
let bind_scope_lets (acc : scope_lets Bindlib.box) (scope_let : D.scope_let) :
|
||||
scope_lets Bindlib.box =
|
||||
let pos = snd scope_let.D.scope_let_var in
|
||||
|
||||
(* Cli.debug_print @@ Format.asprintf "binding let %a. Variable occurs = %b"
|
||||
Print.format_var (fst scope_let.D.scope_let_var) (Bindlib.occur (fst
|
||||
scope_let.D.scope_let_var) acc); *)
|
||||
let binder = Bindlib.bind_var (fst scope_let.D.scope_let_var) acc in
|
||||
Bindlib.box_apply2
|
||||
(fun expr binder ->
|
||||
(* Cli.debug_print @@ Format.asprintf "free variables in expression: %a"
|
||||
(Format.pp_print_list Print.format_var) (D.free_vars_list expr); *)
|
||||
ScopeLet
|
||||
{
|
||||
scope_let_kind = scope_let.D.scope_let_kind;
|
||||
scope_let_typ = scope_let.D.scope_let_typ;
|
||||
scope_let_expr = expr;
|
||||
scope_let_next = binder;
|
||||
scope_let_pos = pos;
|
||||
})
|
||||
scope_let.D.scope_let_expr binder
|
||||
|
||||
let bind_scope_body (body : D.scope_body) : scope_body Bindlib.box =
|
||||
(* it is a fold_right and not a fold_left. *)
|
||||
let body_result =
|
||||
ListLabels.fold_right body.D.scope_body_lets
|
||||
~init:(Bindlib.box_apply (fun e -> Result e) body.D.scope_body_result)
|
||||
~f:(Fun.flip bind_scope_lets)
|
||||
in
|
||||
|
||||
(* Cli.debug_print @@ Format.asprintf "binding arg %a" Print.format_var
|
||||
body.D.scope_body_arg; *)
|
||||
let scope_body_result = Bindlib.bind_var body.D.scope_body_arg body_result in
|
||||
|
||||
(* Cli.debug_print @@ Format.asprintf "isfinal term is closed: %b"
|
||||
(Bindlib.is_closed scope_body_result); *)
|
||||
Bindlib.box_apply
|
||||
(fun scope_body_result ->
|
||||
(* Cli.debug_print @@ Format.asprintf "rank of the final term: %i"
|
||||
(Bindlib.binder_rank scope_body_result); *)
|
||||
{
|
||||
scope_body_output_struct = body.D.scope_body_output_struct;
|
||||
scope_body_input_struct = body.D.scope_body_input_struct;
|
||||
scope_body_result;
|
||||
})
|
||||
scope_body_result
|
||||
|
||||
let bind_scope
|
||||
((scope_name, scope_var, scope_body) :
|
||||
D.ScopeName.t * D.expr Bindlib.var * D.scope_body)
|
||||
(acc : scopes Bindlib.box) : scopes Bindlib.box =
|
||||
Bindlib.box_apply2
|
||||
(fun scope_body scope_next ->
|
||||
ScopeDef { scope_name; scope_body; scope_next })
|
||||
(bind_scope_body scope_body)
|
||||
(Bindlib.bind_var scope_var acc)
|
||||
|
||||
let bind_scopes
|
||||
(scopes : (D.ScopeName.t * D.expr Bindlib.var * D.scope_body) list) :
|
||||
scopes Bindlib.box =
|
||||
let result =
|
||||
ListLabels.fold_right scopes ~init:(Bindlib.box Nil) ~f:bind_scope
|
||||
in
|
||||
(* Cli.debug_print @@ Format.asprintf "free variable in the program : [%a]"
|
||||
(Format.pp_print_list Print.format_var) (free_vars_list_scopes
|
||||
(Bindlib.unbox result)); *)
|
||||
result
|
@ -1,68 +0,0 @@
|
||||
(* This file is part of the Catala compiler, a specification language for tax
|
||||
and social benefits computation rules. Copyright (C) 2020-2022 Inria,
|
||||
contributor: Alain Delaët-Tixeuil <alain.delaet--tixeuil@inria.fr>
|
||||
|
||||
Licensed under the Apache License, Version 2.0 (the "License"); you may not
|
||||
use this file except in compliance with the License. You may obtain a copy of
|
||||
the License at
|
||||
|
||||
http://www.apache.org/licenses/LICENSE-2.0
|
||||
|
||||
Unless required by applicable law or agreed to in writing, software
|
||||
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
|
||||
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
|
||||
License for the specific language governing permissions and limitations under
|
||||
the License. *)
|
||||
|
||||
module D = Ast
|
||||
|
||||
(** Alternative representation of the Dcalc Ast. It is currently used in the
|
||||
transformation without exceptions. We make heavy use of bindlib, binding
|
||||
each scope-let-variable and each scope explicitly. *)
|
||||
|
||||
(** In [Ast], [Ast.scope_lets] is defined as a list of kind, var, and boxed
|
||||
expression. This representation binds using bindlib the tail of the list
|
||||
with the variable defined in the let. *)
|
||||
type scope_lets =
|
||||
| Result of D.expr Utils.Pos.marked
|
||||
| ScopeLet of {
|
||||
scope_let_kind : D.scope_let_kind;
|
||||
scope_let_typ : D.typ Utils.Pos.marked;
|
||||
scope_let_expr : D.expr Utils.Pos.marked;
|
||||
scope_let_next : (D.expr, scope_lets) Bindlib.binder;
|
||||
scope_let_pos : Utils.Pos.t;
|
||||
}
|
||||
|
||||
type scope_body = {
|
||||
scope_body_input_struct : D.StructName.t;
|
||||
scope_body_output_struct : D.StructName.t;
|
||||
scope_body_result : (D.expr, scope_lets) Bindlib.binder;
|
||||
}
|
||||
(** As a consequence, the scope_body contains only a result and input/output
|
||||
signature, as the other elements are stored inside the scope_let. The binder
|
||||
present is the argument of type [scope_body_input_struct]. *)
|
||||
|
||||
(** Finally, we do the same transformation for the whole program for the kinded
|
||||
lets. This permit us to use bindlib variables for scopes names. *)
|
||||
type scopes =
|
||||
| Nil
|
||||
| ScopeDef of {
|
||||
scope_name : D.ScopeName.t;
|
||||
scope_body : scope_body;
|
||||
scope_next : (D.expr, scopes) Bindlib.binder;
|
||||
}
|
||||
|
||||
val free_vars_list_scope_lets : scope_lets -> D.Var.t list
|
||||
(** List of variables not binded inside a scope_lets *)
|
||||
|
||||
val free_vars_list_scope_body : scope_body -> D.Var.t list
|
||||
(** List of variables not binded inside a scope_body. *)
|
||||
|
||||
val free_vars_list_scopes : scopes -> D.Var.t list
|
||||
(** List of variables not binded inside scopes*)
|
||||
|
||||
val bind_scopes :
|
||||
(D.ScopeName.t * D.expr Bindlib.var * D.scope_body) list -> scopes Bindlib.box
|
||||
(** Transform a list of scopes into our representation of scopes. It requires
|
||||
that scopes are topologically-well-ordered, and ensure there is no free
|
||||
variables in the returned [scopes] *)
|
@ -458,7 +458,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) :
|
||||
| ErrorOnEmpty e' ->
|
||||
let e' = evaluate_expr ctx e' in
|
||||
if Pos.unmark e' = A.ELit LEmptyError then
|
||||
Errors.raise_spanned_error (Pos.get_position e)
|
||||
Errors.raise_spanned_error (Pos.get_position e')
|
||||
"This variable evaluated to an empty term (no rule that defined it \
|
||||
applied in this situation)"
|
||||
else e'
|
||||
|
@ -190,38 +190,71 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked)
|
||||
let optimize_expr (decl_ctx : decl_ctx) (e : expr Pos.marked) =
|
||||
partial_evaluation { var_values = VarMap.empty; decl_ctx } e
|
||||
|
||||
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 =
|
||||
match scope_body_expr with
|
||||
| Result e -> Bindlib.box_apply (fun e' -> Result e') (t ctx e)
|
||||
| ScopeLet scope_let ->
|
||||
let var, next = Bindlib.unbind scope_let.scope_let_next in
|
||||
let new_scope_let_expr = t ctx scope_let.scope_let_expr in
|
||||
let new_next = scope_lets_map t ctx next in
|
||||
let new_next = Bindlib.bind_var var new_next in
|
||||
Bindlib.box_apply2
|
||||
(fun new_scope_let_expr new_next ->
|
||||
ScopeLet
|
||||
{
|
||||
scope_let with
|
||||
scope_let_expr = new_scope_let_expr;
|
||||
scope_let_next = new_next;
|
||||
})
|
||||
new_scope_let_expr new_next
|
||||
|
||||
let rec scopes_map
|
||||
(t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box)
|
||||
(ctx : 'a)
|
||||
(scopes : scopes) : scopes Bindlib.box =
|
||||
match scopes with
|
||||
| Nil -> Bindlib.box Nil
|
||||
| ScopeDef scope_def ->
|
||||
let scope_var, scope_next = Bindlib.unbind scope_def.scope_next in
|
||||
let scope_arg_var, scope_body_expr =
|
||||
Bindlib.unbind scope_def.scope_body.scope_body_expr
|
||||
in
|
||||
let new_scope_body_expr = scope_lets_map t ctx scope_body_expr in
|
||||
let new_scope_body_expr =
|
||||
Bindlib.bind_var scope_arg_var new_scope_body_expr
|
||||
in
|
||||
let new_scope_next = scopes_map t ctx scope_next in
|
||||
let new_scope_next = Bindlib.bind_var scope_var new_scope_next in
|
||||
Bindlib.box_apply2
|
||||
(fun new_scope_body_expr new_scope_next ->
|
||||
ScopeDef
|
||||
{
|
||||
scope_def with
|
||||
scope_next = new_scope_next;
|
||||
scope_body =
|
||||
{
|
||||
scope_def.scope_body with
|
||||
scope_body_expr = new_scope_body_expr;
|
||||
};
|
||||
})
|
||||
new_scope_body_expr new_scope_next
|
||||
|
||||
let program_map
|
||||
(t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box)
|
||||
(ctx : 'a)
|
||||
(p : program) : program =
|
||||
{
|
||||
p with
|
||||
scopes =
|
||||
List.map
|
||||
(fun (s_name, s_var, s_body) ->
|
||||
let new_s_body =
|
||||
{
|
||||
s_body with
|
||||
scope_body_lets =
|
||||
List.map
|
||||
(fun scope_let ->
|
||||
{
|
||||
scope_let with
|
||||
scope_let_expr =
|
||||
Bindlib.unbox
|
||||
(Bindlib.box_apply (t ctx) scope_let.scope_let_expr);
|
||||
})
|
||||
s_body.scope_body_lets;
|
||||
}
|
||||
in
|
||||
(s_name, s_var, new_s_body))
|
||||
p.scopes;
|
||||
}
|
||||
(p : program) : program Bindlib.box =
|
||||
Bindlib.box_apply
|
||||
(fun new_scopes -> { p with scopes = new_scopes })
|
||||
(scopes_map t ctx p.scopes)
|
||||
|
||||
let optimize_program (p : program) : program =
|
||||
program_map partial_evaluation
|
||||
Bindlib.unbox
|
||||
(program_map partial_evaluation
|
||||
{ var_values = VarMap.empty; decl_ctx = p.decl_ctx }
|
||||
p
|
||||
p)
|
||||
|
||||
let rec remove_all_logs (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
|
||||
let pos = Pos.get_position e in
|
||||
|
@ -215,10 +215,17 @@ let driver source_file (options : Cli.options) : int =
|
||||
if Option.is_some options.ex_scope then
|
||||
Format.fprintf fmt "%a\n"
|
||||
(Dcalc.Print.format_scope ~debug:options.debug prgm.decl_ctx)
|
||||
(let _, _, s =
|
||||
List.find (fun (name, _, _) -> name = scope_uid) prgm.scopes
|
||||
in
|
||||
(scope_uid, s))
|
||||
( scope_uid,
|
||||
Option.get
|
||||
(Dcalc.Ast.fold_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"
|
||||
(Dcalc.Print.format_expr prgm.decl_ctx)
|
||||
@ -228,8 +235,8 @@ let driver source_file (options : Cli.options) : int =
|
||||
end;
|
||||
Cli.debug_print "Typechecking...";
|
||||
let _typ = Dcalc.Typing.infer_type prgm.decl_ctx prgrm_dcalc_expr in
|
||||
(* Cli.debug_print (Format.asprintf "Typechecking results :@\n%a"
|
||||
(Dcalc.Print.format_typ prgm.decl_ctx) typ); *)
|
||||
(* Cli.debug_format "Typechecking results :@\n%a"
|
||||
(Dcalc.Print.format_typ prgm.decl_ctx) typ; *)
|
||||
match backend with
|
||||
| Cli.Typecheck ->
|
||||
(* That's it! *)
|
||||
@ -242,7 +249,7 @@ let driver source_file (options : Cli.options) : int =
|
||||
| None -> None
|
||||
| Some _ -> Some scope_uid)
|
||||
in
|
||||
Verification.Solver.solve_vc prgm prgm.decl_ctx vcs;
|
||||
Verification.Solver.solve_vc prgm.decl_ctx vcs;
|
||||
0
|
||||
| Cli.Interpret ->
|
||||
Cli.debug_print "Starting interpretation...";
|
||||
@ -288,6 +295,23 @@ let driver source_file (options : Cli.options) : int =
|
||||
end
|
||||
else prgm
|
||||
in
|
||||
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 = 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
|
||||
if backend = Cli.Lcalc then begin
|
||||
let fmt, at_end =
|
||||
match options.output_file with
|
||||
|
@ -62,6 +62,7 @@ module Var = struct
|
||||
end
|
||||
|
||||
module VarMap = Map.Make (Var)
|
||||
module VarSet = Set.Make (Var)
|
||||
|
||||
type vars = expr Bindlib.mvar
|
||||
|
||||
@ -90,9 +91,16 @@ let make_let_in
|
||||
(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
|
||||
|
||||
make_app (make_abs (Array.of_list [ x ]) e2 pos [ tau ] pos) [ e1 ] pos
|
||||
|
||||
let make_multiple_let_in
|
||||
(xs : Var.t array)
|
||||
(taus : D.typ Pos.marked list)
|
||||
(e1 : expr Pos.marked Bindlib.box list)
|
||||
(e2 : expr Pos.marked Bindlib.box)
|
||||
(pos : Pos.t) : expr Pos.marked Bindlib.box =
|
||||
make_app (make_abs xs e2 pos taus pos) e1 pos
|
||||
|
||||
let ( let+ ) x f = Bindlib.box_apply f x
|
||||
let ( and+ ) x y = Bindlib.box_pair x y
|
||||
let option_enum : D.EnumName.t = D.EnumName.fresh ("eoption", Pos.no_pos)
|
||||
|
@ -74,6 +74,7 @@ module Var : sig
|
||||
end
|
||||
|
||||
module VarMap : Map.S with type key = Var.t
|
||||
module VarSet : Set.S with type elt = Var.t
|
||||
|
||||
type vars = expr Bindlib.mvar
|
||||
|
||||
@ -100,6 +101,14 @@ val make_let_in :
|
||||
expr Pos.marked Bindlib.box ->
|
||||
expr Pos.marked Bindlib.box
|
||||
|
||||
val make_multiple_let_in :
|
||||
Var.t array ->
|
||||
Dcalc.Ast.typ Pos.marked list ->
|
||||
expr Pos.marked Bindlib.box list ->
|
||||
expr Pos.marked Bindlib.box ->
|
||||
Pos.t ->
|
||||
expr Pos.marked Bindlib.box
|
||||
|
||||
val option_enum : Dcalc.Ast.EnumName.t
|
||||
val none_constr : Dcalc.Ast.EnumConstructor.t
|
||||
val some_constr : Dcalc.Ast.EnumConstructor.t
|
||||
|
318
compiler/lcalc/closure_conversion.ml
Normal file
318
compiler/lcalc/closure_conversion.ml
Normal file
@ -0,0 +1,318 @@
|
||||
(* This file is part of the Catala compiler, a specification language for tax
|
||||
and social benefits computation rules. Copyright (C) 2022 Inria, contributor:
|
||||
Denis Merigoux <denis.merigoux@inria.fr>
|
||||
|
||||
Licensed under the Apache License, Version 2.0 (the "License"); you may not
|
||||
use this file except in compliance with the License. You may obtain a copy of
|
||||
the License at
|
||||
|
||||
http://www.apache.org/licenses/LICENSE-2.0
|
||||
|
||||
Unless required by applicable law or agreed to in writing, software
|
||||
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
|
||||
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
|
||||
License for the specific language governing permissions and limitations under
|
||||
the License. *)
|
||||
|
||||
open Ast
|
||||
open Utils
|
||||
|
||||
(** TODO: This version is not yet debugged and ought to be specialized when
|
||||
Lcalc has more structure. *)
|
||||
|
||||
type closure = { name : Var.t; expr : expr Pos.marked Bindlib.box }
|
||||
type ctx = { name_context : string; globally_bound_vars : VarSet.t }
|
||||
|
||||
(** Returns the expression with closed closures and the set of free variables
|
||||
inside this new expression. Implementation guided by
|
||||
http://gallium.inria.fr/~fpottier/mpri/cours04.pdf#page=9. *)
|
||||
let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
|
||||
expr Pos.marked Bindlib.box * VarSet.t =
|
||||
match Pos.unmark e with
|
||||
| EVar v ->
|
||||
( Bindlib.box_apply
|
||||
(fun new_v -> (new_v, Pos.get_position v))
|
||||
(Bindlib.box_var (Pos.unmark v)),
|
||||
VarSet.diff (VarSet.singleton (Pos.unmark v)) ctx.globally_bound_vars )
|
||||
| ETuple (args, s) ->
|
||||
let new_args, free_vars =
|
||||
List.fold_left
|
||||
(fun (new_args, free_vars) arg ->
|
||||
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
|
||||
(new_arg :: new_args, VarSet.union new_free_vars free_vars))
|
||||
([], VarSet.empty) args
|
||||
in
|
||||
( Bindlib.box_apply
|
||||
(fun new_args -> (ETuple (List.rev new_args, s), Pos.get_position e))
|
||||
(Bindlib.box_list new_args),
|
||||
free_vars )
|
||||
| ETupleAccess (e1, n, s, typs) ->
|
||||
let new_e1, free_vars = closure_conversion_expr ctx e1 in
|
||||
( Bindlib.box_apply
|
||||
(fun new_e1 ->
|
||||
(ETupleAccess (new_e1, n, s, typs), Pos.get_position e))
|
||||
new_e1,
|
||||
free_vars )
|
||||
| EInj (e1, n, e_name, typs) ->
|
||||
let new_e1, free_vars = closure_conversion_expr ctx e1 in
|
||||
( Bindlib.box_apply
|
||||
(fun new_e1 -> (EInj (new_e1, n, e_name, typs), Pos.get_position e))
|
||||
new_e1,
|
||||
free_vars )
|
||||
| EMatch (e1, arms, e_name) ->
|
||||
let new_e1, free_vars = closure_conversion_expr ctx e1 in
|
||||
(* We do not close the clotures inside the arms of the match expression,
|
||||
since they get a special treatment at compilation to Scalc. *)
|
||||
let new_arms, free_vars =
|
||||
List.fold_right
|
||||
(fun arm (new_arms, free_vars) ->
|
||||
match Pos.unmark arm with
|
||||
| EAbs ((binder, binder_pos), typs) ->
|
||||
let vars, body = Bindlib.unmbind binder in
|
||||
let new_body, new_free_vars =
|
||||
closure_conversion_expr ctx body
|
||||
in
|
||||
let new_binder = Bindlib.bind_mvar vars new_body in
|
||||
( Bindlib.box_apply
|
||||
(fun new_binder ->
|
||||
( EAbs ((new_binder, binder_pos), typs),
|
||||
Pos.get_position arm ))
|
||||
new_binder
|
||||
:: new_arms,
|
||||
VarSet.union free_vars new_free_vars )
|
||||
| _ -> failwith "should not happen")
|
||||
arms ([], free_vars)
|
||||
in
|
||||
( Bindlib.box_apply2
|
||||
(fun new_e1 new_arms ->
|
||||
(EMatch (new_e1, new_arms, e_name), Pos.get_position e))
|
||||
new_e1
|
||||
(Bindlib.box_list new_arms),
|
||||
free_vars )
|
||||
| EArray args ->
|
||||
let new_args, free_vars =
|
||||
List.fold_right
|
||||
(fun arg (new_args, free_vars) ->
|
||||
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
|
||||
(new_arg :: new_args, VarSet.union free_vars new_free_vars))
|
||||
args ([], VarSet.empty)
|
||||
in
|
||||
( Bindlib.box_apply
|
||||
(fun new_args -> (EArray new_args, Pos.get_position e))
|
||||
(Bindlib.box_list new_args),
|
||||
free_vars )
|
||||
| ELit l -> (Bindlib.box (ELit l, Pos.get_position e), VarSet.empty)
|
||||
| EApp ((EAbs ((binder, binder_pos), typs_abs), e1_pos), args) ->
|
||||
(* let-binding, we should not close these *)
|
||||
let vars, body = Bindlib.unmbind binder in
|
||||
let new_body, free_vars = closure_conversion_expr ctx body in
|
||||
let new_binder = Bindlib.bind_mvar vars new_body in
|
||||
let new_args, free_vars =
|
||||
List.fold_right
|
||||
(fun arg (new_args, free_vars) ->
|
||||
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
|
||||
(new_arg :: new_args, VarSet.union free_vars new_free_vars))
|
||||
args ([], free_vars)
|
||||
in
|
||||
( Bindlib.box_apply2
|
||||
(fun new_binder new_args ->
|
||||
( EApp
|
||||
((EAbs ((new_binder, binder_pos), typs_abs), e1_pos), new_args),
|
||||
Pos.get_position e ))
|
||||
new_binder
|
||||
(Bindlib.box_list new_args),
|
||||
free_vars )
|
||||
| EAbs ((binder, binder_pos), typs) ->
|
||||
(* λ x.t *)
|
||||
(* Converting the closure. *)
|
||||
let vars, body = Bindlib.unmbind binder in
|
||||
(* t *)
|
||||
let new_body, body_vars = closure_conversion_expr ctx body in
|
||||
(* [[t]] *)
|
||||
let extra_vars =
|
||||
VarSet.diff body_vars (VarSet.of_list (Array.to_list vars))
|
||||
in
|
||||
let extra_vars_list = VarSet.elements extra_vars in
|
||||
(* x1, ..., xn *)
|
||||
let code_var = Var.make (ctx.name_context, binder_pos) in
|
||||
(* code *)
|
||||
let inner_c_var = Var.make ("env", binder_pos) in
|
||||
let new_closure_body =
|
||||
make_multiple_let_in
|
||||
(Array.of_list extra_vars_list)
|
||||
(List.init (List.length extra_vars_list) (fun _ ->
|
||||
(Dcalc.Ast.TAny, binder_pos)))
|
||||
(List.mapi
|
||||
(fun i _ ->
|
||||
Bindlib.box_apply
|
||||
(fun inner_c_var ->
|
||||
( ETupleAccess
|
||||
( (inner_c_var, binder_pos),
|
||||
i + 1,
|
||||
None,
|
||||
List.init
|
||||
(List.length extra_vars_list + 1)
|
||||
(fun _ -> (Dcalc.Ast.TAny, binder_pos)) ),
|
||||
binder_pos ))
|
||||
(Bindlib.box_var inner_c_var))
|
||||
extra_vars_list)
|
||||
new_body binder_pos
|
||||
in
|
||||
let new_closure =
|
||||
make_abs
|
||||
(Array.concat [ Array.make 1 inner_c_var; vars ])
|
||||
new_closure_body binder_pos
|
||||
((Dcalc.Ast.TAny, binder_pos) :: typs)
|
||||
(Pos.get_position e)
|
||||
in
|
||||
( make_let_in code_var
|
||||
(Dcalc.Ast.TAny, Pos.get_position e)
|
||||
new_closure
|
||||
(Bindlib.box_apply2
|
||||
(fun code_var extra_vars ->
|
||||
( ETuple
|
||||
( (code_var, binder_pos)
|
||||
:: List.map
|
||||
(fun extra_var -> (extra_var, binder_pos))
|
||||
extra_vars,
|
||||
None ),
|
||||
Pos.get_position e ))
|
||||
(Bindlib.box_var code_var)
|
||||
(Bindlib.box_list
|
||||
(List.map
|
||||
(fun extra_var -> Bindlib.box_var extra_var)
|
||||
extra_vars_list))),
|
||||
extra_vars )
|
||||
| EApp ((EOp op, pos_op), args) ->
|
||||
(* This corresponds to an operator call, which we don't want to
|
||||
transform*)
|
||||
let new_args, free_vars =
|
||||
List.fold_right
|
||||
(fun arg (new_args, free_vars) ->
|
||||
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
|
||||
(new_arg :: new_args, VarSet.union free_vars new_free_vars))
|
||||
args ([], VarSet.empty)
|
||||
in
|
||||
( Bindlib.box_apply
|
||||
(fun new_e2 -> (EApp ((EOp op, pos_op), new_e2), Pos.get_position e))
|
||||
(Bindlib.box_list new_args),
|
||||
free_vars )
|
||||
| EApp ((EVar (v, _), v_pos), args) when VarSet.mem v ctx.globally_bound_vars
|
||||
->
|
||||
(* This corresponds to a scope call, which we don't want to transform*)
|
||||
let new_args, free_vars =
|
||||
List.fold_right
|
||||
(fun arg (new_args, free_vars) ->
|
||||
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
|
||||
(new_arg :: new_args, VarSet.union free_vars new_free_vars))
|
||||
args ([], VarSet.empty)
|
||||
in
|
||||
( Bindlib.box_apply2
|
||||
(fun new_v new_e2 ->
|
||||
(EApp ((new_v, v_pos), new_e2), Pos.get_position e))
|
||||
(Bindlib.box_var v)
|
||||
(Bindlib.box_list new_args),
|
||||
free_vars )
|
||||
| EApp (e1, args) ->
|
||||
let new_e1, free_vars = closure_conversion_expr ctx e1 in
|
||||
let env_var = Var.make ("env", Pos.get_position e1) in
|
||||
let code_var = Var.make ("code", Pos.get_position e1) in
|
||||
let new_args, free_vars =
|
||||
List.fold_right
|
||||
(fun arg (new_args, free_vars) ->
|
||||
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
|
||||
(new_arg :: new_args, VarSet.union free_vars new_free_vars))
|
||||
args ([], free_vars)
|
||||
in
|
||||
let call_expr =
|
||||
make_let_in code_var
|
||||
(Dcalc.Ast.TAny, Pos.get_position e)
|
||||
(Bindlib.box_apply
|
||||
(fun env_var ->
|
||||
( ETupleAccess
|
||||
((env_var, Pos.get_position e1), 0, None, [ (*TODO: fill?*) ]),
|
||||
Pos.get_position e ))
|
||||
(Bindlib.box_var env_var))
|
||||
(Bindlib.box_apply3
|
||||
(fun code_var env_var new_args ->
|
||||
( EApp
|
||||
( (code_var, Pos.get_position e1),
|
||||
(env_var, Pos.get_position e1) :: new_args ),
|
||||
Pos.get_position e ))
|
||||
(Bindlib.box_var code_var) (Bindlib.box_var env_var)
|
||||
(Bindlib.box_list new_args))
|
||||
in
|
||||
( make_let_in env_var (Dcalc.Ast.TAny, Pos.get_position e) new_e1 call_expr,
|
||||
free_vars )
|
||||
| EAssert e1 ->
|
||||
let new_e1, free_vars = closure_conversion_expr ctx e1 in
|
||||
( Bindlib.box_apply
|
||||
(fun new_e1 -> (EAssert new_e1, Pos.get_position e))
|
||||
new_e1,
|
||||
free_vars )
|
||||
| EOp op -> (Bindlib.box (EOp op, Pos.get_position e), VarSet.empty)
|
||||
| EIfThenElse (e1, e2, e3) ->
|
||||
let new_e1, free_vars1 = closure_conversion_expr ctx e1 in
|
||||
let new_e2, free_vars2 = closure_conversion_expr ctx e2 in
|
||||
let new_e3, free_vars3 = closure_conversion_expr ctx e3 in
|
||||
( Bindlib.box_apply3
|
||||
(fun new_e1 new_e2 new_e3 ->
|
||||
(EIfThenElse (new_e1, new_e2, new_e3), Pos.get_position e))
|
||||
new_e1 new_e2 new_e3,
|
||||
VarSet.union (VarSet.union free_vars1 free_vars2) free_vars3 )
|
||||
| ERaise except ->
|
||||
(Bindlib.box (ERaise except, Pos.get_position e), VarSet.empty)
|
||||
| ECatch (e1, except, e2) ->
|
||||
let new_e1, free_vars1 = closure_conversion_expr ctx e1 in
|
||||
let new_e2, free_vars2 = closure_conversion_expr ctx e2 in
|
||||
( Bindlib.box_apply2
|
||||
(fun new_e1 new_e2 ->
|
||||
(ECatch (new_e1, except, new_e2), Pos.get_position e))
|
||||
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
|
||||
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 )
|
@ -147,32 +147,33 @@ and translate_expr (ctx : ctx) (e : D.expr Pos.marked) :
|
||||
| D.EDefault (exceptions, just, cons) ->
|
||||
translate_default ctx exceptions just cons (Pos.get_position e)
|
||||
|
||||
let translate_program (prgm : D.program) : A.program =
|
||||
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 =
|
||||
{
|
||||
scopes =
|
||||
(let acc, _ =
|
||||
List.fold_left
|
||||
(fun ((acc, ctx) : _ * A.Var.t D.VarMap.t) (scope_name, n, e) ->
|
||||
let new_n = A.Var.make (Bindlib.name_of n, Pos.no_pos) in
|
||||
let new_acc =
|
||||
{
|
||||
Ast.scope_body_name = scope_name;
|
||||
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 prgm.decl_ctx e
|
||||
(D.build_whole_scope_expr decl_ctx scope_def.scope_body
|
||||
(Pos.get_position
|
||||
(Dcalc.Ast.ScopeName.get_info scope_name)))));
|
||||
(Dcalc.Ast.ScopeName.get_info scope_def.scope_name)))));
|
||||
}
|
||||
:: acc
|
||||
in
|
||||
let new_ctx = D.VarMap.add n new_n ctx in
|
||||
(new_acc, new_ctx))
|
||||
([], D.VarMap.empty) prgm.scopes
|
||||
in
|
||||
List.rev acc);
|
||||
let new_ctx = D.VarMap.add scope_var new_n ctx in
|
||||
new_scope :: translate_scopes decl_ctx new_ctx scope_next
|
||||
|
||||
let translate_program (prgm : D.program) : A.program =
|
||||
{
|
||||
scopes = translate_scopes prgm.decl_ctx D.VarMap.empty prgm.scopes;
|
||||
decl_ctx = prgm.decl_ctx;
|
||||
}
|
||||
|
@ -17,7 +17,6 @@
|
||||
open Utils
|
||||
module D = Dcalc.Ast
|
||||
module A = Ast
|
||||
open Dcalc.Binded_representation
|
||||
|
||||
(** The main idea around this pass is to compile Dcalc to Lcalc without using
|
||||
[raise EmptyError] nor [try _ with EmptyError -> _]. To do so, we use the
|
||||
@ -392,7 +391,7 @@ 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 : scope_lets) =
|
||||
let rec translate_scope_let (ctx : ctx) (lets : D.scope_body_expr) =
|
||||
match lets with
|
||||
| Result e -> translate_expr ~append_esome:false ctx e
|
||||
| ScopeLet
|
||||
@ -484,11 +483,11 @@ let rec translate_scope_let (ctx : ctx) (lets : scope_lets) =
|
||||
(translate_expr ctx ~append_esome:false expr)
|
||||
(translate_scope_let ctx' next)
|
||||
|
||||
let translate_scope_body (scope_pos : Pos.t) (ctx : ctx) (body : scope_body) :
|
||||
let translate_scope_body (scope_pos : Pos.t) (ctx : ctx) (body : D.scope_body) :
|
||||
A.expr Pos.marked Bindlib.box =
|
||||
match body with
|
||||
| {
|
||||
scope_body_result = result;
|
||||
scope_body_expr = result;
|
||||
scope_body_input_struct = input_struct;
|
||||
scope_body_output_struct = _output_struct;
|
||||
} ->
|
||||
@ -502,7 +501,7 @@ let translate_scope_body (scope_pos : Pos.t) (ctx : ctx) (body : scope_body) :
|
||||
[ (D.TTuple ([], Some input_struct), Pos.no_pos) ]
|
||||
Pos.no_pos
|
||||
|
||||
let rec translate_scopes (ctx : ctx) (scopes : scopes) :
|
||||
let rec translate_scopes (ctx : ctx) (scopes : D.scopes) :
|
||||
Ast.scope_body list Bindlib.box =
|
||||
match scopes with
|
||||
| Nil -> Bindlib.box []
|
||||
@ -528,13 +527,13 @@ let rec translate_scopes (ctx : ctx) (scopes : scopes) :
|
||||
:: tail)
|
||||
new_body tail
|
||||
|
||||
let translate_scopes (ctx : ctx) (scopes : scopes) : Ast.scope_body list =
|
||||
let translate_scopes (ctx : ctx) (scopes : D.scopes) : Ast.scope_body list =
|
||||
Bindlib.unbox (translate_scopes ctx scopes)
|
||||
|
||||
let translate_program (prgm : D.program) : A.program =
|
||||
let inputs_structs =
|
||||
ListLabels.fold_left prgm.scopes ~init:[] ~f:(fun acc (_, _, body) ->
|
||||
body.D.scope_body_input_struct :: acc)
|
||||
D.fold_scope_defs prgm.scopes ~init:[] ~f:(fun acc scope_def ->
|
||||
scope_def.D.scope_body.scope_body_input_struct :: acc)
|
||||
in
|
||||
|
||||
(* Cli.debug_print @@ Format.asprintf "List of structs to modify: [%a]"
|
||||
@ -566,8 +565,7 @@ let translate_program (prgm : D.program) : A.program =
|
||||
in
|
||||
|
||||
let scopes =
|
||||
prgm.scopes |> bind_scopes |> Bindlib.unbox
|
||||
|> translate_scopes { decl_ctx; vars = D.VarMap.empty }
|
||||
prgm.scopes |> translate_scopes { decl_ctx; vars = D.VarMap.empty }
|
||||
in
|
||||
|
||||
{ scopes; decl_ctx }
|
||||
|
@ -149,6 +149,15 @@ let rec peephole_expr (_ : unit) (e : expr Pos.marked) :
|
||||
| EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ]) ->
|
||||
e3
|
||||
| _ -> default_mark @@ EIfThenElse (e1, e2, e3))
|
||||
| ECatch (e1, except, e2) -> (
|
||||
let+ e1 = peephole_expr () e1 and+ e2 = peephole_expr () e2 in
|
||||
match (Pos.unmark e1, Pos.unmark e2) with
|
||||
| ERaise except', ERaise except''
|
||||
when except' = except && except = except'' ->
|
||||
default_mark @@ ERaise except
|
||||
| ERaise except', _ when except' = except -> e2
|
||||
| _, ERaise except' when except' = except -> e1
|
||||
| _ -> default_mark @@ ECatch (e1, except, e2))
|
||||
| _ -> visitor_map peephole_expr () e
|
||||
|
||||
let peephole_optimizations (p : program) : program =
|
||||
|
@ -24,6 +24,7 @@ type ctxt = {
|
||||
decl_ctx : D.decl_ctx;
|
||||
var_dict : A.LocalName.t L.VarMap.t;
|
||||
inside_definition_of : A.LocalName.t option;
|
||||
context_name : string;
|
||||
}
|
||||
|
||||
(* Expressions can spill out side effect, hence this function also returns a
|
||||
@ -94,8 +95,26 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Pos.marked) :
|
||||
| L.EOp op -> ([], (A.EOp op, Pos.get_position expr))
|
||||
| L.ELit l -> ([], (A.ELit l, Pos.get_position expr))
|
||||
| _ ->
|
||||
let tmp_var = A.LocalName.fresh ("local_var", Pos.get_position expr) in
|
||||
let ctxt = { ctxt with inside_definition_of = Some tmp_var } in
|
||||
let tmp_var =
|
||||
A.LocalName.fresh
|
||||
( (*This piece of logic is used to make the code more readable. TODO:
|
||||
should be removed when
|
||||
https://github.com/CatalaLang/catala/issues/240 is fixed. *)
|
||||
(match ctxt.inside_definition_of with
|
||||
| None -> ctxt.context_name
|
||||
| Some v ->
|
||||
let v = Pos.unmark (A.LocalName.get_info v) in
|
||||
let tmp_rex = Re.Pcre.regexp "^temp_" in
|
||||
if Re.Pcre.pmatch ~rex:tmp_rex v then v else "temp_" ^ v),
|
||||
Pos.get_position expr )
|
||||
in
|
||||
let ctxt =
|
||||
{
|
||||
ctxt with
|
||||
inside_definition_of = Some tmp_var;
|
||||
context_name = Pos.unmark (A.LocalName.get_info tmp_var);
|
||||
}
|
||||
in
|
||||
let tmp_stmts = translate_statements ctxt expr in
|
||||
( ( A.SLocalDecl
|
||||
((tmp_var, Pos.get_position expr), (D.TAny, Pos.get_position expr)),
|
||||
@ -150,7 +169,11 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Pos.marked) :
|
||||
List.map
|
||||
(fun (x, _tau, arg) ->
|
||||
let ctxt =
|
||||
{ ctxt with inside_definition_of = Some (Pos.unmark x) }
|
||||
{
|
||||
ctxt with
|
||||
inside_definition_of = Some (Pos.unmark x);
|
||||
context_name = Pos.unmark (A.LocalName.get_info (Pos.unmark x));
|
||||
}
|
||||
in
|
||||
let arg_stmts, new_arg = translate_expr ctxt arg in
|
||||
arg_stmts @ [ (A.SLocalDef (x, new_arg), binder_pos) ])
|
||||
@ -165,7 +188,8 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Pos.marked) :
|
||||
in
|
||||
let closure_name =
|
||||
match ctxt.inside_definition_of with
|
||||
| None -> A.LocalName.fresh ("closure", Pos.get_position block_expr)
|
||||
| None ->
|
||||
A.LocalName.fresh (ctxt.context_name, Pos.get_position block_expr)
|
||||
| Some x -> x
|
||||
in
|
||||
let ctxt =
|
||||
@ -258,6 +282,7 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Pos.marked) :
|
||||
])
|
||||
|
||||
let translate_scope
|
||||
(scope_name : D.ScopeName.t)
|
||||
(decl_ctx : D.decl_ctx)
|
||||
(func_dict : A.TopLevelName.t L.VarMap.t)
|
||||
(scope_expr : L.expr Pos.marked) :
|
||||
@ -280,7 +305,13 @@ let translate_scope
|
||||
in
|
||||
let new_body =
|
||||
translate_statements
|
||||
{ decl_ctx; func_dict; var_dict; inside_definition_of = None }
|
||||
{
|
||||
decl_ctx;
|
||||
func_dict;
|
||||
var_dict;
|
||||
inside_definition_of = None;
|
||||
context_name = Pos.unmark (D.ScopeName.get_info scope_name);
|
||||
}
|
||||
body
|
||||
in
|
||||
(param_list, new_body)
|
||||
@ -295,8 +326,8 @@ let translate_program (p : L.program) : A.program =
|
||||
List.fold_left
|
||||
(fun (func_dict, new_scopes) body ->
|
||||
let new_scope_params, new_scope_body =
|
||||
translate_scope p.decl_ctx func_dict
|
||||
body.Lcalc.Ast.scope_body_expr
|
||||
translate_scope body.L.scope_body_name p.decl_ctx func_dict
|
||||
body.L.scope_body_expr
|
||||
in
|
||||
let func_id =
|
||||
A.TopLevelName.fresh
|
||||
|
@ -191,10 +191,46 @@ let format_name_cleaned (fmt : Format.formatter) (s : string) : unit =
|
||||
let lowercase_name = avoid_keywords (to_ascii lowercase_name) in
|
||||
Format.fprintf fmt "%s" lowercase_name
|
||||
|
||||
module StringMap = Map.Make (String)
|
||||
module IntMap = Map.Make (Int)
|
||||
|
||||
(** For each `LocalName.t` defined by its string and then by its hash, we keep
|
||||
track of which local integer id we've given it. This is used to keep
|
||||
variable naming with low indices rather than one global counter for all
|
||||
variables. TODO: should be removed when
|
||||
https://github.com/CatalaLang/catala/issues/240 is fixed. *)
|
||||
let string_counter_map : int IntMap.t StringMap.t ref = ref StringMap.empty
|
||||
|
||||
let format_var (fmt : Format.formatter) (v : LocalName.t) : unit =
|
||||
let v_str = Pos.unmark (LocalName.get_info v) in
|
||||
let hash = LocalName.hash v in
|
||||
let local_id =
|
||||
match StringMap.find_opt v_str !string_counter_map with
|
||||
| Some ids -> (
|
||||
match IntMap.find_opt hash ids with
|
||||
| None ->
|
||||
let max_id =
|
||||
snd
|
||||
(List.hd
|
||||
(List.fast_sort
|
||||
(fun (_, x) (_, y) -> Int.compare y x)
|
||||
(IntMap.bindings ids)))
|
||||
in
|
||||
string_counter_map :=
|
||||
StringMap.add v_str
|
||||
(IntMap.add hash (max_id + 1) ids)
|
||||
!string_counter_map;
|
||||
max_id + 1
|
||||
| Some local_id -> local_id)
|
||||
| None ->
|
||||
string_counter_map :=
|
||||
StringMap.add v_str (IntMap.singleton hash 0) !string_counter_map;
|
||||
0
|
||||
in
|
||||
if v_str = "_" then Format.fprintf fmt "_"
|
||||
else Format.fprintf fmt "%a_%d" format_name_cleaned v_str (LocalName.hash v)
|
||||
(* special case for the unit pattern *)
|
||||
else if local_id = 0 then format_name_cleaned fmt v_str
|
||||
else Format.fprintf fmt "%a_%d" format_name_cleaned v_str local_id
|
||||
|
||||
let format_toplevel_name (fmt : Format.formatter) (v : TopLevelName.t) : unit =
|
||||
let v_str = Pos.unmark (TopLevelName.get_info v) in
|
||||
|
@ -335,14 +335,16 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
|
||||
|
||||
(** The result of a rule translation is a list of assignment, with variables and
|
||||
expressions. We also return the new translation context available after the
|
||||
assignment to use in later rule translations. The list is actually a list of
|
||||
list because we want to group in assignments that are independent of each
|
||||
other to speed up the translation by minimizing Bindlib.bind_mvar *)
|
||||
assignment to use in later rule translations. The list is actually a
|
||||
continuation yielding a [Dcalc.scope_body_expr] by giving it what should
|
||||
come later in the chain of let-bindings. *)
|
||||
let translate_rule
|
||||
(ctx : ctx)
|
||||
(rule : Ast.rule)
|
||||
((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info) :
|
||||
Dcalc.Ast.scope_let list * ctx =
|
||||
(Dcalc.Ast.scope_body_expr Bindlib.box ->
|
||||
Dcalc.Ast.scope_body_expr Bindlib.box)
|
||||
* ctx =
|
||||
match rule with
|
||||
| Definition ((ScopeVar a, var_def_pos), tau, a_io, e) ->
|
||||
let a_name = Ast.ScopeVar.get_info (Pos.unmark a) in
|
||||
@ -367,14 +369,19 @@ let translate_rule
|
||||
(Dcalc.Ast.VarDef (Pos.unmark tau))
|
||||
[ (sigma_name, pos_sigma); a_name ]
|
||||
in
|
||||
( [
|
||||
( (fun next ->
|
||||
Bindlib.box_apply2
|
||||
(fun next merged_expr ->
|
||||
Dcalc.Ast.ScopeLet
|
||||
{
|
||||
Dcalc.Ast.scope_let_var = (a_var, Pos.get_position a);
|
||||
Dcalc.Ast.scope_let_next = next;
|
||||
Dcalc.Ast.scope_let_typ = tau;
|
||||
Dcalc.Ast.scope_let_expr = merged_expr;
|
||||
Dcalc.Ast.scope_let_kind = Dcalc.Ast.ScopeVarDefinition;
|
||||
};
|
||||
],
|
||||
Dcalc.Ast.scope_let_pos = Pos.get_position a;
|
||||
})
|
||||
(Bindlib.bind_var a_var next)
|
||||
merged_expr),
|
||||
{
|
||||
ctx with
|
||||
scope_vars =
|
||||
@ -416,9 +423,13 @@ let translate_rule
|
||||
[ (Dcalc.Ast.TLit TUnit, var_def_pos) ]
|
||||
var_def_pos
|
||||
in
|
||||
( [
|
||||
( (fun next ->
|
||||
Bindlib.box_apply2
|
||||
(fun next thunked_or_nonempty_new_e ->
|
||||
Dcalc.Ast.ScopeLet
|
||||
{
|
||||
Dcalc.Ast.scope_let_var = (a_var, Pos.get_position a_name);
|
||||
Dcalc.Ast.scope_let_next = next;
|
||||
Dcalc.Ast.scope_let_pos = Pos.get_position a_name;
|
||||
Dcalc.Ast.scope_let_typ =
|
||||
(match Pos.unmark a_io.io_input with
|
||||
| NoInput -> failwith "should not happen"
|
||||
@ -428,8 +439,9 @@ let translate_rule
|
||||
var_def_pos ));
|
||||
Dcalc.Ast.scope_let_expr = thunked_or_nonempty_new_e;
|
||||
Dcalc.Ast.scope_let_kind = Dcalc.Ast.SubScopeVarDefinition;
|
||||
};
|
||||
],
|
||||
})
|
||||
(Bindlib.bind_var a_var next)
|
||||
thunked_or_nonempty_new_e),
|
||||
{
|
||||
ctx with
|
||||
subscope_vars =
|
||||
@ -543,24 +555,34 @@ let translate_rule
|
||||
Some called_scope_return_struct ),
|
||||
pos_sigma )
|
||||
in
|
||||
let call_scope_let =
|
||||
let call_scope_let (next : Dcalc.Ast.scope_body_expr Bindlib.box) =
|
||||
Bindlib.box_apply2
|
||||
(fun next call_expr ->
|
||||
Dcalc.Ast.ScopeLet
|
||||
{
|
||||
Dcalc.Ast.scope_let_var = (result_tuple_var, pos_sigma);
|
||||
Dcalc.Ast.scope_let_next = next;
|
||||
Dcalc.Ast.scope_let_pos = pos_sigma;
|
||||
Dcalc.Ast.scope_let_kind = Dcalc.Ast.CallingSubScope;
|
||||
Dcalc.Ast.scope_let_typ = result_tuple_typ;
|
||||
Dcalc.Ast.scope_let_expr = call_expr;
|
||||
}
|
||||
})
|
||||
(Bindlib.bind_var result_tuple_var next)
|
||||
call_expr
|
||||
in
|
||||
let result_bindings_lets =
|
||||
List.mapi
|
||||
(fun i (var_ctx, v) ->
|
||||
let result_bindings_lets (next : Dcalc.Ast.scope_body_expr Bindlib.box) =
|
||||
List.fold_right
|
||||
(fun (var_ctx, v) (next, i) ->
|
||||
( Bindlib.box_apply2
|
||||
(fun next r ->
|
||||
Dcalc.Ast.ScopeLet
|
||||
{
|
||||
Dcalc.Ast.scope_let_var = (v, pos_sigma);
|
||||
Dcalc.Ast.scope_let_typ = (var_ctx.scope_var_typ, pos_sigma);
|
||||
Dcalc.Ast.scope_let_kind = Dcalc.Ast.DestructuringSubScopeResults;
|
||||
Dcalc.Ast.scope_let_next = next;
|
||||
Dcalc.Ast.scope_let_pos = pos_sigma;
|
||||
Dcalc.Ast.scope_let_typ =
|
||||
(var_ctx.scope_var_typ, pos_sigma);
|
||||
Dcalc.Ast.scope_let_kind =
|
||||
Dcalc.Ast.DestructuringSubScopeResults;
|
||||
Dcalc.Ast.scope_let_expr =
|
||||
Bindlib.box_apply
|
||||
(fun r ->
|
||||
( Dcalc.Ast.ETupleAccess
|
||||
( r,
|
||||
i,
|
||||
@ -569,12 +591,15 @@ let translate_rule
|
||||
(fun (var_ctx, _) ->
|
||||
(var_ctx.scope_var_typ, pos_sigma))
|
||||
all_subscope_output_vars_dcalc ),
|
||||
pos_sigma ))
|
||||
(Dcalc.Ast.make_var (result_tuple_var, pos_sigma));
|
||||
pos_sigma );
|
||||
})
|
||||
(Bindlib.bind_var v next)
|
||||
(Dcalc.Ast.make_var (result_tuple_var, pos_sigma)),
|
||||
i - 1 ))
|
||||
all_subscope_output_vars_dcalc
|
||||
(next, List.length all_subscope_output_vars_dcalc - 1)
|
||||
in
|
||||
( call_scope_let :: result_bindings_lets,
|
||||
( (fun next -> call_scope_let (fst (result_bindings_lets next))),
|
||||
{
|
||||
ctx with
|
||||
subscope_vars =
|
||||
@ -589,24 +614,28 @@ let translate_rule
|
||||
} )
|
||||
| Assertion e ->
|
||||
let new_e = translate_expr ctx e in
|
||||
( [
|
||||
( (fun next ->
|
||||
Bindlib.box_apply2
|
||||
(fun next new_e ->
|
||||
Dcalc.Ast.ScopeLet
|
||||
{
|
||||
Dcalc.Ast.scope_let_var =
|
||||
(Dcalc.Ast.Var.make ("_", Pos.get_position e), Pos.get_position e);
|
||||
Dcalc.Ast.scope_let_typ = (Dcalc.Ast.TLit TUnit, Pos.get_position e);
|
||||
Dcalc.Ast.scope_let_next = next;
|
||||
Dcalc.Ast.scope_let_pos = Pos.get_position e;
|
||||
Dcalc.Ast.scope_let_typ =
|
||||
(Dcalc.Ast.TLit TUnit, Pos.get_position e);
|
||||
Dcalc.Ast.scope_let_expr =
|
||||
(* To ensure that we throw an error if the value is not defined,
|
||||
we add an check "ErrorOnEmpty" here. *)
|
||||
Bindlib.box_apply
|
||||
(fun new_e ->
|
||||
(* To ensure that we throw an error if the value is not
|
||||
defined, we add an check "ErrorOnEmpty" here. *)
|
||||
Pos.same_pos_as
|
||||
(Dcalc.Ast.EAssert
|
||||
(Dcalc.Ast.ErrorOnEmpty new_e, Pos.get_position e))
|
||||
e)
|
||||
new_e;
|
||||
Dcalc.Ast.scope_let_kind = Dcalc.Ast.Assertion;
|
||||
};
|
||||
],
|
||||
})
|
||||
(Bindlib.bind_var
|
||||
(Dcalc.Ast.Var.make ("_", Pos.get_position e))
|
||||
next)
|
||||
new_e),
|
||||
ctx )
|
||||
|
||||
let translate_rules
|
||||
@ -614,15 +643,16 @@ 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_let list * Dcalc.Ast.expr Pos.marked Bindlib.box * ctx =
|
||||
Dcalc.Ast.scope_body_expr Bindlib.box * ctx =
|
||||
let scope_lets, new_ctx =
|
||||
List.fold_left
|
||||
(fun (scope_lets, ctx) rule ->
|
||||
let new_scope_lets, new_ctx =
|
||||
translate_rule ctx rule (sigma_name, pos_sigma)
|
||||
in
|
||||
(scope_lets @ new_scope_lets, new_ctx))
|
||||
([], ctx) rules
|
||||
((fun next -> scope_lets (new_scope_lets next)), new_ctx))
|
||||
((fun next -> next), ctx)
|
||||
rules
|
||||
in
|
||||
let scope_variables = Ast.ScopeVarMap.bindings new_ctx.scope_vars in
|
||||
let scope_output_variables =
|
||||
@ -640,14 +670,19 @@ let translate_rules
|
||||
Dcalc.Ast.make_var (dcalc_var, pos_sigma))
|
||||
scope_output_variables))
|
||||
in
|
||||
(scope_lets, return_exp, new_ctx)
|
||||
( scope_lets
|
||||
(Bindlib.box_apply
|
||||
(fun return_exp -> Dcalc.Ast.Result return_exp)
|
||||
return_exp),
|
||||
new_ctx )
|
||||
|
||||
let translate_scope_decl
|
||||
(struct_ctx : Ast.struct_ctx)
|
||||
(enum_ctx : Ast.enum_ctx)
|
||||
(sctx : scope_sigs_ctx)
|
||||
(scope_name : Ast.ScopeName.t)
|
||||
(sigma : Ast.scope_decl) : Dcalc.Ast.scope_body * Dcalc.Ast.struct_ctx =
|
||||
(sigma : Ast.scope_decl) :
|
||||
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
|
||||
@ -679,7 +714,7 @@ let translate_scope_decl
|
||||
let scope_input_struct_name = scope_sig.scope_sig_input_struct in
|
||||
let scope_return_struct_name = scope_sig.scope_sig_output_struct in
|
||||
let pos_sigma = Pos.get_position sigma_info in
|
||||
let rules, return_exp, ctx =
|
||||
let rules_with_return_expr, ctx =
|
||||
translate_rules ctx sigma.scope_decl_rules sigma_info
|
||||
scope_return_struct_name
|
||||
in
|
||||
@ -716,16 +751,20 @@ let translate_scope_decl
|
||||
pos_sigma )
|
||||
| NoInput -> failwith "should not happen"
|
||||
in
|
||||
let input_destructurings =
|
||||
List.mapi
|
||||
(fun i (var_ctx, v) ->
|
||||
let input_destructurings (next : Dcalc.Ast.scope_body_expr Bindlib.box) =
|
||||
fst
|
||||
(List.fold_right
|
||||
(fun (var_ctx, v) (next, i) ->
|
||||
( Bindlib.box_apply2
|
||||
(fun next r ->
|
||||
Dcalc.Ast.ScopeLet
|
||||
{
|
||||
Dcalc.Ast.scope_let_kind = Dcalc.Ast.DestructuringInputStruct;
|
||||
Dcalc.Ast.scope_let_var = (v, pos_sigma);
|
||||
Dcalc.Ast.scope_let_kind =
|
||||
Dcalc.Ast.DestructuringInputStruct;
|
||||
Dcalc.Ast.scope_let_next = next;
|
||||
Dcalc.Ast.scope_let_pos = pos_sigma;
|
||||
Dcalc.Ast.scope_let_typ = input_var_typ var_ctx;
|
||||
Dcalc.Ast.scope_let_expr =
|
||||
Bindlib.box_apply
|
||||
(fun r ->
|
||||
( Dcalc.Ast.ETupleAccess
|
||||
( r,
|
||||
i,
|
||||
@ -733,10 +772,13 @@ let translate_scope_decl
|
||||
List.map
|
||||
(fun (var_ctx, _) -> input_var_typ var_ctx)
|
||||
scope_input_variables ),
|
||||
pos_sigma ))
|
||||
(Dcalc.Ast.make_var (scope_input_var, pos_sigma));
|
||||
pos_sigma );
|
||||
})
|
||||
(Bindlib.bind_var v next)
|
||||
(Dcalc.Ast.make_var (scope_input_var, pos_sigma)),
|
||||
i - 1 ))
|
||||
scope_input_variables
|
||||
(next, List.length scope_input_variables - 1))
|
||||
in
|
||||
let scope_return_struct_fields =
|
||||
List.map
|
||||
@ -761,13 +803,15 @@ let translate_scope_decl
|
||||
(Ast.StructMap.singleton scope_return_struct_name
|
||||
scope_return_struct_fields)
|
||||
in
|
||||
( {
|
||||
Dcalc.Ast.scope_body_lets = input_destructurings @ rules;
|
||||
Dcalc.Ast.scope_body_result = return_exp;
|
||||
( Bindlib.box_apply
|
||||
(fun scope_body_expr ->
|
||||
{
|
||||
Dcalc.Ast.scope_body_expr;
|
||||
Dcalc.Ast.scope_body_input_struct = scope_input_struct_name;
|
||||
Dcalc.Ast.scope_body_output_struct = scope_return_struct_name;
|
||||
Dcalc.Ast.scope_body_arg = scope_input_var;
|
||||
},
|
||||
})
|
||||
(Bindlib.bind_var scope_input_var
|
||||
(input_destructurings rules_with_return_expr)),
|
||||
new_struct_ctx )
|
||||
|
||||
let translate_program (prgm : Ast.program) :
|
||||
@ -844,18 +888,9 @@ 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)
|
||||
: (Ast.ScopeName.t * Dcalc.Ast.expr Bindlib.var * Dcalc.Ast.scope_body)
|
||||
list
|
||||
* _ =
|
||||
let (scopes, decl_ctx) : Dcalc.Ast.scopes Bindlib.box * _ =
|
||||
List.fold_right
|
||||
(fun scope_name
|
||||
((scopes, decl_ctx) :
|
||||
(Ast.ScopeName.t
|
||||
* Dcalc.Ast.expr Bindlib.var
|
||||
* Dcalc.Ast.scope_body)
|
||||
list
|
||||
* _) ->
|
||||
(fun scope_name (scopes, decl_ctx) ->
|
||||
let scope = Ast.ScopeMap.find scope_name prgm.program_scopes in
|
||||
let scope_body, scope_out_struct =
|
||||
translate_scope_decl struct_ctx enum_ctx sctx scope_name scope
|
||||
@ -870,7 +905,15 @@ let translate_program (prgm : Ast.program) :
|
||||
decl_ctx.Dcalc.Ast.ctx_structs scope_out_struct;
|
||||
}
|
||||
in
|
||||
((scope_name, dvar, scope_body) :: scopes, decl_ctx))
|
||||
scope_ordering ([], decl_ctx)
|
||||
let scope_next = Bindlib.bind_var dvar scopes in
|
||||
let new_scopes =
|
||||
Bindlib.box_apply2
|
||||
(fun scope_body scope_next ->
|
||||
Dcalc.Ast.ScopeDef { scope_name; scope_body; scope_next })
|
||||
scope_body scope_next
|
||||
in
|
||||
({ scopes; decl_ctx }, types_ordering)
|
||||
(new_scopes, decl_ctx))
|
||||
scope_ordering
|
||||
(Bindlib.box Dcalc.Ast.Nil, decl_ctx)
|
||||
in
|
||||
({ scopes = Bindlib.unbox scopes; decl_ctx }, types_ordering)
|
||||
|
@ -115,6 +115,12 @@ let avoid_exceptions =
|
||||
& info [ "avoid_exceptions" ]
|
||||
~doc:"Compiles the default calculus without exceptions")
|
||||
|
||||
let closure_conversion =
|
||||
Arg.(
|
||||
value & flag
|
||||
& info [ "closure_conversion" ]
|
||||
~doc:"Performs closure conversion on the lambda calculus")
|
||||
|
||||
let wrap_weaved_output =
|
||||
Arg.(
|
||||
value & flag
|
||||
@ -186,6 +192,7 @@ type options = {
|
||||
optimize : bool;
|
||||
ex_scope : string option;
|
||||
output_file : string option;
|
||||
closure_conversion : bool;
|
||||
}
|
||||
|
||||
let options =
|
||||
@ -194,6 +201,7 @@ let options =
|
||||
unstyled
|
||||
wrap_weaved_output
|
||||
avoid_exceptions
|
||||
closure_conversion
|
||||
backend
|
||||
language
|
||||
max_prec_digits
|
||||
@ -215,11 +223,12 @@ let options =
|
||||
optimize;
|
||||
ex_scope;
|
||||
output_file;
|
||||
closure_conversion;
|
||||
}
|
||||
in
|
||||
Term.(
|
||||
const make $ debug $ unstyled $ wrap_weaved_output $ avoid_exceptions
|
||||
$ backend $ language $ max_prec_digits_opt $ trace_opt
|
||||
$ closure_conversion $ backend $ language $ max_prec_digits_opt $ trace_opt
|
||||
$ disable_counterexamples_opt $ optimize $ ex_scope $ output)
|
||||
|
||||
let catala_t f = Term.(const f $ file $ options)
|
||||
|
@ -90,6 +90,7 @@ type options = {
|
||||
optimize : bool;
|
||||
ex_scope : string option;
|
||||
output_file : string option;
|
||||
closure_conversion : bool;
|
||||
}
|
||||
(** {2 Command-line application} *)
|
||||
|
||||
|
@ -25,7 +25,12 @@ type vc_return = expr Pos.marked * typ Pos.marked VarMap.t
|
||||
(** The return type of VC generators is the VC expression plus the types of any
|
||||
locally free variable inside that expression. *)
|
||||
|
||||
type ctx = { decl : decl_ctx; input_vars : Var.t list }
|
||||
type ctx = {
|
||||
current_scope_name : ScopeName.t;
|
||||
decl : decl_ctx;
|
||||
input_vars : Var.t list;
|
||||
scope_variables_typs : typ Pos.marked VarMap.t;
|
||||
}
|
||||
|
||||
let conjunction (args : vc_return list) (pos : Pos.t) : vc_return =
|
||||
let acc, list =
|
||||
@ -298,47 +303,35 @@ type verification_condition = {
|
||||
vc_free_vars_typ : typ Pos.marked VarMap.t;
|
||||
}
|
||||
|
||||
let generate_verification_conditions
|
||||
(p : program) (s : Dcalc.Ast.ScopeName.t option) :
|
||||
verification_condition list =
|
||||
List.fold_left
|
||||
(fun acc (s_name, _s_var, s_body) ->
|
||||
let is_selected_scope =
|
||||
match s with
|
||||
| Some s when Dcalc.Ast.ScopeName.compare s s_name = 0 -> true
|
||||
| None -> true
|
||||
| _ -> false
|
||||
let rec generate_verification_conditions_scope_body_expr
|
||||
(ctx : ctx) (scope_body_expr : scope_body_expr) :
|
||||
ctx * verification_condition list =
|
||||
match scope_body_expr with
|
||||
| Result _ -> (ctx, [])
|
||||
| ScopeLet scope_let ->
|
||||
let scope_let_var, scope_let_next =
|
||||
Bindlib.unbind scope_let.scope_let_next
|
||||
in
|
||||
if is_selected_scope then
|
||||
let ctx = { decl = p.decl_ctx; input_vars = [] } in
|
||||
let acc, _ =
|
||||
List.fold_left
|
||||
(fun (acc, ctx) s_let ->
|
||||
match s_let.scope_let_kind with
|
||||
let new_ctx, vc_list =
|
||||
match scope_let.scope_let_kind with
|
||||
| DestructuringInputStruct ->
|
||||
( acc,
|
||||
{
|
||||
ctx with
|
||||
input_vars =
|
||||
Pos.unmark s_let.scope_let_var :: ctx.input_vars;
|
||||
} )
|
||||
({ ctx with input_vars = scope_let_var :: ctx.input_vars }, [])
|
||||
| ScopeVarDefinition | SubScopeVarDefinition ->
|
||||
(* For scope variables, we should check both that they never
|
||||
evaluate to emptyError nor conflictError. But for subscope
|
||||
variable definitions, what we're really doing is adding
|
||||
exceptions to something defined in the subscope so we just
|
||||
ought to verify only that the exceptions overlap. *)
|
||||
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
|
||||
(Bindlib.unbox s_let.scope_let_expr)
|
||||
scope_let.scope_let_expr
|
||||
in
|
||||
let vc_confl, vc_confl_typs =
|
||||
generate_vs_must_not_return_confict ctx e
|
||||
in
|
||||
let vc_confl =
|
||||
if !Cli.optimize_flag then
|
||||
Bindlib.unbox
|
||||
(Optimizations.optimize_expr p.decl_ctx vc_confl)
|
||||
Bindlib.unbox (Optimizations.optimize_expr ctx.decl vc_confl)
|
||||
else vc_confl
|
||||
in
|
||||
let vc_list =
|
||||
@ -346,14 +339,17 @@ let generate_verification_conditions
|
||||
{
|
||||
vc_guard = Pos.same_pos_as (Pos.unmark vc_confl) e;
|
||||
vc_kind = NoOverlappingExceptions;
|
||||
vc_free_vars_typ = vc_confl_typs;
|
||||
vc_scope = s_name;
|
||||
vc_variable = s_let.scope_let_var;
|
||||
vc_free_vars_typ =
|
||||
VarMap.union
|
||||
(fun _ _ -> failwith "should not happen")
|
||||
ctx.scope_variables_typs vc_confl_typs;
|
||||
vc_scope = ctx.current_scope_name;
|
||||
vc_variable = (scope_let_var, scope_let.scope_let_pos);
|
||||
};
|
||||
]
|
||||
in
|
||||
let vc_list =
|
||||
match s_let.scope_let_kind with
|
||||
match scope_let.scope_let_kind with
|
||||
| ScopeVarDefinition ->
|
||||
let vc_empty, vc_empty_typs =
|
||||
generate_vc_must_not_return_empty ctx e
|
||||
@ -361,23 +357,89 @@ let generate_verification_conditions
|
||||
let vc_empty =
|
||||
if !Cli.optimize_flag then
|
||||
Bindlib.unbox
|
||||
(Optimizations.optimize_expr p.decl_ctx vc_empty)
|
||||
(Optimizations.optimize_expr ctx.decl vc_empty)
|
||||
else vc_empty
|
||||
in
|
||||
{
|
||||
vc_guard = Pos.same_pos_as (Pos.unmark vc_empty) e;
|
||||
vc_kind = NoEmptyError;
|
||||
vc_free_vars_typ = vc_empty_typs;
|
||||
vc_scope = s_name;
|
||||
vc_variable = s_let.scope_let_var;
|
||||
vc_free_vars_typ =
|
||||
VarMap.union
|
||||
(fun _ _ -> failwith "should not happen")
|
||||
ctx.scope_variables_typs vc_empty_typs;
|
||||
vc_scope = ctx.current_scope_name;
|
||||
vc_variable = (scope_let_var, scope_let.scope_let_pos);
|
||||
}
|
||||
:: vc_list
|
||||
| _ -> vc_list
|
||||
in
|
||||
(vc_list @ acc, ctx)
|
||||
| _ -> (acc, ctx))
|
||||
(acc, ctx) s_body.scope_body_lets
|
||||
(ctx, vc_list)
|
||||
| _ -> (ctx, [])
|
||||
in
|
||||
acc
|
||||
else acc)
|
||||
[] p.scopes
|
||||
let new_ctx, new_vcs =
|
||||
generate_verification_conditions_scope_body_expr
|
||||
{
|
||||
new_ctx with
|
||||
scope_variables_typs =
|
||||
VarMap.add scope_let_var scope_let.scope_let_typ
|
||||
new_ctx.scope_variables_typs;
|
||||
}
|
||||
scope_let_next
|
||||
in
|
||||
(new_ctx, vc_list @ new_vcs)
|
||||
|
||||
let rec generate_verification_conditions_scopes
|
||||
(decl_ctx : decl_ctx) (scopes : scopes) (s : ScopeName.t option) :
|
||||
verification_condition list =
|
||||
match scopes with
|
||||
| Nil -> []
|
||||
| ScopeDef scope_def ->
|
||||
let is_selected_scope =
|
||||
match s with
|
||||
| Some s when Dcalc.Ast.ScopeName.compare s scope_def.scope_name = 0 ->
|
||||
true
|
||||
| None -> true
|
||||
| _ -> false
|
||||
in
|
||||
let vcs =
|
||||
if is_selected_scope then
|
||||
let _scope_input_var, scope_body_expr =
|
||||
Bindlib.unbind scope_def.scope_body.scope_body_expr
|
||||
in
|
||||
let ctx =
|
||||
{
|
||||
current_scope_name = scope_def.scope_name;
|
||||
decl = decl_ctx;
|
||||
input_vars = [];
|
||||
scope_variables_typs =
|
||||
VarMap.empty
|
||||
(* We don't need to add the typ of the scope input var here
|
||||
because it will never appear in an expression for which we
|
||||
generate a verification conditions (the big struct is
|
||||
destructured with a series of let bindings just after. )*);
|
||||
}
|
||||
in
|
||||
let _, vcs =
|
||||
generate_verification_conditions_scope_body_expr ctx scope_body_expr
|
||||
in
|
||||
vcs
|
||||
else []
|
||||
in
|
||||
let _scope_var, next = Bindlib.unbind scope_def.scope_next in
|
||||
generate_verification_conditions_scopes decl_ctx next s @ vcs
|
||||
|
||||
let generate_verification_conditions
|
||||
(p : program) (s : Dcalc.Ast.ScopeName.t option) :
|
||||
verification_condition list =
|
||||
let vcs = generate_verification_conditions_scopes p.decl_ctx p.scopes s in
|
||||
(* We sort this list by scope name and then variable name to ensure consistent
|
||||
output for testing*)
|
||||
List.sort
|
||||
(fun vc1 vc2 ->
|
||||
let to_str vc =
|
||||
Format.asprintf "%s.%s"
|
||||
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
|
||||
(Bindlib.name_of (Pos.unmark vc.vc_variable))
|
||||
in
|
||||
String.compare (to_str vc1) (to_str vc2))
|
||||
vcs
|
||||
|
@ -20,9 +20,8 @@ open Dcalc.Ast
|
||||
expressions [vcs] corresponding to verification conditions that must be
|
||||
discharged by Z3, and attempts to solve them **)
|
||||
let solve_vc
|
||||
(prgm : program)
|
||||
(decl_ctx : decl_ctx)
|
||||
(vcs : Conditions.verification_condition list) : unit =
|
||||
(decl_ctx : decl_ctx) (vcs : Conditions.verification_condition list) : unit
|
||||
=
|
||||
(* Right now we only use the Z3 backend but the functorial interface should
|
||||
make it easy to mix and match different proof backends. *)
|
||||
Z3backend.Io.init_backend ();
|
||||
@ -34,12 +33,7 @@ let solve_vc
|
||||
let ctx, z3_vc =
|
||||
Z3backend.Io.translate_expr
|
||||
(Z3backend.Io.make_context decl_ctx
|
||||
(VarMap.union
|
||||
(fun _ _ _ ->
|
||||
failwith
|
||||
"[Proof encoding]: A Variable cannot be both free \
|
||||
and bound")
|
||||
(variable_types prgm) vc.Conditions.vc_free_vars_typ))
|
||||
vc.Conditions.vc_free_vars_typ)
|
||||
(Bindlib.unbox
|
||||
(Dcalc.Optimizations.remove_all_logs vc.Conditions.vc_guard))
|
||||
in
|
||||
|
@ -17,7 +17,4 @@
|
||||
(** Solves verification conditions using various proof backends *)
|
||||
|
||||
val solve_vc :
|
||||
Dcalc.Ast.program ->
|
||||
Dcalc.Ast.decl_ctx ->
|
||||
Conditions.verification_condition list ->
|
||||
unit
|
||||
Dcalc.Ast.decl_ctx -> Conditions.verification_condition list -> unit
|
||||
|
5387
french_law/js/french_law.js
generated
5387
french_law/js/french_law.js
generated
File diff suppressed because one or more lines are too long
1272
french_law/ocaml/law_source/allocations_familiales.ml
generated
1272
french_law/ocaml/law_source/allocations_familiales.ml
generated
File diff suppressed because it is too large
Load Diff
3398
french_law/python/src/allocations_familiales.py
generated
3398
french_law/python/src/allocations_familiales.py
generated
File diff suppressed because it is too large
Load Diff
@ -1,18 +1,18 @@
|
||||
let TestBool_7 :
|
||||
let TestBool_13 :
|
||||
TestBool_in{"foo_in": unit → bool; "bar_in": unit → integer} →
|
||||
TestBool_out{"foo_out": bool; "bar_out": integer} =
|
||||
λ (TestBool_in_8: TestBool_in{"foo_in": unit → bool; "bar_in":
|
||||
λ (TestBool_in_14: TestBool_in{"foo_in": unit → bool; "bar_in":
|
||||
unit → integer}) →
|
||||
let foo_9 : unit → bool = TestBool_in_8."foo_in" in
|
||||
let bar_10 : unit → integer = TestBool_in_8."bar_in" in
|
||||
let bar_11 : integer = error_empty
|
||||
⟨bar_10 () | true ⊢
|
||||
let foo_15 : unit → bool = TestBool_in_14."foo_in" in
|
||||
let bar_16 : unit → integer = TestBool_in_14."bar_in" in
|
||||
let bar_17 : integer = error_empty
|
||||
⟨bar_16 () | true ⊢
|
||||
⟨⟨true ⊢ ⟨⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
|
||||
⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
|
||||
let foo_12 : bool = error_empty
|
||||
⟨foo_9 () | true ⊢
|
||||
⟨⟨true ⊢ ⟨⟨bar_11 < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩,
|
||||
⟨true ⊢ ⟨⟨bar_11 >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
|
||||
let foo_18 : bool = error_empty
|
||||
⟨foo_15 () | true ⊢
|
||||
⟨⟨true ⊢ ⟨⟨bar_17 < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩,
|
||||
⟨true ⊢ ⟨⟨bar_17 >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
|
||||
true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
|
||||
TestBool_out {"foo_out"= foo_12; "bar_out"= bar_11} in
|
||||
TestBool_7
|
||||
TestBool_out {"foo_out"= foo_18; "bar_out"= bar_17} in
|
||||
TestBool_13
|
||||
|
@ -1,23 +1,23 @@
|
||||
let A =
|
||||
λ (A_in_11: A_in{"c_in": integer; "d_in": integer; "e_in":
|
||||
λ (A_in_31: A_in{"c_in": integer; "d_in": integer; "e_in":
|
||||
unit → integer; "f_in": unit → integer}) →
|
||||
let c_12 : integer = A_in_11."c_in" in
|
||||
let d_13 : integer = A_in_11."d_in" in
|
||||
let e_14 : unit → integer = A_in_11."e_in" in
|
||||
let f_15 : unit → integer = A_in_11."f_in" in
|
||||
let a_16 : integer = error_empty
|
||||
let c_32 : integer = A_in_31."c_in" in
|
||||
let d_33 : integer = A_in_31."d_in" in
|
||||
let e_34 : unit → integer = A_in_31."e_in" in
|
||||
let f_35 : unit → integer = A_in_31."f_in" in
|
||||
let a_36 : integer = error_empty
|
||||
⟨⟨true ⊢ ⟨⟨true ⊢ 0⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
|
||||
⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
|
||||
let b_17 : integer = error_empty
|
||||
⟨⟨true ⊢ ⟨⟨true ⊢ a_16 + 1⟩ | false ⊢ ∅ ⟩⟩ | true
|
||||
let b_37 : integer = error_empty
|
||||
⟨⟨true ⊢ ⟨⟨true ⊢ a_36 + 1⟩ | false ⊢ ∅ ⟩⟩ | true
|
||||
⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
|
||||
let e_18 : integer = error_empty
|
||||
⟨e_14 () | true ⊢
|
||||
let e_38 : integer = error_empty
|
||||
⟨e_34 () | true ⊢
|
||||
⟨⟨true ⊢
|
||||
⟨⟨true ⊢ b_17 + c_12 + d_13 + 1⟩ | false ⊢ ∅ ⟩⟩
|
||||
⟨⟨true ⊢ b_37 + c_32 + d_33 + 1⟩ | false ⊢ ∅ ⟩⟩
|
||||
| true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
|
||||
let f_19 : integer = error_empty
|
||||
⟨f_15 () | true ⊢
|
||||
⟨⟨true ⊢ ⟨⟨true ⊢ e_18 + 1⟩ | false ⊢ ∅ ⟩⟩ |
|
||||
let f_39 : integer = error_empty
|
||||
⟨f_35 () | true ⊢
|
||||
⟨⟨true ⊢ ⟨⟨true ⊢ e_38 + 1⟩ | false ⊢ ∅ ⟩⟩ |
|
||||
true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
|
||||
A_out {"b_out"= b_17; "d_out"= d_13; "f_out"= f_19}
|
||||
A_out {"b_out"= b_37; "d_out"= d_33; "f_out"= f_39}
|
||||
|
@ -1,8 +1,8 @@
|
||||
let B =
|
||||
λ (B_in_14: B_in{}) →
|
||||
let a.x_15 : bool = error_empty
|
||||
λ (B_in_31: B_in{}) →
|
||||
let a.x_32 : bool = error_empty
|
||||
⟨true ⊢ ⟨⟨true ⊢ false⟩ | false ⊢ ∅ ⟩⟩ in
|
||||
let result_16 : A_out{"y_out": integer} = A_3 (A_in {"x_in"= a.x_15}) in
|
||||
let a.y_17 : integer = result_16."y_out" in
|
||||
let __18 : unit = assert (error_empty a.y_17 = 1) in
|
||||
let result_33 : A_out{"y_out": integer} = A_24 (A_in {"x_in"= a.x_32}) in
|
||||
let a.y_34 : integer = result_33."y_out" in
|
||||
let __35 : unit = assert (error_empty a.y_34 = 1) in
|
||||
B_out {}
|
||||
|
@ -1,11 +1,11 @@
|
||||
let B =
|
||||
λ (B_in_18: B_in{}) →
|
||||
let a.a_19 : unit → integer = λ (__20: unit) → ∅ in
|
||||
let a.b_21 : integer = error_empty
|
||||
λ (B_in_40: B_in{}) →
|
||||
let a.a_41 : unit → integer = λ (__42: unit) → ∅ in
|
||||
let a.b_43 : integer = error_empty
|
||||
⟨⟨true ⊢ ⟨⟨true ⊢ 2⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
|
||||
⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
|
||||
let result_22 : A_out{"c_out": integer} =
|
||||
A_3 (A_in {"a_in"= a.a_19; "b_in"= a.b_21}) in
|
||||
let a.c_23 : integer = result_22."c_out" in
|
||||
let __24 : unit = assert (error_empty a.c_23 = 1) in
|
||||
let result_44 : A_out{"c_out": integer} =
|
||||
A_32 (A_in {"a_in"= a.a_41; "b_in"= a.b_43}) in
|
||||
let a.c_45 : integer = result_44."c_out" in
|
||||
let __46 : unit = assert (error_empty a.c_45 = 1) in
|
||||
B_out {}
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.y] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/array_length-empty.catala_en
|
||||
|
|
||||
@ -6,5 +8,3 @@
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[ERROR] [A.y] At least two exceptions overlap for this variable:
|
||||
--> tests/test_proof/bad/array_length-overlap.catala_en
|
||||
@ -6,5 +8,3 @@
|
||||
| ^
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.y] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/dates_get_year-empty.catala_en
|
||||
|
|
||||
@ -6,5 +8,3 @@
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[ERROR] [A.y] At least two exceptions overlap for this variable:
|
||||
--> tests/test_proof/bad/dates_get_year-overlap.catala_en
|
||||
@ -6,5 +8,3 @@
|
||||
| ^
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.y] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/dates_simple-empty.catala_en
|
||||
|
|
||||
@ -6,5 +8,3 @@
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[ERROR] [A.y] At least two exceptions overlap for this variable:
|
||||
--> tests/test_proof/bad/dates_simple-overlap.catala_en
|
||||
@ -6,5 +8,3 @@
|
||||
| ^
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.y] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/duration-empty.catala_en
|
||||
|
|
||||
@ -6,5 +8,3 @@
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[ERROR] [A.y] At least two exceptions overlap for this variable:
|
||||
--> tests/test_proof/bad/duration-overlap.catala_en
|
||||
@ -6,5 +8,3 @@
|
||||
| ^
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.y] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/enums_inj-empty.catala_en
|
||||
|
|
||||
@ -6,5 +8,3 @@
|
||||
+ Article
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[ERROR] [A.y] At least two exceptions overlap for this variable:
|
||||
--> tests/test_proof/bad/enums_inj-overlap.catala_en
|
||||
@ -6,5 +8,3 @@
|
||||
| ^
|
||||
+ Article
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.y] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/enums_unit-empty.catala_en
|
||||
|
|
||||
@ -6,5 +8,3 @@
|
||||
+ Article
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[ERROR] [A.y] At least two exceptions overlap for this variable:
|
||||
--> tests/test_proof/bad/enums_unit-overlap.catala_en
|
||||
@ -6,5 +8,3 @@
|
||||
| ^
|
||||
+ Article
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.y] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/money-empty.catala_en
|
||||
|
|
||||
@ -6,5 +8,3 @@
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[ERROR] [A.y] At least two exceptions overlap for this variable:
|
||||
--> tests/test_proof/bad/money-overlap.catala_en
|
||||
@ -6,5 +8,3 @@
|
||||
| ^
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[ERROR] [A.y] At least two exceptions overlap for this variable:
|
||||
--> tests/test_proof/bad/no_vars-conflict.catala_en
|
||||
@ -6,5 +8,3 @@
|
||||
| ^
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.y] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/no_vars-empty.catala_en
|
||||
|
|
||||
@ -6,5 +8,3 @@
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -11,12 +11,12 @@ Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [Amount.correct_amount] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [Amount.eligibility.is_professor] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [Amount.eligibility.is_student] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [Amount.number_of_advisors] This variable never returns an empty error
|
||||
[RESULT] [Amount.number_of_advisors] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [Amount.is_professor] This variable never returns an empty error
|
||||
[RESULT] [Amount.is_professor] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [Amount.is_student] This variable never returns an empty error
|
||||
[RESULT] [Amount.is_student] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [Amount.number_of_advisors] This variable never returns an empty error
|
||||
[RESULT] [Amount.number_of_advisors] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [Eligibility.is_eligible] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/prolala_motivating_example.catala_en
|
||||
|
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.y] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/rationals-empty.catala_en
|
||||
|
|
||||
@ -6,5 +8,3 @@
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[ERROR] [A.y] At least two exceptions overlap for this variable:
|
||||
--> tests/test_proof/bad/rationals-overlap.catala_en
|
||||
@ -6,5 +8,3 @@
|
||||
| ^
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,3 +1,5 @@
|
||||
[RESULT] [A.x1] This variable never returns an empty error
|
||||
[RESULT] [A.x1] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.x10] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/sat_solving.catala_en
|
||||
|
|
||||
@ -6,21 +8,19 @@
|
||||
+ Test
|
||||
Counterexample generation is disabled so none was generated.
|
||||
[RESULT] [A.x10] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x9] This variable never returns an empty error
|
||||
[RESULT] [A.x9] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x8] This variable never returns an empty error
|
||||
[RESULT] [A.x8] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x7] This variable never returns an empty error
|
||||
[RESULT] [A.x7] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x6] This variable never returns an empty error
|
||||
[RESULT] [A.x6] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x5] This variable never returns an empty error
|
||||
[RESULT] [A.x5] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x4] This variable never returns an empty error
|
||||
[RESULT] [A.x4] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x3] This variable never returns an empty error
|
||||
[RESULT] [A.x3] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x2] This variable never returns an empty error
|
||||
[RESULT] [A.x2] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x1] This variable never returns an empty error
|
||||
[RESULT] [A.x1] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x3] This variable never returns an empty error
|
||||
[RESULT] [A.x3] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x4] This variable never returns an empty error
|
||||
[RESULT] [A.x4] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x5] This variable never returns an empty error
|
||||
[RESULT] [A.x5] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x6] This variable never returns an empty error
|
||||
[RESULT] [A.x6] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x7] This variable never returns an empty error
|
||||
[RESULT] [A.x7] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x8] This variable never returns an empty error
|
||||
[RESULT] [A.x8] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x9] This variable never returns an empty error
|
||||
[RESULT] [A.x9] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,4 +1,4 @@
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,4 +1,4 @@
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,4 +1,4 @@
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,4 +1,4 @@
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,4 +1,4 @@
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,4 +1,4 @@
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,4 +1,4 @@
|
||||
[RESULT] [A.z] This variable never returns an empty error
|
||||
[RESULT] [A.z] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.z] This variable never returns an empty error
|
||||
[RESULT] [A.z] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,4 +1,4 @@
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,4 +1,4 @@
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
|
@ -1,6 +1,6 @@
|
||||
[RESULT] [A.z] This variable never returns an empty error
|
||||
[RESULT] [A.z] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.z] This variable never returns an empty error
|
||||
[RESULT] [A.z] No two exceptions to ever overlap for this variable
|
||||
|
Loading…
Reference in New Issue
Block a user