{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Language.LOL.Typing.Type.Synotype where

import Control.Monad (forM)
import Data.Bool
import Data.Eq (Eq(..))
import qualified Data.Foldable as Foldable
import Data.Function (($), (.), id)
import Data.Functor ((<$>))
import qualified Data.Graph as Graph (scc, buildG)
import Data.Int (Int)
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (Maybe(..), fromMaybe, maybe)
import Data.Monoid (Monoid(..), (<>))
import Data.Ord (Ord(..))
import qualified Data.Text as Text
import Data.Text.Buildable (Buildable(..))
import qualified Data.Tree as Tree (flatten)
import Data.Tuple (uncurry)
import Prelude (Num(..), error)
import Text.Show (Show(..), showChar, showParen, showString)

import Language.LOL.Typing.Type.Monotype
import Language.LOL.Typing.Type.Substitution
import Language.LOL.Typing.Lib.Data.Empty (Empty(..))

-- * Type 'Synotype'

-- | An (unordered) collection of /type synonyms/.
data Synotype
 = Synotype
 { synotype_arity    :: Arity
 , synotype_monotype :: [Monotype] -> Monotype
 }
type Synotypes
 = Map Synoname Synotype

type Synoname = Monoconst

-- | An ordering of 'Synotypes'.
type Synotype_Ordering
 = Map Synoname Synotype_Position

-- | A position in a 'Synotype_Ordering'.
type Synotype_Position = Int

-- | 'Synotypes' with a 'Synotype_Ordering'.
data Synotype_Substitution
 =   Synotype_Substitution
 {   synotypes_ordering :: Synotype_Ordering
 ,   synotypes          :: Synotypes
 }
instance Show Synotype_Substitution where
	showsPrec d Synotype_Substitution{synotypes_ordering} =
		showParen (d > 10) $
		showString "Synotype_Substitution" .
		showChar ' ' .
		showChar '[' .
		showString
		 (mconcat $ List.intersperse ", " $
			Text.unpack <$> Map.keys synotypes_ordering) .
		showChar ']'
instance Buildable Synotype_Substitution where
	build Synotype_Substitution{synotypes_ordering} =
		"[" <>
		mconcat (
			List.intersperse ", " $
			build <$> Map.keys
			synotypes_ordering) <>
		"]"

instance Empty Synotype_Substitution where
	empty = Synotype_Substitution
	 { synotypes_ordering = mempty
	 , synotypes          = mempty
	 }

-- | A 'type_String' is a 'type_List' of 'type_Char's
synotype_String :: Synotype_Substitution
synotype_String =
	Synotype_Substitution
	 (Map.singleton "String" 0)
	 (Map.singleton "String" $ Synotype 0 $ \_ -> type_List type_Char)

-- | Return the 'Synotype_Ordering' of given 'Synotypes'
-- along with the mutually recursive 'Synotypes' that are detected.
synorder
 :: Synotypes
 -> (Synotype_Ordering, [[Synoname]])
synorder sys =
	let keys = Map.keys sys in
	let names = Map.fromList $ List.zip keys [0..] in
	let positions = Map.fromList $ List.zip [0..] keys in
	
	let err = error "synorder: error in lookup table" in
	let name_lookup n = fromMaybe err (Map.lookup n names) in
	let pos_lookup  p = fromMaybe err (Map.lookup p positions) in
	
	let edges = Map.foldrWithKey go [] sys
		where
		go s1 (Synotype ari monoty) es =
			Map.foldrWithKey add es $
			monoconsts $ monoty (Monotype_Var <$> [0 .. ari - 1])
			where
			add s2 _ =
				case Map.lookup s2 names of
				 Just i2 -> (:) (i2, i1)
				 Nothing -> id
				where
				i1 = name_lookup s1
	 in
	
	let graph = Graph.buildG (0, Map.size sys - 1) edges in
	let list  = Tree.flatten <$> Graph.scc graph in
	
	let (ordering, recursive, _) =
		List.foldr go (Map.empty, [], 0) list
		where
		go ps (os, rs, counter) =
			case ps of
			 [p] | (p, p) `List.notElem` edges -> -- NOTE: correct type synotype
				( Map.insert (pos_lookup p) counter os
				, rs
				, counter + 1
				)
			 _ ->
				( os
				, (pos_lookup <$> ps) : rs
				, counter
				)
	 in
	(ordering, recursive)

-- | Return whether given 'Synoname'
-- 
is_panthom_synotype :: Synotype_Substitution -> Synoname -> Bool
is_panthom_synotype Synotype_Substitution{synotypes} name =
	case Map.lookup name synotypes of
	 Nothing -> False
	 Just (Synotype ari monoty) ->
		let args = List.take ari [0..] in
		let subvars_ty = subvars $ monoty (Monotype_Var <$> args) in
		Foldable.any (`List.notElem` subvars_ty) args

-- | Fully expand a type in a recursive way.
synexpand :: Synotypes -> Monotype -> Monotype
synexpand sys ty =
	top_expanded `monoapp` (synexpand sys <$> tail)
	where top_expanded `App_Spine` tail =
		app_spine_left $ synexpand_tops sys ty

-- | Fully expand the top-level 'Monotype_Const's.
synexpand_tops :: Synotypes -> Monotype -> Monotype
synexpand_tops sys ty =
	maybe ty (synexpand_tops sys) $
	synexpand_top_step sys ty

{-
-- | Fully expand the top-level 'Monotype_Const'.
synexpand_top :: Synotype_Substitution -> Monotype -> Maybe Monotype
synexpand_top Synotype_Substitution{synotypes} =
	(synexpand_tops synotypes <$>) .
	synexpand_top_step synotypes
-}

-- | Try to expand the top-level 'Monotype_Const' one step.
synexpand_top_step :: Synotypes -> Monotype -> Maybe Monotype
synexpand_top_step sys ty =
	case app_spine_left ty of
	 Monotype_Const c `App_Spine` args ->
		case Map.lookup c sys of
		 Just (Synotype ari monoty)
		  | ari == List.length args -> Just (monoty args)
		  | otherwise -> err "synotype arity mismatch"
		 Nothing -> Nothing
	 _ -> Nothing
	where
		err s = error $ "synexpand_top_step: " <> s

-- | Try to expand the top-level 'Monotype_Const'
-- of one of the two paired 'Monotype's.
--
-- If both top-level 'Monotype_Const' can be expanded one step,
-- then the 'Synotype' which appears first
-- in the 'Synotype_Ordering' is expanded.
synexpand_top_step_ordered
 :: Synotype_Substitution
 -> (Monotype, Monotype)
 -> Maybe (Monotype, Monotype)
synexpand_top_step_ordered
 Synotype_Substitution{synotypes_ordering, synotypes}
 (ty1, ty2) =
	case (position ty1, position ty2) of
	 (Just p1, Just p2) | p1 <= p2  -> Just (expand_top_step ty1, ty2)
	                    | otherwise -> Just (ty1, expand_top_step ty2)
	 (Just _ , Nothing) -> Just (expand_top_step ty1, ty2)
	 (Nothing, Just _ ) -> Just (ty1, expand_top_step ty2)
	 _ -> Nothing
	where
	position ty =
		case app_spine_left ty of
		 Monotype_Const c `App_Spine` _ -> Map.lookup c synotypes_ordering
		 _ -> Nothing
	expand_top_step ty =
		fromMaybe
		 (error "synexpand_top_step_ordered: Synotype_Substitution is invalid")
		 (synexpand_top_step synotypes ty)

-- | Return the /most general type/
-- (i.e. with the least number of expansions).
-- of two 'Monotype's which must be equal
-- under given 'Synotype_Substitution'.
mgt_with_synotypes
 :: Synotype_Substitution
 -> Monotype -> Monotype
 -> Maybe Monotype
mgt_with_synotypes syns t1 t2 =
	case (app_spine_left t1, app_spine_left t2) of
	 (  Monotype_Var v `App_Spine` []
	  , Monotype_Var _ `App_Spine` [] )
	  -> Just $ Monotype_Var v
	 (  Monotype_Const c1 `App_Spine` tail1
	  , Monotype_Const c2 `App_Spine` tail2 )
	  | c1 == c2 && not (is_panthom_synotype syns c1)
	  -> do
		mgts <-
			forM (List.zip tail1 tail2) $ uncurry $
			mgt_with_synotypes syns
		Just (Monotype_Const c1 `monoapp` mgts)
	  | otherwise -> do
		(t1', t2') <- synexpand_top_step_ordered syns (t1, t2)
		mgt_with_synotypes syns t1' t2'
	 _ -> Nothing