X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=34b305ba54d06e7d3f514e9dc2b018bf783805db;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=15b2d848bf7cab4facc1ace9784900fa2100f8ac;hpb=af8005720dd5a6e90f052202a7c5f108f54e652b;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 15b2d848b..34b305ba5 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -38,12 +38,14 @@ let ppterm ctx t =
   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
   CicPp.pp t names
 ;;
+
 let is_propositional context sort = 
   match CicReduction.whd context sort with
   | Cic.Sort Cic.Prop 
   | Cic.Sort (Cic.CProp _) -> true
   | _-> false
 ;;
+
 let is_in_prop context subst metasenv ty =
   let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
   is_propositional context sort
@@ -368,32 +370,12 @@ let init_cache_and_tables
 =
   let _, metasenv, subst, _, _, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let is_prop m s c t = 
-    let ty,_ = 
-      CicTypeChecker.type_of_aux' m ~subst:s c t CicUniv.oblivion_ugraph
-    in
-    let sort,_ = 
-      CicTypeChecker.type_of_aux' m ~subst:s c ty CicUniv.oblivion_ugraph
-    in
-    match CicReduction.whd ~subst c sort with
-    | 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
+    List.fold_left 
+      (fun automation_cache (t,_) -> 
+          AutomationCache.add_term_to_active automation_cache
+           metasenv subst context t None)
+      automation_cache ct
   in
   if restricted_univ = [] then
     let ct = 
@@ -406,29 +388,22 @@ 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, _ = add_list_to_tables metasenv subst automation_cache ct 
+    let automation_cache = 
+      add_list_to_tables metasenv subst automation_cache ct 
     in
-    (* AutomationCache.pp_cache automation_cache; *)
+(*     AutomationCache.pp_cache automation_cache; *)
     automation_cache.AutomationCache.univ, 
     automation_cache.AutomationCache.tables, 
     cache
   else
-    let metasenv, t_ty, s_t_ty, _ = 
-      List.fold_left
-        (fun (metasenv as orig,acc, sacc, maxmeta) t ->
-           let ty, _ = 
-             CicTypeChecker.type_of_aux' 
-               metasenv ~subst:[] context t CicUniv.oblivion_ugraph 
-           in
-           let head, metasenv, args, maxmeta =
-             TermUtil.saturate_term maxmeta metasenv context ty 0
-           in
-           if List.exists (is_prop metasenv subst context) args then
-             orig, (t,ty)::acc, sacc, maxmeta
-           else
-             let st = if args = [] then t else Cic.Appl (t::args) in
-             metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta)
-        (metasenv, [],[], CicMkImplicit.new_meta metasenv subst) restricted_univ
+    let t_ty = 
+      List.map
+        (fun  t ->
+          let ty, _ = CicTypeChecker.type_of_aux' 
+            metasenv ~subst:[] context t CicUniv.oblivion_ugraph
+          in
+            t, ty)
+        restricted_univ
     in
     (* let automation_cache = AutomationCache.empty () in *) 
     let automation_cache = 
@@ -439,74 +414,21 @@ let init_cache_and_tables
       { automation_cache with AutomationCache.univ = universe }
     in
     let ct = 
-      if use_context then find_context_theorems context metasenv else [] 
+     if use_context then find_context_theorems context metasenv else t_ty
     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 *)
+      add_list_to_tables metasenv subst automation_cache ct
+    in
     (* AutomationCache.pp_cache automation_cache; *)
     automation_cache.AutomationCache.univ, 
     automation_cache.AutomationCache.tables, 
-    (* cache_add_list cache_empty context t_ty *)
     cache_empty
 ;;
-  (*
-(*   let signature = MetadataQuery.signature_of metasenv goal in *)
-(*   let newmeta = CicMkImplicit.new_meta metasenv [] in *)
-  let equations = 
-    retrieve_equations dont_filter (* true *) signature universe cache context metasenv 
-  in
-  debug_print 
-    (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
-  let eqs_and_types =
-    HExtlib.filter_map 
-      (fun t -> 
-         let ty,_ =
-           CicTypeChecker.type_of_aux' 
-             metasenv context t CicUniv.oblivion_ugraph
-         in
-         (* retrieve_equations could also return flexible terms *)
-         if is_an_equality ty then Some(t,ty) 
-         else
-           try
-             let ty' = unfold context ty in
-             if is_an_equality ty' then Some(t,ty') else None
-           with ProofEngineTypes.Fail _ -> None) 
-      equations
-  in
-  let bag = Equality.mk_equality_bag () in
-  let units, other_equalities, newmeta = 
-    partition_unit_equalities context metasenv newmeta bag eqs_and_types 
-  in
-  (* SIMPLIFICATION STEP 
-  let equalities = 
-    let env = (metasenv, context, CicUniv.oblivion_ugraph) in 
-    let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
-    Saturation.simplify_equalities bag eq_uri env units 
-  in 
-  *)
-  let passive = Saturation.make_passive units in
-  let no = List.length units in
-  let active = Saturation.make_active [] in
-  let active,passive,newmeta = 
-    if paramod then active,passive,newmeta
-    else
-      Saturation.pump_actives 
-        context bag newmeta active passive (no+1) infinity
-  in 
-    (active,passive,bag),cache,newmeta
-*)
 
