{-# 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, carried, deeper, inferred, insideUniverse, leadsTo, onward, opening, parking, severing, universed)
import Rewriter (Rewritten)

type Dataized = (Bytes, [Rewritten])

type Dataizable = Morphed

data Outcome
  = Dataized Bytes
  | Residual Expression
  deriving stock (Outcome -> Outcome -> Bool
(Outcome -> Outcome -> Bool)
-> (Outcome -> Outcome -> Bool) -> Eq Outcome
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Outcome -> Outcome -> Bool
== :: Outcome -> Outcome -> Bool
$c/= :: Outcome -> Outcome -> Bool
/= :: Outcome -> Outcome -> Bool
Eq, Int -> Outcome -> ShowS
[Outcome] -> ShowS
Outcome -> String
(Int -> Outcome -> ShowS)
-> (Outcome -> String) -> ([Outcome] -> ShowS) -> Show Outcome
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Outcome -> ShowS
showsPrec :: Int -> Outcome -> ShowS
$cshow :: Outcome -> String
show :: Outcome -> String
$cshowList :: [Outcome] -> ShowS
showList :: [Outcome] -> ShowS
Show)

dataize :: Expression -> State -> ReduceContext -> IO (Outcome, [Rewritten], State)
dataize :: Expression
-> State -> ReduceContext -> IO (Outcome, [Rewritten], State)
dataize Expression
universe State
state ctx :: ReduceContext
ctx@ReduceContext{Bool
Int
[Text]
Maybe (Int, Judgment, Expression)
Maybe (Expression, [Binding], Expression)
Maybe Expression
Maybe Acyclic
Maybe Memo
Maybe Deadline
Maybe Tally
IORef Int
Seen
Expression
Judgment
Lambdas
Engine
Steps
BuildTermFunc
SaveStepFunc
ReductionFunc
Evaluation -> IO ()
EvaluationFunc
_locator :: Expression
_site :: Expression
_universe :: Maybe Expression
_maxDepth :: Int
_maxCycles :: Int
_steps :: Steps
_tally :: Maybe Tally
_minted :: IORef Int
_deadline :: Maybe Deadline
_memo :: Maybe Memo
_nesting :: Int
_opened :: Maybe (Int, Judgment, Expression)
_depthSensitive :: Bool
_shuffle :: Bool
_partial :: Bool
_acyclic :: Maybe Acyclic
_maxLoops :: Int
_judgment :: Judgment
_parked :: [Text]
_entered :: Seen
_placed :: Maybe (Expression, [Binding], Expression)
_symbolic :: Lambdas
_buildTerm :: BuildTermFunc
_reduce :: ReductionFunc
_evaluate :: EvaluationFunc
_saveStep :: SaveStepFunc
_saveEval :: Evaluation -> IO ()
_engine :: Engine
$sel:_locator:ReduceContext :: ReduceContext -> Expression
$sel:_site:ReduceContext :: ReduceContext -> Expression
$sel:_universe:ReduceContext :: ReduceContext -> Maybe Expression
$sel:_maxDepth:ReduceContext :: ReduceContext -> Int
$sel:_maxCycles:ReduceContext :: ReduceContext -> Int
$sel:_steps:ReduceContext :: ReduceContext -> Steps
$sel:_tally:ReduceContext :: ReduceContext -> Maybe Tally
$sel:_minted:ReduceContext :: ReduceContext -> IORef Int
$sel:_deadline:ReduceContext :: ReduceContext -> Maybe Deadline
$sel:_memo:ReduceContext :: ReduceContext -> Maybe Memo
$sel:_nesting:ReduceContext :: ReduceContext -> Int
$sel:_opened:ReduceContext :: ReduceContext -> Maybe (Int, Judgment, Expression)
$sel:_depthSensitive:ReduceContext :: ReduceContext -> Bool
$sel:_shuffle:ReduceContext :: ReduceContext -> Bool
$sel:_partial:ReduceContext :: ReduceContext -> Bool
$sel:_acyclic:ReduceContext :: ReduceContext -> Maybe Acyclic
$sel:_maxLoops:ReduceContext :: ReduceContext -> Int
$sel:_judgment:ReduceContext :: ReduceContext -> Judgment
$sel:_parked:ReduceContext :: ReduceContext -> [Text]
$sel:_entered:ReduceContext :: ReduceContext -> Seen
$sel:_placed:ReduceContext :: ReduceContext -> Maybe (Expression, [Binding], Expression)
$sel:_symbolic:ReduceContext :: ReduceContext -> Lambdas
$sel:_buildTerm:ReduceContext :: ReduceContext -> BuildTermFunc
$sel:_reduce:ReduceContext :: ReduceContext -> ReductionFunc
$sel:_evaluate:ReduceContext :: ReduceContext -> EvaluationFunc
$sel:_saveStep:ReduceContext :: ReduceContext -> SaveStepFunc
$sel:_saveEval:ReduceContext :: ReduceContext -> Evaluation -> IO ()
$sel:_engine:ReduceContext :: ReduceContext -> Engine
..} = do
  Expression
expr <- Expression -> Expression -> IO Expression
locatedExpression Expression
_locator Expression
universe
  Either ReduceException (Dataized, State)
result <- IO (Dataized, State)
-> IO (Either ReduceException (Dataized, State))
forall e a. Exception e => IO a -> IO (Either e a)
try (Dataizable
-> Expression -> State -> ReduceContext -> IO (Dataized, State)
dataize' (Expression
expr, (Expression
universe, Maybe (Judgment, String)
forall a. Maybe a
Nothing) Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| []) Expression
universe State
state ReduceContext
ctx)
  case Either ReduceException (Dataized, State)
result of
    Right ((Bytes
bytes, [Rewritten]
seq), State
state') -> (Outcome, [Rewritten], State) -> IO (Outcome, [Rewritten], State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bytes -> Outcome
Dataized Bytes
bytes, [Rewritten] -> [Rewritten]
forall a. [a] -> [a]
reverse [Rewritten]
seq, State
state')
    Left (StuckAt Text
func NonEmpty Rewritten
seq State
parked) | Bool
_partial -> NonEmpty Rewritten -> State -> IO (Outcome, [Rewritten], State)
residual NonEmpty Rewritten
seq State
parked{_stuck = Just func}
    Left (OutOfStepsAt Budget
_ NonEmpty Rewritten
seq State
parked) | Bool
_partial -> NonEmpty Rewritten -> State -> IO (Outcome, [Rewritten], State)
residual NonEmpty Rewritten
seq State
parked
    Left (LoopingAt Expression
_ NonEmpty Rewritten
seq State
parked) | Bool
_partial -> NonEmpty Rewritten -> State -> IO (Outcome, [Rewritten], State)
residual NonEmpty Rewritten
seq State
parked
    Left (Undataizable Expression
term NonEmpty Rewritten
seq State
parked) | Bool
_partial -> do
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Text
dead Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
_parked) (Evaluation -> IO ()
_saveEval (Int -> Text -> Judgment -> Expression -> Evaluation
EvStuck Int
_nesting Text
dead Judgment
Dataization Expression
term))
      NonEmpty Rewritten -> State -> IO (Outcome, [Rewritten], State)
residual NonEmpty Rewritten
seq State
parked{_stuck = Just dead}
    Left ReduceException
failure -> ReduceException -> IO (Outcome, [Rewritten], State)
forall e a. Exception e => e -> IO a
throwIO (ReduceException
failure :: ReduceException)
  where
    dead :: T.Text
    dead :: Text
dead = Text
"⊥"
    residual :: NonEmpty Rewritten -> State -> IO (Outcome, [Rewritten], State)
    residual :: NonEmpty Rewritten -> State -> IO (Outcome, [Rewritten], State)
residual NonEmpty Rewritten
seq State
parked = do
      Expression
