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 and Generics.Kind 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 provided via kind-polymophic generics (see Generics.Kind):

Sinkable instance for FoilTerm'.
CoSinkable instance for FoilPattern', giving access to extendScopePattern and withRefreshedPattern (among other utilities).

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

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Associated Types

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

type RepK (FoilPattern' a n l :: Type) = D1 ('MetaData "FoilPattern'" "Language.LambdaPi.Impl.FoilTH" "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.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 #

HasNameBinders (FoilPattern' a) Source #

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

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]) #

GenericK FoilPattern' Source #

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Associated Types

type RepK FoilPattern'

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

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.FoilTH

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.FoilTH

Associated Types

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

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.FoilTH

Associated Types

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

type RepK (FoilPattern' a n :: S -> Type) = D1 ('MetaData "FoilPattern'" "Language.LambdaPi.Impl.FoilTH" "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 #

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

type RepK (FoilPattern' a n l :: Type) = D1 ('MetaData "FoilPattern'" "Language.LambdaPi.Impl.FoilTH" "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.FoilTH

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

type RepK (FoilPattern' a n :: S -> Type) = D1 ('MetaData "FoilPattern'" "Language.LambdaPi.Impl.FoilTH" "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))))))))

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

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

Constructors

FoilAScopedTerm a (FoilTerm' a n)

Instances

Instances details

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Methods

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

GenericK (FoilScopedTerm' a n :: Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Associated Types

type RepK (FoilScopedTerm' a n :: Type)

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

type RepK (FoilScopedTerm' a n :: Type) = D1 ('MetaData "FoilScopedTerm'" "Language.LambdaPi.Impl.FoilTH" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) (C1 ('MetaCons "FoilAScopedTerm" '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 (FoilTerm' a n) :: Atom Type Type))))

Methods

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

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

GenericK FoilScopedTerm' Source #

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Associated Types

type RepK FoilScopedTerm'

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

type RepK FoilScopedTerm' = D1 ('MetaData "FoilScopedTerm'" "Language.LambdaPi.Impl.FoilTH" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) (C1 ('MetaCons "FoilAScopedTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> S -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon FoilTerm' :: Atom (Type -> S -> Type) (Type -> S -> Type)) ':@: (Var0 :: Atom (Type -> S -> Type) Type)) ':@: (Var1 :: Atom (Type -> S -> Type) S)))))

Methods

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

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

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Associated Types

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

type RepK (FoilScopedTerm' a :: S -> Type) = D1 ('MetaData "FoilScopedTerm'" "Language.LambdaPi.Impl.FoilTH" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) (C1 ('MetaCons "FoilAScopedTerm" '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 (FoilTerm' a) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)))))

Methods

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

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

type RepK (FoilScopedTerm' a n :: Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

type RepK (FoilScopedTerm' a n :: Type) = D1 ('MetaData "FoilScopedTerm'" "Language.LambdaPi.Impl.FoilTH" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) (C1 ('MetaCons "FoilAScopedTerm" '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 (FoilTerm' a n) :: Atom Type Type))))

type RepK FoilScopedTerm' Source #

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

type RepK FoilScopedTerm' = D1 ('MetaData "FoilScopedTerm'" "Language.LambdaPi.Impl.FoilTH" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) (C1 ('MetaCons "FoilAScopedTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field (Var0 :: Atom (Type -> S -> Type) Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Field ((('Kon FoilTerm' :: Atom (Type -> S -> Type) (Type -> S -> Type)) ':@: (Var0 :: Atom (Type -> S -> Type) Type)) ':@: (Var1 :: Atom (Type -> S -> Type) S)))))

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

type RepK (FoilScopedTerm' a :: S -> Type) = D1 ('MetaData "FoilScopedTerm'" "Language.LambdaPi.Impl.FoilTH" "lambda-pi-0.2.0-5DHIXViRYMqFeHcab75Oc" 'False) (C1 ('MetaCons "FoilAScopedTerm" '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 (FoilTerm' a) :: Atom (S -> Type) (S -> Type)) ':@: (Var0 :: Atom (S -> Type) S)))))

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

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Methods

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

GenericK (FoilTerm' a n :: Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Associated Types

type RepK (FoilTerm' a n :: Type)

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Methods

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

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

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 #

GenericK FoilTerm' Source #

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Associated Types

type RepK FoilTerm'

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Methods

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

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

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Associated Types

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

Methods

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

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

type RepK (FoilTerm' a n :: Type) Source #

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

type RepK FoilTerm' Source #

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

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

Instance details

Defined in Language.LambdaPi.Impl.FoilTH

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).