X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.ml;h=dd8b00ae327aeb0248acc88a92024046320b7051;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=1a0211102b782552daa204c60e8c370e6f35d59b;hpb=0e74e8e94eada756157addce67e4adeb8dff1feb;p=helm.git

diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml
index 1a0211102..dd8b00ae3 100644
--- a/helm/ocaml/mathql_generator/mQueryGenerator.ml
+++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml
@@ -34,9 +34,19 @@ module U = MQGUtil
 
 let locate s =
    let query = 
-      M.Property true M.RefineExact ["objectName"] [] [] [] []
-                 false (M.Const s) 
-   in M.StatQuery query
+      M.Property (true,M.RefineExact,["objectName"],[],[],[],[],false,(M.Const s) )
+   in 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 query
 
 let compose cl = 
    let letin = ref [] in
@@ -68,13 +78,17 @@ let compose cl =
       con "h:depth" (List.map U.string_of_depth d)
    in
    let property_must n c =
-      M.Property true M.RefineExact [n] []
-	         (cons false c) [] [] false (M.Const "") 
+      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
-      M.Property false M.RefineExact [n] []
-	         ! univ cll [] false (M.Proj None (M.AVar "obj"))
+      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 
       | [] -> ()
@@ -82,17 +96,17 @@ let compose cl =
          only := true; 
 	 let l = List.map U.string_of_position l in
 	 univ := [(false, ["h:position"], set_val l)]; aux tail 
-      | T.MustObj r p d :: tail ->
+      | T.MustObj(r,p,d) :: tail ->
          must := property_must "refObj" (r, [], p, d) :: ! must; aux tail  
-      | T.MustSort s p d :: tail ->
+      | T.MustSort(s,p,d) :: tail ->
 	 must := property_must "refSort" ([], s, p, d) :: ! must; aux tail 
-      | T.MustRel p d :: tail ->
+      | T.MustRel(p,d) :: tail ->
 	 must := property_must "refRel" ([], [], p, d) :: ! must; aux tail
-      | T.OnlyObj r p d :: tail ->
+      | T.OnlyObj(r,p,d) :: tail ->
 	 onlyobj := (r, [], p, d) :: ! onlyobj; aux tail
-      | T.OnlySort s p d :: tail ->
+      | T.OnlySort(s,p,d) :: tail ->
          onlysort := ([], s, p, d) :: ! onlysort; aux tail
-      | T.OnlyRel p d :: tail ->
+      | T.OnlyRel(p,d) :: tail ->
          onlyrel := ([], [], p, d) :: ! onlyrel; aux tail
    in
    let rec iter f g = function
@@ -100,35 +114,36 @@ 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  
-         M.Property false M.RefineExact [] [] [] [] [] true (M.Const ".*")
+         M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const ".*"))
       else 
-         iter (fun x -> x) (fun x y -> M.Bin M.BinFMeet x y) ! must   
+         iter (fun x -> x) (fun x y -> M.Bin(M.BinFMeet,x,y)) ! must   
    in 
-   let onlyobj_val = M.Not (M.Proj None (property_only "refObj" ! onlyobj)) in
-   let onlysort_val = M.Not (M.Proj None (property_only "refSort" ! onlysort)) in
-   let onlyrel_val = M.Not (M.Proj None (property_only "refRel" ! onlyrel)) in
+   let onlyobj_val = M.Not (M.Proj(None,(property_only "refObj" ! onlyobj))) in
+   let onlysort_val = M.Not (M.Proj(None,(property_only "refSort" ! onlysort))) in
+   let onlyrel_val = M.Not (M.Proj(None,(property_only "refRel" ! onlyrel))) in
    let select_query x =
       match ! onlyobj, ! onlysort, ! onlyrel with
          | [], [], [] -> x
-	 | _, [], []  -> M.Select "obj" x onlyobj_val
-	 | [], _, []  -> M.Select "obj" x onlysort_val
-         | [], [], _  -> M.Select "obj" x onlyrel_val
-         | _, _, []   -> M.Select "obj" x (M.Test M.And onlyobj_val onlysort_val)
-         | _, [], _   -> M.Select "obj" x (M.Test M.And onlyobj_val onlyrel_val)
-         | [], _, _   -> M.Select "obj" x (M.Test M.And onlysort_val onlyrel_val)
-	 | _, _, _    -> M.Select "obj" x (M.Test M.And (M.Test M.And onlyobj_val onlysort_val) onlyrel_val)
+	 | _, [], []  -> M.Select("obj",x,onlyobj_val)
+	 | [], _, []  -> M.Select("obj",x,onlysort_val)
+         | [], [], _  -> M.Select("obj",x,onlyrel_val)
+         | _, _, []   -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlysort_val)))
+         | _, [], _   -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlyrel_val)))
+         | [], _, _   -> M.Select("obj",x,(M.Test(M.And,onlysort_val,onlyrel_val)))
+	 | _, _, _    -> M.Select("obj",x,(M.Test(M.And,(M.Test(M.And,onlyobj_val,onlysort_val)),onlyrel_val)))
    in	 
    let letin_query = 
       if ! letin = [] then fun x -> x
       else 
-        let f (vvar, msval) x = M.LetVVar vvar msval x in 
+        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  ****************************************************)
 
@@ -172,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)
-