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 module Codomain = struct
28 let compare = Pervasives.compare
30 module S = Set.Make(Codomain)
31 module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
34 type cache_key = Cic.term
37 | Succeded of Cic.term
40 type cache = (universe * ((cache_key * cache_elem) list));;
42 let cache_empty = (TI.empty,[]);;
43 let get_candidates (univ,_) ty =
44 S.elements (TI.retrieve_unifiables univ ty)
47 let rec unfold context = function
48 | Cic.Prod(name,s,t) ->
49 let t' = unfold ((Some (name,Cic.Decl s))::context) t in
51 | t -> ProofEngineReduction.unfold context t
53 let rec head = function
54 | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t)
58 let index ((univ,oldcache) as cache) key term =
62 prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
63 (TI.index univ key term,oldcache)
66 let index_term_and_unfolded_term cache context t ty =
68 let cache = index cache key t in
70 let key = head (unfold context ty) in
72 with ProofEngineTypes.Fail _ -> cache
75 let cache_add_library dbd proof gl cache =
76 let univ = MetadataQuery.universe_of_goals ~dbd proof gl in
77 let terms = List.map CicUtil.term_of_uri univ in
78 let tyof t = fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)in
82 let key = head (tyof term) in
85 index_term_and_unfolded_term acc [] term (tyof term))
88 let cache_add_context context metasenv cache =
89 let tail = function [] -> [] | h::tl -> tl in
92 (fun (acc,i,ctx) ctxentry ->
94 | Some (_,Cic.Decl t) ->
95 let ty = CicSubstitution.lift i t in
96 let elem = Cic.Rel i in
97 index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
98 (* index acc key elem, i+1, tail ctx *)
99 | Some (_,Cic.Def (_,Some t)) ->
100 let ty = CicSubstitution.lift i t in
101 let elem = Cic.Rel i in
102 index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
103 | Some (_,Cic.Def (t,None)) ->
104 let ctx = tail ctx in
106 CicSubstitution.lift i
107 (fst (CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph))
109 let elem = Cic.Rel i in
110 index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
111 | _ -> acc,i+1,tail ctx)
112 (cache,1,context) context
117 let cache_examine (_,oldcache) cache_key =
118 try List.assoc cache_key oldcache with Not_found -> Notfound
120 let cache_replace (univ,oldcache) key v =
121 let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
122 univ, (key,v)::oldcache
124 let cache_remove (univ,oldcache) key =
125 let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
128 let cache_add_failure cache cache_key depth =
129 match cache_examine cache cache_key with
130 | Failed_in i when i > depth -> cache
133 | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
135 prerr_endline (CicPp.ppterm t);
136 assert false (* if succed it can't fail *)
138 let cache_add_success ((univ,_) as cache) cache_key proof =
139 TI.index univ cache_key proof,snd
140 (match cache_examine cache cache_key with
141 | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
142 | UnderInspection -> cache_replace cache cache_key (Succeded proof)
143 | Succeded t -> (* we may decide to keep the smallest proof *) cache
144 | Notfound -> cache_replace cache cache_key (Succeded proof))
146 let cache_add_underinspection ((univ,oldcache) as cache) cache_key depth =
147 match cache_examine cache cache_key with
148 | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
149 | Notfound -> univ,(cache_key,UnderInspection)::oldcache
152 | Succeded _ -> assert false (* it must be a new goal *)
154 let cache_print context (_,oldcache) =
155 let names = List.map (function None -> None | Some (x,_) -> Some x) context in
159 | (k,Succeded _) -> Some (CicPp.pp k names)
163 let cache_remove_underinspection ((univ,oldcache) as cache) cache_key =
164 match cache_examine cache cache_key with
166 | UnderInspection -> cache_remove cache cache_key
167 | Failed_in _ -> assert false
168 | Succeded _ -> assert false (* it must be a new goal *)
170 let cache_size (_,oldcache) =
171 List.length (List.filter (function (_,Succeded _) -> true | _ -> false) oldcache)
173 let cache_clean (univ,oldcache) =
174 univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache