mbrcknl

{-# LANGUAGE ScopedTypeVariables #-}

-- | Solve the r-peg Towers of Hanoi puzzle, using the Frame-Stewart algorithm.

module Hanoi where

import Prelude
  ( Bool(..), Int, Integer, Integral, Eq(..), Ord(..), Ordering(..)
  , error, fst, length, map, otherwise, snd, (+), (++), (-), (*), ($)
  , minimum, head, last

mbrcknl

-- Matthew Brecknell @mbrcknl
-- BFPG.org, March 2015

open import Agda.Primitive using (_⊔_)

postulate
  String : Set

{-# BUILTIN STRING String #-}

mbrcknl

Definition red_split_a {red: red_type} {e: aexp} (ret: red_cexp red a e): red_aexp red e :=
  match ret in red_cexp _ t e return
        (match t return exp_type t -> Type with
           | a => fun e' => red_aexp red e'
           | b => fun _  => unit
         end e)
  with
    | RCNum       n     => RANum   n
    | RCPlus  _ _ a1 a2 => RAPlus  a1 a2
    | RCMinus _ _ a1 a2 => RAMinus a1 a2

mbrcknl

-- Matthew Brecknell @mbrcknl
-- BFPG.org, March-April 2015

-- With thanks to Conor McBride (@pigworker) for his lecture series:
-- https://www.youtube.com/playlist?list=PL44F162A8B8CB7C87
-- from which I learned most of what I know about Agda, and
-- from which I stole several ideas for this talk.

open import Agda.Primitive using (_⊔_)

mbrcknl

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}

import qualified Data.Map as M
import Control.Applicative as A

newtype JObject = JObject (M.Map String Json)
newtype JList = JList [Json]

data Json

mbrcknl

Fixpoint R (T:ty) (t:tm) {struct T} : Prop :=
  has_type empty t T /\ halts t /\
  match T with
    | TBool  => True
    | TArrow T1 T2 => (forall s, R T1 s -> R T2 (tapp t s))
    | TProd T1 T2 => R T1 (tfst t) /\ R T2 (tsnd t)
  end.

mbrcknl

Fixpoint R (T:ty) (t:tm) {struct T} : Prop :=
  has_type empty t T /\ halts t /\
  match T with
    | TBool  => True
    | TArrow T1 T2 => (forall s, R T1 s -> R T2 (tapp t s))
    | TProd T1 T2 => exists t1, exists t2, t ==>* tpair t1 t2 /\ R T1 t1 /\ R T2 t2
  end.

mbrcknl

Require Import List.

Inductive type : Type :=
| base : type
| arr  : type -> type -> type.

Infix "==>" := arr (right associativity, at level 52).

Inductive elem {A: Type} (x: A): list A -> Type :=
| here  : forall xs, elem x (x :: xs)

mbrcknl

Require Import Sorted.
Require Import Permutation.

Definition isSortingFunction (A: Type) (R: A -> A -> Prop) (f: list A -> list A): Prop :=
  forall (xs: list A), Permutation xs (f xs) /\ Sorted R (f xs).

Check (isSortingFunction: forall (A: Type), (A -> A -> Prop) -> (list A -> list A) -> Prop).

mbrcknl

Require Import List.

Inductive type : Type :=
| base : type
| arr  : type -> type -> type.

Infix "==>" := arr (right associativity, at level 52).

Inductive elem {A: Type} (x: A): list A -> Type :=
| here  : forall xs, elem x (x :: xs)