diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-10-21 19:24:39 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-10-21 19:24:39 -0400 |
| commit | 17b3f5af99c07d7361fb99124412aff1768cfe13 (patch) | |
| tree | fcfbcfaf492be1aa13c484eea28cfedaf565ed6c | |
| parent | d66bb9f256db65e3487dec361a4a5a9d7ee238b0 (diff) | |
Sum demo, minus inference of {Unit}s
| -rw-r--r-- | demo/link.ur | 2 | ||||
| -rw-r--r-- | demo/sum.ur | 9 | ||||
| -rw-r--r-- | demo/sum.urp | 2 | ||||
| -rw-r--r-- | demo/sum.urs | 1 | ||||
| -rw-r--r-- | lib/top.ur | 14 | ||||
| -rw-r--r-- | lib/top.urs | 9 | ||||
| -rw-r--r-- | src/elaborate.sml | 19 |
7 files changed, 47 insertions, 9 deletions
diff --git a/demo/link.ur b/demo/link.ur index f9e33968..122b98f1 100644 --- a/demo/link.ur +++ b/demo/link.ur @@ -3,5 +3,5 @@ fun target () = return <xml><body> </body></xml> fun main () = return <xml><body> - <a link={target ()}>Go there</a> + <a link={target}>Go there</a> </body></xml> diff --git a/demo/sum.ur b/demo/sum.ur new file mode 100644 index 00000000..96a45891 --- /dev/null +++ b/demo/sum.ur @@ -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> diff --git a/demo/sum.urp b/demo/sum.urp new file mode 100644 index 00000000..e872a81b --- /dev/null +++ b/demo/sum.urp @@ -0,0 +1,2 @@ + +sum diff --git a/demo/sum.urs b/demo/sum.urs new file mode 100644 index 00000000..6ac44e0b --- /dev/null +++ b/demo/sum.urs @@ -0,0 +1 @@ +val main : unit -> transaction page @@ -6,6 +6,9 @@ con sndTT (t :: (Type * Type)) = t.2 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 compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) 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 --git a/lib/top.urs b/lib/top.urs index bf26d534..abdb7477 100644 --- a/lib/top.urs +++ b/lib/top.urs @@ -6,6 +6,9 @@ con sndTT = fn t :: (Type * Type) => t.2 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 compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type 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 --git a/src/elaborate.sml b/src/elaborate.sml index b965f0da..1ea854cd 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -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 |