comparison lib/basis.urs @ 251:326fb4686f60

Monoize transaction identifiers; improve disjointness prover on irreducible folds; change 'query' type
author Adam Chlipala <adamc@hcoop.net>
date Sun, 31 Aug 2008 10:36:54 -0400
parents 71bafe66dbe1
children 7e9bd70ad3ce
comparison
equal deleted inserted replaced
250:98f551ddd54b 251:326fb4686f60
153 -> t -> transaction t 153 -> t -> transaction t
154 val bind : t1 ::: Type -> t2 ::: Type 154 val bind : t1 ::: Type -> t2 ::: Type
155 -> transaction t1 -> (t1 -> transaction t2) 155 -> transaction t1 -> (t1 -> transaction t2)
156 -> transaction t2 156 -> transaction t2
157 157
158 val query : tables ::: {{Type}} -> exps ::: {Type} 158 val query : tables ::: {{Type}} -> exps ::: {Type} -> tables ~ exps
159 -> sql_query tables exps 159 -> sql_query tables exps
160 -> state ::: Type 160 -> state ::: Type
161 -> ($(fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables) 161 -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
162 -> $exps
163 -> state 162 -> state
164 -> transaction state) 163 -> transaction state)
165 -> state 164 -> state
166 -> transaction state 165 -> transaction state
167 166