{-# 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       = [Map Name ModTParam] -> Map Name ModTParam
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((ModParamNames -> Map Name ModTParam)
-> [ModParamNames] -> [Map Name ModTParam]
forall a b. (a -> b) -> [a] -> [b]
map ModParamNames -> Map Name ModTParam
mpnTypes [ModParamNames]
ps)
    , mpnConstraints :: [Located Prop]
mpnConstraints = (ModParamNames -> [Located Prop])
-> [ModParamNames] -> [Located Prop]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ModParamNames -> [Located Prop]
mpnConstraints [ModParamNames]
ps
    , mpnFuns :: Map Name ModVParam
mpnFuns        = [Map Name ModVParam] -> Map Name ModVParam
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((ModParamNames -> Map Name ModVParam)
-> [ModParamNames] -> [Map Name ModVParam]
forall a b. (a -> b) -> [a] -> [b]
map ModParamNames -> Map Name ModVParam
mpnFuns [ModParamNames]
ps)
    , mpnTySyn :: Map Name TySyn
mpnTySyn       = [Map Name TySyn] -> Map Name TySyn
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((ModParamNames -> Map Name TySyn)
-> [ModParamNames] -> [Map Name TySyn]
forall a b. (a -> b) -> [a] -> [b]
map ModParamNames -> Map Name TySyn
mpnTySyn [ModParamNames]
ps)
    , mpnDoc :: Maybe Text
mpnDoc         = Maybe Text
forall a. Maybe a
Nothing
    }
  where
  ps :: [ModParamNames]
ps = (ModParam -> ModParamNames) -> [ModParam] -> [ModParamNames]
forall a b. (a -> b) -> [a] -> [b]
map ModParam -> ModParamNames
mpParameters (FunctorParams -> [ModParam]
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]
(Int -> ModParam -> ShowS)
-> (ModParam -> [Char]) -> ([ModParam] -> ShowS) -> Show ModParam
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ModParam -> ShowS
showsPrec :: Int -> ModParam -> ShowS
$cshow :: ModParam -> [Char]
show :: ModParam -> [Char]
$cshowList :: [ModParam] -> ShowS
showList :: [ModParam] -> ShowS
Show, (forall x. ModParam -> Rep ModParam x)
-> (forall x. Rep ModParam x -> ModParam) -> Generic ModParam
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
$cfrom :: forall x. ModParam -> Rep ModParam x
from :: forall x. ModParam -> Rep ModParam x
$cto :: forall x. Rep ModParam x -> ModParam
to :: forall x. Rep ModParam x -> ModParam
Generic, ModParam -> ()
(ModParam -> ()) -> NFData ModParam
forall a. (a -> ()) -> NFData a
$crnf :: ModParam -> ()
rnf :: 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 Prop]
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]
(Int -> ModParamNames -> ShowS)
-> (ModParamNames -> [Char])
-> ([ModParamNames] -> ShowS)
-> Show ModParamNames
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ModParamNames -> ShowS
showsPrec :: Int -> ModParamNames -> ShowS
$cshow :: ModParamNames -> [Char]
show :: ModParamNames -> [Char]
$cshowList :: [ModParamNames] -> ShowS
showList :: [ModParamNames] -> ShowS
Show, (forall x. ModParamNames -> Rep ModParamNames x)
-> (forall x. Rep ModParamNames x -> ModParamNames)
-> Generic ModParamNames
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
$cfrom :: forall x. ModParamNames -> Rep ModParamNames x
from :: forall x. ModParamNames -> Rep ModParamNames x
$cto :: forall x. Rep ModParamNames x -> ModParamNames
to :: forall x. Rep ModParamNames x -> ModParamNames
Generic, ModParamNames -> ()
(ModParamNames -> ()) -> NFData ModParamNames
forall a. (a -> ()) -> NFData a
$crnf :: ModParamNames -> ()
rnf :: 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]
(Int -> ModTParam -> ShowS)
-> (ModTParam -> [Char])
-> ([ModTParam] -> ShowS)
-> Show ModTParam
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ModTParam -> ShowS
showsPrec :: Int -> ModTParam -> ShowS
$cshow :: ModTParam -> [Char]
show :: ModTParam -> [Char]
$cshowList :: [ModTParam] -> ShowS
showList :: [ModTParam] -> ShowS
Show,(forall x. ModTParam -> Rep ModTParam x)
-> (forall x. Rep ModTParam x -> ModTParam) -> Generic ModTParam
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
$cfrom :: forall x. ModTParam -> Rep ModTParam x
from :: forall x. ModTParam -> Rep ModTParam x
$cto :: forall x. Rep ModTParam x -> ModTParam
to :: forall x. Rep ModTParam x -> ModTParam
Generic,ModTParam -> ()
(ModTParam -> ()) -> NFData ModTParam
forall a. (a -> ()) -> NFData a
$crnf :: ModTParam -> ()
rnf :: 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]
(Int -> ModVParam -> ShowS)
-> (ModVParam -> [Char])
-> ([ModVParam] -> ShowS)
-> Show ModVParam
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ModVParam -> ShowS
showsPrec :: Int -> ModVParam -> ShowS
$cshow :: ModVParam -> [Char]
show :: ModVParam -> [Char]
$cshowList :: [ModVParam] -> ShowS
showList :: [ModVParam] -> ShowS
Show,(forall x. ModVParam -> Rep ModVParam x)
-> (forall x. Rep ModVParam x -> ModVParam) -> Generic ModVParam
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
$cfrom :: forall x. ModVParam -> Rep ModVParam x
from :: forall x. ModVParam -> Rep ModVParam x
$cto :: forall x. Rep ModVParam x -> ModVParam
to :: forall x. Rep ModVParam x -> ModVParam
Generic,ModVParam -> ()
(ModVParam -> ()) -> NFData ModVParam
forall a. (a -> ()) -> NFData a
$crnf :: ModVParam -> ()
rnf :: ModVParam -> ()
NFData)
--------------------------------------------------------------------------------




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

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

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

isMono :: Schema -> Maybe Type
isMono :: Schema -> Maybe Prop
isMono Schema
s =
  case Schema
s of
    Forall [] [] Prop
t -> Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t
    Schema
_              -> Maybe Prop
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

nominalParam :: Name -> TPFlavor
nominalParam :: Name -> TPFlavor
nominalParam = Name -> TPFlavor
TPNominalParam

primParam :: Name -> TPFlavor
primParam :: Name -> TPFlavor
primParam = Name -> TPFlavor
TPPrimParam

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       -> Maybe Name
forall a. Maybe a
Nothing
    TPModParam Name
x     -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
    TPSchemaParam Name
x  -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
    TPTySynParam Name
x   -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
    TPPropSynParam Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
    TPNominalParam Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
    TPPrimParam Name
x    -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x

tpName :: TParam -> Maybe Name
tpName :: TParam -> Maybe Name
tpName = TPFlavor -> Maybe Name
tpfName (TPFlavor -> Maybe Name)
-> (TParam -> TPFlavor) -> TParam -> Maybe Name
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

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

              deriving (Int -> Prop -> ShowS
[Prop] -> ShowS
Prop -> [Char]
(Int -> Prop -> ShowS)
-> (Prop -> [Char]) -> ([Prop] -> ShowS) -> Show Prop
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Prop -> ShowS
showsPrec :: Int -> Prop -> ShowS
$cshow :: Prop -> [Char]
show :: Prop -> [Char]
$cshowList :: [Prop] -> ShowS
showList :: [Prop] -> ShowS
Show, (forall x. Prop -> Rep Prop x)
-> (forall x. Rep Prop x -> Prop) -> Generic Prop
forall x. Rep Prop x -> Prop
forall x. Prop -> Rep Prop x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Prop -> Rep Prop x
from :: forall x. Prop -> Rep Prop x
$cto :: forall x. Rep Prop x -> Prop
to :: forall x. Rep Prop x -> Prop
Generic, Prop -> ()
(Prop -> ()) -> NFData Prop
forall a. (a -> ()) -> NFData a
$crnf :: Prop -> ()
rnf :: Prop -> ()
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]
(Int -> TVar -> ShowS)
-> (TVar -> [Char]) -> ([TVar] -> ShowS) -> Show TVar
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TVar -> ShowS
showsPrec :: Int -> TVar -> ShowS
$cshow :: TVar -> [Char]
show :: TVar -> [Char]
$cshowList :: [TVar] -> ShowS
showList :: [TVar] -> ShowS
Show, (forall x. TVar -> Rep TVar x)
-> (forall x. Rep TVar x -> TVar) -> Generic TVar
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
$cfrom :: forall x. TVar -> Rep TVar x
from :: forall x. TVar -> Rep TVar x
$cto :: forall x. Rep TVar x -> TVar
to :: forall x. Rep TVar x -> TVar
Generic, TVar -> ()
(TVar -> ()) -> NFData TVar
forall a. (a -> ()) -> NFData a
$crnf :: TVar -> ()
rnf :: 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]
(Int -> TVarInfo -> ShowS)
-> (TVarInfo -> [Char]) -> ([TVarInfo] -> ShowS) -> Show TVarInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TVarInfo -> ShowS
showsPrec :: Int -> TVarInfo -> ShowS
$cshow :: TVarInfo -> [Char]
show :: TVarInfo -> [Char]
$cshowList :: [TVarInfo] -> ShowS
showList :: [TVarInfo] -> ShowS
Show, (forall x. TVarInfo -> Rep TVarInfo x)
-> (forall x. Rep TVarInfo x -> TVarInfo) -> Generic TVarInfo
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
$cfrom :: forall x. TVarInfo -> Rep TVarInfo x
from :: forall x. TVarInfo -> Rep TVarInfo x
$cto :: forall x. Rep TVarInfo x -> TVarInfo
to :: forall x. Rep TVarInfo x -> TVarInfo
Generic, TVarInfo -> ()
(TVarInfo -> ()) -> NFData TVarInfo
forall a. (a -> ()) -> NFData a
$crnf :: TVarInfo -> ()
rnf :: 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
                | CasedExpression
                | ConPat
                | TypeErrorPlaceHolder
                  deriving (Int -> TypeSource -> ShowS
[TypeSource] -> ShowS
TypeSource -> [Char]
(Int -> TypeSource -> ShowS)
-> (TypeSource -> [Char])
-> ([TypeSource] -> ShowS)
-> Show TypeSource
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TypeSource -> ShowS
showsPrec :: Int -> TypeSource -> ShowS
$cshow :: TypeSource -> [Char]
show :: TypeSource -> [Char]
$cshowList :: [TypeSource] -> ShowS
showList :: [TypeSource] -> ShowS
Show, (forall x. TypeSource -> Rep TypeSource x)
-> (forall x. Rep TypeSource x -> TypeSource) -> Generic TypeSource
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
$cfrom :: forall x. TypeSource -> Rep TypeSource x
from :: forall x. TypeSource -> Rep TypeSource x
$cto :: forall x. Rep TypeSource x -> TypeSource
to :: forall x. Rep TypeSource x -> TypeSource
Generic, TypeSource -> ()
(TypeSource -> ()) -> NFData TypeSource
forall a. (a -> ()) -> NFData a
$crnf :: TypeSource -> ()
rnf :: 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]
(Int -> ArgDescr -> ShowS)
-> (ArgDescr -> [Char]) -> ([ArgDescr] -> ShowS) -> Show ArgDescr
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ArgDescr -> ShowS
showsPrec :: Int -> ArgDescr -> ShowS
$cshow :: ArgDescr -> [Char]
show :: ArgDescr -> [Char]
$cshowList :: [ArgDescr] -> ShowS
showList :: [ArgDescr] -> ShowS
Show,(forall x. ArgDescr -> Rep ArgDescr x)
-> (forall x. Rep ArgDescr x -> ArgDescr) -> Generic ArgDescr
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
$cfrom :: forall x. ArgDescr -> Rep ArgDescr x
from :: forall x. ArgDescr -> Rep ArgDescr x
$cto :: forall x. Rep ArgDescr x -> ArgDescr
to :: forall x. Rep ArgDescr x -> ArgDescr
Generic,ArgDescr -> ()
(ArgDescr -> ()) -> NFData ArgDescr
forall a. (a -> ()) -> NFData a
$crnf :: ArgDescr -> ()
rnf :: ArgDescr -> ()
NFData)

noArgDescr :: ArgDescr
noArgDescr :: ArgDescr
noArgDescr = ArgDescr { argDescrFun :: Maybe Name
argDescrFun = Maybe Name
forall a. Maybe a
Nothing, argDescrNumber :: Maybe Int
argDescrNumber = Maybe Int
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 -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
    TVFromSignature Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
    TypeParamInstNamed Name
x Ident
_ -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
    TypeParamInstPos Name
x Int
_ -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
    DefinitionOf Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
    TypeOfArg ArgDescr
x -> ArgDescr -> Maybe Name
argDescrFun ArgDescr
x
    TypeSource
_ -> Maybe Name
forall a. Maybe a
Nothing


-- | A type annotated with information on how it came about.
data TypeWithSource = WithSource
  { TypeWithSource -> Prop
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 -> [Prop]
tsConstraints :: [Prop]     -- ^ Ensure body is OK
                    , TySyn -> Prop
tsDef         :: Type       -- ^ Definition
                    , TySyn -> Maybe Text
tsDoc         :: !(Maybe Text) -- ^ Documentation
                    }
              deriving (Int -> TySyn -> ShowS
[TySyn] -> ShowS
TySyn -> [Char]
(Int -> TySyn -> ShowS)
-> (TySyn -> [Char]) -> ([TySyn] -> ShowS) -> Show TySyn
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TySyn -> ShowS
showsPrec :: Int -> TySyn -> ShowS
$cshow :: TySyn -> [Char]
show :: TySyn -> [Char]
$cshowList :: [TySyn] -> ShowS
showList :: [TySyn] -> ShowS
Show, (forall x. TySyn -> Rep TySyn x)
-> (forall x. Rep TySyn x -> TySyn) -> Generic TySyn
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
$cfrom :: forall x. TySyn -> Rep TySyn x
from :: forall x. TySyn -> Rep TySyn x
$cto :: forall x. Rep TySyn x -> TySyn
to :: forall x. Rep TySyn x -> TySyn
Generic, TySyn -> ()
(TySyn -> ()) -> NFData TySyn
forall a. (a -> ()) -> NFData a
$crnf :: TySyn -> ()
rnf :: TySyn -> ()
NFData)





-- | Nominal types
data NominalType = NominalType
  { NominalType -> Name
ntName        :: Name
  , NominalType -> [TParam]
ntParams      :: [TParam]
  , NominalType -> Kind
ntKind        :: !Kind             -- ^ Result kind
  , NominalType -> [Prop]
ntConstraints :: [Prop]
  , NominalType -> NominalTypeDef
ntDef         :: NominalTypeDef
  , NominalType -> Maybe Fixity
ntFixity      :: !(Maybe Fixity)
  , NominalType -> Maybe Text
ntDoc         :: Maybe Text
  } deriving (Int -> NominalType -> ShowS
[NominalType] -> ShowS
NominalType -> [Char]
(Int -> NominalType -> ShowS)
-> (NominalType -> [Char])
-> ([NominalType] -> ShowS)
-> Show NominalType
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NominalType -> ShowS
showsPrec :: Int -> NominalType -> ShowS
$cshow :: NominalType -> [Char]
show :: NominalType -> [Char]
$cshowList :: [NominalType] -> ShowS
showList :: [NominalType] -> ShowS
Show, (forall x. NominalType -> Rep NominalType x)
-> (forall x. Rep NominalType x -> NominalType)
-> Generic NominalType
forall x. Rep NominalType x -> NominalType
forall x. NominalType -> Rep NominalType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NominalType -> Rep NominalType x
from :: forall x. NominalType -> Rep NominalType x
$cto :: forall x. Rep NominalType x -> NominalType
to :: forall x. Rep NominalType x -> NominalType
Generic, NominalType -> ()
(NominalType -> ()) -> NFData NominalType
forall a. (a -> ()) -> NFData a
$crnf :: NominalType -> ()
rnf :: NominalType -> ()
NFData)

-- | Definition of a nominal type
data NominalTypeDef =
    Struct StructCon
  | Enum [EnumCon]
  | Abstract
  deriving (Int -> NominalTypeDef -> ShowS
[NominalTypeDef] -> ShowS
NominalTypeDef -> [Char]
(Int -> NominalTypeDef -> ShowS)
-> (NominalTypeDef -> [Char])
-> ([NominalTypeDef] -> ShowS)
-> Show NominalTypeDef
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NominalTypeDef -> ShowS
showsPrec :: Int -> NominalTypeDef -> ShowS
$cshow :: NominalTypeDef -> [Char]
show :: NominalTypeDef -> [Char]
$cshowList :: [NominalTypeDef] -> ShowS
showList :: [NominalTypeDef] -> ShowS
Show, (forall x. NominalTypeDef -> Rep NominalTypeDef x)
-> (forall x. Rep NominalTypeDef x -> NominalTypeDef)
-> Generic NominalTypeDef
forall x. Rep NominalTypeDef x -> NominalTypeDef
forall x. NominalTypeDef -> Rep NominalTypeDef x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NominalTypeDef -> Rep NominalTypeDef x
from :: forall x. NominalTypeDef -> Rep NominalTypeDef x
$cto :: forall x. Rep NominalTypeDef x -> NominalTypeDef
to :: forall x. Rep NominalTypeDef x -> NominalTypeDef
Generic, NominalTypeDef -> ()
(NominalTypeDef -> ()) -> NFData NominalTypeDef
forall a. (a -> ()) -> NFData a
$crnf :: NominalTypeDef -> ()
rnf :: NominalTypeDef -> ()
NFData)

-- | Constructor for a struct (aka newtype)
data StructCon = StructCon
  { StructCon -> Name
ntConName     :: !Name
  , StructCon -> RecordMap Ident Prop
ntFields      :: RecordMap Ident Type
  } deriving (Int -> StructCon -> ShowS
[StructCon] -> ShowS
StructCon -> [Char]
(Int -> StructCon -> ShowS)
-> (StructCon -> [Char])
-> ([StructCon] -> ShowS)
-> Show StructCon
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> StructCon -> ShowS
showsPrec :: Int -> StructCon -> ShowS
$cshow :: StructCon -> [Char]
show :: StructCon -> [Char]
$cshowList :: [StructCon] -> ShowS
showList :: [StructCon] -> ShowS
Show, (forall x. StructCon -> Rep StructCon x)
-> (forall x. Rep StructCon x -> StructCon) -> Generic StructCon
forall x. Rep StructCon x -> StructCon
forall x. StructCon -> Rep StructCon x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. StructCon -> Rep StructCon x
from :: forall x. StructCon -> Rep StructCon x
$cto :: forall x. Rep StructCon x -> StructCon
to :: forall x. Rep StructCon x -> StructCon
Generic, StructCon -> ()
(StructCon -> ()) -> NFData StructCon
forall a. (a -> ()) -> NFData a
$crnf :: StructCon -> ()
rnf :: StructCon -> ()
NFData)

-- | Constructor for an enumeration
data EnumCon = EnumCon
  { EnumCon -> Name
ecName        :: Name
  , EnumCon -> Int
ecNumber      :: !Int -- ^ Number of constructor in the declaration
  , EnumCon -> [Prop]
ecFields      :: [Type]
  , EnumCon -> Bool
ecPublic      :: Bool
  , EnumCon -> Maybe Text
ecDoc         :: Maybe Text
  } deriving (Int -> EnumCon -> ShowS
[EnumCon] -> ShowS
EnumCon -> [Char]
(Int -> EnumCon -> ShowS)
-> (EnumCon -> [Char]) -> ([EnumCon] -> ShowS) -> Show EnumCon
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EnumCon -> ShowS
showsPrec :: Int -> EnumCon -> ShowS
$cshow :: EnumCon -> [Char]
show :: EnumCon -> [Char]
$cshowList :: [EnumCon] -> ShowS
showList :: [EnumCon] -> ShowS
Show,(forall x. EnumCon -> Rep EnumCon x)
-> (forall x. Rep EnumCon x -> EnumCon) -> Generic EnumCon
forall x. Rep EnumCon x -> EnumCon
forall x. EnumCon -> Rep EnumCon x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. EnumCon -> Rep EnumCon x
from :: forall x. EnumCon -> Rep EnumCon x
$cto :: forall x. Rep EnumCon x -> EnumCon
to :: forall x. Rep EnumCon x -> EnumCon
Generic,EnumCon -> ()
(EnumCon -> ()) -> NFData EnumCon
forall a. (a -> ()) -> NFData a
$crnf :: EnumCon -> ()
rnf :: EnumCon -> ()
NFData)


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

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


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

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

instance HasKind Type where
  kindOf :: Prop -> Kind
kindOf Prop
ty =
    case Prop
ty of
      TVar TVar
a      -> TVar -> Kind
forall t. HasKind t => t -> Kind
kindOf TVar
a
      TCon TCon
c [Prop]
ts   -> Kind -> [Prop] -> Kind
forall a. Kind -> [a] -> Kind
quickApply (TCon -> Kind
forall t. HasKind t => t -> Kind
kindOf TCon
c) [Prop]
ts
      TUser Name
_ [Prop]
_ Prop
t -> Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf Prop
t
      TRec {}     -> Kind
KType
      TNominal NominalType
nt [Prop]
ts ->
        case NominalType -> NominalTypeDef
ntDef NominalType
nt of
          Struct {} -> Kind
KType
          Enum {}   -> Kind
KType
          NominalTypeDef
Abstract  -> Kind -> [Prop] -> Kind
forall a. Kind -> [a] -> Kind
quickApply (NominalType -> Kind
forall t. HasKind t => t -> Kind
kindOf NominalType
nt) [Prop]
ts

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

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

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

quickApply :: Kind -> [a] -> Kind
quickApply :: forall a. Kind -> [a] -> Kind
quickApply Kind
k []               = Kind
k
quickApply (Kind
_ :-> Kind
k) (a
_ : [a]
ts) = Kind -> [a] -> Kind
forall a. Kind -> [a] -> Kind
quickApply Kind
k [a]
ts
quickApply Kind
k [a]
_                = [Char] -> [[Char]] -> Kind
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"Cryptol.TypeCheck.AST.quickApply"
                                  [ [Char]
"Applying a non-function kind:", Kind -> [Char]
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
_ [Prop]
_ Prop
x == :: Prop -> Prop -> Bool
== Prop
y        = Prop
x Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
y
  Prop
x == TUser Name
_ [Prop]
_ Prop
y        = Prop
y Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
x

  TCon TCon
x [Prop]
xs == TCon TCon
y [Prop]
ys  = TCon
x TCon -> TCon -> Bool
forall a. Eq a => a -> a -> Bool
== TCon
y Bool -> Bool -> Bool
&& [Prop]
xs [Prop] -> [Prop] -> Bool
forall a. Eq a => a -> a -> Bool
== [Prop]
ys
  TVar TVar
x    == TVar TVar
y     = TVar
x TVar -> TVar -> Bool
forall a. Eq a => a -> a -> Bool
== TVar
y
  TRec RecordMap Ident Prop
xs   == TRec RecordMap Ident Prop
ys    = RecordMap Ident Prop
xs RecordMap Ident Prop -> RecordMap Ident Prop -> Bool
forall a. Eq a => a -> a -> Bool
== RecordMap Ident Prop
ys
  TNominal NominalType
ntx [Prop]
xs == TNominal NominalType
nty [Prop]
ys = NominalType
ntx NominalType -> NominalType -> Bool
forall a. Eq a => a -> a -> Bool
== NominalType
nty Bool -> Bool -> Bool
&& [Prop]
xs [Prop] -> [Prop] -> Bool
forall a. Eq a => a -> a -> Bool
== [Prop]
ys

  Prop
_         == Prop
_          = Bool
False

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

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

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

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

      (TNominal NominalType
x [Prop]
xs, TNominal NominalType
y [Prop]
ys) -> (NominalType, [Prop]) -> (NominalType, [Prop]) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (NominalType
x,[Prop]
xs) (NominalType
y,[Prop]
ys)

instance Eq TParam where
  TParam
x == :: TParam -> TParam -> Bool
== TParam
y = TParam -> Int
tpUnique TParam
x Int -> Int -> Bool
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 = Int -> Int -> Ordering
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 -> TVar
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 :: Prop -> Set Prop
superclassSet (TCon (PC PC
PPrime) [Prop
n]) =
  [Prop] -> Set Prop
forall a. Ord a => [a] -> Set a
Set.fromList [ Prop -> Prop
pFin Prop
n, Prop
n Prop -> Prop -> Prop
>== Prop
tTwo ]

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

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

superclassSet Prop
_ = Set Prop
forall a. Monoid a => a
mempty


nominalTypeConTypes :: NominalType -> [(Name,Schema)]
nominalTypeConTypes :: NominalType -> [(Name, Schema)]
nominalTypeConTypes NominalType
nt =
  case NominalType -> NominalTypeDef
ntDef NominalType
nt of
    Struct StructCon
s -> [ ( StructCon -> Name
ntConName StructCon
s
                  , [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
ctrs (RecordMap Ident Prop -> Prop
TRec (StructCon -> RecordMap Ident Prop
ntFields StructCon
s) Prop -> Prop -> Prop
`tFun` Prop
resT)
                  ) ]
    Enum [EnumCon]
cs  -> [ ( EnumCon -> Name
ecName EnumCon
c
                  , [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as [Prop]
ctrs ((Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Prop -> Prop
tFun Prop
resT (EnumCon -> [Prop]
ecFields EnumCon
c))
                  )
                | EnumCon
c <- [EnumCon]
cs
                ]
    NominalTypeDef
Abstract -> []
  where
  as :: [TParam]
as    = NominalType -> [TParam]
ntParams NominalType
nt
  ctrs :: [Prop]
ctrs  = NominalType -> [Prop]
ntConstraints NominalType
nt
  resT :: Prop
resT  = NominalType -> [Prop] -> Prop
TNominal NominalType
nt ((TParam -> Prop) -> [TParam] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Prop
TVar (TVar -> Prop) -> (TParam -> TVar) -> TParam -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
tpVar) [TParam]
as)

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

instance Eq TVar where
  TVBound TParam
x       == :: TVar -> TVar -> Bool
== TVBound TParam
y       = TParam
x TParam -> TParam -> Bool
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 Int -> Int -> Bool
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
_) = Int -> Int -> Ordering
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) = TParam -> TParam -> Ordering
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 :: Prop -> Maybe Prop
tIsError Prop
ty = case Prop -> Prop
tNoUser Prop
ty of
                TCon (TError Kind
_) [Prop
t] -> Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t
                TCon (TError Kind
_) [Prop]
_   -> [Char] -> [[Char]] -> Maybe Prop
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"tIsError" [[Char]
"Malformed error"]
                Prop
_                   -> Maybe Prop
forall a. Maybe a
Nothing

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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






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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

            PC
_ -> [Prop]
forall {a}. a
bad

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

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

    Prop
_ -> [Prop]
forall {a}. a
bad

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


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

noFreeVariables :: FVS t => t -> Bool
noFreeVariables :: forall t. FVS t => t -> Bool
noFreeVariables = (TVar -> Bool) -> [TVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (TVar -> Bool) -> TVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TVar -> Bool
isFreeTV) ([TVar] -> Bool) -> (t -> [TVar]) -> t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (Set TVar -> [TVar]) -> (t -> Set TVar) -> t -> [TVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Set TVar
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 = [Set TParam] -> Set TParam
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((TVar -> Set TParam) -> [TVar] -> [Set TParam]
forall a b. (a -> b) -> [a] -> [b]
map TVar -> Set TParam
params (Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (t -> Set TVar
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) = TParam -> Set TParam
forall a. a -> Set a
Set.singleton TParam
tp

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

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


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

instance FVS a => FVS [a] where
  fvs :: [a] -> Set TVar
fvs [a]
xs        = [Set TVar] -> Set TVar
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((a -> Set TVar) -> [a] -> [Set TVar]
forall a b. (a -> b) -> [a] -> [b]
map a -> Set TVar
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) = Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
Set.union (a -> Set TVar
forall t. FVS t => t -> Set TVar
fvs a
x) (b -> Set TVar
forall t. FVS t => t -> Set TVar
fvs b
y)

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

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

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

instance PP (WithNames TParam) where
  ppPrec :: Int -> WithNames TParam -> Doc
ppPrec Int
_ (WithNames TParam
p NameMap
mp) = NameMap -> TVar -> Doc
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 = ((Int, [Char]) -> NameMap -> NameMap)
-> NameMap -> [(Int, [Char])] -> NameMap
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Int -> [Char] -> NameMap -> NameMap)
-> (Int, [Char]) -> NameMap -> NameMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> [Char] -> NameMap -> NameMap
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert) NameMap
ns
                ([(Int, [Char])] -> NameMap) -> [(Int, [Char])] -> NameMap
forall a b. (a -> b) -> a -> b
$ [(Int, [Char])]
named [(Int, [Char])] -> [(Int, [Char])] -> [(Int, [Char])]
forall a. [a] -> [a] -> [a]
++ [Int] -> [[Char]] -> [(Int, [Char])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
unnamed_nums [[Char]]
numNames
                        [(Int, [Char])] -> [(Int, [Char])] -> [(Int, [Char])]
forall a. [a] -> [a] -> [a]
++ [Int] -> [[Char]] -> [(Int, [Char])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
unnamed_vals [[Char]]
valNames

  where avail :: [[Char]] -> [[Char]]
avail [[Char]]
xs = ([Char] -> Bool) -> [[Char]] -> [[Char]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Char] -> [[Char]] -> Bool
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,Doc -> [Char]
forall a. Show a => a -> [Char]
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
n)) | (Int
u,Just Name
n,Kind
_)  <- (TParam -> (Int, Maybe Name, Kind))
-> [TParam] -> [(Int, Maybe Name, 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)  <- (TParam -> (Int, Maybe Name, Kind))
-> [TParam] -> [(Int, Maybe Name, Kind)]
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) <- (TParam -> (Int, Maybe Name, Kind))
-> [TParam] -> [(Int, Maybe Name, Kind)]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> (Int, Maybe Name, Kind)
nm [TParam]
as ]

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

ppNominalShort :: NominalType -> Doc
ppNominalShort :: NominalType -> Doc
ppNominalShort NominalType
nt =
  Doc
kw Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp (NominalType -> Name
ntName NominalType
nt) Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ((TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> Int -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
9) [TParam]
ps)
  where
  ps :: [TParam]
ps = NominalType -> [TParam]
ntParams NominalType
nt
  nm :: NameMap
nm = [TParam] -> NameMap -> NameMap
addTNames [TParam]
ps NameMap
emptyNameMap
  kw :: Doc
kw = case NominalType -> NominalTypeDef
ntDef NominalType
nt of
         Struct {} -> Doc
"newtype"
         Enum {}   -> Doc
"enum"
         Abstract {} -> Doc
"primitive type"

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

    Struct StructCon
con -> Doc -> Doc -> Doc
ppKWDef Doc
"newtype" (Doc
"=" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp (StructCon -> Name
ntConName StructCon
con) Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 Doc
fs)
      where fs :: Doc
fs = [Doc] -> Doc
vcat [ Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
f Doc -> Doc -> Doc
<.> Doc
":" Doc -> Doc -> Doc
<+> Prop -> Doc
forall a. PP a => a -> Doc
pp Prop
t
                      | (Ident
f,Prop
t) <- RecordMap Ident Prop -> [(Ident, Prop)]
forall a b. RecordMap a b -> [(a, b)]
canonicalFields (StructCon -> RecordMap Ident Prop
ntFields StructCon
con) ]
    Enum [EnumCon]
cons ->
      Doc -> Doc -> Doc
ppKWDef Doc
"enum" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
      [Doc] -> Doc
vcat [ Doc
pref Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp (EnumCon -> Name
ecName EnumCon
con) Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Prop -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
1) (EnumCon -> [Prop]
ecFields EnumCon
con))
           | (Doc
pref,EnumCon
con) <- [Doc] -> [EnumCon] -> [(Doc, EnumCon)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Doc
"=" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: Doc -> [Doc]
forall a. a -> [a]
repeat Doc
"|") [EnumCon]
cons
           ]

    NominalTypeDef
