From 0c004688c7c8f8855d5be5732482a9bb447c948c Mon Sep 17 00:00:00 2001
From: William Ball <williampi103@gmail.com>
Date: Fri, 29 Nov 2024 20:39:42 -0800
Subject: [PATCH] made preprocessor not reinclude files multiple times

---
 examples/peano.pg   |  6 +-----
 lib/Parser.hs       |  4 +---
 lib/Preprocessor.hs | 35 ++++++++++++++++++++++-------------
 3 files changed, 24 insertions(+), 21 deletions(-)

diff --git a/examples/peano.pg b/examples/peano.pg
index 9f95907..6aa899c 100644
--- a/examples/peano.pg
+++ b/examples/peano.pg
@@ -3,15 +3,11 @@
 -- import basic logic definitions from <logic.pg>
 
 @include logic.pg
-
-binop (A : *) := A -> A -> A;
+@include algebra.pg
 
 comp (A B C : *) (g : B -> C) (f : A -> B) (x : A) : C :=
   g (f x);
 
-assoc (A : *) (op : binop A) := forall (c a b : A),
-  eq A (op a (op b c)) (op (op a b) c);
-
 -- }}}
 
 -- {{{ Axioms
diff --git a/lib/Parser.hs b/lib/Parser.hs
index c4d5c44..8297d26 100644
--- a/lib/Parser.hs
+++ b/lib/Parser.hs
@@ -236,6 +236,4 @@ parseProgram :: Env -> Text -> Either String Env
 parseProgram initial input = first errorBundlePretty $ evalState (runParserT pProgram "" input) $ emptyBinders initial
 
 handleFile :: Env -> String -> ExceptT String IO Env
-handleFile initial filename = do
-    text <- toString `withExceptT` preprocess filename
-    liftEither $ parseProgram initial text
+handleFile initial filename = (toString `withExceptT` runPreprocessor filename) >>= liftEither . parseProgram initial
diff --git a/lib/Preprocessor.hs b/lib/Preprocessor.hs
index 4b1db6e..4517d8d 100644
--- a/lib/Preprocessor.hs
+++ b/lib/Preprocessor.hs
@@ -1,6 +1,6 @@
 module Preprocessor where
 
-import Control.Monad.Except
+import qualified Data.Set as S
 import qualified Data.Text as T
 import System.FilePath
 
@@ -13,23 +13,32 @@ instance ToString PreprocessorError where
     toString = toString . toText
 
 type Result = Either PreprocessorError
-type ResultIO = ExceptT PreprocessorError IO
+type ResultStateIO = ExceptT PreprocessorError (StateT (S.Set FilePath) IO)
 
-concatMapM :: (Applicative f) => (a -> f Text) -> [a] -> f Text
-concatMapM _ [] = pure mempty
-concatMapM f (x : xs) = ((<>) . (<> "\n") <$> f x) <*> concatMapM f xs
+-- There's a clever way to do this with `foldM` or something, but I think this is still pretty elegant
+handleLines :: FilePath -> [Text] -> ResultStateIO Text
+handleLines _ [] = pure ""
+handleLines filename (line : rest) = do
+    line' <- preprocessLine (takeDirectory filename) line
+    rest' <- handleLines filename rest
+    pure $ line' <> "\n" <> rest'
 
-preprocess :: String -> ResultIO Text
-preprocess filename = do
-    text <- decodeUtf8With lenientDecode <$> readFileBS filename
-    result <- concatMapM (preprocessLine $ takeDirectory filename) (lines text)
-    putStrLn $ "loading: " ++ filename
-    pure result
+preprocess :: String -> ResultStateIO Text
+preprocess filename =
+    ifM (gets $ S.member filename) (pure "") $ do
+        modify $ S.insert filename
+        text <- decodeUtf8With lenientDecode <$> readFileBS filename
+        result <- handleLines filename $ lines text
+        putStrLn $ "loading: " ++ filename
+        pure result
 
 parseInclude :: Text -> Result Text
 parseInclude line = maybeToRight (ParseError line) $ T.stripPrefix "@include " line
 
-preprocessLine :: FilePath -> Text -> ResultIO Text
+preprocessLine :: FilePath -> Text -> ResultStateIO Text
 preprocessLine base line
-    | "@include " `T.isPrefixOf` line = liftEither (parseInclude line) >>= preprocess . normalise . (base </>) . toString
+    | "@include " `T.isPrefixOf` line = preprocess $ normalise $ base </> toString (fromRight "" $ parseInclude line)
     | otherwise = pure line
+
+runPreprocessor :: String -> ExceptT PreprocessorError IO Text
+runPreprocessor filename = liftIO (evalStateT (runExceptT (preprocess filename)) S.empty) >>= hoistEither