{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# OPTIONS_GHC -Wno-unused-record-wildcards #-}

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

module Morph (Answer (..), Deadline (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), admitting, argued, awaited, boxed, called, carried, charged, coined, counted, deeper, emptyState, ended, enter, entering, execBuildTerm, expired, fired, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, opening, origin, parking, recalled, refused, remember, remembered, retained, settled, severing, starved, tallied, timed, universed, unparked) where

import AST
import Builder (buildExpressionThrows, nameIn)
import Control.Applicative ((<|>))
import Control.Exception (Exception, catch, evaluate, throwIO, try)
import Control.Monad (when)
import Data.IORef (IORef, atomicModifyIORef', modifyIORef', newIORef, readIORef, writeIORef)
import Data.List (find, partition)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe, isJust, listToMaybe)
import qualified Data.Text as T
import Deps (Acyclic (..), BuildTermFunc, BuildTermMethod, Evaluation (..), Judgment (..), SaveEvalFunc, SaveStepFunc, State (..), Term (..), dontSaveStep)
import Engine (Engine (..))
import GHC.Clock (getMonotonicTime)
import qualified Inference as In
import Lambdas (Lambdas)
import Locator (locatedExpression, withLocatedExpression)
import Matcher (substEmpty)
import Must (Must (..))
import Printer (printExpression)
import Random (shuffle)
import Rewriter (RewriteContext (RewriteContext), Rewritten, Seen, rewrite, seenInsert)
import Rule (RuleContext (RuleContext))
import System.Timeout (timeout)
import Text.Printf (printf)
import Yaml (ExtraArgument (..))

type Morphed = (Expression, NonEmpty Rewritten)

type ReductionFunc = Expression -> ReduceContext -> Expression -> State -> IO (Maybe Bytes, State)

type EvaluationFunc = ReduceContext -> State -> Expression -> Expression -> IO (Expression, State)

emptyState :: State
emptyState :: State
emptyState = Maybe Int -> Maybe Text -> [Expression] -> State
State Maybe Int
forall a. Maybe a
Nothing Maybe Text
forall a. Maybe a
Nothing []

data Steps = Steps
  { Steps -> Int
_limit :: Int
  , Steps -> Int
_spent :: Int
  }

data Tally = Tally
  { Tally -> Int
_ceiling :: Int
  , Tally -> IORef Int
_count :: IORef Int
  }

data Deadline = Deadline
  { Deadline -> Int
_seconds :: Int
  , Deadline -> Double
_until :: Double
  }

data Memo = Memo (IORef (Store (Int, Kept))) (IORef (Map.Map Firing Answer)) (IORef Int) (IORef Int)

data Answer
  = Answer Expression Expression
  | Joined Expression

ended :: Answer -> Expression
ended :: Answer -> Expression
ended (Answer Expression
_ Expression
normal) = Expression
normal
ended (Joined Expression
normal) = Expression
normal

data Firing = Firing T.Text [Either Int Bytes] [Expression]
  deriving (Firing -> Firing -> Bool
(Firing -> Firing -> Bool)
-> (Firing -> Firing -> Bool) -> Eq Firing
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Firing -> Firing -> Bool
== :: Firing -> Firing -> Bool
$c/= :: Firing -> Firing -> Bool
/= :: Firing -> Firing -> Bool
Eq, Eq Firing
Eq Firing =>
(Firing -> Firing -> Ordering)
-> (Firing -> Firing -> Bool)
-> (Firing -> Firing -> Bool)
-> (Firing -> Firing -> Bool)
-> (Firing -> Firing -> Bool)
-> (Firing -> Firing -> Firing)
-> (Firing -> Firing -> Firing)
-> Ord Firing
Firing -> Firing -> Bool
Firing -> Firing -> Ordering
Firing -> Firing -> Firing
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Firing -> Firing -> Ordering
compare :: Firing -> Firing -> Ordering
$c< :: Firing -> Firing -> Bool
< :: Firing -> Firing -> Bool
$c<= :: Firing -> Firing -> Bool
<= :: Firing -> Firing -> Bool
$c> :: Firing -> Firing -> Bool
> :: Firing -> Firing -> Bool
$c>= :: Firing -> Firing -> Bool
>= :: Firing -> Firing -> Bool
$cmax :: Firing -> Firing -> Firing
max :: Firing -> Firing -> Firing
$cmin :: Firing -> Firing -> Firing
min :: Firing -> Firing -> Firing
Ord)

data Kept
  = Answered Answer
  | Looped Expression
  | Stalled T.Text Int

type Store answer = Map.Map Int [(Expression, answer)]

data ReduceContext = ReduceContext
  { ReduceContext -> Expression
_locator :: Expression
  , ReduceContext -> Expression
_site :: Expression
  , ReduceContext -> Maybe Expression
_universe :: Maybe Expression
  , ReduceContext -> Int
_maxDepth :: Int
  , ReduceContext -> Int
_maxCycles :: Int
  , ReduceContext -> Steps
_steps :: Steps
  , ReduceContext -> Maybe Tally
_tally :: Maybe Tally
  , ReduceContext -> IORef Int
_minted :: IORef Int
  , ReduceContext -> Maybe Deadline
_deadline :: Maybe Deadline
  , ReduceContext -> Maybe Memo
_memo :: Maybe Memo
  , ReduceContext -> Int
_nesting :: Int
  , ReduceContext -> Maybe (Int, Judgment, Expression)
_opened :: Maybe (Int, Judgment, Expression)
  , ReduceContext -> Bool
_depthSensitive :: Bool
  , ReduceContext -> Bool
_shuffle :: Bool
  , ReduceContext -> Bool
_partial :: Bool
  , ReduceContext -> Maybe Acyclic
_acyclic :: Maybe Acyclic
  , ReduceContext -> Int
_maxLoops :: Int
  , ReduceContext -> Judgment
_judgment :: Judgment
  , ReduceContext -> [Text]
_parked :: [T.Text]
  , ReduceContext -> Seen
_entered :: Seen
  , ReduceContext -> Maybe (Expression, [Binding], Expression)
_placed :: Maybe (Expression, [Binding], Expression)
  , ReduceContext -> Lambdas
_symbolic :: Lambdas
  , ReduceContext -> BuildTermFunc
_buildTerm :: BuildTermFunc
  , ReduceContext -> ReductionFunc
_reduce :: ReductionFunc
  , ReduceContext
-> ReduceContext
-> State
-> Expression
-> Expression
-> IO (Expression, State)
_evaluate :: EvaluationFunc
  , ReduceContext -> SaveStepFunc
_saveStep :: SaveStepFunc
  , ReduceContext -> Evaluation -> IO ()
_saveEval :: SaveEvalFunc
  , ReduceContext -> Engine
_engine :: Engine
  }

data Budget
  = Depth Judgment Int
  | Firings Int
  | Cycles Int

data ReduceException
  = OutOfSteps Budget
  | OutOfTime Int
  | Stuck T.Text
  | StuckAt T.Text (NonEmpty Rewritten) State
  | OutOfStepsAt Budget (NonEmpty Rewritten) State
  | Diverged T.Text
  | Looping Expression
  | LoopingAt Expression (NonEmpty Rewritten) State
  | Undataizable Expression (NonEmpty Rewritten) State
  | Unmorphable Expression
  deriving anyclass (Show ReduceException
Typeable ReduceException
(Typeable ReduceException, Show ReduceException) =>
(ReduceException -> SomeException)
-> (SomeException -> Maybe ReduceException)
-> (ReduceException -> String)
-> Exception ReduceException
SomeException -> Maybe ReduceException
ReduceException -> String
ReduceException -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e) -> (e -> String) -> Exception e
$ctoException :: ReduceException -> SomeException
toException :: ReduceException -> SomeException
$cfromException :: SomeException -> Maybe ReduceException
fromException :: SomeException -> Maybe ReduceException
$cdisplayException :: ReduceException -> String
displayException :: ReduceException -> String
Exception)

instance Show ReduceException where
  show :: ReduceException -> String
show (OutOfSteps (Depth Judgment
judgment Int
limit)) =
    String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s did not finish before reaching the limit of steps: --max-steps=%d" (Judgment -> String
forall a. Show a => a -> String
show Judgment
judgment) Int
limit
  show (OutOfSteps (Firings Int
limit)) =
    String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"Evaluation did not finish before reaching the limit of firings: --max-firings=%d" Int
limit
  show (OutOfSteps (Cycles Int
limit)) =
    String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"Normalization did not finish before reaching the limit of cycles: --max-cycles=%d" Int
limit
  show (OutOfStepsAt Budget
budget NonEmpty Rewritten
_ State
_) = ReduceException -> String
forall a. Show a => a -> String
show (Budget -> ReduceException
OutOfSteps Budget
budget)
  show (OutOfTime Int
limit) =
    String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"Evaluation did not finish before reaching the limit of seconds: --max-seconds=%d" Int
limit
  show (Stuck Text
func) = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"No entry of --symbolic answers the λ function '%s'" (Text -> String
T.unpack Text
func)
  show (StuckAt Text
func NonEmpty Rewritten
_ State
_) = ReduceException -> String
forall a. Show a => a -> String
show (Text -> ReduceException
Stuck Text
func)
  show (Diverged Text
func) = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"The λ function '%s' could not join its two sides" (Text -> String
T.unpack Text
func)
  show (Looping Expression
term) = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"Reduction entered a formation it is already inside: %s" (Expression -> String
printExpression Expression
term)
  show (LoopingAt Expression
term NonEmpty Rewritten
_ State
_) = ReduceException -> String
forall a. Show a => a -> String
show (Expression -> ReduceException
Looping Expression
term)
  show (Undataizable Expression
ExTermination NonEmpty Rewritten
_ State
_) = String
"dataization reached the terminator ⊥, which signals an error and cannot be dataized"
  show (Undataizable Expression
term NonEmpty Rewritten
_ State
_) = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"no dataization rule matched, while dataization expects a normal form: %s" (Expression -> String
printExpression Expression
term)
  show (Unmorphable Expression
term) = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"Morphing expects a normal form, but no morphing rule matches: %s" (Expression -> String
printExpression Expression
term)

deeper :: ReduceContext -> IO ReduceContext
deeper :: ReduceContext -> IO ReduceContext
deeper ctx :: ReduceContext
ctx@ReduceContext{$sel:_steps:ReduceContext :: ReduceContext -> Steps
_steps = Steps Int
limit Int
spent} = do
  ReduceContext -> IO ()
clocked ReduceContext
ctx
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
spent Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
limit) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    Maybe Memo -> IO ()
starve ReduceContext
ctx._memo
    ReduceContext
ctx._saveEval (Int -> Int -> Judgment -> Expression -> Evaluation
EvStarved ReduceContext
ctx._nesting Int
limit ReduceContext
ctx._judgment ReduceContext
ctx._site)
    ReduceException -> IO ()
