elim tactic: it needs two arguments, a term as well as a pattern

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

diff --git a/components/tactics/eliminationTactics.ml b/components/tactics/eliminationTactics.ml
index 85eade2d08e0291ac53b7a5cab724f47b4831e26..f18d2b333b68b322523b656db7db9527816c7324 100644 (file)
--- a/components/tactics/eliminationTactics.ml
+++ b/components/tactics/eliminationTactics.ml
@@ -34,24 +34,11 @@ module T    = Tacticals
 module PESR = ProofEngineStructuralRules
 module F    = FreshNamesGenerator
 module PET  = ProofEngineTypes
-module H    = ProofEngineHelpers
 module RT   = ReductionTactics
 module E    = CicEnvironment
 module R    = CicReduction
 module Un   = CicUniv
-
-(* from ProceduralClasify ***************************************************)
-
-let split c t =
-   let add s v c = Some (s, C.Decl v) :: c in
-   let rec aux whd a n c = function
-      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
-      | v when whd        -> v :: a, n
-      | v                 -> aux true a n c (R.whd ~delta:true c v)
-    in
-    aux false [] 0 c t
-
-(****************************************************************************)
+module PEH  = ProofEngineHelpers
 
 let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None 
 
@@ -64,9 +51,9 @@ let get_inductive_def uri =
 let is_not_recursive uri tyno tys = 
    let map mutinds (_, ty) = 
 (* FG: we can do much better here *)      
-      let map mutinds t = I.S.union mutinds (I.get_mutinds_of_uri uri t) in
+      let map mutinds (_, t) = I.S.union mutinds (I.get_mutinds_of_uri uri t) in
 (**********************************)      
-      let premises, _ = split [] ty in
+      let premises, _ = PEH.split_with_whd ([], ty) in
       List.fold_left map mutinds (List.tl premises)
    in
    let msg = "recursiveness check non implemented for mutually inductive types" in
@@ -80,14 +67,14 @@ let rec check_type sorts metasenv context t =
       | C.MutInd (uri, tyno, _) as t -> 
          let lpsno, tys = get_inductive_def uri in
          let _, inductive, arity, _ = List.nth tys tyno in
-         let _, psno = split [] arity in
+         let _, psno = PEH.split_with_whd ([], arity) in
          let not_relation = (lpsno = psno) in
          let not_recursive = is_not_recursive uri tyno tys in
          let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in
-         let sort = match split context ty_ty with
-            | C.Sort sort ::_ , _ -> CicPp.ppsort sort
-           | C.Meta _ :: _, _    -> CicPp.ppsort (C.Type (Un.fresh ()))
-           | _                   -> assert false
+         let sort = match PEH.split_with_whd (context, ty_ty) with
+            | (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort
+           | (_, C.Meta _) :: _, _    -> CicPp.ppsort (C.Type (Un.fresh ()))
+           | _                        -> assert false
          in
          let right_sort = List.mem sort sorts in
          if not_relation && inductive && not_recursive && right_sort then
@@ -108,7 +95,7 @@ let rec scan_tac ~old_context_length ~index ~tactic =
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let context_length = List.length context in
       let rec aux index =
-         match H.get_name context index with 
+         match PEH.get_name context index with 
            | _ when index <= 0 -> (proof, [goal])
            | None              -> aux (pred index)
            | Some what         -> 
@@ -126,11 +113,10 @@ let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
       let (proof, goal) = status in
       let _, metasenv, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
-      let index, ty = H.lookup_type metasenv context what in
-      let pattern = PET.conclusion_pattern (Some (C.Rel index)) in
+      let index, ty = PEH.lookup_type metasenv context what in
       let tac = 
          if check_type sorts metasenv context (S.lift index ty) then 
-            T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback pattern)
+            T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
                    ~continuation:(PESR.clear [what])
         else 
            let msg = "unexported elim_clear: not an decomposable type" in
@@ -149,9 +135,8 @@ let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth
     P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback
   in
   let elim_type_tac status =
-    let pattern = PET.conclusion_pattern (Some (C.Rel 1)) in
     let tac =
-      T.thens ~start: (P.cut_tac what) ~continuations:[elim pattern; T.id_tac]
+      T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
     in
     PET.apply_tactic tac status
   in