Prepare direct inductive kernel proofs

1 files changed, 73 insertions, 0 deletions

diff --git a/source/Test/Unit/Kernel.hs b/source/Test/Unit/Kernel.hs
index 1cc481a..c8ed786 100644
--- a/source/Test/Unit/Kernel.hs
+++ b/source/Test/Unit/Kernel.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE PatternSynonyms #-}
 
 module Test.Unit.Kernel (unitTests) where
 
@@ -8,6 +9,10 @@ import Checking.Foundation qualified as Foundation
 import Checking.Kernel.Derivation
 import Checking.Kernel.Semantics qualified as Semantics
 import Checking.Kernel.SetLfp qualified as SetLfp
+import Checking.Transition (checkedGlobalType)
+import Checking.Typed.Inductive qualified as Inductive
+import Report.Location (pattern Nowhere)
+import Syntax.Internal qualified as Internal
 
 import Data.Set qualified as Set
 import Data.Vector qualified as Vector
@@ -37,6 +42,9 @@ unitTests =
             "checks and replays the exact set fixed-point rules"
             checksSetLfpRules
         , testCase
+            "replays direct inductive facts"
+            replaysDirectInductiveFacts
+        , testCase
             "rejects altered set fixed-point applications"
             rejectsAlteredSetLfpApplications
         , testCase
@@ -413,6 +421,71 @@ checksSetLfpRules = do
         (Set.singleton Foundation.SetLfpBound)
         (replayedKernelRuleUses replayed)
 
+replaysDirectInductiveFacts :: Assertion
+replaysDirectInductiveFacts = do
+    foundation <-
+        expectRight Foundation.checkedFoundation
+    traverse_
+        (replayInductive foundation)
+        [ Inductive.DirectInductive
+            []
+            (Internal.EmptySet Nowhere)
+            (Inductive.DirectInductiveClause
+                []
+                []
+                (Internal.EmptySet Nowhere)
+                :| [])
+        , let x = Internal.NamedVar "x"
+          in Inductive.DirectInductive
+                []
+                (Internal.EmptySet Nowhere)
+                ( Inductive.DirectInductiveClause
+                    []
+                    []
+                    (Internal.EmptySet Nowhere)
+                :| [ Inductive.DirectInductiveClause
+                        [x]
+                        [Inductive.DirectRecursiveCondition
+                            (Internal.TermVar x)]
+                        (Internal.TermVar x)
+                   ]
+                )
+        ]
+  where
+    replayInductive foundation inductive = do
+        prepared <-
+            expectRight
+                (Inductive.prepareTypedInductive
+                    foundation
+                    (const Nothing)
+                    (Internal.Marker "direct_inductive")
+                    inductive)
+        imports <-
+            traverse
+                (expectRight . derivationImportJudgment)
+                (Inductive.typedInductiveGuardTargets
+                    prepared)
+        traverse_
+            (\fact -> do
+                replayed <-
+                    expectRight
+                        (replayKernelDerivation
+                            foundation
+                            defaultKernelReplayLimits
+                            (Just . checkedGlobalType)
+                            imports
+                            (Inductive.typedInductiveFactTarget
+                                fact)
+                            (Inductive.typedInductiveFactDerivation
+                                fact))
+                assertEqual
+                    "replay target"
+                    (Inductive.typedInductiveFactTarget
+                        fact)
+                    (replayedKernelTarget replayed))
+            (Inductive.typedInductiveFacts
+                prepared)
+
 rejectsAlteredSetLfpApplications :: Assertion
 rejectsAlteredSetLfpApplications = do
     foundation <-