helm/gTopLevel/mquery.ml

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