coq1

Module Test.

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

Definition next_weekday (d:day) : day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => monday
  | saturday => monday
  | sunday => monday
  end.

Definition prev_weekday (d:day) : day :=
  match d with
  | monday => friday
  | tuesday => monday
  | wednesday => tuesday
  | thursday => wednesday
  | friday => thursday
  | saturday => friday
  | sunday => friday
  end.

Example test_next_weekday:
  next_weekday (next_weekday saturday) = tuesday.
Proof. simpl. reflexivity. Qed.

Example test_prev_weekday:
  prev_weekday (prev_weekday saturday) = thursday.
Proof. simpl. reflexivity. Qed.

End Test.

Require Extraction.
Extraction Language Haskell.
Recursive Extraction Test.


 ----> After compilation to Haskell <----


module Main where

import qualified Prelude

data Day =
   Monday
 | Tuesday
 | Wednesday
 | Thursday
 | Friday
 | Saturday
 | Sunday

day_rect :: a1 -> a1 -> a1 -> a1 -> a1 -> a1 -> a1 -> Day -> a1
day_rect f f0 f1 f2 f3 f4 f5 d =
  case d of {
   Monday -> f;
   Tuesday -> f0;
   Wednesday -> f1;
   Thursday -> f2;
   Friday -> f3;
   Saturday -> f4;
   Sunday -> f5}

day_rec :: a1 -> a1 -> a1 -> a1 -> a1 -> a1 -> a1 -> Day -> a1
day_rec =
  day_rect

next_weekday :: Day -> Day
next_weekday d =
  case d of {
   Monday -> Tuesday;
   Tuesday -> Wednesday;
   Wednesday -> Thursday;
   Thursday -> Friday;
   _ -> Monday}

prev_weekday :: Day -> Day
prev_weekday d =
  case d of {
   Tuesday -> Monday;
   Wednesday -> Tuesday;
   Thursday -> Wednesday;
   Friday -> Thursday;
   _ -> Friday}