1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: coq.ml 11948 2009-02-27 16:01:53Z glondu $ *)
29
let prerr_endline s = if !debug then prerr_endline s else ()
31
let output = ref (Format.formatter_of_out_channel stdout)
34
let b = Buffer.create 103 in
35
Pp.msg_with (Format.formatter_of_buffer b) m;
42
(* To hide goal in lower window.
43
Problem: should not hide "xx is assumed"
46
Flags.make_silent true;
47
(* don't set a too large undo stack because Edit.create allocates an array *)
48
Pfedit.set_undo (Some 5000);
55
let get_version_date () =
57
if Glib.Utf8.validate Coq_config.date
59
else "<date not printable>" in
61
let ch = open_in (Coq_config.coqsrc^"/revision") in
62
let ver = input_line ch in
63
let rev = input_line ch in
65
with _ -> (Coq_config.version,date)
67
let short_version () =
68
let (ver,date) = get_version_date () in
69
Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date
72
let (ver,date) = get_version_date () in
74
"The Coq Proof Assistant, version %s (%s)\
75
\nArchitecture %s running %s operating system\
77
\nThis is the %s version (%s is the best one for this architecture and OS)\
80
Coq_config.arch Sys.os_type
81
(let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
82
(if Mltop.is_native then "native" else "bytecode")
83
(if Coq_config.best="opt" then "native" else "bytecode")
85
let is_in_coq_lib dir =
86
prerr_endline ("Is it a coq theory ? : "^dir);
87
let is_same_file = same_file dir in
91
Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in
92
prerr_endline (" Comparing to: "^fdir);
93
if is_same_file fdir then (prerr_endline " YES";true)
94
else (prerr_endline"NO";false))
95
Coq_config.theories_dirs
97
let is_in_loadpath dir =
98
Library.is_in_load_paths (System.physical_path_of_string dir)
100
let is_in_coq_path f =
102
let base = Filename.chop_extension (Filename.basename f) in
103
let _ = Library.locate_qualified_library false
104
(Libnames.make_qualid Names.empty_dirpath
105
(Names.id_of_string base)) in
106
prerr_endline (f ^ " is in coq path");
109
prerr_endline (f ^ " is NOT in coq path");
112
let is_in_proof_mode () =
113
match Decl_mode.get_current_mode () with
114
Decl_mode.Mode_none -> false
117
let user_error_loc l s =
118
raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
120
type printing_state = {
121
mutable printing_implicit : bool;
122
mutable printing_coercions : bool;
123
mutable printing_raw_matching : bool;
124
mutable printing_no_notation : bool;
125
mutable printing_all : bool;
126
mutable printing_evar_instances : bool;
127
mutable printing_universes : bool;
128
mutable printing_full_all : bool
131
let printing_state = {
132
printing_implicit = false;
133
printing_coercions = false;
134
printing_raw_matching = false;
135
printing_no_notation = false;
136
printing_all = false;
137
printing_evar_instances = false;
138
printing_universes = false;
139
printing_full_all = false;
142
let printing_implicit_data = ["Printing";"Implicit"], false
143
let printing_coercions_data = ["Printing";"Coercions"], false
144
let printing_raw_matching_data = ["Printing";"Matching"], true
145
let printing_no_synth_data = ["Printing";"Synth"], true
146
let printing_no_notation_data = ["Printing";"Notations"], true
147
let printing_all_data = ["Printing";"All"], false
148
let printing_evar_instances_data = ["Printing";"Existential";"Instances"],false
149
let printing_universes_data = ["Printing";"Universes"], false
151
let known_options = ref []
153
let prepare_option (l,dft) =
154
known_options := l :: !known_options;
155
let set = (String.concat " " ("Set"::l)) ^ "." in
156
let unset = (String.concat " " ("Unset"::l)) ^ "." in
157
if dft then unset,set else set,unset
159
let coqide_known_option = function
160
| Goptions.TertiaryTable (a,b,c) -> List.mem [a;b;c] !known_options
161
| Goptions.SecondaryTable (a,b) -> List.mem [a;b] !known_options
162
| Goptions.PrimaryTable a -> List.mem [a] !known_options
164
let with_printing_implicit = prepare_option printing_implicit_data
165
let with_printing_coercions = prepare_option printing_coercions_data
166
let with_printing_raw_matching = prepare_option printing_raw_matching_data
167
let with_printing_no_synth = prepare_option printing_no_synth_data
168
let with_printing_no_notation = prepare_option printing_no_notation_data
169
let with_printing_all = prepare_option printing_all_data
170
let with_printing_evar_instances = prepare_option printing_evar_instances_data
171
let with_printing_universes = prepare_option printing_universes_data
173
let make_option_commands () =
174
let p = printing_state in
175
(if p.printing_implicit then [with_printing_implicit] else [])@
176
(if p.printing_coercions then [with_printing_coercions] else [])@
177
(if p.printing_raw_matching then [with_printing_raw_matching;with_printing_no_synth] else [])@
178
(if p.printing_no_notation then [with_printing_no_notation] else [])@
179
(if p.printing_all then [with_printing_all] else [])@
180
(if p.printing_evar_instances then [with_printing_evar_instances] else [])@
181
(if p.printing_universes then [with_printing_universes] else [])@
182
(if p.printing_full_all then [with_printing_all;with_printing_evar_instances;with_printing_universes] else [])
184
let make_option_commands () =
185
let l = make_option_commands () in
186
List.iter (fun (a,b) -> prerr_endline a; prerr_endline b) l;
189
type command_attribute =
190
NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand
191
| OtherStatePreservingCommand | GoalStartingCommand | SolveCommand
194
let rec attribute_of_vernac_command = function
196
| VernacTime com -> attribute_of_vernac_command com
197
| VernacList _ -> [] (* unsupported *)
201
| VernacTacticNotation _ -> []
202
| VernacSyntaxExtension _ -> []
203
| VernacDelimiters _ -> []
204
| VernacBindScope _ -> []
205
| VernacOpenCloseScope _ -> []
206
| VernacArgumentsScope _ -> []
207
| VernacInfix _ -> []
208
| VernacNotation _ -> []
211
| VernacDefinition (_,_,DefineBody _,_) -> []
212
| VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand]
213
| VernacStartTheoremProof _ -> [GoalStartingCommand]
214
| VernacEndProof _ -> [ProofEndingCommand]
215
| VernacExactProof _ -> [ProofEndingCommand]
217
| VernacAssumption _ -> []
218
| VernacInductive _ -> []
219
| VernacFixpoint _ -> []
220
| VernacCoFixpoint _ -> []
221
| VernacScheme _ -> []
222
| VernacCombinedScheme _ -> []
225
| VernacDeclareModule _ -> []
226
| VernacDefineModule _ -> []
227
| VernacDeclareModuleType _ -> []
228
| VernacInclude _ -> []
230
(* Gallina extensions *)
231
| VernacBeginSection _ -> []
232
| VernacEndSegment _ -> []
233
| VernacRequire _ -> []
234
| VernacImport _ -> []
235
| VernacCanonical _ -> []
236
| VernacCoercion _ -> []
237
| VernacIdentityCoercion _ -> []
240
| VernacInstance _ -> []
241
| VernacContext _ -> []
242
| VernacDeclareInstance _ -> []
245
| VernacSolve _ -> [SolveCommand]
246
| VernacSolveExistential _ -> [SolveCommand]
249
| VernacDeclProof -> [SolveCommand]
250
| VernacReturn -> [SolveCommand]
251
| VernacProofInstr _ -> [SolveCommand]
253
(* Auxiliary file and library management *)
254
| VernacRequireFrom _ -> []
255
| VernacAddLoadPath _ -> []
256
| VernacRemoveLoadPath _ -> []
257
| VernacAddMLPath _ -> []
258
| VernacDeclareMLModule _ -> []
259
| VernacChdir _ -> [OtherStatePreservingCommand]
261
(* State management *)
262
| VernacWriteState _ -> []
263
| VernacRestoreState _ -> []
266
| VernacRemoveName _ -> [NavigationCommand]
267
| VernacResetName _ -> [NavigationCommand]
268
| VernacResetInitial -> [NavigationCommand]
269
| VernacBack _ -> [NavigationCommand]
270
| VernacBackTo _ -> [NavigationCommand]
273
| VernacDeclareTacticDefinition _ -> []
274
| VernacCreateHintDb _ -> []
275
| VernacHints _ -> []
276
| VernacSyntacticDefinition _ -> []
277
| VernacDeclareImplicits _ -> []
278
| VernacReserve _ -> []
279
| VernacSetOpacity _ -> []
280
| VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) ->
282
| VernacSetOption (o,BoolValue true) | VernacUnsetOption o ->
283
if coqide_known_option o then [KnownOptionCommand] else []
284
| VernacSetOption _ -> []
285
| VernacRemoveOption _ -> []
286
| VernacAddOption _ -> []
287
| VernacMemOption _ -> [QueryCommand]
289
| VernacPrintOption _ -> [QueryCommand]
290
| VernacCheckMayEval _ -> [QueryCommand]
291
| VernacGlobalCheck _ -> [QueryCommand]
292
| VernacPrint _ -> [QueryCommand]
293
| VernacSearch _ -> [QueryCommand]
294
| VernacLocate _ -> [QueryCommand]
296
| VernacComments _ -> [OtherStatePreservingCommand]
297
| VernacNop -> [OtherStatePreservingCommand]
299
(* Proof management *)
300
| VernacGoal _ -> [GoalStartingCommand]
302
| VernacAbort _ -> [NavigationCommand]
303
| VernacAbortAll -> [NavigationCommand]
304
| VernacRestart -> [NavigationCommand]
305
| VernacSuspend -> [NavigationCommand]
306
| VernacResume _ -> [NavigationCommand]
307
| VernacUndo _ -> [NavigationCommand]
308
| VernacUndoTo _ -> [NavigationCommand]
309
| VernacBacktrack _ -> [NavigationCommand]
311
| VernacFocus _ -> [SolveCommand]
312
| VernacUnfocus -> [SolveCommand]
314
| VernacShow _ -> [OtherStatePreservingCommand]
315
| VernacCheckGuard -> [OtherStatePreservingCommand]
316
| VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand]
317
| VernacProof _ -> []
319
(* Toplevel control *)
320
| VernacToplevelControl _ -> []
323
| VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
324
| VernacExtend _ -> []
326
let is_vernac_goal_starting_command com =
327
List.mem GoalStartingCommand (attribute_of_vernac_command com)
329
let is_vernac_navigation_command com =
330
List.mem NavigationCommand (attribute_of_vernac_command com)
332
let is_vernac_query_command com =
333
List.mem QueryCommand (attribute_of_vernac_command com)
335
let is_vernac_known_option_command com =
336
List.mem KnownOptionCommand (attribute_of_vernac_command com)
338
let is_vernac_debug_command com =
339
List.mem DebugCommand (attribute_of_vernac_command com)
341
let is_vernac_goal_printing_command com =
342
let attribute = attribute_of_vernac_command com in
343
List.mem GoalStartingCommand attribute or
344
List.mem SolveCommand attribute
346
let is_vernac_state_preserving_command com =
347
let attribute = attribute_of_vernac_command com in
348
List.mem OtherStatePreservingCommand attribute or
349
List.mem QueryCommand attribute
351
let is_vernac_tactic_command com =
352
List.mem SolveCommand (attribute_of_vernac_command com)
354
let is_vernac_proof_ending_command com =
355
List.mem ProofEndingCommand (attribute_of_vernac_command com)
357
type undo_info = identifier list
359
let undo_info () = Pfedit.get_all_proof_names ()
362
| ResetToId of Names.identifier (* Relying on identifiers only *)
363
| ResetToState of Libnames.object_name (* Relying on states if any *)
367
| ResetAtSegmentStart of Names.identifier
368
| ResetAtRegisteredObject of reset_mark
370
type reset_info = reset_status * undo_info * bool ref
373
let reset_mark id = match Lib.has_top_frozen_state () with
375
prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
377
| None -> ResetToId id
379
let compute_reset_info = function
380
| VernacBeginSection id
381
| VernacDefineModule (_,id, _, _, _)
382
| VernacDeclareModule (_,id, _, _)
383
| VernacDeclareModuleType (id, _, _) ->
384
ResetAtSegmentStart (snd id), undo_info(), ref true
386
| VernacDefinition (_, (_,id), DefineBody _, _)
387
| VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
388
| VernacInductive (_, (((_,(_,id)),_,_,_,_),_) :: _) ->
389
ResetAtRegisteredObject (reset_mark id), undo_info(), ref true
391
| com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true
392
| VernacEndSegment _ -> NoReset, undo_info(), ref true
394
| com when is_vernac_tactic_command com -> NoReset, undo_info(), ref true
396
(match Lib.has_top_frozen_state () with
398
prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
399
ResetAtRegisteredObject (ResetToState sp)
400
| None -> NoReset), undo_info(), ref true
402
let reset_initial () =
403
prerr_endline "Reset initial called"; flush stderr;
404
Vernacentries.abort_refine Lib.reset_initial ()
406
let reset_to = function
408
prerr_endline ("Reset called with "^(string_of_id id));
409
Lib.reset_name (Util.dummy_loc,id)
412
("Reset called with state "^(Libnames.string_of_path (fst sp)));
413
Lib.reset_to_state sp
415
let reset_to_mod id =
416
prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id));
417
Lib.reset_mod (Util.dummy_loc,id)
420
Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s))
422
let interp_with_options verbosely options s =
423
prerr_endline "Starting interp...";
425
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
426
let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in
427
(* Temporary hack to make coqide.byte work (WTF???) *)
428
Pervasives.prerr_endline "";
430
| None -> assert false
431
| Some((loc,vernac) as last) ->
432
if is_vernac_debug_command vernac then
433
user_error_loc loc (str "Debug mode not available within CoqIDE");
434
if is_vernac_navigation_command vernac then
435
user_error_loc loc (str "Use CoqIDE navigation instead");
436
if is_vernac_known_option_command vernac then
437
user_error_loc loc (str "Use CoqIDE display menu instead");
438
if is_vernac_query_command vernac then
440
"Warning: query commands should not be inserted in scripts";
441
if not (is_vernac_goal_printing_command vernac) then
442
(* Verbose if in small step forward and not a tactic *)
443
Flags.make_silent (not verbosely);
444
let reset_info = compute_reset_info vernac in
445
List.iter (fun (set_option,_) -> raw_interp set_option) options;
447
Flags.make_silent true;
448
List.iter (fun (_,unset_option) -> raw_interp unset_option) options;
449
prerr_endline ("...Done with interp of : "^s);
452
let interp verbosely phrase =
453
interp_with_options verbosely (make_option_commands ()) phrase
455
let interp_and_replace s =
456
let result = interp false s in
457
let msg = read_stdout () in
461
List.length (fst (Refiner.frontier (Tacmach.proof_of_pftreestate pf)))
465
| Success of int (* nb of goals after *)
468
let try_interptac s =
470
prerr_endline ("Starting try_interptac: "^s);
471
let pf = get_pftreestate () in
472
let pe = Pcoq.Gram.Entry.parse
474
(Pcoq.Gram.parsable (Stream.of_string s))
476
| Some (loc,(VernacSolve (n, tac, _))) ->
477
let tac = Tacinterp.interp tac in
478
let pf' = solve_nth_pftreestate n tac pf in
479
prerr_endline "Success";
480
let nb_goals = nb_subgoals pf' - nb_subgoals pf in
483
prerr_endline "try_interptac: not a tactic"; Failed
485
| Sys.Break | Stdpp.Exc_located (_,Sys.Break)
486
-> prerr_endline "try_interp: interrupted"; Interrupted
487
| Stdpp.Exc_located (_,e) -> prerr_endline ("try_interp: failed ("^(Printexc.to_string e)); Failed
490
let rec is_pervasive_exn = function
491
| Out_of_memory | Stack_overflow | Sys.Break -> true
492
| Error_in_file (_,_,e) -> is_pervasive_exn e
493
| Stdpp.Exc_located (_,e) -> is_pervasive_exn e
494
| DuringCommandInterp (_,e) -> is_pervasive_exn e
497
let print_toplevel_error exc =
500
| DuringCommandInterp (loc,ie) ->
501
if loc = dummy_loc then (None,ie) else (Some loc, ie)
506
| Stdpp.Exc_located (loc, ie) -> (Some loc),ie
507
| Error_in_file (s, (_,fname, loc), ie) -> None, ie
511
| End_of_input -> str "Please report: End of input",None
512
| Vernacexpr.ProtectedLoop ->
513
str "ProtectedLoop not allowed by coqide!",None
514
| Vernacexpr.Drop -> str "Drop is not allowed by coqide!",None
515
| Vernacexpr.Quit -> str "Quit is not allowed by coqide! Use menus.",None
517
(try Cerrors.explain_exn exc with e ->
518
str "Failed to explain error. This is an internal Coq error. Please report.\n"
519
++ str (Printexc.to_string e)),
520
(if is_pervasive_exn exc then None else loc)
522
let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
524
let interp_last last =
527
vernac_com (States.with_heavy_rollback Vernacentries.interp) last;
528
Lib.add_frozen_state()
530
let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s);
534
type hyp = env * evar_map *
535
((identifier * string) * constr option * constr) *
537
type concl = env * evar_map * constr * string
538
type meta = env * evar_map * string
539
type goal = hyp list * concl
541
let prepare_hyp sigma env ((i,c,d) as a) =
543
((i,string_of_id i),c,d),
544
(msg (pr_var_decl env a), msg (pr_ltype_env env d))
546
let prepare_hyps sigma env =
547
assert (rel_context env = []);
550
(fun env d acc -> let hyp = prepare_hyp sigma env d in hyp :: acc)
555
let prepare_goal_main sigma g =
556
let env = evar_env g in
557
(prepare_hyps sigma env,
558
(env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl)))
560
let prepare_goal sigma g =
561
let options = make_option_commands () in
562
List.iter (fun (set_option,_) -> raw_interp set_option) options;
563
let x = prepare_goal_main sigma g in
564
List.iter (fun (_,unset_option) -> raw_interp unset_option) options;
567
let get_current_pm_goal () =
568
let pfts = get_pftreestate () in
569
let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in
570
let sigma= sig_sig gls in
571
let gl = sig_it gls in
572
prepare_goal sigma gl
575
let get_current_goals () =
576
let pfts = get_pftreestate () in
577
let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
578
let sigma = Tacmach.evc_of_pftreestate pfts in
579
List.map (prepare_goal sigma) gls
581
let get_current_goals_nb () =
582
try List.length (get_current_goals ()) with _ -> 0
584
let print_no_goal () =
585
let pfts = get_pftreestate () in
586
let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
588
let sigma = Tacmach.project (Tacmach.top_goal_of_pftreestate pfts) in
589
msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls)
592
let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
593
[("clear "^ident),("clear "^ident^".");
596
("apply "^ident^".");
599
("exact "^ident^".");
601
("generalize "^ident),
602
("generalize "^ident^".");
604
("absurd <"^ident^">"),
609
(if is_equation ast then
610
[ "discriminate "^ident, "discriminate "^ident^".";
611
"injection "^ident, "injection "^ident^"." ]
615
(let _,t = splay_prod env sigma ast in
616
if is_equation t then
617
[ "rewrite "^ident, "rewrite "^ident^".";
618
"rewrite <- "^ident, "rewrite <- "^ident^"." ]
625
("inversion "^ident),
626
("inversion "^ident^".");
628
("inversion clear "^ident),
629
("inversion_clear "^ident^".")]
631
let concl_menu (_,_,concl,_) =
632
let is_eq = is_equation concl in
635
"intuition","intuition." ] @
638
["reflexivity", "reflexivity.";
639
"discriminate", "discriminate.";
640
"symmetry", "symmetry." ]
644
["assumption" ,"assumption.";
647
"auto with *", "auto with *.";
648
"eauto with *", "eauto with *.";
650
"trivial", "trivial.";
651
"decide equality", "decide equality.";
663
let id_of_name = function
664
| Names.Anonymous -> id_of_string "x"
668
let qualified_name = Libnames.qualid_of_string s in
669
let glob_ref = Nametab.locate qualified_name in
671
| Libnames.IndRef i ->
672
let {Declarations.mind_nparams = np},
673
{Declarations.mind_consnames = carr ;
674
Declarations.mind_nf_lc = tarr }
675
= Global.lookup_inductive i
677
Util.array_fold_right2
679
let (al,_) = Term.decompose_prod t in
680
let al,_ = Util.list_chop (List.length al - np) al in
681
let rec rename avoid = function
684
let n' = next_global_ident_away true
687
in (string_of_id n')::(rename (n'::avoid) l)
689
let al' = rename [] (List.rev al) in
690
(string_of_id n :: al') :: l
695
| _ -> raise Not_found
697
let current_status () =
698
let path = msg (Libnames.pr_dirpath (Lib.cwd ())) in
699
let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in
701
path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ()))
added
removed
ide/coq.ml
