Commit 59219ac8 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

seance5 : qq améliorations (en particulier le Vnth que je n'avais pas retrouvé en direct)

parent 94c4a59b
......@@ -42,7 +42,13 @@ Check (Zero : Fin 2).
Check (Succ Zero : Fin 2).
(** Application: Vnth *)
(** Application: [Vnth]
Les entiers "bornées" du type Fin permettent de donner un
type précis et un comportement sans erreur à l'accès
au "n-ieme" élément d'un vecteur. *)
(** On reprend le type [vect] de la semaine dernière: *)
Inductive vect (A:Type) : nat -> Type :=
| Vnil : vect A 0
......@@ -51,21 +57,31 @@ Inductive vect (A:Type) : nat -> Type :=
Arguments Vnil {A}.
Arguments Vcons {A} {n}.
(* TODO
Fixpoint Vnth {A} {n} (p:Fin n) : vect A n -> A :=
match p in Fin m' return vect A m' -> A with
| @Zero m => fun (v:vect A (S m)) =>
match v with
| Vcons a _ => a
end
| @Succ m p => fun (v:vect A (S m)) =>
match v with
| Vcons _ v => Vnth v p
end
match p with
| Zero => fun v => match v with Vcons x _ => x end
| Succ p => fun v => Vnth p (match v with Vcons _ v => v end)
end.
(** NB: ce genre de programmation est encore relativement nouveau
en Coq, et encore fort délicat. Par exemple, l'exemple précédent
est rejeté par Coq si on déplace l'appel à [Vnth] sous
le dernier match, ou qu'on rassemble les deux [fun v =>]
en un seul avant le [match p].
*)
(** Exemples d'utilisation : avec une liste de taille 3,
on peut bien accéder aux éléments d'indice 0, 1, 2, mais
pas 3. *)
Definition testvec := Vcons 1 (Vcons 2 (Vcons 3 Vnil)).
Compute Vnth Zero testvec.
Compute Vnth (Succ Zero) testvec.
Compute Vnth (Succ (Succ Zero)) testvec.
Fail Compute Vnth (Succ (Succ (Succ Zero))) testvec.
(** * Monades *)
......@@ -139,6 +155,8 @@ Definition somme_deux_premiers4 l :=
Check somme_deux_premiers4.
(** Avec une jolie notation *)
Infix ">>=" := option_bind (at level 20, left associativity).
Definition somme_deux_premiers5 l :=
......@@ -147,7 +165,7 @@ Definition somme_deux_premiers5 l :=
head l' >>= fun b =>
Some (a+b).
Compute somme_deux_premiers4 [1;2;3].
Compute somme_deux_premiers5 [1;2;3].
(** Généralisation : l'interface des monades *)
......@@ -173,7 +191,7 @@ End MErr.
Infix ">>=" := MErr.bind (at level 20, left associativity).
Definition somme_deux_premiers5 l :=
Definition somme_deux_premiers6 l :=
tail l >>= fun l' =>
head l >>= fun a =>
head l' >>= fun b =>
......@@ -242,7 +260,3 @@ Module MState <: MONAD.
Definition bind {A B} (m:t A) (f:A->t B) :=
fun st => let (st',a) := m st in f a st'.
End MState.
(** * Modules *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment