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

Implementing closure conversion (#475)

Browse Source
This commit is contained in:
Denis Merigoux 2023-06-22 12:30:54 +02:00 committed by GitHub
commit 3329a1b48b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
50 changed files with 7578 additions and 8480 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
catala_legifrance.opam
View File

@ -1,6 +1,6 @@
opam-version: "2.0"
version: "0.8.0"
synopsis: "Linter that queries the LégiFrance API to check for correctness and expiration of Catala programs."
synopsis: "Linter that queries the LégiFrance API to check for correctness and expiration of Catala programs"
maintainer: ["contact@catala-lang.org"]
authors: ["Denis Merigoux"]
license: "Apache-2.0"

32
compiler/catala_utils/message.ml
View File

@ -75,7 +75,7 @@ let print_time_marker =
time := new_time;
let delta = (new_time -. old_time) *. 1000. in
if delta > 50. then
Format.fprintf ppf "@{<bold;black>[TIME] %.0fms@}@," delta
Format.fprintf ppf "@{<bold;black>[TIME] %.0fms@}@ " delta
let pp_marker target ppf =
let open Ocolor_types in
@ -105,22 +105,28 @@ module Content = struct
let of_string (s : string) : t =
{ message = (fun ppf -> Format.pp_print_string ppf s); positions = [] }
let internal_error_prefix =
"Internal Error, please report to \
https://github.com/CatalaLang/catala/issues : "
let prepend_message (content : t) prefix : t =
{
content with
message = (fun ppf -> Format.fprintf ppf "%t@,%t" prefix content.message);
}
let mark_as_internal_error (content : t) : t =
{
content with
message =
(fun ppf ->
Format.fprintf ppf "%s@,%t" internal_error_prefix content.message);
}
end
open Content
let internal_error_prefix =
"Internal Error, please report to \
https://github.com/CatalaLang/catala/issues: "
let to_internal_error (content : Content.t) : Content.t =
{
content with
message =
(fun ppf ->
Format.fprintf ppf "%s@,%t" internal_error_prefix content.message);
}
let emit_content (content : Content.t) (target : content_type) : unit =
let { message; positions } = content in
match !Cli.message_format_flag with

4
compiler/catala_utils/message.mli
View File

@ -33,10 +33,10 @@ module Content : sig
val of_message : (Format.formatter -> unit) -> t
val of_string : string -> t
val mark_as_internal_error : t -> t
val prepend_message : t -> (Format.formatter -> unit) -> t
end
val to_internal_error : Content.t -> Content.t
type content_type = Error | Warning | Debug | Log | Result
val emit_content : Content.t -> content_type -> unit

53
compiler/driver.ml
View File

@ -312,7 +312,8 @@ let driver backend source_file (options : Cli.global_options) : int =
try Shared_ast.Typing.program prgm ~leave_unresolved:false
with Message.CompilerError error_content ->
raise
(Message.CompilerError (Message.to_internal_error error_content))
(Message.CompilerError
(Message.Content.mark_as_internal_error error_content))
in
(* That's it! *)
Message.emit_result "Typechecking successful!"
@ -347,7 +348,8 @@ let driver backend source_file (options : Cli.global_options) : int =
try Shared_ast.Typing.program ~leave_unresolved:false prgm
with Message.CompilerError error_content ->
raise
(Message.CompilerError (Message.to_internal_error error_content))
(Message.CompilerError
(Message.Content.mark_as_internal_error error_content))
in
if !Cli.check_invariants_flag then (
Message.emit_debug "Checking invariants...";
@ -377,7 +379,12 @@ let driver backend source_file (options : Cli.global_options) : int =
options.link_modules);
Message.emit_debug "Starting interpretation (dcalc)...";
let results =
Shared_ast.Interpreter.interpret_program_dcalc prgm scope_uid
try Shared_ast.Interpreter.interpret_program_dcalc prgm scope_uid
with Shared_ast.Interpreter.CatalaException exn ->
Message.raise_error
"During interpretation, the error %a has been raised but not \
caught!"
Shared_ast.Print.except exn
in
let results =
List.sort
@ -432,7 +439,10 @@ let driver backend source_file (options : Cli.global_options) : int =
Message.raise_error
"Option --avoid_exceptions must be enabled for \
--closure_conversion";
Message.emit_debug "Performing closure conversion...";
if not options.optimize then
Message.raise_error
"Option --optimize must be enabled for --closure_conversion"
Message.emit_debug "Performing closure conversion...";
let prgm = Lcalc.Closure_conversion.closure_conversion prgm in
let prgm = Bindlib.unbox prgm in
let prgm =
@ -442,11 +452,28 @@ let driver backend source_file (options : Cli.global_options) : int =
else prgm
in
Message.emit_debug "Retyping lambda calculus...";
let prgm =
Shared_ast.Program.untype
(Shared_ast.Typing.program ~leave_unresolved:true prgm)
in
prgm)
try
let prgm =
Shared_ast.Program.untype
(Shared_ast.Typing.program ~leave_unresolved:true prgm)
in
prgm
with Message.CompilerError content ->
raise
(Message.CompilerError
(Message.Content.prepend_message content (fun fmt ->
Format.fprintf fmt
"As part of the compilation process, one of the \
step (closure conversion) modified the Catala \
program and re-typing after this modification \
failed with the error message below. This \
re-typing error if not your fault, but is \
likely to indicate that the program you are \
trying to compile is incompatible with the \
current compilation scheme provided by the \
Catala compiler. Try to rewrite the program to \
avoid the problematic pattern or contact the \
compiler developers for help.@\n"))))
else prgm
in
match backend with
@ -465,7 +492,13 @@ let driver backend source_file (options : Cli.global_options) : int =
| `Interpret_Lcalc ->
Message.emit_debug "Starting interpretation (lcalc)...";
let results =
Shared_ast.Interpreter.interpret_program_lcalc prgm scope_uid
try
Shared_ast.Interpreter.interpret_program_lcalc prgm scope_uid
with Shared_ast.Interpreter.CatalaException exn ->
Message.raise_error
"During interpretation, the error %a has been raised but \
not caught!"
Shared_ast.Print.except exn
in
let results =
List.sort

4
compiler/index.mld
View File

@ -89,9 +89,9 @@ More documentation can be found on each intermediate representations here.
}
Most of these intermediate representations use a {{: shared_ast.html} shared AST libary}.
The main compilation chain is defined in:
The main compilation chain is defined in {!module: Driver}.
{!modules: Driver}
{!modules: Shared_ast Driver}
Additionally, the compiler features a verification plugin that generates
verification condition for proof backends. More information can be found here:

4
compiler/lcalc/ast.ml
View File

@ -113,13 +113,13 @@ module OptionMonad = struct
(List.to_seq
[
( Expr.none_constr,
let x = Var.make var_name in
let x = Var.make "_" in
Expr.eabs
(Expr.bind [| x |] (Expr.eraise NoValueProvided mark))
[TAny, Expr.mark_pos mark]
mark );
(* | None x -> raise NoValueProvided *)
Expr.some_constr, Expr.fun_id mark (* | Some x -> x*);
Expr.some_constr, Expr.fun_id ~var_name mark (* | Some x -> x*);
])
in
if toplevel then Expr.ematch arg Expr.option_enum cases mark

460
compiler/lcalc/closure_conversion.ml
View File

@ -19,9 +19,6 @@ open Shared_ast
open Ast
module D = Dcalc.Ast
(** TODO: This version is not yet debugged and ought to be specialized when
Lcalc has more structure. *)
type 'm ctx = {
decl_ctx : decl_ctx;
name_context : string;
@ -30,64 +27,7 @@ type 'm ctx = {
let tys_as_tanys tys = List.map (fun x -> Mark.map (fun _ -> TAny) x) tys
type 'm hoisted_closure = { name : 'm expr Var.t; closure : 'm expr }
let rec hoist_context_free_closures :
type m. m ctx -> m expr -> m hoisted_closure list * m expr boxed =
fun ctx e ->
let m = Mark.get e in
match Mark.remove e with
| EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ | EArray _
| ELit _ | EAssert _ | EOp _ | EIfThenElse _ | ERaise _ | ECatch _ | EVar _
| EExternal _ ->
Expr.map_gather ~acc:[] ~join:( @ ) ~f:(hoist_context_free_closures ctx) e
| EMatch { e; cases; name } ->
let collected_closures, new_e = (hoist_context_free_closures ctx) e 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 collected_closures, new_cases =
EnumConstructor.Map.fold
(fun cons e1 (collected_closures, new_cases) ->
match Mark.remove e1 with
| EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in
let new_collected_closures, new_body =
(hoist_context_free_closures ctx) body
in
let new_binder = Expr.bind vars new_body in
( collected_closures @ new_collected_closures,
EnumConstructor.Map.add cons
(Expr.eabs new_binder tys (Mark.get e1))
new_cases )
| _ -> failwith "should not happen")
cases
(collected_closures, EnumConstructor.Map.empty)
in
collected_closures, Expr.ematch new_e name new_cases m
| EApp { f = EAbs { binder; tys }, e1_pos; args } ->
(* let-binding, we should not close these *)
let vars, body = Bindlib.unmbind binder in
let collected_closures, new_body = (hoist_context_free_closures ctx) body in
let new_binder = Expr.bind vars new_body in
let collected_closures, new_args =
List.fold_right
(fun arg (collected_closures, new_args) ->
let new_collected_closures, new_arg =
(hoist_context_free_closures ctx) arg
in
collected_closures @ new_collected_closures, new_arg :: new_args)
args (collected_closures, [])
in
( collected_closures,
Expr.eapp (Expr.eabs new_binder (tys_as_tanys tys) e1_pos) new_args m )
| EAbs _ ->
(* this is the closure we want to hoist*)
let closure_var = Var.make ctx.name_context in
[{ name = closure_var; closure = e }], Expr.make_var closure_var m
| EApp _ ->
Expr.map_gather ~acc:[] ~join:( @ ) ~f:(hoist_context_free_closures ctx) e
| _ -> .
[@@warning "-32"]
(** { 1 Transforming closures}*)
(** Returns the expression with closed closures and the set of free variables
inside this new expression. Implementation guided by
@ -120,7 +60,9 @@ let rec transform_closures_expr :
let vars, body = Bindlib.unmbind binder in
let new_free_vars, new_body = (transform_closures_expr ctx) body in
let new_binder = Expr.bind vars new_body in
( Var.Set.union free_vars new_free_vars,
( Var.Set.union free_vars
(Var.Set.diff new_free_vars
(Var.Set.of_list (Array.to_list vars))),
EnumConstructor.Map.add cons
(Expr.eabs new_binder tys (Mark.get e1))
new_cases )
@ -159,28 +101,38 @@ let rec transform_closures_expr :
(* x1, ..., xn *)
let code_var = Var.make ctx.name_context in
(* code *)
let inner_c_var = Var.make "env" in
let closure_env_arg_var = Var.make "env" in
let closure_env_var = Var.make "env" in
let any_ty = TAny, binder_pos in
(* let env = from_closure_env env in let arg0 = env.0 in ... *)
let new_closure_body =
Expr.make_multiple_let_in
(Array.of_list extra_vars_list)
(List.map (fun _ -> any_ty) extra_vars_list)
(List.mapi
(fun i _ ->
Expr.etupleaccess
(Expr.evar inner_c_var binder_mark)
i
(List.length extra_vars_list)
binder_mark)
extra_vars_list)
new_body
(Expr.mark_pos binder_mark)
Expr.make_let_in closure_env_var any_ty
(Expr.eapp
(Expr.eop Operator.FromClosureEnv
[TClosureEnv, binder_pos]
binder_mark)
[Expr.evar closure_env_arg_var binder_mark]
binder_mark)
(Expr.make_multiple_let_in
(Array.of_list extra_vars_list)
(List.map (fun _ -> any_ty) extra_vars_list)
(List.mapi
(fun i _ ->
Expr.etupleaccess
(Expr.evar closure_env_var binder_mark)
i
(List.length extra_vars_list)
binder_mark)
extra_vars_list)
new_body binder_pos)
binder_pos
in
(* fun env arg0 ... -> new_closure_body *)
let new_closure =
Expr.make_abs
(Array.concat [Array.make 1 inner_c_var; vars])
(Array.concat [Array.make 1 closure_env_arg_var; vars])
new_closure_body
((TAny, binder_pos) :: tys)
((TClosureEnv, binder_pos) :: tys)
(Expr.pos e)
in
( extra_vars,
@ -190,14 +142,54 @@ let rec transform_closures_expr :
(Expr.etuple
((Bindlib.box_var code_var, binder_mark)
:: [
Expr.etuple
(List.map
(fun extra_var -> Bindlib.box_var extra_var, binder_mark)
extra_vars_list)
m;
Expr.eapp
(Expr.eop Operator.ToClosureEnv
[TAny, Expr.pos e]
(Mark.get e))
[
(if extra_vars_list = [] then Expr.elit LUnit binder_mark
else
Expr.etuple
(List.map
(fun extra_var ->
Bindlib.box_var extra_var, binder_mark)
extra_vars_list)
m);
]
(Mark.get e);
])
m)
(Expr.pos e) )
| EApp
{
f =
(EOp { op = HandleDefaultOpt | Fold | Map | Filter | Reduce; _ }, _)
as f;
args;
} ->
(* Special case for some operators: its arguments shall remain thunks (which
are closures) because if you want to extract it as a function you need
these closures to preserve evaluation order, but backends that don't
support closures will simply extract these operators in a inlined way and
skip the thunks. *)
let free_vars, new_args =
List.fold_right
(fun (arg : (lcalc, m) gexpr) (free_vars, new_args) ->
let m_arg = Mark.get arg in
match Mark.remove arg with
| EAbs { binder; tys } ->
let vars, arg = Bindlib.unmbind binder in
let new_free_vars, new_arg = (transform_closures_expr ctx) arg in
let new_arg =
Expr.make_abs vars new_arg tys (Expr.mark_pos m_arg)
in
Var.Set.union free_vars new_free_vars, new_arg :: new_args
| _ ->
let new_free_vars, new_arg = transform_closures_expr ctx arg in
Var.Set.union free_vars new_free_vars, new_arg :: new_args)
args (Var.Set.empty, [])
in
free_vars, Expr.eapp (Expr.box f) new_args (Mark.get e)
| EApp { f = EOp _, _; _ } ->
(* This corresponds to an operator call, which we don't want to transform*)
Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union
@ -243,7 +235,7 @@ let rec transform_closures_expr :
(* Here I have to reimplement Scope.map_exprs_in_lets because I'm changing the
type *)
let closure_conversion_scope_let ctx scope_body_expr =
let transform_closures_scope_let ctx scope_body_expr =
Scope.fold_right_lets
~f:(fun scope_let var_next acc ->
let _free_vars, new_scope_let_expr =
@ -272,10 +264,10 @@ let closure_conversion_scope_let ctx scope_body_expr =
(Expr.Box.lift new_scope_let_expr))
scope_body_expr
let closure_conversion (p : 'm program) : 'm program Bindlib.box =
let transform_closures_program (p : 'm program) : 'm program Bindlib.box =
let _, new_code_items =
Scope.fold_map
~f:(fun (toplevel_vars, decl_ctx) var code_item ->
~f:(fun toplevel_vars var code_item ->
match code_item with
| ScopeDef (name, body) ->
let scope_input_var, scope_body_expr =
@ -289,30 +281,13 @@ let closure_conversion (p : 'm program) : 'm program Bindlib.box =
}
in
let new_scope_lets =
closure_conversion_scope_let ctx scope_body_expr
transform_closures_scope_let ctx scope_body_expr
in
let new_scope_body_expr =
Bindlib.bind_var scope_input_var new_scope_lets
in
let new_decl_ctx =
(* Because closure conversion can change the type of input and
output scope variables that are structs, their type will change.
So we replace their type decleration in the structs with TAny so
that a later re-typing phase can infer them. *)
let replace_type_with_any s =
Some
(StructField.Map.map (fun t -> Mark.copy t TAny) (Option.get s))
in
{
decl_ctx with
ctx_structs =
StructName.Map.update body.scope_body_output_struct
replace_type_with_any
(StructName.Map.update body.scope_body_input_struct
replace_type_with_any decl_ctx.ctx_structs);
}
in
( (Var.Set.add var toplevel_vars, new_decl_ctx),
( Var.Set.add var toplevel_vars,
Bindlib.box_apply
(fun scope_body_expr ->
ScopeDef (name, { body with scope_body_expr }))
@ -326,16 +301,279 @@ let closure_conversion (p : 'm program) : 'm program Bindlib.box =
}
in
let _free_vars, new_expr = transform_closures_expr ctx expr in
( (Var.Set.add var toplevel_vars, decl_ctx),
( Var.Set.add var toplevel_vars,
Bindlib.box_apply
(fun e -> Topdef (name, ty, e))
(Expr.Box.lift new_expr) ))
~varf:(fun v -> v)
(Var.Set.empty, p.decl_ctx)
(* TODO: handle_default and handle_default_opt are now operators and not
variables. *)
p.code_items
Var.Set.empty p.code_items
in
(* Now we need to further tweak [decl_ctx] because some of the user-defined
types can have closures in them and these closured might have changed type.
So we reset them to [TAny] and leave the typechecker to figure it out. This
will not yield any type unification conflicts because of the special type
[TClosureEnv]. Indeed, consider the following closure: [let f = if ... then
fun v -> x + v else fun v -> v]. To be typed correctly once converted, this
closure needs an existential type, this is what [TClosureEnv] is for. This
kind of situation is difficult to produce using the Catala surface
language: it can only happen if you store a closure which is the output of
a scope inside a user-defined data structure, and if you do it in two
different places in the code with two closures that don't have the same
capture footprint. See
[tests/tests_func/good/scope_call_func_struct_closure.catala_en]. *)
let new_decl_ctx =
let rec type_contains_arrow t =
match Mark.remove t with
| TArrow _ -> true
| TAny -> true
| TOption t' -> type_contains_arrow t'
| TClosureEnv | TLit _ -> false
| TArray ts -> type_contains_arrow ts
| TTuple ts -> List.exists type_contains_arrow ts
| TEnum e ->
EnumConstructor.Map.exists
(fun _ t' -> type_contains_arrow t')
(EnumName.Map.find e p.decl_ctx.ctx_enums)
| TStruct s ->
StructField.Map.exists
(fun _ t' -> type_contains_arrow t')
(StructName.Map.find s p.decl_ctx.ctx_structs)
in
let replace_fun_typs t =
if type_contains_arrow t then Mark.copy t TAny else t
in
{
p.decl_ctx with
ctx_structs =
StructName.Map.map
(StructField.Map.map replace_fun_typs)
p.decl_ctx.ctx_structs;
ctx_enums =
EnumName.Map.map
(EnumConstructor.Map.map replace_fun_typs)
p.decl_ctx.ctx_enums;
}
in
Bindlib.box_apply
(fun new_code_items ->
{ code_items = new_code_items; decl_ctx = new_decl_ctx })
new_code_items
(** {1 Hoisting closures}*)
type 'm hoisted_closure = {
name : 'm expr Var.t;
ty : typ;
closure : (lcalc, 'm) boxed_gexpr (* Starts with [EAbs]. *);
}
let rec hoist_closures_expr :
type m. string -> m expr -> m hoisted_closure list * m expr boxed =
fun name_context e ->
let m = Mark.get e in
match Mark.remove e with
| EMatch { e; cases; name } ->
let collected_closures, new_e = (hoist_closures_expr name_context) e in
(* We do not close the closures inside the arms of the match expression,
since they get a special treatment at compilation to Scalc. *)
let collected_closures, new_cases =
EnumConstructor.Map.fold
(fun cons e1 (collected_closures, new_cases) ->
match Mark.remove e1 with
| EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in
let new_collected_closures, new_body =
(hoist_closures_expr name_context) body
in
let new_binder = Expr.bind vars new_body in
( collected_closures @ new_collected_closures,
EnumConstructor.Map.add cons
(Expr.eabs new_binder tys (Mark.get e1))
new_cases )
| _ -> failwith "should not happen")
cases
(collected_closures, EnumConstructor.Map.empty)
in
collected_closures, Expr.ematch new_e name new_cases m
| EApp { f = EAbs { binder; tys }, e1_pos; args } ->
(* let-binding, we should not close these *)
let vars, body = Bindlib.unmbind binder in
let collected_closures, new_body =
(hoist_closures_expr name_context) body
in
let new_binder = Expr.bind vars new_body in
let collected_closures, new_args =
List.fold_right
(fun arg (collected_closures, new_args) ->
let new_collected_closures, new_arg =
(hoist_closures_expr name_context) arg
in
collected_closures @ new_collected_closures, new_arg :: new_args)
args (collected_closures, [])
in
( collected_closures,
Expr.eapp (Expr.eabs new_binder (tys_as_tanys tys) e1_pos) new_args m )
| EApp
{
f =
(EOp { op = HandleDefaultOpt | Fold | Map | Filter | Reduce; _ }, _)
as f;
args;
} ->
(* Special case for some operators: its arguments closures thunks because if
you want to extract it as a function you need these closures to preserve
evaluation order, but backends that don't support closures will simply
extract these operators in a inlined way and skip the thunks. *)
let collected_closures, new_args =
List.fold_right
(fun (arg : (lcalc, m) gexpr) (collected_closures, new_args) ->
let m_arg = Mark.get arg in
match Mark.remove arg with
| EAbs { binder; tys } ->
let vars, arg = Bindlib.unmbind binder in
let new_collected_closures, new_arg =
(hoist_closures_expr name_context) arg
in
let new_arg =
Expr.make_abs vars new_arg tys (Expr.mark_pos m_arg)
in
new_collected_closures @ collected_closures, new_arg :: new_args
| _ ->
let new_collected_closures, new_arg =
hoist_closures_expr name_context arg
in
new_collected_closures @ collected_closures, new_arg :: new_args)
args ([], [])
in
collected_closures, Expr.eapp (Expr.box f) new_args (Mark.get e)
| EAbs { tys; _ } ->
(* this is the closure we want to hoist*)
let closure_var = Var.make ("closure_" ^ name_context) in
(* TODO: This will end up as a toplevel name. However for now we assume
toplevel names are unique, but this breaks this assertions and can lead
to name wrangling in the backends. We need to have a better system for
name disambiguation when for instance printing to Dcalc/Lcalc/Scalc but
also OCaml, Python, etc. *)
( [
{
name = closure_var;
ty = TArrow (tys, (TAny, Expr.mark_pos m)), Expr.mark_pos m;
closure = Expr.rebox e;
};
],
Expr.make_var closure_var m )
| EApp _ | EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _
| EArray _ | ELit _ | EAssert _ | EOp _ | EIfThenElse _ | ERaise _ | ECatch _
| EVar _ ->
Expr.map_gather ~acc:[] ~join:( @ ) ~f:(hoist_closures_expr name_context) e
| EExternal _ -> failwith "unimplemented"
| _ -> .
(* Here I have to reimplement Scope.map_exprs_in_lets because I'm changing the
type *)
let hoist_closures_scope_let name_context scope_body_expr =
Scope.fold_right_lets
~f:(fun scope_let var_next (hoisted_closures, next_scope_lets) ->
let new_hoisted_closures, new_scope_let_expr =
(hoist_closures_expr (Bindlib.name_of var_next))
scope_let.scope_let_expr
in
( new_hoisted_closures @ hoisted_closures,
Bindlib.box_apply2
(fun scope_let_next scope_let_expr ->
ScopeLet { scope_let with scope_let_next; scope_let_expr })
(Bindlib.bind_var var_next next_scope_lets)
(Expr.Box.lift new_scope_let_expr) ))
~init:(fun res ->
let hoisted_closures, new_scope_let_expr =
(hoist_closures_expr name_context) res
in
(* INVARIANT here: the result expr of a scope is simply a struct
containing all output variables so nothing should be converted here, so
no need to take into account free variables. *)
( hoisted_closures,
Bindlib.box_apply
(fun res -> Result res)
(Expr.Box.lift new_scope_let_expr) ))
scope_body_expr
let rec hoist_closures_code_item_list
(code_items : (lcalc, 'm) gexpr code_item_list) :
(lcalc, 'm) gexpr code_item_list Bindlib.box =
match code_items with
| Nil -> Bindlib.box Nil
| Cons (code_item, next_code_items) ->
let code_item_var, next_code_items = Bindlib.unbind next_code_items in
let hoisted_closures, new_code_item =
match code_item with
| ScopeDef (name, body) ->
let scope_input_var, scope_body_expr =
Bindlib.unbind body.scope_body_expr
in
let new_hoisted_closures, new_scope_lets =
hoist_closures_scope_let
(fst (ScopeName.get_info name))
scope_body_expr
in
let new_scope_body_expr =
Bindlib.bind_var scope_input_var new_scope_lets
in
( new_hoisted_closures,
Bindlib.box_apply
(fun scope_body_expr ->
ScopeDef (name, { body with scope_body_expr }))
new_scope_body_expr )
| Topdef (name, ty, expr) ->
let new_hoisted_closures, new_expr =
hoist_closures_expr (Mark.remove (TopdefName.get_info name)) expr
in
( new_hoisted_closures,
Bindlib.box_apply
(fun e -> Topdef (name, ty, e))
(Expr.Box.lift new_expr) )
in
let next_code_items = hoist_closures_code_item_list next_code_items in
let next_code_items =
Bindlib.box_apply2
(fun next_code_items new_code_item ->
Cons (new_code_item, next_code_items))
(Bindlib.bind_var code_item_var next_code_items)
new_code_item
in
let next_code_items =
List.fold_left
(fun (next_code_items : (lcalc, 'm) gexpr code_item_list Bindlib.box)
(hoisted_closure : 'm hoisted_closure) ->
let next_code_items =
Bindlib.bind_var hoisted_closure.name next_code_items
in
let closure, closure_mark = hoisted_closure.closure in
Bindlib.box_apply2
(fun next_code_items closure ->
Cons
( Topdef
( TopdefName.fresh
( Bindlib.name_of hoisted_closure.name,
Expr.mark_pos closure_mark ),
hoisted_closure.ty,
(closure, closure_mark) ),
next_code_items ))
next_code_items closure)
next_code_items hoisted_closures
in
next_code_items
let hoist_closures_program (p : 'm program) : 'm program Bindlib.box =
let new_code_items = hoist_closures_code_item_list p.code_items in
(*TODO: we need to insert the hoisted closures just before the scopes they
belong to, because some of them call sub-scopes and putting them all at the
beginning breaks dependency ordering. *)
Bindlib.box_apply
(fun new_code_items -> { p with code_items = new_code_items })
new_code_items
(** { 1 Closure conversion }*)
let closure_conversion (p : 'm program) : 'm program Bindlib.box =
let new_p = transform_closures_program p in
hoist_closures_program (Bindlib.unbox new_p)

9
compiler/lcalc/closure_conversion.mli
View File

@ -14,6 +14,11 @@
License for the specific language governing permissions and limitations under
the License. *)
(** This module performs environment-passing style closure conversion, relying
on the existential [TClosureEnv] type and tuples for closure environments.
The implementation is based on François Pottier's
{{:http://gallium.inria.fr/~fpottier/mpri/cours04.pdf#page=10} MPRI lesson}.
After closure conversion, closure hoisting is perform and all closures end
up as toplevel definitions. *)
val closure_conversion : 'm Ast.program -> 'm Ast.program Bindlib.box
(** Warning/todo: no effort was yet made to ensure correct propagation of type
annotations in the typed case *)

92
compiler/lcalc/compile_without_exceptions.ml
View File

@ -56,10 +56,10 @@ let rec trans_typ_keep (tau : typ) : typ =
| TTuple ts -> TTuple (List.map trans_typ_keep ts)
| TStruct s -> TStruct s
| TEnum en -> TEnum en
| TOption _ ->
| TOption _ | TClosureEnv ->
Message.raise_internal_error
"The type option should not appear before the dcalc -> lcalc \
translation step."
"The types option and closure_env should not appear before the dcalc \
-> lcalc translation step."
| TAny -> TAny
| TArray ts ->
TArray (TOption (trans_typ_keep ts), m) (* catala is not polymorphic *)
@ -102,6 +102,12 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
let mark = m in
let pos = Expr.pos e in
(* Message.emit_debug "%a" (Print.expr ~debug:true ()) e; *)
let context_or_same_var (ctx : typed ctx) (e : typed D.expr) : string =
match Mark.remove e with
| EInj { e = EVar v, _; _ } | EVar v -> Bindlib.name_of v
| EInj { e = ELit _, _; _ } | ELit _ -> "lit"
| _ -> ctx.ctx_context_name
in
match Mark.remove e with
| EVar x ->
if (Var.Map.find x ctx.ctx_vars).info_pure then
@ -153,7 +159,7 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
| EErrorOnEmpty arg ->
let arg' = trans ctx arg in
Ast.OptionMonad.error_on_empty arg' ~mark ~toplevel:false
~var_name:ctx.ctx_context_name
~var_name:(context_or_same_var ctx arg)
| EApp { f = EVar scope, _; args = [(EStruct { fields; name }, _)] }
when (Var.Map.find scope ctx.ctx_vars).is_scope ->
(* Scopes are encoded as functions that can take option arguments, and
@ -176,19 +182,21 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
As every function of type [a -> b] but top-level scopes is built using
this function, returning a function of type [a -> b option], we should
use [Ast.OptionMonad.mbind]. *)
let f_var = Var.make ctx.ctx_context_name in
let f_var = Var.make (Bindlib.name_of ff) in
Ast.OptionMonad.bind_var ~mark
(Ast.OptionMonad.mbind ~var_name:ctx.ctx_context_name
(Ast.OptionMonad.mbind
~var_name:(context_or_same_var ctx (List.hd args))
(Expr.evar f_var mark)
(List.map (trans ctx) args)
~mark)
f_var (trans ctx f)
| EApp { f = (EStructAccess _, _) as f; args } ->
| EApp { f = (EStructAccess { e = es; _ }, _) as f; args } ->
(* This occurs when calling a subscope function. The same encoding as the
one for [EApp (Var _) _] if the variable is not a scope works. *)
let f_var = Var.make ctx.ctx_context_name in
let f_var = Var.make (context_or_same_var ctx es) in
Ast.OptionMonad.bind_var ~mark
(Ast.OptionMonad.mbind ~var_name:ctx.ctx_context_name
(Ast.OptionMonad.mbind
~var_name:(context_or_same_var ctx es)
(Expr.evar f_var mark)
(List.map (trans ctx) args)
~mark)
@ -224,15 +232,17 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
let x1 = Var.make "f" in
let x2 = Var.make "init" in
let f' =
Ast.OptionMonad.bind_cont ~mark ~var_name:ctx.ctx_context_name
(fun f ->
Ast.OptionMonad.bind_cont ~mark
~var_name:(context_or_same_var ctx f)
(fun f' ->
Ast.OptionMonad.return ~mark
(Expr.eabs
(Expr.bind [| x1; x2 |]
(Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
(Ast.OptionMonad.mbind_cont
~var_name:(context_or_same_var ctx f)
~mark
(fun vars ->
Expr.eapp (Expr.evar f m)
Expr.eapp (Expr.evar f' m)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
m)
[Expr.evar x1 m; Expr.evar x2 m]))
@ -240,7 +250,8 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
m))
(trans ctx f)
in
Ast.OptionMonad.mbind ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mbind
~var_name:(context_or_same_var ctx f)
(Expr.eop (trans_op Op.Fold) tys opmark)
[f'; Ast.OptionMonad.return ~mark (trans ctx init); trans ctx l]
~mark
@ -248,15 +259,17 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
let x1 = Var.make "f" in
let x2 = Var.make "init" in
let f' =
Ast.OptionMonad.bind_cont ~mark ~var_name:ctx.ctx_context_name
(fun f ->
Ast.OptionMonad.bind_cont ~mark
~var_name:(context_or_same_var ctx f)
(fun f' ->
Ast.OptionMonad.return ~mark
(Expr.eabs
(Expr.bind [| x1; x2 |]
(Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
(Ast.OptionMonad.mbind_cont
~var_name:(context_or_same_var ctx f)
~mark
(fun vars ->
Expr.eapp (Expr.evar f m)
Expr.eapp (Expr.evar f' m)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
m)
[Expr.evar x1 m; Expr.evar x2 m]))
@ -264,7 +277,8 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
m))
(trans ctx f)
in
Ast.OptionMonad.mbind ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mbind
~var_name:(context_or_same_var ctx f)
(Expr.eop (trans_op Op.Reduce) tys opmark)
[f'; Ast.OptionMonad.return ~mark (trans ctx init); trans ctx l]
~mark
@ -290,7 +304,8 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
m))
(trans ctx f)
in
Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mbind_cont
~var_name:(context_or_same_var ctx f)
(fun vars ->
Ast.OptionMonad.return ~mark
(Expr.eapp
@ -304,19 +319,20 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
requires an function of type [a option -> bool]. Hence we need to modify
[f] by first matching the input, and second using the error_on_empty on
the result. *)
let x1 = Var.make ctx.ctx_context_name in
let x1 = Var.make (context_or_same_var ctx f) in
let f' =
Ast.OptionMonad.bind_cont ~mark ~var_name:ctx.ctx_context_name
(fun f ->
Ast.OptionMonad.bind_cont ~mark
~var_name:(context_or_same_var ctx f)
(fun f' ->
Ast.OptionMonad.return ~mark
(Expr.eabs
(Expr.bind [| x1 |]
(Ast.OptionMonad.error_on_empty ~toplevel:true ~mark
~var_name:ctx.ctx_context_name
~var_name:(context_or_same_var ctx f)
(Ast.OptionMonad.mbind_cont ~mark
~var_name:ctx.ctx_context_name
~var_name:(context_or_same_var ctx f)
(fun vars ->
Expr.eapp (Expr.evar f m)
Expr.eapp (Expr.evar f' m)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
m)
[Expr.evar x1 m])))
@ -324,7 +340,8 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
m))
(trans ctx f)
in
Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mbind_cont
~var_name:(context_or_same_var ctx f)
(fun vars ->
Ast.OptionMonad.return ~mark
(Expr.eapp
@ -345,7 +362,8 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
op
| EApp { f = EOp { op; tys }, opmark; args } ->
let res =
Ast.OptionMonad.mmap ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mmap
~var_name:(context_or_same_var ctx (List.hd args))
(Expr.eop (trans_op op) tys opmark)
(List.map (trans ctx) args)
~mark
@ -377,7 +395,8 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
Expr.eabs binder tys m
| _ -> assert false)
in
Ast.OptionMonad.bind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont
~var_name:(context_or_same_var ctx e)
(fun e -> Expr.ematch (Expr.evar e m) name cases m)
(trans ctx e) ~mark
| EArray args ->
@ -405,19 +424,22 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
(List.map (trans ctx) fields)
~mark
| EIfThenElse { cond; etrue; efalse } ->
Ast.OptionMonad.bind_cont ~mark ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont ~mark
~var_name:(context_or_same_var ctx cond)
(fun cond ->
Expr.eifthenelse (Expr.evar cond mark) (trans ctx etrue)
(trans ctx efalse) mark)
(trans ctx cond)
| EInj { name; cons; e } ->
Ast.OptionMonad.bind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont
~var_name:(context_or_same_var ctx e)
(fun e ->
Ast.OptionMonad.return ~mark
(Expr.einj (Expr.evar e mark) cons name mark))
(trans ctx e) ~mark
| EStructAccess { name; e; field } ->
Ast.OptionMonad.bind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont
~var_name:(context_or_same_var ctx e)
(fun e -> Expr.estructaccess (Expr.evar e mark) field name mark)
(trans ctx e) ~mark
| ETuple args ->
@ -428,11 +450,13 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
(List.map (trans ctx) args)
~mark
| ETupleAccess { e; index; size } ->
Ast.OptionMonad.bind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont
~var_name:(context_or_same_var ctx e)
(fun e -> Expr.etupleaccess (Expr.evar e mark) index size mark)
(trans ctx e) ~mark
| EAssert e ->
Ast.OptionMonad.bind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont
~var_name:(context_or_same_var ctx e)
(fun e ->
Ast.OptionMonad.return ~mark (Expr.eassert (Expr.evar e mark) mark))
(trans ctx e) ~mark

8
compiler/lcalc/lcalc.mld
View File

@ -23,6 +23,14 @@ Related modules:
{!modules: Lcalc.Compile_with_exceptions Lcalc.Compile_without_exceptions}
{1 Closure conversion }
To target languages that don't have support for closures, we need to convert
the closures to first-class functions in function-pointer-passing style
computations.
{!modules: Lcalc.Closure_conversion }
{1 Backends}
The OCaml backend of the lambda calculus is merely a syntactic formatting,

1
compiler/lcalc/to_ocaml.ml
View File

@ -176,6 +176,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit =
(t1 @ [t2])
| TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ_with_parens t1
| TAny -> Format.fprintf fmt "_"
| TClosureEnv -> failwith "unimplemented!"
let format_var (fmt : Format.formatter) (v : 'm Var.t) : unit =
let lowercase_name =

1
compiler/plugins/api_web.ml
View File

@ -86,6 +86,7 @@ module To_jsoo = struct
~pp_sep:(fun fmt () -> Format.pp_print_string fmt " -> ")
format_typ_with_parens)
t1 format_typ_with_parens t2
| TClosureEnv -> Format.fprintf fmt "Js.Unsafe.any Js.t"
let rec format_typ_to_jsoo fmt typ =
match Mark.remove typ with

2
compiler/scalc/to_python.ml
View File

@ -89,6 +89,7 @@ let format_op (fmt : Format.formatter) (op : operator Mark.pos) : unit =
| Fold -> Format.pp_print_string fmt "list_fold_left"
| HandleDefault -> Format.pp_print_string fmt "handle_default"
| HandleDefaultOpt -> Format.pp_print_string fmt "handle_default_opt"
| FromClosureEnv | ToClosureEnv -> failwith "unimplemented"
let format_uid_list (fmt : Format.formatter) (uids : Uid.MarkedString.info list)
: unit =
@ -184,6 +185,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit =
t1 format_typ_with_parens t2
| TArray t1 -> Format.fprintf fmt "List[%a]" format_typ_with_parens t1
| TAny -> Format.fprintf fmt "Any"
| TClosureEnv -> failwith "unimplemented!"
let format_name_cleaned (fmt : Format.formatter) (s : string) : unit =
s

2
compiler/scopelang/dependency.ml
View File

@ -258,7 +258,7 @@ let rec get_structs_or_enums_in_type (t : typ) : TVertexSet.t =
|> List.map get_structs_or_enums_in_type
|> List.fold_left TVertexSet.union TVertexSet.empty)
(get_structs_or_enums_in_type t2)
| TLit _ | TAny -> TVertexSet.empty
| TClosureEnv | TLit _ | TAny -> TVertexSet.empty
| TOption t1 | TArray t1 -> get_structs_or_enums_in_type t1
| TTuple ts ->
List.fold_left

3
compiler/shared_ast/definitions.ml
View File

@ -159,6 +159,7 @@ and naked_typ =
| TArrow of typ list * typ
| TArray of typ
| TAny
| TClosureEnv (** Hides an existential type needed for closure conversion *)
(** {2 Constants and operators} *)
@ -211,6 +212,8 @@ module Op = struct
(* * polymorphic *)
| Length : < polymorphic ; .. > t
| Log : log_entry * Uid.MarkedString.info list -> < polymorphic ; .. > t
| ToClosureEnv : < polymorphic ; .. > t
| FromClosureEnv : < polymorphic ; .. > t
(* * overloaded *)
| Minus : < overloaded ; .. > t
| Minus_int : < resolved ; .. > t

4
compiler/shared_ast/expr.ml
View File

@ -185,8 +185,8 @@ let mark_pos (type m) (m : m mark) : Pos.t =
let pos (type m) (x : ('a, m) marked) : Pos.t = mark_pos (Mark.get x)
let fun_id mark : ('a any, 'm) boxed_gexpr =
let x = Var.make "x" in
let fun_id ?(var_name : string = "x") mark : ('a any, 'm) boxed_gexpr =
let x = Var.make var_name in
eabs (bind [| x |] (evar x mark)) [TAny, mark_pos mark] mark
let ty (_, m) : typ = match m with Typed { ty; _ } -> ty

2
compiler/shared_ast/expr.mli
View File

@ -154,7 +154,7 @@ val ecustom :
'm mark ->
(< custom : Definitions.yes ; .. >, 'm) boxed_gexpr
val fun_id : 'm mark -> ('a any, 'm) boxed_gexpr
val fun_id : ?var_name:string -> 'm mark -> ('a any, 'm) boxed_gexpr
(** {2 Manipulation of marks} *)

26
compiler/shared_ast/interpreter.ml
View File

@ -162,7 +162,13 @@ let rec evaluate_operator
in
let err () =
Message.raise_multispanned_error
([Some "Operator:", pos]
([
( Some
(Format.asprintf "Operator (value %a):"
(Print.operator ~debug:true)
op),
pos );
]
@ List.mapi
(fun i arg ->
( Some
@ -184,6 +190,12 @@ let rec evaluate_operator
| Log (entry, infos), [e'] ->
print_log entry infos pos e';
Mark.remove e'
| (FromClosureEnv | ToClosureEnv), [e'] ->
(* [FromClosureEnv] and [ToClosureEnv] are just there to bypass the need for
existential types when typing code after closure conversion. There are
effectively no-ops. *)
Mark.remove e'
| (ToClosureEnv | FromClosureEnv), _ -> err ()
| Eq, [(e1, _); (e2, _)] ->
ELit (LBool (handle_eq (evaluate_operator evaluate_expr) m e1 e2))
| Map, [f; (EArray es, _)] ->
@ -333,6 +345,13 @@ let rec evaluate_operator
ELit (LBool (o_eq_dat_dat x y))
| Eq_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_eq_dur_dur x y))
| HandleDefault, _ ->
Message.raise_internal_error
"The interpreter is trying to evaluate the \"handle_default\" operator, \
which is the leftover from the dcalc->lcalc compilation pass. This \
indicates that you are trying to interpret the lcalc without having \
activating --avoid_exceptions. This interpretation is not implemented, \
just try to interpret the dcalc (with \"Interpret\") instead."
| HandleDefaultOpt, [(EArray exps, _); justification; conclusion] -> (
let valid_exceptions =
ListLabels.filter exps ~f:(function
@ -340,7 +359,6 @@ let rec evaluate_operator
EnumConstructor.equal cons Expr.some_constr
| _ -> err ())
in
match valid_exceptions with
| [] -> (
match
@ -385,8 +403,7 @@ let rec evaluate_operator
| Lte_mon_mon | Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_rat_rat
| Gt_mon_mon | Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat
| Gte_mon_mon | Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat
| Eq_mon_mon | Eq_dat_dat | Eq_dur_dur | HandleDefault | HandleDefaultOpt
),
| Eq_mon_mon | Eq_dat_dat | Eq_dur_dur | HandleDefaultOpt ),
_ ) ->
err ()
@ -436,6 +453,7 @@ let rec runtime_to_val :
let e = runtime_to_val eval_expr ctx m ty (Obj.field o 0) in
EInj { name; cons; e }, m
| TOption _ty -> assert false
| TClosureEnv -> assert false
| TArray ty ->
( EArray
(List.map

2
compiler/shared_ast/interpreter.mli
View File

@ -20,6 +20,8 @@
open Catala_utils
open Definitions
exception CatalaException of except
type features =
< monomorphic : yes
; polymorphic : yes

13
compiler/shared_ast/operator.ml
View File

@ -109,6 +109,8 @@ let name : type a. a t -> string = function
| Fold -> "o_fold"
| HandleDefault -> "o_handledefault"
| HandleDefaultOpt -> "o_handledefaultopt"
| ToClosureEnv -> "o_toclosureenv"
| FromClosureEnv -> "o_fromclosureenv"
let compare_log_entries l1 l2 =
match l1, l2 with
@ -229,7 +231,8 @@ let compare (type a1 a2) (t1 : a1 t) (t2 : a2 t) =
| Eq_dur_dur, Eq_dur_dur
| Fold, Fold
| HandleDefault, HandleDefault
| HandleDefaultOpt, HandleDefaultOpt -> 0
| HandleDefaultOpt, HandleDefaultOpt
| FromClosureEnv, FromClosureEnv | ToClosureEnv, ToClosureEnv -> 0
| Not, _ -> -1 | _, Not -> 1
| Length, _ -> -1 | _, Length -> 1
| GetDay, _ -> -1 | _, GetDay -> 1
@ -314,6 +317,8 @@ let compare (type a1 a2) (t1 : a1 t) (t2 : a2 t) =
| Eq_dur_dur, _ -> -1 | _, Eq_dur_dur -> 1
| HandleDefault, _ -> -1 | _, HandleDefault -> 1
| HandleDefaultOpt, _ -> -1 | _, HandleDefaultOpt -> 1
| FromClosureEnv, _ -> -1 | _, FromClosureEnv -> 1
| ToClosureEnv, _ -> -1 | _, ToClosureEnv -> 1
| Fold, _ | _, Fold -> .
let equal t1 t2 = compare t1 t2 = 0
@ -335,7 +340,8 @@ let kind_dispatch :
| Or | Xor ) as op ->
monomorphic op
| ( Log _ | Length | Eq | Map | Concat | Filter | Reduce | Fold
| HandleDefault | HandleDefaultOpt ) as op ->
| HandleDefault | HandleDefaultOpt | FromClosureEnv | ToClosureEnv ) as op
->
polymorphic op
| ( Minus | ToRat | ToMoney | Round | Add | Sub | Mult | Div | Lt | Lte | Gt
| Gte ) as op ->
@ -376,7 +382,8 @@ let translate (t : 'a no_overloads t) : 'b no_overloads t =
| Lte_int_int | Lte_rat_rat | Lte_mon_mon | Lte_dat_dat | Lte_dur_dur
| Gt_int_int | Gt_rat_rat | Gt_mon_mon | Gt_dat_dat | Gt_dur_dur
| Gte_int_int | Gte_rat_rat | Gte_mon_mon | Gte_dat_dat | Gte_dur_dur
| Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dat_dat | Eq_dur_dur ) as op ->
| Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dat_dat | Eq_dur_dur
| FromClosureEnv | ToClosureEnv ) as op ->
op
let monomorphic_type ((op : monomorphic t), pos) =

28
compiler/shared_ast/optimizations.ml
View File

@ -58,6 +58,29 @@ let all_match_cases_map_to_same_constructor cases n =
| _ -> false)
| _ -> assert false)
let binder_vars_used_at_most_once
(binder :
( (('a, 'b) dcalc_lcalc, ('a, 'b) dcalc_lcalc, 'm) base_gexpr,
(('a, 'b) dcalc_lcalc, 'm) gexpr )
Bindlib.mbinder) : bool =
(* fast path: variables not used at all *)
(not (Array.exists Fun.id (Bindlib.mbinder_occurs binder)))
||
let vars, body = Bindlib.unmbind binder in
let rec vars_count (e : (('a, 'b) dcalc_lcalc, 'm) gexpr) : int array =
match e with
| EVar v, _ ->
Array.map
(fun i -> if Bindlib.eq_vars v (Array.get vars i) then 1 else 0)
(Array.make (Array.length vars) 0)
| e ->
Expr.shallow_fold
(fun e' acc -> Array.map2 (fun x y -> x + y) (vars_count e') acc)
e
(Array.make (Array.length vars) 0)
in
not (Array.exists (fun c -> c > 1) (vars_count body))
let rec optimize_expr :
type a b.
(a, b, 'm) optimizations_ctx ->
@ -177,8 +200,9 @@ let rec optimize_expr :
| _ -> assert false)
in
EMatch { e = arg; cases; name = n1 }
| EApp { f = EAbs { binder; _ }, _; args } ->
(* beta reduction *)
| EApp { f = EAbs { binder; _ }, _; args }
when binder_vars_used_at_most_once binder ->
(* beta reduction when variables not used. *)
Mark.remove (Bindlib.msubst binder (List.map fst args |> Array.of_list))
| EStructAccess { name; field; e = EStruct { name = name1; fields }, _ }
when name = name1 ->

102
compiler/shared_ast/print.ml
View File

@ -80,19 +80,32 @@ let enum_constructor (fmt : Format.formatter) (c : EnumConstructor.t) : unit =
let struct_field (fmt : Format.formatter) (c : StructField.t) : unit =
Format.fprintf fmt "@{<magenta>%a@}" StructField.format_t c
let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit =
let rec typ
(ctx : decl_ctx option)
~(colors : Ocolor_types.color4 list)
(fmt : Format.formatter)
(ty : typ) : unit =
let typ = typ ctx in
let typ_with_parens (fmt : Format.formatter) (t : typ) =
if typ_needs_parens t then Format.fprintf fmt "(%a)" typ t else typ fmt t
let typ_with_parens ~colors (fmt : Format.formatter) (t : typ) =
if typ_needs_parens t then (
Format.pp_open_hvbox fmt 1;
pp_color_string (List.hd colors) fmt "(";
typ ~colors:(List.tl colors) fmt t;
Format.pp_close_box fmt ();
pp_color_string (List.hd colors) fmt ")")
else typ ~colors fmt t
in
match Mark.remove ty with
| TLit l -> tlit fmt l
| TTuple ts ->
Format.fprintf fmt "@[<hov 2>(%a)@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " %a@ " op_style "*")
typ)
ts
Format.pp_open_hvbox fmt 2;
pp_color_string (List.hd colors) fmt "(";
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " %a@ " op_style "*")
(typ ~colors:(List.tl colors)))
fmt ts;
Format.pp_close_box fmt ();
pp_color_string (List.hd colors) fmt ")"
| TStruct s -> (
match ctx with
| None -> StructName.format_t fmt s
@ -101,16 +114,20 @@ let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit =
if StructField.Map.is_empty fields then StructName.format_t fmt s
else
Format.fprintf fmt "@[<hv 2>%a %a@,%a@;<0 -2>%a@]" StructName.format_t s
punctuation "{"
(pp_color_string (List.hd colors))
"{"
(Format.pp_print_list
~pp_sep:(fun fmt () ->
punctuation fmt ";";
op_style fmt ";";
Format.pp_print_space fmt ())
(fun fmt (field_name, field_typ) ->
Format.fprintf fmt "@[<hv 2>%a%a@ %a@]" struct_field field_name
punctuation ":" typ field_typ))
punctuation ":"
(typ ~colors:(List.tl colors))
field_typ))
(StructField.Map.bindings fields)
punctuation "}")
(pp_color_string (List.hd colors))
"}")
| TEnum e -> (
match ctx with
| None -> Format.fprintf fmt "@[<hov 2>%a@]" EnumName.format_t e
@ -121,22 +138,31 @@ let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit =
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ %a@ " punctuation "|")
(fun fmt (case, mty) ->
Format.fprintf fmt "%a%a@ %a" enum_constructor case punctuation ":"
typ mty))
(typ ~colors) mty))
(EnumConstructor.Map.bindings (EnumName.Map.find e ctx.ctx_enums))
punctuation "]")
| TOption t -> Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "option" typ t
| TOption t ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "eoption" (typ ~colors) t
| TArrow ([t1], t2) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" typ_with_parens t1 op_style "→"
typ t2
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" (typ_with_parens ~colors) t1
op_style "→" (typ ~colors) t2
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a%a%a@ %a@ %a@]" op_style "("
Format.fprintf fmt "@[<hov 2>%a%a%a@ %a@ %a@]"
(pp_color_string (List.hd colors))
"("
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " op_style ",")
typ_with_parens)
t1 op_style ")" op_style "→" typ t2
(typ_with_parens ~colors:(List.tl colors)))
t1
(pp_color_string (List.hd colors))
")" op_style "→"
(typ ~colors:(List.tl colors))
t2
| TArray t1 ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "collection" typ t1
Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "collection" (typ ~colors)
t1
| TAny -> base_type fmt "any"
| TClosureEnv -> base_type fmt "closure_env"
let lit (fmt : Format.formatter) (l : lit) : unit =
match l with
@ -252,6 +278,8 @@ let operator_to_string : type a. a Op.t -> string =
| Fold -> "fold"
| HandleDefault -> "handle_default"
| HandleDefaultOpt -> "handle_default_opt"
| ToClosureEnv -> "to_closure_env"
| FromClosureEnv -> "from_closure_env"
let operator_to_shorter_string : type a. a Op.t -> string =
let open Op in
@ -294,6 +322,8 @@ let operator_to_shorter_string : type a. a Op.t -> string =
| Fold -> "fold"
| HandleDefault -> "handle_default"
| HandleDefaultOpt -> "handle_default_opt"
| ToClosureEnv -> "to_closure_env"
| FromClosureEnv -> "from_closure_env"
let operator : type a. ?debug:bool -> Format.formatter -> a operator -> unit =
fun ?(debug = true) fmt op ->
@ -373,7 +403,7 @@ module Precedence = struct
| Div_dur_dur ->
Op Div
| HandleDefault | HandleDefaultOpt | Map | Concat | Filter | Reduce | Fold
->
| ToClosureEnv | FromClosureEnv ->
App)
| EApp _ -> App
| EOp _ -> Contained
@ -465,11 +495,16 @@ let rec expr_aux :
| EVar v -> var fmt v
| EExternal eref -> Qident.format fmt eref
| ETuple es ->
Format.fprintf fmt "@[<hov 2>%a%a%a@]" punctuation "("
Format.fprintf fmt "@[<hov 2>%a%a%a@]"
(pp_color_string (List.hd colors))
"("
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(fun fmt e -> lhs exprc fmt e))
es punctuation ")"
~pp_sep:(fun fmt () ->
Format.fprintf fmt "%a@ " (pp_color_string (List.hd colors)) ",")
(fun fmt e -> lhs ~colors:(List.tl colors) exprc fmt e))
es
(pp_color_string (List.hd colors))
")"
| EArray es ->
Format.fprintf fmt "@[<hv 2>%a %a@] %a" punctuation "["
(Format.pp_print_list
@ -493,7 +528,7 @@ let rec expr_aux :
(fun fmt (x, tau, arg) ->
Format.fprintf fmt
"@[<hv 2>@[<hov 4>%a %a %a@ %a@ %a@]@ %a@;<1 -2>%a@]" keyword
"let" var x punctuation ":" (typ None) tau punctuation "="
"let" var x punctuation ":" (typ None ~colors) tau punctuation "="
(exprc colors) arg keyword "in")
fmt xs_tau_arg;
Format.pp_print_cut fmt ();
@ -516,7 +551,7 @@ let rec expr_aux :
var fmt x;
punctuation fmt ":";
Format.pp_print_space fmt ();
typ None fmt tau;
typ None ~colors fmt tau;
Format.pp_close_box fmt ();
punctuation fmt ")"))
xs_tau punctuation "→" (rhs expr) body
@ -549,7 +584,7 @@ let rec expr_aux :
| EApp { f; args } ->
Format.fprintf fmt "@[<hv 2>%a@ %a@]" (lhs exprc) f
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
(rhs exprc))
args
| EIfThenElse _ ->
@ -674,8 +709,8 @@ let rec colors =
let open Ocolor_types in
blue :: cyan :: green :: yellow :: red :: magenta :: colors
let typ_debug = typ None
let typ ctx = typ (Some ctx)
let typ_debug = typ None ~colors
let typ ctx = typ (Some ctx) ~colors
let expr ?(hide_function_body = false) ?(debug = !Cli.debug_flag) () ppf e =
expr_aux ~hide_function_body ~debug Bindlib.empty_ctxt colors ppf e
@ -824,16 +859,15 @@ let code_item ?(debug = false) decl_ctx fmt c =
match c with
| ScopeDef (n, b) -> scope ~debug decl_ctx fmt (n, b)
| Topdef (n, ty, e) ->
Format.fprintf fmt "@[%a %a %a %a %a %a @]" keyword "let topval"
TopdefName.format_t n op_style ":" (typ decl_ctx) ty op_style "="
(expr ~debug ()) e
Format.fprintf fmt "@[<v 2>@[<hov 2>%a@ %a@ %a@ %a@ %a@]@ %a@]" keyword
"let topval" TopdefName.format_t n op_style ":" (typ decl_ctx) ty op_style
"=" (expr ~debug ()) e
let rec code_item_list ?(debug = false) decl_ctx fmt c =
match c with
| Nil -> ()
| Cons (c, b) ->
let _x, cl = Bindlib.unbind b in
Format.fprintf fmt "%a @.%a"
(code_item ~debug decl_ctx)
c

12
compiler/shared_ast/type.ml
View File

@ -31,9 +31,9 @@ let rec equal ty1 ty2 =
| TOption t1, TOption t2 -> equal t1 t2
| TArrow (t1, t1'), TArrow (t2, t2') -> equal_list t1 t2 && equal t1' t2'
| TArray t1, TArray t2 -> equal t1 t2
| TAny, TAny -> true
| TClosureEnv, TClosureEnv | TAny, TAny -> true
| ( ( TLit _ | TTuple _ | TStruct _ | TEnum _ | TOption _ | TArrow _
| TArray _ | TAny ),
| TArray _ | TAny | TClosureEnv ),
_ ) ->
false
@ -52,7 +52,9 @@ let rec unifiable ty1 ty2 =
| TArrow (t1, t1'), TArrow (t2, t2') ->
unifiable_list t1 t2 && unifiable t1' t2'
| TArray t1, TArray t2 -> unifiable t1 t2
| ( (TLit _ | TTuple _ | TStruct _ | TEnum _ | TOption _ | TArrow _ | TArray _),
| TClosureEnv, TClosureEnv -> true
| ( ( TLit _ | TTuple _ | TStruct _ | TEnum _ | TOption _ | TArrow _
| TArray _ | TClosureEnv ),
_ ) ->
false
@ -69,7 +71,7 @@ let rec compare ty1 ty2 =
| TArrow (a1, b1), TArrow (a2, b2) -> (
match List.compare compare a1 a2 with 0 -> compare b1 b2 | n -> n)
| TArray t1, TArray t2 -> compare t1 t2
| TAny, TAny -> 0
| TAny, TAny | TClosureEnv, TClosureEnv -> 0
| TLit _, _ -> -1
| _, TLit _ -> 1
| TTuple _, _ -> -1
@ -84,5 +86,7 @@ let rec compare ty1 ty2 =
| _, TArrow _ -> 1
| TArray _, _ -> -1
| _, TArray _ -> 1
| TClosureEnv, _ -> -1
| _, TClosureEnv -> 1
let rec arrow_return = function TArrow (_, b), _ -> arrow_return b | t -> t

134
compiler/shared_ast/typing.ml
View File

@ -33,9 +33,9 @@ module Any =
()
type unionfind_typ = naked_typ Mark.pos UnionFind.elem
(** We do not reuse {!type: Shared_ast.typ} because we have to include a new
[TAny] variant. Indeed, error terms can have any type and this has to be
captured by the type sytem. *)
(** We do not reuse {!type: A.typ} because we have to include a new [TAny]
variant. Indeed, error terms can have any type and this has to be captured
by the type sytem. *)
and naked_typ =
| TLit of A.typ_lit
@ -46,6 +46,7 @@ and naked_typ =
| TOption of unionfind_typ
| TArray of unionfind_typ
| TAny of Any.t
| TClosureEnv
let rec typ_to_ast ~leave_unresolved (ty : unionfind_typ) : A.typ =
let typ_to_ast = typ_to_ast ~leave_unresolved in
@ -66,6 +67,7 @@ let rec typ_to_ast ~leave_unresolved (ty : unionfind_typ) : A.typ =
typing. *)
Message.raise_spanned_error pos
"Internal error: typing at this point could not be resolved"
| TClosureEnv -> TClosureEnv, pos
let rec ast_to_typ (ty : A.typ) : unionfind_typ =
let ty' =
@ -78,6 +80,7 @@ let rec ast_to_typ (ty : A.typ) : unionfind_typ =
| A.TOption t -> TOption (ast_to_typ t)
| A.TArray t -> TArray (ast_to_typ t)
| A.TAny -> TAny (Any.fresh ())
| A.TClosureEnv -> TClosureEnv
in
UnionFind.make (Mark.copy ty ty')
@ -85,48 +88,82 @@ let rec ast_to_typ (ty : A.typ) : unionfind_typ =
let typ_needs_parens (t : unionfind_typ) : bool =
let t = UnionFind.get (UnionFind.find t) in
match Mark.remove t with
| TArrow _ | TArray _ | TOption _ -> true
| _ -> false
match Mark.remove t with TArrow _ | TArray _ -> true | _ -> false
let with_color f color fmt x =
(* equivalent to [Format.fprintf fmt "@{<color>%s@}" s] *)
Format.pp_open_stag fmt Ocolor_format.(Ocolor_style_tag (Fg (C4 color)));
f fmt x;
Format.pp_close_stag fmt ()
let pp_color_string = with_color Format.pp_print_string
let rec format_typ
(ctx : A.decl_ctx)
~(colors : Ocolor_types.color4 list)
(fmt : Format.formatter)
(naked_typ : unionfind_typ) : unit =
let format_typ = format_typ ctx in
let format_typ_with_parens (fmt : Format.formatter) (t : unionfind_typ) =
if typ_needs_parens t then Format.fprintf fmt "(%a)" format_typ t
else Format.fprintf fmt "%a" format_typ t
let format_typ_with_parens
~colors
(fmt : Format.formatter)
(t : unionfind_typ) =
if typ_needs_parens t then (
Format.pp_open_hvbox fmt 1;
pp_color_string (List.hd colors) fmt "(";
format_typ ~colors:(List.tl colors) fmt t;
Format.pp_close_box fmt ();
pp_color_string (List.hd colors) fmt ")")
else Format.fprintf fmt "%a" (format_typ ~colors) t
in
let naked_typ = UnionFind.get (UnionFind.find naked_typ) in
match Mark.remove naked_typ with
| TLit l -> Format.fprintf fmt "%a" Print.tlit l
| TTuple ts ->
Format.fprintf fmt "@[<hov 2>(%a)@]"
Format.fprintf fmt "@[<hov 2>%a%a%a@]"
(pp_color_string (List.hd colors))
"("
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ *@ ")
(fun fmt t -> Format.fprintf fmt "%a" format_typ t))
(fun fmt t ->
Format.fprintf fmt "%a" (format_typ ~colors:(List.tl colors)) t))
ts
(pp_color_string (List.hd colors))
")"
| TStruct s -> Format.fprintf fmt "%a" A.StructName.format_t s
| TEnum e -> Format.fprintf fmt "%a" A.EnumName.format_t e
| TOption t ->
Format.fprintf fmt "@[<hov 2>(%a)@ %s@]" format_typ_with_parens t "eoption"
Format.fprintf fmt "@[<hov 2>option %a@]"
(format_typ_with_parens ~colors:(List.tl colors))
t
| TArrow ([t1], t2) ->
Format.fprintf fmt "@[<hov 2>%a@ →@ %a@]" format_typ_with_parens t1
format_typ t2
Format.fprintf fmt "@[<hov 2>%a@ →@ %a@]"
(format_typ_with_parens ~colors)
t1 (format_typ ~colors) t2
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>(%a)@ →@ %a@]"
Format.fprintf fmt "@[<hov 2>%a%a%a@ →@ %a@]"
(pp_color_string (List.hd colors))
"("
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
format_typ_with_parens)
t1 format_typ t2
(format_typ_with_parens ~colors:(List.tl colors)))
t1
(pp_color_string (List.hd colors))
")" (format_typ ~colors) t2
| TArray t1 -> (
match Mark.remove (UnionFind.get (UnionFind.find t1)) with
| TAny _ when not !Cli.debug_flag -> Format.pp_print_string fmt "collection"
| _ -> Format.fprintf fmt "@[collection@ %a@]" format_typ t1)
| _ -> Format.fprintf fmt "@[collection@ %a@]" (format_typ ~colors) t1)
| TAny v ->
if !Cli.debug_flag then Format.fprintf fmt "<a%d>" (Any.hash v)
else Format.pp_print_string fmt "<any>"
| TClosureEnv -> Format.fprintf fmt "closure_env"
let rec colors =
let open Ocolor_types in
blue :: cyan :: green :: yellow :: red :: magenta :: colors
let format_typ ctx fmt naked_typ = format_typ ctx ~colors fmt naked_typ
exception Type_error of A.any_expr * unionfind_typ * unionfind_typ
@ -159,9 +196,10 @@ let rec unify
if not (A.EnumName.equal e1 e2) then raise_type_error ()
| TOption t1, TOption t2 -> unify e t1 t2
| TArray t1', TArray t2' -> unify e t1' t2'
| TClosureEnv, TClosureEnv -> ()
| TAny _, _ | _, TAny _ -> ()
| ( ( TLit _ | TArrow _ | TTuple _ | TStruct _ | TEnum _ | TOption _
| TArray _ ),
| TArray _ | TClosureEnv ),
_ ) ->
raise_type_error ()
in
@ -196,8 +234,9 @@ let handle_type_error ctx (A.AnyExpr e) t1 t2 =
t2_pos );
]
"@[<v>Error during typechecking, incompatible types:@,\
@{<bold;blue>-->@} @[<hov>%a@]@,\
@{<bold;blue>-->@} @[<hov>%a@]@]" (format_typ ctx) t1 (format_typ ctx) t2
@[<v>@{<bold;blue>@<3>%s@} @[<hov>%a@]@,\
@{<bold;blue>@<3>%s@} @[<hov>%a@]@]@]" "┌─⯈" (format_typ ctx) t1 "└─⯈"
(format_typ ctx) t2
let lit_type (lit : A.lit) : naked_typ =
match lit with
@ -223,6 +262,7 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) :
let bt = lazy (UnionFind.make (TLit TBool, pos)) in
let ut = lazy (UnionFind.make (TLit TUnit, pos)) in
let it = lazy (UnionFind.make (TLit TInt, pos)) in
let cet = lazy (UnionFind.make (TClosureEnv, pos)) in
let array a = lazy (UnionFind.make (TArray (Lazy.force a), pos)) in
let option a = lazy (UnionFind.make (TOption (Lazy.force a), pos)) in
let ( @-> ) x y =
@ -243,6 +283,8 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) :
| HandleDefaultOpt ->
[array (option any); [ut] @-> option bt; [ut] @-> option any]
@-> option any
| ToClosureEnv -> [any] @-> cet
| FromClosureEnv -> [cet] @-> any
in
Lazy.force ty
@ -910,7 +952,7 @@ let scope_body ~leave_unresolved ctx env body =
(TArrow ([ty_in], ty_out))) )
let rec scopes ~leave_unresolved ctx env = function
| A.Nil -> Bindlib.box A.Nil
| A.Nil -> Bindlib.box A.Nil, env
| A.Cons (item, next_bind) ->
let var, next = Bindlib.unbind next_bind in
let env, def =
@ -925,17 +967,49 @@ let rec scopes ~leave_unresolved ctx env = function
let e' = Expr.map_marks ~f:(get_ty_mark ~leave_unresolved) e' in
( Env.add var uf env,
Bindlib.box_apply
(fun e -> A.Topdef (name, typ, e))
(fun e -> A.Topdef (name, Expr.ty e', e))
(Expr.Box.lift e') )
in
let next' = scopes ~leave_unresolved ctx env next in
let next', env = scopes ~leave_unresolved ctx env next in
let next_bind' = Bindlib.bind_var (Var.translate var) next' in
Bindlib.box_apply2 (fun item next -> A.Cons (item, next)) def next_bind'
( Bindlib.box_apply2 (fun item next -> A.Cons (item, next)) def next_bind',
env )
let program ~leave_unresolved prg =
let code_items =
Bindlib.unbox
(scopes ~leave_unresolved prg.A.decl_ctx (Env.empty prg.A.decl_ctx)
prg.A.code_items)
let code_items, new_env =
scopes ~leave_unresolved prg.A.decl_ctx (Env.empty prg.A.decl_ctx)
prg.A.code_items
in
{ prg with code_items }
{
A.code_items = Bindlib.unbox code_items;
decl_ctx =
{
prg.decl_ctx with
ctx_structs =
A.StructName.Map.mapi
(fun s_name fields ->
A.StructField.Map.mapi
(fun f_name (t : A.typ) ->
match Mark.remove t with
| TAny ->
typ_to_ast ~leave_unresolved
(A.StructField.Map.find f_name
(A.StructName.Map.find s_name new_env.structs))
| _ -> t)
fields)
prg.decl_ctx.ctx_structs;
ctx_enums =
A.EnumName.Map.mapi
(fun e_name cons ->
A.EnumConstructor.Map.mapi
(fun cons_name (t : A.typ) ->
match Mark.remove t with
| TAny ->
typ_to_ast ~leave_unresolved
(A.EnumConstructor.Map.find cons_name
(A.EnumName.Map.find e_name new_env.enums))
| _ -> t)
cons)
prg.decl_ctx.ctx_enums;
};
}

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

@ -204,6 +204,8 @@ let rec print_z3model_expr (ctx : context) (ty : typ) (e : Expr.expr) : string =
(* For now, only the length of arrays is modeled *)
Format.asprintf "(length = %s)" (Expr.to_string e)
| TAny -> failwith "[Z3 model]: Pretty-printing of Any not supported"
| TClosureEnv ->
failwith "[Z3 model]: Pretty-printing of closure_env not supported"
(** [print_model] pretty prints a Z3 model, used to exhibit counter examples
where verification conditions are not satisfied. The context [ctx] is useful
@ -277,6 +279,7 @@ let rec translate_typ (ctx : context) (t : naked_typ) : context * Sort.sort =
Ultimately, the type of an array should also contain its elements *)
ctx, Arithmetic.Integer.mk_sort ctx.ctx_z3
| TAny -> failwith "[Z3 encoding] TAny type not supported"
| TClosureEnv -> failwith "[Z3 encoding] TClosureEnv type not supported"
(** [find_or_create_enum] attempts to retrieve the Z3 sort corresponding to the
Catala enumeration [enum]. If no such sort exists yet, it constructs it by

14
examples/aides_logement/tests/tests_calculette_globale.catala_fr
View File

@ -168,6 +168,13 @@ $ catala Interpret_Lcalc -s Exemple1 --avoid_exceptions
[RESULT] éligibilité = ESome true
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple1 --avoid_exceptions -O --closure_conversion
[RESULT] Computation successful! Results:
[RESULT] montant_versé = ESome 246.23 €
[RESULT] éligibilité = ESome true
```
```catala-test-inline
$ catala Interpret -s Exemple2
[RESULT] Computation successful! Results:
@ -181,3 +188,10 @@ $ catala Interpret -s Exemple2 --avoid_exceptions
[RESULT] montant_versé = 230.63 €
[RESULT] éligibilité = true
```
```catala-test-inline
$ catala Interpret -s Exemple2 --avoid_exceptions -O --closure_conversion
[RESULT] Computation successful! Results:
[RESULT] montant_versé = 230.63 €
[RESULT] éligibilité = true
```

878
french_law/js/src/french_law.js generated
View File

File diff suppressed because one or more lines are too long

1
french_law/ocaml/law_source/aides_logement.ml generated
View File

@ -1,3 +1,4 @@
(** This file has been generated by the Catala compiler, do not edit! *)
open Runtime_ocaml.Runtime

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

@ -1,3 +1,4 @@
(** This file has been generated by the Catala compiler, do not edit! *)
open Runtime_ocaml.Runtime

13618
french_law/python/src/aides_logement.py generated
View File

File diff suppressed because it is too large Load Diff

20
tests/test_array/good/aggregation_3.catala_en
View File

@ -41,27 +41,27 @@ let scope S (x: integer|internal|output) =
filter (λ (i: integer) → i > 2) [ 1; 2; 3 ])
= [ 5 ];
assert (reduce
(λ (sum1: integer) (sum2: integer) → sum1 + sum2),
0,
(λ (sum1: integer) (sum2: integer) → sum1 + sum2)
0
[ 1; 2; 3 ])
= 6;
assert (reduce
(λ (sum1: integer) (sum2: integer) → sum1 + sum2),
0,
(λ (sum1: integer) (sum2: integer) → sum1 + sum2)
0
map (λ (i: integer) → i + 2) [ 1; 2; 3 ])
= 12;
assert (length [ 1; 2; 3 ]) = 3;
assert (length filter (λ (i: integer) → i >= 2) [ 1; 2; 3 ]) = 2;
assert (reduce
(λ (max1: integer) (max2: integer) →
if max1 > max2 then max1 else max2),
10,
if max1 > max2 then max1 else max2)
10
[ 1; 2; 3 ])
= 3;
assert (reduce
(λ (max1: decimal) (max2: decimal) →
if max1 > max2 then max1 else max2),
10.,
if max1 > max2 then max1 else max2)
10.
map (λ (i: integer) → to_rat i) [ 1; 2; 3 ])
= 3.;
assert (reduce
@ -72,8 +72,8 @@ let scope S (x: integer|internal|output) =
< let i : integer = i_2 in
to_rat ((2 - i) * (2 - i))
then i_1
else i_2),
42,
else i_2)
42
[ 1; 2; 3 ])
= 2
```

4
tests/test_bool/bad/bad_assert.catala_en
View File

@ -13,8 +13,8 @@ scope Foo:
```catala-test-inline
$ catala Interpret -s Foo
[ERROR] Error during typechecking, incompatible types:
--> integer
--> bool
┌─⯈ integer
└─⯈ bool
Error coming from typechecking the following expression:
┌─⯈ tests/test_bool/bad/bad_assert.catala_en:9.13-9.14:

