Reset tooling gloss state per module

2 files changed, 41 insertions, 38 deletions

diff --git a/source/Api.hs b/source/Api.hs
index 42ec4b0..8f7bd5b 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -63,8 +63,6 @@ import Felix.Source
 import Filter(filterTask)
 import Meaning
     ( GlossError(..)
-    , glossStep
-    , initialGlossState
     , meaning
     )
 import Provers
@@ -169,12 +167,6 @@ parse file = do
     result <- liftIO (parseDefaultWorkspace file)
     Felix.importedBeforeImporterBlocks <$> either throwWorkspaceError pure result
 
-parseWith :: MonadIO io => FilePath -> (Raw.Block -> IO ()) -> io ()
-parseWith file emitBlock = do
-    result <- liftIO
-        (parseDefaultWorkspaceWith file (\_source block -> emitBlock block))
-    void (either throwWorkspaceError pure result)
-
 parseDefaultWorkspace
     :: FilePath
     -> IO (Either ParseWorkspaceError ParsedSourceWorkspace)
@@ -186,18 +178,6 @@ parseDefaultWorkspace file = do
         Right (mounts, request) ->
             Felix.parseSourceWorkspace mounts request
 
-parseDefaultWorkspaceWith
-    :: FilePath
-    -> (ResolvedSource -> Raw.Block -> IO ())
-    -> IO (Either ParseWorkspaceError ParsedSourceWorkspace)
-parseDefaultWorkspaceWith file emitBlock = do
-    prepared <- prepareDefaultSourceRequest file
-    case prepared of
-        Left err ->
-            pure (Left err)
-        Right (mounts, request) ->
-            Felix.parseSourceWorkspaceWith mounts request emitBlock
-
 prepareDefaultSourceRequest
     :: FilePath
     -> IO (Either ParseWorkspaceError (SourceMounts, RootRequest))
@@ -252,26 +232,19 @@ throwWorkspaceError = \case
 simpleStream :: TokStream -> [[Token]]
 simpleStream TokStream{unTokStream=chunks} = [unLocated <$> ch | ch <- chunks]
 
--- | gloss generates internal represantation of the LaTeX files.
--- First the file will be parsed and therefore checkt for grammer.
--- 'meaning' then transfer the raw parsed grammer to the internal semantics.
+-- | Parse the workspace, then gloss each module independently in
+-- imported-before-importer order.
 gloss :: MonadIO io => FilePath -> io [Internal.Block]
 gloss file = do
-    blocksRef <- liftIO (newIORef [])
-    glossWith file (\block -> modifyIORef' blocksRef (block :))
-    reverse <$> liftIO (readIORef blocksRef)
-
-glossWith :: MonadIO io => FilePath -> (Internal.Block -> IO ()) -> io ()
-glossWith file emitBlock = do
-    glossStateRef <- liftIO (newIORef initialGlossState)
-    parseWith file \rawBlock -> do
-        glossState <- readIORef glossStateRef
-        case glossStep glossState rawBlock of
-            Left err ->
-                throwIO err
-            Right (glossedBlock, nextGlossState) -> do
-                writeIORef glossStateRef nextGlossState
-                emitBlock glossedBlock
+    result <- liftIO (parseDefaultWorkspace file)
+    workspace <- either throwWorkspaceError pure result
+    liftIO
+        (concat
+            <$> traverse
+                (glossModule . Felix.parsedModuleBlocks)
+                (toList
+                    (Felix.parsedWorkspaceImportedBeforeImporter
+                        workspace)))
 
 
 generateTasks :: (MonadIO io, MonadReader Options io) => FilePath -> io [Internal.Task]
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index 2872d2b..7e8f6f4 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -17,8 +17,11 @@ import Felix.Source
 import Felix.Source.Content qualified as Content
 import Report.Location
 import Provers qualified
+import Syntax.Internal qualified as Internal
 import Syntax.Interface qualified as Syntax
 
+import Bound.Scope (fromScope)
+import Bound.Var (Var(..))
 import Data.ByteString qualified as ByteString
 import Data.Text.Encoding qualified as Text
 import Control.Exception (try)
@@ -39,6 +42,8 @@ unitTests =
             identifiesCommentOnlyInput
         , testCase "coalesces syntax without collapsing semantic imports"
             coalescesSharedDirectSyntax
+        , testCase "resets gloss state between modules"
+            resetsGlossStatePerModule
         , testCase "makes selected unsupported syntax terminal"
             rejectsUnsupportedTypedSource
         , testCase "routes production verification by complete graph"
@@ -247,6 +252,31 @@ coalescesSharedDirectSyntax = do
                 assertFailure "empty typed module did not seal"
                     >> fail "unreachable"
 
+resetsGlossStatePerModule :: Assertion
+resetsGlossStatePerModule = do
+    blocks <- Api.gloss "test/phase3/gloss-root.tex"
+    binders <- traverse signatureBinder blocks
+    assertEqual "fresh variables restart at each module boundary"
+        [Internal.FreshVar 0, Internal.FreshVar 0, Internal.FreshVar 1]
+        binders
+  where
+    signatureBinder = \case
+        Internal.BlockSig
+                _location
+                _marker
+                _assumptions
+                (Internal.SignatureFormula
+                    (Internal.Quantified Internal.Universally scope)) ->
+            case nubOrd [binder | B binder <- toList (fromScope scope)] of
+                [binder] -> pure binder
+                binders ->
+                    assertFailure
+                        ("unexpected signature binders: " <> show binders)
+                        >> fail "unreachable"
+        block ->
+            assertFailure ("unexpected glossed block: " <> show block)
+                >> fail "unreachable"
+
 rejectsUnsupportedTypedSource :: Assertion
 rejectsUnsupportedTypedSource = do
     result <-