(*i camlp4deps: "parsing/grammar.cma" i*) (*Toplevel loop for the communication between Coq and Centaur *) open Names;; open Nameops;; open Util;; open Ast;; open Term;; open Pp;; open Libnames;; open Libobject;; open Library;; open Vernacinterp;; open Evd;; open Proof_trees;; open Termast;; open Tacmach;; open Pfedit;; open Proof_type;; open Parsing;; open Environ;; open Declare;; open Declarations;; open Rawterm;; open Reduction;; open Classops;; open Vernacinterp;; open Vernac;; open Command;; open Protectedtoplevel;; open Coqast;; open Line_oriented_parser;; open Xlate;; open Vtp;; open Ascent;; open Translate;; open Name_to_ast;; open Pbp;; open Blast;; (* open Dad;; *) open Debug_tac;; open Search;; open Constrintern;; open Nametab;; open Showproof;; open Showproof_ct;; open Tacexpr;; open Vernacexpr;; let pcoq_started = ref None;; let if_pcoq f a = if !pcoq_started <> None then f a else error "Pcoq is not started";; let text_proof_flag = ref "en";; (* let current_proof_name = ref "";; *) let current_proof_name () = try string_of_id (get_current_proof_name ()) with UserError("Pfedit.get_proof", _) -> "";; let current_goal_index = ref 0;; let guarded_force_eval_stream (s : std_ppcmds) = let l = ref [] in let f elt = l:= elt :: !l in (try Stream.iter f s with | _ -> f (Stream.next (str "error guarded_force_eval_stream"))); Stream.of_list (List.rev !l);; let rec string_of_path p = match p with [] -> "\n" | i::p -> (string_of_int i)^" "^ (string_of_path p) ;; let print_path p = output_results_nl (str "Path:" ++ str (string_of_path p)) ;; let kill_proof_node index = let paths = History.historical_undo (current_proof_name()) index in let _ = List.iter (fun path -> (traverse_to path; Pfedit.mutate weak_undo_pftreestate; traverse_to [])) paths in History.border_length (current_proof_name());; (*Message functions, the text of these messages is recognized by the protocols *) (*of CtCoq *) let ctf_header message_name request_id = fnl () ++ str "message" ++ fnl() ++ str message_name ++ fnl() ++ int request_id ++ fnl();; let ctf_acknowledge_command request_id command_count opt_exn = let goal_count, goal_index = if refining() then let g_count = List.length (fst (frontier (proof_of_pftreestate (get_pftreestate ())))) in g_count, (min g_count !current_goal_index) else (0, 0) in (ctf_header "acknowledge" request_id ++ int command_count ++ fnl() ++ int goal_count ++ fnl () ++ int goal_index ++ fnl () ++ str (current_proof_name()) ++ fnl() ++ (match opt_exn with Some e -> Cerrors.explain_exn e | None -> mt ()) ++ fnl() ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());; let ctf_undoResults = ctf_header "undo_results";; let ctf_TextMessage = ctf_header "text_proof";; let ctf_SearchResults = ctf_header "search_results";; let ctf_OtherGoal = ctf_header "other_goal";; let ctf_Location = ctf_header "location";; let ctf_StateMessage = ctf_header "state";; let ctf_PathGoalMessage () = fnl () ++ str "message" ++ fnl () ++ str "single_goal" ++ fnl ();; let ctf_GoalReqIdMessage = ctf_header "single_goal_state";; let ctf_NewStateMessage = ctf_header "fresh_state";; let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++ str "saved" ++ fnl();; let ctf_KilledMessage req_id ngoals = ctf_header "killed" req_id ++ int ngoals ++ fnl ();; let ctf_AbortedAllMessage () = fnl() ++ str "message" ++ fnl() ++ str "aborted_all" ++ fnl();; let ctf_AbortedMessage request_id na = ctf_header "aborted_proof" request_id ++ str na ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();; let ctf_UserErrorMessage request_id stream = let stream = guarded_force_eval_stream stream in ctf_header "user_error" request_id ++ stream ++ fnl() ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl();; let ctf_ResetInitialMessage () = fnl () ++ str "message" ++ fnl () ++ str "reset_initial" ++ fnl ();; let ctf_ResetIdentMessage request_id s = ctf_header "reset_ident" request_id ++ str s ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl();; type vtp_tree = | P_rl of ct_RULE_LIST | P_r of ct_RULE | P_s_int of ct_SIGNED_INT_LIST | P_pl of ct_PREMISES_LIST | P_cl of ct_COMMAND_LIST | P_t of ct_TACTIC_COM | P_text of ct_TEXT | P_ids of ct_ID_LIST;; let print_tree t = (match t with | P_rl x -> fRULE_LIST x | P_r x -> fRULE x | P_s_int x -> fSIGNED_INT_LIST x | P_pl x -> fPREMISES_LIST x | P_cl x -> fCOMMAND_LIST x | P_t x -> fTACTIC_COM x | P_text x -> fTEXT x | P_ids x -> fID_LIST x); print_string "e\nblabla\n";; let break_happened = ref false;; let output_results stream vtp_tree = let _ = Sys.signal Sys.sigint (Sys.Signal_handle(fun i -> (break_happened := true;()))) in msg stream; match vtp_tree with Some t -> print_tree t | None -> ();; let output_results_nl stream = let _ = Sys.signal Sys.sigint (Sys.Signal_handle(fun i -> break_happened := true;())) in msgnl stream;; let rearm_break () = let _ = Sys.signal Sys.sigint (Sys.Signal_handle(fun i -> raise Sys.Break)) in ();; let check_break () = if (!break_happened) then begin break_happened := false; raise Sys.Break end else ();; let print_past_goal index = let path = History.get_path_for_rank (current_proof_name()) index in try traverse_to path; let pf = proof_of_pftreestate (get_pftreestate ()) in output_results (ctf_PathGoalMessage ()) (Some (P_r (translate_goal pf.goal))) with | Invalid_argument s -> ((try traverse_to [] with _ -> ()); error "No focused proof (No proof-editing in progress)") | e -> (try traverse_to [] with _ -> ()); raise e ;; let show_nth n = try let pf = proof_of_pftreestate (get_pftreestate()) in if (!text_proof_flag<>"off") then (if n=0 then output_results (ctf_TextMessage !global_request_id) (Some (P_text (show_proof !text_proof_flag []))) else let path = History.get_nth_open_path (current_proof_name()) n in output_results (ctf_TextMessage !global_request_id) (Some (P_text (show_proof !text_proof_flag path)))) else output_results (ctf_GoalReqIdMessage !global_request_id) (let goal = List.nth (fst (frontier pf)) (n - 1) in (Some (P_r (translate_goal goal)))) with | Invalid_argument s -> error "No focused proof (No proof-editing in progress)";; (* The rest of the file contains commands that are changed from the plain Coq distribution *) let ctv_SEARCH_LIST = ref ([] : ct_PREMISE list);; (* let filter_by_module_from_varg_list l = let dir_list, b = Vernacentries.interp_search_restriction l in Search.filter_by_module_from_list (dir_list, b);; *) let add_search (global_reference:global_reference) assumptions cstr = try let id_string = string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty global_reference) in let ast = try CT_premise (CT_ident id_string, translate_constr false assumptions cstr) with Not_found -> CT_premise (CT_ident id_string, CT_coerce_ID_to_FORMULA( CT_ident ("Error printing" ^ id_string))) in ctv_SEARCH_LIST:= ast::!ctv_SEARCH_LIST with e -> msgnl (str "add_search raised an exception"); raise e;; (* let make_error_stream node_string = str "The syntax of " ++ str node_string ++ str " is inconsistent with the vernac interpreter entry";; *) let ctf_EmptyGoalMessage id = fnl () ++ str "Empty Goal is a no-op. Fun oh fun." ++ fnl ();; let print_check judg = let {uj_val=value; uj_type=typ} = judg in let value_ct_ast = (try translate_constr false (Global.env()) value with UserError(f,str) -> raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env()) value) ++ fnl () ++ str ))) in let type_ct_ast = (try translate_constr false (Global.env()) typ with UserError(f,str) -> raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env()) value) ++ fnl() ++ str))) in ((ctf_SearchResults !global_request_id), (Some (P_pl (CT_premises_list [CT_coerce_TYPED_FORMULA_to_PREMISE (CT_typed_formula(value_ct_ast,type_ct_ast) )]))));; let ct_print_eval ast red_fun env judg = ((if refining() then traverse_to []); let {uj_val=value; uj_type=typ} = judg in let nvalue = red_fun value (* // Attention , ici il faut peut être utiliser des environnemenst locaux *) and ntyp = nf_betaiota typ in (ctf_SearchResults !global_request_id, Some (P_pl (CT_premises_list [CT_eval_result (xlate_formula ast, translate_constr false env nvalue, translate_constr false env ntyp)]))));; (* The following function is copied from globpr in env/printer.ml *) let globcv x = match x with | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) -> convert_qualid (Nametab.shortest_qualid_of_global Idset.empty (IndRef(sp,tyi))) | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) -> convert_qualid (Nametab.shortest_qualid_of_global Idset.empty (ConstructRef ((sp, tyi), i))) | _ -> failwith "globcv : unexpected value";; let pbp_tac_pcoq = pbp_tac (function (x:raw_tactic_expr) -> output_results (ctf_header "pbp_results" !global_request_id) (Some (P_t(xlate_tactic x))));; let blast_tac_pcoq = blast_tac (function (x:raw_tactic_expr) -> output_results (ctf_header "pbp_results" !global_request_id) (Some (P_t(xlate_tactic x))));; (* <\cpa> let dad_tac_pcoq = dad_tac(function x -> output_results (ctf_header "pbp_results" !global_request_id) (Some (P_t(xlate_tactic x))));; *) let search_output_results () = output_results (ctf_SearchResults !global_request_id) (Some (P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));; let debug_tac2_pcoq tac = (fun g -> let the_goal = ref (None : goal sigma option) in let the_ast = ref tac in let the_path = ref ([] : int list) in try let result = report_error tac the_goal the_ast the_path [] g in (errorlabstrm "DEBUG TACTIC" (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++ fnl () ++ str "the tactic is" ++ fnl () ++ Pptactic.pr_glob_tactic tac); result) with e -> match !the_goal with None -> raise e | Some g -> (output_results (ctf_Location !global_request_id) (Some (P_s_int (CT_signed_int_list (List.map (fun n -> CT_coerce_INT_to_SIGNED_INT (CT_int n)) (clean_path tac (List.rev !the_path))))))); (output_results (ctf_OtherGoal !global_request_id) (Some (P_r (translate_goal (sig_it g))))); raise e);; let rec selectinspect n env = match env with [] -> [] | a::tl -> if n = 0 then [] else match a with (sp, Lib.Leaf lobj) -> a::(selectinspect (n -1 ) tl) | _ -> (selectinspect n tl);; open Term;; let inspect n = let env = Global.env() in let add_search2 x y = add_search x env y in let l = selectinspect n (Lib.contents_after None) in ctv_SEARCH_LIST := []; List.iter (fun a -> try (match a with oname, Lib.Leaf lobj -> (match oname, object_tag lobj with (sp,_), "VARIABLE" -> let (_, _, v) = get_variable (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), "CONSTANT" -> let {const_type=typ} = Global.lookup_constant kn in add_search2 (Nametab.locate (qualid_of_sp sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_sp sp)) (Pretyping.understand Evd.empty (Global.env()) (RRef(dummy_loc, IndRef(kn,0)))) | _ -> failwith ("unexpected value 1 for "^ (string_of_id (basename (fst oname))))) | _ -> failwith "unexpected value") with e -> ()) l; output_results (ctf_SearchResults !global_request_id) (Some (P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));; let ct_int_to_TARG n = CT_coerce_FORMULA_OR_INT_to_TARG (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT (CT_coerce_INT_to_ID_OR_INT (CT_int n)));; let pair_list_to_ct l = CT_user_tac(CT_ident "pair_int_list", CT_targ_list (List.map (fun (a,b) -> CT_coerce_TACTIC_COM_to_TARG (CT_user_tac (CT_ident "pair_int", CT_targ_list [ct_int_to_TARG a; ct_int_to_TARG b]))) l));; (* Annule toutes les commandes qui s'appliquent sur les sous-buts du but auquel a été appliquée la n-ième tactique *) let logical_kill n = let path = History.get_path_for_rank (current_proof_name()) n in begin traverse_to path; Pfedit.mutate weak_undo_pftreestate; (let kept_cmds, undone_cmds, remaining_goals, current_goal = History.logical_undo (current_proof_name()) n in output_results (ctf_undoResults !global_request_id) (Some (P_t (CT_user_tac (CT_ident "log_undo_result", CT_targ_list [CT_coerce_TACTIC_COM_to_TARG (pair_list_to_ct kept_cmds); CT_coerce_TACTIC_COM_to_TARG(pair_list_to_ct undone_cmds); ct_int_to_TARG remaining_goals; ct_int_to_TARG current_goal]))))); traverse_to [] end;; let simulate_solve n tac = let path = History.get_nth_open_path (current_proof_name()) n in solve_nth n (Tacinterp.hide_interp tac (get_end_tac())); traverse_to path; Pfedit.mutate weak_undo_pftreestate; traverse_to [] let kill_node_verbose n = let ngoals = kill_proof_node n in output_results_nl (ctf_KilledMessage !global_request_id ngoals) let set_text_mode s = text_proof_flag := s let pcoq_reset_initial() = output_results(ctf_AbortedAllMessage()) None; Vernacentries.abort_refine Lib.reset_initial (); output_results(ctf_ResetInitialMessage()) None;; let pcoq_reset x = if refining() then output_results (ctf_AbortedAllMessage ()) None; Vernacentries.abort_refine Lib.reset_name (dummy_loc,x); output_results (ctf_ResetIdentMessage !global_request_id (string_of_id x)) None;; VERNAC ARGUMENT EXTEND text_mode | [ "fr" ] -> [ "fr" ] | [ "en" ] -> [ "en" ] | [ "Off" ] -> [ "off" ] END VERNAC COMMAND EXTEND TextMode | [ "Text" "Mode" text_mode(s) ] -> [ set_text_mode s ] END VERNAC COMMAND EXTEND OutputGoal [ "Goal" ] -> [ output_results_nl(ctf_EmptyGoalMessage "") ] END VERNAC COMMAND EXTEND OutputGoal [ "Goal" "Cmd" natural(n) "with" tactic(tac) ] -> [ simulate_solve n tac ] END VERNAC COMMAND EXTEND KillProofAfter | [ "Kill" "Proof" "after" natural(n) ] -> [ kill_node_verbose n ] END VERNAC COMMAND EXTEND KillProofAt | [ "Kill" "Proof" "at" natural(n) ] -> [ kill_node_verbose n ] END VERNAC COMMAND EXTEND KillSubProof [ "Kill" "SubProof" natural(n) ] -> [ logical_kill n ] END VERNAC COMMAND EXTEND PcoqReset [ "Pcoq" "Reset" ident(x) ] -> [ pcoq_reset x ] END VERNAC COMMAND EXTEND PcoqResetInitial [ "Pcoq" "ResetInitial" ] -> [ pcoq_reset_initial() ] END let start_proof_hook () = History.start_proof (current_proof_name()); current_goal_index := 1 let solve_hook n = let name = current_proof_name () in let old_n_count = History.border_length name in let pf = proof_of_pftreestate (get_pftreestate ()) in let n_goals = (List.length (fst (frontier pf))) + 1 - old_n_count in begin current_goal_index := n; History.push_command name n n_goals end let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s) let pcoq_search s l = ctv_SEARCH_LIST:=[]; begin match s with | SearchAbout locqid -> raw_search_about (filter_by_module_from_list l) add_search (Nametab.global locqid) | SearchPattern c -> let _,pat = interp_constrpattern Evd.empty (Global.env()) c in raw_pattern_search (filter_by_module_from_list l) add_search pat | SearchRewrite c -> let _,pat = interp_constrpattern Evd.empty (Global.env()) c in raw_search_rewrite (filter_by_module_from_list l) add_search pat; | SearchHead locqid -> filtered_search (filter_by_module_from_list l) add_search (Nametab.global locqid) end; search_output_results() let pcoq_print_name ref = let results = xlate_vernac_list (name_to_ast ref) in output_results (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl ()) (Some (P_cl results)) let pcoq_print_check j = let a,b = print_check j in output_results a b let pcoq_print_eval redfun env c j = let strm, vtp = ct_print_eval c redfun env j in output_results strm vtp;; open Vernacentries let pcoq_show_goal = function | Some n -> show_nth n | None -> if !pcoq_started = Some true (* = debug *) then show_open_subgoals () else errorlabstrm "show_goal" (str "Show must be followed by an integer in Centaur mode");; let pcoq_hook = { start_proof = start_proof_hook; solve = solve_hook; abort = abort_hook; search = pcoq_search; print_name = pcoq_print_name; print_check = pcoq_print_check; print_eval = pcoq_print_eval; show_goal = pcoq_show_goal } (* let command_changes = [ ("TEXT_MODE", (function | [Coqast.VARG_AST (Str(_,x))] -> (fun () -> set_text_mode x))); ("StartProof", (function | (Coqast.VARG_STRING kind) :: ((Coqast.VARG_IDENTIFIER s) :: ((Coqast.VARG_CONSTR c) :: [])) -> let stre = match kind with | "THEOREM" -> NeverDischarge | "LEMMA" -> NeverDischarge | "FACT" -> make_strength_1 () | "REMARK" -> make_strength_0 () | "DEFINITION" -> NeverDischarge | "LET" -> make_strength_2 () | "LETTOP" -> NotDeclare | "LOCAL" -> make_strength_0 () | _ -> errorlabstrm "StartProof" (make_error_stream "StartProof") in fun () -> begin if kind = "LETTOP" && not(refining ()) then errorlabstrm "StartProof" (str "Let declarations can only be used in proof editing mode" ); let str = (string_of_id s) in start_proof_com (Some s) stre c; start_proof_hook str; end | _ -> errorlabstrm "StartProof" (make_error_stream "StartProof"))); ("GOAL", (function | (Coqast.VARG_CONSTR c) :: [] -> (fun () -> if not (refining ()) then begin start_proof_com None NeverDischarge c; start_proof_hook "Unnamed_thm" end) | [] -> (function () -> output_results_nl(ctf_EmptyGoalMessage "")) | _ -> errorlabstrm "Goal" (make_error_stream "Goal"))); ("SOLVE", (function | [Coqast.VARG_NUMBER n; Coqast.VARG_TACTIC tcom] -> (fun () -> if not (refining ()) then error "Unknown command of the non proof-editing mode"; solve_nth n (Tacinterp.hide_interp tcom); (* pcoq *) solve_hook n (**) | _ -> errorlabstrm "SOLVE" (make_error_stream "SOLVE"))); (* SIMULE SOLVE SANS EFFET *) ("GOAL_CMD", (function | (Coqast.VARG_NUMBER n) :: ((Coqast.VARG_TACTIC tac) :: []) -> (function () -> let path = History.get_nth_open_path !current_proof_name n in solve_nth n (Tacinterp.hide_interp tac); traverse_to path; Pfedit.mutate weak_undo_pftreestate; traverse_to []) | _ -> errorlabstrm "GOAL_CMD" (make_error_stream "GOAL_CMD"))); (* Revient à l'état avant l'application de la n-ième tactique *) ("KILL_NODE", (function | (Coqast.VARG_NUMBER n) :: [] -> (function () -> let ngoals = kill_proof_node n in output_results_nl (ctf_KilledMessage !global_request_id ngoals)) | _ -> errorlabstrm "KILL_NODE" (make_error_stream "KILL_NODE"))); (* Annule toutes les commandes qui s'appliquent sur les sous-buts du but auquel a été appliquée la n-ième tactique *) ("KILL_SUB_PROOF", (function | [Coqast.VARG_NUMBER n] -> (function () -> logical_kill n) | _ -> errorlabstrm "KILL_SUB_PROOF" (make_error_stream "KILL_SUB_PROOF"))); ("RESUME", (function [Coqast.VARG_IDENTIFIER id] -> (fun () -> let str = (string_of_id id) in resume_proof id; (* Pcoq *) current_proof_name := str) (**) | _ -> errorlabstrm "RESUME" (make_error_stream "RESUME"))); (* NoOp... *) ("BeginSilent", (function | [] -> (function () -> errorlabstrm "Begin Silent" (str "not available in Centaur mode")) | _ -> errorlabstrm "BeginSilent" (make_error_stream "BeginSilent"))); ("EndSilent", (function | [] -> (function () -> errorlabstrm "End Silent" (str "not available in Centaur mode")) | _ -> errorlabstrm "EndSilent" (make_error_stream "EndSilent"))); ("ABORT", (function | (Coqast.VARG_IDENTIFIER id) :: [] -> (function () -> delete_proof id; (* Pcoq *) current_proof_name := ""; output_results_nl (ctf_AbortedMessage !global_request_id (string_of_id id))) (**) | [] -> (function () -> delete_current_proof (); (* Pcoq *) current_proof_name := ""; output_results_nl (ctf_AbortedMessage !global_request_id "")) (**) | _ -> errorlabstrm "ABORT" (make_error_stream "ABORT"))); ("SEARCH", function (Coqast.VARG_QUALID qid)::l -> (fun () -> ctv_SEARCH_LIST:=[]; let global_ref = Nametab.global dummy_loc qid in filtered_search (filter_by_module_from_varg_list l) add_search (Nametab.locate qid); search_output_results()) | _ -> failwith "bad form of arguments"); ("SearchRewrite", function (Coqast.VARG_CONSTR c)::l -> (fun () -> ctv_SEARCH_LIST:=[]; let _,pat = interp_constrpattern Evd.empty (Global.env()) c in raw_search_rewrite (filter_by_module_from_varg_list l) add_search pat; search_output_results()) | _ -> failwith "bad form of arguments"); ("SearchPattern", function (Coqast.VARG_CONSTR c)::l -> (fun () -> ctv_SEARCH_LIST := []; let _,pat = interp_constrpattern Evd.empty (Global.env()) c in raw_pattern_search (filter_by_module_from_varg_list l) add_search pat; search_output_results()) | _ -> failwith "bad form of arguments"); ("PrintId", (function | [Coqast.VARG_QUALID qid] -> (function () -> let results = xlate_vernac_list (Ctast.ast_to_ct (name_to_ast qid)) in output_results (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl ()) (Some (P_cl results))) | _ -> errorlabstrm "PrintId" (make_error_stream "PrintId"))); ("Check", (function | (Coqast.VARG_STRING kind) :: ((Coqast.VARG_CONSTR c) :: g) -> let evmap, env = Vernacentries.get_current_context_of_args g in let f = match kind with | "CHECK" -> print_check | "PRINTTYPE" -> errorlabstrm "PrintType" (str "Not yet supported in CtCoq") | _ -> errorlabstrm "CHECK" (make_error_stream "CHECK") in (function () -> let a,b = f (c, judgment_of_rawconstr evmap env c) in output_results a b) | _ -> errorlabstrm "CHECK" (make_error_stream "CHECK"))); ("Eval", (function | Coqast.VARG_TACTIC_ARG(Redexp redexp):: Coqast.VARG_CONSTR c :: g -> let evmap, env = Vernacentries.get_current_context_of_args g in let redfun = ct_print_eval (Ctast.ast_to_ct c) (Tacred.reduction_of_redexp redexp env evmap) env in fun () -> let strm, vtp = redfun evmap (judgment_of_rawconstr evmap env c) in output_results strm vtp | _ -> errorlabstrm "Eval" (make_error_stream "Eval"))); ("Centaur_Reset", (function | (Coqast.VARG_IDENTIFIER c) :: [] -> if refining () then output_results (ctf_AbortedAllMessage ()) None; current_proof_name := ""; (match string_of_id c with | "CtCoqInitialState" -> (function () -> current_proof_name := ""; Vernacentries.abort_refine Lib.reset_initial (); output_results (ctf_ResetInitialMessage ()) None) | _ -> (function () -> current_proof_name := ""; Vernacentries.abort_refine Lib.reset_name c; output_results (ctf_ResetIdentMessage !global_request_id (string_of_id c)) None)) | _ -> errorlabstrm "Centaur_Reset" (make_error_stream "Centaur_Reset"))); ("Show_dad_rules", (function | [] -> (fun () -> let results = dad_rule_names() in output_results (ctf_header "dad_rule_names" !global_request_id) (Some (P_ids (CT_id_list (List.map (fun s -> CT_ident s) results))))) | _ -> errorlabstrm "Show_dad_rules" (make_error_stream "Show_dad_rules"))); ("INSPECT", (function | [Coqast.VARG_NUMBER n] -> (function () -> inspect n) | _ -> errorlabstrm "INSPECT" (make_error_stream "INSPECT"))) ];; *) (* let non_debug_changes = [ ("SHOW", (function | [Coqast.VARG_NUMBER n] -> (function () -> show_nth n) | _ -> errorlabstrm "SHOW" (make_error_stream "SHOW")))];; *) (* Moved to Vernacentries... let command_creations = [ ("Comments", function l -> (fun () -> message ("Comments ok\n"))); (* Dead code ("CommentsBold", function l -> (fun () -> message ("CommentsBold ok\n"))); ("Title", function l -> (fun () -> message ("Title ok\n"))); ("Author", function l -> (fun () -> message ("Author ok\n"))); ("Note", function l -> (fun () -> message ("Note ok\n"))); ("NL", function l -> (fun () -> message ("Newline ok\n"))) *) ];; *) TACTIC EXTEND Pbp | [ "Pbp" ident_opt(idopt) natural_list(nl) ] -> [ if_pcoq pbp_tac_pcoq idopt nl ] END (* <\cpa> TACTIC EXTEND Blast | [ "Blast" ne_natural_list(nl) ] -> [ if_pcoq blast_tac_pcoq nl ] END TACTIC EXTEND Dad | [ "Dad" natural_list(nl1) "to" natural_list(nl2) ] -> [ if_pcoq dad_tac_pcoq nl1 nl2 ] END *) TACTIC EXTEND CtDebugTac | [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ] END TACTIC EXTEND CtDebugTac2 | [ "DebugTac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ] END let start_pcoq_mode debug = begin pcoq_started := Some debug; (* <\cpa> start_dad(); *) declare_in_coq(); (* add_tactic "PcoqPbp" pbp_tac_pcoq; add_tactic "PcoqBlast" blast_tac_pcoq; add_tactic "Dad" dad_tac_pcoq; add_tactic "CtDebugTac" debug_tac2_pcoq; add_tactic "CtDebugTac2" debug_tac2_pcoq; *) (* The following ones are added to enable rich comments in pcoq *) (* TODO ... add_tactic "Image" (fun _ -> tclIDTAC); *) (* "Comments" moved to Vernacentries, other obsolete ? List.iter (fun (a,b) -> vinterp_add a b) command_creations; *) (* Now hooks in Vernacentries List.iter (fun (a,b) -> overwriting_vinterp_add a b) command_changes; if not debug then List.iter (fun (a,b) -> overwriting_vinterp_add a b) non_debug_changes; *) set_pcoq_hook pcoq_hook; end;; let start_pcoq () = start_pcoq_mode false; set_acknowledge_command ctf_acknowledge_command; set_start_marker "CENTAUR_RESERVED_TOKEN_start_command"; set_end_marker "CENTAUR_RESERVED_TOKEN_end_command"; raise Vernacexpr.ProtectedLoop;; let start_pcoq_debug () = start_pcoq_mode true; set_acknowledge_command ctf_acknowledge_command; set_start_marker "--->"; set_end_marker "<---"; raise Vernacexpr.ProtectedLoop;; VERNAC COMMAND EXTEND StartPcoq [ "Start" "Pcoq" "Mode" ] -> [ start_pcoq () ] END VERNAC COMMAND EXTEND Pcoq_inspect [ "Pcoq_inspect" ] -> [ inspect 15 ] END VERNAC COMMAND EXTEND StartPcoqDebug | [ "Start" "Pcoq" "Debug" "Mode" ] -> [ start_pcoq_debug () ] END