{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
-- Orphan Alpha Void instance
{-# OPTIONS_GHC -fno-warn-orphans #-}

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

-- |
-- Module      :  Disco.AST.Generic
-- Copyright   :  disco team and contributors
-- Maintainer  :  [email protected]
--
-- Abstract syntax trees representing the generic syntax of the Disco
-- language. Concrete AST instances may use this module as a template.
--
-- For more detail on the approach used here, see
--
-- Najd and Peyton Jones, "Trees that Grow". Journal of Universal
-- Computer Science, vol. 23 no. 1 (2017), 42-62.
-- <https://arxiv.org/abs/1610.04799>
--
-- Essentially, we define a basic generic 'Term_' type, with a type
-- index to indicate what kind of term it is, i.e. what phase the term
-- belongs to.  Each constructor has a type family used to define any
-- extra data that should go in the constructor for a particular
-- phase; there is also one additional constructor which can be used
-- to store arbitrary additional information, again governed by a type
-- family.  Together with the use of pattern synonyms, the result is
-- that it looks like we have a different type for each phase, each
-- with its own set of constructors, but in fact all use the same
-- underlying type.  Particular instantiations of the generic
-- framework here can be found in "Disco.AST.Surface",
-- "Disco.AST.Typed", and "Disco.AST.Desugared".
module Disco.AST.Generic (
  -- * Telescopes
  Telescope (..),
  telCons,
  foldTelescope,
  mapTelescope,
  traverseTelescope,
  toTelescope,
  fromTelescope,

  -- * Utility types
  Side (..),
  selectSide,
  fromSide,
  Container (..),
  Ellipsis (..),

  -- * Term
  Term_ (..),
  X_TVar,
  X_TPrim,
  X_TLet,
  X_TParens,
  X_TUnit,
  X_TBool,
  X_TNat,
  X_TRat,
  X_TChar,
  X_TString,
  X_TAbs,
  X_TApp,
  X_TTup,
  X_TCase,
  X_TChain,
  X_TTyOp,
  X_TContainer,
  X_TContainerComp,
  X_TAscr,
  X_Term,
  ForallTerm,

  -- * Link
  Link_ (..),
  X_TLink,
  ForallLink,

  -- * Qual
  Qual_ (..),
  X_QBind,
  X_QGuard,
  ForallQual,

  -- * Binding
  Binding_ (..),

  -- * Branch
  Branch_,

  -- * Guard
  Guard_ (..),
  X_GBool,
  X_GPat,
  X_GLet,
  ForallGuard,

  -- * Pattern
  Pattern_ (..),
  X_PVar,
  X_PWild,
  X_PAscr,
  X_PUnit,
  X_PBool,
  X_PTup,
  X_PInj,
  X_PNat,
  X_PChar,
  X_PString,
  X_PCons,
  X_PList,
  X_PAdd,
  X_PMul,
  X_PSub,
  X_PNeg,
  X_PFrac,
  X_Pattern,
  ForallPattern,

  -- * Quantifiers
  Quantifier (..),
  Binder_,
  X_Binder,

  -- * Property
  Property_,
)
where

import Control.Lens.Plated
import Data.Data (Data)
import Data.Data.Lens (uniplate)
import Data.Typeable
import GHC.Exts (Constraint)
import GHC.Generics (Generic)

import Data.Void
import Unbound.Generics.LocallyNameless

import Disco.Pretty
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Types

------------------------------------------------------------
-- Telescopes
------------------------------------------------------------

-- | A telescope is essentially a list, except that each item can bind
--   names in the rest of the list.
data Telescope b where
  -- | The empty telescope.
  TelEmpty :: Telescope b
  -- | A binder of type @b@ followed by zero or more @b@'s.  This @b@
  --   can bind variables in the subsequent @b@'s.
  TelCons :: Rebind b (Telescope b) -> Telescope b
  deriving (Int -> Telescope b -> ShowS
[Telescope b] -> ShowS
Telescope b -> String
(Int -> Telescope b -> ShowS)
-> (Telescope b -> String)
-> ([Telescope b] -> ShowS)
-> Show (Telescope b)
forall b. Show b => Int -> Telescope b -> ShowS
forall b. Show b => [Telescope b] -> ShowS
forall b. Show b => Telescope b -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall b. Show b => Int -> Telescope b -> ShowS
showsPrec :: Int -> Telescope b -> ShowS
$cshow :: forall b. Show b => Telescope b -> String
show :: Telescope b -> String
$cshowList :: forall b. Show b => [Telescope b] -> ShowS
showList :: [Telescope b] -> ShowS
Show, (forall x. Telescope b -> Rep (Telescope b) x)
-> (forall x. Rep (Telescope b) x -> Telescope b)
-> Generic (Telescope b)
forall x. Rep (Telescope b) x -> Telescope b
forall x. Telescope b -> Rep (Telescope b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall b x. Rep (Telescope b) x -> Telescope b
forall b x. Telescope b -> Rep (Telescope b) x
$cfrom :: forall b x. Telescope b -> Rep (Telescope b) x
from :: forall x. Telescope b -> Rep (Telescope b) x
$cto :: forall b x. Rep (Telescope b) x -> Telescope b
to :: forall x. Rep (Telescope b) x -> Telescope b
Generic, Show (Telescope b)
Show (Telescope b) =>
(AlphaCtx -> Telescope b -> Telescope b -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx
    -> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b))
-> (AlphaCtx -> NamePatFind -> Telescope b -> Telescope b)
-> (AlphaCtx -> NthPatFind -> Telescope b -> Telescope b)
-> (Telescope b -> DisjointSet AnyName)
-> (Telescope b -> All)
-> (Telescope b -> Bool)
-> (Telescope b -> NthPatFind)
-> (Telescope b -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx
    -> Telescope b -> (Telescope b -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName))
-> (AlphaCtx -> Telescope b -> Telescope b -> Ordering)
-> Alpha (Telescope b)
AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b
AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
AlphaCtx -> NthPatFind -> Telescope b -> Telescope b
AlphaCtx -> Telescope b -> Telescope b -> Bool
AlphaCtx -> Telescope b -> Telescope b -> Ordering
Telescope b -> Bool
Telescope b -> All
Telescope b -> NamePatFind
Telescope b -> NthPatFind
Telescope b -> 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 b. Alpha b => Show (Telescope b)
forall b.
Alpha b =>
AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b
forall b.
Alpha b =>
AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
forall b.
Alpha b =>
AlphaCtx -> NthPatFind -> Telescope b -> Telescope b
forall b. Alpha b => AlphaCtx -> Telescope b -> Telescope b -> Bool
forall b.
Alpha b =>
AlphaCtx -> Telescope b -> Telescope b -> Ordering
forall b. Alpha b => Telescope b -> Bool
forall b. Alpha b => Telescope b -> All
forall b. Alpha b => Telescope b -> NamePatFind
forall b. Alpha b => Telescope b -> NthPatFind
forall b. Alpha b => Telescope b -> DisjointSet AnyName
forall b (f :: * -> *).
(Alpha b, Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b)
forall b (m :: * -> *).
(Alpha b, Fresh m) =>
AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName)
forall b (m :: * -> *) b.
(Alpha b, LFresh m) =>
AlphaCtx
-> Telescope b -> (Telescope b -> Perm AnyName -> m b) -> m b
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b)
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Telescope b -> (Telescope b -> Perm AnyName -> m b) -> m b
$caeq' :: forall b. Alpha b => AlphaCtx -> Telescope b -> Telescope b -> Bool
aeq' :: AlphaCtx -> Telescope b -> Telescope b -> Bool
$cfvAny' :: forall b (f :: * -> *).
(Alpha b, Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b)
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b)
$cclose :: forall b.
Alpha b =>
AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
close :: AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
$copen :: forall b.
Alpha b =>
AlphaCtx -> NthPatFind -> Telescope b -> Telescope b
open :: AlphaCtx -> NthPatFind -> Telescope b -> Telescope b
$cisPat :: forall b. Alpha b => Telescope b -> DisjointSet AnyName
isPat :: Telescope b -> DisjointSet AnyName
$cisTerm :: forall b. Alpha b => Telescope b -> All
isTerm :: Telescope b -> All
$cisEmbed :: forall b. Alpha b => Telescope b -> Bool
isEmbed :: Telescope b -> Bool
$cnthPatFind :: forall b. Alpha b => Telescope b -> NthPatFind
nthPatFind :: Telescope b -> NthPatFind
$cnamePatFind :: forall b. Alpha b => Telescope b -> NamePatFind
namePatFind :: Telescope b -> NamePatFind
$cswaps' :: forall b.
Alpha b =>
AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b
swaps' :: AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b
$clfreshen' :: forall b (m :: * -> *) b.
(Alpha b, LFresh m) =>
AlphaCtx
-> Telescope b -> (Telescope b -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Telescope b -> (Telescope b -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall b (m :: * -> *).
(Alpha b, Fresh m) =>
AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName)
$cacompare' :: forall b.
Alpha b =>
AlphaCtx -> Telescope b -> Telescope b -> Ordering
acompare' :: AlphaCtx -> Telescope b -> Telescope b -> Ordering
Alpha, Subst t, Typeable (Telescope b)
Typeable (Telescope b) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Telescope b -> c (Telescope b))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Telescope b))
-> (Telescope b -> Constr)
-> (Telescope b -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Telescope b)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Telescope b)))
-> ((forall b. Data b => b -> b) -> Telescope b -> Telescope b)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Telescope b -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Telescope b -> r)
-> (forall u. (forall d. Data d => d -> u) -> Telescope b -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Telescope b -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b))
-> Data (Telescope b)
Telescope b -> Constr
Telescope b -> DataType
(forall b. Data b => b -> b) -> Telescope b -> Telescope b
forall b. Data b => Typeable (Telescope b)
forall b. Data b => Telescope b -> Constr
forall b. Data b => Telescope b -> DataType
forall b.
Data b =>
(forall b. Data b => b -> b) -> Telescope b -> Telescope b
forall b u.
Data b =>
Int -> (forall d. Data d => d -> u) -> Telescope b -> u
forall b u.
Data b =>
(forall d. Data d => d -> u) -> Telescope b -> [u]
forall b r r'.
Data b =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
forall b r r'.
Data b =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
forall b (m :: * -> *).
(Data b, Monad m) =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
forall b (m :: * -> *).
(Data b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
forall b (c :: * -> *).
Data b =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Telescope b)
forall b (c :: * -> *).
Data b =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Telescope b -> c (Telescope b)
forall b (t :: * -> *) (c :: * -> *).
(Data b, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
forall b (t :: * -> * -> *) (c :: * -> *).
(Data b, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Telescope b))
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) -> Telescope b -> u
forall u. (forall d. Data d => d -> u) -> Telescope b -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Telescope b)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Telescope b -> c (Telescope b)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Telescope b))
$cgfoldl :: forall b (c :: * -> *).
Data b =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Telescope b -> c (Telescope b)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Telescope b -> c (Telescope b)
$cgunfold :: forall b (c :: * -> *).
Data b =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Telescope b)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Telescope b)
$ctoConstr :: forall b. Data b => Telescope b -> Constr
toConstr :: Telescope b -> Constr
$cdataTypeOf :: forall b. Data b => Telescope b -> DataType
dataTypeOf :: Telescope b -> DataType
$cdataCast1 :: forall b (t :: * -> *) (c :: * -> *).
(Data b, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
$cdataCast2 :: forall b (t :: * -> * -> *) (c :: * -> *).
(Data b, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Telescope b))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Telescope b))
$cgmapT :: forall b.
Data b =>
(forall b. Data b => b -> b) -> Telescope b -> Telescope b
gmapT :: (forall b. Data b => b -> b) -> Telescope b -> Telescope b
$cgmapQl :: forall b r r'.
Data b =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
$cgmapQr :: forall b r r'.
Data b =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
$cgmapQ :: forall b u.
Data b =>
(forall d. Data d => d -> u) -> Telescope b -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Telescope b -> [u]
$cgmapQi :: forall b u.
Data b =>
Int -> (forall d. Data d => d -> u) -> Telescope b -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Telescope b -> u
$cgmapM :: forall b (m :: * -> *).
(Data b, Monad m) =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
$cgmapMp :: forall b (m :: * -> *).
(Data b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
$cgmapMo :: forall b (m :: * -> *).
(Data b, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
Data)

-- | Add a new item to the beginning of a 'Telescope'.
telCons :: Alpha b => b -> Telescope b -> Telescope b
telCons :: forall b. Alpha b => b -> Telescope b -> Telescope b
telCons b
b Telescope b
tb = Rebind b (Telescope b) -> Telescope b
forall b. Rebind b (Telescope b) -> Telescope b
TelCons (b -> Telescope b -> Rebind b (Telescope b)
forall p1 p2. (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2
rebind b
b Telescope b
tb)

-- | Fold a telescope given a combining function and a value to use
--   for the empty telescope.  Analogous to 'foldr' for lists.
foldTelescope :: Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope :: forall b r. Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope b -> r -> r
_ r
z Telescope b
TelEmpty = r
z
foldTelescope b -> r -> r
f r
z (TelCons (Rebind b (Telescope b) -> (b, Telescope b)
forall p1 p2. (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
unrebind -> (b
b, Telescope b
bs))) = b -> r -> r
f b
b ((b -> r -> r) -> r -> Telescope b -> r
forall b r. Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope b -> r -> r
f r
z Telescope b
bs)

-- | Apply a function to every item in a telescope.
mapTelescope :: (Alpha a, Alpha b) => (a -> b) -> Telescope a -> Telescope b
mapTelescope :: forall a b.
(Alpha a, Alpha b) =>
(a -> b) -> Telescope a -> Telescope b
mapTelescope a -> b
f = [b] -> Telescope b
forall b. Alpha b => [b] -> Telescope b
toTelescope ([b] -> Telescope b)
-> (Telescope a -> [b]) -> Telescope a -> Telescope b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f ([a] -> [b]) -> (Telescope a -> [a]) -> Telescope a -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope a -> [a]
forall b. Alpha b => Telescope b -> [b]
fromTelescope

-- | Traverse over a telescope.
traverseTelescope ::
  (Applicative f, Alpha a, Alpha b) =>
  (a -> f b) ->
  Telescope a ->
  f (Telescope b)
traverseTelescope :: forall (f :: * -> *) a b.
(Applicative f, Alpha a, Alpha b) =>
(a -> f b) -> Telescope a -> f (Telescope b)
traverseTelescope a -> f b
f = (a -> f (Telescope b) -> f (Telescope b))
-> f (Telescope b) -> Telescope a -> f (Telescope b)
forall b r. Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope (\a
a f (Telescope b)
ftb -> b -> Telescope b -> Telescope b
forall b. Alpha b => b -> Telescope b -> Telescope b
telCons (b -> Telescope b -> Telescope b)
-> f b -> f (Telescope b -> Telescope b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
a f (Telescope b -> Telescope b)
-> f (Telescope b) -> f (Telescope b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Telescope b)
ftb) (Telescope b -> f (Telescope b)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Telescope b
forall b. Telescope b
TelEmpty)

-- | Convert a list to a telescope.
toTelescope :: Alpha b => [b] -> Telescope b
toTelescope :: forall b. Alpha b => [b] -> Telescope b
toTelescope = (b -> Telescope b -> Telescope b)
-> Telescope b -> [b] -> Telescope b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr b -> Telescope b -> Telescope b
forall b. Alpha b => b -> Telescope b -> Telescope b
telCons Telescope b
forall b. Telescope b
TelEmpty

-- | Convert a telescope to a list.
fromTelescope :: Alpha b => Telescope b -> [b]
fromTelescope :: forall b. Alpha b => Telescope b -> [b]
fromTelescope = (b -> [b] -> [b]) -> [b] -> Telescope b -> [b]
forall b r. Alpha b => (b -> r -> r) -> r -> Telescope b -> r
foldTelescope (:) []

------------------------------------------------------------
-- Utility types
------------------------------------------------------------

-- | Injections into a sum type (@inl@ or @inr@) have a "side" (@L@ or @R@).
data Side = L | R
  deriving (Int -> Side -> ShowS
[Side] -> ShowS
Side -> String
(Int -> Side -> ShowS)
-> (Side -> String) -> ([Side] -> ShowS) -> Show Side
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Side -> ShowS
showsPrec :: Int -> Side -> ShowS
$cshow :: Side -> String
show :: Side -> String
$cshowList :: [Side] -> ShowS
showList :: [Side] -> ShowS
Show, Side -> Side -> Bool
(Side -> Side -> Bool) -> (Side -> Side -> Bool) -> Eq Side
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Side -> Side -> Bool
== :: Side -> Side -> Bool
$c/= :: Side -> Side -> Bool
/= :: Side -> Side -> Bool
Eq, Eq Side
Eq Side =>
(Side -> Side -> Ordering)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Bool)
-> (Side -> Side -> Side)
-> (Side -> Side -> Side)
-> Ord Side
Side -> Side -> Bool
Side -> Side -> Ordering
Side -> Side -> Side
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 :: Side -> Side -> Ordering
compare :: Side -> Side -> Ordering
$c< :: Side -> Side -> Bool
< :: Side -> Side -> Bool
$c<= :: Side -> Side -> Bool
<= :: Side -> Side -> Bool
$c> :: Side -> Side -> Bool
> :: Side -> Side -> Bool
$c>= :: Side -> Side -> Bool
>= :: Side -> Side -> Bool
$cmax :: Side -> Side -> Side
max :: Side -> Side -> Side
$cmin :: Side -> Side -> Side
min :: Side -> Side -> Side
Ord, Int -> Side
Side -> Int
Side -> [Side]
Side -> Side
Side -> Side -> [Side]
Side -> Side -> Side -> [Side]
(Side -> Side)
-> (Side -> Side)
-> (Int -> Side)
-> (Side -> Int)
-> (Side -> [Side])
-> (Side -> Side -> [Side])
-> (Side -> Side -> [Side])
-> (Side -> Side -> Side -> [Side])
-> Enum Side
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Side -> Side
succ :: Side -> Side
$cpred :: Side -> Side
pred :: Side -> Side
$ctoEnum :: Int -> Side
toEnum :: Int -> Side
$cfromEnum :: Side -> Int
fromEnum :: Side -> Int
$cenumFrom :: Side -> [Side]
enumFrom :: Side -> [Side]
$cenumFromThen :: Side -> Side -> [Side]
enumFromThen :: Side -> Side -> [Side]
$cenumFromTo :: Side -> Side -> [Side]
enumFromTo :: Side -> Side -> [Side]
$cenumFromThenTo :: Side -> Side -> Side -> [Side]
enumFromThenTo :: Side -> Side -> Side -> [Side]
Enum, Side
Side -> Side -> Bounded Side
forall a. a -> a -> Bounded a
$cminBound :: Side
minBound :: Side
$cmaxBound :: Side
maxBound :: Side
Bounded, (forall x. Side -> Rep Side x)
-> (forall x. Rep Side x -> Side) -> Generic Side
forall x. Rep Side x -> Side
forall x. Side -> Rep Side x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Side -> Rep Side x
from :: forall x. Side -> Rep Side x
$cto :: forall x. Rep Side x -> Side
to :: forall x. Rep Side x -> Side
Generic, Typeable Side
Typeable Side =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Side -> c Side)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Side)
-> (Side -> Constr)
-> (Side -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Side))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Side))
-> ((forall b. Data b => b -> b) -> Side -> Side)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r)
-> (forall u. (forall d. Data d => d -> u) -> Side -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Side -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Side -> m Side)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Side -> m Side)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Side -> m Side)
-> Data Side
Side -> Constr
Side -> DataType
(forall b. Data b => b -> b) -> Side -> Side
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) -> Side -> u
forall u. (forall d. Data d => d -> u) -> Side -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Side -> m Side
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Side -> m Side
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Side
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Side -> c Side
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Side)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Side)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Side -> c Side
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Side -> c Side
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Side
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Side
$ctoConstr :: Side -> Constr
toConstr :: Side -> Constr
$cdataTypeOf :: Side -> DataType
dataTypeOf :: Side -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Side)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Side)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Side)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Side)
$cgmapT :: (forall b. Data b => b -> b) -> Side -> Side
gmapT :: (forall b. Data b => b -> b) -> Side -> Side
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Side -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Side -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Side -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Side -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Side -> m Side
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Side -> m Side
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Side -> m Side
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Side -> m Side
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Side -> m Side
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Side -> m Side
Data, Show Side
Show Side =>
(AlphaCtx -> Side -> Side -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Side -> f Side)
-> (AlphaCtx -> NamePatFind -> Side -> Side)
-> (AlphaCtx -> NthPatFind -> Side -> Side)
-> (Side -> DisjointSet AnyName)
-> (Side -> All)
-> (Side -> Bool)
-> (Side -> NthPatFind)
-> (Side -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Side -> Side)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Side -> m (Side, Perm AnyName))
-> (AlphaCtx -> Side -> Side -> Ordering)
-> Alpha Side
AlphaCtx -> Perm AnyName -> Side -> Side
AlphaCtx -> NamePatFind -> Side -> Side
AlphaCtx -> NthPatFind -> Side -> Side
AlphaCtx -> Side -> Side -> Bool
AlphaCtx -> Side -> Side -> Ordering
Side -> Bool
Side -> All
Side -> NamePatFind
Side -> NthPatFind
Side -> 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) -> Side -> f Side
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Side -> m (Side, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b
$caeq' :: AlphaCtx -> Side -> Side -> Bool
aeq' :: AlphaCtx -> Side -> Side -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Side -> f Side
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Side -> f Side
$cclose :: AlphaCtx -> NamePatFind -> Side -> Side
close :: AlphaCtx -> NamePatFind -> Side -> Side
$copen :: AlphaCtx -> NthPatFind -> Side -> Side
open :: AlphaCtx -> NthPatFind -> Side -> Side
$cisPat :: Side -> DisjointSet AnyName
isPat :: Side -> DisjointSet AnyName
$cisTerm :: Side -> All
isTerm :: Side -> All
$cisEmbed :: Side -> Bool
isEmbed :: Side -> Bool
$cnthPatFind :: Side -> NthPatFind
nthPatFind :: Side -> NthPatFind
$cnamePatFind :: Side -> NamePatFind
namePatFind :: Side -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> Side -> Side
swaps' :: AlphaCtx -> Perm AnyName -> Side -> Side
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Side -> m (Side, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Side -> m (Side, Perm AnyName)
$cacompare' :: AlphaCtx -> Side -> Side -> Ordering
acompare' :: AlphaCtx -> Side -> Side -> Ordering
Alpha, Subst t)

instance Pretty Side where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Side -> Sem r (Doc ann)
pretty = \case
    Side
L -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"left"
    Side
R -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"right"

-- | Use a 'Side' to select one of two arguments (the first argument
--   for 'L', and the second for 'R').
selectSide :: Side -> a -> a -> a
selectSide :: forall a. Side -> a -> a -> a
selectSide Side
L a
a a
_ = a
a
selectSide Side
R a
_ a
b = a
b

-- | Convert a 'Side' to a boolean.
fromSide :: Side -> Bool
fromSide :: Side -> Bool
fromSide Side
s = Side -> Bool -> Bool -> Bool
forall a. Side -> a -> a -> a
selectSide Side
s Bool
False Bool
True

-- | An enumeration of the different kinds of containers in disco:
--   lists, bags, and sets.
data Container where
  ListContainer :: Container
  BagContainer :: Container
  SetContainer :: Container
  deriving (Int -> Container -> ShowS
[Container] -> ShowS
Container -> String
(Int -> Container -> ShowS)
-> (Container -> String)
-> ([Container] -> ShowS)
-> Show Container
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Container -> ShowS
showsPrec :: Int -> Container -> ShowS
$cshow :: Container -> String
show :: Container -> String
$cshowList :: [Container] -> ShowS
showList :: [Container] -> ShowS
Show, Container -> Container -> Bool
(Container -> Container -> Bool)
-> (Container -> Container -> Bool) -> Eq Container
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Container -> Container -> Bool
== :: Container -> Container -> Bool
$c/= :: Container -> Container -> Bool
/= :: Container -> Container -> Bool
Eq, Int -> Container
Container -> Int
Container -> [Container]
Container -> Container
Container -> Container -> [Container]
Container -> Container -> Container -> [Container]
(Container -> Container)
-> (Container -> Container)
-> (Int -> Container)
-> (Container -> Int)
-> (Container -> [Container])
-> (Container -> Container -> [Container])
-> (Container -> Container -> [Container])
-> (Container -> Container -> Container -> [Container])
-> Enum Container
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Container -> Container
succ :: Container -> Container
$cpred :: Container -> Container
pred :: Container -> Container
$ctoEnum :: Int -> Container
toEnum :: Int -> Container
$cfromEnum :: Container -> Int
fromEnum :: Container -> Int
$cenumFrom :: Container -> [Container]
enumFrom :: Container -> [Container]
$cenumFromThen :: Container -> Container -> [Container]
enumFromThen :: Container -> Container -> [Container]
$cenumFromTo :: Container -> Container -> [Container]
enumFromTo :: Container -> Container -> [Container]
$cenumFromThenTo :: Container -> Container -> Container -> [Container]
enumFromThenTo :: Container -> Container -> Container -> [Container]
Enum, (forall x. Container -> Rep Container x)
-> (forall x. Rep Container x -> Container) -> Generic Container
forall x. Rep Container x -> Container
forall x. Container -> Rep Container x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Container -> Rep Container x
from :: forall x. Container -> Rep Container x
$cto :: forall x. Rep Container x -> Container
to :: forall x. Rep Container x -> Container
Generic, Typeable Container
Typeable Container =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Container -> c Container)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Container)
-> (Container -> Constr)
-> (Container -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Container))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Container))
-> ((forall b. Data b => b -> b) -> Container -> Container)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Container -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Container -> r)
-> (forall u. (forall d. Data d => d -> u) -> Container -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Container -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Container -> m Container)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Container -> m Container)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Container -> m Container)
-> Data Container
Container -> Constr
Container -> DataType
(forall b. Data b => b -> b) -> Container -> Container
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) -> Container -> u
forall u. (forall d. Data d => d -> u) -> Container -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Container -> m Container
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Container -> m Container
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Container
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Container -> c Container
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Container)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Container)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Container -> c Container
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Container -> c Container
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Container
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Container
$ctoConstr :: Container -> Constr
toConstr :: Container -> Constr
$cdataTypeOf :: Container -> DataType
dataTypeOf :: Container -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Container)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Container)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Container)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Container)
$cgmapT :: (forall b. Data b => b -> b) -> Container -> Container
gmapT :: (forall b. Data b => b -> b) -> Container -> Container
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Container -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Container -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Container -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Container -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Container -> m Container
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Container -> m Container
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Container -> m Container
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Container -> m Container
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Container -> m Container
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Container -> m Container
Data, Show Container
Show Container =>
(AlphaCtx -> Container -> Container -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Container -> f Container)
-> (AlphaCtx -> NamePatFind -> Container -> Container)
-> (AlphaCtx -> NthPatFind -> Container -> Container)
-> (Container -> DisjointSet AnyName)
-> (Container -> All)
-> (Container -> Bool)
-> (Container -> NthPatFind)
-> (Container -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Container -> Container)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> Container -> (Container -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Container -> m (Container, Perm AnyName))
-> (AlphaCtx -> Container -> Container -> Ordering)
-> Alpha Container
AlphaCtx -> Perm AnyName -> Container -> Container
AlphaCtx -> NamePatFind -> Container -> Container
AlphaCtx -> NthPatFind -> Container -> Container
AlphaCtx -> Container -> Container -> Bool
AlphaCtx -> Container -> Container -> Ordering
Container -> Bool
Container -> All
Container -> NamePatFind
Container -> NthPatFind
Container -> 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) -> Container -> f Container
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Container -> m (Container, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Container -> (Container -> Perm AnyName -> m b) -> m b
$caeq' :: AlphaCtx -> Container -> Container -> Bool
aeq' :: AlphaCtx -> Container -> Container -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Container -> f Container
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Container -> f Container
$cclose :: AlphaCtx -> NamePatFind -> Container -> Container
close :: AlphaCtx -> NamePatFind -> Container -> Container
$copen :: AlphaCtx -> NthPatFind -> Container -> Container
open :: AlphaCtx -> NthPatFind -> Container -> Container
$cisPat :: Container -> DisjointSet AnyName
isPat :: Container -> DisjointSet AnyName
$cisTerm :: Container -> All
isTerm :: Container -> All
$cisEmbed :: Container -> Bool
isEmbed :: Container -> Bool
$cnthPatFind :: Container -> NthPatFind
nthPatFind :: Container -> NthPatFind
$cnamePatFind :: Container -> NamePatFind
namePatFind :: Container -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> Container -> Container
swaps' :: AlphaCtx -> Perm AnyName -> Container -> Container
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Container -> (Container -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Container -> (Container -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Container -> m (Container, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Container -> m (Container, Perm AnyName)
$cacompare' :: AlphaCtx -> Container -> Container -> Ordering
acompare' :: AlphaCtx -> Container -> Container -> Ordering
Alpha, Subst t)

-- | An ellipsis is an "omitted" part of a literal container (such as
--   a list or set), of the form @.. t@.  We don't have open-ended
--   ellipses since everything is evaluated eagerly and hence
--   containers must be finite.
data Ellipsis t where
  -- | 'Until' represents an ellipsis with a given endpoint, as in @[3 .. 20]@.
  Until :: t -> Ellipsis t -- @.. t@
  deriving (Int -> Ellipsis t -> ShowS
[Ellipsis t] -> ShowS
Ellipsis t -> String
(Int -> Ellipsis t -> ShowS)
-> (Ellipsis t -> String)
-> ([Ellipsis t] -> ShowS)
-> Show (Ellipsis t)
forall t. Show t => Int -> Ellipsis t -> ShowS
forall t. Show t => [Ellipsis t] -> ShowS
forall t. Show t => Ellipsis t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> Ellipsis t -> ShowS
showsPrec :: Int -> Ellipsis t -> ShowS
$cshow :: forall t. Show t => Ellipsis t -> String
show :: Ellipsis t -> String
$cshowList :: forall t. Show t => [Ellipsis t] -> ShowS
showList :: [Ellipsis t] -> ShowS
Show, (forall x. Ellipsis t -> Rep (Ellipsis t) x)
-> (forall x. Rep (Ellipsis t) x -> Ellipsis t)
-> Generic (Ellipsis t)
forall x. Rep (Ellipsis t) x -> Ellipsis t
forall x. Ellipsis t -> Rep (Ellipsis t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (Ellipsis t) x -> Ellipsis t
forall t x. Ellipsis t -> Rep (Ellipsis t) x
$cfrom :: forall t x. Ellipsis t -> Rep (Ellipsis t) x
from :: forall x. Ellipsis t -> Rep (Ellipsis t) x
$cto :: forall t x. Rep (Ellipsis t) x -> Ellipsis t
to :: forall x. Rep (Ellipsis t) x -> Ellipsis t
Generic, (forall a b. (a -> b) -> Ellipsis a -> Ellipsis b)
-> (forall a b. a -> Ellipsis b -> Ellipsis a) -> Functor Ellipsis
forall a b. a -> Ellipsis b -> Ellipsis a
forall a b. (a -> b) -> Ellipsis a -> Ellipsis b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Ellipsis a -> Ellipsis b
fmap :: forall a b. (a -> b) -> Ellipsis a -> Ellipsis b
$c<$ :: forall a b. a -> Ellipsis b -> Ellipsis a
<$ :: forall a b. a -> Ellipsis b -> Ellipsis a
Functor, (forall m. Monoid m => Ellipsis m -> m)
-> (forall m a. Monoid m => (a -> m) -> Ellipsis a -> m)
-> (forall m a. Monoid m => (a -> m) -> Ellipsis a -> m)
-> (forall a b. (a -> b -> b) -> b -> Ellipsis a -> b)
-> (forall a b. (a -> b -> b) -> b -> Ellipsis a -> b)
-> (forall b a. (b -> a -> b) -> b -> Ellipsis a -> b)
-> (forall b a. (b -> a -> b) -> b -> Ellipsis a -> b)
-> (forall a. (a -> a -> a) -> Ellipsis a -> a)
-> (forall a. (a -> a -> a) -> Ellipsis a -> a)
-> (forall a. Ellipsis a -> [a])
-> (forall a. Ellipsis a -> Bool)
-> (forall a. Ellipsis a -> Int)
-> (forall a. Eq a => a -> Ellipsis a -> Bool)
-> (forall a. Ord a => Ellipsis a -> a)
-> (forall a. Ord a => Ellipsis a -> a)
-> (forall a. Num a => Ellipsis a -> a)
-> (forall a. Num a => Ellipsis a -> a)
-> Foldable Ellipsis
forall a. Eq a => a -> Ellipsis a -> Bool
forall a. Num a => Ellipsis a -> a
forall a. Ord a => Ellipsis a -> a
forall m. Monoid m => Ellipsis m -> m
forall a. Ellipsis a -> Bool
forall a. Ellipsis a -> Int
forall a. Ellipsis a -> [a]
forall a. (a -> a -> a) -> Ellipsis a -> a
forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Ellipsis m -> m
fold :: forall m. Monoid m => Ellipsis m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
foldr1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
foldl1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
$ctoList :: forall a. Ellipsis a -> [a]
toList :: forall a. Ellipsis a -> [a]
$cnull :: forall a. Ellipsis a -> Bool
null :: forall a. Ellipsis a -> Bool
$clength :: forall a. Ellipsis a -> Int
length :: forall a. Ellipsis a -> Int
$celem :: forall a. Eq a => a -> Ellipsis a -> Bool
elem :: forall a. Eq a => a -> Ellipsis a -> Bool
$cmaximum :: forall a. Ord a => Ellipsis a -> a
maximum :: forall a. Ord a => Ellipsis a -> a
$cminimum :: forall a. Ord a => Ellipsis a -> a
minimum :: forall a. Ord a => Ellipsis a -> a
$csum :: forall a. Num a => Ellipsis a -> a
sum :: forall a. Num a => Ellipsis a -> a
$cproduct :: forall a. Num a => Ellipsis a -> a
product :: forall a. Num a => Ellipsis a -> a
Foldable, Functor Ellipsis
Foldable Ellipsis
(Functor Ellipsis, Foldable Ellipsis) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Ellipsis a -> f (Ellipsis b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Ellipsis (f a) -> f (Ellipsis a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Ellipsis a -> m (Ellipsis b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Ellipsis (m a) -> m (Ellipsis a))
-> Traversable Ellipsis
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Ellipsis (m a) -> m (Ellipsis a)
forall (f :: * -> *) a.
Applicative f =>
Ellipsis (f a) -> f (Ellipsis a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ellipsis a -> m (Ellipsis b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ellipsis a -> f (Ellipsis b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ellipsis a -> f (Ellipsis b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ellipsis a -> f (Ellipsis b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Ellipsis (f a) -> f (Ellipsis a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Ellipsis (f a) -> f (Ellipsis a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ellipsis a -> m (Ellipsis b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ellipsis a -> m (Ellipsis b)
$csequence :: forall (m :: * -> *) a. Monad m => Ellipsis (m a) -> m (Ellipsis a)
sequence :: forall (m :: * -> *) a. Monad m => Ellipsis (m a) -> m (Ellipsis a)
Traversable, Show (Ellipsis t)
Show (Ellipsis t) =>
(AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t))
-> (AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t)
-> (AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t)
-> (Ellipsis t -> DisjointSet AnyName)
-> (Ellipsis t -> All)
-> (Ellipsis t -> Bool)
-> (Ellipsis t -> NthPatFind)
-> (Ellipsis t -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx
    -> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName))
-> (AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering)
-> Alpha (Ellipsis t)
AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t
AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t
AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool
AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering
Ellipsis t -> Bool
Ellipsis t -> All
Ellipsis t -> NamePatFind
Ellipsis t -> NthPatFind
Ellipsis t -> 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 t. Alpha t => Show (Ellipsis t)
forall t.
Alpha t =>
AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t
forall t.
Alpha t =>
AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
forall t.
Alpha t =>
AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t
forall t. Alpha t => AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool
forall t.
Alpha t =>
AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering
forall t. Alpha t => Ellipsis t -> Bool
forall t. Alpha t => Ellipsis t -> All
forall t. Alpha t => Ellipsis t -> NamePatFind
forall t. Alpha t => Ellipsis t -> NthPatFind
forall t. Alpha t => Ellipsis t -> DisjointSet AnyName
forall t (f :: * -> *).
(Alpha t, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t)
forall t (m :: * -> *).
(Alpha t, Fresh m) =>
AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName)
forall t (m :: * -> *) b.
(Alpha t, LFresh m) =>
AlphaCtx
-> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t)
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b
$caeq' :: forall t. Alpha t => AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool
aeq' :: AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool
$cfvAny' :: forall t (f :: * -> *).
(Alpha t, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t)
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t)
$cclose :: forall t.
Alpha t =>
AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
close :: AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
$copen :: forall t.
Alpha t =>
AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t
open :: AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t
$cisPat :: forall t. Alpha t => Ellipsis t -> DisjointSet AnyName
isPat :: Ellipsis t -> DisjointSet AnyName
$cisTerm :: forall t. Alpha t => Ellipsis t -> All
isTerm :: Ellipsis t -> All
$cisEmbed :: forall t. Alpha t => Ellipsis t -> Bool
isEmbed :: Ellipsis t -> Bool
$cnthPatFind :: forall t. Alpha t => Ellipsis t -> NthPatFind
nthPatFind :: Ellipsis t -> NthPatFind
$cnamePatFind :: forall t. Alpha t => Ellipsis t -> NamePatFind
namePatFind :: Ellipsis t -> NamePatFind
$cswaps' :: forall t.
Alpha t =>
AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t
swaps' :: AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t
$clfreshen' :: forall t (m :: * -> *) b.
(Alpha t, LFresh m) =>
AlphaCtx
-> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall t (m :: * -> *).
(Alpha t, Fresh m) =>
AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName)
$cacompare' :: forall t.
Alpha t =>
AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering
acompare' :: AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering
Alpha, Subst a, Typeable (Ellipsis t)
Typeable (Ellipsis t) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Ellipsis t))
-> (Ellipsis t -> Constr)
-> (Ellipsis t -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Ellipsis t)))
-> ((forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r)
-> (forall u. (forall d. Data d => d -> u) -> Ellipsis t -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Ellipsis t -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t))
-> Data (Ellipsis t)
Ellipsis t -> Constr
Ellipsis t -> DataType
(forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t
forall t. Data t => Typeable (Ellipsis t)
forall t. Data t => Ellipsis t -> Constr
forall t. Data t => Ellipsis t -> DataType
forall t.
Data t =>
(forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Ellipsis t -> u
forall t u.
Data t =>
(forall d. Data d => d -> u) -> Ellipsis t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ellipsis t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ellipsis t))
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) -> Ellipsis t -> u
forall u. (forall d. Data d => d -> u) -> Ellipsis t -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ellipsis t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ellipsis t))
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ellipsis t)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ellipsis t)
$ctoConstr :: forall t. Data t => Ellipsis t -> Constr
toConstr :: Ellipsis t -> Constr
$cdataTypeOf :: forall t. Data t => Ellipsis t -> DataType
dataTypeOf :: Ellipsis t -> DataType
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ellipsis t))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ellipsis t))
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t
gmapT :: (forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> Ellipsis t -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Ellipsis t -> [u]
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> Ellipsis t -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ellipsis t -> u
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
Data)

