diff options
author | 2001-04-04 07:45:34 +0000 | |
---|---|---|
committer | 2001-04-04 07:45:34 +0000 | |
commit | 1dd2c8e1a03078583887dd2dfb20273fc5c11c1c (patch) | |
tree | 6f7a575476680e75ce27221809ebb413e5d038ee /contrib/correctness/ptype.mli | |
parent | 231d0032cc337aa8116caa16635d10d2aa91fffb (diff) |
deux fichiers (past et ptype) uniquement sous forme de .mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1527 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/ptype.mli')
-rw-r--r-- | contrib/correctness/ptype.mli | 74 |
1 files changed, 57 insertions, 17 deletions
diff --git a/contrib/correctness/ptype.mli b/contrib/correctness/ptype.mli index bbb517a20..3f511ddf2 100644 --- a/contrib/correctness/ptype.mli +++ b/contrib/correctness/ptype.mli @@ -10,24 +10,64 @@ (* $Id$ *) -(* Generated automatically by ocamlc -i *) +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 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 = Term.constr assertion -type 'a binder_type = | BindType of 'a | BindSet | Untyped type 'a binder = Names.identifier * 'a binder_type -type variant = Term.constr * Term.constr * Term.constr + +(* 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 - | Arrow of 'a ml_type_v binder list * 'a ml_type_c - | TypePure of 'a + 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 -type type_v = Term.constr ml_type_v -type type_c = Term.constr ml_type_c -val is_mutable : 'a ml_type_v -> bool -val is_pure : 'a ml_type_v -> bool + (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 + + |