diff options
Diffstat (limited to 'src/coq.mli')
| -rw-r--r-- | src/coq.mli | 232 |
1 files changed, 232 insertions, 0 deletions
diff --git a/src/coq.mli b/src/coq.mli new file mode 100644 index 0000000..9cf0db7 --- /dev/null +++ b/src/coq.mli @@ -0,0 +1,232 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Interface with Coq where we define some handlers for Coq's API, + and we import several definitions from Coq's standard library. + + This general purpose library could be reused by other plugins. + + Some salient points: + - we use Caml's module system to mimic Coq's one, and avoid cluttering + the namespace; + - we also provide several handlers for standard coq tactics, in + order to provide a unified setting (we replace functions that + modify the evar_map by functions that operate on the whole + goal, and repack the modified evar_map with it). + +*) + +(** {2 Getting Coq terms from the environment} *) + +val init_constant_constr : string list -> string -> Constr.t +val init_constant : string list -> string -> EConstr.constr + +(** {2 General purpose functions} *) + +type goal_sigma = Proof_type.goal Evd.sigma +val resolve_one_typeclass : Proof_type.goal Evd.sigma -> EConstr.types -> EConstr.constr * goal_sigma +val cps_resolve_one_typeclass: ?error:Pp.t -> EConstr.types -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic +val nf_evar : goal_sigma -> EConstr.constr -> EConstr.constr +val evar_unit :goal_sigma ->EConstr.constr -> EConstr.constr* goal_sigma +val evar_binary: goal_sigma -> EConstr.constr -> EConstr.constr* goal_sigma +val evar_relation: goal_sigma -> EConstr.constr -> EConstr.constr* goal_sigma +val cps_evar_relation : EConstr.constr -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic +(** [cps_mk_letin name v] binds the constr [v] using a letin tactic *) +val cps_mk_letin : string -> EConstr.constr -> ( EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic + +val retype : EConstr.constr -> Proof_type.tactic + +val decomp_term : Evd.evar_map -> EConstr.constr -> (EConstr.constr , EConstr.types, EConstr.ESorts.t, EConstr.EInstance.t) Constr.kind_of_term +val lapp : EConstr.constr lazy_t -> EConstr.constr array -> EConstr.constr + +(** {2 Bindings with Coq' Standard Library} *) + +(** Coq lists *) +module List: +sig + (** [of_list ty l] *) + val of_list:EConstr.constr ->EConstr.constr list ->EConstr.constr + + (** [type_of_list ty] *) + val type_of_list:EConstr.constr ->EConstr.constr +end + +(** Coq pairs *) +module Pair: +sig + val typ:EConstr.constr lazy_t + val pair:EConstr.constr lazy_t + val of_pair : EConstr.constr -> EConstr.constr -> EConstr.constr * EConstr.constr -> EConstr.constr +end + +module Bool : sig + val typ : EConstr.constr lazy_t + val of_bool : bool -> EConstr.constr +end + + +module Comparison : sig + val typ : EConstr.constr lazy_t + val eq : EConstr.constr lazy_t + val lt : EConstr.constr lazy_t + val gt : EConstr.constr lazy_t +end + +module Leibniz : sig + val eq_refl : EConstr.types -> EConstr.constr -> EConstr.constr +end + +module Option : sig + val typ : EConstr.constr lazy_t + val some : EConstr.constr -> EConstr.constr -> EConstr.constr + val none : EConstr.constr -> EConstr.constr + val of_option : EConstr.constr -> EConstr.constr option -> EConstr.constr +end + +(** Coq positive numbers (pos) *) +module Pos: +sig + val typ:EConstr.constr lazy_t + val of_int: int ->EConstr.constr +end + +(** Coq unary numbers (peano) *) +module Nat: +sig + val typ:EConstr.constr lazy_t + val of_int: int ->EConstr.constr +end + +(** Coq typeclasses *) +module Classes: +sig + val mk_morphism: EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr + val mk_equivalence: EConstr.constr -> EConstr.constr -> EConstr.constr + val mk_reflexive: EConstr.constr -> EConstr.constr -> EConstr.constr + val mk_transitive: EConstr.constr -> EConstr.constr -> EConstr.constr +end + +module Relation : sig + type t = {carrier : EConstr.constr; r : EConstr.constr;} + val make : EConstr.constr -> EConstr.constr -> t + val split : t -> EConstr.constr * EConstr.constr +end + +module Transitive : sig + type t = + { + carrier : EConstr.constr; + leq : EConstr.constr; + transitive : EConstr.constr; + } + val make : EConstr.constr -> EConstr.constr -> EConstr.constr -> t + val infer : goal_sigma -> EConstr.constr -> EConstr.constr -> t * goal_sigma + val from_relation : goal_sigma -> Relation.t -> t * goal_sigma + val cps_from_relation : Relation.t -> (t -> Proof_type.tactic) -> Proof_type.tactic + val to_relation : t -> Relation.t +end + +module Equivalence : sig + type t = + { + carrier : EConstr.constr; + eq : EConstr.constr; + equivalence : EConstr.constr; + } + val make : EConstr.constr -> EConstr.constr -> EConstr.constr -> t + val infer : goal_sigma -> EConstr.constr -> EConstr.constr -> t * goal_sigma + val from_relation : goal_sigma -> Relation.t -> t * goal_sigma + val cps_from_relation : Relation.t -> (t -> Proof_type.tactic) -> Proof_type.tactic + val to_relation : t -> Relation.t + val split : t -> EConstr.constr * EConstr.constr * EConstr.constr +end + +(** [match_as_equation ?context goal c] try to decompose c as a + relation applied to two terms. An optionnal rel-context can be + provided to ensure that the term remains typable *) +val match_as_equation : ?context:EConstr.rel_context -> goal_sigma -> EConstr.constr -> (EConstr.constr * EConstr.constr * Relation.t) option + +(** {2 Some tacticials} *) + +(** time the execution of a tactic *) +val tclTIME : string -> Proof_type.tactic -> Proof_type.tactic + +(** emit debug messages to see which tactics are failing *) +val tclDEBUG : string -> Proof_type.tactic -> Proof_type.tactic + +(** print the current goal *) +val tclPRINT : Proof_type.tactic -> Proof_type.tactic + + +(** {2 Error related mechanisms} *) + +val anomaly : string -> 'a +val user_error : Pp.t -> 'a +val warning : string -> unit + + +(** {2 Rewriting tactics used in aac_rewrite} *) + +module Rewrite : sig + +(** The rewriting tactics used in aac_rewrite, build as handlers of the usual [setoid_rewrite]*) + + +(** {2 Datatypes} *) + +(** We keep some informations about the hypothesis, with an (informal) + invariant: + - [typeof hyp = typ] + - [typ = forall context, body] + - [body = rel left right] + +*) +type hypinfo = + { + hyp : EConstr.constr; (** the actual constr corresponding to the hypothese *) + hyptype : EConstr.constr; (** the type of the hypothesis *) + context : EConstr.rel_context; (** the quantifications of the hypothese *) + body : EConstr.constr; (** the body of the hypothese*) + rel : Relation.t; (** the relation *) + left : EConstr.constr; (** left hand side *) + right : EConstr.constr; (** right hand side *) + l2r : bool; (** rewriting from left to right *) + } + +(** [get_hypinfo H l2r ?check_type k] analyse the hypothesis H, and + build the related hypinfo, in CPS style. Moreover, an optionnal + function can be provided to check the type of every free + variable of the body of the hypothesis. *) +val get_hypinfo :EConstr.constr -> l2r:bool -> ?check_type:(EConstr.types -> bool) -> (hypinfo -> Proof_type.tactic) -> Proof_type.tactic + +(** {2 Rewriting with bindings} + + The problem : Given a term to rewrite of type [H :forall xn ... x1, + t], we have to instanciate the subset of [xi] of type + [carrier]. [subst : (int * constr)] is the mapping the De Bruijn + indices in [t] to the [constrs]. We need to handle the rest of the + indexes. Two ways : + + - either using fresh evars and rewriting [H tn ?1 tn-2 ?2 ] + - either building a term like [fun 1 2 => H tn 1 tn-2 2] + + Both these terms have the same type. +*) + +(** build the constr to rewrite, in CPS style, with lambda abstractions *) +val build : hypinfo -> (int * EConstr.constr) list -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic + +(** build the constr to rewrite, in CPS style, with evars *) +val build_with_evar : hypinfo -> (int * EConstr.constr) list -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic + +(** [rewrite ?abort hypinfo subst] builds the rewriting tactic + associated with the given [subst] and [hypinfo], and feeds it to + the given continuation. If [abort] is set to [true], we build + [tclIDTAC] instead. *) +val rewrite : ?abort:bool -> hypinfo -> (int * EConstr.constr) list -> (Proof_type.tactic -> Proof_type.tactic) -> Proof_type.tactic +end |