Abstract ->
      Doc
"primitive type" Doc -> Doc -> Doc
<+> Doc
paramBinds Doc -> Doc -> Doc
<+> Doc
ctrs Doc -> Doc -> Doc
<+> Doc
ppTyUse Doc -> Doc -> Doc
<+>
                                                        Doc
":" Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. PP a => a -> Doc
pp (NominalType -> Kind
ntKind NominalType
nt)
      where
      paramBinds :: Doc
paramBinds =
        case [TParam]
ps of
          [] -> Doc
forall a. Monoid a => a
mempty
          [TParam]
_  -> Doc -> Doc
braces ([Doc] -> Doc
commaSep ((TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> Doc
forall {t}. (PP (WithNames t), HasKind t) => t -> Doc
ppBind [TParam]
ps))
      ppBind :: t -> Doc
ppBind t
p = NameMap -> Int -> t -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
0 t
p Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. PP a => a -> Doc
pp (t -> Kind
forall t. HasKind t => t -> Kind
kindOf t
p)
      ppC :: Prop -> Doc
ppC     = NameMap -> Int -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
0
      ctrs :: Doc
ctrs = case NominalType -> [Prop]
ntConstraints NominalType
nt of
               [] -> Doc
forall a. Monoid a => a
mempty
               [Prop]
_  -> Doc -> Doc
parens ([Doc] -> Doc
commaSep ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Doc
ppC (NominalType -> [Prop]
ntConstraints NominalType
nt))) Doc -> Doc -> Doc
<+> Doc
"=>"
  where
  ps :: [TParam]
