helm/gTopLevel/mQueryGenerator.ml

   1 open MQueryUtil
   2 open MathQL
   3 open Cic
   4
   5 (* raw HTML representation *)
   6
   7 let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
   8
   9 let nl () = "<br>"
  10
  11 let par () = "<p>"
  12
  13 (* CIC term inspecting functions *)
  14
  15 let ie_out (r, b, v) =
  16    let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
  17    res (pos ^ str_uref r) ^ nl ()
  18
  19 let rec il_out = function
  20    | []           -> ""
  21    | head :: tail -> ie_out head ^ il_out tail
  22
  23 let ie_struri (u, b, v) = str_uref u
  24
  25 let rec il_restrict level = function
  26    | []                -> []
  27    | (u, b, v) :: tail ->
  28       if v <= level then (u, b, v) :: il_restrict level tail
  29       else il_restrict level tail
  30
  31 let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) =
  32    UriManager.eq u1 u2 && f1 = f2 && b1 = b2
  33
  34 let rec ie_insert ie = function
  35    | []           -> [ie]
  36    | head :: tail ->
  37       head :: if ie_eq head ie then tail else ie_insert ie tail
  38
  39 let inspect_uri main l uri tc v =
  40    let fi = match tc with
  41       | t0 :: c0 :: _ -> [t0 + 1; c0]
  42       | t0 :: _       -> [t0 + 1]
  43       | []            -> []
  44    in ie_insert ((uri, fi), main, v) l
  45
  46 let rec inspect_term main l v = function
  47    | Rel i                        -> l
  48    | Meta (i, _)                  -> l
  49    | Sort s                       -> l
  50    | Implicit                     -> l
  51    | Var u                        -> inspect_uri main l u [] v
  52    | Const (u, i)                 -> inspect_uri main l u [] v
  53    | MutInd (u, i, t)             -> inspect_uri main l u [t] v
  54    | MutConstruct (u, i, t, c)    -> inspect_uri main l u [t; c] v
  55    | Cast (uu, _)                 ->
  56       (*CSC: Cast modified so that it behaves exactly as if no Cast was there *)
  57       inspect_term main l v uu
  58    | Prod (n, uu, tt)             ->
  59       let luu = inspect_term false l (v + 1) uu in
  60       inspect_term false luu (v + 1) tt
  61    | Lambda (n, uu, tt)           ->
  62       let luu = inspect_term false l (v + 1) uu in
  63       inspect_term false luu (v + 1) tt
  64    | LetIn (n, uu, tt)            ->
  65       let luu = inspect_term false l (v + 1) uu in
  66       inspect_term false luu (v + 1) tt
  67    | Appl m                       -> inspect_list main l true v m
  68    | MutCase (u, i, t, tt, uu, m) ->
  69       let lu = inspect_uri main l u [t] (v + 1) in
  70       let ltt = inspect_term false lu (v + 1) tt in
  71       let luu = inspect_term false ltt (v + 1) uu in
  72       inspect_list main luu false (v + 1) m
  73    | Fix (i, m)                   -> inspect_ind l (v + 1) m
  74    | CoFix (i, m)                 -> inspect_coind l (v + 1) m
  75 and inspect_list main l head v = function
  76    | []      -> l
  77    | tt :: m ->
  78       let ltt = inspect_term main l (if head then v else v+1) tt in
  79       inspect_list false ltt false v m
  80 and inspect_ind l v = function
  81    | []                  -> l
  82    | (n, i, tt, uu) :: m ->
  83       let ltt = inspect_term false l v tt in
  84       let luu = inspect_term false ltt v uu in
  85       inspect_ind luu v m
  86 and inspect_coind l v = function
  87    | []               -> l
  88    | (n, tt, uu) :: m ->
  89       let ltt = inspect_term false l v tt in
  90       let luu = inspect_term false ltt v uu in
  91       inspect_coind luu v m
  92
  93 let inspect t = inspect_term true [] 0 t
  94
  95 (* query building functions *)
  96
  97 let save s =
  98    let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
  99                           (64 * 6 + 8 * 6 + 4) "MQGenLog.htm" in
 100    output_string och s; flush och; s
 101
 102 let build_select (r, b, v) n  =
 103    let rvar = "ref" ^ string_of_int n in
 104    let svar = "str" ^ string_of_int n in
 105    let mqs = if b then MQMConclusion else MQConclusion in
 106    MQSelect (rvar,
 107              MQUse (MQReference [str_uref r], svar),
 108              MQIs (MQStringSVar svar, mqs)
 109             )
 110
 111 let rec build_inter n = function
 112    | []       -> MQPattern [(None, [MQBSS], [MQFSS])]
 113    | [ie]     -> build_select ie n
 114    | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
 115
 116 let restrict_universe query =
 117  function
 118     [] -> query   (* no constraints ===> the universe is the library *)
 119   | l ->
 120      let universe =
 121        MQReference (List.map ie_struri l)
 122      in
 123       MQLetIn (
 124        "universe", universe,
 125         MQSelect (
 126          "uri", query,
 127           MQSubset (
 128            MQSelect (
 129             "uri2",
 130             MQUsedBy (MQListRVar "uri", "pos"),
 131             MQOr (
 132              MQIs (MQStringSVar "pos", MQConclusion),
 133              MQIs (MQStringSVar "pos", MQMConclusion)
 134             )
 135            ),
 136            MQListLVar "universe"
 137           )
 138         )
 139       )
 140
 141 let build_result query =
 142    let html = par () ^ out_query query ^ nl () in
 143    let result = Mqint.execute query in
 144    save (html ^ out_result result)
 145
 146 let init = Mqint.init
 147
 148 let close = Mqint.close
 149
 150 let locate s =
 151    let query =
 152 (*CSC: next query to be fixed
 153   1) I am exploiting the bug that does not quote '|'
 154   2) I am searching only constants and mutual inductive definition blocks
 155      (i.e. no fragment identifier at all)
 156 *)
 157       MQList (MQSelect ("ref",
 158                         MQPattern [(Some "cic", [MQBSS ; MQBC ".con|.ind"],[])],
 159                         MQIs (MQFunc (MQName, "ref"),
 160                               MQCons s
 161                              )
 162                        )
 163              )
 164    in
 165    build_result query
 166
 167 let backward t level =
 168    let il = inspect t in
 169    let query = build_inter 0 (il_restrict level il) in
 170    let query' = restrict_universe query il in
 171    let query'' = MQList query' in
 172    par () ^ il_out il ^ build_result query''
 173