]> matita.cs.unibo.it Git - helm.git/commitdiff
ported to version 1.4
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 7 Nov 2003 11:47:11 +0000 (11:47 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 7 Nov 2003 11:47:11 +0000 (11:47 +0000)
helm/ocaml/mathql_generator/mQueryGenerator.ml

index 40c0ea0b8372dc063f79f4087ccde41aaa04c310..81154695621e3bfea936f1583f29cc67237c409c 100644 (file)
@@ -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  ****************************************************)