forall e a. Exception e => e -> IO a
throwIO (Budget -> ReduceException
OutOfSteps (Judgment -> Int -> Budget
Depth ReduceContext
ctx._judgment Int
limit))
  ReduceContext -> IO ReduceContext
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ReduceContext
ctx{_steps = Steps limit (spent + 1)}
  where
    starve :: Maybe Memo -> IO ()
    starve :: Maybe Memo -> IO ()
starve Maybe Memo
Nothing = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    starve (Just (Memo IORef (Store (Int, Kept))
_ IORef (Map Firing Answer)
_ IORef Int
_ IORef Int
exhausted)) = IORef Int -> (Int -> Int) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Int
exhausted (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

tallied :: Maybe Int -> IO (Maybe Tally)
tallied :: Maybe Int -> IO (Maybe Tally)
tallied = (Int -> IO Tally) -> Maybe Int -> IO (Maybe Tally)
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 (\Int
cap -> Int -> IORef Int -> Tally
Tally Int
cap (IORef Int -> Tally) -> IO (IORef Int) -> IO Tally
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0)

timed :: Maybe Int -> IO (Maybe Deadline)
timed :: Maybe Int -> IO (Maybe Deadline)
timed = (Int -> IO Deadline) -> Maybe Int -> IO (Maybe Deadline)
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 (\Int
cap -> Int -> Double -> Deadline
Deadline Int
cap (Double -> Deadline) -> (Double -> Double) -> Double -> Deadline
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
cap) (Double -> Deadline) -> IO Double -> IO Deadline
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Double
getMonotonicTime)

charged :: ReduceContext -> IO ()
charged :: ReduceContext -> IO ()
charged ReduceContext
ctx = do
  ReduceContext -> IO ()
clocked ReduceContext
ctx
  (Tally -> IO ()) -> Maybe Tally -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Tally -> IO ()
billed ReduceContext
ctx._tally
  where
    billed :: Tally -> IO ()
    billed :: Tally -> IO ()
billed (Tally Int
cap IORef Int
count) = do
      Int
fired <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
count
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
fired Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
cap) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        ReduceContext
ctx._saveEval (Int -> Int -> Judgment -> Expression -> Evaluation
EvSpent ReduceContext
ctx._nesting Int
cap ReduceContext
ctx._judgment ReduceContext
ctx._site)
        ReduceException -> IO ()
forall e a. Exception e => e -> IO a
throwIO (Budget -> ReduceException
OutOfSteps (Int -> Budget
Firings Int
cap))
      IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Int
count (Int
fired Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

clocked :: ReduceContext -> IO ()
clocked :: ReduceContext -> IO ()
clocked ReduceContext
ctx = (Deadline -> IO ()) -> Maybe Deadline -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Deadline -> IO ()
clock ReduceContext
ctx._deadline
  where
    clock :: Deadline -> IO ()
    clock :: Deadline -> IO ()
clock (Deadline Int
cap Double
due) = do
      Double
now <- IO Double
getMonotonicTime
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Double
now Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
>= Double
due) (ReduceContext -> Int -> IO ()
forall a. ReduceContext -> Int -> IO a
expired ReduceContext
ctx Int
cap)

expired :: ReduceContext -> Int -> IO a
expired :: forall a. ReduceContext -> Int -> IO a
expired ReduceContext
ctx Int
cap = do
  ReduceContext
ctx._saveEval (Int -> Int -> Judgment -> Expression -> Evaluation
EvTimeout ReduceContext
ctx._nesting Int
cap ReduceContext
ctx._judgment ReduceContext
ctx._site)
  ReduceException -> IO a
forall e a. Exception e => e -> IO a
throwIO (Int -> ReduceException
OutOfTime Int
cap)

awaited :: ReduceContext -> IO a -> IO a
awaited :: forall a. ReduceContext -> IO a -> IO a
awaited ReduceContext
ctx IO a
action = case ReduceContext
ctx._deadline of
  Maybe Deadline
Nothing -> IO a
action
  Just (Deadline Int
cap Double
due) -> do
    Double
now <- IO Double
getMonotonicTime
    IO a -> (a -> IO a) -> Maybe a -> IO a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ReduceContext -> Int -> IO a
forall a. ReduceContext -> Int -> IO a
expired ReduceContext
ctx Int
cap) a -> IO a
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe a -> IO a) -> IO (Maybe a) -> IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> IO a -> IO (Maybe a)
forall a. Int -> IO a -> IO (Maybe a)
timeout (Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Double -> Double -> Double
forall a. Ord a => a -> a -> a
max Double
0 (Double
due Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
now) Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
1000000)) IO a
action

memoized :: Maybe Acyclic -> IO (Maybe Memo)
memoized :: Maybe Acyclic -> IO (Maybe Memo)
memoized (Just Acyclic
Plausible) = Memo -> Maybe Memo
forall a. a -> Maybe a
Just (Memo -> Maybe Memo) -> IO Memo -> IO (Maybe Memo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (IORef (Store (Int, Kept))
-> IORef (Map Firing Answer) -> IORef Int -> IORef Int -> Memo
Memo (IORef (Store (Int, Kept))
 -> IORef (Map Firing Answer) -> IORef Int -> IORef Int -> Memo)
-> IO (IORef (Store (Int, Kept)))
-> IO (IORef (Map Firing Answer) -> IORef Int -> IORef Int -> Memo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Store (Int, Kept) -> IO (IORef (Store (Int, Kept)))
forall a. a -> IO (IORef a)
newIORef Store (Int, Kept)
forall k a. Map k a
Map.empty IO (IORef (Map Firing Answer) -> IORef Int -> IORef Int -> Memo)
-> IO (IORef (Map Firing Answer))
-> IO (IORef Int -> IORef Int -> Memo)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map Firing Answer -> IO (IORef (Map Firing Answer))
forall a. a -> IO (IORef a)
newIORef Map Firing Answer
forall k a. Map k a
Map.empty IO (IORef Int -> IORef Int -> Memo)
-> IO (IORef Int) -> IO (IORef Int -> Memo)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0 IO (IORef Int -> Memo) -> IO (IORef Int) -> IO Memo
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0)
memoized Maybe Acyclic
_ = Maybe Memo -> IO (Maybe Memo)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Memo
forall a. Maybe a
Nothing

recalled :: Maybe Memo -> Expression -> Int -> IO (Maybe Kept)
recalled :: Maybe Memo -> Expression -> Int -> IO (Maybe Kept)
recalled Maybe Memo
Nothing Expression
_ Int
_ = Maybe Kept -> IO (Maybe Kept)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Kept
forall a. Maybe a
Nothing
recalled (Just (Memo IORef (Store (Int, Kept))
store IORef (Map Firing Answer)
_ IORef Int
answers IORef Int
_)) Expression
form Int
spent = do
  Store (Int, Kept)
kept <- IORef (Store (Int, Kept)) -> IO (Store (Int, Kept))
forall a. IORef a -> IO a
readIORef IORef (Store (Int, Kept))
store
  Int
count <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
answers
  let live :: [Kept]
live = [Kept
known | (Expression
term, (Int
stamp, Kept
known)) <- [(Expression, (Int, Kept))]
-> Int -> Store (Int, Kept) -> [(Expression, (Int, Kept))]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] (Expression -> Int
hashExpression Expression
form) Store (Int, Kept)
kept, Expression
term Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
form, Int -> Int -> Kept -> Bool
current Int
count Int
stamp Kept
known]
  Maybe Kept -> IO (Maybe Kept)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Kept -> Bool) -> [Kept] -> Maybe Kept
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Kept -> Bool
answered [Kept]
live Maybe Kept -> Maybe Kept -> Maybe Kept
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Kept] -> Maybe Kept
forall a. [a] -> Maybe a
listToMaybe [Kept]
live)
  where
    current :: Int -> Int -> Kept -> Bool
    current :: Int -> Int -> Kept -> Bool
current Int
count Int
stamp (Stalled Text
_ Int
least) = Int
stamp Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
count Bool -> Bool -> Bool
&& Int
spent Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
least
    current Int
_ Int
_ Kept
_ = Bool
True
    answered :: Kept -> Bool
    answered :: Kept -> Bool
answered (Answered Answer
_) = Bool
True
    answered Kept
_ = Bool
False

counted :: Maybe Memo -> IO Int
counted :: Maybe Memo -> IO Int
counted Maybe Memo
Nothing = Int -> IO Int
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0
counted (Just (Memo IORef (Store (Int, Kept))
_ IORef (Map Firing Answer)
_ IORef Int
answers IORef Int
_)) = IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
answers

starved :: Maybe Memo -> IO Int
starved :: Maybe Memo -> IO Int
starved Maybe Memo
Nothing = Int -> IO Int
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0
starved (Just (Memo IORef (Store (Int, Kept))
_ IORef (Map Firing Answer)
_ IORef Int
_ IORef Int
exhausted)) = IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
exhausted

retained :: Maybe Memo -> Expression -> Int -> Kept -> IO ()
retained :: Maybe Memo -> Expression -> Int -> Kept -> IO ()
retained Maybe Memo
Nothing Expression
_ Int
_ Kept
_ = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
retained (Just (Memo IORef (Store (Int, Kept))
store IORef (Map Firing Answer)
_ IORef Int
_ IORef Int
_)) Expression
form Int
stamp Kept
kept =
  IORef (Store (Int, Kept))
-> (Store (Int, Kept) -> Store (Int, Kept)) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Store (Int, Kept))
store (([(Expression, (Int, Kept))]
 -> [(Expression, (Int, Kept))] -> [(Expression, (Int, Kept))])
-> Int
-> [(Expression, (Int, Kept))]
-> Store (Int, Kept)
-> Store (Int, Kept)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [(Expression, (Int, Kept))]
-> [(Expression, (Int, Kept))] -> [(Expression, (Int, Kept))]
forall a. [a] -> [a] -> [a]
(++) (Expression -> Int
hashExpression Expression
form) [(Expression
form, (Int
stamp, Kept
kept))])

remembered :: Maybe Memo -> Firing -> IO (Maybe Answer)
remembered :: Maybe Memo -> Firing -> IO (Maybe Answer)
remembered Maybe Memo
Nothing Firing
_ = Maybe Answer -> IO (Maybe Answer)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Answer
forall a. Maybe a
Nothing
remembered (Just (Memo IORef (Store (Int, Kept))
_ IORef (Map Firing Answer)
firings IORef Int
_ IORef Int
_)) Firing
firing = Firing -> Map Firing Answer -> Maybe Answer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Firing
firing (Map Firing Answer -> Maybe Answer)
-> IO (Map Firing Answer) -> IO (Maybe Answer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Map Firing Answer) -> IO (Map Firing Answer)
forall a. IORef a -> IO a
readIORef IORef (Map Firing Answer)
firings

remember :: Maybe Memo -> Firing -> Answer -> IO ()
remember :: Maybe Memo -> Firing -> Answer -> IO ()
remember Maybe Memo
Nothing Firing
_ Answer
_ = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
remember (Just (Memo IORef (Store (Int, Kept))
_ IORef (Map Firing Answer)
firings IORef Int
answers IORef Int
_)) Firing
firing Answer
answer = do
  IORef (Map Firing Answer)
-> (Map Firing Answer -> Map Firing Answer) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Map Firing Answer)
firings (Firing -> Answer -> Map Firing Answer -> Map Firing Answer
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Firing
firing Answer
answer)
  IORef Int -> (Int -> Int) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Int
answers (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

parking :: NonEmpty Rewritten -> State -> IO a -> IO a
parking :: forall a. NonEmpty Rewritten -> State -> IO a -> IO a
parking NonEmpty Rewritten
seq State
state IO a
action = IO a
action IO a -> (ReduceException -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` ReduceException -> IO a
forall a. ReduceException -> IO a
rethrow
  where
    rethrow :: ReduceException -> IO a
    rethrow :: forall a. ReduceException -> IO a
rethrow (Stuck Text
func) = ReduceException -> IO a
forall e a. Exception e => e -> IO a
throwIO (Text -> NonEmpty Rewritten -> State -> ReduceException
StuckAt Text
func NonEmpty Rewritten
seq State
state)
    rethrow (OutOfSteps Budget
budget) = ReduceException -> IO a
forall e a. Exception e => e -> IO a
throwIO (Budget -> NonEmpty Rewritten -> State -> ReduceException
OutOfStepsAt Budget
budget NonEmpty Rewritten
seq State
state)
    rethrow (Looping Expression
term) = ReduceException -> IO a
forall e a. Exception e => e -> IO a
throwIO (Expression -> NonEmpty Rewritten -> State -> ReduceException
LoopingAt Expression
term NonEmpty Rewritten
seq State
state)
    rethrow ReduceException
failure = ReduceException -> IO a
forall e a. Exception e => e -> IO a
throwIO ReduceException
failure

unparked :: IO a -> IO a
unparked :: forall a. IO a -> IO a
unparked IO a
action = IO a
action IO a -> (ReduceException -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` ReduceException -> IO a
forall a. ReduceException -> IO a
rethrow
  where
    rethrow :: ReduceException -> IO a
    rethrow :: forall a. ReduceException -> IO a
rethrow (StuckAt Text
func NonEmpty Rewritten
_ State
_) = ReduceException -> IO a
forall e a. Exception e => e -> IO a
throwIO (Text -> ReduceException
Stuck Text
func)
    rethrow (OutOfStepsAt Budget
budget NonEmpty Rewritten
_ State
_) = ReduceException -> IO a
forall e a. Exception e => e -> IO a
throwIO (Budget -> ReduceException
OutOfSteps Budget
budget)
    rethrow (LoopingAt Expression
term NonEmpty Rewritten
_ State
_) = ReduceException -> IO a
forall e a. Exception e => e -> IO a
throwIO (Expression -> ReduceException
Looping Expression
term)
    rethrow ReduceException
failure = ReduceException -> IO a
forall e a. Exception e => e -> IO a
throwIO ReduceException
failure

entering :: Expression -> ReduceContext -> IO ReduceContext
entering :: Expression -> ReduceContext -> IO ReduceContext
entering Expression
term ReduceContext
ctx = IO ReduceContext
-> (Expression -> IO ReduceContext)
-> Maybe Expression
-> IO ReduceContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ReduceContext -> IO ReduceContext
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ReduceContext
ctx) (Expression -> ReduceContext -> IO ReduceContext
`enter` ReduceContext
ctx) (Judgment -> Expression -> Maybe Expression
entrance ReduceContext
ctx._judgment Expression
term)

admitting :: Expression -> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext)
admitting :: Expression
-> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext)
admitting Expression
term ReduceContext
ctx = IO (Either (Acyclic, Expression) ReduceContext)
-> (Expression -> IO (Either (Acyclic, Expression) ReduceContext))
-> Maybe Expression
-> IO (Either (Acyclic, Expression) ReduceContext)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Either (Acyclic, Expression) ReduceContext
-> IO (Either (Acyclic, Expression) ReduceContext)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ReduceContext -> Either (Acyclic, Expression) ReduceContext
forall a b. b -> Either a b
Right ReduceContext
ctx)) (Expression
-> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext)
`admitted` ReduceContext
ctx) (Judgment -> Expression -> Maybe Expression
entrance ReduceContext
ctx._judgment Expression
term)

enter :: Expression -> ReduceContext -> IO ReduceContext
enter :: Expression -> ReduceContext -> IO ReduceContext
enter Expression
form ReduceContext
ctx = Expression
-> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext)
admitted Expression
form ReduceContext
ctx IO (Either (Acyclic, Expression) ReduceContext)
-> (Either (Acyclic, Expression) ReduceContext -> IO ReduceContext)
-> IO ReduceContext
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ((Acyclic, Expression) -> IO ReduceContext)
-> (ReduceContext -> IO ReduceContext)
-> Either (Acyclic, Expression) ReduceContext
-> IO ReduceContext
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Expression
-> ReduceContext -> (Acyclic, Expression) -> IO ReduceContext
forall a.
Expression -> ReduceContext -> (Acyclic, Expression) -> IO a
refused Expression
form ReduceContext
ctx) ReduceContext -> IO ReduceContext
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

refused :: Expression -> ReduceContext -> (Acyclic, Expression) -> IO a
refused :: forall a.
Expression -> ReduceContext -> (Acyclic, Expression) -> IO a
refused Expression
form ReduceContext
ctx (Acyclic
mode, Expression
before) = do
  ReduceContext
ctx._saveEval (Int
-> Judgment
-> Acyclic
-> Expression
-> Expression
-> Maybe (Int, Expression)
-> Evaluation
EvLooped ReduceContext
ctx._nesting ReduceContext
ctx._judgment Acyclic
mode Expression
before ReduceContext
ctx._site Maybe (Int, Expression)
forall a. Maybe a
Nothing)
  ReduceException -> IO a
forall e a. Exception e => e -> IO a
throwIO (Expression -> ReduceException
Looping Expression
form)

severing :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, ReduceContext)
severing :: Expression
-> Expression
-> State
-> ReduceContext
-> IO (Expression, ReduceContext)
severing Expression
term Expression
univ State
state ReduceContext
ctx = case Judgment -> Expression -> Maybe Expression
entrance ReduceContext
ctx._judgment Expression
term of
  Just Expression
form -> (Expression -> (Expression, ReduceContext))
-> (ReduceContext -> (Expression, ReduceContext))
-> Either Expression ReduceContext
-> (Expression, ReduceContext)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (,ReduceContext
ctx) (Expression
term,) (Either Expression ReduceContext -> (Expression, ReduceContext))
-> IO (Either Expression ReduceContext)
-> IO (Expression, ReduceContext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression
-> Expression
-> State
-> ReduceContext
-> IO (Either Expression ReduceContext)
sever Expression
form Expression
univ State
state ReduceContext
ctx
  Maybe Expression
Nothing -> (Expression, ReduceContext) -> IO (Expression, ReduceContext)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
term, ReduceContext
ctx)

sever :: Expression -> Expression -> State -> ReduceContext -> IO (Either Expression ReduceContext)
sever :: Expression
-> Expression
-> State
-> ReduceContext
-> IO (Either Expression ReduceContext)
sever Expression
form Expression
univ State
state ReduceContext
ctx = Expression
-> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext)
admitted Expression
form ReduceContext
ctx IO (Either (Acyclic, Expression) ReduceContext)
-> (Either (Acyclic, Expression) ReduceContext
    -> IO (Either Expression ReduceContext))
-> IO (Either Expression ReduceContext)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ((Acyclic, Expression) -> IO (Either Expression ReduceContext))
-> (ReduceContext -> IO (Either Expression ReduceContext))
-> Either (Acyclic, Expression) ReduceContext
-> IO (Either Expression ReduceContext)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Acyclic, Expression) -> IO (Either Expression ReduceContext)
cut (Either Expression ReduceContext
-> IO (Either Expression ReduceContext)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Expression ReduceContext
 -> IO (Either Expression ReduceContext))
-> (ReduceContext -> Either Expression ReduceContext)
-> ReduceContext
-> IO (Either Expression ReduceContext)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReduceContext -> Either Expression ReduceContext
forall a b. b -> Either a b
Right (ReduceContext -> Either Expression ReduceContext)
-> (ReduceContext -> ReduceContext)
-> ReduceContext
-> Either Expression ReduceContext
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReduceContext -> ReduceContext
placing)
  where
    placing :: ReduceContext -> ReduceContext
    placing :: ReduceContext -> ReduceContext
placing ReduceContext
entered = case Expression
form of
      ExFormation [Binding]
known -> ReduceContext
entered{_placed = maybe entered._placed (Just . (form,known,)) (called univ ctx known)}
      Expression
_ -> ReduceContext
entered
    cut :: (Acyclic, Expression) -> IO (Either Expression ReduceContext)
    cut :: (Acyclic, Expression) -> IO (Either Expression ReduceContext)
cut (Acyclic, Expression)
loop = case Expression
form of
      ExFormation [Binding]
bds
        | [Binding] -> Bool
boxed [Binding]
bds Bool -> Bool -> Bool
|| ReduceContext
ctx._judgment Judgment -> [Judgment] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Judgment
Dataization, Judgment
Evaluation]
        , Just Expression
call <- Expression -> ReduceContext -> [Binding] -> Maybe Expression
called Expression
univ ReduceContext
ctx [Binding]
bds ->
            Expression -> Either Expression ReduceContext
forall a b. a -> Either a b
Left (Expression -> Either Expression ReduceContext)
-> IO Expression -> IO (Either Expression ReduceContext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression
-> ReduceContext
-> State
-> Expression
-> [Binding]
-> Expression
-> (Acyclic, Expression)
-> IO Expression
severed Expression
univ ReduceContext
ctx State
state Expression
form [Binding]
bds Expression
call (Acyclic, Expression)
loop
        | ReduceContext
ctx._judgment Judgment -> [Judgment] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Judgment
Dataization, Judgment
Evaluation] -> IO (Either Expression ReduceContext)
-> ((Expression, [Binding], Expression)
    -> IO (Either Expression ReduceContext))
-> Maybe (Expression, [Binding], Expression)
-> IO (Either Expression ReduceContext)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Expression
-> ReduceContext
-> (Acyclic, Expression)
-> IO (Either Expression ReduceContext)
forall a.
Expression -> ReduceContext -> (Acyclic, Expression) -> IO a
refused Expression
form ReduceContext
ctx (Acyclic, Expression)
loop) (\(Expression
copy, [Binding]
known, Expression
call) -> Expression -> Either Expression ReduceContext
forall a b. a -> Either a b
Left (Expression -> Either Expression ReduceContext)
-> IO Expression -> IO (Either Expression ReduceContext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression
-> ReduceContext
-> State
-> Expression
-> [Binding]
-> Expression
-> (Acyclic, Expression)
-> IO Expression
severed Expression
univ ReduceContext
ctx State
state Expression
copy [Binding]
known Expression
call (Acyclic, Expression)
loop) ReduceContext
ctx._placed
      Expression
_ -> Expression
-> ReduceContext
-> (Acyclic, Expression)
-> IO (Either Expression ReduceContext)
forall a.
Expression -> ReduceContext -> (Acyclic, Expression) -> IO a
refused Expression
form ReduceContext
ctx (Acyclic, Expression)
loop

severed :: Expression -> ReduceContext -> State -> Expression -> [Binding] -> Expression -> (Acyclic, Expression) -> IO Expression
severed :: Expression
-> ReduceContext
-> State
-> Expression
-> [Binding]
-> Expression
-> (Acyclic, Expression)
-> IO Expression
severed Expression
univ ReduceContext
ctx State
state Expression
form [Binding]
bds Expression
call (Acyclic
mode, Expression
before) = do
  Expression
reckoned <- Expression
-> ReduceContext
-> State
-> Expression
-> [Binding]
-> Expression
-> IO Expression
argued Expression
univ ReduceContext
ctx State
state Expression
form [Binding]
bds Expression
call
  Int
fresh <- ReduceContext -> IO Int
coined ReduceContext
ctx
  ReduceContext
ctx._saveEval (Int
-> Judgment
-> Acyclic
-> Expression
-> Expression
-> Maybe (Int, Expression)
-> Evaluation
EvLooped ReduceContext
ctx._nesting ReduceContext
ctx._judgment Acyclic
mode Expression
before ReduceContext
ctx._site ((Int, Expression) -> Maybe (Int, Expression)
forall a. a -> Maybe a
Just (Int
fresh, Expression
reckoned)))
  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)])

coined :: ReduceContext -> IO Int
coined :: ReduceContext -> IO Int
coined ReduceContext
ctx = IORef Int -> (Int -> (Int, Int)) -> IO Int
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' ReduceContext
ctx._minted (\Int
count -> (Int -> Int
forall a. Enum a => a -> a
succ Int
count, Int -> Int
forall a. Enum a => a -> a
succ Int
count))

fired :: Expression -> ReduceContext -> Expression -> State -> Expression -> IO (Expression, State)
fired :: Expression
-> ReduceContext
-> Expression
-> State
-> Expression
-> IO (Expression, State)
fired Expression
univ ReduceContext
ctx Expression
site State
state Expression
form = Expression
-> Expression
-> State
-> ReduceContext
-> IO (Either Expression ReduceContext)
sever Expression
form Expression
univ State
state ReduceContext
ctx{_judgment = Evaluation, _site = site} IO (Either Expression ReduceContext)
-> (Either Expression ReduceContext -> IO (Expression, State))
-> IO (Expression, State)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Expression -> IO (Expression, State))
-> (ReduceContext -> IO (Expression, State))
-> Either Expression ReduceContext
-> IO (Expression, State)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Expression, State) -> IO (Expression, State))
-> (Expression -> (Expression, State))
-> Expression
-> IO (Expression, State)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,State
state)) ReduceContext -> IO (Expression, State)
kindled
  where
    kindled :: ReduceContext -> IO (Expression, State)
    kindled :: ReduceContext -> IO (Expression, State)
kindled ReduceContext
entered = do
      ReduceContext
deep <- ReduceContext -> IO ReduceContext
deeper ReduceContext
entered
      ReduceContext
deep._evaluate ReduceContext
deep State
state Expression
form Expression
univ

called :: Expression -> ReduceContext -> [Binding] -> Maybe Expression
called :: Expression -> ReduceContext -> [Binding] -> Maybe Expression
called Expression
univ ReduceContext
ctx [Binding]
known = (Expression -> [Binding] -> Expression)
-> (Expression, [Binding]) -> Expression
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expression -> [Binding] -> Expression
applied ((Expression, [Binding]) -> Expression)
-> Maybe (Expression, [Binding]) -> Maybe Expression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression
-> ReduceContext -> [Binding] -> Maybe (Expression, [Binding])
origin Expression
univ ReduceContext
ctx [Binding]
known
  where
    applied :: Expression -> [Binding] -> Expression
    applied :: Expression -> [Binding] -> Expression
applied Expression
path [Binding]
declared = (Expression -> Argument -> Expression)
-> Expression -> [Argument] -> Expression
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expression -> Argument -> Expression
ExApplication Expression
path [Attribute -> Expression -> Argument
ArTau Attribute
attr Expression
value | BiTau Attribute
attr Expression
value <- [Binding]
known, Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute
AtRho, Attribute -> Binding
BiVoid Attribute
attr Binding -> [Binding] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Binding]
declared]

origin :: Expression -> ReduceContext -> [Binding] -> Maybe (Expression, [Binding])
origin :: Expression
-> ReduceContext -> [Binding] -> Maybe (Expression, [Binding])
origin Expression
univ ReduceContext
ctx [Binding]
bds = do
  Expression
parent <- 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
    [] -> Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
ExRoot
    [BiTau Attribute
AtRho (ExFormation [Binding]
outer)] -> (Expression, [Binding]) -> Expression
forall a b. (a, b) -> a
fst ((Expression, [Binding]) -> Expression)
-> Maybe (Expression, [Binding]) -> Maybe Expression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression
-> ReduceContext -> [Binding] -> Maybe (Expression, [Binding])
origin Expression
univ ReduceContext
ctx [Binding]
outer
    [BiTau Attribute
AtRho Expression
path] -> Expression -> Maybe Expression
forall a. a -> Maybe a
Just (Expression -> Expression
erased Expression
path)
    [Binding]
_ -> Maybe Expression
forall a. Maybe a
Nothing
  ExFormation [Binding]
siblings <- Expression -> Expression -> Maybe Expression
located Expression
parent (Expression -> Maybe Expression -> Expression
forall a. a -> Maybe a -> a
fromMaybe Expression
univ ReduceContext
ctx._universe)
  [(Expression, [Binding])] -> Maybe (Expression, [Binding])
chosen [(Expression -> Attribute -> Expression
ExDispatch Expression
parent Attribute
attr, [Binding]
declared) | BiTau Attribute
attr (ExFormation [Binding]
declared) <- [Binding]
siblings, Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute
AtRho, [Binding] -> Bool
fits [Binding]
declared]
  where
    fits :: [Binding] -> Bool
    fits :: [Binding] -> Bool
fits [Binding]
declared = (Maybe Attribute -> Bool) -> [Maybe Attribute] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe Attribute -> [Maybe Attribute] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Binding -> Maybe Attribute) -> [Binding] -> [Maybe Attribute]
forall a b. (a -> b) -> [a] -> [b]
map Binding -> Maybe Attribute
attributeFromBinding [Binding]
declared) [Binding -> Maybe Attribute
attributeFromBinding Binding
bd | Binding
bd <- [Binding]
bds, Binding -> Maybe Attribute
attributeFromBinding Binding
bd Maybe Attribute -> Maybe Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute -> Maybe Attribute
forall a. a -> Maybe a
Just Attribute
AtRho]
    chosen :: [(Expression, [Binding])] -> Maybe (Expression, [Binding])
    chosen :: [(Expression, [Binding])] -> Maybe (Expression, [Binding])
chosen [] = Maybe (Expression, [Binding])
forall a. Maybe a
Nothing
    chosen [(Expression, [Binding])]
candidates = case [(Expression, [Binding])
candidate | (Expression, [Binding])
candidate <- [(Expression, [Binding])]
candidates, (Expression, [Binding]) -> (Bool, Int, Int)
agreed (Expression, [Binding])
candidate (Bool, Int, Int) -> (Bool, Int, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== [(Bool, Int, Int)] -> (Bool, Int, Int)
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (((Expression, [Binding]) -> (Bool, Int, Int))
-> [(Expression, [Binding])] -> [(Bool, Int, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Expression, [Binding]) -> (Bool, Int, Int)
agreed [(Expression, [Binding])]
candidates)] of
      [(Expression, [Binding])
one] -> (Expression, [Binding]) -> Maybe (Expression, [Binding])
forall a. a -> Maybe a
Just (Expression, [Binding])
one
      [(Expression, [Binding])]
_ -> Maybe (Expression, [Binding])
forall a. Maybe a
Nothing
    agreed :: (Expression, [Binding]) -> (Bool, Int, Int)
    agreed :: (Expression, [Binding]) -> (Bool, Int, Int)
agreed (Expression
_, [Binding]
declared) = ((Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Binding -> [Binding] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Binding]
declared) [Binding]
own Bool -> Bool -> Bool
&& [Binding] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Binding]
own Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Binding] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Binding]
declared, [Attribute] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Attribute
attr | BiTau Attribute
attr Expression
_ <- [Binding]
bds, Attribute -> Binding
BiVoid Attribute
attr Binding -> [Binding] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Binding]
declared], [Binding] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Binding -> Bool) -> [Binding] -> [Binding]
forall a. (a -> Bool) -> [a] -> [a]
filter (Binding -> [Binding] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Binding]
declared) [Binding]
bds))
    own :: [Binding]
    own :: [Binding]
own = (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
    located :: Expression -> Expression -> Maybe Expression
    located :: Expression -> Expression -> Maybe Expression
located Expression
ExRoot Expression
whole = Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
whole
    located (ExDispatch Expression
path Attribute
attr) Expression
whole = case Expression -> Expression -> Maybe Expression
located Expression
path Expression
whole of
      Just (ExFormation [Binding]
siblings) -> [Expression] -> Maybe Expression
forall a. [a] -> Maybe a
listToMaybe [Expression
body | BiTau Attribute
attr' Expression
body <- [Binding]
siblings, Attribute
attr' Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
attr]
      Maybe Expression
_ -> Maybe Expression
forall a. Maybe a
Nothing
    located Expression
_ Expression
_ = Maybe Expression
forall a. Maybe a
Nothing
    erased :: Expression -> Expression
    erased :: Expression -> Expression
erased (ExApplication Expression
target Argument
_) = Expression -> Expression
erased Expression
target
    erased (ExDispatch Expression
target Attribute
attr) = Expression -> Attribute -> Expression
ExDispatch (Expression -> Expression
erased Expression
target) Attribute
attr
    erased Expression
other = Expression
other

argued :: Expression -> ReduceContext -> State -> Expression -> [Binding] -> Expression -> IO Expression
argued :: Expression
-> ReduceContext
-> State
-> Expression
-> [Binding]
-> Expression
-> IO Expression
argued Expression
univ ReduceContext
ctx State
state Expression
site [Binding]
bds = Expression -> IO Expression
go
  where
    go :: Expression -> IO Expression
    go :: Expression -> IO Expression
go (ExApplication Expression
target (ArTau Attribute
attr Expression
body)) = do
      Expression
target' <- Expression -> IO Expression
go Expression
target
      Expression -> Argument -> Expression
ExApplication Expression
target' (Argument -> Expression)
-> (Expression -> Argument) -> Expression -> Expression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attribute -> Expression -> Argument
ArTau Attribute
attr (Expression -> Expression) -> IO Expression -> IO Expression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Attribute -> Expression -> IO Expression
reckoned Attribute
attr Expression
body
    go Expression
call = Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
call
    reckoned :: Attribute -> Expression -> IO Expression
    reckoned :: Attribute -> Expression -> IO Expression
reckoned Attribute
_ body :: Expression
body@(ExFormation [BiLambda (FnSymbol Int
_)]) = Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
body
    reckoned Attribute
attr 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))
      Expression -> Expression -> IO Expression
