]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/newConstraints.ml
New syntax.
[helm.git] / helm / ocaml / tactics / newConstraints.ml
1 (* Copyright (C) 2000-2002, 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 (*********************************************************************)
27 (*                                                                   *)
28 (*                           PROJECT HELM                            *)
29 (*                                                                   *)
30 (*               Andrea Asperti <asperti@cs.unibo.it>                *)
31 (*                            18/03/2004                             *)
32 (*                                                                   *)
33 (*                                                                   *)
34 (*********************************************************************)
35
36 (* the file contains functions for computing prefixes and related
37    stuff, required by the new management of matching *)
38
39 module SortedString =
40   struct
41     type t = string
42     let compare = Pervasives.compare
43   end
44 ;;
45
46 module StringSet = Set.Make (SortedString)
47 ;;
48
49 module SetSet = Set.Make (StringSet)
50 ;;
51
52
53 (*
54   module SetSet :
55   sig
56     type elt = StringSet.t
57     and t = Set.Make(StringSet).t
58     val empty : t
59     val is_empty : t -> bool
60     val mem : elt -> t -> bool
61     val add : elt -> t -> t
62     val singleton : elt -> t
63     val remove : elt -> t -> t
64     val union : t -> t -> t
65     val inter : t -> t -> t
66     val diff : t -> t -> t
67     val compare : t -> t -> int
68     val equal : t -> t -> bool
69     val subset : t -> t -> bool
70     val iter : (elt -> unit) -> t -> unit
71     val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
72     val for_all : (elt -> bool) -> t -> bool
73     val exists : (elt -> bool) -> t -> bool
74     val filter : (elt -> bool) -> t -> t
75     val partition : (elt -> bool) -> t -> t * t
76     val cardinal : t -> int
77     val elements : t -> elt list
78     val min_elt : t -> elt
79     val max_elt : t -> elt
80     val choose : t -> elt
81   end
82 *)
83
84 let pp_StringSet set =
85   if (StringSet.is_empty set) then "EMPTY"
86   else
87     "{" ^ (String.concat "," (StringSet.elements set)) ^ "}"
88 ;;
89
90 let pp_SetSet set =
91   let el = List.map pp_StringSet (SetSet.elements set) in
92   "{" ^ (String.concat ",\n" el) ^ "}"
93 ;;
94
95 let pp_prefix (n,l) =
96   (string_of_int n) ^ 
97   ": {" ^ (String.concat "," l) ^ "}"
98
99 let pp_prefixes l =
100   let el = List.map pp_prefix l in
101   "{" ^ (String.concat ",\n" el) ^ "}"
102
103
104
105 let filter_by_card n =
106   SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
107 ;;
108   
109 let merge n a b = 
110   let init = SetSet.union a b in
111   let merge_single_set s1 b = 
112     SetSet.fold 
113       (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
114       b SetSet.empty in
115   let res = 
116     SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
117   in
118   filter_by_card n res 
119 ;;
120
121 let mutinduri u t =
122   (UriManager.string_of_uri u) ^ "#xpointer(1/" ^ (string_of_int (t+1)) ^ ")"
123 ;; 
124
125 let mutconstructuri u t c =
126   (UriManager.string_of_uri u) 
127   ^ "#xpointer(1/" ^ (string_of_int (t+1)) ^ "/" ^ (string_of_int c) ^ ")" 
128 ;;
129
130 let rec inspect_children n childs =
131   List.fold_left 
132     (fun res term -> merge n (inspect_conclusion n term) res)
133     SetSet.empty childs 
134
135 and add_root n root childs =
136   let childunion = inspect_children n childs in
137   let addroot = StringSet.add root in
138     SetSet.fold 
139       (fun child newsets -> SetSet.add (addroot child) newsets)
140       childunion 
141       (SetSet.singleton (StringSet.singleton root))
142
143 and inspect_conclusion n t = 
144 if n = 0 then SetSet.empty
145 else match t with
146       Cic.Rel _                    
147     | Cic.Meta _                     
148     | Cic.Sort _ 
149     | Cic.Implicit _ -> SetSet.empty 
150     | Cic.Var (u,exp_named_subst) -> SetSet.empty
151     | Cic.Const (u,exp_named_subst) -> 
152         SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
153     | Cic.MutInd (u, t, exp_named_subst) -> 
154         SetSet.singleton (StringSet.singleton (mutinduri u t))
155     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
156         SetSet.singleton (StringSet.singleton (mutconstructuri u t c))
157     | Cic.Cast (t, _) -> inspect_conclusion n t
158     | Cic.Prod (_, s, t) -> 
159         merge n (inspect_conclusion n s) (inspect_conclusion n t)
160     | Cic.Lambda (_, s, t) ->
161         merge n (inspect_conclusion n s) (inspect_conclusion n t)
162     | Cic.LetIn (_, s, t) ->
163         merge n (inspect_conclusion n s) (inspect_conclusion n t)
164     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
165         let suri = UriManager.string_of_uri u in
166         add_root (n-1) suri l
167     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
168         let suri = mutinduri u t in
169         add_root (n-1) suri l
170     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
171         let suri = mutconstructuri u t c in
172         add_root (n-1) suri l
173     | Cic.Appl l -> 
174         SetSet.empty
175     | Cic.MutCase (u, t, tt, uu, m) ->
176         SetSet.empty
177     | Cic.Fix (_, m) -> 
178         SetSet.empty
179     | Cic.CoFix (_, m) -> 
180         SetSet.empty
181 ;; 
182
183 let rec inspect_term n t = 
184 if n = 0 then assert false
185 else match t with
186       Cic.Rel _                    
187     | Cic.Meta _                     
188     | Cic.Sort _ 
189     | Cic.Implicit _ -> None, SetSet.empty 
190     | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
191     | Cic.Const (u,exp_named_subst) -> 
192         Some (UriManager.string_of_uri u), SetSet.empty
193     | Cic.MutInd (u, t, exp_named_subst) -> 
194         Some (mutinduri u t), SetSet.empty
195     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
196         Some (mutconstructuri u t c), SetSet.empty
197     | Cic.Cast (t, _) -> inspect_term n t
198     | Cic.Prod (_, _, t) -> inspect_term n t
199     | Cic.LetIn (_, _, t) -> inspect_term n t
200     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
201         let suri = UriManager.string_of_uri u in
202         let childunion = inspect_children (n-1) l in
203         Some suri, childunion
204     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
205         let suri = mutinduri u t in
206         if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
207           (* equality is handled in a special way: in particular, 
208              the type, if defined, is always added to the prefix, 
209              and n is not decremented - it should have been n-2 *)
210           match l with
211               Cic.Const (u1,exp_named_subst1)::l1 ->
212                 let suri1 = UriManager.string_of_uri u1 in
213                 let inconcl = add_root (n-1) suri1 l1 in
214                 Some suri, inconcl
215             | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
216                 let suri1 = mutinduri u1 t1 in
217                 let inconcl = add_root (n-1) suri1 l1 in  
218                 Some suri, inconcl
219             | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
220                 let suri1 = mutconstructuri u1 t1 c1 in
221                 let inconcl = add_root (n-1) suri1 l1 in  
222                 Some suri, inconcl
223             | _ :: _ -> Some suri, SetSet.empty
224             | _ -> assert false (* args number must be > 0 *)
225         else
226           let childunion = inspect_children (n-1) l in
227           Some suri, childunion
228     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
229         let suri = mutconstructuri u t c in
230         let childunion = inspect_children (n-1) l in
231         Some suri, childunion
232     | _ -> None, SetSet.empty
233
234 let rec add uri children =
235   List.fold_left
236     (fun acc t ->
237        StringSet.union (constants_concl t) acc)
238     (StringSet.singleton uri) children
239   
240 (* this function creates the set of all different constants appearing in 
241    the conclusion of the term *)
242 and constants_concl = 
243   function
244       Cic.Rel _                    
245     | Cic.Meta _                     
246     | Cic.Sort _ 
247     | Cic.Implicit _ -> StringSet.empty 
248     | Cic.Var (u,exp_named_subst) -> StringSet.empty
249     | Cic.Const (u,exp_named_subst) -> 
250         StringSet.singleton (UriManager.string_of_uri u)
251     | Cic.MutInd (u, t, exp_named_subst) -> 
252         StringSet.singleton (mutinduri u t)
253     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
254         StringSet.singleton (mutconstructuri u t c)
255     | Cic.Cast (t, _) -> constants_concl t
256     | Cic.Prod (_, s, t) -> 
257         StringSet.union (constants_concl s) (constants_concl t)
258     | Cic.Lambda (_, s, t) ->
259         StringSet.union (constants_concl s) (constants_concl t)
260     | Cic.LetIn (_, s, t) ->
261         StringSet.union (constants_concl s) (constants_concl t)
262     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
263         let suri = UriManager.string_of_uri u in
264           add suri l
265     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
266         let suri = mutinduri u t in
267         add suri l
268     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
269         let suri = mutconstructuri u t c in
270         add suri l
271     | Cic.Appl l -> 
272         StringSet.empty
273     | Cic.MutCase (u, t, tt, uu, m) ->
274         StringSet.empty
275     | Cic.Fix (_, m) -> 
276         StringSet.empty
277     | Cic.CoFix (_, m) -> 
278         StringSet.empty
279 ;;
280
281 (* (constants_of t) returns a pair (b,n) where n is the number of 
282    constants in the conclusion of t, and b is true if in MainConclusion
283    we have an equality *)
284
285 let rec constants_of = function
286   | Cic.Cast (t, _)      -> constants_of t
287   | Cic.Prod (_, _, t)   -> constants_of t               
288   | Cic.LetIn (_, _, t) -> constants_of t
289   | (Cic.Appl ((Cic.MutInd (u, _, _))::l)) as t when 
290      u = HelmLibraryObjects.Logic.eq_URI ->
291       (true, constants_concl t)
292   | t -> (false, constants_concl t)
293 ;;
294
295           
296 let add_cardinality s =
297   let l = SetSet.elements s in
298   let res = 
299     List.map 
300       (fun set -> 
301          let el = StringSet.elements set in
302          (List.length el, el)) l in
303     (* ordered by descending cardinality *)
304     List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
305 ;;
306
307 let prefixes n t =
308   match inspect_term n t with
309       Some a, set -> Some a, add_cardinality set
310     | None, set when (SetSet.is_empty set) -> None, []
311     | _, _ -> assert false
312 ;;