{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE OverloadedStrings    #-}
{-# LANGUAGE PatternSynonyms      #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Disco.Types
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- The "Disco.Types" module defines the set of types used in the disco
-- language type system, along with various utility functions.
--
-----------------------------------------------------------------------------

-- SPDX-License-Identifier: BSD-3-Clause

module Disco.Types
       (
       -- * Disco language types
       -- ** Atomic types

         BaseTy(..), isCtr, Var(..), Ilk(..), pattern U, pattern S
       , Atom(..)
       , isVar, isBase, isSkolem
       , UAtom(..), uisVar, uatomToAtom, uatomToEither

       -- ** Type constructors

       , Con(..)
       , pattern CList, pattern CBag, pattern CSet

       -- ** Types

       , Type(..)

       , pattern TyVar
       , pattern TySkolem
       , pattern TyVoid
       , pattern TyUnit
       , pattern TyBool
       , pattern TyProp
       , pattern TyN
       , pattern TyZ
       , pattern TyF
       , pattern TyQ
       , pattern TyC
       -- , pattern TyFin
       , pattern (:->:)
       , pattern (:*:)
       , pattern (:+:)
       , pattern TyList
       , pattern TyBag
       , pattern TySet
       , pattern TyGraph
       , pattern TyMap
       , pattern TyContainer
       , pattern TyUser
       , pattern TyString

       -- ** Quantified types

       , PolyType(..)
       , toPolyType, closeType

       -- * Type predicates

       , isNumTy, isEmptyTy, isFiniteTy, isSearchable

       -- * Type substitutions

       , Substitution, atomToTypeSubst, uatomToTypeSubst

       -- * Strictness
       , Strictness(..), strictness

       -- * Utilities
       , isTyVar
       , containerVars
       , countType
       , unpair
       , S
       , TyDefBody(..)
       , TyDefCtx

       -- * HasType class
       , HasType(..)
       )
       where

import           Data.Coerce
import           Data.Data                         (Data)
import           Disco.Data                        ()
import           GHC.Generics                      (Generic)
import           Unbound.Generics.LocallyNameless  hiding (lunbind)

import           Control.Lens                      (toListOf)
import           Data.List                         (nub)
import           Data.Map                          (Map)
import qualified Data.Map                          as M
import           Data.Set                          (Set)
import qualified Data.Set                          as S
import           Data.Void
import           Math.Combinatorics.Exact.Binomial (choose)

import           Disco.Effects.LFresh

import           Disco.Pretty                      hiding ((<>))
import           Disco.Subst                       (Substitution)
import           Disco.Types.Qualifiers

--------------------------------------------------
-- Disco types
--------------------------------------------------

----------------------------------------
-- Base types

-- | Base types are the built-in types which form the basis of the
--   disco type system, out of which more complex types can be built.
data BaseTy where

  -- | The void type, with no inhabitants.
  Void :: BaseTy

  -- | The unit type, with one inhabitant.
  Unit :: BaseTy

  -- | Booleans.
  B    :: BaseTy

  -- | Propositions.
  P    :: BaseTy

  -- | Natural numbers.
  N    :: BaseTy

  -- | Integers.
  Z    :: BaseTy

  -- | Fractionals (i.e. nonnegative rationals).
  F    :: BaseTy

  -- | Rationals.
  Q    :: BaseTy

  -- | Unicode characters.
  C    :: BaseTy

  -- Finite types. The single argument is a natural number defining
  -- the exact number of inhabitants.
  -- Fin  :: Integer -> BaseTy

  -- | Set container type.  It's a bit odd putting these here since
  --   they have kind * -> * and all the other base types have kind *;
  --   but there's nothing fundamentally wrong with it and in
  --   particular this allows us to reuse all the existing constraint
  --   solving machinery for container subtyping.
  CtrSet :: BaseTy

  -- | Bag container type.
  CtrBag :: BaseTy

  -- | List container type.
  CtrList :: BaseTy

  deriving (Int -> BaseTy -> ShowS
[BaseTy] -> ShowS
BaseTy -> String
(Int -> BaseTy -> ShowS)
-> (BaseTy -> String) -> ([BaseTy] -> ShowS) -> Show BaseTy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BaseTy] -> ShowS
$cshowList :: [BaseTy] -> ShowS
show :: BaseTy -> String
$cshow :: BaseTy -> String
showsPrec :: Int -> BaseTy -> ShowS
$cshowsPrec :: Int -> BaseTy -> ShowS
Show, BaseTy -> BaseTy -> Bool
(BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool) -> Eq BaseTy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BaseTy -> BaseTy -> Bool
$c/= :: BaseTy -> BaseTy -> Bool
== :: BaseTy -> BaseTy -> Bool
$c== :: BaseTy -> BaseTy -> Bool
Eq, Eq BaseTy
Eq BaseTy
-> (BaseTy -> BaseTy -> Ordering)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> BaseTy)
-> (BaseTy -> BaseTy -> BaseTy)
-> Ord BaseTy
BaseTy -> BaseTy -> Bool
BaseTy -> BaseTy -> Ordering
BaseTy -> BaseTy -> BaseTy
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: BaseTy -> BaseTy -> BaseTy
$cmin :: BaseTy -> BaseTy -> BaseTy
max :: BaseTy -> BaseTy -> BaseTy
$cmax :: BaseTy -> BaseTy -> BaseTy
>= :: BaseTy -> BaseTy -> Bool
$c>= :: BaseTy -> BaseTy -> Bool
> :: BaseTy -> BaseTy -> Bool
$c> :: BaseTy -> BaseTy -> Bool
<= :: BaseTy -> BaseTy -> Bool
$c<= :: BaseTy -> BaseTy -> Bool
< :: BaseTy -> BaseTy -> Bool
$c< :: BaseTy -> BaseTy -> Bool
compare :: BaseTy -> BaseTy -> Ordering
$ccompare :: BaseTy -> BaseTy -> Ordering
$cp1Ord :: Eq BaseTy
Ord, (forall x. BaseTy -> Rep BaseTy x)
-> (forall x. Rep BaseTy x -> BaseTy) -> Generic BaseTy
forall x. Rep BaseTy x -> BaseTy
forall x. BaseTy -> Rep BaseTy x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BaseTy x -> BaseTy
$cfrom :: forall x. BaseTy -> Rep BaseTy x
Generic, Typeable BaseTy
DataType
Constr
Typeable BaseTy
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> BaseTy -> c BaseTy)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BaseTy)
-> (BaseTy -> Constr)
-> (BaseTy -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BaseTy))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy))
-> ((forall b. Data b => b -> b) -> BaseTy -> BaseTy)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BaseTy -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BaseTy -> r)
-> (forall u. (forall d. Data d => d -> u) -> BaseTy -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy)
-> Data BaseTy
BaseTy -> DataType
BaseTy -> Constr
(forall b. Data b => b -> b) -> BaseTy -> BaseTy
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
$cCtrList :: Constr
$cCtrBag :: Constr
$cCtrSet :: Constr
$cC :: Constr
$cQ :: Constr
$cF :: Constr
$cZ :: Constr
$cN :: Constr
$cP :: Constr
$cB :: Constr
$cUnit :: Constr
$cVoid :: Constr
$tBaseTy :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapMp :: (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapM :: (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapQi :: Int -> (forall d. Data d => d -> u) -> BaseTy -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
gmapQ :: (forall d. Data d => d -> u) -> BaseTy -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
gmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
$cgmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c BaseTy)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
dataTypeOf :: BaseTy -> DataType
$cdataTypeOf :: BaseTy -> DataType
toConstr :: BaseTy -> Constr
$ctoConstr :: BaseTy -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
$cp1Data :: Typeable BaseTy
Data, Show BaseTy
Show BaseTy
-> (AlphaCtx -> BaseTy -> BaseTy -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> BaseTy -> f BaseTy)
-> (AlphaCtx -> NamePatFind -> BaseTy -> BaseTy)
-> (AlphaCtx -> NthPatFind -> BaseTy -> BaseTy)
-> (BaseTy -> DisjointSet AnyName)
-> (BaseTy -> All)
-> (BaseTy -> Bool)
-> (BaseTy -> NthPatFind)
-> (BaseTy -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> BaseTy -> (BaseTy -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName))
-> (AlphaCtx -> BaseTy -> BaseTy -> Ordering)
-> Alpha BaseTy
AlphaCtx -> NthPatFind -> BaseTy -> BaseTy
AlphaCtx -> NamePatFind -> BaseTy -> BaseTy
AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy
AlphaCtx -> BaseTy -> BaseTy -> Bool
AlphaCtx -> BaseTy -> BaseTy -> Ordering
BaseTy -> Bool
BaseTy -> All
BaseTy -> DisjointSet AnyName
BaseTy -> NthPatFind
BaseTy -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> BaseTy -> f BaseTy
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BaseTy -> (BaseTy -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> BaseTy -> BaseTy -> Ordering
$cacompare' :: AlphaCtx -> BaseTy -> BaseTy -> Ordering
freshen' :: AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
lfreshen' :: AlphaCtx -> BaseTy -> (BaseTy -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BaseTy -> (BaseTy -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy
$cswaps' :: AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy
namePatFind :: BaseTy -> NamePatFind
$cnamePatFind :: BaseTy -> NamePatFind
nthPatFind :: BaseTy -> NthPatFind
$cnthPatFind :: BaseTy -> NthPatFind
isEmbed :: BaseTy -> Bool
$cisEmbed :: BaseTy -> Bool
isTerm :: BaseTy -> All
$cisTerm :: BaseTy -> All
isPat :: BaseTy -> DisjointSet AnyName
$cisPat :: BaseTy -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> BaseTy -> BaseTy
$copen :: AlphaCtx -> NthPatFind -> BaseTy -> BaseTy
close :: AlphaCtx -> NamePatFind -> BaseTy -> BaseTy
$cclose :: AlphaCtx -> NamePatFind -> BaseTy -> BaseTy
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> BaseTy -> f BaseTy
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> BaseTy -> f BaseTy
aeq' :: AlphaCtx -> BaseTy -> BaseTy -> Bool
$caeq' :: AlphaCtx -> BaseTy -> BaseTy -> Bool
$cp1Alpha :: Show BaseTy
Alpha, Subst BaseTy, Subst Atom, Subst UAtom, Subst Type)

instance Pretty BaseTy where
  pretty :: BaseTy -> Sem r Doc
pretty = \case
    BaseTy
Void    -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Void"
    BaseTy
Unit    -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Unit"
    BaseTy
B       -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Bool"
    BaseTy
P       -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Prop"
    BaseTy
N       -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"ℕ"
    BaseTy
Z       -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"ℤ"
    BaseTy
Q       -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"ℚ"
    BaseTy
F       -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"𝔽"
    BaseTy
C       -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Char"
    BaseTy
CtrList -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"List"
    BaseTy
CtrBag  -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Bag"
    BaseTy
CtrSet  -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Set"

-- | Test whether a 'BaseTy' is a container (set, bag, or list).
isCtr :: BaseTy -> Bool
isCtr :: BaseTy -> Bool
isCtr = (BaseTy -> [BaseTy] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BaseTy
CtrSet, BaseTy
CtrBag, BaseTy
CtrList])

