{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}

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

module Deps where

import AST
import Bytes (btsSize, btsToNum)
import Control.Monad (foldM, guard, unless, when, zipWithM, (>=>))
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State.Strict (StateT, get, modify, put, runStateT)
import Data.Bifunctor (bimap, first, second)
import Data.Char (isAlphaNum)
import Data.Either (lefts, rights)
import Data.IORef (IORef, readIORef, writeIORef)
import Data.List (intercalate, sortOn)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe, listToMaybe, mapMaybe, maybeToList)
import qualified Data.Text as T
import Data.Time (ZonedTime, defaultTimeLocale, formatTime)
import Files (overwrite)
import Forks (Refusal (..), Side (..))
import GHC.Clock (getMonotonicTime)
import Logger (logDebug, logInfo)
import Matcher
import Printer (printAlpha, printAttribute, printBinding, printFunction)
import System.Directory (createDirectoryIfMissing)
import System.FilePath
import System.IO (Handle, hPutStrLn)
import Text.Printf (printf)
import XMIR (escapeXML, escapeXMLText)
import Yaml (ExtraArgument)

data Term
  = TeExpression Expression
  | TeAttribute Attribute
  | TeBytes Bytes
  | TeBindings [Binding]

type BuildTermMethod = [ExtraArgument] -> Subst -> IO Term

data State = State
  { State -> Maybe Int
_manufactured :: Maybe Int
  , State -> Maybe Text
_stuck :: Maybe T.Text
  , State -> [Expression]
_copies :: [Expression]
  }

type BuildTermMethodS = [ExtraArgument] -> Subst -> IO (Term, State)

type BuildTermFunc = String -> BuildTermMethod

type SaveStepFunc = Expression -> IO ()

saveStep :: Maybe FilePath -> String -> (Expression -> IO String) -> Int -> SaveStepFunc
saveStep :: Maybe String
-> String -> (Expression -> IO String) -> Int -> SaveStepFunc
saveStep Maybe String
Nothing String
_ Expression -> IO String
_ Int
_ Expression
_ = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
saveStep (Just String
dir) String
ext Expression -> IO String
render Int
step Expression
expr = do
  Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
dir
  let path :: String
path = String
dir String -> String -> String
</> String -> Int -> String -> String
forall r. PrintfType r => String -> r
printf String
"%05d.%s" Int
step String
ext
  String
content <- Expression -> IO String
render Expression
expr
  String -> String -> IO ()
overwrite String
path String
content
  String -> IO ()
logDebug (String -> Int -> String -> String
forall r. PrintfType r => String -> r
printf String
"Saved step '%d' to '%s'" Int
step String
path)

dontSaveStep :: SaveStepFunc
dontSaveStep :: SaveStepFunc
dontSaveStep = Maybe String
-> String -> (Expression -> IO String) -> Int -> SaveStepFunc
saveStep Maybe String
forall a. Maybe a
Nothing String
"" (\Expression
_ -> String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"") Int
0

type SaveMadeFunc = Expression -> Expression -> IO ()

dontSaveMade :: SaveMadeFunc
dontSaveMade :: SaveMadeFunc
dontSaveMade Expression
_ Expression
_ = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

data Judgment
  = Normalization
  | Morphing
  | Dataization
  | Evaluation
  | Contextualization
  deriving (Judgment -> Judgment -> Bool
(Judgment -> Judgment -> Bool)
-> (Judgment -> Judgment -> Bool) -> Eq Judgment
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Judgment -> Judgment -> Bool
== :: Judgment -> Judgment -> Bool
$c/= :: Judgment -> Judgment -> Bool
/= :: Judgment -> Judgment -> Bool
Eq, Int -> Judgment -> String -> String
[Judgment] -> String -> String
Judgment -> String
(Int -> Judgment -> String -> String)
-> (Judgment -> String)
-> ([Judgment] -> String -> String)
-> Show Judgment
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Judgment -> String -> String
showsPrec :: Int -> Judgment -> String -> String
$cshow :: Judgment -> String
show :: Judgment -> String
$cshowList :: [Judgment] -> String -> String
showList :: [Judgment] -> String -> String
Show)

letter :: Judgment -> String
letter :: Judgment -> String
letter Judgment
Normalization = String
"𝒩"
letter Judgment
Morphing = String
"𝕄"
letter Judgment
Dataization = String
"𝔻"
letter Judgment
Evaluation = String
"𝔼"
letter Judgment
Contextualization = String
"𝒞"

opened :: Judgment -> String
opened :: Judgment -> String
opened Judgment
Normalization = String
"normalize"
opened Judgment
Morphing = String
"morph"
opened Judgment
Dataization = String
"dataize"
opened Judgment
Evaluation = String
"evaluate"
opened Judgment
Contextualization = String
"contextualize"

data Acyclic
  = Proven
  | Plausible
  deriving (Acyclic
Acyclic -> Acyclic -> Bounded Acyclic
forall a. a -> a -> Bounded a
$cminBound :: Acyclic
minBound :: Acyclic
$cmaxBound :: Acyclic
maxBound :: Acyclic
Bounded, Int -> Acyclic
Acyclic -> Int
Acyclic -> [Acyclic]
Acyclic -> Acyclic
Acyclic -> Acyclic -> [Acyclic]
Acyclic -> Acyclic -> Acyclic -> [Acyclic]
(Acyclic -> Acyclic)
-> (Acyclic -> Acyclic)
-> (Int -> Acyclic)
-> (Acyclic -> Int)
-> (Acyclic -> [Acyclic])
-> (Acyclic -> Acyclic -> [Acyclic])
-> (Acyclic -> Acyclic -> [Acyclic])
-> (Acyclic -> Acyclic -> Acyclic -> [Acyclic])
-> Enum Acyclic
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Acyclic -> Acyclic
succ :: Acyclic -> Acyclic
$cpred :: Acyclic -> Acyclic
pred :: Acyclic -> Acyclic
$ctoEnum :: Int -> Acyclic
toEnum :: Int -> Acyclic
$cfromEnum :: Acyclic -> Int
fromEnum :: Acyclic -> Int
$cenumFrom :: Acyclic -> [Acyclic]
enumFrom :: Acyclic -> [Acyclic]
$cenumFromThen :: Acyclic -> Acyclic -> [Acyclic]
enumFromThen :: Acyclic -> Acyclic -> [Acyclic]
$cenumFromTo :: Acyclic -> Acyclic -> [Acyclic]
enumFromTo :: Acyclic -> Acyclic -> [Acyclic]
$cenumFromThenTo :: Acyclic -> Acyclic -> Acyclic -> [Acyclic]
enumFromThenTo :: Acyclic -> Acyclic -> Acyclic -> [Acyclic]
Enum, Acyclic -> Acyclic -> Bool
(Acyclic -> Acyclic -> Bool)
-> (Acyclic -> Acyclic -> Bool) -> Eq Acyclic
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Acyclic -> Acyclic -> Bool
== :: Acyclic -> Acyclic -> Bool
$c/= :: Acyclic -> Acyclic -> Bool
/= :: Acyclic -> Acyclic -> Bool
Eq, Int -> Acyclic -> String -> String
[Acyclic] -> String -> String
Acyclic -> String
(Int -> Acyclic -> String -> String)
-> (Acyclic -> String)
-> ([Acyclic] -> String -> String)
-> Show Acyclic
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Acyclic -> String -> String
showsPrec :: Int -> Acyclic -> String -> String
$cshow :: Acyclic -> String
show :: Acyclic -> String
$cshowList :: [Acyclic] -> String -> String
showList :: [Acyclic] -> String -> String
Show)

certainty :: Acyclic -> String
certainty :: Acyclic -> String
certainty Acyclic
Proven = String
"proven"
certainty Acyclic
Plausible = String
"plausible"

refused :: Refusal -> String
refused :: Refusal -> String
refused Refusal
refusal = case Refusal
refusal of
  Refusal
Unnamed -> String
"the join names no otherwise"
  Unformed Side
side -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"the %s side is no formation" (Side -> String
handed Side
side)
  Holding Side
side Attribute
AtLambda -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"the %s side is an atom" (Side -> String
handed Side
side)
  Holding Side
side Attribute
AtDelta -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"the %s side is a datum" (Side -> String
handed Side
side)
  Holding Side
side Attribute
attr -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"the %s side has %s" (Side -> String
handed Side
side) (Attribute -> String
printAttribute Attribute
attr)
  Unripe Side
Lefthand Attribute
attr -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s is void on the left and attached on the right" (Attribute -> String
printAttribute Attribute
attr)
  Unripe Side
Righthand Attribute
attr -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s is void on the right and attached on the left" (Attribute -> String
printAttribute Attribute
attr)
  where
    handed :: Side -> String
    handed :: Side -> String
handed Side
Lefthand = String
"left"
    handed Side
Righthand = String
"right"

dotted :: [Attribute] -> String
dotted :: [Attribute] -> String
dotted = (Attribute -> String) -> [Attribute] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Char
'.' Char -> String -> String
forall a. a -> [a] -> [a]
:) (String -> String) -> (Attribute -> String) -> Attribute -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attribute -> String
printAttribute)

lodged :: [Attribute] -> Expression -> Maybe Binding
lodged :: [Attribute] -> Expression -> Maybe Binding
lodged [Attribute
attr] (ExFormation [Binding]
bds) = [Binding] -> Maybe Binding
forall a. [a] -> Maybe a
listToMaybe [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
attr]
lodged (Attribute
attr : [Attribute]
path) (ExFormation [Binding]
bds) = [Expression] -> Maybe Expression
forall a. [a] -> Maybe a
listToMaybe [Expression
inner | BiTau Attribute
attr' Expression
inner <- [Binding]
bds, Attribute
attr' Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
attr] Maybe Expression -> (Expression -> Maybe Binding) -> Maybe Binding
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Attribute] -> Expression -> Maybe Binding
lodged [Attribute]
path
lodged [Attribute]
_ Expression
_ = Maybe Binding
forall a. Maybe a
Nothing

data Evaluation
  = EvRun Judgment T.Text
  | EvFiring Int T.Text Judgment Expression
  | EvStarted Int Judgment Expression
  | EvDelta Int Bytes
  | EvManufactured Int Int
  | EvBoxed Int Expression
  | EvUndressed Int Expression
  | EvLooped Int Judgment Acyclic Expression Expression (Maybe (Int, Expression))
  | EvStuck Int T.Text Judgment Expression
  | EvStall Int T.Text
  | EvStuckOn Int T.Text
  | EvStarved Int Int Judgment Expression
  | EvTimeout Int Int Judgment Expression
  | EvSpent Int Int Judgment Expression
  | EvData Int T.Text Expression (Either Int Bytes)
  | EvTerm Int T.Text Judgment Expression Expression
  | EvBound Int Expression Expression
  | EvReshaped Int T.Text T.Text Expression Expression
  | EvSymbolized Int Int Bytes
  | EvCast Int T.Text Expression Expression Expression
  | EvMinted Int Int [Either Int Bytes]
  | EvDeferred Int Int Judgment Expression (Maybe Expression) Expression
  | EvApplied Int Judgment Expression Expression Expression
  | EvBuilt Int Expression
  | EvAnswer Int Expression
  | EvMorphed Int Expression
  | EvJoined Int (Either T.Text Expression) Int (Int, Int) (Maybe Int) (Maybe Expression)
  | EvDiverged Int (Expression, Expression) (Expression, Expression) [Attribute] Refusal
  | EvUnripe Int (Expression, Expression) (Expression, Expression) Side Attribute
  | EvFabricated Int (Expression, Expression) (Expression, Expression) Expression
  | EvTaken Int Expression
  | EvWorld Expression
  | EvHeader Header Expression Expression

data Header = Header String (Maybe String) ZonedTime [String] World (Maybe (FilePath, Int))

data World = World (Maybe FilePath) Int Int Int Int

type SaveEvalFunc = Evaluation -> IO ()

resited :: Expression -> Expression -> Evaluation -> Evaluation
resited :: Expression -> Expression -> Evaluation -> Evaluation
resited Expression
from Expression
to = Evaluation -> Evaluation
record
  where
    record :: Evaluation -> Evaluation
    record :: Evaluation -> Evaluation
record (EvFiring Int
depth Text
key Judgment
judgment Expression
site) = Int -> Text -> Judgment -> Expression -> Evaluation
EvFiring Int
depth Text
key Judgment
judgment (Expression -> Expression
moved Expression
site)
    record (EvStarted Int
depth Judgment
judgment Expression
site) = Int -> Judgment -> Expression -> Evaluation
EvStarted Int
depth Judgment
judgment (Expression -> Expression
moved Expression
site)
    record (EvLooped Int
depth Judgment
judgment Acyclic
mode Expression
self Expression
site Maybe (Int, Expression)
answered) = Int
-> Judgment
-> Acyclic
-> Expression
-> Expression
-> Maybe (Int, Expression)
-> Evaluation
EvLooped Int
depth Judgment
judgment Acyclic
mode Expression
self (Expression -> Expression
moved Expression
site) Maybe (Int, Expression)
answered
    record (EvStarved Int
depth Int
limit Judgment
judgment Expression
site) = Int -> Int -> Judgment -> Expression -> Evaluation
EvStarved Int
depth Int
limit Judgment
judgment (Expression -> Expression
moved Expression
site)
    record (EvTimeout Int
depth Int
limit Judgment
judgment Expression
site) = Int -> Int -> Judgment -> Expression -> Evaluation
EvTimeout Int
depth Int
limit Judgment
judgment (Expression -> Expression
moved Expression
site)
    record (EvSpent Int
depth Int
limit Judgment
judgment Expression
site) = Int -> Int -> Judgment -> Expression -> Evaluation
EvSpent Int
depth Int
limit Judgment
judgment (Expression -> Expression
moved Expression
site)
    record (EvDeferred Int
depth Int
sym Judgment
judgment Expression
copy Maybe Expression
call Expression
site) = Int
-> Int
-> Judgment
-> Expression
-> Maybe Expression
-> Expression
-> Evaluation
EvDeferred Int
depth Int
sym Judgment
judgment Expression
copy Maybe Expression
call (Expression -> Expression
moved Expression
site)
    record (EvApplied Int
depth Judgment
judgment Expression
call Expression
object Expression
site) = Int
-> Judgment -> Expression -> Expression -> Expression -> Evaluation
EvApplied Int
depth Judgment
judgment Expression
call Expression
object (Expression -> Expression
moved Expression
site)
    record Evaluation
other = Evaluation
other
    moved :: Expression -> Expression
    moved :: Expression -> Expression
moved Expression
site
      | Expression
site Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
from = Expression
to
      | Bool
otherwise = Expression
site

ieee :: Bytes -> Maybe String
ieee :: Bytes -> Maybe String
ieee Bytes
bytes
  | Bytes -> Int
btsSize Bytes
bytes Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
8 = String -> Maybe String
forall a. a -> Maybe a
Just (Double -> String
forall a. Show a => a -> String
show (Bytes -> Double
btsToNum Bytes
bytes))
  | Bool
otherwise = Maybe String
forall a. Maybe a
Nothing

tier :: Evaluation -> Int
tier :: Evaluation -> Int
tier EvRun{} = Int
0
tier (EvFiring Int
depth Text
_ Judgment
_ Expression
_) = Int
depth
tier (EvStarted Int
depth Judgment
_ Expression
_) = Int
depth
tier (EvDelta Int
depth Bytes
_) = Int
depth
tier (EvManufactured Int
depth Int
_) = Int
depth
tier (EvBoxed Int
depth Expression
_) = Int
depth
tier (EvUndressed Int
depth Expression
_) = Int
depth
tier (EvLooped Int
depth Judgment
_ Acyclic
_ Expression
_ Expression
_ Maybe (Int, Expression)
_) = Int
depth
tier (EvStuck Int
depth Text
_ Judgment
_ Expression
_) = Int
depth
tier (EvStall Int
depth Text
_) = Int
depth
tier (EvStuckOn Int
depth Text
_) = Int
depth
tier (EvStarved Int
depth Int
_ Judgment
_ Expression
_) = Int
depth
tier (EvTimeout Int
depth Int
_ Judgment
_ Expression
_) = Int
depth
tier (EvSpent Int
depth Int
_ Judgment
_ Expression
_) = Int
depth
tier (EvData Int
depth Text
_ Expression
_ Either Int Bytes
_) = Int
depth
tier (EvTerm Int
depth Text
_ Judgment
_ Expression
_ Expression
_) = Int
depth
tier (EvBound Int
depth Expression
_ Expression
_) = Int
depth
tier (EvReshaped Int
depth Text
_ Text
_ Expression
_ Expression
_) = Int
depth
tier (EvSymbolized Int
depth Int
_ Bytes
_) = Int
depth
tier (EvCast Int
depth Text
_ Expression
_ Expression
_ Expression
_) = Int
depth
tier (EvMinted Int
depth Int
_ [Either Int Bytes]
_) = Int
depth
tier (EvDeferred Int
depth Int
_ Judgment
_ Expression
_ Maybe Expression
_ Expression
_) = Int
depth
tier (EvApplied Int
depth Judgment
_ Expression
_ Expression
_ Expression
_) = Int
depth
tier (EvBuilt Int
depth Expression
_) = Int
depth
tier (EvAnswer Int
depth Expression
_) = Int
depth
tier (EvMorphed Int
depth Expression
_) = Int
depth
tier (EvJoined Int
depth Either Text Expression
_ Int
_ (Int, Int)
_ Maybe Int
_ Maybe Expression
_) = Int
depth
tier (EvDiverged Int
depth (Expression, Expression)
_ (Expression, Expression)
_ [Attribute]
_ Refusal
_) = Int
depth
tier (EvUnripe Int
depth (Expression, Expression)
_ (Expression, Expression)
_ Side
_ Attribute
_) = Int
depth
tier (EvFabricated Int
depth (Expression, Expression)
_ (Expression, Expression)
_ Expression
_) = Int
depth
tier (EvTaken Int
depth Expression
_) = Int
depth
tier EvWorld{} = Int
forall a. Bounded a => a
maxBound
tier EvHeader{} = Int
0

type Named a = Map.Map Int [(Expression, a)]

