From 442feb2c07f8f5824e814bba504f02c2742637e2 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:08:09 +0000 Subject: Vernacexpr is now a mli-only file, locality stuff now in locality.ml Adds a directory ./intf for pure interfaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CREDITS | 2 +- Makefile.common | 4 +- _tags | 1 + dev/ocamldebug-coq.template | 2 +- dev/printers.mllib | 2 +- intf/vernacexpr.mli | 357 +++++++++++++++++++++++++++++ lib/errors.ml | 2 + lib/errors.mli | 2 + parsing/g_ltac.ml4 | 1 + parsing/g_obligations.ml4 | 2 +- parsing/g_proofs.ml4 | 1 + parsing/g_vernac.ml4 | 1 + parsing/grammar.mllib | 2 +- plugins/firstorder/g_ground.ml4 | 2 +- tactics/eauto.ml4 | 2 +- tactics/rewrite.ml4 | 14 +- toplevel/ide_slave.ml | 6 +- toplevel/locality.ml | 112 +++++++++ toplevel/locality.mli | 61 +++++ toplevel/toplevel.ml | 13 +- toplevel/toplevel.mllib | 2 +- toplevel/vernac.ml | 15 ++ toplevel/vernac.mli | 3 + toplevel/vernacentries.ml | 2 +- toplevel/vernacexpr.ml | 497 ---------------------------------------- toplevel/vernacinterp.ml | 1 - 26 files changed, 583 insertions(+), 526 deletions(-) create mode 100644 intf/vernacexpr.mli create mode 100644 toplevel/locality.ml create mode 100644 toplevel/locality.mli delete mode 100644 toplevel/vernacexpr.ml diff --git a/CREDITS b/CREDITS index 35057ea8f..c654db2ee 100644 --- a/CREDITS +++ b/CREDITS @@ -12,7 +12,7 @@ The "Coq proof assistant" was jointly developed by All files of the "Coq proof assistant" in directories or sub-directories of - config dev ide interp kernel lib library parsing pretyping proofs + config dev ide interp intf kernel lib library parsing pretyping proofs scripts states tactics test-suite theories tools toplevel are distributed under the terms of the GNU Lesser General Public License diff --git a/Makefile.common b/Makefile.common index 22b06a40e..d5b152432 100644 --- a/Makefile.common +++ b/Makefile.common @@ -72,7 +72,7 @@ SRCDIRS:=\ config tools tools/coqdoc scripts lib \ kernel kernel/byterun library proofs tactics \ pretyping interp toplevel/utils toplevel parsing \ - ide/utils ide \ + intf ide/utils ide \ $(addprefix plugins/, \ omega romega micromega quote ring \ setoid_ring xml extraction fourier \ @@ -345,7 +345,7 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ OCAMLDOCDIR=dev/ocamldoc -DOCMLIS=$(wildcard ./lib/*.mli ./kernel/*.mli ./library/*.mli \ +DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ ./pretyping/*.mli ./interp/*.mli \ ./parsing/*.mli ./proofs/*.mli \ ./tactics/*.mli ./toplevel/*.mli) diff --git a/_tags b/_tags index cf8319bd9..08dc9f1af 100644 --- a/_tags +++ b/_tags @@ -64,6 +64,7 @@ "ide": include "ide/utils": include "interp": include +"intf": include "kernel": include "kernel/byterun": include "lib": include diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template index 743205888..5358673ff 100644 --- a/dev/ocamldebug-coq.template +++ b/dev/ocamldebug-coq.template @@ -13,7 +13,7 @@ exec $OCAMLDEBUG \ -I $CAMLP4LIB \ -I $COQTOP \ -I $COQTOP/config \ - -I $COQTOP/lib -I $COQTOP/kernel \ + -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \ -I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ diff --git a/dev/printers.mllib b/dev/printers.mllib index f93d01daf..c1a95cdb2 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -137,6 +137,6 @@ Tactic_printer Egrammar Himsg Cerrors -Vernacexpr +Locality Vernacinterp Top_printers diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli new file mode 100644 index 000000000..238400806 --- /dev/null +++ b/intf/vernacexpr.mli @@ -0,0 +1,357 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit exception Timeout +exception Drop +exception Quit (** Like [Exc_located], but specifies the outermost file read, the input buffer associated to the location of the error (or the module name diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 2f129637d..bf0e13e02 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -12,6 +12,7 @@ open Topconstr open Glob_term open Tacexpr open Vernacexpr +open Locality open Pcoq open Prim open Tactic diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 index f86fd0fec..8ec546ffd 100644 --- a/parsing/g_obligations.ml4 +++ b/parsing/g_obligations.ml4 @@ -117,7 +117,7 @@ VERNAC COMMAND EXTEND Admit_Obligations VERNAC COMMAND EXTEND Set_Solver | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ set_default_tactic - (Vernacexpr.use_section_locality ()) + (Locality.use_section_locality ()) (Tacinterp.glob_tactic t) ] END diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 23e7e31bf..5f44a9e9c 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -13,6 +13,7 @@ open Util open Vernac_ open Topconstr open Vernacexpr +open Locality open Prim open Constr open Tok diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 320ca4eb0..f684b9a0d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -15,6 +15,7 @@ open Names open Topconstr open Extend open Vernacexpr +open Locality open Pcoq open Tactic open Decl_kinds diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index 0d7cd3649..39fd88506 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -71,7 +71,7 @@ Tacexpr Tok Lexer Extend -Vernacexpr +Locality Extrawit Pcoq Q_util diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 48bb87214..a5ee551a5 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -59,7 +59,7 @@ let (set_default_solver, default_solver, print_default_solver) = VERNAC COMMAND EXTEND Firstorder_Set_Solver | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [ set_default_solver - (Vernacexpr.use_section_locality ()) + (Locality.use_section_locality ()) (Tacinterp.glob_tactic t) ] END diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index fb9439d73..2700b2b7d 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -613,6 +613,6 @@ END VERNAC COMMAND EXTEND HintCut | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ let entry = HintsCutEntry p in - Auto.add_hints (Vernacexpr.use_section_locality ()) + Auto.add_hints (Locality.use_section_locality ()) (match dbnames with None -> ["core"] | Some l -> l) entry ] END diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 458c5bec6..88170d6dd 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1477,7 +1477,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = new_instance binders instance (Some (CRecord (dummy_loc,None,fields))) - ~global:(not (Vernacexpr.use_section_locality ())) ~generalize:false None + ~global:(not (Locality.use_section_locality ())) ~generalize:false None let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" @@ -1496,7 +1496,7 @@ let declare_instance_trans global binders a aeq n lemma = let declare_relation ?(binders=[]) a aeq n refl symm trans = init_setoid (); - let global = not (Vernacexpr.use_section_locality ()) in + let global = not (Locality.use_section_locality ()) in let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in ignore(anew_instance global binders instance []); match (refl,symm,trans) with @@ -1754,16 +1754,16 @@ let add_morphism glob binders m s n = VERNAC COMMAND EXTEND AddSetoid1 [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Vernacexpr.use_section_locality ())) [] a aeq t n ] + [ add_setoid (not (Locality.use_section_locality ())) [] a aeq t n ] | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Vernacexpr.use_section_locality ())) binders a aeq t n ] + [ add_setoid (not (Locality.use_section_locality ())) binders a aeq t n ] | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> - [ add_morphism_infer (not (Vernacexpr.use_section_locality ())) m n ] + [ add_morphism_infer (not (Locality.use_section_locality ())) m n ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> - [ add_morphism (not (Vernacexpr.use_section_locality ())) [] m s n ] + [ add_morphism (not (Locality.use_section_locality ())) [] m s n ] | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> - [ add_morphism (not (Vernacexpr.use_section_locality ())) binders m s n ] + [ add_morphism (not (Locality.use_section_locality ())) binders m s n ] END (** Bind to "rewrite" too *) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 292c288a8..cc3c7c18d 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -102,7 +102,7 @@ let coqide_cmd_checks (loc,ast) = user_error "Debug mode not available within CoqIDE"; if is_known_option ast then user_error "Use CoqIDE display menu instead"; - if is_navigation_vernac ast then + if Vernac.is_navigation_vernac ast then user_error "Use CoqIDE navigation instead"; if is_undo ast then msgerrnl (str "Warning: rather use CoqIDE navigation instead"); @@ -362,8 +362,8 @@ let eval_call c = 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!" + | Errors.Drop -> None, "Drop is not allowed by coqide!" + | Errors.Quit -> None, "Quit is not allowed by coqide!" | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner | Error_in_file (_,_,inner) -> None, pr_exn inner | Loc.Exc_located (loc, inner) when loc = dummy_loc -> None, pr_exn inner diff --git a/toplevel/locality.ml b/toplevel/locality.ml new file mode 100644 index 000000000..436250c92 --- /dev/null +++ b/toplevel/locality.ml @@ -0,0 +1,112 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Decl_kinds.Local + | false -> Decl_kinds.Global + +let check_locality () = + match !locality_flag with + | Some (loc,b) -> + let s = if b then "Local" else "Global" in + Errors.user_err_loc + (loc,"",Pp.str ("This command does not support the \""^s^"\" prefix.")) + | None -> () + +(** Extracting the locality flag *) + +(* Commands which supported an inlined Local flag *) + +let enforce_locality_full local = + let local = + match !locality_flag with + | Some (_,false) when local -> + Errors.error "Cannot be simultaneously Local and Global." + | Some (_,true) when local -> + Errors.error "Use only prefix \"Local\"." + | None -> + if local then begin + Flags.if_warn + Pp.msg_warning (Pp.str"Obsolete syntax: use \"Local\" as a prefix."); + Some true + end else + None + | Some (_,b) -> Some b in + locality_flag := None; + local + +(* Commands which did not supported an inlined Local flag (synonym of + [enforce_locality_full false]) *) + +let use_locality_full () = + let r = Option.map snd !locality_flag in + locality_flag := None; + r + +(** Positioning locality for commands supporting discharging and export + outside of modules *) + +(* For commands whose default is to discharge and export: + Global is the default and is neutral; + Local in a section deactivates discharge, + Local not in a section deactivates export *) + +let make_locality = function Some true -> true | _ -> false + +let use_locality () = make_locality (use_locality_full ()) + +let use_locality_exp () = local_of_bool (use_locality ()) + +let enforce_locality local = make_locality (enforce_locality_full local) + +let enforce_locality_exp local = local_of_bool (enforce_locality local) + +(* For commands whose default is not to discharge and not to export: + Global forces discharge and export; + Local is the default and is neutral *) + +let use_non_locality () = + match use_locality_full () with Some false -> false | _ -> true + +(* For commands whose default is to not discharge but to export: + Global in sections forces discharge, Global not in section is the default; + Local in sections is the default, Local not in section forces non-export *) + +let make_section_locality = + function Some b -> b | None -> Lib.sections_are_opened () + +let use_section_locality () = + make_section_locality (use_locality_full ()) + +let enforce_section_locality local = + make_section_locality (enforce_locality_full local) + +(** Positioning locality for commands supporting export but not discharge *) + +(* For commands whose default is to export (if not in section): + Global in sections is forbidden, Global not in section is neutral; + Local in sections is the default, Local not in section forces non-export *) + +let make_module_locality = function + | Some false -> + if Lib.sections_are_opened () then + Errors.error + "This command does not support the Global option in sections."; + false + | Some true -> true + | None -> false + +let use_module_locality () = + make_module_locality (use_locality_full ()) + +let enforce_module_locality local = + make_module_locality (enforce_locality_full local) diff --git a/toplevel/locality.mli b/toplevel/locality.mli new file mode 100644 index 000000000..5e8d45d87 --- /dev/null +++ b/toplevel/locality.mli @@ -0,0 +1,61 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +(** * Extracting the locality flag *) + +(** Commands which supported an inlined Local flag *) + +val enforce_locality_full : bool -> bool option + +(** Commands which did not supported an inlined Local flag + (synonym of [enforce_locality_full false]) *) + +val use_locality_full : unit -> bool option + +(** * Positioning locality for commands supporting discharging and export + outside of modules *) + +(** For commands whose default is to discharge and export: + Global is the default and is neutral; + Local in a section deactivates discharge, + Local not in a section deactivates export *) + +val make_locality : bool option -> bool +val use_locality : unit -> bool +val use_locality_exp : unit -> Decl_kinds.locality +val enforce_locality : bool -> bool +val enforce_locality_exp : bool -> Decl_kinds.locality + +(** For commands whose default is not to discharge and not to export: + Global forces discharge and export; + Local is the default and is neutral *) + +val use_non_locality : unit -> bool + +(** For commands whose default is to not discharge but to export: + Global in sections forces discharge, Global not in section is the default; + Local in sections is the default, Local not in section forces non-export *) + +val make_section_locality : bool option -> bool +val use_section_locality : unit -> bool +val enforce_section_locality : bool -> bool + +(** * Positioning locality for commands supporting export but not discharge *) + +(** For commands whose default is to export (if not in section): + Global in sections is forbidden, Global not in section is neutral; + Local in sections is the default, Local not in section forces non-export *) + +val make_module_locality : bool option -> bool +val use_module_locality : unit -> bool +val enforce_module_locality : bool -> bool diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 6a06ba3dc..952f80aad 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -12,7 +12,6 @@ open Util open Flags open Cerrors open Vernac -open Vernacexpr open Pcoq open Compat @@ -302,11 +301,11 @@ let print_toplevel_error exc = match exc with | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0 - | Vernacexpr.Drop -> (* Last chance *) - if Mltop.is_ocaml_top() then raise Vernacexpr.Drop; + | Errors.Drop -> (* Last chance *) + if Mltop.is_ocaml_top() then raise Errors.Drop; (str"Error: There is no ML toplevel." ++ fnl ()) - | Vernacexpr.Quit -> - raise Vernacexpr.Quit + | Errors.Quit -> + raise Errors.Quit | _ -> (if is_pervasive_exn exc then (mt ()) else locstrm) ++ Errors.print exc @@ -372,9 +371,9 @@ let rec loop () = reset_input_buffer stdin top_buffer; while true do do_vernac() done with - | Vernacexpr.Drop -> () + | Errors.Drop -> () | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0 - | Vernacexpr.Quit -> exit 0 + | Errors.Quit -> exit 0 | e -> msgerrnl (str"Anomaly. Please report."); loop () diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index d242036f7..43d15eb43 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -1,7 +1,7 @@ Himsg Cerrors Class -Vernacexpr +Locality Metasyntax Auto_ind_decl Libtypes diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 5cb404df7..32387e793 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -27,6 +27,21 @@ exception DuringCommandInterp of Pp.loc * exn exception HasNotFailed +(* The navigation vernac commands will be handled separately *) + +let rec is_navigation_vernac = function + | VernacResetInitial + | VernacResetName _ + | VernacBacktrack _ + | VernacBackTo _ + | VernacBack _ -> true + | c -> is_deep_navigation_vernac c + +and is_deep_navigation_vernac = function + | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c + | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l + | _ -> false + (* 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 *) diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 9998fb19c..79ea1a4c5 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -44,3 +44,6 @@ val load_vernac : bool -> string -> unit (** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *) val compile : bool -> string -> unit + + +val is_navigation_vernac : Vernacexpr.vernac_expr -> bool diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4c12b4e7b..b6e625136 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1626,7 +1626,7 @@ let interp c = Flags.program_cmd := false; Obligations.set_program_mode isprogcmd; try - interp c; check_locality (); + interp c; Locality.check_locality (); Flags.program_mode := mode with e -> Flags.program_mode := mode; diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml deleted file mode 100644 index 95384c1c9..000000000 --- a/toplevel/vernacexpr.ml +++ /dev/null @@ -1,497 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(*