{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE DeriveTraversable    #-}
{-# LANGUAGE OverloadedStrings    #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE UndecidableInstances #-}

-- Orphan Alpha Void instance
{-# OPTIONS_GHC -fno-warn-orphans #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Disco.AST.Generic
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- 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".
-----------------------------------------------------------------------------

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

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
showList :: [Telescope b] -> ShowS
$cshowList :: forall b. Show b => [Telescope b] -> ShowS
show :: Telescope b -> String
$cshow :: forall b. Show b => Telescope b -> String
showsPrec :: Int -> Telescope b -> ShowS
$cshowsPrec :: forall b. Show b => Int -> 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
$cto :: forall b x. Rep (Telescope b) x -> Telescope b
$cfrom :: forall b x. Telescope b -> Rep (Telescope b) x
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 -> NthPatFind -> Telescope b -> Telescope b
AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b
AlphaCtx -> Telescope b -> Telescope b -> Bool
AlphaCtx -> Telescope b -> Telescope b -> Ordering
Telescope b -> Bool
Telescope b -> All
Telescope b -> DisjointSet AnyName
Telescope b -> NthPatFind
Telescope b -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall b. Alpha b => Show (Telescope b)
forall b.
Alpha b =>
AlphaCtx -> NthPatFind -> Telescope b -> Telescope b
forall b.
Alpha b =>
AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
forall b.
Alpha b =>
AlphaCtx -> Perm AnyName -> 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 -> DisjointSet AnyName
forall b. Alpha b => Telescope b -> NthPatFind
forall b. Alpha b => Telescope b -> NamePatFind
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
acompare' :: AlphaCtx -> Telescope b -> Telescope b -> Ordering
$cacompare' :: forall b.
Alpha b =>
AlphaCtx -> Telescope b -> Telescope b -> Ordering
freshen' :: AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName)
$cfreshen' :: forall b (m :: * -> *).
(Alpha b, Fresh m) =>
AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName)
lfreshen' :: AlphaCtx
-> Telescope b -> (Telescope b -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall b (m :: * -> *) b.
(Alpha b, LFresh m) =>
AlphaCtx
-> Telescope b -> (Telescope b -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b
$cswaps' :: forall b.
Alpha b =>
AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b
namePatFind :: Telescope b -> NamePatFind
$cnamePatFind :: forall b. Alpha b => Telescope b -> NamePatFind
nthPatFind :: Telescope b -> NthPatFind
$cnthPatFind :: forall b. Alpha b => Telescope b -> NthPatFind
isEmbed :: Telescope b -> Bool
$cisEmbed :: forall b. Alpha b => Telescope b -> Bool
isTerm :: Telescope b -> All
$cisTerm :: forall b. Alpha b => Telescope b -> All
isPat :: Telescope b -> DisjointSet AnyName
$cisPat :: forall b. Alpha b => Telescope b -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Telescope b -> Telescope b
$copen :: forall b.
Alpha b =>
AlphaCtx -> NthPatFind -> Telescope b -> Telescope b
close :: AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
$cclose :: forall b.
Alpha b =>
AlphaCtx -> NamePatFind -> Telescope b -> Telescope b
fvAny' :: AlphaCtx
-> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b)
$cfvAny' :: forall b (f :: * -> *).
(Alpha b, Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b)
aeq' :: AlphaCtx -> Telescope b -> Telescope b -> Bool
$caeq' :: forall b. Alpha b => AlphaCtx -> Telescope b -> Telescope b -> Bool
$cp1Alpha :: forall b. Alpha b => Show (Telescope b)
Alpha, Subst t, Typeable (Telescope b)
DataType
Constr
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 -> DataType
Telescope b -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
(forall b. Data b => b -> b) -> Telescope b -> Telescope b
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Telescope b -> c (Telescope b)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Telescope b)
forall b. Data b => Typeable (Telescope b)
forall b. Data b => Telescope b -> DataType
forall b. Data b => Telescope b -> Constr
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))
$cTelCons :: Constr
$cTelEmpty :: Constr
$tTelescope :: DataType
gmapMo :: (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)
gmapMp :: (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)
gmapM :: (forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
$cgmapM :: forall b (m :: * -> *).
(Data b, Monad m) =>
(forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)
gmapQi :: Int -> (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
gmapQ :: (forall d. Data d => d -> u) -> Telescope b -> [u]
$cgmapQ :: forall b u.
Data b =>
(forall d. Data d => d -> u) -> Telescope b -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
$cgmapQl :: forall b r r'.
Data b =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Telescope b -> r
gmapT :: (forall b. Data b => b -> b) -> Telescope b -> Telescope b
$cgmapT :: forall b.
Data b =>
(forall b. Data b => b -> b) -> Telescope b -> Telescope b
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> 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))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
$cdataCast1 :: forall b (t :: * -> *) (c :: * -> *).
(Data b, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Telescope b))
dataTypeOf :: Telescope b -> DataType
$cdataTypeOf :: forall b. Data b => Telescope b -> DataType
toConstr :: Telescope b -> Constr
$ctoConstr :: forall b. Data b => Telescope b -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> 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)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Telescope b -> 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)
$cp1Data :: forall b. Data b => Typeable (Telescope b)
Data)

