New tactic "case1_tac" that make "intro" followed by case of the first

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 2521498ba8f71115d0cb44638bed8be6051f226f..87be3279f18ade3f1f49ad8bbebb443e94251d9c 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -288,6 +288,14 @@ let typeof status where t =
   None, ctx, ty
 ;;
   
+let whd status ?delta where t =
+  let _,_,metasenv,subst,_ = status.pstatus in
+  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
+  let _,_,t = relocate ctx t in
+  let t = NCicReduction.whd ~subst ?delta ctx t in
+  None, ctx, t
+;;
+  
 let unify status where a b =
   let n,h,metasenv,subst,o = status.pstatus in
   let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
@@ -448,6 +456,8 @@ let exact t status goal =
  instantiate status goal t
 ;;
 
+let exact_tac t = distribute_tac (exact t) ;;
+
 let reopen status =
  let n,h,metasenv,subst,o = status.pstatus in
  let subst, newm = 
@@ -515,4 +525,32 @@ let elim_tac ~what ~where status =
    status
 ;;
 
+let intro_tac name =
+ exact_tac
+  ("",0,(CicNotationPt.Binder (`Lambda,
+   (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
+;;
 
+let case status goal =
+ let _,ctx,_ = get_goal status goal in
+ let ty = typeof status (`Ctx ctx) ("",ctx,NCic.Rel 1) in
+ let ref =
+  match whd status (`Ctx ctx) ty with
+     _,_,NCic.Const ref
+   | _,_,NCic.Appl (NCic.Const ref :: _) -> ref
+   | _,_,_ -> fail (lazy ("not an inductive type")) in
+ let _,_,tl,_,i = NCicEnvironment.get_checked_indtys ref in
+ let _,_,_,cl = List.nth tl i in
+ let consno = List.length cl in
+ let t =
+  NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,HExtlib.mk_list (NCic.Implicit `Term) consno)
+ in
+ let status,t,ty = refine status (`Ctx ctx) ("",ctx,t) None in
+ instantiate status goal t
+;;
+
+let case_tac = distribute_tac case;;
+
+let case1_tac name =
+ block_tac [ intro_tac name; case_tac ]
+;;