(* AUTOMATICALLY GENERATED BY src/sdml/silly *) (* DO NOT EDIT THIS FILE -- edit Stardust.silly.grm instead *) (* StardustML grammar *) (* Uses preprocessing directives removed by the `silly' script, *) (* which you need to run by hand* after editing this file. *) (* * or with: OS.Process.system "cd sdml;./silly"; *) val {dprint, dprnt} = Debug.register {full_name= "grammar", short_name= "grammar"} local val index = Option.valOf (Debug.from "grammar") in fun fail s = Debug.makeFail index s end open Sdml structure CC = Sdml.ConcreteContext structure F = Fixity structure X = Indexing val decslevel = ref 0 fun mungeEnvForFwdRef env string = ( (* print ("mungeEnvForFwdRef " ^ string ^ "\n"); *) case ParseLib.Pvar.lookup_soft env string of NONE => () | SOME (ParseLib.Ordvar (_, pvstatus as ref ParseLib.Neutral), pv) => let val _ = "Declared but undefined variable: this is a forward reference:" val _ = " change it to `FutureFun'." val _ = dprnt "Neutral (---> FutureFun)" in pvstatus := ParseLib.FutureFun end | SOME (ParseLib.Ordvar (_, ref ParseLib.FutureFun), pv) => dprnt "FutureFun" | SOME (ParseLib.Ordvar (_, ref ParseLib.DefinedFun), pv) => dprnt "DefinedFun" | SOME (ParseLib.Ordvar (_, ref ParseLib.DefinedVal), pv) => dprnt "DefinedVal" | SOME (ParseLib.Convar, pv) => dprnt "Convar" ) (* Valid sequences of declarations: anything of the form val* fun* val* with all other declarations arbitrarily interspersed. *) fun check_decs ds = let fun applyFix f x = ( (* print (Print.p Print.printDecs x ^ "\n"); *) case f x of SOME x' => applyFix f x' | NONE => x ) fun rotateValsOverFuns [] = NONE | rotateValsOverFuns ((d1 as (_, Dec(_, ValKW, _))) :: (d2 as (_, Dec(_, FunKW, _))) :: ds) = (SOME (d2 :: d1 :: ds)) | rotateValsOverFuns (d :: ds) = let in case rotateValsOverFuns ds of NONE => NONE | SOME ds => SOME (d :: ds) end fun check0 [] = [] | check0 ((d as (_, Dec(_,ValKW,_))) :: ds) = d :: check2 ds | check0 ((d as (_, Dec(_,FunKW,_))) :: ds) = d :: check1 ds | check0 (d :: ds) = d :: check0 ds and check1 [] = [] | check1 ((d as (_, Dec(_,ValKW,_))) :: ds) = d :: check2 ds | check1 ((d as (_, Dec(_,FunKW,_))) :: ds) = d :: check1 ds | check1 (d :: ds) = d :: check1 ds and check2 [] = [] | check2 ((d as (_, Dec(_,ValKW,_))) :: ds) = d :: check2 ds | check2 ((d as (_, Dec(_,FunKW,_))) :: _) = raise Option | check2 (d :: ds) = d :: check2 ds val check = check0 val _ = dprint (fn () => Print.p Print.printDecs ds) val rotated_ds = applyFix rotateValsOverFuns ds val _ = dprint (fn () => Print.p Print.printDecs rotated_ds) in ((*check*) rotated_ds) handle Option => (print ("Declarations invalid: `val' mixed with block of `fun's\n"); raise Option) end fun var'n'fix env s errexp = let val (info, pv) = ParseLib.Pvar.lookup errexp env s val f = pv in (case info of ParseLib.Convar => Con pv | ParseLib.Ordvar _ => Var pv, f) end (* cf. Definition of Standard ML, p. 72, and http://www.standardml.org/Basis/top-level-chapter.html *) fun fixityfn pv = case PV.proper_name pv of "*" => F.infixleft 7 | "/" => F.infixleft 7 | "div" => F.infixleft 7 | "mod" => F.infixleft 7 | "+" => F.infixleft 6 | "-" => F.infixleft 6 | "^" => F.infixleft 6 | "<" => F.infixleft 4 | ">" => F.infixleft 4 | "<=" => F.infixleft 4 | ">=" => F.infixleft 4 | "<>" => F.infixleft 4 | "=" => F.infixleft 4 | _ => F.NONfix fun unflatten locexps = let fun applyFn ((loc1,e1), (loc2, e2)) = let val loc = Location.span loc1 loc2 in (loc, let in case e1 of Con c => Conapp(c, (loc2,e2)) | _ => App((loc1,e1), (loc2,e2)) end) end fun pairFn ((loc1,e1), (loc2,e2)) = (Location.span loc1 loc2, Tuple[(loc1,e1), (loc2,e2)]) val locexp = Precedence.parse PV.proper_name {apply= applyFn, pair= pairFn} (locexps, fixityfn) in locexp end val X_var'n'fix = let fun X_var'n'fix env s errexp = let val (iv, syminfo) = ParseLib.lookup_iv errexp env s (* val xxx = print ("`" ^ s ^ "' X_var'n'fix " ^ IndexSym.toString iv ^ "\n") *) val f = iv (* case ParseLib.Pvar.lookup_soft env (IndexSym.toShortString iv) of SOME (_, f) => f | NONE => ~1 *) val exp = case syminfo of X.IUVar _ => X.Uvar iv | X.IEVar _ => X.Evar iv | X.INil _ => X.Nil iv | X.ITrue => X.True | X.IFalse => X.False | X.INODIM => X.NODIM | X.IBaseDim => X.BaseDim iv | X.IFun _ => X.Uvar iv (* bogus? *) in (exp, f) end in X_var'n'fix : (ParseLib.env -> string -> (string -> unit) -> (Indexing.exp * IndexSym.sym)) end fun X_fixityfn iv = case IndexSym.toShortString iv of "+" => F.infixleft 6 | "-" => F.infixleft 6 | "*" => F.infixleft 7 | "/" => F.infixleft 7 | "<" => F.infixleft 4 | ">" => F.infixleft 4 | "<=" => F.infixleft 4 | ">=" => F.infixleft 4 | "<>" => F.infixleft 4 | "=" => F.infixleft 4 (* XXX don't have Definition with me right now; is this right? *) (* | "/\\" => F.infixleft 3 (* XXX *) | "\\/" => F.infixleft 3 (* XXX *) *) | "^" => F.infixright 8 (* power; probably inconsistent with ^ operator in ML, but that's string concatenation, so who's counting? *) | _ => F.NONfix fun X_unflatten exps = let fun applyFn (e1, e2) = let in case e1 of X.Uvar v => X.App(v, e2) | _ => (print ("X_unflatten dying on index expression ``" ^ X.Exp.toString e1 ^ "'' \n"); raise Option) end val exp = Precedence.parse (IndexSym.toString) {apply= applyFn, pair= fn (e1, e2) => (X.Tuple [e1, e2]) } (exps, X_fixityfn) in exp end structure Stringdec = struct datatype t = (* Dec of (string * PV.sym) * (ParseLib.env -> Sdml.locexp) | *) ValType of (string * PV.sym) * Dectype.dectype | Datacon of (string * PV.sym) * (ParseLib.env -> Sdml.texp) | TyvarVariance of string * Sdml.Variance.t | DatatypeWith of string * Indexing.Sorting.t type loct = Location.location * t fun getVariance defaultVariance tvname stringdecs = let val self = getVariance defaultVariance tvname in case stringdecs of [] => defaultVariance | (loc, TyvarVariance (tvname', variance)) :: rest => if tvname = tvname' then variance else self rest | _ :: rest => self rest end fun getSorting tcname stringdecs = case stringdecs of [] => X.Sorting.None | (loc, DatatypeWith (tcname', sorting)) :: rest => if tcname = tcname' then sorting else getSorting tcname rest | _ :: rest => getSorting tcname rest fun frobDatacon env stringdec = case stringdec of (loc, Datacon ((string, pv), texpSusp)) => SOME (string, (pv, texpSusp env)) | _ => NONE fun getValtypes stringdecs = List.mapPartial (fn (loc, ValType ((_, pv), dectype)) => SOME (loc, Sdml.ValType(pv, dectype)) | _ => NONE) stringdecs fun getValtype stringdecs string = let val matches = List.mapPartial (fn (loc, ValType ((string', pv), dectype)) => if string = string' then SOME (pv, dectype) else NONE | _ => NONE) stringdecs in case matches of [] => NONE | [onlyMatch] => SOME onlyMatch | multipleMatches => fail ("Multiple type annotations for same val " ^ string) end val getValtype = getValtype : loct list -> string -> (PV.sym * Dectype.dectype) option end (* structure StringDec *) fun buildSynonym env ((*typbind*) list : (TC.sym * (ParseLib.env -> (((string * TV.sym) list * texp)))) list) location = let val (tcs, infos) = (ListPair.unzip list) : TC.sym list * (ParseLib.env -> (((string * TV.sym) list * texp))) list val (bindings, algFns) = ListPair.unzip (List.map (fn (tc, entry) => let val fresh_tv = TV.fresh (TC.toShortString tc) in ((TC.toShortString tc, ParseLib.TypeSynonym (tc, fresh_tv)) , fn env => let val (params, texp) = entry env val (paramNames, paramTVs) = ListPair.unzip params in Sdml.Synonym{tc= tc, tv= fresh_tv, params= paramTVs, definition= texp} end ) end) list) val withTCs = ParseLib.Type.extend env bindings val typedecs = List.map (fn f => f withTCs) algFns val result = [(location, Typedec typedecs)] : decs in (withTCs, result) : ParseLib.env * decs end %% %verbose %pos int %name Sdml %nonassoc WITHTYPE %right HANDLE COMMA AND DARROW %left SEMICOLON RBRACE MINUS AMP DBLAMP RAISE ANDALSO ORELSE DBLCOLON ELSE %right ARROW %left EQUALOP PLUS ASTERISK RBRACK SLASH DBLSLASH DQUESTION %nonassoc COLON %term EOF | ID of string | TYVAR of string | INT of string | REAL of string | STRING of string | CHAR of string | AND | ANDALSO | AS | CASE | DATACON | DATASORT | DATATYPE | DO | ELSE | END | FN | FUN | HANDLE | IF | IN | INDEXCONSTANT | INDEXFUN | INDEXPRED | INDEXSORT | LET | LETHINT | LOCAL | NOT | OF | OP | ORELSE | PRIMITIVE | RAISE | REC | TESTSUBTYPE | THEN | TRY | TYPE | UNIT | VAL | WHERE | WITH | WITHTYPE | ANTICOLON | APOSTROPHE | ARROW | ASTERISK | BAR | COLON | COMMA | DARROW | DBLCOLON | DBLCOMMA | DQUESTION | EQUALOP (* var. EQUALOP *) | HASH | LBRACE | RBRACE | LBRACK | RBRACK | LPAREN | RPAREN | MINUS | PLUS | SEMICOLON | TURNSTILE | WILD | SOME (* "some" *) | PERIOD (* "." *) | LEFTANNO (* >:> *) | TOP | BOT | AMP | SLASH | DBLAMP | DBLSLASH | DASHALL | DASHEXISTS %nonterm tcname of string | id of string | idcon of string | idw of string | optionalsemicolon of unit | in_or_notin of Sdml.testsubtype_sense | program of ParseLib.env * decs -> ParseLib.env * program | typbind of (TC.sym * (ParseLib.env -> (string * TV.sym) list * texp)) list | AND_typbind_opt of (TC.sym * (ParseLib.env -> (string * TV.sym) list * texp)) list | variancesymbol of Sdml.Variance.t | nativename of string option | indexrecordspec of ParseLib.env -> ParseLib.env * (X.fieldname * X.Sorting.spec) list | indexspec of ParseLib.env -> ParseLib.env * X.Sorting.t | defaultindexspec of ParseLib.env -> X.exp option | dec of ParseLib.env -> (ParseLib.env * decs) | decs of ParseLib.env -> (ParseLib.env * decs) (* | decsunchecked of ParseLib.env -> (ParseLib.env * decs) *) (* | trailer of (pos * pos) * ParseLib.env -> locexp *) | synonymtypbind of ParseLib.env -> ParseLib.env * decs | valdec of ParseLib.env -> ParseLib.env * locdec list | valtypedec of ParseLib.env -> ParseLib.env * locdec | fdec of ParseLib.env -> ParseLib.env * locdec | fdef of ParseLib.env -> locexp | colonoranticolon of Sdml.annotation -> Dectype.dectype (* 0 exp ::= expA | fn x => exp 10 expA ::= expB | expA ,, expB 15 expB ::= expC | d >:> expB 20 expC ::= expD | case expD of (... => expD)* 40 expD ::= expI | expI ; expD 60 expI ::= expR | if expR then expI else expI 70 expR ::= raise expS | expS (andalso expS)* | expS (orelse expS)* (eventually; right now, just expS andalso expS | expS orelse expS) 80 expS ::= expZ | expZ : annotation | ?? expZ | try exp handle id => exp end 100 expZ ::= app_exp 100 app_exp *) | exp of ParseLib.env -> locexp | expA of ParseLib.env -> locexp | expB of ParseLib.env -> locexp | expC of ParseLib.env -> locexp | expD of ParseLib.env -> locexp | expI of ParseLib.env -> locexp | expR of ParseLib.env -> locexp | expS of ParseLib.env -> locexp | expZ of ParseLib.env -> locexp | recordexp_component of ParseLib.env -> locexp | recordexp_component_list of ParseLib.env -> locexp list | record_component of ParseLib.env -> ParseLib.env * texp | record_component_list of ParseLib.env -> ParseLib.env * (texp list) | exp_2c of (ParseLib.env -> locexp) list | exp_list of (ParseLib.env -> locexp) list | app_exp of ParseLib.env -> (locexp, PV.sym) fixitem list | aexp of ParseLib.env -> locexp | arms of (ParseLib.env -> arm) list | arm of ParseLib.env -> arm | pattern of ParseLib.env -> ParseLib.env * pattern | patternl of ParseLib.env -> ParseLib.env * pattern list | patternlz of ParseLib.env -> ParseLib.env * pattern list | atpattern of ParseLib.env -> ParseLib.env * pattern (* | atpatternl of ParseLib.env -> ParseLib.env * pattern list *) | stringseq of string | stringopt of string option | idl of string list | ids of string list (* | exp_2comma_leftassoc of ParseLib.env -> locexp list *) | proposition of ParseLib.env -> X.constraint | tyvarseq of string list | tyvarvariance of string * Sdml.Variance.t | tyvarvarianceseq of (string * Sdml.Variance.t) list | tyvars of string list (* texp ::= -all- texp | texpI texpI ::= texpC & ... texpC ::= texpD -> ... texpD ::= -exists- [P] ... texpE texpE ::= texpU * ... texpU ::= texpY \/ ... texpY ::= {{P}} texp | {record} | texpZ texpZ ::= atomictexp texpl (texpl may be empty) atomictexp ::= tycon indexrefinement | () | top | bot | ( texp ) *) | texp of ParseLib.env -> (ParseLib.env * texp) | texpI of ParseLib.env -> (ParseLib.env * texp) | texpC of ParseLib.env -> (ParseLib.env * texp) | texpD of ParseLib.env -> (ParseLib.env * texp) | texpE of ParseLib.env -> (ParseLib.env * texp list) | texpU of ParseLib.env -> (ParseLib.env * texp) | texpY of ParseLib.env -> (ParseLib.env * texp) | texpZ of ParseLib.env -> (ParseLib.env * texp) | atomictexp of ParseLib.env -> (ParseLib.env * texp) | dashalltail of ParseLib.env -> (ParseLib.env * texp) | texpl of ParseLib.env -> (ParseLib.env * texp list) (* | texps of ParseLib.env -> (ParseLib.env * texp list) *) | commaids of string list | commatyvars of string list | indexrefinement of ParseLib.env -> X.record (* | indexfield of ParseLib.env -> (IndexFieldName.sym * X.exp) | indexfields of ParseLib.env -> (IndexFieldName.sym * X.exp) list *) | sort of ParseLib.env -> X.sort | sort0 of ParseLib.env -> X.sort | sprodel of ParseLib.env -> X.sort list | X_exp of ParseLib.env -> X.exp | X_appexp of ParseLib.env -> (X.exp, IndexSym.sym) fixitem list | X_aexp of ParseLib.env -> X.exp | X_exp_2c of (ParseLib.env -> X.exp) list | X_explist0 of (ParseLib.env -> X.exp) list | X_explist of ParseLib.env -> X.exp (* | typedec of ParseLib.env -> (string * Dectype.dectype) | typedeczzz of ParseLib.env -> Dectype.dectype *) | datasortpair of string * string | datasortpairs of (string * string) list | primdec of ParseLib.env -> ParseLib.env | complement of ParseLib.env -> IndexSym.sym option | indexfunctioncomponent of ParseLib.env -> {domain:X.sort, range:X.sort, complement:IndexSym.sym option} | indexfunctionspec of ParseLib.env -> {domain:X.sort, range:X.sort, complement:IndexSym.sym option} list | indexpredspec of ParseLib.env -> {domain:X.sort} list (* ITRS '12-style *) | annotationtype of ParseLib.env -> ParseLib.env * annotype | annotationtypelist of ParseLib.env -> ParseLib.env * annotype list (* Contextual typing annotations *) (* | ccelem of ParseLib.env -> ParseLib.env * ConcreteContext.elem | ccelemlist of ParseLib.env -> ParseLib.env * ConcreteContext.elem list | concrete_ctxt of ParseLib.env -> ParseLib.env * concrete_ctxt | typing of ParseLib.env -> typing | typinglist of ParseLib.env -> typing list *) | ctxanno of ParseLib.env -> annotation %arg (argument) : (pos * pos -> string -> unit) * (pos -> pos -> Location.location) * (pos -> pos -> Sdml.exp -> Sdml.locexp) %start program %eop EOF %noshift EOF %% program: decs (decslevel := 0; ( fn (env, library_decs) => let val _ = decslevel := 0 val (env, decs') = decs env val trailerexp = (#3(argument)) decsright decsright (Tuple []) val locexp = (#3(argument)) decsleft decsright (Let (library_decs @ decs', trailerexp)) in (env, Program (ParseLib.get_libinfo env, [], locexp)) end)) optionalsemicolon: SEMICOLON (()) | (()) in_or_notin: IN (IsSubtype) | NOT IN (IsNotSubtype) | EQUALOP (MutualSubtypes) defaultindexspec: EQUALOP X_exp (fn env => SOME (X_exp env)) | (fn env => NONE) indexrecordspec: ID COLON sort defaultindexspec indexrecordspec (fn env => let val fld = IndexFieldName.fresh ID val env = ParseLib.extend_fields env [(ID, (fld, ()))] val (env, rest) = indexrecordspec env in (env, (fld, (sort env, defaultindexspec env)) :: rest) end ) | (fn env => (env, [])) indexspec: WITH indexrecordspec (fn env => let val (env, irs) = indexrecordspec env in (env, X.Sorting.Fields irs) end) | WITH sort defaultindexspec (fn env => (env, X.Sorting.Nameless (sort env, defaultindexspec env))) | (fn env => (env, X.Sorting.None)) typbind: tyvarseq tcname EQUALOP texp AND_typbind_opt (let val tyvar_names = tyvarseq : string list val tc = TC.fresh tcname in (tc, fn env => let val tvbindings = ListPair.zip (tyvar_names, List.map TV.fresh tyvar_names) val withTVs = ParseLib.Tyvar.extend env tvbindings val (_, parsed_texp) = texp withTVs in (tvbindings, parsed_texp) end) :: AND_typbind_opt end) AND_typbind_opt: AND typbind (typbind) | ([]) synonymtypbind : typbind (fn env => buildSynonym env typbind ((#2(argument)) typbindleft typbindright)) nativename : EQUALOP STRING (SOME STRING) | (NONE) dec: DATATYPE tcname nativename indexspec tyvarvarianceseq (fn env => let val tc = case nativename of SOME native => TC.sanitary_fresh tcname native | NONE => TC.fresh tcname val tc = TC.fresh tcname val tvinfos = List.map (fn (tyvar, variance) => Tvinfo (TV.fresh tyvar, variance)) tyvarvarianceseq val (env, sorting) = indexspec env val env = ParseLib.Type.extend env [(tcname, ParseLib.SimpleType tc)] val typedec = Datatype {tc= tc, builtin= Option.isSome nativename, params= tvinfos, sorting= sorting, constructors= []} val dec = Typedec [typedec] in ( env , [((#2(argument)) DATATYPEleft indexspecright, dec)] ) end) | DATACON idcon COLON texp nativename (fn env => let val (env, A) = texp env val (env, pv) = case ParseLib.Pvar.lookup_soft env idcon of SOME (ParseLib.Convar, pv) => (env, pv) | _ => let val pv = case nativename of SOME native => PV.sanitary_fresh idcon native | NONE => PV.fresh idcon val _ = ("Constructor declaration -- freshening " ^ idcon ^ " --> " ^ PV.toString pv ^ "\n") val (env) = ParseLib.Con.extend env (idcon, pv) in (env, pv) end in (env, [((#2(argument)) DATACONleft texpright, Datacon (pv, A))]) end) | DATASORT tcname COLON datasortpairs (fn env => let val tc = ParseLib.Type.lookup_simple_type ((#1(argument))(tcnameleft, tcnameright)) env tcname val env' = ParseLib.process_subsortpairs tc env datasortpairs in (env', []) end) | INDEXSORT id EQUALOP sort (fn env => let val newSort = IndexSortSym.fresh id val sort' = case sort env of X.Base sortname => X.Base sortname | sort' => sort' val env = ParseLib.extend_is env [(id, (newSort, sort'))] in (env, []) end) | INDEXFUN id COLON indexfunctioncomponent indexfunctionspec (fn env => let val iv = IndexSym.fresh id val info = (iv, X.IFun (indexfunctioncomponent env :: indexfunctionspec env)) val _ = X.addFun info val env' = ParseLib.extend_iv env [(id, info)] in (env', []) end) | INDEXCONSTANT id COLON sort (fn env => let val iv = IndexSym.fresh id val range = sort env val info = (iv, case id of "true" => X.ITrue | "false" => X.IFalse | "NODIM" => X.INODIM | _ => if range = X.Base(X.getDimSort()) then X.IBaseDim else X.INil range) val _ = X.addFun info val env' = ParseLib.extend_iv env [(id, info)] in (env', []) end) | INDEXPRED id complement COLON sort indexpredspec (fn env => let val iv = IndexSym.fresh id val first = {domain= sort env} val rest = indexpredspec env val complementaryPred = complement env val info = (iv, X.IFun (map (fn {domain= domain} => {domain= domain, range= X.Base (X.getBoolSort()), complement= complementaryPred}) (first :: rest))) val _ = X.addFun info val env = case complementaryPred of NONE => env | SOME pred => let in case X.getSyminfo pred of SOME (X.IFun xs) => let val infoC = X.IFun( map (fn {domain= s1, range= s2, complement= NONE} => {domain=s1, range=s2, complement= SOME iv}) xs) in X.addFun (pred, infoC); ParseLib.extend_iv env [(IndexSym.toShortString pred, (pred, infoC))] end end val env = ParseLib.extend_iv env [(id, info)] in (env, []) end) | TESTSUBTYPE texp in_or_notin texp END (fn env => let val (env, A) = texp1 env val sense = in_or_notin val (env, B) = texp2 env val loc = (#2(argument)) texp1left texp2right val d = TestSubtype (sense, (A, B)) in (env, [(loc, d)]) end) | PRIMITIVE primdec (fn env => let val env = primdec env in (env, []) end) | TYPE synonymtypbind (synonymtypbind) | VAL valdec (fn env => let val (env, decs) = valdec env in (env, decs) end) | VAL valtypedec (fn env => let val (env, dec) = valtypedec env in (env, [dec]) end) | FUN fdec (fn env => let val (env, d) = fdec env in (env, [d]) end) decs: dec decs (fn env => let val (env, ds) = dec env val (env, dsl) = decs env in (env, ds @ dsl) end) | (fn env => (env, [])) colonoranticolon: COLON (fn anno => Sdml.Dectype.AGAINST anno ) | ANTICOLON (fn anno => let in case anno of [Sdml.AnnotationType.Type A] => Sdml.Dectype.TOPLEVEL_NOT A | _ => fail ":! used with complex annotation" end) valtypedec: id colonoranticolon annotationtypelist (fn env => let val (env, anno) = annotationtypelist env val (env, pv) = case ParseLib.Pvar.lookup_soft env id of NONE => let val pv = PV.fresh id in (ParseLib.Pvar.extendOpt env [(id, pv, SOME (Dectype.AGAINST anno), ParseLib.Neutral)], pv) end | SOME (ParseLib.Ordvar (SOME _, ref ParseLib.Neutral), pv) => (print ("Warning: unused type declaration (" ^ PV.toShortString pv ^ "), shadowed by new type declaration\n"); let val pv = PV.fresh id in (ParseLib.Pvar.extendOpt env [(id, pv, SOME (Dectype.AGAINST anno), ParseLib.Neutral)], pv) end) | SOME (ParseLib.Ordvar (_, pvstatus), pv) => (let val pv = PV.fresh id in (ParseLib.Pvar.extendOpt env [(id, pv, SOME (Dectype.AGAINST anno), ParseLib.Neutral)], pv) end) | SOME (ParseLib.Convar, pv) => (print ("Cannot shadow a constructor with a variable (" ^ PV.toShortString pv ^ ")\n"); raise Option) val dectype = colonoranticolon anno in (env, ((#2(argument)) idleft annotationtypelistright, ValType (pv, dectype)) ) end) valdec: idw EQUALOP exp (fn env => let val (envWithThisDec, pv, annoOpt) = case ParseLib.Pvar.lookup_soft env idw of NONE => let val pv = PV.fresh idw val _ = dprint (fn () => "valdec " ^ idw ^ ": -NONE-") val env = ParseLib.Pvar.extendOpt env [(idw, pv, NONE, ParseLib.DefinedVal)] in (env, pv, NONE) end | SOME (ParseLib.Ordvar (annoOpt, pvstatus as ref ParseLib.Neutral), pv) => let val _ = dprint (fn () => "valdec " ^ idw ^ ": ParseLib.Neutral") val _ = pvstatus := ParseLib.DefinedVal in (env, pv, annoOpt) end | SOME (ParseLib.Ordvar (annoOpt, ref ParseLib.DefinedVal), pv) => let val pv = PV.fresh idw val _ = dprint (fn () => "valdec " ^ idw ^ ": ParseLib.DefinedVal") val env = ParseLib.Pvar.extendOpt env [(idw, pv, annoOpt, ParseLib.DefinedVal)] in (env, pv, annoOpt) end | SOME (ParseLib.Ordvar (annoOpt, ref ParseLib.DefinedFun), pv) => (print ("Cannot use `val' to redefine `fun' " ^ PV.toShortString pv ^ "\n"); raise Option) | SOME (ParseLib.Ordvar (annoOpt, ref ParseLib.FutureFun), pv) => (print ("Must use `fun' to declare variable " ^ PV.toShortString pv ^ "\n"); raise Option) | SOME (ParseLib.Convar, pv) => (print ("Cannot shadow a constructor with a variable (" ^ PV.toShortString pv ^ ")\n"); raise Option) val loc = (#2(argument)) idwleft expright val texpdec = case annoOpt of NONE => [] | SOME dectype => let in [(loc, ValType (pv, dectype))] end val expdec = [(loc, Dec (pv, ValKW, exp env))] in (envWithThisDec, texpdec @ expdec ) end) idw: id (id) | WILD ("anon_") idcon: id (id) | DBLCOLON ("::") fdec: id fdef (fn env => let val (envWithFun, pv) = case ParseLib.Pvar.lookup_soft env id of NONE => let val pv = PV.fresh id in (ParseLib.Pvar.extendOpt env [(id, pv, NONE, ParseLib.DefinedFun)], pv) end | SOME (ParseLib.Ordvar (annoOpt, pvstatus as ref ParseLib.Neutral), pv) => let val _ = pvstatus := ParseLib.DefinedFun in (env, pv) end | SOME (ParseLib.Ordvar (annoOpt, pvstatus as ref ParseLib.FutureFun), pv) => let val _ = pvstatus := ParseLib.DefinedFun in (env, pv) end | SOME (ParseLib.Ordvar (annoOpt, ref ParseLib.DefinedFun), pv) => (print ("Cannot shadow `fun' with `fun': variable " ^ PV.toShortString pv ^ "\n"); raise Option) | SOME (ParseLib.Ordvar (annoOpt, ref ParseLib.DefinedVal), pv) => (print ("Cannot shadow `val' with `fun': variable " ^ PV.toShortString pv ^ "\n"); raise Option) | SOME (ParseLib.Convar, pv) => (print ("Cannot shadow a constructor with a variable (" ^ PV.toShortString pv ^ ")\n"); raise Option) in (envWithFun, ((#2(argument)) idleft fdefright, Dec(pv, FunKW, fdef envWithFun)) ) end) fdef: idl fdef (fn env => let val pvl = List.map PV.fresh idl val bindings = ListPair.zip (idl, pvl) val env' = ParseLib.Pvar.extend_DefinedVal env bindings in (#3(argument)) idlleft fdefright (ParseLib.Pvar.tupleize pvl (fdef env')) end) | idl EQUALOP exp (fn env => let val pvl = List.map PV.fresh idl val bindings = ListPair.zip (idl, pvl) val env' = ParseLib.Pvar.extend_DefinedVal env bindings in (#3(argument)) idlleft expright (ParseLib.Pvar.tupleize pvl (exp env')) end) exp: expA (fn env => expA env) | FN idl DARROW exp (fn env => let val pvl = map PV.fresh idl val bindings = ListPair.zip (idl, pvl) val env' = ParseLib.Pvar.extend_DefinedVal env bindings in (#3(argument)) FNleft expright (ParseLib.Pvar.tupleize pvl (exp env')) end) expA: expA DBLCOMMA expB (fn env => let val head = expA env val tail = expB env in case head of (loc, Merge head) => (#3(argument)) expAleft expBright (Merge (head @ [tail])) | head => (#3(argument)) expAleft expBright (Merge [head, tail]) end) | expB (fn env => expB env) expB: WHERE ID COLON texp DO expB (fn env => let val (_, A) = texp env val (pvinfo, pv) = ParseLib.Pvar.lookup ((#1(argument))(IDleft, IDright)) env ID val tail = expB env in case pvinfo of ParseLib.Convar => ((#1(argument))(IDleft, IDright) "constructors forbidden in concrete contexts"; raise Debug.StdExcept("", "")) | ParseLib.Ordvar _ => let val leftanno = LeftProgramVar (pv, A) in ((#2(argument)) IDleft expBright, Leftanno (leftanno, tail)) end end) | expC (fn env => expC env) expC: expD (fn env => expD env) | CASE expD OF arms (fn env => (#3(argument)) CASEleft armsright (Case(expD env, Basic.mapapply arms env)) ) expD: expI (fn env => expI env) | expI SEMICOLON expD (fn env => (#3(argument)) expIleft expDright (Let( [((#2(argument)) expIleft expDright, Dec(PV.fresh "anonSemi", ValKW, expI env))], expD env))) expI: expR (fn env => expR env) | IF expR THEN expI ELSE expI (fn env => let val {true= true_pv, false= false_pv} = ParseLib.Con.get_bool ((#1(argument))(IFleft,expI2right)) env in (#3(argument)) IFleft expI2right (Case(expR env, [Arm(CtorPattern(true_pv,NONE),expI1 env), Arm(CtorPattern(false_pv,NONE),expI2 env)])) end) expR: expS (fn env => expS env) | expS ORELSE expS (fn env => let val {true= true_pv, false= false_pv} = ParseLib.Con.get_bool ((#1(argument))(expS1left,expS2right)) env in (#3(argument)) expS1left expS2right (Case(expS1 env, [Arm(CtorPattern(true_pv,NONE), (#3(argument)) ORELSEleft ORELSEright (Var true_pv)), Arm(CtorPattern(false_pv,NONE), expS2 env)])) end) | expS ANDALSO expS (fn env => let val {true= true_pv, false= false_pv} = ParseLib.Con.get_bool ((#1(argument))(expS1left,expS2right)) env in (#3(argument)) expS1left expS2right (Case(expS1 env, [Arm(CtorPattern(true_pv,NONE), expS2 env), Arm(CtorPattern(false_pv,NONE), (#3(argument)) ANDALSOleft ANDALSOright (Var false_pv))])) end) | RAISE expS (fn env => (#3(argument)) RAISEleft expSright (Raise (expS env))) expS: expZ (fn env => expZ env) | expZ ctxanno (fn env => let val anno = ctxanno env in (#3(argument)) expZleft ctxannoright (Anno (expZ env, anno)) end) | DQUESTION expZ (fn env => let val e0 = expZ env in (#3(argument)) DQUESTIONleft expZright (Spy ((), e0)) end) | TRY exp HANDLE id DARROW exp END (fn env => let val pv = PV.fresh id val env' = ParseLib.Pvar.extend_DefinedVal env [(id, pv)] in (#3(argument)) exp1left exp2right (Handle (exp1 env, pv, exp2 env')) end) expZ: app_exp (fn env => unflatten (app_exp env)) app_exp : aexp (fn env => let val item = aexp env in [{item= item, loc=(#2(argument)) aexpleft aexpright, fixity=NONE}] end) | id (fn env => let val _ = mungeEnvForFwdRef env id val (v,f) = var'n'fix env id ((#1(argument))(idleft,idright)) in [{item=(#3(argument)) idleft idright (v), loc=(#2(argument)) idleft idright, fixity=SOME f}] end) | aexp app_exp (fn env => let val item = aexp env val tail = app_exp env in {item= item, loc= (#2(argument)) aexpleft aexpright, fixity=NONE} :: tail end) | id app_exp (fn env => let val _ = mungeEnvForFwdRef env id val (v,f) = var'n'fix env id ((#1(argument))(idleft,idright)) in {item=(#3(argument)) idleft idright v, loc=(#2(argument)) idleft idright, fixity=SOME f} :: (app_exp env) end) recordexp_component : ID EQUALOP exp (fn env => (#3(argument)) IDleft expright (RecordExp(ID, exp env))) recordexp_component_list : recordexp_component COMMA recordexp_component_list (fn env => (recordexp_component env) :: (recordexp_component_list env)) | recordexp_component (fn env => [recordexp_component env]) aexp : INT (fn env => let val tc = ParseLib.Type.get "int" ((#1(argument))(INTleft, INTright)) env in (#3(argument)) INTleft INTright (Const(Tycon(tc, X.O(X.Literal (X.getIntSort(), INT)), []), INT)) end) | REAL (fn env => let val tc = ParseLib.Type.get "real" ((#1(argument))(REALleft, REALright)) env val texp = if Real.== (Option.valOf (Real.fromString REAL), 0.0) then let val zz = IndexSym.fresh "zz" in Univ(zz, X.Base (X.getDimSort()), Tycon(tc, X.O (X.Uvar zz), [])) end else Tycon(tc, X.N, []) in (#3(argument)) REALleft REALright (Const(texp, REAL)) end) | STRING (fn env => let val tc = ParseLib.Type.get "string" ((#1(argument))(STRINGleft, STRINGright)) env in (#3(argument)) STRINGleft STRINGright (Const(Tycon(tc, X.N, []), STRING)) end) | CHAR (fn env => let val tc = ParseLib.Type.get "char" ((#1(argument))(CHARleft, CHARright)) env in (#3(argument)) CHARleft CHARright (Const(Tycon(tc, X.N, []), CHAR)) end) | LBRACE recordexp_component_list RBRACE (fn env => let val recordexps = recordexp_component_list env in (#3(argument)) LBRACEleft RBRACEright (Merge recordexps) end) | LET decs IN exp END (fn env => let val _ = decslevel := !decslevel + 1 val (env, dsl) = decs env in (#3(argument)) LETleft ENDright (Let (dsl, exp env)) before decslevel := !decslevel - 1 end) | LETHINT annotationtypelist IN exp END (fn env => let val (_, anno) = annotationtypelist env in (#3(argument)) INright ENDleft (Lethint(anno, exp env)) end) | HASH INT LPAREN exp RPAREN (fn env => (#3(argument)) HASHleft RPARENright (Proj (INT, exp env))) | HASH ID LPAREN exp RPAREN (fn env => (#3(argument)) HASHleft RPARENright (Proj (ID, exp env))) | LPAREN RPAREN (fn env => (#3(argument)) LPARENleft RPARENright (Tuple [])) | LPAREN exp RPAREN (fn env => exp env) | LPAREN exp_2c RPAREN (fn env => case exp_2c of [exp] => raise Option | list => (#3(argument)) LPARENleft RPARENright (Tuple (Basic.mapapply list env))) | LBRACK exp_list RBRACK (fn env => let val {nil= nil_pv, cons=cons_pv} = ParseLib.Con.get_list ((#1(argument))(exp_listleft,exp_listright)) env fun aux [] = (#3(argument)) LBRACKleft RBRACKright (Con nil_pv) | aux (exp::exps) = (#3(argument)) LBRACKleft RBRACKright (Conapp (cons_pv, (#3(argument)) LBRACKleft RBRACKright (Tuple([exp env, aux exps])))) in aux exp_list end) exp_list: exp_2c (exp_2c) | exp ([exp]) | ([]) arms: arm ([arm]) | arm BAR arms (arm :: arms) atpattern: id (fn env => let in case ParseLib.Pvar.lookup_soft env id of SOME (ParseLib.Convar, pv) => (env, CtorPattern(pv, NONE)) | _ => let val pv = PV.fresh id in (ParseLib.Pvar.extend_DefinedVal env [(id, pv)], VarPattern pv) end end) | LBRACK patternlz RBRACK (fn env => let val {nil= nil_pv, cons= cons_pv} = ParseLib.Con.get_list ((#1(argument))(patternlzleft, patternlzright)) env val (env, pat_list) = patternlz env fun loop env [] = (env, CtorPattern (nil_pv, NONE)) | loop env (head :: pats) = let val (env, tail) = loop env pats in (env, CtorPattern (cons_pv, SOME (TuplePattern[head, tail]))) end in loop env pat_list end) | WILD (fn env => (env, WildPattern)) | INT (fn env => (env, IntPattern (valOf (Int.fromString INT)))) | STRING (fn env => (env, StringPattern STRING)) | LPAREN RPAREN (fn env => (env, TuplePattern [])) | LPAREN pattern patternl RPAREN (fn env => let val (env, pattern') = pattern env val (env, patternl'') = patternl env in case patternl'' of [] => (env, pattern') | patternl'' => (env, TuplePattern (pattern' :: patternl'')) end) | ID atpattern (fn env => case ParseLib.Pvar.lookup_soft env ID of SOME (ParseLib.Convar, pv) => let val (env, atpattern') = atpattern env in (env, CtorPattern(pv, SOME atpattern')) end | _ => ((#1(argument))(IDleft,IDright) ("identifier \"" ^ ID ^ "\" in constructor position in pattern is not a constructor") ; raise Debug.StdExcept("", ""))) | ID AS atpattern (fn env => let val pv = PV.fresh ID val env = ParseLib.Pvar.extend_DefinedVal env [(ID, pv)] val (env, atpattern') = atpattern env in (env, AsPattern (pv, atpattern')) end) pattern: atpattern (fn env => atpattern env) | atpattern DBLCOLON pattern (fn env => let val (env, head) = atpattern env val (env, tail) = pattern env val {cons= cons_pv, ...} = ParseLib.Con.get_list ((#1(argument))(atpatternleft, patternright)) env in (env, CtorPattern (cons_pv, SOME (TuplePattern[head, tail]))) end) patternl: (fn env => (env, [])) | COMMA pattern patternl (fn env => let val (env, pattern') = pattern env val (env, patternl'') = patternl env in (env, pattern' :: patternl'') end) patternlz: (fn env => (env, [])) | pattern patternl (fn env => let val (env, pattern') = pattern env val (env, patternl'') = patternl env in (env, pattern' :: patternl'') end) arm: pattern DARROW expD (fn env => let val (env', pattern') = pattern env in Arm(pattern', expD env') end) idl: idw ([idw]) | LPAREN ids RPAREN (ids) | LPAREN RPAREN ([]) ids: idw ([idw]) | idw COMMA ids (idw::ids) exp_2c: exp COMMA exp_2c (exp::exp_2c) | exp COMMA exp ([exp1,exp2]) proposition: X_exp (fn env => case X_exp env of X.App(sym, exp) => let in case X.getSyminfo sym of NONE => ((#1(argument))(X_expleft, X_expright) ("undefined index function/predicate: " ^ IndexSym.toShortString sym); X.TRUE) | SOME (X.IFun [{domain= domain, range= codomain, ...}]) => let in if codomain = X.Base (X.getBoolSort()) then let in if IndexSym.toShortString sym = "=" then let in case (domain, exp) of (X.Product[sort1, sort2], X.Tuple[exp1, exp2]) => X.EQ(sort1, exp1, exp2) end else X.PRED(sym, exp) end else ((#1(argument))(X_expleft, X_expright) ("`" ^ IndexSym.toShortString sym ^ "' is a function, not a predicate"); X.TRUE) end | SOME (X.IFun _) => ((#1(argument))(X_expleft, X_expright) ("`" ^ IndexSym.toShortString sym ^ "' is multi-sorted, and is therefore a function, not a predicate"); X.TRUE) end | _ => ((#1(argument))(X_expleft, X_expright) ("proposition expected"); X.TRUE) ) | proposition AND proposition (fn env => X.AND(proposition1 env, proposition2 env)) | proposition ORELSE proposition (fn env => X.OR(proposition1 env, proposition2 env)) tyvarseq: TYVAR ([TYVAR]) | LPAREN tyvars RPAREN (tyvars) | ([]) tyvarvariance: TYVAR variancesymbol ((TYVAR, variancesymbol)) tyvarvarianceseq: tyvarvariance tyvarvarianceseq (tyvarvariance :: tyvarvarianceseq) | ([]) tyvars: TYVAR ([TYVAR]) | TYVAR COMMA tyvars (TYVAR::tyvars) texp: texpI (texpI) | DASHALL dashalltail (dashalltail) texpI: texpC (texpC) | texpI AMP texpC (fn env => let val (env', tLeft) = texpI env val (env'', tRight) = texpC env' in (env'', Sect(tLeft, tRight)) end) | texpI DBLAMP texpC (fn env => let val (env', tLeft) = texpI env val (env'', tRight) = texpC env' in (env'', Rsect(tLeft, tRight)) end) texpC: texpD (texpD) | texpD ARROW texpC (fn env => let val (env', tLeft) = texpD env val (env'', tRight) = texpC env' in (env'', Arrow(tLeft, tRight)) end) dashalltail: ID commaids COLON sort MINUS texp (fn env => let val _ = dprnt "dashalltail ID" val srt = sort env val idlist = ID :: commaids val bindings = map (fn idstring => (idstring, (IndexSym.fresh idstring, X.IUVar srt))) idlist val env' = ParseLib.extend_iv env bindings val (env'', t) = texp env' val _ = dprint (fn () => "texp in scope of Univ: " ^ Print.pTexp t) fun buildUnivs [] = t | buildUnivs ((_, (iv, _)) :: rest) = Univ(iv, srt, buildUnivs rest) in (env, buildUnivs bindings) end) | TYVAR commatyvars MINUS texp (fn env => let val idlist = TYVAR :: commatyvars val bindings = map (fn idstring => (idstring, TV.fresh idstring)) idlist val env' = ParseLib.Tyvar.extend env bindings val (env'', t) = texp env' fun buildAlls [] = t | buildAlls ((_, tv) :: rest) = All(tv, Types.outer_universe, buildAlls rest) in (env, buildAlls bindings) end) commaids: COMMA ID commaids (ID :: commaids) | ([]) commatyvars: COMMA TYVAR commatyvars (TYVAR :: commatyvars) | ([]) indexrefinement: LBRACK X_explist RBRACK (fn env => X.O (X_explist env)) | (fn env => X.N) texpD: texpE (fn env => let val (env', tl) = texpE env in (env', case tl of [t] => t | tl => Product tl) end) | DASHEXISTS ID commaids COLON sort MINUS texpD (fn env => let val srt = sort env val idlist = ID :: commaids val bindings = map (fn idstring => (idstring, (IndexSym.fresh idstring, X.IEVar srt))) idlist val env' = ParseLib.extend_iv env bindings val (env'', t) = texpD env' fun buildExiss [] = t | buildExiss ((_, (iv, _)) :: rest) = Exis(iv, srt, buildExiss rest) in (env, buildExiss bindings) end) | LBRACK proposition RBRACK texpD (fn env => let val prop = proposition env val (env, t) = texpD env in (env, Conj(prop, t)) end) texpE: texpU (fn env => let val (env',t) = texpU env in (env',[t]) end) | texpE ASTERISK texpU (fn env => let val (env',tl) = texpE env val (env'',t) = texpU env' in (env'', tl @ [t]) end) texpU: texpY (texpY) | texpU SLASH texpU (fn env => let val (env',tLeft) = texpU1 env val (env'',tRight) = texpU2 env' in (env'', Union(tLeft, tRight)) end) | texpU DBLSLASH texpU (fn env => let val (env',tLeft) = texpU1 env val (env'',tRight) = texpU2 env' in (env'', Runion(tLeft, tRight)) end) record_component : ID COLON texp (fn env => let val (env, field_type) = texp env in (env, Record(ID, field_type)) end) record_component_list : record_component COMMA record_component_list (fn env => let val (env, component) = record_component env val (env, component_list) = record_component_list env in (env, component :: component_list) end) | record_component (fn env => let val (env, component) = record_component env in (env, [component]) end) texpY: texpZ (texpZ) | LBRACE LBRACE proposition RBRACE RBRACE texp (fn (env) => let val prop = proposition env val (env, t) = texp (env) in (env, Implies(prop, t)) end) | LBRACE record_component_list RBRACE (fn env => let val (env, fields : texp list) = record_component_list env val intersection = List.foldl (Sdml.mkSect) Top fields in (env, intersection) end) texpZ: atomictexp texpl (fn env => let val (env, atomic) = atomictexp env val (env, new_args) = texpl env in case atomic of Tycon (tc, ix, old_args) => (env, Tycon (tc, ix, old_args @ new_args)) | texp => (env, texp) end) atomictexp: LPAREN texp RPAREN (texp) | TYVAR (fn env => let val (env', tv) = case ParseLib.Tyvar.lookup_soft env TYVAR of NONE => ((#1(argument))(TYVARleft, TYVARright) ("undefined type variable: " ^ TYVAR); (env, TV.fromInt ~1)) | SOME tv => (env, tv) in (env', Typevar tv) end) | tcname indexrefinement (fn env => let val ix1 = indexrefinement env val (env', tl) = (env, []) fun process tc1 = (env', Tycon (tc1, ix1, tl)) val (env, result) = case ParseLib.Type.lookup ((#1(argument))(tcnameleft,tcnameright)) env tcname of ParseLib.SimpleType tc1 => process tc1 | ParseLib.Datasort(ds, _) => process ds | ParseLib.TypeSynonym (tc, tv) => (env, Extypevar tv) in ("PARSED type: " ^ Types.typeToString result ^ "\n"); (env, result) end) | UNIT (fn env => (env, Product [])) | TOP (fn env => (env,Top)) | BOT (fn env => (env,Bot)) texpl: atomictexp texpl (fn env => let val (env',t) = atomictexp env val (env'',tl) = texpl env' in (env', t::tl) end) | (fn env => (env, [])) tcname: ID (ID) id: ID (ID) | ASTERISK ("*") | PLUS ("+") | MINUS ("-") | EQUALOP ("=") | SLASH ("/") datasortpair: ID ID ID (if (ID2 <> "<") andalso (ID2 <> "<=") then ((#1(argument)) (ID2left, ID2right) ("bad subsort declaration: missing `<='"); raise Option) else (ID1, ID3)) datasortpairs: datasortpair ([datasortpair]) | datasortpair SEMICOLON datasortpairs (datasortpair :: datasortpairs) complement: (fn env => NONE) | ANTICOLON id (fn env => let val (iv, syminfo) = ParseLib.lookup_iv ((#1(argument))(idleft, idright)) env id in case syminfo of X.IFun _ => SOME iv | _ => ((#1(argument)) (idleft, idright) ("indexpred complement spec is not an index predicate: " ^ id); NONE) end) indexfunctioncomponent: sort ARROW sort (fn env => {domain=sort1 env, range= sort2 env, complement= NONE}) indexfunctionspec: (fn env => []) | COMMA indexfunctioncomponent indexfunctionspec (fn env => let val c = indexfunctioncomponent env val rest = indexfunctionspec env in c :: rest end) indexpredspec: (fn env => []) | COMMA sort indexpredspec (fn env => let val c = {domain= sort env} val rest = indexpredspec env in c :: rest end) variancesymbol: PLUS (Sdml.Variance.Co) | MINUS (Sdml.Variance.Contra) | ASTERISK (Sdml.Variance.Non) | (Sdml.Variance.Non) primdec: TYPE tcname indexspec (fn env => let val tc = TC.fresh tcname val (env, ispec) = indexspec env val env = ParseLib.Type.extend_libinfo env (tc, ispec) val env = ParseLib.Type.extend env [(tcname, ParseLib.SimpleType tc)] in env end) | FUN id stringopt COLON texp EQUALOP stringseq (fn env => let val sanitized_name = Option.getOpt (stringopt, id) val pv = PV.sanitary_fresh id sanitized_name val (_, t) = texp env val elaboration = stringseq val env = ParseLib.Pvar.extend_libinfo_primop env (pv, {source_texp= t, elaboration= elaboration, proper_name= id, sanitized_name= sanitized_name}) val env = ParseLib.Pvar.extend_DefinedVal env [(id, pv)] in env end) | VAL id COLON texp EQUALOP stringseq (fn env => let val pv = PV.fresh id val (_, t) = texp env val elaboration = stringseq val env = ParseLib.Pvar.extend_libinfo_primop env (pv, {source_texp= t, elaboration= elaboration, proper_name= id, sanitized_name= id}) val env = ParseLib.Pvar.extend_DefinedVal env [(id, pv)] in env end) stringseq: STRING (STRING) | STRING stringseq (String.concat [STRING, "\n", stringseq]) stringopt: STRING (SOME STRING) | (NONE) sort: sprodel (fn env => case sprodel env of [s] => s | sl => X.Product sl) | UNIT (fn env => X.Product []) | LBRACE ID COLON sort BAR proposition RBRACE (fn env => let val sym = IndexSym.fresh ID val sort' = sort env val env' = ParseLib.extend_iv env [(ID, (sym, X.IUVar sort'))] val prop = proposition env' in X.Subset (sort', sym, prop) end) sprodel: sort0 (fn env => [sort0 env]) | sort0 ASTERISK sprodel (fn env => (sort0 env) :: (sprodel env)) sort0: ID (fn env => let val (sortSym, sort) = ParseLib.lookup_is ((#1(argument))(IDleft, IDright)) env ID in sort end) | LPAREN sort RPAREN (sort) | LBRACE ID RBRACE (fn env => let in case ID of "uninterpreted" => let val sortname = IndexSortSym.fresh "uninterpreted" in X.Base sortname end | _ => ((#1(argument))(IDleft,IDright) "unknown {}-indexsort (known: `uninterpreted')"; raise Debug.StdExcept("", "")) end) | LBRACK sort RBRACK (fn env => X.List (sort env)) X_exp: X_appexp (fn env => X_unflatten (X_appexp env)) X_appexp : X_aexp (fn env => [{item=X_aexp env, loc=(#2(argument)) X_aexpleft X_aexpright, fixity=NONE}]) | id (fn env => let val (v,f) = X_var'n'fix env id ((#1(argument))(idleft, idright)) in [{item=v, loc=(#2(argument)) idleft idright, fixity=SOME f}] end) | X_aexp X_appexp (fn env => {item=X_aexp env, loc=(#2(argument)) X_aexpleft X_aexpright, fixity=NONE} :: (X_appexp env)) | id X_appexp (fn env => let val (v,f) = X_var'n'fix env id ((#1(argument))(idleft, idright)) in {item=v, loc=(#2(argument)) idleft idright, fixity=SOME f} :: (X_appexp env) end) X_aexp: LPAREN RPAREN (fn env => X.Tuple []) | HASH INT LPAREN X_exp RPAREN (fn env => X.Proj (Option.valOf (Int.fromString INT), X_exp env)) | INT (fn env => X.Literal(X.getIntSort(), INT)) | LPAREN X_exp RPAREN (X_exp) | LPAREN X_exp_2c RPAREN (fn env => case X_exp_2c of [X_exp] => raise Option | list => X.Tuple (Basic.mapapply list env)) X_exp_2c: X_exp COMMA X_exp_2c (X_exp :: X_exp_2c) | X_exp COMMA X_exp ([X_exp1, X_exp2]) X_explist0: X_exp COMMA X_explist0 (X_exp :: X_explist0) | X_exp ([X_exp]) X_explist: X_explist0 (fn env => case X_explist0 of [X_exp] => X_exp env | exps => X.Tuple (Basic.mapapply exps env)) annotationtypelist: annotationtype (fn env => let val (env', anno) = annotationtype env in (env', [anno]) end) | LPAREN annotationtypelist RPAREN (fn env => annotationtypelist env) | annotationtype DBLCOMMA annotationtypelist (fn env => let val (env', anno) = annotationtype env val (env'', annos) = annotationtypelist env' in (env'', anno::annos) end) annotationtype: texp (fn env => let val (env', A) = texp env in (env', AnnotationType.Type A) end) | SOME ID COLON sort PERIOD annotationtype (fn env => let val sym = IndexSym.fresh ID val env' = ParseLib.extend_iv env [(ID, (sym, X.IUVar (sort env)))] val (_, anno) = annotationtype env' in (env, AnnotationType.Some (sym, sort env', anno)) end) | ID COLON texp LEFTANNO annotationtype (fn env => let val (_, A) = texp env val (pvinfo, pv) = ParseLib.Pvar.lookup ((#1(argument))(IDleft, IDright)) env ID val (_, anno) = annotationtype env in case pvinfo of ParseLib.Convar => ((#1(argument))(IDleft, IDright) "constructors forbidden in concrete contexts"; raise Debug.StdExcept("", "")) | ParseLib.Ordvar _ => (env, AnnotationType.LeftProgramVar (pv, A, anno)) end) ctxanno: COLON texp (fn env => let val (_, texp') = texp env in Sdml.just texp' end)