Commits

Rob Simmons committed 1384226

Add examples, more improvements to parser based on examining those examples

  • Participants
  • Parent commits d9c440b

Comments (0)

Files changed (4)

pygments/lexers/functional.py

       ';', '\.\.\.', '_', 
       # '\|', '=', '=>', '->', '#', ':>'
     ]
-    symbols = r'[!%&$#+-/:<=>?@\~`^|*]'
+    alphanums = r'[a-zA-Z][0-9a-zA-Z_\']*'
+    symbols = r'[!%&$#+-/:<=>?@\\~`^|*]+'
     primitives = [
       'bool', 'int', 'real', 'string', 'char', 'word', 'list', 'ref', 'exn'
     ]
             (r'\b(%s)\b' % '|'.join(corekeywords), Keyword.Reserved),
             (r'\b(%s)\b' % '|'.join(sigkeywords), Keyword.Namespace),
             (r'\b(%s)\b' % '|'.join(primitives), Keyword.Type),
+            (r'\(\*', Comment.Multiline, 'comment'),
             (r'%s' % '|'.join(keyopts), Operator),
             
-            # Special constants: floats, numbers in decimal and hexadecimal
-            (r'~?\d+(\.\d+|[eE]\d+|.\d+[eE]\d+)', Number.Float),
-            (r'~?\d+', Number.Integer),
-            (r'~?0x[\da-fA-F]+', Number.Hex),
-            (r'0w\d+', Number.Integer),
-            (r'0wx[\da-fA-F]+', Number.Hex),
-            
-            # An identifier is either alphanumeric: any sequence of letters,
-            # digits, primes, and underbars starting with a letter or prime...
-            (r'\'[a-zA-Z_\']*', Name.Decorator),
-            (r'[a-zA-Z][a-zA-Z\'_]*\s*\.', Name.Namespace),
-            (r'[a-zA-Z][a-zA-Z\'_]*', Name),
-            
-            # or symbolic: any non-empty sequence of the following symbols
-            (r'(%s)+\s*\.' % symbols, Name.Namespace),
-            (r'(%s)+' % symbols, Name), 
-            
             # The class Lab is extended to include the numeric labels 1 2 3,
             # i.e. any numeral not starting with 0
-            (r'#[1-9][0-9]*', Name.Label),
-            (r'#[a-zA-Z][a-zA-Z_\']*', Name.Label),
+            (r'#\s*[1-9][0-9]*', Name.Label),
+            (r'#\s*(%s)' % alphanums, Name.Label),
+            (r'#\s*(%s)' % symbols, Name),
+
+            # An identifier is either alphanumeric: any sequence of letters,
+            # digits, primes, and underbars starting with a letter or prime...
+            (r'\'[0-9a-zA-Z_\']*', Name.Decorator),
+            (r'(%s)\s*\.' % alphanums, Name.Namespace),
+            (r'(%s)' % alphanums, Name),
             
+            # or symbolic: any non-empty sequence of the following symbols
+            (r'(%s)\s*\.' % symbols, Name.Namespace),
+            (r'(%s)' % symbols, Name), 
+            
+            # Special constants: floats, numbers in decimal and hexadecimal
+            (r'~?0x[0-9a-fA-F]+', Number.Hex),
+            (r'0wx[0-9a-fA-F]+', Number.Hex),
+            (r'0w\d+', Number.Integer),
+            (r'~?\d+\.\d+[eE]~?\d+', Number.Float),
+            (r'~?\d+\.\d+', Number.Float),
+            (r'~?\d+[eE]~?\d+', Number.Float),
+            (r'~?\d+', Number.Integer),
+                        
             (r'#"', String.Char, 'char'),
             (r'"', String.Double, 'string'),
         ],
+        'comment': [
+            (r'[^(*)]', Comment.Multiline),
+            (r'\(\*', Comment.Multiline, '#push'),
+            (r'\*\)', Comment.Multiline, '#pop'),
+            (r'[(*)]', Comment.Multiline),
+        ],
         'char': stringy(String.Char),
         'string': stringy(String.Double),
     }

tests/examplefiles/example.sml

+(*(*(*(*(* This file is all pretty strange Standard ML *)*)*)*) (**)*)
+(* Robert J. Simmons *)
+
+signature BA_Z = sig end 
+
+structure **$*#$ = struct (* What (* A * strange * name *) for ) a ( struct *)
+
+structure Bar :> BA_Z = struct end
+structure !%&$#+-/:<=>?@\~`^|* :> BA_Z = struct end
+
+val$$$ = fn x => fn y => fn z => fn w => w
+val (foo, ++, bar, ||) = (4, 4, 5, 5)
+val _ = $$$foo++bar||
+
+val x : ' list = []
+val x : (' -> ') = fn x => x
+val x : ('a -> 'a) = fn x => x
+val x : (''a -> ''a) = fn x => x
+val x : ('''' -> '''') = fn x => x
+val x : unit = print "Weird, huh?\n"
+val w = {x=1,y=2,##= =3,4=3}
+val {##=, x, 4=a,...} = w
+val z = #4 w
+val z = # ##= w
+
+datatype ('0, 'b, '_, ') fo'o = Bar | baZ12' | dsfa_fad | #@$
+
+val _ = 123
+val _ = 0001
+val _ = ~123
+val _ = ~0001
+val _ = 0w12412
+val _ = 0w12412
+val _ = 0xfA0
+val _ = ~0xfA0
+val _ = 0wxfA0
+val _ = 1.4
+val _ = ~1.4
+val _ = 1e~2
+val _ = 1E~2
+val _ = 1e2
+val _ = 1E2
+val _ = 1.4e~2
+val _ = 1.4E~2
+val _ = 1.4e2
+val _ = 1.4E2
+
+val st = "foo \
+ 	 \ bar" ^ "baz \        
+  	 \ and \ 
+   	 \ such\n"
+
+val () = print st
+
+val _ = foo::bar::4::[++]
+
+end

tests/examplefiles/intsyn.fun

+(* 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);

tests/examplefiles/intsyn.sig

+(* 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 *)