module gen

import Control.Applicative
import Control.Monad => qualified join
import Control.Monad.State
import Control.Monad.Writer
:mport Control.Monad.Trans
import Data.Either
import Data.Func
import Data.Functor
import Data.Functor.Identity
import Data.Generics
import Data.List
import Data.Maybe
import Data.Monoid
import Data.Tuple
import StdEnv, StdGeneric
import Text

:: Box b a =: Box b
derive bimap Box
unBox (Box b) :== b
box b :== Box b
reBox x :== box (unBox x)

:: GType
	= GTyBasic String
	| GTyArrow GType GType
	| GTyArray ArrayType GType
	| GTyUList UListType GType
	| GTyUnit
	| GTyEither GType GType
	| GTyPair GType GType
	| GTyCons GenericConsDescriptor GType
	| GTyField GenericFieldDescriptor GType
	| GTyObject GenericTypeDefDescriptor GType
	| GTyRecord GenericRecordDescriptor GType
:: ArrayType = AStrict | ALazy | AUnboxed | A32Unboxed
:: UListType = ULLazy | ULStrict
instance == UListType
where
	(==) ULLazy ULLazy = True
	(==) ULStrict ULStrict = True
	(==) _ _ = False
instance == ArrayType
where
	(==) AStrict AStrict = True
	(==) ALazy ALazy = True
	(==) AUnboxed AUnboxed = True
	(==) A32Unboxed A32Unboxed = True
	(==) _ _ = False

instance == GType where (==) x y = gTypeEqShallow 999 x y
gTypeEqShallow :: Int GType GType -> Bool
gTypeEqShallow i _ _
	| i < 0 = True
gTypeEqShallow _ (GTyBasic i) (GTyBasic j) = i == j
gTypeEqShallow i (GTyArrow l1 r1) (GTyArrow l2 r2) = gTypeEqShallow (dec i) l1 l2 && gTypeEqShallow (dec i) r1 r2
gTypeEqShallow i (GTyArray s1 a1) (GTyArray s2 a2) = s1 == s2 && gTypeEqShallow (dec i) a1 a2
gTypeEqShallow i (GTyUList s1 a1) (GTyUList s2 a2) = s1 == s2 && gTypeEqShallow (dec i) a1 a2
gTypeEqShallow _ GTyUnit GTyUnit = True
gTypeEqShallow i (GTyEither l1 r1) (GTyEither l2 r2) = gTypeEqShallow i l1 l2 && gTypeEqShallow i r1 r2
gTypeEqShallow i (GTyPair l1 r1) (GTyPair l2 r2) = gTypeEqShallow i l1 l2 && gTypeEqShallow i r1 r2
gTypeEqShallow i (GTyCons i1 a1) (GTyCons i2 a2) = i1.gcd_name == i2.gcd_name && gTypeEqShallow i a1 a2
gTypeEqShallow i (GTyField i1 a1) (GTyField i2 a2)
	= i1.gfd_name == i2.gfd_name && i1.gfd_cons.grd_name == i2.gfd_cons.grd_name && gTypeEqShallow i a1 a2
gTypeEqShallow i (GTyObject i1 a1) (GTyObject i2 a2)
	= i1.gtd_name == i2.gtd_name && gTypeEqShallow (dec i) a1 a2
gTypeEqShallow i (GTyRecord i1 a1) (GTyRecord i2 a2)
	= i1.grd_name == i2.grd_name && gTypeEqShallow (dec i) a1 a2
gTypeEqShallow _ _ _ = False

class print a :: a [String] -> [String]
instance print Bool where print s c = [toString s:c]
instance print Int where print s c = [toString s:c]
instance print Char where print s c = [toString s:c]
instance print String where print s c = [s:c]
instance print UListType
where
	print ULStrict c = ["!":c]
	print ULLazy c = c
instance print ArrayType
where
	print AStrict c = ["!":c]
	print AUnboxed c = ["#":c]
	print A32Unboxed c = ["32#":c]
	print ALazy c = c
instance print GType
where
	print (GTyBasic s) c = [s:c]
	print (GTyArrow l r) c = ["((->)":print l [" ":print r [")":c]]]
	print (GTyArray s a) c = ["{":print s $ print a ["}":c]]
	print (GTyUList s a) c = ["[#":print s $ print s ["]":c]]
	print GTyUnit c = ["UNIT":c]
	print (GTyEither l r) c = ["(EITHER ":print l [" ":print r [")":c]]]
	print (GTyPair l r) c = ["(PAIR ":print l [")":c]]
	print (GTyCons i a) c = ["(CONS ", i.gcd_name, " ":print a [")":c]]
	print (GTyField i a) c = ["(FIELD ", i.gfd_name, " ":print a [")":c]]
	print (GTyObject i a) c = ["(OBJECT ", i.gtd_name, " ":print a [")":c]]
	print (GTyRecord i a) c = ["(RECORD ", i.grd_name, " ":print a [")":c]]

:: Type
	= TyBasic String
	| TyArrow Type Type
	| TyArray ArrayType Type
	| TyUList UListType Type
	| TyNewType GenericTypeDefDescriptor GenericConsDescriptor Type
	| TyObject GenericTypeDefDescriptor [(GenericConsDescriptor, [Type])]
	| TyRecord GenericRecordDescriptor [(GenericFieldDescriptor, Type)]
instance == Type
where
	(==) (TyBasic a1) (TyBasic a2) = a1 == a2
	(==) (TyArrow l1 r1) (TyArrow l2 r2) = l1 == l2 && r1 == r2
	(==) (TyArray s1 a1) (TyArray s2 a2) = s1 == s2 && a1 == a2
	(==) (TyUList s1 a1) (TyUList s2 a2) = s1 == s2 && a1 == a2
	(==) (TyNewType i1 j1 a1) (TyNewType i2 j2 a2)
		= i1.gtd_name == i2.gtd_name && a1 == a2
	(==) (TyObject i1 a1) (TyObject i2 a2)
		= i1.gtd_name == i2.gtd_name && length a1 == length a2
		&& and [l1.gcd_name == l2.gcd_name && t1 == t2\\(l1, t1)<-a1 & (l2, t2)<-a2]
	(==) (TyRecord i1 a1) (TyRecord i2 a2)
		= i1.grd_name == i2.grd_name && length a1 == length a2
		&& and [l1.gfd_name == l2.gfd_name && t1 == t2\\(l1, t1)<-a1 & (l2, t2)<-a2]
	(==) _ _ = False

predef :: [(String, String)]
predef =:
	[("_List", "[]"), ("_!List", "[! ]"), ("_List!", "[ !]"), ("_!List!", "[!!]")
	,("_#List", "[#]"), ("_#List!", "[#!]")
	,("_Array", "{}"), ("_!Array", "{!}"), ("_#Array", "{#}")
	:[("_Tuple" +++ toString i, "(" +++ createArray i ',' +++")")\\i<-[2..32]]]

translateType :: String -> String
translateType s = maybe s id $ lookup s predef

instance print Type
where
	print (TyBasic s) c = [translateType s:c]
	print (TyArrow l r) c = print l [" -> ":print r c]
	print (TyArray s a) c = ["{":print s ["}":print a c]]
	print (TyUList s a) c = ["[#":print s ["]":print a c]]
	print (TyNewType i j cons) c = pTyVars i.gtd_name i.gtd_arity
		[": ", j.gcd_name, " ":print (nttype j.gcd_type) c]
	where nttype (GenTypeArrow l r) = l
	print (TyRecord i fields) c = pTyVars i.grd_name i.grd_type_arity
		[" {":isperse ", " (pField (\i c->[i.gfd_name, " :: ":c]) fields i.grd_type) ["}":c]]
	print (TyObject i conses) c = pTyVars i.gtd_name i.gtd_arity
			$ [" ":isperse " | " (map pCons conses) c]
	where
		pCons :: (GenericConsDescriptor, [Type]) [String] -> [String]
		pCons (i, ts) c = n [" ":isperse " " (pField (\_->id) [(i, t)\\t<-ts] i.gcd_type) c]
		where
			n c = case i.gcd_prio of
				GenConsNoPrio = [i.gcd_name:c]
				GenConsPrio a s = ["(",i.gcd_name,") infix",case a of
					GenConsAssocRight = "r";
					GenConsAssocLeft = "l"
					_ = "", " ":print s c]

