morte 1.1.1 → 1.1.2
raw patch · 5 files changed
+29/−24 lines, 5 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ Morte.Core: shift :: Int -> Text -> Expr -> Expr
Files
- dist/build/Morte/Parser.hs +2/−1
- morte.cabal +1/−1
- src/Morte/Core.hs +20/−17
- src/Morte/Parser.y +2/−1
- src/Morte/Tutorial.hs +4/−4
dist/build/Morte/Parser.hs view
@@ -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
morte.cabal view
@@ -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
src/Morte/Core.hs view
@@ -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
src/Morte/Parser.y view
@@ -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
src/Morte/Tutorial.hs view
@@ -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.