namedLookup :: Expression -> Named a -> Maybe a
namedLookup :: forall a. Expression -> Named a -> Maybe a
namedLookup Expression
term Named a
names = Expression -> [(Expression, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Expression
term ([(Expression, a)] -> Int -> Named a -> [(Expression, a)]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] (Expression -> Int
hashExpression Expression
term) Named a
names)

namedInsert :: forall a. Expression -> a -> Named a -> Named a
namedInsert :: forall a. Expression -> a -> Named a -> Named a
namedInsert Expression
term a
naming = (Maybe [(Expression, a)] -> Maybe [(Expression, a)])
-> Int -> Map Int [(Expression, a)] -> Map Int [(Expression, a)]
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter Maybe [(Expression, a)] -> Maybe [(Expression, a)]
renamed (Expression -> Int
hashExpression Expression
term)
  where
    renamed :: Maybe [(Expression, a)] -> Maybe [(Expression, a)]
    renamed :: Maybe [(Expression, a)] -> Maybe [(Expression, a)]
renamed Maybe [(Expression, a)]
entries = [(Expression, a)] -> Maybe [(Expression, a)]
forall a. a -> Maybe a
Just ((Expression
term, a
naming) (Expression, a) -> [(Expression, a)] -> [(Expression, a)]
forall a. a -> [a] -> [a]
: ((Expression, a) -> Bool) -> [(Expression, a)] -> [(Expression, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
/= Expression
term) (Expression -> Bool)
-> ((Expression, a) -> Expression) -> (Expression, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expression, a) -> Expression
forall a b. (a, b) -> a
fst) ([(Expression, a)] -> Maybe [(Expression, a)] -> [(Expression, a)]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [(Expression, a)]
entries))

namedFormation :: Expression -> a -> Named a -> Named a
namedFormation :: forall a. Expression -> a -> Named a -> Named a
namedFormation term :: Expression
term@(ExFormation [Binding]
bds) a
naming Named a
names
  | (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Maybe Attribute -> [Maybe Attribute] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Attribute -> Maybe Attribute
forall a. a -> Maybe a
Just Attribute
AtLambda, Attribute -> Maybe Attribute
forall a. a -> Maybe a
Just Attribute
AtDelta]) (Maybe Attribute -> Bool)
-> (Binding -> Maybe Attribute) -> Binding -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binding -> Maybe Attribute
attributeFromBinding) [Binding]
bds = Expression -> a -> Named a -> Named a
forall a. Expression -> a -> Named a -> Named a
namedInsert Expression
term a
naming Named a
names
namedFormation Expression
_ a
_ Named a
names = Named a
names

abbreviated :: Named Expression -> Expression -> Expression
abbreviated :: Named Expression -> Expression -> Expression
abbreviated Named Expression
names Expression
term
  | Named Expression -> Bool
forall k a. Map k a -> Bool
Map.null Named Expression
names = Expression
term
  | Bool
otherwise = Expression -> Maybe Expression -> Expression
forall a. a -> Maybe a -> a
fromMaybe (Named Expression -> Expression -> Expression
abbreviatedInside Named Expression
names Expression
term) (Expression -> Named Expression -> Maybe Expression
forall a. Expression -> Named a -> Maybe a
namedLookup Expression
term Named Expression
names)

abbreviatedInside :: Named Expression -> Expression -> Expression
abbreviatedInside :: Named Expression -> Expression -> Expression
abbreviatedInside Named Expression
names (ExFormation [Binding]
bds) = [Binding] -> Expression
ExFormation ((Binding -> Binding) -> [Binding] -> [Binding]
forall a b. (a -> b) -> [a] -> [b]
map Binding -> Binding
binding [Binding]
bds)
  where
    binding :: Binding -> Binding
    binding :: Binding -> Binding
binding (BiTau Attribute
attr Expression
expr) = Attribute -> Expression -> Binding
BiTau Attribute
attr (Named Expression -> Expression -> Expression
abbreviated Named Expression
names Expression
expr)
    binding Binding
bd = Binding
bd
abbreviatedInside Named Expression
names (ExApplication Expression
expr (ArTau Attribute
attr Expression
arg)) = Expression -> Argument -> Expression
ExApplication (Named Expression -> Expression -> Expression
abbreviated Named Expression
names Expression
expr) (Attribute -> Expression -> Argument
ArTau Attribute
attr (Named Expression -> Expression -> Expression
abbreviated Named Expression
names Expression
arg))
abbreviatedInside Named Expression
names (ExApplication Expression
expr (ArAlpha Alpha
alpha Expression
arg)) = Expression -> Argument -> Expression
ExApplication (Named Expression -> Expression -> Expression
abbreviated Named Expression
names Expression
expr) (Alpha -> Expression -> Argument
ArAlpha Alpha
alpha (Named Expression -> Expression -> Expression
abbreviated Named Expression
names Expression
arg))
abbreviatedInside Named Expression
names (ExDispatch Expression
expr Attribute
attr) = Expression -> Attribute -> Expression
ExDispatch (Named Expression -> Expression -> Expression
abbreviated Named Expression
names Expression
expr) Attribute
attr
abbreviatedInside Named Expression
_ Expression
term = Expression
term

data Protocol = Protocol
  { Protocol -> Int
_fired :: Int
  , Protocol -> Named Text
_named :: Named T.Text
  , Protocol -> [(Int, Int)]
_open :: [(Int, Int)]
  , Protocol -> Bool
_begun :: Bool
  , Protocol -> Named Expression
_made :: Named Expression
  , Protocol -> Map Int Int
_counted :: Map.Map Int Int
  , Protocol -> Map Int Int
_built :: Map.Map Int Int
  , Protocol -> Map Int Int
_deltas :: Map.Map Int Int
  , Protocol -> Maybe (Either Int Bytes, String)
_found :: Maybe (Either Int Bytes, String)
  , Protocol -> [(Int, Maybe (Judgment, String), String, Bool)]
_blocks :: [(Int, Maybe (Judgment, String), String, Bool)]
  , Protocol -> [(Int, Expression, String)]
_answered :: [(Int, Expression, String)]
  , Protocol -> Map Int (Named Expression)
_unwritten :: Map.Map Int (Named Expression)
  }

emptyProtocol :: Protocol
emptyProtocol :: Protocol
emptyProtocol = Int
-> Named Text
-> [(Int, Int)]
-> Bool
-> Named Expression
-> Map Int Int
-> Map Int Int
-> Map Int Int
-> Maybe (Either Int Bytes, String)
-> [(Int, Maybe (Judgment, String), String, Bool)]
-> [(Int, Expression, String)]
-> Map Int (Named Expression)
-> Protocol
Protocol Int
0 Named Text
forall k a. Map k a
Map.empty [] Bool
False Named Expression
forall k a. Map k a
Map.empty Map Int Int
forall k a. Map k a
Map.empty Map Int Int
forall k a. Map k a
Map.empty Map Int Int
forall k a. Map k a
Map.empty Maybe (Either Int Bytes, String)
forall a. Maybe a
Nothing [] [] Map Int (Named Expression)
forall k a. Map k a
Map.empty

data Nesting = Nesting
  { Nesting -> Int
_fires :: Int
  , Nesting -> [(Int, Int)]
_openedAt :: [(Int, Int)]
  , Nesting -> [(Int, String)]
_closing :: [(Int, String)]
  , Nesting -> Named Expression
_objects :: Named Expression
  , Nesting -> Map Int Int
_numbered :: Map.Map Int Int
  , Nesting -> Map Int Int
_parts :: Map.Map Int Int
  , Nesting -> Map Int Int
_datums :: Map.Map Int Int
  , Nesting -> Maybe (Either Int Bytes, String)
_held :: Maybe (Either Int Bytes, String)
  , Nesting -> [(Int, (Judgment, Expression))]
_heads :: [(Int, (Judgment, Expression))]
  , Nesting -> [(Int, Judgment, Expression)]
_pending :: [(Int, Judgment, Expression)]
  , Nesting -> [(Int, Expression, String)]
_sources :: [(Int, Expression, String)]
  , Nesting -> Map Attribute Expression
_world :: Map.Map Attribute Expression
  , Nesting -> Map [Maybe Attribute] [(Expression, [Binding])]
_shapes :: Map.Map [Maybe Attribute] [(Expression, [Binding])]
  , Nesting -> Int
_opaque :: Int
  , Nesting -> Map Int (Named Expression)
_unmarked :: Map.Map Int (Named Expression)
  }

type Naming = StateT (Nesting, [String]) IO

emptyNesting :: Nesting
emptyNesting :: Nesting
emptyNesting = Int
-> [(Int, Int)]
-> [(Int, String)]
-> Named Expression
-> Map Int Int
-> Map Int Int
-> Map Int Int
-> Maybe (Either Int Bytes, String)
-> [(Int, (Judgment, Expression))]
-> [(Int, Judgment, Expression)]
-> [(Int, Expression, String)]
-> Map Attribute Expression
-> Map [Maybe Attribute] [(Expression, [Binding])]
-> Int
-> Map Int (Named Expression)
-> Nesting
Nesting Int
0 [] [] Named Expression
forall k a. Map k a
Map.empty Map Int Int
forall k a. Map k a
Map.empty Map Int Int
forall k a. Map k a
Map.empty Map Int Int
forall k a. Map k a
Map.empty Maybe (Either Int Bytes, String)
forall a. Maybe a
Nothing [] [] [] Map Attribute Expression
forall k a. Map k a
Map.empty Map [Maybe Attribute] [(Expression, [Binding])]
forall k a. Map k a
Map.empty Int
0 Map Int (Named Expression)
forall k a. Map k a
Map.empty

saveEval :: Handle -> IORef Protocol -> (Expression -> IO String) -> (Expression -> IO String) -> SaveEvalFunc
saveEval :: Handle
-> IORef Protocol
-> (Expression -> IO String)
-> (Expression -> IO String)
-> SaveEvalFunc
saveEval Handle
handle IORef Protocol
cursor Expression -> IO String
printed Expression -> IO String
printed' Evaluation
report = do
  [String]
made <- IORef Protocol
-> (Protocol -> IO (Protocol, [String])) -> IO [String]
forall a b. IORef a -> (a -> IO (a, b)) -> IO b
atomicModify IORef Protocol
cursor (((Protocol, Maybe String) -> (Protocol, [String]))
-> IO (Protocol, Maybe String) -> IO (Protocol, [String])
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Protocol -> Protocol)
-> (Protocol, [String]) -> (Protocol, [String])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Evaluation -> Protocol -> Protocol
forgotten Evaluation
report) ((Protocol, [String]) -> (Protocol, [String]))
-> ((Protocol, Maybe String) -> (Protocol, [String]))
-> (Protocol, Maybe String)
-> (Protocol, [String])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Protocol, Maybe String) -> (Protocol, [String])
headed) (IO (Protocol, Maybe String) -> IO (Protocol, [String]))
-> (Protocol -> IO (Protocol, Maybe String))
-> Protocol
-> IO (Protocol, [String])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Evaluation -> Protocol -> IO (Protocol, Maybe String)
written (Evaluation -> Int
tier Evaluation
report) Evaluation
report (Protocol -> IO (Protocol, Maybe String))
-> (Protocol -> Protocol)
-> Protocol
-> IO (Protocol, Maybe String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Evaluation -> Protocol -> Protocol
beside (Evaluation -> Int
tier Evaluation
report) Evaluation
report (Protocol -> Protocol)
-> (Protocol -> Protocol) -> Protocol -> Protocol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Protocol -> Protocol
outer (Evaluation -> Int
tier Evaluation
report))
  (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
saved [String]
made
  where
    forgotten :: Evaluation -> Protocol -> Protocol
    forgotten :: Evaluation -> Protocol -> Protocol
forgotten EvBound{} Protocol
protocol = Protocol
protocol
    forgotten EvDelta{} Protocol
protocol = Protocol
protocol
    forgotten EvManufactured{} Protocol
protocol = Protocol
protocol
    forgotten EvWorld{} Protocol
protocol = Protocol
protocol
    forgotten Evaluation
_ Protocol
protocol = Protocol
protocol{_found = Nothing}
    beside :: Int -> Evaluation -> Protocol -> Protocol
    beside :: Int -> Evaluation -> Protocol -> Protocol
beside Int
_ EvStarted{} Protocol
protocol = Protocol
protocol
    beside Int
_ EvMinted{} Protocol
protocol = Protocol
protocol
    beside Int
_ EvBound{} Protocol
protocol = Protocol
protocol
    beside Int
at Evaluation
_ Protocol
protocol = Protocol
protocol{_blocks = dropWhile (\(Int
level, Maybe (Judgment, String)
_, String
_, Bool
_) -> Int
level Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
at) protocol._blocks}
    headed :: (Protocol, Maybe String) -> (Protocol, [String])
    headed :: (Protocol, Maybe String) -> (Protocol, [String])
headed (Protocol
protocol, Maybe String
Nothing) = (Protocol
protocol, [])
    headed (Protocol
protocol, Just String
line) =
      ( Protocol
protocol{_blocks = [(level, heading, opening, True) | (level, heading, opening, _) <- protocol._blocks]}
      , [String
opening | (Int
_, Maybe (Judgment, String)
_, String
opening, Bool
False) <- [(Int, Maybe (Judgment, String), String, Bool)]
-> [(Int, Maybe (Judgment, String), String, Bool)]
forall a. [a] -> [a]
reverse Protocol
protocol._blocks] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ String -> [String]
lines String
line
      )
    render :: Expression -> IO String
    render :: Expression -> IO String
render Expression
term = do
      Protocol
protocol <- IORef Protocol -> IO Protocol
forall a. IORef a -> IO a
readIORef IORef Protocol
cursor
      Expression -> IO String
printed (Named Expression -> Expression -> Expression
abbreviated Protocol
protocol._made Expression
term)
    located :: Protocol -> Expression -> IO String
    located :: Protocol -> Expression -> IO String
located Protocol
protocol Expression
site = case [String
naming | (Int
_, Expression
built, String
naming) <- Protocol
protocol._answered, Expression
built Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
site] of
      String
naming : [String]
_ -> String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
naming
      [] -> Expression -> IO String
salted (Protocol -> Expression -> Expression
unwritten Protocol
protocol Expression
site)
    context :: Protocol -> Judgment -> Expression -> IO [String]
    context :: Protocol -> Judgment -> Expression -> IO [String]
context Protocol
protocol Judgment
judgment Expression
site = do
      String
locator <- Protocol -> Expression -> IO String
located Protocol
protocol Expression
site
      let said :: String
said = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s(%s)" (Judgment -> String
letter Judgment
judgment) String
locator
      [String] -> IO [String]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [String
said | Protocol -> Maybe String
innermost Protocol
protocol Maybe String -> Maybe String -> Bool
forall a. Eq a => a -> a -> Bool
/= String -> Maybe String
forall a. a -> Maybe a
Just String
said]
    innermost :: Protocol -> Maybe String
    innermost :: Protocol -> Maybe String
innermost Protocol
protocol = case Protocol
protocol._blocks of
      (Int
_, Maybe (Judgment, String)
heading, String
_, Bool
_) : [(Int, Maybe (Judgment, String), String, Bool)]
_ -> (Judgment, String) -> String
forall a b. (a, b) -> b
snd ((Judgment, String) -> String)
-> Maybe (Judgment, String) -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Judgment, String)
heading
      [] -> Maybe String
forall a. Maybe a
Nothing
    remarked :: String -> [String] -> String
    remarked :: String -> [String] -> String
remarked String
line [] = String
line
    remarked String
line [String]
remarks = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s  # %s" String
line (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
remarks)
    salted :: Expression -> IO String
    salted :: Expression -> IO String
salted Expression
term = do
      Protocol
protocol <- IORef Protocol -> IO Protocol
forall a. IORef a -> IO a
readIORef IORef Protocol
cursor
      Expression -> IO String
printed' (Named Expression -> Expression -> Expression
abbreviated Protocol
protocol._made Expression
term)
    saved :: String -> IO ()
    saved :: String -> IO ()
saved String
line = do
      Handle -> String -> IO ()
hPutStrLn Handle
handle String
line
      String -> IO ()
logDebug (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Saved one line of the protocol: %s" ((Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ') String
line))
    written :: Int -> Evaluation -> Protocol -> IO (Protocol, Maybe String)
    written :: Int -> Evaluation -> Protocol -> IO (Protocol, Maybe String)
written Int
_ (EvRun Judgment
judgment Text
locator) Protocol
protocol =
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol{_begun = True, _blocks = [(0, Just (judgment, heading), heading ++ ":", True)]}, String -> Maybe String
forall a. a -> Maybe a
Just (String
heading String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":"))
      where
        heading :: String
        heading :: String
heading = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s(%s)" (Judgment -> String
letter Judgment
judgment) (Text -> String
T.unpack Text
locator)
    written Int
at (EvFiring Int
depth Text
key Judgment
judgment Expression
site) Protocol
protocol = do
      String
opening <- Int -> String -> String
indented Int
at (String -> String) -> ([String] -> String) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> String
remarked (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"𝔼(%s):" (Text -> String
T.unpack Text
key)) ([String] -> String) -> IO [String] -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Protocol -> Judgment -> Expression -> IO [String]
context Protocol
protocol Judgment
judgment Expression
site
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( Protocol
protocol
            { _fired = firings
            , _open = (depth, firings) : protocol._open
            , _blocks = (at, Nothing, opening, True) : protocol._blocks
            }
        , String -> Maybe String
forall a. a -> Maybe a
Just String
opening
        )
      where
        firings :: Int
        firings :: Int
firings = Protocol
protocol._fired Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    written Int
at (EvStarted Int
_ Judgment
judgment Expression
site) Protocol
protocol = do
      String
locator <- Protocol -> Expression -> IO String
located Protocol
protocol Expression
site
      let heading :: String
heading = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s(%s)" (Judgment -> String
letter Judgment
judgment) String
locator
          inner :: [(Int, Maybe (Judgment, String), String, Bool)]
