module Facet.Core.Type
( -- * Kinds
  Kind(..)
  -- * Types
, Interface(..)
, Signature(..)
, fromInterfaces
, singleton
, interfaces
, mapSignature
, Type(..)
, global
, free
, metavar
, unNeutral
, unComp
, Classifier(..)
, classifierType
, occursIn
  -- ** Elimination
, ($$)
, ($$*)
  -- * Type expressions
, TExpr(..)
  -- * Quotation
, quote
, eval
, apply
) where

import           Control.Effect.Empty
import           Data.Foldable (foldl')
import           Data.Function (on, (&))
import           Data.Maybe (fromMaybe)
import qualified Data.Set as Set
import           Facet.Core.Pattern
import           Facet.Env hiding (empty)
import           Facet.Name
import           Facet.Snoc
import           Facet.Subst
import           Facet.Syntax
import           Facet.Usage hiding (singleton)
import           GHC.Stack
import           Prelude hiding (lookup)

-- Kinds

data Kind
  = KType
  | KInterface
  | KArrow (Maybe Name) Kind Kind
  deriving (Eq, Ord, Show)


-- Types

data Interface a = Interface RName (Snoc a)
  deriving (Eq, Foldable, Functor, Ord, Show, Traversable)

newtype Signature a = Signature { getSignature :: Set.Set (Interface a) }
  deriving (Eq, Foldable, Monoid, Ord, Semigroup, Show)

fromInterfaces :: Ord a => [Interface a] -> Signature a
fromInterfaces = Signature . Set.fromList

singleton :: Interface a -> Signature a
singleton = Signature . Set.singleton

interfaces :: Signature a -> [Interface a]
interfaces = Set.toList . getSignature

mapSignature :: Ord b => (a -> b) -> Signature a -> Signature b
mapSignature f = Signature . Set.map (fmap f) . getSignature


data Type
  = VString
  | VForAll Name Kind (Type -> Type)
  | VArrow (Maybe Name) Quantity Type Type
  | VNe (Var (Either Meta (LName Level))) (Snoc Type)
  | VComp (Signature Type) Type

instance Eq Type where
  (==) = (==) `on` quote 0

instance Ord Type where
  compare = compare `on` quote 0


global :: RName -> Type
global = var . Global

free :: LName Level -> Type
free = var . Free . Right

metavar :: Meta -> Type
metavar = var . Free . Left


var :: Var (Either Meta (LName Level)) -> Type
var v = VNe v Nil


unNeutral :: Has Empty sig m => Type -> m (Var (Either Meta (LName Level)), Snoc Type)
unNeutral = \case
  VNe h sp -> pure (h, sp)
  _        -> empty

unComp :: Has Empty sig m => Type -> m (Signature Type, Type)
unComp = \case
  VComp sig _T -> pure (sig, _T)
  _T           -> empty


data Classifier
  = CK Kind
  | CT Type

classifierType :: Classifier -> Maybe Type
classifierType = \case
  CK _K -> empty
  CT _T -> pure _T


occursIn :: Meta -> Level -> Type -> Bool
occursIn p = go
  where
  go d = \case
    VForAll n _ b  -> go (succ d) (b (free (LName d n)))
    VArrow _ _ a b -> go d a || go d b
    VComp s t      -> any (go d) s || go d t
    VNe h sp       -> any (either (== p) (const False)) h || any (go d) sp
    VString        -> False


-- Elimination

($$) :: HasCallStack => Type -> Type -> Type
VNe h es $$ a = VNe h (es :> a)
_        $$ _ = error "can’t apply non-neutral/forall type"

($$*) :: (HasCallStack, Foldable t) => Type -> t Type -> Type
($$*) = foldl' ($$)

infixl 9 $$, $$*


-- Type expressions

data TExpr
  = TString
  | TVar (Var (Either Meta (LName Index)))
  | TForAll Name Kind TExpr
  | TArrow (Maybe Name) Quantity TExpr TExpr
  | TComp (Signature TExpr) TExpr
  | TApp TExpr TExpr
  deriving (Eq, Ord, Show)


-- Quotation

quote :: Level -> Type -> TExpr
quote d = \case
  VString        -> TString
  VForAll n t b  -> TForAll n t (quote (succ d) (b (free (LName d n))))
  VArrow n q a b -> TArrow n q (quote d a) (quote d b)
  VComp s t      -> TComp (mapSignature (quote d) s) (quote d t)
  VNe n sp       -> foldl' (&) (TVar (fmap (fmap (levelToIndex d)) <$> n)) (flip TApp . quote d <$> sp)

eval :: HasCallStack => Subst Type -> Env Type -> TExpr -> Type
eval subst = go where
  go env = \case
    TString               -> VString
    TVar (Global n)       -> global n
    TVar (Free (Right n)) -> index env n
    TVar (Free (Left m))  -> fromMaybe (metavar m) (lookupMeta m subst)
    TForAll n t b         -> VForAll n t (\ _T -> go (env |> pvar (n :=: _T)) b)
    TArrow n q a b        -> VArrow n q (go env a) (go env b)
    TComp s t             -> VComp (mapSignature (go env) s) (go env t)
    TApp  f a             -> go env f $$  go env a

apply :: HasCallStack => Subst Type -> Env Type -> Type -> Type
apply subst env = eval subst env . quote (level env)

 * Kinds
 * Types
 ** Elimination
 * Type expressions
 * Quotation
 Kinds
 Types
 Elimination
 Type expressions
 Quotation
module Facet.Core.Type
  Kind(..)
, Interface(..)
, Signature(..)
, fromInterfaces
, singleton
, interfaces
, mapSignature
, Type(..)
, global
, free
, metavar
, unNeutral
, unComp
, Classifier(..)
, classifierType
, occursIn
, ($$)
, ($$*)
, TExpr(..)
, quote
, eval
, apply
) where

