]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mathQL.ml
Fun implemented.
[helm.git] / helm / ocaml / mathql / mathQL.ml
index b424d110b56bc8247b6fa8b750487668bf603842..d375d92afeac7ecf3971081247b8ad2dd5316e71 100644 (file)
@@ -47,13 +47,15 @@ type refine_op = ExactOp
                | SubOp
               | SuperOp
 
+type path = string list
+
 type vvar_list = vvar list
 
 type set_exp = SVar of svar
             | RVar of rvar
              | Ref of val_exp
              | Pattern of val_exp
-            | Relation of refine_op * string * set_exp * vvar_list
+            | Relation of refine_op * path * set_exp * vvar_list
              | Select of rvar * set_exp * boole_exp
             | Union of set_exp * set_exp
             | Intersect of set_exp * set_exp
@@ -64,7 +66,7 @@ type set_exp = SVar of svar
 and boole_exp = False
               | True
              | Not of boole_exp
-             | Ex of boole_exp
+             | Ex of rvar list * boole_exp   
              | And of boole_exp * boole_exp
              | Or of boole_exp * boole_exp
              | Sub of val_exp * val_exp
@@ -76,7 +78,7 @@ and val_exp = Const of string list
            | Record of rvar * vvar
            | VVar of vvar
            | Fun of string * val_exp
-           | Attribute of refine_op * string * val_exp
+           | Attribute of refine_op * path * val_exp
 
 type query = set_exp