(* s is a string consisting of an identifier, followed by one or more whitespace characters other than newlines, followed by "::" *) fun chop s = let fun stripws s' = let val last = String.sub (s', size(s')-1) in case last of #" " => stripws (substring (s', 0, (size(s')-1))) | #"\t" => stripws (substring (s', 0, (size(s')-1))) | c => s' end in stripws (substring (s, 0, size(s)-2)) end structure D = DextSyn' structure L = Lexer %% %name Delphin %pos int %header (functor DelphinLrValsFun (structure Token : TOKEN structure DextSyn' : DEXTSYN)) %eop EOF %noshift EOF %verbose %term ID of string | COLON | DOT | EQUAL | DBLCOLON | BLOCKDEC | BLOCK of string | VAL | FUN | CASE | OF | BAR | LET | IN | END | NEW | CHOOSE | SOME of string | ALL | EXISTS | ALLOMITTED | EXISTSOMITTED | TYPE | RTARROW | LTARROW | RTPAREN | LTPAREN | RTBRACKET | LTBRACKET | RTBRACE | LTBRACE | AND | DBLARROW | COMMA | PAR | EOF | LTANGLE | RTANGLE | TRUE | UNIT | LLAM | RLAM | AT | TIMES | PLUS | UNDERSCORE | WORLD | PREC1 | FORMID of string | PREC0 %nonterm start of D.Ast | decs of D.Decs | formdecl of D.FormDecl | fundecl of D.FunDecl | valdecl of D.ValDecl | term of D.Term | cases of D.Cases | dec of D.Dec | form of D.Form | head of D.Head | mdec of D.MDec | pat of D.Pat | prog of D.Prog | world of D.World | id of string | lfdecs of D.Dec list %left UNDERSCORE %left COLON %left LTARROW %left AT %left PREC0 %left PREC1 %left AND %right DOT %right DBLCOLON %right ID TRUE ALL EXISTS ALLOMITTED EXISTSOMITTED VAL FUN CASE OF BAR LET IN END NEW CHOOSE %right RTARROW DBLARROW %nonassoc LTBRACE RTBRACE LTBRACKET RTBRACKET LLAM RLAM %nonassoc LTPAREN RTPAREN LTANGLE RTANGLE %% start : decs (D.Ast decs) decs : (D.Empty) | fundecl decs (D.FunDecl (fundecl, decs)) | formdecl decs (D.FormDecl (formdecl, decs)) | valdecl decs (D.ValDecl (valdecl, decs)) | NEW LTPAREN dec RTPAREN decs (D.NewDecl (dec, decs)) formdecl : FORMID form (D.Form (chop (FORMID), form)) fundecl : FUN head EQUAL prog %prec PREC1 (D.Fun (head, prog)) | BAR head EQUAL prog %prec PREC1 (D.Bar (head, prog)) | AND head EQUAL prog %prec PREC1 (D.FunAnd (head, prog)) valdecl : VAL pat DBLCOLON form EQUAL prog %prec ID (D.Val (pat, prog, SOME form)) | VAL pat EQUAL prog %prec ID (D.Val (pat, prog, NONE)) term : TYPE (D.Type) | ID (D.Id ID) | TRUE (D.Id "true") | AND (D.Id "and") | ALL (D.Id "all") | ALLOMITTED (D.Id "all^") | EXISTS (D.Id "exists") | EXISTSOMITTED (D.Id "exists^") | VAL (D.Id "val") | FUN (D.Id "fun") | CASE (D.Id "case") | OF (D.Id "of") | PAR (D.Id "||") | BAR (D.Id "|") | LET (D.Id "let") | TIMES (D.Id "*") | PLUS (D.Id "+") | IN (D.Id "in") | END (D.Id "end") | NEW (D.Id "new") | CHOOSE (D.Id "choose") | term RTARROW term (D.Rtarrow (term1, term2)) | term LTARROW term (D.Ltarrow (term1, term2)) | LTBRACE dec RTBRACE term (D.Pi (dec, term)) | LTBRACKET dec RTBRACKET term (D.Fn (dec, term)) | LTPAREN term RTPAREN (D.Paren term) | ID term (D.App (D.Id ID, term)) | TRUE term (D.App (D.Id "true", term)) | AND term (D.App (D.Id "and", term)) | ALL term (D.App (D.Id "all", term)) | ALLOMITTED term (D.App (D.Id "all^", term)) | EXISTS term (D.App (D.Id "exists", term)) | EXISTSOMITTED term (D.App (D.Id "exists^", term)) | VAL term (D.App (D.Id "val", term)) | FUN term (D.App (D.Id "fun", term)) | CASE term (D.App (D.Id "case", term)) | OF term (D.App (D.Id "of", term)) | BAR term (D.App (D.Id "|", term)) | PAR term (D.App (D.Id "||", term)) | LET term (D.App (D.Id "let", term)) | IN term (D.App (D.Id "in", term)) | END term (D.App (D.Id "end", term)) | NEW term (D.App (D.Id "new", term)) | CHOOSE term (D.App (D.Id "choose", term)) | UNDERSCORE term (D.Omit) | LTPAREN term RTPAREN term (D.App (D.Paren term1, term2)) | term COLON term (D.Of (term1, term2)) | UNDERSCORE (D.Omit) | term DOT ID (D.Dot (term1, ID)) world : LTPAREN world RTPAREN (world) | ID (D.WorldIdent ID) | world world (D.Concat (world1, world2)) | world PLUS world (D.Plus (world, world)) | world TIMES (D.Times world) dec : ID COLON term (D.Dec (ID, term)) | ID (D.Dec (ID, D.Omit)) form : WORLD world form %prec UNDERSCORE (D.World (world, form)) | ALL LTBRACE dec RTBRACE form (D.Forall (dec, form)) | ALLOMITTED LTBRACE dec RTBRACE form (D.ForallOmitted (dec, form)) | EXISTS LTBRACE dec RTBRACE form (D.Exists (dec, form)) | EXISTSOMITTED LTBRACE dec RTBRACE form (D.ExistsOmitted (dec, form)) | form AND form (*%prec AND*) (D.And (form1, form2)) | LTPAREN form RTPAREN (form) | TRUE (D.True) prog : ID (D.Const (ID)) | prog ID (D.AppTerm (prog, D.Id ID)) | prog UNDERSCORE (D.AppTerm (prog, D.Id "_")) | prog LTPAREN term RTPAREN (D.AppTerm (prog, term)) | LTPAREN prog RTPAREN (prog) | UNIT (D.Unit) | CASE prog OF cases (D.Unit) | prog PAR prog (D.Par (prog1, prog2)) | LTPAREN prog COMMA prog RTPAREN (D.Pair (prog1, prog2)) | prog AT prog (D.AppProg (prog1, prog2)) | LTANGLE term COMMA prog RTANGLE (D.Inx (term, prog)) | LLAM dec RLAM prog (D.Lam (dec, prog)) | LET decs IN prog END (D.Let (decs, prog)) | NEW lfdecs IN prog END (D.New (lfdecs, prog)) | CHOOSE LTPAREN dec RTPAREN IN prog END (D.Choose (dec, prog)) lfdecs : (nil) | LTPAREN dec RTPAREN lfdecs (dec :: lfdecs) cases : pat DBLARROW prog %prec PREC0 (D.First (pat, prog)) | cases BAR pat DBLARROW prog %prec PREC1 (D.Alt (cases, pat, prog)) head : ID (D.Head (ID)) | head ID (D.AppLF (head, D.Id ID)) | head UNDERSCORE (D.AppLF (head, D.Omit)) | head LTPAREN term RTPAREN (D.AppLF (head, term)) | head AT pat (D.AppMeta (head, pat)) mdec : ID (D.MDec (ID, NONE)) | FORMID form (D.MDec (chop (FORMID), SOME (form))) pat : mdec (D.PatVar (mdec)) | LTPAREN pat COMMA pat RTPAREN (D.PatPair (pat1, pat2)) | LTANGLE term COMMA pat RTANGLE (D.PatInx (term, pat)) | UNIT (D.PatUnit) | UNDERSCORE (D.PatUnderscore)