-let fill_hypothesis context metasenv term tables (universe:Universe.universe) cache auto fast = 
+let fill_hypothesis context metasenv subst term tables (universe:Universe.universe) cache auto fast = 
   let actives, passives, bag = tables in 
   let bag, head, metasenv, args = 
-    Equality.saturate_term bag metasenv context term 
+    Equality.saturate_term bag metasenv subst context term 
   in
   let tables = actives, passives, bag in 
   let propositional_args = 
@@ -568,14 +490,14 @@ let fill_hypothesis context metasenv term tables (universe:Universe.universe) ca
   results,cache,tables
 ;;
 
-let build_equalities auto context metasenv tables universe cache equations =
+let build_equalities auto context metasenv subst tables universe cache equations =
   List.fold_left 
     (fun (tables,facts,cache) (t,ty) ->
        (* in any case we add the equation to the cache *)
        let cache = AutoCache.cache_add_list cache context [(t,ty)] in
        try
          let saturated, cache, tables = 
-           fill_hypothesis context metasenv ty tables universe cache auto true
+           fill_hypothesis context metasenv subst ty tables universe cache auto true
          in
          let eqs, tables = 
            List.fold_left 
@@ -596,10 +518,9 @@ let build_equalities auto context metasenv tables universe cache equations =
       )
     (tables,[],cache) equations
 
-let close_more tables context status auto universe cache =
+let close_more tables context status auto signature universe cache =
   let proof, goalno = status in
-  let _, metasenv,_subst,_,_, _ = proof in  
-  let signature = MetadataQuery.signature_of metasenv goalno in
+  let _, metasenv,subst,_,_, _ = proof in  
   let equations = 
     retrieve_equations false signature universe cache context metasenv 
   in
@@ -613,7 +534,7 @@ let close_more tables context status auto universe cache =
            if is_an_equality ty then Some(t,ty) else None)
       equations in
   let tables, units, cache = 
-    build_equalities auto context metasenv tables universe cache eqs_and_types 
+    build_equalities auto context metasenv subst tables universe cache eqs_and_types 
   in
   let active,passive,bag = tables in
   let passive = Saturation.add_to_passive units passive in
