1(* Internal Syntax *)
2(* Author: Frank Pfenning, Carsten Schuermann *)
3(* Modified: Roberto Virga *)
4
5signature INTSYN =
6sig
7
8  type cid = int			(* Constant identifier        *)
9  type mid = int                        (* Structure identifier       *)
10  type csid = int                       (* CS module identifier       *)
11
12
13  type FgnExp = exn                     (* foreign expression representation *)
14  exception UnexpectedFgnExp of FgnExp
15                                        (* raised by a constraint solver
16					   if passed an incorrect arg *)
17  type FgnCnstr = exn                   (* foreign constraint representation *)
18  exception UnexpectedFgnCnstr of FgnCnstr
19                                        (* raised by a constraint solver
20                                           if passed an incorrect arg *)
21
22  (* Contexts *)
23
24  datatype 'a Ctx =			(* Contexts                   *)
25    Null				(* G ::= .                    *)
26  | Decl of 'a Ctx * 'a			(*     | G, D                 *)
27
28  val ctxPop : 'a Ctx -> 'a Ctx
29  val ctxLookup: 'a Ctx * int -> 'a
30  val ctxLength: 'a Ctx -> int
31
32  datatype Depend =                     (* Dependency information     *)
33    No                                  (* P ::= No                   *)
34  | Maybe                               (*     | Maybe                *)
35  | Meta				(*     | Meta                 *)
36
37  (* expressions *)
38
39  datatype Uni =			(* Universes:                 *)
40    Kind				(* L ::= Kind                 *)
41  | Type				(*     | Type                 *)
42
43  datatype Exp =			(* Expressions:               *)
44    Uni   of Uni			(* U ::= L                    *)
45  | Pi    of (Dec * Depend) * Exp	(*     | Pi (D, P). V         *)
46  | Root  of Head * Spine		(*     | H @ S                *)
47  | Redex of Exp * Spine		(*     | U @ S                *)
48  | Lam   of Dec * Exp			(*     | lam D. U             *)
49  | EVar  of Exp option ref * Dec Ctx * Exp * (Cnstr ref) list ref
50                                        (*     | X<I> : G|-V, Cnstr   *)
51  | EClo  of Exp * Sub			(*     | U[s]                 *)
52  | AVar  of Exp option ref             (*     | A<I>                 *)
53
54  | FgnExp of csid * FgnExp             (*     | (foreign expression) *)
55
56  | NVar  of int			(*     | n (linear,
57                                               fully applied variable
58                                               used in indexing       *)
59
60  and Head =				(* Head:                      *)
61    BVar  of int			(* H ::= k                    *)
62  | Const of cid			(*     | c                    *)
63  | Proj  of Block * int		(*     | #k(b)                *)
64  | Skonst of cid			(*     | c#                   *)
65  | Def   of cid			(*     | d (strict)           *)
66  | NSDef of cid			(*     | d (non strict)       *)
67  | FVar  of string * Exp * Sub		(*     | F[s]                 *)
68  | FgnConst of csid * ConDec           (*     | (foreign constant)   *)
69
70  and Spine =				(* Spines:                    *)
71    Nil					(* S ::= Nil                  *)
72  | App   of Exp * Spine		(*     | U ; S                *)
73  | SClo  of Spine * Sub		(*     | S[s]                 *)
74
75  and Sub =				(* Explicit substitutions:    *)
76    Shift of int			(* s ::= ^n                   *)
77  | Dot   of Front * Sub		(*     | Ft.s                 *)
78
79  and Front =				(* Fronts:                    *)
80    Idx of int				(* Ft ::= k                   *)
81  | Exp of Exp				(*     | U                    *)
82  | Axp of Exp				(*     | U                    *)
83  | Block of Block			(*     | _x                   *)
84  | Undef				(*     | _                    *)
85
86  and Dec =				(* Declarations:              *)
87    Dec of string option * Exp		(* D ::= x:V                  *)
88  | BDec of string option * (cid * Sub)	(*     | v:l[s]               *)
89  | ADec of string option * int	        (*     | v[^-d]               *)
90  | NDec of string option
91
92  and Block =				(* Blocks:                    *)
93    Bidx of int				(* b ::= v                    *)
94  | LVar of Block option ref * Sub * (cid * Sub)
95                                        (*     | L(l[^k],t)           *)
96  | Inst of Exp list                    (*     | U1, ..., Un          *)
97  (* It would be better to consider having projections count
98     like substitutions, then we could have Inst of Sub here,
99     which would simplify a lot of things.
100
101     I suggest however to wait until the next big overhaul
102     of the system -- cs *)
103
104
105(*  | BClo of Block * Sub                 (*     | b[s]                 *) *)
106
107  (* constraints *)
108
109  and Cnstr =				(* Constraint:                *)
110    Solved                      	(* Cnstr ::= solved           *)
111  | Eqn      of Dec Ctx * Exp * Exp     (*         | G|-(U1 == U2)    *)
112  | FgnCnstr of csid * FgnCnstr         (*         | (foreign)        *)
113
114  and Status =                          (* Status of a constant:      *)
115    Normal                              (*   inert                    *)
116  | Constraint of csid * (Dec Ctx * Spine * int -> Exp option)
117                                        (*   acts as constraint       *)
118  | Foreign of csid * (Spine -> Exp)    (*   is converted to foreign  *)
119
120  and FgnUnify =                        (* Result of foreign unify    *)
121    Succeed of FgnUnifyResidual list
122    (* succeed with a list of residual operations *)
123  | Fail
124
125  and FgnUnifyResidual =
126    Assign of Dec Ctx * Exp * Exp * Sub
127    (* perform the assignment G |- X = U [ss] *)
128  | Delay of Exp * Cnstr ref
129    (* delay cnstr, associating it with all the rigid EVars in U  *)
130
131  (* Global signature *)
132
133  and ConDec =			        (* Constant declaration       *)
134    ConDec of string * mid option * int * Status
135                                        (* a : K : kind  or           *)
136              * Exp * Uni	        (* c : A : type               *)
137  | ConDef of string * mid option * int	(* a = A : K : kind  or       *)
138              * Exp * Exp * Uni		(* d = M : A : type           *)
139              * Ancestor                (* Ancestor info for d or a   *)
140  | AbbrevDef of string * mid option * int
141                                        (* a = A : K : kind  or       *)
142              * Exp * Exp * Uni		(* d = M : A : type           *)
143  | BlockDec of string * mid option     (* %block l : SOME G1 PI G2   *)
144              * Dec Ctx * Dec list
145  | BlockDef of string * mid option * cid list
146                                        (* %block l = (l1 | ... | ln) *)
147  | SkoDec of string * mid option * int	(* sa: K : kind  or           *)
148              * Exp * Uni	        (* sc: A : type               *)
149
150  and Ancestor =			(* Ancestor of d or a         *)
151    Anc of cid option * int * cid option (* head(expand(d)), height, head(expand[height](d)) *)
152                                        (* NONE means expands to {x:A}B *)
153
154  datatype StrDec =                     (* Structure declaration      *)
155      StrDec of string * mid option
156
157  (* Form of constant declaration *)
158  datatype ConDecForm =
159    FromCS				(* from constraint domain *)
160  | Ordinary				(* ordinary declaration *)
161  | Clause				(* %clause declaration *)
162
163  (* Type abbreviations *)
164  type dctx = Dec Ctx			(* G = . | G,D                *)
165  type eclo = Exp * Sub   		(* Us = U[s]                  *)
166  type bclo = Block * Sub   		(* Bs = B[s]                  *)
167  type cnstr = Cnstr ref
168
169  exception Error of string		(* raised if out of space     *)
170
171  (* standard operations on foreign expressions *)
172  structure FgnExpStd : sig
173    (* convert to internal syntax *)
174    structure ToInternal : FGN_OPN where type arg = unit
175                                   where type result = Exp
176
177    (* apply function to subterms *)
178    structure Map : FGN_OPN where type arg = Exp -> Exp
179			    where type result = Exp
180
181    (* apply function to subterms, for effect *)
182    structure App : FGN_OPN where type arg = Exp -> unit
183			    where type result = unit
184
185    (* test for equality *)
186    structure EqualTo : FGN_OPN where type arg = Exp
187                                where type result = bool
188
189    (* unify with another term *)
190    structure UnifyWith : FGN_OPN where type arg = Dec Ctx * Exp
191                                  where type result = FgnUnify
192
193    (* fold a function over the subterms *)
194    val fold : (csid * FgnExp) -> (Exp * 'a -> 'a) -> 'a -> 'a
195  end
196
197  (* standard operations on foreign constraints *)
198  structure FgnCnstrStd : sig
199    (* convert to internal syntax *)
200    structure ToInternal : FGN_OPN where type arg = unit
201                                   where type result = (Dec Ctx * Exp) list
202
203    (* awake *)
204    structure Awake : FGN_OPN where type arg = unit
205                              where type result = bool
206
207    (* simplify *)
208    structure Simplify : FGN_OPN where type arg = unit
209                                 where type result = bool
210  end
211
212  val conDecName   : ConDec -> string
213  val conDecParent : ConDec -> mid option
214  val conDecImp    : ConDec -> int
215  val conDecStatus : ConDec -> Status
216  val conDecType   : ConDec -> Exp
217  val conDecBlock  : ConDec -> dctx * Dec list
218  val conDecUni    : ConDec -> Uni
219
220  val strDecName   : StrDec -> string
221  val strDecParent : StrDec -> mid option
222
223  val sgnReset     : unit -> unit
224  val sgnSize      : unit -> cid * mid
225
226  val sgnAdd   : ConDec -> cid
227  val sgnLookup: cid -> ConDec
228  val sgnApp   : (cid -> unit) -> unit
229
230  val sgnStructAdd    : StrDec -> mid
231  val sgnStructLookup : mid -> StrDec
232
233  val constType   : cid -> Exp		(* type of c or d             *)
234  val constDef    : cid -> Exp		(* definition of d            *)
235  val constImp    : cid -> int
236  val constStatus : cid -> Status
237  val constUni    : cid -> Uni
238  val constBlock  : cid -> dctx * Dec list
239
240  (* Declaration Contexts *)
241
242  val ctxDec    : dctx * int -> Dec	(* get variable declaration   *)
243  val blockDec  : dctx * Block * int -> Dec
244
245  (* Explicit substitutions *)
246
247  val id        : Sub			(* id                         *)
248  val shift     : Sub			(* ^                          *)
249  val invShift  : Sub                   (* ^-1                        *)
250
251  val bvarSub   : int * Sub -> Front    (* k[s]                       *)
252  val frontSub  : Front * Sub -> Front	(* H[s]                       *)
253  val decSub    : Dec * Sub -> Dec	(* x:V[s]                     *)
254  val blockSub  : Block * Sub -> Block  (* B[s]                       *)
255
256  val comp      : Sub * Sub -> Sub	(* s o s'                     *)
257  val dot1      : Sub -> Sub		(* 1 . (s o ^)                *)
258  val invDot1   : Sub -> Sub		(* (^ o s) o ^-1)             *)
259
260  (* EVar related functions *)
261
262  val newEVar    : dctx * Exp -> Exp	(* creates X:G|-V, []         *)
263  val newAVar    : unit ->  Exp	        (* creates A (bare)           *)
264  val newTypeVar : dctx -> Exp		(* creates X:G|-type, []      *)
265  val newLVar    : Sub * (cid * Sub) -> Block
266					(* creates B:(l[^k],t)        *)
267
268  (* Definition related functions *)
269  val headOpt : Exp -> Head option
270  val ancestor : Exp -> Ancestor
271  val defAncestor : cid -> Ancestor
272
273  (* Type related functions *)
274
275  (* Not expanding type definitions *)
276  val targetHeadOpt : Exp -> Head option (* target type family or NONE *)
277  val targetHead : Exp -> Head           (* target type family         *)
278
279  (* Expanding type definitions *)
280  val targetFamOpt : Exp -> cid option  (* target type family or NONE *)
281  val targetFam : Exp -> cid            (* target type family         *)
282
283  (* Used in Flit *)
284  val rename : cid * string -> unit
285
286end;  (* signature INTSYN *)
287