Mercurial > urweb

comparison lib/top.urs @ 411:06fcddcd20d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
410:c5a3d223f157 411:06fcddcd20d3
3 con fstTT = fn t :: (Type * Type) => t.1 3 con fstTT = fn t :: (Type * Type) => t.1
4 con sndTT = fn t :: (Type * Type) => t.2 4 con sndTT = fn t :: (Type * Type) => t.2
5 5
6 con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] => 6 con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] =>
7 [nm = f t] ++ acc) [] 7 [nm = f t] ++ acc) []
8
9 con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
10 [nm = f] ++ acc) []
8 11
9 con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => 12 con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
10 [nm = f t] ++ acc) [] 13 [nm = f t] ++ acc) []
11 14
12 con ex = fn tf :: (Type -> Type) => 15 con ex = fn tf :: (Type -> Type) =>
17 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type 20 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
18 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) 21 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
19 22
20 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t 23 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
21 -> xml ctx use [] 24 -> xml ctx use []
25
26 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
27 -> (nm :: Name -> rest :: {Unit}
28 -> fn [[nm] ~ rest] =>
29 tf -> tr rest -> tr ([nm] ++ rest))
30 -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r
22 31
23 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) 32 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
24 -> (nm :: Name -> t :: Type -> rest :: {Type} 33 -> (nm :: Name -> t :: Type -> rest :: {Type}
25 -> fn [[nm] ~ rest] => 34 -> fn [[nm] ~ rest] =>
26 tf t -> tr rest -> tr ([nm = t] ++ rest)) 35 tf t -> tr rest -> tr ([nm = t] ++ rest))