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