summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/elaborate.sml10
-rw-r--r--src/source.sml1
-rw-r--r--src/source_print.sml6
-rw-r--r--src/urweb.grm118
4 files changed, 67 insertions, 68 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 49b826eb..6f8575db 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1291,7 +1291,15 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
(L'.TRecord c, loc)),
(env, bound))
end
-
+
+ | L.PAnnot (p, t) =>
+ let
+ val ((p', pt), (env, bound)) = elabPat (p, (env, bound))
+ val (t', k, _) = elabCon (env, D.empty) t
+ in
+ checkPatCon env p' pt t';
+ ((p', t'), (env, bound))
+ end
end
(* This exhaustiveness checking follows Luc Maranget's paper "Warnings for pattern matching." *)
diff --git a/src/source.sml b/src/source.sml
index 0f62cadd..bfa270d8 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -109,6 +109,7 @@ and pat' =
| PPrim of Prim.t
| PCon of string list * string * pat option
| PRecord of (string * pat) list * bool
+ | PAnnot of pat * con
and exp' =
EAnnot of exp * con
diff --git a/src/source_print.sml b/src/source_print.sml
index b4f9bfd3..a16b5bb1 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -207,6 +207,12 @@ fun p_pat' par (p, _) =
string "}"]
end
+ | PAnnot (p, t) => box [p_pat p,
+ space,
+ string ":",
+ space,
+ p_con t]
+
and p_pat x = p_pat' false x
fun p_exp' par (e, _) =
diff --git a/src/urweb.grm b/src/urweb.grm
index bfb230a6..638ede12 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -178,6 +178,11 @@ datatype prop_kind = Delete | Update
datatype attr = Class of exp | Normal of con * exp
+fun patType loc (p : pat) =
+ case #1 p of
+ PAnnot (_, t) => t
+ | _ => (CWild (KType, loc), loc)
+
%%
%header (functor UrwebLrValsFn(structure Token : TOKEN))
@@ -290,6 +295,7 @@ datatype attr = Class of exp | Normal of con * exp
| earg of exp * con -> exp * con
| eargp of exp * con -> exp * con
+ | earga of exp * con -> exp * con
| eargs of exp * con -> exp * con
| eargl of exp * con -> exp * con
| eargl2 of exp * con -> exp * con
@@ -297,6 +303,7 @@ datatype attr = Class of exp | Normal of con * exp
| branch of pat * exp
| branchs of (pat * exp) list
| pat of pat
+ | patS of pat
| pterm of pat
| rpat of (string * pat) list * bool
| ptuple of pat list
@@ -971,79 +978,53 @@ eargl : eargp eargp (eargp1 o eargp2)
eargl2 : (fn x => x)
| eargp eargl2 (eargp o eargl2)
-earg : SYMBOL kcolon kind (fn (e, t) =>
- let
- val loc = s (SYMBOLleft, kindright)
- in
- ((ECAbs (kcolon, SYMBOL, kind, e), loc),
- (TCFun (kcolon, SYMBOL, kind, t), loc))
- end)
- | SYMBOL COLON cexp (fn (e, t) =>
+earg : patS (fn (e, t) =>
let
- val loc = s (SYMBOLleft, cexpright)
+ val loc = s (patSleft, patSright)
+ val pt = patType loc patS
+
+ val e' = case #1 patS of
+ PVar x => (EAbs (x, NONE, e), loc)
+ | _ => (EAbs ("$x", SOME pt,
+ (ECase ((EVar ([], "$x", DontInfer),
+ loc),
+ [(patS, e)]), loc)), loc)
in
- ((EAbs (SYMBOL, SOME cexp, e), loc),
- (TFun (cexp, t), loc))
+ (e', (TFun (pt, t), loc))
end)
- | UNDER COLON cexp (fn (e, t) =>
- let
- val loc = s (UNDERleft, cexpright)
- in
- ((EAbs ("_", SOME cexp, e), loc),
- (TFun (cexp, t), loc))
- end)
- | eargp (eargp)
+ | earga (earga)
-eargp : SYMBOL (fn (e, t) =>
- let
- val loc = s (SYMBOLleft, SYMBOLright)
- in
- ((EAbs (SYMBOL, NONE, e), loc),
- (TFun ((CWild (KType, loc), loc), t), loc))
- end)
- | UNIT (fn (e, t) =>
+eargp : pterm (fn (e, t) =>
let
- val loc = s (UNITleft, UNITright)
- val t' = (TRecord (CRecord [], loc), loc)
+ val loc = s (ptermleft, ptermright)
+ val pt = patType loc pterm
+
+ val e' = case #1 pterm of
+ PVar x => (EAbs (x, NONE, e), loc)
+ | _ => (EAbs ("$x", SOME pt,
+ (ECase ((EVar ([], "$x", DontInfer),
+ loc),
+ [(pterm, e)]), loc)), loc)
in
- ((EAbs ("_", SOME t', e), loc),
- (TFun (t', t), loc))
+ (e', (TFun (pt, t), loc))
end)
- | UNDER (fn (e, t) =>
- let
- val loc = s (UNDERleft, UNDERright)
- in
- ((EAbs ("_", NONE, e), loc),
- (TFun ((CWild (KType, loc), loc), t), loc))
- end)
- | LPAREN SYMBOL kcolon kind RPAREN(fn (e, t) =>
+ | earga (earga)
+
+earga : LBRACK SYMBOL RBRACK (fn (e, t) =>
let
- val loc = s (LPARENleft, RPARENright)
+ val loc = s (LBRACKleft, RBRACKright)
+ val kind = (KWild, loc)
+ in
+ ((ECAbs (Implicit, SYMBOL, kind, e), loc),
+ (TCFun (Implicit, SYMBOL, kind, t), loc))
+ end)
+ | LBRACK SYMBOL kcolon kind RBRACK(fn (e, t) =>
+ let
+ val loc = s (LBRACKleft, RBRACKright)
in
((ECAbs (kcolon, SYMBOL, kind, e), loc),
(TCFun (kcolon, SYMBOL, kind, t), loc))
end)
- | LPAREN SYMBOL COLON cexp RPAREN (fn (e, t) =>
- let
- val loc = s (LPARENleft, RPARENright)
- in
- ((EAbs (SYMBOL, SOME cexp, e), loc),
- (TFun (cexp, t), loc))
- end)
- | LPAREN UNDER COLON cexp RPAREN (fn (e, t) =>
- let
- val loc = s (LPARENleft, RPARENright)
- in
- ((EAbs ("_", SOME cexp, e), loc),
- (TFun (cexp, t), loc))
- end)
- | LPAREN cexp TWIDDLE cexp RPAREN (fn (e, t) =>
- let
- val loc = s (LPARENleft, RPARENright)
- in
- ((EDisjoint (cexp1, cexp2, e), loc),
- (TDisjoint (cexp1, cexp2, t), loc))
- end)
| LBRACK cexp TWIDDLE cexp RBRACK(fn (e, t) =>
let
val loc = s (LBRACKleft, RBRACKright)
@@ -1051,7 +1032,7 @@ eargp : SYMBOL (fn (e, t) =>
((EDisjoint (cexp1, cexp2, e), loc),
(TDisjoint (cexp1, cexp2, t), loc))
end)
- | CSYMBOL (fn (e, t) =>
+ | LBRACK CSYMBOL RBRACK (fn (e, t) =>
let
val loc = s (CSYMBOLleft, CSYMBOLright)
in
@@ -1214,15 +1195,18 @@ branch : pat DARROW eexp (pat, eexp)
branchs: ([])
| BAR branch branchs (branch :: branchs)
-pat : pterm (pterm)
- | cpath pterm (PCon (#1 cpath, #2 cpath, SOME pterm), s (cpathleft, ptermright))
- | pterm DCOLON pat (let
- val loc = s (ptermleft, patright)
+patS : pterm (pterm)
+ | pterm DCOLON patS (let
+ val loc = s (ptermleft, patSright)
in
(PCon (["Basis"], "Cons", SOME (PRecord ([("1", pterm),
- ("2", pat)], false), loc)),
+ ("2", patS)], false), loc)),
loc)
end)
+ | patS COLON cexp (PAnnot (patS, cexp), s (patSleft, cexpright))
+
+pat : patS (patS)
+ | cpath pterm (PCon (#1 cpath, #2 cpath, SOME pterm), s (cpathleft, ptermright))
pterm : SYMBOL (PVar SYMBOL, s (SYMBOLleft, SYMBOLright))
| cpath (PCon (#1 cpath, #2 cpath, NONE), s (cpathleft, cpathright))
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-17 23:04:11 +0000