diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Eval.hs | 4 | ||||
| -rw-r--r-- | src/Helper.hs | 3 | ||||
| -rw-r--r-- | src/Optimizer.hs | 2 | ||||
| -rw-r--r-- | src/Reducer.hs | 117 | ||||
| -rw-r--r-- | src/Reducer/ION.hs | 9 | ||||
| -rw-r--r-- | src/Reducer/RKNL.hs | 117 |
6 files changed, 141 insertions, 111 deletions
diff --git a/src/Eval.hs b/src/Eval.hs index 097613f..cc7fdfa 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -277,8 +277,8 @@ evalCommand inp s@(EnvState env@(Environment envDefs) conf cache) = \case print (ContextualError err $ Context inp $ _nicePath conf) >> pure s Right (Test e1' e2') -> do - lhs <- reduce e1' - rhs <- reduce e2' + lhs <- reduce conf e1' + rhs <- reduce conf e2' when (lhs /= rhs) (print $ FailedTest e1 e2 lhs rhs) >> pure s _ -> pure s | otherwise diff --git a/src/Helper.hs b/src/Helper.hs index 50d8b95..fbb7dd8 100644 --- a/src/Helper.hs +++ b/src/Helper.hs @@ -175,6 +175,7 @@ data Args = Args { _argMode :: ArgMode , _argNoTests :: Bool , _argOptimizeTarget :: String + , _argReducer :: String , _argPath :: Maybe String } @@ -185,6 +186,7 @@ data EvalConf = EvalConf , _path :: String , _evalPaths :: [String] , _optimizeTarget :: String + , _reducer :: String } newtype ExpFlags = ExpFlags @@ -215,6 +217,7 @@ argsToConf args = EvalConf { _isRepl = isNothing $ _argPath args , _nicePath = path , _evalPaths = [] , _optimizeTarget = _argOptimizeTarget args + , _reducer = _argReducer args } where path = fromMaybe "" (_argPath args) diff --git a/src/Optimizer.hs b/src/Optimizer.hs index 2744b8f..260c149 100644 --- a/src/Optimizer.hs +++ b/src/Optimizer.hs @@ -83,4 +83,4 @@ optimizeToTarget conf e = do Right res -> return $ toExpression target res optimizedReduce :: EvalConf -> Expression -> IO Expression -optimizedReduce conf e = optimizeToTarget conf e >>= reduce +optimizedReduce conf e = optimizeToTarget conf e >>= reduce conf diff --git a/src/Reducer.hs b/src/Reducer.hs index 820cc04..3be8306 100644 --- a/src/Reducer.hs +++ b/src/Reducer.hs @@ -1,117 +1,18 @@ --- MIT License, Copyright (c) 2023 Marvin Borner --- based on the RKNL abstract machine +-- MIT License, Copyright (c) 2024 Marvin Borner module Reducer ( reduce , unsafeReduce ) where -import Control.Concurrent.MVar -import Data.List ( elemIndex ) -import Data.Map.Strict ( Map ) -import qualified Data.Map.Strict as Map -import Data.Maybe ( fromMaybe ) import Helper -import System.IO.Unsafe ( unsafePerformIO ) -- TODO: AAH +import qualified Reducer.ION as ION +import qualified Reducer.RKNL as RKNL -type Store = Map Int Box -type Stack = [Redex] +reduce :: EvalConf -> Expression -> IO Expression +reduce conf e = case _reducer conf of + "RKNL" -> RKNL.reduce e + "ION" -> pure $ ION.reduce e + _ -> error "Invalid reducer" -newtype NameGen = NameGen Int -data BoxValue = Todo Redex | Done Redex | Empty -newtype Box = Box (MVar BoxValue) -data Rvar = Num Int | Hole -data Redex = Rabs Int Redex | Rapp Redex Redex | Rvar Rvar | Rclosure Redex Store | Rcache Box Redex -data Conf = Econf NameGen Redex Store Stack | Cconf NameGen Stack Redex | End - -nextName :: NameGen -> (Int, NameGen) -nextName (NameGen x) = (x, NameGen $ x + 1) - -toRedex :: Expression -> Redex -toRedex = convertWorker (NameGen 1) [] - where - convertWorker g ns (Abstraction e) = - let (v, g') = nextName g - t = convertWorker g' (v : ns) e - in Rabs v t - convertWorker g ns (Application l r) = - let lhs = convertWorker g ns l - rhs = convertWorker g ns r - in Rapp lhs rhs - convertWorker _ ns (Bruijn i) = - Rvar $ Num (if i < 0 || i >= length ns then i else ns !! i) - convertWorker g ns (Unquote e) = convertWorker g ns e - convertWorker _ _ _ = invalidProgramState - -fromRedex :: Redex -> Expression -fromRedex = convertWorker [] - where - convertWorker es (Rabs n e) = Abstraction $ convertWorker (n : es) e - convertWorker es (Rapp l r) = - let lhs = convertWorker es l - rhs = convertWorker es r - in Application lhs rhs - convertWorker es (Rvar (Num n)) = Bruijn $ fromMaybe n (elemIndex n es) - convertWorker _ _ = invalidProgramState - -transition :: Conf -> IO Conf -transition (Econf g (Rapp u v) e s) = - pure $ Econf g u e (Rapp (Rvar Hole) (Rclosure v e) : s) -transition (Econf g (Rabs x t) e s) = do - box <- newMVar Empty - pure $ Cconf g s (Rcache (Box box) (Rclosure (Rabs x t) e)) -transition (Econf g (Rvar (Num x)) e s) = do - def <- newMVar $ Done $ Rvar $ Num x - let b@(Box m) = Map.findWithDefault (Box def) x e - rd <- readMVar m - case rd of - Todo (Rclosure v e') -> pure $ Econf g v e' (Rcache b (Rvar Hole) : s) - Done t -> pure $ Cconf g s t - _ -> invalidProgramState -transition (Cconf g ((Rcache (Box m) (Rvar Hole)) : s) t) = do - modifyMVar_ m (\_ -> pure $ Done t) - pure $ Cconf g s t -transition (Cconf g ((Rapp (Rvar Hole) ve) : s) (Rcache _ (Rclosure (Rabs x t) e))) - = do - box <- newMVar (Todo ve) - pure $ Econf g t (Map.insert x (Box box) e) s -transition (Cconf g s (Rcache (Box m) (Rclosure (Rabs x t) e))) = do - rd <- readMVar m - case rd of - Done v -> pure $ Cconf g s v - Empty -> do - let (x1, g') = nextName g - box <- newMVar $ Done $ Rvar $ Num x1 - pure $ Econf g' - t - (Map.insert x (Box box) e) - (Rabs x1 (Rvar Hole) : Rcache (Box m) (Rvar Hole) : s) - Todo _ -> invalidProgramState -transition (Cconf g ((Rapp (Rvar Hole) (Rclosure v e)) : s) t) = - pure $ Econf g v e (Rapp t (Rvar Hole) : s) -transition (Cconf g ((Rapp t (Rvar Hole)) : s) v) = pure $ Cconf g s (Rapp t v) -transition (Cconf g ((Rabs x1 (Rvar Hole)) : s) v) = - pure $ Cconf g s (Rabs x1 v) -transition (Cconf _ [] _) = pure End -transition _ = invalidProgramState - -forEachState :: Conf -> (Conf -> IO Conf) -> IO Conf -forEachState conf trans = trans conf >>= \case - End -> pure conf - next -> forEachState next trans - --- TODO: NameGen is arbitrary to not conflict with toRedex -loadTerm :: Redex -> Conf -loadTerm t = Econf (NameGen 1000000) t Map.empty [] - -reduce :: Expression -> IO Expression -reduce e = do - let redex = toRedex e - forEachState (loadTerm redex) transition >>= \case - Cconf _ [] v -> pure $ fromRedex v - _ -> invalidProgramState - --- TODO: AAAAAAAAAAAAAAAAH remove this --- (probably not thaaat bad) -{-# NOINLINE unsafeReduce #-} unsafeReduce :: Expression -> Expression -unsafeReduce = unsafePerformIO . reduce +unsafeReduce = RKNL.unsafeReduce diff --git a/src/Reducer/ION.hs b/src/Reducer/ION.hs new file mode 100644 index 0000000..1a27605 --- /dev/null +++ b/src/Reducer/ION.hs @@ -0,0 +1,9 @@ +-- MIT License, Copyright (c) 2024 Marvin Borner +module Reducer.ION + ( reduce + ) where + +import Helper + +reduce :: Expression -> Expression +reduce e = e diff --git a/src/Reducer/RKNL.hs b/src/Reducer/RKNL.hs new file mode 100644 index 0000000..9513e38 --- /dev/null +++ b/src/Reducer/RKNL.hs @@ -0,0 +1,117 @@ +-- MIT License, Copyright (c) 2023 Marvin Borner +-- based on the RKNL abstract machine +module Reducer.RKNL + ( reduce + , unsafeReduce + ) where + +import Control.Concurrent.MVar +import Data.List ( elemIndex ) +import Data.Map.Strict ( Map ) +import qualified Data.Map.Strict as Map +import Data.Maybe ( fromMaybe ) +import Helper +import System.IO.Unsafe ( unsafePerformIO ) -- TODO: AAH + +type Store = Map Int Box +type Stack = [Redex] + +newtype NameGen = NameGen Int +data BoxValue = Todo Redex | Done Redex | Empty +newtype Box = Box (MVar BoxValue) +data Rvar = Num Int | Hole +data Redex = Rabs Int Redex | Rapp Redex Redex | Rvar Rvar | Rclosure Redex Store | Rcache Box Redex +data Conf = Econf NameGen Redex Store Stack | Cconf NameGen Stack Redex | End + +nextName :: NameGen -> (Int, NameGen) +nextName (NameGen x) = (x, NameGen $ x + 1) + +toRedex :: Expression -> Redex +toRedex = convertWorker (NameGen 1) [] + where + convertWorker g ns (Abstraction e) = + let (v, g') = nextName g + t = convertWorker g' (v : ns) e + in Rabs v t + convertWorker g ns (Application l r) = + let lhs = convertWorker g ns l + rhs = convertWorker g ns r + in Rapp lhs rhs + convertWorker _ ns (Bruijn i) = + Rvar $ Num (if i < 0 || i >= length ns then i else ns !! i) + convertWorker g ns (Unquote e) = convertWorker g ns e + convertWorker _ _ _ = invalidProgramState + +fromRedex :: Redex -> Expression +fromRedex = convertWorker [] + where + convertWorker es (Rabs n e) = Abstraction $ convertWorker (n : es) e + convertWorker es (Rapp l r) = + let lhs = convertWorker es l + rhs = convertWorker es r + in Application lhs rhs + convertWorker es (Rvar (Num n)) = Bruijn $ fromMaybe n (elemIndex n es) + convertWorker _ _ = invalidProgramState + +transition :: Conf -> IO Conf +transition (Econf g (Rapp u v) e s) = + pure $ Econf g u e (Rapp (Rvar Hole) (Rclosure v e) : s) +transition (Econf g (Rabs x t) e s) = do + box <- newMVar Empty + pure $ Cconf g s (Rcache (Box box) (Rclosure (Rabs x t) e)) +transition (Econf g (Rvar (Num x)) e s) = do + def <- newMVar $ Done $ Rvar $ Num x + let b@(Box m) = Map.findWithDefault (Box def) x e + rd <- readMVar m + case rd of + Todo (Rclosure v e') -> pure $ Econf g v e' (Rcache b (Rvar Hole) : s) + Done t -> pure $ Cconf g s t + _ -> invalidProgramState +transition (Cconf g ((Rcache (Box m) (Rvar Hole)) : s) t) = do + modifyMVar_ m (\_ -> pure $ Done t) + pure $ Cconf g s t +transition (Cconf g ((Rapp (Rvar Hole) ve) : s) (Rcache _ (Rclosure (Rabs x t) e))) + = do + box <- newMVar (Todo ve) + pure $ Econf g t (Map.insert x (Box box) e) s +transition (Cconf g s (Rcache (Box m) (Rclosure (Rabs x t) e))) = do + rd <- readMVar m + case rd of + Done v -> pure $ Cconf g s v + Empty -> do + let (x1, g') = nextName g + box <- newMVar $ Done $ Rvar $ Num x1 + pure $ Econf g' + t + (Map.insert x (Box box) e) + (Rabs x1 (Rvar Hole) : Rcache (Box m) (Rvar Hole) : s) + Todo _ -> invalidProgramState +transition (Cconf g ((Rapp (Rvar Hole) (Rclosure v e)) : s) t) = + pure $ Econf g v e (Rapp t (Rvar Hole) : s) +transition (Cconf g ((Rapp t (Rvar Hole)) : s) v) = pure $ Cconf g s (Rapp t v) +transition (Cconf g ((Rabs x1 (Rvar Hole)) : s) v) = + pure $ Cconf g s (Rabs x1 v) +transition (Cconf _ [] _) = pure End +transition _ = invalidProgramState + +forEachState :: Conf -> (Conf -> IO Conf) -> IO Conf +forEachState conf trans = trans conf >>= \case + End -> pure conf + next -> forEachState next trans + +-- TODO: NameGen is arbitrary to not conflict with toRedex +loadTerm :: Redex -> Conf +loadTerm t = Econf (NameGen 1000000) t Map.empty [] + +reduce :: Expression -> IO Expression +reduce e = do + let redex = toRedex e + forEachState (loadTerm redex) transition >>= \case + Cconf _ [] v -> pure $ fromRedex v + _ -> invalidProgramState + +-- TODO: AAAAAAAAAAAAAAAAH remove this +-- (probably not thaaat bad) +{-# NOINLINE unsafeReduce #-} +unsafeReduce :: Expression -> Expression +unsafeReduce = unsafePerformIO . reduce |