lambda-cube-0.3.0: Some thoughts on Calculus of Constructions

Safe Haskell	None
Language	Haskell2010

L3.Loader.Loader

Description

Load and parse '.l3' files

Synopsis

wrapPrelude :: [(FilePath, ByteString)] -> (ShowCtx, ShowExpr -> ShowExpr)
embeddedPrelude :: [(FilePath, ByteString)]
embeddedPreludeIO :: IO [(FilePath, ByteString)]
takeDirectoryName :: FilePath -> String
takeNamespacedFileName :: FilePath -> String
loadPrelude :: [(FilePath, ByteString)] -> (ShowCtx, ShowCtx)
tauSubst :: (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
tauNorm :: (Eq a, Enum a, Show a) => Expr a -> Expr a

Documentation

wrapPrelude :: [(FilePath, ByteString)] -> (ShowCtx, ShowExpr -> ShowExpr) Source #

Fold the prelude context through lambda application into a type-context and expression-context-mapper. That is, `let a = x in b` = `(λ a -> b) x`

embeddedPrelude :: [(FilePath, ByteString)] Source #

Embed and retrieve all '.l3' files in the prelude directory

embeddedPreludeIO :: IO [(FilePath, ByteString)] Source #

takeDirectoryName :: FilePath -> String Source #

Get the last directory name from a path

takeNamespacedFileName :: FilePath -> String Source #

Format a file into either non-namespaced file or namespaced dir@file

loadPrelude :: [(FilePath, ByteString)] -> (ShowCtx, ShowCtx) Source #

Lex and parse the prelude into a type-context and expression-context

tauSubst :: (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a Source #

Substitute all occurrences of a variable v with an expression e, but only where v appears in a type.

tauNorm :: (Eq a, Enum a, Show a) => Expr a -> Expr a Source #

Partially evaluate the types of an expression through lambda-application substitutions. This should remain correct, but allows for binding types and evaluating by-reference.