]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/mQueryGenerator.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / mathql_generator / mQueryGenerator.ml
index 7e0dd9c965ba8aeb4ddef341ad9f6a60a6cada5c..dd8b00ae327aeb0248acc88a92024046320b7051 100644 (file)
@@ -35,7 +35,7 @@ module U = MQGUtil
 let locate s =
    let query = 
       M.Property (true,M.RefineExact,["objectName"],[],[],[],[],false,(M.Const s) )
-   in M.StatQuery query
+   in query
 
 let unreferred target_pattern source_pattern =
    let query = 
@@ -46,7 +46,7 @@ let unreferred target_pattern source_pattern =
          M.Property(false,M.RefineExact,["refObj"],["h:occurrence"],[],[],[],true,(M.Const source_pattern))
       
       ))
-   in M.StatQuery query
+   in query
 
 let compose cl = 
    let letin = ref [] in
@@ -81,7 +81,13 @@ let compose cl =
       M.Property(true,M.RefineExact,[n],[],(cons false c),[],[],false,(M.Const ""))
    in   
    let property_only n cl =
-      let cll = List.map (cons true) cl in
+      let rec build = function
+         | []      -> []
+        | c :: tl ->
+           let r = (cons true) c in
+           if r = [] then build tl else r :: build tl 
+      in
+      let cll = build cl in
       M.Property(false,M.RefineExact,[n],[],!univ,cll,[],false,(M.Proj(None,(M.AVar "obj"))))
    in
    let rec aux = function 
@@ -108,8 +114,8 @@ let compose cl =
       | [head]       -> (f head) 
       | head :: tail -> let t = (iter f g tail) in g (f head) t
    in
-   prerr_endline "(** Compose: received constraints **)";
-   U.mathql_of_specs prerr_string cl; flush stderr;
+   (* prerr_endline "(** Compose: received constraints **)";
+   U.mathql_of_specs prerr_string cl; flush stderr; *)
    aux cl;
    let must_query =
       if ! must = [] then  
@@ -137,7 +143,7 @@ let compose cl =
         let f (vvar, msval) x = M.LetVVar(vvar,msval,x) in 
         iter f (fun x y z -> x (y z)) ! letin
    in 
-   M.StatQuery (letin_query (select_query must_query))
+   letin_query (select_query must_query)
 
 (* high-level functions  ****************************************************)
 
@@ -181,4 +187,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)
-