------------------------------------------------------------
-- Terms
------------------------------------------------------------

type family X_TVar e
type family X_TPrim e
type family X_TLet e
type family X_TParens e
type family X_TUnit e
type family X_TBool e
type family X_TNat e
type family X_TRat e
type family X_TChar e
type family X_TString e
type family X_TAbs e
type family X_TApp e
type family X_TTup e
type family X_TCase e
type family X_TChain e
type family X_TTyOp e
type family X_TContainer e
type family X_TContainerComp e
type family X_TAscr e
type family X_Term e

-- | The base generic AST representing terms in the disco language.
--   @e@ is a type index indicating the kind of term, i.e. the phase
--   (for example, surface, typed, or desugared).  Type families like
--   'X_TVar' and so on use the phase index to determine what extra
--   information (if any) should be stored in each constructor.  For
--   example, in the typed phase many constructors store an extra
--   type, giving the type of the term.
data Term_ e where
  -- | A term variable.
  TVar_ :: X_TVar e -> Name (Term_ e) -> Term_ e
  -- | A primitive, /i.e./ a constant  which is interpreted specially
  --   at runtime.  See "Disco.Syntax.Prims".
  TPrim_ :: X_TPrim e -> Prim -> Term_ e
  -- | A (non-recursive) let expression, @let x1 = t1, x2 = t2, ... in t@.
  TLet_ :: X_TLet e -> Bind (Telescope (Binding_ e)) (Term_ e) -> Term_ e
  -- | Explicit parentheses.  We need to keep track of these in the
  --   surface syntax in order to syntactically distinguish
  --   multiplication and function application.  However, note that
  --   these disappear after the surface syntax phase.
  TParens_ :: X_TParens e -> Term_ e -> Term_ e
  -- | The unit value, (), of type Unit.
  TUnit_ :: X_TUnit e -> Term_ e
  -- | A boolean value.
  TBool_ :: X_TBool e -> Bool -> Term_ e
  -- | A natural number.
  TNat_ :: X_TNat e -> Integer -> Term_ e
  -- | A nonnegative rational number, parsed as a decimal.  (Note
  --   syntax like @3/5@ does not parse as a rational, but rather as
  --   the application of a division operator to two natural numbers.)
  TRat_ :: X_TRat e -> Rational -> Term_ e
  -- | A literal unicode character, /e.g./ @'d'@.
  TChar_ :: X_TChar e -> Char -> Term_ e
  -- | A string literal, /e.g./ @"disco"@.
  TString_ :: X_TString e -> [Char] -> Term_ e
  -- | A binding abstraction, of the form @Q vars. expr@ where @Q@ is
  --   a quantifier and @vars@ is a list of bound variables and
  --   optional type annotations.  In particular, this could be a
  --   lambda abstraction, /i.e./ an anonymous function (/e.g./ @\x,
  --   (y:N). 2x + y@), a universal quantifier (@forall x, (y:N). x^2 +
  --   y > 0@), or an existential quantifier (@exists x, (y:N). x^2 + y
  --   == 0@).
  TAbs_ :: Quantifier -> X_TAbs e -> Binder_ e (Term_ e) -> Term_ e
  -- | Function application, @t1 t2@.
  TApp_ :: X_TApp e -> Term_ e -> Term_ e -> Term_ e
  -- | An n-tuple, @(t1, ..., tn)@.
  TTup_ :: X_TTup e -> [Term_ e] -> Term_ e
  -- | A case expression.
  TCase_ :: X_TCase e -> [Branch_ e] -> Term_ e
  -- | A chained comparison, consisting of a term followed by one or
  --   more "links", where each link is a comparison operator and
  --   another term.
  TChain_ :: X_TChain e -> Term_ e -> [Link_ e] -> Term_ e
  -- | An application of a type operator.
  TTyOp_ :: X_TTyOp e -> TyOp -> Type -> Term_ e
  -- | A containter literal (set, bag, or list).
  TContainer_ :: X_TContainer e -> Container -> [(Term_ e, Maybe (Term_ e))] -> Maybe (Ellipsis (Term_ e)) -> Term_ e
  -- | A container comprehension.
  TContainerComp_ :: X_TContainerComp e -> Container -> Bind (Telescope (Qual_ e)) (Term_ e) -> Term_ e
  -- | Type ascription, @(Term_ e : type)@.
  TAscr_ :: X_TAscr e -> Term_ e -> PolyType -> Term_ e
  -- | A data constructor with an extension descriptor that a "concrete"
  --   implementation of a generic AST may use to carry extra information.
  XTerm_ :: X_Term e -> Term_ e
  deriving ((forall x. Term_ e -> Rep (Term_ e) x)
-> (forall x. Rep (Term_ e) x -> Term_ e) -> Generic (Term_ e)
forall x. Rep (Term_ e) x -> Term_ e
forall x. Term_ e -> Rep (Term_ e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Term_ e) x -> Term_ e
forall e x. Term_ e -> Rep (Term_ e) x
$cfrom :: forall e x. Term_ e -> Rep (Term_ e) x
from :: forall x. Term_ e -> Rep (Term_ e) x
$cto :: forall e x. Rep (Term_ e) x -> Term_ e
to :: forall x. Rep (Term_ e) x -> Term_ e
Generic)

