Mercurial > urweb

comparison src/urweb.grm @ 354:527529a083d9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Basis indents and type-checks with new twiddle syntax
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Oct 2008 11:44:43 -0400
parents b85e6ba56618
children 383c72d11db8
comparison
equal deleted inserted replaced
353:9390c55b9f1f 354:527529a083d9
527 | SYMBOL kcolon kind ARROW cexp (TCFun (kcolon, SYMBOL, kind, cexp), s (SYMBOLleft, cexpright)) 527 | SYMBOL kcolon kind ARROW cexp (TCFun (kcolon, SYMBOL, kind, cexp), s (SYMBOLleft, cexpright))
528 528
529 | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) 529 | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right))
530 530
531 | FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright))))) 531 | FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright)))))
532 | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
533 532
534 | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) 533 | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
535 534
536 | UNDER DCOLON kind (CWild kind, s (UNDERleft, UNDERright)) 535 | UNDER DCOLON kind (CWild kind, s (UNDERleft, UNDERright))
537 | ctuple (let 536 | ctuple (let
590 val loc = s (LPARENleft, RPARENright) 589 val loc = s (LPARENleft, RPARENright)
591 in 590 in
592 ((CAbs (SYMBOL, SOME kind, c), loc), 591 ((CAbs (SYMBOL, SOME kind, c), loc),
593 (KArrow (kind, k), loc)) 592 (KArrow (kind, k), loc))
594 end) 593 end)
594 | LBRACK cterm TWIDDLE cterm RBRACK (fn (c, k) =>
595 let
596 val loc = s (LBRACKleft, RBRACKright)
597 in
598 ((CDisjoint (cterm1, cterm2, c), loc),
599 k)
600 end)
595 601
596 path : SYMBOL ([], SYMBOL) 602 path : SYMBOL ([], SYMBOL)
597 | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) 603 | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end)
598 604
599 cpath : CSYMBOL ([], CSYMBOL) 605 cpath : CSYMBOL ([], CSYMBOL)
648 | FN eargs DARROW eexp (let 654 | FN eargs DARROW eexp (let
649 val loc = s (FNleft, eexpright) 655 val loc = s (FNleft, eexpright)
650 in 656 in
651 #1 (eargs (eexp, (CWild (KType, loc), loc))) 657 #1 (eargs (eexp, (CWild (KType, loc), loc)))
652 end) 658 end)
653 | LBRACK cterm TWIDDLE cterm RBRACK DARROW eexp(EDisjoint (cterm1, cterm2, eexp), s (LBRACKleft, RBRACKright))
654 | eexp COLON cexp (EAnnot (eexp, cexp), s (eexpleft, cexpright)) 659 | eexp COLON cexp (EAnnot (eexp, cexp), s (eexpleft, cexpright))
655 | eexp MINUSMINUS cexp (ECut (eexp, cexp), s (eexpleft, cexpright)) 660 | eexp MINUSMINUS cexp (ECut (eexp, cexp), s (eexpleft, cexpright))
656 | CASE eexp OF barOpt branch branchs (ECase (eexp, branch :: branchs), s (CASEleft, branchsright)) 661 | CASE eexp OF barOpt branch branchs (ECase (eexp, branch :: branchs), s (CASEleft, branchsright))
657 | IF eexp THEN eexp ELSE eexp (let 662 | IF eexp THEN eexp ELSE eexp (let
658 val loc = s (IFleft, eexp3right) 663 val loc = s (IFleft, eexp3right)
706 let 711 let
707 val loc = s (UNDERleft, cexpright) 712 val loc = s (UNDERleft, cexpright)
708 in 713 in
709 ((EAbs ("_", SOME cexp, e), loc), 714 ((EAbs ("_", SOME cexp, e), loc),
710 (TFun (cexp, t), loc)) 715 (TFun (cexp, t), loc))
716 end)
717 | cterm TWIDDLE cterm (fn (e, t) =>
718 let
719 val loc = s (cterm1left, cterm2right)
720 in
721 ((EDisjoint (cterm1, cterm2, e), loc),
722 (CDisjoint (cterm1, cterm2, t), loc))
711 end) 723 end)
712 | eargp (eargp) 724 | eargp (eargp)
713 725
714 eargp : SYMBOL (fn (e, t) => 726 eargp : SYMBOL (fn (e, t) =>
715 let 727 let
751 let 763 let
752 val loc = s (LPARENleft, RPARENright) 764 val loc = s (LPARENleft, RPARENright)
753 in 765 in
754 ((EAbs ("_", SOME cexp, e), loc), 766 ((EAbs ("_", SOME cexp, e), loc),
755 (TFun (cexp, t), loc)) 767 (TFun (cexp, t), loc))
768 end)
769 | LPAREN cterm TWIDDLE cterm RPAREN(fn (e, t) =>
770 let
771 val loc = s (LPARENleft, RPARENright)
772 in
773 ((EDisjoint (cterm1, cterm2, e), loc),
774 (CDisjoint (cterm1, cterm2, t), loc))
756 end) 775 end)
757 776
758 eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) 777 eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
759 | LPAREN etuple RPAREN (let 778 | LPAREN etuple RPAREN (let
760 val loc = s (LPARENleft, RPARENright) 779 val loc = s (LPARENleft, RPARENright)