X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FsubstTactic.ml;h=feff68f3fb8186f4ab4644ff2b07cce1b0e7accc;hb=b02253b371aadbbb37226a685b9bd8777a64d175;hp=1c01246485443179fe9eaac7eeb098f7272d2d8b;hpb=e436c170ce2b9154d3e090c2140e8a0172f4a016;p=helm.git

diff --git a/helm/software/components/tactics/substTactic.ml b/helm/software/components/tactics/substTactic.ml
index 1c0124648..feff68f3f 100644
--- a/helm/software/components/tactics/substTactic.ml
+++ b/helm/software/components/tactics/substTactic.ml
@@ -24,6 +24,7 @@
  *)
 
 module C    = Cic
+module DT   = DiscriminationTactics
 module DTI  = DoubleTypeInference
 module ET   = EqualityTactics
 module HEL  = HExtlib
@@ -31,85 +32,133 @@ module LO   = LibraryObjects
 module PEH  = ProofEngineHelpers
 module PESR = ProofEngineStructuralRules
 module PET  = ProofEngineTypes
+module RT   = ReductionTactics
 module S    = CicSubstitution
 module T    = Tacticals
 module TC   = CicTypeChecker
 
-(* FG: This should be replaced by T.try_tactic *)
-let try_tactic ~tactic =
-   let try_tactic status =
-      try PET.apply_tactic tactic status with
-         | PET.Fail _ -> PET.apply_tactic T.id_tac status
-   in
-   PET.mk_tactic try_tactic
-
-let rec lift_rewrite_tac ~context ~direction ~pattern equality =
+let lift_rewrite_tac ~context ~direction ~pattern equality =
    let lift_rewrite_tac status =
       let (proof, goal) = status in
-      let (_, metasenv, _, _, _) = proof in
+      let (_, metasenv, _subst, _, _, _) = proof in
       let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
       let n = List.length new_context - List.length context in
-      let equality = if n > 0 then S.lift n equality else equality in
+      let equality = S.lift n equality in
       PET.apply_tactic (ET.rewrite_tac ~direction ~pattern equality []) status
    in
    PET.mk_tactic lift_rewrite_tac
 
-
+let lift_destruct_tac ~context ~what =
+   let lift_destruct_tac status =
+      let (proof, goal) = status in
+      let (_, metasenv, _subst, _, _, _) = proof in
+      let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
+      let n = List.length new_context - List.length context in
+      let what = S.lift n what in
+      PET.apply_tactic (DT.destruct_tac ~term:what) status
+   in
+   PET.mk_tactic lift_destruct_tac
+      
 let msg0 = lazy "Subst: not found in context"
-let msg1 = lazy "Subst: not a simple equality"
+let msg1 = lazy "Subst: not an erasable equation"
 let msg2 = lazy "Subst: recursive equation" 
+let msg3 = lazy "Subst: no progress" 
 
