From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 5 May 2009 11:11:00 +0000 (+0000)
Subject: Nuova gestione di "by" per auto.
X-Git-Tag: make_still_working~4023
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=af8005720dd5a6e90f052202a7c5f108f54e652b;p=helm.git

Nuova gestione di "by" per auto.
---

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 73a96d23b..15b2d848b 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -379,6 +379,22 @@ let init_cache_and_tables
     | Cic.Sort Cic.Prop | Cic.Sort (Cic.CProp _) -> true
     | _ -> false
   in
+  let add_list_to_tables metasenv subst automation_cache ct =
+    let _,_,bag = automation_cache.AutomationCache.tables in
+    let maxmeta = Equality.maxmeta bag in
+    List.fold_left
+      (fun (c,maxmeta) (t,ty) ->            
+         let head, metasenv, args, maxmeta =
+           TermUtil.saturate_term maxmeta metasenv context ty 0
+         in
+         if List.exists (is_prop metasenv subst context) args then
+           c,maxmeta
+         else
+           let st = if args = [] then t else Cic.Appl (t::args) in
+           AutomationCache.add_term_to_active 
+             c metasenv [] context st (Some head), maxmeta)
+       (automation_cache,maxmeta) ct
+  in
   if restricted_univ = [] then
     let ct = 
       if use_context then find_context_theorems context metasenv else [] 
@@ -390,19 +406,7 @@ let init_cache_and_tables
     in
     let cache = AutoCache.cache_empty in
     let cache = cache_add_list cache context (ct@lt) in  
-    let automation_cache, _ = 
-     List.fold_left
-      (fun (c,maxmeta) (t,ty) ->            
-         let head, metasenv, args, maxmeta =
-           TermUtil.saturate_term maxmeta metasenv context ty 0
-         in
-         if List.exists (is_prop metasenv subst context) args then
-           c,maxmeta
-         else
-           let st = if args = [] then t else Cic.Appl (t::args) in
-           AutomationCache.add_term_to_active 
-             c metasenv [] context st (Some head), maxmeta)
-       (automation_cache,CicMkImplicit.new_meta metasenv subst) ct
+    let automation_cache, _ = add_list_to_tables metasenv subst automation_cache ct 
     in
     (* AutomationCache.pp_cache automation_cache; *)
     automation_cache.AutomationCache.univ, 
@@ -426,24 +430,31 @@ let init_cache_and_tables
              metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta)
         (metasenv, [],[], CicMkImplicit.new_meta metasenv subst) restricted_univ
     in
-    let automation_cache = AutomationCache.empty () in
+    (* let automation_cache = AutomationCache.empty () in *) 
     let automation_cache = 
-      let universe = automation_cache.AutomationCache.univ in
+      let universe = Universe.empty in
       let universe = 
         Universe.index_list universe context t_ty
       in
       { automation_cache with AutomationCache.univ = universe }
     in
+    let ct = 
+      if use_context then find_context_theorems context metasenv else [] 
+    in
+    let automation_cache, _ = add_list_to_tables metasenv subst automation_cache ct
+    in
+    (* proviamo a tenere tutte le equazioni 
     let automation_cache = 
      List.fold_left
       (fun c (t,ty) ->            
          AutomationCache.add_term_to_active c metasenv [] context t (Some ty))
        automation_cache s_t_ty
-    in
+    in *)
     (* AutomationCache.pp_cache automation_cache; *)
     automation_cache.AutomationCache.univ, 
     automation_cache.AutomationCache.tables, 
-    cache_add_list cache_empty context t_ty
+    (* cache_add_list cache_empty context t_ty *)
+    cache_empty
 ;;
   (*
 (*   let signature = MetadataQuery.signature_of metasenv goal in *)
@@ -1779,7 +1790,11 @@ let smart_applicative_case dbd
   let smart_candidates = 
     List.filter
       (fun x -> not(List.mem x candidates)) smart_candidates
-  in
+  in 
+  let debug_msg =
+    (lazy ("smart_candidates" ^ " = " ^ 
+             (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
+  debug_print debug_msg;
   let candidates = List.filter (only signature context metasenv) candidates in
   let smart_candidates = 
     List.filter (only signature context metasenv) smart_candidates