-- 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 <tt>morte</tt> program.
--   
--   <a>Morte.Core</a> contains the core calculus of constructions for this
--   language
--   
--   <a>Morte.Lexer</a> contains the <tt>alex</tt>-generated lexer for
--   Morte
--   
--   <a>Morte.Parser</a> contains the parser for Morte
--   
--   Read <a>Morte.Tutorial</a> to learn how to use this library
@package morte
@version 1.6.18


-- | All <a>Context</a>-related operations
module Morte.Context

-- | Bound variable names and their types
--   
--   Variable names may appear more than once in the <a>Context</a>. The
--   <tt>Var</tt> <tt>x@n</tt> refers to the <tt>n</tt>th occurrence of
--   <tt>x</tt> in the <a>Context</a> (using 0-based numbering).
data Context a

-- | An empty context with no key-value pairs
--   
--   <pre>
--   toList empty = []
--   </pre>
empty :: Context a

-- | Add a key-value pair to the <a>Context</a>
insert :: Text -> a -> Context a -> Context a

-- | Lookup a key by name and index
--   
--   <pre>
--   lookup k 0 (insert k v0              ctx ) = Just v0
--   lookup k 1 (insert k v0 (insert k v1 ctx)) = Just v1
--   </pre>
lookup :: Text -> Int -> Context a -> Maybe a

-- | Return all key-value associations as a list
toList :: Context a -> [(Text, a)]
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Morte.Context.Context a)
instance GHC.Base.Functor Morte.Context.Context


-- | 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".
--   
--   
--   <a>http://research.microsoft.com/en-us/um/people/simonpj/papers/henk.ps.gz</a>
--   
--   Morte is a strongly normalizing language, meaning that:
--   
--   <ul>
--   <li>Every expression has a unique normal form computed by
--   <a>normalize</a></li>
--   <li>You test expressions for equality of their normal forms using
--   <a>==</a></li>
--   <li>Equational reasoning preserves normal forms</li>
--   </ul>
--   
--   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 <a>Morte.Tutorial</a> or read "Recursive types
--   for free!":
--   
--   
--   <a>http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt</a>
--   
--   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 <a>Text</a> field is the variable's name (i.e. "<tt>x</tt>").
--   
--   The <a>Int</a> field disambiguates variables with the same name if
--   there are multiple bound variables of the same name in scope. Zero
--   refers to the nearest bound variable and the index increases by one
--   for each bound variable of the same name going outward. The following
--   diagram may help:
--   
--   <pre>
--                             +-refers to-+
--                             |           |
--                             v           |
--   \(x : *) -&gt; \(y : *) -&gt; \(x : *) -&gt; x@0
--   
--     +-------------refers to-------------+
--     |                                   |
--     v                                   |
--   \(x : *) -&gt; \(y : *) -&gt; \(x : *) -&gt; x@1
--   </pre>
--   
--   This <a>Int</a> behaves like a De Bruijn index in the special case
--   where all variables have the same name.
--   
--   You can optionally omit the index if it is <tt>0</tt>:
--   
--   <pre>
--                             +refers to+
--                             |         |
--                             v         |
--   \(x : *) -&gt; \(y : *) -&gt; \(x : *) -&gt; x
--   </pre>
--   
--   Zero indices are omitted when pretty-printing <a>Var</a>s and non-zero
--   indices appear as a numeric suffix.
data Var
V :: Text -> Int -> Var

-- | Constants for the calculus of constructions
--   
--   The only axiom is:
--   
--   <pre>
--   ⊦ * : □
--   </pre>
--   
--   ... and all four rule pairs are valid:
--   
--   <pre>
--   ⊦ * ↝ * : *
--   ⊦ □ ↝ * : *
--   ⊦ * ↝ □ : □
--   ⊦ □ ↝ □ : □
--   </pre>
data Const
Star :: Const
Box :: Const

-- | Path to an external resource
data Path
File :: FilePath -> Path
URL :: Text -> Path

-- | Like <a>Void</a>, except with an <a>NFData</a> instance in order to
--   avoid orphan instances
newtype X
X :: (forall a. a) -> X
[absurd] :: X -> forall a. a

-- | Syntax tree for expressions
data Expr a

-- | <pre>
--   Const c        ~  c
--   </pre>
Const :: Const -> Expr a

-- | <pre>
--   Var (V x 0)    ~  x
--   Var (V x n)    ~  x@n
--   </pre>
Var :: Var -> Expr a

-- | <pre>
--   Lam x     A b  ~  λ(x : A) → b
--   </pre>
Lam :: Text -> (Expr a) -> (Expr a) -> Expr a

-- | <pre>
--   Pi x      A B  ~  ∀(x : A) → B
--   Pi unused A B  ~        A  → B
--   </pre>
Pi :: Text -> (Expr a) -> (Expr a) -> Expr a

-- | <pre>
--   App f a        ~  f a
--   </pre>
App :: (Expr a) -> (Expr a) -> Expr a

-- | <pre>
--   Embed path     ~  #path
--   </pre>
Embed :: a -> Expr a

-- | Bound variable names and their types
--   
--   Variable names may appear more than once in the <a>Context</a>. The
--   <tt>Var</tt> <tt>x@n</tt> refers to the <tt>n</tt>th occurrence of
--   <tt>x</tt> in the <a>Context</a> (using 0-based numbering).
data Context a

-- | Type-check an expression and return the expression's type if
--   type-checking suceeds or an error if type-checking fails
--   
--   <a>typeWith</a> 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 <a>normalize</a> it
--   afterwards.
typeWith :: Context (Expr X) -> Expr X -> Either TypeError (Expr X)

-- | <a>typeOf</a> is the same as <a>typeWith</a> with an empty context,
--   meaning that the expression must be closed (i.e. no free variables),
--   otherwise type-checking will fail.
typeOf :: Expr X -> Either TypeError (Expr X)

-- | Reduce an expression to its normal form, performing both beta
--   reduction and eta reduction
--   
--   <a>normalize</a> 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 a -> Expr a

-- | <tt>shift n x</tt> adds <tt>n</tt> to the index of all free variables
--   named <tt>x</tt> within an <a>Expr</a>
shift :: Int -> Text -> Expr a -> Expr a

-- | Substitute all occurrences of a variable with an expression
--   
--   <pre>
--   subst x n C B  ~  B[x@n := C]
--   </pre>
subst :: Text -> Int -> Expr a -> Expr a -> Expr a

-- | Pretty-print a value
pretty :: Buildable a => a -> Text

-- | Pretty-print an expression as a <a>Builder</a>, using Unicode symbols
buildExpr :: Buildable a => Expr a -> Builder

-- | Pretty-print an expression as a <a>Builder</a>, using ASCII symbols
buildExprASCII :: Buildable a => Expr a -> Builder

-- | A structured type error that includes context
data TypeError
TypeError :: Context (Expr X) -> Expr X -> TypeMessage -> TypeError
[context] :: TypeError -> Context (Expr X)
[current] :: TypeError -> Expr X
[typeMessage] :: TypeError -> TypeMessage

-- | The specific type error
data TypeMessage
UnboundVariable :: TypeMessage
InvalidInputType :: (Expr X) -> TypeMessage
InvalidOutputType :: (Expr X) -> TypeMessage
NotAFunction :: TypeMessage
TypeMismatch :: (Expr X) -> (Expr X) -> TypeMessage
Untyped :: Const -> TypeMessage
instance GHC.Show.Show Morte.Core.TypeMessage
instance GHC.Show.Show a => GHC.Show.Show (Morte.Core.Expr a)
instance Data.Traversable.Traversable Morte.Core.Expr
instance Data.Foldable.Foldable Morte.Core.Expr
instance GHC.Base.Functor Morte.Core.Expr
instance GHC.Show.Show Morte.Core.Path
instance GHC.Classes.Ord Morte.Core.Path
instance GHC.Classes.Eq Morte.Core.Path
instance GHC.Enum.Enum Morte.Core.Const
instance GHC.Enum.Bounded Morte.Core.Const
instance GHC.Show.Show Morte.Core.Const
instance GHC.Classes.Eq Morte.Core.Const
instance GHC.Show.Show Morte.Core.Var
instance GHC.Classes.Eq Morte.Core.Var
instance GHC.Show.Show Morte.Core.TypeError
instance GHC.Exception.Exception Morte.Core.TypeError
instance Control.DeepSeq.NFData Morte.Core.TypeError
instance Formatting.Buildable.Buildable Morte.Core.TypeError
instance Control.DeepSeq.NFData Morte.Core.TypeMessage
instance Formatting.Buildable.Buildable Morte.Core.TypeMessage
instance GHC.Base.Applicative Morte.Core.Expr
instance GHC.Base.Monad Morte.Core.Expr
instance GHC.Classes.Eq a => GHC.Classes.Eq (Morte.Core.Expr a)
instance Data.Binary.Class.Binary a => Data.Binary.Class.Binary (Morte.Core.Expr a)
instance Data.String.IsString (Morte.Core.Expr a)
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Morte.Core.Expr a)
instance Formatting.Buildable.Buildable a => Formatting.Buildable.Buildable (Morte.Core.Expr a)
instance GHC.Classes.Eq Morte.Core.X
instance GHC.Show.Show Morte.Core.X
instance Control.DeepSeq.NFData Morte.Core.X
instance Formatting.Buildable.Buildable Morte.Core.X
instance Data.Binary.Class.Binary Morte.Core.X
instance Formatting.Buildable.Buildable Morte.Core.Path
instance Data.Binary.Class.Binary Morte.Core.Const
instance Control.DeepSeq.NFData Morte.Core.Const
instance Formatting.Buildable.Buildable Morte.Core.Const
instance Data.Binary.Class.Binary Morte.Core.Var
instance Data.String.IsString Morte.Core.Var
instance Control.DeepSeq.NFData Morte.Core.Var
instance Formatting.Buildable.Buildable Morte.Core.Var


-- | Lexing logic for the Morte language
module Morte.Lexer

-- | Convert a text representation of an expression into a stream of tokens
--   
--   <a>lexExpr</a> keeps track of position and returns the remainder of
--   the input if lexing fails.
lexExpr :: Text -> Producer LocatedToken (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
File :: FilePath -> Token
URL :: Text -> 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

-- | A <a>Token</a> augmented with <a>Position</a> information
data LocatedToken
LocatedToken :: !Token -> {-# UNPACK #-} !Position -> LocatedToken
[token] :: LocatedToken -> !Token
[position] :: LocatedToken -> {-# UNPACK #-} !Position
instance GHC.Show.Show Morte.Lexer.LocatedToken
instance GHC.Show.Show Morte.Lexer.Token
instance GHC.Classes.Eq Morte.Lexer.Token
instance GHC.Show.Show Morte.Lexer.Position


-- | Parsing logic for the Morte language
module Morte.Parser

-- | Parse an <a>Expr</a> from <a>Text</a> or return a <a>ParseError</a> if
--   parsing fails
exprFromText :: Text -> Either ParseError (Expr Path)

-- | 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 and the expected tokens
Parsing :: Token -> [Token] -> ParseMessage
instance GHC.Show.Show Morte.Parser.ParseMessage
instance GHC.Show.Show Morte.Parser.ParseError
instance GHC.Exception.Exception Morte.Parser.ParseError
instance Formatting.Buildable.Buildable Morte.Parser.ParseError


-- | Morte lets you import external expressions located either in local
--   files or hosted on network endpoints.
--   
--   To import a local file as an expression, just insert the path to the
--   file, prepending a <tt>./</tt> if the path is relative to the current
--   directory. For example, suppose we had the following three local
--   files:
--   
--   <pre>
--   -- id
--   \(a : *) -&gt; \(x : a) -&gt; x
--   </pre>
--   
--   <pre>
--   -- Bool
--   forall (Bool : *) -&gt; forall (True : Bool) -&gt; forall (False : Bool) -&gt; Bool
--   </pre>
--   
--   <pre>
--   -- True
--   \(Bool : *) -&gt; \(True : Bool) -&gt; \(False : Bool) -&gt; True
--   </pre>
--   
--   You could then reference them within a Morte expression using this
--   syntax:
--   
--   <pre>
--   ./id ./Bool ./True
--   </pre>
--   
--   ... which would embed their expressions directly within the syntax
--   tree:
--   
--   <pre>
--   -- ... expands out to:
--   (\(a : *) -&gt; \(x : a) -&gt; x)
--       (forall (Bool : *) -&gt; forall (True : Bool) -&gt; forall (False : Bool) -&gt; True)
--       (\(Bool : *) -&gt; \(True : Bool) -&gt; \(False : Bool) -&gt; True)
--   </pre>
--   
--   ... and which normalizes to:
--   
--   <pre>
--   λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
--   </pre>
--   
--   Imported expressions may contain imports of their own, too, which will
--   continue to be resolved. However, Morte will prevent cyclic imports.
--   For example, if you had these two files:
--   
--   <pre>
--   -- foo
--   ./bar
--   </pre>
--   
--   <pre>
--   -- bar
--   ./foo
--   </pre>
--   
--   ... Morte would throw the following exception if you tried to import
--   <tt>foo</tt>:
--   
--   <pre>
--   morte: 
--   ⤷ ./foo
--   ⤷ ./bar
--   Cyclic import: ./foo
--   </pre>
--   
--   You can also import expressions hosted on network endpoints. Just use
--   the URL
--   
--   <pre>
--   http://host[:port]/path
--   </pre>
--   
--   The compiler expects the downloaded expressions to be in the same
--   format as local files, specifically UTF8-encoded source code text.
--   
--   For example, if our <tt>id</tt> expression were hosted at
--   <tt><a>http://example.com/id</a></tt>, then we would embed the
--   expression within our code using:
--   
--   <pre>
--   http://example.com/id
--   </pre>
--   
--   You can also reuse directory names as expressions. If you provide a
--   path to a local or remote directory then the compiler will look for a
--   file named <tt>@</tt> within that directory and use that file to
--   represent the directory.
module Morte.Import

-- | Resolve all imports within an expression
--   
--   By default the starting path is the current directory, but you can
--   override the starting path with a file if you read in the expression
--   from that file
load :: Maybe Path -> Expr Path -> IO (Expr X)

-- | An import failed because of a cycle in the import graph
newtype Cycle
Cycle :: Path -> Cycle

-- | The offending cyclic import
[cyclicImport] :: Cycle -> Path

-- | Morte tries to ensure that all expressions hosted on network endpoints
--   are weakly referentially transparent, meaning roughly that any two
--   clients will compile the exact same result given the same URL.
--   
--   To be precise, a strong interpretaton of referential transparency
--   means that if you compiled a URL you could replace the expression
--   hosted at that URL with the compiled result. Let's term this "static
--   linking". Morte (very intentionally) does not satisfy this stronger
--   interpretation of referential transparency since "statically linking"
--   an expression (i.e. permanently resolving all imports) means that the
--   expression will no longer update if its dependencies change.
--   
--   In general, either interpretation of referential transparency is not
--   enforceable in a networked context since one can easily violate
--   referential transparency with a custom DNS, but Morte can still try to
--   guard against common unintentional violations. To do this, Morte
--   enforces that a non-local import may not reference a local import.
--   
--   Local imports are defined as:
--   
--   <ul>
--   <li>A file</li>
--   <li>A URL with a host of <tt>localhost</tt> or <tt>127.0.0.1</tt></li>
--   </ul>
--   
--   All other imports are defined to be non-local
newtype ReferentiallyOpaque
ReferentiallyOpaque :: Path -> ReferentiallyOpaque

-- | The offending opaque import
[opaqueImport] :: ReferentiallyOpaque -> Path

-- | Extend another exception with the current import stack
data Imported e
Imported :: [Path] -> e -> Imported e

-- | Imports resolved so far, in reverse order
[importStack] :: Imported e -> [Path]

-- | The nested exception
[nested] :: Imported e -> e
instance GHC.Exception.Exception e => GHC.Exception.Exception (Morte.Import.Imported e)
instance GHC.Show.Show e => GHC.Show.Show (Morte.Import.Imported e)
instance GHC.Exception.Exception Morte.Import.ReferentiallyOpaque
instance GHC.Show.Show Morte.Import.ReferentiallyOpaque
instance GHC.Exception.Exception Morte.Import.Cycle
instance GHC.Show.Show Morte.Import.Cycle


-- | 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:
--   
--   <ul>
--   <li>Be super-optimizable - by disabling unrestricted recursion</li>
--   <li>Be portable - so you can transmit code between different
--   languages</li>
--   <li>Be efficient - so that Morte can scale to large code bases</li>
--   <li>Be simple - so people can reason about Morte's soundness</li>
--   </ul>
--   
--   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
