diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 534 |
1 files changed, 375 insertions, 159 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index fceb0bf3..f7ba3053 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -29,7 +29,6 @@ open Decl_kinds open Constrexpr open Redexpr open Lemmas -open Misctypes open Locality open Vernacinterp @@ -184,29 +183,27 @@ let print_modules () = pr_vertical_list DirPath.print only_loaded -let print_module r = - let qid = qualid_of_reference r in +let print_module qid = try - let globdir = Nametab.locate_dir qid.v in + let globdir = Nametab.locate_dir qid in match globdir with DirModule { obj_dir; obj_mp; _ } -> Printmod.print_module (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with - Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid.v) + Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) -let print_modtype r = - let qid = qualid_of_reference r in +let print_modtype qid = try - let kn = Nametab.locate_modtype qid.v in + let kn = Nametab.locate_modtype qid in Printmod.print_modtype kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try - let mp = Nametab.locate_module qid.v in + let mp = Nametab.locate_module qid in Printmod.print_module false mp with Not_found -> - user_err (str"Unknown Module Type or Module " ++ pr_qualid qid.v) + user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) let print_namespace ns = let ns = List.rev (Names.DirPath.repr ns) in @@ -266,15 +263,13 @@ let print_namespace ns = let matches mp = match match_modulepath ns mp with | Some [] -> true | _ -> false in - let constants = (Environ.pre_env (Global.env ())).Pre_env.env_globals.Pre_env.env_constants in let constants_in_namespace = - Cmap_env.fold (fun c (body,_) acc -> - let kn = Constant.user c in - if matches (KerName.modpath kn) then - acc++fnl()++hov 2 (print_constant kn body) - else - acc - ) constants (str"") + Environ.fold_constants (fun c body acc -> + let kn = Constant.user c in + if matches (KerName.modpath kn) + then acc++fnl()++hov 2 (print_constant kn body) + else acc) + (Global.env ()) (str"") in (print_list Id.print ns)++str":"++fnl()++constants_in_namespace @@ -368,33 +363,32 @@ let msg_found_library = function | Library.LibInPath, fulldir, file -> hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file) -let err_unmapped_library ?loc ?from qid = +let err_unmapped_library ?from qid = let dir = fst (repr_qualid qid) in let prefix = match from with | None -> str "." | Some from -> str " and prefix " ++ DirPath.print from ++ str "." in - user_err ?loc + user_err ?loc:qid.CAst.loc ~hdr:"locate_library" (strbrk "Cannot find a physical path bound to logical path matching suffix " ++ DirPath.print dir ++ prefix) -let err_notfound_library ?loc ?from qid = +let err_notfound_library ?from qid = let prefix = match from with | None -> str "." | Some from -> str " with prefix " ++ DirPath.print from ++ str "." in - user_err ?loc ~hdr:"locate_library" + user_err ?loc:qid.CAst.loc ~hdr:"locate_library" (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) -let print_located_library r = - let {loc;v=qid} = qualid_of_reference r in +let print_located_library qid = try msg_found_library (Library.locate_qualified_library ~warn:false qid) with - | Library.LibUnmappedDir -> err_unmapped_library ?loc qid - | Library.LibNotFound -> err_notfound_library ?loc qid + | Library.LibUnmappedDir -> err_unmapped_library qid + | Library.LibNotFound -> err_notfound_library qid let smart_global r = let gr = Smartlocate.smart_global r in @@ -437,6 +431,10 @@ let vernac_notation ~atts = let local = enforce_module_locality atts.locality in Metasyntax.add_notation local (Global.env()) +let vernac_custom_entry ~atts s = + let local = enforce_module_locality atts.locality in + Metasyntax.declare_custom_entry local s + (***********) (* Gallina *) @@ -449,7 +447,7 @@ let start_proof_and_print k l hook = let evi = Evarutil.nf_evar_info sigma evi in let env = Evd.evar_filtered_env evi in try - let concl = EConstr.of_constr evi.Evd.evar_concl in + let concl = evi.Evd.evar_concl in if not (Evarutil.is_ground_env sigma env && Evarutil.is_ground_term sigma concl) then raise Exit; @@ -518,7 +516,7 @@ 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. *) let status = Pfedit.by (Tactics.exact_proof c) in - save_proof (Vernacexpr.(Proved(Opaque,None))); + save_proof (Vernacexpr.(Proved(Proof_global.Opaque,None))); if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption ~atts discharge kind l nl = @@ -534,38 +532,52 @@ let vernac_assumption ~atts discharge kind l nl = if not status then Feedback.feedback Feedback.AddedAxiom let should_treat_as_cumulative cum poly = - if poly then - match cum with - | GlobalCumulativity | LocalCumulativity -> true - | GlobalNonCumulativity | LocalNonCumulativity -> false - else - match cum with - | GlobalCumulativity | GlobalNonCumulativity -> false - | LocalCumulativity -> - user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") - | LocalNonCumulativity -> - user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") - -let vernac_record cum k poly finite struc binders sort nameopt cfs = + match cum with + | Some VernacCumulative -> + if poly then true + else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") + | Some VernacNonCumulative -> + if poly then false + else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") + | None -> poly && Flags.is_polymorphic_inductive_cumulativity () + +let uniform_inductive_parameters = ref false + +let should_treat_as_uniform () = + if !uniform_inductive_parameters + then ComInductive.UniformParameters + else ComInductive.NonUniformParameters + +let vernac_record cum k poly finite records = let is_cumulative = should_treat_as_cumulative cum poly in - let const = match nameopt with - | None -> add_prefix "Build_" (fst (snd struc)).v - | Some ({v=id} as lid) -> - Dumpglob.dump_definition lid false "constr"; id in - if Dumpglob.dump () then ( - Dumpglob.dump_definition (fst (snd struc)) false "rec"; - List.iter (fun (((_, x), _), _) -> - match x with - | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> Dumpglob.dump_definition (make ?loc id) false "proj" - | _ -> ()) cfs); - ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort)) + let map ((coe, (id, pl)), binders, sort, nameopt, cfs) = + let const = match nameopt with + | None -> add_prefix "Build_" id.v + | Some lid -> + let () = Dumpglob.dump_definition lid false "constr" in + lid.v + in + let () = + if Dumpglob.dump () then + let () = Dumpglob.dump_definition id false "rec" in + let iter (((_, x), _), _) = match x with + | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> + Dumpglob.dump_definition (make ?loc id) false "proj" + | _ -> () + in + List.iter iter cfs + in + coe, id, pl, binders, cfs, const, sort + in + let records = List.map map records in + ignore(Record.definition_structure k is_cumulative poly finite records) (** When [poly] is true the type is declared polymorphic. When [lo] is true, then the type is declared private (as per the [Private] keyword). [finite] indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive ~atts cum lo finite indl = - let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in + let open Pp in if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -575,34 +587,86 @@ let vernac_inductive ~atts cum lo finite indl = Dumpglob.dump_definition lid false "constr") cstrs | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; + let is_record = function + | ((_ , _ , _ , _, RecordDecl _), _) -> true + | _ -> false + in + let is_constructor = function + | ((_ , _ , _ , _, Constructors _), _) -> true + | _ -> false + in + let is_defclass = match indl with + | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l) + | _ -> None + in + if Option.has_some is_defclass then + (** Definitional class case *) + let (id, bl, c, l) = Option.get is_defclass in + let (coe, (lid, ce)) = l in + let coe' = if coe then Some true else None in + let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in + vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] + else if List.for_all is_record indl then + (** Mutual record case *) + let check_kind ((_, _, _, kind, _), _) = match kind with + | Variant -> + user_err (str "The Variant keyword does not support syntax { ... }.") + | Record | Structure | Class _ | Inductive_kw | CoInductive -> () + in + let () = List.iter check_kind indl in + let check_where ((_, _, _, _, _), wh) = match wh with + | [] -> () + | _ :: _ -> + user_err (str "where clause not supported for records") + in + let () = List.iter check_where indl in + let unpack ((id, bl, c, _, decl), _) = match decl with + | RecordDecl (oc, fs) -> + (id, bl, c, oc, fs) + | Constructors _ -> assert false (** ruled out above *) + in + let ((_, _, _, kind, _), _) = List.hd indl in + let kind = match kind with Class _ -> Class false | _ -> kind in + let recordl = List.map unpack indl in + vernac_record cum kind atts.polymorphic finite recordl + else if List.for_all is_constructor indl then + (** Mutual inductive case *) + let check_kind ((_, _, _, kind, _), _) = match kind with + | (Record | Structure) -> + user_err (str "The Record keyword is for types defined using the syntax { ... }.") + | Class _ -> + user_err (str "Inductive classes not supported") + | Variant | Inductive_kw | CoInductive -> () + in + let () = List.iter check_kind indl in + let check_name ((na, _, _, _, _), _) = match na with + | (true, _) -> + user_err (str "Variant types do not handle the \"> Name\" \ + syntax, which is reserved for records. Use the \":>\" \ + syntax on constructors instead.") + | _ -> () + in + let () = List.iter check_name indl in + let unpack (((_, id) , bl, c, _, decl), ntn) = match decl with + | Constructors l -> (id, bl, c, l), ntn + | RecordDecl _ -> assert false (* ruled out above *) + in + let indl = List.map unpack indl in + let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in + let uniform = should_treat_as_uniform () in + ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo ~uniform finite + else + user_err (str "Mixed record-inductive definitions are not allowed") +(* + match indl with - | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] -> - user_err Pp.(str "The Record keyword is for types defined using the syntax { ... }.") - | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> - user_err Pp.(str "The Variant keyword does not support syntax { ... }.") - | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> - vernac_record cum (match b with Class _ -> Class false | _ -> b) - atts.polymorphic finite id bl c oc fs | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> let f = let (coe, ({loc;v=id}, ce)) = l in let coe' = if coe then Some true else None in (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), []) - in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f] - | [ ( _ , _, _, Class _, Constructors _), [] ] -> - user_err Pp.(str "Inductive classes not supported") - | [ ( id , bl , c , Class _, _), _ :: _ ] -> - user_err Pp.(str "where clause not supported for classes") - | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> - user_err Pp.(str "where clause not supported for (co)inductive records") - | _ -> let unpack = function - | ( (false, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn - | ( (true,_),_,_,_,Constructors _),_ -> - user_err Pp.(str "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead.") - | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") - in - let indl = List.map unpack indl in - ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite + in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] + *) let vernac_fixpoint ~atts discharge l = let local = enforce_locality_exp atts.locality discharge in @@ -640,7 +704,7 @@ let vernac_scheme l = let vernac_combined_scheme lid l = if Dumpglob.dump () then (Dumpglob.dump_definition lid false "def"; - List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Misctypes.AN (make ?loc @@ Ident id))) l); + List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (qualid_of_ident ?loc id))) l); Indschemes.do_combined_scheme lid l let vernac_universe ~atts l = @@ -661,7 +725,7 @@ let vernac_constraint ~atts l = (* Modules *) let vernac_import export refl = - Library.import_module export (List.map qualid_of_reference refl) + Library.import_module export refl let vernac_declare_module export {loc;v=id} binders_ast mty_ast = (* We check the state of the system (in section, in module type) @@ -675,11 +739,11 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast - id binders_ast (Enforce mty_ast) [] + id binders_ast (Declaremods.Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); - Option.iter (fun export -> vernac_import export [make @@ Ident id]) export + Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) @@ -704,7 +768,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [make @@ Ident id]) export + (fun export -> vernac_import export [qualid_of_ident id]) export ) argsexport | _::_ -> let binders_ast = List.map @@ -719,14 +783,14 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); - Option.iter (fun export -> vernac_import export [make @@ Ident id]) + Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export let vernac_end_module export {loc;v=id} = let mp = Declaremods.end_module () in Dumpglob.dump_modref ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); - Option.iter (fun export -> vernac_import export [make ?loc @@ Ident id]) export + Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then @@ -751,7 +815,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [make ?loc @@ Ident id]) export + (fun export -> vernac_import export [qualid_of_ident ?loc id]) export ) argsexport | _ :: _ -> @@ -813,22 +877,20 @@ let warn_require_in_section = let vernac_require from import qidl = if Lib.sections_are_opened () then warn_require_in_section (); - let qidl = List.map qualid_of_reference qidl in let root = match from with | None -> None | Some from -> - let qid = Libnames.qualid_of_reference from in - let (hd, tl) = Libnames.repr_qualid qid.v in + let (hd, tl) = Libnames.repr_qualid from in Some (Libnames.add_dirpath_suffix hd tl) in - let locate {loc;v=qid} = + let locate qid = try let warn = not !Flags.quiet in let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in (dir, f) with - | Library.LibUnmappedDir -> err_unmapped_library ?loc ?from:root qid - | Library.LibNotFound -> err_notfound_library ?loc ?from:root qid + | Library.LibUnmappedDir -> err_unmapped_library ?from:root qid + | Library.LibNotFound -> err_notfound_library ?from:root qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then @@ -858,7 +920,7 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance ~atts abst sup inst props pri = let global = not (make_section_locality atts.locality) in - Dumpglob.dump_constraint inst false "inst"; + Dumpglob.dump_constraint (fst (pi1 inst)) false "inst"; let program_mode = Flags.is_program_mode () in ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri) @@ -912,7 +974,7 @@ let vernac_set_used_variables e = if List.is_empty to_clear then (p, ()) else let tac = Tactics.clear to_clear in - fst (Pfedit.solve SelectAll None tac p), () + fst (Pfedit.solve Goal_select.SelectAll None tac p), () end (*****************************) @@ -980,7 +1042,7 @@ let vernac_remove_hints ~atts dbs ids = let vernac_hints ~atts lb h = let local = enforce_module_locality atts.locality in - Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h) + Hints.add_hints ~local lb (Hints.interp_hints atts.polymorphic h) let vernac_syntactic_definition ~atts lid x y = Dumpglob.dump_definition lid false "syndef"; @@ -1134,15 +1196,16 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags = let names = rename prev_names names in let renaming_specified = Option.has_some !example_renaming in - if !rename_flag_required && not rename_flag then - user_err ~hdr:"vernac_declare_arguments" - (strbrk "To rename arguments the \"rename\" flag must be specified." - ++ spc () ++ - match !example_renaming with - | None -> mt () - | Some (o,n) -> - str "Argument " ++ Name.print o ++ - str " renamed to " ++ Name.print n ++ str "."); + if !rename_flag_required && not rename_flag then begin + let msg = + match !example_renaming with + | None -> + strbrk "To rename arguments the \"rename\" flag must be specified." + | Some (o,n) -> + strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++ + strbrk " into " ++ Name.print n ++ str "." + in user_err ~hdr:"vernac_declare_arguments" msg + end; let duplicate_names = List.duplicates Name.equal (List.filter ((!=) Anonymous) names) @@ -1271,7 +1334,7 @@ let vernac_reserve bl = let vernac_generalizable ~atts = let local = make_non_locality atts.locality in - Implicit_quantifiers.declare_generalizable local + Implicit_quantifiers.declare_generalizable ~local let _ = declare_bool_option @@ -1420,6 +1483,14 @@ let _ = optwrite = Flags.make_polymorphic_inductive_cumulativity } let _ = + declare_bool_option + { optdepr = false; + optname = "Uniform inductive parameters"; + optkey = ["Uniform"; "Inductive"; "Parameters"]; + optread = (fun () -> !uniform_inductive_parameters); + optwrite = (fun b -> uniform_inductive_parameters := b) } + +let _ = declare_int_option { optdepr = false; optname = "the level of inlining during functor application"; @@ -1434,8 +1505,8 @@ let _ = { optdepr = false; optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; - optread = (fun () -> !CClosure.share); - optwrite = (fun b -> CClosure.share := b) } + optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); + optwrite = (fun b -> Global.set_reduction_sharing b) } let _ = declare_bool_option @@ -1468,22 +1539,22 @@ let _ = optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); optwrite = (fun b -> Constrextern.print_universes:=b) } - + let _ = declare_bool_option { optdepr = false; optname = "dumping bytecode after compilation"; optkey = ["Dump";"Bytecode"]; - optread = Flags.get_dump_bytecode; - optwrite = Flags.set_dump_bytecode } + optread = (fun () -> !Cbytegen.dump_bytecode); + optwrite = (:=) Cbytegen.dump_bytecode } let _ = declare_bool_option { optdepr = false; optname = "dumping VM lambda code after compilation"; optkey = ["Dump";"Lambda"]; - optread = Flags.get_dump_lambda; - optwrite = Flags.set_dump_lambda } + optread = (fun () -> !Clambda.dump_lambda); + optwrite = (:=) Clambda.dump_lambda } let _ = declare_bool_option @@ -1614,7 +1685,7 @@ let get_current_context_of_args = function let query_command_selector ?loc = function | None -> None - | Some (SelectNth n) -> Some n + | Some (Goal_select.SelectNth n) -> Some n | _ -> user_err ?loc ~hdr:"query_command_selector" (str "Query commands only support the single numbered goal selector.") @@ -1622,17 +1693,16 @@ let vernac_check_may_eval ~atts redexp glopt rc = let glopt = query_command_selector ?loc:atts.loc glopt in let (sigma, env) = get_current_context_of_args glopt in let sigma, c = interp_open_constr env sigma rc in - let c = EConstr.Unsafe.to_constr c in let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in Evarconv.check_problems_are_solved env sigma; - let sigma,nf = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in let uctx = Evd.universe_context_set sigma in let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma env) in - let c = nf c in let j = - if Evarutil.has_undefined_evars sigma (EConstr.of_constr c) then - Evarutil.j_nf_evar sigma (Retyping.get_judgment_of env sigma (EConstr.of_constr c)) + if Evarutil.has_undefined_evars sigma c then + Evarutil.j_nf_evar sigma (Retyping.get_judgment_of env sigma c) else + let c = EConstr.to_constr sigma c in (* OK to call kernel which does not support evars *) Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c) in @@ -1656,7 +1726,9 @@ let vernac_check_may_eval ~atts redexp glopt rc = let vernac_declare_reduction ~atts s r = let local = make_locality atts.locality in - declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r)) + let env = Global.env () in + let sigma = Evd.from_env env in + declare_red_expr local s (snd (Hook.get f_interp_redexp env sigma r)) (* The same but avoiding the current goal context if any *) let vernac_global_check c = @@ -1690,10 +1762,10 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = let glnumopt = query_command_selector ?loc glopt in let gl,id = match glnumopt, ref_or_by_not.v with - | None,AN {v=Ident id} -> (* goal number not given, catch any failure *) - (try get_nth_goal 1,id with _ -> raise NoHyp) - | Some n,AN {v=Ident id} -> (* goal number given, catch if wong *) - (try get_nth_goal n,id + | None,AN qid when qualid_is_ident qid -> (* goal number not given, catch any failure *) + (try get_nth_goal 1, qualid_basename qid with _ -> raise NoHyp) + | Some n,AN qid when qualid_is_ident qid -> (* goal number given, catch if wong *) + (try get_nth_goal n, qualid_basename qid with Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs" (str "No such goal: " ++ int n ++ str ".")) @@ -1746,7 +1818,7 @@ let vernac_print ~atts env sigma = else str"There may remain asynchronous universe constraints" in begin match dst with - | None -> UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining + | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining | Some s -> dump_universes_gen univ s end | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r) @@ -1774,11 +1846,10 @@ let vernac_print ~atts env sigma = Printer.pr_assumptionset env sigma nassums | PrintStrategy r -> print_strategy r -let global_module r = - let {loc;v=qid} = qualid_of_reference r in +let global_module qid = try Nametab.full_name_module qid with Not_found -> - user_err ?loc ~hdr:"global_module" + user_err ?loc:qid.CAst.loc ~hdr:"global_module" (str "Module/section " ++ pr_qualid qid ++ str " not found.") let interp_search_restriction = function @@ -1916,9 +1987,10 @@ let vernac_subproof gln = Proof_global.simple_with_current_proof (fun _ p -> match gln with | None -> Proof.focus subproof_cond () 1 p - | Some (SelectNth n) -> Proof.focus subproof_cond () n p + | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p + | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p | _ -> user_err ~hdr:"bracket_selector" - (str "Brackets only support the single numbered goal selector.")) + (str "Brackets do not support multi-goal selectors.")) let vernac_end_subproof () = Proof_global.simple_with_current_proof (fun _ p -> @@ -1974,7 +2046,7 @@ let vernac_load interp fname = interp x in let parse_sentence = Flags.with_option Flags.we_are_parsing (fun po -> - match Pcoq.Gram.entry_parse Pcoq.main_entry po with + match Pcoq.Entry.parse Pvernac.main_entry po with | Some x -> x | None -> raise End_of_input) in let fname = @@ -1983,7 +2055,7 @@ let vernac_load interp fname = let input = let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in - Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in + Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in begin try while true do interp (snd (parse_sentence input)) done with End_of_input -> () @@ -2009,10 +2081,6 @@ let interp ?proof ~atts ~st c = | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command") | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") - | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command") - - (* Toplevel control *) - | VernacToplevelControl e -> raise e (* Resetting *) | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") @@ -2029,12 +2097,13 @@ let interp ?proof ~atts ~st c = | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s) - | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc | VernacNotation (c,infpl,sc) -> vernac_notation ~atts c infpl sc | VernacNotationAddFormat(n,k,v) -> Metasyntax.add_notation_extra_printing_rule n k v + | VernacDeclareCustomEntry s -> + vernac_custom_entry ~atts s (* Gallina *) | VernacDefinition ((discharge,kind),lid,d) -> @@ -2044,7 +2113,7 @@ let interp ?proof ~atts ~st c = | VernacExactProof c -> vernac_exact_proof c | VernacAssumption ((discharge,kind),nl,l) -> vernac_assumption ~atts discharge kind l nl - | VernacInductive (cum, priv,finite,l) -> vernac_inductive ~atts cum priv finite l + | VernacInductive (cum, priv, finite, l) -> vernac_inductive ~atts cum priv finite l | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l | VernacScheme l -> vernac_scheme l @@ -2103,8 +2172,6 @@ let interp ?proof ~atts ~st c = vernac_hints ~atts dbnames hints | VernacSyntacticDefinition (id,c,b) -> vernac_syntactic_definition ~atts id c b - | VernacDeclareImplicits (qid,l) -> - vernac_declare_implicits ~atts qid l | VernacArguments (qid, args, more_implicits, nargs, flags) -> vernac_arguments ~atts qid args more_implicits nargs flags | VernacReserve bl -> vernac_reserve bl @@ -2165,6 +2232,7 @@ let check_vernac_supports_locality c l = | Some _, ( VernacOpenCloseScope _ | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _ + | VernacDeclareCustomEntry _ | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ | VernacAssumption _ | VernacStartTheoremProof _ | VernacCoercion _ | VernacIdentityCoercion _ @@ -2172,7 +2240,7 @@ let check_vernac_supports_locality c l = | VernacDeclareMLModule _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ | VernacSyntacticDefinition _ - | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _ + | VernacArguments _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ | VernacSetOption _ | VernacUnsetOption _ @@ -2255,37 +2323,67 @@ let with_fail st b f = | HasNotFailed -> user_err ~hdr:"Fail" (str "The command has not failed!") | HasFailed msg -> - if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info + if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end +let attributes_of_flags f atts = + let assert_empty k v = + if v <> VernacFlagEmpty + then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments") + in + List.fold_left + (fun (polymorphism, atts) (k, v) -> + match k with + | "program" when not atts.program -> + assert_empty k v; + (polymorphism, { atts with program = true }) + | "program" -> + user_err Pp.(str "Program mode specified twice") + | "polymorphic" when polymorphism = None -> + assert_empty k v; + (Some true, atts) + | "monomorphic" when polymorphism = None -> + assert_empty k v; + (Some false, atts) + | ("polymorphic" | "monomorphic") -> + user_err Pp.(str "Polymorphism specified twice") + | "local" when Option.is_empty atts.locality -> + assert_empty k v; + (polymorphism, { atts with locality = Some true }) + | "global" when Option.is_empty atts.locality -> + assert_empty k v; + (polymorphism, { atts with locality = Some false }) + | ("local" | "global") -> + user_err Pp.(str "Locality specified twice") + | "deprecated" when Option.is_empty atts.deprecated -> + begin match v with + | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ] + | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] -> + let since = Some since and note = Some note in + (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ~note ()) }) + | VernacFlagList [ "since", VernacFlagLeaf since ] -> + let since = Some since in + (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ()) }) + | VernacFlagList [ "note", VernacFlagLeaf note ] -> + let note = Some note in + (polymorphism, { atts with deprecated = Some (mk_deprecation ~note ()) }) + | _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute") + end + | "deprecated" -> + user_err Pp.(str "Deprecation specified twice") + | _ -> user_err Pp.(str "Unknown attribute " ++ str k) + ) + (None, atts) + f + let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = let orig_univ_poly = Flags.is_universe_polymorphism () in let orig_program_mode = Flags.is_program_mode () in - let flags f atts = - List.fold_left - (fun (polymorphism, atts) f -> - match f with - | VernacProgram when not atts.program -> - (polymorphism, { atts with program = true }) - | VernacProgram -> - user_err Pp.(str "Program mode specified twice") - | VernacPolymorphic b when polymorphism = None -> - (Some b, atts) - | VernacPolymorphic _ -> - user_err Pp.(str "Polymorphism specified twice") - | VernacLocal b when Option.is_empty atts.locality -> - (polymorphism, { atts with locality = Some b }) - | VernacLocal _ -> - user_err Pp.(str "Locality specified twice") - ) - (None, atts) - f - in let rec control = function | VernacExpr (f, v) -> - let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in + let (polymorphism, atts) = attributes_of_flags f (mk_atts ~program:orig_program_mode ()) in aux ~polymorphism ~atts v | VernacFail v -> with_fail st true (fun () -> control v) | VernacTimeout (n,v) -> @@ -2347,3 +2445,121 @@ let interp ?verbosely ?proof ~st cmd = let exn = CErrors.push exn in Vernacstate.invalidate_cache (); iraise exn + +(** VERNAC EXTEND registering *) + +open Genarg +open Extend + +type classifier = Genarg.raw_generic_argument list -> vernac_classification + +type (_, _) ty_sig = +| TyNil : (atts:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig +| TyNonTerminal : + string option * ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig + +type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml + +let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND") + +let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args +| TyNonTerminal (_, tu, ty) -> fun f args -> + begin match args with + | [] -> type_error () + | Genarg.GenArg (Rawwit tag, v) :: args -> + match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_classifier ty (f v) args + end + +(** Stupid GADTs forces us to duplicate the definition just for typing *) +let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_command ty f args +| TyNonTerminal (_, tu, ty) -> fun f args -> + begin match args with + | [] -> type_error () + | Genarg.GenArg (Rawwit tag, v) :: args -> + match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_command ty (f v) args + end + +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = function +| TUlist1 l -> Alist1 (untype_user_symbol l) +| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUlist0 l -> Alist0 (untype_user_symbol l) +| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUopt o -> Aopt (untype_user_symbol o) +| TUentry a -> Aentry (Pcoq.genarg_grammar (ExtraArg a)) +| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (ExtraArg a), string_of_int i) + +let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function +| TyNil -> [] +| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty +| TyNonTerminal (id, tu, ty) -> + let t = Option.map (fun _ -> rawwit (Egramml.proj_symbol tu)) id in + let symb = untype_user_symbol tu in + Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty + +let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol + +let classifiers : classifier array String.Map.t ref = ref String.Map.empty + +let get_vernac_classifier (name, i) args = + (String.Map.find name !classifiers).(i) args + +let declare_vernac_classifier name f = + classifiers := String.Map.add name f !classifiers + +let vernac_extend ~command ?classifier ?entry ext = + let get_classifier (TyML (_, ty, _, cl)) = match cl with + | Some cl -> untype_classifier ty cl + | None -> + match classifier with + | Some cl -> fun _ -> cl command + | None -> + let e = match entry with + | None -> "COMMAND" + | Some e -> Pcoq.Gram.Entry.name e + in + let msg = Printf.sprintf "\ + Vernac entry \"%s\" misses a classifier. \ + A classifier is a function that returns an expression \ + of type vernac_classification (see Vernacexpr). You can: \n\ + - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \ + new vernacular command does not alter the system state;\n\ + - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \ + new vernacular command alters the system state but not the \ + parser nor it starts a proof or ends one;\n\ + - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \ + a global function f. The function f will be called passing\ + \"%s\" as the only argument;\n\ + - Add a specific classifier in each clause using the syntax:\n\ + '[...] => [ f ] -> [...]'.\n\ + Specific classifiers have precedence over global \ + classifiers. Only one classifier is called." + command e e e command + in + CErrors.user_err (Pp.strbrk msg) + in + let cl = Array.map_of_list get_classifier ext in + let iter i (TyML (depr, ty, f, _)) = + let f = untype_command ty f in + let r = untype_grammar ty in + let () = vinterp_add depr (command, i) f in + Egramml.extend_vernac_command_grammar (command, i) entry r + in + let () = declare_vernac_classifier command cl in + List.iteri iter ext |