From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:01 +0200 Subject: Imported Upstream version 8.4dfsg --- toplevel/auto_ind_decl.ml | 2 +- toplevel/auto_ind_decl.mli | 2 +- toplevel/autoinstance.ml | 2 +- toplevel/autoinstance.mli | 2 +- toplevel/backtrack.ml | 22 ++++++- toplevel/backtrack.mli | 10 +++- toplevel/cerrors.ml | 2 +- toplevel/cerrors.mli | 2 +- toplevel/class.ml | 2 +- toplevel/class.mli | 2 +- toplevel/classes.ml | 2 +- toplevel/classes.mli | 2 +- toplevel/command.ml | 9 +-- toplevel/command.mli | 2 +- toplevel/coqinit.ml | 10 +++- toplevel/coqinit.mli | 4 +- toplevel/coqtop.ml | 21 ++++--- toplevel/coqtop.mli | 2 +- toplevel/discharge.ml | 2 +- toplevel/discharge.mli | 2 +- toplevel/himsg.ml | 57 +++++++++--------- toplevel/himsg.mli | 2 +- toplevel/ide_intf.ml | 43 ++++++++++---- toplevel/ide_intf.mli | 2 +- toplevel/ide_slave.ml | 45 +++++++++------ toplevel/ide_slave.mli | 2 +- toplevel/ind_tables.ml | 2 +- toplevel/ind_tables.mli | 2 +- toplevel/indschemes.ml | 2 +- toplevel/indschemes.mli | 2 +- toplevel/interface.mli | 16 +++-- toplevel/lemmas.ml | 2 +- toplevel/lemmas.mli | 2 +- toplevel/libtypes.ml | 2 +- toplevel/libtypes.mli | 2 +- toplevel/metasyntax.ml | 20 +++++-- toplevel/metasyntax.mli | 4 +- toplevel/mltop.ml4 | 135 ++++++++++++++++++++++--------------------- toplevel/mltop.mli | 25 +++----- toplevel/record.ml | 2 +- toplevel/record.mli | 2 +- toplevel/search.ml | 2 +- toplevel/search.mli | 2 +- toplevel/toplevel.ml | 2 +- toplevel/toplevel.mli | 2 +- toplevel/usage.ml | 4 +- toplevel/usage.mli | 2 +- toplevel/vernac.ml | 39 ++++++++++++- toplevel/vernac.mli | 2 +- toplevel/vernacentries.ml | 141 +++++++++++++++++++++++++++++++++++++++------ toplevel/vernacentries.mli | 4 +- toplevel/vernacexpr.ml | 18 ++++-- toplevel/vernacinterp.ml | 2 +- toplevel/vernacinterp.mli | 2 +- toplevel/whelp.ml4 | 2 +- toplevel/whelp.mli | 2 +- 56 files changed, 462 insertions(+), 239 deletions(-) (limited to 'toplevel') diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index f4dab15f..3690b924 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* while i != Stack.top history do pop () done +(** An auxiliary function to retrieve the number of remaining subgoals *) + +let get_ngoals () = + try + let prf = Proof_global.give_me_the_proof () in + List.length (Evd.sig_it (Proof.V82.background_subgoals prf)) + with Proof_global.NoCurrentProof -> 0 + (** Register the end of a command and store the current state *) let mark_command ast = @@ -85,6 +99,7 @@ let mark_command ast = prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None); prfdepth = max 0 (Pfedit.current_proof_depth ()); reachable = true; + ngoals = get_ngoals (); cmd = ast } history @@ -175,6 +190,7 @@ let reset_initial () = nproofs = 0; prfname = None; prfdepth = 0; + ngoals = 0; reachable = true; cmd = VernacNop } history @@ -215,10 +231,10 @@ let get_script prf = | _ -> () in (try Stack.iter select history with Not_found -> ()); - (* Get rid of intermediate commands which don't grow the depth *) + (* Get rid of intermediate commands which don't grow the proof depth *) let rec filter n = function | [] -> [] - | {prfdepth=d; cmd=c}::l when n < d -> c :: filter d l + | {prfdepth=d; cmd=c; ngoals=ng}::l when n < d -> (c,ng) :: filter d l | {prfdepth=d}::l -> filter d l in (* initial proof depth (after entering the lemma statement) is 1 *) diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli index 3fde5b11..413ecd2e 100644 --- a/toplevel/backtrack.mli +++ b/toplevel/backtrack.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit +(** Is this history stack active (i.e. nonempty) ? + The stack is currently inactive when compiling files (coqc). *) + +val is_active : unit -> bool + (** The [Invalid] exception is raised when one of the following function tries to empty the history stack, or reach an unknown states, etc. The stack is preserved in these cases. *) @@ -76,7 +81,7 @@ val mark_unreachable : ?after:int -> Names.identifier list -> unit (** Parse the history stack for printing the script of a proof *) -val get_script : Names.identifier -> Vernacexpr.vernac_expr list +val get_script : Names.identifier -> (Vernacexpr.vernac_expr * int) list (** For debug purpose, a dump of the history *) @@ -86,6 +91,7 @@ type info = { nproofs : int; prfname : Names.identifier option; prfdepth : int; + ngoals : int; cmd : Vernacexpr.vernac_expr; mutable reachable : bool; } diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 5f2c3dbb..3b6f0f7c 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* false - (* Very syntactical equality *) let eq_local_binder d1 d2 = match d1,d2 with | LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) -> List.length nal1 = List.length nal2 && k1 = k2 && List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 && - eq_constr_expr c1 c2 + Constrextern.is_same_type c1 c2 | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) -> - id1 = id2 && eq_constr_expr c1 c2 + id1 = id2 && Constrextern.is_same_type c1 c2 | _ -> false diff --git a/toplevel/command.mli b/toplevel/command.mli index 8ffdbdec..b1cf2053 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Flags.V8_3 + | "8.2" -> Flags.V8_2 + | ("8.1" | "8.0") as s -> + warning ("Compatibility with version "^s^" not supported."); + Flags.V8_2 + | s -> Util.error ("Unknown compatibility version \""^s^"\".") diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 43b1556d..9ca1deb4 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit val init_library_roots : unit -> unit val init_ocaml_path : unit -> unit + +val get_compat_version : string -> Flags.compat_version diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a60e0d82..df388d1d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* compat_version := Some V8_3 - | "8.2" -> compat_version := Some V8_2 - | "8.1" -> warning "Compatibility with version 8.1 not supported." - | "8.0" -> warning "Compatibility with version 8.0 not supported." - | s -> error ("Unknown compatibility version \""^s^"\".") - (*s options for the virtual machine *) let boxed_val = ref false @@ -152,6 +145,9 @@ let warning s = msg_warning (str s) let ide_slave = ref false let filter_opts = ref false +let verb_compat_ntn = ref false +let no_compat_ntn = ref false + let parse_args arglist = let glob_opt = ref false in let rec parse = function @@ -243,9 +239,13 @@ let parse_args arglist = | "-debug" :: rem -> set_debug (); parse rem - | "-compat" :: v :: rem -> set_compat_version v; parse rem + | "-compat" :: v :: rem -> + Flags.compat_version := get_compat_version v; parse rem | "-compat" :: [] -> usage () + | "-verbose-compat-notations" :: rem -> verb_compat_ntn := true; parse rem + | "-no-compat-notations" :: rem -> no_compat_ntn := true; parse rem + | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); @@ -332,6 +332,9 @@ let init arglist = Mltop.init_known_plugins (); set_vm_opt (); engage (); + (* Be careful to set these variables after the inputstate *) + Syntax_def.set_verbose_compat_notations !verb_compat_ntn; + Syntax_def.set_compat_notations (not !no_compat_ntn); if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 16d2b874..73e21484 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - (match Typeclasses.class_of_constr evi.evar_concl with - | Some c -> - let env = Evd.evar_env evi in - fnl () ++ str "Could not find an instance for " ++ - pr_lconstr_env env evi.evar_concl ++ - pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env - | None -> mt()) + match Typeclasses.class_of_constr evi.evar_concl with + | Some c -> + let env = Evd.evar_env evi in + fnl () ++ str "Could not find an instance for " ++ + pr_lconstr_env env evi.evar_concl ++ + pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env | _ -> mt() let explain_unsolvable_implicit env evi k explain = @@ -698,12 +695,8 @@ let explain_no_instance env (_,id) l = let is_goal_evar evi = match evi.evar_source with (_, GoalEvar) -> true | _ -> false let pr_constraints printenv env evm = - let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evm) in - let evm = fold_undefined - (fun ev evi evm' -> - if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm - in let l = Evd.to_list evm in + assert(l <> []); let (ev, evi) = List.hd l in if List.for_all (fun (ev', evi') -> eq_named_context_val evi.evar_hyps evi'.evar_hyps) l @@ -719,18 +712,23 @@ let pr_constraints printenv env evm = pr_evar_map None evm let explain_unsatisfiable_constraints env evd constr = - let evm = Evarutil.nf_evar_map evd in - let undef = Evd.undefined_evars evm in + let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evd) in + (* Remove goal evars *) + let undef = fold_undefined + (fun ev evi evm' -> + if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm + in match constr with | None -> str"Unable to satisfy the following constraints:" ++ fnl() ++ pr_constraints true env undef | Some (ev, k) -> - explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++ - if List.length (Evd.to_list undef) > 1 then - str"With the following constraints:" ++ fnl() ++ - pr_constraints false env (Evd.remove undef ev) - else mt () + explain_typeclass_resolution env (Evd.find evm ev) k ++ fnl () ++ + (let remaining = Evd.remove undef ev in + if Evd.has_undefined remaining then + str"With the following constraints:" ++ fnl() ++ + pr_constraints false env remaining + else mt ()) let explain_mismatched_contexts env c i j = str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ @@ -995,6 +993,11 @@ let explain_reduction_tactic_error = function let explain_ltac_call_trace (nrep,last,trace,loc) = let calls = (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) in + let tacexpr_differ te te' = + (* NB: The following comparison may raise an exception + since a tacexpr may embed a functional part via a TacExtend *) + try te <> te' with Invalid_argument _ -> false + in let pr_call (n,ck) = (match ck with | Proof_type.LtacNotationCall s -> quote (str s) @@ -1006,11 +1009,11 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (dummy_loc,te))) ++ (match !otac with - | Some te' when (Obj.magic te' <> te) -> - strbrk " (expanded to " ++ quote - (Pptactic.pr_tactic (Global.env()) - (Tacexpr.TacAtom (dummy_loc,te'))) - ++ str ")" + | Some te' when tacexpr_differ (Obj.magic te') te -> + strbrk " (expanded to " ++ quote + (Pptactic.pr_tactic (Global.env()) + (Tacexpr.TacAtom (dummy_loc,te'))) + ++ str ")" | _ -> mt ()) | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) -> let filter = diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index a763472b..84d3ec95 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* +| Element ("status", [], [path; name; prfs; snum; pnum]) -> { - status_path = to_option to_string path; + status_path = to_list to_string path; status_proofname = to_option to_string name; + status_allproofs = to_list to_string prfs; + status_statenum = to_int snum; + status_proofnum = to_int pnum; } | _ -> raise Marshal_error @@ -370,14 +382,16 @@ let to_goal = function | _ -> raise Marshal_error let of_goals g = + let of_glist = of_list of_goal in let fg = of_list of_goal g.fg_goals in - let bg = of_list of_goal g.bg_goals in + let bg = of_list (of_pair of_glist of_glist) g.bg_goals in Element ("goals", [], [fg; bg]) let to_goals = function | Element ("goals", [], [fg; bg]) -> + let to_glist = to_list to_goal in let fg = to_list to_goal fg in - let bg = to_list to_goal bg in + let bg = to_list (to_pair to_glist to_glist) bg in { fg_goals = fg; bg_goals = bg; } | _ -> raise Marshal_error @@ -495,9 +509,9 @@ let pr_string s = "["^s^"]" let pr_bool b = if b then "true" else "false" let pr_status s = - let path = match s.status_path with - | None -> "no path; " - | Some p -> "path = " ^ p ^ "; " + let path = + let l = String.concat "." s.status_path in + "path=" ^ l ^ ";" in let name = match s.status_proofname with | None -> "no proof;" @@ -512,7 +526,14 @@ let pr_mkcases l = let pr_goals_aux g = if g.fg_goals = [] then if g.bg_goals = [] then "Proof completed." - else Printf.sprintf "Still %i unfocused goals." (List.length g.bg_goals) + else + let rec pr_focus _ = function + | [] -> assert false + | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg) + | (lg, rg) :: l -> + Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l + in + Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals else let pr_menu s = s in let pr_goal { goal_hyp = hyps; goal_ccl = goal } = diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli index deee50e5..26c6b671 100644 --- a/toplevel/ide_intf.mli +++ b/toplevel/ide_intf.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* "),("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") @@ -150,11 +150,11 @@ let concl_next_tac sigma concl = "intro"; "intros"; "intuition" - ] @ (if Hipattern.is_equality_type (Goal.V82.concl sigma concl) then [ + ] @ [ "reflexivity"; "discriminate"; "symmetry" - ] else []) @ [ + ] @ [ "assumption"; "omega"; "ring"; @@ -180,19 +180,21 @@ let process_goal sigma g = 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_id = id; } -(* hyps,(ccl,concl_next_tac sigma g)) *) let goals () = try let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in - let fg = List.map (process_goal sigma) all_goals in - let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in - let bg = List.map (process_goal sigma) bgoals in + let (goals, zipper, sigma) = Proof.proof pfts in + let fg = List.map (process_goal sigma) goals in + let map_zip (lg, rg) = + let lg = List.map (process_goal sigma) lg in + let rg = List.map (process_goal sigma) rg in + (lg, rg) + in + let bg = List.map map_zip zipper in Some { Interface.fg_goals = fg; Interface.bg_goals = bg; } with Proof_global.NoCurrentProof -> None @@ -231,16 +233,23 @@ let status () = and display the other parts (opened sections and modules) *) let path = let l = Names.repr_dirpath (Lib.cwd ()) in - let l = snd (Util.list_sep_last l) in - if l = [] then None - else Some (Names.string_of_dirpath (Names.make_dirpath l)) + List.rev_map Names.string_of_id l in let proof = - try - Some (Names.string_of_id (Pfedit.get_current_proof_name ())) + try Some (Names.string_of_id (Proof_global.get_current_proof_name ())) with _ -> None in - { Interface.status_path = path; Interface.status_proofname = proof } + let allproofs = + let l = Proof_global.get_all_proof_names () in + List.map Names.string_of_id l + in + { + Interface.status_path = path; + Interface.status_proofname = proof; + Interface.status_allproofs = allproofs; + Interface.status_statenum = Lib.current_command_label (); + Interface.status_proofnum = Pfedit.current_proof_depth (); + } (** This should be elsewhere... *) let search flags = diff --git a/toplevel/ide_slave.mli b/toplevel/ide_slave.mli index 13dff280..fb927cf3 100644 --- a/toplevel/ide_slave.mli +++ b/toplevel/ide_slave.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* if assoc <> None then error"An associativity is given more than once."; interp (Some a) level etyps format l - | SetOnlyParsing :: l -> + | SetOnlyParsing _ :: l -> onlyparsing := true; interp assoc level etyps format l | SetFormat s :: l -> @@ -770,8 +770,13 @@ let check_infix_modifiers modifiers = if t <> [] then error "Explicit entry level or type unexpected in infix notation." -let no_syntax_modifiers modifiers = - modifiers = [] or modifiers = [SetOnlyParsing] +let no_syntax_modifiers = function + | [] | [SetOnlyParsing _] -> true + | _ -> false + +let is_only_parsing = function + | [SetOnlyParsing _] -> true + | _ -> false (* Compute precedences from modifiers (or find default ones) *) @@ -1118,7 +1123,7 @@ let add_notation local c ((loc,df),modifiers) sc = let df' = if no_syntax_modifiers modifiers then (* No syntax data: try to rely on a previously declared rule *) - let onlyparse = modifiers=[SetOnlyParsing] in + let onlyparse = is_only_parsing modifiers in try add_notation_interpretation_core local df c sc onlyparse with NoSyntaxRule -> (* Try to determine a default syntax rule *) @@ -1193,6 +1198,9 @@ let add_syntactic_definition ident (vars,c) local onlyparse = let vars,pat = interp_aconstr i_vars [] c in List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat in - let onlyparse = onlyparse or is_not_printable pat in + let onlyparse = match onlyparse with + | None when (is_not_printable pat) -> Some Flags.Current + | p -> p + in Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 32568854..38a0ae59 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* identifier list * constr_expr -> - bool -> bool -> unit + bool -> Flags.compat_version option -> unit (** Print the Camlp4 state of a grammar *) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 025c972f..2059ca60 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* f()) !known_loaded_plugins + +(** ml object = ml module or plugin *) + let init_ml_object mname = try Stringmap.find mname !known_loaded_plugins () with Not_found -> () @@ -246,81 +253,75 @@ let load_ml_object mname fname= add_known_module mname; init_ml_object mname -let add_known_plugin init name = - let name = String.capitalize name in - add_known_module name; - known_loaded_plugins := Stringmap.add name init !known_loaded_plugins - -let init_known_plugins () = - Stringmap.iter (fun _ f -> f()) !known_loaded_plugins - (* Summary of declared ML Modules *) -(* List and not Stringset because order is important *) +(* List and not Stringset because order is important: most recent first. *) + let loaded_modules = ref [] -let get_loaded_modules () = !loaded_modules +let get_loaded_modules () = List.rev !loaded_modules let add_loaded_module md = loaded_modules := md :: !loaded_modules +let reset_loaded_modules () = loaded_modules := [] -let orig_loaded_modules = ref !loaded_modules -let init_ml_modules () = loaded_modules := !orig_loaded_modules +let if_verbose_load verb f name fname = + if not verb then f name fname + else + let info = "[Loading ML file "^fname^" ..." in + try + f name fname; + msgnl (str (info^" done]")); + with e -> + msgnl (str (info^" failed]")); + raise e + +(** Load a module for the first time (i.e. dynlink it) + or simulate its reload (i.e. doing nothing except maybe + an initialization function). *) + +let cache_ml_object verb reinit name = + begin + if module_is_known name then + (if reinit then init_ml_object name) + else if not has_dynlink then + error ("Dynamic link not supported (module "^name^")") + else + if_verbose_load (verb && is_verbose ()) + load_ml_object name (file_of_name name) + end; + add_loaded_module name let unfreeze_ml_modules x = - loaded_modules := []; - List.iter - (fun name -> - let mname = mod_of_name name in - if not (module_is_known mname) then - if has_dynlink then - let fname = file_of_name mname in - load_ml_object mname fname - else - errorlabstrm "Mltop.unfreeze_ml_modules" - (str"Loading of ML object file forbidden in a native Coq.") - else init_ml_object mname; - add_loaded_module mname) - x + reset_loaded_modules (); + List.iter (cache_ml_object false false) x let _ = Summary.declare_summary "ML-MODULES" - { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules())); - Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x); - Summary.init_function = (fun () -> init_ml_modules ()) } - -(* Same as restore_ml_modules, but verbosely *) - -let cache_ml_module_object (_,{mnames=mnames}) = - List.iter - (fun name -> - let mname = mod_of_name name in - if not (module_is_known mname) then - if has_dynlink then - let fname = file_of_name mname in - try - if_verbose - msg (str"[Loading ML file " ++ str fname ++ str" ..."); - load_ml_object mname fname; - if_verbose msgnl (str" done]"); - add_loaded_module mname - with e -> - if_verbose msgnl (str" failed]"); - raise e - else - (if_verbose msgnl (str" failed]"); - error ("Dynamic link not supported (module "^name^")")) - else init_ml_object mname) - mnames - -let classify_ml_module_object ({mlocal=mlocal} as o) = + { Summary.freeze_function = get_loaded_modules; + Summary.unfreeze_function = unfreeze_ml_modules; + Summary.init_function = reset_loaded_modules } + +(* Liboject entries of declared ML Modules *) + +type ml_module_object = { + mlocal : Vernacexpr.locality_flag; + mnames : string list +} + +let cache_ml_objects (_,{mnames=mnames}) = + List.iter (cache_ml_object true true) mnames + +let classify_ml_objects ({mlocal=mlocal} as o) = if mlocal then Dispose else Substitute o let inMLModule : ml_module_object -> obj = - declare_object {(default_object "ML-MODULE") with - load_function = (fun _ -> cache_ml_module_object); - cache_function = cache_ml_module_object; - subst_function = (fun (_,o) -> o); - classify_function = classify_ml_module_object } + declare_object + {(default_object "ML-MODULE") with + load_function = (fun _ -> cache_ml_objects); + cache_function = cache_ml_objects; + subst_function = (fun (_,o) -> o); + classify_function = classify_ml_objects } let declare_ml_modules local l = + let l = List.map mod_of_name l in Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l}) let print_ml_path () = @@ -328,7 +329,7 @@ let print_ml_path () = ppnl (str"ML Load Path:" ++ fnl () ++ str" " ++ hv 0 (prlist_with_sep pr_fnl pr_str l)) - (* Printing of loaded ML modules *) +(* Printing of loaded ML modules *) let print_ml_modules () = let l = get_loaded_modules () in diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 99b96ed7..ebea73f1 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit val module_is_known : string -> bool val load_ml_object : string -> string -> unit -(* Declare a plugin and its initialization function. - * A plugin is just an ML module with an initialization function. - * Adding a known plugin implies adding it as a known ML module. - * The initialization function is granted to be called after Coq is fully - * bootstrapped, even if the plugin is statically linked with the toplevel *) +(** Declare a plugin and its initialization function. + A plugin is just an ML module with an initialization function. + Adding a known plugin implies adding it as a known ML module. + The initialization function is granted to be called after Coq is fully + bootstrapped, even if the plugin is statically linked with the toplevel *) val add_known_plugin : (unit -> unit) -> string -> unit -(* Calls all initialization functions in a non-specified order *) +(** Calls all initialization functions in a non-specified order *) val init_known_plugins : unit -> unit -(** Summary of Declared ML Modules *) -val get_loaded_modules : unit -> string list -val add_loaded_module : string -> unit -val init_ml_modules : unit -> unit -val unfreeze_ml_modules : string list -> unit - -type ml_module_object = { - mlocal: Vernacexpr.locality_flag; - mnames: string list; -} - val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit val print_ml_path : unit -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index 0c55861f..3708c2f7 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* !atomic_load); + Goptions.optwrite = ((:=) atomic_load) } + (* Specifies which file is read. The intermediate file names are discarded here. The Drop exception becomes an error. We forget if the error ocurred during interpretation or not *) @@ -272,16 +296,24 @@ and read_vernac_file verbosely s = else Flags.silently Vernacentries.interp in let checknav loc cmd = - if is_navigation_vernac cmd then + if is_navigation_vernac cmd && not (is_reset cmd) then user_error loc "Navigation commands forbidden in files" in + let end_inner_command cmd = + if !atomic_load || is_reset cmd then + Lib.mark_end_of_command () (* for Reset in coqc or coqtop -l *) + else + Backtrack.mark_command cmd; (* for Show Script, cf bug #2820 *) + in let (in_chan, fname, input) = open_file_twice_if verbosely s in try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do - vernac_com interpfun checknav (parse_sentence input); + let loc_ast = parse_sentence input in + vernac_com interpfun checknav loc_ast; + end_inner_command (snd loc_ast); pp_flush () done with e -> (* whatever the exception *) @@ -324,6 +356,7 @@ let load_vernac verb file = chan_beautify := if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout; try + Lib.mark_end_of_command (); (* in case we're still in coqtop init *) read_vernac_file verb file; if !Flags.beautify_file then close_out !chan_beautify; with e -> diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index bcfe9b71..96bc8865 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ngprev then + (* We've branched *) + (ng - ngprev + 1, ng1 - 1 :: ngl1) + else if ng < ngprev then + (* A subgoal have been solved. Let's compute the new current level + by discarding all levels with 0 remaining goals. *) + let _ = assert (ng = ngprev - 1) in + let rec loop = function + | (0, ng2::ngl2) -> loop (ng2,ngl2) + | p -> p + in loop (ng1-1, ngl1) + else + (* Standard case, same goal number as before *) + (ng1, ngl1) + in + (* When a subgoal have been solved, separate this block by an empty line *) + let new_nl = (ng < ngprev) + in + (* Indentation depth *) + let ind = List.length ngl1 + in + (* Some special handling of bullets and { }, to get a nicer display *) + let pred n = max 0 (n-1) in + let ind, nl, new_beginend = match cmd with + | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend + | VernacEndSubproof -> List.hd beginend, false, List.tl beginend + | VernacBullet _ -> pred ind, nl, beginend + | _ -> ind, nl, beginend + in + let pp = + (if nl then fnl () else mt ()) ++ + (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)) + in + (new_ngl, new_nl, new_beginend, pp :: ppl) + let show_script () = let prf = Pfedit.get_current_proof_name () in let cmds = Backtrack.get_script prf in - msgnl (Util.prlist_with_sep Pp.fnl Ppvernac.pr_vernac cmds) + let _,_,_,indented_cmds = + List.fold_left indent_script_item ((1,[]),false,[],[]) cmds + in + let indented_cmds = List.rev (indented_cmds) in + msgnl (v 0 (Util.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds)) let show_thesis () = msgnl (anomaly "TODO" ) @@ -311,6 +360,11 @@ let smart_global r = Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr; gr +let dump_global r = + try + let gr = Smartlocate.smart_global r in + Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr + with _ -> () (**********) (* Syntax *) @@ -389,8 +443,10 @@ let vernac_end_proof = function let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) - by (Tactics.exact_proof c); - save_named true + let prf = Pfedit.get_current_proof_name () in + by (Tactics.exact_proof c); + save_named true; + Backtrack.mark_unreachable [prf] let vernac_assumption kind l nl= let global = fst kind = Global in @@ -458,9 +514,21 @@ let vernac_cofixpoint l = List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; do_cofixpoint l -let vernac_scheme = Indschemes.do_scheme - -let vernac_combined_scheme = Indschemes.do_combined_scheme +let vernac_scheme l = + if Dumpglob.dump () then + List.iter (fun (lid, s) -> + Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid; + match s with + | InductionScheme (_, r, _) + | CaseScheme (_, r, _) + | EqualityScheme r -> dump_global r) l; + Indschemes.do_scheme l + +let vernac_combined_scheme lid l = + if Dumpglob.dump () then + (Dumpglob.dump_definition lid false "def"; + List.iter (fun lid -> dump_global (Genarg.AN (Ident lid))) l); + Indschemes.do_combined_scheme lid l (**********************) (* Modules *) @@ -1190,6 +1258,7 @@ let vernac_check_may_eval redexp glopt rc = if !pcoq <> None then (Option.get !pcoq).print_check env j else msg (print_judgment env j) | Some r -> + Tacinterp.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in let redfun = fst (reduction_of_red_expr r_interp) in if !pcoq <> None @@ -1248,8 +1317,10 @@ let vernac_print = function pp (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) | PrintVisibility s -> pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) - | PrintAbout qid -> msg (print_about qid) - | PrintImplicit qid -> msg (print_impargs qid) + | PrintAbout qid -> + msg (print_about qid) + | PrintImplicit qid -> + dump_global qid; msg (print_impargs qid) | PrintAssumptions (o,r) -> (* Prints all the axioms and section variables used by a term *) let cstr = constr_of_global (smart_global r) in @@ -1340,10 +1411,43 @@ let vernac_back n = with Backtrack.Invalid -> error "Invalid backtrack." let vernac_reset_name id = - try Backtrack.reset_name id; try_print_subgoals () - with Backtrack.Invalid -> error "Invalid Reset." + try + let globalized = + try + let gr = Smartlocate.global_with_alias (Ident id) in + Dumpglob.add_glob (fst id) gr; + true + with _ -> false in + + if not globalized then begin + try begin match Lib.find_opening_node (snd id) with + | Lib.OpenedSection _ -> Dumpglob.dump_reference (fst id) + (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; + (* Might be nice to implement module cases, too.... *) + | _ -> () + end with UserError _ -> () + end; -let vernac_reset_initial () = Backtrack.reset_initial () + if Backtrack.is_active () then + (Backtrack.reset_name id; try_print_subgoals ()) + else + (* When compiling files, Reset is now allowed again + as asked by A. Chlipala. we emulate a simple reset, + that discards all proofs. *) + let lbl = Lib.label_before_name id in + Pfedit.delete_all_proofs (); + Pp.msg_warning (str "Reset command occurred in non-interactive mode."); + Lib.reset_label lbl + with Backtrack.Invalid | Not_found -> error "Invalid Reset." + + +let vernac_reset_initial () = + if Backtrack.is_active () then + Backtrack.reset_initial () + else begin + Pp.msg_warning (str "Reset command occurred in non-interactive mode."); + Lib.reset_label Lib.first_command_label + end (* For compatibility with ProofGeneral: *) @@ -1393,7 +1497,10 @@ let vernac_undoto n = let vernac_focus gln = let p = Proof_global.give_me_the_proof () in let n = match gln with None -> 1 | Some n -> n in - Proof.focus focus_command_cond () n p; print_subgoals () + if n = 0 then + Util.error "Invalid goal number: 0. Goal numbering starts with 1." + else + Proof.focus focus_command_cond () n p; print_subgoals () (* Unfocuses one step in the focus stack. *) let vernac_unfocus () = @@ -1594,11 +1701,11 @@ let interp c = match c with | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof (None, None) -> () - | VernacProof (Some tac, None) -> vernac_set_end_tac tac - | VernacProof (None, Some l) -> vernac_set_used_variables l + | VernacProof (None, None) -> print_subgoals () + | VernacProof (Some tac, None) -> vernac_set_end_tac tac ; print_subgoals () + | VernacProof (None, Some l) -> vernac_set_used_variables l ; print_subgoals () | VernacProof (Some tac, Some l) -> - vernac_set_end_tac tac; vernac_set_used_variables l + vernac_set_end_tac tac; vernac_set_used_variables l ; print_subgoals () | VernacProofMode mn -> Proof_global.set_proof_mode mn (* Toplevel control *) | VernacToplevelControl e -> raise e diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index a9d384ea..b0d41b15 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit + (** Vernacular entries *) val show_script : unit -> unit diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index d9f15337..3106e866 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Current, it contains the name of the coq version + which this notation is trying to be compatible with *) type option_value = Goptionstyp.option_value = | BoolValue of bool @@ -189,7 +192,7 @@ type syntax_modifier = | SetLevel of int | SetAssoc of gram_assoc | SetEntryType of string * simple_constr_prod_entry_key - | SetOnlyParsing + | SetOnlyParsing of Flags.compat_version | SetFormat of string located type proof_end = @@ -377,13 +380,20 @@ let rec is_navigation_vernac = function | VernacBacktrack _ | VernacBackTo _ | VernacBack _ -> true + | VernacTime c -> is_navigation_vernac c (* Time Back* is harmless *) | c -> is_deep_navigation_vernac c and is_deep_navigation_vernac = function - | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c + | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l | _ -> false +(* NB: Reset is now allowed again as asked by A. Chlipala *) + +let is_reset = function + | VernacResetInitial | VernacResetName _ -> true + | _ -> false + (* Locating errors raised just after the dot is parsed but before the interpretation phase *) diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 10c5a00f..c4cc4ae5 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*