----------------------------------------
-- Type variables

-- | 'Var' represents /type variables/, that is, variables which stand
--   for some type. There are two kinds of type variables:
--
--   * /Unification variables/ stand for an unknown type, about which
--     we might learn additional information during the typechecking
--     process.  For example, given a function of type @List a -> List
--     a@, if we typecheck an application of the function to the list
--     @[1,2,3]@, we would learn that @List a@ has to be @List N@, and
--     hence that @a@ has to be @N@.
--
--   * /Skolem variables/ stand for a fixed generic type, and are used
--     to typecheck universally quantified type signatures (/i.e./
--     type signatures which contain type variables).  For example, if
--     a function has the declared type @List a -> N@, it amounts to a
--     claim that the function will work no matter what type is
--     substituted for @a@. We check this by making up a new skolem
--     variable for @a@.  Skolem variables are equal to themselves,
--     but nothing else.  In contrast to a unification variable,
--     "learning something" about a skolem variable is an error: it
--     means that the function will only work for certain types, in
--     contradiction to its claim to work for any type at all.
data Ilk = Skolem | Unification
  deriving (Ilk -> Ilk -> Bool
(Ilk -> Ilk -> Bool) -> (Ilk -> Ilk -> Bool) -> Eq Ilk
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ilk -> Ilk -> Bool
$c/= :: Ilk -> Ilk -> Bool
== :: Ilk -> Ilk -> Bool
$c== :: Ilk -> Ilk -> Bool
Eq, Eq Ilk
Eq Ilk
-> (Ilk -> Ilk -> Ordering)
-> (Ilk -> Ilk -> Bool)
-> (Ilk -> Ilk -> Bool)
-> (Ilk -> Ilk -> Bool)
-> (Ilk -> Ilk -> Bool)
-> (Ilk -> Ilk -> Ilk)
-> (Ilk -> Ilk -> Ilk)
-> Ord Ilk
Ilk -> Ilk -> Bool
Ilk -> Ilk -> Ordering
Ilk -> Ilk -> Ilk
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ilk -> Ilk -> Ilk
$cmin :: Ilk -> Ilk -> Ilk
max :: Ilk -> Ilk -> Ilk
$cmax :: Ilk -> Ilk -> Ilk
>= :: Ilk -> Ilk -> Bool
$c>= :: Ilk -> Ilk -> Bool
> :: Ilk -> Ilk -> Bool
$c> :: Ilk -> Ilk -> Bool
<= :: Ilk -> Ilk -> Bool
$c<= :: Ilk -> Ilk -> Bool
< :: Ilk -> Ilk -> Bool
$c< :: Ilk -> Ilk -> Bool
compare :: Ilk -> Ilk -> Ordering
$ccompare :: Ilk -> Ilk -> Ordering
$cp1Ord :: Eq Ilk
Ord, ReadPrec [Ilk]
ReadPrec Ilk
Int -> ReadS Ilk
ReadS [Ilk]
(Int -> ReadS Ilk)
-> ReadS [Ilk] -> ReadPrec Ilk -> ReadPrec [Ilk] -> Read Ilk
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Ilk]
$creadListPrec :: ReadPrec [Ilk]
readPrec :: ReadPrec Ilk
$creadPrec :: ReadPrec Ilk
readList :: ReadS [Ilk]
$creadList :: ReadS [Ilk]
readsPrec :: Int -> ReadS Ilk
$creadsPrec :: Int -> ReadS Ilk
Read, Int -> Ilk -> ShowS
[Ilk] -> ShowS
Ilk -> String
(Int -> Ilk -> ShowS)
-> (Ilk -> String) -> ([Ilk] -> ShowS) -> Show Ilk
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ilk] -> ShowS
$cshowList :: [Ilk] -> ShowS
show :: Ilk -> String
$cshow :: Ilk -> String
showsPrec :: Int -> Ilk -> ShowS
$cshowsPrec :: Int -> Ilk -> ShowS
Show, (forall x. Ilk -> Rep Ilk x)
-> (forall x. Rep Ilk x -> Ilk) -> Generic Ilk
forall x. Rep Ilk x -> Ilk
forall x. Ilk -> Rep Ilk x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Ilk x -> Ilk
$cfrom :: forall x. Ilk -> Rep Ilk x
Generic, Typeable Ilk
DataType
Constr
Typeable Ilk
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Ilk -> c Ilk)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Ilk)
-> (Ilk -> Constr)
-> (Ilk -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Ilk))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ilk))
-> ((forall b. Data b => b -> b) -> Ilk -> Ilk)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r)
-> (forall u. (forall d. Data d => d -> u) -> Ilk -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Ilk -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Ilk -> m Ilk)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ilk -> m Ilk)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ilk -> m Ilk)
-> Data Ilk
Ilk -> DataType
Ilk -> Constr
(forall b. Data b => b -> b) -> Ilk -> Ilk
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ilk -> c Ilk
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ilk
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Ilk -> u
forall u. (forall d. Data d => d -> u) -> Ilk -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ilk
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ilk -> c Ilk
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ilk)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ilk)
$cUnification :: Constr
$cSkolem :: Constr
$tIlk :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Ilk -> m Ilk
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
gmapMp :: (forall d. Data d => d -> m d) -> Ilk -> m Ilk
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
gmapM :: (forall d. Data d => d -> m d) -> Ilk -> m Ilk
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ilk -> m Ilk
gmapQi :: Int -> (forall d. Data d => d -> u) -> Ilk -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ilk -> u
gmapQ :: (forall d. Data d => d -> u) -> Ilk -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Ilk -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r
gmapT :: (forall b. Data b => b -> b) -> Ilk -> Ilk
$cgmapT :: (forall b. Data b => b -> b) -> Ilk -> Ilk
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ilk)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ilk)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Ilk)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ilk)
dataTypeOf :: Ilk -> DataType
$cdataTypeOf :: Ilk -> DataType
toConstr :: Ilk -> Constr
$ctoConstr :: Ilk -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ilk
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ilk
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ilk -> c Ilk
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ilk -> c Ilk
$cp1Data :: Typeable Ilk
Data, Show Ilk
Show Ilk
-> (AlphaCtx -> Ilk -> Ilk -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Ilk -> f Ilk)
-> (AlphaCtx -> NamePatFind -> Ilk -> Ilk)
-> (AlphaCtx -> NthPatFind -> Ilk -> Ilk)
-> (Ilk -> DisjointSet AnyName)
-> (Ilk -> All)
-> (Ilk -> Bool)
-> (Ilk -> NthPatFind)
-> (Ilk -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Ilk -> Ilk)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> Ilk -> (Ilk -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Ilk -> m (Ilk, Perm AnyName))
-> (AlphaCtx -> Ilk -> Ilk -> Ordering)
-> Alpha Ilk
AlphaCtx -> NthPatFind -> Ilk -> Ilk
AlphaCtx -> NamePatFind -> Ilk -> Ilk
AlphaCtx -> Perm AnyName -> Ilk -> Ilk
AlphaCtx -> Ilk -> Ilk -> Bool
AlphaCtx -> Ilk -> Ilk -> Ordering
Ilk -> Bool
Ilk -> All
Ilk -> DisjointSet AnyName
Ilk -> NthPatFind
Ilk -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ilk -> f Ilk
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ilk -> m (Ilk, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Ilk -> (Ilk -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Ilk -> Ilk -> Ordering
$cacompare' :: AlphaCtx -> Ilk -> Ilk -> Ordering
freshen' :: AlphaCtx -> Ilk -> m (Ilk, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ilk -> m (Ilk, Perm AnyName)
lfreshen' :: AlphaCtx -> Ilk -> (Ilk -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Ilk -> (Ilk -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Ilk -> Ilk
$cswaps' :: AlphaCtx -> Perm AnyName -> Ilk -> Ilk
namePatFind :: Ilk -> NamePatFind
$cnamePatFind :: Ilk -> NamePatFind
nthPatFind :: Ilk -> NthPatFind
$cnthPatFind :: Ilk -> NthPatFind
isEmbed :: Ilk -> Bool
$cisEmbed :: Ilk -> Bool
isTerm :: Ilk -> All
$cisTerm :: Ilk -> All
isPat :: Ilk -> DisjointSet AnyName
$cisPat :: Ilk -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Ilk -> Ilk
$copen :: AlphaCtx -> NthPatFind -> Ilk -> Ilk
close :: AlphaCtx -> NamePatFind -> Ilk -> Ilk
$cclose :: AlphaCtx -> NamePatFind -> Ilk -> Ilk
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Ilk -> f Ilk
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ilk -> f Ilk
aeq' :: AlphaCtx -> Ilk -> Ilk -> Bool
$caeq' :: AlphaCtx -> Ilk -> Ilk -> Bool
$cp1Alpha :: Show Ilk
Alpha, Subst Atom, Subst Type)

instance Pretty Ilk where
  pretty :: Ilk -> Sem r Doc
pretty = \case
    Ilk
Skolem      -> Sem r Doc
"S"
    Ilk
Unification -> Sem r Doc
"U"

-- | 'Var' represents /type variables/, that is, variables which stand
--   for some type.
data Var where
  V :: Ilk -> Name Type -> Var
  deriving (Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
(Int -> Var -> ShowS)
-> (Var -> String) -> ([Var] -> ShowS) -> Show Var
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show, Var -> Var -> Bool
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Eq Var
-> (Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
$cp1Ord :: Eq Var
Ord, (forall x. Var -> Rep Var x)
-> (forall x. Rep Var x -> Var) -> Generic Var
forall x. Rep Var x -> Var
forall x. Var -> Rep Var x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Var x -> Var
$cfrom :: forall x. Var -> Rep Var x
Generic, Typeable Var
DataType
Constr
Typeable Var
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Var -> c Var)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Var)
-> (Var -> Constr)
-> (Var -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Var))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var))
-> ((forall b. Data b => b -> b) -> Var -> Var)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r)
-> (forall u. (forall d. Data d => d -> u) -> Var -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Var -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Var -> m Var)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Var -> m Var)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Var -> m Var)
-> Data Var
Var -> DataType
Var -> Constr
(forall b. Data b => b -> b) -> Var -> Var
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var -> c Var
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Var
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Var -> u
forall u. (forall d. Data d => d -> u) -> Var -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Var -> m Var
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var -> m Var
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Var
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var -> c Var
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Var)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var)
$cV :: Constr
$tVar :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Var -> m Var
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var -> m Var
gmapMp :: (forall d. Data d => d -> m d) -> Var -> m Var
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var -> m Var
gmapM :: (forall d. Data d => d -> m d) -> Var -> m Var
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Var -> m Var
gmapQi :: Int -> (forall d. Data d => d -> u) -> Var -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Var -> u
gmapQ :: (forall d. Data d => d -> u) -> Var -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Var -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r
gmapT :: (forall b. Data b => b -> b) -> Var -> Var
$cgmapT :: (forall b. Data b => b -> b) -> Var -> Var
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Var)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Var)
dataTypeOf :: Var -> DataType
$cdataTypeOf :: Var -> DataType
toConstr :: Var -> Constr
$ctoConstr :: Var -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Var
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Var
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var -> c Var
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var -> c Var
$cp1Data :: Typeable Var
Data, Show Var
Show Var
-> (AlphaCtx -> Var -> Var -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Var -> f Var)
-> (AlphaCtx -> NamePatFind -> Var -> Var)
-> (AlphaCtx -> NthPatFind -> Var -> Var)
-> (Var -> DisjointSet AnyName)
-> (Var -> All)
-> (Var -> Bool)
-> (Var -> NthPatFind)
-> (Var -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Var -> Var)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> Var -> (Var -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Var -> m (Var, Perm AnyName))
-> (AlphaCtx -> Var -> Var -> Ordering)
-> Alpha Var
AlphaCtx -> NthPatFind -> Var -> Var
AlphaCtx -> NamePatFind -> Var -> Var
AlphaCtx -> Perm AnyName -> Var -> Var
AlphaCtx -> Var -> Var -> Bool
AlphaCtx -> Var -> Var -> Ordering
Var -> Bool
Var -> All
Var -> DisjointSet AnyName
Var -> NthPatFind
Var -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Var -> f Var
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Var -> m (Var, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Var -> (Var -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Var -> Var -> Ordering
$cacompare' :: AlphaCtx -> Var -> Var -> Ordering
freshen' :: AlphaCtx -> Var -> m (Var, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Var -> m (Var, Perm AnyName)
lfreshen' :: AlphaCtx -> Var -> (Var -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Var -> (Var -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Var -> Var
$cswaps' :: AlphaCtx -> Perm AnyName -> Var -> Var
namePatFind :: Var -> NamePatFind
$cnamePatFind :: Var -> NamePatFind
nthPatFind :: Var -> NthPatFind
$cnthPatFind :: Var -> NthPatFind
isEmbed :: Var -> Bool
$cisEmbed :: Var -> Bool
isTerm :: Var -> All
$cisTerm :: Var -> All
isPat :: Var -> DisjointSet AnyName
$cisPat :: Var -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Var -> Var
$copen :: AlphaCtx -> NthPatFind -> Var -> Var
close :: AlphaCtx -> NamePatFind -> Var -> Var
$cclose :: AlphaCtx -> NamePatFind -> Var -> Var
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Var -> f Var
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Var -> f Var
aeq' :: AlphaCtx -> Var -> Var -> Bool
$caeq' :: AlphaCtx -> Var -> Var -> Bool
$cp1Alpha :: Show Var
Alpha, Subst Atom, Subst Type)

pattern U :: Name Type -> Var
pattern $bU :: Name Type -> Var
$mU :: forall r. Var -> (Name Type -> r) -> (Void# -> r) -> r
U v = V Unification v

pattern S :: Name Type -> Var
pattern $bS :: Name Type -> Var
$mS :: forall r. Var -> (Name Type -> r) -> (Void# -> r) -> r
S v = V Skolem v

{-# COMPLETE U, S #-}

----------------------------------------
-- Atomic types

-- | An /atomic type/ is either a base type or a type variable.  The
--   alternative is a /compound type/ which is built out of type
--   constructors.  The reason we split out the concept of atomic
--   types into its own data type 'Atom' is because constraints
--   involving compound types can always be simplified/translated into
--   constraints involving only atomic types.  After that
--   simplification step, we want to be able to work with collections
--   of constraints that are guaranteed to contain only atomic types.
data Atom where
  AVar  :: Var -> Atom
  ABase :: BaseTy -> Atom
  deriving (Int -> Atom -> ShowS
[Atom] -> ShowS
Atom -> String
(Int -> Atom -> ShowS)
-> (Atom -> String) -> ([Atom] -> ShowS) -> Show Atom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Atom] -> ShowS
$cshowList :: [Atom] -> ShowS
show :: Atom -> String
$cshow :: Atom -> String
showsPrec :: Int -> Atom -> ShowS
$cshowsPrec :: Int -> Atom -> ShowS
Show, Atom -> Atom -> Bool
(Atom -> Atom -> Bool) -> (Atom -> Atom -> Bool) -> Eq Atom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Atom -> Atom -> Bool
$c/= :: Atom -> Atom -> Bool
== :: Atom -> Atom -> Bool
$c== :: Atom -> Atom -> Bool
Eq, Eq Atom
Eq Atom
-> (Atom -> Atom -> Ordering)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Atom)
-> (Atom -> Atom -> Atom)
-> Ord Atom
Atom -> Atom -> Bool
Atom -> Atom -> Ordering
Atom -> Atom -> Atom
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Atom -> Atom -> Atom
$cmin :: Atom -> Atom -> Atom
max :: Atom -> Atom -> Atom
$cmax :: Atom -> Atom -> Atom
>= :: Atom -> Atom -> Bool
$c>= :: Atom -> Atom -> Bool
> :: Atom -> Atom -> Bool
$c> :: Atom -> Atom -> Bool
<= :: Atom -> Atom -> Bool
$c<= :: Atom -> Atom -> Bool
< :: Atom -> Atom -> Bool
$c< :: Atom -> Atom -> Bool
compare :: Atom -> Atom -> Ordering
$ccompare :: Atom -> Atom -> Ordering
$cp1Ord :: Eq Atom
Ord, (forall x. Atom -> Rep Atom x)
-> (forall x. Rep Atom x -> Atom) -> Generic Atom
forall x. Rep Atom x -> Atom
forall x. Atom -> Rep Atom x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Atom x -> Atom
$cfrom :: forall x. Atom -> Rep Atom x
Generic, Typeable Atom
DataType
Constr
Typeable Atom
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Atom -> c Atom)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Atom)
-> (Atom -> Constr)
-> (Atom -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Atom))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Atom))
-> ((forall b. Data b => b -> b) -> Atom -> Atom)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r)
-> (forall u. (forall d. Data d => d -> u) -> Atom -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Atom -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Atom -> m Atom)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Atom -> m Atom)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Atom -> m Atom)
-> Data Atom
Atom -> DataType
Atom -> Constr
(forall b. Data b => b -> b) -> Atom -> Atom
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Atom -> c Atom
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Atom
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Atom -> u
forall u. (forall d. Data d => d -> u) -> Atom -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Atom
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Atom -> c Atom
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Atom)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Atom)
$cABase :: Constr
$cAVar :: Constr
$tAtom :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Atom -> m Atom
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
gmapMp :: (forall d. Data d => d -> m d) -> Atom -> m Atom
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
gmapM :: (forall d. Data d => d -> m d) -> Atom -> m Atom
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Atom -> m Atom
gmapQi :: Int -> (forall d. Data d => d -> u) -> Atom -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Atom -> u
gmapQ :: (forall d. Data d => d -> u) -> Atom -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Atom -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r
gmapT :: (forall b. Data b => b -> b) -> Atom -> Atom
$cgmapT :: (forall b. Data b => b -> b) -> Atom -> Atom
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Atom)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Atom)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Atom)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Atom)
dataTypeOf :: Atom -> DataType
$cdataTypeOf :: Atom -> DataType
toConstr :: Atom -> Constr
$ctoConstr :: Atom -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Atom
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Atom
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Atom -> c Atom
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Atom -> c Atom
$cp1Data :: Typeable Atom
Data, Show Atom
Show Atom
-> (AlphaCtx -> Atom -> Atom -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Atom -> f Atom)
-> (AlphaCtx -> NamePatFind -> Atom -> Atom)
-> (AlphaCtx -> NthPatFind -> Atom -> Atom)
-> (Atom -> DisjointSet AnyName)
-> (Atom -> All)
-> (Atom -> Bool)
-> (Atom -> NthPatFind)
-> (Atom -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Atom -> Atom)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> Atom -> (Atom -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Atom -> m (Atom, Perm AnyName))
-> (AlphaCtx -> Atom -> Atom -> Ordering)
-> Alpha Atom
AlphaCtx -> NthPatFind -> Atom -> Atom
AlphaCtx -> NamePatFind -> Atom -> Atom
AlphaCtx -> Perm AnyName -> Atom -> Atom
AlphaCtx -> Atom -> Atom -> Bool
AlphaCtx -> Atom -> Atom -> Ordering
Atom -> Bool
Atom -> All
Atom -> DisjointSet AnyName
Atom -> NthPatFind
Atom -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Atom -> f Atom
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Atom -> m (Atom, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Atom -> (Atom -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Atom -> Atom -> Ordering
$cacompare' :: AlphaCtx -> Atom -> Atom -> Ordering
freshen' :: AlphaCtx -> Atom -> m (Atom, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Atom -> m (Atom, Perm AnyName)
lfreshen' :: AlphaCtx -> Atom -> (Atom -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Atom -> (Atom -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Atom -> Atom
$cswaps' :: AlphaCtx -> Perm AnyName -> Atom -> Atom
namePatFind :: Atom -> NamePatFind
$cnamePatFind :: Atom -> NamePatFind
nthPatFind :: Atom -> NthPatFind
$cnthPatFind :: Atom -> NthPatFind
isEmbed :: Atom -> Bool
$cisEmbed :: Atom -> Bool
isTerm :: Atom -> All
$cisTerm :: Atom -> All
isPat :: Atom -> DisjointSet AnyName
$cisPat :: Atom -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Atom -> Atom
$copen :: AlphaCtx -> NthPatFind -> Atom -> Atom
close :: AlphaCtx -> NamePatFind -> Atom -> Atom
$cclose :: AlphaCtx -> NamePatFind -> Atom -> Atom
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Atom -> f Atom
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Atom -> f Atom
aeq' :: AlphaCtx -> Atom -> Atom -> Bool
$caeq' :: AlphaCtx -> Atom -> Atom -> Bool
$cp1Alpha :: Show Atom
Alpha, Subst Type)

instance Subst Atom Atom where
  isvar :: Atom -> Maybe (SubstName Atom Atom)
isvar (AVar (U Name Type
x)) = SubstName Atom Atom -> Maybe (SubstName Atom Atom)
forall a. a -> Maybe a
Just (Name Atom -> SubstName Atom Atom
forall a b. (a ~ b) => Name a -> SubstName a b
SubstName (Name Type -> Name Atom
coerce Name Type
x))
  isvar Atom
_            = Maybe (SubstName Atom Atom)
forall a. Maybe a
Nothing

instance Pretty Atom where
  pretty :: Atom -> Sem r Doc
pretty = \case
    AVar (U Name Type
v) -> Name Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Type
v
    AVar (S Name Type
v) -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"$" Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Name Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Type
v
    ABase BaseTy
b    -> BaseTy -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty BaseTy
b

-- | Is this atomic type a variable?
isVar :: Atom -> Bool
isVar :: Atom -> Bool
isVar (AVar Var
_) = Bool
True
isVar Atom
_        = Bool
False

-- | Is this atomic type a base type?
isBase :: Atom -> Bool
isBase :: Atom -> Bool
isBase = Bool -> Bool
not (Bool -> Bool) -> (Atom -> Bool) -> Atom -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom -> Bool
isVar

-- | Is this atomic type a skolem variable?
isSkolem :: Atom -> Bool
isSkolem :: Atom -> Bool
isSkolem (AVar (S Name Type
_)) = Bool
True
isSkolem Atom
_            = Bool
False

-- | /Unifiable/ atomic types are the same as atomic types but without
--   skolem variables.  Hence, a unifiable atomic type is either a base
--   type or a unification variable.
--
--   Again, the reason this has its own type is that at some stage of
--   the typechecking/constraint solving process, these should be the
--   only things around; we can get rid of skolem variables because
--   either they impose no constraints, or result in an error if they
--   are related to something other than themselves.  After checking
--   these things, we can just focus on base types and unification
--   variables.
data UAtom where
  UB :: BaseTy    -> UAtom
  UV :: Name Type -> UAtom
  deriving (Int -> UAtom -> ShowS
[UAtom] -> ShowS
UAtom -> String
(Int -> UAtom -> ShowS)
-> (UAtom -> String) -> ([UAtom] -> ShowS) -> Show UAtom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UAtom] -> ShowS
$cshowList :: [UAtom] -> ShowS
show :: UAtom -> String
$cshow :: UAtom -> String
showsPrec :: Int -> UAtom -> ShowS
$cshowsPrec :: Int -> UAtom -> ShowS
Show, UAtom -> UAtom -> Bool
(UAtom -> UAtom -> Bool) -> (UAtom -> UAtom -> Bool) -> Eq UAtom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UAtom -> UAtom -> Bool
$c/= :: UAtom -> UAtom -> Bool
== :: UAtom -> UAtom -> Bool
$c== :: UAtom -> UAtom -> Bool
Eq, Eq UAtom
Eq UAtom
-> (UAtom -> UAtom -> Ordering)
-> (UAtom -> UAtom -> Bool)
-> (UAtom -> UAtom -> Bool)
-> (UAtom -> UAtom -> Bool)
-> (UAtom -> UAtom -> Bool)
-> (UAtom -> UAtom -> UAtom)
-> (UAtom -> UAtom -> UAtom)
-> Ord UAtom
UAtom -> UAtom -> Bool
UAtom -> UAtom -> Ordering
UAtom -> UAtom -> UAtom
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: UAtom -> UAtom -> UAtom
$cmin :: UAtom -> UAtom -> UAtom
max :: UAtom -> UAtom -> UAtom
$cmax :: UAtom -> UAtom -> UAtom
>= :: UAtom -> UAtom -> Bool
$c>= :: UAtom -> UAtom -> Bool
> :: UAtom -> UAtom -> Bool
$c> :: UAtom -> UAtom -> Bool
<= :: UAtom -> UAtom -> Bool
$c<= :: UAtom -> UAtom -> Bool
< :: UAtom -> UAtom -> Bool
$c< :: UAtom -> UAtom -> Bool
compare :: UAtom -> UAtom -> Ordering
$ccompare :: UAtom -> UAtom -> Ordering
$cp1Ord :: Eq UAtom
Ord, (forall x. UAtom -> Rep UAtom x)
-> (forall x. Rep UAtom x -> UAtom) -> Generic UAtom
forall x. Rep UAtom x -> UAtom
forall x. UAtom -> Rep UAtom x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep UAtom x -> UAtom
$cfrom :: forall x. UAtom -> Rep UAtom x
Generic, Show UAtom
Show UAtom
-> (AlphaCtx -> UAtom -> UAtom -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> UAtom -> f UAtom)
-> (AlphaCtx -> NamePatFind -> UAtom -> UAtom)
-> (AlphaCtx -> NthPatFind -> UAtom -> UAtom)
-> (UAtom -> DisjointSet AnyName)
-> (UAtom -> All)
-> (UAtom -> Bool)
-> (UAtom -> NthPatFind)
-> (UAtom -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> UAtom -> UAtom)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> UAtom -> (UAtom -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> UAtom -> m (UAtom, Perm AnyName))
-> (AlphaCtx -> UAtom -> UAtom -> Ordering)
-> Alpha UAtom
AlphaCtx -> NthPatFind -> UAtom -> UAtom
AlphaCtx -> NamePatFind -> UAtom -> UAtom
AlphaCtx -> Perm AnyName -> UAtom -> UAtom
AlphaCtx -> UAtom -> UAtom -> Bool
AlphaCtx -> UAtom -> UAtom -> Ordering
UAtom -> Bool
UAtom -> All
UAtom -> DisjointSet AnyName
UAtom -> NthPatFind
UAtom -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> UAtom -> f UAtom
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UAtom -> m (UAtom, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> UAtom -> (UAtom -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> UAtom -> UAtom -> Ordering
$cacompare' :: AlphaCtx -> UAtom -> UAtom -> Ordering
freshen' :: AlphaCtx -> UAtom -> m (UAtom, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UAtom -> m (UAtom, Perm AnyName)
lfreshen' :: AlphaCtx -> UAtom -> (UAtom -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> UAtom -> (UAtom -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> UAtom -> UAtom
$cswaps' :: AlphaCtx -> Perm AnyName -> UAtom -> UAtom
namePatFind :: UAtom -> NamePatFind
$cnamePatFind :: UAtom -> NamePatFind
nthPatFind :: UAtom -> NthPatFind
$cnthPatFind :: UAtom -> NthPatFind
isEmbed :: UAtom -> Bool
$cisEmbed :: UAtom -> Bool
isTerm :: UAtom -> All
$cisTerm :: UAtom -> All
isPat :: UAtom -> DisjointSet AnyName
$cisPat :: UAtom -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> UAtom -> UAtom
$copen :: AlphaCtx -> NthPatFind -> UAtom -> UAtom
close :: AlphaCtx -> NamePatFind -> UAtom -> UAtom
$cclose :: AlphaCtx -> NamePatFind -> UAtom -> UAtom
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> UAtom -> f UAtom
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> UAtom -> f UAtom
aeq' :: AlphaCtx -> UAtom -> UAtom -> Bool
$caeq' :: AlphaCtx -> UAtom -> UAtom -> Bool
$cp1Alpha :: Show UAtom
Alpha, Subst BaseTy)

instance Subst UAtom UAtom where
  isvar :: UAtom -> Maybe (SubstName UAtom UAtom)
isvar (UV Name Type
x) = SubstName UAtom UAtom -> Maybe (SubstName UAtom UAtom)
forall a. a -> Maybe a
Just (Name UAtom -> SubstName UAtom UAtom
forall a b. (a ~ b) => Name a -> SubstName a b
SubstName (Name Type -> Name UAtom
coerce Name Type
x))
  isvar UAtom
_      = Maybe (SubstName UAtom UAtom)
forall a. Maybe a
Nothing

instance Pretty UAtom where
  pretty :: UAtom -> Sem r Doc
pretty (UB BaseTy
b) = BaseTy -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty BaseTy
b
  pretty (UV Name Type
n) = Name Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Type
n

-- | Is this unifiable atomic type a (unification) variable?
uisVar :: UAtom -> Bool
uisVar :: UAtom -> Bool
uisVar (UV Name Type
_) = Bool
True
uisVar UAtom
_      = Bool
False

-- | Convert a unifiable atomic type into a regular atomic type.
uatomToAtom :: UAtom -> Atom
uatomToAtom :: UAtom -> Atom
uatomToAtom (UB BaseTy
b) = BaseTy -> Atom
ABase BaseTy
b
uatomToAtom (UV Name Type
x) = Var -> Atom
AVar (Name Type -> Var
U Name Type
x)

-- | Convert a unifiable atomic type to an explicit @Either@ type.
uatomToEither :: UAtom -> Either BaseTy (Name Type)
uatomToEither :: UAtom -> Either BaseTy (Name Type)
uatomToEither (UB BaseTy
b) = BaseTy -> Either BaseTy (Name Type)
forall a b. a -> Either a b
Left BaseTy
b
uatomToEither (UV Name Type
v) = Name Type -> Either BaseTy (Name Type)
forall a b. b -> Either a b
Right Name Type
v

----------------------------------------
-- Type constructors

-- | /Compound types/, such as functions, product types, and sum
--   types, are an application of a /type constructor/ to one or more
--   argument types.
data Con where
  -- | Function type constructor, @T1 -> T2@.
  CArr  :: Con
  -- | Product type constructor, @T1 * T2@.
  CProd :: Con
  -- | Sum type constructor, @T1 + T2@.
  CSum  :: Con

  -- | Container type (list, bag, or set) constructor.  Note this
  --   looks like it could contain any 'Atom', but it will only ever
  --   contain either a type variable or a 'CtrList', 'CtrBag', or
  --   'CtrSet'.
  --
  --   See also 'CList', 'CBag', and 'CSet'.
  CContainer :: Atom -> Con


  -- | Key value maps, Map k v
  CMap :: Con

  -- | Graph constructor, Graph a
  CGraph :: Con

  -- | The name of a user defined algebraic datatype.
  CUser :: String -> Con

  deriving (Int -> Con -> ShowS
[Con] -> ShowS
Con -> String
(Int -> Con -> ShowS)
-> (Con -> String) -> ([Con] -> ShowS) -> Show Con
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Con] -> ShowS
$cshowList :: [Con] -> ShowS
show :: Con -> String
$cshow :: Con -> String
showsPrec :: Int -> Con -> ShowS
$cshowsPrec :: Int -> Con -> ShowS
Show, Con -> Con -> Bool
(Con -> Con -> Bool) -> (Con -> Con -> Bool) -> Eq Con
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Con -> Con -> Bool
$c/= :: Con -> Con -> Bool
== :: Con -> Con -> Bool
$c== :: Con -> Con -> Bool
Eq, Eq Con
Eq Con
-> (Con -> Con -> Ordering)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Con)
-> (Con -> Con -> Con)
-> Ord Con
Con -> Con -> Bool
Con -> Con -> Ordering
Con -> Con -> Con
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Con -> Con -> Con
$cmin :: Con -> Con -> Con
max :: Con -> Con -> Con
$cmax :: Con -> Con -> Con
>= :: Con -> Con -> Bool
$c>= :: Con -> Con -> Bool
> :: Con -> Con -> Bool
$c> :: Con -> Con -> Bool
<= :: Con -> Con -> Bool
$c<= :: Con -> Con -> Bool
< :: Con -> Con -> Bool
$c< :: Con -> Con -> Bool
compare :: Con -> Con -> Ordering
$ccompare :: Con -> Con -> Ordering
$cp1Ord :: Eq Con
Ord, (forall x. Con -> Rep Con x)
-> (forall x. Rep Con x -> Con) -> Generic Con
forall x. Rep Con x -> Con
forall x. Con -> Rep Con x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Con x -> Con
$cfrom :: forall x. Con -> Rep Con x
Generic, Typeable Con
DataType
Constr
Typeable Con
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Con -> c Con)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Con)
-> (Con -> Constr)
-> (Con -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Con))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Con))
-> ((forall b. Data b => b -> b) -> Con -> Con)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r)
-> (forall u. (forall d. Data d => d -> u) -> Con -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Con -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Con -> m Con)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Con -> m Con)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Con -> m Con)
-> Data Con
Con -> DataType
Con -> Constr
(forall b. Data b => b -> b) -> Con -> Con
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Con -> c Con
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Con
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Con -> u
forall u. (forall d. Data d => d -> u) -> Con -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Con -> m Con
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Con -> m Con
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Con
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Con -> c Con
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Con)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Con)
$cCUser :: Constr
$cCGraph :: Constr
$cCMap :: Constr
$cCContainer :: Constr
$cCSum :: Constr
$cCProd :: Constr
$cCArr :: Constr
$tCon :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Con -> m Con
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Con -> m Con
gmapMp :: (forall d. Data d => d -> m d) -> Con -> m Con
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Con -> m Con
gmapM :: (forall d. Data d => d -> m d) -> Con -> m Con
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Con -> m Con
gmapQi :: Int -> (forall d. Data d => d -> u) -> Con -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Con -> u
gmapQ :: (forall d. Data d => d -> u) -> Con -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Con -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
gmapT :: (forall b. Data b => b -> b) -> Con -> Con
$cgmapT :: (forall b. Data b => b -> b) -> Con -> Con
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Con)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Con)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Con)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Con)
dataTypeOf :: Con -> DataType
$cdataTypeOf :: Con -> DataType
toConstr :: Con -> Constr
$ctoConstr :: Con -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Con
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Con
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Con -> c Con
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Con -> c Con
$cp1Data :: Typeable Con
Data, Show Con
Show Con
-> (AlphaCtx -> Con -> Con -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Con -> f Con)
-> (AlphaCtx -> NamePatFind -> Con -> Con)
-> (AlphaCtx -> NthPatFind -> Con -> Con)
-> (Con -> DisjointSet AnyName)
-> (Con -> All)
-> (Con -> Bool)
-> (Con -> NthPatFind)
-> (Con -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Con -> Con)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Con -> m (Con, Perm AnyName))
-> (AlphaCtx -> Con -> Con -> Ordering)
-> Alpha Con
AlphaCtx -> NthPatFind -> Con -> Con
AlphaCtx -> NamePatFind -> Con -> Con
AlphaCtx -> Perm AnyName -> Con -> Con
AlphaCtx -> Con -> Con -> Bool
AlphaCtx -> Con -> Con -> Ordering
Con -> Bool
Con -> All
Con -> DisjointSet AnyName
Con -> NthPatFind
Con -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Con -> f Con
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Con -> m (Con, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Con -> Con -> Ordering
$cacompare' :: AlphaCtx -> Con -> Con -> Ordering
freshen' :: AlphaCtx -> Con -> m (Con, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Con -> m (Con, Perm AnyName)
lfreshen' :: AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Con -> Con
$cswaps' :: AlphaCtx -> Perm AnyName -> Con -> Con
namePatFind :: Con -> NamePatFind
$cnamePatFind :: Con -> NamePatFind
nthPatFind :: Con -> NthPatFind
$cnthPatFind :: Con -> NthPatFind
isEmbed :: Con -> Bool
$cisEmbed :: Con -> Bool
isTerm :: Con -> All
$cisTerm :: Con -> All
isPat :: Con -> DisjointSet AnyName
$cisPat :: Con -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Con -> Con
$copen :: AlphaCtx -> NthPatFind -> Con -> Con
close :: AlphaCtx -> NamePatFind -> Con -> Con
$cclose :: AlphaCtx -> NamePatFind -> Con -> Con
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Con -> f Con
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Con -> f Con
aeq' :: AlphaCtx -> Con -> Con -> Bool
$caeq' :: AlphaCtx -> Con -> Con -> Bool
$cp1Alpha :: Show Con
Alpha)