4
tests/test_bool/bad/test_xor_with_int.catala_en
View File

@ -11,8 +11,8 @@ scope TestXorWithInt:
```catala-test-inline
$ catala Typecheck
[ERROR] Error during typechecking, incompatible types:
--> integer
--> bool
┌─⯈ integer
└─⯈ bool
Error coming from typechecking the following expression:
┌─⯈ tests/test_bool/bad/test_xor_with_int.catala_en:8.30-8.32:

4
tests/test_enum/bad/quick_pattern_2.catala_en
View File

@ -31,8 +31,8 @@ scope B:
```catala-test-inline
$ catala Interpret -s A
[ERROR] Error during typechecking, incompatible types:
--> E
--> F
┌─⯈ E
└─⯈ F
Error coming from typechecking the following expression:
┌─⯈ tests/test_enum/bad/quick_pattern_2.catala_en:28.23-28.24:

4
tests/test_enum/bad/quick_pattern_3.catala_en
View File

@ -21,8 +21,8 @@ definition y equals x with pattern Case3
```catala-test-inline
$ catala Interpret -s A
[ERROR] Error during typechecking, incompatible types:
--> E
--> F
┌─⯈ E
└─⯈ F
Error coming from typechecking the following expression:
┌─⯈ tests/test_enum/bad/quick_pattern_3.catala_en:18.21-18.22:

4
tests/test_enum/bad/quick_pattern_4.catala_en
View File

@ -20,8 +20,8 @@ definition y equals x with pattern Case3
```catala-test-inline
$ catala Interpret -s A
[ERROR] Error during typechecking, incompatible types:
--> E
--> F
┌─⯈ E
└─⯈ F
Error coming from typechecking the following expression:
┌─⯈ tests/test_enum/bad/quick_pattern_4.catala_en:17.21-17.22:

