{-# Language Safe, DeriveGeneric, DeriveAnyClass, RecordWildCards #-}
{-# Language FlexibleInstances, FlexibleContexts #-}
{-# Language PatternGuards #-}
{-# Language OverloadedStrings #-}
module Cryptol.TypeCheck.Type
  ( module Cryptol.TypeCheck.Type
  , module Cryptol.TypeCheck.TCon
  ) where


import GHC.Generics (Generic)
import Control.DeepSeq

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(Range,emptyRange)
import Cryptol.ModuleSystem.Name
import Cryptol.Utils.Ident (Ident, isInfixIdent, exprModName)
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`



-- | 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
/= :: Schema -> Schema -> Bool
$c/= :: Schema -> Schema -> Bool
== :: Schema -> Schema -> Bool
$c== :: Schema -> Schema -> Bool
Eq, Int -> Schema -> ShowS
[Schema] -> ShowS
Schema -> String
(Int -> Schema -> ShowS)
-> (Schema -> String) -> ([Schema] -> ShowS) -> Show Schema
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Schema] -> ShowS
$cshowList :: [Schema] -> ShowS
show :: Schema -> String
$cshow :: Schema -> String
showsPrec :: Int -> Schema -> ShowS
$cshowsPrec :: Int -> 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
$cto :: forall x. Rep Schema x -> Schema
$cfrom :: forall x. Schema -> Rep Schema x
Generic, Schema -> ()
(Schema -> ()) -> NFData Schema
forall a. (a -> ()) -> NFData a
rnf :: Schema -> ()
$crnf :: Schema -> ()
NFData)

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

data TPFlavor = TPModParam Name
              | TPOther (Maybe 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
$cto :: forall x. Rep TPFlavor x -> TPFlavor
$cfrom :: forall x. TPFlavor -> Rep TPFlavor x
Generic, TPFlavor -> ()
(TPFlavor -> ()) -> NFData TPFlavor
forall a. (a -> ()) -> NFData a
rnf :: TPFlavor -> ()
$crnf :: TPFlavor -> ()
NFData, Int -> TPFlavor -> ShowS
[TPFlavor] -> ShowS
TPFlavor -> String
(Int -> TPFlavor -> ShowS)
-> (TPFlavor -> String) -> ([TPFlavor] -> ShowS) -> Show TPFlavor
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TPFlavor] -> ShowS
$cshowList :: [TPFlavor] -> ShowS
show :: TPFlavor -> String
$cshow :: TPFlavor -> String
showsPrec :: Int -> TPFlavor -> ShowS
$cshowsPrec :: Int -> 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
x = Maybe Name -> TPFlavor
TPOther (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x)

tySynParam :: Name -> TPFlavor
tySynParam :: Name -> TPFlavor
tySynParam Name
x = Maybe Name -> TPFlavor
TPOther (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x)

propSynParam :: Name -> TPFlavor
propSynParam :: Name -> TPFlavor
propSynParam Name
x = Maybe Name -> TPFlavor
TPOther (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x)

newtypeParam :: Name -> TPFlavor
newtypeParam :: Name -> TPFlavor
newtypeParam Name
x = Maybe Name -> TPFlavor
TPOther (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x)

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
    TPModParam Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
    TPOther Maybe Name
x -> Maybe 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

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

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

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

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


-- | Explains how this type came to be, for better error messages.
data TypeSource = TVFromModParam Name     -- ^ Name of module parameter
                | TVFromSignature Name    -- ^ A variable in a signature
                | TypeWildCard
                | TypeOfRecordField Ident
                | TypeOfTupleField Int
                | TypeOfSeqElement
                | LenOfSeq
                | TypeParamInstNamed {-Fun-}Name {-Param-}Ident
                | TypeParamInstPos   {-Fun-}Name {-Pos (from 1)-}Int
                | DefinitionOf Name
                | LenOfCompGen
                | TypeOfArg ArgDescr
                | TypeOfRes
                | FunApp
                | TypeOfIfCondExpr
                | TypeFromUserAnnotation
                | GeneratorOfListComp
                | TypeErrorPlaceHolder
                  deriving (Int -> TypeSource -> ShowS
[TypeSource] -> ShowS
TypeSource -> String
(Int -> TypeSource -> ShowS)
-> (TypeSource -> String)
-> ([TypeSource] -> ShowS)
-> Show TypeSource
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeSource] -> ShowS
$cshowList :: [TypeSource] -> ShowS
show :: TypeSource -> String
$cshow :: TypeSource -> String
showsPrec :: Int -> TypeSource -> ShowS
$cshowsPrec :: Int -> 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
$cto :: forall x. Rep TypeSource x -> TypeSource
$cfrom :: forall x. TypeSource -> Rep TypeSource x
Generic, TypeSource -> ()
(TypeSource -> ()) -> NFData TypeSource
forall a. (a -> ()) -> NFData a
rnf :: TypeSource -> ()
$crnf :: TypeSource -> ()
NFData)

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

noArgDescr :: ArgDescr
noArgDescr :: ArgDescr
noArgDescr = ArgDescr :: Maybe Name -> Maybe Int -> ArgDescr
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
  }


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





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


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




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


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

instance HasKind TySyn where
  kindOf :: TySyn -> Kind
kindOf TySyn
ts = (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
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 Newtype where
  kindOf :: Newtype -> Kind
kindOf Newtype
nt = (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) Kind
KType ((TParam -> Kind) -> [TParam] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> Kind
forall t. HasKind t => t -> Kind
kindOf (Newtype -> [TParam]
ntParams Newtype
nt))

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

quickApply :: Kind -> [a] -> Kind
quickApply :: 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]
_                = String -> [String] -> Kind
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.AST.quickApply"
                                  [ String
"Applying a non-function kind:", Kind -> String
forall a. Show a => a -> String
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

  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


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
p = TParam -> TVar
TVBound TParam
p

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


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

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

superclassSet :: 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


newtypeConType :: Newtype -> Schema
newtypeConType :: Newtype -> Schema
newtypeConType Newtype
nt =
  [TParam] -> [Prop] -> Prop -> Schema
Forall [TParam]
as (Newtype -> [Prop]
ntConstraints Newtype
nt)
    (Prop -> Schema) -> Prop -> Schema
forall a b. (a -> b) -> a -> b
$ RecordMap Ident Prop -> Prop
TRec ([(Ident, Prop)] -> RecordMap Ident Prop
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields (Newtype -> [(Ident, Prop)]
ntFields Newtype
nt)) Prop -> Prop -> Prop
`tFun` TCon -> [Prop] -> Prop
TCon (Newtype -> TCon
newtypeTyCon Newtype
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)
  where
  as :: [TParam]
as = Newtype -> [TParam]
ntParams Newtype
nt


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

instance Eq TVar where
  TVBound TParam
x       == :: TVar -> TVar -> Bool
== TVBound TParam
y       = TParam
x 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]
_   -> String -> [String] -> Maybe Prop
forall a. HasCallStack => String -> [String] -> a
panic String
"tIsError" [String
"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 (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

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 :: 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

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

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 (t :: * -> *) a. Foldable t => t a -> Int
length [Prop]
ts))) [Prop]
ts

newtypeTyCon :: Newtype -> TCon
newtypeTyCon :: Newtype -> TCon
newtypeTyCon Newtype
nt = TC -> TCon
TC (TC -> TCon) -> TC -> TCon
forall a b. (a -> b) -> a -> b
$ UserTC -> TC
TCNewtype (UserTC -> TC) -> UserTC -> TC
forall a b. (a -> b) -> a -> b
$ Name -> Kind -> UserTC
UserTC (Newtype -> Name
ntName Newtype
nt) (Newtype -> Kind
forall t. HasKind t => t -> Kind
kindOf Newtype
nt)


-- | 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]

-- | 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]


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

noFreeVariables :: FVS t => t -> Bool
noFreeVariables :: 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 :: 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)

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, String) -> NameMap -> NameMap)
-> NameMap -> [(Int, String)] -> NameMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Int -> String -> NameMap -> NameMap)
-> (Int, String) -> NameMap -> NameMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> String -> NameMap -> NameMap
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert) NameMap
ns
                ([(Int, String)] -> NameMap) -> [(Int, String)] -> NameMap
forall a b. (a -> b) -> a -> b
$ [(Int, String)]
named [(Int, String)] -> [(Int, String)] -> [(Int, String)]
forall a. [a] -> [a] -> [a]
++ [Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
unnamed_nums [String]
numNames
                        [(Int, String)] -> [(Int, String)] -> [(Int, String)]
forall a. [a] -> [a] -> [a]
++ [Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
unnamed_vals [String]
valNames

  where avail :: [String] -> [String]
avail [String]
xs = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
used) ([String] -> [String]
nameList [String]
xs)
        numNames :: [String]
numNames = [String] -> [String]
avail [String
"n",String
"m",String
"i",String
"j",String
"k"]
        valNames :: [String]
valNames = [String] -> [String]
avail [String
"a",String
"b",String
"c",String
"d",String
"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, String)]
named        = [ (Int
u,Doc -> String
forall a. Show a => a -> String
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 :: [String]
used    = ((Int, String) -> String) -> [(Int, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, String) -> String
forall a b. (a, b) -> b
snd [(Int, String)]
named [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ NameMap -> [String]
forall a. IntMap a -> [a]
IntMap.elems NameMap
ns

ppNewtypeShort :: Newtype -> Doc
ppNewtypeShort :: Newtype -> Doc
ppNewtypeShort Newtype
nt =
  String -> Doc
text String
"newtype" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp (Newtype -> Name
ntName Newtype
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  = Newtype -> [TParam]
ntParams Newtype
nt
  nm :: NameMap
nm = [TParam] -> NameMap -> NameMap
addTNames [TParam]
ps NameMap
emptyNameMap


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 (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [TParam]
sVars Schema
s) Bool -> Bool -> Bool
&& [Prop] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [Prop]
sProps Schema
s) = Doc
body
    | Bool
otherwise = Doc -> Int -> Doc -> Doc
hang (Doc
vars Doc -> Doc -> Doc
<+> Doc
props) Int
2 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
      [] -> Doc
empty
      [TParam]
vs -> Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
commaSep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (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
      [] -> Doc
empty
      [Prop]
ps -> Doc -> Doc
parens ([Doc] -> Doc
commaSep ((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
<+> String -> Doc
text String
"=>"

    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) =
    String -> Doc
text String
"type" Doc -> Doc -> Doc
<+> Doc
ctr Doc -> Doc -> Doc
<+> Doc
lhs Doc -> Doc -> Doc
<+> Char -> Doc
char Char
'=' Doc -> Doc -> Doc
<+> 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 -> String -> Doc
text String
"constraint"
                  Kind
_     -> Doc
empty
          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 Doc -> Doc -> Doc
<+> Ident -> Doc
forall a. PP a => a -> Doc
pp (Name -> Ident
nameIdent Name
n) Doc -> Doc -> Doc
<+> 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
<+> [Doc] -> Doc
sep ((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 Newtype where
  ppPrec :: Int -> Newtype -> Doc
ppPrec = NameMap -> Int -> Newtype -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty

instance PP (WithNames Newtype) where
  ppPrec :: Int -> WithNames Newtype -> Doc
ppPrec Int
_  (WithNames Newtype
nt NameMap
_) = Newtype -> Doc
ppNewtypeShort Newtype
nt -- XXX: do the full thing?



-- | The precedence levels used by this pretty-printing instance
-- correspond with parser non-terminals as follows:
--
--   * 0-1: @type@
--
--   * 2: @infix_type@
--
--   * 3: @app_type@
--
--   * 4: @dimensions atype@
--
--   * 5: @atype@
instance PP (WithNames Type) where
  ppPrec :: Int -> WithNames 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
      TRec RecordMap Ident Prop
fs -> Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma
                    [ Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
l Doc -> Doc -> Doc
<+> String -> Doc
text String
":" 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 -> NameInfo
nameInfo Name
c of
          Declared ModName
m NameSource
_
            | NameFormat
NotInScope <- ModName -> Ident -> NameDisp -> NameFormat
getNameFormat ModName
m (Name -> Ident
nameIdent Name
c) 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
          NameInfo
_ ->
            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
$ Name -> Doc
forall a. PP a => a -> Doc
pp Name
c Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((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,   [])       -> String -> Doc
text String
"inf"
          (TC
TCBit,   [])       -> String -> Doc
text String
"Bit"
          (TC
TCInteger, [])     -> String -> Doc
text String
"Integer"
          (TC
TCRational, [])    -> String -> Doc
text String
"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
$ String -> Doc
text String
"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
<+> String -> Doc
text String
"->" 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
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([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
$ TC -> Doc
forall a. PP a => a -> Doc
pp TC
tc Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((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
<+> String -> Doc
text String
"==" 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
<+> String -> Doc
text String
"!=" 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
<+> String -> Doc
text String
">=" 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
$ String -> Doc
text String
"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
$ String -> Doc
text String
"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
<+> String -> Doc
text String
"of"
                               Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
go Int
0 Prop
t1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"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])     -> Doc -> Doc
parens ([Doc] -> Doc
commaSep ((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
_, [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
$ PC -> Doc
forall a. PP a => a -> Doc
pp PC
pc Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((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
$ TCon -> Doc
forall a. PP a => a -> Doc
pp TCon
f Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((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 (m :: * -> *) a. Monad m => a -> m a
return Infix :: forall op thing. op -> thing -> thing -> Fixity -> Infix op thing
Infix { Fixity
Ident
WithNames Prop
ieFixity :: Fixity
ieRight :: WithNames Prop
ieLeft :: WithNames Prop
ieOp :: Ident
ieFixity :: Fixity
ieOp :: Ident
ieRight :: WithNames Prop
ieLeft :: WithNames Prop
.. }

    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 (m :: * -> *) a. Monad m => a -> m a
return Infix :: forall op thing. op -> thing -> thing -> Fixity -> Infix op thing
Infix { Fixity
Ident
WithNames Prop
ieOp :: Ident
ieFixity :: Fixity
ieRight :: WithNames Prop
ieLeft :: WithNames Prop
ieFixity :: Fixity
ieRight :: WithNames Prop
ieLeft :: WithNames Prop
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 String
a <- Int -> NameMap -> Maybe String
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (TVar -> Int
tvUnique TVar
tv) NameMap
mp = String -> Doc
text String
a
      | Bool
otherwise =
          case TVar
tv of
            TVBound TParam
x ->
              case TParam -> TPFlavor
tpFlav TParam
x of
                TPModParam Name
n     -> Name -> Doc
forall a. PPName a => a -> Doc
ppPrefixName Name
n
                TPOther (Just Name
n) -> Name -> Doc
forall a. PP a => a -> Doc
pp Name
n Doc -> Doc -> Doc
<.> Doc
"`" Doc -> Doc -> Doc
<.> Int -> Doc
int (TParam -> Int
tpUnique TParam
x)
                TPFlavor
_  -> Kind -> TypeSource -> Int -> Doc
pickTVarName (TParam -> Kind
tpKind TParam
x) (TVarInfo -> TypeSource
tvarDesc (TParam -> TVarInfo
tpInfo TParam
x)) (TParam -> Int
tpUnique TParam
x)

            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 =
  String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
  case TypeSource
src of
    TVFromModParam Name
n       -> Name -> String
forall a. PP a => a -> String
using Name
n
    TVFromSignature Name
n      -> Name -> String
forall a. PP a => a -> String
using Name
n
    TypeSource
TypeWildCard           -> ShowS
mk ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ case Kind
k of
                                     Kind
KNum -> String
"n"
                                     Kind
_    -> String
"a"
    TypeOfRecordField Ident
i    -> Ident -> String
forall a. PP a => a -> String
using Ident
i
    TypeOfTupleField Int
n     -> ShowS
mk (String
"tup_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)
    TypeSource
TypeOfSeqElement       -> ShowS
mk String
"a"
    TypeSource
LenOfSeq               -> ShowS
mk String
"n"
    TypeParamInstNamed Name
_ Ident
i -> Ident -> String
forall a. PP a => a -> String
using Ident
i
    TypeParamInstPos Name
f Int
n   -> ShowS
mk (Name -> String
forall a. PP a => a -> String
sh Name
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)
    DefinitionOf Name
x ->
      case Name -> NameInfo
nameInfo Name
x of
        Declared ModName
m NameSource
SystemName | ModName
m ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
exprModName -> ShowS
mk String
"it"
        NameInfo
_ -> Name -> String
forall a. PP a => a -> String
using Name
x
    TypeSource
LenOfCompGen           -> ShowS
mk String
"n"
    TypeSource
GeneratorOfListComp    -> String
"seq"
    TypeSource
TypeOfIfCondExpr       -> String
"b"
    TypeOfArg ArgDescr
ad           -> ShowS
mk (case ArgDescr -> Maybe Int
argDescrNumber ArgDescr
ad of
                                    Maybe Int
Nothing -> String
"arg"
                                    Just Int
n  -> String
"arg_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)
    TypeSource
TypeOfRes              -> String
"res"
    TypeSource
FunApp                 -> String
"fun"
    TypeSource
TypeFromUserAnnotation -> String
"user"
    TypeSource
TypeErrorPlaceHolder   -> String
"err"
  where
  sh :: a -> String
sh a
a      = Doc -> String
forall a. Show a => a -> String
show (a -> Doc
forall a. PP a => a -> Doc
pp a
a)
  using :: a -> String
using a
a   = ShowS
mk (a -> String
forall a. PP a => a -> String
sh a
a)
  mk :: ShowS
mk String
a      = String
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
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 = TypeSource -> Doc
forall a. PP a => a -> Doc
pp (TVarInfo -> TypeSource
tvarDesc TVarInfo
tvinfo) Doc -> Doc -> Doc
<+> Doc
loc
    where
    loc :: Doc
loc = if Range
rng Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Range
emptyRange then Doc
empty 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
which Doc -> Doc -> Doc
<+> Doc
"argument" Doc -> Doc -> Doc
<+> 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 -> Doc
empty
                  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"