]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/autoCache.ml
we were generating a name for the main fix twice
[helm.git] / helm / software / components / tactics / autoCache.ml
1 (* Copyright (C) 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 type cache_key = Cic.term
27 type cache_elem = 
28   | Failed_in of int
29   | Succeded of Cic.term
30   | UnderInspection
31   | Notfound
32 type cache = (Universe.universe * ((cache_key * cache_elem) list));;
33
34 let debug = false;;
35 let prerr_endline s = 
36   if debug then prerr_endline s else ()
37 ;;
38
39 let cache_empty = (Universe.empty,[]);;
40
41 let get_candidates (univ,_) ty = 
42 (*   if Universe.key ty = ty then *)
43     Universe.get_candidates univ ty
44 (*
45   else 
46     (prerr_endline ("skip: " ^ CicPp.ppterm (Universe.key ty)); [])
47  *)
48 ;;
49
50 let index (univ,cache) key term =
51   Universe.index univ key term,cache
52 ;;
53
54 let index_term_and_unfolded_term (univ,cache) context t ty =
55   Universe.index_local_term univ context t ty, cache
56 ;;
57
58 let cache_add_list (univ,cache) context terms_and_types =
59   let univ = 
60     List.fold_left
61       (fun univ (t,ty) -> 
62          prerr_endline ("indexing: " ^ CicPp.ppterm ty);
63          Universe.index_local_term univ context t ty)
64       univ terms_and_types  
65   in
66   univ, cache
67
68 let cache_examine (_,oldcache) cache_key = 
69   prerr_endline ("examine : " ^ CicPp.ppterm cache_key);
70   try snd (List.find (fun (x,_) -> CicUtil.alpha_equivalence x cache_key) 
71         oldcache) with Not_found -> 
72     prerr_endline "notfound";
73     Notfound
74 ;;
75 let cache_replace (univ,oldcache) key v =
76   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
77   univ, (key,v)::oldcache
78 ;;
79 let cache_remove (univ,oldcache) key =
80   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
81   univ,oldcache
82 ;;
83 let cache_add_failure cache cache_key depth =
84   prerr_endline 
85     ("CACHE: ADD FAIL " ^ CicPp.ppterm cache_key ^ 
86       " depth: " ^ string_of_int depth);
87   match cache_examine cache cache_key with
88   | Failed_in i when i > depth -> cache
89   | Notfound  
90   | Failed_in _ 
91   | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
92   | Succeded t -> cache 
93                   (*
94       prerr_endline (CicPp.ppterm t);
95       assert false (* if succed it can't fail *) *)
96 ;;
97 let cache_add_success ((univ,_) as cache) cache_key proof =
98   let u_key = Universe.key cache_key in
99   if u_key <> cache_key then
100     Universe.index univ u_key proof, snd cache
101   else
102     univ, 
103     snd 
104     (match cache_examine cache cache_key with
105     | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
106     | UnderInspection -> cache_replace cache cache_key (Succeded proof)
107     | Succeded t -> (* we may decide to keep the smallest proof *) cache
108     | Notfound -> cache_replace cache cache_key (Succeded proof))
109 (*
110   (if Universe.key cache_key = cache_key then
111     Universe.index univ cache_key proof
112   else
113     univ),snd
114   (prerr_endline ("CACHE: ADD SUCCESS" ^ CicPp.ppterm cache_key);
115   match cache_examine cache cache_key with
116   | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
117   | UnderInspection -> cache_replace cache cache_key (Succeded proof)
118   | Succeded t -> (* we may decide to keep the smallest proof *) cache
119   | Notfound -> cache_replace cache cache_key (Succeded proof))
120 ;;
121 *)
122 let cache_add_underinspection ((univ,oldcache) as cache) cache_key depth =
123   prerr_endline ("CACHE: ADD INSPECTING" ^ CicPp.ppterm cache_key);
124   match cache_examine cache cache_key with
125   | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
126   | Notfound -> univ,(cache_key,UnderInspection)::oldcache
127   | Failed_in _ 
128   | UnderInspection 
129   | Succeded _ -> assert false (* it must be a new goal *)
130 ;;
131 let cache_print context (_,oldcache) = 
132   let names = List.map (function None -> None | Some (x,_) -> Some x) context in
133   String.concat "\n" 
134     (HExtlib.filter_map 
135       (function 
136         | (k,Succeded _) -> Some ("CACHE SUCCESS: " ^ CicPp.pp k names)
137         | _ -> None)
138       oldcache)
139 ;;
140 let cache_remove_underinspection ((univ,oldcache) as cache) cache_key =
141   prerr_endline ("CACHE: REMOVE INSPECTING" ^ CicPp.ppterm cache_key);
142   match cache_examine cache cache_key with
143   | Notfound 
144   | Failed_in _ (* -> assert false  *)
145   | UnderInspection ->  cache_remove cache cache_key
146   | Succeded _ -> cache (* 
147       prerr_endline (CicPp.ppterm cache_key);            
148       assert false (* it must be a new goal *) *)
149 ;;
150 let cache_size (_,oldcache) = 
151   List.length (List.filter (function (_,Succeded _) -> true | _ -> false) oldcache)
152 ;;
153 let cache_clean (univ,oldcache) = 
154   univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache
155 ;;