From e84e0f9e4eb6263e870deb1e00929170bc0301ea Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 23 Mar 2011 17:18:57 +0000 Subject: Ide: stronger separation from coqtop Former module Ide_blob is now divided in Ide_intf (linked both by coqtop and coqide) and Ide_slave (now only in coqtop). Ide_intf has almost no dependencies, we can now compile coqide with only coq_config.cm* and lib.cm(x)a TODO: - Devise a better way to display whether coqide is byte or opt in the about message (instead of Mltop.is_native, I display now the executable name, which hopefully contains opt or byte) - Check the late error handling in ide/coq.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.common | 9 +- ide/command_windows.ml | 8 +- ide/coq.ml | 98 +++----- ide/coq.mli | 24 +- ide/coqide.ml | 40 ++-- ide/ideproof.ml | 4 +- toplevel/coqtop.ml | 4 +- toplevel/ide_blob.ml | 595 ------------------------------------------------ toplevel/ide_blob.mli | 46 ---- toplevel/ide_intf.ml | 84 +++++++ toplevel/ide_intf.mli | 47 ++++ toplevel/ide_slave.ml | 536 +++++++++++++++++++++++++++++++++++++++++++ toplevel/ide_slave.mli | 17 ++ toplevel/toplevel.mllib | 3 +- 14 files changed, 759 insertions(+), 756 deletions(-) delete mode 100644 toplevel/ide_blob.ml delete mode 100644 toplevel/ide_blob.mli create mode 100644 toplevel/ide_intf.ml create mode 100644 toplevel/ide_intf.mli create mode 100644 toplevel/ide_slave.ml create mode 100644 toplevel/ide_slave.mli diff --git a/Makefile.common b/Makefile.common index fa76dac60b..c51ca4011a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -217,10 +217,15 @@ INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS)) LINKCMO:=$(CONFIG) $(CORECMA) $(STATICPLUGINS) LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) +LIBCMA:=lib/lib.cma IDECMA:=ide/ide.cma +IDEINTF:=toplevel/ide_intf.cmo -LINKIDE:=$(LINKCMO) $(IDECMA) ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTDEPS) $(LINKCMX) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml +IDELIBS:=$(CONFIG) $(LIBCMA) $(IDEINTF) $(IDECMA) +IDELIBSOPT:=$(subst .cmo,.cmx,$(IDELIBS:.cma=.cmxa)) + +LINKIDE:=$(IDELIBS) ide/coqide_main.ml +LINKIDEOPT:=$(IDEOPTDEPS) $(IDELIBSOPT) ide/coqide_main_opt.ml # modules known by the toplevel of Coq diff --git a/ide/command_windows.ml b/ide/command_windows.ml index a351107d91..70bc4d1cd1 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -106,13 +106,13 @@ object(self) try result#buffer#set_text (match Coq.raw_interp coqtop phrase with - | Ide_blob.Fail (l,str) -> + | Ide_intf.Fail (l,str) -> ("Error while interpreting "^phrase^":\n"^str) - | Ide_blob.Good () -> + | Ide_intf.Good () -> match Coq.read_stdout coqtop with - | Ide_blob.Fail (l,str) -> + | Ide_intf.Fail (l,str) -> ("Error while fetching "^phrase^"results:\n"^str) - | Ide_blob.Good results -> + | Ide_intf.Good results -> ("Result for command " ^ phrase ^ ":\n" ^ results)) with e -> let (s,loc) = Coq.process_exn e in diff --git a/ide/coq.ml b/ide/coq.ml index 89040aa5f7..41c9546d1f 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -6,24 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Vernac -open Vernacexpr -open Pfedit -open Pp open Util -open Names -open Term -open Printer -open Environ -open Evarutil -open Evd -open Hipattern -open Tacmach -open Reductionops -open Termops -open Namegen -open Ideutils open Compat +open Pp +open Ideutils type coqtop = { mutable pid : int; @@ -69,13 +55,13 @@ 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") + (Filename.basename Sys.executable_name) + Coq_config.best let rec read_all_lines in_chan = try @@ -116,20 +102,20 @@ let check_connection args = List.iter Pervasives.prerr_endline lines; exit 1 -let eval_call coqtop (c:'a Ide_blob.call) = +let eval_call coqtop (c:'a Ide_intf.call) = Marshal.to_channel coqtop.cin c []; flush coqtop.cin; - (Marshal.from_channel: in_channel -> 'a Ide_blob.value) coqtop.cout + (Marshal.from_channel: in_channel -> 'a Ide_intf.value) coqtop.cout -let is_in_loadpath coqtop s = eval_call coqtop (Ide_blob.is_in_loadpath s) +let is_in_loadpath coqtop s = eval_call coqtop (Ide_intf.is_in_loadpath s) -let raw_interp coqtop s = eval_call coqtop (Ide_blob.raw_interp s) +let raw_interp coqtop s = eval_call coqtop (Ide_intf.raw_interp s) -let interp coqtop b s = eval_call coqtop (Ide_blob.interp b s) +let interp coqtop b s = eval_call coqtop (Ide_intf.interp b s) -let rewind coqtop i = eval_call coqtop (Ide_blob.rewind i) +let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i) -let read_stdout coqtop = eval_call coqtop Ide_blob.read_stdout +let read_stdout coqtop = eval_call coqtop Ide_intf.read_stdout let toplvl_ctr = ref 0 @@ -209,56 +195,30 @@ struct (fun acc cmd -> let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in match raw_interp coqtop str with - | Ide_blob.Good () -> acc - | Ide_blob.Fail (l,errstr) -> Ide_blob.Fail (l,"Could not eval \""^str^"\": "^errstr) + | Ide_intf.Good () -> acc + | Ide_intf.Fail (l,errstr) -> Ide_intf.Fail (l,"Could not eval \""^str^"\": "^errstr) ) - (Ide_blob.Good ()) + (Ide_intf.Good ()) opt - let enforce_hack coqtop = Hashtbl.fold (fun opt v acc -> - match set coqtop opt v with - | Ide_blob.Good () -> Ide_blob.Good () - | Ide_blob.Fail str -> Ide_blob.Fail str) - state_hack (Ide_blob.Good ()) + let enforce_hack coqtop = Hashtbl.fold + (fun opt v acc -> + match set coqtop opt v with + | Ide_intf.Good () -> Ide_intf.Good () + | Ide_intf.Fail str -> Ide_intf.Fail str) + state_hack (Ide_intf.Good ()) end -let rec is_pervasive_exn = function - | Out_of_memory | Stack_overflow | Sys.Break -> true - | Error_in_file (_,_,e) -> is_pervasive_exn e - | Loc.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 - | Loc.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 process_exn = function + | End_of_file -> + "Warning: End_of_file occurred (possibly a forced restart of coqtop)", None + | e -> Printexc.to_string e,None let goals coqtop = match PrintOpt.enforce_hack coqtop with - | Ide_blob.Good () -> eval_call coqtop Ide_blob.current_goals - | Ide_blob.Fail str -> Ide_blob.Fail str + | Ide_intf.Good () -> eval_call coqtop Ide_intf.current_goals + | Ide_intf.Fail str -> Ide_intf.Fail str -let make_cases coqtop s = eval_call coqtop (Ide_blob.make_cases s) +let make_cases coqtop s = eval_call coqtop (Ide_intf.make_cases s) -let current_status coqtop = eval_call coqtop Ide_blob.current_status +let current_status coqtop = eval_call coqtop Ide_intf.current_status diff --git a/ide/coq.mli b/ide/coq.mli index c909a559ff..a96ed31c76 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -6,12 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Term -open Environ -open Evd -open Ide_blob - val short_version : unit -> string val version : unit -> string val filter_coq_opts : string list -> bool * string list @@ -42,25 +36,25 @@ sig val existential : t val universes : t - val set : coqtop -> t -> bool -> unit Ide_blob.value + val set : coqtop -> t -> bool -> unit Ide_intf.value end -val raw_interp : coqtop -> string -> unit Ide_blob.value +val raw_interp : coqtop -> string -> unit Ide_intf.value -val interp : coqtop -> bool -> string -> int Ide_blob.value +val interp : coqtop -> bool -> string -> int Ide_intf.value -val rewind : coqtop -> int -> int Ide_blob.value +val rewind : coqtop -> int -> int Ide_intf.value -val read_stdout : coqtop -> string Ide_blob.value +val read_stdout : coqtop -> string Ide_intf.value -val is_in_loadpath : coqtop -> string -> bool Ide_blob.value +val is_in_loadpath : coqtop -> string -> bool Ide_intf.value -val make_cases : coqtop -> string -> string list list Ide_blob.value +val make_cases : coqtop -> string -> string list list Ide_intf.value (* Message to display in lower status bar. *) -val current_status : coqtop -> string Ide_blob.value +val current_status : coqtop -> string Ide_intf.value -val goals : coqtop -> goals Ide_blob.value +val goals : coqtop -> Ide_intf.goals Ide_intf.value val msgnl : Pp.std_ppcmds -> string diff --git a/ide/coqide.ml b/ide/coqide.ml index 475b8f8a42..c7b231bf35 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -319,9 +319,9 @@ let setopts ct opts v = List.fold_left (fun acc o -> match set ct o v with - | Ide_blob.Good () -> acc - | Ide_blob.Fail lstr -> Ide_blob.Fail lstr - ) (Ide_blob.Good ()) opts + | Ide_intf.Good () -> acc + | Ide_intf.Fail lstr -> Ide_intf.Fail lstr + ) (Ide_intf.Good ()) opts (* Reset this to None on page change ! *) let (last_completion:(string*int*int*bool) option ref) = ref None @@ -788,9 +788,9 @@ object(self) (fun _ _ -> ()) in try match Coq.goals mycoqtop with - | Ide_blob.Fail (l,str) -> + | Ide_intf.Fail (l,str) -> self#set_message ("Error in coqtop :\n"^str) - | Ide_blob.Good goals -> + | Ide_intf.Good goals -> Ideproof.display (Ideproof.mode_tactic menu_callback) proof_view goals @@ -830,14 +830,14 @@ object(self) full_goal_done <- false; prerr_endline "Send_to_coq starting now"; match Coq.interp mycoqtop verbosely phrase with - | Ide_blob.Fail (l,str) -> sync display_error (str,l); None - | Ide_blob.Good r -> + | Ide_intf.Fail (l,str) -> sync display_error (str,l); None + | Ide_intf.Good r -> match Coq.read_stdout mycoqtop with - | Ide_blob.Fail (_,str) -> + | Ide_intf.Fail (_,str) -> self#set_message ("interp successful but unable to fetch goal, please report bug:\n"^str); None - | Ide_blob.Good msg -> + | Ide_intf.Good msg -> sync display_output msg; Some (true,r) with @@ -1051,10 +1051,10 @@ object(self) begin try match Coq.rewind mycoqtop (n_step 0) with - | Ide_blob.Fail (l,str) -> + | Ide_intf.Fail (l,str) -> sync self#set_message ("Problem while backtracking, CoqIDE and coqtop may be out of sync, you may want to restart :\n"^str) - | Ide_blob.Good _ -> + | Ide_intf.Good _ -> sync (fun _ -> let start = if Stack.is_empty cmd_stack then input_buffer#start_iter @@ -1192,17 +1192,17 @@ object(self) | None -> () | Some f -> let dir = Filename.dirname f in match Coq.is_in_loadpath mycoqtop dir with - | Ide_blob.Fail (_,str) -> + | Ide_intf.Fail (_,str) -> self#set_message ("Could not determine lodpath, this might lead to problems:\n"^str) - | Ide_blob.Good true -> () - | Ide_blob.Good false -> + | Ide_intf.Good true -> () + | Ide_intf.Good false -> match Coq.interp mycoqtop false (Printf.sprintf "Add LoadPath \"%s\". " dir) with - | Ide_blob.Fail (l,str) -> + | Ide_intf.Fail (l,str) -> self#set_message ("Couln't add loadpath:\n"^str) - | Ide_blob.Good _ -> () + | Ide_intf.Good _ -> () end method electric_handler = @@ -2260,9 +2260,9 @@ let main files = pop_info (); push_info (match Coq.current_status current.toplvl with - | Ide_blob.Fail (l,str) -> + | Ide_intf.Fail (l,str) -> "Oops, problem while fetching coq status." - | Ide_blob.Good str -> str) + | Ide_intf.Good str -> str) ) [session_notebook#current_term] in @@ -2502,8 +2502,8 @@ let main files = let cur_ct = session_notebook#current_term.toplvl in try match Coq.make_cases cur_ct w with - | Ide_blob.Fail _ -> raise Not_found - | Ide_blob.Good cases -> + | Ide_intf.Fail _ -> raise Not_found + | Ide_intf.Good cases -> let print c = function | [x] -> Format.fprintf c " | %s => _@\n" x | x::l -> Format.fprintf c " | (%s%a) => _@\n" x diff --git a/ide/ideproof.ml b/ide/ideproof.ml index c84887d1aa..701203061f 100644 --- a/ide/ideproof.ml +++ b/ide/ideproof.ml @@ -89,7 +89,7 @@ let mode_cesar (proof:GText.view) = function let display mode (view:GText.view) goals = view#buffer#set_text ""; match goals with - | Ide_blob.Message msg -> + | Ide_intf.Message msg -> view#buffer#insert msg - | Ide_blob.Goals g -> + | Ide_intf.Goals g -> mode view g diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b85c00714f..93476f4c41 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -319,7 +319,7 @@ let init arglist = if !ide_slave then begin Flags.make_silent true; Pfedit.set_undo (Some 5000); - Ide_blob.init_stdout () + Ide_slave.init_stdout () end; if_verbose print_header (); init_load_path (); @@ -354,7 +354,7 @@ let init_toplevel = init let start () = init_toplevel (List.tl (Array.to_list Sys.argv)); if !ide_slave then - Ide_blob.loop () + Ide_slave.loop () else Toplevel.loop(); (* Initialise and launch the Ocaml toplevel *) diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml deleted file mode 100644 index ff8dbb2d6e..0000000000 --- a/toplevel/ide_blob.ml +++ /dev/null @@ -1,595 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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] - - (* 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 _ -> [] - | VernacRemoveHints _ -> [] - | 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 _ -> [NavigationCommand] - | VernacAbortAll -> [NavigationCommand] - | VernacRestart -> [NavigationCommand] - | VernacSuspend -> [NavigationCommand] - | VernacResume _ -> [NavigationCommand] - | VernacUndo _ -> [NavigationCommand] - | VernacUndoTo _ -> [NavigationCommand] - | VernacBacktrack _ -> [NavigationCommand] - - | VernacFocus _ -> [SolveCommand] - | VernacUnfocus -> [SolveCommand] - | VernacShow _ -> [OtherStatePreservingCommand] - | VernacCheckGuard -> [OtherStatePreservingCommand] - | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand] - | VernacProof _ -> [] - - | VernacProofMode _ -> [] - | VernacSubproof _ -> [] - | VernacEndSubproof -> [] - - (* Toplevel control *) - | VernacToplevelControl _ -> [] - - (* Extensions *) - | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand] - | VernacExtend _ -> [] - -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) - -(* End of Necronomicon exerpts *) - -type reset_status = - | NoReset - | ResetToNextMark - | ResetAtMark of Libnames.object_name - -type reset_info = { - status : reset_status; - proofs : identifier list; - cur_prf : (identifier * int) option; - loc_ast : Util.loc * Vernacexpr.vernac_expr; -} - -let com_stk = Stack.create () - -let reinit () = - Vernacentries.abort_refine Lib.reset_initial (); - Stack.clear com_stk - -let compute_reset_info loc_ast = - let status,cur_prf = match snd loc_ast with - | com when is_vernac_tactic_command com -> - NoReset,Some (Pfedit.get_current_proof_name (),Pfedit.current_proof_depth ()) - | com when is_vernac_state_preserving_command com -> NoReset,None - | com when is_vernac_proof_ending_command com -> ResetToNextMark,None - | VernacEndSegment _ -> NoReset,None - | _ -> - (match Lib.has_top_frozen_state () with - | Some sp -> - prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); - ResetAtMark sp,None - | None -> prerr_endline "No top state"; (NoReset,None)) - in - { status = status; - proofs = Pfedit.get_all_proof_names (); - cur_prf = cur_prf; - loc_ast = loc_ast; - } - -let parsable_of_string s = - Pcoq.Gram.parsable (Stream.of_string s) - -let eval_expr loc_ast = - let rewind_info = compute_reset_info loc_ast in - Vernac.eval_expr loc_ast; - Stack.push rewind_info com_stk; - Stack.length com_stk - -let raw_interp s = - Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string s,None)) - -let user_error_loc l s = - raise (Loc.Exc_located (l, Util.UserError ("CoqIde", s))) - -let interp verbosely s = - prerr_endline "Starting interp..."; - prerr_endline s; - let pa = parsable_of_string s in - try - let (loc,vernac) = Vernac.parse_sentence (pa,None) in - (* Temporary hack to make coqide.byte work (WTF???) - now with - * less screen - * * pollution *) - Pervasives.prerr_string " \r"; Pervasives.flush stderr; - 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 - msgerrnl (str "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 stack_depth = eval_expr (loc,vernac) in - Flags.make_silent true; - prerr_endline ("...Done with interp of : "^s); - stack_depth - with Vernac.End_of_input -> assert false - -let rewind count = - let undo_ops = Hashtbl.create 31 in - let current_proofs = Pfedit.get_all_proof_names () in - let rec do_rewind count reset_op prev_proofs curprf = - if (count <= 0) && (reset_op <> ResetToNextMark) && - (Util.list_subset prev_proofs current_proofs) then - (* We backtracked at least what we wanted to, we have no - * proof to reopen, and we don't need to find a reset mark *) - begin - Hashtbl.iter - (fun id depth -> - if List.mem id prev_proofs then begin - Pfedit.suspend_proof (); - 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.suspend_proof (); - 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"; - (match reset_op with - | NoReset -> prerr_endline "No Reset" - | ResetAtMark m -> (prerr_endline ("Reset at "^(Libnames.string_of_path (fst m))); Lib.reset_to_state m) - | ResetToNextMark -> assert false); - prerr_endline "OK for reset" - end - else - begin - prerr_endline "pop"; - let coq = Stack.pop com_stk in - 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 - do_rewind (pred count) - (if coq.status <> NoReset then coq.status else reset_op) coq.proofs curprf; - if count <= 0 then begin - (* we had to backtrack further to find a suitable - * anchor point, replaying *) - prerr_endline "push"; - ignore (eval_expr coq.loc_ast); - end - end - in - do_rewind count NoReset current_proofs None; - Stack.length com_stk - -let is_in_loadpath dir = - Library.is_in_load_paths (System.physical_path_of_string dir) - -let string_of_ppcmds c = - Pp.msg_with Format.str_formatter c; - Format.flush_str_formatter () - -type 'a menu = 'a * (string * string) list - -type goals = - | Message of string - | Goals of ((string menu) list * string menu) list - -let hyp_next_tac sigma env (id,_,ast) = - let id_s = Names.string_of_id id in - let type_s = string_of_ppcmds (pr_ltype_env env ast) in - [ - ("clear "^id_s),("clear "^id_s^".\n"); - ("apply "^id_s),("apply "^id_s^".\n"); - ("exact "^id_s),("exact "^id_s^".\n"); - ("generalize "^id_s),("generalize "^id_s^".\n"); - ("absurd <"^id_s^">"),("absurd "^type_s^".\n") - ] @ (if Hipattern.is_equality_type ast then [ - ("discriminate "^id_s),("discriminate "^id_s^".\n"); - ("injection "^id_s),("injection "^id_s^".\n") - ] else []) @ (if Hipattern.is_equality_type (snd (Reductionops.splay_prod env sigma ast)) then [ - ("rewrite "^id_s),("rewrite "^id_s^".\n"); - ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n") - ] else []) @ [ - ("elim "^id_s), ("elim "^id_s^".\n"); - ("inversion "^id_s), ("inversion "^id_s^".\n"); - ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n") - ] - -let concl_next_tac sigma concl = - let expand s = (s,s^".\n") in - List.map expand ([ - "intro"; - "intros"; - "intuition" - ] @ (if Hipattern.is_equality_type (Goal.V82.concl sigma concl) then [ - "reflexivity"; - "discriminate"; - "symmetry" - ] else []) @ [ - "assumption"; - "omega"; - "ring"; - "auto"; - "eauto"; - "tauto"; - "trivial"; - "decide equality"; - "simpl"; - "subst"; - "red"; - "split"; - "left"; - "right" - ]) - -let current_goals () = - try - let pfts = - Proof_global.give_me_the_proof () - in - let { Evd.it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in - if all_goals = [] then - begin - Message (string_of_ppcmds ( - let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in - match bgoals with - | [] -> - let exl = Evarutil.non_instantiated sigma in - (str (if exl = [] then "Proof Completed." else - "No more subgoals but non-instantiated existential variables:") ++ - (fnl ()) ++ (pr_evars_int 1 exl)) - | _ -> - Util.list_fold_left_i - (fun i a g -> - a ++ (Printer.pr_concl i sigma g) ++ (spc ())) 1 - (str "This subproof is complete, but there are still unfocused goals:" ++ (fnl ())) - bgoals)) - end - else - begin - let process_goal g = - let env = Goal.V82.env sigma g in - let ccl = - let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in - let process_hyp h_env d acc = - let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in - (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in - let hyps = - List.rev (Environ.fold_named_context process_hyp env ~init:[]) in - (hyps,(ccl,concl_next_tac sigma g)) - in - Goals (List.map process_goal all_goals) - end - with Proof_global.NoCurrentProof -> Message "" (* quick hack to have a clean message screen *) - -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 = string_of_ppcmds (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 orig_stdout = ref stdout - -let init_stdout,read_stdout = - let out_buff = Buffer.create 100 in - let out_ft = Format.formatter_of_buffer out_buff in - let deep_out_ft = Format.formatter_of_buffer out_buff in - let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in - (fun () -> - flush_all (); - orig_stdout := Unix.out_channel_of_descr (Unix.dup Unix.stdout); - Unix.dup2 Unix.stderr Unix.stdout; - Pp_control.std_ft := out_ft; - Pp_control.err_ft := out_ft; - Pp_control.deep_ft := deep_out_ft; - set_binary_mode_out !orig_stdout true; - set_binary_mode_in stdin true; - ), - (fun () -> Format.pp_print_flush out_ft (); - let r = Buffer.contents out_buff in - Buffer.clear out_buff; r) - -(* XXX - duplicates toplevel/toplevel.ml. should be merged. *) -let explain_exn e = - let toploc,exc = - match e with - | Loc.Exc_located (loc, inner) -> - (if loc = dummy_loc then None else Some loc),inner - | Error_in_file (s, (is_in_lib, fname, loc), inner) -> - None,inner - | _ -> None,e - in - toploc,(Cerrors.explain_exn exc) - - -(** - * Wrappers around Coq calls. We use phantom types and GADT to protect ourselves - * against wild casts - *) - -type 'a call = - | In_loadpath of string - | Raw_interp of string - | Interp of bool * string - | Rewind of int - | Read_stdout - | Cur_goals - | Cur_status - | Cases of string - -type 'a value = - | Good of 'a - | Fail of (Util.loc option * string) - -let eval_call c = - let filter_compat_exn = function - | Vernac.DuringCommandInterp (loc,inner) -> inner - | Vernacexpr.Quit -> raise Vernacexpr.Quit - | e -> e - in - try Good (match c with - | In_loadpath s -> Obj.magic (is_in_loadpath s) - | Raw_interp s -> Obj.magic (raw_interp s) - | Interp (b,s) -> Obj.magic (interp b s) - | Rewind i -> Obj.magic (rewind i) - | Read_stdout -> Obj.magic (read_stdout ()) - | Cur_goals -> Obj.magic (current_goals ()) - | Cur_status -> Obj.magic (current_status ()) - | Cases s -> Obj.magic (make_cases s)) - with e -> - let (l,pp) = explain_exn (filter_compat_exn e) in - (* force evaluation of format stream *) - Fail (l,string_of_ppcmds pp) - -let is_in_loadpath s : bool call = - In_loadpath s - -let raw_interp s : unit call = - Raw_interp s - -let interp b s : int call = - Interp (b,s) - -let rewind i : int call = - Rewind i - -let read_stdout : string call = - Read_stdout - -let current_goals : goals call = - Cur_goals - -let current_status : string call = - Cur_status - -let make_cases s : string list list call = - Cases s - -(* End of wrappers *) - -let loop () = - Sys.catch_break true; - try - while true do - let q = (Marshal.from_channel: in_channel -> 'a call) stdin in - let r = eval_call q in - Marshal.to_channel !orig_stdout r []; - flush !orig_stdout - done - with - | Vernacexpr.Quit -> exit 0 - | _ -> exit 1 diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli deleted file mode 100644 index 34879f0577..0000000000 --- a/toplevel/ide_blob.mli +++ /dev/null @@ -1,46 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a value - -val raw_interp : string -> unit call - -val interp : bool -> string -> int call - -val rewind : int -> int call - -val is_in_loadpath : string -> bool call - -val make_cases : string -> string list list call - -val current_status : string call - -val current_goals : goals call - -val read_stdout : string call - -val loop : unit -> unit diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml new file mode 100644 index 0000000000..fb8c9e94d3 --- /dev/null +++ b/toplevel/ide_intf.ml @@ -0,0 +1,84 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool; + raw_interp : string -> unit; + interp : bool -> string -> int; + rewind : int -> int; + read_stdout : unit -> string; + current_goals : unit -> goals; + current_status : unit -> string; + make_cases : string -> string list list; +} + +let abstract_eval_call handler explain_exn c = + try + let res = match c with + | In_loadpath s -> Obj.magic (handler.is_in_loadpath s) + | Raw_interp s -> Obj.magic (handler.raw_interp s) + | Interp (b,s) -> Obj.magic (handler.interp b s) + | Rewind i -> Obj.magic (handler.rewind i) + | Read_stdout -> Obj.magic (handler.read_stdout ()) + | Cur_goals -> Obj.magic (handler.current_goals ()) + | Cur_status -> Obj.magic (handler.current_status ()) + | Cases s -> Obj.magic (handler.make_cases s) + in Good res + with e -> + let (l,str) = explain_exn e in + Fail (l,str) diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli new file mode 100644 index 0000000000..2550a30cd3 --- /dev/null +++ b/toplevel/ide_intf.mli @@ -0,0 +1,47 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit call +val interp : bool -> string -> int call +val rewind : int -> int call +val is_in_loadpath : string -> bool call +val make_cases : string -> string list list call +val current_status : string call +val current_goals : goals call +val read_stdout : string call + +(** * Coq answers to CoqIde *) + +type 'a value = + | Good of 'a + | Fail of (Util.loc option * string) + +type handler = { + is_in_loadpath : string -> bool; + raw_interp : string -> unit; + interp : bool -> string -> int; + rewind : int -> int; + read_stdout : unit -> string; + current_goals : unit -> goals; + current_status : unit -> string; + make_cases : string -> string list list; +} + +val abstract_eval_call : + handler -> (exn -> Util.loc option * string) -> + 'a call -> 'a value diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml new file mode 100644 index 0000000000..5a51471aaf --- /dev/null +++ b/toplevel/ide_slave.ml @@ -0,0 +1,536 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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] + + (* 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 _ -> [] + | VernacRemoveHints _ -> [] + | 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 _ -> [NavigationCommand] + | VernacAbortAll -> [NavigationCommand] + | VernacRestart -> [NavigationCommand] + | VernacSuspend -> [NavigationCommand] + | VernacResume _ -> [NavigationCommand] + | VernacUndo _ -> [NavigationCommand] + | VernacUndoTo _ -> [NavigationCommand] + | VernacBacktrack _ -> [NavigationCommand] + + | VernacFocus _ -> [SolveCommand] + | VernacUnfocus -> [SolveCommand] + | VernacShow _ -> [OtherStatePreservingCommand] + | VernacCheckGuard -> [OtherStatePreservingCommand] + | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand] + | VernacProof _ -> [] + + | VernacProofMode _ -> [] + | VernacSubproof _ -> [] + | VernacEndSubproof -> [] + + (* Toplevel control *) + | VernacToplevelControl _ -> [] + + (* Extensions *) + | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand] + | VernacExtend _ -> [] + +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 reset_status = + | NoReset + | ResetToNextMark + | ResetAtMark of Libnames.object_name + +type reset_info = { + status : reset_status; + proofs : identifier list; + cur_prf : (identifier * int) option; + loc_ast : Util.loc * Vernacexpr.vernac_expr; +} + +let com_stk = Stack.create () + +let reinit () = + Vernacentries.abort_refine Lib.reset_initial (); + Stack.clear com_stk + +let compute_reset_info loc_ast = + let status,cur_prf = match snd loc_ast with + | com when is_vernac_tactic_command com -> + NoReset,Some (Pfedit.get_current_proof_name (),Pfedit.current_proof_depth ()) + | com when is_vernac_state_preserving_command com -> NoReset,None + | com when is_vernac_proof_ending_command com -> ResetToNextMark,None + | VernacEndSegment _ -> NoReset,None + | _ -> + (match Lib.has_top_frozen_state () with + | Some sp -> + prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); + ResetAtMark sp,None + | None -> prerr_endline "No top state"; (NoReset,None)) + in + { status = status; + proofs = Pfedit.get_all_proof_names (); + cur_prf = cur_prf; + loc_ast = loc_ast; + } + +let parsable_of_string s = + Pcoq.Gram.parsable (Stream.of_string s) + +let eval_expr loc_ast = + let rewind_info = compute_reset_info loc_ast in + Vernac.eval_expr loc_ast; + Stack.push rewind_info com_stk; + Stack.length com_stk + +let raw_interp s = + Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string s,None)) + +let user_error_loc l s = + raise (Loc.Exc_located (l, Util.UserError ("CoqIde", s))) + +let interp verbosely s = + prerr_endline "Starting interp..."; + prerr_endline s; + let pa = parsable_of_string s in + try + let (loc,vernac) = Vernac.parse_sentence (pa,None) in + (* Temporary hack to make coqide.byte work (WTF???) - now with + * less screen + * * pollution *) + Pervasives.prerr_string " \r"; Pervasives.flush stderr; + 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 + msgerrnl (str "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 stack_depth = eval_expr (loc,vernac) in + Flags.make_silent true; + prerr_endline ("...Done with interp of : "^s); + stack_depth + with Vernac.End_of_input -> assert false + +let rewind count = + let undo_ops = Hashtbl.create 31 in + let current_proofs = Pfedit.get_all_proof_names () in + let rec do_rewind count reset_op prev_proofs curprf = + if (count <= 0) && (reset_op <> ResetToNextMark) && + (Util.list_subset prev_proofs current_proofs) then + (* We backtracked at least what we wanted to, we have no + * proof to reopen, and we don't need to find a reset mark *) + begin + Hashtbl.iter + (fun id depth -> + if List.mem id prev_proofs then begin + Pfedit.suspend_proof (); + 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.suspend_proof (); + 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"; + (match reset_op with + | NoReset -> prerr_endline "No Reset" + | ResetAtMark m -> (prerr_endline ("Reset at "^(Libnames.string_of_path (fst m))); Lib.reset_to_state m) + | ResetToNextMark -> assert false); + prerr_endline "OK for reset" + end + else + begin + prerr_endline "pop"; + let coq = Stack.pop com_stk in + 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 + do_rewind (pred count) + (if coq.status <> NoReset then coq.status else reset_op) coq.proofs curprf; + if count <= 0 then begin + (* we had to backtrack further to find a suitable + * anchor point, replaying *) + prerr_endline "push"; + ignore (eval_expr coq.loc_ast); + end + end + in + do_rewind count NoReset current_proofs None; + Stack.length com_stk + +let is_in_loadpath dir = + Library.is_in_load_paths (System.physical_path_of_string dir) + +let string_of_ppcmds c = + Pp.msg_with Format.str_formatter c; + Format.flush_str_formatter () + +let hyp_next_tac sigma env (id,_,ast) = + let id_s = Names.string_of_id id in + let type_s = string_of_ppcmds (pr_ltype_env env ast) in + [ + ("clear "^id_s),("clear "^id_s^".\n"); + ("apply "^id_s),("apply "^id_s^".\n"); + ("exact "^id_s),("exact "^id_s^".\n"); + ("generalize "^id_s),("generalize "^id_s^".\n"); + ("absurd <"^id_s^">"),("absurd "^type_s^".\n") + ] @ (if Hipattern.is_equality_type ast then [ + ("discriminate "^id_s),("discriminate "^id_s^".\n"); + ("injection "^id_s),("injection "^id_s^".\n") + ] else []) @ (if Hipattern.is_equality_type (snd (Reductionops.splay_prod env sigma ast)) then [ + ("rewrite "^id_s),("rewrite "^id_s^".\n"); + ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n") + ] else []) @ [ + ("elim "^id_s), ("elim "^id_s^".\n"); + ("inversion "^id_s), ("inversion "^id_s^".\n"); + ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n") + ] + +let concl_next_tac sigma concl = + let expand s = (s,s^".\n") in + List.map expand ([ + "intro"; + "intros"; + "intuition" + ] @ (if Hipattern.is_equality_type (Goal.V82.concl sigma concl) then [ + "reflexivity"; + "discriminate"; + "symmetry" + ] else []) @ [ + "assumption"; + "omega"; + "ring"; + "auto"; + "eauto"; + "tauto"; + "trivial"; + "decide equality"; + "simpl"; + "subst"; + "red"; + "split"; + "left"; + "right" + ]) + +let current_goals () = + try + let pfts = + Proof_global.give_me_the_proof () + in + let { Evd.it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in + if all_goals = [] then + begin + Ide_intf.Message (string_of_ppcmds ( + let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in + match bgoals with + | [] -> + let exl = Evarutil.non_instantiated sigma in + (str (if exl = [] then "Proof Completed." else + "No more subgoals but non-instantiated existential variables:") ++ + (fnl ()) ++ (pr_evars_int 1 exl)) + | _ -> + Util.list_fold_left_i + (fun i a g -> + a ++ (Printer.pr_concl i sigma g) ++ (spc ())) 1 + (str "This subproof is complete, but there are still unfocused goals:" ++ (fnl ())) + bgoals)) + end + else + begin + let process_goal g = + let env = Goal.V82.env sigma g in + let ccl = + let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in + string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in + let process_hyp h_env d acc = + let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in + (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in + let hyps = + List.rev (Environ.fold_named_context process_hyp env ~init:[]) in + (hyps,(ccl,concl_next_tac sigma g)) + in + Ide_intf.Goals (List.map process_goal all_goals) + end + with Proof_global.NoCurrentProof -> + Ide_intf.Message "" (* quick hack to have a clean message screen *) + +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 = string_of_ppcmds (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 orig_stdout = ref stdout + +let init_stdout,read_stdout = + let out_buff = Buffer.create 100 in + let out_ft = Format.formatter_of_buffer out_buff in + let deep_out_ft = Format.formatter_of_buffer out_buff in + let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in + (fun () -> + flush_all (); + orig_stdout := Unix.out_channel_of_descr (Unix.dup Unix.stdout); + Unix.dup2 Unix.stderr Unix.stdout; + Pp_control.std_ft := out_ft; + Pp_control.err_ft := out_ft; + Pp_control.deep_ft := deep_out_ft; + set_binary_mode_out !orig_stdout true; + set_binary_mode_in stdin true; + ), + (fun () -> Format.pp_print_flush out_ft (); + let r = Buffer.contents out_buff in + Buffer.clear out_buff; r) + +(* XXX - duplicates toplevel/toplevel.ml. should be merged. *) +let explain_exn e = + let toploc,exc = + match e with + | Loc.Exc_located (loc, inner) -> + (if loc = dummy_loc then None else Some loc),inner + | Error_in_file (s, (is_in_lib, fname, loc), inner) -> + None,inner + | _ -> None,e + in + toploc,(Cerrors.explain_exn exc) + +let eval_call c = + let rec handle_exn = function + | Vernac.DuringCommandInterp (loc,inner) -> handle_exn inner + | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!" + | Vernacexpr.Quit -> raise Vernacexpr.Quit + | e -> + let (l,pp) = explain_exn e in + l,string_of_ppcmds pp + in + let handler = { + Ide_intf.is_in_loadpath = is_in_loadpath; + Ide_intf.raw_interp = raw_interp; + Ide_intf.interp = interp; + Ide_intf.rewind = rewind; + Ide_intf.read_stdout = read_stdout; + Ide_intf.current_goals = current_goals; + Ide_intf.current_status = current_status; + Ide_intf.make_cases = make_cases } + in + Ide_intf.abstract_eval_call handler handle_exn c + +let loop () = + Sys.catch_break true; + try + while true do + let q = (Marshal.from_channel: in_channel -> 'a Ide_intf.call) stdin in + let r = eval_call q in + Marshal.to_channel !orig_stdout r []; + flush !orig_stdout + done + with + | Vernacexpr.Quit -> exit 0 + | _ -> exit 1 diff --git a/toplevel/ide_slave.mli b/toplevel/ide_slave.mli new file mode 100644 index 0000000000..272616ae30 --- /dev/null +++ b/toplevel/ide_slave.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +val init_stdout : unit -> unit + +val eval_call : 'a Ide_intf.call -> 'a Ide_intf.value + +val loop : unit -> unit diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 7443edefdd..8b03e93803 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -18,7 +18,8 @@ Mltop Vernacentries Whelp Vernac -Ide_blob +Ide_intf +Ide_slave Toplevel Usage Coqinit -- cgit v1.2.3