morte 1.5.1 → 1.6.0
raw patch · 9 files changed
+290/−154 lines, 9 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
- Morte.Core: URL :: String -> Path
+ Morte.Core: URL :: Text -> Path
- Morte.Import: load :: Expr Path -> IO (Expr X)
+ Morte.Import: load :: Maybe Path -> Expr Path -> IO (Expr X)
- Morte.Lexer: URL :: String -> Token
+ Morte.Lexer: URL :: Text -> Token
Files
- bench/Main.hs +1/−1
- exec/Main.hs +4/−4
- morte.cabal +2/−2
- src/Morte/Core.hs +26/−21
- src/Morte/Import.hs +204/−81
- src/Morte/Lexer.x +20/−12
- src/Morte/Parser.hs +1/−1
- src/Morte/Tutorial.hs +31/−31
- test/Main.hs +1/−1
bench/Main.hs view
@@ -19,7 +19,7 @@ text <- Text.readFile str case Morte.exprFromText text of Left e -> throwIO e- Right expr -> Morte.load expr+ Right expr -> Morte.load Nothing expr main :: IO () main = defaultMain
exec/Main.hs view
@@ -3,14 +3,14 @@ import Control.Exception (Exception, throwIO) import Data.Monoid (mempty) import Data.Traversable-import qualified Data.Text.Lazy.IO as Text import Morte.Core (typeOf, pretty, normalize)+import Morte.Import (load) import Morte.Parser (exprFromText) import Options.Applicative hiding (Const) import System.IO (stderr) import System.Exit (exitFailure) -import Morte.Import (load)+import qualified Data.Text.Lazy.IO as Text throws :: Exception e => Either e a -> IO a throws (Left e) = throwIO e@@ -72,7 +72,7 @@ Default -> do inText <- Text.getContents expr <- throws (exprFromText inText)- expr' <- load expr+ expr' <- load Nothing expr typeExpr <- throws (typeOf expr') Text.hPutStrLn stderr (pretty (normalize typeExpr)) Text.hPutStrLn stderr mempty@@ -80,7 +80,7 @@ Resolve -> do inText <- Text.getContents expr <- throws (exprFromText inText)- expr' <- load expr+ expr' <- load Nothing expr Text.putStrLn (pretty expr') TypeCheck -> do inText <- Text.getContents
morte.cabal view
@@ -1,5 +1,5 @@ Name: morte-Version: 1.5.1+Version: 1.6.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.2@@ -22,7 +22,7 @@ . "Morte.Lexer" contains the @alex@-generated lexer for Morte .- "Morte.Parser" contains the @happy@-generated parser for Morte+ "Morte.Parser" contains the parser for Morte . Read "Morte.Tutorial" to learn how to use this library Category: Compiler
src/Morte/Core.hs view
@@ -69,32 +69,31 @@ TypeMessage(..), ) where -import Control.Applicative (Applicative(pure, (<*>)), (<$>))+import Control.Applicative (Applicative(..), (<$>)) import Control.DeepSeq (NFData(..)) import Control.Exception (Exception) import Control.Monad (mzero)-import Control.Monad.Trans.State (evalState)-import qualified Control.Monad.Trans.State as State import Data.Binary (Binary(..), Get, Put)-import Data.Binary.Get (getWord64le)-import Data.Binary.Put (putWord64le)-import Data.Foldable (Foldable(..))+import Data.Foldable import Data.Monoid ((<>)) import Data.String (IsString(..)) import Data.Text.Buildable (Buildable(..))-import Data.Text.Lazy (Text, unpack)-import qualified Data.Text.Encoding as Text-import qualified Data.Text.Lazy as Text-import qualified Data.Text.Lazy.Builder as Builder-import Data.Traversable (Traversable(..))+import Data.Text.Lazy (Text)+import Data.Traversable import Data.Typeable (Typeable) import Data.Word (Word8) import Filesystem.Path.CurrentOS (FilePath)-import qualified Filesystem.Path.CurrentOS as Filesystem import Morte.Context (Context) import Prelude hiding (FilePath) -import qualified Morte.Context as Context+import qualified Control.Monad.Trans.State.Strict as State+import qualified Data.Binary.Get as Get+import qualified Data.Binary.Put as Put+import qualified Data.Text.Encoding as Text+import qualified Data.Text.Lazy as Text+import qualified Data.Text.Lazy.Builder as Builder+import qualified Filesystem.Path.CurrentOS as Filesystem+import qualified Morte.Context as Context {-| Label for a bound variable @@ -143,8 +142,8 @@ instance Binary Var where put (V x n) = do putUtf8 x- putWord64le (fromIntegral n)- get = V <$> getUtf8 <*> fmap fromIntegral getWord64le+ Put.putWord64le (fromIntegral n)+ get = V <$> getUtf8 <*> fmap fromIntegral Get.getWord64le instance IsString Var where@@ -204,14 +203,20 @@ -- | Path to an external resource data Path = File FilePath- | URL String+ | URL Text deriving (Eq, Ord, Show) instance Buildable Path where- build (File file) = "#" <> build (toText' file) <> " "+ build (File file)+ | Text.isPrefixOf "./" txt+ || Text.isPrefixOf "/" txt+ || Text.isPrefixOf "../" txt+ = build txt <> " "+ | otherwise+ = "./" <> build txt <> " " where- toText' = either id id . Filesystem.toText- build (URL str ) = "#" <> build str <> " "+ txt = Text.fromStrict (either id id (Filesystem.toText file))+ build (URL str ) = build str <> " " {-| Like `Data.Void.Void`, except with an `NFData` instance in order to avoid orphan instances@@ -283,7 +288,7 @@ nR' = if xR == xR' then nR - 1 else nR instance Eq a => Eq (Expr a) where- eL0 == eR0 = evalState (go (normalize eL0) (normalize eR0)) []+ eL0 == eR0 = State.evalState (go (normalize eL0) (normalize eR0)) [] where -- go :: Expr a -> Expr a -> State [(Text, Text)] Bool go (Const cL) (Const cR) = return (cL == cR)@@ -441,7 +446,7 @@ } deriving (Typeable) instance Show TypeError where- show = unpack . pretty+ show = Text.unpack . pretty instance Exception TypeError
src/Morte/Import.hs view
@@ -5,21 +5,22 @@ {-| Morte lets you import external expressions located either in local files or hosted on network endpoints. - To import a local file as an expression, just prepend the file path with a- hash tag. For example, suppose we had the following three local files:+ To import a local file as an expression, just insert the path to the file,+ prepending a @./@ if the path is relative to the current directory. For+ example, suppose we had the following three local files: > -- id > \(a : *) -> \(x : a) -> x > -- Bool- > forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> True+ > forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> Bool > -- True > \(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True You could then reference them within a Morte expression using this syntax: - > #id #Bool #True+ > ./id ./Bool ./True ... which would embed their expressions directly within the syntax tree: @@ -28,27 +29,31 @@ > (forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> True) > (\(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True) + ... and which normalizes to:++ > λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True+ Imported expressions may contain imports of their own, too, which will continue to be resolved. However, Morte will prevent cyclic imports. For example, if you had these two files: > -- foo- > #bar+ > ./bar > -- bar- > #foo+ > ./foo ... Morte would throw the following exception if you tried to import @foo@: > morte: - > ⤷ #foo- > ⤷ #bar- > Cyclic import: #foo+ > ⤷ ./foo+ > ⤷ ./bar+ > Cyclic import: ./foo - You can also import expressions hosted on network endpoints. Just use a- hashtag followed by a URL:+ You can also import expressions hosted on network endpoints. Just use the+ URL - > #http://host[:port]/path+ > http://host[:port]/path The compiler expects the downloaded expressions to be in the same format as local files, specifically UTF8-encoded source code text.@@ -56,7 +61,7 @@ For example, if our @id@ expression were hosted at @http://example.com/id@, then we would embed the expression within our code using: - > #http://example.com/id+ > http://example.com/id You can also reuse directory names as expressions. If you provide a path to a local or remote directory then the compiler will look for a file named@@ -73,34 +78,40 @@ import Control.Exception (Exception, IOException, catch, onException, throwIO) import Control.Monad (join)-import Control.Monad.IO.Class (MonadIO(liftIO))-import Control.Monad.Trans.State.Strict (StateT, evalStateT, get, put)+import Control.Monad.IO.Class (MonadIO(..))+import Control.Monad.Trans.State.Strict (StateT) import Data.Map.Strict (Map)-import qualified Data.Map.Strict as Map import Data.Monoid ((<>)) import Data.Text.Buildable (build)-import qualified Data.Text.Lazy as Text-import qualified Data.Text.Lazy.Encoding as Text+import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder)-import qualified Data.Text.Lazy.Builder as Builder import Data.Traversable (traverse) import Data.Typeable (Typeable)-import Filesystem.Path ((</>))+import Filesystem.Path ((</>), FilePath) import Filesystem as Filesystem import Lens.Micro (Lens') import Lens.Micro.Mtl (zoom)+import Morte.Core (Expr, Path(..), X(..)) import Network.HTTP.Client (Manager)-import qualified Network.HTTP.Client as HTTP-import qualified Network.HTTP.Client.TLS as HTTP import Prelude hiding (FilePath) -import Morte.Core (Expr, Path(..), X(..), typeOf)-import Morte.Parser (exprFromText)+import qualified Control.Monad.Trans.State.Strict as State+import qualified Data.Foldable as Foldable+import qualified Data.List as List+import qualified Data.Map.Strict as Map+import qualified Data.Text.Lazy as Text+import qualified Data.Text.Lazy.Builder as Builder+import qualified Data.Text.Lazy.Encoding as Text+import qualified Morte.Core as Morte+import qualified Morte.Parser as Morte+import qualified Network.HTTP.Client as HTTP+import qualified Network.HTTP.Client.TLS as HTTP+import qualified Filesystem.Path.CurrentOS as Filesystem builderToString :: Builder -> String builderToString = Text.unpack . Builder.toLazyText --- | An import failed because of a cycle import+-- | An import failed because of a cycle in the import graph newtype Cycle = Cycle { cyclicImport :: Path -- ^ The offending cyclic import }@@ -158,9 +169,11 @@ instance Show e => Show (Imported e) where show (Imported paths e) = "\n"- ++ unlines (map (\path -> "⤷ " ++ builderToString (build path))- (reverse paths) )+ ++ unlines (map (\path -> "⤷ " ++ builderToString (build path)) paths') ++ show e+ where+ -- Canonicalize all paths+ paths' = drop 1 (reverse (canonicalizeAll paths)) data Status = Status { _stack :: [Path]@@ -168,6 +181,9 @@ , _manager :: Maybe Manager } +canonicalizeAll :: [Path] -> [Path]+canonicalizeAll = map canonicalize . List.tails+ stack :: Lens' Status [Path] stack k s = fmap (\x -> s { _stack = x }) (k (_stack s)) @@ -179,37 +195,112 @@ needManager :: StateT Status IO Manager needManager = do- x <- zoom manager get+ x <- zoom manager State.get case x of Just m -> return m Nothing -> do let settings = HTTP.tlsManagerSettings { HTTP.managerResponseTimeout = Just 1000000 } -- 1 second m <- liftIO (HTTP.newManager settings)- zoom manager (put (Just m))+ zoom manager (State.put (Just m)) return m --- | Load a `Path` as a \"dynamic\" expression (without resolving any imports)+{-| This function computes the current path by taking the last absolute path+ (either an absolute `FilePath` or `URL`) and combining it with all following+ relative paths++ For example, if the file `./foo/bar` imports `./baz`, that will resolve to+ `./foo/baz`. Relative imports are relative to a file's parent directory.+ This also works for URLs, too.++ This code is full of all sorts of edge cases so it wouldn't surprise me at+ all if you find something broken in here. Most of the ugliness is due to:++ * Handling paths ending with @/\@@ by stripping the @/\@@ suffix if and only+ if you navigate to any downstream relative paths+ * Removing spurious @.@s and @..@s from the path++ Also, there are way too many `reverse`s in the URL-handling cod For now I+ don't mind, but if were to really do this correctly we'd store the URLs as+ `Text` for O(1) access to the end of the string. The only reason we use+ `String` at all is for consistency with the @http-client@ library.+-}+canonicalize :: [Path] -> Path+canonicalize [] = File "."+canonicalize (File file0:paths0) =+ if Filesystem.relative file0+ then go file0 paths0+ else File (clean file0)+ where+ go currPath [] = File (clean currPath)+ go currPath (URL url0:_ ) = combine prefix suffix+ where+ prefix = parentURL (removeAtFromURL url0)++ suffix = clean currPath++ -- `clean` will resolve internal @.@/@..@'s in @currPath@, but we still+ -- need to manually handle @.@/@..@'s at the beginning of the path+ combine url path = case Filesystem.stripPrefix ".." path of+ Just path' -> combine url' path'+ where+ url' = parentURL (removeAtFromURL url)+ Nothing -> case Filesystem.stripPrefix "." path of+ Just path' -> combine url path'+ Nothing -> + -- This `last` is safe because the lexer constraints all+ -- URLs to be non-empty. I couldn't find a simple and safe+ -- equivalent in the `text` API+ case Text.last url of+ '/' -> URL (url <> path')+ _ -> URL (url <> "/" <> path')+ where+ path' = Text.fromStrict (case Filesystem.toText path of+ Left txt -> txt+ Right txt -> txt )+ go currPath (File file:paths) =+ if Filesystem.relative file+ then go file' paths+ else File (clean file')+ where+ file' = Filesystem.parent (removeAtFromFile file) </> currPath+canonicalize (URL path:_) = URL path++parentURL :: Text -> Text+parentURL = Text.dropWhileEnd (/= '/')++removeAtFromURL:: Text -> Text+removeAtFromURL url+ | Text.isSuffixOf "/@" url = Text.dropEnd 2 url+ | Text.isSuffixOf "/" url = Text.dropEnd 1 url+ | otherwise = url++removeAtFromFile :: FilePath -> FilePath+removeAtFromFile file =+ if Filesystem.filename file == "@"+ then Filesystem.parent file+ else file++-- | Remove all @.@'s and @..@'s in the path+clean :: FilePath -> FilePath+clean = strip . Filesystem.collapse+ where+ strip p = case Filesystem.stripPrefix "." p of+ Nothing -> p+ Just p' -> p'++{-| Load a `Path` as a \"dynamic\" expression (without resolving any imports)++ This also returns the true final path (i.e. explicit "/@" at the end for+ directories)+-} loadDynamic :: Path -> StateT Status IO (Expr Path) loadDynamic p = do- paths <- zoom stack get- txt <- case p of- File file -> do- let readFile' = do- Filesystem.readTextFile file `catch` (\e -> do- -- Unfortunately, GHC throws an `InappropriateType`- -- exception when trying to read a directory, but does not- -- export the exception, so I must resort to a more- -- heavy-handed `catch`- let _ = e :: IOException- -- If the fallback fails, reuse the original exception to- -- avoid user confusion- Filesystem.readTextFile (file </> "@")- `onException` throwIO e )- liftIO (fmap Text.fromStrict readFile')- URL url -> do- request <- liftIO (HTTP.parseUrl url)- m <- needManager+ paths <- zoom stack State.get++ let readURL url = do+ request <- liftIO (HTTP.parseUrl (Text.unpack url))+ m <- needManager let httpLbs' = do HTTP.httpLbs request m `catch` (\e -> case e of HTTP.StatusCodeException _ _ _ -> do@@ -217,69 +308,93 @@ { HTTP.path = HTTP.path request <> "/@" } -- If the fallback fails, reuse the original -- exception to avoid user confusion- HTTP.httpLbs request' m `onException` throwIO e- _ -> throwIO e )+ HTTP.httpLbs request' m+ `onException` throwIO (Imported paths e)+ _ -> throwIO (Imported paths e) ) response <- liftIO httpLbs' case Text.decodeUtf8' (HTTP.responseBody response) of- Left err -> liftIO (throwIO err)+ Left err -> liftIO (throwIO (Imported paths err)) Right txt -> return txt - let abort err = liftIO (throwIO (Imported paths err))- case exprFromText txt of- Left err -> case p of+ let readFile' file = liftIO (do+ (do txt <- Filesystem.readTextFile file+ return (Text.fromStrict txt) ) `catch` (\e -> do+ -- Unfortunately, GHC throws an `InappropriateType`+ -- exception when trying to read a directory, but does not+ -- export the exception, so I must resort to a more+ -- heavy-handed `catch`+ let _ = e :: IOException+ -- If the fallback fails, reuse the original exception to+ -- avoid user confusion+ let file' = file </> "@"+ txt <- Filesystem.readTextFile file'+ `onException` throwIO (Imported paths e)+ return (Text.fromStrict txt) ) )++ txt <- case canonicalize (p:paths) of+ File file -> readFile' file+ URL url -> readURL url+ + let abort err = liftIO (throwIO (Imported (p:paths) err))+ case Morte.exprFromText txt of+ Left err -> case canonicalize (p:paths) of URL url -> do -- Also try the fallback in case of a parse error, since the -- parse error might signify that this URL points to a directory -- list- request <- liftIO (HTTP.parseUrl url)+ request <- liftIO (HTTP.parseUrl (Text.unpack url)) let request' = request { HTTP.path = HTTP.path request <> "/@" } m <- needManager response <- liftIO (HTTP.httpLbs request' m `onException` abort err) case Text.decodeUtf8' (HTTP.responseBody response) of Left _ -> liftIO (abort err)- Right txt' -> case exprFromText txt' of+ Right txt' -> case Morte.exprFromText txt' of Left _ -> liftIO (abort err) Right expr -> return expr- _ -> liftIO (abort err)- Right expr -> return expr + _ -> liftIO (abort err)+ Right expr -> return expr -- | Load a `Path` as a \"static\" expression (with all imports resolved) loadStatic :: Path -> StateT Status IO (Expr X) loadStatic path = do- paths <- zoom stack get+ paths <- zoom stack State.get - let local (URL url) = case HTTP.parseUrl url of+ let local (URL url) = case HTTP.parseUrl (Text.unpack url) of Nothing -> False Just request -> case HTTP.host request of "127.0.0.1" -> True "localhost" -> True _ -> False local (File _) = True- case paths of- parent:_ ->- if local path && not (local parent)- then liftIO (throwIO (Imported paths (ReferentiallyOpaque path)))- else return ()- _ -> return () - let paths' = path:paths- zoom stack (put paths')- (expr, cached) <- if path `elem` paths+ let parent = canonicalize paths+ let here = canonicalize (path:paths)++ if local here && not (local parent)+ then liftIO (throwIO (Imported paths (ReferentiallyOpaque path)))+ else return ()++ (expr, cached) <- if here `elem` canonicalizeAll paths then liftIO (throwIO (Imported paths (Cycle path))) else do- m <- zoom cache get- case Map.lookup path m of+ m <- zoom cache State.get+ case Map.lookup here m of Just expr -> return (expr, True) Nothing -> do expr' <- loadDynamic path expr'' <- case traverse (\_ -> Nothing) expr' of -- No imports left Just expr -> do- zoom cache (put $! Map.insert path expr m)+ zoom cache (State.put $! Map.insert here expr m) return expr -- Some imports left, so recurse- Nothing -> fmap join (traverse loadStatic expr')+ Nothing -> do+ let paths' = path:paths+ zoom stack (State.put paths')+ expr'' <- fmap join (traverse loadStatic expr')+ zoom stack (State.put paths)+ return expr'' return (expr'', False) -- Type-check expressions here for two separate reasons:@@ -291,16 +406,24 @@ -- have already been checked if cached then return ()- else case typeOf expr of- Left err -> liftIO (throwIO (Imported paths' err))+ else case Morte.typeOf expr of+ Left err -> liftIO (throwIO (Imported (path:paths) err)) Right _ -> return () - zoom stack (put paths)- return expr --- | Resolve all imports within an expression-load :: Expr Path -> IO (Expr X)-load expr = evalStateT (fmap join (traverse loadStatic expr)) status+{-| Resolve all imports within an expression++ By default the starting path is the current directory, but you can override+ the starting path with a file if you read in the expression from that file+-}+load+ :: Maybe Path+ -- ^ Starting path+ -> Expr Path+ -- ^ Expression to resolve+ -> IO (Expr X)+load here expr =+ State.evalStateT (fmap join (traverse loadStatic expr)) status where- status = Status [] Map.empty Nothing+ status = Status (Foldable.toList here) Map.empty Nothing
src/Morte/Lexer.x view
@@ -12,18 +12,21 @@ LocatedToken(..) ) where -import Control.Monad.Trans.State.Strict (State, get)+import Control.Monad.Trans.State.Strict (State) import Data.Bits (shiftR, (.&.)) import Data.Char (digitToInt, ord)+import Data.Int (Int64) import Data.Text.Lazy (Text)-import qualified Data.Text.Lazy as Text import Data.Word (Word8) import Filesystem.Path.CurrentOS (FilePath)-import qualified Filesystem.Path.CurrentOS as Filesystem import Lens.Micro.Mtl ((.=), (+=)) import Pipes (Producer, for, lift, yield) import Prelude hiding (FilePath) +import qualified Control.Monad.Trans.State.Strict as State+import qualified Data.Text.Lazy as Text+import qualified Filesystem.Path.CurrentOS as Filesystem+ } $digit = 0-9@@ -55,19 +58,24 @@ "\" | "λ" { \_ -> yield Lambda } $fst $labelchar* | "(" $opchar+ ")" { \text -> yield (Label text) } $digit+ { \text -> yield (Number (toInt text)) }- "#https://" $nonwhite+ { \text -> yield (URL (toUrl text)) }- "#http://" $nonwhite+ { \text -> yield (URL (toUrl text)) }- "#" $nonwhite+ { \text -> yield (File (toFile text)) }+ "#https://" $nonwhite+ { \text -> yield (URL (toUrl 1 text)) }+ "#http://" $nonwhite+ { \text -> yield (URL (toUrl 1 text)) }+ "https://" $nonwhite+ { \text -> yield (URL (toUrl 0 text)) }+ "http://" $nonwhite+ { \text -> yield (URL (toUrl 0 text)) }+ "#" $nonwhite+ { \text -> yield (File (toFile 1 text))}+ "/" $nonwhite+ { \text -> yield (File (toFile 0 text))}+ "./" $nonwhite+ { \text -> yield (File (toFile 2 text))}+ "../" $nonwhite+ { \text -> yield (File (toFile 0 text))} { toInt :: Text -> Int toInt = Text.foldl' (\x c -> 10 * x + digitToInt c) 0 -toUrl :: Text -> String-toUrl = Text.unpack . Text.drop 1+toUrl :: Int64 -> Text -> Text+toUrl = Text.drop -toFile :: Text -> FilePath-toFile = Filesystem.fromText . Text.toStrict . Text.drop 1+toFile :: Int64 -> Text -> FilePath+toFile n = Filesystem.fromText . Text.toStrict . Text.drop n -- This was lifted almost intact from the @alex@ source code encode :: Char -> (Word8, [Word8])@@ -138,7 +146,7 @@ lexExpr text = for (go (AlexInput '\n' [] text)) tag where tag token = do- pos <- lift get+ pos <- lift State.get yield (LocatedToken token pos) go input = case alexScan input 0 of@@ -172,7 +180,7 @@ | Label Text | Number Int | File FilePath- | URL String+ | URL Text | EOF deriving (Eq, Show) }
src/Morte/Parser.hs view
@@ -62,7 +62,7 @@ unsafeFromFile (LocatedToken (Lexer.File n) _) = n -url :: Prod r e LocatedToken String+url :: Prod r e LocatedToken Text url = fmap unsafeFromURL (satisfy isURL) where isURL (LocatedToken (Lexer.URL _) _) = True
src/Morte/Tutorial.hs view
@@ -2035,11 +2035,11 @@ > -> \(Zero : Nat) > -> Succ (n Nat Succ Zero) - You can then import any of these expressions by prepending their file name- with a hash tag. For example:+ You can then import any of these expressions by their file name (as long as+ you prefix relative paths with @./@). For example: > $ morte-> #Succ (#Succ (#Succ #Zero ))+> ./Succ (./Succ (./Succ ./Zero )) > <Ctrl-D> > ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat >@@ -2049,7 +2049,7 @@ were to write: > $ morte-> #Succ (#Succ (#Succ #Zero))+> ./Succ (./Succ (./Succ ./Zero)) ... then you would get this parsing error: @@ -2069,7 +2069,7 @@ file, so it would be as if you wrote the following really long expression: > $ morte-> -- #Succ+> -- ./Succ > ( \( n > : forall (Nat : *) > -> forall (Succ : Nat -> Nat)@@ -2081,7 +2081,7 @@ > -> \(Zero : Nat) > -> Succ (n Nat Succ Zero) > )-> ( -- #Succ+> ( -- ./Succ > ( \( n > : forall (Nat : *) > -> forall (Succ : Nat -> Nat)@@ -2093,7 +2093,7 @@ > -> \(Zero : Nat) > -> Succ (n Nat Succ Zero) > )-> ( -- #Succ+> ( -- ./Succ > ( \( n > : forall (Nat : *) > -> forall (Succ : Nat -> Nat)@@ -2105,7 +2105,7 @@ > -> \(Zero : Nat) > -> Succ (n Nat Succ Zero) > )-> -- #Zero+> -- ./Zero > ( \(Nat : *) > -> \(Succ : Nat -> Nat) > -> \(Zero : Nat)@@ -2129,60 +2129,60 @@ expressions like: > $ morte-> #id #Bool #Bool/True+> ./id ./Bool ./Bool/True > <Ctrl-D> > ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool > > λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True > $ morte > exampleNumber # Save an example number to the file `exampleNumber`-> #Nat/Succ (#Nat/Succ (#Nat/Succ #Nat/Zero ))+> ./Nat/Succ (./Nat/Succ (./Nat/Succ ./Nat/Zero )) > <Ctrl-D> > ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat > > $ morte # Now we can import our saved number-> #Nat/(+) #exampleNumber #exampleNumber+> ./Nat/(+) ./exampleNumber ./exampleNumber > <Ctrl-D> > ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat > > λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zero))))) > $ morte-> #even #exampleNumber+> ./even ./exampleNumber > <Ctrl-D> > ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool > > λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False-> $ morte > exampleList #Save an example list to the file `exampleList`-> #List/Cons #Bool #Bool/True (#List/Cons #Bool #Bool/True (#List/Cons #Bool #Bool/False (#List/Nil #Bool )))+> $ morte > exampleList # Save an example list to the file `exampleList`+> ./List/Cons ./Bool ./Bool/True (./List/Cons ./Bool ./Bool/True (./List/Cons ./Bool ./Bool/False (./List/Nil ./Bool ))) > <Ctrl-D> > ∀(List : *) → ∀(Cons : ∀(head : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → ∀(tail : List) → List) → ∀(Nil : List) → List > > $ morte-> #length #Bool #exampleList+> ./length ./Bool ./exampleList > <Ctrl-D> > ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat > > λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero)) > $ morte-> #Bool/and #exampleList+> ./Bool/and ./exampleList > <Ctrl-D> > ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool > > λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False > $ morte > double # We can even save functions-> \(n : #Nat ) -> #Nat/(+) n n+> \(n : ./Nat ) -> ./Nat/(+) n n > <Ctrl-D> > ∀(n : ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat) → ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat > $ morte # ... then reuse those saved functions-> #double #exampleNumber+> ./double ./exampleNumber > <Ctrl-D> > ∀(Nat : *) → ∀(Succ : Nat → Nat) → ∀(Zero : Nat) → Nat > > λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zero))))) - Notice that some paths (like @#Bool@) actually point to directories. If you+ Notice that some paths (like @./Bool@) actually point to directories. If you provide a directory then Morte will look for a file named @\'\@\'@ located underneath that directory and use that instead. So, for example, if we- specify @#Bool@ that actually translates to the file located at @Bool/\@@.+ specify @./Bool@ that actually translates to the file located at @Bool/\@@. You can also import expressions hosted on network endpoints. For example, there are several example expressions hosted at:@@ -2199,9 +2199,9 @@ We can either import these expressions directly by referencing their URLs: > $ morte-> #http://sigil.place/tutorial/morte/1.2/id -> #http://sigil.place/tutorial/morte/1.2/Bool-> #http://sigil.place/tutorial/morte/1.2/Bool/True+> http://sigil.place/tutorial/morte/1.2/id +> http://sigil.place/tutorial/morte/1.2/Bool+> http://sigil.place/tutorial/morte/1.2/Bool/True > <Ctrl-D> > ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool > @@ -2209,16 +2209,16 @@ ... or we could use local files to create short aliases for these URLs: -> $ echo "#http://sigil.place/tutorial/morte/1.2/id" > id+> $ echo "http://sigil.place/tutorial/morte/1.2/id" > id > $ mkdir Bool-> $ echo "#http://sigil.place/tutorial/morte/1.2/Bool" > Bool/@-> $ echo "#http://sigil.place/tutorial/morte/1.2/Bool/True" > Bool/True+> $ echo "http://sigil.place/tutorial/morte/1.2/Bool" > Bool/@+> $ echo "http://sigil.place/tutorial/morte/1.2/Bool/True" > Bool/True Now whenever we reference these local files they will in turn download the expressions hosted on the URL that they point to: > $ morte-> #id #Bool #Bool/True -- Exact same result, except now using remote code+> ./id ./Bool ./Bool/True -- Exact same result, except now using remote code > <Ctrl-D> > ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool > @@ -2239,9 +2239,9 @@ For example, suppose that we wished to take our contrived example and host it on the network. We'd simply host this text on any URL that we own: -> #http://sigil.place/tutorial/morte/1.2/id-> #http://sigil.place/tutorial/morte/1.2/Bool-> #http://sigil.place/tutorial/morte/1.2/Bool/True+> http://sigil.place/tutorial/morte/1.2/id+> http://sigil.place/tutorial/morte/1.2/Bool+> http://sigil.place/tutorial/morte/1.2/Bool/True ... and then other people would be able to import our code within their programs by referencing our URL. Then when they downloaded our expression@@ -2250,7 +2250,7 @@ Note that when we host an expression on the network we can no longer use local imports within our code. For example, you cannot host code like this: -> #id #Bool #Bool/True+> ./id ./Bool ./Bool/True ... because client compilers that download your code would have no way of retrieving your local files. Fortunately, the compiler enforces that all
test/Main.hs view
@@ -82,7 +82,7 @@ case Morte.exprFromText stdin of Left e -> throwIO e Right expr -> do- expr' <- Morte.load expr+ expr' <- Morte.load Nothing expr case Morte.typeOf expr' of Left e -> throwIO e Right typeExpr -> do