diff lib/ur/basis.urs @ 714:0f42461273cf

CHECK constraints
author Adam Chlipala <adamc@hcoop.net>
date Thu, 09 Apr 2009 15:30:15 -0400
parents 915ec60592d4
children e28637743279
line wrap: on
line diff
--- a/lib/ur/basis.urs	Thu Apr 09 14:59:29 2009 -0400
+++ b/lib/ur/basis.urs	Thu Apr 09 15:30:15 2009 -0400
@@ -198,12 +198,18 @@
            OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
        -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
 
+con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
+
+val check : fs ::: {Type}
+            -> sql_exp [] [] fs bool
+            -> sql_constraint fs []
+
+
 
 (*** Queries *)
 
 con sql_query :: {{Type}} -> {Type} -> Type
 con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type
-con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
 
 con sql_subset :: {{Type}} -> {{Type}} -> Type
 val sql_subset : keep_drop :: {({Type} * {Type})}