phino-0.0.143: test/BuilderSpec.hs
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT
module BuilderSpec where
import AST
import Builder
import Control.Exception (SomeException)
import Control.Monad
import Data.Either (isLeft)
import Data.List (isInfixOf)
import Data.Map.Strict qualified as Map
import Data.Text qualified as T
import Matcher
import System.Random (randomRIO)
import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, anyException, describe, it, shouldBe, shouldSatisfy, shouldThrow)
import Text.Printf (printf)
import Yaml qualified as Y
test :: (Show a, Eq a) => (a -> Subst -> Either String a) -> [(String, a, [(T.Text, MetaValue)], Either String a)] -> SpecWith (Arg Expectation)
test function useCases =
forM_ useCases $ \(desc, expr, mp, res) ->
it desc $ function expr (Subst (Map.mapKeys Named (Map.fromList mp))) `shouldBe` res
spec :: Spec
spec = do
describe "buildExpression" $
test
buildExpression
[
( "Q.!t => (!t >> x) => Q.x"
, ExDispatch ExRoot (AtMeta "t")
, [("t", MvAttribute (AtLabel "x"))]
, Right (ExDispatch ExRoot (AtLabel "x"))
)
,
( "Q.c(!t -> !e) => (!t >> x, !e >> $.y.z) => Q.c(x -> $.y.z)"
, ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArTau (AtMeta "t") (ExMeta "e"))
, [("t", MvAttribute (AtLabel "x")), ("e", MvExpression (ExDispatch (ExDispatch ExXi (AtLabel "y")) (AtLabel "z")))]
, Right (ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArTau (AtLabel "x") (ExDispatch (ExDispatch ExXi (AtLabel "y")) (AtLabel "z"))))
)
,
( "[[!t -> $.x, !B]] => (!t >> y, !B >> [[b -> ?, L> Func]]) => [[y -> $.x, b -> ?, L> Func]]"
, ExFormation [BiTau (AtMeta "t") (ExDispatch ExXi (AtLabel "x")), BiMeta "B"]
, [("t", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "b"), BiLambda (Function "Func")])]
, Right
( ExFormation
[ BiTau (AtLabel "y") (ExDispatch ExXi (AtLabel "x"))
, BiVoid (AtLabel "b")
, BiLambda (Function "Func")
]
)
)
,
( "Q.!t => () => X"
, ExDispatch ExRoot (AtMeta "t")
, []
, Left "meta 't' is either does not exist or refers to an inappropriate term"
)
,
( "!e3(!t1 -> !e1, !t2 => !e2) => (!e3 >> [[]], !t1 >> x, !e1 >> Q, !t2 >> y, !e2 >> $) => [[]](x -> Q, y -> $)"
, ExApplication (ExApplication (ExMeta "e3") (ArTau (AtMeta "t1") (ExMeta "e1"))) (ArTau (AtMeta "t2") (ExMeta "e2"))
,
[ ("e3", MvExpression (ExFormation []))
, ("t1", MvAttribute (AtLabel "x"))
, ("e1", MvExpression ExRoot)
, ("t2", MvAttribute (AtLabel "y"))
, ("e2", MvExpression ExXi)
]
, Right (ExApplication (ExApplication (ExFormation []) (ArTau (AtLabel "x") ExRoot)) (ArTau (AtLabel "y") ExXi))
)
,
( "⟦!t ↦ ∅, !B⟧.!t => (!t >> t, !B >> ⟦ x ↦ ξ.t ⟧ ) => ⟦ t ↦ ∅, x ↦ ξ.t ⟧.t"
, ExDispatch (ExFormation [BiVoid (AtMeta "t"), BiMeta "B"]) (AtMeta "t")
,
[ ("t", MvAttribute (AtLabel "t"))
, ("B", MvBindings [BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))])
]
, Right
( ExDispatch
( ExFormation
[ BiVoid (AtLabel "t")
, BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))
]
)
(AtLabel "t")
)
)
,
( "Q.c(α!i -> !e) => (!i >> 2, !e >> $) => Q.c(α2 -> $)"
, ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArAlpha (AlMeta "i") (ExMeta "e"))
, [("i", MvIndex 2), ("e", MvExpression ExXi)]
, Right (ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArAlpha (Alpha 2) ExXi))
)
,
( "Q.c(α!i -> Q) => () => X"
, ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArAlpha (AlMeta "i") ExRoot)
, []
, Left "meta 'i' is either does not exist or refers to an inappropriate term"
)
]
describe "buildExpressions" $ do
it "!e => [(!e >> Q.x), (!e >> $.y)] => [Q.x, $.y]" $ do
built <-
buildExpressionsThrows
(ExMeta "e")
[ substSingle "e" (MvExpression (ExDispatch ExRoot (AtLabel "x")))
, substSingle "e" (MvExpression (ExDispatch ExXi (AtLabel "y")))
]
built `shouldBe` [ExDispatch ExRoot (AtLabel "x"), ExDispatch ExXi (AtLabel "y")]
it "!e => [(!e1 >> Q.x)] => X" $
buildExpressionsThrows
(ExMeta "e")
[substSingle "e1" (MvExpression (ExDispatch ExRoot (AtLabel "x")))]
`shouldThrow` anyException
describe "contextualize" $
let commonContext :: Expression
commonContext = ExFormation [BiVoid AtRho]
in forM_
[ ("replaces a xi expression with the context", ExXi, commonContext, commonContext)
, ("keeps a root expression untouched", ExRoot, commonContext, ExRoot)
,
( "keeps an empty formation untouched"
, ExFormation [BiVoid AtRho]
, ExFormation [BiVoid AtRho, BiVoid AtRho]
, ExFormation [BiVoid AtRho]
)
,
( "recurses into a dispatch application"
, ExDispatch ExXi (AtLabel "z")
, commonContext
, ExDispatch commonContext (AtLabel "z")
)
, ("keeps a termination untouched", ExTermination, commonContext, ExTermination)
,
( "recurses into both sides of an application with a tau argument"
, ExApplication ExXi (ArTau (AtLabel "x") ExXi)
, commonContext
, ExApplication commonContext (ArTau (AtLabel "x") commonContext)
)
,
( "recurses into both sides of an application with an alpha argument"
, ExApplication ExXi (ArAlpha (Alpha 0) ExXi)
, commonContext
, ExApplication commonContext (ArAlpha (Alpha 0) commonContext)
)
, ("leaves any other expression untouched", ExMeta "e", commonContext, ExMeta "e")
]
(\(desc, expr, context, expected) -> it desc (contextualize expr context `shouldBe` expected))
describe "contextualize against the contextualization rules" $ do
it "contextualizes every random term as the one rule matching it concludes" $ do
pairs <- replicateM 500 ((,) <$> term 3 <*> term 2)
map (\(expr, context) -> conclusions expr context Y.contextualizationRules) pairs
`shouldBe` map (\(expr, context) -> [contextualize expr context]) pairs
it "leaves no contextualization rule unmatched by random terms" $ do
pairs <- replicateM 500 ((,) <$> term 3 <*> term 2)
[rule.name | rule <- Y.contextualizationRules, all (\(expr, context) -> null (conclusions expr context [rule])) pairs]
`shouldBe` []
describe "buildBinding: lambda and delta bindings from metas" $
forM_
[
( "builds a lambda binding from a bound function meta"
, BiLambda (FnMeta "f")
, substSingle "f" (MvFunction (Function "Func"))
, Right [BiLambda (Function "Func")]
)
,
( "fails to build a lambda binding from an unbound function meta"
, BiLambda (FnMeta "f")
, substEmpty
, Left "meta 'f' is either does not exist or refers to an inappropriate term"
)
,
( "builds a delta binding from a bound bytes meta"
, BiDelta (BtMeta "b")
, substSingle "b" (MvBytes (BtOne "00"))
, Right [BiDelta (BtOne "00")]
)
,
( "fails to build a delta binding from an unbound bytes meta"
, BiDelta (BtMeta "b")
, substEmpty
, Left "meta 'b' is either does not exist or refers to an inappropriate term"
)
,
( "fails to build a meta binding that is unbound"
, BiMeta "B"
, substEmpty
, Left "meta 'B' is either does not exist or refers to an inappropriate term"
)
]
(\(desc, binding, subst, expected) -> it desc (buildBinding binding subst `shouldBe` expected))
describe "the throwing builders report a descriptive message" $
forM_
[
( "buildBytesThrows names the bytes it could not build"
, void (buildBytesThrows (BtMeta "b") substEmpty)
, "Couldn't build bytes"
)
,
( "buildBindingThrows names the binding it could not build"
, void (buildBindingThrows (BiMeta "B") substEmpty)
, "Couldn't build binding"
)
,
( "buildAttributeThrows names the attribute it could not build"
, void (buildAttributeThrows (AtMeta "t") substEmpty)
, "Couldn't build attribute"
)
,
( "buildExpressionThrows names the expression it could not build"
, void (buildExpressionThrows (ExMeta "e") substEmpty)
, "Couldn't build expression"
)
]
(\(desc, action, message) -> it desc (action `shouldThrow` (\exc -> message `isInfixOf` show (exc :: SomeException))))
describe "builds an anonymous meta only from the pattern that bound it" $ do
-- An anonymous slot is a key of the very substitution its own pattern
-- produced, which is how a fired pattern is rebuilt for replacement. Asked
-- for it under any other substitution, the builder says plainly that the
-- meta has no name to be referenced by, rather than inventing a term.
forM_
[
( "buildExpression rebuilds an anonymous expression from its own slot"
, buildExpression (ExAny (Slot "e" 7)) (substSlot (Slot "e" 7) (MvExpression ExRoot))
, Right ExRoot
)
,
( "buildExpression refuses an anonymous expression bound by another pattern"
, buildExpression (ExAny (Slot "e" 7)) (substSlot (Slot "e" 9) (MvExpression ExRoot))
, Left "anonymous meta '!e' cannot be referenced"
)
]
(\(desc, built, expected) -> it desc (built `shouldBe` expected))
forM_
[
( "buildAttribute rebuilds an anonymous attribute from its own slot"
, buildAttribute (AtAny (Slot "t" 2)) (substSlot (Slot "t" 2) (MvAttribute AtPhi))
, Right AtPhi
)
,
( "buildAttribute refuses an anonymous attribute bound by another pattern"
, buildAttribute (AtAny (Slot "t" 2)) substEmpty
, Left "anonymous meta '!t' cannot be referenced"
)
]
(\(desc, built, expected) -> it desc (built `shouldBe` expected))
describe "build with duplicate attributes in bindings" $ do
it "build binding with duplicates" $
buildBinding (BiMeta "B") (substSingle "B" (MvBindings [BiVoid AtRho, BiVoid AtRho])) `shouldSatisfy` isLeft
it "build formation with duplicates" $
buildExpression (ExMeta "e") (substSingle "e" (MvExpression (ExFormation [BiVoid AtRho, BiVoid AtRho]))) `shouldSatisfy` isLeft
describe "buildExpression" $
it "does not leave an invalid global application around rho" $
buildExpression
(ExApplication ExRoot (ArTau AtRho (ExFormation [BiVoid AtRho])))
substEmpty
`shouldBe` Right ExRoot
describe "pathOf" $
it "names the world itself as Φ" $
pathOf
(ExFormation [BiTau (AtLabel "qwv") (ExFormation [BiVoid AtRho]), BiLambda (Function "Kzr")])
(ExFormation [BiTau (AtLabel "qwv") (ExFormation [BiVoid AtRho]), BiLambda (Function "Kzr")])
`shouldBe` ExRoot
where
-- A term of the calculus no deeper than the given depth, made of the six
-- forms 𝒞 is defined over, so every contextualization rule meets some.
term :: Int -> IO Expression
term depth = do
form <- randomRIO (0 :: Int, if depth > 0 then 6 else 2)
case form of
0 -> pure ExXi
1 -> pure ExRoot
2 -> pure ExTermination
3 -> do
attr <- attribute
body <- term (depth - 1)
pure (ExFormation [BiTau attr body, BiVoid AtRho])
4 -> ExDispatch <$> term (depth - 1) <*> attribute
5 -> ExApplication <$> term (depth - 1) <*> (ArTau <$> attribute <*> term (depth - 1))
_ -> ExApplication <$> term (depth - 1) <*> (ArAlpha . Alpha <$> randomRIO (0, 9) <*> term (depth - 1))
attribute :: IO Attribute
attribute = do
letters <- replicateM 3 (randomRIO ('a', 'z'))
pick <- randomRIO (0 :: Int, 3)
pure ([AtLabel (T.pack letters), AtPhi, AtLabel (T.pack (reverse letters)), AtLambda] !! pick)
-- What the given rules conclude 𝒞(n, c) to be, one conclusion per match,
-- reading every premise 𝒞 of a smaller term off 'contextualize' itself.
conclusions :: Expression -> Expression -> [Y.ContextualizeRule] -> [Expression]
conclusions expr context rules =
[ built
| rule <- rules
, matched <- matchExpression' rule.match expr
, around <- matchExpression' rule.cmatch context
, Just subst <- [combine matched around]
, Right built <- [foldM premised subst rule.premises >>= buildExpression rule.cresult]
]
premised :: Subst -> Y.Premise -> Either String Subst
premised subst (Y.Premise result (Y.OpContextualize expr context)) = do
inner <- buildExpression expr subst
outer <- buildExpression context subst
maybe (Left (printf "premise meta '%s' clashes with a binding" (T.unpack result))) Right (combine (substSingle result (MvExpression (contextualize inner outer))) subst)
premised _ premise = Left (printf "premise '%s' is not a contextualization" (T.unpack premise.result))