diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2017 The Disciplined Disciple Compiler Strike Force + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. 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/shimmer.cabal b/shimmer.cabal new file mode 100644 --- /dev/null +++ b/shimmer.cabal @@ -0,0 +1,70 @@ +name: shimmer +version: 0.1.1 +license: MIT +license-file: LICENSE +author: Ben Lippmeier +maintainer: Ben Lippmeier +build-type: Simple +cabal-version: >=1.6 +category: Compilers/Interpreters +description: The Reflective Lambda Machine +synopsis: The Reflective Lambda Machine + +library + hs-source-dirs: + src + + build-depends: + base >= 4.10 && < 4.11, + text >= 1.2 && < 1.3, + vector >= 0.12 && < 0.13, + containers >= 0.5 && < 0.6, + bytestring >= 0.10 && < 0.11, + filepath >= 1.4.0 && < 1.5, + haskeline >= 0.7 && < 0.8 + + exposed-modules: + SMR.Codec.Peek + SMR.Codec.Poke + SMR.Codec.Size + + SMR.Core.Exp + SMR.Core.Step + SMR.Core.World + + SMR.Data.Bag + SMR.Data.Located + + SMR.Prim.Name + + SMR.Prim.Op.Base + SMR.Prim.Op.Bool + SMR.Prim.Op.List + SMR.Prim.Op.Match + SMR.Prim.Op.Nat + SMR.Prim.Op.Nom + SMR.Prim.Op.Sym + SMR.Prim.Op + + SMR.Source.Expected + SMR.Source.Lexer + SMR.Source.Parsec + SMR.Source.Parser + SMR.Source.Pretty + SMR.Source.Token + + other-modules: + SMR.CLI.Driver.Load + SMR.CLI.Config + SMR.CLI.Help + SMR.CLI.Repl + + SMR.Core.Exp.Base + SMR.Core.Exp.Compounds + SMR.Core.Exp.Push + SMR.Core.Exp.Train + + + extensions: + PatternGuards + OverloadedStrings diff --git a/src/SMR/CLI/Config.hs b/src/SMR/CLI/Config.hs new file mode 100644 --- /dev/null +++ b/src/SMR/CLI/Config.hs @@ -0,0 +1,75 @@ + +module SMR.CLI.Config where +import qualified System.Exit as System + + +-- | Command line mode. +data Mode + -- No mode specified. + = ModeNone + + -- Parse and check a .smr source file. + | ModeCheck FilePath + + -- Start the REPL with the given file. + | ModeREPL (Maybe FilePath) + + -- Convert a file from one format to another. + | ModeConvert FilePath FilePath + deriving Show + + +-- | Command line config. +data Config + = Config + { configMode :: Mode } + deriving Show + + +configZero :: Config +configZero + = Config + { configMode = ModeNone } + + +-- | Parse command-line arguments. +parseArgs :: [String] -> Config -> IO Config +parseArgs [] config + = return config + +parseArgs ss config + | "-check" : filePath : ssRest <- ss + = parseArgs ssRest + $ config { configMode = ModeCheck filePath } + + | "-convert" : fileSource : fileDest : ssRest <- ss + = parseArgs ssRest + $ config { configMode = ModeConvert fileSource fileDest } + + | "-help" : _ssRest <- ss + = do putStr usage + System.exitSuccess + + | "--help" : _ssRest <- ss + = do putStr usage + System.exitSuccess + + + | filePath : ssRest <- ss + , c : _ <- filePath + , c /= '-' + = parseArgs ssRest + $ config { configMode = ModeREPL (Just filePath) } + + | otherwise + = do putStr usage + System.exitSuccess + +usage :: String +usage + = unlines + [ "shimmer Start the REPL with no soure file." + , "shimmer FILE Start the REPL with the given file." + , "shimmer -help Display this help page." + , "shimmer -check FILE Check that a source file is well formed." + , "shimmer -convert FILE1 FILE2 Convert file from one format to another." ] diff --git a/src/SMR/CLI/Driver/Load.hs b/src/SMR/CLI/Driver/Load.hs new file mode 100644 --- /dev/null +++ b/src/SMR/CLI/Driver/Load.hs @@ -0,0 +1,53 @@ + +module SMR.CLI.Driver.Load + (runLoadFileDecls) +where +import qualified SMR.Prim.Op as Prim +import qualified SMR.Prim.Name as Prim +import qualified SMR.Source.Parser as Source +import qualified SMR.Source.Lexer as Source +import qualified SMR.Codec.Peek as Codec +import SMR.Core.Exp (Decl) +import SMR.Prim.Op.Base (Prim) + +import qualified Foreign.Marshal.Alloc as Foreign + +import qualified System.FilePath as System +import qualified System.IO as System +import Control.Monad +import Data.Text (Text) + + +-- | Load decls from the given file. +runLoadFileDecls :: FilePath -> IO [Decl Text Prim] +runLoadFileDecls path + -- Shimmer text source file. + | System.takeExtension path == ".smr" + = do str <- readFile path + + let (ts, _loc, _csRest) + = Source.lexTokens (Source.L 1 1) str + + let config + = Source.Config + { Source.configReadSym = Just + , Source.configReadPrm = Prim.readPrim Prim.primOpTextNames } + + case Source.parseDecls config ts of + Left err -> error $ show err + Right decls -> return decls + + + -- Shimmer binary store file. + | System.takeExtension path == ".sms" + = do + h <- System.openBinaryFile path System.ReadMode + nSize <- fmap fromIntegral $ System.hFileSize h + Foreign.allocaBytes nSize $ \pBuf + -> do nRead <- System.hGetBuf h pBuf nSize + when (nRead /= nSize) $ error "runConvert: short read" + (decls, _p, _n) <- Codec.peekFileDecls pBuf nSize + return decls + + | otherwise + = error "runLoadFileDecls: cannot load this file" diff --git a/src/SMR/CLI/Help.hs b/src/SMR/CLI/Help.hs new file mode 100644 --- /dev/null +++ b/src/SMR/CLI/Help.hs @@ -0,0 +1,58 @@ + +module SMR.CLI.Help where + + +helpCommands :: String +helpCommands + = unlines $ + [ " :quit,:q Quit the REPL." + , " :help Show this Help page." + , " :grammar Show the language grammar." + , " :prims Show the list of available primitives." + , " :reload,:r Reload the current source files." + , " :decls NAMES? Show named declarations, or all decls if no names given." + , " :parse EXP Parse an expression and print it back." + , " :push EXP Push down substitutions in an expression." + , " :step EXP Single step evaluate an expression." + , " :steps EXP Multi-step evaluate an expression." + , " :trace EXP Multi-step evaluate an expression, showing intermediate states." ] + + +helpGrammar :: String +helpGrammar + = unlines $ + [ " Decl ::= '@' Name Param* '=' Exp ';' (Macro declaration)" + , "" + , " Exp ::= Ref (External reference)" + , " | Key Exp (Keyword application)" + , " | Exp Exp+ (Function application)" + , " | Name ('^' Nat)? (Variable with lifting specifier)" + , " | '\\' Param+ '.' Exp (Function abstraction)" + , " | Train '.' Exp (Substitution train)" + , "" + , " Ref ::= '@' Name (Macro reference)" + , " | '%' Name (Symbol reference)" + , " | '#' Name (Primitive reference)" + , " | '?' Nat (Nominal reference)" + , "" + , " Key ::= '##tag' (Tag an expression)" + , " | '##seq' (Sequence evaluation)" + , " | '##box' (Box an expression, delaying evaluation)" + , " | '##run' (Run an expression, forcing evaluation)" + , "" + , " Param ::= Name (Call-by-value parameter)" + , " | '!' Name (Explicitly call-by-value parameter)" + , " | '~' Name (Explicitly call-by-name parameter)" + , "" + , " Train ::= Car+ (Substitution train)" + , "" + , " Car ::= '[' Bind,* ']' (Simultaneous substitution)" + , " | '[[' Bind,* ']]' (Recursive substitution)" + , " | '{' Bump,* '}' (Lifting specifier)" + , "" + , " Bind ::= Name ('^' Nat)? '=' Exp (Variable substitution binding)" + , " | '?' Nat '=' Exp (Nominal substitution binding)" + , "" + , " Bump ::= Name ('^' Nat)? ':' Nat (Lifting bump)" + ] + diff --git a/src/SMR/CLI/Repl.hs b/src/SMR/CLI/Repl.hs new file mode 100644 --- /dev/null +++ b/src/SMR/CLI/Repl.hs @@ -0,0 +1,386 @@ +{-# LANGUAGE BangPatterns #-} +module SMR.CLI.Repl where +import SMR.Core.Exp +import qualified SMR.CLI.Help as Help +import qualified SMR.CLI.Driver.Load as Driver +import qualified SMR.Core.Step as Step +import qualified SMR.Core.World as World +import qualified SMR.Prim.Name as Prim +import qualified SMR.Prim.Op as Prim +import qualified SMR.Prim.Op.Base as Prim +import qualified SMR.Source.Parser as Source +import qualified SMR.Source.Lexer as Source +import qualified SMR.Source.Pretty as Source +import qualified SMR.Source.Expected as Source +import qualified Data.Text.Lazy.IO as TL +import qualified Data.Text.Lazy.Builder as BL +import qualified System.Console.Haskeline as HL +import qualified Data.Char as Char +import qualified Data.Map as Map +import qualified Data.Set as Set +import qualified Data.Text as Text +import Control.Monad.IO.Class +import Data.Text (Text) +import Data.Set (Set) +import Data.Monoid + + +------------------------------------------------------------------------------- +data Mode s p w + = ModeNone + | ModeParse + | ModePush (Exp s p) + | ModeStep (Step.Config s p w) (Exp s p) + + +data State s p w + = State + { -- | Current interpreter mode. + stateMode :: Mode s p w + + -- | Top-level declarations parsed from source files. + , stateDecls :: [Decl s p] + + -- | Working source files. + , stateFiles :: [FilePath] + + -- | Execution world. + , stateWorld :: World.World w } + + +type RState = State Text Prim.Prim () +type RConfig = Step.Config Text Prim.Prim () +type RWorld = World.World () +type RDecl = Decl Text Prim.Prim +type RExp = Exp Text Prim.Prim + + +------------------------------------------------------------------------------- +replStart :: RState -> IO () +replStart state + = HL.runInputT HL.defaultSettings + $ do HL.outputStrLn "Shimmer, version 0.1. The Lambda Machine." + HL.outputStrLn "Type :help for help." + replReload state + + +-- | Main repl loop dispatcher +replLoop :: RState -> HL.InputT IO () +replLoop state + = do minput <- HL.getInputLine "> " + case minput of + Nothing + -> return () + + Just input + | all Char.isSpace input + -> case stateMode state of + ModeNone -> replLoop state + ModePush xx -> replPush_next state xx + ModeStep c xx -> replStep_next state c xx + _ -> replLoop state + + | otherwise + -> case words input of + ":quit" : [] -> replQuit state + ":help" : [] -> replHelp state + ":reload" : [] -> replReload state + ":r" : [] -> replReload state + ":grammar" : [] -> replGrammar state + ":prims" : [] -> replPrims state + + ":decls" : xs + -> let strip ('@' : name) = name + strip name = name + in replDecls state + $ Set.fromList $ map Text.pack + $ map strip xs + + ":parse" : xs -> replParse state (unwords xs) + ":push" : xs -> replPush state (unwords xs) + ":step" : xs -> replStep state (unwords xs) + ":steps" : xs -> replSteps state (unwords xs) + ":trace" : xs -> replTrace state (unwords xs) + _ -> replSteps state input + + +------------------------------------------------------------------------------- +-- | Quit the repl. +replQuit :: RState -> HL.InputT IO () +replQuit _state + = do return () + + +------------------------------------------------------------------------------- +-- | Display the help page. +replHelp :: RState -> HL.InputT IO () +replHelp state + = do HL.outputStr $ Help.helpCommands + replLoop state + + +------------------------------------------------------------------------------- +-- | Display the language grammar. +replGrammar :: RState -> HL.InputT IO () +replGrammar state + = do HL.outputStr $ Help.helpGrammar + replLoop state + + +------------------------------------------------------------------------------- +-- | Display the list of primops. +replPrims :: RState -> HL.InputT IO () +replPrims state + = do HL.outputStrLn + $ " name params description" + + HL.outputStrLn + $ " ---- ------ -----------" + + HL.outputStr + $ unlines + [ " #unit unit value" + , " #true boolean true" + , " #false boolean false" + , " #nat'NAT natural number" + , " #list list constructor" ] + + HL.outputStr + $ unlines + $ [ leftPad 16 (" #" ++ (Text.unpack $ name)) + ++ leftPad 10 (concat [showForm f | f <- Prim.primEvalForm p]) + ++ Text.unpack (Prim.primEvalDesc p) + + | p@(Prim.PrimEval { Prim.primEvalName = Prim.PrimOp name }) + <- Prim.primEvals ] + + replLoop state + +showForm :: Form -> String +showForm PVal = "!" +showForm PExp = "~" + +leftPad :: Int -> [Char] -> [Char] +leftPad n ss + = ss ++ replicate (n - length ss) ' ' + + +------------------------------------------------------------------------------- +-- | Display the list of current declarations. +replDecls :: RState -> Set Name -> HL.InputT IO () +replDecls state names + = do liftIO $ mapM_ (printDecl names) + $ stateDecls state + + replLoop state + + +printDecl :: Set Name -> RDecl -> IO () +printDecl names decl + | Set.null names + = do TL.putStr + $ BL.toLazyText + $ Source.buildDecl decl + + | DeclMac name _ <- decl + , Set.member name names + = do TL.putStr + $ BL.toLazyText + $ Source.buildDecl decl + + | otherwise + = return () + + +------------------------------------------------------------------------------- +-- | Reload the current source file. +replReload :: RState -> HL.InputT IO () +replReload state + = do + decls <- liftIO + $ fmap concat $ mapM Driver.runLoadFileDecls + $ stateFiles state + + replLoop (state + { stateDecls = decls }) + + +------------------------------------------------------------------------------- +-- | Parse and print back an expression. +replParse :: RState -> String -> HL.InputT IO () +replParse state str + = do result <- liftIO $ replParseExp state str + case result of + Nothing + -> replLoop state + + Just xx + -> do liftIO $ TL.putStrLn + $ BL.toLazyText + $ Source.buildExp Source.CtxTop xx + HL.outputStr "\n" + + replLoop state + + +------------------------------------------------------------------------------- +-- | Parse an expression and push down substitutions. +replPush :: RState -> String -> HL.InputT IO () +replPush state str + = do result <- liftIO $ replParseExp state str + case result of + Nothing -> replLoop state + Just xx -> replPush_next state xx + + +-- | Advance the train pusher. +replPush_next :: RState -> RExp -> HL.InputT IO () +replPush_next state xx + = case pushDeep xx of + Nothing -> replLoop $ state { stateMode = ModeNone } + Just xx' + -> do liftIO $ TL.putStrLn + $ BL.toLazyText + $ Source.buildExp Source.CtxTop xx' + + replLoop $ state { stateMode = ModePush xx' } + + +------------------------------------------------------------------------------- +-- | Parse an expression and single-step it. +replStep :: RState -> String -> HL.InputT IO () +replStep state str + = replLoadExp state str replStep_next + +-- | Advance the single stepper. +replStep_next + :: RState -> RConfig -> RExp + -> HL.InputT IO () + +replStep_next state config xx + = do erx <- liftIO $ Step.step config (stateWorld state) xx + case erx of + Left Step.ResultDone + -> replLoop $ state { stateMode = ModeNone } + + Left (Step.ResultError msg) + -> do HL.outputStrLn + $ Text.unpack + $ Text.pack "error: " <> msg + + Right xx' + -> do liftIO $ TL.putStrLn + $ BL.toLazyText + $ Source.buildExp Source.CtxTop xx' + + replLoop $ state { stateMode = ModeStep config xx' } + + +------------------------------------------------------------------------------- +-- | Parse an expression and normalize it. +replSteps :: RState -> String -> HL.InputT IO () +replSteps state str + = replLoadExp state str replSteps_next + +-- | Advance the evaluator stepper. +replSteps_next + :: RState -> RConfig -> RExp + -> HL.InputT IO () + +replSteps_next state config xx + = do erx <- liftIO $ Step.steps config (stateWorld state) xx + case erx of + Left msg + -> do HL.outputStrLn + $ Text.unpack + $ Text.pack "error: " <> msg + + Right xx' + -> do liftIO $ TL.putStrLn + $ BL.toLazyText + $ Source.buildExp Source.CtxTop xx' + + replLoop $ state { stateMode = ModeNone } + + +------------------------------------------------------------------------------- +-- | Parse an expression and normalize it, +-- printing out each intermediate state. +replTrace :: RState -> String -> HL.InputT IO () +replTrace state str + = replLoadExp state str replTrace_next + +-- | Advance the evaluator stepper. +replTrace_next + :: RState -> RConfig -> RExp + -> HL.InputT IO () + +replTrace_next state config !xx0 + = loop xx0 + where + loop !xx + = do erx <- liftIO $ Step.step config (stateWorld state) xx + case erx of + Left (Step.ResultError msg) + -> do HL.outputStrLn + $ Text.unpack + $ Text.pack "error: " <> msg + + Left Step.ResultDone + -> replLoop $ state { stateMode = ModeNone } + + Right xx' + -> do liftIO $ TL.putStrLn + $ BL.toLazyText + $ Source.buildExp Source.CtxTop xx' + + loop xx' + +------------------------------------------------------------------------------- +replLoadExp + :: RState -> String + -> (RState -> RConfig -> RExp -> HL.InputT IO ()) + -> HL.InputT IO () +replLoadExp state str eat + = do result <- liftIO $ replParseExp state str + case result of + Nothing -> replLoop state + + Just xx + -> let + decls = Map.fromList + $ [ (n, x) | DeclMac n x <- stateDecls state ] + + prims = Map.fromList + $ [ (Prim.primEvalName p, p) | p <- Prim.primEvals ] + + config = Step.Config + { Step.configUnderLambdas = True + , Step.configHeadArgs = True + , Step.configDeclsMac = decls + , Step.configPrims = prims } + + in eat state config xx + + +------------------------------------------------------------------------------- +replParseExp :: RState -> String -> IO (Maybe RExp) +replParseExp _state str + = do let (ts, _loc, _csRest) + = Source.lexTokens (Source.L 1 1) str + + let config + = Source.Config + { Source.configReadSym = Just + , Source.configReadPrm = Prim.readPrim Prim.primOpTextNames } + + case Source.parseExp config ts of + Left err + -> do liftIO $ putStrLn + $ "parse error\n" + ++ Source.pprParseError err + return Nothing + + Right xx + -> return (Just xx) + diff --git a/src/SMR/Codec/Peek.hs b/src/SMR/Codec/Peek.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Codec/Peek.hs @@ -0,0 +1,486 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE BangPatterns #-} +module SMR.Codec.Peek + ( peekFileDecls + , peekDecl + , peekExp, peekKey, peekParam + , peekCar, peekSnvBind, peekUpsBump + , peekRef + , peekName, peekBump, peekNom + , peekWord8, peekWord16, peekWord32, peekWord64) +where +import SMR.Core.Exp +import SMR.Prim.Op.Base + +import qualified Foreign.Marshal.Utils as F +import qualified Foreign.Marshal.Alloc as F +import qualified Foreign.Storable as F +import qualified Foreign.Ptr as F + +import qualified Data.Text as T +import qualified Data.Text.Encoding as T +import qualified Data.ByteString.Unsafe as BS + +import Control.Monad +import Foreign.Ptr +import Data.Text (Text) +import Data.Bits +import Data.Word + + +--------------------------------------------------------------------------------------------------- +type Peek a = Ptr Word8 -> Int -> IO (a, Ptr Word8, Int) + + +--------------------------------------------------------------------------------------------------- +-- | Peek a list of `Decl` from memory, including the SMR file header. +peekFileDecls :: Peek [Decl Text Prim] +peekFileDecls !p0 !n0 + = do (b0, p1, n1) <- peekWord8 p0 n0 + (b1, p2, n2) <- peekWord8 p1 n1 + (b2, p3, n3) <- peekWord8 p2 n2 + (b3, p4, n4) <- peekWord8 p3 n3 + when ( b0 /= 0x53 || b1 /= 0x4d || b2 /= 0x52 || b3 /= 0x31) + $ error "peekFileDecls: bad magic" + + (ds, p5, n5) <- peekList peekDecl p4 n4 + return (ds, p5, n5) +{-# NOINLINE peekFileDecls #-} + + +-- | Peek a `Decl` from memory. +peekDecl :: Peek (Decl Text Prim) +peekDecl !p0 !n0 + = do (b0, p1, n1) <- peekWord8 p0 n0 + p1 `seq` case b0 of + 0xa1 + -> do (tx, p2, n2) <- peekName p1 n1 + (x, p3, n3) <- peekExp p2 n2 + return (DeclMac tx x, p3, n3) + + 0xa2 + -> do (tx, p2, n2) <- peekName p1 n1 + (x, p3, n3) <- peekExp p2 n2 + return (DeclSet tx x, p3, n3) + + _ -> error "peekDecl: invalid header" +{-# NOINLINE peekDecl #-} + + +--------------------------------------------------------------------------------------------------- +-- | Peek an `Exp` from memory. +peekExp :: Peek (Exp Text Prim) +peekExp !p0 !n0 + = do (b0, p1, n1) <- peekWord8 p0 n0 + p1 `seq` case b0 of + 0xb1 + -> do (r, p2, n2) <- peekRef p1 n1 + return (XRef r, p2, n2) + + 0xb2 + -> do (key, p2, n2) <- peekKey p1 n1 + (xx, p3, n3) <- peekExp p2 n2 + return (XKey key xx, p3, n3) + + 0xb3 + -> do (x1, p2, n2) <- peekExp p1 n1 + (xs, p3, n3) <- peekList peekExp p2 n2 + return (XApp x1 xs, p3, n3) + + 0xb4 + -> do (n, p2, n2) <- peekName p1 n1 + (i, p3, n3) <- peekBump p2 n2 + return (XVar n i, p3, n3) + + 0xb5 + -> do (ps, p2, n2) <- peekList peekParam p1 n1 + (x, p3, n3) <- peekExp p2 n2 + return (XAbs ps x, p3, n3) + + 0xb6 + -> do (cs, p2, n2) <- peekList peekCar p1 n1 + (x, p3, n3) <- peekExp p2 n2 + return (XSub cs x, p3, n3) + + _ -> error "peekExp: invalid header" +{-# NOINLINE peekExp #-} + + +-- | Peek a `Key` from memory. +peekKey :: Peek Key +peekKey !p0 !n0 + = do (b0, p1, n1) <- peekWord8 p0 n0 + p1 `seq` case b0 of + 0xba -> return (KBox, p1, n1) + 0xbb -> return (KRun, p1, n1) + _ -> error $ "peekKey: invalid header" +{-# INLINE peekKey #-} + + +-- | Peek a `Param` from memory. +peekParam :: Peek Param +peekParam !p0 !n0 + = do (b0, p1, n1) <- peekWord8 p0 n0 + p1 `seq` case b0 of + 0xbc + -> do (tx, p2, n2) <- peekName p1 n1 + return (PParam tx PVal, p2, n2) + + 0xbd + -> do (tx, p2, n2) <- peekName p1 n1 + return (PParam tx PExp, p2, n2) + + _ -> error $ "peekParam: invalid header " ++ show b0 ++ " " ++ show p1 +{-# INLINE peekParam #-} + + +-- | Peek a `Car` from memory. +peekCar :: Peek (Car Text Prim) +peekCar !p0 !n0 + = do (b0, p1, n1) <- peekWord8 p0 n0 + p1 `seq` case b0 of + 0xc1 + -> do (sbs, p2, n2) <- peekList peekSnvBind p1 n1 + return (CSim (SSnv sbs), p2, n2) + + 0xc2 + -> do (sbs, p2, n2) <- peekList peekSnvBind p1 n1 + return (CRec (SSnv sbs), p2, n2) + + 0xc3 + -> do (ups, p2, n2) <- peekList peekUpsBump p1 n1 + return (CUps (UUps ups), p2, n2) + + _ -> error $ "peekCar: invalid header" +{-# INLINE peekCar #-} + + +-- | Peek an `SnvBind` from memory. +peekSnvBind :: Peek (SnvBind Text Prim) +peekSnvBind !p0 !n0 + = do (b0, p1, n1) <- peekWord8 p0 n0 + p1 `seq` case b0 of + 0xca + -> do (n, p2, n2) <- peekName p1 n1 + (d, p3, n3) <- peekBump p2 n2 + (x, p4, n4) <- peekExp p3 n3 + return (BindVar n d x, p4, n4) + + 0xcb + -> do (n, p2, n2) <- peekNom p1 n1 + (x, p3, n3) <- peekExp p2 n2 + return (BindNom n x, p3, n3) + + _ -> error $ "peekSnvBind: invalid header" +{-# INLINE peekSnvBind #-} + + +-- | Peek an `UpsBump` from memory. +peekUpsBump :: Peek UpsBump +peekUpsBump !p0 !n0 + = do (b0, p1, n1) <- peekWord8 p0 n0 + when (b0 /= 0xcc) $ error $ "peekUpsBump: invalid header" + (n, p2, n2) <- peekName p1 n1 + (d, p3, n3) <- peekBump p2 n2 + (i, p4, n4) <- peekBump p3 n3 + return $ (((n, d), i), p4, n4) +{-# INLINE peekUpsBump #-} + + +--------------------------------------------------------------------------------------------------- +-- | Peek a `Ref` from memory. +peekRef :: Peek (Ref Text Prim) +peekRef !p0 !n0 + = do (b0, p1, n1) <- peekWord8 p0 n0 + p1 `seq` case b0 of + 0xd1 + -> do (tx, p2, n2) <- peekText p1 n1 + return (RSym tx, p2, n2) + + 0xd2 + -> do (m, p2, n2) <- peekPrim p1 n1 + return (RPrm m, p2, n2) + + 0xd3 + -> do (tx, p2, n2) <- peekText p1 n1 + return (RMac tx, p2, n2) + + 0xd4 + -> do (tx, p2, n2) <- peekText p1 n1 + return (RSet tx, p2, n2) + + 0xd5 + -> do (i, p2, n2) <- peekNom p1 n1 + return (RNom i, p2, n2) + + _ -> error "peekRef: invalid header" +{-# INLINE peekRef #-} + + +--------------------------------------------------------------------------------------------------- +-- | Peek a `Name` from memory. +peekName :: Peek Name +peekName !p !n + = do peekText p n +{-# INLINE peekName #-} + + +-- | Peek a `Bump` counter from memory. +peekBump :: Peek Integer +peekBump !p0 !n0 + = do (i, p1, n1) <- peekWord16 p0 n0 + return (fromIntegral i, p1, n1) +{-# INLINE peekBump #-} + + +-- | Peek a `Nom` from memory. +peekNom :: Peek Integer +peekNom !p0 !n0 + = do (i, p1, n1) <- peekWord32 p0 n0 + return (fromIntegral i, p1, n1) +{-# INLINE peekNom #-} + + +--------------------------------------------------------------------------------------------------- +-- | Peek a prim from memory. +peekPrim :: Peek Prim +peekPrim !p0 !n0 + | n0 >= 1 + = do (b0, p1, n1) <- peekWord8' p0 n0 + p1 `seq` case b0 of + 0xda -> return (PrimTagUnit, p1, n1) + 0xdb -> return (PrimLitBool True, p1, n1) + 0xdc -> return (PrimLitBool False, p1, n1) + + 0xdf + -> do (tx, p2, n2) <- peekText p1 n1 + return (PrimOp tx, p2, n2) + + 0xef + -> do (tx, p2, n2) <- peekText p1 n1 + case T.unpack tx of + "nat" + -> do (ls, p3, n3) <- peekList peekWord8 p2 n2 + case ls of + [x0, x1, x2, x3, x4, x5, x6, x7] + -> do let w = to64 x0 `shiftL` 56 + .|. to64 x1 `shiftL` 48 + .|. to64 x2 `shiftL` 40 + .|. to64 x3 `shiftL` 32 + .|. to64 x4 `shiftL` 24 + .|. to64 x5 `shiftL` 16 + .|. to64 x6 `shiftL` 8 + .|. to64 x7 + return (PrimLitNat $ fromIntegral w, p3, n3) + _ -> error "peekPrim: invalid payload" + + s -> error $ "peekPrim: unknown tag " ++ show s + + _ -> error $ "peekPrim: invalid header" + + | otherwise + = error "peekPrim: invalid header" +{-# INLINE peekPrim #-} + + +--------------------------------------------------------------------------------------------------- +-- | Peek a list of things from memory. +peekList :: Peek a -> Peek [a] +peekList peekA p0 n0 + | n0 >= 1 + = do (b0, _p1, n1) <- peekWord8' p0 n0 + case b0 of + 0xf1 + | n1 >= 1 + -> do nElems <- fmap fromIntegral $ peek8 p0 1 + go nElems [] (F.plusPtr p0 2) (n1 - 1) + + 0xf2 + | n1 >= 2 + -> do nElems <- fmap fromIntegral $ peek16 p0 1 + go nElems [] (F.plusPtr p0 3) (n1 - 2) + + 0xf3 + | n1 >= 4 + -> do nElems <- fmap fromIntegral $ peek32 p0 1 + go nElems [] (F.plusPtr p0 5) (n1 - 4) + + _ -> error "peekList: invalid header" + + | otherwise + = error "peekList: invalid header" + + where go (0 :: Int) acc p n + = return (reverse acc, p, n) + + go i acc p n + = do (x, p', n') <- peekA p n + go (i - 1) (x : acc) p' n' + {-# NOINLINE go #-} + +{-# INLINE peekList #-} + + +--------------------------------------------------------------------------------------------------- +-- | Peek a text value from memory as UTF8 characters. +peekText :: Peek Text +peekText !p0 !n0 + | n0 >= 1 + = do (b0, _, n1) <- peekWord8' p0 n0 + case b0 of + 0xf1 + | n1 >= 1 + -> do nBytes <- fmap fromIntegral $ peek8 p0 1 + buf <- F.mallocBytes nBytes + let p2 = F.plusPtr p0 2 + let n2 = n0 - 2 + when (not (n2 >= nBytes)) $ error "peekText: pointer out of range" + F.copyBytes buf p2 nBytes + bs <- BS.unsafePackMallocCStringLen (buf, nBytes) + return (T.decodeUtf8 bs, F.plusPtr p2 nBytes, n2 - nBytes) + + 0xf2 + -> do nBytes <- fmap fromIntegral $ peek16 p0 1 + buf <- F.mallocBytes nBytes + let p2 = F.plusPtr p0 3 + let n2 = n0 - 3 + when (not (n2 >= nBytes)) $ error "peekText: pointer out of range" + F.copyBytes buf p2 nBytes + bs <- BS.unsafePackMallocCStringLen (buf, nBytes) + return (T.decodeUtf8 bs, F.plusPtr p2 nBytes, n2 - nBytes) + + 0xf3 + -> do nBytes <- fmap fromIntegral $ peek32 p0 1 + buf <- F.mallocBytes nBytes + let p2 = F.plusPtr p0 5 + let n2 = n0 - 5 + when (not (n2 >= nBytes)) $ error "peekText: pointer out of range" + F.copyBytes buf p2 nBytes + bs <- BS.unsafePackMallocCStringLen (buf, nBytes) + return (T.decodeUtf8 bs, F.plusPtr p2 nBytes, n2 - nBytes) + + _ -> error $ "peekText: invalid header" + + | otherwise + = error "peekText: pointer out of range" +{-# NOINLINE peekText #-} + +--------------------------------------------------------------------------------------------------- +-- | Peek a `Word8` from memory, in network byte order, with bounds check. +peekWord8 :: Peek Word8 +peekWord8 p n + | n >= 1 = peekWord8' p n + | otherwise = error "peekWord8: pointer out of bounds" +{-# NOINLINE peekWord8 #-} + + +-- | Peek a `Word8` from memory, in network byte order, with no bounds check. +peekWord8' :: Peek Word8 +peekWord8' p n + = do w <- F.peek p + return (w, F.plusPtr p 1, n - 1) +{-# INLINE peekWord8' #-} + + +-- | Peek a `Word16` from memory, in network byte order, with bounds check. +peekWord16 :: Peek Word16 +peekWord16 p n + | n >= 2 = peekWord16' p n + | otherwise = error "peekWord16: pointer out of bounds" +{-# NOINLINE peekWord16 #-} + + +-- | Peek a `Word16` from memory, in network byte order, with no bound check. +peekWord16' :: Peek Word16 +peekWord16' p n + = do b0 <- fmap to16 $ peek8 p 0 + b1 <- fmap to16 $ peek8 p 1 + let w = b0 `shiftL` 8 + .|. b1 + return (w, F.plusPtr p 2, n - 2) +{-# INLINE peekWord16' #-} + + +-- | Peek a `Word32` from memory, in network byte order, with bounds check. +peekWord32 :: Peek Word32 +peekWord32 p n + | n >= 4 = peekWord32' p n + | otherwise = error "peekWord32: pointer out of bounds" +{-# NOINLINE peekWord32 #-} + + +-- | Peek a `Word32` from memory, in network byte order, with no bounds check. +peekWord32' :: Peek Word32 +peekWord32' p n + = do b0 <- fmap to32 $ peek8 p 0 + b1 <- fmap to32 $ peek8 p 1 + b2 <- fmap to32 $ peek8 p 2 + b3 <- fmap to32 $ peek8 p 3 + let w = b0 `shiftL` 24 + .|. b1 `shiftL` 16 + .|. b2 `shiftL` 8 + .|. b3 + return (w, F.plusPtr p 4, n - 4) +{-# INLINE peekWord32' #-} + + +-- | Peek a `Word64` from memory, in network byte order, with bounds check. +peekWord64 :: Peek Word64 +peekWord64 p n + | n >= 8 = peekWord64' p n + | otherwise = error "peekWord64: pointer out of bounds" +{-# NOINLINE peekWord64 #-} + + +-- | Peek a `Word64` from memory, in network byte order, in network byte order. +peekWord64' :: Peek Word64 +peekWord64' p n + = do b0 <- fmap to64 $ peek8 p 0 + b1 <- fmap to64 $ peek8 p 1 + b2 <- fmap to64 $ peek8 p 2 + b3 <- fmap to64 $ peek8 p 3 + b4 <- fmap to64 $ peek8 p 4 + b5 <- fmap to64 $ peek8 p 5 + b6 <- fmap to64 $ peek8 p 6 + b7 <- fmap to64 $ peek8 p 7 + let w = b0 `shiftL` 56 + .|. b1 `shiftL` 48 + .|. b2 `shiftL` 40 + .|. b3 `shiftL` 32 + .|. b4 `shiftL` 24 + .|. b5 `shiftL` 16 + .|. b6 `shiftL` 8 + .|. b7 + return (w, F.plusPtr p 8, n - 8) +{-# INLINE peekWord64' #-} + + +to16 :: Word8 -> Word16 +to16 = fromIntegral +{-# INLINE to16 #-} + + +to64 :: Word8 -> Word64 +to64 = fromIntegral +{-# INLINE to64 #-} + + +to32 :: Word8 -> Word32 +to32 = fromIntegral +{-# INLINE to32 #-} + + +peek8 :: Ptr a -> Int -> IO Word8 +peek8 p o = F.peekByteOff p o +{-# INLINE peek8 #-} + + +peek16 :: Ptr a -> Int -> IO Word16 +peek16 p o = F.peekByteOff p o +{-# INLINE peek16 #-} + + +peek32 :: Ptr a -> Int -> IO Word32 +peek32 p o = F.peekByteOff p o +{-# INLINE peek32 #-} + diff --git a/src/SMR/Codec/Poke.hs b/src/SMR/Codec/Poke.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Codec/Poke.hs @@ -0,0 +1,324 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DoAndIfThenElse #-} +module SMR.Codec.Poke + ( pokeFileDecls + , pokeDecl + , pokeExp, pokeKey, pokeParam + , pokeCar, pokeSnvBind, pokeUpsBump + , pokeRef + , pokeName, pokeBump, pokeNom + , pokeWord8, pokeWord16, pokeWord32, pokeWord64) +where +import SMR.Core.Exp +import SMR.Prim.Op.Base + +import qualified Foreign.Marshal.Utils as F +import qualified Foreign.Storable as F +import qualified Foreign.Ptr as F + +import qualified Data.Text as T +import qualified Data.Text.Encoding as T +import qualified Data.ByteString.Unsafe as BS + +import Data.Text (Text) +import Foreign.Ptr (Ptr) +import Control.Monad +import Data.Bits +import Data.Word + + +--------------------------------------------------------------------------------------------------- +type Poke a = a -> Ptr Word8 -> IO (Ptr Word8) + + +--------------------------------------------------------------------------------------------------- +-- | Poke a list of `Decl` into memory, including the SMR file header. +pokeFileDecls :: Poke [Decl Text Prim] +pokeFileDecls ds + = pokeWord8 0x53 -- 'S' + >=> pokeWord8 0x4d -- 'M' + >=> pokeWord8 0x52 -- 'R' + >=> pokeWord8 0x31 -- '1' + >=> pokeList pokeDecl ds +{-# NOINLINE pokeFileDecls #-} + + +-- | Poke a `Decl` into memory. +pokeDecl :: Poke (Decl Text Prim) +pokeDecl xx + = case xx of + DeclMac name x + -> pokeWord8 0xa1 >=> pokeText name >=> pokeExp x + + DeclSet name x + -> pokeWord8 0xa2 >=> pokeText name >=> pokeExp x +{-# NOINLINE pokeDecl #-} + + +--------------------------------------------------------------------------------------------------- +-- | Poke an `Exp` into memory. +pokeExp :: Poke (Exp Text Prim) +pokeExp xx + = case xx of + XRef ref + -> pokeWord8 0xb1 >=> pokeRef ref + + XKey key x + -> pokeWord8 0xb2 >=> pokeKey key >=> pokeExp x + + XApp x1 xs + -> pokeWord8 0xb3 >=> pokeExp x1 >=> pokeList pokeExp xs + + XVar name i + -> pokeWord8 0xb4 >=> pokeName name >=> pokeBump i + + XAbs ps x + -> pokeWord8 0xb5 >=> pokeList pokeParam ps >=> pokeExp x + + XSub cs x + -> pokeWord8 0xb6 >=> pokeList pokeCar cs >=> pokeExp x +{-# NOINLINE pokeExp #-} + + +-- | Poke a `Key` into memory. +pokeKey :: Poke Key +pokeKey key + = case key of + KBox -> pokeWord8 0xba + KRun -> pokeWord8 0xbb +{-# INLINE pokeKey #-} + + +-- | Poke a `Param` into memory. +pokeParam :: Poke Param +pokeParam pp + = case pp of + PParam tx PVal + -> pokeWord8 0xbc >=> pokeName tx + + PParam tx PExp + -> pokeWord8 0xbd >=> pokeName tx +{-# INLINE pokeParam #-} + + +-- | Poke a `Car` into memory. +pokeCar :: Poke (Car Text Prim) +pokeCar car + = case car of + CSim (SSnv sbs) + -> pokeWord8 0xc1 >=> pokeList pokeSnvBind sbs + + CRec (SSnv sbs) + -> pokeWord8 0xc2 >=> pokeList pokeSnvBind sbs + + CUps (UUps ups) + -> pokeWord8 0xc3 >=> pokeList pokeUpsBump ups +{-# INLINE pokeCar #-} + + +-- | Poke an `SnvBind` into memory. +pokeSnvBind :: Poke (SnvBind Text Prim) +pokeSnvBind !b + = case b of + BindVar n d x + -> pokeWord8 0xca >=> pokeName n >=> pokeBump d >=> pokeExp x + + BindNom n x + -> pokeWord8 0xcb >=> pokeNom n >=> pokeExp x +{-# INLINE pokeSnvBind #-} + + +-- | Poke an `UpsBump` into memory. +pokeUpsBump :: Poke UpsBump +pokeUpsBump ((n, d), i) + = pokeWord8 0xcc >=> pokeName n >=> pokeBump d >=> pokeBump i +{-# INLINE pokeUpsBump #-} + + +--------------------------------------------------------------------------------------------------- +-- | Poke a `Ref` into memory. +pokeRef :: Poke (Ref Text Prim) +pokeRef !r + = case r of + RSym tx -> pokeWord8 0xd1 >=> pokeName tx + RPrm p -> pokeWord8 0xd2 >=> pokePrim p + RMac tx -> pokeWord8 0xd3 >=> pokeName tx + RSet tx -> pokeWord8 0xd4 >=> pokeName tx + RNom i -> pokeWord8 0xd5 >=> pokeNom i +{-# INLINE pokeRef #-} + + +--------------------------------------------------------------------------------------------------- +-- | Peek a `Name` from memory. +pokeName :: Poke Name +pokeName !p n + = pokeText p n +{-# INLINE pokeName #-} + + +-- | Poke a `Bump` into memory. +pokeBump :: Poke Integer +pokeBump !n !p + = if n <= 2^(16 :: Int) then + do pokeWord16 (fromIntegral n) p + else error "shimmer.pokeBump: bump counter too large." +{-# NOINLINE pokeBump #-} + + +-- | Poke a `Nom` into memory. +pokeNom :: Poke Integer +pokeNom !n !p + = if n <= 2^(28 :: Int) then + do pokeWord32 (fromIntegral n) p + else error "shimmer.pokeNom: nominal constant index too large." +{-# NOINLINE pokeNom #-} + + +--------------------------------------------------------------------------------------------------- +-- | Poke a prim into memory. +pokePrim :: Poke Prim +pokePrim !pp + = case pp of + PrimTagUnit -> pokeWord8 0xda + PrimLitBool True -> pokeWord8 0xdb + PrimLitBool False -> pokeWord8 0xdc + PrimOp tx -> pokeWord8 0xdf >=> pokeText tx + + -- Integers are currently squashed into Word64s. + PrimLitNat n + -> pokeWord8 0xef + >=> pokeName (T.pack "nat") + >=> pokeList pokeWord8 + [ fromIntegral $ (n .&. 0xff00000000000000) `shiftR` 56 + , fromIntegral $ (n .&. 0x00ff000000000000) `shiftR` 48 + , fromIntegral $ (n .&. 0x0000ff0000000000) `shiftR` 40 + , fromIntegral $ (n .&. 0x000000ff00000000) `shiftR` 32 + , fromIntegral $ (n .&. 0x00000000ff000000) `shiftR` 24 + , fromIntegral $ (n .&. 0x0000000000ff0000) `shiftR` 16 + , fromIntegral $ (n .&. 0x000000000000ff00) `shiftR` 8 + , fromIntegral $ (n .&. 0x00000000000000ff)] + + PrimTagList{} -> error "TODO: pokePrim: handle lists" +{-# INLINE pokePrim #-} + + +--------------------------------------------------------------------------------------------------- +-- | Poke a list of things into memory, including size info. +pokeList :: Poke a -> Poke [a] +pokeList pokeA ls + = do let n = length ls + if n <= 2^(8 :: Int) - 1 + then pokeWord8 0xf1 >=> pokeWord8 (fromIntegral n) >=> go ls + + else if n <= 2^(16 :: Int) - 1 + then pokeWord8 0xf2 >=> pokeWord16 (fromIntegral n) >=> go ls + + else if n <= 2^(28 :: Int) + then pokeWord8 0xf2 >=> pokeWord32 (fromIntegral n) >=> go ls + + else error "shimmer.pokeList: list too long." + + where go [] !p0 = return p0 + go (x : xs) !p0 + = do p1 <- pokeA x p0 + go xs p1 + {-# NOINLINE go #-} + +{-# INLINE pokeList #-} + + +--------------------------------------------------------------------------------------------------- +-- | Poke a text value into memory as UTF8 characters. +pokeText :: Poke Text +pokeText !tx !p0 + = do let bs = T.encodeUtf8 tx + + BS.unsafeUseAsCStringLen bs $ \(pStr, nBytes) + -> if nBytes <= 255 then + do p1 <- pokeWord8 0xf1 p0 + p2 <- pokeWord8 (fromIntegral nBytes) p1 + F.copyBytes (F.castPtr p2) pStr nBytes + return (F.plusPtr p2 nBytes) + + else if nBytes <= 65535 then + do p1 <- pokeWord8 0xf2 p0 + p2 <- pokeWord16 (fromIntegral nBytes) p1 + F.copyBytes (F.castPtr p2) pStr nBytes + return (F.plusPtr p2 nBytes) + + -- The Haskell Int type is only guaranteed to have at least 29 + -- bits of precision. We just limit the string size to 2^28, + -- as 256MB should be enough for any sort of program text. + else if nBytes <= 2^(28 :: Int) then + do p1 <- pokeWord8 0xf3 p0 + p2 <- pokeWord32 (fromIntegral nBytes) p1 + F.copyBytes (F.castPtr p2) pStr nBytes + return (F.plusPtr p2 nBytes) + + else error "shimmer.pokeText: text string too large." +{-# NOINLINE pokeText #-} + + +--------------------------------------------------------------------------------------------------- +-- | Poke a `Word8` into memory. +pokeWord8 :: Poke Word8 +pokeWord8 w p + = do F.poke p w + return (F.plusPtr p 1) +{-# INLINE pokeWord8 #-} + + +-- | Poke a `Word16` into memory, in network byte order. +pokeWord16 :: Poke Word16 +pokeWord16 w p + = do poke8 p 0 $ from16 $ (w .&. 0xff00) `shiftR` 8 + poke8 p 1 $ from16 $ (w .&. 0x00ff) + return (F.plusPtr p 2) +{-# INLINE pokeWord16 #-} + + +-- | Poke a `Word32` into memory, in network byte order. +pokeWord32 :: Poke Word32 +pokeWord32 w p + = do poke8 p 0 $ from32 $ (w .&. 0xff000000) `shiftR` 24 + poke8 p 1 $ from32 $ (w .&. 0x00ff0000) `shiftR` 16 + poke8 p 2 $ from32 $ (w .&. 0x0000ff00) `shiftR` 8 + poke8 p 3 $ from32 $ (w .&. 0x000000ff) + return (F.plusPtr p 4) +{-# INLINE pokeWord32 #-} + + +-- | Poke a `Word64` into memory, in network byte order. +pokeWord64 :: Poke Word64 +pokeWord64 w p + = do poke8 p 0 $ from64 $ (w .&. 0xff00000000000000) `shiftR` 56 + poke8 p 1 $ from64 $ (w .&. 0x00ff000000000000) `shiftR` 48 + poke8 p 2 $ from64 $ (w .&. 0x0000ff0000000000) `shiftR` 40 + poke8 p 3 $ from64 $ (w .&. 0x000000ff00000000) `shiftR` 32 + poke8 p 4 $ from64 $ (w .&. 0x00000000ff000000) `shiftR` 24 + poke8 p 5 $ from64 $ (w .&. 0x0000000000ff0000) `shiftR` 16 + poke8 p 6 $ from64 $ (w .&. 0x000000000000ff00) `shiftR` 8 + poke8 p 7 $ from64 $ (w .&. 0x00000000000000ff) + return (F.plusPtr p 8) +{-# INLINE pokeWord64 #-} + + +from16 :: Word16 -> Word8 +from16 = fromIntegral +{-# INLINE from16 #-} + + +from32 :: Word32 -> Word8 +from32 = fromIntegral +{-# INLINE from32 #-} + + +from64 :: Word64 -> Word8 +from64 = fromIntegral +{-# INLINE from64 #-} + + +poke8 :: Ptr a -> Int -> Word8 -> IO () +poke8 p i w = F.pokeByteOff p i w +{-# INLINE poke8 #-} + diff --git a/src/SMR/Codec/Size.hs b/src/SMR/Codec/Size.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Codec/Size.hs @@ -0,0 +1,132 @@ + +module SMR.Codec.Size + ( sizeOfSeq + , sizeOfFile, sizeOfDecl + , sizeOfRef + , sizeOfExp, sizeOfParam + , sizeOfCar, sizeOfSnvBind, sizeOfUpsBump + , sizeOfName, sizeOfBump, sizeOfNom) +where +import SMR.Core.Exp +import SMR.Prim.Op.Base +import qualified Data.Text.Foreign as T +import qualified Data.Text as T + + +--------------------------------------------------------------------------------------------------- +-- | Compute the size of a serialized shimmer file containing the given decls. +sizeOfFile :: [Decl Text Prim] -> Int +sizeOfFile decls + = 4 + sizeOfSeq sizeOfDecl decls + + +-- | Compute the serialized size of a given declaration. +sizeOfDecl :: Decl Text Prim -> Int +sizeOfDecl dd + = case dd of + DeclMac n x -> 1 + sizeOfName n + sizeOfExp x + DeclSet n x -> 1 + sizeOfName n + sizeOfExp x + + +--------------------------------------------------------------------------------------------------- +-- | Compute the serialized size of the given expression. +sizeOfExp :: Exp Text Prim -> Int +sizeOfExp xx + = case xx of + XRef ref -> 1 + sizeOfRef ref + XKey _key x -> 2 + sizeOfExp x + XApp x1 xs -> 1 + sizeOfExp x1 + sizeOfSeq sizeOfExp xs + XVar n b -> 1 + sizeOfName n + sizeOfBump b + XAbs ps x -> 1 + sizeOfSeq sizeOfParam ps + sizeOfExp x + XSub cs x -> 1 + sizeOfSeq sizeOfCar cs + sizeOfExp x + + +-- | Compute the serialized size of a parameter. +sizeOfParam :: Param -> Int +sizeOfParam (PParam n _form) + = 1 + sizeOfName n + + +-- | Compute the serialized size of a substitution car. +sizeOfCar :: Car Text Prim -> Int +sizeOfCar cc + = case cc of + CSim (SSnv snv) -> 1 + sizeOfSeq sizeOfSnvBind snv + CRec (SSnv snv) -> 1 + sizeOfSeq sizeOfSnvBind snv + CUps (UUps ups) -> 1 + sizeOfSeq sizeOfUpsBump ups + + +-- | Compute the serialized size of a substitution bind. +sizeOfSnvBind :: SnvBind Text Prim -> Int +sizeOfSnvBind sb + = case sb of + BindVar n i x -> 1 + sizeOfName n + sizeOfBump i + sizeOfExp x + BindNom i x -> 1 + sizeOfBump i + sizeOfExp x + + +-- | Compute the serialized size of an lifting bump. +sizeOfUpsBump :: UpsBump -> Int +sizeOfUpsBump ub + = case ub of + ((n, d), i) -> 1 + sizeOfName n + sizeOfBump d + sizeOfBump i + + +--------------------------------------------------------------------------------------------------- +-- | Compute the serialized size of the given reference. +sizeOfRef :: Ref Text Prim -> Int +sizeOfRef rr + = case rr of + RSym n -> 1 + sizeOfName n + RPrm p -> 1 + sizeOfPrim p + RMac n -> 1 + sizeOfName n + RSet n -> 1 + sizeOfName n + RNom n -> 1 + sizeOfNom n + + +sizeOfPrim :: Prim -> Int +sizeOfPrim pp + = case pp of + PrimTagUnit -> 1 + PrimLitBool _ -> 1 + PrimOp tx -> 1 + sizeOfName tx + + PrimLitNat _ -> 1 + sizeOfName (T.pack "nat") + + sizeOfSeq (const 1) (replicate (8 :: Int) (0 :: Int)) + + _ -> error "TODO: handle lists" + + +--------------------------------------------------------------------------------------------------- +-- | Compute the serialized size of a text string. +sizeOfName :: Text -> Int +sizeOfName tt + = result + where n = T.lengthWord16 tt + result + | n < 2^(8 :: Int) = 1 + 1 + n + | n < 2^(16 :: Int) = 1 + 2 + n + | n < 2^(32 :: Int) = 1 + 4 + n + | otherwise = error "shimmer.sizeOfName: name too long to serialize." + + +-- | Compute the serialized size of a bump bounter. +sizeOfBump :: Integer -> Int +sizeOfBump _ = 2 + + +-- | Compute the serialized size of a nominal atom. +sizeOfNom :: Integer -> Int +sizeOfNom _ = 4 + + +-- | Compute the serialized size of a sequence of things. +sizeOfSeq :: (a -> Int) -> [a] -> Int +sizeOfSeq fs xs + = result + where n = length xs + result + | n < 2^(8 :: Int) = 1 + 1 + sum (map fs xs) + | n < 2^(16 :: Int) = 1 + 2 + sum (map fs xs) + | n < 2^(32 :: Int) = 1 + 4 + sum (map fs xs) + | otherwise = error "shimmer.sizeOfSeq: sequence too long to serialize." + diff --git a/src/SMR/Core/Exp.hs b/src/SMR/Core/Exp.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Core/Exp.hs @@ -0,0 +1,38 @@ + +module SMR.Core.Exp + ( -- * Abstract Syntax + Decl (..) + , Exp (..) + , Param (..) + , Form (..) + , Key (..) + , Train + , Car (..) + , Snv (..), SnvBind(..) + , Ups (..), UpsBump + , Ref (..) + , Name, Nom, Depth, Bump + , Text + + -- * Compounds + , makeXApps, takeXApps + , makeXAbs + , nameOfParam, formOfParam + + -- * Substitution Trains + , trainCons + , trainAppend + , trainApply + , snvApply + , snvOfNamesArgs + + -- * Substitution Pushing + , pushHead + , pushDeep) +where +import SMR.Core.Exp.Base +import SMR.Core.Exp.Compounds +import SMR.Core.Exp.Train +import SMR.Core.Exp.Push +import Data.Text (Text) + diff --git a/src/SMR/Core/Exp/Base.hs b/src/SMR/Core/Exp/Base.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Core/Exp/Base.hs @@ -0,0 +1,143 @@ +{-# LANGUAGE BangPatterns #-} +-- | The Shimmer Abstract Syntax Tree (AST) +module SMR.Core.Exp.Base where +import Data.Text (Text) + + +-- | Top-level declaration, +-- parameterised by the types of symbols and primitives. +data Decl s p + = DeclMac Name (Exp s p) + | DeclSet Name (Exp s p) + deriving Show + + +-- | Expression, +-- parameterised by the types of symbols and primitives +data Exp s p + -- | Reference to an external thing. + = XRef !(Ref s p) + + -- | Keyed expressions. + | XKey !Key !(Exp s p) + + -- | Application of a function expression to an argument. + | XApp !(Exp s p) ![Exp s p] + + -- | Variable name with a depth counter. + | XVar !Name !Depth + + -- | Abstraction with a list of parameters and a body expression. + | XAbs ![Param] !(Exp s p) + + -- | Substitution train applied to an expression. + -- The train car at the head of the list is applied first. + | XSub !(Train s p) !(Exp s p) + deriving Show + + +-- | Substitution train. +type Train s p + = [Car s p] + + +-- | Function parameter. +data Param + = PParam !Name !Form + deriving Show + + +-- | Form of argument required in application. +data Form + -- | Value for call-by-value. + = PVal + + -- | Expression for call-by-name + | PExp + deriving Show + + +-- | Expression keys (super primitives) +data Key + -- | Delay evaluation of an expression used as the argument + -- of a call-by-value function application. + = KBox + + -- | Run a boxed expression. + | KRun + + deriving Show + + +-- | A car on the substitution train, +-- parameterised by the types used for symbols and primitives. +data Car s p + -- | Simultaneous subsitution. + = CSim !(Snv s p) + + -- | Recursive substitution. + | CRec !(Snv s p) + + -- | Lifting. + | CUps !Ups + deriving Show + + +-- | Explicit substitution map, +-- parameterised by the types used for symbols and primitives. +data Snv s p + = SSnv ![SnvBind s p] + deriving Show + +data SnvBind s p + = BindVar !Name !Depth !(Exp s p) + | BindNom !Nom !(Exp s p) + deriving Show + + +-- | Lifting indicator, +-- mapping name and binding depth to number of levels to lift. +data Ups + = UUps ![UpsBump] + deriving Show + + +-- | Indicates how to bump the index on a variable. +type UpsBump + = ((Name, Depth), Bump) + + +-- | Binding depth indicator. +type Depth = Integer + + +-- | Bump index indicator. +type Bump = Integer + + +-- | A reference to some external thing. +data Ref s p + -- | An uninterpreted symbol. + = RSym !s + + -- | A primitive value. + | RPrm !p + + -- | A macro name. + | RMac !Name + + -- | A set name. + | RSet !Name + + -- | A nominal variable. + | RNom !Nom + deriving Show + + +-- | Generic names for things. +type Name = Text + + +-- | Index of a nominal constant. +type Nom = Integer + diff --git a/src/SMR/Core/Exp/Compounds.hs b/src/SMR/Core/Exp/Compounds.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Core/Exp/Compounds.hs @@ -0,0 +1,50 @@ + +module SMR.Core.Exp.Compounds where +import SMR.Core.Exp.Base + + +-- Apps ----------------------------------------------------------------------- +-- | Make an application of a function to the given list of arguments, +-- suppressing the application of there are no arguments. +makeXApps :: Exp s p -> [Exp s p] -> Exp s p +makeXApps xFun [] = xFun +makeXApps xFun xsArgs = XApp xFun xsArgs + + +-- | Take an application of a function to a list of arguments. +-- TODO(BL): fix rubbish list append complexity. +takeXApps :: Exp s p -> Maybe (Exp s p, [Exp s p]) +takeXApps xx + = case xx of + XApp x1@(XApp _ _) x2 + -> case takeXApps x1 of + Just (f1, xs1) -> Just (f1, xs1 ++ x2) + Nothing -> Nothing + + XApp x1 x2 + -> Just (x1, x2) + + _ -> Nothing + + +-- Abs ------------------------------------------------------------------------ +-- | Make an abstraction, +-- short circuiting to the body if there are no parameters. +makeXAbs :: [Param] -> Exp s p -> Exp s p +makeXAbs [] xBody = xBody +makeXAbs ps xBody = XAbs ps xBody + + +-- Param ---------------------------------------------------------------------- +-- | Get the name of a function parameter. +nameOfParam :: Param -> Name +nameOfParam p + = case p of + PParam n _ -> n + + +-- | Get the argument form required by a parameter. +formOfParam :: Param -> Form +formOfParam p + = case p of + PParam _ f -> f diff --git a/src/SMR/Core/Exp/Push.hs b/src/SMR/Core/Exp/Push.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Core/Exp/Push.hs @@ -0,0 +1,104 @@ + +module SMR.Core.Exp.Push where +import SMR.Core.Exp.Train +import SMR.Core.Exp.Compounds +import SMR.Core.Exp.Base + + +-- | Push down any outermost substitution train to reveal the head constructor. +pushHead :: Exp s p -> Maybe (Exp s p) +pushHead xx + = case xx of + XRef _ -> Nothing + XVar _ _ -> Nothing + XAbs _ _ -> Nothing + XApp _ _ -> Nothing + XSub cs2 x2 -> pushTrain cs2 x2 + XKey _ _ -> Nothing + + +-- | Push down the left-most substitution train in an expression, +-- or 'Nothing' if there isn't one. +pushDeep :: Exp s p -> Maybe (Exp s p) +pushDeep xx + = case xx of + XRef _ -> Nothing + XVar _ _ -> Nothing + + XKey k1 x2 + | Just x2' <- pushDeep x2 + -> Just $ XKey k1 x2' + + | otherwise -> Nothing + + XApp x1 xs2 + | Just x1' <- pushDeep x1 + -> Just $ XApp x1' xs2 + + | Just xs2' <- pushDeepFirst xs2 + -> Just $ XApp x1 xs2' + + | otherwise -> Nothing + + + XAbs ns x + -> case pushDeep x of + Nothing -> Nothing + Just x' -> Just (XAbs ns x') + + XSub cs1 x2 -> pushTrain cs1 x2 + + +-- | Push down the first substiution train in the given list. +pushDeepFirst :: [Exp s p] -> Maybe [Exp s p] +pushDeepFirst [] = Nothing +pushDeepFirst (x : xs) + = case pushDeep x of + Nothing + | Just xs' <- pushDeepFirst xs + -> Just (x : xs') + | otherwise -> Nothing + + Just x' + -> Just (x' : xs) + + +-- | Push a substitution train down into an expression to reveal +-- the head constructor. +pushTrain :: [Car s p] -> Exp s p -> Maybe (Exp s p) +pushTrain cs1 x2 + = case x2 of + -- Unfold macro under a substitution. + -- Macro and symbol bodies are closed, + -- so we can drop the substitution. + XRef (RMac _) -> Just x2 + XRef (RSym _) -> Just x2 + XRef (RPrm _) -> Just x2 + XRef (RNom _) -> Just x2 + + -- Reference to some other thing. + XRef _ -> Nothing + + -- Apply the train to a variable. + XVar name depth + -> Just $ trainApplyVar cs1 name depth + + -- Push train under key. + XKey k21 x22 + -> Just $ XKey k21 (trainApply cs1 x22) + + -- Push train into both sides of an application. + XApp x21 x22 + -> Just $ XApp (trainApply cs1 x21) (map (trainApply cs1) x22) + + -- Push train under abstraction. + XAbs ps21 x22 + -> let ns21 = map nameOfParam ps21 + cs1' = trainBump ns21 cs1 + in Just $ XAbs ps21 (trainApply cs1' x22) + + -- Combine trains. + XSub cs2 x22 + -> Just $ trainApply (cs2 ++ cs1) x22 + + diff --git a/src/SMR/Core/Exp/Train.hs b/src/SMR/Core/Exp/Train.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Core/Exp/Train.hs @@ -0,0 +1,279 @@ +{-# LANGUAGE ParallelListComp #-} +module SMR.Core.Exp.Train where +import SMR.Core.Exp.Base +import Data.Maybe + + +-- Train ---------------------------------------------------------------------- +-- | Cons a car on the front of an existing train. +-- +-- If the new car is empty it will be suppressed. +-- +-- If the new car can be combined with the first car on the existing +-- train then it will be combined. +-- +trainCons :: Car s p -> [Car s p] -> [Car s p] +trainCons c1 cs2 + | carIsEmpty c1 = cs2 + | otherwise + = case cs2 of + [] + -> c1 : [] + + c2 : cs2' + | CUps ups1 <- c1 + , CUps ups2 <- c2 + -> CUps (upsCombine ups1 ups2) : cs2' + + | otherwise + -> c1 : cs2 + + +-- | Append two trains. +trainAppend :: [Car s p] -> [Car s p] -> [Car s p] +trainAppend ccA ccB + = case ccA of + [] -> ccB + cA : csA -> trainAppend' cA csA ccB + where + trainAppend' c1 cs1 cc2 + = case cs1 of + -- Combine the state with the first car on the second train. + [] + -> trainCons c1 cc2 + + -- Walk over the first train, combining ups's as we go. + c1' : cs1' + | CUps ups1 <- c1 + , CUps ups1' <- c1' + -> trainAppend' (CUps (upsCombine ups1 ups1')) cs1' cc2 + + | otherwise + -> c1 : (trainAppend' c1' cs1' cc2) + + +-- | Bump a train due to pushing it under an abstraction with the +-- given parameter names. +trainBump :: [Name] -> [Car s p] -> [Car s p] +trainBump ns cs + = case cs of + [] -> [] + + CSim snv : cs' + -> trainCons (CSim (snvBump ns snv)) $ trainBump ns cs' + + CRec snv : cs' + -> trainCons (CRec (snvBump ns snv)) $ trainBump ns cs' + + CUps ups : cs' + -> trainCons (CUps (upsBump ns ups)) $ trainBump ns cs' + + +-- | Wrap an expression in a substitution train. +-- If the expression is a plain +trainApply :: [Car s p] -> Exp s p -> Exp s p +trainApply cs1 xx + | [] <- cs1 + = xx + + | otherwise + = case xx of + XRef (RMac _) -> xx + XRef (RSym _) -> xx + XRef (RPrm _) -> xx + XRef (RNom ix) -> trainApplyNom cs1 ix + XVar name depth -> trainApplyVar cs1 name depth + XSub cs2 x2 -> trainApply (trainAppend cs2 cs1) x2 + _ -> XSub cs1 xx + + +-- | Apply a train to a named variable of a given name and depth. +trainApplyVar :: [Car s p] -> Name -> Integer -> Exp s p +trainApplyVar cs name depth + = case cs of + [] -> XVar name depth + CSim snv : cs' -> trainApply cs' (snvApplyVar False snv name depth) + CRec snv : cs' -> trainApply cs' (snvApplyVar True snv name depth) + CUps ups : cs' -> trainApply cs' (upsApplyVar ups name depth) + + +-- | Apply a train to a nominal variable of a given index. +trainApplyNom :: [Car s p] -> Integer -> Exp s p +trainApplyNom cs ix + = case cs of + [] -> XRef (RNom ix) + CSim snv : cs' -> trainApply cs' (snvApplyNom False snv ix) + CRec snv : cs' -> trainApply cs' (snvApplyNom True snv ix) + CUps _ups : cs' -> trainApply cs' (XRef (RNom ix)) + + +-- Car ------------------------------------------------------------------------ +-- | Check if a substitution car is empty. +carIsEmpty :: Car s p -> Bool +carIsEmpty c + = case c of + CSim snv -> snvIsEmpty snv + CRec snv -> snvIsEmpty snv + CUps ups -> upsIsEmpty ups + + +-- Snv ------------------------------------------------------------------------ +-- | Build a substitution from lists of names and arguments. +snvOfNamesArgs :: [Name] -> [Exp s p] -> Snv s p +snvOfNamesArgs ns xs + = SSnv [BindVar n 0 x | n <- ns | x <- xs] + + +-- | Check if the given substitution is empty. +snvIsEmpty :: Snv s p -> Bool +snvIsEmpty (SSnv bs) + = case bs of + [] -> True + _ -> False + + +-- | Bump a substitution due to pushing it under an abstraction with +-- the given parameter names. +snvBump :: [Name] -> Snv s p -> Snv s p +snvBump ns (SSnv ts) + = SSnv $ mapMaybe (snvBump1 ns) ts + where + snvBump1 names (BindVar name depth x) + = Just $ BindVar name + (depth + (if elem name names then 1 else 0)) + (upsApply (UUps (map (\name' -> ((name', 0), 1)) names)) x) + + snvBump1 names (BindNom ix x) + = Just $ BindNom ix + (upsApply (UUps (map (\name' -> ((name', 0), 1)) names)) x) + + +-- | Wrap a train consisting of a single simultaneous substitution +-- around an expression. +snvApply :: Bool -> Snv s p -> Exp s p -> Exp s p +snvApply isRec snv@(SSnv bs) xx + = case bs of + [] -> xx + _ | isRec -> trainApply (CRec snv : []) xx + _ -> trainApply (CSim snv : []) xx + + +-- | Apply a substitution to a variable of a given name and depth. +snvApplyVar :: Bool -> Snv s p -> Name -> Integer -> Exp s p +snvApplyVar isRec snv@(SSnv bs) name depth + = case bs of + [] + -> XVar name depth + + BindVar name' depth' x' : bs' + | name == name' + , depth == depth' + -> if isRec then XSub (CRec snv : []) x' + else x' + + | name == name' + , depth > depth' + -> XVar name (depth - 1) + + | otherwise + -> snvApplyVar isRec (SSnv bs') name depth + + BindNom{} : bs' + -> snvApplyVar isRec (SSnv bs') name depth + + +-- | Apply a substitution to a nominal variable of the given index. +snvApplyNom :: Bool -> Snv s p -> Integer -> Exp s p +snvApplyNom isRec snv@(SSnv bs) ix + = case bs of + [] + -> XRef (RNom ix) + + BindVar{} : bs' + -> snvApplyNom isRec (SSnv bs') ix + + BindNom ix' x' : bs' + | ix == ix' + -> if isRec then XSub (CRec snv : []) x' + else x' + + | otherwise + -> snvApplyNom isRec (SSnv bs') ix + + +-- Ups ------------------------------------------------------------------------ +-- | Check if the given ups is empty. +upsIsEmpty :: Ups -> Bool +upsIsEmpty (UUps bs) + = case bs of + [] -> True + _ -> False + + +-- | Wrap an expression in a train consisting of a single ups. +upsApply :: Ups -> Exp s p -> Exp s p +upsApply ups@(UUps us) xx + = case us of + [] -> xx + _ -> trainApply ((CUps ups) : []) xx + + +-- | Apply an ups to a variable. +upsApplyVar :: Ups -> Name -> Integer -> Exp s n +upsApplyVar (UUps bs) name ix + = case bs of + [] + -> XVar name ix + + ((name', depth'), inc') : bs' + | name == name' + , depth' <= ix + -> upsApplyVar (UUps bs') name (ix + inc') + + | otherwise + -> upsApplyVar (UUps bs') name ix + + +-- | Bump ups (substitution lifting) due to pushing it +-- under an absraction with the given named binders. +upsBump :: [Name] -> Ups -> Ups +upsBump ns0 (UUps bs) + = UUps $ mapMaybe (upsBump1 ns0) bs + where + upsBump1 ns l + | ((n, d), inc) <- l + , elem n ns + = Just ((n, d + 1), inc) + + | otherwise + = Just l + + +-- | Combine two lists of ups. +upsCombine :: Ups -> Ups -> Ups +upsCombine (UUps ts1) (UUps ts2) + = UUps (foldr upsCombineBump ts2 ts1) + + +-- | Combine a bump with an existing list of them. +-- Applying the result to an expression will achieve the same result as +-- applying the whole list and then the extra one. +upsCombineBump :: UpsBump -> [UpsBump] -> [UpsBump] +upsCombineBump b bs + | ((name, depth), inc) <- b + = case bs of + -- We cannot combine the new bump with anything else, + -- so add it to the end of the list. + [] + -> [b] + + b'@((name', depth'), inc') : bs' + -- Combine the new bump with an existing one of the same name. + | name == name' + , depth == depth' + -> ((name, depth'), inc + inc') : bs' + + -- Try to combine the new bump with the tail of the list. + | otherwise + -> b' : (upsCombineBump b bs') + diff --git a/src/SMR/Core/Step.hs b/src/SMR/Core/Step.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Core/Step.hs @@ -0,0 +1,349 @@ +{-# LANGUAGE BangPatterns #-} +module SMR.Core.Step + ( Config (..) + , Result (..) + , steps + , step) +where +import SMR.Core.Exp +import SMR.Core.World +import SMR.Prim.Op.Base +import Data.Text (Text) +import Data.Map (Map) +import qualified Data.Map as Map + + +-------------------------------------------------------------------------------- +-- | Evaluation config +data Config s p w + = Config + { -- | Reduce under lambda abstractions. + configUnderLambdas :: !Bool + + -- | Reduce arguments when head is not an abstraction. + , configHeadArgs :: !Bool + + -- | Primitive operator declarations. + , configPrims :: !(Map p (PrimEval s p w)) + + -- | Macro declarations. + , configDeclsMac :: !(Map Name (Exp s p)) } + + +-- | Result of evaluation. +data Result + = ResultDone + | ResultError Text + deriving Show + + +------------------------------------------------------------------------------- +-- | Multi-step reduction to normal form. +steps :: (Ord p, Show p) + => Config s p w + -> World w -> Exp s p + -> IO (Either Text (Exp s p)) + +steps !config !world !xx + = do erx <- step config world xx + case erx of + Left ResultDone -> return $ Right xx + Left (ResultError err) -> return $ Left err + Right xx' -> steps config world xx' + + +------------------------------------------------------------------------------- +-- | Single step reduction. +-- +-- This is a definitional interpreter, intended to be easy to understand +-- and get right, but not fast. Each time we take a step we decend into +-- the AST looking for the next redex, which causes evaluation to have +-- a higher asymptotic complexity than it would with an evaluator that +-- that manages the evaluation context properly. +-- +step :: (Ord p, Show p) + => Config s p w + -> World w -> Exp s p + -> IO (Either Result (Exp s p)) + +step !config !world !xx + = case xx of + -- Reference + XRef ref + -> case ref of + -- Expand macro declarations. + RMac n + -> case Map.lookup n (configDeclsMac config) of + Nothing -> return $ Left ResultDone + Just x -> return $ Right x + + -- Leave other references as-is. + _ -> return $ Left ResultDone + + -- Plain variable, we're done. + XVar{} + -> return $ Left ResultDone + + -- Abstraction. + XAbs ns1 x2 + -- Reduce the body of the abstraction if requested. + | configUnderLambdas config + -> do er2' <- step config world x2 + case er2' of + Left r2 -> return $ Left r2 + Right x2' -> return $ Right $ XAbs ns1 x2' + + -- Otherwise treat abstractions as values. + | otherwise + -> return $ Left ResultDone + + -- Application. + XApp xF [] + -> return $ Right xF + + XApp{} + -- Unzip the application and try to step the functional expression first. + | Just (xF, xsArgs) <- takeXApps xx + -> do erx <- step (config { configUnderLambdas = False }) + world xF + case erx of + -- Functional expression makes progress. + Right xF' + -> return $ Right $ makeXApps xF' xsArgs + + -- Evaluation of functional expression failed. + Left err@(ResultError _) + -> return $ Left err + + -- Functional expression is done. + Left ResultDone + -> case xF of + XRef (RPrm primF) -> stepAppPrm config world primF xsArgs + XAbs nsParam xBody -> stepAppAbs config world nsParam xBody xsArgs + + -- Functional expression is inactive, but optionally + -- continue reducing arguments to eliminate all of + -- the redexes in the expression. + _ | configHeadArgs config + -> do erxArgs <- stepFirstVal config world xsArgs + case erxArgs of + Right xsArgs' -> return $ Right $ makeXApps xF xsArgs' + Left res -> return $ Left res + + | otherwise + -> return $ Left ResultDone + + | otherwise + -> return $ Left ResultDone + + -- Substitution trains. + XSub{} + -> case pushHead xx of + Nothing -> return $ Left ResultDone + Just xx' -> return $ Right xx' + + -- Boxed expressions are already normal forms. + XKey KBox _ + -> return $ Left ResultDone + + -- Run a boxed expression. + XKey KRun x1 + -> do erx <- step (config { configUnderLambdas = False + , configHeadArgs = False }) + world x1 + + case erx of + -- Body makes progress. + Right x1' + -> return $ Right (XKey KRun x1') + + -- Body expression evaluation failed. + Left err@(ResultError _) + -> return $ Left err + + -- If the body expression is a box then unwrap it, + -- otherwise just return the value as-is. + Left ResultDone + -> case x1 of + XKey KBox x11 -> return $ Right x11 + _ -> return $ Right x1 + + +------------------------------------------------------------------------------- +-- | Step an application of a primitive operators to its arguments. +stepAppPrm + :: (Ord p, Show p) + => Config s p w + -> World w -> p -> [Exp s p] + -> IO (Either Result (Exp s p)) + +stepAppPrm !config !world !prim !xsArgs + = case Map.lookup prim (configPrims config) of + Nothing -> return $ Left ResultDone + Just primEval -> stepPrim config world primEval xsArgs + + +------------------------------------------------------------------------------- +-- | Step an application of an abstraction applied to its arguments. +stepAppAbs + :: (Ord p, Show p) + => Config s p w + -> World w -> [Param] -> Exp s p -> [Exp s p] + -> IO (Either Result (Exp s p)) + +stepAppAbs !config !world !psParam !xBody !xsArgs + = do + let arity = length psParam + let args = length xsArgs + let xsArgs_sat = take arity xsArgs + let xsArgs_remain = drop arity xsArgs + let fsParam_sat = map formOfParam psParam + + erxs <- stepFirst config world xsArgs_sat fsParam_sat + case erxs of + -- One of the args makes progress. + Right xsArgs_sat' + -> do let xFun = XAbs psParam xBody + return $ Right + $ makeXApps (makeXApps xFun xsArgs_sat') xsArgs_remain + + -- Stepping one of the arguments failed. + Left err@(ResultError _) + -> return $ Left err + + -- The arguments are all done. + Left ResultDone + -- Saturated application + | args == arity + -> do let nsParam = map nameOfParam psParam + let snv = snvOfNamesArgs nsParam xsArgs + return $ Right + $ snvApply False snv xBody + + -- Under application. + | args < arity + -> do let psParam_sat = take args psParam + let nsParam_sat = map nameOfParam psParam_sat + let psParam_remain = drop args psParam + let snv = snvOfNamesArgs nsParam_sat xsArgs_sat + return $ Right + $ makeXApps + (snvApply False snv $ XAbs psParam_remain xBody) + xsArgs_remain + + -- Over application. + | otherwise + -> do let nsParam = map nameOfParam psParam + let snv = snvOfNamesArgs nsParam xsArgs_sat + return $ Right + $ makeXApps + (snvApply False snv xBody) + xsArgs_remain + + +------------------------------------------------------------------------------- +-- | Step an application of a primitive operator to some arguments. +stepPrim + :: (Ord p, Show p) + => Config s p w + -> World w -> PrimEval s p w -> [Exp s p] + -> IO (Either Result (Exp s p)) + +stepPrim !config !world !pe !xsArgs + | PrimEval _prim _desc csArg eval <- pe + = let + -- Evaluation of arguments is complete. + evalArgs [] [] xsArgsDone + = do mr <- eval world (reverse xsArgsDone) + case mr of + Just xResult -> return $ Right xResult + Nothing -> return $ Left ResultDone + + -- We have more args than the primitive will accept. + evalArgs [] xsArgsRemain xsArgsDone + = do mr <- eval world (reverse xsArgsDone) + case mr of + Just xResult -> return $ Right $ makeXApps xResult xsArgsRemain + Nothing -> return $ Left ResultDone + + -- Evaluate the next argument if needed. + evalArgs (cArg' : csArg') (xArg' : xsArg') xsArgsDone + -- Primitive does not demand a value fo rthis arg. + | PExp <- cArg' + = evalArgs csArg' xsArg' (xArg' : xsArgsDone) + + -- Primtiive demands a value for this arg. + | otherwise + = do erxArg' <- step (config { configUnderLambdas = False + , configHeadArgs = False }) + world xArg' + case erxArg' of + Left err@(ResultError _) + -> return $ Left err + + Left ResultDone + -> evalArgs csArg' xsArg' (xArg' : xsArgsDone) + + Right xArg'' + -> return $ Right + $ makeXApps (XRef (RPrm (primEvalName pe))) + $ (reverse xsArgsDone) ++ (xArg'' : xsArg') + + -- We have less args than the prim will accept, + -- so leave the application as it is. + evalArgs _ [] _xsArgsDone + = return $ Left ResultDone + + in evalArgs csArg xsArgs [] + + +------------------------------------------------------------------------------- +-- | Step the first available expression in a list, +-- reducing them all towards values. +stepFirstVal + :: (Ord p, Show p) + => Config s p w + -> World w -> [Exp s p] + -> IO (Either Result [Exp s p]) + +stepFirstVal !config !world !xx + = stepFirst config world xx (replicate (length xx) PVal) + + +-- | Step the first available expression in a list. +stepFirst + :: (Ord p, Show p) + => Config s p w + -> World w -> [Exp s p] -> [Form] + -> IO (Either Result [Exp s p]) + +stepFirst !config !world !xx !ff + = case (xx, ff) of + ([], _) + -> return $ Left ResultDone + + (_, []) + -> return $ Left ResultDone + + (x1 : xs2, f1 : fs2) + | PExp <- f1 + -> do erx <- stepFirst config world xs2 fs2 + case erx of + Left r -> return $ Left r + Right xs2' -> return $ Right $ x1 : xs2' + + | otherwise + -> do erx1 <- step config world x1 + case erx1 of + Left err@(ResultError{}) + -> return $ Left err + + Left ResultDone + -> do erxs2 <- stepFirst config world xs2 fs2 + case erxs2 of + Left r -> return $ Left r + Right xs2' -> return $ Right $ x1 : xs2' + + Right x1' + -> return $ Right $ x1' : xs2 + diff --git a/src/SMR/Core/World.hs b/src/SMR/Core/World.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Core/World.hs @@ -0,0 +1,22 @@ + +module SMR.Core.World where +import Data.IORef + + +-- | World state for evaluation +data World w + = World + { -- | Generator for nominal variables. + worldNomGen :: !(IORef Integer) + + -- | User state + , worldUser :: w } + + +-- | Initialize a new world. +worldInit :: w -> IO (World w) +worldInit w + = do refNomGen <- newIORef 0 + return $ World + { worldNomGen = refNomGen + , worldUser = w } diff --git a/src/SMR/Data/Bag.hs b/src/SMR/Data/Bag.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Data/Bag.hs @@ -0,0 +1,64 @@ + +module SMR.Data.Bag where +import Prelude hiding (map) +import qualified Data.List as List + + +-- | An unordered collection of things. +-- O(1) to add a single element, a list of elements, or union two bags. +data Bag a + = BagNil + | BagElem a + | BagList [a] + | BagUnion (Bag a) (Bag a) + deriving Show + + +-- | O(1). Construct an empty bag. +nil :: Bag a +nil = BagNil + + +-- | O(1). Construct a bag containing a single element. +singleton :: a -> Bag a +singleton x + = BagElem x + + +-- | O(1). Construct a bag containing a list of elements. +list :: [a] -> Bag a +list xs + = BagList xs + + +-- | O(1). Union two bags. +union :: Bag a -> Bag a -> Bag a +union xs1 xs2 + = BagUnion xs1 xs2 + + +-- | O(n). Convert a bag to a list. +-- The elements come out in some deterministic but arbitrary order, no promises. +toList :: Bag a -> [a] +toList bag + = go [] bag + where + go xs1 BagNil = xs1 + go xs1 (BagElem x) = x : xs1 + go xs1 (BagList xs2) = go_list xs1 xs2 + go xs1 (BagUnion b1 b2) = go (go xs1 b1) b2 + + go_list _ [] = [] + go_list xs1 (x : xs2) = go_list (x : xs1) xs2 + + +-- | Apply a function to all the elements in a bag. +map :: (a -> b) -> Bag a -> Bag b +map f bag + = case bag of + BagNil -> BagNil + BagElem x -> BagElem (f x) + BagList xs -> BagList (List.map f xs) + BagUnion b1 b2 -> BagUnion (map f b1) (map f b2) + + diff --git a/src/SMR/Data/Located.hs b/src/SMR/Data/Located.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Data/Located.hs @@ -0,0 +1,39 @@ + +module SMR.Data.Located where + + +-- | Location in a source file. +data Location + = L Int Int + deriving Show + + +-- | A thing located at the given range in a source file. +data Located a + = LL Location Location a + deriving Show + + +-- | Take the start point of a located thing. +startOfLocated :: Located a -> Location +startOfLocated (LL start _ _) = start + + +-- | Take the end point of a located thing. +endOfLocated :: Located a -> Location +endOfLocated (LL _ end _) = end + + +-- | Take the value of a located thing. +valueOfLocated :: Located a -> a +valueOfLocated (LL _ _ x) = x + +-- | Increment the character position of a located thing. +incCharOfLocation :: Int -> Location -> Location +incCharOfLocation n (L l c) = L l (c + n) + + +-- | Increment the line position of a located thing. +incLineOfLocation :: Int -> Location -> Location +incLineOfLocation n (L l _) = L (l + n) 1 + diff --git a/src/SMR/Prim/Name.hs b/src/SMR/Prim/Name.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Prim/Name.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE OverloadedStrings #-} +module SMR.Prim.Name where +import SMR.Prim.Op.Base +import Data.Text (Text) +import Data.Set (Set) +import qualified Data.Set as Set +import qualified Data.Char as Char +import qualified Data.Text as Text + + +-- | Pretty print a primitive operator. +pprPrim :: Prim -> Text +pprPrim pp + = case pp of + PrimOp op -> op + + PrimLitBool True -> "true" + PrimLitBool False -> "false" + + PrimLitNat n -> Text.pack $ "nat'" ++ show n + + PrimTagUnit -> "unit" + PrimTagList -> "list" + + +-- | Parse a primitive name, without the leading '#'. +readPrim :: Set Text -> Text -> Maybe Prim +readPrim ps tx + -- Literal Booleans. + | tx == "true" = Just $ PrimLitBool True + | tx == "false" = Just $ PrimLitBool False + + -- Literal Nats. + | Text.isPrefixOf "nat'" tx + , tx' <- Text.unpack $ Text.drop 4 tx + , all Char.isDigit tx' + , not $ null tx' + = Just $ PrimLitNat (read tx') + + -- Other primtiives. + | Set.member tx ps + = Just $ PrimOp tx + + | tx == "unit" = Just PrimTagUnit + | tx == "list" = Just PrimTagList + + -- Unrecognised. + | otherwise + = Nothing diff --git a/src/SMR/Prim/Op.hs b/src/SMR/Prim/Op.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Prim/Op.hs @@ -0,0 +1,27 @@ +module SMR.Prim.Op where +import SMR.Prim.Op.Base +import SMR.Prim.Op.Bool +import SMR.Prim.Op.Nat +import SMR.Prim.Op.Sym +import SMR.Prim.Op.Nom +import SMR.Prim.Op.List +import SMR.Prim.Op.Match +import Data.Text (Text) +import Data.Set (Set) +import qualified Data.Set as Set + + +primEvals :: [PrimEval Text Prim w] +primEvals + = concat + [ primOpsBool + , primOpsNat + , primOpsList + , primOpsSym + , primOpsNom + , primOpsMatch ] + + +primOpTextNames :: Set Text +primOpTextNames + = Set.fromList [ n | PrimOp n <- map primEvalName $ primEvals ] diff --git a/src/SMR/Prim/Op/Base.hs b/src/SMR/Prim/Op/Base.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Prim/Op/Base.hs @@ -0,0 +1,113 @@ + +module SMR.Prim.Op.Base + ( Prim (..) + , PrimEval (..) + + -- * Exp + , takeArgExp + + -- * Bool + , makeXBool, takeXBool, takeArgBool + + -- * Nat + , makeXNat, takeXNat, takeArgNat + + -- * List + , makeXList) +where +import SMR.Core.Exp +import SMR.Core.World +import Data.Text (Text) + + +------------------------------------------------------------------------------- +-- | Primitive values and operators. +data Prim + = PrimOp Text + | PrimLitBool Bool + | PrimLitNat Integer + | PrimTagUnit + | PrimTagList + deriving (Eq, Ord, Show) + + +-- Exp ---------------------------------------------------- +-- | Take the first expression argument from a list of primitives. +takeArgExp + :: [Exp s Prim] + -> Maybe (Exp s Prim, [Exp s Prim]) +takeArgExp xx + = case xx of + x1 : xs -> Just (x1, xs) + _ -> Nothing + + +-- Bool --------------------------------------------------- +-- | Take a literal Bool from an expression. +takeXBool :: Exp s Prim -> Maybe Bool +takeXBool xx + = case xx of + XRef (RPrm (PrimLitBool b)) -> Just b + _ -> Nothing + + +-- | Make a literal Bool expression. +makeXBool :: Bool -> Exp s Prim +makeXBool b + = XRef (RPrm (PrimLitBool b)) + + +-- | Split a literal Bool from an argument list. +takeArgBool :: [Exp s Prim] -> Maybe (Bool, [Exp s Prim]) +takeArgBool xx + = case xx of + XRef (RPrm (PrimLitBool b)) : xs + -> Just (b, xs) + _ -> Nothing + + +-- Nat ---------------------------------------------------- +-- | Take a literal Nat from an expression. +takeXNat :: Exp s Prim -> Maybe Integer +takeXNat xx + = case xx of + XRef (RPrm (PrimLitNat n)) -> Just n + _ -> Nothing + +-- | Make a literal Nat expression. +makeXNat :: Integer -> Exp s Prim +makeXNat n + = XRef (RPrm (PrimLitNat n)) + + +-- | Split a literal Nat from an argument list. +takeArgNat :: [Exp s Prim] -> Maybe (Integer, [Exp s Prim]) +takeArgNat xx + = case xx of + XRef (RPrm (PrimLitNat n)) : xs + -> Just (n, xs) + _ -> Nothing + + +-- List --------------------------------------------------- +-- | Make a list of expressions. +makeXList :: [Exp s Prim] -> Exp s Prim +makeXList xs + = XApp (XRef (RPrm PrimTagList)) xs + + +------------------------------------------------------------------------------- +-- | Primitive evaluator. +data PrimEval s p w + = PrimEval + { primEvalName :: p -- ^ Op name. + , primEvalDesc :: Text -- ^ Op description. + , primEvalForm :: [Form] -- ^ Argument passing methods. + + -- | Evaluation function. + , primEvalFun + :: World w + -> [Exp s p] + -> IO (Maybe (Exp s p)) + } + diff --git a/src/SMR/Prim/Op/Bool.hs b/src/SMR/Prim/Op/Bool.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Prim/Op/Bool.hs @@ -0,0 +1,66 @@ +{-# LANGUAGE OverloadedStrings #-} +module SMR.Prim.Op.Bool where +import SMR.Core.Exp +import SMR.Prim.Op.Base +import Data.Text (Text) + + +-- | Primitive evaluators for boolean operators. +primOpsBool :: [PrimEval s Prim w] +primOpsBool + = [ primOpBool1 "not" "boolean negation" (\b -> not b) + , primOpBool2 "and" "boolean and" (&&) + , primOpBool2 "or" "boolean or" (||) + , primOpIf ] + + +-- | Construct an evaluator for 1-arity bool operator. +primOpBool1 + :: Name -> Text + -> (Bool -> Bool) + -> PrimEval s Prim w + +primOpBool1 name desc fn + = PrimEval (PrimOp name) desc [PVal] fn' + where fn' _world as0 + | Just (b1, []) <- takeArgBool as0 + = return $ Just $ makeXBool (fn b1) + fn' _world _ + = return $ Nothing + + +-- | Construct an evaluator for 2-arity bool operator. +primOpBool2 + :: Name -> Text + -> (Bool -> Bool -> Bool) + -> PrimEval s Prim w + +primOpBool2 name desc fn + = PrimEval (PrimOp name) desc [PVal, PVal] fn' + where + fn' _world as0 + | Just (b1, as1) <- takeArgBool as0 + , Just (b2, []) <- takeArgBool as1 + = return $ Just $ makeXBool (fn b1 b2) + fn' _world _ + = return $ Nothing + + +-- | Primitive evaluator for the #if operator. +-- Only the scrutinee is demanded, while the branches are not. +primOpIf :: PrimEval s Prim w +primOpIf + = PrimEval + (PrimOp "if") + "boolean if-then-else operator" + [PVal, PExp, PExp] fn' + where + fn' _world as0 + | Just (b1, as1) <- takeArgBool as0 + , Just (x1, as2) <- takeArgExp as1 + , Just (x2, []) <- takeArgExp as2 + = return $ Just $ if b1 then x1 else x2 + + fn' _world _ + = return $ Nothing + diff --git a/src/SMR/Prim/Op/List.hs b/src/SMR/Prim/Op/List.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Prim/Op/List.hs @@ -0,0 +1,106 @@ +{-# LANGUAGE OverloadedStrings #-} +module SMR.Prim.Op.List where +import SMR.Core.Exp +import SMR.Prim.Op.Base + + +-- | Primitive evaluators for list operators. +primOpsList :: [PrimEval s Prim w] +primOpsList + = [ primOpListCons, primOpListUncons + , primOpListSnoc, primOpListUnsnoc + , primOpListAppend ] + + +-- | Cons an element to a the front of a list. +primOpListCons :: PrimEval s Prim w +primOpListCons + = PrimEval + (PrimOp "list-cons") + "add an element to the front of a list" + [PExp, PVal] fn' + where + fn' _world as0 + | Just (x1, as1) <- takeArgExp as0 + , Just (XApp tag@(XRef (RPrm PrimTagList)) xs, []) + <- takeArgExp as1 + = return $ Just $ XApp tag (x1 : xs) + + fn' _world _ + = return $ Nothing + + +-- | Split an element from the front of a list. +primOpListUncons :: PrimEval s Prim w +primOpListUncons + = PrimEval + (PrimOp "list-uncons") + "split an element from the front of a list" + [PVal, PExp] fn' + where + fn' _world as0 + | Just (XApp tag@(XRef (RPrm PrimTagList)) xx, as1) + <- takeArgExp as0 + , Just (x2, []) <- takeArgExp as1 + = case xx of + x1 : xs -> return $ Just $ XApp x2 [x1, XApp tag xs] + [] -> return $ Nothing + fn' _world _ + = return $ Nothing + + +-- | Snoc an element to a the end of a list. +primOpListSnoc :: PrimEval s Prim w +primOpListSnoc + = PrimEval + (PrimOp "list-snoc") + "add an element to the end of a list" + [PVal, PExp] fn' + where + fn' _world as0 + | Just (XApp tag@(XRef (RPrm PrimTagList)) xs, as1) + <- takeArgExp as0 + , Just (x1, []) <- takeArgExp as1 + = return $ Just $ XApp tag (xs ++ [x1]) + fn' _world _ + = return $ Nothing + + +-- | Unsnoc an element from the end of a list. +primOpListUnsnoc :: PrimEval s Prim w +primOpListUnsnoc + = PrimEval + (PrimOp "list-unsnoc") + "split an element from the end of a list" + [PVal, PExp] fn' + where + fn' _world as0 + | Just (XApp tag@(XRef (RPrm PrimTagList)) xx, as1) + <- takeArgExp as0 + , Just (x2, []) <- takeArgExp as1 + = case reverse xx of + x1 : xs -> return $ Just $ XApp x2 [XApp tag (reverse xs), x1] + [] -> return $ Nothing + + fn' _world _ + = return $ Nothing + + +-- | Append two lists. +primOpListAppend :: PrimEval s Prim w +primOpListAppend + = PrimEval + (PrimOp "list-append") + "append two lists" + [PVal, PVal] fn' + where + fn' _world as0 + | Just (XApp (XRef (RPrm PrimTagList)) xs1, as1) + <- takeArgExp as0 + , Just (XApp tag@(XRef (RPrm PrimTagList)) xs2, []) + <- takeArgExp as1 + = return $ Just (XApp tag (xs1 ++ xs2)) + + fn' _world _ + = return $ Nothing + diff --git a/src/SMR/Prim/Op/Match.hs b/src/SMR/Prim/Op/Match.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Prim/Op/Match.hs @@ -0,0 +1,163 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ParallelListComp #-} +module SMR.Prim.Op.Match where +import SMR.Core.Exp +import SMR.Core.World +import SMR.Prim.Op.Base +import Data.IORef + + +-- | Primitive matching operators. +primOpsMatch :: [PrimEval s Prim w] +primOpsMatch + = [ primOpMatchSym + , primOpMatchApp + , primOpMatchAbs + , primOpMatchAbs1 ] + + + +-- | Match against a given symbol. +primOpMatchSym :: PrimEval s Prim w +primOpMatchSym + = PrimEval + (PrimOp "match-sym") + "match a symbol" + [PVal, PExp, PExp] fn' + where + fn' _world as0 + | Just (x1, as1) <- takeArgExp as0 + , Just (x2, as2) <- takeArgExp as1 + , Just (x3, []) <- takeArgExp as2 + = case x1 of + XRef (RSym _s1) + -> return $ Just $ XApp x3 [x1] + _ -> return $ Just $ x2 + + fn' _world _ + = return $ Nothing + + +-- | Match an application. +-- TODO(BL: pack the args into a list) +primOpMatchApp :: PrimEval s Prim w +primOpMatchApp + = PrimEval + (PrimOp "match-app") + "match an application" + [PVal, PExp, PExp] fn' + where + fn' _world as0 + | Just (x1, as1) <- takeArgExp as0 + , Just (x2, as2) <- takeArgExp as1 + , Just (x3, []) <- takeArgExp as2 + = case x1 of + XRef{} -> return $ Nothing + XKey{} -> return $ Nothing + XApp x11 xs12 -> return $ Just $ XApp x3 (x11 : xs12) + XVar{} -> return $ Nothing + XAbs{} -> return $ Just x2 + XSub{} -> return $ Nothing + + fn' _world _ + = return $ Nothing + + + +-- | Match all parameters of an abstraction. +primOpMatchAbs :: PrimEval s Prim w +primOpMatchAbs + = PrimEval + (PrimOp "match-abs") + "match all parameters of an abstraction" + [PVal, PExp, PExp] fn' + where + fn' world as0 + | Just (x1, as1) <- takeArgExp as0 + , Just (x2, as2) <- takeArgExp as1 + , Just (x3, []) <- takeArgExp as2 + = case x1 of + XAbs ps11 x12 -> fnAbs world x3 ps11 x12 + _ -> return $ Just $ x2 + + fn' _world _ + = return Nothing + + newNom world _ + = do ix <- atomicModifyIORef (worldNomGen world) + $ \ix -> (ix + 1, ix) + + return ix + + fnAbs world x2 ps11 x12 + = do -- Create new variables for each of the parameters. + ixs <- mapM (newNom world) ps11 + + let boolOfForm PVal = True + boolOfForm PExp = False + + let xIxs + = makeXList + [ makeXList + [ XRef (RNom ix) + , XRef (RPrm (PrimLitBool (boolOfForm $ formOfParam p))) ] + | ix <- ixs | p <- ps11 ] + + let xBody + = XSub [CSim (SSnv [BindVar (nameOfParam p) 0 (XRef (RNom ix)) + | p <- ps11 | ix <- ixs ])] + x12 + + return $ Just + $ XApp x2 (xIxs : [xBody]) + + +-- | Match the first parameter of an abstraction. +primOpMatchAbs1 :: PrimEval s Prim w +primOpMatchAbs1 + = PrimEval + (PrimOp "match-abs1") + "match the first parameter of an abstraction" + [PVal, PExp, PExp] fn' + where + fn' world as0 + | Just (x1, as1) <- takeArgExp as0 + , Just (x2, as2) <- takeArgExp as1 + , Just (x3, []) <- takeArgExp as2 + = case x1 of + XRef{} -> return $ Nothing + XKey{} -> return $ Nothing + XApp{} -> return $ Just x2 + XVar{} -> return $ Nothing + XAbs ps11 x12 -> fnAbs world x3 ps11 x12 + XSub{} -> return $ Nothing + + fn' _world _ + = return Nothing + + newNom world _ + = do ix <- atomicModifyIORef (worldNomGen world) + $ \ix -> (ix + 1, ix) + + return ix + + fnAbs _world _x2 [] _x12 + = return Nothing + + fnAbs world x2 (p1 : ps11) x12 + = do ix <- newNom world p1 + + let boolOfForm PVal = True + boolOfForm PExp = False + + let xIx = makeXList + [ XRef (RNom ix) + , XRef (RPrm (PrimLitBool (boolOfForm $ formOfParam p1))) ] + + let xBody + = XSub [ CSim (SSnv [BindVar (nameOfParam p1) 0 (XRef (RNom ix))])] + $ makeXAbs ps11 x12 + + return $ Just + $ XApp x2 (xIx : [xBody]) + diff --git a/src/SMR/Prim/Op/Nat.hs b/src/SMR/Prim/Op/Nat.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Prim/Op/Nat.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE OverloadedStrings #-} +module SMR.Prim.Op.Nat where +import SMR.Core.Exp +import SMR.Prim.Op.Base + + +type Nat = Integer + +-- | Primitive evaluators for nat operators. +primOpsNat :: [PrimEval s Prim w] +primOpsNat + = [ primOpNat2Nat "nat-add" "natural addition" (+) + , primOpNat2Nat "nat-sub" "natural subtration" + (\a b -> let x = a - b + in if x < 0 then 0 else x) + + , primOpNat2Nat "nat-mul" "natural multiplication" (*) + , primOpNat2Nat "nat-div" "natural division" div + , primOpNat2Nat "nat-rem" "natural remainder" rem + , primOpNat2Bool "nat-eq" "natural equality" (==) + , primOpNat2Bool "nat-neq" "natural negated equality" (/=) + , primOpNat2Bool "nat-lt" "natural less than" (<) + , primOpNat2Bool "nat-le" "natural less than equal" (<=) + , primOpNat2Bool "nat-gt" "natural greater than" (>) + , primOpNat2Bool "nat-ge" "natural greather than equal" (>=) ] + + +-- | Construct an evaluator for a 2-arity nat operator returning nat. +primOpNat2Nat + :: Text -> Text -> (Nat -> Nat -> Nat) + -> PrimEval s Prim w +primOpNat2Nat name desc fn + = PrimEval (PrimOp name) desc [PVal, PVal] fn' + where fn' _world as0 + | Just (n1, as1) <- takeArgNat as0 + , Just (n2, []) <- takeArgNat as1 + = return $ Just $ makeXNat (fn n1 n2) + fn' _world _ + = return $ Nothing + + +-- | Construct an evaluator for a 2-arity nat operator returning bool. +primOpNat2Bool + :: Text -> Text -> (Nat -> Nat -> Bool) + -> PrimEval s Prim w +primOpNat2Bool name desc fn + = PrimEval (PrimOp name) desc [PVal, PVal] fn' + where fn' _world as0 + | Just (n1, as1) <- takeArgNat as0 + , Just (n2, []) <- takeArgNat as1 + = return $ Just $ makeXBool (fn n1 n2) + fn' _world _ + = return $ Nothing diff --git a/src/SMR/Prim/Op/Nom.hs b/src/SMR/Prim/Op/Nom.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Prim/Op/Nom.hs @@ -0,0 +1,68 @@ +{-# LANGUAGE OverloadedStrings #-} +module SMR.Prim.Op.Nom where +import SMR.Prim.Op.Base +import SMR.Core.Exp.Base +import SMR.Core.World +import Data.IORef + + +-- | Primitive evalutor for nominal variable operators. +primOpsNom :: [PrimEval s Prim w] +primOpsNom + = [ primOpNomEq + , primOpNomFresh + , primOpNomClose ] + + +-- | Check for equality of two nominal variables. +primOpNomEq :: PrimEval s Prim w +primOpNomEq + = PrimEval + (PrimOp "nom-eq") + ("check equality of two nominal variables") + [PVal, PVal] fn' + where + fn' _world as0 + | Just (XRef (RNom n1), as1) <- takeArgExp as0 + , Just (XRef (RNom n2), []) <- takeArgExp as1 + = return $ Just + $ if n1 == n2 then XRef $ RPrm $ PrimLitBool True + else XRef $ RPrm $ PrimLitBool False + fn' _world _ + = return $ Nothing + + +-- | Allocate a fresh nominal variable. +primOpNomFresh :: PrimEval s Prim w +primOpNomFresh + = PrimEval + (PrimOp "nom-fresh") + "allocate a fresh nominal variable" + [PVal] fn' + where + fn' world as0 + | Just (XRef (RPrm PrimTagUnit), []) <- takeArgExp as0 + = do ix <- readIORef (worldNomGen world) + writeIORef (worldNomGen world) (ix + 1) + return $ Just $ XRef (RNom ix) + + fn' _world _ + = do return $ Nothing + + +-- | Create a closing substitution for a nominal variable. +primOpNomClose :: PrimEval s Prim w +primOpNomClose + = PrimEval + (PrimOp "nom-close") + ("creating a closing substitution for a nominal variable") + [PVal, PExp, PExp] fn' + where + fn' _world as0 + | Just (XRef (RNom n1), as1) <- takeArgExp as0 + , Just (x1, as2) <- takeArgExp as1 + , Just (x2, []) <- takeArgExp as2 + = return $ Just $ XSub [CSim (SSnv [BindNom n1 x1])] x2 + + fn' _world _ + = return $ Nothing diff --git a/src/SMR/Prim/Op/Sym.hs b/src/SMR/Prim/Op/Sym.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Prim/Op/Sym.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE OverloadedStrings #-} +module SMR.Prim.Op.Sym where +import SMR.Prim.Op.Base +import SMR.Core.Exp.Base + + +-- | Primitive evaluator for symbol operators. +primOpsSym :: Eq s => [PrimEval s Prim w] +primOpsSym + = [ primOpSymEq ] + + +-- | Check equality of two symbols. +primOpSymEq :: Eq s => PrimEval s Prim w +primOpSymEq + = PrimEval + (PrimOp "sym-eq") + ("check equality of two symbols") + [PVal, PVal] fn' + where + fn' _world as0 + | Just (XRef (RSym n1), as1) <- takeArgExp as0 + , Just (XRef (RSym n2), []) <- takeArgExp as1 + = return $ Just + $ if n1 == n2 then XRef $ RPrm $ PrimLitBool True + else XRef $ RPrm $ PrimLitBool False + fn' _world _ + = return $ Nothing diff --git a/src/SMR/Source/Expected.hs b/src/SMR/Source/Expected.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Source/Expected.hs @@ -0,0 +1,106 @@ + +module SMR.Source.Expected where +import SMR.Source.Parsec +import SMR.Source.Token +import SMR.Data.Located +import SMR.Data.Bag (Bag) +import Data.Text (Text) +import qualified SMR.Data.Bag as Bag +import qualified Data.Text as Text + +------------------------------------------------------------------------------- +-- | What we were expecting at the point there was a parse error. +data Expected t s p + -- | Expecting end of input. + = ExBaseEnd + + -- | Expecting a name in the given namespace. + | ExBaseNameOf Space + + -- | Expecting a name in any namespace. + | ExBaseNameAny + + -- | Expecting a natural number. + | ExBaseNat + + -- | Expecting a punctuation character. + | ExBasePunc Char + + -- | Expecting something described by the given message. + | ExBaseMsg String + + -- | Expecting something while parsing a declaration. + | ExContextDecl + Text + (Bag (Blocker t (Expected t s p))) + + -- | Expecting something while parsing a binding. + | ExContextBind + Text + (Bag (Blocker t (Expected t s p))) + deriving Show + + +-- | Pretty print an expected thing. +pprExpected + :: (Show s, Show p) + => Expected (Located Token) s p -> String +pprExpected bb + = case bb of + ExBaseEnd -> "expecting end of input" + ExBaseNameOf s -> "expecting name " ++ show s + ExBaseNat -> "expecting natural number" + ExBasePunc c -> "expecting " ++ show c + ExBaseMsg t -> "expecting " ++ show t + ExBaseNameAny -> "expecting name" + + ExContextDecl n es + -> "in declaration @" ++ Text.unpack n ++ "\n" + ++ (unlines $ map pprBlocker $ Bag.toList es) + + ExContextBind n esBag + | e : _ <- Bag.toList esBag + -> "in binding " ++ Text.unpack n ++ "\n" + ++ pprBlocker e + + | otherwise + -> "in binding " ++ Text.unpack n + + +-- | Pretty print a blocker. +pprBlocker + :: (Show s, Show p) + => Blocker (Located Token) (Expected (Located Token) s p) + -> String + +pprBlocker (Blocker [] e) + = pprExpected e + +pprBlocker (Blocker (t : _) e) + = pprLocation (startOfLocated t) + ++ " " ++ pprExpected e + + +pprLocation :: Location -> String +pprLocation (L l c) + = show l ++ ":" ++ show c + + +------------------------------------------------------------------------------- +-- | Parser error. +data ParseError t e + = ParseError [Blocker t e] + deriving Show + + +-- | Pretty print a parser error. +pprParseError + :: (Show s, Show p) + => ParseError (Located Token) (Expected (Located Token) s p) -> String + +pprParseError (ParseError []) + = "at end of input" + +pprParseError (ParseError (b : _bs)) + = pprBlocker b + diff --git a/src/SMR/Source/Lexer.hs b/src/SMR/Source/Lexer.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Source/Lexer.hs @@ -0,0 +1,179 @@ + +module SMR.Source.Lexer + ( lexTokens + , Located (..) + , Location(..)) +where +import SMR.Source.Token +import SMR.Data.Located +import Data.Text (Text) +import qualified Data.Text as Text +import qualified Data.Char as Char + + +-- Lexer ---------------------------------------------------------------------- +-- | Lex a sequence of tokens. +lexTokens :: Location -> [Char] -> ([Located Token], Location, [Char]) +lexTokens lStart0 cs0 + = case skipSpace lStart0 cs0 of + (lStart, []) + -> ( LL lStart lStart KEnd : [] + , lStart, []) + + (lStart, cs) + -> case lexToken lStart cs of + Nothing + -> ([], lStart, cs) + + Just (k, cs') + | (ks, lStart', cs'') <- lexTokens (endOfLocated k) cs' + -> (k : ks, lStart', cs'') + + +-- | Lex a single token. +lexToken :: Location -> [Char] -> Maybe (Located Token, [Char]) +lexToken lStart xx + = case xx of + [] + -> Nothing + + c : cs + -- Punctuation. + | isCharPunc c + -> let lEnd = incCharOfLocation 1 lStart + tok = KPunc c + in Just (LL lStart lEnd tok, cs) + + -- Variable name. + | Just (space, xx') <- takeSpace c cs + , Just (name, lEnd, csRest) <- lexName (incCharOfLocation 1 lStart) xx' + -> let tok = KName space name + in Just (LL lStart lEnd tok, csRest) + + -- Natural number. + | Char.isDigit c + , Just (nat, lEnd, csRest) <- lexNat lStart (c : cs) + -> let tok = KNat nat + in Just (LL lStart lEnd tok, csRest) + + | otherwise + -> Nothing + + +-- | Lex a variable name. +lexName :: Location -> [Char] -> Maybe (Text, Location, [Char]) +lexName lStart xx + = go lStart [] xx + where + go lStart' acc [] + | not $ null acc + = let name = Text.pack $ reverse acc + in Just (name, lStart', []) + + | otherwise + = Nothing + + go lStart' acc (c : cs) + | isNameBodyChar c + = go (incCharOfLocation 1 lStart') (c : acc) cs + + | otherwise + = let name = Text.pack $ reverse acc + in Just (name, lStart', c : cs) + + +-- | Lex a natural number. +lexNat :: Location -> [Char] -> Maybe (Integer, Location, [Char]) +lexNat lStart xx + = go lStart [] xx + where + go lStart' acc [] + | not $ null acc + , all Char.isDigit acc + , nat <- read $ reverse acc + = Just (nat, lStart', []) + + go lStart' acc (c : cs) + | Char.isDigit c + = go (incCharOfLocation 1 lStart') (c : acc) cs + + | all Char.isDigit acc + , not $ null acc + , nat <- read $ reverse acc + = Just (nat, lStart', c : cs) + + go _ _ _ + = Nothing + + +-- Whitespace ----------------------------------------------------------------- +skipSpace :: Location -> [Char] -> (Location, [Char]) +skipSpace lStart xx + = case xx of + [] -> (lStart, xx) + + c : cs + -- Skip whitespace. + | c == ' ' -> skipSpace (incCharOfLocation 1 lStart) cs + | c == '\n' -> skipSpace (incLineOfLocation 1 lStart) cs + | c == '\t' -> skipSpace (incCharOfLocation 8 lStart) cs + + -- Skip comments + | c == '-' + , c2 : cs2 <- cs + , c2 == '-' + -> skipSpace lStart $ dropWhile (\x -> x /= '\n') cs2 + + | otherwise -> (lStart, xx) + + +-- | Take the namespace qualifier from the front of a name. +takeSpace :: Char -> [Char] -> Maybe (Space, [Char]) +takeSpace c cs + | Char.isLower c = Just (SVar, c : cs) + | c == '@' = Just (SMac, cs) + | c == '%' = Just (SSym, cs) + | c == '+' = Just (SSet, cs) + | c == '#' + , c' : cs' <- cs + , c' == '#' + = Just (SKey, cs') + + | c == '#' = Just (SPrm, cs) + | otherwise = Nothing + + +-- Character Classes ---------------------------------------------------------- +-- | Check if this character can appear in the body of a name. +isNameBodyChar :: Char -> Bool +isNameBodyChar c + = Char.isLower c + || Char.isUpper c + || Char.isDigit c + || (c == '-' || c == '\'' || c == '_') + + +-- | Check if this is a punctuation character. +isCharPunc :: Char -> Bool +isCharPunc c + | c == '(' = True + | c == ')' = True + | c == '{' = True + | c == '}' = True + | c == '[' = True + | c == ']' = True + | c == '<' = True + | c == '>' = True + | c == '^' = True + | c == ',' = True + | c == ':' = True + | c == '\\' = True + | c == '.' = True + | c == ';' = True + | c == '=' = True + | c == '$' = True + | c == '!' = True + | c == '~' = True + | c == '?' = True + | otherwise = False + diff --git a/src/SMR/Source/Parsec.hs b/src/SMR/Source/Parsec.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Source/Parsec.hs @@ -0,0 +1,368 @@ + +-- | Parser combinator framework. +module SMR.Source.Parsec where +import qualified SMR.Data.Bag as Bag +import SMR.Data.Bag (Bag) + +------------------------------------------------------------------------------- +-- | Parser is a function that takes a list of tokens, +-- and returns a list of remaining tokens along with +-- (on error) a list of descriptions of expected input, +-- (on success) a parsed value. +-- +data Parser t e a + = Parser ([t] -> ParseResult t e a) + + +-- | Result of a parser, +-- parameterised by +-- (t) the type of tokens, +-- (e) the type for decriptions of what we're expecting to parse. +-- (a) type of value to parse. +-- +data ParseResult t e a + -- | Parser failed after consuming no input. + -- The parser looked at one or more tokens at the front of the + -- input but based on these the input does not look like whatever + -- syntax the parser was supposed to parse. + = ParseSkip + (Bag (Blocker t e)) -- Where we got blocked trying other parses. + + -- | Parser yielding a value after consuming no input. + -- The parser returned a value without looking at any tokens, + -- this is a pure value returning action. + | ParseReturn + (Bag (Blocker t e)) -- Where we got blocked trying other parses. + a -- Produced value. + + -- | Parse failed after partially consuming input. + -- The parser thought that the input sequence looked like what it + -- was supposed to parse, but complete parsing failed once it + -- had committed. + | ParseFailure + (Bag (Blocker t e)) -- Where we got blocked trying other parses. + + -- | Parse succeeded yielding a value after consuming input. + -- We have a complete value, and have consumed some input tokens. + | ParseSuccess + a -- Produced value. + [t] -- Remaining input tokens. + deriving Show + + +-- | Describes why the parser could not make further progress. +data Blocker t e + = Blocker + { blockerTokens :: [t] -- ^ Remaining input tokens where we failed. + , blockerExpected :: e -- ^ Description of what we were expecting. + } + deriving Show + + +------------------------------------------------------------------------------- +-- | Apply a parser to a list of input tokens. +parse :: Parser t e a -> [t] -> ParseResult t e a +parse (Parser p) ts = p ts + + +-- Functor -------------------------------------------------------------------- +instance Functor (Parser t e) where + fmap f parserA + = Parser $ \ts0 + -> case parse parserA ts0 of + ParseSkip bs1 -> ParseSkip bs1 + ParseReturn bs1 x -> ParseReturn bs1 (f x) + ParseFailure bs1 -> ParseFailure bs1 + ParseSuccess a ts1 -> ParseSuccess (f a) ts1 + + +-- Applicative ---------------------------------------------------------------- +instance Applicative (Parser t e) where + pure x + = Parser $ \_ + -> ParseReturn Bag.nil x + + (<*>) parserF parserA + = Parser $ \ts0 + -> case parse parserF ts0 of + ParseSkip es1 + -> ParseSkip es1 + + ParseFailure bs1 + -> ParseFailure bs1 + + ParseReturn es1 f + -> case parse parserA ts0 of + ParseSkip es2 -> ParseSkip (Bag.union es1 es2) + ParseReturn es2 x -> ParseReturn (Bag.union es1 es2) (f x) + ParseFailure bs2 -> ParseFailure (Bag.union es1 bs2) + ParseSuccess x ts2 -> ParseSuccess (f x) ts2 + + ParseSuccess f ts1 + -> case parse parserA ts1 of + ParseSkip bs2 -> ParseFailure bs2 + ParseReturn _ x -> ParseSuccess (f x) ts1 + ParseFailure bs2 -> ParseFailure bs2 + ParseSuccess x ts2 -> ParseSuccess (f x) ts2 + + +-- Monad ---------------------------------------------------------------------- +instance Monad (Parser t e) where + return x + = Parser $ \_ + -> ParseReturn Bag.nil x + + (>>=) parserA mkParserB + = Parser $ \ts0 + -> case parse parserA ts0 of + ParseSkip bs1 + -> ParseSkip bs1 + + ParseFailure bs1 + -> ParseFailure bs1 + + -- First parser produced a value but did not consume input. + ParseReturn _ xa + -> parse (mkParserB xa) ts0 + + -- First parser produced a value and consumed input. + ParseSuccess xa ts1 + -> case parse (mkParserB xa) ts1 of + -- The second parser skipped, but as we've already consumed + -- input tokens we treat this as a failure. + ParseSkip bs2 -> ParseFailure bs2 + + -- The second parser returned a value, and though it didn't + -- consume input itself, the whole computation has, + -- so still treat this as a success. + ParseReturn _ xb -> ParseSuccess xb ts1 + + -- The second parser failed. + ParseFailure bs2 -> ParseFailure bs2 + + -- The second parser suceeded, to take the new value. + ParseSuccess xb ts2 -> ParseSuccess xb ts2 + + +-- Prim ----------------------------------------------------------------------- +-- Primitive parsers. + +-- | Always fail, producing no possible parses and no helpful error message. +fail :: Parser t e a +fail + = Parser $ \_ + -> ParseFailure Bag.nil + + +-- | Always fail, yielding the given message describing what was expected. +expected :: e -> Parser t e a +expected xe + = Parser $ \ts + -> ParseFailure (Bag.singleton (Blocker ts xe)) + + +-- | Commit to the given parser, so if it skips or returns without +-- consuming any input then treat that as failure. +commit :: Parser t e a -> Parser t e a +commit parserA + = Parser $ \ts0 + -> case parse parserA ts0 of + ParseSkip bs1 -> ParseFailure bs1 + ParseReturn bs1 _ -> ParseFailure bs1 + ParseFailure bs1 -> ParseFailure bs1 + ParseSuccess xb xs2 -> ParseSuccess xb xs2 + + +-- | Parse in an expectation context. +enter :: (Bag (Blocker t e) -> e) -> Parser t e a -> Parser t e a +enter mk parserA + = Parser $ \ts0 + -> case parse parserA ts0 of + ParseSkip bs1 + -> ParseSkip (Bag.singleton (Blocker ts0 (mk bs1))) + + ParseReturn bs1 x + -> ParseReturn (Bag.singleton (Blocker ts0 (mk bs1))) x + + ParseFailure bs1 + -> ParseFailure (Bag.singleton (Blocker ts0 (mk bs1))) + + ParseSuccess xb ts2 + -> ParseSuccess xb ts2 + + +-- | If the given parser suceeds then enter an expectation context +-- for the next one. +enterOn :: Parser t e a + -> (a -> Bag (Blocker t e) -> e) + -> (a -> Parser t e b) + -> Parser t e b + +enterOn parserA mk mkParserB + = Parser $ \ts0 + -> case parse parserA ts0 of + ParseSkip bs0 + -> ParseSkip bs0 + + ParseFailure bs1 + -> ParseFailure bs1 + + ParseReturn _ xa + -> case parse (mkParserB xa) ts0 of + ParseSkip bs2 + -> ParseSkip (Bag.singleton (Blocker ts0 (mk xa bs2))) + + ParseReturn bs2 xb + -> ParseReturn (Bag.singleton (Blocker ts0 (mk xa bs2))) xb + + ParseFailure bs2 + -> ParseFailure (Bag.singleton (Blocker ts0 (mk xa bs2))) + + ParseSuccess xb ts2 + -> ParseSuccess xb ts2 + + + ParseSuccess xa ts1 + -> case parse (mkParserB xa) ts1 of + ParseSkip bs2 + -> ParseSkip (Bag.singleton (Blocker ts0 (mk xa bs2))) + + ParseReturn bs2 xb + -> ParseReturn (Bag.singleton (Blocker ts0 (mk xa bs2))) xb + + ParseFailure bs2 + -> ParseFailure (Bag.singleton (Blocker ts0 (mk xa bs2))) + + ParseSuccess xb ts2 + -> ParseSuccess xb ts2 + + +-- | Peek at the first input token, without consuming at it. +peek :: Parser t e t +peek + = Parser $ \ts + -> case ts of + [] -> ParseFailure Bag.nil + t : _ -> ParseReturn Bag.nil t + + +-- | Consume the first input token, failing if there aren't any. +item :: e -> Parser t e t +item xe + = Parser $ \ts + -> case ts of + [] -> ParseSkip (Bag.singleton (Blocker ts xe)) + t : ts' -> ParseSuccess t ts' + + +-- | Consume the first input token if it matches the given predicate, +-- failing without consuming if the predicate does not match. +satisfies :: e -> (t -> Bool) -> Parser t e t +satisfies xe p + = Parser $ \ts + -> case ts of + [] -> ParseSkip (Bag.singleton (Blocker ts xe)) + t : ts' + | p t -> ParseSuccess t ts' + | otherwise -> ParseSkip (Bag.singleton (Blocker ts xe)) + + +-- | Consume the first input token if it is accepted by the given match +-- function. Fail without consuming if there is no match. +from :: e -> (t -> Maybe a) -> Parser t e a +from xe accept + = Parser $ \ts + -> case ts of + [] -> ParseSkip (Bag.singleton (Blocker ts xe)) + t : ts' + -> case accept t of + Just x -> ParseSuccess x ts' + Nothing -> ParseSkip (Bag.singleton (Blocker ts xe)) + + +-- | Given two parsers, try the first and if it succeeds produce +-- the output of that parser, if not try the second. +alt :: Parser t e a -> Parser t e a -> Parser t e a +alt parserA parserB + = alts (parserA : parserB : []) + + +-- | Like 'alt' but take a list of parser, trying them in order. +alts :: [Parser t e a] -> Parser t e a +alts parsers + = Parser $ \ts0 + -> go ts0 (False, Nothing) (Bag.nil, Bag.nil) parsers + where + go _ (False, Nothing) (bsSkip, _bsFail) [] + = ParseSkip bsSkip + + go _ (False, (Just x)) (bsSkip, _bsFail) [] + = ParseReturn bsSkip x + + go _ (True, _) (_bsSkip, bsFail) [] + = ParseFailure bsFail + + go ts0 (failed, mx) (bsSkip, bsFail) (p : ps) + = case parse p ts0 of + ParseSkip bs1 + -> go ts0 (failed, mx) (Bag.union bsSkip bs1, bsFail) ps + + ParseFailure bs1 + -> go ts0 (True, mx) (bsSkip, Bag.union bsFail bs1) ps + + ParseReturn bs1 x + -> go ts0 (failed, Just x) (Bag.union bsSkip bs1, bsFail) ps + + ParseSuccess x ts1 + -> ParseSuccess x ts1 + + +-- Derived -------------------------------------------------------------------- +-- Parsers derived from the primitive ones. + +-- | Parse zero or more things, yielding a list of those things. +some :: Parser t e a -> Parser t e [a] +some parserA + = alt (do + x <- parserA + xs <- some parserA + return $ x : xs) + (return []) + + +-- | Parse one or more things, yielding a list of those things. +many :: Parser t e a -> Parser t e [a] +many parserA + = do x <- parserA + xs <- some parserA + return $ x : xs + + +-- | Parse some things separated by other things. +sepBy :: Parser t e a -> Parser t e s -> Parser t e [a] +sepBy parserA parserS + = alt (sepBy1 parserA parserS) + (return []) + + +-- | Parse at least one thing separated by other things. +sepBy1 :: Parser t e a -> Parser t e s -> Parser t e [a] +sepBy1 parserA parserS + = do x <- parserA + alt + (do _s <- parserS + xs <- sepBy1 parserA parserS + return $ x : xs) + + (do return $ x : []) + + +-- | Run a parser, peeking at the starting and ending tokens. +withDelims :: Parser t e a -> Parser t e (t, a, t) +withDelims p + = do kStart <- peek + x <- p + kEnd <- peek + return (kStart, x, kEnd) + + diff --git a/src/SMR/Source/Parser.hs b/src/SMR/Source/Parser.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Source/Parser.hs @@ -0,0 +1,351 @@ + +module SMR.Source.Parser where +import SMR.Core.Exp.Base +import SMR.Source.Expected +import SMR.Source.Token +import SMR.Source.Lexer +import SMR.Data.Located + +import Data.Text (Text) + +import qualified SMR.Source.Parsec as P +import qualified SMR.Data.Bag as Bag +import qualified Data.Text as Text + + +type Parser s p a + = P.Parser (Located Token) (Expected (Located Token) s p) a + + +-- Config --------------------------------------------------------------------- +data Config s p + = Config + { configReadSym :: Text -> Maybe s + , configReadPrm :: Text -> Maybe p } + + +-- Interface ------------------------------------------------------------------ +parseDecls + :: Config s p + -> [Located Token] + -> Either (ParseError (Located Token) (Expected (Located Token) s p)) + [Decl s p] +parseDecls c ts + = case P.parse pDeclsEnd ts of + P.ParseSkip es -> Left $ ParseError (Bag.toList es) + P.ParseReturn _ xx -> Right xx + P.ParseFailure bs -> Left $ ParseError (Bag.toList bs) + P.ParseSuccess xx _ -> Right xx + where + pDeclsEnd + = do ds <- pDecls c + _ <- pEnd + return ds + + + +-- | Parse a complete expression from the given list of tokens. +parseExp + :: Config s p + -> [Located Token] + -> Either (ParseError (Located Token) (Expected (Located Token) s p)) + (Exp s p) +parseExp c ts + = case P.parse pExpEnd ts of + P.ParseSkip es -> Left $ ParseError (Bag.toList es) + P.ParseReturn _ xx -> Right xx + P.ParseFailure bs -> Left $ ParseError (Bag.toList bs) + P.ParseSuccess xx _ -> Right xx + where + pExpEnd + = do x <- pExp c + _ <- pEnd + return x + + +-- Decl ----------------------------------------------------------------------- +pDecls :: Config s p -> Parser s p [Decl s p] +pDecls c + = P.some (pDecl c) + + +pDecl :: Config s p -> Parser s p (Decl s p) +pDecl c + = P.alts + [ P.enterOn (pNameOfSpace SMac) ExContextDecl $ \name + -> do psParam <- P.some pParam + _ <- pPunc '=' + xBody <- pExp c + _ <- pPunc ';' + if length psParam == 0 + then return (DeclMac name xBody) + else return (DeclMac name $ XAbs psParam xBody) + + , P.enterOn (pNameOfSpace SSet) ExContextDecl $ \name + -> do _ <- pPunc '=' + xBody <- pExp c + _ <- pPunc ';' + return (DeclSet name xBody) + ] + + +-- Exp ------------------------------------------------------------------------ +pExp :: Config s p -> Parser s p (Exp s p) +pExp c + -- Abstraction. + = P.alts + [ do _ <- pPunc '\\' + psParam <- P.some pParam + _ <- pPunc '.' + xBody <- pExp c + return $ XAbs psParam xBody + + -- Substitution train. + , do csTrain <- pTrain c + _ <- pPunc '.' + xBody <- pExp c + return $ XSub (reverse csTrain) xBody + + -- Application possibly using '$' + , do xHead <- pExpApp c + P.alt + (do _ <- pPunc '$' + xRest <- pExp c + return $ XApp xHead [xRest]) + (return xHead) + ] + + +-- | Parser for an application. +pExpApp :: Config s p -> Parser s p (Exp s p) +pExpApp c + -- Application of a superprim. + = P.alts + [ do nKey + <- do nKey' <- pNameOfSpace SKey + if nKey' == Text.pack "box" then return KBox + else if nKey' == Text.pack "run" then return KRun + else P.fail + + xArg <- pExpAtom c + return $ XKey nKey xArg + + -- Application of some other expression. + , do xFun <- pExpAtom c + xsArgs <- P.some (pExpAtom c) + case xsArgs of + [] -> return $ xFun + _ -> return $ XApp xFun xsArgs + ] + + +-- | Parser for an atomic expression. +pExpAtom :: Config s p -> Parser s p (Exp s p) +pExpAtom c + -- Parenthesised expression. + = P.alts + [ do _ <- pPunc '(' + x <- pExp c + _ <- pPunc ')' + return x + + -- Nominal variable. + , do _ <- pPunc '?' + n <- pNat + return $ XRef (RNom n) + + -- Named variable with or without index. + , do (space, name) <- pName + + case space of + -- Named variable. + SVar + -> P.alt (do _ <- pPunc '^' + ix <- pNat + return $ XVar name ix) + (return $ XVar name 0) + + -- Named macro. + SMac -> return $ XRef (RMac name) + + -- Named set. + SSet -> return $ XRef (RSet name) + + -- Named symbol + SSym + -> case configReadSym c name of + Just s -> return (XRef (RSym s)) + Nothing -> P.fail + + -- Named primitive. + SPrm + -> case configReadPrm c name of + Just p -> return (XRef (RPrm p)) + Nothing -> P.fail + + -- Named keyword. + SKey -> P.fail + + -- Named nominal (should be handled above) + SNom -> P.fail + ] + + +-- Param ---------------------------------------------------------------------- +-- | Parser for a function parameter. +pParam :: Parser s p Param +pParam + = P.alts + [ do _ <- pPunc '!' + n <- pNameOfSpace SVar + return $ PParam n PVal + + , do _ <- pPunc '~' + n <- pNameOfSpace SVar + return $ PParam n PExp + + , do n <- pNameOfSpace SVar + return $ PParam n PVal + + ] + + +-- Train ---------------------------------------------------------------------- +-- | Parser for a substitution train. +-- The cars are produced in reverse order. +pTrain :: Config s p -> Parser s p [Car s p] +pTrain c + = do cCar <- pTrainCar c + P.alt + (do csCar <- pTrain c + return $ cCar : csCar) + (do return $ cCar : []) + + +-- | Parse a single car in the train. +pTrainCar :: Config s p -> Parser s p (Car s p) +pTrainCar c + = P.alt + -- Substitution, both simultaneous and recursive + (do car <- pCarSimRec c + return car) + + (do -- An ups car. + ups <- pUps + return (CUps ups)) + + +-- Snv ------------------------------------------------------------------------ +-- | Parser for a substitution environment. +-- +-- Snv ::= '[' Bind*, ']' +-- +pCarSimRec :: Config s p -> Parser s p (Car s p) +pCarSimRec c + = do _ <- pPunc '[' + + P.alt -- Recursive substitution. + (do _ <- pPunc '[' + bs <- P.sepBy (pBind c) (pPunc ',') + _ <- pPunc ']' + _ <- pPunc ']' + return $ CRec (SSnv (reverse bs))) + + -- Simultaneous substitution. + (do bs <- P.sepBy (pBind c) (pPunc ',') + _ <- pPunc ']' + return $ CSim (SSnv (reverse bs))) + + +-- | Parser for a binding. +-- +-- Bind ::= Name '=' Exp +-- | Name '^' Nat '=' Exp +-- +pBind :: Config s p -> Parser s p (SnvBind s p) +pBind c + = P.alt + (P.enterOn (pNameOfSpace SVar) ExContextBind $ \name + -> P.alt + (do _ <- pPunc '=' + x <- pExp c + return $ BindVar name 0 x) + + (do _ <- pPunc '^' + bump <- pNat + _ <- pPunc '=' + x <- pExp c + return $ BindVar name bump x)) + + (do pPunc '?' + ix <- pNat + _ <- pPunc '=' + x <- pExp c + return $ BindNom ix x) + + +-- Ups ------------------------------------------------------------------------ +-- | Parser for an ups. +-- +-- Ups ::= '{' Bump*, '}' +-- +pUps :: Parser s p Ups +pUps + = do _ <- pPunc '{' + bs <- P.sepBy pBump (pPunc ',') + _ <- pPunc '}' + return $ UUps (reverse bs) + + +-- | Parser for a bump. +-- +-- Bump ::= Name ':' Nat +-- | Name '^' Nat ':' Nat +-- +pBump :: Parser s p UpsBump +pBump + = do name <- pNameOfSpace SVar + P.alt + (do _ <- pPunc ':' + inc <- pNat + return ((name, 0), inc)) + + (do _ <- pPunc '^' + depth <- pNat + _ <- pPunc ':' + inc <- pNat + return ((name, depth), inc)) + + +------------------------------------------------------------------------------- +-- | Parser for a natural number. +pNat :: Parser s p Integer +pNat + = P.from ExBaseNat (takeNatOfToken . valueOfLocated) + + +-- | Parser for a name in the given space. +pNameOfSpace :: Space -> Parser s p Text +pNameOfSpace s + = P.from (ExBaseNameOf s) (takeNameOfToken s . valueOfLocated) + + +-- | Parser for a name of any space. +pName :: Parser s p (Space, Text) +pName + = P.from ExBaseNameAny (takeAnyNameOfToken . valueOfLocated) + + +-- | Parser for the end of input token. +pEnd :: Parser s p () +pEnd + = do _ <- P.satisfies ExBaseEnd (isToken KEnd . valueOfLocated) + return () + + +-- | Parser for a punctuation character. +pPunc :: Char -> Parser s p () +pPunc c + = do _ <- P.satisfies (ExBasePunc c) (isToken (KPunc c) . valueOfLocated) + return () + diff --git a/src/SMR/Source/Pretty.hs b/src/SMR/Source/Pretty.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Source/Pretty.hs @@ -0,0 +1,200 @@ +{-# LANGUAGE OverloadedStrings #-} +module SMR.Source.Pretty where +import SMR.Core.Exp.Base +import SMR.Prim.Name +import SMR.Prim.Op.Base +import Data.Monoid +import Data.Text (Text) +import Data.Text.Lazy.Builder (Builder) +import qualified Data.Text.Lazy.Builder as B + + +-- Class ---------------------------------------------------------------------- +-- | Class of things that can be converted to text builders. +class Build a where + build :: a -> Builder + +instance Build Text where + build tx = B.fromText tx + +instance Build Prim where + build pp = buildPrim pp + + +-- | Context we're currently in when pretty printing. +data Ctx + = CtxTop -- ^ Top level context. + | CtxFun -- ^ Functional expression in an an application. + | CtxArg -- ^ Argument expression in an application. + deriving Show + + +-- | Wrap a thing in parenthesis. +parens :: Builder -> Builder +parens bb + = "(" <> bb <> ")" + + +-- Decl ----------------------------------------------------------------------- +-- | Yield a builder for a declaration. +buildDecl + :: (Build s, Build p) + => Decl s p -> Builder +buildDecl dd + = case dd of + DeclMac n xx + -> "@" <> B.fromText n <> " = " <> buildExp CtxTop xx <> ";\n" + + DeclSet n xx + -> "+" <> B.fromText n <> " = " <> buildExp CtxTop xx <> ";\n" + + +-- Exp ------------------------------------------------------------------------ +-- | Yield a builder for an expression. +buildExp + :: (Build s, Build p) + => Ctx -> Exp s p -> Builder +buildExp ctx xx + = case xx of + XRef r -> buildRef r + + XVar n 0 -> B.fromText n + XVar n d -> B.fromText n <> "^" <> B.fromString (show d) + + XKey k1 x2 + -> let ppExp = buildKey k1 <> " " <> buildExp CtxArg x2 + in case ctx of + CtxArg -> parens ppExp + _ -> ppExp + + XApp x1 xs2 + -> let ppExp = buildExp CtxFun x1 <> " " <> go xs2 + go [] = "" + go (x : []) = buildExp CtxArg x + go (x11 : x21 : xs) = buildExp CtxArg x11 <> " " <> go (x21 : xs) + in case ctx of + CtxArg -> parens ppExp + _ -> ppExp + + XAbs vs x + -> let go [] = "." + go (p1 : []) = buildParam p1 <> "." + go (p1 : ps) = buildParam p1 <> " " <> go ps + ss = "\\" <> go vs <> buildExp CtxTop x + in case ctx of + CtxArg -> parens ss + CtxFun -> parens ss + _ -> ss + + XSub train x + | length train == 0 + -> buildExp ctx x + | otherwise + -> let ss = buildTrain train <> "." <> buildExp CtxTop x + in case ctx of + CtxArg -> parens ss + CtxFun -> parens ss + _ -> ss + + +-- | Yield a builder for a parameter. +buildParam :: Param -> Builder +buildParam pp + = case pp of + PParam n PVal -> B.fromText n + PParam n PExp -> "~" <> B.fromText n + + +-- | Yield a builder for a keyword. +buildKey :: Key -> Builder +buildKey kk + = case kk of + KBox -> "##box" + KRun -> "##run" + + +-- Train ---------------------------------------------------------------------- +-- | Yield a builder for a train. +buildTrain :: (Build s, Build p) => Train s p -> Builder +buildTrain cs0 + = go cs0 + where go [] = "" + go (c : cs) = go cs <> buildCar c + + +-- | Yield a builder for a train car. +buildCar :: (Build s, Build p) => Car s p -> Builder +buildCar cc + = case cc of + CSim snv -> buildSnv snv + CRec snv -> "[" <> buildSnv snv <> "]" + CUps ups -> buildUps ups + + +-- Snv ------------------------------------------------------------------------ +-- | Yield a builder for a substitution. +buildSnv :: (Build s, Build p) => Snv s p -> Builder +buildSnv (SSnv vs) + = "[" <> go (reverse vs) <> "]" + where go [] = "" + go (b : []) = buildSnvBind b + go (b : bs) = buildSnvBind b <> ", " <> go bs + + +-- | Yield a builder for a substitution binding. +buildSnvBind :: (Build s, Build p) => SnvBind s p -> Builder +buildSnvBind (BindVar name bump xx) + | bump == 0 + = B.fromText name + <> "=" <> buildExp CtxTop xx + + | otherwise + = B.fromText name <> "^" <> B.fromString (show bump) + <> "=" <> buildExp CtxTop xx + +buildSnvBind (BindNom ix xx) + = "?" <> B.fromString (show ix) + <> "=" <> buildExp CtxTop xx + + +-- Ups ------------------------------------------------------------------------ +-- | Yield a builder for an ups. +buildUps :: Ups -> Builder +buildUps (UUps vs) + = "{" <> go (reverse vs) <> "}" + where go [] = "" + go (b : []) = buildUpsBump b + go (b : bs) = buildUpsBump b <> ", " <> go bs + + +-- | Yield a builder for an ups bump. +buildUpsBump :: UpsBump -> Builder +buildUpsBump ((name, bump), inc) + | bump == 0 + = B.fromText name + <> "=" <> B.fromString (show inc) + + | otherwise + = B.fromText name <> "^" <> B.fromString (show bump) + <> "=" <> B.fromString (show inc) + + +-- Ref ------------------------------------------------------------------------ +-- | Yield a builder for a reference. +buildRef :: (Build s, Build p) => Ref s p -> Builder +buildRef rr + = case rr of + RMac n -> "@" <> B.fromText n + RSet n -> "+" <> B.fromText n + RSym s -> "%" <> build s + RPrm p -> "#" <> build p + RNom i -> "?" <> B.fromString (show i) + + +-- Prim ----------------------------------------------------------------------- +-- | Yield a builder for a primitive. +buildPrim :: Prim -> Builder +buildPrim pp + = B.fromText $ pprPrim pp + + diff --git a/src/SMR/Source/Token.hs b/src/SMR/Source/Token.hs new file mode 100644 --- /dev/null +++ b/src/SMR/Source/Token.hs @@ -0,0 +1,65 @@ + +module SMR.Source.Token where +import Data.Text (Text) + + +-- | Tokens for for the source language. +data Token + = KEnd -- ^ End of input. + | KPunc Char -- ^ Punctuation character. + | KName Space Text -- ^ A scoped name. + | KNat Integer -- ^ A natural number. + deriving (Show, Eq) + + +-- | Name space of a name. +data Space + = SVar -- ^ Local variable. + | SMac -- ^ Macro name. + | SSym -- ^ Symbol name. + | SSet -- ^ Set name. + | SPrm -- ^ Primitive name. + | SKey -- ^ Keyword (super primitive) + | SNom -- ^ Nominal name. + deriving (Show, Eq) + + +-- | Check if a token is equal to the give none. +isToken :: Token -> Token -> Bool +isToken k1 k2 = k1 == k2 + + +-- | Check is token is punctuation using the given character. +isKPunc :: Char -> Token -> Bool +isKPunc c k + = case k of + KPunc c' -> c == c' + _ -> False + + +-- | Take the name from a token, if any. +takeNameOfToken :: Space -> Token -> Maybe Text +takeNameOfToken ss1 kk + = case kk of + KName ss2 n + | ss1 == ss2 -> Just n + | otherwise -> Nothing + _ -> Nothing + + +-- | Take the name from a token, if any. +takeAnyNameOfToken :: Token -> Maybe (Space, Text) +takeAnyNameOfToken kk + = case kk of + KName ss2 n -> Just (ss2, n) + _ -> Nothing + + +-- | Take the natural number from a token, if any. +takeNatOfToken :: Token -> Maybe Integer +takeNatOfToken kk + = case kk of + KNat n -> Just n + _ -> Nothing + +