réparation Correctness; options Extraction (changement de syntaxe)

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

13 files changed, 60 insertions, 77 deletions

diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v
index bc12ec755..0c47512ed 100644
--- a/contrib/correctness/Correctness.v
+++ b/contrib/correctness/Correctness.v
@@ -22,13 +22,4 @@ Require Export ProgWf.
 
 Require Export Arrays.
 
-Declare ML Module
-    "pmisc" "peffect" "prename" 
-    "perror" "penv" "putil" "pdb" "pcic" "pmonad" "pcicenv"
-    "pred" "ptyping" "pwp" "pmlize" "ptactic" "psyntax".
-
 Token "'".
-
-
-
-
diff --git a/contrib/correctness/examples/exp.v b/contrib/correctness/examples/exp.v
index 1b6bc0b38..e4aaa49c2 100644
--- a/contrib/correctness/examples/exp.v
+++ b/contrib/correctness/examples/exp.v
@@ -149,7 +149,7 @@ Correctness i_exp
     let e = ref n in
     begin
       while (notzerop_bool !e) do
-        { invariant (power x n)=(mult y (power m e)) as I
+        { invariant (power x n)=(mult y (power m e)) as Inv
           variant e for lt }
         (if not (even_odd_bool !e) then y := (mult !y !m))
           { (power x n) = (mult y (power m (double (div2 e)))) as Q };
@@ -161,11 +161,10 @@ Correctness i_exp
     { result=(power x n) }
 .
 Proof.
-Rewrite (odd_double e0 Test1) in I. Rewrite I. Simpl. Auto with arith.
+stop.
+Rewrite (odd_double e0 Test1) in Inv. Rewrite Inv. Simpl. Auto with arith.
 
-Rewrite (even_double e0 Test1) in I. Rewrite I. Reflexivity.
-
-Split.
+Rewrite (even_double e0 Test1) in Inv. Rewrite Inv. Reflexivity.
 
 Exact (lt_div2 e0 Test2).
 
@@ -177,8 +176,8 @@ Rewrite (power_2n m0 (div2 e0)). Reflexivity.
 
 Auto with arith.
 
-Decompose [and] I.
-Rewrite H0. Rewrite H1.
+Decompose [and] Inv.
+Rewrite H. Rewrite H0.
 Auto with arith.
 Save.
 
diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v
index dc55eafa1..e6beecccf 100644
--- a/contrib/correctness/examples/exp_int.v
+++ b/contrib/correctness/examples/exp_int.v
@@ -27,7 +27,7 @@
 Require Zpower.
 Require Zcomplements.
 
-Require Programs.
+Require Correctness.
 Require ZArithRing.
 Require Omega.
 
@@ -52,12 +52,12 @@ Intro. Absurd `0 > 0`; [ Omega | Assumption ].
 Destruct p; Auto with zarith.
 
 Simpl.
-Intro p.
+Intro p0.
 Replace (POS (xI p0)) with `2*(POS p0)+1`.
 Omega.
 Simpl. Auto with zarith.
 
-Intro p.
+Intro p0.
 Simpl.
 Replace (POS (xO p0)) with `2*(POS p0)`.
 Omega.
@@ -120,7 +120,7 @@ Correctness i_exp
     let e = ref n in
     begin
       while !e > 0 do
-        { invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as I
+        { invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as Inv
           variant e }
         (if not (Zeven_odd_bool !e) then y := (Zmult !y !m))
           { (Zpower x n) = (Zmult y (Zpower m (Zdouble (Zdiv2 e)))) as Q };
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index cf233a988..4395aa53a 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -185,10 +185,11 @@ let rawconstr_of_prog p =
       	let args = tyl @ cl in
 	RApp (dummy_loc, RRef (dummy_loc, tuple), args)
 
-    | CC_case (_,b,el) ->
+    | CC_case (ty,b,el) ->
 	let c = trad avoid nenv b in
 	let cl = List.map (trad avoid nenv) el in
-	ROldCase (dummy_loc, false, None, c, Array.of_list cl)
+	let ty = Detyping.detype avoid nenv ty in
+	ROldCase (dummy_loc, false, Some ty, c, Array.of_list cl)
 
     | CC_expr c -> 
 	Detyping.detype avoid nenv c
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 77356e17c..d6a15959b 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -17,8 +17,6 @@ open Term
 
 module SpSet = Set.Make(struct type t = section_path let compare = sp_ord end)
 
-let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
-
 (* debug *)
 
 let debug = ref false
@@ -148,6 +146,12 @@ let real_subst_in_constr = replace_vars
 
 (* Coq constants *)
 
+let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
+
+let bool_sp = coq_constant ["Init"; "Datatypes"] "bool"
+let coq_true = mkMutConstruct (((bool_sp,0),1), [||])
+let coq_false = mkMutConstruct (((bool_sp,0),2), [||])
+
 let constant s =
   let id = id_of_string s in
   Declare.global_reference CCI id
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index 96519ee9f..a4359b6d8 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -15,8 +15,6 @@ open Term
 
 module SpSet : Set.S with type elt = section_path
 
-val coq_constant : string list -> string -> section_path
-
 (* Some misc. functions *)
 
 val reraise_with_loc : Coqast.loc -> ('a -> 'b) -> 'a -> 'b
@@ -57,8 +55,12 @@ val subst_ast_in_ast : (identifier * Coqast.t) list -> Coqast.t -> Coqast.t
 val real_subst_in_constr : (identifier * constr) list -> constr -> constr
 
 val constant : string -> constr
+val coq_constant : string list -> string -> section_path
 val conj : constr -> constr -> constr
 
+val coq_true : constr
+val coq_false : constr
+
 val connective_and : identifier
 val connective_or  : identifier
 val connective_not : identifier
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml
index 9d69ecdcb..49d8d9bf7 100644
--- a/contrib/correctness/pmonad.ml
+++ b/contrib/correctness/pmonad.ml
@@ -402,14 +402,19 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c =
  *)
 
 let make_if_case ren env ty (b,qb) (br1,br2) =
-  let ty',id_b = match qb with
+  let id_b,ty',ty1,ty2 = match qb with
     | Some q ->  
   	let q = apply_post ren env (current_date ren) q in
     	let (name,t1,t2) = Term.destLambda q.a_value in
-    	Term.mkLambda (name, t1, (mkArrow t2 ty)), q.a_name
+	q.a_name,
+    	Term.mkLambda (name, t1, mkArrow t2 ty),
+	Term.mkApp (q.a_value, [| coq_true |]),
+	Term.mkApp (q.a_value, [| coq_false |])
     | None -> assert false
   in
-  CC_app (CC_case (ty', b, [br1;br2]),
+  let n = test_name Anonymous in
+  CC_app (CC_case (ty', b, [CC_lam ([n,CC_typed_binder ty1], br1);
+			    CC_lam ([n,CC_typed_binder ty2], br2)]),
 	  [CC_var (post_name id_b)])
 
 let make_if ren env (tb,cb) ren' (t1,c1) (t2,c2) c =
@@ -436,17 +441,10 @@ let make_if ren env (tb,cb) ren' (t1,c1) (t2,c2) c =
   in
   let t1,ty1 = branch c1 t1 in
   let t2,ty2 = branch c2 t2 in
-  let t1,t2 =
-    let n = test_name Anonymous in
-    CC_lam ([n,CC_untyped_binder],t1),
-    CC_lam ([n,CC_untyped_binder],t2) in
   let ty = ty1 in
   let qb = force_bool_name qb in
   let t = make_if_case ren env ty (CC_var resb,qb) (t1,t2) in
-  let t = 
-    make_let_in ren env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty)
-  in
-  t
+  make_let_in ren env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty)
 
 
 (* [make_while ren env (cphi,r,a) (tb,cb) (te,ce) c]
@@ -509,10 +507,6 @@ let make_body_while ren env phi_of a r id_phi0 id_w (tb,cb) tbl (i,c) =
       (CC_expr (constant "tt"),constant "unit") (ef,is)
   in
 
-  let t1,t2 =
-    let n = test_name Anonymous in
-    CC_lam ([n,CC_untyped_binder],t1),
-    CC_lam ([n,CC_untyped_binder],t2) in
   let b_al = current_vars ren' (get_reads eb) in
   let qb = force_bool_name qb in
   let t = make_if_case ren' env ty (CC_var resb,qb) (t1,t2) in
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 64a291026..80399858c 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -94,7 +94,7 @@ let ast_of_int n =
 let constr_of_int n =
   Astterm.interp_constr Evd.empty (Global.env ()) (ast_of_int n)
 
-let ast_constant loc s = <:ast< ($VAR $s) >>
+let ast_constant loc s = <:ast< (QUALID ($VAR $s)) >>
 
 let conj_assert {a_name=n;a_value=a} {a_value=b} = 
   let loc = Ast.loc a in
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 45ab72c38..950ef30b5 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -98,7 +98,7 @@ open Equality
 let nat = IndRef (coq_constant ["Init";"Datatypes"] "nat", 0)
 let lt = ConstRef (coq_constant ["Init";"Peano"] "lt")
 let well_founded = ConstRef (coq_constant ["Init";"Wf"] "well_founded")
-let z = IndRef (coq_constant ["Init";"fast_integer"] "Z", 0)
+let z = IndRef (coq_constant ["Zarith";"fast_integer"] "Z", 0)
 let and_ = IndRef (coq_constant ["Init";"Logic"] "and", 0)
 let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0)
 
