- destruct: core of subst tactic implemented,

  must be linked to destruct in order to work
- "if" tactical implemented (used by core subst tactic) - to be tested
- added freqently used constant hole = Cic.Implicit (Some 'Hole)

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index f31b52a2e329b9a5dccd0566db9202adb1f296e5..83f676ed33ee6acc471a526bf6fd9f9fbdd1fdaf 100644 (file)
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/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)

diff --git a/helm/software/components/tactics/proofEngineTypes.ml b/helm/software/components/tactics/proofEngineTypes.ml
index abe460775b935a5271a6cda8a5deb8e1ac5a879f..93436e799586b899ecd4ffe6a7ebb098e8e3f5b0 100644 (file)
--- a/helm/software/components/tactics/proofEngineTypes.ml
+++ b/helm/software/components/tactics/proofEngineTypes.ml
@@ -76,13 +76,15 @@ type ('term, 'lazy_term) pattern =
 
 type lazy_pattern = (Cic.term, Cic.lazy_term) pattern
 
+let hole = Cic.Implicit (Some `Hole)
+
 let conclusion_pattern t =
   let t' = 
     match t with
     | None -> None
     | Some t -> Some (const_lazy_term t)
   in
-  t',[],Some (Cic.Implicit (Some `Hole))
+  t',[], Some hole
 
   (** tactic failure *)
 exception Fail of string Lazy.t

diff --git a/helm/software/components/tactics/proofEngineTypes.mli b/helm/software/components/tactics/proofEngineTypes.mli
index 6edcfeccc053a7559b715604e9a08f8c421a66f9..7c7b8330ee13d7cf075c6247dd4a293dc9520d16 100644 (file)
--- a/helm/software/components/tactics/proofEngineTypes.mli
+++ b/helm/software/components/tactics/proofEngineTypes.mli
@@ -75,3 +75,4 @@ type mk_fresh_name_type =
 
 val goals_of_proof: proof -> goal list
 
+val hole: Cic.term

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index 06f96a573c28f367c244a649080c4fc136c7e981..cf5f22206d75faa5463932311a3c3b13625f2544 100644 (file)
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -180,6 +180,28 @@ let seq ~tactics =
         (HExtlib.list_concat ~sep:[ C.Semicolon ]
           (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
 
+let if_ ~start ~continuation ~fail =
+  S.mk_tactic
+    (fun istatus -> 
+      let xostatus = 
+         try 
+           let res = C.eval (C.Tactical (C.Tactic start)) istatus in
+           info (lazy ("Tacticals.if_: succedeed!!!"));
+           Some res
+        with PET.Fail _ -> None
+      in
+      match xostatus with
+         | Some ostatus ->
+            let opened,closed = S.goals ostatus in
+            begin match opened with
+                | [] -> ostatus
+                | _ ->
+                   fold_eval (S.focus ~-1 ostatus)
+                      [ C.Semicolon; C.Tactical (C.Tactic continuation) ]
+            end
+        | None -> C.eval (C.Tactical (C.Tactic fail)) istatus
+    )
+
 (* Tacticals that cannot be implemented on top of tynycals *)
 
 let first ~tactics =

diff --git a/helm/software/components/tactics/tacticals.mli b/helm/software/components/tactics/tacticals.mli
index cdc3bac77f3557b4bc2b65ccb517892be45290e6..800991bb560fa9abd4da4e79399192333352694b 100644 (file)
--- a/helm/software/components/tactics/tacticals.mli
+++ b/helm/software/components/tactics/tacticals.mli
@@ -31,6 +31,7 @@ val fail_tac: tactic
 val first: tactics: tactic list -> tactic
 val thens: start: tactic -> continuations: tactic list -> tactic
 val then_: start: tactic -> continuation: tactic -> tactic
+val if_: start: tactic -> continuation: tactic -> fail: tactic -> tactic
 val seq: tactics: tactic list -> tactic (** "folding" of then_ *)
 val repeat_tactic: tactic: tactic -> tactic
 val do_tactic: n: int -> tactic: tactic -> tactic