phino-0.0.145: test/DataizeSpec.hs
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT
module DataizeSpec (spec) where
import AST
import Control.Exception (SomeException)
import Control.Monad
import Data.Aeson (FromJSON)
import Data.List (find, isInfixOf, nub)
import Data.List.NonEmpty (NonEmpty (..))
import Data.Map.Strict qualified as Map
import Data.Maybe (fromMaybe)
import Data.Yaml qualified as Decode
import Dataize (Outcome (..), dataize, dataize', reduction)
import Deps (Judgment (..), State, dontSaveEval, dontSaveStep)
import Engine (Engine (_normal), building)
import Evaluate (evaluation, fired)
import Files (allPathsIn)
import Fixtures (defaultReduceContext, fixtureLambdas, linked, loopingLambdas, overdue, primitives, recorded, withLambdas)
import GHC.Generics (Generic)
import Lambdas (Lambdas, emptyLambdas, readLambdas)
import Matcher (substEmpty)
import Morph (ReduceContext (..), Steps (..), emptyState, execBuildTerm)
import Parser (parseBytes, parseExpressionThrows)
import Rewriter (Rewritten)
import Rule (RuleContext (RuleContext), matchExpressionWithRule')
import System.FilePath (makeRelative)
import Test.Hspec
import Yaml qualified
test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> State -> ReduceContext -> IO ((a, [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 DataizePack = DataizePack
{ location :: Maybe String
, input :: String
, model :: Maybe Bool
, symbolic :: Maybe Bool
, result :: Maybe String
, fails :: Maybe String
}
deriving (Generic, Show, FromJSON)
testDataize :: Lambdas -> FilePath -> Expectation
testDataize known pth = do
DataizePack{..} <- Decode.decodeFileThrow pth
expr <- parseExpressionThrows (if model == Just True then primitives input else input)
loc <- parseExpressionThrows (fromMaybe "Q" location)
let ctx = (defaultReduceContext loc){_symbolic = if symbolic == Just True then known else emptyLambdas}
case (result, fails) of
(Just res, Nothing) -> do
bts <- either (fail . ("cannot read the expected bytes: " ++)) pure (parseBytes res)
(value, _, _) <- dataize expr emptyState ctx
value `shouldBe` Dataized bts
(Nothing, Just message) ->
dataize expr emptyState ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException))
_ -> expectationFailure "The pack holds neither a single 'result' nor a single 'fails'"
partially :: Lambdas -> String -> IO ((Outcome, [Rewritten]), String)
partially known src = do
expr <- parseExpressionThrows (primitives src)
recorded $ \record -> do
let ctx = (withLambdas known (defaultReduceContext ExRoot)){_partial = True, _saveEval = record}
(outcome, chain, _) <- dataize expr emptyState ctx
pure (outcome, chain)
looping :: (Lambdas -> IO a) -> IO a
looping action = loopingLambdas (readLambdas >=> action)
spec :: Spec
spec = do
known <- runIO fixtureLambdas
describe "dataize' fails when no dataization rule matches the term" $
it "throws instead of treating the unmatched meta as ⊥" $
dataize' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)
`shouldThrow` (\e -> "no dataization rule matched" `isInfixOf` show (e :: SomeException))
describe "dataization 'norm' is disjoint from the specific clauses" $ do
let rctx = RuleContext (execBuildTerm ExRoot (defaultReduceContext ExRoot)) Nothing (_normal linked)
dataizeRule :: String -> Yaml.DataizeRule
dataizeRule nm = fromMaybe (error ("no dataization rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.dataizationRules)
asRule :: Yaml.DataizeRule -> Yaml.Rule
asRule r = Yaml.Rule r.name Nothing Nothing r.match ExRoot r.when Nothing Nothing
it "does not fire on a formation" $ do
substs <- matchExpressionWithRule' [substEmpty] (ExFormation [BiDelta (BtOne "00")]) (asRule (dataizeRule "norm")) rctx
substs `shouldBe` []
it "does not fire on the termination ⊥" $ do
substs <- matchExpressionWithRule' [substEmpty] ExTermination (asRule (dataizeRule "norm")) rctx
substs `shouldBe` []
it "still fires on a non-formation, non-termination normal form" $ do
substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (dataizeRule "norm")) rctx
null substs `shouldBe` False
describe "dataize" $ do
let resources = "test-resources/dataization-packs"
packs <- runIO (allPathsIn resources)
forM_ packs (\pth -> it (makeRelative resources pth) (testDataize known pth))
describe "dataize'" $
test
dataize'
[ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExRoot, BtOne "00")
,
( "[[ @ -> [[ D> 00-]] ]] => 00-"
, ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "00"), BiVoid AtRho]), BiVoid AtRho]
, ExRoot
, BtOne "00"
)
,
( "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]] => 01-"
, ExFormation
[ BiTau
AtPhi
( ExDispatch
( ExFormation
[ BiTau
(AtLabel "x")
( ExApplication
( ExFormation
[ BiDelta (BtOne "01")
, BiVoid (AtLabel "y")
, BiVoid AtRho
]
)
(ArTau (AtLabel "y") (ExFormation []))
)
]
)
(AtLabel "x")
)
]
, ExRoot
, BtOne "01"
)
]
describe "fails to dataize the terminator" $ do
let failsOn desc input =
it desc $
dataize' (input, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)
`shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
failsOn "throws on ⊥ instead of mapping it to empty bytes" ExTermination
failsOn "throws on a data-less formation, which dataizes ⊥" (ExFormation [])
failsOn
"throws on a void slot fed a non-absolute argument instead of looping forever"
(ExApplication (ExFormation [BiVoid (AtLabel "x")]) (ArTau (AtLabel "x") (ExDispatch ExXi (AtLabel "foo"))))
describe "stops a dataization that never reaches bytes" $ do
it "fails on the step limit instead of morphing forever" $
looping $ \endless -> do
expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_loop ⟧ ⟧"
dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty endless (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
`shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException))
it "parks the step limit as a residual with --partial" $
looping $ \endless -> do
expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_loop ⟧ ⟧"
(outcome, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing Nothing Nothing 1 False True True False 1 Nothing Dataization [] Map.empty endless (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
case outcome of
Residual _ -> pure ()
Dataized bts -> expectationFailure ("expected a residual, dataized to " ++ show bts)
describe "stops a dataization by the clock of --max-seconds" $
it "fails a partial dataization once the deadline has passed" $ do
expr <- parseExpressionThrows "[[ @ -> [[ D> 7E- ]] ]]"
deadline <- overdue 29
dataize expr emptyState (defaultReduceContext ExRoot){_deadline = Just deadline, _partial = True}
`shouldThrow` (\e -> "--max-seconds=29" `isInfixOf` show (e :: SomeException))
describe "partially evaluates around a λ function that cannot fire (--partial)" $ do
let placeholder = ExFormation [BiLambda (Function "Sym_arg_0")]
it "fails on it without the flag, naming the λ function" $ do
expr <- parseExpressionThrows (primitives "2.times(3).nope")
dataize expr emptyState (withLambdas known (defaultReduceContext ExRoot))
`shouldThrow` (\e -> "No entry of --symbolic answers the λ function 'L_number_nope'" `isInfixOf` show (e :: SomeException))
it "leaves the application of the unanswered λ function in place" $ do
((outcome, _), _) <- partially known "2.times(3).nope"
case outcome of
Residual (ExFormation bds) -> bds `shouldContain` [BiLambda (Function "L_number_nope")]
other -> expectationFailure ("expected a residual formation, got " ++ show other)
it "keeps what was evaluated before the stuck site in the residue" $ do
((outcome, _), _) <- partially known "2.times(3).nope"
case outcome of
Residual (ExFormation bds) -> do
let rho = [value | BiTau AtRho value <- bds]
length rho `shouldBe` 1
[() | ExApplication (ExDispatch ExRoot (AtLabel "number")) (ArTau AtPhi _) <- rho] `shouldBe` [()]
other -> expectationFailure ("expected a residual formation, got " ++ show other)
it "writes the firing that answered into the protocol and stops at the stuck one" $ do
(_, protocol) <- partially known "2.times(3).nope"
protocol
`shouldBe` unlines
[ " formation(⟦ bytes(φ) ↦ ⟦ not(ρ) ↦ L_bytes_not:λ, eq(ρ, b) ↦ L_bytes_eq:λ ⟧, bool(φ) ↦ ⟦ if(ρ, then, else) ↦ L_fork:λ ⟧, number(φ) ↦ ⟦ as-bytes ↦ φ, plus(ρ, x) ↦ L_number_plus:λ, times(ρ, x) ↦ L_number_times:λ, div(ρ, x) ↦ L_number_div:λ, gt(ρ, x) ↦ L_number_gt:λ, eq(ρ, x) ↦ ρ.as-bytes.eq( x.as-bytes ):φ, nope(ρ) ↦ L_number_nope:λ ⟧, φ ↦ 2.times( 3 ).nope ⟧) # 𝔻(Φ)"
, " 𝔼(L_number_times) # 𝕄(Φ)"
, " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-00-00-00-00-00-00-00:Δ ), as-bytes ↦ φ, plus(ρ, x) ↦ L_number_plus:λ, times(ρ, x) ↦ L_number_times:λ, div(ρ, x) ↦ L_number_div:λ, gt(ρ, x) ↦ L_number_gt:λ, eq(ρ, x) ↦ ρ.as-bytes.eq( x.as-bytes ):φ, nope(ρ) ↦ L_number_nope:λ ⟧) # 𝔻(Φ.a🌵17)"
, " formation(⟦ φ ↦ 40-00-00-00-00-00-00-00:Δ, not(ρ) ↦ L_bytes_not:λ, eq(ρ, b) ↦ L_bytes_eq:λ ⟧) # 𝔻(Φ.a🌵17)"
, " 𝛿1.1 := 40-00-00-00-00-00-00-00 # 𝔻(ξ.ρ)"
, " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-08-00-00-00-00-00-00:Δ ), as-bytes ↦ φ, plus(ρ, x) ↦ L_number_plus:λ, times(ρ, x) ↦ L_number_times:λ, div(ρ, x) ↦ L_number_div:λ, gt(ρ, x) ↦ L_number_gt:λ, eq(ρ, x) ↦ ρ.as-bytes.eq( x.as-bytes ):φ, nope(ρ) ↦ L_number_nope:λ ⟧) # 𝔻(Φ.a🌵18)"
, " formation(⟦ φ ↦ 40-08-00-00-00-00-00-00:Δ, not(ρ) ↦ L_bytes_not:λ, eq(ρ, b) ↦ L_bytes_eq:λ ⟧) # 𝔻(Φ.a🌵18)"
, " 𝛿2.1 := 40-08-00-00-00-00-00-00 # 𝔻(ξ.x)"
, " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"
, " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, as-bytes ↦ φ, plus(ρ, x) ↦ L_number_plus:λ, times(ρ, x) ↦ L_number_times:λ, div(ρ, x) ↦ L_number_div:λ, gt(ρ, x) ↦ L_number_gt:λ, eq(ρ, x) ↦ ρ.as-bytes.eq( x.as-bytes ):φ, nope(ρ) ↦ L_number_nope:λ ⟧ # 𝕄(𝑛.1.1)"
, " unanswered(L_number_nope) # 𝔻(⟦ ρ ↦ Φ.number( φ ↦ 𝜎1:λ ), λ ⤍ L_number_nope ⟧)"
]
it "leaves an unanswered λ function dataized directly as the whole residue" $ do
((outcome, chain), protocol) <- partially known "[[ L> Sym_arg_0 ]]"
outcome `shouldBe` Residual placeholder
protocol `shouldBe` " formation(⟦ bytes(φ) ↦ ⟦ not(ρ) ↦ L_bytes_not:λ, eq(ρ, b) ↦ L_bytes_eq:λ ⟧, bool(φ) ↦ ⟦ if(ρ, then, else) ↦ L_fork:λ ⟧, number(φ) ↦ ⟦ as-bytes ↦ φ, plus(ρ, x) ↦ L_number_plus:λ, times(ρ, x) ↦ L_number_times:λ, div(ρ, x) ↦ L_number_div:λ, gt(ρ, x) ↦ L_number_gt:λ, eq(ρ, x) ↦ ρ.as-bytes.eq( x.as-bytes ):φ, nope(ρ) ↦ L_number_nope:λ ⟧, φ ↦ Sym_arg_0:λ ⟧) # 𝔻(Φ)\n unanswered(Sym_arg_0) # 𝔻(Sym_arg_0:λ)\n"
map fst chain `shouldEndWith` [placeholder]
it "still reaches the manufactured datum when nothing is stuck" $ do
((outcome, _), _) <- partially known "2.times(3)"
outcome `shouldBe` Dataized (BtMany ["40", "45", "00", "00", "00", "00", "00", "00"])
it "parks a firing whose operand dataizes the terminator ⊥" $ do
((outcome, _), protocol) <- partially known "5.plus( ⟦ ⟧ )"
case outcome of
Residual (ExFormation bds) -> bds `shouldContain` [BiLambda (Function "L_number_plus")]
other -> expectationFailure ("expected a residual formation, got " ++ show other)
protocol `shouldSatisfy` isInfixOf "unanswered(⊥) # 𝔻(⊥)"
describe "ReduceContext's --max-depth/--max-cycles reach into the normalization it splices in" $ do
let boxed = "[[ @ -> [[ D> 00- ]] ]]"
forM_
[
( "--max-cycles"
, ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing Nothing Nothing 1 True True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked
, "--max-cycles=0"
)
,
( "--max-depth"
, ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing Nothing Nothing 1 True True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked
, "--max-depth=0"
)
]
( \(flag, ctx, message) ->
it ("throws once " ++ flag ++ " is exhausted with --depth-sensitive") $ do
expr <- parseExpressionThrows "[[ @ -> [[ x -> [[ D> 00- ]] ]].x ]]"
dataize expr emptyState ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))
)
it "does not throw without --depth-sensitive even once --max-depth is exhausted" $ do
expr <- parseExpressionThrows boxed
(value, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
value `shouldBe` Dataized (BtOne "00")
it "throws once --max-cycles is exhausted even without --depth-sensitive" $ do
expr <- parseExpressionThrows boxed
dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
`shouldThrow` (\e -> "--max-cycles=0" `isInfixOf` show (e :: SomeException))
describe "labels every step with a defined rule or operation" $ do
let verb op = case op of
Yaml.OpMorph _ _ -> "morph"
Yaml.OpNormalize _ -> "normalize"
Yaml.OpEvaluate _ _ -> "evaluate"
Yaml.OpContextualize _ _ -> "contextualize"
Yaml.OpDataize _ _ -> "dataize"
allowed =
map (.name) Yaml.morphingRules
++ map (.name) Yaml.dataizationRules
++ map (.name) Yaml.normalizationRules
++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.morphingRules
++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.dataizationRules
it "uses no step label without a defining rule or operation" $ do
expr <- parseExpressionThrows (primitives "5.plus(6)")
loc <- parseExpressionThrows "Q"
(_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext loc))
let orphans = nub [label | (_, Just (_, label)) <- chain, label `notElem` allowed, label /= "symbol"]
unless
(null orphans)
(expectationFailure ("Dataization emitted step labels with no defining rule or operation: " ++ show orphans))
it "takes the step of a firing by evaluation" $ do
expr <- parseExpressionThrows (primitives "5.plus(6)")
loc <- parseExpressionThrows "Q"
(_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext loc))
map snd chain `shouldContain` [Just (Evaluation, "evaluate")]
it "takes the step of a box by contextualization" $ do
expr <- parseExpressionThrows "[[ @ -> [[ D> 0A- ]] ]]"
(_, chain, _) <- dataize expr emptyState (defaultReduceContext ExRoot)
map snd chain `shouldContain` [Just (Contextualization, "contextualize")]
it "takes the step of a delta by dataization" $ do
expr <- parseExpressionThrows "[[ D> 3C- ]]"
(_, chain, _) <- dataize expr emptyState (defaultReduceContext ExRoot)
map snd chain `shouldBe` [Just (Dataization, "delta"), Nothing]
describe "names every rule uniquely across rule sets" $
it "shares no rule name between morphing, dataization, normalization and contextualization" $ do
let names =
map (.name) Yaml.morphingRules
++ map (.name) Yaml.dataizationRules
++ map (.name) Yaml.normalizationRules
++ map (.name) Yaml.contextualizationRules
clashes = nub (filter (\n -> length (filter (== n) names) > 1) names)
clashes `shouldBe` []
describe "preserves the reduction label sequence" $ do
let labelsOf loc src = do
expr <- parseExpressionThrows src
loc' <- parseExpressionThrows loc
(_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext loc'))
pure [label | (_, Just (_, label)) <- chain]
it "dataizes 5.plus(6) through the expected rules" $ do
labels <-
labelsOf
"Q"
"[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
labels
`shouldBe` [ "contextualize"
, "maa"
, "alpha"
, "copy"
, "mf"
, "evaluate"
, "contextualize"
, "symbol"
]
it "dataizes a located reference through the expected rules" $ do
labels <- labelsOf "Q.foo.bar" "[[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"
labels `shouldBe` ["contextualize", "md", "dot", "skip", "mf", "delta"]
it "takes every step of 5.plus(6) by the judgment of its rule" $ do
expr <- parseExpressionThrows "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
(_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext ExRoot))
[judgment | (_, Just (judgment, _)) <- chain]
`shouldBe` [ Contextualization
, Morphing
, Normalization
, Normalization
, Morphing
, Evaluation
, Contextualization
, Dataization
]