diff options
Diffstat (limited to 'coq.mli')
| -rw-r--r-- | coq.mli | 117 |
1 files changed, 117 insertions, 0 deletions
@@ -0,0 +1,117 @@ +(***************************************************************************) +(* 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 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 : string list -> string -> Term.constr + +(** {2 General purpose functions} *) + +type goal_sigma = Proof_type.goal Tacmach.sigma +val goal_update : goal_sigma -> Evd.evar_map -> goal_sigma +val resolve_one_typeclass : Proof_type.goal Tacmach.sigma -> Term.types -> Term.constr * goal_sigma +val nf_evar : goal_sigma -> Term.constr -> Term.constr +val evar_unit :goal_sigma ->Term.constr*Term.constr-> Term.constr* goal_sigma +val evar_binary: goal_sigma -> Term.constr*Term.constr -> Term.constr* goal_sigma + + +(** [mk_letin name v] binds the constr [v] using a letin tactic *) +val mk_letin : string ->Term.constr ->Term.constr * Proof_type.tactic + +(** [mk_letin' name v] is a drop-in replacement for [mk_letin' name v] + that does not make a binding (useful to test whether using lets is + efficient) *) +val mk_letin' : string ->Term.constr ->Term.constr * Proof_type.tactic + +(* decomp_term : constr -> (constr, types) kind_of_term *) +val decomp_term : Term.constr -> (Term.constr , Term.types) Term.kind_of_term + + +(** {2 Bindings with Coq' Standard Library} *) + +(** Coq lists *) +module List: +sig + (** [of_list ty l] *) + val of_list:Term.constr ->Term.constr list ->Term.constr + + (** [type_of_list ty] *) + val type_of_list:Term.constr ->Term.constr +end + +(** Coq pairs *) +module Pair: +sig + val typ:Term.constr lazy_t + val pair:Term.constr lazy_t +end + +(** Coq positive numbers (pos) *) +module Pos: +sig + val typ:Term.constr lazy_t + val of_int: int ->Term.constr +end + +(** Coq unary numbers (peano) *) +module Nat: +sig + val typ:Term.constr lazy_t + val of_int: int ->Term.constr +end + + +(** Coq typeclasses *) +module Classes: +sig + val mk_morphism: Term.constr -> Term.constr -> Term.constr -> Term.constr + val mk_equivalence: Term.constr -> Term.constr -> Term.constr +end + +(** Both in OCaml and Coq, we represent finite multisets using + weighted lists ([('a*int) list]), see {!Matcher.mset}. + + [mk_mset ty l] constructs a Coq multiset from an OCaml multiset + [l] of Coq terms of type [ty] *) + +val mk_mset:Term.constr -> (Term.constr * int) list ->Term.constr + +(** pairs [(x,r)] such that [r: Relation x] *) +type reltype = Term.constr * Term.constr + +(** triples [((x,r),e)] such that [e : @Equivalence x r]*) +type eqtype = reltype * Term.constr + + +(** {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 + + |