Safe Haskell	None
Language	Haskell2010

Language.LambdaPi.Impl.FreeFoil

Description

Free foil implementation of the $\lambda\Pi$-calculus (with pairs).

Free foil provides general definitions or implementations for the following:

Freely generated (from a simple signature) scope-safe AST.
Correct capture-avoiding substitution (see substitute).
Correct $\alpha$-equivalence checks (see alphaEquiv and alphaEquivRefreshed) as well as $\alpha$-normalization (see refreshAST).
Conversion helpers (see convertToAST and convertFromAST).

The following is implemented manually in this module:

Convenient pattern synonyms.
ZipMatch instances (enabling general $\alpha$-equivalence).
Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see toLambdaPi and fromLambdaPi.
Computation of weak head normal form (WHNF), see whnf.
Entry point, gluing everything together. See defaultMain.

Note: free foil does not (easily) support patterns at the moment, so only wildcard patterns and variable patterns are handled in this implementation.

See Language.LambdaPi.Impl.FreeFoilTH for a variation of this with more automation via Template Haskell.

Synopsis

data LambdaPiF scope term
- = AppF term term
- | LamF scope
- | PiF term scope
- | UniverseF
data PairF scope term
- = PairF term term
- | FirstF term
- | SecondF term
- | ProductF term term
type (:+:) = Sum :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type
type LambdaPi (n :: S) = AST NameBinder (LambdaPiF :+: PairF) n
pattern App :: LambdaPi n -> LambdaPi n -> LambdaPi n
pattern Lam :: () => NameBinder n l -> LambdaPi l -> LambdaPi n
pattern Pi :: () => NameBinder n l -> LambdaPi n -> LambdaPi l -> LambdaPi n
pattern Pair :: LambdaPi n -> LambdaPi n -> LambdaPi n
pattern First :: LambdaPi n -> LambdaPi n
pattern Second :: LambdaPi n -> LambdaPi n
pattern Product :: LambdaPi n -> LambdaPi n -> LambdaPi n
pattern Universe :: LambdaPi n
whnf :: forall (n :: S). Distinct n => Scope n -> LambdaPi n -> LambdaPi n
toLambdaPiLam :: forall (n :: S). Distinct n => Scope n -> Map VarIdent (Name n) -> Pattern -> ScopedTerm -> LambdaPi n
toLambdaPiPi :: forall (n :: S). Distinct n => Scope n -> Map VarIdent (Name n) -> Pattern -> Term -> ScopedTerm -> LambdaPi n
toLambdaPi :: forall (n :: S). Distinct n => Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPiClosed :: Term -> LambdaPi 'VoidS
fromLambdaPi :: forall (n :: S). [VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi' :: forall (n :: S). LambdaPi n -> Term
ppLambdaPi :: LambdaPi 'VoidS -> String
interpretCommand :: Command -> IO ()
interpretProgram :: Program -> IO ()
defaultMain :: IO ()

Documentation

>>> import qualified Control.Monad.Foil as Foil
>>> import Control.Monad.Free.Foil
>>> :set -XOverloadedStrings
>>> :set -XDataKinds

data LambdaPiF scope term Source #

The signature Bifunctor for the $\lambda\Pi$.

Constructors

AppF term term	Application: $(t_1 \; t_2)$
LamF scope	Abstraction: $\lambda x. t$
PiF term scope	Dependent function type: $\prod_{x : T_1} T_2$
UniverseF	Universe (type of types): $\mathcal{U}$

Instances

Instances details

Bifoldable LambdaPiF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

bifold :: Monoid m => LambdaPiF m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> LambdaPiF a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> LambdaPiF a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> LambdaPiF a b -> c #

Bifunctor LambdaPiF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

bimap :: (a -> b) -> (c -> d) -> LambdaPiF a c -> LambdaPiF b d #

first :: (a -> b) -> LambdaPiF a c -> LambdaPiF b c #

second :: (b -> c) -> LambdaPiF a b -> LambdaPiF a c #

Bitraversable LambdaPiF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> LambdaPiF a b -> f (LambdaPiF c d) #

GenericK (LambdaPiF scope term :: Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Associated Types

type RepK (LambdaPiF scope term :: Type)

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK (LambdaPiF scope term :: Type) = D1 ('MetaData "LambdaPiF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "AppF" 'PrefixI 'False) (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 "LamF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom Type Type)))) :+: (C1 ('MetaCons "PiF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom Type Type))) :+: C1 ('MetaCons "UniverseF" 'PrefixI 'False) (U1 :: LoT Type -> Type)))

Methods

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

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

Foldable (LambdaPiF scope) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

fold :: Monoid m => LambdaPiF scope m -> m #

foldMap :: Monoid m => (a -> m) -> LambdaPiF scope a -> m #

foldMap' :: Monoid m => (a -> m) -> LambdaPiF scope a -> m #

foldr :: (a -> b -> b) -> b -> LambdaPiF scope a -> b #

foldr' :: (a -> b -> b) -> b -> LambdaPiF scope a -> b #

foldl :: (b -> a -> b) -> b -> LambdaPiF scope a -> b #

foldl' :: (b -> a -> b) -> b -> LambdaPiF scope a -> b #

foldr1 :: (a -> a -> a) -> LambdaPiF scope a -> a #

foldl1 :: (a -> a -> a) -> LambdaPiF scope a -> a #

toList :: LambdaPiF scope a -> [a] #

null :: LambdaPiF scope a -> Bool #

length :: LambdaPiF scope a -> Int #

elem :: Eq a => a -> LambdaPiF scope a -> Bool #

maximum :: Ord a => LambdaPiF scope a -> a #

minimum :: Ord a => LambdaPiF scope a -> a #

sum :: Num a => LambdaPiF scope a -> a #

product :: Num a => LambdaPiF scope a -> a #

IsString (LambdaPi 'VoidS) Source #

$\lambda\Pi$-terms can be (unsafely) parsed from a String via Term.

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

fromString :: String -> LambdaPi 'VoidS #

Traversable (LambdaPiF scope) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

traverse :: Applicative f => (a -> f b) -> LambdaPiF scope a -> f (LambdaPiF scope b) #

sequenceA :: Applicative f => LambdaPiF scope (f a) -> f (LambdaPiF scope a) #

mapM :: Monad m => (a -> m b) -> LambdaPiF scope a -> m (LambdaPiF scope b) #

sequence :: Monad m => LambdaPiF scope (m a) -> m (LambdaPiF scope a) #

Functor (LambdaPiF scope) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

fmap :: (a -> b) -> LambdaPiF scope a -> LambdaPiF scope b #

(<$) :: a -> LambdaPiF scope b -> LambdaPiF scope a #

Show (LambdaPi 'VoidS) Source #

$\lambda\Pi$-terms are pretty-printed using BNFC-generated printer via Term.

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

showsPrec :: Int -> LambdaPi 'VoidS -> ShowS #

show :: LambdaPi 'VoidS -> String #

showList :: [LambdaPi 'VoidS] -> ShowS #

(Show term, Show scope) => Show (LambdaPiF scope term) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

showsPrec :: Int -> LambdaPiF scope term -> ShowS #

show :: LambdaPiF scope term -> String #

showList :: [LambdaPiF scope term] -> ShowS #

(Eq term, Eq scope) => Eq (LambdaPiF scope term) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

(==) :: LambdaPiF scope term -> LambdaPiF scope term -> Bool #

(/=) :: LambdaPiF scope term -> LambdaPiF scope term -> Bool #

ZipMatchK LambdaPiF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

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

GenericK LambdaPiF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Associated Types

type RepK LambdaPiF

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK LambdaPiF = D1 ('MetaData "LambdaPiF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "AppF" 'PrefixI 'False) (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 "LamF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type) Type)))) :+: (C1 ('MetaCons "PiF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type) Type))) :+: C1 ('MetaCons "UniverseF" 'PrefixI 'False) (U1 :: LoT (Type -> Type -> Type) -> Type)))

Methods

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

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

GenericK (LambdaPiF scope :: Type -> Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Associated Types

type RepK (LambdaPiF scope :: Type -> Type)

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK (LambdaPiF scope :: Type -> Type) = D1 ('MetaData "LambdaPiF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "AppF" 'PrefixI 'False) (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 "LamF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom (Type -> Type) Type)))) :+: (C1 ('MetaCons "PiF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom (Type -> Type) Type))) :+: C1 ('MetaCons "UniverseF" 'PrefixI 'False) (U1 :: LoT (Type -> Type) -> Type)))

Methods

fromK :: forall (x :: LoT (Type -> Type)). (LambdaPiF scope :@@: x) -> RepK (LambdaPiF scope) x #

toK :: forall (x :: LoT (Type -> Type)). RepK (LambdaPiF scope) x -> LambdaPiF scope :@@: x #

type RepK (LambdaPiF scope term :: Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK (LambdaPiF scope term :: Type) = D1 ('MetaData "LambdaPiF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "AppF" 'PrefixI 'False) (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 "LamF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom Type Type)))) :+: (C1 ('MetaCons "PiF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom Type Type))) :+: C1 ('MetaCons "UniverseF" 'PrefixI 'False) (U1 :: LoT Type -> Type)))

type RepK LambdaPiF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK LambdaPiF = D1 ('MetaData "LambdaPiF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "AppF" 'PrefixI 'False) (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 "LamF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type) Type)))) :+: (C1 ('MetaCons "PiF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type -> Type) Type))) :+: C1 ('MetaCons "UniverseF" 'PrefixI 'False) (U1 :: LoT (Type -> Type -> Type) -> Type)))

type RepK (LambdaPiF scope :: Type -> Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK (LambdaPiF scope :: Type -> Type) = D1 ('MetaData "LambdaPiF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "AppF" 'PrefixI 'False) (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 "LamF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom (Type -> Type) Type)))) :+: (C1 ('MetaCons "PiF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon scope :: Atom (Type -> Type) Type))) :+: C1 ('MetaCons "UniverseF" 'PrefixI 'False) (U1 :: LoT (Type -> Type) -> Type)))

data PairF scope term Source #

The signature Bifunctor for pairs.

Constructors

PairF term term	Pair: $\langle t_1, t_2 \rangle$
FirstF term	First projection: $\pi_1(t)$
SecondF term	Second projection: $\pi_2(t)$
ProductF term term	Product type (non-dependent): $T_1 \times T_2$

Instances

Instances details

Bifoldable PairF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

bifold :: Monoid m => PairF m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> PairF a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> PairF a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> PairF a b -> c #

Bifunctor PairF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

bimap :: (a -> b) -> (c -> d) -> PairF a c -> PairF b d #

first :: (a -> b) -> PairF a c -> PairF b c #

second :: (b -> c) -> PairF a b -> PairF a c #

Bitraversable PairF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> PairF a b -> f (PairF c d) #

GenericK (PairF scope term :: Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Associated Types

type RepK (PairF scope term :: Type)

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK (PairF scope term :: Type) = D1 ('MetaData "PairF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "PairF" 'PrefixI 'False) (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 "FirstF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)))) :+: (C1 ('MetaCons "SecondF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type))) :+: C1 ('MetaCons "ProductF" 'PrefixI 'False) (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). (PairF scope term :@@: x) -> RepK (PairF scope term) x #

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

Foldable (PairF scope) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

fold :: Monoid m => PairF scope m -> m #

foldMap :: Monoid m => (a -> m) -> PairF scope a -> m #

foldMap' :: Monoid m => (a -> m) -> PairF scope a -> m #

foldr :: (a -> b -> b) -> b -> PairF scope a -> b #

foldr' :: (a -> b -> b) -> b -> PairF scope a -> b #

foldl :: (b -> a -> b) -> b -> PairF scope a -> b #

foldl' :: (b -> a -> b) -> b -> PairF scope a -> b #

foldr1 :: (a -> a -> a) -> PairF scope a -> a #

foldl1 :: (a -> a -> a) -> PairF scope a -> a #

toList :: PairF scope a -> [a] #

null :: PairF scope a -> Bool #

length :: PairF scope a -> Int #

elem :: Eq a => a -> PairF scope a -> Bool #

maximum :: Ord a => PairF scope a -> a #

minimum :: Ord a => PairF scope a -> a #

sum :: Num a => PairF scope a -> a #

product :: Num a => PairF scope a -> a #

IsString (LambdaPi 'VoidS) Source #

$\lambda\Pi$-terms can be (unsafely) parsed from a String via Term.

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

fromString :: String -> LambdaPi 'VoidS #

Traversable (PairF scope) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

traverse :: Applicative f => (a -> f b) -> PairF scope a -> f (PairF scope b) #

sequenceA :: Applicative f => PairF scope (f a) -> f (PairF scope a) #

mapM :: Monad m => (a -> m b) -> PairF scope a -> m (PairF scope b) #

sequence :: Monad m => PairF scope (m a) -> m (PairF scope a) #

Functor (PairF scope) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

fmap :: (a -> b) -> PairF scope a -> PairF scope b #

(<$) :: a -> PairF scope b -> PairF scope a #

Show (LambdaPi 'VoidS) Source #

$\lambda\Pi$-terms are pretty-printed using BNFC-generated printer via Term.

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

showsPrec :: Int -> LambdaPi 'VoidS -> ShowS #

show :: LambdaPi 'VoidS -> String #

showList :: [LambdaPi 'VoidS] -> ShowS #

Show term => Show (PairF scope term) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

showsPrec :: Int -> PairF scope term -> ShowS #

show :: PairF scope term -> String #

showList :: [PairF scope term] -> ShowS #

Eq term => Eq (PairF scope term) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

(==) :: PairF scope term -> PairF scope term -> Bool #

(/=) :: PairF scope term -> PairF scope term -> Bool #

ZipMatchK PairF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Methods

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

GenericK PairF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Associated Types

type RepK PairF

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK PairF = D1 ('MetaData "PairF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "PairF" 'PrefixI 'False) (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 "FirstF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)))) :+: (C1 ('MetaCons "SecondF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type))) :+: C1 ('MetaCons "ProductF" 'PrefixI 'False) (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)). (PairF :@@: x) -> RepK PairF x #

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

GenericK (PairF scope :: Type -> Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

Associated Types

type RepK (PairF scope :: Type -> Type)

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK (PairF scope :: Type -> Type) = D1 ('MetaData "PairF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "PairF" 'PrefixI 'False) (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 "FirstF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)))) :+: (C1 ('MetaCons "SecondF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type))) :+: C1 ('MetaCons "ProductF" 'PrefixI 'False) (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)). (PairF scope :@@: x) -> RepK (PairF scope) x #

toK :: forall (x :: LoT (Type -> Type)). RepK (PairF scope) x -> PairF scope :@@: x #

type RepK (PairF scope term :: Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK (PairF scope term :: Type) = D1 ('MetaData "PairF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "PairF" 'PrefixI 'False) (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 "FirstF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type)))) :+: (C1 ('MetaCons "SecondF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon term :: Atom Type Type))) :+: C1 ('MetaCons "ProductF" 'PrefixI 'False) (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 PairF Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK PairF = D1 ('MetaData "PairF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "PairF" 'PrefixI 'False) (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 "FirstF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type)))) :+: (C1 ('MetaCons "SecondF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var1 :: Atom (Type -> Type -> Type) Type))) :+: C1 ('MetaCons "ProductF" 'PrefixI 'False) (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 (PairF scope :: Type -> Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoil

type RepK (PairF scope :: Type -> Type) = D1 ('MetaData "PairF" "Language.LambdaPi.Impl.FreeFoil" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) ((C1 ('MetaCons "PairF" 'PrefixI 'False) (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 "FirstF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type)))) :+: (C1 ('MetaCons "SecondF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> Type) Type))) :+: C1 ('MetaCons "ProductF" 'PrefixI 'False) (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 (:+:) = Sum :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type Source #

Sum of signature bifunctors.

type LambdaPi (n :: S) = AST NameBinder (LambdaPiF :+: PairF) n Source #

$\lambda\Pi$-terms in scope n, freely generated from the sum of signatures LambdaPiF and PairF.

pattern App :: LambdaPi n -> LambdaPi n -> LambdaPi n Source #

pattern Lam :: () => NameBinder n l -> LambdaPi l -> LambdaPi n Source #

pattern Pi :: () => NameBinder n l -> LambdaPi n -> LambdaPi l -> LambdaPi n Source #

pattern Pair :: LambdaPi n -> LambdaPi n -> LambdaPi n Source #

pattern First :: LambdaPi n -> LambdaPi n Source #

pattern Second :: LambdaPi n -> LambdaPi n Source #

pattern Product :: LambdaPi n -> LambdaPi n -> LambdaPi n Source #

pattern Universe :: LambdaPi n Source #

whnf :: forall (n :: S). Distinct n => Scope n -> LambdaPi n -> LambdaPi n Source #

Compute weak head normal form (WHNF) of a $\lambda\Pi$-term.

>>> whnf Foil.emptyScope "(λx.(λ_.x)(λy.x))(λy.λz.z)"
λ x0 . λ x1 . x1

>>> whnf Foil.emptyScope "(λs.λz.s(s(z)))(λs.λz.s(s(z)))"
λ x1 . (λ x0 . λ x1 . x0 (x0 x1)) ((λ x0 . λ x1 . x0 (x0 x1)) x1)

Note that during computation bound variables can become unordered in the sense that binders may easily repeat or decrease. For example, in the following expression, inner binder has lower index that the outer one:

>>> whnf Foil.emptyScope "(λx.λy.x)(λx.x)"
λ x1 . λ x0 . x0

At the same time, without substitution, we get regular, increasing binder indices:

>>> "λx.λy.y" :: LambdaPi Foil.VoidS
λ x0 . λ x1 . x1

To compare terms for $\alpha$-equivalence, we may use alphaEquiv:

>>> alphaEquiv Foil.emptyScope (whnf Foil.emptyScope "(λx.λy.x)(λx.x)") "λx.λy.y"
True

We may also normalize binders using refreshAST:

>>> refreshAST Foil.emptyScope (whnf Foil.emptyScope "(λx.λy.x)(λx.x)")
λ x0 . λ x1 . x1

toLambdaPiLam Source #

Arguments

:: forall (n :: S). Distinct n
=> Scope n	Target scope of the $\lambda\Pi$-term.
-> Map VarIdent (Name n)	Mapping for the free variables in the raw term.
-> Pattern	Raw pattern (argument) of the $\lambda$-abstraction.
-> ScopedTerm	Raw body of the $\lambda$-abstraction.
-> LambdaPi n

Convert a raw $\lambda$-abstraction into a scope-safe $\lambda\Pi$-term.

toLambdaPiPi Source #

Arguments

:: forall (n :: S). Distinct n
=> Scope n	Target scope of the $\lambda\Pi$-term.
-> Map VarIdent (Name n)	Mapping for the free variables in the raw term.
-> Pattern	Raw argument pattern of the $\Pi$-type.
-> Term	Raw argument type of the $\Pi$-type.
-> ScopedTerm	Raw body (result type family) of the $\Pi$-type.
-> LambdaPi n

Convert a raw $\Pi$-type into a scope-safe $\lambda\Pi$-term.

toLambdaPi Source #

Arguments

:: forall (n :: S). Distinct n
=> Scope n	Target scope of the $\lambda\Pi$-term.
-> Map VarIdent (Name n)	Mapping for the free variables in the raw term.
-> Term	Raw expression or type.
-> LambdaPi n

Convert a raw expression into a scope-safe $\lambda\Pi$-term.

toLambdaPiClosed :: Term -> LambdaPi 'VoidS Source #

Convert a raw expression into a closed scope-safe $\lambda\Pi$-term.

fromLambdaPi Source #

Arguments

:: forall (n :: S). [VarIdent]	Stream of fresh raw identifiers.
-> NameMap n VarIdent	A total map for all names in scope `n`.
-> LambdaPi n	A scope-safe $\lambda\Pi$-term.
-> Term

Convert back from a scope-safe $\lambda\Pi$-term into a raw expression or type.

fromLambdaPi' Source #

Arguments

:: forall (n :: S). LambdaPi n	A scope-safe $\lambda\Pi$-term.
-> Term

Convert back from a scope-safe $\lambda\Pi$-term into a raw expression or type.

In contrast to fromLambdaPi, this function uses the raw foil identifiers (integers) to generate names for the variables. This makes them transparent when printing.

ppLambdaPi :: LambdaPi 'VoidS -> String Source #

Pretty-print a closed $\lambda\Pi$-term.

interpretCommand :: Command -> IO () Source #

Interpret a $\lambda\Pi$ command.

interpretProgram :: Program -> IO () Source #

Interpret a $\lambda\Pi$ program.

defaultMain :: IO () Source #

A $\lambda\Pi$ interpreter implemented via the free foil.

AppF term term	Application: \((t_1 \; t_2)\)
LamF scope	Abstraction: \(\lambda x. t\)
PiF term scope	Dependent function type: \(\prod_{x : T_1} T_2\)
UniverseF	Universe (type of types): \(\mathcal{U}\)

PairF term term	Pair: \(\langle t_1, t_2 \rangle\)
FirstF term	First projection: \(\pi_1(t)\)
SecondF term	Second projection: \(\pi_2(t)\)
ProductF term term	Product type (non-dependent): \(T_1 \times T_2\)

:: forall (n :: S). Distinct n
=> Scope n	Target scope of the \(\lambda\Pi\)-term.
-> Map VarIdent (Name n)	Mapping for the free variables in the raw term.
-> Pattern	Raw pattern (argument) of the \(\lambda\)-abstraction.
-> ScopedTerm	Raw body of the \(\lambda\)-abstraction.
-> LambdaPi n

:: forall (n :: S). LambdaPi n	A scope-safe \(\lambda\Pi\)-term.
-> Term