diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comAssumption.ml | 296 | ||||
| -rw-r--r-- | vernac/comAssumption.mli | 37 | ||||
| -rw-r--r-- | vernac/comDefinition.ml | 1 | ||||
| -rw-r--r-- | vernac/comPrimitive.ml | 37 | ||||
| -rw-r--r-- | vernac/comPrimitive.mli | 11 | ||||
| -rw-r--r-- | vernac/declareDef.ml | 5 | ||||
| -rw-r--r-- | vernac/declareDef.mli | 2 | ||||
| -rw-r--r-- | vernac/declareObl.ml | 3 | ||||
| -rw-r--r-- | vernac/declaremods.ml | 14 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 3 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 5 | ||||
| -rw-r--r-- | vernac/locality.ml | 6 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 294 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 29 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 278 | ||||
| -rw-r--r-- | vernac/vernacinterp.mli | 33 |
18 files changed, 576 insertions, 485 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index e3f90ab98c..a0b0dcf4c8 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -11,7 +11,6 @@ open CErrors open Util open Vars -open Declare open Names open Context open Constrexpr_ops @@ -41,27 +40,24 @@ let should_axiom_into_instance = let open Decls in function true | Definitional | Logical | Conjectural -> !axiom_into_instance -let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=name} = -let open DeclareDef in -match scope with -| Discharge -> - let univs = match univs with - | Monomorphic_entry univs -> univs - | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs - in +let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let kind = Decls.IsAssumption kind in - let decl = SectionLocalAssum {typ; univs; poly; impl} in - let () = declare_variable ~name ~kind decl in - let () = assumption_message name in + let decl = Declare.SectionLocalAssum {typ; impl} in + let () = Declare.declare_variable ~name ~kind decl in + let () = Declare.assumption_message name in let r = GlobRef.VarRef name in let () = maybe_declare_manual_implicits true r imps in let env = Global.env () in let sigma = Evd.from_env env in let () = Classes.declare_instance env sigma None true r in let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in - (r,Univ.Instance.empty) + () -| Global local -> +let instance_of_univ_entry = function + | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs + | Monomorphic_entry _ -> Univ.Instance.empty + +let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name} = let do_instance = should_axiom_into_instance kind in let inl = let open Declaremods in match nl with | NoInline -> None @@ -70,42 +66,65 @@ match scope with in let kind = Decls.IsAssumption kind in let decl = Declare.ParameterEntry (None,(typ,univs),inl) in - let kn = declare_constant ~name ~local ~kind decl in + let kn = Declare.declare_constant ~name ~local ~kind decl in let gr = GlobRef.ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in let () = Declare.declare_univ_binders gr pl in - let () = assumption_message name in + let () = Declare.assumption_message name in let env = Global.env () in let sigma = Evd.from_env env in let () = if do_instance then Classes.declare_instance env sigma None false gr in - let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in - let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in - let inst = match univs with - | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs - | Monomorphic_entry _ -> Univ.Instance.empty + let local = match local with + | Declare.ImportNeedQualified -> true + | Declare.ImportDefaultBehavior -> false in + let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in + let inst = instance_of_univ_entry univs in (gr,inst) let interp_assumption ~program_mode sigma env impls c = let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in sigma, (ty, impls) -(* When monomorphic the universe constraints are declared with the first declaration only. *) -let next_uctx = - let empty_uctx = Monomorphic_entry Univ.ContextSet.empty in +(* When monomorphic the universe constraints and universe names are + declared with the first declaration only. *) +let next_univs = + let empty_univs = Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders in function - | Polymorphic_entry _ as uctx -> uctx - | Monomorphic_entry _ -> empty_uctx + | Polymorphic_entry _, _ as univs -> univs + | Monomorphic_entry _, _ -> empty_univs -let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl = - let refs, _ = - List.fold_left (fun (refs,uctx) id -> - let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps Glob_term.Explicit nl id in - ref::refs, next_uctx uctx) - ([],uctx) idl - in - List.rev refs +let context_set_of_entry = function + | Polymorphic_entry (_,uctx) -> Univ.ContextSet.of_context uctx + | Monomorphic_entry uctx -> uctx +let declare_assumptions ~poly ~scope ~kind univs nl l = + let open DeclareDef in + let () = match scope with + | Discharge -> + (* declare universes separately for variables *) + Declare.declare_universe_context ~poly (context_set_of_entry (fst univs)) + | Global _ -> () + in + let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) -> + (* NB: here univs are ignored when scope=Discharge *) + let typ = replace_vars subst typ in + let univs,subst' = + List.fold_left_map (fun univs id -> + let refu = match scope with + | Discharge -> + declare_variable is_coe ~kind typ imps Glob_term.Explicit id; + GlobRef.VarRef id.CAst.v, Univ.Instance.empty + | Global local -> + declare_axiom is_coe ~local ~poly ~kind typ univs imps nl id + in + next_univs univs, (id.CAst.v, Constr.mkRef refu)) + univs idl + in + subst'@subst, next_univs univs) + ([], univs) l + in + () let maybe_error_many_udecls = function | ({CAst.loc;v=id}, Some _) -> @@ -175,139 +194,114 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = IMO, thus I think we should adapt `prepare_parameter` to handle this case too. *) let sigma = Evd.restrict_universe_context sigma uvars in - let uctx = Evd.check_univ_decl ~poly sigma udecl in + let univs = Evd.check_univ_decl ~poly sigma udecl in let ubinders = Evd.universe_binders sigma in - let _, _ = List.fold_left (fun (subst,uctx) ((is_coe,idl),typ,imps) -> - let typ = replace_vars subst typ in - let refs = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in - let subst' = List.map2 - (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) - idl refs - in - subst'@subst, next_uctx uctx) - ([], uctx) l + declare_assumptions ~poly ~scope ~kind (univs,ubinders) nl l + +let context_subst subst (name,b,t,impl) = + name, Option.map (Vars.substl subst) b, Vars.substl subst t, impl + +let context_insection sigma ~poly ctx = + let uctx = Evd.universe_context_set sigma in + let () = Declare.declare_universe_context ~poly uctx in + let fn subst (name,_,_,_ as d) = + let d = context_subst subst d in + let () = match d with + | name, None, t, impl -> + let kind = Decls.Context in + declare_variable false ~kind t [] impl (CAst.make name) + | name, Some b, t, impl -> + (* We need to get poly right for check_same_poly *) + let univs = if poly then Polymorphic_entry ([| |], Univ.UContext.empty) + else Monomorphic_entry Univ.ContextSet.empty + in + let entry = Declare.definition_entry ~univs ~types:t b in + let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge + ~kind:Decls.(IsDefinition Definition) UnivNames.empty_binders entry [] + in + () + in + Constr.mkVar name :: subst in + let _ : Vars.substl = List.fold_left fn [] ctx in () -let do_primitive id prim typopt = - if Lib.sections_are_opened () then - CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections."); - if Dumpglob.dump () then Dumpglob.dump_definition id false "ax"; - let env = Global.env () in - let evd = Evd.from_env env in - let evd, typopt = Option.fold_left_map - (interp_type_evars_impls ~impls:empty_internalization_env env) - evd typopt - in - let evd = Evd.minimize_universes evd in - let uvars, impls, typopt = match typopt with - | None -> Univ.LSet.empty, [], None - | Some (ty,impls) -> - EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty) +let context_nosection sigma ~poly ctx = + let univs = + match ctx, poly with + | [_], _ | _, true -> Evd.univ_entry ~poly sigma + | _, false -> + (* Multiple monomorphic axioms: declare universes separately to + avoid redeclaring them. *) + let uctx = Evd.universe_context_set sigma in + let () = Declare.declare_universe_context ~poly uctx in + Monomorphic_entry Univ.ContextSet.empty in - let evd = Evd.restrict_universe_context evd uvars in - let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in - let entry = { prim_entry_type = typopt; - prim_entry_univs = uctx; - prim_entry_content = prim; - } + let fn subst d = + let (name,b,t,_impl) = context_subst subst d in + let kind = Decls.(IsAssumption Logical) in + let decl = match b with + | None -> + Declare.ParameterEntry (None,(t,univs),None) + | Some b -> + let entry = Declare.definition_entry ~univs ~types:t b in + Declare.DefinitionEntry entry + in + let local = if Lib.is_modtype () then Declare.ImportDefaultBehavior + else Declare.ImportNeedQualified + in + let cst = Declare.declare_constant ~name ~kind ~local decl in + let () = Declare.assumption_message name in + let env = Global.env () in + (* why local when is_modtype? *) + let () = if Lib.is_modtype() || Option.is_empty b then + Classes.declare_instance env sigma None (Lib.is_modtype()) (GlobRef.ConstRef cst) + in + Constr.mkConstU (cst,instance_of_univ_entry univs) :: subst in - let _kn : Names.Constant.t = - declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (PrimitiveEntry entry) in - Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared") - -let named_of_rel_context l = - let open EConstr.Vars in - let open RelDecl in - let acc, ctx = - List.fold_right - (fun decl (subst, ctx) -> - let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in - let d = match decl with - | LocalAssum (_,t) -> id, None, substl subst t - | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in - (EConstr.mkVar id :: subst, d :: ctx)) - l ([], []) - in ctx + let _ : Vars.substl = List.fold_left fn [] ctx in + () let context ~poly l = let env = Global.env() in let sigma = Evd.from_env env in - let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in + let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in (* Note, we must use the normalized evar from now on! *) let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in - let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in - let ctx = - try named_of_rel_context fullctx - with e when CErrors.noncritical e -> - user_err Pp.(str "Anonymous variables not allowed in contexts.") - in - let univs = - match ctx with - | [] -> assert false - | [_] -> Evd.univ_entry ~poly sigma - | _::_::_ -> - if Lib.sections_are_opened () - then - (* More than 1 variable in a section: we can't associate - universes to any specific variable so we declare them - separately. *) - begin - let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context ~poly uctx; - if poly then Polymorphic_entry ([||], Univ.UContext.empty) - else Monomorphic_entry Univ.ContextSet.empty - end - else if poly then - (* Multiple polymorphic axioms: they are all polymorphic the same way. *) - Evd.univ_entry ~poly sigma - else - (* Multiple monomorphic axioms: declare universes separately - to avoid redeclaring them. *) - begin - let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context ~poly uctx; - Monomorphic_entry Univ.ContextSet.empty - end - in - let fn (name, b, t) = - let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in - if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - (* Declare the universe context once *) - let kind = Decls.(IsAssumption Logical) in - let decl = match b with - | None -> - Declare.ParameterEntry (None,(t,univs),None) - | Some b -> - let entry = Declare.definition_entry ~univs ~types:t b in - Declare.DefinitionEntry entry + let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in + (* reorder, evar-normalize and add implicit status *) + let ctx = List.rev_map (fun d -> + let {binder_name=name}, b, t = RelDecl.to_tuple d in + let name = match name with + | Anonymous -> user_err Pp.(str "Anonymous variables not allowed in contexts.") + | Name id -> id in - let cst = Declare.declare_constant ~name ~kind decl in - let env = Global.env () in - Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (GlobRef.ConstRef cst); - () - else + let b = Option.map (EConstr.to_constr sigma) b in + let t = EConstr.to_constr sigma t in let test x = match x.CAst.v with | Some (Name id',_) -> Id.equal name id' | _ -> false in - let impl = if List.exists test impls then Glob_term.Implicit else Glob_term.Explicit in - let scope = - if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in - match b with - | None -> - let _, _ = - declare_assumption false ~scope ~poly ~kind:Decls.Context t - univs UnivNames.empty_binders [] impl - Declaremods.NoInline (CAst.make name) - in - () - | Some b -> - let entry = Declare.definition_entry ~univs ~types:t b in - let _gr = DeclareDef.declare_definition - ~name ~scope:DeclareDef.Discharge - ~kind:Decls.Definition UnivNames.empty_binders entry [] in - () + let impl = Glob_term.(if List.exists test impls then Implicit else Explicit) in + name,b,t,impl) + ctx in - List.iter fn (List.rev ctx) + if Global.sections_are_opened () + then context_insection sigma ~poly ctx + else context_nosection sigma ~poly ctx + +(* Deprecated *) +let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl name = +let open DeclareDef in +match scope with +| Discharge -> + let univs = match univs with + | Monomorphic_entry univs -> univs + | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs + in + let () = Declare.declare_universe_context ~poly univs in + declare_variable is_coe ~kind typ imps impl name; + GlobRef.VarRef name.CAst.v, Univ.Instance.empty +| Global local -> + declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl name diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 2715bd8305..ae9edefcac 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -23,29 +23,46 @@ val do_assumptions -> (ident_decl list * constr_expr) with_coercion list -> unit -(** returns [false] if the assumption is neither local to a section, - nor in a module type and meant to be instantiated. *) -val declare_assumption +val declare_variable : coercion_flag - -> poly:bool - -> scope:DeclareDef.locality -> kind:Decls.assumption_object_kind -> Constr.types - -> Entries.universes_entry - -> UnivNames.universe_binders -> Impargs.manual_implicits -> Glob_term.binding_kind + -> variable CAst.t + -> unit + +val declare_axiom + : coercion_flag + -> poly:bool + -> local:Declare.import_status + -> kind:Decls.assumption_object_kind + -> Constr.types + -> Entries.universes_entry * UnivNames.universe_binders + -> Impargs.manual_implicits -> Declaremods.inline -> variable CAst.t -> GlobRef.t * Univ.Instance.t (** Context command *) -(** returns [false] if, for lack of section, it declares an assumption - (unless in a module type). *) val context : poly:bool -> local_binder_expr list -> unit -val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit +(** Deprecated *) +val declare_assumption + : coercion_flag + -> poly:bool + -> scope:DeclareDef.locality + -> kind:Decls.assumption_object_kind + -> Constr.types + -> Entries.universes_entry + -> UnivNames.universe_binders + -> Impargs.manual_implicits + -> Glob_term.binding_kind + -> Declaremods.inline + -> variable CAst.t + -> GlobRef.t * Univ.Instance.t +[@@ocaml.deprecated "Use declare_variable or declare_axiom instead."] diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 9745358ba2..5b3f15a08c 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -104,4 +104,5 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o let ce = check_definition ~program_mode def in let uctx = Evd.evar_universe_context evd in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in + let kind = Decls.IsDefinition kind in ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps) diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml new file mode 100644 index 0000000000..b66ff876d3 --- /dev/null +++ b/vernac/comPrimitive.ml @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let do_primitive id prim typopt = + if Global.sections_are_opened () then + CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections."); + if Dumpglob.dump () then Dumpglob.dump_definition id false "ax"; + let env = Global.env () in + let evd = Evd.from_env env in + let evd, typopt = Option.fold_left_map + Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env env) + evd typopt + in + let evd = Evd.minimize_universes evd in + let uvars, impls, typopt = match typopt with + | None -> Univ.LSet.empty, [], None + | Some (ty,impls) -> + EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty) + in + let evd = Evd.restrict_universe_context evd uvars in + let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in + let entry = Entries.{ + prim_entry_type = typopt; + prim_entry_univs = uctx; + prim_entry_content = prim; + } + in + let _kn : Names.Constant.t = + Declare.declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry) in + Flags.if_verbose Feedback.msg_info Pp.(Names.Id.print id.CAst.v ++ str " is declared") diff --git a/vernac/comPrimitive.mli b/vernac/comPrimitive.mli new file mode 100644 index 0000000000..c0db1cc464 --- /dev/null +++ b/vernac/comPrimitive.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val do_primitive : Names.lident -> CPrimitives.op_or_type -> Constrexpr.constr_expr option -> unit diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 1926faaf0e..67733c95a1 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -48,11 +48,11 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let gr = match scope with | Discharge -> let () = - declare_variable ~name ~kind:Decls.(IsDefinition kind) (SectionLocalDef ce) + declare_variable ~name ~kind (SectionLocalDef ce) in Names.GlobRef.VarRef name | Global local -> - let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in + let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in let gr = Names.GlobRef.ConstRef kn in let () = Declare.declare_univ_binders gr udecl in gr @@ -69,6 +69,7 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in + let kind = Decls.IsDefinition kind in declare_definition ~name ~scope ~kind ?hook_data udecl ce imps let check_definition_evars ~allow_evars sigma = diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 54a0c9a7e8..d6001f5970 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -42,7 +42,7 @@ end val declare_definition : name:Id.t -> scope:locality - -> kind:Decls.definition_object_kind + -> kind:Decls.logical_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> UnivNames.universe_binders -> Evd.side_effects Declare.proof_entry diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 8fd6bc7eab..2c56f707f1 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -351,7 +351,8 @@ let declare_definition prg = let ubinders = UState.universe_binders uctx in let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in DeclareDef.declare_definition - ~name:prg.prg_name ~scope:prg.prg_scope ubinders ~kind:prg.prg_kind ce + ~name:prg.prg_name ~scope:prg.prg_scope ubinders + ~kind:Decls.(IsDefinition prg.prg_kind) ce prg.prg_implicits ?hook_data let rec lam_index n t acc = diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 58a7dff5fd..c7b68d18c2 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -211,7 +211,7 @@ let compute_visibility exists i = (** Iterate some function [iter_objects] on all components of a module *) let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs = - let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir ; obj_mp; } in let dirinfo = Nametab.GlobDirRef.DirModule prefix in consistency_checks exists obj_dir dirinfo; Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo; @@ -266,14 +266,14 @@ and load_objects i prefix objs = and load_include i ((sp,kn), aobjs) = let obj_dir = Libnames.dirpath sp in let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir; obj_mp; } in let o = expand_aobjs aobjs in load_objects i prefix o and load_keep i ((sp,kn),kobjs) = (* Invariant : seg isn't empty *) let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in - let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir ; obj_mp; } in let modobjs = try ModObjs.get obj_mp with Not_found -> assert false (* a substobjs should already be loaded *) @@ -327,7 +327,7 @@ let rec open_object i (name, obj) = | KeepObject objs -> open_keep i (name, objs) and open_module i obj_dir obj_mp sobjs = - let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir ; obj_mp; } in let dirinfo = Nametab.GlobDirRef.DirModule prefix in consistency_checks true obj_dir dirinfo; Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo; @@ -353,7 +353,7 @@ and open_modtype i ((sp,kn),_) = and open_include i ((sp,kn), aobjs) = let obj_dir = Libnames.dirpath sp in let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir; obj_mp; } in let o = expand_aobjs aobjs in open_objects i prefix o @@ -363,7 +363,7 @@ and open_export i mpl = and open_keep i ((sp,kn),kobjs) = let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir; obj_mp; } in open_objects i prefix kobjs let rec cache_object (name, obj) = @@ -380,7 +380,7 @@ let rec cache_object (name, obj) = and cache_include ((sp,kn), aobjs) = let obj_dir = Libnames.dirpath sp in let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir; obj_mp; } in let o = expand_aobjs aobjs in load_objects 1 prefix o; open_objects 1 prefix o diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 8a94a010a0..efcb2635be 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -62,7 +62,8 @@ let make_bullet s = | _ -> assert false let parse_compat_version = let open Flags in function - | "8.10" -> Current + | "8.11" -> Current + | "8.10" -> V8_10 | "8.9" -> V8_9 | "8.8" -> V8_8 | ("8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 42d1a1f3fc..e49277c51b 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -265,7 +265,8 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect Univ.ContextSet.of_context univs | Monomorphic_entry univs -> univs in - let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in + let () = Declare.declare_universe_context ~poly univs in + let c = Declare.SectionLocalAssum {typ=t_i; impl} in let () = Declare.declare_variable ~name ~kind c in GlobRef.VarRef name, impargs | Global local -> @@ -359,7 +360,7 @@ let save_lemma_admitted ~(lemma : t) : unit = let env = Global.env () in let ids_typ = Environ.global_vars_set env typ in let ids_def = Environ.global_vars_set env pproof in - Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) + Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None in let universes = Proof_global.get_initial_euctx lemma.proof in let ctx = UState.check_univ_decl ~poly universes udecl in diff --git a/vernac/locality.ml b/vernac/locality.ml index f033d32874..5862f51b43 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -39,7 +39,7 @@ let enforce_locality_exp locality_flag discharge = match locality_flag, discharge with | Some b, NoDischarge -> Global (importability_of_bool b) | None, NoDischarge -> Global Declare.ImportDefaultBehavior - | None, DoDischarge when not (Lib.sections_are_opened ()) -> + | None, DoDischarge when not (Global.sections_are_opened ()) -> (* If a Let/Variable is defined outside a section, then we consider it as a local definition *) warn_local_declaration (); Global Declare.ImportNeedQualified @@ -55,7 +55,7 @@ let enforce_locality locality_flag = 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 () + function Some b -> b | None -> Global.sections_are_opened () let enforce_section_locality locality_flag = make_section_locality locality_flag @@ -68,7 +68,7 @@ let enforce_section_locality locality_flag = let make_module_locality = function | Some false -> - if Lib.sections_are_opened () then + if Global.sections_are_opened () then CErrors.user_err Pp.(str "This command does not support the Global option in sections."); false diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 4868182bb3..afc701edbc 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -26,16 +26,16 @@ Indschemes Obligations ComDefinition Classes +ComPrimitive ComAssumption ComInductive ComFixpoint ComProgramFixpoint Record Assumptions -Vernacstate Mltop Topfmt Loadpath Vernacentries - -Misctypes +Vernacstate +Vernacinterp diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ca29a6afb9..430cee62c2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -35,12 +35,6 @@ module NamedDecl = Context.Named.Declaration (** TODO: make this function independent of Ltac *) let (f_interp_redexp, interp_redexp_hook) = Hook.make () -let debug = false - -(* XXX Should move to a common library *) -let vernac_pperr_endline pp = - if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else () - (* Utility functions, at some point they should all disappear and instead enviroment/state selection should be done at the Vernac DSL level. *) @@ -468,28 +462,6 @@ let vernac_notation ~atts = let vernac_custom_entry ~module_local s = Metasyntax.declare_custom_entry module_local s -(* Default proof mode, to be set at the beginning of proofs for - programs that cannot be statically classified. *) -let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode) -let get_default_proof_mode () = !default_proof_mode - -let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode -let set_default_proof_mode_opt name = - default_proof_mode := - match Pvernac.lookup_proof_mode name with - | Some pm -> pm - | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)) - -let proof_mode_opt_name = ["Default";"Proof";"Mode"] -let () = - Goptions.declare_string_option Goptions.{ - optdepr = false; - optname = "default proof mode" ; - optkey = proof_mode_opt_name; - optread = get_default_proof_mode_opt; - optwrite = set_default_proof_mode_opt; - } - (***********) (* Gallina *) @@ -838,14 +810,14 @@ let vernac_combined_scheme lid l = Indschemes.do_combined_scheme lid l let vernac_universe ~poly l = - if poly && not (Lib.sections_are_opened ()) then + if poly && not (Global.sections_are_opened ()) then user_err ~hdr:"vernac_universe" (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); Declare.do_universe ~poly l let vernac_constraint ~poly l = - if poly && not (Lib.sections_are_opened ()) then + if poly && not (Global.sections_are_opened ()) then user_err ~hdr:"vernac_constraint" (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); @@ -865,7 +837,7 @@ let vernac_import 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) and what module information is supplied *) - if Lib.sections_are_opened () then + if Global.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); let binders_ast = List.map (fun (export,idl,ty) -> @@ -880,7 +852,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = 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) and what module information is supplied *) - if Lib.sections_are_opened () then + if Global.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mexpr_ast_l with | [] -> @@ -921,7 +893,7 @@ let vernac_end_module export {loc;v=id} = 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 + if Global.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mty_ast_l with @@ -967,7 +939,9 @@ let vernac_include l = Declaremods.declare_include l let vernac_begin_section ~poly ({v=id} as lid) = Dumpglob.dump_definition lid true "sec"; - Lib.open_section ~poly id; + Lib.open_section id; + (* If there was no polymorphism attribute this just sets the option + to its current value ie noop. *) set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly let vernac_end_section {CAst.loc} = @@ -995,7 +969,7 @@ let warn_require_in_section = (fun () -> strbrk "Use of “Require” inside a section is deprecated.") let vernac_require from import qidl = - if Lib.sections_are_opened () then warn_require_in_section (); + if Global.sections_are_opened () then warn_require_in_section (); let root = match from with | None -> None | Some from -> @@ -2124,7 +2098,7 @@ let vernac_register qid r = | RegisterCoqlib n -> let ns, id = Libnames.repr_qualid n in if DirPath.equal (dirpath_of_string "kernel") ns then begin - if Lib.sections_are_opened () then + if Global.sections_are_opened () then user_err Pp.(str "Registering a kernel type is not allowed in sections"); let pind = match Id.to_string id with | "ind_bool" -> CPrimitives.PIT_bool @@ -2235,115 +2209,9 @@ let vernac_check_guard ~pstate = (str ("Condition violated: ") ++s) in message -(** A global default timeout, controlled by option "Set Default Timeout n". - Use "Unset Default Timeout" to deactivate it (or set it to 0). *) - -let default_timeout = ref None - -(* Timeout *) -let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b = - match !default_timeout, timeout with - | _, Some n - | Some n, None -> - Control.timeout n f x Timeout - | None, None -> - f x - -(* Fail *) -let test_mode = ref false - -(* Restoring the state is the caller's responsibility *) -let with_fail f : (Pp.t, unit) result = - try - let _ = f () in - Error () - with - (* Fail Timeout is a common pattern so we need to support it. *) - | e when CErrors.noncritical e || e = Timeout -> - (* The error has to be printed in the failing state *) - Ok CErrors.(iprint (push e)) - -(* We restore the state always *) -let with_fail ~st f = - let res = with_fail f in - Vernacstate.invalidate_cache (); - Vernacstate.unfreeze_interp_state st; - match res with - | Error () -> - user_err ~hdr:"Fail" (str "The command has not failed!") - | Ok msg -> - if not !Flags.quiet || !test_mode - then Feedback.msg_notice (str "The command has indeed failed with message:" ++ fnl () ++ msg) - -let locate_if_not_already ?loc (e, info) = - match Loc.get_loc info with - | None -> (e, Option.cata (Loc.add_loc info) info loc) - | Some l -> (e, info) - -let mk_time_header = - (* Drop the time header to print the command, we should indeed use a - different mechanism to `-time` commands than the current hack of - adding a time control to the AST. *) - let pr_time_header vernac = - let vernac = match vernac with - | { v = { control = ControlTime _ :: control; attrs; expr }; loc } -> - CAst.make ?loc { control; attrs; expr } - | _ -> vernac - in - Topfmt.pr_cmd_header vernac - in - fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac) - -let interp_control_flag ~time_header (f : control_flag) ~st - (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) = - match f with - | ControlFail -> - with_fail ~st (fun () -> fn ~st); - st.Vernacstate.lemmas - | ControlTimeout timeout -> - vernac_timeout ~timeout (fun () -> fn ~st) () - | ControlTime batch -> - let header = if batch then Lazy.force time_header else Pp.mt () in - System.with_time ~batch ~header (fun () -> fn ~st) () - | ControlRedirect s -> - Topfmt.with_output_to_file s (fun () -> fn ~st) () - -(* EJGA: We may remove this, only used twice below *) -let vernac_require_open_lemma ~stack f = - match stack with - | Some stack -> f stack - | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)") - -let interp_typed_vernac c ~stack = - let open Vernacextend in - match c with - | VtDefault f -> f (); stack - | VtNoProof f -> - if Option.has_some stack then - user_err Pp.(str "Command not supported (Open proofs remain)"); - let () = f () in - stack - | VtCloseProof f -> - vernac_require_open_lemma ~stack (fun stack -> - let lemma, stack = Vernacstate.LemmaStack.pop stack in - f ~lemma; - stack) - | VtOpenProof f -> - Some (Vernacstate.LemmaStack.push stack (f ())) - | VtModifyProof f -> - Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack - | VtReadProofOpt f -> - let pstate = Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:(fun x -> x)) stack in - f ~pstate; - stack - | VtReadProof f -> - vernac_require_open_lemma ~stack - (Vernacstate.LemmaStack.with_top_pstate ~f:(fun pstate -> f ~pstate)); - stack - (* We interpret vernacular commands to a DSL that specifies their allowed actions on proof states *) -let rec translate_vernac ~atts v = let open Vernacextend in match v with +let translate_vernac ~atts v = let open Vernacextend in match v with | VernacAbortAll | VernacRestart | VernacUndo _ @@ -2353,6 +2221,9 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacBack _ | VernacAbort _ -> anomaly (str "type_vernac") + | VernacLoad _ -> + anomaly (str "Load is not supported recursively") + (* Syntax *) | VernacSyntaxExtension (infix, sl) -> VtDefault(fun () -> with_module_locality ~atts vernac_syntax_extension infix sl) @@ -2605,7 +2476,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacPrimitive (id, prim, typopt) -> VtDefault(fun () -> unsupported_attributes atts; - ComAssumption.do_primitive id prim typopt) + ComPrimitive.do_primitive id prim typopt) | VernacComments l -> VtDefault(fun () -> unsupported_attributes atts; @@ -2654,141 +2525,6 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacEndProof pe -> VtCloseProof (vernac_end_proof pe) - | VernacLoad (verbosely,fname) -> - VtNoProof(fun () -> - unsupported_attributes atts; - vernac_load ~verbosely fname) - (* Extensions *) | VernacExtend (opn,args) -> Vernacextend.type_vernac ~atts opn args - -(* "locality" is the prefix "Local" attribute, while the "local" component - * is the outdated/deprecated "Local" attribute of some vernacular commands - * still parsed as the obsolete_locality grammar entry for retrocompatibility. - * loc is the Loc.t of the vernacular command being interpreted. *) -and interp_expr ~atts ~st c = - let stack = st.Vernacstate.lemmas in - vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); - match c with - - (* The STM should handle that, but LOAD bypasses the STM... *) - | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") - | 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") - - (* Resetting *) - | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") - | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") - | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") - - (* This one is possible to handle here *) - | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") - - | v -> - let fv = translate_vernac ~atts v in - interp_typed_vernac ~stack fv - -(* XXX: This won't properly set the proof mode, as of today, it is - controlled by the STM. Thus, we would need access information from - the classifier. The proper fix is to move it to the STM, however, - the way the proof mode is set there makes the task non trivial - without a considerable amount of refactoring. -*) -and vernac_load ~verbosely fname = - let exception End_of_input in - - (* Note that no proof should be open here, so the state here is just token for now *) - let st = Vernacstate.freeze_interp_state ~marshallable:false in - let fname = - Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in - let fname = CUnix.make_suffix fname ".v" in - let input = - let longfname = Loadpath.locate_file fname in - let in_chan = open_utf8_file_in longfname in - Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in - (* Parsing loop *) - let v_mod = if verbosely then Flags.verbosely else Flags.silently in - let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing - (fun po -> - match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with - | Some x -> x - | None -> raise End_of_input) in - let rec load_loop ~stack = - try - let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in - let stack = - v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) - (parse_sentence proof_mode input) in - load_loop ~stack - with - End_of_input -> - stack - in - let stack = load_loop ~stack:st.Vernacstate.lemmas in - (* If Load left a proof open, we fail too. *) - if Option.has_some stack then - CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); - () - -and interp_control ~st ({ v = cmd } as vernac) = - let time_header = mk_time_header vernac in - List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) - cmd.control - (fun ~st -> - let before_univs = Global.universes () in - let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in - if before_univs == Global.universes () then pstack - else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack) - ~st - -(* Interpreting a possibly delayed proof *) -let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option = - let stack = st.Vernacstate.lemmas in - let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in - let () = match pe with - | Admitted -> - save_lemma_admitted_delayed ~proof ~info - | Proved (_,idopt) -> - save_lemma_proved_delayed ~proof ~info ~idopt in - stack - -let interp_qed_delayed_control ~proof ~info ~st ~control { loc; v=pe } = - let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in - List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) - control - (fun ~st -> interp_qed_delayed ~proof ~info ~st pe) - ~st - -(* General interp with management of state *) -let () = - declare_int_option - { optdepr = false; - optname = "the default timeout"; - optkey = ["Default";"Timeout"]; - optread = (fun () -> !default_timeout); - optwrite = ((:=) default_timeout) } - -(* Be careful with the cache here in case of an exception. *) -let interp_gen ~verbosely ~st ~interp_fn cmd = - Vernacstate.unfreeze_interp_state st; - try vernac_timeout (fun st -> - let v_mod = if verbosely then Flags.verbosely else Flags.silently in - let ontop = v_mod (interp_fn ~st) cmd in - Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"]; - Vernacstate.freeze_interp_state ~marshallable:false - ) st - with exn -> - let exn = CErrors.push exn in - let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in - Vernacstate.invalidate_cache (); - iraise exn - -(* Regular interp *) -let interp ?(verbosely=true) ~st cmd = - interp_gen ~verbosely ~st ~interp_fn:interp_control cmd - -let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t = - interp_gen ~verbosely:false ~st - ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index e65f9d3cfe..6368ebeed8 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -8,25 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** The main interpretation function of vernacular expressions *) -val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t - -(** Execute a Qed but with a proof_object which may contain a delayed - proof and won't be forced *) -val interp_qed_delayed_proof - : proof:Proof_global.proof_object - -> info:Lemmas.Info.t - -> st:Vernacstate.t - -> control:Vernacexpr.control_flag list - -> Vernacexpr.proof_end CAst.t - -> Vernacstate.t - -(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *) -val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit - -(** Flag set when the test-suite is called. Its only effect to display - verbose information for [Fail] *) -val test_mode : bool ref +(** Vernac Translation into the Vernac DSL *) +val translate_vernac + : atts:Attributes.vernac_flags + -> Vernacexpr.vernac_expr + -> Vernacextend.typed_vernac (** Vernacular require command *) val vernac_require : @@ -38,8 +24,3 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr (** Miscellaneous stuff *) val command_focus : unit Proof.focus_kind - -(** Default proof mode set by `start_proof` *) -val get_default_proof_mode : unit -> Pvernac.proof_mode - -val proof_mode_opt_name : string list diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 2725516a76..e29086d726 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -54,7 +54,6 @@ and proof_block_name = string (** open type of delimiters *) type typed_vernac = | VtDefault of (unit -> unit) - | VtNoProof of (unit -> unit) | VtCloseProof of (lemma:Lemmas.t -> unit) | VtOpenProof of (unit -> Lemmas.t) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml new file mode 100644 index 0000000000..c14fc78462 --- /dev/null +++ b/vernac/vernacinterp.ml @@ -0,0 +1,278 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Vernacexpr + +(* XXX Should move to a common library *) +let debug = false +let vernac_pperr_endline pp = + if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else () + +(* EJGA: We may remove this, only used twice below *) +let vernac_require_open_lemma ~stack f = + match stack with + | Some stack -> f stack + | None -> + CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress)") + +let interp_typed_vernac c ~stack = + let open Vernacextend in + match c with + | VtDefault f -> f (); stack + | VtNoProof f -> + if Option.has_some stack then + CErrors.user_err (Pp.str "Command not supported (Open proofs remain)"); + let () = f () in + stack + | VtCloseProof f -> + vernac_require_open_lemma ~stack (fun stack -> + let lemma, stack = Vernacstate.LemmaStack.pop stack in + f ~lemma; + stack) + | VtOpenProof f -> + Some (Vernacstate.LemmaStack.push stack (f ())) + | VtModifyProof f -> + Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack + | VtReadProofOpt f -> + let pstate = Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:(fun x -> x)) stack in + f ~pstate; + stack + | VtReadProof f -> + vernac_require_open_lemma ~stack + (Vernacstate.LemmaStack.with_top_pstate ~f:(fun pstate -> f ~pstate)); + stack + +(* Default proof mode, to be set at the beginning of proofs for + programs that cannot be statically classified. *) +let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode) +let get_default_proof_mode () = !default_proof_mode + +let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode +let set_default_proof_mode_opt name = + default_proof_mode := + match Pvernac.lookup_proof_mode name with + | Some pm -> pm + | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)) + +let proof_mode_opt_name = ["Default";"Proof";"Mode"] +let () = + Goptions.declare_string_option Goptions.{ + optdepr = false; + optname = "default proof mode" ; + optkey = proof_mode_opt_name; + optread = get_default_proof_mode_opt; + optwrite = set_default_proof_mode_opt; + } + +(** A global default timeout, controlled by option "Set Default Timeout n". + Use "Unset Default Timeout" to deactivate it (or set it to 0). *) + +let default_timeout = ref None + +(* Timeout *) +let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b = + match !default_timeout, timeout with + | _, Some n + | Some n, None -> + Control.timeout n f x CErrors.Timeout + | None, None -> + f x + +(* Fail *) +let test_mode = ref false + +(* Restoring the state is the caller's responsibility *) +let with_fail f : (Pp.t, unit) result = + try + let _ = f () in + Error () + with + (* Fail Timeout is a common pattern so we need to support it. *) + | e when CErrors.noncritical e || e = CErrors.Timeout -> + (* The error has to be printed in the failing state *) + Ok CErrors.(iprint (push e)) + +(* We restore the state always *) +let with_fail ~st f = + let res = with_fail f in + Vernacstate.invalidate_cache (); + Vernacstate.unfreeze_interp_state st; + match res with + | Error () -> + CErrors.user_err ~hdr:"Fail" (Pp.str "The command has not failed!") + | Ok msg -> + if not !Flags.quiet || !test_mode + then Feedback.msg_notice Pp.(str "The command has indeed failed with message:" ++ fnl () ++ msg) + +let locate_if_not_already ?loc (e, info) = + match Loc.get_loc info with + | None -> (e, Option.cata (Loc.add_loc info) info loc) + | Some l -> (e, info) + +let mk_time_header = + (* Drop the time header to print the command, we should indeed use a + different mechanism to `-time` commands than the current hack of + adding a time control to the AST. *) + let pr_time_header vernac = + let vernac = match vernac with + | { CAst.v = { control = ControlTime _ :: control; attrs; expr }; loc } -> + CAst.make ?loc { control; attrs; expr } + | _ -> vernac + in + Topfmt.pr_cmd_header vernac + in + fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac) + +let interp_control_flag ~time_header (f : control_flag) ~st + (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) = + match f with + | ControlFail -> + with_fail ~st (fun () -> fn ~st); + st.Vernacstate.lemmas + | ControlTimeout timeout -> + vernac_timeout ~timeout (fun () -> fn ~st) () + | ControlTime batch -> + let header = if batch then Lazy.force time_header else Pp.mt () in + System.with_time ~batch ~header (fun () -> fn ~st) () + | ControlRedirect s -> + Topfmt.with_output_to_file s (fun () -> fn ~st) () + +(* "locality" is the prefix "Local" attribute, while the "local" component + * is the outdated/deprecated "Local" attribute of some vernacular commands + * still parsed as the obsolete_locality grammar entry for retrocompatibility. + * loc is the Loc.t of the vernacular command being interpreted. *) +let rec interp_expr ~atts ~st c = + let stack = st.Vernacstate.lemmas in + vernac_pperr_endline Pp.(fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); + match c with + + (* The STM should handle that, but LOAD bypasses the STM... *) + | VernacAbortAll -> CErrors.user_err (Pp.str "AbortAll cannot be used through the Load command") + | VernacRestart -> CErrors.user_err (Pp.str "Restart cannot be used through the Load command") + | VernacUndo _ -> CErrors.user_err (Pp.str "Undo cannot be used through the Load command") + | VernacUndoTo _ -> CErrors.user_err (Pp.str "UndoTo cannot be used through the Load command") + + (* Resetting *) + | VernacResetName _ -> CErrors.anomaly (Pp.str "VernacResetName not handled by Stm.") + | VernacResetInitial -> CErrors.anomaly (Pp.str "VernacResetInitial not handled by Stm.") + | VernacBack _ -> CErrors.anomaly (Pp.str "VernacBack not handled by Stm.") + + (* This one is possible to handle here *) + | VernacAbort id -> CErrors.user_err (Pp.str "Abort cannot be used through the Load command") + | VernacLoad (verbosely, fname) -> + Attributes.unsupported_attributes atts; + vernac_load ~verbosely fname + | v -> + let fv = Vernacentries.translate_vernac ~atts v in + interp_typed_vernac ~stack fv + +and vernac_load ~verbosely fname = + let exception End_of_input in + + (* Note that no proof should be open here, so the state here is just token for now *) + let st = Vernacstate.freeze_interp_state ~marshallable:false in + let fname = + Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (Pp.str x)) fname in + let fname = CUnix.make_suffix fname ".v" in + let input = + let longfname = Loadpath.locate_file fname in + let in_chan = Util.open_utf8_file_in longfname in + Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in + (* Parsing loop *) + let v_mod = if verbosely then Flags.verbosely else Flags.silently in + let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing + (fun po -> + match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with + | Some x -> x + | None -> raise End_of_input) in + let rec load_loop ~stack = + try + let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in + let stack = + v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) + (parse_sentence proof_mode input) in + load_loop ~stack + with + End_of_input -> + stack + in + let stack = load_loop ~stack:st.Vernacstate.lemmas in + (* If Load left a proof open, we fail too. *) + if Option.has_some stack then + CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); + stack + +and interp_control ~st ({ CAst.v = cmd } as vernac) = + let time_header = mk_time_header vernac in + List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) + cmd.control + (fun ~st -> + let before_univs = Global.universes () in + let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in + if before_univs == Global.universes () then pstack + else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack) + ~st + +(* XXX: This won't properly set the proof mode, as of today, it is + controlled by the STM. Thus, we would need access information from + the classifier. The proper fix is to move it to the STM, however, + the way the proof mode is set there makes the task non trivial + without a considerable amount of refactoring. +*) + +(* Interpreting a possibly delayed proof *) +let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option = + let stack = st.Vernacstate.lemmas in + let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in + let () = match pe with + | Admitted -> + Lemmas.save_lemma_admitted_delayed ~proof ~info + | Proved (_,idopt) -> + Lemmas.save_lemma_proved_delayed ~proof ~info ~idopt in + stack + +let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } = + let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in + List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) + control + (fun ~st -> interp_qed_delayed ~proof ~info ~st pe) + ~st + +(* General interp with management of state *) +let () = let open Goptions in + declare_int_option + { optdepr = false; + optname = "the default timeout"; + optkey = ["Default";"Timeout"]; + optread = (fun () -> !default_timeout); + optwrite = ((:=) default_timeout) } + +(* Be careful with the cache here in case of an exception. *) +let interp_gen ~verbosely ~st ~interp_fn cmd = + Vernacstate.unfreeze_interp_state st; + try vernac_timeout (fun st -> + let v_mod = if verbosely then Flags.verbosely else Flags.silently in + let ontop = v_mod (interp_fn ~st) cmd in + Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"]; + Vernacstate.freeze_interp_state ~marshallable:false + ) st + with exn -> + let exn = CErrors.push exn in + let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in + Vernacstate.invalidate_cache (); + Util.iraise exn + +(* Regular interp *) +let interp ?(verbosely=true) ~st cmd = + interp_gen ~verbosely ~st ~interp_fn:interp_control cmd + +let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t = + interp_gen ~verbosely:false ~st + ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli new file mode 100644 index 0000000000..16849686da --- /dev/null +++ b/vernac/vernacinterp.mli @@ -0,0 +1,33 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** The main interpretation function of vernacular expressions *) +val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t + +(** Execute a Qed but with a proof_object which may contain a delayed + proof and won't be forced *) +val interp_qed_delayed_proof + : proof:Proof_global.proof_object + -> info:Lemmas.Info.t + -> st:Vernacstate.t + -> control:Vernacexpr.control_flag list + -> Vernacexpr.proof_end CAst.t + -> Vernacstate.t + +(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *) +val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit + +(** Flag set when the test-suite is called. Its only effect to display + verbose information for [Fail] *) +val test_mode : bool ref + +(** Default proof mode set by `start_proof` *) +val get_default_proof_mode : unit -> Pvernac.proof_mode +val proof_mode_opt_name : string list |