@@ -107,7 +107,7 @@ let wf_nat_pattern =
   PApp (PRef well_founded, [| PRef nat; PRef lt |])
 (* ["((well_founded Z (Zwf ?1))"] *)
 let wf_z_pattern = 
-  let zwf = ConstRef (coq_constant ["correctness";"Zwf"] "Zwf") in
+  let zwf = ConstRef (coq_constant ["correctness";"ProgWf"] "Zwf") in
   PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta (Some 1) |]) |])
 (* ["(and ?1 ?2)"] *)
 let and_pattern = 
@@ -252,14 +252,9 @@ let wrap_save_named b =
   Command.save_named b;
   register pf_id None
 
-let wrap_save_anonymous_thm b id =
+let wrap_save_anonymous b id =
   let pf_id = Pfedit.get_current_proof_name () in
-  Command.save_anonymous_thm b (string_of_id id);
-  register pf_id (Some id)
-
-let wrap_save_anonymous_remark b id =
-  let pf_id = Pfedit.get_current_proof_name () in
-  Command.save_anonymous_remark b (string_of_id id);
+  Command.save_anonymous b (string_of_id id);
   register pf_id (Some id)
 
 let _ = add "SaveNamed"
@@ -272,14 +267,9 @@ let _ = add "DefinedNamed"
 		              wrap_save_named false)
     |   _  -> assert false)
 
