(**** FILE: paths.sig ****) (* Paths, Occurrences, and Error Locations *) (* Author: Frank Pfenning *) signature PATHS = sig datatype region = Reg of int * int (* r ::= (i,j) is interval [i,j) *) datatype location = Loc of string * region (* loc ::= (filename, region) *) (* line numbering, used when printing regions *) type linesInfo (* mapping from character positions to lines in a file *) val resetLines : unit -> unit (* reset line numbering *) val newLine : int -> unit (* new line starts at character i *) val getLinesInfo : unit -> linesInfo (* get lines info for current file *) val join : region * region -> region (* join(r1,r2) = smallest region enclosing r1 and r2 *) val toString : region -> string (* line1.col1-line2.col2, parsable by Emacs *) val wrap : region * string -> string (* add region to error message, parsable by Emacs *) val wrapLoc : location * string -> string (* add location to error message, also parsable *) val wrapLoc' : location * linesInfo option * string -> string (* add location to error message in line.col format *) (* Paths, occurrences and occurrence trees only work well for normal forms *) (* In the general case, regions only approximate true source location *) (* Follow path through a term to obtain subterm *) datatype Path = Label of Path (* [x:#] U or {x:#} V *) | Body of Path (* [x:V] # or {x:V} # *) | Head (* # @ S, term in normal form *) | Arg of int * Path (* H @ S1; ...; #; ...; Sn; Nil *) | Here (* #, covers Uni, EVar, Redex(?) *) (* Construct an occurrence when traversing a term. The resulting occurrence can be translated to a region via an occurrence tree stored with the term. An occurrence is a path in reverse order. *) type occ val top : occ val label : occ -> occ val body : occ -> occ val head : occ -> occ val arg : int * occ -> occ (* An occurrence tree is a data structure mapping occurrences in a term to regions in an input stream. Occurrence trees are constructed during parsing. *) type occExp (* occurrence tree for u expressions *) and occSpine (* occurrence tree for s spines *) val leaf : region -> occExp (* could be _ or identifier *) val bind : region * occExp option * occExp -> occExp val root : region * occExp * int * int * occSpine -> occExp val app : occExp * occSpine -> occSpine val nils : occSpine type occConDec (* occurrence tree for constant declarations *) val dec : int * occExp -> occConDec (* (#implicit, v) in c : V *) val def : int * occExp * occExp option -> occConDec (* (#implicit, u, v) in c : V = U *) val toRegion : occExp -> region val toRegionSpine : occSpine * region -> region val posToPath : occExp -> int -> Path val occToRegionExp : occExp -> occ -> region val occToRegionDec : occConDec -> occ -> region (* into v for c : V *) val occToRegionDef1 : occConDec -> occ -> region (* into u for c : V = U *) val occToRegionDef2 : occConDec -> occ -> region (* into v for c : V = U *) end; (* signature PATHS *) (* Stub code to allow sorting checking the parser without including a bunch of other files. *) structure Paths :> PATHS = struct (*[ assumesig PATHS]*) end (**** FILE: 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 *) (* 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 : G|-V, Cnstr *) | EClo of Exp * Sub (* | U[s] *) | AVar of Exp option ref (* | A *) | FgnExp of csid * (* | (foreign expression) *) { toInternal : unit -> Exp, (* convert to internal syntax *) map : (Exp -> Exp) -> Exp, (* apply to subterms *) equalTo : Exp -> bool, (* test for equality *) unifyWith : Dec Ctx * Exp -> FgnUnify (* unify with another term *) } 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 *) | 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] *) and Block = (* Blocks: *) Bidx of int (* b ::= v *) | LVar of Block option ref * (cid * Sub) (* | L(l,s) *) (* | 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 * (* | (foreign) *) { toInternal : unit -> (Dec Ctx * Exp) list, (* convert to internal syntax *) awake : unit -> bool, (* awake *) simplify : unit -> bool (* simplify *) } 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 *) | 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 | SkoDec of string * mid option * int (* sa: K : kind or *) * Exp * Uni (* sc: A : type *) 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 *) 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 : cid * Sub -> Block (* creates B:(l,s) *) (* 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 *) end; (* signature INTSYN *) (* For sort checking, to reduce the number of files required. *) structure IntSyn :> INTSYN = struct (*[ assumesig INTSYN ]*) end (***** FILE: stream.sml *****) (* Stream Library *) (* Author: Frank Pfenning *) (* BASIC_STREAM defines the visible "core" of streams *) signature BASIC_STREAM = sig type 'a stream datatype 'a front = Empty | Cons of 'a * 'a stream (*[ sortdef 'a infStream < stream datasort 'a infFront = Cons of 'a * 'a infStream ]*) (*[ val delay <: (unit -> 'a front) -> 'a stream & (unit -> 'a infFront) -> 'a infStream ]*) (* Lazy stream construction and exposure *) val delay : (unit -> 'a front) -> 'a stream (*[ val expose <: 'a stream -> 'a front & 'a infStream -> 'a infFront ]*) val expose : 'a stream -> 'a front (* Eager stream construction *) val empty : 'a stream (*[ val cons <: 'a * 'a stream -> 'a stream & 'a * 'a infStream -> 'a infStream ]*) val cons : 'a * 'a stream -> 'a stream end; structure BasicStream :> BASIC_STREAM = struct datatype 'a stream = Stream of unit -> 'a front and 'a front = Empty | Cons of 'a * 'a stream (*[ datasort 'a infStream = Stream of unit -> 'a infFront and 'a infFront = Cons of 'a * 'a infStream ]*) (*[ val delay <: (unit -> 'a front) -> 'a stream & (unit -> 'a infFront) -> 'a infStream ]*) fun delay (d) = Stream(d) (*[ val expose <: 'a stream -> 'a front & 'a infStream -> 'a infFront ]*) fun expose (Stream(d)) = d () val empty = Stream (fn () => Empty) (*[ val cons <: 'a * 'a stream -> 'a stream & 'a * 'a infStream -> 'a infStream ]*) fun cons (x, s) = Stream (fn () => Cons (x, s)) end; (* Note that this implementation is NOT semantically *) (* equivalent to the plain (non-memoizing) streams, since *) (* effects will be executed only once in this implementation *) (*structure BasicMemoStream :> BASIC_STREAM = struct datatype 'a stream = Stream of unit -> 'a front and 'a front = Empty | Cons of 'a * 'a stream (*[ datasort 'a infStream = Stream of unit -> 'a infFront and 'a infFront = Cons of 'a * 'a infStream ]*) exception Uninitialized (*[ val delay <: (unit -> 'a front) -> 'a stream & (unit -> 'a infFront) -> 'a infStream ]*) (*[ val expose <: 'a stream -> 'a front & 'a infStream -> 'a infFront ]*) (*[ val cons <: 'a * 'a stream -> 'a stream & 'a * 'a infStream -> 'a infStream ]*) fun expose (Stream (d)) = d () fun 'a delay (d) = let (*[ memo : (*(unit -> 'a front) ref,*) (unit -> 'a infFront) ref ]*) val memo = ref (fn () => raise Uninitialized) fun memoFun () = let val r = d () in ( memo := (fn () => r) ; r ) end handle exn => ( memo := (fn () => raise exn) ; raise exn ) in memo := memoFun ; (Stream (*[ <: (unit -> 'a infFront) -> 'a infStream ]*)) (fn () => !memo () (*[ <: unit -> 'a infFront ]*)) end val empty = Stream (fn () => Empty) fun cons (x, s) = Stream (fn () => Cons (x, s)) end; *) (* STREAM extends BASIC_STREAMS by operations *) (* definable without reference to the implementation *) signature STREAM = sig include BASIC_STREAM exception EmptyStream val null : 'a stream -> bool val hd : 'a stream -> 'a val tl : 'a stream -> 'a stream val map : ('a -> 'b) -> 'a stream -> 'b stream val filter : ('a -> bool) -> 'a stream -> 'a stream val exists : ('a -> bool) -> 'a stream -> bool val take : 'a stream * int -> 'a list val drop : 'a stream * int -> 'a stream val fromList : 'a list -> 'a stream val toList : 'a stream -> 'a list val tabulate : (int -> 'a) -> 'a stream end; functor Stream (structure BasicStream : BASIC_STREAM) :> STREAM = struct open BasicStream exception EmptyStream (* functions null, hd, tl, map, filter, exists, take, drop *) (* parallel the functions in the List structure *) fun null (s) = null' (expose s) and null' (Empty) = true | null' (Cons _) = false fun hd (s) = hd' (expose s) and hd' (Empty) = raise EmptyStream | hd' (Cons (x,s)) = x fun tl (s) = tl' (expose s) and tl' (Empty) = raise EmptyStream | tl' (Cons (x,s)) = s fun map f s = delay (fn () => map' f (expose s)) and map' f (Empty) = Empty | map' f (Cons(x,s)) = Cons (f(x), map f s) fun filter p s = delay (fn () => filter' p (expose s)) and filter' p (Empty) = Empty | filter' p (Cons(x,s)) = if p(x) then Cons (x, filter p s) else filter' p (expose s) fun exists p s = exists' p (expose s) and exists' p (Empty) = false | exists' p (Cons(x,s)) = p(x) orelse exists p s fun takePos (s, 0) = nil | takePos (s, n) = take' (expose s, n) and take' (Empty, _) = nil | take' (Cons(x,s), n) = x::takePos(s, n-1) fun take (s,n) = if n < 0 then raise Subscript else takePos (s,n) fun fromList (nil) = empty | fromList (x::l) = cons(x,fromList(l)) fun toList (s) = toList' (expose s) and toList' (Empty) = nil | toList' (Cons(x,s)) = x::toList(s) fun dropPos (s, 0) = s | dropPos (s, n) = drop' (expose s, n) and drop' (Empty, _) = empty | drop' (Cons(x,s), n) = dropPos (s, n-1) fun drop (s,n) = if n < 0 then raise Subscript else dropPos (s,n) fun tabulate f = delay (fn () => tabulate' f) and tabulate' f = Cons (f(0), tabulate (fn i => f(i+1))) end; (* structure Stream :> STREAM --- non-memoizing *) structure Stream :> STREAM = Stream (structure BasicStream = BasicStream); (* structure MStream :> STREAM --- memoizing *) (*structure MStream :> STREAM = Stream (structure BasicStream = BasicMemoStream); *) (* structure S = Stream; (* abbreviation *) (* simple definition *) fun ones' () = S.Cons(1, S.delay ones'); val ones = S.delay ones'; (* alternative definitions *) val ones = S.tabulate (fn _ => 1); val nats = S.tabulate (fn i => i); val poss = S.map (fn i => i+1) nats; val evens = S.map (fn i => 2*i) nats; (* notMultiple p q >=> true iff q is not a multiple of p *) fun notMultiple p q = (q mod p <> 0); fun sieve s = S.delay (fn () => sieve' (S.expose s)) and sieve' (S.Empty) = S.Empty | sieve' (S.Cons(p, s)) = S.Cons (p, sieve (S.filter (notMultiple p) s)); val primes = sieve (S.tabulate (fn i => i+2)); *) (***** FILE: lexer.sig *****) (* Lexer *) (* Author: Frank Pfenning *) signature LEXER = sig (* Stream is not memoizing for efficiency *) structure Stream : STREAM (*! structure Paths : PATHS !*) datatype IdCase = Upper (* [A-Z] or _ *) | Lower (* any other *) | Quoted (* '', currently unused *) datatype Token = EOF (* end of file or stream, also `%.' *) | DOT (* `.' *) | PATHSEP (* `.' between s *) | COLON (* `:' *) | LPAREN | RPAREN (* `(' `)' *) | LBRACKET | RBRACKET (* `[' `]' *) | LBRACE | RBRACE (* `{' `}' *) | BACKARROW | ARROW (* `<-' `->' *) | TYPE (* `type' *) | EQUAL (* `=' *) | ID of IdCase * string (* identifer *) | UNDERSCORE (* `_' *) | INFIX | PREFIX | POSTFIX (* `%infix' `%prefix' `%postfix' *) | NAME (* `%name' *) | DEFINE (* `%define' *) (* -rv 8/27/01 *) | SOLVE (* `%solve' *) | QUERY (* `%query' *) | QUERYTABLED (* `%querytabled' *) | MODE (* `%mode' *) | COVERS (* `%covers' *) (* -fp 3/7/01 *) | TOTAL (* `%total' *) (* -fp 3/18/01 *) | TERMINATES (* `%terminates' *) | BLOCK (* `%block' *) (* -cs 5/29/01 *) | WORLDS (* `%worlds' *) | REDUCES (* `%reduces' *) (* -bp 6/5/99 *) | TABLED (* `%tabled' *) (* -bp 6/5/99 *) | THEOREM (* `%theorem' *) | PROVE (* `%prove' *) | ESTABLISH (* `%establish' *) | ASSERT (* `%assert' *) | ABBREV (* `%abbrev' *) | FREEZE (* `%freeze' *) | DETERMINISTIC (* `%deterministic' *) (* -rv 11/27/01 *) | CLAUSE (* `%clause' *) (* -fp 8/9/02 *) | SIG (* `%sig' *) | STRUCT (* `%struct' *) | WHERE (* `%where' *) | INCLUDE (* `%include' *) | OPEN (* `%open' *) | USE (* `%use' *) | STRING of string (* string constants *) (*[ datasort idToken = ID of IdCase * string ]*) exception Error of string (* lexer returns an infinite stream, terminated by EOF token *) val lexStream : TextIO.instream -> (Token * Paths.region) Stream.stream val lexTerminal : string * string -> (Token * Paths.region) Stream.stream val toString : Token -> string (* Utilities *) exception NotDigit of char val stringToNat : string -> int val isUpper : string -> bool end; (* signature LEXER *) (* Stub code to allow sorting checking the parser without including a bunch of other files. *) structure Lexer :> LEXER = struct (*[ assumesig LEXER ]*) end (***** FILE: parsing.sig *****) (* General basis for parsing modules *) (* Author: Frank Pfenning *) signature PARSING = sig (* structure Stream : STREAM *) (* structure Lexer : LEXER sharing Lexer.Stream = Stream *) type lexResult = Lexer.Token * Paths.region type 'a parser = lexResult Stream.front -> 'a * lexResult Stream.front (* sortdef 'a parser = lexResult Stream.infFront -> 'a * lexResult Stream.infFront *) (* recursive parser (allows parsing functions that need to parse a signature expression to temporarily suspend themselves) *) datatype 'a RecParseResult = Done of 'a | Continuation of 'a RecParseResult parser type 'a recparser = 'a RecParseResult parser (* useful combinator for recursive parsers *) val recwith : 'a recparser * ('a -> 'b) -> 'b recparser exception Error of string val error : Paths.region * string -> 'a (* always raises Error *) end; (* signature PARSING *) (* Stub code to allow sorting checking the parser without including a bunch of other files. *) structure Parsing :> PARSING = struct (*[ assumesig PARSING ]*) end (***** FILE: names.sig *****) (* Names of Constants and Variables *) (* Author: Frank Pfenning *) (* Modified: Jeff Polakow *) signature FIXITY = sig datatype associativity = Left | Right | None datatype precedence = Strength of int val maxPrec : precedence val minPrec : precedence val less : precedence * precedence -> bool val leq : precedence * precedence -> bool val compare : precedence * precedence -> order val inc : precedence -> precedence val dec : precedence -> precedence datatype fixity = Nonfix | Infix of precedence * associativity | Prefix of precedence | Postfix of precedence val prec : fixity -> precedence val toString : fixity -> string end; (* signature FIXITY *) signature NAMES = sig (*! structure IntSyn : INTSYN !*) exception Error of string exception Unprintable structure Fixity : FIXITY (* Constant names and fixities *) datatype Qid = Qid of string list * string val qidToString : Qid -> string val stringToQid : string -> Qid option val unqualified : Qid -> string option type namespace val newNamespace : unit -> namespace val insertConst : namespace * IntSyn.cid -> unit (* shadowing disallowed *) val insertStruct : namespace * IntSyn.mid -> unit (* shadowing disallowed *) val appConsts : (string * IntSyn.cid -> unit) -> namespace -> unit val appStructs : (string * IntSyn.mid -> unit) -> namespace -> unit val reset : unit -> unit val resetFrom : IntSyn.cid * IntSyn.mid -> unit (* The following functions have to do with the mapping from names to cids/mids only. *) val installConstName : IntSyn.cid -> unit val installStructName : IntSyn.mid -> unit val constLookup : Qid -> IntSyn.cid option val structLookup : Qid -> IntSyn.mid option val constUndef : Qid -> Qid option (* shortest undefined prefix of Qid *) val structUndef : Qid -> Qid option val constLookupIn : namespace * Qid -> IntSyn.cid option val structLookupIn : namespace * Qid -> IntSyn.mid option val constUndefIn : namespace * Qid -> Qid option val structUndefIn : namespace * Qid -> Qid option (* This function maps cids/mids to names. It uses the information in the IntSyn.ConDec or IntSyn.StrDec entries only, and only considers the name->cid/mid mapping defined above in order to tell whether a name is shadowed (any constant or structure whose canonical name would map to something else, or to nothing at all, in the case of an anonymous structure, is shadowed). *) val conDecQid : IntSyn.ConDec -> Qid val constQid : IntSyn.cid -> Qid (* will mark if shadowed *) val structQid : IntSyn.mid -> Qid (* will mark if shadowed *) val installFixity : IntSyn.cid * Fixity.fixity -> unit val getFixity : IntSyn.cid -> Fixity.fixity val fixityLookup : Qid -> Fixity.fixity (* Nonfix if undefined *) (* Name preferences for anonymous variables: a, EPref, UPref *) val installNamePref : IntSyn.cid * (string * string option) -> unit val getNamePref : IntSyn.cid -> (string * string) option val installComponents : IntSyn.mid * namespace -> unit val getComponents : IntSyn.mid -> namespace (* EVar and BVar name choices *) val varReset : IntSyn.dctx -> unit (* context in which EVars are created *) val addEVar : IntSyn.Exp * string -> unit (* assumes name not already used *) val getEVarOpt : string -> IntSyn.Exp option (* NONE, if undefined or not EVar *) val evarName : IntSyn.dctx * IntSyn.Exp -> string (* create, if undefined *) val bvarName : IntSyn.dctx * int -> string (* raises Unprintable if undefined *) val decName : IntSyn.dctx * IntSyn.Dec -> IntSyn.Dec (* status unknown, like decEName *) val decEName : IntSyn.dctx * IntSyn.Dec -> IntSyn.Dec (* assign existential name *) val decUName : IntSyn.dctx * IntSyn.Dec -> IntSyn.Dec (* assign universal name *) val decLUName: IntSyn.dctx * IntSyn.Dec -> IntSyn.Dec (* assign local universal name *) val ctxName : IntSyn.dctx -> IntSyn.dctx (* assign global existential names *) val ctxLUName: IntSyn.dctx -> IntSyn.dctx (* assign local universal names *) val nameConDec : IntSyn.ConDec -> IntSyn.ConDec (* Skolem constants *) val skonstName : string -> string (* Named EVars, used for queries *) val namedEVars : unit -> (IntSyn.Exp * string) list (* Uninstantiated named EVars with constraints *) val evarCnstr : unit -> (IntSyn.Exp * string) list end; (* signature NAMES *) (***** FILE: recon-term.sig *****) (* External Syntax and Type Reconstruction *) (* Author: Frank Pfenning *) (* signature EXTSYN provides the interface for type reconstruction as seen by the parser *) signature EXTSYN = sig (*! structure Paths : PATHS !*) type term (* term *) type dec (* variable declaration *) val lcid : string list * string * Paths.region -> term (* lower case id *) val ucid : string list * string * Paths.region -> term (* upper case id *) val quid : string list * string * Paths.region -> term (* quoted id, currently not parsed *) val scon : string * Paths.region -> term (* string constant *) (* unconditionally interpreted as such *) val evar : string * Paths.region -> term val fvar : string * Paths.region -> term val typ : Paths.region -> term (* type, region for "type" *) val arrow : term * term -> term (* tm -> tm *) val backarrow : term * term -> term (* tm <- tm *) val pi : dec * term -> term (* {d} tm *) val lam : dec * term -> term (* [d] tm *) val app : term * term -> term (* tm tm *) val hastype : term * term -> term (* tm : tm *) val omitted : Paths.region -> term (* _ as object, region for "_" *) (* region for "{dec}" "[dec]" etc. *) val dec : string option * term * Paths.region -> dec (* id : tm | _ : tm *) val dec0 : string option * Paths.region -> dec (* id | _ (type omitted) *) end; (* signature EXTSYN *) (* signature RECON_TERM provides the interface to type reconstruction seen by Twelf *) signature RECON_TERM = sig (*! structure IntSyn : INTSYN !*) include EXTSYN exception Error of string val resetErrors : string -> unit (* filename -fp *) val checkErrors : Paths.region -> unit datatype TraceMode = Progressive | Omniscient val trace : bool ref val traceMode : TraceMode ref (* Reconstruction jobs *) type job val jnothing : job val jand : job * job -> job val jwithctx : dec IntSyn.Ctx * job -> job val jterm : term -> job val jclass : term -> job val jof : term * term -> job datatype Job = JNothing | JAnd of Job * Job | JWithCtx of IntSyn.Dec IntSyn.Ctx * Job | JTerm of (IntSyn.Exp * Paths.occExp) * IntSyn.Exp * IntSyn.Uni | JClass of (IntSyn.Exp * Paths.occExp) * IntSyn.Uni | JOf of (IntSyn.Exp * Paths.occExp) * (IntSyn.Exp * Paths.occExp) * IntSyn.Uni val recon : job -> Job val reconQuery : job -> Job val termRegion : term -> Paths.region val decRegion : dec -> Paths.region val ctxRegion : dec IntSyn.Ctx -> Paths.region option (* unimplemented for the moment *) val internalInst : 'a -> 'b val externalInst : 'a -> 'b end; (* signature RECON_TERM *) (***** FILE: parse-term.sig *****) (* Parsing Terms and Declarations *) (* Author: Frank Pfenning *) (* Sorts added by: Rowan Davies *) signature PARSE_TERM = sig (*! structure Parsing : PARSING !*) structure ExtSyn : EXTSYN val parseQualId' : (string list * Parsing.lexResult) Parsing.parser val parseQualIds' : ((string list * string) list) Parsing.parser val parseFreeze' : ((string list * string) list) Parsing.parser val parseDeterministic' : ((string list * string) list) Parsing.parser val parseTerm' : ExtSyn.term Parsing.parser val parseDec' : (string option * ExtSyn.term option) Parsing.parser val parseCtx' : (ExtSyn.dec list) Parsing.parser (* To specify the refinements for these functions, we need to expand the uses of Parsing.parser, since the sort checker currently does not support transparent sort specs in signatures (although it does support transparent datasort specs). *) (* Here are the value specifications with Parsing.parser expanded, just for comparison with the value sort specifications below. *) (* val parseQualId' : Parsing.lexResult Stream.front -> (string list * Parsing.lexResult) * Parsing.lexResult Stream.front val parseQualIds' : Parsing.lexResult Stream.front -> ((string list * string) list) * Parsing.lexResult Stream.front val parseFreeze' : Parsing.lexResult Stream.front -> ((string list * string) list) * Parsing.lexResult Stream.front val parseDeterministic' : Parsing.lexResult Stream.front -> ((string list * string) list) * Parsing.lexResult Stream.front val parseTerm' : Parsing.lexResult Stream.front -> ExtSyn.term * Parsing.lexResult Stream.front val parseDec' : Parsing.lexResult Stream.front -> (string option * ExtSyn.term option) * Parsing.lexResult Stream.front val parseCtx' : Parsing.lexResult Stream.front -> (ExtSyn.dec list) * Parsing.lexResult Stream.front *) (* Here are the corresponding sorts, using the refinement infFront of front for infinite streams, i.e. ones that are guaranteed not to ever reach nil. *) (*[ val parseQualId' <: Parsing.lexResult Stream.infFront -> (string list * (Lexer.idToken * Paths.region)) * Parsing.lexResult Stream.infFront val parseQualIds' <: Parsing.lexResult Stream.infFront -> ((string list * string) list) * Parsing.lexResult Stream.infFront val parseFreeze' <: Parsing.lexResult Stream.infFront -> ((string list * string) list) * Parsing.lexResult Stream.infFront val parseDeterministic' <: Parsing.lexResult Stream.infFront -> ((string list * string) list) * Parsing.lexResult Stream.infFront val parseTerm' <: Parsing.lexResult Stream.infFront -> ExtSyn.term * Parsing.lexResult Stream.infFront val parseDec' <: Parsing.lexResult Stream.infFront -> (string option * ExtSyn.term option) * Parsing.lexResult Stream.infFront val parseCtx' <: Parsing.lexResult Stream.infFront -> (ExtSyn.dec list) * Parsing.lexResult Stream.infFront ]*) end; (* signature PARSE_TERM *)