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