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