X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryGenerator.ml;h=b12f19bace500030c256e89d0090dab59a267090;hb=4f0c4e9db2be6bea38377d2a74d813bee4c53b02;hp=1776db1d34f0753fd77778d908a486760eda760d;hpb=7074f0403d1bec7f4d60715e50a0fe0ef0993567;p=helm.git

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 1776db1d3..b12f19bac 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -33,114 +33,6 @@
 (*                                                                            *)
 (******************************************************************************)
 
-(* level managing functions *************************************************)
-
-type levels_spec = (string * bool * int) list
-
-let levels_of_term metasenv context term =
-   let module TC = CicTypeChecker in
-   let module Red = CicReduction in
-   let module Util = MQueryUtil in
-   let degree t =
-      let rec degree_aux = function
-         | Cic.Sort _         -> 1 
-         | Cic.Cast (u, _)    -> degree_aux u
-         | Cic.Prod (_, _, t) -> degree_aux t
-         | _                  -> 2
-      in 
-      let u = TC.type_of_aux' metasenv context t in
-      degree_aux (Red.whd context u)
-   in
-   let entry_eq (s1, b1, v1) (s2, b2, v2) =
-      s1 = s2 && b1 = b2 
-   in
-   let rec entry_in e = function
-      | []           -> [e]
-      | head :: tail -> 
-         head :: if entry_eq head e then tail else entry_in e tail
-   in
-   let inspect_uri main l uri tc v term =
-      let d = degree term in 
-      entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l 
-   in
-   let rec inspect_term main l v term = match term with
-        Cic.Rel _                        -> l
-      | Cic.Meta _                       -> l
-      | Cic.Sort _                       -> l 
-      | Cic.Implicit                     -> l 
-      | Cic.Var (u,exp_named_subst)      ->
-         let l' = inspect_uri main l u [] v term in
-          inspect_exp_named_subst l' (v+1) exp_named_subst
-      | Cic.Const (u,exp_named_subst)    ->
-         let l' = inspect_uri main l u [] v term in
-          inspect_exp_named_subst l' (v+1) exp_named_subst
-      | Cic.MutInd (u, t, exp_named_subst) ->
-         let l' = inspect_uri main l u [t] v term in
-          inspect_exp_named_subst l' (v+1) exp_named_subst
-      | Cic.MutConstruct (u, t, c, exp_named_subst)    ->
-         let l' = inspect_uri main l u [t; c] v term in
-          inspect_exp_named_subst l' (v+1) exp_named_subst
-      | Cic.Cast (uu, _)                 -> 
-         inspect_term main l v uu
-      | Cic.Prod (_, uu, tt)             ->
-         let luu = inspect_term false l (v + 1) uu in
-         inspect_term main luu (v + 1) tt         
-      | Cic.Lambda (_, uu, tt)           ->
-         let luu = inspect_term false l (v + 1) uu in
-         inspect_term false luu (v + 1) tt 
-      | Cic.LetIn (_, uu, tt)            ->
-         let luu = inspect_term false l (v + 1) uu in
-         inspect_term false luu (v + 1) tt
-      | Cic.Appl m                       -> inspect_list main l true v m 
-      | Cic.MutCase (u, t, tt, uu, m) -> 
-         let lu = inspect_uri main l u [t] (v + 1) term in
-         let ltt = inspect_term false lu (v + 1) tt in
-         let luu = inspect_term false ltt (v + 1) uu in
-         inspect_list main luu false (v + 1) m
-      | Cic.Fix (_, m)                   -> inspect_ind l (v + 1) m 
-      | Cic.CoFix (_, m)                 -> inspect_coind l (v + 1) m 
-   and inspect_list main l head v = function
-      | []      -> l
-      | tt :: m -> 
-         let ltt = inspect_term main l (if head then v else v + 1) tt in
-         inspect_list false ltt false v m
-   and inspect_exp_named_subst l v = function
-        []      -> l
-      | (_,t) :: tl -> 
-         let l' = inspect_term false l v t in
-          inspect_exp_named_subst l' v tl
-   and inspect_ind l v = function
-      | []                  -> l
-      | (_, _, tt, uu) :: m ->  
-         let ltt = inspect_term false l v tt in
-         let luu = inspect_term false ltt v uu in
-         inspect_ind luu v m
-   and inspect_coind l v = function
-      | []               -> l
-      | (_, tt, uu) :: m ->
-         let ltt = inspect_term false l v tt in
-         let luu = inspect_term false ltt v uu in
-         inspect_coind luu v m
-   in
-   let rec inspect_backbone = function
-      | Cic.Cast (uu, _)      -> inspect_backbone uu
-      | Cic.Prod (_, _, tt)   -> inspect_backbone tt                
-      | Cic.LetIn (_, uu, tt) -> inspect_backbone tt
-      | t                     -> inspect_term true [] 0 t
-   in 
-   inspect_backbone term  
-
-let string_of_levels l sep =
-   let entry_out (s, b, v) =
-      let pos = if b then " HEAD: " else " TAIL: " in
-      string_of_int v ^ pos ^ s ^ sep 
-   in
-   let rec levels_out = function
-      | []           -> ""
-      | head :: tail -> entry_out head ^ levels_out tail
-   in
-   levels_out l
-
 (* Query issuing functions **************************************************)
 
 exception Discard  
@@ -199,19 +91,31 @@ let execute_query query =
 
 let locate s =
    let module M = MathQL in
-   let q = M.Ref (M.Fun "nameObject" (M.Const [s])) in
-   execute_query q
+   let q =
+    M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
+   in
+    execute_query q
 
 let searchPattern e c t level =
    let module M = MathQL in
+   let module L = MQueryLevels in
+   let in_path s = (s, []) in
+   let assign v p = (in_path v, in_path p) in 
    let v_pos = M.Const ["MainConclusion"; "InConclusion"] in
-   let q_where = M.Sub (M.RefOf (
-      M.Select ("uri", 
-                M.Relation (M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]),
-                M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos"))) 
-	       )),      M.VVar "universe"
-		       )
-   in
+   let q_where =
+    M.Sub
+     (M.RefOf
+       (M.Select
+         ("uri", 
+           M.Relation
+            (false, M.RefineExact, in_path "refObj", M.RVar "uri0", 
+	     [assign "pos" "position"]),
+           M.Ex ["uri"]
+            (M.Meet (M.VVar "positions", M.Record ("uri", in_path "pos")))
+	  )
+       ),
+       M.VVar "universe"
+     ) in
    let uri_of_entry (r, b, v) = r in
    let rec restrict level = function
       | []                -> []
@@ -220,19 +124,18 @@ let searchPattern e c t level =
          else restrict level tail
    in
    let build_select (r, b, v) =
-      let pos = if b then "MainConclusion" else "InConclusion" in
+    let pos = if b then "MainConclusion" else "InConclusion" in
       M.Select
        ("uri", 
-        M.Relation (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]),
-        M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
-       )
-   in 
+        M.Relation (false, M.RefineExact, ("backPointer", []),
+	            M.Ref (M.Const [r]), [assign "pos" "position"]),
+        M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", in_path "pos")))) in 
    let rec build_intersect = function
-      | []       -> M.Pattern (M.Const [".*"])
+      | []       -> M.Pattern (M.Const ["[.]*"])
       | [hd]     -> build_select hd
       | hd :: tl -> M.Intersect (build_select hd, build_intersect tl)
    in
-   let levels = levels_of_term e c t in
+   let levels = L.levels_of_term e c t in
    let rest = restrict level levels in
    info := [string_of_int (List.length rest)];
    let q_in = build_intersect rest in