phino-0.0.145: test/YamlSpec.hs

{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE NamedFieldPuns #-}

-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT

module YamlSpec where

import AST (Alpha, Attribute, Binding, Bytes, Expression (ExMeta, ExRoot))
import Control.Exception (Exception (displayException), SomeException)
import Control.Monad
import Data.Either (isLeft)
import Data.List (isInfixOf, nub, sort, (\\))
import Data.Maybe (fromMaybe)
import Data.Text qualified as T
import Data.Text.Encoding (encodeUtf8)
import Data.Yaml qualified as Yaml
import Files (allPathsIn)
import System.FilePath
import Test.Hspec (Spec, describe, expectationFailure, it, runIO, shouldBe, shouldSatisfy, shouldThrow)
import Yaml (Condition (..), ContextualizeRule (..), DataizeRule (..), MorphRule (..), Number, Operation (..), Premise (..), Rule, contextualizationRules, dataizationRules, morphingRules, yamlRule)

decodeYaml' :: (Yaml.FromJSON a) => String -> Either Yaml.ParseException a
decodeYaml' = Yaml.decodeEither' . encodeUtf8 . T.pack

failsWith :: String -> Either Yaml.ParseException a -> Bool
failsWith fragment decoded = case decoded of
  Left err -> fragment `isInfixOf` Yaml.prettyPrintParseException err
  Right _ -> False

failsAsRedundant :: Either Yaml.ParseException a -> Bool
failsAsRedundant = failsWith "redundant"

spec :: Spec
spec = do
  describe "parses yaml rule" $ do
    let resources = "test-resources/yaml-packs"
    packs <- runIO (allPathsIn resources)
    forM_
      packs
      (\pth -> it (makeRelative resources pth) (void (yamlRule pth)))

  describe "fails on yaml typos" $ do
    let resources = "test-resources/yaml-typos"
    packs <- runIO (allPathsIn resources)
    forM_
      packs
      ( \pth ->
          it (makeRelative resources pth) $
            shouldThrow
              (yamlRule pth)
              ( \e ->
                  let msg = displayException (e :: SomeException)
                   in "Unknown" `isInfixOf` msg || "Exactly one" `isInfixOf` msg
              )
      )

  describe "rejects malformed rule content" $ do
    let primYaml = "name: prim\nlabel: prim\nmatch: ⟦𝐵⟧\nuniverse: 𝑒\nconclusion: ⟦𝐵⟧"
        endYaml = "name: end\nlabel: end\nmatch: ⊥\nuniverse: 𝑒\nconclusion: '--'"
        cxiYaml = "name: cxi\nlabel: cxi\nmatch: ξ\nc-match: 𝑘\nc-result: 𝑘"
    forM_
      [ ("a label that equals the name in a morphing rule", primYaml, failsAsRedundant (decodeYaml' primYaml :: Either Yaml.ParseException MorphRule))
      , ("a label that equals the name in a dataization rule", endYaml, failsAsRedundant (decodeYaml' endYaml :: Either Yaml.ParseException DataizeRule))
      , ("a label that equals the name in a contextualization rule", cxiYaml, failsAsRedundant (decodeYaml' cxiYaml :: Either Yaml.ParseException ContextualizeRule))
      , ("a malformed embedded 𝜑-syntax: an index meta that does not parse", "'bogus'", isLeft (decodeYaml' "'bogus'" :: Either Yaml.ParseException Number))
      , ("a malformed embedded 𝜑-syntax: an attribute that does not parse", "'123'", isLeft (decodeYaml' "'123'" :: Either Yaml.ParseException Attribute))
      , ("a malformed embedded 𝜑-syntax: an alpha that does not parse", "'bogus'", isLeft (decodeYaml' "'bogus'" :: Either Yaml.ParseException Alpha))
      , ("a malformed embedded 𝜑-syntax: bytes that do not parse", "'0a-'", isLeft (decodeYaml' "'0a-'" :: Either Yaml.ParseException Bytes))
      , ("a malformed embedded 𝜑-syntax: an expression that does not parse", "'L>'", isLeft (decodeYaml' "'L>'" :: Either Yaml.ParseException Expression))
      , ("a malformed embedded 𝜑-syntax: a binding that does not parse", "'L>'", isLeft (decodeYaml' "'L>'" :: Either Yaml.ParseException Binding))
      ]
      ( \(desc, yaml, valid) ->
          it ("rejects " ++ desc) (unless valid (expectationFailure ("expected rejection for: " ++ yaml)))
      )

  it "rejects an 'e-match' in a rewriting rule" $
    (decodeYaml' "name: kvz\npattern: '⟦ 𝜏1 ↦ 𝑒1 ⟧'\ne-match: '𝑒2'\nresult: '𝑒2'" :: Either Yaml.ParseException Rule)
      `shouldSatisfy` failsWith "The rule 'kvz' carries an 'e-match'"
  describe "rejects an anonymous meta outside a pattern" $ do
    let rewriting :: String -> String
        rewriting field = "name: foo\npattern: '⟦ 𝜏1 ↦ 𝑒1 ⟧'\n" ++ field
        inferring :: String -> String
        inferring field = "name: foo\nmatch: '⟦ 𝜏1 ↦ 𝑒1 ⟧'\n" ++ field
    forM_
      [
        ( "in 'result' of a rewriting rule"
        , failsWith
            "anonymous meta '!e' cannot be referenced in 'result' of rule 'foo'"
            (decodeYaml' (rewriting "result: '𝑒'") :: Either Yaml.ParseException Rule)
        )
      ,
        ( "in 'when' of a rewriting rule"
        , failsWith
            "anonymous meta '!t' cannot be referenced in 'when' of rule 'foo'"
            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhen:\n  in: ['𝜏', '!B1']") :: Either Yaml.ParseException Rule)
        )
      ,
        ( "in 'where' of a rewriting rule"
        , failsWith
            "anonymous meta '!e' cannot be referenced in 'where' of rule 'foo'"
            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhere:\n  - meta: '!t1'\n    function: concat\n    args: ['𝑒']") :: Either Yaml.ParseException Rule)
        )
      ,
        ( "in 'having' of a rewriting rule"
        , failsWith
            "anonymous meta '!e' cannot be referenced in 'having' of rule 'foo'"
            (decodeYaml' (rewriting "result: '⟦ ⟧'\nhaving:\n  formation: '𝑒'") :: Either Yaml.ParseException Rule)
        )
      ,
        ( "as a bare index meta in 'when' of a rewriting rule"
        , failsWith
            "anonymous meta '!i' cannot be referenced in 'when' of rule 'foo'"
            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhen:\n  eq: ['𝑖', 1]") :: Either Yaml.ParseException Rule)
        )
      ,
        ( "inside an 'nf' condition of a rewriting rule"
        , failsWith
            "anonymous meta '!e' cannot be referenced in 'when' of rule 'foo'"
            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhen:\n  nf: '𝑒'") :: Either Yaml.ParseException Rule)
        )
      ,
        ( "in 'conclusion' of a morphing rule"
        , failsWith
            "anonymous meta '!n' cannot be referenced in 'conclusion' of rule 'foo'"
            (decodeYaml' (inferring "universe: 𝑒2\nconclusion: '𝑛'") :: Either Yaml.ParseException MorphRule)
        )
      ,
        ( "in a premise of a morphing rule"
        , failsWith
            "anonymous meta '!e' cannot be referenced in 'premises' of rule 'foo'"
            (decodeYaml' (inferring "universe: 𝑒2\nconclusion: 𝑛1\npremises:\n  - n-result: 𝑛1\n    normalize: '𝑒'") :: Either Yaml.ParseException MorphRule)
        )
      ,
        ( "in 'when' of a morphing rule"
        , failsWith
            "anonymous meta '!e' cannot be referenced in 'when' of rule 'foo'"
            (decodeYaml' (inferring "universe: 𝑒2\nconclusion: 𝑛1\nwhen:\n  formation: '𝑒'") :: Either Yaml.ParseException MorphRule)
        )
      ,
        ( "in 'conclusion' of a dataization rule"
        , failsWith
            "anonymous meta '!d' cannot be referenced in 'conclusion' of rule 'foo'"
            (decodeYaml' (inferring "universe: 𝑒2\nconclusion: '𝛿'") :: Either Yaml.ParseException DataizeRule)
        )
      ,
        ( "in 'when' of a dataization rule"
        , failsWith
            "anonymous meta '!e' cannot be referenced in 'when' of rule 'foo'"
            (decodeYaml' (inferring "universe: 𝑒2\nconclusion: 𝛿1\nwhen:\n  formation: '𝑒'") :: Either Yaml.ParseException DataizeRule)
        )
      ,
        ( "in a premise of a dataization rule"
        , failsWith
            "anonymous meta '!e' cannot be referenced in 'premises' of rule 'foo'"
            (decodeYaml' (inferring "universe: 𝑒2\nconclusion: 𝛿1\npremises:\n  - d-result: 𝛿1\n    dataize: ['𝑒', 𝑒2]") :: Either Yaml.ParseException DataizeRule)
        )
      ,
        ( "in a premise of a contextualization rule"
        , failsWith
            "anonymous meta '!e' cannot be referenced in 'premises' of rule 'foo'"
            (decodeYaml' (inferring "c-match: 𝑘1\nc-result: 𝑛1\npremises:\n  - n-result: 𝑛1\n    normalize: '𝑒'") :: Either Yaml.ParseException ContextualizeRule)
        )
      ,
        ( "in 'c-result' of a contextualization rule"
        , failsWith
            "anonymous meta '!k' cannot be referenced in 'c-result' of rule 'foo'"
            (decodeYaml' (inferring "c-match: 𝑘1\nc-result: '𝑘'") :: Either Yaml.ParseException ContextualizeRule)
        )
      ]
      (\(desc, rejected) -> it ("rejects an anonymous meta " ++ desc) (rejected `shouldBe` True))

  describe "keeps effective labels unique across rule sets" $
    it "across morphing, dataization and contextualization rules" $ do
      let labels :: [String]
          labels =
            map (\MorphRule{name, label} -> fromMaybe name label) morphingRules
              ++ map (\DataizeRule{name, label} -> fromMaybe name label) dataizationRules
              ++ map (\ContextualizeRule{name, label} -> fromMaybe name label) contextualizationRules
      (labels \\ nub labels) `shouldBe` []

  describe "keeps one rule per file in every rule directory" $ do
    let named :: FilePath -> IO [String]
        named dir = map takeBaseName . sort . filter ((== ".yaml") . takeExtension) <$> allPathsIn dir
    morphed <- runIO (named "resources/morphing")
    dataized <- runIO (named "resources/dataization")
    contextualized <- runIO (named "resources/contextualization")
    it "names one morphing file after every morphing rule" $
      morphed `shouldBe` map (\MorphRule{name} -> name) morphingRules
    it "names one dataization file after every dataization rule" $
      dataized `shouldBe` map (\DataizeRule{name} -> name) dataizationRules
    it "names one contextualization file after every contextualization rule" $
      contextualized `shouldBe` map (\ContextualizeRule{name} -> name) contextualizationRules

  describe "reserves 𝑛-family metas for normal forms" $
    it "no contextualize premise in a morphing or dataization rule binds an 𝑛-reserved meta" $ do
      let expressionValued :: Operation -> Bool
          expressionValued OpContextualize{} = True
          expressionValued _ = False
          verbOf :: Operation -> String
          verbOf OpContextualize{} = "contextualize"
          verbOf _ = "?"
          premisesOf :: [(String, [Premise])]
          premisesOf =
            map (\MorphRule{name, premises} -> (name, premises)) morphingRules
              ++ map (\DataizeRule{name, premises} -> (name, premises)) dataizationRules
          offenders :: [String]
          offenders =
            [ ruleName ++ ": " ++ verbOf operation ++ " result '" ++ T.unpack result ++ "'"
            | (ruleName, premises) <- premisesOf
            , Premise{result, operation} <- premises
            , expressionValued operation
            , T.isPrefixOf (T.pack "n") result
            ]
      offenders `shouldBe` []

  describe "parses a 'formation' condition" $
    it "decodes 'formation: <expr>' into IsFormation" $
      case (decodeYaml' "formation: 'Q'" :: Either Yaml.ParseException Condition) of
        Right cond -> cond `shouldBe` IsFormation ExRoot
        Left err -> expectationFailure (Yaml.prettyPrintParseException err)

  describe "rejects a condition object naming no known key" $
    it "fails with 'Unknown condition type'" $
      case (decodeYaml' "{}" :: Either Yaml.ParseException Condition) of
        Left err -> "Unknown condition type" `isInfixOf` Yaml.prettyPrintParseException err `shouldBe` True
        Right _ -> expectationFailure "expected decoding to fail"

  describe "rejects a condition whose arguments count is wrong" $
    forM_
      [ ("'eq' with a single argument", "eq: [1]", "'eq' expects exactly two arguments")
      , ("'gt' with a single argument", "gt: [1]", "'gt' expects exactly two arguments")
      , ("'in' with a single argument", "in: ['!t']", "'in' expects exactly two arguments")
      , ("'matches' with a single argument", "matches: ['hi']", "'matches' expects exactly two arguments")
      , ("'part-of' with a single argument", "part-of: ['!e']", "'part-of' expects exactly two arguments")
      , ("'disjoint' with a single argument", "disjoint: [[]]", "'disjoint' expects exactly two arguments")
      ]
      (\(desc, yaml, message) -> it desc ((decodeYaml' yaml :: Either Yaml.ParseException Condition) `shouldSatisfy` failsWith message))

  describe "rejects a malformed premise" $
    forM_
      [ ("fails when neither 'n-result' nor 'd-result' is present", "morph: [𝑛, 𝑒]")
      , ("fails when 'n-result' is not an expression meta", "n-result: Q\nmorph: [𝑛, 𝑒]")
      , ("fails when 'd-result' is not a bytes meta", "d-result: '--'\ndataize: [𝑛, 𝑒]")
      , ("fails when 'morph' does not take exactly two arguments", "n-result: 𝑛1\nmorph: [𝑛2]")
      , ("fails when 'evaluate' does not take exactly two arguments", "n-result: 𝑛1\nevaluate: [𝑛2]")
      , ("fails when 'contextualize' does not take exactly two arguments", "n-result: 𝑛1\ncontextualize: [𝑛2]")
      , ("fails when 'dataize' does not take exactly two arguments", "d-result: 𝛿1\ndataize: [𝑛1]")
      ]
      (\(desc, yaml) -> it desc ((decodeYaml' yaml :: Either Yaml.ParseException Premise) `shouldSatisfy` isLeft))

  describe "reads the universe a premise names" $
    forM_
      [ ("beside the term of 'morph'", "n-result: 𝑛1\nmorph: [𝑛2, 𝑒1]", Premise{result = T.pack "n1", operation = OpMorph (ExMeta (T.pack "n2")) (ExMeta (T.pack "e1"))})
      , ("beside the term of 'dataize'", "d-result: 𝛿1\ndataize: [𝑛1, 𝑒1]", Premise{result = T.pack "d1", operation = OpDataize (ExMeta (T.pack "n1")) (ExMeta (T.pack "e1"))})
      ]
      (\(desc, yaml, premise) -> it desc (either (const Nothing) Just (decodeYaml' yaml) `shouldBe` Just premise))

  describe "rejects a numerable expression that is neither an object, a number nor an index meta" $
    it "fails on a bare boolean" $
      (decodeYaml' "true" :: Either Yaml.ParseException Number) `shouldSatisfy` isLeft

  describe "parses a literal number" $
    it "accepts a whole number" $
      (decodeYaml' "5" :: Either Yaml.ParseException Number) `shouldSatisfy` (not . isLeft)

  describe "rejects a fractional literal number" $
    it "fails on a fraction instead of silently rounding it" $
      (decodeYaml' "2.5" :: Either Yaml.ParseException Number) `shouldSatisfy` isLeft

  describe "rejects an empty 'and' condition" $
    it "fails on 'and: []'" $
      (decodeYaml' "and: []" :: Either Yaml.ParseException Condition) `shouldSatisfy` isLeft

  describe "rejects an empty 'or' condition" $
    it "fails on 'or: []'" $
      (decodeYaml' "or: []" :: Either Yaml.ParseException Condition) `shouldSatisfy` isLeft