phino-0.0.154: src/Evaluate.hs

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

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

module Evaluate (evaluation) where

import AST
import Builder (buildExpressionThrows)
import Control.Exception (throwIO, try)
import Control.Monad (foldM, unless)
import Data.IORef (readIORef, writeIORef)
import Data.List (partition)
import Data.List.NonEmpty (NonEmpty (..))
import Data.Maybe (fromMaybe, listToMaybe)
import qualified Data.Text as T
import Deps (Evaluation (..), Judgment (Evaluation, Morphing), State (..), resited)
import Engine (Engine (..))
import Lambdas (Lambda (..), Meta (..), joined, matched, message, minted, symbolized, thrown)
import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot)
import Morph (Answer, Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), charged, counted, deeper, entering, isLambda, lambda, morphing, normalized, opening, recalled, remember, remembered, retained, settled, starved, unparked)
import Printer (printFunction)
import Rule (RuleContext (RuleContext), matchExpressionWithRule', xiFree)
import Text.Printf (printf)
import qualified Yaml as Y

evaluation :: ReduceContext -> State -> Expression -> Expression -> IO (Expression, State)
evaluation ctx state form univ = case form of
  ExFormation bds
    | not (any isLambda bds) -> pure (form, state)
    | otherwise -> case lambda bds of
        Just (func, args) -> do
          (raw, state') <- symbol func form args univ state ctx
          (normal, _) <- normalized raw ((univ, Nothing) :| []) ctx
          pure (normal, state')
        Nothing -> case unknown bds of
          Just idx -> stuck idx form
          Nothing -> throwIO (userError "Function evaluate() expects a formation with a single λ binding naming a function")
  _ -> throwIO (userError "Function evaluate() expects a formation")
  where
    unknown :: [Binding] -> Maybe Int
    unknown bindings = case partition isLambda bindings of
      ([BiLambda (FnSymbol idx)], _) -> Just idx
      _ -> Nothing
    stuck :: Int -> Expression -> IO (Expression, State)
    stuck idx form = do
      unless (name `elem` ctx._parked) (ctx._saveEval (EvStuck ctx._nesting name ctx._judgment form))
      throwIO (Stuck name)
      where
        name :: T.Text
        name = T.pack (printFunction (FnSymbol idx))

symbol :: T.Text -> Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)
symbol func form self univ state caller = case matched caller._symbolic func of
  Nothing -> do
    unless (func `elem` caller._parked) (caller._saveEval (EvStuck caller._nesting func caller._judgment form))
    throwIO (Stuck func)
  Just entry -> do
    known <- recalled caller._memo form caller._steps._spent
    maybe (made entry) told known
  where
    made :: Lambda -> IO (Expression, State)
    made entry = do
      charged caller
      stamp <- counted caller._memo
      exhausted <- starved caller._memo
      caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)
      let ctx = caller{_nesting = caller._nesting + 1}
      outcome <- try $ do
        (bound, dataized, conditions) <- foldM (down ctx) (substEmpty, state, []) entry._dataized
        (bound', morphed, normals) <- foldM (through ctx) (bound, dataized, []) entry._morphed
        let firing = Firing func (reverse conditions) (reverse normals)
        known <- remembered caller._memo firing
        maybe (worked ctx entry firing bound' morphed) (\answer -> (answer, morphed) <$ shown ctx._nesting answer) known
      case outcome of
        Right (answer, state') -> do
          retained caller._memo form stamp (Answered answer)
          pure (snd answer, state')
        Left failure -> do
          exhausted' <- starved caller._memo
          mapM_ (retained caller._memo form stamp) (kept (exhausted' /= exhausted) failure)
          mapM_ (caller._saveEval . EvStuckOn (caller._nesting + 1)) (stranded failure)
          throwIO failure
    worked :: ReduceContext -> Lambda -> Firing -> Subst -> State -> IO (Answer, State)
    worked ctx entry firing@(Firing _ operands _) bound state' = do
      (fired, state'') <- foldM (evaluated ctx entry) (bound, state') entry._evaluated
      rewrote <- foldM (reshaped ctx) fired entry._rewritten
      stood <- foldM (masked ctx) rewrote entry._symbolized
      (forked, joining) <- foldM (paired ctx entry (listToMaybe operands)) (stood, state'') entry._paired
      (answer, state''') <- answered ctx entry operands forked joining
      remember caller._memo firing answer
      pure (answer, state''')
    shown :: Int -> Answer -> IO ()
    shown depth (built, normal) = do
      caller._saveEval (EvBuilt depth built)
      caller._saveEval (EvAnswer depth normal)
    kept :: Bool -> ReduceException -> Maybe Kept
    kept _ (Looping term) = Just (Looped term)
    kept _ (LoopingAt term _ _) = Just (Looped term)
    kept starving (Stuck name) = Just (Stalled name (least starving))
    kept starving (StuckAt name _ _) = Just (Stalled name (least starving))
    kept _ _ = Nothing
    least :: Bool -> Int
    least True = caller._steps._spent
    least False = 0
    stranded :: ReduceException -> Maybe T.Text
    stranded (Stuck name) = Just name
    stranded (StuckAt name _ _) = Just name
    stranded _ = Nothing
    told :: Kept -> IO (Expression, State)
    told (Answered answer) = do
      caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)
      shown (caller._nesting + 1) answer
      pure (snd answer, state)
    told (Looped term) = do
      caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)
      mapM_ (\mode -> caller._saveEval (EvLooped (caller._nesting + 1) caller._judgment mode term caller._site)) caller._acyclic
      throwIO (Looping term)
    told (Stalled name _) = do
      caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)
      caller._saveEval (EvStall (caller._nesting + 1) name)
      throwIO (Stuck name)
    down :: ReduceContext -> (Subst, State, [Either Int Bytes]) -> (Meta, Expression) -> IO (Subst, State, [Either Int Bytes])
    down ctx (bound, state', conditions) (meta, term) = do
      placed <- operand term
      (value, state'') <- unparked (ctx._reduce univ ctx placed state'{_manufactured = Nothing, _stuck = Nothing})
      case value of
        Nothing -> throwIO (Stuck (fromMaybe func state''._stuck))
        Just bytes -> do
          let datum = maybe (Right bytes) Left state''._manufactured
          ctx._saveEval (EvData ctx._nesting meta._spelling term datum)
          bound' <- bind meta (MvBytes bytes) bound
          pure (bound', state'', datum : conditions)
    through :: ReduceContext -> (Subst, State, [Expression]) -> (Meta, Expression) -> IO (Subst, State, [Expression])
    through ctx (bound, state', normals) (meta, term) = do
      placed <- operand term
      (normal, state'') <- morphing univ ctx placed state'
      ctx._saveEval (EvTerm ctx._nesting meta._spelling Morphing term normal)
      bound' <- bind meta (MvExpression normal) bound
      pure (bound', state'', normal : normals)
    evaluated :: ReduceContext -> Lambda -> (Subst, State) -> (Meta, Meta) -> IO (Subst, State)
    evaluated ctx entry (bound, state') (meta, source) = do
      term <- buildExpressionThrows (ExMeta source._name) bound
      (answer, state'') <- fire ctx entry source state' term
      ctx._saveEval (EvTerm ctx._nesting meta._spelling Evaluation (ExMeta source._name) answer)
      bound' <- bind meta (MvExpression answer) bound
      pure (bound', state'')
    fire :: ReduceContext -> Lambda -> Meta -> State -> Expression -> IO (Expression, State)
    fire _ entry _ state' term
      | raising entry term = pure (term, state')
    fire ctx _ source state' term@(ExFormation _) = do
      entered <- deeper =<< entering term ctx{_judgment = Evaluation, _site = ExMeta source._name}
      evaluation entered state' term univ
    fire _ _ _ _ _ = throwIO (Stuck func)
    reshaped :: ReduceContext -> Subst -> (Meta, (Meta, [Y.Rule])) -> IO Subst
    reshaped ctx bound (meta, (source, rules)) = do
      term <- buildExpressionThrows (ExMeta source._name) bound
      shaped <- rewritten rules (RuleContext ctx._buildTerm Nothing ctx._engine._normal) term
      ctx._saveEval (EvSymbolize ctx._nesting meta._spelling (ExMeta source._name) shaped)
      bind meta (MvExpression shaped) bound
    masked :: ReduceContext -> Subst -> (Meta, Expression) -> IO Subst
    masked ctx bound (meta, term) = do
      reduced <- buildExpressionThrows term bound
      (stood, known, spent) <- symbolized reduced <$> readIORef ctx._minted
      writeIORef ctx._minted spent
      mapM_ (ctx._saveEval . fact) known
      ctx._saveEval (EvSymbolize ctx._nesting meta._spelling term stood)
      bind meta (MvExpression stood) bound
      where
        fact :: (Int, Bytes) -> Evaluation
        fact (fresh, bytes) = EvKnown ctx._nesting fresh bytes
    paired :: ReduceContext -> Lambda -> Maybe (Either Int Bytes) -> (Subst, State) -> (Meta, (Meta, Meta)) -> IO (Subst, State)
    paired ctx entry condition (bound, state') (meta, (left, right)) = do
      one <- branch left
      two <- branch right
      case (raising entry one, raising entry two) of
        (True, False) -> terminating "left" left one two
        (False, True) -> terminating "right" right two one
        _ -> both one two
      where
        both :: Expression -> Expression -> IO (Subst, State)
        both one two = do
          outcome <- joined entry._lenient one two <$> readIORef ctx._minted
          case outcome of
            Just made -> written state' made
            Nothing
              | entry._lenient && (hanging one || hanging two) -> do
                  (one', reducing) <- reduced left one state'
                  (two', state'') <- reduced right two reducing
                  outcome' <- joined entry._lenient one' two' <$> readIORef ctx._minted
                  maybe (throwIO (Stuck func)) (written state'') outcome'
              | otherwise -> throwIO (Stuck func)
        written :: State -> (Expression, [(Int, (Int, Int))], Int) -> IO (Subst, State)
        written state'' (term, made, spent) = do
          writeIORef ctx._minted spent
          mapM_ (ctx._saveEval . fact) made
          ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)
          bound' <- bind meta (MvExpression term) bound
          pure (bound', state'')
        reduced :: Meta -> Expression -> State -> IO (Expression, State)
        reduced side term state''
          | hanging term = do
              (normal, morphed) <- morphing univ ctx (ExDispatch term AtPhi) state''
              ctx._saveEval (EvTerm ctx._nesting side._spelling Morphing (ExDispatch (ExMeta side._name) AtPhi) normal)
              (answer, state''') <- fire ctx entry side morphed normal
              ctx._saveEval (EvTerm ctx._nesting side._spelling Evaluation (ExMeta side._name) answer)
              pure (answer, state''')
          | otherwise = pure (term, state'')
        hanging :: Expression -> Bool
        hanging (ExFormation bds) = not (any isLambda bds) && or [not (xiFree body) | BiTau AtPhi body <- bds]
        hanging _ = False
        terminating :: T.Text -> Meta -> Expression -> Expression -> IO (Subst, State)
        terminating side raised fault term = do
          ctx._saveEval (EvTerminate ctx._nesting condition side raised._spelling (message fault))
          ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)
          bound' <- bind meta (MvExpression term) bound
          pure (bound', state')
        branch :: Meta -> IO Expression
        branch named = buildExpressionThrows (ExMeta named._name) bound
        fact :: (Int, (Int, Int)) -> Evaluation
        fact (fresh, pair) = EvJoined ctx._nesting fresh pair
    raising :: Lambda -> Expression -> Bool
    raising _ ExTermination = True
    raising entry term = thrown entry._terminators term
    answered :: ReduceContext -> Lambda -> [Either Int Bytes] -> Subst -> State -> IO (Answer, State)
    answered ctx entry operands bound state' = do
      (fresh, spent) <- minted entry._answer <$> readIORef ctx._minted
      writeIORef ctx._minted spent
      mapM_ (\idx -> ctx._saveEval (EvMinted ctx._nesting idx operands)) [idx | (_, FnSymbol idx) <- fresh]
      symbolic <- foldM mint bound fresh
      built <- buildExpressionThrows entry._answer symbolic
      ctx._saveEval (EvBuilt ctx._nesting built)
      (normal, state'') <- settled built univ state' =<< opening Morphing ctx{_saveEval = ctx._saveEval . resited ctx._site built}
      ctx._saveEval (EvAnswer ctx._nesting normal)
      pure ((built, normal), state'')
    mint :: Subst -> (Slot, Function) -> IO Subst
    mint bound (slot, fresh) = case combine (substSlot slot (MvFunction fresh)) bound of
      Just bound' -> pure bound'
      Nothing -> throwIO (userError (printf "A fresh symbol of λ function '%s' clashes with an existing binding" (T.unpack func)))
    operand :: Expression -> IO Expression
    operand term = caller._engine._contextualize term self
    bind :: Meta -> MetaValue -> Subst -> IO Subst
    bind meta value bound = case combine (substSingle meta._name value) bound of
      Just bound' -> pure bound'
      Nothing ->
        throwIO
          (userError (printf "The meta '%s' of λ function '%s' clashes with an existing binding" (T.unpack meta._spelling) (T.unpack func)))

rewritten :: [Y.Rule] -> RuleContext -> Expression -> IO Expression
rewritten rules ctx = goExpr
  where
    goExpr :: Expression -> IO Expression
    goExpr expr = goRules rules
      where
        goRules :: [Y.Rule] -> IO Expression
        goRules [] = inside expr
        goRules (rule : rest) = do
          substs <- matchExpressionWithRule' [substEmpty] expr rule ctx
          case substs of
            subst : _ -> buildExpressionThrows rule.result subst
            [] -> goRules rest
    inside :: Expression -> IO Expression
    inside (ExFormation bds) = ExFormation <$> mapM goBinding bds
    inside (ExApplication expr arg) = ExApplication <$> goExpr expr <*> goArgument arg
    inside (ExDispatch expr attr) = (`ExDispatch` attr) <$> goExpr expr
    inside (ExPhiMeet prefix idx expr) = ExPhiMeet prefix idx <$> goExpr expr
    inside (ExPhiAgain prefix idx expr) = ExPhiAgain prefix idx <$> goExpr expr
    inside expr = pure expr
    goBinding :: Binding -> IO Binding
    goBinding (BiTau attr expr) = BiTau attr <$> goExpr expr
    goBinding bd = pure bd
    goArgument :: Argument -> IO Argument
    goArgument (ArTau attr expr) = ArTau attr <$> goExpr expr
    goArgument (ArAlpha alpha expr) = ArAlpha alpha <$> goExpr expr