residue <- Expression -> Expression -> IO Expression
locatedExpression Expression
_locator (Rewritten -> Expression
forall a b. (a, b) -> a
fst (NonEmpty Rewritten -> Rewritten
forall a. NonEmpty a -> a
NE.head NonEmpty Rewritten
seq))
      (Outcome, [Rewritten], State) -> IO (Outcome, [Rewritten], State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Outcome
Residual Expression
residue, [Rewritten] -> [Rewritten]
forall a. [a] -> [a]
reverse (NonEmpty Rewritten -> [Rewritten]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty Rewritten
seq), State
parked)

dataize' :: Dataizable -> Expression -> State -> ReduceContext -> IO (Dataized, State)
dataize' :: Dataizable
-> Expression -> State -> ReduceContext -> IO (Dataized, State)
dataize' (Expression
start, NonEmpty Rewritten
seq) Expression
univ State
held ReduceContext
caller = do
  let (State
state, ReduceContext
aware) = State -> ReduceContext -> (State, ReduceContext)
carried State
held ReduceContext
caller
  (Expression
expr, ReduceContext
entered) <- Expression
-> Expression
-> State
-> ReduceContext
-> IO (Expression, ReduceContext)
severing Expression
start Expression
univ State
state (ReduceContext -> IO (Expression, ReduceContext))
-> IO ReduceContext -> IO (Expression, ReduceContext)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< NonEmpty Rewritten -> State -> IO ReduceContext -> IO ReduceContext
forall a. NonEmpty Rewritten -> State -> IO a -> IO a
parking NonEmpty Rewritten
seq State
state (Expression -> ReduceContext -> IO ReduceContext
universed Expression
univ ReduceContext
aware{_judgment = Dataization})
  ReduceContext
ctx <- Judgment -> ReduceContext -> IO ReduceContext
opening Judgment
Dataization (ReduceContext -> IO ReduceContext)
-> IO ReduceContext -> IO ReduceContext
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReduceContext -> IO ReduceContext
deeper ReduceContext
entered
  NonEmpty Rewritten
-> State -> IO (Dataized, State) -> IO (Dataized, State)
forall a. NonEmpty Rewritten -> State -> IO a -> IO a
parking NonEmpty Rewritten
seq State
state (IO (Dataized, State) -> IO (Dataized, State))
-> IO (Dataized, State) -> IO (Dataized, State)
forall a b. (a -> b) -> a -> b
$ case Expression -> Maybe Int
unknown Expression
expr of
    Just Int
idx -> Int -> State -> ReduceContext -> IO (Dataized, State)
manufactured Int
idx State
state ReduceContext
ctx
    Maybe Int
Nothing -> do
      Maybe (Conclusion Bytes, State)
reached <- Expression
-> Expression
-> State
-> ReduceContext
-> [Inference Bytes]
-> IO (Maybe (Conclusion Bytes, State))
forall value.
Expression
-> Expression
-> State
-> ReduceContext
-> [Inference value]
-> IO (Maybe (Conclusion value, State))
inferred Expression
expr Expression
univ State
state ReduceContext
ctx ReduceContext
ctx._engine._dataization
      case Maybe (Conclusion Bytes, State)
reached of
        Just (In.Answered (Judgment, String)
step Bytes
bts, State
state') -> do
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Judgment, String)
step (Judgment, String) -> (Judgment, String) -> Bool
forall a. Eq a => a -> a -> Bool
== (Judgment
Dataization, String
"delta")) (ReduceContext
ctx._saveEval (Int -> Bytes -> Evaluation
EvDelta ReduceContext
ctx._nesting Bytes
bts))
          NonEmpty Rewritten
