diff options
Diffstat (limited to 'src/versions/standard/structures.ml')
| -rw-r--r-- | src/versions/standard/structures.ml | 67 |
1 files changed, 31 insertions, 36 deletions
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index d7e7f96..d069dde 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -10,9 +10,6 @@ (**************************************************************************) -open Entries - - (* Constr generation and manipulation *) type id = Names.variable let mkId = Names.Id.of_string @@ -41,55 +38,48 @@ let destRel = Constr.destRel let lift = Vars.lift let mkApp = Constr.mkApp let decompose_app = Constr.decompose_app -let mkLambda = Constr.mkLambda -let mkProd = Constr.mkProd -let mkLetIn = Constr.mkLetIn +let mkLambda (n, t, c) = Constr.mkLambda (Context.make_annot n Sorts.Relevant, t, c) +let mkProd (n, t, c) = Constr.mkProd (Context.make_annot n Sorts.Relevant, t, c) +let mkLetIn (n, c1, t, c2) = Constr.mkLetIn (Context.make_annot n Sorts.Relevant, c1, t, c2) +let mkArrow a b = Term.mkArrow a Sorts.Relevant b let pr_constr_env env = Printer.pr_constr_env env Evd.empty let pr_constr = pr_constr_env Environ.empty_env -let mkUConst : Constr.t -> Safe_typing.private_constants Entries.definition_entry = fun c -> +let mkUConst : Constr.t -> Evd.side_effects Declare.proof_entry = fun c -> let env = Global.env () in let evd = Evd.from_env env in let evd, ty = Typing.type_of env evd (EConstr.of_constr c) in - { Entries.const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), - Safe_typing.empty_private_constants); - const_entry_secctx = None; - const_entry_feedback = None; - const_entry_type = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Constr.t *) - const_entry_universes = Evd.const_univ_entry ~poly:false evd; - const_entry_opaque = false; - const_entry_inline_code = false } + Declare.definition_entry + ~opaque:false + ~inline:false + ~types:(EConstr.Unsafe.to_constr ty) (* Cannot contain evars since it comes from a Constr.t *) + ~univs:(Evd.univ_entry ~poly:false evd) + c let mkTConst c noc ty = let env = Global.env () in let evd = Evd.from_env env in let evd, _ = Typing.type_of env evd (EConstr.of_constr noc) in - { const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), - Safe_typing.empty_private_constants); - const_entry_secctx = None; - const_entry_feedback = None; - const_entry_type = Some ty; - const_entry_universes = Evd.const_univ_entry ~poly:false evd; - const_entry_opaque = false; - const_entry_inline_code = false } + Declare.definition_entry + ~opaque:false + ~inline:false + ~types:ty + ~univs:(Evd.univ_entry ~poly:false evd) + c (* TODO : Set -> Type *) let declare_new_type t = - let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_const_entry Univ.ContextSet.empty) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in + let _ = ComAssumption.declare_variable false ~kind:Decls.Definitional Constr.mkSet [] Glob_term.Explicit (CAst.make t) in Constr.mkVar t let declare_new_variable v constr_t = - let env = Global.env () in - let evd = Evd.from_env env in - let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in - let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.const_univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in + let _ = ComAssumption.declare_variable false ~kind:Decls.Definitional constr_t [] Glob_term.Explicit (CAst.make v) in Constr.mkVar v let declare_constant n c = - Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition) - + Declare.declare_constant ~name:n ~kind:(Decls.IsDefinition Decls.Definition) (Declare.DefinitionEntry c) type cast_kind = Constr.cast_kind @@ -103,8 +93,11 @@ let econstr_of_constr = EConstr.of_constr (* Modules *) -let gen_constant_in_modules s m n = UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n +let gen_constant_in_modules s m n = + (* UnivGen.constr_of_monomorphic_global will crash on universe polymorphic constants *) + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules s m n let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) +let init_modules = Coqlib.init_modules (* Int63 *) @@ -166,13 +159,14 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = (* Micromega *) module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Mutils_full +module Micromega_plugin_Mutils = Micromega_plugin.Mutils module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega_full +module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega +module Micromega_plugin_Persistent_cache = Micromega_plugin.Persistent_cache let micromega_coq_proofTerm = (* Cannot contain evars *) - lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin_Coq_micromega.M.coq_proofTerm))) + lazy (gen_constant_in_modules "ZMicromega" [["Coq"; "micromega";"ZMicromega"]] "ZArithProof") let micromega_dump_proof_term p = (* Cannot contain evars *) @@ -188,7 +182,7 @@ let assert_before n c = Tactics.assert_before n (EConstr.of_constr c) let vm_cast_no_check c = Tactics.vm_cast_no_check (EConstr.of_constr c) let mk_tactic tac = - Proofview.Goal.nf_enter (fun gl -> + Proofview.Goal.enter (fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let t = Proofview.Goal.concl gl in @@ -222,7 +216,8 @@ let constrextern_extern_constr c = Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c) let get_rel_dec_name = function - | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) -> n + | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) -> + Context.binder_name n let retyping_get_type_of env sigma c = (* Cannot contain evars since it comes from a Constr.t *) |