From a5fdcebddee2eec50b03c993081ce9b91a59cbe0 Mon Sep 17 00:00:00 2001
From: Christian Gram Kalhauge <chrg@dtu.dk>
Date: Thu, 29 Feb 2024 10:06:18 +0100
Subject: [PATCH] Add fixpoint mode
---
rtree-c/bin/Main.hs | 34 +++++++++++++++++++++++++---------
1 file changed, 25 insertions(+), 9 deletions(-)
diff --git a/rtree-c/bin/Main.hs b/rtree-c/bin/Main.hs
index 2d189de..aad22c6 100644
--- a/rtree-c/bin/Main.hs
+++ b/rtree-c/bin/Main.hs
@@ -14,6 +14,7 @@ import Control.Monad
import Control.Monad.IRTree qualified as RPath
import Control.Monad.State
import Data.Foldable
+import Data.Function
import Data.Functor
import Data.Text qualified as Text
import Data.Time (getCurrentTime)
@@ -74,6 +75,14 @@ run = do
, help "check every output for validity"
]
+ fixpoint <-
+ flag False True $
+ fold
+ [ long "fixpoint"
+ , short 'F'
+ , help "run the computation to a fixpoint"
+ ]
+
pedandic <-
flag False True $
fold
@@ -195,19 +204,26 @@ run = do
liftIO exitSuccess
l <-
- (if expmode then IRTree.reduceExp else IRTree.reduce)
- (check' file)
- (ReduceC.defaultReduceC c)
+ c & fix \rec prevc -> do
+ mc' <-
+ (if expmode then IRTree.reduceExp else IRTree.reduce)
+ (check' file)
+ (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
liftIO $ copyFile file (file <.> "last")
- case l of
- Just l' ->
- output file l'
- Nothing -> do
- logError "Was unable to produce any output"
- cleanup file
+ output file l
where
parseCFile file = do
res <- liftIO $ C.parseCFilePre file
--
GitLab