{-# 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  :  [email protected]
--
-- 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 TyGen,
  -- , 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

  Gen :: BaseTy
  -- | Set container type.  It's a bit odd putting these here since
  --   they have kind * -> * and all the other base types have kind *;
  --   but there's nothing fundamentally wrong with it and in
  --   particular this allows us to reuse all the existing constraint
  --   solving machinery for container subtyping.
  CtrSet :: BaseTy
  -- | Bag container type.
  CtrBag :: BaseTy
  -- | List container type.
  CtrList :: BaseTy
  deriving (Int -> BaseTy -> ShowS
[BaseTy] -> ShowS
BaseTy -> String
(Int -> BaseTy -> ShowS)
-> (BaseTy -> String) -> ([BaseTy] -> ShowS) -> Show BaseTy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BaseTy -> ShowS
showsPrec :: Int -> BaseTy -> ShowS
$cshow :: BaseTy -> String
show :: BaseTy -> String
$cshowList :: [BaseTy] -> ShowS
showList :: [BaseTy] -> ShowS
Show, BaseTy -> BaseTy -> Bool
(BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool) -> Eq BaseTy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BaseTy -> BaseTy -> Bool
== :: BaseTy -> BaseTy -> Bool
$c/= :: BaseTy -> BaseTy -> Bool
/= :: BaseTy -> BaseTy -> Bool
Eq, Eq BaseTy
Eq BaseTy =>
(BaseTy -> BaseTy -> Ordering)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> Bool)
-> (BaseTy -> BaseTy -> BaseTy)
-> (BaseTy -> BaseTy -> BaseTy)
-> Ord BaseTy
BaseTy -> BaseTy -> Bool
BaseTy -> BaseTy -> Ordering
BaseTy -> BaseTy -> BaseTy
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BaseTy -> BaseTy -> Ordering
compare :: BaseTy -> BaseTy -> Ordering
$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
>= :: BaseTy -> BaseTy -> Bool
$cmax :: BaseTy -> BaseTy -> BaseTy
max :: BaseTy -> BaseTy -> BaseTy
$cmin :: BaseTy -> BaseTy -> BaseTy
min :: BaseTy -> BaseTy -> BaseTy
Ord, (forall x. BaseTy -> Rep BaseTy x)
-> (forall x. Rep BaseTy x -> BaseTy) -> Generic BaseTy
forall x. Rep BaseTy x -> BaseTy
forall x. BaseTy -> Rep BaseTy x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BaseTy -> Rep BaseTy x
from :: forall x. BaseTy -> Rep BaseTy x
$cto :: forall x. Rep BaseTy x -> BaseTy
to :: forall x. Rep BaseTy x -> BaseTy
Generic, Typeable BaseTy
Typeable BaseTy =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BaseTy -> c BaseTy)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BaseTy)
-> (BaseTy -> Constr)
-> (BaseTy -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BaseTy))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy))
-> ((forall b. Data b => b -> b) -> BaseTy -> BaseTy)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BaseTy -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BaseTy -> r)
-> (forall u. (forall d. Data d => d -> u) -> BaseTy -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy)
-> Data BaseTy
BaseTy -> Constr
BaseTy -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BaseTy -> c BaseTy
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BaseTy
$ctoConstr :: BaseTy -> Constr
toConstr :: BaseTy -> Constr
$cdataTypeOf :: BaseTy -> DataType
dataTypeOf :: BaseTy -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BaseTy)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy)
$cgmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
gmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> BaseTy -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BaseTy -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BaseTy -> m BaseTy
Data, Show BaseTy
Show BaseTy =>
(AlphaCtx -> BaseTy -> BaseTy -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> BaseTy -> f BaseTy)
-> (AlphaCtx -> NamePatFind -> BaseTy -> BaseTy)
-> (AlphaCtx -> NthPatFind -> BaseTy -> BaseTy)
-> (BaseTy -> DisjointSet AnyName)
-> (BaseTy -> All)
-> (BaseTy -> Bool)
-> (BaseTy -> NthPatFind)
-> (BaseTy -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> BaseTy -> (BaseTy -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName))
-> (AlphaCtx -> BaseTy -> BaseTy -> Ordering)
-> Alpha BaseTy
AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy
AlphaCtx -> NamePatFind -> BaseTy -> BaseTy
AlphaCtx -> NthPatFind -> BaseTy -> BaseTy
AlphaCtx -> BaseTy -> BaseTy -> Bool
AlphaCtx -> BaseTy -> BaseTy -> Ordering
BaseTy -> Bool
BaseTy -> All
BaseTy -> NamePatFind
BaseTy -> NthPatFind
BaseTy -> DisjointSet AnyName
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
$caeq' :: AlphaCtx -> BaseTy -> BaseTy -> Bool
aeq' :: AlphaCtx -> BaseTy -> BaseTy -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> BaseTy -> f BaseTy
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> BaseTy -> f BaseTy
$cclose :: AlphaCtx -> NamePatFind -> BaseTy -> BaseTy
close :: AlphaCtx -> NamePatFind -> BaseTy -> BaseTy
$copen :: AlphaCtx -> NthPatFind -> BaseTy -> BaseTy
open :: AlphaCtx -> NthPatFind -> BaseTy -> BaseTy
$cisPat :: BaseTy -> DisjointSet AnyName
isPat :: BaseTy -> DisjointSet AnyName
$cisTerm :: BaseTy -> All
isTerm :: BaseTy -> All
$cisEmbed :: BaseTy -> Bool
isEmbed :: BaseTy -> Bool
$cnthPatFind :: BaseTy -> NthPatFind
nthPatFind :: BaseTy -> NthPatFind
$cnamePatFind :: BaseTy -> NamePatFind
namePatFind :: BaseTy -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy
swaps' :: AlphaCtx -> Perm AnyName -> BaseTy -> BaseTy
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BaseTy -> (BaseTy -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BaseTy -> (BaseTy -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BaseTy -> m (BaseTy, Perm AnyName)
$cacompare' :: AlphaCtx -> BaseTy -> BaseTy -> Ordering
acompare' :: AlphaCtx -> BaseTy -> BaseTy -> Ordering
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 -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Void"
    BaseTy
Unit -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Unit"
    BaseTy
B -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Bool"
    BaseTy
P -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Prop"
    BaseTy
N -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"ℕ"
    BaseTy
Z -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"ℤ"
    BaseTy
Q -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"ℚ"
    BaseTy
F -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"𝔽"
    BaseTy
C -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Char"
    BaseTy
CtrList -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"List"
    BaseTy
CtrBag -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Bag"
    BaseTy
CtrSet -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Set"
    BaseTy
Gen -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"Gen"

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

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

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

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

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

{-# COMPLETE U, S #-}

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

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

instance Subst Atom Atom where
  isvar :: Atom -> Maybe (SubstName Atom Atom)
isvar (AVar (U Name Type
x)) = SubstName Atom Atom -> Maybe (SubstName Atom Atom)
forall a. a -> Maybe a
Just (Name Atom -> SubstName Atom Atom
forall a b. (a ~ b) => Name a -> SubstName a b
SubstName (Name Type -> Name Atom
forall a b. Coercible a b => a -> b
coerce Name Type
x))
  isvar Atom
_ = Maybe (SubstName Atom 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) -> Name Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Type -> Sem r (Doc ann)
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) -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"$" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> Name Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Type
v
    ABase BaseTy
b -> BaseTy -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
BaseTy -> Sem r (Doc ann)
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 (Bool -> Bool) -> (Atom -> Bool) -> Atom -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom -> Bool
isVar

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

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

instance Subst UAtom UAtom where
  isvar :: UAtom -> Maybe (SubstName UAtom UAtom)
isvar (UV Name Type
x) = SubstName UAtom UAtom -> Maybe (SubstName UAtom UAtom)
forall a. a -> Maybe a
Just (Name UAtom -> SubstName UAtom UAtom
forall a b. (a ~ b) => Name a -> SubstName a b
SubstName (Name Type -> Name UAtom
forall a b. Coercible a b => a -> b
coerce Name Type
x))
  isvar UAtom
_ = Maybe (SubstName UAtom 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) = BaseTy -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
BaseTy -> Sem r (Doc ann)
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) = Name Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Type -> Sem r (Doc ann)
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) = BaseTy -> Either BaseTy (Name Type)
forall a b. a -> Either a b
Left BaseTy
b
uatomToEither (UV Name Type
v) = Name Type -> Either BaseTy (Name Type)
forall a b. b -> Either a b
Right Name Type
v

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

-- | /Compound types/, such as functions, product types, and sum
--   types, are an application of a /type constructor/ to one or more
--   argument types.
data Con where
  -- | Function type constructor, @T1 -> T2@.
  CArr :: Con
  -- | Product type constructor, @T1 * T2@.
  CProd :: Con
  -- | Sum type constructor, @T1 + T2@.
  CSum :: Con
  -- | Container type (list, bag, or set) constructor.  Note this
  --   looks like it could contain any 'Atom', but it will only ever
  --   contain either a type variable or a 'CtrList', 'CtrBag', or
  --   'CtrSet'.
  --
  --   See also 'CList', 'CBag', and 'CSet'.
  CContainer :: Atom -> Con
  -- | Key value maps, Map k v
  CMap :: Con
  -- | Graph constructor, Graph a
  CGraph :: Con
  -- | The name of a user defined algebraic datatype.
  CUser :: String -> Con
  deriving (Int -> Con -> ShowS
[Con] -> ShowS
Con -> String
(Int -> Con -> ShowS)
-> (Con -> String) -> ([Con] -> ShowS) -> Show Con
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Con -> ShowS
showsPrec :: Int -> Con -> ShowS
$cshow :: Con -> String
show :: Con -> String
$cshowList :: [Con] -> ShowS
showList :: [Con] -> ShowS
Show, Con -> Con -> Bool
(Con -> Con -> Bool) -> (Con -> Con -> Bool) -> Eq Con
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Con -> Con -> Bool
== :: Con -> Con -> Bool
$c/= :: Con -> Con -> Bool
/= :: Con -> Con -> Bool
Eq, Eq Con
Eq Con =>
(Con -> Con -> Ordering)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Bool)
-> (Con -> Con -> Con)
-> (Con -> Con -> Con)
-> Ord Con
Con -> Con -> Bool
Con -> Con -> Ordering
Con -> Con -> Con
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Con -> Con -> Ordering
compare :: Con -> Con -> Ordering
$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
>= :: Con -> Con -> Bool
$cmax :: Con -> Con -> Con
max :: Con -> Con -> Con
$cmin :: Con -> Con -> Con
min :: Con -> Con -> Con
Ord, (forall x. Con -> Rep Con x)
-> (forall x. Rep Con x -> Con) -> Generic Con
forall x. Rep Con x -> Con
forall x. Con -> Rep Con x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Con -> Rep Con x
from :: forall x. Con -> Rep Con x
$cto :: forall x. Rep Con x -> Con
to :: forall x. Rep Con x -> Con
Generic, Typeable Con
Typeable Con =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Con -> c Con)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Con)
-> (Con -> Constr)
-> (Con -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Con))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Con))
-> ((forall b. Data b => b -> b) -> Con -> Con)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r)
-> (forall u. (forall d. Data d => d -> u) -> Con -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Con -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Con -> m Con)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Con -> m Con)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Con -> m Con)
-> Data Con
Con -> Constr
Con -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Con -> c Con
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Con -> c Con
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Con
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Con
$ctoConstr :: Con -> Constr
toConstr :: Con -> Constr
$cdataTypeOf :: Con -> DataType
dataTypeOf :: Con -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Con)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Con)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Con)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Con)
$cgmapT :: (forall b. Data b => b -> b) -> Con -> Con
gmapT :: (forall b. Data b => b -> b) -> Con -> Con
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Con -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Con -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Con -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Con -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Con -> m Con
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Con -> m Con
Data, Show Con
Show Con =>
(AlphaCtx -> Con -> Con -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Con -> f Con)
-> (AlphaCtx -> NamePatFind -> Con -> Con)
-> (AlphaCtx -> NthPatFind -> Con -> Con)
-> (Con -> DisjointSet AnyName)
-> (Con -> All)
-> (Con -> Bool)
-> (Con -> NthPatFind)
-> (Con -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Con -> Con)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Con -> m (Con, Perm AnyName))
-> (AlphaCtx -> Con -> Con -> Ordering)
-> Alpha Con
AlphaCtx -> Perm AnyName -> Con -> Con
AlphaCtx -> NamePatFind -> Con -> Con
AlphaCtx -> NthPatFind -> Con -> Con
AlphaCtx -> Con -> Con -> Bool
AlphaCtx -> Con -> Con -> Ordering
Con -> Bool
Con -> All
Con -> NamePatFind
Con -> NthPatFind
Con -> DisjointSet AnyName
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
$caeq' :: AlphaCtx -> Con -> Con -> Bool
aeq' :: AlphaCtx -> Con -> Con -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Con -> f Con
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Con -> f Con
$cclose :: AlphaCtx -> NamePatFind -> Con -> Con
close :: AlphaCtx -> NamePatFind -> Con -> Con
$copen :: AlphaCtx -> NthPatFind -> Con -> Con
open :: AlphaCtx -> NthPatFind -> Con -> Con
$cisPat :: Con -> DisjointSet AnyName
isPat :: Con -> DisjointSet AnyName
$cisTerm :: Con -> All
isTerm :: Con -> All
$cisEmbed :: Con -> Bool
isEmbed :: Con -> Bool
$cnthPatFind :: Con -> NthPatFind
nthPatFind :: Con -> NthPatFind
$cnamePatFind :: Con -> NamePatFind
namePatFind :: Con -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> Con -> Con
swaps' :: AlphaCtx -> Perm AnyName -> Con -> Con
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Con -> m (Con, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Con -> m (Con, Perm AnyName)
$cacompare' :: AlphaCtx -> Con -> Con -> Ordering
acompare' :: AlphaCtx -> Con -> Con -> Ordering
Alpha)

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

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

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

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

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

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

