Mercurial > urweb

changeset 67:9f89f0b00b84

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating cfold
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 09:48:54 -0400
parents 1ec5703c09c4
children c1e21ab42896
files src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/lacweb.lex src/source.sml src/source_print.sml tests/cfold.lac
diffstat 10 files changed, 90 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab.sml	Thu Jun 26 09:09:30 2008 -0400
+++ b/src/elab.sml	Thu Jun 26 09:48:54 2008 -0400
@@ -59,6 +59,7 @@
 
        | CRecord of kind * (con * con) list
        | CConcat of con * con
+       | CFold of kind * kind
 
        | CError
        | CUnif of kind * string * con option ref
--- a/src/elab_print.sml	Thu Jun 26 09:09:30 2008 -0400
+++ b/src/elab_print.sml	Thu Jun 26 09:48:54 2008 -0400
@@ -152,6 +152,7 @@
                                               string "++",
                                               space,
                                               p_con env c2])
+      | CFold _ => string "fold"
 
       | CError => string "<ERROR>"
       | CUnif (_, _, ref (SOME c)) => p_con' par env c
--- a/src/elab_util.sml	Thu Jun 26 09:09:30 2008 -0400
+++ b/src/elab_util.sml	Thu Jun 26 09:48:54 2008 -0400
@@ -143,6 +143,12 @@
                          S.map2 (mfc ctx c2,
                               fn c2' =>
                                  (CConcat (c1', c2'), loc)))
+              | CFold (k1, k2) =>
+                S.bind2 (mfk k1,
+                         fn k1' =>
+                            S.map2 (mfk k2,
+                                    fn k2' =>
+                                       (CFold (k1', k2'), loc)))
 
               | CError => S.return2 cAll
               | CUnif (_, _, ref (SOME c)) => mfc' ctx c
--- a/src/elaborate.sml	Thu Jun 26 09:09:30 2008 -0400
+++ b/src/elaborate.sml	Thu Jun 26 09:48:54 2008 -0400
@@ -115,6 +115,7 @@
          UnboundCon of ErrorMsg.span * string
        | UnboundStrInCon of ErrorMsg.span * string
        | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
+       | DuplicateField of ErrorMsg.span * string
 
 fun conError env err =
     case err of
@@ -128,6 +129,8 @@
                      ("Have kind", p_kind k1),
                      ("Need kind", p_kind k2)];
          kunifyError kerr)
+      | DuplicateField (loc, s) =>
+        ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
 
 fun checkKind env c k1 k2 =
     unifyKinds k1 k2
