{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# 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 (..), dontSaveEval, dontSaveStep, resited)
import Engine (Engine (..))
import Forks (Refusal (Unnamed, Unripe), forked, joined)
import Lambdas (Ending (..), Lambda (..), Line (..), Meta (..), cast, emptyLambdas, matched, minted, rewritten, stayed, symbolized, thrown)
import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot)
import Morph (Answer (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), argued, awaited, boxed, called, charged, coined, counted, deeper, ended, expired, fired, isLambda, lambda, morphing, normalized, opening, origin, recalled, remember, remembered, retained, settled, starved, unparked)
import Printer (printFunction)
import Rule (RuleContext (RuleContext))
import Text.Printf (printf)

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

symbol :: T.Text -> Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)
symbol :: Text
-> Expression
-> Expression
-> Expression
-> State
-> ReduceContext
-> IO (Expression, State)
symbol Text
func Expression
form Expression
self Expression
univ State
state ReduceContext
caller = case Lambdas -> Text -> Maybe Lambda
matched ReduceContext
caller._symbolic Text
func of
  Maybe Lambda
Nothing -> do
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Text
func Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ReduceContext
caller._parked) (ReduceContext
caller._saveEval (Int -> Text -> Judgment -> Expression -> Evaluation
EvStuck ReduceContext
caller._nesting Text
func ReduceContext
caller._judgment Expression
form))
    ReduceException -> IO (Expression, State)
forall e a. Exception e => e -> IO a
throwIO (Text -> ReduceException
Stuck Text
func)
  Just Lambda
entry -> do
    Maybe Kept
known <- Maybe Memo -> Expression -> Int -> IO (Maybe Kept)
recalled ReduceContext
caller._memo Expression
form ReduceContext
caller._steps._spent
    IO (Expression, State)
-> (Kept -> IO (Expression, State))
-> Maybe Kept
-> IO (Expression, State)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Lambda -> IO (Expression, State)
made Lambda
entry) Kept -> IO (Expression, State)
told Maybe Kept
known
  where
    made :: Lambda -> IO (Expression, State)
    made :: Lambda -> IO (Expression, State)
made Lambda
entry = do
      ReduceContext -> IO ()
charged ReduceContext
caller
      Int
stamp <- Maybe Memo -> IO Int
counted ReduceContext
caller._memo
      Int
exhausted <- Maybe Memo -> IO Int
starved ReduceContext
caller._memo
      ReduceContext
caller._saveEval (Int -> Text -> Judgment -> Expression -> Evaluation
EvFiring ReduceContext
caller._nesting Text
func ReduceContext
caller._judgment ReduceContext
caller._site)
      let ctx :: ReduceContext
ctx = ReduceContext
caller{_nesting = caller._nesting + 1}
      Either ReduceException (Answer, State)
outcome <- IO (Answer, State) -> IO (Either ReduceException (Answer, State))
forall e a. Exception e => IO a -> IO (Either e a)
try (IO (Answer, State) -> IO (Either ReduceException (Answer, State)))
-> IO (Answer, State)
-> IO (Either ReduceException (Answer, State))
forall a b. (a -> b) -> a -> b
$ do
        (Subst
bound, State
dataized, [Either Int Bytes]
conditions) <- ((Subst, State, [Either Int Bytes])
 -> (Meta, Expression) -> IO (Subst, State, [Either Int Bytes]))
-> (Subst, State, [Either Int Bytes])
-> [(Meta, Expression)]
-> IO (Subst, State, [Either Int Bytes])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (ReduceContext
-> (Subst, State, [Either Int Bytes])
-> (Meta, Expression)
-> IO (Subst, State, [Either Int Bytes])
down ReduceContext
ctx) (Subst
substEmpty, State
state, []) Lambda
entry._dataized
        (Subst
bound', State
morphed, [Expression]
normals) <- ((Subst, State, [Expression])
 -> (Meta, Expression) -> IO (Subst, State, [Expression]))
-> (Subst, State, [Expression])
-> [(Meta, Expression)]
-> IO (Subst, State, [Expression])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (ReduceContext
-> Text
-> (State -> Expression -> IO (Expression, State))
-> (Subst, State, [Expression])
-> (Meta, Expression)
-> IO (Subst, State, [Expression])
through ReduceContext
ctx Text
"morph" ((Expression -> IO Expression)
-> State -> Expression -> IO (Expression, State)
still Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure)) (Subst
bound, State
dataized, []) Lambda
entry._morphed
        (Subst
bound'', State
undressed, [Expression]
normals') <- ((Subst, State, [Expression])
 -> (Meta, Expression) -> IO (Subst, State, [Expression]))
-> (Subst, State, [Expression])
-> [(Meta, Expression)]
-> IO (Subst, State, [Expression])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (ReduceContext
-> Text
-> (State -> Expression -> IO (Expression, State))
-> (Subst, State, [Expression])
-> (Meta, Expression)
-> IO (Subst, State, [Expression])
through ReduceContext
ctx Text
"undress" (ReduceContext -> State -> Expression -> IO (Expression, State)
peeled ReduceContext
ctx)) (Subst
bound', State
morphed, [Expression]
normals) Lambda
entry._undressed
        Firing
firing <- Text -> [Either Int Bytes] -> [Expression] -> Firing
Firing Text
func ([Either Int Bytes] -> [Either Int Bytes]
forall a. [a] -> [a]
reverse [Either Int Bytes]
conditions) ([Expression] -> Firing)
-> ([Expression] -> [Expression]) -> [Expression] -> Firing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Expression] -> [Expression]
forall a. [a] -> [a]
reverse [Expression]
normals' [Expression] -> [Expression] -> [Expression]
forall a. [a] -> [a] -> [a]
++) ([Expression] -> Firing) -> IO [Expression] -> IO Firing
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ending -> IO [Expression]
sides Lambda
entry._ending
        Maybe Answer
known <- Maybe Memo -> Firing -> IO (Maybe Answer)
remembered ReduceContext
caller._memo Firing
firing
        IO (Answer, State)
-> (Answer -> IO (Answer, State))
-> Maybe Answer
-> IO (Answer, State)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ReduceContext
-> Lambda -> Firing -> Subst -> State -> IO (Answer, State)
worked ReduceContext
ctx Lambda
entry Firing
firing Subst
bound'' State
undressed) (\Answer
answer -> (Answer
answer, State
undressed) (Answer, State) -> IO () -> IO (Answer, State)
forall a b. a -> IO b -> IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Int -> Answer -> IO ()
shown ReduceContext
ctx._nesting Answer
answer) Maybe Answer
known
      case Either ReduceException (Answer, State)
