X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fauto.ml;h=b9ce25174edefc00c876253864f9172b52933507;hb=b0a6c05decc9f0e731f70cfc5ae5350ae4046b79;hp=01749a59cbd66888c9abff969da7a6c28202b9d8;hpb=b8f54b66890a55cfc255fa1df3e40fe60b78ee15;p=helm.git

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 01749a59c..b9ce25174 100644
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -66,11 +66,11 @@ let naif_closure ?(prefix_name="xxx_") t metasenv context =
 let lambda_close ?prefix_name t menv ctx =
   let t = naif_closure ?prefix_name t menv ctx in
     List.fold_left
-      (fun t -> function 
-        | None -> CicSubstitution.subst (Cic.Implicit None) t (* delift *)
-        | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t)
-        | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t))
-      t ctx
+      (fun (t,i) -> function 
+        | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *)
+        | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1
+        | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t),i+1)
+      (t,List.length menv) ctx
 ;;
   
 (* functions for retrieving theorems *)
@@ -147,7 +147,9 @@ let is_unit_equation context metasenv oldnewmeta term =
     args
   in
     if propositional_args = [] then 
-      let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
+      let newmetas = 
+        List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv 
+      in
         Some (args,metasenv,newmetas,head,newmeta)
     else None
 ;;
@@ -163,19 +165,21 @@ let get_candidates universe cache t =
   candidates
 ;;
 
-let only signature context t =
+let only signature context metasenv t =
   try
-    let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
+    let ty,_ = 
+      CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph 
+    in
     let consts = MetadataConstraints.constants_of ty in
     let b = MetadataConstraints.UriManagerSet.subset consts signature in
     if b then b 
     else
-      try
-        let ty' = unfold context ty in
-        let consts' = MetadataConstraints.constants_of ty' in
-        MetadataConstraints.UriManagerSet.subset consts' signature 
-      with _-> false
-  with _ -> false
+      let ty' = unfold context ty in
+      let consts' = MetadataConstraints.constants_of ty' in
+      MetadataConstraints.UriManagerSet.subset consts' signature 
+  with 
+  | CicTypeChecker.TypeCheckerFailure _ -> assert false
+  | ProofEngineTypes.Fail _ -> false (* unfold may fail *)
 ;;
 
 let not_default_eq_term t =
@@ -184,7 +188,7 @@ let not_default_eq_term t =
       not (LibraryObjects.in_eq_URIs uri)
   with Invalid_argument _ -> true
 
-let retrieve_equations signature universe cache context=
+let retrieve_equations dont_filter signature universe cache context metasenv =
   match LibraryObjects.eq_URI() with
     | None -> [] 
     | Some eq_uri -> 
@@ -192,11 +196,10 @@ let retrieve_equations signature universe cache context=
         let fake= Cic.Meta(-1,[]) in
         let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
         let candidates = get_candidates universe cache fake_eq in
-    (* defaults eq uris are built-in in auto *)
-        let candidates = List.filter not_default_eq_term candidates in
-        let candidates = List.filter (only signature context) candidates in
-        List.iter (fun t -> debug_print (lazy (CicPp.ppterm t))) candidates;
-        candidates
+        if dont_filter then candidates
+        else 
+          let candidates = List.filter not_default_eq_term candidates in
+          List.filter (only signature context metasenv) candidates 
 
 let build_equality bag head args proof newmetas maxmeta = 
   match head with
@@ -218,6 +221,14 @@ let build_equality bag head args proof newmetas maxmeta =
 let partition_unit_equalities context metasenv newmeta bag equations =
   List.fold_left
     (fun (units,other,maxmeta)(t,ty) ->
+       if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then
+         let _ = 
+           HLog.warn 
+           ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context
+             ^ " since it is not meta closed")
+         in
+         units,(t,ty)::other,maxmeta
+       else
        match is_unit_equation context metasenv maxmeta ty with
          | Some (args,metasenv,newmetas,head,newmeta') ->
              let maxmeta,equality =
@@ -232,50 +243,58 @@ let empty_tables =
    Saturation.make_passive [],
    Equality.mk_equality_bag)
 
-let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
+let init_cache_and_tables 
+  ?dbd use_library paramod use_context dont_filter universe (proof, goal) 
+=
   (* the local cache in initially empty  *)
   let cache = AutoCache.cache_empty in
   let _, metasenv, _subst,_, _, _ = proof in
   let signature = MetadataQuery.signature_of metasenv goal in
   let newmeta = CicMkImplicit.new_meta metasenv [] in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let ct = find_context_theorems context metasenv in
+  let ct = if use_context then find_context_theorems context metasenv else [] in
   debug_print 
     (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct))));
   let lt = 
-    if use_library then 
-       find_library_theorems dbd metasenv goal 
-    else [] in
+    match use_library, dbd with
+    | true, Some dbd -> find_library_theorems dbd metasenv goal 
+    | _ -> []
+  in
   debug_print 
     (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
   let cache = cache_add_list cache context (ct@lt) in  
   let equations = 
-    retrieve_equations signature universe cache context in
+    retrieve_equations dont_filter 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.empty_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 _ -> None) (* catturare l'eccezione giusta di unfold *)
-      equations in
+           CicTypeChecker.type_of_aux' 
+             metasenv context t CicUniv.empty_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 _ -> None) (* catturare l'eccezione giusta di unfold *)
+      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
-  (* let env = (metasenv, context, CicUniv.empty_ugraph) in 
-    let equalities = 
-    let eq_uri = 
-    match LibraryObjects.eq_URI() with
-      | None ->assert false
-      | Some eq_uri -> eq_uri in
-    Saturation.simplify_equalities bag eq_uri env units in *)
+    partition_unit_equalities context metasenv newmeta bag eqs_and_types 
+  in
+  (* SIMPLIFICATION STEP 
+  let equalities = 
+    let env = (metasenv, context, CicUniv.empty_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
@@ -380,7 +399,9 @@ let close_more tables maxmeta context status auto universe cache =
   let proof, goalno = status in
   let _, metasenv,_subst,_,_, _ = proof in  
   let signature = MetadataQuery.signature_of metasenv goalno in
-  let equations = retrieve_equations signature universe cache context in
+  let equations = 
+    retrieve_equations false signature universe cache context metasenv 
+  in
   let eqs_and_types =
     HExtlib.filter_map 
       (fun t -> 
@@ -509,7 +530,7 @@ let new_metasenv_and_unify_and_t
  in
  match 
    let (active, passive,bag), cache, maxmeta =
-     init_cache_and_tables dbd flags.use_library true universe
+     init_cache_and_tables ~dbd flags.use_library true true false universe
      (proof'''',newmeta)
    in
      Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive 
@@ -831,9 +852,13 @@ let pause b = in_pause := b;;
 let cond = Condition.create ();;
 let mutex = Mutex.create ();;
 let hint = ref None;;
+let prune_hint = ref [];;
 
 let step _ = Condition.signal cond;;
 let give_hint n = hint := Some n;;
+let give_prune_hint hint =
+  prune_hint := hint :: !prune_hint
+;;
 
 let check_pause _ =
   if !in_pause then
@@ -1081,7 +1106,7 @@ let equational_case
         assert (maxmeta >= maxm);
         let res' =
           List.map 
-            (fun subst',(_,metasenv,_subst,proof,_, _),open_goals ->
+            (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
                assert_subst_are_disjoint subst subst';
                let subst = subst@subst' in
                let open_goals = 
@@ -1119,8 +1144,8 @@ let try_candidate
 ;;
 
 let sort_new_elems = 
- List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2)
-(*  List.sort (fun (_,_,_,l2) (_,_,_,l1) -> List.length l1 - List.length l2)  *)
+ List.sort (fun (_,_,_,l1) (_,_,_,l2) -> 
+  List.length (prop_only l1) - List.length (prop_only l2))
 ;;
 
 let applicative_case 
@@ -1184,6 +1209,25 @@ let remove_s_from_fl (id,_,_) (fl : fail list) =
   in 
     aux fl
 ;;
+
+let prunable_for_size flags s m todo =
+  let rec aux b = function
+    | (S _)::tl -> aux b tl
+    | (D (_,_,T))::tl -> aux b tl
+    | (D g)::tl -> 
+	(match calculate_goal_ty g s m with
+          | None -> aux b tl
+          | Some (canonical_ctx, gty) -> 
+            let gsize, _ = 
+              Utils.weight_of_term 
+		~consider_metas:false ~count_metas_occurrences:true gty in
+	    let newb = b || gsize > flags.maxgoalsizefactor in
+	    aux newb tl)
+    | [] -> b
+  in
+    aux false todo
+
+(*
 let prunable ty todo =
   let rec aux b = function
     | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
@@ -1193,12 +1237,63 @@ let prunable ty todo =
   in
     aux false todo
 ;;
+*)
 
+let prunable menv subst ty todo =
+  let rec aux = function
+    | (S(_,k,_,_))::tl ->
+	 (match Equality.meta_convertibility_subst k ty menv with
+	  | None -> aux tl
+	  | Some variant -> 
+	       no_progress variant tl (* || aux tl*))
+    | (D (_,_,T))::tl -> aux tl
+    | _ -> false
+  and no_progress variant = function
+    | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
+    | D ((n,_,P) as g)::tl -> 
+	(match calculate_goal_ty g subst menv with
+           | None -> no_progress variant tl
+           | Some (_, gty) -> 
+	       (match calculate_goal_ty g variant menv with
+		  | None -> assert false
+		  | Some (_, gty') ->
+		      if gty = gty' then
+			 no_progress variant tl
+		      else false))
+    | _::tl -> no_progress variant tl
+  in
+    aux todo
+
+;;
+let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
+  let s = 
+    HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo 
+  in
+  List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
+;;
+let filter_prune_hint l =
+  let prune = !prune_hint in
+  prune_hint := []; (* possible race... *)
+  if prune = [] then l
+  else List.filter (condition_for_prune_hint prune) l
+;;
 let auto_main tables maxm context flags universe cache elems =
   auto_context := context;
   let rec aux tables maxm flags cache (elems : status) =
 (*     pp_status context elems; *)
+(* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
+    auto_status := elems;
+    check_pause ();
+*)
+    let elems = filter_prune_hint elems in
     match elems with
+    | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
+        (match !hint with
+        | Some i when condition_for_hint i todo ->
+            aux tables maxm flags cache orlist
+        | _ ->
+          hint := None;
+          aux tables maxm flags cache elems)
     | [] ->
         (* complete failure *)
         Gaveup (tables, cache, maxm)
@@ -1244,12 +1339,15 @@ let auto_main tables maxm context flags universe cache elems =
             aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist)
         | Some (canonical_ctx, gty) -> 
             let gsize, _ = 
-              Utils.weight_of_term ~count_metas_occurrences:true gty 
+              Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty 
             in
             if gsize > flags.maxgoalsizefactor then
-              (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int size));
+	      (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
                aux tables maxm flags cache orlist)
-            else
+            else if prunable_for_size flags s m todo then
+		(debug_print (lazy ("POTO at depth: "^(string_of_int depth)));
+	         aux tables maxm flags cache orlist)
+	    else
             (* still to be proved *)
             (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
             match cache_examine cache gty with
@@ -1269,12 +1367,8 @@ let auto_main tables maxm context flags universe cache elems =
                 aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
             | Notfound 
             | Failed_in _ when depth > 0 -> 
-                (match !hint with
-                | Some i when condition_for_hint i todo ->
-                    aux tables maxm flags cache orlist
-                | _ -> hint := None;
-                    (* more depth or is the first time we see the goal *)
-                    if prunable gty todo then
+                ( (* more depth or is the first time we see the goal *)
+                    if prunable m s gty todo then
                       (debug_print (lazy(
                          "FAIL: LOOP: one father is equal"));
                        aux tables maxm flags cache orlist)
@@ -1606,8 +1700,8 @@ let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) =
       (* just for testing *)
       let use_library = flags.use_library in
       let tables,cache,newmeta =
-        init_cache_and_tables dbd use_library flags.use_only_paramod 
-          universe (proof, goal) in
+        init_cache_and_tables ~dbd use_library flags.use_only_paramod true 
+          false universe (proof, goal) in
       let tables,cache,newmeta =
         if flags.close_more then
           close_more 
@@ -1622,8 +1716,8 @@ let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) =
       in
       match auto_main tables newmeta context flags universe cache [elem] with
         | Proved (metasenv,subst,_, tables,cache,_) -> 
-            prerr_endline 
-              ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
+            (*prerr_endline 
+              ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));*)
             let proof,metasenv =
             ProofEngineHelpers.subst_meta_and_metasenv_in_proof
               proof goal subst metasenv
@@ -1649,15 +1743,57 @@ let eq_of_goal = function
   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
 ;;
 
+(* performs steps of rewrite with the universe, obtaining if possible 
+ * a trivial goal *)
+let solve_rewrite_tac ~universe ?(steps=1) (proof,goal as status)= 
+  let _,metasenv,_subst,_,_,_ = proof in
+  let _,context,ty = CicUtil.lookup_meta goal metasenv in
+  let eq_uri = eq_of_goal ty in
+  let (active,passive,bag), cache, maxm =
+     (* we take the whole universe (no signature filtering) *)
+     init_cache_and_tables false true false true universe (proof,goal) 
+  in
+  let initgoal = [], metasenv, ty in
+  let table = 
+    let equalities = (Saturation.list_of_passive passive) in
+    (* we demodulate using both actives passives *)
+    List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
+  in
+  let env = metasenv,context,CicUniv.empty_ugraph in
+  match Indexing.solve_demodulating bag env table initgoal steps with 
+  | Some (proof, metasenv, newty) ->
+      let refl = 
+        match newty with
+        | Cic.Appl[Cic.MutInd _;eq_ty;left;_] ->
+            Equality.Exact (Equality.refl_proof eq_uri eq_ty left)
+        | _ -> assert false
+      in
+      let proofterm,_ = 
+        Equality.build_goal_proof 
+          bag eq_uri proof refl newty [] context metasenv
+      in
+      ProofEngineTypes.apply_tactic
+        (PrimitiveTactics.apply_tac ~term:proofterm) status
+  | None -> 
+      raise 
+        (ProofEngineTypes.Fail (lazy 
+          ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
+;;
+let solve_rewrite_tac ~universe ?steps () =
+  ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ?steps)
+;;
+
 (* DEMODULATE *)
 let demodulate_tac ~dbd ~universe (proof,goal)= 
   let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-  let initgoal = [], [], ty in
+  let initgoal = [], metasenv, ty in
   let eq_uri = eq_of_goal ty in
   let (active,passive,bag), cache, maxm =
-     init_cache_and_tables dbd false true universe (proof,goal) in
+     init_cache_and_tables 
+       ~dbd false true true false universe (proof,goal) 
+  in
   let equalities = (Saturation.list_of_passive passive) in
   (* we demodulate using both actives passives *)
   let table = 
@@ -1698,3 +1834,4 @@ let demodulate_tac ~dbd ~universe =
 let pp_proofterm = Equality.pp_proofterm;;
 
 let revision = "$Revision$";;
+let size_and_depth context metasenv t = 100, 100