47
tests/test_func/good/closure_conversion.catala_en
View File

@ -12,13 +12,44 @@ scope S:
```
```catala-test-inline
$ catala Lcalc -s S --avoid_exceptions -O --closure_conversion
[ERROR] Variable x not found in the current context
$ catala Lcalc --avoid_exceptions -O --closure_conversion
type eoption = | ENone of unit | ESome of any
type S = { z: eoption integer; }
type S_in = { x_in: eoption bool; }
let topval closure_f : (closure_env, integer) → eoption integer =
λ (env: closure_env) (y: integer) →
ESome
match
(match (from_closure_env env).0 with
| ENone _ → ENone _
| ESome x → if x then ESome y else ESome - y)
with
| ENone _ → raise NoValueProvided
| ESome f → f
let scope S (S_in: S_in {x_in: eoption bool}): S {z: eoption integer} =
let get x : eoption bool = S_in.x_in in
let set f :
eoption ((closure_env, integer) → eoption integer * closure_env) =
ESome (closure_f, to_closure_env (x))
in
let set z : eoption integer =
ESome
match
(match f with
| ENone _ → ENone _
| ESome f →
let code_and_env :
((closure_env, integer) → eoption integer * closure_env) =
f
in
code_and_env.0 code_and_env.1 -1)
with
| ENone _ → raise NoValueProvided
| ESome z → z
in
return { S z = z; }
┌─⯈ tests/test_func/good/closure_conversion.catala_en:5.12-5.13:
└─┐
5 │ internal f content integer depends on y content integer
│ ‾
└─ Article
#return code 255#
```

62
tests/test_func/good/closure_conversion_reduce.catala_en Normal file
View File

@ -0,0 +1,62 @@
# Article
```catala
declaration scope S:
input x content collection integer
output y content integer
scope S:
definition y equals
potential_max among x such that potential_max is minimum or if collection empty then -1
```
```catala-test-inline
$ catala Lcalc -s S --avoid_exceptions -O --closure_conversion
let scope S
(S_in: S_in {x_in: eoption collection eoption integer})
: S {y: eoption integer}
=
let get x : eoption collection eoption integer = S_in.x_in in
let set y : eoption integer =
ESome
match
(match x with
| ENone _ → ENone _
| ESome y_2 →
reduce
(λ (f: eoption integer) (init: eoption integer) →
match init with
| ENone _ → ENone _
| ESome y_3 →
match f with
| ENone _ → ENone _
| ESome y_0 →
let potential_max_1 : integer = y_0 in
let potential_max_2 : integer = y_3 in
if potential_max_1 < potential_max_2
then ESome potential_max_1
else ESome potential_max_2)
ESome -1
y_2)
with
| ENone _ → raise NoValueProvided
| ESome y → y
in
return { S y = y; }
```
The next test of closure conversion does not go through for the moment.
The detection of closures that should not be converted because they are arguments
to reduce or other special operators relies on pattern matching the special
operator and its EAbs argument. However without exceptions on, because the
--avoid_exceptions pass is not optimized and produces more options than needed,
the closures that are arguments to special operators are let-binded with an
option. This let-binding is reduced by partial evaluation, which is why the test
with optimizations on passes.
```catala-test-inline
$ catala Lcalc -s S --avoid_exceptions --closure_conversion
[ERROR] Option --optimize must be enabled for --closure_conversion
#return code 255#
```

35
tests/test_func/good/closure_return.catala_en
View File

@ -7,6 +7,37 @@ declaration scope S:
scope S:
definition f of y equals if x then y else - y
# TODO: pass this
```
```catala-test-inline
$ catala Lcalc --avoid_exceptions -O --closure_conversion
type eoption = | ENone of unit | ESome of any
type S = {
f: eoption ((closure_env, integer) → eoption integer * closure_env);
}
type S_in = { x_in: eoption bool; }
let topval closure_f : (closure_env, integer) → eoption integer =
λ (env: closure_env) (y: integer) →
ESome
match
(match (from_closure_env env).0 with
| ENone _ → ENone _
| ESome x → if x then ESome y else ESome - y)
with
| ENone _ → raise NoValueProvided
| ESome f → f
let scope S
(S_in: S_in {x_in: eoption bool})
: S {f: eoption ((closure_env, integer) → eoption integer * closure_env)}
=
let get x : eoption bool = S_in.x_in in
let set f :
eoption ((closure_env, integer) → eoption integer * closure_env) =
ESome (closure_f, to_closure_env (x))
in
return { S f = f; }
```

