Safe Haskell	None
Language	Haskell2010

Language.SOAS.Impl.Generated

Contents

Generated code
User-defined helpers
Orphan instances

Synopsis

type ScopedOpArgTyping' a (n :: S) = ScopedOpArgTyping'Sig a (ScopedAST (TypeBinders' a) (Type'Sig a) n) (AST (TypeBinders' a) (Type'Sig a) n)
data ScopedOpArgTyping'Sig a scope term where
- ScopedOpArgTypingSig :: forall a scope term. a -> OpArgTyping'Sig a scope term -> ScopedOpArgTyping'Sig a scope term
type OpArgTyping' a (n :: S) = OpArgTyping'Sig a (ScopedAST (TypeBinders' a) (Type'Sig a) n) (AST (TypeBinders' a) (Type'Sig a) n)
data OpArgTyping'Sig a scope term where
- OpArgTypingSig :: forall a term scope. a -> [term] -> term -> OpArgTyping'Sig a scope term
type ScopedType' a = ScopedAST (TypeBinders' a) (Type'Sig a)
type Type' a = AST (TypeBinders' a) (Type'Sig a)
data Type'Sig a scope term where
- TypeFunSig :: forall a term scope. a -> term -> term -> Type'Sig a scope term
- TypeProductSig :: forall a term scope. a -> term -> term -> Type'Sig a scope term
type OpArg' a (n :: S) = OpArg'Sig a (ScopedAST (Binders' a) (Term'Sig a) n) (AST (Binders' a) (Term'Sig a) n)
data OpArg'Sig a scope term where
- OpArgSig :: forall a scope term. a -> scope -> OpArg'Sig a scope term
- PlainOpArgSig :: forall a term scope. a -> term -> OpArg'Sig a scope term
type ScopedTerm' a = ScopedAST (Binders' a) (Term'Sig a)
type Term' a = AST (Binders' a) (Term'Sig a)
data Term'Sig a scope term where
- OpSig :: forall a scope term. a -> OpIdent -> [OpArg'Sig a scope term] -> Term'Sig a scope term
- MetaVarSig :: forall a term scope. a -> MetaVarIdent -> [term] -> Term'Sig a scope term
data TypeBinders' a (o :: S) (i :: S) where
- NoTypeBinders :: forall a (o :: S). a -> TypeBinders' a o o
- SomeTypeBinders :: forall a (o :: S) (i1 :: S) (i :: S). a -> NameBinder o i1 -> TypeBinders' a i1 i -> TypeBinders' a o i
data Binders' a (o :: S) (i :: S) where
- NoBinders :: forall a (o :: S). a -> Binders' a o o
- SomeBinders :: forall a (o :: S) (i1 :: S) (i :: S). a -> NameBinder o i1 -> Binders' a i1 i -> Binders' a o i
data TermTyping' a (o :: S) where
- TermTyping :: forall a (o :: S) (i :: S). a -> TypeBinders' a o i -> Context' a -> Term' a i -> Type' a i -> TermTyping' a o
data VarTyping' a (o :: S) where
- VarTyping :: forall a (o :: S). a -> Name o -> Type' a o -> VarTyping' a o
data Constraint' a (o :: S) where
- ConstraintEq :: forall a (o :: S) (i :: S). a -> Binders' a o i -> Term' a i -> Term' a i -> Constraint' a o
data OpTyping' a (o :: S) where
- OpTyping :: forall a (o :: S) (i :: S). a -> OpIdent -> TypeBinders' a o i -> [ScopedOpArgTyping' a i] -> Type' a i -> OpTyping' a o
data MetaVarTyping' a (o :: S) where
- MetaVarTyping :: forall a (o :: S). a -> MetaVarIdent -> [Type' a o] -> Type' a o -> MetaVarTyping' a o
data Subst' a (o :: S) where
- Subst :: forall a (o :: S) (i :: S). a -> MetaVarIdent -> Binders' a o i -> Term' a i -> Subst' a o
pattern ScopedOpArgTyping :: forall a (o :: S). a -> OpArgTyping' a o -> ScopedOpArgTyping' a o
pattern OpArgTyping :: forall a (o :: S). a -> [Type' a o] -> Type' a o -> OpArgTyping' a o
pattern TypeProduct :: a -> Type' a o -> Type' a o -> Type' a o
pattern TypeFun :: a -> Type' a o -> Type' a o -> Type' a o
pattern PlainOpArg :: forall a (o :: S). a -> Term' a o -> OpArg' a o
pattern OpArg :: forall a (o :: S) (i :: S). () => a -> Binders' a o i -> Term' a i -> OpArg' a o
pattern MetaVar :: a -> MetaVarIdent -> [Term' a o] -> Term' a o
pattern Op :: a -> OpIdent -> [OpArg' a o] -> Term' a o
fromTerm'Sig :: Term'Sig a (Binders' a, ScopedTerm' a) (Term' a) -> Term' a
fromOpArg'Sig :: OpArg'Sig a (Binders' a, ScopedTerm' a) (Term' a) -> OpArg' a
fromBinders' :: forall a (o :: S) (i :: S). Binders' a o i -> Binders' a
fromOpArg' :: forall a (o :: S). OpArg' a o -> OpArg' a
fromTerm' :: forall a (o :: S). Term' a o -> Term' a
fromType'Sig :: Type'Sig a (TypeBinders' a, ScopedType' a) (Type' a) -> Type' a
fromOpArgTyping'Sig :: OpArgTyping'Sig a (TypeBinders' a, ScopedType' a) (Type' a) -> OpArgTyping' a
fromScopedOpArgTyping'Sig :: ScopedOpArgTyping'Sig a (TypeBinders' a, ScopedType' a) (Type' a) -> ScopedOpArgTyping' a
fromTypeBinders' :: forall a (o :: S) (i :: S). TypeBinders' a o i -> TypeBinders' a
fromOpArgTyping' :: forall a (o :: S). OpArgTyping' a o -> OpArgTyping' a
fromScopedOpArgTyping' :: forall a (i :: S). ScopedOpArgTyping' a i -> ScopedOpArgTyping' a
fromType' :: forall a (o :: S). Type' a o -> Type' a
fromSubst' :: forall a (o :: S). Subst' a o -> Subst' a
fromMetaVarTyping' :: forall a (o :: S). MetaVarTyping' a o -> MetaVarTyping' a
fromOpTyping' :: forall a (o :: S). OpTyping' a o -> OpTyping' a
fromConstraint' :: forall a (o :: S). Constraint' a o -> Constraint' a
fromVarTyping' :: forall a (o :: S). VarTyping' a o -> VarTyping' a
fromTermTyping' :: forall a (o :: S). TermTyping' a o -> TermTyping' a
toTerm'Sig :: Term' a -> Either VarIdent (Term'Sig a (Binders' a, ScopedTerm' a) (Term' a))
toOpArg'Sig :: OpArg' a -> OpArg'Sig a (Binders' a, ScopedTerm' a) (Term' a)
toBinders' :: forall (o :: S) a r. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> Binders' a -> (forall (i :: S). DExt o i => Binders' a o i -> Map VarIdent (Name i) -> r) -> r
toOpArg' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> OpArg' a -> OpArg' a o
toTerm' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> Term' a -> Term' a o
toType'Sig :: Type' a -> Either VarIdent (Type'Sig a (TypeBinders' a, ScopedType' a) (Type' a))
toOpArgTyping'Sig :: OpArgTyping' a -> OpArgTyping'Sig a (TypeBinders' a, ScopedType' a) (Type' a)
toScopedOpArgTyping'Sig :: ScopedOpArgTyping' a -> ScopedOpArgTyping'Sig a (TypeBinders' a, ScopedType' a) (Type' a)
toTypeBinders' :: forall (o :: S) a r. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> TypeBinders' a -> (forall (i :: S). DExt o i => TypeBinders' a o i -> Map VarIdent (Name i) -> r) -> r
toOpArgTyping' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> OpArgTyping' a -> OpArgTyping' a o
toScopedOpArgTyping' :: forall (i :: S) a. (Distinct i, Ord VarIdent) => Scope i -> Map VarIdent (Name i) -> ScopedOpArgTyping' a -> ScopedOpArgTyping' a i
toType' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> Type' a -> Type' a o
toSubst' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> Subst' a -> Subst' a o
toMetaVarTyping' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> MetaVarTyping' a -> MetaVarTyping' a o
toOpTyping' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> OpTyping' a -> OpTyping' a o
toConstraint' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> Constraint' a -> Constraint' a o
toVarTyping' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> VarTyping' a -> VarTyping' a o
toTermTyping' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> TermTyping' a -> TermTyping' a o
unsafeParse :: ([Token] -> Either String a) -> String -> a

Documentation

>>> :set -XOverloadedStrings
>>> :set -XDataKinds
>>> import qualified Control.Monad.Foil as Foil
>>> import qualified Language.SOAS.Syntax.Abs as Raw
>>> import Control.Monad.Free.Foil
>>> import Data.String (fromString)

Generated code

type ScopedOpArgTyping' a (n :: S) = ScopedOpArgTyping'Sig a (ScopedAST (TypeBinders' a) (Type'Sig a) n) (AST (TypeBinders' a) (Type'Sig a) n) Source #

Generated with mkFreeFoil. A scope-safe version of ScopedOpArgTyping'.

data ScopedOpArgTyping'Sig a scope term where Source #

Generated with mkFreeFoil. A signature based on ScopedOpArgTyping'.

Constructors

ScopedOpArgTypingSig :: forall a scope term. a -> OpArgTyping'Sig a scope term -> ScopedOpArgTyping'Sig a scope term

Corresponds to ScopedOpArgTyping.

Instances

Instances details

Bifoldable (ScopedOpArgTyping'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bifold :: Monoid m => ScopedOpArgTyping'Sig a m m -> m #

bifoldMap :: Monoid m => (a0 -> m) -> (b -> m) -> ScopedOpArgTyping'Sig a a0 b -> m #

bifoldr :: (a0 -> c -> c) -> (b -> c -> c) -> c -> ScopedOpArgTyping'Sig a a0 b -> c #

bifoldl :: (c -> a0 -> c) -> (c -> b -> c) -> c -> ScopedOpArgTyping'Sig a a0 b -> c #

Bifunctor (ScopedOpArgTyping'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bimap :: (a0 -> b) -> (c -> d) -> ScopedOpArgTyping'Sig a a0 c -> ScopedOpArgTyping'Sig a b d #

first :: (a0 -> b) -> ScopedOpArgTyping'Sig a a0 c -> ScopedOpArgTyping'Sig a b c #

second :: (b -> c) -> ScopedOpArgTyping'Sig a a0 b -> ScopedOpArgTyping'Sig a a0 c #

Bitraversable (ScopedOpArgTyping'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bitraverse :: Applicative f => (a0 -> f c) -> (b -> f d) -> ScopedOpArgTyping'Sig a a0 b -> f (ScopedOpArgTyping'Sig a c d) #

Foldable (ScopedOpArgTyping'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fold :: Monoid m => ScopedOpArgTyping'Sig a scope m -> m #

foldMap :: Monoid m => (a0 -> m) -> ScopedOpArgTyping'Sig a scope a0 -> m #

foldMap' :: Monoid m => (a0 -> m) -> ScopedOpArgTyping'Sig a scope a0 -> m #

foldr :: (a0 -> b -> b) -> b -> ScopedOpArgTyping'Sig a scope a0 -> b #

foldr' :: (a0 -> b -> b) -> b -> ScopedOpArgTyping'Sig a scope a0 -> b #

foldl :: (b -> a0 -> b) -> b -> ScopedOpArgTyping'Sig a scope a0 -> b #

foldl' :: (b -> a0 -> b) -> b -> ScopedOpArgTyping'Sig a scope a0 -> b #

foldr1 :: (a0 -> a0 -> a0) -> ScopedOpArgTyping'Sig a scope a0 -> a0 #

foldl1 :: (a0 -> a0 -> a0) -> ScopedOpArgTyping'Sig a scope a0 -> a0 #

toList :: ScopedOpArgTyping'Sig a scope a0 -> [a0] #

null :: ScopedOpArgTyping'Sig a scope a0 -> Bool #

length :: ScopedOpArgTyping'Sig a scope a0 -> Int #

elem :: Eq a0 => a0 -> ScopedOpArgTyping'Sig a scope a0 -> Bool #

maximum :: Ord a0 => ScopedOpArgTyping'Sig a scope a0 -> a0 #

minimum :: Ord a0 => ScopedOpArgTyping'Sig a scope a0 -> a0 #

sum :: Num a0 => ScopedOpArgTyping'Sig a scope a0 -> a0 #

product :: Num a0 => ScopedOpArgTyping'Sig a scope a0 -> a0 #

Traversable (ScopedOpArgTyping'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

traverse :: Applicative f => (a0 -> f b) -> ScopedOpArgTyping'Sig a scope a0 -> f (ScopedOpArgTyping'Sig a scope b) #

sequenceA :: Applicative f => ScopedOpArgTyping'Sig a scope (f a0) -> f (ScopedOpArgTyping'Sig a scope a0) #

mapM :: Monad m => (a0 -> m b) -> ScopedOpArgTyping'Sig a scope a0 -> m (ScopedOpArgTyping'Sig a scope b) #

sequence :: Monad m => ScopedOpArgTyping'Sig a scope (m a0) -> m (ScopedOpArgTyping'Sig a scope a0) #

Functor (ScopedOpArgTyping'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fmap :: (a0 -> b) -> ScopedOpArgTyping'Sig a scope a0 -> ScopedOpArgTyping'Sig a scope b #

(<$) :: a0 -> ScopedOpArgTyping'Sig a scope b -> ScopedOpArgTyping'Sig a scope a0 #

Generic (ScopedOpArgTyping'Sig a scope term) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type Rep (ScopedOpArgTyping'Sig a scope term)

Instance details

Defined in Language.SOAS.Impl.Generated

type Rep (ScopedOpArgTyping'Sig a scope term) = D1 ('MetaData "ScopedOpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "ScopedOpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (OpArgTyping'Sig a scope term))))

Methods

from :: ScopedOpArgTyping'Sig a scope term -> Rep (ScopedOpArgTyping'Sig a scope term) x #

to :: Rep (ScopedOpArgTyping'Sig a scope term) x -> ScopedOpArgTyping'Sig a scope term #

type Rep (ScopedOpArgTyping'Sig a scope term) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type Rep (ScopedOpArgTyping'Sig a scope term) = D1 ('MetaData "ScopedOpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "ScopedOpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (OpArgTyping'Sig a scope term))))

type OpArgTyping' a (n :: S) = OpArgTyping'Sig a (ScopedAST (TypeBinders' a) (Type'Sig a) n) (AST (TypeBinders' a) (Type'Sig a) n) Source #

Generated with mkFreeFoil. A scope-safe version of OpArgTyping'.

data OpArgTyping'Sig a scope term where Source #

Generated with mkFreeFoil. A signature based on OpArgTyping'.

Constructors

OpArgTypingSig :: forall a term scope. a -> [term] -> term -> OpArgTyping'Sig a scope term

Corresponds to OpArgTyping.

Instances

Instances details

GenericK (OpArgTyping'Sig a scope term :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (OpArgTyping'Sig a scope term :: Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArgTyping'Sig a scope term :: Type) = D1 ('MetaData "OpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon [term] :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)))))

Methods

fromK :: forall (x :: LoT Type). (OpArgTyping'Sig a scope term :@@: x) -> RepK (OpArgTyping'Sig a scope term) x #

toK :: forall (x :: LoT Type). RepK (OpArgTyping'Sig a scope term) x -> OpArgTyping'Sig a scope term :@@: x #

Bifoldable (OpArgTyping'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bifold :: Monoid m => OpArgTyping'Sig a m m -> m #

bifoldMap :: Monoid m => (a0 -> m) -> (b -> m) -> OpArgTyping'Sig a a0 b -> m #

bifoldr :: (a0 -> c -> c) -> (b -> c -> c) -> c -> OpArgTyping'Sig a a0 b -> c #

bifoldl :: (c -> a0 -> c) -> (c -> b -> c) -> c -> OpArgTyping'Sig a a0 b -> c #

Bifunctor (OpArgTyping'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bimap :: (a0 -> b) -> (c -> d) -> OpArgTyping'Sig a a0 c -> OpArgTyping'Sig a b d #

first :: (a0 -> b) -> OpArgTyping'Sig a a0 c -> OpArgTyping'Sig a b c #

second :: (b -> c) -> OpArgTyping'Sig a a0 b -> OpArgTyping'Sig a a0 c #

Bitraversable (OpArgTyping'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bitraverse :: Applicative f => (a0 -> f c) -> (b -> f d) -> OpArgTyping'Sig a a0 b -> f (OpArgTyping'Sig a c d) #

Foldable (OpArgTyping'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fold :: Monoid m => OpArgTyping'Sig a scope m -> m #

foldMap :: Monoid m => (a0 -> m) -> OpArgTyping'Sig a scope a0 -> m #

foldMap' :: Monoid m => (a0 -> m) -> OpArgTyping'Sig a scope a0 -> m #

foldr :: (a0 -> b -> b) -> b -> OpArgTyping'Sig a scope a0 -> b #

foldr' :: (a0 -> b -> b) -> b -> OpArgTyping'Sig a scope a0 -> b #

foldl :: (b -> a0 -> b) -> b -> OpArgTyping'Sig a scope a0 -> b #

foldl' :: (b -> a0 -> b) -> b -> OpArgTyping'Sig a scope a0 -> b #

foldr1 :: (a0 -> a0 -> a0) -> OpArgTyping'Sig a scope a0 -> a0 #

foldl1 :: (a0 -> a0 -> a0) -> OpArgTyping'Sig a scope a0 -> a0 #

toList :: OpArgTyping'Sig a scope a0 -> [a0] #

null :: OpArgTyping'Sig a scope a0 -> Bool #

length :: OpArgTyping'Sig a scope a0 -> Int #

elem :: Eq a0 => a0 -> OpArgTyping'Sig a scope a0 -> Bool #

maximum :: Ord a0 => OpArgTyping'Sig a scope a0 -> a0 #

minimum :: Ord a0 => OpArgTyping'Sig a scope a0 -> a0 #

sum :: Num a0 => OpArgTyping'Sig a scope a0 -> a0 #

product :: Num a0 => OpArgTyping'Sig a scope a0 -> a0 #

Traversable (OpArgTyping'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

traverse :: Applicative f => (a0 -> f b) -> OpArgTyping'Sig a scope a0 -> f (OpArgTyping'Sig a scope b) #

sequenceA :: Applicative f => OpArgTyping'Sig a scope (f a0) -> f (OpArgTyping'Sig a scope a0) #

mapM :: Monad m => (a0 -> m b) -> OpArgTyping'Sig a scope a0 -> m (OpArgTyping'Sig a scope b) #

sequence :: Monad m => OpArgTyping'Sig a scope (m a0) -> m (OpArgTyping'Sig a scope a0) #

Functor (OpArgTyping'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fmap :: (a0 -> b) -> OpArgTyping'Sig a scope a0 -> OpArgTyping'Sig a scope b #

(<$) :: a0 -> OpArgTyping'Sig a scope b -> OpArgTyping'Sig a scope a0 #

GenericK OpArgTyping'Sig Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK OpArgTyping'Sig

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK OpArgTyping'Sig = D1 ('MetaData "OpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon [] :: Atom (Type -> Type -> Type -> Type) (Type -> Type)) ':@: (Var2 :: Atom (Type -> Type -> Type -> Type) Type))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type)))))

Methods

fromK :: forall (x :: LoT (Type -> Type -> Type -> Type)). (OpArgTyping'Sig :@@: x) -> RepK OpArgTyping'Sig x #

toK :: forall (x :: LoT (Type -> Type -> Type -> Type)). RepK OpArgTyping'Sig x -> OpArgTyping'Sig :@@: x #

GenericK (OpArgTyping'Sig a :: Type -> Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (OpArgTyping'Sig a :: Type -> Type -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArgTyping'Sig a :: Type -> Type -> Type) = D1 ('MetaData "OpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon [] :: Atom (Type -> Type -> Type) (Type -> Type)) ':@: (Var1 :: Atom (Type -> Type -> Type) Type))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)))))

Methods

fromK :: forall (x :: LoT (Type -> Type -> Type)). (OpArgTyping'Sig a :@@: x) -> RepK (OpArgTyping'Sig a) x #

toK :: forall (x :: LoT (Type -> Type -> Type)). RepK (OpArgTyping'Sig a) x -> OpArgTyping'Sig a :@@: x #

GenericK (OpArgTyping'Sig a scope :: Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (OpArgTyping'Sig a scope :: Type -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArgTyping'Sig a scope :: Type -> Type) = D1 ('MetaData "OpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon [] :: Atom (Type -> Type) (Type -> Type)) ':@: (Var0 :: Atom (Type -> Type) Type))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)))))

Methods

fromK :: forall (x :: LoT (Type -> Type)). (OpArgTyping'Sig a scope :@@: x) -> RepK (OpArgTyping'Sig a scope) x #

toK :: forall (x :: LoT (Type -> Type)). RepK (OpArgTyping'Sig a scope) x -> OpArgTyping'Sig a scope :@@: x #

Generic (OpArgTyping'Sig a scope term) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type Rep (OpArgTyping'Sig a scope term)

Instance details

Defined in Language.SOAS.Impl.Generated

type Rep (OpArgTyping'Sig a scope term) = D1 ('MetaData "OpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [term]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term))))

Methods

from :: OpArgTyping'Sig a scope term -> Rep (OpArgTyping'Sig a scope term) x #

to :: Rep (OpArgTyping'Sig a scope term) x -> OpArgTyping'Sig a scope term #

type RepK (OpArgTyping'Sig a scope term :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArgTyping'Sig a scope term :: Type) = D1 ('MetaData "OpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon [term] :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)))))

type RepK OpArgTyping'Sig Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK OpArgTyping'Sig = D1 ('MetaData "OpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon [] :: Atom (Type -> Type -> Type -> Type) (Type -> Type)) ':@: (Var2 :: Atom (Type -> Type -> Type -> Type) Type))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type)))))

type RepK (OpArgTyping'Sig a :: Type -> Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArgTyping'Sig a :: Type -> Type -> Type) = D1 ('MetaData "OpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon [] :: Atom (Type -> Type -> Type) (Type -> Type)) ':@: (Var1 :: Atom (Type -> Type -> Type) Type))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)))))

type RepK (OpArgTyping'Sig a scope :: Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArgTyping'Sig a scope :: Type -> Type) = D1 ('MetaData "OpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon [] :: Atom (Type -> Type) (Type -> Type)) ':@: (Var0 :: Atom (Type -> Type) Type))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)))))

type Rep (OpArgTyping'Sig a scope term) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type Rep (OpArgTyping'Sig a scope term) = D1 ('MetaData "OpArgTyping'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgTypingSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [term]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term))))

type ScopedType' a = ScopedAST (TypeBinders' a) (Type'Sig a) Source #

Generated with mkFreeFoil. A scoped (and scope-safe) version of Type'.

type Type' a = AST (TypeBinders' a) (Type'Sig a) Source #

Generated with mkFreeFoil. A scope-safe version of Type'.

data Type'Sig a scope term where Source #

Generated with mkFreeFoil. A signature based on Type'.

Constructors

TypeFunSig :: forall a term scope. a -> term -> term -> Type'Sig a scope term	Corresponds to `TypeFun`.
TypeProductSig :: forall a term scope. a -> term -> term -> Type'Sig a scope term	Corresponds to `TypeProduct`.

Instances

Instances details

GenericK (Type'Sig a scope term :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Type'Sig a scope term :: Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Type'Sig a scope term :: Type) = D1 ('MetaData "Type'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "TypeFunSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)))) :+: C1 ('MetaCons "TypeProductSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)))))

Methods

fromK :: forall (x :: LoT Type). (Type'Sig a scope term :@@: x) -> RepK (Type'Sig a scope term) x #

toK :: forall (x :: LoT Type). RepK (Type'Sig a scope term) x -> Type'Sig a scope term :@@: x #

Bifoldable (Type'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bifold :: Monoid m => Type'Sig a m m -> m #

bifoldMap :: Monoid m => (a0 -> m) -> (b -> m) -> Type'Sig a a0 b -> m #

bifoldr :: (a0 -> c -> c) -> (b -> c -> c) -> c -> Type'Sig a a0 b -> c #

bifoldl :: (c -> a0 -> c) -> (c -> b -> c) -> c -> Type'Sig a a0 b -> c #

Bifunctor (Type'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bimap :: (a0 -> b) -> (c -> d) -> Type'Sig a a0 c -> Type'Sig a b d #

first :: (a0 -> b) -> Type'Sig a a0 c -> Type'Sig a b c #

second :: (b -> c) -> Type'Sig a a0 b -> Type'Sig a a0 c #

Bitraversable (Type'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bitraverse :: Applicative f => (a0 -> f c) -> (b -> f d) -> Type'Sig a a0 b -> f (Type'Sig a c d) #

Foldable (Type'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fold :: Monoid m => Type'Sig a scope m -> m #

foldMap :: Monoid m => (a0 -> m) -> Type'Sig a scope a0 -> m #

foldMap' :: Monoid m => (a0 -> m) -> Type'Sig a scope a0 -> m #

foldr :: (a0 -> b -> b) -> b -> Type'Sig a scope a0 -> b #

foldr' :: (a0 -> b -> b) -> b -> Type'Sig a scope a0 -> b #

foldl :: (b -> a0 -> b) -> b -> Type'Sig a scope a0 -> b #

foldl' :: (b -> a0 -> b) -> b -> Type'Sig a scope a0 -> b #

foldr1 :: (a0 -> a0 -> a0) -> Type'Sig a scope a0 -> a0 #

foldl1 :: (a0 -> a0 -> a0) -> Type'Sig a scope a0 -> a0 #

toList :: Type'Sig a scope a0 -> [a0] #

null :: Type'Sig a scope a0 -> Bool #

length :: Type'Sig a scope a0 -> Int #

elem :: Eq a0 => a0 -> Type'Sig a scope a0 -> Bool #

maximum :: Ord a0 => Type'Sig a scope a0 -> a0 #

minimum :: Ord a0 => Type'Sig a scope a0 -> a0 #

sum :: Num a0 => Type'Sig a scope a0 -> a0 #

product :: Num a0 => Type'Sig a scope a0 -> a0 #

IsString (Type' BNFC'Position 'VoidS) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromString :: String -> Type' BNFC'Position 'VoidS #

Traversable (Type'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

traverse :: Applicative f => (a0 -> f b) -> Type'Sig a scope a0 -> f (Type'Sig a scope b) #

sequenceA :: Applicative f => Type'Sig a scope (f a0) -> f (Type'Sig a scope a0) #

mapM :: Monad m => (a0 -> m b) -> Type'Sig a scope a0 -> m (Type'Sig a scope b) #

sequence :: Monad m => Type'Sig a scope (m a0) -> m (Type'Sig a scope a0) #

Functor (Type'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fmap :: (a0 -> b) -> Type'Sig a scope a0 -> Type'Sig a scope b #

(<$) :: a0 -> Type'Sig a scope b -> Type'Sig a scope a0 #

Show (Type' a n) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

showsPrec :: Int -> Type' a n -> ShowS #

show :: Type' a n -> String #

showList :: [Type' a n] -> ShowS #

GenericK Type'Sig Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK Type'Sig

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK Type'Sig = D1 ('MetaData "Type'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "TypeFunSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type)))) :+: C1 ('MetaCons "TypeProductSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type)))))

Methods

fromK :: forall (x :: LoT (Type -> Type -> Type -> Type)). (Type'Sig :@@: x) -> RepK Type'Sig x #

toK :: forall (x :: LoT (Type -> Type -> Type -> Type)). RepK Type'Sig x -> Type'Sig :@@: x #

ZipMatchK a => ZipMatchK (Type'Sig a :: Type -> Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type -> Type)) (bs :: LoT (Type -> Type -> Type)) (cs :: LoT (Type -> Type -> Type)). Mappings as bs cs -> (Type'Sig a :@@: as) -> (Type'Sig a :@@: bs) -> Maybe (Type'Sig a :@@: cs) #

GenericK (Type'Sig a :: Type -> Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Type'Sig a :: Type -> Type -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Type'Sig a :: Type -> Type -> Type) = D1 ('MetaData "Type'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "TypeFunSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)))) :+: C1 ('MetaCons "TypeProductSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)))))

Methods

fromK :: forall (x :: LoT (Type -> Type -> Type)). (Type'Sig a :@@: x) -> RepK (Type'Sig a) x #

toK :: forall (x :: LoT (Type -> Type -> Type)). RepK (Type'Sig a) x -> Type'Sig a :@@: x #

GenericK (Type'Sig a scope :: Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Type'Sig a scope :: Type -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Type'Sig a scope :: Type -> Type) = D1 ('MetaData "Type'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "TypeFunSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)))) :+: C1 ('MetaCons "TypeProductSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)))))

Methods

fromK :: forall (x :: LoT (Type -> Type)). (Type'Sig a scope :@@: x) -> RepK (Type'Sig a scope) x #

toK :: forall (x :: LoT (Type -> Type)). RepK (Type'Sig a scope) x -> Type'Sig a scope :@@: x #

Generic (Type'Sig a scope term) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type Rep (Type'Sig a scope term)

Instance details

Defined in Language.SOAS.Impl.Generated

type Rep (Type'Sig a scope term) = D1 ('MetaData "Type'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "TypeFunSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term))) :+: C1 ('MetaCons "TypeProductSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term))))

Methods

from :: Type'Sig a scope term -> Rep (Type'Sig a scope term) x #

to :: Rep (Type'Sig a scope term) x -> Type'Sig a scope term #

type RepK (Type'Sig a scope term :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Type'Sig a scope term :: Type) = D1 ('MetaData "Type'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "TypeFunSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)))) :+: C1 ('MetaCons "TypeProductSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)))))

