changes in declarative language : by term using tactic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9512 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 83 insertions, 34 deletions

diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 8ace0a085b..beda246298 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -22,9 +22,11 @@ open Pp
 
 let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) 
 
-let intern_justification globs = function
-    Automated l -> Automated (List.map (intern_constr globs) l)
-  | By_tactic tac -> By_tactic (intern_tactic globs tac) 
+let intern_justification_items globs = 
+  option_map (List.map (intern_constr globs))
+
+let intern_justification_method globs = 
+  option_map (intern_tactic globs)
 
 let intern_statement intern_it globs st =
   {st_label=st.st_label;
@@ -54,7 +56,8 @@ let intern_hyps iconstr globs hyps =
 
 let intern_cut intern_it globs cut=
  {cut_stat=intern_statement intern_it globs cut.cut_stat;
-  cut_by=intern_justification globs cut.cut_by}
+  cut_by=intern_justification_items globs cut.cut_by;
+  cut_using=intern_justification_method globs cut.cut_using}
 
 let intern_casee globs = function 
     Real c -> Real (intern_constr globs c)
@@ -118,10 +121,8 @@ let rec intern_proof_instr globs instr=
   {emph = instr.emph;
    instr = intern_bare_proof_instr globs instr.instr}
 
-let interp_justification env sigma  = function
-    Automated l -> 
-      Automated (List.map (fun c ->understand env sigma (fst c)) l)
-  | By_tactic tac -> By_tactic tac 
+let interp_justification_items env sigma  =
+    option_map (List.map (fun c ->understand env sigma (fst c)))
 
 let interp_constr check_sort env sigma c = 
   if check_sort then 
@@ -368,8 +369,9 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
 	     pat_expr=pat},thyps
 
 let interp_cut interp_it env sigma cut=
- {cut_stat=interp_statement interp_it env sigma cut.cut_stat;
-  cut_by=interp_justification env sigma cut.cut_by}
+  {cut with 
+    cut_stat=interp_statement interp_it env sigma cut.cut_stat;
+    cut_by=interp_justification_items env sigma cut.cut_by}
 
 let interp_casee env sigma = function 
     Real c -> Real (understand env sigma (fst c))
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 2e3e0d3c89..244cb288e2 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -259,13 +259,12 @@ let add_justification_hyps keep items gls =
 	    letin_tac false (Names.Name id) c Tacexpr.nowhere gls in 
     tclMAP add_aux items gls   
 
-let apply_to_prepared_goal items kont gls =
+let prepare_goal items gls =
   let tokeep = ref Idset.empty in
   let auxres = add_justification_hyps tokeep items gls in
    tclTHENLIST
      [ (fun _ -> auxres);
-       filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep);
-       kont ] gls
+       filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep)] gls
 
 let my_automation_tac = ref 
   (fun gls -> anomaly "No automation registered")
@@ -276,7 +275,7 @@ let automation_tac gls = !my_automation_tac gls
 
 let justification tac gls= 
     tclORELSE 
-      (tclSOLVE [tac]) 
+      (tclSOLVE [tclTHEN tac assumption]) 
       (fun gls -> 
 	 if get_strictness () then 
 	   error "insufficient justification" 
@@ -286,8 +285,8 @@ let justification tac gls=
 	     daimon_tac gls
 	   end) gls
 
-let default_justification items gls=
-  justification (apply_to_prepared_goal items automation_tac) gls
+let default_justification elems gls=
+  justification (tclTHEN (prepare_goal elems) automation_tac) gls
 
 (* code for have/then/thus/hence *)
 
@@ -452,19 +451,26 @@ let mk_stat_or_thesis info = function
 	    "\"thesis\" is split, please specify which part you refer to."
 			
 let instr_cut mkstat _thus _then cut gls0 = 
-  let info = get_its_info gls0 in  
-  let just_tac gls = 
+  let info = get_its_info gls0 in
+  let items_tac gls =
     match cut.cut_by with
-        Automated l ->	
-	  let elems = 
+	None -> tclIDTAC gls
+      | Some items -> 
+	  let items_ = 
 	    if _then then
 	      match info.pm_last with
-		  Anonymous -> l
-		| Name id -> (mkVar id) ::l
-	    else l in
-	    default_justification elems gls
-      | By_tactic t -> 
-	  justification (Tacinterp.eval_tactic t) gls in
+		  Anonymous -> error "no previous statement to use"
+		| Name id -> (mkVar id)::items
+	    else items
+	  in prepare_goal items_ gls in
+  let method_tac gls = 
+    match cut.cut_using with
+        None ->	
+	  automation_tac gls
+      | Some tac -> 
+	  (Tacinterp.eval_tactic tac) gls in
+  let just_tac gls =
+    justification (tclTHEN items_tac method_tac) gls in
   let c_id = match cut.cut_stat.st_label with 
       Anonymous -> 
 	pf_get_new_id (id_of_string "_fact") gls0 
@@ -501,13 +507,18 @@ let instr_rew _thus rew_side cut gls0 =
 	Anonymous -> error "no previous equality"
       | Name id -> id in
   let typ,lhs,rhs = decompose_eq last_id gls0 in  
-  let just_tac gls = 
+  let items_tac gls =
     match cut.cut_by with
-        Automated l ->	
-	  let elems = (mkVar last_id) :: l in
-	    default_justification elems gls
-      | By_tactic t -> 
-	  justification (Tacinterp.eval_tactic t) gls in
+	None -> tclIDTAC gls
+      | Some items -> prepare_goal items gls in
+  let method_tac gls = 
+    match cut.cut_using with
+        None ->	
+	  automation_tac gls
+      | Some tac -> 
+	  (Tacinterp.eval_tactic tac) gls in
+  let just_tac gls =
+    justification (tclTHEN items_tac method_tac) gls in
   let c_id = match cut.cut_stat.st_label with 
       Anonymous -> 
 	pf_get_new_id (id_of_string "_eq") gls0 
@@ -1201,6 +1212,30 @@ let hrec_for obj_id fix_id per_info gls=
 	    else None
       | _ -> None
 
+
+(* custom elim performs the case analysis of hypothesis id from the local 
+context, 
+
+- generalizing hypotheses below id
+- computing the elimination predicate (abstract inductive predicate) 
+- build case analysis term 
+- generalize rec_calls (use wf_paths)
+- vector of introduced identifiers per branch 
+
+match id in t return p with
+ C1 ... => ?1 
+|C2 ... => ?2
+...
+end*)
+
+
+    
+
+
+
+
+
+
 let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = 
   match tree with
       Pop t ->  
@@ -1431,8 +1466,20 @@ let rec postprocess pts instr =
     | Pcut _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
     | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts
     | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts
-    | Pescape ->
-	escape_command pts
+    | Pescape -> escape_command pts
+    | Pend (B_elim ET_Induction) ->
+  	begin
+	  let pf = proof_of_pftreestate pts in
+	  let (pfterm,_) = extract_open_pftreestate pts in
+	  let env =  Evd.evar_env (goal_of_proof pf) in
+	    try 
+	      Inductiveops.control_only_guard env pfterm;
+	      goto_current_focus_or_top (mark_as_done pts)
+ 	    with 
+		Type_errors.TypeError(env,
+				      Type_errors.IllFormedRecBody(_,_,_)) ->
+		  anomaly "\"end induction\" generated an ill-formed fixpoint"
+	end
     | Pend _ -> 
 	goto_current_focus_or_top (mark_as_done pts)