Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

1 files changed, 163 insertions, 144 deletions

diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index 8c706cdf8..97e234f57 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -6,85 +6,90 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Arith.
-Require PolyList.
+Require Import Arith.
+Require Import List.
 
 (*** STANDARD EXAMPLES *)
 
 (** Functions. *)
 
-Definition idnat := [x:nat]x.
+Definition idnat (x:nat) := x.
 Extraction idnat.
 (* let idnat x = x *)
 
-Definition id := [X:Type][x:X]x.      
+Definition id (X:Type) (x:X) := x.      
 Extraction id. (* let id x = x *)
-Definition id' := (id Set nat).
+Definition id' := id Set nat.
 Extraction id'. (* type id' = nat *)
 
-Definition test2 := [f:nat->nat][x:nat](f x).
+Definition test2 (f:nat -> nat) (x:nat) := f x.
 Extraction test2.
 (* let test2 f x = f x *)
 
-Definition test3 := [f:nat->Set->nat][x:nat](f x nat).
+Definition test3 (f:nat -> Set -> nat) (x:nat) := f x nat.
 Extraction test3.
 (* let test3 f x = f x __ *)
 
-Definition test4 := [f:(nat->nat)->nat][x:nat][g:nat->nat](f g).
+Definition test4 (f:(nat -> nat) -> nat) (x:nat) (g:nat -> nat) := f g.
 Extraction test4.
 (* let test4 f x g = f g *)
 
-Definition test5 := ((1),(0)).
+Definition test5 := (1, 0).
 Extraction test5.
 (* let test5 = Pair ((S O), O) *)
 
-Definition cf :=  [x:nat][_:(le x O)](S x).
+Definition cf (x:nat) (_:x <= 0) := S x.
 Extraction NoInline cf.
-Definition test6 := (cf O (le_n O)).
+Definition test6 := cf 0 (le_n 0).
 Extraction test6.  
 (* let test6 = cf O *)
 
-Definition test7 := ([X:Set][x:X]x nat).
+Definition test7 := (fun (X:Set) (x:X) => x) nat.
 Extraction test7.
 (* let test7 x = x *)
 
-Definition d := [X:Type]X.
+Definition d (X:Type) := X.
 Extraction d. (* type 'x d = 'x *)
-Definition d2 := (d Set).
+Definition d2 := d Set.
 Extraction d2. (* type d2 = __ d *)
-Definition d3 := [x:(d Set)]O.
+Definition d3 (x:d Set) := 0.
 Extraction d3. (* let d3 _ = O *)
-Definition d4 := (d nat). 
+Definition d4 := d nat. 
 Extraction d4. (* type d4 = nat d *)
-Definition d5 := ([x:(d Type)]O Type).  
+Definition d5 := (fun x:d Type => 0) Type.  
 Extraction d5.  (* let d5 = O *)
-Definition d6 := ([x:(d Type)]x).
+Definition d6 (x:d Type) := x.
 Extraction d6.  (* type 'x d6 = 'x *)
 
-Definition test8 := ([X:Type][x:X]x Set nat).
+Definition test8 := (fun (X:Type) (x:X) => x) Set nat.
 Extraction test8. (* type test8 = nat *)
 
-Definition test9 := let t = nat in (id Set t).
+Definition test9 := let t := nat in id Set t.
 Extraction test9.  (* type test9 = nat *)
 
-Definition test10 := ([X:Type][x:X]O Type Type).
+Definition test10 := (fun (X:Type) (x:X) => 0) Type Type.
 Extraction test10. (* let test10 = O *)
 
-Definition test11 := let n=O in let p=(S n) in (S p).
+Definition test11 := let n := 0 in let p := S n in S p.
 Extraction test11. (* let test11 = S (S O) *)
 
-Definition test12 := (x:(X:Type)X->X)(x Type Type).
+Definition test12 := forall x:forall X:Type, X -> X, x Type Type.
 Extraction test12. 
 (* type test12 = (__ -> __ -> __) -> __ *)
 
 
-Definition test13 := Cases (left True True I) of (left x)=>(S O) | (right x)=>O end.
+Definition test13 := match left True I with
+                     | left x => 1
+                     | right x => 0
+                     end.
 Extraction test13. (* let test13 = S O *)
 
 
 (** example with more arguments that given by the type *)
 
-Definition test19 := (nat_rec [n:nat]nat->nat [n:nat]O [n:nat][f:nat->nat]f O O).
+Definition test19 :=
+  nat_rec (fun n:nat => nat -> nat) (fun n:nat => 0)
+    (fun (n:nat) (f:nat -> nat) => f) 0 0.
 Extraction test19.
 (* let test19 =
   let rec f = function
@@ -96,7 +101,7 @@ Extraction test19.
 
 (** casts *)
 
-Definition test20 := (True :: Type).
+Definition test20 := True:Type.
 Extraction test20.
 (* type test20 = __ *)
 
@@ -119,9 +124,9 @@ let sumbool_rect f f0 = function
 
 (** Less simple inductive type. *)
 
-Inductive c [x:nat] : nat -> Set :=
-    refl : (c x x)                  
-  | trans : (y,z:nat)(c x y)->(le y z)->(c x z).
+Inductive c (x:nat) : nat -> Set :=
+  | refl : c x x
+  | trans : forall y z:nat, c x y -> y <= z -> c x z.
 Extraction c.
 (* 
 type c =
@@ -129,15 +134,15 @@ type c =
   | Trans of nat * nat * c
 *)
 
-Definition Ensemble := [U:Type]U->Prop.
-Definition Empty_set := [U:Type][x:U]False.
-Definition Add := [U:Type][A:(Ensemble U)][x:U][y:U](A y) \/ x==y.
+Definition Ensemble (U:Type) := U -> Prop.
+Definition Empty_set (U:Type) (x:U) := False.
+Definition Add (U:Type) (A:Ensemble U) (x y:U) := A y \/ x = y.
 
-Inductive Finite [U:Type] : (Ensemble U) -> Set :=
-      Empty_is_finite: (Finite U (Empty_set U))
-   |  Union_is_finite:
-      (A: (Ensemble U)) (Finite U A) -> 
-      (x: U) ~ (A x) -> (Finite U (Add U A x)).
+Inductive Finite (U:Type) : Ensemble U -> Set :=
+  | Empty_is_finite : Finite U (Empty_set U)
+  | Union_is_finite :
+      forall A:Ensemble U,
+        Finite U A -> forall x:U, ~ A x -> Finite U (Add U A x).
 Extraction Finite.
 (* 
 type 'u finite =
@@ -148,11 +153,11 @@ type 'u finite =
 
 (** Mutual Inductive *)
 
-Inductive tree : Set := 
-   Node : nat -> forest -> tree
+Inductive tree : Set :=
+    Node : nat -> forest -> tree
 with forest : Set :=
- | Leaf : nat -> forest
- | Cons : tree -> forest -> forest .
+  | Leaf : nat -> forest
+  | Cons : tree -> forest -> forest.
 
 Extraction tree.
 (* 
@@ -163,13 +168,16 @@ and forest =
   | Cons of tree * forest
 *)
 
-Fixpoint tree_size [t:tree] : nat :=
-         Cases t of (Node a f) => (S (forest_size f)) end
-with forest_size [f:forest] : nat :=
-         Cases f of 
-	 | (Leaf b) => (S O)
-         | (Cons t f') => (plus (tree_size t) (forest_size f'))
-         end.
+Fixpoint tree_size (t:tree) : nat :=
+  match t with
+  | Node a f => S (forest_size f)
+  end
+ 
+ with forest_size (f:forest) : nat :=
+  match f with
+  | Leaf b => 1
+  | Cons t f' => tree_size t + forest_size f'
+  end.
 
 Extraction tree_size.
 (* 
@@ -183,35 +191,39 @@ and forest_size = function
 
 (** Eta-expansions of inductive constructor *)
 
-Inductive titi : Set := tata : nat->nat->nat->nat->titi.
-Definition test14 := (tata O).
+Inductive titi : Set :=
+    tata : nat -> nat -> nat -> nat -> titi.
+Definition test14 := tata 0.
 Extraction test14.
 (* let test14 x x0 x1 = Tata (O, x, x0, x1) *)
-Definition test15 := (tata O (S O)).
+Definition test15 := tata 0 1.
 Extraction test15. 
 (* let test15 x x0 = Tata (O, (S O), x, x0) *)
 
-Inductive eta : Set := eta_c : nat->Prop->nat->Prop->eta.
+Inductive eta : Set :=
+    eta_c : nat -> Prop -> nat -> Prop -> eta.
 Extraction eta_c.
 (* 
 type eta =
   | Eta_c of nat * nat
 *)
-Definition test16 := (eta_c O).
+Definition test16 := eta_c 0.
 Extraction test16.
 (* let test16 x = Eta_c (O, x) *)
-Definition test17 := (eta_c O True).
+Definition test17 := eta_c 0 True.
 Extraction test17.
 (* let test17 x = Eta_c (O, x) *)
-Definition test18 := (eta_c O True O).
+Definition test18 := eta_c 0 True 0.
 Extraction test18. 
 (* let test18 _ = Eta_c (O, O) *)
 
 
 (** Example of singleton inductive type *)
 
-Inductive bidon [A:Prop;B:Type] : Set := tb : (x:A)(y:B)(bidon A B). 
-Definition fbidon := [A,B:Type][f:A->B->(bidon True nat)][x:A][y:B](f x y).
+Inductive bidon (A:Prop) (B:Type) : Set :=
+    tb : forall (x:A) (y:B), bidon A B. 
+Definition fbidon (A B:Type) (f:A -> B -> bidon True nat) 
+  (x:A) (y:B) := f x y.
 Extraction bidon.
 (* type 'b bidon = 'b *)
 Extraction tb.
@@ -221,7 +233,7 @@ Extraction fbidon.
   f x y
 *)
 
-Definition fbidon2 := (fbidon True nat (tb True nat)).
+Definition fbidon2 := fbidon True nat (tb True nat).
 Extraction fbidon2. (* let fbidon2 y = y *)
 Extraction NoInline fbidon.
 Extraction fbidon2.
@@ -231,10 +243,10 @@ Extraction fbidon2.
 
 (** mutual inductive on many sorts *)
 
-Inductive 
-  test_0 : Prop := ctest0 : test_0 
-with 
-  test_1 : Set := ctest1 : test_0-> test_1.  
+Inductive test_0 : Prop :=
+    ctest0 : test_0
+with test_1 : Set :=
+    ctest1 : test_0 -> test_1.  
 Extraction test_0.
 (* test0 : logical inductive *)
 Extraction test_1. 
@@ -254,8 +266,10 @@ Extraction eq_rect.
 
 (** No more propagation of type parameters. Obj.t instead. *)
 
-Inductive tp1 : Set := 
-  T : (C:Set)(c:C)tp2 -> tp1 with tp2 : Set  := T' : tp1->tp2.
+Inductive tp1 : Set :=
+    T : forall (C:Set) (c:C), tp2 -> tp1
+with tp2 : Set :=
+    T' : tp1 -> tp2.
 Extraction tp1.
 (* 
 type tp1 =
@@ -264,9 +278,10 @@ and tp2 =
   | T' of tp1
 *) 
 
-Inductive tp1bis : Set := 
-  Tbis : tp2bis -> tp1bis 
-with tp2bis : Set  := T'bis : (C:Set)(c:C)tp1bis->tp2bis.
+Inductive tp1bis : Set :=
+    Tbis : tp2bis -> tp1bis
+with tp2bis : Set :=
+    T'bis : forall (C:Set) (c:C), tp1bis -> tp2bis.
 Extraction tp1bis.
 (* 
 type tp1bis =
@@ -278,9 +293,9 @@ and tp2bis =
 
 (** Strange inductive type. *)
 
-Inductive Truc : Set->Set :=
-       chose  : (A:Set)(Truc A)
-     | machin : (A:Set)A->(Truc bool)->(Truc A).
+Inductive Truc : Set -> Set :=
+  | chose : forall A:Set, Truc A
+  | machin : forall A:Set, A -> Truc bool -> Truc A.
 Extraction Truc.
 (*
 type 'x truc =
@@ -291,19 +306,17 @@ type 'x truc =
 
 (** Dependant type over Type *)
 
-Definition test24:= (sigT Set [a:Set](option a)).
+Definition test24 := sigT (fun a:Set => option a).
 Extraction test24.
 (* type test24 = (__, __ option) sigT *)
 
 
 (** Coq term non strongly-normalizable after extraction *)
 
-Require Gt.
-Definition loop := 
- [Ax:(Acc nat gt O)]
- (Fix F {F [a:nat;b:(Acc nat gt a)] : nat := 
-          (F (S a) (Acc_inv nat gt a b (S a) (gt_Sn_n a)))}
- O Ax).
+Require Import Gt.
+Definition loop (Ax:Acc gt 0) :=
+  (fix F (a:nat) (b:Acc gt a) {struct b} : nat :=
+     F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax.
 Extraction loop.
 (* let loop _ =
   let rec f a =
@@ -315,14 +328,14 @@ Extraction loop.
 
 (** False conversion of type: *)
 
-Lemma oups : (H:(nat==(list nat)))nat -> nat.
-Intros.
-Generalize H0;Intros.
-Rewrite H in H1.
-Case H1.
-Exact H0.
-Intros.
-Exact n.
+Lemma oups : forall H:nat = list nat, nat -> nat.
+intros.
+generalize H0; intros.
+rewrite H in H1.
+case H1.
+exact H0.
+intros.
+exact n.
 Qed.
 Extraction oups.
 (* 
@@ -335,7 +348,8 @@ let oups h0 =
 
 (** hybrids *)
 
-Definition horibilis := [b:bool]<[b:bool]if b then Type else nat>if b then Set else O.
+Definition horibilis (b:bool) :=
+  if b as b return (if b then Type else nat) then Set else 0.
 Extraction horibilis.
 (* 
 let horibilis = function
@@ -343,13 +357,13 @@ let horibilis = function
   | False -> Obj.magic O
 *)
 
-Definition PropSet := [b:bool]if b then Prop else Set.
+Definition PropSet (b:bool) := if b then Prop else Set.
 Extraction PropSet. (* type propSet = __ *)
 
-Definition natbool := [b:bool]if b then nat else bool.
+Definition natbool (b:bool) := if b then nat else bool.
 Extraction natbool. (* type natbool = __ *)
 
-Definition zerotrue := [b:bool]<natbool>if b then O else true.
+Definition zerotrue (b:bool) := if b as x return natbool x then 0 else true.
 Extraction zerotrue. 
 (* 
 let zerotrue = function
@@ -357,11 +371,11 @@ let zerotrue = function
   | False -> Obj.magic True
 *)
 
-Definition natProp := [b:bool]<[_:bool]Type>if b then nat else Prop.
+Definition natProp (b:bool) := if b return Type then nat else Prop.
 
-Definition natTrue := [b:bool]<[_:bool]Type>if b then nat else True.
+Definition natTrue (b:bool) := if b return Type then nat else True.
 
-Definition zeroTrue := [b:bool]<natProp>if b then O else True.
+Definition zeroTrue (b:bool) := if b as x return natProp x then 0 else True.
 Extraction zeroTrue.
 (* 
 let zeroTrue = function
@@ -369,9 +383,9 @@ let zeroTrue = function
   | False -> Obj.magic __
 *)
 
-Definition natTrue2 := [b:bool]<[_:bool]Type>if b then nat else True.
+Definition natTrue2 (b:bool) := if b return Type then nat else True.
 
-Definition zeroprop := [b:bool]<natTrue>if b then O else I.
+Definition zeroprop (b:bool) := if b as x return natTrue x then 0 else I.
 Extraction zeroprop.
 (* 
 let zeroprop = function
@@ -381,20 +395,22 @@ let zeroprop = function
 
 (** polymorphic f applied several times *)
 
-Definition test21 := (id nat O, id bool true).
+Definition test21 := (id nat 0, id bool true).
 Extraction test21.
 (* let test21 = Pair ((id O), (id True)) *)
 
 (** ok *)
 
-Definition test22 := ([f:(X:Type)X->X](f nat O, f bool true) [X:Type][x:X]x).
+Definition test22 :=
+  (fun f:forall X:Type, X -> X => (f nat 0, f bool true))
+    (fun (X:Type) (x:X) => x).
 Extraction test22. 
 (* let test22 = 
   let f = fun x -> x in Pair ((f O), (f True)) *)
 
 (* still ok via optim beta -> let *)
 
-Definition test23 := [f:(X:Type)X->X](f nat O, f bool true).
+Definition test23 (f:forall X:Type, X -> X) := (f nat 0, f bool true).
 Extraction test23.
 (* let test23 f = Pair ((Obj.magic f __ O), (Obj.magic f __ True)) *)
 
@@ -404,27 +420,30 @@ Extraction test23.
 
 (** Dummy constant __ can be applied.... *)
 
-Definition f : (X:Type)(nat->X)->(X->bool)->bool := 
- [X:Type;x:nat->X;y:X->bool](y (x O)).
+Definition f (X:Type) (x:nat -> X) (y:X -> bool) : bool := y (x 0).
 Extraction f.
 (* let f x y =
   y (x O)
 *)
 
-Definition f_prop := (f (O=O) [_](refl_equal ? O) [_]true).
+Definition f_prop := f (0 = 0) (fun _ => refl_equal 0) (fun _ => true).
 Extraction NoInline f.
 Extraction f_prop.
 (* let f_prop =
   f (Obj.magic __) (fun _ -> True)
 *)
 
-Definition f_arity := (f Set [_:nat]nat [_:Set]true).
+Definition f_arity := f Set (fun _:nat => nat) (fun _:Set => true).
 Extraction f_arity.
 (* let f_arity =
   f (Obj.magic __) (fun _ -> True)
 *)
 
-Definition f_normal := (f nat [x]x [x](Cases x of O => true | _ => false end)).
+Definition f_normal :=
+  f nat (fun x => x) (fun x => match x with
+                               | O => true
+                               | _ => false
+                               end).
 Extraction f_normal.
 (* let f_normal =
   f (fun x -> x) (fun x -> match x with
@@ -435,8 +454,8 @@ Extraction f_normal.
 
 (* inductive with magic needed *)
 
-Inductive Boite : Set := 
-  boite : (b:bool)(if b then nat else nat*nat)->Boite. 
+Inductive Boite : Set :=
+    boite : forall b:bool, (if b then nat else (nat * nat)%type) -> Boite. 
 Extraction Boite. 
 (*
 type boite =
@@ -444,18 +463,19 @@ type boite =
 *)
 
 
-Definition boite1 := (boite true O).
+Definition boite1 := boite true 0.
 Extraction boite1.
 (* let boite1 = Boite (True, (Obj.magic O)) *)
 
-Definition boite2 := (boite false (O,O)).
+Definition boite2 := boite false (0, 0).
 Extraction boite2.
 (* let boite2 = Boite (False, (Obj.magic (Pair (O, O)))) *)
 
-Definition test_boite := [B:Boite]<nat>Cases B of 
-  (boite true n) => n 
-| (boite false n) => (plus (fst ? ? n) (snd ? ? n))
-end.
+Definition test_boite (B:Boite) :=
+  match B return nat with
+  | boite true n => n
+  | boite false n => fst n + snd n
+  end.
 Extraction test_boite. 
 (* 
 let test_boite = function
@@ -467,18 +487,18 @@ let test_boite = function
 
 (* singleton inductive with magic needed *)
 
-Inductive Box : Set := 
-  box : (A:Set)A -> Box. 
+Inductive Box : Set :=
+    box : forall A:Set, A -> Box. 
 Extraction Box.
 (* type box = __ *)
 
-Definition box1 := (box nat O). 
+Definition box1 := box nat 0. 
 Extraction box1. (* let box1 = Obj.magic O *)
 
 (* applied constant, magic needed *)
 
-Definition idzarb := [b:bool][x:(if b then nat else bool)]x.
-Definition zarb := (idzarb true O).
+Definition idzarb (b:bool) (x:if b then nat else bool) := x.
+Definition zarb := idzarb true 0.
 Extraction NoInline idzarb. 
 Extraction zarb. 
 (* let zarb = Obj.magic idzarb True (Obj.magic O) *)
@@ -486,30 +506,31 @@ Extraction zarb.
 (** function of variable arity. *)
 (** Fun n = nat -> nat -> ... -> nat *)  
 
-Fixpoint Fun [n:nat] : Set := 
-   Cases n of 
-     O => nat
-   | (S n) => nat -> (Fun n)
+Fixpoint Fun (n:nat) : Set :=
+  match n with
+  | O => nat
+  | S n => nat -> Fun n
   end.
 
-Fixpoint Const [k,n:nat] : (Fun n) := 
-  <Fun>Cases n of 
-     O => k 
-   | (S n) => [p:nat](Const k n)
+Fixpoint Const (k n:nat) {struct n} : Fun n :=
+  match n as x return Fun x with
+  | O => k
+  | S n => fun p:nat => Const k n
   end.
 
-Fixpoint proj [k,n:nat] : (Fun n) := 
-  <Fun>Cases n of 
-    O => O (* ou assert false ....*)
-  | (S n) => Cases k of 
-             O => [x](Const x n)
-           | (S k) => [x](proj k n)
-          end 
+Fixpoint proj (k n:nat) {struct n} : Fun n :=
+  match n as x return Fun x with
+  | O => 0 (* ou assert false ....*)
+  | S n =>
+      match k with
+      | O => fun x => Const x n
+      | S k => fun x => proj k n
+      end
   end. 
 
-Definition test_proj := (proj (2) (4) (0) (1) (2) (3)).
+Definition test_proj := proj 2 4 0 1 2 3.
 
-Eval Compute in test_proj. 
+Eval compute in test_proj. 
 
 Recursive Extraction test_proj. 
 
@@ -518,16 +539,14 @@ Recursive Extraction test_proj.
 (*** TO SUM UP: ***) 
 
 
-Extraction "test_extraction.ml" 
-  idnat id id' test2 test3 test4 test5 test6 test7 
-  d d2 d3 d4 d5 d6 test8 id id' test9 test10 test11 
-  test12 test13 test19 test20 
-  nat sumbool_rect c Finite tree tree_size
-  test14 test15 eta_c test16 test17 test18 bidon tb fbidon fbidon2 
-  fbidon2 test_0 test_1 eq eq_rect tp1 tp1bis Truc oups test24 loop
-  horibilis PropSet natbool zerotrue zeroTrue zeroprop test21 test22 
-  test23 f f_prop f_arity f_normal
-  Boite boite1 boite2 test_boite
-  Box box1 zarb test_proj.
-
+Extraction
+ "test_extraction.ml" idnat id id' test2 test3 test4 test5 test6 test7 d d2
+                     d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
+                     test13 test19 test20 nat sumbool_rect c Finite tree
+                     tree_size test14 test15 eta_c test16 test17 test18 bidon
+                     tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
+                     tp1bis Truc oups test24 loop horibilis PropSet natbool
+                     zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
+                     f_arity f_normal Boite boite1 boite2 test_boite Box box1
+                     zarb test_proj.