-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A bare-bones calculus of constructions -- -- Morte is a typed, purely functional, and strongly normalizing -- intermediate language designed for whole-program super-optimization. -- Use this library to type-check, optimize, parse, pretty-print, -- serialize and deserialize expressions in this intermediate language. -- -- This library also installs an executable that you can use to -- type-check and optimize a morte program. -- -- Morte.Core contains the core calculus of constructions for this -- language -- -- Morte.Lexer contains the alex-generated lexer for -- Morte -- -- Morte.Parser contains the happy-generated parser for -- Morte -- -- Read Morte.Tutorial to learn how to use this library @package morte @version 1.0.0 -- | Lexing logic for the Morte language module Morte.Lexer -- | Convert a text representation of an expression into a stream of tokens -- -- lexExpr keeps track of position and returns the remainder of -- the input if lexing fails. lexExpr :: Text -> Producer Token (State Position) (Maybe Text) -- | Token type, used to communicate between the lexer and parser data Token OpenParen :: Token CloseParen :: Token Colon :: Token At :: Token Star :: Token Box :: Token Arrow :: Token Lambda :: Token Pi :: Token Label :: Text -> Token Number :: Int -> Token EOF :: Token -- | The cursor's location while lexing the text data Position P :: {-# UNPACK #-} !Int -> {-# UNPACK #-} !Int -> Position lineNo :: Position -> {-# UNPACK #-} !Int columnNo :: Position -> {-# UNPACK #-} !Int instance Show Position instance Show Token instance Functor AlexLastAcc -- | This module contains the core calculus for the Morte language. This -- language is a minimalist implementation of the calculus of -- constructions, which is in turn a specific kind of pure type system. -- If you are new to pure type systems you may wish to read "Henk: a -- typed intermediate language". -- -- -- http://research.microsoft.com/en-us/um/people/simonpj/papers/henk.ps.gz -- -- Morte is a strongly normalizing language, meaning that: -- -- -- -- Strong normalization comes at a price: Morte forbids recursion. -- Instead, you must translate all recursion to F-algebras and translate -- all corecursion to F-coalgebras. If you are new to F-(co)algebras then -- you may wish to read Morte.Tutorial or read "Recursive types -- for free!": -- -- -- http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt -- -- Morte is designed to be a super-optimizing intermediate language with -- a simple optimization scheme. You optimize a Morte expression by just -- normalizing the expression. If you normalize a long-lived program -- encoded as an F-coalgebra you typically get a state machine, and if -- you normalize a long-lived program encoded as an F-algebra you -- typically get an unrolled loop. -- -- Strong normalization guarantees that all abstractions encodable in -- Morte are "free", meaning that they may increase your program's -- compile times but they will never increase your program's run time -- because they will normalize to the same code. module Morte.Core -- | Label for a bound variable -- -- The Text field is the variable's name. -- -- The Int field disambiguates variables with the same name. Zero -- is a good default. Non-zero values will appear as a numeric suffix -- when pretty-printing the Var. data Var V :: Text -> Int -> Var -- | Constants for the calculus of constructions -- -- The only axiom is: -- -- 
--    
--
data Const Star :: Const Box :: Const -- | Syntax tree for expressions data Expr -- | 
--   Const c        ~  c
--
Const :: Const -> Expr -- | 
--   Var (V x 0)    ~  x
--   Var (V x n)    ~  x@n
--
Var :: Var -> Expr -- | 
--   Lam x     A b  ~  
--
Lam :: Var -> Expr -> Expr -> Expr -- | 
--   Pi x      A B  ~  ∀(x : A) 
--
Pi :: Var -> Expr -> Expr -> Expr -- | 
--   App f a        ~  f a
--
App :: Expr -> Expr -> Expr -- | Bound variables and their types -- -- Earlier Vars shadow later matching Vars type Context = [(Var, Expr)] -- | Type-check an expression and return the expression's type if -- type-checking suceeds or an error if type-checking fails -- -- typeWith does not necessarily normalize the type since full -- normalization is not necessary for just type-checking. If you actually -- care about the returned type then you may want to normalize it -- afterwards. typeWith :: Context -> Expr -> Either TypeError Expr -- | typeOf is the same as typeWith with an empty context, -- meaning that the expression must be closed (i.e. no free variables), -- otherwise type-checking will fail. typeOf :: Expr -> Either TypeError Expr -- | Reduce an expression to its normal form, performing both beta -- reduction and eta reduction -- -- normalize does not type-check the expression. You may want to -- type-check expressions before normalizing them since normalization can -- convert an ill-typed expression into a well-typed expression. normalize :: Expr -> Expr -- | Pretty-print an expression -- -- The result is a syntactically valid Morte program prettyExpr :: Expr -> Text -- | Pretty-print a type error prettyTypeError :: TypeError -> Text -- | A structured type error that includes context data TypeError TypeError :: Context -> Expr -> TypeMessage -> TypeError context :: TypeError -> Context current :: TypeError -> Expr typeMessage :: TypeError -> TypeMessage -- | The specific type error data TypeMessage UnboundVariable :: TypeMessage InvalidInputType :: Expr -> TypeMessage InvalidOutputType :: Expr -> TypeMessage NotAFunction :: TypeMessage TypeMismatch :: Expr -> Expr -> TypeMessage Untyped :: Const -> TypeMessage instance Typeable TypeMessage instance Typeable TypeError instance Eq Var instance Show Var instance Eq Const instance Show Const instance Bounded Const instance Enum Const instance Show Expr instance Show TypeMessage instance Show TypeError instance Exception TypeError instance IsString Expr instance Binary Expr instance Eq Expr instance Binary Const instance IsString Var instance Binary Var -- | Parsing logic for the Morte language module Morte.Parser -- | Parse an Expr from Text or return a ParseError if -- parsing fails exprFromText :: Text -> Either ParseError Expr -- | Pretty-print a ParseError prettyParseError :: ParseError -> Text -- | Structured type for parsing errors data ParseError ParseError :: Position -> ParseMessage -> ParseError position :: ParseError -> Position parseMessage :: ParseError -> ParseMessage -- | The specific parsing error data ParseMessage -- | Lexing failed, returning the remainder of the text Lexing :: Text -> ParseMessage -- | Parsing failed, returning the invalid token Parsing :: Token -> ParseMessage instance Show ParseMessage instance Show ParseError instance Error ParseMessage -- | Morte is a minimalist implementation of the calculus of constructions -- that comes with a parser, type-checker, optimizer, and pretty-printer. -- -- You can think of Morte as a very low-level intermediate language for -- functional languages. This virtual machine was designed with the -- following design principles, in descending order of importance: -- -- -- -- This library does not provide any front-end or back-end language for -- Morte. These will be provided as separate libraries in the future. -- -- The "Introduction" section walks through basic usage of the compiler -- and library. -- -- The "Desugaring" section explains how to desugar complex abstractions -- to Morte's core calculus. -- -- The "Optimization" section explains how Morte optimizes programs, -- providing several long-form example programs and their optimized -- output. module Morte.Tutorial