inner = ((Int, Maybe (Judgment, String), String, Bool) -> Bool)
-> [(Int, Maybe (Judgment, String), String, Bool)]
-> [(Int, Maybe (Judgment, String), String, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (\(Int
level, Maybe (Judgment, String)
_, String
_, Bool
_) -> Int
level Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
at) Protocol
protocol._blocks
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Protocol, Maybe String) -> IO (Protocol, Maybe String))
-> (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a b. (a -> b) -> a -> b
$ case [(Int, Maybe (Judgment, String), String, Bool)]
inner of
        (Int
level, Just (Judgment, String)
heading', String
_, Bool
_) : [(Int, Maybe (Judgment, String), String, Bool)]
_ | Int
level Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
at Bool -> Bool -> Bool
&& (Judgment, String)
heading' (Judgment, String) -> (Judgment, String) -> Bool
forall a. Eq a => a -> a -> Bool
== (Judgment
judgment, String
heading) -> (Protocol
protocol{_blocks = inner}, Maybe String
forall a. Maybe a
Nothing)
        [(Int, Maybe (Judgment, String), String, Bool)]
_ -> (Protocol
protocol{_blocks = (at, Just (judgment, heading), indented at (heading ++ ":"), False) : dropWhile (\(Int
level, Maybe (Judgment, String)
_, String
_, Bool
_) -> Int
level Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
at) inner}, Maybe String
forall a. Maybe a
Nothing)
    written Int
at (EvDelta Int
_ Bytes
bytes) Protocol
protocol = do
      String
datum <- Expression -> IO String
render (Bytes -> Expression
ExBytes Bytes
bytes)
      let (String
naming, Protocol
protocol') = Either Int Bytes -> Protocol -> (String, Protocol)
stored (Bytes -> Either Int Bytes
forall a b. b -> Either a b
Right Bytes
bytes) Protocol
protocol
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol', String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> [String] -> String
remarked (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s := %s" String
naming String
datum) ([String] -> (String -> [String]) -> Maybe String -> [String]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bytes -> Maybe String
ieee Bytes
bytes)))))
    written Int
at (EvManufactured Int
_ Int
symbol) Protocol
protocol = do
      String
datum <- Either Int Bytes -> IO String
spelt (Int -> Either Int Bytes
forall a b. a -> Either a b
Left Int
symbol)
      let (String
naming, Protocol
protocol') = Either Int Bytes -> Protocol -> (String, Protocol)
stored (Int -> Either Int Bytes
forall a b. a -> Either a b
Left Int
symbol) Protocol
protocol
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol', String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s := %s" String
naming String
datum)))
    written Int
at (EvBoxed Int
_ Expression
term) Protocol
protocol = Int
-> String -> Expression -> Protocol -> IO (Protocol, Maybe String)
taking Int
at String
"boxed" Expression
term Protocol
protocol
    written Int
at (EvUndressed Int
_ Expression
term) Protocol
protocol = Int
-> String -> Expression -> Protocol -> IO (Protocol, Maybe String)
taking Int
at String
"undressed" Expression
term Protocol
protocol
    written Int
at (EvLooped Int
_ Judgment
judgment Acyclic
mode Expression
self Expression
site Maybe (Int, Expression)
answered) Protocol
protocol = do
      String
form <- Expression -> IO String
render Expression
self
      [String]
remarks <- Protocol -> Judgment -> Expression -> IO [String]
context Protocol
protocol Judgment
judgment Expression
site
      (String
line, [String]
notes) <- IO (String, [String])
-> ((Int, Expression) -> IO (String, [String]))
-> Maybe (Int, Expression)
-> IO (String, [String])
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((String, [String]) -> IO (String, [String])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"looped %s" String
form, [])) (String -> (Int, Expression) -> IO (String, [String])
severed String
form) Maybe (Int, Expression)
answered
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> [String] -> String
remarked String
line ([String]
remarks [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ Acyclic -> String
certainty Acyclic
mode String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
notes))))
      where
        severed :: String -> (Int, Expression) -> IO (String, [String])
        severed :: String -> (Int, Expression) -> IO (String, [String])
severed String
form (Int
symbol, Expression
call) = do
          String
made <- Expression -> IO String
printed (Named Expression -> Expression -> Expression
abbreviatedInside Protocol
protocol._made Expression
call)
          (String, [String]) -> IO (String, [String])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"looped %s := %s" (Function -> String
printFunction (Int -> Function
FnSymbol Int
symbol)) String
made, [String -> String -> String
forall r. PrintfType r => String -> r
printf String
"repeats %s" String
form])
    written Int
at (EvStuck Int
_ Text
key Judgment
judgment Expression
self) Protocol
protocol = do
      String
form <- Expression -> IO String
render Expression
self
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"unanswered %s  # %s(%s)" (Text -> String
T.unpack Text
key) (Judgment -> String
letter Judgment
judgment) String
form)))
    written Int
at (EvStall Int
_ Text
key) Protocol
protocol =
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"stall %s" (Text -> String
T.unpack Text
key))))
    written Int
at (EvStuckOn Int
_ Text
key) Protocol
protocol =
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"stuck %s" (Text -> String
T.unpack Text
key))))
    written Int
at (EvStarved Int
_ Int
limit Judgment
judgment Expression
site) Protocol
protocol = do
      [String]
remarks <- Protocol -> Judgment -> Expression -> IO [String]
context Protocol
protocol Judgment
judgment Expression
site
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> [String] -> String
remarked (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"starved %d" Int
limit) [String]
remarks)))
    written Int
at (EvTimeout Int
_ Int
limit Judgment
judgment Expression
site) Protocol
protocol = do
      [String]
remarks <- Protocol -> Judgment -> Expression -> IO [String]
context Protocol
protocol Judgment
judgment Expression
site
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> [String] -> String
remarked (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"timeout %d" Int
limit) [String]
remarks)))
    written Int
at (EvSpent Int
_ Int
limit Judgment
judgment Expression
site) Protocol
protocol = do
      [String]
remarks <- Protocol -> Judgment -> Expression -> IO [String]
context Protocol
protocol Judgment
judgment Expression
site
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> [String] -> String
remarked (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"spent %d" Int
limit) [String]
remarks)))
    written Int
at (EvData Int
_ Text
spelling Expression
operand Either Int Bytes
value) Protocol
protocol = do
      String
datum <- IO String -> (String -> IO String) -> Maybe String -> IO String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Either Int Bytes -> IO String
spelt Either Int Bytes
value) String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Int Bytes
-> Maybe (Either Int Bytes, String) -> Maybe String
found Either Int Bytes
value Protocol
protocol._found)
      String
line <- Protocol -> String -> Judgment -> Expression -> IO String
commented Protocol
protocol (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s := %s" (Protocol -> Text -> String
labelled Protocol
protocol Text
spelling) String
datum) Judgment
Dataization Expression
operand
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at String
line))
    written Int
at (EvTerm Int
_ Text
spelling Judgment
judgment Expression
operand Expression
term) Protocol
protocol = do
      let naming :: String
naming = Protocol -> Text -> String
labelled Protocol
protocol Text
spelling
      (Protocol
protocol', String
value) <- Protocol -> String -> Expression -> IO (Protocol, String)
valued Protocol
protocol String
naming Expression
term
      String
line <- Protocol -> String -> Judgment -> Expression -> IO String
commented Protocol
protocol (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s := %s" String
naming String
value) Judgment
judgment Expression
operand
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol', String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at String
line))
    written Int
_ (EvBound Int
_ Expression
meta Expression
term) Protocol
protocol =
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol{_unwritten = Map.alter (Just . namedInsert meta term . fromMaybe Map.empty) (opener protocol) protocol._unwritten}, Maybe String
forall a. Maybe a
Nothing)
    written Int
at (EvReshaped Int
_ Text
spelling Text
block Expression
source Expression
term) Protocol
protocol = do
      let naming :: String
naming = Protocol -> Text -> String
labelled Protocol
protocol Text
spelling
      (Protocol
protocol', String
value) <- Protocol -> String -> Expression -> IO (Protocol, String)
valued Protocol
protocol String
naming Expression
term
      String
line <- String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s := %s  # %s(%s)" String
naming String
value (Text -> String
T.unpack Text
block) (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> IO String
salted (Protocol -> Expression -> Expression
unwritten Protocol
protocol Expression
source)
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol', String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at String
line))
    written Int
at (EvSymbolized Int
_ Int
symbol Bytes
bytes) Protocol
protocol = do
      String
datum <- Expression -> IO String
render (Bytes -> Expression
ExBytes Bytes
bytes)
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> [String] -> String
remarked (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"symbolized %s := %s" (Function -> String
printFunction (Int -> Function
FnSymbol Int
symbol)) String
datum) ([String] -> (String -> [String]) -> Maybe String -> [String]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bytes -> Maybe String
ieee Bytes
bytes)))))
    written Int
at (EvCast Int
_ Text
spelling Expression
source Expression
model Expression
term) Protocol
protocol = do
      let naming :: String
naming = Protocol -> Text -> String
labelled Protocol
protocol Text
spelling
      (Protocol
protocol', String
value) <- Protocol -> String -> Expression -> IO (Protocol, String)
valued Protocol
protocol String
naming Expression
term
      String
one <- Protocol -> Expression -> IO String
spoken Protocol
protocol Expression
source
      String
two <- Protocol -> Expression -> IO String
spoken Protocol
protocol Expression
model
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol', String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"cast %s := %s  # %s up to %s" String
naming String
value String
one String
two)))
    written Int
_ EvMinted{} Protocol
protocol = (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, Maybe String
forall a. Maybe a
Nothing)
    written Int
at (EvDeferred Int
_ Int
symbol Judgment
judgment Expression
copy Maybe Expression
call Expression
site) Protocol
protocol = do
      String
form <- IO String
-> (Expression -> IO String) -> Maybe Expression -> IO String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Expression -> IO String
render Expression
copy) (Expression -> IO String
printed (Expression -> IO String)
-> (Expression -> Expression) -> Expression -> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Expression -> Expression -> Expression
abbreviatedInside Protocol
protocol._made) Maybe Expression
call
      [String]
remarks <- Protocol -> Judgment -> Expression -> IO [String]
context Protocol
protocol Judgment
judgment Expression
site
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> [String] -> String
remarked (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"deferred %s := %s" (Function -> String
printFunction (Int -> Function
FnSymbol Int
symbol)) String
form) [String]
remarks)))
    written Int
at (EvApplied Int
_ Judgment
judgment Expression
call Expression
object Expression
site) Protocol
protocol = do
      let (Int
index, Protocol
counted) = Protocol -> (Int, Protocol)
numbered Protocol
protocol
          (Int
index', Protocol
counted') = Protocol -> (Int, Protocol)
numbered Protocol
counted
          stem :: String
          stem :: String
stem = Protocol -> Text -> String
labelled Protocol
protocol Text
answer
      String
form <- Expression -> IO String
printed (Named Expression -> Expression -> Expression
abbreviatedInside Protocol
protocol._made Expression
call)
      String
body <- Expression -> IO String
printed (Named Expression -> Expression -> Expression
abbreviatedInside Protocol
protocol._made Expression
object)
      [String]
remarks <- Protocol -> Judgment -> Expression -> IO [String]
context Protocol
protocol Judgment
judgment Expression
site
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( Protocol
counted'{_made = namedInsert call (alias (opener protocol) index) (namedInsert object (alias (opener protocol) index') counted'._made)}
        , String -> Maybe String
forall a. a -> Maybe a
Just ([String] -> String
unlines [Int -> String -> String
indented Int
at (String -> [String] -> String
remarked (String -> String -> Int -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d := %s" String
stem Int
index String
form) [String]
remarks), Int -> String -> String
indented Int
at (String -> String -> Int -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d := %s" String
stem Int
index' String
body)])
        )
    written Int
at (EvBuilt Int
depth Expression
term) Protocol
protocol = do
      let (Int
index, Protocol
counted) = Protocol -> (Int, Protocol)
numbered Protocol
protocol
      String
value <- Protocol -> Expression -> IO String
borrowed Protocol
protocol Expression
term
      let naming :: String
naming = String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d" (Protocol -> Text -> String
labelled Protocol
protocol Text
answer) Int
index
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
counted{_built = Map.insert (opener protocol) index counted._built, _answered = (depth, term, naming) : counted._answered}, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s := %s  # %s" String
naming String
value (Text -> String
T.unpack Text
answer))))
    written Int
at (EvAnswer Int
_ Expression
term) Protocol
protocol = do
      let (Int
index, Protocol
counted) = Protocol -> (Int, Protocol)
numbered Protocol
protocol
          stem :: String
          stem :: String
stem = Protocol -> Text -> String
labelled Protocol
protocol Text
answer
          naming :: String
          naming :: String
naming = String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d" String
stem Int
index
      (Protocol
protocol', String
value) <- Protocol -> String -> Expression -> IO (Protocol, String)
valued Protocol
counted String
naming Expression
term
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol'{_made = namedFormation term (alias (opener protocol) index) protocol'._made}, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s := %s  # 𝕄(%s·%d)" String
naming String
value String
stem (Int -> Int -> Map Int Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Int
1 (Protocol -> Int
opener Protocol
protocol) Protocol
protocol._built))))
    written Int
at (EvMorphed Int
_ Expression
term) Protocol
protocol = do
      let (Int
index, Protocol
counted) = Protocol -> (Int, Protocol)
numbered Protocol
protocol
          naming :: String
          naming :: String
naming = String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d" (Protocol -> Text -> String
labelled Protocol
protocol Text
answer) Int
index
      (Protocol
protocol', String
value) <- case (Expression -> Named Expression -> Maybe Expression
forall a. Expression -> Named a -> Maybe a
namedLookup Expression
term Protocol
protocol._made, Expression -> Named Text -> Maybe Text
forall a. Expression -> Named a -> Maybe a
namedLookup Expression
term Protocol
protocol._named) of
        (Maybe Expression
Nothing, Maybe Text
Nothing) -> Protocol -> String -> Expression -> IO (Protocol, String)
valued Protocol
counted String
naming Expression
term
        (Maybe Expression, Maybe Text)
_ -> (,) Protocol
counted (String -> (Protocol, String))
-> IO String -> IO (Protocol, String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Protocol -> Expression -> IO String
borrowed Protocol
protocol Expression
term
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol'{_made = namedFormation term (alias (opener protocol) index) protocol'._made}, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"morphed %s := %s" String
naming String
value)))
    written Int
at (EvJoined Int
_ Either Text Expression
condition Int
symbol (Int
left, Int
right) Maybe Int
bottom Maybe Expression
raised) Protocol
protocol = do
      String
on <- (Text -> IO String)
-> (Expression -> IO String) -> Either Text Expression -> IO String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> IO String) -> (Text -> String) -> Text -> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Protocol -> Text -> String
labelled Protocol
protocol) Expression -> IO String
salted Either Text Expression
condition
      String
termination <- Expression -> IO String
render Expression
ExTermination
      Maybe String
raiser <- (Expression -> IO String) -> Maybe Expression -> IO (Maybe String)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse Expression -> IO String
salted Maybe Expression
raised
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> [String] -> String
remarked (String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"joined %s := %s ? %s : %s" (Function -> String
printFunction (Int -> Function
FnSymbol Int
symbol)) String
on (Function -> String
printFunction (Int -> Function
FnSymbol Int
left)) (Function -> String
printFunction (Int -> Function
FnSymbol Int
right))) [String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"where %s is %s%s" (Function -> String
printFunction (Int -> Function
FnSymbol Int
idx)) String
termination (String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String -> String -> String
forall r. PrintfType r => String -> r
printf String
" raised by %s") Maybe String
raiser :: String) | Just Int
idx <- [Maybe Int
bottom], Int
idx Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int
left, Int
right]])))
    written Int
at (EvDiverged Int
_ (Expression, Expression)
left (Expression, Expression)
right [Attribute]
path Refusal
refusal) Protocol
protocol = do
      String
one <- Protocol -> (Expression, Expression) -> IO String
sided Protocol
protocol (Expression, Expression)
left
      String
two <- Protocol -> (Expression, Expression) -> IO String
sided Protocol
protocol (Expression, Expression)
right
      String
differed <- Protocol -> [Attribute] -> Expression -> Expression -> IO String
explained Protocol
protocol [Attribute]
path ((Expression, Expression) -> Expression
forall a b. (a, b) -> b
snd (Expression, Expression)
left) ((Expression, Expression) -> Expression
forall a b. (a, b) -> b
snd (Expression, Expression)
right)
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"diverged %s vs %s  # cannot join: %s; cannot fabricate: %s" String
one String
two String
differed (Refusal -> String
refused Refusal
refusal))))
    written Int
at (EvUnripe Int
_ (Expression, Expression)
left (Expression, Expression)
right Side
side Attribute
attr) Protocol
protocol = do
      String
one <- Protocol -> (Expression, Expression) -> IO String
sided Protocol
protocol (Expression, Expression)
left
      String
two <- Protocol -> (Expression, Expression) -> IO String
sided Protocol
protocol (Expression, Expression)
right
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"unripe %s vs %s  # %s" String
one String
two (Refusal -> String
refused (Side -> Attribute -> Refusal
Unripe Side
side Attribute
attr)))))
    written Int
at (EvFabricated Int
_ (Expression, Expression)
left (Expression, Expression)
right Expression
term) Protocol
protocol = do
      String
one <- Protocol -> (Expression, Expression) -> IO String
sided Protocol
protocol (Expression, Expression)
left
      String
two <- Protocol -> (Expression, Expression) -> IO String
sided Protocol
protocol (Expression, Expression)
right
      String
body <- Expression -> IO String
printed (Named Expression -> Expression -> Expression
abbreviatedInside Protocol
protocol._made Expression
term)
      let (Int
index, Protocol
counted) = Protocol -> (Int, Protocol)
numbered Protocol
protocol
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
counted{_made = namedInsert term (alias (opener protocol) index) counted._made}, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> Int -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"fabricated %s·%d := %s and %s  # %s" (Protocol -> Text -> String
labelled Protocol
protocol Text
answer) Int
index String
one String
two String
body)))
    written Int
at (EvTaken Int
_ Expression
term) Protocol
protocol = do
      let (Int
index, Protocol
counted) = Protocol -> (Int, Protocol)
numbered Protocol
protocol
          naming :: String
          naming :: String
naming = String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d" (Protocol -> Text -> String
labelled Protocol
protocol Text
answer) Int
index
      (Protocol
protocol', String
value) <- Protocol -> String -> Expression -> IO (Protocol, String)
valued Protocol
counted String
naming Expression
term
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol'{_made = namedFormation term (alias (opener protocol) index) protocol'._made}, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s := %s" String
naming String
value)))
    written Int
_ (EvWorld Expression
world) Protocol
protocol = (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol{_made = namedInsert world ExRoot protocol._made}, Maybe String
forall a. Maybe a
Nothing)
    written Int
_ (EvHeader (Header String
release Maybe String
revision ZonedTime
dated [String]
command (World Maybe String
file Int
count Int
size Int
tops Int
bindings) Maybe (String, Int)
table) Expression
locator Expression
expression) Protocol
protocol = do
      String
place <- Expression -> IO String
printed Expression
locator
      String
