content: {-# 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
  
  -- | If the supplied 'Type' is a 'TNominal' type, then return @'Just' (nt, ts)@,
  -- where @nt@ and @ts@ are the underlying 'NominalType' and 'Type' arguments.
  -- Otherwise, return 'Nothing'.
  tIsNominal :: Type -> Maybe (NominalType, [Type])
  tIsNominal ty = case tNoUser ty of
                    TNominal nm ts -> Just (nm, ts)
                    _              -> 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"
            [ "Unexpected 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 :: PPCfg -> [TParam] -> NameMap -> NameMap
  addTNames cfg as ns =
    foldr (uncurry IntMap.insert) ns
    $ named ++ zip unnamed_nums numNames
            ++ zip unnamed_vals valNames
  
    where avail xs = map text (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,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 (show . fixPPCfg cfg) (map snd named ++ IntMap.elems ns)
  
  ppNominalShort :: NominalType -> Doc
  ppNominalShort nt =
    withPPCfg $ \cfg ->
    let
      ps = ntParams nt
      nm = addTNames cfg ps emptyNameMap
      kw = case ntDef nt of
             Struct {} -> "newtype"
             Enum {}   -> "enum"
             Abstract {} -> "primitive type"
    in
      kw <+> pp (ntName nt) <+> hsep (map (ppWithNamesPrec nm 9) ps)
  
  
  ppNominalFull :: NominalType -> Doc
  ppNominalFull nt =
    withPPCfg $ \cfg ->
    let
      ps = ntParams nt
      cs = vcat (map pp (ntConstraints nt))
      nm = addTNames cfg ps emptyNameMap
      ppTyUse = pp (ntName nt) <+> hsep (map (ppWithNamesPrec nm 9) ps)
      ppKWDef kw def = (kw <+> ppTyUse) $$ nest 2 (cs $$ def)
    in
  
    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))) <+> "=>"
    
  
  
  instance PP Schema where
    ppPrec = ppWithNamesPrec IntMap.empty
  
  instance PP (WithNames Schema) where
    ppPrec _ (WithNames s ns) =
      withPPCfg $ \cfg ->
      let
        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 cfg (sVars s) ns
      in if null (sVars s) && null (sProps s)
          then body
          else nest 2 (sep (vars ++ props ++ [body]))
  
  
  instance PP TySyn where
    ppPrec = ppWithNamesPrec IntMap.empty
  
  instance PP (WithNames TySyn) where
    ppPrec _ (WithNames ts ns) =
      withPPCfg $ \cfg ->
      let
        ns1 = addTNames cfg (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
      in
      nest 2 $ sep
        [ fsep ([text "type"] ++ ctr ++ lhs ++ [char '='])
        , ppWithNames ns1 (tsDef ts)
        ]
  
  
  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 = 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 =
    withPPCfg $ \cfg ->
    let
      sh a      = show (fixPPCfg cfg (pp a))
      using a   = mk (sh a)
      mk a      = a ++ "`" ++ show uni
    in
    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"
  
  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 ++
              [ "type constraint" <+>
                  parens (commaSep (map (pp . thing) (mpnConstraints ps)))
              | not (null (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)
  
  
  