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