-- A type that abstracts over constraints for generic data constructors.
-- This makes it easier to derive typeclass instances for generic types.
type ForallTerm (a :: * -> Constraint) e =
  ( a (X_TVar e)
  , a (X_TPrim e)
  , a (X_TLet e)
  , a (X_TParens e)
  , a (X_TUnit e)
  , a (X_TBool e)
  , a (X_TNat e)
  , a (X_TRat e)
  , a (X_TChar e)
  , a (X_TString e)
  , a (X_TAbs e)
  , a (X_TApp e)
  , a (X_TCase e)
  , a (X_TTup e)
  , a (X_TChain e)
  , a (X_TTyOp e)
  , a (X_TContainer e)
  , a (X_TContainerComp e)
  , a (X_TAscr e)
  , a (X_Term e)
  , a (Qual_ e)
  , a (Guard_ e)
  , a (Link_ e)
  , a (Binding_ e)
  , a (Pattern_ e)
  , a (Binder_ e (Term_ e))
  )

deriving instance ForallTerm Show e => Show (Term_ e)
instance
  ( Typeable e
  , ForallTerm (Subst Type) e
  , ForallTerm Alpha e
  ) =>
  Subst Type (Term_ e)
instance (Typeable e, ForallTerm Alpha e) => Alpha (Term_ e)
deriving instance (Data e, Typeable e, ForallTerm Data e) => Data (Term_ e)

instance (Data e, ForallTerm Data e) => Plated (Term_ e) where
  plate :: Traversal' (Term_ e) (Term_ e)
plate = (Term_ e -> f (Term_ e)) -> Term_ e -> f (Term_ e)
forall a. Data a => Traversal' a a
Traversal' (Term_ e) (Term_ e)
uniplate

------------------------------------------------------------
-- Link
------------------------------------------------------------

type family X_TLink e

-- | A "link" is a comparison operator and a term; a single term
--   followed by a sequence of links makes up a comparison chain, such
--   as @2 < x < y < 10@.
data Link_ e where
  -- | Note that although the type of 'TLink_' says it can hold any
  --   'BOp', it should really only hold comparison operators.
  TLink_ :: X_TLink e -> BOp -> Term_ e -> Link_ e
  deriving ((forall x. Link_ e -> Rep (Link_ e) x)
-> (forall x. Rep (Link_ e) x -> Link_ e) -> Generic (Link_ e)
forall x. Rep (Link_ e) x -> Link_ e
forall x. Link_ e -> Rep (Link_ e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Link_ e) x -> Link_ e
forall e x. Link_ e -> Rep (Link_ e) x
$cfrom :: forall e x. Link_ e -> Rep (Link_ e) x
from :: forall x. Link_ e -> Rep (Link_ e) x
$cto :: forall e x. Rep (Link_ e) x -> Link_ e
to :: forall x. Rep (Link_ e) x -> Link_ e
Generic)

type ForallLink (a :: * -> Constraint) e =
  ( a (X_TLink e)
  , a (Term_ e)
  )

deriving instance ForallLink Show e => Show (Link_ e)
instance ForallLink (Subst Type) e => Subst Type (Link_ e)
instance (Typeable e, Show (Link_ e), ForallLink Alpha e) => Alpha (Link_ e)
deriving instance (Typeable e, Data e, ForallLink Data e) => Data (Link_ e)

------------------------------------------------------------
-- Qual
------------------------------------------------------------

type family X_QBind e
type family X_QGuard e

-- | A container comprehension consists of a head term and then a list
--   of qualifiers. Each qualifier either binds a variable to some
--   collection or consists of a boolean guard.
data Qual_ e where
  -- | A binding qualifier (i.e. @x in t@).
  QBind_ :: X_QBind e -> Name (Term_ e) -> Embed (Term_ e) -> Qual_ e
  -- | A boolean guard qualfier (i.e. @x + y > 4@).
  QGuard_ :: X_QGuard e -> Embed (Term_ e) -> Qual_ e
  deriving ((forall x. Qual_ e -> Rep (Qual_ e) x)
-> (forall x. Rep (Qual_ e) x -> Qual_ e) -> Generic (Qual_ e)
forall x. Rep (Qual_ e) x -> Qual_ e
forall x. Qual_ e -> Rep (Qual_ e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Qual_ e) x -> Qual_ e
forall e x. Qual_ e -> Rep (Qual_ e) x
$cfrom :: forall e x. Qual_ e -> Rep (Qual_ e) x
from :: forall x. Qual_ e -> Rep (Qual_ e) x
$cto :: forall e x. Rep (Qual_ e) x -> Qual_ e
to :: forall x. Rep (Qual_ e) x -> Qual_ e
Generic)

