CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 16:28:12 +03:00
Code Issues Projects Releases Wiki Activity

Rename marked_gexpr -> gexpr, gexpr -> naked_gexpr

Browse Source 
Since the marked kind is used throughout, this should be more clear
This commit is contained in:
Louis Gesbert 2022-08-25 16:31:32 +02:00 committed by Denis Merigoux
parent aaca280ccc
commit 8f7ba5ccaf
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
20 changed files with 169 additions and 169 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
compiler/dcalc/ast.ml
View File

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

4
compiler/dcalc/ast.mli
View File

@ -21,7 +21,7 @@ open Shared_ast
type lit = dcalc glit
type 'm expr = (dcalc, 'm mark) gexpr
and 'm marked_expr = (dcalc, 'm mark) marked_gexpr
type 'm expr = (dcalc, 'm mark) naked_gexpr
and 'm marked_expr = (dcalc, 'm mark) gexpr
type 'm program = 'm expr Shared_ast.program

10
compiler/dcalc/typing.ml
View File

@ -120,7 +120,7 @@ type mark = { pos : Pos.t; uf : unionfind_typ }
(** Raises an error if unification cannot be performed *)
let rec unify
(ctx : A.decl_ctx)
(e : ('a, 'm A.mark) A.marked_gexpr) (* used for error context *)
(e : ('a, 'm A.mark) A.gexpr) (* used for error context *)
(t1 : typ Marked.pos UnionFind.elem)
(t2 : typ Marked.pos UnionFind.elem) : unit =
let unify = unify ctx in
@ -307,11 +307,11 @@ let box_ty e = Bindlib.unbox (Bindlib.box_apply ty e)
let rec typecheck_expr_bottom_up
(ctx : A.decl_ctx)
(env : 'm Ast.expr env)
(e : 'm Ast.marked_expr) : (A.dcalc, mark) A.marked_gexpr Bindlib.box =
(e : 'm Ast.marked_expr) : (A.dcalc, mark) A.gexpr Bindlib.box =
(* Cli.debug_format "Looking for type of %a" (Expr.format ~debug:true ctx)
e; *)
let pos_e = A.Expr.pos e in
let mark (e : (A.dcalc, mark) A.gexpr) uf =
let mark (e : (A.dcalc, mark) A.naked_gexpr) uf =
Marked.mark { uf; pos = pos_e } e
in
let unionfind_make ?(pos = e) t = UnionFind.make (add_pos pos t) in
@ -471,12 +471,12 @@ and typecheck_expr_top_down
(ctx : A.decl_ctx)
(env : 'm Ast.expr env)
(tau : typ Marked.pos UnionFind.elem)
(e : 'm Ast.marked_expr) : (A.dcalc, mark) A.marked_gexpr Bindlib.box =
(e : 'm Ast.marked_expr) : (A.dcalc, mark) A.gexpr Bindlib.box =
(* Cli.debug_format "Propagating type %a for expr %a" (format_typ ctx) tau
(Expr.format ctx) e; *)
let pos_e = A.Expr.pos e in
let mark e = Marked.mark { uf = tau; pos = pos_e } e in
let unify_and_mark (e' : (A.dcalc, mark) A.gexpr) tau' =
let unify_and_mark (e' : (A.dcalc, mark) A.naked_gexpr) tau' =
(* This try...with was added because of
[tests/test_bool/bad/bad_assert.catala_en] but we shouldn't need it.
TODO: debug why it is needed here. *)

2
compiler/desugared/ast.ml
View File

@ -94,7 +94,7 @@ Set.Make (struct
let compare = Expr.compare_location
end)
type expr = (desugared, Pos.t) gexpr
type expr = (desugared, Pos.t) naked_gexpr
type marked_expr = expr Marked.pos
module ExprMap = Map.Make (struct

4
compiler/desugared/ast.mli
View File

@ -49,8 +49,8 @@ module ScopeDefSet : Set.S with type elt = ScopeDef.t
(** {2 Expressions} *)
type expr = (desugared, Pos.t) gexpr
(** See {!type:Shared_ast.gexpr} for the complete definition *)
type expr = (desugared, Pos.t) naked_gexpr
(** See {!type:Shared_ast.naked_gexpr} for the complete definition *)
and marked_expr = expr Marked.pos

4
compiler/lcalc/ast.ml
View File

@ -19,8 +19,8 @@ include Shared_ast
type lit = lcalc glit
type 'm expr = (lcalc, 'm mark) gexpr
and 'm marked_expr = (lcalc, 'm mark) marked_gexpr
type 'm expr = (lcalc, 'm mark) naked_gexpr
and 'm marked_expr = (lcalc, 'm mark) gexpr
type 'm program = 'm expr Shared_ast.program

4
compiler/lcalc/ast.mli
View File

@ -23,8 +23,8 @@ open Shared_ast
type lit = lcalc glit
type 'm expr = (lcalc, 'm mark) gexpr
and 'm marked_expr = (lcalc, 'm mark) marked_gexpr
type 'm expr = (lcalc, 'm mark) naked_gexpr
and 'm marked_expr = (lcalc, 'm mark) gexpr
type 'm program = 'm expr Shared_ast.program

2
compiler/scopelang/ast.ml
View File

@ -36,7 +36,7 @@ Set.Make (struct
let compare = Expr.compare_location
end)
type expr = (scopelang, Pos.t) gexpr
type expr = (scopelang, Pos.t) naked_gexpr
type marked_expr = expr Marked.pos
module ExprMap = Map.Make (struct

4
compiler/scopelang/ast.mli
View File

@ -41,8 +41,8 @@ module LocationSet : Set.S with type elt = location Marked.pos
(** {1 Abstract syntax tree} *)
type expr = (scopelang, Pos.t) gexpr
type marked_expr = (scopelang, Pos.t) marked_gexpr
type expr = (scopelang, Pos.t) naked_gexpr
type marked_expr = (scopelang, Pos.t) gexpr
module ExprMap : Map.S with type key = marked_expr

116
compiler/shared_ast/definitions.ml
View File

@ -174,90 +174,90 @@ type 'a glocation =
ScopeName.t * SubScopeName.t Marked.pos * ScopeVar.t Marked.pos
-> [< desugared | scopelang ] glocation
type ('a, 't) marked_gexpr = (('a, 't) gexpr, 't) Marked.t
type ('a, 't) gexpr = (('a, 't) naked_gexpr, 't) Marked.t
(** 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 example,
are then defined with [type expr = dcalc gexpr] plus the annotations.
are then defined with [type expr = dcalc naked_gexpr] plus the annotations.
A few tips on using this GADT:
- To write a function that handles cases from different ASTs, explicit the
type variables: [fun (type a) (x: a gexpr) -> ...]
type variables: [fun (type a) (x: a naked_gexpr) -> ...]
- For recursive functions, you may need to additionally explicit the
generalisation of the variable: [let rec f: type a . a gexpr -> ...] *)
generalisation of the variable: [let rec f: type a . a naked_gexpr -> ...] *)
(** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib}
library, based on higher-order abstract syntax *)
and ('a, 't) gexpr =
and ('a, 't) naked_gexpr =
(* Constructors common to all ASTs *)
| ELit : 'a glit -> ('a any, 't) gexpr
| ELit : 'a glit -> ('a any, 't) naked_gexpr
| EApp :
('a, 't) marked_gexpr * ('a, 't) marked_gexpr list
-> ('a any, 't) gexpr
| EOp : operator -> ('a any, 't) gexpr
| EArray : ('a, 't) marked_gexpr list -> ('a any, 't) gexpr
('a, 't) gexpr * ('a, 't) gexpr list
-> ('a any, 't) naked_gexpr
| EOp : operator -> ('a any, 't) naked_gexpr
| EArray : ('a, 't) gexpr list -> ('a any, 't) naked_gexpr
(* All but statement calculus *)
| EVar :
('a, 't) gexpr Bindlib.var
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) gexpr
('a, 't) naked_gexpr Bindlib.var
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) naked_gexpr
| EAbs :
(('a, 't) gexpr, ('a, 't) marked_gexpr) Bindlib.mbinder * marked_typ list
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) gexpr
(('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder * marked_typ list
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) naked_gexpr
| EIfThenElse :
('a, 't) marked_gexpr * ('a, 't) marked_gexpr * ('a, 't) marked_gexpr
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) gexpr
('a, 't) gexpr * ('a, 't) gexpr * ('a, 't) gexpr
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) naked_gexpr
(* Early stages *)
| ELocation : 'a glocation -> (([< desugared | scopelang ] as 'a), 't) gexpr
| ELocation : 'a glocation -> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
| EStruct :
StructName.t * ('a, 't) marked_gexpr StructFieldMap.t
-> (([< desugared | scopelang ] as 'a), 't) gexpr
StructName.t * ('a, 't) gexpr StructFieldMap.t
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
| EStructAccess :
('a, 't) marked_gexpr * StructFieldName.t * StructName.t
-> (([< desugared | scopelang ] as 'a), 't) gexpr
('a, 't) gexpr * StructFieldName.t * StructName.t
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
| EEnumInj :
('a, 't) marked_gexpr * EnumConstructor.t * EnumName.t
-> (([< desugared | scopelang ] as 'a), 't) gexpr
('a, 't) gexpr * EnumConstructor.t * EnumName.t
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
| EMatchS :
('a, 't) marked_gexpr
('a, 't) gexpr
* EnumName.t
* ('a, 't) marked_gexpr EnumConstructorMap.t
-> (([< desugared | scopelang ] as 'a), 't) gexpr
* ('a, 't) gexpr EnumConstructorMap.t
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
(* Lambda-like *)
| ETuple :
('a, 't) marked_gexpr list * StructName.t option
-> (([< dcalc | lcalc ] as 'a), 't) gexpr
('a, 't) gexpr list * StructName.t option
-> (([< dcalc | lcalc ] as 'a), 't) naked_gexpr
| ETupleAccess :
('a, 't) marked_gexpr * int * StructName.t option * marked_typ list
-> (([< dcalc | lcalc ] as 'a), 't) gexpr
('a, 't) gexpr * int * StructName.t option * marked_typ list
-> (([< dcalc | lcalc ] as 'a), 't) naked_gexpr
| EInj :
('a, 't) marked_gexpr * int * EnumName.t * marked_typ list
-> (([< dcalc | lcalc ] as 'a), 't) gexpr
('a, 't) gexpr * int * EnumName.t * marked_typ list
-> (([< dcalc | lcalc ] as 'a), 't) naked_gexpr
| EMatch :
('a, 't) marked_gexpr * ('a, 't) marked_gexpr list * EnumName.t
-> (([< dcalc | lcalc ] as 'a), 't) gexpr
| EAssert : ('a, 't) marked_gexpr -> (([< dcalc | lcalc ] as 'a), 't) gexpr
('a, 't) gexpr * ('a, 't) gexpr list * EnumName.t
-> (([< dcalc | lcalc ] as 'a), 't) naked_gexpr
| EAssert : ('a, 't) gexpr -> (([< dcalc | lcalc ] as 'a), 't) naked_gexpr
(* Default terms *)
| EDefault :
('a, 't) marked_gexpr list * ('a, 't) marked_gexpr * ('a, 't) marked_gexpr
-> (([< desugared | scopelang | dcalc ] as 'a), 't) gexpr
('a, 't) gexpr list * ('a, 't) gexpr * ('a, 't) gexpr
-> (([< desugared | scopelang | dcalc ] as 'a), 't) naked_gexpr
| ErrorOnEmpty :
('a, 't) marked_gexpr
-> (([< desugared | scopelang | dcalc ] as 'a), 't) gexpr
('a, 't) gexpr
-> (([< desugared | scopelang | dcalc ] as 'a), 't) naked_gexpr
(* Lambda calculus with exceptions *)
| ERaise : except -> ((lcalc as 'a), 't) gexpr
| ERaise : except -> ((lcalc as 'a), 't) naked_gexpr
| ECatch :
('a, 't) marked_gexpr * except * ('a, 't) marked_gexpr
-> ((lcalc as 'a), 't) gexpr
('a, 't) gexpr * except * ('a, 't) gexpr
-> ((lcalc as 'a), 't) naked_gexpr
(* (\* Statement calculus *\)
* | ESVar: LocalName.t -> (scalc as 'a, 't) gexpr
* | ESStruct: ('a, 't) marked_gexpr list * StructName.t -> (scalc as 'a, 't) gexpr
* | ESStructFieldAccess: ('a, 't) marked_gexpr * StructFieldName.t * StructName.t -> (scalc as 'a, 't) gexpr
* | ESInj: ('a, 't) marked_gexpr * EnumConstructor.t * EnumName.t -> (scalc as 'a, 't) gexpr
* | ESFunc: TopLevelName.t -> (scalc as 'a, 't) gexpr *)
* | ESVar: LocalName.t -> (scalc as 'a, 't) naked_gexpr
* | ESStruct: ('a, 't) gexpr list * StructName.t -> (scalc as 'a, 't) naked_gexpr
* | ESStructFieldAccess: ('a, 't) gexpr * StructFieldName.t * StructName.t -> (scalc as 'a, 't) naked_gexpr
* | ESInj: ('a, 't) gexpr * EnumConstructor.t * EnumName.t -> (scalc as 'a, 't) naked_gexpr
* | ESFunc: TopLevelName.t -> (scalc as 'a, 't) naked_gexpr *)
type 'e anyexpr = 'e constraint 'e = (_ any, _) gexpr
type 'e anyexpr = 'e constraint 'e = (_ any, _) naked_gexpr
(** Shorter alias for functions taking any kind of expression *)
(** {2 Markings} *)
@ -267,25 +267,25 @@ type typed = { pos : Pos.t; ty : marked_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
[marked_gexpr] (a ['t] annotation different from this type is used in the
appropriate. Expected to fill the ['t] parameter of [naked_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
type 'e marked = ('e, 'm mark) Marked.t constraint 'e = ('a, 'm mark) gexpr
(** [('a, 't) gexpr marked] is equivalent to [('a, 'm mark) marked_gexpr] but
type 'e marked = ('e, 'm mark) Marked.t constraint 'e = ('a, 'm mark) naked_gexpr
(** [('a, 't) naked_gexpr marked] is equivalent to [('a, 'm mark) gexpr] but
often more convenient to write since we generally use the type of
expressions ['e = (_, _ mark) gexpr] as type parameter. *)
expressions ['e = (_, _ mark) naked_gexpr] as type parameter. *)
(** Useful for errors and printing, for example *)
type any_marked_expr =
| AnyExpr : (_ any, _ mark) marked_gexpr -> any_marked_expr
| AnyExpr : (_ any, _ mark) gexpr -> any_marked_expr
(** {2 Higher-level program structure} *)
(** Constructs scopes and programs on top of expressions. The ['e] type
parameter throughout is expected to match instances of the [gexpr] type
parameter throughout is expected to match instances of the [naked_gexpr] type
defined above. Markings are constrained to the [mark] GADT defined above.
Note that this structure is at the moment only relevant for [dcalc] and
[lcalc], as [scopelang] has its own scope structure, as the name implies. *)
@ -310,7 +310,7 @@ type 'e scope_let = {
scope_let_next : ('e, 'e scope_body_expr) Bindlib.binder;
scope_let_pos : Pos.t;
}
constraint 'e = ('a, 'm mark) gexpr
constraint 'e = ('a, 'm mark) naked_gexpr
(** This type is parametrized by the expression type so it can be reused in
later intermediate representations. *)
@ -320,7 +320,7 @@ type 'e scope_let = {
and 'e scope_body_expr =
| Result of 'e marked
| ScopeLet of 'e scope_let
constraint 'e = ('a, 'm mark) gexpr
constraint 'e = ('a, 'm mark) naked_gexpr
type 'e scope_body = {
scope_body_input_struct : StructName.t;
@ -343,7 +343,7 @@ type 'e scope_def = {
and 'e scopes =
| Nil
| ScopeDef of 'e scope_def
constraint 'e = ('a, 'm mark) gexpr
constraint 'e = ('a, 'm mark) naked_gexpr
type struct_ctx = (StructFieldName.t * marked_typ) list StructMap.t
type enum_ctx = (EnumConstructor.t * marked_typ) list EnumMap.t

16
compiler/shared_ast/expr.ml
View File

@ -147,8 +147,8 @@ let fold_marks
let map
(type a)
(ctx : 'ctx)
~(f : 'ctx -> (a, 'm1) marked_gexpr -> (a, 'm2) marked_gexpr Bindlib.box)
(e : ((a, 'm1) gexpr, 'm2) Marked.t) : (a, 'm2) marked_gexpr Bindlib.box =
~(f : 'ctx -> (a, 'm1) gexpr -> (a, 'm2) gexpr Bindlib.box)
(e : ((a, 'm1) naked_gexpr, 'm2) Marked.t) : (a, 'm2) gexpr Bindlib.box =
let m = Marked.get_mark e in
match Marked.unmark e with
| ELit l -> elit l m
@ -281,7 +281,7 @@ let make_default exceptions just cons mark =
(* Tests *)
let is_value (type a) (e : (a, 'm mark) gexpr marked) =
let is_value (type a) (e : (a, 'm mark) naked_gexpr marked) =
match Marked.unmark e with
| ELit _ | EAbs _ | EOp _ | ERaise _ -> true
| _ -> false
@ -531,11 +531,11 @@ let compare_except ex1 ex2 = Stdlib.compare ex1 ex2
(* weird indentation; see
https://github.com/ocaml-ppx/ocamlformat/issues/2143 *)
let rec equal_list :
'a. ('a, 't) marked_gexpr list -> ('a, 't) marked_gexpr list -> bool =
'a. ('a, 't) gexpr list -> ('a, 't) gexpr list -> bool =
fun es1 es2 ->
try List.for_all2 equal es1 es2 with Invalid_argument _ -> false
and equal : type a. (a, 't) marked_gexpr -> (a, 't) marked_gexpr -> bool =
and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
fun e1 e2 ->
match Marked.unmark e1, Marked.unmark e2 with
| EVar v1, EVar v2 -> Bindlib.eq_vars v1 v2
@ -584,7 +584,7 @@ and equal : type a. (a, 't) marked_gexpr -> (a, 't) marked_gexpr -> bool =
_ ) ->
false
let rec compare : type a. (a, _) marked_gexpr -> (a, _) marked_gexpr -> int =
let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
fun e1 e2 ->
(* Infix operator to chain comparisons lexicographically. *)
let ( @@< ) cmp1 cmpf = match cmp1 with 0 -> cmpf () | n -> n in
@ -681,7 +681,7 @@ let rec compare : type a. (a, _) marked_gexpr -> (a, _) marked_gexpr -> int =
| ERaise _, _ -> -1 | _, ERaise _ -> 1
| ECatch _, _ -> . | _, ECatch _ -> .
let rec free_vars : type a. (a, 't) gexpr marked -> (a, 't) gexpr Var.Set.t =
let rec free_vars : type a. (a, 't) naked_gexpr marked -> (a, 't) naked_gexpr Var.Set.t =
fun e ->
match Marked.unmark e with
| EOp _ | ELit _ | ERaise _ -> Var.Set.empty
@ -731,7 +731,7 @@ let remove_logging_calls e =
let format ?debug decl_ctx ppf e = Print.expr ?debug decl_ctx ppf e
let rec size : type a. (a, 't) gexpr marked -> int =
let rec size : type a. (a, 't) naked_gexpr marked -> int =
fun e ->
match Marked.unmark e with
| EVar _ | ELit _ | EOp _ -> 1

126
compiler/shared_ast/expr.mli
View File

@ -22,97 +22,97 @@ open Definitions
(** {2 Boxed constructors} *)
val box : ('a, 't) marked_gexpr -> ('a, 't) marked_gexpr Bindlib.box
val evar : ('a, 't) gexpr Bindlib.var -> 't -> ('a, 't) marked_gexpr Bindlib.box
val box : ('a, 't) gexpr -> ('a, 't) gexpr Bindlib.box
val evar : ('a, 't) naked_gexpr Bindlib.var -> 't -> ('a, 't) gexpr Bindlib.box
val etuple :
(([< dcalc | lcalc ] as 'a), 't) marked_gexpr Bindlib.box list ->
(([< dcalc | lcalc ] as 'a), 't) gexpr Bindlib.box list ->
StructName.t option ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val etupleaccess :
(([< dcalc | lcalc ] as 'a), 't) marked_gexpr Bindlib.box ->
(([< dcalc | lcalc ] as 'a), 't) gexpr Bindlib.box ->
int ->
StructName.t option ->
marked_typ list ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val einj :
(([< dcalc | lcalc ] as 'a), 't) marked_gexpr Bindlib.box ->
(([< dcalc | lcalc ] as 'a), 't) gexpr Bindlib.box ->
int ->
EnumName.t ->
marked_typ list ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val ematch :
(([< dcalc | lcalc ] as 'a), 't) marked_gexpr Bindlib.box ->
('a, 't) marked_gexpr Bindlib.box list ->
(([< dcalc | lcalc ] as 'a), 't) gexpr Bindlib.box ->
('a, 't) gexpr Bindlib.box list ->
EnumName.t ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val earray :
('a any, 't) marked_gexpr Bindlib.box list ->
('a any, 't) gexpr Bindlib.box list ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val elit : 'a any glit -> 't -> ('a, 't) marked_gexpr Bindlib.box
val elit : 'a any glit -> 't -> ('a, 't) gexpr Bindlib.box
val eabs :
(('a any, 't) gexpr, ('a, 't) marked_gexpr) Bindlib.mbinder Bindlib.box ->
(('a any, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder Bindlib.box ->
marked_typ list ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val eapp :
('a any, 't) marked_gexpr Bindlib.box ->
('a, 't) marked_gexpr Bindlib.box list ->
('a any, 't) gexpr Bindlib.box ->
('a, 't) gexpr Bindlib.box list ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val eassert :
(([< dcalc | lcalc ] as 'a), 't) marked_gexpr Bindlib.box ->
(([< dcalc | lcalc ] as 'a), 't) gexpr Bindlib.box ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val eop : operator -> 't -> (_ any, 't) marked_gexpr Bindlib.box
val eop : operator -> 't -> (_ any, 't) gexpr Bindlib.box
val edefault :
(([< desugared | scopelang | dcalc ] as 'a), 't) marked_gexpr Bindlib.box list ->
('a, 't) marked_gexpr Bindlib.box ->
('a, 't) marked_gexpr Bindlib.box ->
(([< desugared | scopelang | dcalc ] as 'a), 't) gexpr Bindlib.box list ->
('a, 't) gexpr Bindlib.box ->
('a, 't) gexpr Bindlib.box ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val eifthenelse :
('a any, 't) marked_gexpr Bindlib.box ->
('a, 't) marked_gexpr Bindlib.box ->
('a, 't) marked_gexpr Bindlib.box ->
('a any, 't) gexpr Bindlib.box ->
('a, 't) gexpr Bindlib.box ->
('a, 't) gexpr Bindlib.box ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val eerroronempty :
(([< desugared | scopelang | dcalc ] as 'a), 't) marked_gexpr Bindlib.box ->
(([< desugared | scopelang | dcalc ] as 'a), 't) gexpr Bindlib.box ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val ecatch :
(lcalc, 't) marked_gexpr Bindlib.box ->
(lcalc, 't) gexpr Bindlib.box ->
except ->
(lcalc, 't) marked_gexpr Bindlib.box ->
(lcalc, 't) gexpr Bindlib.box ->
't ->
(lcalc, 't) marked_gexpr Bindlib.box
(lcalc, 't) gexpr Bindlib.box
val eraise : except -> 't -> (lcalc, 't) marked_gexpr Bindlib.box
val eraise : except -> 't -> (lcalc, 't) gexpr Bindlib.box
(** Manipulation of marks *)
val no_mark : 'm mark -> 'm mark
val mark_pos : 'm mark -> Pos.t
val pos : ('e, _) gexpr marked -> Pos.t
val pos : ('e, _) naked_gexpr marked -> Pos.t
val ty : (_, typed mark) Marked.t -> marked_typ
val with_ty : marked_typ -> ('a, _ mark) Marked.t -> ('a, typed mark) Marked.t
@ -130,15 +130,15 @@ val fold_marks :
(Pos.t list -> Pos.t) -> (typed list -> marked_typ) -> 'm mark list -> 'm mark
val untype :
('a, 'm mark) marked_gexpr -> ('a, untyped mark) marked_gexpr Bindlib.box
('a, 'm mark) gexpr -> ('a, untyped mark) gexpr Bindlib.box
(** {2 Traversal functions} *)
val map :
'ctx ->
f:('ctx -> ('a, 't1) marked_gexpr -> ('a, 't2) marked_gexpr Bindlib.box) ->
(('a, 't1) gexpr, 't2) Marked.t ->
('a, 't2) marked_gexpr Bindlib.box
f:('ctx -> ('a, 't1) gexpr -> ('a, 't2) gexpr Bindlib.box) ->
(('a, 't1) naked_gexpr, 't2) Marked.t ->
('a, 't2) gexpr Bindlib.box
(** Flat (non-recursive) mapping on expressions.
If you want to apply a map transform to an expression, you can save up
@ -159,35 +159,35 @@ val map :
around during your map traversal. *)
val map_top_down :
f:(('a, 't1) marked_gexpr -> (('a, 't1) gexpr, 't2) Marked.t) ->
('a, 't1) marked_gexpr ->
('a, 't2) marked_gexpr Bindlib.box
f:(('a, 't1) gexpr -> (('a, 't1) naked_gexpr, 't2) Marked.t) ->
('a, 't1) gexpr ->
('a, 't2) gexpr Bindlib.box
(** 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) marked_gexpr -> ('a, 't2) marked_gexpr Bindlib.box
f:('t1 -> 't2) -> ('a, 't1) gexpr -> ('a, 't2) gexpr Bindlib.box
(** {2 Expression building helpers} *)
val make_var : 'a Bindlib.var * 'b -> ('a * 'b) Bindlib.box
val make_abs :
('a, 't) gexpr Var.vars ->
('a, 't) marked_gexpr Bindlib.box ->
('a, 't) naked_gexpr Var.vars ->
('a, 't) gexpr Bindlib.box ->
typ Marked.pos list ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
val make_app :
((_ any, 'm mark) gexpr as 'e) marked Bindlib.box ->
((_ any, 'm mark) naked_gexpr as 'e) marked Bindlib.box ->
'e marked Bindlib.box list ->
'm mark ->
'e marked Bindlib.box
val empty_thunked_term :
'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) gexpr marked
'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) naked_gexpr marked
val make_let_in :
'e Bindlib.var ->
@ -198,12 +198,12 @@ val make_let_in :
'e marked Bindlib.box
val make_let_in_raw :
('a any, 't) gexpr Bindlib.var ->
('a any, 't) naked_gexpr Bindlib.var ->
marked_typ ->
('a, 't) marked_gexpr Bindlib.box ->
('a, 't) marked_gexpr Bindlib.box ->
('a, 't) gexpr Bindlib.box ->
('a, 't) gexpr Bindlib.box ->
't ->
('a, 't) marked_gexpr Bindlib.box
('a, 't) gexpr Bindlib.box
(** Version with any mark; to be removed once we use the [mark] type everywhere. *)
val make_multiple_let_in :
@ -215,11 +215,11 @@ val make_multiple_let_in :
'e marked Bindlib.box
val make_default :
(([< desugared | scopelang | dcalc ] as 'a), 't) marked_gexpr list ->
('a, 't) marked_gexpr ->
('a, 't) marked_gexpr ->
(([< desugared | scopelang | dcalc ] as 'a), 't) gexpr list ->
('a, 't) gexpr ->
('a, 't) gexpr ->
't ->
('a, 't) marked_gexpr
('a, 't) gexpr
(** [make_default ?pos exceptions just cons] builds a term semantically
equivalent to [<exceptions | just :- cons>] (the [EDefault] constructor)
while avoiding redundant nested constructions. The position is extracted
@ -236,7 +236,7 @@ val make_default :
(** {2 Transformations} *)
val remove_logging_calls :
((_ any, 't) gexpr as 'e) marked -> 'e marked Bindlib.box
((_ any, 't) naked_gexpr as 'e) marked -> 'e marked Bindlib.box
(** Removes all calls to [Log] unary operators in the AST, replacing them by
their argument. *)
@ -254,16 +254,16 @@ val compare_lit : 'a glit -> 'a glit -> int
val equal_location : 'a glocation Marked.pos -> 'a glocation Marked.pos -> bool
val compare_location : 'a glocation Marked.pos -> 'a glocation Marked.pos -> int
val equal : ('a, 't) marked_gexpr -> ('a, 't) marked_gexpr -> bool
val equal : ('a, 't) gexpr -> ('a, 't) gexpr -> bool
(** Determines if two expressions are equal, omitting their position information *)
val compare : ('a, 't) marked_gexpr -> ('a, 't) marked_gexpr -> int
val compare : ('a, 't) gexpr -> ('a, 't) gexpr -> int
(** Standard comparison function, suitable for e.g. [Set.Make]. Ignores position
information *)
val compare_typ : marked_typ -> marked_typ -> int
val is_value : (_ any, 'm mark) gexpr marked -> bool
val is_value : (_ any, 'm mark) naked_gexpr marked -> bool
val free_vars : 'e marked -> 'e Var.Set.t
val size : (_ any, 't) gexpr marked -> int
val size : (_ any, 't) naked_gexpr marked -> int
(** Used by the optimizer to know when to stop *)

6
compiler/shared_ast/print.ml
View File

@ -208,7 +208,7 @@ let except (fmt : Format.formatter) (exn : except) : unit =
let var fmt v =
Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
let needs_parens (type a) (e : (a, _) marked_gexpr) : bool =
let needs_parens (type a) (e : (a, _) gexpr) : bool =
match Marked.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false
let rec expr :
@ -216,10 +216,10 @@ let rec expr :
?debug:bool ->
decl_ctx ->
Format.formatter ->
('a, 't) marked_gexpr ->
('a, 't) gexpr ->
unit =
fun (type a) ?(debug : bool = false) (ctx : decl_ctx) (fmt : Format.formatter)
(e : (a, 't) marked_gexpr) ->
(e : (a, 't) gexpr) ->
let expr e = expr ~debug ctx e in
let with_parens fmt e =
if needs_parens e then (

2
compiler/shared_ast/print.mli
View File

@ -47,5 +47,5 @@ val expr :
?debug:bool (** [true] for debug printing *) ->
decl_ctx ->
Format.formatter ->
('a, 't) marked_gexpr ->
('a, 't) gexpr ->
unit

4
compiler/shared_ast/program.ml
View File

@ -22,9 +22,9 @@ let map_exprs ~f ~varf { scopes; decl_ctx } =
(fun scopes -> { scopes; decl_ctx })
(Scope.map_exprs ~f ~varf scopes)
let untype : 'm. ('a, 'm mark) gexpr program -> ('a, untyped mark) gexpr program
let untype : 'm. ('a, 'm mark) naked_gexpr program -> ('a, untyped mark) naked_gexpr program
=
fun (prg : ('a, 'm mark) gexpr program) ->
fun (prg : ('a, 'm mark) naked_gexpr program) ->
Bindlib.unbox (map_exprs ~f:Expr.untype ~varf:Var.translate prg)
let rec find_scope name vars = function

6
compiler/shared_ast/program.mli
View File

@ -26,11 +26,11 @@ val map_exprs :
'expr2 program Bindlib.box
val untype :
(([< dcalc | lcalc ] as 'a), 'm mark) gexpr program ->
('a, untyped mark) gexpr program
(([< dcalc | lcalc ] as 'a), 'm mark) naked_gexpr program ->
('a, untyped mark) naked_gexpr program
val to_expr :
(([< dcalc | lcalc ], _) gexpr as 'e) program ->
(([< dcalc | lcalc ], _) naked_gexpr as 'e) program ->
ScopeName.t ->
'e marked Bindlib.box
(** Usage: [build_whole_program_expr program main_scope] builds an expression

6
compiler/shared_ast/scope.mli
View File

@ -80,7 +80,7 @@ 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 mark) naked_gexpr scope_body -> 'm mark
(** {2 Conversions} *)
@ -93,7 +93,7 @@ val format :
val to_expr :
decl_ctx ->
((_ any, 'm mark) gexpr as 'e) scope_body ->
((_ any, 'm mark) naked_gexpr as 'e) scope_body ->
'm mark ->
'e marked Bindlib.box
(** Usage: [to_expr ctx body scope_position] where [scope_position] corresponds
@ -105,7 +105,7 @@ type 'e scope_name_or_var =
val unfold :
decl_ctx ->
((_ any, 'm mark) gexpr as 'e) scopes ->
((_ any, 'm mark) naked_gexpr as 'e) scopes ->
'm mark ->
'e scope_name_or_var ->
'e marked Bindlib.box

12
compiler/shared_ast/shared_ast.mld
View File

@ -8,19 +8,19 @@ helpers that are reused in various passes of the compiler.
The main module {!modules: Shared_ast.Definitions} is exposed at top-level of
the library (so that [open Shared_ast] gives access to the structures). It
defines literals, operators, and in particular the type {!types:
Shared_ast.gexpr}.
Shared_ast.naked_gexpr}.
The {!types: Shared_ast.gexpr} type regroups all the cases for the {{:
The {!types: Shared_ast.naked_gexpr} type regroups all the cases for the {{:
../dcalc.html} Dcalc} and {{: ../lcalc.html} Lcalc} ASTs, with unconstrained
annotations (used for positions, types, etc.). A GADT is used to eliminate
irrelevant cases, so that e.g. [(dcalc, _) gexpr] doesn't have the [ERaise] and
[ECatch] cases, while [(lcalc, _) gexpr] doesn't have [EDefault].
irrelevant cases, so that e.g. [(dcalc, _) naked_gexpr] doesn't have the [ERaise] and
[ECatch] cases, while [(lcalc, _) naked_gexpr] doesn't have [EDefault].
For example, Lcalc expressions are then defined as
[type 'm expr = (Shared_ast.lcalc, 'm mark) Shared_ast.gexpr].
[type 'm expr = (Shared_ast.lcalc, 'm mark) 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, _) gexpr] as input, while retaining a much
ASTs, by having it take a [('a, _) naked_gexpr] as input, while retaining a much
stricter policy than polymorphic variants.
The module additionally defines the encompassing [scope] and [program]

4
compiler/shared_ast/var.ml
View File

@ -18,7 +18,7 @@ open Definitions
(** {1 Variables and their collections} *)
(** This module provides types and helpers for Bindlib variables on the [gexpr]
(** This module provides types and helpers for Bindlib variables on the [naked_gexpr]
type *)
type 'e t = 'e anyexpr Bindlib.var
@ -36,7 +36,7 @@ type 'e var = 'e t
(* The purpose of this module is just to lift a type parameter outside of
[Set.S] and [Map.S], so that we can have ['e Var.Set.t] for sets of variables
bound to the ['e = ('a, 't) gexpr] expression type. This is made possible by
bound to the ['e = ('a, 't) naked_gexpr] expression type. This is made possible by
the fact that [Bindlib.compare_vars] is polymorphic in that parameter; we
first hide that parameter inside an existential, then re-add a phantom type
outside of the set to ensure consistency. Extracting the elements is then

2
compiler/shared_ast/var.mli
View File

@ -18,7 +18,7 @@ open Definitions
(** {1 Variables and their collections} *)
(** This module provides types and helpers for Bindlib variables on the [gexpr]
(** This module provides types and helpers for Bindlib variables on the [naked_gexpr]
type *)
type 'e t = 'e anyexpr Bindlib.var