helm/ocaml/mathql_generator/mQueryGenerator.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 type uri = string
  27 type position = string
  28 type depth = string
  29 type sort = string
  30
  31 type spec = MustObj  of uri list * position list * depth list
  32           | MustSort of sort list * position list * depth list
  33           | MustRel  of position list * depth list
  34           | OnlyObj  of uri list * position list * depth list
  35           | OnlySort of sort list * position list * depth list
  36           | OnlyRel  of position list * depth list
  37           | Universe of position list
  38
  39 let text_of_builtin s =
  40    let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
  41    if s = ns ^ "MainHypothesis" then "$MH" else
  42    if s = ns ^ "InHypothesis" then "$IH" else
  43    if s = ns ^ "MainConclusion" then "$MC" else
  44    if s = ns ^ "InConclusion" then "$IC" else
  45    if s = ns ^ "InBody" then "$IB" else
  46    if s = ns ^ "Set" then "$SET" else
  47    if s = ns ^ "Prop" then "$PROP" else
  48    if s = ns ^ "Type" then "$TYPE" else s
  49
  50 let text_of_spec out l =
  51    let rec iter = function
  52       | []        -> ()
  53       | [s]       -> out "\""; out (text_of_builtin s); out "\""
  54       | s :: tail -> out "\""; out (text_of_builtin s); out "\", "; iter tail
  55    in
  56    let txt_list l = out "{"; iter l; out "} " in
  57    let txt_spec = function
  58       | MustObj  (u, p, d) -> out "mustobj  "; txt_list u; txt_list p; txt_list d; out "\n"
  59       | MustSort (s, p, d) -> out "mustsort "; txt_list s; txt_list p; txt_list d; out "\n"
  60       | MustRel  (   p, d) -> out "mustrel  "; txt_list p; txt_list d; out "\n"
  61       | OnlyObj  (u, p, d) -> out "onlyobj  "; txt_list u; txt_list p; txt_list d; out "\n"
  62       | OnlySort (s, p, d) -> out "onlysort "; txt_list s; txt_list p; txt_list d; out "\n"
  63       | OnlyRel  (   p, d) -> out "onlyrel  "; txt_list p; txt_list d; out "\n"
  64       | Universe (   p   ) -> out "universe "; txt_list p; out "\n"
  65    in
  66    List.iter txt_spec l
  67
  68 module M = MathQL
  69
  70 let locate s =
  71    let query =
  72       M.Property true M.RefineExact ["objectName"] [] [] [] []
  73                  false (M.Const s)
  74    in M.StatQuery query
  75
  76 let compose cl =
  77    let letin = ref [] in
  78    let must = ref [] in
  79    let onlyobj = ref [] in
  80    let onlysort = ref [] in
  81    let onlyrel = ref [] in
  82    let only = ref true in
  83    let univ = ref [] in
  84    let set_val = function
  85       | [s] -> M.Const s
  86       | l   ->
  87          let msval = M.Set (List.map (fun s -> M.Const s) l) in
  88          if ! only then begin
  89            let vvar = "val" ^ string_of_int (List.length ! letin) in
  90            letin := (vvar, msval) :: ! letin;
  91            M.VVar vvar
  92          end else msval
  93    in
  94    let cons o (r, s, p, d) =
  95       let con p = function
  96          | [] -> []
  97          | l  -> [(false, [p], set_val l)]
  98       in
  99       only := o;
 100       con "h:occurrence" r @ con "h:sort" s @
 101       con "h:position" p @ con "h:depth" d
 102    in
 103    let property_must n c =
 104       M.Property true M.RefineExact [n] []
 105                  (cons false c) [] [] false (M.Const "")
 106    in
 107    let property_only n cl =
 108       let cll = List.map (cons true) cl in
 109       M.Property false M.RefineExact [n] []
 110                  ! univ cll [] false (M.Proj None (M.AVar "obj"))
 111    in
 112    let rec aux = function
 113       | [] -> ()
 114       | Universe l :: tail    ->
 115          only := true; univ := [(false, ["h:position"], set_val l)]; aux tail
 116       | MustObj r p d :: tail ->
 117          must := property_must "refObj" (r, [], p, d) :: ! must; aux tail
 118       | MustSort s p d :: tail ->
 119          must := property_must "refSort" ([], s, p, d) :: ! must; aux tail
 120       | MustRel p d :: tail ->
 121          must := property_must "refRel" ([], [], p, d) :: ! must; aux tail
 122       | OnlyObj r p d :: tail ->
 123          onlyobj := (r, [], p, d) :: ! onlyobj; aux tail
 124       | OnlySort s p d :: tail ->
 125          onlysort := ([], s, p, d) :: ! onlysort; aux tail
 126       | OnlyRel p d :: tail ->
 127          onlyrel := ([], [], p, d) :: ! onlyrel; aux tail
 128    in
 129    let rec iter f g = function
 130       | []           -> raise (Failure "MQueryGenerator.iter")
 131       | [head]       -> (f head)
 132       | head :: tail -> let t = (iter f g tail) in g (f head) t
 133    in
 134    text_of_spec prerr_string cl;
 135    aux cl;
 136    let must_query =
 137       if ! must = [] then
 138          M.Property false M.RefineExact [] [] [] [] [] true (M.Const ".*")
 139       else
 140          iter (fun x -> x) (fun x y -> M.Bin M.BinFMeet x y) ! must
 141    in
 142    let onlyobj_val = M.Not (M.Proj None (property_only "refObj" ! onlyobj)) in
 143    let onlysort_val = M.Not (M.Proj None (property_only "refSort" ! onlysort)) in
 144    let onlyrel_val = M.Not (M.Proj None (property_only "refRel" ! onlyrel)) in
 145    let select_query x =
 146       match ! onlyobj, ! onlysort, ! onlyrel with
 147          | [], [], [] -> x
 148          | _, [], []  -> M.Select "obj" x onlyobj_val
 149          | [], _, []  -> M.Select "obj" x onlysort_val
 150          | [], [], _  -> M.Select "obj" x onlyrel_val
 151          | _, _, []   -> M.Select "obj" x (M.Test M.And onlyobj_val onlysort_val)
 152          | _, [], _   -> M.Select "obj" x (M.Test M.And onlyobj_val onlyrel_val)
 153          | [], _, _   -> M.Select "obj" x (M.Test M.And onlysort_val onlyrel_val)
 154          | _, _, _    -> M.Select "obj" x (M.Test M.And (M.Test M.And onlyobj_val onlysort_val) onlyrel_val)
 155    in
 156    let letin_query =
 157       if ! letin = [] then fun x -> x
 158       else
 159         let f (vvar, msval) x = M.LetVVar vvar msval x in
 160         iter f (fun x y z -> x (y z)) ! letin
 161    in
 162    M.StatQuery (letin_query (select_query must_query))
 163
 164 let builtin s =
 165    let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
 166    match s with
 167       | "MH"   -> ns ^ "MainHypothesis"
 168       | "IH"   -> ns ^ "InHypothesis"
 169       | "MC"   -> ns ^ "MainConclusion"
 170       | "IC"   -> ns ^ "InConclusion"
 171       | "IB"   -> ns ^ "InBody"
 172       | "SET"  -> ns ^ "Set"
 173       | "PROP" -> ns ^ "Prop"
 174       | "TYPE" -> ns ^ "Type"
 175       | _      -> raise (Failure "MQueryGenerator.builtin")
 176
 177 (* conversion functions from the old constraints  ***************************)
 178
 179 type old_depth = int option
 180
 181 type r_obj = uri * position * old_depth
 182 type r_rel = position * old_depth
 183 type r_sort = position * old_depth * sort
 184
 185 type universe = position list option
 186
 187 type must_restrictions = r_obj list * r_rel list * r_sort list
 188 type only_restrictions =
 189    r_obj list option * r_rel list option * r_sort list option
 190
 191 let query_of_constraints u (musts_obj, musts_rel, musts_sort)
 192                            (onlys_obj, onlys_rel, onlys_sort) =
 193    let conv = function
 194       | None   -> []
 195       | Some i -> [string_of_int i]
 196    in
 197    let must_obj (r, p, d) = MustObj ([r], [p], conv d) in
 198    let must_sort (p, d, s) = MustSort ([s], [p], conv d) in
 199    let must_rel (p, d) = MustRel ([p], conv d) in
 200    let only_obj (r, p, d) = OnlyObj ([r], [p], conv d) in
 201    let only_sort (p, d, s) = OnlySort ([s], [p], conv d) in
 202    let only_rel (p, d) = OnlyRel ([p], conv d) in
 203    let must = List.map must_obj musts_obj @
 204               List.map must_rel musts_rel @
 205               List.map must_sort musts_sort
 206    in
 207    let only =
 208       (match onlys_obj with
 209          | None    -> []
 210          | Some [] -> [OnlyObj ([], [], [])]
 211          | Some l  -> List.map only_obj l
 212       ) @
 213       (match onlys_rel with
 214          | None    -> []
 215          | Some [] -> [OnlyRel ([], [])]
 216          | Some l  -> List.map only_rel l
 217       ) @
 218       (match onlys_sort with
 219          | None    -> []
 220          | Some [] -> [OnlySort ([], [], [])]
 221          | Some l  -> List.map only_sort l
 222       )
 223    in
 224    let univ = match u with None -> [] | Some l -> [Universe l] in
 225    compose (must @ only @ univ)