instance Pretty Con where
  pretty :: Con -> Sem r Doc
pretty = \case
    Con
CMap         -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Map"
    Con
CGraph       -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Graph"
    CUser String
s      -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
s
    Con
CList        -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"List"
    Con
CBag         -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Bag"
    Con
CSet         -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Set"
    CContainer Atom
v -> Atom -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Atom
v
    Con
c            -> String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"Impossible: got Con " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Con -> String
forall a. Show a => a -> String
show Con
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in pretty @Con"

-- | 'CList' is provided for convenience; it represents a list type
--   constructor (/i.e./ @List a@).
pattern CList :: Con
pattern $bCList :: Con
$mCList :: forall r. Con -> (Void# -> r) -> (Void# -> r) -> r
CList = CContainer (ABase CtrList)

-- | 'CBag' is provided for convenience; it represents a bag type
--   constructor (/i.e./ @Bag a@).
pattern CBag :: Con
pattern $bCBag :: Con
$mCBag :: forall r. Con -> (Void# -> r) -> (Void# -> r) -> r
CBag = CContainer (ABase CtrBag)

-- | 'CSet' is provided for convenience; it represents a set type
--   constructor (/i.e./ @Set a@).
pattern CSet :: Con
pattern $bCSet :: Con
$mCSet :: forall r. Con -> (Void# -> r) -> (Void# -> r) -> r
CSet = CContainer (ABase CtrSet)

{-# COMPLETE CArr, CProd, CSum, CList, CBag, CSet, CGraph, CMap, CUser #-}

----------------------------------------
-- Types

-- | The main data type for representing types in the disco language.
--   A type can be either an atomic type, or the application of a type
--   constructor to one or more type arguments.
--
--   @Type@s are broken down into two cases (@TyAtom@ and @TyCon@) for
--   ease of implementation: there are many situations where all atoms
--   can be handled generically in one way and all type constructors
--   can be handled generically in another.  However, using this
--   representation to write down specific types is tedious; for
--   example, to represent the type @N -> a@ one must write something
--   like @TyCon CArr [TyAtom (ABase N), TyAtom (AVar (U a))]@.  For
--   this reason, pattern synonyms such as ':->:', 'TyN', and
--   'TyVar' are provided so that one can use them to construct and
--   pattern-match on types when convenient.  For example, using these
--   synonyms the foregoing example can be written @TyN :->: TyVar a@.
data Type where

  -- | Atomic types (variables and base types), /e.g./ @N@, @Bool@, /etc./
  TyAtom :: Atom -> Type

  -- | Application of a type constructor to type arguments, /e.g./ @N
  --   -> Bool@ is the application of the arrow type constructor to the
  --   arguments @N@ and @Bool@.
  TyCon  :: Con -> [Type] -> Type

  deriving (Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show, Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq, Eq Type
Eq Type
-> (Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmax :: Type -> Type -> Type
>= :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c< :: Type -> Type -> Bool
compare :: Type -> Type -> Ordering
$ccompare :: Type -> Type -> Ordering
$cp1Ord :: Eq Type
Ord, (forall x. Type -> Rep Type x)
-> (forall x. Rep Type x -> Type) -> Generic Type
forall x. Rep Type x -> Type
forall x. Type -> Rep Type x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Type x -> Type
$cfrom :: forall x. Type -> Rep Type x
Generic, Typeable Type
DataType
Constr
Typeable Type
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Type -> c Type)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Type)
-> (Type -> Constr)
-> (Type -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Type))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type))
-> ((forall b. Data b => b -> b) -> Type -> Type)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
-> (forall u. (forall d. Data d => d -> u) -> Type -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Type -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Type -> m Type)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Type -> m Type)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Type -> m Type)
-> Data Type
Type -> DataType
Type -> Constr
(forall b. Data b => b -> b) -> Type -> Type
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
forall u. (forall d. Data d => d -> u) -> Type -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
$cTyCon :: Constr
$cTyAtom :: Constr
$tType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapMp :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapM :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
gmapQ :: (forall d. Data d => d -> u) -> Type -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapT :: (forall b. Data b => b -> b) -> Type -> Type
$cgmapT :: (forall b. Data b => b -> b) -> Type -> Type
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Type)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
dataTypeOf :: Type -> DataType
$cdataTypeOf :: Type -> DataType
toConstr :: Type -> Constr
$ctoConstr :: Type -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
$cp1Data :: Typeable Type
Data, Show Type
Show Type
-> (AlphaCtx -> Type -> Type -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Type -> f Type)
-> (AlphaCtx -> NamePatFind -> Type -> Type)
-> (AlphaCtx -> NthPatFind -> Type -> Type)
-> (Type -> DisjointSet AnyName)
-> (Type -> All)
-> (Type -> Bool)
-> (Type -> NthPatFind)
-> (Type -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Type -> Type)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> Type -> (Type -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Type -> m (Type, Perm AnyName))
-> (AlphaCtx -> Type -> Type -> Ordering)
-> Alpha Type
AlphaCtx -> NthPatFind -> Type -> Type
AlphaCtx -> NamePatFind -> Type -> Type
AlphaCtx -> Perm AnyName -> Type -> Type
AlphaCtx -> Type -> Type -> Bool
AlphaCtx -> Type -> Type -> Ordering
Type -> Bool
Type -> All
Type -> DisjointSet AnyName
Type -> NthPatFind
Type -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Type -> f Type
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Type -> m (Type, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Type -> (Type -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Type -> Type -> Ordering
$cacompare' :: AlphaCtx -> Type -> Type -> Ordering
freshen' :: AlphaCtx -> Type -> m (Type, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Type -> m (Type, Perm AnyName)
lfreshen' :: AlphaCtx -> Type -> (Type -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Type -> (Type -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Type -> Type
$cswaps' :: AlphaCtx -> Perm AnyName -> Type -> Type
namePatFind :: Type -> NamePatFind
$cnamePatFind :: Type -> NamePatFind
nthPatFind :: Type -> NthPatFind
$cnthPatFind :: Type -> NthPatFind
isEmbed :: Type -> Bool
$cisEmbed :: Type -> Bool
isTerm :: Type -> All
$cisTerm :: Type -> All
isPat :: Type -> DisjointSet AnyName
$cisPat :: Type -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Type -> Type
$copen :: AlphaCtx -> NthPatFind -> Type -> Type
close :: AlphaCtx -> NamePatFind -> Type -> Type
$cclose :: AlphaCtx -> NamePatFind -> Type -> Type
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Type -> f Type
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Type -> f Type
aeq' :: AlphaCtx -> Type -> Type -> Bool
$caeq' :: AlphaCtx -> Type -> Type -> Bool
$cp1Alpha :: Show Type
Alpha)

instance Pretty Type where
  pretty :: Type -> Sem r Doc
pretty (TyAtom Atom
a)     = Atom -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Atom
a
  pretty (Type
ty1 :->: Type
ty2) = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
tarrPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
    Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"→" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2)
  pretty (Type
ty1 :*: Type
ty2)  = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
tmulPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
    Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"×" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2)
  pretty (Type
ty1 :+: Type
ty2)  = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
taddPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
    Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"+" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty2)
  pretty (TyCon Con
c [])   = Con -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Con
c
  pretty (TyCon Con
c [Type]
tys)  = do
    [Sem r Doc]