pTyVars :: String Int [String] -> [String]
pTyVars ty arity c = [":: ", ty, " ":isperse " " (map print ['a'..'a'+toChar (arity-1)]) [" =":c]]

pField :: (a [String] -> [String]) [(a, Type)] GenType -> [[String] -> [String]]
pField pre [] _ = []
pField pre [(i, t):xs] (GenTypeArrow l r) = [pre i o print l:pField pre xs r]

instance == GenType
where
	(==) (GenTypeVar i) (GenTypeVar j) = i == j
	(==) (GenTypeApp l1 r1) (GenTypeApp l2 r2) = l1 == l2 && r1 == r2
	(==) (GenTypeCons i) (GenTypeCons j) = i == j
	(==) (GenTypeArrow l1 r1) (GenTypeArrow l2 r2) = l1 == l2 && r1 == r2
	(==) _ _ = False
instance print GenType
where
	print (GenTypeVar i) c = print (['a'..] !! i) c
	print t=:(GenTypeApp _ _) c = ["(":isperse " " (collectApps t []) [")":c]]
	where
		collectApps (GenTypeApp l r) c = collectApps l [print r:c]
		collectApps a c = [print a:c]
	print (GenTypeCons s) c = [translateType s:c]
	print (GenTypeArrow l r) c = ["(":print l [" -> ":print r [")":c]]]

isperse :: a [[a] -> [a]] [a] -> [a]
isperse s m c = foldr id c $ intersperse (\c->[s:c]) m

gTypeToType :: GType -> Maybe Type
gTypeToType (GTyBasic a) = pure $ TyBasic a
gTypeToType (GTyArrow l r) = TyArrow <$> gTypeToType l <*> gTypeToType r
gTypeToType (GTyArray s a) = TyArray s <$> gTypeToType a
gTypeToType (GTyUList s a) = TyUList s <$> gTypeToType a
gTypeToType (GTyRecord i t) = TyRecord i <$> gtrec t
where
	gtrec (GTyField i t) = (\x->[(i, x)]) <$> gTypeToType t
	gtrec (GTyPair l r) = (++) <$> gtrec l <*> gtrec r
	gtrec _ = Nothing
gTypeToType (GTyObject i t)
	| i.gtd_num_conses == 0 = TyNewType i (hd i.gtd_conses) <$> gTypeToType t
	                        = TyObject i <$> gtobj t
where
	gtobj :: GType -> Maybe [(GenericConsDescriptor, [Type])]
	gtobj (GTyEither l r) = (++) <$> gtobj l <*> gtobj r
	gtobj (GTyCons i a) = (\x->[(i, x)]) <$> gtcons a
	gtobj _ = Nothing
	
	gtcons :: GType -> Maybe [Type]
	gtcons GTyUnit = pure []
	gtcons (GTyPair l r) = (++) <$> gtcons l <*> gtcons r
	gtcons t = (\x->[x]) <$> gTypeToType t

