{-# 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 :: FunctorParams -> ModParamNames
allParamNames FunctorParams
mps =
  ModParamNames
    { mpnTypes :: Map Name ModTParam
mpnTypes       = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions (forall a b. (a -> b) -> [a] -> [b]
map ModParamNames -> Map Name ModTParam
mpnTypes [ModParamNames]
ps)
    , mpnConstraints :: [Located Type]
mpnConstraints = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ModParamNames -> [Located Type]
mpnConstraints [ModParamNames]
ps
    , mpnFuns :: Map Name ModVParam
mpnFuns        = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions (forall a b. (a -> b) -> [a] -> [b]
map ModParamNames -> Map Name ModVParam
mpnFuns [ModParamNames]
ps)
    , mpnTySyn :: Map Name TySyn
mpnTySyn       = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions (forall a b. (a -> b) -> [a] -> [b]
map ModParamNames -> Map Name TySyn
mpnTySyn [ModParamNames]
ps)
    , mpnDoc :: Maybe Text
mpnDoc         = forall a. Maybe a
Nothing
    }
  where
  ps :: [ModParamNames]
ps = forall a b. (a -> b) -> [a] -> [b]
map ModParam -> ModParamNames
mpParameters (forall k a. Map k a -> [a]
Map.elems FunctorParams
mps)


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

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

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

  , ModParam -> ModParamNames
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 (Int -> ModParam -> ShowS
[ModParam] -> ShowS
ModParam -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ModParam] -> ShowS
$cshowList :: [ModParam] -> ShowS
show :: ModParam -> [Char]
$cshow :: ModParam -> [Char]
showsPrec :: Int -> ModParam -> ShowS
$cshowsPrec :: Int -> ModParam -> ShowS
Show, forall x. Rep ModParam x -> ModParam
forall x. ModParam -> Rep ModParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModParam x -> ModParam
$cfrom :: forall x. ModParam -> Rep ModParam x
Generic, ModParam -> ()
forall a. (a -> ()) -> NFData a
rnf :: ModParam -> ()
$crnf :: ModParam -> ()
NFData)

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

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

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


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

  , ModParamNames -> Maybe Text
mpnDoc         :: !(Maybe Text)
    -- ^ Documentation about the interface.
  } deriving (Int -> ModParamNames -> ShowS
[ModParamNames] -> ShowS
ModParamNames -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ModParamNames] -> ShowS
$cshowList :: [ModParamNames] -> ShowS
show :: ModParamNames -> [Char]
$cshow :: ModParamNames -> [Char]
showsPrec :: Int -> ModParamNames -> ShowS
$cshowsPrec :: Int -> ModParamNames -> ShowS
Show, forall x. Rep ModParamNames x -> ModParamNames
forall x. ModParamNames -> Rep ModParamNames x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModParamNames x -> ModParamNames
$cfrom :: forall x. ModParamNames -> Rep ModParamNames x
Generic, ModParamNames -> ()
forall a. (a -> ()) -> NFData a
rnf :: ModParamNames -> ()
$crnf :: ModParamNames -> ()
NFData)

-- | A type parameter of a module.
data ModTParam = ModTParam
  { ModTParam -> Name
mtpName   :: Name
  , ModTParam -> Kind
mtpKind   :: Kind
  , ModTParam -> Maybe Text
mtpDoc    :: Maybe Text
  } deriving (Int -> ModTParam -> ShowS
[ModTParam] -> ShowS
ModTParam -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ModTParam] -> ShowS
$cshowList :: [ModTParam] -> ShowS
show :: ModTParam -> [Char]
$cshow :: ModTParam -> [Char]
showsPrec :: Int -> ModTParam -> ShowS
$cshowsPrec :: Int -> ModTParam -> ShowS
Show,forall x. Rep ModTParam x -> ModTParam
forall x. ModTParam -> Rep ModTParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModTParam x -> ModTParam
$cfrom :: forall x. ModTParam -> Rep ModTParam x
Generic,ModTParam -> ()
forall a. (a -> ()) -> NFData a
rnf :: ModTParam -> ()
$crnf :: ModTParam -> ()
NFData)


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

-- | A value parameter of a module.
data ModVParam = ModVParam
  { ModVParam -> Name
mvpName   :: Name
  , ModVParam -> Schema
mvpType   :: Schema
  , ModVParam -> Maybe Text
mvpDoc    :: Maybe Text
  , ModVParam -> Maybe Fixity
mvpFixity :: Maybe Fixity       -- XXX: This should be in the name?
  } deriving (Int -> ModVParam -> ShowS
[ModVParam] -> ShowS
ModVParam -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ModVParam] -> ShowS
$cshowList :: [ModVParam] -> ShowS
show :: ModVParam -> [Char]
$cshow :: ModVParam -> [Char]
showsPrec :: Int -> ModVParam -> ShowS
$cshowsPrec :: Int -> ModVParam -> ShowS
Show,forall x. Rep ModVParam x -> ModVParam
forall x. ModVParam -> Rep ModVParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModVParam x -> ModVParam
$cfrom :: forall x. ModVParam -> Rep ModVParam x
Generic,ModVParam -> ()
forall a. (a -> ()) -> NFData a
rnf :: ModVParam -> ()
$crnf :: ModVParam -> ()
NFData)
--------------------------------------------------------------------------------




-- | The types of polymorphic values.
data Schema = Forall { Schema -> [TParam]
sVars :: [TParam], Schema -> [Type]
sProps :: [Prop], Schema -> Type
sType :: Type }
              deriving (Schema -> Schema -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Schema -> Schema -> Bool
$c/= :: Schema -> Schema -> Bool
== :: Schema -> Schema -> Bool
$c== :: Schema -> Schema -> Bool
Eq, Int -> Schema -> ShowS
[Schema] -> ShowS
Schema -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Schema] -> ShowS
$cshowList :: [Schema] -> ShowS
show :: Schema -> [Char]
$cshow :: Schema -> [Char]
showsPrec :: Int -> Schema -> ShowS
$cshowsPrec :: Int -> Schema -> ShowS
Show, forall x. Rep Schema x -> Schema
forall x. Schema -> Rep Schema x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Schema x -> Schema
$cfrom :: forall x. Schema -> Rep Schema x
Generic, Schema -> ()
forall a. (a -> ()) -> NFData a
rnf :: Schema -> ()
$crnf :: Schema -> ()
NFData)

-- | Type parameters.
data TParam = TParam { TParam -> Int
tpUnique :: !Int       -- ^ Parameter identifier
                     , TParam -> Kind
tpKind   :: Kind       -- ^ Kind of parameter
                     , TParam -> TPFlavor
tpFlav   :: TPFlavor
                        -- ^ What sort of type parameter is this
                     , TParam -> TVarInfo
tpInfo   :: !TVarInfo
                       -- ^ A description for better messages.
                     }
              deriving (forall x. Rep TParam x -> TParam
forall x. TParam -> Rep TParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TParam x -> TParam
$cfrom :: forall x. TParam -> Rep TParam x
Generic, TParam -> ()
forall a. (a -> ()) -> NFData a
rnf :: TParam -> ()
$crnf :: TParam -> ()
NFData, Int -> TParam -> ShowS
[TParam] -> ShowS
TParam -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TParam] -> ShowS
$cshowList :: [TParam] -> ShowS
show :: TParam -> [Char]
$cshow :: TParam -> [Char]
showsPrec :: Int -> TParam -> ShowS
$cshowsPrec :: Int -> TParam -> ShowS
Show)

