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:

\(\alpha\)-equivalence checks and \(\alpha\)-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 #

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

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 #

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 #

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

Generated with mkFoilData. A scope-safe version of ScopedTerm'.

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 #

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

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 #

Generated with mkExtendScopeFoilPattern. 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 #

Generated with mkWithRefreshedFoilPattern. 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 #

Generated with mkToFoilTerm. 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 #

Generated with mkToFoilTerm. 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 #

Generated with mkToFoilTerm. 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 #

Generated with mkFromFoil. 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 #

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

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

Generated with mkFromFoil. 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 \(\lambda\Pi\) command.

interpretProgram :: Program -> IO () Source #

Interpret a \(\lambda\Pi\) program.

defaultMain :: IO () Source #

Default interpreter program. Reads a \(\lambda\Pi\) 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).