From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- toplevel/auto_ind_decl.mli | 1 - toplevel/cerrors.ml | 46 +++++----- toplevel/cerrors.mli | 2 +- toplevel/classes.ml | 15 ++- toplevel/classes.mli | 3 +- toplevel/command.ml | 19 ++-- toplevel/command.mli | 3 +- toplevel/coqinit.ml | 33 +++---- toplevel/coqinit.mli | 4 +- toplevel/coqtop.ml | 18 ++-- toplevel/himsg.ml | 4 +- toplevel/indschemes.ml | 2 +- toplevel/metasyntax.ml | 33 ++++++- toplevel/mltop.ml | 19 +--- toplevel/mltop.mli | 1 - toplevel/obligations.ml | 24 +++-- toplevel/obligations.mli | 7 +- toplevel/record.ml | 7 +- toplevel/toplevel.mllib | 1 - toplevel/usage.ml | 10 +- toplevel/vernacentries.ml | 98 ++++++++++++-------- toplevel/vernacinterp.ml | 22 ++++- toplevel/vernacinterp.mli | 8 +- toplevel/whelp.ml4 | 224 --------------------------------------------- toplevel/whelp.mli | 20 ---- 25 files changed, 218 insertions(+), 406 deletions(-) delete mode 100644 toplevel/whelp.ml4 delete mode 100644 toplevel/whelp.mli (limited to 'toplevel') diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index 5dbd5379..80787298 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Names open Ind_tables diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 22ea09c5..b29ba1ef 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Pp open Errors open Indtypes @@ -53,12 +52,15 @@ let _ = Errors.register_handler explain_exn_default (** Pre-explain a vernac interpretation error *) -let wrap_vernac_error (exn, info) strm = - let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in - let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in - (e, info) +let wrap_vernac_error with_header (exn, info) strm = + if with_header then + let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in + let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in + (e, info) + else + (EvaluatedError (strm, None), info) -let process_vernac_interp_error exn = match fst exn with +let process_vernac_interp_error with_header exn = match fst exn with | Univ.UniverseInconsistency i -> let msg = if !Constrextern.print_universes then @@ -66,40 +68,40 @@ let process_vernac_interp_error exn = match fst exn with Univ.explain_universe_inconsistency Universes.pr_with_global_universes i else mt() in - wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".") + wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> - wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te) + wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te) | PretypeError(ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) + wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te) | Typeclasses_errors.TypeClassError(env, te) -> - wrap_vernac_error exn (Himsg.explain_typeclass_error env te) + wrap_vernac_error with_header exn (Himsg.explain_typeclass_error env te) | InductiveError e -> - wrap_vernac_error exn (Himsg.explain_inductive_error e) + wrap_vernac_error with_header exn (Himsg.explain_inductive_error e) | Modops.ModuleTypingError e -> - wrap_vernac_error exn (Himsg.explain_module_error e) + wrap_vernac_error with_header exn (Himsg.explain_module_error e) | Modintern.ModuleInternalizationError e -> - wrap_vernac_error exn (Himsg.explain_module_internalization_error e) + wrap_vernac_error with_header exn (Himsg.explain_module_internalization_error e) | RecursionSchemeError e -> - wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e) + wrap_vernac_error with_header exn (Himsg.explain_recursion_scheme_error e) | Cases.PatternMatchingError (env,sigma,e) -> - wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) + wrap_vernac_error with_header exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> - wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) + wrap_vernac_error with_header exn (Himsg.explain_reduction_tactic_error e) | Logic.RefinerError e -> - wrap_vernac_error exn (Himsg.explain_refiner_error e) + wrap_vernac_error with_header exn (Himsg.explain_refiner_error e) | Nametab.GlobalizationError q -> - wrap_vernac_error exn + wrap_vernac_error with_header exn (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ spc () ++ str "was not found" ++ spc () ++ str "in the current" ++ spc () ++ str "environment.") | Refiner.FailError (i,s) -> let s = Lazy.force s in - wrap_vernac_error exn + wrap_vernac_error with_header exn (str "Tactic failure" ++ (if Pp.is_empty s then s else str ": " ++ s) ++ if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").") | AlreadyDeclared msg -> - wrap_vernac_error exn (msg ++ str ".") + wrap_vernac_error with_header exn (msg ++ str ".") | _ -> exn @@ -108,9 +110,9 @@ let rec strip_wrapping_exceptions = function strip_wrapping_exceptions e | exc -> exc -let process_vernac_interp_error (exc, info) = +let process_vernac_interp_error ?(with_header=true) (exc, info) = let exc = strip_wrapping_exceptions exc in - let e = process_vernac_interp_error (exc, info) in + let e = process_vernac_interp_error with_header (exc, info) in let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in let loc = Option.default Loc.ghost (Loc.get_loc info) in match ltac_trace with diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 1768af11..100b3772 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds (** Pre-explain a vernac interpretation error *) -val process_vernac_interp_error : Util.iexn -> Util.iexn +val process_vernac_interp_error : ?with_header:bool -> Util.iexn -> Util.iexn (** General explain function. Should not be used directly now, see instead function [Errors.print] and variants *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index f44ac367..33891ad9 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -103,8 +103,13 @@ let instance_hook k pri global imps ?hook cst = let declare_instance_constant k pri global imps ?hook id poly uctx term termtype = let kind = IsDefinition Instance in + let uctx = + let levels = Univ.LSet.union (Universes.universes_of_constr termtype) + (Universes.universes_of_constr term) in + Universes.restrict_universe_context uctx levels + in let entry = - Declare.definition_entry ~types:termtype ~poly ~univs:uctx term + Declare.definition_entry ~types:termtype ~poly ~univs:(Univ.ContextSet.to_context uctx) term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in @@ -165,7 +170,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro in let env' = push_rel_context ctx env in evars := Evarutil.nf_evar_map !evars; - evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env !evars; + evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars; let subst = List.map (Evarutil.nf_evar !evars) subst in if abstract then begin @@ -208,7 +213,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro let get_id = function | Ident id' -> id' - | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled") + | Qualid (loc,id') -> (loc, snd (repr_qualid id')) in let props, rest = List.fold_left @@ -232,7 +237,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Loc.ghost, Some Evar_kinds.GoalEvar, Misctypes.IntroAnonymous, None) :: props), rest + (CHole (Loc.ghost, None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None) :: props), rest else props, rest) ([], props) k.cl_props in @@ -277,7 +282,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro in let term = Option.map nf term in if not (Evd.has_undefined evm) && not (Option.is_empty term) then - let ctx = Evd.universe_context evm in + let ctx = Evd.universe_context_set evm in declare_instance_constant k pri global imps ?hook id poly ctx (Option.get term) termtype else if !refine_instance || Option.is_empty term then begin diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 0a351d3c..2b7e9e4f 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -8,7 +8,6 @@ open Names open Context -open Evd open Environ open Constrexpr open Typeclasses @@ -33,7 +32,7 @@ val declare_instance_constant : ?hook:(Globnames.global_reference -> unit) -> Id.t -> (** name *) bool -> (* polymorphic *) - Univ.universe_context -> (* Universes *) + Univ.universe_context_set -> (* Universes *) Constr.t -> (** body *) Term.types -> (** type *) Names.Id.t diff --git a/toplevel/command.ml b/toplevel/command.ml index 9cb3bb86..754ad852 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -233,9 +233,9 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma in (gr,inst,Lib.is_modtype_strict ()) -let interp_assumption evdref env bl c = +let interp_assumption evdref env impls bl c = let c = prod_constr_expr c bl in - let ty, impls = interp_type_evars_impls env evdref c in + let ty, impls = interp_type_evars_impls env evdref ~impls c in let evd, nf = nf_evars_and_universes !evdref in let ctx = Evd.universe_context_set evd in ((nf ty, ctx), impls) @@ -259,12 +259,15 @@ let do_assumptions (_, poly, _ as kind) nl l = l [] else l in - let _,l = List.fold_map (fun env (is_coe,(idl,c)) -> - let (t,ctx),imps = interp_assumption evdref env [] c in + let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) -> + let (t,ctx),imps = interp_assumption evdref env ienv [] c in let env = push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in - (env,((is_coe,idl),t,(ctx,imps)))) - env l + let ienv = List.fold_right (fun (_,id) ienv -> + let impls = compute_internalization_data env Variable t imps in + Id.Map.add id impls ienv) idl ienv in + ((env,ienv),((is_coe,idl),t,(ctx,imps)))) + (env,empty_internalization_env) l in let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in let l = List.map (on_pi2 (nf_evar evd)) l in @@ -746,8 +749,8 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx -let declare_fix (_,poly,_ as kind) ctx f ((def,_),eff) t imps = - let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in +let declare_fix ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps = + let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r)) let _ = Obligations.declare_fix_ref := declare_fix diff --git a/toplevel/command.mli b/toplevel/command.mli index 894333ad..3a38e52c 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -11,7 +11,6 @@ open Term open Entries open Libnames open Globnames -open Tacexpr open Vernacexpr open Constrexpr open Decl_kinds @@ -167,5 +166,5 @@ val do_cofixpoint : val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit -val declare_fix : definition_kind -> Univ.universe_context -> Id.t -> +val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 03074ced..f1d8a492 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -57,28 +57,20 @@ let load_rcfile() = else Flags.if_verbose msg_info (str"Skipping rcfile loading.") -(* Puts dir in the path of ML and in the LoadPath *) -let coq_add_path unix_path s = - Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true; - Mltop.add_ml_dir unix_path - (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = - if !Flags.load_init then - Mltop.add_rec_path ~unix_path ~coq_root ~implicit:true - else - Mltop.add_path ~unix_path ~coq_root ~implicit:false; + Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init); if with_ml then Mltop.add_rec_ml_dir unix_path let add_userlib_path ~unix_path = - Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; + Mltop.add_rec_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false; Mltop.add_rec_ml_dir unix_path (* Options -I, -I-as, and -R of the command line *) let includes = ref [] -let push_include s alias recursive implicit = - includes := (s,alias,recursive,implicit) :: !includes +let push_include s alias implicit = + includes := (s, alias, implicit) :: !includes let ml_includes = ref [] let push_ml_include s = ml_includes := s :: !ml_includes @@ -91,10 +83,11 @@ let init_load_path () = let coq_root = Names.DirPath.make [Nameops.coq_root] in (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) - if Coq_config.local then coq_add_path (coqlib/"dev") "dev"; + if Coq_config.local then + Mltop.add_ml_dir (coqlib/"dev"); (* main loops *) if Coq_config.local || !Flags.boot then begin - let () = Mltop.add_ml_dir (coqlib/"stm") in + Mltop.add_ml_dir (coqlib/"stm"); Mltop.add_ml_dir (coqlib/"ide") end; Mltop.add_ml_dir (coqlib/"toploop"); @@ -109,13 +102,13 @@ let init_load_path () = List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs; (* then directories in COQPATH *) List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath; - (* then current directory *) - Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix ~implicit:false; - (* additional loadpath, given with options -I-as, -Q, and -R *) + (* then current directory (not recursively!) *) + Mltop.add_ml_dir "."; + Loadpath.add_load_path "." Nameops.default_root_prefix ~implicit:false; + (* additional loadpath, given with options -Q and -R *) List.iter - (fun (unix_path, coq_root, reci, implicit) -> - (if reci then Mltop.add_rec_path else Mltop.add_path) - ~unix_path ~coq_root ~implicit) + (fun (unix_path, coq_root, implicit) -> + Mltop.add_rec_path ~unix_path ~coq_root ~implicit) (List.rev !includes); (* additional ml directories, given with option -I *) List.iter Mltop.add_ml_dir (List.rev !ml_includes) diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 5f7133c3..c019cc1c 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -15,8 +15,8 @@ val set_rcfile : string -> unit val no_load_rc : unit -> unit val load_rcfile : unit -> unit -val push_include : string -> Names.DirPath.t -> bool -> bool -> unit -(** [push_include phys_path log_path recursive implicit] *) +val push_include : string -> Names.DirPath.t -> bool -> unit +(** [push_include phys_path log_path implicit] *) val push_ml_include : string -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 142f3386..e9e86953 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -135,9 +135,9 @@ let set_outputstate s = outputstate:=s let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate -let set_include d p recursive implicit = +let set_include d p implicit = let p = dirpath_of_string p in - push_include d p recursive implicit + push_include d p implicit let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = @@ -378,7 +378,7 @@ let schedule_vio_compilation () = let get_native_name s = (* We ignore even critical errors because this mode has to be super silent *) try - String.concat Filename.dir_sep [Filename.dirname s; + String.concat "/" [Filename.dirname s; Nativelib.output_dir; Library.native_name_from_filename s] with _ -> "" @@ -402,21 +402,21 @@ let parse_args arglist = (* Complex options with many args *) |"-I"|"-include" -> begin match rem with - | d :: "-as" :: p :: rem -> set_include d p false true; args := rem - | d :: "-as" :: [] -> error_missing_arg "-as" | d :: rem -> push_ml_include d; args := rem | [] -> error_missing_arg opt end |"-Q" -> begin match rem with - | d :: p :: rem -> set_include d p true false; args := rem + | d :: p :: rem -> set_include d p false; args := rem | _ -> error_missing_arg opt end |"-R" -> begin match rem with - | d :: "-as" :: [] -> error_missing_arg "-as" - | d :: "-as" :: p :: rem - | d :: p :: rem -> set_include d p true true; args := rem + | d :: "-as" :: [] -> error_missing_arg opt + | d :: "-as" :: p :: rem -> + warning "option -R * -as * deprecated, remove the -as"; + set_include d p true; args := rem + | d :: p :: rem -> set_include d p true; args := rem | _ -> error_missing_arg opt end diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 9341f2f7..5429e660 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -879,7 +879,9 @@ let explain_label_already_declared l = str ("The label "^Label.to_string l^" is already declared.") let explain_application_to_not_path _ = - str "Application of modules is restricted to paths." + strbrk "A module cannot be applied to another module application or " ++ + strbrk "with-expression; you must give a name to the intermediate result " ++ + strbrk "module first." let explain_not_a_functor () = str "Application of a non-functor." diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index e6b23828..fbc45b4a 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -85,7 +85,7 @@ let _ = { optsync = true; optdepr = false; optname = "automatic declaration of boolean equality"; - optkey = ["Equality";"Schemes"]; + optkey = ["Boolean";"Equality";"Schemes"]; optread = (fun () -> !eq_flag) ; optwrite = (fun b -> eq_flag := b) } let _ = (* compatibility *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 161cf824..639ec1e6 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -61,23 +61,42 @@ let rec make_tags = function | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l | [] -> [] +let make_fresh_key = + let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in + fun () -> + let cur = incr id; !id in + let lbl = Id.of_string ("_" ^ string_of_int cur) in + let kn = Lib.make_kn lbl in + let (mp, dir, _) = KerName.repr kn in + (** We embed the full path of the kernel name in the label so that the + identifier should be unique. This ensures that including two modules + together won't confuse the corresponding labels. *) + let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i" + (ModPath.to_string mp) (DirPath.to_string dir) cur) + in + KerName.make mp dir (Label.of_id lbl) + type tactic_grammar_obj = { + tacobj_key : KerName.t; tacobj_local : locality_flag; tacobj_tacgram : tactic_grammar; tacobj_tacpp : Pptactic.pp_tactic; tacobj_body : Tacexpr.glob_tactic_expr } -let cache_tactic_notation ((_, key), tobj) = +let cache_tactic_notation (_, tobj) = + let key = tobj.tacobj_key in Tacenv.register_alias key tobj.tacobj_body; Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp -let open_tactic_notation i ((_, key), tobj) = +let open_tactic_notation i (_, tobj) = + let key = tobj.tacobj_key in if Int.equal i 1 && not tobj.tacobj_local then Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram -let load_tactic_notation i ((_, key), tobj) = +let load_tactic_notation i (_, tobj) = + let key = tobj.tacobj_key in (** Only add the printing and interpretation rules. *) Tacenv.register_alias key tobj.tacobj_body; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp; @@ -85,7 +104,10 @@ let load_tactic_notation i ((_, key), tobj) = Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram let subst_tactic_notation (subst, tobj) = - { tobj with tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body; } + { tobj with + tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key; + tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body; + } let classify_tactic_notation tacobj = Substitute tacobj @@ -115,6 +137,7 @@ let add_tactic_notation (local,n,prods,e) = tacgram_prods = prods; } in let tacobj = { + tacobj_key = make_fresh_key (); tacobj_local = local; tacobj_tacgram = parule; tacobj_tacpp = pprule; @@ -1103,7 +1126,7 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - if Int.equal i 1 then begin + if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin (* Declare the interpretation *) Notation.declare_notation_interpretation ntn scope pat df; (* Declare the uninterpretation *) diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 9dc1dd5b..0b6fc48c 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -161,17 +161,6 @@ let add_rec_ml_dir unix_path = (* Adding files to Coq and ML loadpath *) -let add_path ~unix_path:dir ~coq_root:coq_dirpath ~implicit = - if exists_dir dir then - begin - add_ml_dir dir; - Loadpath.add_load_path dir - (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath) - coq_dirpath - end - else - msg_warning (str ("Cannot open " ^ dir)) - let convert_string d = try Names.Id.of_string d with UserError _ -> @@ -191,11 +180,9 @@ let add_rec_path ~unix_path ~coq_root ~implicit = let dirs = List.map_filter convert_dirs dirs in let () = add_ml_dir unix_path in let add (path, dir) = - Loadpath.add_load_path path Loadpath.ImplicitPath dir in - let () = if implicit then List.iter add dirs in - Loadpath.add_load_path unix_path - (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath) - coq_root + Loadpath.add_load_path path ~implicit dir in + let () = List.iter add dirs in + Loadpath.add_load_path unix_path ~implicit coq_root else msg_warning (str ("Cannot open " ^ unix_path)) diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 2a91afd8..4f3f4ddd 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -47,7 +47,6 @@ val add_ml_dir : string -> unit val add_rec_ml_dir : string -> unit (** Adds a path to the Coq and ML paths *) -val add_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit (** List of modules linked to the toplevel *) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index aa068586..523134b5 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -21,7 +21,7 @@ open Pp open Errors open Util -let declare_fix_ref = ref (fun _ _ _ _ _ _ -> assert false) +let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false) let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) let trace s = @@ -319,6 +319,7 @@ type program_info = { prg_kind : definition_kind; prg_reduce : constr -> constr; prg_hook : unit Lemmas.declaration_hook; + prg_opaque : bool; } let assumption_message = Declare.assumption_message @@ -512,8 +513,9 @@ let declare_definition prg = let body, typ = subst_body true prg in let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) (Evd.evar_universe_context_subst prg.prg_ctx) in + let opaque = prg.prg_opaque in let ce = - definition_entry ~types:(nf typ) ~poly:(pi2 prg.prg_kind) + definition_entry ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) in progmap_remove prg; @@ -564,6 +566,7 @@ let declare_mutual_definition l = let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in let (local,poly,kind) = first.prg_kind in let fixnames = first.prg_deps in + let opaque = first.prg_opaque in let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in let indexes, fixdecls = match fixkind with @@ -584,7 +587,7 @@ let declare_mutual_definition l = in (* Declare the recursive definitions *) let ctx = Evd.evar_context_universe_context first.prg_ctx in - let kns = List.map4 (!declare_fix_ref (local, poly, kind) ctx) + let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter Metasyntax.add_notation_interpretation first.prg_notations; @@ -640,7 +643,7 @@ let declare_obligation prg obl body ty uctx = else Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) } -let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook = +let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls kind reduce hook = let obls', b = match b with | None -> @@ -655,7 +658,7 @@ let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook Array.mapi (fun i (n, t, l, o, d, tac) -> { obl_name = n ; obl_body = None; - obl_location = l; obl_type = reduce t; obl_status = o; + obl_location = l; obl_type = t; obl_status = o; obl_deps = d; obl_tac = tac }) obls, b in @@ -664,7 +667,8 @@ let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; - prg_hook = hook; } + prg_hook = hook; + prg_opaque = opaque; } let get_prog name = let prg_infos = !from_prg in @@ -976,9 +980,9 @@ let show_term n = ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body) let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic - ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) obls = + ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) obls = let info = str (Id.to_string n) ++ str " has type-checked" in - let prg = init_prog_info n term t ctx [] None [] obls implicits kind reduce hook in + let prg = init_prog_info ~opaque n term t ctx [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose msg_info (info ++ str "."); @@ -994,11 +998,11 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) | _ -> res) let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) - ?(hook=Lemmas.mk_hook (fun _ _ -> ())) notations fixkind = + ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) notations fixkind = let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> - let prg = init_prog_info n (Some b) t ctx deps (Some fixkind) + let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind) notations obls imps kind reduce hook in progmap_add n prg) l; let _defined = diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 582b4935..40f124ca 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -14,10 +14,9 @@ open Pp open Globnames open Vernacexpr open Decl_kinds -open Tacexpr (** Forward declaration. *) -val declare_fix_ref : (definition_kind -> Univ.universe_context -> Id.t -> +val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref val declare_definition_ref : @@ -69,7 +68,7 @@ val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(Term.constr -> Term.constr) -> - ?hook:unit Lemmas.declaration_hook -> obligation_info -> progress + ?hook:unit Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list @@ -85,7 +84,7 @@ val add_mutual_definitions : ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(Term.constr -> Term.constr) -> - ?hook:unit Lemmas.declaration_hook -> + ?hook:unit Lemmas.declaration_hook -> ?opaque:bool -> notations -> fixpoint_kind -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index 55f53351..737b7fb5 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -472,10 +472,15 @@ let add_inductive_class ind = let k = let ctx = oneind.mind_arity_ctxt in let inst = Univ.UContext.instance mind.mind_universes in + let map = function + | (_, Some _, _) -> None + | (_, None, t) -> Some (lazy t) + in + let args = List.map_filter map ctx in let ty = Inductive.type_of_inductive_knowing_parameters (push_rel_context ctx (Global.env ())) ((mind,oneind),inst) - (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx)) + (Array.of_list args) in { cl_impl = IndRef ind; cl_context = List.map (const None) ctx, ctx; diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index d22524e5..bf0f305a 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -13,7 +13,6 @@ Record Vernacinterp Mltop Vernacentries -Whelp Vernac Usage Coqloop diff --git a/toplevel/usage.ml b/toplevel/usage.ml index d4d44569..f053839c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -23,9 +23,7 @@ let print_usage_channel co command = output_string co " -I dir look for ML files in dir\ \n -include dir (idem)\ -\n -I dir -as coqdir implicitly map physical dir to logical coqdir\ -\n -R dir -as coqdir recursively map physical dir to logical coqdir\ -\n -R dir coqdir (idem)\ +\n -R dir coqdir recursively map physical dir to logical coqdir\ \n -Q dir coqdir map physical dir to logical coqdir\ \n -top coqdir set the toplevel name to be coqdir instead of Top\ \n -notop set the toplevel name to be the empty logical path\ @@ -47,6 +45,11 @@ let print_usage_channel co command = \n -require f load Coq object file f.vo and import it (Require f.)\ \n -compile f compile Coq file f.v (implies -batch)\ \n -compile-verbose f verbosely compile Coq file f.v (implies -batch)\ +\n -quick quickly compile .v files to .vio files (skip proofs)\ +\n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ +\n into fi.vo\ +\n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ +\n proofs in each fi.vio\ \n\ \n -where print Coq's standard library location and exit\ \n -config print Coq's configuration information and exit\ @@ -66,6 +69,7 @@ let print_usage_channel co command = \n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\ \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ +\n -type-in-type disable universe consistency checking\ \n -time display the time taken by each command\ \n -no-native-compiler disable the native_compute reduction machinery\ \n -h, -help print this list of options\ diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fb12edfb..cfa9bddc 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -387,12 +387,13 @@ let err_unmapped_library loc qid = pr_dirpath dir ++ str".") let err_notfound_library loc qid = - msg_error - (hov 0 (strbrk "Unable to locate library " ++ pr_qualid qid ++ str".")) + user_err_loc + (loc,"locate_library", + strbrk "Unable to locate library " ++ pr_qualid qid ++ str".") let print_located_library r = let (loc,qid) = qualid_of_reference r in - try msg_found_library (Library.locate_qualified_library false 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 @@ -496,7 +497,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 = by (Tactics.New.exact_proof c) in - save_proof (Vernacexpr.Proved(true,None)); + save_proof (Vernacexpr.(Proved(Opaque None,None))); if not status then Pp.feedback Feedback.AddedAxiom let vernac_assumption locality poly (local, kind) l nl = @@ -598,11 +599,8 @@ let vernac_constraint l = do_constraint l (* Modules *) let vernac_import export refl = - let import ref = - Library.import_module export (qualid_of_reference ref) - in - List.iter import refl; - Lib.add_frozen_state () + Library.import_module export (List.map qualid_of_reference refl); + Lib.add_frozen_state () let vernac_declare_module export (loc, id) binders_ast mty_ast = (* We check the state of the system (in section, in module type) @@ -752,9 +750,25 @@ let vernac_end_segment (_,id as lid) = (* Libraries *) -let vernac_require import qidl = +let vernac_require from import qidl = let qidl = List.map qualid_of_reference qidl in - let modrefl = List.map Library.try_locate_qualified_library 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 in + Some (Libnames.add_dirpath_suffix hd tl) + in + let locate (loc, qid) = + try + let warn = Flags.is_verbose () in + let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in + (dir, f) + with + | Library.LibUnmappedDir -> err_unmapped_library loc qid + | Library.LibNotFound -> err_notfound_library loc qid + in + let modrefl = List.map locate qidl in if Dumpglob.dump () then List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl); Library.require_library_from_dirpath modrefl import @@ -878,11 +892,10 @@ let vernac_set_used_variables e = let expand filename = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename -let vernac_add_loadpath isrec pdir ldiropt = +let vernac_add_loadpath implicit pdir ldiropt = let pdir = expand pdir in let alias = Option.default Nameops.default_root_prefix ldiropt in - (if isrec then Mltop.add_rec_path else Mltop.add_path) - ~unix_path:pdir ~coq_root:alias ~implicit:true + Mltop.add_rec_path ~unix_path:pdir ~coq_root:alias ~implicit let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) @@ -963,20 +976,27 @@ let register_ltac local isrec tacl = (name, body) in let rfun = List.map map tacl in - let ltacrecvars = + let recvars = let fold accu (op, _) = match op with | UpdateTac _ -> accu - | NewTac id -> Id.Map.add id (Lib.make_kn id) accu + | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu in - if isrec then List.fold_left fold Id.Map.empty rfun - else Id.Map.empty + if isrec then List.fold_left fold [] rfun + else [] in - let ist = { (Tacintern.make_empty_glob_sign ()) with Genintern.ltacrecvars; } in + let ist = Tacintern.make_empty_glob_sign () in let map (name, body) = let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in (name, body) in - let defs = List.map map rfun in + let defs () = + (** Register locally the tactic to handle recursivity. This function affects + the whole environment, so that we transactify it afterwards. *) + let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in + let () = List.iter iter_rec recvars in + List.map map rfun + in + let defs = Future.transactify defs () in let iter (def, tac) = match def with | NewTac id -> Tacenv.register_ltac false local id tac; @@ -1124,6 +1144,7 @@ let vernac_declare_arguments locality r l nargs flags = vernac_declare_implicits locality r implicits; if nargs >= 0 && nargs < List.fold_left max 0 rargs then error "The \"/\" option must be placed after the last \"!\"."; + let no_flags = List.is_empty flags in let rec narrow = function | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl | [] -> [] | _ :: tl -> narrow tl in @@ -1141,7 +1162,7 @@ let vernac_declare_arguments locality r l nargs flags = some_implicits_specified || some_scopes_specified || some_simpl_flags_specified) && - List.length flags = 0 then + no_flags then msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'") @@ -1503,7 +1524,7 @@ let vernac_check_may_eval redexp glopt rc = Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in let uctx = Evd.universe_context sigma' in - let env = Environ.push_context uctx env in + let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in let c = nf c in let j = if Evarutil.has_undefined_evars sigma' c then @@ -1516,12 +1537,8 @@ let vernac_check_may_eval redexp glopt rc = let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in msg_notice (print_judgment env sigma' j ++ - (if l != Evar.Set.empty then - let l = Evar.Set.fold (fun ev -> Evar.Map.add ev (Evarutil.nf_evar_info sigma' (Evd.find sigma' ev))) l Evar.Map.empty in - (fnl () ++ str "where" ++ fnl () ++ pr_evars sigma' l) - else - mt ()) ++ - Printer.pr_universe_ctx uctx) + pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ + Printer.pr_universe_ctx uctx) | Some r -> Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in @@ -1883,7 +1900,7 @@ let interp ?proof locality poly c = | VernacNameSectionHypSet (lid, set) -> vernac_name_sec_hyp lid set - | VernacRequire (export, qidl) -> vernac_require export qidl + | VernacRequire (from, export, qidl) -> vernac_require from export qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t @@ -1951,14 +1968,16 @@ let interp ?proof locality poly c = | VernacComments l -> if_verbose msg_info (str "Comments ok\n") | VernacNop -> () + (* The STM should handle that, but LOAD bypasses the STM... *) + | VernacAbort id -> msg_warning (str "VernacAbort not handled by Stm") + | VernacAbortAll -> msg_warning (str "VernacAbortAll not handled by Stm") + | VernacRestart -> msg_warning (str "VernacRestart not handled by Stm") + | VernacUndo _ -> msg_warning (str "VernacUndo not handled by Stm") + | VernacUndoTo _ -> msg_warning (str "VernacUndoTo not handled by Stm") + | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm") + (* Proof management *) | VernacGoal t -> vernac_start_proof poly Theorem [None,([],t,None)] false - | VernacAbort id -> anomaly (str "VernacAbort not handled by Stm") - | VernacAbortAll -> anomaly (str "VernacAbortAll not handled by Stm") - | VernacRestart -> anomaly (str "VernacRestart not handled by Stm") - | VernacUndo _ -> anomaly (str "VernacUndo not handled by Stm") - | VernacUndoTo _ -> anomaly (str "VernacUndoTo not handled by Stm") - | VernacBacktrack _ -> anomaly (str "VernacBacktrack not handled by Stm") | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () | VernacUnfocused -> vernac_unfocused () @@ -2061,7 +2080,7 @@ let locate_if_not_already loc (e, info) = | Some l -> if Loc.is_ghost l then (e, Loc.add_loc info loc) else (e, info) exception HasNotFailed -exception HasFailed of string +exception HasFailed of std_ppcmds let with_fail b f = if not b then f () @@ -2076,8 +2095,8 @@ let with_fail b f = | HasNotFailed as e -> raise e | e -> let e = Errors.push e in - raise (HasFailed (Pp.string_of_ppcmds - (Errors.iprint (Cerrors.process_vernac_interp_error e))))) + raise (HasFailed (Errors.iprint + (Cerrors.process_vernac_interp_error ~with_header:false e)))) () with e when Errors.noncritical e -> let (e, _) = Errors.push e in @@ -2086,8 +2105,7 @@ let with_fail b f = errorlabstrm "Fail" (str "The command has not failed!") | HasFailed msg -> if is_verbose () || !Flags.ide_slave then msg_info - (str "The command has indeed failed with message:" ++ - fnl () ++ str "=> " ++ hov 0 (str msg)) + (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 17f971fd..d3e48f75 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -10,14 +10,17 @@ open Util open Pp open Errors +type deprecation = bool +type vernac_command = Genarg.raw_generic_argument list -> unit -> unit + (* Table of vernac entries *) let vernac_tab = (Hashtbl.create 51 : - (Vernacexpr.extend_name, (Genarg.raw_generic_argument list -> unit -> unit)) Hashtbl.t) + (Vernacexpr.extend_name, deprecation * vernac_command) Hashtbl.t) -let vinterp_add s f = +let vinterp_add depr s f = try - Hashtbl.add vernac_tab s f + Hashtbl.add vernac_tab s (depr, f) with Failure _ -> errorlabstrm "vinterp_add" (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.") @@ -28,7 +31,7 @@ let overwriting_vinterp_add s f = let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s with Not_found -> () end; - Hashtbl.add vernac_tab s f + Hashtbl.add vernac_tab s (false, f) let vinterp_map s = try @@ -44,7 +47,16 @@ let vinterp_init () = Hashtbl.clear vernac_tab let call ?locality (opn,converted_args) = let loc = ref "Looking up command" in try - let callback = vinterp_map opn in + let depr, callback = vinterp_map opn in + let () = if depr then + let rules = Egramml.get_extend_vernac_rule opn in + let pr_gram = function + | Egramml.GramTerminal s -> str s + | Egramml.GramNonTerminal _ -> str "_" + in + let pr = pr_sequence pr_gram rules in + msg_warning (str "Deprecated vernacular command: " ++ pr) + in loc:= "Checking arguments"; let hunk = callback converted_args in loc:= "Executing command"; diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 38fce5d1..02820654 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -8,9 +8,13 @@ (** Interpretation of extended vernac phrases. *) -val vinterp_add : Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit +type deprecation = bool +type vernac_command = Genarg.raw_generic_argument list -> unit -> unit + +val vinterp_add : deprecation -> Vernacexpr.extend_name -> + vernac_command -> unit val overwriting_vinterp_add : - Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit + Vernacexpr.extend_name -> vernac_command -> unit val vinterp_init : unit -> unit val call : ?locality:bool -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 deleted file mode 100644 index daedc30f..00000000 --- a/toplevel/whelp.ml4 +++ /dev/null @@ -1,224 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* !whelp_server_name); - optwrite = (fun s -> whelp_server_name := s) } - -let _ = - declare_string_option - { optsync = false; - optdepr = false; - optname = "Whelp getter"; - optkey = ["Whelp";"Getter"]; - optread = (fun () -> !getter_server_name); - optwrite = (fun s -> getter_server_name := s) } - - -let make_whelp_request req c = - !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty¶m.profile=firewall&profile=firewall¶m.keys=d_c%2CC1%2CHC2%2CL¶m.embedkeys=d_c%2CTC1%2CHC2%2CL¶m.thkeys=T1%2CT2%2CL%2CE¶m.prooftreekeys=HAT%2CG%2CHAO%2CL¶m.media-type=text%2Fhtml¶m.thmedia-type=&prooftreemedia-type=¶m.doctype-public=¶m.encoding=¶m.thencoding=¶m.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE¶m.expression=" ^ c ^ "¶m.action=" ^ req - -let b = Buffer.create 16 - -let url_char c = - if 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' || - '0' <= c && c <= '9' || c ='.' - then Buffer.add_char b c - else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c)) - -let url_string s = String.iter url_char s - -let rec url_list_with_sep sep f = function - | [] -> () - | [a] -> f a - | a::l -> f a; url_string sep; url_list_with_sep sep f l - -let url_id id = url_string (Id.to_string id) - -let uri_of_dirpath dir = - url_string "cic:/"; url_list_with_sep "/" url_id (List.rev dir) - -let error_whelp_unknown_reference ref = - let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in - errorlabstrm "" - (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++ - strbrk ", are not supported in Whelp.") - -let uri_of_repr_kn ref (mp,dir,l) = - match mp with - | MPfile sl -> - uri_of_dirpath (Label.to_id l :: DirPath.repr dir @ DirPath.repr sl) - | _ -> - error_whelp_unknown_reference ref - -let url_paren f l = url_char '('; f l; url_char ')' -let url_bracket f l = url_char '['; f l; url_char ']' - -let whelp_of_glob_sort = function - | GProp -> "Prop" - | GSet -> "Set" - | GType _ -> "Type" - -let uri_int n = Buffer.add_string b (string_of_int n) - -let uri_of_ind_pointer l = - url_string ".ind#xpointer"; url_paren (url_list_with_sep "/" uri_int) l - -let uri_of_global ref = - match ref with - | VarRef id -> error ("Unknown Whelp reference: "^(Id.to_string id)^".") - | ConstRef cst -> - uri_of_repr_kn ref (repr_con cst); url_string ".con" - | IndRef (kn,i) -> - uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1] - | ConstructRef ((kn,i),j) -> - uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1;j] - -let whelm_special = Id.of_string "WHELM_ANON_VAR" - -let url_of_name = function - | Name id -> url_id id - | Anonymous -> url_id whelm_special (* No anon id in Whelp *) - -let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c - -let uri_params f = function - | [] -> () - | l -> url_string "\\subst"; - url_bracket (url_list_with_sep ";" (uri_of_binding f)) l - -let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp) - -let section_parameters = function - | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_)),_) -> - get_discharged_hyp_names (path_of_global (IndRef(induri,0))) - | GRef (_,(ConstRef cst as ref),_) -> - get_discharged_hyp_names (path_of_global ref) - | _ -> [] - -let merge vl al = - let rec aux acc = function - | ([],l) | (_,([] as l)) -> List.rev acc, l - | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al) - in aux [] (vl,al) - -let rec uri_of_constr c = - match c with - | GVar (_,id) -> url_id id - | GRef (_,ref,_) -> uri_of_global ref - | GHole _ | GEvar _ -> url_string "?" - | GSort (_,s) -> url_string (whelp_of_glob_sort s) - | GApp (_,f,args) -> - let inst,rest = merge (section_parameters f) args in - uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; - url_list_with_sep " " uri_of_constr rest - | GLambda (_,na,k,ty,c) -> - url_string "\\lambda "; url_of_name na; url_string ":"; - uri_of_constr ty; url_string "."; uri_of_constr c - | GProd (_,Anonymous,k,ty,c) -> - uri_of_constr ty; url_string "\\to "; uri_of_constr c - | GProd (_,Name id,k,ty,c) -> - url_string "\\forall "; url_id id; url_string ":"; - uri_of_constr ty; url_string "."; uri_of_constr c - | GLetIn (_,na,b,c) -> - url_string "let "; url_of_name na; url_string "\\def "; - uri_of_constr b; url_string " in "; uri_of_constr c - | GCast (_,c, (CastConv t|CastVM t|CastNative t)) -> - uri_of_constr c; url_string ":"; uri_of_constr t - | GRec _ | GIf _ | GLetTuple _ | GCases _ -> - error "Whelp does not support pattern-matching and (co-)fixpoint." - | GCast (_,_, CastCoerce) -> - anomaly (Pp.str "Written w/o parenthesis") - | GPatVar _ -> - anomaly (Pp.str "Found constructors not supported in constr") - -let make_string f x = Buffer.reset b; f x; Buffer.contents b - -let send_whelp req s = - let url = make_whelp_request req s in - let command = Util.subst_command_placeholder browser_cmd_fmt url in - let _ = CUnix.run_command ~hook:print_string command in () - -let whelp_constr env sigma req c = - let c = detype false [whelm_special] env sigma c in - send_whelp req (make_string uri_of_constr c) - -let whelp_constr_expr req c = - let (sigma,env)= Lemmas.get_current_context () in - let _,c = interp_open_constr env sigma c in - whelp_constr env sigma req c - -let whelp_locate s = - send_whelp "locate" s - -let whelp_elim ind = - send_whelp "elim" (make_string uri_of_global (IndRef ind)) - -let on_goal f = - let gls = Proof.V82.subgoals (get_pftreestate ()) in - let gls = { gls with Evd.it = List.hd gls.Evd.it } in - f (pf_env gls) (project gls) (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) - -type whelp_request = - | Locate of string - | Elim of inductive - | Constr of string * constr - -let whelp = function - | Locate s -> whelp_locate s - | Elim ind -> whelp_elim ind - | Constr (s,c) -> whelp_constr (Global.env()) (Evd.empty) s c - -VERNAC ARGUMENT EXTEND whelp_constr_request -| [ "Match" ] -> [ "match" ] -| [ "Instance" ] -> [ "instance" ] -END - -VERNAC COMMAND EXTEND Whelp CLASSIFIED AS QUERY -| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (Smartlocate.global_inductive_with_alias r) ] -| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] -END - -VERNAC COMMAND EXTEND WhelpHint CLASSIFIED AS QUERY -| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ] -| [ "Whelp" "Hint" ] => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] -> - [ on_goal (fun env sigma -> whelp_constr env sigma "hint") ] -END diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli deleted file mode 100644 index 62272c50..00000000 --- a/toplevel/whelp.mli +++ /dev/null @@ -1,20 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit -- cgit v1.2.3