-let _ = add "SaveAnonymousThm"
+let _ = add "SaveAnonymous"
     (function [VARG_IDENTIFIER id] -> 
        (fun () -> if not(Options.is_silent()) then show_script();
-	          wrap_save_anonymous_thm true id)
+	          wrap_save_anonymous true id)
     |   _  -> assert false)
 
-let _ = add "SaveAnonymousRmk"
-    (function [VARG_IDENTIFIER id] -> 
-        (fun () -> if not(Options.is_silent()) then show_script();
-	            wrap_save_anonymous_remark true id)
-    |   _  -> assert false)
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index c4c62b3cb..e909d4511 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -12,10 +12,10 @@ Grammar vernac vernac : ast :=
 | extr_list   [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] ->
               [ (ExtractionRec ($LIST $l)) ]
 | extr_list   
-     [ "Extraction" options($o) stringarg($f) ne_qualidarg_list($l) "." ] 
+     [ "Extraction" stringarg($f) options($o) ne_qualidarg_list($l) "." ] 
   -> [ (ExtractionFile $o $f ($LIST $l)) ]
 | extr_module 
-     [ "Extraction" options($o) "Module" identarg($m) "." ]
+     [ "Extraction" "Module" options($o) identarg($m) "." ]
   -> [ (ExtractionModule $o $m) ]
 
 | extract_constant 
@@ -39,7 +39,7 @@ with idorstring : ast :=
 | ids_string [ stringarg($s) ] -> [ $s ]
 
 with options : ast :=
-| ext_opt_noopt [ "noopt" ] -> [ (VERNACARGLIST "noopt") ]
-| ext_op_expand [ "expand" "[" ne_qualidarg_list($l) "]" ] -> 
+| ext_opt_noopt [ "[" "noopt" "]" ] -> [ (VERNACARGLIST "noopt") ]
+| ext_op_expand [ "[" "expand" ne_qualidarg_list($l) "]" ] -> 
                 [ (VERNACARGLIST "expand" ($LIST $l)) ]
 | ext_opt_none  [ ] -> [ (VERNACARGLIST "nooption") ].
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index b0bb1ad3a..616591048 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -161,13 +161,13 @@ let _ =
 
 let interp_options keep modular = function
   | [VARG_STRING "noopt"] ->
-      { no_opt = true; modular = modular; 
+      { optimization = false; modular = modular; 
 	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
   | [VARG_STRING "nooption"] ->
-      { no_opt = false; modular = modular;
+      { optimization = not modular; modular = modular;
 	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
   | VARG_STRING "expand" :: l ->
-      { no_opt = false; modular = modular;
+      { optimization = not modular; modular = modular;
 	to_keep = refs_set_of_list keep; 
 	to_expand = refs_set_of_list (refs_of_vargl l) }
   | _ -> 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 4b04c4dec..b7a07c706 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -202,26 +202,29 @@ module Refset =
 
 type extraction_params = {
   modular : bool;       (* modular extraction *)
-  no_opt : bool;        (* no optimization at all *)
+  optimization : bool;  (* we need optimization *)
   to_keep : Refset.t;   (* globals to keep *)
   to_expand : Refset.t; (* globals to expand *)
 }
 
-let ml_subst_glob r m = 
+let subst_glob_ast r m = 
   let rec substrec = function
     | MLglob r' as t -> if r = r' then m else t
     | t -> ast_map substrec t
   in
   substrec
 
-let expand r m = function
-  | Dglob(r',t') -> Dglob(r', ml_subst_glob r m t')
+let subst_glob_decl r m = function
+  | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t')
   | d -> d
 
 let normalize = betared_ast
 
-let keep prm r t' = true
-  (* prm.no_opt || Refset.mem r prm.to_keep *)
+let expansion_test r t = false
+
+let expand prm r t = 
+  (not (Refset.mem r prm.to_keep)) &&
+  (Refset.mem r prm.to_expand || (prm.optimization && expansion_test r t))
 
 let warning_expansion r = 
   wARN (hOV 0 [< 'sTR "The constant"; 'sPC;
@@ -240,13 +243,12 @@ let rec optimize prm = function
       let t' = normalize t in [ Dglob(r,t') ]
   | Dglob(r,t) as d :: l ->
       let t' = normalize t in
-      if keep prm r t' then
-	(Dglob(r,t')) :: (optimize prm l)
-      else begin
+      if expand prm r t' then begin
 	warning_expansion r;
-	let l' = List.map (expand r t') l in
+	let l' = List.map (subst_glob_decl r t') l in
         optimize prm l'
-      end
+      end else 
+	(Dglob(r,t')) :: (optimize prm l)
 
 (*s Table for direct ML extractions. *)
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index af931b648..f4aae3b7f 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -45,7 +45,7 @@ module Refset : Set.S with type elt = global_reference
 
 type extraction_params = {
   modular : bool;       (* modular extraction *)
-  no_opt : bool;        (* no optimization at all *)
+  optimization : bool;  (* we need optimization *)
   to_keep : Refset.t;   (* globals to keep *)
   to_expand : Refset.t; (* globals to expand *)
 }