packages feed

phino 0.0.100 → 0.0.101

raw patch · 9 files changed

+81/−26 lines, 9 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

+ Canonizer: canonizeExpr :: Expression -> Expression
+ LaTeX: [_canonize] :: LatexContext -> Bool
- CLI.Types: PrintCtx :: SugarType -> LineFormat -> Int -> XmirContext -> Bool -> Bool -> Bool -> Int -> Int -> Expression -> Maybe String -> Maybe String -> Maybe String -> IOFormat -> PrintContext
+ CLI.Types: PrintCtx :: SugarType -> LineFormat -> Int -> XmirContext -> Bool -> Bool -> Bool -> Bool -> Int -> Int -> Expression -> Maybe String -> Maybe String -> Maybe String -> IOFormat -> PrintContext
- LaTeX: LatexContext :: SugarType -> LineFormat -> Int -> Bool -> Bool -> Int -> Int -> Expression -> Maybe String -> Maybe String -> Maybe String -> LatexContext
+ LaTeX: LatexContext :: SugarType -> LineFormat -> Int -> Bool -> Bool -> Bool -> Int -> Int -> Expression -> Maybe String -> Maybe String -> Maybe String -> LatexContext

Files

phino.cabal view
@@ -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 <https://github.com/objectionary/phino#readme>
resources/contextualization.yaml view
@@ -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
resources/normalize/dot.yaml view
@@ -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⟧
src/CLI/Helpers.hs view
@@ -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]
src/CLI/Runners.hs view
@@ -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
src/CLI/Types.hs view
@@ -22,6 +22,7 @@   , _xmirCtx :: XmirContext   , _nonumber :: Bool   , _compress :: Bool+  , _canonize :: Bool   , _sequence :: Bool   , _meetPopularity :: Int   , _meetLength :: Int
src/Canonizer.hs view
@@ -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
src/LaTeX.hs view
@@ -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         ]     )
test/CLISpec.hs view
@@ -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 }"