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