+(* 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
+
+(* string linearization of a reference *)
+
+let str_uptoken = function
+ | MQString s -> s
+ | MQSlash -> "/"
+ | MQAnyChr -> "?"
+ | MQAst -> "*"
+ | MQAstAst -> "**"
+
+let rec str_up = function
+ | [] -> ""
+ | head :: tail -> str_uptoken head ^ str_up tail
+
+let str_fi = function
+ | (None, _) -> ""
+ | (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_uref (u, i) =
+ UriManager.string_of_uri u ^ str_fi i
+
+(* raw HTML representation *)
+
+let key s = "<font color=\"blue\">" ^ s ^ " </font>"
+
+let sym s = s ^ " "
+
+let sep s = s
+
+let con s = "<font color=\"red\">\"" ^ s ^ "\" </font>"
+
+let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
+
+let nl () = "<br>"
+
+let par () = "<p>"
+
+(* HTML representation of a query *)
+
+let out_rvar s = sym s
+
+let out_svar s = sep "$" ^ sym s
+
+let out_tref r = con (str_tref r)
+
+let out_pat p = out_tref p
+
+let out_func = function
+ | MQName -> key "name"
+
+let out_str = function
+ | MQCons s -> con s
+ | MQRVar s -> out_rvar s
+ | MQSVar s -> out_svar s
+ | MQFunc (f, r) -> out_func f ^ out_rvar r
+ | MQMConclusion -> key "mainconclusion"
+ | MQConclusion -> key "conclusion"
+
+let rec out_bool = function
+ | MQTrue -> key "true"
+ | MQFalse -> key "false"
+ | MQIs (s, t) -> out_str s ^ key "is" ^ out_str t
+ | 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 ")"
+
+let rec 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 ")"
+
+let out_query = function
+ | MQList l -> out_list l
+
+(* Converting functions *)
+
+let split s =
+ try
+ 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, "")
+ with
+ Not_found -> (s, "", "")
+
+let encode = function
+ | Str.Text s -> MQString s
+ | Str.Delim s ->
+ if s = "?" then MQAnyChr else
+ if s = "*" then MQAst else
+ if s = "**" then MQAstAst else
+ if s = "/" then MQSlash else MQString s
+
+let tref_uref (u, i) =
+ let s = UriManager.string_of_uri u in
+ match split s with
+ | (p, q, r) ->
+ let rx = Str.regexp "\?\|\*\*\|\*\|/" in
+ let l = Str.full_split rx q in
+ (p, List.map encode l, r, i)
+
+(* CIC term inspecting functions *)
+
+let out_ie (r, b) =
+ let pos = if b then "HEAD: " else "TAIL: " in
+ res (pos ^ str_uref r) ^ nl () ^
+ con (pos ^ str_tref (tref_uref r)) ^ nl ()
+
+let rec out_il = function
+ | [] -> ""
+ | head :: tail -> out_ie head ^ out_il tail
+
+let tie_uie (r, b) = (tref_uref r, b)
+
+let ie_eq ((u1, f1), b1) ((u2, f2), b2) =
+ UriManager.eq u1 u2 && f1 = f2 && b1 = b2
+
+let rec ie_insert ie = function
+ | [] -> [ie]
+ | 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
+ | Rel 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
+ | Prod (n, uu, tt) ->
+ let luu = inspect_term false l uu in
+ inspect_term false luu tt
+ | Lambda (n, uu, tt) ->
+ let luu = inspect_term false l uu in
+ inspect_term false luu 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
+ | 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
+ | [] -> l
+ | tt :: m ->
+ let ltt = inspect_term main l tt in
+ inspect_list false ltt m
+and inspect_ind l = 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
+ | [] -> 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 inspect t = inspect_term true [] 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 mqs = if b then MQMConclusion else MQConclusion in
+ MQSelect (rvar,
+ MQUse (MQPattern r, svar),
+ MQIs (MQSVar svar, mqs)
+ )
+
+let rec build_inter n = function
+ | [] -> MQPattern ("cic", [MQAstAst], "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
+ )
+ )
+ )
+ in
+ out_query query ^ nl ()
+ in
+ match Str.split (Str.regexp "[ \t]+") s with
+ | [] -> ""
+ | head :: tail -> par () ^ locate_aux head
+
+let backward t =
+ 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 ^ *)