figured (Expression -> Attribute -> Expression
ExDispatch Expression
site Attribute
attr) Expression
placed
    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
    figured :: Expression -> Expression -> IO Expression
    figured :: Expression -> Expression -> IO Expression
figured Expression
place Expression
placed = IO Expression -> IO Expression
forall a. IO a -> IO a
unparked (IO Expression -> IO Expression) -> IO Expression -> IO Expression
forall a b. (a -> b) -> a -> b
$ do
      (Expression
normal, State
morphed) <- Expression
-> Expression -> State -> ReduceContext -> IO (Expression, State)
settled Expression
placed 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{_site = place}
      case Expression
normal of
        ExFormation [Binding]
_ -> (Expression, State) -> Expression
forall a b. (a, b) -> a
fst ((Expression, State) -> Expression)
-> IO (Expression, State) -> IO Expression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression
-> ReduceContext
-> Expression
-> State
-> Expression
-> IO (Expression, State)
fired Expression
univ ReduceContext
ctx Expression
place State
morphed Expression
normal
        Expression
_ -> Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
normal

admitted :: Expression -> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext)
admitted :: Expression
-> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext)
admitted Expression
form ReduceContext
ctx = IO (Either (Acyclic, Expression) ReduceContext)
-> (Acyclic -> IO (Either (Acyclic, Expression) ReduceContext))
-> Maybe Acyclic
-> IO (Either (Acyclic, Expression) ReduceContext)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Either (Acyclic, Expression) ReduceContext
-> IO (Either (Acyclic, Expression) ReduceContext)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ReduceContext -> Either (Acyclic, Expression) ReduceContext
forall a b. b -> Either a b
Right ReduceContext
ctx)) Acyclic -> IO (Either (Acyclic, Expression) ReduceContext)
remembered ReduceContext
ctx._acyclic
  where
    remembered :: Acyclic -> IO (Either (Acyclic, Expression) ReduceContext)
    remembered :: Acyclic -> IO (Either (Acyclic, Expression) ReduceContext)
remembered Acyclic
mode = Either (Acyclic, Expression) ReduceContext
-> (Expression -> Either (Acyclic, Expression) ReduceContext)
-> Maybe Expression
-> Either (Acyclic, Expression) ReduceContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ReduceContext -> Either (Acyclic, Expression) ReduceContext
forall a b. b -> Either a b
Right ReduceContext
ctx{_entered = seenInsert (digest mode form) form ctx._entered}) (\Expression
before -> (Acyclic, Expression) -> Either (Acyclic, Expression) ReduceContext
forall a b. a -> Either a b
Left (Acyclic
mode, Expression
before)) (Maybe Expression -> Either (Acyclic, Expression) ReduceContext)
-> ([Expression] -> Maybe Expression)
-> [Expression]
-> Either (Acyclic, Expression) ReduceContext
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expression] -> Maybe Expression
forall a. [a] -> Maybe a
listToMaybe ([Expression] -> Maybe Expression)
-> ([Expression] -> [Expression])
-> [Expression]
-> Maybe Expression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Expression] -> [Expression]
forall a. Int -> [a] -> [a]
drop ReduceContext
ctx._maxLoops ([Expression] -> Either (Acyclic, Expression) ReduceContext)
-> IO [Expression]
-> IO (Either (Acyclic, Expression) ReduceContext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Acyclic -> Expression -> ReduceContext -> IO [Expression]
repeats Acyclic
mode Expression
form ReduceContext
ctx

repeats :: Acyclic -> Expression -> ReduceContext -> IO [Expression]
repeats :: Acyclic -> Expression -> ReduceContext -> IO [Expression]
repeats Acyclic
mode Expression
form ReduceContext
ctx = ReduceContext -> IO [Expression] -> IO [Expression]
forall a. ReduceContext -> IO a -> IO a
awaited ReduceContext
ctx ([Expression] -> IO [Expression]
forall a. a -> IO a
evaluate ([Expression] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expression]
hits Int -> [Expression] -> [Expression]
forall a b. a -> b -> b
`seq` [Expression]
hits))
  where
    hits :: [Expression]
    hits :: [Expression]
hits = Int -> [Expression] -> [Expression]
forall a. Int -> [a] -> [a]
take (Int -> Int
forall a. Enum a => a -> a
succ ReduceContext
ctx._maxLoops) ((Expression -> Bool) -> [Expression] -> [Expression]
forall a. (a -> Bool) -> [a] -> [a]
filter (Acyclic -> Expression -> Bool
repeated Acyclic
mode) ([Expression] -> Int -> Seen -> [Expression]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] (Acyclic -> Expression -> Int
digest Acyclic
mode Expression
form) ReduceContext
ctx._entered))
    repeated :: Acyclic -> Expression -> Bool
    repeated :: Acyclic -> Expression -> Bool
repeated Acyclic
Proven Expression
before = Expression -> Expression -> Bool
alike Expression
form Expression
before
    repeated Acyclic
Plausible Expression
before = Expression -> Expression -> Bool
within Expression
before Expression
form

digest :: Acyclic -> Expression -> Int
digest :: Acyclic -> Expression -> Int
digest Acyclic
Proven = Expression -> Int
hashShape
digest Acyclic
Plausible = Expression -> Int
hashSkeleton

entrance :: Judgment -> Expression -> Maybe Expression
entrance :: Judgment -> Expression -> Maybe Expression
entrance Judgment
Dataization term :: Expression
term@(ExFormation [Binding]
bds)
  | [Binding] -> Bool
boxed [Binding]
bds Bool -> Bool -> Bool
|| Maybe (Text, Expression) -> Bool
forall a. Maybe a -> Bool
isJust ([Binding] -> Maybe (Text, Expression)
lambda [Binding]
bds) = Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
term
entrance Judgment
Morphing (ExDispatch form :: Expression
form@(ExFormation [Binding]
bds) Attribute
_)
  | Maybe (Text, Expression) -> Bool
forall a. Maybe a -> Bool
isJust ([Binding] -> Maybe (Text, Expression)
lambda [Binding]
bds) = Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
form
entrance Judgment
Evaluation term :: Expression
term@(ExFormation [Binding]
bds)
  | Maybe (Text, Expression) -> Bool
forall a. Maybe a -> Bool
isJust ([Binding] -> Maybe (Text, Expression)
lambda [Binding]
bds) = Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
term
entrance Judgment
_ Expression
_ = Maybe Expression
forall a. Maybe a
Nothing

