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

Internally type default terms in the compiler (#528)

Browse Source
This commit is contained in:
Louis Gesbert 2023-11-28 13:51:42 +01:00 committed by GitHub
commit 1b02a672fa
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
138 changed files with 1781 additions and 1865 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
build_system/dune
View File

@ -32,5 +32,7 @@
(:standard
(:include custom_linking.sexp)))
(libraries clerk.driver)
(link_deps ../compiler/catala.exe)
; not a real dependency, but when running clerk in practice you always want the catala binary to be up-to-date (e.g. `dune exec -- ckerk test`)
(modules clerk)
(package clerk))

7
compiler/catala_utils/cli.ml
View File

@ -346,6 +346,11 @@ module Flags = struct
& flag
& info ["check_invariants"] ~doc:"Check structural invariants on the AST."
let no_typing =
value
& flag
& info ["no-typing"] ~doc:"Don't check the consistency of types"
let wrap_weaved_output =
value
& flag
@ -400,7 +405,7 @@ module Flags = struct
& info ["closure_conversion"]
~doc:
"Performs closure conversion on the lambda calculus. Implies \
$(b,--avoid-exceptions) and $(b,--optimize)."
$(b,--avoid-exceptions)."
let disable_counterexamples =
value

1
compiler/catala_utils/cli.mli
View File

@ -113,6 +113,7 @@ module Flags : sig
(** Parsers for all flags and options that commands can use *)
val check_invariants : bool Term.t
val no_typing : bool Term.t
val wrap_weaved_output : bool Term.t
val print_only_law : bool Term.t
val ex_scope : string Term.t

2
compiler/catala_web_interpreter.ml
View File

@ -25,7 +25,7 @@ let () =
in
let prg, ctx, _type_order =
Passes.dcalc options ~includes:[] ~optimize:false
~check_invariants:false
~check_invariants:false ~typed:Shared_ast.Expr.typed
in
Shared_ast.Interpreter.interpret_program_dcalc prg
(Commands.get_scope_uid ctx scope)

92
compiler/dcalc/from_scopelang.ml
View File