body <- Expression -> IO String
printed Expression
expression
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol, String -> Maybe String
forall a. a -> Maybe a
Just ([String] -> String
unlines ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"# " String -> String -> String
forall a. [a] -> [a] -> [a]
++) ([String]
told [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"Locator: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
place, String
"Expression: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
body]) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
""])))
      where
        told :: [String]
        told :: [String]
told =
          [ String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Written by phino %s on %s" (String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
release (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s (%s)" String
release) Maybe String
revision) (TimeLocale -> String -> ZonedTime -> String
forall t. FormatTime t => TimeLocale -> String -> t -> String
formatTime TimeLocale
defaultTimeLocale String
"%Y-%m-%d %H:%M:%S %Ez" ZonedTime
dated)
          , String
"Command: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
commanded [String]
command
          , String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"World: %s, %s" (String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"stdin" Maybe String
file) (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [Int -> String -> String -> String
amount Int
count String
"line" String
"lines", Int -> String -> String -> String
amount Int
size String
"byte" String
"bytes", Int -> String -> String -> String
amount Int
tops String
"object" String
"objects" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" at the top", Int -> String -> String -> String
amount Int
bindings String
"binding" String
"bindings"])
          ]
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"Symbolic: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
path String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String -> String
amount Int
entries String
"entry" String
"entries" | Just (String
path, Int
entries) <- [Maybe (String, Int)
table]]
        amount :: Int -> String -> String -> String
        amount :: Int -> String -> String -> String
amount Int
1 String
one String
_ = String
"1 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
one
        amount Int
many String
_ String
several = Int -> String
forall a. Show a => a -> String
show Int
many String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
several
    spelt :: Either Int Bytes -> IO String
    spelt :: Either Int Bytes -> IO String
spelt (Left Int
symbol) = String -> String -> String
forall r. PrintfType r => String -> r
printf String
"𝔻(%s)" (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> IO String
render (Int -> Expression
standing Int
symbol)
    spelt (Right Bytes
bytes) = Expression -> IO String
render (Bytes -> Expression
ExBytes Bytes
bytes)
    valued :: Protocol -> String -> Expression -> IO (Protocol, String)
    valued :: Protocol -> String -> Expression -> IO (Protocol, String)
valued Protocol
protocol String
naming Expression
term = case Expression -> Maybe Int
denoted Expression
term of
      Maybe Int
Nothing -> (,) Protocol
protocol (String -> (Protocol, String))
-> IO String -> IO (Protocol, String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> IO String
render Expression
term
      Just Int
_ -> do
        String
value <- IO String -> (Text -> IO String) -> Maybe Text -> IO String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Expression -> IO String
render Expression
term) (String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> IO String) -> (Text -> String) -> Text -> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack) (Expression -> Named Text -> Maybe Text
forall a. Expression -> Named a -> Maybe a
namedLookup Expression
term Protocol
protocol._named)
        (Protocol, String) -> IO (Protocol, String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
protocol{_named = namedInsert term (T.pack naming) protocol._named}, String
value)
    borrowed :: Protocol -> Expression -> IO String
    borrowed :: Protocol -> Expression -> IO String
borrowed Protocol
protocol Expression
term = case Expression -> Named Text -> Maybe Text
forall a. Expression -> Named a -> Maybe a
namedLookup Expression
term Protocol
protocol._named of
      Maybe Text
Nothing -> Expression -> IO String
render Expression
term
      Just Text
naming -> String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> String
T.unpack Text
naming)
    explained :: Protocol -> [Attribute] -> Expression -> Expression -> IO String
    explained :: Protocol -> [Attribute] -> Expression -> Expression -> IO String
explained Protocol
protocol [Attribute]
path Expression
one Expression
two = case [Attribute] -> [Attribute]
forall a. [a] -> [a]
reverse [Attribute]
path of
      [] -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"the left side is %s and the right side is %s" (String -> String -> String) -> IO String -> IO (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Protocol -> Expression -> IO String
borrowed Protocol
protocol Expression
one IO (String -> String) -> IO String -> IO String
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Protocol -> Expression -> IO String
borrowed Protocol
protocol Expression
two
      Attribute
attr : [Attribute]
_ -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"at %s the left side %s and the right side %s" ([Attribute] -> String
dotted [Attribute]
path) (String -> String -> String) -> IO String -> IO (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> IO String
had Expression
one IO (String -> String) -> IO String -> IO String
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> IO String
had Expression
two
        where
          had :: Expression -> IO String
          had :: Expression -> IO String
had Expression
side = IO String -> (Binding -> IO String) -> Maybe Binding -> IO String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"has no %s" (Attribute -> String
printAttribute Attribute
attr))) ((String -> String) -> IO String -> IO String
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
"has " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (IO String -> IO String)
-> (Binding -> IO String) -> Binding -> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binding -> IO String
bound) ([Attribute] -> Expression -> Maybe Binding
lodged [Attribute]
path Expression
side)
          bound :: Binding -> IO String
          bound :: Binding -> IO String
bound (BiTau Attribute
attr' Expression
term) = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s ↦ %s" (Attribute -> String
printAttribute Attribute
attr') (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Protocol -> Expression -> IO String
borrowed Protocol
protocol Expression
term
          bound (BiVoid Attribute
attr') = String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s ↦ ∅" (Attribute -> String
printAttribute Attribute
attr'))
          bound (BiDelta Bytes
bytes) = String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Δ ⤍ %s" (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> IO String
render (Bytes -> Expression
ExBytes Bytes
bytes)
          bound (BiLambda Function
func) = String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"λ ⤍ %s" (Function -> String
printFunction Function
func))
          bound Binding
bd = String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Binding -> String
printBinding Binding
bd)
    sided :: Protocol -> (Expression, Expression) -> IO String
    sided :: Protocol -> (Expression, Expression) -> IO String
sided Protocol
_ (Expression
_, term :: Expression
term@(ExFormation [BiLambda (FnSymbol Int
_)])) = Expression -> IO String
render Expression
term
    sided Protocol
protocol (side :: Expression
side@(ExMeta Text
_), Expression
_) = Protocol -> Expression -> IO String
spoken Protocol
protocol Expression
side
    sided Protocol
protocol (Expression
_, Expression
term) = Protocol -> Expression -> IO String
borrowed Protocol
protocol Expression
term
    spoken :: Protocol -> Expression -> IO String
    spoken :: Protocol -> Expression -> IO String
spoken Protocol
protocol Expression
meta = IO String
-> (Expression -> IO String) -> Maybe Expression -> IO String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Protocol -> Text -> String
labelled Protocol
protocol (Text -> String) -> (String -> Text) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> IO String
salted Expression
meta) (Protocol -> Expression -> IO String
borrowed Protocol
protocol) (Expression -> Named Expression -> Maybe Expression
forall a. Expression -> Named a -> Maybe a
namedLookup Expression
meta (Protocol -> Named Expression
held Protocol
protocol))
    commented :: Protocol -> String -> Judgment -> Expression -> IO String
    commented :: Protocol -> String -> Judgment -> Expression -> IO String
commented Protocol
protocol String
line Judgment
judgment Expression
operand = String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s  # %s(%s)" String
line (Judgment -> String
letter Judgment
judgment) (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> IO String
salted (Protocol -> Expression -> Expression
unwritten Protocol
protocol Expression
operand)
    unwritten :: Protocol -> Expression -> Expression
    unwritten :: Protocol -> Expression -> Expression
unwritten Protocol
protocol = Named Expression -> Expression -> Expression
abbreviated (Protocol -> Named Expression
held Protocol
protocol)
    held :: Protocol -> Named Expression
    held :: Protocol -> Named Expression
held Protocol
protocol = Named Expression
-> Int -> Map Int (Named Expression) -> Named Expression
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Named Expression
forall k a. Map k a
Map.empty (Protocol -> Int
opener Protocol
protocol) Protocol
protocol._unwritten
    outer :: Int -> Protocol -> Protocol
    outer :: Int -> Protocol -> Protocol
outer Int
depth Protocol
protocol = Protocol
protocol{_open = dropWhile ((>= depth) . fst) protocol._open, _answered = dropWhile (\(Int
level, Expression
_, String
_) -> Int
level Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
depth) protocol._answered, _unwritten = foldr (Map.delete . snd) protocol._unwritten (takeWhile ((>= depth) . fst) protocol._open)}
    labelled :: Protocol -> T.Text -> String
    labelled :: Protocol -> Text -> String
labelled Protocol
protocol Text
spelling = String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d" (Text -> String
T.unpack Text
spelling) (Protocol -> Int
opener Protocol
protocol)
    opener :: Protocol -> Int
    opener :: Protocol -> Int
opener Protocol
protocol = Int -> ((Int, Int) -> Int) -> Maybe (Int, Int) -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 (Int, Int) -> Int
forall a b. (a, b) -> b
snd ([(Int, Int)] -> Maybe (Int, Int)
forall a. [a] -> Maybe a
listToMaybe Protocol
protocol._open)
    stored :: Either Int Bytes -> Protocol -> (String, Protocol)
    stored :: Either Int Bytes -> Protocol -> (String, Protocol)
stored Either Int Bytes
value Protocol
protocol = (String
naming, Protocol
protocol{_deltas = Map.insert (opener protocol) index protocol._deltas, _found = Just (value, naming)})
      where
        index :: Int
        index :: Int
index = Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
1 (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> Map Int Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Protocol -> Int
opener Protocol
protocol) Protocol
protocol._deltas)
        naming :: String
        naming :: String
naming = String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d" (Protocol -> Text -> String
labelled Protocol
protocol Text
sigil) Int
index
    numbered :: Protocol -> (Int, Protocol)
    numbered :: Protocol -> (Int, Protocol)
numbered Protocol
protocol = (Int
index, Protocol
protocol{_counted = Map.insert (opener protocol) index protocol._counted})
      where
        index :: Int
        index :: Int
index = Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
1 (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> Map Int Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Protocol -> Int
opener Protocol
protocol) Protocol
protocol._counted)
    taking :: Int -> String -> Expression -> Protocol -> IO (Protocol, Maybe String)
    taking :: Int
-> String -> Expression -> Protocol -> IO (Protocol, Maybe String)
taking Int
at String
word Expression
term Protocol
protocol = do
      let (Int
index, Protocol
counted) = Protocol -> (Int, Protocol)
numbered Protocol
protocol
      String
taken <- Expression -> IO String
printed (Named Expression -> Expression -> Expression
abbreviatedInside Protocol
protocol._made Expression
term)
      (Protocol, Maybe String) -> IO (Protocol, Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Protocol
counted{_made = namedInsert term (alias (opener protocol) index) counted._made}, String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String -> String
indented Int
at (String -> String -> String -> Int -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s %s·%d := %s" String
word (Protocol -> Text -> String
labelled Protocol
protocol Text
answer) Int
index String
taken)))

endEval :: Handle -> IORef Protocol -> Double -> IO ()
endEval :: Handle -> IORef Protocol -> Double -> IO ()
endEval Handle
handle IORef Protocol
cursor Double
began = do
  Protocol
protocol <- IORef Protocol -> IO Protocol
forall a. IORef a -> IO a
readIORef IORef Protocol
cursor
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Protocol
protocol._begun (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    Double
now <- IO Double
getMonotonicTime
    let taken :: Int
taken = Double -> Double -> Int
milliseconds Double
began Double
now
    Handle -> String -> IO ()
hPutStrLn Handle
handle (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"msec %d" Int
taken)
    Handle -> String -> IO ()
hPutStrLn Handle
handle (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"firings %d" Protocol
protocol._fired)
    Handle -> String -> IO ()
hPutStrLn Handle
handle (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"fps %d" (Int -> Int -> Int
perSecond Protocol
protocol._fired Int
taken))

milliseconds :: Double -> Double -> Int
milliseconds :: Double -> Double -> Int
milliseconds Double
began Double
now = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
round ((Double
now Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
began) Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
1000)

perSecond :: Int -> Int -> Int
perSecond :: Int -> Int -> Int
perSecond Int
firings Int
taken = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
round (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
firings Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
1000 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
1 Int
taken) :: Double)

saveEvalXml :: Handle -> IORef Nesting -> (Expression -> IO String) -> SaveEvalFunc
saveEvalXml :: Handle
-> IORef Nesting -> (Expression -> IO String) -> SaveEvalFunc
saveEvalXml Handle
handle IORef Nesting
cursor Expression -> IO String
printed Evaluation
report = do
  [String]
written <- IORef Nesting -> (Nesting -> IO (Nesting, [String])) -> IO [String]
forall a b. IORef a -> (a -> IO (a, b)) -> IO b
atomicModify IORef Nesting
cursor (Nesting -> IO (Nesting, [String])
flushed (Nesting -> IO (Nesting, [String]))
-> (Nesting -> Nesting) -> Nesting -> IO (Nesting, [String])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Evaluation -> Nesting -> Nesting
beside (Evaluation -> Int
tier Evaluation
report) Evaluation
report (Nesting -> Nesting) -> (Nesting -> Nesting) -> Nesting -> Nesting
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nesting -> Nesting
outer (Evaluation -> Int
tier Evaluation
report) (Nesting -> IO (Nesting, [String]))
-> ((Nesting, [String]) -> IO (Nesting, [String]))
-> Nesting
-> IO (Nesting, [String])
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Int -> (Nesting, [String]) -> IO (Nesting, [String])
opened' (Evaluation -> Int
tier Evaluation
report))
  (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Handle -> String -> IO ()
hPutStrLn Handle
handle) [String]
written
  String -> IO ()
logDebug (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"Saved %d line(s) of the XML protocol" ([String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
written))
  where
    opened' :: Int -> (Nesting, [String]) -> IO (Nesting, [String])
    opened' :: Int -> (Nesting, [String]) -> IO (Nesting, [String])
opened' Int
at (Nesting
nesting, [String]
openings) = (Nesting -> Nesting)
-> ([String] -> [String])
-> (Nesting, [String])
-> (Nesting, [String])
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Evaluation -> Nesting -> Nesting
forgotten Evaluation
report) ([String]
openings [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++) ((Nesting, [String]) -> (Nesting, [String]))
-> IO (Nesting, [String]) -> IO (Nesting, [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Evaluation -> Nesting -> IO (Nesting, [String])
elements Int
at Evaluation
report Nesting
nesting
    beside :: Int -> Evaluation -> Nesting -> Nesting
    beside :: Int -> Evaluation -> Nesting -> Nesting
beside Int
_ EvStarted{} Nesting
nesting = Nesting
nesting
    beside Int
_ EvBound{} Nesting
nesting = Nesting
nesting
    beside Int
at Evaluation
_ Nesting
nesting = Nesting
nesting{_heads = dropWhile ((>= at) . fst) nesting._heads, _pending = dropWhile (\(Int
level, Judgment
_, Expression
_) -> Int
level Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
at) nesting._pending}
    flushed :: Nesting -> IO (Nesting, [String])
    flushed :: Nesting -> IO (Nesting, [String])
flushed Nesting
nesting
      | Evaluation -> Bool
silent Evaluation
report = (Nesting, [String]) -> IO (Nesting, [String])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nesting
nesting, [])
      | Bool
otherwise = ((Nesting, [String])
 -> (Int, Judgment, Expression) -> IO (Nesting, [String]))
-> (Nesting, [String])
-> [(Int, Judgment, Expression)]
-> IO (Nesting, [String])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Nesting, [String])
-> (Int, Judgment, Expression) -> IO (Nesting, [String])
pended (Nesting
nesting{_pending = []}, []) ([(Int, Judgment, Expression)] -> [(Int, Judgment, Expression)]
forall a. [a] -> [a]
reverse Nesting
nesting._pending)
    pended :: (Nesting, [String]) -> (Int, Judgment, Expression) -> IO (Nesting, [String])
    pended :: (Nesting, [String])
-> (Int, Judgment, Expression) -> IO (Nesting, [String])
pended (Nesting
nesting, [String]
openings) (Int
level, Judgment
judgment, Expression
site) = do
      (Nesting
nesting', [String]
lines') <- Int -> Nesting -> Naming String -> IO (Nesting, [String])
staged Int
level Nesting
nesting (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<%s at=\"%s\">" (Judgment -> String
opened Judgment
judgment) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXML (String -> String) -> Naming String -> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
located Int
level Expression
site)
      (Nesting, [String]) -> IO (Nesting, [String])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nesting
nesting'{_closing = (level, opened judgment) : nesting'._closing}, [String]
openings [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
lines')
    silent :: Evaluation -> Bool
    silent :: Evaluation -> Bool
silent EvStarted{} = Bool
True
    silent EvWorld{} = Bool
True
    silent EvBound{} = Bool
True
    silent Evaluation
_ = Bool
False
    forgotten :: Evaluation -> Nesting -> Nesting
    forgotten :: Evaluation -> Nesting -> Nesting
forgotten EvBound{} Nesting
nesting = Nesting
nesting
    forgotten EvDelta{} Nesting
nesting = Nesting
nesting
    forgotten EvManufactured{} Nesting
nesting = Nesting
nesting
    forgotten EvWorld{} Nesting
nesting = Nesting
nesting
    forgotten Evaluation
_ Nesting
nesting = Nesting
nesting{_held = Nothing}
    staged :: Int -> Nesting -> Naming String -> IO (Nesting, [String])
    staged :: Int -> Nesting -> Naming String -> IO (Nesting, [String])
staged Int
depth Nesting
nesting Naming String
naming = do
      (String
element, (Nesting
nesting', [String]
records)) <- Naming String
-> (Nesting, [String]) -> IO (String, (Nesting, [String]))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Naming String
naming (Nesting
nesting, [])
      (Nesting, [String]) -> IO (Nesting, [String])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nesting
nesting', (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> String -> String
indentedXml Int
depth) ([String] -> [String]
forall a. [a] -> [a]
reverse (String
element String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
records)))
    placed :: Int -> Nesting -> Naming String -> IO (Nesting, [String])
    placed :: Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
