changeset 411:06fcddcd20d3

Sum demo, minus inference of {Unit}s
author Adam Chlipala <adamc@hcoop.net>
date Tue, 21 Oct 2008 19:24:39 -0400
parents c5a3d223f157
children df4cbd90a26e
files demo/link.ur demo/sum.ur demo/sum.urp demo/sum.urs lib/top.ur lib/top.urs src/elaborate.sml
diffstat 7 files changed, 47 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/demo/link.ur	Tue Oct 21 18:44:52 2008 -0400
+++ b/demo/link.ur	Tue Oct 21 19:24:39 2008 -0400
@@ -3,5 +3,5 @@
 </body></xml>
 
 fun main () = return <xml><body>
-  <a link={target ()}>Go there</a>
+  <a link={target}>Go there</a>
 </body></xml>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/sum.ur	Tue Oct 21 19:24:39 2008 -0400
@@ -0,0 +1,9 @@
+fun sum (fs :: {Unit}) (x : $(mapUT int fs)) =
+    foldUR [int] [fn _ => int]
+    (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] n acc => n + acc)
+    0 [fs] x
+
+fun main () = return <xml><body>
+  {[sum [[A, B]] {A = 0, B = 1}]}<br/>
+  {[sum [[C, D, E]] {C = 2, D = 3, E = 4}]}
+</body></xml>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/sum.urp	Tue Oct 21 19:24:39 2008 -0400
@@ -0,0 +1,2 @@
+
+sum
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/sum.urs	Tue Oct 21 19:24:39 2008 -0400
@@ -0,0 +1,1 @@
+val main : unit -> transaction page
--- a/lib/top.ur	Tue Oct 21 18:44:52 2008 -0400
+++ b/lib/top.ur	Tue Oct 21 19:24:39 2008 -0400
@@ -6,6 +6,9 @@
 con mapTT (f :: Type -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
                                          [nm = f t] ++ acc) []
 
+con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
+                                     [nm = f] ++ acc) []
+
 con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
                                                    [nm = f t] ++ acc) []
 
@@ -22,6 +25,17 @@
 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) =
     cdata (@show sh v)
 
+fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
+           (f : nm :: Name -> rest :: {Unit}
+                -> fn [[nm] ~ rest] =>
+                      tf -> tr rest -> tr ([nm] ++ rest))
+           (i : tr []) =
+    fold [fn r :: {Unit} => $(mapUT tf r) -> tr r]
+             (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) (acc : $(mapUT tf rest) -> tr rest)
+                              [[nm] ~ rest] (r : $([nm = tf] ++ mapUT tf rest)) =>
+                 f [nm] [rest] r.nm (acc (r -- nm)))
+             (fn _ => i)
+
 fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
            (f : nm :: Name -> t :: Type -> rest :: {Type}
                 -> fn [[nm] ~ rest] =>
--- a/lib/top.urs	Tue Oct 21 18:44:52 2008 -0400
+++ b/lib/top.urs	Tue Oct 21 19:24:39 2008 -0400
@@ -6,6 +6,9 @@
 con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] =>
                                              [nm = f t] ++ acc) []
 
+con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
+                                     [nm = f] ++ acc) []
+
 con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
                                                        [nm = f t] ++ acc) []
 
@@ -20,6 +23,12 @@
 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
           -> xml ctx use []
 
+val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
+             -> (nm :: Name -> rest :: {Unit}
+                 -> fn [[nm] ~ rest] =>
+                       tf -> tr rest -> tr ([nm] ++ rest))
+             -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r
+
 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
              -> (nm :: Name -> t :: Type -> rest :: {Type}
                  -> fn [[nm] ~ rest] =>
--- a/src/elaborate.sml	Tue Oct 21 18:44:52 2008 -0400
+++ b/src/elaborate.sml	Tue Oct 21 19:24:39 2008 -0400
@@ -821,17 +821,20 @@
              gs1 @ gs2 @ gs3 @ gs4
          end
        | _ =>
-         let
-             val (c1, gs1) = hnormCon (env, denv) c1
-             val (c2, gs2) = hnormCon (env, denv) c2
-         in
+         case (kindof env c1, kindof env c2) of
+             ((L'.KUnit, _), (L'.KUnit, _)) => []
+           | _ =>
              let
-                 val gs3 = unifyCons'' (env, denv) c1 c2
+                 val (c1, gs1) = hnormCon (env, denv) c1
+                 val (c2, gs2) = hnormCon (env, denv) c2
              in
-                 gs1 @ gs2 @ gs3
+                 let
+                     val gs3 = unifyCons'' (env, denv) c1 c2
+                 in
+                     gs1 @ gs2 @ gs3
+                 end
+                 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
              end
-             handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
-         end
 
  and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
      let