-let subst_tac ~hyp =
+let rec subst_tac ~try_tactic ~hyp =
    let hole = C.Implicit (Some `Hole) in
+   let meta = C.Implicit None in
+   let rec ind = function
+      | C.MutInd _       -> true
+      | C.Appl (t :: tl) -> ind t
+      | _                -> false
+   in
+   let rec constr = function
+      | C.MutConstruct _ -> true
+      | C.Appl (t :: tl) -> constr t
+      | _                -> false
+   in
    let subst_tac status =
       let (proof, goal) = status in
-      let (_, metasenv, _, _, _) = proof in
+      let (_, metasenv, _subst, _, _, _) = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let what = match PEH.get_rel context hyp with
          | Some t -> t
 	 | None   -> raise (PET.Fail msg0)
       in
       let ty, _ = TC.type_of_aux' metasenv context what CicUniv.empty_ugraph in
-      let direction, i, t = match ty with
+      let subst_g direction i t =
+         let rewrite pattern =
+            let tactic = lift_rewrite_tac ~context ~direction ~pattern what in
+	    try_tactic ~tactic
+         in
+         let var = match PEH.get_name context i with
+            | Some name -> name
+	    | None      -> raise (PET.Fail msg0)	
+         in
+         if DTI.does_not_occur i t then () else raise (PET.Fail msg2);
+         let map self = function
+            | Some (C.Name s, _) when s <> self -> 
+               Some (rewrite (None, [(s, hole)], None))
+            | _                                 -> None
+         in
+         let rew_hips = HEL.list_rev_map_filter (map hyp) context in
+         let rew_concl = rewrite (None, [], Some hole) in
+         let clear = PESR.clear ~hyps:[hyp; var] in
+         List.rev_append (rew_concl :: rew_hips) [clear]
+      in
+      let destruct_g () =
+         [lift_destruct_tac ~context ~what; PESR.clear ~hyps:[hyp]]
+      in
+      let whd_g () =
+         let whd_pattern = C.Appl [meta; hole; hole; hole] in
+	 let pattern = None, [hyp, whd_pattern], None in
+	 [RT.whd_tac ~pattern; subst_tac ~try_tactic ~hyp]
+      in
+      let tactics = match ty with
          | (C.Appl [(C.MutInd (uri, 0, [])); _; C.Rel i; t]) 
-	    when LO.is_eq_URI uri -> `LeftToRight, i, t
+	    when LO.is_eq_URI uri -> subst_g `LeftToRight i t
          | (C.Appl [(C.MutInd (uri, 0, [])); _; t; C.Rel i]) 
-	    when LO.is_eq_URI uri -> `RightToLeft, i, t
+	    when LO.is_eq_URI uri -> subst_g `RightToLeft i t
+	 | (C.Appl [(C.MutInd (uri, 0, [])); t; t1; t2]) 
+	    when LO.is_eq_URI uri && ind t && constr t1 && constr t2 -> destruct_g ()
+	 | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2])
+	    when LO.is_eq_URI uri -> whd_g () 	 
 	 | _ -> raise (PET.Fail msg1)
-      in    
-      let rewrite pattern =
-         let tactic = lift_rewrite_tac ~context ~direction ~pattern what in
-	 try_tactic ~tactic
-      in
-      let var = match PEH.get_name context i with
-         | Some name -> name
-	 | None      -> raise (PET.Fail msg0)	
       in
-      if DTI.does_not_occur i t then () else raise (PET.Fail msg2);
-      let map self = function
-         | Some (C.Name s, _) when s <> self -> 
-            Some (rewrite (None, [(s, hole)], None))
-         | _                                 -> None
-      in
-      let rew_hips = HEL.list_rev_map_filter (map hyp) context in
-      let rew_concl = rewrite (None, [], Some hole) in
-      let clear = PESR.clear ~hyps:[hyp; var] in
-      let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in
       PET.apply_tactic (T.seq ~tactics) status
    in
    PET.mk_tactic subst_tac
 
 let subst_tac =
-   let subst hyp = try_tactic ~tactic:(subst_tac hyp) in
-   let map = function
-      | Some (C.Name s, _) -> Some (subst s)
-      | _                  -> None
-   in
    let subst_tac status =
+      let progress = ref false in
+      let try_tactic ~tactic =
+         let try_tactic status =
+            try 
+	       let result = PET.apply_tactic tactic status in
+	       progress := true; result
+	    with
+               | PET.Fail _ -> PET.apply_tactic T.id_tac status
+         in
+         PET.mk_tactic try_tactic
+      in
+      let subst hyp = try_tactic ~tactic:(subst_tac ~try_tactic ~hyp) in
+      let map = function
+         | Some (C.Name s, _) -> Some (subst s)
+         | _                  -> None
+      in
       let (proof, goal) = status in
-      let (_, metasenv, _, _, _) = proof in
+      let (_, metasenv, _subst, _, _, _) = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let tactics = HEL.list_rev_map_filter map context in
-      PET.apply_tactic (T.seq ~tactics) status
+      let result = PET.apply_tactic (T.seq ~tactics) status in
+      if !progress then result else raise (PET.Fail msg3)
    in
    PET.mk_tactic subst_tac
+
+   let try_tac tactic = T.try_tactic ~tactic 
+   let then_tac start continuation = T.then_ ~start ~continuation 
+
+let subst_tac = 
+   let tactic = T.repeat_tactic ~tactic:subst_tac in
+   T.try_tactic ~tactic