Elaborate efold

8 files changed, 64 insertions, 6 deletions

diff --git a/src/elab.sml b/src/elab.sml
index ea00d199..7c3ec6b1 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -78,6 +78,7 @@ datatype exp' =
 
        | ERecord of (con * exp * con) list
        | EField of exp * con * { field : con, rest : con }
+       | EFold of kind
 
        | EError
 
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 2b515a03..085caac7 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -88,10 +88,11 @@ fun p_con' par env (c, _) =
                           p_con' true env c]
 
       | CRel n =>
-        if !debug then
-            string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n)
-        else
-            string (#1 (E.lookupCRel env n))
+        ((if !debug then
+              string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n)
+          else
+              string (#1 (E.lookupCRel env n)))
+         handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
       | CNamed n =>
         ((if !debug then
               string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
@@ -248,7 +249,8 @@ fun p_exp' par env (e, _) =
             box [p_exp' true env e,
                  string ".",
                  p_con' true env c]
-            
+      | EFold _ => string "fold"            
+
       | EError => string "<ERROR>"
 
 and p_exp env = p_exp' false env
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 7892211c..f764395d 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -273,6 +273,11 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                                                   fn rest' =>
                                                      (EField (e', c', {field = field', rest = rest'}), loc)))))
 
+              | EFold k =>
+                S.map2 (mfk k,
+                         fn k' =>
+                            (EFold k', loc))
+
               | EError => S.return2 eAll
     in
         mfe
diff --git a/src/elaborate.sml b/src/elaborate.sml
index d6e3085d..e31bf908 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -665,6 +665,15 @@ and hnormCon env (cAll as (c, loc)) =
                                      (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)
+                          | L'.CConcat ((L'.CRecord (k, (x, c) :: rest), _), rest') =>
+                            let
+                                val rest'' = (L'.CConcat ((L'.CRecord (k, rest), loc), rest'), loc)
+                            in
+                                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),
+                                                             rest''), loc)), loc)
+                            end
                           | _ => cAll)
                      | _ => cAll)
                 | _ => cAll)
@@ -674,6 +683,9 @@ and hnormCon env (cAll as (c, loc)) =
         (case (hnormCon env c1, hnormCon env c2) of
              ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) =>
              (L'.CRecord (k, xcs1 @ xcs2), loc)
+           | ((L'.CRecord (_, []), _), c2') => c2'
+           | ((L'.CConcat (c11, c12), loc), c2') =>
+             hnormCon env (L'.CConcat (c11, (L'.CConcat (c12, c2'), loc)), loc)
            | _ => cAll)
 
       | _ => cAll
@@ -758,6 +770,10 @@ and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =
           | (L'.CConcat _, _) => isRecord ()
           | (_, L'.CConcat _) => isRecord ()
 
+          | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
+            (unifyKinds dom1 dom2;
+             unifyKinds ran1 ran2)
+
           | _ => err CIncompatible
     end
 
@@ -804,6 +820,28 @@ fun primType env p =
       | P.Float _ => !float
       | P.String _ => !string
 
+fun recCons (k, nm, v, rest, loc) =
+    (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc),
+                 rest), loc)
+
+fun foldType (dom, loc) =
+    (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
+               (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
+                                    (L'.TCFun (L'.Explicit, "v", dom,
+                                               (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
+                                                          (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
+                                                                    (L'.CApp ((L'.CRel 3, loc),
+                                                                              recCons (dom,
+                                                                                       (L'.CRel 2, loc),
+                                                                                       (L'.CRel 1, loc),
+                                                                                       (L'.CRel 0, loc),
+                                                                                       loc)), loc)), loc)),
+                                                loc)), loc)), loc),
+                         (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
+                                   (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
+                                              (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
+                          loc)), loc)), loc)
+
 fun typeof env (e, loc) =
     case e of
         L'.EPrim p => primType env p
@@ -836,6 +874,7 @@ fun typeof env (e, loc) =
 
       | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc)
       | L'.EField (_, _, {field, ...}) => field
+      | L'.EFold dom => foldType (dom, loc)
 
       | L'.EError => cerror
 
@@ -988,6 +1027,13 @@ fun elabExp env (e, loc) =
             checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc);
             ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft)
         end
+
+      | L.EFold =>
+        let
+            val dom = kunif ()
+        in
+            ((L'.EFold dom, loc), foldType (dom, loc))
+        end
             
 
 datatype decl_error =
diff --git a/src/explify.sml b/src/explify.sml
index 0a84c5fe..86d408c6 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -79,6 +79,7 @@ fun explifyExp (e, loc) =
       | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (explifyCon c, explifyExp e, explifyCon t)) xes), loc)
       | L.EField (e1, c, {field, rest}) => (L'.EField (explifyExp e1, explifyCon c,
                                                        {field = explifyCon field, rest = explifyCon rest}), loc)
+      | L.EFold _ => raise Fail "Explify EFold"
 
       | L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc)
 
diff --git a/src/lacweb.grm b/src/lacweb.grm
index c1cf6712..c42b5eb5 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -249,6 +249,8 @@ eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))
        | FLOAT                          (EPrim (Prim.Float FLOAT), s (FLOATleft, FLOATright))
        | STRING                         (EPrim (Prim.String STRING), s (STRINGleft, STRINGright))
 
+       | FOLD                           (EFold, s (FOLDleft, FOLDright))
+
 rexp   :                                ([])
        | ident EQ eexp                  ([(ident, eexp)])
        | ident EQ eexp COMMA rexp       ((ident, eexp) :: rexp)
diff --git a/src/source.sml b/src/source.sml
index 2246399b..d36e86ca 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -93,6 +93,7 @@ datatype exp' =
 
        | ERecord of (con * exp) list
        | EField of exp * con
+       | EFold
 
 withtype exp = exp' located
 
diff --git a/src/source_print.sml b/src/source_print.sml
index b4496a7a..aa880e08 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -201,7 +201,7 @@ fun p_exp' par (e, _) =
       | EField (e, c) => box [p_exp' true e,
                               string ".",
                               p_con' true c]
-
+      | EFold => string "fold"
 
 and p_exp e = p_exp' false e