CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-20 00:41:05 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into allocations_logement

Browse Source
This commit is contained in:
Denis Merigoux 2022-02-25 17:10:23 +01:00
commit cfbca7b2be
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
36 changed files with 9993 additions and 7804 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.nix/no-web.patch
View File

@ -14,7 +14,7 @@ index 31d5289..0000000
- (language : Js.js_string Js.t) (trace : bool) =
- driver
- (Contents (Js.to_string contents))
- false false false "Interpret"
- false false false false "Interpret"
- (Some (Js.to_string language))
- None trace false false
- (Some (Js.to_string scope))

2
compiler/catala_web_interpreter.ml
View File

@ -8,7 +8,7 @@ let _ =
(language : Js.js_string Js.t) (trace : bool) =
driver
(Contents (Js.to_string contents))
false false false "Interpret"
false false false false "Interpret"
(Some (Js.to_string language))
None trace false false
(Some (Js.to_string scope))

30
compiler/dcalc/ast.ml
View File

@ -93,7 +93,7 @@ type log_entry = VarDef of typ | BeginCall | EndCall | PosRecordIfTrueBool
type unop =
| Not
| Minus of op_kind
| Log of log_entry * (Utils.Uid.MarkedString.info list[@opaque])
| Log of log_entry * Utils.Uid.MarkedString.info list
| Length
| IntToRat
| GetDay
@ -103,7 +103,7 @@ type unop =
type operator = Ternop of ternop | Binop of binop | Unop of unop
type expr =
| EVar of (expr Bindlib.var[@opaque]) Pos.marked
| EVar of expr Bindlib.var Pos.marked
| ETuple of expr Pos.marked list * struct_name option
| ETupleAccess of expr Pos.marked * int * struct_name option * typ Pos.marked list
| EInj of expr Pos.marked * int * enum_name * typ Pos.marked list
@ -143,8 +143,8 @@ type 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_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;
}
@ -164,6 +164,28 @@ 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 =
match Pos.unmark e with
| EVar (v, _) -> VarMap.singleton v ()
| ETuple (es, _) | EArray es -> es |> List.map free_vars_set |> List.fold_left union VarMap.empty
| ETupleAccess (e1, _, _, _) | EAssert e1 | ErrorOnEmpty e1 | EInj (e1, _, _, _) ->
free_vars_set e1
| EApp (e1, es) | EMatch (e1, es, _) ->
e1 :: es |> List.map free_vars_set |> List.fold_left union VarMap.empty
| EDefault (es, ejust, econs) ->
ejust :: econs :: es |> List.map free_vars_set |> List.fold_left union VarMap.empty
| EOp _ | ELit _ -> VarMap.empty
| EIfThenElse (e1, e2, e3) ->
[ e1; e2; e3 ] |> List.map free_vars_set |> List.fold_left union VarMap.empty
| EAbs ((binder, _), _) ->
let vs, body = Bindlib.unmbind binder in
Array.fold_right VarMap.remove vs (free_vars_set body)
let free_vars_list (e : expr Pos.marked) : Var.t list =
free_vars_set e |> VarMap.bindings |> List.map fst
type vars = expr Bindlib.mvar
let make_var ((x, pos) : Var.t Pos.marked) : expr Pos.marked Bindlib.box =

6
compiler/dcalc/ast.mli
View File

@ -119,7 +119,7 @@ type expr =
(** The [MarkedString.info] is the former enum case name *)
| EArray of expr Pos.marked list
| ELit of lit
| EAbs of (expr, expr Pos.marked) Bindlib.mbinder Pos.marked * typ Pos.marked list
| EAbs of ((expr, expr Pos.marked) Bindlib.mbinder[@opaque]) Pos.marked * typ Pos.marked list
| EApp of expr Pos.marked * expr Pos.marked list
| EAssert of expr Pos.marked
| EOp of operator
@ -183,6 +183,10 @@ end
module VarMap : Map.S with type key = Var.t
val free_vars_set : expr Pos.marked -> unit VarMap.t
val free_vars_list : expr Pos.marked -> Var.t list
type vars = expr Bindlib.mvar
val make_var : Var.t Pos.marked -> expr Pos.marked Bindlib.box

132
compiler/dcalc/binded_representation.ml Normal file
View File

@ -0,0 +1,132 @@
(* 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

63
compiler/dcalc/binded_representation.mli Normal file
View File

@ -0,0 +1,63 @@
(* 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] *)

6
compiler/dcalc/optimizations.ml
View File

@ -123,9 +123,11 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : expr Pos.marked)
((ELit (LBool false) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ])), _),
_ ) ->
(ELit LEmptyError, pos)
| [], just, cons ->
| [], just, cons when not !Cli.avoid_exceptions_flag ->
(* without exceptions, a default is just an [if then else] raising an error in the
else case *)
else case. This exception is only valid in the context of
compilation_with_exceptions, so we desactivate with a global flag to know if we
will be compiling using exceptions or the option monad. *)
(EIfThenElse (just, cons, (ELit LEmptyError, pos)), pos)
| exceptions, just, cons -> (EDefault (exceptions, just, cons), pos))
(List.map rec_helper exceptions |> Bindlib.box_list)

13
compiler/driver.ml
View File

