module dsl

import StdEnv

import Data.Func => qualified app
import Data.Functor
import Data.Either
import Data.GenEq
import Data.Functor.Identity
import Control.Applicative
import Control.Monad => qualified join
import Text

import Text.Parsers.Simple.Core

class Symantics v where
	int  :: Int -> v Int
	bool :: Bool -> v Bool
	lam  :: ((v a) -> v b) -> v (a -> b)
	app  :: (v (a -> b)) (v a) -> v b
	Fix  :: ((v a) -> (v a)) -> v a
	add  :: (v a) (v a) -> v a | + a
	mul  :: (v a) (v a) -> v a | * a
	leq  :: (v a) (v a) -> v Bool | Ord a
	If   :: (v Bool) (v a) (v a) -> v a

//Run the object
:: Run a = Run a
runRun (Run a) = a
instance Functor Run where fmap f a = Run $ f $ runRun a
instance pure Run where pure a = Run a
instance <*> Run where <*> a b = Run $ runRun a $ runRun b
instance Symantics Run where
	int a    = pure a
	bool a   = pure a
	lam f    = pure $ runRun o f o Run
	app f a  = f <*> a
	Fix f    = pure $ let x = runRun $ f $ pure x in x
	add a b  = (+) <$> a <*> b
	mul a b  = (*) <$> a <*> b
	leq a b  = (<=) <$> a <*> b
	If i t e = if` <$> i <*> t <*> e

//Length of the object
:: Length a = Length Int
runLength (Length i) = i
(+.) infixl 6
(+.) (Length a) (Length b) = Length $ a + b
instance one (Length a) where one = Length 1
instance zero (Length a) where zero = Length 0
instance Symantics Length where
	int _    = one
	bool _   = one
	lam f    = f zero +. one
	app f a  = f +. a +. one
	Fix f    = f zero +. one
	add a b  = a +. b +. one
	mul a b  = a +. b +. one
	leq a b  = a +. b +. one
	If i t e = i +. t +. e +. one

//Print the object
:: Print a = Print (Int [String] -> [String])
runPrint (Print a) = a
print a = concat $ runPrint a 0 []
var i = "v" +++ toString i
show a = Print \_ c->[toString a:c]
binop op (Print a) (Print b) = Print \i c->["(":a i [op: b i [")":c]]]
instance Symantics Print where
	int a    = show a
	bool a   = show a
	lam f    = Print \i c->["(\\", var i, ".":runPrint (f $ show $ var i) (i+1) [")":c]]
	app f a  = Print \i c->["(":runPrint f i [" ":runPrint a i [")":c]]]
	Fix f    = Print \i c->["fix (\\","self.":runPrint (f $ show "self") (i+1) [")":c]]
	add a b  = binop "+" a b
	mul a b  = binop "*" a b
	leq a b  = binop "<=" a b
	If p t e = Print \i c->["if ":runPrint p i [" then ":runPrint t i [" else ":runPrint e i c]]]

//Parsing
:: Token = IntToken Int | BoolToken Bool | BrackOpenToken | BrackCloseToken | LeqToken | AddToken | MulToken | IfToken
derive gEq Token
instance == Token where == a b = a === b

lex :: [Char] -> Either [String] [Token]
lex [] = Right []
lex [')':cs] = clex cs BrackCloseToken
lex ['(':cs] = clex cs BrackOpenToken
lex ['<=':cs] = clex cs LeqToken
lex ['+':cs] = clex cs AddToken
lex ['*':cs] = clex cs MulToken
lex ['True':cs] = clex cs $ BoolToken True
lex ['False':cs] = clex cs $ BoolToken False
lex ['-',c:cs]
	| isDigit c = lex [c:cs] >>= \v->case v of
		[IntToken i:rest] = Right [IntToken (~i):rest]
		x = pure x
lex [c:cs]
	| isSpace c = lex cs
	| isDigit c
		# (d, cs) = span isDigit [c:cs]
		= clex cs $ IntToken $ toInt $ toString d
	= Left ["Unexpected: " +++ toString c +++ " ord: " +++ toString (toInt c)]

clex :: [Char] Token -> Either [String] [Token]
clex cs t = (\ts->[t:ts]) <$> lex cs

class parseSym a where
	parseSym :: Parser Token (v a) | Symantics v
instance parseSym Int where
	parseSym
		=   flip pChainl1 (add <$ pToken AddToken)
		$   flip pChainl1 (mul <$ pToken MulToken)
		$   pToken BrackOpenToken *> parseSym <* pToken BrackCloseToken
		<|> If <$ pToken IfToken <*> parseSym <*> parseSym <*> parseSym
		<|> int <$> pInt
	where
		pInt = pSatisfy (\t->t=:(IntToken _)) >>= \(IntToken i)->pure i
instance parseSym Bool where
	parseSym
		=   leq <$> parseSymInt <* pToken LeqToken <*> parseSymInt
		<|> If <$ pToken IfToken <*> parseSym <*> parseSym <*> parseSym
		<|> pToken BrackOpenToken *> parseSym <* pToken BrackCloseToken
		<|> bool <$> pBool
	where
		pBool = pSatisfy (\t->t=:(BoolToken _)) >>= \(BoolToken b)->pure b

		parseSymInt :: Parser Token (v Int) | Symantics v
		parseSymInt = parseSym

Start = print <$> exp
where
	exp :: Either [String] (v Bool) | Symantics v
	exp = lex (fromString inp) >>= parse parseSym

	inp = "1+2*3 <= 42*42"
//Start =
//	[ toString $ runRun fourtytwo
//	, print fourtytwo
//	, toString $ runRun true
//	, print true
//	, toString $ runRun powfix33
//	, print powfix33
//	, toString $ runRun factfix5
//	, print factfix5
//	]

fourtytwo :: v Int | Symantics v
fourtytwo = add (int 38) (int 4)

true :: v Bool | Symantics v
true = app (lam (\x->x)) (bool True)

powfix = lam \x->Fix \self->lam \n->
	If (leq n (int 0)) (int 1)
		(mul x (app self (add n (int -1))))

powfix33 = app (app powfix (int 3)) (int 3)

factfix = Fix \self->lam \n->
	If (leq n (int 0)) (int 1)
		(mul n (app self (add n (int -1))))

factfix5 = app factfix (int 5)