diff options
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 953 |
1 files changed, 271 insertions, 682 deletions
@@ -1,53 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 15025 2012-03-09 14:27:07Z glondu $ *) - -open Vernac -open Vernacexpr -open Pfedit -open Pp -open Util -open Names -open Term -open Printer -open Environ -open Evarutil -open Evd -open Decl_mode -open Hipattern -open Tacmach -open Reductionops -open Termops -open Namegen open Ideutils -let msg m = - let b = Buffer.create 103 in - Pp.msg_with (Format.formatter_of_buffer b) m; - Buffer.contents b - -let msgnl m = - (msg m)^"\n" - -let init () = - (* To hide goal in lower window. - Problem: should not hide "xx is assumed" - messages *) -(**) - Flags.make_silent true; - (* don't set a too large undo stack because Edit.create allocates an array *) - Pfedit.set_undo (Some 5000); -(**) - Coqtop.init_ide () - - -let i = ref 0 +(** * Version and date *) let get_version_date () = let date = @@ -55,7 +16,12 @@ let get_version_date () = then Coq_config.date else "<date not printable>" in try - let ch = open_in (Coq_config.coqsrc^"/revision") in + (* the following makes sense only when running with local layout *) + let coqroot = Filename.concat + (Filename.dirname Sys.executable_name) + Filename.parent_dir_name + in + let ch = open_in (Filename.concat coqroot "revision") in let ver = input_line ch in let rev = input_line ch in (ver,rev) @@ -71,656 +37,279 @@ let version () = "The Coq Proof Assistant, version %s (%s)\ \nArchitecture %s running %s operating system\ \nGtk version is %s\ - \nThis is the %s version (%s is the best one for this architecture and OS)\ + \nThis is %s (%s is the best one for this architecture and OS)\ \n" ver date Coq_config.arch Sys.os_type (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z) - (if Mltop.is_native then "native" else "bytecode") - (if Coq_config.best="opt" then "native" else "bytecode") - -let is_in_coq_lib dir = - prerr_endline ("Is it a coq theory ? : "^dir); - let is_same_file = same_file dir in - List.exists - (fun s -> - let fdir = - Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in - prerr_endline (" Comparing to: "^fdir); - if is_same_file fdir then (prerr_endline " YES";true) - else (prerr_endline"NO";false)) - Coq_config.theories_dirs - -let is_in_loadpath dir = - Library.is_in_load_paths (System.physical_path_of_string dir) - -let is_in_coq_path f = - try - let base = Filename.chop_extension (Filename.basename f) in - let _ = Library.locate_qualified_library false - (Libnames.make_qualid Names.empty_dirpath - (Names.id_of_string base)) in - prerr_endline (f ^ " is in coq path"); - true - with _ -> - prerr_endline (f ^ " is NOT in coq path"); - false - -let is_in_proof_mode () = - match Decl_mode.get_current_mode () with - Decl_mode.Mode_none -> false - | _ -> true - -let user_error_loc l s = - raise (Compat.Exc_located (l, Util.UserError ("CoqIde", s))) - -type printing_state = { - mutable printing_implicit : bool; - mutable printing_coercions : bool; - mutable printing_raw_matching : bool; - mutable printing_no_notation : bool; - mutable printing_all : bool; - mutable printing_evar_instances : bool; - mutable printing_universes : bool; - mutable printing_full_all : bool -} + (Filename.basename Sys.executable_name) + Coq_config.best -let printing_state = { - printing_implicit = false; - printing_coercions = false; - printing_raw_matching = false; - printing_no_notation = false; - printing_all = false; - printing_evar_instances = false; - printing_universes = false; - printing_full_all = false; -} -let printing_implicit_data = ["Printing";"Implicit"], false -let printing_coercions_data = ["Printing";"Coercions"], false -let printing_raw_matching_data = ["Printing";"Matching"], true -let printing_no_synth_data = ["Printing";"Synth"], true -let printing_no_notation_data = ["Printing";"Notations"], true -let printing_all_data = ["Printing";"All"], false -let printing_evar_instances_data = ["Printing";"Existential";"Instances"],false -let printing_universes_data = ["Printing";"Universes"], false - -let known_options = ref [] - -let prepare_option (l,dft) = - known_options := l :: !known_options; - let set = (String.concat " " ("Set"::l)) ^ "." in - let unset = (String.concat " " ("Unset"::l)) ^ "." in - if dft then unset,set else set,unset - -let coqide_known_option table = List.mem table !known_options - -let with_printing_implicit = prepare_option printing_implicit_data -let with_printing_coercions = prepare_option printing_coercions_data -let with_printing_raw_matching = prepare_option printing_raw_matching_data -let with_printing_no_synth = prepare_option printing_no_synth_data -let with_printing_no_notation = prepare_option printing_no_notation_data -let with_printing_all = prepare_option printing_all_data -let with_printing_evar_instances = prepare_option printing_evar_instances_data -let with_printing_universes = prepare_option printing_universes_data - -let make_option_commands () = - let p = printing_state in - (if p.printing_implicit then [with_printing_implicit] else [])@ - (if p.printing_coercions then [with_printing_coercions] else [])@ - (if p.printing_raw_matching then [with_printing_raw_matching;with_printing_no_synth] else [])@ - (if p.printing_no_notation then [with_printing_no_notation] else [])@ - (if p.printing_all then [with_printing_all] else [])@ - (if p.printing_evar_instances then [with_printing_evar_instances] else [])@ - (if p.printing_universes then [with_printing_universes] else [])@ - (if p.printing_full_all then [with_printing_all;with_printing_evar_instances;with_printing_universes] else []) - -let make_option_commands () = - let l = make_option_commands () in - List.iter (fun (a,b) -> prerr_endline a; prerr_endline b) l; - l - -type command_attribute = - NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand - | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand - | ProofEndingCommand - -let rec attribute_of_vernac_command = function - (* Control *) - | VernacTime com -> attribute_of_vernac_command com - | VernacTimeout(_,com) -> attribute_of_vernac_command com - | VernacFail com -> attribute_of_vernac_command com - | VernacList _ -> [] (* unsupported *) - | VernacLoad _ -> [] - - (* Syntax *) - | VernacTacticNotation _ -> [] - | VernacSyntaxExtension _ -> [] - | VernacDelimiters _ -> [] - | VernacBindScope _ -> [] - | VernacOpenCloseScope _ -> [] - | VernacArgumentsScope _ -> [] - | VernacInfix _ -> [] - | VernacNotation _ -> [] - - (* Gallina *) - | VernacDefinition (_,_,DefineBody _,_) -> [] - | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand] - | VernacStartTheoremProof _ -> [GoalStartingCommand] - | VernacEndProof _ -> [ProofEndingCommand] - | VernacExactProof _ -> [ProofEndingCommand] - - | VernacAssumption _ -> [] - | VernacInductive _ -> [] - | VernacFixpoint _ -> [] - | VernacCoFixpoint _ -> [] - | VernacScheme _ -> [] - | VernacCombinedScheme _ -> [] - - (* Modules *) - | VernacDeclareModule _ -> [] - | VernacDefineModule _ -> [] - | VernacDeclareModuleType _ -> [] - | VernacInclude _ -> [] - - (* Gallina extensions *) - | VernacBeginSection _ -> [] - | VernacEndSegment _ -> [] - | VernacRequire _ -> [] - | VernacImport _ -> [] - | VernacCanonical _ -> [] - | VernacCoercion _ -> [] - | VernacIdentityCoercion _ -> [] - - (* Type classes *) - | VernacInstance _ -> [] - | VernacContext _ -> [] - | VernacDeclareInstance _ -> [] - | VernacDeclareClass _ -> [] - - (* Solving *) - | VernacSolve _ -> [SolveCommand] - | VernacSolveExistential _ -> [SolveCommand] - - (* MMode *) - | VernacDeclProof -> [SolveCommand] - | VernacReturn -> [SolveCommand] - | VernacProofInstr _ -> [SolveCommand] - - (* Auxiliary file and library management *) - | VernacRequireFrom _ -> [] - | VernacAddLoadPath _ -> [] - | VernacRemoveLoadPath _ -> [] - | VernacAddMLPath _ -> [] - | VernacDeclareMLModule _ -> [] - | VernacChdir _ -> [OtherStatePreservingCommand] - - (* State management *) - | VernacWriteState _ -> [] - | VernacRestoreState _ -> [] - - (* Resetting *) - | VernacRemoveName _ -> [NavigationCommand] - | VernacResetName _ -> [NavigationCommand] - | VernacResetInitial -> [NavigationCommand] - | VernacBack _ -> [NavigationCommand] - | VernacBackTo _ -> [NavigationCommand] - - (* Commands *) - | VernacDeclareTacticDefinition _ -> [] - | VernacCreateHintDb _ -> [] - | VernacHints _ -> [] - | VernacSyntacticDefinition _ -> [] - | VernacDeclareImplicits _ -> [] - | VernacDeclareReduction _ -> [] - | VernacReserve _ -> [] - | VernacGeneralizable _ -> [] - | VernacSetOpacity _ -> [] - | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand] - | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) -> - if coqide_known_option o then [KnownOptionCommand] else [] - | VernacSetOption _ -> [] - | VernacRemoveOption _ -> [] - | VernacAddOption _ -> [] - | VernacMemOption _ -> [QueryCommand] - - | VernacPrintOption _ -> [QueryCommand] - | VernacCheckMayEval _ -> [QueryCommand] - | VernacGlobalCheck _ -> [QueryCommand] - | VernacPrint _ -> [QueryCommand] - | VernacSearch _ -> [QueryCommand] - | VernacLocate _ -> [QueryCommand] - - | VernacComments _ -> [OtherStatePreservingCommand] - | VernacNop -> [OtherStatePreservingCommand] - - (* Proof management *) - | VernacGoal _ -> [GoalStartingCommand] - - | VernacAbort _ -> [] - | VernacAbortAll -> [NavigationCommand] - | VernacRestart -> [NavigationCommand] - | VernacSuspend -> [NavigationCommand] - | VernacResume _ -> [NavigationCommand] - | VernacUndo _ -> [NavigationCommand] - | VernacUndoTo _ -> [NavigationCommand] - | VernacBacktrack _ -> [NavigationCommand] - - | VernacFocus _ -> [SolveCommand] - | VernacUnfocus -> [SolveCommand] - | VernacGo _ -> [] - | VernacShow _ -> [OtherStatePreservingCommand] - | VernacCheckGuard -> [OtherStatePreservingCommand] - | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand] - | VernacProof _ -> [] - - (* Toplevel control *) - | VernacToplevelControl _ -> [] - - (* Extensions *) - | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand] - | VernacExtend _ -> [] - -let is_vernac_goal_starting_command com = - List.mem GoalStartingCommand (attribute_of_vernac_command com) - -let is_vernac_navigation_command com = - List.mem NavigationCommand (attribute_of_vernac_command com) - -let is_vernac_query_command com = - List.mem QueryCommand (attribute_of_vernac_command com) - -let is_vernac_known_option_command com = - List.mem KnownOptionCommand (attribute_of_vernac_command com) - -let is_vernac_debug_command com = - List.mem DebugCommand (attribute_of_vernac_command com) - -let is_vernac_goal_printing_command com = - let attribute = attribute_of_vernac_command com in - List.mem GoalStartingCommand attribute or - List.mem SolveCommand attribute - -let is_vernac_state_preserving_command com = - let attribute = attribute_of_vernac_command com in - List.mem OtherStatePreservingCommand attribute or - List.mem QueryCommand attribute - -let is_vernac_tactic_command com = - List.mem SolveCommand (attribute_of_vernac_command com) - -let is_vernac_proof_ending_command com = - List.mem ProofEndingCommand (attribute_of_vernac_command com) - -type undo_info = identifier list - -let undo_info () = Pfedit.get_all_proof_names () - -type reset_mark = Libnames.object_name - -type reset_status = - | NoReset - | ResetAtSegmentStart of Names.identifier - | ResetAtRegisteredObject of reset_mark - -type reset_info = { - status : reset_status; - proofs : identifier list; - cur_prf : (identifier * int) option; - loc_ast : Util.loc * Vernacexpr.vernac_expr; +(** * Initial checks by launching test coqtop processes *) + +let rec read_all_lines in_chan = + try + let arg = input_line in_chan in + arg::(read_all_lines in_chan) + with End_of_file -> [] + +let fatal_error_popup msg = + let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok + ~message_type:`ERROR ~message:msg () + in ignore (popup#run ()); exit 1 + +let final_info_popup small msg = + if small then + let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok + ~message_type:`INFO ~message:msg () + in + let _ = popup#run () in + exit 0 + else + let popup = GWindow.dialog () in + let button = GButton.button ~label:"ok" ~packing:popup#action_area#add () + in + let scroll = GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC + ~packing:popup#vbox#add ~height:500 () + in + let _ = GMisc.label ~text:msg ~packing:scroll#add_with_viewport () in + let _ = popup#connect#destroy ~callback:(fun _ -> exit 0) in + let _ = button#connect#clicked ~callback:(fun _ -> exit 0) in + let _ = popup#run () in + exit 0 + +let connection_error cmd lines exn = + fatal_error_popup + ("Connection with coqtop failed!\n"^ + "Command was: "^cmd^"\n"^ + "Answer was: "^(String.concat "\n " lines)^"\n"^ + "Exception was: "^Printexc.to_string exn) + +let display_coqtop_answer cmd lines = + final_info_popup (List.length lines < 30) + ("Coqtop exited\n"^ + "Command was: "^cmd^"\n"^ + "Answer was: "^(String.concat "\n " lines)) + +let check_remaining_opt arg = + if arg <> "" && arg.[0] = '-' then fatal_error_popup ("Illegal option: "^arg) + +let rec filter_coq_opts args = + let argstr = String.concat " " (List.map Filename.quote args) in + let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in + let cmd = requote cmd in + let filtered_args = ref [] in + let errlines = ref [] in + try + let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in + filtered_args := read_all_lines oc; + errlines := read_all_lines ec; + match Unix.close_process_full (oc,ic,ec) with + | Unix.WEXITED 0 -> + List.iter check_remaining_opt !filtered_args; !filtered_args + | Unix.WEXITED 127 -> asks_for_coqtop args + | _ -> display_coqtop_answer cmd (!filtered_args @ !errlines) + with Sys_error _ -> asks_for_coqtop args + | e -> connection_error cmd (!filtered_args @ !errlines) e + +and asks_for_coqtop args = + let pb_mes = GWindow.message_dialog + ~message:"Failed to load coqtop. Reset the preference to default ?" + ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in + match pb_mes#run () with + | `YES -> + let () = !Preferences.current.Preferences.cmd_coqtop <- None in + let () = custom_coqtop := None in + let () = pb_mes#destroy () in + filter_coq_opts args + | `DELETE_EVENT | `NO -> + let () = pb_mes#destroy () in + let cmd_sel = GWindow.file_selection + ~title:"Coqtop to execute (edit your preference then)" + ~filename:(coqtop_path ()) ~urgency_hint:true () in + match cmd_sel#run () with + | `OK -> + let () = custom_coqtop := (Some cmd_sel#filename) in + let () = cmd_sel#destroy () in + filter_coq_opts args + | `CANCEL | `DELETE_EVENT | `HELP -> exit 0 + +exception WrongExitStatus of string + +let print_status = function + | Unix.WEXITED n -> "WEXITED "^string_of_int n + | Unix.WSIGNALED n -> "WSIGNALED "^string_of_int n + | Unix.WSTOPPED n -> "WSTOPPED "^string_of_int n + +let check_connection args = + let lines = ref [] in + let argstr = String.concat " " (List.map Filename.quote args) in + let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in + let cmd = requote cmd in + try + let ic = Unix.open_process_in cmd in + lines := read_all_lines ic; + match Unix.close_process_in ic with + | Unix.WEXITED 0 -> () (* coqtop seems ok *) + | st -> raise (WrongExitStatus (print_status st)) + with e -> connection_error cmd !lines e + +(** * The structure describing a coqtop sub-process *) + +type coqtop = { + pid : int; (* Unix process id *) + cout : in_channel ; + cin : out_channel ; + sup_args : string list; } -let compute_reset_info loc_ast = - let status,cur_prf = match snd loc_ast with - | com when is_vernac_proof_ending_command com -> NoReset,None - | VernacEndSegment _ -> NoReset,None - | com when is_vernac_tactic_command com -> - NoReset,Some (Pfedit.get_current_proof_name (), Pfedit.current_proof_depth ()) - | _ -> - (match Lib.has_top_frozen_state () with - | Some sp -> - prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); - ResetAtRegisteredObject sp,None - | None -> NoReset,None) - in - { status = status; - proofs = Pfedit.get_all_proof_names (); - cur_prf = cur_prf; - loc_ast = loc_ast; - } - -let reset_initial () = - prerr_endline "Reset initial called"; - Vernacentries.abort_refine Lib.reset_initial () - -let reset_to sp = - prerr_endline - ("Reset called with state "^(Libnames.string_of_path (fst sp))); - Lib.reset_to_state sp - -let raw_interp s = - Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)) - -let interp_with_options verbosely options s = - prerr_endline "Starting interp..."; - prerr_endline s; - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in - (* Temporary hack to make coqide.byte work (WTF???) - now with less screen - * pollution *) - (try Pervasives.prerr_string " \r"; Pervasives.flush stderr with _ -> ()); - match pe with - | None -> assert false - | Some((loc,vernac) as last) -> - if is_vernac_debug_command vernac then - user_error_loc loc (str "Debug mode not available within CoqIDE"); - if is_vernac_navigation_command vernac then - user_error_loc loc (str "Use CoqIDE navigation instead"); - if is_vernac_known_option_command vernac then - user_error_loc loc (str "Use CoqIDE display menu instead"); - if is_vernac_query_command vernac then - flash_info - "Warning: query commands should not be inserted in scripts"; - if not (is_vernac_goal_printing_command vernac) then - (* Verbose if in small step forward and not a tactic *) - Flags.make_silent (not verbosely); - let reset_info = compute_reset_info last in - List.iter (fun (set_option,_) -> raw_interp set_option) options; - raw_interp s; - Flags.make_silent true; - List.iter (fun (_,unset_option) -> raw_interp unset_option) options; - prerr_endline ("...Done with interp of : "^s); - reset_info - -let interp verbosely phrase = - interp_with_options verbosely (make_option_commands ()) phrase - -let interp_and_replace s = - let result = interp false s in - let msg = read_stdout () in - result,msg - -let rec is_pervasive_exn = function - | Out_of_memory | Stack_overflow | Sys.Break -> true - | Error_in_file (_,_,e) -> is_pervasive_exn e - | Compat.Exc_located (_,e) -> is_pervasive_exn e - | DuringCommandInterp (_,e) -> is_pervasive_exn e - | _ -> false - -let print_toplevel_error exc = - let (dloc,exc) = - match exc with - | DuringCommandInterp (loc,ie) -> - if loc = dummy_loc then (None,ie) else (Some loc, ie) - | _ -> (None, exc) - in - let (loc,exc) = - match exc with - | Compat.Exc_located (loc, ie) -> (Some loc),ie - | Error_in_file (s, (_,fname, loc), ie) -> None, ie - | _ -> dloc,exc - in - match exc with - | End_of_input -> str "Please report: End of input",None - | Vernacexpr.Drop -> str "Drop is not allowed by coqide!",None - | Vernacexpr.Quit -> str "Quit is not allowed by coqide! Use menus.",None - | _ -> - (try Cerrors.explain_exn exc with e -> - str "Failed to explain error. This is an internal Coq error. Please report.\n" - ++ str (Printexc.to_string e)), - (if is_pervasive_exn exc then None else loc) - -let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc) - -let interp_last last = - prerr_string "*"; +(** * Count of all active coqtops *) + +let toplvl_ctr = ref 0 + +let toplvl_ctr_mtx = Mutex.create () + +let coqtop_zombies () = + Mutex.lock toplvl_ctr_mtx; + let res = !toplvl_ctr in + Mutex.unlock toplvl_ctr_mtx; + res + + +(** * Starting / signaling / ending a real coqtop sub-process *) + +(** We simulate a Unix.open_process that also returns the pid of + the created process. Note: this uses Unix.create_process, which + doesn't call bin/sh, so args shouldn't be quoted. The process + cannot be terminated by a Unix.close_process, but rather by a + kill of the pid. + + >--ide2top_w--[pipe]--ide2top_r--> + coqide coqtop + <--top2ide_r--[pipe]--top2ide_w--< + + Note: we use Unix.stderr in Unix.create_process to get debug + messages from the coqtop's Ide_slave loop. + + NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r) + in coqtop. We do this indirectly via [Unix.set_close_on_exec]. + This way, coqide has the only remaining copies of these descriptors, + and closing them later will have visible effects in coqtop. Cf man 7 pipe : + + - If all file descriptors referring to the write end of a pipe have been + closed, then an attempt to read(2) from the pipe will see end-of-file + (read(2) will return 0). + - If all file descriptors referring to the read end of a pipe have been + closed, then a write(2) will cause a SIGPIPE signal to be generated for + the calling process. If the calling process is ignoring this signal, + then write(2) fails with the error EPIPE. + + Symmetrically, coqtop's descriptors (ide2top_r and top2ide_w) should be + closed in coqide. +*) + +let open_process_pid prog args = + let (ide2top_r,ide2top_w) = Unix.pipe () in + let (top2ide_r,top2ide_w) = Unix.pipe () in + Unix.set_close_on_exec ide2top_w; + Unix.set_close_on_exec top2ide_r; + let pid = Unix.create_process prog args ide2top_r top2ide_w Unix.stderr in + assert (pid <> 0); + Unix.close ide2top_r; + Unix.close top2ide_w; + let oc = Unix.out_channel_of_descr ide2top_w in + let ic = Unix.in_channel_of_descr top2ide_r in + set_binary_mode_out oc true; + set_binary_mode_in ic true; + (pid,ic,oc) + +let spawn_coqtop sup_args = + Mutex.lock toplvl_ctr_mtx; try - vernac_com Vernacentries.interp last; - Lib.add_frozen_state() + let prog = coqtop_path () in + let args = Array.of_list (prog :: "-ideslave" :: sup_args) in + let (pid,ic,oc) = open_process_pid prog args in + incr toplvl_ctr; + Mutex.unlock toplvl_ctr_mtx; + { pid = pid; cin = oc; cout = ic ; sup_args = sup_args } with e -> - let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s); + Mutex.unlock toplvl_ctr_mtx; raise e -let push_phrase cmd_stk reset_info ide_payload = - Stack.push (ide_payload,reset_info) cmd_stk - -type backtrack = - | BacktrackToNextActiveMark - | BacktrackToMark of reset_mark - | NoBacktrack - -let apply_reset = function - | BacktrackToMark mark -> reset_to mark - | NoBacktrack -> () - | BacktrackToNextActiveMark -> assert false - -let rewind sequence cmd_stk = - let undo_ops = Hashtbl.create 31 in - let current_proofs = undo_info () in - let pop_state cont seq coq reset_op prev_proofs curprf = - prerr_endline "pop"; - let curprf = - Option.map - (fun (curprf,depth) -> - (if Hashtbl.mem undo_ops curprf then Hashtbl.replace else Hashtbl.add) - undo_ops curprf depth; - curprf) - coq.cur_prf in - let reset_op = - match coq.status with - | ResetAtRegisteredObject mark -> - BacktrackToMark mark - | _ when is_vernac_state_preserving_command (snd coq.loc_ast) -> - reset_op - | _ when is_vernac_tactic_command (snd coq.loc_ast) -> - reset_op - | _ -> - BacktrackToNextActiveMark in - cont seq reset_op coq.proofs curprf - in - let rec do_rewind seq reset_op prev_proofs curprf = - match seq with - | [] when ((reset_op <> BacktrackToNextActiveMark) && - (Util.list_subset prev_proofs current_proofs)) -> - begin - Hashtbl.iter - (fun id depth -> - if List.mem id prev_proofs then begin - Pfedit.resume_proof (Util.dummy_loc,id); - Pfedit.undo_todepth depth - end) - undo_ops; - prerr_endline "OK for undos"; - Option.iter (fun id -> if List.mem id prev_proofs then - Pfedit.resume_proof (Util.dummy_loc,id)) curprf; - prerr_endline "OK for focusing"; - List.iter - (fun id -> Pfedit.delete_proof (Util.dummy_loc,id)) - (Util.list_subtract current_proofs prev_proofs); - prerr_endline "OK for aborts"; - apply_reset reset_op; - prerr_endline "OK for reset" - end - | [] -> - begin - try - let ide,coq = Stack.pop cmd_stk in - pop_state do_rewind [] coq reset_op prev_proofs curprf; - prerr_endline "push"; - let reset_info = compute_reset_info coq.loc_ast in - interp_last coq.loc_ast; - push_phrase cmd_stk reset_info ide - with Stack.Empty -> reset_initial () - end - | coq::rem -> - pop_state do_rewind rem coq reset_op prev_proofs curprf - in - do_rewind sequence NoBacktrack current_proofs None - -type tried_tactic = - | Interrupted - | Success of int (* nb of goals after *) - | Failed - -type hyp = env * evar_map * - ((identifier * string) * constr option * constr) * - (string * string) -type concl = env * evar_map * constr * string -type meta = env * evar_map * string -type goal = hyp list * concl - -let prepare_hyp sigma env ((i,c,d) as a) = - env, sigma, - ((i,string_of_id i),c,d), - (msg (pr_var_decl env a), msg (pr_ltype_env env d)) - -let prepare_hyps sigma env = - assert (rel_context env = []); - let hyps = - fold_named_context - (fun env d acc -> let hyp = prepare_hyp sigma env d in hyp :: acc) - env ~init:[] - in - List.rev hyps - -let prepare_goal_main sigma g = - let env = evar_env g in - (prepare_hyps sigma env, - (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl))) - -let prepare_goal sigma g = - let options = make_option_commands () in - List.iter (fun (set_option,_) -> raw_interp set_option) options; - let x = prepare_goal_main sigma g in - List.iter (fun (_,unset_option) -> raw_interp unset_option) options; - x - -let get_current_pm_goal () = - let pfts = get_pftreestate () in - let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in - let sigma= sig_sig gls in - let gl = sig_it gls in - prepare_goal sigma gl - -let get_current_goals () = - let pfts = get_pftreestate () in - let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in - let sigma = Tacmach.evc_of_pftreestate pfts in - List.map (prepare_goal sigma) gls - -let print_no_goal () = - (* Fall back on standard coq goal printer for completed goal printing *) - msg (pr_open_subgoals ()) - -let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) = - [("clear "^ident),("clear "^ident^"."); - - ("apply "^ident), - ("apply "^ident^"."); - - ("exact "^ident), - ("exact "^ident^"."); - - ("generalize "^ident), - ("generalize "^ident^"."); - - ("absurd <"^ident^">"), - ("absurd "^ - pr_ast - ^".") ] @ - - (if is_equality_type ast then - [ "discriminate "^ident, "discriminate "^ident^"."; - "injection "^ident, "injection "^ident^"." ] - else - []) @ - - (let _,t = splay_prod env sigma ast in - if is_equality_type t then - [ "rewrite "^ident, "rewrite "^ident^"."; - "rewrite <- "^ident, "rewrite <- "^ident^"." ] - else - []) @ - - [("elim "^ident), - ("elim "^ident^"."); - - ("inversion "^ident), - ("inversion "^ident^"."); - - ("inversion clear "^ident), - ("inversion_clear "^ident^".")] - -let concl_menu (_,_,concl,_) = - let is_eq = is_equality_type concl in - ["intro", "intro."; - "intros", "intros."; - "intuition","intuition." ] @ - - (if is_eq then - ["reflexivity", "reflexivity."; - "discriminate", "discriminate."; - "symmetry", "symmetry." ] - else - []) @ - - ["assumption" ,"assumption."; - "omega", "omega."; - "ring", "ring."; - "auto with *", "auto with *."; - "eauto with *", "eauto with *."; - "tauto", "tauto."; - "trivial", "trivial."; - "decide equality", "decide equality."; - - "simpl", "simpl."; - "subst", "subst."; - - "red", "red."; - "split", "split."; - "left", "left."; - "right", "right."; - ] - - -let id_of_name = function - | Names.Anonymous -> id_of_string "x" - | Names.Name x -> x - -let make_cases s = - let qualified_name = Libnames.qualid_of_string s in - let glob_ref = Nametab.locate qualified_name in - match glob_ref with - | Libnames.IndRef i -> - let {Declarations.mind_nparams = np}, - {Declarations.mind_consnames = carr ; - Declarations.mind_nf_lc = tarr } - = Global.lookup_inductive i - in - Util.array_fold_right2 - (fun n t l -> - let (al,_) = Term.decompose_prod t in - let al,_ = Util.list_chop (List.length al - np) al in - let rec rename avoid = function - | [] -> [] - | (n,_)::l -> - let n' = next_ident_away_in_goal - (id_of_name n) - avoid - in (string_of_id n')::(rename (n'::avoid) l) - in - let al' = rename [] (List.rev al) in - (string_of_id n :: al') :: l - ) - carr - tarr - [] - | _ -> raise Not_found - -let current_status () = - let path = msg (Libnames.pr_dirpath (Lib.cwd ())) in - let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in - try - path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ())) - with _ -> path +let respawn_coqtop coqtop = spawn_coqtop coqtop.sup_args +let interrupter = ref (fun pid -> Unix.kill pid Sys.sigint) +let killer = ref (fun pid -> Unix.kill pid Sys.sigkill) + +let break_coqtop coqtop = + try !interrupter coqtop.pid + with _ -> prerr_endline "Error while sending Ctrl-C" + +let kill_coqtop coqtop = + let pid = coqtop.pid in + begin + try !killer pid + with _ -> prerr_endline "Kill -9 failed. Process already terminated ?" + end; + try + ignore (Unix.waitpid [] pid); + Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx + with _ -> prerr_endline "Error while waiting for child" + +(** * Calls to coqtop *) + +(** Cf [Ide_intf] for more details *) + +let p = Xml_parser.make () +let () = Xml_parser.check_eof p false + +let eval_call coqtop (c:'a Ide_intf.call) = + Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c); + flush coqtop.cin; + let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in + (Ide_intf.to_answer xml c : 'a Interface.value) + +let interp coqtop ?(raw=false) ?(verbose=true) s = + eval_call coqtop (Ide_intf.interp (raw,verbose,s)) +let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i) +let inloadpath coqtop s = eval_call coqtop (Ide_intf.inloadpath s) +let mkcases coqtop s = eval_call coqtop (Ide_intf.mkcases s) +let status coqtop = eval_call coqtop Ide_intf.status +let hints coqtop = eval_call coqtop Ide_intf.hints + +module PrintOpt = +struct + type t = string list + let implicit = ["Printing"; "Implicit"] + let coercions = ["Printing"; "Coercions"] + let raw_matching = ["Printing"; "Matching"; "Synth"] + let notations = ["Printing"; "Notations"] + let all_basic = ["Printing"; "All"] + let existential = ["Printing"; "Existential"; "Instances"] + let universes = ["Printing"; "Universes"] + + let state_hack = Hashtbl.create 11 + let _ = List.iter (fun opt -> Hashtbl.add state_hack opt false) + [ implicit; coercions; raw_matching; notations; all_basic; existential; universes ] + + let set coqtop options = + let () = List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) options in + let options = List.map (fun (name, v) -> (name, Interface.BoolValue v)) options in + match eval_call coqtop (Ide_intf.set_options options) with + | Interface.Good () -> () + | _ -> raise (Failure "Cannot set options.") + + let enforce_hack coqtop = + let elements = Hashtbl.fold (fun opt v acc -> (opt, v) :: acc) state_hack [] in + set coqtop elements + +end + +let goals coqtop = + let () = PrintOpt.enforce_hack coqtop in + eval_call coqtop Ide_intf.goals + +let evars coqtop = + let () = PrintOpt.enforce_hack coqtop in + eval_call coqtop Ide_intf.evars |