Georg Brandl avatar Georg Brandl committed f1251d8 Merge

Merged in robsimmons/pygments-main (pull request #14)

Comments (0)

Files changed (6)

 * Ken Schutte -- Matlab lexers
 * Tassilo Schweyer -- Io, MOOCode lexers
 * Joerg Sieker -- ABAP lexer
+* Robert Simmons -- Standard ML lexer
 * Kirill Simonov -- YAML lexer
 * Steve Spigarelli -- XQuery lexer
 * Jerome St-Louis -- eC lexer

pygments/lexers/_mapping.py

     'RubyConsoleLexer': ('pygments.lexers.agile', 'Ruby irb session', ('rbcon', 'irb'), (), ('text/x-ruby-shellsession',)),
     'RubyLexer': ('pygments.lexers.agile', 'Ruby', ('rb', 'ruby', 'duby'), ('*.rb', '*.rbw', 'Rakefile', '*.rake', '*.gemspec', '*.rbx', '*.duby'), ('text/x-ruby', 'application/x-ruby')),
     'SLexer': ('pygments.lexers.math', 'S', ('splus', 's', 'r'), ('*.S', '*.R'), ('text/S-plus', 'text/S', 'text/R')),
+    'SMLLexer': ('pygments.lexers.functional', 'Standard ML', ('sml',), ('*.sml', '*.sig', '*.fun'), ('text/x-standard-ml',)),
     'SassLexer': ('pygments.lexers.web', 'Sass', ('sass', 'SASS'), ('*.sass',), ('text/x-sass',)),
     'ScalaLexer': ('pygments.lexers.compiled', 'Scala', ('scala',), ('*.scala',), ('text/x-scala',)),
     'ScamlLexer': ('pygments.lexers.web', 'Scaml', ('scaml', 'SCAML'), ('*.scaml',), ('text/x-scaml',)),

pygments/lexers/functional.py

 
 from pygments.lexer import Lexer, RegexLexer, bygroups, include, do_insertions
 from pygments.token import Text, Comment, Operator, Keyword, Name, \
-     String, Number, Punctuation, Literal, Generic
+     String, Number, Punctuation, Literal, Generic, Error
 
 
 __all__ = ['SchemeLexer', 'CommonLispLexer', 'HaskellLexer', 'LiterateHaskellLexer',
+           'SMLLexer', 
            'OcamlLexer', 'ErlangLexer', 'ErlangShellLexer']
 
 
             yield item
 
 
+class SMLLexer(RegexLexer):
+    """
+    For the Standard ML language.
+    """
+
+    name = 'Standard ML'
+    aliases = ['sml']
+    filenames = ['*.sml', '*.sig', '*.fun',]
+    mimetypes = ['text/x-standardml', 'application/x-standardml']
+
+    alphanumid_reserved = [
+      # Core 
+      'abstype', 'and', 'andalso', 'as', 'case', 'datatype', 'do', 'else',
+      'end', 'exception', 'fn', 'fun', 'handle', 'if', 'in', 'infix', 
+      'infixr', 'let', 'local', 'nonfix', 'of', 'op', 'open', 'orelse',
+      'raise', 'rec', 'then', 'type', 'val', 'with', 'withtype', 'while',
+      # Modules
+      'eqtype', 'functor', 'include', 'sharing', 'sig', 'signature',
+      'struct', 'structure', 'where',
+    ]
+
+    symbolicid_reserved = [
+      # Core 
+      ':', '\|', '=', '=>', '->', '#',
+      # Modules
+      ':>',
+    ]
+
+    nonid_reserved = [ '(', ')', '[', ']', '{', '}', ',', ';', '...', '_' ]
+
+    alphanumid_re = r"[a-zA-Z][a-zA-Z0-9_']*"
+    symbolicid_re = r"[!%&$#+\-/:<=>?@\\~`^|*]+"
+
+    # A character constant is a sequence of the form #s, where s is a string
+    # constant denoting a string of size one character. This setup just parses
+    # the entire string as either a String.Double or a String.Char (depending 
+    # on the argument), even if the String.Char is an erronous 
+    # multiple-character string. 
+    def stringy (whatkind):
+        return [
+            (r'[^"\\]', whatkind),
+            (r'\\[\\\"abtnvfr]', String.Escape),
+            (r'\\\^[@-^]', String.Escape),
+            (r'\\[0-9]{3}', String.Escape),
+            (r'\\u[0-9a-fA-F]{4}', String.Escape),
+            (r'\\\s+\\', String.Interpol),
+            (r'"', whatkind, '#pop'),
+        ]
+
+    # Callbacks for distinguishing tokens and reserved words
+    def long_id_callback(self, match):
+        if match.group(1) in self.alphanumid_reserved: token = Error
+        else: token = Name.Namespace
+        yield match.start(1), token, match.group(1)
+        yield match.start(2), Punctuation, match.group(2) 
+
+    def end_id_callback(self, match):
+        if match.group(1) in self.alphanumid_reserved: token = Error
+        elif match.group(1) in self.symbolicid_reserved: token = Error
+        else: token = Name
+        yield match.start(1), token, match.group(1)
+        
+    def id_callback(self, match):
+        str = match.group(1)
+        if str in self.alphanumid_reserved: token = Keyword.Reserved
+        elif str in self.symbolicid_reserved: token = Punctuation
+        else: token = Name
+        yield match.start(1), token, str
+
+    tokens = {
+        # Whitespace and comments are (almost) everywhere
+        'whitespace': [
+            (r'\s+', Text),
+            (r'\(\*', Comment.Multiline, 'comment'),
+        ],
+
+        'delimiters': [
+            # This lexer treats these delimiters specially:
+            # Delimiters define scopes, and the scope is how the meaning of 
+            # the `|' is resolved - is it a case/handle expression, or function
+            # definition by cases? (This is not how the Definition works, but
+            # it's how MLton behaves, see http://mlton.org/SMLNJDeviations)
+            (r'\(|\[|{', Punctuation, 'main'),
+            (r'\)|\]|}', Punctuation, '#pop'),
+            (r'\b(let|if|local)\b(?!\')', Keyword.Reserved, ('main', 'main')),
+            (r'\b(struct|sig|while)\b(?!\')', Keyword.Reserved, 'main'),
+            (r'\b(do|else|end|in|then)\b(?!\')', Keyword.Reserved, '#pop'),
+        ],
+
+        'core': [
+            # Punctuation that doesn't overlap symbolic identifiers
+            (r'(%s)' % '|'.join([re.escape(z) for z in nonid_reserved]), 
+             Punctuation),
+
+            # Special constants: strings, floats, numbers in decimal and hex
+            (r'#"', String.Char, 'char'),
+            (r'"', String.Double, 'string'),
+            (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),                        
+
+            # Labels
+            (r'#\s*[1-9][0-9]*', Name.Label),
+            (r'#\s*(%s)' % alphanumid_re, Name.Label),
+            (r'#\s+(%s)' % symbolicid_re, Name.Label),
+            # Some reserved words trigger a special, local lexer state change
+            (r'\b(datatype|abstype)\b(?!\')', Keyword.Reserved, 'dname'),
+            (r'(?=\b(exception)\b(?!\'))', Text, ('ename')),
+            (r'\b(functor|include|open|signature|structure)\b(?!\')',
+             Keyword.Reserved, 'sname'),
+            (r'\b(type|eqtype)\b(?!\')', Keyword.Reserved, 'tname'),
+
+            # Regular identifiers, long and otherwise
+            (r'\'[0-9a-zA-Z_\']*', Name.Decorator),
+            (r'(%s)(\.)' % alphanumid_re, long_id_callback, "dotted"),
+            (r'(%s)' % alphanumid_re, id_callback),
+            (r'(%s)' % symbolicid_re, id_callback),
+        ],
+        'dotted': [
+            (r'(%s)(\.)' % alphanumid_re, long_id_callback),
+            (r'(%s)' % alphanumid_re, end_id_callback, "#pop"),
+            (r'(%s)' % symbolicid_re, end_id_callback, "#pop"),
+            (r'\s+', Error),
+            (r'\S+', Error),
+        ],
+
+
+        # Main parser (prevents errors in files that have scoping errors)
+        'root': [ (r'', Text, 'main') ], 
+
+        # In this scope, I expect '|' to not be followed by a function name, 
+        # and I expect 'and' to be followed by a binding site
+        'main': [            
+            include('whitespace'),
+
+            # Special behavior of val/and/fun
+            (r'\b(val|and)\b(?!\')', Keyword.Reserved, 'vname'),
+            (r'\b(fun)\b(?!\')', Keyword.Reserved, 
+             ('#pop', 'main-fun', 'fname')),
+
+            include('delimiters'),
+            include('core'),
+            (r'\S+', Error),            
+        ],
+
+        # In this scope, I expect '|' and 'and' to be followed by a function
+        'main-fun': [
+            include('whitespace'),
+
+            (r'\s', Text),
+            (r'\(\*', Comment.Multiline, 'comment'),
+
+            # Special behavior of val/and/fun
+            (r'\b(fun|and)\b(?!\')', Keyword.Reserved, 'fname'),
+            (r'\b(val)\b(?!\')', Keyword.Reserved, 
+             ('#pop', 'main', 'vname')),
+
+            # Special behavior of '|' and '|'-manipulating keywords
+            (r'\|', Punctuation, 'fname'),
+            (r'\b(case|handle)\b(?!\')', Keyword.Reserved,
+             ('#pop', 'main')),
+
+            include('delimiters'),
+            include('core'),
+            (r'\S+', Error),            
+        ],
+
+        # Character and string parsers
+        'char': stringy(String.Char),
+        'string': stringy(String.Double),
+
+        'breakout': [
+            (r'(?=\b(%s)\b(?!\'))' % '|'.join(alphanumid_reserved), Text, '#pop'),
+        ],
+
+        # Dealing with what comes after module system keywords
+        'sname': [
+            include('whitespace'),
+            include('breakout'),
+
+            (r'(%s)' % alphanumid_re, Name.Namespace),
+            (r'', Text, '#pop'),            
+        ],
+
+        # Dealing with what comes after the 'fun' (or 'and' or '|') keyword
+        'fname': [
+            include('whitespace'),
+            (r'\'[0-9a-zA-Z_\']*', Name.Decorator),
+            (r'\(', Punctuation, 'tyvarseq'),
+
+            (r'(%s)' % alphanumid_re, Name.Function, '#pop'),
+            (r'(%s)' % symbolicid_re, Name.Function, '#pop'), 
+
+            # Ignore interesting function declarations like "fun (x + y) = ..."
+            (r'', Text, '#pop'), 
+        ],
+
+        # Dealing with what comes after the 'val' (or 'and') keyword
+        'vname': [
+            include('whitespace'),
+            (r'\'[0-9a-zA-Z_\']*', Name.Decorator),
+            (r'\(', Punctuation, 'tyvarseq'),
+
+            (r'(%s)(\s*)(=(?!%s))' % (alphanumid_re, symbolicid_re), 
+             bygroups(Name.Variable, Text, Punctuation), '#pop'),
+            (r'(%s)(\s*)(=(?!%s))' % (symbolicid_re, symbolicid_re), 
+             bygroups(Name.Variable, Text, Punctuation), '#pop'), 
+            (r'(%s)' % alphanumid_re, Name.Variable, '#pop'),
+            (r'(%s)' % symbolicid_re, Name.Variable, '#pop'),
+
+            # Ignore interesting patterns like 'val (x, y)'
+            (r'', Text, '#pop'), 
+        ],
+
+        # Dealing with what comes after the 'type' (or 'and') keyword
+        'tname': [
+            include('whitespace'),
+            include('breakout'),
+
+            (r'\'[0-9a-zA-Z_\']*', Name.Decorator),
+            (r'\(', Punctuation, 'tyvarseq'),
+            (r'=(?!%s)' % symbolicid_re, Punctuation, ('#pop', 'typbind')),
+
+            (r'(%s)' % alphanumid_re, Keyword.Type),
+            (r'(%s)' % symbolicid_re, Keyword.Type),
+            (r'\S+', Error, '#pop'),            
+        ],
+
+        # A type binding includes most identifiers
+        'typbind': [
+            include('whitespace'),
+
+            (r'\b(and)\b(?!\')', Keyword.Reserved, ('#pop', 'tname')),
+
+            include('breakout'),
+            include('core'),
+            (r'\S+', Error, '#pop'),            
+        ],
+
+        # Dealing with what comes after the 'datatype' (or 'and') keyword
+        'dname': [
+            include('whitespace'),
+            include('breakout'),
+
+            (r'\'[0-9a-zA-Z_\']*', Name.Decorator),
+            (r'\(', Punctuation, 'tyvarseq'),
+            (r'(=)(\s*)(datatype)', 
+             bygroups(Punctuation, Text, Keyword.Reserved), '#pop'), 
+            (r'=(?!%s)' % symbolicid_re, Punctuation, 
+             ('#pop', 'datbind', 'datcon')),
+
+            (r'(%s)' % alphanumid_re, Keyword.Type),
+            (r'(%s)' % symbolicid_re, Keyword.Type),
+            (r'\S+', Error, '#pop'),            
+        ],
+
+        # common case - A | B | C of int 
+        'datbind': [
+            include('whitespace'),
+
+            (r'\b(and)\b(?!\')', Keyword.Reserved, ('#pop', 'dname')),
+            (r'\b(withtype)\b(?!\')', Keyword.Reserved, ('#pop', 'tname')),
+            (r'\b(of)\b(?!\')', Keyword.Reserved),
+
+            (r'(\|)(\s*)(%s)' % alphanumid_re,
+             bygroups(Punctuation, Text, Name.Class)),
+            (r'(\|)(\s+)(%s)' % symbolicid_re,
+             bygroups(Punctuation, Text, Name.Class)),
+
+            include('breakout'),
+            include('core'),
+            (r'\S+', Error),            
+        ],
+
+        # Dealing with what comes after an exception
+        'ename': [
+            include('whitespace'),
+
+            (r'(exception|and)\b(\s+)(%s)' % alphanumid_re,
+             bygroups(Keyword.Reserved, Text, Name.Class)),
+            (r'(exception|and)\b(\s*)(%s)' % symbolicid_re,
+             bygroups(Keyword.Reserved, Text, Name.Class)),
+            (r'\b(of)\b(?!\')', Keyword.Reserved),
+
+            include('breakout'),
+            include('core'),
+            (r'\S+', Error),            
+        ],
+
+        'datcon': [
+            include('whitespace'),
+            (r'(%s)' % alphanumid_re, Name.Class, '#pop'),
+            (r'(%s)' % symbolicid_re, Name.Class, '#pop'), 
+            (r'\S+', Error, '#pop'),            
+        ],
+
+        # Series of type variables
+        'tyvarseq': [
+            (r'\s', Text),
+            (r'\(\*', Comment.Multiline, 'comment'),
+
+            (r'\'[0-9a-zA-Z_\']*', Name.Decorator),
+            (r',', Punctuation),
+            (r'\)', Punctuation, '#pop'),
+            (r'', Error, '#pop'),            
+        ],
+
+        'comment': [
+            (r'[^(*)]', Comment.Multiline),
+            (r'\(\*', Comment.Multiline, '#push'),
+            (r'\*\)', Comment.Multiline, '#pop'),
+            (r'[(*)]', Comment.Multiline),
+        ],
+    }
+
+
 class OcamlLexer(RegexLexer):
     """
     For the OCaml language.

tests/examplefiles/example.sml

+structure C = struct
+   val a = 12
+   fun f x = x + 5
+end
+
+(*(*(*(*(* This file is all pretty strange Standard ML *)*)*)*) (**)*)
+(* Robert J. Simmons *)
+
+(* Comments (* can be nested *) *)
+structure S = struct
+  val x = (1, 2, "three")
+end
+
+structure Sv = struct
+  (* These look good *)
+  val x = (1, 2, "three")
+  val z = #2 x
+
+  (* Although these look bad (not all the numbers are constants),       *
+   * they never occur in practice, as they are equivalent to the above. *)
+  val x = {1 = 1, 3 = "three", 2 = 2}
+  val z = #
+            2 x
+
+  val || = 12
+end
+
+signature S = sig end
+
+structure S = struct
+  val x = (1, 2, "three")
+  datatype 'a t = T of 'a
+       and u = U of v * v
+  withtype v = {left: int t, right: int t}
+  exception E1 of int and E2
+  fun 'a id (x: 'a) : 'a = x
+
+  val 
+      'a id = fn (x : 'a) => x
+end
+
+signature R = sig
+  type t
+  val x : t
+  val f : t * int -> int
+end
+structure R : R = struct
+  datatype t = T of int
+  val x : t = T 0
+  fun f (T x, i : int) : int = x + i
+  fun 'a id (x: 'a) : 'a = x
+end
+
+signature BA_Z = sig 
+   val s: int
+   include S R
+end 
+
+structure b______ = struct (* What (* A * strange * name *) for ) a ( struct *)
+
+val !%&$#+-/:<=>?@\~`^|* = 3
+
+type struct' = int list
+and 'a sig' = 'a list
+and ('a, 'b) end' = 'b option * 'a list
+
+structure baz = struct
+  structure Bar = struct 
+    val foo = !%&$#+-/:<=>?@\~`^|*
+  end  
+end
+
+infixr +!+ 
+fun (a +!+ b) = (op +) (a, b)
+
+open baz S R
+
+val$$$ = fn x => fn y => fn z => fn w => w
+val (foo, ++, bar, ||) = (4, baz.Bar.foo, !%&$#+-/:<=>?@\~`^|*, Bar.foo)
+val _ = $$$foo++bar||
+
+val val'ue : ' list = []
+val struct3 : (' -> ') = fn x => x
+val end_struct_' : ('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
+
+fun f x y 0 = 4 
+  | f x y z = 4 + Sv.||
+
+exception Foo of int
+datatype ('0, 'b, '_, ') f'o'o = Bar | baZ12' | dsfa_fad | #@$ | Bug
+and (', ''', '''', ''''') bar = 
+   Bee of unit
+ | Ben of (', ''', '''', ''''') f'o'o * int
+ | X of ''' list
+
+fun q x = raise Foo x
+and h x = raise Foo (~x)
+
+val x = 4
+and y = 5
+
+fun q 0 = 4
+  | q 1 = (case 1 of 1 => 2 | 3 => 4 | x => y)
+  | q y = case y of 1 => 2 | 3 => 4 | x => y
+
+val x = ref true
+fun q 0 = 4
+  | q 1 = if false then case 1 of 1 => 2 | 3 => 4 | x => y else 19
+  | q 2 = (while !x handle Match => !x | Fail _ => !x do () ; 2)
+  | q x = (raise Match) handle Domain => 9 | Match => 3
+
+fun p 0 = 12
+  | p 1 = 8
+  | p 2 = r false
+  | p x = r true
+and r true = 19
+  | r false = 12
+
+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 c = #"\000"
+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 *)
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.