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