- destruct: core of subst tactic implemented,

[helm.git] / components / tactics / discriminationTactics.ml

diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml
index f31b52a2e329b9a5dccd0566db9202adb1f296e5..83f676ed33ee6acc471a526bf6fd9f9fbdd1fdaf 100644 (file)
--- a/components/tactics/discriminationTactics.ml
+++ b/components/tactics/discriminationTactics.ml
@@ -37,6 +37,7 @@ module CU = CicUniv
 module S = CicSubstitution
 module RT = ReductionTactics
 module PEH = ProofEngineHelpers
+module ET = EqualityTactics
 
 let debug = false
 let debug_print = 
@@ -242,7 +243,7 @@ let discriminate_tac ~term =
              ~continuation:
                (T.then_
                  ~start:
-                   (EqualityTactics.rewrite_simpl_tac
+                   (ET.rewrite_simpl_tac
                      ~direction:`RightToLeft
                      ~pattern:(PET.conclusion_pattern None)
                      term [])
@@ -418,8 +419,8 @@ let rec injection_tac ~map ~term ~i ~continuation =
         with
         | CTC.TypeCheckerFailure _ -> false
       in
-      if not go_on then
-        PET.apply_tactic T.id_tac status (* FG: ??????? *)
+      if not go_on then 
+        PET.apply_tactic (continuation ~map) status
       else
         let tac term = 
           let tac status =
@@ -441,11 +442,11 @@ let rec injection_tac ~map ~term ~i ~continuation =
                  RT.change_tac
                      ~pattern:(None, [], Some (PEH.pattern_of ~term:gty [new_t1']))
                      (fun _ m u -> changed,m,u);
-                 EqualityTactics.rewrite_simpl_tac
+                 ET.rewrite_simpl_tac
                      ~direction:`LeftToRight
                      ~pattern:(PET.conclusion_pattern None)
                      term [];
-                  EqualityTactics.reflexivity_tac   
+                  ET.reflexivity_tac   
               ] in
               PET.apply_tactic tac status
           in
@@ -455,7 +456,7 @@ let rec injection_tac ~map ~term ~i ~continuation =
        PET.apply_tactic   
           (T.thens ~start: (P.cut_tac cutted)
                    ~continuations:[
-                     (qnify_tac ~first_time:false ~term:(C.Rel 1) ~map:id 
+                     (destruct ~first_time:false ~term:(C.Rel 1) ~map:id 
                                 ~continuation:(after2 continuation succ map) 
                      );  
                      tac term] 
@@ -467,11 +468,37 @@ let rec injection_tac ~map ~term ~i ~continuation =
 (* ~term vive nel contesto della tattica una volta ~mappato
  * ~continuation riceve la mappa assoluta
  *)
-and qnify_tac ~first_time ~map ~term ~continuation =
+and subst_tac ~map ~term ~direction ~where ~continuation =
+   let fail_tactic = continuation ~map in
+   let subst_tac status =
+      let term = relocate_term map term in
+      let tactic = match where with
+         | None      -> 
+           let pattern = PET.conclusion_pattern None in
+            let tactic = ET.rewrite_tac ~direction ~pattern term [] in
+            T.then_ ~start:(T.try_tactic ~tactic)
+                   ~continuation:fail_tactic
+        | Some name ->   
+            let pattern = None, [name, PET.hole], None in
+            let start = ET.rewrite_tac ~direction ~pattern term [] in
+            let continuation =
+              destruct ~first_time:false ~term:(C.Rel 1) ~map:id 
+                       ~continuation:(after2 continuation succ map)
+           in
+           T.if_ ~start ~continuation ~fail:fail_tactic
+      in 
+      PET.apply_tactic tactic status
+   in
+   PET.mk_tactic subst_tac
+
+(* ~term vive nel contesto della tattica una volta ~mappato
+ * ~continuation riceve la mappa assoluta
+ *)
+and destruct ~first_time ~map ~term ~continuation =
  let are_convertible hd1 hd2 metasenv context = 
    fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph)
  in
- let qnify_tac status = 
+ let destruct status = 
   let (proof, goal) = status in
   let _,metasenv,_subst, _,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
@@ -527,7 +554,7 @@ and qnify_tac ~first_time ~map ~term ~continuation =
             | _ when not first_time -> continuation ~map
             | _ (* when first_time *) -> 
                T.then_ ~start:(simpl_in_term context term)
-                       ~continuation:(qnify_tac ~first_time:false ~term ~map ~continuation)
+                       ~continuation:(destruct ~first_time:false ~term ~map ~continuation)
            end
         | _ when not first_time -> continuation ~map
         | _ (* when first_time *) -> raise exn_nonproj
@@ -536,10 +563,10 @@ and qnify_tac ~first_time ~map ~term ~continuation =
   in  
     PET.apply_tactic tac status
  in 
-   PET.mk_tactic qnify_tac
+   PET.mk_tactic destruct
 
 (* destruct performs either injection or discriminate *)
 (* equivalent to Coq's "analyze equality"             *)
 let destruct_tac =
- qnify_tac
+ destruct
   ~first_time:true ~map:id ~continuation:(fun ~map -> T.id_tac)