From 4eb5933ad084551e6fc2460a9622c348bb16d6cd Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Thu, 23 Jun 2022 14:06:11 +0200 Subject: [PATCH] Porting the interpreter to the marked AST --- compiler/dcalc/ast.ml | 162 +++++++---- compiler/dcalc/ast.mli | 10 +- compiler/dcalc/interpreter.ml | 135 +++++---- compiler/lcalc/ast.ml | 258 ++++++++---------- compiler/lcalc/ast.mli | 180 ++++++------ compiler/lcalc/closure_conversion.ml | 145 +++++----- compiler/lcalc/closure_conversion.mli | 19 ++ compiler/lcalc/compile_with_exceptions.ml | 70 ++--- compiler/lcalc/compile_with_exceptions.mli | 4 +- compiler/lcalc/compile_without_exceptions.ml | 157 ++++++----- compiler/lcalc/compile_without_exceptions.mli | 2 +- compiler/lcalc/optimizations.ml | 26 +- compiler/lcalc/optimizations.mli | 4 +- compiler/lcalc/print.ml | 48 ++-- compiler/lcalc/print.mli | 6 +- compiler/lcalc/to_ocaml.ml | 29 +- compiler/lcalc/to_ocaml.mli | 2 +- compiler/plugin.ml | 2 +- compiler/plugin.mli | 6 +- compiler/scalc/compile_from_lambda.ml | 75 ++--- compiler/scalc/print.ml | 18 +- compiler/scalc/to_python.ml | 2 +- compiler/scopelang/scope_to_dcalc.ml | 2 +- 23 files changed, 729 insertions(+), 633 deletions(-) create mode 100644 compiler/lcalc/closure_conversion.mli diff --git a/compiler/dcalc/ast.ml b/compiler/dcalc/ast.ml index c18d1fcb..6aea46df 100644 --- a/compiler/dcalc/ast.ml +++ b/compiler/dcalc/ast.ml @@ -250,7 +250,7 @@ let with_ty (type m) (ty : Infer.unionfind_typ) (x : ('a, m) marked) : | Typed m -> Typed { m with ty }) (Marked.unmark x) -let evar v mark = Bindlib.box_apply (fun v' -> v', mark) (Bindlib.box_var v) +let evar v mark = Bindlib.box_apply (Marked.mark mark) (Bindlib.box_var v) let etuple args s mark = Bindlib.box_apply (fun args -> ETuple (args, s), mark) (Bindlib.box_list args) @@ -348,11 +348,11 @@ let rec fold_right_scope_lets ~f ~init scope_body_expr = let map_exprs_in_scope_lets ~f ~varf scope_body_expr = fold_right_scope_lets ~f:(fun scope_let var_next acc -> - Bindlib.box_apply2 - (fun scope_let_next scope_let_expr -> - ScopeLet { scope_let with scope_let_next; scope_let_expr }) - (Bindlib.bind_var (varf var_next) acc) - (f scope_let.scope_let_expr)) + Bindlib.box_apply2 + (fun scope_let_next scope_let_expr -> + ScopeLet { scope_let with scope_let_next; scope_let_expr }) + (Bindlib.bind_var (varf var_next) acc) + (f scope_let.scope_let_expr)) ~init:(fun res -> Bindlib.box_apply (fun res -> Result res) (f res)) scope_body_expr @@ -395,22 +395,22 @@ let map_exprs_in_scopes ~f ~varf scopes = let new_next = Bindlib.bind_var (varf var_next) acc in Bindlib.box_apply2 (fun scope_body_expr scope_next -> - ScopeDef { - scope_def with - scope_body = { scope_def.scope_body with scope_body_expr }; - scope_next; - }) - new_scope_body_expr - new_next) - ~init:(Bindlib.box Nil) - scopes + ScopeDef + { + scope_def with + scope_body = { scope_def.scope_body with scope_body_expr }; + scope_next; + }) + new_scope_body_expr new_next) + ~init:(Bindlib.box Nil) scopes type 'm var = 'm expr Bindlib.var +type 'm vars = 'm expr Bindlib.mvar let new_var s = Bindlib.new_var (fun x -> EVar x) s module Var = struct - type t = V : 'm var -> t + type t = V : 'a expr Bindlib.var -> t (* We use this trivial GADT to make the 'm parameter disappear under an existential. It's fine for a use as keys only. (bindlib defines [any_var] similarly but it's not exported) @@ -418,7 +418,7 @@ module Var = struct let t v = V v - let make (s : string) : t = V (new_var s) + let get (V v) = Bindlib.copy_var v (fun x -> EVar x) (Bindlib.name_of v) let compare (V x) (V y) = Bindlib.compare_vars x y end @@ -426,50 +426,89 @@ end module VarSet = Set.Make (Var) module VarMap = Map.Make (Var) -(* let rec free_vars_expr (e : untyped marked_expr) : VarSet.t = match - Marked.unmark e with | EVar v -> VarSet.singleton v | ETuple (es, _) | EArray - es -> es |> List.map free_vars_expr |> List.fold_left VarSet.union - VarSet.empty | ETupleAccess (e1, _, _, _) | EAssert e1 | ErrorOnEmpty e1 | - EInj (e1, _, _, _) -> free_vars_expr e1 | EApp (e1, es) | EMatch (e1, es, _) - -> e1 :: es |> List.map free_vars_expr |> List.fold_left VarSet.union - VarSet.empty | EDefault (es, ejust, econs) -> ejust :: econs :: es |> - List.map free_vars_expr |> List.fold_left VarSet.union VarSet.empty | EOp _ | - ELit _ -> VarSet.empty | EIfThenElse (e1, e2, e3) -> [e1; e2; e3] |> List.map - free_vars_expr |> List.fold_left VarSet.union VarSet.empty | EAbs (binder, _) - -> let vs, body = Bindlib.unmbind binder in Array.fold_right VarSet.remove vs - (free_vars_expr body) +(** {[ + let rec free_vars_expr (e : untyped marked_expr) : VarSet.t = + match Marked.unmark e with + | EVar v -> VarSet.singleton v + | ETuple (es, _) | EArray es -> + es |> List.map free_vars_expr + |> List.fold_left VarSet.union VarSet.empty + | ETupleAccess (e1, _, _, _) + | EAssert e1 + | ErrorOnEmpty e1 + | EInj (e1, _, _, _) -> + free_vars_expr e1 + | EApp (e1, es) | EMatch (e1, es, _) -> + e1 :: es |> List.map free_vars_expr + |> List.fold_left VarSet.union VarSet.empty + | EDefault (es, ejust, econs) -> + ejust :: econs :: es |> List.map free_vars_expr + |> List.fold_left VarSet.union VarSet.empty + | EOp _ | ELit _ -> VarSet.empty + | EIfThenElse (e1, e2, e3) -> + [e1; e2; e3] |> List.map free_vars_expr + |> List.fold_left VarSet.union VarSet.empty + | EAbs (binder, _) -> + let vs, body = Bindlib.unmbind binder in + Array.fold_right VarSet.remove vs (free_vars_expr body) - module VarMap = Map.Make (Var(struct type t = untyped end)) module VarSet = - Set.Make (Var(struct type t = untyped end)) + module VarMap = Map.Make (Var (struct + type t = untyped + end)) - let rec free_vars_expr (e : expr) : VarSet.t = match Marked.unmark e with | - EVar (v, _) -> VarSet.singleton v | ETuple (es, _) | EArray es -> es |> - List.map free_vars_expr |> List.fold_left VarSet.union VarSet.empty | - ETupleAccess (e1, _, _, _) | EAssert e1 | ErrorOnEmpty e1 | EInj (e1, _, _, - _) -> free_vars_expr e1 | EApp (e1, es) | EMatch (e1, es, _) -> e1 :: es |> - List.map free_vars_expr |> List.fold_left VarSet.union VarSet.empty | - EDefault (es, ejust, econs) -> ejust :: econs :: es |> List.map - free_vars_expr |> List.fold_left VarSet.union VarSet.empty | EOp _ | ELit _ - -> VarSet.empty | EIfThenElse (e1, e2, e3) -> [e1; e2; e3] |> List.map - free_vars_expr |> List.fold_left VarSet.union VarSet.empty | EAbs ((binder, - _), _) -> let vs, body = Bindlib.unmbind binder in Array.fold_right - VarSet.remove vs (free_vars_expr body) + module VarSet = Set.Make (Var (struct + type t = untyped + end)) - let rec free_vars_scope_body_expr (scope_lets : expr scope_body_expr) : - VarSet.t = match scope_lets with | Result e -> free_vars_expr e | ScopeLet { - scope_let_expr = e; scope_let_next = next; _ } -> let v, body = - Bindlib.unbind next in VarSet.union (free_vars_expr e) (VarSet.remove v - (free_vars_scope_body_expr body)) + let rec free_vars_expr (e : expr) : VarSet.t = + match Marked.unmark e with + | EVar (v, _) -> VarSet.singleton v + | ETuple (es, _) | EArray es -> + es |> List.map free_vars_expr + |> List.fold_left VarSet.union VarSet.empty + | ETupleAccess (e1, _, _, _) + | EAssert e1 + | ErrorOnEmpty e1 + | EInj (e1, _, _, _) -> + free_vars_expr e1 + | EApp (e1, es) | EMatch (e1, es, _) -> + e1 :: es |> List.map free_vars_expr + |> List.fold_left VarSet.union VarSet.empty + | EDefault (es, ejust, econs) -> + ejust :: econs :: es |> List.map free_vars_expr + |> List.fold_left VarSet.union VarSet.empty + | EOp _ | ELit _ -> VarSet.empty + | EIfThenElse (e1, e2, e3) -> + [e1; e2; e3] |> List.map free_vars_expr + |> List.fold_left VarSet.union VarSet.empty + | EAbs ((binder, _), _) -> + let vs, body = Bindlib.unmbind binder in + Array.fold_right VarSet.remove vs (free_vars_expr body) - let free_vars_scope_body (scope_body : expr scope_body) : VarSet.t = let { - scope_body_expr = binder; _ } = scope_body in let v, body = Bindlib.unbind - binder in VarSet.remove v (free_vars_scope_body_expr body) + let rec free_vars_scope_body_expr (scope_lets : expr scope_body_expr) : + VarSet.t = + match scope_lets with + | Result e -> free_vars_expr e + | ScopeLet { scope_let_expr = e; scope_let_next = next; _ } -> + let v, body = Bindlib.unbind next in + VarSet.union (free_vars_expr e) + (VarSet.remove v (free_vars_scope_body_expr body)) - let rec free_vars_scopes (scopes : expr scopes) : VarSet.t = match scopes - with | Nil -> VarSet.empty | ScopeDef { scope_body = body; scope_next = next; - _ } -> let v, next = Bindlib.unbind next in VarSet.union (VarSet.remove v - (free_vars_scopes next)) (free_vars_scope_body body) (* type vars = expr - Bindlib.mvar *) *) + let free_vars_scope_body (scope_body : expr scope_body) : VarSet.t = + let { scope_body_expr = binder; _ } = scope_body in + let v, body = Bindlib.unbind binder in + VarSet.remove v (free_vars_scope_body_expr body) + + let rec free_vars_scopes (scopes : expr scopes) : VarSet.t = + match scopes with + | Nil -> VarSet.empty + | ScopeDef { scope_body = body; scope_next = next; _ } -> + let v, next = Bindlib.unbind next in + VarSet.union + (VarSet.remove v (free_vars_scopes next)) + (free_vars_scope_body body) + (* type vars = expr Bindlib.mvar *) + ]}*) let make_var ((x, mark) : ('m expr Bindlib.var, 'm) marked) : 'm marked_expr Bindlib.box = @@ -746,9 +785,18 @@ let rec unfold_scopes mark_witness main_scope) scope_pos +let rec find_scope name vars = function + | Nil -> raise Not_found + | ScopeDef {scope_name; scope_body; _} when scope_name = name -> + List.rev vars, scope_body + | ScopeDef {scope_next; _} -> + let var, next = Bindlib.unbind scope_next in + find_scope name (var :: vars) next + let build_whole_program_expr (p : 'm program) (main_scope : ScopeName.t) = + let _, main_scope_body = find_scope main_scope [] p.scopes in unfold_scopes ~box_expr ~make_abs ~make_let_in p.decl_ctx p.scopes - p.mark_witness (ScopeName main_scope) + (get_scope_body_mark main_scope_body) (ScopeName main_scope) let rec expr_size (e : 'm marked_expr) : int = match Marked.unmark e with diff --git a/compiler/dcalc/ast.mli b/compiler/dcalc/ast.mli index 1b3cd381..e819c6eb 100644 --- a/compiler/dcalc/ast.mli +++ b/compiler/dcalc/ast.mli @@ -229,6 +229,7 @@ type 'm program = { decl_ctx : decl_ctx; scopes : ('m expr, 'm) scopes } (** {2 Manipulation of marks} *) val no_mark: 'm mark -> 'm mark +val mark_pos: 'm mark -> Pos.t val pos: ('a, 'm) marked -> Pos.t val ty: ('a, typed) marked -> typ val with_ty: Infer.unionfind_typ -> ('a, 'm) marked -> ('a, typed) marked @@ -402,12 +403,11 @@ type 'm var = 'm expr Bindlib.var val new_var: string -> 'm var -(** {2 Boxed term constructors} *) module Var : sig type t - val t: 'm var -> t - val make : string -> t + val t: 'm expr Bindlib.var -> t + val get: t -> 'm expr Bindlib.var val compare : t -> t -> int end @@ -422,7 +422,9 @@ module VarSet : Set.S with type elt = Var.t (* type vars = expr Bindlib.mvar *) -val make_var : ('m expr Bindlib.var, 'm) marked -> 'm marked_expr Bindlib.box +val make_var : ('m var, 'm) marked -> 'm marked_expr Bindlib.box + +(** {2 Boxed term constructors} *) type ('e, 'm) make_abs_sig = 'e Bindlib.mvar -> diff --git a/compiler/dcalc/interpreter.ml b/compiler/dcalc/interpreter.ml index beae3254..f92e3ae2 100644 --- a/compiler/dcalc/interpreter.ml +++ b/compiler/dcalc/interpreter.ml @@ -30,27 +30,29 @@ let log_indent = ref 0 let rec evaluate_operator (ctx : Ast.decl_ctx) - (op : A.operator Marked.pos) - (args : 'm A.marked_expr list) : 'm A.marked_expr = + (op : A.operator) + (pos : Pos.t) + (args : 'm A.marked_expr list) : 'm A.expr = (* Try to apply [div] and if a [Division_by_zero] exceptions is catched, use [op] to raise multispanned errors. *) - let apply_div_or_raise_err (div : unit -> 'm A.expr) (op : A.operator Marked.pos) + let apply_div_or_raise_err (div : unit -> 'm A.expr) : 'm A.expr = try div () with Division_by_zero -> Errors.raise_multispanned_error [ - Some "The division operator:", Marked.get_mark op; + Some "The division operator:", pos; Some "The null denominator:", Ast.pos (List.nth args 1); ] "division by zero at runtime" in - let get_binop_args_pos (arg0::arg1::_ : ('m A.expr * 'm) list) : - (string option * Pos.t) list = - [ - None, Ast.pos arg0; - None, Ast.pos arg1; - ] + let get_binop_args_pos = function + | (arg0::arg1::_ : 'm A.marked_expr list) -> + [ + None, Ast.pos arg0; + None, Ast.pos arg1; + ] + | _ -> assert false in (* Try to apply [cmp] and if a [UncomparableDurations] exceptions is catched, use [args] to raise multispanned errors. *) @@ -63,8 +65,7 @@ let rec evaluate_operator "Cannot compare together durations that cannot be converted to a \ precise number of days" in - Marked.same_mark_as - (match Marked.unmark op, List.map Marked.unmark args with + match op, List.map Marked.unmark args with | A.Ternop A.Fold, [_f; _init; EArray es] -> Marked.unmark (List.fold_left @@ -85,7 +86,7 @@ let rec evaluate_operator | A.Binop (A.Mult KInt), [ELit (LInt i1); ELit (LInt i2)] -> A.ELit (LInt Runtime.(i1 *! i2)) | A.Binop (A.Div KInt), [ELit (LInt i1); ELit (LInt i2)] -> - apply_div_or_raise_err (fun _ -> A.ELit (LInt Runtime.(i1 /! i2))) op + apply_div_or_raise_err (fun _ -> A.ELit (LInt Runtime.(i1 /! i2))) | A.Binop (A.Add KRat), [ELit (LRat i1); ELit (LRat i2)] -> A.ELit (LRat Runtime.(i1 +& i2)) | A.Binop (A.Sub KRat), [ELit (LRat i1); ELit (LRat i2)] -> @@ -93,7 +94,7 @@ let rec evaluate_operator | A.Binop (A.Mult KRat), [ELit (LRat i1); ELit (LRat i2)] -> A.ELit (LRat Runtime.(i1 *& i2)) | A.Binop (A.Div KRat), [ELit (LRat i1); ELit (LRat i2)] -> - apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(i1 /& i2))) op + apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(i1 /& i2))) | A.Binop (A.Add KMoney), [ELit (LMoney m1); ELit (LMoney m2)] -> A.ELit (LMoney Runtime.(m1 +$ m2)) | A.Binop (A.Sub KMoney), [ELit (LMoney m1); ELit (LMoney m2)] -> @@ -101,7 +102,7 @@ let rec evaluate_operator | A.Binop (A.Mult KMoney), [ELit (LMoney m1); ELit (LRat m2)] -> A.ELit (LMoney Runtime.(m1 *$ m2)) | A.Binop (A.Div KMoney), [ELit (LMoney m1); ELit (LMoney m2)] -> - apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(m1 /$ m2))) op + apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(m1 /$ m2))) | A.Binop (A.Add KDuration), [ELit (LDuration d1); ELit (LDuration d2)] -> A.ELit (LDuration Runtime.(d1 +^ d2)) | A.Binop (A.Sub KDuration), [ELit (LDuration d1); ELit (LDuration d2)] -> @@ -118,7 +119,6 @@ let rec evaluate_operator Errors.raise_multispanned_error (get_binop_args_pos args) "Cannot divide durations that cannot be converted to a precise \ number of days") - op | A.Binop (A.Mult KDuration), [ELit (LDuration d1); ELit (LInt i1)] -> A.ELit (LDuration Runtime.(d1 *^ i1)) | A.Binop (A.Lt KInt), [ELit (LInt i1); ELit (LInt i2)] -> @@ -180,7 +180,7 @@ let rec evaluate_operator (try List.for_all2 (fun e1 e2 -> - match Marked.unmark (evaluate_operator ctx op [e1; e2]) with + match evaluate_operator ctx op pos [e1; e2] with | A.ELit (LBool b) -> b | _ -> assert false (* should not happen *)) @@ -194,7 +194,7 @@ let rec evaluate_operator && List.for_all2 (fun e1 e2 -> match - Marked.unmark (evaluate_operator ctx op [e1; e2]) + evaluate_operator ctx op pos [e1; e2] with | A.ELit (LBool b) -> b | _ -> assert false @@ -207,7 +207,7 @@ let rec evaluate_operator (try en1 = en2 && i1 = i2 && - match Marked.unmark (evaluate_operator ctx op [e1; e2]) with + match evaluate_operator ctx op pos [e1; e2] with | A.ELit (LBool b) -> b | _ -> assert false (* should not happen *) @@ -216,8 +216,7 @@ let rec evaluate_operator A.ELit (LBool false) (* comparing anything else return false *) | A.Binop A.Neq, [_; _] -> ( match - Marked.unmark - (evaluate_operator ctx (Marked.same_mark_as (A.Binop A.Eq) op) args) + evaluate_operator ctx (A.Binop A.Eq) pos args with | A.ELit (A.LBool b) -> A.ELit (A.LBool (not b)) | _ -> assert false (*should not happen *)) @@ -240,7 +239,7 @@ let rec evaluate_operator | A.ELit (A.LBool b), _ -> b | _ -> Errors.raise_spanned_error - (Marked.get_mark (List.nth args 0)) + (A.pos (List.nth args 0)) "This predicate evaluated to something else than a boolean \ (should not happen if the term was well-typed)") es) @@ -285,7 +284,7 @@ let rec evaluate_operator let expr_str = Format.asprintf "%a" (Print.format_expr ctx ~debug:false) - (e', Pos.no_pos) + (List.hd args) in let expr_str = Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*") @@ -294,7 +293,6 @@ let rec evaluate_operator in Cli.with_style [ANSITerminal.green] "%s" expr_str) | PosRecordIfTrueBool -> ( - let pos = Marked.get_mark op in match pos <> Pos.no_pos, e' with | true, ELit (LBool true) -> Cli.log_format "%*s%a%s:\n%s" (!log_indent * 2) "" @@ -316,24 +314,23 @@ let rec evaluate_operator | A.Unop _, [ELit LEmptyError] -> A.ELit LEmptyError | _ -> Errors.raise_multispanned_error - ([Some "Operator:", Marked.get_mark op] + ([Some "Operator:", pos] @ List.mapi (fun i arg -> ( Some (Format.asprintf "Argument n°%d, value %a" (i + 1) (Print.format_expr ctx ~debug:true) arg), - Marked.get_mark arg )) + A.pos arg )) args) "Operator applied to the wrong arguments\n\ - (should not happen if the term was well-typed)") - op + (should not happen if the term was well-typed)" and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : 'm A.marked_expr = match Marked.unmark e with | EVar _ -> - Errors.raise_spanned_error (Marked.get_mark e) + Errors.raise_spanned_error (A.pos e) "free variable found at evaluation (should not happen if term was \ well-typed" | EApp (e1, args) -> ( @@ -345,17 +342,17 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : evaluate_expr ctx (Bindlib.msubst binder (Array.of_list (List.map Marked.unmark args))) else - Errors.raise_spanned_error (Marked.get_mark e) + Errors.raise_spanned_error (A.pos e) "wrong function call, expected %d arguments, got %d" (Bindlib.mbinder_arity binder) (List.length args) | EOp op -> Marked.same_mark_as - (Marked.unmark (evaluate_operator ctx (Marked.same_mark_as op e1) args)) + (evaluate_operator ctx op (A.pos e) args) e | ELit LEmptyError -> Marked.same_mark_as (A.ELit LEmptyError) e | _ -> - Errors.raise_spanned_error (Marked.get_mark e) + Errors.raise_spanned_error (A.pos e) "function has not been reduced to a lambda at evaluation (should not \ happen if the term was well-typed") | EAbs _ | ELit _ | EOp _ -> e (* these are values *) @@ -373,19 +370,19 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : | Some s, Some s' when s = s' -> () | _ -> Errors.raise_multispanned_error - [None, Marked.get_mark e; None, Marked.get_mark e1] + [None, A.pos e; None, A.pos e1] "Error during tuple access: not the same structs (should not happen \ if the term was well-typed)"); match List.nth_opt es n with | Some e' -> e' | None -> - Errors.raise_spanned_error (Marked.get_mark e1) + Errors.raise_spanned_error (A.pos e1) "The tuple has %d components but the %i-th element was requested \ (should not happen if the term was well-type)" (List.length es) n) | ELit LEmptyError -> Marked.same_mark_as (A.ELit LEmptyError) e | _ -> - Errors.raise_spanned_error (Marked.get_mark e1) + Errors.raise_spanned_error (A.pos e1) "The expression %a should be a tuple with %d components but is not \ (should not happen if the term was well-typed)" (Print.format_expr ctx ~debug:true) @@ -400,14 +397,14 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : | A.EInj (e1, n, e_name', _) -> if e_name <> e_name' then Errors.raise_multispanned_error - [None, Marked.get_mark e; None, Marked.get_mark e1] + [None, A.pos e; None, A.pos e1] "Error during match: two different enums found (should not happend \ if the term was well-typed)"; let es_n = match List.nth_opt es n with | Some es_n -> es_n | None -> - Errors.raise_spanned_error (Marked.get_mark e) + Errors.raise_spanned_error (A.pos e) "sum type index error (should not happend if the term was \ well-typed)" in @@ -415,7 +412,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : evaluate_expr ctx new_e | A.ELit A.LEmptyError -> Marked.same_mark_as (A.ELit A.LEmptyError) e | _ -> - Errors.raise_spanned_error (Marked.get_mark e1) + Errors.raise_spanned_error (A.pos e1) "Expected a term having a sum type as an argument to a match (should \ not happend if the term was well-typed") | EDefault (exceptions, just, cons) -> ( @@ -429,7 +426,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : | ELit (LBool true) -> evaluate_expr ctx cons | ELit (LBool false) -> Marked.same_mark_as (A.ELit LEmptyError) e | _ -> - Errors.raise_spanned_error (Marked.get_mark e) + Errors.raise_spanned_error (A.pos e) "Default justification has not been reduced to a boolean at \ evaluation (should not happen if the term was well-typed") | 1 -> List.find (fun sub -> not (is_empty_error sub)) exceptions @@ -438,7 +435,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : (List.map (fun except -> ( Some "This consequence has a valid justification:", - Marked.get_mark except )) + A.pos except )) (List.filter (fun sub -> not (is_empty_error sub)) exceptions)) "There is a conflict between multiple valid consequences for assigning \ the same variable.") @@ -448,7 +445,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : | ELit (LBool false) -> evaluate_expr ctx ef | ELit LEmptyError -> Marked.same_mark_as (A.ELit LEmptyError) e | _ -> - Errors.raise_spanned_error (Marked.get_mark cond) + Errors.raise_spanned_error (A.pos cond) "Expected a boolean literal for the result of this condition (should \ not happen if the term was well-typed)") | EArray es -> @@ -459,7 +456,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : | ErrorOnEmpty e' -> let e' = evaluate_expr ctx e' in if Marked.unmark e' = A.ELit LEmptyError then - Errors.raise_spanned_error (Marked.get_mark e') + Errors.raise_spanned_error (A.pos e') "This variable evaluated to an empty term (no rule that defined it \ applied in this situation)" else e' @@ -470,45 +467,64 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : match Marked.unmark e' with | Ast.ErrorOnEmpty ( EApp - ( (Ast.EOp (Binop op), pos_op), + ( (Ast.EOp (Binop op), _), [((ELit _, _) as e1); ((ELit _, _) as e2)] ), _ ) | EApp ( (Ast.EOp (Ast.Unop (Ast.Log _)), _), [ ( Ast.EApp - ( (Ast.EOp (Binop op), pos_op), + ( (Ast.EOp (Binop op), _), [((ELit _, _) as e1); ((ELit _, _) as e2)] ), _ ); ] ) | EApp - ( (Ast.EOp (Binop op), pos_op), + ( (Ast.EOp (Binop op), _), [((ELit _, _) as e1); ((ELit _, _) as e2)] ) -> - Errors.raise_spanned_error (Marked.get_mark e') + Errors.raise_spanned_error (A.pos e') "Assertion failed: %a %a %a" (Print.format_expr ctx ~debug:false) - e1 Print.format_binop (op, pos_op) + e1 Print.format_binop op (Print.format_expr ctx ~debug:false) e2 | _ -> Cli.debug_format "%a" (Print.format_expr ctx) e'; - Errors.raise_spanned_error (Marked.get_mark e') "Assertion failed") + Errors.raise_spanned_error (A.pos e') "Assertion failed") | ELit LEmptyError -> Marked.same_mark_as (A.ELit LEmptyError) e | _ -> - Errors.raise_spanned_error (Marked.get_mark e') + Errors.raise_spanned_error (A.pos e') "Expected a boolean literal for the result of this assertion (should \ not happen if the term was well-typed)") (** {1 API} *) -let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Marked.pos) : - (Uid.MarkedString.info * Ast.expr Marked.pos) list = - match Marked.unmark (evaluate_expr ctx e) with - | Ast.EAbs (_, [(Ast.TTuple (taus, Some s_in), _)]) -> ( - let application_term = List.map (fun _ -> Ast.empty_thunked_term) taus in +let interpret_program: 'm. Ast.decl_ctx -> 'm Ast.marked_expr -> (Uid.MarkedString.info * 'm Ast.marked_expr) list = +fun + (ctx : Ast.decl_ctx) (e : 'm Ast.marked_expr) : + (Uid.MarkedString.info * 'm Ast.marked_expr) list -> + match evaluate_expr ctx e with + | Ast.EAbs (_, [(Ast.TTuple (taus, Some s_in), _) as targs]), mark_e -> + begin + let application_term = + List.map (fun ty -> + Ast.empty_thunked_term (A.map_mark (fun pos -> pos) + (fun _ -> A.Infer.ast_to_typ ty) mark_e)) + taus + in let to_interpret = - ( Ast.EApp (e, [Ast.ETuple (application_term, Some s_in), Pos.no_pos]), - Pos.no_pos ) + ( Ast.EApp (e, [Ast.ETuple (application_term, Some s_in), + A.fold_marks + (fun pos_l -> List.hd pos_l) + (fun _ -> A.Infer.ast_to_typ targs) + (List.map Marked.get_mark application_term) + ]), + A.map_mark (fun pos -> pos) + (fun ty -> match UnionFind.get ty with + | A.Infer.TArrow (_, t_out), _ -> t_out + | _ -> + Errors.raise_spanned_error (A.pos e) + "(bug) Result of interpretation doesn't have the expected type") + mark_e ) in match Marked.unmark (evaluate_expr ctx to_interpret) with | Ast.ETuple (args, Some s_out) -> @@ -519,10 +535,11 @@ let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Marked.pos) : in List.map2 (fun arg var -> var, arg) args s_out_fields | _ -> - Errors.raise_spanned_error (Marked.get_mark e) + Errors.raise_spanned_error (A.pos e) "The interpretation of a program should always yield a struct \ - corresponding to the scope variables") + corresponding to the scope variables" + end | _ -> - Errors.raise_spanned_error (Marked.get_mark e) + Errors.raise_spanned_error (A.pos e) "The interpreter can only interpret terms starting with functions having \ thunked arguments" diff --git a/compiler/lcalc/ast.ml b/compiler/lcalc/ast.ml index 76d5029a..f8a9a9a3 100644 --- a/compiler/lcalc/ast.ml +++ b/compiler/lcalc/ast.ml @@ -28,128 +28,99 @@ type lit = type except = ConflictError | EmptyError | NoValueProvided | Crash -type marked_expr = expr Marked.pos +type 'm mark = 'm D.mark -and expr = - | EVar of expr Bindlib.var - | ETuple of marked_expr list * D.StructName.t option +type 'm marked_expr = ('m expr, 'm) D.marked + +and 'm expr = + | EVar of 'm expr Bindlib.var + | ETuple of 'm marked_expr list * D.StructName.t option (** The [MarkedString.info] is the former struct field name*) | ETupleAccess of - marked_expr * int * D.StructName.t option * D.typ Marked.pos list + 'm marked_expr * int * D.StructName.t option * D.typ Marked.pos list (** The [MarkedString.info] is the former struct field name *) - | EInj of marked_expr * int * D.EnumName.t * D.typ Marked.pos list + | EInj of 'm marked_expr * int * D.EnumName.t * D.typ Marked.pos list (** The [MarkedString.info] is the former enum case name *) - | EMatch of marked_expr * marked_expr list * D.EnumName.t + | EMatch of 'm marked_expr * 'm marked_expr list * D.EnumName.t (** The [MarkedString.info] is the former enum case name *) - | EArray of marked_expr list + | EArray of 'm marked_expr list | ELit of lit - | EAbs of (expr, marked_expr) Bindlib.mbinder * D.typ Marked.pos list - | EApp of marked_expr * marked_expr list - | EAssert of marked_expr + | EAbs of ('m expr, 'm marked_expr) Bindlib.mbinder * D.typ Marked.pos list + | EApp of 'm marked_expr * 'm marked_expr list + | EAssert of 'm marked_expr | EOp of D.operator - | EIfThenElse of marked_expr * marked_expr * marked_expr + | EIfThenElse of 'm marked_expr * 'm marked_expr * 'm marked_expr | ERaise of except - | ECatch of marked_expr * except * marked_expr + | ECatch of 'm marked_expr * except * 'm marked_expr -type program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : expr Dcalc.Ast.scopes } +type 'm program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : ('m expr, 'm) Dcalc.Ast.scopes } -let evar (v : expr Bindlib.var) (pos : Pos.t) : expr Marked.pos Bindlib.box = - Bindlib.box_apply (fun v' -> v', pos) (Bindlib.box_var v) +(* *) -let etuple - (args : expr Marked.pos Bindlib.box list) - (s : Dcalc.Ast.StructName.t option) - (pos : Pos.t) : expr Marked.pos Bindlib.box = - Bindlib.box_apply (fun args -> ETuple (args, s), pos) (Bindlib.box_list args) +let evar v mark = Bindlib.box_apply (Marked.mark mark) (Bindlib.box_var v) -let etupleaccess - (e1 : expr Marked.pos Bindlib.box) - (i : int) - (s : Dcalc.Ast.StructName.t option) - (typs : Dcalc.Ast.typ Marked.pos list) - (pos : Pos.t) : expr Marked.pos Bindlib.box = - Bindlib.box_apply (fun e1 -> ETupleAccess (e1, i, s, typs), pos) e1 +let etuple args s mark = + Bindlib.box_apply (fun args -> ETuple (args, s), mark) (Bindlib.box_list args) -let einj - (e1 : expr Marked.pos Bindlib.box) - (i : int) - (e_name : Dcalc.Ast.EnumName.t) - (typs : Dcalc.Ast.typ Marked.pos list) - (pos : Pos.t) : expr Marked.pos Bindlib.box = - Bindlib.box_apply (fun e1 -> EInj (e1, i, e_name, typs), pos) e1 +let etupleaccess e1 i s typs mark = + Bindlib.box_apply (fun e1 -> ETupleAccess (e1, i, s, typs), mark) e1 -let ematch - (arg : expr Marked.pos Bindlib.box) - (arms : expr Marked.pos Bindlib.box list) - (e_name : Dcalc.Ast.EnumName.t) - (pos : Pos.t) : expr Marked.pos Bindlib.box = +let einj e1 i e_name typs mark = + Bindlib.box_apply (fun e1 -> EInj (e1, i, e_name, typs), mark) e1 + +let ematch arg arms e_name mark = Bindlib.box_apply2 - (fun arg arms -> EMatch (arg, arms, e_name), pos) + (fun arg arms -> EMatch (arg, arms, e_name), mark) arg (Bindlib.box_list arms) -let earray (args : expr Marked.pos Bindlib.box list) (pos : Pos.t) : - expr Marked.pos Bindlib.box = - Bindlib.box_apply (fun args -> EArray args, pos) (Bindlib.box_list args) +let earray args mark = + Bindlib.box_apply (fun args -> EArray args, mark) (Bindlib.box_list args) -let elit (l : lit) (pos : Pos.t) : expr Marked.pos Bindlib.box = - Bindlib.box (ELit l, pos) +let elit l mark = Bindlib.box (ELit l, mark) -let eabs - (binder : (expr, expr Marked.pos) Bindlib.mbinder Bindlib.box) - (typs : Dcalc.Ast.typ Marked.pos list) - (pos : Pos.t) : expr Marked.pos Bindlib.box = - Bindlib.box_apply (fun binder -> EAbs (binder, typs), pos) binder +let eabs binder typs mark = + Bindlib.box_apply (fun binder -> EAbs (binder, typs), mark) binder -let eapp - (e1 : expr Marked.pos Bindlib.box) - (args : expr Marked.pos Bindlib.box list) - (pos : Pos.t) : expr Marked.pos Bindlib.box = +let eapp e1 args mark = Bindlib.box_apply2 - (fun e1 args -> EApp (e1, args), pos) + (fun e1 args -> EApp (e1, args), mark) e1 (Bindlib.box_list args) -let eassert (e1 : expr Marked.pos Bindlib.box) (pos : Pos.t) : - expr Marked.pos Bindlib.box = - Bindlib.box_apply (fun e1 -> EAssert e1, pos) e1 +let eassert e1 mark = Bindlib.box_apply (fun e1 -> EAssert e1, mark) e1 -let eop (op : Dcalc.Ast.operator) (pos : Pos.t) : expr Marked.pos Bindlib.box = - Bindlib.box (EOp op, pos) +let eop op mark = Bindlib.box (EOp op, mark) -let eraise (e1 : except) (pos : Pos.t) : expr Marked.pos Bindlib.box = - Bindlib.box (ERaise e1, pos) - -let ecatch - (e1 : expr Marked.pos Bindlib.box) - (exn : except) - (e2 : expr Marked.pos Bindlib.box) - (pos : Pos.t) : expr Marked.pos Bindlib.box = - Bindlib.box_apply2 (fun e1 e2 -> ECatch (e1, exn, e2), pos) e1 e2 - -let eifthenelse - (e1 : expr Marked.pos Bindlib.box) - (e2 : expr Marked.pos Bindlib.box) - (e3 : expr Marked.pos Bindlib.box) - (pos : Pos.t) : expr Marked.pos Bindlib.box = +let eifthenelse e1 e2 e3 pos = Bindlib.box_apply3 (fun e1 e2 e3 -> EIfThenElse (e1, e2, e3), pos) e1 e2 e3 +type 'm var = 'm expr Bindlib.var +type 'm vars = 'm expr Bindlib.mvar + +let new_var s = Bindlib.new_var (fun x -> EVar x) s + module Var = struct - type t = expr Bindlib.var + type t = V : 'a var -> t + (* See Dcalc.Ast.var *) - let make (s : string) : t = - Bindlib.new_var (fun (x : expr Bindlib.var) : expr -> EVar x) s + let t v = V v - let compare x y = Bindlib.compare_vars x y + let get (V v) = Bindlib.copy_var v (fun x -> EVar x) (Bindlib.name_of v) + + let compare (V x) (V y) = Bindlib.compare_vars x y end -module VarMap = Map.Make (Var) module VarSet = Set.Make (Var) +module VarMap = Map.Make (Var) -type vars = expr Bindlib.mvar +(* *) -let map_expr - (ctx : 'a) - ~(f : 'a -> expr Marked.pos -> expr Marked.pos Bindlib.box) - (e : expr Marked.pos) : expr Marked.pos Bindlib.box = +let eraise e1 pos = + Bindlib.box (ERaise e1, pos) + +let ecatch e1 exn e2 pos = + Bindlib.box_apply2 (fun e1 e2 -> ECatch (e1, exn, e2), pos) e1 e2 + +let map_expr ctx ~f e = match Marked.unmark e with | EVar v -> evar v (Marked.get_mark e) | EApp (e1, args) -> @@ -173,41 +144,50 @@ let map_expr | ECatch (e1, exn, e2) -> ecatch (f ctx e1) exn (f ctx e2) (Marked.get_mark e) (** See [Bindlib.box_term] documentation for why we are doing that. *) -let box_expr (e : expr Marked.pos) : expr Marked.pos Bindlib.box = +let box_expr (e : 'm marked_expr) : 'm marked_expr Bindlib.box = let rec id_t () e = map_expr () ~f:id_t e in id_t () e -let make_var ((x, pos) : Var.t Marked.pos) : expr Marked.pos Bindlib.box = - Bindlib.box_apply (fun x -> x, pos) (Bindlib.box_var x) +let make_var (x, mark) = + Bindlib.box_apply (fun x -> x, mark) (Bindlib.box_var x) -let make_abs - (xs : vars) - (e : expr Marked.pos Bindlib.box) - (taus : D.typ Marked.pos list) - (pos : Pos.t) : expr Marked.pos Bindlib.box = - Bindlib.box_apply (fun b -> EAbs (b, taus), pos) (Bindlib.bind_mvar xs e) +let make_abs xs e taus mark = + Bindlib.box_apply (fun b -> EAbs (b, taus), mark) (Bindlib.bind_mvar xs e) -let make_app - (e : expr Marked.pos Bindlib.box) - (u : expr Marked.pos Bindlib.box list) - (pos : Pos.t) : expr Marked.pos Bindlib.box = - Bindlib.box_apply2 (fun e u -> EApp (e, u), pos) e (Bindlib.box_list u) +let make_app e u mark = + Bindlib.box_apply2 (fun e u -> EApp (e, u), mark) e (Bindlib.box_list u) -let make_let_in - (x : Var.t) - (tau : D.typ Marked.pos) - (e1 : expr Marked.pos Bindlib.box) - (e2 : expr Marked.pos Bindlib.box) - (pos : Pos.t) : expr Marked.pos Bindlib.box = - make_app (make_abs (Array.of_list [x]) e2 [tau] pos) [e1] pos +let make_let_in x tau e1 e2 pos = + let m_e1 = Marked.get_mark (Bindlib.unbox e1) in + let m_e2 = Marked.get_mark (Bindlib.unbox e2) in + let m_abs = + D.map_mark2 + (fun _ _ -> pos) + (fun m1 m2 -> UnionFind.make (D.Infer.TArrow (m1.ty, m2.ty), m1.pos)) + m_e1 m_e2 + in + make_app (make_abs [| x |] e2 [tau] m_abs) [e1] m_e2 -let make_multiple_let_in - (xs : Var.t array) - (taus : D.typ Marked.pos list) - (e1 : expr Marked.pos Bindlib.box list) - (e2 : expr Marked.pos Bindlib.box) - (pos : Pos.t) : expr Marked.pos Bindlib.box = - make_app (make_abs xs e2 taus pos) e1 pos +let make_multiple_let_in xs taus e1s e2 pos = + (* let m_e1s = List.map (fun e -> Marked.get_mark (Bindlib.unbox e)) e1s in *) + let m_e1s = + D.fold_marks List.hd (fun tys -> + UnionFind.make + (D.Infer.TTuple + (List.map (fun t -> t.D.ty) tys, None), + (List.hd tys).D.pos) + ) + (List.map (fun e -> Marked.get_mark (Bindlib.unbox e)) e1s) + in + let m_e2 = Marked.get_mark (Bindlib.unbox e2) in + let m_abs = + D.map_mark2 + (fun _ _ -> pos) + (fun m1 m2 -> + UnionFind.make (D.Infer.TArrow (m1.ty, m2.ty), pos)) + m_e1s m_e2 + in + make_app (make_abs xs e2 taus m_abs) e1s m_e2 let ( let+ ) x f = Bindlib.box_apply f x let ( and+ ) x y = Bindlib.box_pair x y @@ -222,29 +202,33 @@ let some_constr : D.EnumConstructor.t = let option_enum_config : (D.EnumConstructor.t * D.typ Marked.pos) list = [none_constr, (D.TLit D.TUnit, Pos.no_pos); some_constr, (D.TAny, Pos.no_pos)] -let make_none (pos : Pos.t) : expr Marked.pos Bindlib.box = - let mark : 'a -> 'a Marked.pos = Marked.mark pos in +(* FIXME: proper typing in all the constructors below *) + +let make_none m = + let mark = Marked.mark m in + let tunit = D.TLit D.TUnit, D.mark_pos m in Bindlib.box @@ mark @@ EInj - (mark @@ ELit LUnit, 0, option_enum, [D.TLit D.TUnit, pos; D.TAny, pos]) + (Marked.mark (D.map_mark (fun pos -> pos) (fun _ -> D.Infer.ast_to_typ tunit) m) + (ELit LUnit), + 0, + option_enum, + [D.TLit D.TUnit, Pos.no_pos; D.TAny, Pos.no_pos]) -let make_some (e : expr Marked.pos Bindlib.box) : expr Marked.pos Bindlib.box = - let pos = Marked.get_mark @@ Bindlib.unbox e in - let mark : 'a -> 'a Marked.pos = Marked.mark pos in +let make_some e = + let m = Marked.get_mark @@ Bindlib.unbox e in + let mark = Marked.mark m in begin[@ocamlformat "disable"] let+ e = e in - mark @@ EInj (e, 1, option_enum, [ (D.TLit D.TUnit, pos); (D.TAny, pos) ]) + mark @@ EInj (e, 1, option_enum, [ (D.TLit D.TUnit, D.mark_pos m); (D.TAny, D.mark_pos m) ]) end (** [make_matchopt_with_abs_arms arg e_none e_some] build an expression [match arg with |None -> e_none | Some -> e_some] and requires e_some and e_none to be in the form [EAbs ...].*) -let make_matchopt_with_abs_arms - (arg : expr Marked.pos Bindlib.box) - (e_none : expr Marked.pos Bindlib.box) - (e_some : expr Marked.pos Bindlib.box) : expr Marked.pos Bindlib.box = - let pos = Marked.get_mark @@ Bindlib.unbox arg in - let mark : 'a -> 'a Marked.pos = Marked.mark pos in +let make_matchopt_with_abs_arms arg e_none e_some = + let m = Marked.get_mark @@ Bindlib.unbox arg in + let mark = Marked.mark m in begin[@ocamlformat "disable"] let+ arg = arg and+ e_none = e_none @@ -256,20 +240,14 @@ let make_matchopt_with_abs_arms [match arg with | None () -> e_none | Some v -> e_some]. It binds v to e_some, permitting it to be used inside the expression. There is no requirements on the form of both e_some and e_none. *) -let make_matchopt - (pos : Pos.t) - (v : Var.t) - (tau : D.typ Marked.pos) - (arg : expr Marked.pos Bindlib.box) - (e_none : expr Marked.pos Bindlib.box) - (e_some : expr Marked.pos Bindlib.box) : expr Marked.pos Bindlib.box = - let x = Var.make "_" in +let make_matchopt m v tau arg e_none e_some = + let x = new_var "_" in make_matchopt_with_abs_arms arg - (make_abs (Array.of_list [x]) e_none [D.TLit D.TUnit, pos] pos) - (make_abs (Array.of_list [v]) e_some [tau] pos) + (make_abs (Array.of_list [x]) e_none [D.TLit D.TUnit, D.mark_pos m] m) + (make_abs (Array.of_list [v]) e_some [tau] m) -let handle_default = Var.make "handle_default" -let handle_default_opt = Var.make "handle_default_opt" +let handle_default = Var.t (new_var "handle_default") +let handle_default_opt = Var.t (new_var "handle_default_opt") -type binder = (expr, expr Marked.pos) Bindlib.binder +type 'm binder = ('m expr, 'm marked_expr) Bindlib.binder diff --git a/compiler/lcalc/ast.mli b/compiler/lcalc/ast.mli index 615b0617..493ef1b7 100644 --- a/compiler/lcalc/ast.mli +++ b/compiler/lcalc/ast.mli @@ -34,153 +34,159 @@ type lit = type except = ConflictError | EmptyError | NoValueProvided | Crash -type marked_expr = expr Marked.pos +type 'm mark = 'm Dcalc.Ast.mark -and expr = - | EVar of expr Bindlib.var - | ETuple of marked_expr list * Dcalc.Ast.StructName.t option +type 'm marked_expr = ('m expr, 'm) Dcalc.Ast.marked + +and 'm expr = + | EVar of 'm expr Bindlib.var + | ETuple of 'm marked_expr list * Dcalc.Ast.StructName.t option (** The [MarkedString.info] is the former struct field name*) | ETupleAccess of - marked_expr + 'm marked_expr * int * Dcalc.Ast.StructName.t option * Dcalc.Ast.typ Marked.pos list (** The [MarkedString.info] is the former struct field name *) | EInj of - marked_expr * int * Dcalc.Ast.EnumName.t * Dcalc.Ast.typ Marked.pos list + 'm marked_expr * int * Dcalc.Ast.EnumName.t * Dcalc.Ast.typ Marked.pos list (** The [MarkedString.info] is the former enum case name *) - | EMatch of marked_expr * marked_expr list * Dcalc.Ast.EnumName.t + | EMatch of 'm marked_expr * 'm marked_expr list * Dcalc.Ast.EnumName.t (** The [MarkedString.info] is the former enum case name *) - | EArray of marked_expr list + | EArray of 'm marked_expr list | ELit of lit - | EAbs of (expr, marked_expr) Bindlib.mbinder * Dcalc.Ast.typ Marked.pos list - | EApp of marked_expr * marked_expr list - | EAssert of marked_expr + | EAbs of ('m expr, 'm marked_expr) Bindlib.mbinder * Dcalc.Ast.typ Marked.pos list + | EApp of 'm marked_expr * 'm marked_expr list + | EAssert of 'm marked_expr | EOp of Dcalc.Ast.operator - | EIfThenElse of marked_expr * marked_expr * marked_expr + | EIfThenElse of 'm marked_expr * 'm marked_expr * 'm marked_expr | ERaise of except - | ECatch of marked_expr * except * marked_expr + | ECatch of 'm marked_expr * except * 'm marked_expr -type program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : (expr, Dcalc.Ast.untyped) Dcalc.Ast.scopes } +type 'm program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : ('m expr, 'm) Dcalc.Ast.scopes } (** {1 Variable helpers} *) -module Var : sig - type t = expr Bindlib.var +type 'm var = 'm expr Bindlib.var +type 'm vars = 'm expr Bindlib.mvar - val make : string -> t +module Var : sig + type t + + val t: 'm expr Bindlib.var -> t + val get: t -> 'm expr Bindlib.var val compare : t -> t -> int end - module VarMap : Map.S with type key = Var.t module VarSet : Set.S with type elt = Var.t -type vars = expr Bindlib.mvar -type binder = (expr, expr Marked.pos) Bindlib.binder +val new_var: string -> 'm var -(** {1 Boxed constructors}*) +type 'm binder = ('m expr, 'm marked_expr) Bindlib.binder -val evar : expr Bindlib.var -> Pos.t -> expr Marked.pos Bindlib.box +(** {1 Boxed constructors} *) + +val evar : 'm expr Bindlib.var -> 'm mark -> 'm marked_expr Bindlib.box val etuple : - expr Marked.pos Bindlib.box list -> + 'm marked_expr Bindlib.box list -> Dcalc.Ast.StructName.t option -> - Pos.t -> - expr Marked.pos Bindlib.box + 'm mark -> + 'm marked_expr Bindlib.box val etupleaccess : - expr Marked.pos Bindlib.box -> + 'm marked_expr Bindlib.box -> int -> Dcalc.Ast.StructName.t option -> Dcalc.Ast.typ Marked.pos list -> - Pos.t -> - expr Marked.pos Bindlib.box + 'm mark -> + 'm marked_expr Bindlib.box val einj : - expr Marked.pos Bindlib.box -> + 'm marked_expr Bindlib.box -> int -> Dcalc.Ast.EnumName.t -> Dcalc.Ast.typ Marked.pos list -> - Pos.t -> - expr Marked.pos Bindlib.box + 'm mark -> + 'm marked_expr Bindlib.box val ematch : - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box list -> + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box list -> Dcalc.Ast.EnumName.t -> - Pos.t -> - expr Marked.pos Bindlib.box + 'm mark -> + 'm marked_expr Bindlib.box val earray : - expr Marked.pos Bindlib.box list -> Pos.t -> expr Marked.pos Bindlib.box + 'm marked_expr Bindlib.box list -> 'm mark -> 'm marked_expr Bindlib.box -val elit : lit -> Pos.t -> expr Marked.pos Bindlib.box +val elit : lit -> 'm mark -> 'm marked_expr Bindlib.box val eabs : - (expr, expr Marked.pos) Bindlib.mbinder Bindlib.box -> + ('m expr, 'm marked_expr) Bindlib.mbinder Bindlib.box -> Dcalc.Ast.typ Marked.pos list -> - Pos.t -> - expr Marked.pos Bindlib.box + 'm mark -> + 'm marked_expr Bindlib.box val eapp : - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box list -> - Pos.t -> - expr Marked.pos Bindlib.box + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box list -> + 'm mark -> + 'm marked_expr Bindlib.box val eassert : - expr Marked.pos Bindlib.box -> Pos.t -> expr Marked.pos Bindlib.box + 'm marked_expr Bindlib.box -> 'm mark -> 'm marked_expr Bindlib.box -val eop : Dcalc.Ast.operator -> Pos.t -> expr Marked.pos Bindlib.box +val eop : Dcalc.Ast.operator -> 'm mark -> 'm marked_expr Bindlib.box val eifthenelse : - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box -> - Pos.t -> - expr Marked.pos Bindlib.box + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box -> + 'm mark -> + 'm marked_expr Bindlib.box val ecatch : - expr Marked.pos Bindlib.box -> + 'm marked_expr Bindlib.box -> except -> - expr Marked.pos Bindlib.box -> - Pos.t -> - expr Marked.pos Bindlib.box + 'm marked_expr Bindlib.box -> + 'm mark -> + 'm marked_expr Bindlib.box -val eraise : except -> Pos.t -> expr Marked.pos Bindlib.box +val eraise : except -> 'm mark -> 'm marked_expr Bindlib.box (** {1 Language terms construction}*) -val make_var : Var.t Marked.pos -> expr Marked.pos Bindlib.box +val make_var : ('m var, 'm) Dcalc.Ast.marked -> 'm marked_expr Bindlib.box val make_abs : - vars -> - expr Marked.pos Bindlib.box -> + 'm vars -> + 'm marked_expr Bindlib.box -> Dcalc.Ast.typ Marked.pos list -> - Pos.t -> - expr Marked.pos Bindlib.box + 'm mark -> + 'm marked_expr Bindlib.box val make_app : - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box list -> - Pos.t -> - expr Marked.pos Bindlib.box + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box list -> + 'm mark -> + 'm marked_expr Bindlib.box val make_let_in : - Var.t -> + 'm var -> Dcalc.Ast.typ Marked.pos -> - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box -> + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box -> Pos.t -> - expr Marked.pos Bindlib.box + 'm marked_expr Bindlib.box val make_multiple_let_in : - Var.t array -> + 'm vars -> Dcalc.Ast.typ Marked.pos list -> - expr Marked.pos Bindlib.box list -> - expr Marked.pos Bindlib.box -> + 'm marked_expr Bindlib.box list -> + 'm marked_expr Bindlib.box -> Pos.t -> - expr Marked.pos Bindlib.box + 'm marked_expr Bindlib.box val option_enum : Dcalc.Ast.EnumName.t val none_constr : Dcalc.Ast.EnumConstructor.t @@ -189,29 +195,29 @@ val some_constr : Dcalc.Ast.EnumConstructor.t val option_enum_config : (Dcalc.Ast.EnumConstructor.t * Dcalc.Ast.typ Marked.pos) list -val make_none : Pos.t -> expr Marked.pos Bindlib.box -val make_some : expr Marked.pos Bindlib.box -> expr Marked.pos Bindlib.box +val make_none : 'm mark -> 'm marked_expr Bindlib.box +val make_some : 'm marked_expr Bindlib.box -> 'm marked_expr Bindlib.box val make_matchopt_with_abs_arms : - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box val make_matchopt : - Pos.t -> - Var.t -> + 'm mark -> + 'm var -> Dcalc.Ast.typ Marked.pos -> - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box -> - expr Marked.pos Bindlib.box + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box -> + 'm marked_expr Bindlib.box (** [e' = make_matchopt'' pos v e e_none e_some] Builds the term corresponding to [match e with | None -> fun () -> e_none |Some -> fun v -> e_some]. *) -val box_expr : expr Marked.pos -> expr Marked.pos Bindlib.box +val box_expr : 'm marked_expr -> 'm marked_expr Bindlib.box -(** {1 Special symbols}*) +(** {1 Special symbols} *) val handle_default : Var.t val handle_default_opt : Var.t diff --git a/compiler/lcalc/closure_conversion.ml b/compiler/lcalc/closure_conversion.ml index 7cd616ee..b2287dae 100644 --- a/compiler/lcalc/closure_conversion.ml +++ b/compiler/lcalc/closure_conversion.ml @@ -21,46 +21,51 @@ module D = Dcalc.Ast (** TODO: This version is not yet debugged and ought to be specialized when Lcalc has more structure. *) -type closure = { name : Var.t; expr : expr Marked.pos Bindlib.box } type ctx = { name_context : string; globally_bound_vars : VarSet.t } (** Returns the expression with closed closures and the set of free variables inside this new expression. Implementation guided by http://gallium.inria.fr/~fpottier/mpri/cours04.pdf#page=9. *) -let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) : - expr Marked.pos Bindlib.box * VarSet.t = +let closure_conversion_expr (type m) (ctx: ctx) (e: m marked_expr) : m marked_expr Bindlib.box = + let module MVarSet = Set.Make(struct + type t = m var + let compare = Bindlib.compare_vars + end) in + let rec aux e = match Marked.unmark e with | EVar v -> ( Bindlib.box_apply (fun new_v -> new_v, Marked.get_mark e) (Bindlib.box_var v), - VarSet.diff (VarSet.singleton v) ctx.globally_bound_vars ) + if VarSet.mem (Var.t v) ctx.globally_bound_vars + then MVarSet.empty + else MVarSet.singleton v) | ETuple (args, s) -> let new_args, free_vars = List.fold_left (fun (new_args, free_vars) arg -> - let new_arg, new_free_vars = closure_conversion_expr ctx arg in - new_arg :: new_args, VarSet.union new_free_vars free_vars) - ([], VarSet.empty) args + let new_arg, new_free_vars = aux arg in + new_arg :: new_args, MVarSet.union new_free_vars free_vars) + ([], MVarSet.empty) args in ( Bindlib.box_apply (fun new_args -> ETuple (List.rev new_args, s), Marked.get_mark e) (Bindlib.box_list new_args), free_vars ) | ETupleAccess (e1, n, s, typs) -> - let new_e1, free_vars = closure_conversion_expr ctx e1 in + let new_e1, free_vars = aux e1 in ( Bindlib.box_apply (fun new_e1 -> ETupleAccess (new_e1, n, s, typs), Marked.get_mark e) new_e1, free_vars ) | EInj (e1, n, e_name, typs) -> - let new_e1, free_vars = closure_conversion_expr ctx e1 in + let new_e1, free_vars = aux e1 in ( Bindlib.box_apply (fun new_e1 -> EInj (new_e1, n, e_name, typs), Marked.get_mark e) new_e1, free_vars ) | EMatch (e1, arms, e_name) -> - let new_e1, free_vars = closure_conversion_expr ctx e1 in + let new_e1, free_vars = aux e1 in (* We do not close the clotures inside the arms of the match expression, since they get a special treatment at compilation to Scalc. *) let new_arms, free_vars = @@ -69,13 +74,13 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) : match Marked.unmark arm with | EAbs (binder, typs) -> let vars, body = Bindlib.unmbind binder in - let new_body, new_free_vars = closure_conversion_expr ctx body in + let new_body, new_free_vars = aux body in let new_binder = Bindlib.bind_mvar vars new_body in ( Bindlib.box_apply (fun new_binder -> EAbs (new_binder, typs), Marked.get_mark arm) new_binder :: new_arms, - VarSet.union free_vars new_free_vars ) + MVarSet.union free_vars new_free_vars ) | _ -> failwith "should not happen") arms ([], free_vars) in @@ -89,25 +94,25 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) : let new_args, free_vars = List.fold_right (fun arg (new_args, free_vars) -> - let new_arg, new_free_vars = closure_conversion_expr ctx arg in - new_arg :: new_args, VarSet.union free_vars new_free_vars) - args ([], VarSet.empty) + let new_arg, new_free_vars = aux arg in + new_arg :: new_args, MVarSet.union free_vars new_free_vars) + args ([], MVarSet.empty) in ( Bindlib.box_apply (fun new_args -> EArray new_args, Marked.get_mark e) (Bindlib.box_list new_args), free_vars ) - | ELit l -> Bindlib.box (ELit l, Marked.get_mark e), VarSet.empty + | ELit l -> Bindlib.box (ELit l, Marked.get_mark e), MVarSet.empty | EApp ((EAbs (binder, typs_abs), e1_pos), args) -> (* let-binding, we should not close these *) let vars, body = Bindlib.unmbind binder in - let new_body, free_vars = closure_conversion_expr ctx body in + let new_body, free_vars = aux body in let new_binder = Bindlib.bind_mvar vars new_body in let new_args, free_vars = List.fold_right (fun arg (new_args, free_vars) -> - let new_arg, new_free_vars = closure_conversion_expr ctx arg in - new_arg :: new_args, VarSet.union free_vars new_free_vars) + let new_arg, new_free_vars = aux arg in + new_arg :: new_args, MVarSet.union free_vars new_free_vars) args ([], free_vars) in ( Bindlib.box_apply2 @@ -119,40 +124,39 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) : free_vars ) | EAbs (binder, typs) -> (* λ x.t *) - let binder_pos = Marked.get_mark e in + let binder_mark = Marked.get_mark e in + let binder_pos = D.mark_pos binder_mark in (* Converting the closure. *) let vars, body = Bindlib.unmbind binder in (* t *) - let new_body, body_vars = closure_conversion_expr ctx body in + let new_body, body_vars = aux body in (* [[t]] *) let extra_vars = - VarSet.diff body_vars (VarSet.of_list (Array.to_list vars)) + MVarSet.diff body_vars (MVarSet.of_list (Array.to_list vars)) in - let extra_vars_list = VarSet.elements extra_vars in + let extra_vars_list = MVarSet.elements extra_vars in (* x1, ..., xn *) - let code_var = Var.make ctx.name_context in + let code_var = new_var ctx.name_context in (* code *) - let inner_c_var = Var.make "env" in + let inner_c_var = new_var "env" in + let any_ty = Dcalc.Ast.TAny, binder_pos in let new_closure_body = make_multiple_let_in (Array.of_list extra_vars_list) - (List.init (List.length extra_vars_list) (fun _ -> - Dcalc.Ast.TAny, binder_pos)) + (List.map (fun _ -> any_ty) extra_vars_list) (List.mapi (fun i _ -> Bindlib.box_apply (fun inner_c_var -> ( ETupleAccess - ( (inner_c_var, binder_pos), + ( (inner_c_var, binder_mark), i + 1, None, - List.init - (List.length extra_vars_list + 1) - (fun _ -> Dcalc.Ast.TAny, binder_pos) ), - binder_pos )) + List.map (fun _ -> any_ty) extra_vars_list), + binder_mark )) (Bindlib.box_var inner_c_var)) extra_vars_list) - new_body binder_pos + new_body (D.mark_pos binder_mark) in let new_closure = make_abs @@ -162,14 +166,14 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) : (Marked.get_mark e) in ( make_let_in code_var - (Dcalc.Ast.TAny, Marked.get_mark e) + (Dcalc.Ast.TAny, D.pos e) new_closure (Bindlib.box_apply2 (fun code_var extra_vars -> ( ETuple - ( (code_var, binder_pos) + ( (code_var, binder_mark) :: List.map - (fun extra_var -> extra_var, binder_pos) + (fun extra_var -> extra_var, binder_mark) extra_vars, None ), Marked.get_mark e )) @@ -178,29 +182,29 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) : (List.map (fun extra_var -> Bindlib.box_var extra_var) extra_vars_list))) - (Marked.get_mark e), + (D.pos e), extra_vars ) | EApp ((EOp op, pos_op), args) -> (* This corresponds to an operator call, which we don't want to transform*) let new_args, free_vars = List.fold_right (fun arg (new_args, free_vars) -> - let new_arg, new_free_vars = closure_conversion_expr ctx arg in - new_arg :: new_args, VarSet.union free_vars new_free_vars) - args ([], VarSet.empty) + let new_arg, new_free_vars = aux arg in + new_arg :: new_args, MVarSet.union free_vars new_free_vars) + args ([], MVarSet.empty) in ( Bindlib.box_apply (fun new_e2 -> EApp ((EOp op, pos_op), new_e2), Marked.get_mark e) (Bindlib.box_list new_args), free_vars ) - | EApp ((EVar v, v_pos), args) when VarSet.mem v ctx.globally_bound_vars -> + | EApp ((EVar v, v_pos), args) when VarSet.mem (Var.t v) ctx.globally_bound_vars -> (* This corresponds to a scope call, which we don't want to transform*) let new_args, free_vars = List.fold_right (fun arg (new_args, free_vars) -> - let new_arg, new_free_vars = closure_conversion_expr ctx arg in - new_arg :: new_args, VarSet.union free_vars new_free_vars) - args ([], VarSet.empty) + let new_arg, new_free_vars = aux arg in + new_arg :: new_args, MVarSet.union free_vars new_free_vars) + args ([], MVarSet.empty) in ( Bindlib.box_apply2 (fun new_v new_e2 -> EApp ((new_v, v_pos), new_e2), Marked.get_mark e) @@ -208,19 +212,19 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) : (Bindlib.box_list new_args), free_vars ) | EApp (e1, args) -> - let new_e1, free_vars = closure_conversion_expr ctx e1 in - let env_var = Var.make "env" in - let code_var = Var.make "code" in + let new_e1, free_vars = aux e1 in + let env_var = new_var "env" in + let code_var = new_var "code" in let new_args, free_vars = List.fold_right (fun arg (new_args, free_vars) -> - let new_arg, new_free_vars = closure_conversion_expr ctx arg in - new_arg :: new_args, VarSet.union free_vars new_free_vars) + let new_arg, new_free_vars = aux arg in + new_arg :: new_args, MVarSet.union free_vars new_free_vars) args ([], free_vars) in let call_expr = make_let_in code_var - (Dcalc.Ast.TAny, Marked.get_mark e) + (Dcalc.Ast.TAny, D.pos e) (Bindlib.box_apply (fun env_var -> ( ETupleAccess @@ -235,50 +239,50 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) : Marked.get_mark e )) (Bindlib.box_var code_var) (Bindlib.box_var env_var) (Bindlib.box_list new_args)) - (Marked.get_mark e) + (D.pos e) in ( make_let_in env_var - (Dcalc.Ast.TAny, Marked.get_mark e) - new_e1 call_expr (Marked.get_mark e), + (Dcalc.Ast.TAny, D.pos e) + new_e1 call_expr (D.pos e), free_vars ) | EAssert e1 -> - let new_e1, free_vars = closure_conversion_expr ctx e1 in + let new_e1, free_vars = aux e1 in ( Bindlib.box_apply (fun new_e1 -> EAssert new_e1, Marked.get_mark e) new_e1, free_vars ) - | EOp op -> Bindlib.box (EOp op, Marked.get_mark e), VarSet.empty + | EOp op -> Bindlib.box (EOp op, Marked.get_mark e), MVarSet.empty | EIfThenElse (e1, e2, e3) -> - let new_e1, free_vars1 = closure_conversion_expr ctx e1 in - let new_e2, free_vars2 = closure_conversion_expr ctx e2 in - let new_e3, free_vars3 = closure_conversion_expr ctx e3 in + let new_e1, free_vars1 = aux e1 in + let new_e2, free_vars2 = aux e2 in + let new_e3, free_vars3 = aux e3 in ( Bindlib.box_apply3 (fun new_e1 new_e2 new_e3 -> EIfThenElse (new_e1, new_e2, new_e3), Marked.get_mark e) new_e1 new_e2 new_e3, - VarSet.union (VarSet.union free_vars1 free_vars2) free_vars3 ) + MVarSet.union (MVarSet.union free_vars1 free_vars2) free_vars3 ) | ERaise except -> - Bindlib.box (ERaise except, Marked.get_mark e), VarSet.empty + Bindlib.box (ERaise except, Marked.get_mark e), MVarSet.empty | ECatch (e1, except, e2) -> - let new_e1, free_vars1 = closure_conversion_expr ctx e1 in - let new_e2, free_vars2 = closure_conversion_expr ctx e2 in + let new_e1, free_vars1 = aux e1 in + let new_e2, free_vars2 = aux e2 in ( Bindlib.box_apply2 (fun new_e1 new_e2 -> ECatch (new_e1, except, new_e2), Marked.get_mark e) new_e1 new_e2, - VarSet.union free_vars1 free_vars2 ) + MVarSet.union free_vars1 free_vars2 ) + in + let e', _vars = aux e in + e' -let closure_conversion (p : program) : program Bindlib.box = +let closure_conversion (p : 'm program) : 'm program Bindlib.box = let new_scopes, _ = D.fold_left_scope_defs - ~f: - (fun ((acc_new_scopes, global_vars) : - (expr D.scopes Bindlib.box -> expr D.scopes Bindlib.box) - * VarSet.t) (scope : expr D.scope_def) (scope_var : Var.t) -> + ~f:(fun (acc_new_scopes, global_vars) scope scope_var -> (* [acc_new_scopes] represents what has been translated in the past, it needs a continuation to attach the rest of the translated scopes. *) let scope_input_var, scope_body_expr = Bindlib.unbind scope.scope_body.scope_body_expr in - let global_vars = VarSet.add scope_var global_vars in + let global_vars = VarSet.add (Var.t scope_var) global_vars in let ctx = { name_context = @@ -288,7 +292,8 @@ let closure_conversion (p : program) : program Bindlib.box = in let new_scope_lets = D.map_exprs_in_scope_lets - ~f:(fun e -> fst (closure_conversion_expr ctx e)) + ~f:(closure_conversion_expr ctx) + ~varf:(fun v -> v) scope_body_expr in let new_scope_body_expr = diff --git a/compiler/lcalc/closure_conversion.mli b/compiler/lcalc/closure_conversion.mli new file mode 100644 index 00000000..de2a1f6d --- /dev/null +++ b/compiler/lcalc/closure_conversion.mli @@ -0,0 +1,19 @@ +(* This file is part of the Catala compiler, a specification language for tax + and social benefits computation rules. Copyright (C) 2022 Inria, contributor: + Denis Merigoux + + Licensed under the Apache License, Version 2.0 (the "License"); you may not + use this file except in compliance with the License. You may obtain a copy of + the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, WITHOUT + WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the + License for the specific language governing permissions and limitations under + the License. *) + +val closure_conversion: 'm Ast.program -> 'm Ast.program Bindlib.box +(** Warning/todo: no effort was yet made to ensure + correct propagation of type annotations in the typed case *) diff --git a/compiler/lcalc/compile_with_exceptions.ml b/compiler/lcalc/compile_with_exceptions.ml index c9c6cd98..c61da45b 100644 --- a/compiler/lcalc/compile_with_exceptions.ml +++ b/compiler/lcalc/compile_with_exceptions.ml @@ -18,11 +18,11 @@ open Utils module D = Dcalc.Ast module A = Ast -type ctx = A.Var.t D.VarMap.t +type 'm ctx = 'm A.var D.VarMap.t (** This environment contains a mapping between the variables in Dcalc and their correspondance in Lcalc. *) -let translate_lit (l : D.lit) : A.expr = +let translate_lit (l : D.lit) : 'm A.expr = match l with | D.LBool l -> A.ELit (A.LBool l) | D.LInt i -> A.ELit (A.LInt i) @@ -33,38 +33,38 @@ let translate_lit (l : D.lit) : A.expr = | D.LDuration d -> A.ELit (A.LDuration d) | D.LEmptyError -> A.ERaise A.EmptyError -let thunk_expr (e : A.expr Marked.pos Bindlib.box) (pos : Pos.t) : - A.expr Marked.pos Bindlib.box = - let dummy_var = A.Var.make "_" in - A.make_abs [| dummy_var |] e [D.TAny, pos] pos +let thunk_expr (e : 'm A.marked_expr Bindlib.box) (mark: 'm A.mark) : + 'm A.marked_expr Bindlib.box = + let dummy_var = A.new_var "_" in + A.make_abs [| dummy_var |] e [D.TAny, D.mark_pos mark] mark let rec translate_default - (ctx : ctx) - (exceptions : D.expr Marked.pos list) - (just : D.expr Marked.pos) - (cons : D.expr Marked.pos) - (pos_default : Pos.t) : A.expr Marked.pos Bindlib.box = + (ctx : 'm ctx) + (exceptions : 'm D.marked_expr list) + (just : 'm D.marked_expr) + (cons : 'm D.marked_expr) + (mark_default : 'm D.mark) : 'm A.marked_expr Bindlib.box = let exceptions = List.map - (fun except -> thunk_expr (translate_expr ctx except) pos_default) + (fun except -> thunk_expr (translate_expr ctx except) mark_default) exceptions in let exceptions = A.make_app - (A.make_var (A.handle_default, pos_default)) + (A.make_var (A.Var.get A.handle_default, mark_default)) [ - A.earray exceptions pos_default; - thunk_expr (translate_expr ctx just) pos_default; - thunk_expr (translate_expr ctx cons) pos_default; + A.earray exceptions mark_default; + thunk_expr (translate_expr ctx just) mark_default; + thunk_expr (translate_expr ctx cons) mark_default; ] - pos_default + mark_default in exceptions -and translate_expr (ctx : ctx) (e : D.expr Marked.pos) : - A.expr Marked.pos Bindlib.box = +and translate_expr (ctx : 'm ctx) (e : 'm D.marked_expr) : + 'm A.marked_expr Bindlib.box = match Marked.unmark e with - | D.EVar v -> A.make_var (D.VarMap.find v ctx, Marked.get_mark e) + | D.EVar v -> A.make_var (D.VarMap.find (D.Var.t v) ctx, Marked.get_mark e) | D.ETuple (args, s) -> A.etuple (List.map (translate_expr ctx) args) s (Marked.get_mark e) | D.ETupleAccess (e1, i, s, ts) -> @@ -96,8 +96,8 @@ and translate_expr (ctx : ctx) (e : D.expr Marked.pos) : let ctx, lc_vars = Array.fold_right (fun var (ctx, lc_vars) -> - let lc_var = A.Var.make (Bindlib.name_of var) in - D.VarMap.add var lc_var ctx, lc_var :: lc_vars) + let lc_var = A.new_var (Bindlib.name_of var) in + D.VarMap.add (D.Var.t var) lc_var ctx, lc_var :: lc_vars) vars (ctx, []) in let lc_vars = Array.of_list lc_vars in @@ -117,18 +117,18 @@ and translate_expr (ctx : ctx) (e : D.expr Marked.pos) : let rec translate_scope_lets (decl_ctx : D.decl_ctx) - (ctx : A.Var.t D.VarMap.t) - (scope_lets : D.expr D.scope_body_expr) : - A.expr D.scope_body_expr Bindlib.box = + (ctx : 'm ctx) + (scope_lets : ('m D.expr, 'm) D.scope_body_expr) : + ('m A.expr, 'm) D.scope_body_expr Bindlib.box = match scope_lets with | Result e -> Bindlib.box_apply (fun e -> D.Result e) (translate_expr ctx e) | ScopeLet scope_let -> let old_scope_let_var, scope_let_next = Bindlib.unbind scope_let.scope_let_next in - let new_scope_let_var = A.Var.make (Bindlib.name_of old_scope_let_var) in + let new_scope_let_var = A.new_var (Bindlib.name_of old_scope_let_var) in let new_scope_let_expr = translate_expr ctx scope_let.scope_let_expr in - let new_ctx = D.VarMap.add old_scope_let_var new_scope_let_var ctx in + let new_ctx = D.VarMap.add (D.Var.t old_scope_let_var) new_scope_let_var ctx in let new_scope_next = translate_scope_lets decl_ctx new_ctx scope_let_next in let new_scope_next = Bindlib.bind_var new_scope_let_var new_scope_next in Bindlib.box_apply2 @@ -145,29 +145,29 @@ let rec translate_scope_lets let rec translate_scopes (decl_ctx : D.decl_ctx) - (ctx : A.Var.t D.VarMap.t) - (scopes : D.expr D.scopes) : A.expr D.scopes Bindlib.box = + (ctx : 'm ctx) + (scopes : ('m D.expr, 'm) D.scopes) : ('m A.expr, 'm) D.scopes Bindlib.box = match scopes with | Nil -> Bindlib.box D.Nil | ScopeDef scope_def -> let old_scope_var, scope_next = Bindlib.unbind scope_def.scope_next in let new_scope_var = - A.Var.make (Marked.unmark (D.ScopeName.get_info scope_def.scope_name)) + A.new_var (Marked.unmark (D.ScopeName.get_info scope_def.scope_name)) in let old_scope_input_var, scope_body_expr = Bindlib.unbind scope_def.scope_body.scope_body_expr in let new_scope_input_var = - A.Var.make (Bindlib.name_of old_scope_input_var) + A.new_var (Bindlib.name_of old_scope_input_var) in - let new_ctx = D.VarMap.add old_scope_input_var new_scope_input_var ctx in + let new_ctx = D.VarMap.add (D.Var.t old_scope_input_var) new_scope_input_var ctx in let new_scope_body_expr = translate_scope_lets decl_ctx new_ctx scope_body_expr in let new_scope_body_expr = Bindlib.bind_var new_scope_input_var new_scope_body_expr in - let new_scope : A.expr D.scope_body Bindlib.box = + let new_scope : ('m A.expr, 'm) D.scope_body Bindlib.box = Bindlib.box_apply (fun new_scope_body_expr -> { @@ -179,7 +179,7 @@ let rec translate_scopes }) new_scope_body_expr in - let new_ctx = D.VarMap.add old_scope_var new_scope_var new_ctx in + let new_ctx = D.VarMap.add (D.Var.t old_scope_var) new_scope_var new_ctx in let scope_next = Bindlib.bind_var new_scope_var (translate_scopes decl_ctx new_ctx scope_next) @@ -194,7 +194,7 @@ let rec translate_scopes }) new_scope scope_next -let translate_program (prgm : D.program) : A.program = +let translate_program (prgm : 'm D.program) : 'm A.program = { scopes = Bindlib.unbox (translate_scopes prgm.decl_ctx D.VarMap.empty prgm.scopes); diff --git a/compiler/lcalc/compile_with_exceptions.mli b/compiler/lcalc/compile_with_exceptions.mli index 924f2a09..da0f4d78 100644 --- a/compiler/lcalc/compile_with_exceptions.mli +++ b/compiler/lcalc/compile_with_exceptions.mli @@ -15,6 +15,6 @@ the License. *) (** Translation from the default calculus to the lambda calculus. This - translation uses exceptions handle empty default terms. *) + translation uses exceptions to handle empty default terms. *) -val translate_program : Dcalc.Ast.typed Dcalc.Ast.program -> Ast.program +val translate_program : 'm Dcalc.Ast.program -> 'm Ast.program diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml index e751bafa..1930d0c0 100644 --- a/compiler/lcalc/compile_without_exceptions.ml +++ b/compiler/lcalc/compile_without_exceptions.ml @@ -40,12 +40,12 @@ module A = Ast hoisted and later handled by the [translate_expr] function. Every other cases is found in the translate_and_hoist function. *) -type hoists = D.expr Marked.pos A.VarMap.t +type 'm hoists = 'm D.marked_expr A.VarMap.t (** Hoists definition. It represent bindings between [A.Var.t] and [D.expr]. *) -type info = { - expr : A.expr Marked.pos Bindlib.box; - var : A.expr Bindlib.var; +type 'm info = { + expr : 'm A.marked_expr Bindlib.box; + var : 'm A.expr Bindlib.var; is_pure : bool; } (** Information about each encontered Dcalc variable is stored inside a context @@ -54,19 +54,19 @@ type info = { indicating whenever the variable can be an EmptyError and hence should be matched (false) or if it never can be EmptyError (true). *) -let pp_info (fmt : Format.formatter) (info : info) = +let pp_info (fmt : Format.formatter) (info : 'm info) = Format.fprintf fmt "{var: %a; is_pure: %b}" Print.format_var info.var info.is_pure -type ctx = { +type 'm ctx = { decl_ctx : D.decl_ctx; - vars : info D.VarMap.t; + vars : 'm info D.VarMap.t; (** information context about variables in the current scope *) } -let _pp_ctx (fmt : Format.formatter) (ctx : ctx) = - let pp_binding (fmt : Format.formatter) ((v, info) : D.Var.t * info) = - Format.fprintf fmt "%a: %a" Dcalc.Print.format_var v pp_info info +let _pp_ctx (fmt : Format.formatter) (ctx : 'm ctx) = + let pp_binding (fmt : Format.formatter) ((v, info) : D.Var.t * 'm info) = + Format.fprintf fmt "%a: %a" Dcalc.Print.format_var (D.Var.get v) pp_info info in let pp_bindings = @@ -79,10 +79,10 @@ let _pp_ctx (fmt : Format.formatter) (ctx : ctx) = (** [find ~info n ctx] is a warpper to ocaml's Map.find that handle errors in a slightly better way. *) -let find ?(info : string = "none") (n : D.Var.t) (ctx : ctx) : info = +let find ?(info : string = "none") (n : 'm D.var) (ctx : 'm ctx) : 'm info = (* let _ = Format.asprintf "Searching for variable %a inside context %a" Dcalc.Print.format_var n pp_ctx ctx |> Cli.debug_print in *) - try D.VarMap.find n ctx.vars + try D.VarMap.find (D.Var.t n) ctx.vars with Not_found -> Errors.raise_spanned_error Pos.no_pos "Internal Error: Variable %a was not found in the current environment. \ @@ -93,16 +93,16 @@ let find ?(info : string = "none") (n : D.Var.t) (ctx : ctx) : info = var, creating a unique corresponding variable in Lcalc, with the corresponding expression, and the boolean is_pure. It is usefull for debuging purposes as it printing each of the Dcalc/Lcalc variable pairs. *) -let add_var (pos : Pos.t) (var : D.Var.t) (is_pure : bool) (ctx : ctx) : ctx = - let new_var = A.Var.make (Bindlib.name_of var) in - let expr = A.make_var (new_var, pos) in +let add_var (mark : 'm D.mark) (var : 'm D.var) (is_pure : bool) (ctx : 'm ctx) : 'm ctx = + let new_var = A.new_var (Bindlib.name_of var) in + let expr = A.make_var (new_var, mark) in (* Cli.debug_print @@ Format.asprintf "D.%a |-> A.%a" Dcalc.Print.format_var var Print.format_var new_var; *) { ctx with vars = - D.VarMap.update var + D.VarMap.update (D.Var.t var) (fun _ -> Some { expr; var = new_var; is_pure }) ctx.vars; } @@ -161,8 +161,8 @@ let disjoint_union_maps (pos : Pos.t) (cs : 'a A.VarMap.t list) : 'a A.VarMap.t the equivalence between the execution of e and the execution of e' are equivalent in an environement where each variable v, where (v, e_v) is in hoists, has the non-empty value in e_v. *) -let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) : - A.expr Marked.pos Bindlib.box * hoists = +let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.marked_expr) : + 'm A.marked_expr Bindlib.box * 'm hoists = let pos = Marked.get_mark e in match Marked.unmark e with (* empty-producing/using terms. We hoist those. (D.EVar in some cases, @@ -174,46 +174,46 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) : assumption can change in the future, and this case is here for this reason. *) if not (find ~info:"search for a variable" v ctx).is_pure then - let v' = A.Var.make (Bindlib.name_of v) in + let v' = A.new_var (Bindlib.name_of v) in (* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a, created a variable %a to replace it" Dcalc.Print.format_var v Print.format_var v'; *) - A.make_var (v', pos), A.VarMap.singleton v' e + A.make_var (v', pos), A.VarMap.singleton (A.Var.t v') e else (find ~info:"should never happend" v ctx).expr, A.VarMap.empty | D.EApp ((D.EVar v, p), [(D.ELit D.LUnit, _)]) -> if not (find ~info:"search for a variable" v ctx).is_pure then - let v' = A.Var.make (Bindlib.name_of v) in + let v' = A.new_var (Bindlib.name_of v) in (* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a, created a variable %a to replace it" Dcalc.Print.format_var v Print.format_var v'; *) - A.make_var (v', pos), A.VarMap.singleton v' (D.EVar v, p) + A.make_var (v', pos), A.VarMap.singleton (A.Var.t v') (D.EVar v, p) else - Errors.raise_spanned_error pos + Errors.raise_spanned_error (D.pos e) "Internal error: an pure variable was found in an unpure environment." | D.EDefault (_exceptions, _just, _cons) -> - let v' = A.Var.make "default_term" in - A.make_var (v', pos), A.VarMap.singleton v' e + let v' = A.new_var "default_term" in + A.make_var (v', pos), A.VarMap.singleton (A.Var.t v') e | D.ELit D.LEmptyError -> - let v' = A.Var.make "empty_litteral" in - A.make_var (v', pos), A.VarMap.singleton v' e + let v' = A.new_var "empty_litteral" in + A.make_var (v', pos), A.VarMap.singleton (A.Var.t v') e (* This one is a very special case. It transform an unpure expression environement to a pure expression. *) | ErrorOnEmpty arg -> (* [ match arg with | None -> raise NoValueProvided | Some v -> {{ v }} ] *) - let silent_var = A.Var.make "_" in - let x = A.Var.make "non_empty_argument" in + let silent_var = A.new_var "_" in + let x = A.new_var "non_empty_argument" in let arg' = translate_expr ctx arg in ( A.make_matchopt_with_abs_arms arg' (A.make_abs [| silent_var |] (Bindlib.box (A.ERaise A.NoValueProvided, pos)) - [D.TAny, pos] + [D.TAny, D.pos e] pos) - (A.make_abs [| x |] (A.make_var (x, pos)) [D.TAny, pos] pos), + (A.make_abs [| x |] (A.make_var (x, pos)) [D.TAny, D.pos e] pos), A.VarMap.empty ) (* pure terms *) - | D.ELit l -> A.elit (translate_lit l pos) pos, A.VarMap.empty + | D.ELit l -> A.elit (translate_lit l (D.pos e)) pos, A.VarMap.empty | D.EIfThenElse (e1, e2, e3) -> let e1', h1 = translate_and_hoist ctx e1 in let e2', h2 = translate_and_hoist ctx e2 in @@ -223,7 +223,7 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) : (*(* equivalent code : *) let e' = let+ e1' = e1' and+ e2' = e2' and+ e3' = e3' in (A.EIfThenElse (e1', e2', e3'), pos) in *) - e', disjoint_union_maps pos [h1; h2; h3] + e', disjoint_union_maps (D.pos e) [h1; h2; h3] | D.EAssert e1 -> (* same behavior as in the ICFP paper: if e1 is empty, then no error is raised. *) @@ -260,7 +260,7 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) : args |> List.map (translate_and_hoist ctx) |> List.split in - let hoists = disjoint_union_maps pos (h1 :: h_args) in + let hoists = disjoint_union_maps (D.pos e) (h1 :: h_args) in let e' = A.eapp e1' args' pos in e', hoists | ETuple (args, s) -> @@ -268,7 +268,7 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) : args |> List.map (translate_and_hoist ctx) |> List.split in - let hoists = disjoint_union_maps pos h_args in + let hoists = disjoint_union_maps (D.pos e) h_args in A.etuple args' s pos, hoists | ETupleAccess (e1, i, s, ts) -> let e1', hoists = translate_and_hoist ctx e1 in @@ -284,17 +284,17 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) : cases |> List.map (translate_and_hoist ctx) |> List.split in - let hoists = disjoint_union_maps pos (h1 :: h_cases) in + let hoists = disjoint_union_maps (D.pos e) (h1 :: h_cases) in let e' = A.ematch e1' cases' en pos in e', hoists | EArray es -> let es', hoists = es |> List.map (translate_and_hoist ctx) |> List.split in - A.earray es' pos, disjoint_union_maps pos hoists + A.earray es' pos, disjoint_union_maps (D.pos e) hoists | EOp op -> Bindlib.box (A.EOp op, pos), A.VarMap.empty -and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Marked.pos) : - A.expr Marked.pos Bindlib.box = +and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.marked_expr) : + 'm A.marked_expr Bindlib.box = let e', hoists = translate_and_hoist ctx e in let hoists = A.VarMap.bindings hoists in @@ -305,10 +305,10 @@ and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Marked.pos) : (Format.pp_print_list Print.format_var) (List.map fst hoists); *) ListLabels.fold_left hoists ~init:(if append_esome then A.make_some e' else e') - ~f:(fun acc (v, (hoist, pos_hoist)) -> + ~f:(fun acc (v, (hoist, mark_hoist)) -> (* Cli.debug_print @@ Format.asprintf "hoist using A.%a" Print.format_var v; *) - let c' : A.expr Marked.pos Bindlib.box = + let c' : 'm A.marked_expr Bindlib.box = match hoist with (* Here we have to handle only the cases appearing in hoists, as defined the [translate_and_hoist] function. *) @@ -319,37 +319,37 @@ and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Marked.pos) : let cons' = translate_expr ctx cons in (* calls handle_option. *) A.make_app - (A.make_var (A.handle_default_opt, pos_hoist)) + (A.make_var (A.Var.get A.handle_default_opt, mark_hoist)) [ Bindlib.box_apply - (fun excep' -> A.EArray excep', pos_hoist) + (fun excep' -> A.EArray excep', mark_hoist) (Bindlib.box_list excep'); just'; cons'; ] - pos_hoist - | D.ELit D.LEmptyError -> A.make_none pos_hoist + mark_hoist + | D.ELit D.LEmptyError -> A.make_none mark_hoist | D.EAssert arg -> let arg' = translate_expr ctx arg in (* [ match arg with | None -> raise NoValueProvided | Some v -> assert {{ v }} ] *) - let silent_var = A.Var.make "_" in - let x = A.Var.make "assertion_argument" in + let silent_var = A.new_var "_" in + let x = A.new_var "assertion_argument" in A.make_matchopt_with_abs_arms arg' (A.make_abs [| silent_var |] - (Bindlib.box (A.ERaise A.NoValueProvided, pos_hoist)) - [D.TAny, pos_hoist] - pos_hoist) + (Bindlib.box (A.ERaise A.NoValueProvided, mark_hoist)) + [D.TAny, D.mark_pos mark_hoist] + mark_hoist) (A.make_abs [| x |] (Bindlib.box_apply - (fun arg -> A.EAssert arg, pos_hoist) - (A.make_var (x, pos_hoist))) - [D.TAny, pos_hoist] - pos_hoist) + (fun arg -> A.EAssert arg, mark_hoist) + (A.make_var (x, mark_hoist))) + [D.TAny, D.mark_pos mark_hoist] + mark_hoist) | _ -> - Errors.raise_spanned_error pos_hoist + Errors.raise_spanned_error (D.mark_pos mark_hoist) "Internal Error: An term was found in a position where it should \ not be" in @@ -358,11 +358,11 @@ and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Marked.pos) : ] *) (* Cli.debug_print @@ Format.asprintf "build matchopt using %a" Print.format_var v; *) - A.make_matchopt pos_hoist v (D.TAny, pos_hoist) c' (A.make_none pos_hoist) + A.make_matchopt mark_hoist (A.Var.get v) (D.TAny, D.mark_pos mark_hoist) c' (A.make_none mark_hoist) acc) -let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) : - A.expr D.scope_body_expr Bindlib.box = +let rec translate_scope_let (ctx : 'm ctx) (lets : ('m D.expr, 'm) D.scope_body_expr) : + ('m A.expr, 'm) D.scope_body_expr Bindlib.box = match lets with | Result e -> Bindlib.box_apply @@ -372,7 +372,7 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) : { scope_let_kind = SubScopeVarDefinition; scope_let_typ = typ; - scope_let_expr = D.EAbs (binder, _), _; + scope_let_expr = D.EAbs (binder, _), emark; scope_let_next = next; scope_let_pos = pos; } -> @@ -384,7 +384,10 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) : let var, next = Bindlib.unbind next in (* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var var; *) - let ctx' = add_var pos var var_is_pure ctx in + let vmark = + D.map_mark (fun _ -> pos) (fun _ -> D.Infer.ast_to_typ typ) emark + in + let ctx' = add_var vmark var var_is_pure ctx in let new_var = (find ~info:"variable that was just created" var ctx').var in let new_next = translate_scope_let ctx' next in Bindlib.box_apply2 @@ -403,7 +406,7 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) : { scope_let_kind = SubScopeVarDefinition; scope_let_typ = typ; - scope_let_expr = (D.ErrorOnEmpty _, _) as expr; + scope_let_expr = (D.ErrorOnEmpty _, emark) as expr; scope_let_next = next; scope_let_pos = pos; } -> @@ -412,7 +415,10 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) : let var, next = Bindlib.unbind next in (* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var var; *) - let ctx' = add_var pos var var_is_pure ctx in + let vmark = + D.map_mark (fun _ -> pos) (fun _ -> D.Infer.ast_to_typ typ) emark + in + let ctx' = add_var vmark var var_is_pure ctx in let new_var = (find ~info:"variable that was just created" var ctx').var in Bindlib.box_apply2 (fun new_expr new_next -> @@ -464,7 +470,10 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) : let var, next = Bindlib.unbind next in (* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var var; *) - let ctx' = add_var pos var var_is_pure ctx in + let vmark = + D.map_mark (fun _ -> pos) (fun _ -> D.Infer.ast_to_typ typ) (Marked.get_mark expr) + in + let ctx' = add_var vmark var var_is_pure ctx in let new_var = (find ~info:"variable that was just created" var ctx').var in Bindlib.box_apply2 (fun new_expr new_next -> @@ -481,8 +490,8 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) : let translate_scope_body (scope_pos : Pos.t) - (ctx : ctx) - (body : D.expr D.scope_body) : A.expr D.scope_body Bindlib.box = + (ctx : 'm ctx) + (body : ('m D.expr, 'm) D.scope_body) : ('m A.expr, 'm) D.scope_body Bindlib.box = match body with | { scope_body_expr = result; @@ -490,7 +499,11 @@ let translate_scope_body scope_body_output_struct = output_struct; } -> let v, lets = Bindlib.unbind result in - let ctx' = add_var scope_pos v true ctx in + let vmark = + let m = match lets with Result e | ScopeLet { scope_let_expr=e; _} -> Marked.get_mark e in + D.map_mark (fun _ -> scope_pos) (fun ty -> ty) m + in + let ctx' = add_var vmark v true ctx in let v' = (find ~info:"variable that was just created" v ctx').var in Bindlib.box_apply (fun new_expr -> @@ -501,13 +514,17 @@ let translate_scope_body }) (Bindlib.bind_var v' (translate_scope_let ctx' lets)) -let rec translate_scopes (ctx : ctx) (scopes : D.expr D.scopes) : - A.expr D.scopes Bindlib.box = +let rec translate_scopes (ctx : 'm ctx) (scopes : ('m D.expr, 'm) D.scopes) : + ('m A.expr, 'm) D.scopes Bindlib.box = match scopes with | Nil -> Bindlib.box D.Nil | ScopeDef { scope_name; scope_body; scope_next } -> let scope_var, next = Bindlib.unbind scope_next in - let new_ctx = add_var Pos.no_pos scope_var true ctx in + let vmark = + match Bindlib.unbind scope_body.scope_body_expr with _, (Result e | ScopeLet { scope_let_expr=e; _}) -> Marked.get_mark e + in + + let new_ctx = add_var vmark scope_var true ctx in let new_scope_name = (find ~info:"variable that was just created" scope_var new_ctx).var in @@ -523,7 +540,7 @@ let rec translate_scopes (ctx : ctx) (scopes : D.expr D.scopes) : new_body (Bindlib.bind_var new_scope_name tail) -let translate_program (prgm : D.program) : A.program = +let translate_program (prgm : 'm D.program) : 'm A.program = let inputs_structs = D.fold_left_scope_defs prgm.scopes ~init:[] ~f:(fun acc scope_def _ -> scope_def.D.scope_body.scope_body_input_struct :: acc) diff --git a/compiler/lcalc/compile_without_exceptions.mli b/compiler/lcalc/compile_without_exceptions.mli index 4f513103..6bb2b18d 100644 --- a/compiler/lcalc/compile_without_exceptions.mli +++ b/compiler/lcalc/compile_without_exceptions.mli @@ -19,4 +19,4 @@ transformation is one piece to permit to compile toward legacy languages that does not contains exceptions. *) -val translate_program : Dcalc.Ast.typed Dcalc.Ast.program -> Ast.program +val translate_program : 'm Dcalc.Ast.program -> 'm Ast.program diff --git a/compiler/lcalc/optimizations.ml b/compiler/lcalc/optimizations.ml index b4efd07f..fec01d55 100644 --- a/compiler/lcalc/optimizations.ml +++ b/compiler/lcalc/optimizations.ml @@ -20,9 +20,9 @@ let ( let+ ) x f = Bindlib.box_apply f x let ( and+ ) x y = Bindlib.box_pair x y let visitor_map - (t : 'a -> expr Marked.pos -> expr Marked.pos Bindlib.box) + (t : 'a -> 'm marked_expr -> 'm marked_expr Bindlib.box) (ctx : 'a) - (e : expr Marked.pos) : expr Marked.pos Bindlib.box = + (e : 'm marked_expr) : 'm marked_expr Bindlib.box = (* calls [t ctx] on every direct childs of [e], then rebuild an abstract syntax tree modified. Used in other transformations. *) let default_mark e' = Marked.same_mark_as e' e in @@ -66,7 +66,7 @@ let visitor_map default_mark @@ ECatch (e1, exn, e2) | ERaise _ | ELit _ | EOp _ -> Bindlib.box e -let rec iota_expr (_ : unit) (e : expr Marked.pos) : expr Marked.pos Bindlib.box +let rec iota_expr (_ : unit) (e : 'm marked_expr) : 'm marked_expr Bindlib.box = let default_mark e' = Marked.mark (Marked.get_mark e) e' in match Marked.unmark e with @@ -86,7 +86,7 @@ let rec iota_expr (_ : unit) (e : expr Marked.pos) : expr Marked.pos Bindlib.box visitor_map iota_expr () e' | _ -> visitor_map iota_expr () e -let rec beta_expr (_ : unit) (e : expr Marked.pos) : expr Marked.pos Bindlib.box +let rec beta_expr (_ : unit) (e : 'm marked_expr) : 'm marked_expr Bindlib.box = let default_mark e' = Marked.same_mark_as e' e in match Marked.unmark e with @@ -100,20 +100,20 @@ let rec beta_expr (_ : unit) (e : expr Marked.pos) : expr Marked.pos Bindlib.box | _ -> default_mark @@ EApp (e1, args)) | _ -> visitor_map beta_expr () e -let iota_optimizations (p : program) : program = - let new_scopes = Dcalc.Ast.map_exprs_in_scopes ~f:(iota_expr ()) p.scopes in +let iota_optimizations (p : 'm program) : 'm program = + let new_scopes = Dcalc.Ast.map_exprs_in_scopes ~f:(iota_expr ()) ~varf:(fun v -> v) p.scopes in { p with scopes = Bindlib.unbox new_scopes } (* TODO: beta optimizations apply inlining of the program. We left the inclusion of beta-optimization as future work since its produce code that is harder to read, and can produce exponential blowup of the size of the generated program. *) -let _beta_optimizations (p : program) : program = - let new_scopes = Dcalc.Ast.map_exprs_in_scopes ~f:(beta_expr ()) p.scopes in +let _beta_optimizations (p : 'm program) : 'm program = + let new_scopes = Dcalc.Ast.map_exprs_in_scopes ~f:(beta_expr ()) ~varf:(fun v -> v) p.scopes in { p with scopes = Bindlib.unbox new_scopes } -let rec peephole_expr (_ : unit) (e : expr Marked.pos) : - expr Marked.pos Bindlib.box = +let rec peephole_expr (_ : unit) (e : 'm marked_expr) : + 'm marked_expr Bindlib.box = let default_mark e' = Marked.mark (Marked.get_mark e) e' in match Marked.unmark e with @@ -140,11 +140,11 @@ let rec peephole_expr (_ : unit) (e : expr Marked.pos) : | _ -> default_mark @@ ECatch (e1, except, e2)) | _ -> visitor_map peephole_expr () e -let peephole_optimizations (p : program) : program = +let peephole_optimizations (p : 'm program) : 'm program = let new_scopes = - Dcalc.Ast.map_exprs_in_scopes ~f:(peephole_expr ()) p.scopes + Dcalc.Ast.map_exprs_in_scopes ~f:(peephole_expr ()) ~varf:(fun v -> v) p.scopes in { p with scopes = Bindlib.unbox new_scopes } -let optimize_program (p : program) : program = +let optimize_program (p : 'm program) : 'm program = p |> iota_optimizations |> peephole_optimizations diff --git a/compiler/lcalc/optimizations.mli b/compiler/lcalc/optimizations.mli index 4e7ab958..30e15a3a 100644 --- a/compiler/lcalc/optimizations.mli +++ b/compiler/lcalc/optimizations.mli @@ -16,4 +16,6 @@ open Ast -val optimize_program : program -> program +val optimize_program : 'm program -> 'm program +(** Warning/todo: no effort was yet made to ensure + correct propagation of type annotations in the typed case *) diff --git a/compiler/lcalc/print.ml b/compiler/lcalc/print.ml index 6214a3ad..4bfa6fdc 100644 --- a/compiler/lcalc/print.ml +++ b/compiler/lcalc/print.ml @@ -68,19 +68,19 @@ let format_keyword (fmt : Format.formatter) (s : string) : unit = let format_punctuation (fmt : Format.formatter) (s : string) : unit = Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ANSITerminal.cyan]) s -let needs_parens (e : expr Marked.pos) : bool = +let needs_parens (e : 'm marked_expr) : bool = match Marked.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false -let format_var (fmt : Format.formatter) (v : Var.t) : unit = +let format_var (fmt : Format.formatter) (v : 'm Ast.var) : unit = Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v) let rec format_expr ?(debug : bool = false) (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) - (e : expr Marked.pos) : unit = + (e : 'm marked_expr) : unit = let format_expr = format_expr ctx ~debug in - let format_with_parens (fmt : Format.formatter) (e : expr Marked.pos) = + let format_with_parens (fmt : Format.formatter) (e : 'm marked_expr) = if needs_parens e then Format.fprintf fmt "%a%a%a" format_punctuation "(" format_expr e format_punctuation ")" @@ -136,23 +136,21 @@ let rec format_expr format_expr e)) (List.combine es (List.map fst (Dcalc.Ast.EnumMap.find e_name ctx.ctx_enums))) - | ELit l -> Format.fprintf fmt "%a" format_lit (Marked.same_mark_as l e) + | ELit l -> Format.fprintf fmt "%a" format_lit (Marked.mark (Dcalc.Ast.pos e) l) | EApp ((EAbs (binder, taus), _), args) -> let xs, body = Bindlib.unmbind binder in - let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in - let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in Format.fprintf fmt "%a%a" (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "") - (fun fmt (x, tau, arg) -> + (fun fmt ((x, tau), arg) -> Format.fprintf fmt "@[%a@ %a@ %a@ %a@ %a@ %a@ %a@]@\n" format_keyword "let" format_var x format_punctuation ":" (Dcalc.Print.format_typ ctx) - tau format_punctuation "=" format_expr arg format_keyword "in")) - xs_tau_arg format_expr body + (Marked.unmark tau) format_punctuation "=" format_expr arg format_keyword "in")) + (List.combine (List.combine (Array.to_list xs) taus) args) + format_expr body | EAbs (binder, taus) -> let xs, body = Bindlib.unmbind binder in - let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in Format.fprintf fmt "@[%a %a %a@ %a@]" format_punctuation "λ" (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") @@ -160,21 +158,22 @@ let rec format_expr Format.fprintf fmt "%a%a%a %a%a" format_punctuation "(" format_var x format_punctuation ":" (Dcalc.Print.format_typ ctx) - tau format_punctuation ")")) - xs_tau format_punctuation "→" format_expr body + (Marked.unmark tau) format_punctuation ")")) + (List.combine (Array.to_list xs) taus) + format_punctuation "→" format_expr body | EApp ((EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _), [arg1; arg2]) -> Format.fprintf fmt "@[%a@ %a@ %a@]" Dcalc.Print.format_binop - (op, Pos.no_pos) format_with_parens arg1 format_with_parens arg2 + op format_with_parens arg1 format_with_parens arg2 | EApp ((EOp (Binop op), _), [arg1; arg2]) -> Format.fprintf fmt "@[%a@ %a@ %a@]" format_with_parens arg1 - Dcalc.Print.format_binop (op, Pos.no_pos) format_with_parens arg2 + Dcalc.Print.format_binop op format_with_parens arg2 | EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug -> Format.fprintf fmt "%a" format_with_parens arg1 | EApp ((EOp (Unop op), _), [arg1]) -> Format.fprintf fmt "@[%a@ %a@]" Dcalc.Print.format_unop - (op, Pos.no_pos) format_with_parens arg1 + op format_with_parens arg1 | EApp (f, args) -> Format.fprintf fmt "@[%a@ %a@]" format_expr f (Format.pp_print_list @@ -186,11 +185,11 @@ let rec format_expr format_expr e1 format_keyword "then" format_expr e2 format_keyword "else" format_expr e3 | EOp (Ternop op) -> - Format.fprintf fmt "%a" Dcalc.Print.format_ternop (op, Pos.no_pos) + Format.fprintf fmt "%a" Dcalc.Print.format_ternop op | EOp (Binop op) -> - Format.fprintf fmt "%a" Dcalc.Print.format_binop (op, Pos.no_pos) + Format.fprintf fmt "%a" Dcalc.Print.format_binop op | EOp (Unop op) -> - Format.fprintf fmt "%a" Dcalc.Print.format_unop (op, Pos.no_pos) + Format.fprintf fmt "%a" Dcalc.Print.format_unop op | ECatch (e1, exn, e2) -> Format.fprintf fmt "@[%a@ %a@ %a@ %a ->@ %a@]" format_keyword "try" format_with_parens e1 format_keyword "with" format_exception exn @@ -202,14 +201,13 @@ let rec format_expr Format.fprintf fmt "@[%a@ %a%a%a@]" format_keyword "assert" format_punctuation "(" format_expr e' format_punctuation ")" -let format_scope - ?(debug : bool = false) - (ctx : Dcalc.Ast.decl_ctx) - (fmt : Format.formatter) - ((n, s) : Dcalc.Ast.ScopeName.t * Ast.expr Dcalc.Ast.scope_body) : unit = +let format_scope ?(debug=false) ctx fmt (n, s) = Format.fprintf fmt "@[%a %a =@ %a@]" format_keyword "let" Dcalc.Ast.ScopeName.format_t n (format_expr ctx ~debug) (Bindlib.unbox (Dcalc.Ast.build_whole_scope_expr ~make_abs:Ast.make_abs ~make_let_in:Ast.make_let_in ~box_expr:Ast.box_expr ctx s - (Marked.get_mark (Dcalc.Ast.ScopeName.get_info n)))) + (Dcalc.Ast.map_mark + (fun _ -> Marked.get_mark (Dcalc.Ast.ScopeName.get_info n)) + (fun ty -> ty) + (Dcalc.Ast.get_scope_body_mark s)))) diff --git a/compiler/lcalc/print.mli b/compiler/lcalc/print.mli index 9815b88f..65d2a4ab 100644 --- a/compiler/lcalc/print.mli +++ b/compiler/lcalc/print.mli @@ -24,19 +24,19 @@ val begins_with_uppercase : string -> bool (** {1 Formatters} *) val format_lit : Format.formatter -> Ast.lit Marked.pos -> unit -val format_var : Format.formatter -> Ast.Var.t -> unit +val format_var : Format.formatter -> 'm Ast.var -> unit val format_exception : Format.formatter -> Ast.except -> unit val format_expr : ?debug:bool -> Dcalc.Ast.decl_ctx -> Format.formatter -> - Ast.expr Marked.pos -> + 'm Ast.marked_expr -> unit val format_scope : ?debug:bool -> Dcalc.Ast.decl_ctx -> Format.formatter -> - Dcalc.Ast.ScopeName.t * Ast.expr Dcalc.Ast.scope_body -> + Dcalc.Ast.ScopeName.t * ('m Ast.expr, 'm) Dcalc.Ast.scope_body -> unit diff --git a/compiler/lcalc/to_ocaml.ml b/compiler/lcalc/to_ocaml.ml index 0add392d..933fcb54 100644 --- a/compiler/lcalc/to_ocaml.ml +++ b/compiler/lcalc/to_ocaml.ml @@ -40,13 +40,13 @@ let find_enum (en : D.EnumName.t) (ctx : D.decl_ctx) : let format_lit (fmt : Format.formatter) (l : lit Marked.pos) : unit = match Marked.unmark l with | LBool b -> - Dcalc.Print.format_lit fmt (Marked.same_mark_as (Dcalc.Ast.LBool b) l) + Dcalc.Print.format_lit fmt (Dcalc.Ast.LBool b) | LInt i -> Format.fprintf fmt "integer_of_string@ \"%s\"" (Runtime.integer_to_string i) - | LUnit -> Dcalc.Print.format_lit fmt (Marked.same_mark_as Dcalc.Ast.LUnit l) + | LUnit -> Dcalc.Print.format_lit fmt Dcalc.Ast.LUnit | LRat i -> Format.fprintf fmt "decimal_of_string \"%a\"" Dcalc.Print.format_lit - (Marked.same_mark_as (Dcalc.Ast.LRat i) l) + (Dcalc.Ast.LRat i) | LMoney e -> Format.fprintf fmt "money_of_cents_string@ \"%s\"" (Runtime.integer_to_string (Runtime.money_to_cents e)) @@ -221,7 +221,7 @@ let rec format_typ (fmt : Format.formatter) (typ : Dcalc.Ast.typ Marked.pos) : | TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ_with_parens t1 | TAny -> Format.fprintf fmt "_" -let format_var (fmt : Format.formatter) (v : Var.t) : unit = +let format_var (fmt : Format.formatter) (v : 'm var) : unit = let lowercase_name = to_lowercase (to_ascii (Bindlib.name_of v)) in let lowercase_name = Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\\.") @@ -236,7 +236,7 @@ let format_var (fmt : Format.formatter) (v : Var.t) : unit = else if lowercase_name = "_" then Format.fprintf fmt "%s" lowercase_name else Format.fprintf fmt "%s_" lowercase_name -let needs_parens (e : expr Marked.pos) : bool = +let needs_parens (e : 'm marked_expr) : bool = match Marked.unmark e with | EApp ((EAbs (_, _), _), _) | ELit (LBool _ | LUnit) @@ -261,9 +261,9 @@ let format_exception (fmt : Format.formatter) (exc : except Marked.pos) : unit = let rec format_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) - (e : expr Marked.pos) : unit = + (e : 'm marked_expr) : unit = let format_expr = format_expr ctx in - let format_with_parens (fmt : Format.formatter) (e : expr Marked.pos) = + let format_with_parens (fmt : Format.formatter) (e : 'm marked_expr) = if needs_parens e then Format.fprintf fmt "(%a)" format_expr e else Format.fprintf fmt "%a" format_expr e in @@ -326,7 +326,7 @@ let rec format_expr (* should not happen *)) e)) (List.combine es (List.map fst (find_enum e_name ctx))) - | ELit l -> Format.fprintf fmt "%a" format_lit (Marked.same_mark_as l e) + | ELit l -> Format.fprintf fmt "%a" format_lit (Marked.mark (D.pos e) l) | EApp ((EAbs (binder, taus), _), args) -> let xs, body = Bindlib.unmbind binder in let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in @@ -363,8 +363,9 @@ let rec format_expr when !Cli.trace_flag -> Format.fprintf fmt "(log_variable_definition@ %a@ (%a)@ %a)" format_uid_list info typ_embedding_name (tau, Pos.no_pos) format_with_parens arg1 - | EApp ((EOp (Unop (D.Log (D.PosRecordIfTrueBool, _))), pos), [arg1]) + | EApp ((EOp (Unop (D.Log (D.PosRecordIfTrueBool, _))), m), [arg1]) when !Cli.trace_flag -> + let pos = D.mark_pos m in Format.fprintf fmt "(log_decision_taken@ @[{filename = \"%s\";@ start_line=%d;@ \ start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@]@ %a)" @@ -398,11 +399,11 @@ let rec format_expr "@[if @ %a@ then@ ()@ else@ raise AssertionFailed@]" format_with_parens e' | ERaise exc -> - Format.fprintf fmt "raise@ %a" format_exception (exc, Marked.get_mark e) + Format.fprintf fmt "raise@ %a" format_exception (exc, D.pos e) | ECatch (e1, exc, e2) -> Format.fprintf fmt "@[try@ %a@ with@ %a@ ->@ %a@]" format_with_parens e1 format_exception - (exc, Marked.get_mark e) + (exc, D.pos e) format_with_parens e2 let format_struct_embedding @@ -510,7 +511,7 @@ let format_ctx let rec format_scope_body_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) - (scope_lets : Ast.expr Dcalc.Ast.scope_body_expr) : unit = + (scope_lets : ('m Ast.expr, 'm) Dcalc.Ast.scope_body_expr) : unit = match scope_lets with | Dcalc.Ast.Result e -> format_expr ctx fmt e | Dcalc.Ast.ScopeLet scope_let -> @@ -526,7 +527,7 @@ let rec format_scope_body_expr let rec format_scopes (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) - (scopes : Ast.expr Dcalc.Ast.scopes) : unit = + (scopes : ('m Ast.expr, 'm) Dcalc.Ast.scopes) : unit = match scopes with | Dcalc.Ast.Nil -> () | Dcalc.Ast.ScopeDef scope_def -> @@ -543,7 +544,7 @@ let rec format_scopes let format_program (fmt : Format.formatter) - (p : Ast.program) + (p : 'm Ast.program) (type_ordering : Scopelang.Dependency.TVertex.t list) : unit = Cli.style_flag := false; Format.fprintf fmt diff --git a/compiler/lcalc/to_ocaml.mli b/compiler/lcalc/to_ocaml.mli index f9e22f03..f734870d 100644 --- a/compiler/lcalc/to_ocaml.mli +++ b/compiler/lcalc/to_ocaml.mli @@ -17,5 +17,5 @@ (** Formats a lambda calculus program into a valid OCaml program *) val format_program : - Format.formatter -> Ast.program -> Scopelang.Dependency.TVertex.t list -> unit + Format.formatter -> 'm Ast.program -> Scopelang.Dependency.TVertex.t list -> unit (** Usage [format_program fmt p type_dependencies_ordering] *) diff --git a/compiler/plugin.ml b/compiler/plugin.ml index 482f6936..5233d4b3 100644 --- a/compiler/plugin.ml +++ b/compiler/plugin.ml @@ -20,7 +20,7 @@ type 'ast gen = { apply : string option -> 'ast -> Scopelang.Dependency.TVertex.t list -> unit; } -type t = Lcalc of Lcalc.Ast.program gen | Scalc of Scalc.Ast.program gen +type t = Lcalc of Dcalc.Ast.typed Lcalc.Ast.program gen | Scalc of Scalc.Ast.program gen let name = function Lcalc { name; _ } | Scalc { name; _ } -> name let backend_plugins : (string, t) Hashtbl.t = Hashtbl.create 17 diff --git a/compiler/plugin.mli b/compiler/plugin.mli index 59ec7bed..3f7d0c14 100644 --- a/compiler/plugin.mli +++ b/compiler/plugin.mli @@ -22,7 +22,9 @@ type 'ast gen = { apply : string option -> 'ast -> Scopelang.Dependency.TVertex.t list -> unit; } -type t = Lcalc of Lcalc.Ast.program gen | Scalc of Scalc.Ast.program gen +type t = + | Lcalc of Dcalc.Ast.typed Lcalc.Ast.program gen + | Scalc of Scalc.Ast.program gen val find : string -> t (** Find a registered plugin *) @@ -40,7 +42,7 @@ module PluginAPI : sig name:string -> extension:string -> (string option -> - Lcalc.Ast.program -> + Dcalc.Ast.typed Lcalc.Ast.program -> Scopelang.Dependency.TVertex.t list -> unit) -> unit diff --git a/compiler/scalc/compile_from_lambda.ml b/compiler/scalc/compile_from_lambda.ml index ae9a22e1..9f81d895 100644 --- a/compiler/scalc/compile_from_lambda.ml +++ b/compiler/scalc/compile_from_lambda.ml @@ -29,15 +29,15 @@ type ctxt = { (* Expressions can spill out side effect, hence this function also returns a list of statements to be prepended before the expression is evaluated *) -let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) : +let rec translate_expr (ctxt : ctxt) (expr : 'm L.marked_expr) : A.block * A.expr Marked.pos = match Marked.unmark expr with | L.EVar v -> let local_var = - try A.EVar (L.VarMap.find v ctxt.var_dict) - with Not_found -> A.EFunc (L.VarMap.find v ctxt.func_dict) + try A.EVar (L.VarMap.find (L.Var.t v) ctxt.var_dict) + with Not_found -> A.EFunc (L.VarMap.find (L.Var.t v) ctxt.func_dict) in - [], (local_var, Marked.get_mark expr) + [], (local_var, D.pos expr) | L.ETuple (args, Some s_name) -> let args_stmts, new_args = List.fold_left @@ -48,7 +48,7 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) : in let new_args = List.rev new_args in let args_stmts = List.rev args_stmts in - args_stmts, (A.EStruct (new_args, s_name), Marked.get_mark expr) + args_stmts, (A.EStruct (new_args, s_name), D.pos expr) | L.ETuple (_, None) -> failwith "Non-struct tuples cannot be compiled to scalc" | L.ETupleAccess (e1, num_field, Some s_name, _) -> @@ -58,7 +58,7 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) : (List.nth (D.StructMap.find s_name ctxt.decl_ctx.ctx_structs) num_field) in ( e1_stmts, - (A.EStructFieldAccess (new_e1, field_name, s_name), Marked.get_mark expr) + (A.EStructFieldAccess (new_e1, field_name, s_name), D.pos expr) ) | L.ETupleAccess (_, _, None, _) -> failwith "Non-struct tuples cannot be compiled to scalc" @@ -67,7 +67,7 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) : let cons_name = fst (List.nth (D.EnumMap.find e_name ctxt.decl_ctx.ctx_enums) num_cons) in - e1_stmts, (A.EInj (new_e1, cons_name, e_name), Marked.get_mark expr) + e1_stmts, (A.EInj (new_e1, cons_name, e_name), D.pos expr) | L.EApp (f, args) -> let f_stmts, new_f = translate_expr ctxt f in let args_stmts, new_args = @@ -78,7 +78,7 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) : ([], []) args in let new_args = List.rev new_args in - f_stmts @ args_stmts, (A.EApp (new_f, new_args), Marked.get_mark expr) + f_stmts @ args_stmts, (A.EApp (new_f, new_args), D.pos expr) | L.EArray args -> let args_stmts, new_args = List.fold_left @@ -88,9 +88,9 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) : ([], []) args in let new_args = List.rev new_args in - args_stmts, (A.EArray new_args, Marked.get_mark expr) - | L.EOp op -> [], (A.EOp op, Marked.get_mark expr) - | L.ELit l -> [], (A.ELit l, Marked.get_mark expr) + args_stmts, (A.EArray new_args, D.pos expr) + | L.EOp op -> [], (A.EOp op, D.pos expr) + | L.ELit l -> [], (A.ELit l, D.pos expr) | _ -> let tmp_var = A.LocalName.fresh @@ -103,7 +103,7 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) : let v = Marked.unmark (A.LocalName.get_info v) in let tmp_rex = Re.Pcre.regexp "^temp_" in if Re.Pcre.pmatch ~rex:tmp_rex v then v else "temp_" ^ v), - Marked.get_mark expr ) + D.pos expr ) in let ctxt = { @@ -114,20 +114,21 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) : in let tmp_stmts = translate_statements ctxt expr in ( ( A.SLocalDecl - ((tmp_var, Marked.get_mark expr), (D.TAny, Marked.get_mark expr)), - Marked.get_mark expr ) + ((tmp_var, D.pos expr), (D.TAny, D.pos expr)), + D.pos expr ) :: tmp_stmts, - (A.EVar tmp_var, Marked.get_mark expr) ) + (A.EVar tmp_var, D.pos expr) ) -and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) : +and translate_statements (ctxt : ctxt) (block_expr : 'm L.marked_expr) : A.block = match Marked.unmark block_expr with | L.EAssert e -> (* Assertions are always encapsulated in a unit-typed let binding *) let e_stmts, new_e = translate_expr ctxt e in - e_stmts @ [A.SAssert (Marked.unmark new_e), Marked.get_mark block_expr] - | L.EApp ((L.EAbs (binder, taus), binder_pos), args) -> + e_stmts @ [A.SAssert (Marked.unmark new_e), D.pos block_expr] + | L.EApp ((L.EAbs (binder, taus), binder_mark), args) -> (* This defines multiple local variables at the time *) + let binder_pos = D.mark_pos binder_mark in let vars, body = Bindlib.unmbind binder in let vars_tau = List.map2 (fun x tau -> x, tau) (Array.to_list vars) taus in let ctxt = @@ -136,7 +137,7 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) : var_dict = List.fold_left (fun var_dict (x, _) -> - L.VarMap.add x + L.VarMap.add (L.Var.t x) (A.LocalName.fresh (Bindlib.name_of x, binder_pos)) var_dict) ctxt.var_dict vars_tau; @@ -145,14 +146,14 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) : let local_decls = List.map (fun (x, tau) -> - ( A.SLocalDecl ((L.VarMap.find x ctxt.var_dict, binder_pos), tau), + ( A.SLocalDecl ((L.VarMap.find (L.Var.t x) ctxt.var_dict, binder_pos), tau), binder_pos )) vars_tau in let vars_args = List.map2 (fun (x, tau) arg -> - (L.VarMap.find x ctxt.var_dict, binder_pos), tau, arg) + (L.VarMap.find (L.Var.t x) ctxt.var_dict, binder_pos), tau, arg) vars_tau args in let def_blocks = @@ -174,11 +175,11 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) : local_decls @ List.flatten def_blocks @ rest_of_block | L.EAbs (binder, taus) -> let vars, body = Bindlib.unmbind binder in - let binder_pos = Marked.get_mark block_expr in + let binder_pos = D.pos block_expr in let vars_tau = List.map2 (fun x tau -> x, tau) (Array.to_list vars) taus in let closure_name = match ctxt.inside_definition_of with - | None -> A.LocalName.fresh (ctxt.context_name, Marked.get_mark block_expr) + | None -> A.LocalName.fresh (ctxt.context_name, D.pos block_expr) | Some x -> x in let ctxt = @@ -187,7 +188,7 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) : var_dict = List.fold_left (fun var_dict (x, _) -> - L.VarMap.add x + L.VarMap.add (L.Var.t x) (A.LocalName.fresh (Bindlib.name_of x, binder_pos)) var_dict) ctxt.var_dict vars_tau; @@ -202,7 +203,7 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) : func_params = List.map (fun (var, tau) -> - (L.VarMap.find var ctxt.var_dict, binder_pos), tau) + (L.VarMap.find (L.Var.t var) ctxt.var_dict, binder_pos), tau) vars_tau; func_body = new_body; } ), @@ -219,10 +220,10 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) : assert (Array.length vars = 1); let var = vars.(0) in let scalc_var = - A.LocalName.fresh (Bindlib.name_of var, Marked.get_mark arg) + A.LocalName.fresh (Bindlib.name_of var, D.pos arg) in let ctxt = - { ctxt with var_dict = L.VarMap.add var scalc_var ctxt.var_dict } + { ctxt with var_dict = L.VarMap.add (L.Var.t var) scalc_var ctxt.var_dict } in let new_arg = translate_statements ctxt body in (new_arg, scalc_var) :: new_args @@ -232,18 +233,18 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) : in let new_args = List.rev new_args in e1_stmts - @ [A.SSwitch (new_e1, e_name, new_args), Marked.get_mark block_expr] + @ [A.SSwitch (new_e1, e_name, new_args), D.pos block_expr] | L.EIfThenElse (cond, e_true, e_false) -> let cond_stmts, s_cond = translate_expr ctxt cond in let s_e_true = translate_statements ctxt e_true in let s_e_false = translate_statements ctxt e_false in cond_stmts - @ [A.SIfThenElse (s_cond, s_e_true, s_e_false), Marked.get_mark block_expr] + @ [A.SIfThenElse (s_cond, s_e_true, s_e_false), D.pos block_expr] | L.ECatch (e_try, except, e_catch) -> let s_e_try = translate_statements ctxt e_try in let s_e_catch = translate_statements ctxt e_catch in - [A.STryExcept (s_e_try, except, s_e_catch), Marked.get_mark block_expr] - | L.ERaise except -> [A.SRaise except, Marked.get_mark block_expr] + [A.STryExcept (s_e_try, except, s_e_catch), D.pos block_expr] + | L.ERaise except -> [A.SRaise except, D.pos block_expr] | _ -> ( let e_stmts, new_e = translate_expr ctxt block_expr in e_stmts @@ -259,7 +260,7 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) : ( (match ctxt.inside_definition_of with | None -> A.SReturn (Marked.unmark new_e) | Some x -> A.SLocalDef (Marked.same_mark_as x new_e, new_e)), - Marked.get_mark block_expr ); + D.pos block_expr ); ]) let rec translate_scope_body_expr @@ -267,7 +268,7 @@ let rec translate_scope_body_expr (decl_ctx : D.decl_ctx) (var_dict : A.LocalName.t L.VarMap.t) (func_dict : A.TopLevelName.t L.VarMap.t) - (scope_expr : L.expr D.scope_body_expr) : A.block = + (scope_expr : ('m L.expr, 'm) D.scope_body_expr) : A.block = match scope_expr with | Result e -> let block, new_e = @@ -287,7 +288,7 @@ let rec translate_scope_body_expr let let_var_id = A.LocalName.fresh (Bindlib.name_of let_var, scope_let.scope_let_pos) in - let new_var_dict = L.VarMap.add let_var let_var_id var_dict in + let new_var_dict = L.VarMap.add (L.Var.t let_var) let_var_id var_dict in (match scope_let.scope_let_kind with | D.Assertion -> translate_statements @@ -322,7 +323,7 @@ let rec translate_scope_body_expr @ translate_scope_body_expr scope_name decl_ctx new_var_dict func_dict scope_let_next -let translate_program (p : L.program) : A.program = +let translate_program (p : 'm L.program) : A.program = { decl_ctx = p.L.decl_ctx; scopes = @@ -339,7 +340,7 @@ let translate_program (p : L.program) : A.program = A.LocalName.fresh (Bindlib.name_of scope_input_var, input_pos) in let var_dict = - L.VarMap.singleton scope_input_var scope_input_var_id + L.VarMap.singleton (L.Var.t scope_input_var) scope_input_var_id in let new_scope_body = translate_scope_body_expr scope_def.D.scope_name p.decl_ctx @@ -348,7 +349,7 @@ let translate_program (p : L.program) : A.program = let func_id = A.TopLevelName.fresh (Bindlib.name_of scope_var, Pos.no_pos) in - let func_dict = L.VarMap.add scope_var func_id func_dict in + let func_dict = L.VarMap.add (L.Var.t scope_var) func_id func_dict in ( func_dict, { Ast.scope_body_name = scope_def.D.scope_name; diff --git a/compiler/scalc/print.ml b/compiler/scalc/print.ml index 6c05dbe4..9171efaa 100644 --- a/compiler/scalc/print.ml +++ b/compiler/scalc/print.ml @@ -80,15 +80,15 @@ let rec format_expr ((EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _), [arg1; arg2]) -> Format.fprintf fmt "@[%a@ %a@ %a@]" Dcalc.Print.format_binop - (op, Pos.no_pos) format_with_parens arg1 format_with_parens arg2 + op format_with_parens arg1 format_with_parens arg2 | EApp ((EOp (Binop op), _), [arg1; arg2]) -> Format.fprintf fmt "@[%a@ %a@ %a@]" format_with_parens arg1 - Dcalc.Print.format_binop (op, Pos.no_pos) format_with_parens arg2 + Dcalc.Print.format_binop op format_with_parens arg2 | EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug -> Format.fprintf fmt "%a" format_with_parens arg1 | EApp ((EOp (Unop op), _), [arg1]) -> Format.fprintf fmt "@[%a@ %a@]" Dcalc.Print.format_unop - (op, Pos.no_pos) format_with_parens arg1 + op format_with_parens arg1 | EApp (f, args) -> Format.fprintf fmt "@[%a@ %a@]" format_expr f (Format.pp_print_list @@ -96,11 +96,11 @@ let rec format_expr format_with_parens) args | EOp (Ternop op) -> - Format.fprintf fmt "%a" Dcalc.Print.format_ternop (op, Pos.no_pos) + Format.fprintf fmt "%a" Dcalc.Print.format_ternop op | EOp (Binop op) -> - Format.fprintf fmt "%a" Dcalc.Print.format_binop (op, Pos.no_pos) + Format.fprintf fmt "%a" Dcalc.Print.format_binop op | EOp (Unop op) -> - Format.fprintf fmt "%a" Dcalc.Print.format_unop (op, Pos.no_pos) + Format.fprintf fmt "%a" Dcalc.Print.format_unop op let rec format_statement (decl_ctx : Dcalc.Ast.decl_ctx) @@ -118,7 +118,7 @@ let rec format_statement Format.fprintf fmt "%a%a %a@ %a%a" Dcalc.Print.format_punctuation "(" LocalName.format_t name Dcalc.Print.format_punctuation ":" (Dcalc.Print.format_typ decl_ctx) - typ Dcalc.Print.format_punctuation ")")) + (Marked.unmark typ) Dcalc.Print.format_punctuation ")")) func.func_params Dcalc.Print.format_punctuation "=" (format_block decl_ctx ~debug) func.func_body @@ -127,7 +127,7 @@ let rec format_statement "decl" LocalName.format_t (Marked.unmark name) Dcalc.Print.format_punctuation ":" (Dcalc.Print.format_typ decl_ctx) - typ + (Marked.unmark typ) | SLocalDef (name, expr) -> Format.fprintf fmt "@[%a %a@ %a@]" LocalName.format_t (Marked.unmark name) Dcalc.Print.format_punctuation "=" @@ -204,7 +204,7 @@ let format_scope Format.fprintf fmt "%a%a %a@ %a%a" Dcalc.Print.format_punctuation "(" LocalName.format_t name Dcalc.Print.format_punctuation ":" (Dcalc.Print.format_typ decl_ctx) - typ Dcalc.Print.format_punctuation ")")) + (Marked.unmark typ) Dcalc.Print.format_punctuation ")")) body.scope_body_func.func_params Dcalc.Print.format_punctuation "=" (format_block decl_ctx ~debug) body.scope_body_func.func_body diff --git a/compiler/scalc/to_python.ml b/compiler/scalc/to_python.ml index e55c9a1e..bae5845f 100644 --- a/compiler/scalc/to_python.ml +++ b/compiler/scalc/to_python.ml @@ -30,7 +30,7 @@ let format_lit (fmt : Format.formatter) (l : L.lit Marked.pos) : unit = | LUnit -> Format.fprintf fmt "Unit()" | LRat i -> Format.fprintf fmt "decimal_of_string(\"%a\")" Dcalc.Print.format_lit - (Marked.same_mark_as (Dcalc.Ast.LRat i) l) + (Dcalc.Ast.LRat i) | LMoney e -> Format.fprintf fmt "money_of_cents_string(\"%s\")" (Runtime.integer_to_string (Runtime.money_to_cents e)) diff --git a/compiler/scopelang/scope_to_dcalc.ml b/compiler/scopelang/scope_to_dcalc.ml index cf572bd8..7a10ffd2 100644 --- a/compiler/scopelang/scope_to_dcalc.ml +++ b/compiler/scopelang/scope_to_dcalc.ml @@ -556,7 +556,7 @@ let translate_rule should have been defined (even an empty definition, if they're not defined by any rule in the source code) by the translation from desugared to the scope language. *) - Bindlib.box Dcalc.Ast.empty_thunked_term + Bindlib.box (Dcalc.Ast.empty_thunked_term (Untyped {pos = pos_call})) else let a_var, _, _ = Ast.ScopeVarMap.find subvar.scope_var_name subscope_vars_defined