diff options
Diffstat (limited to 'src/trace')
-rw-r--r-- | src/trace/coqInterface.ml | 47 | ||||
-rw-r--r-- | src/trace/coqInterface.mli | 9 | ||||
-rw-r--r-- | src/trace/smtCommands.ml | 2 |
3 files changed, 22 insertions, 36 deletions
diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml index 9b2c72c..f33f091 100644 --- a/src/trace/coqInterface.ml +++ b/src/trace/coqInterface.ml @@ -10,9 +10,6 @@ (**************************************************************************) -open Entries - - (* Constr generation and manipulation *) type id = Names.variable let mkId = Names.Id.of_string @@ -50,47 +47,39 @@ 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.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.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 ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_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 ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.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 @@ -163,8 +152,6 @@ type constr_expr = Constrexpr.constr_expr let error s = CErrors.user_err (Pp.str s) let warning n s = CWarnings.create ~name:n ~category:"SMTCoq plugin" Pp.str s -let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c) - let destruct_rel_decl r = Context.Rel.Declaration.get_name r, Context.Rel.Declaration.get_type r @@ -175,7 +162,7 @@ let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr let constrextern_extern_constr c = let env = Global.env () in - Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c) + Constrextern.extern_constr ~inctx: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, _, _) -> diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli index 0536ef1..af34d87 100644 --- a/src/trace/coqInterface.mli +++ b/src/trace/coqInterface.mli @@ -43,11 +43,11 @@ val mkArrow : types -> types -> constr val pr_constr_env : Environ.env -> constr -> Pp.t val pr_constr : constr -> Pp.t -val mkUConst : constr -> Safe_typing.private_constants Entries.definition_entry -val mkTConst : constr -> constr -> types -> Safe_typing.private_constants Entries.definition_entry +val mkUConst : constr -> Evd.side_effects Declare.proof_entry +val mkTConst : constr -> constr -> types -> Evd.side_effects Declare.proof_entry val declare_new_type : id -> types val declare_new_variable : id -> types -> constr -val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t +val declare_constant : id -> Evd.side_effects Declare.proof_entry -> Names.Constant.t type cast_kind val vmcast : cast_kind @@ -99,10 +99,9 @@ val set_evars_tac : constr -> tactic type constr_expr = Constrexpr.constr_expr val error : string -> 'a val warning : string -> string -> unit -val extern_constr : constr -> constr_expr val destruct_rel_decl : (constr, types) Context.Rel.Declaration.pt -> name * types val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr -val ppconstr_lsimpleconstr : Notation_gram.tolerability +val ppconstr_lsimpleconstr : Constrexpr.entry_relative_level val constrextern_extern_constr : constr -> constr_expr val get_rel_dec_name : (constr, types) Context.Rel.Declaration.pt -> name val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 2108da4..27ba80c 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -681,7 +681,7 @@ let gen_rel_name = let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma = let warn () = - CoqInterface.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (CoqInterface.extern_constr clemma)))); + CoqInterface.warning "Lemma" ("Discarding the following lemma (unsupported): "^(SmtMisc.string_coq_constr clemma)); None in |