@@ -629,7 +550,7 @@ let find_context_equalities dbd tables context proof (universe:Universe.universe
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let _,metasenv,_subst,_,_, _ = proof in
+  let _,metasenv,subst,_,_, _ = proof in
   (* if use_auto is true, we try to close the hypothesis of equational
     statements using auto; a naif, and probably wrong approach *)
   let rec aux tables cache index = function
@@ -644,7 +565,7 @@ let find_context_equalities dbd tables context proof (universe:Universe.universe
               (try 
                 let term = S.lift index term in
                 let saturated, cache, tables = 
-                  fill_hypothesis context metasenv term 
+                  fill_hypothesis context metasenv subst term 
                     tables universe cache default_auto false
                 in
                 let actives, passives, bag = tables in 
@@ -1115,8 +1036,8 @@ let apply_smart_aux
            automation_cache univ (proof'''',newmeta)
         in
         match
-          Saturation.given_clause bag (proof'''',newmeta) active passive 
-            1 0 infinity
+          Saturation.solve_narrowing bag (proof'''',newmeta) active passive 
+            1 (*0 infinity*)
         with 
           | None, active, passive, bag -> 
               raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
@@ -1619,8 +1540,7 @@ let equational_case
           1,0,flags.timeout 
         in
         match
-          Saturation.given_clause bag status active passive 
-            goal_steps saturation_steps timeout
+          Saturation.solve_narrowing bag status active passive goal_steps 
         with 
           | None, active, passive, bag -> 
               [], (active,passive,bag), cache, flags
@@ -1712,18 +1632,27 @@ let try_candidate dbd
 ;;
 
 let applicative_case dbd
-  tables depth subst fake_proof goalno goalty metasenv context universe
-  cache flags
+  tables depth subst fake_proof goalno goalty metasenv context 
+  signature universe cache flags
 = 
-  let goalty_aux = 
+  (* let goalty_aux = 
     match goalty with
     | Cic.Appl (hd::tl) -> 
         Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
     | _ -> goalty
-  in
+  in *)
+  let goalty_aux = goalty in
   let candidates = 
     get_candidates flags.skip_trie_filtering universe cache goalty_aux
   in
+  (* if the goal is an equality we skip the congruence theorems *)
+  let candidates =
+    if is_equational_case goalty flags 
+    then List.filter not_default_eq_term candidates
+    else candidates
+  in
+  let candidates = List.filter (only signature context metasenv) candidates 
+  in
   let tables, elems = 
     List.fold_left 
       (fun (tables,elems) cand ->
@@ -1771,10 +1700,9 @@ let try_smart_candidate dbd
 ;;
 
 let smart_applicative_case dbd
-  tables depth subst fake_proof goalno goalty metasenv context universe
-  cache flags
+  tables depth subst fake_proof goalno goalty metasenv context signature
+  universe cache flags
 = 
-  let signature = MetadataQuery.signature_of metasenv goalno in
   let goalty_aux = 
     match goalty with
     | Cic.Appl (hd::tl) -> 
@@ -1838,7 +1766,7 @@ let smart_applicative_case dbd
 ;;
 
 let equational_and_applicative_case dbd
-  universe flags m s g gty tables cache context 
+  signature universe flags m s g gty tables cache context 
 =
   let goalno, depth, sort = g in
   let fake_proof = mk_fake_proof m s g gty context in
@@ -1853,7 +1781,7 @@ let equational_and_applicative_case dbd
       else
         applicative_case dbd
           tables depth s fake_proof goalno 
-            gty m context universe cache flags
+            gty m context signature universe cache flags
     in
       elems@more_elems, tables, cache, flags            
   else
@@ -1861,10 +1789,10 @@ let equational_and_applicative_case dbd
       match LibraryObjects.eq_URI () with
       | Some _ ->
          smart_applicative_case dbd tables depth s fake_proof goalno 
-           gty m context universe cache flags
+           gty m context signature universe cache flags
       | None -> 
          applicative_case dbd tables depth s fake_proof goalno 
-           gty m context universe cache flags
+           gty m context signature universe cache flags
     in
       elems, tables, cache, flags  
 ;;
@@ -1961,7 +1889,8 @@ let filter_prune_hint c l =
     cache_reset_underinspection c,      
     List.filter (condition_for_prune_hint prune) l
 ;;
-let auto_main dbd tables context flags universe cache elems =
+
+let auto_main dbd tables context flags signature universe cache elems =
   auto_context := context;
   let rec aux tables flags cache (elems : status) =
     pp_status context elems;
@@ -2073,7 +2002,7 @@ let auto_main dbd tables context flags universe cache elems =
                     (* elems are possible computations for proving gty *)
                     let elems, tables, cache, flags =
                       equational_and_applicative_case dbd
-                        universe flags m s g gty tables cache context
+                        signature universe flags m s g gty tables cache context
                     in
                     if elems = [] then
                       (* this goal has failed *)
@@ -2122,6 +2051,14 @@ let auto_main dbd tables context flags universe cache elems =
 let
   auto_all_solutions dbd tables universe cache context metasenv gl flags 
 =
+  let signature =
+    List.fold_left 
+      (fun set g ->
+	 MetadataConstraints.UriManagerSet.union set 
+	     (MetadataQuery.signature_of metasenv g)
+       )
+      MetadataConstraints.UriManagerSet.empty gl 
+  in
   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
   let goals = 
     List.map 
@@ -2129,7 +2066,7 @@ let
   in
   let elems = [metasenv,[],1,[],goals,[]] in
   let rec aux tables solutions cache elems flags =
-    match auto_main dbd tables context flags universe cache elems with
+    match auto_main dbd tables context flags signature universe cache elems with
     | Gaveup (tables,cache) ->
         solutions,cache, tables
     | Proved (metasenv,subst,others,tables,cache) -> 
@@ -2156,12 +2093,21 @@ let
 
 (******************* AUTO ***************)
 
+
 let auto dbd flags metasenv tables universe cache context metasenv gl =
-  let initial_time = Unix.gettimeofday() in
+  let initial_time = Unix.gettimeofday() in  
+  let signature =
+    List.fold_left 
+      (fun set g ->
+	 MetadataConstraints.UriManagerSet.union set 
+	     (MetadataQuery.signature_of metasenv g)
+       )
+      MetadataConstraints.UriManagerSet.empty gl 
+  in
   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
   let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
   let elems = [metasenv,[],1,[],goals,[]] in
-  match auto_main dbd tables context flags universe cache elems with
+  match auto_main dbd tables context flags signature universe cache elems with
   | Proved (metasenv,subst,_, tables,cache) -> 
       debug_print(lazy
         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
@@ -2182,19 +2128,32 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa
   in
   let _,metasenv,subst,_,_, _ = proof in
   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
+  let signature = MetadataQuery.signature_of metasenv goal in
+  let signature = 
+    List.fold_left 
+      (fun set t ->
+         let ty, _ = 
+	   CicTypeChecker.type_of_aux' metasenv context t 
+	     CicUniv.oblivion_ugraph
+	 in
+	 MetadataConstraints.UriManagerSet.union set 
+	   (MetadataConstraints.constants_of ty)
+       )
+      signature univ
+  in
   let tables,cache =
     if flags.close_more then
       close_more 
         tables context (proof, goal) 
-          (auto_all_solutions dbd) universe cache 
+          (auto_all_solutions dbd) signature universe cache 
     else tables,cache in
   let initial_time = Unix.gettimeofday() in
   let (_,oldmetasenv,_,_,_, _) = proof in
-  hint := None;
+    hint := None;
   let elem = 
     metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
   in
-  match auto_main dbd tables context flags universe cache [elem] with
+  match auto_main dbd tables context flags signature universe cache [elem] with
     | Proved (metasenv,subst,_, tables,cache) -> 
         debug_print (lazy 
           ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));