# HG changeset patch # User Adam Chlipala # Date 1224631479 14400 # Node ID 06fcddcd20d3c9b8bc9461b0d4565a84e467c18a # Parent c5a3d223f157ea0da2c80d1ea1eba41a96e0002c Sum demo, minus inference of {Unit}s diff -r c5a3d223f157 -r 06fcddcd20d3 demo/link.ur --- 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 @@ fun main () = return - Go there + Go there diff -r c5a3d223f157 -r 06fcddcd20d3 demo/sum.ur --- /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 + {[sum [[A, B]] {A = 0, B = 1}]}
+ {[sum [[C, D, E]] {C = 2, D = 3, E = 4}]} + diff -r c5a3d223f157 -r 06fcddcd20d3 demo/sum.urp --- /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 diff -r c5a3d223f157 -r 06fcddcd20d3 demo/sum.urs --- /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 diff -r c5a3d223f157 -r 06fcddcd20d3 lib/top.ur --- 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] => diff -r c5a3d223f157 -r 06fcddcd20d3 lib/top.urs --- 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] => diff -r c5a3d223f157 -r 06fcddcd20d3 src/elaborate.sml --- 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