changeset 71:6431b315a1e3

Elaborate efold
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 11:09:30 -0400
parents 2e0f3b21fb85
children 0ee10f4d73cf
files src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/source.sml src/source_print.sml tests/cfold.lac tests/efold.lac
diffstat 10 files changed, 76 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab.sml	Thu Jun 26 10:02:34 2008 -0400
+++ b/src/elab.sml	Thu Jun 26 11:09:30 2008 -0400
@@ -78,6 +78,7 @@
 
        | ERecord of (con * exp * con) list
        | EField of exp * con * { field : con, rest : con }
+       | EFold of kind
 
        | EError
 
--- a/src/elab_print.sml	Thu Jun 26 10:02:34 2008 -0400
+++ b/src/elab_print.sml	Thu Jun 26 11:09:30 2008 -0400
@@ -88,10 +88,11 @@
                           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 @@
             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
--- a/src/elab_util.sml	Thu Jun 26 10:02:34 2008 -0400
+++ b/src/elab_util.sml	Thu Jun 26 11:09:30 2008 -0400
@@ -273,6 +273,11 @@
                                                   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
--- a/src/elaborate.sml	Thu Jun 26 10:02:34 2008 -0400
+++ b/src/elaborate.sml	Thu Jun 26 11:09:30 2008 -0400
@@ -665,6 +665,15 @@
                                      (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 @@
         (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 @@
           | (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 @@
       | 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 @@
 
       | 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 @@
             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 =
--- a/src/explify.sml	Thu Jun 26 10:02:34 2008 -0400
+++ b/src/explify.sml	Thu Jun 26 11:09:30 2008 -0400
@@ -79,6 +79,7 @@
       | 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)
 
--- a/src/lacweb.grm	Thu Jun 26 10:02:34 2008 -0400
+++ b/src/lacweb.grm	Thu Jun 26 11:09:30 2008 -0400
@@ -249,6 +249,8 @@
        | 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)
--- a/src/source.sml	Thu Jun 26 10:02:34 2008 -0400
+++ b/src/source.sml	Thu Jun 26 11:09:30 2008 -0400
@@ -93,6 +93,7 @@
 
        | ERecord of (con * exp) list
        | EField of exp * con
+       | EFold
 
 withtype exp = exp' located
 
--- a/src/source_print.sml	Thu Jun 26 10:02:34 2008 -0400
+++ b/src/source_print.sml	Thu Jun 26 11:09:30 2008 -0400
@@ -201,7 +201,7 @@
       | EField (e, c) => box [p_exp' true e,
                               string ".",
                               p_con' true c]
-
+      | EFold => string "fold"
 
 and p_exp e = p_exp' false e
 
--- a/tests/cfold.lac	Thu Jun 26 10:02:34 2008 -0400
+++ b/tests/cfold.lac	Thu Jun 26 11:09:30 2008 -0400
@@ -1,12 +1,15 @@
 con currier = fold (fn nm => fn t => fn acc => t -> acc) {}
 
-con greenCurry = currier []
+con greenCurryIngredients :: {Type} = []
+con greenCurry = currier greenCurryIngredients
 val greenCurry : greenCurry = {}
 
-con redCurry = currier [A = int, B = string]
+con redCurryIngredients = [A = int, B = string]
+con redCurry = currier redCurryIngredients
 val redCurry : redCurry = fn x : int => fn y : string => {}
 
-con yellowCurry = currier [A = string, B = int, C = float]
+con yellowCurryIngredients = [A = string, B = int, C = float]
+con yellowCurry = currier yellowCurryIngredients
 val yellowCurry : yellowCurry = fn x => fn y => fn z => {}
 
 val main = yellowCurry
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/efold.lac	Thu Jun 26 11:09:30 2008 -0400
@@ -0,0 +1,6 @@
+val currier : rs :: {Type} -> Cfold.currier rs =
+        fold [Cfold.currier] (fn nm :: Name => fn t :: Type => fn rest :: {Type} => fn acc => fn x => acc) {}
+
+val greenCurry : Cfold.greenCurry = currier [Cfold.greenCurryIngredients]
+val redCurry : Cfold.redCurry = currier [Cfold.redCurryIngredients]
+val yellowCurry : Cfold.yellowCurry = currier [Cfold.yellowCurryIngredients]