- bug fix in destruct

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

diff --git a/components/tactics/destructTactic.ml b/components/tactics/destructTactic.ml
index bbfee8041ac0f827f12ca84971d0010258286c79..2ea9e047c79458d13c1975055c83161f6d7ffdef 100644 (file)
--- a/components/tactics/destructTactic.ml
+++ b/components/tactics/destructTactic.ml
@@ -45,54 +45,6 @@ let debug = true
 let debug_print = 
   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
 
-(* funzione generale di rilocazione dei riferimenti locali *)
-
-let relocate_term map t =
-   let rec map_xnss k xnss =
-      let imap (uri, t) = uri, map_term k t in
-      List.map imap xnss
-   and map_mss k mss =
-      let imap = function
-         | None   -> None
-         | Some t -> Some (map_term k t)
-      in
-      List.map imap mss
-   and map_fs len k fs = 
-      let imap (name, i, ty, bo) = name, i, map_term k ty, map_term (k + len) bo in
-      List.map imap fs
-   and map_cfs len k cfs = 
-      let imap (name, ty, bo) = name, map_term k ty, map_term (k + len) bo in
-      List.map imap cfs
-   and map_term k = function
-      | C.Rel m -> if m < k then C.Rel m else C.Rel (map (m - k))
-      | C.Sort _ as t -> t
-      | C.Implicit _ as t -> t
-      | C.Var (uri, xnss) -> C.Var (uri, map_xnss k xnss)
-      | C.Const (uri, xnss) -> C.Const (uri, map_xnss k xnss)
-      | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, map_xnss k xnss)
-      | C.MutConstruct (uri, tyno, consno, xnss) ->
-         C.MutConstruct (uri, tyno, consno, map_xnss k xnss)
-      | C.Meta (i, mss) -> C.Meta(i, map_mss k mss)
-      | C.Cast (te, ty) -> C.Cast (map_term k te, map_term k ty)
-      | C.Appl ts -> C.Appl (List.map (map_term k) ts)
-      | C.MutCase (sp, i, outty, t, pl) ->
-         C.MutCase (sp, i, map_term k outty, map_term k t, List.map (map_term k) pl)    
-      | C.Prod (n, s, t) -> C.Prod (n, map_term k s, map_term (succ k) t)
-      | C.Lambda (n, s, t) -> C.Lambda (n, map_term k s, map_term (succ k) t)
-      | C.LetIn (n, s, t) -> C.LetIn (n, map_term k s, map_term (succ k) t)
-      | C.Fix (i, fs) -> C.Fix (i, map_fs (List.length fs) k fs)
-      | C.CoFix (i, cfs) -> C.CoFix (i, map_cfs (List.length cfs) k cfs)
-   in
-   map_term 0 t
-
-let id n = n
-
-let after continuation aftermap beforemap = 
-   continuation ~map:(fun n -> aftermap (beforemap n))
-
-let after2 continuation aftermap beforemap ~map = 
-   continuation ~map:(fun n -> map (aftermap (beforemap n)))
-
 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
 diversi *)
 
@@ -322,7 +274,7 @@ let rec recur_on_child_tac name =
       let rec search_name i = function
          | []                                      -> T.id_tac
          | Some (Cic.Name n, _) :: _ when n = name -> 
-             destruct ~first_time:false ~term:(Cic.Rel i)
+             destruct ~first_time:false (Cic.Rel i)
         | _ :: tl -> search_name (succ i) tl
       in
       PET.apply_tactic (search_name 1 context) status  
@@ -532,10 +484,7 @@ and subst_tac ~lterm ~direction ~where ~continuation =
    in
    PET.mk_tactic subst_tac
 
-(* ~term vive nel contesto della tattica una volta ~mappato
- * ~continuation riceve la mappa assoluta
- *)
-and destruct ~first_time ~term =
+and destruct ?(simplified = false) ~first_time term =
  let are_convertible hd1 hd2 metasenv context = 
    fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
  in
@@ -625,13 +574,17 @@ and destruct ~first_time ~term =
            | _, C.Rel i2 when DTI.does_not_occur i2 t1 ->
               mk_subst_chain `RightToLeft i2 t1 t2
 (* else part *)
-           | _ when not first_time -> T.id_tac
-            | _ (* when first_time *) -> 
+           | _ when first_time && simplified -> raise exn_nothingtodo
+           | _ when simplified (* && not first time *) -> T.id_tac
+            | _ (* when not simplified *) -> 
                T.then_ ~start:(simpl_in_term context term)
-                       ~continuation:(destruct ~first_time:false ~term)
+                       ~continuation:(destruct ~simplified:true ~first_time term)
            end
-     | _ when not first_time -> T.id_tac
-     | _ (* when first_time *) -> raise exn_nothingtodo
+     | _ when first_time && simplified -> raise exn_nothingtodo
+     | _ when simplified (* && not first time *) -> T.id_tac
+     | _ (* when not simplified *) -> 
+        T.then_ ~start:(simpl_in_term context term)
+                ~continuation:(destruct ~simplified:true ~first_time term)
   in  
     PET.apply_tactic tac status
  in 
@@ -644,7 +597,7 @@ let lazy_destruct_tac ~first_time ~lterm =
       let _,context,_ = CicUtil.lookup_meta goal metasenv in
       let term, _, _ = lterm context metasenv CU.empty_ugraph in
       let tactic = 
-         if exists context term then destruct ~first_time ~term else T.id_tac
+         if exists context term then destruct ~first_time term else T.id_tac
       in
       PET.apply_tactic tactic status
    in
@@ -653,7 +606,7 @@ let lazy_destruct_tac ~first_time ~lterm =
 (* destruct performs either injection or discriminate *)
 (* equivalent to Coq's "analyze equality"             *)
 let destruct_tac = function
-   | Some term -> destruct ~first_time:true ~term
+   | Some term -> destruct ~first_time:true term
    | None      ->
       let destruct_all status =
          let (proof, goal) = status in