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

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 1776db1d3..88a50c41d 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -33,115 +33,29 @@
 (*                                                                            *)
 (******************************************************************************)
 
-(* level managing functions *************************************************)
+(* Query issuing functions **************************************************)
+
+
+
+type uri = string
+type position = string
+type depth = int
+type sort = string 
+
+type r_obj = (uri * position * depth option)  
+type r_rel = (position* depth) 
+type r_sort = (position* depth * sort) 
+
+type must_restrictions = (r_obj list * r_rel list * r_sort list)
+type can_restrictions = (r_obj list option * r_rel list option * r_sort list option)
+
+
+
+
 
-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,45 +113,228 @@ 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 searchPattern must_use can_use =    
    let module M = MathQL 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 uri_of_entry (r, b, v) = r in
-   let rec restrict level = function
-      | []                -> []
-      | (u, b, v) :: tail ->
-         if v <= level then (u, b, v) :: restrict level tail
-         else restrict level tail
+   let in_path s = (s, []) in
+   let assign v p = (in_path v, in_path p) in 
+   
+   let q_where_obj = function
+       Some l ->
+         M.Sub
+         (M.RefOf
+           (M.Select
+             ("uri", 
+               M.Relation
+                (false, M.RefineExact, in_path "refObj", 
+   	         M.Ref (M.RefOf (M.RVar "uri0")), 
+	         [assign "pos" "position"]),
+               M.Ex ["uri"]
+                (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos")))
+	      )
+           ),
+           M.VVar "universe"
+         )
+     | None -> M.True  	 
+   in 
+    
+   let q_where_rel = function
+       Some l ->
+         M.And
+        (M.Sub(M.VVar "rel_positions", M.Property(false, M.RefineExact, ("refRel", ["position"]), M.RefOf(M.RVar "uri0"))),
+         M.Sub(M.VVar "rel_depths", M.Property(false, M.RefineExact, ("refRel", ["depth"]), M.RefOf(M.RVar "uri0"))))
+     | None -> M.True
+   in 
+
+   let q_where_sort = function
+       Some l ->
+         M.And
+	(M.And
+        (M.Sub(M.VVar "sort_positions", M.Property(false, M.RefineExact, ("refSort", ["position"]), M.RefOf(M.RVar "uri0"))),
+         M.Sub(M.VVar "sort_depths", M.Property(false, M.RefineExact, ("refSort", ["depth"]), M.RefOf(M.RVar "uri0")))),
+	 M.Sub(M.VVar "sorts", M.Property(false, M.RefineExact, ("refSort", ["sort"]), M.RefOf(M.RVar "uri0"))))
+     | None -> M.True
    in
-   let build_select (r, b, v) =
-      let pos = if b then "MainConclusion" else "InConclusion" in
-      M.Select
+   
+   let q_where cr =
+     let (cr_o,cr_r,cr_s) = cr in
+     M.And(M.And(q_where_obj cr_o, q_where_rel cr_r), q_where_sort cr_s)     
+   
+       in
+   
+   let uri_of_entry (r, p, d) = r in
+   
+   let build_select_obj (r, pos, dep) =
+     match dep with
+       None -> M.Select
+                 ("uri", 
+                  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")))))
+     | Some dep -> let string_dep = string_of_int dep in
+                   M.Select
+                     ("uri", 
+                      M.Relation (false, M.RefineExact, ("backPointer", []),
+	                          M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]),
+                      M.Ex ["uri"] 
+                      (M.And
+	              ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
+	              (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))	
+   in 
+  
+   let build_select_rel (pos, dep) =       
+      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")))
-       )
+        M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]), 
+        M.Ex ["uri"] 
+        (M.And
+	((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
+	(M.Sub (M.Const [dep], M.Record ("uri", in_path "d"))))))
    in 