data TPFlavor = TPModParam Name
              | TPUnifyVar
              | TPSchemaParam Name
              | TPTySynParam Name
              | TPPropSynParam Name
              | TPNewtypeParam Name
              | TPPrimParam Name
              deriving (forall x. Rep TPFlavor x -> TPFlavor
forall x. TPFlavor -> Rep TPFlavor x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TPFlavor x -> TPFlavor
$cfrom :: forall x. TPFlavor -> Rep TPFlavor x
Generic, TPFlavor -> ()
forall a. (a -> ()) -> NFData a
rnf :: TPFlavor -> ()
$crnf :: TPFlavor -> ()
NFData, Int -> TPFlavor -> ShowS
[TPFlavor] -> ShowS
TPFlavor -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TPFlavor] -> ShowS
$cshowList :: [TPFlavor] -> ShowS
show :: TPFlavor -> [Char]
$cshow :: TPFlavor -> [Char]
showsPrec :: Int -> TPFlavor -> ShowS
$cshowsPrec :: Int -> TPFlavor -> ShowS
Show)

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

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


schemaParam :: Name -> TPFlavor
schemaParam :: Name -> TPFlavor
schemaParam = Name -> TPFlavor
TPSchemaParam

tySynParam :: Name -> TPFlavor
tySynParam :: Name -> TPFlavor
tySynParam = Name -> TPFlavor
TPTySynParam

propSynParam :: Name -> TPFlavor
propSynParam :: Name -> TPFlavor
propSynParam = Name -> TPFlavor
TPPropSynParam

newtypeParam :: Name -> TPFlavor
newtypeParam :: Name -> TPFlavor
newtypeParam = Name -> TPFlavor
TPNewtypeParam

modTyParam :: Name -> TPFlavor
modTyParam :: Name -> TPFlavor
modTyParam = Name -> TPFlavor
TPModParam


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

tpName :: TParam -> Maybe Name
tpName :: TParam -> Maybe Name
tpName = TPFlavor -> Maybe Name
tpfName forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TPFlavor
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

            | TNewtype !Newtype ![Type]
              -- ^ A newtype

              deriving (Int -> Type -> ShowS
[Type] -> ShowS
Type -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> [Char]
$cshow :: Type -> [Char]
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show, forall x. Rep Type x -> Type
forall x. Type -> Rep Type x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Type x -> Type
$cfrom :: forall x. Type -> Rep Type x
Generic, Type -> ()
forall a. (a -> ()) -> NFData a
rnf :: Type -> ()
$crnf :: Type -> ()
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 (Int -> TVar -> ShowS
[TVar] -> ShowS
TVar -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TVar] -> ShowS
$cshowList :: [TVar] -> ShowS
show :: TVar -> [Char]
$cshow :: TVar -> [Char]
showsPrec :: Int -> TVar -> ShowS
$cshowsPrec :: Int -> TVar -> ShowS
Show, forall x. Rep TVar x -> TVar
forall x. TVar -> Rep TVar x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TVar x -> TVar
$cfrom :: forall x. TVar -> Rep TVar x
Generic, TVar -> ()
forall a. (a -> ()) -> NFData a
rnf :: TVar -> ()
$crnf :: TVar -> ()
NFData)

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

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

data TVarInfo = TVarInfo { TVarInfo -> Range
tvarSource :: !Range -- ^ Source code that gave rise
                         , TVarInfo -> TypeSource
tvarDesc   :: !TypeSource -- ^ Description
                         }
              deriving (Int -> TVarInfo -> ShowS
[TVarInfo] -> ShowS
TVarInfo -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TVarInfo] -> ShowS
$cshowList :: [TVarInfo] -> ShowS
show :: TVarInfo -> [Char]
$cshow :: TVarInfo -> [Char]
showsPrec :: Int -> TVarInfo -> ShowS
$cshowsPrec :: Int -> TVarInfo -> ShowS
Show, forall x. Rep TVarInfo x -> TVarInfo
forall x. TVarInfo -> Rep TVarInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TVarInfo x -> TVarInfo
$cfrom :: forall x. TVarInfo -> Rep TVarInfo x
Generic, TVarInfo -> ()
forall a. (a -> ()) -> NFData a
rnf :: TVarInfo -> ()
$crnf :: TVarInfo -> ()
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
                | TypeErrorPlaceHolder
                  deriving (Int -> TypeSource -> ShowS
[TypeSource] -> ShowS
TypeSource -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TypeSource] -> ShowS
$cshowList :: [TypeSource] -> ShowS
show :: TypeSource -> [Char]
$cshow :: TypeSource -> [Char]
showsPrec :: Int -> TypeSource -> ShowS
$cshowsPrec :: Int -> TypeSource -> ShowS
Show, forall x. Rep TypeSource x -> TypeSource
forall x. TypeSource -> Rep TypeSource x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TypeSource x -> TypeSource
$cfrom :: forall x. TypeSource -> Rep TypeSource x
Generic, TypeSource -> ()
forall a. (a -> ()) -> NFData a
rnf :: TypeSource -> ()
$crnf :: TypeSource -> ()
NFData)

data ArgDescr = ArgDescr
  { ArgDescr -> Maybe Name
argDescrFun    :: Maybe Name
  , ArgDescr -> Maybe Int
argDescrNumber :: Maybe Int
  }
  deriving (Int -> ArgDescr -> ShowS
[ArgDescr] -> ShowS
ArgDescr -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ArgDescr] -> ShowS
$cshowList :: [ArgDescr] -> ShowS
show :: ArgDescr -> [Char]
$cshow :: ArgDescr -> [Char]
showsPrec :: Int -> ArgDescr -> ShowS
$cshowsPrec :: Int -> ArgDescr -> ShowS
Show,forall x. Rep ArgDescr x -> ArgDescr
forall x. ArgDescr -> Rep ArgDescr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ArgDescr x -> ArgDescr
$cfrom :: forall x. ArgDescr -> Rep ArgDescr x
Generic,ArgDescr -> ()
forall a. (a -> ()) -> NFData a
rnf :: ArgDescr -> ()
$crnf :: ArgDescr -> ()
NFData)

noArgDescr :: ArgDescr
noArgDescr :: ArgDescr
noArgDescr = ArgDescr { argDescrFun :: Maybe Name
argDescrFun = forall a. Maybe a
Nothing, argDescrNumber :: Maybe Int
argDescrNumber = forall a. Maybe a
Nothing }

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


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


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





-- | Type synonym.
data TySyn  = TySyn { TySyn -> Name
tsName        :: Name       -- ^ Name
                    , TySyn -> [TParam]
tsParams      :: [TParam]   -- ^ Parameters
                    , TySyn -> [Type]
tsConstraints :: [Prop]     -- ^ Ensure body is OK
                    , TySyn -> Type
tsDef         :: Type       -- ^ Definition
                    , TySyn -> Maybe Text
tsDoc         :: !(Maybe Text) -- ^ Documentation
                    }
              deriving (Int -> TySyn -> ShowS
[TySyn] -> ShowS
TySyn -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TySyn] -> ShowS
$cshowList :: [TySyn] -> ShowS
show :: TySyn -> [Char]
$cshow :: TySyn -> [Char]
showsPrec :: Int -> TySyn -> ShowS
$cshowsPrec :: Int -> TySyn -> ShowS
Show, forall x. Rep TySyn x -> TySyn
forall x. TySyn -> Rep TySyn x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TySyn x -> TySyn
$cfrom :: forall x. TySyn -> Rep TySyn x
Generic, TySyn -> ()
forall a. (a -> ()) -> NFData a
rnf :: TySyn -> ()
$crnf :: TySyn -> ()
NFData)





-- | Named records
data Newtype  = Newtype { Newtype -> Name
ntName   :: Name
                        , Newtype -> [TParam]
ntParams :: [TParam]
                        , Newtype -> [Type]
ntConstraints :: [Prop]
                        , Newtype -> Name
ntConName :: !Name
                        , Newtype -> RecordMap Ident Type
ntFields :: RecordMap Ident Type
                        , Newtype -> Maybe Text
ntDoc :: Maybe Text
                        } deriving (Int -> Newtype -> ShowS
[Newtype] -> ShowS
Newtype -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Newtype] -> ShowS
$cshowList :: [Newtype] -> ShowS
show :: Newtype -> [Char]
$cshow :: Newtype -> [Char]
showsPrec :: Int -> Newtype -> ShowS
$cshowsPrec :: Int -> Newtype -> ShowS
Show, forall x. Rep Newtype x -> Newtype
forall x. Newtype -> Rep Newtype x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Newtype x -> Newtype
$cfrom :: forall x. Newtype -> Rep Newtype x
Generic, Newtype -> ()
forall a. (a -> ()) -> NFData a
rnf :: Newtype -> ()
$crnf :: Newtype -> ()
NFData)


instance Eq Newtype where
  Newtype
x == :: Newtype -> Newtype -> Bool
== Newtype
y = Newtype -> Name
ntName Newtype
x forall a. Eq a => a -> a -> Bool
== Newtype -> Name
ntName Newtype
y

instance Ord Newtype where
  compare :: Newtype -> Newtype -> Ordering
compare Newtype
x Newtype
y = forall a. Ord a => a -> a -> Ordering
compare (Newtype -> Name
ntName Newtype
x) (Newtype -> Name
ntName Newtype
y)


-- | Information about an abstract type.
data AbstractType = AbstractType
  { AbstractType -> Name
atName    :: Name
  , AbstractType -> Kind
atKind    :: Kind
  , AbstractType -> ([TParam], [Type])
atCtrs    :: ([TParam], [Prop])
  , AbstractType -> Maybe Fixity
atFixitiy :: Maybe Fixity
  , AbstractType -> Maybe Text
atDoc     :: Maybe Text
  } deriving (Int -> AbstractType -> ShowS
[AbstractType] -> ShowS
AbstractType -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [AbstractType] -> ShowS
$cshowList :: [AbstractType] -> ShowS
show :: AbstractType -> [Char]
$cshow :: AbstractType -> [Char]
showsPrec :: Int -> AbstractType -> ShowS
$cshowsPrec :: Int -> AbstractType -> ShowS
Show, forall x. Rep AbstractType x -> AbstractType
forall x. AbstractType -> Rep AbstractType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep AbstractType x -> AbstractType
$cfrom :: forall x. AbstractType -> Rep AbstractType x
Generic, AbstractType -> ()
forall a. (a -> ()) -> NFData a
rnf :: AbstractType -> ()
$crnf :: AbstractType -> ()
NFData)




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

instance HasKind AbstractType where
  kindOf :: AbstractType -> Kind
kindOf AbstractType
at = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) (AbstractType -> Kind
atKind AbstractType
at) (forall a b. (a -> b) -> [a] -> [b]
map forall t. HasKind t => t -> Kind
kindOf (forall a b. (a, b) -> a
fst (AbstractType -> ([TParam], [Type])
atCtrs AbstractType
at)))

instance HasKind TVar where
  kindOf :: TVar -> Kind
kindOf (TVFree  Int
_ Kind
k Set TParam
_ TVarInfo
_) = Kind
k
  kindOf (TVBound TParam
tp) = forall t. HasKind t => t -> Kind
kindOf TParam
tp

instance HasKind Type where
  kindOf :: Type -> Kind
kindOf Type
ty =
    case Type
ty of
      TVar TVar
a      -> forall t. HasKind t => t -> Kind
kindOf TVar
a
      TCon TCon
c [Type]
ts   -> forall a. Kind -> [a] -> Kind
quickApply (forall t. HasKind t => t -> Kind
kindOf TCon
c) [Type]
ts
      TUser Name
_ [Type]
_ Type
t -> forall t. HasKind t => t -> Kind
kindOf Type
t
      TRec {}     -> Kind
KType
      TNewtype{}  -> Kind
KType

instance HasKind TySyn where
  kindOf :: TySyn -> Kind
kindOf TySyn
ts = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) (forall t. HasKind t => t -> Kind
kindOf (TySyn -> Type
tsDef TySyn
ts)) (forall a b. (a -> b) -> [a] -> [b]
map forall t. HasKind t => t -> Kind
kindOf (TySyn -> [TParam]
tsParams TySyn
ts))

instance HasKind Newtype where
  kindOf :: Newtype -> Kind
kindOf Newtype
nt = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) Kind
KType (forall a b. (a -> b) -> [a] -> [b]
map forall t. HasKind t => t -> Kind
kindOf (Newtype -> [TParam]
ntParams Newtype
nt))

instance HasKind TParam where
  kindOf :: TParam -> Kind
kindOf TParam
p = TParam -> Kind
tpKind TParam
p

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

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

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

-- | Syntactic equality, ignoring type synonyms and record order.
instance Eq Type where
  TUser Name
_ [Type]
_ Type
x == :: Type -> Type -> Bool
== Type
y        = Type
x forall a. Eq a => a -> a -> Bool
== Type
y
  Type
x == TUser Name
_ [Type]
_ Type
y        = Type
y forall a. Eq a => a -> a -> Bool
== Type
x

  TCon TCon
x [Type]
xs == TCon TCon
y [Type]
ys  = TCon
x forall a. Eq a => a -> a -> Bool
== TCon
y Bool -> Bool -> Bool
&& [Type]
xs forall a. Eq a => a -> a -> Bool
== [Type]
ys
  TVar TVar
x    == TVar TVar
y     = TVar
x forall a. Eq a => a -> a -> Bool
== TVar
y
  TRec RecordMap Ident Type
xs   == TRec RecordMap Ident Type
ys    = RecordMap Ident Type
xs forall a. Eq a => a -> a -> Bool
== RecordMap Ident Type
ys
  TNewtype Newtype
ntx [Type]
xs == TNewtype Newtype
nty [Type]
ys = Newtype
ntx forall a. Eq a => a -> a -> Bool
== Newtype
nty Bool -> Bool -> Bool
&& [Type]
xs forall a. Eq a => a -> a -> Bool
== [Type]
ys

  Type
_         == Type
_          = Bool
False

instance Ord Type where
  compare :: Type -> Type -> Ordering
compare Type
x0 Type
y0 =
    case (Type
x0,Type
y0) of
      (TUser Name
_ [Type]
_ Type
t, Type
_)        -> forall a. Ord a => a -> a -> Ordering
compare Type
t Type
y0
      (Type
_, TUser Name
_ [Type]
_ Type
t)        -> forall a. Ord a => a -> a -> Ordering
compare Type
x0 Type
t

      (TVar TVar
x, TVar TVar
y)        -> forall a. Ord a => a -> a -> Ordering
compare TVar
x TVar
y
      (TVar {}, Type
_)            -> Ordering
LT
      (Type
_, TVar {})            -> Ordering
GT

      (TCon TCon
x [Type]
xs, TCon TCon
y [Type]
ys)  -> forall a. Ord a => a -> a -> Ordering
compare (TCon
x,[Type]
xs) (TCon
y,[Type]
ys)
      (TCon {}, Type
_)            -> Ordering
LT
      (Type
_,TCon {})             -> Ordering
GT

      (TRec RecordMap Ident Type
xs, TRec RecordMap Ident Type
ys)      -> forall a. Ord a => a -> a -> Ordering
compare RecordMap Ident Type
xs RecordMap Ident Type
ys
      (TRec{}, Type
_)             -> Ordering
LT
      (Type
_, TRec{})             -> Ordering
GT

      (TNewtype Newtype
x [Type]
xs, TNewtype Newtype
y [Type]
ys) -> forall a. Ord a => a -> a -> Ordering
compare (Newtype
x,[Type]
xs) (Newtype
y,[Type]
ys)

instance Eq TParam where
  TParam
x == :: TParam -> TParam -> Bool
== TParam
y = TParam -> Int
tpUnique TParam
x forall a. Eq a => a -> a -> Bool
== TParam -> Int
tpUnique TParam
y

instance Ord TParam where
  compare :: TParam -> TParam -> Ordering
compare TParam
x TParam
y = forall a. Ord a => a -> a -> Ordering
compare (TParam -> Int
tpUnique TParam
x) (TParam -> Int
tpUnique TParam
y)

tpVar :: TParam -> TVar
tpVar :: TParam -> TVar
tpVar TParam
p = TParam -> TVar
TVBound TParam
p

-- | 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 :: Type -> Set Type
superclassSet (TCon (PC PC
PPrime) [Type
n]) =
  forall a. Ord a => [a] -> Set a
Set.fromList [ Type -> Type
pFin Type
n, Type
n Type -> Type -> Type
>== Type
tTwo ]

superclassSet (TCon (PC PC
p0) [Type
t]) = PC -> Set Type
go PC
p0
  where
  super :: PC -> Set Type
super PC
p = forall a. Ord a => a -> Set a -> Set a
Set.insert (TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
p) [Type
t]) (PC -> Set Type
go PC
p)

  go :: PC -> Set Type
go PC
PRing      = PC -> Set Type
super PC
PZero
  go PC
PLogic     = PC -> Set Type
super PC
PZero
  go PC
PField     = PC -> Set Type
super PC
PRing
  go PC
PIntegral  = PC -> Set Type
super PC
PRing
  go PC
PRound     = PC -> Set Type
super PC
PField forall a. Semigroup a => a -> a -> a
<> PC -> Set Type
super PC
PCmp
  go PC
PCmp       = PC -> Set Type
super PC
PEq
  go PC
PSignedCmp = PC -> Set Type
super PC
PEq
  go PC
_ = forall a. Monoid a => a
mempty

superclassSet Type
_ = forall a. Monoid a => a
mempty


newtypeConType :: Newtype -> Schema
newtypeConType :: Newtype -> Schema
newtypeConType Newtype
nt =
  [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
as (Newtype -> [Type]
ntConstraints Newtype
nt)
    forall a b. (a -> b) -> a -> b
$ RecordMap Ident Type -> Type
TRec (Newtype -> RecordMap Ident Type
ntFields Newtype
nt) Type -> Type -> Type
`tFun` Newtype -> [Type] -> Type
TNewtype Newtype
nt (forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Type
TVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
tpVar) [TParam]
as)
  where
  as :: [TParam]
as = Newtype -> [TParam]
ntParams Newtype
nt


abstractTypeTC :: AbstractType -> TCon
abstractTypeTC :: AbstractType -> TCon
abstractTypeTC AbstractType
at =
  case Name -> Maybe TCon
builtInType (AbstractType -> Name
atName AbstractType
at) of
    Just TCon
tcon
      | forall t. HasKind t => t -> Kind
kindOf TCon
tcon forall a. Eq a => a -> a -> Bool
== AbstractType -> Kind
atKind AbstractType
at -> TCon
tcon
      | Bool
otherwise ->
        forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"abstractTypeTC"
          [ [Char]
"Mismatch between built-in and declared type."
          , [Char]
"Name: " forall a. [a] -> [a] -> [a]
++ forall a. PP a => a -> [Char]
pretty (AbstractType -> Name
atName AbstractType
at)
          , [Char]
"Declared: " forall a. [a] -> [a] -> [a]
++ forall a. PP a => a -> [Char]
pretty (AbstractType -> Kind
atKind AbstractType
at)
          , [Char]
"Built-in: " forall a. [a] -> [a] -> [a]
++ forall a. PP a => a -> [Char]
pretty (forall t. HasKind t => t -> Kind
kindOf TCon
tcon)
          ]
    Maybe TCon
_         -> TC -> TCon
TC forall a b. (a -> b) -> a -> b
$ UserTC -> TC
TCAbstract forall a b. (a -> b) -> a -> b
$ Name -> Kind -> UserTC
UserTC (AbstractType -> Name
atName AbstractType
at) (AbstractType -> Kind
atKind AbstractType
at)

instance Eq TVar where
  TVBound TParam
x       == :: TVar -> TVar -> Bool
== TVBound TParam
y       = TParam
x forall a. Eq a => a -> a -> Bool
== TParam
y
  TVFree  Int
x Kind
_ Set TParam
_ TVarInfo
_ == TVFree  Int
y Kind
_ Set TParam
_ TVarInfo
_ = Int
x forall a. Eq a => a -> a -> Bool
== Int
y
  TVar
_             == TVar
_              = Bool
False

instance Ord TVar where
  compare :: TVar -> TVar -> Ordering
compare (TVFree Int
x Kind
_ Set TParam
_ TVarInfo
_) (TVFree Int
y Kind
_ Set TParam
_ TVarInfo
_) = forall a. Ord a => a -> a -> Ordering
compare Int
x Int
y
  compare (TVFree Int
_ Kind
_ Set TParam
_ TVarInfo
_) TVar
_                = Ordering
LT
  compare TVar
_            (TVFree Int
_ Kind
_ Set TParam
_ TVarInfo
_)     = Ordering
GT

  compare (TVBound TParam
x) (TVBound TParam
y) = forall a. Ord a => a -> a -> Ordering
compare TParam
x TParam
y

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

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

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


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

tHasErrors :: Type -> Bool
tHasErrors :: Type -> Bool
tHasErrors Type
ty =
  case Type -> Type
tNoUser Type
ty of
    TCon (TError Kind
_) [Type]
_   -> Bool
True
    TCon TCon
_ [Type]
ts           -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
tHasErrors [Type]
ts
    TRec RecordMap Ident Type
mp             -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
tHasErrors RecordMap Ident Type
mp
    Type
_                   -> Bool
False

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

tIsNum :: Type -> Maybe Integer
tIsNum :: Type -> Maybe Integer
tIsNum Type
ty = do Nat Integer
x <- Type -> Maybe Nat'
tIsNat' Type
ty
               forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x

tIsInf :: Type -> Bool
tIsInf :: Type -> Bool
tIsInf Type
ty = Type -> Maybe Nat'
tIsNat' Type
ty forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Nat'
Inf

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

tZero     :: Type
tZero :: Type
tZero     = forall a. Integral a => a -> Type
tNum (Int
0 :: Int)

tOne     :: Type
tOne :: Type
tOne      = forall a. Integral a => a -> Type
tNum (Int
1 :: Int)

tTwo     :: Type
tTwo :: Type
tTwo      = forall a. Integral a => a -> Type
tNum (Int
2 :: Int)

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

tNat'    :: Nat' -> Type
tNat' :: Nat' -> Type
tNat' Nat'
n'  = case Nat'
n' of
              Nat'
Inf   -> Type
tInf
              Nat Integer
n -> forall a. Integral a => a -> Type
tNum Integer
n

tAbstract :: UserTC -> [Type] -> Type
tAbstract :: UserTC -> [Type] -> Type
tAbstract UserTC
u [Type]
ts = TCon -> [Type] -> Type
TCon (TC -> TCon
TC (UserTC -> TC
TCAbstract UserTC
u)) [Type]
ts

tNewtype :: Newtype -> [Type] -> Type
tNewtype :: Newtype -> [Type] -> Type
tNewtype Newtype
nt [Type]
ts = Newtype -> [Type] -> Type
TNewtype Newtype
nt [Type]
ts

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

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

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

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

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

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

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

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

tChar :: Type
tChar :: Type
tChar = Type -> Type
tWord (forall a. Integral a => a -> Type
tNum (Int
8 :: Int))

tString :: Int -> Type
tString :: Int -> Type
tString Int
len = Type -> Type -> Type
tSeq (forall a. Integral a => a -> Type
tNum Int
len) Type
tChar

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

tTuple   :: [Type] -> Type
tTuple :: [Type] -> Type
tTuple [Type]
ts = TCon -> [Type] -> Type
TCon (TC -> TCon
TC (Int -> TC
TCTuple (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts))) [Type]
ts

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

-- | Eliminate outermost type synonyms.
tNoUser :: Type -> Type
tNoUser :: Type -> Type
tNoUser Type
t = case Type
t of
              TUser Name
_ [Type]
_ Type
a -> Type -> Type
tNoUser Type
a
              Type
_           -> Type
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 :: Type -> Type
tError Type
t = TCon -> [Type] -> Type
TCon (Kind -> TCon
TError (Kind
k Kind -> Kind -> Kind
:-> Kind
k)) [Type
t]
  where k :: Kind
k = forall t. HasKind t => t -> Kind
kindOf Type
t

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

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

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

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

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

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

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

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

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

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

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

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






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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

pTrue :: Prop
pTrue :: Type
pTrue = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PTrue) []

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

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

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

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

pPrime :: Type -> Prop
pPrime :: Type -> Type
pPrime Type
ty =
  case Type -> Type
tNoUser Type
ty of
    TCon (TC TC
TCInf) [Type]
_ -> Type -> Type
tError Type
prop
    Type
_ -> Type
prop
  where
  prop :: Type
prop = TCon -> [Type] -> Type
TCon (PC -> TCon
PC PC
PPrime) [Type
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 :: Type -> [Type]
pNegNumeric Type
prop =
  case Type -> Type
tNoUser Type
prop of
    TCon TCon
tcon [Type]
tys ->
      case TCon
tcon of
        PC PC
pc ->
          case PC
pc of

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

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

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

            -- not (fin x)  <=>  x == Inf
            PC
PFin | [Type
ty] <- [Type]
tys -> [Type
ty Type -> Type -> Type
=#= Type
tInf]
                 | Bool
otherwise -> forall {a}. a
bad

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

            PC
_ -> forall {a}. a
bad

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

        TC TC
_tc -> forall {a}. a
bad
        TF TFun
_tf -> forall {a}. a
bad

    Type
_ -> forall {a}. a
bad

  where
  bad :: a
bad = forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"pNegNumeric"
          [ [Char]
"Unexpeceted numeric constraint:"
          , forall a. PP a => a -> [Char]
pretty Type
prop
          ]


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

noFreeVariables :: FVS t => t -> Bool
noFreeVariables :: forall t. FVS t => t -> Bool
noFreeVariables = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. TVar -> Bool
isFreeTV) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. FVS t => t -> Set TVar
fvs

freeParams :: FVS t => t -> Set TParam
freeParams :: forall t. FVS t => t -> Set TParam
freeParams t
x = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map TVar -> Set TParam
params (forall a. Set a -> [a]
Set.toList (forall t. FVS t => t -> Set TVar
fvs t
x)))
  where
    params :: TVar -> Set TParam
params (TVFree Int
_ Kind
_ Set TParam
tps TVarInfo
_) = Set TParam
tps
    params (TVBound TParam
tp) = forall a. a -> Set a
Set.singleton TParam
tp

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

instance FVS Type where
  fvs :: Type -> Set TVar
fvs = Type -> Set TVar
go
    where
    go :: Type -> Set TVar
go Type
ty =
      case Type
ty of
        TCon TCon
_ [Type]
ts   -> forall t. FVS t => t -> Set TVar
fvs [Type]
ts
        TVar TVar
x      -> forall a. a -> Set a
Set.singleton TVar
x
        TUser Name
_ [Type]
_ Type
t -> Type -> Set TVar
go Type
t
        TRec RecordMap Ident Type
fs     -> forall t. FVS t => t -> Set TVar
fvs (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs)
        TNewtype Newtype
_nt [Type]
ts -> forall t. FVS t => t -> Set TVar
fvs [Type]
ts


-- | Find the abstract types mentioned in a type.
class FreeAbstract t where
  freeAbstract :: t -> Set UserTC

instance FreeAbstract a => FreeAbstract [a] where
  freeAbstract :: [a] -> Set UserTC
freeAbstract = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall t. FreeAbstract t => t -> Set UserTC
freeAbstract

instance (FreeAbstract a, FreeAbstract b) => FreeAbstract (a,b) where
  freeAbstract :: (a, b) -> Set UserTC
freeAbstract (a
a,b
b) = forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall t. FreeAbstract t => t -> Set UserTC
freeAbstract a
a) (forall t. FreeAbstract t => t -> Set UserTC
freeAbstract b
b)

instance FreeAbstract TCon where
  freeAbstract :: TCon -> Set UserTC
freeAbstract TCon
tc =
    case TCon
tc of
      TC (TCAbstract UserTC
ut) -> forall a. a -> Set a
Set.singleton UserTC
ut
      TCon
_                  -> forall a. Set a
Set.empty

instance FreeAbstract Type where
  freeAbstract :: Type -> Set UserTC
freeAbstract Type
ty =
    case Type
ty of
      TCon TCon
tc [Type]
ts      -> forall t. FreeAbstract t => t -> Set UserTC
freeAbstract (TCon
tc,[Type]
ts)
      TVar {}         -> forall a. Set a
Set.empty
      TUser Name
_ [Type]
_ Type
t     -> forall t. FreeAbstract t => t -> Set UserTC
freeAbstract Type
t
      TRec RecordMap Ident Type
fs         -> forall t. FreeAbstract t => t -> Set UserTC
freeAbstract (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs)
      TNewtype Newtype
_nt [Type]
ts -> forall t. FreeAbstract t => t -> Set UserTC
freeAbstract [Type]
ts



instance FVS a => FVS (Maybe a) where
  fvs :: Maybe a -> Set TVar
fvs Maybe a
Nothing  = forall a. Set a
Set.empty
  fvs (Just a
x) = forall t. FVS t => t -> Set TVar
fvs a
x

instance FVS a => FVS [a] where
  fvs :: [a] -> Set TVar
fvs [a]
xs        = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map forall t. FVS t => t -> Set TVar
fvs [a]
xs)

instance (FVS a, FVS b) => FVS (a,b) where
  fvs :: (a, b) -> Set TVar
fvs (a
x,b
y) = forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall t. FVS t => t -> Set TVar
fvs a
x) (forall t. FVS t => t -> Set TVar
fvs b
y)

instance FVS Schema where
  fvs :: Schema -> Set TVar
fvs (Forall [TParam]
as [Type]
ps Type
t) =
      forall a. Ord a => Set a -> Set a -> Set a
Set.difference (forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall t. FVS t => t -> Set TVar
fvs [Type]
ps) (forall t. FVS t => t -> Set TVar
fvs Type
t)) Set TVar
bound
    where bound :: Set TVar
bound = forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar [TParam]
as)

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

instance PP TParam where
  ppPrec :: Int -> TParam -> Doc
ppPrec = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty

instance PP (WithNames TParam) where
  ppPrec :: Int -> WithNames TParam -> Doc
ppPrec Int
_ (WithNames TParam
p NameMap
mp) = forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
mp (TParam -> TVar
tpVar TParam
p)

addTNames :: [TParam] -> NameMap -> NameMap
addTNames :: [TParam] -> NameMap -> NameMap
addTNames [TParam]
as NameMap
ns = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert) NameMap
ns
                forall a b. (a -> b) -> a -> b
$ [(Int, [Char])]
named forall a. [a] -> [a] -> [a]
++ forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
unnamed_nums [[Char]]
numNames
                        forall a. [a] -> [a] -> [a]
++ forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
unnamed_vals [[Char]]
valNames

  where avail :: [[Char]] -> [[Char]]
avail [[Char]]
xs = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [[Char]]
used) ([[Char]] -> [[Char]]
nameList [[Char]]
xs)
        numNames :: [[Char]]
numNames = [[Char]] -> [[Char]]
avail [[Char]
"n",[Char]
"m",[Char]
"i",[Char]
"j",[Char]
"k"]
        valNames :: [[Char]]
valNames = [[Char]] -> [[Char]]
avail [[Char]
"a",[Char]
"b",[Char]
"c",[Char]
"d",[Char]
"e"]

        nm :: TParam -> (Int, Maybe Name, Kind)
nm TParam
x = (TParam -> Int
tpUnique TParam
x, TParam -> Maybe Name
tpName TParam
x, TParam -> Kind
tpKind TParam
x)

        named :: [(Int, [Char])]
named        = [ (Int
u,forall a. Show a => a -> [Char]
show (forall a. PP a => a -> Doc
pp Name
n)) | (Int
u,Just Name
n,Kind
_)  <- forall a b. (a -> b) -> [a] -> [b]
map TParam -> (Int, Maybe Name, Kind)
nm [TParam]
as ]
        unnamed_nums :: [Int]
unnamed_nums = [ Int
u               | (Int
u,Maybe Name
Nothing,Kind
KNum)  <- forall a b. (a -> b) -> [a] -> [b]
map TParam -> (Int, Maybe Name, Kind)
nm [TParam]
as ]
        unnamed_vals :: [Int]
unnamed_vals = [ Int
u               | (Int
u,Maybe Name
Nothing,Kind
KType) <- forall a b. (a -> b) -> [a] -> [b]
map TParam -> (Int, Maybe Name, Kind)
nm [TParam]
as ]

        used :: [[Char]]
used    = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Int, [Char])]
named forall a. [a] -> [a] -> [a]
++ forall a. IntMap a -> [a]
IntMap.elems NameMap
ns

ppNewtypeShort :: Newtype -> Doc
ppNewtypeShort :: Newtype -> Doc
ppNewtypeShort Newtype
nt =
  [Char] -> Doc
text [Char]
"newtype" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (Newtype -> Name
ntName Newtype
nt) Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
9) [TParam]
ps)
  where
  ps :: [TParam]
ps  = Newtype -> [TParam]
ntParams Newtype
nt
  nm :: NameMap
nm = [TParam] -> NameMap -> NameMap
addTNames [TParam]
ps NameMap
emptyNameMap

ppNewtypeFull :: Newtype -> Doc
ppNewtypeFull :: Newtype -> Doc
ppNewtypeFull Newtype
nt =
  [Char] -> Doc
text [Char]
"newtype" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (Newtype -> Name
ntName Newtype
nt) Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
9) [TParam]
ps)
  Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Doc
cs Doc -> Doc -> Doc
$$ (Doc
"=" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (Newtype -> Name
ntConName Newtype
nt) Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 Doc
fs))
  where
  ps :: [TParam]
ps = Newtype -> [TParam]
ntParams Newtype
nt
  nm :: NameMap
nm = [TParam] -> NameMap -> NameMap
addTNames [TParam]
ps NameMap
emptyNameMap
  fs :: Doc
fs = [Doc] -> Doc
vcat [ forall a. PP a => a -> Doc
pp Ident
f Doc -> Doc -> Doc
<.> Doc
":" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Type
t | (Ident
f,Type
t) <- forall a b. RecordMap a b -> [(a, b)]
canonicalFields (Newtype -> RecordMap Ident Type
ntFields Newtype
nt) ]
  cs :: Doc
cs = [Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp (Newtype -> [Type]
ntConstraints Newtype
nt))



instance PP Schema where
  ppPrec :: Int -> Schema -> Doc
ppPrec = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty

instance PP (WithNames Schema) where
  ppPrec :: Int -> WithNames Schema -> Doc
ppPrec Int
_ (WithNames Schema
s NameMap
ns)
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [TParam]
sVars Schema
s) Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [Type]
sProps Schema
s) = Doc
body
    | Bool
otherwise = Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
sep ([Doc]
vars forall a. [a] -> [a] -> [a]
++ [Doc]
props forall a. [a] -> [a] -> [a]
++ [Doc
body]))
    where
    body :: Doc
body = forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 (Schema -> Type
sType Schema
s)

    vars :: [Doc]
vars = case Schema -> [TParam]
sVars Schema
s of
      [] -> []
      [TParam]
vs -> [Int -> Doc -> Doc
nest Int
1 (Doc -> Doc
braces ([Doc] -> Doc
commaSepFill (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [TParam]
vs)))]

    props :: [Doc]
props = case Schema -> [Type]
sProps Schema
s of
      [] -> []
      [Type]
ps -> [Int -> Doc -> Doc
nest Int
1 (Doc -> Doc
parens ([Doc] -> Doc
commaSepFill (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [Type]
ps))) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"=>"]

    ns1 :: NameMap
ns1 = [TParam] -> NameMap -> NameMap
addTNames (Schema -> [TParam]
sVars Schema
s) NameMap
ns

instance PP TySyn where
  ppPrec :: Int -> TySyn -> Doc
ppPrec = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty

instance PP (WithNames TySyn) where
  ppPrec :: Int -> WithNames TySyn -> Doc
ppPrec Int
_ (WithNames TySyn
ts NameMap
ns) =
    Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep
      [ [Doc] -> Doc
fsep ([[Char] -> Doc
text [Char]
"type"] forall a. [a] -> [a] -> [a]
++ [Doc]
ctr forall a. [a] -> [a] -> [a]
++ [Doc]
lhs forall a. [a] -> [a] -> [a]
++ [Char -> Doc
char Char
'='])
      , forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 (TySyn -> Type
tsDef TySyn
ts)
      ]
    where ns1 :: NameMap
ns1 = [TParam] -> NameMap -> NameMap
addTNames (TySyn -> [TParam]
tsParams TySyn
ts) NameMap
ns
          ctr :: [Doc]
ctr = case Kind -> Kind
kindResult (forall t. HasKind t => t -> Kind
kindOf TySyn
ts) of
                  Kind
KProp -> [[Char] -> Doc
text [Char]
"constraint"]
                  Kind
_     -> []
          n :: Name
n = TySyn -> Name
tsName TySyn
ts
          lhs :: [Doc]
lhs = case (Name -> Maybe Fixity
nameFixity Name
n, TySyn -> [TParam]
tsParams TySyn
ts) of
                  (Just Fixity
_, [TParam
x, TParam
y]) ->
                    [forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 TParam
x, forall a. PP a => a -> Doc
pp (Name -> Ident
nameIdent Name
n), forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 TParam
y]
                  (Maybe Fixity
_, [TParam]
ps) ->
                    [forall a. PP a => a -> Doc
pp Name
n] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [TParam]
ps

instance PP Newtype where
  ppPrec :: Int -> Newtype -> Doc
ppPrec = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty

instance PP (WithNames Newtype) where
  ppPrec :: Int -> WithNames Newtype -> Doc
ppPrec Int
_  (WithNames Newtype
nt NameMap
_) = Newtype -> Doc
ppNewtypeShort Newtype
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 :: Int -> WithNames Type -> Doc
ppPrec Int
prec ty0 :: WithNames Type
ty0@(WithNames Type
ty NameMap
nmMap) =
    case Type
ty of
      TVar TVar
a  -> forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nmMap TVar
a
      TNewtype Newtype
nt [Type]
ts -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep (forall a. PP a => a -> Doc
pp (Newtype -> Name
ntName Newtype
nt) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5) [Type]
ts)
      TRec RecordMap Ident Type
