+(* 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 Cic
+open MathQL
+open MQueryHTML
+open MQueryUtil
+
+(* CIC term inspecting functions ********************************************)
+
+let env = ref [] (* metasemv *)
+let cont = ref [] (* context *)
+
+let ie_out (r, b, v) =
+ let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
+ res (pos ^ str_uref r) ^ nl ()
+ (* FG: si puo' usare xp_str_uref se si vuole xpointer *)
+
+let rec il_out = function
+ | [] -> ""
+ | head :: tail -> ie_out head ^ il_out tail
+
+let rec il_max = function
+ | [] -> 0
+ | (_, _, v) :: tail ->
+ let v0 = il_max tail in
+ if v > v0 then v else v0
+
+let ie_str_uri (u, b, v) = xp_str_uref u
+
+let rec il_restrict level = function
+ | [] -> []
+ | (u, b, v) :: tail ->
+ if v <= level then (u, b, v) :: il_restrict level tail
+ else il_restrict level tail
+
+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
+ | [] -> [ie]
+ | head :: tail ->
+ head :: if ie_eq head ie then tail else ie_insert ie tail
+
+let degree t =
+ let u0 = CicTypeChecker.type_of_aux' !env !cont t in
+ let u = CicReduction.whd !cont u0 in
+ let rec deg = function
+ | Sort _ -> 1
+ | Cast (uu, _) -> deg uu
+ | Prod (_, _, tt) -> deg tt
+ | _ -> 2
+ in deg u
+
+let inspect_uri main l uri tc v term =
+ let d = degree term in
+ let fi = match tc with
+ | t0 :: c0 :: _ -> [t0 + 1; c0]
+ | t0 :: _ -> [t0 + 1]
+ | [] -> []
+ in ie_insert ((uri, fi), main, 2 * v + d - 1) l
+
+let rec inspect_term main l v term =
+ match term with
+ | Rel _ -> l
+ | Meta (_, _) -> l
+ | Sort _ -> l
+ | Implicit -> l
+ | Var u -> inspect_uri main l u [] v term
+ | Const (u, _) -> inspect_uri main l u [] v term
+ | MutInd (u, _, t) -> inspect_uri main l u [t] v term
+ | MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term
+ | Cast (uu, _) ->
+ inspect_term main l v uu
+ | Prod (_, uu, tt) ->
+ let luu = inspect_term false l (v + 1) uu in
+ inspect_term main luu (v + 1) tt
+ | Lambda (_, uu, tt) ->
+ let luu = inspect_term false l (v + 1) uu in
+ inspect_term false luu (v + 1) tt
+ | LetIn (_, 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 true v m
+ | MutCase (u, _, t, tt, uu, m) ->
+ let lu = inspect_uri main l u [t] (v + 1) term 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 (_, m) -> inspect_ind l (v + 1) m
+ | CoFix (_, m) -> inspect_coind l (v + 1) m
+and inspect_list main l head v = function
+ | [] -> l
+ | tt :: 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
+ | (_, _, tt, uu) :: m ->
+ 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
+ | (_, tt, uu) :: 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 rec inspect_backbone = function
+ | Cast (uu, _) -> inspect_backbone uu
+ | Prod (_, _, tt) -> inspect_backbone tt
+ | LetIn (_, uu, tt) -> inspect_backbone tt
+ | t -> inspect_term true [] 0 t
+
+let inspect t = inspect_backbone t
+
+(* query building functions *************************************************)
+
+let issue = ref (fun _ -> true)
+
+let save s =
+ let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
+ (64 * 6 + 8 * 6 + 4) "MQGenLog.htm" in
+ output_string och s; flush och; s
+
+let build_result query =
+ if ! issue query then
+ let html = par () ^ out_query query ^ nl () in
+ let result = Mqint.execute query in
+ save (html ^ out_result result)
+ else ""
+
+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 (MQReference [xp_str_uref r], svar),
+ MQIs (MQStringSVar svar, mqs)
+ )
+
+let rec build_inter n = function
+ | [] -> MQPattern (None, [MQBSS], [MQFSS])
+ | [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 =
+ MQReference (List.map ie_str_uri l)
+ in
+ MQLetIn (
+ "universe", universe,
+ MQSelect (
+ "uri", query,
+ MQSubset (
+ MQSelect (
+ "uri2",
+ MQUsedBy (MQListRVar "uri", "pos"),
+ MQOr (
+ MQIs (MQStringSVar "pos", MQConclusion),
+ MQIs (MQStringSVar "pos", MQMConclusion)
+ )
+ ),
+ MQListLVar "universe"
+ )
+ )
+ )
+
+let init = Mqint.init
+
+let close = Mqint.close
+
+let locate_query s =
+(*CSC: next query to be fixed
+ 1) I am exploiting the bug that does not quote '|'
+ 2) I am searching only constants and mutual inductive definition blocks
+ (i.e. no fragment identifier at all)
+*)
+ MQList (MQSelect ("ref",
+ MQPattern (Some "cic", [MQBSS ; MQBC ".con|.ind"],[]),
+ MQIs (MQFunc (MQName, "ref"),
+ MQCons s
+ )
+ )
+ )
+
+let locate s = Mqint.execute (locate_query s)
+let locate_html s = build_result (locate_query s)
+
+let levels e c t =
+ env := e; cont := c;
+ let il = inspect t in
+ par () ^ il_out il ^ nl ()
+
+let call_back f =
+ issue := f
+
+let backward e c t level =
+ let t0 = Sys.time () in
+ env := e; cont := c;
+ let il = inspect t in
+ let query = build_inter 0 (il_restrict level il) in
+ let query' = restrict_universe query il in
+ let query'' = MQList query' in
+ let r = build_result query'' in
+ if r <> "" then
+ begin
+ print_endline ("GEN = " ^ string_of_int (List.length il) ^ ":" ^
+ string_of_float (Sys.time () -. t0) ^ "s");
+ par () ^ il_out il ^ r
+ end else ""