-- | Add a new item to the beginning of a 'Telescope'.
telCons :: Alpha b => b -> Telescope b -> Telescope b
telCons :: 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 :: (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 :: (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 :: (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Telescope b)
ftb) (Telescope b -> f (Telescope b)
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 :: [b] -> Telescope b
toTelescope = (b -> Telescope b -> Telescope b)
-> Telescope b -> [b] -> Telescope 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 :: 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
showList :: [Side] -> ShowS
$cshowList :: [Side] -> ShowS
show :: Side -> String
$cshow :: Side -> String
showsPrec :: Int -> Side -> ShowS
$cshowsPrec :: Int -> Side -> ShowS
Show, Side -> Side -> Bool
(Side -> Side -> Bool) -> (Side -> Side -> Bool) -> Eq Side
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Side -> Side -> Bool
$c/= :: Side -> Side -> Bool
== :: Side -> Side -> Bool
$c== :: 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
min :: Side -> Side -> Side
$cmin :: Side -> Side -> Side
max :: Side -> Side -> Side
$cmax :: Side -> Side -> Side
>= :: Side -> Side -> Bool
$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
compare :: Side -> Side -> Ordering
$ccompare :: Side -> Side -> Ordering
$cp1Ord :: Eq 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
enumFromThenTo :: Side -> Side -> Side -> [Side]
$cenumFromThenTo :: Side -> Side -> Side -> [Side]
enumFromTo :: Side -> Side -> [Side]
$cenumFromTo :: Side -> Side -> [Side]
enumFromThen :: Side -> Side -> [Side]
$cenumFromThen :: Side -> Side -> [Side]
enumFrom :: Side -> [Side]
$cenumFrom :: Side -> [Side]
fromEnum :: Side -> Int
$cfromEnum :: Side -> Int
toEnum :: Int -> Side
$ctoEnum :: Int -> Side
pred :: Side -> Side
$cpred :: Side -> Side
succ :: Side -> Side
$csucc :: Side -> Side
Enum, Side
Side -> Side -> Bounded Side
forall a. a -> a -> Bounded a
maxBound :: Side
$cmaxBound :: Side
minBound :: Side
$cminBound :: 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
$cto :: forall x. Rep Side x -> Side
$cfrom :: forall x. Side -> Rep Side x
Generic, Typeable Side
DataType
Constr
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 -> DataType
Side -> Constr
(forall b. Data b => b -> b) -> Side -> Side
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Side -> c Side
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cR :: Constr
$cL :: Constr
$tSide :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> Side -> m Side
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Side -> m Side
gmapQi :: Int -> (forall d. Data d => d -> u) -> Side -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Side -> u
gmapQ :: (forall d. Data d => d -> u) -> Side -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Side -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r
gmapT :: (forall b. Data b => b -> b) -> Side -> Side
$cgmapT :: (forall b. Data b => b -> b) -> Side -> Side
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Side)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Side)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Side)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Side)
dataTypeOf :: Side -> DataType
$cdataTypeOf :: Side -> DataType
toConstr :: Side -> Constr
$ctoConstr :: Side -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Side
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Side
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Side -> c Side
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Side -> c Side
$cp1Data :: Typeable 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 -> NthPatFind -> Side -> Side
AlphaCtx -> NamePatFind -> Side -> Side
AlphaCtx -> Perm AnyName -> Side -> Side
AlphaCtx -> Side -> Side -> Bool
AlphaCtx -> Side -> Side -> Ordering
Side -> Bool
Side -> All
Side -> DisjointSet AnyName
Side -> NthPatFind
Side -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> 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
acompare' :: AlphaCtx -> Side -> Side -> Ordering
$cacompare' :: AlphaCtx -> Side -> Side -> Ordering
freshen' :: AlphaCtx -> Side -> m (Side, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Side -> m (Side, Perm AnyName)
lfreshen' :: AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Side -> Side
$cswaps' :: AlphaCtx -> Perm AnyName -> Side -> Side
namePatFind :: Side -> NamePatFind
$cnamePatFind :: Side -> NamePatFind
nthPatFind :: Side -> NthPatFind
$cnthPatFind :: Side -> NthPatFind
isEmbed :: Side -> Bool
$cisEmbed :: Side -> Bool
isTerm :: Side -> All
$cisTerm :: Side -> All
isPat :: Side -> DisjointSet AnyName
$cisPat :: Side -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Side -> Side
$copen :: AlphaCtx -> NthPatFind -> Side -> Side
close :: AlphaCtx -> NamePatFind -> Side -> Side
$cclose :: AlphaCtx -> NamePatFind -> Side -> Side
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Side -> f Side
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Side -> f Side
aeq' :: AlphaCtx -> Side -> Side -> Bool
$caeq' :: AlphaCtx -> Side -> Side -> Bool
$cp1Alpha :: Show Side
Alpha, Subst t)

instance Pretty Side where
  pretty :: Side -> Sem r Doc
pretty = \case
    Side
L -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"left"
    Side
R -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
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 :: 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
showList :: [Container] -> ShowS
$cshowList :: [Container] -> ShowS
show :: Container -> String
$cshow :: Container -> String
showsPrec :: Int -> Container -> ShowS
$cshowsPrec :: Int -> Container -> ShowS
Show, Container -> Container -> Bool
(Container -> Container -> Bool)
-> (Container -> Container -> Bool) -> Eq Container
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Container -> Container -> Bool
$c/= :: Container -> Container -> Bool
== :: Container -> Container -> Bool
$c== :: 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
enumFromThenTo :: Container -> Container -> Container -> [Container]
$cenumFromThenTo :: Container -> Container -> Container -> [Container]
enumFromTo :: Container -> Container -> [Container]
$cenumFromTo :: Container -> Container -> [Container]
enumFromThen :: Container -> Container -> [Container]
$cenumFromThen :: Container -> Container -> [Container]
enumFrom :: Container -> [Container]
$cenumFrom :: Container -> [Container]
fromEnum :: Container -> Int
$cfromEnum :: Container -> Int
toEnum :: Int -> Container
$ctoEnum :: Int -> Container
pred :: Container -> Container
$cpred :: Container -> Container
succ :: Container -> Container
$csucc :: 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
$cto :: forall x. Rep Container x -> Container
$cfrom :: forall x. Container -> Rep Container x
Generic, Typeable Container
DataType
Constr
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 -> DataType
Container -> Constr
(forall b. Data b => b -> b) -> Container -> Container
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Container -> c Container
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cSetContainer :: Constr
$cBagContainer :: Constr
$cListContainer :: Constr
$tContainer :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> Container -> m Container
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Container -> m Container
gmapQi :: Int -> (forall d. Data d => d -> u) -> Container -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Container -> u
gmapQ :: (forall d. Data d => d -> u) -> Container -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Container -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Container -> r
gmapT :: (forall b. Data b => b -> b) -> Container -> Container
$cgmapT :: (forall b. Data b => b -> b) -> Container -> Container
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Container)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Container)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Container)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Container)
dataTypeOf :: Container -> DataType
$cdataTypeOf :: Container -> DataType
toConstr :: Container -> Constr
$ctoConstr :: Container -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Container
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Container
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Container -> c Container
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Container -> c Container
$cp1Data :: Typeable 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 -> NthPatFind -> Container -> Container
AlphaCtx -> NamePatFind -> Container -> Container
AlphaCtx -> Perm AnyName -> Container -> Container
AlphaCtx -> Container -> Container -> Bool
AlphaCtx -> Container -> Container -> Ordering
Container -> Bool
Container -> All
Container -> DisjointSet AnyName
Container -> NthPatFind
Container -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> 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
acompare' :: AlphaCtx -> Container -> Container -> Ordering
$cacompare' :: AlphaCtx -> Container -> Container -> Ordering
freshen' :: AlphaCtx -> Container -> m (Container, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Container -> m (Container, Perm AnyName)
lfreshen' :: AlphaCtx -> Container -> (Container -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Container -> (Container -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Container -> Container
$cswaps' :: AlphaCtx -> Perm AnyName -> Container -> Container
namePatFind :: Container -> NamePatFind
$cnamePatFind :: Container -> NamePatFind
nthPatFind :: Container -> NthPatFind
$cnthPatFind :: Container -> NthPatFind
isEmbed :: Container -> Bool
$cisEmbed :: Container -> Bool
isTerm :: Container -> All
$cisTerm :: Container -> All
isPat :: Container -> DisjointSet AnyName
$cisPat :: Container -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Container -> Container
$copen :: AlphaCtx -> NthPatFind -> Container -> Container
close :: AlphaCtx -> NamePatFind -> Container -> Container
$cclose :: AlphaCtx -> NamePatFind -> Container -> Container
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Container -> f Container
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Container -> f Container
aeq' :: AlphaCtx -> Container -> Container -> Bool
$caeq' :: AlphaCtx -> Container -> Container -> Bool
$cp1Alpha :: Show Container
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
showList :: [Ellipsis t] -> ShowS
$cshowList :: forall t. Show t => [Ellipsis t] -> ShowS
show :: Ellipsis t -> String
$cshow :: forall t. Show t => Ellipsis t -> String
showsPrec :: Int -> Ellipsis t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> 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
$cto :: forall t x. Rep (Ellipsis t) x -> Ellipsis t
$cfrom :: forall t x. Ellipsis t -> Rep (Ellipsis t) x
Generic, a -> Ellipsis b -> Ellipsis a
(a -> b) -> Ellipsis a -> Ellipsis b
(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
<$ :: a -> Ellipsis b -> Ellipsis a
$c<$ :: forall a b. a -> Ellipsis b -> Ellipsis a
fmap :: (a -> b) -> Ellipsis a -> Ellipsis b
$cfmap :: forall a b. (a -> b) -> Ellipsis a -> Ellipsis b
Functor, Ellipsis a -> Bool
(a -> m) -> Ellipsis a -> m
(a -> b -> b) -> b -> Ellipsis a -> b
(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
product :: Ellipsis a -> a
$cproduct :: forall a. Num a => Ellipsis a -> a
sum :: Ellipsis a -> a
$csum :: forall a. Num a => Ellipsis a -> a
minimum :: Ellipsis a -> a
$cminimum :: forall a. Ord a => Ellipsis a -> a
maximum :: Ellipsis a -> a
$cmaximum :: forall a. Ord a => Ellipsis a -> a
elem :: a -> Ellipsis a -> Bool
$celem :: forall a. Eq a => a -> Ellipsis a -> Bool
length :: Ellipsis a -> Int
$clength :: forall a. Ellipsis a -> Int
null :: Ellipsis a -> Bool
$cnull :: forall a. Ellipsis a -> Bool
toList :: Ellipsis a -> [a]
$ctoList :: forall a. Ellipsis a -> [a]
foldl1 :: (a -> a -> a) -> Ellipsis a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
foldr1 :: (a -> a -> a) -> Ellipsis a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Ellipsis a -> a
foldl' :: (b -> a -> b) -> b -> Ellipsis a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
foldl :: (b -> a -> b) -> b -> Ellipsis a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Ellipsis a -> b
foldr' :: (a -> b -> b) -> b -> Ellipsis a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
foldr :: (a -> b -> b) -> b -> Ellipsis a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Ellipsis a -> b
foldMap' :: (a -> m) -> Ellipsis a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
foldMap :: (a -> m) -> Ellipsis a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Ellipsis a -> m
fold :: Ellipsis m -> m
$cfold :: forall m. Monoid m => Ellipsis m -> m
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
(a -> f b) -> Ellipsis a -> f (Ellipsis b)
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)
sequence :: Ellipsis (m a) -> m (Ellipsis a)
$csequence :: forall (m :: * -> *) a. Monad m => Ellipsis (m a) -> m (Ellipsis a)
mapM :: (a -> m b) -> Ellipsis a -> m (Ellipsis b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ellipsis a -> m (Ellipsis b)
sequenceA :: Ellipsis (f a) -> f (Ellipsis a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Ellipsis (f a) -> f (Ellipsis a)
traverse :: (a -> f b) -> Ellipsis a -> f (Ellipsis b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ellipsis a -> f (Ellipsis b)
$cp2Traversable :: Foldable Ellipsis
$cp1Traversable :: Functor Ellipsis
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 -> NthPatFind -> Ellipsis t -> Ellipsis t
AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t
AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool
AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering
Ellipsis t -> Bool
Ellipsis t -> All
Ellipsis t -> DisjointSet AnyName
Ellipsis t -> NthPatFind
Ellipsis t -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall t. Alpha t => Show (Ellipsis t)
forall t.
Alpha t =>
AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t
forall t.
Alpha t =>
AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
forall t.
Alpha t =>
AlphaCtx -> Perm AnyName -> 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 -> DisjointSet AnyName
forall t. Alpha t => Ellipsis t -> NthPatFind
forall t. Alpha t => Ellipsis t -> NamePatFind
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
acompare' :: AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering
$cacompare' :: forall t.
Alpha t =>
AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering
freshen' :: AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName)
$cfreshen' :: forall t (m :: * -> *).
(Alpha t, Fresh m) =>
AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName)
lfreshen' :: AlphaCtx
-> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall t (m :: * -> *) b.
(Alpha t, LFresh m) =>
AlphaCtx
-> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t
$cswaps' :: forall t.
Alpha t =>
AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t
namePatFind :: Ellipsis t -> NamePatFind
$cnamePatFind :: forall t. Alpha t => Ellipsis t -> NamePatFind
nthPatFind :: Ellipsis t -> NthPatFind
$cnthPatFind :: forall t. Alpha t => Ellipsis t -> NthPatFind
isEmbed :: Ellipsis t -> Bool
$cisEmbed :: forall t. Alpha t => Ellipsis t -> Bool
isTerm :: Ellipsis t -> All
$cisTerm :: forall t. Alpha t => Ellipsis t -> All
isPat :: Ellipsis t -> DisjointSet AnyName
$cisPat :: forall t. Alpha t => Ellipsis t -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t
$copen :: forall t.
Alpha t =>
AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t
close :: AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
$cclose :: forall t.
Alpha t =>
AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t)
$cfvAny' :: forall t (f :: * -> *).
(Alpha t, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t)
aeq' :: AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool
$caeq' :: forall t. Alpha t => AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool
$cp1Alpha :: forall t. Alpha t => Show (Ellipsis t)
Alpha, Subst a, Typeable (Ellipsis t)
DataType
Constr
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 -> DataType
Ellipsis t -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
(forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ellipsis t)
forall t. Data t => Typeable (Ellipsis t)
forall t. Data t => Ellipsis t -> DataType
forall t. Data t => Ellipsis t -> Constr
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))
$cUntil :: Constr
$tEllipsis :: DataType
gmapMo :: (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)
gmapMp :: (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)
gmapM :: (forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)
gmapQi :: Int -> (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
gmapQ :: (forall d. Data d => d -> u) -> Ellipsis t -> [u]
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> Ellipsis t -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r
gmapT :: (forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> 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))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ellipsis t))
dataTypeOf :: Ellipsis t -> DataType
$cdataTypeOf :: forall t. Data t => Ellipsis t -> DataType
toConstr :: Ellipsis t -> Constr
$ctoConstr :: forall t. Data t => Ellipsis t -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> 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)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ellipsis t -> 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)
$cp1Data :: forall t. Data t => Typeable (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
$cto :: forall e x. Rep (Term_ e) x -> Term_ e
$cfrom :: forall e x. Term_ e -> Rep (Term_ e) x
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 :: (Term_ e -> f (Term_ e)) -> Term_ e -> f (Term_ e)
plate = (Term_ e -> f (Term_ e)) -> Term_ e -> f (Term_ e)
forall a. Data a => Traversal' a a
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
$cto :: forall e x. Rep (Link_ e) x -> Link_ e
$cfrom :: forall e x. Link_ e -> Rep (Link_ e) x
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
$cto :: forall e x. Rep (Qual_ e) x -> Qual_ e
$cfrom :: forall e x. Qual_ e -> Rep (Qual_ e) x
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
$cto :: forall e x. Rep (Binding_ e) x -> Binding_ e
$cfrom :: forall e x. Binding_ e -> Rep (Binding_ e) x
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
$cto :: forall e x. Rep (Guard_ e) x -> Guard_ e
$cfrom :: forall e x. Guard_ e -> Rep (Guard_ e) x
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

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