Safe Haskell	None
Language	Haskell2010

Language.LambdaPi.Impl.FoilTH

Contents

Generated code
User-defined

Description

Foil implementation of the \(\lambda\Pi\)-calculus (with pairs) using Template Haskell to reduce boilerplate.

Template Haskell helpers generate the following:

Scope-safe AST, generated from a raw definition. See FoilTerm, FoilScopedTerm, and FoilPattern.
Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see toFoilTerm and fromFoilTerm.
Helper functions for patterns. See extendScopeFoilPattern and withRefreshedFoilPattern.

The following is implemented manually in this module:

Correct capture-avoiding substitution (see substitute).
Computation of weak head normal form (WHNF), see whnf.
Entry point, gluing everything together. See defaultMain.

The following is not implemented:

α-equivalence checks and α-normalization helpers.

This implementation supports (nested) patterns for pairs.

Synopsis

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
data FoilScopedTerm' a (n :: S) = FoilAScopedTerm a (FoilTerm' a n)
data FoilTerm' a (n :: S) where
- FoilVar :: forall a (n :: S). a -> Name n -> FoilTerm' a n
- FoilPi :: forall a (n :: S) (l :: S). a -> FoilPattern' a n l -> FoilTerm' a n -> FoilScopedTerm' a l -> FoilTerm' a n
- FoilLam :: forall a (n :: S) (l :: S). a -> FoilPattern' a n l -> FoilScopedTerm' a l -> FoilTerm' a n
- FoilApp :: forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n -> FoilTerm' a n
- FoilProduct :: forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n -> FoilTerm' a n
- FoilPair :: forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n -> FoilTerm' a n
- FoilFirst :: forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n
- FoilSecond :: forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n
- FoilUniverse :: forall a (n :: S). a -> FoilTerm' a n
extendScopeFoilPattern' :: forall a (n :: S) (l :: S). FoilPattern' a n l -> Scope n -> Scope l
withRefreshedFoilPattern' :: forall a (o :: S) (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, InjectName e, Sinkable e) => Scope o -> FoilPattern' a n l -> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> FoilPattern' a o o' -> r) -> r
toFoilTerm' :: forall (n :: S) a. Distinct n => Scope n -> Map VarIdent (Name n) -> Term' a -> FoilTerm' a n
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
toFoilScopedTerm' :: forall (n :: S) a. Distinct n => Scope n -> Map VarIdent (Name n) -> ScopedTerm' a -> FoilScopedTerm' a n
fromFoilTerm' :: forall (n :: S) a. [VarIdent] -> NameMap n VarIdent -> FoilTerm' a n -> Term' a
fromFoilPattern' :: forall (n :: S) a (l :: S) r. [VarIdent] -> NameMap n VarIdent -> FoilPattern' a n l -> ([VarIdent] -> NameMap l VarIdent -> Pattern' a -> r) -> r
fromFoilScopedTerm' :: forall (n :: S) a. [VarIdent] -> NameMap n VarIdent -> FoilScopedTerm' a n -> ScopedTerm' a
type FoilTerm = FoilTerm' BNFC'Position
type FoilPattern = FoilPattern' BNFC'Position
fromFoilTermClosed :: [VarIdent] -> FoilTerm 'VoidS -> Term
substitute :: forall (o :: S) (i :: S). Distinct o => Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
matchPattern :: forall (n :: S) (l :: S). FoilPattern n l -> FoilTerm n -> Substitution FoilTerm l n
whnf :: forall (n :: S). Distinct n => Scope n -> FoilTerm n -> FoilTerm n
interpretCommand :: Command -> IO ()
interpretProgram :: Program -> IO ()
defaultMain :: IO ()
printFoilTerm :: FoilTerm 'VoidS -> String

Generated code

Scope-safe AST

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

Constructors

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

Instances

Instances details

CoSinkable (FoilPattern' a) Source #
Instance details Defined in Language.LambdaPi.Impl.FoilTH 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 #

data FoilScopedTerm' a (n :: S) Source #

Constructors

FoilAScopedTerm a (FoilTerm' a n)

Instances

Instances details

Sinkable (FoilScopedTerm' a) Source #
Instance details Defined in Language.LambdaPi.Impl.FoilTH Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> FoilScopedTerm' a n -> FoilScopedTerm' a l #

data FoilTerm' a (n :: S) where Source #

Constructors

FoilVar :: forall a (n :: S). a -> Name n -> FoilTerm' a n
FoilPi :: forall a (n :: S) (l :: S). a -> FoilPattern' a n l -> FoilTerm' a n -> FoilScopedTerm' a l -> FoilTerm' a n
FoilLam :: forall a (n :: S) (l :: S). a -> FoilPattern' a n l -> FoilScopedTerm' a l -> FoilTerm' a n
FoilApp :: forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n -> FoilTerm' a n
FoilProduct :: forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n -> FoilTerm' a n
FoilPair :: forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n -> FoilTerm' a n
FoilFirst :: forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n
FoilSecond :: forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n
FoilUniverse :: forall a (n :: S). a -> FoilTerm' a n

Instances

Instances details

InjectName (FoilTerm' a) Source #
Instance details Defined in Language.LambdaPi.Impl.FoilTH Methods injectName :: forall (n :: S). Name n -> FoilTerm' a n #
Sinkable (FoilTerm' a) Source #
Instance details Defined in Language.LambdaPi.Impl.FoilTH Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> FoilTerm' a n -> FoilTerm' a l #

Conversion from raw to scope-safe AST

extendScopeFoilPattern' :: forall a (n :: S) (l :: S). FoilPattern' a n l -> Scope n -> Scope l Source #

Extend a scope with the names bound by the given pattern. This is a more flexible version of extendScope.

withRefreshedFoilPattern' :: forall a (o :: S) (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, InjectName e, Sinkable e) => Scope o -> FoilPattern' a n l -> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> FoilPattern' a o o' -> r) -> r Source #

Refresh (if needed) bound variables introduced in a pattern. This is a more flexible version of withRefreshed.

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

Convert a raw term into a scope-safe term.

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 #

Convert a raw pattern into a scope-safe pattern.

toFoilScopedTerm' :: forall (n :: S) a. Distinct n => Scope n -> Map VarIdent (Name n) -> ScopedTerm' a -> FoilScopedTerm' a n Source #

Convert a raw scoped term into a scope-safe scoped term.

Conversion from scope-safe to raw AST

fromFoilTerm' :: forall (n :: S) a. [VarIdent] -> NameMap n VarIdent -> FoilTerm' a n -> Term' a Source #

Convert a scope-safe term into a raw term.

fromFoilPattern' :: forall (n :: S) a (l :: S) r. [VarIdent] -> NameMap n VarIdent -> FoilPattern' a n l -> ([VarIdent] -> NameMap l VarIdent -> Pattern' a -> r) -> r Source #

Convert a scope-safe pattern into a raw pattern.

fromFoilScopedTerm' :: forall (n :: S) a. [VarIdent] -> NameMap n VarIdent -> FoilScopedTerm' a n -> ScopedTerm' a Source #

Convert a scope-safe scoped term into a raw scoped term.

type FoilTerm = FoilTerm' BNFC'Position Source #

type FoilPattern = FoilPattern' BNFC'Position Source #

fromFoilTermClosed Source #

Arguments

:: [VarIdent]	A stream of fresh variable identifiers.
-> FoilTerm 'VoidS	A scope safe term in scope `n`.
-> Term

Convert a closed scope-safe term into a raw term.

User-defined

Substitution

substitute :: forall (o :: S) (i :: S). Distinct o => Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o Source #

Perform substitution in a \(\lambda\Pi\)-term.

Computation

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

Match a pattern against an expression.

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

Compute weak head normal form (WHNF).

Interpreter

interpretCommand :: Command -> IO () Source #

Interpret a λΠ command.

interpretProgram :: Program -> IO () Source #

Interpret a λΠ program.

defaultMain :: IO () Source #

Default interpreter program. Reads a λΠ program from the standard input and runs the commands.

Pretty-printing

printFoilTerm :: FoilTerm 'VoidS -> String Source #

Pretty-print a closed scode-safe \(\lambda\Pi\)-term using BNFC-generated printer (via Term).