61
tests/test_func/good/closure_through_scope.catala_en Normal file
View File

@ -0,0 +1,61 @@
## Article
```catala
declaration scope S:
output f content integer depends on y content integer
input x content boolean
declaration scope T:
s scope S
output y content integer
scope S:
definition f of y equals if x then y else - y
scope T:
definition s.x equals false
definition y equals s.f of 2
```
```catala-test-inline
$ catala Lcalc -s T --avoid_exceptions -O --closure_conversion
let scope T (T_in: T_in): T {y: eoption integer} =
let sub_set s.x : bool = false in
let call result :
eoption
S {
f:
eoption
((closure_env, integer) → eoption integer * closure_env)
} =
ESome S { S_in x_in = ESome s.x; }
in
let sub_get s.f :
eoption ((closure_env, integer) → eoption integer * closure_env) =
match result with
| ENone _ → ENone _
| ESome result → result.f
in
let set y : eoption integer =
ESome
match
(match s.f with
| ENone _ → ENone _
| ESome s.f →
let code_and_env :
((closure_env, integer) → eoption integer * closure_env) =
s.f
in
code_and_env.0 code_and_env.1 2)
with
| ENone _ → raise NoValueProvided
| ESome y → y
in
return { T y = y; }
```
```catala-test-inline
$ catala Interpret_lcalc -s T --avoid_exceptions -O --closure_conversion
[RESULT] Computation successful! Results:
[RESULT] y = ESome -2
```

