phino 0.0.148 → 0.0.149
raw patch · 33 files changed
+436/−204 lines, 33 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Deps: [_minted] :: State -> Int
+ CLI.Parsers: optAbridgedData :: Parser Bool
+ CLI.Types: [_abridgedData] :: OptsMorph -> Bool
+ Morph: [_minted] :: ReduceContext -> IORef Int
- Abridge: abridged :: Int -> EXPRESSION -> EXPRESSION
+ Abridge: abridged :: Bool -> Int -> EXPRESSION -> EXPRESSION
- CLI.Helpers: started :: Expression -> State
+ CLI.Helpers: started :: Expression -> ReduceContext -> IO ()
- CLI.Types: OptsDataize :: LogLevel -> Int -> IOFormat -> IOFormat -> SugarType -> Bool -> LineFormat -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Maybe Acyclic -> Bool -> Int -> Int -> Int -> Maybe Int -> Maybe Int -> Int -> Maybe Int -> Maybe Int -> [String] -> [String] -> String -> String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe FilePath -> Maybe FilePath -> Maybe Int -> Maybe FilePath -> Maybe FilePath -> OptsDataize
+ CLI.Types: OptsDataize :: LogLevel -> Int -> IOFormat -> IOFormat -> SugarType -> Bool -> LineFormat -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Maybe Acyclic -> Bool -> Int -> Int -> Int -> Maybe Int -> Maybe Int -> Int -> Maybe Int -> Maybe Int -> [String] -> [String] -> String -> String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe FilePath -> Maybe FilePath -> Maybe Int -> Bool -> Maybe FilePath -> Maybe FilePath -> OptsDataize
- CLI.Types: OptsMorph :: LogLevel -> Int -> IOFormat -> IOFormat -> SugarType -> Bool -> LineFormat -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Bool -> Int -> Maybe Acyclic -> Bool -> Int -> Int -> Int -> Maybe Int -> Maybe Int -> Int -> Maybe Int -> Maybe Int -> [String] -> [String] -> String -> String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe FilePath -> Maybe FilePath -> Maybe Int -> Maybe FilePath -> Maybe FilePath -> OptsMorph
+ CLI.Types: OptsMorph :: LogLevel -> Int -> IOFormat -> IOFormat -> SugarType -> Bool -> LineFormat -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Bool -> Int -> Maybe Acyclic -> Bool -> Int -> Int -> Int -> Maybe Int -> Maybe Int -> Int -> Maybe Int -> Maybe Int -> [String] -> [String] -> String -> String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe FilePath -> Maybe FilePath -> Maybe Int -> Bool -> Maybe FilePath -> Maybe FilePath -> OptsMorph
- CLI.Types: PrintCtx :: SugarType -> Bool -> Maybe Int -> LineFormat -> Int -> XmirContext -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Int -> Expression -> Maybe String -> Maybe String -> Maybe String -> IOFormat -> PrintContext
+ CLI.Types: PrintCtx :: SugarType -> Bool -> Maybe Int -> Bool -> LineFormat -> Int -> XmirContext -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Int -> Expression -> Maybe String -> Maybe String -> Maybe String -> IOFormat -> PrintContext
- Deps: State :: Int -> Maybe Int -> Maybe Text -> State
+ Deps: State :: Maybe Int -> Maybe Text -> State
- Filter: exclude :: [Rewritten] -> [Expression] -> [Rewritten]
+ Filter: exclude :: [Rewritten] -> [Expression] -> IO [Rewritten]
- Filter: exclude' :: Expression -> [Expression] -> Expression
+ Filter: exclude' :: Expression -> [Expression] -> IO Expression
- Morph: ReduceContext :: Expression -> Expression -> Maybe Expression -> Int -> Int -> Steps -> Maybe Tally -> Maybe Deadline -> Maybe Memo -> Int -> Bool -> Bool -> Bool -> Bool -> Int -> Maybe Acyclic -> Judgment -> [Text] -> Seen -> Lambdas -> BuildTermFunc -> ReductionFunc -> EvaluationFunc -> FiringFunc -> SaveStepFunc -> SaveEvalFunc -> Engine -> ReduceContext
+ Morph: ReduceContext :: Expression -> Expression -> Maybe Expression -> Int -> Int -> Steps -> Maybe Tally -> IORef Int -> Maybe Deadline -> Maybe Memo -> Int -> Bool -> Bool -> Bool -> Bool -> Int -> Maybe Acyclic -> Judgment -> [Text] -> Seen -> Lambdas -> BuildTermFunc -> ReductionFunc -> EvaluationFunc -> FiringFunc -> SaveStepFunc -> SaveEvalFunc -> Engine -> ReduceContext
Files
- README.md +23/−6
- benchmark/Main.hs +9/−4
- phino.cabal +1/−1
- src/Abridge.hs +3/−3
- src/CLI/Helpers.hs +7/−7
- src/CLI/Parsers.hs +13/−3
- src/CLI/Runners.hs +20/−9
- src/CLI/Types.hs +3/−0
- src/Deps.hs +1/−2
- src/Evaluate.hs +26/−23
- src/Filter.hs +17/−21
- src/Functions.hs +1/−0
- src/LaTeX.hs +6/−3
- src/Morph.hs +33/−35
- src/Parser.hs +18/−5
- src/Rewriter.hs +1/−1
- src/Sugar.hs +12/−1
- src/XMIR.hs +4/−2
- src/Yaml.hs +23/−0
- test/AbridgeSpec.hs +21/−9
- test/CLIHelpersSpec.hs +1/−1
- test/CLISpec.hs +38/−2
- test/CompiledSpec.hs +4/−4
- test/DataizeSpec.hs +31/−21
- test/EvaluateSpec.hs +13/−8
- test/FilterSpec.hs +16/−13
- test/Fixtures.hs +6/−2
- test/FunctionsSpec.hs +13/−0
- test/LaTeXSpec.hs +11/−0
- test/MorphSpec.hs +26/−17
- test/ParserSpec.hs +14/−0
- test/XMIRSpec.hs +6/−0
- test/YamlSpec.hs +15/−1
README.md view
@@ -34,7 +34,7 @@ ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.145+cabal install --overwrite-policy=always phino-0.0.148 phino --version ``` @@ -875,11 +875,11 @@ run fills the protocol with lines tens of thousands of characters long. The `--abridged` option shortens every term the protocol writes, in the text and the XML alike: a formation longer than sixty-four characters keeps its `φ`,-`Δ` and `λ` bindings and folds the rest into a count, and a byte string longer-than eight bytes keeps its first two bytes and its last two, with the count of-the bytes cut out between them. The width is a value of the option,-`--abridged=120`, for a run that can read longer lines. The result the run-prints stays whole, and the option is refused without `--protocol`:+`Δ` and `λ` bindings and folds the rest into a count. The width is a value of+the option, `--abridged=120`, for a run that can read longer lines. The result+the run prints stays whole, and the option is refused without `--protocol`.+Every byte string the protocol writes stays whole too, since a reader may need+the data a firing came down to: <!-- markdownlint-disable MD013 --> @@ -895,6 +895,23 @@ ⟧ $ phino dataize --locator=Q.t --protocol=wide.txt --abridged --quiet \ --sweet --hide-rho wide.phi+$ cat wide.txt+𝔻(Φ.t)+ formation(⟦ φ ↦ 48-65-6C-6C-6F-2C-20-77-6F-72-6C-64:Δ, +3 ⟧) # 𝔻(Φ.t)+```++<!-- markdownlint-enable MD013 -->++The `--abridged-data` option cuts the data too: a byte string longer than eight+bytes keeps its first two bytes and its last two, with the count of the bytes+cut out between them. A formation folded into a count loses its data either+way, and the option is refused without `--abridged`:++<!-- markdownlint-disable MD013 -->++```bash+$ phino dataize --locator=Q.t --protocol=wide.txt --abridged \+ --abridged-data --quiet --sweet --hide-rho wide.phi $ cat wide.txt 𝔻(Φ.t) formation(⟦ φ ↦ 48-65-..(8b)..-6C-64:Δ, +3 ⟧) # 𝔻(Φ.t)
benchmark/Main.hs view
@@ -8,6 +8,7 @@ import Compiled (compiled) import Control.Exception (evaluate) import Control.Monad (replicateM, replicateM_)+import Data.IORef (IORef, newIORef) import qualified Data.List.NonEmpty as NE import qualified Data.Map.Strict as Map import Data.Maybe (fromMaybe)@@ -22,7 +23,7 @@ import Lining (LineFormat (MULTILINE, SINGLELINE)) import Margin (defaultMargin) import Merge (merge)-import Morph (Memo, ReduceContext (ReduceContext), Steps (Steps), memoized, morph)+import Morph (Memo, ReduceContext (ReduceContext), Steps (Steps), emptyState, memoized, morph) import Must (Must (MtDisabled)) import Parser (parseExpressionThrows) import Printer (printExpression')@@ -60,8 +61,8 @@ Nothing dontSaveStep -symbolicCtx :: Acyclic -> Maybe Memo -> Lambdas -> Expression -> ReduceContext-symbolicCtx acyclic memo lambdas locator =+symbolicCtx :: Acyclic -> Maybe Memo -> IORef Int -> Lambdas -> Expression -> ReduceContext+symbolicCtx acyclic memo minted lambdas locator = ReduceContext locator locator@@ -70,6 +71,7 @@ 25 (Steps 1000 0) Nothing+ minted Nothing memo 1@@ -192,5 +194,8 @@ symbolic acyclic universe lambdas locator = do seedTaus universe memo <- memoized (Just acyclic)- (answer, _, _) <- morph universe (started universe) (symbolicCtx acyclic memo lambdas locator)+ minted <- newIORef 0+ let ctx = symbolicCtx acyclic memo minted lambdas locator+ started universe ctx+ (answer, _, _) <- morph universe emptyState ctx pure (hashExpression answer)
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.148+version: 0.0.149 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
src/Abridge.hs view
@@ -10,8 +10,8 @@ import Lining (toSingleLine) import Render (render) -abridged :: Int -> EXPRESSION -> EXPRESSION-abridged width = goExpr+abridged :: Bool -> Int -> EXPRESSION -> EXPRESSION+abridged cut width = goExpr where goExpr :: EXPRESSION -> EXPRESSION goExpr expr@EX_FORMATION{..}@@ -68,7 +68,7 @@ goAppArgs AAS_EMPTY = AAS_EMPTY goBytes :: BYTES -> BYTES goBytes (BT_MANY bts)- | length bts > 8 = BT_CUT (take 2 bts) (length bts - 4) (drop (length bts - 2) bts)+ | cut && length bts > 8 = BT_CUT (take 2 bts) (length bts - 4) (drop (length bts - 2) bts) goBytes bts = bts short :: EXPRESSION -> Bool short expr = T.length (render (toSingleLine expr)) <= width
src/CLI/Helpers.hs view
@@ -23,7 +23,7 @@ import qualified Data.Map.Strict as M import Data.Maybe import qualified Data.Text as T-import Deps (Evaluation (EvRun), Judgment, SaveEvalFunc, SaveStepFunc, State (..), dontSaveEval, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, progressed, saveEval, saveEvalXml, saveStep)+import Deps (Evaluation (EvRun), Judgment, SaveEvalFunc, SaveStepFunc, dontSaveEval, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, progressed, saveEval, saveEvalXml, saveStep) import Encoding import Engine (Engine, fresh, yaml) import Files (ensuredFile, overwrite)@@ -35,7 +35,7 @@ import Lining (LineFormat (SINGLELINE)) import Locator (locatedExpression) import Logger-import Morph (ReduceContext, emptyState, insideUniverse)+import Morph (ReduceContext (..), insideUniverse) import Parser (parseExpressionThrows) import qualified Printer as P import qualified Random as R@@ -63,8 +63,8 @@ | _outputFormat == LATEX = "tex" | otherwise = show _outputFormat render expr = do- shown <- F.include' expr included- printInFormat ctx ((if _canonize then canonizeExpr else id) (F.exclude' shown excluded))+ shown <- F.include' expr included >>= (`F.exclude'` excluded)+ printInFormat ctx ((if _canonize then canonizeExpr else id) shown) save :: SaveStepFunc save expr = do step <- atomicModifyIORef' counter (\value -> (value + 1, value + 1))@@ -118,8 +118,8 @@ logDebug (printf "The option '--symbolic' is specified, reading the λ functions from '%s'" file) ensuredFile file >>= readLambdas -started :: Expression -> State-started expr = emptyState{_minted = taken expr}+started :: Expression -> ReduceContext -> IO ()+started expr ctx = writeIORef ctx._minted (taken expr) heading :: SaveEvalFunc -> PrintContext -> Judgment -> Expression -> IO () heading record ctx judgment locator =@@ -130,7 +130,7 @@ pure (P.printExpressionWith shaped expr (_sugar, UNICODE, SINGLELINE, _margin)) where shaped :: SugarType -> EXPRESSION -> EXPRESSION- shaped sugar = maybe id abridged _abridged . hidden ctx sugar+ shaped sugar = maybe id (abridged _abridgedData) _abridged . hidden ctx sugar salted :: PrintContext -> Expression -> IO String salted ctx = flattened ctx{_sugar = SALTY}
src/CLI/Parsers.hs view
@@ -290,13 +290,21 @@ ( long "abridged" <> help "Shorten every 𝜑-expression written to the --protocol file: a formation longer than the width \- \keeps its φ, Δ and λ bindings and folds the rest into a count, as '+34', and a byte string \- \longer than eight bytes keeps its first two bytes and its last two with the count of the bytes \- \between them, as '00-00-..(45b)..-FF-EE'; the width is 64 characters unless given as --abridged=WIDTH"+ \keeps its φ, Δ and λ bindings and folds the rest into a count, as '+34', while every byte string \+ \it writes stays whole; the width is 64 characters unless given as --abridged=WIDTH" ) <|> option auto (long "abridged" <> metavar "WIDTH" <> internal) ) +optAbridgedData :: Parser Bool+optAbridgedData =+ switch+ ( long "abridged-data"+ <> help+ "Cut every byte string longer than eight bytes that the --abridged protocol writes to its first \+ \two bytes and its last two with the count of the bytes between them, as '00-00-..(45b)..-FF-EE'"+ )+ optShuffle :: Parser Bool optShuffle = switch (long "shuffle" <> help "Shuffle rules before applying") @@ -408,6 +416,7 @@ <*> optStepsDir <*> optProtocol <*> optAbridged+ <*> optAbridgedData <*> optSymbolic <*> argInputFile )@@ -457,6 +466,7 @@ <*> optStepsDir <*> optProtocol <*> optAbridged+ <*> optAbridgedData <*> optSymbolic <*> argInputFile )
src/CLI/Runners.hs view
@@ -16,6 +16,7 @@ import Control.Exception import Control.Monad (unless, when) import Data.Foldable (traverse_)+import Data.IORef (newIORef) import Data.List (intercalate) import qualified Data.List.NonEmpty as NE import qualified Data.Map.Strict as Map@@ -76,7 +77,7 @@ save <- saveStepFunc _stepsDir printCtx included excluded let steps = map (stepOf linked) rules (rewrittens, exceeded) <- rewrite expr steps (RewriteContext loc _maxDepth _maxCycles _depthSensitive Nothing (building linked) linked._normal (every steps) _must _breakpoint save)- rewrittens' <- exclude <$> include (if _sequence then NE.toList rewrittens else [NE.last rewrittens])+ rewrittens' <- include (if _sequence then NE.toList rewrittens else [NE.last rewrittens]) >>= exclude logDebug (printf "Printing rewritten 𝜑-expression as %s" (show _outputFormat)) exprs <- printRewrittens printCtx (rewrittens', exceeded) output _targetFile exprs@@ -138,6 +139,7 @@ _sugarType _hideRho Nothing+ False _flat _margin xmirCtx@@ -173,6 +175,7 @@ include = (`F.include` included) save <- saveStepFunc _stepsDir printCtx included excluded tally <- tallied _maxFirings+ minted <- newIORef 0 memo <- memoized _acyclic linked <- engine (outcome, chain, _) <-@@ -180,13 +183,14 @@ _protocol printCtx ( \record -> do- let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally deadline memo 1 _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 _depthSensitive _shuffle _partial False 1 _acyclic Dataization [] Map.empty lambdas (building linked) reduction evaluation fired save record linked (universe, aiming) <- aimed _inside expr ctx heading record printCtx Dataization aiming._locator- dataize universe (started universe) aiming+ started universe aiming+ dataize universe emptyState aiming )- when _sequence (include chain >>= \shown -> printRewrittens printCtx (exclude shown, False) >>= putStrLn)- unless _quiet (printOutcome printCtx (\residue -> (`F.exclude'` excluded) <$> F.include' residue included) outcome >>= putStrLn)+ when _sequence (include chain >>= exclude >>= \shown -> printRewrittens printCtx (shown, False) >>= putStrLn)+ unless _quiet (printOutcome printCtx (\residue -> F.include' residue included >>= (`F.exclude'` excluded)) outcome >>= putStrLn) where printOutcome :: PrintContext -> (Expression -> IO Expression) -> Outcome -> IO String printOutcome _ _ (Dataized bytes) = pure (P.printBytes bytes)@@ -205,6 +209,7 @@ validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus when (length _show > 1) (invalidCLIArguments "The option --show can be used only once") when (isJust _abridged && isNothing _protocol) (invalidCLIArguments "The option --abridged requires --protocol, since only the protocol is abridged")+ when (_abridgedData && isNothing _abridged) (invalidCLIArguments "The option --abridged-data requires --abridged, since only an abridged protocol cuts its data") when (isJust _inside && _locator /= "Q") (invalidCLIArguments "The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")@@ -214,6 +219,7 @@ _sugarType _hideRho _abridged+ _abridgedData _flat _margin (XmirContext _omitListing _omitComments _hideRho listing atoms)@@ -252,6 +258,7 @@ include = (`F.include` included) save <- saveStepFunc _stepsDir printCtx included excluded tally <- tallied _maxFirings+ minted <- newIORef 0 memo <- memoized _acyclic linked <- engine (morphed, chain, _) <-@@ -259,19 +266,20 @@ _protocol printCtx ( \record -> do- let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally deadline memo 1 _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 _depthSensitive _shuffle _partial _deep _jobs _acyclic Morphing [] Map.empty lambdas (building linked) reduction evaluation fired save record linked (universe, aiming) <- aimed _inside expr ctx heading record printCtx Morphing aiming._locator- morph universe (started universe) aiming+ started universe aiming+ morph universe emptyState aiming ) printed <- if _quiet then pure Nothing else do- answer <- (`F.exclude'` excluded) <$> F.include' (if foc == ExRoot then morphed else maybe morphed fst (lastMaybe chain)) included+ answer <- F.include' (if foc == ExRoot then morphed else maybe morphed fst (lastMaybe chain)) included >>= (`F.exclude'` excluded) validateXmirTopLevel _outputFormat answer Just <$> printAnswer printCtx answer- when _sequence (include chain >>= \shown -> printRewrittens printCtx (exclude shown, False) >>= putStrLn)+ when _sequence (include chain >>= exclude >>= \shown -> printRewrittens printCtx (shown, False) >>= putStrLn) mapM_ putStrLn printed where lastMaybe :: [a] -> Maybe a@@ -287,6 +295,7 @@ validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus when (length _show > 1) (invalidCLIArguments "The option --show can be used only once") when (isJust _abridged && isNothing _protocol) (invalidCLIArguments "The option --abridged requires --protocol, since only the protocol is abridged")+ when (_abridgedData && isNothing _abridged) (invalidCLIArguments "The option --abridged-data requires --abridged, since only an abridged protocol cuts its data") when (_jobs > 1 && not _deep) (invalidCLIArguments "The option --jobs requires --deep, since only the deep walk runs on several workers") when (isJust _inside && _locator /= "Q")@@ -297,6 +306,7 @@ _sugarType _hideRho _abridged+ _abridgedData _flat _margin (XmirContext _omitListing _omitComments _hideRho listing atoms)@@ -363,6 +373,7 @@ _sugarType False Nothing+ False _flat _margin xmirCtx
src/CLI/Types.hs view
@@ -20,6 +20,7 @@ { _sugar :: SugarType , _hideRho :: Bool , _abridged :: Maybe Int+ , _abridgedData :: Bool , _line :: LineFormat , _margin :: Int , _xmirCtx :: XmirContext@@ -126,6 +127,7 @@ , _stepsDir :: Maybe FilePath , _protocol :: Maybe FilePath , _abridged :: Maybe Int+ , _abridgedData :: Bool , _symbolic :: Maybe FilePath , _inputFile :: Maybe FilePath }@@ -172,6 +174,7 @@ , _stepsDir :: Maybe FilePath , _protocol :: Maybe FilePath , _abridged :: Maybe Int+ , _abridgedData :: Bool , _symbolic :: Maybe FilePath , _inputFile :: Maybe FilePath }
src/Deps.hs view
@@ -35,8 +35,7 @@ type BuildTermMethod = [ExtraArgument] -> Subst -> IO Term data State = State- { _minted :: Int- , _manufactured :: Maybe Int+ { _manufactured :: Maybe Int , _stuck :: Maybe T.Text }
src/Evaluate.hs view
@@ -11,6 +11,7 @@ import Builder (buildExpressionThrows) import Control.Exception (catch, throwIO, try) import Control.Monad (foldM, unless)+import Data.IORef (readIORef, writeIORef) import Data.List (partition) import Data.List.NonEmpty (NonEmpty (..)) import Data.Maybe (fromMaybe, isNothing, listToMaybe)@@ -85,9 +86,9 @@ worked :: ReduceContext -> Lambda -> Firing -> Subst -> State -> IO (Answer, State) worked ctx entry firing@(Firing _ operands _) bound state' = do rewrote <- foldM (reshaped ctx) bound entry._rewritten- (bound', stood) <- foldM (masked ctx) (rewrote, state') entry._symbolized- (bound'', forked) <- foldM (paired ctx (listToMaybe operands)) (bound', stood) entry._paired- (answer, state'') <- answered ctx entry operands bound'' forked+ stood <- foldM (masked ctx) rewrote entry._symbolized+ forked <- foldM (paired ctx (listToMaybe operands)) stood entry._paired+ (answer, state'') <- answered ctx entry operands forked state' remember caller._memo firing answer pure (answer, state'') shown :: Int -> Answer -> IO ()@@ -144,19 +145,19 @@ shaped <- rewritten rules (RuleContext ctx._buildTerm Nothing ctx._engine._normal) term ctx._saveEval (EvSymbolize ctx._nesting meta._spelling (ExMeta source._name) shaped) bind meta (MvExpression shaped) bound- masked :: ReduceContext -> (Subst, State) -> (Meta, Expression) -> IO (Subst, State)- masked ctx (bound, state') (meta, term) = do+ masked :: ReduceContext -> Subst -> (Meta, Expression) -> IO Subst+ masked ctx bound (meta, term) = do reduced <- buildExpressionThrows term bound- let (stood, known, spent) = symbolized reduced state'._minted+ (stood, known, spent) <- symbolized reduced <$> readIORef ctx._minted+ writeIORef ctx._minted spent mapM_ (ctx._saveEval . fact) known ctx._saveEval (EvSymbolize ctx._nesting meta._spelling term stood)- bound' <- bind meta (MvExpression stood) bound- pure (bound', state'{_minted = spent})+ bind meta (MvExpression stood) bound where fact :: (Int, Bytes) -> Evaluation fact (fresh, bytes) = EvKnown ctx._nesting fresh bytes- paired :: ReduceContext -> Maybe (Either Int Bytes) -> (Subst, State) -> (Meta, (Meta, Meta)) -> IO (Subst, State)- paired ctx condition (bound, state') (meta, (left, right)) = do+ paired :: ReduceContext -> Maybe (Either Int Bytes) -> Subst -> (Meta, (Meta, Meta)) -> IO Subst+ paired ctx condition bound (meta, (left, right)) = do one <- branch left two <- branch right case (one, two) of@@ -165,32 +166,34 @@ (_, ExTermination) -> terminating "right" right one _ -> both one two where- both :: Expression -> Expression -> IO (Subst, State)- both one two = case joined one two state'._minted of- Nothing -> throwIO (Stuck func)- Just (term, made, spent) -> do- mapM_ (ctx._saveEval . fact) made- ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)- bound' <- bind meta (MvExpression term) bound- pure (bound', state'{_minted = spent})- terminating :: T.Text -> Meta -> Expression -> IO (Subst, State)+ both :: Expression -> Expression -> IO Subst+ both one two = do+ outcome <- joined one two <$> readIORef ctx._minted+ case outcome of+ Nothing -> throwIO (Stuck func)+ Just (term, made, spent) -> do+ writeIORef ctx._minted spent+ mapM_ (ctx._saveEval . fact) made+ ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)+ 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) ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)- bound' <- bind meta (MvExpression term) bound- pure (bound', state')+ bind meta (MvExpression term) bound branch :: Meta -> IO Expression branch named = buildExpressionThrows (ExMeta named._name) bound fact :: (Int, (Int, Int)) -> Evaluation fact (fresh, pair) = EvJoined ctx._nesting fresh pair answered :: ReduceContext -> Lambda -> [Either Int Bytes] -> Subst -> State -> IO (Answer, State) answered ctx entry operands bound state' = do- let (fresh, spent) = minted entry._answer state'._minted+ (fresh, spent) <- minted entry._answer <$> readIORef ctx._minted+ writeIORef ctx._minted spent mapM_ (\idx -> ctx._saveEval (EvMinted ctx._nesting idx operands)) [idx | (_, FnSymbol idx) <- fresh] symbolic <- foldM mint bound fresh built <- buildExpressionThrows entry._answer symbolic ctx._saveEval (EvBuilt ctx._nesting built)- (normal, state'') <- settled built univ state'{_minted = spent} ctx+ (normal, state'') <- settled built univ state' ctx ctx._saveEval (EvAnswer ctx._nesting normal) pure ((built, normal), state'') mint :: Subst -> (Slot, Function) -> IO Subst
src/Filter.hs view
@@ -11,29 +11,25 @@ import Misc import Rewriter -exclude' :: Expression -> [Expression] -> Expression-exclude' expr [] = expr-exclude' expr@(ExFormation _) (fqn : remaining) = case fqnToAttrs fqn of- Just fqn' -> exclude' (excludedFormation expr fqn') remaining- _ -> expr+exclude' :: Expression -> [Expression] -> IO Expression+exclude' expr [] = pure expr+exclude' expr (fqn : remaining) = case fqnToAttrs fqn of+ Just attrs@(_ : _) -> maybe (throwIO (CanNotFindObjectByLocator fqn)) (`exclude'` remaining) (excludedFormation expr attrs)+ _ -> throwIO (InvalidLocatorProvided fqn) where- excludedFormation :: Expression -> [Attribute] -> Expression- excludedFormation (ExFormation bindings) [at] = ExFormation [bd | bd <- bindings, attributeFromBinding bd /= Just at]- excludedFormation (ExFormation bindings) atts = ExFormation (excludedBindings bindings atts)- where- excludedBindings :: [Binding] -> [Attribute] -> [Binding]- excludedBindings [] _ = []- excludedBindings (bd@(BiTau at' form@(ExFormation _)) : bs) as@(at'' : rs)- | at' == at'' = BiTau at' (excludedFormation form rs) : bs- | otherwise = bd : excludedBindings bs as- excludedBindings (bd : bs) as = bd : excludedBindings bs as- excludedFormation e _ = e-exclude' expr _ = expr+ excludedFormation :: Expression -> [Attribute] -> Maybe Expression+ excludedFormation (ExFormation bindings) [at]+ | any ((== Just at) . attributeFromBinding) bindings = Just (ExFormation [bd | bd <- bindings, attributeFromBinding bd /= Just at])+ excludedFormation (ExFormation bindings) (at : rest) = case break (nested at) bindings of+ (before, BiTau at' form : after) -> (\form' -> ExFormation (before ++ BiTau at' form' : after)) <$> excludedFormation form rest+ _ -> Nothing+ excludedFormation _ _ = Nothing+ nested :: Attribute -> Binding -> Bool+ nested at (BiTau at' (ExFormation _)) = at == at'+ nested _ _ = False -exclude :: [Rewritten] -> [Expression] -> [Rewritten]-exclude [] _ = []-exclude rs [] = rs-exclude ((expr, maybeRule) : rest) exprs = (exclude' expr exprs, maybeRule) : exclude rest exprs+exclude :: [Rewritten] -> [Expression] -> IO [Rewritten]+exclude rs exprs = traverse (\(expr, maybeRule) -> (,maybeRule) <$> exclude' expr exprs) rs include' :: Expression -> [Expression] -> IO Expression include' expr [] = pure expr
src/Functions.hs view
@@ -213,6 +213,7 @@ _number _ _ = throwIO (userError "Function number() requires exactly 1 argument as 'Φ.string'") _sum :: BuildTermMethod+_sum [] _ = throwIO (userError "Function sum() requires at least 1 argument") _sum args subst = do nums <- traverse (`argToNumber` subst) args pure (TeExpression (DataNumber (numToBts (sum nums))))
src/LaTeX.hs view
@@ -155,7 +155,7 @@ ( \idx comment (item, rule) reached -> let item' = toLatex (baseTab idx) item opening = if idx == 0 then item' else printf " %s %s" (relation reached) item'- in comment ++ maybe opening (\(judgment, name) -> printf "%s %s[\\nameref{r:%s}]" opening (relation judgment) name) rule+ in comment ++ maybe opening (\(judgment, name) -> printf "%s %s[\\nameref{r:%s}]" opening (relation judgment) (escaped name)) rule ) [0 ..] comments@@ -468,12 +468,15 @@ inference :: String -> String -> Maybe String -> Maybe Y.Condition -> [String] -> String -> String inference env name label cond premises conclusion = intercalate "\n" $- ["\\begin{" ++ env ++ "}", " \\phinoName{" ++ name ++ "}"]+ ["\\begin{" ++ env ++ "}", " \\phinoName{" ++ escaped name ++ "}"] ++ maybe [] (\symbol -> [" \\phinoLabel{" ++ symbol ++ "}"]) label ++ maybe [] (\rendered -> [" \\phinoCondition{ " ++ rendered ++ " }"]) (conditionInLatex cond) ++ map (\premise -> " \\phinoPremise{ " ++ premise ++ " }") premises ++ [" \\phinoConclusion{ " ++ conclusion ++ " }", "\\end{" ++ env ++ "}"] +escaped :: String -> String+escaped = T.unpack . toLaTeX . T.pack+ renderExpr :: Expression -> String renderExpr expr = renderToLatex (expressionToCST expr) defaultLatexContext @@ -484,7 +487,7 @@ trrule macro label name lhs rhs cond extras = intercalate "\n "- [ macro ++ labelArg ++ "{" ++ name ++ "}"+ [ macro ++ labelArg ++ "{" ++ escaped name ++ "}" , braced lhs , braced rhs , conditionToLatex cond
src/Morph.hs view
@@ -19,7 +19,7 @@ import Control.Exception (Exception, SomeException, catch, evaluate, throwIO, try) import Control.Monad (unless, when) import Data.Bifunctor (first)-import Data.IORef (IORef, modifyIORef', newIORef, readIORef, writeIORef)+import Data.IORef (IORef, atomicModifyIORef', modifyIORef', newIORef, readIORef, writeIORef) import Data.List (find, partition) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE@@ -54,7 +54,7 @@ type FiringFunc = Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Maybe Expression, State) emptyState :: State-emptyState = State 0 Nothing Nothing+emptyState = State Nothing Nothing data Steps = Steps { _limit :: Int@@ -95,6 +95,7 @@ , _maxCycles :: Int , _steps :: Steps , _tally :: Maybe Tally+ , _minted :: IORef Int , _deadline :: Maybe Deadline , _memo :: Maybe Memo , _nesting :: Int@@ -440,12 +441,10 @@ form <- held path store if copied form then do+ fresh <- coined caller looped caller mode before (Just (fresh, called form))- throwIO (Severed (ExFormation [BiLambda (FnSymbol fresh)]) reached{_minted = fresh})+ throwIO (Severed (ExFormation [BiLambda (FnSymbol fresh)]) reached) else refused caller refusal- where- fresh :: Int- fresh = reached._minted + 1 cut _ _ caller refusal = refused caller refusal copied :: Expression -> Bool copied (ExFormation bds) = boxed bds && not (any abstract bds) && any code bds@@ -488,11 +487,11 @@ } deferred :: Expression -> State -> ReduceContext -> IO (Expression, State) deferred copy state' caller = do+ fresh <- coined caller caller._saveEval (EvDeferred caller._nesting fresh caller._judgment copy (called copy) caller._site)- pure (ExFormation [BiLambda (FnSymbol fresh)], state'{_minted = fresh})- where- fresh :: Int- fresh = state'._minted + 1+ pure (ExFormation [BiLambda (FnSymbol fresh)], state')+ coined :: ReduceContext -> IO Int+ coined caller = atomicModifyIORef' caller._minted (\count -> (count + 1, count + 1)) called :: Expression -> Maybe Expression called copy@(ExFormation bds) = do (path, declared) <- origin copy@@ -552,45 +551,44 @@ spread :: Maybe Expression -> Frame -> Expression -> State -> ReduceContext -> IO (Expression, State) spread standing (Frame world _ _ _) form@(ExFormation bds) state' caller | not (any abstract bds) = do- jobs <- mapM (planned (synonym caller._universe form)) (zip [1 ..] bds)- (entered, _, state'') <- pooled caller._jobs jobs gathered ([], 0, state')+ floor' <- readIORef caller._minted+ jobs <- mapM (planned floor' (synonym caller._universe form)) (zip [1 ..] bds)+ (entered, state'') <- pooled caller._jobs jobs (gathered floor') ([], state') pure (ExFormation (reverse entered), state'') where- floor' :: Int- floor' = state'._minted- planned :: Maybe (Expression, [Attribute]) -> (Int, Binding) -> IO (IO ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State))))- planned alias (idx, BiTau attr body)+ planned :: Int -> Maybe (Expression, [Attribute]) -> (Int, Binding) -> IO (IO ([Evaluation], Int, Either SomeException (Int -> IO (Binding, Maybe State))))+ planned floor' alias (idx, BiTau attr body) | attr /= AtRho = do new <- if closed body then fresh alias attr caller else pure True- pure (if new then worker idx attr body else kept (BiTau attr body))- planned _ (_, bd) = pure (kept bd)- kept :: Binding -> IO ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State)))- kept bd = pure ([], Right (const (pure (bd, Nothing))))- worker :: Int -> Attribute -> Expression -> IO ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State)))- worker idx attr body = do+ pure (if new then worker floor' idx attr body else kept (BiTau attr body))+ planned _ _ (_, bd) = pure (kept bd)+ kept :: Binding -> IO ([Evaluation], Int, Either SomeException (Int -> IO (Binding, Maybe State)))+ kept bd = pure ([], 0, Right (const (pure (bd, Nothing))))+ worker :: Int -> Int -> Attribute -> Expression -> IO ([Evaluation], Int, Either SomeException (Int -> IO (Binding, Maybe State)))+ worker floor' idx attr body = do buffer <- newIORef [] tau <- tausOf idx tally <- tallied (fmap (\(Tally cap _) -> cap) caller._tally)+ minted <- newIORef floor' memo <- memoized caller._acyclic copy <- newIORef =<< readIORef world (store, path) <- home standing copy form- let own = caller{_jobs = 1, _tally = tally, _memo = memo, _saveEval = modifyIORef' buffer . (:), _buildTerm = minting tau caller._buildTerm}+ let own = caller{_jobs = 1, _tally = tally, _minted = minted, _memo = memo, _saveEval = modifyIORef' buffer . (:), _buildTerm = minting tau caller._buildTerm} outcome <- try (try (go (fmap (`ExDispatch` attr) standing) Nothing (Frame copy store path (Just attr)) body state' own)) records <- reverse <$> readIORef buffer- pure (records, fmap (either severed (\(term, walked) offset -> pure (BiTau attr (lifted floor' offset term), Just (moved offset walked)))) outcome)- severed :: Severed -> Int -> IO (Binding, Maybe State)- severed (Severed answer reached) offset = throwIO (Severed (lifted floor' offset answer) (moved offset reached))- moved :: Int -> State -> State- moved offset walked =- walked- { _minted = walked._minted + offset- , _manufactured = fmap (\sym -> if sym > floor' then sym + offset else sym) walked._manufactured- }- gathered :: ([Binding], Int, State) -> ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State))) -> IO ([Binding], Int, State)- gathered (done, offset, current) (records, outcome) = do+ spent <- subtract floor' <$> readIORef minted+ pure (records, spent, fmap (either (severed floor') (\(term, walked) offset -> pure (BiTau attr (lifted floor' offset term), Just (moved floor' offset walked)))) outcome)+ severed :: Int -> Severed -> Int -> IO (Binding, Maybe State)+ severed floor' (Severed answer reached) offset = throwIO (Severed (lifted floor' offset answer) (moved floor' offset reached))+ moved :: Int -> Int -> State -> State+ moved floor' offset walked = walked{_manufactured = fmap (\sym -> if sym > floor' then sym + offset else sym) walked._manufactured}+ gathered :: Int -> ([Binding], State) -> ([Evaluation], Int, Either SomeException (Int -> IO (Binding, Maybe State))) -> IO ([Binding], State)+ gathered floor' (done, current) (records, spent, outcome) = do+ offset <- subtract floor' <$> readIORef caller._minted mapM_ (caller._saveEval . renumbered floor' offset) records+ modifyIORef' caller._minted (+ spent) (bd, walked) <- either throwIO ($ offset) outcome- pure (bd : done, maybe offset (\after -> after._minted - floor') walked, fromMaybe current walked)+ pure (bd : done, fromMaybe current walked) spread standing frame term state' caller = parts standing frame term state' caller minting :: IO T.Text -> BuildTermFunc -> BuildTermFunc minting tau build func
src/Parser.hs view
@@ -25,7 +25,7 @@ import Control.Exception (Exception) import Control.Monad (guard, when) import Data.Char (isAsciiLower, isAsciiUpper, isDigit)-import Data.Scientific (toRealFloat)+import Data.Scientific (scientific, toRealFloat) import qualified Data.Set as Set import qualified Data.Text as T import Data.Void@@ -74,7 +74,7 @@ label' :: Parser T.Text label' = lexeme $ do first <- oneOf ['a' .. 'z']- rest <- many (satisfy (`notElem` " \r\n\t,.|':;!?][}{)(⟧⟦") <?> "allowed character")+ rest <- many (choice [try (char '-' <* notFollowedBy (char '>')), satisfy (`notElem` " \r\n\t,.|':;!?][}{)(⟧⟦-↦⤍>\"ξΦ⊥")] <?> "allowed character") return (T.pack (first : rest)) function :: Parser String@@ -186,16 +186,29 @@ number :: Parser Expression number = do sign <- optional (choice [char '-', char '+'])- unsigned <- lexeme L.scientific+ unsigned <- lexeme magnitude return ( DataNumber ( numToBts ( case sign of- Just '-' -> negate (toRealFloat unsigned)- _ -> toRealFloat unsigned+ Just '-' -> negate unsigned+ _ -> unsigned ) ) )+ where+ magnitude :: Parser Double+ magnitude = do+ whole <- some digitChar+ fraction <- option "" (try (char '.' >> some digitChar))+ power <- option 0 (try (oneOf ['e', 'E'] >> L.signed (pure ()) L.decimal))+ pure (scaled (read (whole ++ fraction)) (power - toInteger (length fraction)) (toInteger (length (whole ++ fraction))))+ scaled :: Integer -> Integer -> Integer -> Double+ scaled coefficient power digits+ | coefficient == 0 = 0+ | power > 400 = 1 / 0+ | power < negate (400 + digits) = 0+ | otherwise = toRealFloat (scientific coefficient (fromInteger power)) root :: Parser Expression root = do
src/Rewriter.hs view
@@ -200,7 +200,7 @@ _applied rule (RuleContext _buildTerm _universe _normal) expression >>= \case Nothing -> do logDebug (printf "Rule '%s' does not match, rewriting is stopped" ruleName)- if _breakpoint == Just ruleName+ if _breakpoint == Just ruleName && ruleName `notElem` [fired | (_, Just (_, fired)) <- NE.toList _rewrittens] then do logDebug (printf "Rule '%s' is a breakpoint, dropping down all the previous rewritings..." ruleName) pure (_rewrittens, expression, _unique, True, _found)
src/Sugar.hs view
@@ -62,8 +62,19 @@ | otherwise = Just (AA_TAU (APP_BINDING (goPair pair))) goArgument (AA_TAUS binding) = case goArgBinding binding of BI_EMPTY{} -> Nothing- binding' -> Just (AA_TAUS binding')+ binding'+ | sugar == SWEET, Just args <- positional binding' -> Just (AA_EXPRS args)+ | otherwise -> Just (AA_TAUS binding') goArgument (AA_EXPRS args) = Just (AA_EXPRS (goAppArg args))+ positional :: BINDING -> Maybe APP_ARG+ positional (BI_PAIR (PA_ALPHA (AL_IDX _ 0) _ first) rest _) = APP_ARG first <$> following 1 rest+ where+ following :: Int -> BINDINGS -> Maybe APP_ARGS+ following _ BDS_EMPTY{} = Just AAS_EMPTY+ following next (BDS_PAIR eol' tab' (PA_ALPHA (AL_IDX _ index) _ arg) more)+ | index == next = AAS_EXPR eol' tab' arg <$> following (next + 1) more+ following _ _ = Nothing+ positional _ = Nothing goArgBinding :: BINDING -> BINDING goArgBinding empty@BI_EMPTY{} = empty goArgBinding BI_META{..} = BI_META meta (goArgBindings bindings) tab
src/XMIR.hs view
@@ -618,7 +618,9 @@ | not (hasAttr "base" arg) && hasText arg = do key <- asToKey arg idx bytes <- getText arg- pure (ExApplication expr (mkArg key (ExFormation [BiDelta (bytesToBts bytes)])))+ bds <- mapM (\node -> xmirToFormationBinding derived node fqn) (arg C.$/ C.element (toName "o"))+ let delta = BiDelta (bytesToBts (T.unpack (T.strip (T.pack bytes))))+ pure (ExApplication expr (mkArg key (ExFormation (delta : bds)))) | otherwise = do key <- asToKey arg idx arg' <- xmirToExpression derived arg fqn@@ -662,7 +664,7 @@ at : _ -> let attr = T.unpack at in if null attr- then throwIO (InvalidXMIRFormat (printf "The attribute '%s' is not expected to be empty" attr) cur)+ then throwIO (InvalidXMIRFormat (printf "The attribute '%s' is not expected to be empty" key) cur) else pure attr hasText :: C.Cursor -> Bool
src/Yaml.hs view
@@ -21,6 +21,7 @@ import Data.Maybe (fromMaybe) import Data.Scientific (isInteger) import Data.Text (Text, unpack)+import qualified Data.Text as T import Data.Yaml (Parser) import qualified Data.Yaml as Yaml import GHC.Generics (Generic)@@ -197,6 +198,7 @@ referenceless rule.name "where" rule.where_ referenceless rule.name "having" rule.having targets rule (metas rule.pattern) (fromMaybe [] rule.where_)+ steps rule (named (metas rule.pattern)) (fromMaybe [] rule.where_) pure rule where targets :: Rule -> [Text] -> [Extra] -> Parser ()@@ -211,6 +213,27 @@ fresh rule known bound | bound `elem` known = fail (printf "The rule '%s' has a 'where' step that binds the meta '%s' again, while it is already bound" rule.name (unpack bound)) | otherwise = pure ()+ named :: [Text] -> [Text]+ named = filter ((> 1) . T.length)+ steps :: Rule -> [Text] -> [Extra] -> Parser ()+ steps rule known [] = do+ unread rule known "result" (metas rule.result)+ unread rule known "when" (metas rule.when)+ unread rule known "having" (metas rule.having)+ steps rule known (extra : rest) = do+ unread rule known "where" (metas extra.args)+ steps rule (known ++ named (metas extra.meta)) rest+ unread :: Rule -> [Text] -> String -> [Text] -> Parser ()+ unread rule known field used = case filter (`notElem` known) (named used) of+ [] -> pure ()+ missing : _ ->+ fail+ ( printf+ "The rule '%s' reads the meta '%s' it never binds, in '%s', since neither its pattern nor an earlier 'where' step binds it"+ rule.name+ (unpack missing)+ field+ ) data Number = MetaIndex Text
test/AbridgeSpec.hs view
@@ -21,25 +21,25 @@ describe "abridged" $ do it "leaves a formation no longer than the width as it is" $ printExpressionWith- (const (abridged 64))+ (const (abridged True 64)) (ExFormation [BiTau (AtLabel "kübel") (ExDispatch ExXi (AtLabel "wand")), BiVoid (AtLabel "zaun")]) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "⟦ kübel ↦ wand, zaun ↦ ∅ ⟧" it "keeps a formation exactly as wide as the width" $ printExpressionWith- (const (abridged 68))+ (const (abridged True 68)) (ExFormation (map (\idx -> BiTau (AtLabel (T.pack ("ort-" <> show idx))) ExRoot) [1 .. 6 :: Int])) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "⟦ ort-1 ↦ Φ, ort-2 ↦ Φ, ort-3 ↦ Φ, ort-4 ↦ Φ, ort-5 ↦ Φ, ort-6 ↦ Φ ⟧" it "folds a formation one character wider than the width" $ printExpressionWith- (const (abridged 67))+ (const (abridged True 67)) (ExFormation (map (\idx -> BiTau (AtLabel (T.pack ("ort-" <> show idx))) ExRoot) [1 .. 6 :: Int])) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "⟦ +6 ⟧" it "keeps the data and the λ of a long formation and folds the rest into a count" $ printExpressionWith- (const (abridged 64))+ (const (abridged True 64)) ( ExFormation ( BiDelta (BtMany ["00", "77", "66"]) : BiLambda (Function "L_xxx")@@ -50,7 +50,7 @@ `shouldBe` "⟦ Δ ⤍ 00-77-66, λ ⤍ L_xxx, +34 ⟧" it "keeps the φ of a long formation and folds the formation it holds" $ printExpressionWith- (const (abridged 64))+ (const (abridged True 64)) ( ExFormation [ BiTau (AtLabel "hund") ExRoot , BiTau AtPhi (ExFormation (map (\idx -> BiTau (AtLabel (T.pack ("pfote-" <> show idx))) ExRoot) [1 .. 9 :: Int]))@@ -61,25 +61,37 @@ `shouldBe` "⟦ φ ↦ ⟦ +9 ⟧, +2 ⟧" it "cuts a long byte string to its first bytes, its last bytes and the count of the bytes between them" $ printExpressionWith- (const (abridged 64))+ (const (abridged True 64)) (ExFormation [BiDelta (BtMany (map (printf "%02X") [7 .. 51 :: Int]))]) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "07-08-..(41b)..-32-33:Δ" it "cuts a long byte string inside a formation too short to fold" $ printExpressionWith- (const (abridged 64))+ (const (abridged True 64)) (ExFormation [BiTau (AtLabel "k") (ExFormation [BiDelta (BtMany ["01", "02", "03", "04", "05", "06", "07", "08", "09", "0A"])])]) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "01-02-..(6b)..-09-0A:Δ:k"+ it "keeps a long byte string whole unless told to cut the data" $+ printExpressionWith+ (const (abridged False 64))+ (ExFormation [BiDelta (BtMany (map (printf "%02X") [3 .. 19 :: Int]))])+ (SWEET, UNICODE, SINGLELINE, defaultMargin)+ `shouldBe` "03-04-05-06-07-08-09-0A-0B-0C-0D-0E-0F-10-11-12-13:Δ"+ it "folds a long formation and keeps its long byte string whole unless told to cut the data" $+ printExpressionWith+ (const (abridged False 64))+ (ExFormation (BiDelta (BtMany ["30", "31", "32", "33", "34", "35", "36", "37", "38", "39", "41", "42"]) : map (\idx -> BiVoid (AtLabel (T.pack ("fenster-" <> show idx)))) [1 .. 7 :: Int]))+ (SWEET, UNICODE, SINGLELINE, defaultMargin)+ `shouldBe` "⟦ Δ ⤍ 30-31-32-33-34-35-36-37-38-39-41-42, +7 ⟧" it "keeps a byte string of eight bytes whole" $ printExpressionWith- (const (abridged 64))+ (const (abridged True 64)) (ExFormation (BiDelta (BtMany ["40", "60", "E0", "00", "00", "00", "00", "01"]) : map (\idx -> BiVoid (AtLabel (T.pack ("ränder-" <> show idx)))) [1 .. 5 :: Int])) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "⟦ Δ ⤍ 40-60-E0-00-00-00-00-01, +5 ⟧" it "spells a folded formation the same way in ASCII" $ printExpressionWith- (const (abridged 64))+ (const (abridged True 64)) (ExFormation (BiLambda (Function "F") : map (\idx -> BiVoid (AtLabel (T.pack ("sehr-langes-" <> show idx)))) [1 .. 5 :: Int])) (SWEET, ASCII, SINGLELINE, defaultMargin) `shouldBe` "[[ L> F, +5 ]]"
test/CLIHelpersSpec.hs view
@@ -22,7 +22,7 @@ {-# ANN testPrintContext ("HLint: ignore Eta reduce" :: String) #-} testPrintContext :: IOFormat -> PrintContext testPrintContext format =- PrintCtx SWEET False Nothing MULTILINE 2 defaultXmirContext False False False False False 1 1 ExRoot Nothing Nothing Nothing format+ PrintCtx SWEET False Nothing False MULTILINE 2 defaultXmirContext False False False False False 1 1 ExRoot Nothing Nothing Nothing format spec :: Spec spec = do
test/CLISpec.hs view
@@ -238,6 +238,12 @@ , ["rewrite", "--sweet", "--hide-rho", "--margin=3"] , ["⟦\n b(c) ↦ ⟦⟧\n⟧:x:a"] )+ ,+ ( "prints positional arguments as such once the rho is gone"+ , "⟦ a ↦ ξ.b(ρ ↦ ξ, α0 ↦ ξ.c, α1 ↦ ξ.d) ⟧"+ , ["rewrite", "--flat", "--sweet", "--hide-rho"]+ , ["b( c, d ):a"]+ ) ] (\(desc, input, args, expected) -> it desc (withStdin input (testCLISucceeded args expected))) @@ -1168,6 +1174,12 @@ withStdin "[[ x -> $ ]]" $ testCLISucceeded ["rewrite", "--rule=" ++ fix, "--max-depth=1", "--depth-sensitive", "--flat"] ["⟦ x ↦ Φ ⟧"] + it "keeps the rewritten expression when the --breakpoint rule fired" $+ withStdin "⟦ a ↦ ⟦ b ↦ Φ ⟧.b ⟧" $+ testCLISucceeded+ ["rewrite", "--flat", "--normalize", "--breakpoint=dot"]+ ["⟦ a ↦ Φ( ρ ↦ ⟦ b ↦ Φ ⟧ ) ⟧"]+ describe "morph --focus under --locator" $ do it "finds the same object for the steps and for the answer" $ withStdin "⟦ t ↦ ⟦ a ↦ ⟦ Δ ⤍ 01- ⟧ ⟧, a ↦ ⟦ Δ ⤍ 02- ⟧ ⟧" $ do@@ -1181,6 +1193,10 @@ (out, _) <- withStdout (try (runCLI ["morph", "--locator=Q.t", "--focus=Q.nope", "--flat", "--sequence"]) :: IO (Either ExitCode ())) out `shouldNotContain` "⟦ t ↦" + it "fails on a --hide locator that matches nothing, as --show does" $+ withStdin "[[ x -> Q.y ]]" $+ testCLIFailed ["rewrite", "--hide=Q.nope"] ["Can't find object by locator: 'Φ.nope'"]+ describe "dataize" $ do it "prints help" $ testCLISucceeded ["dataize", "--help"] ["Dataize the 𝜑-expression"]@@ -1379,15 +1395,29 @@ , ("XMLXXXXXX.xml", " <bind meta=\"𝛿1.1\">01-02-..(8b)..-0B-0C</bind>") ] ( \(template, line) ->- it ("cuts a long datum a firing came down to, as " ++ line) $+ it ("cuts a long datum a firing came down to under --abridged-data, as " ++ line) $ withTempFile template $ \(path, stream) -> do hClose stream withLambdasOf (T.pack "- λ: L_outer\n dataize:\n 𝛿1: ξ.arg\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n") $ \outer -> withStdin "⟦ x ↦ ⟦ arg ↦ ⟦ Δ ⤍ 01-02-03-04-05-06-07-08-09-0A-0B-0C ⟧, λ ⤍ L_outer ⟧ ⟧" $- testCLISucceeded ["dataize", "--symbolic=" ++ outer, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] []+ testCLISucceeded ["dataize", "--symbolic=" ++ outer, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--abridged", "--abridged-data", "--sweet", "--hide-rho", "--quiet"] [] records <- readProtocol path lines records `shouldContain` [line] )+ forM_+ [ ("textXXXXXX.txt", " 𝛿1.1 := 30-31-32-33-34-35-36-37-38-39-41-42-43-44-45-46 # 𝔻(ξ.arg)")+ , ("XMLXXXXXX.xml", " <bind meta=\"𝛿1.1\">30-31-32-33-34-35-36-37-38-39-41-42-43-44-45-46</bind>")+ ]+ ( \(template, line) ->+ it ("keeps a long datum a firing came down to whole without --abridged-data, as " ++ line) $+ withTempFile template $ \(path, stream) -> do+ hClose stream+ withLambdasOf (T.pack "- λ: L_hex\n dataize:\n 𝛿1: ξ.arg\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n") $ \hex ->+ withStdin "⟦ x ↦ ⟦ arg ↦ ⟦ Δ ⤍ 30-31-32-33-34-35-36-37-38-39-41-42-43-44-45-46 ⟧, λ ⤍ L_hex ⟧ ⟧" $+ testCLISucceeded ["dataize", "--symbolic=" ++ hex, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] []+ records <- readProtocol path+ lines records `shouldContain` [line]+ ) it "folds a long formation under the width given as the value" $ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream@@ -1413,6 +1443,12 @@ it "refuses the flag without a protocol" $ withStdin wide $ testCLIFailed ["dataize", "--locator=Q.t", "--abridged"] ["The option --abridged requires --protocol"]+ it "refuses to cut the data in dataize without --abridged" $+ withStdin wide $+ testCLIFailed ["dataize", "--locator=Q.t", "--protocol=daten.txt", "--abridged-data"] ["The option --abridged-data requires --abridged"]+ it "refuses to cut the data in morph without --abridged" $+ withStdin wide $+ testCLIFailed ["morph", "--locator=Q.t", "--protocol=daten.xml", "--abridged-data"] ["The option --abridged-data requires --abridged"] describe "--protocol" $ do let sum' = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
test/CompiledSpec.hs view
@@ -87,11 +87,11 @@ matched :: Expression -> IO (Set.Set Int) matched expr = Set.fromList . map fst <$> filterM (\(_, rule) -> not . null <$> matchExpressionWithRule expr rule (RuleContext (building yaml) Nothing (_normal yaml))) (zip [0 ..] Y.normalizationRules) morphed :: Lambdas -> Engine -> Expression -> IO (Either String String)- morphed lambdas engine world = settled (show . fst <$> morph' (ExDispatch ExRoot (AtLabel "x"), (world, Nothing) :| []) world emptyState (reducing lambdas engine))+ morphed lambdas engine world = settled (show . fst <$> (morph' (ExDispatch ExRoot (AtLabel "x"), (world, Nothing) :| []) world emptyState =<< reducing lambdas engine)) dataized :: Lambdas -> Engine -> Expression -> IO (Either String String)- dataized lambdas engine world = settled (show . fst <$> dataize' (ExDispatch ExRoot (AtLabel "x"), (world, Nothing) :| []) world emptyState (reducing lambdas engine))- reducing :: Lambdas -> Engine -> ReduceContext- reducing lambdas engine = (defaultReduceContext ExRoot){_engine = engine, _buildTerm = building engine, _shuffle = False, _steps = Steps 40 0, _symbolic = lambdas}+ dataized lambdas engine world = settled (show . fst <$> (dataize' (ExDispatch ExRoot (AtLabel "x"), (world, Nothing) :| []) world emptyState =<< reducing lambdas engine))+ reducing :: Lambdas -> Engine -> IO ReduceContext+ reducing lambdas engine = (\ctx -> ctx{_engine = engine, _buildTerm = building engine, _shuffle = False, _steps = Steps 40 0, _symbolic = lambdas}) <$> defaultReduceContext ExRoot program :: Int -> Expression program seed = fst (formation False 4 (mkStdGen seed)) contextualized :: Engine -> Expression -> Expression -> IO (Either String String)
test/DataizeSpec.hs view
@@ -13,6 +13,7 @@ import Control.Exception (SomeException) import Control.Monad import Data.Aeson (FromJSON)+import Data.IORef (newIORef) import Data.List (find, isInfixOf, nub) import Data.List.NonEmpty (NonEmpty (..)) import Data.Map.Strict qualified as Map@@ -39,7 +40,7 @@ test func useCases = forM_ useCases $ \(desc, input, expr, output) -> it desc $ do- ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultReduceContext ExRoot)+ ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState =<< defaultReduceContext ExRoot res `shouldBe` output data DataizePack = DataizePack@@ -57,7 +58,8 @@ DataizePack{..} <- Decode.decodeFileThrow pth expr <- parseExpressionThrows (if model == Just True then primitives input else input) loc <- parseExpressionThrows (fromMaybe "Q" location)- let ctx = (defaultReduceContext loc){_symbolic = if symbolic == Just True then known else emptyLambdas}+ base <- defaultReduceContext loc+ let ctx = base{_symbolic = if symbolic == Just True then known else emptyLambdas} case (result, fails) of (Just res, Nothing) -> do bts <- either (fail . ("cannot read the expected bytes: " ++)) pure (parseBytes res)@@ -71,7 +73,8 @@ partially known src = do expr <- parseExpressionThrows (primitives src) recorded $ \record -> do- let ctx = (withLambdas known (defaultReduceContext ExRoot)){_partial = True, _saveEval = record}+ base <- defaultReduceContext ExRoot+ let ctx = (withLambdas known base){_partial = True, _saveEval = record} (outcome, chain, _) <- dataize expr emptyState ctx pure (outcome, chain) @@ -84,11 +87,12 @@ describe "dataize' fails when no dataization rule matches the term" $ it "throws instead of treating the unmatched meta as ⊥" $- dataize' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)+ (dataize' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState =<< defaultReduceContext ExRoot) `shouldThrow` (\e -> "no dataization rule matched" `isInfixOf` show (e :: SomeException)) describe "dataization 'norm' is disjoint from the specific clauses" $ do- let rctx = RuleContext (execBuildTerm ExRoot (defaultReduceContext ExRoot)) Nothing (_normal linked)+ ctx <- runIO (defaultReduceContext ExRoot)+ let rctx = RuleContext (execBuildTerm ExRoot ctx) Nothing (_normal linked) dataizeRule :: String -> Yaml.DataizeRule dataizeRule nm = fromMaybe (error ("no dataization rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.dataizationRules) asRule :: Yaml.DataizeRule -> Yaml.Rule@@ -156,7 +160,7 @@ describe "fails to dataize the terminator" $ do let failsOn desc input = it desc $- dataize' (input, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)+ (dataize' (input, (ExRoot, Nothing) :| []) ExRoot emptyState =<< defaultReduceContext ExRoot) `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException)) failsOn "throws on ⊥ instead of mapping it to empty bytes" ExTermination failsOn "throws on a data-less formation, which dataizes ⊥" (ExFormation [])@@ -168,13 +172,15 @@ it "fails on the step limit instead of morphing forever" $ looping $ \endless -> do expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_loop ⟧ ⟧"- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty endless (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)+ minted <- newIORef 0+ dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing minted Nothing Nothing 1 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 ⟧ ⟧"- (outcome, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing Nothing Nothing 1 False True True False 1 Nothing Dataization [] Map.empty endless (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)+ minted <- newIORef 0+ (outcome, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing minted Nothing Nothing 1 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)@@ -183,14 +189,15 @@ it "fails a partial dataization once the deadline has passed" $ do expr <- parseExpressionThrows "[[ @ -> [[ D> 7E- ]] ]]" deadline <- overdue 29- dataize expr emptyState (defaultReduceContext ExRoot){_deadline = Just deadline, _partial = True}+ ctx <- defaultReduceContext ExRoot+ dataize expr emptyState ctx{_deadline = Just deadline, _partial = True} `shouldThrow` (\e -> "--max-seconds=29" `isInfixOf` show (e :: SomeException)) describe "partially evaluates around a λ function that cannot fire (--partial)" $ do let placeholder = ExFormation [BiLambda (Function "Sym_arg_0")] it "fails on it without the flag, naming the λ function" $ do expr <- parseExpressionThrows (primitives "2.times(3).nope")- dataize expr emptyState (withLambdas known (defaultReduceContext ExRoot))+ (dataize expr emptyState . withLambdas known =<< defaultReduceContext ExRoot) `shouldThrow` (\e -> "No entry of --symbolic answers the λ function 'L_number_nope'" `isInfixOf` show (e :: SomeException)) it "leaves the application of the unanswered λ function in place" $ do ((outcome, _), _) <- partially known "2.times(3).nope"@@ -241,27 +248,30 @@ forM_ [ ( "--max-cycles"- , ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing Nothing Nothing 1 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 True True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked , "--max-cycles=0" ) , ( "--max-depth"- , ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing Nothing Nothing 1 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 True True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked , "--max-depth=0" ) ]- ( \(flag, ctx, message) ->+ ( \(flag, reducing, message) -> it ("throws once " ++ flag ++ " is exhausted with --depth-sensitive") $ do expr <- parseExpressionThrows "[[ @ -> [[ x -> [[ D> 00- ]] ]].x ]]"+ ctx <- reducing <$> newIORef 0 dataize expr emptyState ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException)) ) it "does not throw without --depth-sensitive even once --max-depth is exhausted" $ do expr <- parseExpressionThrows boxed- (value, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)+ minted <- newIORef 0+ (value, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing minted Nothing Nothing 1 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- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)+ minted <- newIORef 0+ dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing minted Nothing Nothing 1 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@@ -280,7 +290,7 @@ it "uses no step label without a defining rule or operation" $ do expr <- parseExpressionThrows (primitives "5.plus(6)") loc <- parseExpressionThrows "Q"- (_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext loc))+ (_, chain, _) <- dataize expr emptyState . withLambdas known =<< defaultReduceContext loc let orphans = nub [label | (_, Just (_, label)) <- chain, label `notElem` allowed, label /= "symbol"] unless (null orphans)@@ -288,15 +298,15 @@ it "takes the step of a firing by evaluation" $ do expr <- parseExpressionThrows (primitives "5.plus(6)") loc <- parseExpressionThrows "Q"- (_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext loc))+ (_, chain, _) <- dataize expr emptyState . withLambdas known =<< defaultReduceContext loc map snd chain `shouldContain` [Just (Evaluation, "evaluate")] it "takes the step of a box by contextualization" $ do expr <- parseExpressionThrows "[[ @ -> [[ D> 0A- ]] ]]"- (_, chain, _) <- dataize expr emptyState (defaultReduceContext ExRoot)+ (_, chain, _) <- dataize expr emptyState =<< defaultReduceContext ExRoot map snd chain `shouldContain` [Just (Contextualization, "contextualize")] it "takes the step of a delta by dataization" $ do expr <- parseExpressionThrows "[[ D> 3C- ]]"- (_, chain, _) <- dataize expr emptyState (defaultReduceContext ExRoot)+ (_, chain, _) <- dataize expr emptyState =<< defaultReduceContext ExRoot map snd chain `shouldBe` [Just (Dataization, "delta"), Nothing] describe "names every rule uniquely across rule sets" $@@ -313,7 +323,7 @@ let labelsOf loc src = do expr <- parseExpressionThrows src loc' <- parseExpressionThrows loc- (_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext loc'))+ (_, chain, _) <- dataize expr emptyState . withLambdas known =<< defaultReduceContext loc' pure [label | (_, Just (_, label)) <- chain] it "dataizes 5.plus(6) through the expected rules" $ do labels <-@@ -335,7 +345,7 @@ labels `shouldBe` ["contextualize", "md", "dot", "skip", "mf", "delta"] it "takes every step of 5.plus(6) by the judgment of its rule" $ do expr <- parseExpressionThrows "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"- (_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext ExRoot))+ (_, chain, _) <- dataize expr emptyState . withLambdas known =<< defaultReduceContext ExRoot [judgment | (_, Just (judgment, _)) <- chain] `shouldBe` [ Contextualization , Morphing
test/EvaluateSpec.hs view
@@ -26,7 +26,7 @@ import Lining (LineFormat (SINGLELINE)) import Margin (defaultMargin) import Matcher (substEmpty)-import Morph (ReduceContext (..), Steps (..), execBuildTerm, memoized, morph)+import Morph (ReduceContext (..), Steps (..), emptyState, execBuildTerm, memoized, morph) import Parser (parseExpressionThrows) import Printer (printExpression, printExpression', printExpressionHidingRho') import Sugar (SugarType (SWEET))@@ -65,8 +65,9 @@ (_, written) <- recorded' hidden $ \record -> do let mode = named <$> acyclic cells <- memoized mode+ base <- defaultReduceContext loc let ctx =- (defaultReduceContext loc)+ base { _deep = deep == Just True , _partial = partial == Just True , _acyclic = mode@@ -76,11 +77,12 @@ , _saveEval = record } record (EvRun Morphing (T.pack (printExpression loc)))+ started expr ctx case fails of Just message ->- morph expr (started expr) ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException))+ morph expr emptyState ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException)) Nothing -> do- (morphed, _, _) <- morph expr (started expr) ctx+ (morphed, _, _) <- morph expr emptyState ctx forM_ result $ \res -> do expected <- parseExpressionThrows res spelled hidden morphed `shouldBe` spelled False expected@@ -103,8 +105,9 @@ describe "execBuildTerm 'evaluate'" $ do let univ = ExFormation []- ctx = withLambdas known (defaultReduceContext ExRoot)- runEvaluate args = execBuildTerm univ ctx "evaluate" args substEmpty+ runEvaluate args = do+ ctx <- withLambdas known <$> defaultReduceContext ExRoot+ execBuildTerm univ ctx "evaluate" args substEmpty forM_ [ ( "the first argument is not a formation"@@ -124,7 +127,8 @@ it "gets stuck on a λ naming a symbol, instead of refusing the formation" $ do (_, written) <- recorded $ \record -> do- let stuck = (withLambdas known (defaultReduceContext ExRoot)){_saveEval = record}+ ctx <- withLambdas known <$> defaultReduceContext ExRoot+ let stuck = ctx{_saveEval = record} fire = execBuildTerm univ stuck "evaluate" [ArgExpression (ExFormation [BiLambda (FnSymbol 1)]), ArgExpression univ] substEmpty fire `shouldThrow` (\e -> "No entry of --symbolic answers the λ function '𝜎1'" `isInfixOf` show (e :: SomeException)) written `shouldBe` " unanswered(𝜎1) # 𝕄(𝜎1:λ)\n"@@ -147,7 +151,8 @@ it "evaluates a λ-bearing formation to the answer of its entry, normalized" $ do let form = ExFormation [BiLambda (Function "L_answer"), BiTau AtRho (ExFormation [BiDelta (BtOne "00")])] answered <- withLambdasOf "- λ: L_answer\n 𝑛: ⟦ Δ ⤍ FF- ⟧\n" readLambdas- result <- execBuildTerm univ (withLambdas answered ctx) "evaluate" [ArgExpression form, ArgExpression univ] substEmpty+ ctx <- withLambdas answered <$> defaultReduceContext ExRoot+ result <- execBuildTerm univ ctx "evaluate" [ArgExpression form, ArgExpression univ] substEmpty case result of TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "FF")] _ -> expectationFailure "expected TeExpression"
test/FilterSpec.hs view
@@ -44,30 +44,33 @@ included <- traverse parseExpressionThrows shown excluded <- traverse parseExpressionThrows hidden res <- parseExpressionThrows result- [(expr', _)] <- (`F.exclude` excluded) <$> F.include [(expr, Nothing)] included+ [(expr', _)] <- F.include [(expr, Nothing)] included >>= (`F.exclude` excluded) expr' `shouldBe` res ) describe "direct unit tests" $ do describe "exclude" $ do- it "leaves the expression untouched when the fqn is not a Q-dispatch chain" $ do- expr <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"- badFqn <- parseExpressionThrows "$.x"- let [(expr', _)] = F.exclude [(expr, Nothing)] [badFqn]- expr' `shouldBe` expr-- it "leaves a non-formation expression untouched" $ do- expr <- parseExpressionThrows "Q.x"- fqn <- parseExpressionThrows "Q.y"- let [(expr', _)] = F.exclude [(expr, Nothing)] [fqn]- expr' `shouldBe` expr+ forM_+ [ ("fails when the fqn is not a Q-dispatch chain", "[[ x -> ?, y -> ? ]]", "$.x")+ , ("fails when the fqn is the whole program", "[[ x -> ?, y -> ? ]]", "Q")+ , ("fails when nothing matches the fqn", "[[ x -> ? ]]", "Q.nope")+ , ("fails when a nested fqn stops short of its last attribute", "[[ x -> [[ y -> ? ]] ]]", "Q.x.nope")+ , ("fails for a non-formation expression", "Q.x", "Q.y")+ , ("fails when the fqn walks into something that is not a formation", "[[ org -> [[ eolang -> Q.x ]] ]]", "Q.org.eolang.number")+ ]+ ( \(desc, phi, locator) ->+ it desc $ do+ expr <- parseExpressionThrows phi+ fqn <- parseExpressionThrows locator+ F.exclude [(expr, Nothing)] [fqn] `shouldThrow` anyException+ ) it "recurses over a multi-element rewrite list, preserving each rule label" $ do first' <- parseExpressionThrows "[[ x -> ?, y -> ? ]]" second' <- parseExpressionThrows "[[ x -> ?, y -> ? ]]" fqn <- parseExpressionThrows "Q.x" expected <- parseExpressionThrows "[[ y -> ? ]]"- let excluded = F.exclude [(first', Just (Normalization, "rule-a")), (second', Just (Evaluation, "rule-b"))] [fqn]+ excluded <- F.exclude [(first', Just (Normalization, "rule-a")), (second', Just (Evaluation, "rule-b"))] [fqn] map fst excluded `shouldBe` [expected, expected] map snd excluded `shouldBe` [Just (Normalization, "rule-a"), Just (Evaluation, "rule-b")]
test/Fixtures.hs view
@@ -30,6 +30,7 @@ import Data.Aeson (FromJSON (parseJSON), withObject, (.:)) import Data.ByteString qualified as BS import Data.Char (toLower)+import Data.IORef (newIORef) import Data.List (isPrefixOf, stripPrefix) import Data.Map.Strict qualified as Map import Data.Maybe (fromMaybe)@@ -50,8 +51,10 @@ import System.IO (Handle, IOMode (ReadMode), hClose, hGetContents, hSetEncoding, openBinaryTempFile, utf8, withFile) import XMIR (defaultXmirContext) -defaultReduceContext :: Expression -> ReduceContext-defaultReduceContext loc = ReduceContext loc loc Nothing 25 25 (Steps 250 0) Nothing Nothing Nothing 1 False True False False 1 Nothing Morphing [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked+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 False True False False 1 Nothing Morphing [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked) linked :: Engine linked = fromMaybe yaml compiled@@ -117,6 +120,7 @@ SWEET hidden Nothing+ False MULTILINE 2 defaultXmirContext
test/FunctionsSpec.hs view
@@ -187,6 +187,18 @@ , [ArgExpression (DataNumber (numToBts 2)), ArgExpression (DataNumber (numToBts 3))] , \term -> expectExpression term (DataNumber (numToBts 5)) )+ ,+ ( "sum keeps a single numeric argument as is"+ , "sum"+ , [ArgExpression (DataNumber (numToBts 7))]+ , \term -> expectExpression term (DataNumber (numToBts 7))+ )+ ,+ ( "sum of operands that cancel out is still zero"+ , "sum"+ , [ArgExpression (DataNumber (numToBts 4)), ArgExpression (DataNumber (numToBts (-4)))]+ , \term -> expectExpression term (DataNumber (numToBts 0))+ ) ] failureCases :: [(String, String, [ExtraArgument], String)]@@ -226,6 +238,7 @@ , [ArgExpression (DataNumber (BtMany ["68", "65", "6C", "6C", "6F"]))] , "Expected 8 bytes for a number, got 5" )+ , ("sum fails on an empty argument list", "sum", [], "sum() requires at least 1 argument") , ( "an unsupported function name fails with a descriptive message" , "no-such-function"
test/LaTeXSpec.hs view
@@ -248,6 +248,17 @@ explainRules [Y.Rule "rt" Nothing Nothing ptn ptn Nothing (Just [Y.Extra (Y.ArgAttribute (AtMeta "t1")) "random-tau" []]) Nothing] `shouldContain` "\\randomTau{" + it "escapes the name of the rule it refers to" $ do+ step1 <- parseExpressionThrows "[[ x -> Q.y ]]"+ step2 <- parseExpressionThrows "[[ x -> Q.z ]]"+ latex <- rewrittensToLatex ([(step1, Nothing), (step2, Just (Normalization, "my_rule%1"))], False) defaultLatexContext+ latex `shouldContain` "\\nameref{r:my\\char95{}rule\\char37{}1}"++ it "escapes the name of the rule it explains" $ do+ ptn <- parseExpressionThrows "Q.x"+ explainRules [Y.Rule "my_rule%1" Nothing Nothing ptn ptn Nothing Nothing Nothing]+ `shouldContain` "\\phinoNormalizationRule{my\\char95{}rule\\char37{}1}"+ it "prefixes each step with a '% === Step' header when '_headers' is set" $ do step1 <- parseExpressionThrows "[[ x -> Q.y ]]" step2 <- parseExpressionThrows "[[ x -> Q.z ]]"
test/MorphSpec.hs view
@@ -44,7 +44,7 @@ test' func useCases = forM_ useCases $ \(desc, input, expr, output) -> it desc $ do- ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultReduceContext ExRoot)+ ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState =<< defaultReduceContext ExRoot res `shouldBe` output data MorphPack = MorphPack@@ -64,8 +64,9 @@ expr <- parseExpressionThrows (if model == Just True then primitives input else input) seedTaus expr loc <- parseExpressionThrows (fromMaybe "Q" location)+ base <- defaultReduceContext loc let ctx =- (defaultReduceContext loc)+ base { _deep = deep , _partial = partial == Just True , _symbolic = if symbolic == Just True then known else emptyLambdas@@ -90,7 +91,7 @@ it "reports the chain of steps oldest first" $ do expr <- parseExpressionThrows "[[ D> 00- ]]"- (morphed, chain, _) <- morph expr emptyState (defaultReduceContext ExRoot)+ (morphed, chain, _) <- morph expr emptyState =<< defaultReduceContext ExRoot morphed `shouldBe` expr map snd chain `shouldBe` [Just (Morphing, "mf"), Nothing] map fst chain `shouldBe` [expr, expr]@@ -99,7 +100,8 @@ expr <- parseExpressionThrows "[[ w -> [[ k -> [[ ]] ]].k, y -> Q.w ]]" loc <- parseExpressionThrows "Q.y" saved <- newIORef (0 :: Int)- _ <- morph expr emptyState (defaultReduceContext loc){_saveStep = const (modifyIORef' saved (+ 1))}+ ctx <- defaultReduceContext loc+ _ <- morph expr emptyState ctx{_saveStep = const (modifyIORef' saved (+ 1))} readIORef saved `shouldReturn` 2 describe "morph with '_deep'" $ do@@ -112,7 +114,8 @@ withLambdasOf "- λ: L_answer\n 𝑛: ⟦ Δ ⤍ FF- ⟧\n" $ \file -> do box <- readLambdas file world <- parseExpressionThrows "[[ foo -> [[ f -> [[ a -> ?, @ -> $.a, L> L_answer ]] ]], x -> Q.foo.f( a -> [[ D> 01- ]] ).@ ]]"- (morphed, _, _) <- morph world emptyState (withLambdas box (defaultReduceContext ExRoot)){_deep = True}+ ctx <- withLambdas box <$> defaultReduceContext ExRoot+ (morphed, _, _) <- morph world emptyState ctx{_deep = True} morphed `shouldBe` world describe "morph'" $@@ -157,27 +160,29 @@ describe "inferred" $ it "morphs a premise in the universe it names, not in the one the frame is in" $ do world <- parseExpressionThrows "[[ x -> [[ ]] ]]"+ ctx <- defaultReduceContext ExRoot Just (Answered _ answer, _) <- inferred ExRoot ExRoot emptyState- (defaultReduceContext ExRoot)+ ctx [direct (\_ _ -> [Morphs ExRoot world (pure . Concludes . Answered (Morphing, "premise"))])] answer `shouldBe` world describe "morph' fails when no morphing rule matches the term" $ it "throws instead of looping when handed a bare, unmatched meta" $- morph' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)+ (morph' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState =<< defaultReduceContext ExRoot) `shouldThrow` (\e -> "Morphing expects a normal form" `isInfixOf` show (e :: SomeException)) describe "execBuildTerm 'morph'" $ do let univ = ExFormation []- ctx = defaultReduceContext ExRoot- it "throws when not given exactly one expression argument" $+ it "throws when not given exactly one expression argument" $ do+ ctx <- defaultReduceContext ExRoot execBuildTerm univ ctx "morph" [] substEmpty `shouldThrow` (\e -> "requires exactly 1 expression argument" `isInfixOf` show (e :: SomeException)) it "morphs a single expression argument to its already-normal form" $ do+ ctx <- defaultReduceContext ExRoot result <- execBuildTerm univ ctx "morph" [ArgExpression (ExFormation [BiDelta (BtOne "00")])] substEmpty case result of TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "00")]@@ -188,7 +193,7 @@ reduced src = do univ <- parseExpressionThrows universe target <- parseExpressionThrows src- (extended, ctx) <- insideUniverse target univ (defaultReduceContext ExRoot)+ (extended, ctx) <- insideUniverse target univ =<< defaultReduceContext ExRoot (outcome, _, _) <- dataize extended emptyState ctx pure outcome it "reduces an expression the program does not contain" $ do@@ -199,7 +204,7 @@ value `shouldBe` Dataized (BtOne "01") it "refuses a universe which is not a formation" $ do target <- parseExpressionThrows "Q.y"- insideUniverse target ExRoot (defaultReduceContext ExRoot)+ (insideUniverse target ExRoot =<< defaultReduceContext ExRoot) `shouldThrow` (\e -> "not a formation" `isInfixOf` show (e :: SomeException)) describe "morphing is order-independent under --shuffle" $ do@@ -217,11 +222,12 @@ ] forM_ cases $ \(desc, input, univ, expected) -> it ("morphs " ++ desc ++ " to the same form across 100 random rule orders") $ do- results <- replicateM 100 (fst . fst <$> morph' (input, (univ, Nothing) :| []) univ emptyState (defaultReduceContext ExRoot))+ results <- replicateM 100 (fst . fst <$> (morph' (input, (univ, Nothing) :| []) univ emptyState =<< defaultReduceContext ExRoot)) nub results `shouldBe` [expected] describe "morphing 'md' is disjoint from 'ml'" $ do- let rctx = RuleContext (execBuildTerm ExRoot (defaultReduceContext ExRoot)) Nothing (_normal linked)+ ctx <- runIO (defaultReduceContext ExRoot)+ let rctx = RuleContext (execBuildTerm ExRoot ctx) Nothing (_normal linked) morphRule :: String -> Yaml.MorphRule morphRule nm = fromMaybe (error ("no morphing rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.morphingRules) asRule :: Yaml.MorphRule -> Yaml.Rule@@ -236,19 +242,21 @@ it "drills a chained λ-formation dispatch down to the base 'ml'" $ do let base = ExFormation [BiLambda (Function "F")] chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c")- morph' (chain, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)+ (morph' (chain, (ExRoot, Nothing) :| []) ExRoot emptyState =<< defaultReduceContext ExRoot) `shouldThrow` (\e -> "No entry of --symbolic answers the λ function 'F'" `isInfixOf` show (e :: SomeException)) describe "stops by the clock of --max-seconds" $ do it "fails a morphing that fires nothing once the deadline has passed" $ do expr <- parseExpressionThrows "[[ k -> [[ D> 3F- ]] ]]" deadline <- overdue 17- morph expr emptyState (defaultReduceContext ExRoot){_deadline = Just deadline}+ ctx <- defaultReduceContext ExRoot+ morph expr emptyState ctx{_deadline = Just deadline} `shouldThrow` (\e -> "--max-seconds=17" `isInfixOf` show (e :: SomeException)) it "fails a partial morphing once the deadline has passed" $ do expr <- parseExpressionThrows "[[ q -> [[ D> 5A- ]] ]]" deadline <- overdue 23- morph expr emptyState (defaultReduceContext ExRoot){_deadline = Just deadline, _partial = True}+ ctx <- defaultReduceContext ExRoot+ morph expr emptyState ctx{_deadline = Just deadline, _partial = True} `shouldThrow` (\e -> "--max-seconds=23" `isInfixOf` show (e :: SomeException)) describe "stops an entrance by the clock of --max-seconds" $@@ -256,6 +264,7 @@ due <- (+ 0.2) <$> getMonotonicTime let formation :: Expression -> Int -> Expression formation base depth = ExFormation [BiTau (AtLabel "x") (iterate (`ExDispatch` AtLabel "w") base !! depth), BiLambda (Function "L_q")]- ctx <- enter (formation ExRoot 1300) (defaultReduceContext ExRoot){_acyclic = Just Plausible, _deadline = Just (Deadline 31 due)}+ base <- defaultReduceContext ExRoot+ ctx <- enter (formation ExRoot 1300) base{_acyclic = Just Plausible, _deadline = Just (Deadline 31 due)} timeout 10000000 (enter (formation ExXi 1700) ctx) `shouldThrow` (\e -> "--max-seconds=31" `isInfixOf` show (e :: SomeException))
test/ParserSpec.hs view
@@ -413,6 +413,16 @@ fromLeft "" (parseExpression "⟦\n a ↦ ξ,\n b ↦ ξ,\n b ↦ Φ\n⟧\n\n\n") `shouldSatisfy` isInfixOf "expression:4:3:" + describe "an arrow ends an attribute name" $+ forM_+ [ ("⟦ a ↦ ξ.b(c↦ξ) ⟧", "⟦ a ↦ ξ.b(c ↦ ξ) ⟧")+ , ("[[ a -> $.b(c->$) ]]", "[[ a -> $.b(c -> $) ]]")+ , ("⟦ a ↦ ξ.as-bytes(x-y↦ξ) ⟧", "⟦ a ↦ ξ.as-bytes(x-y ↦ ξ) ⟧")+ ]+ ( \(tight, spaced) ->+ it tight (parseExpression tight `shouldBe` parseExpression spaced)+ )+ describe "parse number" $ test parseNumber@@ -433,6 +443,10 @@ , ("1.5e2", Just (DataNumber (BtMany ["40", "62", "C0", "00", "00", "00", "00", "00"]))) , ("2e-3", Just (DataNumber (BtMany ["3F", "60", "62", "4D", "D2", "F1", "A9", "FC"]))) , ("-1e10", Just (DataNumber (BtMany ["C2", "02", "A0", "5F", "20", "00", "00", "00"])))+ , ("1e18446744073709551617", Just (DataNumber (BtMany ["7F", "F0", "00", "00", "00", "00", "00", "00"])))+ , ("-1e18446744073709551617", Just (DataNumber (BtMany ["FF", "F0", "00", "00", "00", "00", "00", "00"])))+ , ("1e9223372036854775808", Just (DataNumber (BtMany ["7F", "F0", "00", "00", "00", "00", "00", "00"])))+ , ("5e-18446744073709551615", Just (DataNumber (BtMany ["00", "00", "00", "00", "00", "00", "00", "00"]))) , ("abc", Nothing) , ("", Nothing) ]
test/XMIRSpec.hs view
@@ -304,6 +304,7 @@ , ("keeps Δ data between sibling bindings", "[[ top -> [[ a -> [[]], D> 01-02, b -> [[]] ]] ]]") , ("keeps a bare 'Q' bound to a named attribute", "[[ x -> Q ]]") , ("keeps a formation bound to φ", "[[ k -> [[ @ -> [[ L> S8 ]] ]] ]]")+ , ("keeps byte data and sibling bindings in an application argument", "[[ x -> Q.y(a -> [[ D> 01-02, b -> Q.z ]]) ]]") ] ( \(desc, source) -> it desc $ do expr <- parseExpressionThrows source@@ -341,6 +342,11 @@ expr <- parseExpressionThrows "[[ x -> [[ a -> ? ]](a -> Q.y) ]]" try (void (expressionToXMIR expr defaultXmirContext)) :: IO (Either SomeException ()) , ["XMIR does not support such expression", "a ↦ Φ.y"]+ )+ ,+ ( "names the attribute that is empty"+ , try (void (parseXMIRThrows "<object><o name=\"a\" base=\"\"/></object>" >>= xmirToPhi)) :: IO (Either SomeException ())+ , ["The attribute 'base' is not expected to be empty"] ) , ( "explains an unsupported binding"
test/YamlSpec.hs view
@@ -9,7 +9,7 @@ import AST (Alpha, Attribute, Binding, Bytes, Expression (ExMeta, ExRoot)) import Control.Exception (Exception (displayException), SomeException) import Control.Monad-import Data.Either (isLeft)+import Data.Either (isLeft, isRight) import Data.List (isInfixOf, nub, sort, (\\)) import Data.Maybe (fromMaybe) import Data.Text qualified as T@@ -85,6 +85,20 @@ it "rejects a 'where' step whose meta is not a meta" $ (decodeYaml' "name: nometa\npattern: '⟦ x ↦ 𝑒1 ⟧'\nresult: '⟦ x ↦ 𝑒1 ⟧'\nwhere:\n - meta: 'z'\n function: concat\n args: ['\"a\"']" :: Either Yaml.ParseException Rule) `shouldSatisfy` failsWith "whose 'meta' is not a meta"++ describe "rejects a meta that nothing binds" $+ forM_+ [ ("in 'when'", "name: w\npattern: '⟦ x ↦ 𝑒1 ⟧'\nresult: '⟦ y ↦ 𝑒1 ⟧'\nwhen:\n not:\n eq: ['𝑒9', '𝑒1']", "'e9'")+ , ("in 'result'", "name: r\npattern: '⟦ x ↦ 𝑒1, 𝐵1 ⟧'\nresult: '⟦ y ↦ 𝑒9, 𝐵1 ⟧'", "'e9'")+ , ("in a 'where' argument", "name: a\npattern: '⟦ x ↦ 𝑒1 ⟧'\nresult: '⟦ x ↦ 𝑒2 ⟧'\nwhere:\n - meta: '𝑒2'\n function: concat\n args: ['𝑒7']", "'e7'")+ ]+ ( \(desc, yaml, meta) ->+ it desc ((decodeYaml' yaml :: Either Yaml.ParseException Rule) `shouldSatisfy` failsWith ("reads the meta " ++ meta))+ )++ it "accepts a meta that an earlier 'where' step binds" $+ (decodeYaml' "name: ok\npattern: '⟦ x ↦ 𝑒1 ⟧'\nresult: '⟦ x ↦ 𝑒3 ⟧'\nwhere:\n - meta: '𝑒2'\n function: concat\n args: ['𝑒1']\n - meta: '𝑒3'\n function: concat\n args: ['𝑒2']" :: Either Yaml.ParseException Rule)+ `shouldSatisfy` isRight it "rejects an 'e-match' in a rewriting rule" $ (decodeYaml' "name: kvz\npattern: '⟦ 𝜏1 ↦ 𝑒1 ⟧'\ne-match: '𝑒2'\nresult: '𝑒2'" :: Either Yaml.ParseException Rule)