comparison src/urweb.grm @ 823:669ac5e9a69e

Demo compiles with pattern-matching-fu
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 May 2009 10:35:25 -0400
parents d4e811beb8eb
children 7f871c03e3a1
comparison
equal deleted inserted replaced
822:d4e811beb8eb 823:669ac5e9a69e
983 val loc = s (patSleft, patSright) 983 val loc = s (patSleft, patSright)
984 val pt = patType loc patS 984 val pt = patType loc patS
985 985
986 val e' = case #1 patS of 986 val e' = case #1 patS of
987 PVar x => (EAbs (x, NONE, e), loc) 987 PVar x => (EAbs (x, NONE, e), loc)
988 | PAnnot ((PVar x, _), t) => (EAbs (x, SOME t, e), loc)
988 | _ => (EAbs ("$x", SOME pt, 989 | _ => (EAbs ("$x", SOME pt,
989 (ECase ((EVar ([], "$x", DontInfer), 990 (ECase ((EVar ([], "$x", DontInfer),
990 loc), 991 loc),
991 [(patS, e)]), loc)), loc) 992 [(patS, e)]), loc)), loc)
992 in 993 in
999 val loc = s (ptermleft, ptermright) 1000 val loc = s (ptermleft, ptermright)
1000 val pt = patType loc pterm 1001 val pt = patType loc pterm
1001 1002
1002 val e' = case #1 pterm of 1003 val e' = case #1 pterm of
1003 PVar x => (EAbs (x, NONE, e), loc) 1004 PVar x => (EAbs (x, NONE, e), loc)
1005 | PAnnot ((PVar x, _), t) => (EAbs (x, SOME t, e), loc)
1004 | _ => (EAbs ("$x", SOME pt, 1006 | _ => (EAbs ("$x", SOME pt,
1005 (ECase ((EVar ([], "$x", DontInfer), 1007 (ECase ((EVar ([], "$x", DontInfer),
1006 loc), 1008 loc),
1007 [(pterm, e)]), loc)), loc) 1009 [(pterm, e)]), loc)), loc)
1008 in 1010 in