diff options
Diffstat (limited to 'contrib/correctness/ptype.mli')
-rw-r--r-- | contrib/correctness/ptype.mli | 73 |
1 files changed, 0 insertions, 73 deletions
diff --git a/contrib/correctness/ptype.mli b/contrib/correctness/ptype.mli deleted file mode 100644 index be181bcc..00000000 --- a/contrib/correctness/ptype.mli +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* 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 5920 2004-07-16 20:01:26Z herbelin $ *) - -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 - - |