diff --git a/dist/build/Morte/Parser.hs b/dist/build/Morte/Parser.hs --- a/dist/build/Morte/Parser.hs +++ b/dist/build/Morte/Parser.hs @@ -320,7 +320,8 @@ -- | Pretty-print a `ParseError` prettyParseError :: ParseError -> Text prettyParseError (ParseError (Lexer.P l c) e) = Builder.toLazyText ( - "Line: " <> decimal l <> "\n" + "\n" + <> "Line: " <> decimal l <> "\n" <> "Column: " <> decimal c <> "\n" <> "\n" <> case e of diff --git a/morte.cabal b/morte.cabal --- a/morte.cabal +++ b/morte.cabal @@ -1,5 +1,5 @@ Name: morte -Version: 1.1.1 +Version: 1.1.2 Cabal-Version: >=1.8.0.2 Build-Type: Simple License: BSD3 diff --git a/src/Morte/Core.hs b/src/Morte/Core.hs --- a/src/Morte/Core.hs +++ b/src/Morte/Core.hs @@ -53,6 +53,7 @@ -- * Utilities used, + shift, prettyExpr, prettyTypeError, @@ -171,7 +172,8 @@ 1 -> return Box _ -> fail "get Const: Invalid tag byte" -instance NFData Const +instance NFData Const where + rnf c = seq c () axiom :: Const -> Either TypeError Const axiom Star = return Box @@ -424,7 +426,8 @@ -- | Render a pretty-printed `TypeError` as a `Builder` buildTypeError :: TypeError -> Builder buildTypeError (TypeError ctx expr msg) - = ( if Text.null (toLazyText buildContext ) + = "\n" + <> ( if Text.null (toLazyText buildContext ) then mempty else "Context:\n" <> buildContext <> "\n" ) @@ -447,20 +450,20 @@ Lam x' _A b -> Lam x' (subst x n e' _A) b' where n' = if x == x' then n + 1 else n - b' = n' `seq` subst x n' (shift 1 x' 0 e') b + b' = n' `seq` subst x n' (shift 1 x' e') b Pi x' _A _B -> Pi x' (subst x n e' _A) _B' where n' = if x == x' then n + 1 else n - _B' = n' `seq` subst x n' (shift 1 x' 0 e') _B + _B' = n' `seq` subst x n' (shift 1 x' e') _B App f a -> App (subst x n e' f) (subst x n e' a) Var (V x' n') -> if x == x' && n == n' then e' else e Const k -> Const k -{-| @shift n x 0@ adds @n@ to the index of all free variables named @x@ within - an `Expr` +{-| @shift n x@ adds @n@ to the index of all free variables named @x@ within an + `Expr` -} -shift :: Int -> Text -> Int -> Expr -> Expr -shift d x0 c0 e0 = go e0 c0 +shift :: Int -> Text -> Expr -> Expr +shift d x0 e0 = go e0 0 where go e c = case e of Lam x _A b -> Lam x (go _A c) (go b $! c') @@ -489,7 +492,7 @@ Nothing -> Left (TypeError ctx e UnboundVariable) Just a -> return a Lam x _A b -> do - let ctx' = [ (x', shift 1 x 0 _A') | (x', _A') <- (x, _A):ctx ] + let ctx' = [ (x', shift 1 x _A') | (x', _A') <- (x, _A):ctx ] _B <- typeWith ctx' b let p = Pi x _A _B _t <- typeWith ctx p @@ -499,7 +502,7 @@ s <- case eS of Const s -> return s _ -> Left (TypeError ctx e (InvalidInputType _A)) - let ctx' = [ (x', shift 1 x 0 _A') | (x', _A') <- (x, _A):ctx ] + let ctx' = [ (x', shift 1 x _A') | (x', _A') <- (x, _A):ctx ] eT <- fmap whnf (typeWith ctx' _B) t <- case eT of Const t -> return t @@ -513,9 +516,9 @@ _A' <- typeWith ctx a if _A == _A' then do - let a' = shift 1 x 0 a + let a' = shift 1 x a _B' = subst x 0 a' _B - return (shift (-1) x 0 _B') + return (shift (-1) x _B') else do let nf_A = normalize _A nf_A' = normalize _A' @@ -532,9 +535,9 @@ whnf :: Expr -> Expr whnf e = case e of App f a -> case whnf f of - Lam x _A b -> whnf (shift (-1) x 0 b') -- Beta reduce + Lam x _A b -> whnf (shift (-1) x b') -- Beta reduce where - a' = shift 1 x 0 a + a' = shift 1 x a b' = subst x 0 a' b _ -> e _ -> e @@ -568,7 +571,7 @@ Lam x _A b -> case b' of App f a -> case a of Var v' | v == v' && not (v `freeIn` f) -> - shift (-1) x 0 f -- Eta reduce + shift (-1) x f -- Eta reduce | otherwise -> e' where @@ -580,9 +583,9 @@ e' = Lam x (normalize _A) b' Pi x _A _B -> Pi x (normalize _A) (normalize _B) App f a -> case normalize f of - Lam x _A b -> normalize (shift (-1) x 0 b') -- Beta reduce + Lam x _A b -> normalize (shift (-1) x b') -- Beta reduce where - a' = shift 1 x 0 a + a' = shift 1 x (normalize a) b' = subst x 0 a' b f' -> App f' (normalize a) Var _ -> e diff --git a/src/Morte/Parser.y b/src/Morte/Parser.y --- a/src/Morte/Parser.y +++ b/src/Morte/Parser.y @@ -137,7 +137,8 @@ -- | Pretty-print a `ParseError` prettyParseError :: ParseError -> Text prettyParseError (ParseError (Lexer.P l c) e) = Builder.toLazyText ( - "Line: " <> decimal l <> "\n" + "\n" + <> "Line: " <> decimal l <> "\n" <> "Column: " <> decimal c <> "\n" <> "\n" <> case e of diff --git a/src/Morte/Tutorial.hs b/src/Morte/Tutorial.hs --- a/src/Morte/Tutorial.hs +++ b/src/Morte/Tutorial.hs @@ -1058,7 +1058,7 @@ {- $optimization You might wonder why Morte forbids recursion, forcing us to encode data - types F-algebras or F-coalgebras. Morte imposes this restriction this in + types as F-algebras or F-coalgebras. Morte imposes this restriction in order to super-optimize your program. For example, consider the following program which maps the identity function over a list: @@ -1489,7 +1489,7 @@ Normalization leads to certain emergent properties when optimizing recursive code or corecursive code. If you optimize a corecursive loop you will - produce code equivalent an @while@ loop where the seed is the initial state + produce code equivalent to a @while@ loop where the seed is the initial state of the loop and the generating step function unfolds one iteration of the loop. If you optimize a recursive loop you will generate an unrolled loop. See the next section for an example of Morte generating a very large @@ -2005,7 +2005,7 @@ If every functional language has a Morte encoder/decoder, then eventually there can be a code utility analogous to @pandoc@ that converts code written - any of these languages to code written in any other of these language. + in any of these languages to code written in any other. Additionally, Morte provides a standard `Data.Binary.Binary` interface that you can use for serializing and deserializing code. You may find this @@ -2031,7 +2031,7 @@ in order to reuse the large body of research for translating programming abstractions to and from the polymorphic lambda calculus. - Finally, you can use Morte as a equational reasoning engine to learn how + Finally, you can use Morte as an equational reasoning engine to learn how high-level abstractions reduce to low-level abstractions. If you are teaching lambda calculus you can use Morte as a teaching tool for how to encode abstractions within lambda calculus.