shimmer (empty) → 0.1.1
raw patch · 34 files changed
+4637/−0 lines, 34 filesdep +basedep +bytestringdep +containerssetup-changed
Dependencies added: base, bytestring, containers, filepath, haskeline, text, vector
Files
- LICENSE +21/−0
- Setup.hs +2/−0
- shimmer.cabal +70/−0
- src/SMR/CLI/Config.hs +75/−0
- src/SMR/CLI/Driver/Load.hs +53/−0
- src/SMR/CLI/Help.hs +58/−0
- src/SMR/CLI/Repl.hs +386/−0
- src/SMR/Codec/Peek.hs +486/−0
- src/SMR/Codec/Poke.hs +324/−0
- src/SMR/Codec/Size.hs +132/−0
- src/SMR/Core/Exp.hs +38/−0
- src/SMR/Core/Exp/Base.hs +143/−0
- src/SMR/Core/Exp/Compounds.hs +50/−0
- src/SMR/Core/Exp/Push.hs +104/−0
- src/SMR/Core/Exp/Train.hs +279/−0
- src/SMR/Core/Step.hs +349/−0
- src/SMR/Core/World.hs +22/−0
- src/SMR/Data/Bag.hs +64/−0
- src/SMR/Data/Located.hs +39/−0
- src/SMR/Prim/Name.hs +49/−0
- src/SMR/Prim/Op.hs +27/−0
- src/SMR/Prim/Op/Base.hs +113/−0
- src/SMR/Prim/Op/Bool.hs +66/−0
- src/SMR/Prim/Op/List.hs +106/−0
- src/SMR/Prim/Op/Match.hs +163/−0
- src/SMR/Prim/Op/Nat.hs +53/−0
- src/SMR/Prim/Op/Nom.hs +68/−0
- src/SMR/Prim/Op/Sym.hs +28/−0
- src/SMR/Source/Expected.hs +106/−0
- src/SMR/Source/Lexer.hs +179/−0
- src/SMR/Source/Parsec.hs +368/−0
- src/SMR/Source/Parser.hs +351/−0
- src/SMR/Source/Pretty.hs +200/−0
- src/SMR/Source/Token.hs +65/−0
+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ shimmer.cabal view
@@ -0,0 +1,70 @@+name: shimmer+version: 0.1.1+license: MIT+license-file: LICENSE+author: Ben Lippmeier <benl@ouroborus.net>+maintainer: Ben Lippmeier <benl@ouroborus.net>+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
+ src/SMR/CLI/Config.hs view
@@ -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." ]
+ src/SMR/CLI/Driver/Load.hs view
@@ -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"
+ src/SMR/CLI/Help.hs view
@@ -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)"+ ]+
+ src/SMR/CLI/Repl.hs view
@@ -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)+
+ src/SMR/Codec/Peek.hs view
@@ -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 #-}+
+ src/SMR/Codec/Poke.hs view
@@ -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 #-}+
+ src/SMR/Codec/Size.hs view
@@ -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."+
+ src/SMR/Core/Exp.hs view
@@ -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)+
+ src/SMR/Core/Exp/Base.hs view
@@ -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+
+ src/SMR/Core/Exp/Compounds.hs view
@@ -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
+ src/SMR/Core/Exp/Push.hs view
@@ -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++
+ src/SMR/Core/Exp/Train.hs view
@@ -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')+
+ src/SMR/Core/Step.hs view
@@ -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+
+ src/SMR/Core/World.hs view
@@ -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 }
+ src/SMR/Data/Bag.hs view
@@ -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)++
+ src/SMR/Data/Located.hs view
@@ -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+
+ src/SMR/Prim/Name.hs view
@@ -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
+ src/SMR/Prim/Op.hs view
@@ -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 ]
+ src/SMR/Prim/Op/Base.hs view
@@ -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))+ }+
+ src/SMR/Prim/Op/Bool.hs view
@@ -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+
+ src/SMR/Prim/Op/List.hs view
@@ -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+
+ src/SMR/Prim/Op/Match.hs view
@@ -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])+
+ src/SMR/Prim/Op/Nat.hs view
@@ -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
+ src/SMR/Prim/Op/Nom.hs view
@@ -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
+ src/SMR/Prim/Op/Sym.hs view
@@ -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
+ src/SMR/Source/Expected.hs view
@@ -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+
+ src/SMR/Source/Lexer.hs view
@@ -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+
+ src/SMR/Source/Parsec.hs view
@@ -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)++
+ src/SMR/Source/Parser.hs view
@@ -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 ()+
+ src/SMR/Source/Pretty.hs view
@@ -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++
+ src/SMR/Source/Token.hs view
@@ -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++