245
tests/test_func/good/scope_call_func_struct_closure.catala_en Normal file
View File

@ -0,0 +1,245 @@
```catala
declaration structure Result:
data r content integer depends on z content integer
data q content integer
declaration scope SubFoo1:
input output x content integer
output y content integer depends on z content integer
declaration scope SubFoo2:
input output x1 content integer
input x2 content integer
output y content integer depends on z content integer
declaration scope Foo:
context b content boolean
internal r content Result
output z content integer
scope SubFoo1:
definition y of z equals x + z
scope SubFoo2:
definition y of z equals x1 + x2 + z
scope Foo:
definition b equals true
definition r equals
if b then
let f equals output of SubFoo1 with { -- x: 10 } in
Result { --r: f.y --q: f.x }
else
let f equals output of SubFoo2 with { -- x1: 10 -- x2: 10 } in
Result { --r: f.y --q: f.x1 }
definition z equals r.r of 1
```
This test case is tricky because it creates a situation where the type of the
two closures in Foo.r are different even with optimizations enabled.
```catala-test-inline
$ catala Lcalc --avoid_exceptions -O --closure_conversion
type eoption = | ENone of unit | ESome of any
type Result = {
r: eoption ((closure_env, integer) → eoption integer * closure_env);
q: eoption integer;
}
type SubFoo1 = {
x: eoption integer;
y: eoption ((closure_env, integer) → eoption integer * closure_env);
}
type SubFoo2 = {
x1: eoption integer;
y: eoption ((closure_env, integer) → eoption integer * closure_env);
}
type Foo = { z: eoption integer; }
type SubFoo1_in = { x_in: eoption integer; }
type SubFoo2_in = { x1_in: eoption integer; x2_in: eoption integer; }
type Foo_in = { b_in: eoption bool; }
let topval closure_y : (closure_env, integer) → eoption integer =
λ (env: closure_env) (z: integer) →
ESome
match
(match (from_closure_env env).0 with
| ENone _ → ENone _
| ESome x_0 → ESome (x_0 + z))
with
| ENone _ → raise NoValueProvided
| ESome y → y
let scope SubFoo1
(SubFoo1_in: SubFoo1_in {x_in: eoption integer})
: SubFoo1 {
x: eoption integer;
y: eoption ((closure_env, integer) → eoption integer * closure_env)
}
=
let get x : eoption integer = SubFoo1_in.x_in in
let set y :
eoption ((closure_env, integer) → eoption integer * closure_env) =
ESome (closure_y, to_closure_env (x))
in
return { SubFoo1 x = x; y = y; }
let topval closure_y : (closure_env, integer) → eoption integer =
λ (env: closure_env) (z: integer) →
let env1 : (eoption integer * eoption integer) = from_closure_env env in
ESome
match
(match
(match env1.0 with
| ENone _ → ENone _
| ESome x1_1 →
match env1.1 with
| ENone _ → ENone _
| ESome x1_0 → ESome (x1_0 + x1_1))
with
| ENone _ → ENone _
| ESome y_0 → ESome (y_0 + z))
with
| ENone _ → raise NoValueProvided
| ESome y → y
let scope SubFoo2
(SubFoo2_in: SubFoo2_in {x1_in: eoption integer; x2_in: eoption integer})
: SubFoo2 {
x1: eoption integer;
y: eoption ((closure_env, integer) → eoption integer * closure_env)
}
=
let get x1 : eoption integer = SubFoo2_in.x1_in in
let get x2 : eoption integer = SubFoo2_in.x2_in in
let set y :
eoption ((closure_env, integer) → eoption integer * closure_env) =
ESome (closure_y, to_closure_env (x2, x1))
in
return { SubFoo2 x1 = x1; y = y; }
let topval closure_r : (closure_env, integer) → eoption integer =
λ (env: closure_env) (param0: integer) →
match (SubFoo2 { SubFoo2_in x1_in = ESome 10; x2_in = ESome 10; }).y with
| ENone _ → ENone _
| ESome result →
let code_and_env :
((closure_env, integer) → eoption integer * closure_env) =
result
in
code_and_env.0 code_and_env.1 param0
let topval closure_r : (closure_env, integer) → eoption integer =
λ (env: closure_env) (param0: integer) →
match (SubFoo1 { SubFoo1_in x_in = ESome 10; }).y with
| ENone _ → ENone _
| ESome result →
let code_and_env :
((closure_env, integer) → eoption integer * closure_env) =
result
in
code_and_env.0 code_and_env.1 param0
let scope Foo
(Foo_in: Foo_in {b_in: eoption bool})
: Foo {z: eoption integer}
=
let get b : eoption bool = Foo_in.b_in in
let set b : eoption bool =
ESome
match
(handle_default_opt
[ b ]
(λ (_: unit) → ESome true)
(λ (_: unit) → ESome true))
with
| ENone _ → raise NoValueProvided
| ESome b → b
in
let set r :
eoption
Result {
r:
eoption
((closure_env, integer) → eoption integer * closure_env);
q: eoption integer
} =
ESome
match
(match b with
| ENone _ → ENone _
| ESome b →
if b
then
match
(match (SubFoo1 { SubFoo1_in x_in = ESome 10; }).x with
| ENone _ → ENone _
| ESome result_0 →
ESome
{ SubFoo1
x = ESome result_0;
y = ESome (closure_r, to_closure_env ());
})
with
| ENone _ → ENone _
| ESome f →
match f.x with
| ENone _ → ENone _
| ESome f_1 →
match f.y with
| ENone _ → ENone _
| ESome f_0 → ESome { Result r = ESome f_0; q = ESome f_1; }
else
match
(match
(SubFoo2 { SubFoo2_in x1_in = ESome 10; x2_in = ESome 10; }).
x1
with
| ENone _ → ENone _
| ESome result_0 →
ESome
{ SubFoo2
x1 = ESome result_0;
y = ESome (closure_r, to_closure_env ());
})
with
| ENone _ → ENone _
| ESome f →
match f.x1 with
| ENone _ → ENone _
| ESome f_1 →
match f.y with
| ENone _ → ENone _
| ESome f_0 → ESome { Result r = ESome f_0; q = ESome f_1; })
with
| ENone _ → raise NoValueProvided
| ESome r → r
in
let set z : eoption integer =
ESome
match
(match (match r with
| ENone _ → ENone _
| ESome r → r.r) with
| ENone _ → ENone _
| ESome r →
let code_and_env :
((closure_env, integer) → eoption integer * closure_env) =
r
in
code_and_env.0 code_and_env.1 1)
with
| ENone _ → raise NoValueProvided
| ESome z → z
in
return { Foo z = z; }
```
```catala-test-inline
$ catala Interpret_lcalc -s Foo --avoid_exceptions -O --closure_conversion
[RESULT] Computation successful! Results:
[RESULT] z = ESome 11
```

