From db7a947275c7bcb44a095b25ccf95526af68d737 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 12 Oct 2008 11:44:43 -0400 Subject: Basis indents and type-checks with new twiddle syntax --- src/elisp/urweb-move.el | 6 ++---- src/urweb.grm | 23 +++++++++++++++++++++-- 2 files changed, 23 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/elisp/urweb-move.el b/src/elisp/urweb-move.el index 3c7d5b21..41fc4cc5 100644 --- a/src/elisp/urweb-move.el +++ b/src/elisp/urweb-move.el @@ -76,9 +76,7 @@ ((">" ">=" "<>" "<" "<=" "=") . 4) (("+" "-" "^") . 6) (("/" "*" "%") . 7) - (("++" "--") 8) - (("NOT") 9) - (("~") 10))) + (("NOT") 9))) "Alist of Ur/Web infix operators and their precedence.") (defconst urweb-syntax-prec @@ -91,7 +89,7 @@ (("<-") . 55) ("||" . 70) ("&&" . 80) - ((":" "::" ":::" ":>") . 90) + ((":" ":>") . 90) ("->" . 95) ("with" . 100) (,(cons "end" urweb-begin-syms) . 10000))) diff --git a/src/urweb.grm b/src/urweb.grm index b7b09227..3c270100 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -529,7 +529,6 @@ cexp : capps (capps) | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) | FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright))))) - | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright)) | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) @@ -592,6 +591,13 @@ cargp : SYMBOL (fn (c, k) => ((CAbs (SYMBOL, SOME kind, c), loc), (KArrow (kind, k), loc)) end) + | LBRACK cterm TWIDDLE cterm RBRACK (fn (c, k) => + let + val loc = s (LBRACKleft, RBRACKright) + in + ((CDisjoint (cterm1, cterm2, c), loc), + k) + end) path : SYMBOL ([], SYMBOL) | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) @@ -650,7 +656,6 @@ eexp : eapps (eapps) in #1 (eargs (eexp, (CWild (KType, loc), loc))) end) - | LBRACK cterm TWIDDLE cterm RBRACK DARROW eexp(EDisjoint (cterm1, cterm2, eexp), s (LBRACKleft, RBRACKright)) | eexp COLON cexp (EAnnot (eexp, cexp), s (eexpleft, cexpright)) | eexp MINUSMINUS cexp (ECut (eexp, cexp), s (eexpleft, cexpright)) | CASE eexp OF barOpt branch branchs (ECase (eexp, branch :: branchs), s (CASEleft, branchsright)) @@ -709,6 +714,13 @@ earg : SYMBOL kcolon kind (fn (e, t) => ((EAbs ("_", SOME cexp, e), loc), (TFun (cexp, t), loc)) end) + | cterm TWIDDLE cterm (fn (e, t) => + let + val loc = s (cterm1left, cterm2right) + in + ((EDisjoint (cterm1, cterm2, e), loc), + (CDisjoint (cterm1, cterm2, t), loc)) + end) | eargp (eargp) eargp : SYMBOL (fn (e, t) => @@ -754,6 +766,13 @@ eargp : SYMBOL (fn (e, t) => ((EAbs ("_", SOME cexp, e), loc), (TFun (cexp, t), loc)) end) + | LPAREN cterm TWIDDLE cterm RPAREN(fn (e, t) => + let + val loc = s (LPARENleft, RPARENright) + in + ((EDisjoint (cterm1, cterm2, e), loc), + (CDisjoint (cterm1, cterm2, t), loc)) + end) eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) | LPAREN etuple RPAREN (let -- cgit v1.2.3