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

8 files changed, 104 insertions, 226 deletions

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    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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$ *)
-
-open Term
-open Ptype
-
-(* Programmes impératifs *)
-
-type termination = RecArg of int
-                 | Wf     of Coqast.t * Coqast.t
-
-type variable = Names.identifier
-
-type pattern =
-    PatVar       of Names.identifier
-  | PatConstruct of Names.identifier * ((Names.section_path * int) * int)
-  | PatAlias     of pattern * Names.identifier
-  | PatPair      of pattern * pattern
-  | PatApp       of pattern list
-  
-type epattern =
-    ExnConstant of Names.identifier
-  | ExnBind     of Names.identifier * Names.identifier
-
-type ('a,'b) block_st =
-    Label     of string
-  | Assert    of 'b assertion
-  | Statement of 'a
-
-type ('a,'b) block = ('a,'b) block_st list
-
-(* type of programs with assertions of type 'b and info of type 'a *)
-
-type ('a,'b) t =
-  { desc : ('a,'b) t_desc ;
-    pre  : 'b precondition list ;
-    post : 'b postcondition option ;
-    loc  : Coqast.loc ;
-    info : 'a }
-
-and ('a,'b) t_desc = 
-    Var    of variable
-  | Acc    of variable
-  | Aff    of variable * (('a,'b) t)
-  | TabAcc of bool * variable * (('a,'b) t)
-  | TabAff of bool * variable * (('a,'b) t) * (('a,'b) t)
-  | Seq    of (('a,'b) t,'b) block
-  | While  of (('a,'b) t)           (* test *)
-            * 'b assertion option   (* invariant *)
-	    * ('b * 'b)             (* variant *)
-	    * (('a,'b) t, 'b) block (* corps *)
-  | If     of (('a,'b) t)  * (('a,'b) t) * (('a,'b) t)
-  | Lam    of 'b ml_type_v binder list * ('a,'b) t
-  | App    of (('a,'b) t) * (('a,'b) arg) list
-  | SApp   of (('a,'b) t_desc) list * (('a,'b) t) list  (* for connectives *)
-  | LetRef of variable * (('a,'b) t) * (('a,'b) t)
-  | LetIn  of variable * (('a,'b) t) * (('a,'b) t)
-  | LetRec of variable                                 (* nom *)
-            * 'b ml_type_v binder list * 'b ml_type_v  (* types *)
-            * ('b * 'b)                                (* variant *)
-	    * ('a,'b) t                                (* corps *)
-  | PPoint of string * ('a,'b) t_desc
-  | Expression of constr
-
-  | Debug  of string * (('a,'b) t) 
-
-and ('a,'b) arg = 
-    Term   of (('a,'b) t) 
-  | Refarg of variable
-  | Type   of 'b ml_type_v
-
-type program = (unit, Coqast.t) t
-
-
-(* AST for intermediate constructions.
- *
- * We define an intermediate type between typed program (above)
- * and CIC terms (constr), because we need to perform some eta-reductions
- * (see prog_red.ml for details)
- *
- * But here types are already CIC terms (constr).
- *)
-
-type cc_type = constr
-
-type cc_bind_type =
-    CC_typed_binder of cc_type
-  | CC_untyped_binder
-
-type cc_binder = variable * cc_bind_type
-
-type cc_term =
-    CC_var   of variable
-  | CC_letin of bool                   (* dep. or not *)
-              * cc_type                (* type of result *)
-	      * cc_binder list
-	      * (cc_term * case_info)  (* the matched term and its ind. type *)
-	      * cc_term
-  | CC_lam   of cc_binder list * cc_term
-  | CC_app   of cc_term * cc_term list
-  | CC_tuple of bool                   (* dep. or not *)
-              * cc_type list * cc_term list
-  | CC_case  of cc_type                (* type of result *)
-              * (cc_term * case_info)  (* the test and its inductive type *)
-	      * cc_term list           (* branches *)
-  | CC_expr  of constr
-  | CC_hole  of cc_type
-
-
diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
index d674f7d101..5db3c87b67 100644
--- a/contrib/correctness/past.mli
+++ b/contrib/correctness/past.mli
@@ -10,30 +10,43 @@
 
 (* $Id$ *)
 
-(* Generated automatically by ocamlc -i *)
+(*s Abstract syntax of imperative programs. *)
+
+open Names
+open Ptype
+
+type termination = 
+  | RecArg of int 
+  | Wf of Coqast.t * Coqast.t
+
+type variable = identifier
 
-type termination = | RecArg of int | Wf of Coqast.t * Coqast.t
-type variable = Names.identifier
 type pattern =
-  | PatVar of Names.identifier
-  | PatConstruct of Names.identifier * ((Names.section_path * int) * int)
-  | PatAlias of pattern * Names.identifier
+  | PatVar of identifier
+  | PatConstruct of identifier * ((section_path * int) * int)
+  | PatAlias of pattern * identifier
   | PatPair of pattern * pattern
   | PatApp of pattern list
+
 type epattern =
-  | ExnConstant of Names.identifier
-  | ExnBind of Names.identifier * Names.identifier
+  | ExnConstant of identifier
+  | ExnBind of identifier * identifier
+
 type ('a, 'b) block_st =
   | Label of string
   | Assert of 'b Ptype.assertion
   | Statement of 'a
+
 type ('a, 'b) block = ('a, 'b) block_st list
-type ('a, 'b) t =
-  { desc: ('a, 'b) t_desc;
-    pre: 'b Ptype.precondition list;
-    post: 'b Ptype.postcondition option;
-    loc: Coqast.loc;
-    info: 'a }
+
+type ('a, 'b) t = { 
+  desc : ('a, 'b) t_desc;
+  pre  : 'b Ptype.precondition list;
+  post : 'b Ptype.postcondition option;
+  loc  : Coqast.loc;
+  info : 'a 
+}
+
 and ('a, 'b) t_desc =
   | Var of variable
   | Acc of variable
@@ -54,14 +67,24 @@ and ('a, 'b) t_desc =
   | PPoint of string * ('a, 'b) t_desc
   | Expression of Term.constr
   | Debug of string * ('a, 'b) t
+
 and ('a, 'b) arg =
   | Term of ('a, 'b) t
   | Refarg of variable
   | Type of 'b Ptype.ml_type_v
+
 type program = (unit, Coqast.t) t
+
+(*s Intermediate type for CC terms. *)
+
 type cc_type = Term.constr
-type cc_bind_type = | CC_typed_binder of cc_type | CC_untyped_binder
+
+type cc_bind_type = 
+  | CC_typed_binder of cc_type 
+  | CC_untyped_binder
+
 type cc_binder = variable * cc_bind_type
+
 type cc_term =
   | CC_var of variable
   | CC_letin of 
diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index 31a2bad386..8604968e20 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -116,6 +116,8 @@ let (inProg,outProg) =
                     open_function = (fun _ -> ());
 		    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    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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$ *)
-
-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
-
-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 | <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
+
+
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