correction d'un bug de Correctness (pour Y Bertot)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1812 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 94 insertions, 52 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 3013c2c9b5..ecc17253a1 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -32,7 +32,7 @@ let make_hole c = mkCast (isevar, c)
 let tuple_exists id =
   try let _ = Nametab.sp_of_id CCI id in true with Not_found -> false
 
-let ast_set = Ast.ope ("PROP", [ Ast.ide "Pos" ])
+let ast_set = Ast.ope ("SET", [])
 
 let tuple_n n =
   let name = "tuple_" ^ string_of_int n in
@@ -88,6 +88,20 @@ let sig_n n =
 	    mind_entry_arity = mkSet;
 	    mind_entry_consnames = [ cname ];
 	    mind_entry_lc = [ lc ] } ] }
+
+(*s On the fly generation of needed (possibly dependent) tuples. *)
+
+let check_product_n n =
+  if n > 2 then
+    let s = Printf.sprintf "tuple_%d" n in
+    if not (tuple_exists (id_of_string s)) then tuple_n n
+
+let check_dep_product_n n =
+  if n > 1 then
+    let s = Printf.sprintf "sig_%d" n in
+    if not (tuple_exists (id_of_string s)) then ignore (sig_n n)
+
+(*s Constructors for the tuples. *)
 	
 let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "prod",0),1)
 let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "sig",0),1)
diff --git a/contrib/correctness/pcic.mli b/contrib/correctness/pcic.mli
index f0b629071d..e759ff6b58 100644
--- a/contrib/correctness/pcic.mli
+++ b/contrib/correctness/pcic.mli
@@ -13,6 +13,10 @@
 open Past
 open Rawterm
 
+(* On-the-fly generation of needed (possibly dependent) tuples. *)
+
+val check_product_n : int -> unit
+val check_dep_product_n : int -> unit
 
 (* transforms intermediate functional programs into (raw) CIC terms *)
 
diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml
index 06090fb07e..7ad6a79dba 100644
--- a/contrib/correctness/pdb.ml
+++ b/contrib/correctness/pdb.ml
@@ -33,32 +33,51 @@ let lookup_var ids locop id =
 
 let check_ref idl loc id =
   if (not (List.mem id idl)) & (not (Penv.is_global id)) then
-    Perror.unbound_reference id (Some loc)
-
-(* db types  : just do nothing for the moment ! *)
-
-let rec db_type_v ids = function
-  | Ref v -> Ref (db_type_v ids v)
-  | Array (c,v) -> Array (c,db_type_v ids v)
-  | Arrow (bl,c) -> Arrow (List.map (db_binder ids) bl, db_type_c ids c)
-  | TypePure _ as v -> v
-and db_type_c ids ((id,v),e,p,q) =
-  (id,db_type_v ids v), e, p, q
-  (* TODO: db_condition ? *)
-and db_binder ids = function
-    (n, BindType v) -> (n, BindType (db_type_v ids v))
-  | b -> b
+    Perror.unbound_reference id loc
+
+(* db types : only check the references for the moment *)
+
+let rec check_type_v refs = function
+  | Ref v -> 
+      check_type_v refs v
+  | Array (c,v) -> 
+      check_type_v refs v
+  | Arrow (bl,c) -> 
+      check_binder refs c bl
+  | TypePure _ -> 
+      ()
+
+and check_type_c refs ((_,v),e,_,_) =
+  check_type_v refs v;
+  List.iter (check_ref refs None) (Peffect.get_reads e);
+  List.iter (check_ref refs None) (Peffect.get_writes e)
+  (* TODO: check_condition on p and q *)
+
+and check_binder refs c = function
+  | [] -> 
+      check_type_c refs c
+  | (id, BindType (Ref _ | Array _ as v)) :: bl -> 
+      check_type_v refs v;
+      check_binder (id :: refs) c bl
+  | (_, BindType v) :: bl ->
+      check_type_v refs v;
+      check_binder refs c bl
+  | _ :: bl -> 
+      check_binder refs c bl
 
 (* db binders *)
 
 let rec db_binders ((tids,pids,refs) as idl) = function
