From: Andrea Asperti Date: Mon, 9 Oct 2006 16:33:24 +0000 (+0000) Subject: Theorems from the library and from the context are indexed also in "unfolded" X-Git-Tag: 0.4.95@7852~919 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4fdb66a6436a18128faff1b5b97637c6ffb61f34;p=helm.git Theorems from the library and from the context are indexed also in "unfolded" version. --- diff --git a/components/tactics/autoCache.ml b/components/tactics/autoCache.ml index b4e074a64..4c1871388 100644 --- a/components/tactics/autoCache.ml +++ b/components/tactics/autoCache.ml @@ -43,10 +43,18 @@ let cache_empty = (TI.empty,[]);; let get_candidates (univ,_) ty = S.elements (TI.retrieve_unifiables 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') + | t -> ProofEngineReduction.unfold context t + let rec head = function | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t) | t -> t ;; + let index ((univ,oldcache) as cache) key term = match key with | Cic.Meta _ -> cache @@ -54,40 +62,54 @@ let index ((univ,oldcache) as cache) key term = prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term); (TI.index univ key term,oldcache) ;; + +let index_term_and_unfolded_term cache context t ty = + let key = head ty in + let cache = index cache key t in + try + let key = head (unfold context ty) in + index cache key t + with ProofEngineTypes.Fail _ -> cache +;; + let cache_add_library dbd proof gl cache = let univ = MetadataQuery.universe_of_goals ~dbd proof gl in let terms = List.map CicUtil.term_of_uri univ in let tyof t = fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)in List.fold_left (fun acc term -> + (* let key = head (tyof term) in - index acc key term) + index acc key term + *) + index_term_and_unfolded_term acc [] term (tyof term)) cache terms ;; -let cache_add_context ctx metasenv cache = +let cache_add_context context metasenv cache = let tail = function [] -> [] | h::tl -> tl in let rc,_,_ = List.fold_left (fun (acc,i,ctx) ctxentry -> match ctxentry with | Some (_,Cic.Decl t) -> - let key = CicSubstitution.lift i (head t) in + let ty = CicSubstitution.lift i t in let elem = Cic.Rel i in - index acc key elem, i+1, tail ctx + index_term_and_unfolded_term acc context elem ty, i+1, tail ctx + (* index acc key elem, i+1, tail ctx *) | Some (_,Cic.Def (_,Some t)) -> - let key = CicSubstitution.lift i (head t) in + let ty = CicSubstitution.lift i t in let elem = Cic.Rel i in - index acc key elem, i+1, tail ctx + index_term_and_unfolded_term acc context elem ty, i+1, tail ctx | Some (_,Cic.Def (t,None)) -> let ctx = tail ctx in - let key,_ = - CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph + let ty = + CicSubstitution.lift i + (fst (CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph)) in let elem = Cic.Rel i in - let key = CicSubstitution.lift i (head key) in - index acc key elem, i+1, ctx + index_term_and_unfolded_term acc context elem ty, i+1, tail ctx | _ -> acc,i+1,tail ctx) - (cache,1,ctx) ctx + (cache,1,context) context in rc ;;