* The "backward" query has been refined considering head position as a different

  level w.r.t. non-head positions.
* The "backward" query has been refined using the new Subset construct.

diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml
index b53abbe2169fee5549a45d6a7f60e8996795ea50..73118c962e743ae70b13799d273106875d78525b 100644 (file)
--- a/helm/gTopLevel/mquery.ml
+++ b/helm/gTopLevel/mquery.ml
@@ -70,8 +70,12 @@ let rec out_bool = function
    | MQNot b -> key "not" ^ out_bool b 
    | MQAnd (b1, b2) -> sep "(" ^ out_bool b1 ^ key "and" ^ out_bool b2 ^ sep ")"
    | MQOr (b1, b2) -> sep "(" ^ out_bool b1 ^ key "or" ^ out_bool b2 ^ sep ")"
+   | MQSetEqual (l1, l2) ->
+      sep "(" ^ out_list l1 ^ key "setequal" ^ out_list l2 ^ sep ")"
+   | MQSubset (l1, l2) ->
+      sep "(" ^ out_list l1 ^ key "subset" ^ out_list l2 ^ sep ")"
    
-let rec out_list = function
+and out_list = function
    | MQSelect (r, l, b) -> 
       key "select" ^ out_rvar r ^ key "in" ^ out_list l ^ key "where" ^ out_bool b
    | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v
@@ -79,7 +83,7 @@ let rec out_list = function
    | MQPattern p -> key "pattern" ^ out_pat p
    | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
    | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
-   | _ -> assert false
+   | MQRVarOccur v -> key "rvaroccur" ^ v
 
 let out_query = function
    | MQList l -> out_list l
@@ -145,14 +149,22 @@ let rec ie_insert ie = function
 
 let level = ref 0
 
+(*CSC: che brutto il codice imperativo!!!*)
+let universe = ref [];;
+
 let inspect_uri main l uri t c v =
-   if v > !level then l else
-   let fi =
-      match (t, c) with
-         | (None, _) -> (None, None)
-         | (Some t0, c0) -> (Some (t0 + 1), c0) 
-   in
+ let fi =
+  match (t, c) with
+     | (None, _) -> (None, None)
+     | (Some t0, c0) -> (Some (t0 + 1), c0) 
+ in
+(*CSC: sbagliato, credo. MQString non dovrebbe poter contenere slash *)
+  universe := (tref_uref (uri,fi))::!universe ;
+  if v > !level then
+   l
+  else
    ie_insert ((uri, fi), main, v) l 
+;;
 
 let rec inspect_term main l v = function
    | Rel i                        -> l 
@@ -164,9 +176,9 @@ let rec inspect_term main l v = function
    | Const (u, i)                 -> inspect_uri main l u None None v
    | MutInd (u, i, t)             -> inspect_uri main l u (Some t) None v
    | MutConstruct (u, i, t, c)    -> inspect_uri main l u (Some t) (Some c) v
-   | Cast (uu, tt)                -> 
-      let luu = inspect_term main l (v + 1) uu in
-      inspect_term false luu (v + 1) tt 
+   | Cast (uu, _)                -> 
+      (*CSC: Cast modified so that it behaves exactly as if no Cast was there *)
+      inspect_term main l v uu
    | Prod (n, uu, tt)             ->
       let luu = inspect_term false l (v + 1) uu in
       inspect_term false luu (v + 1) tt
@@ -176,19 +188,19 @@ let rec inspect_term main l v = function
    | LetIn (n, uu, tt)            ->
       let luu = inspect_term false l (v + 1) uu in
       inspect_term false luu (v + 1) tt
-   | Appl m                       -> inspect_list main l (v + 1) m 
+   | Appl m                       -> inspect_list main l true v m 
    | MutCase (u, i, t, tt, uu, m) -> 
       let lu = inspect_uri main l u (Some t) None (v + 1) 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 (v + 1) m
+      inspect_list main luu false (v + 1) m
    | Fix (i, m)                   -> inspect_ind l (v + 1) m 
    | CoFix (i, m)                 -> inspect_coind l (v + 1) m 
-and inspect_list main l v = function
+and inspect_list main l head v = function
    | []      -> l
    | tt :: m -> 
-      let ltt = inspect_term main l v tt in
-      inspect_list false ltt v 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_ind l v = function
    | []                  -> l
    | (n, i, tt, uu) :: m ->  
@@ -225,6 +237,39 @@ let rec build_inter n = function
    | [ie]     -> build_select ie n
    | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
 
+let restrict_universe query =
+ function
+    [] -> query   (* no constraints ===> the universe is the library *)
+  | l ->
+     let universe =
+      (*CSC: Usare tante Union e Pattern per fare un insieme di uri mi   *)
+      (*CSC: sembra un poco penoso. Inoltre creo un albero completamente *)
+      (*CSC: sbilanciato, aumentando il costo della risoluzione della    *)
+      (*CSC: query.                                                      *)
+      let rec compose_universe =
+       function
+          [] -> assert false
+        | [uri] -> MQPattern uri
+        | uri::tl -> MQUnion(MQPattern uri, compose_universe tl)
+      in
+       compose_universe !universe
+     in
+      MQSelect (
+       "uri", query,
+        MQSubset (
+         MQSelect (
+          "uri2",
+          MQUsedBy (MQRVarOccur "uri", "pos"),
+          MQOr (
+           MQIs (MQSVar "pos", MQConclusion),
+           MQIs (MQSVar "pos", MQMConclusion)
+          )
+         ),
+         universe
+        )
+      )
+;;
+
 let build_result query =
    let html = par () ^ out_query query ^ nl () in
    let result = Mqint.execute query in
@@ -247,9 +292,12 @@ let locate s =
    build_result query
 
 let backward t n =
-   level := n;
+   level := n ;
+   universe := [] ;
    let uil = inspect t in
    let til = List.map tie_uie uil in
-   let query = MQList (build_inter 0 til) in 
-   par () ^ out_il uil ^ build_result query
-
+   let query = build_inter 0 til in
+   let query' = restrict_universe query til in
+   let query'' = MQList query' in 
+   par () ^ out_il uil ^ build_result query''
+;;