From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 7 Nov 2003 11:47:11 +0000 (+0000)
Subject: ported to version 1.4
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2f140ccb97dd271c280894e6a038ac0ebcf0bb71;p=helm.git

ported to version 1.4
---

diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml
index 40c0ea0b8..811546956 100644
--- a/helm/ocaml/mathql_generator/mQueryGenerator.ml
+++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml
@@ -30,26 +30,36 @@ module M = MathQL
 module T = MQGTypes
 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, [])]
+let intersect xl = M.Fun (["intersect"], [], xl)
+let lnot x       = M.Fun (["not"], [], [x])
+let lamp xl      = M.Fun (["and"], [], xl)
+
 (* low level functions  *****************************************************)
 
 let locate s =
    let query = 
       M.Property true M.RefineExact ["objectName"] [] [] [] []
-                 false (M.Const s) 
-   in M.StatQuery query
+                 false (const s) 
+   in stat query
 
 let unreferred target_pattern source_pattern =
    let query = 
-      M.Bin M.BinFDiff
+      diff 
       (
          M.Property false M.RefineExact [] [] [] [] []
-                 true (M.Const target_pattern) 
+                 true (const target_pattern) 
       ) (
          M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] []
-                 true (M.Const source_pattern) 
+                 true (const source_pattern) 
       
       )
-   in M.StatQuery query
+   in stat query
 
 let compose cl = 
    let letin = ref [] in
@@ -60,13 +70,13 @@ let compose cl =
    let only = ref true in
    let univ = ref [] in
    let set_val = function
-      | [s] -> M.Const s
+      | [s] -> const s
       | l   -> 
-	 let msval = M.Set (List.map (fun s -> M.Const s) l) in
+	 let msval = union (List.map (fun s -> const s) l) in
 	 if ! only then begin
 	   let vvar = "val" ^ string_of_int (List.length ! letin) in
 	   letin := (vvar, msval) :: ! letin;
-	   M.VVar vvar
+	   M.SVar vvar
 	 end else msval
    in
    let cons o (r, s, p, d) =      
@@ -82,12 +92,12 @@ let compose cl =
    in
    let property_must n c =
       M.Property true M.RefineExact [n] []
-	         (cons false c) [] [] false (M.Const "") 
+	         (cons false c) [] [] false (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"))
+	         ! univ cll [] false (M.AVar "obj")
    in
    let rec aux = function 
       | [] -> ()
@@ -118,31 +128,31 @@ let compose cl =
    aux cl;
    let must_query =
       if ! must = [] then  
-         M.Property false M.RefineExact [] [] [] [] [] true (M.Const ".*")
+         M.Property false M.RefineExact [] [] [] [] [] true (const ".*")
       else 
-         iter (fun x -> x) (fun x y -> M.Bin M.BinFMeet x y) ! must   
+         intersect ! 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 = lnot (property_only "refObj" ! onlyobj) in
+   let onlysort_val = lnot (property_only "refSort" ! onlysort) in
+   let onlyrel_val = lnot (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, lamp [onlyobj_val; onlysort_val])
+         | _, [], _   -> M.Select ("obj", x, lamp [onlyobj_val; onlyrel_val])
+         | [], _, _   -> M.Select ("obj", x, lamp [onlysort_val; onlyrel_val])
+	 | _, _, _    -> M.Select ("obj", x, lamp [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.Let (vvar, msval, x) in 
         iter f (fun x y z -> x (y z)) ! letin
    in 
-   M.StatQuery (letin_query (select_query must_query))
+   stat (letin_query (select_query must_query))
 
 (* high-level functions  ****************************************************)