-   let rec build_intersect = function
-      | []       -> M.Pattern (M.Const [".*"])
-      | [hd]     -> build_select hd
-      | hd :: tl -> M.Intersect (build_select hd, build_intersect tl)
+
+   let build_select_sort (pos, dep, sor) =       
+      M.Select                               
+       ("uri", 
+        M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]), 
+        M.Ex ["uri"] 
+        (M.And
+	((M.And
+	((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
+	(M.Sub (M.Const [dep], M.Record ("uri", in_path "d"))))),
+        (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
+   in 
+
+   let rec build_intersect_obj = function
+       []       -> M.Pattern (M.Const ["[.]*"])
+     | [hd]     -> build_select_obj hd
+     | hd :: tl -> M.Intersect (build_select_obj hd, build_intersect_obj tl)
    in
-   let levels = 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
-   let q_select = M.Select ("uri0", q_in, q_where) in
-   let universe = M.Const (List.map uri_of_entry levels) in
+   
+   let rec build_intersect_rel = function
+       []       -> M.Ref(M.Const [])                      
+     | [hd]     -> build_select_rel hd
+     | hd :: tl -> M.Intersect (build_select_rel hd, build_intersect_rel tl)
+   in
+
+   let rec build_intersect_sort = function
+       []       -> M.Ref(M.Const [])                         
+     | [hd]     -> build_select_sort hd
+     | hd :: tl -> M.Intersect (build_select_sort hd, build_intersect_sort tl)
+   in
+   
+   let build_intersect must = 
+      let tostring_sort (a,b,c) = 
+        let b1 = string_of_int b in 
+          (a,b1,c)
+      in
+      let tostring_rel (a,b) = 
+        let b1 = string_of_int b in 
+          (a,b1)
+      in
+      
+      let (l1,l2,l3) = must in
+      match (l1,l2,l3) with 
+        l1,[],[] -> build_intersect_obj l1
+      |	[],l2,[] -> let lrel = List.map tostring_rel l2 in
+                      build_intersect_rel lrel
+      | [],[],l3 -> let lsort = List.map tostring_sort l3 in
+                      build_intersect_sort lsort
+      | l1,l2,[] -> let lrel = List.map tostring_rel l2 in
+                      M.Intersect (build_intersect_obj l1, build_intersect_rel lrel)
+      | l1,[],l3 -> let lsort = List.map tostring_sort l3 in		      
+                      M.Intersect (build_intersect_obj l1, build_intersect_sort lsort)
+      | [],l2,l3 -> let lrel = List.map tostring_rel l2 in
+                    let lsort = List.map tostring_sort l3 in
+		      M.Intersect (build_intersect_rel lrel, build_intersect_sort lsort)
+      | _ -> let lrel = List.map tostring_rel l2 in
+             let lsort = List.map tostring_sort l3 in			  
+              M.Intersect (M.Intersect (build_intersect_obj l1, build_intersect_rel lrel), build_intersect_sort lsort)
+   in  
+  
+   let q_in = build_intersect must_use in
+   let q_select = M.Select ("uri0", q_in, q_where can_use) in
+   
+   let (cr_o,cr_r,cr_s) = can_use in
+   
+   let universe = 
+     match cr_o with
+       None -> M.Const []
+     | Some cr_o -> M.Const (List.map uri_of_entry cr_o) 
+   in
+  
+   let tfst (a,b,c) = a in
+   let tsnd (a,b,c) = b in
+   let trd (a,b,c) = c in
+   
+   let opos =
+     match cr_o with
+       None -> M.Const []
+     | Some cr_o -> M.Const (List.map tsnd cr_o) in
+   
+   let odep =
+     match cr_o with
+       None -> M.Const []
+     | Some cr_o -> let lofc = List.map trd cr_o in
+                    let f l c =
+		    match c with
+		      None -> l 
+		    | Some c -> l@[c]
+                    in
+		    let lof_dep_int = List.fold_left f [] lofc in
+		      M.Const(List.map string_of_int lof_dep_int)
+   in
+    
+   let rpos = 
+     match cr_r with
+       None -> M.Const []
+     | Some cr_r -> M.Const (List.map fst cr_r) in
+   
+   let rdep = 
+     match cr_r with
+       None -> M.Const []
+     | Some cr_r -> let rdep_int = List.map snd cr_r in
+                      M.Const (List.map string_of_int rdep_int) 
+   in 
+   
+
+   let spos = 
+     match cr_s with
+       None -> M.Const []
+     | Some cr_s -> M.Const (List.map tfst cr_s) in
+   
+      
+   let sdep = 
+     match cr_s with
+       None -> M.Const []
+     | Some cr_s -> let sdep_int = List.map tsnd cr_s in
+                      M.Const (List.map string_of_int sdep_int)
+   in  
+   
+   
+   let sor = 
+     match cr_s with
+       None -> M.Const[]
+     | Some cr_s -> M.Const (List.map trd cr_s) in 
+   
    let q_let_u = M.LetVVar ("universe", universe, q_select) in
-   let q_let_p = M.LetVVar ("positions", v_pos, q_let_u) in
-   execute_query q_let_p
+   
+   let q_let_s = M.LetVVar ("sorts", sor, q_let_u) in
+   
+   let q_let_ds = M.LetVVar ("sort_depths", sdep, q_let_s) in
+   
+   let q_let_dr = M.LetVVar ("rel_depths", rdep, q_let_ds) in
+
+   let q_let_do = M.LetVVar ("obj_depths", odep, q_let_dr) in  
+   
+   let q_let_ps = M.LetVVar ("sort_positions", spos, q_let_do) in
+   
+   let q_let_pr = M.LetVVar ("rel_positions", rpos, q_let_ps) in
+
+   let q_let_po = M.LetVVar ("obj_positions", opos, q_let_pr) in
+print_endline ("### " ^ MQueryUtil.text_of_query q_let_po) ; flush stdout;
+   execute_query q_let_po