morte (empty) → 1.0.0
raw patch · 10 files changed
+3897/−0 lines, 10 filesdep +arraydep +basedep +binarysetup-changed
Dependencies added: array, base, binary, containers, lens-family-core, morte, optparse-applicative, pipes, text, transformers
Files
- LICENSE +24/−0
- Setup.hs +2/−0
- dist/build/Morte/Lexer.hs +372/−0
- dist/build/Morte/Parser.hs +585/−0
- exec/Main.hs +33/−0
- morte.cabal +58/−0
- src/Morte/Core.hs +481/−0
- src/Morte/Lexer.x +153/−0
- src/Morte/Parser.y +147/−0
- src/Morte/Tutorial.hs +2042/−0
+ LICENSE view
@@ -0,0 +1,24 @@+Copyright (c) 2014 Gabriel Gonzalez+All rights reserved.++Redistribution and use in source and binary forms, with or without modification,+are permitted provided that the following conditions are met:+ * Redistributions of source code must retain the above copyright notice,+ this list of conditions and the following disclaimer.+ * Redistributions in binary form must reproduce the above copyright notice,+ this list of conditions and the following disclaimer in the documentation+ and/or other materials provided with the distribution.+ * Neither the name of Gabriel Gonzalez nor the names of other contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ dist/build/Morte/Lexer.hs view
@@ -0,0 +1,372 @@+{-# LANGUAGE CPP,MagicHash,BangPatterns #-}+{-# LINE 1 "src/Morte/Lexer.x" #-}++{-# LANGUAGE OverloadedStrings #-}++-- | Lexing logic for the Morte language+module Morte.Lexer (+ -- * Lexer+ lexExpr,++ -- * Types+ Token(..),+ Position(..)+ ) where++import Control.Monad.Trans.State.Strict (State)+import Data.Bits (shiftR, (.&.))+import Data.Char (ord, digitToInt)+import Data.Text.Lazy (Text)+import qualified Data.Text.Lazy as Text+import Data.Word (Word8)+import Lens.Family.State.Strict ((.=), (+=))+import Pipes (Producer, lift, yield)+++#if __GLASGOW_HASKELL__ >= 603+#include "ghcconfig.h"+#elif defined(__GLASGOW_HASKELL__)+#include "config.h"+#endif+#if __GLASGOW_HASKELL__ >= 503+import Data.Array+import Data.Char (ord)+import Data.Array.Base (unsafeAt)+#else+import Array+import Char (ord)+#endif+#if __GLASGOW_HASKELL__ >= 503+import GHC.Exts+#else+import GlaExts+#endif+alex_base :: AlexAddr+alex_base = AlexA# "\xf8\xff\xff\xff\xd9\xff\xff\xff\x66\xff\xff\xff\x52\x00\x00\x00\x5b\x00\x00\x00\xcc\x00\x00\x00\x00\x00\x00\x00\x4c\x01\x00\x00\x8a\xff\xff\xff\x83\xff\xff\xff\x00\x00\x00\x00\x8d\x01\x00\x00\x6c\xff\xff\xff\x8d\xff\xff\xff\x8e\xff\xff\xff\x7c\xff\xff\xff\x8d\x02\x00\x00\x4d\x02\x00\x00\x00\x00\x00\x00\x06\x00\x00\x00\x00\x00\x00\x00\x43\x03\x00\x00\x2d\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x2e\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02\x04\x00\x00\x00\x00\x00\x00\xe1\xff\xff\xff\x00\x00\x00\x00\x53\x00\x00\x00\x3c\x04\x00\x00\x76\x04\x00\x00\xb0\x04\x00\x00\xea\x04\x00\x00\x00\x00\x00\x00\x24\x05\x00\x00\x5e\x05\x00\x00\x98\x05\x00\x00\xd2\x05\x00\x00"#++alex_table :: AlexAddr+alex_table = AlexA# "\x00\x00\x13\x00\x14\x00\x13\x00\x13\x00\x13\x00\x15\x00\x1c\x00\x0e\x00\x0f\x00\x1f\x00\x0d\x00\x1f\x00\x1f\x00\x1d\x00\x13\x00\x1f\x00\x13\x00\x13\x00\x13\x00\x00\x00\x00\x00\x00\x00\x1d\x00\x13\x00\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16\x00\x17\x00\x1a\x00\x00\x00\x00\x00\x01\x00\x13\x00\x21\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x18\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x19\x00\x26\x00\x23\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x00\x00\x20\x00\x00\x00\x00\x00\x26\x00\x00\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x25\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x03\x00\x08\x00\x03\x00\x03\x00\x03\x00\x03\x00\x00\x00\x00\x00\x27\x00\x03\x00\x03\x00\x00\x00\x03\x00\x03\x00\x03\x00\x00\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x22\x00\x00\x00\x03\x00\x03\x00\x03\x00\x03\x00\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x03\x00\x00\x00\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0c\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x03\x00\x00\x00\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x09\x00\x10\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x0b\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x04\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x11\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x03\x00\x00\x00\x03\x00\x03\x00\x03\x00\x03\x00\x00\x00\x00\x00\x00\x00\x03\x00\x03\x00\x00\x00\x03\x00\x03\x00\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x03\x00\x03\x00\x03\x00\x03\x00\x03\x00\x00\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x03\x00\x00\x00\x03\x00\x00\x00\x26\x00\x00\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x03\x00\x00\x00\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x10\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x12\x00\x11\x00\x04\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0b\x00\x07\x00\x06\x00\x06\x00\x06\x00\x05\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x00\x00\x00\x00\x00\x00\x00\x00\x26\x00\x00\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x2b\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x00\x00\x00\x00\x00\x00\x00\x00\x26\x00\x00\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x00\x00\x00\x00\x00\x00\x00\x00\x26\x00\x00\x00\x29\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x00\x00\x00\x00\x00\x00\x00\x00\x26\x00\x00\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x28\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x00\x00\x00\x00\x00\x00\x00\x00\x26\x00\x00\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x00\x00\x00\x00\x00\x00\x00\x00\x26\x00\x00\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x24\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x00\x00\x00\x00\x00\x00\x00\x00\x26\x00\x00\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x2a\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x00\x00\x00\x00\x00\x00\x00\x00\x26\x00\x00\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x1e\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x1b\x00\x26\x00\x26\x00\x00\x00\x00\x00\x00\x00\x00\x00\x26\x00\x00\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x26\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#++alex_check :: AlexAddr+alex_check = AlexA# "\xff\xff\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x2d\x00\xa1\x00\x7e\x00\x86\x00\x7c\x00\x88\x00\xa0\x00\x80\x00\x92\x00\x09\x00\x2f\x00\x0b\x00\x0c\x00\x0d\x00\xff\xff\xff\xff\xff\xff\x3e\x00\x20\x00\x96\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x28\x00\x29\x00\x2a\x00\xff\xff\xff\xff\x2d\x00\x20\x00\xbb\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\x5c\x00\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x21\x00\x7c\x00\x23\x00\x24\x00\x25\x00\x26\x00\xff\xff\xff\xff\x29\x00\x2a\x00\x2b\x00\xff\xff\x2d\x00\x2e\x00\x2f\x00\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x5c\x00\xff\xff\x5e\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xce\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x7c\x00\xff\xff\x7e\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xe2\x00\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x00\x00\x01\x00\x02\x00\x03\x00\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x0e\x00\x0f\x00\x10\x00\x11\x00\x12\x00\x13\x00\x14\x00\x15\x00\x16\x00\x17\x00\x18\x00\x19\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x20\x00\x21\x00\x22\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x5b\x00\x5c\x00\x5d\x00\x5e\x00\x5f\x00\x60\x00\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x7b\x00\x7c\x00\x7d\x00\x7e\x00\x7f\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x0a\x00\x21\x00\xff\xff\x23\x00\x24\x00\x25\x00\x26\x00\xff\xff\xff\xff\xff\xff\x2a\x00\x2b\x00\xff\xff\x2d\x00\x2e\x00\x2f\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x5c\x00\xff\xff\x5e\x00\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x7c\x00\xff\xff\x7e\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#++alex_deflt :: AlexAddr+alex_deflt = AlexA# "\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x0a\x00\x0a\x00\xff\xff\xff\xff\xff\xff\x12\x00\x12\x00\xff\xff\xff\xff\xff\xff\xff\xff\x15\x00\x15\x00\x15\x00\xff\xff\xff\xff\x15\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#++alex_accept = listArray (0::Int,43) [[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[(AlexAccSkip)],[(AlexAcc (alex_action_1))],[(AlexAccSkip)],[(AlexAcc (alex_action_3))],[(AlexAcc (alex_action_4))],[(AlexAcc (alex_action_5))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_7))],[(AlexAcc (alex_action_8))],[(AlexAcc (alex_action_8))],[(AlexAcc (alex_action_9))],[(AlexAcc (alex_action_10))],[(AlexAcc (alex_action_10))],[(AlexAcc (alex_action_11))],[(AlexAcc (alex_action_11))],[(AlexAcc (alex_action_12))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))]]+{-# LINE 55 "src/Morte/Lexer.x" #-}++toInt :: Text -> Int+toInt = Text.foldl' (\x c -> 10 * x + digitToInt c) 0++-- This was lifted almost intact from the @alex@ source code+encode :: Char -> (Word8, [Word8])+encode c = (fromIntegral h, map fromIntegral t)+ where+ (h, t) = go (ord c)++ go n+ | n <= 0x7f = (n, [])+ | n <= 0x7ff = (0xc0 + (n `shiftR` 6), [0x80 + n .&. 0x3f])+ | n <= 0xffff =+ ( 0xe0 + (n `shiftR` 12)+ , [ 0x80 + ((n `shiftR` 6) .&. 0x3f)+ , 0x80 + n .&. 0x3f+ ]+ )+ | otherwise =+ ( 0xf0 + (n `shiftR` 18)+ , [ 0x80 + ((n `shiftR` 12) .&. 0x3f)+ , 0x80 + ((n `shiftR` 6) .&. 0x3f)+ , 0x80 + n .&. 0x3f+ ]+ )++-- | The cursor's location while lexing the text+data Position = P+ { lineNo :: {-# UNPACK #-} !Int+ , columnNo :: {-# UNPACK #-} !Int+ } deriving (Show)++-- line :: Lens' Position Int+line :: Functor f => (Int -> f Int) -> Position -> f Position+line k (P l c) = fmap (\l' -> P l' c) (k l)++-- column :: Lens' Position Int+column :: Functor f => (Int -> f Int) -> Position -> f Position+column k (P l c) = fmap (\c' -> P l c') (k c)++{- @alex@ does not provide a `Text` wrapper, so the following code just modifies+ the code from their @basic@ wrapper to work with `Text`++ I could not get the @basic-bytestring@ wrapper to work; it does not correctly+ recognize Unicode regular expressions.+-}+data AlexInput = AlexInput+ { prevChar :: Char+ , currBytes :: [Word8]+ , currInput :: Text+ }++alexGetByte :: AlexInput -> Maybe (Word8,AlexInput)+alexGetByte (AlexInput c bytes text) = case bytes of+ b:ytes -> Just (b, AlexInput c ytes text)+ [] -> case Text.uncons text of+ Nothing -> Nothing+ Just (t, ext) -> case encode t of+ (b, ytes) -> Just (b, AlexInput t ytes ext)++alexInputPrevChar :: AlexInput -> Char+alexInputPrevChar = prevChar++{-| 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)+lexExpr text = go (AlexInput '\n' [] text)+ where+ go input = case alexScan input 0 of+ AlexEOF -> return Nothing+ AlexError (AlexInput _ _ text) -> return (Just text)+ AlexSkip input' len -> do+ lift (column += len)+ go input'+ AlexToken input' len act -> do+ act (Text.take (fromIntegral len) (currInput input))+ lift (column += len)+ go input'++-- | Token type, used to communicate between the lexer and parser+data Token+ = OpenParen+ | CloseParen+ | Colon+ | At+ | Star+ | Box+ | Arrow+ | Lambda+ | Pi+ | Label Text+ | Number Int+ | EOF+ deriving (Show)++alex_action_1 = \_ -> lift (do+ line += 1+ column .= 0 ) +alex_action_3 = \_ -> yield OpenParen +alex_action_4 = \_ -> yield CloseParen +alex_action_5 = \_ -> yield Colon +alex_action_6 = \_ -> yield At +alex_action_7 = \_ -> yield Star +alex_action_8 = \_ -> yield Box +alex_action_9 = \_ -> yield Arrow +alex_action_10 = \_ -> yield Pi +alex_action_11 = \_ -> yield Lambda +alex_action_12 = \text -> yield (Number (toInt text)) +alex_action_13 = \text -> yield (Label text) +{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "<built-in>" #-}+{-# LINE 1 "<command-line>" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+-- -----------------------------------------------------------------------------+-- ALEX TEMPLATE+--+-- This code is in the PUBLIC DOMAIN; you may copy it freely and use+-- it for any purpose whatsoever.++-- -----------------------------------------------------------------------------+-- INTERNALS and main scanner engine++{-# LINE 37 "templates/GenericTemplate.hs" #-}++{-# LINE 47 "templates/GenericTemplate.hs" #-}+++data AlexAddr = AlexA# Addr#++#if __GLASGOW_HASKELL__ < 503+uncheckedShiftL# = shiftL#+#endif++{-# INLINE alexIndexInt16OffAddr #-}+alexIndexInt16OffAddr (AlexA# arr) off =+#ifdef WORDS_BIGENDIAN+ narrow16Int# i+ where+ !i = word2Int# ((high `uncheckedShiftL#` 8#) `or#` low)+ !high = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))+ !low = int2Word# (ord# (indexCharOffAddr# arr off'))+ !off' = off *# 2#+#else+ indexInt16OffAddr# arr off+#endif++++++{-# INLINE alexIndexInt32OffAddr #-}+alexIndexInt32OffAddr (AlexA# arr) off = +#ifdef WORDS_BIGENDIAN+ narrow32Int# i+ where+ !i = word2Int# ((b3 `uncheckedShiftL#` 24#) `or#`+ (b2 `uncheckedShiftL#` 16#) `or#`+ (b1 `uncheckedShiftL#` 8#) `or#` b0)+ !b3 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 3#)))+ !b2 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 2#)))+ !b1 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))+ !b0 = int2Word# (ord# (indexCharOffAddr# arr off'))+ !off' = off *# 4#+#else+ indexInt32OffAddr# arr off+#endif++++++#if __GLASGOW_HASKELL__ < 503+quickIndex arr i = arr ! i+#else+-- GHC >= 503, unsafeAt is available from Data.Array.Base.+quickIndex = unsafeAt+#endif+++++-- -----------------------------------------------------------------------------+-- Main lexing routines++data AlexReturn a+ = AlexEOF+ | AlexError !AlexInput+ | AlexSkip !AlexInput !Int+ | AlexToken !AlexInput !Int a++-- alexScan :: AlexInput -> StartCode -> AlexReturn a+alexScan input (I# (sc))+ = alexScanUser undefined input (I# (sc))++alexScanUser user input (I# (sc))+ = case alex_scan_tkn user input 0# input sc AlexNone of+ (AlexNone, input') ->+ case alexGetByte input of+ Nothing -> ++++ AlexEOF+ Just _ ->++++ AlexError input'++ (AlexLastSkip input'' len, _) ->++++ AlexSkip input'' len++ (AlexLastAcc k input''' len, _) ->++++ AlexToken input''' len k+++-- Push the input through the DFA, remembering the most recent accepting+-- state it encountered.++alex_scan_tkn user orig_input len input s last_acc =+ input `seq` -- strict in the input+ let + new_acc = (check_accs (alex_accept `quickIndex` (I# (s))))+ in+ new_acc `seq`+ case alexGetByte input of+ Nothing -> (new_acc, input)+ Just (c, new_input) -> ++++ let+ (!(base)) = alexIndexInt32OffAddr alex_base s+ (!((I# (ord_c)))) = fromIntegral c+ (!(offset)) = (base +# ord_c)+ (!(check)) = alexIndexInt16OffAddr alex_check offset+ + (!(new_s)) = if (offset >=# 0#) && (check ==# ord_c)+ then alexIndexInt16OffAddr alex_table offset+ else alexIndexInt16OffAddr alex_deflt s+ in+ case new_s of + -1# -> (new_acc, input)+ -- on an error, we want to keep the input *before* the+ -- character that failed, not after.+ _ -> alex_scan_tkn user orig_input (if c < 0x80 || c >= 0xC0 then (len +# 1#) else len)+ -- note that the length is increased ONLY if this is the 1st byte in a char encoding)+ new_input new_s new_acc++ where+ check_accs [] = last_acc+ check_accs (AlexAcc a : _) = AlexLastAcc a input (I# (len))+ check_accs (AlexAccSkip : _) = AlexLastSkip input (I# (len))+ check_accs (AlexAccPred a predx : rest)+ | predx user orig_input (I# (len)) input+ = AlexLastAcc a input (I# (len))+ check_accs (AlexAccSkipPred predx : rest)+ | predx user orig_input (I# (len)) input+ = AlexLastSkip input (I# (len))+ check_accs (_ : rest) = check_accs rest++data AlexLastAcc a+ = AlexNone+ | AlexLastAcc a !AlexInput !Int+ | AlexLastSkip !AlexInput !Int++instance Functor AlexLastAcc where+ fmap f AlexNone = AlexNone+ fmap f (AlexLastAcc x y z) = AlexLastAcc (f x) y z+ fmap f (AlexLastSkip x y) = AlexLastSkip x y++data AlexAcc a user+ = AlexAcc a+ | AlexAccSkip+ | AlexAccPred a (AlexAccPred user)+ | AlexAccSkipPred (AlexAccPred user)++type AlexAccPred user = user -> AlexInput -> Int -> AlexInput -> Bool++-- -----------------------------------------------------------------------------+-- Predicates on a rule++alexAndPred p1 p2 user in1 len in2+ = p1 user in1 len in2 && p2 user in1 len in2++--alexPrevCharIsPred :: Char -> AlexAccPred _ +alexPrevCharIs c _ input _ _ = c == alexInputPrevChar input++alexPrevCharMatches f _ input _ _ = f (alexInputPrevChar input)++--alexPrevCharIsOneOfPred :: Array Char Bool -> AlexAccPred _ +alexPrevCharIsOneOf arr _ input _ _ = arr ! alexInputPrevChar input++--alexRightContext :: Int -> AlexAccPred _+alexRightContext (I# (sc)) user _ _ input = + case alex_scan_tkn user input 0# input sc AlexNone of+ (AlexNone, _) -> False+ _ -> True+ -- TODO: there's no need to find the longest+ -- match when checking the right context, just+ -- the first match will do.++-- used by wrappers+iUnbox (I# (i)) = i
+ dist/build/Morte/Parser.hs view
@@ -0,0 +1,585 @@+{-# OPTIONS_GHC -w #-}+{-# OPTIONS -fglasgow-exts -cpp #-}+{-# LANGUAGE OverloadedStrings #-}++-- | Parsing logic for the Morte language++module Morte.Parser (+ -- * Parser+ exprFromText,++ -- * Errors+ prettyParseError,+ ParseError(..),+ ParseMessage(..)+ ) where++import Control.Monad.Trans.Error (ErrorT, Error(..), throwError, runErrorT)+import Control.Monad.Trans.State.Strict (State, runState)+import Data.Functor.Identity (Identity, runIdentity)+import Data.Monoid (mempty, (<>))+import Data.Text.Lazy (Text)+import qualified Data.Text.Lazy as Text+import qualified Data.Text.Lazy.Builder as Builder+import Data.Text.Lazy.Builder.Int (decimal)+import Lens.Family.Stock (_1, _2)+import Lens.Family.State.Strict ((.=), use, zoom)+import Morte.Core (Var(..), Const(..), Expr(..))+import qualified Morte.Lexer as Lexer+import Morte.Lexer (Token, Position)+import Pipes (Producer, hoist, lift, next)+import qualified Data.Array as Happy_Data_Array+import qualified GHC.Exts as Happy_GHC_Exts++-- parser produced by Happy Version 1.18.9++newtype HappyAbsSyn = HappyAbsSyn HappyAny+#if __GLASGOW_HASKELL__ >= 607+type HappyAny = Happy_GHC_Exts.Any+#else+type HappyAny = forall a . a+#endif+happyIn4 :: (Expr) -> (HappyAbsSyn )+happyIn4 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn4 #-}+happyOut4 :: (HappyAbsSyn ) -> (Expr)+happyOut4 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut4 #-}+happyIn5 :: (Var) -> (HappyAbsSyn )+happyIn5 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn5 #-}+happyOut5 :: (HappyAbsSyn ) -> (Var)+happyOut5 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut5 #-}+happyIn6 :: (Expr) -> (HappyAbsSyn )+happyIn6 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn6 #-}+happyOut6 :: (HappyAbsSyn ) -> (Expr)+happyOut6 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut6 #-}+happyIn7 :: (Expr) -> (HappyAbsSyn )+happyIn7 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn7 #-}+happyOut7 :: (HappyAbsSyn ) -> (Expr)+happyOut7 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut7 #-}+happyInTok :: (Token) -> (HappyAbsSyn )+happyInTok x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyInTok #-}+happyOutTok :: (HappyAbsSyn ) -> (Token)+happyOutTok x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOutTok #-}+++happyActOffsets :: HappyAddr+happyActOffsets = HappyA# "\x01\x00\x0e\x00\x00\x00\x0e\x00\x00\x00\x01\x00\x00\x00\x00\x00\x3b\x00\x37\x00\x07\x00\x3c\x00\x3a\x00\x32\x00\x32\x00\x00\x00\x01\x00\x2c\x00\x38\x00\x00\x00\x00\x00\x00\x00\x36\x00\x35\x00\x01\x00\x01\x00\x34\x00\x33\x00\x10\x00\xfa\xff\x01\x00\x01\x00\x00\x00\x00\x00\x00\x00"#++happyGotoOffsets :: HappyAddr+happyGotoOffsets = HappyA# "\x31\x00\x02\x00\x00\x00\x0f\x00\x00\x00\x2d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0f\x00\x00\x00\x00\x00\x15\x00\x14\x00\x00\x00\x29\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x25\x00\x21\x00\x00\x00\x00\x00\x00\x00\x00\x00\x1d\x00\x19\x00\x00\x00\x00\x00\x00\x00"#++happyDefActions :: HappyAddr+happyDefActions = HappyA# "\x00\x00\x00\x00\xf6\xff\x00\x00\xf7\xff\x00\x00\xf5\xff\xf4\xff\xf9\xff\x00\x00\xfe\xff\x00\x00\x00\x00\x00\x00\x00\x00\xf8\xff\x00\x00\x00\x00\x00\x00\xf3\xff\xfa\xff\xfb\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xfc\xff\xfd\xff"#++happyCheck :: HappyAddr+happyCheck = HappyA# "\xff\xff\x07\x00\x01\x00\x01\x00\x02\x00\x03\x00\x05\x00\x06\x00\x01\x00\x08\x00\x09\x00\x0a\x00\x05\x00\x06\x00\x07\x00\x01\x00\x01\x00\x0a\x00\x03\x00\x05\x00\x06\x00\x01\x00\x01\x00\x07\x00\x0a\x00\x00\x00\x01\x00\x02\x00\x03\x00\x00\x00\x01\x00\x02\x00\x03\x00\x00\x00\x01\x00\x02\x00\x03\x00\x00\x00\x01\x00\x02\x00\x03\x00\x00\x00\x01\x00\x02\x00\x03\x00\x00\x00\x01\x00\x02\x00\x03\x00\x00\x00\x01\x00\x02\x00\x03\x00\x02\x00\x02\x00\x0b\x00\x03\x00\x03\x00\x02\x00\x01\x00\x0a\x00\x01\x00\xff\xff\x04\x00\xff\xff\xff\xff\xff\xff\x0c\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#++happyTable :: HappyAddr+happyTable = HappyA# "\x00\x00\x1f\x00\x06\x00\x02\x00\x03\x00\x04\x00\x07\x00\x08\x00\x06\x00\x0c\x00\x0d\x00\x09\x00\x07\x00\x08\x00\x11\x00\x06\x00\x02\x00\x09\x00\x0f\x00\x07\x00\x08\x00\x16\x00\x17\x00\x20\x00\x09\x00\x20\x00\x02\x00\x0a\x00\x04\x00\x21\x00\x02\x00\x0a\x00\x04\x00\x1a\x00\x02\x00\x0a\x00\x04\x00\x1b\x00\x02\x00\x0a\x00\x04\x00\x15\x00\x02\x00\x0a\x00\x04\x00\x12\x00\x02\x00\x0a\x00\x04\x00\x09\x00\x02\x00\x0a\x00\x04\x00\x1d\x00\x1e\x00\x15\x00\x19\x00\x1a\x00\x14\x00\x0e\x00\x09\x00\x0f\x00\x00\x00\x12\x00\x00\x00\x00\x00\x00\x00\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#++happyReduceArr = Happy_Data_Array.array (1, 12) [+ (1 , happyReduce_1),+ (2 , happyReduce_2),+ (3 , happyReduce_3),+ (4 , happyReduce_4),+ (5 , happyReduce_5),+ (6 , happyReduce_6),+ (7 , happyReduce_7),+ (8 , happyReduce_8),+ (9 , happyReduce_9),+ (10 , happyReduce_10),+ (11 , happyReduce_11),+ (12 , happyReduce_12)+ ]++happy_n_terms = 13 :: Int+happy_n_nonterms = 4 :: Int++happyReduce_1 = happySpecReduce_1 0# happyReduction_1+happyReduction_1 happy_x_1+ = case happyOut6 happy_x_1 of { happy_var_1 -> + happyIn4+ (happy_var_1+ )}++happyReduce_2 = happyReduce 8# 0# happyReduction_2+happyReduction_2 (happy_x_8 `HappyStk`+ happy_x_7 `HappyStk`+ happy_x_6 `HappyStk`+ happy_x_5 `HappyStk`+ happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut5 happy_x_3 of { happy_var_3 -> + case happyOut4 happy_x_5 of { happy_var_5 -> + case happyOut4 happy_x_8 of { happy_var_8 -> + happyIn4+ (Lam happy_var_3 happy_var_5 happy_var_8+ ) `HappyStk` happyRest}}}++happyReduce_3 = happyReduce 8# 0# happyReduction_3+happyReduction_3 (happy_x_8 `HappyStk`+ happy_x_7 `HappyStk`+ happy_x_6 `HappyStk`+ happy_x_5 `HappyStk`+ happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut5 happy_x_3 of { happy_var_3 -> + case happyOut4 happy_x_5 of { happy_var_5 -> + case happyOut4 happy_x_8 of { happy_var_8 -> + happyIn4+ (Pi happy_var_3 happy_var_5 happy_var_8+ ) `HappyStk` happyRest}}}++happyReduce_4 = happySpecReduce_3 0# happyReduction_4+happyReduction_4 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut6 happy_x_1 of { happy_var_1 -> + case happyOut4 happy_x_3 of { happy_var_3 -> + happyIn4+ (Pi "_" happy_var_1 happy_var_3+ )}}++happyReduce_5 = happySpecReduce_3 1# happyReduction_5+happyReduction_5 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOutTok happy_x_1 of { (Lexer.Label happy_var_1) -> + case happyOutTok happy_x_3 of { (Lexer.Number happy_var_3) -> + happyIn5+ (V happy_var_1 happy_var_3+ )}}++happyReduce_6 = happySpecReduce_1 1# happyReduction_6+happyReduction_6 happy_x_1+ = case happyOutTok happy_x_1 of { (Lexer.Label happy_var_1) -> + happyIn5+ (V happy_var_1 0+ )}++happyReduce_7 = happySpecReduce_2 2# happyReduction_7+happyReduction_7 happy_x_2+ happy_x_1+ = case happyOut6 happy_x_1 of { happy_var_1 -> + case happyOut7 happy_x_2 of { happy_var_2 -> + happyIn6+ (App happy_var_1 happy_var_2+ )}}++happyReduce_8 = happySpecReduce_1 2# happyReduction_8+happyReduction_8 happy_x_1+ = case happyOut7 happy_x_1 of { happy_var_1 -> + happyIn6+ (happy_var_1+ )}++happyReduce_9 = happySpecReduce_1 3# happyReduction_9+happyReduction_9 happy_x_1+ = case happyOut5 happy_x_1 of { happy_var_1 -> + happyIn7+ (Var happy_var_1+ )}++happyReduce_10 = happySpecReduce_1 3# happyReduction_10+happyReduction_10 happy_x_1+ = happyIn7+ (Const Star+ )++happyReduce_11 = happySpecReduce_1 3# happyReduction_11+happyReduction_11 happy_x_1+ = happyIn7+ (Const Box+ )++happyReduce_12 = happySpecReduce_3 3# happyReduction_12+happyReduction_12 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut4 happy_x_2 of { happy_var_2 -> + happyIn7+ (happy_var_2+ )}++happyNewToken action sts stk+ = lexer(\tk -> + let cont i = happyDoAction i tk action sts stk in+ case tk of {+ Lexer.EOF -> happyDoAction 12# tk action sts stk;+ Lexer.OpenParen -> cont 1#;+ Lexer.CloseParen -> cont 2#;+ Lexer.Colon -> cont 3#;+ Lexer.At -> cont 4#;+ Lexer.Star -> cont 5#;+ Lexer.Box -> cont 6#;+ Lexer.Arrow -> cont 7#;+ Lexer.Lambda -> cont 8#;+ Lexer.Pi -> cont 9#;+ Lexer.Label happy_dollar_dollar -> cont 10#;+ Lexer.Number happy_dollar_dollar -> cont 11#;+ _ -> happyError' tk+ })++happyError_ 12# tk = happyError' tk+happyError_ _ tk = happyError' tk++happyThen :: () => Lex a -> (a -> Lex b) -> Lex b+happyThen = (>>=)+happyReturn :: () => a -> Lex a+happyReturn = (return)+happyThen1 = happyThen+happyReturn1 :: () => a -> Lex a+happyReturn1 = happyReturn+happyError' :: () => (Token) -> Lex a+happyError' tk = parseError tk++parseExpr = happySomeParser where+ happySomeParser = happyThen (happyParse 0#) (\x -> happyReturn (happyOut4 x))++happySeq = happyDontSeq+++-- | The specific parsing error+data ParseMessage+ -- | Lexing failed, returning the remainder of the text+ = Lexing Text+ -- | Parsing failed, returning the invalid token+ | Parsing Token+ deriving (Show)++{- This is purely to satisfy the unnecessary `Error` constraint for `ErrorT`++ I will switch to `ExceptT` when the Haskell Platform incorporates+ `transformers-0.4.*`.+-}+instance Error ParseMessage where++type Status = (Position, Producer Token (State Position) (Maybe Text))++type Lex = ErrorT ParseMessage (State Status)++-- To avoid an explicit @mmorph@ dependency+generalize :: Monad m => Identity a -> m a+generalize = return . runIdentity++lexer :: (Token -> Lex a) -> Lex a+lexer k = do+ x <- lift (do+ p <- use _2+ hoist generalize (zoom _1 (next p)) )+ case x of+ Left ml -> case ml of+ Nothing -> k Lexer.EOF+ Just le -> throwError (Lexing le)+ Right (token, p') -> do+ lift (_2 .= p')+ k token++parseError :: Token -> Lex a+parseError token = throwError (Parsing token)++-- | Parse an `Expr` from `Text` or return a `ParseError` if parsing fails+exprFromText :: Text -> Either ParseError Expr+exprFromText text = case runState (runErrorT parseExpr) initialStatus of+ (x, (position, _)) -> case x of+ Left e -> Left (ParseError position e)+ Right expr -> Right expr+ where+ initialStatus = (Lexer.P 1 0, Lexer.lexExpr text)++-- | Structured type for parsing errors+data ParseError = ParseError+ { position :: Position+ , parseMessage :: ParseMessage+ } deriving (Show)++-- | Pretty-print a `ParseError`+prettyParseError :: ParseError -> Text+prettyParseError (ParseError (Lexer.P l c) e) = Builder.toLazyText (+ "Line: " <> decimal l <> "\n"+ <> "Column: " <> decimal c <> "\n"+ <> "\n"+ <> case e of+ Lexing r ->+ "Lexing: \"" <> Builder.fromLazyText remainder <> dots <> "\"\n"+ <> "\n"+ <> "Error: Lexing failed\n"+ where+ remainder = Text.takeWhile (/= '\n') (Text.take 64 r)+ dots = if Text.length r > 64 then "..." else mempty+ Parsing t ->+ "Parsing: " <> Builder.fromString (show t) <> "\n"+ <> "\n"+ <> "Error: Parsing failed\n" )+{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "<built-in>" #-}+{-# LINE 1 "<command-line>" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+-- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp ++{-# LINE 30 "templates/GenericTemplate.hs" #-}+++data Happy_IntList = HappyCons Happy_GHC_Exts.Int# Happy_IntList++++++{-# LINE 51 "templates/GenericTemplate.hs" #-}++{-# LINE 61 "templates/GenericTemplate.hs" #-}++{-# LINE 70 "templates/GenericTemplate.hs" #-}++infixr 9 `HappyStk`+data HappyStk a = HappyStk a (HappyStk a)++-----------------------------------------------------------------------------+-- starting the parse++happyParse start_state = happyNewToken start_state notHappyAtAll notHappyAtAll++-----------------------------------------------------------------------------+-- Accepting the parse++-- If the current token is 0#, it means we've just accepted a partial+-- parse (a %partial parser). We must ignore the saved token on the top of+-- the stack in this case.+happyAccept 0# tk st sts (_ `HappyStk` ans `HappyStk` _) =+ happyReturn1 ans+happyAccept j tk st sts (HappyStk ans _) = + (happyTcHack j (happyTcHack st)) (happyReturn1 ans)++-----------------------------------------------------------------------------+-- Arrays only: do the next action++++happyDoAction i tk st+ = {- nothing -}+++ case action of+ 0# -> {- nothing -}+ happyFail i tk st+ -1# -> {- nothing -}+ happyAccept i tk st+ n | (n Happy_GHC_Exts.<# (0# :: Happy_GHC_Exts.Int#)) -> {- nothing -}++ (happyReduceArr Happy_Data_Array.! rule) i tk st+ where rule = (Happy_GHC_Exts.I# ((Happy_GHC_Exts.negateInt# ((n Happy_GHC_Exts.+# (1# :: Happy_GHC_Exts.Int#))))))+ n -> {- nothing -}+++ happyShift new_state i tk st+ where (new_state) = (n Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#))+ where (off) = indexShortOffAddr happyActOffsets st+ (off_i) = (off Happy_GHC_Exts.+# i)+ check = if (off_i Happy_GHC_Exts.>=# (0# :: Happy_GHC_Exts.Int#))+ then (indexShortOffAddr happyCheck off_i Happy_GHC_Exts.==# i)+ else False+ (action)+ | check = indexShortOffAddr happyTable off_i+ | otherwise = indexShortOffAddr happyDefActions st++{-# LINE 130 "templates/GenericTemplate.hs" #-}+++indexShortOffAddr (HappyA# arr) off =+ Happy_GHC_Exts.narrow16Int# i+ where+ i = Happy_GHC_Exts.word2Int# (Happy_GHC_Exts.or# (Happy_GHC_Exts.uncheckedShiftL# high 8#) low)+ high = Happy_GHC_Exts.int2Word# (Happy_GHC_Exts.ord# (Happy_GHC_Exts.indexCharOffAddr# arr (off' Happy_GHC_Exts.+# 1#)))+ low = Happy_GHC_Exts.int2Word# (Happy_GHC_Exts.ord# (Happy_GHC_Exts.indexCharOffAddr# arr off'))+ off' = off Happy_GHC_Exts.*# 2#++++++data HappyAddr = HappyA# Happy_GHC_Exts.Addr#+++++-----------------------------------------------------------------------------+-- HappyState data type (not arrays)++{-# LINE 163 "templates/GenericTemplate.hs" #-}++-----------------------------------------------------------------------------+-- Shifting a token++happyShift new_state 0# tk st sts stk@(x `HappyStk` _) =+ let (i) = (case Happy_GHC_Exts.unsafeCoerce# x of { (Happy_GHC_Exts.I# (i)) -> i }) in+-- trace "shifting the error token" $+ happyDoAction i tk new_state (HappyCons (st) (sts)) (stk)++happyShift new_state i tk st sts stk =+ happyNewToken new_state (HappyCons (st) (sts)) ((happyInTok (tk))`HappyStk`stk)++-- happyReduce is specialised for the common cases.++happySpecReduce_0 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_0 nt fn j tk st@((action)) sts stk+ = happyGoto nt j tk st (HappyCons (st) (sts)) (fn `HappyStk` stk)++happySpecReduce_1 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_1 nt fn j tk _ sts@((HappyCons (st@(action)) (_))) (v1`HappyStk`stk')+ = let r = fn v1 in+ happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk'))++happySpecReduce_2 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_2 nt fn j tk _ (HappyCons (_) (sts@((HappyCons (st@(action)) (_))))) (v1`HappyStk`v2`HappyStk`stk')+ = let r = fn v1 v2 in+ happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk'))++happySpecReduce_3 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_3 nt fn j tk _ (HappyCons (_) ((HappyCons (_) (sts@((HappyCons (st@(action)) (_))))))) (v1`HappyStk`v2`HappyStk`v3`HappyStk`stk')+ = let r = fn v1 v2 v3 in+ happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk'))++happyReduce k i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happyReduce k nt fn j tk st sts stk+ = case happyDrop (k Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#)) sts of+ sts1@((HappyCons (st1@(action)) (_))) ->+ let r = fn stk in -- it doesn't hurt to always seq here...+ happyDoSeq r (happyGoto nt j tk st1 sts1 r)++happyMonadReduce k nt fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happyMonadReduce k nt fn j tk st sts stk =+ happyThen1 (fn stk tk) (\r -> happyGoto nt j tk st1 sts1 (r `HappyStk` drop_stk))+ where (sts1@((HappyCons (st1@(action)) (_)))) = happyDrop k (HappyCons (st) (sts))+ drop_stk = happyDropStk k stk++happyMonad2Reduce k nt fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happyMonad2Reduce k nt fn j tk st sts stk =+ happyThen1 (fn stk tk) (\r -> happyNewToken new_state sts1 (r `HappyStk` drop_stk))+ where (sts1@((HappyCons (st1@(action)) (_)))) = happyDrop k (HappyCons (st) (sts))+ drop_stk = happyDropStk k stk++ (off) = indexShortOffAddr happyGotoOffsets st1+ (off_i) = (off Happy_GHC_Exts.+# nt)+ (new_state) = indexShortOffAddr happyTable off_i+++++happyDrop 0# l = l+happyDrop n (HappyCons (_) (t)) = happyDrop (n Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#)) t++happyDropStk 0# l = l+happyDropStk n (x `HappyStk` xs) = happyDropStk (n Happy_GHC_Exts.-# (1#::Happy_GHC_Exts.Int#)) xs++-----------------------------------------------------------------------------+-- Moving to a new state after a reduction+++happyGoto nt j tk st = + {- nothing -}+ happyDoAction j tk new_state+ where (off) = indexShortOffAddr happyGotoOffsets st+ (off_i) = (off Happy_GHC_Exts.+# nt)+ (new_state) = indexShortOffAddr happyTable off_i+++++-----------------------------------------------------------------------------+-- Error recovery (0# is the error token)++-- parse error if we are in recovery and we fail again+happyFail 0# tk old_st _ stk@(x `HappyStk` _) =+ let (i) = (case Happy_GHC_Exts.unsafeCoerce# x of { (Happy_GHC_Exts.I# (i)) -> i }) in+-- trace "failing" $ + happyError_ i tk++{- We don't need state discarding for our restricted implementation of+ "error". In fact, it can cause some bogus parses, so I've disabled it+ for now --SDM++-- discard a state+happyFail 0# tk old_st (HappyCons ((action)) (sts)) + (saved_tok `HappyStk` _ `HappyStk` stk) =+-- trace ("discarding state, depth " ++ show (length stk)) $+ happyDoAction 0# tk action sts ((saved_tok`HappyStk`stk))+-}++-- Enter error recovery: generate an error token,+-- save the old token and carry on.+happyFail i tk (action) sts stk =+-- trace "entering error recovery" $+ happyDoAction 0# tk action sts ( (Happy_GHC_Exts.unsafeCoerce# (Happy_GHC_Exts.I# (i))) `HappyStk` stk)++-- Internal happy errors:++notHappyAtAll :: a+notHappyAtAll = error "Internal Happy error\n"++-----------------------------------------------------------------------------+-- Hack to get the typechecker to accept our action functions+++happyTcHack :: Happy_GHC_Exts.Int# -> a -> a+happyTcHack x y = y+{-# INLINE happyTcHack #-}+++-----------------------------------------------------------------------------+-- Seq-ing. If the --strict flag is given, then Happy emits +-- happySeq = happyDoSeq+-- otherwise it emits+-- happySeq = happyDontSeq++happyDoSeq, happyDontSeq :: a -> b -> b+happyDoSeq a b = a `seq` b+happyDontSeq a b = b++-----------------------------------------------------------------------------+-- Don't inline any functions from the template. GHC has a nasty habit+-- of deciding to inline happyGoto everywhere, which increases the size of+-- the generated parser quite a bit.+++{-# NOINLINE happyDoAction #-}+{-# NOINLINE happyTable #-}+{-# NOINLINE happyCheck #-}+{-# NOINLINE happyActOffsets #-}+{-# NOINLINE happyGotoOffsets #-}+{-# NOINLINE happyDefActions #-}++{-# NOINLINE happyShift #-}+{-# NOINLINE happySpecReduce_0 #-}+{-# NOINLINE happySpecReduce_1 #-}+{-# NOINLINE happySpecReduce_2 #-}+{-# NOINLINE happySpecReduce_3 #-}+{-# NOINLINE happyReduce #-}+{-# NOINLINE happyMonadReduce #-}+{-# NOINLINE happyGoto #-}+{-# NOINLINE happyFail #-}++-- end of Happy Template.
+ exec/Main.hs view
@@ -0,0 +1,33 @@+module Main where++import Data.Monoid (mempty)+import qualified Data.Text.Lazy.IO as Text+import Morte.Core (typeOf, prettyTypeError, prettyExpr, normalize)+import Morte.Parser (exprFromText, prettyParseError)+import Options.Applicative+import System.IO (stderr)+import System.Exit (exitFailure)++main :: IO ()+main = do+ execParser $ info (helper <*> pure ())+ ( fullDesc+ <> header "morte - A bare-bones calculus of constructions"+ <> progDesc "Type-check and normalize a Morte program, reading the \+ \program from standard input, writing the program's type \+ \to standard error, and writing the normalized program to\+ \standard output"+ )+ inText <- Text.getContents+ case exprFromText inText of+ Left pe -> do+ Text.hPutStr stderr (prettyParseError pe)+ exitFailure+ Right expr -> case typeOf expr of+ Left te -> do+ Text.hPutStr stderr (prettyTypeError te)+ exitFailure+ Right typeExpr -> do+ Text.hPutStrLn stderr (prettyExpr (normalize typeExpr))+ Text.hPutStrLn stderr mempty+ Text.putStrLn (prettyExpr (normalize expr))
+ morte.cabal view
@@ -0,0 +1,58 @@+Name: morte+Version: 1.0.0+Cabal-Version: >=1.8.0.2+Build-Type: Simple+License: BSD3+License-File: LICENSE+Copyright: 2014 Gabriel Gonzalez+Author: Gabriel Gonzalez+Maintainer: Gabriel439@gmail.com+Bug-Reports: https://github.com/Gabriel439/Haskell-Morte-Library/issues+Synopsis: A bare-bones calculus of constructions+Description: 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+Category: Compiler+Source-Repository head+ Type: git+ Location: https://github.com/Gabriel439/Haskell-Morte-Library++Library+ Hs-Source-Dirs: src+ Build-Depends:+ base >= 4 && < 5 ,+ array >= 0.4.0.0 && < 0.6 ,+ binary < 0.8 ,+ containers < 0.6 ,+ lens-family-core >= 1.0.0 && < 1.2 ,+ pipes >= 4.0.0 && < 4.2 ,+ text >= 0.11.1.0 && < 1.3 ,+ transformers >= 0.2.0.0 && < 0.5+ Exposed-Modules:+ Morte.Core,+ Morte.Lexer,+ Morte.Parser,+ Morte.Tutorial+ Build-Tools: alex, happy+ GHC-Options: -O2++Executable morte+ Hs-Source-Dirs: exec+ Main-Is: Main.hs+ Build-Depends:+ base >= 4 && < 5 ,+ morte ,+ optparse-applicative < 0.11,+ text >= 0.11.1.0 && < 1.3
+ src/Morte/Core.hs view
@@ -0,0 +1,481 @@+{-# LANGUAGE OverloadedStrings, DeriveDataTypeable #-}+{-# OPTIONS_GHC -Wall #-}++{-| 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:++ * Every expression has a unique normal form computed by `normalize`++ * You test expressions for equality of their normal forms using `==`++ * Equational reasoning preserves normal forms+++ 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 (+ -- * Syntax+ Var(..),+ Const(..),+ Expr(..),+ Context,++ -- * Core functions+ typeWith,+ typeOf,+ normalize,++ -- * Utilities+ prettyExpr,+ prettyTypeError,++ -- * Errors+ TypeError(..),+ TypeMessage(..)+ ) where++import Control.Applicative ((<$>), (<*>))+import Control.Exception (Exception)+import Control.Monad.Trans.State (State, evalState, modify)+import qualified Control.Monad.Trans.State as State+import Data.Binary (Binary(get, put), Get)+import Data.Binary.Get (getWord64le)+import Data.Binary.Put (putWord64le)+import Data.IntSet (IntSet)+import qualified Data.IntSet as IntSet+import Data.Monoid (mempty, (<>))+import Data.String (IsString(fromString))+import Data.Text () -- For the `IsString` instance+import Data.Text.Lazy (Text)+import qualified Data.Text.Encoding as Text+import qualified Data.Text.Lazy as Text+import Data.Text.Lazy.Builder (Builder, toLazyText, fromLazyText)+import Data.Text.Lazy.Builder.Int (decimal)+import Data.Typeable (Typeable)+import Data.Word (Word8)++{-| 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 deriving (Eq, Show)++instance Binary Var where+ put (V txt n) = do+ put (Text.encodeUtf8 (Text.toStrict txt))+ putWord64le (fromIntegral n)+ get = do+ bs <- get+ case Text.decodeUtf8' bs of+ Left e ->+ fail (show e)+ Right txt ->+ V (Text.fromStrict txt) <$> fmap fromIntegral getWord64le++instance IsString Var+ where+ fromString str = V (Text.pack str) 0++{-| Constants for the calculus of constructions++ The only axiom is:++> ⊦ * : □++ ... and all four rule pairs are valid:++> ⊦ * ↝ * : *+> ⊦ □ ↝ * : *+> ⊦ * ↝ □ : □+> ⊦ □ ↝ □ : □++-}+data Const = Star | Box deriving (Eq, Show, Bounded, Enum)++instance Binary Const where+ put c = case c of+ Star -> put (0 :: Word8)+ Box -> put (1 :: Word8)+ get = do+ n <- get :: Get Word8+ case n of+ 0 -> return Star+ 1 -> return Box+ _ -> fail "get Const: Invalid tag byte"++axiom :: Const -> Either TypeError Const+axiom Star = return Box+axiom Box = Left (TypeError [] (Const Box) (Untyped Box))++rule :: Const -> Const -> Either TypeError Const+rule Star Box = return Box+rule Star Star = return Star+rule Box Box = return Box+rule Box Star = return Star++-- | Syntax tree for expressions+data Expr+ -- | > Const c ~ c+ = Const Const+ -- | > Var (V x 0) ~ x+ -- > Var (V x n) ~ x@n+ | Var Var+ -- | > Lam x A b ~ λ(x : A) → b+ | Lam Var Expr Expr+ -- | > Pi x A B ~ ∀(x : A) → B+ -- > Pi unused A B ~ A → B+ | Pi Var Expr Expr+ -- | > App f a ~ f a+ | App Expr Expr+ deriving (Show)++instance Eq Expr where+ eL0 == eR0 = evalState (go (normalize eL0) (normalize eR0)) []+ where+ go :: Expr -> Expr -> State [(Var, Var)] Bool+ go (Const cL) (Const cR) = return (cL == cR)+ go (Var xL) (Var xR) = do+ ctx <- State.get+ let x = case lookup xL ctx of+ Nothing -> xL+ Just xR' -> xR'+ return (x == xR)+ go (Lam xL tL bL) (Lam xR tR bR) = do+ modify ((xL, xR):)+ eq1 <- go tL tR+ eq2 <- go bL bR+ return (eq1 && eq2)+ go (Pi xL tL bL) (Pi xR tR bR) = do+ modify ((xL, xR):)+ eq1 <- go tL tR+ eq2 <- go bL bR+ return (eq1 && eq2)+ go (App fL aL) (App fR aR) = do+ b1 <- go fL fR+ b2 <- go aL aR+ return (b1 && b2)+ go _ _ = return False++instance Binary Expr where+ put e = case e of+ Const c -> do+ put (0 :: Word8)+ put c+ Var x -> do+ put (1 :: Word8)+ put x+ Lam x _A b -> do+ put (2 :: Word8)+ put x+ put _A+ put b+ Pi x _A _B -> do+ put (3 :: Word8)+ put x+ put _A+ put _B+ App f a -> do+ put (4 :: Word8)+ put f+ put a++ get = do+ n <- get :: Get Word8+ case n of+ 0 -> Const <$> get+ 1 -> Var <$> get+ 2 -> Lam <$> get <*> get <*> get+ 3 -> Pi <$> get <*> get <*> get+ 4 -> App <$> get <*> get+ _ -> fail "get Expr: Invalid tag byte"++instance IsString Expr+ where+ fromString str = Var (fromString str)++{-| Bound variables and their types++ Earlier `Var`s shadow later matching `Var`s+-}+type Context = [(Var, Expr)]++-- | The specific type error+data TypeMessage+ = UnboundVariable+ | InvalidInputType Expr+ | InvalidOutputType Expr+ | NotAFunction+ | TypeMismatch Expr Expr+ | Untyped Const+ deriving (Show, Typeable)++-- | A structured type error that includes context+data TypeError = TypeError+ { context :: Context+ , current :: Expr+ , typeMessage :: TypeMessage+ } deriving (Show, Typeable)++instance Exception TypeError++buildConst :: Const -> Builder+buildConst c = case c of+ Star -> "*"+ Box -> "□"++buildVar :: Var -> Builder+buildVar (V txt n) =+ fromLazyText txt <> if n == 0 then mempty else "@" <> decimal n++-- | Render a pretty-printed expression as a `Builder`+buildExpr :: Expr -> Builder+buildExpr = go False False+ where+ go :: Bool -> Bool -> Expr -> Builder+ go parenBind parenApp e = case e of+ Const c -> buildConst c+ Var x -> buildVar x+ Lam x _A b ->+ (if parenBind then "(" else "")+ <> "λ("+ <> buildVar x+ <> " : "+ <> go False False _A + <> ") → "+ <> go False False b+ <> (if parenBind then ")" else "")+ Pi x _A b ->+ (if parenBind then "(" else "")+ <> (if used x e+ then "∀(" <> buildVar x <> " : " <> go False False _A <> ")"+ else go True False _A )+ <> " → "+ <> go False False b+ <> (if parenBind then ")" else "")+ App f a ->+ (if parenApp then "(" else "")+ <> go True False f <> " " <> go True True a+ <> (if parenApp then ")" else "")++ used :: Var -> Expr -> Bool+ used x = go'+ where+ go' e = case e of+ Var x' | x == x' -> True+ | otherwise -> False+ Lam _ _A b -> go' _A || go' b+ Pi _ _A b -> go' _A || go' b+ App f a -> go' f || go' a+ Const _ -> False++buildTypeMessage :: TypeMessage -> Builder+buildTypeMessage msg = case msg of+ UnboundVariable ->+ "Error: Unbound variable\n"+ InvalidInputType expr ->+ "Error: Invalid input type\n"+ <> "\n"+ <> "Type: " <> buildExpr expr <> "\n"+ InvalidOutputType expr ->+ "Error: Invalid output type\n"+ <> "\n"+ <> "Type: " <> buildExpr expr <> "\n"+ NotAFunction ->+ "Error: Only functions may be applied to values\n"+ TypeMismatch expr1 expr2 ->+ "Error: Function applied to argument of the wrong type\n"+ <> "\n"+ <> "Expected type: " <> buildExpr expr1 <> "\n"+ <> "Argument type: " <> buildExpr expr2 <> "\n"+ Untyped c ->+ "Error: " <> buildConst c <> " has no type\n"++buildTypeError :: TypeError -> Builder+buildTypeError (TypeError ctx expr msg)+ = ( if Text.null (toLazyText buildContext )+ then mempty+ else "Context:\n" <> buildContext <> "\n"+ )+ <> "Expression: " <> buildExpr expr <> "\n"+ <> "\n"+ <> buildTypeMessage msg+ where+ buildKV (key, val) = buildVar key <> " : " <> buildExpr val++ buildContext =+ (fromLazyText . Text.unlines . map (toLazyText . buildKV) . reverse) ctx+++{-| Find all free variables with a given label and return their `Int`s++ Use this to generate a new variable which does not clash with existing free+ variables+-}+freeOf :: Text -> Expr -> IntSet+freeOf txt = go+ where+ go e = case e of+ Var (V txt' n) | txt == txt' -> IntSet.singleton n+ | otherwise -> IntSet.empty+ Lam (V _ n ) _ b -> IntSet.delete n (go b)+ Pi (V _ n ) _ b -> IntSet.delete n (go b)+ App f a -> IntSet.union (go f) (go a)+ Const _ -> IntSet.empty++{-| Substitute all occurrences of a variable with an expression++> subst x C B ~ B[x := C]+-}+subst :: Var -> Expr -> Expr -> Expr+subst x0 e0 = go+ where+ go e = case e of+ Lam x _A b -> helper Lam x _A b+ Pi x _A b -> helper Pi x _A b+ App f a -> App (go f) (go a)+ Var x -> if (x == x0) then e0 else e+ Const _ -> e++ helper c x@(V txt n) _A b =+ if x == x0+ then c x _A b -- x shadows x0+ else+ let fs = IntSet.union (freeOf txt (Var x0)) (freeOf txt e0)+ in if IntSet.member n fs+ then+ let x' = V txt (IntSet.findMax fs + 1)+ in c x' (go _A) (go (subst x (Var x') b))+ else c x (go _A) (go b)++{-| 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+typeWith ctx e = case e of+ Const c -> fmap Const (axiom c)+ Var x -> case lookup x ctx of+ Nothing -> Left (TypeError ctx e UnboundVariable)+ Just a -> return a+ Lam x _A b -> do+ _B <- typeWith ((x, _A):ctx) b+ let p = Pi x _A _B+ _t <- typeWith ctx p+ return p+ Pi x _A _B -> do+ eS <- fmap whnf (typeWith ctx _A)+ s <- case eS of+ Const s -> return s+ _ -> Left (TypeError ctx e (InvalidInputType _A))+ let ctx' = (x, _A):ctx+ eT <- fmap whnf (typeWith ctx' _B)+ t <- case eT of+ Const t -> return t+ _ -> Left (TypeError ctx' e (InvalidOutputType _B))+ fmap Const (rule s t)+ App f a -> do+ e' <- fmap whnf (typeWith ctx f)+ (x, _A, _B) <- case e' of+ Pi x _A _B -> return (x, _A, _B)+ _ -> Left (TypeError ctx e NotAFunction)+ _A' <- typeWith ctx a+ let nf_A = normalize _A + nf_A' = normalize _A'+ if nf_A == nf_A'+ then return (subst x a _B)+ else Left (TypeError ctx e (TypeMismatch nf_A nf_A'))++{-| `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+typeOf = typeWith []++-- | Reduce an expression to weak-head normal form+whnf :: Expr -> Expr+whnf e = case e of+ App f a -> case whnf f of+ Lam x _A b -> whnf (subst x a b) -- Beta reduce+ _ -> e+ _ -> e++-- | Returns whether a variable is free in an expression+freeIn :: Var -> Expr -> Bool+freeIn x = go+ where+ go e = case e of+ Lam x' _A b -> x /= x' && (go _A || go b)+ Pi x' _A b -> x /= x' && (go _A || go b)+ Var x' -> x == x'+ App f a -> go f || go a+ Const _ -> False++{-| 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+normalize e = case e of+ Lam x _A b -> case b' of+ App f a -> case a of+ Var x' | x == x' && not (x `freeIn` f) -> f -- Eta reduce+ | otherwise -> e'+ _ -> e'+ _ -> e'+ where+ b' = normalize b+ e' = Lam x (normalize _A) b'+ Pi x _A b -> Pi x (normalize _A) (normalize b)+ App f _C -> case normalize f of+ Lam x _A _B -> normalize (subst x _C _B) -- Beta reduce+ f' -> App f' (normalize _C)+ Var _ -> e+ Const _ -> e++{-| Pretty-print an expression++ The result is a syntactically valid Morte program+-}+prettyExpr :: Expr -> Text+prettyExpr = toLazyText . buildExpr++-- | Pretty-print a type error+prettyTypeError :: TypeError -> Text+prettyTypeError = toLazyText . buildTypeError
+ src/Morte/Lexer.x view
@@ -0,0 +1,153 @@+{+{-# LANGUAGE OverloadedStrings #-}++-- | Lexing logic for the Morte language+module Morte.Lexer (+ -- * Lexer+ lexExpr,++ -- * Types+ Token(..),+ Position(..)+ ) where++import Control.Monad.Trans.State.Strict (State)+import Data.Bits (shiftR, (.&.))+import Data.Char (ord, digitToInt)+import Data.Text.Lazy (Text)+import qualified Data.Text.Lazy as Text+import Data.Word (Word8)+import Lens.Family.State.Strict ((.=), (+=))+import Pipes (Producer, lift, yield)++}++$digit = 0-9++-- Same as Haskell+$opchar = [\!\#\$\%\&\*\+\.\/\<\=\>\?\@\\\^\|\-\~]++-- I intentionally disallow `'` or digits in variable labels.+-- Use the `label@number` syntax to disambiguate variables with the same label+$labelchar = [A-Za-z_]++$whiteNoNewline = $white # \n++tokens :-++ $whiteNoNewline+ ;+ \n { \_ -> lift (do+ line += 1+ column .= 0 ) }+ "--".* ;+ "(" { \_ -> yield OpenParen }+ ")" { \_ -> yield CloseParen }+ ":" { \_ -> yield Colon }+ "@" { \_ -> yield At }+ "*" { \_ -> yield Star }+ "BOX" | "□" { \_ -> yield Box }+ "->" | "→" { \_ -> yield Arrow }+ "\/" | "|~|" | "forall" | "∀" | "Π" { \_ -> yield Pi }+ "\" | "λ" { \_ -> yield Lambda }+ $digit+ { \text -> yield (Number (toInt text)) }+ $labelchar+ | "(" $opchar+ ")" { \text -> yield (Label text) }++{+toInt :: Text -> Int+toInt = Text.foldl' (\x c -> 10 * x + digitToInt c) 0++-- This was lifted almost intact from the @alex@ source code+encode :: Char -> (Word8, [Word8])+encode c = (fromIntegral h, map fromIntegral t)+ where+ (h, t) = go (ord c)++ go n+ | n <= 0x7f = (n, [])+ | n <= 0x7ff = (0xc0 + (n `shiftR` 6), [0x80 + n .&. 0x3f])+ | n <= 0xffff =+ ( 0xe0 + (n `shiftR` 12)+ , [ 0x80 + ((n `shiftR` 6) .&. 0x3f)+ , 0x80 + n .&. 0x3f+ ]+ )+ | otherwise =+ ( 0xf0 + (n `shiftR` 18)+ , [ 0x80 + ((n `shiftR` 12) .&. 0x3f)+ , 0x80 + ((n `shiftR` 6) .&. 0x3f)+ , 0x80 + n .&. 0x3f+ ]+ )++-- | The cursor's location while lexing the text+data Position = P+ { lineNo :: {-# UNPACK #-} !Int+ , columnNo :: {-# UNPACK #-} !Int+ } deriving (Show)++-- line :: Lens' Position Int+line :: Functor f => (Int -> f Int) -> Position -> f Position+line k (P l c) = fmap (\l' -> P l' c) (k l)++-- column :: Lens' Position Int+column :: Functor f => (Int -> f Int) -> Position -> f Position+column k (P l c) = fmap (\c' -> P l c') (k c)++{- @alex@ does not provide a `Text` wrapper, so the following code just modifies+ the code from their @basic@ wrapper to work with `Text`++ I could not get the @basic-bytestring@ wrapper to work; it does not correctly+ recognize Unicode regular expressions.+-}+data AlexInput = AlexInput+ { prevChar :: Char+ , currBytes :: [Word8]+ , currInput :: Text+ }++alexGetByte :: AlexInput -> Maybe (Word8,AlexInput)+alexGetByte (AlexInput c bytes text) = case bytes of+ b:ytes -> Just (b, AlexInput c ytes text)+ [] -> case Text.uncons text of+ Nothing -> Nothing+ Just (t, ext) -> case encode t of+ (b, ytes) -> Just (b, AlexInput t ytes ext)++alexInputPrevChar :: AlexInput -> Char+alexInputPrevChar = prevChar++{-| 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)+lexExpr text = go (AlexInput '\n' [] text)+ where+ go input = case alexScan input 0 of+ AlexEOF -> return Nothing+ AlexError (AlexInput _ _ text) -> return (Just text)+ AlexSkip input' len -> do+ lift (column += len)+ go input'+ AlexToken input' len act -> do+ act (Text.take (fromIntegral len) (currInput input))+ lift (column += len)+ go input'++-- | Token type, used to communicate between the lexer and parser+data Token+ = OpenParen+ | CloseParen+ | Colon+ | At+ | Star+ | Box+ | Arrow+ | Lambda+ | Pi+ | Label Text+ | Number Int+ | EOF+ deriving (Show)+}
+ src/Morte/Parser.y view
@@ -0,0 +1,147 @@+{+{-# LANGUAGE OverloadedStrings #-}++-- | Parsing logic for the Morte language++module Morte.Parser (+ -- * Parser+ exprFromText,++ -- * Errors+ prettyParseError,+ ParseError(..),+ ParseMessage(..)+ ) where++import Control.Monad.Trans.Error (ErrorT, Error(..), throwError, runErrorT)+import Control.Monad.Trans.State.Strict (State, runState)+import Data.Functor.Identity (Identity, runIdentity)+import Data.Monoid (mempty, (<>))+import Data.Text.Lazy (Text)+import qualified Data.Text.Lazy as Text+import qualified Data.Text.Lazy.Builder as Builder+import Data.Text.Lazy.Builder.Int (decimal)+import Lens.Family.Stock (_1, _2)+import Lens.Family.State.Strict ((.=), use, zoom)+import Morte.Core (Var(..), Const(..), Expr(..))+import qualified Morte.Lexer as Lexer+import Morte.Lexer (Token, Position)+import Pipes (Producer, hoist, lift, next)++}++%name parseExpr+%tokentype { Token }+%monad { Lex }+%lexer { lexer } { Lexer.EOF }+%error { parseError }++%token+ '(' { Lexer.OpenParen }+ ')' { Lexer.CloseParen }+ ':' { Lexer.Colon }+ '@' { Lexer.At }+ '*' { Lexer.Star }+ 'BOX' { Lexer.Box }+ '->' { Lexer.Arrow }+ '\\' { Lexer.Lambda }+ '|~|' { Lexer.Pi }+ label { Lexer.Label $$ }+ number { Lexer.Number $$ }++%%++Expr :: { Expr }+ : BExpr { $1 }+ | '\\' '(' VExpr ':' Expr ')' '->' Expr { Lam $3 $5 $8 }+ | '|~|' '(' VExpr ':' Expr ')' '->' Expr { Pi $3 $5 $8 }+ | BExpr '->' Expr { Pi "_" $1 $3 }++VExpr :: { Var }+ : label '@' number { V $1 $3 }+ | label { V $1 0 }++BExpr :: { Expr }+ : BExpr AExpr { App $1 $2 }+ | AExpr { $1 }++AExpr :: { Expr }+ : VExpr { Var $1 }+ | '*' { Const Star }+ | 'BOX' { Const Box }+ | '(' Expr ')' { $2 }++{+-- | The specific parsing error+data ParseMessage+ -- | Lexing failed, returning the remainder of the text+ = Lexing Text+ -- | Parsing failed, returning the invalid token+ | Parsing Token+ deriving (Show)++{- This is purely to satisfy the unnecessary `Error` constraint for `ErrorT`++ I will switch to `ExceptT` when the Haskell Platform incorporates+ `transformers-0.4.*`.+-}+instance Error ParseMessage where++type Status = (Position, Producer Token (State Position) (Maybe Text))++type Lex = ErrorT ParseMessage (State Status)++-- To avoid an explicit @mmorph@ dependency+generalize :: Monad m => Identity a -> m a+generalize = return . runIdentity++lexer :: (Token -> Lex a) -> Lex a+lexer k = do+ x <- lift (do+ p <- use _2+ hoist generalize (zoom _1 (next p)) )+ case x of+ Left ml -> case ml of+ Nothing -> k Lexer.EOF+ Just le -> throwError (Lexing le)+ Right (token, p') -> do+ lift (_2 .= p')+ k token++parseError :: Token -> Lex a+parseError token = throwError (Parsing token)++-- | Parse an `Expr` from `Text` or return a `ParseError` if parsing fails+exprFromText :: Text -> Either ParseError Expr+exprFromText text = case runState (runErrorT parseExpr) initialStatus of+ (x, (position, _)) -> case x of+ Left e -> Left (ParseError position e)+ Right expr -> Right expr+ where+ initialStatus = (Lexer.P 1 0, Lexer.lexExpr text)++-- | Structured type for parsing errors+data ParseError = ParseError+ { position :: Position+ , parseMessage :: ParseMessage+ } deriving (Show)++-- | Pretty-print a `ParseError`+prettyParseError :: ParseError -> Text+prettyParseError (ParseError (Lexer.P l c) e) = Builder.toLazyText (+ "Line: " <> decimal l <> "\n"+ <> "Column: " <> decimal c <> "\n"+ <> "\n"+ <> case e of+ Lexing r ->+ "Lexing: \"" <> Builder.fromLazyText remainder <> dots <> "\"\n"+ <> "\n"+ <> "Error: Lexing failed\n"+ where+ remainder = Text.takeWhile (/= '\n') (Text.take 64 r)+ dots = if Text.length r > 64 then "..." else mempty+ Parsing t ->+ "Parsing: " <> Builder.fromString (show t) <> "\n"+ <> "\n"+ <> "Error: Parsing failed\n" )+}
+ src/Morte/Tutorial.hs view
@@ -0,0 +1,2042 @@+{-| 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:++ * Be super-optimizable - by disabling unrestricted recursion++ * Be portable - so you can transmit code between different languages++ * Be efficient - so that Morte can scale to large code bases++ * Be simple - so people can reason about Morte's soundness+++ 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 (+ -- * Introduction+ -- $introduction++ -- * Desugaring+ -- $desugaring++ -- ** Let+ -- $let++ -- ** Simple types+ -- $types++ -- ** Newtypes+ -- $newtypes++ -- ** Recursion+ -- $recursion++ -- ** Existential Quantification+ -- $existential++ -- ** Corecursion+ -- $corecursion++ -- * Optimization+ -- $optimization++ -- ** Normalization+ -- $normalization++ -- * Effects+ -- $effects++ -- * Portability+ -- $portability++ -- * Conclusion+ -- $conclusion+ ) where++import Morte.Core++{- $introduction+ You can test out your first Morte program using the @morte@ executable+ provided by this library. This executable reads a Morte program from+ @stdin@, outputs the type of the program to @stderr@, and outputs the+ optimized program to @stdout@.++ We'll begin by translating Haskell's identity function to Morte. For+ reference, `id` is defined in Haskell as:++> id :: a -> a+> id x = x++ We will enter the equivalent Morte program at the command line:++> $ morte+> \(a : *) -> \(x : a) -> x <Enter>+> <Ctrl-D>+> ∀(a : *) → a → a+> +> λ(a : *) → λ(x : a) → x+> $++ The compiler outputs two lines. The first line is the type, which is output+ to @stderr@. The second line is the optimized program, which is output to+ @stdout@.++ Compare the type output by the compiler with the equivalent Haskell type:++> -- Haskell+> id :: a -> a+>+> -- Morte+> ∀(a : *) → a → a++ The first thing you'll notice is that Morte explicitly quantifies all types.+ In Haskell, you can do this, too, using the @ExplicitForAll@ extension:++> id :: forall a . a -> a++ The Morte compiler uses a Unicode forall symbol to sweeten the output, but+ Morte also accepts other equivalents, too, such as:++> -- Ascii '∀'+> \/(a : *) -> a -> a+>+> -- English+> forall (a : *) -> a -> a+>+> -- Unicode Capital Pi+> Π(a : *) -> a -> a+>+> -- ASCII 'Π'+> |~|(a : *) -> a -> a++ Also, Morte accepts both Unicode and ASCII arrow symbols.++ The compiler's last output line is the optimized program, which in this case+ is identical to our original program (except sweetened with Unicode).+ Compare to the equivalent Haskell code:++> -- Haskell code, desugared to a lambda expression+> id = \x -> x+>+> λ(a : *) → λ(x : a) → x++ Notice that Morte explicitly binds the type @\'a\'@ as an additional+ parameter. We use this to assign a type to the bound variable @x@. In+ Morte, all bound variables must be explicitly annotated with a type because+ Morte does not perform any type inference.++ Now let's modify our program to accept an external type, such as @String@+ and then we can specialize our identity function to that type. Remember+ that the type is just another argument to our function, so we specialize+ our identity function by just applying it to @String@.++ We'll use a file this time instead of entering the program at the command+ line:++> -- id.mt+>+> -- Morte accepts comments+>+> -- Also, whitespace is not significant+> \(String : *) ->+> (\(a : *) -> \(x : a) -> x) String++ Then we'll type-check and optimize this program:++> $ morte < id.mt+> ∀(String : *) → String → String+> +> λ(String : *) → λ(x : String) → x++ Morte optimizes our program to the identity function on @String@s, but if+ you notice carefully this is indistinguishable from our original identity+ function because we still take the @String@ type as parameter. The only+ difference is that we've renamed @\'a\'@ to @String@.++ In fact, Morte knows this and can detect when two expressions are equal+ up to renaming of bound variables (a.k.a. \"alpha-equivalence\"). The+ compiler does not support testing programs for equality, but the library+ does:+ +> $ ghci+> Prelude> import Morte.Core+> Prelude Morte.Core> :set -XOverloadedStrings+> Prelude Morte.Core> let id = Lam "a" (Const Star) (Lam "x" "a" "x")+> Prelude Morte.Core> let id' = Lam "String" (Const Star) (App id "String")+> Prelude Morte.Core> id == id'+> True++ In fact, Morte's equality operator also detects \"beta-equivalence\" and+ \"eta-equivalence\", too, which you can think of as equivalence of normal+ forms.++ We can even use this equality operator to prove the equivalence of many (but+ not all) complex programs, but first we need to learn how to define more+ complex abstractions using Morte's restrictive language, as outlined in the+ next section.+-}++{- $desugaring+ The `Expr` type defines Morte's syntax, which is very simple:++> data Expr+> = Const Const -- Type system constants+> | Var Var -- Bound variables+> | Lam Var Expr Expr -- Lambda+> | Pi Var Expr Expr -- "forall"+> | App Expr Expr -- Function application++ For example, you can see what @id'@ from the previous section expands out to+ by using the `Show` instance for `Expr`:+ +> Lam (V "String" 0) (Const Star) (+> App (Lam (V "a" 0) (Const Star) (+> Lam (V "x" 0) (Var (V "a" 0)) (Var (V "x" 0))))+> (Var (V "String" 0)))++ ... although Morte provides syntactic sugar for building expressions by+ hand using the `OverloadedStrings` instance, so you could instead write:++> Lam "String" (Const Star) (+> App (Lam "a" (Const Star)( Lam "x" "a" "a")) "String" )++ Note that Morte's syntax does not include:++ * @let@ expressions++ * @case@ expressions++ * Built-in values other than functions++ * Built-in types other than function types++ * @newtype@s++ * Support for multiple expressions/statements++ * Modules or imports++ * Recursion / Corecursion+++ Future front-ends to Morte will support these higher-level abstractions, but+ for now you must desugar all of these to lambda calculus before Morte can+ type-check and optimize your program. The following sections explain how to+ desugar these abstractions from a Haskell-like language.+-}++{- $let+ Given a non-recursive @let@ statement of the form:++> let var1 :: type1+> var1 = expr1+>+> var2 :: type2+> var2 = expr2+>+> ...+>+> varN :: typeN+> varN = exprN+>+> in result++ You can desugar that to:++> (\(var1 : type1) -> \(var2 : type2) -> ... -> \(varN : typeN) -> result) expr1 expr2 ... exprN++ Remember that whitespace is not significant, so you can also write that as:++> ( \(var1 : type1)+> -> \(var2 : type2)+> -> ...+> -> \(varN : typeN)+> -> result+> )+> expr1+> expr2+> ...+> exprN++ The Morte compiler does not mistake @expr1@ through @exprN@ for additional+ top-level expresions, because a Morte program only consists of a single+ expression.++ Carefully note that the following expression:++> let var1 : type1+> var1 = expr1+>+> var2 : type2+> var2 = type2+>+> in result++ ... is not the same as:++> let var1 : type1+> var1 = expr1+>+> in let var2 : type2+> var2 = expr2+>+> in result++ They desugar to different Morte code and sometimes the distinction between+ the two is significant.++ Using @let@, you can desugar this:++> let id : forall (a : *) -> a -> a+> id = \(a : *) -> \(x : *) -> x+>+> in id (forall (a : *) -> a -> a) id++ ... into this:++> -- id2.mt+>+> ( \(id : forall (a : *) -> a -> a)+> -> id (forall (a : *) -> a -> a) id -- Apply the identity function to itself+> )+> +> -- id+> (\(a : *) -> \(x : a) -> x)++ ... and the compiler will type-check and optimize that to:++> $ morte < id2.mt+> ∀(a : *) → a → a+> +> λ(a : *) → λ(x : a) → x++-}++{- $types+ The following sections use a technique known as Boehm-Berarducci encoding to+ convert recursive data types to lambda terms. If you already know what+ Boehm-Berarducci encoding is then you can skip these sections. You might+ already recognize this technique by the names of overlapping techniques such+ as CPS-encoding, Church-encoding, or F-algebras.++ I'll first explain how to desugar a somewhat complicated non-recursive type+ and then show how this trick specializes to simpler types. The first+ example is quite long, but you'll see that it gets much more compact in the+ simpler examples.++ Given the following non-recursive type:++> let data T a b c = A | B a | C b c+>+> in result++ You can desugar that to the following Morte code:++> -- The type constructor+> ( \(T : * -> * -> * -> *)+>+> -- The value constructors+> -> \(A : forall (a : *) -> forall (b : *) -> forall (c : *) -> T a b c)+> -> \(B : forall (a : *) -> forall (b : *) -> forall (c : *) -> a -> T a b c)+> -> \(C : forall (a : *) -> forall (b : *) -> forall (c : *) -> b -> c -> T a b c)+>+> -- Pattern match on T+> -> \( matchT+> : forall (a : *) -> forall (b : *) -> forall (c : *)+> -> T a b c+> -> forall (r : *)+> -> r -- `A` branch of the pattern match+> -> (a -> r) -- `B` branch of the pattern match+> -> (b -> c -> r) -- `C` branch of the pattern match+> -> r+> )+> -> result+> )+>+> -- A value of type `T a b c` is just a preformed pattern match+> ( \(a : *) -> \(b : *) -> \(c : *)+> -> forall (r : *)+> -> r -- A branch of the pattern match+> -> (a -> r) -- B branch of the pattern match+> -> (b -> c -> r) -- C branch of the pattern match+> -> r+> )+>+> -- Constructor for A+> ( \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(r : *)+> -> \(A : r)+> -> \(B : a -> r)+> -> \(C : b -> c -> r)+> -> A+> )+>+> -- Constructor for B+> ( \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(va : a)+> -> \(r : *)+> -> \(A : r)+> -> \(B : a -> r)+> -> \(C : b -> c -> r)+> -> B va+> )+>+> -- Constructor for C+> ( \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(vb : b)+> -> \(vc : c)+> -> \(r : *)+> -> \(A : r)+> -> \(B : a -> r)+> -> \(C : b -> c -> r)+> -> C vb vc+> )+>+> -- matchT is just the identity function+> ( \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(t : forall (r : *) -> r -> (a -> r) -> (b -> c -> r) -> r)+> -> t+> )++ Within the @result@ expression, you could assemble values of type @\'T\'@+ using the constructors:++> Context:+> String : *+> Int : *+> Bool : *+> s : String+> i : Int+> b : Bool+>+> A String Int Bool : T String Int Bool+> B String Int Bool s : T String Int Bool+> C String Int Bool i b : T String Int Bool++ ... and you could pattern match on any value of type @\'T\'@ using @matchT@:++> Context:+> String : *+> Int : *+> Bool : *+> r : * -- The result type of all three case branches+> t : T String Int Bool+>+> matchT String Int Bool r t+> ( ...) -- Branch if you match `A`+> (\(s : String) -> ...) -- Branch if you match `B`+> (\(i : Int ) -> \(b : Bool) -> ...) -- Branch if you match `C`++ Now let's see how this specializes to a simpler example: Haskell's `Bool`+ type.++> -- let data Bool = True | False+> --+> -- in result+>+> ( \(Bool : *)+> -> \(True : Bool)+> -> \(False : Bool)+> -> \(if : Bool -> forall (r : *) -> r -> r -> r)+> -> result+> )+> +> -- Bool+> (forall (r : *) -> r -> r -> r)+> +> -- True+> (\(r : *) -> \(x : r) -> \(_ : r) -> x)+> +> -- False+> (\(r : *) -> \(_ : r) -> \(x : r) -> x)+> +> -- if+> (\(b : forall (r : *) -> r -> r -> r) -> b)++ Notice that @if@ is our function to pattern match on a `Bool`. The two+ branches of the @if@ correspond to the @then@ and @else@ clauses.++ Using this definition of `Bool` we can define a simple program:++> -- bool.mt+>+> -- let data Bool = True | False+> --+> -- in if True then One else Zero+>+> ( \(Bool : *)+> -> \(True : Bool)+> -> \(False : Bool)+> -> \(if : Bool -> forall (r : *) -> r -> r -> r)+> -> \(Int : *)+> -> \(Zero : Int)+> -> \(One : Int)+> -> if True Int One Zero+> )+> +> -- Bool+> (forall (r : *) -> r -> r -> r)+> +> -- True+> (\(r : *) -> \(x : r) -> \(_ : r) -> x)+> +> -- False+> (\(r : *) -> \(_ : r) -> \(x : r) -> x)+> +> -- if+> (\(b : forall (r : *) -> r -> r -> r) -> b)++ If you type-check and optimize this, you get:++> $ morte < bool.mt+> ∀(Int : *) → Int → Int → Int+> +> λ(Int : *) → λ(Zero : Int) → λ(One : Int) → One++ The compiler reduces the program to @One@. All the dead code has been+ eliminated. Also, if you study the output program closely, you'll notice+ that it's equivalent to @False@ and the program's type is equivalent to the+ @Bool@ type. Try flipping the @Zero@ and @One@ arguments to @if@ and see+ what happens.++ Now let's implement Haskell's binary tuple type, except using a named type+ and constructor since Morte does not support tuple syntax:++> -- let Pair a b = P a b+> --+> -- in result+>+> ( \(Pair : * -> * -> *)+> -> \(P : forall (a : *) -> forall (b : *) -> a -> b -> Pair a b)+> -> \(fst : forall (a : *) -> forall (b : *) -> Pair a b -> a)+> -> \(snd : forall (a : *) -> forall (b : *) -> Pair a b -> b)+> -> result+> )+> +> -- Pair+> (\(a : *) -> \(b : *) -> forall (r : *) -> (a -> b -> r) -> r)+> +> -- P+> ( \(a : *)+> -> \(b : *)+> -> \(va : a)+> -> \(vb : b)+> -> \(r : *)+> -> \(Pair : a -> b -> r)+> -> Pair va vb+> )+> +> -- fst+> ( \(a : *)+> -> \(b : *)+> -> \(p : forall (r : *) -> (a -> b -> r) -> r)+> -> p a (\(x : a) -> \(_ : b) -> x)+> )+> +> -- snd+> ( \(a : *)+> -> \(b : *)+> -> \(p : forall (r : *) -> (a -> b -> r) -> r)+> -> p b (\(_ : a) -> \(x : b) -> x)+> )++ Here we provide @fst@ and @snd@ functions instead of `matchPair`.++ Let's write a simple program that uses this @Pair@ type:++> -- pair.mt+>+> -- let Pair a b = P a b+> --+> -- in \x y -> snd (P x y)+>+> ( \(Pair : * -> * -> *)+> -> \(P : forall (a : *) -> forall (b : *) -> a -> b -> Pair a b)+> -> \(fst : forall (a : *) -> forall (b : *) -> Pair a b -> a)+> -> \(snd : forall (a : *) -> forall (b : *) -> Pair a b -> b)+> -> \(a : *) -> \(x : a) -> \(y : a) -> snd a a (P a a x y)+> )+>+> -- Pair+> (\(a : *) -> \(b : *) -> forall (r : *) -> (a -> b -> r) -> r)+>+> -- P+> ( \(a : *)+> -> \(b : *)+> -> \(va : a)+> -> \(vb : b)+> -> \(r : *)+> -> \(Pair : a -> b -> r)+> -> Pair va vb+> )+> +> -- fst+> ( \(a : *)+> -> \(b : *)+> -> \(p : forall (r : *) -> (a -> b -> r) -> r)+> -> p a (\(x : a) -> \(_ : b) -> x)+> )+> +> -- snd+> ( \(a : *)+> -> \(b : *)+> -> \(p : forall (r : *) -> (a -> b -> r) -> r)+> -> p b (\(_ : a) -> \(x : b) -> x)+> )++ If you compile and type-check that you get:++> $ morte < pair.mt+> ∀(a : *) → a → a → a+> +> λ(a : *) → λ(x : a) → λ(y : a) → y++ This is also equal to our previous program. Just rename @\'a\'@ to @Int@,+ rename @\'x\'@ to @Zero@ and rename @\'y\'@ to @One@.++ You can also import data types from whatever backend you use by accepting+ those types and functions on those types as explicit arguments to your+ program. For example, if you want to use machine integers, hardware+ arithmetic and integer literals, then you can just parametrize your program+ on the type, operations, and literal values:++> \(Int : *) -- Foreign type+> -> \((+) : Int -> Int -> Int) -- Foreign function+> -> \((*) : Int -> Int -> Int) -- Foreign function+> -> \(lit@0 : Int) -- Foreign integer literal+> -> \(lit@1 : Int) -- Foreign integer literal+> -> \(lit@2 : Int) -- Foreign integer literal+> ...++ However, the more types and operations you encode natively within Morte the+ more the optimizer can simplify your program. This is because there is no+ runtime performance penalty from using natively encoded data types. Morte+ will optimize these all away at compile time because they are just ordinary+ functions under the hood and Morte optimizes away all function calls.+-}++{- $newtypes+ Defining a newtype is no different than defining a data type with a single+ constructor with one field:++> -- let newtype Name = MkName { getName :: String }+> --+> -- in result+>+> ( \(Name : *)+> -> \(MkName : String -> Name )+> -> \(getName : Name -> String)+> -> result+> )+>+> -- Name+> String+> +> -- MkName+> (\(str : String) -> str)+>+> -- getName+> (\(str : String) -> str)++ Within the expression @result@, @Name@ is actually a new type, meaning that+ a value of type @Name@ will not type-check as a @String@ and, vice versa, a+ value of type @String@ will not type-check as a @Name@. You would have to+ explicitly convert back and forth between @Name@ and @String@ using the+ @MkName@ and @getName@ functions.++ We can prove this using the following example program:++> -- newtype.mt+>+> -- let newtype Name = MkName { getName :: String }+> --+> -- in (f :: Name -> Name) (x :: String)+> +> ( \(Name : *)+> -> \(MkName : String -> Name )+> -> \(getName : Name -> String)+> -> \(f : Name -> Name) -> \(x : String) -> f x+> )+> +> -- Name+> String+> +> -- MkName+> (\(str : String) -> str)+> +> -- getName+> (\(str : String) -> str)++ That program fails to type-check, giving the following error message:++> $ morte < newtype.mt+> Context:+> Name : *+> MkName : String → Name+> getName : Name → String+> f : Name → Name+> x : String+> +> Expression: f x+> +> Error: Function applied to argument of the wrong type+> +> Expected type: Name+> Argument type: String++ There is never a performance penalty for using newtypes, but this is just a+ special case of the fact that there is no performance penalty for using any+ natively encoded data types in Morte.+-}++{- $recursion+ Defining a recursive data type is very similar to defining a non-recursive+ type. Let's use lists as an example:++> let data List a = Cons a (List a) | Nil+>+> in result++ The equivalent Morte code is:++> -- let data List a = Cons a (List a) | Nil+> --+> -- in result+> +> ( \(List : * -> *)+> -> \(Cons : forall (a : *) -> a -> List a -> List a)+> -> \(Nil : forall (a : *) -> List a)+> -> \( foldr+> : forall (a : *) -> List a -> forall (r : *) -> (a -> r -> r) -> r -> r+> )+> -> result+> )+> +> -- List+> ( \(a : *)+> -> forall (list : *)+> -> (a -> list -> list) -- Cons+> -> list -- Nil+> -> list+> )+> +> -- Cons+> ( \(a : *)+> -> \(va : a)+> -> \(vas : forall (list : *) -> (a -> list -> list) -> list -> list)+> -> \(list : *)+> -> \(Cons : a -> list -> list)+> -> \(Nil : list)+> -> Cons va (vas list Cons Nil)+> )+> +> -- Nil+> ( \(a : *)+> -> \(list : *)+> -> \(Cons : a -> list -> list)+> -> \(Nil : list)+> -> Nil+> )+> +> -- foldr+> ( \(a : *)+> -> \(vas : forall (list : *) -> (a -> list -> list) -> list -> list)+> -> vas+> )++ Here I use the @list@ type variable where previous examples would use+ @\'r\'@ to emphasize that the continuations that a @List@ consumes both have+ the same shape as the list constructors. You just replace all recursive+ references to the data type with the type of the final result, pretending+ that the final result is a list.++ Let's extend the @List@ example with the @Bool@ code to implement Haskell's+ @all@ function and use it on an actual @List@ of @Bool@s:++> -- all.mt+>+> -- let data Bool = True | False+> --+> -- data List a = Cons a (List a) | Nil+> --+> -- in let (&&) :: Bool -> Bool -> Bool+> -- (&&) b1 b2 = if b1 then b2 else False+> --+> -- bools :: List Bool+> -- bools = Cons True (Cons True (Cons True Nil))+> --+> -- in foldr bools (&&) True+> +> ( \(Bool : *)+> -> \(True : Bool)+> -> \(False : Bool)+> -> \(if : Bool -> forall (r : *) -> r -> r -> r)+> -> \(List : * -> *)+> -> \(Cons : forall (a : *) -> a -> List a -> List a)+> -> \(Nil : forall (a : *) -> List a)+> -> \( foldr+> : forall (a : *) -> List a -> forall (r : *) -> (a -> r -> r) -> r -> r+> )+> -> ( \((&&) : Bool -> Bool -> Bool)+> -> \(bools : List Bool)+> -> foldr Bool bools Bool (&&) True+> )+> +> -- (&&)+> (\(b@1 : Bool) -> \(b@2 : Bool) -> if b@1 Bool b@2 False)+> +> -- bools+> (Cons Bool True (Cons Bool True (Cons Bool True (Nil Bool))))+> )+> +> -- Bool+> (forall (r : *) -> r -> r -> r)+> +> -- True+> (\(r : *) -> \(x : r) -> \(_ : r) -> x)+> +> -- False+> (\(r : *) -> \(_ : r) -> \(x : r) -> x)+> +> -- if+> (\(b : forall (r : *) -> r -> r -> r) -> b)+> +> -- List+> ( \(a : *)+> -> forall (list : *)+> -> (a -> list -> list) -- Cons+> -> list -- Nil+> -> list+> )+> +> -- Cons+> ( \(a : *)+> -> \(va : a)+> -> \(vas : forall (list : *) -> (a -> list -> list) -> list -> list)+> -> \(list : *)+> -> \(Cons : a -> list -> list)+> -> \(Nil : list)+> -> Cons va (vas list Cons Nil)+> )+> +> -- Nil+> ( \(a : *)+> -> \(list : *)+> -> \(Cons : a -> list -> list)+> -> \(Nil : list)+> -> Nil+> )+> +> -- foldr+> ( \(a : *)+> -> \(vas : forall (list : *) -> (a -> list -> list) -> list -> list)+> -> vas+> )++ If you type-check and optimize the program, the compiler will statically+ evaluate the entire computation, reducing the program to @True@:++> $ morte < all.mt+> ∀(r : *) → r → r → r+> +> λ(r : *) → λ(x : r) → λ(_ : r) → x++ Here's another example of encoding a recursive type, using natural numbers:++> -- let data Nat = Succ Nat | Zero+> --+> -- in result+> +> ( \(Nat : *)+> -> \(Succ : Nat -> Nat)+> -> \(Zero : Nat)+> -> \(foldNat : Nat -> forall (r : *) -> (r -> r) -> r -> r)+> -> result+> )+> +> -- Nat+> ( forall (nat : *)+> -> (nat -> nat) -- Succ+> -> nat -- Zero+> -> nat+> )+> +> ( \(n : forall (nat : *) -> (nat -> nat) -> nat -> nat)+> -> \(nat : *)+> -> \(Succ : nat -> nat)+> -> \(Zero : nat)+> -> Succ (n nat Succ Zero)+> )+> +> ( \(nat : *)+> -> \(Succ : nat -> nat)+> -> \(Zero : nat)+> -> Zero+> )+> +> ( \(n : forall (nat : *) -> (nat -> nat) -> nat -> nat)+> -> n+> )++ As an exercise, try implementing @(+)@ for the @Nat@ type, then implementing+ Haskell's @sum@, then using @sum@ on a @List@ of @Nat@s. Verify that the+ compiler statically computes the sum as a Church-encoded numeral.+ + The encoding outlined in this section is equivalent to an F-algebra encoding+ of a recursive type, which is any encoding of the following shape:++> forall (x : *) -> (F x -> x) -> x++ .. where @F@ is a strictly-positive functor.++ Our @List a@ encoding is isomorphic to an F-algebra encoding where:++> F x = Maybe (a, x)++ ... and our @Nat@ encoding is isomorphic to an F-algebra encoding where:++> F x = Maybe x++-}++{- $existential+ You can translate existential quantified types to use universal+ quantification. For example, consider the following existentially+ quantified Haskell type:++> let data Example = forall s . MkExample s (s -> String)+>+> in result++ The equivalent Morte program is:++> -- let data Example = forall s . Example s (s -> String)+> --+> -- in result+> +> \(String : *) ->+> ( \(Example : *)+> -> \(MkExample : forall (s : *) -> s -> (s -> String) -> Example)+> -> \( matchExample+> : Example+> -> forall (x : *)+> -> (forall (s : *) -> s -> (s -> String) -> x)+> -> x+> )+> -> result+> )+> +> -- Example+> ( forall (x : *)+> -> (forall (s : *) -> s -> (s -> String) -> x) -- MkExample+> -> x+> )+> +> -- MkExample+> ( \(s : *)+> -> \(vs : s)+> -> \(fs : s -> String)+> -> \(x : *)+> -> \(MkExample : forall (s : *) -> s -> (s -> String) -> x)+> -> MkExample s vs fs+> )+> +> -- matchExample+> ( \(e : forall (x : *) -> (forall (s : *) -> s -> (s -> String) -> x) -> x)+> -> e+> )++ More generally, for every constructor that you existentially quantify with a+ type variable @\'s\'@ you just add a @(forall (s : *) -> ...)@ prefix to+ that constructor's continuation. If you \"pattern match\" against the+ constructor corresponding to that continuation you will bind the+ existentially quantified type.++ For example, we can pattern match against the @MkExample@ constructor like+ this:++> \(e : Example) -> matchExample e+> (\(s : *) -> (x : s) -> (f : s -> String) -> expr) ++ The type @\'s\'@ will be in scope for @expr@ and we can safely apply the+ bound function to the bound value if we so chose to extract a @String@,+ despite not knowing which type @\'s\'@ we bound:++> \(e : Example) -> matchExample e+> (\(s : *) -> (x : s) -> (f : s -> String) -> f x) ++ The two universal quantifiers in the definition of the @Example@ type+ statically forbid the type @\'s\'@ from leaking from the pattern match.+-}++{- $corecursion+ Recursive types can only encode finite data types. If you want a+ potentially infinite data type (such as an infinite list), you must encode+ the type in a different way.++ For example, consider the following infinite stream type:++> codata Stream a = Cons a (Stream a)++ If you tried to encode that as a recursive type, you would end up with this+ Morte type:++> \(a : *) -> forall (x : *) -> (a -> x -> x) -> x++ However, this type is uninhabited, meaning that you cannot create a value of+ the above type for any choice of @\'a\'@. Try it, if you don't believe+ me.++ Potentially infinite types must be encoded using a dual trick, where we+ store them as an existentially quantified seed and a generating step+ function that emits one layer alongside a new seed.++ For example, the above @Stream@ type would translate to the following+ non-recursive representation. The @StreamF@ constructor represents one+ layer and the @Stream@ type lets us generate an infinite number of layers+ by providing an initial seed of type @s@ and a generation function of type+ @(s -> StreamF a s)@:++> -- Replace the corecursive occurrence of `Stream` with `s`+> data StreamF a s = Cons a s+>+> data Stream a = forall s . MkStream s (s -> StreamF a s)++ The above type will work for any type @\'s\'@ as the @\'s\'@ is+ existentially quantified. The end user of the @Stream@ will never be able+ to detect what the original type of @s@ was, because the @MkStream@+ constructor closes over that information permanently.++ An example @Stream@ is the following lazy stream of natural numbers:++> nats :: Stream Int+> nats = MkStream 0 (\n -> Cons n (n + 1))++ Internally, the above @Stream@ uses an @Int@ as its internal state, but+ that is completely invisible to all downstream code, which cannot access+ the concrete type of the internal state any longer.++ In fact, this trick of using a seed and a generating step function is a+ special case of a F-coalgebra encoding of a corecursive type, which is+ anything of the form:++> exists s . (s, s -> F s)++ ... where @F@ is a strictly-positive functor.++ Once you F-coalgebra encode the @Stream@ type you can translate the type to+ Morte using the rules for existential quantification given in the previous+ section:++> (forall (x : *) -> (forall (s : *) -> s -> (s -> StreamF a s) -> x) -> x++ See the next section for some example @Stream@ code.+-}++{- $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+ order to super-optimize your program. For example, consider the following+ program which maps the identity function over a list:++> -- mapid1.mt+>+> ( \(List : * -> *)+> -> \(map : forall (a : *) -> forall (b : *) -> (a -> b) -> List a -> List b)+> -> \(id : forall (a : *) -> a -> a)+> -> \(a : *) -> map a a (id a)+> )+> +> -- List+> (\(a : *) -> forall (x : *) -> (a -> x -> x) -> x -> x)+> +> -- map+> ( \(a : *)+> -> \(b : *)+> -> \(f : a -> b)+> -> \(l : forall (x : *) -> (a -> x -> x) -> x -> x)+> -> \(x : *)+> -> \(Cons : b -> x -> x)+> -> \(Nil: x)+> -> l x (\(va : a) -> \(vx : x) -> Cons (f va) vx) Nil+> )+> +> -- id+> (\(a : *) -> \(va : a) -> va)++ If we examine the compiler output, we'll see that the compiler fuses away+ the @map@, leaving behind the identity function on lists:++> $ morte < mapid1.mt+> ∀(a : *) → (∀(x : *) → (a → x → x) → x → x) → ∀(x : *) → (a → x → x) → x → x+> +> λ(a : *) → λ(l : ∀(x : *) → (a → x → x) → x → x) → l++ We can prove this by replacing our @map@ with the identity function on+ lists:++> -- mapid2.mt+>+> ( \(List : * -> *)+> -> \(map : forall (a : *) -> forall (b : *) -> (a -> b) -> List a -> List b)+> -> \(id : forall (a : *) -> a -> a)+> -> \(a : *) -> id (List a)+> )+> +> -- List+> (\(a : *) -> forall (x : *) -> (a -> x -> x) -> x -> x)+> +> -- map+> ( \(a : *)+> -> \(b : *)+> -> \(f : a -> b)+> -> \(l : forall (x : *) -> (a -> x -> x) -> x -> x)+> -> \(x : *)+> -> \(Cons : b -> x -> x)+> -> \(Nil: x)+> -> l x (\(va : a) -> \(vx : x) -> Cons (f va) vx) Nil+> )+> +> -- id+> (\(a : *) -> \(va : a) -> va)++ The compiler output for this is alpha-equivalent:++> $ morte < mapid2.mt+> ∀(a : *) → (∀(x : *) → (a → x → x) → x → x) → ∀(x : *) → (a → x → x) → x → x+> +> λ(a : *) → λ(va : ∀(x : *) → (a → x → x) → x → x) → va++ However, we don't have to trust our fallible eyes. We can enlist the+ @morte@ library to mechanically check that the two programs are equal:++> $ ghci+> Prelude> import qualified Data.Text.Lazy.IO as Text+> Prelude Text> txt1 <- Text.readFile "mapid1.mt"+> Prelude Text> txt2 <- Text.readFile "mapid2.mt"+> Prelude Text> import Morte.Parser+> Prelude Text Morte.Parser> let e1 = exprFromText txt1+> Prelude Text Morte.Parser> let e2 = exprFromText txt2+> Prelude Text Morte.Parser> import Control.Applicative+> Prelude Text Morte.Parser Control.Applicative> liftA2 (==) e1 e2+> Right True++ We just mechanically proved that @map id == id@. When we transform our code+ to a non-recursive form we've done most of the work. The compiler can then+ check that the two programs are equal by just optimizing both programs and+ verifying that they produce identical optimized code.++ Using this same trick we can also prove the other map fusion law:++> map (f . g) = map f . map g++ Here is the first program, corresponding to the left-hand side of the+ equation:++> -- mapcomp1.mt+>+> -- map (f . g)+> +> ( \(List : * -> *)+> -> \(map : forall (a : *) -> forall (b : *) -> (a -> b) -> List a -> List b)+> -> \( (.)+> : forall (a : *)+> -> forall (b : *)+> -> forall (c : *)+> -> (b -> c)+> -> (a -> b)+> -> (a -> c)+> )+> -> \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(f : b -> c)+> -> \(g : a -> b)+> -> map a c ((.) a b c f g)+> )+> +> -- List+> (\(a : *) -> forall (x : *) -> (a -> x -> x) -> x -> x)+> +> -- map+> ( \(a : *)+> -> \(b : *)+> -> \(f : a -> b)+> -> \(l : forall (x : *) -> (a -> x -> x) -> x -> x)+> -> \(x : *)+> -> \(Cons : b -> x -> x)+> -> \(Nil: x)+> -> l x (\(va : a) -> \(vx : x) -> Cons (f va) vx) Nil+> )+> +> -- (.)+> ( \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(f : b -> c)+> -> \(g : a -> b)+> -> \(va : a)+> -> f (g va)+> )++ ... and here is the second program, corresponding to the right-hand side:++> -- mapcomp2.mt+> +> ( \(List : * -> *)+> -> \(map : forall (a : *) -> forall (b : *) -> (a -> b) -> List a -> List b)+> -> \( (.)+> : forall (a : *)+> -> forall (b : *)+> -> forall (c : *)+> -> (b -> c)+> -> (a -> b)+> -> (a -> c)+> )+> -> \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(f : b -> c)+> -> \(g : a -> b)+> -> (.) (List a) (List b) (List c) (map b c f) (map a b g)+> )+> +> -- List+> (\(a : *) -> forall (x : *) -> (a -> x -> x) -> x -> x)+> +> -- map+> ( \(a : *)+> -> \(b : *)+> -> \(f : a -> b)+> -> \(l : forall (x : *) -> (a -> x -> x) -> x -> x)+> -> \(x : *)+> -> \(Cons : b -> x -> x)+> -> \(Nil: x)+> -> l x (\(va : a) -> \(vx : x) -> Cons (f va) vx) Nil+> )+> +> -- (.)+> ( \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(f : b -> c)+> -> \(g : a -> b)+> -> \(va : a)+> -> f (g va)+> )++ Verify using the @morte@ library that those produce identical expressions.+ For reference, they both generate the following optimized program that loops+ over the list just once, applying @\'f\'@ and @\'g\'@ to every value:++> $ morte < mapcomp1.mt+> ∀(a : *) → ∀(b : *) → ∀(c : *) → (b → c) → (a → b) → (∀(x : *) → (a → x → x) →+> x → x) → ∀(x : *) → (c → x → x) → x → x+> +> λ(a : *) → λ(b : *) → λ(c : *) → λ(f : b → c) → λ(g : a → b) → λ(l : ∀(x : *) +> → (a → x → x) → x → x) → λ(x : *) → λ(Cons : c → x → x) → l x (λ(va : a) → Con+> s (f (g va)))++ We can also prove @map@ fusion for corecursive streams as well. Just use+ the following program:++> -- first :: (a -> b) -> (a, c) -> (b, c)+> -- first f (va, vb) = (f va, vb) +> -- +> -- data Stream a = Cons (a, Stream a)+> -- +> -- map :: (a -> b) -> Stream a -> Stream b+> -- map f (Cons (va, s)) = Cons (first f (va, map f s))+> -- +> -- -- example1 = example2+> -- +> -- example1 :: Stream a -> Stream a+> -- example1 = map id+> -- +> -- example2 :: Stream a -> Stream a+> -- example2 = id+> -- +> -- -- example3 = example4+> -- +> -- example3 :: (b -> c) -> (a -> b) -> Stream a -> Stream c+> -- example3 f g = map (f . g)+> -- +> -- example4 :: (b -> c) -> (a -> b) -> Stream a -> Stream c+> -- example4 f g = map f . map g+> +> ( \(id : forall (a : *) -> a -> a)+> -> \( (.)+> : forall (a : *)+> -> forall (b : *)+> -> forall (c : *)+> -> (b -> c)+> -> (a -> b)+> -> (a -> c)+> )+> -> \(Pair : * -> * -> *)+> -> \(P : forall (a : *) -> forall (b : *) -> a -> b -> Pair a b)+> -> \( first+> : forall (a : *)+> -> forall (b : *)+> -> forall (c : *)+> -> (a -> b)+> -> Pair a c+> -> Pair b c+> )+> +> -> ( \(Stream : * -> *)+> -> \( map+> : forall (a : *)+> -> forall (b : *)+> -> (a -> b)+> -> Stream a+> -> Stream b+> )+> +> -- example@1 = example@2+> -> ( \(example@1 : forall (a : *) -> Stream a -> Stream a)+> -> \(example@2 : forall (a : *) -> Stream a -> Stream a)+> +> -- example@3 = example@4+> -> \( example@3+> : forall (a : *)+> -> forall (b : *)+> -> forall (c : *)+> -> (b -> c)+> -> (a -> b)+> -> Stream a+> -> Stream c+> )+> +> -> \( example@4+> : forall (a : *)+> -> forall (b : *)+> -> forall (c : *)+> -> (b -> c)+> -> (a -> b)+> -> Stream a+> -> Stream c+> )+> +> -- Uncomment the example you want to test+> -> example@1+> -- -> example@2+> -- -> example@3+> -- -> example@4+> )+> +> -- example@1+> (\(a : *) -> map a a (id a))+> +> -- example@2+> (\(a : *) -> id (Stream a))+> +> -- example@3+> ( \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(f : b -> c)+> -> \(g : a -> b)+> -> map a c ((.) a b c f g)+> )+> +> -- example@4+> ( \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(f : b -> c)+> -> \(g : a -> b)+> -> (.) (Stream a) (Stream b) (Stream c) (map b c f) (map a b g)+> )+> )+> +> -- Stream+> ( \(a : *)+> -> forall (x : *)+> -> (forall (s : *) -> s -> (s -> Pair a s) -> x)+> -> x+> )+> +> -- map+> ( \(a : *)+> -> \(b : *)+> -> \(f : a -> b)+> -> \( st+> : forall (x : *) -> (forall (s : *) -> s -> (s -> Pair a s) -> x) -> x+> )+> -> \(x : *)+> -> \(S : forall (s : *) -> s -> (s -> Pair b s) -> x)+> -> st+> x+> ( \(s : *)+> -> \(seed : s)+> -> \(step : s -> Pair a s)+> -> S+> s+> seed+> (\(seed@1 : s) -> first a b s f (step seed@1))+> )+> )+> )+> +> -- id+> (\(a : *) -> \(va : a) -> va)+> +> -- (.)+> ( \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(f : b -> c)+> -> \(g : a -> b)+> -> \(va : a)+> -> f (g va)+> )+> +> -- Pair+> (\(a : *) -> \(b : *) -> forall (x : *) -> (a -> b -> x) -> x)+> +> -- P+> ( \(a : *)+> -> \(b : *)+> -> \(va : a)+> -> \(vb : b)+> -> \(x : *)+> -> \(P : a -> b -> x)+> -> P va vb+> )+> +> -- first+> ( \(a : *)+> -> \(b : *)+> -> \(c : *)+> -> \(f : a -> b)+> -> \(p : forall (x : *) -> (a -> c -> x) -> x)+> -> \(x : *)+> -> \(Pair : b -> c -> x)+> -> p x (\(va : a) -> \(vc : c) -> Pair (f va) vc)+> )+> ++Both @example\@1@ and @example\@2@ generate identical optimized expressions,+corresponding to the identity function on @Stream@:++> $ morte < corecursive.mt+> ∀(a : *) → (∀(x : *) → (∀(s : *) → s → (s → ∀(x : *) → (a → s → x) → x) → x) →+> x) → ∀(x : *) → (∀(s : *) → s → (s → ∀(x : *) → (a → s → x) → x) → x) → x+> +> λ(a : *) → λ(st : ∀(x : *) → (∀(s : *) → s → (s → ∀(x : *) → (a → s → x) → x) +> → x) → x) → st++Similarly, both @example\@3@ and @example\@4@ generate identical optimized+expressions, corresponding to applying @f@ and @g@ to every value emitted by+the generating step function:++> $ morte < corecursive.mt+> ∀(a : *) → ∀(b : *) → ∀(c : *) → (b → c) → (a → b) → (∀(x : *) → (∀(s : *) → s+> → (s → ∀(x : *) → (a → s → x) → x) → x) → x) → ∀(x : *) → (∀(s : *) → s → (s +> → ∀(x : *) → (c → s → x) → x) → x) → x+> +> λ(a : *) → λ(b : *) → λ(c : *) → λ(f : b → c) → λ(g : a → b) → λ(st : ∀(x : *)+> → (∀(s : *) → s → (s → ∀(x : *) → (a → s → x) → x) → x) → x) → λ(x : *) → λ(S+> : ∀(s : *) → s → (s → ∀(x : *) → (c → s → x) → x) → x) → st x (λ(s : *) → λ(s+> eed : s) → λ(step : s → ∀(x : *) → (a → s → x) → x) → S s seed (λ(seed@1 : s) +> → λ(x : *) → λ(Pair : c → s → x) → step seed@1 x (λ(va : a) → Pair (f (g va)))+> ))++-}++{- $normalization+ Morte has a very simple optimization scheme. The only thing that Morte does+ to optimize programs is beta-reduce them and eta-reduce them to their+ normal form. Since Morte's core calculus is non-recursive, this reduction+ is guaranteed to terminate.++ The way Morte compares expressions for equality is just to compare their+ normal forms. Note that this definition of equality does not detect all+ equal programs. Here's an example of an equality that Morte does not+ currently detect (but might detect in the future):++> k : forall (x : *) -> (a -> x) -> x+>+> k (f . g) = f (k g)++ This is an example of a free theorem: an equality that can be deduced purely+ from the type of @k@. Morte may eventually use free theorems to further+ normalize expression, but for now it does not.++ 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+ 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+ unrolled loop.++ Normalization confers one very useful property: the runtime performance of a+ Morte program is completely impervious to abstraction. Adding additional+ abstraction layers may increase compile time, but runtime performance will+ remain constant. The runtime performance of a program is solely a function+ of the program's normal form, and adding additional abstraction layers never+ changes the normal form your program.+-}++{- $effects+ Morte uses the Haskell approach to effects, where effects are represented as+ terms within the language and evaluation order has no impact on order of+ effects. This is by necessity: if evaluation triggered side effects then+ Morte would be unable to optimize expressions by normalizing them.++ The following example encodes @IO@ within Morte as an abstract syntax tree+ of effects (a.k.a. a "free monad"). Encoding @IO@ as a free monad is not+ strictly necessary, but doing so makes Morte aware of the monad laws, which+ allows it to greatly simplify the program:++> -- recursive.mt+>+> -- The Haskell code we will translate to Morte:+> --+> -- import Prelude hiding (+> -- (+), (*), IO, putStrLn, getLine, (>>=), (>>), return )+> -- +> -- -- Simple prelude+> --+> -- data Nat = Succ Nat | Zero+> --+> -- zero :: Nat+> -- zero = Zero+> --+> -- one :: Nat+> -- one = Succ Zero+> --+> -- (+) :: Nat -> Nat -> Nat+> -- Zero + n = n+> -- Succ m + n = m + Succ n+> --+> -- (*) :: Nat -> Nat -> Nat+> -- Zero * n = Zero+> -- Succ m * n = n + (m * n)+> --+> -- foldNat :: Nat -> (a -> a) -> a -> a+> -- foldNat Zero f x = x+> -- foldNat (Succ m) f x = f (foldNat m f x)+> --+> -- data IO r = PutStrLn String (IO r) | GetLine (String -> IO r) | Return r+> --+> -- putStrLn :: String -> IO U+> -- putStrLn str = PutStrLn str (Return Unit)+> --+> -- getLine :: IO String+> -- getLine = GetLine Return+> --+> -- return :: a -> IO a+> -- return = Return+> --+> -- (>>=) :: IO a -> (a -> IO b) -> IO b+> -- PutStrLn str io >>= f = PutStrLn str (io >>= f)+> -- GetLine k >>= f = GetLine (\str -> k str >>= f)+> -- Return r >>= f = f r+> --+> -- -- Derived functions+> --+> -- (>>) :: IO U -> IO U -> IO U+> -- m >> n = m >>= \_ -> n+> --+> -- two :: Nat+> -- two = one + one+> --+> -- three :: Nat+> -- three = one + one + one+> --+> -- four :: Nat+> -- four = one + one + one + one+> --+> -- five :: Nat+> -- five = one + one + one + one + one+> --+> -- six :: Nat+> -- six = one + one + one + one + one + one+> --+> -- seven :: Nat+> -- seven = one + one + one + one + one + one + one+> --+> -- eight :: Nat+> -- eight = one + one + one + one + one + one + one + one+> --+> -- nine :: Nat+> -- nine = one + one + one + one + one + one + one + one + one+> --+> -- ten :: Nat+> -- ten = one + one + one + one + one + one + one + one + one + one+> --+> -- replicateM_ :: Nat -> IO U -> IO U+> -- replicateM_ n io = foldNat n (io >>) (return Unit)+> --+> -- ninetynine :: Nat+> -- ninetynine = nine * ten + nine+> --+> -- main_ :: IO U+> -- main_ = getLine >>= putStrLn+> +> -- "Free" variables+> ( \(String : * )+> -> \(U : *)+> -> \(Unit : U)+> +> -- Simple prelude+> -> ( \(Nat : *)+> -> \(zero : Nat)+> -> \(one : Nat)+> -> \((+) : Nat -> Nat -> Nat)+> -> \((*) : Nat -> Nat -> Nat)+> -> \(foldNat : Nat -> forall (a : *) -> (a -> a) -> a -> a)+> -> \(IO : * -> *)+> -> \(return : forall (a : *) -> a -> IO a)+> -> \((>>=)+> : forall (a : *)+> -> forall (b : *)+> -> IO a+> -> (a -> IO b)+> -> IO b+> )+> -> \(putStrLn : String -> IO U)+> -> \(getLine : IO String)+> +> -- Derived functions+> -> ( \((>>) : IO U -> IO U -> IO U)+> -> \(two : Nat)+> -> \(three : Nat)+> -> \(four : Nat)+> -> \(five : Nat)+> -> \(six : Nat)+> -> \(seven : Nat)+> -> \(eight : Nat)+> -> \(nine : Nat)+> -> \(ten : Nat)+> -> ( \(replicateM_ : Nat -> IO U -> IO U)+> -> \(ninetynine : Nat)+> -> replicateM_ ninetynine ((>>=) String U getLine putStrLn)+> )+> +> -- replicateM_+> ( \(n : Nat)+> -> \(io : IO U)+> -> foldNat n (IO U) ((>>) io) (return U Unit)+> )+> +> -- ninetynine+> ((+) ((*) nine ten) nine)+> )+> +> -- (>>)+> ( \(m : IO U)+> -> \(n : IO U)+> -> (>>=) U U m (\(_ : U) -> n)+> )+> +> -- two+> ((+) one one)+> +> -- three+> ((+) one ((+) one one))+> +> -- four+> ((+) one ((+) one ((+) one one)))+> +> -- five+> ((+) one ((+) one ((+) one ((+) one one))))+> +> -- six+> ((+) one ((+) one ((+) one ((+) one ((+) one one)))))+> +> -- seven+> ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one one))))))+> +> -- eight+> ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one one)))))))+> -- nine+> ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one one))))))))+> +> -- ten+> ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one ((+) one one)))))))))+> )+> +> -- Nat+> ( forall (a : *)+> -> (a -> a)+> -> a+> -> a+> )+> +> -- zero+> ( \(a : *)+> -> \(Succ : a -> a)+> -> \(Zero : a)+> -> Zero+> )+> +> -- one+> ( \(a : *)+> -> \(Succ : a -> a)+> -> \(Zero : a)+> -> Succ Zero+> )+> +> -- (+)+> ( \(m : forall (a : *) -> (a -> a) -> a -> a)+> -> \(n : forall (a : *) -> (a -> a) -> a -> a)+> -> \(a : *)+> -> \(Succ : a -> a)+> -> \(Zero : a)+> -> m a Succ (n a Succ Zero)+> )+> +> -- (*)+> ( \(m : forall (a : *) -> (a -> a) -> a -> a)+> -> \(n : forall (a : *) -> (a -> a) -> a -> a)+> -> \(a : *)+> -> \(Succ : a -> a)+> -> \(Zero : a)+> -> m a (n a Succ) Zero+> )+> +> -- foldNat+> ( \(n : forall (a : *) -> (a -> a) -> a -> a)+> -> n+> )+> +> -- IO+> ( \(r : *)+> -> forall (x : *)+> -> (String -> x -> x)+> -> ((String -> x) -> x)+> -> (r -> x)+> -> x+> )+> +> -- return+> ( \(a : *)+> -> \(va : a)+> -> \(x : *)+> -> \(PutStrLn : String -> x -> x)+> -> \(GetLine : (String -> x) -> x)+> -> \(Return : a -> x)+> -> Return va+> )+> +> -- (>>=)+> ( \(a : *)+> -> \(b : *)+> -> \(m : forall (x : *)+> -> (String -> x -> x)+> -> ((String -> x) -> x)+> -> (a -> x)+> -> x+> )+> -> \(f : a+> -> forall (x : *)+> -> (String -> x -> x)+> -> ((String -> x) -> x)+> -> (b -> x)+> -> x+> )+> -> \(x : *)+> -> \(PutStrLn : String -> x -> x)+> -> \(GetLine : (String -> x) -> x)+> -> \(Return : b -> x)+> -> m x PutStrLn GetLine (\(va : a) -> f va x PutStrLn GetLine Return)+> )+> +> -- putStrLn+> ( \(str : String)+> -> \(x : *)+> -> \(PutStrLn : String -> x -> x )+> -> \(GetLine : (String -> x) -> x)+> -> \(Return : U -> x)+> -> PutStrLn str (Return Unit)+> )+> +> -- getLine+> ( \(x : *)+> -> \(PutStrLn : String -> x -> x )+> -> \(GetLine : (String -> x) -> x)+> -> \(Return : String -> x)+> -> GetLine Return+> )+> )++If you type-check and normalize this program, the compiler will produce an+unrolled syntax tree representing a program that echoes 99 lines from standard+input to standard output:++> $ morte < recursive.mt+> ∀(String : *) → ∀(U : *) → U → ∀(x : *) → (String → x → x) → ((String → x+> ) → x) → (U → x) → x+> +> λ(String : *) → λ(U : *) → λ(Unit : U) → λ(x : *) → λ(PutStrLn : String →+> x → x) → λ(GetLine : (String → x) → x) → λ(Return : U → x) → GetLine (λ(+> va : String) → PutStrLn va (GetLine (λ(va@1 : String) → PutStrLn va@1 (Ge+> tLine (λ(va@2 : String) → PutStrLn va@2 (GetLine (λ(va@3 : String) → PutS+> trLn va@3 (...+> <snip>+> ... GetLine (λ(va@92 : String) → PutStrLn va@92 (GetLine (λ(va@93 : Strin+> g) → PutStrLn va@93 (GetLine (λ(va@94 : String) → PutStrLn va@94 (GetLine+> (λ(va@95 : String) → PutStrLn va@95 (GetLine (λ(va@96 : String) → PutStr+> Ln va@96 (GetLine (λ(va@97 : String) → PutStrLn va@97 (GetLine (λ(va@98 :+> String) → PutStrLn va@98 (Return Unit)))))))))))))))))))))))))))))))))))+> )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))+> )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))+> )))))))))))))))))++ This program can then be passed to a backend language which interprets the+ syntax tree, translating @GetLine@ and @PutStrLn@ to read and write+ commands.++ Notice that although our program is built using the high-level @replicateM_@+ function, you'd never be able to tell by looking at the optimized program.+ By encoding effects as a free monad, we expose the monad laws to Morte,+ which allows the normalizer to optimize away monadic abstractions like+ @replicateM_@.++ You can also build corecursive programs with effects. Here is an example of+ a corecursive @IO@ syntax tree and a program that infinitely echoes+ standard input to standard output:++> -- corecursive.mt+>+> -- data IOF r s = PutStrLn String s | GetLine (String -> s) | Return r+> --+> -- data IO r = forall s . MkIO s (s -> IOF r s)+> --+> -- main = MkIO Nothing (maybe (\str -> PutStrLn str Nothing) (GetLine Just))+> +> ( \(String : *)+> -> ( \(Maybe : * -> *)+> -> \(Just : forall (a : *) -> a -> Maybe a)+> -> \(Nothing : forall (a : *) -> Maybe a)+> -> \( maybe+> : forall (a : *) -> Maybe a -> forall (x : *) -> (a -> x) -> x -> x+> )+> -> \(IOF : * -> * -> *)+> -> \( PutStrLn+> : forall (r : *)+> -> forall (s : *)+> -> String+> -> s+> -> IOF r s+> )+> -> \( GetLine+> : forall (r : *)+> -> forall (s : *)+> -> (String -> s)+> -> IOF r s+> )+> -> \( Return+> : forall (r : *)+> -> forall (s : *)+> -> r+> -> IOF r s+> )+> -> ( \(IO : * -> *)+> -> \( MkIO+> : forall (r : *) -> forall (s : *) -> s -> (s -> IOF r s) -> IO r+> )+> -> ( \(main : forall (r : *) -> IO r)+> -> main+> )+> +> -- main+> ( \(r : *)+> -> MkIO+> r+> (Maybe String)+> (Nothing String)+> ( \(m : Maybe String)+> -> maybe+> String+> m+> (IOF r (Maybe String))+> (\(str : String) ->+> PutStrLn r (Maybe String) str (Nothing String)+> )+> (GetLine r (Maybe String) (Just String))+> )+> )+> )+> +> -- IO+> ( \(r : *)+> -> forall (x : *)+> -> (forall (s : *) -> s -> (s -> IOF r s) -> x)+> -> x+> )+> +> -- MkIO+> ( \(r : *)+> -> \(s : *)+> -> \(seed : s)+> -> \(step : s -> IOF r s)+> -> \(x : *)+> -> \(k : forall (s : *) -> s -> (s -> IOF r s) -> x)+> -> k s seed step+> )+> )+> +> -- Maybe+> (\(a : *) -> forall (x : *) -> (a -> x) -> x -> x)+> +> -- Just+> ( \(a : *)+> -> \(va : a)+> -> \(x : *)+> -> \(Just : a -> x)+> -> \(Nothing : x)+> -> Just va+> )+> +> -- Nothing+> ( \(a : *)+> -> \(x : *)+> -> \(Just : a -> x)+> -> \(Nothing : x)+> -> Nothing+> )+> +> -- maybe+> (\(a : *) -> \(m : forall (x : *) -> (a -> x) -> x -> x) -> m)+> +> -- IOF+> ( \(r : *)+> -> \(s : *)+> -> forall (x : *)+> -> (String -> s -> x)+> -> ((String -> s) -> x)+> -> (r -> x)+> -> x+> )+> +> -- PutStrLn+> ( \(r : *)+> -> \(s : *)+> -> \(str : String)+> -> \(vs : s)+> -> \(x : *)+> -> \(PutStrLn : String -> s -> x)+> -> \(GetLine : (String -> s) -> x)+> -> \(Return : r -> x)+> -> PutStrLn str vs+> )+> +> -- GetLine+> ( \(r : *)+> -> \(s : *)+> -> \(k : String -> s)+> -> \(x : *)+> -> \(PutStrLn : String -> s -> x)+> -> \(GetLine : (String -> s) -> x)+> -> \(Return : r -> x)+> -> GetLine k+> )+> +> -- Return+> ( \(r : *)+> -> \(s : *)+> -> \(vr : r)+> -> \(x : *)+> -> \(PutStrLn : String -> s -> x)+> -> \(GetLine : (String -> s) -> x)+> -> \(Return : r -> x)+> -> Return vr+> )+> +> )++ If you compile this corecursive program you will get a state machine which+ can then be passed to a backend to step the state machine indefinitely:++> $ morte < corecursive.mt+> ∀(String : *) → ∀(r : *) → ∀(x : *) → (∀(s : *) → s → (s → ∀(x : *) → (String +> → s → x) → ((String → s) → x) → (r → x) → x) → x) → x+> +> λ(String : *) → λ(r : *) → λ(x : *) → λ(k : ∀(s : *) → s → (s → ∀(x : *) → (St+> ring → s → x) → ((String → s) → x) → (r → x) → x) → x) → k (∀(x : *) → (String+> → x) → x → x) (λ(x : *) → λ(Just : String → x) → λ(Nothing : x) → Nothing) (λ+> (m : ∀(x : *) → (String → x) → x → x) → m (∀(x : *) → (String → (∀(x : *) → (S+> tring → x) → x → x) → x) → ((String → ∀(x : *) → (String → x) → x → x) → x) → +> (r → x) → x) (λ(str : String) → λ(x : *) → λ(PutStrLn : String → (∀(x : *) → (+> String → x) → x → x) → x) → λ(GetLine : (String → ∀(x : *) → (String → x) → x +> → x) → x) → λ(Return : r → x) → PutStrLn str (λ(x : *) → λ(Just : String → x) +> → λ(Nothing : x) → Nothing)) (λ(x : *) → λ(PutStrLn : String → (∀(x : *) → (St+> ring → x) → x → x) → x) → λ(GetLine : (String → ∀(x : *) → (String → x) → x → +> x) → x) → λ(Return : r → x) → GetLine (λ(va : String) → λ(x : *) → λ(Just : St+> ring → x) → λ(Nothing : x) → Just va)))++ Any manipulations of this corecursive syntax tree within Morte will compile+ to efficient state transitions.+-}++{- $portability+ You can use Morte as a standard format for transmitting code between+ functional languages. This requires you to encode the source language to+ Morte and decode the Morte into the destination language.++ 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.++ Additionally, Morte provides a standard `Data.Binary.Binary` interface that+ you can use for serializing and deserializing code. You may find this+ useful for transmitting code between distributed services, even within+ the same language.+-}++{- $conclusion+ The primary purpose of Morte is a proof-of-concept that a non-recursive+ calculus of constructions is the ideal system for the super-optimization of+ functional programs. Morte uses a simple, yet powerful, optimization+ scheme that consists entirely of normalizing terms using the ordinary+ reduction rules of lambda calculus. Morte emphasizes pushing optimization+ complexity out of the virtual machine and into the translation of+ abstractions to the calculus of constructions. However, that means that the+ hard work has only just begun and Morte still needs front-end compilers to+ translate from high-level functional languages to the calculus of+ constructions.++ The secondary purpose of Morte is to serve as a standardized format for+ encoding and transmission of functional code between distributed services or+ different functional languages. Morte restricts itself to lambda calculus+ 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+ 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.++ If you have problems, questions, or feature requests, you can open an issue+ on the issue tracker on Github:++ <https://github.com/Gabriel439/Haskell-Morte-Library/issues>+-}