diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/dist/build/Morte/Lexer.hs b/dist/build/Morte/Lexer.hs new file mode 100644 --- /dev/null +++ b/dist/build/Morte/Lexer.hs @@ -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 "" #-} +{-# LINE 1 "" #-} +{-# 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 diff --git a/dist/build/Morte/Parser.hs b/dist/build/Morte/Parser.hs new file mode 100644 --- /dev/null +++ b/dist/build/Morte/Parser.hs @@ -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 "" #-} +{-# LINE 1 "" #-} +{-# 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. diff --git a/exec/Main.hs b/exec/Main.hs new file mode 100644 --- /dev/null +++ b/exec/Main.hs @@ -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)) diff --git a/morte.cabal b/morte.cabal new file mode 100644 --- /dev/null +++ b/morte.cabal @@ -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 diff --git a/src/Morte/Core.hs b/src/Morte/Core.hs new file mode 100644 --- /dev/null +++ b/src/Morte/Core.hs @@ -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\". + + + + + 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!\": + + + + 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 diff --git a/src/Morte/Lexer.x b/src/Morte/Lexer.x new file mode 100644 --- /dev/null +++ b/src/Morte/Lexer.x @@ -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) +} diff --git a/src/Morte/Parser.y b/src/Morte/Parser.y new file mode 100644 --- /dev/null +++ b/src/Morte/Parser.y @@ -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" ) +} diff --git a/src/Morte/Tutorial.hs b/src/Morte/Tutorial.hs new file mode 100644 --- /dev/null +++ b/src/Morte/Tutorial.hs @@ -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 +> +> ∀(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 (... +> +> ... 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: + + +-}