import           Control.Effect.Empty
import           Data.Foldable (foldl')
import           Data.Function (on, (&))
import           Data.Maybe (fromMaybe)
import qualified Data.Set as Set
import           Facet.Core.Pattern
import           Facet.Env hiding (empty)
import           Facet.Name
import           Facet.Snoc
import           Facet.Subst
import           Facet.Syntax
import           Facet.Usage hiding (singleton)
import           GHC.Stack
import           Prelude hiding (lookup)


data Kind
  = KType
  | KInterface
  | KArrow (Maybe Name) Kind Kind
  deriving (Eq, Ord, Show)



data Interface a = Interface RName (Snoc a)
  deriving (Eq, Foldable, Functor, Ord, Show, Traversable)

newtype Signature a = Signature { getSignature :: Set.Set (Interface a) }
  deriving (Eq, Foldable, Monoid, Ord, Semigroup, Show)

fromInterfaces :: Ord a => [Interface a] -> Signature a
fromInterfaces = Signature . Set.fromList

singleton :: Interface a -> Signature a
singleton = Signature . Set.singleton

interfaces :: Signature a -> [Interface a]
interfaces = Set.toList . getSignature

mapSignature :: Ord b => (a -> b) -> Signature a -> Signature b
mapSignature f = Signature . Set.map (fmap f) . getSignature


data Type
  = VString
  | VForAll Name Kind (Type -> Type)
  | VArrow (Maybe Name) Quantity Type Type
  | VNe (Var (Either Meta (LName Level))) (Snoc Type)
  | VComp (Signature Type) Type

instance Eq Type where
  (==) = (==) `on` quote 0

instance Ord Type where
  compare = compare `on` quote 0


global :: RName -> Type
global = var . Global

free :: LName Level -> Type
free = var . Free . Right

metavar :: Meta -> Type
metavar = var . Free . Left


var :: Var (Either Meta (LName Level)) -> Type
var v = VNe v Nil


unNeutral :: Has Empty sig m => Type -> m (Var (Either Meta (LName Level)), Snoc Type)
unNeutral = \case
  VNe h sp -> pure (h, sp)
  _        -> empty

unComp :: Has Empty sig m => Type -> m (Signature Type, Type)
unComp = \case
  VComp sig _T -> pure (sig, _T)
  _T           -> empty


data Classifier
  = CK Kind
  | CT Type

classifierType :: Classifier -> Maybe Type
classifierType = \case
  CK _K -> empty
  CT _T -> pure _T


occursIn :: Meta -> Level -> Type -> Bool
occursIn p = go
  where
  go d = \case
    VForAll n _ b  -> go (succ d) (b (free (LName d n)))
    VArrow _ _ a b -> go d a || go d b
    VComp s t      -> any (go d) s || go d t
    VNe h sp       -> any (either (== p) (const False)) h || any (go d) sp
    VString        -> False



($$) :: HasCallStack => Type -> Type -> Type
VNe h es $$ a = VNe h (es :> a)
_        $$ _ = error "can’t apply non-neutral/forall type"

($$*) :: (HasCallStack, Foldable t) => Type -> t Type -> Type
($$*) = foldl' ($$)

infixl 9 $$, $$*



data TExpr
  = TString
  | TVar (Var (Either Meta (LName Index)))
  | TForAll Name Kind TExpr
  | TArrow (Maybe Name) Quantity TExpr TExpr
  | TComp (Signature TExpr) TExpr
  | TApp TExpr TExpr
  deriving (Eq, Ord, Show)



quote :: Level -> Type -> TExpr
quote d = \case
  VString        -> TString
  VForAll n t b  -> TForAll n t (quote (succ d) (b (free (LName d n))))
  VArrow n q a b -> TArrow n q (quote d a) (quote d b)
  VComp s t      -> TComp (mapSignature (quote d) s) (quote d t)
  VNe n sp       -> foldl' (&) (TVar (fmap (fmap (levelToIndex d)) <$> n)) (flip TApp . quote d <$> sp)

eval :: HasCallStack => Subst Type -> Env Type -> TExpr -> Type
eval subst = go where
  go env = \case
    TString               -> VString
    TVar (Global n)       -> global n
    TVar (Free (Right n)) -> index env n
    TVar (Free (Left m))  -> fromMaybe (metavar m) (lookupMeta m subst)
    TForAll n t b         -> VForAll n t (\ _T -> go (env |> pvar (n :=: _T)) b)
    TArrow n q a b        -> VArrow n q (go env a) (go env b)
    TComp s t             -> VComp (mapSignature (go env) s) (go env t)
    TApp  f a             -> go env f $$  go env a

apply :: HasCallStack => Subst Type -> Env Type -> Type -> Type
apply subst env = eval subst env . quote (level env)
