]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/mQueryGenerator.ml
- new generated query "unreferred" implemented at server side
[helm.git] / helm / ocaml / mathql_generator / mQueryGenerator.ml
index 1a0211102b782552daa204c60e8c370e6f35d59b..40c0ea0b8372dc063f79f4087ccde41aaa04c310 100644 (file)
@@ -38,6 +38,19 @@ let locate s =
                  false (M.Const s) 
    in M.StatQuery query
 
+let unreferred target_pattern source_pattern =
+   let query = 
+      M.Bin M.BinFDiff
+      (
+         M.Property false M.RefineExact [] [] [] [] []
+                 true (M.Const target_pattern) 
+      ) (
+         M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] []
+                 true (M.Const source_pattern) 
+      
+      )
+   in M.StatQuery query
+
 let compose cl = 
    let letin = ref [] in
    let must = ref [] in
@@ -100,7 +113,8 @@ let compose cl =
       | [head]       -> (f head) 
       | head :: tail -> let t = (iter f g tail) in g (f head) t
    in
-   U.mathql_of_specs prerr_string cl;
+   prerr_endline "(** Compose: received constraints **)";
+   U.mathql_of_specs prerr_string cl; flush stderr;
    aux cl;
    let must_query =
       if ! must = [] then