-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
-(* 30/04/2002 *)
-(* *)
-(* *)
-(******************************************************************************)
-
open Mathql
open Cic
| (Some t, None) -> "#1/" ^ string_of_int t
| (Some t, Some c) -> "#1/" ^ string_of_int t ^ "/" ^ string_of_int c
-let str_tref (p, u, x, i) =
- p ^ ":/" ^ str_up u ^ "." ^ x ^ str_fi i
+let str_tref (p, u, i) =
+ p ^ ":/" ^ str_up u ^ str_fi i
let str_uref (u, i) =
UriManager.string_of_uri u ^ str_fi i
let out_func = function
| MQName -> key "name"
+ | _ -> assert false
let out_str = function
| MQCons s -> con s
| 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
| 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 ")"
+ | MQRVarOccur v -> key "rvaroccur" ^ v
let out_query = function
| MQList l -> out_list l
let rec out_list = function
| [] -> ""
- | u :: l -> res u ^ nl () ^ out_list l
+ | u :: l -> res (str_tref u) ^ nl () ^ out_list l
let out_result qr =
par () ^ "Result:" ^ nl () ^
let i = Str.search_forward (Str.regexp_string ":/") s 0 in
let p = Str.string_before s i in
let q = Str.string_after s (i + 2) in
- try
- let j = String.rindex q '.' in
- (p, Str.string_before q j, Str.string_after q (j + 1))
- with
- Not_found -> (p, q, "")
+ (p, q)
with
- Not_found -> (s, "", "")
+ Not_found -> (s, "")
let encode = function
| Str.Text s -> MQString s
let tref_uref (u, i) =
let s = UriManager.string_of_uri u in
match split s with
- | (p, q, r) ->
+ | (p, q) ->
let rx = Str.regexp "\?\|\*\*\|\*\|/" in
let l = Str.full_split rx q in
- (p, List.map encode l, r, i)
+ (p, List.map encode l, i)
(* CIC term inspecting functions *)
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
- | Meta (i, _) -> l
+ | Meta (i, _) -> l
| Sort s -> l
| Implicit -> l
| Abst u -> l
| 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
| 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 ->
let mqs = if b then MQMConclusion else MQConclusion in
MQSelect (rvar,
MQUse (MQPattern r, svar),
- MQIs (MQSVar svar, mqs)
- )
+ MQIs (MQSVar svar, mqs)
+ )
let rec build_inter n = function
- | [] -> MQPattern ("cic", [MQAstAst], "con", (None, None))
+ | [] -> MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None))
| [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
let locate s =
let query =
MQList (MQSelect ("ref",
- MQPattern ("cic", [MQAstAst], "con", (None, None)),
+ MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None)),
MQIs (MQFunc (MQName, "ref"),
MQCons 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''
+;;
projects / helm.git / blobdiff