@@ -198,6 +201,14 @@
       | L.KRecord k => (L'.KRecord (elabKind k), loc)
       | L.KWild => kunif ()
 
+fun foldKind (dom, ran, loc)=
+    (L'.KArrow ((L'.KArrow ((L'.KName, loc),
+                            (L'.KArrow (dom,
+                                        (L'.KArrow (ran, ran), loc)), loc)), loc),
+                (L'.KArrow (ran,
+                            (L'.KArrow ((L'.KRecord dom, loc),
+                                        ran), loc)), loc)), loc)
+
 fun elabCon env (c, loc) =
     case c of
         L.CAnnot (c, k) =>
@@ -278,9 +289,11 @@
             checkKind env c2' k2 dom;
             ((L'.CApp (c1', c2'), loc), ran)
         end
-      | L.CAbs (x, k, t) =>
+      | L.CAbs (x, ko, t) =>
         let
-            val k' = elabKind k
+            val k' = case ko of
+                         NONE => kunif ()
+                       | SOME k => elabKind k
             val env' = E.pushCRel env x k'
             val (t', tk) = elabCon env' t
         in
@@ -304,8 +317,11 @@
                                    checkKind env c' ck k;
                                    (x', c')
                                end) xcs
+
+            val rc = (L'.CRecord (k, xcs'), loc)
+            (* Add duplicate field checking later. *)
         in
-            ((L'.CRecord (k, xcs'), loc), (L'.KRecord k, loc))
+            (rc, (L'.KRecord k, loc))
         end
       | L.CConcat (c1, c2) =>
         let
@@ -318,6 +334,14 @@
             checkKind env c2' k2 k;
             ((L'.CConcat (c1', c2'), loc), k)
         end
+      | L.CFold =>
+        let
+            val dom = kunif ()
+            val ran = kunif ()
+        in
+            ((L'.CFold (dom, ran), loc),
+             foldKind (dom, ran, loc))
+        end
 
       | L.CWild k =>
         let
@@ -473,6 +497,7 @@
 
       | L'.CRecord (k, _) => (L'.KRecord k, loc)
       | L'.CConcat (c, _) => kindof env c
+      | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
 
       | L'.CError => kerror
       | L'.CUnif (k, _, _) => k
@@ -624,10 +649,25 @@
         end
 
       | L'.CApp (c1, c2) =>
-        (case hnormCon env c1 of
-             (L'.CAbs (_, _, cb), _) =>
+        (case #1 (hnormCon env c1) of
+             L'.CAbs (_, _, cb) =>
              ((hnormCon env (subConInCon (0, c2) cb))
               handle SynUnif => cAll)
+           | L'.CApp (c', i) =>
+             (case #1 (hnormCon env c') of
+                  L'.CApp (c', f) =>
+                  (case #1 (hnormCon env c') of
+                       L'.CFold ks =>
+                       (case #1 (hnormCon env c2) of
+                            L'.CRecord (_, []) => hnormCon env i
+                          | L'.CRecord (k, (x, c) :: rest) =>
+                            hnormCon env
+                                     (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
+                                               (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
+                                                         (L'.CRecord (k, rest), loc)), loc)), loc)
+                          | _ => cAll)
+                     | _ => cAll)
+                | _ => cAll)
            | _ => cAll)
 
       | L'.CConcat (c1, c2) =>
--- a/src/explify.sml	Thu Jun 26 09:09:30 2008 -0400
+++ b/src/explify.sml	Thu Jun 26 09:48:54 2008 -0400
@@ -59,6 +59,7 @@
 
       | L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc)
       | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc)
+      | L.CFold _ => raise Fail "Explify CFold"
 
       | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc)
       | L.CUnif (_, _, ref (SOME c)) => explifyCon c
--- a/src/lacweb.grm	Thu Jun 26 09:09:30 2008 -0400
+++ b/src/lacweb.grm	Thu Jun 26 09:48:54 2008 -0400
@@ -40,7 +40,7 @@
  | SYMBOL of string | CSYMBOL of string
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER
- | CON | LTYPE | VAL
+ | CON | LTYPE | VAL | FOLD
  | TYPE | NAME
  | ARROW | LARROW | DARROW
  | FN | PLUSPLUS | DOLLAR
@@ -190,7 +190,8 @@
 
        | cexp PLUSPLUS cexp             (CConcat (cexp1, cexp2), s (cexp1left, cexp1right))
 
-       | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, kind, cexp), s (FNleft, cexpright))
+       | FN SYMBOL DARROW cexp          (CAbs (SYMBOL, NONE, cexp), s (FNleft, cexpright))
+       | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, SOME kind, cexp), s (FNleft, cexpright))
 
        | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
 
@@ -214,6 +215,7 @@
 
        | path                           (CVar path, s (pathleft, pathright))
        | UNDER                          (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
+       | FOLD                           (CFold, s (FOLDleft, FOLDright))
 
 rcon   :                                ([])
        | ident EQ cexp                  ([(ident, cexp)])
--- a/src/lacweb.lex	Thu Jun 26 09:09:30 2008 -0400
+++ b/src/lacweb.lex	Thu Jun 26 09:48:54 2008 -0400
@@ -146,6 +146,7 @@
 <INITIAL> "type"      => (Tokens.LTYPE (pos yypos, pos yypos + size yytext));
 <INITIAL> "val"       => (Tokens.VAL (pos yypos, pos yypos + size yytext));
 <INITIAL> "fn"        => (Tokens.FN (pos yypos, pos yypos + size yytext));
+<INITIAL> "fold"      => (Tokens.FOLD (pos yypos, pos yypos + size yytext));
 
 <INITIAL> "structure" => (Tokens.STRUCTURE (pos yypos, pos yypos + size yytext));
 <INITIAL> "signature" => (Tokens.SIGNATURE (pos yypos, pos yypos + size yytext));
--- a/src/source.sml	Thu Jun 26 09:09:30 2008 -0400
+++ b/src/source.sml	Thu Jun 26 09:48:54 2008 -0400
@@ -51,12 +51,13 @@
 
        | CVar of string list * string
        | CApp of con * con
-       | CAbs of string * kind * con
+       | CAbs of string * kind option * con
 
        | CName of string
 
        | CRecord of (con * con) list
        | CConcat of con * con
+       | CFold
 
        | CWild of kind
 
--- a/src/source_print.sml	Thu Jun 26 09:09:30 2008 -0400
+++ b/src/source_print.sml	Thu Jun 26 09:48:54 2008 -0400
@@ -92,17 +92,24 @@
       | CApp (c1, c2) => parenIf par (box [p_con c1,
                                            space,
                                            p_con' true c2])
-      | CAbs (x, k, c) => parenIf par (box [string "fn",
-                                            space,
-                                            string x,
-                                            space,
-                                            string "::",
-                                            space,
-                                            p_kind k,
-                                            space,
-                                            string "=>",
-                                            space,
-                                            p_con c])
+      | CAbs (x, NONE, c) => parenIf par (box [string "fn",
+                                               space,
+                                               string x,
+                                               space,
+                                               string "=>",
+                                               space,
+                                               p_con c])
+      | CAbs (x, SOME k, c) => parenIf par (box [string "fn",
+                                                 space,
+                                                 string x,
+                                                 space,
+                                                 string "::",
+                                                 space,
+                                                 p_kind k,
+                                                 space,
+                                                 string "=>",
+                                                 space,
+                                                 p_con c])
 
       | CName s => box [string "#", string s]
 
@@ -119,6 +126,7 @@
                                               string "++",
                                               space,
                                               p_con c2])
+      | CFold => string "fold"
       | CWild k => box [string "(_",
                         space,
                         string "::",
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/cfold.lac	Thu Jun 26 09:48:54 2008 -0400
@@ -0,0 +1,10 @@
+con currier = fold (fn nm => fn t => fn acc => t -> acc) {}
+
+con greenCurry = currier []
+val greenCurry : greenCurry = {}
+
+con redCurry = currier [A = int, B = string]
+val redCurry : redCurry = fn x : int => fn y : string => {}
+
+con yellowCurry = currier [A = string, B = int, C = float]
+val yellowCurry : yellowCurry = fn x => fn y => fn z => {}