Skip to content
Snippets Groups Projects
Commit a5fdcebd authored by chrg's avatar chrg
Browse files

Add fixpoint mode

parent 41054fe5
No related branches found
No related tags found
No related merge requests found
...@@ -14,6 +14,7 @@ import Control.Monad ...@@ -14,6 +14,7 @@ import Control.Monad
import Control.Monad.IRTree qualified as RPath import Control.Monad.IRTree qualified as RPath
import Control.Monad.State import Control.Monad.State
import Data.Foldable import Data.Foldable
import Data.Function
import Data.Functor import Data.Functor
import Data.Text qualified as Text import Data.Text qualified as Text
import Data.Time (getCurrentTime) import Data.Time (getCurrentTime)
...@@ -74,6 +75,14 @@ run = do ...@@ -74,6 +75,14 @@ run = do
, help "check every output for validity" , help "check every output for validity"
] ]
fixpoint <-
flag False True $
fold
[ long "fixpoint"
, short 'F'
, help "run the computation to a fixpoint"
]
pedandic <- pedandic <-
flag False True $ flag False True $
fold fold
...@@ -195,19 +204,26 @@ run = do ...@@ -195,19 +204,26 @@ run = do
liftIO exitSuccess liftIO exitSuccess
l <- l <-
c & fix \rec prevc -> do
mc' <-
(if expmode then IRTree.reduceExp else IRTree.reduce) (if expmode then IRTree.reduceExp else IRTree.reduce)
(check' file) (check' file)
(ReduceC.defaultReduceC c) (ReduceC.defaultReduceC prevc)
case mc' of
Just c' ->
if fixpoint && c' /= c
then do
logInfo "Running again until fixpoint"
rec c'
else pure c'
Nothing -> do
logError "Was unable to produce any output"
cleanup file
when pedandic do when pedandic do
liftIO $ copyFile file (file <.> "last") liftIO $ copyFile file (file <.> "last")
case l of output file l
Just l' ->
output file l'
Nothing -> do
logError "Was unable to produce any output"
cleanup file
where where
parseCFile file = do parseCFile file = do
res <- liftIO $ C.parseCFilePre file res <- liftIO $ C.parseCFilePre file
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment