module genericMap

/*
  Genric map definition for assignment 3 in AFP 2018
  Pieter Koopman, pieter@cs.ru.nl
  September 2018
  
  Use StdEnv or iTask environment.
*/

import StdEnv, StdGeneric
import Data.GenEq

generic gMap a b :: a -> b
gMap{|c|} x = x
gMap{|UNIT|} x = x
gMap{|PAIR|}   f g (PAIR x y) = PAIR   (f x) (g y) 
gMap{|EITHER|} f g (LEFT x)   = LEFT   (f x)
gMap{|EITHER|} f g (RIGHT x)  = RIGHT  (g x)
gMap{|CONS|}   f   (CONS x)   = CONS   (f x)
gMap{|OBJECT|} f   (OBJECT x) = OBJECT (f x)

:: Bin a = Leaf | Bin (Bin a) a (Bin a)
t = Bin (Bin Leaf 1 Leaf) 2 (Bin (Bin Leaf 3 Leaf) 4 Leaf)
l = [1..7]

fac 0 = 1
fac n = n * fac (dec n)

derive gMap Bin, [], (,)

Start =
	( gMap{|*->*|} fac t
	, gMap{|*->*|} (\i->(i, fac i)) l
	, gMap{|*->*->*|} (gMap{|*->*|} fac) (gMap{|*->*|} fac) (l, t)
	, gEq{|*|} [1,2] [1,2]
	, gEq{|*|} [1,2] [2,3]
	, gEq{|*->*|} (<) [1,2] [2,3]
	)