outcome of
        Right (Answer
answer, State
state') -> do
          Maybe Memo -> Expression -> Int -> Kept -> IO ()
retained ReduceContext
caller._memo Expression
form Int
stamp (Answer -> Kept
Answered Answer
answer)
          (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Answer -> Expression
ended Answer
answer, State
state')
        Left ReduceException
failure -> do
          Int
exhausted' <- Maybe Memo -> IO Int
starved ReduceContext
caller._memo
          (Kept -> IO ()) -> Maybe Kept -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Maybe Memo -> Expression -> Int -> Kept -> IO ()
retained ReduceContext
caller._memo Expression
form Int
stamp) (Bool -> ReduceException -> Maybe Kept
kept (Int
exhausted' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
exhausted) (ReduceException -> ReduceException
escaped ReduceException
failure))
          (Text -> IO ()) -> Maybe Text -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ReduceContext
caller._saveEval (Evaluation -> IO ()) -> (Text -> Evaluation) -> Text -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Text -> Evaluation
EvStuckOn (ReduceContext
caller._nesting Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) (ReduceException -> Maybe Text
stranded ReduceException
failure)
          ReduceException -> IO (Expression, State)
forall e a. Exception e => e -> IO a
throwIO (ReduceException -> ReduceException
escaped ReduceException
failure)
    worked :: ReduceContext -> Lambda -> Firing -> Subst -> State -> IO (Answer, State)
    worked :: ReduceContext
-> Lambda -> Firing -> Subst -> State -> IO (Answer, State)
worked ReduceContext
ctx Lambda
entry firing :: Firing
firing@(Firing Text
_ [Either Int Bytes]
operands [Expression]
_) Subst
bound State
state' = do
      (Subst
lined, State
state'') <- ((Subst, State) -> Line -> IO (Subst, State))
-> (Subst, State) -> [Line] -> IO (Subst, State)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (ReduceContext
-> Lambda -> (Subst, State) -> Line -> IO (Subst, State)
passing ReduceContext
ctx Lambda
entry) (Subst
bound, State
state') Lambda
entry._lines
      (Answer
answer, State
state''') <- ReduceContext
-> Lambda
-> [Either Int Bytes]
-> Subst
-> State
-> IO (Answer, State)
concluded ReduceContext
ctx Lambda
entry [Either Int Bytes]
operands Subst
lined State
state''
      Maybe Memo -> Firing -> Answer -> IO ()
remember ReduceContext
caller._memo Firing
firing Answer
answer
      (Answer, State) -> IO (Answer, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Answer
answer, State
state''')
    sides :: Ending -> IO [Expression]
    sides :: Ending -> IO [Expression]
sides (Answering Expression
_) = [Expression] -> IO [Expression]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    sides (Joining Either Meta Expression
_ Expression
left Expression
right Maybe Function
_) = (Expression -> IO Expression) -> [Expression] -> IO [Expression]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Expression -> IO Expression
keyed [Expression
left, Expression
right]
    keyed :: Expression -> IO Expression
    keyed :: Expression -> IO Expression
keyed side :: Expression
side@(ExMeta Text
_) = Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
side
    keyed Expression
side = Expression -> IO Expression
operand Expression
side
    passing :: ReduceContext -> Lambda -> (Subst, State) -> Line -> IO (Subst, State)
    passing :: ReduceContext
-> Lambda -> (Subst, State) -> Line -> IO (Subst, State)
passing ReduceContext
ctx Lambda
entry held :: (Subst, State)
held@(Subst
bound, State
state') Line
item = case Line -> Maybe (Meta, Meta)
sourced Line
item of
      Just (Meta
meta, Meta
source) -> do
        Expression
term <- Expression -> Subst -> IO Expression
buildExpressionThrows (Text -> Expression
ExMeta Meta
source._name) Subst
bound
        if [Text] -> Expression -> Bool
thrown Lambda
entry._terminators Expression
term
          then do
            ReduceContext
ctx._saveEval (Int -> Expression -> Expression -> Evaluation
EvBound ReduceContext
ctx._nesting (Text -> Expression
ExMeta Meta
meta._name) Expression
term)
            (,State
state') (Subst -> (Subst, State)) -> IO Subst -> IO (Subst, State)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Meta -> MetaValue -> Subst -> IO Subst
bind Meta
meta (Expression -> MetaValue
MvExpression Expression
term) Subst
bound
          else ReduceContext
-> Ending -> (Subst, State) -> Line -> IO (Subst, State)
line ReduceContext
ctx Lambda
entry._ending (Subst, State)
held Line
item
      Maybe (Meta, Meta)
Nothing -> ReduceContext
-> Ending -> (Subst, State) -> Line -> IO (Subst, State)
line ReduceContext
ctx Lambda
entry._ending (Subst, State)
held Line
item
    sourced :: Line -> Maybe (Meta, Meta)
    sourced :: Line -> Maybe (Meta, Meta)
sourced (Morphed Meta
meta Meta
source) = (Meta, Meta) -> Maybe (Meta, Meta)
forall a. a -> Maybe a
Just (Meta
meta, Meta
source)
    sourced (Undressed Meta
meta Meta
source) = (Meta, Meta) -> Maybe (Meta, Meta)
forall a. a -> Maybe a
Just (Meta
meta, Meta
source)
    sourced (Evaluated Meta
meta Meta
source) = (Meta, Meta) -> Maybe (Meta, Meta)
forall a. a -> Maybe a
Just (Meta
meta, Meta
source)
    sourced (Deferred Meta
meta Meta
source) = (Meta, Meta) -> Maybe (Meta, Meta)
forall a. a -> Maybe a
Just (Meta
meta, Meta
source)
    sourced (Stayed Meta
meta Meta
source) = (Meta, Meta) -> Maybe (Meta, Meta)
forall a. a -> Maybe a
Just (Meta
meta, Meta
source)
    sourced (Rewritten Meta
meta Meta
source [Rule]
_) = (Meta, Meta) -> Maybe (Meta, Meta)
forall a. a -> Maybe a
Just (Meta
meta, Meta
source)
    sourced (Symbolized Meta
meta Meta
source) = (Meta, Meta) -> Maybe (Meta, Meta)
forall a. a -> Maybe a
Just (Meta
meta, Meta
source)
    sourced Line
_ = Maybe (Meta, Meta)
forall a. Maybe a
Nothing
    line :: ReduceContext -> Ending -> (Subst, State) -> Line -> IO (Subst, State)
    line :: ReduceContext
-> Ending -> (Subst, State) -> Line -> IO (Subst, State)
line ReduceContext
ctx Ending
_ (Subst, State)
held (Dataized Meta
meta Meta
source) = ReduceContext
-> (Subst, State) -> Meta -> Meta -> IO (Subst, State)
lowered ReduceContext
ctx (Subst, State)
held Meta
meta Meta
source
    line ReduceContext
ctx Ending
_ (Subst, State)
held (Morphed Meta
meta Meta
source) = ReduceContext
-> (Subst, State) -> Meta -> Meta -> IO (Subst, State)
reduced ReduceContext
ctx (Subst, State)
held Meta
meta Meta
source
    line ReduceContext
ctx Ending
ending (Subst, State)
held (Evaluated Meta
meta Meta
source) = ReduceContext
-> Ending -> (Subst, State) -> Meta -> Meta -> IO (Subst, State)
evaluated ReduceContext
ctx Ending
ending (Subst, State)
held Meta
meta Meta
source
    line ReduceContext
ctx Ending
_ (Subst
bound, State
state') (Deferred Meta
meta Meta
source) = (,State
state') (Subst -> (Subst, State)) -> IO Subst -> IO (Subst, State)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceContext -> State -> Meta -> Meta -> Subst -> IO Subst
deferred ReduceContext
ctx State
state' Meta
meta Meta
source Subst
bound
    line ReduceContext
ctx Ending
_ (Subst, State)
held (Stayed Meta
meta Meta
source) = ReduceContext
-> Text
-> (State -> Expression -> IO (Expression, State))
-> Meta
-> Meta
-> (Subst, State)
-> IO (Subst, State)
reshaped ReduceContext
ctx Text
"stay" ((Expression -> IO Expression)
-> State -> Expression -> IO (Expression, State)
still (Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> IO Expression)
-> (Expression -> Expression) -> Expression -> IO Expression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression -> Expression
stayed)) Meta
meta Meta
source (Subst, State)
held
    line ReduceContext
ctx Ending
_ (Subst, State)
held (Rewritten Meta
meta Meta
source [Rule]
rules) = ReduceContext
-> Text
-> (State -> Expression -> IO (Expression, State))
-> Meta
-> Meta
-> (Subst, State)
-> IO (Subst, State)
reshaped ReduceContext
ctx Text
"rewrite" ((Expression -> IO Expression)
-> State -> Expression -> IO (Expression, State)
still (ReduceContext -> IO Expression -> IO Expression
forall a. ReduceContext -> IO a -> IO a
awaited ReduceContext
ctx (IO Expression -> IO Expression)
-> (Expression -> IO Expression) -> Expression -> IO Expression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RuleContext -> [Rule] -> Expression -> IO Expression
rewritten (BuildTermFunc
-> Maybe Expression -> (Expression -> Bool) -> RuleContext
RuleContext ReduceContext
ctx._buildTerm ReduceContext
ctx._universe ReduceContext
ctx._engine._normal) [Rule]
rules)) Meta
meta Meta
source (Subst, State)
held
    line ReduceContext
ctx Ending
_ (Subst, State)
held (Symbolized Meta
meta Meta
source) = ReduceContext
-> Text
-> (State -> Expression -> IO (Expression, State))
-> Meta
-> Meta
-> (Subst, State)
-> IO (Subst, State)
reshaped ReduceContext
ctx Text
"symbolize" ((Expression -> IO Expression)
-> State -> Expression -> IO (Expression, State)
still (ReduceContext -> Expression -> IO Expression
masked ReduceContext
ctx)) Meta
meta Meta
source (Subst, State)
held
    line ReduceContext
ctx Ending
_ (Subst, State)
held (Undressed Meta
meta Meta
source) = ReduceContext
-> Text
-> (State -> Expression -> IO (Expression, State))
-> Meta
-> Meta
-> (Subst, State)
-> IO (Subst, State)
reshaped ReduceContext
ctx Text
"undress" (ReduceContext -> State -> Expression -> IO (Expression, State)
peeled ReduceContext
ctx) Meta
meta Meta
source (Subst, State)
held
    line ReduceContext
ctx Ending
_ (Subst, State)
held (Cast Meta
one Meta
first Meta
two Meta
second) = ReduceContext
-> (Subst, State)
-> (Meta, Meta)
-> (Meta, Meta)
-> IO (Subst, State)
casting ReduceContext
ctx (Subst, State)
held (Meta
one, Meta
first) (Meta
two, Meta
second)
    shown :: Int -> Answer -> IO ()
    shown :: Int -> Answer -> IO ()
shown Int
depth (Answer Expression
built Expression
normal) = do
      ReduceContext
caller._saveEval (Int -> Expression -> Evaluation
EvBuilt Int
depth Expression
built)
      ReduceContext
caller._saveEval (Int -> Expression -> Evaluation
EvAnswer Int
depth Expression
normal)
    shown Int
depth (Joined Expression
normal) = ReduceContext
caller._saveEval (Int -> Expression -> Evaluation
EvTaken Int
depth Expression
normal)
    kept :: Bool -> ReduceException -> Maybe Kept
    kept :: Bool -> ReduceException -> Maybe Kept
kept Bool
_ (Looping Expression
term) = Kept -> Maybe Kept
forall a. a -> Maybe a
Just (Expression -> Kept
Looped Expression
term)
    kept Bool
_ (LoopingAt Expression
term NonEmpty Rewritten
_ State
_) = Kept -> Maybe Kept
forall a. a -> Maybe a
Just (Expression -> Kept
Looped Expression
term)
    kept Bool
starving (Stuck Text
name) = Kept -> Maybe Kept
forall a. a -> Maybe a
Just (Text -> Int -> Kept
Stalled Text
name (Bool -> Int
least Bool
starving))
    kept Bool
starving (StuckAt Text
name NonEmpty Rewritten
_ State
_) = Kept -> Maybe Kept
forall a. a -> Maybe a
Just (Text -> Int -> Kept
Stalled Text
name (Bool -> Int
least Bool
starving))
    kept Bool
_ ReduceException
_ = Maybe Kept
forall a. Maybe a
Nothing
    least :: Bool -> Int
    least :: Bool -> Int
least Bool
True = ReduceContext
caller._steps._spent
    least Bool
False = Int
0
    stranded :: ReduceException -> Maybe T.Text
    stranded :: ReduceException -> Maybe Text
stranded (Stuck Text
name) = Text -> Maybe Text
forall a. a -> Maybe a
Just Text
name
    stranded (StuckAt Text
name NonEmpty Rewritten
_ State
_) = Text -> Maybe Text
forall a. a -> Maybe a
Just Text
name
    stranded ReduceException
_ = Maybe Text
forall a. Maybe a
Nothing
    escaped :: ReduceException -> ReduceException
    escaped :: ReduceException -> ReduceException
escaped (Diverged Text
name) = Text -> ReduceException
Stuck Text
name
    escaped ReduceException
failure = ReduceException
failure
    told :: Kept -> IO (Expression, State)
    told :: Kept -> IO (Expression, State)
told (Answered Answer
answer) = do
      ReduceContext
caller._saveEval (Int -> Text -> Judgment -> Expression -> Evaluation
EvFiring ReduceContext
caller._nesting Text
func ReduceContext
caller._judgment ReduceContext
caller._site)
      Int -> Answer -> IO ()
shown (ReduceContext
caller._nesting Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Answer
answer
      (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Answer -> Expression
ended Answer
answer, State
state)
    told (Looped Expression
term) = do
      ReduceContext
caller._saveEval (Int -> Text -> Judgment -> Expression -> Evaluation
EvFiring ReduceContext
caller._nesting Text
func ReduceContext
caller._judgment ReduceContext
caller._site)
      (Acyclic -> IO ()) -> Maybe Acyclic -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Acyclic
mode -> ReduceContext
caller._saveEval (Int
-> Judgment
-> Acyclic
-> Expression
-> Expression
-> Maybe (Int, Expression)
-> Evaluation
EvLooped (ReduceContext
caller._nesting Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ReduceContext
caller._judgment Acyclic
mode Expression
term ReduceContext
caller._site Maybe (Int, Expression)
forall a. Maybe a
Nothing)) ReduceContext
caller._acyclic
      ReduceException -> IO (Expression, State)
forall e a. Exception e => e -> IO a
throwIO (Expression -> ReduceException
Looping Expression
term)
    told (Stalled Text
name Int
_) = do
      ReduceContext
caller._saveEval (Int -> Text -> Judgment -> Expression -> Evaluation
EvFiring ReduceContext
caller._nesting Text
func ReduceContext
caller._judgment ReduceContext
caller._site)
      ReduceContext
caller._saveEval (Int -> Text -> Evaluation
EvStall (ReduceContext
caller._nesting Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Text
name)
      ReduceException -> IO (Expression, State)
forall e a. Exception e => e -> IO a
throwIO (Text -> ReduceException
Stuck Text
name)
    down :: ReduceContext -> (Subst, State, [Either Int Bytes]) -> (Meta, Expression) -> IO (Subst, State, [Either Int Bytes])
    down :: ReduceContext
-> (Subst, State, [Either Int Bytes])
-> (Meta, Expression)
-> IO (Subst, State, [Either Int Bytes])
down ReduceContext
ctx (Subst
bound, State
state', [Either Int Bytes]
conditions) (Meta
meta, Expression
term) = do
      (Either Int Bytes
datum, Subst
bound', State
state'') <- ReduceContext
-> Subst
-> State
-> Meta
-> Expression
-> Expression
-> IO (Either Int Bytes, Subst, State)
brought ReduceContext
ctx Subst
bound State
state' Meta
meta Expression
term (Expression -> IO (Either Int Bytes, Subst, State))
-> IO Expression -> IO (Either Int Bytes, Subst, State)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expression -> IO Expression
operand Expression
term
      (Subst, State, [Either Int Bytes])
-> IO (Subst, State, [Either Int Bytes])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
bound', State
state'', Either Int Bytes
datum Either Int Bytes -> [Either Int Bytes] -> [Either Int Bytes]
forall a. a -> [a] -> [a]
: [Either Int Bytes]
conditions)
    lowered :: ReduceContext -> (Subst, State) -> Meta -> Meta -> IO (Subst, State)
    lowered :: ReduceContext
-> (Subst, State) -> Meta -> Meta -> IO (Subst, State)
lowered ReduceContext
ctx (Subst
bound, State
state') Meta
meta Meta
source = do
      (Either Int Bytes
_, Subst
bound', State
state'') <- ReduceContext
-> Subst
-> State
-> Meta
-> Expression
-> Expression
-> IO (Either Int Bytes, Subst, State)
brought ReduceContext
ctx Subst
bound State
state' Meta
meta (Text -> Expression
ExMeta Meta
source._name) (Expression -> IO (Either Int Bytes, Subst, State))
-> IO Expression -> IO (Either Int Bytes, Subst, State)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expression -> Subst -> IO Expression
buildExpressionThrows (Text -> Expression
ExMeta Meta
source._name) Subst
bound
      (Subst, State) -> IO (Subst, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
bound', State
state'')
    brought :: ReduceContext -> Subst -> State -> Meta -> Expression -> Expression -> IO (Either Int Bytes, Subst, State)
    brought :: ReduceContext
-> Subst
-> State
-> Meta
-> Expression
-> Expression
-> IO (Either Int Bytes, Subst, State)
brought ReduceContext
ctx Subst
bound State
state' Meta
meta Expression
origin Expression
term = do
      (Maybe Bytes
value, State
came) <- IO (Maybe Bytes, State) -> IO (Maybe Bytes, State)
forall a. IO a -> IO a
unparked (ReduceContext
ctx._reduce Expression
univ ReduceContext
ctx{_site = origin} Expression
term State
state'{_manufactured = Nothing, _stuck = Nothing, _copies = []})
      let state'' :: State
state'' = State
came{_copies = state'._copies}
      case Maybe Bytes
value of
        Maybe Bytes
Nothing -> ReduceException -> IO (Either Int Bytes, Subst, State)
forall e a. Exception e => e -> IO a
throwIO (Text -> ReduceException
Stuck (Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
func State
state''._stuck))
        Just Bytes
bytes -> do
          let datum :: Either Int Bytes
datum = Either Int Bytes
-> (Int -> Either Int Bytes) -> Maybe Int -> Either Int Bytes
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bytes -> Either Int Bytes
forall a b. b -> Either a b
Right Bytes
bytes) Int -> Either Int Bytes
forall a b. a -> Either a b
Left State
state''._manufactured
          ReduceContext
ctx._saveEval (Int -> Text -> Expression -> Either Int Bytes -> Evaluation
EvData ReduceContext
ctx._nesting Meta
meta._spelling Expression
origin Either Int Bytes
datum)
          Subst
bound' <- Meta -> MetaValue -> Subst -> IO Subst
bind Meta
meta (Bytes -> MetaValue
MvBytes Bytes
bytes) Subst
bound
          (Either Int Bytes, Subst, State)
-> IO (Either Int Bytes, Subst, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Int Bytes
datum, Subst
bound', State
state'')
    through :: ReduceContext -> T.Text -> (State -> Expression -> IO (Expression, State)) -> (Subst, State, [Expression]) -> (Meta, Expression) -> IO (Subst, State, [Expression])
    through :: ReduceContext
-> Text
-> (State -> Expression -> IO (Expression, State))
-> (Subst, State, [Expression])
-> (Meta, Expression)
-> IO (Subst, State, [Expression])
through ReduceContext
ctx Text
block State -> Expression -> IO (Expression, State)
change (Subst
bound, State
state', [Expression]
normals) (Meta
meta, Expression
term) = do
      Expression
placed <- Expression -> IO Expression
operand Expression
term
      (Expression
normal, State
state'') <- Expression
-> ReduceContext -> Expression -> State -> IO (Expression, State)
morphing Expression
univ ReduceContext
ctx{_site = term} Expression
placed State
state'
      (Expression
shaped, State
state''') <- State -> Expression -> IO (Expression, State)
change State
state'' Expression
normal
      ReduceContext
ctx._saveEval
        ( if Expression
shaped Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
normal
            then Int -> Text -> Judgment -> Expression -> Expression -> Evaluation
EvTerm ReduceContext
ctx._nesting Meta
meta._spelling Judgment
Morphing Expression
term Expression
normal
            else Int -> Text -> Text -> Expression -> Expression -> Evaluation
EvReshaped ReduceContext
ctx._nesting Meta
meta._spelling Text
block Expression
term Expression
shaped
        )
      Subst
bound' <- Meta -> MetaValue -> Subst -> IO Subst
bind Meta
meta (Expression -> MetaValue
MvExpression Expression
shaped) Subst
bound
      (Subst, State, [Expression]) -> IO (Subst, State, [Expression])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
bound', State
state''', Expression
shaped Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression]
normals)
    reduced :: ReduceContext -> (Subst, State) -> Meta -> Meta -> IO (Subst, State)
    reduced :: ReduceContext
-> (Subst, State) -> Meta -> Meta -> IO (Subst, State)
reduced ReduceContext
ctx (Subst
bound, State
state') Meta
meta Meta
source = do
      Expression
term <- Expression -> Subst -> IO Expression
buildExpressionThrows (Text -> Expression
ExMeta Meta
source._name) Subst
bound
      (Expression
normal, State
state'') <- Expression
-> ReduceContext -> Expression -> State -> IO (Expression, State)
morphing Expression
univ ReduceContext
ctx{_site = ExMeta source._name} Expression
term State
state'
      ReduceContext
ctx._saveEval (Int -> Text -> Judgment -> Expression -> Expression -> Evaluation
EvTerm ReduceContext
ctx._nesting Meta
meta._spelling Judgment
Morphing (Text -> Expression
ExMeta Meta
source._name) Expression
normal)
      Subst
bound' <- Meta -> MetaValue -> Subst -> IO Subst
bind Meta
meta (Expression -> MetaValue
MvExpression Expression
normal) Subst
bound
      (Subst, State) -> IO (Subst, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
bound', State
state'')
    reshaped :: ReduceContext -> T.Text -> (State -> Expression -> IO (Expression, State)) -> Meta -> Meta -> (Subst, State) -> IO (Subst, State)
    reshaped :: ReduceContext
-> Text
-> (State -> Expression -> IO (Expression, State))
-> Meta
-> Meta
-> (Subst, State)
-> IO (Subst, State)
reshaped ReduceContext
ctx Text
block State -> Expression -> IO (Expression, State)
change Meta
meta Meta
source (Subst
bound, State
state') = do
      Expression
kept <- Expression -> Subst -> IO Expression
buildExpressionThrows (Text -> Expression
ExMeta Meta
source._name) Subst
bound
      (Expression
term, State
state'') <- State -> Expression -> IO (Expression, State)
change State
state' Expression
kept
      ReduceContext
ctx._saveEval
        ( if Expression
term Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
kept
            then Int -> Expression -> Expression -> Evaluation
EvBound ReduceContext
ctx._nesting (Text -> Expression
ExMeta Meta
meta._name) Expression
term
            else Int -> Text -> Text -> Expression -> Expression -> Evaluation
EvReshaped ReduceContext
ctx._nesting Meta
meta._spelling Text
block (Text -> Expression
ExMeta Meta
source._name) Expression
term
        )
      (,State
state'') (Subst -> (Subst, State)) -> IO Subst -> IO (Subst, State)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Meta -> MetaValue -> Subst -> IO Subst
bind Meta
meta (Expression -> MetaValue
MvExpression Expression
term) Subst
bound
    casting :: ReduceContext -> (Subst, State) -> (Meta, Meta) -> (Meta, Meta) -> IO (Subst, State)
    casting :: ReduceContext
-> (Subst, State)
-> (Meta, Meta)
-> (Meta, Meta)
-> IO (Subst, State)
casting ReduceContext
ctx (Subst
bound, State
state') (Meta
one, Meta
first) (Meta
two, Meta
second) = do
      Expression
left <- Expression -> Subst -> IO Expression
buildExpressionThrows (Text -> Expression
ExMeta Meta
first._name) Subst
bound
      Expression
right <- Expression -> Subst -> IO Expression
buildExpressionThrows (Text -> Expression
ExMeta Meta
second._name) Subst
bound
      (,State
state') (Subst -> (Subst, State)) -> IO Subst -> IO (Subst, State)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case (Expression -> Expression -> Maybe Expression
cast Expression
left Expression
right, Expression -> Expression -> Maybe Expression
cast Expression
right Expression
left) of
        (Just Expression
made, Maybe Expression
_) -> Meta -> Meta -> Meta -> Expression -> Subst -> IO Subst
molded Meta
one Meta
first Meta
second Expression
made Subst
bound IO Subst -> (Subst -> IO Subst) -> IO Subst
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Meta -> Expression -> Subst -> IO Subst
kept Meta
two Expression
right
        (Maybe Expression
_, Just Expression
made) -> Meta -> Expression -> Subst -> IO Subst
kept Meta
one Expression
left Subst
bound IO Subst -> (Subst -> IO Subst) -> IO Subst
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Meta -> Meta -> Meta -> Expression -> Subst -> IO Subst
molded Meta
two Meta
second Meta
first Expression
made
        (Maybe Expression, Maybe Expression)
_ -> Meta -> Expression -> Subst -> IO Subst
kept Meta
one Expression
left Subst
bound IO Subst -> (Subst -> IO Subst) -> IO Subst
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Meta -> Expression -> Subst -> IO Subst
kept Meta
two Expression
right
      where
        kept :: Meta -> Expression -> Subst -> IO Subst
        kept :: Meta -> Expression -> Subst -> IO Subst
kept Meta
meta Expression
term Subst
held = do
          ReduceContext
ctx._saveEval (Int -> Expression -> Expression -> Evaluation
EvBound ReduceContext
ctx._nesting (Text -> Expression
ExMeta Meta
meta._name) Expression
term)
          Meta -> MetaValue -> Subst -> IO Subst
bind Meta
meta (Expression -> MetaValue
MvExpression Expression
term) Subst
held
        molded :: Meta -> Meta -> Meta -> Expression -> Subst -> IO Subst
        molded :: Meta -> Meta -> Meta -> Expression -> Subst -> IO Subst
molded Meta
meta Meta
source Meta
shape Expression
made Subst
held = do
          ReduceContext
ctx._saveEval (Int -> Text -> Expression -> Expression -> Expression -> Evaluation
EvCast ReduceContext
ctx._nesting Meta
meta._spelling (Text -> Expression
ExMeta Meta
source._name) (Text -> Expression
ExMeta Meta
shape._name) Expression
made)
          Meta -> MetaValue -> Subst -> IO Subst
bind Meta
meta (Expression -> MetaValue
MvExpression Expression
made) Subst
held
    still :: (Expression -> IO Expression) -> State -> Expression -> IO (Expression, State)
    still :: (Expression -> IO Expression)
-> State -> Expression -> IO (Expression, State)
still Expression -> IO Expression
change State
state' Expression
term = (,State
state') (Expression -> (Expression, State))
-> IO Expression -> IO (Expression, State)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> IO Expression
change Expression
term
    peeled :: ReduceContext -> State -> Expression -> IO (Expression, State)
    peeled :: ReduceContext -> State -> Expression -> IO (Expression, State)
peeled ReduceContext
ctx State
state' term :: Expression
term@(ExFormation [Binding]
bds)
      | [Binding] -> Bool
dressed [Binding]
bds = do
          let taken :: Expression
taken = Expression -> Attribute -> Expression
ExDispatch Expression
term Attribute
AtPhi
          ReduceContext
ctx._saveEval (Int -> Expression -> Evaluation
EvUndressed ReduceContext
ctx._nesting Expression
taken)
          ReduceContext
deep <- ReduceContext -> IO ReduceContext
deeper ReduceContext
ctx{_judgment = Morphing, _site = taken}
          (Expression
normal, State
state'') <- Expression
-> ReduceContext -> Expression -> State -> IO (Expression, State)
morphing Expression
univ ReduceContext
deep Expression
taken State
state'
          ReduceContext -> State -> Expression -> IO (Expression, State)
peeled ReduceContext
deep State
state'' Expression
normal
    peeled ReduceContext
_ State
state' Expression
term = (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
term, State
state')
    dressed :: [Binding] -> Bool
    dressed :: [Binding] -> Bool
dressed [Binding]
bds = case (Binding -> Bool) -> [Binding] -> [Binding]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Maybe Attribute -> Maybe Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute -> Maybe Attribute
forall a. a -> Maybe a
Just Attribute
AtRho) (Maybe Attribute -> Bool)
-> (Binding -> Maybe Attribute) -> Binding -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binding -> Maybe Attribute
attributeFromBinding) [Binding]
bds of
      [BiTau Attribute
AtPhi Expression
_] -> Bool
True
      [Binding]
_ -> Bool
False
    masked :: ReduceContext -> Expression -> IO Expression
    masked :: ReduceContext -> Expression -> IO Expression
masked ReduceContext
ctx Expression
term = do
      (Expression
stood, [(Int, Bytes)]
known, Int
spent) <- Expression -> Int -> (Expression, [(Int, Bytes)], Int)
symbolized Expression
term (Int -> (Expression, [(Int, Bytes)], Int))
-> IO Int -> IO (Expression, [(Int, Bytes)], Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef ReduceContext
ctx._minted
      IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef ReduceContext
ctx._minted Int
spent
      ((Int, Bytes) -> IO ()) -> [(Int, Bytes)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Int
fresh, Bytes
bytes) -> ReduceContext
ctx._saveEval (Int -> Int -> Bytes -> Evaluation
EvSymbolized ReduceContext
ctx._nesting Int
fresh Bytes
bytes)) [(Int, Bytes)]
known
      Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
stood
    evaluated :: ReduceContext -> Ending -> (Subst, State) -> Meta -> Meta -> IO (Subst, State)
    evaluated :: ReduceContext
-> Ending -> (Subst, State) -> Meta -> Meta -> IO (Subst, State)
evaluated ReduceContext
ctx Ending
ending (Subst
bound, State
state') Meta
meta Meta
source = do
      Expression
term <- Expression -> Subst -> IO Expression
buildExpressionThrows (Text -> Expression
ExMeta Meta
source._name) Subst
bound
      (Expression
answer, State
state'') <- ReduceContext
-> Ending
-> Expression
-> State
-> Expression
-> IO (Expression, State)
kindled ReduceContext
ctx Ending
ending (Text -> Expression
ExMeta Meta
source._name) State
state' Expression
term
      ReduceContext
ctx._saveEval
        ( if Expression
answer Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
term
            then Int -> Expression -> Expression -> Evaluation
EvBound ReduceContext
ctx._nesting (Text -> Expression
ExMeta Meta
meta._name) Expression
term
            else Int -> Text -> Judgment -> Expression -> Expression -> Evaluation
EvTerm ReduceContext
ctx._nesting Meta
meta._spelling Judgment
Evaluation (Text -> Expression
ExMeta Meta
source._name) Expression
answer
        )
      Subst
bound' <- Meta -> MetaValue -> Subst -> IO Subst
bind Meta
meta (Expression -> MetaValue
MvExpression Expression
answer) Subst
bound
      (Subst, State) -> IO (Subst, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
bound', State
state'')
    kindled :: ReduceContext -> Ending -> Expression -> State -> Expression -> IO (Expression, State)
    kindled :: ReduceContext
-> Ending
-> Expression
-> State
-> Expression
-> IO (Expression, State)
kindled ReduceContext
_ Ending
_ Expression
_ State
state' term :: Expression
term@(ExFormation [BiLambda (FnSymbol Int
_)]) = (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
term, State
state')
    kindled ReduceContext
ctx Ending
_ Expression
_ State
state' term :: Expression
term@(ExFormation [Binding]
bds)
      | ReduceContext -> [Binding] -> Bool
owned ReduceContext
ctx [Binding]
bds = (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
term, State
state')
    kindled ReduceContext
ctx Ending
_ Expression
site State
state' term :: Expression
term@(ExFormation [Binding]
_) = ReduceContext
-> Expression -> State -> Expression -> IO (Expression, State)
fire ReduceContext
ctx Expression
site State
state' Expression
term
    kindled ReduceContext
_ Joining{} Expression
_ State
state' Expression
term = (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
term, State
state')
    kindled ReduceContext
ctx Ending
_ Expression
site State
state' Expression
term = ReduceContext
-> Expression -> State -> Expression -> IO (Expression, State)
fire ReduceContext
ctx Expression
site State
state' Expression
term
    owned :: ReduceContext -> [Binding] -> Bool
    owned :: ReduceContext -> [Binding] -> Bool
owned ReduceContext
ctx [Binding]
bds = Bool
-> ((Expression, [Binding]) -> Bool)
-> Maybe (Expression, [Binding])
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (\(Expression
_, [Binding]
voids) -> (Attribute -> Bool) -> [Attribute] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Attribute -> [Attribute] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (Attribute
AtRho Attribute -> [Attribute] -> [Attribute]
forall a. a -> [a] -> [a]
: [Attribute
attr | BiVoid Attribute
attr <- [Binding]
voids])) [Attribute
attr | BiTau Attribute
attr Expression
_ <- [Binding]
bds, Bool -> Bool
not (Attribute -> Bool
cactus Attribute
attr)]) (Expression
-> ReduceContext -> [Binding] -> Maybe (Expression, [Binding])
origin Expression
univ ReduceContext
ctx [Binding]
bds)
    cactus :: Attribute -> Bool
    cactus :: Attribute -> Bool
cactus (AtLabel Text
label) = Text
"🌵" Text -> Text -> Bool
`T.isSuffixOf` Text
label
    cactus Attribute
_ = Bool
False
    fire :: ReduceContext -> Expression -> State -> Expression -> IO (Expression, State)
    fire :: ReduceContext
-> Expression -> State -> Expression -> IO (Expression, State)
fire ReduceContext
_ Expression
_ State
state' Expression
ExTermination = (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
ExTermination, State
state')
    fire ReduceContext
ctx Expression
site State
state' term :: Expression
term@(ExFormation [Binding]
_) = Expression
-> ReduceContext
-> Expression
-> State
-> Expression
-> IO (Expression, State)
fired Expression
univ ReduceContext
ctx Expression
site State
state' Expression
term
    fire ReduceContext
_ Expression
_ State
_ Expression
_ = ReduceException -> IO (Expression, State)
forall e a. Exception e => e -> IO a
throwIO (Text -> ReduceException
Stuck Text
func)
    named :: Attribute -> Binding -> Bool
    named :: Attribute -> Binding -> Bool
named Attribute
attr (BiTau Attribute
attr' Expression
_) = Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
attr'
    named Attribute
_ Binding
_ = Bool
False
    deferred :: ReduceContext -> State -> Meta -> Meta -> Subst -> IO Subst
    deferred :: ReduceContext -> State -> Meta -> Meta -> Subst -> IO Subst
deferred ReduceContext
ctx State
state' Meta
meta Meta
source Subst
bound = do
      Expression
term <- Expression -> Subst -> IO Expression
buildExpressionThrows (Text -> Expression
ExMeta Meta
source._name) Subst
bound
      Expression
answer <- ReduceContext
-> State -> Expression -> Expression -> IO (Maybe Expression)
postponing ReduceContext
ctx State
state' (Text -> Expression
ExMeta Meta
source._name) Expression
term IO (Maybe Expression)
-> (Maybe Expression -> IO Expression) -> IO Expression
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO Expression
-> (Expression -> IO Expression)
-> Maybe Expression
-> IO Expression
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Expression -> IO Expression
kept Expression
term) Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      Meta -> MetaValue -> Subst -> IO Subst
bind Meta
meta (Expression -> MetaValue
MvExpression Expression
answer) Subst
bound
      where
        kept :: Expression -> IO Expression
        kept :: Expression -> IO Expression
kept Expression
term = Expression
term Expression -> IO () -> IO Expression
forall a b. a -> IO b -> IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ReduceContext
ctx._saveEval (Int -> Expression -> Expression -> Evaluation
EvBound ReduceContext
ctx._nesting (Text -> Expression
ExMeta Meta
meta._name) Expression
term)
    postponing :: ReduceContext -> State -> Expression -> Expression -> IO (Maybe Expression)
    postponing :: ReduceContext
-> State -> Expression -> Expression -> IO (Maybe Expression)
postponing ReduceContext
ctx State
state' Expression
site (ExFormation [Binding]
bds)
      | [Binding] -> Bool
copied [Binding]
bds = do
          [Binding]
known <- (Binding -> IO Binding) -> [Binding] -> IO [Binding]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Binding -> IO Binding
resolved [Binding]
bds
          if (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Binding -> Bool
bare [Binding]
known then Expression -> Maybe Expression
forall a. a -> Maybe a
Just (Expression -> Maybe Expression)
-> IO Expression -> IO (Maybe Expression)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Binding] -> IO Expression
postponed [Binding]
known else Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
      where
        copied :: [Binding] -> Bool
        copied :: [Binding] -> Bool
copied [Binding]
bds = [Binding] -> Bool
boxed [Binding]
bds Bool -> Bool -> Bool
&& Bool -> Bool
not ((Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Binding -> Bool
void [Binding]
bds) Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool -> Bool
not (Expression -> Bool
formed Expression
body) | BiTau Attribute
AtPhi Expression
body <- [Binding]
bds]
          where
            void :: Binding -> Bool
            void :: Binding -> Bool
void (BiVoid Attribute
_) = Bool
True
            void Binding
_ = Bool
False
            formed :: Expression -> Bool
            formed :: Expression -> Bool
formed (ExFormation [Binding]
_) = Bool
True
            formed Expression
_ = Bool
False
        bare :: Binding -> Bool
        bare :: Binding -> Bool
bare (BiTau Attribute
attr (ExFormation [BiLambda (FnSymbol Int
_)])) = Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute
AtPhi Bool -> Bool -> Bool
&& Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute
AtRho
        bare Binding
_ = Bool
False
        resolved :: Binding -> IO Binding
        resolved :: Binding -> IO Binding
resolved bd :: Binding
bd@(BiTau Attribute
attr Expression
body)
          | Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute
AtPhi Bool -> Bool -> Bool
&& Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute
AtRho Bool -> Bool -> Bool
&& Expression -> Bool
reducible Expression
body = do
              Expression
placed <- ReduceContext
ctx._engine._contextualize Expression
body ([Binding] -> Expression
ExFormation ((Binding -> Bool) -> [Binding] -> [Binding]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Binding -> Bool) -> Binding -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attribute -> Binding -> Bool
named Attribute
attr) [Binding]
bds))
              Either ReduceException (Expression, State)
outcome <- IO (Expression, State)
-> IO (Either ReduceException (Expression, State))
forall e a. Exception e => IO a -> IO (Either e a)
try (Expression
-> Expression -> State -> ReduceContext -> IO (Expression, State)
settled Expression
placed Expression
univ State
state' ReduceContext
reading)
              case Either ReduceException (Expression, State)
outcome of
                Right (sole :: Expression
sole@(ExFormation [BiLambda (FnSymbol Int
_)]), State
_) -> Binding -> IO Binding
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Attribute -> Expression -> Binding
BiTau Attribute
attr Expression
sole)
                Left (OutOfTime Int
cap) -> ReduceContext -> Int -> IO Binding
forall a. ReduceContext -> Int -> IO a
expired ReduceContext
ctx Int
cap
                Either ReduceException (Expression, State)
_ -> Binding -> IO Binding
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding
bd
        resolved Binding
bd = Binding -> IO Binding
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding
bd
        reducible :: Expression -> Bool
        reducible :: Expression -> Bool
reducible (ExDispatch Expression
_ Attribute
_) = Bool
True
        reducible (ExApplication Expression
_ Argument
_) = Bool
True
        reducible Expression
_ = Bool
False
        reading :: ReduceContext
        reading :: ReduceContext
reading = ReduceContext
ctx{_symbolic = emptyLambdas, _memo = Nothing, _tally = Nothing, _acyclic = Nothing, _saveStep = dontSaveStep, _saveEval = dontSaveEval}
        postponed :: [Binding] -> IO Expression
        postponed :: [Binding] -> IO Expression
postponed [Binding]
known = do
          Maybe Expression
call <- (Expression -> IO Expression)
-> Maybe Expression -> IO (Maybe Expression)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (Expression
-> ReduceContext
-> State
-> Expression
-> [Binding]
-> Expression
-> IO Expression
argued Expression
univ ReduceContext
ctx State
state' Expression
site [Binding]
known) (Expression -> ReduceContext -> [Binding] -> Maybe Expression
called Expression
univ ReduceContext
ctx [Binding]
known)
          Int
fresh <- ReduceContext -> IO Int
coined ReduceContext
caller
          ReduceContext
ctx._saveEval (Int
-> Int
-> Judgment
-> Expression
-> Maybe Expression
-> Expression
-> Evaluation
EvDeferred ReduceContext
ctx._nesting Int
fresh Judgment
Morphing ([Binding] -> Expression
ExFormation [Binding]
known) Maybe Expression
call (Expression -> Attribute -> Expression
ExDispatch Expression
site Attribute
AtPhi))
          Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Binding] -> Expression
ExFormation [Function -> Binding
BiLambda (Int -> Function
FnSymbol Int
fresh)])
    postponing ReduceContext
_ State
_ Expression
_ Expression
_ = Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
    concluded :: ReduceContext -> Lambda -> [Either Int Bytes] -> Subst -> State -> IO (Answer, State)
    concluded :: ReduceContext
-> Lambda
-> [Either Int Bytes]
-> Subst
-> State
-> IO (Answer, State)
concluded ReduceContext
ctx Lambda
entry [Either Int Bytes]
operands Subst
bound State
state' = case Lambda
entry._ending of
      Answering Expression
template -> ReduceContext
-> Expression
-> [Either Int Bytes]
-> Subst
-> State
-> IO (Answer, State)
answered ReduceContext
ctx Expression
template [Either Int Bytes]
operands Subst
bound State
state'
      Joining Either Meta Expression
on Expression
left Expression
right Maybe Function
fallback -> ReduceContext
-> [Text]
-> Subst
-> [(Text, Either Int Bytes)]
-> Either Meta Expression
-> Expression
-> Expression
-> Maybe Function
-> State
-> IO (Answer, State)
merged ReduceContext
ctx Lambda
entry._terminators Subst
bound ([Text] -> [Either Int Bytes] -> [(Text, Either Int Bytes)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Meta, Expression) -> Text) -> [(Meta, Expression)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Meta -> Text
_name (Meta -> Text)
-> ((Meta, Expression) -> Meta) -> (Meta, Expression) -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Meta, Expression) -> Meta
forall a b. (a, b) -> a
fst) Lambda
entry._dataized) [Either Int Bytes]
operands) Either Meta Expression
on Expression
left Expression
right Maybe Function
fallback State
state'
    answered :: ReduceContext -> Expression -> [Either Int Bytes] -> Subst -> State -> IO (Answer, State)
    answered :: ReduceContext
-> Expression
-> [Either Int Bytes]
-> Subst
-> State
-> IO (Answer, State)
answered ReduceContext
ctx Expression
template [Either Int Bytes]
operands Subst
bound State
state' = do
      ([(Slot, Function)]
fresh, Int
spent) <- Expression -> Int -> ([(Slot, Function)], Int)
minted Expression
template (Int -> ([(Slot, Function)], Int))
-> IO Int -> IO ([(Slot, Function)], Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef ReduceContext
ctx._minted
      IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef ReduceContext
ctx._minted Int
spent
      (Int -> IO ()) -> [Int] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Int
idx -> ReduceContext
ctx._saveEval (Int -> Int -> [Either Int Bytes] -> Evaluation
EvMinted ReduceContext
ctx._nesting Int
idx [Either Int Bytes]
operands)) [Int
idx | (Slot
_, FnSymbol Int
idx) <- [(Slot, Function)]
fresh]
      Subst
symbolic <- (Subst -> (Slot, Function) -> IO Subst)
-> Subst -> [(Slot, Function)] -> IO Subst
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Subst -> (Slot, Function) -> IO Subst
mint Subst
bound [(Slot, Function)]
fresh
      Expression
built <- Expression -> Subst -> IO Expression
buildExpressionThrows Expression
template Subst
symbolic
      ReduceContext
ctx._saveEval (Int -> Expression -> Evaluation
EvBuilt ReduceContext
ctx._nesting Expression
built)
      (Expression
normal, State
state'') <- Expression
-> Expression -> State -> ReduceContext -> IO (Expression, State)
settled Expression
built Expression
univ State
state' (ReduceContext -> IO (Expression, State))
-> IO ReduceContext -> IO (Expression, State)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Judgment -> ReduceContext -> IO ReduceContext
opening Judgment
Morphing ReduceContext
ctx{_saveEval = ctx._saveEval . resited ctx._site built}
      ReduceContext
ctx._saveEval (Int -> Expression -> Evaluation
EvAnswer ReduceContext
ctx._nesting Expression
normal)
      (Answer, State) -> IO (Answer, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Expression -> Answer
Answer Expression
built Expression
normal, State
state'')
    merged :: ReduceContext -> [T.Text] -> Subst -> [(T.Text, Either Int Bytes)] -> Either Meta Expression -> Expression -> Expression -> Maybe Function -> State -> IO (Answer, State)
    merged :: ReduceContext
-> [Text]
-> Subst
-> [(Text, Either Int Bytes)]
-> Either Meta Expression
-> Expression
-> Expression
-> Maybe Function
-> State
-> IO (Answer, State)
merged ReduceContext
ctx [Text]
terminators Subst
bound [(Text, Either Int Bytes)]
operands Either Meta Expression
on Expression
left Expression
right Maybe Function
fallback State
state' = do
      Either Int Bytes
condition <- [(Text, Either Int Bytes)]
-> Either Meta Expression -> IO (Either Int Bytes)
weighed [(Text, Either Int Bytes)]
operands Either Meta Expression
on
      (Expression
one, State
state'') <- ReduceContext
-> Subst -> Expression -> State -> IO (Expression, State)
reached ReduceContext
ctx Subst
bound Expression
left State
state'
      (Expression
two, State
state''') <- ReduceContext
-> Subst -> Expression -> State -> IO (Expression, State)
reached ReduceContext
ctx Subst
bound Expression
right State
state''
      Int
spent <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef ReduceContext
ctx._minted
      let raised :: Maybe Expression
raised = case (Expression -> Bool) -> [Expression] -> [Expression]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Text] -> Expression -> Bool
thrown [Text]
terminators) [Expression
one, Expression
two] of
            [Expression
side] -> Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
side
            [Expression]
_ -> Maybe Expression
forall a. Maybe a
Nothing
          stopped :: Expression -> Expression
          stopped :: Expression -> Expression
stopped Expression
side
            | Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
side Maybe Expression -> Maybe Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Expression
raised = Expression
ExTermination
            | Bool
otherwise = Expression
side
      case Expression
-> Expression
-> Int
-> Either
     [Attribute] (Expression, [(Int, (Int, Int))], Maybe Int, Int)
joined (Expression -> Expression
stopped Expression
one) (Expression -> Expression
stopped Expression
two) Int
spent of
        Right (Expression
term, [(Int, (Int, Int))]
made, Maybe Int
bottom, Int
spent') -> do
          IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef ReduceContext
ctx._minted Int
spent'
          ((Int, (Int, Int)) -> IO ()) -> [(Int, (Int, Int))] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Int
fresh, (Int, Int)
pair) -> ReduceContext
ctx._saveEval (Int
-> Either Text Expression
-> Int
-> (Int, Int)
-> Maybe Int
-> Maybe Expression
-> Evaluation
EvJoined ReduceContext
ctx._nesting ((Meta -> Either Text Expression)
-> (Expression -> Either Text Expression)
-> Either Meta Expression
-> Either Text Expression
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Text -> Either Text Expression
forall a b. a -> Either a b
Left (Text -> Either Text Expression)
-> (Meta -> Text) -> Meta -> Either Text Expression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Meta -> Text
_spelling) Expression -> Either Text Expression
forall a b. b -> Either a b
Right Either Meta Expression
on) Int
fresh (Int, Int)
pair Maybe Int
bottom Maybe Expression
raised)) [(Int, (Int, Int))]
made
          ReduceContext
ctx._saveEval (Int -> Expression -> Evaluation
EvTaken ReduceContext
ctx._nesting Expression
term)
          (Answer, State) -> IO (Answer, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Answer
Joined Expression
term, State
state''')
        Left [Attribute]
path -> case Either Refusal Expression
-> (Function -> Either Refusal Expression)
-> Maybe Function
-> Either Refusal Expression
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Refusal -> Either Refusal Expression
forall a b. a -> Either a b
Left Refusal
Unnamed) (\Function
name -> Function
-> Either Int Bytes
-> Expression
-> Expression
-> Either Refusal Expression
forked Function
name Either Int Bytes
condition Expression
one Expression
two) Maybe Function
fallback of
          Right Expression
term -> do
            ReduceContext
ctx._saveEval (Int
-> (Expression, Expression)
-> (Expression, Expression)
-> Expression
-> Evaluation
EvFabricated ReduceContext
ctx._nesting (Expression
left, Expression
one) (Expression
right, Expression
two) Expression
term)
            (Answer, State) -> IO (Answer, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Answer
Joined Expression
term, State
state''')
          Left (Unripe Side
side Attribute
attr) -> do
            ReduceContext
ctx._saveEval (Int
-> (Expression, Expression)
-> (Expression, Expression)
-> Side
-> Attribute
-> Evaluation
EvUnripe ReduceContext
ctx._nesting (Expression
left, Expression
one) (Expression
right, Expression
two) Side
side Attribute
attr)
            ReduceException -> IO (Answer, State)
forall e a. Exception e => e -> IO a
throwIO (Text -> ReduceException
Diverged Text
func)
          Left Refusal
refusal -> do
            ReduceContext
ctx._saveEval (Int
-> (Expression, Expression)
-> (Expression, Expression)
-> [Attribute]
-> Refusal
-> Evaluation
EvDiverged ReduceContext
ctx._nesting (Expression
left, Expression
one) (Expression
right, Expression
two) [Attribute]
path Refusal
refusal)
            ReduceException -> IO (Answer, State)
forall e a. Exception e => e -> IO a
throwIO (Text -> ReduceException
Diverged Text
func)
    weighed :: [(T.Text, Either Int Bytes)] -> Either Meta Expression -> IO (Either Int Bytes)
    weighed :: [(Text, Either Int Bytes)]
-> Either Meta Expression -> IO (Either Int Bytes)
weighed [(Text, Either Int Bytes)]
operands (Left Meta
meta) =
      IO (Either Int Bytes)
-> (Either Int Bytes -> IO (Either Int Bytes))
-> Maybe (Either Int Bytes)
-> IO (Either Int Bytes)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
        (IOError -> IO (Either Int Bytes)
forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"The meta '%s' of λ function '%s' is bound by no operand of 'dataize'" (Text -> String
T.unpack Meta
meta._spelling) (Text -> String
T.unpack Text
func))))
        Either Int Bytes -> IO (Either Int Bytes)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        (Text -> [(Text, Either Int Bytes)] -> Maybe (Either Int Bytes)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Meta
meta._name [(Text, Either Int Bytes)]
operands)
    weighed [(Text, Either Int Bytes)]
_ (Right Expression
path) = Expression -> IO Expression
operand Expression
path IO Expression
-> (Expression -> IO (Either Int Bytes)) -> IO (Either Int Bytes)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO (Either Int Bytes)
-> (Either Int Bytes -> IO (Either Int Bytes))
-> Maybe (Either Int Bytes)
-> IO (Either Int Bytes)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ReduceException -> IO (Either Int Bytes)
forall e a. Exception e => e -> IO a
throwIO (Text -> ReduceException
Stuck Text
func)) Either Int Bytes -> IO (Either Int Bytes)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Either Int Bytes) -> IO (Either Int Bytes))
-> (Expression -> Maybe (Either Int Bytes))
-> Expression
-> IO (Either Int Bytes)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression -> Maybe (Either Int Bytes)
held
      where
        held :: Expression -> Maybe (Either Int Bytes)
        held :: Expression -> Maybe (Either Int Bytes)
held Expression
term = case Expression -> Maybe Expression
walked Expression
term of
          Just (ExFormation [Binding]
bds) -> [Either Int Bytes] -> Maybe (Either Int Bytes)
forall a. [a] -> Maybe a
listToMaybe ([Int -> Either Int Bytes
forall a b. a -> Either a b
Left Int
idx | BiLambda (FnSymbol Int
idx) <- [Binding]
bds] [Either Int Bytes] -> [Either Int Bytes] -> [Either Int Bytes]
forall a. [a] -> [a] -> [a]
++ [Bytes -> Either Int Bytes
forall a b. b -> Either a b
Right Bytes
bytes | BiDelta Bytes
bytes <- [Binding]
bds])
          Maybe Expression
_ -> Maybe (Either Int Bytes)
forall a. Maybe a
Nothing
        walked :: Expression -> Maybe Expression
        walked :: Expression -> Maybe Expression
walked (ExDispatch Expression
base Attribute
attr) = case Expression -> Maybe Expression
walked Expression
base of
          Just (ExFormation [Binding]
bds) -> [Expression] -> Maybe Expression
forall a. [a] -> Maybe a
listToMaybe [Expression
term | BiTau Attribute
attr' Expression
term <- [Binding]
bds, Attribute
attr' Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
attr]
          Maybe Expression
_ -> Maybe Expression
forall a. Maybe a
Nothing
        walked Expression
term = Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
term
    reached :: ReduceContext -> Subst -> Expression -> State -> IO (Expression, State)
    reached :: ReduceContext
-> Subst -> Expression -> State -> IO (Expression, State)
reached ReduceContext
_ Subst
bound (ExMeta Text
name) State
state' = (,State
state') (Expression -> (Expression, State))
-> IO Expression -> IO (Expression, State)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Subst -> IO Expression
buildExpressionThrows (Text -> Expression
ExMeta Text
name) Subst
bound
    reached ReduceContext
ctx Subst
_ Expression
side State
state' = (\Expression
placed -> Expression
-> ReduceContext -> Expression -> State -> IO (Expression, State)
morphing Expression
univ ReduceContext
ctx{_site = side} Expression
placed State
state') (Expression -> IO (Expression, State))
-> IO Expression -> IO (Expression, State)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expression -> IO Expression
operand Expression
side
    mint :: Subst -> (Slot, Function) -> IO Subst
    mint :: Subst -> (Slot, Function) -> IO Subst
mint Subst
bound (Slot
slot, Function
fresh) = case Subst -> Subst -> Maybe Subst
combine (Slot -> MetaValue -> Subst
substSlot Slot
slot (Function -> MetaValue
MvFunction Function
fresh)) Subst
bound of
      Just Subst
bound' -> Subst -> IO Subst
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst
bound'
      Maybe Subst
Nothing -> IOError -> IO Subst
forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"A fresh symbol of λ function '%s' clashes with an existing binding" (Text -> String
T.unpack Text
func)))
    operand :: Expression -> IO Expression
    operand :: Expression -> IO Expression
operand Expression
term = ReduceContext
caller._engine._contextualize Expression
term Expression
self
    bind :: Meta -> MetaValue -> Subst -> IO Subst
    bind :: Meta -> MetaValue -> Subst -> IO Subst
bind Meta
meta MetaValue
value Subst
bound = case Subst -> Subst -> Maybe Subst
combine (Text -> MetaValue -> Subst
substSingle Meta
meta._name MetaValue
value) Subst
bound of
      Just Subst
bound' -> Subst -> IO Subst
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst
bound'
      Maybe Subst
Nothing ->
        IOError -> IO Subst
forall e a. Exception e => e -> IO a
throwIO
          (String -> IOError
userError (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"The meta '%s' of λ function '%s' clashes with an existing binding" (Text -> String
T.unpack Meta
meta._spelling) (Text -> String
T.unpack Text
func)))