- inside dicrimination_tree is now checked the invariant that bad terms are indexed...

- autoCache (should) not index bad terms

diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml
index b2906e1c9c741d774b0492790a62861f9a5aae82..92877a8297f8ae0f775e2507cd6d229686731b0c 100644 (file)
--- a/helm/software/components/cic/discrimination_tree.ml
+++ b/helm/software/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/helm/software/components/tactics/autoCache.ml b/helm/software/components/tactics/autoCache.ml
index 57701310c445b3de47adc3e56aa3806708e397fc..5fb4640d71e2c8308280a64e090c0bb5a32d6494 100644 (file)
--- a/helm/software/components/tactics/autoCache.ml
+++ b/helm/software/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/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index b2348f732a0b014fa26d515e28b8b9cb0401bd57..8442779d34dd2896c8f6777617963d9e6f82903b 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/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/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index 6dbdb950ab1b66265ccb087058687fd4085d0bbd..99041ed1ba33a8e1e526d1e96656f7c13a612046 100644 (file)
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/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/helm/software/components/tactics/universe.mli b/helm/software/components/tactics/universe.mli
index 4ae0ff961e2fa511c4ea8db2632629094fdcc4ce..ee5dc489aa63d9d1a1104032e2109527c8c5894c 100644 (file)
--- a/helm/software/components/tactics/universe.mli
+++ b/helm/software/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: