{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

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

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

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

-- |
-- 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.
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
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
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
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
Ord, 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
BaseTy -> DataType
BaseTy -> Constr
(forall b. Data b => b -> b) -> BaseTy -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
Alpha, Subst BaseTy, Subst Atom, Subst UAtom, Subst Type)

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

-- | Test whether a 'BaseTy' is a container (set, bag, or list).
isCtr :: BaseTy -> Bool
isCtr :: BaseTy -> Bool
isCtr = (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
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
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
Ord, ReadPrec [Ilk]
ReadPrec Ilk
Int -> ReadS Ilk
ReadS [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
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. 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
Ilk -> DataType
Ilk -> Constr
(forall b. Data b => b -> b) -> Ilk -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Ilk -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ilk -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Ilk -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Ilk -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ilk -> m (Ilk, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ilk -> m (Ilk, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
Alpha, Subst Atom, Subst Type)

instance Pretty Ilk where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Ilk -> Sem r (Doc ann)
pretty = \case
    Ilk
Skolem -> Sem r (Doc ann)
"S"
    Ilk
Unification -> Sem r (Doc ann)
"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
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
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
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
Ord, 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
Var -> DataType
Var -> Constr
(forall b. Data b => b -> b) -> Var -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Var -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Var -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Var -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Var -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Var -> m (Var, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Var -> m (Var, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
Alpha, Subst Atom, Subst Type)

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

pattern S :: Name Type -> Var
pattern $bS :: Name Type -> Var
$mS :: forall {r}. Var -> (Name Type -> r) -> ((# #) -> 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
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
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
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
Ord, 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
Atom -> DataType
Atom -> Constr
(forall b. Data b => b -> b) -> Atom -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Atom -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Atom -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Atom -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Atom -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Atom -> m (Atom, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Atom -> m (Atom, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
Alpha, Subst Type)

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

instance Pretty Atom where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Atom -> Sem r (Doc ann)
pretty = \case
    AVar (U Name Type
v) -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Type
v
    AVar (S Name Type
v) -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"$" forall a. Semigroup a => a -> a -> a
<> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Type
v
    ABase BaseTy
b -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
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 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
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
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
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
Ord, 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
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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UAtom -> m (UAtom, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UAtom -> m (UAtom, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
Alpha, Subst BaseTy)

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

instance Pretty UAtom where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
UAtom -> Sem r (Doc ann)
pretty (UB BaseTy
b) = forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty BaseTy
b
  pretty (UV Name Type
n) = forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
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) = forall a b. a -> Either a b
Left BaseTy
b
uatomToEither (UV Name Type
v) = 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
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
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
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
Ord, 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
Con -> DataType
Con -> Constr
(forall b. Data b => b -> b) -> Con -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Con -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Con -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Con -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Con -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Con -> m (Con, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Con -> m (Con, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
Alpha)

instance Pretty Con where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Con -> Sem r (Doc ann)
pretty = \case
    Con
CMap -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Map"
    Con
CGraph -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Graph"
    CUser String
s -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s
    Con
CList -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"List"
    Con
CBag -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Bag"
    Con
CSet -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Set"
    CContainer Atom
v -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Atom
v
    Con
c -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible: got Con " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Con
c 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 -> ((# #) -> r) -> ((# #) -> 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 -> ((# #) -> r) -> ((# #) -> 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 -> ((# #) -> r) -> ((# #) -> 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
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
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
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
Ord, 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
Type -> DataType
Type -> Constr
(forall b. Data b => b -> b) -> Type -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Type -> m (Type, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Type -> m (Type, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
Alpha)

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

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

pattern TyVar :: Name Type -> Type
pattern $bTyVar :: Name Type -> Type
$mTyVar :: forall {r}. Type -> (Name Type -> r) -> ((# #) -> 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) -> ((# #) -> r) -> r
TySkolem v = TyAtom (AVar (S v))

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

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

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

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

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

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

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

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

pattern TyC :: Type
pattern $bTyC :: Type
$mTyC :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> 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) -> ((# #) -> 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) -> ((# #) -> 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) -> ((# #) -> r) -> r
(:+:) ty1 ty2 = TyCon CSum [ty1, ty2]

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

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

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

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

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

pattern TyMap :: Type -> Type -> Type
pattern $bTyMap :: Type -> Type -> Type
$mTyMap :: forall {r}. Type -> (Type -> Type -> r) -> ((# #) -> 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) -> ((# #) -> r) -> r
TyUser nm args = TyCon (CUser nm) args

pattern TyString :: Type
pattern $bTyString :: Type
$mTyString :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> 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 = forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (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 = forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (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 = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (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 = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (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 :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
(String, TyDefBody) -> Sem r (Doc ann)
pretty (String
tyName, TyDefBody [String]
ps [Type] -> Type
body) =
    Sem r (Doc ann)
"type" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
tyName forall a. Semigroup a => a -> a -> a
<> [String] -> Sem r (Doc ann)
prettyArgs [String]
ps) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"=" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty ([Type] -> Type
body (forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Type
TyVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> Name a
string2Name) [String]
ps))
   where
    prettyArgs :: [String] -> Sem r (Doc ann)
prettyArgs [] = forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty
    prettyArgs [String]
_ = do
      [Sem r (Doc ann)]
ds <- forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text [String]
ps)
      forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
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
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. 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
PolyType -> DataType
PolyType -> Constr
(forall b. Data b => b -> b) -> PolyType -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> PolyType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PolyType -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
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 :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
PolyType -> Sem r (Doc ann)
pretty (Forall Bind [Name Type] Type
bnd) = 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 forall a b. (a -> b) -> a -> b
$
    \([Name Type]
_, Type
body) -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
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 (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 (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf 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 = forall a. a -> Maybe a
Just Integer
0
countType Type
TyUnit = forall a. a -> Maybe a
Just Integer
1
countType Type
TyBool = forall a. a -> Maybe a
Just Integer
2
-- countType (TyFin n)     = Just n
countType Type
TyC = forall a. a -> Maybe a
Just (Integer
17 forall a. Num a => a -> a -> a
* Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
16 :: Integer))
countType (Type
ty1 :+: Type
ty2) = forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty1 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 = forall a. a -> Maybe a
Just Integer
0
  | Type -> Bool
isEmptyTy Type
ty2 = forall a. a -> Maybe a
Just Integer
0
  | Bool
otherwise = forall a. Num a => a -> a -> a
(*) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty1 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
_) -> forall a. a -> Maybe a
Just Integer
1
    (Maybe Integer
_, Just Integer
0) -> forall a. a -> Maybe a
Just Integer
0
    (Maybe Integer
_, Just Integer
1) -> forall a. a -> Maybe a
Just Integer
1
    (Maybe Integer
c1, Maybe Integer
c2) -> forall a b. (Num a, Integral b) => a -> b -> a
(^) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
c2 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 = forall a. a -> Maybe a
Just Integer
1
  | Bool
otherwise = forall a. Maybe a
Nothing
countType (TyBag Type
ty)
  | Type -> Bool
isEmptyTy Type
ty = forall a. a -> Maybe a
Just Integer
1
  | Bool
otherwise = forall a. Maybe a
Nothing
countType (TySet Type
ty) = (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^) 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 -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Integer
n -> (Integer
t forall a. Integral a => a -> a -> a
`choose` Integer
n) forall a. Num a => a -> a -> a
* Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
n forall a. Num a => a -> a -> a
* Integer
n)) [Integer
0 .. Integer
t])
    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 = forall a. a -> Maybe a
Just Integer
1 -- If we can't have any keys or values,
  | Type -> Bool
isEmptyTy Type
tyValue = forall a. a -> Maybe a
Just Integer
1 -- only option is empty map
  | Bool
otherwise = (\Integer
k Integer
v -> (Integer
v forall a. Num a => a -> a -> a
+ Integer
1) forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
k) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
tyKey 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
_ = 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 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
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
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. 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
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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Strictness -> m (Strictness, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Strictness -> m (Strictness, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
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 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 = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Ord a => a -> Set a -> Set a
`S.insert` 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) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Set (Name Type)
containerVars [Type]
tys
containerVars 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
_ = forall a. a -> a
id