type ForallQual (a :: * -> Constraint) e =
  ( a (X_QBind e)
  , a (X_QGuard e)
  , a (Term_ e)
  )

deriving instance ForallQual Show e => Show (Qual_ e)
instance ForallQual (Subst Type) e => Subst Type (Qual_ e)
instance (Typeable e, ForallQual Alpha e) => Alpha (Qual_ e)
deriving instance (Typeable e, Data e, ForallQual Data e) => Data (Qual_ e)

------------------------------------------------------------
-- Binding
------------------------------------------------------------

-- | A binding is a name along with its definition, and optionally its
--   type.
data Binding_ e = Binding_ (Maybe (Embed PolyType)) (Name (Term_ e)) (Embed (Term_ e))
  deriving ((forall x. Binding_ e -> Rep (Binding_ e) x)
-> (forall x. Rep (Binding_ e) x -> Binding_ e)
-> Generic (Binding_ e)
forall x. Rep (Binding_ e) x -> Binding_ e
forall x. Binding_ e -> Rep (Binding_ e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Binding_ e) x -> Binding_ e
forall e x. Binding_ e -> Rep (Binding_ e) x
$cfrom :: forall e x. Binding_ e -> Rep (Binding_ e) x
from :: forall x. Binding_ e -> Rep (Binding_ e) x
$cto :: forall e x. Rep (Binding_ e) x -> Binding_ e
to :: forall x. Rep (Binding_ e) x -> Binding_ e
Generic)

