-(* 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
+ | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v
+ | MQUsedBy (l, v) -> key "usedby" ^ 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
+(* HTML representation of a query result *)
+
+let rec out_list = function
+ | [] -> ""
+ | u :: l -> res (str_tref u) ^ nl () ^ out_list l
+
+let out_result qr =
+ par () ^ "Result:" ^ nl () ^
+ match qr with
+ | MQRefs l -> out_list l
+
(* Converting functions *)
let split s =
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 out_ie (r, b) =
- let pos = if b then "HEAD: " else "TAIL: " in
+let out_ie (r, b, v) =
+ let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
res (pos ^ str_uref r) ^ nl () ^
con (pos ^ str_tref (tref_uref r)) ^ nl ()
| [] -> ""
| head :: tail -> out_ie head ^ out_il tail
-let tie_uie (r, b) = (tref_uref r, b)
+let tie_uie (r, b, v) = (tref_uref r, b, v)
-let ie_eq ((u1, f1), b1) ((u2, f2), b2) =
+let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) =
UriManager.eq u1 u2 && f1 = f2 && b1 = b2
let rec ie_insert ie = function
| head :: tail ->
head :: if ie_eq head ie then tail else ie_insert ie tail
-let inspect_uri main l uri t c =
- let fi =
- match (t, c) with
- | (None, _) -> (None, None)
- | (Some t0, c0) -> (Some (t0 + 1), c0)
- in
- ie_insert ((uri, fi), main) l
-
-let rec inspect_term main l = function
+let level = ref 0
+
+(*CSC: che brutto il codice imperativo!!!*)
+let universe = ref [];;
+
+let inspect_uri main l uri t c v =
+ 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
- | Var u -> inspect_uri main l u None None
- | Const (u, i) -> inspect_uri main l u None None
- | MutInd (u, i, t) -> inspect_uri main l u (Some t) None
- | MutConstruct (u, i, t, c) -> inspect_uri main l u (Some t) (Some c)
- | Cast (uu, tt) ->
- let luu = inspect_term main l uu in
- inspect_term false luu tt
+ | Var u -> inspect_uri main l u None None v
+ | 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, _) ->
+ (*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 uu in
- inspect_term false luu tt
+ let luu = inspect_term false l (v + 1) uu in
+ inspect_term false luu (v + 1) tt
| Lambda (n, uu, tt) ->
- let luu = inspect_term false l uu in
- inspect_term false luu 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 uu in
- inspect_term false luu tt
- | Appl m -> inspect_list main l m
+ let luu = inspect_term false l (v + 1) uu in
+ inspect_term false luu (v + 1) tt
+ | 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 in
- let ltt = inspect_term false lu tt in
- let luu = inspect_term false ltt uu in
- inspect_list main luu m
- | Fix (i, m) -> inspect_ind l m
- | CoFix (i, m) -> inspect_coind l m
-and inspect_list main l = function
+ 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 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 head v = function
| [] -> l
| tt :: m ->
- let ltt = inspect_term main l tt in
- inspect_list false ltt m
-and inspect_ind l = function
+ 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 ltt = inspect_term false l tt in
- let luu = inspect_term false ltt uu in
- inspect_ind luu m
-and inspect_coind l = function
+ 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
| (n, tt, uu) :: m ->
- let ltt = inspect_term false l tt in
- let luu = inspect_term false ltt uu in
- inspect_coind luu m
+ let ltt = inspect_term false l v tt in
+ let luu = inspect_term false ltt v uu in
+ inspect_coind luu v m
-let inspect t = inspect_term true [] t
+let inspect t = inspect_term true [] 0 t
(* query building functions *)
-let build_select (r, b) n =
- let rvar = "uri" ^ string_of_int n in
- let svar = "s" ^ string_of_int n in
+let save s =
+ let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
+ (64 * 6 + 8 * 6 + 4) "mquery.htm" in
+ output_string och s; flush och; s
+
+let build_select (r, b, v) n =
+ let rvar = "ref" ^ string_of_int n in
+ let svar = "str" ^ string_of_int n in
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 locate s =
- let locate_aux txt =
- let query =
- MQList (MQSelect ("uri",
- MQPattern ("cic", [MQAstAst], "con", (None, None)),
- MQIs (MQFunc (MQName, "uri"),
- MQCons txt
- )
- )
- )
+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
- out_query query ^ nl ()
+ 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
+ save (html ^ out_result result)
+
+let init = Mqint.init
+
+let close = Mqint.close
+
+let locate s =
+ let query =
+ MQList (MQSelect ("ref",
+ MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None)),
+ MQIs (MQFunc (MQName, "ref"),
+ MQCons s
+ )
+ )
+ )
in
- match Str.split (Str.regexp "[ \t]+") s with
- | [] -> ""
- | head :: tail -> par () ^ locate_aux head
+ build_result query
-let backward t =
+let backward t 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_query query ^ nl () (* par () ^ out_il uil ^ *)
+ 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