seq' <- NonEmpty Rewritten
-> (Judgment, String)
-> Expression
-> ReduceContext
-> IO (NonEmpty Rewritten)
leadsTo NonEmpty Rewritten
seq (Judgment, String)
step (Bytes -> Expression
ExBytes Bytes
bts) ReduceContext
ctx
          (Dataized, State) -> IO (Dataized, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Bytes
bts, NonEmpty Rewritten -> [Rewritten]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty Rewritten
seq'), State
state'{_manufactured = Nothing})
        Just (In.Onward Way
way Expression
built Expression
world, State
state') -> do
          ReduceContext
ctx' <- Way -> Expression -> ReduceContext -> IO ReduceContext
boxing Way
way Expression
built ReduceContext
ctx
          (Dataizable
dataizable, State
state'') <- NonEmpty Rewritten
-> State
-> Way
-> Expression
-> ReduceContext
-> IO (Dataizable, State)
onward NonEmpty Rewritten
seq State
state' Way
way Expression
built ReduceContext
ctx'
          Dataizable
-> Expression -> State -> ReduceContext -> IO (Dataized, State)
dataize' Dataizable
dataizable Expression
world State
state'' ReduceContext
ctx'
        Maybe (Conclusion Bytes, State)
Nothing -> ReduceException -> IO (Dataized, State)
forall e a. Exception e => e -> IO a
throwIO (Expression -> NonEmpty Rewritten -> State -> ReduceException
Undataizable Expression
expr NonEmpty Rewritten
seq State
state)
  where
    boxing :: In.Way -> Expression -> ReduceContext -> IO ReduceContext
    boxing :: Way -> Expression -> ReduceContext -> IO ReduceContext
boxing Way
way Expression
built ReduceContext
ctx
      | Way
way Way -> Way -> Bool
forall a. Eq a => a -> a -> Bool
== (Judgment, String) -> Way
In.Normalized (Judgment
Dataization, String
"box") = do
          ReduceContext
ctx._saveEval (Int -> Expression -> Evaluation
EvBoxed ReduceContext
ctx._nesting Expression
built)
          ReduceContext -> IO ReduceContext
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ReduceContext
ctx{_saveEval = ctx._saveEval . resited ctx._site built}
      | Bool
otherwise = ReduceContext -> IO ReduceContext
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ReduceContext
ctx
    unknown :: Expression -> Maybe Int
    unknown :: Expression -> Maybe Int
unknown (ExFormation [Binding]
bds) = [Int] -> Maybe Int
forall a. [a] -> Maybe a
listToMaybe [Int
idx | BiLambda (FnSymbol Int
idx) <- [Binding]
bds]
    unknown Expression
_ = Maybe Int
forall a. Maybe a
Nothing
    manufactured :: Int -> State -> ReduceContext -> IO (Dataized, State)
    manufactured :: Int -> State -> ReduceContext -> IO (Dataized, State)
manufactured Int
idx State
state ReduceContext
ctx = do
      ReduceContext
ctx._saveEval (Int -> Int -> Evaluation
EvManufactured ReduceContext
ctx._nesting Int
idx)
      NonEmpty Rewritten
seq' <- NonEmpty Rewritten
-> (Judgment, String)
-> Expression
-> ReduceContext
-> IO (NonEmpty Rewritten)
leadsTo NonEmpty Rewritten
seq (Judgment
Dataization, String
"symbol") (Bytes -> Expression
ExBytes Bytes
datum) ReduceContext
ctx
      (Dataized, State) -> IO (Dataized, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Bytes
datum, NonEmpty Rewritten -> [Rewritten]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty Rewritten
seq'), State
state{_manufactured = Just idx})

reduction :: ReductionFunc
reduction :: ReductionFunc
reduction Expression
univ ReduceContext
ctx Expression
expr State
state = do
  (Expression
universe, ReduceContext
aiming) <- Expression
-> Expression -> ReduceContext -> IO (Expression, ReduceContext)
insideUniverse Expression
expr Expression
univ ReduceContext
ctx
  (Outcome
outcome, [Rewritten]
_, State
state') <- Expression
-> State -> ReduceContext -> IO (Outcome, [Rewritten], State)
dataize Expression
universe State
state ReduceContext
aiming
  (Maybe Bytes, State) -> IO (Maybe Bytes, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Outcome -> Maybe Bytes
reached Outcome
outcome, State
state')
  where
    reached :: Outcome -> Maybe Bytes
    reached :: Outcome -> Maybe Bytes
reached (Dataized Bytes
bytes) = Bytes -> Maybe Bytes
forall a. a -> Maybe a
Just Bytes
bytes
    reached (Residual Expression
_) = Maybe Bytes
forall a. Maybe a
Nothing

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