{-# Language Safe, DeriveGeneric, DeriveAnyClass, RecordWildCards #-}
{-# Language FlexibleInstances, FlexibleContexts #-}
{-# Language PatternGuards #-}
{-# Language OverloadedStrings #-}
{-| This module contains types related to typechecking and the output of the
typechecker.  In particular, it should contain the types needed by
interface files (see 'Crytpol.ModuleSystem.Interface'), which are (kind of)
the output of the typechker.
-}
module Cryptol.TypeCheck.Type
  ( module Cryptol.TypeCheck.Type
  , module Cryptol.TypeCheck.TCon
  ) where


import GHC.Generics (Generic)
import Control.DeepSeq

import           Data.Map(Map)
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import           Data.Maybe (fromMaybe)
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Text (Text)

import Cryptol.Parser.Selector
import Cryptol.Parser.Position(Located,thing,Range,emptyRange)
import Cryptol.Parser.AST(ImpName(..))
import Cryptol.ModuleSystem.Name
import Cryptol.Utils.Ident (Ident, isInfixIdent, exprModName, ogModule, ModName)
import Cryptol.TypeCheck.TCon
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Solver.InfNat
import Cryptol.Utils.Fixity
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.RecordMap
import Prelude

infix  4 =#=, >==
infixr 5 `tFun`


--------------------------------------------------------------------------------
-- Module parameters

type FunctorParams = Map Ident ModParam

-- | Compute the names from all functor parameters
allParamNames :: FunctorParams -> ModParamNames
allParamNames mps =
  ModParamNames
    { mpnTypes       = Map.unions (map mpnTypes ps)
    , mpnConstraints = concatMap mpnConstraints ps
    , mpnFuns        = Map.unions (map mpnFuns ps)
    , mpnTySyn       = Map.unions (map mpnTySyn ps)
    , mpnDoc         = Nothing
    }
  where
  ps = map mpParameters (Map.elems mps)


-- | A module parameter.  Corresponds to a "signature import".
-- A single module parameter can bring multiple things in scope.
data ModParam = ModParam
  { mpName        :: Ident
    -- ^ The name of a functor parameter.

  , mpQual        :: !(Maybe ModName)
    -- ^ This is the qualifier for the parameter.  We use it to
    -- derive parameter names when doing `_` imports.

  , mpIface       :: ImpName Name
    -- ^ The interface corresponding to this parameter.
    -- This is thing in `import interface`

  , mpParameters  :: ModParamNames
    {- ^ These are the actual parameters, not the ones in the interface
      For example if the same interface is used for multiple parameters
      the `ifmpParameters` would all be different. -}
  } deriving (Show, Generic, NFData)

-- | Information about the names brought in through an "interface import".
-- This is also used to keep information about.
data ModParamNames = ModParamNames
  { mpnTypes       :: Map Name ModTParam
    -- ^ Type parameters

  , mpnTySyn      :: !(Map Name TySyn)
    -- ^ Type synonyms

  , mpnConstraints :: [Located Prop]
    -- ^ Constraints on param. types


  , mpnFuns        :: Map.Map Name ModVParam
    -- ^ Value parameters

  , mpnDoc         :: !(Maybe Text)
    -- ^ Documentation about the interface.
  } deriving (Show, Generic, NFData)

-- | A type parameter of a module.
data ModTParam = ModTParam
  { mtpName   :: Name
  , mtpKind   :: Kind
  , mtpDoc    :: Maybe Text
  } deriving (Show,Generic,NFData)


-- | This is how module parameters appear in actual types.
mtpParam :: ModTParam -> TParam
mtpParam mtp = TParam { tpUnique = nameUnique (mtpName mtp)
                      , tpKind   = mtpKind mtp
                      , tpFlav   = TPModParam (mtpName mtp)
                      , tpInfo   = desc
                      }
  where desc = TVarInfo { tvarDesc   = TVFromModParam (mtpName mtp)
                        , tvarSource = nameLoc (mtpName mtp)
                        }

-- | A value parameter of a module.
data ModVParam = ModVParam
  { mvpName   :: Name
  , mvpType   :: Schema
  , mvpDoc    :: Maybe Text
  , mvpFixity :: Maybe Fixity       -- XXX: This should be in the name?
  } deriving (Show,Generic,NFData)
--------------------------------------------------------------------------------




-- | The types of polymorphic values.
data Schema = Forall { sVars :: [TParam], sProps :: [Prop], sType :: Type }
              deriving (Eq, Show, Generic, NFData)

-- | Type parameters.
data TParam = TParam { tpUnique :: !Int       -- ^ Parameter identifier
                     , tpKind   :: Kind       -- ^ Kind of parameter
                     , tpFlav   :: TPFlavor
                        -- ^ What sort of type parameter is this
                     , tpInfo   :: !TVarInfo
                       -- ^ A description for better messages.
                     }
              deriving (Generic, NFData, Show)

data TPFlavor = TPModParam Name
              | TPUnifyVar
              | TPSchemaParam Name
              | TPTySynParam Name
              | TPPropSynParam Name
              | TPNominalParam Name
              | TPPrimParam Name
              deriving (Generic, NFData, Show)

tMono :: Type -> Schema
tMono = Forall [] []

isMono :: Schema -> Maybe Type
isMono s =
  case s of
    Forall [] [] t -> Just t
    _              -> Nothing


schemaParam :: Name -> TPFlavor
schemaParam = TPSchemaParam

tySynParam :: Name -> TPFlavor
tySynParam = TPTySynParam

propSynParam :: Name -> TPFlavor
propSynParam = TPPropSynParam

nominalParam :: Name -> TPFlavor
nominalParam = TPNominalParam

primParam :: Name -> TPFlavor
primParam = TPPrimParam

modTyParam :: Name -> TPFlavor
modTyParam = TPModParam


tpfName :: TPFlavor -> Maybe Name
tpfName f =
  case f of
    TPUnifyVar       -> Nothing
    TPModParam x     -> Just x
    TPSchemaParam x  -> Just x
    TPTySynParam x   -> Just x
    TPPropSynParam x -> Just x
    TPNominalParam x -> Just x
    TPPrimParam x    -> Just x

tpName :: TParam -> Maybe Name
tpName = tpfName . tpFlav

-- | The internal representation of types.
-- These are assumed to be kind correct.
data Type   = TCon !TCon ![Type]
              -- ^ Type constant with args

            | TVar TVar
              -- ^ Type variable (free or bound)

            | TUser !Name ![Type] !Type
              {- ^ This is just a type annotation, for a type that
              was written as a type synonym.  It is useful so that we
              can use it to report nicer errors.
              Example: @TUser T ts t@ is really just the type @t@ that
              was written as @T ts@ by the user. -}

            | TRec !(RecordMap Ident Type)
              -- ^ Record type

            | TNominal !NominalType ![Type]
              -- ^ A nominal types

              deriving (Show, Generic, NFData)



-- | Type variables.
data TVar   = TVFree !Int Kind (Set TParam) TVarInfo
              -- ^ Unique, kind, ids of bound type variables that are in scope.
              -- The last field gives us some info for nicer warnings/errors.


            | TVBound {-# UNPACK #-} !TParam
              deriving (Show, Generic, NFData)

tvInfo :: TVar -> TVarInfo
tvInfo tv =
  case tv of
    TVFree _ _ _ d -> d
    TVBound tp     -> tpInfo tp

tvUnique :: TVar -> Int
tvUnique (TVFree u _ _ _) = u
tvUnique (TVBound TParam { tpUnique = u }) = u

data TVarInfo = TVarInfo { tvarSource :: !Range -- ^ Source code that gave rise
                         , tvarDesc   :: !TypeSource -- ^ Description
                         }
              deriving (Show, Generic, NFData)


-- | Explains how this type came to be, for better error messages.
data TypeSource = TVFromModParam Name     -- ^ Name of module parameter
                | TVFromSignature Name    -- ^ A variable in a signature
                | TypeWildCard
                | TypeOfRecordField Ident
                | TypeOfTupleField Int
                | TypeOfSeqElement
                | LenOfSeq
                | TypeParamInstNamed {-Fun-}Name {-Param-}Ident
                | TypeParamInstPos   {-Fun-}Name {-Pos (from 1)-}Int
                | DefinitionOf Name
                | LenOfCompGen
                | TypeOfArg ArgDescr
                | TypeOfRes
                | FunApp
                | TypeOfIfCondExpr
                | TypeFromUserAnnotation
                | GeneratorOfListComp
                | CasedExpression
                | ConPat
                | TypeErrorPlaceHolder
                  deriving (Show, Generic, NFData)

data ArgDescr = ArgDescr
  { argDescrFun    :: Maybe Name
  , argDescrNumber :: Maybe Int
  }
  deriving (Show,Generic,NFData)

noArgDescr :: ArgDescr
noArgDescr = ArgDescr { argDescrFun = Nothing, argDescrNumber = Nothing }

-- | Get the names of something that is related to the tvar.
tvSourceName :: TypeSource -> Maybe Name
tvSourceName tvs =
  case tvs of
    TVFromModParam x -> Just x
    TVFromSignature x -> Just x
    TypeParamInstNamed x _ -> Just x
    TypeParamInstPos x _ -> Just x
    DefinitionOf x -> Just x
    TypeOfArg x -> argDescrFun x
    _ -> Nothing


-- | A type annotated with information on how it came about.
data TypeWithSource = WithSource
  { twsType   :: Type
  , twsSource :: TypeSource
  , twsRange  :: !(Maybe Range)
  }


-- | The type is supposed to be of kind 'KProp'.
type Prop   = Type





-- | Type synonym.
data TySyn  = TySyn { tsName        :: Name       -- ^ Name
                    , tsParams      :: [TParam]   -- ^ Parameters
                    , tsConstraints :: [Prop]     -- ^ Ensure body is OK
                    , tsDef         :: Type       -- ^ Definition
                    , tsDoc         :: !(Maybe Text) -- ^ Documentation
                    }
              deriving (Show, Generic, NFData)





-- | Nominal types
data NominalType = NominalType
  { ntName        :: Name
  , ntParams      :: [TParam]
  , ntKind        :: !Kind             -- ^ Result kind
  , ntConstraints :: [Prop]
  , ntDef         :: NominalTypeDef
  , ntFixity      :: !(Maybe Fixity)
  , ntDoc         :: Maybe Text
  } deriving (Show, Generic, NFData)

-- | Definition of a nominal type
data NominalTypeDef =
    Struct StructCon
  | Enum [EnumCon]
  | Abstract
  deriving (Show, Generic, NFData)

-- | Constructor for a struct (aka newtype)
data StructCon = StructCon
  { ntConName     :: !Name
  , ntFields      :: RecordMap Ident Type
  } deriving (Show, Generic, NFData)

-- | Constructor for an enumeration
data EnumCon = EnumCon
  { ecName        :: Name
  , ecNumber      :: !Int -- ^ Number of constructor in the declaration
  , ecFields      :: [Type]
  , ecPublic      :: Bool
  , ecDoc         :: Maybe Text
  } deriving (Show,Generic,NFData)


instance Eq NominalType where
  x == y = ntName x == ntName y

instance Ord NominalType where
  compare x y = compare (ntName x) (ntName y)


--------------------------------------------------------------------------------

instance HasKind TVar where
  kindOf (TVFree  _ k _ _) = k
  kindOf (TVBound tp) = kindOf tp

instance HasKind Type where
  kindOf ty =
    case ty of
      TVar a      -> kindOf a
      TCon c ts   -> quickApply (kindOf c) ts
      TUser _ _ t -> kindOf t
      TRec {}     -> KType
      TNominal nt ts ->
        case ntDef nt of
          Struct {} -> KType
          Enum {}   -> KType
          Abstract  -> quickApply (kindOf nt) ts

instance HasKind TySyn where
  kindOf ts = foldr (:->) (kindOf (tsDef ts)) (map kindOf (tsParams ts))

instance HasKind NominalType where
  kindOf nt = foldr (:->) (ntKind nt) (map kindOf (ntParams nt))

instance HasKind TParam where
  kindOf = tpKind

quickApply :: Kind -> [a] -> Kind
quickApply k []               = k
quickApply (_ :-> k) (_ : ts) = quickApply k ts
quickApply k _                = panic "Cryptol.TypeCheck.AST.quickApply"
                                  [ "Applying a non-function kind:", show k ]

kindResult :: Kind -> Kind
kindResult (_ :-> k) = kindResult k
kindResult k         = k

--------------------------------------------------------------------------------

-- | Syntactic equality, ignoring type synonyms and record order.
instance Eq Type where
  TUser _ _ x == y        = x == y
  x == TUser _ _ y        = y == x

  TCon x xs == TCon y ys  = x == y && xs == ys
  TVar x    == TVar y     = x == y
  TRec xs   == TRec ys    = xs == ys
  TNominal ntx xs == TNominal nty ys = ntx == nty && xs == ys

  _         == _          = False

instance Ord Type where
  compare x0 y0 =
    case (x0,y0) of
      (TUser _ _ t, _)        -> compare t y0
      (_, TUser _ _ t)        -> compare x0 t

      (TVar x, TVar y)        -> compare x y
      (TVar {}, _)            -> LT
      (_, TVar {})            -> GT

      (TCon x xs, TCon y ys)  -> compare (x,xs) (y,ys)
      (TCon {}, _)            -> LT
      (_,TCon {})             -> GT

      (TRec xs, TRec ys)      -> compare xs ys
      (TRec{}, _)             -> LT
      (_, TRec{})             -> GT

      (TNominal x xs, TNominal y ys) -> compare (x,xs) (y,ys)

instance Eq TParam where
  x == y = tpUnique x == tpUnique y

instance Ord TParam where
  compare x y = compare (tpUnique x) (tpUnique y)

tpVar :: TParam -> TVar
tpVar = TVBound

-- | The type is "simple" (i.e., it contains no type functions).
type SType  = Type


--------------------------------------------------------------------
-- Superclass

-- | Compute the set of all @Prop@s that are implied by the
--   given prop via superclass constraints.
superclassSet :: Prop -> Set Prop

superclassSet (TCon (PC PPrime) [n]) =
  Set.fromList [ pFin n, n >== tTwo ]

superclassSet (TCon (PC p0) [t]) = go p0
  where
  super p = Set.insert (TCon (PC p) [t]) (go p)

  go PRing      = super PZero
  go PLogic     = super PZero
  go PField     = super PRing
  go PIntegral  = super PRing
  go PRound     = super PField <> super PCmp
  go PCmp       = super PEq
  go PSignedCmp = super PEq
  go _ = mempty

superclassSet _ = mempty


nominalTypeConTypes :: NominalType -> [(Name,Schema)]
nominalTypeConTypes nt =
  case ntDef nt of
    Struct s -> [ ( ntConName s
                  , Forall as ctrs (TRec (ntFields s) `tFun` resT)
                  ) ]
    Enum cs  -> [ ( ecName c
                  , Forall as ctrs (foldr tFun resT (ecFields c))
                  )
                | c <- cs
                ]
    Abstract -> []
  where
  as    = ntParams nt
  ctrs  = ntConstraints nt
  resT  = TNominal nt (map (TVar . tpVar) as)

nominalTypeIsAbstract :: NominalType -> Bool
nominalTypeIsAbstract nt =
  case ntDef nt of
    Abstract -> True
    _        -> False

instance Eq TVar where
  TVBound x       == TVBound y       = x == y
  TVFree  x _ _ _ == TVFree  y _ _ _ = x == y
  _             == _              = False

instance Ord TVar where
  compare (TVFree x _ _ _) (TVFree y _ _ _) = compare x y
  compare (TVFree _ _ _ _) _                = LT
  compare _            (TVFree _ _ _ _)     = GT

  compare (TVBound x) (TVBound y) = compare x y

--------------------------------------------------------------------------------
-- Queries

isFreeTV :: TVar -> Bool
isFreeTV (TVFree {}) = True
isFreeTV _           = False

isBoundTV :: TVar -> Bool
isBoundTV (TVBound {})  = True
isBoundTV _             = False


tIsError :: Type -> Maybe Type
tIsError ty = case tNoUser ty of
                TCon (TError _) [t] -> Just t
                TCon (TError _) _   -> panic "tIsError" ["Malformed error"]
                _                   -> Nothing

tHasErrors :: Type -> Bool
tHasErrors ty =
  case tNoUser ty of
    TCon (TError _) _   -> True
    TCon _ ts           -> any tHasErrors ts
    TRec mp             -> any tHasErrors mp
    _                   -> False

tIsNat' :: Type -> Maybe Nat'
tIsNat' ty =
  case tNoUser ty of
    TCon (TC (TCNum x)) [] -> Just (Nat x)
    TCon (TC TCInf)     [] -> Just Inf
    _                      -> Nothing

tIsNum :: Type -> Maybe Integer
tIsNum ty = do Nat x <- tIsNat' ty
               return x

tIsInf :: Type -> Bool
tIsInf ty = tIsNat' ty == Just Inf

tIsVar :: Type -> Maybe TVar
tIsVar ty = case tNoUser ty of
              TVar x -> Just x
              _      -> Nothing

tIsFun :: Type -> Maybe (Type, Type)
tIsFun ty = case tNoUser ty of
              TCon (TC TCFun) [a, b] -> Just (a, b)
              _                      -> Nothing

tIsSeq :: Type -> Maybe (Type, Type)
tIsSeq ty = case tNoUser ty of
              TCon (TC TCSeq) [n, a] -> Just (n, a)
              _                      -> Nothing

tIsBit :: Type -> Bool
tIsBit ty = case tNoUser ty of
              TCon (TC TCBit) [] -> True
              _                  -> False

tIsInteger :: Type -> Bool
tIsInteger ty = case tNoUser ty of
                  TCon (TC TCInteger) [] -> True
                  _                      -> False

tIsIntMod :: Type -> Maybe Type
tIsIntMod ty = case tNoUser ty of
                 TCon (TC TCIntMod) [n] -> Just n
                 _                      -> Nothing

tIsRational :: Type -> Bool
tIsRational ty =
  case tNoUser ty of
    TCon (TC TCRational) [] -> True
    _                       -> False

tIsFloat :: Type -> Maybe (Type, Type)
tIsFloat ty =
  case tNoUser ty of
    TCon (TC TCFloat) [e, p] -> Just (e, p)
    _                        -> Nothing

tIsTuple :: Type -> Maybe [Type]
tIsTuple ty = case tNoUser ty of
                TCon (TC (TCTuple _)) ts -> Just ts
                _                        -> Nothing

tIsRec :: Type -> Maybe (RecordMap Ident Type)
tIsRec ty = case tNoUser ty of
              TRec fs -> Just fs
              _       -> Nothing

tIsBinFun :: TFun -> Type -> Maybe (Type,Type)
tIsBinFun f ty = case tNoUser ty of
                   TCon (TF g) [a,b] | f == g -> Just (a,b)
                   _                          -> Nothing

-- | Split up repeated occurances of the given binary type-level function.
tSplitFun :: TFun -> Type -> [Type]
tSplitFun f t0 = go t0 []
  where go ty xs = case tIsBinFun f ty of
                     Just (a,b) -> go a (go b xs)
                     Nothing    -> ty : xs


pIsFin :: Prop -> Maybe Type
pIsFin ty = case tNoUser ty of
              TCon (PC PFin) [t1] -> Just t1
              _                   -> Nothing

pIsPrime :: Prop -> Maybe Type
pIsPrime ty = case tNoUser ty of
                TCon (PC PPrime) [t1] -> Just t1
                _                     -> Nothing

pIsGeq :: Prop -> Maybe (Type,Type)
pIsGeq ty = case tNoUser ty of
              TCon (PC PGeq) [t1,t2] -> Just (t1,t2)
              _                      -> Nothing

pIsEqual :: Prop -> Maybe (Type,Type)
pIsEqual ty = case tNoUser ty of
                TCon (PC PEqual) [t1,t2] -> Just (t1,t2)
                _                        -> Nothing

pIsZero :: Prop -> Maybe Type
pIsZero ty = case tNoUser ty of
               TCon (PC PZero) [t1] -> Just t1
               _                    -> Nothing

pIsLogic :: Prop -> Maybe Type
pIsLogic ty = case tNoUser ty of
                TCon (PC PLogic) [t1] -> Just t1
                _                     -> Nothing

pIsRing :: Prop -> Maybe Type
pIsRing ty = case tNoUser ty of
                TCon (PC PRing) [t1] -> Just t1
                _                    -> Nothing

pIsField :: Prop -> Maybe Type
pIsField ty = case tNoUser ty of
                TCon (PC PField) [t1] -> Just t1
                _                     -> Nothing

pIsIntegral :: Prop -> Maybe Type
pIsIntegral ty = case tNoUser ty of
                   TCon (PC PIntegral) [t1] -> Just t1
                   _                        -> Nothing

pIsRound :: Prop -> Maybe Type
pIsRound ty = case tNoUser ty of
                     TCon (PC PRound) [t1] -> Just t1
                     _                     -> Nothing

pIsEq :: Prop -> Maybe Type
pIsEq ty = case tNoUser ty of
             TCon (PC PEq) [t1] -> Just t1
             _                  -> Nothing

pIsCmp :: Prop -> Maybe Type
pIsCmp ty = case tNoUser ty of
              TCon (PC PCmp) [t1] -> Just t1
              _                   -> Nothing

pIsSignedCmp :: Prop -> Maybe Type
pIsSignedCmp ty = case tNoUser ty of
                    TCon (PC PSignedCmp) [t1] -> Just t1
                    _                         -> Nothing

pIsLiteral :: Prop -> Maybe (Type, Type)
pIsLiteral ty = case tNoUser ty of
                  TCon (PC PLiteral) [t1, t2] -> Just (t1, t2)
                  _                           -> Nothing

pIsLiteralLessThan :: Prop -> Maybe (Type, Type)
pIsLiteralLessThan ty =
  case tNoUser ty of
    TCon (PC PLiteralLessThan) [t1, t2] -> Just (t1, t2)
    _                                   -> Nothing

pIsFLiteral :: Prop -> Maybe (Type,Type,Type,Type)
pIsFLiteral ty = case tNoUser ty of
                   TCon (PC PFLiteral) [t1,t2,t3,t4] -> Just (t1,t2,t3,t4)
                   _                                 -> Nothing

pIsTrue :: Prop -> Bool
pIsTrue ty  = case tNoUser ty of
                TCon (PC PTrue) _ -> True
                _                 -> False

pIsWidth :: Prop -> Maybe Type
pIsWidth ty = case tNoUser ty of
                TCon (TF TCWidth) [t1] -> Just t1
                _                      -> Nothing

pIsValidFloat :: Prop -> Maybe (Type,Type)
pIsValidFloat ty = case tNoUser ty of
                     TCon (PC PValidFloat) [a,b] -> Just (a,b)
                     _                           -> Nothing

--------------------------------------------------------------------------------


tNum     :: Integral a => a -> Type
tNum n    = TCon (TC (TCNum (toInteger n))) []

tZero     :: Type
tZero     = tNum (0 :: Int)

tOne     :: Type
tOne      = tNum (1 :: Int)

tTwo     :: Type
tTwo      = tNum (2 :: Int)

tInf     :: Type
tInf      = TCon (TC TCInf) []

tNat'    :: Nat' -> Type
tNat' n'  = case n' of
              Inf   -> tInf
              Nat n -> tNum n

tNominal :: NominalType -> [Type] -> Type
tNominal = TNominal

tBit     :: Type
tBit      = TCon (TC TCBit) []

tInteger :: Type
tInteger  = TCon (TC TCInteger) []

tRational :: Type
tRational  = TCon (TC TCRational) []

tFloat   :: Type -> Type -> Type
tFloat e p = TCon (TC TCFloat) [ e, p ]

tIntMod :: Type -> Type
tIntMod n = TCon (TC TCIntMod) [n]

tArray :: Type -> Type -> Type
tArray a b = TCon (TC TCArray) [a, b]

tWord    :: Type -> Type
tWord a   = tSeq a tBit

tSeq     :: Type -> Type -> Type
tSeq a b  = TCon (TC TCSeq) [a,b]

tChar :: Type
tChar = tWord (tNum (8 :: Int))

tString :: Int -> Type
tString len = tSeq (tNum len) tChar

tRec     :: RecordMap Ident Type -> Type
tRec      = TRec

tTuple   :: [Type] -> Type
tTuple ts = TCon (TC (TCTuple (length ts))) ts

-- | Make a function type.
tFun     :: Type -> Type -> Type
tFun a b  = TCon (TC TCFun) [a,b]

-- | Eliminate outermost type synonyms.
tNoUser :: Type -> Type
tNoUser t = case t of
              TUser _ _ a -> tNoUser a
              _           -> t


--------------------------------------------------------------------------------
-- Construction of type functions

-- | Make an error value of the given type to replace
-- the given malformed type (the argument to the error function)
tError :: Type -> Type
tError t = TCon (TError (k :-> k)) [t]
  where k = kindOf t

tf1 :: TFun -> Type -> Type
tf1 f x = TCon (TF f) [x]

tf2 :: TFun -> Type -> Type -> Type
tf2 f x y = TCon (TF f) [x,y]

tf3 :: TFun -> Type -> Type -> Type -> Type
tf3 f x y z = TCon (TF f) [x,y,z]

tSub :: Type -> Type -> Type
tSub = tf2 TCSub

tMul :: Type -> Type -> Type
tMul = tf2 TCMul

tDiv :: Type -> Type -> Type
tDiv = tf2 TCDiv

tMod :: Type -> Type -> Type
tMod = tf2 TCMod

tExp :: Type -> Type -> Type
tExp = tf2 TCExp

tMin :: Type -> Type -> Type
tMin = tf2 TCMin

tCeilDiv :: Type -> Type -> Type
tCeilDiv = tf2 TCCeilDiv

tCeilMod :: Type -> Type -> Type
tCeilMod = tf2 TCCeilMod

tLenFromThenTo :: Type -> Type -> Type -> Type
tLenFromThenTo = tf3 TCLenFromThenTo






--------------------------------------------------------------------------------
-- Construction of constraints.

-- | Equality for numeric types.
(=#=) :: Type -> Type -> Prop
x =#= y = TCon (PC PEqual) [x,y]

(=/=) :: Type -> Type -> Prop
x =/= y = TCon (PC PNeq) [x,y]

pZero :: Type -> Prop
pZero t = TCon (PC PZero) [t]

pLogic :: Type -> Prop
pLogic t = TCon (PC PLogic) [t]

pRing :: Type -> Prop
pRing t = TCon (PC PRing) [t]

pIntegral :: Type -> Prop
pIntegral t = TCon (PC PIntegral) [t]

pField :: Type -> Prop
pField t = TCon (PC PField) [t]

pRound :: Type -> Prop
pRound t = TCon (PC PRound) [t]

pEq :: Type -> Prop
pEq t = TCon (PC PEq) [t]

pCmp :: Type -> Prop
pCmp t = TCon (PC PCmp) [t]

pSignedCmp :: Type -> Prop
pSignedCmp t = TCon (PC PSignedCmp) [t]

pLiteral :: Type -> Type -> Prop
pLiteral x y = TCon (PC PLiteral) [x, y]

pLiteralLessThan :: Type -> Type -> Prop
pLiteralLessThan x y = TCon (PC PLiteralLessThan) [x, y]

-- | Make a greater-than-or-equal-to constraint.
(>==) :: Type -> Type -> Prop
x >== y = TCon (PC PGeq) [x,y]

-- | A @Has@ constraint, used for tuple and record selection.
pHas :: Selector -> Type -> Type -> Prop
pHas l ty fi = TCon (PC (PHas l)) [ty,fi]

pTrue :: Prop
pTrue = TCon (PC PTrue) []

pAnd :: [Prop] -> Prop
pAnd []       = pTrue
pAnd [x]      = x
pAnd (x : xs)
  | Just _ <- tIsError x    = x
  | pIsTrue x               = rest
  | Just _ <- tIsError rest = rest
  | pIsTrue rest            = x
  | otherwise               = TCon (PC PAnd) [x, rest]
  where rest = pAnd xs

pSplitAnd :: Prop -> [Prop]
pSplitAnd p0 = go [p0]
  where
  go [] = []
  go (q : qs) =
    case tNoUser q of
      TCon (PC PAnd) [l,r] -> go (l : r : qs)
      TCon (PC PTrue) _    -> go qs
      _                    -> q : go qs

pFin :: Type -> Prop
pFin ty =
  case tNoUser ty of
    TCon (TC (TCNum _)) _ -> pTrue
    TCon (TC TCInf)     _ -> tError prop -- XXX: should we be doing this here??
    _                     -> prop
  where
  prop = TCon (PC PFin) [ty]

pValidFloat :: Type -> Type -> Type
pValidFloat e p = TCon (PC PValidFloat) [e,p]

pPrime :: Type -> Prop
pPrime ty =
  case tNoUser ty of
    TCon (TC TCInf) _ -> tError prop
    _ -> prop
  where
  prop = TCon (PC PPrime) [ty]

-- Negation --------------------------------------------------------------------

{-| `pNegNumeric` negates a simple (i.e., not And, not prime, etc) prop
over numeric type vars.  The result is a conjunction of properties.  -}
pNegNumeric :: Prop -> [Prop]
pNegNumeric prop =
  case tNoUser prop of
    TCon tcon tys ->
      case tcon of
        PC pc ->
          case pc of

            -- not (x == y)  <=>  x /= y
            PEqual -> [TCon (PC PNeq) tys]

            -- not (x /= y)  <=>  x == y
            PNeq -> [TCon (PC PEqual) tys]

            -- not (x >= y)  <=>  x /= y and y >= x
            PGeq -> [TCon (PC PNeq) tys, TCon (PC PGeq) (reverse tys)]

            -- not (fin x)  <=>  x == Inf
            PFin | [ty] <- tys -> [ty =#= tInf]
                 | otherwise -> bad

            -- not True  <=>  0 == 1
            PTrue -> [TCon (PC PEqual) [tZero, tOne]]

            _ -> bad

        TError _ki -> [prop] -- propogates `TError`

        TC _tc -> bad
        TF _tf -> bad

    _ -> bad

  where
  bad = panic "pNegNumeric"
          [ "Unexpeceted numeric constraint:"
          , pretty prop
          ]


--------------------------------------------------------------------------------

noFreeVariables :: FVS t => t -> Bool
noFreeVariables = all (not . isFreeTV) . Set.toList . fvs

freeParams :: FVS t => t -> Set TParam
freeParams x = Set.unions (map params (Set.toList (fvs x)))
  where
    params (TVFree _ _ tps _) = tps
    params (TVBound tp) = Set.singleton tp

class FVS t where
  fvs :: t -> Set TVar

instance FVS Type where
  fvs = go
    where
    go ty =
      case ty of
        TCon _ ts   -> fvs ts
        TVar x      -> Set.singleton x
        TUser _ _ t -> go t
        TRec fs     -> fvs (recordElements fs)
        TNominal _nt ts -> fvs ts


instance FVS a => FVS (Maybe a) where
  fvs Nothing  = Set.empty
  fvs (Just x) = fvs x

instance FVS a => FVS [a] where
  fvs xs        = Set.unions (map fvs xs)

instance (FVS a, FVS b) => FVS (a,b) where
  fvs (x,y) = Set.union (fvs x) (fvs y)

instance FVS Schema where
  fvs (Forall as ps t) =
      Set.difference (Set.union (fvs ps) (fvs t)) bound
    where bound = Set.fromList (map tpVar as)

-- Pretty Printing -------------------------------------------------------------

instance PP TParam where
  ppPrec = ppWithNamesPrec IntMap.empty

instance PP (WithNames TParam) where
  ppPrec _ (WithNames p mp) = ppWithNames mp (tpVar p)

addTNames :: [TParam] -> NameMap -> NameMap
addTNames as ns = foldr (uncurry IntMap.insert) ns
                $ named ++ zip unnamed_nums numNames
                        ++ zip unnamed_vals valNames

  where avail xs = filter (`notElem` used) (nameList xs)
        numNames = avail ["n","m","i","j","k"]
        valNames = avail ["a","b","c","d","e"]

        nm x = (tpUnique x, tpName x, tpKind x)

        named        = [ (u,show (pp n)) | (u,Just n,_)  <- map nm as ]
        unnamed_nums = [ u               | (u,Nothing,KNum)  <- map nm as ]
        unnamed_vals = [ u               | (u,Nothing,KType) <- map nm as ]

        used    = map snd named ++ IntMap.elems ns

ppNominalShort :: NominalType -> Doc
ppNominalShort nt =
  kw <+> pp (ntName nt) <+> hsep (map (ppWithNamesPrec nm 9) ps)
  where
  ps = ntParams nt
  nm = addTNames ps emptyNameMap
  kw = case ntDef nt of
         Struct {} -> "newtype"
         Enum {}   -> "enum"
         Abstract {} -> "primitive type"

ppNominalFull :: NominalType -> Doc
ppNominalFull nt =
  case ntDef nt of

    Struct con -> ppKWDef "newtype" ("=" <+> pp (ntConName con) $$ nest 2 fs)
      where fs = vcat [ pp f <.> ":" <+> pp t
                      | (f,t) <- canonicalFields (ntFields con) ]
    Enum cons ->
      ppKWDef "enum" $
      vcat [ pref <+> pp (ecName con) <+> hsep (map (ppPrec 1) (ecFields con))
           | (pref,con) <- zip ("=" : repeat "|") cons
           ]

    Abstract ->
      "primitive type" <+> paramBinds <+> ctrs <+> ppTyUse <+>
                                                        ":" <+> pp (ntKind nt)
      where
      paramBinds =
        case ps of
          [] -> mempty
          _  -> braces (commaSep (map ppBind ps))
      ppBind p = ppWithNamesPrec nm 0 p <+> ":" <+> pp (kindOf p)
      ppC     = ppWithNamesPrec nm 0
      ctrs = case ntConstraints nt of
               [] -> mempty
               _  -> parens (commaSep (map ppC (ntConstraints nt))) <+> "=>"
  where
  ps = ntParams nt
  cs = vcat (map pp (ntConstraints nt))
  nm = addTNames ps emptyNameMap
  ppTyUse = pp (ntName nt) <+> hsep (map (ppWithNamesPrec nm 9) ps)
  ppKWDef kw def = (kw <+> ppTyUse) $$ nest 2 (cs $$ def)



instance PP Schema where
  ppPrec = ppWithNamesPrec IntMap.empty

instance PP (WithNames Schema) where
  ppPrec _ (WithNames s ns)
    | null (sVars s) && null (sProps s) = body
    | otherwise = nest 2 (sep (vars ++ props ++ [body]))
    where
    body = ppWithNames ns1 (sType s)

    vars = case sVars s of
      [] -> []
      vs -> [nest 1 (braces (commaSepFill (map (ppWithNames ns1) vs)))]

    props = case sProps s of
      [] -> []
      ps -> [nest 1 (parens (commaSepFill (map (ppWithNames ns1) ps))) <+> text "=>"]

    ns1 = addTNames (sVars s) ns

instance PP TySyn where
  ppPrec = ppWithNamesPrec IntMap.empty

instance PP (WithNames TySyn) where
  ppPrec _ (WithNames ts ns) =
    nest 2 $ sep
      [ fsep ([text "type"] ++ ctr ++ lhs ++ [char '='])
      , ppWithNames ns1 (tsDef ts)
      ]
    where ns1 = addTNames (tsParams ts) ns
          ctr = case kindResult (kindOf ts) of
                  KProp -> [text "constraint"]
                  _     -> []
          n = tsName ts
          lhs = case (nameFixity n, tsParams ts) of
                  (Just _, [x, y]) ->
                    [ppWithNames ns1 x, pp (nameIdent n), ppWithNames ns1 y]
                  (_, ps) ->
                    [pp n] ++ map (ppWithNames ns1) ps

instance PP NominalType where
  ppPrec = ppWithNamesPrec IntMap.empty

instance PP (WithNames NominalType) where
  ppPrec _  (WithNames nt _) = ppNominalShort nt -- XXX: do the full thing?



-- | The precedence levels used by this pretty-printing instance
-- correspond with parser non-terminals as follows:
--
--   * 0-1: @type@
--
--   * 2: @infix_type@
--
--   * 3: @app_type@
--
--   * 4: @dimensions atype@
--
--   * 5: @atype@
instance PP (WithNames Type) where
  ppPrec prec ty0@(WithNames ty nmMap) =
    case ty of
      TVar a  -> ppWithNames nmMap a
      TNominal nt ts -> optParens (prec > 3)
                                  (fsep (pp (ntName nt) : map (go 5) ts))
      TRec fs -> ppRecord
                    [ pp l <+> text ":" <+> go 0 t | (l,t) <- displayFields fs ]

      _ | Just tinf <- isTInfix ty0 -> optParens (prec > 2)
                                     $ ppInfix 2 isTInfix tinf

      TUser c ts t ->
        withNameDisp $ \disp ->
        case asOrigName c of
          Just og | NotInScope <- getNameFormat og disp ->
              go prec t -- unfold type synonym if not in scope
          _ ->
            case ts of
              [] -> pp c
              _ -> optParens (prec > 3) $ fsep (pp c : map (go 5) ts)

      TCon (TC tc) ts ->
        case (tc,ts) of
          (TCNum n, [])       -> integer n
          (TCInf,   [])       -> text "inf"
          (TCBit,   [])       -> text "Bit"
          (TCInteger, [])     -> text "Integer"
          (TCRational, [])    -> text "Rational"

          (TCIntMod, [n])     -> optParens (prec > 3) $ text "Z" <+> go 5 n

          (TCSeq,   [t1,TCon (TC TCBit) []]) -> brackets (go 0 t1)
          (TCSeq,   [t1,t2])  -> optParens (prec > 4)
                              $ brackets (go 0 t1) <.> go 4 t2

          (TCFun,   [t1,t2])  -> optParens (prec > 1)
                              $ go 2 t1 <+> text "->" <+> go 1 t2

          (TCTuple _, fs)     -> ppTuple $ map (go 0) fs

          (_, _)              -> optParens (prec > 3) $ fsep (pp tc : (map (go 5) ts))

      TCon (PC pc) ts ->
        case (pc,ts) of
          (PEqual, [t1,t2])   -> go 0 t1 <+> text "==" <+> go 0 t2
          (PNeq ,  [t1,t2])   -> go 0 t1 <+> text "!=" <+> go 0 t2
          (PGeq,  [t1,t2])    -> go 0 t1 <+> text ">=" <+> go 0 t2
          (PFin,  [t1])       -> optParens (prec > 3) $ text "fin" <+> (go 5 t1)
          (PPrime,  [t1])     -> optParens (prec > 3) $ text "prime" <+> (go 5 t1)
          (PHas x, [t1,t2])   -> ppSelector x <+> text "of"
                               <+> go 0 t1 <+> text "is" <+> go 0 t2
          (PAnd, [t1,t2])     -> nest 1 (parens (commaSepFill (map (go 0) (t1 : pSplitAnd t2))))

          (PRing, [t1])       -> pp pc <+> go 5 t1
          (PField, [t1])      -> pp pc <+> go 5 t1
          (PIntegral, [t1])   -> pp pc <+> go 5 t1
          (PRound, [t1])      -> pp pc <+> go 5 t1

          (PCmp, [t1])        -> pp pc <+> go 5 t1
          (PSignedCmp, [t1])  -> pp pc <+> go 5 t1
          (PLiteral, [t1,t2]) -> pp pc <+> go 5 t1 <+> go 5 t2
          (PLiteralLessThan, [t1,t2]) -> pp pc <+> go 5 t1 <+> go 5 t2

          (_, _)              -> optParens (prec > 3) $ fsep (pp pc : map (go 5) ts)

      TCon f ts -> optParens (prec > 3) $ fsep (pp f : map (go 5) ts)

    where
    go p t = ppWithNamesPrec nmMap p t

    isTInfix (WithNames (TCon tc [ieLeft',ieRight']) _) =
      do let ieLeft  = WithNames ieLeft' nmMap
             ieRight = WithNames ieRight' nmMap
         (ieOp, ieFixity) <- infixPrimTy tc
         return Infix { .. }

    isTInfix (WithNames (TUser n [ieLeft',ieRight'] _) _)
      | isInfixIdent (nameIdent n) =
      do let ieLeft   = WithNames ieLeft' nmMap
             ieRight  = WithNames ieRight' nmMap
             ieFixity = fromMaybe defaultFixity (nameFixity n)
             ieOp     = nameIdent n
         return Infix { .. }

    isTInfix _ = Nothing



instance PP (WithNames TVar) where

  ppPrec _ (WithNames tv mp) =
    case tv of
      TVBound {} -> nmTxt
      TVFree {} -> "?" <.> nmTxt
    where
    nmTxt
      | Just a <- IntMap.lookup (tvUnique tv) mp = text a
      | otherwise =
          case tv of
            TVBound x ->
              let declNm n = pp n <.> "`" <.> int (tpUnique x) in
              case tpFlav x of
                TPModParam n     -> ppPrefixName n
                TPUnifyVar       -> pickTVarName (tpKind x) (tvarDesc (tpInfo x)) (tpUnique x)
                TPSchemaParam n  -> declNm n
                TPTySynParam n   -> declNm n
                TPPropSynParam n -> declNm n
                TPNominalParam n -> declNm n
                TPPrimParam n    -> declNm n

            TVFree x k _ d -> pickTVarName k (tvarDesc d) x


pickTVarName :: Kind -> TypeSource -> Int -> Doc
pickTVarName k src uni =
  text $
  case src of
    TVFromModParam n       -> using n
    TVFromSignature n      -> using n
    TypeWildCard           -> mk $ case k of
                                     KNum -> "n"
                                     _    -> "a"
    TypeOfRecordField i    -> using i
    TypeOfTupleField n     -> mk ("tup_" ++ show n)
    TypeOfSeqElement       -> mk "a"
    LenOfSeq               -> mk "n"
    TypeParamInstNamed _ i -> using i
    TypeParamInstPos f n   -> mk (sh f ++ "_" ++ show n)
    DefinitionOf x ->
      case nameInfo x of
        GlobalName SystemName og
          | ogModule og == TopModule exprModName -> mk "it"
        _ -> using x
    LenOfCompGen           -> mk "n"
    GeneratorOfListComp    -> "seq"
    TypeOfIfCondExpr       -> "b"
    TypeOfArg ad           -> mk (case argDescrNumber ad of
                                    Nothing -> "arg"
                                    Just n  -> "arg_" ++ show n)
    TypeOfRes              -> "res"
    FunApp                 -> "fun"
    TypeFromUserAnnotation -> "user"
    TypeErrorPlaceHolder   -> "err"
    CasedExpression        -> "case"
    ConPat                 -> "conp"
  where
  sh a      = show (pp a)
  using a   = mk (sh a)
  mk a      = a ++ "`" ++ show uni

instance PP TVar where
  ppPrec = ppWithNamesPrec IntMap.empty

instance PP Type where
  ppPrec n t = ppWithNamesPrec IntMap.empty n t

instance PP TVarInfo where
  ppPrec _ tvinfo = hsep $ [pp (tvarDesc tvinfo)] ++ loc
    where
    loc = if rng == emptyRange then [] else ["at" <+> pp rng]
    rng = tvarSource tvinfo

instance PP ArgDescr where
  ppPrec _ ad = hsep ([which, "argument"] ++ ofFun)
        where
        which = maybe "function" ordinal (argDescrNumber ad)
        ofFun = case argDescrFun ad of
                  Nothing -> []
                  Just f  -> ["of" <+> pp f]


instance PP TypeSource where
  ppPrec _ tvsrc =
    case tvsrc of
      TVFromModParam m    -> "module parameter" <+> pp m
      TVFromSignature x   -> "signature variable" <+> quotes (pp x)
      TypeWildCard        -> "type wildcard (_)"
      TypeOfRecordField l -> "type of field" <+> quotes (pp l)
      TypeOfTupleField n  -> "type of" <+> ordinal n <+> "tuple field"
      TypeOfSeqElement    -> "type of sequence member"
      LenOfSeq            -> "length of sequence"
      TypeParamInstNamed f i -> "type argument" <+> quotes (pp i) <+>
                                          "of" <+> quotes (pp f)
      TypeParamInstPos   f i -> ordinal i <+> "type argument of" <+>
                                                      quotes (pp f)
      DefinitionOf x      -> "the type of" <+> quotes (pp x)
      LenOfCompGen        -> "length of comprehension generator"
      TypeOfArg ad        -> "type of" <+> pp ad
      TypeOfRes             -> "type of function result"
      TypeOfIfCondExpr      -> "type of `if` condition"
      TypeFromUserAnnotation -> "user annotation"
      GeneratorOfListComp    -> "generator in a list comprehension"
      FunApp                -> "function call"
      TypeErrorPlaceHolder  -> "type error place-holder"
      CasedExpression       -> "cased expression"
      ConPat                -> "constructor pattern"

instance PP ModParamNames where
  ppPrec _ ps =
    let tps = Map.elems (mpnTypes ps)
    in
    vcat $ map pp tps ++
          if null (mpnConstraints ps) then [] else
            [ "type constraint" <+>
                parens (commaSep (map (pp . thing) (mpnConstraints ps)))
            ] ++
           [ pp t | t <- Map.elems (mpnTySyn ps) ] ++
           map pp (Map.elems (mpnFuns ps))

instance PP ModTParam where
  ppPrec _ p =
    "type" <+> pp (mtpName p) <+> ":" <+> pp (mtpKind p)

instance PP ModVParam where
  ppPrec _ p = pp (mvpName p) <+> ":" <+> pp (mvpType p)