-    [] -> idl, []
-  | (id, BindType (Ref _ | Array _ as v)) :: rem ->
+  | [] -> 
+      idl, []
+  | (id, BindType (Ref _ | Array _ as v)) as b :: rem ->
+      check_type_v refs v;
       let idl',rem' = db_binders (tids,pids,id::refs) rem in
-      idl', (id, BindType (db_type_v tids v)) :: rem'
-  | (id, BindType v) :: rem ->
+      idl', b :: rem'
+  | (id, BindType v) as b :: rem ->
+      check_type_v refs v;
       let idl',rem' = db_binders (tids,id::pids,refs) rem in
-      idl', (id, BindType (db_type_v tids v)) :: rem'
+      idl', b :: rem'
   | ((id, BindSet) as t) :: rem ->
       let idl',rem' = db_binders (id::tids,pids,refs) rem in
       idl', t :: rem'
@@ -88,7 +107,7 @@ let rec db_pattern = function
 	     let ids',p' = db_pattern p in ids'@ids,p'::pl) pl ([],[]) in
   	ids,PatApp pl'
   | PatConstruct _ ->
-      failwith "constructor in a pattern after parsing !"
+      assert false (* constructor in a pattern after parsing ! *)
 
 
 (* db programs *)
@@ -96,21 +115,21 @@ let rec db_pattern = function
 let db_prog e =
   (* tids = type identifiers, ids = variables, refs = references and arrays *)
   let rec db_desc ((tids,ids,refs) as idl) = function
-      (Var x) as t ->
+    | (Var x) as t ->
 	(match lookup_var ids (Some e.loc) x with
 	     None -> t
 	   | Some c -> Expression c)
     | (Acc x) as t ->
-	check_ref refs e.loc x;
+	check_ref refs (Some e.loc) x;
 	t
     | Aff (x,e1) ->
-	check_ref refs e.loc x;
+	check_ref refs (Some e.loc) x;
 	Aff (x, db idl e1)
     | TabAcc (b,x,e1) ->
-	check_ref refs e.loc x;
+	check_ref refs (Some e.loc) x;
 	TabAcc(b,x,db idl e1)
     | TabAff (b,x,e1,e2) ->
