phino-0.0.134: test/Fixtures.hs

{-# LANGUAGE OverloadedStrings #-}

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

-- The λ functions the specs fire. phino implements none of them, so a spec that
-- needs one to answer brings its own: the fixture file
-- 'test-resources/atoms.yaml', which spells them in the very rule language
-- '--symbolic' reads, or a file of its own written for the occasion.
module Fixtures
  ( defaultReduceContext
  , fixtureLambdas
  , lambdasFile
  , loopingLambdas
  , primitives
  , readUtf8
  , recorded
  , recorded'
  , withLambdas
  , withLambdasOf
  , withTemp
  )
where

import AST (Expression (ExRoot))
import CLI.Helpers (withEvalFunc)
import CLI.Types (IOFormat (PHI), PrintContext (PrintCtx))
import Control.Exception (bracket, evaluate)
import Data.ByteString qualified as BS
import Data.Map.Strict qualified as Map
import Data.Text qualified as T
import Data.Text.Encoding (encodeUtf8)
import Dataize (reduction)
import Deps (Judgment (..), SaveEvalFunc, dontSaveEval, dontSaveStep)
import Evaluate (evaluation, fired)
import Functions (buildTerm)
import Lambdas (Lambdas, emptyLambdas, readLambdas)
import Lining (LineFormat (MULTILINE))
import Morph (ReduceContext (..), Steps (..))
import Sugar (SugarType (SWEET))
import System.Directory (getTemporaryDirectory, removePathForcibly)
import System.IO (Handle, IOMode (ReadMode), hClose, hGetContents, hSetEncoding, openBinaryTempFile, utf8, withFile)
import XMIR (defaultXmirContext)

-- The context every reduction of a spec starts from. Shuffle is enabled so the
-- suite exercises the order-independence of the morphing and dataization rules
-- (#909): a hidden overlap surfaces as a nondeterministic failure instead of
-- staying silently green. No λ function is registered, since phino implements
-- none of them: a case that needs one to answer brings the fixture file in
-- through 'withLambdas'.
defaultReduceContext :: Expression -> ReduceContext
defaultReduceContext loc = ReduceContext loc loc Nothing 25 25 (Steps 250 0) 1 False True False False False Morphing [] Map.empty Map.empty emptyLambdas buildTerm reduction evaluation fired dontSaveStep dontSaveEval

-- The same context with the given λ functions registered
withLambdas :: Lambdas -> ReduceContext -> ReduceContext
withLambdas lambdas ctx = ctx{_symbolic = lambdas}

-- The file '--symbolic' reads in every case that fires one of the fixture λ
-- functions, for the specs that go through the command line.
lambdasFile :: FilePath
lambdasFile = "test-resources/atoms.yaml"

-- The same λ functions, read once, for the specs that drive 𝕄 and 𝔻 directly.
fixtureLambdas :: IO Lambdas
fixtureLambdas = readLambdas lambdasFile

-- The one λ function that answers with a firing of itself, so that a run fires
-- it until the step budget is gone. Recursion is nothing phino prevents on its
-- own — that is the object model's business — so a program built on this one is
-- how the specs reach the '--max-steps' limit, and how they ask '--acyclic' to
-- end the same run before the limit does.
loopingLambdas :: (FilePath -> IO a) -> IO a
loopingLambdas = withLambdasOf "- λ: L_loop\n  𝑛: ⟦ λ ⤍ L_loop ⟧\n"

-- The given λ functions, as the YAML file '--symbolic' reads, in a temporary
-- file removed afterwards.
withLambdasOf :: T.Text -> (FilePath -> IO a) -> IO a
withLambdasOf lambdas = withTemp "phino-symbolic-.yaml" (encodeUtf8 lambdas)

-- The EO objects the fixture λ functions answer for, declared the way
-- 'number.eo', 'bytes.eo' and 'bool.eo' declare them, so a case only has to
-- spell the expression under φ. 'number.eq' is the one operation with no λ
-- function of its own: EO spells it out of 'L_bytes_eq' (eq.eo), so the fixture
-- composes it the same way, and 'bool.if' is where a branch meets the symbol
-- its condition came down to. 'number.nope' is declared and left out of the
-- file on purpose: it is the λ function that cannot fire, the one '--partial'
-- parks on.
primitives :: String -> String
primitives src =
  unlines
    [ "[["
    , "  bytes -> [["
    , "    φ -> ?,"
    , "    not -> [[ L> L_bytes_not ]],"
    , "    eq -> [[ b -> ?, L> L_bytes_eq ]]"
    , "  ]],"
    , "  bool -> [["
    , "    φ -> ?,"
    , "    if -> [[ then -> ?, else -> ?, L> L_fork ]]"
    , "  ]],"
    , "  number -> [["
    , "    φ -> ?,"
    , "    as-bytes -> $.φ,"
    , "    plus -> [[ x -> ?, L> L_number_plus ]],"
    , "    times -> [[ x -> ?, L> L_number_times ]],"
    , "    div -> [[ x -> ?, L> L_number_div ]],"
    , "    gt -> [[ x -> ?, L> L_number_gt ]],"
    , "    eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]],"
    , "    nope -> [[ L> L_number_nope ]]"
    , "  ]],"
    , "  @ -> " ++ src
    , "]]"
    ]

-- Run the action with the function '--protocol' writes the run through, handing
-- back what it wrote alongside the answer, verbatim. The protocol goes through
-- the very plumbing the option runs, and it is handed back as the text of the
-- file and not as the lines of it, so a case asserting it asserts the very
-- bytes a user of the option reads back — the indentation of every record, the
-- order they stand in and the line the file ends on included.
recorded :: (SaveEvalFunc -> IO a) -> IO (a, String)
recorded = recorded' False

-- The same, with the ρ bindings of every term dropped when asked, the way
-- '--hide-rho' drops them: a caller reading a protocol back for the terms an
-- entry answered with has no business reading the universe those terms were
-- fired inside, and the flag is what says so.
recorded' :: Bool -> (SaveEvalFunc -> IO a) -> IO (a, String)
recorded' hidden action =
  withTemp "phino-protocol-.txt" BS.empty $ \path -> do
    answer <- withEvalFunc (Just path) printing action
    written <- readUtf8 path
    pure (answer, written)
  where
    -- The protocol flattens every term itself, so the only things this context
    -- decides are that the terms are 𝜑 and not XMIR and whether they carry
    -- their ρ bindings.
    printing :: PrintContext
    printing =
      PrintCtx
        SWEET
        hidden
        MULTILINE
        2
        defaultXmirContext
        False
        False
        False
        False
        False
        1
        1
        ExRoot
        Nothing
        Nothing
        Nothing
        PHI

-- Read a text file phino wrote, in the encoding it wrote it with. The whole
-- content is forced before the handle closes, since a lazy read of a closed
-- handle answers nothing. The file is read as text and not as bytes, so the
-- line terminator the platform writes is the one it reads back: on Windows
-- every line of a text file ends CRLF, and a case asserting the content of one
-- has no business seeing that.
readUtf8 :: FilePath -> IO String
readUtf8 path =
  withFile path ReadMode $ \stream -> do
    hSetEncoding stream utf8
    content <- hGetContents stream
    _ <- evaluate (length content)
    pure content

-- Write the content to a fresh temporary file, hand its path to the action and
-- delete the file afterwards.
withTemp :: String -> BS.ByteString -> (FilePath -> IO a) -> IO a
withTemp template content action = do
  dir <- getTemporaryDirectory
  bracket (openBinaryTempFile dir template) discarded $ \(path, handle) -> do
    BS.hPut handle content
    hClose handle
    action path
  where
    discarded :: (FilePath, Handle) -> IO ()
    discarded (path, handle) = hClose handle >> removePathForcibly path