comparison src/urweb.grm @ 478:6ee1c761818f

Some small changes while failing to write [restrict]
author Adam Chlipala <adamc@hcoop.net>
date Sat, 08 Nov 2008 13:15:00 -0500
parents 04b91c33ef54
children ae03d09043c1
comparison
equal deleted inserted replaced
477:667c0e54632a 478:6ee1c761818f
623 val loc = s (LPARENleft, RPARENright) 623 val loc = s (LPARENleft, RPARENright)
624 in 624 in
625 ((CAbs (SYMBOL, SOME kind, c), loc), 625 ((CAbs (SYMBOL, SOME kind, c), loc),
626 (KArrow (kind, k), loc)) 626 (KArrow (kind, k), loc))
627 end) 627 end)
628 | LBRACK cterm TWIDDLE cterm RBRACK (fn (c, k) => 628 | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) =>
629 let 629 let
630 val loc = s (LBRACKleft, RBRACKright) 630 val loc = s (LBRACKleft, RBRACKright)
631 in 631 in
632 ((CDisjoint (cterm1, cterm2, c), loc), 632 ((CDisjoint (cexp1, cexp2, c), loc),
633 k) 633 k)
634 end) 634 end)
635 635
636 path : SYMBOL ([], SYMBOL) 636 path : SYMBOL ([], SYMBOL)
637 | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) 637 | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end)
808 val loc = s (LPARENleft, RPARENright) 808 val loc = s (LPARENleft, RPARENright)
809 in 809 in
810 ((EAbs ("_", SOME cexp, e), loc), 810 ((EAbs ("_", SOME cexp, e), loc),
811 (TFun (cexp, t), loc)) 811 (TFun (cexp, t), loc))
812 end) 812 end)
813 | LPAREN cterm TWIDDLE cterm RPAREN(fn (e, t) => 813 | LPAREN cexp TWIDDLE cexp RPAREN (fn (e, t) =>
814 let 814 let
815 val loc = s (LPARENleft, RPARENright) 815 val loc = s (LPARENleft, RPARENright)
816 in 816 in
817 ((EDisjoint (cterm1, cterm2, e), loc), 817 ((EDisjoint (cexp1, cexp2, e), loc),
818 (CDisjoint (cterm1, cterm2, t), loc)) 818 (CDisjoint (cexp1, cexp2, t), loc))
819 end) 819 end)
820 | LBRACK cterm TWIDDLE cterm RBRACK(fn (e, t) => 820 | LBRACK cexp TWIDDLE cexp RBRACK(fn (e, t) =>
821 let 821 let
822 val loc = s (LBRACKleft, RBRACKright) 822 val loc = s (LBRACKleft, RBRACKright)
823 in 823 in
824 ((EDisjoint (cterm1, cterm2, e), loc), 824 ((EDisjoint (cexp1, cexp2, e), loc),
825 (CDisjoint (cterm1, cterm2, t), loc)) 825 (CDisjoint (cexp1, cexp2, t), loc))
826 end) 826 end)
827 827
828 eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) 828 eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
829 | LPAREN etuple RPAREN (let 829 | LPAREN etuple RPAREN (let
830 val loc = s (LPARENleft, RPARENright) 830 val loc = s (LPARENleft, RPARENright)