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
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
|
(* Internal Syntax *)
(* Author: Frank Pfenning, Carsten Schuermann *)
(* Modified: Roberto Virga *)
signature INTSYN =
sig
type cid = int (* Constant identifier *)
type mid = int (* Structure identifier *)
type csid = int (* CS module identifier *)
type FgnExp = exn (* foreign expression representation *)
exception UnexpectedFgnExp of FgnExp
(* raised by a constraint solver
if passed an incorrect arg *)
type FgnCnstr = exn (* foreign constraint representation *)
exception UnexpectedFgnCnstr of FgnCnstr
(* raised by a constraint solver
if passed an incorrect arg *)
(* Contexts *)
datatype 'a Ctx = (* Contexts *)
Null (* G ::= . *)
| Decl of 'a Ctx * 'a (* | G, D *)
val ctxPop : 'a Ctx -> 'a Ctx
val ctxLookup: 'a Ctx * int -> 'a
val ctxLength: 'a Ctx -> int
datatype Depend = (* Dependency information *)
No (* P ::= No *)
| Maybe (* | Maybe *)
| Meta (* | Meta *)
(* expressions *)
datatype Uni = (* Universes: *)
Kind (* L ::= Kind *)
| Type (* | Type *)
datatype Exp = (* Expressions: *)
Uni of Uni (* U ::= L *)
| Pi of (Dec * Depend) * Exp (* | Pi (D, P). V *)
| Root of Head * Spine (* | H @ S *)
| Redex of Exp * Spine (* | U @ S *)
| Lam of Dec * Exp (* | lam D. U *)
| EVar of Exp option ref * Dec Ctx * Exp * (Cnstr ref) list ref
(* | X<I> : G|-V, Cnstr *)
| EClo of Exp * Sub (* | U[s] *)
| AVar of Exp option ref (* | A<I> *)
| FgnExp of csid * FgnExp (* | (foreign expression) *)
| NVar of int (* | n (linear,
fully applied variable
used in indexing *)
and Head = (* Head: *)
BVar of int (* H ::= k *)
| Const of cid (* | c *)
| Proj of Block * int (* | #k(b) *)
| Skonst of cid (* | c# *)
| Def of cid (* | d (strict) *)
| NSDef of cid (* | d (non strict) *)
| FVar of string * Exp * Sub (* | F[s] *)
| FgnConst of csid * ConDec (* | (foreign constant) *)
and Spine = (* Spines: *)
Nil (* S ::= Nil *)
| App of Exp * Spine (* | U ; S *)
| SClo of Spine * Sub (* | S[s] *)
and Sub = (* Explicit substitutions: *)
Shift of int (* s ::= ^n *)
| Dot of Front * Sub (* | Ft.s *)
and Front = (* Fronts: *)
Idx of int (* Ft ::= k *)
| Exp of Exp (* | U *)
| Axp of Exp (* | U *)
| Block of Block (* | _x *)
| Undef (* | _ *)
and Dec = (* Declarations: *)
Dec of string option * Exp (* D ::= x:V *)
| BDec of string option * (cid * Sub) (* | v:l[s] *)
| ADec of string option * int (* | v[^-d] *)
| NDec of string option
and Block = (* Blocks: *)
Bidx of int (* b ::= v *)
| LVar of Block option ref * Sub * (cid * Sub)
(* | L(l[^k],t) *)
| Inst of Exp list (* | U1, ..., Un *)
(* It would be better to consider having projections count
like substitutions, then we could have Inst of Sub here,
which would simplify a lot of things.
I suggest however to wait until the next big overhaul
of the system -- cs *)
(* | BClo of Block * Sub (* | b[s] *) *)
(* constraints *)
and Cnstr = (* Constraint: *)
Solved (* Cnstr ::= solved *)
| Eqn of Dec Ctx * Exp * Exp (* | G|-(U1 == U2) *)
| FgnCnstr of csid * FgnCnstr (* | (foreign) *)
and Status = (* Status of a constant: *)
Normal (* inert *)
| Constraint of csid * (Dec Ctx * Spine * int -> Exp option)
(* acts as constraint *)
| Foreign of csid * (Spine -> Exp) (* is converted to foreign *)
and FgnUnify = (* Result of foreign unify *)
Succeed of FgnUnifyResidual list
(* succeed with a list of residual operations *)
| Fail
and FgnUnifyResidual =
Assign of Dec Ctx * Exp * Exp * Sub
(* perform the assignment G |- X = U [ss] *)
| Delay of Exp * Cnstr ref
(* delay cnstr, associating it with all the rigid EVars in U *)
(* Global signature *)
and ConDec = (* Constant declaration *)
ConDec of string * mid option * int * Status
(* a : K : kind or *)
* Exp * Uni (* c : A : type *)
| ConDef of string * mid option * int (* a = A : K : kind or *)
* Exp * Exp * Uni (* d = M : A : type *)
* Ancestor (* Ancestor info for d or a *)
| AbbrevDef of string * mid option * int
(* a = A : K : kind or *)
* Exp * Exp * Uni (* d = M : A : type *)
| BlockDec of string * mid option (* %block l : SOME G1 PI G2 *)
* Dec Ctx * Dec list
| BlockDef of string * mid option * cid list
(* %block l = (l1 | ... | ln) *)
| SkoDec of string * mid option * int (* sa: K : kind or *)
* Exp * Uni (* sc: A : type *)
and Ancestor = (* Ancestor of d or a *)
Anc of cid option * int * cid option (* head(expand(d)), height, head(expand[height](d)) *)
(* NONE means expands to {x:A}B *)
datatype StrDec = (* Structure declaration *)
StrDec of string * mid option
(* Form of constant declaration *)
datatype ConDecForm =
FromCS (* from constraint domain *)
| Ordinary (* ordinary declaration *)
| Clause (* %clause declaration *)
(* Type abbreviations *)
type dctx = Dec Ctx (* G = . | G,D *)
type eclo = Exp * Sub (* Us = U[s] *)
type bclo = Block * Sub (* Bs = B[s] *)
type cnstr = Cnstr ref
exception Error of string (* raised if out of space *)
(* standard operations on foreign expressions *)
structure FgnExpStd : sig
(* convert to internal syntax *)
structure ToInternal : FGN_OPN where type arg = unit
where type result = Exp
(* apply function to subterms *)
structure Map : FGN_OPN where type arg = Exp -> Exp
where type result = Exp
(* apply function to subterms, for effect *)
structure App : FGN_OPN where type arg = Exp -> unit
where type result = unit
(* test for equality *)
structure EqualTo : FGN_OPN where type arg = Exp
where type result = bool
(* unify with another term *)
structure UnifyWith : FGN_OPN where type arg = Dec Ctx * Exp
where type result = FgnUnify
(* fold a function over the subterms *)
val fold : (csid * FgnExp) -> (Exp * 'a -> 'a) -> 'a -> 'a
end
(* standard operations on foreign constraints *)
structure FgnCnstrStd : sig
(* convert to internal syntax *)
structure ToInternal : FGN_OPN where type arg = unit
where type result = (Dec Ctx * Exp) list
(* awake *)
structure Awake : FGN_OPN where type arg = unit
where type result = bool
(* simplify *)
structure Simplify : FGN_OPN where type arg = unit
where type result = bool
end
val conDecName : ConDec -> string
val conDecParent : ConDec -> mid option
val conDecImp : ConDec -> int
val conDecStatus : ConDec -> Status
val conDecType : ConDec -> Exp
val conDecBlock : ConDec -> dctx * Dec list
val conDecUni : ConDec -> Uni
val strDecName : StrDec -> string
val strDecParent : StrDec -> mid option
val sgnReset : unit -> unit
val sgnSize : unit -> cid * mid
val sgnAdd : ConDec -> cid
val sgnLookup: cid -> ConDec
val sgnApp : (cid -> unit) -> unit
val sgnStructAdd : StrDec -> mid
val sgnStructLookup : mid -> StrDec
val constType : cid -> Exp (* type of c or d *)
val constDef : cid -> Exp (* definition of d *)
val constImp : cid -> int
val constStatus : cid -> Status
val constUni : cid -> Uni
val constBlock : cid -> dctx * Dec list
(* Declaration Contexts *)
val ctxDec : dctx * int -> Dec (* get variable declaration *)
val blockDec : dctx * Block * int -> Dec
(* Explicit substitutions *)
val id : Sub (* id *)
val shift : Sub (* ^ *)
val invShift : Sub (* ^-1 *)
val bvarSub : int * Sub -> Front (* k[s] *)
val frontSub : Front * Sub -> Front (* H[s] *)
val decSub : Dec * Sub -> Dec (* x:V[s] *)
val blockSub : Block * Sub -> Block (* B[s] *)
val comp : Sub * Sub -> Sub (* s o s' *)
val dot1 : Sub -> Sub (* 1 . (s o ^) *)
val invDot1 : Sub -> Sub (* (^ o s) o ^-1) *)
(* EVar related functions *)
val newEVar : dctx * Exp -> Exp (* creates X:G|-V, [] *)
val newAVar : unit -> Exp (* creates A (bare) *)
val newTypeVar : dctx -> Exp (* creates X:G|-type, [] *)
val newLVar : Sub * (cid * Sub) -> Block
(* creates B:(l[^k],t) *)
(* Definition related functions *)
val headOpt : Exp -> Head option
val ancestor : Exp -> Ancestor
val defAncestor : cid -> Ancestor
(* Type related functions *)
(* Not expanding type definitions *)
val targetHeadOpt : Exp -> Head option (* target type family or NONE *)
val targetHead : Exp -> Head (* target type family *)
(* Expanding type definitions *)
val targetFamOpt : Exp -> cid option (* target type family or NONE *)
val targetFam : Exp -> cid (* target type family *)
(* Used in Flit *)
val rename : cid * string -> unit
end; (* signature INTSYN *)
|
