From: Enrico Tassi Date: Sat, 6 Jan 2007 16:16:40 +0000 (+0000) Subject: - inside dicrimination_tree is now checked the invariant that bad terms are indexed... X-Git-Tag: 0.4.95@7852~676 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cd8e629ba1f9f4a0af45092ddd924910e5209bfd;p=helm.git - inside dicrimination_tree is now checked the invariant that bad terms are indexed, but this invariant is not always respected, so a 'Dead' representative is used and a warning is printed. - autoCache (should) not index bad terms --- diff --git a/components/cic/discrimination_tree.ml b/components/cic/discrimination_tree.ml index b2906e1c9..92877a829 100644 --- a/components/cic/discrimination_tree.ml +++ b/components/cic/discrimination_tree.ml @@ -30,8 +30,8 @@ module DiscriminationTreeIndexing = struct type path_string_elem = - | Function | Constant of UriManager.uri - | Bound of int | Variable | Proposition | Datatype ;; + | Constant of UriManager.uri + | Bound of int | Variable | Proposition | Datatype | Dead;; type path_string = path_string_elem list;; @@ -39,28 +39,34 @@ module DiscriminationTreeIndexing = * "functions" *) let ppelem = function - | Function -> "Fun" | Constant uri -> UriManager.name_of_uri uri | Bound i -> string_of_int i | Variable -> "?" | Proposition -> "Prop" | Datatype -> "Type" + | Dead -> "DEAD" ;; let pppath l = String.concat "::" (List.map ppelem l) ;; let elem_of_cic = function - | Cic.Meta _ -> Variable - | Cic.Lambda _ -> Function + | Cic.Meta _ | Cic.Implicit _ -> Variable | Cic.Rel i -> Bound i | Cic.Sort (Cic.Prop) -> Proposition | Cic.Sort _ -> Datatype - | term -> - try Constant (CicUtil.uri_of_term term) - with Invalid_argument _ -> Variable (* HACK! *) + | Cic.Const _ | Cic.Var _ | Cic.MutInd _ | Cic.MutConstruct _ as t -> + (try Constant (CicUtil.uri_of_term t) + with Invalid_argument _ -> assert false) + | Cic.Appl _ -> + assert false (* should not happen *) + | Cic.LetIn _ | Cic.Lambda _ | Cic.Prod _ | Cic.Cast _ + | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> + prerr_endline "FIXME: the trie receives an invalid term"; + Dead + (* assert false universe.ml removes these *) ;; let path_string_of_term arities = let set_arity arities k n = (assert (k<>Variable || n=0); - (k,n)::(List.remove_assoc k arities)) + if k = Dead then arities else (k,n)::(List.remove_assoc k arities)) in let rec aux arities = function | Cic.Appl ((hd::tl) as l) -> diff --git a/components/tactics/autoCache.ml b/components/tactics/autoCache.ml index 57701310c..5fb4640d7 100644 --- a/components/tactics/autoCache.ml +++ b/components/tactics/autoCache.ml @@ -35,7 +35,10 @@ type cache = (Universe.universe * ((cache_key * cache_elem) list));; let cache_empty = (Universe.empty,[]);; let get_candidates (univ,_) ty = - Universe.get_candidates univ ty + if Universe.key ty = ty then + Universe.get_candidates univ ty + else + [] ;; let index (univ,cache) key term = @@ -77,7 +80,10 @@ let cache_add_failure cache cache_key depth = assert false (* if succed it can't fail *) ;; let cache_add_success ((univ,_) as cache) cache_key proof = - Universe.index univ cache_key proof,snd + (if Universe.key cache_key = cache_key then + Universe.index univ cache_key proof + else + univ),snd (match cache_examine cache cache_key with | Failed_in _ -> cache_replace cache cache_key (Succeded proof) | UnderInspection -> cache_replace cache cache_key (Succeded proof) diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index b2348f732..8442779d3 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1294,10 +1294,10 @@ let fix_proof metasenv context all_implicits p = aux metasenv 0 p ;; -let fix_metasenv metasenv context = +let fix_metasenv metasenv = List.fold_left (fun m (i,c,t) -> - let m,t = fix_proof m context false t in + let m,t = fix_proof m c false t in let m = List.filter (fun (j,_,_) -> j<>i) m in (i,c,t)::m) metasenv metasenv @@ -1344,7 +1344,7 @@ let build_proof context proof_menv in let goal_proof = Subst.apply_subst subsumption_subst goal_proof in - let real_menv = fix_metasenv (proof_menv@metasenv) context in + let real_menv = fix_metasenv (proof_menv@metasenv) in let real_menv,goal_proof = fix_proof real_menv context false goal_proof in (* diff --git a/components/tactics/universe.ml b/components/tactics/universe.ml index 6dbdb950a..99041ed1b 100644 --- a/components/tactics/universe.ml +++ b/components/tactics/universe.ml @@ -41,7 +41,7 @@ let get_candidates univ ty = let rec unfold context = function | Cic.Prod(name,s,t) -> let t' = unfold ((Some (name,Cic.Decl s))::context) t in - Cic.Prod(name,s,t') + Cic.Prod(name,s,t') | t -> ProofEngineReduction.unfold context t let rec collapse_head_metas t = @@ -74,25 +74,26 @@ let rec collapse_head_metas t = let rec dummies_of_coercions = function | Cic.Appl (c::l) when CoercDb.is_a_coercion' c -> - Cic.Meta (-1,[]) + Cic.Meta (-1,[]) | Cic.Appl l -> - let l' = List.map dummies_of_coercions l in Cic.Appl l' + let l' = List.map dummies_of_coercions l in Cic.Appl l' | Cic.Lambda(n,s,t) -> - let s' = dummies_of_coercions s in - let t' = dummies_of_coercions t in - Cic.Lambda (n,s',t') + let s' = dummies_of_coercions s in + let t' = dummies_of_coercions t in + Cic.Lambda (n,s',t') | Cic.Prod(n,s,t) -> - let s' = dummies_of_coercions s in - let t' = dummies_of_coercions t in - Cic.Prod (n,s',t') + let s' = dummies_of_coercions s in + let t' = dummies_of_coercions t in + Cic.Prod (n,s',t') | Cic.LetIn(n,s,t) -> - let s' = dummies_of_coercions s in - let t' = dummies_of_coercions t in - Cic.LetIn (n,s',t') + let s' = dummies_of_coercions s in + let t' = dummies_of_coercions t in + Cic.LetIn (n,s',t') | Cic.MutCase _ -> Cic.Meta (-1,[]) | t -> t ;; + let rec head remove_coercions t = let clean_up t = if remove_coercions then dummies_of_coercions t @@ -118,6 +119,8 @@ let keys context ty = [head true ty; head true (unfold context ty)] with ProofEngineTypes.Fail _ -> [head true ty] +let key term = head false term + let index_term_and_unfolded_term univ context t ty = let key = head true ty in let univ = index univ key t in diff --git a/components/tactics/universe.mli b/components/tactics/universe.mli index 4ae0ff961..ee5dc489a 100644 --- a/components/tactics/universe.mli +++ b/components/tactics/universe.mli @@ -32,6 +32,7 @@ val index: Cic.term -> (* value *) universe val keys: Cic.context -> Cic.term -> Cic.term list +val key: Cic.term -> Cic.term val index_term_and_unfolded_term: universe -> Cic.context -> Cic.term -> Cic.term -> universe val index_local_term: