diff options
Diffstat (limited to 'ide')
-rw-r--r-- | ide/command_windows.ml | 4 | ||||
-rw-r--r-- | ide/coq.ml | 460 | ||||
-rw-r--r-- | ide/coq.mli | 12 | ||||
-rw-r--r-- | ide/coqide.ml | 4 | ||||
-rw-r--r-- | ide/ideproof.ml | 4 | ||||
-rw-r--r-- | ide/ideutils.ml | 20 | ||||
-rw-r--r-- | ide/ideutils.mli | 3 |
7 files changed, 23 insertions, 484 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 92dcd8222..beb8ebb52 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -104,9 +104,9 @@ object(self) then com ^ " " else com ^ " " ^ entry#text ^" . " in try - ignore(Coq.interp Coq.dummy_coqtop false phrase); + Coq.raw_interp Coq.dummy_coqtop phrase; result#buffer#set_text - ("Result for command " ^ phrase ^ ":\n" ^ Ideutils.read_stdout ()) + ("Result for command " ^ phrase ^ ":\n" ^ (Coq.read_stdout Coq.dummy_coqtop)) with e -> let (s,loc) = Coq.process_exn e in assert (Glib.Utf8.validate s); diff --git a/ide/coq.ml b/ide/coq.ml index e79d315a9..80e2da562 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -77,326 +77,17 @@ let version () = (if Mltop.is_native then "native" else "bytecode") (if Coq_config.best="opt" then "native" else "bytecode") -let is_in_loadpath coqtop dir = - Library.is_in_load_paths (System.physical_path_of_string dir) +let is_in_loadpath coqtop = Ide_blob.is_in_loadpath + +let reset_initial = Ide_blob.reinit -let user_error_loc l s = - raise (Loc.Exc_located (l, Util.UserError ("CoqIde", s))) +let raw_interp coqtop = Ide_blob.raw_interp -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 - -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] - - (* 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 _ -> [NavigationCommand] - | 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 _ -> [] - - | VernacProofMode _ -> [] - - | VernacSubproof _ -> [SolveCommand] - | VernacEndSubproof _ -> [SolveCommand] - - (* 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 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 parsable_of_string s = - Pcoq.Gram.parsable (Stream.of_string s) - -let reset_initial coqtop = - prerr_endline "Reset initial called"; flush stderr; - Stack.clear com_stk; - Vernacentries.abort_refine Lib.reset_initial () - -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 eval_expr cmd_stk loc_ast = - let rewind_info = compute_reset_info loc_ast in - Vernac.eval_expr loc_ast; - Stack.push rewind_info cmd_stk; - Stack.length cmd_stk - -let interp coqtop 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 - 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 stack_depth = eval_expr com_stk (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 coqtop 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 com_stk coq.loc_ast); - end - end - in - do_rewind count NoReset current_proofs None; - Stack.length com_stk +let interp coqtop = Ide_blob.interp +let rewind coqtop = Ide_blob.rewind + +let read_stdout = Ide_blob.read_stdout module PrintOpt = struct @@ -418,17 +109,12 @@ struct List.iter (fun cmd -> let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in - Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string str,None))) + Ide_blob.raw_interp str) opt let enforce_hack () = Hashtbl.iter (set ()) state_hack end -(* -let forbid_vernac blacklist (loc,vernac) = - List.map (fun (test,err) -> if test vernac then err loc - *) - let rec is_pervasive_exn = function | Out_of_memory | Stack_overflow | Sys.Break -> true | Error_in_file (_,_,e) -> is_pervasive_exn e @@ -466,132 +152,10 @@ type tried_tactic = | Success of int (* nb of goals after *) | Failed -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 goals coqtop = PrintOpt.enforce_hack (); - let pfts = Pfedit.get_pftreestate () in - let { it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in - if all_goals = [] then - begin - Message ( - let exl = Evarutil.non_instantiated sigma in - if exl = [] then "Proof Completed.\n" else - ("No more subgoals but non-instantiated existential variables:\n"^ - string_of_ppcmds (pr_evars_int 1 exl))) - 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 - + Ide_blob.current_goals () -let id_of_name = function - | Names.Anonymous -> id_of_string "x" - | Names.Name x -> x - -let make_cases coqtop 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 coqtop = - 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 make_cases coqtop = Ide_blob.make_cases +let current_status = Ide_blob.current_status diff --git a/ide/coq.mli b/ide/coq.mli index d1568203f..231d2dc63 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -10,6 +10,7 @@ open Names open Term open Environ open Evd +open Ide_blob val short_version : unit -> string val version : unit -> string @@ -35,10 +36,15 @@ end val reset_initial : coqtop -> unit val init : unit -> string list + +val raw_interp : coqtop -> string -> unit + val interp : coqtop -> bool -> string -> int val rewind : coqtop -> int -> int +val read_stdout : coqtop -> string + val process_exn : exn -> string*(Util.loc option) val is_in_loadpath : coqtop -> string -> bool @@ -54,10 +60,4 @@ type tried_tactic = val current_status : coqtop -> string -type 'a menu = 'a * (string * string) list - -type goals = - | Message of string - | Goals of ((string menu) list * string menu) list - val goals : coqtop -> goals diff --git a/ide/coqide.ml b/ide/coqide.ml index 32f2bdd71..e49434303 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -778,7 +778,7 @@ object(self) prerr_endline "Send_to_coq starting now"; let r = Coq.interp Coq.dummy_coqtop verbosely phrase in let is_complete = true in - let msg = read_stdout () in + let msg = Coq.read_stdout Coq.dummy_coqtop in sync display_output msg; Some (is_complete,r) with e -> @@ -1008,7 +1008,6 @@ object(self) prerr_endline "Moving (long) start_of_input..."; input_buffer#move_mark ~where:start (`NAME "start_of_input"); self#show_goals; - clear_stdout (); self#clear_message) (); with _ -> @@ -3121,7 +3120,6 @@ let start () = then Pp.warning msg else failwith ("Coqide internal error: " ^ msg))); Command_windows.main (); - init_stdout (); main files; if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ()); while true do diff --git a/ide/ideproof.ml b/ide/ideproof.ml index fe8a70e01..e8f21e239 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 - | Coq.Message msg -> + | Ide_blob.Message msg -> view#buffer#insert msg - | Coq.Goals g -> + | Ide_blob.Goals g -> mode view g diff --git a/ide/ideutils.ml b/ide/ideutils.ml index aaade8aa5..46e6d43eb 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -147,26 +147,6 @@ let set_highlight_timer f = Some (GMain.Timeout.add ~ms:2000 ~callback:(fun () -> f (); highlight_timer := None; true)) - -(* Get back the standard coq out channels *) -let init_stdout,read_stdout,clear_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 () -> - Pp_control.std_ft := out_ft; - Pp_control.err_ft := out_ft; - Pp_control.deep_ft := deep_out_ft; -), - (fun () -> Format.pp_print_flush out_ft (); - let r = Buffer.contents out_buff in - prerr_endline "Output from Coq is: "; prerr_endline r; - Buffer.clear out_buff; r), - (fun () -> - Format.pp_print_flush out_ft (); Buffer.clear out_buff) - - let last_dir = ref "" let filter_all_files () = GFile.filter diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 0d57b855e..993856a3a 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -16,8 +16,6 @@ val doc_url : unit -> string val browse : (string -> unit) -> string -> unit val browse_keyword : (string -> unit) -> string -> unit val byte_offset_to_char_offset : string -> int -> int -val init_stdout : unit -> unit -val clear_stdout : unit -> unit val debug : bool ref val disconnect_revert_timer : unit -> unit val disconnect_auto_save_timer : unit -> unit @@ -36,7 +34,6 @@ val prerr_endline : string -> unit val prerr_string : string -> unit val print_id : 'a -> unit -val read_stdout : unit -> string val revert_timer : GMain.Timeout.id option ref val auto_save_timer : GMain.Timeout.id option ref val select_file_for_open : |