summaryrefslogtreecommitdiff
path: root/tests/examplefiles/intsyn.fun
diff options
context:
space:
mode:
Diffstat (limited to 'tests/examplefiles/intsyn.fun')
-rw-r--r--tests/examplefiles/intsyn.fun675
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);
View Lorry Controller Status