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