diff --git a/compiler/dcalc/ast.ml b/compiler/dcalc/ast.ml index 3e73d09d..f735c845 100644 --- a/compiler/dcalc/ast.ml +++ b/compiler/dcalc/ast.ml @@ -17,7 +17,7 @@ open Shared_ast -type 'm naked_expr = (dcalc, 'm mark) naked_gexpr -and 'm expr = (dcalc, 'm mark) gexpr +type 'm naked_expr = (dcalc, 'm) naked_gexpr +and 'm expr = (dcalc, 'm) gexpr type 'm program = 'm expr Shared_ast.program diff --git a/compiler/dcalc/ast.mli b/compiler/dcalc/ast.mli index 0c0a776a..6b539829 100644 --- a/compiler/dcalc/ast.mli +++ b/compiler/dcalc/ast.mli @@ -19,7 +19,7 @@ open Shared_ast -type 'm naked_expr = (dcalc, 'm mark) naked_gexpr -and 'm expr = (dcalc, 'm mark) gexpr +type 'm naked_expr = (dcalc, 'm) naked_gexpr +and 'm expr = (dcalc, 'm) gexpr type 'm program = 'm expr Shared_ast.program diff --git a/compiler/dcalc/from_scopelang.ml b/compiler/dcalc/from_scopelang.ml index 2a8ee43f..1d975f1b 100644 --- a/compiler/dcalc/from_scopelang.ml +++ b/compiler/dcalc/from_scopelang.ml @@ -65,7 +65,7 @@ let mark_tany m pos = Expr.with_ty m (Mark.add pos TAny) ~pos (* Expression argument is used as a type witness, its type and positions aren't used *) -let pos_mark_mk (type a m) (e : (a, m mark) gexpr) : +let pos_mark_mk (type a m) (e : (a, m) gexpr) : (Pos.t -> m mark) * ((_, Pos.t) Mark.ed -> m mark) = let pos_mark pos = Expr.map_mark (fun _ -> pos) (fun _ -> TAny, pos) (Mark.get e) @@ -75,8 +75,8 @@ let pos_mark_mk (type a m) (e : (a, m mark) gexpr) : let merge_defaults ~(is_func : bool) - (caller : (dcalc, 'm mark) boxed_gexpr) - (callee : (dcalc, 'm mark) boxed_gexpr) : (dcalc, 'm mark) boxed_gexpr = + (caller : (dcalc, 'm) boxed_gexpr) + (callee : (dcalc, 'm) boxed_gexpr) : (dcalc, 'm) boxed_gexpr = (* the merging of the two defaults, from the reentrant caller and the callee, is straightfoward in the general case and a little subtler when the variable being defined is a function. *) @@ -92,7 +92,7 @@ let merge_defaults let pos = Expr.mark_pos m in Expr.make_app caller (List.map2 - (fun (var : (dcalc, 'm mark) naked_gexpr Bindlib.var) ty -> + (fun (var : (dcalc, 'm) naked_gexpr Bindlib.var) ty -> Expr.evar var (* we have to correctly propagate types when doing this rewriting *) diff --git a/compiler/desugared/ast.ml b/compiler/desugared/ast.ml index 5f22f281..43f20895 100644 --- a/compiler/desugared/ast.ml +++ b/compiler/desugared/ast.ml @@ -83,7 +83,7 @@ module LocationSet : Set.S with type elt = location Mark.pos = Set.Make (struct let compare = Expr.compare_location end) -type expr = (desugared, untyped mark) gexpr +type expr = (desugared, untyped) gexpr module ExprMap = Map.Make (struct type t = expr diff --git a/compiler/desugared/ast.mli b/compiler/desugared/ast.mli index 8c3e43f7..09aa7d6c 100644 --- a/compiler/desugared/ast.mli +++ b/compiler/desugared/ast.mli @@ -41,7 +41,7 @@ module AssertionName : Uid.Id with type info = Uid.MarkedString.info (** {2 Expressions} *) -type expr = (desugared, untyped mark) gexpr +type expr = (desugared, untyped) gexpr (** See {!type:Shared_ast.naked_gexpr} for the complete definition *) type location = desugared glocation diff --git a/compiler/lcalc/ast.ml b/compiler/lcalc/ast.ml index 011f349d..23474b05 100644 --- a/compiler/lcalc/ast.ml +++ b/compiler/lcalc/ast.ml @@ -16,8 +16,8 @@ open Shared_ast -type 'm naked_expr = (lcalc, 'm mark) naked_gexpr -and 'm expr = (lcalc, 'm mark) gexpr +type 'm naked_expr = (lcalc, 'm) naked_gexpr +and 'm expr = (lcalc, 'm) gexpr type 'm program = 'm expr Shared_ast.program diff --git a/compiler/lcalc/ast.mli b/compiler/lcalc/ast.mli index 70af985e..7129b7ed 100644 --- a/compiler/lcalc/ast.mli +++ b/compiler/lcalc/ast.mli @@ -20,8 +20,8 @@ open Shared_ast (** {1 Abstract syntax tree} *) -type 'm naked_expr = (lcalc, 'm mark) naked_gexpr -and 'm expr = (lcalc, 'm mark) gexpr +type 'm naked_expr = (lcalc, 'm) naked_gexpr +and 'm expr = (lcalc, 'm) gexpr type 'm program = 'm expr Shared_ast.program @@ -30,78 +30,76 @@ type 'm program = 'm expr Shared_ast.program (** {2 Term building and management for the [option] monad}*) module OptionMonad : sig - val return : - mark:'m mark -> ('a any, 'm mark) boxed_gexpr -> ('a, 'm mark) boxed_gexpr - - val empty : mark:'m mark -> ('a any, 'm mark) boxed_gexpr + val return : mark:'m mark -> ('a any, 'm) boxed_gexpr -> ('a, 'm) boxed_gexpr + val empty : mark:'m mark -> ('a any, 'm) boxed_gexpr val bind_var : mark:'m mark -> - ('a any, 'm mark) boxed_gexpr -> - ('a, 'm mark) gexpr Var.t -> - ('a, 'm mark) boxed_gexpr -> - ('a, 'm mark) boxed_gexpr + ('a any, 'm) boxed_gexpr -> + ('a, 'm) gexpr Var.t -> + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr val bind : mark:'m mark -> var_name:string -> - ('a any, 'm mark) boxed_gexpr -> - ('a, 'm mark) boxed_gexpr -> - ('a, 'm mark) boxed_gexpr + ('a any, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr val bind_cont : mark:'m mark -> var_name:string -> - (('a any, 'm mark) gexpr Var.t -> ('a, 'm mark) boxed_gexpr) -> - ('a, 'm mark) boxed_gexpr -> - ('a, 'm mark) boxed_gexpr + (('a any, 'm) gexpr Var.t -> ('a, 'm) boxed_gexpr) -> + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr val mbind_mvar : mark:'m mark -> - ('a any, 'm mark) boxed_gexpr -> - ('a, 'm mark) gexpr Var.t list -> - ('a, 'm mark) boxed_gexpr list -> - ('a, 'm mark) boxed_gexpr + ('a any, 'm) boxed_gexpr -> + ('a, 'm) gexpr Var.t list -> + ('a, 'm) boxed_gexpr list -> + ('a, 'm) boxed_gexpr val mbind : mark:'m mark -> var_name:string -> - ('a any, 'm mark) boxed_gexpr -> - ('a, 'm mark) boxed_gexpr list -> - ('a, 'm mark) boxed_gexpr + ('a any, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr list -> + ('a, 'm) boxed_gexpr val mbind_cont : mark:'m mark -> var_name:string -> - (('a any, 'm mark) gexpr Var.t list -> ('a, 'm mark) boxed_gexpr) -> - ('a, 'm mark) boxed_gexpr list -> - ('a, 'm mark) boxed_gexpr + (('a any, 'm) gexpr Var.t list -> ('a, 'm) boxed_gexpr) -> + ('a, 'm) boxed_gexpr list -> + ('a, 'm) boxed_gexpr val error_on_empty : mark:'m mark -> var_name:string -> ?toplevel:bool -> - ((< exceptions : yes ; .. > as 'a), 'm mark) boxed_gexpr -> - ('a, 'm mark) boxed_gexpr + ((< exceptions : yes ; .. > as 'a), 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr val map : mark:'m mark -> var_name:string -> - ((< exceptions : no ; .. > as 'a), 'm mark) boxed_gexpr -> - ('a, 'm mark) boxed_gexpr -> - ('a, 'm mark) boxed_gexpr + ((< exceptions : no ; .. > as 'a), 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr val mmap_mvar : mark:'m mark -> - ('a any, 'm mark) boxed_gexpr -> - ('a, 'm mark) gexpr Var.t list -> - ('a, 'm mark) boxed_gexpr list -> - ('a, 'm mark) boxed_gexpr + ('a any, 'm) boxed_gexpr -> + ('a, 'm) gexpr Var.t list -> + ('a, 'm) boxed_gexpr list -> + ('a, 'm) boxed_gexpr val mmap : mark:'m mark -> var_name:string -> - ('a any, 'm mark) boxed_gexpr -> - ('a, 'm mark) boxed_gexpr list -> - ('a, 'm mark) boxed_gexpr + ('a any, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr list -> + ('a, 'm) boxed_gexpr end diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml index 0bca5672..20a92cca 100644 --- a/compiler/lcalc/compile_without_exceptions.ml +++ b/compiler/lcalc/compile_without_exceptions.ml @@ -76,8 +76,7 @@ let trans_op : dcalc Op.t -> lcalc Op.t = Operator.translate type 'm var_ctx = { info_pure : bool; is_scope : bool; var : 'm Ast.expr Var.t } type 'm ctx = { - ctx_vars : - ((dcalc, 'm mark) Shared_ast__Definitions.gexpr, 'm var_ctx) Var.Map.t; + ctx_vars : ((dcalc, 'm) gexpr, 'm var_ctx) Var.Map.t; ctx_context_name : string; } @@ -97,8 +96,8 @@ let trans_var (ctx : 'm ctx) (x : 'm D.expr Var.t) : 'm Ast.expr Var.t = literals, this mean that a expression of type [money] will be of type [money option]. We rely on later optimization to shorten the size of the generated code. *) -let rec trans (ctx : typed ctx) (e : typed D.expr) : - (lcalc, typed mark) boxed_gexpr = +let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr + = let m = Mark.get e in let mark = m in let pos = Expr.pos e in @@ -622,7 +621,7 @@ let rec trans_scope_let (ctx : typed ctx) (s : typed D.expr scope_let) = scope_let_expr scope_let_next and trans_scope_body_expr ctx s : - (lcalc, typed mark) gexpr scope_body_expr Bindlib.box = + (lcalc, typed) gexpr scope_body_expr Bindlib.box = match s with | Result e -> begin (* invariant : result is always in the form of a record. *) @@ -662,7 +661,7 @@ let trans_scope_body binder let rec trans_code_items (ctx : typed ctx) (c : typed D.expr code_item_list) : - (lcalc, typed mark) gexpr code_item_list Bindlib.box = + (lcalc, typed) gexpr code_item_list Bindlib.box = match c with | Nil -> Bindlib.box Nil | Cons (c, next) -> ( diff --git a/compiler/plugins/lazy_interp.ml b/compiler/plugins/lazy_interp.ml index 93026e62..988e6da2 100644 --- a/compiler/plugins/lazy_interp.ml +++ b/compiler/plugins/lazy_interp.ml @@ -37,8 +37,7 @@ let value_level = { eval_struct = false; eval_op = true; eval_default = true } module Env = struct type 'm t = - | Env of - ((dcalc, 'm mark) gexpr, ((dcalc, 'm mark) gexpr * 'm t) ref) Var.Map.t + | Env of ((dcalc, 'm) gexpr, ((dcalc, 'm) gexpr * 'm t) ref) Var.Map.t let find v (Env t) = Var.Map.find v t let add v e e_env (Env t) = Env (Var.Map.add v (ref (e, e_env)) t) @@ -62,8 +61,8 @@ let rec lazy_eval : decl_ctx -> 'm Env.t -> laziness_level -> - (dcalc, 'm mark) gexpr -> - (dcalc, 'm mark) gexpr * 'm Env.t = + (dcalc, 'm) gexpr -> + (dcalc, 'm) gexpr * 'm Env.t = fun ctx env llevel e0 -> let eval_to_value ?(eval_default = true) env e = lazy_eval ctx env { value_level with eval_default } e @@ -212,9 +211,8 @@ let rec lazy_eval : | _ -> error e "Invalid assertion condition %a" Expr.format e) | _ -> . -let interpret_program - (prg : ('dcalc, 'm mark) gexpr program) - (scope : ScopeName.t) : ('t, 'm mark) gexpr * 'm Env.t = +let interpret_program (prg : ('dcalc, 'm) gexpr program) (scope : ScopeName.t) : + ('t, 'm) gexpr * 'm Env.t = let ctx = prg.decl_ctx in let all_env, scopes = Scope.fold_left prg.code_items ~init:(Env.empty, ScopeName.Map.empty) diff --git a/compiler/scopelang/ast.ml b/compiler/scopelang/ast.ml index 87813dc3..94382ab7 100644 --- a/compiler/scopelang/ast.ml +++ b/compiler/scopelang/ast.ml @@ -25,7 +25,7 @@ module LocationSet : Set.S with type elt = location Mark.pos = Set.Make (struct let compare = Expr.compare_location end) -type 'm expr = (scopelang, 'm mark) gexpr +type 'm expr = (scopelang, 'm) gexpr let rec locations_used (e : 'm expr) : LocationSet.t = match e with diff --git a/compiler/scopelang/ast.mli b/compiler/scopelang/ast.mli index 7ae5fb3f..069c8b06 100644 --- a/compiler/scopelang/ast.mli +++ b/compiler/scopelang/ast.mli @@ -27,7 +27,7 @@ module LocationSet : Set.S with type elt = location Mark.pos (** {1 Abstract syntax tree} *) -type 'm expr = (scopelang, 'm mark) gexpr +type 'm expr = (scopelang, 'm) gexpr val locations_used : 'm expr -> LocationSet.t diff --git a/compiler/shared_ast/definitions.ml b/compiler/shared_ast/definitions.ml index 5e11bc93..c26845b6 100644 --- a/compiler/shared_ast/definitions.ml +++ b/compiler/shared_ast/definitions.ml @@ -287,6 +287,24 @@ end type 'a operator = 'a Op.t type except = ConflictError | EmptyError | NoValueProvided | Crash +(** {2 Markings} *) + +type untyped = { pos : Pos.t } [@@caml.unboxed] +type typed = { pos : Pos.t; ty : typ } +type 'a custom = { pos : Pos.t; custom : 'a } + +(** The generic type of AST markings. Using a GADT allows functions to be + polymorphic in the marking, but still do transformations on types when + appropriate. The [Custom] case can be used within passes that need to store + specific information, e.g. typing *) +type _ mark = + | Untyped : untyped -> untyped mark + | Typed : typed -> typed mark + | Custom : 'a custom -> 'a custom mark + +type ('a, 'm) marked = ('a, 'm mark) Mark.ed +(** Type of values marked with the above standard mark GADT *) + (** {2 Generic expressions} *) (** Define a common base type for the expressions in most passes of the compiler *) @@ -317,9 +335,9 @@ type 'a glocation = TopdefName.t Mark.pos -> < explicitScopes : yes ; .. > glocation -type ('a, 't) gexpr = (('a, 't) naked_gexpr, 't) Mark.ed +type ('a, 'm) gexpr = (('a, 'm) naked_gexpr, 'm) marked -and ('a, 't) naked_gexpr = ('a, 'a, 't) base_gexpr +and ('a, 'm) naked_gexpr = ('a, 'a, 'm) base_gexpr (** General expressions: groups all expression cases of the different ASTs, and uses a GADT to eliminate irrelevant cases for each one. The ['t] annotations are also totally unconstrained at this point. The dcalc exprs, for ex ample, @@ -340,132 +358,117 @@ and ('a, 't) naked_gexpr = ('a, 'a, 't) base_gexpr well-formed AST types, but differentiating them ephemerally allows us to do well-typed recursive transformations on the AST that change its type *) -and ('a, 'b, 't) base_gexpr = +and ('a, 'b, 'm) base_gexpr = (* Constructors common to all ASTs *) - | ELit : lit -> ('a, < .. >, 't) base_gexpr + | ELit : lit -> ('a, < .. >, 'm) base_gexpr | EApp : { - f : ('a, 't) gexpr; - args : ('a, 't) gexpr list; + f : ('a, 'm) gexpr; + args : ('a, 'm) gexpr list; } - -> ('a, < .. >, 't) base_gexpr + -> ('a, < .. >, 'm) base_gexpr | EOp : { op : 'b operator; tys : typ list; } - -> ('a, (< .. > as 'b), 't) base_gexpr - | EArray : ('a, 't) gexpr list -> ('a, < .. >, 't) base_gexpr - | EVar : ('a, 't) naked_gexpr Bindlib.var -> ('a, _, 't) base_gexpr + -> ('a, (< .. > as 'b), 'm) base_gexpr + | EArray : ('a, 'm) gexpr list -> ('a, < .. >, 'm) base_gexpr + | EVar : ('a, 'm) naked_gexpr Bindlib.var -> ('a, _, 'm) base_gexpr | EAbs : { - binder : (('a, 'a, 't) base_gexpr, ('a, 't) gexpr) Bindlib.mbinder; + binder : (('a, 'a, 'm) base_gexpr, ('a, 'm) gexpr) Bindlib.mbinder; tys : typ list; } - -> ('a, < .. >, 't) base_gexpr + -> ('a, < .. >, 'm) base_gexpr | EIfThenElse : { - cond : ('a, 't) gexpr; - etrue : ('a, 't) gexpr; - efalse : ('a, 't) gexpr; + cond : ('a, 'm) gexpr; + etrue : ('a, 'm) gexpr; + efalse : ('a, 'm) gexpr; } - -> ('a, < .. >, 't) base_gexpr + -> ('a, < .. >, 'm) base_gexpr | EStruct : { name : StructName.t; - fields : ('a, 't) gexpr StructField.Map.t; + fields : ('a, 'm) gexpr StructField.Map.t; } - -> ('a, < .. >, 't) base_gexpr + -> ('a, < .. >, 'm) base_gexpr | EInj : { name : EnumName.t; - e : ('a, 't) gexpr; + e : ('a, 'm) gexpr; cons : EnumConstructor.t; } - -> ('a, < .. >, 't) base_gexpr + -> ('a, < .. >, 'm) base_gexpr | EMatch : { name : EnumName.t; - e : ('a, 't) gexpr; - cases : ('a, 't) gexpr EnumConstructor.Map.t; + e : ('a, 'm) gexpr; + cases : ('a, 'm) gexpr EnumConstructor.Map.t; } - -> ('a, < .. >, 't) base_gexpr - | ETuple : ('a, 't) gexpr list -> ('a, < .. >, 't) base_gexpr + -> ('a, < .. >, 'm) base_gexpr + | ETuple : ('a, 'm) gexpr list -> ('a, < .. >, 'm) base_gexpr | ETupleAccess : { - e : ('a, 't) gexpr; + e : ('a, 'm) gexpr; index : int; size : int; } - -> ('a, < .. >, 't) base_gexpr + -> ('a, < .. >, 'm) base_gexpr (* Early stages *) - | ELocation : 'b glocation -> ('a, (< .. > as 'b), 't) base_gexpr + | ELocation : 'b glocation -> ('a, (< .. > as 'b), 'm) base_gexpr | EScopeCall : { scope : ScopeName.t; - args : ('a, 't) gexpr ScopeVar.Map.t; + args : ('a, 'm) gexpr ScopeVar.Map.t; } - -> ('a, < explicitScopes : yes ; .. >, 't) base_gexpr + -> ('a, < explicitScopes : yes ; .. >, 'm) base_gexpr | EDStructAccess : { name_opt : StructName.t option; - e : ('a, 't) gexpr; + e : ('a, 'm) gexpr; field : IdentName.t; } - -> ('a, < syntacticNames : yes ; .. >, 't) base_gexpr + -> ('a, < syntacticNames : yes ; .. >, 'm) base_gexpr (** [desugared] has ambiguous struct fields *) | EStructAccess : { name : StructName.t; - e : ('a, 't) gexpr; + e : ('a, 'm) gexpr; field : StructField.t; } - -> ('a, < resolvedNames : yes ; .. >, 't) base_gexpr + -> ('a, < resolvedNames : yes ; .. >, 'm) base_gexpr (** Resolved struct/enums, after [desugared] *) (* Lambda-like *) - | EAssert : ('a, 't) gexpr -> ('a, < assertions : yes ; .. >, 't) base_gexpr + | EAssert : ('a, 'm) gexpr -> ('a, < assertions : yes ; .. >, 'm) base_gexpr (* Default terms *) | EDefault : { - excepts : ('a, 't) gexpr list; - just : ('a, 't) gexpr; - cons : ('a, 't) gexpr; + excepts : ('a, 'm) gexpr list; + just : ('a, 'm) gexpr; + cons : ('a, 'm) gexpr; } - -> ('a, < defaultTerms : yes ; .. >, 't) base_gexpr - | EEmptyError : ('a, < defaultTerms : yes ; .. >, 't) base_gexpr + -> ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr + | EEmptyError : ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr | EErrorOnEmpty : - ('a, 't) gexpr - -> ('a, < defaultTerms : yes ; .. >, 't) base_gexpr + ('a, 'm) gexpr + -> ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr (* Lambda calculus with exceptions *) - | ERaise : except -> ('a, < exceptions : yes ; .. >, 't) base_gexpr + | ERaise : except -> ('a, < exceptions : yes ; .. >, 'm) base_gexpr | ECatch : { - body : ('a, 't) gexpr; + body : ('a, 'm) gexpr; exn : except; - handler : ('a, 't) gexpr; + handler : ('a, 'm) gexpr; } - -> ('a, < exceptions : yes ; .. >, 't) base_gexpr + -> ('a, < exceptions : yes ; .. >, 'm) base_gexpr -(* Useful for errors and printing, for example *) -(* type any_expr = AnyExpr : ('a, _ mark) gexpr -> any_expr *) +(** Useful for errors and printing, for example *) +type any_expr = AnyExpr : ('a, _) gexpr -> any_expr -type ('a, 't) boxed_gexpr = (('a, 't) naked_gexpr Bindlib.box, 't) Mark.ed +type ('a, 'm) boxed_gexpr = (('a, 'm) naked_gexpr Bindlib.box, 'm) marked (** The annotation is lifted outside of the box for expressions *) -type 'e boxed = ('a, 't) boxed_gexpr constraint 'e = ('a, 't) gexpr -(** [('a, 't) gexpr boxed] is [('a, 't) boxed_gexpr]. The difference with - [('a, 't) gexpr Bindlib.box] is that the annotations is outside of the box, +type 'e boxed = ('a, 'm) boxed_gexpr constraint 'e = ('a, 'm) gexpr +(** [('a, 'm) gexpr boxed] is [('a, 'm) boxed_gexpr]. The difference with + [('a, 'm) gexpr Bindlib.box] is that the annotations is outside of the box, and can therefore be accessed without the need to resolve the box *) -type ('e, 'b) binder = (('a, 't) naked_gexpr, 'b) Bindlib.binder - constraint 'e = ('a, 't) gexpr +type ('e, 'b) binder = (('a, 'm) naked_gexpr, 'b) Bindlib.binder + constraint 'e = ('a, 'm) gexpr (** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib} library, based on higher-order abstract syntax *) -type ('e, 'b) mbinder = (('a, 't) naked_gexpr, 'b) Bindlib.mbinder - constraint 'e = ('a, 't) gexpr - -(** {2 Markings} *) - -type untyped = { pos : Pos.t } [@@ocaml.unboxed] -type typed = { pos : Pos.t; ty : typ } - -(** The generic type of AST markings. Using a GADT allows functions to be - polymorphic in the marking, but still do transformations on types when - appropriate. Expected to fill the ['t] parameter of [gexpr] and [gexpr] (a - ['t] annotation different from this type is used in the middle of the typing - processing, but all visible ASTs should otherwise use this. *) -type _ mark = Untyped : untyped -> untyped mark | Typed : typed -> typed mark - -(** Useful for errors and printing, for example *) -type any_expr = AnyExpr : ('a, _ mark) gexpr -> any_expr +type ('e, 'b) mbinder = (('a, 'm) naked_gexpr, 'b) Bindlib.mbinder + constraint 'e = ('a, 'm) gexpr (** {2 Higher-level program structure} *) @@ -496,7 +499,7 @@ type 'e scope_let = { (* todo ? Factorise the code_item _list type below and use it here *) scope_let_pos : Pos.t; } - constraint 'e = ('a any, _ mark) gexpr + constraint 'e = ('a any, _) gexpr (** This type is parametrized by the expression type so it can be reused in later intermediate representations. *) @@ -506,14 +509,14 @@ type 'e scope_let = { and 'e scope_body_expr = | Result of 'e | ScopeLet of 'e scope_let - constraint 'e = ('a any, _ mark) gexpr + constraint 'e = ('a any, _) gexpr type 'e scope_body = { scope_body_input_struct : StructName.t; scope_body_output_struct : StructName.t; scope_body_expr : ('e, 'e scope_body_expr) binder; } - constraint 'e = ('a any, _ mark) gexpr + constraint 'e = ('a any, _) gexpr (** Instead of being a single expression, we give a little more ad-hoc structure to the scope body by decomposing it in an ordered list of let-bindings, and a result expression that uses the let-binded variables. The first binder is diff --git a/compiler/shared_ast/expr.ml b/compiler/shared_ast/expr.ml index 1acd254c..2388861a 100644 --- a/compiler/shared_ast/expr.ml +++ b/compiler/shared_ast/expr.ml @@ -174,24 +174,25 @@ let escopecall scope args mark = let no_mark : type m. m mark -> m mark = function | Untyped _ -> Untyped { pos = Pos.no_pos } | Typed _ -> Typed { pos = Pos.no_pos; ty = Mark.add Pos.no_pos TAny } + | Custom { custom; pos = _ } -> Custom { pos = Pos.no_pos; custom } let mark_pos (type m) (m : m mark) : Pos.t = - match m with Untyped { pos } | Typed { pos; _ } -> pos + match m with Untyped { pos } | Typed { pos; _ } | Custom { pos; _ } -> pos -let pos (type m) (x : ('a, m mark) Mark.ed) : Pos.t = mark_pos (Mark.get x) +let pos (type m) (x : ('a, m) marked) : Pos.t = mark_pos (Mark.get x) -let fun_id mark : ('a any, 'm mark) boxed_gexpr = +let fun_id mark : ('a any, 'm) boxed_gexpr = let x = Var.make "x" in eabs (bind [| x |] (evar x mark)) [TAny, mark_pos mark] mark let ty (_, m) : typ = match m with Typed { ty; _ } -> ty -let set_ty (type m) (ty : typ) (x : ('a, m mark) Mark.ed) : - ('a, typed mark) Mark.ed = +let set_ty (type m) (ty : typ) (x : ('a, m) marked) : ('a, typed) marked = Mark.add (match Mark.get x with | Untyped { pos } -> Typed { pos; ty } - | Typed m -> Typed { m with ty }) + | Typed m -> Typed { m with ty } + | Custom { pos; _ } -> Typed { pos; ty }) (Mark.remove x) let map_mark (type m) (pos_f : Pos.t -> Pos.t) (ty_f : typ -> typ) (m : m mark) @@ -199,6 +200,7 @@ let map_mark (type m) (pos_f : Pos.t -> Pos.t) (ty_f : typ -> typ) (m : m mark) match m with | Untyped { pos } -> Untyped { pos = pos_f pos } | Typed { pos; ty } -> Typed { pos = pos_f pos; ty = ty_f ty } + | Custom { pos; custom } -> Custom { pos = pos_f pos; custom } let map_mark2 (type m) @@ -209,6 +211,7 @@ let map_mark2 match m1, m2 with | Untyped m1, Untyped m2 -> Untyped { pos = pos_f m1.pos m2.pos } | Typed m1, Typed m2 -> Typed { pos = pos_f m1.pos m2.pos; ty = ty_f m1 m2 } + | Custom _, Custom _ -> invalid_arg "map_mark2" let fold_marks (type m) @@ -225,6 +228,7 @@ let fold_marks pos = pos_f (List.map (function Typed { pos; _ } -> pos) ms); ty = ty_f (List.map (function Typed m -> m) ms); } + | Custom _ :: _ -> invalid_arg "map_mark2" let with_pos (type m) (pos : Pos.t) (m : m mark) : m mark = map_mark (fun _ -> pos) (fun ty -> ty) m @@ -236,7 +240,9 @@ let with_ty (type m) (m : m mark) ?pos (ty : typ) : m mark = map_mark (fun default -> Option.value pos ~default) (fun _ -> ty) m let maybe_ty (type m) ?(typ = TAny) (m : m mark) : typ = - match m with Untyped { pos } -> Mark.add pos typ | Typed { ty; _ } -> ty + match m with + | Untyped { pos } | Custom { pos; _ } -> Mark.add pos typ + | Typed { ty; _ } -> ty (* - Predefined types (option) - *) @@ -254,7 +260,7 @@ let option_enum_config = let map (type a b) ~(f : (a, 'm1) gexpr -> (b, 'm2) boxed_gexpr) - (e : ((a, b, 'm1) base_gexpr, 'm2) Mark.ed) : (b, 'm2) boxed_gexpr = + (e : ((a, b, 'm1) base_gexpr, 'm2) marked) : (b, 'm2) boxed_gexpr = let m = Mark.get e in match Mark.remove e with | ELit l -> elit l m @@ -294,9 +300,7 @@ let map escopecall scope fields m let rec map_top_down ~f e = map ~f:(map_top_down ~f) (f e) - -let map_marks ~f e = - map_top_down ~f:(Mark.map_mark f) e +let map_marks ~f e = map_top_down ~f:(Mark.map_mark f) e (* Folds the given function on the direct children of the given expression. *) let shallow_fold @@ -333,7 +337,7 @@ let map_gather ~(acc : 'acc) ~(join : 'acc -> 'acc -> 'acc) ~(f : (a, 'm1) gexpr -> 'acc * (a, 'm2) boxed_gexpr) - (e : ((a, 'm1) naked_gexpr, 'm2) Mark.ed) : 'acc * (a, 'm2) boxed_gexpr = + (e : ((a, 'm1) naked_gexpr, 'm2) marked) : 'acc * (a, 'm2) boxed_gexpr = let m = Mark.get e in let lfoldmap es = let acc, r_es = diff --git a/compiler/shared_ast/expr.mli b/compiler/shared_ast/expr.mli index 5621d40f..7d55894e 100644 --- a/compiler/shared_ast/expr.mli +++ b/compiler/shared_ast/expr.mli @@ -22,130 +22,134 @@ open Definitions (** {2 Boxed constructors} *) -val box : ('a, 't) gexpr -> ('a, 't) boxed_gexpr +val box : ('a, 'm) gexpr -> ('a, 'm) boxed_gexpr (** Box the expression from the outside *) -val unbox : ('a, 't) boxed_gexpr -> ('a, 't) gexpr +val unbox : ('a, 'm) boxed_gexpr -> ('a, 'm) gexpr (** For closed expressions, similar to [Bindlib.unbox] *) -val rebox : ('a any, 't) gexpr -> ('a, 't) boxed_gexpr +val rebox : ('a any, 'm) gexpr -> ('a, 'm) boxed_gexpr (** Rebuild the whole term, re-binding all variables and exposing free variables *) -val evar : ('a, 't) gexpr Var.t -> 't -> ('a, 't) boxed_gexpr +val evar : ('a, 'm) gexpr Var.t -> 'm mark -> ('a, 'm) boxed_gexpr val bind : - ('a, 't) gexpr Var.t array -> - ('a, 't) boxed_gexpr -> - (('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder Bindlib.box + ('a, 'm) gexpr Var.t array -> + ('a, 'm) boxed_gexpr -> + (('a, 'm) naked_gexpr, ('a, 'm) gexpr) Bindlib.mbinder Bindlib.box val subst : - (('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder -> - ('a, 't) gexpr list -> - ('a, 't) gexpr + (('a, 'm) naked_gexpr, ('a, 'm) gexpr) Bindlib.mbinder -> + ('a, 'm) gexpr list -> + ('a, 'm) gexpr -val etuple : ('a, 't) boxed_gexpr list -> 't -> ('a any, 't) boxed_gexpr +val etuple : ('a, 'm) boxed_gexpr list -> 'm mark -> ('a any, 'm) boxed_gexpr val etupleaccess : - ('a, 't) boxed_gexpr -> int -> int -> 't -> ('a any, 't) boxed_gexpr + ('a, 'm) boxed_gexpr -> int -> int -> 'm mark -> ('a any, 'm) boxed_gexpr -val earray : ('a, 't) boxed_gexpr list -> 't -> ('a any, 't) boxed_gexpr -val elit : lit -> 't -> ('a any, 't) boxed_gexpr +val earray : ('a, 'm) boxed_gexpr list -> 'm mark -> ('a any, 'm) boxed_gexpr +val elit : lit -> 'm mark -> ('a any, 'm) boxed_gexpr val eabs : - (('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder Bindlib.box -> + (('a, 'm) naked_gexpr, ('a, 'm) gexpr) Bindlib.mbinder Bindlib.box -> typ list -> - 't -> - ('a any, 't) boxed_gexpr + 'm mark -> + ('a any, 'm) boxed_gexpr val eapp : - ('a, 't) boxed_gexpr -> - ('a, 't) boxed_gexpr list -> - 't -> - ('a any, 't) boxed_gexpr + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr list -> + 'm mark -> + ('a any, 'm) boxed_gexpr val eassert : - ('a, 't) boxed_gexpr -> - 't -> - ((< assertions : yes ; .. > as 'a), 't) boxed_gexpr + ('a, 'm) boxed_gexpr -> + 'm mark -> + ((< assertions : yes ; .. > as 'a), 'm) boxed_gexpr -val eop : 'a operator -> typ list -> 't -> ('a any, 't) boxed_gexpr +val eop : 'a operator -> typ list -> 'm mark -> ('a any, 'm) boxed_gexpr val edefault : - ('a, 't) boxed_gexpr list -> - ('a, 't) boxed_gexpr -> - ('a, 't) boxed_gexpr -> - 't -> - ((< defaultTerms : yes ; .. > as 'a), 't) boxed_gexpr + ('a, 'm) boxed_gexpr list -> + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> + 'm mark -> + ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr val eifthenelse : - ('a, 't) boxed_gexpr -> - ('a, 't) boxed_gexpr -> - ('a, 't) boxed_gexpr -> - 't -> - ('a any, 't) boxed_gexpr + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> + 'm mark -> + ('a any, 'm) boxed_gexpr -val eemptyerror : 't -> ((< defaultTerms : yes ; .. > as 'a), 't) boxed_gexpr +val eemptyerror : + 'm mark -> ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr val eerroronempty : - ('a, 't) boxed_gexpr -> - 't -> - ((< defaultTerms : yes ; .. > as 'a), 't) boxed_gexpr + ('a, 'm) boxed_gexpr -> + 'm mark -> + ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr val ecatch : - ('a, 't) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> except -> - ('a, 't) boxed_gexpr -> - 't -> - ((< exceptions : yes ; .. > as 'a), 't) boxed_gexpr + ('a, 'm) boxed_gexpr -> + 'm mark -> + ((< exceptions : yes ; .. > as 'a), 'm) boxed_gexpr -val eraise : except -> 't -> (< exceptions : yes ; .. >, 't) boxed_gexpr -val elocation : 'a glocation -> 't -> ((< .. > as 'a), 't) boxed_gexpr +val eraise : except -> 'm mark -> (< exceptions : yes ; .. >, 'm) boxed_gexpr +val elocation : 'a glocation -> 'm mark -> ((< .. > as 'a), 'm) boxed_gexpr val estruct : StructName.t -> - ('a, 't) boxed_gexpr StructField.Map.t -> - 't -> - ('a any, 't) boxed_gexpr + ('a, 'm) boxed_gexpr StructField.Map.t -> + 'm mark -> + ('a any, 'm) boxed_gexpr val edstructaccess : - ('a, 't) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> IdentName.t -> StructName.t option -> - 't -> - ((< syntacticNames : yes ; .. > as 'a), 't) boxed_gexpr + 'm mark -> + ((< syntacticNames : yes ; .. > as 'a), 'm) boxed_gexpr val estructaccess : - ('a, 't) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> StructField.t -> StructName.t -> - 't -> - ((< resolvedNames : yes ; .. > as 'a), 't) boxed_gexpr + 'm mark -> + ((< resolvedNames : yes ; .. > as 'a), 'm) boxed_gexpr val einj : - ('a, 't) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> EnumConstructor.t -> EnumName.t -> - 't -> - ('a any, 't) boxed_gexpr + 'm mark -> + ('a any, 'm) boxed_gexpr val ematch : - ('a, 't) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> EnumName.t -> - ('a, 't) boxed_gexpr EnumConstructor.Map.t -> - 't -> - ('a any, 't) boxed_gexpr + ('a, 'm) boxed_gexpr EnumConstructor.Map.t -> + 'm mark -> + ('a any, 'm) boxed_gexpr val escopecall : ScopeName.t -> - ('a, 't) boxed_gexpr ScopeVar.Map.t -> - 't -> - ((< explicitScopes : yes ; .. > as 'a), 't) boxed_gexpr + ('a, 'm) boxed_gexpr ScopeVar.Map.t -> + 'm mark -> + ((< explicitScopes : yes ; .. > as 'a), 'm) boxed_gexpr -val fun_id : 'm mark -> ('a any, 'm mark) boxed_gexpr +val fun_id : 'm mark -> ('a any, 'm) boxed_gexpr (** {2 Manipulation of marks} *) val no_mark : 'm mark -> 'm mark +(** Returns an empty mark, using the argument as type witness. Note that the + custom part is kept on [Custom] marks *) + val mark_pos : 'm mark -> Pos.t val with_pos : Pos.t -> 'm mark -> 'm mark @@ -163,9 +167,11 @@ val map_mark2 : 'm mark -> 'm mark -> 'm mark +(** @raise Invalid_arg on custom marks*) val fold_marks : (Pos.t list -> Pos.t) -> (typed list -> typ) -> 'm mark list -> 'm mark +(** @raise Invalid_arg on custom marks*) val maybe_ty : ?typ:naked_typ -> 'm mark -> typ (** Returns the corresponding type on a typed expr, or [typ] (defaulting to @@ -180,16 +186,16 @@ val option_enum_config : typ EnumConstructor.Map.t (** Manipulation of marked expressions *) -val pos : ('a, 'm mark) Mark.ed -> Pos.t -val ty : ('e, typed mark) Mark.ed -> typ -val set_ty : typ -> ('a, 'm mark) Mark.ed -> ('a, typed mark) Mark.ed -val untype : ('a, 'm mark) gexpr -> ('a, untyped mark) boxed_gexpr +val pos : ('a, 'm) marked -> Pos.t +val ty : ('e, typed) marked -> typ +val set_ty : typ -> ('a, 'm) marked -> ('a, typed) marked +val untype : ('a, 'm) gexpr -> ('a, untyped) boxed_gexpr (** {2 Traversal functions} *) val map : f:(('a, 'm1) gexpr -> ('b, 'm2) boxed_gexpr) -> - (('a, 'b, 'm1) base_gexpr, 'm2) Mark.ed -> + (('a, 'b, 'm1) base_gexpr, 'm2) marked -> ('b, 'm2) boxed_gexpr (** Shallow mapping on expressions (non recursive): applies the given function to all sub-terms of the given expression, and rebuilds the node. @@ -223,17 +229,18 @@ val map : becomes useful. *) val map_top_down : - f:(('a, 't1) gexpr -> (('a, 't1) naked_gexpr, 't2) Mark.ed) -> - ('a, 't1) gexpr -> - ('a, 't2) boxed_gexpr + f:(('a, 'm1) gexpr -> (('a, 'm1) naked_gexpr, 'm2) marked) -> + ('a, 'm1) gexpr -> + ('a, 'm2) boxed_gexpr (** Recursively applies [f] to the nodes of the expression tree. The type returned by [f] is hybrid since the mark at top-level has been rewritten, but not yet the marks in the subtrees. *) -val map_marks : f:('t1 -> 't2) -> ('a, 't1) gexpr -> ('a, 't2) boxed_gexpr +val map_marks : + f:('m1 mark -> 'm2 mark) -> ('a, 'm1) gexpr -> ('a, 'm2) boxed_gexpr val shallow_fold : - (('a, 't) gexpr -> 'acc -> 'acc) -> ('a, 't) gexpr -> 'acc -> 'acc + (('a, 'm) gexpr -> 'acc -> 'acc) -> ('a, 'm) gexpr -> 'acc -> 'acc (** Applies a function on all sub-terms of the given expression. Does not recurse. It opens binders unless you avoid sending binders to the function like the example below. Useful as helper for recursive calls within @@ -252,9 +259,9 @@ val shallow_fold : val map_gather : acc:'acc -> join:('acc -> 'acc -> 'acc) -> - f:(('a, 't1) gexpr -> 'acc * ('a, 't2) boxed_gexpr) -> - (('a, 't1) naked_gexpr, 't2) Mark.ed -> - 'acc * ('a, 't2) boxed_gexpr + f:(('a, 'm1) gexpr -> 'acc * ('a, 'm2) boxed_gexpr) -> + (('a, 'm1) naked_gexpr, 'm2) marked -> + 'acc * ('a, 'm2) boxed_gexpr (** Shallow mapping similar to [map], but additionally allows to gather an accumulator bottom-up. [acc] is the accumulator value returned on terminal nodes, and [join] is used to merge accumulators from the different sub-terms @@ -273,52 +280,49 @@ val map_gather : (** {2 Expression building helpers} *) -val make_var : ('a, 't) gexpr Var.t -> 't -> ('a, 't) boxed_gexpr +val make_var : ('a, 'm) gexpr Var.t -> 'm mark -> ('a, 'm) boxed_gexpr val make_abs : - ('a, 'm mark) gexpr Var.vars -> - ('a, 'm mark) boxed_gexpr -> + ('a, 'm) gexpr Var.vars -> + ('a, 'm) boxed_gexpr -> typ list -> Pos.t -> - ('a any, 'm mark) boxed_gexpr + ('a any, 'm) boxed_gexpr val make_app : - ('a any, 'm mark) boxed_gexpr -> - ('a, 'm mark) boxed_gexpr list -> + ('a any, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr list -> Pos.t -> - ('a any, 'm mark) boxed_gexpr + ('a any, 'm) boxed_gexpr val empty_thunked_term : - 'm mark -> (< defaultTerms : yes ; .. >, 'm mark) boxed_gexpr + 'm mark -> (< defaultTerms : yes ; .. >, 'm) boxed_gexpr -val thunk_term : - ('a any, 'b mark) boxed_gexpr -> 'b mark -> ('a, 'b mark) boxed_gexpr - -val unthunk_term_nobox : - ('a any, 'm mark) gexpr -> 'm mark -> ('a, 'm mark) gexpr +val thunk_term : ('a any, 'b) boxed_gexpr -> 'b mark -> ('a, 'b) boxed_gexpr +val unthunk_term_nobox : ('a any, 'm) gexpr -> 'm mark -> ('a, 'm) gexpr val make_let_in : - ('a, 'm mark) gexpr Var.t -> + ('a, 'm) gexpr Var.t -> typ -> - ('a, 'm mark) boxed_gexpr -> - ('a, 'm mark) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> Pos.t -> - ('a any, 'm mark) boxed_gexpr + ('a any, 'm) boxed_gexpr val make_multiple_let_in : - ('a, 'm mark) gexpr Var.vars -> + ('a, 'm) gexpr Var.vars -> typ list -> - ('a, 'm mark) boxed_gexpr list -> - ('a, 'm mark) boxed_gexpr -> + ('a, 'm) boxed_gexpr list -> + ('a, 'm) boxed_gexpr -> Pos.t -> - ('a any, 'm mark) boxed_gexpr + ('a any, 'm) boxed_gexpr val make_default : - ('a, 't) boxed_gexpr list -> - ('a, 't) boxed_gexpr -> - ('a, 't) boxed_gexpr -> - 't -> - ((< polymorphic : yes ; defaultTerms : yes ; .. > as 'a), 't) boxed_gexpr + ('a, 'm) boxed_gexpr list -> + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> + 'm mark -> + ((< polymorphic : yes ; defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr (** [make_default ?pos exceptions just cons] builds a term semantically equivalent to [] (the [EDefault] constructor) while avoiding redundant nested constructions. The position is extracted @@ -333,7 +337,7 @@ val make_default : [EDefault], is rewritten as [ex] *) val make_tuple : - ('a any, 'm mark) boxed_gexpr list -> 'm mark -> ('a, 'm mark) boxed_gexpr + ('a any, 'm) boxed_gexpr list -> 'm mark -> ('a, 'm) boxed_gexpr (** Builds a tuple; the mark argument is only used as witness and for position when building 0-uples *) @@ -343,11 +347,11 @@ val skip_wrappers : ('a, 'm) gexpr -> ('a, 'm) gexpr (** Removes surface logging calls and [EErrorOnEmpty] nodes. Shallow function *) val remove_logging_calls : - ((< polymorphic : yes ; .. > as 'a), 't) gexpr -> ('a, 't) boxed_gexpr + ((< polymorphic : yes ; .. > as 'a), 'm) gexpr -> ('a, 'm) boxed_gexpr (** Removes all calls to [Log] unary operators in the AST, replacing them by their argument. *) -val format : Format.formatter -> ('a, 'm mark) gexpr -> unit +val format : Format.formatter -> ('a, 'm) gexpr -> unit (** Simple printing without debug, use [Print.expr ()] instead to follow the command-line debug setting *) @@ -360,17 +364,17 @@ val compare_location : 'a glocation Mark.pos -> 'a glocation Mark.pos -> int val equal_except : except -> except -> bool val compare_except : except -> except -> int -val equal : ('a, 't) gexpr -> ('a, 't) gexpr -> bool +val equal : ('a, 'm) gexpr -> ('a, 'm) gexpr -> bool (** Determines if two expressions are equal, omitting their position information *) -val compare : ('a, 't) gexpr -> ('a, 't) gexpr -> int +val compare : ('a, 'm) gexpr -> ('a, 'm) gexpr -> int (** Standard comparison function, suitable for e.g. [Set.Make]. Ignores position information *) -val is_value : ('a any, 't) gexpr -> bool -val free_vars : ('a any, 't) gexpr -> ('a, 't) gexpr Var.Set.t +val is_value : ('a any, 'm) gexpr -> bool +val free_vars : ('a any, 'm) gexpr -> ('a, 'm) gexpr Var.Set.t -val size : ('a, 't) gexpr -> int +val size : ('a, 'm) gexpr -> int (** Used by the optimizer to know when to stop *) (** {2 Low-level handling of boxed expressions} *) @@ -385,11 +389,11 @@ module Box : sig add the annotation outside of the box, and delay its injection (using [lift]) to when the parent term gets built. *) - val lift : ('a, 't) boxed_gexpr -> ('a, 't) gexpr Bindlib.box + val lift : ('a, 'm) boxed_gexpr -> ('a, 'm) gexpr Bindlib.box (** Inject the annotation within the box, to use e.g. when a [gexpr box] is required for building parent terms *) - val app0 : ('a, 't) naked_gexpr -> 't -> ('a, 't) boxed_gexpr + val app0 : ('a, 'm) naked_gexpr -> 'm mark -> ('a, 'm) boxed_gexpr (** The [app*] functions allow building boxed expressions using [Bindlib.apply_box] and its variants, while correctly handling the expression annotations. Note that the function provided as argument should @@ -397,49 +401,49 @@ module Box : sig a separate argument. *) val app1 : - ('a, 't1) boxed_gexpr -> - (('a, 't1) gexpr -> ('a, 't2) naked_gexpr) -> - 't2 -> - ('a, 't2) boxed_gexpr + ('a, 'm1) boxed_gexpr -> + (('a, 'm1) gexpr -> ('a, 'm2) naked_gexpr) -> + 'm2 mark -> + ('a, 'm2) boxed_gexpr val app2 : - ('a, 't) boxed_gexpr -> - ('a, 't) boxed_gexpr -> - (('a, 't) gexpr -> ('a, 't) gexpr -> ('a, 't) naked_gexpr) -> - 't -> - ('a, 't) boxed_gexpr + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> + (('a, 'm) gexpr -> ('a, 'm) gexpr -> ('a, 'm) naked_gexpr) -> + 'm mark -> + ('a, 'm) boxed_gexpr val app3 : - ('a, 't) boxed_gexpr -> - ('a, 't) boxed_gexpr -> - ('a, 't) boxed_gexpr -> - (('a, 't) gexpr -> ('a, 't) gexpr -> ('a, 't) gexpr -> ('a, 't) naked_gexpr) -> - 't -> - ('a, 't) boxed_gexpr + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> + (('a, 'm) gexpr -> ('a, 'm) gexpr -> ('a, 'm) gexpr -> ('a, 'm) naked_gexpr) -> + 'm mark -> + ('a, 'm) boxed_gexpr val appn : - ('a, 't) boxed_gexpr list -> - (('a, 't) gexpr list -> ('a, 't) naked_gexpr) -> - 't -> - ('a, 't) boxed_gexpr + ('a, 'm) boxed_gexpr list -> + (('a, 'm) gexpr list -> ('a, 'm) naked_gexpr) -> + 'm mark -> + ('a, 'm) boxed_gexpr val app1n : - ('a, 't) boxed_gexpr -> - ('a, 't) boxed_gexpr list -> - (('a, 't) gexpr -> ('a, 't) gexpr list -> ('a, 't) naked_gexpr) -> - 't -> - ('a, 't) boxed_gexpr + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr list -> + (('a, 'm) gexpr -> ('a, 'm) gexpr list -> ('a, 'm) naked_gexpr) -> + 'm mark -> + ('a, 'm) boxed_gexpr val app2n : - ('a, 't) boxed_gexpr -> - ('a, 't) boxed_gexpr -> - ('a, 't) boxed_gexpr list -> - (('a, 't) gexpr -> - ('a, 't) gexpr -> - ('a, 't) gexpr list -> - ('a, 't) naked_gexpr) -> - 't -> - ('a, 't) boxed_gexpr + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr -> + ('a, 'm) boxed_gexpr list -> + (('a, 'm) gexpr -> + ('a, 'm) gexpr -> + ('a, 'm) gexpr list -> + ('a, 'm) naked_gexpr) -> + 'm mark -> + ('a, 'm) boxed_gexpr val fv : 'b Bindlib.box -> string list (** [fv] return the list of free variables from a boxed term. *) diff --git a/compiler/shared_ast/interpreter.mli b/compiler/shared_ast/interpreter.mli index c78f5760..a59210e5 100644 --- a/compiler/shared_ast/interpreter.mli +++ b/compiler/shared_ast/interpreter.mli @@ -21,11 +21,11 @@ open Catala_utils open Definitions val evaluate_operator : - ((((_, _) dcalc_lcalc as 'a), 'm mark) gexpr -> ('a, 'm mark) gexpr) -> + ((((_, _) dcalc_lcalc as 'a), 'm) gexpr -> ('a, 'm) gexpr) -> 'a operator -> 'm mark -> - ('a, 'm mark) gexpr list -> - ('a, 'm mark) gexpr + ('a, 'm) gexpr list -> + ('a, 'm) gexpr (** Evaluates the result of applying the given operator to the given arguments, which are expected to be already reduced to values. The first argument is used to evaluate expressions and called when reducing e.g. the [map] @@ -33,23 +33,23 @@ val evaluate_operator : val evaluate_expr : decl_ctx -> - (('a, 'b) dcalc_lcalc, 'm mark) gexpr -> - (('a, 'b) dcalc_lcalc, 'm mark) gexpr + (('a, 'b) dcalc_lcalc, 'm) gexpr -> + (('a, 'b) dcalc_lcalc, 'm) gexpr (** Evaluates an expression according to the semantics of the default calculus. *) val interpret_program_dcalc : - (dcalc, 'm mark) gexpr program -> + (dcalc, 'm) gexpr program -> ScopeName.t -> - (Uid.MarkedString.info * (dcalc, 'm mark) gexpr) list + (Uid.MarkedString.info * (dcalc, 'm) gexpr) list (** Interprets a program. This function expects an expression typed as a function whose argument are all thunked. The function is executed by providing for each argument a thunked empty default. Returns a list of all the computed values for the scope variables of the executed scope. *) val interpret_program_lcalc : - (lcalc, 'm mark) gexpr program -> + (lcalc, 'm) gexpr program -> ScopeName.t -> - (Uid.MarkedString.info * (lcalc, 'm mark) gexpr) list + (Uid.MarkedString.info * (lcalc, 'm) gexpr) list (** Interprets a program. This function expects an expression typed as a function whose argument are all thunked. The function is executed by providing for each argument a thunked empty default. Returns a list of all diff --git a/compiler/shared_ast/optimizations.ml b/compiler/shared_ast/optimizations.ml index 71143a52..aebd99a6 100644 --- a/compiler/shared_ast/optimizations.ml +++ b/compiler/shared_ast/optimizations.ml @@ -19,8 +19,8 @@ open Definitions type ('a, 'b, 'm) optimizations_ctx = { var_values : - ( (('a, 'b) dcalc_lcalc, 'm mark) gexpr, - (('a, 'b) dcalc_lcalc, 'm mark) gexpr ) + ( (('a, 'b) dcalc_lcalc, 'm) gexpr, + (('a, 'b) dcalc_lcalc, 'm) gexpr ) Var.Map.t; decl_ctx : decl_ctx; } @@ -61,14 +61,14 @@ let all_match_cases_map_to_same_constructor cases n = let rec optimize_expr : type a b. (a, b, 'm) optimizations_ctx -> - ((a, b) dcalc_lcalc, 'm mark) gexpr -> - ((a, b) dcalc_lcalc, 'm mark) boxed_gexpr = + ((a, b) dcalc_lcalc, 'm) gexpr -> + ((a, b) dcalc_lcalc, 'm) boxed_gexpr = fun ctx e -> (* We proceed bottom-up, first apply on the subterms *) let e = Expr.map ~f:(optimize_expr ctx) e in let mark = Mark.get e in (* Then reduce the parent node *) - let reduce (e : ((a, b) dcalc_lcalc, 'm mark) gexpr) = + let reduce (e : ((a, b) dcalc_lcalc, 'm) gexpr) = (* Todo: improve the handling of eapp(log,elit) cases here, it obfuscates the matches and the log calls are not preserved, which would be a good property *) @@ -302,9 +302,7 @@ let rec optimize_expr : in Expr.Box.app1 e reduce mark -let optimize_expr - (decl_ctx : decl_ctx) - (e : (('a, 'b) dcalc_lcalc, 'm mark) gexpr) = +let optimize_expr (decl_ctx : decl_ctx) (e : (('a, 'b) dcalc_lcalc, 'm) gexpr) = optimize_expr { var_values = Var.Map.empty; decl_ctx } e let optimize_program (p : 'm program) : 'm program = diff --git a/compiler/shared_ast/optimizations.mli b/compiler/shared_ast/optimizations.mli index 13102d24..ea413388 100644 --- a/compiler/shared_ast/optimizations.mli +++ b/compiler/shared_ast/optimizations.mli @@ -22,12 +22,12 @@ open Definitions val optimize_expr : decl_ctx -> - (('a, 'b) dcalc_lcalc, 'm mark) gexpr -> - (('a, 'b) dcalc_lcalc, 'm mark) boxed_gexpr + (('a, 'b) dcalc_lcalc, 'm) gexpr -> + (('a, 'b) dcalc_lcalc, 'm) boxed_gexpr val optimize_program : - (('a, 'b) dcalc_lcalc, 'm mark) gexpr program -> - (('a, 'b) dcalc_lcalc, 'm mark) gexpr program + (('a, 'b) dcalc_lcalc, 'm) gexpr program -> + (('a, 'b) dcalc_lcalc, 'm) gexpr program (** {1 Tests}*) diff --git a/compiler/shared_ast/print.mli b/compiler/shared_ast/print.mli index 112f711f..ba5423fd 100644 --- a/compiler/shared_ast/print.mli +++ b/compiler/shared_ast/print.mli @@ -56,7 +56,7 @@ val expr : ?debug:bool -> unit -> Format.formatter -> - ('a, 'm mark) gexpr -> + ('a, 'm) gexpr -> unit (** Same as [expr], but with a debug flag that defaults to [!Cli.debug_flag]. If [~hide_function_body:true], prints "" for [EAbs] nodes *) @@ -69,8 +69,7 @@ val scope : ?debug:bool -> decl_ctx -> Format.formatter -> - ScopeName.t * ('a, 'm mark) gexpr scope_body -> + ScopeName.t * ('a, 'm) gexpr scope_body -> unit -val program : - ?debug:bool -> Format.formatter -> ('a, 'm mark) gexpr program -> unit +val program : ?debug:bool -> Format.formatter -> ('a, 'm) gexpr program -> unit diff --git a/compiler/shared_ast/program.ml b/compiler/shared_ast/program.ml index 104ec64e..c14e3b07 100644 --- a/compiler/shared_ast/program.ml +++ b/compiler/shared_ast/program.ml @@ -40,8 +40,7 @@ let get_scope_body { code_items; _ } scope = | None -> raise Not_found | Some body -> body -let untype : 'm. ('a, 'm mark) gexpr program -> ('a, untyped mark) gexpr program - = +let untype : 'm. ('a, 'm) gexpr program -> ('a, untyped) gexpr program = fun prg -> Bindlib.unbox (map_exprs ~f:Expr.untype ~varf:Var.translate prg) let rec find_scope name vars = function diff --git a/compiler/shared_ast/program.mli b/compiler/shared_ast/program.mli index 6acf672f..5f636fdb 100644 --- a/compiler/shared_ast/program.mli +++ b/compiler/shared_ast/program.mli @@ -34,7 +34,7 @@ val fold_right_exprs : val get_scope_body : ((_ any, 't) gexpr as 'e) program -> ScopeName.t -> 'e scope_body -val untype : ('a any, _ mark) gexpr program -> ('a, untyped mark) gexpr program +val untype : ('a any, _) gexpr program -> ('a, untyped) gexpr program val to_expr : ((_ any, _) gexpr as 'e) program -> ScopeName.t -> 'e boxed (** Usage: [build_whole_program_expr program main_scope] builds an expression diff --git a/compiler/shared_ast/scope.ml b/compiler/shared_ast/scope.ml index 1ccf45ee..fa9a204e 100644 --- a/compiler/shared_ast/scope.ml +++ b/compiler/shared_ast/scope.ml @@ -168,8 +168,8 @@ let build_typ_from_sig type 'e scope_name_or_var = ScopeName of ScopeName.t | ScopeVar of 'e Var.t -let to_expr (ctx : decl_ctx) (body : 'e scope_body) (mark_scope : 'm mark) : - 'e boxed = +let to_expr (ctx : decl_ctx) (body : 'e scope_body) (mark_scope : 'm) : 'e boxed + = let var, body_expr = Bindlib.unbind body.scope_body_expr in let body_expr = unfold_body_expr ctx body_expr in Expr.make_abs [| var |] body_expr diff --git a/compiler/shared_ast/scope.mli b/compiler/shared_ast/scope.mli index 4919e8f9..8321f2b9 100644 --- a/compiler/shared_ast/scope.mli +++ b/compiler/shared_ast/scope.mli @@ -107,15 +107,12 @@ val map_exprs : (** This is the main map visitor for all the expressions inside all the scopes of the program. *) -val get_body_mark : (_, 'm mark) gexpr scope_body -> 'm mark +val get_body_mark : (_, 'm) gexpr scope_body -> 'm mark (** {2 Conversions} *) val to_expr : - decl_ctx -> - ('a any, 'm mark) gexpr scope_body -> - 'm mark -> - ('a, 'm mark) boxed_gexpr + decl_ctx -> ('a any, 'm) gexpr scope_body -> 'm mark -> ('a, 'm) boxed_gexpr (** Usage: [to_expr ctx body scope_position] where [scope_position] corresponds to the line of the scope declaration for instance. *) @@ -123,7 +120,7 @@ type 'e scope_name_or_var = ScopeName of ScopeName.t | ScopeVar of 'e Var.t val unfold : decl_ctx -> - ((_, 'm mark) gexpr as 'e) code_item_list -> + ((_, 'm) gexpr as 'e) code_item_list -> 'm mark -> 'e scope_name_or_var -> 'e boxed diff --git a/compiler/shared_ast/shared_ast.mld b/compiler/shared_ast/shared_ast.mld index 2ffe7c39..56a1e2ff 100644 --- a/compiler/shared_ast/shared_ast.mld +++ b/compiler/shared_ast/shared_ast.mld @@ -17,7 +17,7 @@ irrelevant cases, so that e.g. [(dcalc, _) naked_gexpr] doesn't have the [ERaise [ECatch] cases, while [(lcalc, _) naked_gexpr] doesn't have [EDefault]. For example, Lcalc expressions are then defined as -[type 'm naked_expr = (Shared_ast.lcalc, 'm mark) Shared_ast.naked_gexpr]. +[type 'm naked_expr = (Shared_ast.lcalc, 'm) Shared_ast.naked_gexpr]. This makes it possible to write a single function that works on the different ASTs, by having it take a [('a, _) naked_gexpr] as input, while retaining a much diff --git a/compiler/shared_ast/typing.ml b/compiler/shared_ast/typing.ml index c9091311..f8c29d9f 100644 --- a/compiler/shared_ast/typing.ml +++ b/compiler/shared_ast/typing.ml @@ -130,13 +130,11 @@ let rec format_typ exception Type_error of A.any_expr * unionfind_typ * unionfind_typ -type mark = { pos : Pos.t; uf : unionfind_typ } - (** Raises an error if unification cannot be performed. The position annotation of the second [unionfind_typ] argument is propagated (unless it is [TAny]). *) let rec unify (ctx : A.decl_ctx) - (e : ('a, 'm A.mark) A.gexpr) (* used for error context *) + (e : ('a, 'm) A.gexpr) (* used for error context *) (t1 : unionfind_typ) (t2 : unionfind_typ) : unit = let unify = unify ctx in @@ -172,14 +170,9 @@ let rec unify (fun t1 t2 -> match Mark.remove t2 with TAny _ -> t1 | _ -> t2) t1 t2 -let handle_type_error ctx e t1 t2 = +let handle_type_error ctx (A.AnyExpr e) t1 t2 = (* TODO: if we get weird error messages, then it means that we should use the persistent version of the union-find data structure. *) - let pos = - match e with - | A.AnyExpr e -> ( - match Mark.get e with A.Untyped { pos } -> pos | Typed { pos; _ } -> pos) - in let t1_repr = UnionFind.get (UnionFind.find t1) in let t2_repr = UnionFind.get (UnionFind.find t2) in let t1_pos = Mark.get t1_repr in @@ -204,7 +197,7 @@ let handle_type_error ctx e t1 t2 = ( Some (Format.asprintf "Error coming from typechecking the following expression:"), - pos ); + Expr.pos e ); Some (Format.asprintf "Type %a coming from expression:" t1_s ()), t1_pos; Some (Format.asprintf "Type %a coming from expression:" t2_s ()), t2_pos; ] @@ -336,16 +329,18 @@ module Env = struct end let add_pos e ty = Mark.add (Expr.pos e) ty -let ty (_, { uf; _ }) = uf + +let ty : (_, unionfind_typ A.custom) A.marked -> unionfind_typ = + fun (_, A.Custom { A.custom; _ }) -> custom (** Infers the most permissive type from an expression *) let rec typecheck_expr_bottom_up : type a m. leave_unresolved:bool -> A.decl_ctx -> - (a, m A.mark) A.gexpr Env.t -> - (a, m A.mark) A.gexpr -> - (a, mark) A.boxed_gexpr = + (a, m) A.gexpr Env.t -> + (a, m) A.gexpr -> + (a, unionfind_typ A.custom) A.boxed_gexpr = fun ~leave_unresolved ctx env e -> typecheck_expr_top_down ~leave_unresolved ctx env (UnionFind.make (add_pos e (TAny (Any.fresh ())))) @@ -356,10 +351,10 @@ and typecheck_expr_top_down : type a m. leave_unresolved:bool -> A.decl_ctx -> - (a, m A.mark) A.gexpr Env.t -> + (a, m) A.gexpr Env.t -> unionfind_typ -> - (a, m A.mark) A.gexpr -> - (a, mark) A.boxed_gexpr = + (a, m) A.gexpr -> + (a, unionfind_typ A.custom) A.boxed_gexpr = fun ~leave_unresolved ctx env tau e -> (* Cli.debug_format "Propagating type %a for naked_expr %a" (format_typ ctx) tau (Expr.format ctx) e; *) @@ -370,12 +365,13 @@ and typecheck_expr_top_down : match Mark.get e with | A.Untyped _ | A.Typed { A.ty = A.TAny, _; _ } -> () | A.Typed { A.ty; _ } -> unify ctx e tau (ast_to_typ ty) + | A.Custom _ -> assert false in - let context_mark = { uf = tau; pos = pos_e } in + let context_mark = A.Custom { A.custom = tau; pos = pos_e } in let mark_with_tau_and_unify uf = (* Unify with the supplied type first, and return the mark *) unify ctx e uf tau; - { uf; pos = pos_e } + A.Custom { A.custom = uf; pos = pos_e } in let unionfind ?(pos = e) t = UnionFind.make (add_pos pos t) in let ty_mark ty = mark_with_tau_and_unify (unionfind ty) in @@ -472,7 +468,8 @@ and typecheck_expr_top_down : let candidate_structs = try A.IdentName.Map.find field ctx.ctx_struct_fields with Not_found -> - Errors.raise_spanned_error context_mark.pos + Errors.raise_spanned_error + (Expr.mark_pos context_mark) "Field %a does not belong to structure %a (no structure defines \ it)" (Cli.format_with_style [ANSITerminal.yellow]) @@ -482,7 +479,8 @@ and typecheck_expr_top_down : in try A.StructName.Map.find name candidate_structs with Not_found -> - Errors.raise_spanned_error context_mark.pos + Errors.raise_spanned_error + (Expr.mark_pos context_mark) "Field %a does not belong to structure %a, but to %a" (Cli.format_with_style [ANSITerminal.yellow]) ("\"" ^ field ^ "\"") @@ -755,7 +753,7 @@ and typecheck_expr_top_down : unify ctx e t_ret (resolve_overload_ret_type ~leave_unresolved ctx e op tys'); ( List.map (typ_to_ast ~leave_unresolved) tys', - { uf = t_func; pos = pos_e } )) + A.Custom { A.custom = t_func; pos = pos_e } )) ~resolved:(fun op -> let mark = mark_with_tau_and_unify @@ -818,7 +816,7 @@ let wrap_expr ctx f e = (** {1 API} *) -let get_ty_mark ~leave_unresolved { uf; pos } = +let get_ty_mark ~leave_unresolved (A.Custom { A.custom = uf; pos }) = A.Typed { ty = typ_to_ast ~leave_unresolved uf; pos } let expr_raw @@ -827,7 +825,7 @@ let expr_raw (ctx : A.decl_ctx) ?(env = Env.empty ctx) ?(typ : A.typ option) - (e : (a, 'm) A.gexpr) : (a, mark) A.gexpr = + (e : (a, 'm) A.gexpr) : (a, unionfind_typ A.custom) A.gexpr = let fty = match typ with | None -> typecheck_expr_bottom_up ~leave_unresolved ctx env @@ -838,7 +836,7 @@ let expr_raw let check_expr ~leave_unresolved ctx ?env ?typ e = Expr.map_marks - ~f:(fun { pos; _ } -> A.Untyped { pos }) + ~f:(fun (Custom { pos; _ }) -> A.Untyped { pos }) (expr_raw ctx ~leave_unresolved ?env ?typ e) (* Infer the type of an expression *) @@ -922,7 +920,7 @@ let rec scopes ~leave_unresolved ctx env = function Bindlib.box_apply (fun body -> A.ScopeDef (name, body)) body_e ) | A.Topdef (name, typ, e) -> let e' = expr_raw ~leave_unresolved ctx ~env ~typ e in - let uf = (Mark.get e').uf in + let (A.Custom { custom = uf; _ }) = Mark.get e' in let e' = Expr.map_marks ~f:(get_ty_mark ~leave_unresolved) e' in ( Env.add var uf env, Bindlib.box_apply diff --git a/compiler/shared_ast/typing.mli b/compiler/shared_ast/typing.mli index 0602a31f..c295b34d 100644 --- a/compiler/shared_ast/typing.mli +++ b/compiler/shared_ast/typing.mli @@ -40,8 +40,8 @@ val expr : decl_ctx -> ?env:'e Env.t -> ?typ:typ -> - (('a, 'm mark) gexpr as 'e) -> - ('a, typed mark) boxed_gexpr + (('a, 'm) gexpr as 'e) -> + ('a, typed) boxed_gexpr (** Infers and marks the types for the given expression. If [typ] is provided, it is assumed to be the outer type and used for inference top-down. @@ -56,17 +56,15 @@ val check_expr : decl_ctx -> ?env:'e Env.t -> ?typ:typ -> - (('a, 'm mark) gexpr as 'e) -> - ('a, untyped mark) boxed_gexpr + (('a, 'm) gexpr as 'e) -> + ('a, untyped) boxed_gexpr (** Same as [expr], but doesn't annotate the returned expression. Equivalent to [Typing.expr |> Expr.untype], but more efficient. This can be useful for type-checking and disambiguation (some AST nodes are updated with missing information, e.g. any [TAny] appearing in the AST is replaced) *) val program : - leave_unresolved:bool -> - ('a, 'm mark) gexpr program -> - ('a, typed mark) gexpr program + leave_unresolved:bool -> ('a, 'm) gexpr program -> ('a, typed) gexpr program (** Typing on whole programs (as defined in Shared_ast.program, i.e. for the later dcalc/lcalc stages. diff --git a/french_law/catala_legifrance/catala_legifrance.ml b/french_law/catala_legifrance/catala_legifrance.ml index a897cc8a..b6c84d79 100644 --- a/french_law/catala_legifrance/catala_legifrance.ml +++ b/french_law/catala_legifrance/catala_legifrance.ml @@ -54,8 +54,7 @@ let check_article_expiration "%s %s has expired! Its expiration date is %s according to \ LĂ©giFrance.%s" (Mark.remove law_heading.Surface.Ast.law_heading_name) - (Pos.to_string - (Mark.get law_heading.Surface.Ast.law_heading_name)) + (Pos.to_string (Mark.get law_heading.Surface.Ast.law_heading_name)) (Date.print_tm legifrance_expiration_date) (match new_version with | None -> ""