1 files changed, 73 insertions, 0 deletions
diff --git a/contrib/correctness/ptype.mli b/contrib/correctness/ptype.mli
new file mode 100644
index 00000000..f2dc85e3
--- /dev/null
+++ b/contrib/correctness/ptype.mli
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
+
+(* $Id: ptype.mli,v 1.2.16.1 2004/07/16 19:30:06 herbelin Exp $ *)
+
+open Term
+
+(* Types des valeurs (V) et des calculs (C).
+ *
+ * On a C = r:V,E,P,Q 
+ *
+ *   et V = (x1:V1)...(xn:Vn)C | V ref | V array | <type pur>
+ *
+ * INVARIANT: l'effet E contient toutes les variables apparaissant dans
+ *            le programme ET les annotations P et Q
+ *            Si E = { x1,...,xn | y1,...,ym }, les variables x sont les
+ *            variables en lecture seule et y1 les variables modifiées
+ *            les xi sont libres dans P et Q, et les yi,result liées dans Q
+ *            i.e.  P = p(x)
+ *               et Q = [y1]...[yn][res]q(x,y,res)
+ *)
+
+(* pre and post conditions *)
+
+type 'a precondition = { p_assert : bool; p_name : Names.name; p_value : 'a }
+
+type 'a assertion  = { a_name : Names.name; a_value : 'a }
+
+type 'a postcondition = 'a assertion
+
+type predicate = constr assertion
+
+(* binders *)
+
+type 'a binder_type =
+    BindType  of 'a
+  | BindSet
+  | Untyped
+
+type 'a binder = Names.identifier * 'a binder_type
+
+(* variant *)
+
+type variant = constr * constr * constr (* phi, R, A *)
+
+(* types des valeurs *)
+
+type 'a ml_type_v =
+    Ref       of 'a ml_type_v
+  | Array     of 'a * 'a ml_type_v   (* size x type *)
+  | Arrow     of 'a ml_type_v binder list * 'a ml_type_c
+
+  | TypePure  of 'a
+
+(* et type des calculs *)
+
+and 'a ml_type_c =
+    (Names.identifier * 'a ml_type_v) 
+  * Peffect.t
+  * ('a precondition list) * ('a postcondition option)
+
+(* at beginning they contain Coq AST but they become constr after typing *)
+type type_v = constr ml_type_v
+type type_c = constr ml_type_c
+
+