:: FlatMonad :== State FMState GType
:: FMState = { objects :: [String], otypes :: [GType], types :: [GType], depth :: Int}
flattenGType :: GType -> (GType, [GType])
flattenGType ot = appSnd (\x->x.types) $ runState (mkf ot) {objects=[], types=[], otypes=[], depth=10}
where
	write :: (a GType -> GType) a GType -> FlatMonad | genericDescriptorName a
	write cons t a = modify (\x->{x & depth=dec x.depth}) >>| getState >>= \s
		//We have seen the type but it might've had different arguments
		| isMember name s.objects
			//We have not seen this configuration
			| isEmpty [ot \\ ot<-s.otypes | gTypeEqShallow s.depth ot a]
				= mkf a *> r
			//If not, just return the basictype
				= r
		//We have not seen the type so we add, calculate and output it
		= cons t <$ modify (\x->{x & otypes=[a:x.otypes], objects=[name:x.objects]}) <*> mkf a
			>>= \ty->modify (\x->{x & types=[ty:x.types]}) >>| r
	where
		name = genericDescriptorName t
		r = pure $ GTyBasic name

	mkf :: GType -> FlatMonad
	mkf (GTyObject t a) = write GTyObject t a
	mkf (GTyRecord t a) = write GTyRecord t a
	mkf (GTyEither l r) = GTyEither <$> mkf l <*> mkf r
	mkf (GTyPair l r) = GTyPair <$> mkf l <*> mkf r
	mkf (GTyCons i a) = GTyCons i <$> mkf a
	mkf (GTyField i a) = GTyField i <$> mkf a
	mkf (GTyArrow l r) = GTyArrow <$> mkf l <*> mkf r
	mkf (GTyArray s a) = GTyArray s <$> mkf a
	mkf (GTyUList s a) = GTyUList s <$> mkf a
	mkf GTyUnit = pure GTyUnit
	mkf a=:(GTyBasic _) = pure a

generic type a :: Box GType a
type{|Int|} = box $ GTyBasic "Int"
type{|Bool|} = box $ GTyBasic "Bool"
type{|Real|} = box $ GTyBasic "Real"
type{|Char|} = box $ GTyBasic "Char"
type{|World|} = box $ GTyBasic "World"
type{|Dynamic|} = box $ GTyBasic "Dynamic"
type{|(->)|} l r = box $ GTyArrow (unBox l) (unBox r)
type{|[#]|} a = box $ GTyUList ULLazy $ unBox a
type{|[#!]|} a = box $ GTyUList ULStrict $ unBox a
type{|{}|} a = box $ GTyArray ALazy $ unBox a
type{|{!}|} a = box $ GTyArray AStrict $ unBox a
type{|{#}|} a = box $ GTyArray AUnboxed $ unBox a
type{|{32#}|} a = box $ GTyArray A32Unboxed $ unBox a

type{|UNIT|} = box GTyUnit
type{|EITHER|} l r = box $ GTyEither (unBox l) (unBox r)
type{|PAIR|} l r = box $ GTyPair (unBox l) (unBox r)
type{|CONS of gcd|} a = box $ GTyCons gcd $ unBox a
type{|FIELD of gfd|} a = box $ GTyField gfd $ unBox a
type{|OBJECT of gtd|} a = box $ GTyObject gtd $ unBox a
type{|RECORD of grd|} a = box $ GTyRecord grd $ unBox a

derive type ?#, ?, ?^
derive type [], [! ], [ !], [!!]
derive type (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
derive type Either, Maybe, T, R, Frac, Tr, Fix

:: T a =: T2 a
:: R a = {f1 :: Maybe (R a), f2 :: Bool, f3 :: T a, f4 :: Char -> Dynamic,
	f5 :: [[([#Int], [#Int!], [!Int!], [!Int], [Int!], {!Int}, {R Bool}, {#Char})]]/*({!Int}, {#Char}, {R Bool})*/}

:: Tr m b= Tr (m Int b)

:: Frac a = (/.) infixl 7 a a 

//Start :: [String]
//Start = foldr (\i c->print i ["\n":c]) [] $ catMaybes $ map gTypeToType $ flattenGType $ unBox t
Start = foldr (\i c->print i ["\n":c]) []
	$ catMaybes
	$ map gTypeToType
	$ snd $ flattenGType
	$ unBox t

:: Fix f = Fix (f (Fix f))

//t :: Box GType (?# Int)
//t :: Box GType (Maybe [Maybe (Either Bool String)])
//t :: Box GType [Either [[!Int]] [[![Bool]]]]
t :: Box GType ([Either (R (T *World)) (Frac Real)], Tr Either Bool, Fix Maybe)
t = type{|*|}