Mercurial > urweb
comparison lib/ur/top.urs @ 1172:ad15700272f6
Changing foldRX to mapX
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 28 Feb 2010 13:06:10 -0500 |
parents | 7fc4e0087e50 |
children | 983d9b38abc7 |
comparison
equal
deleted
inserted
replaced
1171:7a2a7a8f9cab | 1172:ad15700272f6 |
---|---|
96 -> [[nm] ~ rest] => | 96 -> [[nm] ~ rest] => |
97 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest)) | 97 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest)) |
98 -> tr [] | 98 -> tr [] |
99 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r | 99 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r |
100 | 100 |
101 val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit} | 101 val mapUX : tf :: Type -> ctx :: {Unit} |
102 -> (nm :: Name -> t :: K -> rest :: {K} | 102 -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => |
103 -> [[nm] ~ rest] => | 103 tf -> xml ctx [] []) |
104 tf t -> xml ctx [] []) | 104 -> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] [] |
105 -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] | 105 |
106 | 106 val mapX : K --> tf :: (K -> Type) -> ctx :: {Unit} |
107 val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} | 107 -> (nm :: Name -> t :: K -> rest :: {K} |
108 -> (nm :: Name -> t :: K -> rest :: {K} | 108 -> [[nm] ~ rest] => |
109 -> [[nm] ~ rest] => | 109 tf t -> xml ctx [] []) |
110 tf1 t -> tf2 t -> xml ctx [] []) | 110 -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] |
111 -> r ::: {K} -> folder r | 111 |
112 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] | 112 val mapX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} |
113 | 113 -> (nm :: Name -> t :: K -> rest :: {K} |
114 val foldRX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit} | 114 -> [[nm] ~ rest] => |
115 -> (nm :: Name -> t :: K -> rest :: {K} | 115 tf1 t -> tf2 t -> xml ctx [] []) |
116 -> [[nm] ~ rest] => | 116 -> r ::: {K} -> folder r |
117 tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) | 117 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] |
118 -> r ::: {K} -> folder r | 118 |
119 -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] [] | 119 val mapX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit} |
120 -> (nm :: Name -> t :: K -> rest :: {K} | |
121 -> [[nm] ~ rest] => | |
122 tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) | |
123 -> r ::: {K} -> folder r | |
124 -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] [] | |
120 | 125 |
121 val queryL : tables ::: {{Type}} -> exps ::: {Type} | 126 val queryL : tables ::: {{Type}} -> exps ::: {Type} |
122 -> [tables ~ exps] => | 127 -> [tables ~ exps] => |
123 sql_query tables exps | 128 sql_query tables exps |
124 -> transaction (list $(exps ++ map (fn fields :: {Type} => $fields) tables)) | 129 -> transaction (list $(exps ++ map (fn fields :: {Type} => $fields) tables)) |