--- Towers of Hanoi is a puzzle with three rods and n disks of decreasing size.
--- The disks are stacked on top of each other through the first rod.
--- The aim of the game is to move the stack of disks to another rod while
--- following these rules:
---
--- 1. Only one disk can be moved at a time
---
--- 2. You may only move a disk from the top of one of the stacks to the top of another stack
---
--- 3. No disk may be moved on top of a smaller disk
---
--- The function ;hanoi; computes the sequence of moves to solve puzzle.
module Hanoi;

import Stdlib.Prelude open;

--- Concatenates a list of strings
--- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil;
concat (list : List String) : String := foldl (++str) "" list;

intercalate (sep : String) (xs : List String) : String :=
  concat (intersperse sep xs);

--- Produce a singleton List
singleton {A} (a : A) : List A := a :: nil;

--- Produce a ;String; representation of a ;List Nat;
showList (xs : List Nat) : String :=
  "[" ++str intercalate "," (map natToString xs) ++str "]";

--- A Peg represents a peg in the towers of Hanoi game
type Peg :=
  | left
  | middle
  | right;

showPeg : Peg -> String
  | left := "left"
  | middle := "middle"
  | right := "right";

--- A Move represents a move between pegs
type Move :=
  mkMove@{
    from : Peg;
    to : Peg;
  };

showMove (move : Move) : String :=
  showPeg (Move.from move) ++str " -> " ++str showPeg (Move.to move);

--- Produce a list of ;Move;s that solves the towers of Hanoi game
hanoi : Nat -> Peg -> Peg -> Peg -> List Move
  | zero _ _ _ := nil
  | (suc n) p1 p2 p3 :=
    hanoi n p1 p3 p2 ++ singleton (mkMove p1 p2) ++ hanoi n p3 p2 p1;

main : IO := printStringLn (unlines (map showMove (hanoi 5 left middle right)));