Plug back the declarative mode.

It seems to work ok, but I'm not too confident in the long run.

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

1 files changed, 46 insertions, 80 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 3b8487d75d..e47776bd7d 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -214,8 +214,7 @@ let filter_hyps f gls =
 
 let local_hyp_prefix = Id.of_string "___"
 
-let add_justification_hyps keep items gls = assert false
-(* arnaud: todo
+let add_justification_hyps keep items gls =
   let add_aux c gls=
     match kind_of_term c with
 	Var id ->
@@ -224,10 +223,9 @@ let add_justification_hyps keep items gls = assert false
       | _ ->
 	  let id=pf_get_new_id local_hyp_prefix gls in
 	    keep:=Id.Set.add id !keep;
-	    tclTHEN (letin_tac None (Names.Name id) c None Locusops.nowhere)
+	    tclTHEN (Proofview.V82.of_tactic (letin_tac None (Names.Name id) c None Locusops.nowhere))
               (thin_body [id]) gls in
     tclMAP add_aux items gls
-*)
 
 let prepare_goal items gls =
   let tokeep = ref Id.Set.empty in
@@ -255,10 +253,8 @@ let justification tac gls=
 	     daimon_tac gls
 	   end) gls
 
-let default_justification elems gls= assert false
-(* arnaud: todo
-  justification (tclTHEN (prepare_goal elems) automation_tac) gls
-*)
+let default_justification elems gls=
+  justification (tclTHEN (prepare_goal elems) (Proofview.V82.of_tactic automation_tac)) gls
 
 (* code for conclusion refining *)
 
@@ -456,8 +452,7 @@ let mk_stat_or_thesis info gls = function
       error "\"thesis for ...\" is not applicable here."
   | Thesis Plain -> pf_concl gls
 
-let just_tac _then cut info gls0 = assert false
-(* arnaud: todo
+let just_tac _then cut info gls0 =
   let last_item =
     if _then then
       try [mkVar (get_last (pf_env gls0))]
@@ -472,14 +467,12 @@ let just_tac _then cut info gls0 = assert false
   let method_tac gls =
     match cut.cut_using with
         None ->
-	  automation_tac gls
+	  Proofview.V82.of_tactic automation_tac gls
       | Some tac ->
-	  (Tacinterp.eval_tactic tac) gls in
+	  Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in
     justification (tclTHEN items_tac method_tac) gls0
-*)
 
-let instr_cut mkstat _thus _then cut gls0 = assert false
-(* arnaud:
+let instr_cut mkstat _thus _then cut gls0 =
   let info = get_its_info gls0 in
   let stat = cut.cut_stat in
   let (c_id,_) = match stat.st_label with
@@ -491,10 +484,9 @@ let instr_cut mkstat _thus _then cut gls0 = assert false
     if _thus then
       thus_tac (mkVar c_id) c_stat [] gls
     else tclIDTAC gls in
-    tclTHENS (assert_postpone c_id c_stat)
+    tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat))
       [tclTHEN tcl_erase_info (just_tac _then cut info);
        thus_tac] gls0
-*)
 
 
 (* iterated equality *)
@@ -512,8 +504,7 @@ let decompose_eq id gls =
 	  else error "Previous step is not an equality."
       | _ -> error "Previous step is not an equality."
 
