diff 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
line wrap: on
line diff
--- a/lib/basis.urs	Sun Aug 31 09:52:52 2008 -0400
+++ b/lib/basis.urs	Sun Aug 31 10:36:54 2008 -0400
@@ -155,11 +155,10 @@
         -> transaction t1 -> (t1 -> transaction t2)
         -> transaction t2
 
-val query : tables ::: {{Type}} -> exps ::: {Type}
+val query : tables ::: {{Type}} -> exps ::: {Type} -> tables ~ exps
         -> sql_query tables exps
         -> state ::: Type
-        -> ($(fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
-                -> $exps
+        -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
                 -> state
                 -> transaction state)
         -> state