diff options
Diffstat (limited to 'src/versions/standard/structures.mli')
-rw-r--r-- | src/versions/standard/structures.mli | 143 |
1 files changed, 82 insertions, 61 deletions
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli index 3d17203..3d6f6b2 100644 --- a/src/versions/standard/structures.mli +++ b/src/versions/standard/structures.mli @@ -10,74 +10,80 @@ (**************************************************************************) -(* Constr generation and manipulation *) (* WARNING: currently, we map all the econstr into constr: we suppose that the goal does not contain existencial variables *) -val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr -val gen_constant : string list list -> string -> Term.constr lazy_t + +(* Constr generation and manipulation *) +type id = Names.variable +val mkId : string -> id + +type name +val name_of_id : id -> name +val mkName : string -> name +val string_of_name : name -> string + +type constr = Constr.t +type types = constr +val eq_constr : constr -> constr -> bool +val hash_constr : constr -> int +val mkProp : types +val mkConst : Names.Constant.t -> constr +val mkVar : id -> constr +val mkRel : int -> constr +val isRel : constr -> bool +val destRel : constr -> int +val lift : int -> constr -> constr +val mkApp : constr * constr array -> constr +val decompose_app : constr -> constr * constr list +val mkLambda : name * types * constr -> constr +val mkProd : name * types * types -> types +val mkLetIn : name * constr * types * constr -> 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 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 + +type cast_kind +val vmcast : cast_kind +val mkCast : constr * cast_kind * constr -> constr + + +(* EConstr *) +type econstr = EConstr.t +val econstr_of_constr : constr -> econstr + + +(* Modules *) +val gen_constant : string list list -> string -> constr lazy_t + (* Int63 *) val int63_modules : string list list -val int31_module : string list list -val cD0 : Term.constr lazy_t -val cD1 : Term.constr lazy_t -val cI31 : Term.constr lazy_t -val mkInt : int -> Term.constr -val cint : Term.constr lazy_t +val mkInt : int -> constr +val cint : constr lazy_t + (* PArray *) val parray_modules : string list list -val cmake : Term.constr lazy_t -val cset : Term.constr lazy_t val max_array_size : int -val mkArray : Term.types * Term.constr array -> Term.constr +val mkArray : types * constr array -> constr + (* Traces *) val mkTrace : - ('a -> Term.constr) -> + ('a -> constr) -> ('a -> 'a) -> 'b -> - Term.constr Lazy.t -> - Term.constr Lazy.t -> - Term.constr Lazy.t -> - Term.constr Lazy.t -> - int -> Term.constr -> Term.constr -> 'a ref -> Term.constr - -(* Differences between the two versions of Coq *) -val mkUConst : - Term.constr -> Safe_typing.private_constants Entries.definition_entry -val mkTConst : - Term.constr -> - Term.constr -> - Term.types -> Safe_typing.private_constants Entries.definition_entry -val error : string -> 'a -val coqtype : Term.types Future.computation -val declare_new_type : Names.variable -> Term.constr -val declare_new_variable : Names.variable -> Term.constr -> Term.constr -val extern_constr : Term.constr -> Constrexpr.constr_expr -val vernacentries_interp : Constrexpr.constr_expr -> unit -val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds -val lift : int -> Constr.constr -> Constr.constr -val destruct_rel_decl : Context.Rel.Declaration.t -> Names.Name.t * Constr.t -val interp_constr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Term.constr -val tclTHEN : - unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic -val tclTHENLAST : - unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic -val assert_before : Names.Name.t -> Term.types -> unit Proofview.tactic - -val vm_conv : Reduction.conv_pb -> Term.types Reduction.kernel_conversion_function -val vm_cast_no_check : Term.constr -> unit Proofview.tactic -val cbv_vm : Environ.env -> Term.constr -> Term.types -> Term.constr - -val mk_tactic : - (Environ.env -> Evd.evar_map -> Term.constr -> unit Proofview.tactic) -> - unit Proofview.tactic -val set_evars_tac : Term.constr -> unit Proofview.tactic -val ppconstr_lsimpleconstr : Ppconstr.precedence -val constrextern_extern_constr : Term.constr -> Constrexpr.constr_expr -val get_rel_dec_name : Context.Rel.Declaration.t -> Names.Name.t -val retyping_get_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr + constr Lazy.t -> + constr Lazy.t -> + constr Lazy.t -> + constr Lazy.t -> + int -> constr -> constr -> 'a ref -> constr (* Micromega *) @@ -86,15 +92,30 @@ module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega module Micromega_plugin_Micromega = Micromega_plugin.Micromega module Micromega_plugin_Mutils = Micromega_plugin.Mutils -val micromega_coq_proofTerm : Term.constr lazy_t -val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> Term.constr +val micromega_coq_proofTerm : constr lazy_t +val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr -(* Types in the Coq source code *) +(* Tactics *) type tactic = unit Proofview.tactic -type names_id = Names.Id.t +val tclTHEN : tactic -> tactic -> tactic +val tclTHENLAST : tactic -> tactic -> tactic +val assert_before : name -> types -> tactic +val vm_cast_no_check : constr -> tactic +val mk_tactic : (Environ.env -> Evd.evar_map -> constr -> tactic) -> tactic +val set_evars_tac : constr -> tactic + + +(* Other differences between the two versions of Coq *) type constr_expr = Constrexpr.constr_expr +val error : string -> 'a +val extern_constr : constr -> constr_expr +val destruct_rel_decl : Context.Rel.Declaration.t -> name * constr +val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr +val ppconstr_lsimpleconstr : Notation_term.tolerability +val constrextern_extern_constr : constr -> constr_expr +val get_rel_dec_name : Context.Rel.Declaration.t -> name +val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr -(* EConstr *) -type econstr = EConstr.t -val econstr_of_constr : Term.constr -> econstr +val vm_conv : Reduction.conv_pb -> types Reduction.kernel_conversion_function +val cbv_vm : Environ.env -> constr -> types -> constr |