type RepK Type'Sig Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK Type'Sig = D1 ('MetaData "Type'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "TypeFunSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type)))) :+: C1 ('MetaCons "TypeProductSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type)))))

type RepK (Type'Sig a :: Type -> Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Type'Sig a :: Type -> Type -> Type) = D1 ('MetaData "Type'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "TypeFunSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)))) :+: C1 ('MetaCons "TypeProductSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)))))

type RepK (Type'Sig a scope :: Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Type'Sig a scope :: Type -> Type) = D1 ('MetaData "Type'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "TypeFunSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)))) :+: C1 ('MetaCons "TypeProductSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)))))

type Rep (Type'Sig a scope term) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type Rep (Type'Sig a scope term) = D1 ('MetaData "Type'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "TypeFunSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term))) :+: C1 ('MetaCons "TypeProductSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term))))

type OpArg' a (n :: S) = OpArg'Sig a (ScopedAST (Binders' a) (Term'Sig a) n) (AST (Binders' a) (Term'Sig a) n) Source #

Generated with mkFreeFoil. A scope-safe version of OpArg'.

data OpArg'Sig a scope term where Source #

Generated with mkFreeFoil. A signature based on OpArg'.

Constructors

OpArgSig :: forall a scope term. a -> scope -> OpArg'Sig a scope term	Corresponds to `OpArg`.
PlainOpArgSig :: forall a term scope. a -> term -> OpArg'Sig a scope term	Corresponds to `PlainOpArg`.

Instances

Instances details

GenericK (OpArg'Sig a scope term :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (OpArg'Sig a scope term :: Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArg'Sig a scope term :: Type) = D1 ('MetaData "OpArg'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom Type Type))) :+: C1 ('MetaCons "PlainOpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type))))

Methods

fromK :: forall (x :: LoT Type). (OpArg'Sig a scope term :@@: x) -> RepK (OpArg'Sig a scope term) x #

toK :: forall (x :: LoT Type). RepK (OpArg'Sig a scope term) x -> OpArg'Sig a scope term :@@: x #

Bifoldable (OpArg'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bifold :: Monoid m => OpArg'Sig a m m -> m #

bifoldMap :: Monoid m => (a0 -> m) -> (b -> m) -> OpArg'Sig a a0 b -> m #

bifoldr :: (a0 -> c -> c) -> (b -> c -> c) -> c -> OpArg'Sig a a0 b -> c #

bifoldl :: (c -> a0 -> c) -> (c -> b -> c) -> c -> OpArg'Sig a a0 b -> c #

Bifunctor (OpArg'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bimap :: (a0 -> b) -> (c -> d) -> OpArg'Sig a a0 c -> OpArg'Sig a b d #

first :: (a0 -> b) -> OpArg'Sig a a0 c -> OpArg'Sig a b c #

second :: (b -> c) -> OpArg'Sig a a0 b -> OpArg'Sig a a0 c #

Bitraversable (OpArg'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bitraverse :: Applicative f => (a0 -> f c) -> (b -> f d) -> OpArg'Sig a a0 b -> f (OpArg'Sig a c d) #

Foldable (OpArg'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fold :: Monoid m => OpArg'Sig a scope m -> m #

foldMap :: Monoid m => (a0 -> m) -> OpArg'Sig a scope a0 -> m #

foldMap' :: Monoid m => (a0 -> m) -> OpArg'Sig a scope a0 -> m #

foldr :: (a0 -> b -> b) -> b -> OpArg'Sig a scope a0 -> b #

foldr' :: (a0 -> b -> b) -> b -> OpArg'Sig a scope a0 -> b #

foldl :: (b -> a0 -> b) -> b -> OpArg'Sig a scope a0 -> b #

foldl' :: (b -> a0 -> b) -> b -> OpArg'Sig a scope a0 -> b #

foldr1 :: (a0 -> a0 -> a0) -> OpArg'Sig a scope a0 -> a0 #

foldl1 :: (a0 -> a0 -> a0) -> OpArg'Sig a scope a0 -> a0 #

toList :: OpArg'Sig a scope a0 -> [a0] #

null :: OpArg'Sig a scope a0 -> Bool #

length :: OpArg'Sig a scope a0 -> Int #

elem :: Eq a0 => a0 -> OpArg'Sig a scope a0 -> Bool #

maximum :: Ord a0 => OpArg'Sig a scope a0 -> a0 #

minimum :: Ord a0 => OpArg'Sig a scope a0 -> a0 #

sum :: Num a0 => OpArg'Sig a scope a0 -> a0 #

product :: Num a0 => OpArg'Sig a scope a0 -> a0 #

Traversable (OpArg'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

traverse :: Applicative f => (a0 -> f b) -> OpArg'Sig a scope a0 -> f (OpArg'Sig a scope b) #

sequenceA :: Applicative f => OpArg'Sig a scope (f a0) -> f (OpArg'Sig a scope a0) #

mapM :: Monad m => (a0 -> m b) -> OpArg'Sig a scope a0 -> m (OpArg'Sig a scope b) #

sequence :: Monad m => OpArg'Sig a scope (m a0) -> m (OpArg'Sig a scope a0) #

Functor (OpArg'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fmap :: (a0 -> b) -> OpArg'Sig a scope a0 -> OpArg'Sig a scope b #

(<$) :: a0 -> OpArg'Sig a scope b -> OpArg'Sig a scope a0 #

GenericK OpArg'Sig Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK OpArg'Sig

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK OpArg'Sig = D1 ('MetaData "OpArg'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type -> Type) Type))) :+: C1 ('MetaCons "PlainOpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type))))

Methods

fromK :: forall (x :: LoT (Type -> Type -> Type -> Type)). (OpArg'Sig :@@: x) -> RepK OpArg'Sig x #

toK :: forall (x :: LoT (Type -> Type -> Type -> Type)). RepK OpArg'Sig x -> OpArg'Sig :@@: x #

ZipMatchK a => ZipMatchK (OpArg'Sig a :: Type -> Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type -> Type)) (bs :: LoT (Type -> Type -> Type)) (cs :: LoT (Type -> Type -> Type)). Mappings as bs cs -> (OpArg'Sig a :@@: as) -> (OpArg'Sig a :@@: bs) -> Maybe (OpArg'Sig a :@@: cs) #

GenericK (OpArg'Sig a :: Type -> Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (OpArg'Sig a :: Type -> Type -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArg'Sig a :: Type -> Type -> Type) = D1 ('MetaData "OpArg'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type) Type))) :+: C1 ('MetaCons "PlainOpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type))))

Methods

fromK :: forall (x :: LoT (Type -> Type -> Type)). (OpArg'Sig a :@@: x) -> RepK (OpArg'Sig a) x #

toK :: forall (x :: LoT (Type -> Type -> Type)). RepK (OpArg'Sig a) x -> OpArg'Sig a :@@: x #

GenericK (OpArg'Sig a scope :: Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (OpArg'Sig a scope :: Type -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArg'Sig a scope :: Type -> Type) = D1 ('MetaData "OpArg'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom (Type -> Type) Type))) :+: C1 ('MetaCons "PlainOpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type))))

Methods

fromK :: forall (x :: LoT (Type -> Type)). (OpArg'Sig a scope :@@: x) -> RepK (OpArg'Sig a scope) x #

toK :: forall (x :: LoT (Type -> Type)). RepK (OpArg'Sig a scope) x -> OpArg'Sig a scope :@@: x #

Generic (OpArg'Sig a scope term) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type Rep (OpArg'Sig a scope term)

Instance details

Defined in Language.SOAS.Impl.Generated

type Rep (OpArg'Sig a scope term) = D1 ('MetaData "OpArg'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 scope)) :+: C1 ('MetaCons "PlainOpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term)))

Methods

from :: OpArg'Sig a scope term -> Rep (OpArg'Sig a scope term) x #

