From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- ide/coq.ml | 511 ++++++++++++++++++++++++++++++++++++++++++------------------- 1 file changed, 355 insertions(+), 156 deletions(-) (limited to 'ide/coq.ml') diff --git a/ide/coq.ml b/ide/coq.ml index d318e339..5166fb21 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 10174 2007-10-04 13:52:23Z vsiles $ *) +(* $Id: coq.ml 11126 2008-06-13 18:45:04Z herbelin $ *) open Vernac open Vernacexpr @@ -43,33 +43,38 @@ let init () = Problem: should not hide "xx is assumed" messages *) (**) - Options.make_silent true; + Flags.make_silent true; (**) Coqtop.init_ide () let i = ref 0 -let version () = +let get_version_date () = let date = if Glib.Utf8.validate Coq_config.date then Coq_config.date else "" in - let get_version_date () = - try - let ch = open_in (Coq_config.coqtop^"/revision") in - let ver = input_line ch in - let rev = input_line ch in - (ver,rev) - with _ -> (Coq_config.version,date) in - let (rev,ver) = get_version_date () in + try + let ch = open_in (Coq_config.coqtop^"/revision") in + let ver = input_line ch in + let rev = input_line ch in + (ver,rev) + with _ -> (Coq_config.version,date) + +let short_version () = + let (ver,date) = get_version_date () in + Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date + +let version () = + let (ver,date) = get_version_date () in Printf.sprintf "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)\ \n" - rev ver + 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.get () = Mltop.Native then "native" else "bytecode") @@ -110,7 +115,310 @@ let is_in_proof_mode () = let user_error_loc l s = raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s))) -let interp verbosely 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 +} + +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 = function + | Goptions.TertiaryTable (a,b,c) -> List.mem [a;b;c] !known_options + | Goptions.SecondaryTable (a,b) -> List.mem [a;b] !known_options + | Goptions.PrimaryTable a -> List.mem [a] !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 + | 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 _ -> [] + | VernacRecord _ -> [] + | VernacRequire _ -> [] + | VernacImport _ -> [] + | VernacCanonical _ -> [] + | VernacCoercion _ -> [] + | VernacIdentityCoercion _ -> [] + + (* Type classes *) + | VernacClass _ -> [] + | VernacInstance _ -> [] + | VernacContext _ -> [] + | VernacDeclareInstance _ -> [] + + (* Solving *) + | VernacSolve _ -> [SolveCommand] + | VernacSolveExistential _ -> [SolveCommand] + + (* MMode *) + | VernacDeclProof -> [] + | VernacReturn -> [] + | VernacProofInstr _ -> [] + + (* 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 _ -> [] + | VernacHints _ -> [] + | VernacSyntacticDefinition _ -> [] + | VernacDeclareImplicits _ -> [] + | VernacReserve _ -> [] + | VernacSetOpacity _ -> [] + | VernacSetOption (Goptions.SecondaryTable ("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 _ -> [] + + (* 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 = + | ResetToId of Names.identifier (* Relying on identifiers only *) + | ResetToState of Libnames.object_name (* Relying on states if any *) + +type reset_status = + | NoReset + | ResetAtSegmentStart of Names.identifier + | ResetAtRegisteredObject of reset_mark + +type reset_info = reset_status * undo_info * bool ref + + +let reset_mark id = match Lib.has_top_frozen_state () with + | Some sp -> + prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); + ResetToState sp + | None -> ResetToId id + +let compute_reset_info = function + | VernacBeginSection id + | VernacDefineModule (_,id, _, _, _) + | VernacDeclareModule (_,id, _, _) + | VernacDeclareModuleType (id, _, _) -> + ResetAtSegmentStart (snd id), undo_info(), ref true + + | VernacDefinition (_, (_,id), DefineBody _, _) + | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_) + | VernacInductive (_, (((_,id),_,_,_),_) :: _) -> + ResetAtRegisteredObject (reset_mark id), undo_info(), ref true + + | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true + | VernacEndSegment _ -> NoReset, undo_info(), ref true + + | com when is_vernac_tactic_command com -> NoReset, undo_info(), ref true + | _ -> + (match Lib.has_top_frozen_state () with + | Some sp -> + prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); + ResetAtRegisteredObject (ResetToState sp) + | None -> NoReset), undo_info(), ref true + +let reset_initial () = + prerr_endline "Reset initial called"; flush stderr; + Vernacentries.abort_refine Lib.reset_initial () + +let reset_to = function + | ResetToId id -> + prerr_endline ("Reset called with "^(string_of_id id)); + Lib.reset_name (Util.dummy_loc,id) + | ResetToState sp -> + prerr_endline + ("Reset called with state "^(Libnames.string_of_path (fst sp))); + Lib.reset_to_state sp + +let reset_to_mod id = + prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); + Lib.reset_mod (Util.dummy_loc,id) + +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 @@ -118,48 +426,28 @@ let interp verbosely s = match pe with | None -> assert false | Some((loc,vernac) as last) -> - match vernac with - | VernacDefinition _ | VernacStartTheoremProof _ - | VernacBeginSection _ | VernacGoal _ - | VernacDefineModule _ | VernacDeclareModuleType _ - | VernacDeclareTacticDefinition _ - when is_in_proof_mode () -> - user_error_loc loc (str "CoqIDE do not support nested goals") - | VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) -> - user_error_loc loc (str "Debug mode not available within CoqIDE") - | VernacResetName _ - | VernacResetInitial - | VernacBack _ - | VernacAbort _ - | VernacAbortAll - | VernacRestart - | VernacSuspend - | VernacResume _ - | VernacUndo _ -> - user_error_loc loc (str "Use CoqIDE navigation instead") - | _ -> - begin - match vernac with - | VernacPrintOption _ - | VernacCheckMayEval _ - | VernacGlobalCheck _ - | VernacPrint _ - | VernacSearch _ - -> !flash_info - "Warning: query commands should not be inserted in scripts" - | VernacDefinition (_,_,DefineBody _,_) - | VernacInductive _ - | VernacFixpoint _ - | VernacCoFixpoint _ - | VernacEndProof _ - | VernacScheme _ - -> Options.make_silent (not verbosely) - | _ -> () - end; - Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)); - Options.make_silent true; - prerr_endline ("...Done with interp of : "^s); - 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 vernac 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,last + +let interp verbosely phrase = + interp_with_options verbosely (make_option_commands ()) phrase let interp_and_replace s = let result = interp false s in @@ -196,11 +484,6 @@ let try_interptac s = | Stdpp.Exc_located (_,e) -> prerr_endline ("try_interp: failed ("^(Printexc.to_string e)); Failed | e -> Failed -let is_tactic = function - | VernacSolve _ -> true - | _ -> false - - let rec is_pervasive_exn = function | Out_of_memory | Stack_overflow | Sys.Break -> true | Error_in_file (_,_,e) -> is_pervasive_exn e @@ -238,7 +521,8 @@ let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc) let interp_last last = prerr_string "*"; try - vernac_com (States.with_heavy_rollback Vernacentries.interp) last + vernac_com (States.with_heavy_rollback Vernacentries.interp) last; + Lib.add_frozen_state() with e -> let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s); raise e @@ -265,29 +549,25 @@ let prepare_hyps sigma env = in List.rev hyps -let prepare_goal sigma g = +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_meta sigma env (m,typ) = - env, sigma, - (msg (str " ?" ++ int m ++ str " : " ++ pr_ltype_env_at_top env typ)) - -let prepare_metas info sigma env = - List.fold_right - (fun cpl acc -> - let meta = prepare_meta sigma env cpl in meta :: acc) - info.pm_subgoals [] +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 info = Decl_mode.get_info gls.it in - let env = pf_env gls in let sigma= sig_sig gls in - (prepare_hyps sigma env, - prepare_metas info sigma env) + let gl = sig_it gls in + prepare_goal sigma gl + let get_current_goals () = let pfts = get_pftreestate () in @@ -306,75 +586,6 @@ let print_no_goal () = msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls) -type word_class = Normal | Kwd | Reserved - - -let kwd = [(* "Compile";"Inductive";"Qed";"Type";"end";"Axiom"; - "Definition";"Load";"Quit";"Variable";"in";"Cases";"FixPoint"; - "Parameter";"Set";"of";"CoFixpoint";"Grammar";"Proof";"Syntax"; - "using";"CoInductive";"Hypothesis";"Prop";"Theorem"; - *) - "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint"; - "CoInductive"; "Defined"; "Definition"; - "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint"; - "Hypothesis"; "Immediate"; "Implicits"; "Import"; "Inductive"; - "Infix"; "Lemma"; "Load"; "Local"; - "Match"; "Module"; "Module Type"; - "Mutual"; "Parameter"; "Print"; "Proof"; "Qed"; - "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; - "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Unset"; "Variable"; "Variables"; -] - -let reserved = [] - -module SHashtbl = - Hashtbl.Make - (struct - type t = string - let equal = ( = ) - let hash = Hashtbl.hash - end) - - -let word_tbl = SHashtbl.create 37 -let _ = - List.iter (fun w -> SHashtbl.add word_tbl w Kwd) kwd; - List.iter (fun w -> SHashtbl.add word_tbl w Reserved) reserved - -let word_class s = - try - SHashtbl.find word_tbl s - with Not_found -> Normal - -type reset_info = NoReset | Reset of Names.identifier * bool ref - -let compute_reset_info = function - | VernacDefinition (_, (_,id), DefineBody _, _) - | VernacBeginSection (_,id) - | VernacDefineModule (_,(_,id), _, _, _) - | VernacDeclareModule (_,(_,id), _, _) - | VernacDeclareModuleType ((_,id), _, _) - | VernacAssumption (_, (_,((_,id)::_,_))::_) - | VernacInductive (_, (((_,id),_,_,_),_) :: _) -> - Reset (id, ref true) - | VernacDefinition (_, (_,id), ProveBody _, _) - | VernacStartTheoremProof (_, (_,id), _, _, _) -> - Reset (id, ref false) - | _ -> NoReset - -let reset_initial () = - prerr_endline "Reset initial called"; flush stderr; - Vernacentries.abort_refine Lib.reset_initial () - -let reset_to id = - prerr_endline ("Reset called with "^(string_of_id id)); - Vernacentries.abort_refine Lib.reset_name (Util.dummy_loc,id) -let reset_to_mod id = - prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); - Vernacentries.abort_refine Lib.reset_mod (Util.dummy_loc,id) - - let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) = [("clear "^ident),("clear "^ident^"."); @@ -480,21 +691,9 @@ let make_cases s = [] | _ -> raise Not_found -let is_state_preserving = function - | VernacPrint _ | VernacPrintOption _ | VernacGlobalCheck _ - | VernacCheckMayEval _ | VernacSearch _ | VernacLocate _ - | VernacShow _ | VernacMemOption _ | VernacComments _ - | VernacChdir None | VernacNop -> - prerr_endline "state preserving command found"; true - | _ -> - false - - 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 - - -- cgit v1.2.3