Mercurial > urweb
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