aboutsummaryrefslogtreecommitdiffhomepage
path: root/src
diff options
context:
space:
mode:
authorMarvin Borner2024-02-24 18:40:54 +0100
committerMarvin Borner2024-02-24 18:40:54 +0100
commit02d531a2dff18aed6ec8085c10113ac0a46b05b9 (patch)
treedb7af5225a9c67ee1ada684de57dab71332d8c3a /src
parent1f78034588a4f545fce3dcd5070b45c60d3f0bdd (diff)
Added reducer selection flag
Diffstat (limited to 'src')
-rw-r--r--src/Eval.hs4
-rw-r--r--src/Helper.hs3
-rw-r--r--src/Optimizer.hs2
-rw-r--r--src/Reducer.hs117
-rw-r--r--src/Reducer/ION.hs9
-rw-r--r--src/Reducer/RKNL.hs117
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