depth Nesting
nesting Naming String
naming = ([String] -> [String])
-> (Nesting, [String]) -> (Nesting, [String])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([String]
closers [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++) ((Nesting, [String]) -> (Nesting, [String]))
-> IO (Nesting, [String]) -> IO (Nesting, [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Nesting -> Naming String -> IO (Nesting, [String])
staged Int
depth Nesting
nesting{_closing = kept} Naming String
naming
      where
        ([(Int, String)]
kept, [String]
closers) = Int -> [(Int, String)] -> ([(Int, String)], [String])
closed Int
depth Nesting
nesting._closing
    elements :: Int -> Evaluation -> Nesting -> IO (Nesting, [String])
    elements :: Int -> Evaluation -> Nesting -> IO (Nesting, [String])
elements Int
_ (EvRun Judgment
judgment Text
locator) Nesting
nesting =
      (Nesting, [String]) -> IO (Nesting, [String])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( Nesting
nesting{_closing = (0, opened judgment) : rooted kept}
        , Nesting -> [String]
prologue Nesting
nesting [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
closers [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
run]
        )
      where
        ([(Int, String)]
kept, [String]
closers) = Int -> [(Int, String)] -> ([(Int, String)], [String])
closed Int
0 Nesting
nesting._closing
        run :: String
        run :: String
run = Int -> String -> String
indentedXml Int
0 (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<%s at=\"%s\">" (Judgment -> String
opened Judgment
judgment) (Text -> String
quoted Text
locator))
    elements Int
_ (EvHeader (Header String
release Maybe String
revision ZonedTime
dated [String]
command (World Maybe String
file Int
count Int
size Int
tops Int
bindings) Maybe (String, Int)
table) Expression
locator Expression
_) Nesting
nesting = do
      String
place <- Expression -> IO String
printed Expression
locator
      (Nesting, [String]) -> IO (Nesting, [String])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( Nesting
nesting{_closing = rooted nesting._closing}
        , Nesting -> [String]
prologue Nesting
nesting
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map
              (Int -> String -> String
indentedXml Int
0)
              ( [ String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<written by=\"phino\" version=\"%s\"%s on=\"%s\"/>" (String -> String
escapeXML String
release) (String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String -> String -> String
forall r. PrintfType r => String -> r
printf String
" revision=\"%s\"" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXML) Maybe String
revision :: String) (TimeLocale -> String -> ZonedTime -> String
forall t. FormatTime t => TimeLocale -> String -> t -> String
formatTime TimeLocale
defaultTimeLocale String
"%Y-%m-%dT%H:%M:%S%Ez" ZonedTime
dated)
                , String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<command>%s</command>" (String -> String
escapeXMLText ([String] -> String
commanded [String]
command))
                , String -> String -> Int -> Int -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"<world%s lines=\"%d\" bytes=\"%d\" objects=\"%d\" bindings=\"%d\"/>" (String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String -> String -> String
forall r. PrintfType r => String -> r
printf String
" file=\"%s\"" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXML) Maybe String
file :: String) Int
count Int
size Int
tops Int
bindings
                ]
                  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"<symbolic file=\"%s\" entries=\"%d\"/>" (String -> String
escapeXML String
path) Int
entries | Just (String
path, Int
entries) <- [Maybe (String, Int)
table]]
                  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<locator>%s</locator>" (String -> String
escapeXMLText String
place)]
              )
        )
    elements Int
at (EvFiring Int
depth Text
key Judgment
judgment Expression
site) Nesting
nesting = do
      (Nesting
fired, [String]
lines') <- Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<evaluate λ=\"%s\" by=\"%s\" at=\"%s\">" (Text -> String
quoted Text
key) (Judgment -> String
opened Judgment
judgment) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXML (String -> String) -> Naming String -> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
located Int
depth Expression
site)
      (Nesting, [String]) -> IO (Nesting, [String])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nesting
fired{_fires = fired._fires + 1, _openedAt = (depth, fired._fires + 1) : fired._openedAt, _closing = (at, "evaluate") : fired._closing}, [String]
lines')
    elements Int
at (EvStarted Int
_ Judgment
judgment Expression
site) Nesting
nesting =
      (Nesting, [String]) -> IO (Nesting, [String])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Nesting, [String]) -> IO (Nesting, [String]))
-> (Nesting, [String]) -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ case [(Int, (Judgment, Expression))]
inner of
        (Int
level, (Judgment, Expression)
opening) : [(Int, (Judgment, Expression))]
_ | Int
level Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
at Bool -> Bool -> Bool
&& (Judgment, Expression)
opening (Judgment, Expression) -> (Judgment, Expression) -> Bool
forall a. Eq a => a -> a -> Bool
== (Judgment
judgment, Expression
site) -> (Nesting
nesting{_heads = inner, _pending = pending}, [])
        [(Int, (Judgment, Expression))]
_ -> (Nesting
nesting{_heads = (at, (judgment, site)) : dropWhile ((>= at) . fst) inner, _pending = (at, judgment, site) : dropWhile (\(Int
level, Judgment
_, Expression
_) -> Int
level Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
at) pending, _closing = kept}, [String]
closers)
      where
        inner :: [(Int, (Judgment, Expression))]
        inner :: [(Int, (Judgment, Expression))]
inner = ((Int, (Judgment, Expression)) -> Bool)
-> [(Int, (Judgment, Expression))]
-> [(Int, (Judgment, Expression))]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
at) (Int -> Bool)
-> ((Int, (Judgment, Expression)) -> Int)
-> (Int, (Judgment, Expression))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (Judgment, Expression)) -> Int
forall a b. (a, b) -> a
fst) Nesting
nesting._heads
        pending :: [(Int, Judgment, Expression)]
        pending :: [(Int, Judgment, Expression)]
pending = ((Int, Judgment, Expression) -> Bool)
-> [(Int, Judgment, Expression)] -> [(Int, Judgment, Expression)]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (\(Int
level, Judgment
_, Expression
_) -> Int
level Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
at) Nesting
nesting._pending
        ([(Int, String)]
kept, [String]
closers) = Int -> [(Int, String)] -> ([(Int, String)], [String])
closed Int
at Nesting
nesting._closing
    elements Int
at (EvLooped Int
depth Judgment
judgment Acyclic
mode Expression
self Expression
site Maybe (Int, Expression)
Nothing) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ do
        String
locator <- Int -> Expression -> Naming String
located Int
depth Expression
site
        (String, String)
origin <- Int -> Expression -> Naming (String, String)
sole Int
depth Expression
self
        String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> (String, String) -> String
enclosed String
"looped" (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<looped by=\"%s\" match=\"%s\" at=\"%s\"" (Judgment -> String
opened Judgment
judgment) (Acyclic -> String
certainty Acyclic
mode) (String -> String
escapeXML String
locator)) (String, String)
origin)
    elements Int
at (EvLooped Int
depth Judgment
judgment Acyclic
mode Expression
self Expression
site (Just (Int
symbol, Expression
call))) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ do
        String
locator <- Int -> Expression -> Naming String
located Int
depth Expression
site
        String
origin <- Int -> Expression -> Naming String
leaf Int
depth Expression
self
        (String
object, String
given) <- Int -> Expression -> Naming (String, String)
called Int
depth Expression
call
        String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
-> String
-> String
-> String
-> String
-> String
-> String
-> String
-> String
forall r. PrintfType r => String -> r
printf String
"<looped symbol=\"%s\" by=\"%s\" match=\"%s\" at=\"%s\" of=\"%s\" object=\"%s\">%s</looped>" (Int -> String
sigma Int
symbol) (Judgment -> String
opened Judgment
judgment) (Acyclic -> String
certainty Acyclic
mode) (String -> String
escapeXML String
locator) (String -> String
escapeXML String
origin) (String -> String
escapeXML String
object) String
given)
    elements Int
at (EvStuck Int
depth Text
key Judgment
judgment Expression
self) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<unanswered λ=\"%s\" by=\"%s\">%s</unanswered>" (Text -> String
quoted Text
key) (Judgment -> String
opened Judgment
judgment) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXMLText (String -> String) -> Naming String -> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
leaf Int
depth Expression
self)
    elements Int
at (EvStall Int
_ Text
key) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<stalled λ=\"%s\"/>" (Text -> String
quoted Text
key)))
    elements Int
at (EvStuckOn Int
_ Text
key) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<stuck λ=\"%s\"/>" (Text -> String
quoted Text
key)))
    elements Int
at (EvStarved Int
depth Int
limit Judgment
judgment Expression
site) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> Int -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<starved limit=\"%d\" by=\"%s\" at=\"%s\"/>" Int
limit (Judgment -> String
opened Judgment
judgment) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXML (String -> String) -> Naming String -> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
located Int
depth Expression
site)
    elements Int
at (EvTimeout Int
depth Int
limit Judgment
judgment Expression
site) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> Int -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<timeout limit=\"%d\" by=\"%s\" at=\"%s\"/>" Int
limit (Judgment -> String
opened Judgment
judgment) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXML (String -> String) -> Naming String -> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
located Int
depth Expression
site)
    elements Int
at (EvSpent Int
depth Int
limit Judgment
judgment Expression
site) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> Int -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<spent limit=\"%d\" by=\"%s\" at=\"%s\"/>" Int
limit (Judgment -> String
opened Judgment
judgment) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXML (String -> String) -> Naming String -> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
located Int
depth Expression
site)
    elements Int
at (EvDelta Int
_ Bytes
bytes) Nesting
nesting = do
      String
datum <- Expression -> IO String
printed (Bytes -> Expression
ExBytes Bytes
bytes)
      let (String
naming, Nesting
nesting') = Either Int Bytes -> Nesting -> (String, Nesting)
stored (Bytes -> Either Int Bytes
forall a b. b -> Either a b
Right Bytes
bytes) Nesting
nesting
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting' (String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<dataized meta=\"%s\"%s>%s</dataized>" (String -> String
escapeXML String
naming) (String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String -> String -> String
forall r. PrintfType r => String -> r
printf String
" number=\"%s\"" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXML) (Bytes -> Maybe String
ieee Bytes
bytes) :: String) (String -> String
escapeXMLText String
datum)))
    elements Int
at (EvManufactured Int
_ Int
symbol) Nesting
nesting = Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting' (String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<manufactured meta=\"%s\">%s</manufactured>" (String -> String
escapeXML String
naming) (Int -> String
sigma Int
symbol)))
      where
        (String
naming, Nesting
nesting') = Either Int Bytes -> Nesting -> (String, Nesting)
stored (Int -> Either Int Bytes
forall a b. a -> Either a b
Left Int
symbol) Nesting
nesting
    elements Int
at (EvBoxed Int
depth Expression
term) Nesting
nesting = Int
-> String -> Int -> Expression -> Nesting -> IO (Nesting, [String])
taken Int
at String
"boxed" Int
depth Expression
term Nesting
nesting
    elements Int
at (EvUndressed Int
depth Expression
term) Nesting
nesting = Int
-> String -> Int -> Expression -> Nesting -> IO (Nesting, [String])
taken Int
at String
"undressed" Int
depth Expression
term Nesting
nesting
    elements Int
at (EvData Int
_ Text
spelling Expression
_ Either Int Bytes
value) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ case (Either Int Bytes
-> Maybe (Either Int Bytes, String) -> Maybe String
found Either Int Bytes
value Nesting
nesting._held, Either Int Bytes
value) of
        (Just String
naming, Either Int Bytes
_) -> String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String
bound (String -> String
escapeXMLText String
naming))
        (Maybe String
Nothing, Left Int
symbol) -> String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String
bound (Int -> String
sigma Int
symbol))
        (Maybe String
Nothing, Right Bytes
bytes) -> String -> String
bound (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXMLText (String -> String) -> Naming String -> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Expression -> IO String
printed (Bytes -> Expression
ExBytes Bytes
bytes))
      where
        bound :: String -> String
        bound :: String -> String
bound = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<bound meta=\"%s\">%s</bound>" (String -> String
escapeXML (Nesting -> Text -> String
labelled Nesting
nesting Text
spelling))
    elements Int
at (EvTerm Int
depth Text
spelling Judgment
_ Expression
_ Expression
term) Nesting
nesting = Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Int -> Nesting -> Text -> Expression -> Naming String
bind Int
depth Nesting
nesting Text
spelling Expression
term)
    elements Int
_ (EvBound Int
_ Expression
meta Expression
term) Nesting
nesting = (Nesting, [String]) -> IO (Nesting, [String])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nesting
nesting{_unmarked = Map.alter (Just . namedInsert meta term . fromMaybe Map.empty) (opener nesting) nesting._unmarked}, [])
    elements Int
at (EvReshaped Int
depth Text
spelling Text
_ Expression
_ Expression
term) Nesting
nesting = Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Int -> Nesting -> Text -> Expression -> Naming String
bind Int
depth Nesting
nesting Text
spelling Expression
term)
    elements Int
at (EvSymbolized Int
_ Int
symbol Bytes
bytes) Nesting
nesting = do
      String
datum <- Expression -> IO String
printed (Bytes -> Expression
ExBytes Bytes
bytes)
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<symbolized symbol=\"%s\"%s>%s</symbolized>" (Int -> String
sigma Int
symbol) (String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String -> String -> String
forall r. PrintfType r => String -> r
printf String
" number=\"%s\"" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXML) (Bytes -> Maybe String
ieee Bytes
bytes) :: String) (String -> String
escapeXMLText String
datum)))
    elements Int
at (EvCast Int
depth Text
spelling Expression
source Expression
model Expression
term) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ do
        String
one <- Int -> Nesting -> Expression -> Naming String
spoken Int
depth Nesting
nesting Expression
source
        String
two <- Int -> Nesting -> Expression -> Naming String
spoken Int
depth Nesting
nesting Expression
model
        String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<cast meta=\"%s\" of=\"%s\" up-to=\"%s\">%s</cast>" (String -> String
escapeXML (Nesting -> Text -> String
labelled Nesting
nesting Text
spelling)) (String -> String
escapeXML String
one) (String -> String
escapeXML String
two) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXMLText (String -> String) -> Naming String -> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
leaf Int
depth Expression
term
    elements Int
at (EvMinted Int
_ Int
symbol [Either Int Bytes]
operands) Nesting
nesting = do
      [String]
spelledOperands <- (Either Int Bytes -> IO String)
-> [Either Int Bytes] -> IO [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Either Int Bytes -> IO String
spelled' [Either Int Bytes]
operands
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([String] -> String
minted [String]
spelledOperands))
      where
        spelled' :: Either Int Bytes -> IO String
        spelled' :: Either Int Bytes -> IO String
spelled' (Left Int
fresh') = String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> String
sigma Int
fresh')
        spelled' (Right Bytes
bytes) = Expression -> IO String
printed (Bytes -> Expression
ExBytes Bytes
bytes)
        minted :: [String] -> String
        minted :: [String] -> String
minted [] = String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<minted symbol=\"%s\"/>" (Int -> String
sigma Int
symbol)
        minted [String]
spelt = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<minted symbol=\"%s\">%s</minted>" (Int -> String
sigma Int
symbol) (String -> String
escapeXMLText ([String] -> String
unwords [String]
spelt))
    elements Int
at (EvDeferred Int
depth Int
symbol Judgment
judgment Expression
copy Maybe Expression
call Expression
site) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ do
        String
locator <- Int -> Expression -> Naming String
located Int
depth Expression
site
        (String, String)
origin <- Naming (String, String)
-> (Expression -> Naming (String, String))
-> Maybe Expression
-> Naming (String, String)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Int -> Expression -> Naming (String, String)
sole Int
depth Expression
copy) (Int -> Expression -> Naming (String, String)
called Int
depth) Maybe Expression
call
        String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> (String, String) -> String
enclosed String
"deferred" (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<deferred symbol=\"%s\" by=\"%s\" at=\"%s\"" (Int -> String
sigma Int
symbol) (Judgment -> String
opened Judgment
judgment) (String -> String
escapeXML String
locator)) (String, String)
origin)
    elements Int
at (EvApplied Int
depth Judgment
judgment Expression
call Expression
object Expression
site) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ do
        String
locator <- Int -> Expression -> Naming String
located Int
depth Expression
site
        (String
origin, String
given) <- Int -> Expression -> Naming (String, String)
parted Int
depth Expression
call
        (String
naming, Expression
aliased) <- Naming (String, Expression)
counted
        ((Nesting, [String]) -> (Nesting, [String]))
-> StateT (Nesting, [String]) IO ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify ((Nesting -> Nesting)
-> ([String] -> [String])
-> (Nesting, [String])
-> (Nesting, [String])
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (\Nesting
nesting' -> Nesting
nesting'{_objects = namedInsert call aliased nesting'._objects}) (String -> String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<applied meta=\"%s\" by=\"%s\" at=\"%s\" of=\"%s\">%s</applied>" (String -> String
escapeXML String
naming) (Judgment -> String
opened Judgment
judgment) (String -> String
escapeXML String
locator) (String -> String
escapeXML String
origin) String
given String -> [String] -> [String]
forall a. a -> [a] -> [a]
:))
        String -> String
element <- Int -> Expression -> Naming (String -> String)
made Int
depth Expression
object
        (String
naming', Expression
aliased') <- Naming (String, Expression)
counted
        ((Nesting, [String]) -> (Nesting, [String]))
-> StateT (Nesting, [String]) IO ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify ((Nesting -> Nesting) -> (Nesting, [String]) -> (Nesting, [String])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\Nesting
nesting' -> Nesting
nesting'{_objects = namedInsert object aliased' nesting'._objects}))
        String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String
element (String -> String
escapeXML String
naming'))
    elements Int
at (EvBuilt Int
depth Expression
term) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ do
        String
body <- Int -> Expression -> Naming String
leaf Int
depth Expression
term
        (String
naming, Expression
_) <- Naming (String, Expression)
counted
        ((Nesting, [String]) -> (Nesting, [String]))
-> StateT (Nesting, [String]) IO ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify ((Nesting -> Nesting) -> (Nesting, [String]) -> (Nesting, [String])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\Nesting
nesting' -> Nesting
nesting'{_sources = (depth, term, naming) : nesting'._sources}))
        String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<built meta=\"%s\">%s</built>" (String -> String
escapeXML String
naming) (String -> String
escapeXMLText String
body))
    elements Int
at (EvAnswer Int
depth Expression
term) Nesting
nesting = Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> Int -> Expression -> Naming String
concluded String
"answered" Int
depth Expression
term)
    elements Int
at (EvMorphed Int
depth Expression
term) Nesting
nesting = Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> Int -> Expression -> Naming String
concluded String
"morphed" Int
depth Expression
term)
    elements Int
at (EvJoined Int
depth Either Text Expression
condition Int
symbol (Int
left, Int
right) Maybe Int
bottom Maybe Expression
raised) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ do
        String
on <- (Text -> Naming String)
-> (Expression -> Naming String)
-> Either Text Expression
-> Naming String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Naming String)
-> (Text -> String) -> Text -> Naming String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nesting -> Text -> String
labelled Nesting
nesting) (IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO String -> Naming String)
-> (Expression -> IO String) -> Expression -> Naming String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression -> IO String
traced) Either Text Expression
condition
        [String]
raiser <- (Expression -> Naming String)
-> [Expression] -> StateT (Nesting, [String]) IO [String]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Int -> Expression -> Naming String
leaf Int
depth) [Expression
term | Just Int
idx <- [Maybe Int
bottom], Int
idx Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int
left, Int
right], Just Expression
term <- [Maybe Expression
raised]]
        String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
-> String
-> String
-> String
-> String
-> String
-> String
-> String
forall r. PrintfType r => String -> r
printf String
"<joined symbol=\"%s\" on=\"%s\" left=\"%s\" right=\"%s\"%s%s/>" (Int -> String
sigma Int
symbol) (String -> String
escapeXML String
on) (Int -> String
sigma Int
left) (Int -> String
sigma Int
right) ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String -> String -> String
forall r. PrintfType r => String -> r
printf String
" terminator=\"%s\"" (Int -> String
sigma Int
idx) :: String | Just Int
idx <- [Maybe Int
bottom], Int
idx Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int
left, Int
right]]) ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String -> String -> String
forall r. PrintfType r => String -> r
printf String
" raised=\"%s\"" (String -> String
escapeXML String
name) :: String | String
name <- [String]
raiser]))
    elements Int
at (EvDiverged Int
depth (Expression, Expression)
left (Expression, Expression)
right [Attribute]
path Refusal
refusal) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ do
        String
one <- Int -> Nesting -> (Expression, Expression) -> Naming String
sided Int
depth Nesting
nesting (Expression, Expression)
left
        String
two <- Int -> Nesting -> (Expression, Expression) -> Naming String
sided Int
depth Nesting
nesting (Expression, Expression)
right
        [String]
places <- ((String, Expression) -> Naming String)
-> [(String, Expression)] -> StateT (Nesting, [String]) IO [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((String -> Expression -> Naming String)
-> (String, Expression) -> Naming String
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Int -> [Attribute] -> String -> Expression -> Naming String
lodging Int
depth [Attribute]
path)) [(String
"left", (Expression, Expression) -> Expression
forall a b. (a, b) -> b
snd (Expression, Expression)
left), (String
"right", (Expression, Expression) -> Expression
forall a b. (a, b) -> b
snd (Expression, Expression)
right)]
        String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<diverged left=\"%s\" right=\"%s\"%s reason=\"%s\">%s</diverged>" (String -> String
escapeXML String
one) (String -> String
escapeXML String
two) (if [Attribute] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Attribute]
path then String
"" else String -> String -> String
forall r. PrintfType r => String -> r
printf String
" at=\"%s\"" (String -> String
escapeXML ([Attribute] -> String
dotted [Attribute]
path)) :: String) (String -> String
escapeXML (Refusal -> String
refused Refusal
refusal)) ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
places))
    elements Int
at (EvUnripe Int
depth (Expression, Expression)
left (Expression, Expression)
right Side
_ Attribute
attr) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ do
        String
one <- Int -> Nesting -> (Expression, Expression) -> Naming String
sided Int
depth Nesting
nesting (Expression, Expression)
left
        String
two <- Int -> Nesting -> (Expression, Expression) -> Naming String
sided Int
depth Nesting
nesting (Expression, Expression)
right
        String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<unripe left=\"%s\" right=\"%s\" at=\"%s\"/>" (String -> String
escapeXML String
one) (String -> String
escapeXML String
two) (String -> String
escapeXML (Attribute -> String
printAttribute Attribute
attr)))
    elements Int
at (EvFabricated Int
depth (Expression, Expression)
left (Expression, Expression)
right Expression
term) Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ do
        String
one <- Int -> Nesting -> (Expression, Expression) -> Naming String
sided Int
depth Nesting
nesting (Expression, Expression)
left
        String
two <- Int -> Nesting -> (Expression, Expression) -> Naming String
sided Int
depth Nesting
nesting (Expression, Expression)
right
        String
body <- Int -> Expression -> Naming String
leaf Int
depth Expression
term
        (String
naming, Expression
_) <- Naming (String, Expression)
counted
        String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<fabricated meta=\"%s\" left=\"%s\" right=\"%s\">%s</fabricated>" (String -> String
escapeXML String
naming) (String -> String
escapeXML String
one) (String -> String
escapeXML String
two) (String -> String
escapeXMLText String
body))
    elements Int
at (EvTaken Int
depth Expression
term) Nesting
nesting = Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (String -> Int -> Expression -> Naming String
concluded String
"answered" Int
depth Expression
term)
    elements Int
_ (EvWorld Expression
world) Nesting
nesting = (Nesting, [String]) -> IO (Nesting, [String])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Nesting -> Nesting
known Expression
world Nesting
nesting, [])
    prologue :: Nesting -> [String]
    prologue :: Nesting -> [String]
prologue Nesting
nesting
      | [(Int, String)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Nesting
nesting._closing = [String
"<?xml version=\"1.0\" encoding=\"UTF-8\"?>", String
"<protocol>"]
      | Bool
otherwise = []
    rooted :: [(Int, String)] -> [(Int, String)]
    rooted :: [(Int, String)] -> [(Int, String)]
rooted [] = [(-Int
1, String
"protocol")]
    rooted [(Int, String)]
open = [(Int, String)]
open
    sided :: Int -> Nesting -> (Expression, Expression) -> Naming String
    sided :: Int -> Nesting -> (Expression, Expression) -> Naming String
sided Int
depth Nesting
_ (Expression
_, term :: Expression
term@(ExFormation [BiLambda (FnSymbol Int
_)])) = Int -> Expression -> Naming String
leaf Int
depth Expression
term
    sided Int
depth Nesting
nesting (side :: Expression
side@(ExMeta Text
_), Expression
_) = Int -> Nesting -> Expression -> Naming String
spoken Int
depth Nesting
nesting Expression
side
    sided Int
depth Nesting
_ (Expression
_, Expression
term) = Int -> Expression -> Naming String
leaf Int
depth Expression
term
    spoken :: Int -> Nesting -> Expression -> Naming String
    spoken :: Int -> Nesting -> Expression -> Naming String
spoken Int
depth Nesting
nesting Expression
meta = Naming String
-> (Expression -> Naming String)
-> Maybe Expression
-> Naming String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Nesting -> Text -> String
labelled Nesting
nesting (Text -> String) -> (String -> Text) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack (String -> String) -> Naming String -> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Expression -> IO String
spelled Expression
meta)) (Int -> Expression -> Naming String
leaf Int
depth) (Expression -> Named Expression -> Maybe Expression
forall a. Expression -> Named a -> Maybe a
namedLookup Expression
meta (Nesting -> Named Expression
held Nesting
nesting))
    held :: Nesting -> Named Expression
    held :: Nesting -> Named Expression
held Nesting
nesting = Named Expression
-> Int -> Map Int (Named Expression) -> Named Expression
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Named Expression
forall k a. Map k a
Map.empty (Nesting -> Int
opener Nesting
nesting) Nesting
nesting._unmarked
    outer :: Int -> Nesting -> Nesting
    outer :: Int -> Nesting -> Nesting
outer Int
depth Nesting
nesting = Nesting
nesting{_openedAt = dropWhile ((>= depth) . fst) nesting._openedAt, _sources = dropWhile (\(Int
level, Expression
_, String
_) -> Int
level Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
depth) nesting._sources, _unmarked = foldr (Map.delete . snd) nesting._unmarked (takeWhile ((>= depth) . fst) nesting._openedAt)}
    labelled :: Nesting -> T.Text -> String
    labelled :: Nesting -> Text -> String
labelled Nesting
nesting Text
spelling = String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d" (Text -> String
T.unpack Text
spelling) (Nesting -> Int
opener Nesting
nesting)
    stored :: Either Int Bytes -> Nesting -> (String, Nesting)
    stored :: Either Int Bytes -> Nesting -> (String, Nesting)
stored Either Int Bytes
value Nesting
nesting = (String
naming, Nesting
nesting{_datums = Map.insert (opener nesting) index nesting._datums, _held = Just (value, naming)})
      where
        index :: Int
        index :: Int
index = Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
1 (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> Map Int Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Nesting -> Int
opener Nesting
nesting) Nesting
nesting._datums)
        naming :: String
        naming :: String
naming = String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d" (Nesting -> Text -> String
labelled Nesting
nesting Text
sigil) Int
index
    opener :: Nesting -> Int
    opener :: Nesting -> Int
opener Nesting
nesting = Int -> ((Int, Int) -> Int) -> Maybe (Int, Int) -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 (Int, Int) -> Int
forall a b. (a, b) -> b
snd ([(Int, Int)] -> Maybe (Int, Int)
forall a. [a] -> Maybe a
listToMaybe Nesting
nesting._openedAt)
    numbered :: Nesting -> (Int, Nesting)
    numbered :: Nesting -> (Int, Nesting)
numbered Nesting
nesting = (Int
index, Nesting
nesting{_numbered = Map.insert (opener nesting) index nesting._numbered})
      where
        index :: Int
        index :: Int
index = Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
1 (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> Map Int Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Nesting -> Int
opener Nesting
nesting) Nesting
nesting._numbered)
    counted :: Naming (String, Expression)
    counted :: Naming (String, Expression)
counted = do
      (Nesting
nesting, [String]
records) <- StateT (Nesting, [String]) IO (Nesting, [String])
forall (m :: * -> *) s. Monad m => StateT s m s
get
      let (Int
index, Nesting
nesting') = Nesting -> (Int, Nesting)
numbered Nesting
nesting
      (Nesting, [String]) -> StateT (Nesting, [String]) IO ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Nesting
nesting', [String]
records)
      (String, Expression) -> Naming (String, Expression)
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d" (Nesting -> Text -> String
labelled Nesting
nesting Text
answer) Int
index, Int -> Int -> Expression
alias (Nesting -> Int
opener Nesting
nesting) Int
index)
    recorded :: Expression -> (String -> String) -> Naming Expression
    recorded :: Expression -> (String -> String) -> Naming Expression
recorded Expression
term String -> String
element = do
      (Nesting
nesting, [String]
records) <- StateT (Nesting, [String]) IO (Nesting, [String])
forall (m :: * -> *) s. Monad m => StateT s m s
get
      let index :: Int
index = Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
1 (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> Map Int Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Nesting -> Int
opener Nesting
nesting) Nesting
nesting._parts)
          aliased :: Expression
aliased = Text -> Expression
ExMeta (String -> Text
T.pack (String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"e·%d·%d" (Nesting -> Int
opener Nesting
nesting) Int
index))
      (Nesting, [String]) -> StateT (Nesting, [String]) IO ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Nesting
nesting{_parts = Map.insert (opener nesting) index nesting._parts, _objects = namedInsert term aliased nesting._objects}, String -> String
element (String -> String
escapeXML (String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s·%d" (Nesting -> Text -> String
labelled Nesting
nesting Text
fragment) Int
index)) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
records)
      Expression -> Naming Expression
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
aliased
    opaque :: Expression -> Naming Expression
    opaque :: Expression -> Naming Expression
opaque Expression
term = do
      (Nesting
nesting, [String]
records) <- StateT (Nesting, [String]) IO (Nesting, [String])
forall (m :: * -> *) s. Monad m => StateT s m s
get
      let meta :: Expression
meta = Text -> Expression
ExMeta (String -> Text
T.pack (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"e%d" (Nesting
nesting._opaque Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)))
      (Nesting, [String]) -> StateT (Nesting, [String]) IO ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Nesting
nesting{_opaque = nesting._opaque + 1, _objects = namedInsert term meta nesting._objects}, [String]
records)
      Expression -> Naming Expression
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
meta
    located :: Int -> Expression -> Naming String
    located :: Int -> Expression -> Naming String
located Int
depth Expression
site = do
      (Nesting
nesting, [String]
_) <- StateT (Nesting, [String]) IO (Nesting, [String])
forall (m :: * -> *) s. Monad m => StateT s m s
get
      Naming String
-> (String -> Naming String) -> Maybe String -> Naming String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Int -> Expression -> Naming Expression
titled Int
depth (Named Expression -> Expression -> Expression
abbreviated (Nesting -> Named Expression
held Nesting
nesting) Expression
site) Naming Expression -> (Expression -> Naming String) -> Naming String
forall a b.
StateT (Nesting, [String]) IO a
-> (a -> StateT (Nesting, [String]) IO b)
-> StateT (Nesting, [String]) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO String -> Naming String)
-> (Expression -> IO String) -> Expression -> Naming String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression -> IO String
traced) String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe [String
naming | (Int
_, Expression
built, String
naming) <- Nesting
nesting._sources, Expression
built Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
site])
    taken :: Int -> String -> Int -> Expression -> Nesting -> IO (Nesting, [String])
    taken :: Int
-> String -> Int -> Expression -> Nesting -> IO (Nesting, [String])
taken Int
at String
tag Int
depth Expression
term Nesting
nesting =
      Int -> Nesting -> Naming String -> IO (Nesting, [String])
placed Int
at Nesting
nesting (Naming String -> IO (Nesting, [String]))
-> Naming String -> IO (Nesting, [String])
forall a b. (a -> b) -> a -> b
$ do
        String
body <- Int -> Expression -> Naming Expression
coined Int
depth Expression
term Naming Expression -> (Expression -> Naming String) -> Naming String
forall a b.
StateT (Nesting, [String]) IO a
-> (a -> StateT (Nesting, [String]) IO b)
-> StateT (Nesting, [String]) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO String -> Naming String)
-> (Expression -> IO String) -> Expression -> Naming String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression -> IO String
spelled
        (String
naming, Expression
aliased) <- Naming (String, Expression)
counted
        ((Nesting, [String]) -> (Nesting, [String]))
-> StateT (Nesting, [String]) IO ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify ((Nesting -> Nesting) -> (Nesting, [String]) -> (Nesting, [String])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\Nesting
nesting' -> Nesting
nesting'{_objects = namedInsert term aliased nesting'._objects}))
        String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<%s meta=\"%s\">%s</%s>" String
tag (String -> String
escapeXML String
naming) (String -> String
escapeXMLText String
body) String
tag)
    concluded :: String -> Int -> Expression -> Naming String
    concluded :: String -> Int -> Expression -> Naming String
concluded String
tag Int
depth Expression
term = do
      String
body <- Int -> Expression -> Naming String
leaf Int
depth Expression
term
      (String
naming, Expression
aliased) <- Naming (String, Expression)
counted
      ((Nesting, [String]) -> (Nesting, [String]))
-> StateT (Nesting, [String]) IO ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify ((Nesting -> Nesting) -> (Nesting, [String]) -> (Nesting, [String])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\Nesting
nesting -> Nesting
nesting{_objects = namedFormation term aliased nesting._objects}))
      String -> Naming String
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<%s meta=\"%s\">%s</%s>" String
tag (String -> String
escapeXML String
naming) (String -> String
escapeXMLText String
body) String
tag)
    bind :: Int -> Nesting -> T.Text -> Expression -> Naming String
    bind :: Int -> Nesting -> Text -> Expression -> Naming String
bind Int
depth Nesting
nesting Text
spelling Expression
term = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<bound meta=\"%s\">%s</bound>" (String -> String
escapeXML (Nesting -> Text -> String
labelled Nesting
nesting Text
spelling)) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXMLText (String -> String) -> Naming String -> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
leaf Int
depth Expression
term
    leaf :: Int -> Expression -> Naming String
    leaf :: Int -> Expression -> Naming String
leaf Int
depth Expression
term = Int -> Expression -> Naming Expression
titled Int
depth Expression
term Naming Expression -> (Expression -> Naming String) -> Naming String
forall a b.
StateT (Nesting, [String]) IO a
-> (a -> StateT (Nesting, [String]) IO b)
-> StateT (Nesting, [String]) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO String -> Naming String)
-> (Expression -> IO String) -> Expression -> Naming String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression -> IO String
spelled
    titled :: Int -> Expression -> Naming Expression
    titled :: Int -> Expression -> Naming Expression
titled Int
depth Expression
term = do
      (Nesting
nesting, [String]
_) <- StateT (Nesting, [String]) IO (Nesting, [String])
forall (m :: * -> *) s. Monad m => StateT s m s
get
      Naming Expression
-> (Expression -> Naming Expression)
-> Maybe Expression
-> Naming Expression
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Int -> Expression -> Naming Expression
coined Int
depth Expression
term) Expression -> Naming Expression
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Named Expression -> Maybe Expression
forall a. Expression -> Named a -> Maybe a
namedLookup Expression
term Nesting
nesting._objects)
    coined :: Int -> Expression -> Naming Expression
    coined :: Int -> Expression -> Naming Expression
coined Int
_ term :: Expression
term@(ExFormation [BiLambda (FnSymbol Int
_)]) = Expression -> Naming Expression
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
term
    coined Int
_ term :: Expression
term@(ExFormation [BiDelta Bytes
_]) = Expression -> Naming Expression
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
term
    coined Int
depth term :: Expression
term@(ExFormation [Binding]
bds) = do
      (Nesting
nesting, [String]
_) <- StateT (Nesting, [String]) IO (Nesting, [String])
forall (m :: * -> *) s. Monad m => StateT s m s
get
      case Nesting
-> [Binding] -> Maybe (Expression, [(Attribute, Expression)])
copied Nesting
nesting [Binding]
bds of
        Just (Expression
origin, []) -> do
          Expression
path <- Int -> Expression -> Naming Expression
titled Int
depth Expression
origin
          ((Nesting, [String]) -> (Nesting, [String]))
-> StateT (Nesting, [String]) IO ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify ((Nesting -> Nesting) -> (Nesting, [String]) -> (Nesting, [String])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (\Nesting
nesting' -> Nesting
nesting'{_objects = namedInsert term path nesting'._objects}))
          Expression -> Naming Expression
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
path
        Maybe (Expression, [(Attribute, Expression)])
copy -> Naming (String -> String)
-> ((Expression, [(Attribute, Expression)])
    -> Naming (String -> String))
-> Maybe (Expression, [(Attribute, Expression)])
-> Naming (String -> String)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Int -> [Binding] -> Naming (String -> String)
anonymous Int
depth [Binding]
bds) (Int
-> (Expression, [(Attribute, Expression)])
-> Naming (String -> String)
cloned Int
depth) Maybe (Expression, [(Attribute, Expression)])
copy Naming (String -> String)
-> ((String -> String) -> Naming Expression) -> Naming Expression
forall a b.
StateT (Nesting, [String]) IO a
-> (a -> StateT (Nesting, [String]) IO b)
-> StateT (Nesting, [String]) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expression -> (String -> String) -> Naming Expression
recorded Expression
term
    coined Int
depth term :: Expression
term@(ExDispatch Expression
inner Attribute
attr) = do
      Expression