deriving instance ForallTerm Show e => Show (Binding_ e)
instance Subst Type (Term_ e) => Subst Type (Binding_ e)
instance (Typeable e, Show (Binding_ e), Alpha (Term_ e)) => Alpha (Binding_ e)
deriving instance (Typeable e, Data e, ForallTerm Data e) => Data (Binding_ e)

------------------------------------------------------------
-- Branch
------------------------------------------------------------

-- | A branch of a case is a list of guards with an accompanying term.
--   The guards scope over the term.  Additionally, each guard scopes
--   over subsequent guards.
type Branch_ e = Bind (Telescope (Guard_ e)) (Term_ e)

------------------------------------------------------------
-- Guard
------------------------------------------------------------

type family X_GBool e
type family X_GPat e
type family X_GLet e

-- | Guards in case expressions.
data Guard_ e where
  -- | Boolean guard (@if <test>@)
  GBool_ :: X_GBool e -> Embed (Term_ e) -> Guard_ e
  -- | Pattern guard (@when term = pat@)
  GPat_ :: X_GPat e -> Embed (Term_ e) -> Pattern_ e -> Guard_ e
  -- | Let (@let x = term@)
  GLet_ :: X_GLet e -> Binding_ e -> Guard_ e
  deriving ((forall x. Guard_ e -> Rep (Guard_ e) x)
-> (forall x. Rep (Guard_ e) x -> Guard_ e) -> Generic (Guard_ e)
forall x. Rep (Guard_ e) x -> Guard_ e
forall x. Guard_ e -> Rep (Guard_ e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Guard_ e) x -> Guard_ e
forall e x. Guard_ e -> Rep (Guard_ e) x
$cfrom :: forall e x. Guard_ e -> Rep (Guard_ e) x
from :: forall x. Guard_ e -> Rep (Guard_ e) x
$cto :: forall e x. Rep (Guard_ e) x -> Guard_ e
to :: forall x. Rep (Guard_ e) x -> Guard_ e
Generic)

