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