Elaborating cfold

9 files changed, 80 insertions, 19 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 43837413..ea00d199 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -59,6 +59,7 @@ datatype con' =
 
        | CRecord of kind * (con * con) list
        | CConcat of con * con
+       | CFold of kind * kind
 
        | CError
        | CUnif of kind * string * con option ref
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 4c02c495..2b515a03 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -152,6 +152,7 @@ fun p_con' par env (c, _) =
                                               string "++",
                                               space,
                                               p_con env c2])
+      | CFold _ => string "fold"
 
       | CError => string "<ERROR>"
       | CUnif (_, _, ref (SOME c)) => p_con' par env c
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 2d075fb4..7892211c 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -143,6 +143,12 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                          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
diff --git a/src/elaborate.sml b/src/elaborate.sml
index cc9c2f80..d6e3085d 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -115,6 +115,7 @@ datatype con_error =
          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 @@ fun conError env err =
                      ("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 @@ fun elabKind (k, loc) =
       | 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 @@ fun elabCon env (c, loc) =
             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 @@ fun elabCon env (c, loc) =
                                    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 @@ fun elabCon env (c, loc) =
             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 @@ fun kindof env (c, loc) =
 
       | 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 @@ and hnormCon env (cAll as (c, loc)) =
         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) =>
diff --git a/src/explify.sml b/src/explify.sml
index 0c3f5f1f..79e3b07f 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -59,6 +59,7 @@ fun explifyCon (c, loc) =
 
       | 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
diff --git a/src/lacweb.grm b/src/lacweb.grm
index e36630ae..c1cf6712 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -40,7 +40,7 @@ val s = ErrorMsg.spanOf
  | 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   : capps                          (capps)
 
        | 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 @@ cterm  : LPAREN cexp RPAREN             (#1 cexp, s (LPARENleft, RPARENright))
 
        | 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)])
diff --git a/src/lacweb.lex b/src/lacweb.lex
index a821cc9e..038e591f 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -146,6 +146,7 @@ realconst = [0-9]+\.[0-9]*;
 <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));
diff --git a/src/source.sml b/src/source.sml
index 9ea1ea20..2246399b 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -51,12 +51,13 @@ datatype con' =
 
        | 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
 
diff --git a/src/source_print.sml b/src/source_print.sml
index ca72c014..b4496a7a 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -92,17 +92,24 @@ fun p_con' par (c, _) =
       | 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 @@ fun p_con' par (c, _) =
                                               string "++",
                                               space,
                                               p_con c2])
+      | CFold => string "fold"
       | CWild k => box [string "(_",
                         space,
                         string "::",