diff options
Diffstat (limited to 'toplevel/ide_slave.ml')
| -rw-r--r-- | toplevel/ide_slave.ml | 436 |
1 files changed, 150 insertions, 286 deletions
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 42ecb75b..93ad052c 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -20,12 +20,6 @@ open Namegen the only one using this mode, but we try here to be as generic as possible, so this may change in the future... *) - -(** Comment the next line for displaying some more debug messages *) - -let prerr_endline _ = () - - (** Signal handling: we postpone ^C during input and output phases, but make it directly raise a Sys.Break during evaluation of the request. *) @@ -59,6 +53,8 @@ let init_stdout,read_stdout = let r = Buffer.contents out_buff in Buffer.clear out_buff; r) +let pr_debug s = + if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s (** Categories of commands *) @@ -73,202 +69,29 @@ let coqide_known_option table = List.mem table [ ["Printing";"Existential";"Instances"]; ["Printing";"Universes"]] -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 _ -> [] - | VernacDeclareInstances _ -> [] - | VernacDeclareClass _ -> [] - - (* Solving *) - | VernacSolve _ -> [SolveCommand] - | VernacSolveExistential _ -> [SolveCommand] - - (* Auxiliary file and library management *) - | VernacRequireFrom _ -> [] - | VernacAddLoadPath _ -> [] - | VernacRemoveLoadPath _ -> [] - | VernacAddMLPath _ -> [] - | VernacDeclareMLModule _ -> [] - | VernacChdir o -> - (* TODO: [Chdir d] is currently not undo-able (not stored in coq state). - But if we register [Chdir] in the state, loading [initial.coq] will - wrongly cd to the compile-time directory at each coqtop launch. *) - if o = None then [QueryCommand] else [] - - (* State management *) - | VernacWriteState _ -> [] - | VernacRestoreState _ -> [] - - (* Resetting *) - | VernacRemoveName _ -> [NavigationCommand] - | VernacResetName _ -> [NavigationCommand] - | VernacResetInitial -> [NavigationCommand] - | VernacBack _ -> [NavigationCommand] - | VernacBackTo _ -> [NavigationCommand] - - (* Commands *) - | VernacDeclareTacticDefinition _ -> [] - | VernacCreateHintDb _ -> [] - | VernacRemoveHints _ -> [] - | VernacHints _ -> [] - | VernacSyntacticDefinition _ -> [] - | VernacDeclareImplicits _ -> [] - | VernacArguments _ -> [] - | 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] - | VernacShow _ -> [OtherStatePreservingCommand] - | VernacCheckGuard -> [OtherStatePreservingCommand] - | VernacProof (None, None) -> [OtherStatePreservingCommand] - | VernacProof _ -> [] - - | VernacProofMode _ -> [] - | VernacBullet _ -> [SolveCommand] - | VernacSubproof _ -> [SolveCommand] - | VernacEndSubproof -> [SolveCommand] - - (* 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) - - -(** Command history stack - - We maintain a stack of the past states of the system. Each - successfully interpreted command adds a [reset_info] element - to this stack, storing what were the (label / open proofs / - current proof depth) just _before_ the interpretation of this - command. A label is just an integer (cf. BackTo and Bactrack - vernac commands). -*) - -type reset_info = { label : int; proofs : identifier list; depth : int } - -let com_stk = Stack.create () - -let compute_reset_info () = - { label = Lib.current_command_label (); - proofs = Pfedit.get_all_proof_names (); - depth = max 0 (Pfedit.current_proof_depth ()) } - - -(** Interpretation (cf. [Ide_intf.interp]) *) +let is_known_option cmd = match cmd with + | VernacSetOption (_,o,BoolValue true) + | VernacUnsetOption (_,o) -> coqide_known_option o + | _ -> false + +let is_debug cmd = match cmd with + | VernacSetOption (_,["Ltac";"Debug"], _) -> true + | _ -> false + +let is_query cmd = match cmd with + | VernacChdir None + | VernacMemOption _ + | VernacPrintOption _ + | VernacCheckMayEval _ + | VernacGlobalCheck _ + | VernacPrint _ + | VernacSearch _ + | VernacLocate _ -> true + | _ -> false + +let is_undo cmd = match cmd with + | VernacUndo _ | VernacUndoTo _ -> true + | _ -> false (** Check whether a command is forbidden by CoqIDE *) @@ -276,82 +99,28 @@ let coqide_cmd_checks (loc,ast) = let user_error s = raise (Loc.Exc_located (loc, Util.UserError ("CoqIde", str s))) in - if is_vernac_debug_command ast then + if is_debug ast then user_error "Debug mode not available within CoqIDE"; - if is_vernac_navigation_command ast then - user_error "Use CoqIDE navigation instead"; - if is_vernac_known_option_command ast then + if is_known_option ast then user_error "Use CoqIDE display menu instead"; - if is_vernac_query_command ast then + if is_navigation_vernac ast then + user_error "Use CoqIDE navigation instead"; + if is_undo ast then + msgerrnl (str "Warning: rather use CoqIDE navigation instead"); + if is_query ast then msgerrnl (str "Warning: query commands should not be inserted in scripts") -let raw_eval_expr = Vernac.eval_expr - -let eval_expr loc_ast = - let rewind_info = compute_reset_info () in - raw_eval_expr loc_ast; - Stack.push rewind_info com_stk +(** Interpretation (cf. [Ide_intf.interp]) *) let interp (raw,verbosely,s) = - if not raw then (prerr_endline "Starting interp..."; prerr_endline s); let pa = Pcoq.Gram.parsable (Stream.of_string s) in let loc_ast = Vernac.parse_sentence (pa,None) in if not raw then coqide_cmd_checks loc_ast; - (* We run tactics silently, since we will query the goal state later. - Otherwise, we honor the IDE verbosity flag. *) - Flags.make_silent - (is_vernac_goal_printing_command (snd loc_ast) || not verbosely); - if raw then raw_eval_expr loc_ast else eval_expr loc_ast; + Flags.make_silent (not verbosely); + Vernac.eval_expr ~preserving:raw loc_ast; Flags.make_silent true; - if not raw then prerr_endline ("...Done with interp of : "^s); read_stdout () - -(** Backtracking (cf. [Ide_intf.rewind]). - We now rely on the [Backtrack] command just as ProofGeneral. *) - -let rewind count = - if count = 0 then 0 - else - let current_proofs = Pfedit.get_all_proof_names () - in - (* 1) First, let's pop the history stack exactly [count] times. - NB: Normally, the IDE will not rewind by more than the numbers - of already interpreted commands, hence no risk of [Stack.Empty]. - *) - let initial_target = - for i = 1 to count - 1 do ignore (Stack.pop com_stk) done; - Stack.pop com_stk - in - (* 2) Backtrack by enough additional steps to avoid re-opening proofs. - Typically, when a Qed has been crossed, we backtrack to the proof start. - NB: We cannot reach the empty stack, since the oldest [reset_info] - in the history cannot have opened proofs. - *) - let already_opened p = List.mem p current_proofs in - let rec extra_back n target = - if List.for_all already_opened target.proofs then n,target - else extra_back (n+1) (Stack.pop com_stk) - in - let extra_count, target = extra_back 0 initial_target - in - (* 3) Now that [target.proofs] is a subset of the opened proofs before - the rewind, we simply abort the extra proofs (if any). - NB: It is critical here that proofs are nested in a regular way - (i.e. no Resume or Suspend, as enforced above). This way, we can simply - count the extra proofs to abort instead of taking care of their names. - *) - let naborts = List.length current_proofs - List.length target.proofs - in - (* 4) We are now ready to call [Backtrack] *) - prerr_endline ("Rewind to state "^string_of_int target.label^ - ", proof depth "^string_of_int target.depth^ - ", num of aborts "^string_of_int naborts); - Vernacentries.vernac_backtrack target.label target.depth naborts; - Lib.mark_end_of_command (); (* We've short-circuited Vernac.eval_expr *) - extra_count - - (** Goal display *) let hyp_next_tac sigma env (id,_,ast) = @@ -404,16 +173,17 @@ let concl_next_tac sigma concl = let process_goal sigma g = let env = Goal.V82.env sigma g in + let id = Goal.uid 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 + string_of_ppcmds (pr_goal_concl_style_env 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)) :: acc 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 - { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl } + { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } (* hyps,(ccl,concl_next_tac sigma g)) *) let goals () = @@ -472,6 +242,82 @@ let status () = in { Interface.status_path = path; Interface.status_proofname = proof } +(** This should be elsewhere... *) +let search flags = + let env = Global.env () in + let rec extract_flags name tpe subtpe mods blacklist = function + | [] -> (name, tpe, subtpe, mods, blacklist) + | (Interface.Name_Pattern s, b) :: l -> + let regexp = + try Str.regexp s + with _ -> Util.error ("Invalid regexp: " ^ s) + in + extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l + | (Interface.Type_Pattern s, b) :: l -> + let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in + let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in + extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l + | (Interface.SubType_Pattern s, b) :: l -> + let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in + let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in + extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l + | (Interface.In_Module m, b) :: l -> + let path = String.concat "." m in + let m = Pcoq.parse_string Pcoq.Constr.global path in + let (_, qid) = Libnames.qualid_of_reference m in + let id = + try Nametab.full_name_module qid + with Not_found -> + Util.error ("Module " ^ path ^ " not found.") + in + extract_flags name tpe subtpe ((id, b) :: mods) blacklist l + | (Interface.Include_Blacklist, b) :: l -> + extract_flags name tpe subtpe mods b l + in + let (name, tpe, subtpe, mods, blacklist) = + extract_flags [] [] [] [] false flags + in + let filter_function ref env constr = + let id = Names.string_of_id (Nametab.basename_of_global ref) in + let path = Libnames.dirpath (Nametab.path_of_global ref) in + let toggle x b = if x then b else not b in + let match_name (regexp, flag) = + toggle (Str.string_match regexp id 0) flag + in + let match_type (pat, flag) = + toggle (Matching.is_matching pat constr) flag + in + let match_subtype (pat, flag) = + toggle (Matching.is_matching_appsubterm ~closed:false pat constr) flag + in + let match_module (mdl, flag) = + toggle (Libnames.is_dirpath_prefix_of mdl path) flag + in + let in_blacklist = + blacklist || (Search.filter_blacklist ref env constr) + in + List.for_all match_name name && + List.for_all match_type tpe && + List.for_all match_subtype subtpe && + List.for_all match_module mods && in_blacklist + in + let ans = ref [] in + let print_function ref env constr = + let name = Names.string_of_id (Nametab.basename_of_global ref) in + let make_path = Names.string_of_id in + let path = + List.rev_map make_path (Names.repr_dirpath (Nametab.dirpath_of_global ref)) + in + let answer = { + Interface.search_answer_full_path = path; + Interface.search_answer_base_name = name; + Interface.search_answer_type = string_of_ppcmds (pr_lconstr_env env constr); + } in + ans := answer :: !ans; + in + let () = Search.gen_filtered_search filter_function print_function in + !ans + let get_options () = let table = Goptions.get_tables () in let fold key state accu = (key, state) :: accu in @@ -485,13 +331,31 @@ let set_options options = in List.iter iter options +let about () = { + Interface.coqtop_version = Coq_config.version; + Interface.protocol_version = Ide_intf.protocol_version; + Interface.release_date = Coq_config.date; + Interface.compile_date = Coq_config.compile_date; +} + (** Grouping all call handlers together + error handling *) +exception Quit + let eval_call c = let rec handle_exn e = catch_break := false; - let pr_exn e = string_of_ppcmds (Errors.print e) in + let pr_exn e = (read_stdout ())^("\n"^(string_of_ppcmds (Errors.print e))) in match e with + | Quit -> + (* Here we do send an acknowledgement message to prove everything went + OK. *) + let dummy = Interface.Good () in + let xml_answer = Ide_intf.of_answer Ide_intf.quit dummy in + let () = Xml_utils.print_xml !orig_stdout xml_answer in + let () = flush !orig_stdout in + let () = pr_debug "Exiting gracefully." in + exit 0 | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!" | Vernacexpr.Quit -> None, "Quit is not allowed by coqide!" | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner @@ -508,17 +372,20 @@ let eval_call c = r in let handler = { - Interface.interp = interruptible interp; - Interface.rewind = interruptible rewind; - Interface.goals = interruptible goals; - Interface.evars = interruptible evars; - Interface.hints = interruptible hints; - Interface.status = interruptible status; - Interface.inloadpath = interruptible inloadpath; - Interface.get_options = interruptible get_options; - Interface.set_options = interruptible set_options; - Interface.mkcases = interruptible Vernacentries.make_cases; - Interface.handle_exn = handle_exn; } + Ide_intf.interp = interruptible interp; + Ide_intf.rewind = interruptible Backtrack.back; + Ide_intf.goals = interruptible goals; + Ide_intf.evars = interruptible evars; + Ide_intf.hints = interruptible hints; + Ide_intf.status = interruptible status; + Ide_intf.search = interruptible search; + Ide_intf.inloadpath = interruptible inloadpath; + Ide_intf.get_options = interruptible get_options; + Ide_intf.set_options = interruptible set_options; + Ide_intf.mkcases = interruptible Vernacentries.make_cases; + Ide_intf.quit = (fun () -> raise Quit); + Ide_intf.about = interruptible about; + Ide_intf.handle_exn = handle_exn; } in (* If the messages of last command are still there, we remove them *) ignore (read_stdout ()); @@ -534,9 +401,6 @@ let eval_call c = between coqtop and ide. With marshalling, reading an answer to a different request could hang the ide... *) -let pr_debug s = - if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s - let fail err = Ide_intf.of_value (fun _ -> assert false) (Interface.Fail (None, err)) @@ -545,9 +409,9 @@ let loop () = let () = Xml_parser.check_eof p false in init_signal_handler (); catch_break := false; - (* ensure we have a command separator object (DOT) so that the first - command can be reseted. *) - Lib.mark_end_of_command(); + (* We'll handle goal fetching and display in our own way *) + Vernacentries.enable_goal_printing := false; + Vernacentries.qed_display_script := false; try while true do let xml_answer = |