From 1aa8b6f6a876af22f538c869f022bc4ca5986b40 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 29 Nov 2010 23:30:48 +0100
Subject: Imported Upstream version 0.1-r13244

---
 coq.mli | 117 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 117 insertions(+)
 create mode 100644 coq.mli

(limited to 'coq.mli')

diff --git a/coq.mli b/coq.mli
new file mode 100644
index 0000000..588a922
--- /dev/null
+++ b/coq.mli
@@ -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
+
+
-- 
cgit v1.2.3