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