{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Language.LOL.Typing.Type.Monotype where

import Data.Bool
import Data.Either (Either(..), either)
import Data.Eq (Eq(..))
import Data.Function (($), (.), id)
import Data.Functor (Functor(..), (<$>))
import Data.Int (Int)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (Maybe(..), maybe, isNothing)
import Data.Monoid (Monoid(..), (<>))
import Data.Ord (Ord(..))
import Data.String (IsString(..))
import Data.Text (Text)
import Data.Text.Buildable (Buildable(..))
import Prelude (Num(..))
import Text.Read (read)
import Text.Show (Show(..))
import qualified Data.Char as Char
import qualified Data.Foldable as Foldable
import qualified Data.List as List
import qualified Data.Text as Text

import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build

-- * Type 'Monotype'

-- | A /monomorphic type/ (aka. /monotype/).
--
-- NOTE: all 'Monotype's that can be constructed are NOT necessarily well-formed.
--
-- NOTE: however, a useful typing of this type language
-- is added by separating 'Monotype', 'Polytype' and 'Polytyref'
-- in order to indicate where to expect a 'Polyvar' or a 'Polytyref_Var'.
data Monotype
 =   Monotype_App   Monotype Monotype -- ^ /binary type application/
 |   Monotype_Const Monoconst         -- ^ /type constant/
 |   Monotype_Var   Monovar           -- ^ /type variable/
 deriving (Eq, Ord, Show)

instance Buildable Monotype where
	build = build . (precedence_Toplevel,)
instance Buildable (Precedence, Monotype) where
	build (prec, typ)
	 | prec >= precedence typ = Build.parens (go typ)
	 | otherwise              = go typ
		where
		go ty =
			case app_spine_left ty of
			 Monotype_Var v `App_Spine` [] -> "m" <> build v
			 Monotype_Const c `App_Spine` [] -> build c
			 Monotype_Const "->" `App_Spine` [t1, t2] ->
				build (precedence_Fun, t1) <>
				" -> " <>
				build (precedence_previous precedence_Fun, t2)
			 Monotype_Const "[]" `App_Spine` [t1] ->
				"[" <> build t1 <> "]"
			 Monotype_Const (is_Tuple -> True) `App_Spine` tys ->
				Build.tuple (build <$> tys)
			 t `App_Spine` tys ->
				mconcat $ List.intersperse " " $
				(build . (precedence_App,)) <$> (t : tys)
instance IsString Monotype where
	fromString = Monotype_Const . fromString

-- * Type 'Precedence'

-- | A /binding precedence/ for an operator.
newtype Precedence
 =      Precedence Int
 deriving (Eq, Ord, Show)

-- ** Class 'Has_Precedence'

class Has_Precedence a where
	precedence :: a -> Precedence
instance Has_Precedence Monotype where
	precedence ty =
		case app_spine_left ty of
		 Monotype_Const "->" `App_Spine` [_, _] -> precedence_Fun
		 Monotype_Const "[]" `App_Spine` [_] -> precedence_Atomic
		 Monotype_Const (is_Tuple -> True) `App_Spine` _ -> precedence_Atomic
		 _ `App_Spine` [] -> precedence_Atomic
		 _ -> precedence_App

precedence_previous :: Precedence -> Precedence
precedence_previous (Precedence p) = Precedence (p - 1)

-- ** Convenient 'Precedence's
precedence_Toplevel :: Precedence
precedence_Toplevel =  Precedence 0
precedence_Fun :: Precedence
precedence_Fun =  Precedence 1
precedence_App :: Precedence
precedence_App =  Precedence 2
precedence_Atomic :: Precedence
precedence_Atomic =  Precedence 3

-- ** Type 'Monoconst'

-- | A /type constant/.
type Monoconst = Text

-- ** Type 'Monoconsts'

-- | A context of 'Monoconst's, without duplicates.
type Monoconsts = Map Monoconst ()

-- *** Class 'Has_Monoconsts'

-- | Return the 'Monoconst's of a 'Monotype', without duplicates.
class Has_Monoconsts a where
	monoconsts :: a -> Monoconsts

instance Has_Monoconsts Monotype where
	monoconsts ty =
		case ty of
		 Monotype_Var _ -> Map.empty
		 Monotype_Const c -> Map.singleton c ()
		 Monotype_App t1 t2 -> monoconsts t1 `Map.union` monoconsts t2

{-
-- | Return the 'Monoconst's of a 'Has_Monotypes' instance, without duplicates.
monoconsts_from :: Has_Monotypes a => a -> [Monoconst]
monoconsts_from =
	List.nub . List.concatMap go . monotypes
	where
	go (Monotype_Var _) = []
	go (Monotype_Const c) = [c]
	go (Monotype_App t1 t2) = go t1 `List.union` go t2
-}

-- | Infinite list of unique 'Monoconst's:
-- @a, b, .., z, a1, b1 .., z1, a2, ..@
const_pool :: [Monoconst]
const_pool =
	[ Text.singleton n
	| n <- ['a'..'z']
	] <>
	[ Text.pack (n:show i)
	| n <- ['a'..'z']
	, i <- [1 :: Int ..]
	]

-- | Return given 'Monoconst' renamed a bit to avoid
-- conflicting with any given 'Monoconst's.
const_freshify
 :: Monoconsts
 -> Monoconst
 -> (Monoconsts, Monoconst)
const_freshify consts_used const =
	let ints = [1..] :: [Int] in
	let fresh_const =
		List.head
		 [ x
		 | extra <- "" : (show <$> ints)
		 , x <- [const <> Text.pack extra]
		 , isNothing (Map.lookup x consts_used)
		 ] in
	( Map.insert fresh_const () consts_used
	, fresh_const )

-- | Return given 'Monotype'
-- with all its 'Monotype_Var's
-- turned into 'Monotype_Const's.
--
-- NOTE: each 'Monovar' being mapped to a 'Monoconst'
-- prefixing by an underscore ('_')
-- the 'show'ed 'Int' of the 'Monovar'.
constify :: Monotype -> Monotype
constify ty =
	case ty of
	 Monotype_Var v   -> Monotype_Const $ Text.pack ('_':show v)
	 Monotype_Const s -> Monotype_Const s
	 Monotype_App l r -> Monotype_App (constify l) (constify r)

-- | Return given 'Monotype'
-- with all previously 'constify'ed 'Monovar's
-- turned back into 'Monotype_Var's.
unconstify :: Monotype -> Monotype
unconstify ty =
	case ty of
	 Monotype_Var v -> Monotype_Var v
	 Monotype_Const (Text.uncons -> Just ('_', c))
	  | not (Text.null c)
	  && Text.all Char.isDigit c ->
		Monotype_Var (read $ Text.unpack c)
	 Monotype_Const c -> Monotype_Const c
	 Monotype_App l r -> Monotype_App
		 (unconstify l)
		 (unconstify r)

-- *** Useful 'Monoconst's

type_Bool   :: Monotype
type_Bool    = Monotype_Const "Bool"
type_Char   :: Monotype
type_Char    = Monotype_Const "Char"
type_Float  :: Monotype
type_Float   = Monotype_Const "Float"
type_Int    :: Monotype
type_Int     = Monotype_Const "Int"
type_String :: Monotype
type_String  = Monotype_Const "String"

-- | Constructs a function 'Monotype' from one 'Monotype' to another.
type_Fun :: Monotype -> Monotype -> Monotype
type_Fun t1 = Monotype_App (Monotype_App (Monotype_Const "->") t1)

-- | Right associative alias for 'type_Fun'.
(.->.) :: Monotype -> Monotype -> Monotype
(.->.) = type_Fun
infixr 0 .->.

-- | For instance, @(type_List type_Int)@ represents @[Int]@
type_List :: Monotype -> Monotype
type_List = Monotype_App (Monotype_Const "[]")

-- | For instance, @(type_IO type_Bool)@ represents @(IO Bool)@
type_IO :: Monotype -> Monotype
type_IO = Monotype_App (Monotype_Const "IO")

-- | A carthesian product of zero or more 'Monotype'.
-- For instance @(type_Tuple [])@ represents @()@,
-- and @(type_Tuple [type_Char, type_String])@ represents @(Char, String)@.
type_Tuple :: [Monotype] -> Monotype
type_Tuple tys = List.foldl Monotype_App (Monotype_Const name) tys
	where
	name | Foldable.null tys  = "()"
	     | otherwise = Text.pack $ "("<>List.replicate (List.length tys - 1) ','<>")"

-- | The unit type. A special instance of 'type_Tuple'.
type_Unit :: Monotype
type_Unit = type_Tuple []

-- ** Type 'Monovar'

-- | A /monomorphic type variable/:
-- a place-holder for a 'Monotype' that is not yet known,
-- but that become available at some time during 'Constraint' solving.
type Monovar = Int

-- | Return the list of 'Monovar's of a 'Monotype', without duplicates.
monovars :: Monotype -> [Monovar]
monovars ty =
	case ty of
	 Monotype_Var v -> [v]
	 Monotype_Const _ -> []
	 Monotype_App t1 t2 -> monovars t1 `List.union` monovars t2

-- * Type 'App'

-- | A /binary 'Monotype' application/.
type App = Monotype -> Monotype -> Monotype

-- | Left associative alias for 'Monotype_App'.
(.!.) :: Monotype -> Monotype -> Monotype
(.!.) = Monotype_App
infixl 5 .!.

-- | 'Monotype_App'ly given 'Monotype's to given 'Monotype'.
monoapp :: Monotype -> [Monotype] -> Monotype
monoapp = List.foldl Monotype_App

-- ** Type 'App_Spine'

-- | A /application spine/ of a 'Monotype'.
data App_Spine
 =   App_Spine
 {   app_spine_end :: Monotype
 ,   app_spine     :: [Monotype]
 }

-- | Return the /left 'App_Spine'/ of a 'Monotype_App'.
--
-- EXAMPLE: if type @t@ is @Either Bool [Int]@,
-- then @app_spine_left t@ is @(Either, [Bool, [Int]])@.
app_spine_left :: Monotype -> App_Spine
app_spine_left = go []
	where
	go tys (Monotype_App t1 t2) = go (t2:tys) t1
	go tys ty = App_Spine ty tys

-- | Return the /right 'App_Spine'/ of a 'Monotype'.
--
-- EXAMPLE: if type @t@ is @Int -> (Bool -> String)@,
-- then @app_spine_right t@ is @([Int, Bool], String)@.
app_spine_right :: Monotype -> App_Spine
app_spine_right = go []
	where
	go tys (Monotype_App (Monotype_App (Monotype_Const "->") t1) t2) = go (t1:tys) t2
	go tys ty = App_Spine ty (List.reverse tys)

-- | Return the /right 'App_Spine'/ of a 'Monotype' upto a maximal length.
app_spine_right_upto :: Int -> Monotype -> App_Spine
app_spine_right_upto maxlen ty =
	let a `App_Spine` as = app_spine_right ty in
	let (bs, cs) = List.splitAt maxlen as in
	List.foldr (.->.) a cs `App_Spine` bs

-- ** Type 'Arity'

-- | The /arity of a 'Monotype'/,
-- i.e. the total number of expected arguments of a 'Monotype'.
type Arity = Int

-- | Return the 'Arity' of a 'Monotype'.
type_arity :: Monotype -> Arity
type_arity = List.length . app_spine . app_spine_right

-- * 'Monotype' predicates
is_Var :: Monotype -> Bool
is_Var (Monotype_Var _) = True
is_Var _ = False

is_Const :: Monotype -> Bool
is_Const (Monotype_Const _) = True
is_Const _ = False

is_App :: Monotype -> Bool
is_App (Monotype_App _ _) = True
is_App _ = False

is_Fun :: Monotype -> Bool
is_Fun (Monotype_App (Monotype_App (Monotype_Const "->") _) _) = True
is_Fun _ = False

is_Tuple :: Monoconst -> Bool
is_Tuple (Text.uncons -> Just ('(', t))
 | Text.null t = False
 | otherwise   = Text.all (',' ==) (Text.init t) && Text.last t == ')'
is_Tuple _ = False

is_IO :: Monotype -> Bool
is_IO (Monotype_App (Monotype_Const "IO") _) = True
is_IO _ = False

-- * Class 'Has_Monotypes'

class Has_Monotypes a where
	monotypes :: a -> [Monotype]
	monotypes_map :: (Monotype -> Monotype) -> a -> a

instance Has_Monotypes Monotype where
	monotypes ty = [ty]
	monotypes_map = ($)
instance Has_Monotypes a => Has_Monotypes [a] where
	monotypes = List.concatMap monotypes
	monotypes_map f = (monotypes_map f <$>)
instance Has_Monotypes a => Has_Monotypes (Maybe a) where
	monotypes = maybe [] monotypes
	monotypes_map = fmap . monotypes_map
instance (Has_Monotypes a, Has_Monotypes b) => Has_Monotypes (Either a b) where
	monotypes  = either monotypes monotypes
	monotypes_map f = either (Left . monotypes_map f) (Right . monotypes_map f)

-- ** Class 'Monotypeable'

-- | A type class to convert something into a 'Monotype'
class Monotypeable a where
	monotype :: a -> Monotype
instance Monotypeable Monotype where
	monotype = id
instance Monotypeable Monovar where
	monotype = Monotype_Var
instance Monotypeable Monoconst where
	monotype = Monotype_Const