type ForallGuard (a :: * -> Constraint) e =
  ( a (X_GBool e)
  , a (X_GPat e)
  , a (X_GLet e)
  , a (Term_ e)
  , a (Pattern_ e)
  , a (Binding_ e)
  )

deriving instance ForallGuard Show e => Show (Guard_ e)
instance ForallGuard (Subst Type) e => Subst Type (Guard_ e)
instance (Typeable e, Show (Guard_ e), ForallGuard Alpha e) => Alpha (Guard_ e)
deriving instance (Typeable e, Data e, ForallGuard Data e) => Data (Guard_ e)

------------------------------------------------------------
-- Pattern
------------------------------------------------------------

type family X_PVar e
type family X_PWild e
type family X_PAscr e
type family X_PUnit e
type family X_PBool e
type family X_PTup e
type family X_PInj e
type family X_PNat e
type family X_PChar e
type family X_PString e
type family X_PCons e
type family X_PList e
type family X_PAdd e
type family X_PMul e
type family X_PSub e
type family X_PNeg e
type family X_PFrac e
type family X_Pattern e

-- | Patterns.
data Pattern_ e where
  -- | Variable pattern: matches anything and binds the variable.
  PVar_ :: X_PVar e -> Name (Term_ e) -> Pattern_ e
  -- | Wildcard pattern @_@: matches anything.
  PWild_ :: X_PWild e -> Pattern_ e
  -- | Type ascription pattern @pat : ty@.
  PAscr_ :: X_PAscr e -> Pattern_ e -> Type -> Pattern_ e
  -- | Unit pattern @()@: matches @()@.
  PUnit_ :: X_PUnit e -> Pattern_ e
  -- | Literal boolean pattern.
  PBool_ :: X_PBool e -> Bool -> Pattern_ e
  -- | Tuple pattern @(pat1, .. , patn)@.
  PTup_ :: X_PTup e -> [Pattern_ e] -> Pattern_ e
  -- | Injection pattern (@inl pat@ or @inr pat@).
  PInj_ :: X_PInj e -> Side -> Pattern_ e -> Pattern_ e
  -- | Literal natural number pattern.
  PNat_ :: X_PNat e -> Integer -> Pattern_ e
  -- | Unicode character pattern
  PChar_ :: X_PChar e -> Char -> Pattern_ e
  -- | String pattern.
  PString_ :: X_PString e -> String -> Pattern_ e
  -- | Cons pattern @p1 :: p2@.
  PCons_ :: X_PCons e -> Pattern_ e -> Pattern_ e -> Pattern_ e
  -- | List pattern @[p1, .., pn]@.
  PList_ :: X_PList e -> [Pattern_ e] -> Pattern_ e
  -- | Addition pattern, @p + t@ or @t + p@
  PAdd_ :: X_PAdd e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e
  -- | Multiplication pattern, @p * t@ or @t * p@
  PMul_ :: X_PMul e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e
  -- | Subtraction pattern, @p - t@
  PSub_ :: X_PSub e -> Pattern_ e -> Term_ e -> Pattern_ e
  -- | Negation pattern, @-p@
  PNeg_ :: X_PNeg e -> Pattern_ e -> Pattern_ e
  -- | Fraction pattern, @p1/p2@
  PFrac_ :: X_PFrac e -> Pattern_ e -> Pattern_ e -> Pattern_ e
  -- | A special placeholder node for a nonlinear occurrence of a
  --   variable; we can only detect this at parse time but need to
  --   generate an error later.
  PNonlinear_ :: Embed (Pattern_ e) -> Name (Term_ e) -> Pattern_ e
  -- | Expansion slot.
  XPattern_ :: X_Pattern e -> Pattern_ e
  deriving ((forall x. Pattern_ e -> Rep (Pattern_ e) x)
-> (forall x. Rep (Pattern_ e) x -> Pattern_ e)
-> Generic (Pattern_ e)
forall x. Rep (Pattern_ e) x -> Pattern_ e
forall x. Pattern_ e -> Rep (Pattern_ e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Pattern_ e) x -> Pattern_ e
forall e x. Pattern_ e -> Rep (Pattern_ e) x
$cfrom :: forall e x. Pattern_ e -> Rep (Pattern_ e) x
from :: forall x. Pattern_ e -> Rep (Pattern_ e) x
$cto :: forall e x. Rep (Pattern_ e) x -> Pattern_ e
to :: forall x. Rep (Pattern_ e) x -> Pattern_ e
Generic)

type ForallPattern (a :: * -> Constraint) e =
  ( a (X_PVar e)
  , a (X_PWild e)
  , a (X_PAscr e)
  , a (X_PUnit e)
  , a (X_PBool e)
  , a (X_PNat e)
  , a (X_PChar e)
  , a (X_PString e)
  , a (X_PTup e)
  , a (X_PInj e)
  , a (X_PCons e)
  , a (X_PList e)
  , a (X_PAdd e)
  , a (X_PMul e)
  , a (X_PSub e)
  , a (X_PNeg e)
  , a (X_PFrac e)
  , a (X_Pattern e)
  , a (Term_ e)
  )

deriving instance ForallPattern Show e => Show (Pattern_ e)
instance ForallPattern (Subst Type) e => Subst Type (Pattern_ e)
instance (Typeable e, Show (Pattern_ e), ForallPattern Alpha e) => Alpha (Pattern_ e)
deriving instance (Typeable e, Data e, ForallPattern Data e) => Data (Pattern_ e)

------------------------------------------------------------
-- Quantifiers and binders
------------------------------------------------------------

-- | A type family specifying what the binder in an abstraction can be.
--   Should have at least variables in it, but how many variables and
--   what other information is carried along may vary.
type family X_Binder e

-- | A binder represents the stuff between the quantifier and the body
--   of a lambda, ∀, or ∃ abstraction, as in @x : N, r : F@.
type Binder_ e a = Bind (X_Binder e) a

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

------------------------------------------------------------
-- Property
------------------------------------------------------------

-- | A property is just a term (of type Prop).
type Property_ e = Term_ e

------------------------------------------------------------
-- Orphan instances
------------------------------------------------------------

-- Need this if we want to put 'Void' as the type
-- of an extension slot (to kill a constructor)
instance Alpha Void