Safe Haskell	None
Language	Haskell2010

Language.LambdaPi.Impl.FreeFoilTH

Contents

Generated code
User-defined code
Orphan instances

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 provided via generic representation via kind-generics (see Generics.Kind): 1. ZipMatch instances for signatures (enabling general $\alpha$-equivalence). 2. Sinkable instances for terms. 3. CoSinkable instances for patterns.

The following is generated using Template Haskell:

Signature bifunctor for terms.
Convenient pattern synonyms.
Conversion between scope-safe and raw term representation.

The following is implemented manually in this module:

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.

Synopsis

data Term'Sig a scope term
- = PiSig a term scope
- | LamSig a scope
- | AppSig a term term
- | ProductSig a term term
- | PairSig a term term
- | FirstSig a term
- | SecondSig a term
- | UniverseSig a
pattern Universe :: a -> AST binder (Term'Sig a) n
pattern Second :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n
pattern First :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n
pattern Pair :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n
pattern Product :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n
pattern App :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n
pattern Lam :: () => a -> binder n l1 -> AST binder (Term'Sig a) l1 -> AST binder (Term'Sig a) n
pattern Pi :: () => a -> AST binder (Term'Sig a) n -> binder n l2 -> AST binder (Term'Sig a) l2 -> AST binder (Term'Sig a) n
convertToTerm'Sig :: Term' a -> Either VarIdent (Term'Sig a (Pattern' a, ScopedTerm' a) (Term' a))
getPattern'Binder :: Pattern' a -> Maybe VarIdent
getTerm'FromScopedTerm' :: ScopedTerm' a -> Term' a
convertFromTerm'Sig :: Term'Sig a (Pattern' a, ScopedTerm' a) (Term' a) -> Term' a
data FoilPattern' a (n :: S) (l :: S) where
- FoilPatternWildcard :: forall a (n :: S). a -> FoilPattern' a n n
- FoilPatternVar :: forall a (n :: S) (l :: S). a -> NameBinder n l -> FoilPattern' a n l
- FoilPatternPair :: forall a (n :: S) (n2 :: S) (l :: S). a -> FoilPattern' a n n2 -> FoilPattern' a n2 l -> FoilPattern' a n l
toFoilPattern' :: forall (n :: S) a r. Distinct n => Scope n -> Map VarIdent (Name n) -> Pattern' a -> (forall (l :: S). DExt n l => FoilPattern' a n l -> Map VarIdent (Name l) -> r) -> r
fromFoilPattern' :: forall a (n :: S) (l :: S). (Int -> VarIdent) -> FoilPattern' a n l -> Pattern' a
type Term' a = AST (FoilPattern' a) (Term'Sig a)
type Term = Term' BNFC'Position
type FoilPattern = FoilPattern' BNFC'Position
toTerm' :: forall (n :: S) a. Distinct n => Scope n -> Map VarIdent (Name n) -> Term' a -> Term' a n
toTerm'Closed :: Term' a -> Term' a 'VoidS
fromTerm' :: forall a (n :: S). Term' a n -> Term' a
matchPattern :: forall (n :: S) (l :: S). FoilPattern n l -> Term n -> Substitution Term l n
whnf :: forall (n :: S). Distinct n => Scope n -> Term n -> Term n
interpretCommand :: Command -> IO ()
interpretProgram :: Program -> IO ()
defaultMain :: IO ()

Documentation

>>> :set -XOverloadedStrings
>>> :set -XDataKinds
>>> import qualified Control.Monad.Foil as Foil
>>> import Control.Monad.Free.Foil
>>> import Data.String (fromString)

Generated code

Signature

data Term'Sig a scope term Source #

Generated with mkSignature. A signature bifunctor, specifying the nodes of a syntax tree corresponding to Term'.

Constructors

PiSig a term scope	Corresponds to `Pi`.
LamSig a scope	Corresponds to `Lam`.
AppSig a term term	Corresponds to `App`.
ProductSig a term term	Corresponds to `Product`.
PairSig a term term	Corresponds to `Pair`.
FirstSig a term	Corresponds to `First`.
SecondSig a term	Corresponds to `Second`.
UniverseSig a	Corresponds to `Universe`.

Instances

Instances details

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Associated Types

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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.LambdaPi.Impl.FreeFoilTH

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.LambdaPi.Impl.FreeFoilTH

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.LambdaPi.Impl.FreeFoilTH

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.LambdaPi.Impl.FreeFoilTH

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 #

Traversable (Term'Sig a scope) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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.LambdaPi.Impl.FreeFoilTH

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 #

GenericK Term'Sig Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Associated Types

type RepK Term'Sig

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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 #

Generic ZipMatchK instance.

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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.LambdaPi.Impl.FreeFoilTH

Associated Types

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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.LambdaPi.Impl.FreeFoilTH

Associated Types

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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 #

IsString (AST FoilPattern (Term'Sig BNFC'Position) 'VoidS) Source #

Parse scope-safe terms via raw representation.

>>> fromString "λx.λy.λx.x" :: Term Foil.VoidS
λ x0 . λ x1 . λ x2 . x2

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Methods

fromString :: String -> AST FoilPattern (Term'Sig BNFC'Position) 'VoidS #

Generic (Term'Sig a scope term) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Associated Types

type Rep (Term'Sig a scope term)

Deriving Generic and GenericK instances.

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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 #

Show (AST (FoilPattern' a) (Term'Sig a) 'VoidS) Source #

Pretty-print scope-safe terms via raw representation.

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Methods

showsPrec :: Int -> AST (FoilPattern' a) (Term'Sig a) 'VoidS -> ShowS #

show :: AST (FoilPattern' a) (Term'Sig a) 'VoidS -> String #

showList :: [AST (FoilPattern' a) (Term'Sig a) 'VoidS] -> ShowS #

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

type RepK Term'Sig Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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

Deriving Generic and GenericK instances.

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Pattern synonyms

pattern Universe :: a -> AST binder (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type UniverseSig.

pattern Second :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type SecondSig.

pattern First :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type FirstSig.

pattern Pair :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type PairSig.

pattern Product :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type ProductSig.

pattern App :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type AppSig.

pattern Lam :: () => a -> binder n l1 -> AST binder (Term'Sig a) l1 -> AST binder (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type LamSig.

pattern Pi :: () => a -> AST binder (Term'Sig a) n -> binder n l2 -> AST binder (Term'Sig a) l2 -> AST binder (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type PiSig.

Conversion helpers

convertToTerm'Sig :: Term' a -> Either VarIdent (Term'Sig a (Pattern' a, ScopedTerm' a) (Term' a)) Source #

Generated with mkConvertToSig. Perform one step of converting Term', peeling off one node of type Term'Sig.

getPattern'Binder :: Pattern' a -> Maybe VarIdent Source #

Generated with mkGetPatternBinder. Extract at most one binder from a pattern or crash.

getTerm'FromScopedTerm' :: ScopedTerm' a -> Term' a Source #

Generated with mkGetScopedTerm. Extract scoped term or crash.

convertFromTerm'Sig :: Term'Sig a (Pattern' a, ScopedTerm' a) (Term' a) -> Term' a Source #

Generated with mkConvertFromSig. Perform one step of converting Term', peeling off one node of type Term'Sig.

Scope-safe patterns

data FoilPattern' a (n :: S) (l :: S) where Source #

Generated with mkFoilPattern. A scope-safe version of Pattern'.

Constructors

FoilPatternWildcard :: forall a (n :: S). a -> FoilPattern' a n n	Corresponds to `PatternWildcard`.
FoilPatternVar :: forall a (n :: S) (l :: S). a -> NameBinder n l -> FoilPattern' a n l	Corresponds to `PatternVar`.
FoilPatternPair :: forall a (n :: S) (n2 :: S) (l :: S). a -> FoilPattern' a n n2 -> FoilPattern' a n2 l -> FoilPattern' a n l	Corresponds to `PatternPair`.

Instances

Instances details

GenericK (FoilPattern' a n l :: Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Associated Types

type RepK (FoilPattern' a n l :: Type)

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

type RepK (FoilPattern' a n l :: Type) = D1 ('MetaData "FoilPattern'" "Language.LambdaPi.Impl.FreeFoilTH" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) (C1 ('MetaCons "FoilPatternWildcard" 'PrefixI 'False) (('Kon (n ~~ l) :: Atom Type Constraint) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type))) :+: (C1 ('MetaCons "FoilPatternVar" '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 (NameBinder n l) :: Atom Type Type))) :+: C1 ('MetaCons "FoilPatternPair" '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 (FoilPattern' a n) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (FoilPattern' a) :: Atom (S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)) ':@: ('Kon l :: Atom (S -> Type) S))))))))

Methods

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

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

CoSinkable (FoilPattern' a) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> FoilPattern' a n l -> (forall (l' :: S). (Name l -> Name l') -> FoilPattern' 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 -> FoilPattern' a n l -> (forall (o' :: S). DExt o o' => f n l o o' -> FoilPattern' a o o' -> r) -> r #

HasNameBinders (FoilPattern' a) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Methods

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

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

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

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

UnifiablePattern (FoilPattern' a) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Methods

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

GenericK FoilPattern' Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Associated Types

type RepK FoilPattern'

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Methods

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

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

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Methods

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

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Associated Types

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Methods

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

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

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Associated Types

type RepK (FoilPattern' a n :: S -> Type)

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

type RepK (FoilPattern' a n :: S -> Type) = D1 ('MetaData "FoilPattern'" "Language.LambdaPi.Impl.FreeFoilTH" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) (C1 ('MetaCons "FoilPatternWildcard" 'PrefixI 'False) ((('Kon ((~~) n :: 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 "FoilPatternVar" 'PrefixI 'False) (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 n) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)))) :+: C1 ('MetaCons "FoilPatternPair" '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 (FoilPattern' a n) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (FoilPattern' 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)). (FoilPattern' a n :@@: x) -> RepK (FoilPattern' a n) x #

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

IsString (AST FoilPattern (Term'Sig BNFC'Position) 'VoidS) Source #

Parse scope-safe terms via raw representation.

>>> fromString "λx.λy.λx.x" :: Term Foil.VoidS
λ x0 . λ x1 . λ x2 . x2

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Methods

fromString :: String -> AST FoilPattern (Term'Sig BNFC'Position) 'VoidS #

Show (AST (FoilPattern' a) (Term'Sig a) 'VoidS) Source #

Pretty-print scope-safe terms via raw representation.

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

Methods

showsPrec :: Int -> AST (FoilPattern' a) (Term'Sig a) 'VoidS -> ShowS #

show :: AST (FoilPattern' a) (Term'Sig a) 'VoidS -> String #

showList :: [AST (FoilPattern' a) (Term'Sig a) 'VoidS] -> ShowS #

type RepK (FoilPattern' a n l :: Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

type RepK (FoilPattern' a n l :: Type) = D1 ('MetaData "FoilPattern'" "Language.LambdaPi.Impl.FreeFoilTH" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) (C1 ('MetaCons "FoilPatternWildcard" 'PrefixI 'False) (('Kon (n ~~ l) :: Atom Type Constraint) :=>: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ('Kon a :: Atom Type Type))) :+: (C1 ('MetaCons "FoilPatternVar" '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 (NameBinder n l) :: Atom Type Type))) :+: C1 ('MetaCons "FoilPatternPair" '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 (FoilPattern' a n) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (FoilPattern' a) :: Atom (S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)) ':@: ('Kon l :: Atom (S -> Type) S))))))))

type RepK FoilPattern' Source #

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

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

Instance details

Defined in Language.LambdaPi.Impl.FreeFoilTH

type RepK (FoilPattern' a n :: S -> Type) = D1 ('MetaData "FoilPattern'" "Language.LambdaPi.Impl.FreeFoilTH" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) (C1 ('MetaCons "FoilPatternWildcard" 'PrefixI 'False) ((('Kon ((~~) n :: 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 "FoilPatternVar" 'PrefixI 'False) (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 n) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)))) :+: C1 ('MetaCons "FoilPatternPair" '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 (FoilPattern' a n) :: Atom (S -> S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon (FoilPattern' a) :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var0 :: Atom (S -> S -> Type) S)) ':@: (Var1 :: Atom (S -> S -> Type) S))))))))

toFoilPattern' :: forall (n :: S) a r. Distinct n => Scope n -> Map VarIdent (Name n) -> Pattern' a -> (forall (l :: S). DExt n l => FoilPattern' a n l -> Map VarIdent (Name l) -> r) -> r Source #

Generated with mkToFoilPattern. Convert a raw pattern into a scope-safe pattern.

fromFoilPattern' :: forall a (n :: S) (l :: S). (Int -> VarIdent) -> FoilPattern' a n l -> Pattern' a Source #

Generated with mkFromFoilPattern. Convert a scope-safe pattern into a raw pattern.

User-defined code

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

Generic annotated scope-safe $\lambda\Pi$-terms with patterns.

type Term = Term' BNFC'Position Source #

Scode-safe $\lambda\Pi$-terms annotated with source code position.

type FoilPattern = FoilPattern' BNFC'Position Source #

Scope-safe patterns annotated with source code position.

Conversion helpers

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

Convert Term' into a scope-safe term. This is a special case of convertToAST.

toTerm'Closed :: Term' a -> Term' a 'VoidS Source #

Convert Term' into a closed scope-safe term. This is a special case of toTerm'.

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

Convert a scope-safe representation back into Term'. This is a special case of convertFromAST.

VarIdent names are generated based on the raw identifiers in the underlying foil representation.

This function does not recover location information for variables, patterns, or scoped terms.

Evaluation

matchPattern :: forall (n :: S) (l :: S). FoilPattern n l -> Term n -> Substitution Term l n Source #

Match a pattern against an term.

whnf :: forall (n :: S). Distinct n => Scope n -> Term n -> Term 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" :: Term 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

$\lambda\Pi$-interpreter

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.

Orphan instances

UnifiableInPattern BNFC'Position Source #	Ignoring location information when unifying patterns.
Instance details Methods unifyInPattern :: BNFC'Position -> BNFC'Position -> Bool #
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) #

Documentation

Generated code

Signature

Instances

Pattern synonyms

Conversion helpers

Scope-safe patterns

Instances

User-defined code

Conversion helpers

Evaluation

\(\lambda\Pi\)-interpreter

Orphan instances