diff lib/top.urs @ 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 fa2d25fe75ce
children ad7e854a518c
line wrap: on
line diff
--- 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] =>