New tactic clear; new syntax # _; to introduce and immediately clear an

[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 f45aa656b5136ce182460ca856526390668129c3..250d50ce39adb949482f89018b98c4f915cf82f4 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -305,29 +305,56 @@ let elim_tac ~what ~where status =
    status
 ;;
 
+let find_in_context name context =
+  let rec aux acc = function
+    | [] -> raise Not_found
+    | (hd,_) :: tl when hd = name -> acc
+    | _ :: tl ->  aux (acc + 1) tl
+  in
+  aux 1 context
+;;
+
+let clear name status goal =
+ let goalty = get_goalty status goal in
+ let j =
+  try find_in_context name (ctx_of goalty)
+  with Not_found -> fail (lazy ("hypothesis '" ^ name ^ "' not found")) in
+ let n,h,metasenv,subst,o = status.pstatus in
+ let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal [j] in
+  { status with pstatus = n,h,metasenv,subst,o }
+;;
+
+let clear_tac name = distribute_tac (clear name);;
+
 let intro_tac name =
- exact_tac
-  ("",0,(CicNotationPt.Binder (`Lambda,
-   (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
+ block_tac
+  [ exact_tac
+    ("",0,(CicNotationPt.Binder (`Lambda,
+     (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)));
+    if name = "_" then clear_tac name else fun x -> x ]
 ;;
 
-let case ~what status goal =
+let cases ~what status goal =
  let gty = get_goalty status goal in
  let status, what = disambiguate status what None (ctx_of gty) in
  let ty = typeof status (ctx_of what) what in
  let ref, consno, left, right = analyse_indty status ty in
  let t =
-  NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,
+  NCic.Match (ref,NCic.Implicit `Term, term_of_cic_term what (ctx_of gty),
     HExtlib.mk_list (NCic.Implicit `Term) consno)
  in
  let ctx = ctx_of gty in
- let status,t,ty = refine status ctx (mk_cic_term ctx t) None in
+ let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in
  instantiate status goal t
 ;;
 
-let case_tac ~what = distribute_tac (case ~what);;
+let cases_tac ~what ~where = 
+  block_tac [ select_tac ~where ; distribute_tac (cases ~what) ]
+;;
 
 let case1_tac name =
  block_tac [ intro_tac name; 
-             case_tac ~what:("",0,CicNotationPt.Ident (name,None)) ]
+             cases_tac 
+              ~where:("",0,(None,[],None)) 
+              ~what:("",0,CicNotationPt.Ident (name,None)) ]
 ;;