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.100 +version: 0.0.101 license: MIT synopsis: Command-Line Manipulator of πœ‘-Calculus Expressions description: Please see the README on GitHub at diff --git a/resources/contextualization.yaml b/resources/contextualization.yaml --- a/resources/contextualization.yaml +++ b/resources/contextualization.yaml @@ -7,6 +7,10 @@ # structurally, replacing each ΞΎ with the context c, descending through # dispatches and applications and stopping at formations β€” which introduce their # own scope and are returned untouched β€” and at the global Ξ¦ and termination βŠ₯. +# The context c is supplied by the caller: DOT dispatching 𝜏 on a formation +# passes that formation WITHOUT the dispatched binding (⟦𝐡1, 𝐡2⟧), so a +# self-referential ΞΎ resolves to an object that lacks 𝜏 and collapses to βŠ₯ +# rather than re-deriving the dispatch and diverging. # # Each rule is an inference rule: when 'match' matches the term and 'c-match' # matches the context (binding the meta c), the rule yields the conclusion diff --git a/resources/normalize/dot.yaml b/resources/normalize/dot.yaml --- a/resources/normalize/dot.yaml +++ b/resources/normalize/dot.yaml @@ -1,6 +1,15 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT --- +# Dispatch 𝜏 on a formation: contextualize the dispatched body 𝑛 and decorate +# it with the whole formation as ρ. The contextualization context is the +# formation WITHOUT the dispatched binding β€” ⟦𝐡1, 𝐡2⟧, not ⟦𝐡1, 𝜏 ↦ 𝑛, 𝐡2⟧ β€” +# so a self-referential ΞΎ inside 𝑛 (as in ⟦ a ↦ ΞΎ ⟧.a or ⟦ a ↦ ΞΎ.a ⟧.a) no +# longer sees 𝜏. Such a self-reference then dispatches on a formation that +# lacks 𝜏 and collapses to βŠ₯ via stop/null/dd instead of rebuilding the same +# βŸ¦β€¦, 𝜏 ↦ 𝑛, β€¦βŸ§.𝜏 term and looping forever. ρ on line 'result' still binds the +# full formation, so sibling and Ο†-decoration references stay intact β€” only the +# self-ΞΎ path narrows, keeping normalization (near-)total. name: dot pattern: ⟦𝐡1, 𝜏 ↦ 𝑛, 𝐡2⟧.𝜏 result: 𝑒(ρ ↦ ⟦𝐡1, 𝜏 ↦ 𝑛, 𝐡2⟧) @@ -9,4 +18,4 @@ function: contextualize args: - 𝑛 - - ⟦𝐡1, 𝜏 ↦ 𝑛, 𝐡2⟧ + - ⟦𝐡1, 𝐡2⟧ diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs --- a/src/CLI/Helpers.hs +++ b/src/CLI/Helpers.hs @@ -9,6 +9,7 @@ import AST import CLI.Types import CLI.Validators (invalidCLIArguments) +import Canonizer (canonize) import Control.Exception import Control.Monad ((>=>)) import Data.Functor ((<&>)) @@ -24,7 +25,7 @@ import Parser (parseExpressionThrows) import qualified Printer as P import qualified Random as R -import Rewriter (Rewrittens') +import Rewriter (Rewritten, Rewrittens') import System.IO (getContents') import Text.Printf (printf) import XMIR (expressionToXMIR, parseXMIRThrows, printXMIR, xmirToPhi) @@ -62,11 +63,17 @@ parseInput xmir XMIR = parseXMIRThrows xmir >>= xmirToPhi parseInput _ LATEX = invalidCLIArguments "LaTeX cannot be used as input format" +-- The LaTeX sequence path canonizes inside 'rewrittensToLatex', after the meet +-- compression (see 'canonizedRewrittens' there); the remaining formats have no +-- meet pass, so canonization happens here right before rendering. printRewrittens :: PrintContext -> Rewrittens' -> IO String printRewrittens ctx@PrintCtx{..} rewrittens@(chain, _) | _outputFormat == LATEX && _sequence = rewrittensToLatex rewrittens (printCtxToLatexCtx ctx) - | _focus == ExRoot = mapM (printInFormat ctx . fst) chain <&> intercalate "\n" - | otherwise = mapM (\(expr, _) -> locatedExpression _focus expr >>= printExpression ctx) chain <&> intercalate "\n" + | _focus == ExRoot = mapM (printInFormat ctx . fst) (canonized chain) <&> intercalate "\n" + | otherwise = mapM (\(expr, _) -> locatedExpression _focus expr >>= printExpression ctx) (canonized chain) <&> intercalate "\n" + where + canonized :: [Rewritten] -> [Rewritten] + canonized = if _canonize then canonize else id printExpression :: PrintContext -> Expression -> IO String printExpression ctx@PrintCtx{..} ex = case _outputFormat of @@ -83,7 +90,7 @@ printCtxToLatexCtx :: PrintContext -> LatexContext printCtxToLatexCtx PrintCtx{..} = - LatexContext _sugar _line _margin _nonumber _compress _meetPopularity _meetLength _focus _expression _label _meetPrefix + LatexContext _sugar _line _margin _nonumber _compress _canonize _meetPopularity _meetLength _focus _expression _label _meetPrefix -- Get rules for rewriting depending on provided flags getRules :: Bool -> Bool -> [FilePath] -> IO [Y.Rule] diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -11,7 +11,6 @@ import CLI.Helpers import CLI.Types import CLI.Validators -import qualified Canonizer as C import Condition (parseConditionThrows) import Control.Exception import Control.Monad (unless, when) @@ -57,11 +56,10 @@ (_, _, _) -> (\rewritten -> P.printExpression' rewritten (_sugarType, UNICODE, _flat, _margin)) xmirCtx = XmirContext _omitListing _omitComments listing printCtx = toPrintCtx xmirCtx foc - canonize = if _canonize then C.canonize else id exclude = (`F.exclude` excluded) include = (`F.include` included) (rewrittens, exceeded) <- rewrite expr rules (context loc printCtx) - let rewrittens' = canonize $ exclude $ include (if _sequence then NE.toList rewrittens else [NE.last rewrittens]) + let rewrittens' = exclude $ include (if _sequence then NE.toList rewrittens else [NE.last rewrittens]) logDebug (printf "Printing rewritten πœ‘-expression as %s" (show _outputFormat)) exprs <- printRewrittens printCtx (rewrittens', exceeded) output _targetFile exprs @@ -124,6 +122,7 @@ xmirCtx _nonumber _compress + _canonize _sequence (justMeetPopularity _meetPopularity) (justMeetLength _meetLength) @@ -144,11 +143,10 @@ expr <- parseInput input _inputFormat seedTaus expr let printCtx = toPrintCtx foc - canonize = if _canonize then C.canonize else id exclude = (`F.exclude` excluded) include = (`F.include` included) (bytes, chain) <- dataize expr (context loc printCtx) - when _sequence (printRewrittens printCtx (canonize $ exclude $ include chain, False) >>= putStrLn) + when _sequence (printRewrittens printCtx (exclude $ include chain, False) >>= putStrLn) unless _quiet (putStrLn (P.printBytes bytes)) where validateOpts :: IO () @@ -171,6 +169,7 @@ defaultXmirContext _nonumber _compress + _canonize _sequence (justMeetPopularity _meetPopularity) (justMeetLength _meetLength) @@ -220,6 +219,7 @@ _flat _margin xmirCtx + False False False False diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs --- a/src/CLI/Types.hs +++ b/src/CLI/Types.hs @@ -22,6 +22,7 @@ , _xmirCtx :: XmirContext , _nonumber :: Bool , _compress :: Bool + , _canonize :: Bool , _sequence :: Bool , _meetPopularity :: Int , _meetLength :: Int diff --git a/src/Canonizer.hs b/src/Canonizer.hs --- a/src/Canonizer.hs +++ b/src/Canonizer.hs @@ -4,7 +4,7 @@ -- Canonization is the process of replacing function names attrached to -- lambda bindings with numbered identifiers started from 'F' -- like 'F1', 'F2', etc. -module Canonizer (canonize) where +module Canonizer (canonize, canonizeExpr) where import AST import qualified Data.Text as T @@ -34,6 +34,12 @@ let (expr', idx') = canonizeExpression expr idx (arg', idx'') = canonizeArgument arg idx' in (ExApplication expr' arg', idx'') +canonizeExpression (ExPhiMeet prefix num expr) idx = + let (expr', idx') = canonizeExpression expr idx + in (ExPhiMeet prefix num expr', idx') +canonizeExpression (ExPhiAgain prefix num expr) idx = + let (expr', idx') = canonizeExpression expr idx + in (ExPhiAgain prefix num expr', idx') canonizeExpression expr idx = (expr, idx) canonizeArgument :: Argument -> Int -> (Argument, Int) @@ -44,6 +50,11 @@ let (expr', idx') = canonizeExpression expr idx in (ArAlpha alpha expr', idx') +-- Canonize a single expression, restarting the 'F' counter from 1 so the +-- numbering is local to that expression. +canonizeExpr :: Expression -> Expression +canonizeExpr expr = fst (canonizeExpression expr 1) + canonize :: [Rewritten] -> [Rewritten] canonize [] = [] -canonize ((expr, maybeRule) : rest) = (fst (canonizeExpression expr 1), maybeRule) : canonize rest +canonize ((expr, maybeRule) : rest) = (canonizeExpr expr, maybeRule) : canonize rest diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -26,6 +26,7 @@ import AST import CST +import Canonizer (canonize, canonizeExpr) import Data.List (intercalate, nub) import Data.Maybe (isJust) import qualified Data.Text as T @@ -49,6 +50,7 @@ , _margin :: Int , _nonumber :: Bool , _compress :: Bool + , _canonize :: Bool , _meetPopularity :: Int , _meetLength :: Int , _focus :: Expression @@ -58,7 +60,7 @@ } defaultLatexContext :: LatexContext -defaultLatexContext = LatexContext SWEET SINGLELINE defaultMargin False False defaultMeetPopularity defaultMeetLength ExRoot Nothing Nothing Nothing +defaultLatexContext = LatexContext SWEET SINGLELINE defaultMargin False False False defaultMeetPopularity defaultMeetLength ExRoot Nothing Nothing Nothing defaultMeetPopularity :: Int defaultMeetPopularity = 50 @@ -168,6 +170,21 @@ let (exprs, rules) = unzip rewrittens in if _compress then zip (meetInExpressions exprs ctx) rules else rewrittens +-- Canonization runs after the meet compression, never before it: 'canonize' +-- renumbers Ξ» bindings by traversal position and restarts the counter for every +-- expression, so the same logical lambda ends up with a different 'Fn' in +-- different steps. Feeding those unstable names to the meet pass (which compares +-- sub-expressions by structural equality) would stop identical sub-expressions +-- from ever matching. So the meet pass sees the original names first, and only +-- its output is canonized. +canonizedRewrittens :: [Rewritten] -> LatexContext -> [Rewritten] +canonizedRewrittens rewrittens LatexContext{_canonize = shouldCanonize} = + if shouldCanonize then canonize rewrittens else rewrittens + +canonizedExpressions :: [Expression] -> LatexContext -> [Expression] +canonizedExpressions exprs LatexContext{_canonize = shouldCanonize} = + if shouldCanonize then map canonizeExpr exprs else exprs + -- Compress a sequence of focused sub-expressions the way 'compressedRewrittens' -- compresses whole expressions: the meet machinery factors recurring -- sub-expressions out across the sequence. Focusing happens before this, so the @@ -181,7 +198,7 @@ pure ( concat [ preamble ctx - , body (compressedRewrittens rewrittens ctx) (\expr -> renderToLatex (expressionToCST expr) ctx) + , body (canonizedRewrittens (compressedRewrittens rewrittens ctx) ctx) (\expr -> renderToLatex (expressionToCST expr) ctx) , ending exceeded ctx ] ) @@ -191,7 +208,7 @@ pure ( concat [ preamble ctx - , body (zip (compressedExpressions focused ctx) rules) (\expr -> renderToLatex (expressionToCST expr) ctx) + , body (zip (canonizedExpressions (compressedExpressions focused ctx) ctx) rules) (\expr -> renderToLatex (expressionToCST expr) ctx) , ending exceeded ctx ] ) diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -558,10 +558,10 @@ [ "\\begin{phiquation}" , "[[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{foo:1}{ [[ D> |42-| ]] } ) . |y| \\leadsto_{\\nameref{r:copy}}" , " \\leadsto \\phinoMeet{foo:2}{ [[ |x| -> \\phinoAgain{foo:1}, |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\phinoAgain{foo:2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\phinoAgain{foo:1} ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2}, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:copy}}" - , " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:stay}}" - , " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]]{.}" + , " \\leadsto \\phinoMeet{foo:3}{ [[ |x| -> \\phinoAgain{foo:1} ]] } . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:dot}}" + , " \\leadsto \\phinoAgain{foo:1} ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:3}, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:3} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:stay}}" + , " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:3} ]]{.}" , "\\end{phiquation}" ] ] @@ -574,10 +574,10 @@ [ "\\begin{phiquation}" , "[[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{1}{ [[ D> |42-| ]] } ) . |y| \\leadsto_{\\nameref{r:copy}}" , " \\leadsto \\phinoMeet{2}{ [[ |x| -> \\phinoAgain{1}, |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\phinoAgain{2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto \\phinoAgain{1} ( \\phiTerminal{\\rho} -> \\phinoAgain{2}, \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:copy}}" - , " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:stay}}" - , " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]]{.}" + , " \\leadsto \\phinoMeet{3}{ [[ |x| -> \\phinoAgain{1} ]] } . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:dot}}" + , " \\leadsto \\phinoAgain{1} ( \\phiTerminal{\\rho} -> \\phinoAgain{3}, \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:copy}}" + , " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{3} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:stay}}" + , " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{3} ]]{.}" , "\\end{phiquation}" ] ] @@ -652,7 +652,7 @@ [ unlines [ "\\begin{phiquation}" , "[[ |x| -> |y|, |y| -> |x| ]] . |x| \\leadsto_{\\nameref{r:dot}}" - , " \\leadsto [[ |x| -> |y|, |y| -> |x| ]] . |y| ( \\phiTerminal{\\rho} -> [[ |x| -> |y|, |y| -> |x| ]] ) \\leadsto" + , " \\leadsto [[ |y| -> |x| ]] . |y| ( \\phiTerminal{\\rho} -> [[ |x| -> |y|, |y| -> |x| ]] ) \\leadsto" , " \\leadsto \\dots" , "\\end{phiquation}" ] @@ -894,6 +894,12 @@ ["dataize", "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--hide=Q.bytes", "--hide=Q.number", "--locator=Q.@", "--focus=Q.@", "--meet-length=5", "--meet-popularity=1"] ["\\phinoMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\leadsto_{\\nameref{r:contextualize}}"] + it "compresses a canonized whole-expression sequence into a meet" $ + withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $ + testCLISucceeded + ["dataize", "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--meet-length=5", "--meet-popularity=1"] + ["\\phinoMeet{dataization:1}"] + it "dataizes with --locator" $ withStdin "[[ ex -> [[ @ -> Q.x ]], x -> [[ D> 42- ]] ]]" $ testCLISucceeded ["dataize", "--locator=Q.ex"] ["42-"] @@ -1012,7 +1018,7 @@ , " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }" , " { e ( \\phiTerminal{\\rho} -> [[ B_1, \\tau -> n, B_2 ]] ) }" , " { }" - , " { \\phinoContextualize{ n }{ [[ B_1, \\tau -> n, B_2 ]] }{ e } }" + , " { \\phinoContextualize{ n }{ [[ B_1, B_2 ]] }{ e } }" , "\\phinoNormalizationRule{miss}" , " { [[ B ]] ( \\tau -> e ) }" , " { T }"