11
tests/test_scope/good/scope_call.catala_en
View File

@ -1,8 +1,4 @@
```catala
declaration structure Test:
data z2 content integer
data z3 content integer
declaration scope SubFoo:
input x content integer
input y content integer
@ -26,13 +22,6 @@ scope Foo:
```catala-test-inline
$ catala interpret -s Foo
[WARNING] The structure "Test" is never used; maybe it's unnecessary?
┌─⯈ tests/test_scope/good/scope_call.catala_en:2.23-2.27:
└─┐
2 │ declaration structure Test:
│ ‾‾‾‾
[RESULT] Computation successful! Results:
[RESULT] example = -7
```

12
tests/test_scope/good/scope_call4.catala_en
View File

@ -46,10 +46,10 @@ f1 =
match
(match (ESome (λ (x1: integer) → ESome (x1 + 1))) with
| ENone _ → ENone _
| ESome f1 → f1 (x + 1))
| ESome g → g (x + 1))
with
| ENone f1 → raise NoValueProvided
| ESome x1 → x1)
| ENone _ → raise NoValueProvided
| ESome f1 → f1)
[RESULT]
f2 =
ESome
@ -58,8 +58,8 @@ f2 =
match
(match (ESome (λ (x1: integer) → ESome (x1 + 1))) with
| ENone _ → ENone _
| ESome f2 → f2 (x + 1))
| ESome g → g (x + 1))
with
| ENone f2 → raise NoValueProvided
| ESome x1 → x1)
| ENone _ → raise NoValueProvided
| ESome f2 → f2)
```

