added applyS

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index a9505d73919f1d33a929599b5741c59a930f4efb..9f54c6cecc15764d460d307281f3fcf262749211 100644 (file)
--- a/components/tactics/autoTactic.ml
+++ b/components/tactics/autoTactic.ml
@@ -354,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))

diff --git a/components/tactics/autoTactic.mli b/components/tactics/autoTactic.mli
index fe72629f02ba338155cfee7eadea102410177954..2070116488d577308330a210a0c860f0fd53bfe9 100644 (file)
--- a/components/tactics/autoTactic.mli
+++ b/components/tactics/autoTactic.mli
@@ -29,3 +29,4 @@ val auto_tac:
   dbd:HMysql.dbd -> unit ->
   ProofEngineTypes.tactic
 
+val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic

diff --git a/components/tactics/tactics.ml b/components/tactics/tactics.ml
index 4d52725891e04f5e2e24ca2d4ec8ae367366fe40..327256b3d2b161a9465a595aeb1a7efdaf32dd87 100644 (file)
--- a/components/tactics/tactics.ml
+++ b/components/tactics/tactics.ml
@@ -27,6 +27,7 @@
 
 let absurd = NegationTactics.absurd_tac
 let apply = PrimitiveTactics.apply_tac
+let applyS = AutoTactic.applyS_tac
 let assumption = VariousTactics.assumption_tac
 let auto = AutoTactic.auto_tac
 let change = ReductionTactics.change_tac

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index 67127e640e10e50c33928aa198ec4d6a570b7efd..06b62911c95492ad6c14468ee9986459afa38d40 100644 (file)
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -1,6 +1,7 @@
 (* GENERATED FILE, DO NOT EDIT. STAMP:Wed Apr 12 11:46:23 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
+val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic
 val assumption : ProofEngineTypes.tactic
 val auto :
   ?depth:int ->