ps = NominalType -> [TParam]
ntParams NominalType
nt
  cs :: Doc
cs = [Doc] -> Doc
vcat ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Doc
forall a. PP a => a -> Doc
pp (NominalType -> [Prop]
ntConstraints NominalType
nt))
  nm :: NameMap
nm = [TParam] -> NameMap -> NameMap
addTNames [TParam]
ps NameMap
emptyNameMap
  ppTyUse :: Doc
ppTyUse = Name -> Doc
forall a. PP a => a -> Doc
pp (NominalType -> Name
ntName NominalType
nt) Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep ((TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> Int -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
9) [TParam]
ps)
  ppKWDef :: Doc -> Doc -> Doc
ppKWDef Doc
kw Doc
def = (Doc
kw Doc -> Doc -> Doc
<+> Doc
ppTyUse) Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Doc
cs Doc -> Doc -> Doc
$$ Doc
def)



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

instance PP (WithNames Schema) where
  ppPrec :: Int -> WithNames Schema -> Doc
ppPrec Int
_ (WithNames Schema
s NameMap
ns)
    | [TParam] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [TParam]
sVars Schema
s) Bool -> Bool -> Bool
&& [Prop] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [Prop]
sProps Schema
s) = Doc
body
    | Bool
otherwise = Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
sep ([Doc]
vars [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
props [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
body]))
    where
    body :: Doc
body = NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 (Schema -> Prop
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 ((TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [TParam]
vs)))]

    props :: [Doc]
props = case Schema -> [Prop]
sProps Schema
s of
      [] -> []
      [Prop]
ps -> [Int -> Doc -> Doc
nest Int
1 (Doc -> Doc
parens ([Doc] -> Doc
commaSepFill ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [Prop]
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 = NameMap -> Int -> TySyn -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
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 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep
      [ [Doc] -> Doc
fsep ([[Char] -> Doc
text [Char]
"type"] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
ctr [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
lhs [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Char -> Doc
char Char
'='])
      , NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 (TySyn -> Prop
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 (TySyn -> Kind
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]) ->
                    [NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 TParam
x, Ident -> Doc
forall a. PP a => a -> Doc
pp (Name -> Ident
nameIdent Name
n), NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 TParam
y]
                  (Maybe Fixity
_, [TParam]
ps) ->
                    [Name -> Doc
forall a. PP a => a -> Doc
pp Name
n] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [TParam]
ps

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

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

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

      TUser Name
c [Prop]
ts Prop
t ->
        (NameDisp -> Doc) -> Doc
withNameDisp ((NameDisp -> Doc) -> Doc) -> (NameDisp -> Doc) -> Doc
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 ->
              Int -> Prop -> Doc
forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
prec Prop
t -- unfold type synonym if not in scope
          Maybe OrigName
_ ->
            case [Prop]
ts of
              [] -> Name -> Doc
forall a. PP a => a -> Doc
pp Name
c
              [Prop]
_ -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep (Name -> Doc
forall a. PP a => a -> Doc
pp Name
c Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Prop -> Doc
forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5) [Prop]
ts)

      TCon (TC TC
tc) [Prop]
ts ->
        case (TC
tc,[Prop]
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, [Prop
n])     -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"Z" Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall {a}. PP (WithNames a) => Int -> a -> Doc
go Int
5 Prop
n

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

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

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

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

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

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

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

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

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

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

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

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

    isTInfix WithNames Prop
_ = Maybe (Infix Ident (WithNames Prop))
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 <- Int -> NameMap -> Maybe [Char]
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 = a -> Doc
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     -> Name -> Doc
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  -> Name -> Doc
forall a. PP a => a -> Doc
declNm Name
n
                TPTySynParam Name
n   -> Name -> Doc
forall a. PP a => a -> Doc
declNm Name
n
                TPPropSynParam Name
n -> Name -> Doc
forall a. PP a => a -> Doc
declNm Name
n
                TPNominalParam Name
n -> Name -> Doc
forall a. PP a => a -> Doc
declNm Name
n
                TPPrimParam Name
n    -> Name -> Doc
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 ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$
  case TypeSource
src of
    TVFromModParam Name
n       -> Name -> [Char]
forall a. PP a => a -> [Char]
using Name
n
    TVFromSignature Name
n      -> Name -> [Char]
forall a. PP a => a -> [Char]
using Name
n
    TypeSource
TypeWildCard           -> ShowS
mk ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ case Kind
k of
                                     Kind
KNum -> [Char]
"n"
                                     Kind
_    -> [Char]
"a"
    TypeOfRecordField Ident
i    -> Ident -> [Char]
forall a. PP a => a -> [Char]
using Ident
i
    TypeOfTupleField Int
n     -> ShowS
mk ([Char]
"tup_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
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 -> Ident -> [Char]
forall a. PP a => a -> [Char]
using Ident
i
    TypeParamInstPos Name
f Int
n   -> ShowS
mk (Name -> [Char]
forall a. PP a => a -> [Char]
sh Name
f [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
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 ModPath -> ModPath -> Bool
forall a. Eq a => a -> a -> Bool
== ModName -> ModPath
TopModule ModName
exprModName -> ShowS
mk [Char]
"it"
        NameInfo
_ -> Name -> [Char]
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_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
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"
    TypeSource
CasedExpression        -> [Char]
"case"
    TypeSource
ConPat                 -> [Char]
"conp"
  where
  sh :: a -> [Char]
sh a
a      = Doc -> [Char]
forall a. Show a => a -> [Char]
show (a -> Doc
forall a. PP a => a -> Doc
pp a
a)
  using :: a -> [Char]
using a
a   = ShowS
mk (a -> [Char]
forall a. PP a => a -> [Char]
sh a
a)
  mk :: ShowS
mk [Char]
a      = [Char]
a [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"`" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
uni

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

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

instance PP TVarInfo where
  ppPrec :: Int -> TVarInfo -> Doc
ppPrec Int
_ TVarInfo
tvinfo = [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [TypeSource -> Doc
forall a. PP a => a -> Doc
pp (TVarInfo -> TypeSource
tvarDesc TVarInfo
tvinfo)] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
loc
    where
    loc :: [Doc]
loc = if Range
rng Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Range
emptyRange then [] else [Doc
"at" Doc -> Doc -> Doc
<+> Range -> 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"] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
ofFun)
        where
        which :: Doc
which = Doc -> (Int -> Doc) -> Maybe Int -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"function" Int -> Doc
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
<+> Name -> 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
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
m
      TVFromSignature Name
x   -> Doc
"signature variable" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Name -> Doc
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 (Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
l)
      TypeOfTupleField Int
n  -> Doc
"type of" Doc -> Doc -> Doc
<+> Int -> 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 (Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
i) Doc -> Doc -> Doc
<+>
                                          Doc
"of" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Name -> Doc
forall a. PP a => a -> Doc
pp Name
f)
      TypeParamInstPos   Name
f Int
i -> Int -> Doc
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 (Name -> Doc
forall a. PP a => a -> Doc
pp Name
f)
      DefinitionOf Name
x      -> Doc
"the type of" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Name -> Doc
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
<+> ArgDescr -> 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"
      TypeSource
CasedExpression       -> Doc
"cased expression"
      TypeSource
ConPat                -> Doc
"constructor pattern"

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