content: {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE DeriveTraversable #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE DeriveFoldable #-}
  {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  
  -- |
  -- Module      :  Pact.Types.Type
  -- Copyright   :  (C) 2016 Stuart Popejoy
  -- License     :  BSD-style (see the file LICENSE)
  -- Maintainer  :  Stuart Popejoy <stuart@kadena.io>
  --
  -- Language types.
  --
  
  module Pact.Types.Type
   (
     TypeName(..),
     Arg(..),aInfo,aName,aType,
     FunType(..),ftArgs,ftReturn,
     FunTypes,funTypes,prettyFunTypes,
     PrimType(..),
     GuardType(..),
     tyInteger,tyDecimal,tyTime,tyBool,tyString,
     tyList,tyObject,tyValue,tyKeySet,tyTable,
     SchemaType(..),
     SchemaPartial(..),
     TypeVarName(..),typeVarName,
     TypeVar(..),tvName,tvConstraint,
     Type(..),tyFunType,tyListType,tySchema,tySchemaType,tySchemaPartial,tyUser,tyVar,tyGuard,
     mkTyVar,mkTyVar',mkSchemaVar,
     isAnyTy,isVarTy,canUnifyWith
     ) where
  
  import Data.Eq.Deriving
  import Text.Show.Deriving
  
  import Control.Lens
  import Data.List
  import Control.Monad
  import Prelude
  import Data.Aeson
  import Data.String
  import Data.Set (Set, isSubsetOf)
  import qualified Data.Set as Set
  import Data.Thyme.Format.Aeson ()
  import GHC.Generics (Generic)
  import Data.Hashable
  import Data.List.NonEmpty (NonEmpty (..))
  import Data.Foldable
  import Control.DeepSeq
  import Data.Text (Text,unpack)
  import Data.Default (Default(..))
  
  import Pact.Types.Pretty
  import Pact.Types.Util
  import Pact.Types.Info
  
  
  newtype TypeName = TypeName Text
    deriving (Eq,Ord,IsString,AsString,ToJSON,FromJSON,Pretty,Generic,NFData,Show)
  
  -- | Pair a name and a type (arguments, bindings etc)
  data Arg o = Arg {
    _aName :: Text,
    _aType :: Type o,
    _aInfo :: Info
    } deriving (Eq,Ord,Functor,Foldable,Traversable,Generic,Show)
  
  instance NFData o => NFData (Arg o)
  instance Pretty o => Pretty (Arg o) where
    pretty (Arg n t _) = pretty n <> colon <> pretty t
  
  -- | Function type
  data FunType o = FunType {
    _ftArgs :: [Arg o],
    _ftReturn :: Type o
    } deriving (Eq,Ord,Functor,Foldable,Traversable,Generic,Show)
  
  instance NFData o => NFData (FunType o)
  instance (Pretty o) => Pretty (FunType o) where
    pretty (FunType as t) = hsep (map pretty as) <+> "->" <+> pretty t
  
  -- | use NonEmpty for function types
  type FunTypes o = NonEmpty (FunType o)
  
  funTypes :: FunType o -> FunTypes o
  funTypes ft = ft :| []
  
  prettyFunTypes :: Pretty o => FunTypes o -> Doc
  prettyFunTypes (t :| []) = pretty t
  prettyFunTypes ts = pretty (toList ts)
  
  data GuardType
    = GTyKeySet
    | GTyKeySetName
    | GTyPact
    | GTyUser
    | GTyModule
    deriving (Eq,Ord,Generic,Show)
  
  instance NFData GuardType
  
  -- | Primitive/unvarying types.
  -- Guard is lame Maybe to allow "wildcards".
  data PrimType =
    TyInteger |
    TyDecimal |
    TyTime |
    TyBool |
    TyString |
    TyValue |
    TyGuard (Maybe GuardType)
    deriving (Eq,Ord,Generic,Show)
  
  instance NFData PrimType
  
  
  tyInteger,tyDecimal,tyTime,tyBool,tyString,tyList,tyObject,tyValue,
    tyKeySet,tyTable,tyGuard :: Text
  tyInteger = "integer"
  tyDecimal = "decimal"
  tyTime = "time"
  tyBool = "bool"
  tyString = "string"
  tyList = "list"
  tyObject = "object"
  tyValue = "value"
  tyKeySet = "keyset"
  tyGuard = "guard"
  tyTable = "table"
  
  instance Pretty PrimType where
    pretty t = pretty $ case t of
      TyInteger -> tyInteger
      TyDecimal -> tyDecimal
      TyTime -> tyTime
      TyBool -> tyBool
      TyString -> tyString
      TyValue -> tyValue
      TyGuard tg -> case tg of
        Just GTyKeySet -> tyKeySet
        _ -> tyGuard
  
  data SchemaType =
    TyTable |
    TyObject |
    TyBinding
    deriving (Eq,Ord,Generic,Show)
  
  instance NFData SchemaType
  instance Pretty SchemaType where
    pretty TyTable   = pretty tyTable
    pretty TyObject  = pretty tyObject
    pretty TyBinding = "binding"
  
  newtype TypeVarName = TypeVarName { _typeVarName :: Text }
    deriving (Eq,Ord,IsString,AsString,ToJSON,FromJSON,Hashable,Pretty,Generic,NFData,Show)
  
  -- | Type variables are namespaced for value types and schema types.
  data TypeVar v =
    TypeVar { _tvName :: TypeVarName, _tvConstraint :: [Type v] } |
    SchemaVar { _tvName :: TypeVarName }
    deriving (Functor,Foldable,Traversable,Generic,Show)
  
  instance NFData v => NFData (TypeVar v)
  instance Eq (TypeVar v) where
    (TypeVar a _) == (TypeVar b _) = a == b
    (SchemaVar a) == (SchemaVar b) = a == b
    _ == _ = False
  instance Ord (TypeVar v) where
    x `compare` y = case (x,y) of
      (TypeVar {},SchemaVar {}) -> LT
      (SchemaVar {},TypeVar {}) -> GT
      (TypeVar a _,TypeVar b _) -> a `compare` b
      (SchemaVar a,SchemaVar b) -> a `compare` b
  instance (Pretty v) => Pretty (TypeVar v) where
    pretty (TypeVar n []) = angles $ pretty n
    pretty (TypeVar n cs) = angles $ pretty n <> commaBrackets (map pretty cs)
    pretty (SchemaVar n)  = angles $ braces $ pretty n
  
  -- | Represent a full or partial schema inhabitant.
  --
  -- @PartialSchema@ represents a schema with only the given subset of fields.
  -- @AnySubschema@ is used in places where any subset of fields can be provided.
  -- @AnySubschema@ unifies with any larger type to give that type.
  data SchemaPartial = FullSchema | PartialSchema !(Set Text) | AnySubschema
    deriving (Eq,Ord,Show,Generic)
  instance NFData SchemaPartial
  instance Default SchemaPartial where def = FullSchema
  
  showPartial :: SchemaPartial -> String
  showPartial FullSchema = ""
  showPartial (PartialSchema ks)
    = "~[" ++ intercalate "," (unpack.asString <$> Set.toList ks) ++ "]"
  showPartial AnySubschema = "~"
  
  -- | Pact types.
  data Type v =
    TyAny |
    TyVar { _tyVar :: TypeVar v } |
    TyPrim PrimType |
    TyList { _tyListType :: Type v } |
    TySchema
    { _tySchema :: SchemaType
    , _tySchemaType :: Type v
    , _tySchemaPartial :: SchemaPartial } |
    TyFun { _tyFunType :: FunType v } |
    TyUser { _tyUser :: v }
      deriving (Eq,Ord,Functor,Foldable,Traversable,Generic,Show)
  
  instance NFData v => NFData (Type v)
  
  instance (Pretty o) => Pretty (Type o) where
    pretty ty = case ty of
      TyVar n        -> pretty n
      TyUser v       -> pretty v
      TyFun f        -> pretty f
      TySchema s t p -> pretty s <> colon <> pretty (showPartial p) <> pretty t
      TyList t       -> brackets $ pretty t
      TyPrim t       -> pretty t
      TyAny          -> "*"
  
  mkTyVar :: TypeVarName -> [Type n] -> Type n
  mkTyVar n cs = TyVar (TypeVar n cs)
  mkTyVar' :: TypeVarName -> Type n
  mkTyVar' n = mkTyVar n []
  mkSchemaVar :: TypeVarName -> Type n
  mkSchemaVar n = TyVar (SchemaVar n)
  
  isAnyTy :: Type v -> Bool
  isAnyTy TyAny = True
  isAnyTy _ = False
  
  isVarTy :: Type v -> Bool
  isVarTy TyVar {} = True
  isVarTy _ = False
  
  -- | a `canUnifyWith` b means a "can represent/contains" b
  canUnifyWith :: Eq n => Type n -> Type n -> Bool
  canUnifyWith TyAny _ = True
  canUnifyWith _ TyAny = True
  canUnifyWith (TyVar (SchemaVar _)) TyUser {} = True
  canUnifyWith (TyVar SchemaVar {}) (TyVar SchemaVar {}) = True
  canUnifyWith (TyVar (TypeVar _ ac)) (TyVar (TypeVar _ bc)) = all (`elem` ac) bc
  canUnifyWith (TyVar (TypeVar _ cs)) b = null cs || b `elem` cs
  canUnifyWith (TyList a) (TyList b) = a `canUnifyWith` b
  canUnifyWith (TySchema _ aTy aP) (TySchema _ bTy bP)
    = aTy `canUnifyWith` bTy && bP `isSubPartial` aP
  canUnifyWith a b = a == b
  {-# INLINE canUnifyWith #-}
  
  -- | @a `isSubPartial` b@ means that @a <= b@ in the lattice given by
  -- @SchemaPartial@, ie, that @a@ is smaller than @b@.
  isSubPartial :: SchemaPartial -> SchemaPartial -> Bool
  isSubPartial _ FullSchema = True
  isSubPartial FullSchema _ = False
  isSubPartial AnySubschema _ = True
  isSubPartial _ AnySubschema = False
  isSubPartial (PartialSchema a) (PartialSchema b) = a `isSubsetOf` b
  
  
  
  
  makeLenses ''Type
  makeLenses ''FunType
  makeLenses ''Arg
  makeLenses ''TypeVar
  makeLenses ''TypeVarName
  
  deriveShow1 ''TypeVar
  deriveShow1 ''Arg
  deriveShow1 ''FunType
  deriveShow1 ''Type
  deriveEq1 ''TypeVar
  deriveEq1 ''Arg
  deriveEq1 ''FunType
  deriveEq1 ''Type
  