Added boxed constructors for Dcalc

This commit is contained in:
Denis Merigoux 2022-04-06 09:35:07 +02:00
parent c4d031d7ef
commit f6047a43ea
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
2 changed files with 160 additions and 0 deletions

View File

@ -159,6 +159,93 @@ and scopes = Nil | ScopeDef of scope_def
type program = { decl_ctx : decl_ctx; scopes : scopes }
let evar (v : expr Bindlib.var) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun v' -> (v', pos)) (Bindlib.box_var v)
let etuple
(args : expr Pos.marked Bindlib.box list)
(s : StructName.t option)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun args -> (ETuple (args, s), pos))
(Bindlib.box_list args)
let etupleaccess
(e1 : expr Pos.marked Bindlib.box)
(i : int)
(s : StructName.t option)
(typs : typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (ETupleAccess (e1, i, s, typs), pos)) e1
let einj
(e1 : expr Pos.marked Bindlib.box)
(i : int)
(e_name : EnumName.t)
(typs : typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (EInj (e1, i, e_name, typs), pos)) e1
let ematch
(arg : expr Pos.marked Bindlib.box)
(arms : expr Pos.marked Bindlib.box list)
(e_name : EnumName.t)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun arg arms -> (EMatch (arg, arms, e_name), pos))
arg (Bindlib.box_list arms)
let earray (args : expr Pos.marked Bindlib.box list) (pos : Pos.t) :
expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun args -> (EArray args, pos)) (Bindlib.box_list args)
let elit (l : lit) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (ELit l, pos)
let eabs
(binder : (expr, expr Pos.marked) Bindlib.mbinder Bindlib.box)
(pos_binder : Pos.t)
(typs : typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun binder -> (EAbs ((binder, pos_binder), typs), pos))
binder
let eapp
(e1 : expr Pos.marked Bindlib.box)
(args : expr Pos.marked Bindlib.box list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun e1 args -> (EApp (e1, args), pos))
e1 (Bindlib.box_list args)
let eassert (e1 : expr Pos.marked Bindlib.box) (pos : Pos.t) :
expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (EAssert e1, pos)) e1
let eop (op : operator) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (EOp op, pos)
let edefault
(excepts : expr Pos.marked Bindlib.box list)
(just : expr Pos.marked Bindlib.box)
(cons : expr Pos.marked Bindlib.box)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply3
(fun excepts just cons -> (EDefault (excepts, just, cons), pos))
(Bindlib.box_list excepts) just cons
let eifthenelse
(e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box)
(e3 : expr Pos.marked Bindlib.box)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply3 (fun e1 e2 e3 -> (EIfThenElse (e1, e2, e3), pos)) e1 e2 e3
let eerroronempty (e1 : expr Pos.marked Bindlib.box) (pos : Pos.t) :
expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (ErrorOnEmpty e1, pos)) e1
let rec fold_scope_lets
~(f : 'a -> scope_let -> 'a)
~(init : 'a)

View File

@ -181,6 +181,79 @@ type program = { decl_ctx : decl_ctx; scopes : scopes }
(** {1 Helpers} *)
(** {2 Boxed constructors}*)
val evar : expr Bindlib.var -> Pos.t -> expr Pos.marked Bindlib.box
val etuple :
expr Pos.marked Bindlib.box list ->
StructName.t option ->
Pos.t ->
expr Pos.marked Bindlib.box
val etupleaccess :
expr Pos.marked Bindlib.box ->
int ->
StructName.t option ->
typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val einj :
expr Pos.marked Bindlib.box ->
int ->
EnumName.t ->
typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val ematch :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box list ->
EnumName.t ->
Pos.t ->
expr Pos.marked Bindlib.box
val earray :
expr Pos.marked Bindlib.box list -> Pos.t -> expr Pos.marked Bindlib.box
val elit : lit -> Pos.t -> expr Pos.marked Bindlib.box
val eabs :
(expr, expr Pos.marked) Bindlib.mbinder Bindlib.box ->
Pos.t ->
typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val eapp :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box list ->
Pos.t ->
expr Pos.marked Bindlib.box
val eassert :
expr Pos.marked Bindlib.box -> Pos.t -> expr Pos.marked Bindlib.box
val eop : operator -> Pos.t -> expr Pos.marked Bindlib.box
val edefault :
expr Pos.marked Bindlib.box list ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
Pos.t ->
expr Pos.marked Bindlib.box
val eifthenelse :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
Pos.t ->
expr Pos.marked Bindlib.box
val eerroronempty :
expr Pos.marked Bindlib.box -> Pos.t -> expr Pos.marked Bindlib.box
(**{2 Program traversal}*)
(** Be careful when using these traversal functions, as the bound variables they