-- | The main data type for representing types in the disco language.
--   A type can be either an atomic type, or the application of a type
--   constructor to one or more type arguments.
--
--   @Type@s are broken down into two cases (@TyAtom@ and @TyCon@) for
--   ease of implementation: there are many situations where all atoms
--   can be handled generically in one way and all type constructors
--   can be handled generically in another.  However, using this
--   representation to write down specific types is tedious; for
--   example, to represent the type @N -> a@ one must write something
--   like @TyCon CArr [TyAtom (ABase N), TyAtom (AVar (U a))]@.  For
--   this reason, pattern synonyms such as ':->:', 'TyN', and
--   'TyVar' are provided so that one can use them to construct and
--   pattern-match on types when convenient.  For example, using these
--   synonyms the foregoing example can be written @TyN :->: TyVar a@.
data Type where
  -- | Atomic types (variables and base types), /e.g./ @N@, @Bool@, /etc./
  TyAtom :: Atom -> Type
  -- | Application of a type constructor to type arguments, /e.g./ @N
  --   -> Bool@ is the application of the arrow type constructor to the
  --   arguments @N@ and @Bool@.
  TyCon :: Con -> [Type] -> Type
  deriving (Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Type -> ShowS
showsPrec :: Int -> Type -> ShowS
$cshow :: Type -> String
show :: Type -> String
$cshowList :: [Type] -> ShowS
showList :: [Type] -> ShowS
Show, Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
/= :: Type -> Type -> Bool
Eq, Eq Type
Eq Type =>
(Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Type -> Type -> Ordering
compare :: Type -> Type -> Ordering
$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
>= :: Type -> Type -> Bool
$cmax :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
min :: Type -> Type -> Type
Ord, (forall x. Type -> Rep Type x)
-> (forall x. Rep Type x -> Type) -> Generic Type
forall x. Rep Type x -> Type
forall x. Type -> Rep Type x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Type -> Rep Type x
from :: forall x. Type -> Rep Type x
$cto :: forall x. Rep Type x -> Type
to :: forall x. Rep Type x -> Type
Generic, Typeable Type
Typeable Type =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Type -> c Type)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Type)
-> (Type -> Constr)
-> (Type -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Type))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type))
-> ((forall b. Data b => b -> b) -> Type -> Type)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
-> (forall u. (forall d. Data d => d -> u) -> Type -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Type -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Type -> m Type)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Type -> m Type)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Type -> m Type)
-> Data Type
Type -> Constr
Type -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
$ctoConstr :: Type -> Constr
toConstr :: Type -> Constr
$cdataTypeOf :: Type -> DataType
dataTypeOf :: Type -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
$cgmapT :: (forall b. Data b => b -> b) -> Type -> Type
gmapT :: (forall b. Data b => b -> b) -> Type -> Type
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
Data, Show Type
Show Type =>
(AlphaCtx -> Type -> Type -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Type -> f Type)
-> (AlphaCtx -> NamePatFind -> Type -> Type)
-> (AlphaCtx -> NthPatFind -> Type -> Type)
-> (Type -> DisjointSet AnyName)
-> (Type -> All)
-> (Type -> Bool)
-> (Type -> NthPatFind)
-> (Type -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Type -> Type)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> Type -> (Type -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Type -> m (Type, Perm AnyName))
-> (AlphaCtx -> Type -> Type -> Ordering)
-> Alpha Type
AlphaCtx -> Perm AnyName -> Type -> Type
AlphaCtx -> NamePatFind -> Type -> Type
AlphaCtx -> NthPatFind -> Type -> Type
AlphaCtx -> Type -> Type -> Bool
AlphaCtx -> Type -> Type -> Ordering
Type -> Bool
Type -> All
Type -> NamePatFind
Type -> NthPatFind
Type -> DisjointSet AnyName
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
$caeq' :: AlphaCtx -> Type -> Type -> Bool
aeq' :: AlphaCtx -> Type -> Type -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Type -> f Type
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Type -> f Type
$cclose :: AlphaCtx -> NamePatFind -> Type -> Type
close :: AlphaCtx -> NamePatFind -> Type -> Type
$copen :: AlphaCtx -> NthPatFind -> Type -> Type
open :: AlphaCtx -> NthPatFind -> Type -> Type
$cisPat :: Type -> DisjointSet AnyName
isPat :: Type -> DisjointSet AnyName
$cisTerm :: Type -> All
isTerm :: Type -> All
$cisEmbed :: Type -> Bool
isEmbed :: Type -> Bool
$cnthPatFind :: Type -> NthPatFind
nthPatFind :: Type -> NthPatFind
$cnamePatFind :: Type -> NamePatFind
namePatFind :: Type -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> Type -> Type
swaps' :: AlphaCtx -> Perm AnyName -> Type -> Type
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Type -> (Type -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Type -> (Type -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Type -> m (Type, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Type -> m (Type, Perm AnyName)
$cacompare' :: AlphaCtx -> Type -> Type -> Ordering
acompare' :: AlphaCtx -> Type -> Type -> Ordering
Alpha)

instance Pretty Type where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
pretty (TyAtom Atom
a) = Atom -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Atom -> Sem r (Doc ann)
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) =
    PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
tarrPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
      Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"→" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
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) =
    PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
tmulPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
      Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"×" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
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) =
    PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
taddPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
      Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty1) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"+" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty2)
  pretty (TyCon Con
c []) = Con -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Con -> Sem r (Doc ann)
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 <- PA -> Sem r [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)])
-> Sem r [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") ((Type -> Sem r (Doc ann)) -> [Type] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Type]
tys)
    Con -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Con -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Con
c Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens ([Sem r (Doc ann)] -> Sem r (Doc ann)
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
_ = Rational -> Rational
forall a. a -> a
id
  substs :: [(Name Type, Type)] -> Rational -> Rational
substs [(Name Type, Type)]
_ = Rational -> Rational
forall a. a -> a
id
  substBvs :: AlphaCtx -> [Type] -> Rational -> Rational
substBvs AlphaCtx
_ [Type]
_ = Rational -> Rational
forall a. a -> a
id
instance Subst Type Void where
  subst :: Name Type -> Type -> Void -> Void
subst Name Type
_ Type
_ = Void -> Void
forall a. a -> a
id
  substs :: [(Name Type, Type)] -> Void -> Void
substs [(Name Type, Type)]
_ = Void -> Void
forall a. a -> a
id
instance Subst Type Con where
  isCoerceVar :: Con -> Maybe (SubstCoerce Con Type)
isCoerceVar (CContainer (AVar (U Name Type
x))) =
    SubstCoerce Con Type -> Maybe (SubstCoerce Con Type)
forall a. a -> Maybe a
Just (Name Type -> (Type -> Maybe Con) -> SubstCoerce Con Type
forall b a. Name b -> (b -> Maybe a) -> SubstCoerce a b
SubstCoerce Name Type
x Type -> Maybe Con
substCtrTy)
   where
    substCtrTy :: Type -> Maybe Con
substCtrTy (TyAtom Atom
a) = Con -> Maybe Con
forall a. a -> Maybe a
Just (Atom -> Con
CContainer Atom
a)
    substCtrTy Type
_ = Maybe Con
forall a. Maybe a
Nothing
  isCoerceVar Con
_ = Maybe (SubstCoerce Con Type)
forall a. Maybe a
Nothing
instance Subst Type Type where
  isvar :: Type -> Maybe (SubstName Type Type)
isvar (TyAtom (AVar (U Name Type
x))) = SubstName Type Type -> Maybe (SubstName Type Type)
forall a. a -> Maybe a
Just (Name Type -> SubstName Type Type
forall a b. (a ~ b) => Name a -> SubstName a b
SubstName Name Type
x)
  isvar Type
_ = Maybe (SubstName Type Type)
forall a. Maybe a
Nothing

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

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

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

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

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

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

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

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

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

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

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

pattern TyGen :: Type
pattern $mTyGen :: forall {r}. Type -> ((# #) -> r) -> ((# #) -> r) -> r
$bTyGen :: Type
TyGen = TyAtom (ABase Gen)

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

infixr 5 :->:

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

infixr 7 :*:

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

infixr 6 :+:

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

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

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

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

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

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

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

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

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

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

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

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

-- | 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" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
tyName Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> [String] -> Sem r (Doc ann)
prettyArgs [String]
ps) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"=" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty ([Type] -> Type
body ((String -> Type) -> [String] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name Type -> Type
TyVar (Name Type -> Type) -> (String -> Name Type) -> String -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name Type
forall a. String -> Name a
string2Name) [String]
ps))
   where
    prettyArgs :: [String] -> Sem r (Doc ann)
prettyArgs [] = Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty
    prettyArgs [String]
_ = do
      [Sem r (Doc ann)]
ds <- Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") ((String -> Sem r (Doc ann)) -> [String] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text [String]
ps)
      Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens ([Sem r (Doc ann)] -> Sem r (Doc ann)
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
(Int -> PolyType -> ShowS)
-> (PolyType -> String) -> ([PolyType] -> ShowS) -> Show PolyType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PolyType -> ShowS
showsPrec :: Int -> PolyType -> ShowS
$cshow :: PolyType -> String
show :: PolyType -> String
$cshowList :: [PolyType] -> ShowS
showList :: [PolyType] -> ShowS
Show, (forall x. PolyType -> Rep PolyType x)
-> (forall x. Rep PolyType x -> PolyType) -> Generic PolyType
forall x. Rep PolyType x -> PolyType
forall x. PolyType -> Rep PolyType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PolyType -> Rep PolyType x
from :: forall x. PolyType -> Rep PolyType x
$cto :: forall x. Rep PolyType x -> PolyType
to :: forall x. Rep PolyType x -> PolyType
Generic, Typeable PolyType
Typeable PolyType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PolyType -> c PolyType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PolyType)
-> (PolyType -> Constr)
-> (PolyType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PolyType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyType))
-> ((forall b. Data b => b -> b) -> PolyType -> PolyType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PolyType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PolyType -> r)
-> (forall u. (forall d. Data d => d -> u) -> PolyType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PolyType -> m PolyType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PolyType -> m PolyType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PolyType -> m PolyType)
-> Data PolyType
PolyType -> Constr
PolyType -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PolyType -> c PolyType
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PolyType -> c PolyType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PolyType
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PolyType
$ctoConstr :: PolyType -> Constr
toConstr :: PolyType -> Constr
$cdataTypeOf :: PolyType -> DataType
dataTypeOf :: PolyType -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PolyType)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PolyType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyType)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyType)
$cgmapT :: (forall b. Data b => b -> b) -> PolyType -> PolyType
gmapT :: (forall b. Data b => b -> b) -> PolyType -> PolyType
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PolyType -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PolyType -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> PolyType -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PolyType -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PolyType -> m PolyType
Data, Show PolyType
Show PolyType =>
(AlphaCtx -> PolyType -> PolyType -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> PolyType -> f PolyType)
-> (AlphaCtx -> NamePatFind -> PolyType -> PolyType)
-> (AlphaCtx -> NthPatFind -> PolyType -> PolyType)
-> (PolyType -> DisjointSet AnyName)
-> (PolyType -> All)
-> (PolyType -> Bool)
-> (PolyType -> NthPatFind)
-> (PolyType -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> PolyType -> PolyType)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> PolyType -> m (PolyType, Perm AnyName))
-> (AlphaCtx -> PolyType -> PolyType -> Ordering)
-> Alpha PolyType
AlphaCtx -> Perm AnyName -> PolyType -> PolyType
AlphaCtx -> NamePatFind -> PolyType -> PolyType
AlphaCtx -> NthPatFind -> PolyType -> PolyType
AlphaCtx -> PolyType -> PolyType -> Bool
AlphaCtx -> PolyType -> PolyType -> Ordering
PolyType -> Bool
PolyType -> All
PolyType -> NamePatFind
PolyType -> NthPatFind
PolyType -> DisjointSet AnyName
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
$caeq' :: AlphaCtx -> PolyType -> PolyType -> Bool
aeq' :: AlphaCtx -> PolyType -> PolyType -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> PolyType -> f PolyType
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> PolyType -> f PolyType
$cclose :: AlphaCtx -> NamePatFind -> PolyType -> PolyType
close :: AlphaCtx -> NamePatFind -> PolyType -> PolyType
$copen :: AlphaCtx -> NthPatFind -> PolyType -> PolyType
open :: AlphaCtx -> NthPatFind -> PolyType -> PolyType
$cisPat :: PolyType -> DisjointSet AnyName
isPat :: PolyType -> DisjointSet AnyName
$cisTerm :: PolyType -> All
isTerm :: PolyType -> All
$cisEmbed :: PolyType -> Bool
isEmbed :: PolyType -> Bool
$cnthPatFind :: PolyType -> NthPatFind
nthPatFind :: PolyType -> NthPatFind
$cnamePatFind :: PolyType -> NamePatFind
namePatFind :: PolyType -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> PolyType -> PolyType
swaps' :: AlphaCtx -> Perm AnyName -> PolyType -> PolyType
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> PolyType -> m (PolyType, Perm AnyName)
$cacompare' :: AlphaCtx -> PolyType -> PolyType -> Ordering
acompare' :: AlphaCtx -> PolyType -> PolyType -> Ordering
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) = Bind [Name Type] Type
-> (([Name Type], Type) -> Sem r (Doc ann)) -> Sem r (Doc ann)
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Name Type] Type
bnd ((([Name Type], Type) -> Sem r (Doc ann)) -> Sem r (Doc ann))
-> (([Name Type], Type) -> Sem r (Doc ann)) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
    \([Name Type]
_, Type
body) -> Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
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 ([Name Type] -> Type -> Bind [Name Type] Type
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [] Type
ty)

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

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

