fn-pattern code in but not tested yet; hello compiles

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))