Mercurial > urweb

comparison src/urweb.grm @ 822:d4e811beb8eb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fn-pattern code in but not tested yet; hello compiles
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 May 2009 10:16:50 -0400
parents 395a5d450cc0
children 669ac5e9a69e
comparison
equal deleted inserted replaced
821:395a5d450cc0 822:d4e811beb8eb
176 176
177 datatype prop_kind = Delete | Update 177 datatype prop_kind = Delete | Update
178 178
179 datatype attr = Class of exp | Normal of con * exp 179 datatype attr = Class of exp | Normal of con * exp
180 180
181 fun patType loc (p : pat) =
182 case #1 p of
183 PAnnot (_, t) => t
184 | _ => (CWild (KType, loc), loc)
185
181 %% 186 %%
182 %header (functor UrwebLrValsFn(structure Token : TOKEN)) 187 %header (functor UrwebLrValsFn(structure Token : TOKEN))
183 188
184 %term 189 %term
185 EOF 190 EOF
288 | edecl of edecl 293 | edecl of edecl
289 | edecls of edecl list 294 | edecls of edecl list
290 295
291 | earg of exp * con -> exp * con 296 | earg of exp * con -> exp * con
292 | eargp of exp * con -> exp * con 297 | eargp of exp * con -> exp * con
298 | earga of exp * con -> exp * con
293 | eargs of exp * con -> exp * con 299 | eargs of exp * con -> exp * con
294 | eargl of exp * con -> exp * con 300 | eargl of exp * con -> exp * con
295 | eargl2 of exp * con -> exp * con 301 | eargl2 of exp * con -> exp * con
296 302
297 | branch of pat * exp 303 | branch of pat * exp
298 | branchs of (pat * exp) list 304 | branchs of (pat * exp) list
299 | pat of pat 305 | pat of pat
306 | patS of pat
300 | pterm of pat 307 | pterm of pat
301 | rpat of (string * pat) list * bool 308 | rpat of (string * pat) list * bool
302 | ptuple of pat list 309 | ptuple of pat list
303 310
304 | attrs of exp option * (con * exp) list 311 | attrs of exp option * (con * exp) list
969 | eargp eargl (eargp o eargl) 976 | eargp eargl (eargp o eargl)
970 977
971 eargl2 : (fn x => x) 978 eargl2 : (fn x => x)
972 | eargp eargl2 (eargp o eargl2) 979 | eargp eargl2 (eargp o eargl2)
973 980
974 earg : SYMBOL kcolon kind (fn (e, t) => 981 earg : patS (fn (e, t) =>
975 let 982 let
976 val loc = s (SYMBOLleft, kindright) 983 val loc = s (patSleft, patSright)
984 val pt = patType loc patS
985
986 val e' = case #1 patS of
987 PVar x => (EAbs (x, NONE, e), loc)
988 | _ => (EAbs ("$x", SOME pt,
989 (ECase ((EVar ([], "$x", DontInfer),
990 loc),
991 [(patS, e)]), loc)), loc)
977 in 992 in
978 ((ECAbs (kcolon, SYMBOL, kind, e), loc), 993 (e', (TFun (pt, t), loc))
979 (TCFun (kcolon, SYMBOL, kind, t), loc))
980 end) 994 end)
981 | SYMBOL COLON cexp (fn (e, t) => 995 | earga (earga)
996
997 eargp : pterm (fn (e, t) =>
982 let 998 let
983 val loc = s (SYMBOLleft, cexpright) 999 val loc = s (ptermleft, ptermright)
1000 val pt = patType loc pterm
1001
1002 val e' = case #1 pterm of
1003 PVar x => (EAbs (x, NONE, e), loc)
1004 | _ => (EAbs ("$x", SOME pt,
1005 (ECase ((EVar ([], "$x", DontInfer),
1006 loc),
1007 [(pterm, e)]), loc)), loc)
984 in 1008 in
985 ((EAbs (SYMBOL, SOME cexp, e), loc), 1009 (e', (TFun (pt, t), loc))
986 (TFun (cexp, t), loc))
987 end) 1010 end)
988 | UNDER COLON cexp (fn (e, t) => 1011 | earga (earga)
989 let 1012
990 val loc = s (UNDERleft, cexpright) 1013 earga : LBRACK SYMBOL RBRACK (fn (e, t) =>
991 in
992 ((EAbs ("_", SOME cexp, e), loc),
993 (TFun (cexp, t), loc))
994 end)
995 | eargp (eargp)
996
997 eargp : SYMBOL (fn (e, t) =>
998 let
999 val loc = s (SYMBOLleft, SYMBOLright)
1000 in
1001 ((EAbs (SYMBOL, NONE, e), loc),
1002 (TFun ((CWild (KType, loc), loc), t), loc))
1003 end)
1004 | UNIT (fn (e, t) =>
1005 let
1006 val loc = s (UNITleft, UNITright)
1007 val t' = (TRecord (CRecord [], loc), loc)
1008 in
1009 ((EAbs ("_", SOME t', e), loc),
1010 (TFun (t', t), loc))
1011 end)
1012 | UNDER (fn (e, t) =>
1013 let
1014 val loc = s (UNDERleft, UNDERright)
1015 in
1016 ((EAbs ("_", NONE, e), loc),
1017 (TFun ((CWild (KType, loc), loc), t), loc))
1018 end)
1019 | LPAREN SYMBOL kcolon kind RPAREN(fn (e, t) =>
1020 let 1014 let
1021 val loc = s (LPARENleft, RPARENright) 1015 val loc = s (LBRACKleft, RBRACKright)
1016 val kind = (KWild, loc)
1017 in
1018 ((ECAbs (Implicit, SYMBOL, kind, e), loc),
1019 (TCFun (Implicit, SYMBOL, kind, t), loc))
1020 end)
1021 | LBRACK SYMBOL kcolon kind RBRACK(fn (e, t) =>
1022 let
1023 val loc = s (LBRACKleft, RBRACKright)
1022 in 1024 in
1023 ((ECAbs (kcolon, SYMBOL, kind, e), loc), 1025 ((ECAbs (kcolon, SYMBOL, kind, e), loc),
1024 (TCFun (kcolon, SYMBOL, kind, t), loc)) 1026 (TCFun (kcolon, SYMBOL, kind, t), loc))
1025 end) 1027 end)
1026 | LPAREN SYMBOL COLON cexp RPAREN (fn (e, t) =>
1027 let
1028 val loc = s (LPARENleft, RPARENright)
1029 in
1030 ((EAbs (SYMBOL, SOME cexp, e), loc),
1031 (TFun (cexp, t), loc))
1032 end)
1033 | LPAREN UNDER COLON cexp RPAREN (fn (e, t) =>
1034 let
1035 val loc = s (LPARENleft, RPARENright)
1036 in
1037 ((EAbs ("_", SOME cexp, e), loc),
1038 (TFun (cexp, t), loc))
1039 end)
1040 | LPAREN cexp TWIDDLE cexp RPAREN (fn (e, t) =>
1041 let
1042 val loc = s (LPARENleft, RPARENright)
1043 in
1044 ((EDisjoint (cexp1, cexp2, e), loc),
1045 (TDisjoint (cexp1, cexp2, t), loc))
1046 end)
1047 | LBRACK cexp TWIDDLE cexp RBRACK(fn (e, t) => 1028 | LBRACK cexp TWIDDLE cexp RBRACK(fn (e, t) =>
1048 let 1029 let
1049 val loc = s (LBRACKleft, RBRACKright) 1030 val loc = s (LBRACKleft, RBRACKright)
1050 in 1031 in
1051 ((EDisjoint (cexp1, cexp2, e), loc), 1032 ((EDisjoint (cexp1, cexp2, e), loc),
1052 (TDisjoint (cexp1, cexp2, t), loc)) 1033 (TDisjoint (cexp1, cexp2, t), loc))
1053 end) 1034 end)
1054 | CSYMBOL (fn (e, t) => 1035 | LBRACK CSYMBOL RBRACK (fn (e, t) =>
1055 let 1036 let
1056 val loc = s (CSYMBOLleft, CSYMBOLright) 1037 val loc = s (CSYMBOLleft, CSYMBOLright)
1057 in 1038 in
1058 ((EKAbs (CSYMBOL, e), loc), 1039 ((EKAbs (CSYMBOL, e), loc),
1059 (TKFun (CSYMBOL, t), loc)) 1040 (TKFun (CSYMBOL, t), loc))
1212 branch : pat DARROW eexp (pat, eexp) 1193 branch : pat DARROW eexp (pat, eexp)
1213 1194
1214 branchs: ([]) 1195 branchs: ([])
1215 | BAR branch branchs (branch :: branchs) 1196 | BAR branch branchs (branch :: branchs)
1216 1197
1217 pat : pterm (pterm) 1198 patS : pterm (pterm)
1199 | pterm DCOLON patS (let
1200 val loc = s (ptermleft, patSright)
1201 in
1202 (PCon (["Basis"], "Cons", SOME (PRecord ([("1", pterm),
1203 ("2", patS)], false), loc)),
1204 loc)
1205 end)
1206 | patS COLON cexp (PAnnot (patS, cexp), s (patSleft, cexpright))
1207
1208 pat : patS (patS)
1218 | cpath pterm (PCon (#1 cpath, #2 cpath, SOME pterm), s (cpathleft, ptermright)) 1209 | cpath pterm (PCon (#1 cpath, #2 cpath, SOME pterm), s (cpathleft, ptermright))
1219 | pterm DCOLON pat (let
1220 val loc = s (ptermleft, patright)
1221 in
1222 (PCon (["Basis"], "Cons", SOME (PRecord ([("1", pterm),
1223 ("2", pat)], false), loc)),
1224 loc)
1225 end)
1226 1210
1227 pterm : SYMBOL (PVar SYMBOL, s (SYMBOLleft, SYMBOLright)) 1211 pterm : SYMBOL (PVar SYMBOL, s (SYMBOLleft, SYMBOLright))
1228 | cpath (PCon (#1 cpath, #2 cpath, NONE), s (cpathleft, cpathright)) 1212 | cpath (PCon (#1 cpath, #2 cpath, NONE), s (cpathleft, cpathright))
1229 | UNDER (PWild, s (UNDERleft, UNDERright)) 1213 | UNDER (PWild, s (UNDERleft, UNDERright))
1230 | INT (PPrim (Prim.Int INT), s (INTleft, INTright)) 1214 | INT (PPrim (Prim.Int INT), s (INTleft, INTright))