head' <- Int -> Expression -> Naming Expression
titled Int
depth Expression
inner
      if Expression -> Bool
pathed Expression
head' then Expression -> Naming Expression
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Attribute -> Expression
ExDispatch Expression
head' Attribute
attr) else Expression -> Naming Expression
opaque Expression
term
    coined Int
depth term :: Expression
term@(ExApplication Expression
_ Argument
_) = do
      (Nesting
nesting, [String]
_) <- StateT (Nesting, [String]) IO (Nesting, [String])
forall (m :: * -> *) s. Monad m => StateT s m s
get
      let (Expression
head', [Argument]
arguments) = Named Expression -> Expression -> (Expression, [Argument])
chained Nesting
nesting._objects Expression
term
      String
origin <- Int -> Expression -> Naming String
leaf Int
depth Expression
head'
      [String]
given <- (Argument -> Naming String)
-> [Argument] -> StateT (Nesting, [String]) IO [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Int -> Argument -> Naming String
argument Int
depth) [Argument]
arguments
      Expression -> (String -> String) -> Naming Expression
recorded Expression
term (\String
naming -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<applied meta=\"%s\" of=\"%s\">%s</applied>" String
naming (String -> String
escapeXML String
origin) ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
given))
    coined Int
_ Expression
term
      | Expression -> Bool
plain Expression
term = Expression -> Naming Expression
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
term
      | Bool
otherwise = Expression -> Naming Expression
opaque Expression
term
    made :: Int -> Expression -> Naming (String -> String)
    made :: Int -> Expression -> Naming (String -> String)
made Int
depth (ExFormation [Binding]
bds) = do
      (Nesting
nesting, [String]
_) <- StateT (Nesting, [String]) IO (Nesting, [String])
forall (m :: * -> *) s. Monad m => StateT s m s
get
      Naming (String -> String)
-> ((Expression, [(Attribute, Expression)])
    -> Naming (String -> String))
-> Maybe (Expression, [(Attribute, Expression)])
-> Naming (String -> String)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Int -> [Binding] -> Naming (String -> String)
anonymous Int
depth [Binding]
bds) (Int
-> (Expression, [(Attribute, Expression)])
-> Naming (String -> String)
cloned Int
depth) (Nesting
-> [Binding] -> Maybe (Expression, [(Attribute, Expression)])
copied Nesting
nesting [Binding]
bds)
    made Int
depth Expression
term = Int
-> (Expression, [(Attribute, Expression)])
-> Naming (String -> String)
cloned Int
depth (Expression
term, [])
    cloned :: Int -> (Expression, [(Attribute, Expression)]) -> Naming (String -> String)
    cloned :: Int
-> (Expression, [(Attribute, Expression)])
-> Naming (String -> String)
cloned Int
depth (Expression
origin, [(Attribute, Expression)]
bound) = do
      String
path <- Int -> Expression -> Naming String
leaf Int
depth Expression
origin
      [String]
given <- ((Attribute, Expression) -> Naming String)
-> [(Attribute, Expression)]
-> StateT (Nesting, [String]) IO [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Attribute
attr, Expression
value) -> Int -> Expression -> Naming Expression
titled Int
depth Expression
value Naming Expression -> (Expression -> Naming String) -> Naming String
forall a b.
StateT (Nesting, [String]) IO a
-> (a -> StateT (Nesting, [String]) IO b)
-> StateT (Nesting, [String]) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO String -> Naming String)
-> (Expression -> IO String) -> Expression -> Naming String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Expression -> IO String
attributed (Attribute -> String
printAttribute Attribute
attr)) [(Attribute, Expression)]
bound
      (String -> String) -> Naming (String -> String)
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (\String
naming -> String -> String -> (String, String) -> String
enclosed String
"formed" (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<formed meta=\"%s\"" String
naming) (String
path, [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
given))
    anonymous :: Int -> [Binding] -> Naming (String -> String)
    anonymous :: Int -> [Binding] -> Naming (String -> String)
anonymous Int
depth [Binding]
bds = do
      [Either String String]
parts <- (Binding -> StateT (Nesting, [String]) IO (Either String String))
-> [Binding]
-> StateT (Nesting, [String]) IO [Either String String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Int
-> Binding -> StateT (Nesting, [String]) IO (Either String String)
part Int
depth) [Binding]
bds
      (String -> String) -> Naming (String -> String)
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (\String
naming -> String -> String -> [Either String String] -> String
gathered String
"formed" (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"formed meta=\"%s\"" String
naming) [Either String String]
parts)
    lodging :: Int -> [Attribute] -> String -> Expression -> Naming String
    lodging :: Int -> [Attribute] -> String -> Expression -> Naming String
lodging Int
depth [] String
tag Expression
side = (\String
body -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<%s>%s</%s>" String
tag (String -> String
escapeXMLText String
body) String
tag) (String -> String) -> Naming String -> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
leaf Int
depth Expression
side
    lodging Int
depth [Attribute]
path String
tag Expression
side = String -> String -> [Either String String] -> String
gathered String
tag String
tag ([Either String String] -> String)
-> StateT (Nesting, [String]) IO [Either String String]
-> Naming String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Binding -> StateT (Nesting, [String]) IO (Either String String))
-> [Binding]
-> StateT (Nesting, [String]) IO [Either String String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Int
-> Binding -> StateT (Nesting, [String]) IO (Either String String)
part Int
depth) (Maybe Binding -> [Binding]
forall a. Maybe a -> [a]
maybeToList ([Attribute] -> Expression -> Maybe Binding
lodged [Attribute]
path Expression
side))
    gathered :: String -> String -> [Either String String] -> String
    gathered :: String -> String -> [Either String String] -> String
gathered String
tag String
opening [Either String String]
parts
      | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
inner = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<%s%s/>" String
opening String
marks
      | Bool
otherwise = String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<%s%s>%s</%s>" String
opening String
marks String
inner String
tag
      where
        marks :: String
        marks :: String
marks = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Either String String] -> [String]
forall a b. [Either a b] -> [a]
lefts [Either String String]
parts)
        inner :: String
        inner :: String
inner = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Either String String] -> [String]
forall a b. [Either a b] -> [b]
rights [Either String String]
parts)
    part :: Int -> Binding -> Naming (Either String String)
    part :: Int
-> Binding -> StateT (Nesting, [String]) IO (Either String String)
part Int
depth (BiTau Attribute
attr Expression
value) = String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String)
-> Naming String
-> StateT (Nesting, [String]) IO (Either String String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Expression -> Naming Expression
titled Int
depth Expression
value Naming Expression -> (Expression -> Naming String) -> Naming String
forall a b.
StateT (Nesting, [String]) IO a
-> (a -> StateT (Nesting, [String]) IO b)
-> StateT (Nesting, [String]) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO String -> Naming String)
-> (Expression -> IO String) -> Expression -> Naming String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Expression -> IO String
attributed (Attribute -> String
printAttribute Attribute
attr))
    part Int
_ (BiVoid Attribute
attr) = Either String String
-> StateT (Nesting, [String]) IO (Either String String)
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Either String String
forall a b. b -> Either a b
Right (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<void attr=\"%s\"/>" (String -> String
escapeXML (Attribute -> String
printAttribute Attribute
attr))))
    part Int
_ (BiLambda Function
func) = Either String String
-> StateT (Nesting, [String]) IO (Either String String)
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Either String String
forall a b. a -> Either a b
Left (String -> String -> String
forall r. PrintfType r => String -> r
printf String
" λ=\"%s\"" (String -> String
escapeXML (Function -> String
printFunction Function
func))))
    part Int
_ (BiDelta Bytes
bytes) = String -> Either String String
forall a b. a -> Either a b
Left (String -> Either String String)
-> (String -> String) -> String -> Either String String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
forall r. PrintfType r => String -> r
printf String
" Δ=\"%s\"" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXML (String -> Either String String)
-> Naming String
-> StateT (Nesting, [String]) IO (Either String String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Expression -> IO String
printed (Bytes -> Expression
ExBytes Bytes
bytes))
    part Int
_ Binding
_ = Either String String
-> StateT (Nesting, [String]) IO (Either String String)
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Either String String
forall a b. b -> Either a b
Right String
"")
    argument :: Int -> Argument -> Naming String
    argument :: Int -> Argument -> Naming String
argument Int
depth (ArTau Attribute
attr Expression
value) = Int -> Expression -> Naming Expression
titled Int
depth Expression
value Naming Expression -> (Expression -> Naming String) -> Naming String
forall a b.
StateT (Nesting, [String]) IO a
-> (a -> StateT (Nesting, [String]) IO b)
-> StateT (Nesting, [String]) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO String -> Naming String)
-> (Expression -> IO String) -> Expression -> Naming String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Expression -> IO String
attributed (Attribute -> String
printAttribute Attribute
attr)
    argument Int
depth (ArAlpha Alpha
alpha Expression
value) = Int -> Expression -> Naming Expression
titled Int
depth Expression
value Naming Expression -> (Expression -> Naming String) -> Naming String
forall a b.
StateT (Nesting, [String]) IO a
-> (a -> StateT (Nesting, [String]) IO b)
-> StateT (Nesting, [String]) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO String -> Naming String)
-> (Expression -> IO String) -> Expression -> Naming String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Expression -> IO String
attributed (Alpha -> String
printAlpha Alpha
alpha)
    attributed :: String -> Expression -> IO String
    attributed :: String -> Expression -> IO String
attributed String
name Expression
ExTermination = String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<bottom attr=\"%s\"/>" (String -> String
escapeXML String
name))
    attributed String
name Expression
value = String -> String -> String
tagged (Expression -> String
kind Expression
value) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeXMLText (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> IO String
spelled Expression
value
      where
        tagged :: String -> String -> String
        tagged :: String -> String -> String
tagged String
tag String
text = String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<%s attr=\"%s\">%s</%s>" String
tag (String -> String
escapeXML String
name) String
text String
tag
    kind :: Expression -> String
    kind :: Expression -> String
kind (ExFormation [BiLambda (FnSymbol Int
_)]) = String
"symbol"
    kind (ExFormation [BiDelta Bytes
_]) = String
"datum"
    kind (ExBytes Bytes
_) = String
"datum"
    kind (ExMeta Text
_) = String
"meta"
    kind Expression
_ = String
"ref"
    chained :: Named Expression -> Expression -> (Expression, [Argument])
    chained :: Named Expression -> Expression -> (Expression, [Argument])
chained Named Expression
objects (ExApplication Expression
inner Argument
arg) = case Expression
inner of
      ExApplication Expression
_ Argument
_ | Maybe Expression
Nothing <- Expression -> Named Expression -> Maybe Expression
forall a. Expression -> Named a -> Maybe a
namedLookup Expression
inner Named Expression
objects -> ([Argument] -> [Argument])
-> (Expression, [Argument]) -> (Expression, [Argument])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([Argument] -> [Argument] -> [Argument]
forall a. [a] -> [a] -> [a]
++ [Argument
arg]) (Named Expression -> Expression -> (Expression, [Argument])
chained Named Expression
objects Expression
inner)
      Expression
_ -> (Expression
inner, [Argument
arg])
    chained Named Expression
_ Expression
term = (Expression
term, [])
    parted :: Int -> Expression -> Naming (String, String)
    parted :: Int -> Expression -> Naming (String, String)
parted Int
depth (ExApplication Expression
term Argument
arg) = (,) (String -> String -> (String, String))
-> Naming String
-> StateT (Nesting, [String]) IO (String -> (String, String))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
leaf Int
depth Expression
term StateT (Nesting, [String]) IO (String -> (String, String))
-> Naming String -> Naming (String, String)
forall a b.
StateT (Nesting, [String]) IO (a -> b)
-> StateT (Nesting, [String]) IO a
-> StateT (Nesting, [String]) IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Argument -> Naming String
argument Int
depth Argument
arg
    parted Int
depth Expression
term = (,String
"") (String -> (String, String))
-> Naming String -> Naming (String, String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
leaf Int
depth Expression
term
    called :: Int -> Expression -> Naming (String, String)
    called :: Int -> Expression -> Naming (String, String)
called Int
depth Expression
term = do
      String
path <- Int -> Expression -> Naming String
leaf Int
depth Expression
object
      [String]
given <- ((Attribute, Expression) -> Naming String)
-> [(Attribute, Expression)]
-> StateT (Nesting, [String]) IO [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Attribute, Expression) -> Naming String
passed [(Attribute, Expression)]
arguments
      (String, String) -> Naming (String, String)
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
path, String -> String -> String
forall r. PrintfType r => String -> r
printf String
"<with>%s</with>" ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
given))
      where
        object :: Expression
        arguments :: [(Attribute, Expression)]
        (Expression
object, [(Attribute, Expression)]
arguments) = Expression -> (Expression, [(Attribute, Expression)])
invoked Expression
term
    sole :: Int -> Expression -> Naming (String, String)
    sole :: Int -> Expression -> Naming (String, String)
sole Int
depth Expression
term = (,String
"") (String -> (String, String))
-> Naming String -> Naming (String, String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Expression -> Naming String
leaf Int
depth Expression
term
    enclosed :: String -> String -> (String, String) -> String
    enclosed :: String -> String -> (String, String) -> String
enclosed String
_ String
opening (String
origin, String
"") = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s of=\"%s\"/>" String
opening (String -> String
escapeXML String
origin)
    enclosed String
tag String
opening (String
origin, String
inner) = String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s of=\"%s\">%s</%s>" String
opening (String -> String
escapeXML String
origin) String
inner String
tag
    invoked :: Expression -> (Expression, [(Attribute, Expression)])
    invoked :: Expression -> (Expression, [(Attribute, Expression)])
invoked (ExApplication Expression
term (ArTau Attribute
attr Expression
value)) = ([(Attribute, Expression)] -> [(Attribute, Expression)])
-> (Expression, [(Attribute, Expression)])
-> (Expression, [(Attribute, Expression)])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([(Attribute, Expression)]
-> [(Attribute, Expression)] -> [(Attribute, Expression)]
forall a. [a] -> [a] -> [a]
++ [(Attribute
attr, Expression
value)]) (Expression -> (Expression, [(Attribute, Expression)])
invoked Expression
term)
    invoked Expression
term = (Expression
term, [])
    passed :: (Attribute, Expression) -> Naming String
    passed :: (Attribute, Expression) -> Naming String
passed (Attribute
attr, Expression
value) = Expression -> Naming Expression
valued Expression
value Naming Expression -> (Expression -> Naming String) -> Naming String
forall a b.
StateT (Nesting, [String]) IO a
-> (a -> StateT (Nesting, [String]) IO b)
-> StateT (Nesting, [String]) IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO String -> Naming String
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Nesting, [String]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO String -> Naming String)
-> (Expression -> IO String) -> Expression -> Naming String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Expression -> IO String
attributed (Attribute -> String
printAttribute Attribute
attr)
    valued :: Expression -> Naming Expression
    valued :: Expression -> Naming Expression
valued Expression
value = do
      (Nesting
nesting, [String]
_) <- StateT (Nesting, [String]) IO (Nesting, [String])
forall (m :: * -> *) s. Monad m => StateT s m s
get
      case (Expression -> Named Expression -> Maybe Expression
forall a. Expression -> Named a -> Maybe a
namedLookup Expression
value Nesting
nesting._objects, Expression -> Maybe Int
symbolic Expression
value) of
        (Just Expression
aliased, Maybe Int
_) -> Expression -> Naming Expression
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
aliased
        (Maybe Expression
Nothing, Just Int
symbol) -> Expression -> Naming Expression
forall a. a -> StateT (Nesting, [String]) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Expression
standing Int
symbol)
        (Maybe Expression
Nothing, Maybe Int
Nothing) -> Expression -> Naming Expression
opaque Expression
value
    symbolic :: Expression -> Maybe Int
    symbolic :: Expression -> Maybe Int
symbolic (ExFormation [BiLambda (FnSymbol Int
idx)]) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
idx
    symbolic (ExFormation [Binding]
bds) = [Expression] -> Maybe Expression
forall a. [a] -> Maybe a
listToMaybe [Expression
body | BiTau Attribute
AtPhi Expression
body <- [Binding]
bds] Maybe Expression -> (Expression -> Maybe Int) -> Maybe Int
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expression -> Maybe Int
symbolic
    symbolic (ExApplication Expression
_ (ArTau Attribute
AtPhi Expression
body)) = Expression -> Maybe Int
symbolic Expression
body
    symbolic Expression
_ = Maybe Int
forall a. Maybe a
Nothing
    spelled :: Expression -> IO String
    spelled :: Expression -> IO String
spelled (ExFormation [BiLambda (FnSymbol Int
idx)]) = String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> String
sigma Int
idx)
    spelled (ExFormation [BiDelta Bytes
bytes]) = Expression -> IO String
printed (Bytes -> Expression
ExBytes Bytes
bytes)
    spelled (ExDispatch Expression
inner Attribute
attr)
      | Expression -> Bool
sigmatic Expression
inner = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s.%s" (String -> String -> String) -> IO String -> IO (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> IO String
spelled Expression
inner IO (String -> String) -> IO String -> IO String
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Attribute -> String
printAttribute Attribute
attr)
    spelled Expression
term = Expression -> IO String
printed Expression
term
    traced :: Expression -> IO String
    traced :: Expression -> IO String
traced Expression
ExXi = String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"ξ"
    traced (ExDispatch Expression
inner Attribute
attr) = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s.%s" (String -> String -> String) -> IO String -> IO (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> IO String
traced Expression
inner IO (String -> String) -> IO String -> IO String
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Attribute -> String
printAttribute Attribute
attr)
    traced Expression
term = Expression -> IO String
spelled Expression
term
    sigmatic :: Expression -> Bool
    sigmatic :: Expression -> Bool
sigmatic (ExFormation [BiLambda (FnSymbol Int
_)]) = Bool
True
    sigmatic (ExDispatch Expression
inner Attribute
_) = Expression -> Bool
sigmatic Expression
inner
    sigmatic Expression
_ = Bool
False
    known :: Expression -> Nesting -> Nesting
    known :: Expression -> Nesting -> Nesting
known world :: Expression
world@(ExFormation [Binding]
bds) Nesting
nesting = Nesting
nesting{_world = world', _shapes = Map.fromListWith (flip (++)) [(shape kept, [(path, kept)]) | (path, kept) <- breadth [(ExDispatch ExRoot attr, inner) | (attr, ExFormation inner) <- Map.toList world']], _objects = namedInsert world ExRoot nesting._objects}
      where
        world' :: Map.Map Attribute Expression
        world' :: Map Attribute Expression