-- | Compute the number of inhabitants of a type.  @Nothing@ means the
--   type is countably infinite.
countType :: Type -> Maybe Integer
countType :: Type -> Maybe Integer
countType Type
TyVoid = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
countType Type
TyUnit = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
countType Type
TyBool = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
2
-- countType (TyFin n)     = Just n
countType Type
TyC = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
17 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
16 :: Integer))
countType (Type
ty1 :+: Type
ty2) = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty1 Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Integer
countType Type
ty2
countType (Type
ty1 :*: Type
ty2)
  | Type -> Bool
isEmptyTy Type
ty1 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
  | Type -> Bool
isEmptyTy Type
ty2 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
  | Bool
otherwise = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty1 Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Integer
countType Type
ty2
countType (Type
ty1 :->: Type
ty2) =
  case (Type -> Maybe Integer
countType Type
ty1, Type -> Maybe Integer
countType Type
ty2) of
    (Just Integer
0, Maybe Integer
_) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
    (Maybe Integer
_, Just Integer
0) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
    (Maybe Integer
_, Just Integer
1) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
    (Maybe Integer
c1, Maybe Integer
c2) -> Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
(^) (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
c2 Maybe (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Integer
c1
countType (TyList Type
ty)
  | Type -> Bool
isEmptyTy Type
ty = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
  | Bool
otherwise = Maybe Integer
forall a. Maybe a
Nothing
countType (TyBag Type
ty)
  | Type -> Bool
isEmptyTy Type
ty = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
  | Bool
otherwise = Maybe Integer
forall a. Maybe a
Nothing
countType (TySet Type
ty) = (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
countType Type
ty
-- t = number of elements in vertex type.
-- n = number of vertices in the graph.
-- For each n in [0..t], we can choose which n values to use for the
--   vertices; then for each ordered pair of vertices (u,v)
--   (including the possibility that u = v), we choose whether or
--   not there is a directed edge u -> v.
--
-- https://oeis.org/A135748

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | A type class for things whose type can be extracted or set.
class HasType t where
  -- | Get the type of a thing.
  getType :: t -> Type

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