helm/gTopLevel/mquery.ml

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