mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-19 16:28:12 +03:00
Testing and debugging closure conversion (#637)
This commit is contained in:
commit
8a6206363e
11
Makefile
11
Makefile
@ -299,7 +299,8 @@ BRANCH = $(shell git branch --show-current 2>/dev/null || echo master)
|
||||
# its usage.
|
||||
local_tmp_clone = { \
|
||||
rm -rf $1.tmp && \
|
||||
trap "rm -rf $1.tmp" EXIT && \
|
||||
CLEANUP_TMP_GIT_CLONES="$${CLEANUP_TMP_GIT_CLONES}rm -rf $1.tmp; " && \
|
||||
trap "$$CLEANUP_TMP_GIT_CLONES" EXIT && \
|
||||
git clone https://github.com/CatalaLang/$1 \
|
||||
--depth 1 --reference-if-able ../$1 \
|
||||
$1.tmp -b $(BRANCH) || \
|
||||
@ -336,8 +337,12 @@ alltest: dependencies-python
|
||||
bench_ocaml \
|
||||
bench_js \
|
||||
bench_python && \
|
||||
printf "\n# \e[42;30m[ ALL TESTS PASSED ]\e[m \e[32m☺\e[m\n" || \
|
||||
{ printf "\n# \e[41;30m[ TESTS FAILED ]\e[m \e[31m☹\e[m\n" ; exit 1; }
|
||||
printf "\n# Full Catala testsuite:\t\t\e[42;30m ALL TESTS PASSED \e[m\t\t\e[32m☺\e[m\n" || \
|
||||
{ printf "\n# Full Catala testsuite:\t\t\e[41;30m TESTS FAILED \e[m\t\t\e[31m☹\e[m\n" ; exit 1; }
|
||||
|
||||
#> alltest- : Like 'alltest', but skips doc building and is much faster
|
||||
alltest-:
|
||||
@$(MAKE) alltest NODOC=1
|
||||
|
||||
#> clean : Clean build artifacts
|
||||
clean:
|
||||
|
@ -488,7 +488,9 @@ let base_bindings catala_exe catala_flags build_dir include_dirs test_flags =
|
||||
let catala_flags_ocaml =
|
||||
List.filter
|
||||
(function
|
||||
| "--avoid-exceptions" | "-O" | "--optimize" -> true | _ -> false)
|
||||
| "--avoid-exceptions" | "-O" | "--optimize" | "--closure-conversion" ->
|
||||
true
|
||||
| _ -> false)
|
||||
test_flags
|
||||
in
|
||||
let catala_flags_python =
|
||||
|
@ -111,21 +111,9 @@ let get_diff p1 p2 =
|
||||
File.process_out ~check_exit:(fun _ -> ()) cmd (args @ [f1; f2])
|
||||
|
||||
let catala_commands_with_output_flag =
|
||||
[
|
||||
"makefile";
|
||||
"html";
|
||||
"latex";
|
||||
"scopelang";
|
||||
"dcalc";
|
||||
"lcalc";
|
||||
"ocaml";
|
||||
"scalc";
|
||||
"python";
|
||||
"r";
|
||||
"c";
|
||||
]
|
||||
["makefile"; "html"; "latex"; "ocaml"; "python"; "r"; "c"]
|
||||
|
||||
let display ~build_dir ppf t =
|
||||
let display ~build_dir file ppf t =
|
||||
let pfile f =
|
||||
f
|
||||
|> String.remove_prefix ~prefix:(build_dir ^ Filename.dir_sep)
|
||||
@ -135,6 +123,10 @@ let display ~build_dir ppf t =
|
||||
List.filter_map
|
||||
(fun s -> if s = "--directory=" ^ build_dir then None else Some (pfile s))
|
||||
t.command_line
|
||||
|> (function
|
||||
| catala :: cmd :: args ->
|
||||
catala :: cmd :: "-I" :: Filename.dirname file :: args
|
||||
| cl -> cl)
|
||||
|> function
|
||||
| catala :: cmd :: args
|
||||
when List.mem
|
||||
@ -180,7 +172,7 @@ let display_file ~build_dir ppf t =
|
||||
in
|
||||
Format.pp_print_break ppf 0 3;
|
||||
Format.pp_open_vbox ppf 0;
|
||||
Format.pp_print_list (display ~build_dir) ppf tests;
|
||||
Format.pp_print_list (display ~build_dir t.name) ppf tests;
|
||||
Format.pp_close_box ppf ()
|
||||
in
|
||||
if t.successful = t.total then (
|
||||
|
@ -34,7 +34,7 @@ type file = { name : File.t; successful : int; total : int; tests : test list }
|
||||
val write_to : File.t -> file -> unit
|
||||
val read_from : File.t -> file
|
||||
val read_many : File.t -> file list
|
||||
val display : build_dir:File.t -> Format.formatter -> test -> unit
|
||||
val display : build_dir:File.t -> File.t -> Format.formatter -> test -> unit
|
||||
|
||||
val summary : build_dir:File.t -> file list -> bool
|
||||
(** Displays a summary to stdout; returns true if all tests succeeded *)
|
||||
|
@ -76,7 +76,7 @@ let catala_test_command test_flags catala_exe catala_opts args out =
|
||||
let cmd0, flags =
|
||||
match String.lowercase_ascii cmd0, flags, test_flags with
|
||||
| "test-scope", scope_name :: flags, test_flags ->
|
||||
"interpret", (("--scope=" ^ scope_name) :: flags) @ test_flags
|
||||
"interpret", flags @ test_flags @ ["--scope=" ^ scope_name]
|
||||
| "test-scope", [], _ ->
|
||||
out_line out
|
||||
"[INVALID TEST] Invalid test command syntax, the 'test-scope' \
|
||||
@ -126,7 +126,7 @@ let run_catala_test filename cmd program expected out_line =
|
||||
out_line result_line;
|
||||
match Seq.uncons expected with
|
||||
| Some (l, expected) -> success && String.equal result_line l, expected
|
||||
| None -> false, expected)
|
||||
| None -> false, Seq.empty)
|
||||
(true, expected) out_lines
|
||||
in
|
||||
let return_code =
|
||||
@ -142,7 +142,7 @@ let run_catala_test filename cmd program expected out_line =
|
||||
match Seq.uncons expected with
|
||||
| Some (l, expected) when String.equal l line -> success, expected
|
||||
| Some (_, expected) -> false, expected
|
||||
| None -> false, expected
|
||||
| None -> false, Seq.empty
|
||||
in
|
||||
success && Seq.is_empty expected
|
||||
|
||||
@ -171,7 +171,7 @@ let run_tests ~catala_exe ~catala_opts ~test_flags ~report ~out filename =
|
||||
| Some ((l, tok, _), lines) ->
|
||||
push_line l;
|
||||
if tok = L.LINE_BLOCK_END then lines else skip_block lines
|
||||
| None -> lines
|
||||
| None -> Seq.empty
|
||||
in
|
||||
let rec get_block acc lines =
|
||||
let return lines acc =
|
||||
@ -189,7 +189,7 @@ let run_tests ~catala_exe ~catala_opts ~test_flags ~report ~out filename =
|
||||
lines, block, (startpos, endpos)
|
||||
in
|
||||
match Seq.uncons lines with
|
||||
| None -> return lines acc
|
||||
| None -> return Seq.empty acc
|
||||
| Some ((_, L.LINE_BLOCK_END, _), lines) -> return lines acc
|
||||
| Some (li, lines) -> get_block (li :: acc) lines
|
||||
in
|
||||
@ -213,7 +213,7 @@ let run_tests ~catala_exe ~catala_opts ~test_flags ~report ~out filename =
|
||||
"[INVALID TEST] Missing test command, use '$ catala <args>'\n"
|
||||
in
|
||||
rtests := t :: !rtests;
|
||||
None, lines
|
||||
None, Seq.empty
|
||||
| Some ((str, L.LINE_BLOCK_END, _), lines) ->
|
||||
let t =
|
||||
broken_test
|
||||
|
@ -47,6 +47,7 @@ end = struct
|
||||
type nonrec t = t
|
||||
|
||||
let pass k ~avoid_exceptions ~closure_conversion ~monomorphize_types =
|
||||
let avoid_exceptions = avoid_exceptions || closure_conversion in
|
||||
(* Should not affect the call convention or actual interfaces: include,
|
||||
optimize, check_invariants, typed *)
|
||||
!(avoid_exceptions : bool)
|
||||
|
@ -202,15 +202,9 @@ module Passes = struct
|
||||
in
|
||||
let (prg : ty Dcalc.Ast.program) =
|
||||
match typed with
|
||||
| Typed _ -> (
|
||||
| Typed _ ->
|
||||
Message.debug "Typechecking again...";
|
||||
try Typing.program 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)
|
||||
Typing.program ~internal_check:true prg
|
||||
| Untyped _ -> prg
|
||||
| Custom _ -> assert false
|
||||
in
|
||||
@ -269,7 +263,7 @@ module Passes = struct
|
||||
let prg =
|
||||
if not closure_conversion then (
|
||||
Message.debug "Retyping lambda calculus...";
|
||||
Typing.program ~fail_on_any:false prg)
|
||||
Typing.program ~fail_on_any:false ~internal_check:true prg)
|
||||
else (
|
||||
Message.debug "Performing closure conversion...";
|
||||
let prg = Lcalc.Closure_conversion.closure_conversion prg in
|
||||
@ -280,14 +274,17 @@ module Passes = struct
|
||||
else prg
|
||||
in
|
||||
Message.debug "Retyping lambda calculus...";
|
||||
Typing.program ~fail_on_any:false prg)
|
||||
Typing.program ~fail_on_any:false ~internal_check:true prg)
|
||||
in
|
||||
let prg, type_ordering =
|
||||
if monomorphize_types then (
|
||||
Message.debug "Monomorphizing types...";
|
||||
let prg, type_ordering = Lcalc.Monomorphize.program prg in
|
||||
Message.debug "Retyping lambda calculus...";
|
||||
let prg = Typing.program ~fail_on_any:false ~assume_op_types:true prg in
|
||||
let prg =
|
||||
Typing.program ~fail_on_any:false ~assume_op_types:true
|
||||
~internal_check:true prg
|
||||
in
|
||||
prg, type_ordering)
|
||||
else prg, type_ordering
|
||||
in
|
||||
@ -837,10 +834,11 @@ module Commands = struct
|
||||
optimize
|
||||
check_invariants
|
||||
avoid_exceptions
|
||||
closure_conversion
|
||||
ex_scope_opt =
|
||||
let prg, type_ordering =
|
||||
Passes.lcalc options ~includes ~optimize ~check_invariants
|
||||
~avoid_exceptions ~typed:Expr.typed ~closure_conversion:false
|
||||
~avoid_exceptions ~typed:Expr.typed ~closure_conversion
|
||||
~monomorphize_types:false
|
||||
in
|
||||
let output_file, with_output =
|
||||
@ -853,7 +851,7 @@ module Commands = struct
|
||||
(Option.value ~default:"stdout" output_file);
|
||||
let exec_scope = Option.map (get_scope_uid prg.decl_ctx) ex_scope_opt in
|
||||
let hashf =
|
||||
Hash.finalise ~avoid_exceptions ~closure_conversion:false
|
||||
Hash.finalise ~avoid_exceptions ~closure_conversion
|
||||
~monomorphize_types:false
|
||||
in
|
||||
Lcalc.To_ocaml.format_program fmt prg ?exec_scope ~hashf type_ordering
|
||||
@ -870,6 +868,7 @@ module Commands = struct
|
||||
$ Cli.Flags.optimize
|
||||
$ Cli.Flags.check_invariants
|
||||
$ Cli.Flags.avoid_exceptions
|
||||
$ Cli.Flags.closure_conversion
|
||||
$ Cli.Flags.ex_scope_opt)
|
||||
|
||||
let scalc
|
||||
|
@ -19,11 +19,20 @@ open Shared_ast
|
||||
open Ast
|
||||
module D = Dcalc.Ast
|
||||
|
||||
type name_context = { prefix : string; mutable counter : int }
|
||||
|
||||
type 'm ctx = {
|
||||
name_context : string;
|
||||
decl_ctx : decl_ctx;
|
||||
name_context : name_context;
|
||||
globally_bound_vars : ('m expr, typ) Var.Map.t;
|
||||
}
|
||||
|
||||
let new_var ?(pfx = "") name_context =
|
||||
name_context.counter <- name_context.counter + 1;
|
||||
Var.make (pfx ^ name_context.prefix ^ string_of_int name_context.counter)
|
||||
|
||||
let new_context prefix = { prefix; counter = 0 }
|
||||
|
||||
(** Function types will be transformed in this way throughout, including in
|
||||
[decl_ctx] *)
|
||||
let rec translate_type t =
|
||||
@ -52,6 +61,76 @@ let join_vars : ('a, 'x) Var.Map.t -> ('a, 'x) Var.Map.t -> ('a, 'x) Var.Map.t =
|
||||
|
||||
(** {1 Transforming closures}*)
|
||||
|
||||
let build_closure :
|
||||
type m.
|
||||
m ctx ->
|
||||
(m expr Var.t * m mark) list ->
|
||||
m expr boxed ->
|
||||
m expr Var.t array ->
|
||||
typ list ->
|
||||
m mark ->
|
||||
m expr boxed =
|
||||
fun ctx free_vars body args tys m ->
|
||||
(* λ x.t *)
|
||||
let pos = Expr.mark_pos m in
|
||||
let mark_ty ty = Expr.with_ty m ty in
|
||||
let free_vars_types = List.map (fun (_, m) -> Expr.maybe_ty m) free_vars in
|
||||
(* x1, ..., xn *)
|
||||
let code_var = new_var ctx.name_context in
|
||||
(* code *)
|
||||
let closure_env_arg_var = Var.make "env" in
|
||||
let closure_env_var = Var.make "env" in
|
||||
let env_ty = TTuple free_vars_types, pos in
|
||||
(* let env = from_closure_env env in let arg0 = env.0 in ... *)
|
||||
let new_closure_body =
|
||||
Expr.make_let_in closure_env_var env_ty
|
||||
(Expr.eappop
|
||||
~op:(Operator.FromClosureEnv, pos)
|
||||
~tys:[TClosureEnv, pos]
|
||||
~args:[Expr.evar closure_env_arg_var (mark_ty (TClosureEnv, pos))]
|
||||
(mark_ty env_ty))
|
||||
(Expr.make_multiple_let_in
|
||||
(Array.of_list (List.map fst free_vars))
|
||||
free_vars_types
|
||||
(List.mapi
|
||||
(fun i _ ->
|
||||
Expr.make_tupleaccess
|
||||
(Expr.evar closure_env_var (mark_ty env_ty))
|
||||
i (List.length free_vars) pos)
|
||||
free_vars)
|
||||
body pos)
|
||||
pos
|
||||
in
|
||||
(* fun env arg0 ... -> new_closure_body *)
|
||||
let new_closure =
|
||||
Expr.make_abs
|
||||
(Array.append [| closure_env_arg_var |] args)
|
||||
new_closure_body
|
||||
((TClosureEnv, pos) :: tys)
|
||||
pos
|
||||
in
|
||||
let new_closure_ty = Expr.maybe_ty (Mark.get new_closure) in
|
||||
Expr.make_let_in code_var new_closure_ty new_closure
|
||||
(Expr.make_tuple
|
||||
((Bindlib.box_var code_var, mark_ty new_closure_ty)
|
||||
:: [
|
||||
Expr.eappop
|
||||
~op:(Operator.ToClosureEnv, pos)
|
||||
~tys:[TTuple free_vars_types, pos]
|
||||
~args:
|
||||
[
|
||||
Expr.etuple
|
||||
(List.map
|
||||
(fun (extra_var, m) ->
|
||||
Bindlib.box_var extra_var, Expr.with_pos pos m)
|
||||
free_vars)
|
||||
(mark_ty (TTuple free_vars_types, pos));
|
||||
]
|
||||
(mark_ty (TClosureEnv, pos));
|
||||
])
|
||||
m)
|
||||
pos
|
||||
|
||||
(** Returns the expression with closed closures and the set of free variables
|
||||
inside this new expression. Implementation guided by
|
||||
http://gallium.inria.fr/~fpottier/mpri/cours04.pdf#page=10
|
||||
@ -63,44 +142,60 @@ let rec transform_closures_expr :
|
||||
let m = Mark.get e in
|
||||
match Mark.remove e with
|
||||
| EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ | EArray _
|
||||
| ELit _ | EExternal _ | EAssert _ | EFatalError _ | EIfThenElse _
|
||||
| ERaiseEmpty | ECatchEmpty _ ->
|
||||
| ELit _ | EAssert _ | EFatalError _ | EIfThenElse _ | ERaiseEmpty
|
||||
| ECatchEmpty _ ->
|
||||
Expr.map_gather ~acc:Var.Map.empty ~join:join_vars
|
||||
~f:(transform_closures_expr ctx)
|
||||
e
|
||||
| (EVar _ | EExternal _) as e -> (
|
||||
let body, (free_vars, fty) =
|
||||
match e with
|
||||
| EVar v -> (
|
||||
( Bindlib.box_var v,
|
||||
match Var.Map.find_opt v ctx.globally_bound_vars with
|
||||
| None -> Var.Map.singleton v m, (Bindlib.box_var v, m)
|
||||
| Some (TArrow (targs, tret), _) ->
|
||||
| None -> Var.Map.singleton v m, None
|
||||
| Some ((TArrow (targs, tret), _) as fty) ->
|
||||
Var.Map.empty, Some (targs, tret, fty)
|
||||
| Some _ -> Var.Map.empty, None ))
|
||||
| EExternal { name = External_value td, _ } as e ->
|
||||
( Bindlib.box e,
|
||||
( Var.Map.empty,
|
||||
match TopdefName.Map.find td ctx.decl_ctx.ctx_topdefs with
|
||||
| (TArrow (targs, tret), _) as fty -> Some (targs, tret, fty)
|
||||
| _ -> None ) )
|
||||
| EExternal { name = External_scope s, pos } ->
|
||||
let fty =
|
||||
let si = ScopeName.Map.find s ctx.decl_ctx.ctx_scopes in
|
||||
let t_in = TStruct si.in_struct_name, pos in
|
||||
let t_out = TStruct si.out_struct_name, pos in
|
||||
[t_in], t_out, (TArrow ([t_in], t_out), pos)
|
||||
in
|
||||
Bindlib.box e, (Var.Map.empty, Some fty)
|
||||
| _ -> assert false
|
||||
in
|
||||
match fty with
|
||||
| None -> free_vars, (body, m)
|
||||
| Some (targs, tret, fty) ->
|
||||
(* 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 args =
|
||||
Array.init (List.length targs) (fun i ->
|
||||
Var.make ("x" ^ string_of_int i))
|
||||
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 ~f:(Expr.rebox e) ~args:arg_vars ~tys:targs
|
||||
(Expr.with_ty m tret)))
|
||||
targs m
|
||||
let closure =
|
||||
let body =
|
||||
Expr.eapp
|
||||
~f:(body, Expr.with_ty m fty)
|
||||
~args:arg_vars ~tys:targs (Expr.with_ty m tret)
|
||||
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 (Expr.maybe_ty m) ctx.globally_bound_vars;
|
||||
}
|
||||
build_closure ctx [] body args targs m
|
||||
in
|
||||
Bindlib.box_apply (transform_closures_expr ctx) (Expr.Box.lift e)
|
||||
in
|
||||
Bindlib.unbox boxed
|
||||
| Some _ -> Var.Map.empty, (Bindlib.box_var v, m))
|
||||
Var.Map.empty, closure)
|
||||
| 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,
|
||||
@ -147,92 +242,18 @@ let rec transform_closures_expr :
|
||||
~f:(Expr.eabs new_binder (List.map translate_type tys) e1_pos)
|
||||
~args:new_args ~tys m )
|
||||
| EAbs { binder; tys } ->
|
||||
(* λ x.t *)
|
||||
let binder_pos = Expr.mark_pos m in
|
||||
let mark_ty ty = Expr.with_ty m ty in
|
||||
(* Converting the closure. *)
|
||||
let vars, body = Bindlib.unmbind binder in
|
||||
(* t *)
|
||||
let body_vars, new_body = (transform_closures_expr ctx) body in
|
||||
let free_vars, body = (transform_closures_expr ctx) body in
|
||||
(* [[t]] *)
|
||||
let extra_vars =
|
||||
Array.fold_left (fun m v -> Var.Map.remove v m) body_vars vars
|
||||
let free_vars =
|
||||
Array.fold_left (fun m v -> Var.Map.remove v m) free_vars vars
|
||||
in
|
||||
let extra_vars_list = Var.Map.bindings extra_vars in
|
||||
let extra_vars_types =
|
||||
List.map (fun (_, m) -> Expr.maybe_ty m) extra_vars_list
|
||||
in
|
||||
(* x1, ..., xn *)
|
||||
let code_var = Var.make ctx.name_context in
|
||||
(* code *)
|
||||
let closure_env_arg_var = Var.make "env" in
|
||||
let closure_env_var = Var.make "env" in
|
||||
let env_ty = TTuple extra_vars_types, binder_pos in
|
||||
(* let env = from_closure_env env in let arg0 = env.0 in ... *)
|
||||
let new_closure_body =
|
||||
Expr.make_let_in closure_env_var env_ty
|
||||
(Expr.eappop
|
||||
~op:(Operator.FromClosureEnv, binder_pos)
|
||||
~tys:[TClosureEnv, binder_pos]
|
||||
~args:
|
||||
[Expr.evar closure_env_arg_var (mark_ty (TClosureEnv, binder_pos))]
|
||||
(mark_ty env_ty))
|
||||
(Expr.make_multiple_let_in
|
||||
(Array.of_list (List.map fst extra_vars_list))
|
||||
extra_vars_types
|
||||
(List.mapi
|
||||
(fun i _ ->
|
||||
Expr.make_tupleaccess
|
||||
(Expr.evar closure_env_var (mark_ty env_ty))
|
||||
i
|
||||
(List.length extra_vars_list)
|
||||
binder_pos)
|
||||
extra_vars_list)
|
||||
new_body binder_pos)
|
||||
binder_pos
|
||||
in
|
||||
(* fun env arg0 ... -> new_closure_body *)
|
||||
let new_closure =
|
||||
Expr.make_abs
|
||||
(Array.append [| closure_env_arg_var |] vars)
|
||||
new_closure_body
|
||||
((TClosureEnv, binder_pos) :: tys)
|
||||
(Expr.pos e)
|
||||
in
|
||||
let new_closure_ty = Expr.maybe_ty (Mark.get new_closure) in
|
||||
( extra_vars,
|
||||
Expr.make_let_in code_var new_closure_ty new_closure
|
||||
(Expr.make_tuple
|
||||
((Bindlib.box_var code_var, mark_ty new_closure_ty)
|
||||
:: [
|
||||
Expr.eappop
|
||||
~op:(Operator.ToClosureEnv, binder_pos)
|
||||
~tys:
|
||||
[
|
||||
( (if extra_vars_list = [] then TLit TUnit
|
||||
else TTuple extra_vars_types),
|
||||
binder_pos );
|
||||
]
|
||||
~args:
|
||||
[
|
||||
(if extra_vars_list = [] then
|
||||
Expr.elit LUnit (mark_ty (TLit TUnit, binder_pos))
|
||||
else
|
||||
Expr.etuple
|
||||
(List.map
|
||||
(fun (extra_var, m) ->
|
||||
( Bindlib.box_var extra_var,
|
||||
Expr.with_pos binder_pos m ))
|
||||
extra_vars_list)
|
||||
(mark_ty (TTuple extra_vars_types, binder_pos)));
|
||||
]
|
||||
(mark_ty (TClosureEnv, binder_pos));
|
||||
])
|
||||
m)
|
||||
(Expr.pos e) )
|
||||
free_vars, build_closure ctx (Var.Map.bindings free_vars) body vars tys m
|
||||
| EAppOp
|
||||
{
|
||||
op = ((HandleDefaultOpt | Fold | Map | Filter | Reduce), _) as op;
|
||||
op = ((HandleDefaultOpt | Fold | Map | Map2 | Filter | Reduce), _) as op;
|
||||
tys;
|
||||
args;
|
||||
} ->
|
||||
@ -318,10 +339,7 @@ let rec transform_closures_expr :
|
||||
pos)
|
||||
pos
|
||||
in
|
||||
( free_vars,
|
||||
Expr.make_let_in code_env_var
|
||||
(TAny, Expr.pos e)
|
||||
new_e1 call_expr (Expr.pos e) )
|
||||
free_vars, Expr.make_let_in code_env_var (TAny, pos) new_e1 call_expr pos
|
||||
| _ -> .
|
||||
|
||||
let transform_closures_scope_let ctx scope_body_expr =
|
||||
@ -329,7 +347,7 @@ let transform_closures_scope_let ctx scope_body_expr =
|
||||
~f:(fun var_next scope_let ->
|
||||
let _free_vars, new_scope_let_expr =
|
||||
(transform_closures_expr
|
||||
{ ctx with name_context = Bindlib.name_of var_next })
|
||||
{ ctx with name_context = new_context (Bindlib.name_of var_next) })
|
||||
scope_let.scope_let_expr
|
||||
in
|
||||
( var_next,
|
||||
@ -360,7 +378,8 @@ let transform_closures_program (p : 'm program) : 'm program Bindlib.box =
|
||||
in
|
||||
let ctx =
|
||||
{
|
||||
name_context = Mark.remove (ScopeName.get_info name);
|
||||
decl_ctx = p.decl_ctx;
|
||||
name_context = new_context (Mark.remove (ScopeName.get_info name));
|
||||
globally_bound_vars = toplevel_vars;
|
||||
}
|
||||
in
|
||||
@ -387,7 +406,9 @@ let transform_closures_program (p : 'm program) : 'm program Bindlib.box =
|
||||
let v, expr = Bindlib.unmbind binder in
|
||||
let ctx =
|
||||
{
|
||||
name_context = Mark.remove (TopdefName.get_info name);
|
||||
decl_ctx = p.decl_ctx;
|
||||
name_context =
|
||||
new_context (Mark.remove (TopdefName.get_info name));
|
||||
globally_bound_vars = toplevel_vars;
|
||||
}
|
||||
in
|
||||
@ -401,7 +422,9 @@ let transform_closures_program (p : 'm program) : 'm program Bindlib.box =
|
||||
| Topdef (name, ty, expr) ->
|
||||
let ctx =
|
||||
{
|
||||
name_context = Mark.remove (TopdefName.get_info name);
|
||||
decl_ctx = p.decl_ctx;
|
||||
name_context =
|
||||
new_context (Mark.remove (TopdefName.get_info name));
|
||||
globally_bound_vars = toplevel_vars;
|
||||
}
|
||||
in
|
||||
@ -462,7 +485,7 @@ type 'm hoisted_closure = {
|
||||
}
|
||||
|
||||
let rec hoist_closures_expr :
|
||||
type m. string -> m expr -> m hoisted_closure list * m expr boxed =
|
||||
type m. name_context -> m expr -> m hoisted_closure list * m expr boxed =
|
||||
fun name_context e ->
|
||||
let m = Mark.get e in
|
||||
match Mark.remove e with
|
||||
@ -541,7 +564,7 @@ let rec hoist_closures_expr :
|
||||
collected_closures, Expr.eappop ~op ~args:new_args ~tys (Mark.get e)
|
||||
| EAbs { tys; _ } ->
|
||||
(* this is the closure we want to hoist *)
|
||||
let closure_var = Var.make ("closure_" ^ name_context) in
|
||||
let closure_var = new_var ~pfx:"closure_" name_context in
|
||||
(* TODO: This will end up as a toplevel name. However for now we assume
|
||||
toplevel names are unique, but this breaks this assertions and can lead
|
||||
to name wrangling in the backends. We need to have a better system for
|
||||
@ -555,14 +578,14 @@ let rec hoist_closures_expr :
|
||||
| EArray _ | ELit _ | EAssert _ | EFatalError _ | EAppOp _ | EIfThenElse _
|
||||
| ERaiseEmpty | ECatchEmpty _ | EVar _ ->
|
||||
Expr.map_gather ~acc:[] ~join:( @ ) ~f:(hoist_closures_expr name_context) e
|
||||
| EExternal _ -> failwith "unimplemented"
|
||||
| EExternal { name } -> [], Expr.box (EExternal { name }, m)
|
||||
| _ -> .
|
||||
|
||||
let hoist_closures_scope_let name_context scope_body_expr =
|
||||
BoundList.fold_right
|
||||
~f:(fun scope_let var_next (hoisted_closures, next_scope_lets) ->
|
||||
let new_hoisted_closures, new_scope_let_expr =
|
||||
(hoist_closures_expr (Bindlib.name_of var_next))
|
||||
(hoist_closures_expr (new_context (Bindlib.name_of var_next)))
|
||||
scope_let.scope_let_expr
|
||||
in
|
||||
( new_hoisted_closures @ hoisted_closures,
|
||||
@ -599,7 +622,7 @@ let rec hoist_closures_code_item_list
|
||||
in
|
||||
let new_hoisted_closures, new_scope_lets =
|
||||
hoist_closures_scope_let
|
||||
(fst (ScopeName.get_info name))
|
||||
(new_context (fst (ScopeName.get_info name)))
|
||||
scope_body_expr
|
||||
in
|
||||
let new_scope_body_expr =
|
||||
@ -613,7 +636,9 @@ let rec hoist_closures_code_item_list
|
||||
| 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
|
||||
hoist_closures_expr
|
||||
(new_context (Mark.remove (TopdefName.get_info name)))
|
||||
expr
|
||||
in
|
||||
let new_binder = Expr.bind v new_expr in
|
||||
( new_hoisted_closures,
|
||||
@ -622,7 +647,9 @@ let rec hoist_closures_code_item_list
|
||||
(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
|
||||
hoist_closures_expr
|
||||
(new_context (Mark.remove (TopdefName.get_info name)))
|
||||
expr
|
||||
in
|
||||
( new_hoisted_closures,
|
||||
Bindlib.box_apply
|
||||
@ -674,6 +701,4 @@ let hoist_closures_program (p : 'm program) : 'm program Bindlib.box =
|
||||
let closure_conversion (p : 'm program) : 'm program =
|
||||
let new_p = transform_closures_program p in
|
||||
let new_p = hoist_closures_program (Bindlib.unbox new_p) in
|
||||
(* FIXME: either fix the types of the marks, or remove the types annotations
|
||||
during the main processing (rather than requiring a new traversal) *)
|
||||
Bindlib.unbox new_p
|
||||
|
@ -219,6 +219,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit =
|
||||
in
|
||||
match Mark.remove typ with
|
||||
| TLit l -> Format.fprintf fmt "%a" Print.tlit l
|
||||
| TTuple [] -> Format.fprintf fmt "unit"
|
||||
| TTuple ts ->
|
||||
Format.fprintf fmt "@[<hov 2>(%a)@]"
|
||||
(Format.pp_print_list
|
||||
@ -239,7 +240,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit =
|
||||
(t1 @ [t2])
|
||||
| TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ_with_parens t1
|
||||
| TAny -> Format.fprintf fmt "_"
|
||||
| TClosureEnv -> failwith "unimplemented!"
|
||||
| TClosureEnv -> Format.fprintf fmt "Obj.t"
|
||||
|
||||
let format_var_str (fmt : Format.formatter) (v : string) : unit =
|
||||
let lowercase_name = String.to_snake_case (String.to_ascii v) in
|
||||
|
@ -223,11 +223,11 @@ type typ = naked_typ Mark.pos
|
||||
|
||||
and naked_typ =
|
||||
| TLit of typ_lit
|
||||
| TArrow of typ list * typ
|
||||
| TTuple of typ list
|
||||
| TStruct of StructName.t
|
||||
| TEnum of EnumName.t
|
||||
| TOption of typ
|
||||
| TArrow of typ list * typ
|
||||
| TArray of typ
|
||||
| TDefault of typ
|
||||
| TAny
|
||||
|
@ -566,7 +566,11 @@ let rec runtime_to_val :
|
||||
let e = runtime_to_val eval_expr ctx m ty (Obj.field o 0) in
|
||||
EInj { name = Expr.option_enum; cons = Expr.some_constr; e }, m
|
||||
| _ -> assert false)
|
||||
| TClosureEnv -> assert false
|
||||
| TClosureEnv ->
|
||||
(* By construction, a closure environment can only be consumed from the same
|
||||
scope where it was built (compiled or not) ; for this reason, we can
|
||||
safely avoid converting in depth here *)
|
||||
Obj.obj o, m
|
||||
| TArray ty ->
|
||||
( EArray
|
||||
(List.map
|
||||
@ -656,6 +660,11 @@ and val_to_runtime :
|
||||
in
|
||||
curry [] targs
|
||||
| TDefault ty, _ -> val_to_runtime eval_expr ctx ty v
|
||||
| TClosureEnv, v ->
|
||||
(* By construction, a closure environment can only be consumed from the same
|
||||
scope where it was built (compiled or not) ; for this reason, we can
|
||||
safely avoid converting in depth here *)
|
||||
Obj.repr v
|
||||
| _ ->
|
||||
Message.error ~internal:true
|
||||
"Could not convert value of type %a@ to@ runtime:@ %a" (Print.typ ctx) ty
|
||||
|
@ -102,7 +102,7 @@ let rec typ_gen
|
||||
Format.pp_open_hvbox fmt 2;
|
||||
pp_color_string (List.hd colors) fmt "(";
|
||||
(Format.pp_print_list
|
||||
~pp_sep:(fun fmt () -> Format.fprintf fmt " %a@ " op_style "*")
|
||||
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " op_style ",")
|
||||
(typ ~colors:(List.tl colors)))
|
||||
fmt ts;
|
||||
Format.pp_close_box fmt ();
|
||||
@ -1113,6 +1113,8 @@ module UserFacing = struct
|
||||
~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ")
|
||||
(value ~fallback lang))
|
||||
l
|
||||
| ETuple [(EAbs { tys = (TClosureEnv, _) :: _; _ }, _); _] ->
|
||||
Format.pp_print_string ppf "<function>"
|
||||
| ETuple l ->
|
||||
Format.fprintf ppf "@[<hv 2>(@,@[<hov>%a@]@;<0 -2>)@]"
|
||||
(Format.pp_print_list
|
||||
|
@ -1103,6 +1103,25 @@ let program ?fail_on_any ?assume_op_types prg =
|
||||
};
|
||||
}
|
||||
|
||||
let program ?fail_on_any ?assume_op_types prg =
|
||||
Message.with_delayed_errors (fun () ->
|
||||
program ?fail_on_any ?assume_op_types prg)
|
||||
let program ?fail_on_any ?assume_op_types ?(internal_check = false) prg =
|
||||
let wrap =
|
||||
if internal_check then (fun f ->
|
||||
try Message.with_delayed_errors f
|
||||
with (Message.CompilerError _ | Message.CompilerErrors _) as exc ->
|
||||
let bt = Printexc.get_raw_backtrace () in
|
||||
let err =
|
||||
match exc with
|
||||
| Message.CompilerError err ->
|
||||
Message.CompilerError (Message.Content.to_internal_error err)
|
||||
| Message.CompilerErrors errs ->
|
||||
Message.CompilerErrors
|
||||
(List.map Message.Content.to_internal_error errs)
|
||||
| _ -> assert false
|
||||
in
|
||||
Message.debug "Faulty intermediate program:@ %a"
|
||||
(Print.program ~debug:true)
|
||||
prg;
|
||||
Printexc.raise_with_backtrace err bt)
|
||||
else fun f -> Message.with_delayed_errors f
|
||||
in
|
||||
wrap @@ fun () -> program ?fail_on_any ?assume_op_types prg
|
||||
|
@ -97,11 +97,15 @@ val check_expr :
|
||||
val program :
|
||||
?fail_on_any:bool ->
|
||||
?assume_op_types:bool ->
|
||||
?internal_check:bool ->
|
||||
('a, 'm) gexpr program ->
|
||||
('a, typed) gexpr program
|
||||
(** Typing on whole programs (as defined in Shared_ast.program, i.e. for the
|
||||
later dcalc/lcalc stages.
|
||||
later dcalc/lcalc stages).
|
||||
|
||||
Any existing type annotations are checked for unification. Use
|
||||
[Program.untype] to remove them beforehand if this is not the desired
|
||||
behaviour. *)
|
||||
behaviour.
|
||||
|
||||
If [internal_check] is set to [true], typing errors will be marked as
|
||||
internal, and the faulty program will be printed if '--debug' is set. *)
|
||||
|
@ -884,6 +884,8 @@ module Oper = struct
|
||||
let o_eq_dur_dur pos d1 d2 = equal_periods pos d1 d2
|
||||
let o_eq_dat_dat d1 d2 = Dates_calc.Dates.compare_dates d1 d2 = 0
|
||||
let o_fold = Array.fold_left
|
||||
let o_toclosureenv = Obj.repr
|
||||
let o_fromclosureenv = Obj.obj
|
||||
end
|
||||
|
||||
include Oper
|
||||
|
@ -432,6 +432,8 @@ module Oper : sig
|
||||
val o_eq_dur_dur : source_position -> duration -> duration -> bool
|
||||
val o_eq_dat_dat : date -> date -> bool
|
||||
val o_fold : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
|
||||
val o_toclosureenv : 'a -> Obj.t
|
||||
val o_fromclosureenv : Obj.t -> 'a
|
||||
end
|
||||
|
||||
include module type of Oper
|
||||
|
@ -76,14 +76,14 @@ let scope S (x: integer|internal|output) =
|
||||
10.
|
||||
map (λ (i: integer) → to_rat i) [1; 2; 3])
|
||||
= 3.;
|
||||
assert (let weights : list of (integer * decimal) =
|
||||
assert (let weights : list of (integer, decimal) =
|
||||
map (λ (i: integer) →
|
||||
(i, let i1 : integer = i in
|
||||
to_rat ((2 - i1) * (2 - i1))))
|
||||
[1; 2; 3]
|
||||
in
|
||||
reduce
|
||||
(λ (x1: (integer * decimal)) (x2: (integer * decimal)) →
|
||||
(λ (x1: (integer, decimal)) (x2: (integer, decimal)) →
|
||||
if x1.1 < x2.1 then x1 else x2)
|
||||
let i : integer = 42 in
|
||||
(i, let i1 : integer = i in
|
||||
|
@ -29,15 +29,81 @@ type Eoption = | ENone of unit | ESome of any
|
||||
type S_in = { x_in: bool; }
|
||||
type S = { z: integer; }
|
||||
|
||||
let topval closure_f : (closure_env, integer) → integer =
|
||||
let topval closure_f1 : (closure_env, integer) → integer =
|
||||
λ (env: closure_env) (y: integer) →
|
||||
if (from_closure_env env).0 then y else - y
|
||||
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))
|
||||
let set f : ((closure_env, integer) → integer, closure_env) =
|
||||
(closure_f1, to_closure_env (x))
|
||||
in
|
||||
let set z : integer = f.0 f.1 -1 in
|
||||
return { S z = z; }
|
||||
|
||||
```
|
||||
|
||||
|
||||
```catala
|
||||
declaration scope S2:
|
||||
output dummy content boolean
|
||||
input output cfun2 content decimal depends on x content integer
|
||||
|
||||
scope S2:
|
||||
definition dummy equals false
|
||||
|
||||
declaration scope S2Use:
|
||||
internal fun content decimal depends on y content integer
|
||||
output o content (S2, S2)
|
||||
|
||||
declaration fun2 content decimal depends on y content integer equals y / 3
|
||||
|
||||
scope S2Use:
|
||||
definition fun of y equals y / 2
|
||||
definition o equals
|
||||
(output of S2 with { -- cfun2: fun },
|
||||
output of S2 with { -- cfun2: fun2 })
|
||||
```
|
||||
|
||||
```catala-test-inline
|
||||
$ catala Lcalc --avoid-exceptions -O --closure-conversion -s S2Use
|
||||
let scope S2Use
|
||||
(S2Use_in: S2Use_in)
|
||||
: S2Use {
|
||||
o:
|
||||
(S2 {
|
||||
dummy: bool;
|
||||
cfun2: ((closure_env, integer) → decimal, closure_env)
|
||||
},
|
||||
S2 {
|
||||
dummy: bool;
|
||||
cfun2: ((closure_env, integer) → decimal, closure_env)
|
||||
})
|
||||
}
|
||||
=
|
||||
let set fun : ((closure_env, integer) → decimal, closure_env) =
|
||||
(closure_fun1, to_closure_env ())
|
||||
in
|
||||
let set o :
|
||||
(S2 {
|
||||
dummy: bool;
|
||||
cfun2: ((closure_env, integer) → decimal, closure_env)
|
||||
},
|
||||
S2 {
|
||||
dummy: bool;
|
||||
cfun2: ((closure_env, integer) → decimal, closure_env)
|
||||
}) =
|
||||
(let result : S2 = S2 { S2_in cfun2_in = fun; } in
|
||||
{ S2
|
||||
dummy = result.dummy;
|
||||
cfun2 = (closure_o1, to_closure_env (result));
|
||||
},
|
||||
let result : S2 =
|
||||
S2 { S2_in cfun2_in = (closure_o3, to_closure_env ()); }
|
||||
in
|
||||
{ S2
|
||||
dummy = result.dummy;
|
||||
cfun2 = (closure_o2, to_closure_env (result));
|
||||
})
|
||||
in
|
||||
return { S2Use o = o; }
|
||||
```
|
||||
|
@ -29,7 +29,7 @@ let scope S (S_in: S_in {x_in: list of integer}): S {y: integer} =
|
||||
let get x : list of integer = S_in.x_in in
|
||||
let set y : integer =
|
||||
(reduce
|
||||
(λ (x1: (integer * integer)) (x2: (integer * integer)) →
|
||||
(λ (x1: (integer, integer)) (x2: (integer, integer)) →
|
||||
if x1.1 < x2.1 then x1 else x2)
|
||||
(-1, -1)
|
||||
map (λ (potential_max: integer) → (potential_max, potential_max)) x).0
|
||||
@ -60,7 +60,7 @@ let scope S (S_in: S_in {x_in: list of integer}): S {y: integer} =
|
||||
(λ () → true)
|
||||
(λ () →
|
||||
ESome
|
||||
(let weights : list of (integer * integer) =
|
||||
(let weights : list of (integer, integer) =
|
||||
map (λ (potential_max: integer) →
|
||||
(potential_max,
|
||||
let potential_max1 : integer = potential_max in
|
||||
@ -68,7 +68,7 @@ let scope S (S_in: S_in {x_in: list of integer}): S {y: integer} =
|
||||
x
|
||||
in
|
||||
reduce
|
||||
(λ (x1: (integer * integer)) (x2: (integer * integer)) →
|
||||
(λ (x1: (integer, integer)) (x2: (integer, integer)) →
|
||||
if x1.1 < x2.1 then x1 else x2)
|
||||
let potential_max : integer = -1 in
|
||||
(potential_max,
|
||||
|
@ -25,18 +25,18 @@ $ catala Typecheck --check-invariants
|
||||
$ catala Lcalc --avoid-exceptions -O --closure-conversion
|
||||
type Eoption = | ENone of unit | ESome of any
|
||||
type S_in = { x_in: bool; }
|
||||
type S = { f: ((closure_env, integer) → integer * closure_env); }
|
||||
type S = { f: ((closure_env, integer) → integer, closure_env); }
|
||||
|
||||
let topval closure_f : (closure_env, integer) → integer =
|
||||
let topval closure_f1 : (closure_env, integer) → integer =
|
||||
λ (env: closure_env) (y: integer) →
|
||||
if (from_closure_env env).0 then y else - y
|
||||
let scope S
|
||||
(S_in: S_in {x_in: bool})
|
||||
: S {f: ((closure_env, integer) → integer * closure_env)}
|
||||
: S {f: ((closure_env, integer) → integer, closure_env)}
|
||||
=
|
||||
let get x : bool = S_in.x_in in
|
||||
let set f : ((closure_env, integer) → integer * closure_env) =
|
||||
(closure_f, to_closure_env (x))
|
||||
let set f : ((closure_env, integer) → integer, closure_env) =
|
||||
(closure_f1, to_closure_env (x))
|
||||
in
|
||||
return { S f = f; }
|
||||
|
||||
|
@ -32,11 +32,11 @@ $ catala Typecheck --check-invariants
|
||||
```catala-test-inline
|
||||
$ catala Lcalc -s T --avoid-exceptions -O --closure-conversion
|
||||
let scope T (T_in: T_in): T {y: integer} =
|
||||
let set s : S {f: ((closure_env, integer) → integer * closure_env)} =
|
||||
{ S f = (closure_s, to_closure_env ()); }
|
||||
let set s : S {f: ((closure_env, integer) → integer, closure_env)} =
|
||||
{ S f = (closure_s1, to_closure_env ()); }
|
||||
in
|
||||
let set y : integer =
|
||||
let code_and_env : ((closure_env, integer) → integer * closure_env) =
|
||||
let code_and_env : ((closure_env, integer) → integer, closure_env) =
|
||||
s.f
|
||||
in
|
||||
code_and_env.0 code_and_env.1 2
|
||||
|
@ -56,72 +56,72 @@ $ catala Typecheck --check-invariants
|
||||
$ catala Lcalc --avoid-exceptions -O --closure-conversion
|
||||
type Eoption = | ENone of unit | ESome of any
|
||||
type Result = {
|
||||
r: ((closure_env, integer) → integer * closure_env);
|
||||
r: ((closure_env, integer) → integer, closure_env);
|
||||
q: integer;
|
||||
}
|
||||
type SubFoo1_in = { x_in: integer; }
|
||||
type SubFoo1 = {
|
||||
x: integer;
|
||||
y: ((closure_env, integer) → integer * closure_env);
|
||||
y: ((closure_env, integer) → integer, closure_env);
|
||||
}
|
||||
type SubFoo2_in = { x1_in: integer; x2_in: integer; }
|
||||
type SubFoo2 = {
|
||||
x1: integer;
|
||||
y: ((closure_env, integer) → integer * closure_env);
|
||||
y: ((closure_env, integer) → integer, closure_env);
|
||||
}
|
||||
type Foo_in = { b_in: ((closure_env, unit) → eoption bool * closure_env); }
|
||||
type Foo_in = { b_in: ((closure_env, unit) → eoption bool, closure_env); }
|
||||
type Foo = { z: integer; }
|
||||
|
||||
let topval closure_y : (closure_env, integer) → integer =
|
||||
let topval closure_y1 : (closure_env, integer) → integer =
|
||||
λ (env: closure_env) (z: integer) →
|
||||
(from_closure_env env).0 + z
|
||||
let scope SubFoo1
|
||||
(SubFoo1_in: SubFoo1_in {x_in: integer})
|
||||
: SubFoo1 {
|
||||
x: integer;
|
||||
y: ((closure_env, integer) → integer * closure_env)
|
||||
y: ((closure_env, integer) → integer, closure_env)
|
||||
}
|
||||
=
|
||||
let get x : integer = SubFoo1_in.x_in in
|
||||
let set y : ((closure_env, integer) → integer * closure_env) =
|
||||
(closure_y, to_closure_env (x))
|
||||
let set y : ((closure_env, integer) → integer, closure_env) =
|
||||
(closure_y1, to_closure_env (x))
|
||||
in
|
||||
return { SubFoo1 x = x; y = y; }
|
||||
let topval closure_y : (closure_env, integer) → integer =
|
||||
let topval closure_y1 : (closure_env, integer) → integer =
|
||||
λ (env: closure_env) (z: integer) →
|
||||
let env1 : (integer * integer) = from_closure_env env in
|
||||
let env1 : (integer, integer) = from_closure_env env in
|
||||
((env1.1 + env1.0 + z))
|
||||
let scope SubFoo2
|
||||
(SubFoo2_in: SubFoo2_in {x1_in: integer; x2_in: integer})
|
||||
: SubFoo2 {
|
||||
x1: integer;
|
||||
y: ((closure_env, integer) → integer * closure_env)
|
||||
y: ((closure_env, integer) → integer, closure_env)
|
||||
}
|
||||
=
|
||||
let get x1 : integer = SubFoo2_in.x1_in in
|
||||
let get x2 : integer = SubFoo2_in.x2_in in
|
||||
let set y : ((closure_env, integer) → integer * closure_env) =
|
||||
(closure_y, to_closure_env (x2, x1))
|
||||
let set y : ((closure_env, integer) → integer, closure_env) =
|
||||
(closure_y1, to_closure_env (x2, x1))
|
||||
in
|
||||
return { SubFoo2 x1 = x1; y = y; }
|
||||
let topval closure_r : (closure_env, integer) → integer =
|
||||
let topval closure_r2 : (closure_env, integer) → integer =
|
||||
λ (env: closure_env) (param0: integer) →
|
||||
let code_and_env : ((closure_env, integer) → integer * closure_env) =
|
||||
let code_and_env : ((closure_env, integer) → integer, closure_env) =
|
||||
(from_closure_env env).0.y
|
||||
in
|
||||
code_and_env.0 code_and_env.1 param0
|
||||
let topval closure_r : (closure_env, integer) → integer =
|
||||
let topval closure_r1 : (closure_env, integer) → integer =
|
||||
λ (env: closure_env) (param0: integer) →
|
||||
let code_and_env : ((closure_env, integer) → integer * closure_env) =
|
||||
let code_and_env : ((closure_env, integer) → integer, closure_env) =
|
||||
(from_closure_env env).0.y
|
||||
in
|
||||
code_and_env.0 code_and_env.1 param0
|
||||
let scope Foo
|
||||
(Foo_in:
|
||||
Foo_in {b_in: ((closure_env, unit) → eoption bool * closure_env)})
|
||||
Foo_in {b_in: ((closure_env, unit) → eoption bool, closure_env)})
|
||||
: Foo {z: integer}
|
||||
=
|
||||
let get b : ((closure_env, unit) → eoption bool * closure_env) =
|
||||
let get b : ((closure_env, unit) → eoption bool, closure_env) =
|
||||
Foo_in.b_in
|
||||
in
|
||||
let set b : bool =
|
||||
@ -133,13 +133,13 @@ let scope Foo
|
||||
in
|
||||
let set r :
|
||||
Result {
|
||||
r: ((closure_env, integer) → integer * closure_env);
|
||||
r: ((closure_env, integer) → integer, closure_env);
|
||||
q: integer
|
||||
} =
|
||||
if b then
|
||||
let f : SubFoo1 =
|
||||
let result : SubFoo1 = SubFoo1 { SubFoo1_in x_in = 10; } in
|
||||
{ SubFoo1 x = result.x; y = (closure_r, to_closure_env (result)); }
|
||||
{ SubFoo1 x = result.x; y = (closure_r1, to_closure_env (result)); }
|
||||
in
|
||||
{ Result r = f.y; q = f.x; }
|
||||
else
|
||||
@ -147,12 +147,15 @@ let scope Foo
|
||||
let result : SubFoo2 =
|
||||
SubFoo2 { SubFoo2_in x1_in = 10; x2_in = 10; }
|
||||
in
|
||||
{ SubFoo2 x1 = result.x1; y = (closure_r, to_closure_env (result)); }
|
||||
{ SubFoo2
|
||||
x1 = result.x1;
|
||||
y = (closure_r2, to_closure_env (result));
|
||||
}
|
||||
in
|
||||
{ Result r = f.y; q = f.x1; }
|
||||
in
|
||||
let set z : integer =
|
||||
let code_and_env : ((closure_env, integer) → integer * closure_env) =
|
||||
let code_and_env : ((closure_env, integer) → integer, closure_env) =
|
||||
r.r
|
||||
in
|
||||
code_and_env.0 code_and_env.1 1
|
||||
|
@ -99,55 +99,55 @@ in
|
||||
let lis3 : list of money =
|
||||
[¤20.00; ¤200.00; ¤10.00; ¤23.00; ¤25.00; ¤12.00]
|
||||
in
|
||||
let grok : (decimal, money, money) → (money * decimal) =
|
||||
let grok : (decimal, money, money) → (money, decimal) =
|
||||
λ (dec: decimal) (mon1: money) (mon2: money) →
|
||||
(mon1 * dec, mon1 / mon2)
|
||||
in
|
||||
let tlist : list of (decimal * money * money) =
|
||||
let tlist : list of (decimal, money, money) =
|
||||
map2
|
||||
(λ (a: decimal) (b_c: (money * money)) → (a, b_c.0, b_c.1))
|
||||
(λ (a: decimal) (b_c: (money, money)) → (a, b_c.0, b_c.1))
|
||||
lis1
|
||||
map2 (λ (b: money) (c: money) → (b, c)) lis2 lis3
|
||||
in
|
||||
let S : S_in → S =
|
||||
λ (S_in: S_in) →
|
||||
let r1 : list of (money * decimal) =
|
||||
map (λ (x: (decimal * money * money)) → grok x.0 x.1 x.2) tlist
|
||||
let r1 : list of (money, decimal) =
|
||||
map (λ (x: (decimal, money, money)) → grok x.0 x.1 x.2) tlist
|
||||
in
|
||||
let r2 : list of (money * decimal) =
|
||||
let r2 : list of (money, decimal) =
|
||||
map2
|
||||
(λ (x: decimal) (zip: (money * money)) →
|
||||
let x1 : (decimal * money * money) = (x, zip.0, zip.1) in
|
||||
(λ (x: decimal) (zip: (money, money)) →
|
||||
let x1 : (decimal, money, money) = (x, zip.0, zip.1) in
|
||||
grok x1.0 x1.1 x1.2)
|
||||
lis1
|
||||
map2 (λ (x: money) (zip: money) → (x, zip)) lis2 lis3
|
||||
in
|
||||
let r3 : list of (money * decimal) =
|
||||
let r3 : list of (money, decimal) =
|
||||
map2
|
||||
(λ (x: decimal) (y_z: (money * money)) →
|
||||
let x_y_z : (decimal * money * money) = (x, y_z.0, y_z.1) in
|
||||
(λ (x: decimal) (y_z: (money, money)) →
|
||||
let x_y_z : (decimal, money, money) = (x, y_z.0, y_z.1) in
|
||||
grok x_y_z.0 x_y_z.1 x_y_z.2)
|
||||
lis1
|
||||
map2 (λ (y: money) (z: money) → (y, z)) lis2 lis3
|
||||
in
|
||||
let r4 : list of (money * decimal) =
|
||||
map (λ (x_y_z: (decimal * money * money)) →
|
||||
let r4 : list of (money, decimal) =
|
||||
map (λ (x_y_z: (decimal, money, money)) →
|
||||
(x_y_z.1 * x_y_z.0, x_y_z.1 / x_y_z.2))
|
||||
tlist
|
||||
in
|
||||
let r5 : list of (money * decimal) =
|
||||
let r5 : list of (money, decimal) =
|
||||
map2
|
||||
(λ (x: decimal) (y_z: (money * money)) →
|
||||
let x_y_z : (decimal * money * money) = (x, y_z.0, y_z.1) in
|
||||
(λ (x: decimal) (y_z: (money, money)) →
|
||||
let x_y_z : (decimal, money, money) = (x, y_z.0, y_z.1) in
|
||||
(x_y_z.1 * x_y_z.0, x_y_z.1 / x_y_z.2))
|
||||
lis1
|
||||
map2 (λ (y: money) (z: money) → (y, z)) lis2 lis3
|
||||
in
|
||||
let r6 : list of (money * decimal) =
|
||||
let r6 : list of (money, decimal) =
|
||||
map2
|
||||
(λ (xy: (decimal * money)) (z: money) →
|
||||
let xy_z : ((decimal * money) * money) = (xy, z) in
|
||||
let xy1 : (decimal * money) = xy_z.0 in
|
||||
(λ (xy: (decimal, money)) (z: money) →
|
||||
let xy_z : ((decimal, money), money) = (xy, z) in
|
||||
let xy1 : (decimal, money) = xy_z.0 in
|
||||
let z1 : money = xy_z.1 in
|
||||
(xy1.1 * xy1.0, xy1.1 / z1))
|
||||
map2 (λ (x: decimal) (y: money) → (x, y)) lis1 lis2
|
||||
|
Loading…
Reference in New Issue
Block a user