world' = Map Attribute Expression
-> Map Attribute Expression -> Map Attribute Expression
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ([(Attribute, Expression)] -> Map Attribute Expression
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Attribute
attr, Expression
value) | BiTau Attribute
attr Expression
value <- [Binding]
bds]) Nesting
nesting._world
        breadth :: [(Expression, [Binding])] -> [(Expression, [Binding])]
        breadth :: [(Expression, [Binding])] -> [(Expression, [Binding])]
breadth [] = []
        breadth [(Expression, [Binding])]
level = [(Expression
path, (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
. Binding -> Bool
rho) [Binding]
inner) | (Expression
path, [Binding]
inner) <- [(Expression, [Binding])]
level] [(Expression, [Binding])]
-> [(Expression, [Binding])] -> [(Expression, [Binding])]
forall a. [a] -> [a] -> [a]
++ [(Expression, [Binding])] -> [(Expression, [Binding])]
breadth [(Expression -> Attribute -> Expression
ExDispatch Expression
path Attribute
attr, [Binding]
inner') | (Expression
path, [Binding]
inner) <- [(Expression, [Binding])]
level, BiTau Attribute
attr (ExFormation [Binding]
inner') <- [Binding]
inner, Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute
AtRho]
    known Expression
_ Nesting
nesting = Nesting
nesting
    shape :: [Binding] -> [Maybe Attribute]
    shape :: [Binding] -> [Maybe Attribute]
shape = (Binding -> Maybe Attribute) -> [Binding] -> [Maybe Attribute]
forall a b. (a -> b) -> [a] -> [b]
map Binding -> Maybe Attribute
label
      where
        label :: Binding -> Maybe Attribute
        label :: Binding -> Maybe Attribute
label (BiTau Attribute
attr Expression
_) = Attribute -> Maybe Attribute
forall a. a -> Maybe a
Just Attribute
attr
        label (BiVoid Attribute
attr) = Attribute -> Maybe Attribute
forall a. a -> Maybe a
Just Attribute
attr
        label Binding
_ = Maybe Attribute
forall a. Maybe a
Nothing
    rho :: Binding -> Bool
    rho :: Binding -> Bool
rho (BiTau Attribute
AtRho Expression
_) = Bool
True
    rho (BiVoid Attribute
AtRho) = Bool
True
    rho Binding
_ = Bool
False
    copied :: Nesting -> [Binding] -> Maybe (Expression, [(Attribute, Expression)])
    copied :: Nesting
-> [Binding] -> Maybe (Expression, [(Attribute, Expression)])
copied Nesting
nesting [Binding]
bds = (Int, (Expression, [(Attribute, Expression)]))
-> (Expression, [(Attribute, Expression)])
forall a b. (a, b) -> b
snd ((Int, (Expression, [(Attribute, Expression)]))
 -> (Expression, [(Attribute, Expression)]))
-> Maybe (Int, (Expression, [(Attribute, Expression)]))
-> Maybe (Expression, [(Attribute, Expression)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, (Expression, [(Attribute, Expression)]))]
-> Maybe (Int, (Expression, [(Attribute, Expression)]))
forall a. [a] -> Maybe a
listToMaybe (((Int, (Expression, [(Attribute, Expression)])) -> Int)
-> [(Int, (Expression, [(Attribute, Expression)]))]
-> [(Int, (Expression, [(Attribute, Expression)]))]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Int, (Expression, [(Attribute, Expression)])) -> Int
forall a b. (a, b) -> a
fst (((Expression, [Binding])
 -> Maybe (Int, (Expression, [(Attribute, Expression)])))
-> [(Expression, [Binding])]
-> [(Int, (Expression, [(Attribute, Expression)]))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Expression, [Binding])
-> Maybe (Int, (Expression, [(Attribute, Expression)]))
matched [(Expression, [Binding])]
candidates))
      where
        own :: [Binding]
        own :: [Binding]
own = (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
. Binding -> Bool
rho) [Binding]
bds
        parents :: [Expression]
        parents :: [Expression]
parents = [Expression
value | BiTau Attribute
AtRho Expression
value <- [Binding]
bds]
        candidates :: [(Expression, [Binding])]
        candidates :: [(Expression, [Binding])]
candidates = case [Expression]
parents of
          [] -> [(Expression, [Binding])]
-> [Maybe Attribute]
-> Map [Maybe Attribute] [(Expression, [Binding])]
-> [(Expression, [Binding])]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] ([Binding] -> [Maybe Attribute]
shape [Binding]
own) Nesting
nesting._shapes
          Expression
value : [Expression]
_ -> [(Expression -> Attribute -> Expression
ExDispatch Expression
value Attribute
attr, (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
. Binding -> Bool
rho) [Binding]
origin) | BiTau Attribute
attr (ExFormation [Binding]
origin) <- [Binding] -> Maybe [Binding] -> [Binding]
forall a. a -> Maybe a -> a
fromMaybe [] (Expression -> Maybe [Binding]
declared Expression
value), Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute
AtRho]
        matched :: (Expression, [Binding]) -> Maybe (Int, (Expression, [(Attribute, Expression)]))
        matched :: (Expression, [Binding])
-> Maybe (Int, (Expression, [(Attribute, Expression)]))
matched (Expression
path, [Binding]
kept) = do
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([Binding] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Binding]
kept 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]
own)
          [(Attribute, Expression)]
given <- [[(Attribute, Expression)]] -> [(Attribute, Expression)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Attribute, Expression)]] -> [(Attribute, Expression)])
-> Maybe [[(Attribute, Expression)]]
-> Maybe [(Attribute, Expression)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Binding -> Binding -> Maybe [(Attribute, Expression)])
-> [Binding] -> [Binding] -> Maybe [[(Attribute, Expression)]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Binding -> Binding -> Maybe [(Attribute, Expression)]
bound [Binding]
kept [Binding]
own
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ((Binding -> Binding -> Bool) -> [Binding] -> [Binding] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Binding -> Binding -> Bool
forall a. Eq a => a -> a -> Bool
(==) [Binding]
kept [Binding]
own) Bool -> Bool -> Bool
|| Bool -> Bool
not ([Expression] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expression]
parents) Bool -> Bool -> Bool
&& [(Attribute, Expression)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Attribute, Expression)]
given Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [() | BiVoid Attribute
_ <- [Binding]
kept])
          (Int, (Expression, [(Attribute, Expression)]))
-> Maybe (Int, (Expression, [(Attribute, Expression)]))
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Attribute, Expression)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Attribute, Expression)]
given, (Expression
path, [(Attribute, Expression)]
given))
        declared :: Expression -> Maybe [Binding]
        declared :: Expression -> Maybe [Binding]
declared Expression
ExRoot = [Binding] -> Maybe [Binding]
forall a. a -> Maybe a
Just [Attribute -> Expression -> Binding
BiTau Attribute
attr Expression
value | (Attribute
attr, Expression
value) <- Map Attribute Expression -> [(Attribute, Expression)]
forall k a. Map k a -> [(k, a)]
Map.toList Nesting
nesting._world]
        declared (ExFormation [Binding]
inner) = [Binding] -> Maybe [Binding]
forall a. a -> Maybe a
Just [Binding]
inner
        declared (ExApplication Expression
target Argument
_) = Expression -> Maybe [Binding]
declared Expression
target
        declared (ExDispatch Expression
target Attribute
attr) = do
          [Binding]
outer' <- Expression -> Maybe [Binding]
declared Expression
target
          [[Binding]] -> Maybe [Binding]
forall a. [a] -> Maybe a
listToMaybe [[Binding]
inner | BiTau Attribute
attr' (ExFormation [Binding]
inner) <- [Binding]
outer', Attribute
attr' Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
attr]
        declared Expression
_ = Maybe [Binding]
forall a. Maybe a
Nothing
        bound :: Binding -> Binding -> Maybe [(Attribute, Expression)]
        bound :: Binding -> Binding -> Maybe [(Attribute, Expression)]
bound (BiVoid Attribute
attr) (BiTau Attribute
attr' Expression
value)
          | Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
attr' = [(Attribute, Expression)] -> Maybe [(Attribute, Expression)]
forall a. a -> Maybe a
Just [(Attribute
attr, Expression
value)]
        bound (BiTau Attribute
attr Expression
origin) (BiTau Attribute
attr' Expression
value)
          | Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
attr' = [(Attribute, Expression)] -> Maybe [(Attribute, Expression)]
forall a. a -> Maybe a
Just [(Attribute
attr, Expression
value) | Expression
origin Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
/= Expression
value]
        bound Binding
origin Binding
binding
          | Binding
origin Binding -> Binding -> Bool
forall a. Eq a => a -> a -> Bool
== Binding
binding = [(Attribute, Expression)] -> Maybe [(Attribute, Expression)]
forall a. a -> Maybe a
Just []
          | Bool
otherwise = Maybe [(Attribute, Expression)]
forall a. Maybe a
Nothing
    pathed :: Expression -> Bool
    pathed :: Expression -> Bool
pathed Expression
ExRoot = Bool
True
    pathed Expression
ExXi = Bool
True
    pathed (ExMeta Text
_) = Bool
True
    pathed (ExDispatch Expression
inner Attribute
_) = Expression -> Bool
pathed Expression
inner
    pathed Expression
term = Expression -> Bool
sigmatic Expression
term
    plain :: Expression -> Bool
    plain :: Expression -> Bool
plain Expression
ExRoot = Bool
True
    plain Expression
ExXi = Bool
True
    plain Expression
ExTermination = Bool
True
    plain (ExMeta Text
_) = Bool
True
    plain (ExBytes Bytes
_) = Bool
True
    plain Expression
_ = Bool
False
    sigma :: Int -> String
    sigma :: Int -> String
sigma = Function -> String
printFunction (Function -> String) -> (Int -> Function) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Function
FnSymbol
    quoted :: T.Text -> String
    quoted :: Text -> String
quoted = String -> String
escapeXML (String -> String) -> (Text -> String) -> Text -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack

endEvalXml :: Handle -> IORef Nesting -> Double -> IO ()
endEvalXml :: Handle -> IORef Nesting -> Double -> IO ()
endEvalXml Handle
handle IORef Nesting
cursor Double
began = do
  Nesting
nesting <- IORef Nesting -> IO Nesting
forall a. IORef a -> IO a
readIORef IORef Nesting
cursor
  (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Handle -> String -> IO ()
hPutStrLn Handle
handle) (([(Int, String)], [String]) -> [String]
forall a b. (a, b) -> b
snd (Int -> [(Int, String)] -> ([(Int, String)], [String])
closed Int
0 Nesting
nesting._closing))
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Int, String)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Nesting
nesting._closing) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    Double
now <- IO Double
getMonotonicTime
    let taken :: Int
taken = Double -> Double -> Int
milliseconds Double
began Double
now
    Handle -> String -> IO ()
hPutStrLn Handle
handle (Int -> String -> String
indentedXml Int
0 (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"<msec>%d</msec>" Int
taken))
    Handle -> String -> IO ()
hPutStrLn Handle
handle (Int -> String -> String
indentedXml Int
0 (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"<firings>%d</firings>" Nesting
nesting._fires))
    Handle -> String -> IO ()
hPutStrLn Handle
handle (Int -> String -> String
indentedXml Int
0 (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"<fps>%d</fps>" (Int -> Int -> Int
perSecond Nesting
nesting._fires Int
taken)))
    Handle -> String -> IO ()
hPutStrLn Handle
handle String
"</protocol>"
  IORef Nesting -> Nesting -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Nesting
cursor Nesting
nesting{_closing = []}

commanded :: [String] -> String
commanded :: [String] -> String
commanded [String]
command = [String] -> String
unwords ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
shelled (String
"phino" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
command))
  where
    shelled :: String -> String
    shelled :: String -> String
shelled String
word
      | Bool -> Bool
not (String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
word) Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
safe String
word = String
word
      | Bool
otherwise = String
"'" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
escaped String
word String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'"
    safe :: Char -> Bool
    safe :: Char -> Bool
safe Char
char = Char -> Bool
isAlphaNum Char
char Bool -> Bool -> Bool
|| Char
char Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (String
"-_./=:,+@%" :: String)
    escaped :: Char -> String
    escaped :: Char -> String
escaped Char
'\'' = String
"'\\''"
    escaped Char
char = [Char
char]

closed :: Int -> [(Int, String)] -> ([(Int, String)], [String])
closed :: Int -> [(Int, String)] -> ([(Int, String)], [String])
closed Int
depth [(Int, String)]
open = ([(Int, String)]
kept, [Int -> String -> String
indentedXml Int
level (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"</%s>" String
element) | (Int
level, String
element) <- [(Int, String)]
shut])
  where
    ([(Int, String)]
shut, [(Int, String)]
kept) = ((Int, String) -> Bool)
-> [(Int, String)] -> ([(Int, String)], [(Int, String)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
depth) (Int -> Bool) -> ((Int, String) -> Int) -> (Int, String) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, String) -> Int
forall a b. (a, b) -> a
fst) [(Int, String)]
open

indented :: Int -> String -> String
indented :: Int -> String -> String
indented Int
depth String
line = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
depth) Char
' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
line

indentedXml :: Int -> String -> String
indentedXml :: Int -> String -> String
indentedXml Int
depth = Int -> String -> String
indented (Int
depth Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

atomicModify :: IORef a -> (a -> IO (a, b)) -> IO b
atomicModify :: forall a b. IORef a -> (a -> IO (a, b)) -> IO b
atomicModify IORef a
ref a -> IO (a, b)
action = IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
ref IO a -> (a -> IO (a, b)) -> IO (a, b)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> IO (a, b)
action IO (a, b) -> ((a, b) -> IO b) -> IO b
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(a
value, b
made) -> IORef a -> a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef a
ref a
value IO () -> IO b -> IO b
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> b -> IO b
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
made

standing :: Int -> Expression
standing :: Int -> Expression
standing Int
symbol = [Binding] -> Expression
ExFormation [Function -> Binding
BiLambda (Int -> Function
FnSymbol Int
symbol)]

answer :: T.Text
answer :: Text
answer = Text
"𝑛"

sigil :: T.Text
sigil :: Text
sigil = Text
"𝛿"

fragment :: T.Text
fragment :: Text
fragment = Text
"𝑒"

found :: Either Int Bytes -> Maybe (Either Int Bytes, String) -> Maybe String
found :: Either Int Bytes
-> Maybe (Either Int Bytes, String) -> Maybe String
found Either Int Bytes
value (Just (Either Int Bytes
held, String
naming))
  | Either Int Bytes
value Either Int Bytes -> Either Int Bytes -> Bool
forall a. Eq a => a -> a -> Bool
== Either Int Bytes
held = String -> Maybe String
forall a. a -> Maybe a
Just String
naming
found Either Int Bytes
_ Maybe (Either Int Bytes, String)
_ = Maybe String
forall a. Maybe a
Nothing

alias :: Int -> Int -> Expression
alias :: Int -> Int -> Expression
alias Int
firing Int
index = Text -> Expression
ExMeta (String -> Text
T.pack (String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"n·%d·%d" Int
firing Int
index))

dontSaveEval :: SaveEvalFunc
dontSaveEval :: SaveEvalFunc
dontSaveEval Evaluation
_ = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

data Progress = Progress
  { Progress -> Double
_began :: Double
  , Progress -> Maybe Double
_told :: Maybe Double
  , Progress -> Int
_formations :: Int
  , Progress -> Int
_firings :: Int
  }

emptyProgress :: Double -> Progress
emptyProgress :: Double -> Progress
emptyProgress Double
began = Double -> Maybe Double -> Int -> Int -> Progress
Progress Double
began Maybe Double
forall a. Maybe a
Nothing Int
0 Int
0

progressed :: IORef Progress -> Double -> (Expression -> IO String) -> SaveEvalFunc -> SaveEvalFunc
progressed :: IORef Progress
-> Double
-> (Expression -> IO String)
-> SaveEvalFunc
-> SaveEvalFunc
progressed IORef Progress
cursor Double
interval Expression -> IO String
render SaveEvalFunc
record Evaluation
evaluation = do
  SaveEvalFunc
record Evaluation
evaluation
  ((Progress -> Progress, Expression) -> IO ())
-> Maybe (Progress -> Progress, Expression) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Progress -> Progress, Expression) -> IO ()
reported (Evaluation -> Maybe (Progress -> Progress, Expression)
sited Evaluation
evaluation)
  where
    sited :: Evaluation -> Maybe (Progress -> Progress, Expression)
    sited :: Evaluation -> Maybe (Progress -> Progress, Expression)
sited (EvFiring Int
_ Text
_ Judgment
_ Expression
site) = (Progress -> Progress, Expression)
-> Maybe (Progress -> Progress, Expression)
forall a. a -> Maybe a
Just (\Progress
progress -> Progress
progress{_firings = progress._firings + 1}, Expression
site)
    sited (EvStarted Int
_ Judgment
Dataization Expression
site) = (Progress -> Progress, Expression)
-> Maybe (Progress -> Progress, Expression)
forall a. a -> Maybe a
Just (\Progress
progress -> Progress
progress{_formations = progress._formations + 1}, Expression
site)
    sited Evaluation
_ = Maybe (Progress -> Progress, Expression)
forall a. Maybe a
Nothing
    reported :: (Progress -> Progress, Expression) -> IO ()
    reported :: (Progress -> Progress, Expression) -> IO ()
reported (Progress -> Progress
counted, Expression
site) = do
      Double
now <- IO Double
getMonotonicTime
      Progress
progress <- Progress -> Progress
counted (Progress -> Progress) -> IO Progress -> IO Progress
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef Progress -> IO Progress
forall a. IORef a -> IO a
readIORef IORef Progress
cursor
      if Bool -> (Double -> Bool) -> Maybe Double -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (\Double
told -> Double
now Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
told Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
>= Double
interval) Progress
progress._told
        then do
          String
locator <- Expression -> IO String
render Expression
site
          String -> IO ()
logInfo (String -> Int -> Int -> Double -> String -> String
forall r. PrintfType r => String -> r
printf String
"Started %d dataizations and fired %d λ functions in %.0fs, now at %s" Progress
progress._formations Progress
progress._firings (Double
now Double -> Double -> Double
forall a. Num a => a -> a -> a
- Progress
progress._began) String
locator)
          IORef Progress -> Progress -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Progress
cursor Progress
progress{_told = Just now}
        else IORef Progress -> Progress -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Progress
cursor Progress
progress