boxed :: [Binding] -> Bool
boxed :: [Binding] -> Bool
boxed [Binding]
bds = (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Binding -> Bool
phi [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
isLambda [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
delta [Binding]
bds)
  where
    phi :: Binding -> Bool
    phi :: Binding -> Bool
phi (BiTau Attribute
AtPhi Expression
_) = Bool
True
    phi Binding
_ = Bool
False
    delta :: Binding -> Bool
    delta :: Binding -> Bool
delta (BiDelta Bytes
_) = Bool
True
    delta Binding
_ = Bool
False

lambda :: [Binding] -> Maybe (T.Text, Expression)
lambda :: [Binding] -> Maybe (Text, Expression)
lambda [Binding]
bds = case (Binding -> Bool) -> [Binding] -> ([Binding], [Binding])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Binding -> Bool
isLambda [Binding]
bds of
  ([BiLambda (Function Text
func)], [Binding]
rest) -> (Text, Expression) -> Maybe (Text, Expression)
forall a. a -> Maybe a
Just (Text
func, [Binding] -> Expression
ExFormation [Binding]
rest)
  ([Binding], [Binding])
_ -> Maybe (Text, Expression)
forall a. Maybe a
Nothing

isLambda :: Binding -> Bool
isLambda :: Binding -> Bool
isLambda (BiLambda Function
_) = Bool
True
isLambda Binding
_ = Bool
False

morph' :: Morphed -> Expression -> State -> ReduceContext -> IO (Morphed, State)
morph' :: Morphed
-> Expression -> State -> ReduceContext -> IO (Morphed, State)
morph' = Bool
-> Morphed
-> Expression
-> State
-> ReduceContext
-> IO (Morphed, State)
morph'' Bool
True

morph'' :: Bool -> Morphed -> Expression -> State -> ReduceContext -> IO (Morphed, State)
morph'' :: Bool
-> Morphed
-> Expression
-> State
-> ReduceContext
-> IO (Morphed, State)
morph'' Bool
owner Morphed
start Expression
univ State
state ReduceContext
entry = Morphed
-> Expression -> State -> ReduceContext -> IO (Morphed, State)
go Morphed
start Expression
univ State
state ReduceContext
entry
  where
    go :: Morphed -> Expression -> State -> ReduceContext -> IO (Morphed, State)
    go :: Morphed
-> Expression -> State -> ReduceContext -> IO (Morphed, State)
go (Expression
expr, NonEmpty Rewritten
seq) Expression
univ State
state ReduceContext
caller = do
      ReduceContext
ctx <- Judgment -> ReduceContext -> IO ReduceContext
opening Judgment
Morphing (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 -> IO ReduceContext)
-> IO ReduceContext -> IO ReduceContext
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expression -> ReduceContext -> IO ReduceContext
entering Expression
expr (ReduceContext -> IO ReduceContext)
-> IO ReduceContext -> IO 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
caller{_judgment = Morphing})
      NonEmpty Rewritten
-> State -> IO (Morphed, State) -> IO (Morphed, State)
forall a. NonEmpty Rewritten -> State -> IO a -> IO a
parking NonEmpty Rewritten
seq State
state (IO (Morphed, State) -> IO (Morphed, State))
-> IO (Morphed, State) -> IO (Morphed, State)
forall a b. (a -> b) -> a -> b
$ do
        Maybe (Conclusion Expression, State)
reached <- Expression
-> Expression
-> State
-> ReduceContext
-> [Inference Expression]
-> IO (Maybe (Conclusion Expression, 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._morphing
        case Maybe (Conclusion Expression, State)
reached of
          Just (In.Answered (Judgment, String)
step Expression
built, State
state') -> do
            Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
owner (ReduceContext
ctx._saveEval (Int -> Expression -> Evaluation
EvMorphed ReduceContext
ctx._nesting Expression
built))
            NonEmpty Rewritten
seq' <- NonEmpty Rewritten
-> (Judgment, String)
-> Expression
-> ReduceContext
-> IO (NonEmpty Rewritten)
leadsTo NonEmpty Rewritten
seq (Judgment, String)
step Expression
built ReduceContext
ctx
            (Morphed, State) -> IO (Morphed, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Expression
built, NonEmpty Rewritten
seq'), State
state')
          Just (In.Onward Way
way Expression
built Expression
world, State
state') -> do
            (Morphed
morphed, State
state'') <- NonEmpty Rewritten
-> State
-> Way
-> Expression
-> ReduceContext
-> IO (Morphed, State)
onward NonEmpty Rewritten
seq State
state' Way
way Expression
built ReduceContext
ctx
            Morphed
-> Expression -> State -> ReduceContext -> IO (Morphed, State)
go Morphed
morphed Expression
world State
state'' ReduceContext
ctx
          Maybe (Conclusion Expression, State)
Nothing -> ReduceException -> IO (Morphed, State)
forall e a. Exception e => e -> IO a
throwIO (Expression -> ReduceException
Unmorphable Expression
expr)

morph :: Expression -> State -> ReduceContext -> IO (Expression, [Rewritten], State)
morph :: Expression
-> State -> ReduceContext -> IO (Expression, [Rewritten], State)
morph Expression
universe State
state caller :: ReduceContext
caller@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 ()
ReduceContext
-> State -> Expression -> Expression -> IO (Expression, State)
$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
-> ReduceContext
-> State
-> Expression
-> Expression
-> IO (Expression, State)
$sel:_saveStep:ReduceContext :: ReduceContext -> SaveStepFunc
$sel:_saveEval:ReduceContext :: ReduceContext -> Evaluation -> IO ()
$sel:_engine:ReduceContext :: ReduceContext -> Engine
_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 :: ReduceContext
-> State -> Expression -> Expression -> IO (Expression, State)
_saveStep :: SaveStepFunc
_saveEval :: Evaluation -> IO ()
_engine :: Engine
..} = do
  Expression
expr <- Expression -> Expression -> IO Expression
locatedExpression Expression
_locator Expression
universe
  Either ReduceException ReduceContext
prepared <- IO ReduceContext -> IO (Either ReduceException ReduceContext)
forall e a. Exception e => IO a -> IO (Either e a)
try (Expression -> ReduceContext -> IO ReduceContext
universed Expression
universe ReduceContext
caller)
  case Either ReduceException ReduceContext
prepared of
    Left (OutOfSteps Budget
_) | Bool
_partial -> (Expression, [Rewritten], State)
-> IO (Expression, [Rewritten], State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
expr, [(Expression
universe, Maybe (Judgment, String)
forall a. Maybe a
Nothing)], State
state)
    Left ReduceException
failure -> ReduceException -> IO (Expression, [Rewritten], State)
forall e a. Exception e => e -> IO a
throwIO (ReduceException
failure :: ReduceException)
    Right ReduceContext
univCtx -> Expression -> ReduceContext -> IO (Expression, [Rewritten], State)
reduced Expression
expr (ReduceContext -> IO (Expression, [Rewritten], State))
-> IO ReduceContext -> IO (Expression, [Rewritten], State)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Judgment -> ReduceContext -> IO ReduceContext
opening Judgment
Morphing ReduceContext
univCtx
  where
    reduced :: Expression -> ReduceContext -> IO (Expression, [Rewritten], State)
    reduced :: Expression -> ReduceContext -> IO (Expression, [Rewritten], State)
reduced Expression
expr ReduceContext
ctx = do
      Either ReduceException (Morphed, State)
result <- IO (Morphed, State) -> IO (Either ReduceException (Morphed, State))
forall e a. Exception e => IO a -> IO (Either e a)
try (Morphed
-> Expression -> State -> ReduceContext -> IO (Morphed, State)
morph' (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 (Morphed, State)
result of
        Right ((Expression
morphed, NonEmpty Rewritten
seq), State
state') -> (Expression, [Rewritten], State)
-> IO (Expression, [Rewritten], State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
morphed, [Rewritten] -> [Rewritten]
forall a. [a] -> [a]
reverse (NonEmpty Rewritten -> [Rewritten]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty Rewritten
seq), State
state')
        Left (StuckAt Text
func NonEmpty Rewritten
seq State
parked) | Bool
_partial -> NonEmpty Rewritten -> State -> IO (Expression, [Rewritten], State)
residue NonEmpty Rewritten
seq State
parked{_stuck = Just func}
        Left (OutOfStepsAt Budget
_ NonEmpty Rewritten
seq State
parked) | Bool
_partial -> NonEmpty Rewritten -> State -> IO (Expression, [Rewritten], State)
residue NonEmpty Rewritten
seq State
parked
        Left (LoopingAt Expression
_ NonEmpty Rewritten
seq State
parked) -> NonEmpty Rewritten -> State -> IO (Expression, [Rewritten], State)
residue NonEmpty Rewritten
seq State
parked
        Left ReduceException
failure -> ReduceException -> IO (Expression, [Rewritten], State)
forall e a. Exception e => e -> IO a
throwIO (ReduceException
failure :: ReduceException)
    residue :: NonEmpty Rewritten -> State -> IO (Expression, [Rewritten], State)
    residue :: NonEmpty Rewritten -> State -> IO (Expression, [Rewritten], State)
residue NonEmpty Rewritten
seq State
parked = do
      Expression
expr <- 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))
      (Expression, [Rewritten], State)
-> IO (Expression, [Rewritten], State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
expr, [Rewritten] -> [Rewritten]
forall a. [a] -> [a]
reverse (NonEmpty Rewritten -> [Rewritten]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty Rewritten
seq), State
parked)

inferred :: Expression -> Expression -> State -> ReduceContext -> [In.Inference value] -> IO (Maybe (In.Conclusion value, State))
inferred :: forall value.
Expression
-> Expression
-> State
-> ReduceContext
-> [Inference value]
-> IO (Maybe (Conclusion value, State))
inferred Expression
expr Expression
univ State
state ReduceContext
ctx [Inference value]
rules = do
  [Inference value]
ordered <- if ReduceContext
ctx._shuffle then [Inference value] -> IO [Inference value]
forall a. [a] -> IO [a]
shuffle [Inference value]
rules else [Inference value] -> IO [Inference value]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Inference value]
rules
  Maybe (Premises value)
matched <- [Inference value] -> IO (Maybe (Premises value))
forall value. [Inference value] -> IO (Maybe (Premises value))
go [Inference value]
ordered
  (Premises value -> IO (Conclusion value, State))
-> Maybe (Premises value) -> IO (Maybe (Conclusion value, State))
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 (State -> Premises value -> IO (Conclusion value, State)
forall value.
State -> Premises value -> IO (Conclusion value, State)
premised State
state) Maybe (Premises value)
matched
  where
    go :: [In.Inference value] -> IO (Maybe (In.Premises value))
    go :: forall value. [Inference value] -> IO (Maybe (Premises value))
go [] = Maybe (Premises value) -> IO (Maybe (Premises value))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Premises value)
forall a. Maybe a
Nothing
    go (Inference value
rule : [Inference value]
rest) = Inference value
rule (BuildTermFunc
-> Maybe Expression -> (Expression -> Bool) -> RuleContext
RuleContext (Expression -> ReduceContext -> BuildTermFunc
execBuildTerm Expression
univ ReduceContext
ctx) (Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
univ) ReduceContext
ctx._engine._normal) Expression
expr Expression
univ IO (Maybe (Premises value))
-> (Maybe (Premises value) -> IO (Maybe (Premises value)))
-> IO (Maybe (Premises value))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO (Maybe (Premises value))
-> (Premises value -> IO (Maybe (Premises value)))
-> Maybe (Premises value)
-> IO (Maybe (Premises value))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Inference value] -> IO (Maybe (Premises value))
forall value. [Inference value] -> IO (Maybe (Premises value))
go [Inference value]
rest) (Maybe (Premises value) -> IO (Maybe (Premises value))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Premises value) -> IO (Maybe (Premises value)))
-> (Premises value -> Maybe (Premises value))
-> Premises value
-> IO (Maybe (Premises value))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Premises value -> Maybe (Premises value)
forall a. a -> Maybe a
Just)
    premised :: State -> In.Premises value -> IO (In.Conclusion value, State)
    premised :: forall value.
State -> Premises value -> IO (Conclusion value, State)
premised State
state' (In.Concludes Conclusion value
conclusion) = (Conclusion value, State) -> IO (Conclusion value, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Conclusion value
conclusion, State
state')
    premised State
state' (In.Morphs Expression
term Expression
world Expression -> IO (Premises value)
next) = do
      (Expression
morphed, State
state'') <- Expression
-> Expression -> State -> ReduceContext -> IO (Expression, State)
detached Expression
term Expression
world State
state' ReduceContext
ctx
      Expression -> IO (Premises value)
next Expression
morphed IO (Premises value)
-> (Premises value -> IO (Conclusion value, State))
-> IO (Conclusion value, State)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= State -> Premises value -> IO (Conclusion value, State)
forall value.
State -> Premises value -> IO (Conclusion value, State)
premised State
state''
    premised State
state' (In.Evaluates Expression
form Expression
world Expression -> IO (Premises value)
next) = do
      (Expression
answer, State
state'') <- ReduceContext
ctx._evaluate ReduceContext
ctx State
state' Expression
form Expression
world
      Expression -> IO (Premises value)
next Expression
answer IO (Premises value)
-> (Premises value -> IO (Conclusion value, State))
-> IO (Conclusion value, State)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= State -> Premises value -> IO (Conclusion value, State)
forall value.
State -> Premises value -> IO (Conclusion value, State)
premised State
state''
    premised State
state' (In.Contextualizes Expression
term Expression
context Expression -> IO (Premises value)
next) = ReduceContext
ctx._engine._contextualize Expression
term Expression
context IO Expression
-> (Expression -> IO (Premises value)) -> IO (Premises value)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expression -> IO (Premises value)
next IO (Premises value)
-> (Premises value -> IO (Conclusion value, State))
-> IO (Conclusion value, State)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= State -> Premises value -> IO (Conclusion value, State)
forall value.
State -> Premises value -> IO (Conclusion value, State)
premised State
state'