2
tests/test_scope/good/simple.catala_en
View File

@ -12,7 +12,7 @@ scope Foo:
$ catala Lcalc -s Foo
let scope Foo (Foo_in: Foo_in): Foo {bar: integer} =
let set bar : integer =
try handle_default [ ], (λ (_: unit) → true), (λ (_: unit) → 0)
try handle_default [ ] (λ (_: unit) → true) (λ (_: unit) → 0)
with EmptyError -> raise NoValueProvided
in
return { Foo bar = bar; }

4
tests/test_typing/bad/err1.catala_en
View File

@ -13,8 +13,8 @@ scope S:
```catala-test-inline
$ catala Typecheck
[ERROR] Error during typechecking, incompatible types:
--> decimal
--> integer
┌─⯈ decimal
└─⯈ integer
Error coming from typechecking the following expression:
┌─⯈ tests/test_typing/bad/err1.catala_en:7.23-7.26:

4
tests/test_typing/bad/err2.catala_en
View File

@ -13,8 +13,8 @@ scope S:
```catala-test-inline
$ catala Typecheck
[ERROR] Error during typechecking, incompatible types:
--> decimal
--> collection
┌─⯈ decimal
└─⯈ collection
Error coming from typechecking the following expression:
┌─⯈ tests/test_typing/bad/err2.catala_en:10.39-10.42:

8
tests/test_typing/bad/err3.catala_en
View File

@ -20,8 +20,8 @@ $ catala Typecheck
│ ‾‾‾
[ERROR] Error during typechecking, incompatible types:
--> integer
--> decimal
┌─⯈ integer
└─⯈ decimal
Error coming from typechecking the following expression:
┌─⯈ tests/test_typing/bad/err3.catala_en:10.42-10.43:
@ -58,8 +58,8 @@ $ catala ocaml
│ ‾‾‾
[ERROR] Error during typechecking, incompatible types:
--> integer
--> decimal
┌─⯈ integer
└─⯈ decimal
Error coming from typechecking the following expression:
┌─⯈ tests/test_typing/bad/err3.catala_en:10.42-10.43:

4
tests/test_typing/bad/err4.catala_en
View File

@ -32,8 +32,8 @@ $ catala ocaml
│ ‾‾‾
[ERROR] Error during typechecking, incompatible types:
--> Enum
--> Structure
┌─⯈ Enum
└─⯈ Structure
Error coming from typechecking the following expression:
┌─⯈ tests/test_typing/bad/err4.catala_en:5.25-5.38:

4
tests/test_typing/bad/err5.catala_en
View File

@ -13,8 +13,8 @@ scope S:
```catala-test-inline
$ catala Typecheck
[ERROR] Error during typechecking, incompatible types:
--> integer
--> Structure
┌─⯈ integer
└─⯈ Structure
Error coming from typechecking the following expression:
┌─⯈ tests/test_typing/bad/err5.catala_en:8.5-8.9:

4
tests/test_typing/bad/err6.catala_en
View File

@ -29,8 +29,8 @@ Should be "catala Typecheck", see test err3
```catala-test-inline
$ catala ocaml
[ERROR] Error during typechecking, incompatible types:
--> decimal
--> integer
┌─⯈ decimal
└─⯈ integer
Error coming from typechecking the following expression:
┌─⯈ tests/test_typing/bad/err6.catala_en:20.27-20.30: