Voting

Category

real language

Bookmarking

Del.icio.us Digg Diigo DZone Earthlink Google Kick.ie
Windows Live LookLater Ma.gnolia Reddit Rojo StumbleUpon Technorati

Language coq

Date:04/01/11
Author:Hugo Feree
URL:n/a
Comments:0
Info:http://coq.inria.fr/
Score: (3.33 in 3 votes)
Require Import String Ascii.
Open Scope string_scope.

Fixpoint ten_div n := match n with
  | S(S(S(S(S(S(S(S(S(S p))))))))) => let (q, r) := ten_div p in (S q, r)
  | _ => (O, n)
end.

Function nts (n : nat) : string := 
match ten_div n with
  | (O, r) => String (ascii_of_nat (48 + r)) ""
  | (q, r) => String (ascii_of_nat (48 + (snd(ten_div q)))) (String (ascii_of_nat (48 + r)) "")
end.

Let take := "
Take one down and pass it around, ".

Fixpoint bottle n := match n with
 | O => ""
 | 2 => "2 bottles of beer on the wall, 2 bottles of beer." ++ take ++ "1 bottle of beer on the
wall.

1 bottle of beer on the wall, 1 bottle of beer." ++ take ++ "no more bottles of beer on the wall.

No more bottles of beer on the wall, no more bottles of beer.
Go to the store and buy some more, 99 bottles of beer on the wall."
 | (S n) => (nts(S n)) ++ " bottles of beer on the wall, " ++ (nts (S n)) ++ " bottles of beer." ++
take ++ (nts n) ++ " bottles of beer on the wall.

" ++ (bottle n)
end.

Eval compute in (bottle 99).


(*
You can check that this is correct:

Lemma correct : bottle 99 ="put here the entire song".
Proof.
reflexivity.
Qed.
*)

Download Source | Write Comment

Alternative Versions

VersionAuthorDateCommentsRate
Coq with LtacJean-Marie Madiot06/25/100

Comments

Download Source | Write Comment

Add Comment

Please provide a value for the fields Name, Comment and Security Code.
This is a gravatar-friendly website.
E-mail addresses will never be shown.
Enter your e-mail address to use your gravatar.

Please don't post large portions of code here! Use the form to submit new examples or updates instead!

Name:

eMail:

URL:

Security Code:
  
Comment: