Commit 0a4d927d authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

seance5, quelques ajustements

parent d59bf1e6
......@@ -110,12 +110,12 @@ Definition somme_deux_premiers l :=
c'est très lourd: *)
Definition somme_deux_premiers2 l :=
match tail l with
match head l with
| None => None
| Some l' =>
match head l with
| Some a =>
match tail l with
| None => None
| Some a =>
| Some l' =>
match head l' with
| Some b => Some (a+b)
| _ => None
......@@ -125,6 +125,8 @@ Definition somme_deux_premiers2 l :=
(** Un peu d'abstraction, via une fonction d'ordre supérieur *)
(** Premier essai: *)
Definition option_map {A B} (o : option A)(f:A -> B) : option B :=
match o with
| Some x => Some (f x)
......@@ -132,9 +134,9 @@ Definition option_map {A B} (o : option A)(f:A -> B) : option B :=
end.
Definition somme_deux_premiers3 l :=
option_map (tail l)
(fun l' => option_map (head l)
(fun a => option_map (head l')
option_map (head l)
(fun a => option_map (tail l)
(fun l' => option_map (head l')
(fun b => a+b))).
Check somme_deux_premiers3. (* Pas le bon type !!! *)
......@@ -148,9 +150,9 @@ Definition option_bind {A B} (o : option A) (f:A -> option B) : option B :=
end.
Definition somme_deux_premiers4 l :=
option_bind (tail l)
(fun l' => option_bind (head l)
(fun a => option_bind (head l')
option_bind (head l)
(fun a => option_bind (tail l)
(fun l' => option_bind (head l')
(fun b => Some (a+b)))).
Check somme_deux_premiers4.
......@@ -160,8 +162,8 @@ Check somme_deux_premiers4.
Infix ">>=" := option_bind (at level 20, left associativity).
Definition somme_deux_premiers5 l :=
tail l >>= fun l' =>
head l >>= fun a =>
tail l >>= fun l' =>
head l' >>= fun b =>
Some (a+b).
......@@ -183,6 +185,8 @@ m >>= return = m
*)
(** La monade d'erreur *)
Module MErr <: MONAD.
Definition t := option.
Definition ret {A} := @Some A.
......@@ -192,8 +196,8 @@ End MErr.
Infix ">>=" := MErr.bind (at level 20, left associativity).
Definition somme_deux_premiers6 l :=
tail l >>= fun l' =>
head l >>= fun a =>
tail l >>= fun l' =>
head l' >>= fun b =>
MErr.ret (a+b).
......@@ -204,7 +208,8 @@ Inductive tree (A:Type) :=
Arguments Leaf {A}.
Arguments Node {A}.
(** Exemple, multiplication des feuilles d'un arbre, avec arrêt au premier zero *)
(** Exemple, multiplication des feuilles d'un arbre,
avec arrêt au premier zero *)
Fixpoint leafmul t :=
match t with
......
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