elim tactic: now takes a pattern instead of just a term

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

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 60eb4dc5b54579611febe23bee2fdff84449c437..2c22aa5ec2c10307dc308f44882367817db9a621 100644 (file)
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -477,7 +477,7 @@ let exact_tac ~term =
   mk_tactic (exact_tac ~term)
 
 (* not really "primitive" tactics .... *)
-let elim_tac ?using ~term = 
+let elim_tac ?using pattern = 
  let elim_tac (proof, goal) =
   let module T = CicTypeChecker in
   let module U = UriManager in
@@ -485,6 +485,10 @@ let elim_tac ?using ~term =
   let module C = Cic in
    let (curi,metasenv,proofbo,proofty, attrs) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+    let term, metasenv, _ = match pattern with 
+       | Some f, [], Some _ -> f context metasenv CicUniv.empty_ugraph
+       | _                  -> assert false
+    in
     let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
     let termty = CicReduction.whd context termty in
     let (termty,metasenv',arguments,fresh_meta) =
@@ -534,7 +538,27 @@ let elim_tac ?using ~term =
           | _ -> 0
         in
          let args_no = find_args_no ety in
-         let term_to_refine =
+(* we find the predicate for the eliminator as in the rewrite tactic ********)
+(*   
+   let fresh_name = 
+       FreshNamesGenerator.mk_fresh_name 
+       ~subst:[] metasenv' context C.Anonymous ~typ:termty in
+  let lifted_gty = S.lift 1 ty in
+  let lifted_conjecture =
+    metano, (Some (fresh_name, Cic.Decl ty)) :: context, lifted_gty in
+  let lifted_t1 = S.lift 1 t1x in
+  let lifted_pattern =
+    let lifted_concl_pat =
+      match concl_pat with
+      | None -> None
+      | Some term -> Some (S.lift 1 term) in
+    Some (fun c m u -> 
+       let distance  = pred (List.length c - List.length context) in
+       S.lift distance lifted_t1, m, u),[],lifted_concl_pat
+  in
+*)
+(****************************************************************************)
+        let term_to_refine =
           let rec make_tl base_case =
            function
               0 -> [base_case]
@@ -660,15 +684,15 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
 
 
 let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
-                    ?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ?using ~term:what)
+                    ?depth ?using pattern =
+ Tacticals.then_ ~start:(elim_tac ?using pattern)
   ~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
 ;;
 
 (* The simplification is performed only on the conclusion *)
 let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
-                          ?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ?using ~term:what)
+                          ?depth ?using pattern =
+ Tacticals.then_ ~start:(elim_tac ?using pattern)
   ~continuation:
    (Tacticals.thens
      ~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())