]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/mQueryGenerator.ml
HELM dependent Mathql-1.4 library
[helm.git] / helm / ocaml / mathql_generator / mQueryGenerator.ml
index fd349c8ea8fdf0f87d3b065f5f7c9ac22bb909f6..bb68b8aea37d01c111b3a889e2d1df52c44d068e 100644 (file)
@@ -32,7 +32,6 @@ module U = MQGUtil
 
 (* helpers  *****************************************************************)
 
-let stat x       = M.Fun (["stat"], [], [x])
 let diff x y     = M.Fun (["diff"], [], [x; y])
 let union xl     = M.Fun (["union"], [], xl)
 let const s      = M.Const [(s, [])]
@@ -46,7 +45,7 @@ let locate s =
    let query = 
       M.Property (true, M.RefineExact, ["objectName"], [], [], [], [],
                  false, (const s)) 
-   in stat query
+   in query
 
 let unreferred target_pattern source_pattern =
    let query = 
@@ -58,7 +57,7 @@ let unreferred target_pattern source_pattern =
          M.Property (false, M.RefineExact, ["refObj"], ["h:occurrence"],
                    [], [], [], true, (const source_pattern))
       )
-   in stat query
+   in query
 
 let compose cl = 
    let letin = ref [] in
@@ -152,7 +151,7 @@ let compose cl =
         let f (vvar, msval) x = M.Let (Some vvar, msval, x) in 
         iter f (fun x y z -> x (y z)) ! letin
    in 
-   stat (letin_query (select_query must_query))
+   letin_query (select_query must_query)
 
 (* high-level functions  ****************************************************)
 
@@ -196,4 +195,3 @@ let query_of_constraints u (musts_obj, musts_rel, musts_sort)
    in
    let univ = match u with None -> [] | Some l -> [T.Universe l] in
    compose (must @ only @ univ)
-