fs -> [Doc] -> Doc
ppRecord
                    [ forall a. PP a => a -> Doc
pp Ident
l Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
":" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t | (Ident
l,Type
t) <- forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
displayFields RecordMap Ident Type
fs ]

      Type
_ | Just Infix Ident (WithNames Type)
tinf <- WithNames Type -> Maybe (Infix Ident (WithNames Type))
isTInfix WithNames Type
ty0 -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
2)
                                     forall a b. (a -> b) -> a -> b
$ forall thing op.
(PP thing, PP op) =>
Int -> (thing -> Maybe (Infix op thing)) -> Infix op thing -> Doc
ppInfix Int
2 WithNames Type -> Maybe (Infix Ident (WithNames Type))
isTInfix Infix Ident (WithNames Type)
tinf

      TUser Name
c [Type]
ts Type
t ->
        (NameDisp -> Doc) -> Doc
withNameDisp forall a b. (a -> b) -> a -> b
$ \NameDisp
disp ->
        case Name -> Maybe OrigName
asOrigName Name
c of
          Just OrigName
og | NameFormat
NotInScope <- OrigName -> NameDisp -> NameFormat
getNameFormat OrigName
og NameDisp
disp ->
              forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
prec Type
t -- unfold type synonym if not in scope
          Maybe OrigName
_ ->
            case [Type]
ts of
              [] -> forall a. PP a => a -> Doc
pp Name
c
              [Type]
_ -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep (forall a. PP a => a -> Doc
pp Name
c forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5) [Type]
ts)

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

          (TC
TCIntMod, [Type
n])     -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"Z" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
n

          (TC
TCSeq,   [Type
t1,TCon (TC TC
TCBit) []]) -> Doc -> Doc
brackets (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1)
          (TC
TCSeq,   [Type
t1,Type
t2])  -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
4)
                              forall a b. (a -> b) -> a -> b
$ Doc -> Doc
brackets (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1) Doc -> Doc -> Doc
<.> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
4 Type
t2

          (TC
TCFun,   [Type
t1,Type
t2])  -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
1)
                              forall a b. (a -> b) -> a -> b
$ forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
2 Type
t1 Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"->" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
1 Type
t2

          (TCTuple Int
_, [Type]
fs)     -> [Doc] -> Doc
ppTuple forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0) [Type]
fs

          (TC
_, [Type]
_)              -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep (forall a. PP a => a -> Doc
pp TC
tc forall a. a -> [a] -> [a]
: (forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5) [Type]
ts))

      TCon (PC PC
pc) [Type]
ts ->
        case (PC
pc,[Type]
ts) of
          (PC
PEqual, [Type
t1,Type
t2])   -> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1 Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"==" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t2
          (PC
PNeq ,  [Type
t1,Type
t2])   -> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1 Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"!=" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t2
          (PC
PGeq,  [Type
t1,Type
t2])    -> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1 Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
">=" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t2
          (PC
PFin,  [Type
t1])       -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"fin" Doc -> Doc -> Doc
<+> (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1)
          (PC
PPrime,  [Type
t1])     -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"prime" Doc -> Doc -> Doc
<+> (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1)
          (PHas Selector
x, [Type
t1,Type
t2])   -> Selector -> Doc
ppSelector Selector
x Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"of"
                               Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t1 Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"is" Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0 Type
t2
          (PC
PAnd, [Type
t1,Type
t2])     -> Int -> Doc -> Doc
nest Int
1 (Doc -> Doc
parens ([Doc] -> Doc
commaSepFill (forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
0) (Type
t1 forall a. a -> [a] -> [a]
: Type -> [Type]
pSplitAnd Type
t2))))

          (PC
PRing, [Type
t1])       -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1
          (PC
PField, [Type
t1])      -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1
          (PC
PIntegral, [Type
t1])   -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1
          (PC
PRound, [Type
t1])      -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1

          (PC
PCmp, [Type
t1])        -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1
          (PC
PSignedCmp, [Type
t1])  -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1
          (PC
PLiteral, [Type
t1,Type
t2]) -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1 Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t2
          (PC
PLiteralLessThan, [Type
t1,Type
t2]) -> forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t1 Doc -> Doc -> Doc
<+> forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Type
t2

          (PC
_, [Type]
_)              -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep (forall a. PP a => a -> Doc
pp PC
pc forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5) [Type]
ts)

      TCon TCon
f [Type]
ts -> Bool -> Doc -> Doc
optParens (Int
prec forall a. Ord a => a -> a -> Bool
> Int
3) forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep (forall a. PP a => a -> Doc
pp TCon
f forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5) [Type]
ts)

    where
    go :: Int -> a -> Doc
go Int
p a
t = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nmMap Int
p a
t

    isTInfix :: WithNames Type -> Maybe (Infix Ident (WithNames Type))