-let instr_rew _thus rew_side cut gls0 = assert false
-(* arnaud:
+let instr_rew _thus rew_side cut gls0 =
   let last_id =
     try get_last (pf_env gls0)
     with UserError _ -> error "No previous equality."
@@ -526,9 +517,9 @@ let instr_rew _thus rew_side cut gls0 = assert false
   let method_tac gls =
     match cut.cut_using with
         None ->
-	  automation_tac gls
+	  Proofview.V82.of_tactic automation_tac gls
       | Some tac ->
-	  (Tacinterp.eval_tactic tac) gls in
+	  Proofview.V82.of_tactic (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
@@ -542,25 +533,23 @@ let instr_rew _thus rew_side cut gls0 = assert false
     match rew_side with
 	Lhs ->
 	  let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in
-	    tclTHENS (assert_postpone c_id new_eq)
+	    tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
 	      [tclTHEN tcl_erase_info
-		 (tclTHENS (transitivity lhs)
+		 (tclTHENS (Proofview.V82.of_tactic (transitivity lhs))
 		    [just_tac;exact_check (mkVar last_id)]);
 	       thus_tac new_eq] gls0
       | Rhs ->
 	  let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in
-	    tclTHENS (assert_postpone c_id new_eq)
+	    tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
 	      [tclTHEN tcl_erase_info
-		 (tclTHENS (transitivity rhs)
+		 (tclTHENS (Proofview.V82.of_tactic (transitivity rhs))
 		    [exact_check (mkVar last_id);just_tac]);
 	       thus_tac new_eq] gls0
-*)
 
 
 (* tactics for claim/focus *)
 
-let instr_claim _thus st gls0 = assert false
-(* arnaud: todo
+let instr_claim _thus st gls0 =
   let info = get_its_info gls0 in
   let (id,_) = match st.st_label with
       Anonymous -> pf_get_new_id (Id.of_string "_claim") gls0,false
@@ -571,24 +560,21 @@ let instr_claim _thus st gls0 = assert false
     else tclIDTAC gls in
   let ninfo1 = {pm_stack=
       (if _thus then Focus_claim else Claim)::info.pm_stack} in
-    tclTHENS (assert_postpone id st.st_it)
+    tclTHENS (Proofview.V82.of_tactic (assert_postpone id st.st_it))
       [thus_tac;
        tcl_change_info ninfo1] gls0
-*)
 
 (* tactics for assume *)
 
-let push_intro_tac coerce nam gls = assert false
-(* arnaud: todo
+let push_intro_tac coerce nam gls =
       let (hid,_) =
 	match nam with
 	    Anonymous -> pf_get_new_id (Id.of_string "_hyp") gls,false
 	  | Name id -> id,true in
 	tclTHENLIST
-	  [intro_mustbe_force hid;
+	  [Proofview.V82.of_tactic (intro_mustbe_force hid);
 	   coerce hid]
 	  gls
-*)
 
 let assume_tac hyps gls =
   List.fold_right
@@ -655,8 +641,7 @@ let rec build_applist prod = function
       let ctx,head = build_applist (prod_applist prod [mkMeta n]) q in
 	(n,typ)::ctx,head
 
-let instr_suffices _then cut gls0 = assert false
-(* arnaud: todo
+let instr_suffices _then cut gls0 =
   let info = get_its_info gls0 in
   let c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in
   let ctx,hd = cut.cut_stat in
@@ -666,13 +651,12 @@ let instr_suffices _then cut gls0 = assert false
   let c_term = applist (mkVar c_id,List.map mkMeta metas) in
   let thus_tac gls=
     thus_tac c_term c_head c_ctx gls in
-   tclTHENS (assert_postpone c_id c_stat)
+   tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat))
      [tclTHENLIST
 	 [ assume_tac ctx;
 	   tcl_erase_info;
 	   just_tac _then cut info];
       thus_tac] gls0
-*)
 
 (* tactics for consider/given *)
 
@@ -692,20 +676,17 @@ let conjunction_arity id gls =
 	    List.length rc
       | _ -> raise Not_found
 
-let rec intron_then n ids ltac gls = assert false
-(* arnaud:
+let rec intron_then n ids ltac gls =
   if n<=0 then
     ltac ids gls
   else
     let id = pf_get_new_id (Id.of_string "_tmp") gls in
       tclTHEN
-	(intro_mustbe_force id)
+	(Proofview.V82.of_tactic (intro_mustbe_force id))
 	(intron_then (pred n) (id::ids) ltac) gls
-*)
 
 
-let rec consider_match may_intro introduced available expected gls = assert false
-(* arnaud:
+let rec consider_match may_intro introduced available expected gls =
   match available,expected with
       [],[] ->
 	  tclIDTAC gls
@@ -716,7 +697,7 @@ let rec consider_match may_intro introduced available expected gls = assert fals
 	  begin
  	    let id = pf_get_new_id (Id.of_string "_tmp") gls in
 	      tclIFTHENELSE
-		(intro_mustbe_force id)
+		(Proofview.V82.of_tactic (intro_mustbe_force id))
 		(consider_match true [] [id] hyps)
 		(fun _ ->
 		   error "Not enough sub-hypotheses to match statements.")
@@ -742,25 +723,22 @@ let rec consider_match may_intro introduced available expected gls = assert fals
 		 try conjunction_arity id gls with
 		     Not_found -> error "Matching hypothesis not found." in
 		 tclTHENLIST
-		   [general_case_analysis false (mkVar id,NoBindings);
+		   [Proofview.V82.of_tactic (general_case_analysis false (mkVar id,NoBindings));
 		    intron_then nhyps []
 		      (fun l -> consider_match may_intro introduced
 			 (List.rev_append l rest_ids) expected)] gls)
 	  end
 	  gls
-*)
 
-let consider_tac c hyps gls = assert false
-(* arnaud: todo
+let consider_tac c hyps gls =
   match kind_of_term (strip_outer_cast c) with
       Var id ->
 	consider_match false [] [id] hyps gls
     | _ ->
 	let id = pf_get_new_id (Id.of_string "_tmp") gls in
 	tclTHEN
-	  (forward None (Some (Loc.ghost, IntroIdentifier id)) c)
+	  (Proofview.V82.of_tactic (forward None (Some (Loc.ghost, IntroIdentifier id)) c))
  	  (consider_match false [] [id] hyps) gls
-*)
 
 
 let given_tac hyps gls =
@@ -788,11 +766,9 @@ let rec build_function args body =
 	  mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun)
     | [] -> body
 
-let define_tac id args body gls = assert false
-(* arnaud: todo:
+let define_tac id args body gls =
   let t = build_function args body in
-    letin_tac None (Name id) t None Locusops.nowhere gls
-*)
+    Proofview.V82.of_tactic (letin_tac None (Name id) t None Locusops.nowhere) gls
 
 (* tactics for reconsider *)
 
@@ -925,8 +901,7 @@ let register_nodep_subcase id= function
       end
   | _ -> anomaly (Pp.str "wrong stack state")
 
-let suppose_tac hyps gls0 = assert false
-(* arnaud: todo
+let suppose_tac hyps gls0 =
   let info = get_its_info gls0 in
   let thesis = pf_concl gls0 in
   let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
@@ -934,12 +909,11 @@ let suppose_tac hyps gls0 = assert false
   let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
   let old_clauses,stack = register_nodep_subcase id info.pm_stack in
   let ninfo2 = {pm_stack=stack} in
-    tclTHENS (assert_postpone id clause)
+    tclTHENS (Proofview.V82.of_tactic (assert_postpone id clause))
       [tclTHENLIST [tcl_change_info ninfo1;
 		    assume_tac hyps;
 		    clear old_clauses];
        tcl_change_info ninfo2] gls0
-*)
 
 (* suppose it is ... *)
 
@@ -1128,8 +1102,7 @@ let rec register_dep_subcase id env per_info pat = function
 	(EK_dep (start_tree env per_info.per_ind per_info.per_wf))
   | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree)
 
