phino-0.0.164: test/MorphSpec.hs
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT
module MorphSpec (spec) where
import AST
import Control.Exception (SomeException)
import Control.Monad
import Data.Aeson (FromJSON)
import Data.IORef (modifyIORef', newIORef, readIORef)
import Data.List (find, isInfixOf, nub)
import Data.List.NonEmpty (NonEmpty (..))
import Data.Maybe (fromMaybe)
import Data.Text qualified as T
import Data.Yaml qualified as Decode
import Dataize (Outcome (..), dataize)
import Deps (Acyclic (..), Evaluation (EvLooped, EvMorphed, EvRecalled, EvWorld), Judgment (..), State, Term (TeExpression))
import Engine (Engine (_normal))
import Files (allPathsIn)
import Fixtures (defaultReduceContext, fixtureLambdas, linked, overdue, primitives)
import GHC.Clock (getMonotonicTime)
import GHC.Generics (Generic)
import Inference (Conclusion (Answered), Premises (Concludes, Morphs), direct)
import Lambdas (Lambdas, emptyLambdas)
import Matcher (substEmpty)
import Morph (Deadline (..), ReduceContext (..), declared, emptyState, enter, execBuildTerm, factual, fired, inferred, insideUniverse, morph, morph', noted, voided)
import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows')
import Rewriter (Rewritten)
import Rule (RuleContext (RuleContext), matchExpressionWithRule')
import System.FilePath (makeRelative)
import System.Timeout (timeout)
import Tau (seedTaus)
import Test.Hspec
import Yaml (ExtraArgument (..))
import Yaml qualified
test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> State -> ReduceContext -> IO ((a, NonEmpty Rewritten), State)) -> [(String, Expression, Expression, a)] -> Spec
test' func useCases =
forM_ useCases $ \(desc, input, expr, output) ->
it desc $ do
((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState =<< defaultReduceContext ExRoot
res `shouldBe` output
data MorphPack = MorphPack
{ location :: Maybe String
, input :: String
, model :: Maybe Bool
, symbolic :: Maybe Bool
, partial :: Maybe Bool
, result :: Maybe String
, fails :: Maybe String
}
deriving (Generic, Show, FromJSON)
testMorph :: Lambdas -> FilePath -> Expectation
testMorph known pth = do
MorphPack{..} <- Decode.decodeFileThrow pth
expr <- parseExpressionThrows' MONOFORM (if model == Just True then primitives input else input)
seedTaus expr
loc <- parseExpressionThrows' MONOFORM (fromMaybe "Q" location)
base <- defaultReduceContext loc
let ctx =
base
{ _partial = partial == Just True
, _symbolic = if symbolic == Just True then known else emptyLambdas
}
case (result, fails) of
(Just res, Nothing) -> do
expected <- parseExpressionThrows' MONOFORM res
(morphed, _, _) <- morph expr emptyState ctx
morphed `shouldBe` expected
(Nothing, Just message) ->
morph expr emptyState ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException))
_ -> expectationFailure "The pack holds neither a single 'result' nor a single 'fails'"
spec :: Spec
spec = do
known <- runIO fixtureLambdas
describe "morph" $ do
let resources = "test-resources/morph-packs"
packs <- runIO (allPathsIn resources)
forM_ packs (\pth -> it (makeRelative resources pth) (testMorph known pth))
it "reports the chain of steps oldest first" $ do
expr <- parseExpressionThrows "[[ D> 00- ]]"
(morphed, chain, _) <- morph expr emptyState =<< defaultReduceContext ExRoot
morphed `shouldBe` expr
map snd chain `shouldBe` [Just (Morphing, "mf"), Nothing]
map fst chain `shouldBe` [expr, expr]
it "resolves Φ to the world it has already normalized" $ do
expr <- parseExpressionThrows "[[ w -> [[ k -> [[ ]] ]].k, y -> Q.w ]]"
loc <- parseExpressionThrows "Q.y"
saved <- newIORef (0 :: Int)
ctx <- defaultReduceContext loc
_ <- morph expr emptyState ctx{_saveStep = const (modifyIORef' saved (+ 1))}
readIORef saved `shouldReturn` 2
it "tells the protocol the world it has normalized" $ do
expr <- parseExpressionThrows "[[ ezh -> [[ D> 0E- ]] ]]"
told <- newIORef []
ctx <- defaultReduceContext ExRoot
_ <- morph expr emptyState ctx{_saveEval = \record -> modifyIORef' told (record :)}
records <- readIORef told
[world | EvWorld world <- records] `shouldBe` [expr]
it "tells the protocol the term it came to as its last record" $ do
expr <- parseExpressionThrows "[[ wz -> [[ kq -> [[ D> 1F- ]] ]], y -> Q.wz.kq ]]"
loc <- parseExpressionThrows "Q.y"
told <- newIORef []
ctx <- defaultReduceContext loc
(morphed, _, _) <- morph expr emptyState ctx{_saveEval = \record -> modifyIORef' told (record :)}
records <- readIORef told
[term | EvMorphed _ term <- take 1 records] `shouldBe` [morphed]
it "tells the protocol nothing of the premises it morphed inside its own block" $ do
expr <- parseExpressionThrows "[[ ox -> [[ ty -> [[ gu -> [[ D> 2A- ]] ]] ]], y -> Q.ox.ty.gu ]]"
loc <- parseExpressionThrows "Q.y"
told <- newIORef []
ctx <- defaultReduceContext loc
_ <- morph expr emptyState ctx{_saveEval = \record -> modifyIORef' told (record :)}
records <- readIORef told
length [term | EvMorphed _ term <- records] `shouldBe` 1
describe "morph'" $
test'
morph'
[ ("[[ D> 00- ]] => [[ D> 00- ]]", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")])
, ("T => T", ExTermination, ExRoot, ExTermination)
, ("$ => X", ExXi, ExRoot, ExTermination)
, ("Q => X", ExRoot, ExRoot, ExTermination)
,
( "Q.x (Q -> [[ x -> [[]] ]]) => [[]]"
, ExDispatch ExRoot (AtLabel "x")
, ExFormation [BiTau (AtLabel "x") (ExFormation [])]
, ExFormation []
)
,
( "Q.x (Q -> [[ x -> [[ ^ -> ? ]] ]]) => [[ ρ -> Q ]]"
, ExDispatch ExRoot (AtLabel "x")
, ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho])]
, ExFormation [BiTau AtRho ExRoot]
)
,
( "[[ x -> ? ]](x -> $.foo) => T"
, ExApplication (ExFormation [BiVoid (AtLabel "x")]) (ArTau (AtLabel "x") (ExDispatch ExXi (AtLabel "foo")))
, ExRoot
, ExTermination
)
,
( "[[ ^ -> ? ]](α0 -> $.foo) => T"
, ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) (ExDispatch ExXi (AtLabel "foo")))
, ExRoot
, ExTermination
)
,
( "Q => [[]] (a universe distinct from Φ) => [[]]"
, ExRoot
, ExFormation []
, ExFormation []
)
]
describe "inferred" $
it "morphs a premise in the universe it names, not in the one the frame is in" $ do
world <- parseExpressionThrows "[[ x -> [[ ]] ]]"
ctx <- defaultReduceContext ExRoot
Just (Answered _ answer, _) <-
inferred
ExRoot
ExRoot
emptyState
ctx
[direct (\_ _ -> [Morphs ExRoot world (pure . Concludes . Answered (Morphing, "premise"))])]
answer `shouldBe` world
describe "morph' fails when no morphing rule matches the term" $
it "throws instead of looping when handed a bare, unmatched meta" $
(morph' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState =<< defaultReduceContext ExRoot)
`shouldThrow` (\e -> "Morphing expects a normal form" `isInfixOf` show (e :: SomeException))
describe "execBuildTerm 'morph'" $ do
let univ = ExFormation []
it "throws when not given exactly one expression argument" $ do
ctx <- defaultReduceContext ExRoot
execBuildTerm univ ctx "morph" [] substEmpty
`shouldThrow` (\e -> "requires exactly 1 expression argument" `isInfixOf` show (e :: SomeException))
it "morphs a single expression argument to its already-normal form" $ do
ctx <- defaultReduceContext ExRoot
result <- execBuildTerm univ ctx "morph" [ArgExpression (ExFormation [BiDelta (BtOne "00")])] substEmpty
case result of
TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "00")]
_ -> expectationFailure "expected TeExpression"
describe "insideUniverse" $ do
let universe = "[[ y -> [[ D> 02- ]] ]]"
reduced src = do
univ <- parseExpressionThrows universe
target <- parseExpressionThrows src
(extended, ctx) <- insideUniverse target univ =<< defaultReduceContext ExRoot
(outcome, _, _) <- dataize extended emptyState ctx
pure outcome
it "reduces an expression the program does not contain" $ do
value <- reduced "Q.y"
value `shouldBe` Dataized (BtOne "02")
it "normalizes what it is handed before 𝔻 sees it" $ do
value <- reduced "[[ x -> [[ D> 01- ]] ]].x"
value `shouldBe` Dataized (BtOne "01")
it "keeps the site the caller names what it reduces by" $ do
univ <- parseExpressionThrows universe
target <- parseExpressionThrows "Q.y"
ctx <- defaultReduceContext ExRoot
(_, aiming) <- insideUniverse target univ ctx{_site = ExDispatch ExXi (AtLabel "ψ")}
aiming._site `shouldBe` ExDispatch ExXi (AtLabel "ψ")
it "refuses a universe which is not a formation" $ do
target <- parseExpressionThrows "Q.y"
(insideUniverse target ExRoot =<< defaultReduceContext ExRoot)
`shouldThrow` (\e -> "not a formation" `isInfixOf` show (e :: SomeException))
describe "morphing is order-independent under --shuffle" $ do
let cases =
[ ("a byte formation", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")])
, ("termination", ExTermination, ExRoot, ExTermination)
, ("xi", ExXi, ExRoot, ExTermination)
, ("the global object", ExRoot, ExRoot, ExTermination)
,
( "a dispatch over a formation"
, ExDispatch ExRoot (AtLabel "x")
, ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho])]
, ExFormation [BiTau AtRho ExRoot]
)
]
forM_ cases $ \(desc, input, univ, expected) ->
it ("morphs " ++ desc ++ " to the same form across 100 random rule orders") $ do
results <- replicateM 100 (fst . fst <$> (morph' (input, (univ, Nothing) :| []) univ emptyState =<< defaultReduceContext ExRoot))
nub results `shouldBe` [expected]
describe "morphing 'md' is disjoint from 'ml'" $ do
ctx <- runIO (defaultReduceContext ExRoot)
let rctx = RuleContext (execBuildTerm ExRoot ctx) Nothing (_normal linked)
morphRule :: String -> Yaml.MorphRule
morphRule nm = fromMaybe (error ("no morphing rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.morphingRules)
asRule :: Yaml.MorphRule -> Yaml.Rule
asRule r = Yaml.Rule r.name Nothing Nothing r.match ExRoot r.when Nothing Nothing
lambdaFormation = ExFormation [BiLambda (Function "L_dummy"), BiVoid AtRho]
it "does not fire on a λ-bearing formation dispatch" $ do
substs <- matchExpressionWithRule' [substEmpty] (ExDispatch lambdaFormation (AtLabel "x")) (asRule (morphRule "md")) rctx
substs `shouldBe` []
it "still fires on a non-λ-formation dispatch" $ do
substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (morphRule "md")) rctx
null substs `shouldBe` False
it "drills a chained λ-formation dispatch down to the base 'ml'" $ do
let base = ExFormation [BiLambda (Function "F")]
chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c")
(morph' (chain, (ExRoot, Nothing) :| []) ExRoot emptyState =<< defaultReduceContext ExRoot)
`shouldThrow` (\e -> "No entry of --symbolic answers the λ function 'F'" `isInfixOf` show (e :: SomeException))
describe "stops by the clock of --max-seconds" $ do
it "fails a morphing that fires nothing once the deadline has passed" $ do
expr <- parseExpressionThrows "[[ k -> [[ D> 3F- ]] ]]"
deadline <- overdue 17
ctx <- defaultReduceContext ExRoot
morph expr emptyState ctx{_deadline = Just deadline}
`shouldThrow` (\e -> "--max-seconds=17" `isInfixOf` show (e :: SomeException))
it "leaves a partial morphing in place once the deadline has passed" $ do
expr <- parseExpressionThrows "[[ q -> [[ D> 5A- ]] ]]"
deadline <- overdue 23
ctx <- defaultReduceContext ExRoot
(residue, _, _) <- morph expr emptyState ctx{_deadline = Just deadline, _partial = True}
residue `shouldBe` expr
describe "stops an entrance by the clock of --max-seconds" $
it "fails a comparison that outlasts the deadline" $ do
due <- (+ 0.2) <$> getMonotonicTime
let formation :: Expression -> Int -> Expression
formation base depth = ExFormation [BiTau (AtLabel "x") (iterate (`ExDispatch` AtLabel "w") base !! depth), BiTau AtPhi ExRoot]
base <- defaultReduceContext ExRoot
ctx <- enter (formation ExRoot 1300) base{_acyclic = Just Plausible, _deadline = Just (Deadline 31 due)}
timeout 10000000 (enter (formation ExXi 1700) ctx)
`shouldThrow` (\e -> "--max-seconds=31" `isInfixOf` show (e :: SomeException))
describe "names a cut by the facts however wide they are" $
it "names a cut held at the end of a wide fact long before the deadline" $ do
let looping :: Expression
looping = ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "pz"))]
wide :: Expression
wide = ExFormation ([BiTau (AtLabel (T.pack ("w" ++ show index))) (ExFormation [BiTau (AtLabel (T.pack ("v" ++ show index))) (ExFormation [BiDelta (BtOne "5C")])]) | index <- [1 :: Int .. 30000]] ++ [BiTau (AtLabel "kq") looping])
facts <- factual
told <- newIORef []
base <- defaultReduceContext ExRoot
noted base{_facts = Just facts} wide (ExDispatch ExRoot (AtLabel "cq"))
due <- (+ 2) <$> getMonotonicTime
ctx <- enter looping base{_acyclic = Just Plausible, _maxLoops = 0, _facts = Just facts, _reckoning = True, _deadline = Just (Deadline 43 due), _saveEval = \record -> modifyIORef' told (record :)}
_ <- timeout 10000000 (fired ExRoot ctx ExRoot emptyState looping)
records <- readIORef told
[answered | EvLooped _ _ _ _ _ (Just (_, answered)) <- records] `shouldBe` [Just (ExDispatch (ExDispatch ExRoot (AtLabel "cq")) (AtLabel "kq"))]
describe "enters a formation again as many times as --max-loops allows" $ do
it "enters a formation holding the one entered above it under --max-loops=1" $ do
let formation :: Int -> Expression
formation depth = ExFormation [BiTau (AtLabel "kv") (iterate (`ExDispatch` AtLabel "zu") ExRoot !! depth), BiTau AtPhi ExRoot]
base <- defaultReduceContext ExRoot
ctx <- enter (formation 4) =<< enter (formation 3) base{_acyclic = Just Plausible, _maxLoops = 1}
length (concat ctx._entered) `shouldBe` 2
it "cuts a formation holding the two entered above it under --max-loops=1" $ do
let formation :: Int -> Expression
formation depth = ExFormation [BiTau (AtLabel "qe") (iterate (`ExDispatch` AtLabel "yo") ExRoot !! depth), BiTau AtPhi ExRoot]
base <- defaultReduceContext ExRoot
(enter (formation 7) =<< enter (formation 6) =<< enter (formation 5) base{_acyclic = Just Plausible, _maxLoops = 1})
`shouldThrow` (\e -> "already inside" `isInfixOf` show (e :: SomeException))
it "enters a copy of an atom that only resembles the copy entered above it" $ do
base <- defaultReduceContext ExRoot
ctx <- enter (ExFormation [BiTau (AtLabel "t") (ExFormation [BiLambda (FnSymbol 4)]), BiLambda (Function "L_vo")]) =<< enter (ExFormation [BiTau (AtLabel "t") (ExDispatch ExRoot (AtLabel "pu")), BiLambda (Function "L_vo")]) base{_acyclic = Just Plausible, _maxLoops = 0}
length (concat ctx._entered) `shouldBe` 2
it "cuts a copy of an atom that repeats the copy entered above it exactly" $ do
let formation :: Expression
formation = ExFormation [BiTau (AtLabel "ka") (ExDispatch ExRoot (AtLabel "mi")), BiLambda (Function "L_ru")]
base <- defaultReduceContext ExRoot
(enter formation =<< enter formation base{_acyclic = Just Plausible, _maxLoops = 0})
`shouldThrow` (\e -> "already inside" `isInfixOf` show (e :: SomeException))
describe "places a formation among the objects of the world" $ do
it "places a formation by the object the fact table maps it to" $ do
let body = ExApplication (ExDispatch ExRoot (AtLabel "zuq")) (ArTau (AtLabel "wo") (ExFormation [BiLambda (FnSymbol 7)]))
facts <- factual
base <- defaultReduceContext ExRoot
noted base{_facts = Just facts} (ExFormation [BiTau AtPhi body]) (ExDispatch ExRoot (AtLabel "nq"))
fmap fst <$> declared (ExFormation [BiTau (AtLabel "nq") (ExFormation [BiVoid AtPhi]), BiTau (AtLabel "kel") (ExFormation [BiTau AtPhi body])]) base{_facts = Just facts} (ExFormation [BiTau AtPhi body])
`shouldReturn` Just (ExDispatch ExRoot (AtLabel "nq"))
it "recalls every fact it follows on its way to the world, one by one" $ do
let head' = ExFormation [BiVoid (AtLabel "ru"), BiTau AtPhi (ExDispatch ExXi (AtLabel "ru"))]
copy = ExFormation [BiTau (AtLabel "ru") (ExFormation [BiLambda (FnSymbol 6)]), BiTau AtPhi (ExDispatch ExXi (AtLabel "ru"))]
applied = ExApplication head' (ArTau (AtLabel "ru") (ExFormation [BiLambda (FnSymbol 6)]))
facts <- factual
told <- newIORef []
base <- defaultReduceContext ExRoot
mapM_ (uncurry (noted base{_facts = Just facts})) [(head', ExDispatch ExRoot (AtLabel "vex")), (copy, applied)]
_ <- declared (ExFormation [BiTau (AtLabel "vex") head']) base{_facts = Just facts, _saveEval = \record -> modifyIORef' told (record :)} copy
records <- readIORef told
reverse [(term, reply) | EvRecalled _ term reply <- records] `shouldBe` [(copy, applied), (head', ExDispatch ExRoot (AtLabel "vex"))]
it "recalls every fact of a circle of facts once, whatever symbol the copy holds" $ do
let recalls :: Int -> IO Int
recalls symbol = do
let head' = ExFormation [BiVoid (AtLabel "ko"), BiLambda (Function "L_jew")]
copy = ExFormation [BiTau (AtLabel "ko") (ExFormation [BiLambda (FnSymbol symbol)]), BiLambda (Function "L_jew")]
twin = ExFormation [BiTau (AtLabel "ko") (ExFormation [BiLambda (FnSymbol symbol)]), BiLambda (Function "L_jew"), BiTau AtRho (ExDispatch ExRoot (AtLabel "jew"))]
answer = ExFormation [BiTau AtPhi twin]
facts <- factual
told <- newIORef []
base <- defaultReduceContext ExRoot
mapM_ (uncurry (noted base{_facts = Just facts})) [(head', ExDispatch ExRoot (AtLabel "jew")), (copy, ExApplication head' (ArTau (AtLabel "ko") (ExFormation [BiLambda (FnSymbol symbol)]))), (answer, copy), (twin, ExDispatch answer AtPhi)]
mapM_ (\index -> noted base{_facts = Just facts} (ExFormation [BiLambda (FnSymbol (symbol + index))]) (ExDispatch ExRoot (AtLabel "pad"))) [1 .. 12]
_ <- declared (ExFormation [BiTau (AtLabel "jew") head']) base{_facts = Just facts, _saveEval = \record -> modifyIORef' told (record :)} answer
(\records -> length [term | EvRecalled _ term _ <- records]) <$> readIORef told
mapM recalls [3, 17 .. 700] `shouldReturn` replicate 50 3
it "answers the voids of the first head a chain of remembered copies was applied to" $ do
let head' = ExFormation [BiVoid (AtLabel "ka"), BiVoid (AtLabel "mu"), BiLambda (Function "L_ozu")]
half = ExFormation [BiTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]), BiVoid (AtLabel "mu"), BiLambda (Function "L_ozu")]
full = ExFormation [BiTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]), BiTau (AtLabel "mu") (ExFormation [BiLambda (FnSymbol 9)]), BiLambda (Function "L_ozu")]
facts <- factual
base <- defaultReduceContext ExRoot
mapM_ (uncurry (noted base{_facts = Just facts})) [(head', ExDispatch ExRoot (AtLabel "ozu")), (half, ExApplication head' (ArTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]))), (full, ExApplication half (ArTau (AtLabel "mu") (ExFormation [BiLambda (FnSymbol 9)])))]
voided base{_facts = Just facts} full `shouldReturn` Just [AtLabel "ka", AtLabel "mu"]
it "answers no voids for a formation the fact table does not hold" $ do
facts <- factual
base <- defaultReduceContext ExRoot
voided base{_facts = Just facts} (ExFormation [BiTau (AtLabel "pe") (ExFormation []), BiLambda (Function "L_uv")]) `shouldReturn` Nothing
it "places nothing the fact table does not map" $ do
let body = ExApplication (ExDispatch ExRoot (AtLabel "zuq")) (ArTau (AtLabel "wo") (ExFormation [BiLambda (FnSymbol 7)]))
facts <- factual
base <- defaultReduceContext ExRoot
fmap fst <$> declared (ExFormation [BiTau (AtLabel "kel") (ExFormation [BiTau AtPhi body])]) base{_facts = Just facts} (ExFormation [BiTau AtPhi body])
`shouldReturn` Nothing