Reset tooling gloss state per module

1 files changed, 30 insertions, 0 deletions

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 <-