helm/gTopLevel/mQueryGenerator.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
  31 (*                                 30/04/2002                                 *)
  32 (*                                                                            *)
  33 (*                                                                            *)
  34 (******************************************************************************)
  35
  36 open Cic
  37 open MathQL
  38 open MQueryHTML
  39 open MQueryUtil
  40
  41 (* CIC term inspecting functions ********************************************)
  42
  43 let env = ref []     (* metasemv *)
  44 let cont = ref []    (* context  *)
  45
  46 let ie_out (r, b, v) =
  47    let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
  48    res (pos ^ str_uref r) ^ nl ()
  49       (* FG: si puo' usare xp_str_uref se si vuole xpointer *)
  50
  51 let rec il_out = function
  52    | []           -> ""
  53    | head :: tail -> ie_out head ^ il_out tail
  54
  55 let rec il_max = function
  56    | []                -> 0
  57    | (_, _, v) :: tail ->
  58       let v0 = il_max tail in
  59       if v > v0 then v else v0
  60
  61 let ie_str_uri (u, b, v) = xp_str_uref u
  62
  63 let rec il_restrict level = function
  64    | []                -> []
  65    | (u, b, v) :: tail ->
  66       if v <= level then (u, b, v) :: il_restrict level tail
  67       else il_restrict level tail
  68
  69 let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) =
  70    UriManager.eq u1 u2 && f1 = f2 && b1 = b2
  71
  72 let rec ie_insert ie = function
  73    | []           -> [ie]
  74    | head :: tail ->
  75       head :: if ie_eq head ie then tail else ie_insert ie tail
  76
  77 let degree t =
  78    let u0 = CicTypeChecker.type_of_aux' !env !cont t in
  79    let u = CicReduction.whd !cont u0 in
  80    let rec deg = function
  81       | Sort _          -> 1
  82       | Cast (uu, _)    -> deg uu
  83       | Prod (_, _, tt) -> deg tt
  84       | _               -> 2
  85    in deg u
  86
  87 let inspect_uri main l uri tc v term =
  88    let d = degree term in
  89    let fi = match tc with
  90       | t0 :: c0 :: _ -> [t0 + 1; c0]
  91       | t0 :: _       -> [t0 + 1]
  92       | []            -> []
  93    in ie_insert ((uri, fi), main, 2 * v + d - 1) l
  94
  95 let rec inspect_term main l v term =
  96    match term with
  97    | Rel _                        -> l
  98    | Meta (_, _)                  -> l
  99    | Sort _                       -> l
 100    | Implicit                     -> l
 101    | Var u                        -> inspect_uri main l u [] v term
 102    | Const (u, _)                 -> inspect_uri main l u [] v term
 103    | MutInd (u, _, t)             -> inspect_uri main l u [t] v term
 104    | MutConstruct (u, _, t, c)    -> inspect_uri main l u [t; c] v term
 105    | Cast (uu, _)                 ->
 106       inspect_term main l v uu
 107    | Prod (_, uu, tt)             ->
 108       let luu = inspect_term false l (v + 1) uu in
 109       inspect_term main luu (v + 1) tt
 110    | Lambda (_, uu, tt)           ->
 111       let luu = inspect_term false l (v + 1) uu in
 112       inspect_term false luu (v + 1) tt
 113    | LetIn (_, uu, tt)            ->
 114       let luu = inspect_term false l (v + 1) uu in
 115       inspect_term false luu (v + 1) tt
 116    | Appl m                       -> inspect_list main l true v m
 117    | MutCase (u, _, t, tt, uu, m) ->
 118       let lu = inspect_uri main l u [t] (v + 1) term in
 119       let ltt = inspect_term false lu (v + 1) tt in
 120       let luu = inspect_term false ltt (v + 1) uu in
 121       inspect_list main luu false (v + 1) m
 122    | Fix (_, m)                   -> inspect_ind l (v + 1) m
 123    | CoFix (_, m)                 -> inspect_coind l (v + 1) m
 124 and inspect_list main l head v = function
 125    | []      -> l
 126    | tt :: m ->
 127       let ltt = inspect_term main l (if head then v else v + 1) tt in
 128       inspect_list false ltt false v m
 129 and inspect_ind l v = function
 130    | []                  -> l
 131    | (_, _, tt, uu) :: m ->
 132       let ltt = inspect_term false l v tt in
 133       let luu = inspect_term false ltt v uu in
 134       inspect_ind luu v m
 135 and inspect_coind l v = function
 136    | []               -> l
 137    | (_, tt, uu) :: m ->
 138       let ltt = inspect_term false l v tt in
 139       let luu = inspect_term false ltt v uu in
 140       inspect_coind luu v m
 141
 142 let rec inspect_backbone = function
 143    | Cast (uu, _)      -> inspect_backbone uu
 144    | Prod (_, _, tt)   -> inspect_backbone tt
 145    | LetIn (_, uu, tt) -> inspect_backbone tt
 146    | t                 -> inspect_term true [] 0 t
 147
 148 let inspect t = inspect_backbone t
 149
 150 (* query building functions *************************************************)
 151
 152 let issue = ref (fun _ -> true)
 153
 154 let save s =
 155    let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
 156                           (64 * 6 + 8 * 6 + 4) "MQGenLog.htm" in
 157    output_string och s; flush och; s
 158
 159 let build_result query =
 160    if ! issue query then
 161       let html = par () ^ out_query query ^ nl () in
 162       let result = Mqint.execute query in
 163       save (html ^ out_result result)
 164     else ""
 165
 166 let build_select (r, b, v) n  =
 167    let rvar = "ref" ^ string_of_int n in
 168    let svar = "str" ^ string_of_int n in
 169    let mqs = if b then MQMConclusion else MQConclusion in
 170    MQSelect (rvar,
 171              MQUse (MQReference [xp_str_uref r], svar),
 172              MQIs (MQStringSVar svar, mqs)
 173             )
 174
 175 let rec build_inter n = function
 176    | []       -> MQPattern (None, [MQBSS], [MQFSS])
 177    | [ie]     -> build_select ie n
 178    | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
 179
 180 let restrict_universe query =
 181  function
 182     [] -> query   (* no constraints ===> the universe is the library *)
 183   | l ->
 184      let universe =
 185        MQReference (List.map ie_str_uri l)
 186      in
 187       MQLetIn (
 188        "universe", universe,
 189         MQSelect (
 190          "uri", query,
 191           MQSubset (
 192            MQSelect (
 193             "uri2",
 194             MQUsedBy (MQListRVar "uri", "pos"),
 195             MQOr (
 196              MQIs (MQStringSVar "pos", MQConclusion),
 197              MQIs (MQStringSVar "pos", MQMConclusion)
 198             )
 199            ),
 200            MQListLVar "universe"
 201           )
 202         )
 203       )
 204
 205 let init = Mqint.init
 206
 207 let close = Mqint.close
 208
 209 let locate_query s =
 210 (*CSC: next query to be fixed
 211   1) I am exploiting the bug that does not quote '|'
 212   2) I am searching only constants and mutual inductive definition blocks
 213      (i.e. no fragment identifier at all)
 214 *)
 215       MQList (MQSelect ("ref",
 216                         MQPattern (Some "cic", [MQBSS ; MQBC ".con|.ind"],[]),
 217                         MQIs (MQFunc (MQName, "ref"),
 218                               MQCons s
 219                              )
 220                        )
 221              )
 222
 223 let locate s =
 224  (*CSC: the code should be: Mqint.execute (locate_query s)                  *)
 225  (*CSC: what follows is the patch to map mutual inductive definition blocks *)
 226  (*CSC: URIs (i.e. no fragment identifier at all) to the URIs of the first  *)
 227  (*CSC: mutual inductive type of their block.                               *)
 228  let MQRefs uris = Mqint.execute (locate_query s) in
 229   MQRefs
 230    (List.map
 231     (function uri ->
 232       if String.sub uri (String.length uri - 4) 4 = ".con" then uri else
 233        uri ^ "#1/1"
 234     ) uris)
 235 ;;
 236
 237 let locate_html s = build_result (locate_query s);;
 238
 239 let levels e c t =
 240    env := e; cont := c;
 241    let il = inspect t in
 242    par () ^ il_out il ^ nl ()
 243
 244 let call_back f =
 245    issue := f
 246
 247 let backward e c t level =
 248    env := e; cont := c;
 249    let il = inspect t in
 250    let query = build_inter 0 (il_restrict level il) in
 251    let query' = restrict_universe query il in
 252    let query'' = MQList query' in
 253    par () ^ il_out il ^ build_result query''
 254