Improve integration of marks into the main AST

Two interdependent changes here:
1. Enforce all instances of Shared_ast.gexpr to use the generic type for marks.
   This makes the interfaces a tad simpler to manipulate: you now write
   `('a, 'm) gexpr` rather than `('a, 'm mark) gexpr`.
2. Define a polymorphic `Custom` mark case for use by pass-specific annotations.
   And leverage this in the typing module
This commit is contained in:
Louis Gesbert 2023-05-17 16:15:00 +02:00
parent fc531777c0
commit 209be6b758
26 changed files with 363 additions and 369 deletions

View File

@ -17,7 +17,7 @@
open Shared_ast open Shared_ast
type 'm naked_expr = (dcalc, 'm mark) naked_gexpr type 'm naked_expr = (dcalc, 'm) naked_gexpr
and 'm expr = (dcalc, 'm mark) gexpr and 'm expr = (dcalc, 'm) gexpr
type 'm program = 'm expr Shared_ast.program type 'm program = 'm expr Shared_ast.program

View File

@ -19,7 +19,7 @@
open Shared_ast open Shared_ast
type 'm naked_expr = (dcalc, 'm mark) naked_gexpr type 'm naked_expr = (dcalc, 'm) naked_gexpr
and 'm expr = (dcalc, 'm mark) gexpr and 'm expr = (dcalc, 'm) gexpr
type 'm program = 'm expr Shared_ast.program type 'm program = 'm expr Shared_ast.program

View File

