phino 0.0.80 → 0.0.81
raw patch · 47 files changed
+950/−761 lines, 47 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- AST: AtAlpha :: Int -> Attribute
- AST: BiMetaLambda :: Text -> Binding
- AST: ExGlobal :: Expression
- AST: ExThis :: Expression
- Yaml: Alpha :: Attribute -> Condition
+ AST: AlMeta :: Text -> Alpha
+ AST: Alpha :: Int -> Alpha
+ AST: ArAlpha :: Alpha -> Expression -> Argument
+ AST: ArTau :: Attribute -> Expression -> Argument
+ AST: ExRoot :: Expression
+ AST: ExXi :: Expression
+ AST: FnMeta :: Text -> Function
+ AST: Function :: Text -> Function
+ AST: data Alpha
+ AST: data Argument
+ AST: data Function
+ AST: instance GHC.Classes.Eq AST.Alpha
+ AST: instance GHC.Classes.Eq AST.Argument
+ AST: instance GHC.Classes.Eq AST.Function
+ AST: instance GHC.Classes.Ord AST.Alpha
+ AST: instance GHC.Classes.Ord AST.Argument
+ AST: instance GHC.Classes.Ord AST.Function
+ AST: instance GHC.Generics.Generic AST.Alpha
+ AST: instance GHC.Generics.Generic AST.Argument
+ AST: instance GHC.Generics.Generic AST.Function
+ AST: instance GHC.Show.Show AST.Alpha
+ AST: instance GHC.Show.Show AST.Argument
+ AST: instance GHC.Show.Show AST.Function
+ AST: primitive :: Expression -> Bool
+ CST: ETA :: META_HEAD
+ CST: ETA' :: META_HEAD
+ CST: H :: META_HEAD
+ CST: P :: META_HEAD
+ CST: P' :: META_HEAD
+ CST: alphaToCST :: Alpha -> ATTRIBUTE
+ CST: instance CST.ToCST AST.Alpha CST.ATTRIBUTE
+ CST: instance CST.ToCST AST.Argument CST.PAIR
+ CST: instance CST.ToCST [AST.Argument] CST.BINDING
+ CST: instance CST.ToCST [AST.Argument] CST.BINDINGS
+ Matcher: MvAlpha :: Alpha -> MetaValue
+ Matcher: matchAlpha :: Alpha -> Alpha -> [Subst]
+ Matcher: matchArgument :: Argument -> Argument -> [Subst]
+ Matcher: matchArgumentExpression :: Argument -> Expression -> [Subst]
+ Matcher: matchFunction :: Function -> Function -> [Subst]
+ Parser: [_alpha] :: PhiParser -> Parser Alpha
+ Parser: parseAlpha :: String -> Either String Alpha
+ Printer: printAlpha :: Alpha -> String
+ Yaml: DaNormalize :: Expression -> DataizeArg
+ Yaml: instance Data.Aeson.Types.FromJSON.FromJSON AST.Alpha
- AST: BiLambda :: Text -> Binding
+ AST: BiLambda :: Function -> Binding
- AST: ExApplication :: Expression -> Binding -> Expression
+ AST: ExApplication :: Expression -> Argument -> Expression
- CST: EX_NUMBER :: Either Int Double -> TAB -> [Binding] -> EXPRESSION
+ CST: EX_NUMBER :: Either Int Double -> TAB -> [Argument] -> EXPRESSION
- CST: EX_STRING :: String -> TAB -> [Binding] -> EXPRESSION
+ CST: EX_STRING :: String -> TAB -> [Argument] -> EXPRESSION
- CST: [rhos] :: EXPRESSION -> [Binding]
+ CST: [rhos] :: EXPRESSION -> [Argument]
- Matcher: TaApplication :: Binding -> Tail
+ Matcher: TaApplication :: Argument -> Tail
- Parser: PhiParser :: Parser Attribute -> Parser Binding -> Parser Expression -> Parser String -> PhiParser
+ Parser: PhiParser :: Parser Attribute -> Parser Alpha -> Parser Binding -> Parser Expression -> Parser String -> PhiParser
- Yaml: Index :: Attribute -> Number
+ Yaml: Index :: Alpha -> Number
Files
- README.md +52/−39
- benchmark/Main.hs +2/−2
- phino.cabal +1/−1
- resources/dataization.yaml +11/−9
- resources/morphing.yaml +17/−26
- resources/normalize/alpha.yaml +2/−2
- resources/normalize/dca.yaml +6/−0
- resources/normalize/miss.yaml +4/−7
- src/AST.hs +52/−23
- src/Builder.hs +29/−15
- src/CLI/Helpers.hs +1/−1
- src/CLI/Runners.hs +2/−2
- src/CLI/Validators.hs +1/−1
- src/CST.hs +47/−22
- src/Canonizer.hs +13/−5
- src/Condition.hs +2/−7
- src/Dataize.hs +45/−28
- src/Encoding.hs +2/−0
- src/Functions.hs +5/−6
- src/LaTeX.hs +10/−3
- src/Locator.hs +2/−2
- src/Matcher.hs +36/−13
- src/Misc.hs +25/−28
- src/Parser.hs +45/−29
- src/Printer.hs +14/−1
- src/Render.hs +5/−0
- src/Replacer.hs +14/−7
- src/Rule.hs +15/−31
- src/Sugar.hs +1/−1
- src/Tau.hs +5/−1
- src/XMIR.hs +41/−38
- src/Yaml.hs +15/−9
- test/ASTSpec.hs +49/−43
- test/BuilderSpec.hs +23/−23
- test/CLISpec.hs +23/−24
- test/CSTSpec.hs +1/−1
- test/ConditionSpec.hs +5/−10
- test/DataizeSpec.hs +29/−27
- test/FunctionsSpec.hs +3/−3
- test/MatcherSpec.hs +104/−73
- test/MiscSpec.hs +4/−4
- test/ParserSpec.hs +72/−72
- test/PrinterSpec.hs +22/−22
- test/ReplacerSpec.hs +81/−88
- test/RewriterSpec.hs +2/−2
- test/RuleSpec.hs +8/−8
- test/TauSpec.hs +2/−2
README.md view
@@ -34,7 +34,7 @@ ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.79+cabal install --overwrite-policy=always phino-0.0.80 phino --version ``` @@ -214,9 +214,9 @@ $ phino explain --normalize \begin{tabular}{rl} \trrule{alpha}- { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_2 -> e ) }+ { [[ B_1, \tau_1 -> ?, B_2 ]] ( \eta -> e ) } { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_1 -> e ) }- { if $ \indexof{ \tau_2 } = \vert B_1 \vert $ }+ { if $ \indexof{ \eta } = \vert \overline{ B_1 } \vert $ } { } \trrule{dc} { T ( \tau -> e ) }@@ -237,13 +237,13 @@ ```bash $ phino explain --morph \begin{tabular}{rl}-\trrule{Mprim}+\trrule{prim} { \mathbb{M}( e ) } { e } { if $ e \in \mathcal{P} $ } { } ...-\trrule{Mphi}+\trrule{root} { \mathbb{M}( Q . \tau * t ) } { \mathbb{M}( e * t ) } { }@@ -288,7 +288,6 @@ = and: [Condition] # logical AND | or: [Condition] # logical OR | not: Condition # logical NOT- | alpha: Attribute' # check if given attribute is alpha | eq: # compare two comparable objects - Comparable - Comparable@@ -319,7 +318,7 @@ Number: # comparable number = Integer # just regular integer- | index: Attribute' # calculate index of alpha attribute+ | index: Alpha' # calculate index of alpha | length: BiMeta' # calculate length of bindings by given meta binding Extension: # substitutions extension used to introduce new meta variables@@ -378,6 +377,7 @@ This is the list of supported meta variables: * `!a` || `𝜏` - attribute+* `!h` || `𝜂` - alpha, the positional index of an application argument * `!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@@ -419,55 +419,55 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1- total: 1299342.512 μs- avg: 129934.251 μs- min: 118253.218 μs- max: 162332.377 μs- std dev: 16619.006 μs+ total: 1400685.745 μs+ avg: 140068.575 μs+ min: 128878.179 μs+ max: 170778.015 μs+ std dev: 15086.312 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1- total: 7609340.593 μs- avg: 760934.059 μs- min: 697264.466 μs- max: 801903.360 μs- std dev: 31387.398 μs+ total: 7628269.229 μs+ avg: 762826.923 μs+ min: 700461.528 μs+ max: 895566.916 μs+ std dev: 53443.050 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1- total: 394738.996 μs- avg: 39473.900 μs- min: 38668.484 μs- max: 40389.889 μs- std dev: 473.832 μs+ total: 389007.790 μs+ avg: 38900.779 μs+ min: 37763.081 μs+ max: 40258.745 μs+ std dev: 794.301 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1- total: 4562591.028 μs- avg: 456259.103 μs- min: 451902.950 μs- max: 462770.604 μs- std dev: 3059.588 μs+ total: 3943382.302 μs+ avg: 394338.230 μs+ min: 375291.020 μs+ max: 416271.808 μs+ std dev: 12394.321 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1- total: 4529234.270 μs- avg: 452923.427 μs- min: 418300.611 μs- max: 476533.304 μs- std dev: 23032.941 μs+ total: 3855869.876 μs+ avg: 385586.988 μs+ min: 365284.728 μs+ max: 405130.834 μs+ std dev: 11941.433 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1- total: 13656171.599 μs- avg: 1365617.160 μs- min: 1311639.249 μs- max: 1429575.023 μs- std dev: 37618.391 μs+ total: 13541528.033 μs+ avg: 1354152.803 μs+ min: 1307453.767 μs+ max: 1399468.749 μs+ std dev: 27649.598 μs ``` The results were calculated in [this GHA job][benchmark-gha]-on 2026-06-11 at 11:02,+on 2026-06-18 at 23:15, on Linux with 4 CPUs. <!-- benchmark_end -->@@ -489,6 +489,19 @@ make coverage ``` +To build a `phino` executable into the root of the repository, run:++```bash+make phino+```++This produces an executable `phino` (or `phino.exe` on Windows) in the+project root, which you can run directly for quick local testing:++```bash+./phino --version+```+ You will need [GHC ≥ 9.6.7][GHC] and [Cabal ≥ 3.0 (recommended)][cabal] or [Stack ≥ 3.0][stack] installed. @@ -503,4 +516,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/27342074018+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/27794897832
benchmark/Main.hs view
@@ -3,7 +3,7 @@ module Main where -import AST (Expression (ExGlobal))+import AST (Expression (ExRoot)) import Control.Exception (evaluate) import Control.Monad (replicateM, replicateM_) import Data.Time.Clock@@ -33,7 +33,7 @@ rewriteCtx :: RewriteContext rewriteCtx = RewriteContext- ExGlobal+ ExRoot 100 100 False
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.80+version: 0.0.81 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
resources/dataization.yaml view
@@ -1,7 +1,8 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----# Dataization 𝔻 — applied top-to-bottom, first matching clause wins.+# Dataization 𝔻 — applied top-to-bottom, first matching clause wins. The input+# is always a normal form: a non-NF expression matches no clause. - name: delta description: '𝔻(⟦𝐵1, Δ ⤍ δ, 𝐵2⟧) ⟿ δ'@@ -9,7 +10,7 @@ then: δ - name: box- description: '𝔻(⟦𝐵1, φ ↦ e, 𝐵2⟧) ⟿ 𝔻(𝒞(e)) if [Δ, λ] ∩ (𝐵1 ∪ 𝐵2) = ∅'+ description: '𝔻(⟦𝐵1, φ ↦ e, 𝐵2⟧) ⟿ 𝔻(𝒩(𝒞(e))) if [Δ, λ] ∩ (𝐵1 ∪ 𝐵2) = ∅' match: ⟦𝐵1, φ ↦ 𝑒, 𝐵2⟧ where: - meta: 𝑒1@@ -22,19 +23,20 @@ - [Δ, λ] - [𝐵1, 𝐵2] then:- dataize: 𝑒1+ dataize:+ normalize: 𝑒1 - name: norm- description: '𝔻(e) ⟿ 𝔻(𝕄(e)) if e ∉ 𝒫'- match: 𝑒+ description: '𝔻(n) ⟿ 𝔻(𝕄(n)) if n ∉ 𝒫'+ match: 𝑛 when: not:- primitive: 𝑒+ primitive: 𝑛 then: dataize:- morph: 𝑒+ morph: 𝑛 - name: none- description: '𝔻(e) ⟿ nothing otherwise'- match: 𝑒+ description: '𝔻(n) ⟿ nothing otherwise'+ match: 𝑛 then: nothing
resources/morphing.yaml view
@@ -1,27 +1,16 @@ # 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: 𝑒+# Morphing 𝕄 — applied top-to-bottom, first matching clause wins. The input+# is always a normal form: a non-NF expression matches no clause. -- name: Mnmz- description: '𝕄(e) ⟿ 𝕄(𝒩(e)) if e ∉ NF'- match: 𝑒- when:- not:- nf: 𝑒- then:- morph:- normalize: 𝑒+- name: prim+ description: '𝕄(p) ⟿ p'+ match: 𝑝+ then: 𝑝 -- name: Mlambda- description: '𝕄(⟦𝐵1, λ ⤍ F, 𝐵2⟧ * t) ⟿ 𝕄(F(⟦𝐵1, 𝐵2⟧) * t)'+- name: lambda+ description: '𝕄(⟦𝐵1, λ ⤍ F, 𝐵2⟧ * t) ⟿ 𝕄(𝒩(F(⟦𝐵1, 𝐵2⟧) * t))' match: '⟦𝐵1, λ ⤍ !F, 𝐵2⟧ * !t' where: - meta: 𝑒@@ -29,10 +18,11 @@ args: - '⟦𝐵1, λ ⤍ !F, 𝐵2⟧' then:- morph: '𝑒 * !t'+ morph:+ normalize: '𝑒 * !t' -- name: Mphi- description: '𝕄(Φ.τ * t) ⟿ 𝕄(e * t) if Φ ↦ ⟦𝐵1, τ ↦ e, 𝐵2⟧'+- name: root+ description: '𝕄(Φ.τ * t) ⟿ 𝕄(𝒩(e * t)) if Φ ↦ ⟦𝐵1, τ ↦ e, 𝐵2⟧' match: 'Φ.𝜏 * !t' where: - meta: 𝑒@@ -40,9 +30,10 @@ args: - 𝜏 then:- morph: '𝑒 * !t'+ morph:+ normalize: '𝑒 * !t' -- name: Mstuck- description: '𝕄(e) ⟿ ⊥ otherwise'- match: 𝑒+- name: stuck+ description: '𝕄(n) ⟿ ⊥ otherwise'+ match: 𝑛 then: ⊥
resources/normalize/alpha.yaml view
@@ -2,9 +2,9 @@ # SPDX-License-Identifier: MIT --- name: alpha-pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏2 ↦ 𝑒)+pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜂 ↦ 𝑒) result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒) when: eq:- - index: 𝜏2+ - index: 𝜂 - domain: 𝐵1
+ resources/normalize/dca.yaml view
@@ -0,0 +1,6 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+name: dca+pattern: ⊥(𝜂 ↦ 𝑒)+result: ⊥
resources/normalize/miss.yaml view
@@ -5,10 +5,7 @@ pattern: ⟦𝐵⟧(𝜏 ↦ 𝑒) result: ⊥ when:- and:- - not:- in:- - 𝜏- - 𝐵- - not:- alpha: 𝜏+ not:+ in:+ - 𝜏+ - 𝐵
src/AST.hs view
@@ -18,10 +18,10 @@ data Expression = ExFormation [Binding]- | ExThis- | ExGlobal+ | ExXi+ | ExRoot | ExTermination- | ExApplication Expression Binding+ | ExApplication Expression Argument | ExDispatch Expression Attribute | ExMeta Text | ExMetaTail Expression Text@@ -29,13 +29,22 @@ | ExPhiAgain (Maybe String) Int Expression deriving (Eq, Ord, Show, Generic) +data Argument+ = ArTau Attribute Expression+ | ArAlpha Alpha Expression+ deriving (Eq, Ord, Show, Generic)++data Alpha+ = Alpha Int+ | AlMeta Text+ deriving (Eq, Ord, Generic)+ data Binding = BiTau Attribute Expression- | BiDelta Bytes | BiVoid Attribute- | BiLambda Text+ | BiDelta Bytes+ | BiLambda Function | BiMeta Text- | BiMetaLambda Text deriving (Eq, Ord, Show, Generic) data Bytes@@ -47,7 +56,6 @@ data Attribute = AtLabel Text- | AtAlpha Int | AtPhi | AtRho | AtLambda@@ -55,15 +63,23 @@ | AtMeta Text deriving (Eq, Generic, Ord) +data Function+ = Function Text+ | FnMeta Text+ deriving (Eq, Generic, Show, Ord)+ instance Show Attribute where show (AtLabel label) = T.unpack label- show (AtAlpha idx) = 'α' : show idx show AtRho = "ρ" show AtPhi = "φ" show AtDelta = "Δ" show AtLambda = "λ" show (AtMeta meta) = '!' : T.unpack meta +instance Show Alpha where+ show (Alpha idx) = 'α' : show idx+ show (AlMeta meta) = '!' : T.unpack meta+ -- A cheap, fixed-size digest of an expression, used for fast (dirty) equality -- checks during loop detection. Equal expressions always produce the same -- digest, but distinct expressions may collide, so a positive digest match@@ -74,60 +90,72 @@ fnvPrime, fnvOffset :: Int fnvPrime = 1099511628211 fnvOffset = 14695981039- -- FNV-1a style mixing step (Int multiplication wraps silently). step :: Int -> Int -> Int step h x = (h `xor` x) * fnvPrime- hashText :: Int -> Text -> Int hashText = T.foldl' (\h c -> step h (fromEnum c))- hashString :: Int -> String -> Int hashString = foldl' (\h c -> step h (fromEnum c))- hashMaybeString :: Int -> Maybe String -> Int hashMaybeString h Nothing = step h 0 hashMaybeString h (Just s) = hashString (step h 1) s- goExpr :: Int -> Expression -> Int goExpr h = \case ExFormation bds -> foldl' goBinding (step h 1) bds- ExThis -> step h 2- ExGlobal -> step h 3+ ExXi -> step h 2+ ExRoot -> step h 3 ExTermination -> step h 4- ExApplication ex bd -> goBinding (goExpr (step h 5) ex) bd+ ExApplication ex arg -> goArgument (goExpr (step h 5) ex) arg ExDispatch ex at -> goAttribute (goExpr (step h 6) ex) at ExMeta t -> hashText (step h 7) t ExMetaTail ex t -> hashText (goExpr (step h 8) ex) t ExPhiMeet ms i ex -> goExpr (hashMaybeString (step (step h 9) i) ms) ex ExPhiAgain ms i ex -> goExpr (hashMaybeString (step (step h 10) i) ms) ex- goBinding :: Int -> Binding -> Int goBinding h = \case BiTau at ex -> goExpr (goAttribute (step h 11) at) ex BiDelta bts -> goBytes (step h 12) bts BiVoid at -> goAttribute (step h 13) at- BiLambda t -> hashText (step h 14) t+ BiLambda fn -> goFunction (step h 14) fn BiMeta t -> hashText (step h 15) t- BiMetaLambda t -> hashText (step h 16) t- goBytes :: Int -> Bytes -> Int goBytes h = \case BtEmpty -> step h 17 BtOne s -> hashString (step h 18) s BtMany ss -> foldl' hashString (step h 19) ss BtMeta t -> hashText (step h 20) t- goAttribute :: Int -> Attribute -> Int goAttribute h = \case AtLabel t -> hashText (step h 21) t- AtAlpha i -> step (step h 22) i AtPhi -> step h 23 AtRho -> step h 24 AtLambda -> step h 25 AtDelta -> step h 26 AtMeta t -> hashText (step h 27) t+ goArgument :: Int -> Argument -> Int+ goArgument h = \case+ ArTau at ex -> goExpr (goAttribute (step h 22) at) ex+ ArAlpha al ex -> goExpr (goAlpha (step h 30) al) ex+ goAlpha :: Int -> Alpha -> Int+ goAlpha h = \case+ Alpha idx -> step (step h 31) idx+ AlMeta t -> hashText (step h 28) t+ goFunction :: Int -> Function -> Int+ goFunction h = \case+ Function t -> hashText (step h 16) t+ FnMeta t -> hashText (step h 29) t +-- A primitive is the termination ⊥ or a formation without a λ binding.+primitive :: Expression -> Bool+primitive ExTermination = True+primitive (ExFormation bds) = not (any lambda bds)+ where+ lambda :: Binding -> Bool+ lambda (BiLambda _) = True+ lambda _ = False+primitive _ = False+ countNodes :: Expression -> Int countNodes (ExFormation bds) = 1 + sum (map nodesInBinding bds) + length bds where@@ -135,7 +163,8 @@ nodesInBinding (BiTau _ expr) = countNodes expr + 2 nodesInBinding (BiMeta _) = 1 nodesInBinding _ = 3-countNodes (ExApplication expr (BiTau _ expr')) = 4 + countNodes expr + countNodes expr'+countNodes (ExApplication expr (ArTau _ expr')) = 4 + countNodes expr + countNodes expr'+countNodes (ExApplication expr (ArAlpha _ expr')) = 4 + countNodes expr + countNodes expr' countNodes (ExDispatch expr' _) = 2 + countNodes expr' countNodes (ExMetaTail expr _) = 2 + countNodes expr countNodes (ExPhiMeet _ _ expr) = countNodes expr
src/Builder.hs view
@@ -24,7 +24,6 @@ import AST import Control.Exception (Exception, throwIO)-import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.Map.Strict as Map import Data.Text (Text) import qualified Data.Text as T@@ -52,13 +51,16 @@ show CouldNotBuildBytes{..} = printf "Couldn't build bytes '%s', %s" (printBytes _bts) _msg contextualize :: Expression -> Expression -> Expression-contextualize ExGlobal _ = ExGlobal-contextualize ExThis ex = ex+contextualize ExRoot _ = ExRoot+contextualize ExXi ex = ex contextualize ExTermination _ = ExTermination contextualize (ExFormation bds) _ = ExFormation bds contextualize (ExDispatch ex at) context = ExDispatch (contextualize ex context) at-contextualize (ExApplication ex (BiTau at bexpr)) context =- ExApplication (contextualize ex context) (BiTau at (contextualize bexpr context))+contextualize (ExApplication ex arg) context =+ ExApplication (contextualize ex context) (contextualizeArg arg)+ where+ contextualizeArg (ArTau at bexpr) = ArTau at (contextualize bexpr context)+ contextualizeArg (ArAlpha al bexpr) = ArAlpha al (contextualize bexpr context) contextualize ex _ = ex buildAttribute :: Attribute -> Subst -> Built Attribute@@ -67,6 +69,12 @@ _ -> Left (metaMsg meta) buildAttribute attr _ = Right attr +buildAlpha :: Alpha -> Subst -> Built Alpha+buildAlpha (AlMeta meta) (Subst mp) = case Map.lookup meta mp of+ Just (MvAlpha alpha) -> Right alpha+ _ -> Left (metaMsg meta)+buildAlpha a _ = Right a+ buildBytes :: Bytes -> Subst -> Built Bytes buildBytes (BtMeta meta) (Subst mp) = case Map.lookup meta mp of Just (MvBytes bytes) -> Right bytes@@ -90,11 +98,21 @@ buildBinding (BiDelta bytes) subst = do bts <- buildBytes bytes subst Right [BiDelta bts]-buildBinding (BiMetaLambda meta) (Subst mp) = case Map.lookup meta mp of- Just (MvFunction func) -> Right [BiLambda func]+buildBinding (BiLambda (FnMeta meta)) (Subst mp) = case Map.lookup meta mp of+ Just (MvFunction func) -> Right [BiLambda (Function func)] _ -> Left (metaMsg meta) buildBinding binding _ = Right [binding] +buildArgument :: Argument -> Subst -> Built Argument+buildArgument (ArTau attr expr) subst = do+ attribute <- buildAttribute attr subst+ expression <- buildExpression expr subst+ Right (ArTau attribute expression)+buildArgument (ArAlpha alpha expr) subst = do+ alpha' <- buildAlpha alpha subst+ expression <- buildExpression expr subst+ Right (ArAlpha alpha' expression)+ -- Build bindings that may contain meta binding (BiMeta) buildBindings :: [Binding] -> Subst -> Built [Binding] buildBindings [] _ = Right []@@ -106,7 +124,7 @@ buildExpressionWithTails :: Expression -> [Tail] -> Subst -> Expression buildExpressionWithTails expr [] _ = expr buildExpressionWithTails ex (tl : rest) subst = case tl of- TaApplication taus -> buildExpressionWithTails (ExApplication ex taus) rest subst+ TaApplication arg -> buildExpressionWithTails (ExApplication ex arg) rest subst TaDispatch at -> buildExpressionWithTails (ExDispatch ex at) rest subst -- Build meta expression with given substitution@@ -115,14 +133,10 @@ dispatched <- buildExpression ex subst at' <- buildAttribute at subst Right (ExDispatch dispatched at')-buildExpression (ExApplication expr (BiTau battr bexpr)) subst = do+buildExpression (ExApplication expr arg) subst = do applied <- buildExpression expr subst- bd :| _ <- nonEmpty' =<< buildBinding (BiTau battr bexpr) subst- Right (ExApplication applied bd)- where- nonEmpty' :: [a] -> Built (NonEmpty a)- nonEmpty' [] = Left ""- nonEmpty' (x : xs) = Right (x :| xs)+ arg' <- buildArgument arg subst+ Right (ExApplication applied arg') buildExpression (ExFormation bds) subst = do bds' <- buildBindings bds subst >>= uniqueBindings Right (ExFormation bds')
src/CLI/Helpers.hs view
@@ -64,7 +64,7 @@ printRewrittens :: PrintProgramContext -> Rewrittens' -> IO String printRewrittens ctx@PrintProgCtx{..} rewrittens@(chain, _) | _outputFormat == LATEX && _sequence = rewrittensToLatex rewrittens (printCtxToLatexCtx ctx)- | _focus == ExGlobal = mapM (printProgram ctx . fst) chain <&> intercalate "\n"+ | _focus == ExRoot = mapM (printProgram ctx . fst) chain <&> intercalate "\n" | otherwise = mapM (\(prog, _) -> locatedExpression _focus prog >>= printExpression ctx) chain <&> intercalate "\n" printExpression :: PrintProgramContext -> Expression -> IO String
src/CLI/Runners.hs view
@@ -224,7 +224,7 @@ False (justMeetPopularity Nothing) (justMeetLength Nothing)- ExGlobal+ ExRoot Nothing Nothing Nothing@@ -246,4 +246,4 @@ else putStrLn (P.printSubsts' substs (_sugarType, UNICODE, _flat, defaultMargin)) where rule :: Expression -> Maybe Y.Condition -> Y.Rule- rule ptn cnd = Y.Rule "custom" Nothing ptn ExGlobal cnd Nothing Nothing+ rule ptn cnd = Y.Rule "custom" Nothing ptn ExRoot cnd Nothing Nothing
src/CLI/Validators.hs view
@@ -25,7 +25,7 @@ asDispatch expr = asDispatch' expr where asDispatch' :: Expression -> IO Expression- asDispatch' ex@ExGlobal = pure ex+ asDispatch' ex@ExRoot = pure ex asDispatch' disp@(ExDispatch ex _) = asDispatch' ex >> pure disp asDispatch' _ = invalidCLIArguments
src/CST.hs view
@@ -11,7 +11,6 @@ module CST where import AST-import Data.Maybe (isJust) import qualified Data.Text as T import Misc import qualified Yaml as Y@@ -84,9 +83,14 @@ | N' -- n | K -- 𝑘 | K' -- k+ | P -- 𝑝+ | P' -- p | A -- a | TAU -- 𝜏 | TAU' -- \tau+ | ETA -- 𝜂+ | ETA' -- \eta+ | H -- h | B -- 𝐵 | B' -- B | D -- δ@@ -164,8 +168,8 @@ | EX_APPLICATION {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, tau :: APP_BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1) | EX_APPLICATION_TAUS {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, taus :: BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1)(a2 -> e2)(...) | EX_APPLICATION_EXPRS {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, args :: APP_ARG, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(e1, e2, ...)- | EX_STRING {str :: String, tab :: TAB, rhos :: [Binding]}- | EX_NUMBER {num :: Either Int Double, tab :: TAB, rhos :: [Binding]}+ | EX_STRING {str :: String, tab :: TAB, rhos :: [Argument]}+ | EX_NUMBER {num :: Either Int Double, tab :: TAB, rhos :: [Argument]} | EX_META {meta :: META} | EX_META_TAIL {expr :: EXPRESSION, meta :: META} | EX_PHI_MEET {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION}@@ -263,6 +267,9 @@ attributeToCST :: Attribute -> ATTRIBUTE attributeToCST = toCST' +alphaToCST :: Alpha -> ATTRIBUTE+alphaToCST = toCST'+ bindingsToCST :: [Binding] -> BINDING bindingsToCST = toCST' @@ -286,12 +293,13 @@ -- The first character of an expression meta name encodes its kind: -- 'n'-prefixed names are normal-form-constrained '𝑛' metas, 'k'-prefixed--- names are absolute-constrained '𝑘' metas, everything else is an--- ordinary '𝑒' meta.+-- names are absolute-constrained '𝑘' metas, 'p'-prefixed names are+-- primitive-constrained '𝑝' metas, everything else is an ordinary '𝑒' meta. exMetaHead :: T.Text -> META_HEAD exMetaHead mt | T.isPrefixOf "n" mt = N | T.isPrefixOf "k" mt = K+ | T.isPrefixOf "p" mt = P | otherwise = E -- This class is used to convert AST to CST@@ -304,8 +312,8 @@ toCST (Program expr) ctx = PR_SWEET LCB (toCST expr ctx) RCB NO_SPACE instance ToCST Expression EXPRESSION where- toCST ExGlobal _ = EX_GLOBAL Φ- toCST ExThis _ = EX_XI XI+ toCST ExRoot _ = EX_GLOBAL Φ+ toCST ExXi _ = EX_XI XI 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@@ -335,7 +343,7 @@ -- their byte form `Φ.number(Φ.bytes(⟦ Δ ⤍ … ⟧))` by falling through to the -- generic application clause below. toCST (DataNumber bts) (tabs, _) | sweetNumber bts = EX_NUMBER (btsToNum bts) (TAB tabs) []- toCST (ExDispatch ExThis attr) ctx = EX_ATTR (toCST attr ctx)+ toCST (ExDispatch ExXi attr) ctx = EX_ATTR (toCST attr ctx) toCST (ExDispatch expr attr) ctx = EX_DISPATCH (toCST expr ctx) NO_SPACE (toCST attr ctx) -- Since we convert AST to CST in sweet notation, here we're trying to get rid of unnecessary rho bindings -- in primitives (more details here: https://github.com/objectionary/phino/issues/451)@@ -353,7 +361,7 @@ next = tabs + 1 (ts', rs) = withoutRhosInPrimitives ex ts obj = ExApplication ex (head' ts')- in if length ts' == 1 && isJust (matchDataObject obj) && sweetCollapsible obj+ in if length ts' == 1 && dataPrimitive obj && sweetCollapsible obj then applicationToPrimitive obj tabs rs else if null exs@@ -380,9 +388,13 @@ where primitives :: [T.Text] primitives = ["number", "string"]- withoutRhosInPrimitives :: Expression -> [Binding] -> ([Binding], [Binding])+ dataPrimitive :: Expression -> Bool+ dataPrimitive obj' = case matchDataObject obj' of+ Just (label, _) -> label `elem` primitives+ Nothing -> False+ withoutRhosInPrimitives :: Expression -> [Argument] -> ([Argument], [Argument]) withoutRhosInPrimitives _ [] = ([], [])- withoutRhosInPrimitives obj@(BaseObject label) bds@(rho@(BiTau AtRho _) : rest)+ withoutRhosInPrimitives obj@(BaseObject label) bds@(rho@(ArTau AtRho _) : rest) | label `elem` primitives = let (bds', rhos) = withoutRhosInPrimitives obj rest in (bds', rho : rhos)@@ -393,7 +405,7 @@ in (bd : bds', rhos) | otherwise = (bds, []) withoutRhosInPrimitives _ bds = (bds, [])- applicationToPrimitive :: Expression -> Int -> [Binding] -> EXPRESSION+ applicationToPrimitive :: Expression -> Int -> [Argument] -> EXPRESSION applicationToPrimitive (DataNumber bts) tabs = EX_NUMBER (btsToNum bts) (TAB tabs) applicationToPrimitive (DataString bts) tabs = EX_STRING (btsToStr bts) (TAB tabs) applicationToPrimitive _ _ = error "applicationToPrimitive expects DataNumber or DataString"@@ -403,24 +415,24 @@ -- 2. list of tau bindings which are applied to start expression -- 3. list of expressions which are applied to start expression with default -- alpha attributes (~0 -> e1, ~1 -> e2, ...)- complexApplication :: Expression -> (Expression, [Binding], [Expression])+ complexApplication :: Expression -> (Expression, [Argument], [Expression]) complexApplication expr = let (expr', taus', exprs') = complexApplication' expr in (expr', reverse taus', reverse exprs') where- complexApplication' :: Expression -> (Expression, [Binding], [Expression])+ complexApplication' :: Expression -> (Expression, [Argument], [Expression]) complexApplication' (ExApplication (ExApplication expr tau) tau') = let (before, taus, exprs) = complexApplication' (ExApplication expr tau) taus' = tau' : taus in if null exprs then (before, taus', []) else case tau' of- BiTau (AtAlpha idx) expr' ->+ ArAlpha (Alpha idx) expr' -> if idx == length exprs then (before, taus', expr' : exprs) else (before, taus', []) _ -> (before, taus', [])- complexApplication' (ExApplication expr (BiTau (AtAlpha 0) expr')) = (expr, [BiTau (AtAlpha 0) expr'], [expr'])+ complexApplication' (ExApplication expr (ArAlpha (Alpha 0) expr')) = (expr, [ArAlpha (Alpha 0) expr'], [expr']) complexApplication' (ExApplication expr tau) = (expr, [tau], []) complexApplication' expr = (expr, [], []) -- This head' works the same as head from Prelude but doesn't throw an error@@ -473,10 +485,22 @@ toCST (BiTau attr exp) ctx = PA_TAU (toCST attr ctx) ARROW (toCST exp ctx) toCST (BiVoid attr) ctx = PA_VOID (toCST attr ctx) ARROW EMPTY toCST (BiDelta bts) ctx = PA_DELTA (toCST bts ctx)- toCST (BiLambda func) _ = PA_LAMBDA func- toCST (BiMetaLambda mt) _ = PA_META_LAMBDA (META EXCL F (metaTail mt))+ toCST (BiLambda (Function name)) _ = PA_LAMBDA name+ toCST (BiLambda (FnMeta mt)) _ = PA_META_LAMBDA (META EXCL F (metaTail mt)) toCST (BiMeta mt) _ = error $ "BiMeta binding " ++ T.unpack mt ++ " cannot be converted to PAIR" +instance ToCST Argument PAIR where+ toCST (ArTau attr exp) ctx = toCST (BiTau attr exp) ctx+ toCST (ArAlpha alpha exp) ctx = PA_TAU (toCST alpha ctx) ARROW (toCST exp ctx)++instance ToCST [Argument] BINDING where+ toCST [] (tabs, _) = BI_EMPTY (TAB tabs)+ toCST (arg : args) ctx@(tabs, _) = BI_PAIR (toCST arg ctx) (toCST args ctx) (TAB tabs)++instance ToCST [Argument] BINDINGS where+ toCST [] (tabs, _) = BDS_EMPTY (TAB tabs)+ toCST (arg : args) ctx@(tabs, eol) = BDS_PAIR eol (TAB tabs) (toCST arg ctx) (toCST args ctx)+ instance ToCST Binding APP_BINDING where toCST bd@(BiTau _ _) ctx = APP_BINDING (toCST bd ctx :: PAIR) toCST bd _ = error $ "Only BiTau binding can be converted to APP_BINDING, got: " ++ show bd@@ -489,17 +513,19 @@ instance ToCST Attribute ATTRIBUTE where toCST (AtLabel label) _ = AT_LABEL label- toCST (AtAlpha idx) _ = AT_ALPHA ALPHA idx toCST AtPhi _ = AT_PHI PHI toCST AtRho _ = AT_RHO RHO toCST AtDelta _ = AT_DELTA DELTA toCST AtLambda _ = AT_LAMBDA LAMBDA toCST (AtMeta mt) _ = AT_META (META NO_EXCL TAU (metaTail mt)) +instance ToCST Alpha ATTRIBUTE where+ toCST (Alpha idx) _ = AT_ALPHA ALPHA idx+ toCST (AlMeta mt) _ = AT_META (META NO_EXCL ETA (metaTail mt))+ instance ToCST Y.Condition CONDITION where 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.Not (Y.Absolute expr)) _ = CO_ABSOLUTE (expressionToCST expr) NOT_IN@@ -512,7 +538,6 @@ toCST (Y.Or conds) _ = case conds of [] -> CO_EMPTY _ -> CO_LOGIC (map toCST' conds) OR- toCST (Y.Alpha attr) _ = CO_BELONGS (attributeToCST attr) IN (ST_ATTRIBUTES [attributeToCST (AtAlpha 0), attributeToCST (AtAlpha 1), AT_REST DOTS]) toCST (Y.NF expr) _ = CO_NF (expressionToCST expr) toCST (Y.Not cond) _ = CO_NOT (conditionToCST cond) toCST (Y.Eq left right) _ = CO_COMPARE (comparableToCST left) EQUAL (comparableToCST right)@@ -525,7 +550,7 @@ toCST (Y.CmpNum num) _ = CMP_NUM (numberToCST num) instance ToCST Y.Number NUMBER where- toCST (Y.Index attr) _ = INDEX (attributeToCST attr)+ toCST (Y.Index alpha) _ = INDEX (alphaToCST alpha) toCST (Y.Length binding) _ = LENGTH (bindingsToCST [binding]) toCST (Y.Domain binding) _ = DOMAIN (bindingsToCST [binding]) toCST (Y.Literal num) _ = LITERAL num
src/Canonizer.hs view
@@ -12,9 +12,9 @@ canonizeBindings :: [Binding] -> Int -> ([Binding], Int) canonizeBindings [] idx = ([], idx)-canonizeBindings ((BiLambda _) : rest) idx =+canonizeBindings ((BiLambda (Function _)) : rest) idx = let (bds', idx') = canonizeBindings rest (idx + 1)- in (BiLambda (T.pack ('F' : show idx)) : bds', idx')+ in (BiLambda (Function (T.pack ('F' : show idx))) : bds', idx') canonizeBindings (BiTau attr expr : rest) idx = let (expr', idx') = canonizeExpression expr idx (bds', idx'') = canonizeBindings rest idx'@@ -30,11 +30,19 @@ canonizeExpression (ExDispatch expr attr) idx = let (expr', idx') = canonizeExpression expr idx in (ExDispatch expr' attr, idx')-canonizeExpression (ExApplication expr (BiTau attr arg)) idx =+canonizeExpression (ExApplication expr arg) idx = let (expr', idx') = canonizeExpression expr idx- (arg', idx'') = canonizeExpression arg idx'- in (ExApplication expr' (BiTau attr arg'), idx'')+ (arg', idx'') = canonizeArgument arg idx'+ in (ExApplication expr' arg', idx'') canonizeExpression expr idx = (expr, idx)++canonizeArgument :: Argument -> Int -> (Argument, Int)+canonizeArgument (ArTau attr expr) idx =+ let (expr', idx') = canonizeExpression expr idx+ in (ArTau attr expr', idx')+canonizeArgument (ArAlpha alpha expr) idx =+ let (expr', idx') = canonizeExpression expr idx+ in (ArAlpha alpha expr', idx') canonize :: [Rewritten] -> [Rewritten] canonize [] = []
src/Condition.hs view
@@ -50,9 +50,9 @@ choice [ do _ <- symbol "index" >> lparen- attr <- _attribute phiParser+ alpha <- _alpha phiParser _ <- rparen- return (Y.Index attr)+ return (Y.Index alpha) , do _ <- symbol "length" >> lparen bd <- _binding phiParser@@ -108,11 +108,6 @@ cond <- condition _ <- rparen return (Y.Not cond)- , do- _ <- symbol "alpha" >> lparen- attr <- _attribute phiParser- _ <- rparen- return (Y.Alpha attr) , do _ <- symbol "eq" >> lparen left <- comparable
src/Dataize.hs view
@@ -52,7 +52,7 @@ formation bds ctx = do let (lambda, bds') = maybeLambda bds case lambda of- Just (BiLambda func) -> Just <$> atom func (ExFormation bds') ctx+ Just (BiLambda (Function func)) -> Just <$> atom func (ExFormation bds') ctx _ -> pure Nothing where maybeLambda :: [Binding] -> (Maybe Binding, [Binding])@@ -65,7 +65,7 @@ [bd] -> (Just bd, rest) _ -> (Nothing, bds) --- Resolve dispatch from global object (Q.tau) for PHI Morphing rule.+-- Resolve dispatch from global object (Q.tau) for ROOT 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 -@@ -81,11 +81,12 @@ BiTau (AtLabel attr) expr' -> if attr == tau then Just expr' else boundExpr bds _ -> boundExpr bds --- The Morphing function 𝕄 maps objects to primitives. It is driven by the+-- The Morphing function 𝕄 maps normal forms 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.+-- the morphed argument is a normalization ('MaNormalize', as in the 'lambda' and+-- 'root' rules), the rewriter runs over the rule's product and its individual+-- steps are spliced into the chain before morphing continues. morph :: Morphed -> DataizeContext -> IO Morphed morph (expr, seq) ctx@DataizeContext{..} = do matched <- firstMatch Y.morphingRules@@ -104,7 +105,7 @@ -- 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+ asRule rule = Y.Rule rule.name rule.description rule.match ExRoot Nothing rule.where_ rule.when apply :: Y.MorphOutcome -> String -> Subst -> IO Morphed apply (Y.MoStop result) name subst = do built <- buildExpressionThrows result subst@@ -114,27 +115,14 @@ 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+ -- 𝕄(𝒩(e)) records the producing step, then delegates to the normalization+ -- rewriter and splices its individual steps (alpha, copy, dot, …) into the+ -- chain before morphing on the resulting normal form.+ apply (Y.MoMorph (Y.MaNormalize arg)) name 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)+ labelled <- leadsTo seq name built ctx+ (expr', seq') <- normalized built labelled ctx 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@@ -162,7 +150,7 @@ (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+ asRule rule = Y.Rule rule.name rule.description rule.match ExRoot Nothing rule.where_ rule.when apply :: Y.DataizeRule -> Subst -> IO Dataized apply rule subst = case rule.then_ of Y.DoData bytes -> do@@ -179,6 +167,14 @@ built <- buildExpressionThrows arg subst (morphed, seq') <- morph (built, seq) ctx dataize' (morphed, seq') ctx+ -- 𝔻(𝒩(e)) records the producing step (the 'box' contextualization), then+ -- normalizes its result back to a normal form before dataizing on, so 𝔻+ -- only ever sees normal forms.+ Y.DoDataize (Y.DaNormalize arg) -> do+ built <- buildExpressionThrows arg subst+ labelled <- leadsTo seq (operation rule) built ctx+ (normal, seq') <- normalized built labelled ctx+ dataize' (normal, seq') ctx operation :: Y.DataizeRule -> String operation rule = case rule.where_ of Just (extra : _) -> Y.function extra@@ -189,14 +185,35 @@ prog' <- withLocatedExpression _locator expr prog pure ((prog', Nothing) :| (prog, Just rule) : rest) +-- Reduce 'expr' to its normal form through the normalization rewriter,+-- splicing the individual steps (alpha, copy, dot, …) into the chain and+-- returning the normalized expression together with the extended sequence.+normalized :: Expression -> NonEmpty Rewritten -> DataizeContext -> IO (Expression, NonEmpty Rewritten)+normalized expr seq ctx@DataizeContext{..} = do+ prog' <- withLocatedExpression _locator expr _program+ (rewrittens, _) <- rewrite prog' normalizationRules (rewriteContext ctx)+ let (rw :| rws) = NE.reverse rewrittens+ seq' = rw :| rws <> NE.tail seq+ expr' <- locatedExpression _locator (fst rw)+ pure (expr', seq')++-- Switch the dataization context to a rewriting context for normalization,+-- disabling the must-checker and breakpoints.+rewriteContext :: DataizeContext -> RewriteContext+rewriteContext DataizeContext{..} =+ RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep+ -- Synthetic dataize function for internal usage inside atoms -- Here we modify original program from context by adding new binding--- which refers to expression we want to dataize.+-- which refers to expression we want to dataize. As a caller of 𝔻, it first+-- reduces the expression to a normal form, since 𝔻 only accepts normal forms. _dataize :: Expression -> DataizeContext -> IO (Maybe Bytes) _dataize expr ctx@DataizeContext{_buildTerm = buildTerm, _program = Program (ExFormation bds)} = do (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty let prog = Program (ExFormation (BiTau attr expr : bds))- (bts, _) <- dataize' (expr, (prog, Nothing) :| []) ctx{_program = prog}+ ctx' = ctx{_program = prog}+ (normal, seq) <- normalized expr ((prog, Nothing) :| []) ctx'+ (bts, _) <- dataize' (normal, seq) ctx' pure bts _dataize _ _ = throwIO (userError "Can't call _dataize from atoms with non-formation program")
src/Encoding.hs view
@@ -33,6 +33,7 @@ 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{meta = META{hd = K, ..}} = EX_META (META EXCL K' rest)+ toASCII EX_META{meta = META{hd = P, ..}} = EX_META (META EXCL P' 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)@@ -73,6 +74,7 @@ toASCII AT_ALPHA{..} = AT_ALPHA ALPHA' idx toASCII AT_PHI{} = AT_PHI AT toASCII AT_RHO{} = AT_RHO CARET+ toASCII AT_META{meta = META{hd = ETA, ..}} = AT_META (META EXCL H rest) toASCII AT_META{..} = AT_META (META EXCL A (rest meta)) toASCII attr = attr
src/Functions.hs view
@@ -211,10 +211,9 @@ join' :: [Binding] -> Set.Set Attribute -> IO [Binding] join' [] _ = pure [] join' (bd : bds) attrs =- case attributesFromBindings [bd] of- [attr] ->- if Set.member attr attrs- then+ case attributeFromBinding bd of+ Just attr+ | Set.member attr attrs -> if attr == AtRho || attr == AtDelta || attr == AtLambda then join' bds attrs else do@@ -223,8 +222,8 @@ BiVoid _ -> BiVoid <$> freshAttr other -> pure other (new :) <$> join' bds attrs- else (bd :) <$> join' bds (Set.insert attr attrs)- _ -> (bd :) <$> join' bds attrs+ | otherwise -> (bd :) <$> join' bds (Set.insert attr attrs)+ Nothing -> (bd :) <$> join' bds attrs freshAttr :: IO Attribute freshAttr = do term <- _randomTau [] subst
src/LaTeX.hs view
@@ -57,7 +57,7 @@ } defaultLatexContext :: LatexContext-defaultLatexContext = LatexContext SWEET SINGLELINE defaultMargin False False defaultMeetPopularity defaultMeetLength ExGlobal Nothing Nothing Nothing+defaultLatexContext = LatexContext SWEET SINGLELINE defaultMargin False False defaultMeetPopularity defaultMeetLength ExRoot Nothing Nothing Nothing defaultMeetPopularity :: Int defaultMeetPopularity = 50@@ -77,13 +77,16 @@ let matched = if countNodes ex >= len then map (const ex) (matchProgram ex prog) else [] in matched ++ case ex of ExDispatch ex' _ -> meetInExpression ex' prog- ExApplication ex' (BiTau _ arg) -> meetInExpression ex' prog ++ meetInExpression arg prog+ ExApplication ex' arg -> meetInExpression ex' prog ++ meetInExpression (argExpr arg) prog ExFormation bds -> meetInBindings bds prog _ -> [] meetInBindings :: [Binding] -> Program -> [Expression] meetInBindings [] _ = [] meetInBindings (BiTau _ ex : bds) prog = meetInExpression ex prog ++ meetInBindings bds prog meetInBindings (_ : bds) prog = meetInBindings bds prog+ argExpr :: Argument -> Expression+ argExpr (ArTau _ ex) = ex+ argExpr (ArAlpha _ ex) = ex {- | Here we're trying to compress sequence of programs with \phiMeet{} and \phiAgain LaTeX functions. We process the sequence of programs and trying to find all expressions in first program which are present@@ -165,7 +168,7 @@ in if _compress then zip (meetInPrograms progs ctx) rules else rewrittens rewrittensToLatex :: Rewrittens' -> LatexContext -> IO String-rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{_focus = ExGlobal} =+rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{_focus = ExRoot} = pure ( concat [ preamble ctx@@ -267,8 +270,11 @@ toLaTeX E = E' toLaTeX N = N' toLaTeX K = K'+ toLaTeX P = P' toLaTeX A = TAU' toLaTeX TAU = TAU'+ toLaTeX ETA = ETA'+ toLaTeX H = ETA' toLaTeX B = B' toLaTeX D = D' toLaTeX mh = mh@@ -372,6 +378,7 @@ 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.DoDataize (Y.DaNormalize expr)) = dataize (normalize (renderToLatex (expressionToCST expr) defaultLatexContext)) dataizeOutcome (Y.DoData bytes) = T.unpack (render (toLaTeX (toCST' bytes :: BYTES))) dataizeOutcome Y.DoNothing = "\\varnothing"
src/Locator.hs view
@@ -26,7 +26,7 @@ show CanNotFindObjectByLocator{..} = printf "Can't find object by locator: '%s'" (printExpression fqn) locatedExpression :: Expression -> Program -> IO Expression-locatedExpression ExGlobal (Program expr) = pure expr+locatedExpression ExRoot (Program expr) = pure expr locatedExpression locator (Program expr) = case fqnToAttrs locator of Just attrs -> locatedExpression' expr attrs _ -> invalidLocator locator@@ -42,7 +42,7 @@ locatedExpression' _ _ = cantFindBy locator withLocatedExpression :: Expression -> Expression -> Program -> IO Program-withLocatedExpression ExGlobal tgt _ = pure (Program tgt)+withLocatedExpression ExRoot tgt _ = pure (Program tgt) withLocatedExpression locator target (Program expr) = case fqnToAttrs locator of Just attrs -> Program <$> withLocatedExpression' expr attrs _ -> invalidLocator locator
src/Matcher.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE OverloadedStrings #-}+ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT @@ -9,12 +11,13 @@ import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Maybe (catMaybes)-import Data.Text (Text)+import Data.Text (Text, isPrefixOf) -- Meta value -- The right part of substitution data MetaValue = MvAttribute Attribute -- !a+ | MvAlpha Alpha -- !h | MvBytes Bytes -- !b | MvBindings [Binding] -- !B | MvFunction Text -- !F@@ -25,7 +28,7 @@ -- Tail operation after expression -- Dispatch or application data Tail- = TaApplication Binding -- BiTau only+ = TaApplication Argument -- application argument | TaDispatch Attribute deriving (Eq, Show) @@ -68,19 +71,33 @@ | ptn == tgt = [substEmpty] | otherwise = [] +matchAlpha :: Alpha -> Alpha -> [Subst]+matchAlpha (AlMeta meta) tgt = [substSingle meta (MvAlpha tgt)]+matchAlpha ptn tgt+ | ptn == tgt = [substEmpty]+ | otherwise = []++matchFunction :: Function -> Function -> [Subst]+matchFunction (FnMeta meta) (Function name) = [substSingle meta (MvFunction name)]+matchFunction ptn tgt+ | ptn == tgt = [substEmpty]+ | otherwise = []+ matchBinding :: Binding -> Binding -> [Subst] matchBinding (BiVoid pattr) (BiVoid tattr) = matchAttribute pattr tattr matchBinding (BiDelta (BtMeta meta)) (BiDelta tdata) = [substSingle meta (MvBytes tdata)] matchBinding (BiDelta pdata) (BiDelta tdata) | pdata == tdata = [substEmpty] | otherwise = []-matchBinding (BiLambda pFunc) (BiLambda tFunc)- | pFunc == tFunc = [substEmpty]- | otherwise = []-matchBinding (BiMetaLambda meta) (BiLambda tFunc) = [substSingle meta (MvFunction tFunc)]+matchBinding (BiLambda pFunc) (BiLambda tFunc) = matchFunction pFunc tFunc matchBinding (BiTau pattr pexp) (BiTau tattr texp) = combineMany (matchAttribute pattr tattr) (matchExpression' pexp texp) matchBinding _ _ = [] +matchArgument :: Argument -> Argument -> [Subst]+matchArgument (ArTau pattr pexp) (ArTau tattr texp) = combineMany (matchAttribute pattr tattr) (matchExpression' pexp texp)+matchArgument (ArAlpha palpha pexp) (ArAlpha talpha texp) = combineMany (matchAlpha palpha talpha) (matchExpression' pexp texp)+matchArgument _ _ = []+ -- Match bindings with ordering matchBindings :: [Binding] -> [Binding] -> [Subst] matchBindings [] [] = [substEmpty]@@ -110,20 +127,22 @@ ExDispatch expr attr -> do (substs, tails) <- tailExpressionsReversed ptn' expr Just (substs, TaDispatch attr : tails)- ExApplication expr tau -> do+ ExApplication expr arg -> do (substs, tails) <- tailExpressionsReversed ptn' expr- Just (substs, TaApplication tau : tails)+ Just (substs, TaApplication arg : tails) _ -> Just ([], []) substs -> Just (substs, []) matchExpression' :: MatchExpressionFunc-matchExpression' (ExMeta meta) tgt = [substSingle meta (MvExpression tgt)]-matchExpression' ExThis ExThis = [substEmpty]-matchExpression' ExGlobal ExGlobal = [substEmpty]+matchExpression' (ExMeta meta) tgt+ | "p" `isPrefixOf` meta = [substSingle meta (MvExpression tgt) | primitive tgt]+ | otherwise = [substSingle meta (MvExpression tgt)]+matchExpression' ExXi ExXi = [substEmpty]+matchExpression' ExRoot ExRoot = [substEmpty] matchExpression' ExTermination ExTermination = [substEmpty] matchExpression' (ExFormation pbs) (ExFormation tbs) = matchBindings pbs tbs matchExpression' (ExDispatch pexp pattr) (ExDispatch texp tattr) = combineMany (matchAttribute pattr tattr) (matchExpression' pexp texp)-matchExpression' (ExApplication pexp pbd) (ExApplication texp tbd) = combineMany (matchExpression' pexp texp) (matchBinding pbd tbd)+matchExpression' (ExApplication pexp parg) (ExApplication texp targ) = combineMany (matchExpression' pexp texp) (matchArgument parg targ) matchExpression' (ExMetaTail expr meta) tgt = case tailExpressions expr tgt of ([], _) -> [] (substs, tails) -> combineMany substs [substSingle meta (MvTail tails)]@@ -140,6 +159,10 @@ matchBindingExpression (BiTau _ expr) ptn = matchExpressionDeep ptn expr matchBindingExpression _ _ = [] +matchArgumentExpression :: Argument -> Expression -> [Subst]+matchArgumentExpression (ArTau _ expr) ptn = matchExpressionDeep ptn expr+matchArgumentExpression (ArAlpha _ expr) ptn = matchExpressionDeep ptn expr+ -- Match expression with deep nested expression(s) matching matchExpressionDeep :: MatchExpressionFunc matchExpressionDeep ptn tgt =@@ -147,7 +170,7 @@ deep = case tgt of ExFormation bds -> concatMap (`matchBindingExpression` ptn) bds ExDispatch expr _ -> matchExpressionDeep ptn expr- ExApplication expr tau -> matchExpressionDeep ptn expr ++ matchBindingExpression tau ptn+ ExApplication expr arg -> matchExpressionDeep ptn expr ++ matchArgumentExpression arg ptn _ -> [] in matched ++ deep
src/Misc.hs view
@@ -78,17 +78,17 @@ show DirectoryDoesNotExist{..} = printf "Directory '%s' does not exist" _dir matchBaseObject :: Expression -> Maybe T.Text-matchBaseObject (ExDispatch ExGlobal (AtLabel label)) = Just label+matchBaseObject (ExDispatch ExRoot (AtLabel label)) = Just label matchBaseObject _ = Nothing pattern BaseObject :: T.Text -> Expression pattern BaseObject label <- (matchBaseObject -> Just label) where- BaseObject label = ExDispatch ExGlobal (AtLabel label)+ BaseObject label = ExDispatch ExRoot (AtLabel label) -- Minimal matcher function (required for view pattern) matchDataObject :: Expression -> Maybe (T.Text, Bytes)-matchDataObject (ExApplication outer (BiTau (AtAlpha 0) inner)) = case (matchOuter outer, matchInner inner) of+matchDataObject (ExApplication outer (ArAlpha (Alpha 0) inner)) = case (matchOuter outer, matchInner inner) of (Just label, Just bts) -> Just (label, bts) _ -> Nothing where@@ -100,7 +100,7 @@ matchInner (ExPhiAgain _ _ inner') = matchInner inner' matchInner inner' = matchInner' inner' matchInner' :: Expression -> Maybe Bytes- matchInner' (ExApplication bytes (BiTau (AtAlpha 0) formation)) = case (matchesBytes bytes, matchFormation formation) of+ matchInner' (ExApplication bytes (ArAlpha (Alpha 0) formation)) = case (matchesBytes bytes, matchFormation formation) of (True, Just bts) -> Just bts _ -> Nothing matchInner' _ = Nothing@@ -126,12 +126,12 @@ DataObject label bts = ExApplication (BaseObject label)- ( BiTau- (AtAlpha 0)+ ( ArAlpha+ (Alpha 0) ( ExApplication (BaseObject "bytes")- ( BiTau- (AtAlpha 0)+ ( ArAlpha+ (Alpha 0) (ExFormation [BiDelta bts, BiVoid AtRho]) ) )@@ -140,11 +140,10 @@ -- Extract attribute from binding attributeFromBinding :: Binding -> Maybe Attribute attributeFromBinding (BiTau attr _) = Just attr+attributeFromBinding (BiVoid attr) = Just attr attributeFromBinding (BiDelta _) = Just AtDelta attributeFromBinding (BiLambda _) = Just AtLambda-attributeFromBinding (BiVoid attr) = Just attr attributeFromBinding (BiMeta _) = Nothing-attributeFromBinding (BiMetaLambda _) = Just AtLambda -- Extract attributes from bindings attributesFromBindings :: [Binding] -> [Attribute]@@ -161,7 +160,7 @@ -- Check if given binding list consists of unique attributes uniqueBindings :: [Binding] -> Either String [Binding]-uniqueBindings bds = case maybeDuplicatedAttribute bds Set.empty of+uniqueBindings bds = case duplicated bds Set.empty of Just attr -> Left ( printf@@ -171,19 +170,13 @@ ) _ -> Right bds where- maybeDuplicatedAttribute :: [Binding] -> Set.Set Attribute -> Maybe Attribute- maybeDuplicatedAttribute [] = const Nothing- maybeDuplicatedAttribute ((BiTau attr _) : rest) = checkAttr attr rest- maybeDuplicatedAttribute (BiVoid attr : rest) = checkAttr attr rest- maybeDuplicatedAttribute (BiLambda _ : rest) = checkAttr AtLambda rest- maybeDuplicatedAttribute (BiMetaLambda _ : rest) = checkAttr AtLambda rest- maybeDuplicatedAttribute (BiDelta _ : rest) = checkAttr AtDelta rest- maybeDuplicatedAttribute (BiMeta _ : rest) = maybeDuplicatedAttribute rest-- checkAttr :: Attribute -> [Binding] -> Set.Set Attribute -> Maybe Attribute- checkAttr attr rest acc- | attr `Set.member` acc = Just attr- | otherwise = maybeDuplicatedAttribute rest (Set.insert attr acc)+ duplicated :: [Binding] -> Set.Set Attribute -> Maybe Attribute+ duplicated [] _ = Nothing+ duplicated (bd : rest) seen = case attributeFromBinding bd of+ Just attr+ | attr `Set.member` seen -> Just attr+ | otherwise -> duplicated rest (Set.insert attr seen)+ Nothing -> duplicated rest seen -- Add void rho binding to the end of the list of any rho binding is not present withVoidRho :: [Binding] -> [Binding]@@ -206,25 +199,29 @@ recoverFormations :: Expression -> Expression recoverFormations (ExFormation bindings) = ExFormation (withVoidRho (map recoverFormations' bindings)) recoverFormations (ExDispatch expr attr) = ExDispatch (recoverFormations expr) attr-recoverFormations (ExApplication expr binding) = ExApplication (recoverFormations expr) (recoverFormations' binding)+recoverFormations (ExApplication expr arg) = ExApplication (recoverFormations expr) (recoverArgument arg) recoverFormations expr = expr recoverFormations' :: Binding -> Binding recoverFormations' (BiTau attr expr) = BiTau attr (recoverFormations expr) recoverFormations' binding = binding +recoverArgument :: Argument -> Argument+recoverArgument (ArTau attr expr) = ArTau attr (recoverFormations expr)+recoverArgument (ArAlpha alpha expr) = ArAlpha alpha (recoverFormations expr)+ -- Transform dispatch to list of attributes--- >>> fqnToAttrs (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "number"))+-- >>> fqnToAttrs (ExDispatch (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")) (AtLabel "number")) -- Just [org,eolang,number] -- >>> fqnToAttrs (ExFormation []) -- Nothing--- >>> fqnToAttrs ExGlobal+-- >>> fqnToAttrs ExRoot -- Just [] fqnToAttrs :: Expression -> Maybe [Attribute] fqnToAttrs expr = fqnToAttrs' expr <&> reverse where fqnToAttrs' :: Expression -> Maybe [Attribute]- fqnToAttrs' ExGlobal = Just []+ fqnToAttrs' ExRoot = Just [] fqnToAttrs' (ExDispatch ex at) = fqnToAttrs' ex <&> (:) at fqnToAttrs' _ = Nothing
src/Parser.hs view
@@ -12,6 +12,7 @@ , parseExpressionThrows , parseAttribute , parseAttributeThrows+ , parseAlpha , parseNumber , parseNumberThrows , parseBinding@@ -47,13 +48,14 @@ data PhiParser = PhiParser { _attribute :: Parser Attribute+ , _alpha :: Parser Alpha , _binding :: Parser Binding , _expression :: Parser Expression , _string :: Parser String } phiParser :: PhiParser-phiParser = PhiParser fullAttribute binding expression quotedStr+phiParser = PhiParser attribute alpha binding expression quotedStr instance Show ParserException where show CouldNotParseProgram{..} = printf "Couldn't parse given phi program, cause: %s" message@@ -239,13 +241,12 @@ [(n, "")] -> return (chr n) _ -> fail ("Invalid hex escape: \\x" ++ digits) -tauBinding :: Parser Attribute -> Parser Binding-tauBinding attr = do- attr' <- attr+tauValue :: Parser Expression+tauValue = choice [ try $ do _ <- arrow- BiTau attr' <$> expression+ expression , do _ <- symbol "(" voids <-@@ -258,12 +259,15 @@ _ <- arrow bs <- formationBindings bds <- validatedBindings (voids ++ bs)- return (BiTau attr' (ExFormation (withVoidRho bds)))+ return (ExFormation (withVoidRho bds)) ] where rb :: Parser String rb = symbol ")" +tauBinding :: Parser Attribute -> Parser Binding+tauBinding attr = BiTau <$> attr <*> tauValue+ metaBinding :: Parser Binding metaBinding = BiMeta <$> meta' 'B' "𝐵" @@ -290,10 +294,10 @@ , try metaBinding , try $ do _ <- lambda- BiLambda . T.pack <$> function+ BiLambda . Function . T.pack <$> function , do _ <- lambda- BiMetaLambda <$> meta 'F'+ BiLambda . FnMeta <$> meta 'F' ] <?> "binding" @@ -326,22 +330,30 @@ ] <?> "attribute" --- full attribute--- 1. label--- 2. meta--- 3. rho--- 4. phi--- 5. alpha-fullAttribute :: Parser Attribute-fullAttribute =+-- alpha+-- 1. index: ~0, α0+-- 2. meta: !h, 𝜂+alpha :: Parser Alpha+alpha = choice- [ attribute- , do+ [ do _ <- choice [symbol "~", symbol "α"]- AtAlpha <$> lexeme L.decimal+ Alpha <$> lexeme L.decimal+ , AlMeta <$> meta' 'h' "𝜂" ]- <?> "full attribute"+ <?> "alpha" +-- application argument+-- 1. tau: <attribute> ↦ <expression>+-- 2. alpha: <alpha> ↦ <expression>+argument :: Parser Argument+argument =+ choice+ [ try (ArAlpha <$> alpha <*> tauValue)+ , ArTau <$> attribute <*> tauValue+ ]+ <?> "argument"+ validatedBindings :: [Binding] -> Parser [Binding] validatedBindings bds = case uniqueBindings bds of Left msg -> fail msg@@ -376,10 +388,10 @@ return (ExFormation (withVoidRho bs)) , do _ <- choice [symbol "$", symbol "ξ"]- return ExThis+ return ExXi , do _ <- global- return ExGlobal+ return ExRoot , do _ <- choice [symbol "T", symbol "⊥"] return ExTermination@@ -388,11 +400,12 @@ , try (ExMeta <$> meta' 'e' "𝑒") , try (ExMeta <$> meta' 'n' "𝑛") , try (ExMeta <$> meta' 'k' "𝑘")- , ExDispatch ExThis <$> attribute+ , try (ExMeta <$> meta' 'p' "𝑝")+ , ExDispatch ExXi <$> attribute ] <?> "expression head" -application :: Expression -> [Binding] -> Expression+application :: Expression -> [Argument] -> Expression application = foldl ExApplication -- tail optional part of application@@ -411,17 +424,17 @@ , do guard ( case expr of- ExThis -> False- ExGlobal -> False+ ExXi -> False+ ExRoot -> False _ -> True ) _ <- symbol "(" bds <- choice- [ try $ tauBinding fullAttribute `sepBy1` symbol ","+ [ try $ argument `sepBy1` symbol "," , do exprs <- expression `sepBy1` symbol ","- return (zipWith (BiTau . AtAlpha) [0 ..] exprs) -- \idx expr -> BiTau (AtAlpha idx) expr+ return (zipWith (ArAlpha . Alpha) [0 ..] exprs) ] _ <- symbol ")" return (application expr bds)@@ -491,7 +504,10 @@ Left err -> throwIO (CouldNotParseNumber err) parseAttribute :: String -> Either String Attribute-parseAttribute = parse' "attribute" fullAttribute+parseAttribute = parse' "attribute" attribute++parseAlpha :: String -> Either String Alpha+parseAlpha = parse' "alpha" alpha parseAttributeThrows :: String -> IO Attribute parseAttributeThrows attr = case parseAttribute attr of
src/Printer.hs view
@@ -10,6 +10,7 @@ , printExpression , printExpression' , printAttribute+ , printAlpha , printBinding , printBytes , printExtraArg@@ -62,12 +63,23 @@ let (_, encoding, _, _) = defaultPrintConfig in printAttribute' att encoding +printAlpha' :: Alpha -> Encoding -> String+printAlpha' index encoding = T.unpack $ render (withEncoding encoding (toCST index (0, NO_EOL) :: ATTRIBUTE))++printAlpha :: Alpha -> String+printAlpha index =+ let (_, encoding, _, _) = defaultPrintConfig+ in printAlpha' index encoding+ printBinding' :: Binding -> PrintConfig -> String printBinding' bd = printExpression' (ExFormation [bd]) printBinding :: Binding -> String printBinding bd = printBinding' bd defaultPrintConfig +printArgument' :: Argument -> PrintConfig -> String+printArgument' arg (_, encoding, _, _) = T.unpack $ render (withEncoding encoding (toCST arg (0, NO_EOL) :: PAIR))+ printBytes :: Bytes -> String printBytes bts = T.unpack $ render (toCST bts (0, NO_EOL) :: BYTES) @@ -81,11 +93,12 @@ printExtraArg arg = printExtraArg' arg defaultPrintConfig printTail :: Tail -> PrintConfig -> String-printTail (TaApplication bd) config = "(" <> printBinding' bd config <> ")"+printTail (TaApplication arg) config = "(" <> printArgument' arg config <> ")" printTail (TaDispatch att) (_, encoding, _, _) = "." <> printAttribute' att encoding printMetaValue :: MetaValue -> PrintConfig -> String printMetaValue (MvAttribute att) (_, encoding, _, _) = printAttribute' att encoding+printMetaValue (MvAlpha index) (_, encoding, _, _) = printAlpha' index encoding printMetaValue (MvExpression ex) config = printExpression' ex config printMetaValue (MvBytes bts) _ = printBytes bts printMetaValue (MvBindings bds) config = printExpression' (ExFormation bds) config
src/Render.hs view
@@ -117,9 +117,14 @@ render N' = "n" render K = "𝑘" render K' = "k"+ render P = "𝑝"+ render P' = "p" render A = "a" render TAU = "𝜏" render TAU' = "\\tau"+ render ETA = "𝜂"+ render ETA' = "\\eta"+ render H = "h" render B = "𝐵" render B' = "B" render D = "δ"
src/Replacer.hs view
@@ -42,6 +42,14 @@ let (bds', ptns', repls') = replaceBindings (bds, ptns, repls) ctx func in (bd : bds', ptns', repls') +replaceArgument :: ReplaceState Argument -> ReplaceContext -> ReplaceExpressionFunc' -> ReplaceState Argument+replaceArgument (ArTau attr expr, ptns, repls) ctx func =+ let (expr', ptns', repls') = func (expr, ptns, repls) ctx+ in (ArTau attr expr', ptns', repls')+replaceArgument (ArAlpha alpha expr, ptns, repls) ctx func =+ let (expr', ptns', repls') = func (expr, ptns, repls) ctx+ in (ArAlpha alpha expr', ptns', repls')+ replaceExpression' :: ReplaceExpressionFunc' replaceExpression' state@(expr, ptns@(ptn : _ptns), repls@(repl : _repls)) ctx = if expr == ptn@@ -50,11 +58,10 @@ ExDispatch inner attr -> let (expr', ptns', repls') = replaceExpression' (inner, ptns, repls) ctx in (ExDispatch expr' attr, ptns', repls')- ExApplication inner tau ->+ ExApplication inner arg -> let (expr', ptns', repls') = replaceExpression' (inner, ptns, repls) ctx- in case replaceBindings ([tau], ptns', repls') ctx replaceExpression' of- ([tau'], ptns'', repls'') -> (ExApplication expr' tau', ptns'', repls'')- (bds', _, _) -> error $ "Expected single binding, got " ++ show (length bds')+ (arg', ptns'', repls'') = replaceArgument (arg, ptns', repls') ctx replaceExpression'+ in (ExApplication expr' arg', ptns'', repls'') ExFormation bds -> let (bds', ptns', repls') = replaceBindings (bds, ptns, repls) ctx replaceExpression' in (ExFormation bds', ptns', repls')@@ -91,10 +98,10 @@ ExDispatch inner attr -> let (expr', ptns', repls') = replaceExpressionFast' (inner, ptns, repls) ctx in (ExDispatch expr' attr, ptns', repls')- ExApplication inner (BiTau attr arg) ->+ ExApplication inner arg -> let (expr', ptns', repls') = replaceExpressionFast' (inner, ptns, repls) ctx- (expr'', ptns'', repls'') = replaceExpressionFast' (arg, ptns', repls') ctx- in (ExApplication expr' (BiTau attr expr''), ptns'', repls'')+ (arg', ptns'', repls'') = replaceArgument (arg, ptns', repls') ctx replaceExpressionFast'+ in (ExApplication expr' arg', ptns'', repls'') _ -> state replaceExpression :: ReplaceExpressionFunc
src/Rule.hs view
@@ -50,11 +50,11 @@ -- Returns True if given expression is in the normal form isNF :: Expression -> RuleContext -> Bool-isNF ExThis _ = True-isNF ExGlobal _ = True+isNF ExXi _ = True+isNF ExRoot _ = True isNF ExTermination _ = True-isNF (ExDispatch ExThis _) _ = True-isNF (ExDispatch ExGlobal _) _ = True+isNF (ExDispatch ExXi _) _ = True+isNF (ExDispatch ExRoot _) _ = True isNF (ExDispatch ExTermination _) _ = False -- dd rule isNF (ExApplication ExTermination _) _ = False -- dc rule isNF (ExFormation []) _ = True@@ -96,10 +96,9 @@ _in :: Attribute -> Binding -> Subst -> RuleContext -> IO [Subst] _in attr binding subst _ = case (buildAttribute attr subst, buildBinding binding subst) of- (Right attr, Right bds) -> pure [subst | attrInBindings attr bds] -- if attrInBindings attr bd then [subst] else []+ (Right attr, Right bds) -> pure [subst | attrInBindings attr bds] (_, _) -> pure [] where- -- Check if given attribute is present in given binding attrInBindings :: Attribute -> [Binding] -> Bool attrInBindings attr (bd : bds) = attrInBinding attr bd || attrInBindings attr bds where@@ -111,13 +110,6 @@ attrInBinding _ _ = False attrInBindings _ _ = False -_alpha :: Attribute -> Subst -> RuleContext -> IO [Subst]-_alpha (AtAlpha _) subst _ = pure [subst]-_alpha (AtMeta name) (Subst mp) _ = case M.lookup name mp of- Just (MvAttribute (AtAlpha _)) -> pure [Subst mp]- _ -> pure []-_alpha _ _ _ = pure []- _eq :: Y.Comparable -> Y.Comparable -> Subst -> RuleContext -> IO [Subst] _eq (Y.CmpNum left) (Y.CmpNum right) subst _ = case (numToInt left subst, numToInt right subst) of (Just left_, Just right_) -> pure [subst | left_ == right_]@@ -125,10 +117,10 @@ where -- Convert Number to Int numToInt :: Y.Number -> Subst -> Maybe Int- numToInt (Y.Index (AtMeta meta)) (Subst mp) = case M.lookup meta mp of- Just (MvAttribute (AtAlpha idx)) -> Just idx+ numToInt (Y.Index (AlMeta meta)) (Subst mp) = case M.lookup meta mp of+ Just (MvAlpha (Alpha idx)) -> Just idx _ -> Nothing- numToInt (Y.Index (AtAlpha idx)) _ = Just idx+ numToInt (Y.Index (Alpha idx)) _ = Just idx numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of Just (MvBindings bds) -> Just (length bds) _ -> Nothing@@ -139,7 +131,6 @@ numToInt _ _ = Nothing notAsset (BiDelta _) = False notAsset (BiLambda _) = False- notAsset (BiMetaLambda _) = False notAsset _ = True _eq (Y.CmpAttr left) (Y.CmpAttr right) subst _ = pure [subst | compareAttrs left right subst] where@@ -189,8 +180,9 @@ where xiFree :: Expression -> Bool xiFree (ExFormation _) = True- xiFree ExGlobal = True- xiFree (ExApplication e (BiTau _ te)) = xiFree e && xiFree te+ xiFree ExRoot = True+ xiFree (ExApplication e (ArTau _ te)) = xiFree e && xiFree te+ xiFree (ExApplication e (ArAlpha _ te)) = xiFree e && xiFree te xiFree (ExDispatch e _) = xiFree e xiFree _ = False @@ -222,15 +214,6 @@ 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.@@ -248,7 +231,6 @@ 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 @@ -257,7 +239,6 @@ meetCondition' (Y.And conds) = _and conds meetCondition' (Y.Not cond) = _not cond meetCondition' (Y.In attr binding) = _in attr binding-meetCondition' (Y.Alpha attr) = _alpha attr meetCondition' (Y.Eq left right) = _eq left right meetCondition' (Y.NF expr) = _nf expr meetCondition' (Y.Absolute expr) = _absolute expr@@ -342,7 +323,7 @@ | T.isPrefixOf prefix mt = [mt] | otherwise = [] go (ExFormation bds) = concatMap goBinding bds- go (ExApplication e bd) = go e ++ goBinding bd+ go (ExApplication e arg) = go e ++ goArgument arg go (ExDispatch e _) = go e go (ExMetaTail e _) = go e go (ExPhiMeet _ _ e) = go e@@ -351,6 +332,9 @@ goBinding :: Binding -> [T.Text] goBinding (BiTau _ e) = go e goBinding _ = []+ goArgument :: Argument -> [T.Text]+ goArgument (ArTau _ expr) = go expr+ goArgument (ArAlpha _ expr) = go expr nfMetaNames :: Expression -> [T.Text] nfMetaNames = metaNamesWithPrefix "n"
src/Sugar.hs view
@@ -113,7 +113,7 @@ toSalty EX_META_TAIL{..} = EX_META_TAIL (toSalty expr) meta toSalty expr = expr -saltifyPrimitive :: EXPRESSION -> EXPRESSION -> EXPRESSION -> TAB -> [Binding] -> EXPRESSION+saltifyPrimitive :: EXPRESSION -> EXPRESSION -> EXPRESSION -> TAB -> [Argument] -> EXPRESSION saltifyPrimitive base bytes data' tb@TAB{..} rhos = let next = TAB (indent + 1) in toSalty
src/Tau.hs view
@@ -53,7 +53,7 @@ exprLabels :: Expression -> Set Text exprLabels (ExFormation bds) = Set.unions (map bindingLabels bds)-exprLabels (ExApplication expr bd) = exprLabels expr <> bindingLabels bd+exprLabels (ExApplication expr arg) = exprLabels expr <> argumentLabels arg exprLabels (ExDispatch expr attr) = exprLabels expr <> attrLabel attr exprLabels (ExMetaTail expr _) = exprLabels expr exprLabels (ExPhiMeet _ _ expr) = exprLabels expr@@ -64,6 +64,10 @@ bindingLabels (BiTau attr expr) = attrLabel attr <> exprLabels expr bindingLabels (BiVoid attr) = attrLabel attr bindingLabels _ = Set.empty++argumentLabels :: Argument -> Set Text+argumentLabels (ArTau attr expr) = attrLabel attr <> exprLabels expr+argumentLabels (ArAlpha _ expr) = exprLabels expr attrLabel :: Attribute -> Set Text attrLabel (AtLabel label) = Set.singleton label
src/XMIR.hs view
@@ -85,8 +85,8 @@ object attrs children = NodeElement (element "o" attrs children) expression :: Expression -> XmirContext -> IO (String, [Node])-expression ExThis _ = pure (printExpression ExThis, [])-expression ExGlobal _ = pure (printExpression ExGlobal, [])+expression ExXi _ = pure (printExpression ExXi, [])+expression ExRoot _ = pure (printExpression ExRoot, []) expression (ExFormation bds) ctx = do nested <- nestedBindings bds ctx pure ("", nested)@@ -102,7 +102,7 @@ expression (DataNumber bytes) XmirContext{..} = let bts = object- [("as", printAttribute (AtAlpha 0)), ("base", "Φ.bytes")]+ [("as", printAlpha (Alpha 0)), ("base", "Φ.bytes")] [object [] [NodeContent (T.pack (printBytes bytes))]] in pure ( "Φ.number"@@ -116,7 +116,7 @@ expression (DataString bytes) XmirContext{..} = let bts = object- [("as", printAttribute (AtAlpha 0)), ("base", "Φ.bytes")]+ [("as", printAlpha (Alpha 0)), ("base", "Φ.bytes")] [object [] [NodeContent (T.pack (printBytes bytes))]] in pure ( "Φ.string"@@ -127,16 +127,18 @@ , bts ] )-expression (ExApplication expr (BiTau attr texpr)) ctx = do+expression (ExApplication expr arg) ctx = do (base, children) <- expression expr ctx (base', children') <- expression texpr ctx- let as = printAttribute attr- attrs =+ let attrs = if null base' then [("as", as)] else [("as", as), ("base", base')] pure (base, children ++ [object attrs children'])-expression (ExApplication (ExFormation bds) tau) _ = throwIO (UnsupportedExpression (ExApplication (ExFormation bds) tau))+ where+ (as, texpr) = case arg of+ ArTau attr value -> (printAttribute attr, value)+ ArAlpha alpha value -> (printAlpha alpha, value) expression expr _ = throwIO (UnsupportedExpression expr) formationBinding :: Binding -> XmirContext -> IO (Maybe Node)@@ -165,7 +167,7 @@ ExFormation _ -> programToXMIR' ExApplication _ _ -> programToXMIR' ExDispatch _ _ -> programToXMIR'- ExGlobal -> programToXMIR'+ ExRoot -> programToXMIR' _ -> throwIO (UnsupportedProgram prog) where programToXMIR' :: IO Document@@ -205,13 +207,13 @@ -- - X: list of package parts -- - Y: root object expression getPackage :: Expression -> IO ([String], Expression)- getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda "Package", BiVoid AtRho]), BiVoid AtRho]) = do- (pckg, expr') <- getPackage (ExFormation [bd, BiLambda "Package", BiVoid AtRho])+ getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho]), BiVoid AtRho]) = do+ (pckg, expr') <- getPackage (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho]) pure (T.unpack label : pckg, expr')- getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda "Package", BiVoid AtRho]), BiLambda "Package", BiVoid AtRho]) = do- (pckg, expr') <- getPackage (ExFormation [bd, BiLambda "Package", BiVoid AtRho])+ getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho]), BiLambda (Function "Package"), BiVoid AtRho]) = do+ (pckg, expr') <- getPackage (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho]) pure (T.unpack label : pckg, expr')- getPackage (ExFormation [BiTau at ex, BiLambda "Package", BiVoid AtRho]) = pure ([], ExFormation [BiTau at ex, BiVoid AtRho])+ getPackage (ExFormation [BiTau at ex, BiLambda (Function "Package"), BiVoid AtRho]) = pure ([], ExFormation [BiTau at ex, BiVoid AtRho]) getPackage (ExFormation [bd, BiVoid AtRho]) = pure ([], ExFormation [bd, BiVoid AtRho]) getPackage ex = throwIO (userError (printf "Can't extract package from given expression:\n %s" (printExpression ex))) -- Convert root Expression to Node@@ -378,7 +380,7 @@ if null pckg then pure (Program (ExFormation [obj, BiVoid AtRho])) else- let bd = foldr (\part acc -> BiTau (AtLabel (T.pack part)) (ExFormation [acc, BiLambda "Package", BiVoid AtRho])) obj pckg+ let bd = foldr (\part acc -> BiTau (AtLabel (T.pack part)) (ExFormation [acc, BiLambda (Function "Package"), BiVoid AtRho])) obj pckg in pure (Program (ExFormation [bd, BiVoid AtRho])) | otherwise -> throwIO (InvalidXMIRFormat "Expected single <object> element" doc) _ -> throwIO (InvalidXMIRFormat "NodeElement is expected as root element" doc)@@ -390,7 +392,7 @@ name <- getAttr "name" cur bds <- mapM (`xmirToFormationBinding` (name : fqn)) (cur C.$/ C.element (toName "o")) >>= uniqueBindings' case name of- "λ" -> pure (BiLambda (T.pack (intercalate "_" ("L" : reverse fqn))))+ "λ" -> pure (BiLambda (Function (T.pack (intercalate "_" ("L" : reverse fqn))))) ('α' : _) -> throwIO (InvalidXMIRFormat "Formation child @name can't start with α" cur) "φ" -> pure (BiTau AtPhi (ExFormation (withVoidRho bds))) _ -> pure (BiTau (AtLabel (T.pack name)) (ExFormation (withVoidRho bds)))@@ -426,14 +428,14 @@ xmirToApplication disp args' fqn "ξ" -> if null (cur C.$/ C.element (toName "o"))- then pure ExThis+ then pure ExXi else throwIO (InvalidXMIRFormat "Application of 'ξ' is illegal in XMIR" cur) "Φ" -> if null (cur C.$/ C.element (toName "o"))- then pure ExGlobal+ then pure ExRoot else throwIO (InvalidXMIRFormat "Application of 'Φ' is illegal in XMIR" cur)- 'Φ' : '.' : rest -> xmirToExpression' ExGlobal "Φ" rest cur fqn- 'ξ' : '.' : rest -> xmirToExpression' ExThis "ξ" rest cur fqn+ 'Φ' : '.' : rest -> xmirToExpression' ExRoot "Φ" rest cur fqn+ 'ξ' : '.' : rest -> xmirToExpression' ExXi "ξ" rest cur fqn _ -> throwIO (InvalidXMIRFormat "The @base attribute must be either ['∅'|'Φ'] or start with ['Φ.'|'ξ.'|'.']" cur) | otherwise = do bds <- mapM (`xmirToFormationBinding` fqn) (cur C.$/ C.element (toName "o")) >>= uniqueBindings'@@ -462,37 +464,38 @@ | hasAttr "base" arg && hasText arg = throwIO (InvalidXMIRFormat "It's illegal in XMIR to have @base and text() at the same time" arg) | not (hasAttr "base" arg) && not (hasText arg) = do bds <- mapM (`xmirToFormationBinding` fqn) (arg C.$/ C.element (toName "o"))- as <- asToAttr arg idx- pure (ExApplication expr (BiTau as (ExFormation (withVoidRho bds))))+ key <- asToKey arg idx+ pure (ExApplication expr (mkArg key (ExFormation (withVoidRho bds)))) | not (hasAttr "base" arg) && hasText arg = do- as <- asToAttr arg idx+ key <- asToKey arg idx bytes <- getText arg- pure (ExApplication expr (BiTau as (ExFormation [BiDelta (bytesToBts bytes), BiVoid AtRho])))+ pure (ExApplication expr (mkArg key (ExFormation [BiDelta (bytesToBts bytes), BiVoid AtRho]))) | otherwise = do- as <- asToAttr arg idx+ key <- asToKey arg idx arg' <- xmirToExpression arg fqn- pure (ExApplication expr (BiTau as arg'))+ pure (ExApplication expr (mkArg key arg')) app' <- app xmirToApplication' (idx + 1) app' args fqn-- asToAttr :: C.Cursor -> Int -> IO Attribute- asToAttr cur idx+ mkArg :: Either Alpha Attribute -> Expression -> Argument+ mkArg (Left alpha) expr = ArAlpha alpha expr+ mkArg (Right attr) expr = ArTau attr expr+ asToKey :: C.Cursor -> Int -> IO (Either Alpha Attribute)+ asToKey cur position | hasAttr "as" cur = do as <- getAttr "as" cur- attr <- toAttr as cur- case attr of- AtRho -> throwIO (InvalidXMIRFormat "The 'ρ' in @as attribute is illegal in XMIR" cur)- _ -> pure attr- | otherwise = pure (AtAlpha idx)+ case as of+ 'α' : rest' -> case TR.readMaybe rest' :: Maybe Int of+ Just idx -> pure (Left (Alpha idx))+ Nothing -> throwIO (InvalidXMIRFormat "The attribute started with 'α' must be followed by integer" cur)+ "ρ" -> throwIO (InvalidXMIRFormat "The 'ρ' in @as attribute is illegal in XMIR" cur)+ _ -> Right <$> toAttr as cur+ | otherwise = pure (Left (Alpha position)) toAttr :: String -> C.Cursor -> IO Attribute toAttr attr cur = case attr of- 'α' : rest' ->- case TR.readMaybe rest' :: Maybe Int of- Just idx -> pure (AtAlpha idx)- Nothing -> throwIO (InvalidXMIRFormat "The attribute started with 'α' must be followed by integer" cur) "φ" -> pure AtPhi "ρ" -> pure AtRho+ 'α' : _ -> throwIO (InvalidXMIRFormat "α-index is not a valid dispatch attribute in XMIR" cur) ch : _ | ch `notElem` ['a' .. 'z'] -> throwIO (InvalidXMIRFormat (printf "The attribute '%s' must start with ['a'..'z']" attr) cur) | '.' `elem` attr -> throwIO (InvalidXMIRFormat "Attribute can't contain dots" cur)
src/Yaml.hs view
@@ -43,6 +43,9 @@ Right attr -> pure attr ) +instance FromJSON Alpha where+ parseJSON = parseJSON' "Alpha" parseAlpha+ instance FromJSON Bytes where parseJSON = parseJSON' "Bytes" parseBytes @@ -78,12 +81,11 @@ withObject "Condition" ( \v -> do- validateYamlObject v ["and", "or", "not", "alpha", "nf", "absolute", "eq", "in", "matches", "part-of", "primitive", "disjoint"]+ validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "in", "matches", "part-of", "primitive", "disjoint"] asum [ And <$> v .: "and" , Or <$> v .: "or" , Not <$> v .: "not"- , Alpha <$> v .: "alpha" , NF <$> v .: "nf" , Absolute <$> v .: "absolute" , Primitive <$> v .: "primitive"@@ -148,7 +150,7 @@ } data Number- = Index Attribute+ = Index Alpha | Length Binding | Domain Binding | Literal Int@@ -165,7 +167,6 @@ | Or [Condition] | In Attribute Binding | Not Condition- | Alpha Attribute | Eq Comparable Comparable | NF Expression | Absolute Expression@@ -207,7 +208,7 @@ decodeRule :: (FilePath, BS.ByteString) -> Rule decodeRule (path, bs) = case Yaml.decodeEither' bs of- Right r -> r+ Right rule -> rule Left err -> error $ "YAML parse error in " ++ path ++ ": " ++ show err yamlRule :: FilePath -> IO Rule@@ -237,11 +238,13 @@ | 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 }').+-- The argument of a dataization continuation: a plain expression ('𝔻(e)'),+-- the morphing of one ('𝔻(𝕄(e))', written '{ morph: e }'), or the+-- normalization of one ('𝔻(𝒩(e))', written '{ normalize: e }'). data DataizeArg = DaExpr Expression | DaMorph Expression+ | DaNormalize Expression deriving (Eq, Generic, Show) -- One ordered morphing rule: match the expression, build extra metas in@@ -289,8 +292,11 @@ instance FromJSON DataizeArg where parseJSON (Object o) = do- validateYamlObject o ["morph"]- DaMorph <$> o .: "morph"+ validateYamlObject o ["morph", "normalize"]+ morphed <- o .:? "morph"+ case morphed of+ Just expr -> pure (DaMorph expr)+ Nothing -> DaNormalize <$> o .: "normalize" parseJSON v = DaExpr <$> parseJSON v instance FromJSON MorphRule where
test/ASTSpec.hs view
@@ -29,14 +29,23 @@ describe "Attribute Show instance renders AtAlpha" $ forM_- [ ("zero index", AtAlpha 0, "α0")- , ("positive index", AtAlpha 42, "α42")- , ("large index", AtAlpha 999, "α999")+ [ ("zero index", Alpha 0, "α0")+ , ("positive index", Alpha 42, "α42")+ , ("large index", Alpha 999, "α999") ] ( \(desc, attr, expected) -> it desc $ show attr `shouldBe` expected ) + describe "Alpha Eq instance compares same constructors" $+ forM_+ [ ("alphas equal", Alpha 1, Alpha 1, True)+ , ("alphas differ", Alpha 1, Alpha 2, False)+ ]+ ( \(desc, lhs, rhs, expected) ->+ it desc $ (lhs == rhs) `shouldBe` expected+ )+ describe "Attribute Show instance renders special attributes" $ forM_ [ ("rho", AtRho, "ρ")@@ -62,8 +71,6 @@ forM_ [ ("labels equal", AtLabel "x", AtLabel "x", True) , ("labels differ", AtLabel "x", AtLabel "y", False)- , ("alphas equal", AtAlpha 1, AtAlpha 1, True)- , ("alphas differ", AtAlpha 1, AtAlpha 2, False) , ("metas equal", AtMeta "a", AtMeta "a", True) , ("metas differ", AtMeta "a", AtMeta "b", False) , ("rho equals rho", AtRho, AtRho, True)@@ -77,8 +84,7 @@ describe "Attribute Eq instance compares different constructors" $ forM_- [ ("label vs alpha", AtLabel "x", AtAlpha 0, False)- , ("rho vs phi", AtRho, AtPhi, False)+ [ ("rho vs phi", AtRho, AtPhi, False) , ("delta vs lambda", AtDelta, AtLambda, False) , ("meta vs label", AtMeta "x", AtLabel "x", False) ]@@ -88,7 +94,7 @@ describe "Attribute Ord instance orders correctly" $ it "sorts attributes by constructor order" $- let attrs = [AtMeta "z", AtDelta, AtLambda, AtRho, AtPhi, AtAlpha 1, AtLabel "a"]+ let attrs = [AtMeta "z", AtDelta, AtLambda, AtRho, AtPhi, AtLabel "a"] first : _ = sort attrs isLabel (AtLabel _) = True isLabel _ = False@@ -126,19 +132,19 @@ describe "Binding Eq instance compares same constructors" $ forM_- [ ("tau equals tau", BiTau AtRho ExGlobal, BiTau AtRho ExGlobal, True)- , ("tau differs by attr", BiTau AtRho ExGlobal, BiTau AtPhi ExGlobal, False)- , ("tau differs by expr", BiTau AtRho ExGlobal, BiTau AtRho ExThis, False)+ [ ("tau equals tau", BiTau AtRho ExRoot, BiTau AtRho ExRoot, True)+ , ("tau differs by attr", BiTau AtRho ExRoot, BiTau AtPhi ExRoot, False)+ , ("tau differs by expr", BiTau AtRho ExRoot, BiTau AtRho ExXi, False) , ("meta equals meta", BiMeta "B", BiMeta "B", True) , ("meta differs", BiMeta "B", BiMeta "C", False) , ("delta equals delta", BiDelta BtEmpty, BiDelta BtEmpty, True) , ("delta differs", BiDelta BtEmpty, BiDelta (BtOne "00"), False) , ("void equals void", BiVoid AtRho, BiVoid AtRho, True) , ("void differs", BiVoid AtRho, BiVoid AtPhi, False)- , ("lambda equals lambda", BiLambda "Func", BiLambda "Func", True)- , ("lambda differs", BiLambda "Func", BiLambda "Other", False)- , ("metalambda equals", BiMetaLambda "F", BiMetaLambda "F", True)- , ("metalambda differs", BiMetaLambda "F", BiMetaLambda "G", False)+ , ("lambda equals lambda", BiLambda (Function "Func"), BiLambda (Function "Func"), True)+ , ("lambda differs", BiLambda (Function "Func"), BiLambda (Function "Other"), False)+ , ("metalambda equals", BiLambda (FnMeta "F"), BiLambda (FnMeta "F"), True)+ , ("metalambda differs", BiLambda (FnMeta "F"), BiLambda (FnMeta "G"), False) ] ( \(desc, lhs, rhs, expected) -> it desc $ (lhs == rhs) `shouldBe` expected@@ -146,9 +152,9 @@ describe "Binding Eq instance compares different constructors" $ forM_- [ ("tau vs meta", BiTau AtRho ExGlobal, BiMeta "B", False)+ [ ("tau vs meta", BiTau AtRho ExRoot, BiMeta "B", False) , ("delta vs void", BiDelta BtEmpty, BiVoid AtDelta, False)- , ("lambda vs metalambda", BiLambda "F", BiMetaLambda "F", False)+ , ("lambda vs metalambda", BiLambda (Function "F"), BiLambda (FnMeta "F"), False) ] ( \(desc, lhs, rhs, expected) -> it desc $ (lhs == rhs) `shouldBe` expected@@ -156,7 +162,7 @@ describe "Binding Ord instance orders correctly" $ it "sorts bindings by constructor order" $- let bindings = [BiMetaLambda "Z", BiLambda "A", BiVoid AtRho, BiDelta BtEmpty, BiMeta "B", BiTau AtRho ExGlobal]+ let bindings = [BiLambda (FnMeta "Z"), BiLambda (Function "A"), BiVoid AtRho, BiDelta BtEmpty, BiMeta "B", BiTau AtRho ExRoot] first : _ = sort bindings isTau (BiTau _ _) = True isTau _ = False@@ -166,16 +172,16 @@ forM_ [ ("formation equals", ExFormation [], ExFormation [], True) , ("formation differs", ExFormation [], ExFormation [BiVoid AtRho], False)- , ("this equals this", ExThis, ExThis, True)- , ("global equals global", ExGlobal, ExGlobal, True)+ , ("this equals this", ExXi, ExXi, True)+ , ("global equals global", ExRoot, ExRoot, True) , ("termination equals", ExTermination, ExTermination, True) , ("meta equals meta", ExMeta "e", ExMeta "e", True) , ("meta differs", ExMeta "e", ExMeta "f", False)- , ("application equals", ExApplication ExGlobal (BiTau AtRho ExThis), ExApplication ExGlobal (BiTau AtRho ExThis), True)- , ("dispatch equals", ExDispatch ExGlobal AtRho, ExDispatch ExGlobal AtRho, True)- , ("dispatch differs", ExDispatch ExGlobal AtRho, ExDispatch ExGlobal AtPhi, False)- , ("metatail equals", ExMetaTail ExGlobal "t", ExMetaTail ExGlobal "t", True)- , ("metatail differs", ExMetaTail ExGlobal "t", ExMetaTail ExGlobal "s", False)+ , ("application equals", ExApplication ExRoot (ArTau AtRho ExXi), ExApplication ExRoot (ArTau AtRho ExXi), True)+ , ("dispatch equals", ExDispatch ExRoot AtRho, ExDispatch ExRoot AtRho, True)+ , ("dispatch differs", ExDispatch ExRoot AtRho, ExDispatch ExRoot AtPhi, False)+ , ("metatail equals", ExMetaTail ExRoot "t", ExMetaTail ExRoot "t", True)+ , ("metatail differs", ExMetaTail ExRoot "t", ExMetaTail ExRoot "s", False) ] ( \(desc, lhs, rhs, expected) -> it desc $ (lhs == rhs) `shouldBe` expected@@ -183,9 +189,9 @@ describe "Expression Eq instance compares different constructors" $ forM_- [ ("formation vs this", ExFormation [], ExThis, False)- , ("global vs termination", ExGlobal, ExTermination, False)- , ("meta vs dispatch", ExMeta "e", ExDispatch ExGlobal AtRho, False)+ [ ("formation vs this", ExFormation [], ExXi, False)+ , ("global vs termination", ExRoot, ExTermination, False)+ , ("meta vs dispatch", ExMeta "e", ExDispatch ExRoot AtRho, False) ] ( \(desc, lhs, rhs, expected) -> it desc $ (lhs == rhs) `shouldBe` expected@@ -193,14 +199,14 @@ describe "Expression Ord instance orders correctly" $ it "sorts expressions by constructor order" $- let exprs = [ExMetaTail ExGlobal "t", ExDispatch ExGlobal AtRho, ExApplication ExGlobal (BiVoid AtRho), ExMeta "e", ExTermination, ExGlobal, ExThis, ExFormation []]+ let exprs = [ExMetaTail ExRoot "t", ExDispatch ExRoot AtRho, ExApplication ExRoot (ArTau AtRho ExRoot), ExMeta "e", ExTermination, ExRoot, ExXi, ExFormation []] first : _ = sort exprs in first `shouldBe` ExFormation [] describe "Program Eq instance compares programs" $ forM_- [ ("same programs equal", Program ExGlobal, Program ExGlobal, True)- , ("different programs differ", Program ExGlobal, Program ExThis, False)+ [ ("same programs equal", Program ExRoot, Program ExRoot, True)+ , ("different programs differ", Program ExRoot, Program ExXi, False) ] ( \(desc, lhs, rhs, expected) -> it desc $ (lhs == rhs) `shouldBe` expected@@ -208,33 +214,33 @@ describe "Program Ord instance orders correctly" $ it "orders programs by expression" $- let progs = [Program ExThis, Program ExGlobal, Program (ExFormation [])]+ let progs = [Program ExXi, Program ExRoot, Program (ExFormation [])] first : _ = sort progs in first `shouldBe` Program (ExFormation []) describe "Program Show instance renders programs" $ it "shows program wrapper" $ let hasProgram str = "Program" `elem` words str- in show (Program ExGlobal) `shouldSatisfy` hasProgram+ in show (Program ExRoot) `shouldSatisfy` hasProgram describe "countNodes counts ExFormation with non-tau bindings" $ forM_- [ ("Q", ExGlobal, 1)+ [ ("Q", ExRoot, 1) , ("T", ExTermination, 1)- , ("$", ExThis, 1)- , ("dispatch on global", ExDispatch ExGlobal (AtLabel "x"), 3)- , ("application with globals", ExApplication ExGlobal (BiTau AtRho ExGlobal), 6)- , ("nested expressions", ExFormation [BiTau AtRho ExGlobal, BiTau AtPhi ExGlobal], 9)+ , ("$", ExXi, 1)+ , ("dispatch on global", ExDispatch ExRoot (AtLabel "x"), 3)+ , ("application with globals", ExApplication ExRoot (ArTau AtRho ExRoot), 6)+ , ("nested expressions", ExFormation [BiTau AtRho ExRoot, BiTau AtPhi ExRoot], 9) , ("empty formation", ExFormation [], 1) , ("void binding", ExFormation [BiVoid AtRho], 5) , ("delta binding", ExFormation [BiDelta BtEmpty], 5)- , ("lambda binding", ExFormation [BiLambda "Func"], 5)+ , ("lambda binding", ExFormation [BiLambda (Function "Func")], 5) , ("meta binding", ExFormation [BiMeta "B"], 3)- , ("metalambda binding", ExFormation [BiMetaLambda "F"], 5)+ , ("metalambda binding", ExFormation [BiLambda (FnMeta "F")], 5) , ("meta expression", ExMeta "e", 1)- , ("metatail expression", ExMetaTail ExGlobal "t", 3)- , ("deeply nested dispatch", ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b"), 5)- , ("formation with dispatch inside", ExFormation [BiTau AtRho (ExDispatch ExGlobal (AtLabel "x"))], 7)+ , ("metatail expression", ExMetaTail ExRoot "t", 3)+ , ("deeply nested dispatch", ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b"), 5)+ , ("formation with dispatch inside", ExFormation [BiTau AtRho (ExDispatch ExRoot (AtLabel "x"))], 7) ] ( \(desc, expr, expected) -> it desc $ countNodes expr `shouldBe` expected
test/BuilderSpec.hs view
@@ -26,64 +26,64 @@ buildExpression [ ( "Q.!a => (!a >> x) => Q.x"- , ExDispatch ExGlobal (AtMeta "a")+ , ExDispatch ExRoot (AtMeta "a") , [("a", MvAttribute (AtLabel "x"))]- , Right (ExDispatch ExGlobal (AtLabel "x"))+ , Right (ExDispatch ExRoot (AtLabel "x")) ) , ( "Q.c(!a -> !e) => (!a >> x, !e >> $.y.z) => Q.c(x -> $.y.z)"- , ExApplication (ExDispatch ExGlobal (AtLabel "c")) (BiTau (AtMeta "a") (ExMeta "e"))- , [("a", MvAttribute (AtLabel "x")), ("e", MvExpression (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z")))]- , Right (ExApplication (ExDispatch ExGlobal (AtLabel "c")) (BiTau (AtLabel "x") (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z"))))+ , ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArTau (AtMeta "a") (ExMeta "e"))+ , [("a", MvAttribute (AtLabel "x")), ("e", MvExpression (ExDispatch (ExDispatch ExXi (AtLabel "y")) (AtLabel "z")))]+ , Right (ExApplication (ExDispatch ExRoot (AtLabel "c")) (ArTau (AtLabel "x") (ExDispatch (ExDispatch ExXi (AtLabel "y")) (AtLabel "z")))) ) , ( "[[!a -> $.x, !B]] => (!a >> y, !B >> [[b -> ?, L> Func]]) => [[y -> $.x, b -> ?, L> Func]]"- , ExFormation [BiTau (AtMeta "a") (ExDispatch ExThis (AtLabel "x")), BiMeta "B"]- , [("a", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "b"), BiLambda "Func"])]+ , ExFormation [BiTau (AtMeta "a") (ExDispatch ExXi (AtLabel "x")), BiMeta "B"]+ , [("a", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "b"), BiLambda (Function "Func")])] , Right ( ExFormation- [ BiTau (AtLabel "y") (ExDispatch ExThis (AtLabel "x"))+ [ BiTau (AtLabel "y") (ExDispatch ExXi (AtLabel "x")) , BiVoid (AtLabel "b")- , BiLambda "Func"+ , BiLambda (Function "Func") ] ) ) , ( "Q * !t => (!t >> [.a, .b, (~1 -> $.x)]) => Q.a.b(~1 -> $.x)"- , ExMetaTail ExGlobal "t"- , [("t", MvTail [TaDispatch (AtLabel "a"), TaDispatch (AtLabel "b"), TaApplication (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "x")))])]- , Right (ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")) (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "x"))))+ , ExMetaTail ExRoot "t"+ , [("t", MvTail [TaDispatch (AtLabel "a"), TaDispatch (AtLabel "b"), TaApplication (ArAlpha (Alpha 1) (ExDispatch ExXi (AtLabel "x")))])]+ , Right (ExApplication (ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")) (ArAlpha (Alpha 1) (ExDispatch ExXi (AtLabel "x")))) ) , ( "Q.!a => () => X"- , ExDispatch ExGlobal (AtMeta "a")+ , ExDispatch ExRoot (AtMeta "a") , [] , Left "meta 'a' is either does not exist or refers to an inappropriate term" ) , ( "!e0(!a1 -> !e1, !a2 => !e2) => (!e0 >> [[]], !a1 >> x, !e1 >> Q, !a2 >> y, !e2 >> $) => [[]](x -> Q, y -> $)"- , ExApplication (ExApplication (ExMeta "e0") (BiTau (AtMeta "a1") (ExMeta "e1"))) (BiTau (AtMeta "a2") (ExMeta "e2"))+ , ExApplication (ExApplication (ExMeta "e0") (ArTau (AtMeta "a1") (ExMeta "e1"))) (ArTau (AtMeta "a2") (ExMeta "e2")) , [ ("e0", MvExpression (ExFormation [])) , ("a1", MvAttribute (AtLabel "x"))- , ("e1", MvExpression ExGlobal)+ , ("e1", MvExpression ExRoot) , ("a2", MvAttribute (AtLabel "y"))- , ("e2", MvExpression ExThis)+ , ("e2", MvExpression ExXi) ]- , Right (ExApplication (ExApplication (ExFormation []) (BiTau (AtLabel "x") ExGlobal)) (BiTau (AtLabel "y") ExThis))+ , Right (ExApplication (ExApplication (ExFormation []) (ArTau (AtLabel "x") ExRoot)) (ArTau (AtLabel "y") ExXi)) ) , ( "⟦!a ↦ ∅, !B⟧.!a => (!a >> t, !B >> ⟦ x ↦ ξ.t ⟧ ) => ⟦ t ↦ ∅, x ↦ ξ.t ⟧.t" , ExDispatch (ExFormation [BiVoid (AtMeta "a"), BiMeta "B"]) (AtMeta "a") , [ ("a", MvAttribute (AtLabel "t"))- , ("B", MvBindings [BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))])+ , ("B", MvBindings [BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))]) ] , Right ( ExDispatch ( ExFormation [ BiVoid (AtLabel "t")- , BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))+ , BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t")) ] ) (AtLabel "t")@@ -96,14 +96,14 @@ built <- buildExpressionsThrows (ExMeta "e")- [ substSingle "e" (MvExpression (ExDispatch ExGlobal (AtLabel "x")))- , substSingle "e" (MvExpression (ExDispatch ExThis (AtLabel "y")))+ [ substSingle "e" (MvExpression (ExDispatch ExRoot (AtLabel "x")))+ , substSingle "e" (MvExpression (ExDispatch ExXi (AtLabel "y"))) ]- built `shouldBe` [ExDispatch ExGlobal (AtLabel "x"), ExDispatch ExThis (AtLabel "y")]+ built `shouldBe` [ExDispatch ExRoot (AtLabel "x"), ExDispatch ExXi (AtLabel "y")] it "!e => [(!e1 >> Q.x)] => X" $ buildExpressionsThrows (ExMeta "e")- [substSingle "e1" (MvExpression (ExDispatch ExGlobal (AtLabel "x")))]+ [substSingle "e1" (MvExpression (ExDispatch ExRoot (AtLabel "x")))] `shouldThrow` anyException describe "build with duplicate attributes in bindings" $ do
test/CLISpec.hs view
@@ -868,7 +868,6 @@ , " \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:copy}}" , " \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}" , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]] ]] ( ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\} \\leadsto_{\\nameref{r:Mprim}}" , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\}{.}" , "\\end{phiquation}" , "01-"@@ -946,9 +945,9 @@ [ unlines [ "\\begin{tabular}{rl}" , "\\trrule{alpha}"- , " { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_2 -> e ) }"+ , " { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\eta -> e ) }" , " { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e ) }"- , " { if $ \\indexof{ \\tau_2 } = \\vert \\overline{ B_1 } \\vert $ }"+ , " { if $ \\indexof{ \\eta } = \\vert \\overline{ B_1 } \\vert $ }" , " { }" , "\\trrule{copy}" , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"@@ -960,6 +959,11 @@ , " { T }" , " { }" , " { }"+ , "\\trrule{dca}"+ , " { T ( \\eta -> e ) }"+ , " { T }"+ , " { }"+ , " { }" , "\\trrule{dd}" , " { T . \\tau }" , " { T }"@@ -973,7 +977,7 @@ , "\\trrule{miss}" , " { [[ B ]] ( \\tau -> e ) }" , " { T }"- , " { if $ \\tau \\notin B \\;\\text{and}\\; \\tau \\notin [ ~0, ~1, \\dots ] $ }"+ , " { if $ \\tau \\notin B $ }" , " { }" , "\\trrule{null}" , " { [[ B_1, \\tau -> ?, B_2 ]] . \\tau }"@@ -1009,28 +1013,23 @@ ["explain", "--morph"] [ unlines [ "\\begin{tabular}{rl}"- , "\\trrule{Mprim}"- , " { \\mathbb{M}( e ) }"- , " { e }"- , " { if $ e \\in \\mathcal{P} $ }"+ , "\\trrule{prim}"+ , " { \\mathbb{M}( p ) }"+ , " { p }" , " { }"- , "\\trrule{Mnmz}"- , " { \\mathbb{M}( e ) }"- , " { \\mathbb{M}( \\mathcal{N}( e ) ) }"- , " { if $ not( \\isnormal{ e } ) $ }" , " { }"- , "\\trrule{Mlambda}"+ , "\\trrule{lambda}" , " { \\mathbb{M}( [[ B_1, L> F, B_2 ]] * t ) }"- , " { \\mathbb{M}( e * t ) }"+ , " { \\mathbb{M}( \\mathcal{N}( e * t ) ) }" , " { }" , " { where $ e \\coloneqq lambda( [[ B_1, L> F, B_2 ]] ) $ }"- , "\\trrule{Mphi}"+ , "\\trrule{root}" , " { \\mathbb{M}( Q . \\tau * t ) }"- , " { \\mathbb{M}( e * t ) }"+ , " { \\mathbb{M}( \\mathcal{N}( e * t ) ) }" , " { }" , " { where $ e \\coloneqq global( \\tau ) $ }"- , "\\trrule{Mstuck}"- , " { \\mathbb{M}( e ) }"+ , "\\trrule{stuck}"+ , " { \\mathbb{M}( n ) }" , " { T }" , " { }" , " { }"@@ -1050,16 +1049,16 @@ , " { }" , "\\trrule{box}" , " { \\mathbb{D}( [[ B_1, @ -> e, B_2 ]] ) }"- , " { \\mathbb{D}( e_1 ) }"+ , " { \\mathbb{D}( \\mathcal{N}( e_1 ) ) }" , " { if $ [ \\Delta, 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} $ }"+ , " { \\mathbb{D}( n ) }"+ , " { \\mathbb{D}( \\mathbb{M}( n ) ) }"+ , " { if $ n \\notin \\mathcal{P} $ }" , " { }" , "\\trrule{none}"- , " { \\mathbb{D}( e ) }"+ , " { \\mathbb{D}( n ) }" , " { \\varnothing }" , " { }" , " { }"@@ -1157,7 +1156,7 @@ it "builds substitutions with conditions" $ withStdin "{[[ x -> Q.y ]].x}" $ testCLISucceeded- ["match", "--pattern=[[ !a -> Q.y, !B ]].!a", "--when=and(not(alpha(!a)),eq(length(!B),1))"]+ ["match", "--pattern=[[ !a -> Q.y, !B ]].!a", "--when=eq(length(!B),1)"] ["B >> ⟦ ρ ↦ ∅ ⟧\na >> x"] it "builds with condition from file" $
test/CSTSpec.hs view
@@ -64,7 +64,7 @@ let number = BaseObject "number" again = ExPhiAgain Nothing 1 bts = BaseObject "bytes"- bt = BiTau (AtAlpha 0)+ bt = ArAlpha (Alpha 0) app = ExApplication form = ExFormation [BiDelta (BtMany ["40", "18", "00", "00", "00", "00", "00", "00"]), BiVoid AtRho] isCSTNumber (EX_NUMBER{}) = True
test/ConditionSpec.hs view
@@ -5,7 +5,7 @@ module ConditionSpec where -import AST (Attribute (AtLabel, AtMeta), Binding (BiMeta), Expression (ExDispatch, ExGlobal, ExMeta))+import AST (Alpha (AlMeta, Alpha), Attribute (AtLabel, AtMeta), Binding (BiMeta), Expression (ExDispatch, ExMeta, ExRoot)) import Condition import Control.Monad (forM_) import Data.Either (isLeft, isRight)@@ -18,15 +18,12 @@ forM_ [ "in (!a, !B)" , " not (in (!a1, !B)) "- , "alpha(x)" , "eq(1, 1)"- , "or(eq(index(a),1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))"- , "and(alpha(q),eq(-5,21))"+ , "or(eq(index(~0),1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))" , "nf([[ x -> !e ]].x)" , "absolute(!e1)" , "matches(\"hello(\\\"\\u0000)\", !e)" , "part-of ( [[ x -> 1 ]] , !B ) "- , "and(not(alpha(!a)),eq(!a,x))" ] (\expr -> it expr (parseCondition expr `shouldSatisfy` isRight)) @@ -34,12 +31,11 @@ forM_ [ ("in(!a, !B)", Y.In (AtMeta "a") (BiMeta "B")) , ("not(in(!a,!B))", Y.Not (Y.In (AtMeta "a") (BiMeta "B")))- , ("alpha(y)", Y.Alpha (AtLabel "y")) , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2))))- , ("eq(index(z),length(!B1))", Y.Eq (Y.CmpNum (Y.Index (AtLabel "z"))) (Y.CmpNum (Y.Length (BiMeta "B1"))))- , ("eq(index(z),domain(!B1))", Y.Eq (Y.CmpNum (Y.Index (AtLabel "z"))) (Y.CmpNum (Y.Domain (BiMeta "B1"))))+ , ("eq(index(α0),length(!B1))", Y.Eq (Y.CmpNum (Y.Index (Alpha 0))) (Y.CmpNum (Y.Length (BiMeta "B1"))))+ , ("eq(index(!h),domain(!B1))", Y.Eq (Y.CmpNum (Y.Index (AlMeta "h"))) (Y.CmpNum (Y.Domain (BiMeta "B1")))) , ("eq(!a1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "a1")) (Y.CmpExpr (ExMeta "e2")))- , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExGlobal (AtLabel "x"))])+ , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExRoot (AtLabel "x"))]) , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")]) ] (\(expr, res) -> it expr (parseCondition expr `shouldBe` Right res))@@ -48,7 +44,6 @@ forM_ [ "some()" , "in(!a, !a)"- , "alpha(!B)" , "or(or(), or())" ] (\expr -> it expr (parseCondition expr `shouldSatisfy` isLeft))
test/DataizeSpec.hs view
@@ -27,7 +27,7 @@ forM_ useCases $ \(desc, input, expr, output) -> it desc $ do let prog = Program expr- (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExGlobal prog)+ (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExRoot prog) res `shouldBe` output test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> DataizeContext -> IO (a, NonEmpty Rewritten)) -> [(String, Expression, Expression, a)] -> Spec@@ -35,7 +35,7 @@ forM_ useCases $ \(desc, input, expr, output) -> it desc $ do let prog = Program expr- (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExGlobal prog)+ (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExRoot prog) res `shouldBe` output testDataize :: [(String, String, String, Bytes)] -> Spec@@ -52,13 +52,13 @@ describe "morph" $ test' morph- [ ("[[ D> 00- ]] => [[ D> 00- ]]", ExFormation [BiDelta (BtOne "00")], ExGlobal, ExFormation [BiDelta (BtOne "00")])- , ("T => T", ExTermination, ExGlobal, ExTermination)- , ("$ => X", ExThis, ExGlobal, ExTermination)- , ("Q => X", ExGlobal, ExGlobal, ExTermination)+ [ ("[[ D> 00- ]] => [[ D> 00- ]]", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")])+ , ("T => T", ExTermination, ExRoot, ExTermination)+ , ("$ => X", ExXi, ExRoot, ExTermination)+ , ("Q => X", ExRoot, ExRoot, ExTermination) , ( "Q.x (Q -> [[ x -> [[]] ]]) => [[]]"- , ExDispatch ExGlobal (AtLabel "x")+ , ExDispatch ExRoot (AtLabel "x") , ExFormation [BiTau (AtLabel "x") (ExFormation [])] , ExFormation [] )@@ -67,21 +67,15 @@ describe "dataize" $ test dataize'- [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExGlobal, Just (BtOne "00"))- , ("T => X", ExTermination, ExGlobal, Nothing)+ [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExRoot, Just (BtOne "00"))+ , ("T => X", ExTermination, ExRoot, Nothing) , ( "[[ @ -> [[ D> 00-]] ]] => 00-" , ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "00"), BiVoid AtRho]), BiVoid AtRho]- , ExGlobal+ , ExRoot , Just (BtOne "00") ) ,- ( "[[ x -> [[ D> 01- ]] ]].x => 01-"- , ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiDelta (BtOne "01"), BiVoid AtRho]), BiVoid AtRho]) (AtLabel "x")- , ExGlobal- , Just (BtOne "01")- )- , ( "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]] => 01-" , ExFormation [ BiTau@@ -97,14 +91,14 @@ , BiVoid AtRho ] )- (BiTau (AtLabel "y") (ExFormation []))+ (ArTau (AtLabel "y") (ExFormation [])) ) ] ) (AtLabel "x") ) ]- , ExGlobal+ , ExRoot , Just (BtOne "01") ) ]@@ -113,7 +107,7 @@ 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+ term <- execBuildTerm (defaultDataizeContext ExRoot prog) "global" [Yaml.ArgAttribute (AtLabel "x")] substEmpty case term of TeExpression actual -> actual `shouldBe` expected _ -> expectationFailure "global() did not return an expression"@@ -144,6 +138,15 @@ (null orphans) (expectationFailure ("Dataization emitted step labels with no defining rule or operation: " ++ show orphans)) + describe "names every rule uniquely across rule sets" $+ it "shares no rule name between morphing, dataization and normalization" $ do+ let names =+ map (.name) Yaml.morphingRules+ ++ map (.name) Yaml.dataizationRules+ ++ map (.name) Yaml.normalizationRules+ clashes = nub (filter (\n -> length (filter (== n) names) > 1) names)+ clashes `shouldBe` []+ describe "preserves the reduction label sequence" $ do let labelsOf loc src = do prog <- parseProgramThrows src@@ -157,33 +160,32 @@ "Q -> [[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" labels `shouldBe` [ "contextualize"- , "Mphi"+ , "root" , "alpha" , "copy" , "dot" , "copy" , "alpha" , "copy"- , "Mlambda"- , "Mphi"+ , "lambda"+ , "root" , "alpha" , "copy"- , "Mprim"+ , "prim" , "contextualize" , "dot"- , "Mphi"+ , "root" , "alpha" , "copy" , "copy"- , "Mprim"+ , "prim" , "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"]+ labels `shouldBe` ["contextualize", "root", "prim"] testDataize [
test/FunctionsSpec.hs view
@@ -20,9 +20,9 @@ spec :: Spec spec = describe "Functions" $ it "contains only unique bindings after 'join'" $ do- let first = ("B1", MvBindings [BiVoid AtRho, BiDelta BtEmpty, BiTau (AtLabel "x") ExGlobal, BiVoid (AtAlpha 0)])- second = ("B2", MvBindings [BiTau AtRho ExThis, BiLambda "Func", BiDelta (BtOne "00"), BiVoid (AtAlpha 1)])- third = ("B3", MvBindings [BiLambda "Some", BiTau (AtLabel "y") ExThis, BiTau (AtLabel "x") ExThis, BiVoid (AtAlpha 0)])+ let first = ("B1", MvBindings [BiVoid AtRho, BiDelta BtEmpty, BiTau (AtLabel "x") ExRoot, BiVoid (AtLabel "a0")])+ second = ("B2", MvBindings [BiTau AtRho ExXi, BiLambda (Function "Func"), BiDelta (BtOne "00"), BiVoid (AtLabel "a1")])+ third = ("B3", MvBindings [BiLambda (Function "Some"), BiTau (AtLabel "y") ExXi, BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "a0")]) subst = Subst (Map.fromList [first, second, third]) TeBindings bds <- buildTerm "join" [ArgBinding (BiMeta "B1"), ArgBinding (BiMeta "B2"), ArgBinding (BiMeta "B3")] subst bds' <- uniqueBindings' bds
test/MatcherSpec.hs view
@@ -37,45 +37,45 @@ matchExpressionDeep [ ( "Q => [[ @ -> Q, ^ -> Q ]] => [(), ()]"- , ExGlobal- , ExFormation [BiTau AtPhi ExGlobal, BiTau AtRho ExGlobal]+ , ExRoot+ , ExFormation [BiTau AtPhi ExRoot, BiTau AtRho ExRoot] , substs [[], []] ) , ( "Q.!a => [[ @ -> Q.y, ^ -> [[ a -> Q.w ]], @ -> Q.y ]] => [(a >> y), (a >> w), (a >> y)]"- , ExDispatch ExGlobal (AtMeta "a")+ , ExDispatch ExRoot (AtMeta "a") , ExFormation- [ BiTau AtPhi (ExDispatch ExGlobal (AtLabel "y"))- , BiTau AtRho (ExFormation [BiTau (AtLabel "a") (ExDispatch ExGlobal (AtLabel "w"))])- , BiTau AtPhi (ExDispatch ExGlobal (AtLabel "y"))+ [ BiTau AtPhi (ExDispatch ExRoot (AtLabel "y"))+ , BiTau AtRho (ExFormation [BiTau (AtLabel "a") (ExDispatch ExRoot (AtLabel "w"))])+ , BiTau AtPhi (ExDispatch ExRoot (AtLabel "y")) ] , substs [[("a", MvAttribute (AtLabel "y"))], [("a", MvAttribute (AtLabel "w"))], [("a", MvAttribute (AtLabel "y"))]] ) , ( "[[!a -> Q.org.!a]] => [[f -> [[x -> Q.org.x]], t -> [[y -> Q.org.y]] => [(!a >> x), (!a >> y)]"- , ExFormation [BiTau (AtMeta "a") (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtMeta "a"))]+ , ExFormation [BiTau (AtMeta "a") (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtMeta "a"))] , ExFormation- [ BiTau (AtLabel "f") (ExFormation [BiTau (AtLabel "x") (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "x"))])- , BiTau (AtLabel "t") (ExFormation [BiTau (AtLabel "y") (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "y"))])+ [ BiTau (AtLabel "f") (ExFormation [BiTau (AtLabel "x") (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "x"))])+ , BiTau (AtLabel "t") (ExFormation [BiTau (AtLabel "y") (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "y"))]) ] , substs [[("a", MvAttribute (AtLabel "x"))], [("a", MvAttribute (AtLabel "y"))]] ) , ( "!e => [[x -> Q]] => [(!e >> [[x -> Q]] ), (!e >> Q)]" , ExMeta "e"- , ExFormation [BiTau (AtLabel "x") ExGlobal]+ , ExFormation [BiTau (AtLabel "x") ExRoot] , substs- [ [("e", MvExpression (ExFormation [BiTau (AtLabel "x") ExGlobal]))]- , [("e", MvExpression ExGlobal)]+ [ [("e", MvExpression (ExFormation [BiTau (AtLabel "x") ExRoot]))]+ , [("e", MvExpression ExRoot)] ] ) , ( "!e.!a => Q.org.eolang => [(!e >> Q.org, !a >> eolang), (!e >> Q, !a >> org)]" , ExDispatch (ExMeta "e") (AtMeta "a")- , ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")+ , ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang") , substs- [ [("e", MvExpression (ExDispatch ExGlobal (AtLabel "org"))), ("a", MvAttribute (AtLabel "eolang"))]- , [("e", MvExpression ExGlobal), ("a", MvAttribute (AtLabel "org"))]+ [ [("e", MvExpression (ExDispatch ExRoot (AtLabel "org"))), ("a", MvAttribute (AtLabel "eolang"))]+ , [("e", MvExpression ExRoot), ("a", MvAttribute (AtLabel "org"))] ] ) ,@@ -84,23 +84,23 @@ , ExApplication ( ExDispatch ( ExFormation- [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))+ [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t")) , BiVoid (AtLabel "t") ] ) (AtLabel "t") )- ( BiTau+ ( ArTau AtRho ( ExFormation- [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))+ [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t")) , BiVoid (AtLabel "t") ] ) ) , substs [- [ ("B1", MvBindings [BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))])+ [ ("B1", MvBindings [BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t"))]) , ("a", MvAttribute (AtLabel "t")) , ("B2", MvBindings []) ]@@ -128,22 +128,22 @@ [ BiTau (AtLabel "i1") ( ExFormation- [ BiTau (AtLabel "a") ExGlobal- , BiTau (AtLabel "b") ExThis+ [ BiTau (AtLabel "a") ExRoot+ , BiTau (AtLabel "b") ExXi ] ) , BiTau (AtLabel "i2") ( ExFormation- [ BiTau (AtLabel "a") ExGlobal+ [ BiTau (AtLabel "a") ExRoot , BiTau (AtLabel "b") (ExFormation [BiVoid AtPhi]) ] ) ] , substs [- [ ("e0", MvExpression ExGlobal)- , ("e-first", MvExpression ExThis)+ [ ("e0", MvExpression ExRoot)+ , ("e-first", MvExpression ExXi) , ("e-second", MvExpression (ExFormation [BiVoid AtPhi])) ] ]@@ -152,15 +152,22 @@ describe "matchAttribute: attribute => attribute => substitution" $ forM_- [ ("~1 => ~1 => [()]", AtAlpha 1, AtAlpha 1, substs [[]])- , ("!a => ^ => [(!a >> ^)]", AtMeta "a", AtRho, substs [[("a", MvAttribute AtRho)]])+ [ ("!a => ^ => [(!a >> ^)]", AtMeta "a", AtRho, substs [[("a", MvAttribute AtRho)]]) , ("!a => @ => [(!a >> @)]", AtMeta "a", AtPhi, substs [[("a", MvAttribute AtPhi)]])- , ("~0 => [] => [()]", AtAlpha 0, AtLabel "x", substs []) ] ( \(desc, ptn, tgt, expected) -> it desc $ matchAttribute ptn tgt `shouldBe` expected ) + describe "matchAlpha: alpha => alpha => substitution" $+ forM_+ [ ("α1 => α1 => [()]", Alpha 1, Alpha 1, substs [[]])+ , ("α0 => α1 => []", Alpha 0, Alpha 1, substs [])+ ]+ ( \(desc, ptn, tgt, expected) ->+ it desc $ matchAlpha ptn tgt `shouldBe` expected+ )+ describe "matchBindings: [binding] => [binding] => substitution" $ test matchBindings@@ -173,13 +180,13 @@ , ( "[[!B]] => T:[[x -> ?, D> 01-, L> Func]] => (!B >> T)" , [BiMeta "B"]- , [BiVoid (AtLabel "x"), BiDelta (BtOne "01"), BiLambda "Func"]- , substs [[("B", MvBindings [BiVoid (AtLabel "x"), BiDelta (BtOne "01"), BiLambda "Func"])]]+ , [BiVoid (AtLabel "x"), BiDelta (BtOne "01"), BiLambda (Function "Func")]+ , substs [[("B", MvBindings [BiVoid (AtLabel "x"), BiDelta (BtOne "01"), BiLambda (Function "Func")])]] ) , ( "[[D> 00-]] => [[D> 00-, L> Func]] => []" , [BiDelta (BtOne "00")]- , [BiDelta (BtOne "00"), BiLambda "Func"]+ , [BiDelta (BtOne "00"), BiLambda (Function "Func")] , substs [] ) ,@@ -203,8 +210,8 @@ , ( "[[!B1, !x -> ?, !B2]] => [[y -> ?, D> -> 00-, L> Func]] => (!x >> y, !B1 >> [[]], !B2 >> [[D> -> 00-, L> Func]])" , [BiMeta "B1", BiVoid (AtMeta "x"), BiMeta "B2"]- , [BiVoid (AtLabel "y"), BiDelta (BtOne "00"), BiLambda "Func"]- , substs [[("B1", MvBindings []), ("B2", MvBindings [BiDelta (BtOne "00"), BiLambda "Func"]), ("x", MvAttribute (AtLabel "y"))]]+ , [BiVoid (AtLabel "y"), BiDelta (BtOne "00"), BiLambda (Function "Func")]+ , substs [[("B1", MvBindings []), ("B2", MvBindings [BiDelta (BtOne "00"), BiLambda (Function "Func")]), ("x", MvAttribute (AtLabel "y"))]] ) , ( "[[!x -> ?, !y -> ?]] => [[a -> ?, b -> ?]] => (!x >> a, !y >> b)"@@ -215,19 +222,19 @@ , ( "[[t -> ?, !B]] => [[t -> ?, x -> Q, y -> $]] => (!B >> [[x -> Q, y -> $]])" , [BiVoid (AtLabel "t"), BiMeta "B"]- , [BiVoid (AtLabel "t"), BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis]- , substs [[("B", MvBindings [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis])]]+ , [BiVoid (AtLabel "t"), BiTau (AtLabel "x") ExRoot, BiTau (AtLabel "y") ExXi]+ , substs [[("B", MvBindings [BiTau (AtLabel "x") ExRoot, BiTau (AtLabel "y") ExXi])]] ) , ( "[[!B, z -> Q]] => [[x -> Q, y -> $, z -> Q]] => (!B >> [[x -> Q, y -> $]])"- , [BiMeta "B", BiTau (AtLabel "z") ExGlobal]- , [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis, BiTau (AtLabel "z") ExGlobal]- , substs [[("B", MvBindings [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis])]]+ , [BiMeta "B", BiTau (AtLabel "z") ExRoot]+ , [BiTau (AtLabel "x") ExRoot, BiTau (AtLabel "y") ExXi, BiTau (AtLabel "z") ExRoot]+ , substs [[("B", MvBindings [BiTau (AtLabel "x") ExRoot, BiTau (AtLabel "y") ExXi])]] ) , ( "[[L> Func, D> 00-]] => [[D> 00-, L> Func]] => []"- , [BiLambda "Func", BiDelta (BtOne "00")]- , [BiDelta (BtOne "00"), BiLambda "Func"]+ , [BiLambda (Function "Func"), BiDelta (BtOne "00")]+ , [BiDelta (BtOne "00"), BiLambda (Function "Func")] , substs [] ) ,@@ -352,98 +359,122 @@ describe "matchExpression: expression => pattern => substitution" $ test matchExpression'- [ ("$ => $ => [()]", ExThis, ExThis, substs [[]])- , ("Q => Q => [()]", ExGlobal, ExGlobal, substs [[]])+ [ ("$ => $ => [()]", ExXi, ExXi, substs [[]])+ , ("Q => Q => [()]", ExRoot, ExRoot, substs [[]]) , ( "!e => Q => [(!e >> Q)]" , ExMeta "e"- , ExGlobal- , substs [[("e", MvExpression ExGlobal)]]+ , ExRoot+ , substs [[("e", MvExpression ExRoot)]] ) ,+ ( "!p => T => [(!p >> T)]"+ , ExMeta "p"+ , ExTermination+ , substs [[("p", MvExpression ExTermination)]]+ )+ ,+ ( "!p => [[ x -> Q ]] => [(!p >> [[ x -> Q ]])]"+ , ExMeta "p"+ , ExFormation [BiTau (AtLabel "x") ExRoot]+ , substs [[("p", MvExpression (ExFormation [BiTau (AtLabel "x") ExRoot]))]]+ )+ ,+ ( "!p => Q => []"+ , ExMeta "p"+ , ExRoot+ , substs []+ )+ ,+ ( "!p => [[ L> Func ]] => []"+ , ExMeta "p"+ , ExFormation [BiLambda (Function "Func")]+ , substs []+ )+ , ( "!e => Q.org(x -> $) => [(!e >> Q.org(x -> $))]" , ExMeta "e"- , ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") ExThis)- , substs [[("e", MvExpression (ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") ExThis)))]]+ , ExApplication (ExDispatch ExRoot (AtLabel "org")) (ArTau (AtLabel "x") ExXi)+ , substs [[("e", MvExpression (ExApplication (ExDispatch ExRoot (AtLabel "org")) (ArTau (AtLabel "x") ExXi)))]] ) , ( "!e1.x => Q.org.x => [(!e1 >> Q.org)]" , ExDispatch (ExMeta "e1") (AtLabel "x")- , ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "x")- , substs [[("e1", MvExpression (ExDispatch ExGlobal (AtLabel "org")))]]+ , ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "x")+ , substs [[("e1", MvExpression (ExDispatch ExRoot (AtLabel "org")))]] ) , ( "!e.org.!a => $.org.x => [(!e >> $, !a >> x)]" , ExDispatch (ExDispatch (ExMeta "e") (AtLabel "org")) (AtMeta "a")- , ExDispatch (ExDispatch ExThis (AtLabel "org")) (AtLabel "x")- , substs [[("e", MvExpression ExThis), ("a", MvAttribute (AtLabel "x"))]]+ , ExDispatch (ExDispatch ExXi (AtLabel "org")) (AtLabel "x")+ , substs [[("e", MvExpression ExXi), ("a", MvAttribute (AtLabel "x"))]] ) , ( "[[!a -> !e, !B]].!a => [[x -> Q, y -> $]].x => [(!a >> x, !e >> Q, !B >> [y -> $])]" , ExDispatch (ExFormation [BiTau (AtMeta "a") (ExMeta "e"), BiMeta "B"]) (AtMeta "a") , ExDispatch ( ExFormation- [ BiTau (AtLabel "x") ExGlobal- , BiTau (AtLabel "y") ExThis+ [ BiTau (AtLabel "x") ExRoot+ , BiTau (AtLabel "y") ExXi ] ) (AtLabel "x") , substs [ [ ("a", MvAttribute (AtLabel "x"))- , ("e", MvExpression ExGlobal)- , ("B", MvBindings [BiTau (AtLabel "y") ExThis])+ , ("e", MvExpression ExRoot)+ , ("B", MvBindings [BiTau (AtLabel "y") ExXi]) ] ] ) , ( "Q * !t => Q.org => [(!t >> [.org])]"- , ExMetaTail ExGlobal "t"- , ExDispatch ExGlobal (AtLabel "x")+ , ExMetaTail ExRoot "t"+ , ExDispatch ExRoot (AtLabel "x") , substs [[("t", MvTail [TaDispatch (AtLabel "x")])]] ) , ( "Q * !t => Q.org(x -> [[]]) => [(!t >> [.org, (x -> [[]])])]"- , ExMetaTail ExGlobal "t"- , ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))- , substs [[("t", MvTail [TaDispatch (AtLabel "org"), TaApplication (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]]+ , ExMetaTail ExRoot "t"+ , ExApplication (ExDispatch ExRoot (AtLabel "org")) (ArTau (AtLabel "x") (ExFormation [BiVoid AtRho]))+ , substs [[("t", MvTail [TaDispatch (AtLabel "org"), TaApplication (ArTau (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]))])]]+ , ExMetaTail (ExDispatch ExRoot (AtLabel "x")) "t"+ , ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") (ExFormation [BiVoid AtRho]))+ , substs [[("t", MvTail [TaApplication (ArTau (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]))- , substs [[("a", MvAttribute (AtLabel "org")), ("t", MvTail [TaDispatch (AtLabel "eolang"), TaApplication (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]]+ , ExMetaTail (ExDispatch ExRoot (AtMeta "a")) "t"+ , ExApplication (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")) (ArTau (AtLabel "x") (ExFormation [BiVoid AtRho]))+ , substs [[("a", MvAttribute (AtLabel "org")), ("t", MvTail [TaDispatch (AtLabel "eolang"), TaApplication (ArTau (AtLabel "x") (ExFormation [BiVoid AtRho]))])]] ) , ( "Q.x(y -> $ * !t1) * !t2 => Q.x(y -> $.q).p => [(!t1 >> [.q], !t2 >> [.p])]"- , ExMetaTail (ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") (ExMetaTail ExThis "t1"))) "t2"- , ExDispatch (ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") (ExDispatch ExThis (AtLabel "q")))) (AtLabel "p")+ , ExMetaTail (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") (ExMetaTail ExXi "t1"))) "t2"+ , ExDispatch (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") (ExDispatch ExXi (AtLabel "q")))) (AtLabel "p") , substs [[("t1", MvTail [TaDispatch (AtLabel "q")]), ("t2", MvTail [TaDispatch (AtLabel "p")])]] ) , ( "[[!B1, !a ↦ !e1, !B2]](!a ↦ !e2) => ⟦ t ↦ ξ.k, x ↦ ξ.t, k ↦ ∅ ⟧(x ↦ ξ) => [(!B1 >> [[ t -> $.k ]], !a >> x, !B2 >> [[ k -> ? ]], !e1 >> $.t, !e2 >> $)]"- , ExApplication (ExFormation [BiMeta "B1", BiTau (AtMeta "a") (ExMeta "e1"), BiMeta "B2"]) (BiTau (AtMeta "a") (ExMeta "e2"))+ , ExApplication (ExFormation [BiMeta "B1", BiTau (AtMeta "a") (ExMeta "e1"), BiMeta "B2"]) (ArTau (AtMeta "a") (ExMeta "e2")) , ExApplication ( ExFormation- [ BiTau (AtLabel "t") (ExDispatch ExThis (AtLabel "k"))- , BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))+ [ BiTau (AtLabel "t") (ExDispatch ExXi (AtLabel "k"))+ , BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t")) , BiVoid (AtLabel "k") ] )- (BiTau (AtLabel "x") ExThis)+ (ArTau (AtLabel "x") ExXi) , substs [- [ ("B1", MvBindings [BiTau (AtLabel "t") (ExDispatch ExThis (AtLabel "k"))])+ [ ("B1", MvBindings [BiTau (AtLabel "t") (ExDispatch ExXi (AtLabel "k"))]) , ("a", MvAttribute (AtLabel "x")) , ("B2", MvBindings [BiVoid (AtLabel "k")])- , ("e1", MvExpression (ExDispatch ExThis (AtLabel "t")))- , ("e2", MvExpression ExThis)+ , ("e1", MvExpression (ExDispatch ExXi (AtLabel "t")))+ , ("e2", MvExpression ExXi) ] ] )
test/MiscSpec.hs view
@@ -32,8 +32,8 @@ ) , ( "[[^ -> Q.x, x -> $.y]] => [[^ -> Q.x, x -> $.y]]"- , [BiTau AtRho (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]- , [BiTau AtRho (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]+ , [BiTau AtRho (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]+ , [BiTau AtRho (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))] ) , ("[[!B]] => [[!B]]", [BiMeta "B"], [BiMeta "B"]) , ("[[x -> ?, !B]] => [[x -> ?, !B]]", [BiVoid (AtLabel "x"), BiMeta "B"], [BiVoid (AtLabel "x"), BiMeta "B"])@@ -54,8 +54,8 @@ ) , ( "[[!a -> Q.x, x -> $.y]] => [[!a -> Q.x, x -> $.y]]"- , [BiTau (AtMeta "a") (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]- , [BiTau (AtMeta "a") (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]+ , [BiTau (AtMeta "a") (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]+ , [BiTau (AtMeta "a") (ExDispatch ExRoot (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))] ) ]
test/ParserSpec.hs view
@@ -32,44 +32,44 @@ test parseProgram [ ("Q -> [[]]", Just (Program (ExFormation [BiVoid AtRho])))- , ("Q -> T(x -> Q)", Just (Program (ExApplication ExTermination (BiTau (AtLabel "x") ExGlobal))))- , ("Q -> Q.org.eolang", Just (Program (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"))))- , ("Q -> [[x -> $, y -> ?]]", Just (Program (ExFormation [BiTau (AtLabel "x") ExThis, BiVoid (AtLabel "y"), BiVoid AtRho])))+ , ("Q -> T(x -> Q)", Just (Program (ExApplication ExTermination (ArTau (AtLabel "x") ExRoot))))+ , ("Q -> Q.org.eolang", Just (Program (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang"))))+ , ("Q -> [[x -> $, y -> ?]]", Just (Program (ExFormation [BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "y"), BiVoid AtRho]))) ] describe "parse expression" $ test parseExpression- [ ("Q.!a", Just (ExDispatch ExGlobal (AtMeta "a")))- , ("[[]](!a1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtMeta "a1") ExThis)))+ [ ("Q.!a", Just (ExDispatch ExRoot (AtMeta "a")))+ , ("[[]](!a1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtMeta "a1") ExXi))) , ( "[[]](~0 -> $)(~11 -> Q)" , Just ( ExApplication ( ExApplication (ExFormation [BiVoid AtRho])- (BiTau (AtAlpha 0) ExThis)+ (ArAlpha (Alpha 0) ExXi) )- (BiTau (AtAlpha 11) ExGlobal)+ (ArAlpha (Alpha 11) ExRoot) ) )- , ("[[]](x -> $, y -> Q)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtLabel "x") ExThis)) (BiTau (AtLabel "y") ExGlobal)))+ , ("[[]](x -> $, y -> Q)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtLabel "x") ExXi)) (ArTau (AtLabel "y") ExRoot))) , ("[[!B, !B1]]", Just (ExFormation [BiMeta "B", BiMeta "B1"]))- , ("[[!B2, !a2 -> $]]", Just (ExFormation [BiMeta "B2", BiTau (AtMeta "a2") ExThis]))+ , ("[[!B2, !a2 -> $]]", Just (ExFormation [BiMeta "B2", BiTau (AtMeta "a2") ExXi])) , ("!e0", Just (ExMeta "e0")) , ("!k", Just (ExMeta "k")) , ("[[x -> !k1]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "k1"), BiVoid AtRho])) , ("[[x -> !e]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "e"), BiVoid AtRho])) , ("[[!a -> !e1]]", Just (ExFormation [BiTau (AtMeta "a") (ExMeta "e1")]))- , ("Q * !t", Just (ExMetaTail ExGlobal "t"))- , ("[[]](x -> $) * !t1", Just (ExMetaTail (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtLabel "x") ExThis)) "t1"))+ , ("Q * !t", Just (ExMetaTail ExRoot "t"))+ , ("[[]](x -> $) * !t1", Just (ExMetaTail (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtLabel "x") ExXi)) "t1")) , ("[[D> --]]", Just (ExFormation [BiDelta BtEmpty, BiVoid AtRho])) , ("[[D> 1F-]]", Just (ExFormation [BiDelta (BtOne "1F"), BiVoid AtRho]))- , ("[[\n L> Func,\n D> 00-\n]]", Just (ExFormation [BiLambda "Func", BiDelta (BtOne "00"), BiVoid AtRho]))+ , ("[[\n L> Func,\n D> 00-\n]]", Just (ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00"), BiVoid AtRho])) , ("[[D> 1F-2A-00]]", Just (ExFormation [BiDelta (BtMany ["1F", "2A", "00"]), BiVoid AtRho])) , ("[[D> !d0]]", Just (ExFormation [BiDelta (BtMeta "d0"), BiVoid AtRho]))- , ("[[L> Function]]", Just (ExFormation [BiLambda "Function", BiVoid AtRho]))- , ("[[L> !F3]]", Just (ExFormation [BiMetaLambda "F3", BiVoid AtRho]))+ , ("[[L> Function]]", Just (ExFormation [BiLambda (Function "Function"), BiVoid AtRho]))+ , ("[[L> !F3]]", Just (ExFormation [BiLambda (FnMeta "F3"), BiVoid AtRho])) , ("[[x() -> [[]] ]]", Just (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])) , ( "[[y(^,@,z) -> [[q -> Q.a]] ]]"@@ -81,7 +81,7 @@ [ BiVoid AtRho , BiVoid AtPhi , BiVoid (AtLabel "z")- , BiTau (AtLabel "q") (ExDispatch ExGlobal (AtLabel "a"))+ , BiTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "a")) ] ) , BiVoid AtRho@@ -93,7 +93,7 @@ , Just ( ExApplication (ExMeta "e")- ( BiTau+ ( ArTau (AtLabel "x") ( ExFormation [ BiVoid AtRho@@ -110,16 +110,16 @@ ( ExFormation [ BiTau (AtLabel "x")- (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z"))+ (ExDispatch (ExDispatch ExXi (AtLabel "y")) (AtLabel "z")) , BiTau (AtLabel "w")- (ExDispatch ExThis AtRho)+ (ExDispatch ExXi AtRho) , BiTau (AtLabel "u")- (ExDispatch ExThis AtPhi)+ (ExDispatch ExXi AtPhi) , BiTau (AtLabel "p")- (ExDispatch ExThis (AtMeta "a"))+ (ExDispatch ExXi (AtMeta "a")) , BiTau (AtLabel "q") (ExMeta "e")@@ -133,19 +133,19 @@ ( ExApplication ( ExApplication ( ExApplication- (ExDispatch ExGlobal (AtLabel "x"))- (BiTau (AtAlpha 0) (ExDispatch ExThis (AtLabel "y")))+ (ExDispatch ExRoot (AtLabel "x"))+ (ArAlpha (Alpha 0) (ExDispatch ExXi (AtLabel "y"))) )- (BiTau (AtAlpha 1) (ExDispatch (ExFormation [BiVoid AtRho]) (AtLabel "z")))+ (ArAlpha (Alpha 1) (ExDispatch (ExFormation [BiVoid AtRho]) (AtLabel "z"))) )- ( BiTau- (AtAlpha 2)+ ( ArAlpha+ (Alpha 2) ( ExApplication ( ExApplication- (ExDispatch ExGlobal (AtLabel "y"))- (BiTau (AtAlpha 0) (ExDispatch ExThis AtRho))+ (ExDispatch ExRoot (AtLabel "y"))+ (ArAlpha (Alpha 0) (ExDispatch ExXi AtRho)) )- (BiTau (AtAlpha 1) (ExDispatch ExThis AtPhi))+ (ArAlpha (Alpha 1) (ExDispatch ExXi AtPhi)) ) ) )@@ -158,15 +158,15 @@ (DataNumber (BtMany ["40", "14", "00", "00", "00", "00", "00", "00"])) (AtLabel "plus") )- ( BiTau- (AtAlpha 0)+ ( ArAlpha+ (Alpha 0) ( ExApplication ( ExDispatch (DataNumber (BtMany ["40", "14", "00", "00", "00", "00", "00", "00"])) (AtLabel "q") )- ( BiTau- (AtAlpha 0)+ ( ArAlpha+ (Alpha 0) ( ExDispatch (DataString (BtMany ["68", "65", "6C", "6C", "6F"])) (AtLabel "length")@@ -181,7 +181,7 @@ , Just ( ExFormation [ BiMeta "B1"- , BiTau (AtMeta "a0") ExThis+ , BiTau (AtMeta "a0") ExXi , BiTau (AtLabel "x") (ExMeta "e") ] )@@ -287,28 +287,28 @@ describe "parse binding" $ test parseBinding- [ ("x -> $", Just (BiTau (AtLabel "x") ExThis))- , ("y -> Q", Just (BiTau (AtLabel "y") ExGlobal))+ [ ("x -> $", Just (BiTau (AtLabel "x") ExXi))+ , ("y -> Q", Just (BiTau (AtLabel "y") ExRoot)) , ("z -> ?", Just (BiVoid (AtLabel "z"))) , ("w -> ∅", Just (BiVoid (AtLabel "w"))) , ("^ -> T", Just (BiTau AtRho ExTermination))- , ("@ -> $", Just (BiTau AtPhi ExThis))- , ("ρ -> Q", Just (BiTau AtRho ExGlobal))+ , ("@ -> $", Just (BiTau AtPhi ExXi))+ , ("ρ -> Q", Just (BiTau AtRho ExRoot)) , ("φ -> T", Just (BiTau AtPhi ExTermination))- , ("!a -> $", Just (BiTau (AtMeta "a") ExThis))- , ("!a0 -> Q", Just (BiTau (AtMeta "a0") ExGlobal))+ , ("!a -> $", Just (BiTau (AtMeta "a") ExXi))+ , ("!a0 -> Q", Just (BiTau (AtMeta "a0") ExRoot)) , ("D> --", Just (BiDelta BtEmpty)) , ("D> 42-", Just (BiDelta (BtOne "42"))) , ("D> 01-02-03", Just (BiDelta (BtMany ["01", "02", "03"]))) , ("D> !d", Just (BiDelta (BtMeta "d"))) , ("Δ ⤍ FF-", Just (BiDelta (BtOne "FF"))) , ("Δ ⤍ --", Just (BiDelta BtEmpty))- , ("L> Func", Just (BiLambda "Func"))- , ("L> Function_name", Just (BiLambda "Function_name"))- , ("L> Aφ", Just (BiLambda "Aφ"))- , ("λ ⤍ Test", Just (BiLambda "Test"))- , ("L> !F", Just (BiMetaLambda "F"))- , ("L> !F0", Just (BiMetaLambda "F0"))+ , ("L> Func", Just (BiLambda (Function "Func")))+ , ("L> Function_name", Just (BiLambda (Function "Function_name")))+ , ("L> Aφ", Just (BiLambda (Function "Aφ")))+ , ("λ ⤍ Test", Just (BiLambda (Function "Test")))+ , ("L> !F", Just (BiLambda (FnMeta "F")))+ , ("L> !F0", Just (BiLambda (FnMeta "F0"))) , ("!B", Just (BiMeta "B")) , ("!B0", Just (BiMeta "B0")) , ("!B_test", Just (BiMeta "B_test"))@@ -317,8 +317,8 @@ , ("x() -> [[]]", Just (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]))) , ("y(^) -> [[]]", Just (BiTau (AtLabel "y") (ExFormation [BiVoid AtRho]))) , ("z(^, @) -> [[]]", Just (BiTau (AtLabel "z") (ExFormation [BiVoid AtRho, BiVoid AtPhi])))- , ("x -> [[y -> $]]", Just (BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExThis, BiVoid AtRho])))- , ("x ↦ ξ", Just (BiTau (AtLabel "x") ExThis))+ , ("x -> [[y -> $]]", Just (BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExXi, BiVoid AtRho])))+ , ("x ↦ ξ", Just (BiTau (AtLabel "x") ExXi)) , ("x -> ", Nothing) , ("-> Q", Nothing) , ("L>", Nothing)@@ -342,11 +342,11 @@ , ("!a_test", Just (AtMeta "a_test")) , ("𝜏", Just (AtMeta "a")) , ("𝜏0", Just (AtMeta "a0"))- , ("~0", Just (AtAlpha 0))- , ("~1", Just (AtAlpha 1))- , ("~123", Just (AtAlpha 123))- , ("α0", Just (AtAlpha 0))- , ("α42", Just (AtAlpha 42))+ , ("~0", Nothing)+ , ("~1", Nothing)+ , ("~123", Nothing)+ , ("α0", Nothing)+ , ("α42", Nothing) , ("X", Nothing) , ("123", Nothing) , ("", Nothing)@@ -384,7 +384,7 @@ describe "parseExpressionThrows" $ do it "returns expression on valid input" $- parseExpressionThrows "Q.x" `shouldReturn` ExDispatch ExGlobal (AtLabel "x")+ parseExpressionThrows "Q.x" `shouldReturn` ExDispatch ExRoot (AtLabel "x") it "throws on invalid input" $ parseExpressionThrows "[[invalid" `shouldThrow` anyException @@ -426,24 +426,24 @@ describe "parse unicode syntax" $ test parseExpression- [ ("ξ", Just ExThis)- , ("Φ", Just ExGlobal)+ [ ("ξ", Just ExXi)+ , ("Φ", Just ExRoot) , ("⊥", Just ExTermination) , ("⟦⟧", Just (ExFormation [BiVoid AtRho]))- , ("⟦ x ↦ ξ ⟧", Just (ExFormation [BiTau (AtLabel "x") ExThis, BiVoid AtRho]))- , ("ξ.ρ", Just (ExDispatch ExThis AtRho))- , ("ξ.φ", Just (ExDispatch ExThis AtPhi))+ , ("⟦ x ↦ ξ ⟧", Just (ExFormation [BiTau (AtLabel "x") ExXi, BiVoid AtRho]))+ , ("ξ.ρ", Just (ExDispatch ExXi AtRho))+ , ("ξ.φ", Just (ExDispatch ExXi AtPhi)) ] describe "parse labels with special characters" $ test parseExpression- [ ("foo123", Just (ExDispatch ExThis (AtLabel "foo123")))- , ("with-dash", Just (ExDispatch ExThis (AtLabel "with-dash")))- , ("with_underscore", Just (ExDispatch ExThis (AtLabel "with_underscore")))- , ("aкирилиця", Just (ExDispatch ExThis (AtLabel "aкирилиця")))- , ("a日本語", Just (ExDispatch ExThis (AtLabel "a日本語")))- , ("name123_test", Just (ExDispatch ExThis (AtLabel "name123_test")))+ [ ("foo123", Just (ExDispatch ExXi (AtLabel "foo123")))+ , ("with-dash", Just (ExDispatch ExXi (AtLabel "with-dash")))+ , ("with_underscore", Just (ExDispatch ExXi (AtLabel "with_underscore")))+ , ("aкирилиця", Just (ExDispatch ExXi (AtLabel "aкирилиця")))+ , ("a日本語", Just (ExDispatch ExXi (AtLabel "a日本語")))+ , ("name123_test", Just (ExDispatch ExXi (AtLabel "name123_test"))) ] describe "parse complex formations" $@@ -452,16 +452,16 @@ [ ("[[^ -> ?]]", Just (ExFormation [BiVoid AtRho])) , ("[[@ -> ?]]", Just (ExFormation [BiVoid AtPhi, BiVoid AtRho])) , ("[[^ -> ?, @ -> ?]]", Just (ExFormation [BiVoid AtRho, BiVoid AtPhi]))- , ("[[^ -> Q, @ -> $]]", Just (ExFormation [BiTau AtRho ExGlobal, BiTau AtPhi ExThis]))+ , ("[[^ -> Q, @ -> $]]", Just (ExFormation [BiTau AtRho ExRoot, BiTau AtPhi ExXi])) ] describe "parse applications with mixed bindings" $ test parseExpression- [ ("[[]](Q)", Just (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtAlpha 0) ExGlobal)))- , ("[[]](Q, T)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtAlpha 0) ExGlobal)) (BiTau (AtAlpha 1) ExTermination)))- , ("Q.x(y -> $)", Just (ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") ExThis)))- , ("[[x -> ?]].x(Q)", Just (ExApplication (ExDispatch (ExFormation [BiVoid (AtLabel "x"), BiVoid AtRho]) (AtLabel "x")) (BiTau (AtAlpha 0) ExGlobal)))+ [ ("[[]](Q)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) ExRoot)))+ , ("[[]](Q, T)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) ExRoot)) (ArAlpha (Alpha 1) ExTermination)))+ , ("Q.x(y -> $)", Just (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") ExXi)))+ , ("[[x -> ?]].x(Q)", Just (ExApplication (ExDispatch (ExFormation [BiVoid (AtLabel "x"), BiVoid AtRho]) (AtLabel "x")) (ArAlpha (Alpha 0) ExRoot))) ] describe "parse meta expressions" $@@ -473,7 +473,7 @@ , ("𝑒", Just (ExMeta "e")) , ("𝑒0", Just (ExMeta "e0")) , ("!e.x", Just (ExDispatch (ExMeta "e") (AtLabel "x")))- , ("!e(Q)", Just (ExApplication (ExMeta "e") (BiTau (AtAlpha 0) ExGlobal)))+ , ("!e(Q)", Just (ExApplication (ExMeta "e") (ArAlpha (Alpha 0) ExRoot))) , ("!n", Just (ExMeta "n")) , ("!n1", Just (ExMeta "n1")) , ("𝑛", Just (ExMeta "n"))@@ -484,8 +484,8 @@ describe "parse meta tails" $ test parseExpression- [ ("Q * !t", Just (ExMetaTail ExGlobal "t"))- , ("Q.x * !t", Just (ExMetaTail (ExDispatch ExGlobal (AtLabel "x")) "t"))+ [ ("Q * !t", Just (ExMetaTail ExRoot "t"))+ , ("Q.x * !t", Just (ExMetaTail (ExDispatch ExRoot (AtLabel "x")) "t")) , ("[[]].y * !t0", Just (ExMetaTail (ExDispatch (ExFormation [BiVoid AtRho]) (AtLabel "y")) "t0")) , ("Q * !t * !t2", Nothing) ]
test/PrinterSpec.hs view
@@ -26,40 +26,38 @@ spec = do describe "printExpression with ASCII singleline renders primitives" $ forM_- [ ("ξ renders as $", ExThis, "$")- , ("Φ renders as Q", ExGlobal, "Q")+ [ ("ξ renders as $", ExXi, "$")+ , ("Φ renders as Q", ExRoot, "Q") , ("⊥ renders as T", ExTermination, "T") , ("ρ void becomes empty", ExFormation [BiVoid AtRho], "[[]]") , ("φ void", ExFormation [BiVoid AtPhi], "[[ @ -> ? ]]") , ("label void", ExFormation [BiVoid (AtLabel "名前")], "[[ 名前 -> ? ]]")- , ("x to Φ", ExFormation [BiTau (AtLabel "x") ExGlobal], "[[ x -> Q ]]")- , ("α0 to ξ", ExFormation [BiTau (AtAlpha 0) ExThis], "[[ ~0 -> $ ]]")+ , ("x to Φ", ExFormation [BiTau (AtLabel "x") ExRoot], "[[ x -> Q ]]") , ("ρ to ⊥", ExFormation [BiTau AtRho ExTermination], "[[ ^ -> T ]]") , ("empty delta", ExFormation [BiDelta BtEmpty], "[[ D> -- ]]") , ("single byte", ExFormation [BiDelta (BtOne "1F")], "[[ D> 1F- ]]") , ("multiple bytes", ExFormation [BiDelta (BtMany ["00", "01", "02"])], "[[ D> 00-01-02 ]]")- , ("función lambda", ExFormation [BiLambda "Función"], "[[ L> Función ]]")- , ("クラス lambda", ExFormation [BiLambda "クラス"], "[[ L> クラス ]]")- , ("Φ.org", ExDispatch ExGlobal (AtLabel "org"), "Q.org")- , ("ξ.ρ as sugar", ExDispatch ExThis AtRho, "^")- , ("ξ.φ as sugar", ExDispatch ExThis AtPhi, "@")- , ("chained dispatch", ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "éolang"), "Q.org.éolang")- , ("ξ.α0 as sugar", ExDispatch ExThis (AtAlpha 0), "~0")+ , ("función lambda", ExFormation [BiLambda (Function "Función")], "[[ L> Función ]]")+ , ("クラス lambda", ExFormation [BiLambda (Function "クラス")], "[[ L> クラス ]]")+ , ("Φ.org", ExDispatch ExRoot (AtLabel "org"), "Q.org")+ , ("ξ.ρ as sugar", ExDispatch ExXi AtRho, "^")+ , ("ξ.φ as sugar", ExDispatch ExXi AtPhi, "@")+ , ("chained dispatch", ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "éolang"), "Q.org.éolang") , ( "dispatch with app"- , ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") ExThis)+ , ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") ExXi) , "Q.x( y -> $ )" ) , ( "formation with app"- , ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtAlpha 0) ExGlobal)+ , ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) ExRoot) , "[[]]( Q )" ) , ("meta expr", ExMeta "e", "!e")- , ("meta tail", ExMetaTail ExGlobal "t", "Q * !t")+ , ("meta tail", ExMetaTail ExRoot "t", "Q * !t") , ("meta binding", ExFormation [BiMeta "B"], "[[ !B ]]")- , ("meta lambda", ExFormation [BiMetaLambda "F"], "[[ L> !F ]]")- , ("meta attr tau", ExFormation [BiTau (AtMeta "a") ExThis], "[[ !a -> $ ]]")+ , ("meta lambda", ExFormation [BiLambda (FnMeta "F")], "[[ L> !F ]]")+ , ("meta attr tau", ExFormation [BiTau (AtMeta "a") ExXi], "[[ !a -> $ ]]") ] ( \(desc, expr, expected) -> it desc (printExpression' expr (SWEET, ASCII, SINGLELINE, defaultMargin) `shouldBe` expected)@@ -84,7 +82,7 @@ describe "printProgram with default config" $ forM_ [ ("empty formation", Program (ExFormation [BiVoid AtRho]), "{⟦⟧}")- , ("dispatch", Program (ExDispatch ExGlobal (AtLabel "org")), "{Φ.org}")+ , ("dispatch", Program (ExDispatch ExRoot (AtLabel "org")), "{Φ.org}") ] ( \(desc, prog, expected) -> it desc (printProgram prog `shouldBe` expected)@@ -104,7 +102,7 @@ ) , ( "rho binding placed after another binding"- , Program (ExFormation [BiTau (AtLabel "café") ExGlobal, BiTau AtRho (ExFormation [BiVoid AtRho])])+ , Program (ExFormation [BiTau (AtLabel "café") ExRoot, BiTau AtRho (ExFormation [BiVoid AtRho])]) , "Φ ↦ ⟦ café ↦ Φ, ρ ↦ ⟦ ρ ↦ ∅ ⟧ ⟧" ) ]@@ -117,7 +115,6 @@ [ ("label", AtLabel "attr", "attr") , ("ρ", AtRho, "ρ") , ("φ", AtPhi, "φ")- , ("α42", AtAlpha 42, "α42") , ("λ", AtLambda, "λ") , ("Δ", AtDelta, "Δ") ]@@ -125,12 +122,15 @@ it desc (printAttribute attr `shouldBe` expected) ) + describe "printAlpha with default encoding" $+ it "α42" (printAlpha (Alpha 42) `shouldBe` "α42")+ describe "printBinding renders as formation" $ forM_- [ ("tau binding", BiTau (AtLabel "x") ExGlobal, "x ↦ Φ")+ [ ("tau binding", BiTau (AtLabel "x") ExRoot, "x ↦ Φ") , ("void binding", BiVoid (AtLabel "y"), "y ↦ ∅") , ("delta binding", BiDelta (BtOne "00"), "Δ ⤍ 00-")- , ("lambda binding", BiLambda "Func", "λ ⤍ Func")+ , ("lambda binding", BiLambda (Function "Func"), "λ ⤍ Func") ] ( \(desc, bd, expected) -> it desc (printBinding bd `shouldContain` expected)@@ -150,7 +150,7 @@ forM_ [ ("attribute arg", ArgAttribute (AtLabel "tëst"), "tëst") , ("binding arg", ArgBinding (BiVoid (AtLabel "βind")), "βind ↦ ∅")- , ("expression arg", ArgExpression ExGlobal, "Φ")+ , ("expression arg", ArgExpression ExRoot, "Φ") , ("bytes arg", ArgBytes (BtOne "FF"), "FF-") ] ( \(desc, arg, expected) ->
test/ReplacerSpec.hs view
@@ -22,42 +22,42 @@ replaceProgram [ ( "Q -> Q.y.x => ([Q.y], [$]) => Q -> $.x"- , Program (ExDispatch (ExDispatch ExGlobal (AtLabel "y")) (AtLabel "x"))- , [ExDispatch ExGlobal (AtLabel "y")]- , [ExThis]- , Program (ExDispatch ExThis (AtLabel "x"))+ , Program (ExDispatch (ExDispatch ExRoot (AtLabel "y")) (AtLabel "x"))+ , [ExDispatch ExRoot (AtLabel "y")]+ , [ExXi]+ , Program (ExDispatch ExXi (AtLabel "x")) ) , ( "Q -> [[x -> [[y -> $]], z -> [[w -> $]] ]] => ([[y -> $], [w -> $]], [Q.y, Q.w]) => Q -> [[x -> Q.y, z -> Q.w]]" , Program ( ExFormation- [ BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExThis])- , BiTau (AtLabel "z") (ExFormation [BiTau (AtLabel "w") ExThis])+ [ BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExXi])+ , BiTau (AtLabel "z") (ExFormation [BiTau (AtLabel "w") ExXi]) ] )- , [ExFormation [BiTau (AtLabel "y") ExThis], ExFormation [BiTau (AtLabel "w") ExThis]]- , [ExDispatch ExGlobal (AtLabel "y"), ExDispatch ExGlobal (AtLabel "w")]+ , [ExFormation [BiTau (AtLabel "y") ExXi], ExFormation [BiTau (AtLabel "w") ExXi]]+ , [ExDispatch ExRoot (AtLabel "y"), ExDispatch ExRoot (AtLabel "w")] , Program ( ExFormation- [ BiTau (AtLabel "x") (ExDispatch ExGlobal (AtLabel "y"))- , BiTau (AtLabel "z") (ExDispatch ExGlobal (AtLabel "w"))+ [ BiTau (AtLabel "x") (ExDispatch ExRoot (AtLabel "y"))+ , BiTau (AtLabel "z") (ExDispatch ExRoot (AtLabel "w")) ] ) )- , ("Q -> [[]] => ([], [$]) => X", Program (ExFormation []), [], [ExThis], Program (ExFormation []))+ , ("Q -> [[]] => ([], [$]) => X", Program (ExFormation []), [], [ExXi], Program (ExFormation [])) , ( "Q -> [[L> Func, D> 00-]] => ([ [[L> Func, D> 00-]] ], [Q]) => Q -> Q"- , Program (ExFormation [BiLambda "Func", BiDelta (BtOne "00")])- , [ExFormation [BiLambda "Func", BiDelta (BtOne "00")]]- , [ExGlobal]- , Program ExGlobal+ , Program (ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00")])+ , [ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00")]]+ , [ExRoot]+ , Program ExRoot ) , ( "Q -> Q.org.eolang => ([Q.org.eolang, Q.org], [$, $]) => $"- , Program (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"))- , [ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"), ExDispatch ExGlobal (AtLabel "org")]- , [ExThis, ExThis]- , Program ExThis+ , Program (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang"))+ , [ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang"), ExDispatch ExRoot (AtLabel "org")]+ , [ExXi, ExXi]+ , Program ExXi ) , ( "Q -> [[ x -> $.t, t -> ? ]].t(^ -> [[ x -> $.t, t -> ? ]]) => ([ [[ x -> $.t, t -> ? ]].t ], [T]) => T(^ -> [[ x -> $.t, t -> ? ]])"@@ -65,16 +65,16 @@ ( ExApplication ( ExDispatch ( ExFormation- [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))+ [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t")) , BiVoid (AtLabel "t") ] ) (AtLabel "t") )- ( BiTau+ ( ArTau AtRho ( ExFormation- [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))+ [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t")) , BiVoid (AtLabel "t") ] )@@ -83,7 +83,7 @@ , [ ExDispatch ( ExFormation- [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))+ [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t")) , BiVoid (AtLabel "t") ] )@@ -93,10 +93,10 @@ , Program ( ExApplication ExTermination- ( BiTau+ ( ArTau AtRho ( ExFormation- [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))+ [ BiTau (AtLabel "x") (ExDispatch ExXi (AtLabel "t")) , BiVoid (AtLabel "t") ] )@@ -112,52 +112,45 @@ ) , ( "Q -> $ => ([$], [Q]) => Q -> Q"- , Program ExThis- , [ExThis]- , [ExGlobal]- , Program ExGlobal- )- ,- ( "Q -> Q.α0 => ([Q.α0], [$.α1]) => Q -> $.α1"- , Program (ExDispatch ExGlobal (AtAlpha 0))- , [ExDispatch ExGlobal (AtAlpha 0)]- , [ExDispatch ExThis (AtAlpha 1)]- , Program (ExDispatch ExThis (AtAlpha 1))+ , Program ExXi+ , [ExXi]+ , [ExRoot]+ , Program ExRoot ) , ( "Q -> [[D> --]] => ([[D> --]], [[[L> Функція]]]) => Q -> [[L> Функція]]" , Program (ExFormation [BiDelta BtEmpty]) , [ExFormation [BiDelta BtEmpty]]- , [ExFormation [BiLambda "Функція"]]- , Program (ExFormation [BiLambda "Функція"])+ , [ExFormation [BiLambda (Function "Функція")]]+ , Program (ExFormation [BiLambda (Function "Функція")]) ) , ( "Q -> Q.プログラム => ([Q.プログラム], [$.コード]) => Q -> $.コード"- , Program (ExDispatch ExGlobal (AtLabel "プログラム"))- , [ExDispatch ExGlobal (AtLabel "プログラム")]- , [ExDispatch ExThis (AtLabel "コード")]- , Program (ExDispatch ExThis (AtLabel "コード"))+ , Program (ExDispatch ExRoot (AtLabel "プログラム"))+ , [ExDispatch ExRoot (AtLabel "プログラム")]+ , [ExDispatch ExXi (AtLabel "コード")]+ , Program (ExDispatch ExXi (AtLabel "コード")) ) , ( "Q -> [[^ -> T, @ -> T]] => ([T, T], [Q, $]) => Q -> [[^ -> Q, @ -> $]]" , Program (ExFormation [BiTau AtRho ExTermination, BiTau AtPhi ExTermination]) , [ExTermination, ExTermination]- , [ExGlobal, ExThis]- , Program (ExFormation [BiTau AtRho ExGlobal, BiTau AtPhi ExThis])+ , [ExRoot, ExXi]+ , Program (ExFormation [BiTau AtRho ExRoot, BiTau AtPhi ExXi]) ) , ( "Q -> [[x -> [[y -> Q]]]].x => ([[y -> Q]], [[[z -> $]]]) => Q -> [[x -> [[z -> $]]]].x"- , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExGlobal])]) (AtLabel "x"))- , [ExFormation [BiTau (AtLabel "y") ExGlobal]]- , [ExFormation [BiTau (AtLabel "z") ExThis]]- , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "z") ExThis])]) (AtLabel "x"))+ , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExRoot])]) (AtLabel "x"))+ , [ExFormation [BiTau (AtLabel "y") ExRoot]]+ , [ExFormation [BiTau (AtLabel "z") ExXi]]+ , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "z") ExXi])]) (AtLabel "x")) ) , ( "Q -> Q.a(b -> Q.c) => ([Q.a, Q.c], [$, T]) => Q -> $(b -> T)"- , Program (ExApplication (ExDispatch ExGlobal (AtLabel "a")) (BiTau (AtLabel "b") (ExDispatch ExGlobal (AtLabel "c"))))- , [ExDispatch ExGlobal (AtLabel "a"), ExDispatch ExGlobal (AtLabel "c")]- , [ExThis, ExTermination]- , Program (ExApplication ExThis (BiTau (AtLabel "b") ExTermination))+ , Program (ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExDispatch ExRoot (AtLabel "c"))))+ , [ExDispatch ExRoot (AtLabel "a"), ExDispatch ExRoot (AtLabel "c")]+ , [ExXi, ExTermination]+ , Program (ExApplication ExXi (ArTau (AtLabel "b") ExTermination)) ) , ( "Q -> [[D> 00-01-02-]] => ([[D> 00-01-02-]], [[[D> FF-]]]) => Q -> [[D> FF-]]"@@ -168,21 +161,21 @@ ) , ( "Q -> [[@ -> $.x, ^ -> $.y]] => ([$.x, $.y], [T, Q]) => Q -> [[@ -> T, ^ -> Q]]"- , Program (ExFormation [BiTau AtPhi (ExDispatch ExThis (AtLabel "x")), BiTau AtRho (ExDispatch ExThis (AtLabel "y"))])- , [ExDispatch ExThis (AtLabel "x"), ExDispatch ExThis (AtLabel "y")]- , [ExTermination, ExGlobal]- , Program (ExFormation [BiTau AtPhi ExTermination, BiTau AtRho ExGlobal])+ , Program (ExFormation [BiTau AtPhi (ExDispatch ExXi (AtLabel "x")), BiTau AtRho (ExDispatch ExXi (AtLabel "y"))])+ , [ExDispatch ExXi (AtLabel "x"), ExDispatch ExXi (AtLabel "y")]+ , [ExTermination, ExRoot]+ , Program (ExFormation [BiTau AtPhi ExTermination, BiTau AtRho ExRoot]) ) , ( "Q -> Q.a.b.c => ([Q.a.b.c, Q.a.b, Q.a], [$, T, Q]) => Q -> $"- , Program (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")) (AtLabel "c"))+ , Program (ExDispatch (ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")) (AtLabel "c")) ,- [ ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")) (AtLabel "c")- , ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")- , ExDispatch ExGlobal (AtLabel "a")+ [ ExDispatch (ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")) (AtLabel "c")+ , ExDispatch (ExDispatch ExRoot (AtLabel "a")) (AtLabel "b")+ , ExDispatch ExRoot (AtLabel "a") ]- , [ExThis, ExTermination, ExGlobal]- , Program ExThis+ , [ExXi, ExTermination, ExRoot]+ , Program ExXi ) ] @@ -193,8 +186,8 @@ ( "Q -> [[^ -> ?, @ -> ?, D> -> ?]] => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> $, !B2 ]] => Q -> [[ ^ -> $, @ -> $, D> -> $ ]]" , Program (ExFormation [BiVoid AtRho, BiVoid AtPhi, BiVoid AtDelta]) , [ExFormation [BiVoid AtRho], ExFormation [BiVoid AtPhi], ExFormation [BiVoid AtDelta]]- , [ExFormation [BiTau AtRho ExThis], ExFormation [BiTau AtPhi ExThis], ExFormation [BiTau AtDelta ExThis]]- , Program (ExFormation [BiTau AtRho ExThis, BiTau AtPhi ExThis, BiTau AtDelta ExThis])+ , [ExFormation [BiTau AtRho ExXi], ExFormation [BiTau AtPhi ExXi], ExFormation [BiTau AtDelta ExXi]]+ , Program (ExFormation [BiTau AtRho ExXi, BiTau AtPhi ExXi, BiTau AtDelta ExXi]) ) , ( "Q -> [[ ^ -> ? ]] => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> [[ !a -> ? ]], !B2 ]] => Q -> [[ ^ -> [[ ^ -> [[ ^ -> [[ ^ -> ? ]] ]] ]] ]]"@@ -205,10 +198,10 @@ ) , ( "Q -> [[ ^ -> T ]](^ -> [[ ^ -> $]]).@ => [[ !B1, !a -> ?, !B2 ]] => [[ !B1, !a -> $, !B2 ]] => Q -> [[ ^ -> $ ]].@"- , Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExTermination]) (BiTau AtRho (ExFormation [BiTau AtRho ExThis]))) AtPhi)- , [ExFormation [BiTau AtRho ExTermination], ExFormation [BiTau AtRho ExThis]]- , [ExFormation [BiTau AtRho ExGlobal], ExFormation [BiVoid AtPhi]]- , Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExGlobal]) (BiTau AtRho (ExFormation [BiVoid AtPhi]))) AtPhi)+ , Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExTermination]) (ArTau AtRho (ExFormation [BiTau AtRho ExXi]))) AtPhi)+ , [ExFormation [BiTau AtRho ExTermination], ExFormation [BiTau AtRho ExXi]]+ , [ExFormation [BiTau AtRho ExRoot], ExFormation [BiVoid AtPhi]]+ , Program (ExDispatch (ExApplication (ExFormation [BiTau AtRho ExRoot]) (ArTau AtRho (ExFormation [BiVoid AtPhi]))) AtPhi) ) , ( "Q -> [[ ]] => ([], []) => Q -> [[ ]]"@@ -219,59 +212,59 @@ ) , ( "Q -> $ => ([$], [T]) => Q -> $"- , Program ExThis- , [ExThis]+ , Program ExXi+ , [ExXi] , [ExTermination]- , Program ExThis+ , Program ExXi ) , ( "Q -> [[ a -> ?, b -> ?, c -> ? ]] => ([[a -> ?]], [[a -> Q]]) => Q -> [[a -> Q, b -> ?, c -> ?]]" , Program (ExFormation [BiVoid (AtLabel "a"), BiVoid (AtLabel "b"), BiVoid (AtLabel "c")]) , [ExFormation [BiVoid (AtLabel "a")]]- , [ExFormation [BiTau (AtLabel "a") ExGlobal]]- , Program (ExFormation [BiTau (AtLabel "a") ExGlobal, BiVoid (AtLabel "b"), BiVoid (AtLabel "c")])+ , [ExFormation [BiTau (AtLabel "a") ExRoot]]+ , Program (ExFormation [BiTau (AtLabel "a") ExRoot, BiVoid (AtLabel "b"), BiVoid (AtLabel "c")]) ) , ( "Q -> [[ λ -> ?, D> 00- ]] => ([[λ -> ?]], [[λ -> $]]) => Q -> [[λ -> $, D> 00-]]" , Program (ExFormation [BiVoid AtLambda, BiDelta (BtOne "00")]) , [ExFormation [BiVoid AtLambda]]- , [ExFormation [BiTau AtLambda ExThis]]- , Program (ExFormation [BiTau AtLambda ExThis, BiDelta (BtOne "00")])+ , [ExFormation [BiTau AtLambda ExXi]]+ , Program (ExFormation [BiTau AtLambda ExXi, BiDelta (BtOne "00")]) ) , ( "Q -> [[x -> [[y -> ?]]]].x => ([[y -> ?]], [[y -> Q]]) => Q -> [[x -> [[y -> Q]]]].x" , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid (AtLabel "y")])]) (AtLabel "x")) , [ExFormation [BiVoid (AtLabel "y")]]- , [ExFormation [BiTau (AtLabel "y") ExGlobal]]- , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExGlobal])]) (AtLabel "x"))+ , [ExFormation [BiTau (AtLabel "y") ExRoot]]+ , Program (ExDispatch (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "y") ExRoot])]) (AtLabel "x")) ) , ( "Q -> [[アイテム -> ?]] => ([[アイテム -> ?]], [[アイテム -> $]]) => Q -> [[アイテム -> $]]" , Program (ExFormation [BiVoid (AtLabel "アイテム")]) , [ExFormation [BiVoid (AtLabel "アイテム")]]- , [ExFormation [BiTau (AtLabel "アイテム") ExThis]]- , Program (ExFormation [BiTau (AtLabel "アイテム") ExThis])+ , [ExFormation [BiTau (AtLabel "アイテム") ExXi]]+ , Program (ExFormation [BiTau (AtLabel "アイテム") ExXi]) ) , ( "Q -> [[a -> ?, a -> ?]] => ([[a -> ?]], [[a -> Q]]) => Q -> [[a -> Q, a -> Q]]" , Program (ExFormation [BiVoid (AtLabel "a"), BiVoid (AtLabel "a")]) , [ExFormation [BiVoid (AtLabel "a")]]- , [ExFormation [BiTau (AtLabel "a") ExGlobal]]- , Program (ExFormation [BiTau (AtLabel "a") ExGlobal, BiTau (AtLabel "a") ExGlobal])+ , [ExFormation [BiTau (AtLabel "a") ExRoot]]+ , Program (ExFormation [BiTau (AtLabel "a") ExRoot, BiTau (AtLabel "a") ExRoot]) ) , ( "Q -> Q.a(b -> [[c -> ?]]) => ([[c -> ?]], [[c -> T]]) => Q -> Q.a(b -> [[c -> T]])"- , Program (ExApplication (ExDispatch ExGlobal (AtLabel "a")) (BiTau (AtLabel "b") (ExFormation [BiVoid (AtLabel "c")])))+ , Program (ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExFormation [BiVoid (AtLabel "c")]))) , [ExFormation [BiVoid (AtLabel "c")]] , [ExFormation [BiTau (AtLabel "c") ExTermination]]- , Program (ExApplication (ExDispatch ExGlobal (AtLabel "a")) (BiTau (AtLabel "b") (ExFormation [BiTau (AtLabel "c") ExTermination])))+ , Program (ExApplication (ExDispatch ExRoot (AtLabel "a")) (ArTau (AtLabel "b") (ExFormation [BiTau (AtLabel "c") ExTermination]))) ) , ( "Q -> [[ L> Функція ]] => ([[ L> Функція ]], [[ L> Код ]]) => Q -> [[ L> Код ]]"- , Program (ExFormation [BiLambda "Функція"])- , [ExFormation [BiLambda "Функція"]]- , [ExFormation [BiLambda "Код"]]- , Program (ExFormation [BiLambda "Код"])+ , Program (ExFormation [BiLambda (Function "Функція")])+ , [ExFormation [BiLambda (Function "Функція")]]+ , [ExFormation [BiLambda (Function "Код")]]+ , Program (ExFormation [BiLambda (Function "Код")]) ) ] @@ -282,7 +275,7 @@ ( "Q -> [[a -> ?]] => ([[a -> ?]], [[a -> $]]) => Q -> [[a -> ?]]" , Program (ExFormation [BiVoid (AtLabel "a")]) , [ExFormation [BiVoid (AtLabel "a")]]- , [ExFormation [BiTau (AtLabel "a") ExThis]]+ , [ExFormation [BiTau (AtLabel "a") ExXi]] , Program (ExFormation [BiVoid (AtLabel "a")]) ) ]
test/RewriterSpec.hs view
@@ -8,7 +8,7 @@ module RewriterSpec where -import AST (Expression (ExGlobal))+import AST (Expression (ExRoot)) import Control.Monad (forM_, unless) import Data.Aeson import Data.Char (isSpace)@@ -107,7 +107,7 @@ prog rules' ( RewriteContext- ExGlobal+ ExRoot repeat' repeat' False
test/RuleSpec.hs view
@@ -7,7 +7,7 @@ module RuleSpec where -import AST (Attribute (..), Binding (..), Bytes (..), Expression (..), Program (Program))+import AST (Argument (..), Attribute (..), Binding (..), Bytes (..), Expression (..), Function (..), Program (Program)) import Control.Monad import Data.Aeson import Data.Yaml qualified as Y@@ -61,17 +61,17 @@ describe "isNF determines normal form" $ do let ctx = RuleContext buildTerm forM_- [ ("returns true for ExThis", ExThis, True)- , ("returns true for ExGlobal", ExGlobal, True)+ [ ("returns true for ExXi", ExXi, True)+ , ("returns true for ExRoot", ExRoot, True) , ("returns true for ExTermination", ExTermination, True)- , ("returns true for dispatch on ExThis", ExDispatch ExThis (AtLabel "foo"), True)- , ("returns true for dispatch on ExGlobal", ExDispatch ExGlobal (AtLabel "bar"), True)+ , ("returns true for dispatch on ExXi", ExDispatch ExXi (AtLabel "foo"), True)+ , ("returns true for dispatch on ExRoot", ExDispatch ExRoot (AtLabel "bar"), True) , ("returns false for dispatch on ExTermination", ExDispatch ExTermination (AtLabel "x"), False)- , ("returns false for application on ExTermination", ExApplication ExTermination (BiTau (AtLabel "y") ExGlobal), False)+ , ("returns false for application on ExTermination", ExApplication ExTermination (ArTau (AtLabel "y") ExRoot), False) , ("returns true for empty formation", ExFormation [], True) , ("returns true for formation with only delta binding", ExFormation [BiDelta (BtMany ["00", "01"])], True) , ("returns true for formation with only void binding", ExFormation [BiVoid (AtLabel "x")], True)- , ("returns true for formation with only lambda binding", ExFormation [BiLambda "Func"], True)- , ("returns true for formation with delta void and lambda", ExFormation [BiDelta (BtOne "FF"), BiVoid (AtLabel "y"), BiLambda "G"], True)+ , ("returns true for formation with only lambda binding", ExFormation [BiLambda (Function "Func")], True)+ , ("returns true for formation with delta void and lambda", ExFormation [BiDelta (BtOne "FF"), BiVoid (AtLabel "y"), BiLambda (Function "G")], True) ] (\(desc, expr, expected) -> it desc $ isNF expr ctx `shouldBe` expected)
test/TauSpec.hs view
@@ -26,8 +26,8 @@ seedTaus ( Program ( ExFormation- [ BiTau (AtLabel "a🌵0") ExGlobal- , BiTau (AtLabel "a🌵2") ExGlobal+ [ BiTau (AtLabel "a🌵0") ExRoot+ , BiTau (AtLabel "a🌵2") ExRoot ] ) )