@ -26,15 +26,17 @@ let extensions = [ (".catala_fr", "fr"); (".catala_en", "en"); (".catala_pl", "p
(** Entry function for the executable. Returns a negative number in case of error. Usage:
[driver source_file debug dcalc unstyled wrap_weaved_output backend language max_prec_digits trace optimize scope_to_execute output_file]*)
let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
(wrap_weaved_output : bool) (backend : string) (language : string option)
(max_prec_digits : int option) (trace : bool) (disable_counterexamples : bool) (optimize : bool)
(ex_scope : string option) (output_file : string option) : int =
(wrap_weaved_output : bool) (avoid_exceptions : bool) (backend : string)
(language : string option) (max_prec_digits : int option) (trace : bool)
(disable_counterexamples : bool) (optimize : bool) (ex_scope : string option)
(output_file : string option) : int =
try
Cli.debug_flag := debug;
Cli.style_flag := not unstyled;
Cli.trace_flag := trace;
Cli.optimize_flag := optimize;
Cli.disable_counterexamples := disable_counterexamples;
Cli.avoid_exceptions_flag := avoid_exceptions;
Cli.debug_print "Reading files...";
let filename = ref "" in
(match source_file with FileName f -> filename := f | Contents c -> Cli.contents := c);
@ -255,7 +257,10 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
0
| Cli.OCaml | Cli.Python | Cli.Lcalc | Cli.Scalc ->
Cli.debug_print "Compiling program into lambda calculus...";
let prgm = Lcalc.Compile_with_exceptions.translate_program prgm in
let prgm =
if avoid_exceptions then Lcalc.Compile_without_exceptions.translate_program prgm
else Lcalc.Compile_with_exceptions.translate_program prgm
in
let prgm =
if optimize then begin
Cli.debug_print "Optimizing lambda calculus...";

63
compiler/lcalc/ast.ml
View File

@ -74,18 +74,63 @@ let make_app (e : expr Pos.marked Bindlib.box) (u : expr Pos.marked Bindlib.box
let make_let_in (x : Var.t) (tau : D.typ Pos.marked) (e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun e u -> (EApp (e, u), Pos.get_position (Bindlib.unbox e2)))
(make_abs
(Array.of_list [ x ])
e2
(Pos.get_position (Bindlib.unbox e2))
[ tau ]
(Pos.get_position (Bindlib.unbox e2)))
(Bindlib.box_list [ e1 ])
let pos = Pos.get_position (Bindlib.unbox e2) in
make_app (make_abs (Array.of_list [ x ]) e2 pos [ tau ] 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)
let none_constr : D.EnumConstructor.t = D.EnumConstructor.fresh ("ENone", Pos.no_pos)
let some_constr : D.EnumConstructor.t = D.EnumConstructor.fresh ("ESome", Pos.no_pos)
let option_enum_config : (D.EnumConstructor.t * D.typ Pos.marked) list =
[ (none_constr, (D.TLit D.TUnit, Pos.no_pos)); (some_constr, (D.TAny, Pos.no_pos)) ]
let make_none (pos : Pos.t) : expr Pos.marked Bindlib.box =
let mark : 'a -> 'a Pos.marked = Pos.mark pos in
Bindlib.box @@ mark
@@ EInj (mark @@ ELit LUnit, 0, option_enum, [ (D.TLit D.TUnit, pos); (D.TAny, pos) ])
let make_some (e : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position @@ Bindlib.unbox e in
let mark : 'a -> 'a Pos.marked = Pos.mark pos in
let+ e = e in
mark @@ EInj (e, 1, option_enum, [ (D.TLit D.TUnit, pos); (D.TAny, pos) ])
(** [make_matchopt_with_abs_arms arg e_none e_some] build an expression
[match arg with |None -> e_none | Some -> e_some] and requires e_some and e_none to be in the
form [EAbs ...].*)
let make_matchopt_with_abs_arms (arg : expr Pos.marked Bindlib.box)
(e_none : expr Pos.marked Bindlib.box) (e_some : expr Pos.marked Bindlib.box) :
expr Pos.marked Bindlib.box =
let pos = Pos.get_position @@ Bindlib.unbox arg in
let mark : 'a -> 'a Pos.marked = Pos.mark pos in
let+ arg = arg and+ e_none = e_none and+ e_some = e_some in
mark @@ EMatch (arg, [ e_none; e_some ], option_enum)
(** [make_matchopt pos v tau arg e_none e_some] builds an expression
[match arg with | None () -> e_none | Some v -> e_some]. It binds v to e_some, permitting it to
be used inside the expression. There is no requirements on the form of both e_some and e_none. *)
let make_matchopt (pos : Pos.t) (v : Var.t) (tau : D.typ Pos.marked)
(arg : expr Pos.marked Bindlib.box) (e_none : expr Pos.marked Bindlib.box)
(e_some : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let x = Var.make ("_", pos) in
make_matchopt_with_abs_arms arg
(make_abs (Array.of_list [ x ]) e_none pos [ (D.TLit D.TUnit, pos) ] pos)
(make_abs (Array.of_list [ v ]) e_some pos [ tau ] pos)
let handle_default = Var.make ("handle_default", Pos.no_pos)
let handle_default_opt = Var.make ("handle_default_opt", Pos.no_pos)
type binder = (expr, expr Pos.marked) Bindlib.binder
type scope_body = {

31
compiler/lcalc/ast.mli
View File

@ -90,8 +90,39 @@ val make_let_in :
expr Pos.marked Bindlib.box ->
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
val option_enum_config : (Dcalc.Ast.EnumConstructor.t * Dcalc.Ast.typ Pos.marked) list
val make_none : Pos.t -> expr Pos.marked Bindlib.box
val make_some : expr Pos.marked Bindlib.box -> expr Pos.marked Bindlib.box
val make_matchopt_with_abs_arms :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box
val make_matchopt :
Pos.t ->
Var.t ->
Dcalc.Ast.typ Pos.marked ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box
(** [e' = make_matchopt'' pos v e e_none e_some] Builds the term corresponding to
[match e with | None -> fun () -> e_none |Some -> fun v -> e_some]. *)
val handle_default : Var.t
val handle_default_opt : Var.t
type binder = (expr, expr Pos.marked) Bindlib.binder
type scope_body = {

3
compiler/lcalc/compile_with_exceptions.mli
View File

@ -12,6 +12,7 @@
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
(** Translation from the default calculus to the lambda calculus *)
(** Translation from the default calculus to the lambda calculus. This translation uses exceptions
handle empty default terms. *)
val translate_program : Dcalc.Ast.program -> Ast.program

481
compiler/lcalc/compile_without_exceptions.ml Normal file
View File

@ -0,0 +1,481 @@
(* 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 = 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 same technique as in rust or erlang to handle
this kind of exceptions. Each [raise EmptyError] will be translated as [None] and each
[try e1 with EmtpyError -> e2] as [match e1 with | None -> e2 | Some x -> x].
When doing this naively, this requires to add matches and Some constructor everywhere. We apply
here an other technique where we generate what we call `hoists`. Hoists are expression whom
could minimally [raise EmptyError]. For instance in
[let x = <e1, e2, ..., en| e_just :- e_cons> * 3 in x + 1], the sub-expression
[<e1, e2, ..., en| e_just :- e_cons>] can produce an empty error. So we make a hoist with a new
variable [y] linked to the Dcalc expression [<e1, e2, ..., en| e_just :- e_cons>], and we return
as the translated expression [let x = y * 3 in x + 1].
The compilation of expressions is found in the functions [translate_and_hoist ctx e] and
[translate_expr ctx e]. Every option-generating expression when calling [translate_and_hoist]
will be hoisted and later handled by the [translate_expr] function. Every other cases is found
in the translate_and_hoist function. *)
type hoists = D.expr Pos.marked A.VarMap.t
(** Hoists definition. It represent bindings between [A.Var.t] and [D.expr]. *)
type info = { expr : A.expr Pos.marked Bindlib.box; var : A.expr Bindlib.var; is_pure : bool }
(** Information about each encontered Dcalc variable is stored inside a context : what is the
corresponding LCalc variable; an expression corresponding to the variable build correctly using
Bindlib, and a boolean `is_pure` indicating whenever the variable can be an EmptyError and hence
should be matched (false) or if it never can be EmptyError (true). *)
let pp_info (fmt : Format.formatter) (info : info) =
Format.fprintf fmt "{var: %a; is_pure: %b}" Print.format_var info.var info.is_pure
type ctx = {
decl_ctx : D.decl_ctx;
vars : info D.VarMap.t; (** information context about variables in the current scope *)
}
let _pp_ctx (fmt : Format.formatter) (ctx : ctx) =
let pp_binding (fmt : Format.formatter) ((v, info) : D.Var.t * info) =
Format.fprintf fmt "%a: %a" Dcalc.Print.format_var v pp_info info
in
let pp_bindings =
Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt "; ") pp_binding
in
Format.fprintf fmt "@[<2>[%a]@]" pp_bindings (D.VarMap.bindings ctx.vars)
(** [find ~info n ctx] is a warpper to ocaml's Map.find that handle errors in a slightly better way. *)
let find ?(info : string = "none") (n : D.Var.t) (ctx : ctx) : info =
(* let _ = Format.asprintf "Searching for variable %a inside context %a" Dcalc.Print.format_var n
pp_ctx ctx |> Cli.debug_print in *)
try D.VarMap.find n ctx.vars
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf
"Internal Error: Variable %a was not found in the current environment. Additional \
informations : %s."
Dcalc.Print.format_var n info)
Pos.no_pos
(** [add_var pos var is_pure ctx] add to the context [ctx] the Dcalc variable var, creating a unique
corresponding variable in Lcalc, with the corresponding expression, and the boolean is_pure. It
is usefull for debuging purposes as it printing each of the Dcalc/Lcalc variable pairs. *)
let add_var (pos : Pos.t) (var : D.Var.t) (is_pure : bool) (ctx : ctx) : ctx =
let new_var = A.Var.make (Bindlib.name_of var, pos) in
let expr = A.make_var (new_var, pos) in
(* Cli.debug_print @@ Format.asprintf "D.%a |-> A.%a" Dcalc.Print.format_var var Print.format_var
new_var; *)
{ ctx with vars = D.VarMap.update var (fun _ -> Some { expr; var = new_var; is_pure }) ctx.vars }
(** [tau' = translate_typ tau] translate the a dcalc type into a lcalc type.
Since positions where there is thunked expressions is exactly where we will put option
expressions. Hence, the transformation simply reduce [unit -> 'a] into ['a option] recursivly.
There is no polymorphism inside catala. *)
let rec translate_typ (tau : D.typ Pos.marked) : D.typ Pos.marked =
(Fun.flip Pos.same_pos_as) tau
begin
match Pos.unmark tau with
| D.TLit l -> D.TLit l
| D.TTuple (ts, s) -> D.TTuple (List.map translate_typ ts, s)
| D.TEnum (ts, en) -> D.TEnum (List.map translate_typ ts, en)
| D.TAny -> D.TAny
| D.TArray ts -> D.TArray (translate_typ ts)
(* catala is not polymorphic *)
| D.TArrow ((D.TLit D.TUnit, pos_unit), t2) ->
D.TEnum ([ (D.TLit D.TUnit, pos_unit); translate_typ t2 ], A.option_enum) (* D.TAny *)
| D.TArrow (t1, t2) -> D.TArrow (translate_typ t1, translate_typ t2)
end
let translate_lit (l : D.lit) (pos : Pos.t) : A.lit =
match l with
| D.LBool l -> A.LBool l
| D.LInt i -> A.LInt i
| D.LRat r -> A.LRat r
| D.LMoney m -> A.LMoney m
| D.LUnit -> A.LUnit
| D.LDate d -> A.LDate d
| D.LDuration d -> A.LDuration d
| D.LEmptyError ->
Errors.raise_spanned_error
"Internal Error: An empty error was found in a place that shouldn't be possible." pos
(** [c = disjoint_union_maps cs] Compute the disjoint union of multiple maps. Raises an internal
error if there is two identicals keys in differnts parts. *)
let disjoint_union_maps (pos : Pos.t) (cs : 'a A.VarMap.t list) : 'a A.VarMap.t =
let disjoint_union =
A.VarMap.union (fun _ _ _ ->
Errors.raise_spanned_error
"Internal Error: Two supposed to be disjoints maps have one shared key." pos)
in
List.fold_left disjoint_union A.VarMap.empty cs
(** [e' = translate_and_hoist ctx e ] Translate the Dcalc expression e into an expression in Lcalc,
given we translate each hoists correctly. It ensures the equivalence between the execution of e
and the execution of e' are equivalent in an environement where each variable v, where (v, e_v)
is in hoists, has the non-empty value in e_v. *)
let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
A.expr Pos.marked Bindlib.box * hoists =
let pos = Pos.get_position e in
match Pos.unmark e with
(* empty-producing/using terms. We hoist those. (D.EVar in some cases, EApp(D.EVar _, [ELit
LUnit]), EDefault _, ELit LEmptyDefault) I'm unsure about assert. *)
| D.EVar v ->
(* todo: for now, every unpure (such that [is_pure] is [false] in the current context) is
thunked, hence matched in the next case. This assumption can change in the future, and this
case is here for this reason. *)
let v, pos_v = v in
if not (find ~info:"search for a variable" v ctx).is_pure then
let v' = A.Var.make (Bindlib.name_of v, pos_v) in
(* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a, created a variable %a to
replace it" Dcalc.Print.format_var v Print.format_var v'; *)
(A.make_var (v', pos), A.VarMap.singleton v' e)
else ((find ~info:"should never happend" v ctx).expr, A.VarMap.empty)
| D.EApp ((D.EVar (v, pos_v), p), [ (D.ELit D.LUnit, _) ]) ->
if not (find ~info:"search for a variable" v ctx).is_pure then
let v' = A.Var.make (Bindlib.name_of v, pos_v) in
(* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a, created a variable %a to
replace it" Dcalc.Print.format_var v Print.format_var v'; *)
(A.make_var (v', pos), A.VarMap.singleton v' (D.EVar (v, pos_v), p))
else
Errors.raise_spanned_error
"Internal error: an pure variable was found in an unpure environment." pos
| D.EDefault (_exceptions, _just, _cons) ->
let v' = A.Var.make ("default_term", pos) in
(A.make_var (v', pos), A.VarMap.singleton v' e)
| D.ELit D.LEmptyError ->
let v' = A.Var.make ("empty_litteral", pos) in
(A.make_var (v', pos), A.VarMap.singleton v' e)
(* This one is a very special case. It transform an unpure expression environement to a pure
expression. *)
| ErrorOnEmpty arg ->
(* [ match arg with | None -> raise NoValueProvided | Some v -> {{ v }} ] *)
let silent_var = A.Var.make ("_", pos) in
let x = A.Var.make ("non_empty_argument", pos) in
let arg' = translate_expr ctx arg in
( A.make_matchopt_with_abs_arms arg'
(A.make_abs [| silent_var |]
(Bindlib.box (A.ERaise A.NoValueProvided, pos))
pos [ (D.TAny, pos) ] pos)
(A.make_abs [| x |] (A.make_var (x, pos)) pos [ (D.TAny, pos) ] pos),
A.VarMap.empty )
(* pure terms *)
| D.ELit l -> (Bindlib.box (A.ELit (translate_lit l pos), pos), A.VarMap.empty)
| D.EIfThenElse (e1, e2, e3) ->
let e1', h1 = translate_and_hoist ctx e1 in
let e2', h2 = translate_and_hoist ctx e2 in
let e3', h3 = translate_and_hoist ctx e3 in
let e' =
Bindlib.box_apply3 (fun e1' e2' e3' -> (A.EIfThenElse (e1', e2', e3'), pos)) e1' e2' e3'
in
(*(* equivalent code : *) let e' = let+ e1' = e1' and+ e2' = e2' and+ e3' = e3' in
(A.EIfThenElse (e1', e2', e3'), pos) in *)
(e', disjoint_union_maps pos [ h1; h2; h3 ])
| D.EAssert e1 ->
(* same behavior as in the ICFP paper: if e1 is empty, then no error is raised. *)
let e1', h1 = translate_and_hoist ctx e1 in
(Bindlib.box_apply (fun e1' -> (A.EAssert e1', pos)) e1', h1)
| D.EAbs ((binder, pos_binder), ts) ->
let vars, body = Bindlib.unmbind binder in
let ctx, lc_vars =
ArrayLabels.fold_right vars ~init:(ctx, []) ~f:(fun var (ctx, lc_vars) ->
(* we suppose the invariant that when applying a function, its arguments cannot be of
the type "option".
The code should behave correctly in the without this assumption if we put here an
is_pure=false, but the types are more compilcated. (unimplemented for now) *)
let ctx = add_var pos var true ctx in
let lc_var = (find var ctx).var in
(ctx, lc_var :: lc_vars))
in
let lc_vars = Array.of_list lc_vars in
(* here we take the guess that if we cannot build the closure because one of the variable is
empty, then we cannot build the function. *)
let new_body, hoists = translate_and_hoist ctx body in
let new_binder = Bindlib.bind_mvar lc_vars new_body in
( Bindlib.box_apply
(fun new_binder -> (A.EAbs ((new_binder, pos_binder), List.map translate_typ ts), pos))
new_binder,
hoists )
| EApp (e1, args) ->
let e1', h1 = translate_and_hoist ctx e1 in
let args', h_args = args |> List.map (translate_and_hoist ctx) |> List.split in
let hoists = disjoint_union_maps pos (h1 :: h_args) in
let e' =
Bindlib.box_apply2
(fun e1' args' -> (A.EApp (e1', args'), pos))
e1' (Bindlib.box_list args')
in
(e', hoists)
| ETuple (args, s) ->
let args', h_args = args |> List.map (translate_and_hoist ctx) |> List.split in
let hoists = disjoint_union_maps pos h_args in
(Bindlib.box_apply (fun args' -> (A.ETuple (args', s), pos)) (Bindlib.box_list args'), hoists)
| ETupleAccess (e1, i, s, ts) ->
let e1', hoists = translate_and_hoist ctx e1 in
let e1' = Bindlib.box_apply (fun e1' -> (A.ETupleAccess (e1', i, s, ts), pos)) e1' in
(e1', hoists)
| EInj (e1, i, en, ts) ->
let e1', hoists = translate_and_hoist ctx e1 in
let e1' = Bindlib.box_apply (fun e1' -> (A.EInj (e1', i, en, ts), pos)) e1' in
(e1', hoists)
| EMatch (e1, cases, en) ->
let e1', h1 = translate_and_hoist ctx e1 in
let cases', h_cases = cases |> List.map (translate_and_hoist ctx) |> List.split in
let hoists = disjoint_union_maps pos (h1 :: h_cases) in
let e' =
Bindlib.box_apply2
(fun e1' cases' -> (A.EMatch (e1', cases', en), pos))
e1' (Bindlib.box_list cases')
in
(e', hoists)
| EArray es ->
let es', hoists = es |> List.map (translate_and_hoist ctx) |> List.split in
( Bindlib.box_apply (fun es' -> (A.EArray es', pos)) (Bindlib.box_list es'),
disjoint_union_maps pos hoists )
| EOp op -> (Bindlib.box (A.EOp op, pos), A.VarMap.empty)
and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Pos.marked) :
A.expr Pos.marked Bindlib.box =
let e', hoists = translate_and_hoist ctx e in
let hoists = A.VarMap.bindings hoists in
let _pos = Pos.get_position e in
(* build the hoists *)
(* Cli.debug_print @@ Format.asprintf "hoist for the expression: [%a]" (Format.pp_print_list
Print.format_var) (List.map fst hoists); *)
ListLabels.fold_left hoists
~init:(if append_esome then A.make_some e' else e')
~f:(fun acc (v, (hoist, pos_hoist)) ->
(* Cli.debug_print @@ Format.asprintf "hoist using A.%a" Print.format_var v; *)
let c' : A.expr Pos.marked Bindlib.box =
match hoist with
(* Here we have to handle only the cases appearing in hoists, as defined the
[translate_and_hoist] function. *)
| D.EVar v -> (find ~info:"should never happend" (Pos.unmark v) ctx).expr
| D.EDefault (excep, just, cons) ->
let excep' = List.map (translate_expr ctx) excep in
let just' = translate_expr ctx just in
let cons' = translate_expr ctx cons in
(* calls handle_option. *)
A.make_app
(A.make_var (A.handle_default_opt, pos_hoist))
[
Bindlib.box_apply
(fun excep' -> (A.EArray excep', pos_hoist))
(Bindlib.box_list excep');
just';
cons';
]
pos_hoist
| D.ELit D.LEmptyError -> A.make_none pos_hoist
| D.EAssert arg ->
let arg' = translate_expr ctx arg in
(* [ match arg with | None -> raise NoValueProvided | Some v -> assert {{ v }} ] *)
let silent_var = A.Var.make ("_", pos_hoist) in
let x = A.Var.make ("assertion_argument", pos_hoist) in
A.make_matchopt_with_abs_arms arg'
(A.make_abs [| silent_var |]
(Bindlib.box (A.ERaise A.NoValueProvided, pos_hoist))
pos_hoist [ (D.TAny, pos_hoist) ] pos_hoist)
(A.make_abs [| x |]
(Bindlib.box_apply
(fun arg -> (A.EAssert arg, pos_hoist))
(A.make_var (x, pos_hoist)))
pos_hoist [ (D.TAny, pos_hoist) ] pos_hoist)
| _ ->
Errors.raise_spanned_error
"Internal Error: An term was found in a position where it should not be" pos_hoist
in
(* [ match {{ c' }} with | None -> None | Some {{ v }} -> {{ acc }} end ] *)
(* Cli.debug_print @@ Format.asprintf "build matchopt using %a" Print.format_var v; *)
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) =
match lets with
| Result e -> translate_expr ~append_esome:false ctx e
| ScopeLet
{
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = typ;
scope_let_expr = D.EAbs ((binder, _), _), _pos;
scope_let_next = next;
scope_let_pos = pos;
} ->
(* special case : the subscope variable is thunked (context i/o). We remove this thunking. *)
let _, expr = Bindlib.unmbind binder in
let var_is_pure = true in
let var, next = Bindlib.unbind next in
(* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var var; *)
let ctx' = add_var pos var var_is_pure ctx in
let new_var = (find ~info:"variable that was just created" var ctx').var in
A.make_let_in new_var (translate_typ typ)
(translate_expr ctx ~append_esome:false expr)
(translate_scope_let ctx' next)
| ScopeLet
{
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = typ;
scope_let_expr = (D.ErrorOnEmpty _, _) as expr;
scope_let_next = next;
scope_let_pos = pos;
} ->
(* special case: regular input to the subscope *)
let var_is_pure = true in
let var, next = Bindlib.unbind next in
(* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var var; *)
let ctx' = add_var pos var var_is_pure ctx in
let new_var = (find ~info:"variable that was just created" var ctx').var in
A.make_let_in new_var (translate_typ typ)
(translate_expr ctx ~append_esome:false expr)
(translate_scope_let ctx' next)
| ScopeLet
{ scope_let_kind = SubScopeVarDefinition; scope_let_pos = pos; scope_let_expr = expr; _ } ->
Errors.raise_spanned_error
(Format.asprintf
"Internal Error: found an SubScopeVarDefinition that does not satisfy the invariants \
when translating Dcalc to Lcalc without exceptions: @[<hov 2>%a@]"
(Dcalc.Print.format_expr ctx.decl_ctx)
expr)
pos
| ScopeLet
{
scope_let_kind = kind;
scope_let_typ = typ;
scope_let_expr = expr;
scope_let_next = next;
scope_let_pos = pos;
} ->
let var_is_pure =
match kind with
| DestructuringInputStruct -> (
(* Here, we have to distinguish between context and input variables. We can do so by
looking at the typ of the destructuring: if it's thunked, then the variable is
context. If it's not thunked, it's a regular input. *)
match Pos.unmark typ with D.TArrow ((D.TLit D.TUnit, _), _) -> false | _ -> true)
| ScopeVarDefinition | SubScopeVarDefinition | CallingSubScope
| DestructuringSubScopeResults | Assertion ->
true
in
let var, next = Bindlib.unbind next in
(* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var var; *)
let ctx' = add_var pos var var_is_pure ctx in
let new_var = (find ~info:"variable that was just created" var ctx').var in
A.make_let_in new_var (translate_typ typ)
(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) :
A.expr Pos.marked Bindlib.box =
match body with
| {
scope_body_result = result;
scope_body_input_struct = input_struct;
scope_body_output_struct = _output_struct;
} ->
let v, lets = Bindlib.unbind result in
let ctx' = add_var scope_pos v true ctx in
let v' = (find ~info:"variable that was just created" v ctx').var in
A.make_abs [| v' |] (translate_scope_let ctx' lets) Pos.no_pos
[ (D.TTuple ([], Some input_struct), Pos.no_pos) ]
Pos.no_pos
let rec translate_scopes (ctx : ctx) (scopes : scopes) : Ast.scope_body list Bindlib.box =
match scopes with
| Nil -> Bindlib.box []
| ScopeDef { scope_name; scope_body; scope_next } ->
let scope_var, next = Bindlib.unbind scope_next in
let new_ctx = add_var Pos.no_pos scope_var true ctx in
let new_scope_name = (find ~info:"variable that was just created" scope_var new_ctx).var in
let scope_pos = Pos.get_position (D.ScopeName.get_info scope_name) in
let new_body = translate_scope_body scope_pos ctx scope_body in
let tail = translate_scopes new_ctx next in
Bindlib.box_apply2
(fun body tail ->
{
Ast.scope_body_var = new_scope_name;
scope_body_name = scope_name;
scope_body_expr = body;
}
:: tail)
new_body tail
let translate_scopes (ctx : ctx) (scopes : 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)
in
(* Cli.debug_print @@ Format.asprintf "List of structs to modify: [%a]" (Format.pp_print_list
D.StructName.format_t) inputs_structs; *)
let decl_ctx =
{
prgm.decl_ctx with
D.ctx_enums = prgm.decl_ctx.ctx_enums |> D.EnumMap.add A.option_enum A.option_enum_config;
}
in
let decl_ctx =
{
decl_ctx with
D.ctx_structs =
prgm.decl_ctx.ctx_structs
|> D.StructMap.mapi (fun n l ->
if List.mem n inputs_structs then
ListLabels.map l ~f:(fun (n, tau) ->
(* Cli.debug_print @@ Format.asprintf "Input type: %a" (Dcalc.Print.format_typ
decl_ctx) tau; Cli.debug_print @@ Format.asprintf "Output type: %a"
(Dcalc.Print.format_typ decl_ctx) (translate_typ tau); *)
(n, translate_typ tau))
else l);
}
in
let scopes =
prgm.scopes |> bind_scopes |> Bindlib.unbox
|> translate_scopes { decl_ctx; vars = D.VarMap.empty }
in
{ scopes; decl_ctx }

19
compiler/lcalc/compile_without_exceptions.mli Normal file
View File

@ -0,0 +1,19 @@
(* This file is part of the Catala compiler, a specification language for tax and social benefits
computation rules. Copyright (C) 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. *)
(** Translation from the default calculus to the lambda calculus. This translation uses an option
monad to handle empty defaults terms. This transformation is one piece to permit to compile
toward legacy languages that does not contains exceptions. *)
val translate_program : Dcalc.Ast.program -> Ast.program

4
compiler/lcalc/dune
View File

@ -1,7 +1,9 @@
(library
(name lcalc)
(public_name catala.lcalc)
(libraries bindlib dcalc scopelang runtime))
(libraries bindlib dcalc scopelang runtime)
(preprocess
(pps visitors.ppx)))
(documentation
(package catala)

148
compiler/lcalc/optimizations.ml
View File

@ -14,58 +14,124 @@
open Utils
open Ast
let rec peephole_expr (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let ( let+ ) x f = Bindlib.box_apply f x
let ( and+ ) x y = Bindlib.box_pair x y
let visitor_map (t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box) (ctx : 'a)
(e : expr Pos.marked) : expr Pos.marked Bindlib.box =
(* calls [t ctx] on every direct childs of [e], then rebuild an abstract syntax tree modified.
Used in other transformations. *)
let default_mark e' = Pos.same_pos_as e' e in
match Pos.unmark e with
| EVar (v, pos) -> Bindlib.box_apply (fun v -> (v, pos)) (Bindlib.box_var v)
| EVar (v, pos) ->
let+ v = Bindlib.box_var v in
(v, pos)
| ETuple (args, n) ->
Bindlib.box_apply
(fun args -> (ETuple (args, n), Pos.get_position e))
(Bindlib.box_list (List.map peephole_expr args))
let+ args = args |> List.map (t ctx) |> Bindlib.box_list in
default_mark @@ ETuple (args, n)
| ETupleAccess (e1, i, n, ts) ->
Bindlib.box_apply
(fun e1 -> (ETupleAccess (e1, i, n, ts), Pos.get_position e))
(peephole_expr e1)
let+ e1 = t ctx e1 in
default_mark @@ ETupleAccess (e1, i, n, ts)
| EInj (e1, i, n, ts) ->
Bindlib.box_apply (fun e1 -> (EInj (e1, i, n, ts), Pos.get_position e)) (peephole_expr e1)
let+ e1 = t ctx e1 in
default_mark @@ EInj (e1, i, n, ts)
| EMatch (arg, cases, n) ->
Bindlib.box_apply2
(fun arg cases -> (EMatch (arg, cases, n), Pos.get_position e))
(peephole_expr arg)
(Bindlib.box_list (List.map peephole_expr cases))
let+ arg = t ctx arg and+ cases = cases |> List.map (t ctx) |> Bindlib.box_list in
default_mark @@ EMatch (arg, cases, n)
| EArray args ->
Bindlib.box_apply
(fun args -> (EArray args, Pos.get_position e))
(Bindlib.box_list (List.map peephole_expr args))
let+ args = args |> List.map (t ctx) |> Bindlib.box_list in
default_mark @@ EArray args
| EAbs ((binder, pos_binder), ts) ->
let vars, body = Bindlib.unmbind binder in
let body = peephole_expr body in
Bindlib.box_apply
(fun binder -> (EAbs ((binder, pos_binder), ts), Pos.get_position e))
(Bindlib.bind_mvar vars body)
let body = t ctx body in
let+ binder = Bindlib.bind_mvar vars body in
default_mark @@ EAbs ((binder, pos_binder), ts)
| EApp (e1, args) ->
Bindlib.box_apply2
(fun e1 args -> (EApp (e1, args), Pos.get_position e))
(peephole_expr e1)
(Bindlib.box_list (List.map peephole_expr args))
| EAssert e1 -> Bindlib.box_apply (fun e1 -> (EAssert e1, Pos.get_position e)) (peephole_expr e1)
let+ e1 = t ctx e1 and+ args = args |> List.map (t ctx) |> Bindlib.box_list in
default_mark @@ EApp (e1, args)
| EAssert e1 ->
let+ e1 = t ctx e1 in
default_mark @@ EAssert e1
| EIfThenElse (e1, e2, e3) ->
Bindlib.box_apply3
(fun e1 e2 e3 ->
match Pos.unmark e1 with
| ELit (LBool true) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ]) -> e2
| ELit (LBool false) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ]) -> e3
| _ -> (EIfThenElse (e1, e2, e3), Pos.get_position e))
(peephole_expr e1) (peephole_expr e2) (peephole_expr e3)
let+ e1 = t ctx e1 and+ e2 = t ctx e2 and+ e3 = t ctx e3 in
default_mark @@ EIfThenElse (e1, e2, e3)
| ECatch (e1, exn, e2) ->
Bindlib.box_apply2
(fun e1 e2 ->
( (match Pos.unmark e2 with
| ERaise exn2 when exn2 = exn -> Pos.unmark e1
| _ -> ECatch (e1, exn, e2)),
Pos.get_position e ))
(peephole_expr e1) (peephole_expr e2)
let+ e1 = t ctx e1 and+ e2 = t ctx e2 in
default_mark @@ ECatch (e1, exn, e2)
| ERaise _ | ELit _ | EOp _ -> Bindlib.box e
let rec iota_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let default_mark e' = Pos.mark (Pos.get_position e) e' in
match Pos.unmark e with
| EMatch ((EInj (e1, i, n', _ts), _), cases, n) when Dcalc.Ast.EnumName.compare n n' = 0 ->
let+ e1 = visitor_map iota_expr () e1
and+ case = visitor_map iota_expr () (List.nth cases i) in
default_mark @@ EApp (case, [ e1 ])
| EMatch (e', cases, n)
when cases
|> List.mapi (fun i (case, _pos) ->
match case with
| EInj (_ei, i', n', _ts') ->
i = i' && (* n = n' *) Dcalc.Ast.EnumName.compare n n' = 0
| _ -> false)
|> List.for_all Fun.id ->
visitor_map iota_expr () e'
| _ -> visitor_map iota_expr () e
let rec beta_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let default_mark e' = Pos.same_pos_as e' e in
match Pos.unmark e with
| EApp (e1, args) -> (
let+ e1 = beta_expr () e1 and+ args = List.map (beta_expr ()) args |> Bindlib.box_list in
match Pos.unmark e1 with
| EAbs ((binder, _pos_binder), _ts) ->
let (_ : (_, _) Bindlib.mbinder) = binder in
Bindlib.msubst binder (List.map fst args |> Array.of_list)
| _ -> default_mark @@ EApp (e1, args))
| _ -> visitor_map beta_expr () e
let iota_optimizations (p : program) : program =
{
p with
scopes =
List.map
(fun scope_body ->
{
scope_body with
scope_body_expr = Bindlib.unbox (iota_expr () scope_body.scope_body_expr);
})
p.scopes;
}
(* TODO: beta optimizations apply inlining of the program. We left the inclusion of
beta-optimization as future work since its produce code that is harder to read, and can produce
exponential blowup of the size of the generated program. *)
let _beta_optimizations (p : program) : program =
{
p with
scopes =
List.map
(fun scope_body ->
{
scope_body with
scope_body_expr = Bindlib.unbox (beta_expr () scope_body.scope_body_expr);
})
p.scopes;
}
let rec peephole_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let default_mark e' = Pos.mark (Pos.get_position e) e' in
match Pos.unmark e with
| EIfThenElse (e1, e2, e3) -> (
let+ e1 = peephole_expr () e1 and+ e2 = peephole_expr () e2 and+ e3 = peephole_expr () e3 in
match Pos.unmark e1 with
| ELit (LBool true) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ]) -> e2
| ELit (LBool false) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ]) -> e3
| _ -> default_mark @@ EIfThenElse (e1, e2, e3))
| _ -> visitor_map peephole_expr () e
let peephole_optimizations (p : program) : program =
{
p with
@ -74,9 +140,9 @@ let peephole_optimizations (p : program) : program =
(fun scope_body ->
{
scope_body with
scope_body_expr = Bindlib.unbox (peephole_expr scope_body.scope_body_expr);
scope_body_expr = Bindlib.unbox (peephole_expr () scope_body.scope_body_expr);
})
p.scopes;
}
let optimize_program (p : program) : program = peephole_optimizations p
let optimize_program (p : program) : program = p |> iota_optimizations |> peephole_optimizations

4
compiler/lcalc/print.ml
View File

@ -63,7 +63,7 @@ let needs_parens (e : expr Pos.marked) : bool =
match Pos.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false
let format_var (fmt : Format.formatter) (v : Var.t) : unit =
Format.fprintf fmt "%s" (Bindlib.name_of v)
Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
let rec format_expr (ctx : Dcalc.Ast.decl_ctx) ?(debug : bool = false) (fmt : Format.formatter)
(e : expr Pos.marked) : unit =
@ -111,7 +111,7 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) ?(debug : bool = false) (fmt : Fo
(fst (List.nth (Dcalc.Ast.EnumMap.find en ctx.ctx_enums) n))
format_expr e
| EMatch (e, es, e_name) ->
Format.fprintf fmt "@[<hov 0>%a@ @[<hov 2>%a@]@ %a@ %a@]" format_keyword "match" format_expr e
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@]" format_keyword "match" format_expr e
format_keyword "with"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")

67
compiler/lcalc/to_ocaml.ml
View File

@ -17,6 +17,26 @@ open Ast
open Backends
module D = Dcalc.Ast
let find_struct (s : D.StructName.t) (ctx : D.decl_ctx) :
(D.StructFieldName.t * D.typ Pos.marked) list =
try D.StructMap.find s ctx.D.ctx_structs
with Not_found ->
let s_name, pos = D.StructName.get_info s in
Errors.raise_spanned_error
(Format.asprintf "Internal Error: Structure %s was not found in the current environment."
s_name)
pos
let find_enum (en : D.EnumName.t) (ctx : D.decl_ctx) : (D.EnumConstructor.t * D.typ Pos.marked) list
=
try D.EnumMap.find en ctx.D.ctx_enums
with Not_found ->
let en_name, pos = D.EnumName.get_info en in
Errors.raise_spanned_error
(Format.asprintf "Internal Error: Enumeration %s was not found in the current environment."
en_name)
pos
let format_lit (fmt : Format.formatter) (l : lit Pos.marked) : unit =
match Pos.unmark l with
| LBool b -> Dcalc.Print.format_lit fmt (Pos.same_pos_as (Dcalc.Ast.LBool b) l)
@ -41,14 +61,6 @@ let format_op_kind (fmt : Format.formatter) (k : Dcalc.Ast.op_kind) =
Format.fprintf fmt "%s"
(match k with KInt -> "!" | KRat -> "&" | KMoney -> "$" | KDate -> "@" | KDuration -> "^")
let format_log_entry (fmt : Format.formatter) (entry : Dcalc.Ast.log_entry) : unit =
Format.fprintf fmt "%s"
(match entry with
| VarDef _ -> ":="
| BeginCall -> "→ "
| EndCall -> "← "
| PosRecordIfTrueBool -> "☛ ")
let format_binop (fmt : Format.formatter) (op : Dcalc.Ast.binop Pos.marked) : unit =
match Pos.unmark op with
| Add k -> Format.fprintf fmt "+%a" format_op_kind k
@ -88,9 +100,10 @@ let format_unop (fmt : Format.formatter) (op : Dcalc.Ast.unop Pos.marked) : unit
match Pos.unmark op with
| Minus k -> Format.fprintf fmt "~-%a" format_op_kind k
| Not -> Format.fprintf fmt "%s" "not"
| Log (entry, infos) ->
Format.fprintf fmt "@[<hov 2>log_entry@ \"%a|%a\"@]" format_log_entry entry format_uid_list
infos
| Log (_entry, _infos) ->
Errors.raise_spanned_error
"Internal error: a log operator has not been caught by the expression match"
(Pos.get_position op)
| Length -> Format.fprintf fmt "%s" "array_length"
| IntToRat -> Format.fprintf fmt "%s" "decimal_of_integer"
| GetDay -> Format.fprintf fmt "%s" "day_of_month_of_date"
@ -158,10 +171,16 @@ let rec format_typ (fmt : Format.formatter) (typ : Dcalc.Ast.typ Pos.marked) : u
Format.fprintf fmt "@[<hov 2>(%a)@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ *@ ")
(fun fmt t -> Format.fprintf fmt "%a" format_typ_with_parens t))
format_typ_with_parens)
ts
| TTuple (_, Some s) -> Format.fprintf fmt "%a" format_struct_name s
| TEnum (_, e) -> Format.fprintf fmt "%a" format_enum_name e
| TEnum ([ t ], e) when D.EnumName.compare e Ast.option_enum = 0 ->
Format.fprintf fmt "@[<hov 2>(%a)@] %a" format_typ_with_parens t format_enum_name e
| TEnum (_, e) when D.EnumName.compare e Ast.option_enum = 0 ->
Errors.raise_spanned_error
"Internal Error: found an typing parameter for an eoption type of the wrong lenght."
(Pos.get_position typ)
| TEnum (_ts, e) -> Format.fprintf fmt "%a" format_enum_name e
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a ->@ %a@]" format_typ_with_parens t1 format_typ_with_parens t2
| TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ_with_parens t1
@ -173,8 +192,10 @@ let format_var (fmt : Format.formatter) (v : Var.t) : unit =
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\\.") ~subst:(fun _ -> "_dot_") lowercase_name
in
let lowercase_name = avoid_keywords (to_ascii lowercase_name) in
if lowercase_name = "handle_default" || Dcalc.Print.begins_with_uppercase (Bindlib.name_of v) then
Format.fprintf fmt "%s" lowercase_name
if
List.mem lowercase_name [ "handle_default"; "handle_default_opt" ]
|| Dcalc.Print.begins_with_uppercase (Bindlib.name_of v)
then Format.fprintf fmt "%s" lowercase_name
else if lowercase_name = "_" then Format.fprintf fmt "%s" lowercase_name
else Format.fprintf fmt "%s_" lowercase_name
@ -220,7 +241,7 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e : exp
(fun fmt (e, struct_field) ->
Format.fprintf fmt "@[<hov 2>%a =@ %a@]" format_struct_field_name struct_field
format_with_parens e))
(List.combine es (List.map fst (Dcalc.Ast.StructMap.find s ctx.ctx_structs)))
(List.combine es (List.map fst (find_struct s ctx)))
| EArray es ->
Format.fprintf fmt "@[<hov 2>[|%a|]@]"
(Format.pp_print_list
@ -238,10 +259,10 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e : exp
format_with_parens e1
| Some s ->
Format.fprintf fmt "%a.%a" format_with_parens e1 format_struct_field_name
(fst (List.nth (Dcalc.Ast.StructMap.find s ctx.ctx_structs) n)))
(fst (List.nth (find_struct s ctx) n)))
| EInj (e, n, en, _ts) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_enum_cons_name
(fst (List.nth (Dcalc.Ast.EnumMap.find en ctx.ctx_enums) n))
(fst (List.nth (find_enum en ctx) n))
format_with_parens e
| EMatch (e, es, e_name) ->
Format.fprintf fmt "@[<hov 2>match@ %a@]@ with@\n%a" format_with_parens e
@ -261,13 +282,13 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e : exp
| _ -> assert false
(* should not happen *))
e))
(List.combine es (List.map fst (Dcalc.Ast.EnumMap.find e_name ctx.ctx_enums)))
(List.combine es (List.map fst (find_enum e_name ctx)))
| ELit l -> Format.fprintf fmt "%a" format_lit (Pos.same_pos_as l e)
| EApp ((EAbs ((binder, _), taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> (x, tau, arg)) xs_tau args in
Format.fprintf fmt "%a%a"
Format.fprintf fmt "(%a%a)"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "")
(fun fmt (x, tau, arg) ->
@ -410,11 +431,9 @@ let format_ctx (type_ordering : Scopelang.Dependency.TVertex.t list) (fmt : Form
(fun struct_or_enum ->
match struct_or_enum with
| Scopelang.Dependency.TVertex.Struct s ->
Format.fprintf fmt "%a@\n@\n" format_struct_decl
(s, Dcalc.Ast.StructMap.find s ctx.Dcalc.Ast.ctx_structs)
Format.fprintf fmt "%a@\n@\n" format_struct_decl (s, find_struct s ctx)
| Scopelang.Dependency.TVertex.Enum e ->
Format.fprintf fmt "%a@\n@\n" format_enum_decl
(e, Dcalc.Ast.EnumMap.find e ctx.Dcalc.Ast.ctx_enums))
Format.fprintf fmt "%a@\n@\n" format_enum_decl (e, find_enum e ctx))
(type_ordering @ scope_structs)
let format_program (fmt : Format.formatter) (p : Ast.program)

17
compiler/runtime.ml
View File

@ -31,6 +31,8 @@ type source_position = {
law_headings : string list;
}
type 'a eoption = ENone of unit | ESome of 'a
exception EmptyError
exception AssertionFailed
@ -213,6 +215,21 @@ let handle_default : 'a. (unit -> 'a) array -> (unit -> bool) -> (unit -> 'a) ->
in
match except with Some x -> x | None -> if just () then cons () else raise EmptyError
let handle_default_opt (exceptions : 'a eoption array) (just : bool eoption) (cons : 'a eoption) :
'a eoption =
let except =
Array.fold_left
(fun acc except ->
match (acc, except) with
| ENone _, _ -> except
| ESome _, ENone _ -> acc
| ESome _, ESome _ -> raise ConflictError)
(ENone ()) exceptions
in
match except with
| ESome _ -> except
| ENone _ -> ( match just with ESome b -> if b then cons else ENone () | ENone _ -> ENone ())
let no_input : unit -> 'a = fun _ -> raise EmptyError
let ( *$ ) (i1 : money) (i2 : decimal) : money =

5
compiler/runtime.mli
View File

@ -33,6 +33,8 @@ type source_position = {
law_headings : string list;
}
type 'a eoption = ENone of unit | ESome of 'a
(** {1 Exceptions} *)
exception EmptyError
@ -173,6 +175,9 @@ val handle_default : (unit -> 'a) array -> (unit -> bool) -> (unit -> 'a) -> 'a
(** @raise EmptyError
@raise ConflictError *)
val handle_default_opt : 'a eoption array -> bool eoption -> 'a eoption -> 'a eoption
(** @raise ConflictError *)
val no_input : unit -> 'a
(**{1 Operators} *)

10
compiler/scalc/compile_from_lambda.ml
View File

@ -67,7 +67,6 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Pos.marked) : A.block * A.ex
([], []) args
in
let new_args = List.rev new_args in
let args_stmts = List.rev args_stmts in
(f_stmts @ args_stmts, (A.EApp (new_f, new_args), Pos.get_position expr))
| L.EArray args ->
let args_stmts, new_args =
@ -78,7 +77,6 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Pos.marked) : A.block * A.ex
([], []) args
in
let new_args = List.rev new_args in
let args_stmts = List.rev args_stmts in
(args_stmts, (A.EArray new_args, Pos.get_position expr))
| L.EOp op -> ([], (A.EOp op, Pos.get_position expr))
| L.ELit l -> ([], (A.ELit l, Pos.get_position expr))
@ -260,8 +258,12 @@ let translate_program (p : L.program) : A.program =
{ A.func_params = new_scope_params; A.func_body = new_scope_body };
}
:: new_scopes ))
( L.VarMap.singleton L.handle_default
(A.TopLevelName.fresh ("handle_default", Pos.no_pos)),
( (if !Cli.avoid_exceptions_flag then
L.VarMap.singleton L.handle_default_opt
(A.TopLevelName.fresh ("handle_default_opt", Pos.no_pos))
else
L.VarMap.singleton L.handle_default
(A.TopLevelName.fresh ("handle_default", Pos.no_pos))),
[] )
p.L.scopes
in

29
compiler/scalc/to_python.ml
View File

@ -147,6 +147,9 @@ let rec format_typ (fmt : Format.formatter) (typ : Dcalc.Ast.typ Pos.marked) : u
(fun fmt t -> Format.fprintf fmt "%a" format_typ_with_parens t))
ts
| TTuple (_, Some s) -> Format.fprintf fmt "%a" format_struct_name s
| TEnum ([ _; some_typ ], e) when D.EnumName.compare e L.option_enum = 0 ->
(* We translate the option type with an overloading by Python's [None] *)
Format.fprintf fmt "Optional[%a]" format_typ some_typ
| TEnum (_, e) -> Format.fprintf fmt "%a" format_enum_name e
| TArrow (t1, t2) ->
Format.fprintf fmt "Callable[[%a], %a]" format_typ_with_parens t1 format_typ_with_parens t2
@ -181,8 +184,8 @@ let format_exception (fmt : Format.formatter) (exc : L.except Pos.marked) : unit
| NoValueProvided ->
let pos = Pos.get_position exc in
Format.fprintf fmt
"NoValueProvided(SourcePosition(filename=\"%s\",@ start_line=%d,@ start_column=%d,@ \
end_line=%d,@ end_column=%d,@ law_headings=%a))"
"NoValueProvided(@[<hov 0>SourcePosition(@[<hov 0>filename=\"%s\",@ start_line=%d,@ \
start_column=%d,@ end_line=%d,@ end_column=%d,@ law_headings=%a)@])@]"
(Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list (Pos.get_law_info pos)
@ -201,6 +204,16 @@ let rec format_expression (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e
(List.combine es (List.map fst (Dcalc.Ast.StructMap.find s ctx.ctx_structs)))
| EStructFieldAccess (e1, field, _) ->
Format.fprintf fmt "%a.%a" (format_expression ctx) e1 format_struct_field_name field
| EInj (_, cons, e_name)
when D.EnumName.compare e_name L.option_enum = 0
&& D.EnumConstructor.compare cons L.none_constr = 0 ->
(* We translate the option type with an overloading by Python's [None] *)
Format.fprintf fmt "None"
| EInj (e, cons, e_name)
when D.EnumName.compare e_name L.option_enum = 0
&& D.EnumConstructor.compare cons L.some_constr = 0 ->
(* We translate the option type with an overloading by Python's [None] *)
format_expression ctx fmt e
| EInj (e, cons, enum_name) ->
Format.fprintf fmt "%a(%a_Code.%a,@ %a)" format_enum_name enum_name format_enum_name enum_name
format_enum_cons_name cons (format_expression ctx) e
@ -240,7 +253,7 @@ let rec format_expression (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e
| EApp ((EOp (Unop op), _), [ arg1 ]) ->
Format.fprintf fmt "%a(%a)" format_unop (op, Pos.no_pos) (format_expression ctx) arg1
| EApp (f, args) ->
Format.fprintf fmt "%a(%a)" (format_expression ctx) f
Format.fprintf fmt "%a(@[<hov 0>%a)@]" (format_expression ctx) f
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(format_expression ctx))
@ -270,6 +283,14 @@ let rec format_statement (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (s
| SIfThenElse (cond, b1, b2) ->
Format.fprintf fmt "@[<hov 4>if %a:@\n%a@]@\n@[<hov 4>else:@\n%a@]" (format_expression ctx)
cond (format_block ctx) b1 (format_block ctx) b2
| SSwitch (e1, e_name, [ (case_none, _); (case_some, case_some_var) ])
when D.EnumName.compare e_name L.option_enum = 0 ->
(* We translate the option type with an overloading by Python's [None] *)
let tmp_var = LocalName.fresh ("perhaps_none_arg", Pos.no_pos) in
Format.fprintf fmt
"%a = %a@\n@[<hov 4>if %a is None:@\n%a@]@\n@[<hov 4>else:@\n%a = %a@\n%a@]" format_var
tmp_var (format_expression ctx) e1 format_var tmp_var (format_block ctx) case_none
format_var case_some_var format_var tmp_var (format_block ctx) case_some
| SSwitch (e1, e_name, cases) ->
let cases =
List.map2 (fun (x, y) (cons, _) -> (x, y, cons)) cases (D.EnumMap.find e_name ctx.ctx_enums)
@ -406,6 +427,8 @@ let format_ctx (type_ordering : Scopelang.Dependency.TVertex.t list) (fmt : Form
let format_program (fmt : Format.formatter) (p : Ast.program)
(type_ordering : Scopelang.Dependency.TVertex.t list) : unit =
(* We disable the style flag in order to enjoy formatting from the pretty-printers of Dcalc and
Lcalc but without the color terminal markers. *)
Cli.style_flag := false;
Format.fprintf fmt
"# This file has been generated by the Catala compiler, do not edit!\n\

9
compiler/scopelang/scope_to_dcalc.ml
View File

@ -530,7 +530,14 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
(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_expr =
Bindlib.box_apply (fun new_e -> Pos.same_pos_as (Dcalc.Ast.EAssert new_e) e) new_e;
(* 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 ->
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;
};
],

9
compiler/utils/cli.ml
View File

@ -36,6 +36,8 @@ let optimize_flag = ref false
let disable_counterexamples = ref false
let avoid_exceptions_flag = ref false
open Cmdliner
let file =
@ -61,6 +63,11 @@ let trace_opt =
"Displays a trace of the interpreter's computation or generates logging instructions in \
translate programs.")
let avoid_exceptions =
Arg.(
value & flag
& info [ "avoid_exceptions" ] ~doc:"Compiles the default calculus without exceptions")
let wrap_weaved_output =
Arg.(
value & flag
@ -126,7 +133,7 @@ let output =
let catala_t f =
Term.(
const f $ file $ debug $ unstyled $ wrap_weaved_output $ backend $ language
const f $ file $ debug $ unstyled $ wrap_weaved_output $ avoid_exceptions $ backend $ language
$ max_prec_digits_opt $ trace_opt $ disable_counterexamples_opt $ optimize $ ex_scope $ output)
let version = "0.5.0"

6
compiler/utils/cli.mli
View File

@ -38,6 +38,9 @@ val trace_flag : bool ref
val disable_counterexamples : bool ref
(** Disables model-generated counterexamples for proofs that fail. *)
val avoid_exceptions_flag : bool ref
(** Avoids using [try ... with] exceptions when compiling the default calculus. *)
(** {2 CLI terms} *)
val file : string Cmdliner.Term.t
@ -79,6 +82,7 @@ val catala_t :
bool ->
bool ->
bool ->
bool ->
string ->
string option ->
int option ->
@ -90,7 +94,7 @@ val catala_t :
'a) ->
'a Cmdliner.Term.t
(** Main entry point:
[catala_t file debug unstyled wrap_weaved_output backend language max_prec_digits_opt trace_opt disable_counterexamples optimize ex_scope output] *)
[catala_t file debug unstyled wrap_weaved_output avoid_exceptions backend language max_prec_digits_opt trace_opt disable_counterexamples optimize ex_scope output] *)
val version : string

2
compiler/utils/pos.ml
View File

@ -175,6 +175,8 @@ let no_pos : t =
in
{ code_pos = (zero_pos, zero_pos); law_pos = [] }
let mark pos e : 'a marked = (e, pos)
let unmark ((x, _) : 'a marked) : 'a = x
let get_position ((_, x) : 'a marked) : t = x

2
compiler/utils/pos.mli
View File

@ -64,6 +64,8 @@ type 'a marked = 'a * t
val no_pos : t
(** Placeholder position *)
val mark : t -> 'a -> 'a marked
val unmark : 'a marked -> 'a
val get_position : 'a marked -> t

9
default.nix
View File

@ -19,15 +19,16 @@
, js_of_ocaml-ppx
, camomile
, cppo
, ppx_deriving
, z3
, menhirLib ? null #for nixos-unstable compatibility.
}:
buildDunePackage rec {
pname = "catala";
version = "0.3.0";
version = "0.5.0";
minimumOCamlVersion = "4.08";
minimumOCamlVersion = "4.11";
src = ./.;
@ -54,6 +55,8 @@ buildDunePackage rec {
pkgs.z3
ppx_deriving
unionfind
bindlib
] ++ (if isNull menhirLib then [ ] else [ menhirLib ]);
@ -68,4 +71,4 @@ buildDunePackage rec {
license = licenses.asl20;
maintainers = with maintainers; [ ];
};
}
}

4261
french_law/js/french_law.js generated
View File

File diff suppressed because one or more lines are too long

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

File diff suppressed because it is too large Load Diff

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

File diff suppressed because it is too large Load Diff

27
french_law/python/src/catala.py
View File

@ -12,7 +12,7 @@
from gmpy2 import log2, mpz, mpq, mpfr, t_divmod # type: ignore
import datetime
import dateutil.relativedelta
from typing import NewType, List, Callable, Tuple, Optional, TypeVar, Iterable, Union
from typing import NewType, List, Callable, Tuple, Optional, TypeVar, Iterable, Union, Any
from functools import reduce
from enum import Enum
import copy
@ -515,6 +515,31 @@ def handle_default(
return acc
def handle_default_opt(
exceptions: List[Optional[Any]],
just: Optional[bool],
cons: Optional[Alpha]
) -> Optional[Alpha]:
acc: Optional[Alpha] = None
for exception in exceptions:
if acc is None:
acc = exception
elif not (acc is None) and exception is None:
pass # acc stays the same
elif not (acc is None) and not (exception is None):
raise ConflictError
if acc is None:
if just is None:
return None
else:
if just:
return cons
else:
return None
else:
return acc
def no_input() -> Callable[[Unit], Alpha]:
def closure(_: Unit):
raise EmptyError

24
tests/test_bool/good/output/test_bool.catala_en.Dcalc
View File

@ -1,18 +1,18 @@
let TestBool_6 :
let TestBool_7 :
TestBool_in{"foo_in": unit → bool; "bar_in": unit → integer} →
TestBool_out{"foo_out": bool; "bar_out": integer} =
λ (TestBool_in_7: TestBool_in{"foo_in": unit → bool; "bar_in":
λ (TestBool_in_8: TestBool_in{"foo_in": unit → bool; "bar_in":
unit → integer}) →
let foo_8 : unit → bool = TestBool_in_7."foo_in" in
let bar_9 : unit → integer = TestBool_in_7."bar_in" in
let bar_10 : integer = error_empty
⟨bar_9 () | true ⊢
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 ⊢
⟨⟨true ⊢ ⟨⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
let foo_11 : bool = error_empty
⟨foo_8 () | true ⊢
⟨⟨true ⊢ ⟨⟨bar_10 < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩,
⟨true ⊢ ⟨⟨bar_10 >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
let foo_12 : bool = error_empty
⟨foo_9 () | true ⊢
⟨⟨true ⊢ ⟨⟨bar_11 < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩,
⟨true ⊢ ⟨⟨bar_11 >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
TestBool_out {"foo_out"= foo_11; "bar_out"= bar_10} in
TestBool_6
TestBool_out {"foo_out"= foo_12; "bar_out"= bar_11} in
TestBool_7

30
tests/test_io/good/output/all_io.catala_en.A.Dcalc
View File

@ -1,23 +1,23 @@
let A =
λ (A_in_10: A_in{"c_in": integer; "d_in": integer; "e_in":
λ (A_in_11: A_in{"c_in": integer; "d_in": integer; "e_in":
unit → integer; "f_in": unit → integer}) →
let c_11 : integer = A_in_10."c_in" in
let d_12 : integer = A_in_10."d_in" in
let e_13 : unit → integer = A_in_10."e_in" in
let f_14 : unit → integer = A_in_10."f_in" in
let a_15 : integer = error_empty
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
⟨⟨true ⊢ ⟨⟨true ⊢ 0⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
let b_16 : integer = error_empty
⟨⟨true ⊢ ⟨⟨true ⊢ a_15 + 1⟩ | false ⊢ ∅ ⟩⟩ | true
let b_17 : integer = error_empty
⟨⟨true ⊢ ⟨⟨true ⊢ a_16 + 1⟩ | false ⊢ ∅ ⟩⟩ | true
⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
let e_17 : integer = error_empty
⟨e_13 () | true ⊢
let e_18 : integer = error_empty
⟨e_14 () | true ⊢
⟨⟨true ⊢
⟨⟨true ⊢ b_16 + c_11 + d_12 + 1⟩ | false ⊢ ∅ ⟩⟩
⟨⟨true ⊢ b_17 + c_12 + d_13 + 1⟩ | false ⊢ ∅ ⟩⟩
| true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
let f_18 : integer = error_empty
⟨f_14 () | true ⊢
⟨⟨true ⊢ ⟨⟨true ⊢ e_17 + 1⟩ | false ⊢ ∅ ⟩⟩ |
let f_19 : integer = error_empty
⟨f_15 () | true ⊢
⟨⟨true ⊢ ⟨⟨true ⊢ e_18 + 1⟩ | false ⊢ ∅ ⟩⟩ |
true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
A_out {"b_out"= b_16; "d_out"= d_12; "f_out"= f_18}
A_out {"b_out"= b_17; "d_out"= d_13; "f_out"= f_19}

10
tests/test_io/good/output/condition_only_input.catala_en.B.Dcalc
View File

@ -1,8 +1,8 @@
let B =
λ (B_in_13: B_in{}) →
let a.x_14 : bool = error_empty
λ (B_in_14: B_in{}) →
let a.x_15 : bool = error_empty
⟨true ⊢ ⟨⟨true ⊢ false⟩ | false ⊢ ∅ ⟩⟩ in
let result_15 : A_out{"y_out": integer} = A_2 (A_in {"x_in"= a.x_14}) in
let a.y_16 : integer = result_15."y_out" in
let __17 : unit = assert (a.y_16 = 1) 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
B_out {}

2
tests/test_io/good/output/condition_only_input.catala_en.B.Interpret
View File

@ -1 +1 @@
[RESULT] Computation successful!
[RESULT] Computation successful!

14
tests/test_io/good/output/subscope.catala_en.B.Dcalc
View File

@ -1,11 +1,11 @@
let B =
λ (B_in_17: B_in{}) →
let a.a_18 : unit → integer = λ (__19: unit) → ∅ in
let a.b_20 : integer = error_empty
λ (B_in_18: B_in{}) →
let a.a_19 : unit → integer = λ (__20: unit) → ∅ in
let a.b_21 : integer = error_empty
⟨⟨true ⊢ ⟨⟨true ⊢ 2⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
let result_21 : A_out{"c_out": integer} =
A_2 (A_in {"a_in"= a.a_18; "b_in"= a.b_20}) in
let a.c_22 : integer = result_21."c_out" in
let __23 : unit = assert (a.c_22 = 1) 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
B_out {}