to :: Rep (OpArg'Sig a scope term) x -> OpArg'Sig a scope term #

type RepK (OpArg'Sig a scope term :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArg'Sig a scope term :: Type) = D1 ('MetaData "OpArg'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom Type Type))) :+: C1 ('MetaCons "PlainOpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type))))

type RepK OpArg'Sig Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK OpArg'Sig = D1 ('MetaData "OpArg'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type -> Type) Type))) :+: C1 ('MetaCons "PlainOpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var2 :: Atom (Type -> Type -> Type -> Type) Type))))

type RepK (OpArg'Sig a :: Type -> Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArg'Sig a :: Type -> Type -> Type) = D1 ('MetaData "OpArg'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type) Type))) :+: C1 ('MetaCons "PlainOpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type))))

type RepK (OpArg'Sig a scope :: Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpArg'Sig a scope :: Type -> Type) = D1 ('MetaData "OpArg'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom (Type -> Type) Type))) :+: C1 ('MetaCons "PlainOpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type))))

type Rep (OpArg'Sig a scope term) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type Rep (OpArg'Sig a scope term) = D1 ('MetaData "OpArg'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 scope)) :+: C1 ('MetaCons "PlainOpArgSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 term)))

type ScopedTerm' a = ScopedAST (Binders' a) (Term'Sig a) Source #

Generated with mkFreeFoil. A scoped (and scope-safe) version of Term'.

type Term' a = AST (Binders' a) (Term'Sig a) Source #

Generated with mkFreeFoil. A scope-safe version of Term'.

data Term'Sig a scope term where Source #

Generated with mkFreeFoil. A signature based on Term'.

Constructors

OpSig :: forall a scope term. a -> OpIdent -> [OpArg'Sig a scope term] -> Term'Sig a scope term	Corresponds to `Op`.
MetaVarSig :: forall a term scope. a -> MetaVarIdent -> [term] -> Term'Sig a scope term	Corresponds to `MetaVar`.

Instances

Instances details

GenericK (Term'Sig a scope term :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Term'Sig a scope term :: Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Term'Sig a scope term :: Type) = D1 ('MetaData "Term'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon OpIdent :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon [OpArg'Sig a scope term] :: Atom Type Type)))) :+: C1 ('MetaCons "MetaVarSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon MetaVarIdent :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon [term] :: Atom Type Type)))))

Methods

fromK :: forall (x :: LoT Type). (Term'Sig a scope term :@@: x) -> RepK (Term'Sig a scope term) x #

