From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 20 Oct 2006 15:32:34 +0000 (+0000)
Subject: a. uniform mangement for context and library
X-Git-Tag: 0.4.95@7852~867
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4996fef9a745a372717fbc20bd5f0eef7a08552b;p=helm.git

a. uniform mangement for context and library
b. collapsing flexible terms (X args) into a single meta. Metas in
   head position give arity problems with discrimination trees.
c. Even terms with a single meta as conlcusion (e.g. elimination
   principles) get indexed.
---

diff --git a/components/tactics/autoCache.ml b/components/tactics/autoCache.ml
index 4c1871388..0b42391fa 100644
--- a/components/tactics/autoCache.ml
+++ b/components/tactics/autoCache.ml
@@ -49,18 +49,30 @@ let rec unfold context = function
       let t' = unfold ((Some (name,Cic.Decl s))::context) t in
 	Cic.Prod(name,s,t')	
   | t -> ProofEngineReduction.unfold context t
+
+
+let rec collapse_head_metas = function 
+  | Cic.Appl(a::l) -> 
+      let a' = collapse_head_metas a in
+      (match a' with
+	| Cic.Meta(n,m) -> Cic.Meta(n,m)
+	| t -> 	
+	    let l' = List.map collapse_head_metas l in
+	       Cic.Appl(t::l'))
+  | t -> t
+;;
   
-let rec head = function 
-  | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t)
+let rec head t = 
+  let rec aux = function
+  | Cic.Prod(_,_,t) -> 
+      CicSubstitution.subst (Cic.Meta (-1,[])) (aux t)
   | t -> t
+  in collapse_head_metas (aux t)
 ;;
 
-let index ((univ,oldcache) as cache) key term =
-  match key with
-  | Cic.Meta _ -> cache
-  | _ -> 
-      prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
-      (TI.index univ key term,oldcache)
+let index (univ,oldcache) 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 =
@@ -72,47 +84,11 @@ let index_term_and_unfolded_term cache context t ty =
   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_term_and_unfolded_term acc [] term (tyof term))
-    cache terms
-;;
-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 ty = CicSubstitution.lift i t in
-          let elem = Cic.Rel i in
-	  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 ty = CicSubstitution.lift i t in
-          let elem = Cic.Rel i in
-	  index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
-      | Some (_,Cic.Def (t,None)) ->
-          let ctx = tail ctx in 
-          let ty = 
-	    CicSubstitution.lift i
-              (fst (CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph))
-          in
-          let elem = Cic.Rel i in
-	  index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
-      |  _ -> acc,i+1,tail ctx)
-    (cache,1,context) context
-  in
-  rc
-;;
+let cache_add_list cache context terms_and_types =
+  List.fold_left  
+    (fun acc (term,ty) -> 
+       index_term_and_unfolded_term acc context term ty)
+    cache terms_and_types
 
 let cache_examine (_,oldcache) cache_key = 
   try List.assoc cache_key oldcache with Not_found -> Notfound
diff --git a/components/tactics/autoCache.mli b/components/tactics/autoCache.mli
index b47a29925..61c658811 100644
--- a/components/tactics/autoCache.mli
+++ b/components/tactics/autoCache.mli
@@ -31,11 +31,8 @@ type cache_elem =
   | UnderInspection
   | Notfound
 val get_candidates: cache -> Cic.term -> Cic.term list
-val cache_add_library: 
-  HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list ->
-    cache -> cache
-val cache_add_context: Cic.context -> Cic.metasenv -> cache -> cache
-
+val cache_add_list: 
+    cache -> Cic.context -> (Cic.term*Cic.term) list -> cache
 val cache_examine: cache -> cache_key -> cache_elem
 val cache_add_failure: cache -> cache_key -> int -> cache 
 val cache_add_success: cache -> cache_key -> Cic.term -> cache