isTInfix (WithNames (TCon TCon
tc [Type
ieLeft',Type
ieRight']) NameMap
_) =
      do let ieLeft :: WithNames Type
ieLeft  = forall a. a -> NameMap -> WithNames a
WithNames Type
ieLeft' NameMap
nmMap
             ieRight :: WithNames Type
ieRight = forall a. a -> NameMap -> WithNames a
WithNames Type
ieRight' NameMap
nmMap
         (Ident
ieOp, Fixity
ieFixity) <- TCon -> Maybe (Ident, Fixity)
infixPrimTy TCon
tc
         forall (m :: * -> *) a. Monad m => a -> m a
return Infix { Fixity
Ident
WithNames Type
ieFixity :: Fixity
ieRight :: WithNames Type
ieLeft :: WithNames Type
ieOp :: Ident
ieFixity :: Fixity
ieOp :: Ident
ieRight :: WithNames Type
ieLeft :: WithNames Type
.. }

    isTInfix (WithNames (TUser Name
n [Type
ieLeft',Type
ieRight'] Type
_) NameMap
_)
      | Ident -> Bool
isInfixIdent (Name -> Ident
nameIdent Name
n) =
      do let ieLeft :: WithNames Type
ieLeft   = forall a. a -> NameMap -> WithNames a
WithNames Type
ieLeft' NameMap
nmMap
             ieRight :: WithNames Type
ieRight  = forall a. a -> NameMap -> WithNames a
WithNames Type
ieRight' NameMap
nmMap
             ieFixity :: Fixity
ieFixity = forall a. a -> Maybe a -> a
fromMaybe Fixity
defaultFixity (Name -> Maybe Fixity
nameFixity Name
n)
             ieOp :: Ident
ieOp     = Name -> Ident
nameIdent Name
n
         forall (m :: * -> *) a. Monad m => a -> m a
return Infix { Fixity
Ident
WithNames Type
ieOp :: Ident
ieFixity :: Fixity
ieRight :: WithNames Type
ieLeft :: WithNames Type
ieFixity :: Fixity
ieRight :: WithNames Type
ieLeft :: WithNames Type
ieOp :: Ident
.. }

    isTInfix WithNames Type
_ = forall a. Maybe a
Nothing



instance PP (WithNames TVar) where

  ppPrec :: Int -> WithNames TVar -> Doc
ppPrec Int
_ (WithNames TVar
tv NameMap
mp) =
    case TVar
tv of
      TVBound {} -> Doc
nmTxt
      TVFree {} -> Doc
"?" Doc -> Doc -> Doc
<.> Doc
nmTxt
    where
    nmTxt :: Doc
nmTxt
      | Just [Char]
a <- forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (TVar -> Int
tvUnique TVar
tv) NameMap
mp = [Char] -> Doc
text [Char]
a
      | Bool
otherwise =
          case TVar
tv of
            TVBound TParam
x ->
              let declNm :: a -> Doc
declNm a
n = forall a. PP a => a -> Doc
pp a
n Doc -> Doc -> Doc
<.> Doc
"`" Doc -> Doc -> Doc
<.> Int -> Doc
int (TParam -> Int
tpUnique TParam
x) in
              case TParam -> TPFlavor
tpFlav TParam
x of
                TPModParam Name
n     -> forall a. PPName a => a -> Doc
ppPrefixName Name
n
                TPFlavor
TPUnifyVar       -> Kind -> TypeSource -> Int -> Doc
pickTVarName (TParam -> Kind
tpKind TParam
x) (TVarInfo -> TypeSource
tvarDesc (TParam -> TVarInfo
tpInfo TParam
x)) (TParam -> Int
tpUnique TParam
x)
                TPSchemaParam Name
n  -> forall a. PP a => a -> Doc
declNm Name
n
                TPTySynParam Name
n   -> forall a. PP a => a -> Doc
declNm Name
n
                TPPropSynParam Name
n -> forall a. PP a => a -> Doc
declNm Name
n
                TPNewtypeParam Name
n -> forall a. PP a => a -> Doc
declNm Name
n
                TPPrimParam Name
n    -> forall a. PP a => a -> Doc
declNm Name
n

            TVFree Int
x Kind
k Set TParam
_ TVarInfo
d -> Kind -> TypeSource -> Int -> Doc
pickTVarName Kind
k (TVarInfo -> TypeSource
tvarDesc TVarInfo
d) Int
x


pickTVarName :: Kind -> TypeSource -> Int -> Doc
pickTVarName :: Kind -> TypeSource -> Int -> Doc
pickTVarName Kind
k TypeSource
src Int
uni =
  [Char] -> Doc
text forall a b. (a -> b) -> a -> b
$
  case TypeSource
src of
    TVFromModParam Name
n       -> forall a. PP a => a -> [Char]
using Name
n
    TVFromSignature Name
n      -> forall a. PP a => a -> [Char]
using Name
n
    TypeSource
TypeWildCard           -> ShowS
mk forall a b. (a -> b) -> a -> b
$ case Kind
k of
                                     Kind
KNum -> [Char]
"n"
                                     Kind
_    -> [Char]
"a"
    TypeOfRecordField Ident
i    -> forall a. PP a => a -> [Char]
using Ident
i
    TypeOfTupleField Int
n     -> ShowS
mk ([Char]
"tup_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n)
    TypeSource
TypeOfSeqElement       -> ShowS
mk [Char]
"a"
    TypeSource
LenOfSeq               -> ShowS
mk [Char]
"n"
    TypeParamInstNamed Name
_ Ident
i -> forall a. PP a => a -> [Char]
using Ident
i
    TypeParamInstPos Name
f Int
n   -> ShowS
mk (forall a. PP a => a -> [Char]
sh Name
f forall a. [a] -> [a] -> [a]
++ [Char]
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n)
    DefinitionOf Name
x ->
      case Name -> NameInfo
nameInfo Name
x of
        GlobalName NameSource
SystemName OrigName
og
          | OrigName -> ModPath
ogModule OrigName
og forall a. Eq a => a -> a -> Bool
== ModName -> ModPath
TopModule ModName
exprModName -> ShowS
mk [Char]
"it"
        NameInfo
_ -> forall a. PP a => a -> [Char]
using Name
x
    TypeSource
LenOfCompGen           -> ShowS
mk [Char]
"n"
    TypeSource
GeneratorOfListComp    -> [Char]
"seq"
    TypeSource
TypeOfIfCondExpr       -> [Char]
"b"
    TypeOfArg ArgDescr
ad           -> ShowS
mk (case ArgDescr -> Maybe Int
argDescrNumber ArgDescr
ad of
                                    Maybe Int
Nothing -> [Char]
"arg"
                                    Just Int
n  -> [Char]
"arg_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n)
    TypeSource
TypeOfRes              -> [Char]
"res"
    TypeSource
FunApp                 -> [Char]
"fun"
    TypeSource
TypeFromUserAnnotation -> [Char]
"user"
    TypeSource
TypeErrorPlaceHolder   -> [Char]
"err"
  where
  sh :: a -> [Char]
sh a
a      = forall a. Show a => a -> [Char]
show (forall a. PP a => a -> Doc
pp a
a)
  using :: a -> [Char]
using a
a   = ShowS
mk (forall a. PP a => a -> [Char]
sh a
a)
  mk :: ShowS
mk [Char]
a      = [Char]
a forall a. [a] -> [a] -> [a]
++ [Char]
"`" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
uni

instance PP TVar where
  ppPrec :: Int -> TVar -> Doc
ppPrec = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty

instance PP Type where
  ppPrec :: Int -> Type -> Doc
ppPrec Int
n Type
t = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty Int
n Type
t

instance PP TVarInfo where
  ppPrec :: Int -> TVarInfo -> Doc
ppPrec Int
_ TVarInfo
tvinfo = [Doc] -> Doc
hsep forall a b. (a -> b) -> a -> b
$ [forall a. PP a => a -> Doc
pp (TVarInfo -> TypeSource
tvarDesc TVarInfo
tvinfo)] forall a. [a] -> [a] -> [a]
++ [Doc]
loc
    where
    loc :: [Doc]
loc = if Range
rng forall a. Eq a => a -> a -> Bool
== Range
emptyRange then [] else [Doc
"at" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Range
rng]
    rng :: Range
rng = TVarInfo -> Range
tvarSource TVarInfo
tvinfo

instance PP ArgDescr where
  ppPrec :: Int -> ArgDescr -> Doc
ppPrec Int
_ ArgDescr
ad = [Doc] -> Doc
hsep ([Doc
which, Doc
"argument"] forall a. [a] -> [a] -> [a]
++ [Doc]
ofFun)
        where
        which :: Doc
which = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"function" forall a. (Integral a, Show a, Eq a) => a -> Doc
ordinal (ArgDescr -> Maybe Int
argDescrNumber ArgDescr
ad)
        ofFun :: [Doc]
ofFun = case ArgDescr -> Maybe Name
argDescrFun ArgDescr
ad of
                  Maybe Name
Nothing -> []
                  Just Name
f  -> [Doc
"of" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Name
f]


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

instance PP ModParamNames where
  ppPrec :: Int -> ModParamNames -> Doc
ppPrec Int
_ ModParamNames
ps =
    let tps :: [ModTParam]
tps = forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
ps)
    in
    [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp [ModTParam]
tps forall a. [a] -> [a] -> [a]
++
          if forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ModParamNames -> [Located Type]
mpnConstraints ModParamNames
ps) then [] else
            [ Doc
"type constraint" Doc -> Doc -> Doc
<+>
                Doc -> Doc
parens ([Doc] -> Doc
commaSep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. PP a => a -> Doc
pp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
thing) (ModParamNames -> [Located Type]
mpnConstraints ModParamNames
ps)))
            ] forall a. [a] -> [a] -> [a]
++
           [ forall a. PP a => a -> Doc
pp TySyn
t | TySyn
t <- forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name TySyn
mpnTySyn ModParamNames
ps) ] forall a. [a] -> [a] -> [a]
++
           forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp (forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
ps))

instance PP ModTParam where
  ppPrec :: Int -> ModTParam -> Doc
ppPrec Int
_ ModTParam
p =
    Doc
"type" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (ModTParam -> Name
mtpName ModTParam
p) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (ModTParam -> Kind
mtpKind ModTParam
p)

instance PP ModVParam where
  ppPrec :: Int -> ModVParam -> Doc
ppPrec Int
_ ModVParam
p = forall a. PP a => a -> Doc
pp (ModVParam -> Name
mvpName ModVParam
p) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (ModVParam -> Schema
mvpType ModVParam
p)