expansion des constr purs

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

4 files changed, 75 insertions, 13 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 4395aa53a..3013c2c9b 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -145,6 +145,12 @@ let rawconstr_of_prog p =
     (*i optimisation : let x = <constr> in e2  =>  e2[x<-constr] 
     | CC_letin (_,_,[id,_],CC_expr c,e2) ->
 	real_subst_in_constr [id,c] (trad e2)
+    | CC_letin (_,_,([_] as b),CC_expr e1,e2) ->
+	let (b',avoid',nenv') = push_vars avoid nenv b in
+      	let c1 = Detyping.detype avoid nenv e1 
+	and c2 = trad avoid' nenv' e2 in
+	let id = Name (fst (List.hd b')) in
+	RLetIn (dummy_loc, id, c1, c2)
     i*)
 
     | CC_letin (_,_,([_] as b),e1,e2) ->
diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml
index c71c91f93..053131567 100644
--- a/contrib/correctness/pred.ml
+++ b/contrib/correctness/pred.ml
@@ -12,6 +12,39 @@
 
 open Pp
 open Past
+open Pmisc
+
+let rec cc_subst subst = function
+  | CC_var id as c -> 
+      (try CC_expr (List.assoc id subst) with Not_found -> c)
+  | CC_letin (b,ty,bl,c1,c2) ->
+      CC_letin (b, real_subst_in_constr subst ty, cc_subst_binders subst bl,
+		cc_subst subst c1, cc_subst (cc_cross_binders subst bl) c2)
+  | CC_lam (bl, c) ->
+      CC_lam (cc_subst_binders subst bl, 
+	      cc_subst (cc_cross_binders subst bl) c)
+  | CC_app (c, cl) ->
+      CC_app (cc_subst subst c, List.map (cc_subst subst) cl)
+  | CC_tuple (b, tl, cl) ->
+      CC_tuple (b, List.map (real_subst_in_constr subst) tl,
+		List.map (cc_subst subst) cl)
+  | CC_case (ty, c, cl) ->
+      CC_case (real_subst_in_constr subst ty, cc_subst subst c,
+	       List.map (cc_subst subst) cl)
+  | CC_expr c ->
+      CC_expr (real_subst_in_constr subst c)
+  | CC_hole ty ->
+      CC_hole (real_subst_in_constr subst ty)
+
+and cc_subst_binders subst = List.map (cc_subst_binder subst)
+
+and cc_subst_binder subst = function
+  | id,CC_typed_binder c -> id,CC_typed_binder (real_subst_in_constr subst c)
+  | b -> b
+
+and cc_cross_binders subst = function
+  | [] -> subst
+  | (id,_) :: bl -> cc_cross_binders (List.remove_assoc id subst) bl
 
 (* here we only perform eta-reductions on programs to eliminate
  * redexes of the kind
@@ -29,6 +62,8 @@ let is_eta_redex bl al =
       Invalid_argument("List.for_all2") -> false
 
 let rec red = function
+  | CC_letin (_, _, [id,_], CC_expr c1, e2) ->
+      red (cc_subst [id,c1] e2)
   | CC_letin (dep, ty, bl, e1, e2) ->
       begin match red e2 with
 	| CC_tuple (false,tl,al) ->
@@ -39,7 +74,6 @@ let rec red = function
 			CC_tuple (false,tl,List.map red al))
 	| e -> CC_letin (dep, ty, bl, red e1, e)
       end
-
   | CC_lam (bl, e) ->
       CC_lam (bl, red e)
   | CC_app (e, al) ->
diff --git a/contrib/correctness/preuves.v b/contrib/correctness/preuves.v
index 55cafbf8d..33659b436 100644
--- a/contrib/correctness/preuves.v
+++ b/contrib/correctness/preuves.v
@@ -19,6 +19,29 @@ Global Variable t : array N of Z.
 
 (**********************************************************************)
 
+Require Exchange.
+Require ArrayPermut.
+
+Correctness swap
+  fun (N:Z)(t:array N of Z)(i,j:Z) ->
+    { `0 <= i < N` /\ `0 <= j < N` }
+    (let v = t[i] in
+     begin
+       t[i] := t[j];
+       t[j] := v
+     end)
+    { (exchange t t@ i j) }.
+Proof.
+Auto with datatypes.
+Save.
+
+Correctness downheap
+  let rec downheap (N:Z)(t:array N of Z) : unit { variant `0` } =
+    (swap N t 0 0) { True }
+.
+
+(**********************************************************************)
+
 Global Variable x : Z ref.
 Debug on.
 Correctness assign0 (x := 0) { `x=0` }.
@@ -37,6 +60,8 @@ Save.
 Global Variable i : Z ref.
 Debug on.
 Correctness if0 { `0 <= i` } (if !i>0 then i:=!i-1 else tt) { `0 <= i` }.
+Omega.
+Save.
 
 (**********************************************************************)
 
@@ -54,11 +79,7 @@ Correctness echange
     assert { #t[i] = #t@B[j] /\ #t[j] = #t@B[i] }
   end.
 Proof.
-Auto.
-Assumption.
-Assumption.
-Elim HH_6; Auto.
-Elim HH_6; Auto.
+Auto with datatypes.
 Save.
 
   
@@ -69,9 +90,9 @@ Save.
  *)
 
 Correctness incrementation
-  while (Z_le_gt_dec !x !y) do
-    { invariant True variant (Zminus (Zs y) x) }
-    x := (Zs !x)
+  while !x < !y do
+    { invariant True variant `(Zs y)-x` }
+    x := !x + 1
   done
   { `y < x` }.
 Proof.
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index e53043fb1..4918910d3 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -11,6 +11,7 @@
 (* $Id$ *)
 
 open Pp
+open Options
 open Names
 open Term
 open Pretyping
@@ -234,7 +235,7 @@ let correctness s p opttac =
     | Some t -> tclTHEN tac t
   in
   solve_nth 1 tac;
-  show_open_subgoals()
+  if_verbose show_open_subgoals ()
 
 
 (* On redéfinit la commande "Save" pour enregistrer les nouveaux programmes *)
@@ -258,18 +259,18 @@ let wrap_save_anonymous b id =
   register pf_id (Some id)
 
 let _ = add "SaveNamed"
-    (function [] -> (fun () -> if not(Options.is_silent()) then show_script();
+    (function [] -> (fun () -> if_verbose show_script ();
 		              wrap_save_named true)
     |   _  -> assert false)
 
 let _ = add "DefinedNamed"
-    (function [] -> (fun () -> if not(Options.is_silent()) then show_script();
+    (function [] -> (fun () -> if_verbose show_script ();
 		              wrap_save_named false)
     |   _  -> assert false)
 
 let _ = add "SaveAnonymous"
     (function [VARG_IDENTIFIER id] -> 
-       (fun () -> if not(Options.is_silent()) then show_script();
+       (fun () -> if_verbose show_script ();
 	          wrap_save_anonymous true id)
     |   _  -> assert false)