@ -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 (* Expression argument is used as a type witness, its type and positions aren't
used *) 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) = (Pos.t -> m mark) * ((_, Pos.t) Mark.ed -> m mark) =
let pos_mark pos = let pos_mark pos =
Expr.map_mark (fun _ -> pos) (fun _ -> TAny, pos) (Mark.get e) 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 let merge_defaults
~(is_func : bool) ~(is_func : bool)
(caller : (dcalc, 'm mark) boxed_gexpr) (caller : (dcalc, 'm) boxed_gexpr)
(callee : (dcalc, 'm mark) boxed_gexpr) : (dcalc, 'm mark) boxed_gexpr = (callee : (dcalc, 'm) boxed_gexpr) : (dcalc, 'm) boxed_gexpr =
(* the merging of the two defaults, from the reentrant caller and the callee, (* 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 is straightfoward in the general case and a little subtler when the
variable being defined is a function. *) variable being defined is a function. *)
@ -92,7 +92,7 @@ let merge_defaults
let pos = Expr.mark_pos m in let pos = Expr.mark_pos m in
Expr.make_app caller Expr.make_app caller
(List.map2 (List.map2
(fun (var : (dcalc, 'm mark) naked_gexpr Bindlib.var) ty -> (fun (var : (dcalc, 'm) naked_gexpr Bindlib.var) ty ->
Expr.evar var Expr.evar var
(* we have to correctly propagate types when doing this (* we have to correctly propagate types when doing this
rewriting *) rewriting *)

View File

@ -83,7 +83,7 @@ module LocationSet : Set.S with type elt = location Mark.pos = Set.Make (struct
let compare = Expr.compare_location let compare = Expr.compare_location
end) end)
type expr = (desugared, untyped mark) gexpr type expr = (desugared, untyped) gexpr
module ExprMap = Map.Make (struct module ExprMap = Map.Make (struct
type t = expr type t = expr

View File

@ -41,7 +41,7 @@ module AssertionName : Uid.Id with type info = Uid.MarkedString.info
(** {2 Expressions} *) (** {2 Expressions} *)
type expr = (desugared, untyped mark) gexpr type expr = (desugared, untyped) gexpr
(** See {!type:Shared_ast.naked_gexpr} for the complete definition *) (** See {!type:Shared_ast.naked_gexpr} for the complete definition *)
type location = desugared glocation type location = desugared glocation

View File

@ -16,8 +16,8 @@
open Shared_ast open Shared_ast
type 'm naked_expr = (lcalc, 'm mark) naked_gexpr type 'm naked_expr = (lcalc, 'm) naked_gexpr
and 'm expr = (lcalc, 'm mark) gexpr and 'm expr = (lcalc, 'm) gexpr
type 'm program = 'm expr Shared_ast.program type 'm program = 'm expr Shared_ast.program

View File

@ -20,8 +20,8 @@ open Shared_ast
(** {1 Abstract syntax tree} *) (** {1 Abstract syntax tree} *)
type 'm naked_expr = (lcalc, 'm mark) naked_gexpr type 'm naked_expr = (lcalc, 'm) naked_gexpr
and 'm expr = (lcalc, 'm mark) gexpr and 'm expr = (lcalc, 'm) gexpr
type 'm program = 'm expr Shared_ast.program 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}*) (** {2 Term building and management for the [option] monad}*)
module OptionMonad : sig module OptionMonad : sig
val return : val return : mark:'m mark -> ('a any, 'm) boxed_gexpr -> ('a, 'm) boxed_gexpr
mark:'m mark -> ('a any, 'm mark) boxed_gexpr -> ('a, 'm mark) boxed_gexpr val empty : mark:'m mark -> ('a any, 'm) boxed_gexpr
val empty : mark:'m mark -> ('a any, 'm mark) boxed_gexpr
val bind_var : val bind_var :
mark:'m mark -> mark:'m mark ->
('a any, 'm mark) boxed_gexpr -> ('a any, 'm) boxed_gexpr ->
('a, 'm mark) gexpr Var.t -> ('a, 'm) gexpr Var.t ->
('a, 'm mark) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 'm mark) boxed_gexpr ('a, 'm) boxed_gexpr
val bind : val bind :
mark:'m mark -> mark:'m mark ->
var_name:string -> var_name:string ->
('a any, 'm mark) boxed_gexpr -> ('a any, 'm) boxed_gexpr ->
('a, 'm mark) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 'm mark) boxed_gexpr ('a, 'm) boxed_gexpr
val bind_cont : val bind_cont :
mark:'m mark -> mark:'m mark ->
var_name:string -> var_name:string ->
(('a any, 'm mark) gexpr Var.t -> ('a, 'm mark) boxed_gexpr) -> (('a any, 'm) gexpr Var.t -> ('a, 'm) boxed_gexpr) ->
('a, 'm mark) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 'm mark) boxed_gexpr ('a, 'm) boxed_gexpr
val mbind_mvar : val mbind_mvar :
mark:'m mark -> mark:'m mark ->
('a any, 'm mark) boxed_gexpr -> ('a any, 'm) boxed_gexpr ->
('a, 'm mark) gexpr Var.t list -> ('a, 'm) gexpr Var.t list ->
('a, 'm mark) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr ('a, 'm) boxed_gexpr
val mbind : val mbind :
mark:'m mark -> mark:'m mark ->
var_name:string -> var_name:string ->
('a any, 'm mark) boxed_gexpr -> ('a any, 'm) boxed_gexpr ->
('a, 'm mark) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr ('a, 'm) boxed_gexpr
val mbind_cont : val mbind_cont :
mark:'m mark -> mark:'m mark ->
var_name:string -> var_name:string ->
(('a any, 'm mark) gexpr Var.t list -> ('a, 'm mark) boxed_gexpr) -> (('a any, 'm) gexpr Var.t list -> ('a, 'm) boxed_gexpr) ->
('a, 'm mark) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr ('a, 'm) boxed_gexpr
val error_on_empty : val error_on_empty :
mark:'m mark -> mark:'m mark ->
var_name:string -> var_name:string ->
?toplevel:bool -> ?toplevel:bool ->
((< exceptions : yes ; .. > as 'a), 'm mark) boxed_gexpr -> ((< exceptions : yes ; .. > as 'a), 'm) boxed_gexpr ->
('a, 'm mark) boxed_gexpr ('a, 'm) boxed_gexpr
val map : val map :
mark:'m mark -> mark:'m mark ->
var_name:string -> var_name:string ->
((< exceptions : no ; .. > as 'a), 'm mark) boxed_gexpr -> ((< exceptions : no ; .. > as 'a), 'm) boxed_gexpr ->
('a, 'm mark) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 'm mark) boxed_gexpr ('a, 'm) boxed_gexpr
val mmap_mvar : val mmap_mvar :
mark:'m mark -> mark:'m mark ->
('a any, 'm mark) boxed_gexpr -> ('a any, 'm) boxed_gexpr ->
('a, 'm mark) gexpr Var.t list -> ('a, 'm) gexpr Var.t list ->
('a, 'm mark) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr ('a, 'm) boxed_gexpr
val mmap : val mmap :
mark:'m mark -> mark:'m mark ->
var_name:string -> var_name:string ->
('a any, 'm mark) boxed_gexpr -> ('a any, 'm) boxed_gexpr ->
('a, 'm mark) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr ('a, 'm) boxed_gexpr
end end

View File

@ -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 var_ctx = { info_pure : bool; is_scope : bool; var : 'm Ast.expr Var.t }
type 'm ctx = { type 'm ctx = {
ctx_vars : ctx_vars : ((dcalc, 'm) gexpr, 'm var_ctx) Var.Map.t;
((dcalc, 'm mark) Shared_ast__Definitions.gexpr, 'm var_ctx) Var.Map.t;
ctx_context_name : string; 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 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 [money option]. We rely on later optimization to shorten the size of the
generated code. *) generated code. *)
let rec trans (ctx : typed ctx) (e : typed D.expr) : let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
(lcalc, typed mark) boxed_gexpr = =
let m = Mark.get e in let m = Mark.get e in
let mark = m in let mark = m in
let pos = Expr.pos e 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 scope_let_expr scope_let_next
and trans_scope_body_expr ctx s : 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 match s with
| Result e -> begin | Result e -> begin
(* invariant : result is always in the form of a record. *) (* invariant : result is always in the form of a record. *)
@ -662,7 +661,7 @@ let trans_scope_body
binder binder
let rec trans_code_items (ctx : typed ctx) (c : typed D.expr code_item_list) : 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 match c with
| Nil -> Bindlib.box Nil | Nil -> Bindlib.box Nil
| Cons (c, next) -> ( | Cons (c, next) -> (

View File

@ -37,8 +37,7 @@ let value_level = { eval_struct = false; eval_op = true; eval_default = true }
module Env = struct module Env = struct
type 'm t = type 'm t =
| Env of | Env of ((dcalc, 'm) gexpr, ((dcalc, 'm) gexpr * 'm t) ref) Var.Map.t
((dcalc, 'm mark) gexpr, ((dcalc, 'm mark) gexpr * 'm t) ref) Var.Map.t
let find v (Env t) = Var.Map.find v 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) 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 -> decl_ctx ->
'm Env.t -> 'm Env.t ->
laziness_level -> laziness_level ->
(dcalc, 'm mark) gexpr -> (dcalc, 'm) gexpr ->
(dcalc, 'm mark) gexpr * 'm Env.t = (dcalc, 'm) gexpr * 'm Env.t =
fun ctx env llevel e0 -> fun ctx env llevel e0 ->
let eval_to_value ?(eval_default = true) env e = let eval_to_value ?(eval_default = true) env e =
lazy_eval ctx env { value_level with eval_default } 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) | _ -> error e "Invalid assertion condition %a" Expr.format e)
| _ -> . | _ -> .
let interpret_program let interpret_program (prg : ('dcalc, 'm) gexpr program) (scope : ScopeName.t) :
(prg : ('dcalc, 'm mark) gexpr program) ('t, 'm) gexpr * 'm Env.t =
(scope : ScopeName.t) : ('t, 'm mark) gexpr * 'm Env.t =
let ctx = prg.decl_ctx in let ctx = prg.decl_ctx in
let all_env, scopes = let all_env, scopes =
Scope.fold_left prg.code_items ~init:(Env.empty, ScopeName.Map.empty) Scope.fold_left prg.code_items ~init:(Env.empty, ScopeName.Map.empty)

View File

@ -25,7 +25,7 @@ module LocationSet : Set.S with type elt = location Mark.pos = Set.Make (struct
let compare = Expr.compare_location let compare = Expr.compare_location
end) end)
type 'm expr = (scopelang, 'm mark) gexpr type 'm expr = (scopelang, 'm) gexpr
let rec locations_used (e : 'm expr) : LocationSet.t = let rec locations_used (e : 'm expr) : LocationSet.t =
match e with match e with

View File

@ -27,7 +27,7 @@ module LocationSet : Set.S with type elt = location Mark.pos
(** {1 Abstract syntax tree} *) (** {1 Abstract syntax tree} *)
type 'm expr = (scopelang, 'm mark) gexpr type 'm expr = (scopelang, 'm) gexpr
val locations_used : 'm expr -> LocationSet.t val locations_used : 'm expr -> LocationSet.t

View File

@ -287,6 +287,24 @@ end
type 'a operator = 'a Op.t type 'a operator = 'a Op.t
type except = ConflictError | EmptyError | NoValueProvided | Crash 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} *) (** {2 Generic expressions} *)
(** Define a common base type for the expressions in most passes of the compiler *) (** 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 TopdefName.t Mark.pos
-> < explicitScopes : yes ; .. > glocation -> < 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 (** General expressions: groups all expression cases of the different ASTs, and
uses a GADT to eliminate irrelevant cases for each one. The ['t] annotations 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, 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-formed AST types, but differentiating them ephemerally allows us to do
well-typed recursive transformations on the AST that change its type *) 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 *) (* Constructors common to all ASTs *)
| ELit : lit -> ('a, < .. >, 't) base_gexpr | ELit : lit -> ('a, < .. >, 'm) base_gexpr
| EApp : { | EApp : {
f : ('a, 't) gexpr; f : ('a, 'm) gexpr;
args : ('a, 't) gexpr list; args : ('a, 'm) gexpr list;
} }
-> ('a, < .. >, 't) base_gexpr -> ('a, < .. >, 'm) base_gexpr
| EOp : { | EOp : {
op : 'b operator; op : 'b operator;
tys : typ list; tys : typ list;
} }
-> ('a, (< .. > as 'b), 't) base_gexpr -> ('a, (< .. > as 'b), 'm) base_gexpr
| EArray : ('a, 't) gexpr list -> ('a, < .. >, 't) base_gexpr | EArray : ('a, 'm) gexpr list -> ('a, < .. >, 'm) base_gexpr
| EVar : ('a, 't) naked_gexpr Bindlib.var -> ('a, _, 't) base_gexpr | EVar : ('a, 'm) naked_gexpr Bindlib.var -> ('a, _, 'm) base_gexpr
| EAbs : { | 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; tys : typ list;
} }
-> ('a, < .. >, 't) base_gexpr -> ('a, < .. >, 'm) base_gexpr
| EIfThenElse : { | EIfThenElse : {
cond : ('a, 't) gexpr; cond : ('a, 'm) gexpr;
etrue : ('a, 't) gexpr; etrue : ('a, 'm) gexpr;
efalse : ('a, 't) gexpr; efalse : ('a, 'm) gexpr;
} }
-> ('a, < .. >, 't) base_gexpr -> ('a, < .. >, 'm) base_gexpr
| EStruct : { | EStruct : {
name : StructName.t; 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 : { | EInj : {
name : EnumName.t; name : EnumName.t;
e : ('a, 't) gexpr; e : ('a, 'm) gexpr;
cons : EnumConstructor.t; cons : EnumConstructor.t;
} }
-> ('a, < .. >, 't) base_gexpr -> ('a, < .. >, 'm) base_gexpr
| EMatch : { | EMatch : {
name : EnumName.t; name : EnumName.t;
e : ('a, 't) gexpr; e : ('a, 'm) gexpr;
cases : ('a, 't) gexpr EnumConstructor.Map.t; cases : ('a, 'm) gexpr EnumConstructor.Map.t;
} }
-> ('a, < .. >, 't) base_gexpr -> ('a, < .. >, 'm) base_gexpr
| ETuple : ('a, 't) gexpr list -> ('a, < .. >, 't) base_gexpr | ETuple : ('a, 'm) gexpr list -> ('a, < .. >, 'm) base_gexpr
| ETupleAccess : { | ETupleAccess : {
e : ('a, 't) gexpr; e : ('a, 'm) gexpr;
index : int; index : int;
size : int; size : int;
} }
-> ('a, < .. >, 't) base_gexpr -> ('a, < .. >, 'm) base_gexpr
(* Early stages *) (* Early stages *)
| ELocation : 'b glocation -> ('a, (< .. > as 'b), 't) base_gexpr | ELocation : 'b glocation -> ('a, (< .. > as 'b), 'm) base_gexpr
| EScopeCall : { | EScopeCall : {
scope : ScopeName.t; 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 : { | EDStructAccess : {
name_opt : StructName.t option; name_opt : StructName.t option;
e : ('a, 't) gexpr; e : ('a, 'm) gexpr;
field : IdentName.t; field : IdentName.t;
} }
-> ('a, < syntacticNames : yes ; .. >, 't) base_gexpr -> ('a, < syntacticNames : yes ; .. >, 'm) base_gexpr
(** [desugared] has ambiguous struct fields *) (** [desugared] has ambiguous struct fields *)
| EStructAccess : { | EStructAccess : {
name : StructName.t; name : StructName.t;
e : ('a, 't) gexpr; e : ('a, 'm) gexpr;
field : StructField.t; field : StructField.t;
} }
-> ('a, < resolvedNames : yes ; .. >, 't) base_gexpr -> ('a, < resolvedNames : yes ; .. >, 'm) base_gexpr
(** Resolved struct/enums, after [desugared] *) (** Resolved struct/enums, after [desugared] *)
(* Lambda-like *) (* Lambda-like *)
| EAssert : ('a, 't) gexpr -> ('a, < assertions : yes ; .. >, 't) base_gexpr | EAssert : ('a, 'm) gexpr -> ('a, < assertions : yes ; .. >, 'm) base_gexpr
(* Default terms *) (* Default terms *)
| EDefault : { | EDefault : {
excepts : ('a, 't) gexpr list; excepts : ('a, 'm) gexpr list;
just : ('a, 't) gexpr; just : ('a, 'm) gexpr;
cons : ('a, 't) gexpr; cons : ('a, 'm) gexpr;
} }
-> ('a, < defaultTerms : yes ; .. >, 't) base_gexpr -> ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr
| EEmptyError : ('a, < defaultTerms : yes ; .. >, 't) base_gexpr | EEmptyError : ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr
| EErrorOnEmpty : | EErrorOnEmpty :
('a, 't) gexpr ('a, 'm) gexpr
-> ('a, < defaultTerms : yes ; .. >, 't) base_gexpr -> ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr
(* Lambda calculus with exceptions *) (* Lambda calculus with exceptions *)
| ERaise : except -> ('a, < exceptions : yes ; .. >, 't) base_gexpr | ERaise : except -> ('a, < exceptions : yes ; .. >, 'm) base_gexpr
| ECatch : { | ECatch : {
body : ('a, 't) gexpr; body : ('a, 'm) gexpr;
exn : except; 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 *) (** Useful for errors and printing, for example *)
(* type any_expr = AnyExpr : ('a, _ mark) gexpr -> any_expr *) 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 *) (** The annotation is lifted outside of the box for expressions *)
type 'e boxed = ('a, 't) boxed_gexpr constraint 'e = ('a, 't) gexpr type 'e boxed = ('a, 'm) boxed_gexpr constraint 'e = ('a, 'm) gexpr
(** [('a, 't) gexpr boxed] is [('a, 't) boxed_gexpr]. The difference with (** [('a, 'm) gexpr boxed] is [('a, 'm) boxed_gexpr]. The difference with
[('a, 't) gexpr Bindlib.box] is that the annotations is outside of the box, [('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 *) and can therefore be accessed without the need to resolve the box *)
type ('e, 'b) binder = (('a, 't) naked_gexpr, 'b) Bindlib.binder type ('e, 'b) binder = (('a, 'm) naked_gexpr, 'b) Bindlib.binder
constraint 'e = ('a, 't) gexpr constraint 'e = ('a, 'm) gexpr
(** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib} (** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib}
library, based on higher-order abstract syntax *) library, based on higher-order abstract syntax *)
type ('e, 'b) mbinder = (('a, 't) naked_gexpr, 'b) Bindlib.mbinder type ('e, 'b) mbinder = (('a, 'm) naked_gexpr, 'b) Bindlib.mbinder
constraint 'e = ('a, 't) gexpr constraint 'e = ('a, 'm) 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
(** {2 Higher-level program structure} *) (** {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 *) (* todo ? Factorise the code_item _list type below and use it here *)
scope_let_pos : Pos.t; 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 (** This type is parametrized by the expression type so it can be reused in
later intermediate representations. *) later intermediate representations. *)
@ -506,14 +509,14 @@ type 'e scope_let = {
and 'e scope_body_expr = and 'e scope_body_expr =
| Result of 'e | Result of 'e
| ScopeLet of 'e scope_let | ScopeLet of 'e scope_let
constraint 'e = ('a any, _ mark) gexpr constraint 'e = ('a any, _) gexpr
type 'e scope_body = { type 'e scope_body = {
scope_body_input_struct : StructName.t; scope_body_input_struct : StructName.t;
scope_body_output_struct : StructName.t; scope_body_output_struct : StructName.t;
scope_body_expr : ('e, 'e scope_body_expr) binder; 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 (** 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 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 a result expression that uses the let-binded variables. The first binder is

View File

@ -174,24 +174,25 @@ let escopecall scope args mark =
let no_mark : type m. m mark -> m mark = function let no_mark : type m. m mark -> m mark = function
| Untyped _ -> Untyped { pos = Pos.no_pos } | Untyped _ -> Untyped { pos = Pos.no_pos }
| Typed _ -> Typed { pos = Pos.no_pos; ty = Mark.add Pos.no_pos TAny } | 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 = 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 let x = Var.make "x" in
eabs (bind [| x |] (evar x mark)) [TAny, mark_pos mark] mark eabs (bind [| x |] (evar x mark)) [TAny, mark_pos mark] mark
let ty (_, m) : typ = match m with Typed { ty; _ } -> ty let ty (_, m) : typ = match m with Typed { ty; _ } -> ty
let set_ty (type m) (ty : typ) (x : ('a, m mark) Mark.ed) : let set_ty (type m) (ty : typ) (x : ('a, m) marked) : ('a, typed) marked =
('a, typed mark) Mark.ed =
Mark.add Mark.add
(match Mark.get x with (match Mark.get x with
| Untyped { pos } -> Typed { pos; ty } | 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) (Mark.remove x)
let map_mark (type m) (pos_f : Pos.t -> Pos.t) (ty_f : typ -> typ) (m : m mark) 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 match m with
| Untyped { pos } -> Untyped { pos = pos_f pos } | Untyped { pos } -> Untyped { pos = pos_f pos }
| Typed { pos; ty } -> Typed { pos = pos_f pos; ty = ty_f ty } | Typed { pos; ty } -> Typed { pos = pos_f pos; ty = ty_f ty }
| Custom { pos; custom } -> Custom { pos = pos_f pos; custom }
let map_mark2 let map_mark2
(type m) (type m)
@ -209,6 +211,7 @@ let map_mark2
match m1, m2 with match m1, m2 with
| Untyped m1, Untyped m2 -> Untyped { pos = pos_f m1.pos m2.pos } | 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 } | 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 let fold_marks
(type m) (type m)
@ -225,6 +228,7 @@ let fold_marks
pos = pos_f (List.map (function Typed { pos; _ } -> pos) ms); pos = pos_f (List.map (function Typed { pos; _ } -> pos) ms);
ty = ty_f (List.map (function Typed m -> m) 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 = let with_pos (type m) (pos : Pos.t) (m : m mark) : m mark =
map_mark (fun _ -> pos) (fun ty -> ty) m 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 map_mark (fun default -> Option.value pos ~default) (fun _ -> ty) m
let maybe_ty (type m) ?(typ = TAny) (m : m mark) : typ = 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) - *) (* - Predefined types (option) - *)
@ -254,7 +260,7 @@ let option_enum_config =
let map let map
(type a b) (type a b)
~(f : (a, 'm1) gexpr -> (b, 'm2) boxed_gexpr) ~(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 let m = Mark.get e in
match Mark.remove e with match Mark.remove e with
| ELit l -> elit l m | ELit l -> elit l m
@ -294,9 +300,7 @@ let map
escopecall scope fields m escopecall scope fields m
let rec map_top_down ~f e = map ~f:(map_top_down ~f) (f e) 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. *) (* Folds the given function on the direct children of the given expression. *)
let shallow_fold let shallow_fold
@ -333,7 +337,7 @@ let map_gather
~(acc : 'acc) ~(acc : 'acc)
~(join : 'acc -> 'acc -> 'acc) ~(join : 'acc -> 'acc -> 'acc)
~(f : (a, 'm1) gexpr -> 'acc * (a, 'm2) boxed_gexpr) ~(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 m = Mark.get e in
let lfoldmap es = let lfoldmap es =
let acc, r_es = let acc, r_es =

View File

@ -22,130 +22,134 @@ open Definitions
(** {2 Boxed constructors} *) (** {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 *) (** 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] *) (** 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 *) (** 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 : val bind :
('a, 't) gexpr Var.t array -> ('a, 'm) gexpr Var.t array ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
(('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder Bindlib.box (('a, 'm) naked_gexpr, ('a, 'm) gexpr) Bindlib.mbinder Bindlib.box
val subst : val subst :
(('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder -> (('a, 'm) naked_gexpr, ('a, 'm) gexpr) Bindlib.mbinder ->
('a, 't) gexpr list -> ('a, 'm) gexpr list ->
('a, 't) gexpr ('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 : 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 earray : ('a, 'm) boxed_gexpr list -> 'm mark -> ('a any, 'm) boxed_gexpr
val elit : lit -> 't -> ('a any, 't) boxed_gexpr val elit : lit -> 'm mark -> ('a any, 'm) boxed_gexpr
val eabs : 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 -> typ list ->
't -> 'm mark ->
('a any, 't) boxed_gexpr ('a any, 'm) boxed_gexpr
val eapp : val eapp :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 't) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
't -> 'm mark ->
('a any, 't) boxed_gexpr ('a any, 'm) boxed_gexpr
val eassert : val eassert :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
't -> 'm mark ->
((< assertions : yes ; .. > as 'a), 't) boxed_gexpr ((< 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 : val edefault :
('a, 't) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
't -> 'm mark ->
((< defaultTerms : yes ; .. > as 'a), 't) boxed_gexpr ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
val eifthenelse : val eifthenelse :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
't -> 'm mark ->
('a any, 't) boxed_gexpr ('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 : val eerroronempty :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
't -> 'm mark ->
((< defaultTerms : yes ; .. > as 'a), 't) boxed_gexpr ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
val ecatch : val ecatch :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
except -> except ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
't -> 'm mark ->
((< exceptions : yes ; .. > as 'a), 't) boxed_gexpr ((< exceptions : yes ; .. > as 'a), 'm) boxed_gexpr
val eraise : except -> 't -> (< exceptions : yes ; .. >, 't) boxed_gexpr val eraise : except -> 'm mark -> (< exceptions : yes ; .. >, 'm) boxed_gexpr
val elocation : 'a glocation -> 't -> ((< .. > as 'a), 't) boxed_gexpr val elocation : 'a glocation -> 'm mark -> ((< .. > as 'a), 'm) boxed_gexpr
val estruct : val estruct :
StructName.t -> StructName.t ->
('a, 't) boxed_gexpr StructField.Map.t -> ('a, 'm) boxed_gexpr StructField.Map.t ->
't -> 'm mark ->
('a any, 't) boxed_gexpr ('a any, 'm) boxed_gexpr
val edstructaccess : val edstructaccess :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
IdentName.t -> IdentName.t ->
StructName.t option -> StructName.t option ->
't -> 'm mark ->
((< syntacticNames : yes ; .. > as 'a), 't) boxed_gexpr ((< syntacticNames : yes ; .. > as 'a), 'm) boxed_gexpr
val estructaccess : val estructaccess :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
StructField.t -> StructField.t ->
StructName.t -> StructName.t ->
't -> 'm mark ->
((< resolvedNames : yes ; .. > as 'a), 't) boxed_gexpr ((< resolvedNames : yes ; .. > as 'a), 'm) boxed_gexpr
val einj : val einj :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
EnumConstructor.t -> EnumConstructor.t ->
EnumName.t -> EnumName.t ->
't -> 'm mark ->
('a any, 't) boxed_gexpr ('a any, 'm) boxed_gexpr
val ematch : val ematch :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
EnumName.t -> EnumName.t ->
('a, 't) boxed_gexpr EnumConstructor.Map.t -> ('a, 'm) boxed_gexpr EnumConstructor.Map.t ->
't -> 'm mark ->
('a any, 't) boxed_gexpr ('a any, 'm) boxed_gexpr
val escopecall : val escopecall :
ScopeName.t -> ScopeName.t ->
('a, 't) boxed_gexpr ScopeVar.Map.t -> ('a, 'm) boxed_gexpr ScopeVar.Map.t ->
't -> 'm mark ->
((< explicitScopes : yes ; .. > as 'a), 't) boxed_gexpr ((< 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} *) (** {2 Manipulation of marks} *)
val no_mark : 'm mark -> 'm mark 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 mark_pos : 'm mark -> Pos.t
val with_pos : Pos.t -> 'm mark -> 'm mark val with_pos : Pos.t -> 'm mark -> 'm mark
@ -163,9 +167,11 @@ val map_mark2 :
'm mark -> 'm mark ->
'm mark -> 'm mark ->
'm mark 'm mark
(** @raise Invalid_arg on custom marks*)
val fold_marks : val fold_marks :
(Pos.t list -> Pos.t) -> (typed list -> typ) -> 'm mark list -> 'm mark (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 val maybe_ty : ?typ:naked_typ -> 'm mark -> typ
(** Returns the corresponding type on a typed expr, or [typ] (defaulting to (** 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 *) (** Manipulation of marked expressions *)
val pos : ('a, 'm mark) Mark.ed -> Pos.t val pos : ('a, 'm) marked -> Pos.t
val ty : ('e, typed mark) Mark.ed -> typ val ty : ('e, typed) marked -> typ
val set_ty : typ -> ('a, 'm mark) Mark.ed -> ('a, typed mark) Mark.ed val set_ty : typ -> ('a, 'm) marked -> ('a, typed) marked
val untype : ('a, 'm mark) gexpr -> ('a, untyped mark) boxed_gexpr val untype : ('a, 'm) gexpr -> ('a, untyped) boxed_gexpr
(** {2 Traversal functions} *) (** {2 Traversal functions} *)
val map : val map :
f:(('a, 'm1) gexpr -> ('b, 'm2) boxed_gexpr) -> 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 ('b, 'm2) boxed_gexpr
(** Shallow mapping on expressions (non recursive): applies the given function (** Shallow mapping on expressions (non recursive): applies the given function
to all sub-terms of the given expression, and rebuilds the node. to all sub-terms of the given expression, and rebuilds the node.
@ -223,17 +229,18 @@ val map :
becomes useful. *) becomes useful. *)
val map_top_down : val map_top_down :
f:(('a, 't1) gexpr -> (('a, 't1) naked_gexpr, 't2) Mark.ed) -> f:(('a, 'm1) gexpr -> (('a, 'm1) naked_gexpr, 'm2) marked) ->
('a, 't1) gexpr -> ('a, 'm1) gexpr ->
('a, 't2) boxed_gexpr ('a, 'm2) boxed_gexpr
(** Recursively applies [f] to the nodes of the expression tree. The type (** 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, returned by [f] is hybrid since the mark at top-level has been rewritten,
but not yet the marks in the subtrees. *) 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 : 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 (** 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 recurse. It opens binders unless you avoid sending binders to the function
like the example below. Useful as helper for recursive calls within like the example below. Useful as helper for recursive calls within
@ -252,9 +259,9 @@ val shallow_fold :
val map_gather : val map_gather :
acc:'acc -> acc:'acc ->
join:('acc -> 'acc -> 'acc) -> join:('acc -> 'acc -> 'acc) ->
f:(('a, 't1) gexpr -> 'acc * ('a, 't2) boxed_gexpr) -> f:(('a, 'm1) gexpr -> 'acc * ('a, 'm2) boxed_gexpr) ->
(('a, 't1) naked_gexpr, 't2) Mark.ed -> (('a, 'm1) naked_gexpr, 'm2) marked ->
'acc * ('a, 't2) boxed_gexpr 'acc * ('a, 'm2) boxed_gexpr
(** Shallow mapping similar to [map], but additionally allows to gather an (** Shallow mapping similar to [map], but additionally allows to gather an
accumulator bottom-up. [acc] is the accumulator value returned on terminal accumulator bottom-up. [acc] is the accumulator value returned on terminal
nodes, and [join] is used to merge accumulators from the different sub-terms nodes, and [join] is used to merge accumulators from the different sub-terms
@ -273,52 +280,49 @@ val map_gather :
(** {2 Expression building helpers} *) (** {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 : val make_abs :
('a, 'm mark) gexpr Var.vars -> ('a, 'm) gexpr Var.vars ->
('a, 'm mark) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
typ list -> typ list ->
Pos.t -> Pos.t ->
('a any, 'm mark) boxed_gexpr ('a any, 'm) boxed_gexpr
val make_app : val make_app :
('a any, 'm mark) boxed_gexpr -> ('a any, 'm) boxed_gexpr ->
('a, 'm mark) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
Pos.t -> Pos.t ->
('a any, 'm mark) boxed_gexpr ('a any, 'm) boxed_gexpr
val empty_thunked_term : val empty_thunked_term :
'm mark -> (< defaultTerms : yes ; .. >, 'm mark) boxed_gexpr 'm mark -> (< defaultTerms : yes ; .. >, 'm) boxed_gexpr
val thunk_term : val thunk_term : ('a any, 'b) boxed_gexpr -> 'b mark -> ('a, 'b) boxed_gexpr
('a any, 'b mark) boxed_gexpr -> 'b mark -> ('a, 'b mark) boxed_gexpr val unthunk_term_nobox : ('a any, 'm) gexpr -> 'm mark -> ('a, 'm) gexpr
val unthunk_term_nobox :
('a any, 'm mark) gexpr -> 'm mark -> ('a, 'm mark) gexpr
val make_let_in : val make_let_in :
('a, 'm mark) gexpr Var.t -> ('a, 'm) gexpr Var.t ->
typ -> typ ->
('a, 'm mark) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 'm mark) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
Pos.t -> Pos.t ->
('a any, 'm mark) boxed_gexpr ('a any, 'm) boxed_gexpr
val make_multiple_let_in : val make_multiple_let_in :
('a, 'm mark) gexpr Var.vars -> ('a, 'm) gexpr Var.vars ->
typ list -> typ list ->
('a, 'm mark) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
Pos.t -> Pos.t ->
('a any, 'm mark) boxed_gexpr ('a any, 'm) boxed_gexpr
val make_default : val make_default :
('a, 't) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
't -> 'm mark ->
((< polymorphic : yes ; defaultTerms : yes ; .. > as 'a), 't) boxed_gexpr ((< polymorphic : yes ; defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
(** [make_default ?pos exceptions just cons] builds a term semantically (** [make_default ?pos exceptions just cons] builds a term semantically
equivalent to [<exceptions | just :- cons>] (the [EDefault] constructor) equivalent to [<exceptions | just :- cons>] (the [EDefault] constructor)
while avoiding redundant nested constructions. The position is extracted while avoiding redundant nested constructions. The position is extracted
@ -333,7 +337,7 @@ val make_default :
[EDefault], is rewritten as [ex] *) [EDefault], is rewritten as [ex] *)
val make_tuple : 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 (** Builds a tuple; the mark argument is only used as witness and for position
when building 0-uples *) 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 *) (** Removes surface logging calls and [EErrorOnEmpty] nodes. Shallow function *)
val remove_logging_calls : 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 (** Removes all calls to [Log] unary operators in the AST, replacing them by
their argument. *) 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 (** Simple printing without debug, use [Print.expr ()] instead to follow the
command-line debug setting *) 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 equal_except : except -> except -> bool
val compare_except : except -> except -> int 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 *) (** 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 (** Standard comparison function, suitable for e.g. [Set.Make]. Ignores position
information *) information *)
val is_value : ('a any, 't) gexpr -> bool val is_value : ('a any, 'm) gexpr -> bool
val free_vars : ('a any, 't) gexpr -> ('a, 't) gexpr Var.Set.t 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 *) (** Used by the optimizer to know when to stop *)
(** {2 Low-level handling of boxed expressions} *) (** {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 add the annotation outside of the box, and delay its injection (using
[lift]) to when the parent term gets built. *) [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 (** Inject the annotation within the box, to use e.g. when a [gexpr box] is
required for building parent terms *) 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 (** The [app*] functions allow building boxed expressions using
[Bindlib.apply_box] and its variants, while correctly handling the [Bindlib.apply_box] and its variants, while correctly handling the
expression annotations. Note that the function provided as argument should expression annotations. Note that the function provided as argument should
@ -397,49 +401,49 @@ module Box : sig
a separate argument. *) a separate argument. *)
val app1 : val app1 :
('a, 't1) boxed_gexpr -> ('a, 'm1) boxed_gexpr ->
(('a, 't1) gexpr -> ('a, 't2) naked_gexpr) -> (('a, 'm1) gexpr -> ('a, 'm2) naked_gexpr) ->
't2 -> 'm2 mark ->
('a, 't2) boxed_gexpr ('a, 'm2) boxed_gexpr
val app2 : val app2 :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
(('a, 't) gexpr -> ('a, 't) gexpr -> ('a, 't) naked_gexpr) -> (('a, 'm) gexpr -> ('a, 'm) gexpr -> ('a, 'm) naked_gexpr) ->
't -> 'm mark ->
('a, 't) boxed_gexpr ('a, 'm) boxed_gexpr
val app3 : val app3 :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
(('a, 't) gexpr -> ('a, 't) gexpr -> ('a, 't) gexpr -> ('a, 't) naked_gexpr) -> (('a, 'm) gexpr -> ('a, 'm) gexpr -> ('a, 'm) gexpr -> ('a, 'm) naked_gexpr) ->
't -> 'm mark ->
('a, 't) boxed_gexpr ('a, 'm) boxed_gexpr
val appn : val appn :
('a, 't) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
(('a, 't) gexpr list -> ('a, 't) naked_gexpr) -> (('a, 'm) gexpr list -> ('a, 'm) naked_gexpr) ->
't -> 'm mark ->
('a, 't) boxed_gexpr ('a, 'm) boxed_gexpr
val app1n : val app1n :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 't) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
(('a, 't) gexpr -> ('a, 't) gexpr list -> ('a, 't) naked_gexpr) -> (('a, 'm) gexpr -> ('a, 'm) gexpr list -> ('a, 'm) naked_gexpr) ->
't -> 'm mark ->
('a, 't) boxed_gexpr ('a, 'm) boxed_gexpr
val app2n : val app2n :
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 't) boxed_gexpr -> ('a, 'm) boxed_gexpr ->
('a, 't) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
(('a, 't) gexpr -> (('a, 'm) gexpr ->
('a, 't) gexpr -> ('a, 'm) gexpr ->
('a, 't) gexpr list -> ('a, 'm) gexpr list ->
('a, 't) naked_gexpr) -> ('a, 'm) naked_gexpr) ->
't -> 'm mark ->
('a, 't) boxed_gexpr ('a, 'm) boxed_gexpr
val fv : 'b Bindlib.box -> string list val fv : 'b Bindlib.box -> string list
(** [fv] return the list of free variables from a boxed term. *) (** [fv] return the list of free variables from a boxed term. *)

View File

@ -21,11 +21,11 @@ open Catala_utils
open Definitions open Definitions
val evaluate_operator : 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 -> 'a operator ->
'm mark -> 'm mark ->
('a, 'm mark) gexpr list -> ('a, 'm) gexpr list ->
('a, 'm mark) gexpr ('a, 'm) gexpr
(** Evaluates the result of applying the given operator to the given arguments, (** 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 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] used to evaluate expressions and called when reducing e.g. the [map]
@ -33,23 +33,23 @@ val evaluate_operator :
val evaluate_expr : val evaluate_expr :
decl_ctx -> decl_ctx ->
(('a, 'b) dcalc_lcalc, 'm mark) gexpr -> (('a, 'b) dcalc_lcalc, 'm) gexpr ->
(('a, 'b) dcalc_lcalc, 'm mark) gexpr (('a, 'b) dcalc_lcalc, 'm) gexpr
(** Evaluates an expression according to the semantics of the default calculus. *) (** Evaluates an expression according to the semantics of the default calculus. *)
val interpret_program_dcalc : val interpret_program_dcalc :
(dcalc, 'm mark) gexpr program -> (dcalc, 'm) gexpr program ->
ScopeName.t -> 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 (** Interprets a program. This function expects an expression typed as a
function whose argument are all thunked. The function is executed by function whose argument are all thunked. The function is executed by
providing for each argument a thunked empty default. Returns a list of all providing for each argument a thunked empty default. Returns a list of all
the computed values for the scope variables of the executed scope. *) the computed values for the scope variables of the executed scope. *)
val interpret_program_lcalc : val interpret_program_lcalc :
(lcalc, 'm mark) gexpr program -> (lcalc, 'm) gexpr program ->
ScopeName.t -> 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 (** Interprets a program. This function expects an expression typed as a
function whose argument are all thunked. The function is executed by function whose argument are all thunked. The function is executed by
providing for each argument a thunked empty default. Returns a list of all providing for each argument a thunked empty default. Returns a list of all

View File

@ -19,8 +19,8 @@ open Definitions
type ('a, 'b, 'm) optimizations_ctx = { type ('a, 'b, 'm) optimizations_ctx = {
var_values : var_values :
( (('a, 'b) dcalc_lcalc, 'm mark) gexpr, ( (('a, 'b) dcalc_lcalc, 'm) gexpr,
(('a, 'b) dcalc_lcalc, 'm mark) gexpr ) (('a, 'b) dcalc_lcalc, 'm) gexpr )
Var.Map.t; Var.Map.t;
decl_ctx : decl_ctx; decl_ctx : decl_ctx;
} }
@ -61,14 +61,14 @@ let all_match_cases_map_to_same_constructor cases n =
let rec optimize_expr : let rec optimize_expr :
type a b. type a b.
(a, b, 'm) optimizations_ctx -> (a, b, 'm) optimizations_ctx ->
((a, b) dcalc_lcalc, 'm mark) gexpr -> ((a, b) dcalc_lcalc, 'm) gexpr ->
((a, b) dcalc_lcalc, 'm mark) boxed_gexpr = ((a, b) dcalc_lcalc, 'm) boxed_gexpr =
fun ctx e -> fun ctx e ->
(* We proceed bottom-up, first apply on the subterms *) (* We proceed bottom-up, first apply on the subterms *)
let e = Expr.map ~f:(optimize_expr ctx) e in let e = Expr.map ~f:(optimize_expr ctx) e in
let mark = Mark.get e in let mark = Mark.get e in
(* Then reduce the parent node *) (* 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 (* 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 the matches and the log calls are not preserved, which would be a good
property *) property *)
@ -302,9 +302,7 @@ let rec optimize_expr :
in in
Expr.Box.app1 e reduce mark Expr.Box.app1 e reduce mark
let optimize_expr let optimize_expr (decl_ctx : decl_ctx) (e : (('a, 'b) dcalc_lcalc, 'm) gexpr) =
(decl_ctx : decl_ctx)
(e : (('a, 'b) dcalc_lcalc, 'm mark) gexpr) =
optimize_expr { var_values = Var.Map.empty; decl_ctx } e optimize_expr { var_values = Var.Map.empty; decl_ctx } e
let optimize_program (p : 'm program) : 'm program = let optimize_program (p : 'm program) : 'm program =

View File

@ -22,12 +22,12 @@ open Definitions
val optimize_expr : val optimize_expr :
decl_ctx -> decl_ctx ->
(('a, 'b) dcalc_lcalc, 'm mark) gexpr -> (('a, 'b) dcalc_lcalc, 'm) gexpr ->
(('a, 'b) dcalc_lcalc, 'm mark) boxed_gexpr (('a, 'b) dcalc_lcalc, 'm) boxed_gexpr
val optimize_program : val optimize_program :
(('a, 'b) dcalc_lcalc, 'm mark) gexpr program -> (('a, 'b) dcalc_lcalc, 'm) gexpr program ->
(('a, 'b) dcalc_lcalc, 'm mark) gexpr program (('a, 'b) dcalc_lcalc, 'm) gexpr program
(** {1 Tests}*) (** {1 Tests}*)

View File

@ -56,7 +56,7 @@ val expr :
?debug:bool -> ?debug:bool ->
unit -> unit ->
Format.formatter -> Format.formatter ->
('a, 'm mark) gexpr -> ('a, 'm) gexpr ->
unit unit
(** Same as [expr], but with a debug flag that defaults to [!Cli.debug_flag]. If (** Same as [expr], but with a debug flag that defaults to [!Cli.debug_flag]. If
[~hide_function_body:true], prints "<function>" for [EAbs] nodes *) [~hide_function_body:true], prints "<function>" for [EAbs] nodes *)
@ -69,8 +69,7 @@ val scope :
?debug:bool -> ?debug:bool ->
decl_ctx -> decl_ctx ->
Format.formatter -> Format.formatter ->
ScopeName.t * ('a, 'm mark) gexpr scope_body -> ScopeName.t * ('a, 'm) gexpr scope_body ->
unit unit
val program : val program : ?debug:bool -> Format.formatter -> ('a, 'm) gexpr program -> unit
?debug:bool -> Format.formatter -> ('a, 'm mark) gexpr program -> unit

View File

@ -40,8 +40,7 @@ let get_scope_body { code_items; _ } scope =
| None -> raise Not_found | None -> raise Not_found
| Some body -> body | 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) fun prg -> Bindlib.unbox (map_exprs ~f:Expr.untype ~varf:Var.translate prg)
let rec find_scope name vars = function let rec find_scope name vars = function

View File

@ -34,7 +34,7 @@ val fold_right_exprs :
val get_scope_body : val get_scope_body :
((_ any, 't) gexpr as 'e) program -> ScopeName.t -> 'e 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 val to_expr : ((_ any, _) gexpr as 'e) program -> ScopeName.t -> 'e boxed
(** Usage: [build_whole_program_expr program main_scope] builds an expression (** Usage: [build_whole_program_expr program main_scope] builds an expression

View File

@ -168,8 +168,8 @@ let build_typ_from_sig
type 'e scope_name_or_var = ScopeName of ScopeName.t | ScopeVar of 'e Var.t 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) : let to_expr (ctx : decl_ctx) (body : 'e scope_body) (mark_scope : 'm) : 'e boxed
'e boxed = =
let var, body_expr = Bindlib.unbind body.scope_body_expr in let var, body_expr = Bindlib.unbind body.scope_body_expr in
let body_expr = unfold_body_expr ctx body_expr in let body_expr = unfold_body_expr ctx body_expr in
Expr.make_abs [| var |] body_expr Expr.make_abs [| var |] body_expr

View File

@ -107,15 +107,12 @@ val map_exprs :
(** This is the main map visitor for all the expressions inside all the scopes (** This is the main map visitor for all the expressions inside all the scopes
of the program. *) 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} *) (** {2 Conversions} *)
val to_expr : val to_expr :
decl_ctx -> decl_ctx -> ('a any, 'm) gexpr scope_body -> 'm mark -> ('a, 'm) boxed_gexpr
('a any, 'm mark) gexpr scope_body ->
'm mark ->
('a, 'm mark) boxed_gexpr
(** Usage: [to_expr ctx body scope_position] where [scope_position] corresponds (** Usage: [to_expr ctx body scope_position] where [scope_position] corresponds
to the line of the scope declaration for instance. *) 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 : val unfold :
decl_ctx -> decl_ctx ->
((_, 'm mark) gexpr as 'e) code_item_list -> ((_, 'm) gexpr as 'e) code_item_list ->
'm mark -> 'm mark ->
'e scope_name_or_var -> 'e scope_name_or_var ->
'e boxed 'e boxed

View File

@ -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]. [ECatch] cases, while [(lcalc, _) naked_gexpr] doesn't have [EDefault].
For example, Lcalc expressions are then defined as 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 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 ASTs, by having it take a [('a, _) naked_gexpr] as input, while retaining a much

View File

@ -130,13 +130,11 @@ let rec format_typ
exception Type_error of A.any_expr * unionfind_typ * unionfind_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 (** Raises an error if unification cannot be performed. The position annotation
of the second [unionfind_typ] argument is propagated (unless it is [TAny]). *) of the second [unionfind_typ] argument is propagated (unless it is [TAny]). *)
let rec unify let rec unify
(ctx : A.decl_ctx) (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) (t1 : unionfind_typ)
(t2 : unionfind_typ) : unit = (t2 : unionfind_typ) : unit =
let unify = unify ctx in let unify = unify ctx in
@ -172,14 +170,9 @@ let rec unify
(fun t1 t2 -> match Mark.remove t2 with TAny _ -> t1 | _ -> t2) (fun t1 t2 -> match Mark.remove t2 with TAny _ -> t1 | _ -> t2)
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 (* TODO: if we get weird error messages, then it means that we should use the
persistent version of the union-find data structure. *) 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 t1_repr = UnionFind.get (UnionFind.find t1) in
let t2_repr = UnionFind.get (UnionFind.find t2) in let t2_repr = UnionFind.get (UnionFind.find t2) in
let t1_pos = Mark.get t1_repr in let t1_pos = Mark.get t1_repr in
@ -204,7 +197,7 @@ let handle_type_error ctx e t1 t2 =
( Some ( Some
(Format.asprintf (Format.asprintf
"Error coming from typechecking the following expression:"), "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:" t1_s ()), t1_pos;
Some (Format.asprintf "Type %a coming from expression:" t2_s ()), t2_pos; Some (Format.asprintf "Type %a coming from expression:" t2_s ()), t2_pos;
] ]
@ -336,16 +329,18 @@ module Env = struct
end end
let add_pos e ty = Mark.add (Expr.pos e) ty 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 *) (** Infers the most permissive type from an expression *)
let rec typecheck_expr_bottom_up : let rec typecheck_expr_bottom_up :
type a m. type a m.
leave_unresolved:bool -> leave_unresolved:bool ->
A.decl_ctx -> A.decl_ctx ->
(a, m A.mark) A.gexpr Env.t -> (a, m) A.gexpr Env.t ->
(a, m A.mark) A.gexpr -> (a, m) A.gexpr ->
(a, mark) A.boxed_gexpr = (a, unionfind_typ A.custom) A.boxed_gexpr =
fun ~leave_unresolved ctx env e -> fun ~leave_unresolved ctx env e ->
typecheck_expr_top_down ~leave_unresolved ctx env typecheck_expr_top_down ~leave_unresolved ctx env
(UnionFind.make (add_pos e (TAny (Any.fresh ())))) (UnionFind.make (add_pos e (TAny (Any.fresh ()))))
@ -356,10 +351,10 @@ and typecheck_expr_top_down :
type a m. type a m.
leave_unresolved:bool -> leave_unresolved:bool ->
A.decl_ctx -> A.decl_ctx ->
(a, m A.mark) A.gexpr Env.t -> (a, m) A.gexpr Env.t ->
unionfind_typ -> unionfind_typ ->
(a, m A.mark) A.gexpr -> (a, m) A.gexpr ->
(a, mark) A.boxed_gexpr = (a, unionfind_typ A.custom) A.boxed_gexpr =
fun ~leave_unresolved ctx env tau e -> fun ~leave_unresolved ctx env tau e ->
(* Cli.debug_format "Propagating type %a for naked_expr %a" (format_typ ctx) (* Cli.debug_format "Propagating type %a for naked_expr %a" (format_typ ctx)
tau (Expr.format ctx) e; *) tau (Expr.format ctx) e; *)
@ -370,12 +365,13 @@ and typecheck_expr_top_down :
match Mark.get e with match Mark.get e with
| A.Untyped _ | A.Typed { A.ty = A.TAny, _; _ } -> () | A.Untyped _ | A.Typed { A.ty = A.TAny, _; _ } -> ()
| A.Typed { A.ty; _ } -> unify ctx e tau (ast_to_typ ty) | A.Typed { A.ty; _ } -> unify ctx e tau (ast_to_typ ty)
| A.Custom _ -> assert false
in 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 = let mark_with_tau_and_unify uf =
(* Unify with the supplied type first, and return the mark *) (* Unify with the supplied type first, and return the mark *)
unify ctx e uf tau; unify ctx e uf tau;
{ uf; pos = pos_e } A.Custom { A.custom = uf; pos = pos_e }
in in
let unionfind ?(pos = e) t = UnionFind.make (add_pos pos t) 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 let ty_mark ty = mark_with_tau_and_unify (unionfind ty) in
@ -472,7 +468,8 @@ and typecheck_expr_top_down :
let candidate_structs = let candidate_structs =
try A.IdentName.Map.find field ctx.ctx_struct_fields try A.IdentName.Map.find field ctx.ctx_struct_fields
with Not_found -> 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 \ "Field %a does not belong to structure %a (no structure defines \
it)" it)"
(Cli.format_with_style [ANSITerminal.yellow]) (Cli.format_with_style [ANSITerminal.yellow])
@ -482,7 +479,8 @@ and typecheck_expr_top_down :
in in
try A.StructName.Map.find name candidate_structs try A.StructName.Map.find name candidate_structs
with Not_found -> 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" "Field %a does not belong to structure %a, but to %a"
(Cli.format_with_style [ANSITerminal.yellow]) (Cli.format_with_style [ANSITerminal.yellow])
("\"" ^ field ^ "\"") ("\"" ^ field ^ "\"")
@ -755,7 +753,7 @@ and typecheck_expr_top_down :
unify ctx e t_ret unify ctx e t_ret
(resolve_overload_ret_type ~leave_unresolved ctx e op tys'); (resolve_overload_ret_type ~leave_unresolved ctx e op tys');
( List.map (typ_to_ast ~leave_unresolved) 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 -> ~resolved:(fun op ->
let mark = let mark =
mark_with_tau_and_unify mark_with_tau_and_unify
@ -818,7 +816,7 @@ let wrap_expr ctx f e =
(** {1 API} *) (** {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 } A.Typed { ty = typ_to_ast ~leave_unresolved uf; pos }
let expr_raw let expr_raw
@ -827,7 +825,7 @@ let expr_raw
(ctx : A.decl_ctx) (ctx : A.decl_ctx)
?(env = Env.empty ctx) ?(env = Env.empty ctx)
?(typ : A.typ option) ?(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 = let fty =
match typ with match typ with
| None -> typecheck_expr_bottom_up ~leave_unresolved ctx env | 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 = let check_expr ~leave_unresolved ctx ?env ?typ e =
Expr.map_marks Expr.map_marks
~f:(fun { pos; _ } -> A.Untyped { pos }) ~f:(fun (Custom { pos; _ }) -> A.Untyped { pos })
(expr_raw ctx ~leave_unresolved ?env ?typ e) (expr_raw ctx ~leave_unresolved ?env ?typ e)
(* Infer the type of an expression *) (* 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 ) Bindlib.box_apply (fun body -> A.ScopeDef (name, body)) body_e )
| A.Topdef (name, typ, e) -> | A.Topdef (name, typ, e) ->
let e' = expr_raw ~leave_unresolved ctx ~env ~typ e in 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 let e' = Expr.map_marks ~f:(get_ty_mark ~leave_unresolved) e' in
( Env.add var uf env, ( Env.add var uf env,
Bindlib.box_apply Bindlib.box_apply

View File

@ -40,8 +40,8 @@ val expr :
decl_ctx -> decl_ctx ->
?env:'e Env.t -> ?env:'e Env.t ->
?typ:typ -> ?typ:typ ->
(('a, 'm mark) gexpr as 'e) -> (('a, 'm) gexpr as 'e) ->
('a, typed mark) boxed_gexpr ('a, typed) boxed_gexpr
(** Infers and marks the types for the given expression. If [typ] is provided, (** 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. it is assumed to be the outer type and used for inference top-down.
@ -56,17 +56,15 @@ val check_expr :
decl_ctx -> decl_ctx ->
?env:'e Env.t -> ?env:'e Env.t ->
?typ:typ -> ?typ:typ ->
(('a, 'm mark) gexpr as 'e) -> (('a, 'm) gexpr as 'e) ->
('a, untyped mark) boxed_gexpr ('a, untyped) boxed_gexpr
(** Same as [expr], but doesn't annotate the returned expression. Equivalent to (** Same as [expr], but doesn't annotate the returned expression. Equivalent to
[Typing.expr |> Expr.untype], but more efficient. This can be useful for [Typing.expr |> Expr.untype], but more efficient. This can be useful for
type-checking and disambiguation (some AST nodes are updated with missing type-checking and disambiguation (some AST nodes are updated with missing
information, e.g. any [TAny] appearing in the AST is replaced) *) information, e.g. any [TAny] appearing in the AST is replaced) *)
val program : val program :
leave_unresolved:bool -> leave_unresolved:bool -> ('a, 'm) gexpr program -> ('a, typed) gexpr program
('a, 'm mark) gexpr program ->
('a, typed mark) gexpr program
(** Typing on whole programs (as defined in Shared_ast.program, i.e. for the (** Typing on whole programs (as defined in Shared_ast.program, i.e. for the
later dcalc/lcalc stages. later dcalc/lcalc stages.

View File

@ -54,8 +54,7 @@ let check_article_expiration
"%s %s has expired! Its expiration date is %s according to \ "%s %s has expired! Its expiration date is %s according to \
LégiFrance.%s" LégiFrance.%s"
(Mark.remove law_heading.Surface.Ast.law_heading_name) (Mark.remove law_heading.Surface.Ast.law_heading_name)
(Pos.to_string (Pos.to_string (Mark.get law_heading.Surface.Ast.law_heading_name))
(Mark.get law_heading.Surface.Ast.law_heading_name))
(Date.print_tm legifrance_expiration_date) (Date.print_tm legifrance_expiration_date)
(match new_version with (match new_version with
| None -> "" | None -> ""