]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mathQL.ml
new semantics for relation and attribute
[helm.git] / helm / ocaml / mathql / mathQL.ml
index a24dc4ed8492e0e659ad11abe6298eeb0e7f6c04..60b19297aa2e8581e0171e10f013cc5aa9b6a2d7 100644 (file)
@@ -47,18 +47,21 @@ type refine_op = ExactOp
                | SubOp
               | SuperOp
 
-type attr_list = vvar list
+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 * attr_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
             | Diff of set_exp * set_exp
-            | Let of svar * set_exp * set_exp
+            | LetSVar of svar * set_exp * set_exp
+            | LetVVar of vvar * val_exp * set_exp
             
 and boole_exp = False
               | True
@@ -73,8 +76,9 @@ and boole_exp = False
 and val_exp = Const of string list 
             | RefOf of set_exp 
            | 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