onward :: NonEmpty Rewritten -> State -> In.Way -> Expression -> ReduceContext -> IO (Morphed, State)
onward :: NonEmpty Rewritten
-> State
-> Way
-> Expression
-> ReduceContext
-> IO (Morphed, State)
onward NonEmpty Rewritten
seq State
state (In.Taken (Judgment, String)
step) Expression
expr ReduceContext
ctx = do
  NonEmpty Rewritten
seq' <- NonEmpty Rewritten
-> (Judgment, String)
-> Expression
-> ReduceContext
-> IO (NonEmpty Rewritten)
leadsTo NonEmpty Rewritten
seq (Judgment, String)
step Expression
expr ReduceContext
ctx
  (Morphed, State) -> IO (Morphed, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Expression
expr, NonEmpty Rewritten
seq'), State
state)
onward NonEmpty Rewritten
seq State
state (In.Normalized (Judgment, String)
step) Expression
expr ReduceContext
ctx = do
  NonEmpty Rewritten
labelled <- NonEmpty Rewritten
-> (Judgment, String)
-> Expression
-> ReduceContext
-> IO (NonEmpty Rewritten)
leadsTo NonEmpty Rewritten
seq (Judgment, String)
step Expression
expr ReduceContext
ctx
  Morphed
normal <- Expression -> NonEmpty Rewritten -> ReduceContext -> IO Morphed
normalized Expression
expr NonEmpty Rewritten
labelled ReduceContext
ctx
  (Morphed, State) -> IO (Morphed, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Morphed
normal, State
state)
onward NonEmpty Rewritten
seq State
state (In.Named (Judgment, String)
step) Expression
expr ReduceContext
ctx = case ReduceContext
ctx._universe of
  Just Expression
world -> NonEmpty Rewritten
-> State
-> Way
-> Expression
-> ReduceContext
-> IO (Morphed, State)
onward NonEmpty Rewritten
seq State
state ((Judgment, String) -> Way
In.Taken (Judgment, String)
step) Expression
world ReduceContext
ctx
  Maybe Expression
Nothing -> NonEmpty Rewritten
-> State
-> Way
-> Expression
-> ReduceContext
-> IO (Morphed, State)
onward NonEmpty Rewritten
seq State
state ((Judgment, String) -> Way
In.Normalized (Judgment, String)
step) Expression
expr ReduceContext
ctx
onward NonEmpty Rewritten
seq State
state (In.Staged Expression
stage) Expression
expr ReduceContext
ctx = Morphed
-> Expression -> State -> ReduceContext -> IO (Morphed, State)
morph' (Expression
expr, NonEmpty Rewritten
seq) Expression
stage State
state ReduceContext
ctx

leadsTo :: NonEmpty Rewritten -> (Judgment, String) -> Expression -> ReduceContext -> IO (NonEmpty Rewritten)
leadsTo :: NonEmpty Rewritten
-> (Judgment, String)
-> Expression
-> ReduceContext
-> IO (NonEmpty Rewritten)
leadsTo ((Expression
current, Maybe (Judgment, String)
_) :| [Rewritten]
rest) (Judgment, String)
rule Expression
expr 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 ()
ReduceContext
-> State -> Expression -> Expression -> IO (Expression, State)
$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
-> ReduceContext
-> State
-> Expression
-> Expression
-> IO (Expression, State)
$sel:_saveStep:ReduceContext :: ReduceContext -> SaveStepFunc
$sel:_saveEval:ReduceContext :: ReduceContext -> Evaluation -> IO ()
$sel:_engine:ReduceContext :: ReduceContext -> Engine
_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 :: ReduceContext
-> State -> Expression -> Expression -> IO (Expression, State)
_saveStep :: SaveStepFunc
_saveEval :: Evaluation -> IO ()
_engine :: Engine
..} = do
  Expression
updated <- Expression -> Expression -> Expression -> IO Expression
withLocatedExpression Expression
_locator Expression
expr Expression
current
  NonEmpty Rewritten -> IO (NonEmpty Rewritten)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Expression
updated, Maybe (Judgment, String)
forall a. Maybe a
Nothing) Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| (Expression
current, (Judgment, String) -> Maybe (Judgment, String)
forall a. a -> Maybe a
Just (Judgment, String)
rule) Rewritten -> [Rewritten] -> [Rewritten]
forall a. a -> [a] -> [a]
: [Rewritten]
rest)

normalized :: Expression -> NonEmpty Rewritten -> ReduceContext -> IO (Expression, NonEmpty Rewritten)
normalized :: Expression -> NonEmpty Rewritten -> ReduceContext -> IO Morphed
normalized Expression
expr NonEmpty Rewritten
seq 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 ()
ReduceContext
-> State -> Expression -> Expression -> IO (Expression, State)
$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
-> ReduceContext
-> State
-> Expression
-> Expression
-> IO (Expression, State)
$sel:_saveStep:ReduceContext :: ReduceContext -> SaveStepFunc
$sel:_saveEval:ReduceContext :: ReduceContext -> Evaluation -> IO ()
$sel:_engine:ReduceContext :: ReduceContext -> Engine
_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 :: ReduceContext
-> State -> Expression -> Expression -> IO (Expression, State)
_saveStep :: SaveStepFunc
_saveEval :: Evaluation -> IO ()
_engine :: Engine
..} = do
  Expression
whole <- Expression -> Expression -> Expression -> IO Expression
withLocatedExpression Expression
_locator Expression
expr (Rewritten -> Expression
forall a b. (a, b) -> a
fst (NonEmpty Rewritten -> Rewritten
forall a. NonEmpty a -> a
NE.head NonEmpty Rewritten
seq))
  (NonEmpty Rewritten
rewrittens, Bool
exceeded) <- Expression
-> [Step] -> RewriteContext -> IO (NonEmpty Rewritten, Bool)
rewrite Expression
whole Engine
_engine._normalization (ReduceContext -> RewriteContext
rewriteContext ReduceContext
ctx)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exceeded (ReduceException -> IO ()
forall e a. Exception e => e -> IO a
throwIO (Budget -> ReduceException
OutOfSteps (Int -> Budget
Cycles Int
_maxCycles)))
  let (Rewritten
rw :| [Rewritten]
rws) = NonEmpty Rewritten -> NonEmpty Rewritten
forall a. NonEmpty a -> NonEmpty a
NE.reverse NonEmpty Rewritten
rewrittens
      seq' :: NonEmpty Rewritten
seq' = Rewritten
rw Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| [Rewritten]
rws [Rewritten] -> [Rewritten] -> [Rewritten]
forall a. Semigroup a => a -> a -> a
<> NonEmpty Rewritten -> [Rewritten]
forall a. NonEmpty a -> [a]
NE.tail NonEmpty Rewritten
seq
  Expression
expr' <- Expression -> Expression -> IO Expression
locatedExpression Expression
_locator (Rewritten -> Expression
forall a b. (a, b) -> a
fst Rewritten
rw)
  Morphed -> IO Morphed
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
expr', NonEmpty Rewritten
seq')
  where
    rewriteContext :: ReduceContext -> RewriteContext
    rewriteContext :: ReduceContext -> RewriteContext
rewriteContext 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 ()
ReduceContext
-> State -> Expression -> Expression -> IO (Expression, State)
$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
-> ReduceContext
-> State
-> Expression
-> Expression
-> IO (Expression, State)
$sel:_saveStep:ReduceContext :: ReduceContext -> SaveStepFunc
$sel:_saveEval:ReduceContext :: ReduceContext -> Evaluation -> IO ()
$sel:_engine:ReduceContext :: ReduceContext -> Engine
_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 :: ReduceContext
-> State -> Expression -> Expression -> IO (Expression, State)
_saveStep :: SaveStepFunc
_saveEval :: Evaluation -> IO ()
_engine :: Engine
..} =
      Expression
-> Int
-> Int
-> Bool
-> Maybe Expression
-> BuildTermFunc
-> (Expression -> Bool)
-> (Maybe Expression -> Expression -> Set Int)
-> Must
-> Maybe String
-> SaveStepFunc
-> SaveMadeFunc
-> RewriteContext
RewriteContext Expression
_locator Int
_maxDepth Int
_maxCycles Bool
_depthSensitive Maybe Expression
_universe BuildTermFunc
_buildTerm Engine
_engine._normal Engine
_engine._matching Must
MtDisabled Maybe String
forall a. Maybe a
Nothing SaveStepFunc
_saveStep (\Expression
redex Expression
object -> Evaluation -> IO ()
_saveEval (Int
-> Judgment -> Expression -> Expression -> Expression -> Evaluation
EvApplied Int
_nesting Judgment
_judgment (Maybe Expression -> Expression -> Expression
called Maybe Expression
_universe Expression
redex) Expression
object Expression
_site))
    called :: Maybe Expression -> Expression -> Expression
    called :: Maybe Expression -> Expression -> Expression
called Maybe Expression
universe (ExApplication Expression
head' Argument
arg) = Expression -> Argument -> Expression
ExApplication (Maybe Expression -> Expression -> Expression
nameIn Maybe Expression
universe Expression
head') Argument
arg
    called Maybe Expression
_ Expression
redex = Expression
redex

universed :: Expression -> ReduceContext -> IO ReduceContext
universed :: Expression -> ReduceContext -> IO ReduceContext
universed Expression
_ ctx :: ReduceContext
ctx@ReduceContext{$sel:_universe:ReduceContext :: ReduceContext -> Maybe Expression
_universe = Just Expression
_} = ReduceContext -> IO ReduceContext
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ReduceContext
ctx
universed Expression
univ ReduceContext
ctx = do
  (Expression
normal, NonEmpty Rewritten
_) <- Expression -> NonEmpty Rewritten -> ReduceContext -> IO Morphed
normalized Expression
univ ((Expression
univ, Maybe (Judgment, String)
forall a. Maybe a
Nothing) Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| []) ReduceContext
ctx{_locator = ExRoot, _saveStep = dontSaveStep}
  ReduceContext
ctx._saveEval (Expression -> Evaluation
EvWorld Expression
normal)
  ReduceContext -> IO ReduceContext
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ReduceContext
ctx{_universe = Just normal}

insideUniverse :: Expression -> Expression -> ReduceContext -> IO (Expression, ReduceContext)
insideUniverse :: Expression
-> Expression -> ReduceContext -> IO (Expression, ReduceContext)
insideUniverse Expression
expr Expression
univ ctx :: ReduceContext
ctx@ReduceContext{$sel:_buildTerm:ReduceContext :: ReduceContext -> BuildTermFunc
_buildTerm = BuildTermFunc
buildTerm} = case Expression
univ of
  ExFormation [Binding]
bds -> do
    (TeAttribute Attribute
attr) <- BuildTermFunc
buildTerm String
"random-tau" [] Subst
substEmpty
    let aiming :: ReduceContext
aiming = ReduceContext
ctx{_locator = ExDispatch ExRoot attr}
        synthetic :: Expression
synthetic = [Binding] -> Expression
ExFormation (Attribute -> Expression -> Binding
BiTau Attribute
attr Expression
expr Binding -> [Binding] -> [Binding]
forall a. a -> [a] -> [a]
: [Binding]
bds)
    (Expression
normal, NonEmpty Rewritten
_) <- Expression -> NonEmpty Rewritten -> ReduceContext -> IO Morphed
normalized Expression
expr ((Expression
synthetic, Maybe (Judgment, String)
forall a. Maybe a
Nothing) Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| []) ReduceContext
aiming
    (Expression, ReduceContext) -> IO (Expression, ReduceContext)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Binding] -> Expression
