-
Notifications
You must be signed in to change notification settings - Fork 5
/
Core.ml
235 lines (197 loc) · 7.5 KB
/
Core.ml
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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
(** {0 Core language} *)
(** {1 Names} *)
(** These names are used as hints for pretty printing binders and variables,
but don’t impact the equality of terms. *)
type name = string
(** {1 Nameless binding structure} *)
(** The binding structure of terms is represented in the core language by
using numbers that represent the distance to a binder, instead of by the
names attached to those binders. *)
(** {i De Bruijn index} that represents a variable occurance by the number of
binders between the occurance and the binder it refers to. *)
type index = int
(** {i De Bruijn level} that represents a variable occurance by the number of
binders from the top of the environment to the binder that the ocurrance
refers to. These do not change their meaning as new bindings are added to
the environment. *)
type level = int
(** Converts a {!level} to an {!index} that is bound in an environment of the
supplied size. Assumes that [ size > level ]. *)
let level_to_index size level =
size - level - 1
(** An environment of bindings that can be looked up directly using a
{!index}, or by inverting a {!level} using {!level_to_index}. *)
type 'a env = 'a list
(** {1 Syntax} *)
(** Type syntax *)
type ty =
| FunType of ty * ty
| IntType
| BoolType
(** Term syntax *)
type tm =
| Var of index
| Let of name * ty * tm * tm
| FunLit of name * ty * tm
| FunApp of tm * tm
| IntLit of int
| BoolLit of bool
| BoolElim of tm * tm * tm
| PrimApp of Prim.t * tm list
module Semantics = struct
(** {1 Values} *)
type vtm =
| Neu of ntm
| FunLit of name * ty * (vtm -> vtm)
| IntLit of int
| BoolLit of bool
and ntm =
| Var of level
| FunApp of ntm * vtm
| BoolElim of ntm * vtm Lazy.t * vtm Lazy.t
| PrimApp of Prim.t * vtm list
(** {1 Eliminators} *)
let fun_app (head : vtm) (arg : vtm) : vtm =
match head with
| Neu ntm -> Neu (FunApp (ntm, arg))
| FunLit (_, _, body) -> body arg
| _ -> invalid_arg "expected function"
let bool_elim (head : vtm) (vtm0 : vtm Lazy.t) (vtm1 : vtm Lazy.t) : vtm =
match head with
| Neu ntm -> Neu (BoolElim (ntm, vtm0, vtm1))
| BoolLit true -> Lazy.force vtm0
| BoolLit false -> Lazy.force vtm1
| _ -> invalid_arg "expected boolean"
let prim_app (prim : Prim.t) : vtm list -> vtm =
let guard f args =
try f args with
| Match_failure _ -> Neu (PrimApp (prim, args))
in
match prim with
| BoolEq -> guard @@ fun[@warning "-partial-match"] [BoolLit t1; BoolLit t2] -> BoolLit (t1 = t2)
| IntEq -> guard @@ fun[@warning "-partial-match"] [IntLit t1; IntLit t2] -> BoolLit (t1 = t2)
| IntAdd -> guard @@ fun[@warning "-partial-match"] [IntLit t1; IntLit t2] -> IntLit (t1 + t2)
| IntSub -> guard @@ fun[@warning "-partial-match"] [IntLit t1; IntLit t2] -> IntLit (t1 - t2)
| IntMul -> guard @@ fun[@warning "-partial-match"] [IntLit t1; IntLit t2] -> IntLit (t1 * t2)
| IntNeg -> guard @@ fun[@warning "-partial-match"] [IntLit t1] -> IntLit (-t1)
(** {1 Evaluation} *)
(** Evaluate a term from the syntax into its semantic interpretation *)
let rec eval (env : vtm env) (tm : tm) : vtm =
match tm with
| Var index -> List.nth env index
| Let (_, _, def, body) ->
let def = eval env def in
eval (def :: env) body
| FunLit (name, param_ty, body) ->
FunLit (name, param_ty, fun arg -> eval (arg :: env) body)
| FunApp (head, arg) ->
let head = eval env head in
let arg = eval env arg in
fun_app head arg
| IntLit i -> IntLit i
| BoolLit b -> BoolLit b
| BoolElim (head, tm0, tm1) ->
let head = eval env head in
let vtm0 = Lazy.from_fun (fun () -> eval env tm0) in
let vtm1 = Lazy.from_fun (fun () -> eval env tm1) in
bool_elim head vtm0 vtm1
| PrimApp (prim, args) ->
prim_app prim (List.map (eval env) args)
(** {1 Quotation} *)
(** Convert terms from the semantic domain back into syntax. *)
let rec quote (size : int) (vtm : vtm) : tm =
match vtm with
| Neu ntm -> quote_neu size ntm
| FunLit (name, param_ty, body) ->
let body = quote (size + 1) (body (Neu (Var size))) in
FunLit (name, param_ty, body)
| IntLit i -> IntLit i
| BoolLit b -> BoolLit b
and quote_neu (size : int) (ntm : ntm) : tm =
match ntm with
| Var level ->
Var (level_to_index size level)
| FunApp (head, arg) ->
FunApp (quote_neu size head, quote size arg)
| BoolElim (head, vtm0, vtm1) ->
let tm0 = quote size (Lazy.force vtm0) in
let tm1 = quote size (Lazy.force vtm1) in
BoolElim (quote_neu size head, tm0, tm1)
| PrimApp (prim, args) ->
PrimApp (prim, List.map (quote size) args)
(** {1 Normalisation} *)
(** By evaluating a term then quoting the result, we can produce a term that
is reduced as much as possible in the current environment. *)
let normalise (env : vtm list) (tm : tm) : tm =
quote (List.length env) (eval env tm)
end
(** {1 Pretty printing} *)
let rec pp_ty (fmt : Format.formatter) (ty : ty) : unit =
match ty with
| FunType (param_ty, body_ty) ->
Format.fprintf fmt "%a -> %a"
pp_atomic_ty param_ty
pp_ty body_ty
| ty ->
pp_atomic_ty fmt ty
and pp_atomic_ty fmt ty =
match ty with
| IntType -> Format.fprintf fmt "Int"
| BoolType -> Format.fprintf fmt "Bool"
| ty -> Format.fprintf fmt "@[(%a)@]" pp_ty ty
let pp_name_ann fmt (name, ty) =
Format.fprintf fmt "@[<2>@[%s :@]@ %a@]" name pp_ty ty
let pp_param fmt (name, ty) =
Format.fprintf fmt "@[<2>(@[%s :@]@ %a)@]" name pp_ty ty
let rec pp_tm (names : name env) (fmt : Format.formatter) (tm : tm) : unit =
match tm with
| Let _ as tm ->
let rec go names fmt tm =
match tm with
| Let (name, def_ty, def, body) ->
Format.fprintf fmt "@[<2>@[let %a@ :=@]@ @[%a;@]@]@ %a"
pp_name_ann (name, def_ty)
(pp_tm names) def
(go (name :: names)) body
| tm -> Format.fprintf fmt "@[%a@]" (pp_tm names) tm
in
Format.fprintf fmt "@[<v>%a@]" (go names) tm
| FunLit (name, param_ty, body) ->
let rec go names fmt tm =
match tm with
| FunLit (name, param_ty, body) ->
Format.fprintf fmt "@ @[fun@ %a@ =>@]%a"
pp_param (name, param_ty)
(go (name :: names)) body
| tm -> Format.fprintf fmt "@]@ @[%a@]@]" (pp_tm names) tm
in
Format.fprintf fmt "@[<hv 2>@[<hv>@[fun@ %a@ =>@]%a"
pp_param (name, param_ty)
(go (name :: names)) body
| BoolElim (head, tm0, tm1) ->
Format.fprintf fmt "@[<hv>@[if@ %a@ then@]@;<1 2>@[%a@]@ else@;<1 2>@[%a@]@]"
(pp_app_tm names) head
(pp_app_tm names) tm0
(pp_tm names) tm1
| tm ->
pp_app_tm names fmt tm
and pp_app_tm names fmt tm =
match tm with
| FunApp (head, arg) ->
Format.fprintf fmt "@[%a@ %a@]"
(pp_app_tm names) head
(pp_atomic_tm names) arg
| PrimApp (prim, args) ->
let pp_sep fmt () = Format.fprintf fmt "@ " in
Format.fprintf fmt "@[#%s@ -%a@]"
(Prim.name prim)
(Format.pp_print_list ~pp_sep (pp_atomic_tm names)) args
| tm ->
pp_atomic_tm names fmt tm
and pp_atomic_tm names fmt tm =
match tm with
| Var index -> Format.fprintf fmt "%s" (List.nth names index)
| IntLit i -> Format.fprintf fmt "%i" i
| BoolLit true -> Format.fprintf fmt "true"
| BoolLit false -> Format.fprintf fmt "false"
| tm -> Format.fprintf fmt "@[(%a)@]" (pp_tm names) tm