phino-0.0.158: src/Dataize.hs

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}

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

module Dataize (dataize, dataize', reduction, Outcome (..)) where

import AST
import Control.Exception (throwIO, try)
import Control.Monad (unless, when)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Maybe (listToMaybe)
import qualified Data.Text as T
import Deps (Evaluation (..), Judgment (..), State (..), resited)
import Engine (Engine (..))
import qualified Inference as In
import Locator (locatedExpression)
import Morph (Morphed, ReduceContext (..), ReduceException (..), ReductionFunc, deeper, entering, inferred, insideUniverse, leadsTo, onward, opening, parking, universed)
import Rewriter (Rewritten)

type Dataized = (Bytes, [Rewritten])

type Dataizable = Morphed

data Outcome
  = Dataized Bytes
  | Residual Expression
  deriving stock (Eq, Show)

dataize :: Expression -> State -> ReduceContext -> IO (Outcome, [Rewritten], State)
dataize universe state ctx@ReduceContext{..} = do
  expr <- locatedExpression _locator universe
  result <- try (dataize' (expr, (universe, Nothing) :| []) universe state ctx)
  case result of
    Right ((bytes, seq), state') -> pure (Dataized bytes, reverse seq, state')
    Left (StuckAt func seq parked) | _partial -> residual seq parked{_stuck = Just func}
    Left (OutOfStepsAt _ seq parked) | _partial -> residual seq parked
    Left (LoopingAt _ seq parked) | _partial -> residual seq parked
    Left (Undataizable term seq parked) | _partial -> do
      unless (dead `elem` _parked) (_saveEval (EvStuck _nesting dead Dataization term))
      residual seq parked{_stuck = Just dead}
    Left failure -> throwIO (failure :: ReduceException)
  where
    dead :: T.Text
    dead = "⊥"
    residual :: NonEmpty Rewritten -> State -> IO (Outcome, [Rewritten], State)
    residual seq parked = do
      residue <- locatedExpression _locator (fst (NE.head seq))
      pure (Residual residue, reverse (NE.toList seq), parked)

dataize' :: Dataizable -> Expression -> State -> ReduceContext -> IO (Dataized, State)
dataize' (expr, seq) univ state caller = do
  ctx <- opening Dataization =<< deeper =<< entering expr =<< parking seq state (universed univ caller{_judgment = Dataization})
  parking seq state $ case unknown expr of
    Just idx -> manufactured idx ctx
    Nothing -> do
      reached <- inferred expr univ state ctx ctx._engine._dataization
      case reached of
        Just (In.Answered step bts, state') -> do
          when (step == (Dataization, "delta")) (ctx._saveEval (EvDelta ctx._nesting bts))
          seq' <- leadsTo seq step (ExBytes bts) ctx
          pure ((bts, NE.toList seq'), state'{_manufactured = Nothing})
        Just (In.Onward way built world, state') -> do
          ctx' <- boxing way built ctx
          (dataizable, state'') <- onward seq state' way built ctx'
          dataize' dataizable world state'' ctx'
        Nothing -> throwIO (Undataizable expr seq state)
  where
    boxing :: In.Way -> Expression -> ReduceContext -> IO ReduceContext
    boxing way built ctx
      | way == In.Normalized (Dataization, "box") = do
          ctx._saveEval (EvBoxed ctx._nesting built)
          pure ctx{_saveEval = ctx._saveEval . resited ctx._site built}
      | otherwise = pure ctx
    unknown :: Expression -> Maybe Int
    unknown (ExFormation bds) = listToMaybe [idx | BiLambda (FnSymbol idx) <- bds]
    unknown _ = Nothing
    manufactured :: Int -> ReduceContext -> IO (Dataized, State)
    manufactured idx ctx = do
      ctx._saveEval (EvManufactured ctx._nesting idx)
      seq' <- leadsTo seq (Dataization, "symbol") (ExBytes datum) ctx
      pure ((datum, NE.toList seq'), state{_manufactured = Just idx})

reduction :: ReductionFunc
reduction univ ctx expr state = do
  (universe, aiming) <- insideUniverse expr univ ctx
  (outcome, _, state') <- dataize universe state aiming
  pure (reached outcome, state')
  where
    reached :: Outcome -> Maybe Bytes
    reached (Dataized bytes) = Just bytes
    reached (Residual _) = Nothing

datum :: Bytes
datum = BtMany ["40", "45", "00", "00", "00", "00", "00", "00"]