ds <- PA -> Sem r [Sem r Doc] -> Sem r [Sem r Doc]
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r [Sem r Doc] -> Sem r [Sem r Doc])
-> Sem r [Sem r Doc] -> Sem r [Sem r Doc]
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Type -> Sem r Doc) -> [Type] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Type]
tys)
    Con -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Con
c Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)

instance Subst Type Qualifier
instance Subst Type Rational where
  subst :: Name Type -> Type -> Rational -> Rational
subst Name Type
_ Type
_ = Rational -> Rational
forall a. a -> a
id
  substs :: [(Name Type, Type)] -> Rational -> Rational
substs [(Name Type, Type)]
_  = Rational -> Rational
forall a. a -> a
id
instance Subst Type Void where
  subst :: Name Type -> Type -> Void -> Void
subst Name Type
_ Type
_ = Void -> Void
forall a. a -> a
id
  substs :: [(Name Type, Type)] -> Void -> Void
substs [(Name Type, Type)]
_  = Void -> Void
forall a. a -> a
id
instance Subst Type Con where
  isCoerceVar :: Con -> Maybe (SubstCoerce Con Type)
isCoerceVar (CContainer (AVar (U Name Type
x)))
    = SubstCoerce Con Type -> Maybe (SubstCoerce Con Type)
