{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module Cube where

import Prelude hiding (pi)
import Exponential

data Sort = Star | Box deriving (Eq,Show,Read)
data F a = Lam a (a -> a) 
	 | Pi a (a -> a)
	 | App a a
	 | Sort Sort

instance ExpFunctor F where
	xmap f g (Lam t k) = Lam (f t) (f . k . g)
	xmap f g (Pi t k) = Pi (f t) (f . k . g)
	xmap f g (App a b) = App (f a) (f b)
	xmap f g (Sort k) = Sort k

instance Show (F a) where
	show (Lam a f) = "(LAM ...)"
	show (Pi a f) = "(PI ...)"
	show (App a b) = "(APP ...)"
	show (Sort Star) = "*"
	show (Sort Box) = "#"

lam :: Rollable F t => t -> (t -> t) -> t
lam t f = roll (Lam t f)

pi :: Rollable F t => t -> (t -> t) -> t
pi t f = roll (Pi t f)

app :: Rollable F t => t -> t -> t
app f a = roll (App f a)

star :: Rollable F t => t
star = roll (Sort Star)

box :: Rollable F t => t
box = roll (Sort Box)

-- Washburn/Weirich
safe :: (forall a. Elim F a) -> ForAll (Elim F)
safe = ForAll

-- Fegaras/Sheard
unsafe :: (forall a. Rec F a) -> ForAll (Rec F)
unsafe = ForAll

instance Cata F (ForAll t) => Show (ForAll t) where 
	show x = cata phi x vars where
		phi :: F ([String] -> String) -> [String] -> String
		phi (Lam t f) (v:vars) = "(lam " ++ v ++ " : " ++ t vars ++ ". " ++ f (const v) vars ++ ")"
		phi (Pi t f) (v:vars) = "(pi " ++ v ++ " : " ++ t vars ++ ". " ++ f (const v) vars ++ ")"
		phi (App a b) vars = "(" ++ a vars ++ " " ++ b vars ++ ")"
		phi (Sort Star) vars = "*"
		phi (Sort Box) vars = "#"
		vars :: [String] 
		vars = [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1..], i <- ['a'..'z'] ]

-- polymorphic identity function
example_id :: Rollable F t => t
example_id = lam star $ \a -> lam a id

example_church_true :: Rollable F t => t
example_church_true  = lam star $ \a -> lam a $ \x -> lam a $ \y -> x

example_church_false :: Rollable F t => t
example_church_false = lam star $ \a -> lam a $ \x -> lam a $ \y -> y

-- cheezy pseudo alpha-equality until I define something better
instance Cata F (ForAll t) => Eq (ForAll t) where a == b = show a == show b

countBoundVars :: Cata F t => t -> Int
countBoundVars = cata phi where
	phi (Lam t f) = t + f 1
	phi (Pi t f) = t + f 1
	phi (Sort k) = 0
	phi (App a b) = a + b

-- a rather traditional evaluator, non-catamorphic, I don't seem to be able to derive this in the Weirich/Washburn setting.
-- maybe I am missing something, but it appears that this needs a paramorphism, and I can't build paramorphisms with just xmap!
eval :: (Unrollable F t, Rollable F t) => t -> t
eval x = case unroll x of 
	Lam t k -> lam t k
	Pi t k -> pi t k
	Sort Star -> star
	Sort Box -> box
	App f a -> 
		let f' = eval f in case unroll f' of
		Lam t k -> k a
		_ 	-> app f' a