From 1bcce271566f8b2c2efdeb2283ebf210f6fcc6f1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 May 2002 15:59:01 +0000 Subject: [PATCH] * 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. --- helm/gTopLevel/mquery.ml | 88 +++++++++++++++++++++++++++++++--------- 1 file changed, 68 insertions(+), 20 deletions(-) diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml index b53abbe21..73118c962 100644 --- 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'' +;; -- 2.39.2