forall a. a -> Maybe a
Just (Name Type -> (Type -> Maybe Con) -> SubstCoerce Con Type
forall b a. Name b -> (b -> Maybe a) -> SubstCoerce a b
SubstCoerce Name Type
x Type -> Maybe Con
substCtrTy)
    where
      substCtrTy :: Type -> Maybe Con
substCtrTy (TyAtom Atom
a) = Con -> Maybe Con
forall a. a -> Maybe a
Just (Atom -> Con
CContainer Atom
a)
      substCtrTy Type
_          = Maybe Con
forall a. Maybe a
Nothing
  isCoerceVar Con
_                         = Maybe (SubstCoerce Con Type)
forall a. Maybe a
Nothing
instance Subst Type Type where
  isvar :: Type -> Maybe (SubstName Type Type)
isvar (TyAtom (AVar (U Name Type
x))) = SubstName Type Type -> Maybe (SubstName Type Type)
forall a. a -> Maybe a
Just (Name Type -> SubstName Type Type
forall a b. (a ~ b) => Name a -> SubstName a b
SubstName Name Type
x)
  isvar Type
_                     = Maybe (SubstName Type Type)
forall a. Maybe a
Nothing

pattern TyVar  :: Name Type -> Type
pattern $bTyVar :: Name Type -> Type
$mTyVar :: forall r. Type -> (Name Type -> r) -> (Void# -> r) -> r
TyVar v = TyAtom (AVar (U v))

pattern TySkolem :: Name Type -> Type
pattern $bTySkolem :: Name Type -> Type
$mTySkolem :: forall r. Type -> (Name Type -> r) -> (Void# -> r) -> r
TySkolem v = TyAtom (AVar (S v))

pattern TyVoid :: Type
pattern $bTyVoid :: Type
$mTyVoid :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyVoid = TyAtom (ABase Void)

pattern TyUnit :: Type
pattern $bTyUnit :: Type
$mTyUnit :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyUnit = TyAtom (ABase Unit)

pattern TyBool :: Type
pattern $bTyBool :: Type
$mTyBool :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyBool = TyAtom (ABase B)

pattern TyProp :: Type
pattern $bTyProp :: Type
$mTyProp :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyProp = TyAtom (ABase P)

pattern TyN :: Type
pattern $bTyN :: Type
$mTyN :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyN = TyAtom (ABase N)

pattern TyZ :: Type
pattern $bTyZ :: Type
$mTyZ :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyZ = TyAtom (ABase Z)

pattern TyF :: Type
pattern $bTyF :: Type
$mTyF :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyF = TyAtom (ABase F)

pattern TyQ :: Type
pattern $bTyQ :: Type
$mTyQ :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyQ = TyAtom (ABase Q)

pattern TyC :: Type
pattern $bTyC :: Type
$mTyC :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyC = TyAtom (ABase C)


-- pattern TyFin :: Integer -> Type
-- pattern TyFin n = TyAtom (ABase (Fin n))

infixr 5 :->:

pattern (:->:) :: Type -> Type -> Type
pattern $b:->: :: Type -> Type -> Type
$m:->: :: forall r. Type -> (Type -> Type -> r) -> (Void# -> r) -> r
(:->:) ty1 ty2 = TyCon CArr [ty1, ty2]

infixr 7 :*:

pattern (:*:) :: Type -> Type -> Type
pattern $b:*: :: Type -> Type -> Type
$m:*: :: forall r. Type -> (Type -> Type -> r) -> (Void# -> r) -> r
(:*:) ty1 ty2 = TyCon CProd [ty1, ty2]

infixr 6 :+:

pattern (:+:) :: Type -> Type -> Type
pattern $b:+: :: Type -> Type -> Type
$m:+: :: forall r. Type -> (Type -> Type -> r) -> (Void# -> r) -> r
(:+:) ty1 ty2 = TyCon CSum [ty1, ty2]

pattern TyList :: Type -> Type
pattern $bTyList :: Type -> Type
$mTyList :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
TyList elTy = TyCon CList [elTy]

pattern TyBag  :: Type -> Type
pattern $bTyBag :: Type -> Type
$mTyBag :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
TyBag elTy = TyCon CBag [elTy]

pattern TySet :: Type -> Type
pattern $bTySet :: Type -> Type
$mTySet :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
TySet elTy = TyCon CSet [elTy]

pattern TyContainer :: Atom -> Type -> Type
pattern $bTyContainer :: Atom -> Type -> Type
$mTyContainer :: forall r. Type -> (Atom -> Type -> r) -> (Void# -> r) -> r
TyContainer c elTy = TyCon (CContainer c) [elTy]

pattern TyGraph :: Type -> Type
pattern $bTyGraph :: Type -> Type
$mTyGraph :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
TyGraph elTy = TyCon CGraph [elTy]

pattern TyMap :: Type -> Type -> Type
pattern $bTyMap :: Type -> Type -> Type
$mTyMap :: forall r. Type -> (Type -> Type -> r) -> (Void# -> r) -> r
TyMap tyKey tyValue = TyCon CMap [tyKey, tyValue]

-- | An application of a user-defined type.
pattern TyUser :: String -> [Type] -> Type
pattern $bTyUser :: String -> [Type] -> Type
$mTyUser :: forall r. Type -> (String -> [Type] -> r) -> (Void# -> r) -> r
TyUser nm args = TyCon (CUser nm) args

pattern TyString :: Type
pattern $bTyString :: Type
$mTyString :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
TyString = TyList TyC

{-# COMPLETE
      TyVar, TySkolem, TyVoid, TyUnit, TyBool, TyProp, TyN, TyZ, TyF, TyQ, TyC,
      (:->:), (:*:), (:+:), TyList, TyBag, TySet, TyGraph, TyMap, TyUser #-}

-- | Is this a type variable?
isTyVar :: Type -> Bool
isTyVar :: Type -> Bool
isTyVar (TyAtom (AVar Var
_)) = Bool
True
isTyVar Type
_                 = Bool
False

-- orphans
instance (Ord a, Subst t a) => Subst t (Set a) where
  subst :: Name t -> t -> Set a -> Set a
subst Name t
x t
t = (a -> a) -> Set a -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (Name t -> t -> a -> a
forall b a. Subst b a => Name b -> b -> a -> a
subst Name t
x t
t)
  substs :: [(Name t, t)] -> Set a -> Set a
substs [(Name t, t)]
s  = (a -> a) -> Set a -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map ([(Name t, t)] -> a -> a
forall b a. Subst b a => [(Name b, b)] -> a -> a
substs [(Name t, t)]
s)
instance (Ord k, Subst t a) => Subst t (Map k a) where
  subst :: Name t -> t -> Map k a -> Map k a
subst Name t
x t
t = (a -> a) -> Map k a -> Map k a
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Name t -> t -> a -> a
forall b a. Subst b a => Name b -> b -> a -> a
subst Name t
x t
t)
  substs :: [(Name t, t)] -> Map k a -> Map k a
substs [(Name t, t)]
s  = (a -> a) -> Map k a -> Map k a
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ([(Name t, t)] -> a -> a
forall b a. Subst b a => [(Name b, b)] -> a -> a
substs [(Name t, t)]
s)

-- | The definition of a user-defined type contains:
--
--   * The actual names of the type variable arguments used in the
--     definition (we keep these around only to help with
--     pretty-printing)
--   * A function representing the body of the definition.  It takes a
--     list of type arguments and returns the body of the definition
--     with the type arguments substituted.
--
--   We represent type definitions this way (using a function, as
--   opposed to a chunk of abstract syntax) because it makes some
--   things simpler, and we don't particularly need to do anything
--   more complicated.
data TyDefBody = TyDefBody [String] ([Type] -> Type)

instance Show TyDefBody where
  show :: TyDefBody -> String
show TyDefBody
_ = String
"<tydef>"

-- | A 'TyDefCtx' is a mapping from type names to their corresponding
--   definitions.
type TyDefCtx = M.Map String TyDefBody

-- | Pretty-print a type definition.
instance Pretty (String, TyDefBody) where

  pretty :: (String, TyDefBody) -> Sem r Doc
pretty (String
tyName, TyDefBody [String]
ps [Type] -> Type
body)
    = Sem r Doc
"type" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
tyName Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> [String] -> Sem r Doc
prettyArgs [String]
ps) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"=" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty ([Type] -> Type
body ((String -> Type) -> [String] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Type
TyVar (Name Type -> Type) -> (String -> Name Type) -> String -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name Type
forall a. String -> Name a
string2Name) [String]
ps))
    where
      prettyArgs :: [String] -> Sem r Doc
prettyArgs [] = Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
empty
      prettyArgs [String]
_  = do
          [Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((String -> Sem r Doc) -> [String] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text [String]
ps)
          Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)

---------------------------------
--  Universally quantified types

-- | 'PolyType' represents a polymorphic type of the form @forall a1
--   a2 ... an. ty@ (note, however, that n may be 0, that is, we can
--   have a "trivial" polytype which quantifies zero variables).
newtype PolyType = Forall (Bind [Name Type] Type)
  deriving (Int -> PolyType -> ShowS
[PolyType] -> ShowS
PolyType -> String
(Int -> PolyType -> ShowS)
-> (PolyType -> String) -> ([PolyType] -> ShowS) -> Show PolyType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PolyType] -> ShowS
$cshowList :: [PolyType] -> ShowS
show :: PolyType -> String
$cshow :: PolyType -> String
showsPrec :: Int -> PolyType -> ShowS
$cshowsPrec :: Int -> PolyType -> ShowS
Show, (forall x. PolyType -> Rep PolyType x)
-> (forall x. Rep PolyType x -> PolyType) -> Generic PolyType
forall x. Rep PolyType x -> PolyType
forall x. PolyType -> Rep PolyType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PolyType x -> PolyType
$cfrom :: forall x. PolyType -> Rep PolyType x
Generic, Typeable PolyType
DataType
Constr
Typeable PolyType
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> PolyType -> c PolyType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PolyType)
-> (PolyType -> Constr)
-> (PolyType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PolyType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyType))
-> ((forall b. Data b => b -> b) -> PolyType -> PolyType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PolyType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PolyType -> r)
-> (forall u. (forall d. Data d => d -> u) -> PolyType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PolyType -> m PolyType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PolyType -> m PolyType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PolyType -> m PolyType)
-> Data PolyType
PolyType -> DataType
PolyType -> Constr
(forall b. Data b => b -> b) -> PolyType -> PolyType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PolyType -> c PolyType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PolyType
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u
forall u. (forall d. Data d => d -> u) -> PolyType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PolyType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PolyType -> c PolyType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PolyType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyType)
$cForall :: Constr
$tPolyType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PolyType -> m PolyType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
gmapMp :: (forall d. Data d => d -> m d) -> PolyType -> m PolyType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
gmapM :: (forall d. Data d => d -> m d) -> PolyType -> m PolyType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
gmapQi :: Int -> (forall d. Data d => d -> u) -> PolyType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u
gmapQ :: (forall d. Data d => d -> u) -> PolyType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PolyType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
gmapT :: (forall b. Data b => b -> b) -> PolyType -> PolyType
$cgmapT :: (forall b. Data b => b -> b) -> PolyType -> PolyType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PolyType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PolyType)
dataTypeOf :: PolyType -> DataType
$cdataTypeOf :: PolyType -> DataType
toConstr :: PolyType -> Constr
$ctoConstr :: PolyType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PolyType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PolyType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PolyType -> c PolyType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PolyType -> c PolyType
$cp1Data :: Typeable PolyType
Data, Show PolyType
Show PolyType
-> (AlphaCtx -> PolyType -> PolyType -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> PolyType -> f PolyType)
-> (AlphaCtx -> NamePatFind -> PolyType -> PolyType)
-> (AlphaCtx -> NthPatFind -> PolyType -> PolyType)
-> (PolyType -> DisjointSet AnyName)
-> (PolyType -> All)
-> (PolyType -> Bool)
-> (PolyType -> NthPatFind)
-> (PolyType -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> PolyType -> PolyType)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> PolyType -> m (PolyType, Perm AnyName))
-> (AlphaCtx -> PolyType -> PolyType -> Ordering)
-> Alpha PolyType
AlphaCtx -> NthPatFind -> PolyType -> PolyType
AlphaCtx -> NamePatFind -> PolyType -> PolyType
AlphaCtx -> Perm AnyName -> PolyType -> PolyType
AlphaCtx -> PolyType -> PolyType -> Bool
AlphaCtx -> PolyType -> PolyType -> Ordering
PolyType -> Bool
PolyType -> All
PolyType -> DisjointSet AnyName
PolyType -> NthPatFind
PolyType -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> PolyType -> f PolyType
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> PolyType -> PolyType -> Ordering
$cacompare' :: AlphaCtx -> PolyType -> PolyType -> Ordering
freshen' :: AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
lfreshen' :: AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> PolyType -> PolyType
$cswaps' :: AlphaCtx -> Perm AnyName -> PolyType -> PolyType
namePatFind :: PolyType -> NamePatFind
$cnamePatFind :: PolyType -> NamePatFind
nthPatFind :: PolyType -> NthPatFind
$cnthPatFind :: PolyType -> NthPatFind
isEmbed :: PolyType -> Bool
$cisEmbed :: PolyType -> Bool
isTerm :: PolyType -> All
$cisTerm :: PolyType -> All
isPat :: PolyType -> DisjointSet AnyName
$cisPat :: PolyType -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> PolyType -> PolyType
$copen :: AlphaCtx -> NthPatFind -> PolyType -> PolyType
close :: AlphaCtx -> NamePatFind -> PolyType -> PolyType
$cclose :: AlphaCtx -> NamePatFind -> PolyType -> PolyType
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> PolyType -> f PolyType
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> PolyType -> f PolyType
aeq' :: AlphaCtx -> PolyType -> PolyType -> Bool
$caeq' :: AlphaCtx -> PolyType -> PolyType -> Bool
$cp1Alpha :: Show PolyType
Alpha, Subst Type)

-- | Pretty-print a polytype.  Note that we never explicitly print
--   @forall@; quantification is implicit, as in Haskell.
instance Pretty PolyType where
  pretty :: PolyType -> Sem r Doc
pretty (Forall Bind [Name Type] Type
bnd) = Bind [Name Type] Type
-> (([Name Type], Type) -> Sem r Doc) -> Sem r Doc
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Name Type] Type
bnd ((([Name Type], Type) -> Sem r Doc) -> Sem r Doc)
-> (([Name Type], Type) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
    \([Name Type]
_, Type
body) -> Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
body

-- | Convert a monotype into a trivial polytype that does not quantify
--   over any type variables.  If the type can contain free type
--   variables, use 'closeType' instead.
toPolyType :: Type -> PolyType
toPolyType :: Type -> PolyType
toPolyType Type
ty = Bind [Name Type] Type -> PolyType
Forall ([Name Type] -> Type -> Bind [Name Type] Type
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [] Type
ty)

-- | Convert a monotype into a polytype by quantifying over all its
--   free type variables.
closeType :: Type -> PolyType
closeType :: Type -> PolyType
closeType Type
ty = Bind [Name Type] Type -> PolyType
Forall ([Name Type] -> Type -> Bind [Name Type] Type
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ([Name Type] -> [Name Type]
forall a. Eq a => [a] -> [a]
nub ([Name Type] -> [Name Type]) -> [Name Type] -> [Name Type]
forall a b. (a -> b) -> a -> b
$ Getting (Endo [Name Type]) Type (Name Type) -> Type -> [Name Type]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [Name Type]) Type (Name Type)
forall a (f :: * -> *) b.
(Alpha a, Typeable b, Contravariant f, Applicative f) =>
(Name b -> f (Name b)) -> a -> f a
fv Type
ty) Type
ty)

--------------------------------------------------
-- Counting inhabitants
--------------------------------------------------

-- | Compute the number of inhabitants of a type.  @Nothing@ means the
--   type is countably infinite.
countType :: Type -> Maybe Integer
countType :: Type -> Maybe Integer
countType Type
TyVoid        = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
countType Type
TyUnit        = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
countType Type
TyBool        = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
2
-- countType (TyFin n)     = Just n
countType Type
TyC           = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
17 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
16 :: Integer))
countType (Type
ty1 :+: Type
ty2) = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty1 Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Integer
countType Type
ty2
countType (Type
ty1 :*: Type
ty2)
  | Type -> Bool
isEmptyTy Type
ty1       = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
  | Type -> Bool
isEmptyTy Type
ty2       = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
  | Bool
otherwise           = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty1 Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Integer
countType Type
ty2
countType (Type
ty1 :->: Type
ty2) =
  case (Type -> Maybe Integer
countType Type
ty1, Type -> Maybe Integer
countType Type
ty2) of
    (Just Integer
0, Maybe Integer
_) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
    (Maybe Integer
_, Just Integer
0) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
    (Maybe Integer
_, Just Integer
1) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
    (Maybe Integer
c1, Maybe Integer
c2)    -> Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
(^) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
c2 Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Integer
c1
countType (TyList Type
ty)
  | Type -> Bool
isEmptyTy Type
ty        = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
  | Bool
otherwise           = Maybe Integer
forall a. Maybe a
Nothing
countType (TyBag Type
ty)
  | Type -> Bool
isEmptyTy Type
ty        = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
  | Bool
