X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=53120a44d80940decbd54ad7d6b5932f6f7bd8cc;hb=25564c06c570e5ab9be455904c0b381842f8d4c4;hp=45cab35026a4dd196ee765c4cd742cf3918da073;hpb=d4b31ea5ca7c7dd3344cb284a89fac22312834cf;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 45cab3502..53120a44d 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -368,16 +368,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
+  let add_list_to_tables metasenv subst automation_cache 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 = 
@@ -390,112 +386,47 @@ 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, 
     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 = 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 t_ty
+    in
     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
+      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_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 = 
@@ -557,14 +488,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 
@@ -587,7 +518,7 @@ let build_equalities auto context metasenv tables universe cache equations =
 
 let close_more tables context status auto universe cache =
   let proof, goalno = status in
-  let _, metasenv,_subst,_,_, _ = proof in  
+  let _, metasenv,subst,_,_, _ = proof in  
   let signature = MetadataQuery.signature_of metasenv goalno in
   let equations = 
     retrieve_equations false signature universe cache context metasenv 
@@ -602,7 +533,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
@@ -618,7 +549,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
@@ -633,7 +564,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 
@@ -1091,9 +1022,37 @@ let apply_smart_aux
        (PrimitiveTactics.apply_tac term'')
        (proof''',goal) 
    in
+
+
+   let (_,m,_,_,_,_ as p) = 
+        let pu,metasenv,subst,proof,px,py = proof'''' in
+        let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+        let proof'''' = pu,metasenv,subst,proof,px,py in
+        let univ, params = params in
+        let use_context = bool params "use_context" true in 
+        let universe, (active,passive,bag), cache =
+         init_cache_and_tables ~use_library:false ~use_context
+           automation_cache univ (proof'''',newmeta)
+        in
+        match
+          Saturation.solve_narrowing bag (proof'''',newmeta) active passive 
+            1 (*0 infinity*)
+        with 
+          | None, active, passive, bag -> 
+              raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
+          | Some(subst',(pu,metasenv,_,proof,px, py),open_goals),active,
+            passive,bag ->
+              assert_subst_are_disjoint subst subst';
+              let subst = subst@subst' in
+              pu,metasenv,subst,proof,px,py
+   in
+
+(*
    let (_,m,_,_,_,_ as p),_ = 
       solve_rewrite ~params ~automation_cache (proof'''',newmeta)
    in
+*)
+
    let open_goals = 
      ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv' ~newmetasenv:m
    in
@@ -1573,6 +1532,32 @@ let equational_case
                 (active,passive,bag), cache, flags
       end
     else
+      begin
+        debug_print (lazy ("NARROWING DEL GOAL: " ^ 
+                         string_of_int goalno ^ " " ^ ppterm goalty ));
+        let goal_steps, saturation_steps, timeout =
+          1,0,flags.timeout 
+        in
+        match
+          Saturation.solve_narrowing bag status active passive goal_steps 
+        with 
+          | None, active, passive, bag -> 
+              [], (active,passive,bag), cache, flags
+          | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
+            passive,bag ->
+              assert_subst_are_disjoint subst subst';
+              let subst = subst@subst' in
+              let open_goals = 
+                order_new_goals metasenv subst open_goals ppterm 
+              in
+              let open_goals = 
+                List.map (fun (x,sort) -> x,depth-1,sort) open_goals 
+              in
+              incr candidate_no;
+              [(!candidate_no,proof),metasenv,subst,open_goals], 
+                (active,passive,bag), cache, flags
+      end
+(*
       begin
         let params = ([],["use_context","false"]) in
         let automation_cache = { 
@@ -1581,6 +1566,7 @@ let equational_case
         in
         try 
           let ((_,metasenv,subst,_,_,_),open_goals) =
+
             solve_rewrite ~params ~automation_cache
               (fake_proof, goalno)
           in
@@ -1607,6 +1593,7 @@ let equational_case
           res', (active,passive,bag), cache, flags 
 *)
       end
+*)
 ;;
 
 let sort_new_elems = 
@@ -1722,7 +1709,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 
@@ -1740,7 +1731,13 @@ let smart_applicative_case dbd
           try_candidate dbd goalty
             tables subst fake_proof goalno depth context cand
         with
-        | None, tables -> tables, elems
+        | None, tables ->
+            (* if normal application fails we try to be smart *)
+	    (match try_smart_candidate dbd goalty
+               tables subst fake_proof goalno depth context cand
+	     with
+	       | None, tables -> tables, elems
+               | Some x, tables -> tables, x::elems)
         | Some x, tables -> tables, x::elems)
       (tables,[]) candidates
   in