diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ ```bash cabal update -cabal install --overwrite-policy=always phino-0.0.0.73 +cabal install --overwrite-policy=always phino-0.0.0.74 phino --version ``` @@ -205,7 +205,10 @@ ## Explain -You can _explain_ rewriting rule by printing them in [LaTeX][latex] format: +You can _explain_ the built-in rules by printing them in [LaTeX][latex] +format. Pass exactly one of `--normalize`, `--morph` or `--dataize` for +the rewriting, morphing (๐•„) or dataization (๐”ป) rules (or `--rule` for a +custom rule file): ```bash $ phino explain --normalize @@ -229,6 +232,42 @@ \end{tabular} ``` +The morphing and dataization rules are printed the same way: + +```bash +$ phino explain --morph +\begin{tabular}{rl} +\trrule{Mprim} + { \mathbb{M}( e ) } + { e } + { if $ e \in \mathcal{P} $ } + { } +... +\trrule{Mphi} + { \mathbb{M}( Q . \tau * t ) } + { \mathbb{M}( e * t ) } + { } + { where $ e \coloneqq global( \tau ) $ } +\end{tabular} +``` + +```bash +$ phino explain --dataize +\begin{tabular}{rl} +\trrule{delta} + { \mathbb{D}( [[ B_1, D> ฮด, B_2 ]] ) } + { ฮด } + { } + { } +... +\trrule{none} + { \mathbb{D}( e ) } + { \varnothing } + { } + { } +\end{tabular} +``` + For more details, use `phino [COMMAND] --help` option. ## Rule structure @@ -355,10 +394,13 @@ * `!a` || `๐œ` - attribute * `!e` || `๐‘’` - any expression +* `!n` || `๐‘›` - any expression that is already in normal form (behaves like + `!e`/`๐‘’`, but only binds a sub-expression in NF, so no explicit + `nf:` guard is needed) * `!B` || `๐ต` - list of bindings * `!d` || `ฮด` - bytes in meta delta binding -* `!t` - tail after expression, sequence of applications and/or dispatches, - must start only with dispatch +* `!t` - tail after expression, a possibly empty sequence of applications + and/or dispatches * `!F` - function name in meta lambda binding Every meta variable may also be used with an integer index, like `!B1` or `๐œ0`. @@ -388,55 +430,55 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1 - total: 1309885.482 ฮผs - avg: 130988.548 ฮผs - min: 119182.611 ฮผs - max: 164424.034 ฮผs - std dev: 17120.368 ฮผs + total: 1412671.918 ฮผs + avg: 141267.192 ฮผs + min: 127755.002 ฮผs + max: 177453.762 ฮผs + std dev: 17165.732 ฮผs === parse/xmir === warmup: 3 iterations batches: 10 x 1 - total: 8166516.875 ฮผs - avg: 816651.687 ฮผs - min: 746631.521 ฮผs - max: 905684.717 ฮผs - std dev: 58484.723 ฮผs + total: 7639818.091 ฮผs + avg: 763981.809 ฮผs + min: 708011.145 ฮผs + max: 797305.119 ฮผs + std dev: 24602.554 ฮผs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1 - total: 1020794.192 ฮผs - avg: 102079.419 ฮผs - min: 98049.050 ฮผs - max: 109067.886 ฮผs - std dev: 2847.343 ฮผs + total: 426645.736 ฮผs + avg: 42664.574 ฮผs + min: 40102.854 ฮผs + max: 47835.610 ฮผs + std dev: 2300.441 ฮผs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1 - total: 5308178.500 ฮผs - avg: 530817.850 ฮผs - min: 500095.243 ฮผs - max: 590475.507 ฮผs - std dev: 29328.246 ฮผs + total: 3941287.369 ฮผs + avg: 394128.737 ฮผs + min: 372511.010 ฮผs + max: 405677.385 ฮผs + std dev: 9679.300 ฮผs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1 - total: 5104935.589 ฮผs - avg: 510493.559 ฮผs - min: 449111.602 ฮผs - max: 555034.745 ฮผs - std dev: 36795.722 ฮผs + total: 4011952.457 ฮผs + avg: 401195.246 ฮผs + min: 382116.656 ฮผs + max: 426194.357 ฮผs + std dev: 13451.138 ฮผs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1 - total: 15066270.227 ฮผs - avg: 1506627.023 ฮผs - min: 1427131.813 ฮผs - max: 1580723.339 ฮผs - std dev: 45705.458 ฮผs + total: 13481660.845 ฮผs + avg: 1348166.084 ฮผs + min: 1297555.496 ฮผs + max: 1397510.998 ฮผs + std dev: 35358.091 ฮผs ``` The results were calculated in [this GHA job][benchmark-gha] -on 2026-06-03 at 13:35, +on 2026-06-08 at 09:53, on Linux with 4 CPUs. @@ -472,4 +514,4 @@ [jna]: https://github.com/java-native-access/jna [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 -[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/26888116250 +[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/27129589244 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.0.74 +version: 0.0.0.75 license: MIT synopsis: Command-Line Manipulator of ๐œ‘-Calculus Expressions description: Please see the README on GitHub at @@ -12,7 +12,7 @@ copyright: 2025 Objectionary.com category: Language, Code Analysis build-type: Simple -extra-source-files: resources/*.yaml +extra-source-files: resources/*.yaml resources/normalize/*.yaml extra-doc-files: README.md source-repository head diff --git a/resources/alpha.yaml b/resources/alpha.yaml deleted file mode 100644 --- a/resources/alpha.yaml +++ /dev/null @@ -1,10 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -name: alpha -pattern: โŸฆ๐ต1, ๐œ1 โ†ฆ โˆ…, ๐ต2โŸง(๐œ2 โ†ฆ ๐‘’) -result: โŸฆ๐ต1, ๐œ1 โ†ฆ โˆ…, ๐ต2โŸง(๐œ1 โ†ฆ ๐‘’) -when: - eq: - - index: ๐œ2 - - domain: ๐ต1 diff --git a/resources/copy.yaml b/resources/copy.yaml deleted file mode 100644 --- a/resources/copy.yaml +++ /dev/null @@ -1,10 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -name: copy -pattern: โŸฆ ๐ต1, ๐œ โ†ฆ โˆ…, ๐ต2 โŸง(๐œ โ†ฆ ๐‘’) -result: โŸฆ ๐ต1, ๐œ โ†ฆ ๐‘’, ๐ต2 โŸง -when: - and: - - xi-free: ๐‘’ - - nf: ๐‘’ diff --git a/resources/dataization.yaml b/resources/dataization.yaml new file mode 100644 --- /dev/null +++ b/resources/dataization.yaml @@ -0,0 +1,40 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +# Dataization ๐”ป โ€” applied top-to-bottom, first matching clause wins. + +- name: delta + description: '๐”ป(โŸฆ๐ต1, ฮ” โค ฮด, ๐ต2โŸง) โŸฟ ฮด' + match: โŸฆ๐ต1, ฮ” โค ฮด, ๐ต2โŸง + then: ฮด + +- name: box + description: '๐”ป(โŸฆ๐ต1, ฯ† โ†ฆ e, ๐ต2โŸง) โŸฟ ๐”ป(๐’ž(e)) if [ฮ”, ฮป] โˆฉ (๐ต1 โˆช ๐ต2) = โˆ…' + match: โŸฆ๐ต1, ฯ† โ†ฆ ๐‘’, ๐ต2โŸง + where: + - meta: ๐‘’1 + function: contextualize + args: + - ๐‘’ + - โŸฆ๐ต1, ฯ† โ†ฆ ๐‘’, ๐ต2โŸง + when: + disjoint: + - [ฮ”, ฮป] + - [๐ต1, ๐ต2] + then: + dataize: ๐‘’1 + +- name: norm + description: '๐”ป(e) โŸฟ ๐”ป(๐•„(e)) if e โˆ‰ ๐’ซ' + match: ๐‘’ + when: + not: + primitive: ๐‘’ + then: + dataize: + morph: ๐‘’ + +- name: none + description: '๐”ป(e) โŸฟ nothing otherwise' + match: ๐‘’ + then: nothing diff --git a/resources/dc.yaml b/resources/dc.yaml deleted file mode 100644 --- a/resources/dc.yaml +++ /dev/null @@ -1,6 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -name: dc -pattern: โŠฅ(๐œ โ†ฆ ๐‘’) -result: โŠฅ diff --git a/resources/dd.yaml b/resources/dd.yaml deleted file mode 100644 --- a/resources/dd.yaml +++ /dev/null @@ -1,6 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -name: dd -pattern: โŠฅ.๐œ -result: โŠฅ diff --git a/resources/dot.yaml b/resources/dot.yaml deleted file mode 100644 --- a/resources/dot.yaml +++ /dev/null @@ -1,14 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -name: dot -pattern: โŸฆ๐ต1, ๐œ โ†ฆ ๐‘’1, ๐ต2โŸง.๐œ -result: ๐‘’2(ฯ โ†ฆ โŸฆ๐ต1, ๐œ โ†ฆ ๐‘’1, ๐ต2โŸง) -when: - nf: ๐‘’1 -where: - - meta: ๐‘’2 - function: contextualize - args: - - ๐‘’1 - - โŸฆ๐ต1, ๐œ โ†ฆ ๐‘’1, ๐ต2โŸง diff --git a/resources/miss.yaml b/resources/miss.yaml deleted file mode 100644 --- a/resources/miss.yaml +++ /dev/null @@ -1,14 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -name: miss -pattern: โŸฆ๐ตโŸง(๐œ โ†ฆ ๐‘’) -result: โŠฅ -when: - and: - - not: - in: - - ๐œ - - ๐ต - - not: - alpha: ๐œ diff --git a/resources/morphing.yaml b/resources/morphing.yaml new file mode 100644 --- /dev/null +++ b/resources/morphing.yaml @@ -0,0 +1,48 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +# Morphing ๐•„ โ€” applied top-to-bottom, first matching clause wins. + +- name: Mprim + description: '๐•„(e) โŸฟ e if e โˆˆ ๐’ซ' + match: ๐‘’ + when: + primitive: ๐‘’ + then: ๐‘’ + +- name: Mnmz + description: '๐•„(e) โŸฟ ๐•„(๐’ฉ(e)) if e โˆ‰ NF' + match: ๐‘’ + when: + not: + nf: ๐‘’ + then: + morph: + normalize: ๐‘’ + +- name: Mlambda + description: '๐•„(โŸฆ๐ต1, ฮป โค F, ๐ต2โŸง * t) โŸฟ ๐•„(F(โŸฆ๐ต1, ๐ต2โŸง) * t)' + match: 'โŸฆ๐ต1, ฮป โค !F, ๐ต2โŸง * !t' + where: + - meta: ๐‘’ + function: lambda + args: + - 'โŸฆ๐ต1, ฮป โค !F, ๐ต2โŸง' + then: + morph: '๐‘’ * !t' + +- name: Mphi + description: '๐•„(ฮฆ.ฯ„ * t) โŸฟ ๐•„(e * t) if ฮฆ โ†ฆ โŸฆ๐ต1, ฯ„ โ†ฆ e, ๐ต2โŸง' + match: 'ฮฆ.๐œ * !t' + where: + - meta: ๐‘’ + function: global + args: + - ๐œ + then: + morph: '๐‘’ * !t' + +- name: Mstuck + description: '๐•„(e) โŸฟ โŠฅ otherwise' + match: ๐‘’ + then: โŠฅ diff --git a/resources/normalize/alpha.yaml b/resources/normalize/alpha.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/alpha.yaml @@ -0,0 +1,10 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: alpha +pattern: โŸฆ๐ต1, ๐œ1 โ†ฆ โˆ…, ๐ต2โŸง(๐œ2 โ†ฆ ๐‘’) +result: โŸฆ๐ต1, ๐œ1 โ†ฆ โˆ…, ๐ต2โŸง(๐œ1 โ†ฆ ๐‘’) +when: + eq: + - index: ๐œ2 + - domain: ๐ต1 diff --git a/resources/normalize/copy.yaml b/resources/normalize/copy.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/copy.yaml @@ -0,0 +1,8 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: copy +pattern: โŸฆ ๐ต1, ๐œ โ†ฆ โˆ…, ๐ต2 โŸง(๐œ โ†ฆ ๐‘›) +result: โŸฆ ๐ต1, ๐œ โ†ฆ ๐‘›, ๐ต2 โŸง +when: + xi-free: ๐‘› diff --git a/resources/normalize/dc.yaml b/resources/normalize/dc.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/dc.yaml @@ -0,0 +1,6 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: dc +pattern: โŠฅ(๐œ โ†ฆ ๐‘’) +result: โŠฅ diff --git a/resources/normalize/dd.yaml b/resources/normalize/dd.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/dd.yaml @@ -0,0 +1,6 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: dd +pattern: โŠฅ.๐œ +result: โŠฅ diff --git a/resources/normalize/dot.yaml b/resources/normalize/dot.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/dot.yaml @@ -0,0 +1,12 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: dot +pattern: โŸฆ๐ต1, ๐œ โ†ฆ ๐‘›, ๐ต2โŸง.๐œ +result: ๐‘’(ฯ โ†ฆ โŸฆ๐ต1, ๐œ โ†ฆ ๐‘›, ๐ต2โŸง) +where: + - meta: ๐‘’ + function: contextualize + args: + - ๐‘› + - โŸฆ๐ต1, ๐œ โ†ฆ ๐‘›, ๐ต2โŸง diff --git a/resources/normalize/miss.yaml b/resources/normalize/miss.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/miss.yaml @@ -0,0 +1,14 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: miss +pattern: โŸฆ๐ตโŸง(๐œ โ†ฆ ๐‘’) +result: โŠฅ +when: + and: + - not: + in: + - ๐œ + - ๐ต + - not: + alpha: ๐œ diff --git a/resources/normalize/null.yaml b/resources/normalize/null.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/null.yaml @@ -0,0 +1,6 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: 'null' +pattern: โŸฆ๐ต1, ๐œ โ†ฆ โˆ…, ๐ต2โŸง.๐œ +result: โŠฅ diff --git a/resources/normalize/over.yaml b/resources/normalize/over.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/over.yaml @@ -0,0 +1,11 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: over +pattern: โŸฆ๐ต1, ๐œ โ†ฆ ๐‘’1, ๐ต2โŸง(๐œ โ†ฆ ๐‘’2) +result: โŠฅ +when: + not: + eq: + - ๐œ + - ฯ diff --git a/resources/normalize/phi.yaml b/resources/normalize/phi.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/phi.yaml @@ -0,0 +1,15 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: phi +pattern: โŸฆ๐ตโŸง.๐œ +result: โŸฆ๐ตโŸง.ฯ†.๐œ +when: + and: + - in: + - ฯ† + - ๐ต + - not: + in: + - ๐œ + - ๐ต diff --git a/resources/normalize/stay.yaml b/resources/normalize/stay.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/stay.yaml @@ -0,0 +1,6 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: stay +pattern: โŸฆ๐ต1, ฯ โ†ฆ ๐‘’1, ๐ต2โŸง(ฯ โ†ฆ ๐‘’2) +result: โŸฆ๐ต1, ฯ โ†ฆ ๐‘’1, ๐ต2โŸง diff --git a/resources/normalize/stop.yaml b/resources/normalize/stop.yaml new file mode 100644 --- /dev/null +++ b/resources/normalize/stop.yaml @@ -0,0 +1,20 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: stop +pattern: โŸฆ๐ตโŸง.๐œ +result: โŠฅ +when: + and: + - not: + in: + - ๐œ + - ๐ต + - not: + in: + - ฯ† + - ๐ต + - not: + in: + - ฮป + - ๐ต diff --git a/resources/null.yaml b/resources/null.yaml deleted file mode 100644 --- a/resources/null.yaml +++ /dev/null @@ -1,6 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -name: 'null' -pattern: โŸฆ๐ต1, ๐œ โ†ฆ โˆ…, ๐ต2โŸง.๐œ -result: โŠฅ diff --git a/resources/over.yaml b/resources/over.yaml deleted file mode 100644 --- a/resources/over.yaml +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -name: over -pattern: โŸฆ๐ต1, ๐œ โ†ฆ ๐‘’1, ๐ต2โŸง(๐œ โ†ฆ ๐‘’2) -result: โŠฅ -when: - not: - eq: - - ๐œ - - ฯ diff --git a/resources/phi.yaml b/resources/phi.yaml deleted file mode 100644 --- a/resources/phi.yaml +++ /dev/null @@ -1,15 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -name: phi -pattern: โŸฆ๐ตโŸง.๐œ -result: โŸฆ๐ตโŸง.ฯ†.๐œ -when: - and: - - in: - - ฯ† - - ๐ต - - not: - in: - - ๐œ - - ๐ต diff --git a/resources/stay.yaml b/resources/stay.yaml deleted file mode 100644 --- a/resources/stay.yaml +++ /dev/null @@ -1,6 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -name: stay -pattern: โŸฆ๐ต1, ฯ โ†ฆ ๐‘’1, ๐ต2โŸง(ฯ โ†ฆ ๐‘’2) -result: โŸฆ๐ต1, ฯ โ†ฆ ๐‘’1, ๐ต2โŸง diff --git a/resources/stop.yaml b/resources/stop.yaml deleted file mode 100644 --- a/resources/stop.yaml +++ /dev/null @@ -1,20 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -# SPDX-License-Identifier: MIT ---- -name: stop -pattern: โŸฆ๐ตโŸง.๐œ -result: โŠฅ -when: - and: - - not: - in: - - ๐œ - - ๐ต - - not: - in: - - ฯ† - - ๐ต - - not: - in: - - ฮป - - ๐ต diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs --- a/src/CLI/Helpers.hs +++ b/src/CLI/Helpers.hs @@ -1,5 +1,6 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT +{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -9,11 +10,13 @@ import CLI.Types import CLI.Validators (invalidCLIArguments) import Control.Exception +import Control.Monad ((>=>)) import Data.Functor ((<&>)) import Data.List (intercalate) import Data.Maybe import Deps (SaveStepFunc, saveStep) import Encoding +import Functions (execFunctions) import LaTeX (LatexContext (..), defaultMeetLength, defaultMeetPopularity, expressionToLaTeX, programToLaTeX, rewrittensToLatex) import Locator (locatedExpression) import Logger @@ -99,12 +102,24 @@ else do logDebug (printf "Using rules from files: [%s]" (intercalate ", " rules)) yamls <- mapM M.ensuredFile rules - mapM Y.yamlRule yamls + mapM (Y.yamlRule >=> validateRewriteRule) yamls if shuffle then do logDebug "The --shuffle option is provided, rules are used in random order" M.shuffle ordered else pure ordered + +-- Pass a user-supplied rewriting rule through unchanged, or fail fast if it +-- references a build-term function which needs the dataization context: those +-- work only for dataization and morphing, never for plain rewriting. +validateRewriteRule :: Y.Rule -> IO Y.Rule +validateRewriteRule rule = + let used = maybe [] (map Y.function) rule.where_ + in case filter (`elem` execFunctions) used of + [] -> pure rule + (fn : _) -> + invalidCLIArguments + (printf "Function '%s' in rule '%s' is available only for dataization and morphing, not for rewriting" fn rule.name) -- Output content printOut :: Maybe FilePath -> String -> IO () diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs --- a/src/CLI/Parsers.hs +++ b/src/CLI/Parsers.hs @@ -174,6 +174,12 @@ optNormalize :: Parser Bool optNormalize = switch (long "normalize" <> help "Use built-in normalization rules") +optMorph :: Parser Bool +optMorph = switch (long "morph" <> help "Explain built-in morphing rules") + +optDataize :: Parser Bool +optDataize = switch (long "dataize" <> help "Explain built-in dataization rules") + optTarget :: Parser (Maybe FilePath) optTarget = optional (strOption (long "target" <> short 't' <> metavar "FILE" <> help "File to save output to")) @@ -226,6 +232,8 @@ <*> optLogLines <*> optRule <*> optNormalize + <*> optMorph + <*> optDataize <*> optShuffle <*> optTarget ) diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -21,7 +22,7 @@ import Encoding import qualified Filter as F import Functions (buildTerm) -import LaTeX (explainRules) +import LaTeX (explainDataizeRules, explainMorphRules, explainRules) import Logger import Margin (defaultMargin) import Merge (merge) @@ -93,7 +94,7 @@ validateBreakpoint :: Maybe String -> [Y.Rule] -> IO () validateBreakpoint Nothing _ = pure () validateBreakpoint (Just rule) rules = - let names = map Y.name rules + let names = map (.name) rules in unless (rule `elem` names) (invalidCLIArguments (printf "The rule '%s' provided in '--breakpoint' option is absent across given rewriting rules: %s" rule (intercalate ", " names))) @@ -182,11 +183,18 @@ runExplain :: OptsExplain -> IO () runExplain OptsExplain{..} = do validateOpts - rules <- getRules _normalize _shuffle _rules - printOut _targetFile (explainRules rules) + explained >>= printOut _targetFile where + explained :: IO String + explained + | _morph = pure (explainMorphRules Y.morphingRules) + | _dataize = pure (explainDataizeRules Y.dataizationRules) + | otherwise = explainRules <$> getRules _normalize _shuffle _rules validateOpts :: IO () - validateOpts = when (null _rules && not _normalize) (invalidCLIArguments "Either --rule or --normalize must be specified") + validateOpts = do + let selected = length (filter id [not (null _rules), _normalize, _morph, _dataize]) + when (selected == 0) (invalidCLIArguments "Either --rule, --normalize, --morph or --dataize must be specified") + when (selected > 1) (invalidCLIArguments "Only one of --rule, --normalize, --morph or --dataize can be specified") runMerge :: OptsMerge -> IO () runMerge OptsMerge{..} = do diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs --- a/src/CLI/Types.hs +++ b/src/CLI/Types.hs @@ -106,6 +106,8 @@ , _logLines :: Int , _rules :: [FilePath] , _normalize :: Bool + , _morph :: Bool + , _dataize :: Bool , _shuffle :: Bool , _targetFile :: Maybe FilePath } diff --git a/src/CST.hs b/src/CST.hs --- a/src/CST.hs +++ b/src/CST.hs @@ -80,6 +80,8 @@ data META_HEAD = E -- ๐‘’ | E' -- e + | N -- ๐‘› + | N' -- n | A -- a | TAU -- ๐œ | TAU' -- \tau @@ -222,6 +224,8 @@ | CO_COMPARE {left :: COMPARABLE, equal :: EQUAL, right :: COMPARABLE} | CO_MATCHES {regex :: String, expr :: EXPRESSION} | CO_PART_OF {expr :: EXPRESSION, binding :: BINDING} + | CO_PRIMITIVE {expr :: EXPRESSION, belongs :: BELONGING} + | CO_DISJOINT {attrs :: [ATTRIBUTE], groups :: [BINDING]} deriving (Eq, Show) data EXTRA_ARG @@ -264,6 +268,14 @@ metaTail :: T.Text -> T.Text metaTail = T.drop 1 +-- The first character of an expression meta name encodes its kind: +-- 'n'-prefixed names are normal-form-constrained '๐‘›' metas, everything +-- else is an ordinary '๐‘’' meta. +exMetaHead :: T.Text -> META_HEAD +exMetaHead mt + | T.isPrefixOf "n" mt = N + | otherwise = E + -- This class is used to convert AST to CST -- CST is created with sugar and unicode -- All further transformations must consider that @@ -276,7 +288,7 @@ instance ToCST Expression EXPRESSION where toCST ExGlobal _ = EX_GLOBAL ฮฆ toCST ExThis _ = EX_XI XI - toCST (ExMeta mt) _ = EX_META (META NO_EXCL E (metaTail mt)) + toCST (ExMeta mt) _ = EX_META (META NO_EXCL (exMetaHead mt) (metaTail mt)) toCST (ExMetaTail expr mt) ctx = EX_META_TAIL (toCST expr ctx) (META EXCL TAIL (metaTail mt)) toCST ExTermination _ = EX_TERMINATION DEAD toCST (ExPhiMeet prefix idx expr) ctx = EX_PHI_MEET prefix idx (toCST expr ctx) @@ -466,6 +478,9 @@ toCST (Y.Not (Y.In attr binding)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_BINDING (bindingsToCST [binding])) toCST (Y.Not (Y.Eq left right)) _ = CO_COMPARE (comparableToCST left) NOT_EQUAL (comparableToCST right) toCST (Y.Not (Y.Alpha attr)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_ATTRIBUTES [attributeToCST (AtAlpha 0), attributeToCST (AtAlpha 1), AT_REST DOTS]) + toCST (Y.Not (Y.Primitive expr)) _ = CO_PRIMITIVE (expressionToCST expr) NOT_IN + toCST (Y.Primitive expr) _ = CO_PRIMITIVE (expressionToCST expr) IN + toCST (Y.Disjoint attrs groups) _ = CO_DISJOINT (map attributeToCST attrs) (map (\bd -> bindingsToCST [bd]) groups) toCST (Y.In attr binding) _ = CO_BELONGS (attributeToCST attr) IN (ST_BINDING (bindingsToCST [binding])) toCST (Y.And conds) _ = case conds of [] -> CO_EMPTY diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} @@ -8,24 +9,25 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Dataize (morph, dataize, dataize', DataizeContext (..)) where +module Dataize (morph, dataize, dataize', DataizeContext (..), execBuildTerm) where import AST -import Builder (contextualize) +import Builder (buildAttributeThrows, buildBytesThrows, buildExpressionThrows) import Control.Exception (throwIO) import Data.List (partition) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Text as T -import Deps (BuildTermFunc, SaveStepFunc, Term (TeAttribute)) +import Deps (BuildTermFunc, BuildTermMethod, SaveStepFunc, Term (TeAttribute, TeExpression)) import Locator (locatedExpression, withLocatedExpression) -import Matcher (substEmpty) +import Matcher (Subst, substEmpty) import Misc import Must (Must (..)) import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite) -import Rule (RuleContext (RuleContext), isNF) +import Rule (RuleContext (RuleContext), matchExpressionWithRule') import Text.Printf (printf) -import Yaml (normalizationRules) +import Yaml (ExtraArgument (..), normalizationRules) +import qualified Yaml as Y type Dataized = (Maybe Bytes, [Rewritten]) @@ -43,127 +45,96 @@ , _saveStep :: SaveStepFunc } -switchContext :: DataizeContext -> RewriteContext -switchContext DataizeContext{..} = - RewriteContext - _locator - _maxDepth - _maxCycles - _depthSensitive - _buildTerm - MtDisabled - Nothing - _saveStep - -maybeBinding :: (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding]) -maybeBinding _ [] = (Nothing, []) -maybeBinding func bds = - let (found, rest) = partition func bds - in case found of - [bd] -> (Just bd, rest) - _ -> (Nothing, bds) - -maybeLambda :: [Binding] -> (Maybe Binding, [Binding]) -maybeLambda = maybeBinding (\case BiLambda _ -> True; _ -> False) - -maybeDelta :: [Binding] -> (Maybe Binding, [Binding]) -maybeDelta = maybeBinding (\case BiDelta _ -> True; _ -> False) - -maybePhi :: [Binding] -> (Maybe Binding, [Binding]) -maybePhi = maybeBinding (\case (BiTau AtPhi _) -> True; _ -> False) - -- Resolve formation for LAMBDA Morphing rule. -- If formation contains ฮป binding, the called atom -- result is returned. -formation :: [Binding] -> DataizeContext -> IO (Maybe (Expression, String)) +formation :: [Binding] -> DataizeContext -> IO (Maybe Expression) formation bds ctx = do let (lambda, bds') = maybeLambda bds case lambda of - Just (BiLambda func) -> do - obj <- atom func (ExFormation bds') ctx - pure (Just (obj, "Mlambda")) + Just (BiLambda func) -> Just <$> atom func (ExFormation bds') ctx _ -> pure Nothing + where + maybeLambda :: [Binding] -> (Maybe Binding, [Binding]) + maybeLambda = maybeBinding (\case BiLambda _ -> True; _ -> False) + maybeBinding :: (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding]) + maybeBinding _ [] = (Nothing, []) + maybeBinding func bds = + let (found, rest) = partition func bds + in case found of + [bd] -> (Just bd, rest) + _ -> (Nothing, bds) -- Resolve dispatch from global object (Q.tau) for PHI Morphing rule. -- Here tau is the name of the attribute which is taken from Q -- and expr is expression which program refers to. -- If Q refers to formation which contains binding with attribute == tau - -- the expression from this binding is returned. -phiDispatch :: T.Text -> Expression -> Maybe (Expression, String) +phiDispatch :: T.Text -> Expression -> Maybe Expression phiDispatch tau expr = case expr of ExFormation bds -> boundExpr bds _ -> Nothing where - boundExpr :: [Binding] -> Maybe (Expression, String) + boundExpr :: [Binding] -> Maybe Expression boundExpr [] = Nothing boundExpr (bd : bds) = case bd of - BiTau (AtLabel attr) expr' -> if attr == tau then Just (expr', "Mphi") else boundExpr bds + BiTau (AtLabel attr) expr' -> if attr == tau then Just expr' else boundExpr bds _ -> boundExpr bds --- Resolve tail PHI and LAMBDA Morphing rules. --- Tail MUST start with dispatch, that's why most of the applications return Nothing -withTail :: Expression -> DataizeContext -> IO (Maybe (Expression, String)) -withTail (ExApplication (ExFormation _) _) _ = pure Nothing -withTail (ExApplication expr tau) ctx = do - tailed <- withTail expr ctx - case tailed of - Just (expr', rule) -> pure (Just (ExApplication expr' tau, rule)) - _ -> pure Nothing -withTail (ExDispatch (ExFormation bds) attr) ctx = do - tailed <- formation bds ctx - case tailed of - Just (obj, rule) -> pure (Just (ExDispatch obj attr, rule)) - _ -> pure Nothing -withTail (ExFormation bds) ctx = formation bds ctx -withTail (ExDispatch ExGlobal (AtLabel label)) DataizeContext{_program = Program expr} = pure (phiDispatch label expr) -withTail (ExDispatch expr attr) ctx = do - tailed <- withTail expr ctx - case tailed of - Just (exp, rule) -> pure (Just (ExDispatch exp attr, rule)) - _ -> pure Nothing -withTail _ _ = pure Nothing - --- The Morphing function M: -> maps objects to --- primitives, possibly modifying the state of evaluation. --- Terminology: --- P(e) - is e Primitive, which is either formation without ฮป binding or termination โŠฅ --- N(e) - normalize e --- NF(e) - is e in normal form (can't be normalized anymore) --- --- PRIM: M(e) -> e if P(e) --- NMZ: M(e1) -> M(e2) if e2 := N(e1) and e1 != e2 --- LAMBDA: M([B1, ฮป -> F, B2] * t) -> M(e2 * t) if e3 := [B1,B2] and e2 := F(e3) --- PHI: M(Q.tau * t) -> M(e * t) if Q -> [B1, tau -> e, B2], t is tail started with dispatch --- M(e) -> โŠฅ otherwise +-- The Morphing function ๐•„ maps objects to primitives. It is driven by the +-- ordered rules from 'morphing.yaml': the first matching rule's 'then' outcome +-- either stops with a primitive ('MoStop') or keeps morphing ('MoMorph'). When +-- the morphed argument is a normalization ('MaNormalize', the 'Mnmz' rule), the +-- rewriter runs and its individual steps are spliced into the chain. morph :: Morphed -> DataizeContext -> IO Morphed -morph (expr@ExTermination, seq) ctx = do - seq' <- leadsTo seq "Mprim" expr ctx -- PRIM - pure (expr, seq') -morph (form@(ExFormation _), seq) ctx = do - resolved <- withTail form ctx - case resolved of - Just (expr, rule) -> do - seq' <- leadsTo seq rule expr ctx -- LAMBDA or PHI - morph (expr, seq') ctx - _ -> do - seq' <- leadsTo seq "Mprim" form ctx -- PRIM - pure (form, seq') morph (expr, seq) ctx@DataizeContext{..} = do - resolved <- withTail expr ctx - case resolved of - Just (expr', rule) -> do - seq' <- leadsTo seq rule expr' ctx + matched <- firstMatch Y.morphingRules + case matched of + Just (rule, subst) -> apply rule.then_ rule.name subst + Nothing -> pure (expr, seq) + where + firstMatch :: [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst)) + firstMatch [] = pure Nothing + firstMatch (rule : rest) = do + substs <- matchExpressionWithRule' expr (asRule rule) (RuleContext (execBuildTerm ctx)) + case substs of + (subst : _) -> pure (Just (rule, subst)) + [] -> firstMatch rest + -- The M/D rules evaluate as 'match โ†’ where โ†’ when', so the rule's guard + -- maps onto the 'having' slot (which runs after 'where'), not 'when' (which + -- 'matchExpressionWithRule'' runs before 'where'). + asRule :: Y.MorphRule -> Y.Rule + asRule rule = Y.Rule rule.name rule.description rule.match ExGlobal Nothing rule.where_ rule.when + apply :: Y.MorphOutcome -> String -> Subst -> IO Morphed + apply (Y.MoStop result) name subst = do + built <- buildExpressionThrows result subst + seq' <- leadsTo seq name built ctx + pure (built, seq') + apply (Y.MoMorph (Y.MaExpr result)) name subst = do + built <- buildExpressionThrows result subst + seq' <- leadsTo seq name built ctx + morph (built, seq') ctx + -- ๐•„(๐’ฉ(e)) delegates to the normalization rewriter and splices its + -- individual steps (alpha, copy, dot, โ€ฆ) into the chain before morphing on. + apply (Y.MoMorph (Y.MaNormalize arg)) _ subst = do + built <- buildExpressionThrows arg subst + prog' <- withLocatedExpression _locator built _program + (rewrittens, _) <- rewrite prog' normalizationRules (switchContext ctx) + let (rw :| rws) = NE.reverse rewrittens + seq' = rw :| rws <> NE.tail seq + expr' <- locatedExpression _locator (fst rw) morph (expr', seq') ctx - _ -> - if isNF expr (RuleContext _buildTerm) - then morph (ExTermination, seq) ctx -- PRIM - else do - prog' <- withLocatedExpression _locator expr _program - (rewrittens, _) <- rewrite prog' normalizationRules (switchContext ctx) -- NMZ - let (rw :| rws) = NE.reverse rewrittens - seq' = rw :| rws <> NE.tail seq - expr' <- locatedExpression _locator (fst rw) - morph (expr', seq') ctx + switchContext :: DataizeContext -> RewriteContext + switchContext DataizeContext{..} = + RewriteContext + _locator + _maxDepth + _maxCycles + _depthSensitive + _buildTerm + MtDisabled + Nothing + _saveStep dataize :: DataizeContext -> IO Dataized dataize ctx@DataizeContext{..} = do @@ -171,33 +142,47 @@ (maybeBytes, seq) <- dataize' (expr, (_program, Nothing) :| []) ctx pure (maybeBytes, reverse seq) --- The goal of 'dataize' function is retrieve bytes from given expression. --- --- DELTA: D(e) -> data if e = [B1, ฮ” -> data, B2] --- BOX: D([B1, ๐œ‘ -> e, B2]) -> D(ะก(e)) if [B1,B2] has no delta/lambda, where ะก(e) - contextualization --- NORM: D(e1) -> D(e2) if e2 := M(e1) and e1 is not primitive --- nothing otherwise +-- The Dataization function ๐”ป retrieves bytes from an expression. It is driven +-- by the ordered rules from 'dataization.yaml': 'delta' yields the asset bytes, +-- 'none' yields nothing, 'box' contextualizes the ฯ†-body and keeps dataizing +-- (its step is labelled by the operation, 'contextualize'), and 'norm' reduces +-- through morphing, splicing the morphing steps into the chain. dataize' :: Dataizable -> DataizeContext -> IO Dataized -dataize' (ExTermination, seq) _ = pure (Nothing, NE.toList seq) -dataize' (form@(ExFormation bds), seq) ctx@DataizeContext{..} = - let _seq = NE.toList seq - in case maybeDelta bds of - (Just (BiDelta bytes), _) -> pure (Just bytes, _seq) - (Just _, _) -> pure (Nothing, _seq) - (Nothing, _) -> case maybePhi bds of - (Just (BiTau AtPhi expr), bds') -> case maybeLambda bds' of - (Just (BiLambda _), _) -> throwIO (userError "The ๐œ‘ and ฮป can't be present in formation at the same time") - (Just _, _) -> pure (Nothing, _seq) - (Nothing, _) -> do - let expr' = contextualize expr form - seq' <- leadsTo seq "contextualize" expr' ctx - dataize' (expr', seq') ctx - (Just _, _) -> pure (Nothing, _seq) - (Nothing, _) -> case maybeLambda bds of - (Just (BiLambda _), _) -> morph (form, seq) ctx >>= (`dataize'` ctx) - (Just _, _) -> pure (Nothing, _seq) - (Nothing, _) -> pure (Nothing, _seq) -dataize' dataizable ctx = morph dataizable ctx >>= (`dataize'` ctx) +dataize' (expr, seq) ctx = do + matched <- firstMatch Y.dataizationRules + case matched of + Just (rule, subst) -> apply rule subst + Nothing -> pure (Nothing, NE.toList seq) + where + firstMatch :: [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst)) + firstMatch [] = pure Nothing + firstMatch (rule : rest) = do + substs <- matchExpressionWithRule' expr (asRule rule) (RuleContext (execBuildTerm ctx)) + case substs of + (subst : _) -> pure (Just (rule, subst)) + [] -> firstMatch rest + asRule :: Y.DataizeRule -> Y.Rule + asRule rule = Y.Rule rule.name rule.description rule.match ExGlobal Nothing rule.where_ rule.when + apply :: Y.DataizeRule -> Subst -> IO Dataized + apply rule subst = case rule.then_ of + Y.DoData bytes -> do + bts <- buildBytesThrows bytes subst + pure (Just bts, NE.toList seq) + Y.DoNothing -> pure (Nothing, NE.toList seq) + Y.DoDataize (Y.DaExpr result) -> do + built <- buildExpressionThrows result subst + seq' <- leadsTo seq (operation rule) built ctx + dataize' (built, seq') ctx + -- ๐”ป(๐•„(e)) delegates to the morphing relation, splicing its steps into + -- the chain before dataizing on. + Y.DoDataize (Y.DaMorph arg) -> do + built <- buildExpressionThrows arg subst + (morphed, seq') <- morph (built, seq) ctx + dataize' (morphed, seq') ctx + operation :: Y.DataizeRule -> String + operation rule = case rule.where_ of + Just (extra : _) -> Y.function extra + _ -> "" leadsTo :: NonEmpty Rewritten -> String -> Expression -> DataizeContext -> IO (NonEmpty Rewritten) leadsTo ((prog, _) :| rest) rule expr DataizeContext{..} = do @@ -248,3 +233,34 @@ else pure (ExDispatch self (AtLabel "y")) _ -> pure ExTermination atom func _ _ = throwIO (userError (printf "Atom '%s' does not exist" (T.unpack func))) + +-- Augment the injected, context-free term builder with the dataization and +-- morphing operations that need the full evaluation context: 'lambda' applies +-- an atom and 'global' dispatches from the universe Q. Every other function is +-- delegated unchanged. +execBuildTerm :: DataizeContext -> BuildTermFunc +execBuildTerm ctx "lambda" = _lambda ctx +execBuildTerm ctx "global" = _global ctx +execBuildTerm ctx func = _buildTerm ctx func + +_lambda :: DataizeContext -> BuildTermMethod +_lambda ctx [ArgExpression expr] subst = do + form <- buildExpressionThrows expr subst + case form of + ExFormation bds -> do + resolved <- formation bds ctx + case resolved of + Just obj -> pure (TeExpression obj) + Nothing -> throwIO (userError "Function lambda() expects a formation with a ฮป binding") + _ -> throwIO (userError "Function lambda() expects a formation") +_lambda _ _ _ = throwIO (userError "Function lambda() requires exactly 1 expression argument") + +_global :: DataizeContext -> BuildTermMethod +_global DataizeContext{_program = Program prog} [ArgAttribute attr] subst = do + attr' <- buildAttributeThrows attr subst + case attr' of + AtLabel label -> case phiDispatch label prog of + Just expr -> pure (TeExpression expr) + Nothing -> throwIO (userError (printf "Universe Q has no attribute '%s'" (show attr'))) + _ -> throwIO (userError "Function global() expects a labelled attribute") +_global _ _ _ = throwIO (userError "Function global() requires exactly 1 attribute argument") diff --git a/src/Encoding.hs b/src/Encoding.hs --- a/src/Encoding.hs +++ b/src/Encoding.hs @@ -31,6 +31,7 @@ toASCII EX_APPLICATION{..} = EX_APPLICATION (toASCII expr) space eol tab (toASCII tau) eol' tab' indent toASCII EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toASCII expr) space eol tab (toASCII taus) eol' tab' indent toASCII EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toASCII expr) space eol tab (toASCII args) eol' tab' indent + toASCII EX_META{meta = META{hd = N, ..}} = EX_META (META EXCL N' rest) toASCII EX_META{..} = EX_META (META EXCL E' (rest meta)) toASCII EX_META_TAIL{..} = EX_META_TAIL (toASCII expr) meta toASCII EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toASCII expr) @@ -98,6 +99,8 @@ toASCII CO_COMPARE{..} = CO_COMPARE (toASCII left) equal (toASCII right) toASCII CO_MATCHES{..} = CO_MATCHES regex (toASCII expr) toASCII CO_PART_OF{..} = CO_PART_OF (toASCII expr) (toASCII binding) + toASCII CO_PRIMITIVE{..} = CO_PRIMITIVE (toASCII expr) belongs + toASCII CO_DISJOINT{..} = CO_DISJOINT (map toASCII attrs) (map toASCII groups) toASCII CO_EMPTY = CO_EMPTY instance ToASCII EXTRA_ARG where diff --git a/src/Functions.hs b/src/Functions.hs --- a/src/Functions.hs +++ b/src/Functions.hs @@ -3,7 +3,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Functions (buildTerm) where +module Functions (buildTerm, execFunctions) where import AST import Builder @@ -23,6 +23,13 @@ import Tau (freshTau) import Text.Printf (printf) import qualified Yaml as Y + +-- Names of build-term functions that need the full evaluation context +-- (program plus atom evaluation) and are therefore provided only by +-- 'Dataize.execBuildTerm', not by 'buildTerm'. They are available while +-- executing dataization and morphing rules, but not rewriting rules. +execFunctions :: [String] +execFunctions = ["lambda", "global"] buildTerm :: BuildTermFunc buildTerm func args subst = do diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -1,6 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} @@ -9,6 +10,8 @@ module LaTeX ( explainRules + , explainMorphRules + , explainDataizeRules , rewrittensToLatex , programToLaTeX , expressionToLaTeX @@ -217,6 +220,7 @@ toLaTeX EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toLaTeX expr) toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toLaTeX expr) toLaTeX EX_META{..} = EX_META (toLaTeX meta) + toLaTeX EX_META_TAIL{..} = EX_META_TAIL (toLaTeX expr) (toLaTeX meta) toLaTeX expr = expr instance ToLaTeX ATTRIBUTE where @@ -260,6 +264,7 @@ instance ToLaTeX META_HEAD where toLaTeX E = E' + toLaTeX N = N' toLaTeX A = TAU' toLaTeX TAU = TAU' toLaTeX B = B' @@ -306,6 +311,8 @@ toLaTeX CO_COMPARE{..} = CO_COMPARE (toLaTeX left) equal (toLaTeX right) toLaTeX CO_MATCHES{..} = CO_MATCHES regex (toLaTeX expr) toLaTeX CO_PART_OF{..} = CO_PART_OF (toLaTeX expr) (toLaTeX binding) + toLaTeX CO_PRIMITIVE{..} = CO_PRIMITIVE (toLaTeX expr) belongs + toLaTeX CO_DISJOINT{..} = CO_DISJOINT (map toLaTeX attrs) (map toLaTeX groups) toLaTeX CO_EMPTY = CO_EMPTY instance ToLaTeX EXTRA_ARG where @@ -319,27 +326,13 @@ explainRule :: Y.Rule -> String explainRule rule = - intercalate - "\n " - [ "\\trrule{" ++ Y.name rule ++ "}" - , braced (renderToLatex (expressionToCST (Y.pattern rule)) defaultLatexContext) - , braced (renderToLatex (expressionToCST (Y.result rule)) defaultLatexContext) - , conditionToLatex (joinedConditions (Y.when rule) (Y.having rule)) - , extraArgumentsToLatex (Y.where_ rule) - ] + trrule + rule.name + (renderToLatex (expressionToCST rule.pattern) defaultLatexContext) + (renderToLatex (expressionToCST rule.result) defaultLatexContext) + (joinedConditions rule.when rule.having) + rule.where_ where - conditionToLatex :: Maybe Y.Condition -> String - conditionToLatex Nothing = "{ }" - conditionToLatex (Just cond) = case conditionToCST cond of - CO_EMPTY -> "{ }" - cond' -> braced ("if $ " <> renderToLatex cond' defaultLatexContext <> " $") - extraArgumentsToLatex :: Maybe [Y.Extra] -> String - extraArgumentsToLatex Nothing = "{ }" - extraArgumentsToLatex (Just extras) = - let extras' = map ((`renderToLatex` defaultLatexContext) . extraToCST) extras - in braced ("where " <> intercalate " and " extras') - braced :: String -> String - braced = printf "{ %s }" -- Join two maybe conditions into single one using Y.And if at least one is just. joinedConditions :: Maybe Y.Condition -> Maybe Y.Condition -> Maybe Y.Condition joinedConditions Nothing Nothing = Nothing @@ -347,11 +340,86 @@ joinedConditions Nothing second@(Just _) = second joinedConditions (Just first) (Just second) = Just (Y.And [first, second]) +explainMorphRule :: Y.MorphRule -> String +explainMorphRule rule = + trrule + rule.name + (morph (renderToLatex (expressionToCST rule.match) defaultLatexContext)) + (morphOutcome rule.then_) + rule.when + rule.where_ + where + morphOutcome :: Y.MorphOutcome -> String + morphOutcome (Y.MoMorph (Y.MaExpr expr)) = morph (renderToLatex (expressionToCST expr) defaultLatexContext) + morphOutcome (Y.MoMorph (Y.MaNormalize expr)) = morph (normalize (renderToLatex (expressionToCST expr) defaultLatexContext)) + morphOutcome (Y.MoStop expr) = renderToLatex (expressionToCST expr) defaultLatexContext + +explainDataizeRule :: Y.DataizeRule -> String +explainDataizeRule rule = + trrule + rule.name + (dataize (renderToLatex (expressionToCST rule.match) defaultLatexContext)) + (dataizeOutcome rule.then_) + rule.when + rule.where_ + where + dataizeOutcome :: Y.DataizeOutcome -> String + dataizeOutcome (Y.DoDataize (Y.DaExpr expr)) = dataize (renderToLatex (expressionToCST expr) defaultLatexContext) + dataizeOutcome (Y.DoDataize (Y.DaMorph expr)) = dataize (morph (renderToLatex (expressionToCST expr) defaultLatexContext)) + dataizeOutcome (Y.DoData bytes) = T.unpack (render (toCST' bytes :: BYTES)) + dataizeOutcome Y.DoNothing = "\\varnothing" + +-- Render a single rule row through the shared \trrule macro: name, left-hand +-- side, right-hand side, the optional 'if' condition and 'where' extras. +trrule :: String -> String -> String -> Maybe Y.Condition -> Maybe [Y.Extra] -> String +trrule name lhs rhs cond extras = + intercalate + "\n " + [ "\\trrule{" ++ name ++ "}" + , braced lhs + , braced rhs + , conditionToLatex cond + , extraArgumentsToLatex extras + ] + +morph :: String -> String +morph inner = "\\mathbb{M}( " ++ inner ++ " )" + +dataize :: String -> String +dataize inner = "\\mathbb{D}( " ++ inner ++ " )" + +normalize :: String -> String +normalize inner = "\\mathcal{N}( " ++ inner ++ " )" + +braced :: String -> String +braced = printf "{ %s }" + +conditionToLatex :: Maybe Y.Condition -> String +conditionToLatex Nothing = "{ }" +conditionToLatex (Just cond) = case conditionToCST cond of + CO_EMPTY -> "{ }" + cond' -> braced ("if $ " <> renderToLatex cond' defaultLatexContext <> " $") + +extraArgumentsToLatex :: Maybe [Y.Extra] -> String +extraArgumentsToLatex Nothing = "{ }" +extraArgumentsToLatex (Just extras) = + let extras' = map ((`renderToLatex` defaultLatexContext) . extraToCST) extras + in braced ("where " <> intercalate " and " extras') + explainRules :: [Y.Rule] -> String -explainRules rules = +explainRules = explainTabular . map explainRule + +explainMorphRules :: [Y.MorphRule] -> String +explainMorphRules = explainTabular . map explainMorphRule + +explainDataizeRules :: [Y.DataizeRule] -> String +explainDataizeRules = explainTabular . map explainDataizeRule + +explainTabular :: [String] -> String +explainTabular rows = intercalate "\n" [ "\\begin{tabular}{rl}" - , intercalate "\n" (map explainRule rules) + , intercalate "\n" rows , "\\end{tabular}" ] diff --git a/src/Lining.hs b/src/Lining.hs --- a/src/Lining.hs +++ b/src/Lining.hs @@ -31,6 +31,7 @@ toSingleLine EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toSingleLine expr) space NO_EOL TAB' (toSingleLine args) NO_EOL TAB' indent toSingleLine EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSingleLine expr) toSingleLine EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSingleLine expr) + toSingleLine EX_META_TAIL{..} = EX_META_TAIL (toSingleLine expr) meta toSingleLine expr = expr instance ToSingleLine APP_BINDING where @@ -81,6 +82,8 @@ toSingleLine CO_COMPARE{..} = CO_COMPARE (toSingleLine left) equal (toSingleLine right) toSingleLine CO_MATCHES{..} = CO_MATCHES regex (toSingleLine expr) toSingleLine CO_PART_OF{..} = CO_PART_OF (toSingleLine expr) (toSingleLine binding) + toSingleLine CO_PRIMITIVE{..} = CO_PRIMITIVE (toSingleLine expr) belongs + toSingleLine CO_DISJOINT{..} = CO_DISJOINT attrs (map toSingleLine groups) toSingleLine CO_EMPTY = CO_EMPTY instance ToSingleLine EXTRA_ARG where diff --git a/src/Matcher.hs b/src/Matcher.hs --- a/src/Matcher.hs +++ b/src/Matcher.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE LambdaCase #-} - -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT @@ -36,6 +34,10 @@ newtype Subst = Subst (Map Text MetaValue) deriving (Eq, Show) +-- A way to match a pattern expression against a target expression, yielding +-- the substitutions under which they agree. +type MatchExpressionFunc = Expression -> Expression -> [Subst] + -- Empty substitution substEmpty :: Subst substEmpty = Subst Map.empty @@ -109,19 +111,12 @@ (substs, tails) <- tailExpressionsReversed ptn' expr Just (substs, TaDispatch attr : tails) ExApplication expr tau -> do - (substs, tails@(t : _)) <- tailExpressionsReversed ptn' expr - if not (null tails) && isDispatch t - then Just (substs, TaApplication tau : tails) - else Nothing - where - isDispatch :: Tail -> Bool - isDispatch = \case - TaDispatch _ -> True - TaApplication _ -> False + (substs, tails) <- tailExpressionsReversed ptn' expr + Just (substs, TaApplication tau : tails) _ -> Just ([], []) substs -> Just (substs, []) -matchExpression' :: Expression -> Expression -> [Subst] +matchExpression' :: MatchExpressionFunc matchExpression' (ExMeta meta) tgt = [substSingle meta (MvExpression tgt)] matchExpression' ExThis ExThis = [substEmpty] matchExpression' ExGlobal ExGlobal = [substEmpty] @@ -146,7 +141,7 @@ matchBindingExpression _ _ = [] -- Match expression with deep nested expression(s) matching -matchExpressionDeep :: Expression -> Expression -> [Subst] +matchExpressionDeep :: MatchExpressionFunc matchExpressionDeep ptn tgt = let matched = matchExpression' ptn tgt deep = case tgt of @@ -156,7 +151,7 @@ _ -> [] in matched ++ deep -matchExpression :: Expression -> Expression -> [Subst] +matchExpression :: MatchExpressionFunc matchExpression = matchExpressionDeep matchProgram :: Expression -> Program -> [Subst] diff --git a/src/Parser.hs b/src/Parser.hs --- a/src/Parser.hs +++ b/src/Parser.hs @@ -385,6 +385,7 @@ , number , lexeme (DataString . strToBts <$> quotedStr) , try (ExMeta <$> meta' 'e' "๐‘’") + , try (ExMeta <$> meta' 'n' "๐‘›") , ExDispatch ExThis <$> attribute ] "expression head" diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -112,6 +112,8 @@ instance Render META_HEAD where render E = "๐‘’" render E' = "e" + render N = "๐‘›" + render N' = "n" render A = "a" render TAU = "๐œ" render TAU' = "\\tau" @@ -250,6 +252,13 @@ render CO_COMPARE{..} = render left <> " " <> render equal <> " " <> render right render CO_MATCHES{..} = "matches( " <> T.pack regex <> ", " <> render expr <> " )" render CO_PART_OF{..} = "part-of( " <> render expr <> ", " <> render binding <> " )" + render CO_PRIMITIVE{..} = render expr <> " " <> render belongs <> " \\mathcal{P}" + render CO_DISJOINT{..} = + "[ " + <> T.intercalate ", " (map render attrs) + <> " ] \\cap ( " + <> T.intercalate " \\cup " (map render groups) + <> " ) = \\emptyset" render CO_EMPTY = "" renderFunc :: Render a => Text -> a -> Text diff --git a/src/Rewriter.hs b/src/Rewriter.hs --- a/src/Rewriter.hs +++ b/src/Rewriter.hs @@ -2,6 +2,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} @@ -145,9 +146,9 @@ where _rewrite :: RewriteState -> Int -> IO RewriteState _rewrite (_rewrittens@((program, _) :| _), _unique, _) _count = - let ruleName = Y.name rule - ptn = Y.pattern rule - res = Y.result rule + let ruleName = rule.name + ptn = rule.pattern + res = rule.result in if _count - 1 == _maxDepth then do logDebug (printf "Max amount of rewriting cycles (%d) for rule '%s' has been reached, rewriting is stopped" _maxDepth ruleName) @@ -191,7 +192,7 @@ leadsTo :: Program -> NonEmpty Rewritten leadsTo _prog = let (program, _) :| rest = _rewrittens - in (_prog, Nothing) :| (program, Just (Y.name rule)) : rest + in (_prog, Nothing) :| (program, Just rule.name) : rest -- Rewrite program by provided locator from RewriteContext rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO Rewrittens diff --git a/src/Rule.hs b/src/Rule.hs --- a/src/Rule.hs +++ b/src/Rule.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} @@ -5,7 +6,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Rule (RuleContext (..), isNF, matchProgramWithRule, matchExpressionWithRule, meetCondition) where +module Rule (RuleContext (..), isNF, matchProgramWithRule, matchExpressionWithRule, matchExpressionWithRule', meetCondition) where import AST import Builder @@ -18,8 +19,10 @@ import Control.Monad (when) import qualified Data.ByteString.Char8 as B import Data.Foldable (foldlM) +import Data.List (nub) import qualified Data.Map.Strict as M import Data.Maybe (catMaybes) +import qualified Data.Text as T import Deps (BuildTermFunc, Term (..)) import GHC.IO (unsafePerformIO) import Logger (logDebug) @@ -207,6 +210,43 @@ partOf expr (BiTau _ expr' : rest) = expr == expr' || partOf expr rest partOf expr (_ : rest) = partOf expr rest +-- A primitive is the termination โŠฅ or a formation without a ฮป binding; +-- expression metas are resolved through the substitution first. +_primitive :: Expression -> Subst -> RuleContext -> IO [Subst] +_primitive (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of + Just (MvExpression expr) -> _primitive expr (Subst mp) ctx + _ -> pure [] +_primitive expr subst _ = pure [subst | primitive expr] + where + primitive :: Expression -> Bool + primitive ExTermination = True + primitive (ExFormation bds) = not (any lambda bds) + primitive _ = False + lambda :: Binding -> Bool + lambda (BiLambda _) = True + lambda (BiMetaLambda _) = True + lambda _ = False + +-- Hold if none of the given attributes is present in the union of the +-- bindings captured by the given binding metas. +_disjoint :: [Attribute] -> [Binding] -> Subst -> RuleContext -> IO [Subst] +_disjoint attrs bindings subst _ = + case (traverse (`buildAttribute` subst) attrs, traverse (`buildBinding` subst) bindings) of + (Right attrs', Right bdss) -> + let bds = concat bdss + in pure [subst | not (any (`presentIn` bds) attrs')] + (_, _) -> pure [] + where + presentIn :: Attribute -> [Binding] -> Bool + presentIn attr = any (presentInBinding attr) + presentInBinding :: Attribute -> Binding -> Bool + presentInBinding attr (BiTau battr _) = attr == battr + presentInBinding attr (BiVoid battr) = attr == battr + presentInBinding AtLambda (BiLambda _) = True + presentInBinding AtLambda (BiMetaLambda _) = True + presentInBinding AtDelta (BiDelta _) = True + presentInBinding _ _ = False + meetCondition' :: Y.Condition -> Subst -> RuleContext -> IO [Subst] meetCondition' (Y.Or conds) = _or conds meetCondition' (Y.And conds) = _and conds @@ -218,6 +258,8 @@ meetCondition' (Y.XiFree expr) = _xiFree expr meetCondition' (Y.Matches pat expr) = _matches pat expr meetCondition' (Y.PartOf expr bd) = _partOf expr bd +meetCondition' (Y.Primitive expr) = _primitive expr +meetCondition' (Y.Disjoint attrs bds) = _disjoint attrs bds -- For each substitution check if it meetCondition to given condition -- If substitution does not meet the condition - it's thrown out @@ -283,32 +325,69 @@ logDebug "Extra substitutions have been built" pure (catMaybes res) +-- Collect the names of NF-constrained expression meta-variables ('๐‘›'/'!n') +-- used in a pattern. Their names are 'n'-prefixed and live in their own +-- key-space, so a pattern may freely mix plain '๐‘’' captures with '๐‘›' ones. +nfMetaNames :: Expression -> [T.Text] +nfMetaNames = nub . go + where + go :: Expression -> [T.Text] + go (ExMeta mt) + | T.isPrefixOf "n" mt = [mt] + | otherwise = [] + go (ExFormation bds) = concatMap goBinding bds + go (ExApplication e bd) = go e ++ goBinding bd + go (ExDispatch e _) = go e + go (ExMetaTail e _) = go e + go (ExPhiMeet _ _ e) = go e + go (ExPhiAgain _ _ e) = go e + go _ = [] + goBinding :: Binding -> [T.Text] + goBinding (BiTau _ e) = go e + goBinding _ = [] + matchExpressionWithRule :: Expression -> Y.Rule -> RuleContext -> IO [Subst] -matchExpressionWithRule expr rule ctx = - let ptn = Y.pattern rule - matched = matchExpression ptn expr - name = Y.name rule +matchExpressionWithRule = matchExpressionBy matchExpression + +-- Like 'matchExpressionWithRule' but matches the pattern against the whole +-- expression only (no deep, sub-expression matching). Used by the dataization +-- and morphing driver, where a rule applies to the entire configuration rather +-- than to nested redexes. +matchExpressionWithRule' :: Expression -> Y.Rule -> RuleContext -> IO [Subst] +matchExpressionWithRule' = matchExpressionBy matchExpression' + +matchExpressionBy :: MatchExpressionFunc -> Expression -> Y.Rule -> RuleContext -> IO [Subst] +matchExpressionBy matcher expr rule ctx = + let ptn = rule.pattern + matched = matcher ptn expr + name = rule.name in if null matched then do logDebug (printf "Pattern from rule '%s' was not matched:\n%s" name (printExpression' ptn logPrintConfig)) pure [] else do - when' <- meetMaybeCondition (Y.when rule) matched ctx - if null when' + inNf <- foldlM (\substs nm -> meetCondition (Y.NF (ExMeta nm)) substs ctx) matched (nfMetaNames ptn) + if null inNf then do - logDebug "The 'when' condition wasn't met" + logDebug "An NF-constrained '๐‘›' meta-variable is not in normal form" pure [] else do - logDebug (printf "Rule %s" name) - extended <- extraSubstitutions when' (Y.where_ rule) ctx - if null extended + when' <- meetMaybeCondition rule.when inNf ctx + if null when' then do - logDebug "Substitution is empty after enxtending, maybe some metas are duplicated" + logDebug "The 'when' condition wasn't met" pure [] else do - met <- meetMaybeCondition (Y.having rule) extended ctx - when (null met) (logDebug "The 'having' condition wan't met") - pure met + logDebug (printf "Rule %s" name) + extended <- extraSubstitutions when' rule.where_ ctx + if null extended + then do + logDebug "Substitution is empty after extending, maybe some metas are duplicated" + pure [] + else do + met <- meetMaybeCondition rule.having extended ctx + when (null met) (logDebug "The 'having' condition wasn't met") + pure met matchProgramWithRule :: Program -> Y.Rule -> RuleContext -> IO [Subst] matchProgramWithRule (Program expr) = matchExpressionWithRule expr diff --git a/src/Sugar.hs b/src/Sugar.hs --- a/src/Sugar.hs +++ b/src/Sugar.hs @@ -110,6 +110,7 @@ rhos toSalty EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSalty expr) toSalty EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSalty expr) + toSalty EX_META_TAIL{..} = EX_META_TAIL (toSalty expr) meta toSalty expr = expr saltifyPrimitive :: EXPRESSION -> EXPRESSION -> EXPRESSION -> TAB -> [Binding] -> EXPRESSION @@ -195,6 +196,8 @@ toSalty CO_COMPARE{..} = CO_COMPARE (toSalty left) equal (toSalty right) toSalty CO_MATCHES{..} = CO_MATCHES regex (toSalty expr) toSalty CO_PART_OF{..} = CO_PART_OF (toSalty expr) (toSalty binding) + toSalty CO_PRIMITIVE{..} = CO_PRIMITIVE (toSalty expr) belongs + toSalty CO_DISJOINT{..} = CO_DISJOINT attrs (map toSalty groups) toSalty CO_EMPTY = CO_EMPTY instance ToSalty EXTRA_ARG where diff --git a/src/Yaml.hs b/src/Yaml.hs --- a/src/Yaml.hs +++ b/src/Yaml.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TemplateHaskell #-} @@ -13,7 +14,7 @@ import Control.Applicative (asum) import Data.Aeson import qualified Data.ByteString as BS -import Data.FileEmbed (embedDir) +import Data.FileEmbed (embedDir, embedFile) import Data.Text (unpack) import Data.Yaml (Parser) import qualified Data.Yaml as Yaml @@ -77,7 +78,7 @@ withObject "Condition" ( \v -> do - validateYamlObject v ["and", "or", "not", "alpha", "nf", "xi-free", "eq", "in", "matches", "part-of"] + validateYamlObject v ["and", "or", "not", "alpha", "nf", "xi-free", "eq", "in", "matches", "part-of", "primitive", "disjoint"] asum [ And <$> v .: "and" , Or <$> v .: "or" @@ -85,7 +86,13 @@ , Alpha <$> v .: "alpha" , NF <$> v .: "nf" , XiFree <$> v .: "xi-free" + , Primitive <$> v .: "primitive" , do + vals <- v .: "disjoint" + case vals of + [attrs_, bds_] -> Disjoint <$> parseJSON attrs_ <*> parseJSON bds_ + _ -> fail "'disjoint' expects exactly two arguments" + , do vals <- v .: "eq" case vals of [left_, right_] -> Eq <$> parseJSON left_ <*> parseJSON right_ @@ -164,6 +171,8 @@ | XiFree Expression | Matches String Expression | PartOf Expression Binding + | Primitive Expression + | Disjoint [Attribute] [Binding] deriving (Eq, Generic, Show) data ExtraArgument @@ -193,7 +202,7 @@ normalizationRules :: [Rule] {-# NOINLINE normalizationRules #-} -normalizationRules = map decodeRule $(embedDir "resources") +normalizationRules = map decodeRule $(embedDir "resources/normalize") where decodeRule :: (FilePath, BS.ByteString) -> Rule decodeRule (path, bs) = @@ -203,3 +212,124 @@ yamlRule :: FilePath -> IO Rule yamlRule = Yaml.decodeFileThrow + +-- The right-hand side of a morphing reduction ๐•„(match) โŸฟ then. +-- A mapping ('{ morph: arg }') keeps reducing under ๐•„; a bare expression +-- (including โŠฅ) is the terminal primitive result. +data MorphOutcome + = MoMorph MorphArg + | MoStop Expression + deriving (Eq, Generic, Show) + +-- The argument of a morphing continuation: either a plain expression ('๐•„(e)') +-- or the normalization of one ('๐•„(๐’ฉ(e))', written '{ normalize: e }'). +data MorphArg + = MaExpr Expression + | MaNormalize Expression + deriving (Eq, Generic, Show) + +-- The right-hand side of a dataization reduction ๐”ป(match) โŸฟ then. +-- A mapping ('{ dataize: arg }') keeps reducing under ๐”ป; a bare bytes scalar +-- yields data; the 'nothing' keyword marks the function as undefined. +data DataizeOutcome + = DoDataize DataizeArg + | DoData Bytes + | DoNothing + deriving (Eq, Generic, Show) + +-- The argument of a dataization continuation: either a plain expression +-- ('๐”ป(e)') or the morphing of one ('๐”ป(๐•„(e))', written '{ morph: e }'). +data DataizeArg + = DaExpr Expression + | DaMorph Expression + deriving (Eq, Generic, Show) + +-- One ordered morphing rule: match the expression, build extra metas in +-- 'where', filter by 'when', then reduce per 'then'. +data MorphRule = MorphRule + { name :: String + , description :: Maybe String + , match :: Expression + , where_ :: Maybe [Extra] + , when :: Maybe Condition + , then_ :: MorphOutcome + } + deriving (Generic, Show) + +-- One ordered dataization rule, structured like 'MorphRule' but reducing +-- under ๐”ป and able to terminate with bytes or 'nothing'. +data DataizeRule = DataizeRule + { name :: String + , description :: Maybe String + , match :: Expression + , where_ :: Maybe [Extra] + , when :: Maybe Condition + , then_ :: DataizeOutcome + } + deriving (Generic, Show) + +instance FromJSON MorphOutcome where + parseJSON (Object o) = do + validateYamlObject o ["morph"] + MoMorph <$> o .: "morph" + parseJSON v = MoStop <$> parseJSON v + +instance FromJSON MorphArg where + parseJSON (Object o) = do + validateYamlObject o ["normalize"] + MaNormalize <$> o .: "normalize" + parseJSON v = MaExpr <$> parseJSON v + +instance FromJSON DataizeOutcome where + parseJSON (Object o) = do + validateYamlObject o ["dataize"] + DoDataize <$> o .: "dataize" + parseJSON (String "nothing") = pure DoNothing + parseJSON v = DoData <$> parseJSON v + +instance FromJSON DataizeArg where + parseJSON (Object o) = do + validateYamlObject o ["morph"] + DaMorph <$> o .: "morph" + parseJSON v = DaExpr <$> parseJSON v + +instance FromJSON MorphRule where + parseJSON = + withObject + "MorphRule" + ( \o -> + MorphRule + <$> o .: "name" + <*> o .:? "description" + <*> o .: "match" + <*> o .:? "where" + <*> o .:? "when" + <*> o .: "then" + ) + +instance FromJSON DataizeRule where + parseJSON = + withObject + "DataizeRule" + ( \o -> + DataizeRule + <$> o .: "name" + <*> o .:? "description" + <*> o .: "match" + <*> o .:? "where" + <*> o .:? "when" + <*> o .: "then" + ) + +decodeRules :: (FromJSON a) => FilePath -> BS.ByteString -> [a] +decodeRules path bs = case Yaml.decodeEither' bs of + Right rs -> rs + Left err -> error $ "YAML parse error in " ++ path ++ ": " ++ show err + +morphingRules :: [MorphRule] +{-# NOINLINE morphingRules #-} +morphingRules = decodeRules "resources/morphing.yaml" $(embedFile "resources/morphing.yaml") + +dataizationRules :: [DataizeRule] +{-# NOINLINE dataizationRules #-} +dataizationRules = decodeRules "resources/dataization.yaml" $(embedFile "resources/dataization.yaml") diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -359,8 +359,14 @@ it "rewrites with single rule" $ withStdin "{T(x -> Q.y)}" $ - testCLISucceeded ["rewrite", "--rule=resources/dc.yaml"] ["ฮฆ โ†ฆ โŠฅ"] + testCLISucceeded ["rewrite", "--rule=resources/normalize/dc.yaml"] ["ฮฆ โ†ฆ โŠฅ"] + it "fails when a rewriting rule uses a dataization-only function" $ + withStdin "{โŸฆโŸง}" $ + testCLIFailed + ["rewrite", rule "lambda-in-rewrite.yaml"] + ["Function 'lambda' in rule 'uses-lambda' is available only for dataization and morphing, not for rewriting"] + it "normalizes with --normalize flag" $ testCLISucceeded ["rewrite", "--normalize", resource "normalize.phi", "--margin=25"] @@ -917,13 +923,13 @@ describe "explain" $ do it "explains single rule" $ testCLISucceeded - ["explain", "--rule=resources/copy.yaml"] + ["explain", "--rule=resources/normalize/copy.yaml"] [ unlines [ "\\begin{tabular}{rl}" , "\\trrule{copy}" - , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }" - , " { [[ B_1, \\tau -> e, B_2 ]] }" - , " { if $ \\xifree{ e } \\;\\text{and}\\; \\isnormal{ e } $ }" + , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> n ) }" + , " { [[ B_1, \\tau -> n, B_2 ]] }" + , " { if $ \\xifree{ n } $ }" , " { }" , "\\end{tabular}" ] @@ -931,7 +937,7 @@ it "explains multiple rules" $ testCLISucceeded - ["explain", "--rule=resources/copy.yaml", "--rule=resources/alpha.yaml"] + ["explain", "--rule=resources/normalize/copy.yaml", "--rule=resources/normalize/alpha.yaml"] ["\\begin{tabular}{rl}", "\\trrule{copy}", "\\trrule{alpha}"] it "explains normalization rules" $ @@ -945,9 +951,9 @@ , " { if $ \\indexof{ \\tau_2 } = \\vert \\overline{ B_1 } \\vert $ }" , " { }" , "\\trrule{copy}" - , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }" - , " { [[ B_1, \\tau -> e, B_2 ]] }" - , " { if $ \\xifree{ e } \\;\\text{and}\\; \\isnormal{ e } $ }" + , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> n ) }" + , " { [[ B_1, \\tau -> n, B_2 ]] }" + , " { if $ \\xifree{ n } $ }" , " { }" , "\\trrule{dc}" , " { T ( \\tau -> e ) }" @@ -960,10 +966,10 @@ , " { }" , " { }" , "\\trrule{dot}" - , " { [[ B_1, \\tau -> e_1, B_2 ]] . \\tau }" - , " { e_2 ( ^ -> [[ B_1, \\tau -> e_1, B_2 ]] ) }" - , " { if $ \\isnormal{ e_1 } $ }" - , " { where $ e_2 \\coloneqq \\ctx{ e_1 }{ [[ B_1, \\tau -> e_1, B_2 ]] } $ }" + , " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }" + , " { e ( ^ -> [[ B_1, \\tau -> n, B_2 ]] ) }" + , " { }" + , " { where $ e \\coloneqq \\ctx{ n }{ [[ B_1, \\tau -> n, B_2 ]] } $ }" , "\\trrule{miss}" , " { [[ B ]] ( \\tau -> e ) }" , " { T }" @@ -998,10 +1004,78 @@ ] ] + it "explains morphing rules" $ + testCLISucceeded + ["explain", "--morph"] + [ unlines + [ "\\begin{tabular}{rl}" + , "\\trrule{Mprim}" + , " { \\mathbb{M}( e ) }" + , " { e }" + , " { if $ e \\in \\mathcal{P} $ }" + , " { }" + , "\\trrule{Mnmz}" + , " { \\mathbb{M}( e ) }" + , " { \\mathbb{M}( \\mathcal{N}( e ) ) }" + , " { if $ not( \\isnormal{ e } ) $ }" + , " { }" + , "\\trrule{Mlambda}" + , " { \\mathbb{M}( [[ B_1, L> F, B_2 ]] * t ) }" + , " { \\mathbb{M}( e * t ) }" + , " { }" + , " { where $ e \\coloneqq lambda( [[ B_1, L> F, B_2 ]] ) $ }" + , "\\trrule{Mphi}" + , " { \\mathbb{M}( Q . \\tau * t ) }" + , " { \\mathbb{M}( e * t ) }" + , " { }" + , " { where $ e \\coloneqq global( \\tau ) $ }" + , "\\trrule{Mstuck}" + , " { \\mathbb{M}( e ) }" + , " { T }" + , " { }" + , " { }" + , "\\end{tabular}" + ] + ] + + it "explains dataization rules" $ + testCLISucceeded + ["explain", "--dataize"] + [ unlines + [ "\\begin{tabular}{rl}" + , "\\trrule{delta}" + , " { \\mathbb{D}( [[ B_1, D> ฮด, B_2 ]] ) }" + , " { ฮด }" + , " { }" + , " { }" + , "\\trrule{box}" + , " { \\mathbb{D}( [[ B_1, @ -> e, B_2 ]] ) }" + , " { \\mathbb{D}( e_1 ) }" + , " { if $ [ ฮ”, L ] \\cap ( B_1 \\cup B_2 ) = \\emptyset $ }" + , " { where $ e_1 \\coloneqq \\ctx{ e }{ [[ B_1, @ -> e, B_2 ]] } $ }" + , "\\trrule{norm}" + , " { \\mathbb{D}( e ) }" + , " { \\mathbb{D}( \\mathbb{M}( e ) ) }" + , " { if $ e \\notin \\mathcal{P} $ }" + , " { }" + , "\\trrule{none}" + , " { \\mathbb{D}( e ) }" + , " { \\varnothing }" + , " { }" + , " { }" + , "\\end{tabular}" + ] + ] + it "fails with no rules specified" $ testCLIFailed ["explain"] - ["Either --rule or --normalize must be specified"] + ["Either --rule, --normalize, --morph or --dataize must be specified"] + + it "fails when more than one rule set is specified" $ + testCLIFailed + ["explain", "--morph", "--dataize"] + ["Only one of --rule, --normalize, --morph or --dataize can be specified"] it "writes to target file" $ bracket diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com @@ -7,13 +8,16 @@ import AST import Control.Monad +import Data.List (nub) import Data.List.NonEmpty (NonEmpty (..)) -import Dataize (DataizeContext (DataizeContext), dataize, dataize', morph) -import Deps (dontSaveStep) +import Dataize (DataizeContext (DataizeContext), dataize, dataize', execBuildTerm, morph) +import Deps (Term (TeExpression), dontSaveStep) import Functions (buildTerm) +import Matcher (substEmpty) import Parser (parseExpressionThrows, parseProgramThrows) import Rewriter (Rewritten) import Test.Hspec +import Yaml qualified defaultDataizeContext :: Expression -> Program -> DataizeContext defaultDataizeContext loc prog = DataizeContext loc prog 25 25 False buildTerm dontSaveStep @@ -104,6 +108,82 @@ , Just (BtOne "01") ) ] + + describe "execBuildTerm" $ + it "resolves global dispatch from the universe Q" $ do + prog <- parseProgramThrows "Q -> [[ x -> [[ D> 42- ]] ]]" + expected <- parseExpressionThrows "[[ D> 42- ]]" + term <- execBuildTerm (defaultDataizeContext ExGlobal prog) "global" [Yaml.ArgAttribute (AtLabel "x")] substEmpty + case term of + TeExpression actual -> actual `shouldBe` expected + _ -> expectationFailure "global() did not return an expression" + + describe "labels every step with a defined rule or operation" $ do + let funcs = maybe [] (map Yaml.function) + allowed = + map (.name) Yaml.morphingRules + ++ map (.name) Yaml.dataizationRules + ++ map (.name) Yaml.normalizationRules + ++ concatMap (funcs . (.where_)) Yaml.morphingRules + ++ concatMap (funcs . (.where_)) Yaml.dataizationRules + it "uses no step label without a defining rule or operation" $ do + prog <- + parseProgramThrows + ( unlines + [ "Q -> [[" + , " bytes(data) -> [[ @ -> $.data ]]," + , " number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]]," + , " @ -> 5.plus(6)" + , "]]" + ] + ) + loc <- parseExpressionThrows "Q" + (_, chain) <- dataize (defaultDataizeContext loc prog) + let orphans = nub [label | (_, Just label) <- chain, label `notElem` allowed] + unless + (null orphans) + (expectationFailure ("Dataization emitted step labels with no defining rule or operation: " ++ show orphans)) + + describe "preserves the reduction label sequence" $ do + let labelsOf loc src = do + prog <- parseProgramThrows src + loc' <- parseExpressionThrows loc + (_, chain) <- dataize (defaultDataizeContext loc' prog) + pure [label | (_, Just label) <- chain] + it "dataizes 5.plus(6) through the expected rules" $ do + labels <- + labelsOf + "Q" + "Q -> [[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" + labels + `shouldBe` [ "contextualize" + , "Mphi" + , "alpha" + , "copy" + , "dot" + , "copy" + , "alpha" + , "copy" + , "Mlambda" + , "Mphi" + , "alpha" + , "copy" + , "Mprim" + , "contextualize" + , "dot" + , "Mphi" + , "alpha" + , "copy" + , "copy" + , "Mprim" + , "contextualize" + , "dot" + , "copy" + , "Mprim" + ] + it "dataizes a located reference through the expected rules" $ do + labels <- labelsOf "Q.foo.bar" "Q -> [[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]" + labels `shouldBe` ["contextualize", "Mphi", "Mprim"] testDataize [ diff --git a/test/MatcherSpec.hs b/test/MatcherSpec.hs --- a/test/MatcherSpec.hs +++ b/test/MatcherSpec.hs @@ -409,6 +409,12 @@ , substs [[("t", MvTail [TaDispatch (AtLabel "org"), TaApplication (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]] ) , + ( "Q.x * !t => Q.x(y -> [[]]) => [(!t >> [(y -> [[]])])]" + , ExMetaTail (ExDispatch ExGlobal (AtLabel "x")) "t" + , ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") (ExFormation [BiVoid AtRho])) + , substs [[("t", MvTail [TaApplication (BiTau (AtLabel "y") (ExFormation [BiVoid AtRho]))])]] + ) + , ( "Q.!a * !t => Q.org.eolang(x -> [[]]) => [(!a >> org, !t >> [ .eolang, ( x -> [[ ]] ) ])]" , ExMetaTail (ExDispatch ExGlobal (AtMeta "a")) "t" , ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho])) diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs --- a/test/ParserSpec.hs +++ b/test/ParserSpec.hs @@ -469,6 +469,11 @@ , ("๐‘’0", Just (ExMeta "e0")) , ("!e.x", Just (ExDispatch (ExMeta "e") (AtLabel "x"))) , ("!e(Q)", Just (ExApplication (ExMeta "e") (BiTau (AtAlpha 0) ExGlobal))) + , ("!n", Just (ExMeta "n")) + , ("!n1", Just (ExMeta "n1")) + , ("๐‘›", Just (ExMeta "n")) + , ("๐‘›1", Just (ExMeta "n1")) + , ("๐‘›.x", Just (ExDispatch (ExMeta "n") (AtLabel "x"))) ] describe "parse meta tails" $ diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs --- a/test/RewriterSpec.hs +++ b/test/RewriterSpec.hs @@ -93,7 +93,7 @@ Just basic' -> mapM ( \name -> do - yaml <- ensuredFile ("resources" replaceExtension name ".yaml") + yaml <- ensuredFile ("resources/normalize" replaceExtension name ".yaml") Y.yamlRule yaml ) basic'