]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/mQueryGenerator.ml
functor added
[helm.git] / helm / ocaml / mathql_generator / mQueryGenerator.ml
index e56a744cd2cde7fd31ae2deda966520138dd6478..fd349c8ea8fdf0f87d3b065f5f7c9ac22bb909f6 100644 (file)
@@ -44,20 +44,19 @@ let lamp xl      = M.Fun (["and"], [], xl)
 
 let locate s =
    let query = 
-      M.Property true M.RefineExact ["objectName"] [] [] [] []
-                 false (const s
+      M.Property (true, M.RefineExact, ["objectName"], [], [], [], [],
+                 false, (const s)
    in stat query
 
 let unreferred target_pattern source_pattern =
    let query = 
       diff 
       (
-         M.Property false M.RefineExact [] [] [] [] []
-                 true (const target_pattern
+         M.Property (false, M.RefineExact, [], [], [], [], [],
+                 true, (const target_pattern)
       ) (
-         M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] []
-                 true (const source_pattern) 
-      
+         M.Property (false, M.RefineExact, ["refObj"], ["h:occurrence"],
+                   [], [], [], true, (const source_pattern))
       )
    in stat query
 
@@ -91,13 +90,13 @@ 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 (const ""
+      M.Property (true, M.RefineExact, [n], [],
+                (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.AVar "obj")
+      M.Property (false, M.RefineExact, [n], [],
+                ! univ, cll, [], false, (M.AVar "obj"))
    in
    let rec aux = function 
       | [] -> ()
@@ -105,17 +104,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
@@ -128,7 +127,8 @@ let compose cl =
    aux cl;
    let must_query =
       if ! must = [] then  
-         M.Property false M.RefineExact [] [] [] [] [] true (const ".*")
+         M.Property (false, M.RefineExact, [], [], 
+                    [], [], [], true, (const ".*"))
       else 
          intersect ! must   
    in