diff lib/ur/basis.urs @ 753:d484df4e841a

Preparing to allow views in SELECT FROM clauses
author Adam Chlipala <adamc@hcoop.net>
date Tue, 28 Apr 2009 14:02:23 -0400
parents f95d652086cd
children 8ce31c052dce
line wrap: on
line diff
--- a/lib/ur/basis.urs	Tue Apr 28 11:18:27 2009 -0400
+++ b/lib/ur/basis.urs	Tue Apr 28 14:02:23 2009 -0400
@@ -124,6 +124,13 @@
 (** SQL *)
 
 con sql_table :: {Type} -> {{Unit}} -> Type
+con sql_view :: {Type} -> Type
+
+class fieldsOf :: Type -> {Type} -> Type
+val fieldsOf_table : fs ::: {Type} -> keys ::: {{Unit}}
+                     -> fieldsOf (sql_table fs keys) fs
+val fieldsOf_view : fs ::: {Type}
+                    -> fieldsOf (sql_view fs) fs
 
 (*** Constraints *)
 
@@ -222,9 +229,9 @@
 
 con sql_from_items :: {{Type}} -> Type
 
-val sql_from_table : cols ::: {Type} -> keys ::: {{Unit}}
-                     -> name :: Name -> sql_table cols keys
-                     -> sql_from_items [name = cols]
+val sql_from_table : t ::: Type -> fs ::: {Type}
+                     -> fieldsOf t fs -> name :: Name
+                     -> t -> sql_from_items [name = fs]
 val sql_from_comma : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
                      -> [tabs1 ~ tabs2]
     => sql_from_items tabs1 -> sql_from_items tabs2