+++ /dev/null
-(* 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
- result, save (html ^ out_result result)
- else MQRefs [], ""
-
-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 =
- let MQRefs uris, html = build_result (locate_query s) in
-(*CSC: here I am mapping .ind URIs to .ind#1/1, i.e. the first type of *)
-(*CSC: the mutual inductive block. It must be removed once the query *)
-(*CSC: works reasonably. *)
- MQRefs (
- List.map
- (function uri ->
- if String.sub uri (String.length uri - 4) 4 = ".ind" then
- uri ^ "#1/1"
- else
- uri
- ) uris
- ), html
-;;
-
-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 res = build_result query'' in
- let r,html = res in
- if html <> "" then
- begin
- print_endline ("GEN = " ^ string_of_int (List.length il) ^ ":" ^
- string_of_float (Sys.time () -. t0) ^ "s");
- r, par () ^ il_out il ^ html
- end else res
projects / helm.git / blobdiff