toK :: forall (x :: LoT Type). RepK (Term'Sig a scope term) x -> Term'Sig a scope term :@@: x #

Bifoldable (Term'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bifold :: Monoid m => Term'Sig a m m -> m #

bifoldMap :: Monoid m => (a0 -> m) -> (b -> m) -> Term'Sig a a0 b -> m #

bifoldr :: (a0 -> c -> c) -> (b -> c -> c) -> c -> Term'Sig a a0 b -> c #

bifoldl :: (c -> a0 -> c) -> (c -> b -> c) -> c -> Term'Sig a a0 b -> c #

Bifunctor (Term'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bimap :: (a0 -> b) -> (c -> d) -> Term'Sig a a0 c -> Term'Sig a b d #

first :: (a0 -> b) -> Term'Sig a a0 c -> Term'Sig a b c #

second :: (b -> c) -> Term'Sig a a0 b -> Term'Sig a a0 c #

Bitraversable (Term'Sig a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

bitraverse :: Applicative f => (a0 -> f c) -> (b -> f d) -> Term'Sig a a0 b -> f (Term'Sig a c d) #

Foldable (Term'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fold :: Monoid m => Term'Sig a scope m -> m #

foldMap :: Monoid m => (a0 -> m) -> Term'Sig a scope a0 -> m #

foldMap' :: Monoid m => (a0 -> m) -> Term'Sig a scope a0 -> m #

foldr :: (a0 -> b -> b) -> b -> Term'Sig a scope a0 -> b #

foldr' :: (a0 -> b -> b) -> b -> Term'Sig a scope a0 -> b #

foldl :: (b -> a0 -> b) -> b -> Term'Sig a scope a0 -> b #

foldl' :: (b -> a0 -> b) -> b -> Term'Sig a scope a0 -> b #

foldr1 :: (a0 -> a0 -> a0) -> Term'Sig a scope a0 -> a0 #

foldl1 :: (a0 -> a0 -> a0) -> Term'Sig a scope a0 -> a0 #

toList :: Term'Sig a scope a0 -> [a0] #

null :: Term'Sig a scope a0 -> Bool #

length :: Term'Sig a scope a0 -> Int #

elem :: Eq a0 => a0 -> Term'Sig a scope a0 -> Bool #

maximum :: Ord a0 => Term'Sig a scope a0 -> a0 #

minimum :: Ord a0 => Term'Sig a scope a0 -> a0 #

sum :: Num a0 => Term'Sig a scope a0 -> a0 #

product :: Num a0 => Term'Sig a scope a0 -> a0 #

IsString (Term' BNFC'Position 'VoidS) Source #

>>> "?m[App(Lam(x.x), Lam(y.y))]" :: Term' Raw.BNFC'Position Foil.VoidS
?m [App (Lam (x0 . x0), Lam (x0 . x0))]
>>> "Lam(y. Let(Lam(x. x), f. ?m[y, App(f, y)]))" :: Term' Raw.BNFC'Position Foil.VoidS
Lam (x0 . Let (Lam (x1 . x1), x1 . ?m [x0, App (x1, x0)]))

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromString :: String -> Term' BNFC'Position 'VoidS #

Traversable (Term'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

traverse :: Applicative f => (a0 -> f b) -> Term'Sig a scope a0 -> f (Term'Sig a scope b) #

sequenceA :: Applicative f => Term'Sig a scope (f a0) -> f (Term'Sig a scope a0) #

mapM :: Monad m => (a0 -> m b) -> Term'Sig a scope a0 -> m (Term'Sig a scope b) #

sequence :: Monad m => Term'Sig a scope (m a0) -> m (Term'Sig a scope a0) #

Functor (Term'Sig a scope) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fmap :: (a0 -> b) -> Term'Sig a scope a0 -> Term'Sig a scope b #

(<$) :: a0 -> Term'Sig a scope b -> Term'Sig a scope a0 #

Show (Term' a n) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

showsPrec :: Int -> Term' a n -> ShowS #

show :: Term' a n -> String #

showList :: [Term' a n] -> ShowS #

GenericK Term'Sig Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK Term'Sig

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromK :: forall (x :: LoT (Type -> Type -> Type -> Type)). (Term'Sig :@@: x) -> RepK Term'Sig x #

toK :: forall (x :: LoT (Type -> Type -> Type -> Type)). RepK Term'Sig x -> Term'Sig :@@: x #

ZipMatchK a => ZipMatchK (Term'Sig a :: Type -> Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

zipMatchWithK :: forall (as :: LoT (Type -> Type -> Type)) (bs :: LoT (Type -> Type -> Type)) (cs :: LoT (Type -> Type -> Type)). Mappings as bs cs -> (Term'Sig a :@@: as) -> (Term'Sig a :@@: bs) -> Maybe (Term'Sig a :@@: cs) #

GenericK (Term'Sig a :: Type -> Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Term'Sig a :: Type -> Type -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromK :: forall (x :: LoT (Type -> Type -> Type)). (Term'Sig a :@@: x) -> RepK (Term'Sig a) x #

toK :: forall (x :: LoT (Type -> Type -> Type)). RepK (Term'Sig a) x -> Term'Sig a :@@: x #

GenericK (Term'Sig a scope :: Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Term'Sig a scope :: Type -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromK :: forall (x :: LoT (Type -> Type)). (Term'Sig a scope :@@: x) -> RepK (Term'Sig a scope) x #

toK :: forall (x :: LoT (Type -> Type)). RepK (Term'Sig a scope) x -> Term'Sig a scope :@@: x #

Generic (Term'Sig a scope term) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type Rep (Term'Sig a scope term)

Instance details

Defined in Language.SOAS.Impl.Generated

type Rep (Term'Sig a scope term) = D1 ('MetaData "Term'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpIdent) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [OpArg'Sig a scope term]))) :+: C1 ('MetaCons "MetaVarSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaVarIdent) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [term]))))

Methods

from :: Term'Sig a scope term -> Rep (Term'Sig a scope term) x #

to :: Rep (Term'Sig a scope term) x -> Term'Sig a scope term #

type RepK (Term'Sig a scope term :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Term'Sig a scope term :: Type) = D1 ('MetaData "Term'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon OpIdent :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon [OpArg'Sig a scope term] :: Atom Type Type)))) :+: C1 ('MetaCons "MetaVarSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon MetaVarIdent :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon [term] :: Atom Type Type)))))

type RepK Term'Sig Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Term'Sig a :: Type -> Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Term'Sig a scope :: Type -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type Rep (Term'Sig a scope term) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type Rep (Term'Sig a scope term) = D1 ('MetaData "Term'Sig" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "OpSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpIdent) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [OpArg'Sig a scope term]))) :+: C1 ('MetaCons "MetaVarSig" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaVarIdent) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [term]))))

data TypeBinders' a (o :: S) (i :: S) where Source #

Generated with mkFreeFoil. A binding type, scope-safe version of TypeBinders'.

Constructors

NoTypeBinders :: forall a (o :: S). a -> TypeBinders' a o o	Corresponds to `NoTypeBinders`.
SomeTypeBinders :: forall a (o :: S) (i1 :: S) (i :: S). a -> NameBinder o i1 -> TypeBinders' a i1 i -> TypeBinders' a o i	Corresponds to `SomeTypeBinders`.

Instances

Instances details

GenericK (TypeBinders' a o i :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (TypeBinders' a o i :: Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (TypeBinders' a o i :: Type) = D1 ('MetaData "TypeBinders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoTypeBinders" 'PrefixI 'False) (('Kon (o ~~ i) :: Atom Type Constraint) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type))) :+: C1 ('MetaCons "SomeTypeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (NameBinder o) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (TypeBinders' a) :: Atom (S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)) ':@: ('Kon i :: Atom (S -> Type) S)))))))

Methods

fromK :: forall (x :: LoT Type). (TypeBinders' a o i :@@: x) -> RepK (TypeBinders' a o i) x #

toK :: forall (x :: LoT Type). RepK (TypeBinders' a o i) x -> TypeBinders' a o i :@@: x #

CoSinkable (TypeBinders' a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> TypeBinders' a n l -> (forall (l' :: S). (Name l -> Name l') -> TypeBinders' a n' l' -> r) -> r #

withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> TypeBinders' a n l -> (forall (o' :: S). DExt o o' => f n l o o' -> TypeBinders' a o o' -> r) -> r #

HasNameBinders (TypeBinders' a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

getNameBinders :: forall (n :: S) (l :: S). TypeBinders' a n l -> NameBinders n l #

unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). TypeBinders' a n l -> NameBinders n l' -> TypeBinders' a n l' #

getNameBindersRaw :: forall (n :: S) (l :: S). TypeBinders' a n l -> [RawName] #

reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). TypeBinders' a n l -> [RawName] -> (TypeBinders' a n l', [RawName]) #

IsString (Type' BNFC'Position 'VoidS) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromString :: String -> Type' BNFC'Position 'VoidS #

Show (Type' a n) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

showsPrec :: Int -> Type' a n -> ShowS #

show :: Type' a n -> String #

showList :: [Type' a n] -> ShowS #

GenericK TypeBinders' Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK TypeBinders'

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromK :: forall (x :: LoT (Type -> S -> S -> Type)). (TypeBinders' :@@: x) -> RepK TypeBinders' x #

toK :: forall (x :: LoT (Type -> S -> S -> Type)). RepK TypeBinders' x -> TypeBinders' :@@: x #

SinkableK (TypeBinders' a :: S -> S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (TypeBinders' a :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (TypeBinders' a :@@: cs) -> r) -> r #

GenericK (TypeBinders' a :: S -> S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (TypeBinders' a :: S -> S -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (TypeBinders' a :: S -> S -> Type) = D1 ('MetaData "TypeBinders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoTypeBinders" 'PrefixI 'False) (((('Kon ((~~) :: S -> S -> Constraint) :: Atom (S -> S -> Type) (S -> S -> Constraint)) ':@: (Var0 :: Atom (S -> S -> Type) S)) ':@: (Var1 :: Atom (S -> S -> Type) S)) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type))) :+: C1 ('MetaCons "SomeTypeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon NameBinder :: Atom (S -> S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (TypeBinders' a) :: Atom (S -> S -> S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))))))

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (TypeBinders' a :@@: x) -> RepK (TypeBinders' a) x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK (TypeBinders' a) x -> TypeBinders' a :@@: x #

GenericK (TypeBinders' a o :: S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (TypeBinders' a o :: S -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (TypeBinders' a o :: S -> Type) = D1 ('MetaData "TypeBinders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoTypeBinders" 'PrefixI 'False) ((('Kon ((~~) o :: S -> Constraint) :: Atom (S -> Type) (S -> Constraint)) ':@: (Var0 :: Atom (S -> Type) S)) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type))) :+: C1 ('MetaCons "SomeTypeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (NameBinder o) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (TypeBinders' a) :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S)) ':@: (Var1 :: Atom (S -> S -> Type) S)))))))

Methods

fromK :: forall (x :: LoT (S -> Type)). (TypeBinders' a o :@@: x) -> RepK (TypeBinders' a o) x #

toK :: forall (x :: LoT (S -> Type)). RepK (TypeBinders' a o) x -> TypeBinders' a o :@@: x #

type RepK (TypeBinders' a o i :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (TypeBinders' a o i :: Type) = D1 ('MetaData "TypeBinders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoTypeBinders" 'PrefixI 'False) (('Kon (o ~~ i) :: Atom Type Constraint) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type))) :+: C1 ('MetaCons "SomeTypeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (NameBinder o) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (TypeBinders' a) :: Atom (S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)) ':@: ('Kon i :: Atom (S -> Type) S)))))))

type RepK TypeBinders' Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (TypeBinders' a :: S -> S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (TypeBinders' a :: S -> S -> Type) = D1 ('MetaData "TypeBinders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoTypeBinders" 'PrefixI 'False) (((('Kon ((~~) :: S -> S -> Constraint) :: Atom (S -> S -> Type) (S -> S -> Constraint)) ':@: (Var0 :: Atom (S -> S -> Type) S)) ':@: (Var1 :: Atom (S -> S -> Type) S)) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type))) :+: C1 ('MetaCons "SomeTypeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon NameBinder :: Atom (S -> S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (TypeBinders' a) :: Atom (S -> S -> S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))))))

type RepK (TypeBinders' a o :: S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (TypeBinders' a o :: S -> Type) = D1 ('MetaData "TypeBinders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoTypeBinders" 'PrefixI 'False) ((('Kon ((~~) o :: S -> Constraint) :: Atom (S -> Type) (S -> Constraint)) ':@: (Var0 :: Atom (S -> Type) S)) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type))) :+: C1 ('MetaCons "SomeTypeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (NameBinder o) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (TypeBinders' a) :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S)) ':@: (Var1 :: Atom (S -> S -> Type) S)))))))

data Binders' a (o :: S) (i :: S) where Source #

Generated with mkFreeFoil. A binding type, scope-safe version of Binders'.

Constructors

NoBinders :: forall a (o :: S). a -> Binders' a o o	Corresponds to `NoBinders`.
SomeBinders :: forall a (o :: S) (i1 :: S) (i :: S). a -> NameBinder o i1 -> Binders' a i1 i -> Binders' a o i	Corresponds to `SomeBinders`.

Instances

Instances details

GenericK (Binders' a o i :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Binders' a o i :: Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Binders' a o i :: Type) = D1 ('MetaData "Binders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoBinders" 'PrefixI 'False) (('Kon (o ~~ i) :: Atom Type Constraint) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type))) :+: C1 ('MetaCons "SomeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (NameBinder o) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (Binders' a) :: Atom (S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)) ':@: ('Kon i :: Atom (S -> Type) S)))))))

Methods

fromK :: forall (x :: LoT Type). (Binders' a o i :@@: x) -> RepK (Binders' a o i) x #

toK :: forall (x :: LoT Type). RepK (Binders' a o i) x -> Binders' a o i :@@: x #

CoSinkable (Binders' a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> Binders' a n l -> (forall (l' :: S). (Name l -> Name l') -> Binders' a n' l' -> r) -> r #

withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> Binders' a n l -> (forall (o' :: S). DExt o o' => f n l o o' -> Binders' a o o' -> r) -> r #

HasNameBinders (Binders' a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

getNameBinders :: forall (n :: S) (l :: S). Binders' a n l -> NameBinders n l #

unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). Binders' a n l -> NameBinders n l' -> Binders' a n l' #

getNameBindersRaw :: forall (n :: S) (l :: S). Binders' a n l -> [RawName] #

reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). Binders' a n l -> [RawName] -> (Binders' a n l', [RawName]) #

UnifiablePattern (Binders' a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => Binders' a n l -> Binders' a n r -> UnifyNameBinders (Binders' a) n l r #

IsString (Term' BNFC'Position 'VoidS) Source #

>>> "?m[App(Lam(x.x), Lam(y.y))]" :: Term' Raw.BNFC'Position Foil.VoidS
?m [App (Lam (x0 . x0), Lam (x0 . x0))]
>>> "Lam(y. Let(Lam(x. x), f. ?m[y, App(f, y)]))" :: Term' Raw.BNFC'Position Foil.VoidS
Lam (x0 . Let (Lam (x1 . x1), x1 . ?m [x0, App (x1, x0)]))

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromString :: String -> Term' BNFC'Position 'VoidS #

Show (Term' a n) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

showsPrec :: Int -> Term' a n -> ShowS #

show :: Term' a n -> String #

showList :: [Term' a n] -> ShowS #

GenericK Binders' Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK Binders'

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromK :: forall (x :: LoT (Type -> S -> S -> Type)). (Binders' :@@: x) -> RepK Binders' x #

toK :: forall (x :: LoT (Type -> S -> S -> Type)). RepK Binders' x -> Binders' :@@: x #

SinkableK (Binders' a :: S -> S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (Binders' a :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (Binders' a :@@: cs) -> r) -> r #

GenericK (Binders' a :: S -> S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Binders' a :: S -> S -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Binders' a :: S -> S -> Type) = D1 ('MetaData "Binders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoBinders" 'PrefixI 'False) (((('Kon ((~~) :: S -> S -> Constraint) :: Atom (S -> S -> Type) (S -> S -> Constraint)) ':@: (Var0 :: Atom (S -> S -> Type) S)) ':@: (Var1 :: Atom (S -> S -> Type) S)) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type))) :+: C1 ('MetaCons "SomeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon NameBinder :: Atom (S -> S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (Binders' a) :: Atom (S -> S -> S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))))))

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (Binders' a :@@: x) -> RepK (Binders' a) x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK (Binders' a) x -> Binders' a :@@: x #

GenericK (Binders' a o :: S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Binders' a o :: S -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Binders' a o :: S -> Type) = D1 ('MetaData "Binders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoBinders" 'PrefixI 'False) ((('Kon ((~~) o :: S -> Constraint) :: Atom (S -> Type) (S -> Constraint)) ':@: (Var0 :: Atom (S -> Type) S)) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type))) :+: C1 ('MetaCons "SomeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (NameBinder o) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (Binders' a) :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S)) ':@: (Var1 :: Atom (S -> S -> Type) S)))))))

Methods

fromK :: forall (x :: LoT (S -> Type)). (Binders' a o :@@: x) -> RepK (Binders' a o) x #

toK :: forall (x :: LoT (S -> Type)). RepK (Binders' a o) x -> Binders' a o :@@: x #

type RepK (Binders' a o i :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Binders' a o i :: Type) = D1 ('MetaData "Binders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoBinders" 'PrefixI 'False) (('Kon (o ~~ i) :: Atom Type Constraint) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type))) :+: C1 ('MetaCons "SomeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (NameBinder o) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (Binders' a) :: Atom (S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)) ':@: ('Kon i :: Atom (S -> Type) S)))))))

type RepK Binders' Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Binders' a :: S -> S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Binders' a :: S -> S -> Type) = D1 ('MetaData "Binders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoBinders" 'PrefixI 'False) (((('Kon ((~~) :: S -> S -> Constraint) :: Atom (S -> S -> Type) (S -> S -> Constraint)) ':@: (Var0 :: Atom (S -> S -> Type) S)) ':@: (Var1 :: Atom (S -> S -> Type) S)) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type))) :+: C1 ('MetaCons "SomeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon NameBinder :: Atom (S -> S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (Binders' a) :: Atom (S -> S -> S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))))))

type RepK (Binders' a o :: S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Binders' a o :: S -> Type) = D1 ('MetaData "Binders'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "NoBinders" 'PrefixI 'False) ((('Kon ((~~) o :: S -> Constraint) :: Atom (S -> Type) (S -> Constraint)) ':@: (Var0 :: Atom (S -> Type) S)) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type))) :+: C1 ('MetaCons "SomeBinders" 'PrefixI 'False) (Exists S (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (NameBinder o) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (Binders' a) :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S)) ':@: (Var1 :: Atom (S -> S -> Type) S)))))))

data TermTyping' a (o :: S) where Source #

Generated with mkFreeFoil. A scope-safe version of TermTyping'.

Constructors

TermTyping :: forall a (o :: S) (i :: S). a -> TypeBinders' a o i -> Context' a -> Term' a i -> Type' a i -> TermTyping' a o

Corresponds to TermTyping.

data VarTyping' a (o :: S) where Source #

Generated with mkFreeFoil. A scope-safe version of VarTyping'.

Constructors

VarTyping :: forall a (o :: S). a -> Name o -> Type' a o -> VarTyping' a o

Corresponds to VarTyping.

data Constraint' a (o :: S) where Source #

Generated with mkFreeFoil. A scope-safe version of Constraint'.

Constructors

ConstraintEq :: forall a (o :: S) (i :: S). a -> Binders' a o i -> Term' a i -> Term' a i -> Constraint' a o

Corresponds to ConstraintEq.

Instances

Instances details

GenericK (Constraint' a o :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Constraint' a o :: Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Constraint' a o :: Type) = D1 ('MetaData "Constraint'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "ConstraintEq" 'PrefixI 'False) (Exists S ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (Binders' a o) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)))))))

Methods

fromK :: forall (x :: LoT Type). (Constraint' a o :@@: x) -> RepK (Constraint' a o) x #

toK :: forall (x :: LoT Type). RepK (Constraint' a o) x -> Constraint' a o :@@: x #

Sinkable (Constraint' a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Constraint' a n -> Constraint' a l #

IsString (Constraint' BNFC'Position 'VoidS) Source #

>>> "∀ x y. ?m[x, y] = App(y, x)" :: Constraint' Raw.BNFC'Position Foil.VoidS
∀ x0 x1 . ?m [x0, x1] = App (x1, x0)

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromString :: String -> Constraint' BNFC'Position 'VoidS #

Show (Constraint' a n) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

showsPrec :: Int -> Constraint' a n -> ShowS #

show :: Constraint' a n -> String #

showList :: [Constraint' a n] -> ShowS #

GenericK Constraint' Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK Constraint'

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromK :: forall (x :: LoT (Type -> S -> Type)). (Constraint' :@@: x) -> RepK Constraint' x #

toK :: forall (x :: LoT (Type -> S -> Type)). RepK Constraint' x -> Constraint' :@@: x #

GenericK (Constraint' a :: S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Constraint' a :: S -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Constraint' a :: S -> Type) = D1 ('MetaData "Constraint'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "ConstraintEq" 'PrefixI 'False) (Exists S ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (Binders' a) :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> Type) S)))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S)))))))

Methods

fromK :: forall (x :: LoT (S -> Type)). (Constraint' a :@@: x) -> RepK (Constraint' a) x #

toK :: forall (x :: LoT (S -> Type)). RepK (Constraint' a) x -> Constraint' a :@@: x #

type RepK (Constraint' a o :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Constraint' a o :: Type) = D1 ('MetaData "Constraint'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "ConstraintEq" 'PrefixI 'False) (Exists S ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (Binders' a o) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)))))))

type RepK Constraint' Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Constraint' a :: S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Constraint' a :: S -> Type) = D1 ('MetaData "Constraint'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "ConstraintEq" 'PrefixI 'False) (Exists S ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (Binders' a) :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> Type) S)))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S)))))))

data OpTyping' a (o :: S) where Source #

Generated with mkFreeFoil. A scope-safe version of OpTyping'.

Constructors

OpTyping :: forall a (o :: S) (i :: S). a -> OpIdent -> TypeBinders' a o i -> [ScopedOpArgTyping' a i] -> Type' a i -> OpTyping' a o

Corresponds to OpTyping.

Instances

Instances details

GenericK (OpTyping' a o :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (OpTyping' a o :: Type)

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromK :: forall (x :: LoT Type). (OpTyping' a o :@@: x) -> RepK (OpTyping' a o) x #

toK :: forall (x :: LoT Type). RepK (OpTyping' a o) x -> OpTyping' a o :@@: x #

Sinkable (OpTyping' a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> OpTyping' a n -> OpTyping' a l #

IsString (OpTyping' BNFC'Position 'VoidS) Source #

>>> "Lam : ∀ a b. (a.b) → a→b" :: OpTyping' Raw.BNFC'Position Foil.VoidS
Lam : ∀ x0 x1 . (x0 . x1) → x0 → x1

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromString :: String -> OpTyping' BNFC'Position 'VoidS #

Show (OpTyping' a n) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

showsPrec :: Int -> OpTyping' a n -> ShowS #

show :: OpTyping' a n -> String #

showList :: [OpTyping' a n] -> ShowS #

GenericK OpTyping' Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK OpTyping'

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromK :: forall (x :: LoT (Type -> S -> Type)). (OpTyping' :@@: x) -> RepK OpTyping' x #

toK :: forall (x :: LoT (Type -> S -> Type)). RepK OpTyping' x -> OpTyping' :@@: x #

GenericK (OpTyping' a :: S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (OpTyping' a :: S -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromK :: forall (x :: LoT (S -> Type)). (OpTyping' a :@@: x) -> RepK (OpTyping' a) x #

toK :: forall (x :: LoT (S -> Type)). RepK (OpTyping' a) x -> OpTyping' a :@@: x #

type RepK (OpTyping' a o :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK OpTyping' Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (OpTyping' a :: S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

data MetaVarTyping' a (o :: S) where Source #

Generated with mkFreeFoil. A scope-safe version of MetaVarTyping'.

Constructors

MetaVarTyping :: forall a (o :: S). a -> MetaVarIdent -> [Type' a o] -> Type' a o -> MetaVarTyping' a o

Corresponds to MetaVarTyping.

data Subst' a (o :: S) where Source #

Generated with mkFreeFoil. A scope-safe version of Subst'.

Constructors

Subst :: forall a (o :: S) (i :: S). a -> MetaVarIdent -> Binders' a o i -> Term' a i -> Subst' a o

Corresponds to Subst.

Instances

Instances details

GenericK (Subst' a o :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Subst' a o :: Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Subst' a o :: Type) = D1 ('MetaData "Subst'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "Subst" 'PrefixI 'False) (Exists S ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon MetaVarIdent :: Atom (S -> Type) Type))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (Binders' a o) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)))))))

Methods

fromK :: forall (x :: LoT Type). (Subst' a o :@@: x) -> RepK (Subst' a o) x #

toK :: forall (x :: LoT Type). RepK (Subst' a o) x -> Subst' a o :@@: x #

Sinkable (Subst' a) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Subst' a n -> Subst' a l #

IsString (Subst' BNFC'Position 'VoidS) Source #

>>> "?m[x y] ↦ App(y, x)" :: Subst' Raw.BNFC'Position Foil.VoidS
?m [x0 x1] ↦ App (x1, x0)

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromString :: String -> Subst' BNFC'Position 'VoidS #

Show (Subst' a n) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

showsPrec :: Int -> Subst' a n -> ShowS #

show :: Subst' a n -> String #

showList :: [Subst' a n] -> ShowS #

GenericK Subst' Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK Subst'

Instance details

Defined in Language.SOAS.Impl.Generated

Methods

fromK :: forall (x :: LoT (Type -> S -> Type)). (Subst' :@@: x) -> RepK Subst' x #

toK :: forall (x :: LoT (Type -> S -> Type)). RepK Subst' x -> Subst' :@@: x #

GenericK (Subst' a :: S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

Associated Types

type RepK (Subst' a :: S -> Type)

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Subst' a :: S -> Type) = D1 ('MetaData "Subst'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "Subst" 'PrefixI 'False) (Exists S ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon MetaVarIdent :: Atom (S -> S -> Type) Type))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (Binders' a) :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S)))))))

Methods

fromK :: forall (x :: LoT (S -> Type)). (Subst' a :@@: x) -> RepK (Subst' a) x #

toK :: forall (x :: LoT (S -> Type)). RepK (Subst' a) x -> Subst' a :@@: x #

type RepK (Subst' a o :: Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Subst' a o :: Type) = D1 ('MetaData "Subst'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "Subst" 'PrefixI 'False) (Exists S ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon MetaVarIdent :: Atom (S -> Type) Type))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (Binders' a o) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)))))))

type RepK Subst' Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Subst' a :: S -> Type) Source #

Instance details

Defined in Language.SOAS.Impl.Generated

type RepK (Subst' a :: S -> Type) = D1 ('MetaData "Subst'" "Language.SOAS.Impl.Generated" "soas-0.2.0-6nIwvOohq1pE2tcrIqGIBi" 'False) (C1 ('MetaCons "Subst" 'PrefixI 'False) (Exists S ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom (S -> S -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon MetaVarIdent :: Atom (S -> S -> Type) Type))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (Binders' a) :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (('Kon (AST (Binders' a) (Term'Sig a)) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S)))))))

pattern ScopedOpArgTyping :: forall a (o :: S). a -> OpArgTyping' a o -> ScopedOpArgTyping' a o Source #

Generated with mkFreeFoil. Pattern synonym for an AST node of type ScopedOpArgTyping.

pattern OpArgTyping :: forall a (o :: S). a -> [Type' a o] -> Type' a o -> OpArgTyping' a o Source #

Generated with mkFreeFoil. Pattern synonym for an AST node of type OpArgTyping.

pattern TypeProduct :: a -> Type' a o -> Type' a o -> Type' a o Source #

Generated with mkFreeFoil. Pattern synonym for an AST node of type TypeProduct.

pattern TypeFun :: a -> Type' a o -> Type' a o -> Type' a o Source #

Generated with mkFreeFoil. Pattern synonym for an AST node of type TypeFun.

pattern PlainOpArg :: forall a (o :: S). a -> Term' a o -> OpArg' a o Source #

Generated with mkFreeFoil. Pattern synonym for an AST node of type PlainOpArg.

pattern OpArg :: forall a (o :: S) (i :: S). () => a -> Binders' a o i -> Term' a i -> OpArg' a o Source #

Generated with mkFreeFoil. Pattern synonym for an AST node of type OpArg.

pattern MetaVar :: a -> MetaVarIdent -> [Term' a o] -> Term' a o Source #

Generated with mkFreeFoil. Pattern synonym for an AST node of type MetaVar.

pattern Op :: a -> OpIdent -> [OpArg' a o] -> Term' a o Source #

Generated with mkFreeFoil. Pattern synonym for an AST node of type Op.

fromTerm'Sig :: Term'Sig a (Binders' a, ScopedTerm' a) (Term' a) -> Term' a Source #

Generated with mkFreeFoil. A helper used to convert from scope-safe to raw representation.

fromOpArg'Sig :: OpArg'Sig a (Binders' a, ScopedTerm' a) (Term' a) -> OpArg' a Source #

Generated with mkFreeFoil. A helper used to convert from scope-safe to raw representation.

fromBinders' :: forall a (o :: S) (i :: S). Binders' a o i -> Binders' a Source #

Generated with mkFreeFoil. Convert a scope-safe to a raw binding.

fromOpArg' :: forall a (o :: S). OpArg' a o -> OpArg' a Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

fromTerm' :: forall a (o :: S). Term' a o -> Term' a Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

fromType'Sig :: Type'Sig a (TypeBinders' a, ScopedType' a) (Type' a) -> Type' a Source #

Generated with mkFreeFoil. A helper used to convert from scope-safe to raw representation.

fromOpArgTyping'Sig :: OpArgTyping'Sig a (TypeBinders' a, ScopedType' a) (Type' a) -> OpArgTyping' a Source #

Generated with mkFreeFoil. A helper used to convert from scope-safe to raw representation.

fromScopedOpArgTyping'Sig :: ScopedOpArgTyping'Sig a (TypeBinders' a, ScopedType' a) (Type' a) -> ScopedOpArgTyping' a Source #

Generated with mkFreeFoil. A helper used to convert from scope-safe to raw representation.

fromTypeBinders' :: forall a (o :: S) (i :: S). TypeBinders' a o i -> TypeBinders' a Source #

Generated with mkFreeFoil. Convert a scope-safe to a raw binding.

fromOpArgTyping' :: forall a (o :: S). OpArgTyping' a o -> OpArgTyping' a Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

fromScopedOpArgTyping' :: forall a (i :: S). ScopedOpArgTyping' a i -> ScopedOpArgTyping' a Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

fromType' :: forall a (o :: S). Type' a o -> Type' a Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

fromSubst' :: forall a (o :: S). Subst' a o -> Subst' a Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

fromMetaVarTyping' :: forall a (o :: S). MetaVarTyping' a o -> MetaVarTyping' a Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

fromOpTyping' :: forall a (o :: S). OpTyping' a o -> OpTyping' a Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

fromConstraint' :: forall a (o :: S). Constraint' a o -> Constraint' a Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

fromVarTyping' :: forall a (o :: S). VarTyping' a o -> VarTyping' a Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

fromTermTyping' :: forall a (o :: S). TermTyping' a o -> TermTyping' a Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

toTerm'Sig :: Term' a -> Either VarIdent (Term'Sig a (Binders' a, ScopedTerm' a) (Term' a)) Source #

Generated with mkFreeFoil. A helper used to convert from raw to scope-safe representation.

toOpArg'Sig :: OpArg' a -> OpArg'Sig a (Binders' a, ScopedTerm' a) (Term' a) Source #

Generated with mkFreeFoil. A helper used to convert from raw to scope-safe representation.

toBinders' :: forall (o :: S) a r. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> Binders' a -> (forall (i :: S). DExt o i => Binders' a o i -> Map VarIdent (Name i) -> r) -> r Source #

Generated with mkFreeFoil. Convert from raw to scope-safe binding (CPS-style).

toOpArg' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> OpArg' a -> OpArg' a o Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

toTerm' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> Term' a -> Term' a o Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

toType'Sig :: Type' a -> Either VarIdent (Type'Sig a (TypeBinders' a, ScopedType' a) (Type' a)) Source #

Generated with mkFreeFoil. A helper used to convert from raw to scope-safe representation.

toOpArgTyping'Sig :: OpArgTyping' a -> OpArgTyping'Sig a (TypeBinders' a, ScopedType' a) (Type' a) Source #

Generated with mkFreeFoil. A helper used to convert from raw to scope-safe representation.

toScopedOpArgTyping'Sig :: ScopedOpArgTyping' a -> ScopedOpArgTyping'Sig a (TypeBinders' a, ScopedType' a) (Type' a) Source #

Generated with mkFreeFoil. A helper used to convert from raw to scope-safe representation.

toTypeBinders' :: forall (o :: S) a r. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> TypeBinders' a -> (forall (i :: S). DExt o i => TypeBinders' a o i -> Map VarIdent (Name i) -> r) -> r Source #

Generated with mkFreeFoil. Convert from raw to scope-safe binding (CPS-style).

toOpArgTyping' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> OpArgTyping' a -> OpArgTyping' a o Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

toScopedOpArgTyping' :: forall (i :: S) a. (Distinct i, Ord VarIdent) => Scope i -> Map VarIdent (Name i) -> ScopedOpArgTyping' a -> ScopedOpArgTyping' a i Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

toType' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> Type' a -> Type' a o Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

toSubst' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> Subst' a -> Subst' a o Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

toMetaVarTyping' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> MetaVarTyping' a -> MetaVarTyping' a o Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

toOpTyping' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> OpTyping' a -> OpTyping' a o Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

toConstraint' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> Constraint' a -> Constraint' a o Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

toVarTyping' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> VarTyping' a -> VarTyping' a o Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

toTermTyping' :: forall (o :: S) a. (Distinct o, Ord VarIdent) => Scope o -> Map VarIdent (Name o) -> TermTyping' a -> TermTyping' a o Source #

Generated with mkFreeFoil. Convert from scope-safe to raw representation.

User-defined helpers

unsafeParse :: ([Token] -> Either String a) -> String -> a Source #

Orphan instances

ZipMatchK BNFC'Position Source #	Ignore `BNFC'Position` when matching terms.
Instance details Methods zipMatchWithK :: forall (as :: LoT Type) (bs :: LoT Type) (cs :: LoT Type). Mappings as bs cs -> (BNFC'Position :@@: as) -> (BNFC'Position :@@: bs) -> Maybe (BNFC'Position :@@: cs) #
ZipMatchK MetaVarIdent Source #	Match `MetaVarIdent` via `Eq`.
Instance details Methods zipMatchWithK :: forall (as :: LoT Type) (bs :: LoT Type) (cs :: LoT Type). Mappings as bs cs -> (MetaVarIdent :@@: as) -> (MetaVarIdent :@@: bs) -> Maybe (MetaVarIdent :@@: cs) #
ZipMatchK OpIdent Source #	Match `OpIdent` via `Eq`.
Instance details Methods zipMatchWithK :: forall (as :: LoT Type) (bs :: LoT Type) (cs :: LoT Type). Mappings as bs cs -> (OpIdent :@@: as) -> (OpIdent :@@: bs) -> Maybe (OpIdent :@@: cs) #