-	check_ref refs e.loc x;
+	check_ref refs (Some e.loc) x;
 	TabAff (b,x, db idl e1, db idl e2)
     | Seq bl ->
 	Seq (List.map (function
@@ -137,7 +156,8 @@ let db_prog e =
 	  
     | LetRec (f,bl,v,var,e) ->
 	let (tids',ids',refs'),bl' = db_binders idl bl in
-	LetRec (f, bl, db_type_v tids' v, var, db (tids',f::ids',refs') e)
+	check_type_v refs' v;
+	LetRec (f, bl, v, var, db (tids',f::ids',refs') e)
 	  
     | Debug (s,e1) ->
 	Debug (s, db idl e1)
@@ -146,10 +166,10 @@ let db_prog e =
     | PPoint (s,d) -> PPoint (s, db_desc idl d)
 	  
   and db_arg ((tids,_,refs) as idl) = function
-      Term ({ desc = Var id } as t) -> 
+    | Term ({ desc = Var id } as t) -> 
 	if List.mem id refs then Refarg id else Term (db idl t)
     | Term t -> Term (db idl t)
-    | Type v -> Type (db_type_v tids v)
+    | Type v as ty -> check_type_v refs v; ty
     | Refarg _ -> assert false
 
   and db idl e =
diff --git a/contrib/correctness/pdb.mli b/contrib/correctness/pdb.mli
index 4b031be6c4..d105bd3d54 100644
--- a/contrib/correctness/pdb.mli
+++ b/contrib/correctness/pdb.mli
@@ -19,7 +19,7 @@ open Past
  * These functions directly raise UserError exceptions on bad programs.
  *)
 
-val db_type_v : Names.identifier list -> 'a ml_type_v -> 'a ml_type_v
+val check_type_v : Names.identifier list -> 'a ml_type_v -> unit
 
 val db_prog : program -> program
 
diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml
index 28d805331c..8fa2fa58e1 100644
--- a/contrib/correctness/pmlize.ml
+++ b/contrib/correctness/pmlize.ml
@@ -56,8 +56,7 @@ and trad_desc ren env ct d =
 	CC_expr c'
       else
       	let ty = trad_ml_type_v ren env tt in
-      	let t = make_tuple [ CC_expr c',ty ] qt ren env (current_date ren) in
-      	t
+      	make_tuple [ CC_expr c',ty ] qt ren env (current_date ren)
       
   | Var id ->
       if is_mutable_in_env env id then
@@ -191,7 +190,7 @@ and trad_desc ren env ct d =
 
   | App (f, args) ->
       let trad_arg (ren,args) = function
-	  Term a ->
+	| Term a ->
 	    let ((_,tya),efa,_,_) as ca = a.info.kappa in
 	    let ta = trad ren a in
 	    let w = get_writes efa in
@@ -279,7 +278,8 @@ and trad_desc ren env ct d =
 
 
 and trad_binders ren env = function
-    [] -> []
+  | [] -> 
+      []
   | (_,BindType (Ref _ | Array _))::bl ->
       trad_binders ren env bl
   | (id,BindType v)::bl ->
@@ -291,7 +291,8 @@ and trad_binders ren env = function
 
 	
 and trad_block ren env = function
-    [] -> []
+  | [] -> 
+      []
   | (Assert c)::block ->
       (Assert c)::(trad_block ren env block)
   | (Label s)::block ->
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml
index 49d8d9bf78..adba100f79 100644
--- a/contrib/correctness/pmonad.ml
+++ b/contrib/correctness/pmonad.ml
@@ -36,11 +36,11 @@ open Peffect
 
 let product_name = function
   | 2 -> "prod"
-  | n -> Printf.sprintf "tuple_%d" n
+  | n -> check_product_n n; Printf.sprintf "tuple_%d" n
 
 let dep_product_name = function
   | 1 -> "sig"
-  | n -> Printf.sprintf "sig_%d" n
+  | n -> check_dep_product_n n; Printf.sprintf "sig_%d" n
 
 let product ren env before lo = function
   | None -> (* non dependent case *)
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index e9bb7c88f9..5e0f9ad428 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -539,7 +539,8 @@ let _ =
 		   Util.errorlabstrm "PROGVARIABLE"
 		     [< 'sTR"Clash with previous constant "; pr_id id >])
 		ids;
-	      let v = Pdb.db_type_v [] (out_typev d) in
+	      let v = out_typev d in
+	      Pdb.check_type_v (all_refs ()) v;
 	      let env = empty in
 	      let ren = update empty_ren "" [] in
 	      let v = Ptyping.cic_type_v env ren v in
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
index e73b9b233e..b00f5c38fc 100644
--- a/contrib/correctness/pwp.ml
+++ b/contrib/correctness/pwp.ml
@@ -67,18 +67,18 @@ let force_post up env top q e =
 
 (* put a post-condition if none is present *)
 let post_if_none_up env top q = function
-    { post = None } as p -> force_post true env top q p 
+  | { post = None } as p -> force_post true env top q p 
   | p -> p
 
 let post_if_none env q = function
-    { post = None } as p -> force_post false env "" q p 
+  | { post = None } as p -> force_post false env "" q p 
   | p -> p
 
 (* [annotation_candidate p] determines if p is a candidate for a 
  * post-condition *)
 
 let annotation_candidate = function
-    { desc = If _ | LetIn _ | LetRef _ ; post = None } -> true
+  | { desc = If _ | LetIn _ | LetRef _ ; post = None } -> true
   | _ -> false
 
 (* [extract_pre p] erase the pre-condition of p and returns it *)
@@ -119,7 +119,7 @@ let normalize_boolean ren env b =
   Perror.check_no_effect b.loc ef;
   if is_bool v then
     match q with
-	Some _ ->
+      | Some _ ->
 	  (* il y a une annotation : on se contente de lui forcer un nom *)
 	  let q = force_bool_name q in
 	  { desc = b.desc; pre = b.pre; post = q; loc = b.loc;
@@ -143,7 +143,7 @@ let normalize_boolean ren env b =
 (* [decomp_boolean c] returns the specs R and S of a boolean expression *)
 
 let decomp_boolean = function
-    Some { a_value = q } ->
+  | Some { a_value = q } ->
       Reduction.whd_betaiota (Term.applist (q, [constant "true"])),
       Reduction.whd_betaiota (Term.applist (q, [constant "false"]))
   | _ -> invalid_arg "Ptyping.decomp_boolean"
@@ -151,11 +151,11 @@ let decomp_boolean = function
 (* top point of a program *)
 
 let top_point = function
-    PPoint (s,_) as p -> s,p
+  | PPoint (s,_) as p -> s,p
   | p -> let s = label_name() in s,PPoint(s,p)
 
 let top_point_block = function
-    (Label s :: _) as b -> s,b
+  | (Label s :: _) as b -> s,b
   | b -> let s = label_name() in s,(Label s)::b
 
 let abstract_unit q = abstract [result_id,constant "unit"] q
@@ -181,7 +181,7 @@ let add_decreasing env inv (var,r) lab bl =
 
 let post_last_statement env top q bl =
   match List.rev bl with
-      Statement e :: rem when annotation_candidate e -> 
+    | Statement e :: rem when annotation_candidate e -> 
 	List.rev ((Statement (post_if_none_up env top q e)) :: rem)
     | _ -> bl
 
@@ -191,7 +191,7 @@ let rec propagate_desc ren info d =
   let env = info.env in
   let (_,_,p,q) = info.kappa in
   match d with
-      If (e1,e2,e3) ->
+    | If (e1,e2,e3) ->
       (* propagation number 2 *)
 	let e1' = normalize_boolean ren env (propagate ren e1) in
 	if e2.post = None or e3.post = None then
@@ -252,7 +252,7 @@ let rec propagate_desc ren info d =
 and propagate ren p =
   let env = p.info.env in
   let p = match p.desc with
-      App (f,l) ->
+    | App (f,l) ->
 	let _,(_,so,ok),(_,_,_,qapp) = effect_app ren env f l in
 	if ok then
 	  let q = option_app (named_app (real_subst_in_constr so)) qapp in
@@ -315,13 +315,15 @@ and propagate ren p =
     | _ -> p
 
 and propagate_arg ren = function
-    Type _ | Refarg _ as a -> a
+  | Type _ | Refarg _ as a -> a
   | Term e -> Term (propagate ren e)
 
 
 and propagate_block ren env = function 
-    [] -> []
+  | [] -> 
+      []
   | (Statement p) :: (Assert q) :: rem when annotation_candidate p ->
+      (* TODO: plutot p.post = None ? *)
       let q' =
 	let ((id,v),_,_,_) = p.info.kappa in
 	let tv = Pmonad.trad_ml_type_v ren env v in
diff --git a/dev/ocamldebug-v7.template b/dev/ocamldebug-v7.template
index 68cd598423..115cba72f9 100644
--- a/dev/ocamldebug-v7.template
+++ b/dev/ocamldebug-v7.template
@@ -30,7 +30,7 @@ case $coqdebug in
         -I $COQTOP/proofs -I $COQTOP/tactics \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
         -I $COQTOP/contrib/omega -I $COQTOP/contrib/ring \
-	-I $COQTOP/contrib/extraction \
+	-I $COQTOP/contrib/extraction -I $COQTOP/contrib/correctness \
 	$* $args;;
     *) exec $OCAMLDEBUG $*;;
 esac