@ -117,10 +117,12 @@ let merge_defaults
(Expr.with_ty m_callee
(Mark.add (Expr.mark_pos m_callee) (TLit TBool)))
in
let d = Expr.edefault [caller] ltrue (Expr.rebox body) m_body in
Expr.make_abs vars
(Expr.eerroronempty d m_body)
tys (Expr.mark_pos m_callee)
let cons = Expr.make_puredefault (Expr.rebox body) in
let d =
Expr.edefault ~excepts:[caller] ~just:ltrue ~cons (Mark.get cons)
in
Expr.make_abs vars (Expr.make_erroronempty d) tys (Expr.mark_pos m_callee)
| _ -> assert false
(* should not happen because there should always be a lambda at the
beginning of a default with a function type *)
@ -138,7 +140,9 @@ let merge_defaults
Expr.elit (LBool true)
(Expr.with_ty m (Mark.add (Expr.mark_pos m) (TLit TBool)))
in
Expr.eerroronempty (Expr.edefault [caller] ltrue callee m) m
let cons = Expr.make_puredefault callee in
Expr.make_erroronempty
(Expr.edefault ~excepts:[caller] ~just:ltrue ~cons (Mark.get cons))
in
body
@ -216,7 +220,7 @@ let input_var_typ typ io_in =
let thunk_scope_arg var_ctx e =
match var_ctx.scope_input_io, var_ctx.scope_input_thunked with
| (Runtime.NoInput, _), _ -> invalid_arg "thunk_scope_arg"
| (Runtime.OnlyInput, _), false -> Expr.eerroronempty e (Mark.get e)
| (Runtime.OnlyInput, _), false -> e
| (Runtime.Reentrant, _), false -> e
| (Runtime.Reentrant, pos), true ->
Expr.make_abs [| Var.make "_" |] e [TLit TUnit, pos] pos
@ -291,11 +295,18 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
]
"Definition of input variable '%a' missing in this scope call"
ScopeVar.format var_name
| None, Some _ ->
Message.raise_multispanned_error
| None, Some e ->
Message.raise_multispanned_error_full
~suggestion:
(List.map
(fun v -> Mark.remove (ScopeVar.get_info v))
(ScopeVar.Map.keys sc_sig.scope_sig_in_fields))
[
None, pos;
( Some "Declaration of scope '%a'",
None, Expr.pos e;
( Some
(fun ppf ->
Format.fprintf ppf "Declaration of scope %a"
ScopeName.format scope),
Mark.get (ScopeName.get_info scope) );
]
"Unknown input variable '%a' in scope call of '%a'"
@ -562,8 +573,9 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
| EDefault { excepts; just; cons } ->
let excepts = collapse_similar_outcomes excepts in
Expr.edefault
(List.map (translate_expr ctx) excepts)
(translate_expr ctx just) (translate_expr ctx cons) m
~excepts:(List.map (translate_expr ctx) excepts)
~just:(translate_expr ctx just) ~cons:(translate_expr ctx cons) m
| EPureDefault e -> Expr.epuredefault (translate_expr ctx e) m
| ELocation (ScopelangScopeVar { name = a }) ->
let v, _, _ = ScopeVar.Map.find (Mark.remove a) ctx.scope_vars in
Expr.evar v m
@ -615,7 +627,7 @@ let translate_rule
* 'm ctx =
match rule with
| Definition ((ScopelangScopeVar { name = a }, var_def_pos), tau, a_io, e) ->
let pos_mark, pos_mark_as = pos_mark_mk e in
let pos_mark, _ = pos_mark_mk e in
let a_name = ScopeVar.get_info (Mark.remove a) in
let a_var = Var.make (Mark.remove a_name) in
let new_e = translate_expr ctx e in
@ -626,8 +638,7 @@ let translate_rule
| OnlyInput -> failwith "should not happen"
(* scopelang should not contain any definitions of input only variables *)
| Reentrant -> merge_defaults ~is_func a_expr new_e
| NoInput ->
if is_func then new_e else Expr.eerroronempty new_e (pos_mark_as a_name)
| NoInput -> new_e
in
let merged_expr =
tag_with_log_entry merged_expr
@ -682,7 +693,7 @@ let translate_rule
let thunked_or_nonempty_new_e =
match a_io.Desugared.Ast.io_input with
| Runtime.NoInput, _ -> assert false
| Runtime.OnlyInput, _ -> Expr.eerroronempty new_e (Mark.get new_e)
| Runtime.OnlyInput, _ -> new_e
| Runtime.Reentrant, pos -> (
match Mark.remove tau with
| TArrow _ -> new_e
@ -738,10 +749,25 @@ let translate_rule
| _ -> true)
all_subscope_vars
in
let called_scope_input_struct = subscope_sig.scope_sig_input_struct in
let called_scope_return_struct = subscope_sig.scope_sig_output_struct in
let all_subscope_output_vars =
List.filter
List.filter_map
(fun var_ctx ->
Mark.remove var_ctx.scope_var_io.Desugared.Ast.io_output)
if Mark.remove var_ctx.scope_var_io.Desugared.Ast.io_output then
(* Retrieve the actual expected output type through the scope output
struct definition *)
let str =
StructName.Map.find called_scope_return_struct
ctx.decl_ctx.ctx_structs
in
let fld =
ScopeVar.Map.find var_ctx.scope_var_name
scope_sig_decl.out_struct_fields
in
let ty = StructField.Map.find fld str in
Some { var_ctx with scope_var_typ = Mark.remove ty }
else None)
all_subscope_vars
in
let pos_call = Mark.get (SubScopeName.get_info subindex) in
@ -752,8 +778,6 @@ let translate_rule
| External_scope_ref name ->
Expr.eexternal ~name:(Mark.map (fun n -> External_scope n) name) m
in
let called_scope_input_struct = subscope_sig.scope_sig_input_struct in
let called_scope_return_struct = subscope_sig.scope_sig_output_struct in
let subscope_vars_defined =
try SubScopeName.Map.find subindex ctx.subscope_vars
with SubScopeName.Map.Not_found _ -> ScopeVar.Map.empty
@ -886,11 +910,9 @@ let translate_rule
scope_let_pos;
scope_let_typ;
scope_let_expr =
(* To ensure that we throw an error if the value is not
defined, we add an check "ErrorOnEmpty" here. *)
Mark.add
(Expr.map_ty (fun _ -> scope_let_typ) (Mark.get e))
(EAssert (Mark.copy e (EErrorOnEmpty new_e)));
(EAssert new_e);
scope_let_kind = Assertion;
})
(Bindlib.bind_var (Var.make "_") next)
@ -1092,9 +1114,10 @@ let translate_program (prgm : 'm Scopelang.Ast.program) : 'm Ast.program =
as the return type of ScopeCalls) ; but input fields are used purely
internally and need to be created here to implement the call
convention for scopes. *)
let module S = Scopelang.Ast in
ScopeVar.Map.filter_map
(fun dvar (typ, vis) ->
match Mark.remove vis.Desugared.Ast.io_input with
(fun dvar svar ->
match Mark.remove svar.S.svar_io.Desugared.Ast.io_input with
| NoInput -> None
| OnlyInput | Reentrant ->
let info = ScopeVar.get_info dvar in
@ -1102,22 +1125,27 @@ let translate_program (prgm : 'm Scopelang.Ast.program) : 'm Ast.program =
Some
{
scope_input_name = StructField.fresh (s, Mark.get info);
scope_input_io = vis.Desugared.Ast.io_input;
scope_input_io = svar.S.svar_io.Desugared.Ast.io_input;
scope_input_typ =
Mark.remove (input_var_typ (Mark.remove typ) vis);
Mark.remove
(input_var_typ
(Mark.remove svar.S.svar_in_ty)
svar.S.svar_io);
scope_input_thunked =
input_var_needs_thunking (Mark.remove typ) vis;
input_var_needs_thunking
(Mark.remove svar.S.svar_in_ty)
svar.S.svar_io;
})
scope.Scopelang.Ast.scope_sig
scope.S.scope_sig
in
{
scope_sig_local_vars =
List.map
(fun (scope_var, (tau, vis)) ->
(fun (scope_var, svar) ->
{
scope_var_name = scope_var;
scope_var_typ = Mark.remove tau;
scope_var_io = vis;
scope_var_typ = Mark.remove svar.Scopelang.Ast.svar_in_ty;
scope_var_io = svar.Scopelang.Ast.svar_io;
})
(ScopeVar.Map.bindings scope.scope_sig);
scope_sig_scope_ref = scope_ref;

5
compiler/desugared/disambiguate.ml
View File

@ -82,7 +82,10 @@ let program prg =
| SubScopeVar _ -> vars)
scope.scope_defs ScopeVar.Map.empty
in
Typing.Env.add_scope scope_name ~vars env)
(* at this stage, rule resolution and the corresponding encapsulation
into default terms hasn't taken place, so input and output
variables don't need different typing *)
Typing.Env.add_scope scope_name ~vars ~in_vars:vars env)
prg.program_scopes env
in
env

1
compiler/desugared/from_surface.ml
View File

@ -446,6 +446,7 @@ let rec translate_expr
| Some (ScopeVar v) -> v
| Some (SubScope _) | None ->
Message.raise_multispanned_error
~suggestion:(Ident.Map.keys scope_def.var_idmap)
[
None, Mark.get fld_id;
( Some

119
compiler/driver.ml
View File

@ -141,18 +141,31 @@ module Passes = struct
in
prg, ctx, exceptions_graphs
let dcalc options ~includes ~optimize ~check_invariants :
typed Dcalc.Ast.program
let dcalc :
type ty.
Cli.options ->
includes:Cli.raw_file list ->
optimize:bool ->
check_invariants:bool ->
typed:ty mark ->
ty Dcalc.Ast.program
* Desugared.Name_resolution.context
* Scopelang.Dependency.TVertex.t list =
fun options ~includes ~optimize ~check_invariants ~typed ->
let prg, ctx, _ = scopelang options ~includes in
debug_pass_name "dcalc";
let type_ordering =
Scopelang.Dependency.check_type_cycles prg.program_ctx.ctx_structs
prg.program_ctx.ctx_enums
in
let (prg : ty Scopelang.Ast.program) =
match typed with
| Typed _ ->
Message.emit_debug "Typechecking...";
let prg = Scopelang.Ast.type_program prg in
Scopelang.Ast.type_program prg
| Untyped _ -> prg
| Custom _ -> invalid_arg "Driver.Passes.dcalc"
in
Message.emit_debug "Translating to default calculus...";
let prg = Dcalc.From_scopelang.translate_program prg in
let prg =
@ -162,47 +175,66 @@ module Passes = struct
end
else prg
in
let (prg : ty Dcalc.Ast.program) =
match typed with
| Typed _ -> (
Message.emit_debug "Typechecking again...";
let prg =
try Typing.program ~leave_unresolved:false prg
with Message.CompilerError error_content ->
let bt = Printexc.get_raw_backtrace () in
Printexc.raise_with_backtrace
(Message.CompilerError
(Message.Content.to_internal_error error_content))
bt
bt)
| Untyped _ -> prg
| Custom _ -> assert false
in
if check_invariants then (
Message.emit_debug "Checking invariants...";
match typed with
| Typed _ ->
let result = Dcalc.Invariants.check_all_invariants prg in
if not result then
raise (Message.raise_internal_error "Some Dcalc invariants are invalid"));
raise
(Message.raise_internal_error "Some Dcalc invariants are invalid")
| _ ->
Message.raise_error "--check_invariants cannot be used with --no-typing");
prg, ctx, type_ordering
let lcalc
(type ty)
options
~includes
~optimize
~check_invariants
~(typed : ty mark)
~avoid_exceptions
~closure_conversion :
untyped Lcalc.Ast.program
* Desugared.Name_resolution.context
* Scopelang.Dependency.TVertex.t list =
let prg, ctx, type_ordering =
dcalc options ~includes ~optimize ~check_invariants
dcalc options ~includes ~optimize ~check_invariants ~typed
in
debug_pass_name "lcalc";
let avoid_exceptions = avoid_exceptions || closure_conversion in
let optimize = optimize || closure_conversion in
(* --closure_conversion implies --avoid_exceptions and --optimize *)
(* --closure_conversion implies --avoid_exceptions *)
let prg =
if avoid_exceptions then (
if options.trace then
match avoid_exceptions, options.trace, typed with
| true, true, _ ->
Message.raise_error
"Option --avoid_exceptions is not compatible with option --trace";
Lcalc.Compile_without_exceptions.translate_program prg)
else Program.untype (Lcalc.Compile_with_exceptions.translate_program prg)
"Option --avoid_exceptions is not compatible with option --trace"
| true, _, Untyped _ ->
Program.untype
(Lcalc.Compile_without_exceptions.translate_program
(Shared_ast.Typing.program ~leave_unresolved:false prg))
| true, _, Typed _ ->
Lcalc.Compile_without_exceptions.translate_program prg
| false, _, Typed _ ->
Program.untype (Lcalc.Compile_with_exceptions.translate_program prg)
| false, _, Untyped _ ->
Lcalc.Compile_with_exceptions.translate_program prg
| _, _, Custom _ -> invalid_arg "Driver.Passes.lcalc"
in
let prg =
if optimize then begin
@ -223,9 +255,15 @@ module Passes = struct
Optimizations.optimize_program prg)
else prg
in
match typed with
| Untyped _ -> prg
| Typed _ ->
Message.emit_debug "Retyping lambda calculus...";
let prg = Program.untype (Typing.program ~leave_unresolved:true prg) in
prg)
let prg =
Program.untype (Typing.program ~leave_unresolved:true prg)
in
prg
| Custom _ -> assert false)
in
prg, ctx, type_ordering
@ -240,8 +278,8 @@ module Passes = struct
* Desugared.Name_resolution.context
* Scopelang.Dependency.TVertex.t list =
let prg, ctx, type_ordering =
lcalc options ~includes ~optimize ~check_invariants ~avoid_exceptions
~closure_conversion
lcalc options ~includes ~optimize ~check_invariants ~typed:Expr.typed
~avoid_exceptions ~closure_conversion
in
debug_pass_name "scalc";
Scalc.From_lcalc.translate_program prg, ctx, type_ordering
@ -507,9 +545,10 @@ module Commands = struct
~doc:"Parses and typechecks a Catala program, without interpreting it.")
Term.(const typecheck $ Cli.Flags.Global.options $ Cli.Flags.include_dirs)
let dcalc options includes output optimize ex_scope_opt check_invariants =
let dcalc typed options includes output optimize ex_scope_opt check_invariants
=
let prg, ctx, _ =
Passes.dcalc options ~includes ~optimize ~check_invariants
Passes.dcalc options ~includes ~optimize ~check_invariants ~typed
in
let _output_file, with_output = get_output_format options output in
with_output
@ -537,6 +576,9 @@ module Commands = struct
prg_dcalc_expr
let dcalc_cmd =
let f no_typing =
if no_typing then dcalc Expr.untyped else dcalc Expr.typed
in
Cmd.v
(Cmd.info "dcalc"
~doc:
@ -544,7 +586,8 @@ module Commands = struct
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope.")
Term.(
const dcalc
const f
$ Cli.Flags.no_typing
$ Cli.Flags.Global.options
$ Cli.Flags.include_dirs
$ Cli.Flags.output
@ -561,6 +604,7 @@ module Commands = struct
disable_counterexamples =
let prg, ctx, _ =
Passes.dcalc options ~includes ~optimize ~check_invariants
~typed:Expr.typed
in
Verification.Globals.setup ~optimize ~disable_counterexamples;
let vcs =
@ -608,15 +652,20 @@ module Commands = struct
result)
results
let interpret_dcalc options includes optimize check_invariants ex_scope =
let interpret_dcalc typed options includes optimize check_invariants ex_scope
=
let prg, ctx, _ =
Passes.dcalc options ~includes ~optimize ~check_invariants
Passes.dcalc options ~includes ~optimize ~check_invariants ~typed
in
Interpreter.load_runtime_modules prg;
print_interpretation_results options Interpreter.interpret_program_dcalc prg
(get_scope_uid ctx ex_scope)
let interpret_cmd =
let f no_typing =
if no_typing then interpret_dcalc Expr.untyped
else interpret_dcalc Expr.typed
in
Cmd.v
(Cmd.info "interpret"
~doc:
@ -624,7 +673,8 @@ module Commands = struct
specified by the $(b,-s) option assuming no additional external \
inputs.")
Term.(
const interpret_dcalc
const f
$ Cli.Flags.no_typing
$ Cli.Flags.Global.options
$ Cli.Flags.include_dirs
$ Cli.Flags.optimize
@ -632,6 +682,7 @@ module Commands = struct
$ Cli.Flags.ex_scope)
let lcalc
typed
options
includes
output
@ -642,7 +693,7 @@ module Commands = struct
ex_scope_opt =
let prg, ctx, _ =
Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion
~avoid_exceptions ~closure_conversion ~typed
in
let _output_file, with_output = get_output_format options output in
with_output
@ -658,6 +709,9 @@ module Commands = struct
Format.pp_print_newline fmt ()
let lcalc_cmd =
let f no_typing =
if no_typing then lcalc Expr.untyped else lcalc Expr.typed
in
Cmd.v
(Cmd.info "lcalc"
~doc:
@ -665,7 +719,8 @@ module Commands = struct
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope.")
Term.(
const lcalc
const f
$ Cli.Flags.no_typing
$ Cli.Flags.Global.options
$ Cli.Flags.include_dirs
$ Cli.Flags.output
@ -676,6 +731,7 @@ module Commands = struct
$ Cli.Flags.ex_scope_opt)
let interpret_lcalc
typed
options
includes
optimize
@ -685,13 +741,17 @@ module Commands = struct
ex_scope =
let prg, ctx, _ =
Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion
~avoid_exceptions ~closure_conversion ~typed
in
Interpreter.load_runtime_modules prg;
print_interpretation_results options Interpreter.interpret_program_lcalc prg
(get_scope_uid ctx ex_scope)
let interpret_lcalc_cmd =
let f no_typing =
if no_typing then interpret_lcalc Expr.untyped
else interpret_lcalc Expr.typed
in
Cmd.v
(Cmd.info "interpret_lcalc"
~doc:
@ -699,7 +759,8 @@ module Commands = struct
executing the scope specified by the $(b,-s) option assuming no \
additional external inputs.")
Term.(
const interpret_lcalc
const f
$ Cli.Flags.no_typing
$ Cli.Flags.Global.options
$ Cli.Flags.include_dirs
$ Cli.Flags.optimize
@ -718,7 +779,7 @@ module Commands = struct
closure_conversion =
let prg, _, type_ordering =
Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion
~avoid_exceptions ~closure_conversion ~typed:Expr.typed
in
let output_file, with_output =
get_output_format options ~ext:".ml" output

4
compiler/driver.mli
View File

@ -44,7 +44,8 @@ module Passes : sig
includes:Cli.raw_file list ->
optimize:bool ->
check_invariants:bool ->
Shared_ast.typed Dcalc.Ast.program
typed:'m Shared_ast.mark ->
'm Dcalc.Ast.program
* Desugared.Name_resolution.context
* Scopelang.Dependency.TVertex.t list
@ -53,6 +54,7 @@ module Passes : sig
includes:Cli.raw_file list ->
optimize:bool ->
check_invariants:bool ->
typed:'m Shared_ast.mark ->
avoid_exceptions:bool ->
closure_conversion:bool ->
Shared_ast.untyped Lcalc.Ast.program

2
compiler/lcalc/ast.ml
View File

@ -122,5 +122,5 @@ module OptionMonad = struct
]
in
if toplevel then Expr.ematch ~e:arg ~name:Expr.option_enum ~cases mark
else return ~mark (Expr.ematch ~e:arg ~name:Expr.option_enum ~cases mark)
else Expr.ematch ~e:arg ~name:Expr.option_enum ~cases mark
end

122
compiler/lcalc/closure_conversion.ml
View File

@ -22,7 +22,7 @@ module D = Dcalc.Ast
type 'm ctx = {
decl_ctx : decl_ctx;
name_context : string;
globally_bound_vars : 'm expr Var.Set.t;
globally_bound_vars : ('m expr, typ) Var.Map.t;
}
let tys_as_tanys tys = List.map (fun x -> Mark.map (fun _ -> TAny) x) tys
@ -44,10 +44,38 @@ let rec transform_closures_expr :
Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union
~f:(transform_closures_expr ctx)
e
| EVar v ->
( (if Var.Set.mem v ctx.globally_bound_vars then Var.Set.empty
else Var.Set.singleton v),
(Bindlib.box_var v, m) )
| EVar v -> (
match Var.Map.find_opt v ctx.globally_bound_vars with
| None -> Var.Set.singleton v, (Bindlib.box_var v, m)
| Some (TArrow (targs, tret), _) ->
(* Here we eta-expand the argument to make sure function pointers are
correctly casted as closures *)
let args = Array.init (List.length targs) (fun _ -> Var.make "eta_arg") in
let arg_vars =
List.map2
(fun v ty -> Expr.evar v (Expr.with_ty m ty))
(Array.to_list args) targs
in
let e =
Expr.eabs
(Expr.bind args
(Expr.eapp (Expr.rebox e) arg_vars (Expr.with_ty m tret)))
targs m
in
let boxed =
let ctx =
(* We hide the type of the toplevel definition so that the function
doesn't loop *)
{
ctx with
globally_bound_vars =
Var.Map.add v (TAny, Pos.no_pos) ctx.globally_bound_vars;
}
in
Bindlib.box_apply (transform_closures_expr ctx) (Expr.Box.lift e)
in
Bindlib.unbox boxed
| Some _ -> Var.Set.empty, (Bindlib.box_var v, m))
| EMatch { e; cases; name } ->
let free_vars, new_e = (transform_closures_expr ctx) e in
(* We do not close the clotures inside the arms of the match expression,
@ -59,6 +87,11 @@ let rec transform_closures_expr :
| EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in
let new_free_vars, new_body = (transform_closures_expr ctx) body in
let new_free_vars =
Array.fold_left
(fun acc v -> Var.Set.remove v acc)
new_free_vars vars
in
let new_binder = Expr.bind vars new_body in
( Var.Set.union free_vars
(Var.Set.diff new_free_vars
@ -75,6 +108,9 @@ let rec transform_closures_expr :
(* let-binding, we should not close these *)
let vars, body = Bindlib.unmbind binder in
let free_vars, new_body = (transform_closures_expr ctx) body in
let free_vars =
Array.fold_left (fun acc v -> Var.Set.remove v acc) free_vars vars
in
let new_binder = Expr.bind vars new_body in
let free_vars, new_args =
List.fold_right
@ -195,11 +231,17 @@ let rec transform_closures_expr :
Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union
~f:(transform_closures_expr ctx)
e
| EApp { f = EVar v, _; _ } when Var.Set.mem v ctx.globally_bound_vars ->
(* This corresponds to a scope call, which we don't want to transform*)
Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union
~f:(transform_closures_expr ctx)
e
| EApp { f = EVar v, f_m; args } when Var.Map.mem v ctx.globally_bound_vars ->
(* This corresponds to a scope or toplevel function call, which we don't
want to transform*)
let free_vars, new_args =
List.fold_right
(fun arg (free_vars, 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.evar v f_m) new_args m
| EApp { f = e1; args } ->
let free_vars, new_e1 = (transform_closures_expr ctx) e1 in
let code_env_var = Var.make "code_and_env" in
@ -286,12 +328,33 @@ let transform_closures_program (p : 'm program) : 'm program Bindlib.box =
let new_scope_body_expr =
Bindlib.bind_var scope_input_var new_scope_lets
in
( Var.Set.add var toplevel_vars,
let ty =
let pos = Mark.get (ScopeName.get_info name) in
( TArrow
( [TStruct body.scope_body_input_struct, pos],
(TStruct body.scope_body_output_struct, pos) ),
pos )
in
( Var.Map.add var ty toplevel_vars,
Bindlib.box_apply
(fun scope_body_expr ->
ScopeDef (name, { body with scope_body_expr }))
new_scope_body_expr )
| Topdef (name, ty, (EAbs { binder; tys }, m)) ->
let v, expr = Bindlib.unmbind binder in
let ctx =
{
decl_ctx = p.decl_ctx;
name_context = Mark.remove (TopdefName.get_info name);
globally_bound_vars = toplevel_vars;
}
in
let _free_vars, new_expr = transform_closures_expr ctx expr in
let new_binder = Expr.bind v new_expr in
( Var.Map.add var ty toplevel_vars,
Bindlib.box_apply
(fun e -> Topdef (name, ty, e))
(Expr.Box.lift (Expr.eabs new_binder tys m)) )
| Topdef (name, ty, expr) ->
let ctx =
{
@ -301,12 +364,12 @@ let transform_closures_program (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,
( Var.Map.add var ty toplevel_vars,
Bindlib.box_apply
(fun e -> Topdef (name, ty, e))
(fun e -> Topdef (name, (TAny, Mark.get ty), e))
(Expr.Box.lift new_expr) ))
~varf:(fun v -> v)
Var.Set.empty p.code_items
Var.Map.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.
@ -326,7 +389,7 @@ let transform_closures_program (p : 'm program) : 'm program Bindlib.box =
match Mark.remove t with
| TArrow _ -> true
| TAny -> true
| TOption t' -> type_contains_arrow t'
| TDefault t' | TOption t' -> type_contains_arrow t'
| TClosureEnv | TLit _ -> false
| TArray ts -> type_contains_arrow ts
| TTuple ts -> List.exists type_contains_arrow ts
@ -342,18 +405,27 @@ let transform_closures_program (p : 'm program) : 'm program Bindlib.box =
let replace_fun_typs t =
if type_contains_arrow t then Mark.copy t TAny else t
in
let rec convert_ctx ctx =
{
p.decl_ctx with
ctx_struct_fields = ctx.ctx_struct_fields;
ctx_modules = ModuleName.Map.map convert_ctx ctx.ctx_modules;
ctx_structs =
StructName.Map.map
(StructField.Map.map replace_fun_typs)
p.decl_ctx.ctx_structs;
ctx.ctx_structs;
ctx_enums =
EnumName.Map.map
(EnumConstructor.Map.map replace_fun_typs)
p.decl_ctx.ctx_enums;
ctx.ctx_enums;
ctx_scopes = ctx.ctx_scopes;
ctx_topdefs = ctx.ctx_topdefs;
(* Toplevel definitions may not contain scope calls or take functions as
arguments at the moment, which ensures that their interfaces aren't
changed by the conversion *)
}
in
convert_ctx p.decl_ctx
in
Bindlib.box_apply
(fun new_code_items ->
{
@ -528,13 +600,23 @@ let rec hoist_closures_code_item_list
(fun scope_body_expr ->
ScopeDef (name, { body with scope_body_expr }))
new_scope_body_expr )
| Topdef (name, ty, (EAbs { binder; tys }, m)) ->
let v, expr = Bindlib.unmbind binder in
let new_hoisted_closures, new_expr =
hoist_closures_expr (Mark.remove (TopdefName.get_info name)) expr
in
let new_binder = Expr.bind v new_expr in
( new_hoisted_closures,
Bindlib.box_apply
(fun e -> Topdef (name, ty, e))
(Expr.Box.lift (Expr.eabs new_binder tys m)) )
| 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))
(fun e -> Topdef (name, (TAny, Mark.get ty), e))
(Expr.Box.lift new_expr) )
in
let next_code_items = hoist_closures_code_item_list next_code_items in

15
compiler/lcalc/compile_with_exceptions.ml
View File

@ -19,12 +19,6 @@ open Shared_ast
module D = Dcalc.Ast
module A = Ast
let thunk_expr (type m) (e : m A.expr boxed) : m A.expr boxed =
let dummy_var = Var.make "_" in
let pos = Expr.pos e in
let arg_t = Mark.add pos (TLit TUnit) in
Expr.make_abs [| dummy_var |] e [arg_t] pos
let translate_var : 'm D.expr Var.t -> 'm A.expr Var.t = Var.translate
let rec translate_default
@ -33,7 +27,9 @@ let rec translate_default
(cons : 'm D.expr)
(mark_default : 'm mark) : 'm A.expr boxed =
let exceptions =
List.map (fun except -> thunk_expr (translate_expr except)) exceptions
List.map
(fun except -> Expr.thunk_term (translate_expr except) (Mark.get except))
exceptions
in
let pos = Expr.mark_pos mark_default in
let exceptions =
@ -43,8 +39,8 @@ let rec translate_default
(Expr.no_mark mark_default))
[
Expr.earray exceptions mark_default;
thunk_expr (translate_expr just);
thunk_expr (translate_expr cons);
Expr.thunk_term (translate_expr just) (Mark.get just);
Expr.thunk_term (translate_expr cons) (Mark.get cons);
]
pos
in
@ -60,6 +56,7 @@ and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
m
| EDefault { excepts; just; cons } ->
translate_default excepts just cons (Mark.get e)
| EPureDefault e -> translate_expr e
| EOp { op; tys } -> Expr.eop (Operator.translate op) tys m
| ( ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EAbs _ | EIfThenElse _
| ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _

841
compiler/lcalc/compile_without_exceptions.ml
View File

@ -1,6 +1,6 @@
(* 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>
and social benefits computation rules. Copyright (C) 2020 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
@ -15,758 +15,149 @@
the License. *)
open Catala_utils
open Shared_ast
module D = Dcalc.Ast
module A = Ast
(** 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].
(** We make use of the strong invriants on the structure of programs:
Defaultable values can only appear in certin positions. This information is
given by the type structure of expressions. In particular this mean we don't
need to use the monadic bind while computing arithmetic opertions or
function calls. The resulting function is not more difficult than what we
had when translating without exceptions.
When doing this naively, this requires to add matches and [Some] constructor
everywhere. We apply optimizations to remove the additional constructors.
The typing translation is to simply trnsform defult type into option types. *)
The compilation process is handled by the [trans_expr] function. *)
open Shared_ast
(** Start of the translation *)
(** {2 Type translating functions}
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. *)
(** In the general case, we use the [trans_typ_to_any] function to put [TAny]
and then ask the typing algorithm to reinfer all the types. However, this is
not sufficient as the typing inference need at least input and output types.
Those a generated using the [trans_typ_keep] function, that build [TOption]s
where needed. *)
let trans_typ_to_any (tau : typ) : typ = Mark.copy tau TAny
let rec trans_typ_keep (tau : typ) : typ =
let m = Mark.get tau in
let rec translate_typ (tau : typ) : typ =
Mark.copy tau
begin
match Mark.remove tau with
| TDefault t -> TOption (translate_typ t)
| TLit l -> TLit l
| TTuple ts -> TTuple (List.map trans_typ_keep ts)
| TTuple ts -> TTuple (List.map translate_typ ts)
| TStruct s -> TStruct s
| TEnum en -> TEnum en
| TOption _ | TClosureEnv ->
| TOption _ ->
Message.raise_internal_error
"The types option and closure_env should not appear before the dcalc \
-> lcalc translation step."
"The types option should not appear before the dcalc -> lcalc \
translation step."
| TClosureEnv ->
Message.raise_internal_error
"The types 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 *)
| TArrow ([(TLit TUnit, _)], t2) -> Mark.remove (trans_typ_keep t2)
| TArrow (t1, t2) ->
TArrow (List.map trans_typ_keep t1, (TOption (trans_typ_keep t2), m))
| TArray ts -> TArray (translate_typ ts)
| TArrow (t1, t2) -> TArrow (List.map translate_typ t1, translate_typ t2)
end
let trans_typ_keep (tau : typ) : typ =
Mark.copy tau (TOption (trans_typ_keep tau))
let trans_op : dcalc Op.t -> lcalc Op.t = Operator.translate
type 'm var_ctx = { info_pure : bool; is_scope : bool; var : 'm Ast.expr Var.t }
type 'm ctx = {
ctx_vars : ((dcalc, 'm) gexpr, 'm var_ctx) Var.Map.t;
ctx_context_name : string;
}
let trans_var (ctx : 'm ctx) (x : 'm D.expr Var.t) : 'm Ast.expr Var.t =
(Var.Map.find x ctx.ctx_vars).var
(** TODO: give better names to variables *)
(** The function [e' = trans ctx e] actually does the translation between
[D.expr] and [L.expr]. The context links every free variables of the [e]
expression to a new lcalc variable [var], and some information [info_pure]
on whenever the variable can be reduced to an [EmptyError], and hence should
be matched. We also keep [is_scope] to indicate if a variable comes from a
top-level scope definition. This is used when applying functions as
described below. Finally, the following invariant is upheld: if [e] is of
type [a], then the result should be of type [trans_typ_keep a]. For
literals, this mean that a expression of type [money] will be of type
[money option]. We rely on later optimization to shorten the size of the
generated code. *)
let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
=
let m = Mark.get e in
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
Ast.OptionMonad.return (Expr.evar (trans_var ctx x) m) ~mark
else Expr.evar (trans_var ctx x) m
| EExternal _ as e -> Expr.map ~f:(trans ctx) (e, m)
| EApp { f = EVar v, _; args = [(ELit LUnit, _)] } ->
(* Invariant: as users cannot write thunks, it can only come from prior
compilation passes. Hence we can safely remove those. *)
assert (not (Var.Map.find v ctx.ctx_vars).info_pure);
Expr.evar (trans_var ctx v) m
| EAbs { binder; tys = [(TLit TUnit, _)] } ->
(* this is to be used with Ast.OptionMonad.bind. *)
let _, body = Bindlib.unmbind binder in
trans ctx body
| EAbs { binder; tys } ->
(* Every function of type [a -> b] is translated to a function of type [a ->
option b] *)
let vars, body = Bindlib.unmbind binder in
let ctx' =
ArrayLabels.fold_right vars ~init:ctx ~f:(fun v ctx ->
{
ctx with
ctx_vars =
Var.Map.add v
{ info_pure = true; is_scope = false; var = Var.translate v }
ctx.ctx_vars;
})
in
let body' = trans ctx' body in
let binder' = Expr.bind (Array.map Var.translate vars) body' in
Ast.OptionMonad.return ~mark (Expr.eabs binder' tys m)
| EDefault { excepts; just; cons } ->
let excepts' = List.map (trans ctx) excepts in
let just' = trans ctx just in
let cons' = trans ctx cons in
(* If the default term has the following type [<es: a list | just: bool |-
cons: a>] then the resulting term will have type [handledefaultOpt (es':
a option list) (just': bool option) (cons': a option)] *)
let m' = match m with Typed m -> Typed { m with ty = TAny, pos } in
let rec translate_default
(exceptions : 'm D.expr list)
(just : 'm D.expr)
(cons : 'm D.expr)
(mark_default : 'm mark) : 'm A.expr boxed =
(* Since the program is well typed, all exceptions have as type [option 't] *)
let exceptions = List.map translate_expr exceptions in
let pos = Expr.mark_pos mark_default in
let exceptions =
Expr.make_app
(Expr.eop Op.HandleDefaultOpt [TAny, pos; TAny, pos; TAny, pos] m')
[Expr.earray excepts' m; Expr.thunk_term just' m; Expr.thunk_term cons' m]
(Expr.eop Op.HandleDefaultOpt
[TAny, pos; TAny, pos; TAny, pos]
(Expr.no_mark mark_default))
[
Expr.earray exceptions mark_default;
(* In call-by-value programming languages, as lcalc, arguments are
evalulated before calling the function. Since we don't want to
execute the justification and conclusion while before checking every
exceptions, we need to thunk them. *)
Expr.thunk_term (translate_expr just) (Mark.get just);
Expr.thunk_term (translate_expr cons) (Mark.get cons);
]
pos
| ELit l -> Ast.OptionMonad.return ~mark (Expr.elit l m)
in
exceptions
and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
let mark = Mark.get e in
match Mark.remove e with
| EEmptyError -> Ast.OptionMonad.empty ~mark
| EErrorOnEmpty arg ->
let arg' = trans ctx arg in
Ast.OptionMonad.error_on_empty arg' ~mark ~toplevel:false
~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
always return (or raise panic exceptions like AssertionFailed,
NoValueProvided or Conflict) a structure that can contain optionnal
elements. Hence, to call a scope, we don't need to use the monad bind. *)
Ast.OptionMonad.return ~mark
(Expr.eapp
(Expr.evar (trans_var ctx scope) mark)
[
Expr.estruct ~name
~fields:(StructField.Map.map (trans ctx) fields)
mark;
]
mark)
| EApp { f = (EVar ff, _) as f; args }
when not (Var.Map.find ff ctx.ctx_vars).is_scope ->
(* INVARIANT: functions are always encoded using this function.
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 (Bindlib.name_of ff) in
Ast.OptionMonad.bind_var ~mark
(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 { 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 (context_or_same_var ctx es) in
Ast.OptionMonad.bind_var ~mark
(Ast.OptionMonad.mbind
~var_name:(context_or_same_var ctx es)
(Expr.evar f_var mark)
(List.map (trans ctx) args)
~mark)
f_var (trans ctx f)
| EApp { f = EAbs { binder; _ }, _; args } ->
(* INVARIANTS: every let have only one argument. (checked by
invariant_let) *)
let var, body = Bindlib.unmbind binder in
let[@warning "-8"] [| var |] = var in
let var' = Var.translate var in
let[@warning "-8"] [arg] = args in
let ctx' =
{
ctx_vars =
Var.Map.add var
{ info_pure = true; is_scope = false; var = var' }
ctx.ctx_vars;
ctx_context_name = Bindlib.name_of var;
}
in
Ast.OptionMonad.bind_var (trans ctx' body) var' (trans ctx arg) ~mark
| EApp { f = EApp { f = EOp { op = Op.Log _; _ }, _; args = _ }, _; _ } ->
Message.raise_internal_error
"Parameter trace is incompatible with parameter avoid_exceptions: some \
tracing logs were added while they are not supported."
(* Encoding of Fold, Filter, Map and Reduce is non trivial because we don't
define new monadic operators for every one of those. *)
| EApp { f = EOp { op = Op.Fold; tys }, opmark; args = [f; init; l] } ->
(* The function f should have type b -> a -> a. Hence, its translation has
type [b] -> [a] -> option [a]. But we need a function of type option [b]
-> option [a] -> option [a] for the type checking of fold. Hence, we
"iota-expand" the function as follows: [λ x y. bindm x y. [f] x y] *)
let x1 = Var.make "f" in
let x2 = Var.make "init" in
let 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:(context_or_same_var ctx f)
~mark
(fun vars ->
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]))
[TAny, pos; TAny, pos]
m))
(trans ctx f)
in
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
| EApp { f = EOp { op = Op.Reduce; tys }, opmark; args = [f; init; l] } ->
let x1 = Var.make "f" in
let x2 = Var.make "init" in
let 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:(context_or_same_var ctx f)
~mark
(fun vars ->
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]))
[TAny, pos; TAny, pos]
m))
(trans ctx f)
in
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
| EApp { f = EOp { op = Op.Map; tys }, opmark; args = [f; l] } ->
(* The funtion [f] has type [a -> option b], but Map needs a function of
type [a -> b], hence we need to transform [f] into a function of type [a
option -> option b]. *)
let x1 = Var.make "f" in
let f' =
Ast.OptionMonad.bind_cont ~mark ~var_name:ctx.ctx_context_name
(fun f ->
Ast.OptionMonad.return ~mark
(Expr.eabs
(Expr.bind [| x1 |]
(Ast.OptionMonad.mbind_cont ~mark
~var_name:ctx.ctx_context_name
(fun vars ->
Expr.eapp (Expr.evar f m)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
m)
[Expr.evar x1 m]))
[TAny, pos]
m))
(trans ctx f)
in
Ast.OptionMonad.mbind_cont
~var_name:(context_or_same_var ctx f)
(fun vars ->
Ast.OptionMonad.return ~mark
(Expr.eapp
(Expr.eop (trans_op Op.Map) tys opmark)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
mark))
[f'; trans ctx l]
~mark
| EApp { f = EOp { op = Op.Filter; tys }, opmark; args = [f; l] } ->
(* The function [f] has type [a -> bool option] while the filter operator
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 (context_or_same_var ctx f) in
let 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:(context_or_same_var ctx f)
(Ast.OptionMonad.mbind_cont ~mark
~var_name:(context_or_same_var ctx f)
(fun vars ->
Expr.eapp (Expr.evar f' m)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
m)
[Expr.evar x1 m])))
[TAny, pos]
m))
(trans ctx f)
in
Ast.OptionMonad.mbind_cont
~var_name:(context_or_same_var ctx f)
(fun vars ->
Ast.OptionMonad.return ~mark
(Expr.eapp
(Expr.eop (trans_op Op.Filter) tys opmark)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
mark))
[f'; trans ctx l]
~mark
| EApp { f = EOp { op = Op.Filter as op; _ }, _; _ }
| EApp { f = EOp { op = Op.Map as op; _ }, _; _ }
| EApp { f = EOp { op = Op.Fold as op; _ }, _; _ }
| EApp { f = EOp { op = Op.Reduce as op; _ }, _; _ } ->
(* Cannot happend: list operator must be fully determined *)
Message.raise_internal_error
"List operator %a was not fully determined: some partial evaluation was \
found while compiling."
(Print.operator ~debug:false)
op
| EApp { f = EOp { op; tys }, opmark; args } ->
let res =
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
in
res
| EMatch { name; e; cases } ->
let cases =
EnumConstructor.Map.map
(fun case ->
match Mark.remove case with
Ast.OptionMonad.error_on_empty ~mark ~var_name:"arg" (translate_expr arg)
| EDefault { excepts; just; cons } ->
translate_default excepts just cons (Mark.get e)
| EPureDefault e -> Ast.OptionMonad.return ~mark (translate_expr e)
(* As we need to translate types as well as terms, we cannot simply use
[Expr.map] for terms that contains types. *)
| EOp { op; tys } ->
Expr.eop (Operator.translate op) (List.map translate_typ tys) mark
| EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in
let ctx' =
ArrayLabels.fold_right vars ~init:ctx ~f:(fun var ctx ->
{
ctx with
ctx_vars =
Var.Map.add var
{
info_pure = true;
is_scope = false;
var = Var.translate var;
}
ctx.ctx_vars;
})
in
let binder =
Expr.bind (Array.map Var.translate vars) (trans ctx' body)
in
Expr.eabs binder tys m
| _ -> assert false)
cases
in
Ast.OptionMonad.bind_cont
~var_name:(context_or_same_var ctx e)
(fun e -> Expr.ematch ~e:(Expr.evar e m) ~name ~cases m)
(trans ctx e) ~mark
| EArray args ->
Ast.OptionMonad.mbind_cont ~mark ~var_name:ctx.ctx_context_name
(fun vars ->
Ast.OptionMonad.return ~mark
(Expr.earray
(List.map
(fun v -> Ast.OptionMonad.return ~mark (Expr.evar v m))
vars)
mark))
(List.map (trans ctx) args)
| EStruct { name; fields } ->
let fields_name, fields = List.split (StructField.Map.bindings fields) in
Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
(fun xs ->
let fields =
ListLabels.fold_right2 fields_name
(List.map
(fun x -> Ast.OptionMonad.return ~mark (Expr.evar x mark))
xs)
~f:StructField.Map.add ~init:StructField.Map.empty
in
Ast.OptionMonad.return ~mark (Expr.estruct ~name ~fields mark))
(List.map (trans ctx) fields)
~mark
| EIfThenElse { cond; etrue; efalse } ->
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:(context_or_same_var ctx e)
(fun e ->
Ast.OptionMonad.return ~mark
(Expr.einj ~e:(Expr.evar e mark) ~cons ~name mark))
(trans ctx e) ~mark
| EStructAccess { name; e; field } ->
Ast.OptionMonad.bind_cont
~var_name:(context_or_same_var ctx e)
(fun e -> Expr.estructaccess ~e:(Expr.evar e mark) ~field ~name mark)
(trans ctx e) ~mark
| ETuple args ->
Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
(fun xs ->
Ast.OptionMonad.return ~mark
(Expr.etuple (List.map (fun x -> Expr.evar x mark) xs) mark))
(List.map (trans ctx) args)
~mark
| ETupleAccess { e; index; size } ->
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:(context_or_same_var ctx e)
(fun e ->
Ast.OptionMonad.return ~mark (Expr.eassert (Expr.evar e mark) mark))
(trans ctx e) ~mark
| EApp _ ->
Message.raise_spanned_error (Expr.pos e)
"Internal Error: found an EApp that does not satisfy the invariants when \
translating Dcalc to Lcalc without exceptions."
(* invalid invariant *)
| EOp _ ->
Message.raise_spanned_error (Expr.pos e)
"Internal Error: found an EOp that does not satisfy the invariants when \
translating Dcalc to Lcalc without exceptions."
| ELocation _ -> .
let body = translate_expr body in
let binder = Expr.bind (Array.map Var.translate vars) body in
let tys = List.map translate_typ tys in
Expr.eabs binder tys mark
| ( ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EIfThenElse _
| ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _
| EStructAccess _ | EMatch _ ) as e ->
Expr.map ~f:translate_expr (Mark.add mark e)
| _ -> .
(** Now we have translated expression, we still need to translate the statements
(scope_let_list) and then scopes. This is pretty much straightforward. *)
let rec trans_scope_let (ctx : typed ctx) (s : typed D.expr scope_let) =
match s with
| {
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = (TArrow ([(TLit TUnit, _)], _), _) as scope_let_typ;
scope_let_expr = EAbs { binder; _ }, _;
scope_let_next;
scope_let_pos;
} ->
(* special case : the subscope variable is thunked (context i/o). We remove
this thunking. *)
let _, scope_let_expr = Bindlib.unmbind binder in
let next_var, next_body = Bindlib.unbind scope_let_next in
let next_var' = Var.translate next_var in
let ctx' =
{
ctx with
ctx_vars =
Var.Map.add next_var
{ info_pure = false; is_scope = false; var = next_var' }
ctx.ctx_vars;
}
in
let next_var = next_var' in
let next_body = trans_scope_body_expr ctx' next_body in
let scope_let_next = Bindlib.bind_var next_var next_body in
let scope_let_expr =
Expr.Box.lift
@@ trans
{ ctx with ctx_context_name = Bindlib.name_of next_var }
scope_let_expr
in
let translate_scope_body_expr (scope_body_expr : 'expr1 scope_body_expr) :
'expr2 scope_body_expr Bindlib.box =
Scope.fold_right_lets
~f:(fun scope_let var_next acc ->
Bindlib.box_apply2
(fun scope_let_expr scope_let_next ->
(fun scope_let_next scope_let_expr ->
ScopeLet
{
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = trans_typ_to_any scope_let_typ;
scope_let_expr;
scope_let with
scope_let_next;
scope_let_pos;
scope_let_expr;
scope_let_typ = translate_typ scope_let.scope_let_typ;
})
scope_let_expr scope_let_next
| {
scope_let_kind = SubScopeVarDefinition;
scope_let_typ;
scope_let_expr = (EAbs _, _) as scope_let_expr;
scope_let_next;
scope_let_pos;
} ->
(* special case : the subscope variable is thunked (context i/o). We remove
this thunking. *)
let next_var, next_body = Bindlib.unbind scope_let_next in
let next_var' = Var.translate next_var in
let ctx' =
{
ctx with
ctx_vars =
Var.Map.add next_var
{ info_pure = false; is_scope = false; var = next_var' }
ctx.ctx_vars;
}
in
let next_var = next_var' in
let next_body = trans_scope_body_expr ctx' next_body in
let scope_let_next = Bindlib.bind_var next_var next_body in
let scope_let_expr =
Expr.Box.lift
@@ trans
{ ctx with ctx_context_name = Bindlib.name_of next_var }
scope_let_expr
in
Bindlib.box_apply2
(fun scope_let_expr scope_let_next ->
{
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = trans_typ_to_any scope_let_typ;
scope_let_expr;
scope_let_next;
scope_let_pos;
})
scope_let_expr scope_let_next
| {
scope_let_kind = SubScopeVarDefinition;
scope_let_typ;
scope_let_expr = EErrorOnEmpty e, mark;
scope_let_next;
scope_let_pos;
} ->
(* special case: regular input to the subscope *)
let next_var, next_body = Bindlib.unbind scope_let_next in
let next_var' = Var.translate next_var in
let ctx' =
{
ctx with
ctx_vars =
Var.Map.add next_var
{ info_pure = true; is_scope = false; var = next_var' }
ctx.ctx_vars;
}
in
let next_var = next_var' in
let next_body = trans_scope_body_expr ctx' next_body in
let scope_let_next = Bindlib.bind_var next_var next_body in
let scope_let_expr =
Expr.Box.lift
@@ Ast.OptionMonad.error_on_empty ~mark ~toplevel:true
~var_name:ctx.ctx_context_name
(trans { ctx with ctx_context_name = Bindlib.name_of next_var } e)
in
Bindlib.box_apply2
(fun scope_let_expr scope_let_next ->
{
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = trans_typ_to_any scope_let_typ;
scope_let_expr;
scope_let_next;
scope_let_pos;
})
scope_let_expr scope_let_next
| { scope_let_kind = SubScopeVarDefinition; scope_let_pos = pos; _ } ->
Message.raise_spanned_error pos
"Internal Error: found an SubScopeVarDefinition that does not satisfy \
the invariants when translating Dcalc to Lcalc without exceptions."
| {
scope_let_kind;
scope_let_typ;
scope_let_expr;
scope_let_next;
scope_let_pos;
} ->
(* base case *)
let next_var, next_body = Bindlib.unbind scope_let_next in
let next_var' = Var.translate next_var in
let ctx' =
{
ctx with
ctx_vars =
Var.Map.add next_var
(match scope_let_kind with
| DestructuringInputStruct -> (
(* note for future: we keep this useless match for distinguishing
further optimization while building the terms. *)
match Mark.remove scope_let_typ with
| TArrow ([(TLit TUnit, _)], _) ->
{ info_pure = false; is_scope = false; var = next_var' }
| _ -> { info_pure = false; is_scope = false; var = next_var' })
| ScopeVarDefinition | SubScopeVarDefinition | CallingSubScope
| DestructuringSubScopeResults | Assertion ->
{ info_pure = false; is_scope = false; var = next_var' })
ctx.ctx_vars;
}
in
let next_var = next_var' in
let next_body = trans_scope_body_expr ctx' next_body in
let scope_let_next = Bindlib.bind_var next_var next_body in
let scope_let_expr =
Expr.Box.lift
@@ trans
{ ctx with ctx_context_name = Bindlib.name_of next_var }
scope_let_expr
in
Bindlib.box_apply2
(fun scope_let_expr scope_let_next ->
{
scope_let_kind;
scope_let_typ = trans_typ_to_any scope_let_typ;
scope_let_expr;
scope_let_next;
scope_let_pos;
})
scope_let_expr scope_let_next
and trans_scope_body_expr ctx s :
(lcalc, typed) gexpr scope_body_expr Bindlib.box =
match s with
| Result e -> begin
(* invariant : result is always in the form of a record. *)
match Mark.remove e with
| EStruct { name; fields } ->
(Bindlib.bind_var (Var.translate var_next) acc)
(Expr.Box.lift (translate_expr scope_let.scope_let_expr)))
~init:(fun res ->
Bindlib.box_apply
(fun e -> Result e)
(Expr.Box.lift
@@ Expr.estruct ~name
~fields:(StructField.Map.map (trans ctx) fields)
(Mark.get e))
| _ -> assert false
end
| ScopeLet s ->
Bindlib.box_apply (fun s -> ScopeLet s) (trans_scope_let ctx s)
(fun res -> Result res)
(Expr.Box.lift (translate_expr res)))
scope_body_expr
let trans_scope_body
(ctx : typed ctx)
({ scope_body_input_struct; scope_body_output_struct; scope_body_expr } :
typed D.expr scope_body) =
let var, body = Bindlib.unbind scope_body_expr in
let body =
trans_scope_body_expr
{
ctx_vars =
Var.Map.add var
{ info_pure = true; is_scope = false; var = Var.translate var }
ctx.ctx_vars;
ctx_context_name = Bindlib.name_of var;
}
body
in
let binder = Bindlib.bind_var (Var.translate var) body in
Bindlib.box_apply
(fun scope_body_expr ->
{ scope_body_input_struct; scope_body_output_struct; scope_body_expr })
binder
let rec trans_code_items (ctx : typed ctx) (c : typed D.expr code_item_list) :
(lcalc, typed) gexpr code_item_list Bindlib.box =
match c with
| Nil -> Bindlib.box Nil
| Cons (c, next) -> (
let var, next = Bindlib.unbind next in
match c with
| Topdef (name, typ, e) ->
let next =
Bindlib.bind_var (Var.translate var)
(trans_code_items
{
ctx_vars =
Var.Map.add var
{
info_pure = false;
is_scope = false;
var = Var.translate var;
}
ctx.ctx_vars;
ctx_context_name = fst (TopdefName.get_info name);
}
next)
in
let e = Expr.Box.lift @@ trans ctx e in
(* Invariant: We suppose there are no defaults in toplevel definitions,
hence we don't need to add an error_on_empty *)
Bindlib.box_apply2
(fun next e -> Cons (Topdef (name, trans_typ_to_any typ, e), next))
next e
let translate_code_items scopes =
let f = function
| ScopeDef (name, body) ->
let next =
Bindlib.bind_var (Var.translate var)
(trans_code_items
{
ctx_vars =
Var.Map.add var
{
info_pure = true;
is_scope = true;
var = Var.translate var;
}
ctx.ctx_vars;
ctx_context_name = fst (ScopeName.get_info name);
}
next)
let scope_input_var, scope_lets = Bindlib.unbind body.scope_body_expr in
let new_body_expr = translate_scope_body_expr scope_lets in
let new_body_expr =
Bindlib.bind_var (Var.translate scope_input_var) new_body_expr
in
let body = trans_scope_body ctx body in
Bindlib.box_apply2
(fun next body -> Cons (ScopeDef (name, body), next))
next body)
Bindlib.box_apply
(fun scope_body_expr -> ScopeDef (name, { body with scope_body_expr }))
new_body_expr
| Topdef (name, typ, expr) ->
Bindlib.box_apply
(fun e -> Topdef (name, typ, e))
(Expr.Box.lift (translate_expr expr))
in
Scope.map ~f ~varf:Var.translate scopes
let translate_program (prgm : typed D.program) : untyped A.program =
let decl_ctx =
let translate_program (prg : typed D.program) : untyped A.program =
Program.untype
@@ Bindlib.unbox
@@ Bindlib.box_apply
(fun code_items ->
let ctx_enums =
EnumName.Map.map
(EnumConstructor.Map.map translate_typ)
prg.decl_ctx.ctx_enums
in
let ctx_structs =
StructName.Map.map
(StructField.Map.map translate_typ)
prg.decl_ctx.ctx_structs
in
{
prgm.decl_ctx with
ctx_enums =
prgm.decl_ctx.ctx_enums
|> EnumName.Map.add Expr.option_enum Expr.option_enum_config;
}
in
let decl_ctx =
{
decl_ctx with
ctx_structs =
prgm.decl_ctx.ctx_structs
|> StructName.Map.mapi (fun _n str ->
StructField.Map.map trans_typ_keep str);
}
in
let code_items =
trans_code_items
{ ctx_vars = Var.Map.empty; ctx_context_name = "" }
prgm.code_items
in
Expr.Box.assert_closed code_items;
(* program is closed here. *)
let code_items = Bindlib.unbox code_items in
Program.untype { prgm with decl_ctx; code_items }
prg with
code_items;
decl_ctx = { prg.decl_ctx with ctx_enums; ctx_structs };
})
(translate_code_items prg.code_items)

5
compiler/lcalc/to_ocaml.ml
View File

@ -200,8 +200,9 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit =
ts
| TStruct s -> Format.fprintf fmt "%a.t" format_to_module_name (`Sname s)
| TOption t ->
Format.fprintf fmt "@[<hov 2>(%a)@] %a" format_typ_with_parens t
format_enum_name Expr.option_enum
Format.fprintf fmt "@[<hov 2>(%a)@] %a.t" format_typ_with_parens t
format_to_module_name (`Ename Expr.option_enum)
| TDefault t -> format_typ fmt t
| TEnum e -> Format.fprintf fmt "%a.t" format_to_module_name (`Ename e)
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a@]"

4
compiler/plugins/api_web.ml
View File

@ -67,6 +67,7 @@ module To_jsoo = struct
| TOption t ->
Format.fprintf fmt "@[<hov 2>(%a)@] %a" format_typ_with_parens t
format_enum_name Expr.option_enum
| TDefault t -> format_typ fmt t
| TEnum e -> Format.fprintf fmt "%a Js.t" format_enum_name e
| TArray t1 ->
Format.fprintf fmt "@[%a@ Js.js_array Js.t@]" format_typ_with_parens t1
@ -92,6 +93,7 @@ module To_jsoo = struct
| TArray t ->
Format.fprintf fmt "Js.array %@%@ Array.map (fun x -> %a x)"
format_typ_to_jsoo t
| TDefault t -> format_typ_to_jsoo fmt t
| TAny | TTuple _ -> Format.fprintf fmt "Js.Unsafe.inject"
| _ -> Format.fprintf fmt ""
@ -439,7 +441,7 @@ let run
Message.raise_error "This plugin requires the --trace flag.";
let prg, _, type_ordering =
Driver.Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion
~avoid_exceptions ~closure_conversion ~typed:Expr.typed
in
let modname =
(* TODO: module directive support *)

3
compiler/plugins/explain.ml
View File

@ -389,6 +389,7 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
((None, Expr.mark_pos m)
:: List.map (fun (e, _) -> None, Expr.pos e) excs)
"Conflicting exceptions")
| EPureDefault e, _ -> lazy_eval ctx env llevel e
| EIfThenElse { cond; etrue; efalse }, _ -> (
match eval_to_value env cond with
| (ELit (LBool true), _), _ ->
@ -1388,7 +1389,7 @@ let options =
let run includes optimize ex_scope explain_options global_options =
let prg, ctx, _ =
Driver.Passes.dcalc global_options ~includes ~optimize
~check_invariants:false
~check_invariants:false ~typed:Expr.typed
in
Interpreter.load_runtime_modules prg;
let scope = Driver.Commands.get_scope_uid ctx ex_scope in

2
compiler/plugins/json_schema.ml
View File

@ -216,7 +216,7 @@ let run
options =
let prg, ctx, _ =
Driver.Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion
~avoid_exceptions ~closure_conversion ~typed:Expr.typed
in
let output_file, with_output =
Driver.Commands.get_output_format options ~ext:"_schema.json" output

2
compiler/plugins/lazy_interp.ml
View File

@ -194,6 +194,7 @@ let rec lazy_eval :
((None, Expr.mark_pos m)
:: List.map (fun (e, _) -> None, Expr.pos e) excs)
"Conflicting exceptions")
| EPureDefault e, _ -> lazy_eval ctx env llevel e
| EIfThenElse { cond; etrue; efalse }, _ -> (
match eval_to_value env cond with
| (ELit (LBool true), _), _ -> lazy_eval ctx env llevel etrue
@ -260,6 +261,7 @@ let interpret_program (prg : ('dcalc, 'm) gexpr program) (scope : ScopeName.t) :
let run includes optimize check_invariants ex_scope options =
let prg, ctx, _ =
Driver.Passes.dcalc options ~includes ~optimize ~check_invariants
~typed:Expr.typed
in
Interpreter.load_runtime_modules prg;
let scope = Driver.Commands.get_scope_uid ctx ex_scope in

1
compiler/scalc/to_python.ml
View File

@ -176,6 +176,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit =
| TOption some_typ ->
(* We translate the option type with an overloading by Python's [None] *)
Format.fprintf fmt "Optional[%a]" format_typ some_typ
| TDefault t -> format_typ fmt t
| TEnum e -> Format.fprintf fmt "%a" format_enum_name e
| TArrow (t1, t2) ->
Format.fprintf fmt "Callable[[%a], %a]"

2
compiler/scalc/to_r.ml
View File

@ -172,7 +172,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit =
format_typ)
ts
| TStruct s -> Format.fprintf fmt "\"catala_struct_%a\"" format_struct_name s
| TOption some_typ ->
| TOption some_typ | TDefault some_typ ->
(* We loose track of optional value as they're crammed into NULL *)
format_typ fmt some_typ
| TEnum e -> Format.fprintf fmt "\"catala_enum_%a\"" format_enum_name e

21
compiler/scopelang/ast.ml
View File

@ -43,9 +43,15 @@ type 'm rule =
| Assertion of 'm expr
| Call of ScopeName.t * SubScopeName.t * 'm mark
type scope_var_ty = {
svar_in_ty : typ;
svar_out_ty : typ;
svar_io : Desugared.Ast.io;
}
type 'm scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : (typ * Desugared.Ast.io) ScopeVar.Map.t;
scope_sig : scope_var_ty ScopeVar.Map.t;
scope_decl_rules : 'm rule list;
scope_options : Desugared.Ast.catala_option Mark.pos list;
}
@ -84,8 +90,14 @@ let type_program (prg : 'm program) : typed program =
let env =
ScopeName.Map.fold
(fun scope_name scope_decl env ->
let vars = ScopeVar.Map.map fst (Mark.remove scope_decl).scope_sig in
Typing.Env.add_scope scope_name ~vars env)
let sg = (Mark.remove scope_decl).scope_sig in
let vars =
ScopeVar.Map.map (fun { svar_out_ty; _ } -> svar_out_ty) sg
in
let in_vars =
ScopeVar.Map.map (fun { svar_in_ty; _ } -> svar_in_ty) sg
in
Typing.Env.add_scope scope_name ~vars ~in_vars env)
prg.program_scopes env
in
env
@ -115,7 +127,8 @@ let type_program (prg : 'm program) : typed program =
(Mark.map (fun scope_decl ->
let env =
ScopeVar.Map.fold
(fun svar (typ, _) env -> Typing.Env.add_scope_var svar typ env)
(fun svar { svar_out_ty; _ } env ->
Typing.Env.add_scope_var svar svar_out_ty env)
scope_decl.scope_sig env
in
let scope_decl_rules =

8
compiler/scopelang/ast.mli
View File

@ -36,9 +36,15 @@ type 'm rule =
| Assertion of 'm expr
| Call of ScopeName.t * SubScopeName.t * 'm mark
type scope_var_ty = {
svar_in_ty : typ;
svar_out_ty : typ;
svar_io : Desugared.Ast.io;
}
type 'm scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : (typ * Desugared.Ast.io) ScopeVar.Map.t;
scope_sig : scope_var_ty ScopeVar.Map.t;
scope_decl_rules : 'm rule list;
scope_options : Desugared.Ast.catala_option Mark.pos list;
}

2
compiler/scopelang/dependency.ml
View File

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

149
compiler/scopelang/from_desugared.ml
View File

@ -29,6 +29,7 @@ type target_scope_vars =
type ctx = {
decl_ctx : decl_ctx;
scope_var_mapping : target_scope_vars ScopeVar.Map.t;
reentrant_vars : typ ScopeVar.Map.t;
var_mapping : (D.expr, untyped Ast.expr Var.t) Var.Map.t;
modules : ctx ModuleName.Map.t;
}
@ -131,7 +132,27 @@ let rec translate_expr (ctx : ctx) (e : D.expr) : untyped Ast.expr boxed =
v'
| States [] -> assert false
in
ScopeVar.Map.add v' (translate_expr ctx e) args')
let e' = translate_expr ctx e in
let m = Mark.get e in
let e' =
match ScopeVar.Map.find_opt v ctx.reentrant_vars with
| Some (TArrow (targs, _), _) ->
(* Functions are treated specially: the default only applies to
their return type *)
let arg = Var.make "arg" in
let pos = Expr.mark_pos m in
Expr.make_abs [| arg |]
(Expr.edefault ~excepts:[] ~just:(Expr.elit (LBool true) m)
~cons:
(Expr.epuredefault
(Expr.make_app e' [Expr.evar arg m] pos)
m)
m)
targs pos
| Some _ -> Expr.epuredefault e' m
| None -> e'
in
ScopeVar.Map.add v' e' args')
args ScopeVar.Map.empty)
m
| EApp { f = EOp { op; tys }, m1; args } ->
@ -148,8 +169,8 @@ let rec translate_expr (ctx : ctx) (e : D.expr) : untyped Ast.expr boxed =
Expr.eapp (Expr.eop op (List.rev tys) m1) (List.rev args) m)
| EOp _ -> assert false (* Only allowed within [EApp] *)
| ( EStruct _ | ETuple _ | ETupleAccess _ | EInj _ | EMatch _ | ELit _
| EApp _ | EDefault _ | EIfThenElse _ | EArray _ | EEmptyError
| EErrorOnEmpty _ ) as e ->
| EApp _ | EDefault _ | EPureDefault _ | EIfThenElse _ | EArray _
| EEmptyError | EErrorOnEmpty _ ) as e ->
Expr.map ~f:(translate_expr ctx) (e, m)
(** {1 Rule tree construction} *)
@ -333,6 +354,7 @@ let def_map_to_tree
let rec rule_tree_to_expr
~(toplevel : bool)
~(is_reentrant_var : bool)
~(subscope : bool)
(ctx : ctx)
(def_pos : Pos.t)
(params : D.expr Var.t list option)
@ -397,29 +419,48 @@ let rec rule_tree_to_expr
list
in
let default_containing_base_cases =
Expr.make_default
(List.map2
(fun base_just base_cons ->
Expr.make_default []
(* Here we insert the logging command that records when a decision
is taken for the value of a variable. *)
(tag_with_log_entry base_just PosRecordIfTrueBool [])
base_cons emark)
Expr.edefault
~excepts:
(List.fold_right2
(fun base_just base_cons acc ->
match Expr.unbox base_just with
| ELit (LBool false), _ -> acc
| _ ->
Expr.edefault
~excepts:[]
(* Here we insert the logging command that records when a
decision is taken for the value of a variable. *)
~just:(tag_with_log_entry base_just PosRecordIfTrueBool [])
~cons:(Expr.epuredefault base_cons emark)
emark
:: acc)
(translate_and_unbox_list base_just_list)
(translate_and_unbox_list base_cons_list))
(Expr.elit (LBool false) emark)
(Expr.eemptyerror emark) emark
(translate_and_unbox_list base_cons_list)
[])
~just:(Expr.elit (LBool false) emark)
~cons:(Expr.eemptyerror emark) emark
in
let exceptions =
List.map
(rule_tree_to_expr ~toplevel:false ~is_reentrant_var ctx def_pos params)
(rule_tree_to_expr ~toplevel:false ~is_reentrant_var ~subscope ctx def_pos
params)
exceptions
in
let default =
Expr.make_default exceptions
(Expr.elit (LBool true) emark)
if exceptions = [] then default_containing_base_cases
else
Expr.edefault ~excepts:exceptions
~just:(Expr.elit (LBool true) emark)
~cons:
(* if toplevel then Expr.eerroronempty default_containing_base_cases emark
* else *)
default_containing_base_cases emark
in
let default =
if toplevel && not (subscope && is_reentrant_var) then
Expr.eerroronempty default emark
else default
in
match params, (List.hd base_rules).D.rule_parameter with
| None, None -> default
| Some new_params, Some (ls, _) ->
@ -430,10 +471,6 @@ let rec rule_tree_to_expr
dealing with a context variable which is reentrant (either in the
caller or callee). In this case the ErrorOnEmpty will be added later in
the scopelang->dcalc translation. *)
let default =
if is_reentrant_var then default else Expr.eerroronempty default emark
in
Expr.make_abs
(new_params
|> List.map (fun x -> Var.Map.find x ctx.var_mapping)
@ -510,7 +547,8 @@ let translate_def
empty_error tys (Expr.mark_pos m)
| _ -> empty_error
else
rule_tree_to_expr ~toplevel:true ~is_reentrant_var:is_reentrant ctx
rule_tree_to_expr ~toplevel:true ~is_reentrant_var:is_reentrant
~subscope:is_subscope_var ctx
(D.ScopeDef.get_position def_info)
(Option.map
(fun (ps, _) ->
@ -620,6 +658,9 @@ let translate_rule
(D.ScopeDef.Map.find def_key exc_graphs)
~is_cond ~is_subscope_var:true
in
let def_typ =
Scope.input_type def_typ scope_def.D.scope_def_io.D.io_input
in
let subscop_real_name =
SubScopeName.Map.find sub_scope_index scope.scope_sub_scopes
in
@ -666,18 +707,27 @@ let translate_scope_interface ctx scope =
let scope_sig =
ScopeVar.Map.fold
(fun var (states : D.var_or_states) acc ->
let get_svar scope_def =
let svar_in_ty =
Scope.input_type scope_def.D.scope_def_typ
scope_def.D.scope_def_io.io_input
in
{
Ast.svar_in_ty;
svar_out_ty = scope_def.D.scope_def_typ;
svar_io = scope_def.scope_def_io;
}
in
match states with
| WholeVar ->
let scope_def =
D.ScopeDef.Map.find (D.ScopeDef.Var (var, None)) scope.D.scope_defs
in
let typ = scope_def.scope_def_typ in
ScopeVar.Map.add
(match ScopeVar.Map.find var ctx.scope_var_mapping with
| WholeVar v -> v
| States _ -> failwith "should not happen")
(typ, scope_def.scope_def_io)
acc
(get_svar scope_def) acc
| States states ->
(* What happens in the case of variables with multiple states is
interesting. We need to create as many Var entries in the scope
@ -693,8 +743,7 @@ let translate_scope_interface ctx scope =
(match ScopeVar.Map.find var ctx.scope_var_mapping with
| WholeVar _ -> failwith "should not happen"
| States states' -> List.assoc state states')
(scope_def.scope_def_typ, scope_def.scope_def_io)
acc)
(get_svar scope_def) acc)
acc states)
scope.scope_vars ScopeVar.Map.empty
in
@ -760,16 +809,43 @@ let translate_program
in
States (List.map (fun state -> state, state_var state) states)
in
let reentrant =
let state =
match states with
| D.WholeVar -> None
| States (s :: _) -> Some s
| States [] -> assert false
in
match
D.ScopeDef.Map.find_opt
(Var (scope_var, state))
scope_decl.D.scope_defs
with
| Some
{
scope_def_io = { io_input = Runtime.Reentrant, _; _ };
scope_def_typ;
_;
} ->
Some scope_def_typ
| _ -> None
in
{
ctx with
scope_var_mapping =
ScopeVar.Map.add scope_var new_var ctx.scope_var_mapping;
reentrant_vars =
Option.fold reentrant
~some:(fun ty ->
ScopeVar.Map.add scope_var ty ctx.reentrant_vars)
~none:ctx.reentrant_vars;
})
scope_decl.D.scope_vars ctx)
desugared.D.program_scopes
{
scope_var_mapping = ScopeVar.Map.empty;
var_mapping = Var.Map.empty;
reentrant_vars = ScopeVar.Map.empty;
decl_ctx = desugared.program_ctx;
modules;
}
@ -777,16 +853,21 @@ let translate_program
let ctx = make_ctx desugared in
let rec gather_scope_vars acc modules =
ModuleName.Map.fold
(fun _modname mctx acc ->
let acc = gather_scope_vars acc mctx.modules in
ScopeVar.Map.union (fun _ _ -> assert false) acc mctx.scope_var_mapping)
(fun _modname mctx (vmap, reentr) ->
let vmap, reentr = gather_scope_vars (vmap, reentr) mctx.modules in
( ScopeVar.Map.union
(fun _ _ -> assert false)
vmap mctx.scope_var_mapping,
ScopeVar.Map.union
(fun _ _ -> assert false)
reentr mctx.reentrant_vars ))
modules acc
in
let ctx =
{
ctx with
scope_var_mapping = gather_scope_vars ctx.scope_var_mapping ctx.modules;
}
let scope_var_mapping, reentrant_vars =
gather_scope_vars (ctx.scope_var_mapping, ctx.reentrant_vars) ctx.modules
in
{ ctx with scope_var_mapping; reentrant_vars }
in
let rec process_decl_ctx ctx decl_ctx =
let ctx_scopes =

13
compiler/scopelang/print.ml
View File

@ -52,15 +52,16 @@ let scope ?debug ctx fmt (name, (decl, _pos)) =
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@]@\n@[<v 2> %a@]"
Print.keyword "let" Print.keyword "scope" ScopeName.format name
(Format.pp_print_list ~pp_sep:Format.pp_print_space
(fun fmt (scope_var, (typ, vis)) ->
(fun fmt (scope_var, svar) ->
Format.fprintf fmt "%a%a%a %a%a%a%a%a" Print.punctuation "("
ScopeVar.format scope_var Print.punctuation ":" (Print.typ ctx) typ
Print.punctuation "|" Print.keyword
(match Mark.remove vis.Desugared.Ast.io_input with
ScopeVar.format scope_var Print.punctuation ":" (Print.typ ctx)
svar.svar_in_ty Print.punctuation "|" Print.keyword
(match Mark.remove svar.svar_io.Desugared.Ast.io_input with
| NoInput -> "internal"
| OnlyInput -> "input"
| Reentrant -> "context")
(if Mark.remove vis.Desugared.Ast.io_output then fun fmt () ->
(if Mark.remove svar.svar_io.Desugared.Ast.io_output then
fun fmt () ->
Format.fprintf fmt "%a@,%a" Print.punctuation "|" Print.keyword
"output"
else fun fmt () -> Format.fprintf fmt "@<0>")
@ -81,7 +82,7 @@ let scope ?debug ctx fmt (name, (decl, _pos)) =
| ScopelangScopeVar { name = v } -> (
match
Mark.remove
(snd (ScopeVar.Map.find (Mark.remove v) decl.scope_sig))
(ScopeVar.Map.find (Mark.remove v) decl.scope_sig).svar_io
.io_input
with
| Reentrant ->

4
compiler/shared_ast/definitions.ml
View File

@ -229,6 +229,7 @@ and naked_typ =
| TOption of typ
| TArrow of typ list * typ
| TArray of typ
| TDefault of typ
| TAny
| TClosureEnv (** Hides an existential type needed for closure conversion *)
@ -549,6 +550,9 @@ and ('a, 'b, 'm) base_gexpr =
cons : ('a, 'm) gexpr;
}
-> ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr
| EPureDefault :
('a, 'm) gexpr
-> ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr
| EEmptyError : ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr
| EErrorOnEmpty :
('a, 'm) gexpr

69
compiler/shared_ast/expr.ml
View File

@ -126,10 +126,12 @@ let eapp f args = Box.app1n f args @@ fun f args -> EApp { f; args }
let eassert e1 = Box.app1 e1 @@ fun e1 -> EAssert e1
let eop op tys = Box.app0 @@ EOp { op; tys }
let edefault excepts just cons =
let edefault ~excepts ~just ~cons =
Box.app2n just cons excepts
@@ fun just cons excepts -> EDefault { excepts; just; cons }
let epuredefault e = Box.app1 e @@ fun e1 -> EPureDefault e1
let eifthenelse cond etrue efalse =
Box.app3 cond etrue efalse
@@ fun cond etrue efalse -> EIfThenElse { cond; etrue; efalse }
@ -248,9 +250,12 @@ let maybe_ty (type m) ?(typ = TAny) (m : m mark) : typ =
| Untyped { pos } | Custom { pos; _ } -> Mark.add pos typ
| Typed { ty; _ } -> ty
let untyped = Untyped { pos = Pos.no_pos }
let typed = Typed { pos = Pos.no_pos; ty = TLit TUnit, Pos.no_pos }
(* - Predefined types (option) - *)
let option_enum = EnumName.fresh [] ("eoption", Pos.no_pos)
let option_enum = EnumName.fresh [] ("Eoption", Pos.no_pos)
let none_constr = EnumConstructor.fresh ("ENone", Pos.no_pos)
let some_constr = EnumConstructor.fresh ("ESome", Pos.no_pos)
@ -285,7 +290,8 @@ let map
| EInj { name; cons; e } -> einj ~name ~cons ~e:(f e) m
| EAssert e1 -> eassert (f e1) m
| EDefault { excepts; just; cons } ->
edefault (List.map f excepts) (f just) (f cons) m
edefault ~excepts:(List.map f excepts) ~just:(f just) ~cons:(f cons) m
| EPureDefault e1 -> epuredefault (f e1) m
| EEmptyError -> eemptyerror m
| EErrorOnEmpty e1 -> eerroronempty (f e1) m
| ECatch { body; exn; handler } -> ecatch (f body) exn (f handler) m
@ -330,6 +336,7 @@ let shallow_fold
| EInj { e; _ } -> acc |> f e
| EAssert e -> acc |> f e
| EDefault { excepts; just; cons } -> acc |> lfold excepts |> f just |> f cons
| EPureDefault e -> acc |> f e
| EErrorOnEmpty e -> acc |> f e
| ECatch { body; handler; _ } -> acc |> f body |> f handler
| EStruct { fields; _ } -> acc |> StructField.Map.fold (fun _ -> f) fields
@ -396,7 +403,10 @@ let map_gather
let acc1, excepts = lfoldmap excepts in
let acc2, just = f just in
let acc3, cons = f cons in
join (join acc1 acc2) acc3, edefault excepts just cons m
join (join acc1 acc2) acc3, edefault ~excepts ~just ~cons m
| EPureDefault e ->
let acc, e = f e in
acc, epuredefault e m
| EEmptyError -> acc, eemptyerror m
| EErrorOnEmpty e ->
let acc, e = f e in
@ -594,6 +604,7 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
| ( EDefault { excepts = exc1; just = def1; cons = cons1 },
EDefault { excepts = exc2; just = def2; cons = cons2 } ) ->
equal def1 def2 && equal cons1 cons2 && equal_list exc1 exc2
| EPureDefault e1, EPureDefault e2 -> equal e1 e2
| ( EIfThenElse { cond = if1; etrue = then1; efalse = else1 },
EIfThenElse { cond = if2; etrue = then2; efalse = else2 } ) ->
equal if1 if2 && equal then1 then2 && equal else1 else2
@ -629,10 +640,10 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
ECustom { obj = obj2; targs = targs2; tret = tret2 } ) ->
Type.equal_list targs1 targs2 && Type.equal tret1 tret2 && obj1 == obj2
| ( ( EVar _ | EExternal _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _
| EAbs _ | EApp _ | EAssert _ | EOp _ | EDefault _ | EIfThenElse _
| EEmptyError | EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _
| EStruct _ | EDStructAccess _ | EStructAccess _ | EInj _ | EMatch _
| EScopeCall _ | ECustom _ ),
| EAbs _ | EApp _ | EAssert _ | EOp _ | EDefault _ | EPureDefault _
| EIfThenElse _ | EEmptyError | EErrorOnEmpty _ | ERaise _ | ECatch _
| ELocation _ | EStruct _ | EDStructAccess _ | EStructAccess _ | EInj _
| EMatch _ | EScopeCall _ | ECustom _ ),
_ ) ->
false
@ -711,6 +722,8 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
compare just1 just2 @@< fun () ->
compare cons1 cons2 @@< fun () ->
List.compare compare exs1 exs2
| EPureDefault e1, EPureDefault e2 ->
compare e1 e2
| EEmptyError, EEmptyError -> 0
| EErrorOnEmpty e1, EErrorOnEmpty e2 ->
compare e1 e2
@ -743,6 +756,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
| EInj _, _ -> -1 | _, EInj _ -> 1
| EAssert _, _ -> -1 | _, EAssert _ -> 1
| EDefault _, _ -> -1 | _, EDefault _ -> 1
| EPureDefault _, _ -> -1 | _, EPureDefault _ -> 1
| EEmptyError , _ -> -1 | _, EEmptyError -> 1
| EErrorOnEmpty _, _ -> -1 | _, EErrorOnEmpty _ -> 1
| ERaise _, _ -> -1 | _, ERaise _ -> 1
@ -763,6 +777,7 @@ let rec skip_wrappers : type a. (a, 'm) gexpr -> (a, 'm) gexpr = function
| EErrorOnEmpty e, _ -> skip_wrappers e
| EDefault { excepts = []; just = ELit (LBool true), _; cons = e }, _ ->
skip_wrappers e
| EPureDefault e, _ -> skip_wrappers e
| e -> e
let remove_logging_calls e =
@ -868,6 +883,7 @@ let rec size : type a. (a, 't) gexpr -> int =
| EInj { e; _ } -> size e + 1
| EAssert e -> size e + 1
| EErrorOnEmpty e -> size e + 1
| EPureDefault e -> size e + 1
| EApp { f; args } ->
List.fold_left (fun acc arg -> acc + size arg) (1 + size f) args
| EAbs { binder; _ } ->
@ -925,6 +941,21 @@ let make_app e args pos =
in
eapp e args mark
let make_erroronempty e =
let mark =
map_mark
(fun pos -> pos)
(function
| TDefault ty, _ -> ty
| TAny, pos -> TAny, pos
| ty ->
Message.raise_internal_error
"wrong type: found %a while expecting a TDefault on@;<1 2>%a"
Print.typ_debug ty format (unbox e))
(Mark.get e)
in
eerroronempty e mark
let thunk_term term mark =
let silent = Var.make "_" in
let pos = mark_pos mark in
@ -941,25 +972,11 @@ let make_let_in x tau e1 e2 mpos =
let make_multiple_let_in xs taus e1s e2 mpos =
make_app (make_abs xs e2 taus mpos) e1s (pos e2)
let make_default_unboxed excepts just cons =
let rec bool_value = function
| ELit (LBool b), _ -> Some b
| EApp { f = EOp { op = Log (l, _); _ }, _; args = [e]; _ }, _
when l <> PosRecordIfTrueBool
(* we don't remove the log calls corresponding to source code
definitions !*) ->
bool_value e
| _ -> None
let make_puredefault e =
let mark =
map_mark (fun pos -> pos) (fun ty -> TDefault ty, Mark.get ty) (Mark.get e)
in
match excepts, bool_value just, cons with
| excepts, Some true, (EDefault { excepts = []; just; cons }, _) ->
EDefault { excepts; just; cons }
| [((EDefault _, _) as except)], Some false, _ -> Mark.remove except
| excepts, _, cons -> EDefault { excepts; just; cons }
let make_default exceptions just cons =
Box.app2n just cons exceptions
@@ fun just cons exceptions -> make_default_unboxed exceptions just cons
epuredefault e mark
let make_tuple el m0 =
match el with

40
compiler/shared_ast/expr.mli
View File

@ -80,8 +80,13 @@ val eassert :
val eop : 'a operator -> typ list -> 'm mark -> ('a any, 'm) boxed_gexpr
val edefault :
('a, 'm) boxed_gexpr list ->
('a, 'm) boxed_gexpr ->
excepts:('a, 'm) boxed_gexpr list ->
just:('a, 'm) boxed_gexpr ->
cons:('a, 'm) boxed_gexpr ->
'm mark ->
((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
val epuredefault :
('a, 'm) boxed_gexpr ->
'm mark ->
((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
@ -193,6 +198,12 @@ val maybe_ty : ?typ:naked_typ -> 'm mark -> typ
(** Returns the corresponding type on a typed expr, or [typ] (defaulting to
[TAny]) at the current position on an untyped one *)
val untyped : untyped mark
(** Type witness for untyped marks *)
val typed : typed mark
(** Type witness for untyped marks *)
(** {2 Predefined types} *)
val option_enum : EnumName.t
@ -311,6 +322,12 @@ val make_app :
Pos.t ->
('a any, 'm) boxed_gexpr
val make_puredefault :
('a, 'm) boxed_gexpr -> ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
val make_erroronempty :
('a, 'm) boxed_gexpr -> ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
val empty_thunked_term :
'm mark -> (< defaultTerms : yes ; .. >, 'm) boxed_gexpr
@ -333,25 +350,6 @@ val make_multiple_let_in :
Pos.t ->
('a any, 'm) boxed_gexpr
val make_default :
('a, 'm) boxed_gexpr list ->
('a, 'm) boxed_gexpr ->
('a, 'm) boxed_gexpr ->
'm mark ->
((< polymorphic : yes ; defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
(** [make_default ?pos exceptions just cons] builds a term semantically
equivalent to [<exceptions | just :- cons>] (the [EDefault] constructor)
while avoiding redundant nested constructions. The position is extracted
from [just] by default.
Note that some simplifications take place here, even though all of them
return an [EDefault] term:
- [<ex | true :- def>], when [def] is a default term [<j :- c>] without
exceptions, is collapsed into [<ex | def>]
- [<ex | false :- _>], when [ex] is a single exception of the form
[EDefault], is rewritten as [ex] *)
val make_tuple :
('a any, 'm) boxed_gexpr list -> 'm mark -> ('a, 'm) boxed_gexpr
(** Builds a tuple; the mark argument is only used as witness and for position

68
compiler/shared_ast/interpreter.ml
View File

@ -338,12 +338,13 @@ let rec evaluate_operator
| 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."
(* TODO ? *)
Message.raise_error
"Command @{<cyan>interpret_lcalc@} is not supported without the \
@{<cyan>--avoid_exceptions@} flag. (the interpreter was found trying to \
evaluate the \"handle_default\" operator, which is a leftover from the \
dcalc->lcalc compilation pass and shouldn't happen with \
@{<cyan>--avoid_exceptions@})."
| HandleDefaultOpt, [(EArray exps, _); justification; conclusion] -> (
let valid_exceptions =
ListLabels.filter exps ~f:(function
@ -353,21 +354,16 @@ let rec evaluate_operator
in
match valid_exceptions with
| [] -> (
match
Mark.remove (evaluate_expr (Expr.unthunk_term_nobox justification m))
with
| EInj { name; cons; e = ELit (LBool true), _ }
when EnumName.equal name Expr.option_enum
&& EnumConstructor.equal cons Expr.some_constr ->
let e = evaluate_expr (Expr.unthunk_term_nobox justification m) in
match Mark.remove e with
| ELit (LBool true) ->
Mark.remove (evaluate_expr (Expr.unthunk_term_nobox conclusion m))
| EInj { name; cons; e = (ELit (LBool false), _) as e }
when EnumName.equal name Expr.option_enum
&& EnumConstructor.equal cons Expr.some_constr ->
| ELit (LBool false) ->
EInj
{
name = Expr.option_enum;
cons = Expr.none_constr;
e = Mark.copy e (ELit LUnit);
e = Mark.copy justification (ELit LUnit);
}
| EInj { name; cons; e }
when EnumName.equal name Expr.option_enum
@ -457,6 +453,7 @@ let rec runtime_to_val :
(Array.to_list (Obj.obj o))),
m )
| TArrow (targs, tret) -> ECustom { obj = o; targs; tret }, m
| TDefault ty -> runtime_to_val eval_expr ctx m ty o
| TAny -> assert false
and val_to_runtime :
@ -521,6 +518,7 @@ and val_to_runtime :
curry (runtime_to_val eval_expr ctx m targ x :: acc) targs)
in
curry [] targs
| TDefault ty, _ -> val_to_runtime eval_expr ctx ty v
| _ ->
Message.raise_internal_error
"Could not convert value of type %a to runtime: %a" (Print.typ ctx) ty
@ -711,7 +709,8 @@ let rec evaluate_expr :
| EEmptyError, _ ->
Message.raise_spanned_error (Expr.pos e')
"This variable evaluated to an empty term (no rule that defined it \
applied in this situation)"
applied in this situation): %a"
Expr.format e
| e -> e)
| EDefault { excepts; just; cons } -> (
let excepts = List.map (evaluate_expr ctx lang) excepts in
@ -720,7 +719,6 @@ let rec evaluate_expr :
| 0 -> (
let just = evaluate_expr ctx lang just in
match Mark.remove just with
| EEmptyError -> Mark.add m EEmptyError
| ELit (LBool true) -> evaluate_expr ctx lang cons
| ELit (LBool false) -> Mark.copy e EEmptyError
| _ ->
@ -736,6 +734,7 @@ let rec evaluate_expr :
(List.filter (fun sub -> not (is_empty_error sub)) excepts))
"There is a conflict between multiple valid consequences for assigning \
the same variable.")
| EPureDefault e -> evaluate_expr ctx lang e
| ERaise exn -> raise (CatalaException exn)
| ECatch { body; exn; handler } -> (
try evaluate_expr ctx lang body
@ -788,6 +787,7 @@ let addcustom e =
| (ECustom _, _) as e -> Expr.map ~f e
| EOp { op; tys }, m -> Expr.eop (Operator.translate op) tys m
| (EDefault _, _) as e -> Expr.map ~f e
| (EPureDefault _, _) as e -> Expr.map ~f e
| (EEmptyError, _) as e -> Expr.map ~f e
| (EErrorOnEmpty _, _) as e -> Expr.map ~f e
| (ECatch _, _) as e -> Expr.map ~f e
@ -809,6 +809,7 @@ let delcustom e =
| ECustom _, _ -> invalid_arg "Custom term remaining in evaluated term"
| EOp { op; tys }, m -> Expr.eop (Operator.translate op) tys m
| (EDefault _, _) as e -> Expr.map ~f e
| (EPureDefault _, _) as e -> Expr.map ~f e
| (EEmptyError, _) as e -> Expr.map ~f e
| (EErrorOnEmpty _, _) as e -> Expr.map ~f e
| (ECatch _, _) as e -> Expr.map ~f e
@ -835,20 +836,47 @@ let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
cannot provide anything so we have to fail. *)
let taus = StructName.Map.find s_in ctx.ctx_structs in
let application_term =
let pos = Expr.mark_pos mark_e in
StructField.Map.map
(fun ty ->
match Mark.remove ty with
| TOption _ ->
| TArrow (ty_in, ((TDefault _, _) as ty_out)) ->
(* Context args may return an option if avoid_exceptions is off *)
Expr.make_abs
(Array.of_list @@ List.map (fun _ -> Var.make "_") ty_in)
(Expr.eraise NoValueProvided (Expr.with_ty mark_e ty_out))
ty_in (Expr.mark_pos mark_e)
| TArrow (ty_in, (TOption _, _)) ->
(* ... or an option if it is on *)
Expr.make_abs
(Array.of_list @@ List.map (fun _ -> Var.make "_") ty_in)
(Expr.einj ~e:(Expr.elit LUnit mark_e) ~cons:Expr.none_constr
~name:Expr.option_enum mark_e
: (_, _) boxed_gexpr)
ty_in pos
| TTuple ((TArrow (ty_in, (TOption _, _)), _) :: _) ->
(* ... or a closure if closure conversion is enabled *)
Expr.make_tuple
[
Expr.make_abs
(Array.of_list @@ List.map (fun _ -> Var.make "_") ty_in)
(Expr.einj ~e:(Expr.elit LUnit mark_e) ~cons:Expr.none_constr
~name:Expr.option_enum mark_e)
ty_in (Expr.mark_pos mark_e);
Expr.eapp
(Expr.eop Operator.ToClosureEnv [TClosureEnv, pos] mark_e)
[Expr.etuple [] mark_e]
mark_e;
]
mark_e
| _ ->
Message.raise_spanned_error (Mark.get ty)
"This scope needs input arguments to be executed. But the Catala \
built-in interpreter does not have a way to retrieve input \
values from the command line, so it cannot execute this scope. \
Please create another scope that provides the input arguments \
to this one and execute it instead. ")
to this one and execute it instead."
Print.typ_debug ty)
taus
in
let to_interpret =

41
compiler/shared_ast/optimizations.ml
View File

@ -213,6 +213,26 @@ let rec optimize_expr :
| EStructAccess { name; field; e = EStruct { name = name1; fields }, _ }
when StructName.equal name name1 ->
Mark.remove (StructField.Map.find field fields)
| EErrorOnEmpty
(EDefault { excepts = []; just = ELit (LBool true), _; cons }, _)
when false
(* FIXME: this optimisation is correct and useful, but currently
breaks expectations of the without-exceptions backend *) ->
(* No exceptions, always true *)
Mark.remove cons
| EErrorOnEmpty
( EDefault
{
excepts =
[
( EDefault { excepts = []; just = ELit (LBool true), _; cons },
_ );
];
_;
},
_ ) ->
(* Single, always true exception *)
Mark.remove cons
| EDefault { excepts; just; cons } -> (
(* TODO: mechanically prove each of these optimizations correct *)
let excepts =
@ -237,19 +257,13 @@ let rec optimize_expr :
assert false
else
match excepts, just with
| [except], _ when Expr.is_value except ->
(* if there is only one exception and it is a non-empty value it is
always chosen *)
Mark.remove except
| ( [],
( ( ELit (LBool true)
| EApp
{
f = EOp { op = Log _; _ }, _;
args = [(ELit (LBool true), _)];
} ),
_ ) ) ->
Mark.remove cons
| ( [
( (EDefault { excepts = []; just = ELit (LBool true), _; _ } as dft),
_ );
],
_ ) ->
(* Single exception with condition [true] *)
dft
| ( [],
( ( ELit (LBool false)
| EApp
@ -258,6 +272,7 @@ let rec optimize_expr :
args = [(ELit (LBool false), _)];
} ),
_ ) ) ->
(* No exceptions and condition false *)
EEmptyError
| excepts, just -> EDefault { excepts; just; cons })
| EIfThenElse

50
compiler/shared_ast/print.ml
View File

@ -164,6 +164,10 @@ let rec typ_gen
| TArray t1 ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "collection" (typ ~colors)
t1
| TDefault t1 ->
punctuation fmt "⟨";
typ ~colors fmt t1;
punctuation fmt "⟩"
| TAny -> base_type fmt "any"
| TClosureEnv -> base_type fmt "closure_env"
@ -424,6 +428,7 @@ module Precedence = struct
| EDStructAccess _ | EStructAccess _ -> Dot
| EAssert _ -> App
| EDefault _ -> Contained
| EPureDefault _ -> Contained
| EEmptyError -> Contained
| EErrorOnEmpty _ -> App
| ERaise _ -> App
@ -511,7 +516,7 @@ module ExprGen (C : EXPR_PARAM) = struct
(pp_color_string (List.hd colors))
")"
| EArray es ->
Format.fprintf fmt "@[<hov 2>%a %a@] %a" punctuation "["
Format.fprintf fmt "@[<hv 2>%a@,@[<hov>%a@]@;<0 -2>%a@]" punctuation "["
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ";@ ")
(fun fmt e -> lhs exprc fmt e))
@ -641,6 +646,12 @@ module ExprGen (C : EXPR_PARAM) = struct
cons
(default_punct (List.hd colors))
"⟩"
| EPureDefault e ->
Format.fprintf fmt "%a%a%a"
(default_punct (List.hd colors))
"⟨" expr e
(default_punct (List.hd colors))
"⟩"
| EEmptyError -> lit_style fmt "∅"
| EErrorOnEmpty e' ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" op_style "error_empty"
@ -678,8 +689,8 @@ module ExprGen (C : EXPR_PARAM) = struct
Format.fprintf fmt "@[<hv 2>%a@ %a@]" EnumConstructor.format cons
(rhs exprc) e
| EMatch { e; cases; _ } ->
Format.fprintf fmt "@[<v 0>@[<hv 2>%a@ %a@ %a@]@ %a@]" keyword "match"
(lhs exprc) e keyword "with"
Format.fprintf fmt "@[<v 0>@[<hv 2>%a@ %a@;<1 -2>%a@]@ %a@]" keyword
"match" (lhs exprc) e keyword "with"
(EnumConstructor.Map.format_bindings
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt pp_cons_name case_expr ->
@ -856,12 +867,11 @@ let struct_
fmt
(pp_name : Format.formatter -> unit)
(c : typ StructField.Map.t) =
Format.fprintf fmt "@[<hv 0>@[<hv 2>@[<h>%a %t %a@;%a@]@;%a@]%a@]@;" keyword
"type" pp_name punctuation "=" punctuation "{"
(StructField.Map.format_bindings
~pp_sep:(fun _ _ -> ())
Format.fprintf fmt "@[<hv 2>%a %t %a %a@ %a@;<1 -2>%a@]@," keyword "type"
pp_name punctuation "=" punctuation "{"
(StructField.Map.format_bindings ~pp_sep:Format.pp_print_space
(fun fmt pp_n ty ->
Format.fprintf fmt "@[<h 2>%t%a %a%a@]@ " pp_n keyword ":"
Format.fprintf fmt "@[<h 2>%t%a %a%a@]" pp_n keyword ":"
(if debug then typ_debug else typ decl_ctx)
ty punctuation ";"))
c punctuation "}"
@ -884,10 +894,21 @@ let scope
scope_body ~debug ctx fmt (n, s);
Format.pp_close_box fmt ()
let code_item ?(debug = false) decl_ctx fmt c =
let code_item ?(debug = false) ?name decl_ctx fmt c =
match c with
| ScopeDef (n, b) -> scope ~debug decl_ctx fmt (n, b)
| ScopeDef (n, b) ->
let n =
match debug, name with
| true, Some n -> ScopeName.fresh [] (n, Pos.no_pos)
| _ -> n
in
scope ~debug decl_ctx fmt (n, b)
| Topdef (n, ty, e) ->
let n =
match debug, name with
| true, Some n -> TopdefName.fresh [] (n, Pos.no_pos)
| _ -> n
in
Format.fprintf fmt "@[<v 2>@[<hov 2>%a@ %a@ %a@ %a@ %a@]@ %a@]" keyword
"let topval" TopdefName.format n op_style ":" (typ decl_ctx) ty op_style
"=" (expr ~debug ()) e
@ -896,9 +917,9 @@ 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
let x, cl = Bindlib.unbind b in
Format.fprintf fmt "%a @.%a"
(code_item ~debug decl_ctx)
(code_item ~debug ~name:(Format.asprintf "%a" var_debug x) decl_ctx)
c
(code_item_list ~debug decl_ctx)
cl
@ -1071,8 +1092,9 @@ module UserFacing = struct
| EAbs _ -> Format.pp_print_string ppf "<function>"
| EExternal _ -> Format.pp_print_string ppf "<external>"
| EApp _ | EOp _ | EVar _ | EIfThenElse _ | EMatch _ | ETupleAccess _
| EStructAccess _ | EAssert _ | EDefault _ | EErrorOnEmpty _ | ERaise _
| ECatch _ | ELocation _ | EScopeCall _ | EDStructAccess _ | ECustom _ ->
| EStructAccess _ | EAssert _ | EDefault _ | EPureDefault _
| EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EScopeCall _
| EDStructAccess _ | ECustom _ ->
fallback ppf e
(* This function is already in module [Expr], but [Expr] depends on this

7
compiler/shared_ast/scope.ml
View File

@ -166,6 +166,13 @@ let build_typ_from_sig
let result_typ = Mark.add pos (TStruct scope_return_struct_name) in
Mark.add pos (TArrow ([input_typ], result_typ))
let input_type ty io =
match io, ty with
| (Runtime.Reentrant, iopos), (TArrow (args, ret), tpos) ->
TArrow (args, (TDefault ret, iopos)), tpos
| (Runtime.Reentrant, iopos), (ty, tpos) -> TDefault (ty, tpos), iopos
| _, ty -> ty
type 'e scope_name_or_var = ScopeName of ScopeName.t | ScopeVar of 'e Var.t
let to_expr (ctx : decl_ctx) (body : 'e scope_body) (mark_scope : 'm) : 'e boxed

7
compiler/shared_ast/scope.mli
View File

@ -130,6 +130,13 @@ val build_typ_from_sig :
(** [build_typ_from_sig ctx in_struct out_struct pos] builds the arrow type for
the specified scope *)
val input_type : typ -> Runtime.io_input Mark.pos -> typ
(** Returns the correct input type for scope input variables: this is [typ] for
non-reentrant variables, but for reentrant variables, it is nested in a
[TDefault], which only applies to the return type on functions. Note that
this doesn't take thunking into account (thunking is added during the
scopelang->dcalc translation) *)
(** {2 Analysis and tests} *)
val free_vars_body_expr : 'e scope_body_expr -> 'e Var.Set.t

8
compiler/shared_ast/type.ml
View File

@ -31,9 +31,10 @@ 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
| TDefault t1, TDefault t2 -> equal t1 t2
| TClosureEnv, TClosureEnv | TAny, TAny -> true
| ( ( TLit _ | TTuple _ | TStruct _ | TEnum _ | TOption _ | TArrow _
| TArray _ | TAny | TClosureEnv ),
| TArray _ | TDefault _ | TAny | TClosureEnv ),
_ ) ->
false
@ -52,9 +53,10 @@ 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
| TDefault t1, TDefault t2 -> unifiable t1 t2
| TClosureEnv, TClosureEnv -> true
| ( ( TLit _ | TTuple _ | TStruct _ | TEnum _ | TOption _ | TArrow _
| TArray _ | TClosureEnv ),
| TArray _ | TDefault _ | TClosureEnv ),
_ ) ->
false
@ -86,6 +88,8 @@ let rec compare ty1 ty2 =
| _, TArrow _ -> 1
| TArray _, _ -> -1
| _, TArray _ -> 1
| TDefault _, _ -> -1
| _, TDefault _ -> 1
| TClosureEnv, _ -> -1
| _, TClosureEnv -> 1

95
compiler/shared_ast/typing.ml
View File

@ -48,6 +48,7 @@ and naked_typ =
| TEnum of A.EnumName.t
| TOption of unionfind_typ
| TArray of unionfind_typ
| TDefault of unionfind_typ
| TAny of Any.t
| TClosureEnv
@ -62,6 +63,7 @@ let rec typ_to_ast ~leave_unresolved (ty : unionfind_typ) : A.typ =
| TOption t -> A.TOption (typ_to_ast t), pos
| TArrow (t1, t2) -> A.TArrow (List.map typ_to_ast t1, typ_to_ast t2), pos
| TArray t1 -> A.TArray (typ_to_ast t1), pos
| TDefault t1 -> A.TDefault (typ_to_ast t1), pos
| TAny _ ->
if leave_unresolved then A.TAny, pos
else
@ -82,6 +84,7 @@ let rec ast_to_typ (ty : A.typ) : unionfind_typ =
| A.TEnum e -> TEnum e
| A.TOption t -> TOption (ast_to_typ t)
| A.TArray t -> TArray (ast_to_typ t)
| A.TDefault t -> TDefault (ast_to_typ t)
| A.TAny -> TAny (Any.fresh ())
| A.TClosureEnv -> TClosureEnv
in
@ -157,6 +160,10 @@ let rec format_typ
| TAny _ when not Cli.globals.debug ->
Format.pp_print_string fmt "collection"
| _ -> Format.fprintf fmt "@[collection@ %a@]" (format_typ ~colors) t1)
| TDefault t1 ->
Format.pp_print_as fmt 1 "⟨";
format_typ ~colors fmt t1;
Format.pp_print_as fmt 1 "⟩"
| TAny v ->
if Cli.globals.debug then Format.fprintf fmt "<a%d>" (Any.hash v)
else Format.pp_print_string fmt "<any>"
@ -199,10 +206,11 @@ 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'
| TDefault t1', TDefault t2' -> unify e t1' t2'
| TClosureEnv, TClosureEnv -> ()
| TAny _, _ | _, TAny _ -> ()
| ( ( TLit _ | TArrow _ | TTuple _ | TStruct _ | TEnum _ | TOption _
| TArray _ | TClosureEnv ),
| TArray _ | TDefault _ | TClosureEnv ),
_ ) ->
raise_type_error ()
in
@ -216,26 +224,44 @@ let handle_type_error ctx (A.AnyExpr e) t1 t2 =
persistent version of the union-find data structure. *)
let t1_repr = UnionFind.get (UnionFind.find t1) in
let t2_repr = UnionFind.get (UnionFind.find t2) in
let e_pos = Expr.pos e in
let t1_pos = Mark.get t1_repr in
let t2_pos = Mark.get t2_repr in
Message.raise_multispanned_error_full
let pos_msgs =
if e_pos = t1_pos then
[
( Some
(fun ppf ->
Format.pp_print_string ppf
"Error coming from typechecking the following expression:"),
Expr.pos e );
( Some
(fun ppf ->
Format.fprintf ppf "Type @{<yellow>%a@} coming from expression:"
(format_typ ctx) t1),
t1_pos );
( Some
(fun ppf ->
Format.fprintf ppf "Type @{<yellow>%a@} coming from expression:"
( (fun ppf ->
Format.fprintf ppf "@[<hv 2>@[<hov>%a@ %a@]:" Format.pp_print_text
"This expression has type" (format_typ ctx) t1;
if Cli.globals.debug then Format.fprintf ppf "@ %a@]" Expr.format e
else Format.pp_close_box ppf ()),
e_pos );
( (fun ppf ->
Format.fprintf ppf
"@[<hov>Expected@ type@ %a@ coming@ from@ expression:@]"
(format_typ ctx) t2),
t2_pos );
]
else
[
( (fun ppf ->
Format.fprintf ppf "@[<hv 2>@[<hov>%a:@]" Format.pp_print_text
"While typechecking the following expression";
if Cli.globals.debug then Format.fprintf ppf "@ %a@]" Expr.format e
else Format.pp_close_box ppf ()),
e_pos );
( (fun ppf ->
Format.fprintf ppf "@[<hov>Type@ %a@ is@ coming@ from:@]"
(format_typ ctx) t1),
t1_pos );
( (fun ppf ->
Format.fprintf ppf "@[<hov>Type@ %a@ is@ coming@ from:@]"
(format_typ ctx) t2),
t2_pos );
]
in
Message.raise_multispanned_error_full
(List.map (fun (a, b) -> Some a, b) pos_msgs)
"@[<v>Error during typechecking, incompatible types:@,\
@[<v>@{<bold;blue>@<3>%s@} @[<hov>%a@]@,\
@{<bold;blue>@<3>%s@} @[<hov>%a@]@]@]" "┌─⯈" (format_typ ctx) t1 "└─⯈"
@ -268,6 +294,7 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) :
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 default a = lazy (UnionFind.make (TDefault (Lazy.force a), pos)) in
let ( @-> ) x y =
lazy (UnionFind.make (TArrow (List.map Lazy.force x, Lazy.force y), pos))
in
@ -282,10 +309,10 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) :
| Log (PosRecordIfTrueBool, _) -> [bt] @-> bt
| Log _ -> [any] @-> any
| Length -> [array any] @-> it
| HandleDefault -> [array ([ut] @-> any); [ut] @-> bt; [ut] @-> any] @-> any
| HandleDefault ->
[array ([ut] @-> default any); [ut] @-> bt; [ut] @-> any] @-> default any
| HandleDefaultOpt ->
[array (option any); [ut] @-> option bt; [ut] @-> option any]
@-> option any
[array (option any); [ut] @-> bt; [ut] @-> option any] @-> option any
| ToClosureEnv -> [any] @-> cet
| FromClosureEnv -> [cet] @-> any
in
@ -314,6 +341,7 @@ module Env = struct
vars : ('e, unionfind_typ) Var.Map.t;
scope_vars : A.typ A.ScopeVar.Map.t;
scopes : A.typ A.ScopeVar.Map.t A.ScopeName.Map.t;
scopes_input : A.typ A.ScopeVar.Map.t A.ScopeName.Map.t;
toplevel_vars : A.typ A.TopdefName.Map.t;
modules : 'e t A.ModuleName.Map.t;
}
@ -333,6 +361,7 @@ module Env = struct
vars = Var.Map.empty;
scope_vars = A.ScopeVar.Map.empty;
scopes = A.ScopeName.Map.empty;
scopes_input = A.ScopeName.Map.empty;
toplevel_vars = A.TopdefName.Map.empty;
modules = A.ModuleName.Map.empty;
}
@ -354,8 +383,12 @@ module Env = struct
let add_scope_var v typ t =
{ t with scope_vars = A.ScopeVar.Map.add v typ t.scope_vars }
let add_scope scope_name ~vars t =
{ t with scopes = A.ScopeName.Map.add scope_name vars t.scopes }
let add_scope scope_name ~vars ~in_vars t =
{
t with
scopes = A.ScopeName.Map.add scope_name vars t.scopes;
scopes_input = A.ScopeName.Map.add scope_name in_vars t.scopes_input;
}
let add_toplevel_var v typ t =
{ t with toplevel_vars = A.TopdefName.Map.add v typ t.toplevel_vars }
@ -667,7 +700,7 @@ and typecheck_expr_top_down :
let mark = mark_with_tau_and_unify (unionfind (TStruct scope_out_struct)) in
let vars =
let env = Env.module_env path env in
A.ScopeName.Map.find scope env.scopes
A.ScopeName.Map.find scope env.scopes_input
in
let args' =
A.ScopeVar.Map.mapi
@ -679,7 +712,10 @@ and typecheck_expr_top_down :
Expr.escopecall ~scope ~args:args' mark
| A.ERaise ex -> Expr.eraise ex context_mark
| A.ECatch { body; exn; handler } ->
let body' = typecheck_expr_top_down ~leave_unresolved ctx env tau body in
let body' =
typecheck_expr_top_down ~leave_unresolved ctx env
(unionfind (TDefault tau)) body
in
let handler' =
typecheck_expr_top_down ~leave_unresolved ctx env tau handler
in
@ -871,7 +907,14 @@ and typecheck_expr_top_down :
let excepts' =
List.map (typecheck_expr_top_down ~leave_unresolved ctx env tau) excepts
in
Expr.edefault excepts' just' cons' context_mark
Expr.edefault ~excepts:excepts' ~just:just' ~cons:cons' context_mark
| A.EPureDefault e1 ->
let inner_ty = unionfind ~pos:e1 (TAny (Any.fresh ())) in
let mark =
mark_with_tau_and_unify (unionfind ~pos:e1 (TDefault inner_ty))
in
let e1' = typecheck_expr_top_down ~leave_unresolved ctx env inner_ty e1 in
Expr.epuredefault e1' mark
| A.EIfThenElse { cond; etrue = et; efalse = ef } ->
let et' = typecheck_expr_top_down ~leave_unresolved ctx env tau et in
let ef' = typecheck_expr_top_down ~leave_unresolved ctx env tau ef in
@ -889,9 +932,11 @@ and typecheck_expr_top_down :
e1
in
Expr.eassert e1' mark
| A.EEmptyError -> Expr.eemptyerror (ty_mark (TAny (Any.fresh ())))
| A.EEmptyError ->
Expr.eemptyerror (ty_mark (TDefault (unionfind (TAny (Any.fresh ())))))
| A.EErrorOnEmpty e1 ->
let e1' = typecheck_expr_top_down ~leave_unresolved ctx env tau e1 in
let tau' = unionfind (TDefault tau) in
let e1' = typecheck_expr_top_down ~leave_unresolved ctx env tau' e1 in
Expr.eerroronempty e1' context_mark
| A.EArray es ->
let cell_type = unionfind (TAny (Any.fresh ())) in

9
compiler/shared_ast/typing.mli
View File

@ -27,7 +27,14 @@ module Env : sig
val add_var : 'e Var.t -> typ -> 'e t -> 'e t
val add_toplevel_var : TopdefName.t -> typ -> 'e t -> 'e t
val add_scope_var : ScopeVar.t -> typ -> 'e t -> 'e t
val add_scope : ScopeName.t -> vars:typ ScopeVar.Map.t -> 'e t -> 'e t
val add_scope :
ScopeName.t ->
vars:typ ScopeVar.Map.t ->
in_vars:typ ScopeVar.Map.t ->
'e t ->
'e t
val add_module : ModuleName.t -> module_env:'e t -> 'e t -> 'e t
val module_env : Uid.Path.t -> 'e t -> 'e t
val open_scope : ScopeName.t -> 'e t -> 'e t

7
compiler/verification/conditions.ml
View File

@ -142,12 +142,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) :
(Print.expr ()) e)
| EErrorOnEmpty d ->
d (* input subscope variables and non-input scope variable *)
| _ ->
Message.raise_spanned_error (Expr.pos e)
"Internal error: this expression does not have the structure expected by \
the VC generator:\n\
%a"
(Print.expr ()) e
| _ -> e
(** {1 Verification conditions generator}*)

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

@ -206,6 +206,8 @@ let rec print_z3model_expr (ctx : context) (ty : typ) (e : Expr.expr) : string =
| TAny -> failwith "[Z3 model]: Pretty-printing of Any not supported"
| TClosureEnv ->
failwith "[Z3 model]: Pretty-printing of closure_env not supported"
| TDefault _ ->
failwith "[Z3 model]: Pretty-printing of default terms 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
@ -273,6 +275,7 @@ let rec translate_typ (ctx : context) (t : naked_typ) : context * Sort.sort =
| TTuple _ -> failwith "[Z3 encoding] TTuple type not supported"
| TEnum e -> find_or_create_enum ctx e
| TOption _ -> failwith "[Z3 encoding] TOption type not supported"
| TDefault _ -> failwith "[Z3 encoding] TDefault type not supported"
| TArrow _ -> failwith "[Z3 encoding] TArrow type not supported"
| TArray _ ->
(* For now, we are only encoding the (symbolic) length of an array.
@ -761,6 +764,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
| EAssert e -> translate_expr ctx e
| EOp _ -> failwith "[Z3 encoding] EOp unsupported"
| EDefault _ -> failwith "[Z3 encoding] EDefault unsupported"
| EPureDefault _ -> failwith "[Z3 encoding] EPureDefault unsupported"
| EIfThenElse { cond = e_if; etrue = e_then; efalse = e_else } ->
(* We rely on Z3's native encoding for ite to encode this node. There might
be some interesting optimization in the future about when to split this

4
examples/aides_logement/tests/tests_calcul_al_accession_propriete.catala_fr
View File

@ -81,7 +81,7 @@ $ catala Interpret -s Exemple1
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple1 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 96,48 €
[RESULT] montant = 96,48 €
```
```catala-test-inline
@ -93,6 +93,6 @@ $ catala Interpret -s Exemple2
```catala-test-inline
$ catala Interpret_lcalc -s Exemple2 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 85,00 €
[RESULT] montant = 85,00 €
```

8
examples/aides_logement/tests/tests_calcul_al_locatif.catala_fr
View File

@ -140,13 +140,13 @@ $ catala Interpret -s Exemple2 --disable_warnings
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple1 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 345,73 €
[RESULT] montant = 345,73 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple2 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 352,77 €
[RESULT] montant = 352,77 €
```
```catala-test-inline
@ -164,11 +164,11 @@ $ catala Interpret -s Exemple4 --disable_warnings
```catala-test-inline
$ catala Interpret_lcalc -s Exemple3 --disable_warnings --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 339,70 €
[RESULT] montant = 339,70 €
```
```catala-test-inline
$ catala Interpret_lcalc -s Exemple4 --disable_warnings --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 230,63 €
[RESULT] montant = 230,63 €
```

2
examples/aides_logement/tests/tests_calcul_al_logement_foyer.catala_fr
View File

@ -39,5 +39,5 @@ $ catala Interpret -s CasTest1 --disable_warnings
```catala-test-inline
$ catala Interpret_Lcalc -s CasTest1 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 76,38 €
[RESULT] montant = 76,38 €
```

8
examples/aides_logement/tests/tests_calcul_apl_accession_propriete.catala_fr
View File

@ -174,20 +174,20 @@ $ catala Interpret -s Exemple4 --disable_warnings
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple1 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 181,91 €
[RESULT] montant = 181,91 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple2 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 67,34 €
[RESULT] montant = 67,34 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple3 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 181,91 €
[RESULT] montant = 181,91 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple4 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 118,59 €
[RESULT] montant = 118,59 €
```

18
examples/aides_logement/tests/tests_calcul_apl_locatif.catala_fr
View File

@ -334,45 +334,45 @@ $ catala Interpret -s Exemple9 --disable_warnings
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple1 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 0,00 €
[RESULT] montant = 0,00 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple2 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 352,77 €
[RESULT] montant = 352,77 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple3 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 321,61 €
[RESULT] montant = 321,61 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple4 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 0,00 €
[RESULT] montant = 0,00 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple5 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 311,56 €
[RESULT] montant = 311,56 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple6 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 0,00 €
[RESULT] montant = 0,00 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple7 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 153,77 €
[RESULT] montant = 153,77 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple8 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 11,06 €
[RESULT] montant = 11,06 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple9 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 210,06 €
[RESULT] montant = 210,06 €
```

10
examples/aides_logement/tests/tests_calcul_apl_logement_foyer.catala_fr
View File

@ -168,25 +168,25 @@ $ catala Interpret -s CasTest5 --disable_warnings
```catala-test-inline
$ catala Interpret_Lcalc -s CasTest1 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 12,06 €
[RESULT] montant = 12,06 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s CasTest2 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 23,12 €
[RESULT] montant = 23,12 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s CasTest3 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 154,78 €
[RESULT] montant = 154,78 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s CasTest4 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 154,78 €
[RESULT] montant = 154,78 €
```
```catala-test-inline
$ catala Interpret_Lcalc -s CasTest5 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant = ESome 129,65 €
[RESULT] montant = 129,65 €
```

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

@ -164,15 +164,15 @@ $ catala Interpret -s Exemple1
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple1 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant_versé = ESome 246,23 €
[RESULT] éligibilité = ESome vrai
[RESULT] montant_versé = 246,23 €
[RESULT] éligibilité = vrai
```
```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 vrai
[RESULT] montant_versé = 246,23 €
[RESULT] éligibilité = vrai
```
```catala-test-inline
@ -185,13 +185,13 @@ $ catala Interpret -s Exemple2
```catala-test-inline
$ catala Interpret_lcalc -s Exemple2 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] montant_versé = ESome 230,63 €
[RESULT] éligibilité = ESome vrai
[RESULT] montant_versé = 230,63 €
[RESULT] éligibilité = vrai
```
```catala-test-inline
$ catala Interpret_lcalc -s Exemple2 -O --avoid_exceptions --closure_conversion
[RESULT] Computation successful! Results:
[RESULT] montant_versé = ESome 230,63 €
[RESULT] éligibilité = ESome vrai
[RESULT] montant_versé = 230,63 €
[RESULT] éligibilité = vrai
```

6
examples/aides_logement/tests/tests_eligibilite_apl.catala_fr
View File

@ -221,7 +221,7 @@ $ catala Interpret -s Exemple1 --disable_warnings
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple1 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] éligible = ESome vrai
[RESULT] éligible = vrai
```
@ -234,7 +234,7 @@ $ catala Interpret -s Exemple2 --disable_warnings
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple2 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] éligible = ESome AllocationLogementFamiliale ()
[RESULT] éligible = AllocationLogementFamiliale ()
```
@ -247,7 +247,7 @@ $ catala Interpret -s Exemple3 --disable_warnings
```catala-test-inline
$ catala Interpret_Lcalc -s Exemple3 --avoid_exceptions
[RESULT] Computation successful! Results:
[RESULT] éligible = ESome AllocationLogementFamiliale ()
[RESULT] éligible = AllocationLogementFamiliale ()
```
```catala-test-inline

27
runtimes/ocaml/runtime.ml
View File

@ -25,7 +25,11 @@ type decimal = Q.t
type date = Dates_calc.Dates.date
type date_rounding = Dates_calc.Dates.date_rounding
type duration = Dates_calc.Dates.period
type 'a eoption = ENone of unit | ESome of 'a
module Eoption = struct
type 'a t = ENone of unit | ESome of 'a
end
type io_input = NoInput | OnlyInput | Reentrant [@@deriving yojson_of]
type io_log = { io_input : io_input; io_output : bool } [@@deriving yojson_of]
@ -591,24 +595,21 @@ let handle_default :
let handle_default_opt
(pos : source_position)
(exceptions : 'a eoption array)
(just : unit -> bool eoption)
(cons : unit -> 'a eoption) : 'a eoption =
(exceptions : 'a Eoption.t array)
(just : unit -> bool)
(cons : unit -> 'a Eoption.t) : 'a Eoption.t =
let except =
Array.fold_left
(fun acc except ->
match acc, except with
| ENone _, _ -> except
| ESome _, ENone _ -> acc
| ESome _, ESome _ -> raise (ConflictError pos))
(ENone ()) exceptions
| Eoption.ENone _, _ -> except
| Eoption.ESome _, Eoption.ENone _ -> acc
| Eoption.ESome _, Eoption.ESome _ -> raise (ConflictError pos))
(Eoption.ENone ()) exceptions
in
match except with
| ESome _ -> except
| ENone _ -> (
match just () with
| ESome b -> if b then cons () else ENone ()
| ENone _ -> ENone ())
| Eoption.ESome _ -> except
| Eoption.ENone _ -> if just () then cons () else Eoption.ENone ()
let no_input : unit -> 'a = fun _ -> raise EmptyError

12
runtimes/ocaml/runtime.mli
View File

@ -40,7 +40,9 @@ type source_position = {
law_headings : string list;
}
type 'a eoption = ENone of unit | ESome of 'a
module Eoption : sig
type 'a t = ENone of unit | ESome of 'a
end
(** This type characterizes the three levels of visibility for a given scope
variable with regards to the scope's input and possible redefinitions inside
@ -305,10 +307,10 @@ val handle_default :
val handle_default_opt :
source_position ->
'a eoption array ->
(unit -> bool eoption) ->
(unit -> 'a eoption) ->
'a eoption
'a Eoption.t array ->
(unit -> bool) ->
(unit -> 'a Eoption.t) ->
'a Eoption.t
(** @raise ConflictError *)
val no_input : unit -> 'a

5
runtimes/python/catala/src/catala/runtime.py
View File

@ -618,7 +618,7 @@ def handle_default(
def handle_default_opt(
pos: SourcePosition,
exceptions: List[Optional[Any]],
just: Callable[[Unit], Optional[bool]],
just: Callable[[Unit], bool],
cons: Callable[[Unit], Optional[Alpha]]
) -> Optional[Alpha]:
acc: Optional[Alpha] = None
@ -631,9 +631,6 @@ def handle_default_opt(
raise ConflictError(pos)
if acc is None:
b = just(Unit())
if b is None:
return None
else:
if b:
return cons(Unit())
else:

8
tests/test_arithmetic/good/priorities.catala_en
View File

@ -23,8 +23,8 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] w = ESome 0
[RESULT] x = ESome 4
[RESULT] y = ESome 4
[RESULT] z = ESome 390.0
[RESULT] w = 0
[RESULT] x = 4
[RESULT] y = 4
[RESULT] z = 390.0
```

10
tests/test_array/good/aggregation.catala_en
View File

@ -40,13 +40,13 @@ $ catala Interpret -s B
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome [ESome $0.00; ESome $9.00; ESome $5.20]
[RESULT] x = [$0.00; $9.00; $5.20]
```
```catala-test-inline
$ catala Interpret_Lcalc -s B --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] max = ESome $18.00
[RESULT] min = ESome $5.00
[RESULT] y = ESome $17.20
[RESULT] z = ESome 1
[RESULT] max = $18.00
[RESULT] min = $5.00
[RESULT] y = $17.20
[RESULT] z = 1
```

10
tests/test_array/good/aggregation_2.catala_en
View File

@ -51,16 +51,14 @@ $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT]
x =
ESome
[
ESome S { -- id: ESome 0 -- income: ESome $0.00 };
ESome S { -- id: ESome 1 -- income: ESome $9.00 };
ESome S { -- id: ESome 2 -- income: ESome $5.20 }
S { -- id: 0 -- income: $0.00 }; S { -- id: 1 -- income: $9.00 };
S { -- id: 2 -- income: $5.20 }
]
```
```catala-test-inline
$ catala Interpret_Lcalc -s B --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] argmax = ESome S { -- id: ESome 1 -- income: ESome $9.00 }
[RESULT] argmin = ESome S { -- id: ESome 0 -- income: ESome $0.00 }
[RESULT] argmax = S { -- id: 1 -- income: $9.00 }
[RESULT] argmin = S { -- id: 0 -- income: $0.00 }
```

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

@ -34,35 +34,35 @@ scope S:
```catala-test-inline
$ catala scopelang -s S
let scope S (x: integer|internal|output) =
let x : integer = ⟨true ⊢ 0⟩;
assert (map (λ (i: integer) → i + 2) [ 1; 2; 3 ]) = [ 3; 4; 5 ];
assert (filter (λ (i: integer) → i >= 2) [ 1; 2; 3 ]) = [ 2; 3 ];
let x : integer = error_empty ⟨ ⟨true ⊢ ⟨0⟩⟩ | false ⊢ ∅ ⟩;
assert (map (λ (i: integer) → i + 2) [1; 2; 3]) = [3; 4; 5];
assert (filter (λ (i: integer) → i >= 2) [1; 2; 3]) = [2; 3];
assert (map (λ (i: integer) → i + 2)
filter (λ (i: integer) → i > 2) [ 1; 2; 3 ])
= [ 5 ];
filter (λ (i: integer) → i > 2) [1; 2; 3])
= [5];
assert (reduce
(λ (sum1: integer) (sum2: integer) → sum1 + sum2)
0
[ 1; 2; 3 ])
[1; 2; 3])
= 6;
assert (reduce
(λ (sum1: integer) (sum2: integer) → sum1 + sum2)
0
map (λ (i: integer) → i + 2) [ 1; 2; 3 ])
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 (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
[ 1; 2; 3 ])
[1; 2; 3])
= 3;
assert (reduce
(λ (max1: decimal) (max2: decimal) →
if max1 > max2 then max1 else max2)
10.
map (λ (i: integer) → to_rat i) [ 1; 2; 3 ])
map (λ (i: integer) → to_rat i) [1; 2; 3])
= 3.;
assert (reduce
(λ (i_1: integer) (i_2: integer) →
@ -75,7 +75,7 @@ let scope S (x: integer|internal|output) =
i_1
else i_2)
42
[ 1; 2; 3 ])
[1; 2; 3])
= 2
```

11
tests/test_array/good/concatenation.catala_en
View File

@ -19,13 +19,6 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT]
x = ESome [ESome 0; ESome 1; ESome 2; ESome 3; ESome 4; ESome 5; ESome 6]
[RESULT]
y =
ESome
[
ESome 0; ESome 1; ESome 2; ESome 3; ESome 4; ESome 5; ESome 6;
ESome 7; ESome 8; ESome 9; ESome 10
]
[RESULT] x = [0; 1; 2; 3; 4; 5; 6]
[RESULT] y = [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10]
```

4
tests/test_array/good/filter.catala_en
View File

@ -25,7 +25,7 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome [ESome $0.00; ESome $9.00; ESome $5.20]
[RESULT] x = [$0.00; $9.00; $5.20]
```
@ -39,5 +39,5 @@ $ catala Interpret -s B
```catala-test-inline
$ catala Interpret_Lcalc -s B --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] y = ESome [ESome $9.00; ESome $5.20]
[RESULT] y = [$9.00; $5.20]
```

6
tests/test_array/good/filter_map.catala_en
View File

@ -32,11 +32,11 @@ $ catala Interpret -s B
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome [ESome $0.00; ESome $9.00; ESome $5.20]
[RESULT] x = [$0.00; $9.00; $5.20]
```
```catala-test-inline
$ catala Interpret_Lcalc -s B --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] y = ESome [ESome $9.00; ESome $5.20]
[RESULT] z = ESome [ESome false; ESome true; ESome true]
[RESULT] y = [$9.00; $5.20]
[RESULT] z = [false; true; true]
```

10
tests/test_array/good/fold.catala_en
View File

@ -51,16 +51,14 @@ $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT]
x =
ESome
[
ESome S { -- id: ESome 0 -- income: ESome $0.00 };
ESome S { -- id: ESome 1 -- income: ESome $9.00 };
ESome S { -- id: ESome 2 -- income: ESome $5.20 }
S { -- id: 0 -- income: $0.00 }; S { -- id: 1 -- income: $9.00 };
S { -- id: 2 -- income: $5.20 }
]
```
```catala-test-inline
$ catala Interpret_Lcalc -s B --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] argmax = ESome S { -- id: ESome 1 -- income: ESome $9.00 }
[RESULT] argmin = ESome S { -- id: ESome 0 -- income: ESome $0.00 }
[RESULT] argmax = S { -- id: 1 -- income: $9.00 }
[RESULT] argmin = S { -- id: 0 -- income: $0.00 }
```

4
tests/test_array/good/map.catala_en
View File

@ -20,6 +20,6 @@ $ catala Interpret -s B
```catala-test-inline
$ catala Interpret_Lcalc -s B --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome [ESome $4.00; ESome $8.00]
[RESULT] z = ESome [ESome false; ESome true]
[RESULT] x = [$4.00; $8.00]
[RESULT] z = [false; true]
```

10
tests/test_array/good/simple.catala_en
View File

@ -38,13 +38,13 @@ $ catala Interpret -s B
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome [ESome 0; ESome 9; ESome 64]
[RESULT] x = [0; 9; 64]
```
```catala-test-inline
$ catala Interpret_Lcalc -s B --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] v = ESome 3
[RESULT] w = ESome true
[RESULT] y = ESome true
[RESULT] z = ESome false
[RESULT] v = 3
[RESULT] w = true
[RESULT] y = true
[RESULT] z = false
```

4
tests/test_array/good/simpler.catala_en
View File

@ -20,6 +20,6 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] w = ESome false
[RESULT] x = ESome [ESome 0; ESome 9; ESome 64]
[RESULT] w = false
[RESULT] x = [0; 9; 64]
```

2
tests/test_array/good/simplest.catala_en
View File

@ -17,5 +17,5 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome [ESome 0; ESome 4; ESome 8]
[RESULT] x = [0; 4; 8]
```

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

@ -17,21 +17,21 @@ Error during typechecking, incompatible types:
┌─⯈ integer
└─⯈ bool
Error coming from typechecking the following expression:
While typechecking the following expression:
┌─⯈ tests/test_bool/bad/bad_assert.catala_en:9.13-9.14:
└─┐
9 │ assertion x
│ ‾
└─ Test
Type integer coming from expression:
Type integer is coming from:
┌─⯈ tests/test_bool/bad/bad_assert.catala_en:5.20-5.27:
└─┐
5 │ output x content integer
│ ‾‾‾‾‾‾‾
└─ Test
Type bool coming from expression:
Type bool is coming from:
┌─⯈ tests/test_bool/bad/bad_assert.catala_en:9.13-9.14:
└─┐
9 │ assertion x

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

@ -15,21 +15,14 @@ Error during typechecking, incompatible types:
┌─⯈ integer
└─⯈ bool
Error coming from typechecking the following expression:
This expression has type integer:
┌─⯈ tests/test_bool/bad/test_xor_with_int.catala_en:8.30-8.32:
└─┐
8 │ definition test_var equals 10 xor 20
│ ‾‾
└─ 'xor' should be a boolean operator
Type integer coming from expression:
┌─⯈ tests/test_bool/bad/test_xor_with_int.catala_en:8.30-8.32:
└─┐
8 │ definition test_var equals 10 xor 20
│ ‾‾
└─ 'xor' should be a boolean operator
Type bool coming from expression:
Expected type bool coming from expression:
┌─⯈ tests/test_bool/bad/test_xor_with_int.catala_en:8.33-8.36:
└─┐
8 │ definition test_var equals 10 xor 20

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

@ -15,14 +15,18 @@ scope TestBool:
$ catala Dcalc
let TestBool : TestBool_in → TestBool =
λ (TestBool_in: TestBool_in) →
let foo : unit → bool = TestBool_in.foo_in in
let bar : unit → integer = TestBool_in.bar_in in
let bar1 : integer = error_empty ⟨ bar () | true ⊢ ⟨true ⊢ 1⟩ ⟩ in
let foo : unit → ⟨bool⟩ = TestBool_in.foo_in in
let bar : unit → ⟨integer⟩ = TestBool_in.bar_in in
let bar1 : integer =
error_empty
⟨ bar () | true ⊢ ⟨error_empty ⟨ ⟨true ⊢ ⟨1⟩⟩ | false ⊢ ∅ ⟩⟩ ⟩
in
let foo1 : bool =
error_empty
⟨ foo ()
| true
⊢ ⟨true ⊢ ⟨ ⟨bar1 >= 0 ⊢ true⟩, ⟨bar1 < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩ ⟩
⊢ ⟨error_empty
⟨ ⟨bar1 >= 0 ⊢ ⟨true⟩⟩, ⟨bar1 < 0 ⊢ ⟨false⟩⟩ | false ⊢ ∅ ⟩⟩ ⟩
in
{ TestBool foo = foo1; bar = bar1; }
in
@ -43,14 +47,16 @@ struct TestBool = {
bar: integer
}
let scope TestBool (foo: bool|context|output) (bar: integer|context|output) =
let bar : integer = reentrant or by default ⟨true ⊢ 1⟩;
let scope TestBool (foo: ⟨bool⟩|context|output) (bar: ⟨integer⟩|context|
output) =
let bar : integer = reentrant or by default
error_empty ⟨ ⟨true ⊢ ⟨1⟩⟩ | false ⊢ ∅ ⟩;
let foo : bool = reentrant or by default
⟨true ⊢ ⟨ ⟨bar >= 0 ⊢ true⟩, ⟨bar < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩
error_empty ⟨ ⟨bar >= 0 ⊢ ⟨true⟩⟩, ⟨bar < 0 ⊢ ⟨false⟩⟩ | false ⊢ ∅ ⟩
```
```catala-test-inline
$ catala Interpret_Lcalc -s TestBool --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] bar = ESome 1
[RESULT] foo = ESome true
[RESULT] bar = 1
[RESULT] foo = true
```

2
tests/test_bool/good/test_precedence.catala_en
View File

@ -16,5 +16,5 @@ $ catala Interpret -s TestBool
```catala-test-inline
$ catala Interpret_Lcalc -s TestBool --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] foo = ESome true
[RESULT] foo = true
```

8
tests/test_bool/good/test_xor.catala_en
View File

@ -25,8 +25,8 @@ $ catala Interpret -s TestXor
```catala-test-inline
$ catala Interpret_Lcalc -s TestXor --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] f_xor_f = ESome false
[RESULT] f_xor_t = ESome true
[RESULT] t_xor_f = ESome true
[RESULT] t_xor_t = ESome false
[RESULT] f_xor_f = false
[RESULT] f_xor_t = true
[RESULT] t_xor_f = true
[RESULT] t_xor_t = false
```

14
tests/test_date/good/durations.catala_en
View File

@ -37,11 +37,11 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] m = ESome [11874 days]
[RESULT] m2 = ESome [6 months]
[RESULT] x = ESome 2019-01-01
[RESULT] y = ESome 2002-09-30
[RESULT] z = ESome true
[RESULT] z2 = ESome true
[RESULT] z3 = ESome [5937 days]
[RESULT] m = [11874 days]
[RESULT] m2 = [6 months]
[RESULT] x = 2019-01-01
[RESULT] y = 2002-09-30
[RESULT] z = true
[RESULT] z2 = true
[RESULT] z3 = [5937 days]
```

6
tests/test_date/good/rounding_option_en.catala_en
View File

@ -27,3 +27,9 @@ $ catala Interpret -s Test
[RESULT] Computation successful! Results:
[RESULT] r = true
```
```catala-test-inline
$ catala Interpret_Lcalc -s Test --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] r = true
```

5
tests/test_date/good/rounding_option_fr.catala_fr
View File

@ -27,3 +27,8 @@ $ catala Interpret -s Test
[RESULT] Computation successful! Results:
[RESULT] r = vrai
```
```catala-test-inline
$ catala Interpret_Lcalc -s Test --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] r = vrai
```

6
tests/test_date/good/simple.catala_en
View File

@ -22,7 +22,7 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 2019-01-01
[RESULT] y = ESome 2002-09-30
[RESULT] z = ESome [5937 days]
[RESULT] x = 2019-01-01
[RESULT] y = 2002-09-30
[RESULT] z = [5937 days]
```

7
tests/test_dec/good/infinite_precision.catala_en
View File

@ -29,9 +29,8 @@ $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT]
a =
ESome
0.000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,078,695,580,959,228,473,468…
[RESULT] x = ESome 84.648,665,652,656,896,23
[RESULT] y = ESome -4.368,297,787,053,206,549,8
[RESULT] z = ESome 654,265,429,805,103,220,650,980,650.5…
[RESULT] x = 84.648,665,652,656,896,23
[RESULT] y = -4.368,297,787,053,206,549,8
[RESULT] z = 654,265,429,805,103,220,650,980,650.5…
```

8
tests/test_dec/good/rounding.catala_en
View File

@ -25,8 +25,8 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 84.648,665
[RESULT] x1 = ESome 85.0
[RESULT] y = ESome 4.368,297
[RESULT] y1 = ESome 4.0
[RESULT] x = 84.648,665
[RESULT] x1 = 85.0
[RESULT] y = 4.368,297
[RESULT] y1 = 4.0
```

8
tests/test_dec/good/simple.catala_en
View File

@ -25,8 +25,8 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] k = ESome 0.333,333,333,333,333,333,33…
[RESULT] x = ESome 84.648,665
[RESULT] y = ESome 4.368,297
[RESULT] z = ESome 19.377,955,528,206,987,757…
[RESULT] k = 0.333,333,333,333,333,333,33…
[RESULT] x = 84.648,665
[RESULT] y = 4.368,297
[RESULT] z = 19.377,955,528,206,987,757…
```

4
tests/test_dec/good/zero_after_comma.catala_en
View File

@ -20,6 +20,6 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 4.0
[RESULT] y = ESome 1.04
[RESULT] x = 4.0
[RESULT] y = 1.04
```

3
tests/test_default/bad/empty.catala_en
View File

@ -19,7 +19,8 @@ $ catala Interpret -s A
│ ‾
└─ Article
[ERROR]
This variable evaluated to an empty term (no rule that defined it applied in this situation)
This variable evaluated to an empty term (no rule that defined it applied in this situation):
error_empty ⟨false ⊢ ∅⟩
┌─⯈ tests/test_default/bad/empty.catala_en:6.10-6.11:
└─┐

4
tests/test_default/bad/empty_with_rules.catala_en
View File

@ -15,7 +15,9 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[ERROR]
This variable evaluated to an empty term (no rule that defined it applied in this situation)
This variable evaluated to an empty term (no rule that defined it applied in this situation):
error_empty
⟨ ⟨ ⟨ ⟨1 = 4 ⊢ ⟨1⟩⟩ | 1 = 3 ⊢ ⟨1⟩ ⟩ | 1 = 2 ⊢ ⟨1⟩ ⟩ | false ⊢ ∅ ⟩
┌─⯈ tests/test_default/bad/empty_with_rules.catala_en:5.10-5.11:
└─┐

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

@ -35,21 +35,21 @@ Error during typechecking, incompatible types:
┌─⯈ E
└─⯈ F
Error coming from typechecking the following expression:
While typechecking the following expression:
┌─⯈ tests/test_enum/bad/quick_pattern_2.catala_en:28.23-28.24:
└──┐
28 │ definition y equals x with pattern Case3
│ ‾
└─ Article
Type E coming from expression:
Type E is coming from:
┌─⯈ tests/test_enum/bad/quick_pattern_2.catala_en:17.21-17.22:
└──┐
17 │ context x content E
│ ‾
└─ Article
Type F coming from expression:
Type F is coming from:
┌─⯈ tests/test_enum/bad/quick_pattern_2.catala_en:28.23-28.43:
└──┐
28 │ definition y equals x with pattern Case3

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

@ -25,21 +25,21 @@ Error during typechecking, incompatible types:
┌─⯈ E
└─⯈ F
Error coming from typechecking the following expression:
While typechecking the following expression:
┌─⯈ tests/test_enum/bad/quick_pattern_3.catala_en:18.21-18.22:
└──┐
18 │ definition y equals x with pattern Case3
│ ‾
└─ Article
Type E coming from expression:
Type E is coming from:
┌─⯈ tests/test_enum/bad/quick_pattern_3.catala_en:13.19-13.20:
└──┐
13 │ context x content E
│ ‾
└─ Article
Type F coming from expression:
Type F is coming from:
┌─⯈ tests/test_enum/bad/quick_pattern_3.catala_en:18.21-18.41:
└──┐
18 │ definition y equals x with pattern Case3

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

@ -24,21 +24,21 @@ Error during typechecking, incompatible types:
┌─⯈ E
└─⯈ F
Error coming from typechecking the following expression:
While typechecking the following expression:
┌─⯈ tests/test_enum/bad/quick_pattern_4.catala_en:17.21-17.22:
└──┐
17 │ definition y equals x with pattern Case3
│ ‾
└─ Test
Type E coming from expression:
Type E is coming from:
┌─⯈ tests/test_enum/bad/quick_pattern_4.catala_en:12.19-12.20:
└──┐
12 │ context x content E
│ ‾
└─ Test
Type F coming from expression:
Type F is coming from:
┌─⯈ tests/test_enum/bad/quick_pattern_4.catala_en:17.21-17.41:
└──┐
17 │ definition y equals x with pattern Case3

6
tests/test_enum/good/disambiguated_cases.catala_en
View File

@ -31,7 +31,7 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] e = ESome Case1 ()
[RESULT] f = ESome Case1 2
[RESULT] x = ESome 2
[RESULT] e = Case1 ()
[RESULT] f = Case1 2
[RESULT] x = 2
```

6
tests/test_enum/good/quick_pattern_check.catala_en
View File

@ -26,7 +26,7 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome Case1 2
[RESULT] y = ESome true
[RESULT] z = ESome false
[RESULT] x = Case1 2
[RESULT] y = true
[RESULT] z = false
```

4
tests/test_enum/good/simple.catala_en
View File

@ -25,6 +25,6 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome Case1 2
[RESULT] y = ESome 42
[RESULT] x = Case1 2
[RESULT] y = 42
```

8
tests/test_enum/good/wildcard.catala_en
View File

@ -52,12 +52,12 @@ $ catala Interpret -s Simple_case
```catala-test-inline
$ catala Interpret_Lcalc -s Simple_case_2 --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome Case3 ()
[RESULT] y = ESome 31
[RESULT] x = Case3 ()
[RESULT] y = 31
```
```catala-test-inline
$ catala Interpret_Lcalc -s Simple_case --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome Case1 2
[RESULT] y = ESome 31
[RESULT] x = Case1 2
[RESULT] y = 31
```

4
tests/test_exception/good/double_definition.catala_en
View File

@ -26,7 +26,7 @@ $ catala Scopelang -s Foo
│ ‾‾‾‾‾‾‾‾‾‾‾‾
└─ Foo
let scope Foo (x: integer|internal|output) =
let x : integer = ⟨true ⊢ ⟨ ⟨true ⊢ 1⟩, ⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩⟩
let x : integer = error_empty ⟨ ⟨true ⊢ ⟨1⟩⟩, ⟨true ⊢ ⟨1⟩⟩ | false ⊢ ∅ ⟩
```
In Scopelang we have what looks like conflicting exceptions. But after
@ -52,7 +52,7 @@ $ catala Dcalc -s Foo
└─ Foo
let scope Foo (Foo_in: Foo_in): Foo {x: integer} =
let set x : integer =
error_empty ⟨true ⊢ ⟨ ⟨ ⟨true ⊢ 1⟩ | true ⊢ 1 ⟩ | false ⊢ ∅ ⟩⟩
error_empty ⟨ ⟨ ⟨true ⊢ ⟨1⟩⟩ | true ⊢ ⟨1⟩ ⟩ | false ⊢ ∅ ⟩
in
return { Foo x = x; }
```

4
tests/test_exception/good/duplicate_labels.catala_en
View File

@ -27,6 +27,6 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 0
[RESULT] y = ESome 0
[RESULT] x = 0
[RESULT] y = 0
```

2
tests/test_exception/good/exception.catala_en
View File

@ -20,5 +20,5 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 1
[RESULT] x = 1
```

2
tests/test_exception/good/exceptions_squared.catala_en
View File

@ -24,5 +24,5 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 2
[RESULT] x = 2
```

4
tests/test_exception/good/grouped_exceptions.catala_en
View File

@ -55,6 +55,6 @@ $ catala Interpret -s Benefit
```catala-test-inline
$ catala Interpret_Lcalc -s Benefit --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] benefit = ESome $2,000.00
[RESULT] person = ESome Person { -- age: ESome 26 -- disabled: ESome true }
[RESULT] benefit = $2,000.00
[RESULT] person = Person { -- age: 26 -- disabled: true }
```

32
tests/test_exception/good/groups_of_exceptions.catala_en
View File

@ -29,19 +29,45 @@ scope Foo:
exception intermediate definition x under condition
y = 5
consequence equals 5
declaration scope Test:
f scope Foo
output x content integer
scope Test:
definition f.y equals 2
definition x equals f.x
```
```catala-test-inline
$ catala interpret -s Test
[RESULT] Computation successful! Results:
[RESULT] x = 2
```
```catala-test-inline
$ catala Scopelang
struct Foo = {
x: integer
}
struct Test = {
x: integer
}
let scope Foo (y: integer|input) (x: integer|internal|output) =
let x : integer =
⟨ ⟨ ⟨true ⊢ ⟨ ⟨y = 4 ⊢ 4⟩, ⟨y = 5 ⊢ 5⟩ | false ⊢ ∅ ⟩⟩
| true ⊢ ⟨ ⟨y = 2 ⊢ 2⟩, ⟨y = 3 ⊢ 3⟩ | false ⊢ ∅ ⟩ ⟩
| true ⊢ ⟨ ⟨y = 0 ⊢ 0⟩, ⟨y = 1 ⊢ 1⟩ | false ⊢ ∅ ⟩ ⟩
error_empty
⟨ ⟨ ⟨ ⟨y = 4 ⊢ ⟨4⟩⟩, ⟨y = 5 ⊢ ⟨5⟩⟩ | false ⊢ ∅ ⟩
| true ⊢ ⟨ ⟨y = 2 ⊢ ⟨2⟩⟩, ⟨y = 3 ⊢ ⟨3⟩⟩ | false ⊢ ∅ ⟩ ⟩
| true ⊢ ⟨ ⟨y = 0 ⊢ ⟨0⟩⟩, ⟨y = 1 ⊢ ⟨1⟩⟩ | false ⊢ ∅ ⟩ ⟩
let scope Test (x: integer|internal|output) =
let f.y : integer = error_empty ⟨ ⟨true ⊢ ⟨2⟩⟩ | false ⊢ ∅ ⟩;
call Foo[f];
let x : integer = error_empty ⟨ ⟨true ⊢ ⟨f.x⟩⟩ | false ⊢ ∅ ⟩
```
```catala-test-inline

6
tests/test_exception/good/same_label_two_variables.catala_en
View File

@ -29,7 +29,7 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 0
[RESULT] y = ESome 1
[RESULT] z = ESome 0
[RESULT] x = 0
[RESULT] y = 1
[RESULT] z = 0
```

2
tests/test_exception/good/split_unlabeled_exception.catala_en
View File

@ -22,5 +22,5 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 1
[RESULT] x = 1
```

2
tests/test_exception/good/two_exceptions_same_outcome.catala_en
View File

@ -28,5 +28,5 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 0
[RESULT] x = 0
```

4
tests/test_exception/good/two_unlabeled_exceptions.catala_en
View File

@ -26,6 +26,6 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 1
[RESULT] y = ESome 3
[RESULT] x = 1
[RESULT] y = 3
```

2
tests/test_exception/good/unlabeled_exception.catala_en
View File

@ -19,5 +19,5 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 1
[RESULT] x = 1
```

4
tests/test_exception/good/unsorted_unlabeled_exceptions.catala_en
View File

@ -26,6 +26,6 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome 1
[RESULT] y = ESome 2
[RESULT] x = 1
[RESULT] y = 2
```

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

@ -13,42 +13,42 @@ scope S:
```catala-test-inline
$ catala Lcalc --avoid_exceptions -O --closure_conversion
type eoption = | ENone of unit | ESome of any
type S_in = { x_in: eoption bool; }
type S = { z: eoption integer; }
type S_in = { x_in: bool; }
let topval closure_f : (closure_env, integer) → eoption integer =
type S = { z: integer; }
let topval closure_f : (closure_env, integer) → 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)
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) → ESome if (from_closure_env env).0 then y else - 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))
| ESome arg → arg
let scope S (S_in: S_in {x_in: bool}): S {z: integer} =
let get x : bool = S_in.x_in in
let set f : ((closure_env, integer) → integer * closure_env) =
(closure_f, to_closure_env (x))
in
let set z : eoption integer =
ESome
let set z : integer =
match
(match f with
| ENone _ → ENone _
| ESome f →
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) →
ESome
let code_and_env :
((closure_env, integer) → eoption integer * closure_env) =
((closure_env, integer) → integer * closure_env) =
f
in
code_and_env.0 code_and_env.1 -1)
code_and_env.0 code_and_env.1 -1))
with
| ENone _ → raise NoValueProvided
| ESome z → z
| ESome arg → arg
in
return { S z = z; }

89
tests/test_func/good/closure_conversion_reduce.catala_en
View File

@ -13,35 +13,24 @@ scope S:
```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
let scope S (S_in: S_in {x_in: collection integer}): S {y: integer} =
let get x : collection integer = S_in.x_in in
let set y : integer =
match
(match x with
| ENone _ → ENone _
| ESome y_2 →
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) →
ESome
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)
(λ (potential_max_1: integer) (potential_max_2: integer) →
if potential_max_1 < potential_max_2 then potential_max_1
else potential_max_2)
-1
x))
with
| ENone _ → raise NoValueProvided
| ESome y → y
| ESome arg → arg
in
return { S y = y; }
```
@ -58,39 +47,35 @@ with optimizations on passes.
```catala-test-inline
$ catala Lcalc -s S --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
let scope S (S_in: S_in {x_in: collection integer}): S {y: integer} =
let get x : collection integer = S_in.x_in in
let set y : integer =
match
(handle_default_opt
[ ]
(λ (_: unit) → ESome true)
[
handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) →
match x with
| ENone _1 → ENone _1
| ESome y_2 →
ESome
reduce
(λ (f: eoption integer) (init: eoption integer) →
match init with
| ENone _1 → ENone _1
| ESome y_3 →
match f with
| ENone _1 → ENone _1
| 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))
(λ (potential_max_1: integer) (potential_max_2: integer) →
if
(let potential_max : integer = potential_max_1 in
potential_max)
< let potential_max : integer = potential_max_2 in
potential_max
then
potential_max_1
else potential_max_2)
-1
x)
]
(λ (_: unit) → false)
(λ (_: unit) → ENone ()))
with
| ENone _ → raise NoValueProvided
| ESome y → y
| ESome arg → arg
in
return { S y = y; }
```

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

@ -11,32 +11,29 @@ scope S:
```catala-test-inline
$ catala Lcalc --avoid_exceptions -O --closure_conversion
type eoption = | ENone of unit | ESome of any
type S_in = { x_in: eoption bool; }
type S = {
f: eoption ((closure_env, integer) → eoption integer * closure_env);
}
type S_in = { x_in: bool; }
let topval closure_f : (closure_env, integer) → eoption integer =
type S = { f: ((closure_env, integer) → integer * closure_env); }
let topval closure_f : (closure_env, integer) → 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)
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) → ESome if (from_closure_env env).0 then y else - y))
with
| ENone _ → raise NoValueProvided
| ESome f → f
| ESome arg → arg
let scope S
(S_in: S_in {x_in: eoption bool})
: S {f: eoption ((closure_env, integer) → eoption integer * closure_env)}
(S_in: S_in {x_in: bool})
: S {f: ((closure_env, integer) → 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))
let get x : bool = S_in.x_in in
let set f : ((closure_env, integer) → integer * closure_env) =
(closure_f, to_closure_env (x))
in
return { S f = f; }

57
tests/test_func/good/closure_through_scope.catala_en
View File

@ -19,37 +19,36 @@ scope T:
```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
let scope T (T_in: T_in): T {y: integer} =
let sub_set s.x : bool =
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)
(handle_default_opt [] (λ (_: unit) → true) (λ (_: unit) → ESome false))
with
| ENone _ → raise NoValueProvided
| ESome y → y
| ESome arg → arg
in
let call result : S {f: ((closure_env, integer) → integer * closure_env)}
=
S { S_in x_in = s.x; }
in
let sub_get s.f : ((closure_env, integer) → integer * closure_env) =
result.f
in
let set y : integer =
match
(handle_default_opt
[]
(λ (_: unit) → true)
(λ (_: unit) →
ESome
let code_and_env :
((closure_env, integer) → integer * closure_env) =
s.f
in
code_and_env.0 code_and_env.1 2))
with
| ENone _ → raise NoValueProvided
| ESome arg → arg
in
return { T y = y; }
```
@ -57,5 +56,5 @@ let scope T (T_in: T_in): T {y: eoption integer} =
```catala-test-inline
$ catala Interpret_lcalc -s T --avoid_exceptions -O --closure_conversion
[RESULT] Computation successful! Results:
[RESULT] y = ESome -2
[RESULT] y = -2
```

2
tests/test_func/good/func.catala_en
View File

@ -29,5 +29,5 @@ $ catala Interpret -s R
```catala-test-inline
$ catala Interpret_Lcalc -s R --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] r = ESome 30
[RESULT] r = 30
```

Some files were not shown because too many files have changed in this diff Show More