1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
open Utils
module D = Dcalc.Ast
type lit =
| LBool of bool
| LInt of Runtime.integer
| LRat of Runtime.decimal
| LMoney of Runtime.money
| LUnit
| LDate of Runtime.date
| LDuration of Runtime.duration
type except = ConflictError | EmptyError | Crash
type expr =
| EVar of expr Bindlib.var Pos.marked
| ETuple of expr Pos.marked list * D.StructName.t option
(** The [MarkedString.info] is the former struct field name*)
| ETupleAccess of expr Pos.marked * int * D.StructName.t option * D.typ Pos.marked list
(** The [MarkedString.info] is the former struct field name *)
| EInj of expr Pos.marked * int * D.EnumName.t * D.typ Pos.marked list
(** The [MarkedString.info] is the former enum case name *)
| EMatch of expr Pos.marked * expr Pos.marked list * D.EnumName.t
(** The [MarkedString.info] is the former enum case name *)
| EArray of expr Pos.marked list
| ELit of lit
| EAbs of Pos.t * (expr, expr Pos.marked) Bindlib.mbinder * D.typ Pos.marked list
| EApp of expr Pos.marked * expr Pos.marked list
| EAssert of expr Pos.marked
| EOp of D.operator
| EIfThenElse of expr Pos.marked * expr Pos.marked * expr Pos.marked
| ERaise of except
| ECatch of expr Pos.marked * except * expr Pos.marked
module Var = struct
type t = expr Bindlib.var
let make (s : string Pos.marked) : t =
Bindlib.new_var
(fun (x : expr Bindlib.var) : expr -> EVar (x, Pos.get_position s))
(Pos.unmark s)
let compare x y = Bindlib.compare_vars x y
end
module VarMap = Map.Make (Var)
type vars = expr Bindlib.mvar
let make_var ((x, pos) : Var.t Pos.marked) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun x -> (x, pos)) (Bindlib.box_var x)
let make_abs (xs : vars) (e : expr Pos.marked Bindlib.box) (pos_binder : Pos.t)
(taus : D.typ Pos.marked list) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun b -> (EAbs (pos_binder, b, taus), pos)) (Bindlib.bind_mvar xs e)
let make_app (e : expr Pos.marked Bindlib.box) (u : expr Pos.marked Bindlib.box list) (pos : Pos.t)
: expr Pos.marked Bindlib.box =
Bindlib.box_apply2 (fun e u -> (EApp (e, u), pos)) e (Bindlib.box_list u)
let make_let_in (x : Var.t) (tau : D.typ Pos.marked) (e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun e u -> (EApp (e, u), Pos.get_position (Bindlib.unbox e2)))
(make_abs
(Array.of_list [ x ])
e2
(Pos.get_position (Bindlib.unbox e2))
[ tau ]
(Pos.get_position (Bindlib.unbox e2)))
(Bindlib.box_list [ e1 ])
type binder = (expr, expr Pos.marked) Bindlib.binder
type program = { decl_ctx : D.decl_ctx; scopes : (Var.t * expr Pos.marked) list }