diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -378,12 +378,18 @@
A `join` line of such an entry takes a formation with `λ ⤍ L_throw`, or an
application of one, for a branch that raises, exactly as it takes `⊥`: it binds
-its meta to the other term and writes `terminate(…)`. The morph of an operand
-of the entry that comes to such a term stops there, and `--deep` walks none of
-its bindings, since its message is what the program reports at runtime and
-there is nothing to reduce in it. A name under `terminators` that a key of the
-file matches is refused when the file is read, since that function fires
-rather than raises.
+its meta to the other term and writes `terminate(…)`. Under `--deep` the walk
+reduces the message of that copy like any other code, records and all, and
+never fires `L_throw` itself, since no entry answers it. The record names the
+reduced `message` as its last argument, as
+`terminate(𝔻(𝜎2:λ), right, 𝑛·4·6) # 𝑛4` in the text format and
+`` in the markup, so
+the error path can be lowered as well as the other branch. A message the walk
+cannot reduce ends the way any operand does: a call no entry answers stays as
+it is written, and a firing that gets stuck fails the run, unless `--partial`
+is given. A raising term with no `message` names none. A name under
+`terminators` that a key of the file matches is refused when the file is read,
+since that function fires rather than raises.
Every symbol a join mints is written into the protocol as a fact of its own,
so a reader ties it to the two it stands for without diffing the terms; the
diff --git a/benchmark/Main.hs b/benchmark/Main.hs
--- a/benchmark/Main.hs
+++ b/benchmark/Main.hs
@@ -87,7 +87,6 @@
[]
Map.empty
lambdas
- []
(building linked)
reduction
evaluation
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
cabal-version: 3.0
name: phino
-version: 0.0.152
+version: 0.0.153
license: MIT
synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
description: Please see the README on GitHub at
diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs
--- a/src/CLI/Runners.hs
+++ b/src/CLI/Runners.hs
@@ -188,7 +188,7 @@
_protocol
printCtx
( \record -> do
- let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally minted deadline memo 1 (Just (1, Dataization, loc)) _depthSensitive _shuffle _partial False 1 _acyclic Dataization [] Map.empty lambdas [] (building linked) reduction evaluation fired save record linked
+ let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally minted deadline memo 1 (Just (1, Dataization, loc)) _depthSensitive _shuffle _partial False 1 _acyclic Dataization [] Map.empty lambdas (building linked) reduction evaluation fired save record linked
(universe, aiming) <- aimed printCtx Dataization _inside expr ctx
started universe aiming
dataize universe emptyState aiming
@@ -270,7 +270,7 @@
_protocol
printCtx
( \record -> do
- let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally minted deadline memo 1 (Just (1, Morphing, loc)) _depthSensitive _shuffle _partial _deep _jobs _acyclic Morphing [] Map.empty lambdas [] (building linked) reduction evaluation fired save record linked
+ let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally minted deadline memo 1 (Just (1, Morphing, loc)) _depthSensitive _shuffle _partial _deep _jobs _acyclic Morphing [] Map.empty lambdas (building linked) reduction evaluation fired save record linked
(universe, aiming) <- aimed printCtx Morphing _inside expr ctx
started universe aiming
morph universe emptyState aiming
diff --git a/src/Deps.hs b/src/Deps.hs
--- a/src/Deps.hs
+++ b/src/Deps.hs
@@ -114,7 +114,7 @@
| EvKnown Int Int Bytes
| EvJoin Int T.Text (T.Text, T.Text) Expression
| EvJoined Int Int (Int, Int)
- | EvTerminate Int (Maybe (Either Int Bytes)) T.Text T.Text
+ | EvTerminate Int (Maybe (Either Int Bytes)) T.Text T.Text (Maybe Expression)
| EvMinted Int Int [Either Int Bytes]
| EvDeferred Int Int Judgment Expression (Maybe Expression) Expression
| EvApplied Int Judgment Expression Expression Expression
@@ -141,7 +141,7 @@
record (EvKnown depth sym bytes) = EvKnown depth (symbol sym) bytes
record (EvJoin depth spelling pair value) = EvJoin depth spelling pair (term value)
record (EvJoined depth fresh (one, two)) = EvJoined depth (symbol fresh) (symbol one, symbol two)
- record (EvTerminate depth condition side raising) = EvTerminate depth (fmap datum condition) side raising
+ record (EvTerminate depth condition side raising message) = EvTerminate depth (fmap datum condition) side raising (fmap term message)
record (EvMinted depth sym operands) = EvMinted depth (symbol sym) (map datum operands)
record (EvDeferred depth sym judgment copy call site) = EvDeferred depth (symbol sym) judgment (term copy) (fmap term call) (term site)
record (EvApplied depth judgment call object site) = EvApplied depth judgment (term call) (term object) (term site)
@@ -199,7 +199,7 @@
tier (EvKnown depth _ _) = depth
tier (EvJoin depth _ _ _) = depth
tier (EvJoined depth _ _) = depth
-tier (EvTerminate depth _ _ _) = depth
+tier (EvTerminate depth _ _ _ _) = depth
tier (EvMinted depth _ _) = depth
tier (EvDeferred depth _ _ _ _ _) = depth
tier (EvApplied depth _ _ _ _) = depth
@@ -403,9 +403,10 @@
left <- render (standing one)
right <- render (standing two)
pure (protocol, Just (indented depth (printf "𝔻(%s) ∈ { 𝔻(%s), 𝔻(%s) }" form left right)))
- written (EvTerminate depth condition side raised) protocol = do
+ written (EvTerminate depth condition side raised message) protocol = do
cond <- maybe (pure []) (fmap pure . spelled) condition
- pure (protocol, Just (indented depth (printf "terminate(%s) # %s" (intercalate ", " (cond ++ [T.unpack side])) (T.unpack raised))))
+ said <- maybe (pure []) (fmap pure . render) message
+ pure (protocol, Just (indented depth (printf "terminate(%s) # %s" (intercalate ", " (cond ++ [T.unpack side] ++ said)) (T.unpack raised))))
where
spelled :: Either Int Bytes -> IO String
spelled (Left symbol) = printf "𝔻(%s)" <$> render (standing symbol)
@@ -614,13 +615,17 @@
(kept, closers) = closed depth nesting._closing
joint :: String
joint = printf "%s %s" (sigma fresh) (sigma one) (sigma two)
- elements (EvTerminate depth condition side _) nesting = do
+ elements (EvTerminate depth condition side _ message) nesting = do
+ said <- maybe (pure "") attributed message
terminal <- case condition of
- Just (Left symbol) -> pure (printf "" (sigma symbol) (quoted side))
- Just (Right bytes) -> printf "%s" (quoted side) . escapeXMLText <$> render (ExBytes bytes)
- Nothing -> pure (printf "" (quoted side))
+ Just (Left symbol) -> pure (printf "" (sigma symbol) (quoted side) said)
+ Just (Right bytes) -> printf "%s" (quoted side) said . escapeXMLText <$> render (ExBytes bytes)
+ Nothing -> pure (printf "" (quoted side) said)
let (kept, closers) = closed depth nesting._closing
pure (nesting{_closing = kept}, closers ++ [indentedXml depth terminal])
+ where
+ attributed :: Expression -> IO String
+ attributed term = printf " message=\"%s\"" . escapeXML <$> render term
elements (EvMinted depth symbol operands) nesting = do
spelledOperands <- mapM spelled operands
let (kept, closers) = closed depth nesting._closing
diff --git a/src/Evaluate.hs b/src/Evaluate.hs
--- a/src/Evaluate.hs
+++ b/src/Evaluate.hs
@@ -18,7 +18,7 @@
import qualified Data.Text as T
import Deps (Evaluation (..), Judgment (Morphing), State (..), resited)
import Engine (Engine (..))
-import Lambdas (Lambda (..), Meta (..), joined, matched, minted, symbolized, thrown)
+import Lambdas (Lambda (..), Meta (..), joined, matched, message, minted, symbolized, thrown)
import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot)
import Morph (Answer, Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Refused (..), Steps (..), admitted, charged, counted, deeper, isLambda, lambda, morphing, normalized, opening, recalled, refused, remember, remembered, retained, settled, starved, unparked)
import Printer (printFunction)
@@ -70,7 +70,7 @@
let ctx = caller{_nesting = caller._nesting + 1}
outcome <- try $ do
(bound, dataized, conditions) <- foldM (down ctx) (substEmpty, state, []) entry._dataized
- (bound', morphed, normals) <- foldM (through ctx{_throwing = entry._terminators}) (bound, dataized, []) entry._morphed
+ (bound', morphed, normals) <- foldM (through ctx) (bound, dataized, []) entry._morphed
let firing = Firing func (reverse conditions) (reverse normals)
known <- remembered caller._memo firing
maybe (worked ctx entry firing bound' morphed) (\answer -> (answer, morphed) <$ shown ctx._nesting answer) known
@@ -161,8 +161,8 @@
one <- branch left
two <- branch right
case (raising one, raising two) of
- (True, False) -> terminating "left" left two
- (False, True) -> terminating "right" right one
+ (True, False) -> terminating "left" left one two
+ (False, True) -> terminating "right" right two one
_ -> both one two
where
raising :: Expression -> Bool
@@ -178,9 +178,9 @@
mapM_ (ctx._saveEval . fact) made
ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)
bind meta (MvExpression term) bound
- terminating :: T.Text -> Meta -> Expression -> IO Subst
- terminating side raised term = do
- ctx._saveEval (EvTerminate ctx._nesting condition side raised._spelling)
+ terminating :: T.Text -> Meta -> Expression -> Expression -> IO Subst
+ terminating side raised fault term = do
+ ctx._saveEval (EvTerminate ctx._nesting condition side raised._spelling (message fault))
ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)
bind meta (MvExpression term) bound
branch :: Meta -> IO Expression
diff --git a/src/Lambdas.hs b/src/Lambdas.hs
--- a/src/Lambdas.hs
+++ b/src/Lambdas.hs
@@ -14,6 +14,7 @@
, emptyLambdas
, joined
, matched
+ , message
, minted
, readLambdas
, symbolized
@@ -350,6 +351,12 @@
thrown names (ExApplication expr _) = thrown names expr
thrown names (ExFormation bds) = any (`elem` [BiLambda (Function name) | name <- names]) bds
thrown _ _ = False
+
+message :: Expression -> Maybe Expression
+message (ExApplication _ (ArTau (AtLabel "message") body)) = Just body
+message (ExApplication expr _) = message expr
+message (ExFormation bds) = listToMaybe [body | BiTau (AtLabel "message") body <- bds]
+message _ = Nothing
minted :: Expression -> Int -> ([(Slot, Function)], Int)
minted answer spent = (zip fresh [FnSymbol idx | idx <- [spent + 1 ..]], spent + length fresh)
diff --git a/src/Morph.hs b/src/Morph.hs
--- a/src/Morph.hs
+++ b/src/Morph.hs
@@ -31,7 +31,7 @@
import Engine (Engine (..))
import GHC.Clock (getMonotonicTime)
import qualified Inference as In
-import Lambdas (Lambdas, emptyLambdas, thrown)
+import Lambdas (Lambdas, emptyLambdas)
import Locator (locatedExpression, withLocatedExpression)
import Matcher (substEmpty)
import Must (Must (..))
@@ -110,7 +110,6 @@
, _parked :: [T.Text]
, _entered :: Seen
, _symbolic :: Lambdas
- , _throwing :: [T.Text]
, _buildTerm :: BuildTermFunc
, _reduce :: ReductionFunc
, _evaluate :: EvaluationFunc
@@ -401,7 +400,7 @@
marked ctx func = (walking ctx){_parked = func : _parked}
walked :: ReduceContext -> Expression -> NonEmpty Rewritten -> State -> IO (Expression, [Rewritten], State)
walked walker morphed seq state'
- | not _deep || thrown _throwing morphed = pure (morphed, reverse (NE.toList seq), state')
+ | not _deep = pure (morphed, reverse (NE.toList seq), state')
| otherwise = do
(deep, state'') <- deepened Nothing morphed universe state' walker
seq' <- leadsTo seq (Morphing, "deep") deep walker
diff --git a/test-resources/evaluate-packs/fails-on-a-message-whose-firing-gets-stuck.yaml b/test-resources/evaluate-packs/fails-on-a-message-whose-firing-gets-stuck.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/evaluate-packs/fails-on-a-message-whose-firing-gets-stuck.yaml
@@ -0,0 +1,106 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+# yamllint disable rule:line-length
+# The walk reduces the message of the copy a branch raises with like any other
+# code, so the firing of 'L_number_plus' it asks for gets stuck on the
+# 'L_number_nope' no entry answers, the way the firing of any operand does, and
+# the run fails (#1867).
+symbolic: |
+ - λ: L_number_gt
+ dataize:
+ 𝛿1: $.ρ
+ 𝛿2: $.x
+ 𝑛: Φ.bool( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
+ - λ: L_number_plus
+ dataize:
+ 𝛿1: $.ρ
+ 𝛿2: $.x
+ 𝑛: Φ.number( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
+ - λ: L_fork
+ dataize:
+ 𝛿1: $.ρ
+ morph:
+ 𝑛1: $.then
+ 𝑛2: $.else
+ symbolize:
+ 𝑛3: 𝑛1
+ 𝑛4: 𝑛2
+ join:
+ 𝑛5: [𝑛3, 𝑛4]
+ terminators: [L_throw]
+ 𝑛: 𝑛5
+location: 'Q.@'
+deep: true
+input: >
+ ⟦ bytes(φ) ↦ ⟦⟧,
+ error(message) ↦ ⟦ λ ⤍ L_throw ⟧,
+ bool(φ) ↦ ⟦ if ↦ ⟦ ρ ↦ ∅, then ↦ ∅, else ↦ ∅, λ ⤍ L_fork ⟧ ⟧,
+ number(φ) ↦ ⟦
+ gt(ρ, x) ↦ ⟦ λ ⤍ L_number_gt ⟧,
+ plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧,
+ nope(ρ, x) ↦ ⟦ λ ⤍ L_number_nope ⟧ ⟧,
+ @ ↦ 5.gt( 0 ).if( then ↦ 1, else ↦ Φ.error( message ↦ 7.plus( 8.nope( 9 ) ) ) ).plus( 6 ) ⟧
+fails: "No entry of --symbolic answers the λ function 'L_number_nope'"
+protocol: |
+ 𝕄(Φ.φ):
+ 𝑛·0·1 := 5
+ 𝑛·0·2 := 𝑛·0·1.gt( x ↦ 0 )
+ 𝔼(L_number_gt):
+ 𝔻(Φ.a🌵0):
+ 𝕄(Φ.a🌵0):
+ 𝑛·1·1 := 5
+ 𝑛·1·2 := Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )
+ 𝛿·1·1 := 40-14-00-00-00-00-00-00 # 5.0
+ 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.ρ)
+ 𝔻(Φ.a🌵1):
+ 𝕄(Φ.a🌵1):
+ 𝑛·1·3 := 0
+ 𝑛·1·4 := Φ.bytes( φ ↦ 00-00-00-00-00-00-00-00:Δ )
+ 𝛿·1·2 := 00-00-00-00-00-00-00-00 # 0.0
+ 𝛿2·1 := 𝛿·1·2 # 𝔻(ξ.x)
+ 𝑛·1·5 := Φ.bool( φ ↦ 𝜎1:λ ) # 𝑛
+ 𝕄(𝑛·1·5):
+ 𝑛·1·6 := Φ.bool( φ ↦ 𝜎1:λ )
+ 𝑛·1·7 := 𝑛·1·6 # 𝕄(𝑛·1·5)
+ 𝑛·0·3 := 𝑛·1·6.if( then ↦ 1 )
+ 𝑛·0·4 := 𝑛·0·3( else ↦ Φ.error( message ↦ 7.plus( 8.nope( 9 ) ) ) )
+ 𝔼(L_fork):
+ 𝔻(Φ.a🌵2):
+ 𝕄(Φ.a🌵2):
+ 𝑛·2·1 := Φ.bool( φ ↦ 𝜎1:λ )
+ 𝛿1·2 := 𝔻(𝜎1:λ) # 𝔻(ξ.ρ)
+ 𝕄(Φ.a🌵3):
+ 𝑛·2·2 := 1
+ 𝕄(Φ.a🌵3.φ):
+ 𝑛·2·3 := Φ.bytes( φ ↦ 3F-F0-00-00-00-00-00-00:Δ )
+ 𝑛1·2 := 𝑛·2·2 # 𝕄(ξ.then)
+ 𝕄(Φ.a🌵4):
+ 𝑛·2·4 := Φ.error( message ↦ 7.plus( 8.nope( 9 ) ) )
+ 𝕄(Φ.a🌵4.message):
+ 𝑛·2·5 := Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ )
+ 𝑛·2·6 := Φ.number( φ ↦ 𝑛·2·5 )
+ 𝑛·2·7 := Φ.number( φ ↦ 𝑛·2·5 )
+ 𝑛·2·8 := Φ.bytes( φ ↦ 40-20-00-00-00-00-00-00:Δ )
+ 𝑛·2·9 := Φ.number( φ ↦ 𝑛·2·8 )
+ 𝑛·2·10 := Φ.number( φ ↦ 𝑛·2·8 )
+ 𝑛·2·11 := Φ.bytes( φ ↦ 40-22-00-00-00-00-00-00:Δ )
+ 𝑛·2·12 := Φ.number( φ ↦ 𝑛·2·11 )
+ 𝑛·2·13 := Φ.number( φ ↦ 𝑛·2·8 )
+ 𝑛·2·14 := 𝑛·2·13.nope( x ↦ 𝑛·2·12 )
+ 𝑛·2·15 := Φ.number( φ ↦ 𝑛·2·5 )
+ 𝑛·2·16 := 𝑛·2·15.plus( x ↦ 𝑛·2·13.nope( 𝑛·2·12 ) )
+ 𝔼(L_number_plus):
+ 𝔻(Φ.a🌵5):
+ 𝕄(Φ.a🌵5):
+ 𝑛·3·1 := Φ.number( φ ↦ 𝑛·2·5 )
+ 𝑛·3·2 := Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ )
+ 𝛿·3·1 := 40-1C-00-00-00-00-00-00 # 7.0
+ 𝛿1·3 := 𝛿·3·1 # 𝔻(ξ.ρ)
+ 𝔻(Φ.a🌵6):
+ 𝕄(Φ.a🌵6):
+ 𝑛·3·3 := Φ.number( φ ↦ 𝑛·2·8 )
+ 𝑛·3·4 := 𝑛·3·3.nope( x ↦ 𝑛·2·12 )
+ unanswered(L_number_nope) # 𝔻(𝑛·3·4)
+ stuck(L_number_nope)
+ stuck(L_number_nope)
diff --git a/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-throws.yaml b/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-throws.yaml
--- a/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-throws.yaml
+++ b/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-throws.yaml
@@ -6,8 +6,9 @@
# purpose, here 'L_throw', rather than with ⊥. The entry of the fork names it
# among its terminators, so the join takes the branch that comes to such a
# copy for one that raises, the way it takes ⊥, and answers the other branch.
-# The morph of that branch stops at the copy and never walks into its message,
-# which here would fire 'L_number_plus' for nothing (#1865).
+# The walk reduces the message of that copy like any other code, firing
+# 'L_number_plus' for it, and never fires 'L_throw', and the 'terminate' line
+# names the meta of the reduced message (#1867).
symbolic: |
- λ: L_number_gt
dataize:
@@ -43,7 +44,7 @@
plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧,
@ ↦ 5.gt( 0 ).if( then ↦ 1.plus( 2 ), else ↦ Φ.error( message ↦ 7.plus( 8 ) ) ).plus( 6 ) ⟧
result: |-
- ⟦ φ ↦ 𝜎3:λ, gt(x) ↦ L_number_gt:λ, plus(x) ↦ L_number_plus:λ ⟧
+ ⟦ φ ↦ 𝜎4:λ, gt(x) ↦ L_number_gt:λ, plus(x) ↦ L_number_plus:λ ⟧
protocol: |
𝕄(Φ.φ):
𝑛·0·1 := 5
@@ -98,29 +99,54 @@
𝑛1·2 := 𝑛·3·7 # 𝕄(ξ.then)
𝕄(Φ.a🌵6):
𝑛·2·6 := Φ.error( message ↦ 7.plus( 8 ) )
+ 𝕄(Φ.a🌵6.message):
+ 𝑛·2·7 := Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ )
+ 𝑛·2·8 := Φ.number( φ ↦ 𝑛·2·7 )
+ 𝑛·2·9 := Φ.number( φ ↦ 𝑛·2·7 )
+ 𝑛·2·10 := Φ.bytes( φ ↦ 40-20-00-00-00-00-00-00:Δ )
+ 𝑛·2·11 := Φ.number( φ ↦ 𝑛·2·10 )
+ 𝑛·2·12 := Φ.number( φ ↦ 𝑛·2·7 )
+ 𝑛·2·13 := 𝑛·2·12.plus( x ↦ 𝑛·2·11 )
+ 𝔼(L_number_plus):
+ 𝔻(Φ.a🌵7):
+ 𝕄(Φ.a🌵7):
+ 𝑛·4·1 := Φ.number( φ ↦ 𝑛·2·7 )
+ 𝑛·4·2 := Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ )
+ 𝛿·4·1 := 40-1C-00-00-00-00-00-00 # 7.0
+ 𝛿1·4 := 𝛿·4·1 # 𝔻(ξ.ρ)
+ 𝔻(Φ.a🌵8):
+ 𝕄(Φ.a🌵8):
+ 𝑛·4·3 := Φ.number( φ ↦ 𝑛·2·10 )
+ 𝑛·4·4 := Φ.bytes( φ ↦ 40-20-00-00-00-00-00-00:Δ )
+ 𝛿·4·2 := 40-20-00-00-00-00-00-00 # 8.0
+ 𝛿2·4 := 𝛿·4·2 # 𝔻(ξ.x)
+ 𝑛·4·5 := Φ.number( φ ↦ 𝜎3:λ ) # 𝑛
+ 𝕄(𝑛·4·5):
+ 𝑛·4·6 := Φ.number( φ ↦ 𝜎3:λ )
+ 𝑛·4·7 := 𝑛·4·6 # 𝕄(𝑛·4·5)
𝑛2·2 := 𝑛·2·6 # 𝕄(ξ.else)
𝑛3·2 := 𝑛1·2 # 𝑛1
𝑛4·2 := 𝑛·2·6 # 𝑛2
- terminate(𝔻(𝜎1:λ), right) # 𝑛4
+ terminate(𝔻(𝜎1:λ), right, 𝑛·4·6) # 𝑛4
𝑛5·2 := 𝑛3·2 # [𝑛3, 𝑛4]
- 𝑛·2·7 := 𝑛5·2 # 𝑛
- 𝑛·2·8 := 𝑛5·2 # 𝕄(𝑛·2·7)
+ 𝑛·2·14 := 𝑛5·2 # 𝑛
+ 𝑛·2·15 := 𝑛5·2 # 𝕄(𝑛·2·14)
𝑛·0·5 := 𝑛·3·6.plus( x ↦ 6 )
𝕄(Φ.φ.x):
𝑛·0·6 := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ )
𝑛·0·7 := Φ.number( φ ↦ 𝑛·0·6 )
𝔼(L_number_plus):
- 𝔻(Φ.a🌵7):
- 𝕄(Φ.a🌵7):
- 𝑛·4·1 := Φ.number( φ ↦ 𝜎2:λ )
- 𝛿1·4 := 𝔻(𝜎2:λ) # 𝔻(ξ.ρ)
- 𝔻(Φ.a🌵8):
- 𝕄(Φ.a🌵8):
- 𝑛·4·2 := Φ.number( φ ↦ 𝑛·0·6 )
- 𝑛·4·3 := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ )
- 𝛿·4·1 := 40-18-00-00-00-00-00-00 # 6.0
- 𝛿2·4 := 𝛿·4·1 # 𝔻(ξ.x)
- 𝑛·4·4 := Φ.number( φ ↦ 𝜎3:λ ) # 𝑛
- 𝕄(𝑛·4·4):
- 𝑛·4·5 := Φ.number( φ ↦ 𝜎3:λ )
- 𝑛·4·6 := 𝑛·4·5 # 𝕄(𝑛·4·4)
+ 𝔻(Φ.a🌵9):
+ 𝕄(Φ.a🌵9):
+ 𝑛·5·1 := Φ.number( φ ↦ 𝜎2:λ )
+ 𝛿1·5 := 𝔻(𝜎2:λ) # 𝔻(ξ.ρ)
+ 𝔻(Φ.a🌵10):
+ 𝕄(Φ.a🌵10):
+ 𝑛·5·2 := Φ.number( φ ↦ 𝑛·0·6 )
+ 𝑛·5·3 := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ )
+ 𝛿·5·1 := 40-18-00-00-00-00-00-00 # 6.0
+ 𝛿2·5 := 𝛿·5·1 # 𝔻(ξ.x)
+ 𝑛·5·4 := Φ.number( φ ↦ 𝜎4:λ ) # 𝑛
+ 𝕄(𝑛·5·4):
+ 𝑛·5·5 := Φ.number( φ ↦ 𝜎4:λ )
+ 𝑛·5·6 := 𝑛·5·5 # 𝕄(𝑛·5·4)
diff --git a/test-resources/evaluate-packs/leaves-unfinished-a-message-no-entry-answers.yaml b/test-resources/evaluate-packs/leaves-unfinished-a-message-no-entry-answers.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/evaluate-packs/leaves-unfinished-a-message-no-entry-answers.yaml
@@ -0,0 +1,117 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+# yamllint disable rule:line-length
+# The walk reduces the message of the copy a branch raises with like any other
+# code, and leaves the call of 'L_number_nope', which no entry answers, as it
+# is written, the way it leaves any binding it cannot fire. The 'terminate'
+# line spells that message out, so the reader sees the error path is
+# unfinished (#1867).
+symbolic: |
+ - λ: L_number_gt
+ dataize:
+ 𝛿1: $.ρ
+ 𝛿2: $.x
+ 𝑛: Φ.bool( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
+ - λ: L_number_plus
+ dataize:
+ 𝛿1: $.ρ
+ 𝛿2: $.x
+ 𝑛: Φ.number( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
+ - λ: L_fork
+ dataize:
+ 𝛿1: $.ρ
+ morph:
+ 𝑛1: $.then
+ 𝑛2: $.else
+ symbolize:
+ 𝑛3: 𝑛1
+ 𝑛4: 𝑛2
+ join:
+ 𝑛5: [𝑛3, 𝑛4]
+ terminators: [L_throw]
+ 𝑛: 𝑛5
+location: 'Q.@'
+deep: true
+input: >
+ ⟦ bytes(φ) ↦ ⟦⟧,
+ error(message) ↦ ⟦ λ ⤍ L_throw ⟧,
+ bool(φ) ↦ ⟦ if ↦ ⟦ ρ ↦ ∅, then ↦ ∅, else ↦ ∅, λ ⤍ L_fork ⟧ ⟧,
+ number(φ) ↦ ⟦
+ gt(ρ, x) ↦ ⟦ λ ⤍ L_number_gt ⟧,
+ plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧,
+ nope(ρ, x) ↦ ⟦ λ ⤍ L_number_nope ⟧ ⟧,
+ @ ↦ 5.gt( 0 ).if( then ↦ 1, else ↦ Φ.error( message ↦ 7.nope( 8 ) ) ).plus( 6 ) ⟧
+result: |-
+ ⟦ φ ↦ 𝜎3:λ, gt(x) ↦ L_number_gt:λ, plus(x) ↦ L_number_plus:λ, nope(x) ↦ L_number_nope:λ ⟧
+protocol: |
+ 𝕄(Φ.φ):
+ 𝑛·0·1 := 5
+ 𝑛·0·2 := 𝑛·0·1.gt( x ↦ 0 )
+ 𝔼(L_number_gt):
+ 𝔻(Φ.a🌵0):
+ 𝕄(Φ.a🌵0):
+ 𝑛·1·1 := 5
+ 𝑛·1·2 := Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )
+ 𝛿·1·1 := 40-14-00-00-00-00-00-00 # 5.0
+ 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.ρ)
+ 𝔻(Φ.a🌵1):
+ 𝕄(Φ.a🌵1):
+ 𝑛·1·3 := 0
+ 𝑛·1·4 := Φ.bytes( φ ↦ 00-00-00-00-00-00-00-00:Δ )
+ 𝛿·1·2 := 00-00-00-00-00-00-00-00 # 0.0
+ 𝛿2·1 := 𝛿·1·2 # 𝔻(ξ.x)
+ 𝑛·1·5 := Φ.bool( φ ↦ 𝜎1:λ ) # 𝑛
+ 𝕄(𝑛·1·5):
+ 𝑛·1·6 := Φ.bool( φ ↦ 𝜎1:λ )
+ 𝑛·1·7 := 𝑛·1·6 # 𝕄(𝑛·1·5)
+ 𝑛·0·3 := 𝑛·1·6.if( then ↦ 1 )
+ 𝑛·0·4 := 𝑛·0·3( else ↦ Φ.error( message ↦ 7.nope( 8 ) ) )
+ 𝔼(L_fork):
+ 𝔻(Φ.a🌵2):
+ 𝕄(Φ.a🌵2):
+ 𝑛·2·1 := Φ.bool( φ ↦ 𝜎1:λ )
+ 𝛿1·2 := 𝔻(𝜎1:λ) # 𝔻(ξ.ρ)
+ 𝕄(Φ.a🌵3):
+ 𝑛·2·2 := 1
+ 𝕄(Φ.a🌵3.φ):
+ 𝑛·2·3 := Φ.bytes( φ ↦ 3F-F0-00-00-00-00-00-00:Δ )
+ 𝑛1·2 := 𝑛·2·2 # 𝕄(ξ.then)
+ 𝕄(Φ.a🌵4):
+ 𝑛·2·4 := Φ.error( message ↦ 7.nope( 8 ) )
+ 𝕄(Φ.a🌵4.message):
+ 𝑛·2·5 := Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ )
+ 𝑛·2·6 := Φ.number( φ ↦ 𝑛·2·5 )
+ 𝑛·2·7 := Φ.number( φ ↦ 𝑛·2·5 )
+ 𝑛·2·8 := Φ.bytes( φ ↦ 40-20-00-00-00-00-00-00:Δ )
+ 𝑛·2·9 := Φ.number( φ ↦ 𝑛·2·8 )
+ 𝑛·2·10 := Φ.number( φ ↦ 𝑛·2·5 )
+ 𝑛·2·11 := 𝑛·2·10.nope( x ↦ 𝑛·2·9 )
+ 𝑛2·2 := 𝑛·2·4 # 𝕄(ξ.else)
+ 𝔻(𝜎2:λ) == 3F-F0-00-00-00-00-00-00
+ 𝑛3·2 := ⟦ φ ↦ Φ.bytes( φ ↦ 𝜎2:λ ), gt(x) ↦ L_number_gt:λ, plus(x) ↦ L_number_plus:λ, nope(x) ↦ L_number_nope:λ ⟧ # 𝑛1
+ 𝑛4·2 := 𝑛·2·4 # 𝑛2
+ terminate(𝔻(𝜎1:λ), right, 𝑛·2·10.nope( 𝑛·2·9 )) # 𝑛4
+ 𝑛5·2 := 𝑛3·2 # [𝑛3, 𝑛4]
+ 𝑛·2·12 := 𝑛5·2 # 𝑛
+ 𝑛·2·13 := 𝑛5·2 # 𝕄(𝑛·2·12)
+ 𝑛·0·5 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎2:λ ) ).plus( x ↦ 6 )
+ 𝕄(Φ.φ.x):
+ 𝑛·0·6 := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ )
+ 𝑛·0·7 := Φ.number( φ ↦ 𝑛·0·6 )
+ 𝔼(L_number_plus):
+ 𝔻(Φ.a🌵5):
+ 𝕄(Φ.a🌵5):
+ 𝑛·3·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎2:λ ) )
+ 𝑛·3·2 := Φ.bytes( φ ↦ 𝜎2:λ )
+ 𝛿1·3 := 𝔻(𝜎2:λ) # 𝔻(ξ.ρ)
+ 𝔻(Φ.a🌵6):
+ 𝕄(Φ.a🌵6):
+ 𝑛·3·3 := Φ.number( φ ↦ 𝑛·0·6 )
+ 𝑛·3·4 := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ )
+ 𝛿·3·1 := 40-18-00-00-00-00-00-00 # 6.0
+ 𝛿2·3 := 𝛿·3·1 # 𝔻(ξ.x)
+ 𝑛·3·5 := Φ.number( φ ↦ 𝜎3:λ ) # 𝑛
+ 𝕄(𝑛·3·5):
+ 𝑛·3·6 := Φ.number( φ ↦ 𝜎3:λ )
+ 𝑛·3·7 := 𝑛·3·6 # 𝕄(𝑛·3·5)
diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs
--- a/test/DataizeSpec.hs
+++ b/test/DataizeSpec.hs
@@ -173,14 +173,14 @@
looping $ \endless -> do
expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_loop ⟧ ⟧"
minted <- newIORef 0
- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing minted Nothing Nothing 1 Nothing False True False False 1 Nothing Dataization [] Map.empty endless [] (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
+ dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing minted Nothing Nothing 1 Nothing False True False False 1 Nothing Dataization [] Map.empty endless (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
`shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException))
it "parks the step limit as a residual with --partial" $
looping $ \endless -> do
expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_loop ⟧ ⟧"
minted <- newIORef 0
- (outcome, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing minted Nothing Nothing 1 Nothing False True True False 1 Nothing Dataization [] Map.empty endless [] (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
+ (outcome, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing minted Nothing Nothing 1 Nothing False True True False 1 Nothing Dataization [] Map.empty endless (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
case outcome of
Residual _ -> pure ()
Dataized bts -> expectationFailure ("expected a residual, dataized to " ++ show bts)
@@ -265,12 +265,12 @@
forM_
[
( "--max-cycles"
- , \minted -> ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing True True False False 1 Nothing Dataization [] Map.empty emptyLambdas [] (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked
+ , \minted -> ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing True True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked
, "--max-cycles=0"
)
,
( "--max-depth"
- , \minted -> ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing True True False False 1 Nothing Dataization [] Map.empty emptyLambdas [] (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked
+ , \minted -> ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing True True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked
, "--max-depth=0"
)
]
@@ -283,12 +283,12 @@
it "does not throw without --depth-sensitive even once --max-depth is exhausted" $ do
expr <- parseExpressionThrows boxed
minted <- newIORef 0
- (value, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False False 1 Nothing Dataization [] Map.empty emptyLambdas [] (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
+ (value, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
value `shouldBe` Dataized (BtOne "00")
it "throws once --max-cycles is exhausted even without --depth-sensitive" $ do
expr <- parseExpressionThrows boxed
minted <- newIORef 0
- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False False 1 Nothing Dataization [] Map.empty emptyLambdas [] (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
+ dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
`shouldThrow` (\e -> "--max-cycles=0" `isInfixOf` show (e :: SomeException))
describe "labels every step with a defined rule or operation" $ do
diff --git a/test/DepsSpec.hs b/test/DepsSpec.hs
--- a/test/DepsSpec.hs
+++ b/test/DepsSpec.hs
@@ -11,7 +11,7 @@
import Data.IORef (modifyIORef', newIORef, readIORef)
import Data.List (isInfixOf, isPrefixOf)
import Data.Time.Clock.POSIX (getPOSIXTime)
-import Deps (Acyclic (Proven), Evaluation (EvAnswer, EvApplied, EvBuilt, EvComputed, EvData, EvDeferred, EvDelta, EvFiring, EvJoined, EvLooped, EvMinted, EvRun, EvStarted, EvTerm), Judgment (Dataization, Morphing), Nesting (..), Protocol (..), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, renumbered, resited, saveStep)
+import Deps (Acyclic (Proven), Evaluation (EvAnswer, EvApplied, EvBuilt, EvComputed, EvData, EvDeferred, EvDelta, EvFiring, EvJoined, EvLooped, EvMinted, EvRun, EvStarted, EvTerm, EvTerminate), Judgment (Dataization, Morphing), Nesting (..), Protocol (..), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, renumbered, resited, saveStep)
import Fixtures (readUtf8, recorded, recordedXml)
import GHC.Clock (getMonotonicTime)
import Logger (LogLevel (DEBUG, ERROR, INFO), setLogConfig)
@@ -145,6 +145,10 @@
case renumbered 1 3 (EvStarted 2 Morphing (ExFormation [BiLambda (FnSymbol 5)])) of
EvStarted _ _ site -> symbols site `shouldBe` [8]
_ -> expectationFailure "The record did not stay the record it was"
+ it "raises the symbols the message of a raising fork carries above the floor" $
+ case renumbered 2 5 (EvTerminate 3 (Just (Left 1)) "right" "𝑛4" (Just (ExApplication (ExDispatch ExRoot (AtLabel "ёрш")) (ArTau AtPhi (ExFormation [BiLambda (FnSymbol 6)]))))) of
+ EvTerminate _ _ _ _ message -> fmap symbols message `shouldBe` Just [11]
+ _ -> expectationFailure "The record did not stay the record it was"
describe "resited" $ do
it "moves an application made at one site to another" $
@@ -234,6 +238,12 @@
it "names the block over an answer by the line that built it" $ do
(_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_ф" Dataization ExRoot, EvBuilt 2 (ExDispatch ExRoot (AtLabel "ю")), EvStarted 2 Morphing (ExDispatch ExRoot (AtLabel "ю")), EvApplied 3 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) (ExDispatch ExRoot (AtLabel "ю"))])
lines written `shouldContain` [" 𝕄(𝑛·1·1):"]
+ it "names the message a fork raises with by the name its application gave it" $ do
+ (_, written) <- recorded (\record -> mapM_ record [EvFiring 1 "L_ф" Morphing ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) ExRoot, EvTerminate 2 (Just (Left 7)) "right" "𝑛4" (Just (ExFormation [BiTau (AtLabel "q") (ExFormation [])]))])
+ last (lines written) `shouldBe` " terminate(𝔻(𝜎7:λ), right, 𝑛·1·1) # 𝑛4"
+ it "writes no message for a fork that raises with none" $ do
+ (_, written) <- recorded (\record -> mapM_ record [EvFiring 1 "L_ф" Morphing ExRoot, EvTerminate 2 (Just (Right (BtOne "0D"))) "left" "𝑛3" Nothing])
+ last (lines written) `shouldBe` " terminate(0D-, left) # 𝑛3"
it "writes no line for an object the walk computed inside" $ do
(_, written) <- recorded (\record -> record (EvComputed 1 (ExFormation [BiTau (AtLabel "ю") ExRoot]) (ExFormation [BiTau (AtLabel "ю") (ExFormation [BiLambda (FnSymbol 3)])])))
written `shouldBe` ""
@@ -278,6 +288,12 @@
it "names the element over an answer by the element that built it" $ do
(_, written) <- recordedXml (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_ф" Dataization ExRoot, EvBuilt 2 (ExDispatch ExRoot (AtLabel "ю")), EvStarted 2 Morphing (ExDispatch ExRoot (AtLabel "ю")), EvApplied 3 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) (ExDispatch ExRoot (AtLabel "ю"))])
lines written `shouldContain` [" "]
+ it "names the message a fork raises with by the name its application gave it in the markup" $ do
+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) ExRoot, EvTerminate 2 (Just (Left 7)) "right" "𝑛4" (Just (ExFormation [BiTau (AtLabel "q") (ExFormation [])]))])
+ lines written `shouldContain` [" "]
+ it "writes the message a fork raises with beside the datum of its condition" $ do
+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvTerminate 1 (Just (Right (BtOne "0D"))) "left" "𝑛3" (Just (ExDispatch ExRoot (AtLabel "щука")))])
+ lines written `shouldContain` [" 0D-"]
describe "perSecond" $ do
it "divides the firings by the seconds the run took" $
diff --git a/test/Fixtures.hs b/test/Fixtures.hs
--- a/test/Fixtures.hs
+++ b/test/Fixtures.hs
@@ -55,7 +55,7 @@
defaultReduceContext :: Expression -> IO ReduceContext
defaultReduceContext loc = do
minted <- newIORef 0
- pure (ReduceContext loc loc Nothing 25 25 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False False 1 Nothing Morphing [] Map.empty emptyLambdas [] (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
+ pure (ReduceContext loc loc Nothing 25 25 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False False 1 Nothing Morphing [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
linked :: Engine
linked = fromMaybe yaml compiled
diff --git a/test/LambdasSpec.hs b/test/LambdasSpec.hs
--- a/test/LambdasSpec.hs
+++ b/test/LambdasSpec.hs
@@ -12,7 +12,7 @@
import Data.List (isInfixOf)
import Data.Text qualified as T
import Fixtures (withLambdasOf)
-import Lambdas (Lambda (..), Lambdas, Meta (..), emptyLambdas, joined, matched, minted, readLambdas, symbolized, taken, thrown)
+import Lambdas (Lambda (..), Lambdas, Meta (..), emptyLambdas, joined, matched, message, minted, readLambdas, symbolized, taken, thrown)
import Parser (parseExpressionThrows)
import Test.Hspec
@@ -215,9 +215,9 @@
, "the terminator 'L_throw' of the key 'L_fork' is answered by the key 'L_th[a-z]+'"
)
]
- ( \(desc, text, message) ->
+ ( \(desc, text, reason) ->
it ("cannot read " ++ desc) $
- lambdasOf text `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException))
+ lambdasOf text `shouldThrow` (\err -> reason `isInfixOf` show (err :: SomeException))
)
describe "emptyLambdas" $
@@ -483,6 +483,29 @@
it ("finds no terminator in " ++ desc) $ do
term <- parseExpressionThrows text
thrown ["L_throw"] term `shouldBe` False
+ )
+
+ describe "message" $ do
+ it "finds the message a formation that throws carries" $ do
+ said <- parseExpressionThrows "Φ.pike( φ ↦ ⟦ λ ⤍ 𝜎9 ⟧ )"
+ term <- parseExpressionThrows "⟦ message ↦ Φ.pike( φ ↦ ⟦ λ ⤍ 𝜎9 ⟧ ), λ ⤍ L_throw ⟧"
+ message term `shouldBe` Just said
+
+ it "finds the message an application gives a formation that throws" $ do
+ said <- parseExpressionThrows "ξ.hog.printf( ξ.y )"
+ term <- parseExpressionThrows "⟦ message ↦ ∅, code ↦ ∅, λ ⤍ L_throw ⟧( message ↦ ξ.hog.printf( ξ.y ) )( code ↦ Φ.z )"
+ message term `shouldBe` Just said
+
+ forM_
+ [ ("the terminator ⊥" :: String, "⊥" :: String)
+ , ("a formation whose message is void", "⟦ message ↦ ∅, λ ⤍ L_throw ⟧")
+ , ("a formation that carries no message", "⟦ code ↦ Φ.cat, λ ⤍ L_throw ⟧")
+ , ("an application that gives no message", "⟦ message ↦ ∅, code ↦ ∅, λ ⤍ L_throw ⟧( code ↦ Φ.cat )")
+ ]
+ ( \(desc, text) ->
+ it ("finds no message in " ++ desc) $ do
+ term <- parseExpressionThrows text
+ message term `shouldBe` Nothing
)
describe "taken" $ do