otherwise           = Maybe Integer
forall a. Maybe a
Nothing
countType (TySet Type
ty)    = (Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty

  -- t = number of elements in vertex type.
  -- n = number of vertices in the graph.
  -- For each n in [0..t], we can choose which n values to use for the
  --   vertices; then for each ordered pair of vertices (u,v)
  --   (including the possibility that u = v), we choose whether or
  --   not there is a directed edge u -> v.
  --
  -- https://oeis.org/A135748

countType (TyGraph Type
ty)  =
  (\Integer
t -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer) -> [Integer] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (\Integer
n -> (Integer
t Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`choose` Integer
n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
n)) [Integer
0 .. Integer
t]) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
  Type -> Maybe Integer
countType Type
ty

countType (TyMap Type
tyKey Type
tyValue)
  | Type -> Bool
isEmptyTy Type
tyKey     = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1     -- If we can't have any keys or values,
  | Type -> Bool
isEmptyTy Type
tyValue   = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1     -- only option is empty map
  | Bool
otherwise           = (\Integer
k Integer
v -> (Integer
vInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
k) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
tyKey Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Integer
countType Type
tyValue
      -- (v+1)^k since for each key, we can choose among v values to associate with it,
      -- or we can choose to not have the key in the map.

-- All other types are infinite. (TyN, TyZ, TyQ, TyF)
countType Type
_             = Maybe Integer
forall a. Maybe a
Nothing

--------------------------------------------------
-- Type predicates
--------------------------------------------------

-- | Check whether a type is a numeric type (@N@, @Z@, @F@, @Q@, or @Zn@).
isNumTy :: Type -> Bool
-- isNumTy (TyFin _) = True
isNumTy :: Type -> Bool
isNumTy Type
ty        = Type
ty Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type
TyN, Type
TyZ, Type
TyF, Type
TyQ]

-- | Decide whether a type is empty, /i.e./ uninhabited.
isEmptyTy :: Type -> Bool
isEmptyTy :: Type -> Bool
isEmptyTy Type
ty
  | Just Integer
0 <- Type -> Maybe Integer
countType Type
ty = Bool
True
  | Bool
otherwise              = Bool
False

-- | Decide whether a type is finite.
isFiniteTy :: Type -> Bool
isFiniteTy :: Type -> Bool
isFiniteTy Type
ty
  | Just Integer
_ <- Type -> Maybe Integer
countType Type
ty = Bool
True
  | Bool
otherwise              = Bool
False

-- XXX coinductively check whether user-defined types are searchable
--   e.g.  L = Unit + N * L  ought to be searchable.
--   See https://github.com/disco-lang/disco/issues/318.

-- | Decide whether a type is searchable, i.e. effectively enumerable.
isSearchable :: Type -> Bool
isSearchable :: Type -> Bool
isSearchable Type
TyProp         = Bool
False
isSearchable Type
ty
  | Type -> Bool
isNumTy Type
ty              = Bool
True
  | Type -> Bool
isFiniteTy Type
ty           = Bool
True
isSearchable (TyList Type
ty)    = Type -> Bool
isSearchable Type
ty
isSearchable (TySet Type
ty)     = Type -> Bool
isSearchable Type
ty
isSearchable (Type
ty1 :+: Type
ty2)  = Type -> Bool
isSearchable Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
isSearchable Type
ty2
isSearchable (Type
ty1 :*: Type
ty2)  = Type -> Bool
isSearchable Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
isSearchable Type
ty2
isSearchable (Type
ty1 :->: Type
ty2) = Type -> Bool
isFiniteTy Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
isSearchable Type
ty2
isSearchable Type
_              = Bool
False

--------------------------------------------------
-- Strictness
--------------------------------------------------

-- | @Strictness@ represents the strictness (either strict or lazy) of
--   a function application or let-expression.
data Strictness = Strict | Lazy
  deriving (Strictness -> Strictness -> Bool
(Strictness -> Strictness -> Bool)
-> (Strictness -> Strictness -> Bool) -> Eq Strictness
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Strictness -> Strictness -> Bool
$c/= :: Strictness -> Strictness -> Bool
== :: Strictness -> Strictness -> Bool
$c== :: Strictness -> Strictness -> Bool
Eq, Int -> Strictness -> ShowS
[Strictness] -> ShowS
Strictness -> String
(Int -> Strictness -> ShowS)
-> (Strictness -> String)
-> ([Strictness] -> ShowS)
-> Show Strictness
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Strictness] -> ShowS
$cshowList :: [Strictness] -> ShowS
show :: Strictness -> String
$cshow :: Strictness -> String
showsPrec :: Int -> Strictness -> ShowS
$cshowsPrec :: Int -> Strictness -> ShowS
Show, (forall x. Strictness -> Rep Strictness x)
-> (forall x. Rep Strictness x -> Strictness) -> Generic Strictness
forall x. Rep Strictness x -> Strictness
forall x. Strictness -> Rep Strictness x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Strictness x -> Strictness
$cfrom :: forall x. Strictness -> Rep Strictness x
Generic, Show Strictness
Show Strictness
-> (AlphaCtx -> Strictness -> Strictness -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Strictness -> f Strictness)
-> (AlphaCtx -> NamePatFind -> Strictness -> Strictness)
-> (AlphaCtx -> NthPatFind -> Strictness -> Strictness)
-> (Strictness -> DisjointSet AnyName)
-> (Strictness -> All)
-> (Strictness -> Bool)
-> (Strictness -> NthPatFind)
-> (Strictness -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Strictness -> Strictness)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx
    -> Strictness -> (Strictness -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Strictness -> m (Strictness, Perm AnyName))
-> (AlphaCtx -> Strictness -> Strictness -> Ordering)
-> Alpha Strictness
AlphaCtx -> NthPatFind -> Strictness -> Strictness
AlphaCtx -> NamePatFind -> Strictness -> Strictness
AlphaCtx -> Perm AnyName -> Strictness -> Strictness
AlphaCtx -> Strictness -> Strictness -> Bool
AlphaCtx -> Strictness -> Strictness -> Ordering
Strictness -> Bool
Strictness -> All
Strictness -> DisjointSet AnyName
Strictness -> NthPatFind
Strictness -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Strictness -> f Strictness
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Strictness -> m (Strictness, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Strictness -> (Strictness -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Strictness -> Strictness -> Ordering
$cacompare' :: AlphaCtx -> Strictness -> Strictness -> Ordering
freshen' :: AlphaCtx -> Strictness -> m (Strictness, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Strictness -> m (Strictness, Perm AnyName)
lfreshen' :: AlphaCtx
-> Strictness -> (Strictness -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Strictness -> (Strictness -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Strictness -> Strictness
$cswaps' :: AlphaCtx -> Perm AnyName -> Strictness -> Strictness
namePatFind :: Strictness -> NamePatFind
$cnamePatFind :: Strictness -> NamePatFind
nthPatFind :: Strictness -> NthPatFind
$cnthPatFind :: Strictness -> NthPatFind
isEmbed :: Strictness -> Bool
$cisEmbed :: Strictness -> Bool
isTerm :: Strictness -> All
$cisTerm :: Strictness -> All
isPat :: Strictness -> DisjointSet AnyName
$cisPat :: Strictness -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Strictness -> Strictness
$copen :: AlphaCtx -> NthPatFind -> Strictness -> Strictness
close :: AlphaCtx -> NamePatFind -> Strictness -> Strictness
$cclose :: AlphaCtx -> NamePatFind -> Strictness -> Strictness
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Strictness -> f Strictness
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Strictness -> f Strictness
aeq' :: AlphaCtx -> Strictness -> Strictness -> Bool
$caeq' :: AlphaCtx -> Strictness -> Strictness -> Bool
$cp1Alpha :: Show Strictness
Alpha)

-- | Numeric types are strict; others are lazy.
strictness :: Type -> Strictness
strictness :: Type -> Strictness
strictness Type
ty
  | Type -> Bool
isNumTy Type
ty = Strictness
Strict
  | Bool
otherwise  = Strictness
Lazy

--------------------------------------------------
-- Utilities
--------------------------------------------------

-- | Decompose a nested product @T1 * (T2 * ( ... ))@ into a list of
--   types.
unpair :: Type -> [Type]
unpair :: Type -> [Type]
unpair (Type
ty1 :*: Type
ty2) = Type
ty1 Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Type -> [Type]
unpair Type
ty2
unpair Type
ty            = [Type
ty]

-- | Define @S@ as a substitution on types (the most common kind)
--   for convenience.
type S = Substitution Type

-- | Convert a substitution on atoms into a substitution on types.
atomToTypeSubst :: Substitution Atom -> Substitution Type
atomToTypeSubst :: Substitution Atom -> Substitution Type
atomToTypeSubst = (Atom -> Type) -> Substitution Atom -> Substitution Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Atom -> Type
TyAtom

-- | Convert a substitution on unifiable atoms into a substitution on
--   types.
uatomToTypeSubst :: Substitution UAtom -> Substitution Type
uatomToTypeSubst :: Substitution UAtom -> Substitution Type
uatomToTypeSubst = Substitution Atom -> Substitution Type
atomToTypeSubst (Substitution Atom -> Substitution Type)
-> (Substitution UAtom -> Substitution Atom)
-> Substitution UAtom
-> Substitution Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UAtom -> Atom) -> Substitution UAtom -> Substitution Atom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UAtom -> Atom
uatomToAtom

-- | Return a set of all the free container variables in a type.
containerVars :: Type -> Set (Name Type)
containerVars :: Type -> Set (Name Type)
containerVars (TyCon (CContainer (AVar (U Name Type
x))) [Type]
tys)
  = Name Type
x Name Type -> Set (Name Type) -> Set (Name Type)
forall a. Ord a => a -> Set a -> Set a
`S.insert` (Type -> Set (Name Type)) -> [Type] -> Set (Name Type)
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Set (Name Type)
containerVars [Type]
tys
containerVars (TyCon Con
_ [Type]
tys) = (Type -> Set (Name Type)) -> [Type] -> Set (Name Type)
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Set (Name Type)
containerVars [Type]
tys
containerVars Type
_ = Set (Name Type)
forall a. Set a
S.empty

------------------------------------------------------------
-- HasType class
------------------------------------------------------------

-- | A type class for things whose type can be extracted or set.
class HasType t where

  -- | Get the type of a thing.
  getType :: t -> Type

  -- | Set the type of a thing, when that is possible; the default
  --   implementation is for 'setType' to do nothing.
  setType :: Type -> t -> t
  setType Type
_ = t -> t
forall a. a -> a
id