From 1dd2c8e1a03078583887dd2dfb20273fc5c11c1c Mon Sep 17 00:00:00 2001 From: filliatr Date: Wed, 4 Apr 2001 07:45:34 +0000 Subject: 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 --- contrib/correctness/Correctness.v | 2 +- contrib/correctness/past.ml | 118 -------------------------------------- contrib/correctness/past.mli | 53 ++++++++++++----- contrib/correctness/penv.ml | 2 + contrib/correctness/ptype.ml | 75 ------------------------ contrib/correctness/ptype.mli | 74 ++++++++++++++++++------ contrib/correctness/putil.ml | 3 + contrib/correctness/putil.mli | 3 + 8 files changed, 104 insertions(+), 226 deletions(-) delete mode 100644 contrib/correctness/past.ml delete mode 100644 contrib/correctness/ptype.ml diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v index 7dc283f7a6..bc12ec7552 100644 --- a/contrib/correctness/Correctness.v +++ b/contrib/correctness/Correctness.v @@ -23,7 +23,7 @@ Require Export ProgWf. Require Export Arrays. Declare ML Module - "pmisc" "peffect" "prename" "ptype" "past" + "pmisc" "peffect" "prename" "perror" "penv" "putil" "pdb" "pcic" "pmonad" "pcicenv" "pred" "ptyping" "pwp" "pmlize" "ptactic" "psyntax". diff --git a/contrib/correctness/past.ml b/contrib/correctness/past.ml deleted file mode 100644 index 612097612a..0000000000 --- a/contrib/correctness/past.ml +++ /dev/null @@ -1,118 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ()); export_function = (fun x -> Some x) }) +let is_mutable = function Ref _ | Array _ -> true | _ -> false + let add_global id v p = try let _ = Env.find id !env in diff --git a/contrib/correctness/ptype.ml b/contrib/correctness/ptype.ml deleted file mode 100644 index a2caa69c46..0000000000 --- a/contrib/correctness/ptype.ml +++ /dev/null @@ -1,75 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - * - * 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 - -let is_mutable = function Ref _ | Array _ -> true | _ -> false -let is_pure = function TypePure _ -> true | _ -> false - diff --git a/contrib/correctness/ptype.mli b/contrib/correctness/ptype.mli index bbb517a206..3f511ddf2d 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 | + * + * 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 + + diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml index 7fd8b7b4ad..2f86d355e2 100644 --- a/contrib/correctness/putil.ml +++ b/contrib/correctness/putil.ml @@ -21,6 +21,9 @@ open Past open Penv open Prename +let is_mutable = function Ref _ | Array _ -> true | _ -> false +let is_pure = function TypePure _ -> true | _ -> false + let named_app f x = { a_name = x.a_name; a_value = (f x.a_value) } let pre_app f x = diff --git a/contrib/correctness/putil.mli b/contrib/correctness/putil.mli index ca139f9e12..fa55960340 100644 --- a/contrib/correctness/putil.mli +++ b/contrib/correctness/putil.mli @@ -18,6 +18,9 @@ open Ptype open Past open Penv +val is_mutable : 'a ml_type_v -> bool +val is_pure : 'a ml_type_v -> bool + val named_app : ('a -> 'b) -> 'a assertion -> 'b assertion val pre_app : ('a -> 'b) -> 'a precondition -> 'b precondition val post_app : ('a -> 'b) -> 'a postcondition -> 'b postcondition -- cgit v1.2.3