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 module M = MathQL
  30 module T = MQGTypes
  31 module U = MQGUtil
  32
  33 (* low level functions  *****************************************************)
  34
  35 let locate s =
  36    let query =
  37       M.Property true M.RefineExact ["objectName"] [] [] [] []
  38                  false (M.Const s)
  39    in M.StatQuery query
  40
  41 let compose cl =
  42    let letin = ref [] in
  43    let must = ref [] in
  44    let onlyobj = ref [] in
  45    let onlysort = ref [] in
  46    let onlyrel = ref [] in
  47    let only = ref true in
  48    let univ = ref [] in
  49    let set_val = function
  50       | [s] -> M.Const s
  51       | l   ->
  52          let msval = M.Set (List.map (fun s -> M.Const s) l) in
  53          if ! only then begin
  54            let vvar = "val" ^ string_of_int (List.length ! letin) in
  55            letin := (vvar, msval) :: ! letin;
  56            M.VVar vvar
  57          end else msval
  58    in
  59    let cons o (r, s, p, d) =
  60       let con p = function
  61          | [] -> []
  62          | l  -> [(false, [p], set_val l)]
  63       in
  64       only := o;
  65       con "h:occurrence" r @
  66       con "h:sort" (List.map U.string_of_sort s) @
  67       con "h:position" (List.map U.string_of_position p) @
  68       con "h:depth" (List.map U.string_of_depth d)
  69    in
  70    let property_must n c =
  71       M.Property true M.RefineExact [n] []
  72                  (cons false c) [] [] false (M.Const "")
  73    in
  74    let property_only n cl =
  75       let cll = List.map (cons true) cl in
  76       M.Property false M.RefineExact [n] []
  77                  ! univ cll [] false (M.Proj None (M.AVar "obj"))
  78    in
  79    let rec aux = function
  80       | [] -> ()
  81       | T.Universe l :: tail    ->
  82          only := true;
  83          let l = List.map U.string_of_position l in
  84          univ := [(false, ["h:position"], set_val l)]; aux tail
  85       | T.MustObj r p d :: tail ->
  86          must := property_must "refObj" (r, [], p, d) :: ! must; aux tail
  87       | T.MustSort s p d :: tail ->
  88          must := property_must "refSort" ([], s, p, d) :: ! must; aux tail
  89       | T.MustRel p d :: tail ->
  90          must := property_must "refRel" ([], [], p, d) :: ! must; aux tail
  91       | T.OnlyObj r p d :: tail ->
  92          onlyobj := (r, [], p, d) :: ! onlyobj; aux tail
  93       | T.OnlySort s p d :: tail ->
  94          onlysort := ([], s, p, d) :: ! onlysort; aux tail
  95       | T.OnlyRel p d :: tail ->
  96          onlyrel := ([], [], p, d) :: ! onlyrel; aux tail
  97    in
  98    let rec iter f g = function
  99       | []           -> raise (Failure "MQueryGenerator.iter")
 100       | [head]       -> (f head)
 101       | head :: tail -> let t = (iter f g tail) in g (f head) t
 102    in
 103    U.mathql_of_specs prerr_string cl;
 104    aux cl;
 105    let must_query =
 106       if ! must = [] then
 107          M.Property false M.RefineExact [] [] [] [] [] true (M.Const ".*")
 108       else
 109          iter (fun x -> x) (fun x y -> M.Bin M.BinFMeet x y) ! must
 110    in
 111    let onlyobj_val = M.Not (M.Proj None (property_only "refObj" ! onlyobj)) in
 112    let onlysort_val = M.Not (M.Proj None (property_only "refSort" ! onlysort)) in
 113    let onlyrel_val = M.Not (M.Proj None (property_only "refRel" ! onlyrel)) in
 114    let select_query x =
 115       match ! onlyobj, ! onlysort, ! onlyrel with
 116          | [], [], [] -> x
 117          | _, [], []  -> M.Select "obj" x onlyobj_val
 118          | [], _, []  -> M.Select "obj" x onlysort_val
 119          | [], [], _  -> M.Select "obj" x onlyrel_val
 120          | _, _, []   -> M.Select "obj" x (M.Test M.And onlyobj_val onlysort_val)
 121          | _, [], _   -> M.Select "obj" x (M.Test M.And onlyobj_val onlyrel_val)
 122          | [], _, _   -> M.Select "obj" x (M.Test M.And onlysort_val onlyrel_val)
 123          | _, _, _    -> M.Select "obj" x (M.Test M.And (M.Test M.And onlyobj_val onlysort_val) onlyrel_val)
 124    in
 125    let letin_query =
 126       if ! letin = [] then fun x -> x
 127       else
 128         let f (vvar, msval) x = M.LetVVar vvar msval x in
 129         iter f (fun x y z -> x (y z)) ! letin
 130    in
 131    M.StatQuery (letin_query (select_query must_query))
 132
 133 (* high-level functions  ****************************************************)
 134
 135 let query_of_constraints u (musts_obj, musts_rel, musts_sort)
 136                            (onlys_obj, onlys_rel, onlys_sort) =
 137    let conv = function
 138       | `MainHypothesis None     -> [T.MainHypothesis], []
 139       | `MainHypothesis (Some d) -> [T.MainHypothesis], [d]
 140       | `MainConclusion None     -> [T.MainConclusion], []
 141       | `MainConclusion (Some d) -> [T.MainConclusion], [d]
 142       | `InHypothesis            -> [T.InHypothesis], []
 143       | `InConclusion            -> [T.InConclusion], []
 144       | `InBody                  -> [T.InBody], []
 145    in
 146    let must_obj (p, u) = let p, d = conv p in T.MustObj ([u], p, d) in
 147    let must_sort (p, s) = let p, d = conv p in T.MustSort ([s], p, d) in
 148    let must_rel p = let p, d = conv p in T.MustRel (p, d) in
 149    let only_obj (p, u) = let p, d = conv p in T.OnlyObj ([u], p, d) in
 150    let only_sort (p, s) = let p, d = conv p in T.OnlySort ([s], p, d) in
 151    let only_rel p = let p, d = conv p in T.OnlyRel (p, d) in
 152    let must = List.map must_obj musts_obj @
 153               List.map must_rel musts_rel @
 154               List.map must_sort musts_sort
 155    in
 156    let only =
 157       (match onlys_obj with
 158          | None    -> []
 159          | Some [] -> [T.OnlyObj ([], [], [])]
 160          | Some l  -> List.map only_obj l
 161       ) @
 162       (match onlys_rel with
 163          | None    -> []
 164          | Some [] -> [T.OnlyRel ([], [])]
 165          | Some l  -> List.map only_rel l
 166       ) @
 167       (match onlys_sort with
 168          | None    -> []
 169          | Some [] -> [T.OnlySort ([], [], [])]
 170          | Some l  -> List.map only_sort l
 171       )
 172    in
 173    let univ = match u with None -> [] | Some l -> [T.Universe l] in
 174    compose (must @ only @ univ)
 175