1 (* Copyright (C) 2002, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 type cache_key = Cic.term
29 | Succeded of Cic.term
32 type cache = (Universe.universe * ((cache_key * cache_elem) list));;
35 let cache_empty = (Universe.empty,[]);;
37 let get_candidates (univ,_) ty =
38 if Universe.key ty = ty then
39 Universe.get_candidates univ ty
44 let index (univ,cache) key term =
45 Universe.index univ key term,cache
48 let index_term_and_unfolded_term (univ,cache) context t ty =
49 Universe.index_local_term univ context t ty, cache
52 let cache_add_list (univ,cache) context terms_and_types =
56 Universe.index_local_term univ context t ty)
61 let cache_examine (_,oldcache) cache_key =
62 try List.assoc cache_key oldcache with Not_found -> Notfound
64 let cache_replace (univ,oldcache) key v =
65 let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
66 univ, (key,v)::oldcache
68 let cache_remove (univ,oldcache) key =
69 let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
72 let cache_add_failure cache cache_key depth =
73 match cache_examine cache cache_key with
74 | Failed_in i when i > depth -> cache
77 | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
79 prerr_endline (CicPp.ppterm t);
80 assert false (* if succed it can't fail *)
82 let cache_add_success ((univ,_) as cache) cache_key proof =
83 (if Universe.key cache_key = cache_key then
84 Universe.index univ cache_key proof
87 (match cache_examine cache cache_key with
88 | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
89 | UnderInspection -> cache_replace cache cache_key (Succeded proof)
90 | Succeded t -> (* we may decide to keep the smallest proof *) cache
91 | Notfound -> cache_replace cache cache_key (Succeded proof))
93 let cache_add_underinspection ((univ,oldcache) as cache) cache_key depth =
94 match cache_examine cache cache_key with
95 | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
96 | Notfound -> univ,(cache_key,UnderInspection)::oldcache
99 | Succeded _ -> assert false (* it must be a new goal *)
101 let cache_print context (_,oldcache) =
102 let names = List.map (function None -> None | Some (x,_) -> Some x) context in
106 | (k,Succeded _) -> Some (CicPp.pp k names)
110 let cache_remove_underinspection ((univ,oldcache) as cache) cache_key =
111 match cache_examine cache cache_key with
113 | UnderInspection -> cache_remove cache cache_key
114 | Failed_in _ -> assert false
115 | Succeded _ -> assert false (* it must be a new goal *)
117 let cache_size (_,oldcache) =
118 List.length (List.filter (function (_,Succeded _) -> true | _ -> false) oldcache)
120 let cache_clean (univ,oldcache) =
121 univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache