X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=9f54c6cecc15764d460d307281f3fcf262749211;hb=e8f64678cc425f19336ff4f905f9b2f00acd6627;hp=9db6ed1c9094d3816c374592d401d5ba35fcdd7f;hpb=a060ed37101ce0e97bc26af8d49ce2491471c60c;p=helm.git

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 9db6ed1c9..9f54c6cec 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -339,7 +339,14 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
     if paramodulation_ok then (
       debug_print (lazy "USO PARAMODULATION...");
 (*       try *)
-      Saturation.saturate dbd ~depth ~width ~full (proof, goal)
+      try
+        let rc = Saturation.saturate dbd ~depth ~width ~full (proof, goal) in
+        prerr_endline (Saturation.get_stats ());
+        rc
+      with exn ->
+        prerr_endline (Saturation.get_stats ());
+        raise exn
+      
 (*       with ProofEngineTypes.Fail _ -> *)
 (*         normal_auto () *)
     ) else
@@ -347,3 +354,115 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
   in
   ProofEngineTypes.mk_tactic (auto_tac dbd)
 ;;
+
+(********************** applyS *******************)
+
+let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' ty termty goal_arity =
+ let (consthead,newmetasenv,arguments,_) =
+   ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
+ let term'' = match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in
+  let proof',metasenv =
+   let (puri,metasenv,pbo,pty) = proof in
+    (puri,newmetasenv,pbo,pty),metasenv
+  in
+   let proof'',goals =
+    match LibraryObjects.eq_URI () with
+    | Some uri -> 
+	    ProofEngineTypes.apply_tactic
+	     (Tacticals.then_
+	       ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*))
+	       ~continuation:
+		 (PrimitiveTactics.cut_tac
+		   (CicSubstitution.lift 1
+		    (Cic.Appl
+		     [Cic.MutInd (uri,0,[]);
+		      Cic.Sort Cic.Prop;
+		      consthead;
+		      ty])))) (proof',goal)
+   | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
+    in
+     match goals with
+        [g1;g2] ->
+	  let proof'',goals =
+	   ProofEngineTypes.apply_tactic
+	    (auto_tac ~paramodulation:"qualsiasi" ~dbd ()) (proof'',g2)
+	  in
+	   let proof'',goals =
+	    ProofEngineTypes.apply_tactic
+	     (Tacticals.then_
+	      ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft
+	        ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1))
+              ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
+	     ) (proof'',g1)
+	   in
+            proof'',
+	     (*CSC: Brrrr.... *)
+	     ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
+	      ~newmetasenv:(let _,m,_,_ = proof'' in m)
+      | _ -> assert false
+
+let rec count_prods context ty =
+ match CicReduction.whd context ty with
+    Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
+  | _ -> 0
+
+let applyS_tac ~dbd ~term (proof, goal) =
+ let module T = CicTypeChecker in
+ let module R = CicReduction in
+ let module C = Cic in
+  let (_,metasenv,_,_) = proof in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
+   let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
+    match term with
+       C.Var (uri,exp_named_subst) ->
+        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+          exp_named_subst
+        in
+         exp_named_subst_diff,newmeta',newmetasenvfragment,
+          C.Var (uri,exp_named_subst')
+     | C.Const (uri,exp_named_subst) ->
+        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+          exp_named_subst
+        in
+         exp_named_subst_diff,newmeta',newmetasenvfragment,
+          C.Const (uri,exp_named_subst')
+     | C.MutInd (uri,tyno,exp_named_subst) ->
+        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+          exp_named_subst
+        in
+         exp_named_subst_diff,newmeta',newmetasenvfragment,
+          C.MutInd (uri,tyno,exp_named_subst')
+     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+        let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+         PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+          exp_named_subst
+        in
+         exp_named_subst_diff,newmeta',newmetasenvfragment,
+          C.MutConstruct (uri,tyno,consno,exp_named_subst')
+     | _ -> [],newmeta,[],term
+   in
+   let metasenv' = metasenv@newmetasenvfragment in
+   let termty,_ = 
+     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+   in
+   let termty =
+     CicSubstitution.subst_vars exp_named_subst_diff termty in
+   let goal_arity = count_prods context ty in
+   let res =
+    new_metasenv_and_unify_and_t dbd proof goal
+     newmeta' metasenv' context term' ty termty goal_arity
+   in
+    res
+
+let applyS_tac ~dbd ~term =
+ ProofEngineTypes.mk_tactic
+  (fun status ->
+    try applyS_tac ~dbd ~term status
+    with 
+    | CicUnification.UnificationFailure msg
+    | CicTypeChecker.TypeCheckerFailure msg ->
+        raise (ProofEngineTypes.Fail msg))