diff options
Diffstat (limited to 'tests/examplefiles/intsyn.fun')
-rw-r--r-- | tests/examplefiles/intsyn.fun | 675 |
1 files changed, 0 insertions, 675 deletions
diff --git a/tests/examplefiles/intsyn.fun b/tests/examplefiles/intsyn.fun deleted file mode 100644 index 777b0fdb..00000000 --- a/tests/examplefiles/intsyn.fun +++ /dev/null @@ -1,675 +0,0 @@ -(* Internal Syntax *) -(* Author: Frank Pfenning, Carsten Schuermann *) -(* Modified: Roberto Virga *) - -functor IntSyn (structure Global : GLOBAL) :> INTSYN = -struct - - type cid = int (* Constant identifier *) - type name = string (* Variable name *) - type mid = int (* Structure identifier *) - type csid = int (* CS module identifier *) - - - (* Contexts *) - datatype 'a Ctx = (* Contexts *) - Null (* G ::= . *) - | Decl of 'a Ctx * 'a (* | G, D *) - - (* ctxPop (G) => G' - Invariant: G = G',D - *) - fun ctxPop (Decl (G, D)) = G - - exception Error of string (* raised if out of space *) - (* ctxLookup (G, k) = D, kth declaration in G from right to left - Invariant: 1 <= k <= |G|, where |G| is length of G - *) - - fun ctxLookup (Decl (G', D), 1) = D - | ctxLookup (Decl (G', _), k') = ctxLookup (G', k'-1) -(* | ctxLookup (Null, k') = (print ("Looking up k' = " ^ Int.toString k' ^ "\n"); raise Error "Out of Bounce\n")*) - (* ctxLookup (Null, k') should not occur by invariant *) - - (* ctxLength G = |G|, the number of declarations in G *) - fun ctxLength G = - let - fun ctxLength' (Null, n) = n - | ctxLength' (Decl(G, _), n)= ctxLength' (G, n+1) - in - ctxLength' (G, 0) - end - - type FgnExp = exn (* foreign expression representation *) - exception UnexpectedFgnExp of FgnExp - (* raised by a constraint solver - if passed an incorrect arg *) - - type FgnCnstr = exn (* foreign unification constraint - representation *) - exception UnexpectedFgnCnstr of FgnCnstr - (* raised by a constraint solver - if passed an incorrect arg *) - - 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 (* | bPi (D, P). V *) - | Root of Head * Spine (* | C @ 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> *) - | NVar of int (* | n (linear, fully applied) *) - (* grafting variable *) - - | FgnExp of csid * FgnExp - (* | (foreign expression) *) - - and Head = (* Heads: *) - BVar of int (* H ::= k *) - | Const of cid (* | c *) - | Proj of Block * int (* | #k(b) *) - | Skonst of cid (* | c# *) - | Def of cid (* | d *) - | NSDef of cid (* | d (non strict) *) - | FVar of name * 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 (assignable) *) - | Block of Block (* | _x *) - | Undef (* | _ *) - - and Dec = (* Declarations: *) - Dec of name option * Exp (* D ::= x:V *) - | BDec of name option * (cid * Sub) (* | v:l[s] *) - | ADec of name option * int (* | v[^-d] *) - | NDec of name 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 *) - - - (* 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 = (* Residual of foreign unify *) - 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 *) *) - - - structure FgnExpStd = struct - - structure ToInternal = FgnOpnTable (type arg = unit - type result = Exp) - - structure Map = FgnOpnTable (type arg = Exp -> Exp - type result = Exp) - - structure App = FgnOpnTable (type arg = Exp -> unit - type result = unit) - - structure EqualTo = FgnOpnTable (type arg = Exp - type result = bool) - - structure UnifyWith = FgnOpnTable (type arg = Dec Ctx * Exp - type result = FgnUnify) - - - - fun fold csfe f b = let - val r = ref b - fun g U = r := f (U,!r) - in - App.apply csfe g ; !r - end - - end - - structure FgnCnstrStd = struct - - structure ToInternal = FgnOpnTable (type arg = unit - type result = (Dec Ctx * Exp) list) - - structure Awake = FgnOpnTable (type arg = unit - type result = bool) - - structure Simplify = FgnOpnTable (type arg = unit - type result = bool) - - end - - fun conDecName (ConDec (name, _, _, _, _, _)) = name - | conDecName (ConDef (name, _, _, _, _, _, _)) = name - | conDecName (AbbrevDef (name, _, _, _, _, _)) = name - | conDecName (SkoDec (name, _, _, _, _)) = name - | conDecName (BlockDec (name, _, _, _)) = name - | conDecName (BlockDef (name, _, _)) = name - - fun conDecParent (ConDec (_, parent, _, _, _, _)) = parent - | conDecParent (ConDef (_, parent, _, _, _, _, _)) = parent - | conDecParent (AbbrevDef (_, parent, _, _, _, _)) = parent - | conDecParent (SkoDec (_, parent, _, _, _)) = parent - | conDecParent (BlockDec (_, parent, _, _)) = parent - | conDecParent (BlockDef (_, parent, _)) = parent - - - (* conDecImp (CD) = k - - Invariant: - If CD is either a declaration, definition, abbreviation, or - a Skolem constant - then k stands for the number of implicit elements. - *) - fun conDecImp (ConDec (_, _, i, _, _, _)) = i - | conDecImp (ConDef (_, _, i, _, _, _, _)) = i - | conDecImp (AbbrevDef (_, _, i, _, _, _)) = i - | conDecImp (SkoDec (_, _, i, _, _)) = i - | conDecImp (BlockDec (_, _, _, _)) = 0 (* watch out -- carsten *) - - fun conDecStatus (ConDec (_, _, _, status, _, _)) = status - | conDecStatus _ = Normal - - (* conDecType (CD) = V - - Invariant: - If CD is either a declaration, definition, abbreviation, or - a Skolem constant - then V is the respective type - *) - fun conDecType (ConDec (_, _, _, _, V, _)) = V - | conDecType (ConDef (_, _, _, _, V, _, _)) = V - | conDecType (AbbrevDef (_, _, _, _, V, _)) = V - | conDecType (SkoDec (_, _, _, V, _)) = V - - - (* conDecBlock (CD) = (Gsome, Lpi) - - Invariant: - If CD is block definition - then Gsome is the context of some variables - and Lpi is the list of pi variables - *) - fun conDecBlock (BlockDec (_, _, Gsome, Lpi)) = (Gsome, Lpi) - - (* conDecUni (CD) = L - - Invariant: - If CD is either a declaration, definition, abbreviation, or - a Skolem constant - then L is the respective universe - *) - fun conDecUni (ConDec (_, _, _, _, _, L)) = L - | conDecUni (ConDef (_, _, _, _, _, L, _)) = L - | conDecUni (AbbrevDef (_, _, _, _, _, L)) = L - | conDecUni (SkoDec (_, _, _, _, L)) = L - - - fun strDecName (StrDec (name, _)) = name - - fun strDecParent (StrDec (_, parent)) = parent - - local - val maxCid = Global.maxCid - val dummyEntry = ConDec("", NONE, 0, Normal, Uni (Kind), Kind) - val sgnArray = Array.array (maxCid+1, dummyEntry) - : ConDec Array.array - val nextCid = ref(0) - - val maxMid = Global.maxMid - val sgnStructArray = Array.array (maxMid+1, StrDec("", NONE)) - : StrDec Array.array - val nextMid = ref (0) - - in - (* Invariants *) - (* Constant declarations are all well-typed *) - (* Constant declarations are stored in beta-normal form *) - (* All definitions are strict in all their arguments *) - (* If Const(cid) is valid, then sgnArray(cid) = ConDec _ *) - (* If Def(cid) is valid, then sgnArray(cid) = ConDef _ *) - - fun sgnClean (i) = if i >= !nextCid then () - else (Array.update (sgnArray, i, dummyEntry); - sgnClean (i+1)) - - fun sgnReset () = ((* Fri Dec 20 12:04:24 2002 -fp *) - (* this circumvents a space leak *) - sgnClean (0); - nextCid := 0; nextMid := 0) - fun sgnSize () = (!nextCid, !nextMid) - - fun sgnAdd (conDec) = - let - val cid = !nextCid - in - if cid > maxCid - then raise Error ("Global signature size " ^ Int.toString (maxCid+1) ^ " exceeded") - else (Array.update (sgnArray, cid, conDec) ; - nextCid := cid + 1; - cid) - end - - (* 0 <= cid < !nextCid *) - fun sgnLookup (cid) = Array.sub (sgnArray, cid) - - fun sgnApp (f) = - let - fun sgnApp' (cid) = - if cid = !nextCid then () else (f cid; sgnApp' (cid+1)) - in - sgnApp' (0) - end - - fun sgnStructAdd (strDec) = - let - val mid = !nextMid - in - if mid > maxMid - then raise Error ("Global signature size " ^ Int.toString (maxMid+1) ^ " exceeded") - else (Array.update (sgnStructArray, mid, strDec) ; - nextMid := mid + 1; - mid) - end - - (* 0 <= mid < !nextMid *) - fun sgnStructLookup (mid) = Array.sub (sgnStructArray, mid) - - (* A hack used in Flit - jcreed 6/05 *) - fun rename (cid, new) = - let - val newConDec = case sgnLookup cid of - ConDec (n,m,i,s,e,u) => ConDec(new,m,i,s,e,u) - | ConDef (n,m,i,e,e',u,a) => ConDef(new,m,i,e,e',u,a) - | AbbrevDef (n,m,i,e,e',u) => AbbrevDef (new,m,i,e,e',u) - | BlockDec (n,m,d,d') => BlockDec (new,m,d,d') - | SkoDec (n,m,i,e,u) => SkoDec (new,m,i,e,u) - in - Array.update (sgnArray, cid, newConDec) - end - - end - - fun constDef (d) = - (case sgnLookup (d) - of ConDef(_, _, _, U,_, _, _) => U - | AbbrevDef (_, _, _, U,_, _) => U) - - fun constType (c) = conDecType (sgnLookup c) - fun constImp (c) = conDecImp (sgnLookup c) - fun constUni (c) = conDecUni (sgnLookup c) - fun constBlock (c) = conDecBlock (sgnLookup c) - - fun constStatus (c) = - (case sgnLookup (c) - of ConDec (_, _, _, status, _, _) => status - | _ => Normal) - - - (* Explicit Substitutions *) - - (* id = ^0 - - Invariant: - G |- id : G id is patsub - *) - val id = Shift(0) - - (* shift = ^1 - - Invariant: - G, V |- ^ : G ^ is patsub - *) - val shift = Shift(1) - - (* invShift = ^-1 = _.^0 - Invariant: - G |- ^-1 : G, V ^-1 is patsub - *) - val invShift = Dot(Undef, id) - - - (* comp (s1, s2) = s' - - Invariant: - If G' |- s1 : G - and G'' |- s2 : G' - then s' = s1 o s2 - and G'' |- s1 o s2 : G - - If s1, s2 patsub - then s' patsub - *) - fun comp (Shift (0), s) = s - (* next line is an optimization *) - (* roughly 15% on standard suite for Twelf 1.1 *) - (* Sat Feb 14 10:15:16 1998 -fp *) - | comp (s, Shift (0)) = s - | comp (Shift (n), Dot (Ft, s)) = comp (Shift (n-1), s) - | comp (Shift (n), Shift (m)) = Shift (n+m) - | comp (Dot (Ft, s), s') = Dot (frontSub (Ft, s'), comp (s, s')) - - (* bvarSub (n, s) = Ft' - - Invariant: - If G |- s : G' G' |- n : V - then Ft' = Ftn if s = Ft1 .. Ftn .. ^k - or Ft' = ^(n+k) if s = Ft1 .. Ftm ^k and m<n - and G |- Ft' : V [s] - *) - and bvarSub (1, Dot(Ft, s)) = Ft - | bvarSub (n, Dot(Ft, s)) = bvarSub (n-1, s) - | bvarSub (n, Shift(k)) = Idx (n+k) - - (* blockSub (B, s) = B' - - Invariant: - If G |- s : G' - and G' |- B block - then G |- B' block - and B [s] == B' - *) - (* in front of substitutions, first case is irrelevant *) - (* Sun Dec 2 11:56:41 2001 -fp *) - and blockSub (Bidx k, s) = - (case bvarSub (k, s) - of Idx k' => Bidx k' - | Block B => B) - | blockSub (LVar (ref (SOME B), sk, _), s) = - blockSub (B, comp (sk, s)) - (* -fp Sun Dec 1 21:18:30 2002 *) - (* --cs Sun Dec 1 11:25:41 2002 *) - (* Since always . |- t : Gsome, discard s *) - (* where is this needed? *) - (* Thu Dec 6 20:30:26 2001 -fp !!! *) - | blockSub (LVar (r as ref NONE, sk, (l, t)), s) = - LVar(r, comp(sk, s), (l, t)) - (* was: - LVar (r, comp(sk, s), (l, comp (t, s))) - July 22, 2010 -fp -cs - *) - (* comp(^k, s) = ^k' for some k' by invariant *) - | blockSub (L as Inst ULs, s') = Inst (map (fn U => EClo (U, s')) ULs) - (* this should be right but somebody should verify *) - - (* frontSub (Ft, s) = Ft' - - Invariant: - If G |- s : G' G' |- Ft : V - then Ft' = Ft [s] - and G |- Ft' : V [s] - - NOTE: EClo (U, s) might be undefined, so if this is ever - computed eagerly, we must introduce an "Undefined" exception, - raise it in whnf and handle it here so Exp (EClo (U, s)) => Undef - *) - and frontSub (Idx (n), s) = bvarSub (n, s) - | frontSub (Exp (U), s) = Exp (EClo (U, s)) - | frontSub (Undef, s) = Undef - | frontSub (Block (B), s) = Block (blockSub (B, s)) - - (* decSub (x:V, s) = D' - - Invariant: - If G |- s : G' G' |- V : L - then D' = x:V[s] - and G |- V[s] : L - *) - (* First line is an optimization suggested by cs *) - (* D[id] = D *) - (* Sat Feb 14 18:37:44 1998 -fp *) - (* seems to have no statistically significant effect *) - (* undo for now Sat Feb 14 20:22:29 1998 -fp *) - (* - fun decSub (D, Shift(0)) = D - | decSub (Dec (x, V), s) = Dec (x, EClo (V, s)) - *) - fun decSub (Dec (x, V), s) = Dec (x, EClo (V, s)) - | decSub (NDec x, s) = NDec x - | decSub (BDec (n, (l, t)), s) = BDec (n, (l, comp (t, s))) - - (* dot1 (s) = s' - - Invariant: - If G |- s : G' - then s' = 1. (s o ^) - and for all V s.t. G' |- V : L - G, V[s] |- s' : G', V - - If s patsub then s' patsub - *) - (* first line is an optimization *) - (* roughly 15% on standard suite for Twelf 1.1 *) - (* Sat Feb 14 10:16:16 1998 -fp *) - fun dot1 (s as Shift (0)) = s - | dot1 s = Dot (Idx(1), comp(s, shift)) - - (* invDot1 (s) = s' - invDot1 (1. s' o ^) = s' - - Invariant: - s = 1 . s' o ^ - If G' |- s' : G - (so G',V[s] |- s : G,V) - *) - fun invDot1 (s) = comp (comp(shift, s), invShift) - - - (* Declaration Contexts *) - - (* ctxDec (G, k) = x:V - Invariant: - If |G| >= k, where |G| is size of G, - then G |- k : V and G |- V : L - *) - fun ctxDec (G, k) = - let (* ctxDec' (G'', k') = x:V - where G |- ^(k-k') : G'', 1 <= k' <= k - *) - fun ctxDec' (Decl (G', Dec (x, V')), 1) = Dec (x, EClo (V', Shift (k))) - | ctxDec' (Decl (G', BDec (n, (l, s))), 1) = BDec (n, (l, comp (s, Shift (k)))) - | ctxDec' (Decl (G', _), k') = ctxDec' (G', k'-1) - (* ctxDec' (Null, k') should not occur by invariant *) - in - ctxDec' (G, k) - end - - (* blockDec (G, v, i) = V - - Invariant: - If G (v) = l[s] - and Sigma (l) = SOME Gsome BLOCK Lblock - and G |- s : Gsome - then G |- pi (v, i) : V - *) - - fun blockDec (G, v as (Bidx k), i) = - let - val BDec (_, (l, s)) = ctxDec (G, k) - (* G |- s : Gsome *) - val (Gsome, Lblock) = conDecBlock (sgnLookup l) - fun blockDec' (t, D :: L, 1, j) = decSub (D, t) - | blockDec' (t, _ :: L, n, j) = - blockDec' (Dot (Exp (Root (Proj (v, j), Nil)), t), - L, n-1, j+1) - in - blockDec' (s, Lblock, i, 1) - end - - - (* EVar related functions *) - - (* newEVar (G, V) = newEVarCnstr (G, V, nil) *) - fun newEVar (G, V) = EVar(ref NONE, G, V, ref nil) - - (* newAVar G = new AVar (assignable variable) *) - (* AVars carry no type, ctx, or cnstr *) - fun newAVar () = AVar(ref NONE) - - (* newTypeVar (G) = X, X new - where G |- X : type - *) - fun newTypeVar (G) = EVar(ref NONE, G, Uni(Type), ref nil) - - (* newLVar (l, s) = (l[s]) *) - fun newLVar (sk, (cid, t)) = LVar (ref NONE, sk, (cid, t)) - - (* Definition related functions *) - (* headOpt (U) = SOME(H) or NONE, U should be strict, normal *) - fun headOpt (Root (H, _)) = SOME(H) - | headOpt (Lam (_, U)) = headOpt U - | headOpt _ = NONE - - fun ancestor' (NONE) = Anc(NONE, 0, NONE) - | ancestor' (SOME(Const(c))) = Anc(SOME(c), 1, SOME(c)) - | ancestor' (SOME(Def(d))) = - (case sgnLookup(d) - of ConDef(_, _, _, _, _, _, Anc(_, height, cOpt)) - => Anc(SOME(d), height+1, cOpt)) - | ancestor' (SOME _) = (* FgnConst possible, BVar impossible by strictness *) - Anc(NONE, 0, NONE) - (* ancestor(U) = ancestor info for d = U *) - fun ancestor (U) = ancestor' (headOpt U) - - (* defAncestor(d) = ancestor of d, d must be defined *) - fun defAncestor (d) = - (case sgnLookup(d) - of ConDef(_, _, _, _, _, _, anc) => anc) - - (* Type related functions *) - - (* targetHeadOpt (V) = SOME(H) or NONE - where H is the head of the atomic target type of V, - NONE if V is a kind or object or have variable type. - Does not expand type definitions. - *) - (* should there possibly be a FgnConst case? also targetFamOpt -kw *) - fun targetHeadOpt (Root (H, _)) = SOME(H) - | targetHeadOpt (Pi(_, V)) = targetHeadOpt V - | targetHeadOpt (Redex (V, S)) = targetHeadOpt V - | targetHeadOpt (Lam (_, V)) = targetHeadOpt V - | targetHeadOpt (EVar (ref (SOME(V)),_,_,_)) = targetHeadOpt V - | targetHeadOpt (EClo (V, s)) = targetHeadOpt V - | targetHeadOpt _ = NONE - (* Root(Bvar _, _), Root(FVar _, _), Root(FgnConst _, _), - EVar(ref NONE,..), Uni, FgnExp _ - *) - (* Root(Skonst _, _) can't occur *) - (* targetHead (A) = a - as in targetHeadOpt, except V must be a valid type - *) - fun targetHead (A) = valOf (targetHeadOpt A) - - (* targetFamOpt (V) = SOME(cid) or NONE - where cid is the type family of the atomic target type of V, - NONE if V is a kind or object or have variable type. - Does expand type definitions. - *) - fun targetFamOpt (Root (Const(cid), _)) = SOME(cid) - | targetFamOpt (Pi(_, V)) = targetFamOpt V - | targetFamOpt (Root (Def(cid), _)) = targetFamOpt (constDef cid) - | targetFamOpt (Redex (V, S)) = targetFamOpt V - | targetFamOpt (Lam (_, V)) = targetFamOpt V - | targetFamOpt (EVar (ref (SOME(V)),_,_,_)) = targetFamOpt V - | targetFamOpt (EClo (V, s)) = targetFamOpt V - | targetFamOpt _ = NONE - (* Root(Bvar _, _), Root(FVar _, _), Root(FgnConst _, _), - EVar(ref NONE,..), Uni, FgnExp _ - *) - (* Root(Skonst _, _) can't occur *) - (* targetFam (A) = a - as in targetFamOpt, except V must be a valid type - *) - fun targetFam (A) = valOf (targetFamOpt A) - -end; (* functor IntSyn *) - -structure IntSyn :> INTSYN = - IntSyn (structure Global = Global); |