1
(*i camlp4deps: "parsing/grammar.cma" i*)
4
* This file has been modified by Lionel Elie Mamane <lionel@mamane.lu>
5
* to implement the following features
6
* - Terms (optionally) as pretty-printed string and not trees
7
* - (Optionally) give most commands their usual Coq semantics
8
* - Add the backtracking information to the status message.
9
* in the following time period
12
* - Make use of new Command.save_hook to generate dependencies at
18
(*Toplevel loop for the communication between Coq and Centaur *)
45
open Protectedtoplevel;;
46
open Line_oriented_parser;;
65
let pcoq_started = ref None;;
68
if !pcoq_started <> None then f a else error "Pcoq is not started";;
70
let text_proof_flag = ref "en";;
72
let pcoq_history = ref true;;
74
let assert_pcoq_history f a =
75
if !pcoq_history then f a else error "Pcoq-style history tracking deactivated";;
77
let current_proof_name () =
79
string_of_id (get_current_proof_name ())
81
UserError("Pfedit.get_proof", _) -> "";;
83
let current_goal_index = ref 0;;
85
let guarded_force_eval_stream (s : std_ppcmds) =
87
let f elt = l:= elt :: !l in
88
(try Stream.iter f s with
89
| _ -> f (Stream.next (str "error guarded_force_eval_stream")));
90
Stream.of_list (List.rev !l);;
93
let rec string_of_path p =
94
match p with [] -> "\n"
95
| i::p -> (string_of_int i)^" "^ (string_of_path p)
98
output_results_nl (str "Path:" ++ str (string_of_path p))
101
let kill_proof_node index =
102
let paths = History.historical_undo (current_proof_name()) index in
104
(fun path -> (traverse_to path;
105
Pfedit.mutate weak_undo_pftreestate;
108
History.border_length (current_proof_name());;
112
| P_rl of ct_RULE_LIST
114
| P_s_int of ct_SIGNED_INT_LIST
115
| P_pl of ct_PREMISES_LIST
116
| P_cl of ct_COMMAND_LIST
117
| P_t of ct_TACTIC_COM
119
| P_ids of ct_ID_LIST;;
123
| P_rl x -> fRULE_LIST x
125
| P_s_int x -> fSIGNED_INT_LIST x
126
| P_pl x -> fPREMISES_LIST x
127
| P_cl x -> fCOMMAND_LIST x
128
| P_t x -> fTACTIC_COM x
129
| P_text x -> fTEXT x
130
| P_ids x -> fID_LIST x)
131
++ (str "e\nblabla\n");;
134
(*Message functions, the text of these messages is recognized by the protocols *)
136
let ctf_header message_name request_id =
137
str "message" ++ fnl() ++ str message_name ++ fnl() ++
138
int request_id ++ fnl();;
140
let ctf_acknowledge_command request_id command_count opt_exn =
141
let goal_count, goal_index =
145
(fst (frontier (proof_of_pftreestate (get_pftreestate ())))) in
146
g_count, !current_goal_index
149
and statnum = Lib.current_command_label ()
150
and dpth = let d = Pfedit.current_proof_depth() in if d >= 0 then d else 0
151
and pending = CT_id_list (List.map xlate_ident (Pfedit.get_all_proof_names())) in
152
(ctf_header "acknowledge" request_id ++
153
int command_count ++ fnl() ++
154
int goal_count ++ fnl () ++
155
int goal_index ++ fnl () ++
156
str (current_proof_name()) ++ fnl() ++
157
int statnum ++ fnl() ++
158
print_tree (P_ids pending) ++
161
Some e -> Cerrors.explain_exn e
162
| None -> mt ()) ++ fnl() ++ str "E-n-d---M-e-s-s-a-g-e" ++ fnl ());;
164
let ctf_undoResults = ctf_header "undo_results";;
166
let ctf_TextMessage = ctf_header "text_proof";;
168
let ctf_SearchResults = ctf_header "search_results";;
170
let ctf_OtherGoal = ctf_header "other_goal";;
172
let ctf_Location = ctf_header "location";;
174
let ctf_StateMessage = ctf_header "state";;
176
let ctf_PathGoalMessage () =
177
fnl () ++ str "message" ++ fnl () ++ str "single_goal" ++ fnl ();;
179
let ctf_GoalReqIdMessage = ctf_header "single_goal_state";;
181
let ctf_GoalsReqIdMessage = ctf_header "goals_state";;
183
let ctf_NewStateMessage = ctf_header "fresh_state";;
185
let ctf_SavedMessage () = fnl () ++ str "message" ++ fnl () ++
186
str "saved" ++ fnl();;
188
let ctf_KilledMessage req_id ngoals =
189
ctf_header "killed" req_id ++ int ngoals ++ fnl ();;
191
let ctf_AbortedAllMessage () =
192
fnl() ++ str "message" ++ fnl() ++ str "aborted_all" ++ fnl();;
194
let ctf_AbortedMessage request_id na =
195
ctf_header "aborted_proof" request_id ++ str na ++ fnl () ++
196
str "E-n-d---M-e-s-s-a-g-e" ++ fnl ();;
198
let ctf_UserErrorMessage request_id stream =
199
let stream = guarded_force_eval_stream stream in
200
ctf_header "user_error" request_id ++ stream ++ fnl() ++
201
str "E-n-d---M-e-s-s-a-g-e" ++ fnl();;
203
let ctf_ResetInitialMessage () =
204
fnl () ++ str "message" ++ fnl () ++ str "reset_initial" ++ fnl ();;
206
let ctf_ResetIdentMessage request_id s =
207
ctf_header "reset_ident" request_id ++ str s ++ fnl () ++
208
str "E-n-d---M-e-s-s-a-g-e" ++ fnl();;
211
let break_happened = ref false;;
213
let output_results stream vtp_tree =
214
let _ = Sys.signal Sys.sigint
215
(Sys.Signal_handle(fun i -> (break_happened := true;()))) in
218
Some t -> print_tree t
221
let output_results_nl stream =
222
let _ = Sys.signal Sys.sigint
223
(Sys.Signal_handle(fun i -> break_happened := true;()))
229
let _ = Sys.signal Sys.sigint (Sys.Signal_handle(fun i -> raise Sys.Break))
233
if (!break_happened) then
235
break_happened := false;
240
let print_past_goal index =
241
let path = History.get_path_for_rank (current_proof_name()) index in
242
try traverse_to path;
243
let pf = proof_of_pftreestate (get_pftreestate ()) in
244
output_results (ctf_PathGoalMessage ())
245
(Some (P_r (translate_goal pf.goal)))
247
| Invalid_argument s ->
248
((try traverse_to [] with _ -> ());
249
error "No focused proof (No proof-editing in progress)")
250
| e -> (try traverse_to [] with _ -> ()); raise e
255
output_results (ctf_GoalReqIdMessage !global_request_id
256
++ pr_nth_open_subgoal n)
259
| Invalid_argument s ->
260
error "No focused proof (No proof-editing in progress)";;
262
let show_subgoals () =
264
output_results (ctf_GoalReqIdMessage !global_request_id
265
++ pr_open_subgoals ())
268
| Invalid_argument s ->
269
error "No focused proof (No proof-editing in progress)";;
271
(* The rest of the file contains commands that are changed from the plain
274
let ctv_SEARCH_LIST = ref ([] : ct_PREMISE list);;
277
let filter_by_module_from_varg_list l =
278
let dir_list, b = Vernacentries.interp_search_restriction l in
279
Search.filter_by_module_from_list (dir_list, b);;
282
let add_search (global_reference:global_reference) assumptions cstr =
285
string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty
289
CT_premise (CT_ident id_string, translate_constr false assumptions cstr)
291
CT_premise (CT_ident id_string,
292
CT_coerce_ID_to_FORMULA(
293
CT_ident ("Error printing" ^ id_string))) in
294
ctv_SEARCH_LIST:= ast::!ctv_SEARCH_LIST
295
with e -> msgnl (str "add_search raised an exception"); raise e;;
298
let make_error_stream node_string =
299
str "The syntax of " ++ str node_string ++
300
str " is inconsistent with the vernac interpreter entry";;
303
let ctf_EmptyGoalMessage id =
304
fnl () ++ str "Empty Goal is a no-op. Fun oh fun." ++ fnl ();;
307
let print_check env judg =
308
((ctf_SearchResults !global_request_id) ++
309
print_judgment env judg,
312
let ct_print_eval red_fun env evmap ast judg =
313
(if refining() then traverse_to []);
314
let {uj_val=value; uj_type=typ} = judg in
315
let nvalue = (red_fun env evmap) value
316
(* // Attention , ici il faut peut �tre utiliser des environnemenst locaux *)
317
and ntyp = nf_betaiota typ in
323
translate_constr false env nvalue,
324
translate_constr false env ntyp)]));;
327
pbp_tac (function (x:raw_tactic_expr) ->
329
(ctf_header "pbp_results" !global_request_id)
330
(Some (P_t(xlate_tactic x))));;
333
blast_tac (function (x:raw_tactic_expr) ->
335
(ctf_header "pbp_results" !global_request_id)
336
(Some (P_t(xlate_tactic x))));;
340
dad_tac(function x ->
342
(ctf_header "pbp_results" !global_request_id)
343
(Some (P_t(xlate_tactic x))));;
346
let search_output_results () =
347
(* LEM: See comments for pcoq_search *)
349
(ctf_SearchResults !global_request_id)
350
(Some (P_pl (CT_premises_list
351
(List.rev !ctv_SEARCH_LIST))));;
354
let debug_tac2_pcoq tac =
356
let the_goal = ref (None : goal sigma option) in
357
let the_ast = ref tac in
358
let the_path = ref ([] : int list) in
360
let _result = report_error tac the_goal the_ast the_path [] g in
361
(errorlabstrm "DEBUG TACTIC"
362
(str "no error here " ++ fnl () ++ Printer.pr_goal (sig_it g) ++
363
fnl () ++ str "the tactic is" ++ fnl () ++
364
Pptactic.pr_glob_tactic (Global.env()) tac) (*
365
Caution, this is in the middle of what looks like dead code. ;
373
(ctf_Location !global_request_id)
377
(fun n -> CT_coerce_INT_to_SIGNED_INT
380
(List.rev !the_path)))))));
382
(ctf_OtherGoal !global_request_id)
383
(Some (P_r (translate_goal (sig_it g)))));
386
let rec selectinspect n env =
394
(sp, Lib.Leaf lobj) -> a::(selectinspect (n -1 ) tl)
395
| _ -> (selectinspect n tl);;
400
let env = Global.env() in
401
let add_search2 x y = add_search x env y in
402
let l = selectinspect n (Lib.contents_after None) in
403
ctv_SEARCH_LIST := [];
408
oname, Lib.Leaf lobj ->
409
(match oname, object_tag lobj with
410
(sp,_), "VARIABLE" ->
411
let (_, _, v) = Global.lookup_named (basename sp) in
412
add_search2 (Nametab.locate (qualid_of_sp sp)) v
413
| (sp,kn), "CONSTANT" ->
414
let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in
415
add_search2 (Nametab.locate (qualid_of_sp sp)) typ
416
| (sp,kn), "MUTUALINDUCTIVE" ->
417
add_search2 (Nametab.locate (qualid_of_sp sp))
418
(Pretyping.Default.understand Evd.empty (Global.env())
419
(RRef(dummy_loc, IndRef(kn,0))))
420
| _ -> failwith ("unexpected value 1 for "^
421
(string_of_id (basename (fst oname)))))
422
| _ -> failwith "unexpected value")
426
(ctf_SearchResults !global_request_id)
428
(P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));;
430
let ct_int_to_TARG n =
431
CT_coerce_FORMULA_OR_INT_to_TARG
432
(CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
433
(CT_coerce_INT_to_ID_OR_INT (CT_int n)));;
435
let pair_list_to_ct l =
436
CT_user_tac(CT_ident "pair_int_list",
438
(List.map (fun (a,b) ->
439
CT_coerce_TACTIC_COM_to_TARG
441
(CT_ident "pair_int",
443
[ct_int_to_TARG a; ct_int_to_TARG b])))
446
(* Annule toutes les commandes qui s'appliquent sur les sous-buts du
447
but auquel a �t� appliqu�e la n-i�me tactique *)
449
let path = History.get_path_for_rank (current_proof_name()) n in
452
Pfedit.mutate weak_undo_pftreestate;
453
(let kept_cmds, undone_cmds, remaining_goals, current_goal =
454
History.logical_undo (current_proof_name()) n in
455
output_results (ctf_undoResults !global_request_id)
459
(CT_ident "log_undo_result",
461
[CT_coerce_TACTIC_COM_to_TARG (pair_list_to_ct kept_cmds);
462
CT_coerce_TACTIC_COM_to_TARG(pair_list_to_ct undone_cmds);
463
ct_int_to_TARG remaining_goals;
464
ct_int_to_TARG current_goal])))));
468
let simulate_solve n tac =
469
let path = History.get_nth_open_path (current_proof_name()) n in
470
solve_nth n (Tacinterp.hide_interp tac (get_end_tac()));
472
Pfedit.mutate weak_undo_pftreestate;
475
let kill_node_verbose n =
476
let ngoals = kill_proof_node n in
477
output_results_nl (ctf_KilledMessage !global_request_id ngoals)
479
let set_text_mode s = text_proof_flag := s
481
let pcoq_reset_initial() =
482
output_results(ctf_AbortedAllMessage()) None;
483
Vernacentries.abort_refine Lib.reset_initial ();
484
output_results(ctf_ResetInitialMessage()) None;;
488
output_results (ctf_AbortedAllMessage ()) None;
489
Vernacentries.abort_refine Lib.reset_name (dummy_loc,x);
491
(ctf_ResetIdentMessage !global_request_id (string_of_id x)) None;;
494
VERNAC ARGUMENT EXTEND text_mode
495
| [ "fr" ] -> [ "fr" ]
496
| [ "en" ] -> [ "en" ]
497
| [ "Off" ] -> [ "off" ]
500
VERNAC COMMAND EXTEND TextMode
501
| [ "Text" "Mode" text_mode(s) ] -> [ set_text_mode s ]
504
VERNAC COMMAND EXTEND OutputGoal
505
[ "Goal" ] -> [ output_results_nl(ctf_EmptyGoalMessage "") ]
508
VERNAC COMMAND EXTEND OutputGoal
509
[ "Goal" "Cmd" natural(n) "with" tactic(tac) ] -> [ assert_pcoq_history (simulate_solve n) tac ]
512
VERNAC COMMAND EXTEND KillProofAfter
513
| [ "Kill" "Proof" "after" natural(n) ] -> [ assert_pcoq_history kill_node_verbose n ]
516
VERNAC COMMAND EXTEND KillProofAt
517
| [ "Kill" "Proof" "at" natural(n) ] -> [ assert_pcoq_history kill_node_verbose n ]
520
VERNAC COMMAND EXTEND KillSubProof
521
[ "Kill" "SubProof" natural(n) ] -> [ assert_pcoq_history logical_kill n ]
524
VERNAC COMMAND EXTEND PcoqReset
525
[ "Pcoq" "Reset" ident(x) ] -> [ pcoq_reset x ]
528
VERNAC COMMAND EXTEND PcoqResetInitial
529
[ "Pcoq" "ResetInitial" ] -> [ pcoq_reset_initial() ]
532
let start_proof_hook () =
533
if !pcoq_history then History.start_proof (current_proof_name());
534
current_goal_index := 1
537
current_goal_index := n;
538
if !pcoq_history then
539
let name = current_proof_name () in
540
let old_n_count = History.border_length name in
541
let pf = proof_of_pftreestate (get_pftreestate ()) in
542
let n_goals = (List.length (fst (frontier pf))) + 1 - old_n_count in
543
History.push_command name n n_goals
545
let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
547
let interp_search_about_item = function
548
| SearchSubPattern pat ->
549
let _,pat = Constrintern.intern_constr_pattern Evd.empty (Global.env()) pat in
550
GlobSearchSubPattern pat
551
| SearchString (s,_) ->
552
warning "Notation case not taken into account";
555
let pcoq_search s l =
556
(* LEM: I don't understand why this is done in this way (redoing the
557
* match on s here) instead of making the code in
558
* parsing/search.ml call the right function instead of
559
* "plain_display". Investigates this later.
565
raw_search_about (filter_by_module_from_list l) add_search
566
(List.map (on_snd interp_search_about_item) sl)
568
let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
569
raw_pattern_search (filter_by_module_from_list l) add_search pat
571
let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
572
raw_search_rewrite (filter_by_module_from_list l) add_search pat;
573
| SearchHead locqid ->
575
(filter_by_module_from_list l) add_search (Nametab.global locqid)
577
search_output_results()
579
(* Check sequentially whether the pattern is one of the premises *)
580
let rec hyp_pattern_filter pat name a c =
581
let _c1 = strip_outer_cast c in
582
match kind_of_term c with
583
| Prod(_, hyp, c2) ->
585
(* let _ = msgnl ((str "WHOLE ") ++ (Printer.pr_lconstr c)) in
586
let _ = msgnl ((str "PAT ") ++ (Printer.pr_constr_pattern pat)) in *)
587
if Matching.is_matching pat hyp then
588
(msgnl (str "ok"); true)
591
with UserError _ -> false) or
592
hyp_pattern_filter pat name a c2
595
let hyp_search_pattern c l =
596
let _, pat = intern_constr_pattern Evd.empty (Global.env()) c in
597
ctv_SEARCH_LIST := [];
599
(fun s a c -> (filter_by_module_from_list l s a c &&
600
(if hyp_pattern_filter pat s a c then
601
(msgnl (str "ok2"); true) else false)))
602
(fun s a c -> (msgnl (str "ok3"); add_search s a c));
604
(ctf_SearchResults !global_request_id)
606
(P_pl (CT_premises_list (List.rev !ctv_SEARCH_LIST))));;
607
let pcoq_print_name ref =
609
(fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl () ++ print_name ref )
612
let pcoq_print_check env j =
613
let a,b = print_check env j in output_results a b
615
let pcoq_print_eval redfun env evmap c j =
617
(ctf_SearchResults !global_request_id
618
++ Prettyp.print_eval redfun env evmap c j)
623
let pcoq_show_goal = function
624
| Some n -> show_nth n
625
| None -> show_subgoals ()
629
start_proof = start_proof_hook;
632
search = pcoq_search;
633
print_name = pcoq_print_name;
634
print_check = pcoq_print_check;
635
print_eval = pcoq_print_eval;
636
show_goal = pcoq_show_goal
640
pr_constr_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_constr_expr c));
641
(* In future translate_constr false (Global.env())
642
* Except with right bool/env which I'll get :)
644
pr_lconstr_expr = (fun c -> fFORMULA (xlate_formula c) ++ str "(pcoq_lconstr_expr of " ++ (default_term_pr.pr_lconstr_expr c) ++ str ")");
645
pr_constr_pattern_expr = (fun c -> str "pcoq_pattern_expr\n" ++ (default_term_pr.pr_constr_pattern_expr c));
646
pr_lconstr_pattern_expr = (fun c -> str "pcoq_constr_expr\n" ++ (default_term_pr.pr_lconstr_pattern_expr c))
649
let start_pcoq_trees () =
650
set_term_pr pcoq_term_pr
652
(* BEGIN functions for object_pr *)
654
(* These functions in general mirror what name_to_ast does in a subcase,
655
and then print the corresponding object as a PCoq tree. *)
657
let object_to_ast_template object_to_ast_list sp =
658
let l = object_to_ast_list sp in
659
VernacList (List.map (fun x -> (dummy_loc, x)) l)
661
let pcoq_print_object_template object_to_ast_list sp =
662
let results = xlate_vernac_list (object_to_ast_template object_to_ast_list sp) in
663
print_tree (P_cl results)
665
(* This function mirror what print_check does *)
667
let pcoq_print_typed_value_in_env env (value, typ) =
669
(try translate_constr false (Global.env()) value
670
with UserError(f,str) ->
671
raise(UserError(f,Printer.pr_lconstr value ++
674
(try translate_constr false (Global.env()) typ
675
with UserError(f,str) ->
676
raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in
680
[CT_coerce_TYPED_FORMULA_to_PREMISE
681
(CT_typed_formula(value_ct_ast,type_ct_ast)
685
(* This function mirrors what show_nth does *)
687
let pcoq_pr_subgoal n gl =
690
(if (!text_proof_flag<>"off") then
691
(* This is a horrendeous hack; it ignores the "gl" argument
692
and just takes the currently focused proof. This will bite
697
if not !pcoq_history then error "Text mode requires Pcoq history tracking.";
699
then (P_text (show_proof !text_proof_flag []))
701
let path = History.get_nth_open_path (current_proof_name()) n in
702
(P_text (show_proof !text_proof_flag path)))
704
(let goal = List.nth gl (n - 1) in
705
(P_r (translate_goal goal))))
709
| Not_found -> error "No such goal";;
711
let pcoq_pr_subgoals close_cmd evar gl =
712
(*LEM: TODO: we should check for evar emptiness or not, and do something *)
715
(if (!text_proof_flag<>"off") then
716
raise (Anomaly ("centaur.ml4:pcoq_pr_subgoals", str "Text mode show all subgoals not implemented"))
718
(P_rl (translate_goals gl)))
722
| Not_found -> error "No such goal";;
725
(* END functions for object_pr *)
727
let pcoq_object_pr = {
728
print_inductive = pcoq_print_object_template inductive_to_ast_list;
729
(* TODO: Check what that with_infos means, and adapt accordingly *)
730
print_constant_with_infos = pcoq_print_object_template constant_to_ast_list;
731
print_section_variable = pcoq_print_object_template variable_to_ast_list;
732
print_syntactic_def = pcoq_print_object_template (fun x -> errorlabstrm "print"
733
(str "printing of syntax definitions not implemented in PCoq syntax"));
734
(* TODO: These are placeholders only; write them *)
735
print_module = (fun x y -> str "pcoq_print_module not implemented");
736
print_modtype = (fun x -> str "pcoq_print_modtype not implemented");
737
print_named_decl = (fun x -> str "pcoq_print_named_decl not implemented");
738
(* TODO: Find out what the first argument x (a bool) is about and react accordingly *)
739
print_leaf_entry = (fun x -> pcoq_print_object_template leaf_entry_to_ast_list);
740
print_library_entry = (fun x y -> Some (str "pcoq_print_library_entry not implemented"));
741
print_context = (fun x y z -> str "pcoq_print_context not implemented");
742
print_typed_value_in_env = pcoq_print_typed_value_in_env;
743
Prettyp.print_eval = ct_print_eval;
746
let pcoq_printer_pr = {
747
pr_subgoals = pcoq_pr_subgoals;
748
pr_subgoal = pcoq_pr_subgoal;
749
pr_goal = (fun x -> str "pcoq_pr_goal not implemented");
753
let start_pcoq_objects () =
754
set_object_pr pcoq_object_pr;
755
set_printer_pr pcoq_printer_pr
757
let start_default_objects () =
758
set_object_pr default_object_pr;
759
set_printer_pr default_printer_pr
761
let full_name_of_ref r =
763
| VarRef _ -> str "VAR"
764
| ConstRef _ -> str "CST"
765
| IndRef _ -> str "IND"
766
| ConstructRef _ -> str "CSR")
767
++ str " " ++ (pr_sp (Nametab.sp_of_global r))
768
(* LEM TODO: Cleanly separate path from id (see Libnames.string_of_path) *)
771
(*LEM TODO: Will I need the Var/Const/Ind/Construct info?*)
772
Depends.o Libnames.string_of_path Nametab.sp_of_global
774
let print_depends compute_depends ptree =
775
output_results (List.fold_left (fun x y -> x ++ (full_name_of_ref y) ++ fnl())
776
(str "This object depends on:" ++ fnl())
777
(compute_depends ptree))
780
let output_depends compute_depends ptree =
781
(* Using an ident list for that is arguably stretching it, but less effort than touching the vtp types *)
782
output_results (ctf_header "depends" !global_request_id ++
783
print_tree (P_ids (CT_id_list (List.map
784
(fun x -> CT_ident (string_of_ref x))
785
(compute_depends ptree)))))
788
let gen_start_depends_dumps print_depends print_depends' print_depends'' print_depends''' =
789
Command.set_declare_definition_hook (print_depends' (Depends.depends_of_definition_entry ~acc:[]));
790
Command.set_declare_assumption_hook (print_depends (fun (c:types) -> Depends.depends_of_constr c []));
791
Command.set_start_hook (print_depends (fun c -> Depends.depends_of_constr c []));
792
Command.set_save_hook (print_depends'' (Depends.depends_of_pftreestate Depends.depends_of_pftree));
793
Refiner.set_solve_hook (print_depends''' (fun pt -> Depends.depends_of_pftree_head pt []))
795
let start_depends_dumps () = gen_start_depends_dumps output_depends output_depends output_depends output_depends
797
let start_depends_dumps_debug () = gen_start_depends_dumps print_depends print_depends print_depends print_depends
800
| [ "pbp" ident_opt(idopt) natural_list(nl) ] ->
801
[ if_pcoq pbp_tac_pcoq idopt nl ]
804
TACTIC EXTEND ct_debugtac
805
| [ "debugtac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
808
TACTIC EXTEND ct_debugtac2
809
| [ "debugtac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
813
let start_pcoq_mode debug =
815
pcoq_started := Some debug;
819
(* The following ones are added to enable rich comments in pcoq *)
821
add_tactic "Image" (fun _ -> tclIDTAC);
823
(* "Comments" moved to Vernacentries, other obsolete ?
824
List.iter (fun (a,b) -> vinterp_add a b) command_creations;
826
(* Now hooks in Vernacentries
827
List.iter (fun (a,b) -> overwriting_vinterp_add a b) command_changes;
829
List.iter (fun (a,b) -> overwriting_vinterp_add a b) non_debug_changes;
831
set_pcoq_hook pcoq_hook;
832
start_pcoq_objects();
833
Flags.print_emacs := false; Pp.make_pp_nonemacs();
838
start_pcoq_mode false;
839
set_acknowledge_command ctf_acknowledge_command;
840
set_start_marker "CENTAUR_RESERVED_TOKEN_start_command";
841
set_end_marker "CENTAUR_RESERVED_TOKEN_end_command";
842
raise Vernacexpr.ProtectedLoop;;
844
let start_pcoq_debug () =
845
start_pcoq_mode true;
846
set_acknowledge_command ctf_acknowledge_command;
847
set_start_marker "--->";
848
set_end_marker "<---";
849
raise Vernacexpr.ProtectedLoop;;
851
VERNAC COMMAND EXTEND HypSearchPattern
852
[ "HypSearchPattern" constr(pat) ] -> [ hyp_search_pattern pat ([], false) ]
855
VERNAC COMMAND EXTEND StartPcoq
856
[ "Start" "Pcoq" "Mode" ] -> [ start_pcoq () ]
859
VERNAC COMMAND EXTEND Pcoq_inspect
860
[ "Pcoq_inspect" ] -> [ inspect 15 ]
863
VERNAC COMMAND EXTEND StartPcoqDebug
864
| [ "Start" "Pcoq" "Debug" "Mode" ] -> [ start_pcoq_debug () ]
867
VERNAC COMMAND EXTEND StartPcoqTerms
868
| [ "Start" "Pcoq" "Trees" ] -> [ start_pcoq_trees () ]
871
VERNAC COMMAND EXTEND StartPcoqObjects
872
| [ "Start" "Pcoq" "Objects" ] -> [ start_pcoq_objects () ]
875
VERNAC COMMAND EXTEND StartDefaultObjects
876
| [ "Start" "Default" "Objects" ] -> [ start_default_objects () ]
879
VERNAC COMMAND EXTEND StartDependencyDumps
880
| [ "Start" "Dependency" "Dumps" ] -> [ start_depends_dumps () ]
883
VERNAC COMMAND EXTEND StopPcoqHistory
884
| [ "Stop" "Pcoq" "History" ] -> [ pcoq_history := false ]
added
removed
contrib/interface/centaur.ml4
