(*i camlp4deps: "parsing/grammar.cma" i*) (* * This file has been modified by Lionel Elie Mamane * to implement the following features * - Terms (optionally) as pretty-printed string and not trees * - (Optionally) give most commands their usual Coq semantics * - Add the backtracking information to the status message. * in the following time period * - May-November 2006 * and * - Make use of new Command.save_hook to generate dependencies at * save-time. * in * - June 2007 *) (*Toplevel loop for the communication between Coq and Centaur *) open Names;; open Nameops;; open Util;; open Term;; open Pp;; open Ppconstr;; open Prettyp;; open Libnames;; open Libobject;; open Library;; open Vernacinterp;; open Evd;; open Proof_trees;; 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 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;; open Printer;; 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 pcoq_history = ref true;; let assert_pcoq_history f a = if !pcoq_history then f a else error "Pcoq-style history tracking deactivated";; 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());; 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) ++ (str "e\nblabla\n");; (*Message functions, the text of these messages is recognized by the protocols *) (*of CtCoq *) let ctf_header message_name request_id = 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, !current_goal_index else (0, 0) and statnum = Lib.current_command_label () and dpth = let d = Pfedit.current_proof_depth() in if d >= 0 then d else 0 and pending = CT_id_list (List.map xlate_ident (Pfedit.get_all_proof_names())) in (ctf_header "acknowledge" request_id ++ int command_count ++ fnl() ++ int goal_count ++ fnl () ++ int goal_index ++ fnl () ++ str (current_proof_name()) ++ fnl() ++ int statnum ++ fnl() ++ print_tree (P_ids pending) ++ int dpth ++ 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_GoalsReqIdMessage = ctf_header "goals_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();; 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 -> mt()));; 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 output_results (ctf_GoalReqIdMessage !global_request_id ++ pr_nth_open_subgoal n) None with | Invalid_argument s -> error "No focused proof (No proof-editing in progress)";; let show_subgoals () = try output_results (ctf_GoalReqIdMessage !global_request_id ++ pr_open_subgoals ()) None 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 env judg = ((ctf_SearchResults !global_request_id) ++ print_judgment env judg, None);; let ct_print_eval red_fun env evmap ast judg = (if refining() then traverse_to []); let {uj_val=value; uj_type=typ} = judg in let nvalue = (red_fun env evmap) value (* // Attention , ici il faut peut être utiliser des environnemenst locaux *) and ntyp = nf_betaiota typ in print_tree (P_pl (CT_premises_list [CT_eval_result (xlate_formula ast, translate_constr false env nvalue, translate_constr false env ntyp)]));; 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 () = (* LEM: See comments for pcoq_search *) 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 () ++ Printer.pr_goal (sig_it g) ++ fnl () ++ str "the tactic is" ++ fnl () ++ Pptactic.pr_glob_tactic (Global.env()) tac) (* Caution, this is in the middle of what looks like dead code. ; 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) = Global.lookup_named (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), "CONSTANT" -> let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in add_search2 (Nametab.locate (qualid_of_sp sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_sp sp)) (Pretyping.Default.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) ] -> [ assert_pcoq_history (simulate_solve n) tac ] END VERNAC COMMAND EXTEND KillProofAfter | [ "Kill" "Proof" "after" natural(n) ] -> [ assert_pcoq_history kill_node_verbose n ] END VERNAC COMMAND EXTEND KillProofAt | [ "Kill" "Proof" "at" natural(n) ] -> [ assert_pcoq_history kill_node_verbose n ] END VERNAC COMMAND EXTEND KillSubProof [ "Kill" "SubProof" natural(n) ] -> [ assert_pcoq_history 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 () = if !pcoq_history then History.start_proof (current_proof_name()); current_goal_index := 1 let solve_hook n = current_goal_index := n; if !pcoq_history then 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 History.push_command name n n_goals let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s) let interp_search_about_item = function | SearchRef qid -> GlobSearchRef (Nametab.global qid) | SearchString s -> GlobSearchString s let pcoq_search s l = (* LEM: I don't understand why this is done in this way (redoing the * match on s here) instead of making the code in * parsing/search.ml call the right function instead of * "plain_display". Investigates this later. * TODO *) ctv_SEARCH_LIST:=[]; begin match s with | SearchAbout sl -> raw_search_about (filter_by_module_from_list l) add_search (List.map interp_search_about_item sl) | 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() (* Check sequentially whether the pattern is one of the premises *) let rec hyp_pattern_filter pat name a c = let _c1 = strip_outer_cast c in match kind_of_term c with | Prod(_, hyp, c2) -> (try (* let _ = msgnl ((str "WHOLE ") ++ (Printer.pr_lconstr c)) in let _ = msgnl ((str "PAT ") ++ (Printer.pr_pattern pat)) in *) if Matching.is_matching pat hyp then (msgnl (str "ok"); true) else false with UserError _ -> false) or hyp_pattern_filter pat name a c2 | _ -> false;; let hyp_search_pattern c l = let _, pat = interp_constrpattern Evd.empty (Global.env()) c in ctv_SEARCH_LIST := []; gen_filtered_search (fun s a c -> (filter_by_module_from_list l s a c && (if hyp_pattern_filter pat s a c then (msgnl (str "ok2"); true) else false))) (fun s a c -> (msgnl (str "ok3"); add_search s a c)); output_results (ctf_SearchResults !global_request_id) (Some (P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));; let pcoq_print_name ref = output_results (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl () ++ print_name ref ) None let pcoq_print_check env j = let a,b = print_check env j in output_results a b let pcoq_print_eval redfun env evmap c j = output_results (ctf_SearchResults !global_request_id ++ Prettyp.print_eval redfun env evmap c j) None;; open Vernacentries let pcoq_show_goal = function | Some n -> show_nth n | None -> show_subgoals () ;; 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 pcoq_term_pr = { pr_constr_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_constr_expr c)); (* In future translate_constr false (Global.env()) * Except with right bool/env which I'll get :) *) pr_lconstr_expr = (fun c -> fFORMULA (xlate_formula c) ++ str "(pcoq_lconstr_expr of " ++ (default_term_pr.pr_lconstr_expr c) ++ str ")"); pr_pattern_expr = (fun c -> str "pcoq_pattern_expr\n" ++ (default_term_pr.pr_pattern_expr c)); pr_lpattern_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_lpattern_expr c)) } let start_pcoq_trees () = set_term_pr pcoq_term_pr (* BEGIN functions for object_pr *) (* These functions in general mirror what name_to_ast does in a subcase, and then print the corresponding object as a PCoq tree. *) let object_to_ast_template object_to_ast_list sp = let l = object_to_ast_list sp in VernacList (List.map (fun x -> (dummy_loc, x)) l) let pcoq_print_object_template object_to_ast_list sp = let results = xlate_vernac_list (object_to_ast_template object_to_ast_list sp) in print_tree (P_cl results) (* This function mirror what print_check does *) let pcoq_print_typed_value_in_env env (value, typ) = let value_ct_ast = (try translate_constr false (Global.env()) value with UserError(f,str) -> raise(UserError(f,Printer.pr_lconstr value ++ fnl () ++ str ))) in let type_ct_ast = (try translate_constr false (Global.env()) typ with UserError(f,str) -> raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in print_tree (P_pl (CT_premises_list [CT_coerce_TYPED_FORMULA_to_PREMISE (CT_typed_formula(value_ct_ast,type_ct_ast) )])) ;; (* This function mirrors what show_nth does *) let pcoq_pr_subgoal n gl = try print_tree (if (!text_proof_flag<>"off") then (* This is a horrendeous hack; it ignores the "gl" argument and just takes the currently focused proof. This will bite us back one day. TODO: Fix this. *) ( if not !pcoq_history then error "Text mode requires Pcoq history tracking."; if n=0 then (P_text (show_proof !text_proof_flag [])) else let path = History.get_nth_open_path (current_proof_name()) n in (P_text (show_proof !text_proof_flag path))) else (let goal = List.nth gl (n - 1) in (P_r (translate_goal goal)))) with | Invalid_argument _ | Failure "nth" | Not_found -> error "No such goal";; let pcoq_pr_subgoals close_cmd evar gl = (*LEM: TODO: we should check for evar emptiness or not, and do something *) try print_tree (if (!text_proof_flag<>"off") then raise (Anomaly ("centaur.ml4:pcoq_pr_subgoals", str "Text mode show all subgoals not implemented")) else (P_rl (translate_goals gl))) with | Invalid_argument _ | Failure "nth" | Not_found -> error "No such goal";; (* END functions for object_pr *) let pcoq_object_pr = { print_inductive = pcoq_print_object_template inductive_to_ast_list; (* TODO: Check what that with_infos means, and adapt accordingly *) print_constant_with_infos = pcoq_print_object_template constant_to_ast_list; print_section_variable = pcoq_print_object_template variable_to_ast_list; print_syntactic_def = pcoq_print_object_template (fun x -> errorlabstrm "print" (str "printing of syntax definitions not implemented in PCoq syntax")); (* TODO: These are placeholders only; write them *) print_module = (fun x y -> str "pcoq_print_module not implemented"); print_modtype = (fun x -> str "pcoq_print_modtype not implemented"); print_named_decl = (fun x -> str "pcoq_print_named_decl not implemented"); (* TODO: Find out what the first argument x (a bool) is about and react accordingly *) print_leaf_entry = (fun x -> pcoq_print_object_template leaf_entry_to_ast_list); print_library_entry = (fun x y -> Some (str "pcoq_print_library_entry not implemented")); print_context = (fun x y z -> str "pcoq_print_context not implemented"); print_typed_value_in_env = pcoq_print_typed_value_in_env; Prettyp.print_eval = ct_print_eval; };; let pcoq_printer_pr = { pr_subgoals = pcoq_pr_subgoals; pr_subgoal = pcoq_pr_subgoal; pr_goal = (fun x -> str "pcoq_pr_goal not implemented"); };; let start_pcoq_objects () = set_object_pr pcoq_object_pr; set_printer_pr pcoq_printer_pr let start_default_objects () = set_object_pr default_object_pr; set_printer_pr default_printer_pr let full_name_of_ref r = (match r with | VarRef _ -> str "VAR" | ConstRef _ -> str "CST" | IndRef _ -> str "IND" | ConstructRef _ -> str "CSR") ++ str " " ++ (pr_sp (Nametab.sp_of_global r)) (* LEM TODO: Cleanly separate path from id (see Libnames.string_of_path) *) let string_of_ref = (*LEM TODO: Will I need the Var/Const/Ind/Construct info?*) Depends.o Libnames.string_of_path Nametab.sp_of_global let print_depends compute_depends ptree = output_results (List.fold_left (fun x y -> x ++ (full_name_of_ref y) ++ fnl()) (str "This object depends on:" ++ fnl()) (compute_depends ptree)) None let output_depends compute_depends ptree = (* Using an ident list for that is arguably stretching it, but less effort than touching the vtp types *) output_results (ctf_header "depends" !global_request_id ++ print_tree (P_ids (CT_id_list (List.map (fun x -> CT_ident (string_of_ref x)) (compute_depends ptree))))) None let gen_start_depends_dumps print_depends print_depends' print_depends'' print_depends''' = Command.set_declare_definition_hook (print_depends' (Depends.depends_of_definition_entry ~acc:[])); Command.set_declare_assumption_hook (print_depends (fun (c:types) -> Depends.depends_of_constr c [])); Command.set_start_hook (print_depends (fun c -> Depends.depends_of_constr c [])); Command.set_save_hook (print_depends'' (Depends.depends_of_pftreestate Depends.depends_of_pftree)); Refiner.set_solve_hook (print_depends''' (fun pt -> Depends.depends_of_pftree_head pt [])) let start_depends_dumps () = gen_start_depends_dumps output_depends output_depends output_depends output_depends let start_depends_dumps_debug () = gen_start_depends_dumps print_depends print_depends print_depends print_depends TACTIC EXTEND pbp | [ "pbp" ident_opt(idopt) natural_list(nl) ] -> [ if_pcoq pbp_tac_pcoq idopt nl ] END TACTIC EXTEND ct_debugtac | [ "debugtac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ] END TACTIC EXTEND ct_debugtac2 | [ "debugtac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ] END let start_pcoq_mode debug = begin pcoq_started := Some debug; (* <\cpa> start_dad(); *) (* 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; start_pcoq_objects(); Flags.print_emacs := false; Pp.make_pp_nonemacs(); 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 HypSearchPattern [ "HypSearchPattern" constr(pat) ] -> [ hyp_search_pattern pat ([], false) ] END 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 VERNAC COMMAND EXTEND StartPcoqTerms | [ "Start" "Pcoq" "Trees" ] -> [ start_pcoq_trees () ] END VERNAC COMMAND EXTEND StartPcoqObjects | [ "Start" "Pcoq" "Objects" ] -> [ start_pcoq_objects () ] END VERNAC COMMAND EXTEND StartDefaultObjects | [ "Start" "Default" "Objects" ] -> [ start_default_objects () ] END VERNAC COMMAND EXTEND StartDependencyDumps | [ "Start" "Dependency" "Dumps" ] -> [ start_depends_dumps () ] END VERNAC COMMAND EXTEND StopPcoqHistory | [ "Stop" "Pcoq" "History" ] -> [ pcoq_history := false ] END