phino 0.0.137 → 0.0.138
raw patch · 6 files changed
+135/−91 lines, 6 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- README.md +64/−64
- phino.cabal +1/−1
- resources/normalize/dot.yaml +16/−4
- resources/normalize/dotg.yaml +13/−4
- src/Morph.hs +39/−16
- test/CLISpec.hs +2/−2
README.md view
@@ -34,7 +34,7 @@ ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.136+cabal install --overwrite-policy=always phino-0.0.137 phino --version ``` @@ -1332,103 +1332,103 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1- total: 1810402.021 μs- avg: 181040.202 μs- min: 169827.114 μs- max: 204681.114 μs- std dev: 13154.216 μs+ total: 1768043.411 μs+ avg: 176804.341 μs+ min: 164618.314 μs+ max: 199224.069 μs+ std dev: 13380.573 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1- total: 7538811.226 μs- avg: 753881.123 μs- min: 694204.271 μs- max: 840942.094 μs- std dev: 41681.127 μs+ total: 7486501.601 μs+ avg: 748650.160 μs+ min: 678843.922 μs+ max: 882138.403 μs+ std dev: 54979.122 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1- total: 597613.462 μs- avg: 59761.346 μs- min: 54912.144 μs- max: 65342.026 μs- std dev: 2994.555 μs+ total: 580244.769 μs+ avg: 58024.477 μs+ min: 53745.242 μs+ max: 67886.567 μs+ std dev: 3972.462 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1- total: 4130310.545 μs- avg: 413031.054 μs- min: 404823.433 μs- max: 426597.938 μs- std dev: 7495.509 μs+ total: 3581738.830 μs+ avg: 358173.883 μs+ min: 353632.119 μs+ max: 364450.476 μs+ std dev: 3758.053 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1- total: 4284120.069 μs- avg: 428412.007 μs- min: 413571.324 μs- max: 445658.981 μs- std dev: 11624.236 μs+ total: 3586003.643 μs+ avg: 358600.364 μs+ min: 348511.573 μs+ max: 363372.650 μs+ std dev: 4666.744 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1- total: 13724020.907 μs- avg: 1372402.091 μs- min: 1344331.661 μs- max: 1409368.695 μs- std dev: 17786.287 μs+ total: 13668454.509 μs+ avg: 1366845.451 μs+ min: 1331880.047 μs+ max: 1392431.918 μs+ std dev: 20241.996 μs === morph/symbolic/demo/e1 === warmup: 3 iterations batches: 10 x 1- total: 866700.384 μs- avg: 86670.038 μs- min: 86184.411 μs- max: 87168.132 μs- std dev: 285.902 μs+ total: 902246.384 μs+ avg: 90224.638 μs+ min: 88957.751 μs+ max: 91781.678 μs+ std dev: 808.904 μs === morph/symbolic/demo/e2 === warmup: 3 iterations batches: 10 x 1- total: 1188660.494 μs- avg: 118866.049 μs- min: 116047.655 μs- max: 136278.751 μs- std dev: 5832.266 μs+ total: 1221686.976 μs+ avg: 122168.698 μs+ min: 119410.311 μs+ max: 123946.713 μs+ std dev: 1478.809 μs === morph/symbolic/demo/e3 === warmup: 3 iterations batches: 10 x 1- total: 1867565.431 μs- avg: 186756.543 μs- min: 185066.327 μs- max: 187725.046 μs- std dev: 1004.396 μs+ total: 1867130.933 μs+ avg: 186713.093 μs+ min: 182254.442 μs+ max: 199500.578 μs+ std dev: 4421.828 μs === morph/symbolic/demo/e4 === warmup: 3 iterations batches: 10 x 1- total: 623551.322 μs- avg: 62355.132 μs- min: 61620.682 μs- max: 63797.384 μs- std dev: 728.465 μs+ total: 638270.776 μs+ avg: 63827.078 μs+ min: 62286.130 μs+ max: 64675.326 μs+ std dev: 647.450 μs === morph/symbolic/demo/e5 === warmup: 3 iterations batches: 10 x 1- total: 186679.533 μs- avg: 18667.953 μs- min: 18384.769 μs- max: 18868.158 μs- std dev: 149.307 μs+ total: 189257.666 μs+ avg: 18925.767 μs+ min: 18570.345 μs+ max: 19165.345 μs+ std dev: 197.617 μs === morph/symbolic/native/e5 ===- warmup: 1 iterations+ warmup: 2 iterations batches: 4 x 1- total: 17947336.400 μs- avg: 4486834.100 μs- min: 4167627.934 μs- max: 4633560.228 μs- std dev: 189453.769 μs+ total: 17870892.725 μs+ avg: 4467723.181 μs+ min: 4368895.499 μs+ max: 4581076.732 μs+ std dev: 95768.713 μs ``` The results were calculated in [this GHA job][benchmark-gha]-on 2026-09-22 at 19:05,+on 2026-09-23 at 19:07, on Linux with 4 CPUs. <!-- benchmark_end -->@@ -1478,4 +1478,4 @@ [jna-native]: https://github.com/java-native-access/jna/blob/master/src/com/sun/jna/Native.java [jeo]: https://github.com/objectionary/jeo-maven-plugin [issue-1291]: https://github.com/objectionary/phino/issues/1291-[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/35770947279+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/35906648654
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.137+version: 0.0.138 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
resources/normalize/dot.yaml view
@@ -15,14 +15,26 @@ # dispatch this one covered alone. Where no universe is known — the 'rewrite' # command, and 'isNF' asking about a term on its own — 𝑒1 binds nothing, the # guard cannot hold, and this rule answers every dispatch as it always did.+# Neither rule dispatches on a formation holding both λ and Δ: 'dl' says such a+# formation is ⊥, and carrying it out into ρ would leave a ρ ↦ ⊥ in a normal+# form that 'dl' firing first reduces to ⊥ outright, so the answer would hang+# on rule order (#1395). name: dot pattern: ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧.𝜏1 e-match: 𝑒1 when:- not:- eq:- - ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧- - 𝑒1+ and:+ - not:+ eq:+ - ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧+ - 𝑒1+ - or:+ - disjoint:+ - [λ]+ - [𝐵1, 𝐵2]+ - disjoint:+ - [Δ]+ - [𝐵1, 𝐵2] result: 𝑒2(ρ ↦ ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧) where: - meta: 𝑒2
resources/normalize/dotg.yaml view
@@ -11,14 +11,23 @@ # a dispatch reaches this rule only once Φ has already been resolved that way. # Everything else is 'dot': the same pattern, the same contextualization # context, and a guard that is the exact complement of the one there, so the-# two never both answer a dispatch and never both refuse one.+# two never both answer a dispatch and never both refuse one, save a formation+# holding both λ and Δ, which both refuse and leave to 'dl' (#1395). name: dotg pattern: ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧.𝜏1 e-match: 𝑒1 when:- eq:- - ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧- - 𝑒1+ and:+ - eq:+ - ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧+ - 𝑒1+ - or:+ - disjoint:+ - [λ]+ - [𝐵1, 𝐵2]+ - disjoint:+ - [Δ]+ - [𝐵1, 𝐵2] result: 𝑒2(ρ ↦ Φ) where: - meta: 𝑒2
src/Morph.hs view
@@ -440,19 +440,21 @@ -- allows. Every entry is charged to the '--max-steps' budget, which is what -- bounds the walk. deepened :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)-deepened expr univ state ctx = go (Just ctx._site) Nothing ExXi expr state ctx+deepened expr univ state ctx = go False (Just ctx._site) Nothing ExXi expr state ctx where -- A term as it was written, together with the locator naming it where one -- does and with what its free ξ stands for: the formation the walk entered -- it from, without the binding it came from, exactly the context the 'dot' -- rule hands a dispatched body. At the top there is no such formation, so ξ -- stands for itself and contextualization leaves the term alone, and the- -- locator is the one the whole run was aimed at.- go :: Maybe Expression -> Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)- go standing dispatched context term state' caller = do+ -- locator is the one the whole run was aimed at. Whether the formation a+ -- term is bound in has its ρ bound is what decides whether a void ρ keeps+ -- a formation from being entered (see 'parts'); at the top there is none.+ go :: Bool -> Maybe Expression -> Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)+ go attached standing dispatched context term state' caller = do let here = sited standing caller ctx' <- deeper here- (walked, walkedState) <- parts standing context term state' here+ (walked, walkedState) <- parts attached standing context term state' here (answer, answered) <- ctx'._fire dispatched (contextualize walked context) univ walkedState ctx' pure (fromMaybe walked answer, answered) -- The context a term is walked in, aimed at the term itself where a locator@@ -466,19 +468,36 @@ -- where they were, so the term keeps the shape it was written in. Only a -- binding of a formation carries the locator further: the head of a -- dispatch and both sides of an application stand under no attribute, so- -- what they hold is entered with no locator of its own.- parts :: Maybe Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)- parts standing _ (ExFormation bds) state' caller = do+ -- what they hold is entered with no locator of its own. An abstract+ -- formation, one holding a void, is a method nobody applied: its body is+ -- parametric, walking it can only end in ⊥ or a stuck term, and a λ there+ -- dataizing a parameter would end the whole run, so it is handed back as it+ -- was written (#1393). A void ρ counts as well where the formation it is+ -- bound in has its own ρ bound: ρ is the parameter a dispatch binds, and+ -- 'dot' binds it in every copy a reduction reaches, so a formation still+ -- holding ρ ↦ ∅ inside such a copy is a method nobody dispatched, and its+ -- ξ.ρ can only collapse to ⊥ (#1397). The program as it was written holds+ -- ρ ↦ ∅ all the way down, since nothing dispatched it either, and its+ -- objects are walked the way they always were.+ parts :: Bool -> Maybe Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)+ parts attached _ _ term@(ExFormation bds) state' _+ | any abstract bds = pure (term, state')+ where+ abstract :: Binding -> Bool+ abstract (BiVoid AtRho) = attached+ abstract (BiVoid _) = True+ abstract _ = False+ parts _ standing _ (ExFormation bds) state' caller = do (entered, state'') <- bindings standing bds bds state' caller pure (ExFormation entered, state'')- parts _ context (ExDispatch target attr) state' caller = do- (entered, state'') <- go Nothing (Just attr) context target state' caller+ parts _ _ context (ExDispatch target attr) state' caller = do+ (entered, state'') <- go False Nothing (Just attr) context target state' caller pure (ExDispatch entered attr, state'')- parts _ context (ExApplication target arg) state' caller = do- (entered, state'') <- go Nothing Nothing context target state' caller+ parts _ _ context (ExApplication target arg) state' caller = do+ (entered, state'') <- go False Nothing Nothing context target state' caller (applied, state''') <- argument context arg state'' caller pure (ExApplication entered applied, state''')- parts _ _ term state' _ = pure (term, state')+ parts _ _ _ term state' _ = pure (term, state') -- Walk the bindings of a formation left to right, threading the state -- through them. Only what the formation itself holds is entered: ρ names -- the object around it rather than one inside it, and a void, Δ or λ@@ -489,9 +508,13 @@ bindings _ _ [] state' _ = pure ([], state') bindings standing whole (BiTau attr body : rest) state' caller | attr /= AtRho = do- (entered, state'') <- go (fmap (`ExDispatch` attr) standing) Nothing (scope attr whole) body state' caller+ (entered, state'') <- go (any bound whole) (fmap (`ExDispatch` attr) standing) Nothing (scope attr whole) body state' caller (others, state''') <- bindings standing whole rest state'' caller pure (BiTau attr entered : others, state''')+ where+ bound :: Binding -> Bool+ bound (BiTau AtRho _) = True+ bound _ = False bindings standing whole (bd : rest) state' caller = do (others, state'') <- bindings standing whole rest state' caller pure (bd : others, state'')@@ -508,10 +531,10 @@ -- applies is walked by the caller and the argument it binds is walked here. argument :: Expression -> Argument -> State -> ReduceContext -> IO (Argument, State) argument context (ArTau attr arg) state' caller = do- (entered, state'') <- go Nothing Nothing context arg state' caller+ (entered, state'') <- go False Nothing Nothing context arg state' caller pure (ArTau attr entered, state'') argument context (ArAlpha alpha arg) state' caller = do- (entered, state'') <- go Nothing Nothing context arg state' caller+ (entered, state'') <- go False Nothing Nothing context arg state' caller pure (ArAlpha alpha entered, state'') -- The premise binding the given expression meta, if any. The conclusion of a
test/CLISpec.hs view
@@ -2197,12 +2197,12 @@ , "\\phinoNormalizationRule{dot}" , " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }" , " { e_2 ( \\phiTerminal{\\rho} -> [[ B_1, \\tau -> n, B_2 ]] ) }"- , " { [[ B_1, \\tau -> n, B_2 ]] \\not= e_1 }"+ , " { [[ B_1, \\tau -> n, B_2 ]] \\not= e_1 \\;\\text{and}\\; \\lparen [ L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\;\\text{or}\\; [ D ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\rparen }" , " { \\phinoContextualize{ n }{ [[ B_1, B_2 ]] }{ e_2 } }" , "\\phinoNormalizationRule{dotg}" , " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }" , " { e_2 ( \\phiTerminal{\\rho} -> Q ) }"- , " { [[ B_1, \\tau -> n, B_2 ]] = e_1 }"+ , " { [[ B_1, \\tau -> n, B_2 ]] = e_1 \\;\\text{and}\\; \\lparen [ L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\;\\text{or}\\; [ D ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\rparen }" , " { \\phinoContextualize{ n }{ [[ B_1, B_2 ]] }{ e_2 } }" , "\\phinoNormalizationRule{miss}" , " { [[ B ]] ( \\tau -> e ) }"