ExFormation (Attribute -> Expression -> Binding
BiTau Attribute
attr Expression
normal Binding -> [Binding] -> [Binding]
forall a. a -> [a] -> [a]
: [Binding]
bds), ReduceContext
aiming{_universe = extended attr normal})
  Expression
_ -> IOError -> IO (Expression, ReduceContext)
forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError String
"Can't reduce an expression inside a universe which is not a formation")
  where
    extended :: Attribute -> Expression -> Maybe Expression
    extended :: Attribute -> Expression -> Maybe Expression
extended Attribute
attr Expression
normal = case ReduceContext
ctx._universe of
      Just (ExFormation [Binding]
bds) -> Expression -> Maybe Expression
forall a. a -> Maybe a
Just ([Binding] -> Expression
ExFormation (Attribute -> Expression -> Binding
BiTau Attribute
attr Expression
normal Binding -> [Binding] -> [Binding]
forall a. a -> [a] -> [a]
: [Binding]
bds))
      Maybe Expression
_ -> Maybe Expression
forall a. Maybe a
Nothing

opening :: Judgment -> ReduceContext -> IO ReduceContext
opening :: Judgment -> ReduceContext -> IO ReduceContext
opening Judgment
judgment ReduceContext
ctx
  | ReduceContext
ctx._opened Maybe (Int, Judgment, Expression)
-> Maybe (Int, Judgment, Expression) -> Bool
forall a. Eq a => a -> a -> Bool
== (Int, Judgment, Expression) -> Maybe (Int, Judgment, Expression)
forall a. a -> Maybe a
Just (ReduceContext
ctx._nesting, Judgment
judgment, ReduceContext
ctx._site) = ReduceContext -> IO ReduceContext
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ReduceContext
ctx{_judgment = judgment}
  | Bool
otherwise = do
      ReduceContext
ctx._saveEval (Int -> Judgment -> Expression -> Evaluation
EvStarted ReduceContext
ctx._nesting Judgment
judgment ReduceContext
ctx._site)
      ReduceContext -> IO ReduceContext
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ReduceContext
ctx{_judgment = judgment, _nesting = ctx._nesting + 1, _opened = Just (ctx._nesting + 1, judgment, ctx._site)}

settled :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)
settled :: Expression
-> Expression -> State -> ReduceContext -> IO (Expression, State)
settled Expression
term Expression
univ State
state ReduceContext
ctx = do
  (Expression
normal, NonEmpty Rewritten
_) <- Expression -> NonEmpty Rewritten -> ReduceContext -> IO Morphed
normalized Expression
term ((Expression
univ, Maybe (Judgment, String)
forall a. Maybe a
Nothing) Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| []) ReduceContext
ctx
  ((Expression
morphed, NonEmpty Rewritten
_), State
state') <- Morphed
-> Expression -> State -> ReduceContext -> IO (Morphed, State)
morph' (Expression
normal, (Expression
univ, Maybe (Judgment, String)
forall a. Maybe a
Nothing) Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| []) Expression
univ State
state ReduceContext
ctx
  (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
morphed, State
state')

morphing :: Expression -> ReduceContext -> Expression -> State -> IO (Expression, State)
morphing :: Expression
-> ReduceContext -> Expression -> State -> IO (Expression, State)
morphing 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
  Expression
normal <- Expression -> Expression -> IO Expression
locatedExpression ReduceContext
aiming._locator Expression
universe
  IO (Expression, State) -> IO (Expression, State)
forall a. IO a -> IO a
unparked (IO (Expression, State) -> IO (Expression, State))
-> IO (Expression, State) -> IO (Expression, State)
forall a b. (a -> b) -> a -> b
$ do
    ReduceContext
opened <- Judgment -> ReduceContext -> IO ReduceContext
opening Judgment
Morphing (ReduceContext -> IO ReduceContext)
-> IO ReduceContext -> IO ReduceContext
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expression -> ReduceContext -> IO ReduceContext
universed Expression
universe ReduceContext
aiming
    ((Expression
morphed, NonEmpty Rewritten
_), State
state') <- Morphed
-> Expression -> State -> ReduceContext -> IO (Morphed, State)
morph' (Expression
normal, (Expression
universe, Maybe (Judgment, String)
forall a. Maybe a
Nothing) Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| []) Expression
universe State
state{_copies = []} ReduceContext
opened
    Expression
-> Expression -> State -> ReduceContext -> IO (Expression, State)
recurring Expression
morphed Expression
universe State
state'{_copies = state._copies ++ state'._copies} ReduceContext
opened
  where
    recurring :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)
    recurring :: Expression
-> Expression -> State -> ReduceContext -> IO (Expression, State)
recurring term :: Expression
term@(ExFormation [Binding]
bds) Expression
world State
state' ReduceContext
opened
      | Just Acyclic
mode <- ReduceContext
opened._acyclic
      , [Binding] -> Bool
boxed [Binding]
bds
      , Just Expression
call <- Expression -> ReduceContext -> [Binding] -> Maybe Expression
called Expression
world ReduceContext
opened [Binding]
bds = do
          [Expression]
hits <- Acyclic -> Expression -> ReduceContext -> IO [Expression]
repeats Acyclic
mode Expression
term ReduceContext
opened
          case Int -> [Expression] -> [Expression]
forall a. Int -> [a] -> [a]
drop ReduceContext
opened._maxLoops [Expression]
hits of
            Expression
before : [Expression]
_ -> (,State
state') (Expression -> (Expression, State))
-> IO Expression -> IO (Expression, State)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression
-> ReduceContext
-> State
-> Expression
-> [Binding]
-> Expression
-> (Acyclic, Expression)
-> IO Expression
severed Expression
world ReduceContext
opened State
state' Expression
term [Binding]
bds Expression
call (Acyclic
mode, Expression
before)
            []
              | [Expression] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expression]
hits -> (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
term, State
state')
              | Bool
otherwise -> (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
term, State
state'{_copies = state'._copies ++ [term]})
    recurring Expression
term Expression
_ State
state' ReduceContext
_ = (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
term, State
state')

carried :: State -> ReduceContext -> (State, ReduceContext)
carried :: State -> ReduceContext -> (State, ReduceContext)
carried State
state ReduceContext
ctx = (State
state{_copies = []}, ReduceContext
-> (Acyclic -> ReduceContext) -> Maybe Acyclic -> ReduceContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReduceContext
ctx (\Acyclic
mode -> ReduceContext
ctx{_entered = foldr (\Expression
form -> Int -> Expression -> Seen -> Seen
seenInsert (Acyclic -> Expression -> Int
digest Acyclic
mode Expression
form) Expression
form) ctx._entered state._copies}) ReduceContext
ctx._acyclic)

execBuildTerm :: Expression -> ReduceContext -> BuildTermFunc
execBuildTerm :: Expression -> ReduceContext -> BuildTermFunc
execBuildTerm Expression
_ ReduceContext
ctx String
"evaluate" = ReduceContext -> BuildTermMethod
evaluated ReduceContext
ctx
execBuildTerm Expression
univ ReduceContext
ctx String
"morph" = Expression -> ReduceContext -> BuildTermMethod
_morph Expression
univ ReduceContext
ctx
execBuildTerm Expression
_ ReduceContext
ctx String
func = ReduceContext -> BuildTermFunc
_buildTerm ReduceContext
ctx String
func

evaluated :: ReduceContext -> BuildTermMethod
evaluated :: ReduceContext -> BuildTermMethod
evaluated ReduceContext
ctx [ArgExpression Expression
expr, ArgExpression Expression
universe] Subst
subst = do
  Expression
form <- Expression -> Subst -> IO Expression
buildExpressionThrows Expression
expr Subst
subst
  Expression
world <- Expression -> Subst -> IO Expression
buildExpressionThrows Expression
universe Subst
subst
  Expression -> Term
TeExpression (Expression -> Term)
-> ((Expression, State) -> Expression)
-> (Expression, State)
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expression, State) -> Expression
forall a b. (a, b) -> a
fst ((Expression, State) -> Term) -> IO (Expression, State) -> IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceContext
ctx._evaluate ReduceContext
ctx State
emptyState Expression
form Expression
world
evaluated ReduceContext
_ [ExtraArgument]
_ Subst
_ = IOError -> IO Term
forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError String
"Function evaluate() requires exactly 2 expression arguments")

_morph :: Expression -> ReduceContext -> BuildTermMethod
_morph :: Expression -> ReduceContext -> BuildTermMethod
_morph Expression
univ ReduceContext
ctx [ArgExpression Expression
expr] Subst
subst = do
  Expression
built <- Expression -> Subst -> IO Expression
buildExpressionThrows Expression
expr Subst
subst
  Expression -> Term
TeExpression (Expression -> Term)
-> ((Expression, State) -> Expression)
-> (Expression, State)
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expression, State) -> Expression
forall a b. (a, b) -> a
fst ((Expression, State) -> Term) -> IO (Expression, State) -> IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression
-> Expression -> State -> ReduceContext -> IO (Expression, State)
detached Expression
built Expression
univ State
emptyState ReduceContext
ctx
_morph Expression
_ ReduceContext
_ [ExtraArgument]
_ Subst
_ = IOError -> IO Term
forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError String
"Function morph() requires exactly 1 expression argument")

detached :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)
detached :: Expression
-> Expression -> State -> ReduceContext -> IO (Expression, State)
detached Expression
expr Expression
univ State
state ReduceContext
ctx = IO (Expression, State) -> IO (Expression, State)
forall a. IO a -> IO a
unparked (IO (Expression, State) -> IO (Expression, State))
-> IO (Expression, State) -> IO (Expression, State)
forall a b. (a -> b) -> a -> b
$ do
  ((Expression
morphed, NonEmpty Rewritten
_), State
state') <- Bool
-> Morphed
-> Expression
-> State
-> ReduceContext
-> IO (Morphed, State)
morph'' (ReduceContext
ctx._judgment Judgment -> Judgment -> Bool
forall a. Eq a => a -> a -> Bool
/= Judgment
Morphing) (Expression
expr, (Expression
univ, Maybe (Judgment, String)
forall a. Maybe a
Nothing) Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| []) Expression
univ State
state ReduceContext
ctx
  (Expression, State) -> IO (Expression, State)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
morphed, State
state')