-let case_tac params pat_info hyps gls0 = assert false
-(* arnaud: todo
+let case_tac params pat_info hyps gls0 =
   let info = get_its_info gls0 in
   let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
   let et,per_info,ek,old_clauses,rest =
@@ -1142,7 +1115,7 @@ let case_tac params pat_info hyps gls0 = assert false
     register_dep_subcase (id,(List.length params,List.length hyps)) 
       (pf_env gls0) per_info pat_info.pat_pat ek in  
   let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
-    tclTHENS (assert_postpone id clause)
+    tclTHENS (Proofview.V82.of_tactic (assert_postpone id clause))
       [tclTHENLIST
 	 [tcl_change_info ninfo1;
 	  assume_st (params@pat_info.pat_vars);
@@ -1150,7 +1123,6 @@ let case_tac params pat_info hyps gls0 = assert false
 	  assume_hyps_or_theses hyps;
 	  clear old_clauses];
        tcl_change_info ninfo2] gls0
-*)
 
 (* end cases *)
 
@@ -1205,8 +1177,7 @@ let hrec_for fix_id per_info gls obj_id =
     compose_lam rc (whd_beta gls.sigma hd2)
 
 
-let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = assert false
-(* arnaud: todo
+let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
   match tree, objs  with
       Close_patt t,_ ->
 	let args0 = pop_stacks args in
@@ -1222,7 +1193,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = asser
 		  List.init (nparams + nhyps) (fun n -> mkMeta (succ n))  in
 		let param_metas,hyp_metas = List.chop nparams all_metas in
 		  tclTHEN
-		    (tclDO nhrec introf)
+		    (tclDO nhrec (Proofview.V82.of_tactic introf))
 		    (tacnext 
 		       (applist (mkVar id,
 				 List.append param_metas 
@@ -1266,7 +1237,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = asser
 		  else (mkVar id::objs),recs,nrec in
 	  let objs,recs,nhrec = aux 0 args_ids in
 	    tclTHENLIST
-	      [tclMAP intro_mustbe_force args_ids;
+	      [tclMAP (fun id -> Proofview.V82.of_tactic (intro_mustbe_force id)) args_ids;
 	       begin
 		 fun gls1 ->
 		   let hrecs =
@@ -1299,7 +1270,6 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = asser
 	anomaly ~label:"execute_cases " (Pp.str "Nothing to skip")
     | End_patt (_,_) , _ :: _  ->
 	anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left")
-*)
 
 let understand_my_constr c gls =
   let env = pf_env gls in
@@ -1311,16 +1281,13 @@ let understand_my_constr c gls =
   in
   Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc)
 
-let my_refine c gls = assert false
-(* arnaud: todo
+let my_refine c gls =
   let oc = understand_my_constr c gls in
-  Refine.refine oc gls
-*)
+  Proofview.V82.of_tactic (Tactics.New.refine oc) gls
 
 (* end focus/claim *)
 
-let end_tac et2 gls = assert false
-(* arnaud: todo
+let end_tac et2 gls =
   let info = get_its_info gls in
   let et1,pi,ek,clauses =
     match info.pm_stack with
@@ -1344,15 +1311,15 @@ let end_tac et2 gls = assert false
       begin
 	match et,ek with
 	    _,EK_unknown ->
-	      tclSOLVE [simplest_elim pi.per_casee]
+	      tclSOLVE [Proofview.V82.of_tactic (simplest_elim pi.per_casee)]
 	  | ET_Case_analysis,EK_nodep ->
 	      tclTHEN
-		(general_case_analysis false (pi.per_casee,NoBindings))
+		(Proofview.V82.of_tactic (general_case_analysis false (pi.per_casee,NoBindings)))
 		(default_justification (List.map mkVar clauses))
 	  | ET_Induction,EK_nodep ->
 	      tclTHENLIST
 		[generalize (pi.per_args@[pi.per_casee]);
-		 simple_induct (AnonHyp (succ (List.length pi.per_args)));
+		 Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args))));
 		 default_justification (List.map mkVar clauses)]
 	  | ET_Case_analysis,EK_dep tree ->
 		 execute_cases Anonymous pi 
@@ -1372,8 +1339,8 @@ let end_tac et2 gls = assert false
 			pf_get_new_id (Id.of_string "_main_arg") gls0 in
 			tclTHENLIST
 			  [fix (Some fix_id) (succ nargs);
-			   tclDO nargs introf;
-			   intro_mustbe_force c_id;
+			   tclDO nargs (Proofview.V82.of_tactic introf);
+			   Proofview.V82.of_tactic (intro_mustbe_force c_id);
 			   execute_cases (Name fix_id) pi
 			     (fun c ->
 				tclTHENLIST
@@ -1385,7 +1352,6 @@ let end_tac et2 gls = assert false
 			     [mkVar c_id]  0 tree] gls0
 		  end
       end gls
-*)
 
 (* escape *)