helm/gTopLevel/mquery.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 Mathql
  37 open Cic
  38
  39 (* string linearization of a reference *)
  40
  41 let str_uptoken = function
  42    | MQString s -> s
  43    | MQSlash    -> "/"
  44    | MQAnyChr   -> "?"
  45    | MQAst      -> "*"
  46    | MQAstAst   -> "**"
  47
  48 let rec str_up = function
  49    | [] -> ""
  50    | head :: tail -> str_uptoken head ^ str_up tail
  51
  52 let str_fi = function
  53    | (None, _)        -> ""
  54    | (Some t, None)   -> "#1/" ^ string_of_int t
  55    | (Some t, Some c) -> "#1/" ^ string_of_int t ^ "/" ^ string_of_int c
  56
  57 let str_tref (p, u, x, i) =
  58    p ^ ":/" ^ str_up u ^ "." ^ x ^ str_fi i
  59
  60 let str_uref (u, i) =
  61    UriManager.string_of_uri u ^ str_fi i
  62
  63 (* raw HTML representation *)
  64
  65 let key s = "<font color=\"blue\">" ^ s ^ " </font>"
  66
  67 let sym s = s ^ " "
  68
  69 let sep s = s
  70
  71 let con s = "<font color=\"red\">\"" ^ s ^ "\" </font>"
  72
  73 let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
  74
  75 let nl () = "<br>"
  76
  77 let par () = "<p>"
  78
  79 (* HTML representation of a query *)
  80
  81 let out_rvar s = sym s
  82
  83 let out_svar s = sep "$" ^ sym s
  84
  85 let out_tref r = con (str_tref r)
  86
  87 let out_pat p = out_tref p
  88
  89 let out_func = function
  90    | MQName -> key "name"
  91
  92 let out_str = function
  93    | MQCons s      -> con s
  94    | MQRVar s      -> out_rvar s
  95    | MQSVar s      -> out_svar s
  96    | MQFunc (f, r) -> out_func f ^ out_rvar r
  97    | MQMConclusion -> key "mainconclusion"
  98    | MQConclusion  -> key "conclusion"
  99
 100 let rec out_bool = function
 101    | MQTrue -> key "true"
 102    | MQFalse -> key "false"
 103    | MQIs (s, t) -> out_str s ^ key "is" ^ out_str t
 104    | MQNot b -> key "not" ^ out_bool b
 105    | MQAnd (b1, b2) -> sep "(" ^ out_bool b1 ^ key "and" ^ out_bool b2 ^ sep ")"
 106    | MQOr (b1, b2) -> sep "(" ^ out_bool b1 ^ key "or" ^ out_bool b2 ^ sep ")"
 107
 108 let rec out_list = function
 109    | MQSelect (r, l, b) ->
 110       key "select" ^ out_rvar r ^ key "in" ^ out_list l ^ key "where" ^ out_bool b
 111    | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v
 112    | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ key "position" ^ out_svar v
 113    | MQPattern p -> key "pattern" ^ out_pat p
 114    | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
 115    | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
 116
 117 let out_query = function
 118    | MQList l -> out_list l
 119
 120 (* HTML representation of a query result *)
 121
 122 let rec out_list = function
 123    | []     -> ""
 124    | u :: l -> res u ^ nl () ^ out_list l
 125
 126 let out_result qr =
 127    par () ^ "Result:" ^ nl () ^
 128    match qr with
 129       | MQRefs l -> out_list l
 130
 131 (* Converting functions *)
 132
 133 let split s =
 134    try
 135       let i = Str.search_forward (Str.regexp_string ":/") s 0 in
 136       let p = Str.string_before s i in
 137       let q = Str.string_after s (i + 2) in
 138       try
 139          let j = String.rindex q '.' in
 140          (p, Str.string_before q j, Str.string_after q (j + 1))
 141       with
 142          Not_found -> (p, q, "")
 143    with
 144       Not_found -> (s, "", "")
 145
 146 let encode = function
 147    | Str.Text s  -> MQString s
 148    | Str.Delim s ->
 149       if s = "?"  then MQAnyChr else
 150       if s = "*"  then MQAst    else
 151       if s = "**" then MQAstAst else
 152       if s = "/"  then MQSlash  else MQString s
 153
 154 let tref_uref (u, i) =
 155    let s = UriManager.string_of_uri u in
 156    match split s with
 157       | (p, q, r) ->
 158          let rx = Str.regexp "\?\|\*\*\|\*\|/" in
 159          let l = Str.full_split rx q in
 160          (p, List.map encode l, r, i)
 161
 162 (* CIC term inspecting functions *)
 163
 164 let out_ie (r, b, v) =
 165    let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
 166    res (pos ^ str_uref r) ^ nl () ^
 167    con (pos ^ str_tref (tref_uref r)) ^ nl ()
 168
 169 let rec out_il = function
 170    | []           -> ""
 171    | head :: tail -> out_ie head ^ out_il tail
 172
 173 let tie_uie (r, b, v) = (tref_uref r, b, v)
 174
 175 let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) =
 176    UriManager.eq u1 u2 && f1 = f2 && b1 = b2
 177
 178 let rec ie_insert ie = function
 179    | []           -> [ie]
 180    | head :: tail ->
 181       head :: if ie_eq head ie then tail else ie_insert ie tail
 182
 183 let level = ref 0
 184
 185 let inspect_uri main l uri t c v =
 186    if v > !level then l else
 187    let fi =
 188       match (t, c) with
 189          | (None, _) -> (None, None)
 190          | (Some t0, c0) -> (Some (t0 + 1), c0)
 191    in
 192    ie_insert ((uri, fi), main, v) l
 193
 194 let rec inspect_term main l v = function
 195    | Rel i                        -> l
 196    | Meta (i, _)                  -> l
 197    | Sort s                       -> l
 198    | Implicit                     -> l
 199    | Abst u                       -> l
 200    | Var u                        -> inspect_uri main l u None None v
 201    | Const (u, i)                 -> inspect_uri main l u None None v
 202    | MutInd (u, i, t)             -> inspect_uri main l u (Some t) None v
 203    | MutConstruct (u, i, t, c)    -> inspect_uri main l u (Some t) (Some c) v
 204    | Cast (uu, tt)                ->
 205       let luu = inspect_term main l (v + 1) uu in
 206       inspect_term false luu (v + 1) tt
 207    | Prod (n, uu, tt)             ->
 208       let luu = inspect_term false l (v + 1) uu in
 209       inspect_term false luu (v + 1) tt
 210    | Lambda (n, uu, tt)           ->
 211       let luu = inspect_term false l (v + 1) uu in
 212       inspect_term false luu (v + 1) tt
 213    | LetIn (n, uu, tt)            ->
 214       let luu = inspect_term false l (v + 1) uu in
 215       inspect_term false luu (v + 1) tt
 216    | Appl m                       -> inspect_list main l (v + 1) m
 217    | MutCase (u, i, t, tt, uu, m) ->
 218       let lu = inspect_uri main l u (Some t) None (v + 1) in
 219       let ltt = inspect_term false lu (v + 1) tt in
 220       let luu = inspect_term false ltt (v + 1) uu in
 221       inspect_list main luu (v + 1) m
 222    | Fix (i, m)                   -> inspect_ind l (v + 1) m
 223    | CoFix (i, m)                 -> inspect_coind l (v + 1) m
 224 and inspect_list main l v = function
 225    | []      -> l
 226    | tt :: m ->
 227       let ltt = inspect_term main l v tt in
 228       inspect_list false ltt v m
 229 and inspect_ind l v = function
 230    | []                  -> l
 231    | (n, i, tt, uu) :: m ->
 232       let ltt = inspect_term false l v tt in
 233       let luu = inspect_term false ltt v uu in
 234       inspect_ind luu v m
 235 and inspect_coind l v = function
 236    | []               -> l
 237    | (n, tt, uu) :: m ->
 238       let ltt = inspect_term false l v tt in
 239       let luu = inspect_term false ltt v uu in
 240       inspect_coind luu v m
 241
 242 let inspect t = inspect_term true [] 0 t
 243
 244 (* query building functions *)
 245
 246 let save s =
 247    let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
 248                           (64 * 6 + 8 * 6 + 4) "mquery.htm" in
 249    output_string och s; flush och; s
 250
 251 let build_select (r, b, v) n =
 252    let rvar = "ref" ^ string_of_int n in
 253    let svar = "str" ^ string_of_int n in
 254    let mqs = if b then MQMConclusion else MQConclusion in
 255    MQSelect (rvar,
 256              MQUse (MQPattern r, svar),
 257              MQIs (MQSVar svar, mqs)
 258             )
 259
 260 let rec build_inter n = function
 261    | []       -> MQPattern ("cic", [MQAstAst], "con", (None, None))
 262    | [ie]     -> build_select ie n
 263    | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
 264
 265 let build_result query =
 266    let html = par () ^ out_query query ^ nl () in
 267    let result = Mqint.execute query in
 268    save (html ^ out_result result)
 269
 270 let init = Mqint.init
 271
 272 let close = Mqint.close
 273
 274 let locate s =
 275    let query =
 276       MQList (MQSelect ("ref",
 277                         MQPattern ("cic", [MQAstAst], "con", (None, None)),
 278                         MQIs (MQFunc (MQName, "ref"),
 279                               MQCons s
 280                              )
 281                        )
 282              )
 283    in
 284    build_result query
 285
 286 let backward t n =
 287    level := n;
 288    let uil = inspect t in
 289    let til = List.map tie_uie uil in
 290    let query = MQList (build_inter 0 til) in
 291    par () ^ out_il uil ^ build_result query