diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ ```bash cabal update -cabal install --overwrite-policy=always phino-0.0.144 +cabal install --overwrite-policy=always phino-0.0.145 phino --version ``` @@ -287,6 +287,15 @@ bringing two such branches to one shape is the program's job and not `phino`'s, which its entry does in a `rewrite` block. +A bare symbol, `⟦ Ξ» ‍ 𝜎A ⟧` with no carrier around it, is what the deep walk +answers a copy it deferred with (see Deep morphing below), and it joins with +a formation too. It has no `Ο†` chain of its own, only the symbol, so the join +pairs `𝜎A` with the symbol the `Ο†` chain of the other term ends in, mints a +fresh `𝜎C` for that pair the usual way, and answers the bare `⟦ Ξ» ‍ 𝜎C ⟧`. +The methods of the formation are dropped, since the other branch may have +none of them. A formation whose `Ο†` chain ends in a datum, or which has no `Ο†` +at all, does not join with a bare symbol. + One term being `βŠ₯` is the exception, since `if. cond value βŠ₯` is how EO spells "raise unless `cond`": the program raises on that side of the condition and has a perfectly good value on the other. The join then mints nothing, binds @@ -553,6 +562,37 @@ of the protocol. The markup spells it ``. +`spent(3) # 𝔻(…)` is where `--max-firings=3` ran out, commented the same way +and written where the firing it refused would have started. +The markup spells it ``. + +`deferred(𝜎2) := Ξ¦.box( x ↦ 𝜎1:Ξ» ) # 𝕄(Ξ¦.y)` is a copy the deep walk +deferred instead of entering it. The fresh symbol it answered the copy with +stands in parentheses. The copy is written as a call of the object of the world +it was made of, given the arguments that fill its voids, read. The comment +names the judgment and the site of the walk. +The object is found through the `ρ` of the copy: no `ρ` means `Ξ¦`, a `ρ` that +is a name means that name with its applications erased, and a `ρ` that is a +formation means the object that formation was made of. Among the formations +declared there, the copy was made of the one whose attributes cover its own, +whose voids it fills the most, and which shares the most bindings with it. +When the world declares no such object, or two of them tie, the copy is +written as it stood, such as `⟦ x ↦ 𝜎1:Ξ», Ο† ↦ x.next ⟧`. +The markup spells it on one line, broken here for reading. The object stands +in `of` and the arguments in ``, both written whatever `--abridged` +says, and the copy as it stood stands in ``, abridged as usual: + +```xml + + 𝜎1 + ⟦ x ↦ 𝜎1:Ξ», Ο† ↦ x.next ⟧ + +``` + +Every argument of the call is an `` of ``, and an argument that +is not a bare symbol is spelled `?`. A copy with no object of the world has +neither `of` nor ``, only ``. + Every term is πœ‘ on a single line, whatever `--output` and `--flat` say about the result of the run, so a program reading the protocol back never has to know what the run printed. The file is truncated at the beginning of every run, so @@ -1122,6 +1162,32 @@ ⟧ ``` +One kind of formation the walk does not enter at all: a copy with a `Ο†` +written as code and an argument that is a bare symbol, a `⟦ Ξ» ‍ 𝜎1 ⟧` with +no carrier around it. The symbol stands for a value nobody knows, so the body +can only ask it questions nobody can answer, and every firing spent inside +that body is wasted. The walk defers such a copy instead: it answers the copy +with a fresh symbol and writes a `deferred` line to the protocol, tying that +symbol to the copy it stands for, which only a run of the program can work out. +The walk reads every argument written as a dispatch before it decides, so +`tup ↦ items.tail` counts when `items.tail` comes to a bare symbol, but it +fires nothing while reading. A copy with no `Ο†`, such as a tuple, only holds +its arguments, so reading one of them reaches the symbol and defers nothing. +Here the walk defers the copy of `box`: + +```bash +$ cat box.phi +⟦ + box(x) ↦ ⟦ Ο† ↦ x.next ⟧, + y ↦ Ξ¦.box( x ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ) +⟧ +$ phino morph --deep --locator=Q.y --protocol=p.txt --sweet --hide-rho box.phi +𝜎2:Ξ» +$ head -2 p.txt +𝕄(Ξ¦.y) + deferred(𝜎2) := Ξ¦.box( x ↦ 𝜎1:Ξ» ) # 𝕄(Ξ¦.y) +``` + ### Acyclic morphing Whether a program terminates is the object model's business, not the @@ -1270,6 +1336,8 @@ 𝔻(𝜎6:Ξ») == 01- 𝑛3.4 := 𝜎6:Ξ» # 𝑛1 𝑛4.4 := ⟦ a ↦ 𝜎3:Ξ», b ↦ Ξ¦.fact( n ↦ 𝜎5:Ξ» ), Ξ» ‍ L_mul ⟧ # 𝑛2 + stuck(L_if) + stuck(L_if) 𝔼(L_if) # 𝕄(Ξ¦.x.Ο†) 𝛿1.7 := 𝔻(𝜎2:Ξ») # 𝔻(ΞΎ.c) 𝑛1.7 := 01-:Ξ” # 𝕄(ΞΎ.left) @@ -1292,10 +1360,16 @@ 𝔻(𝜎6:Ξ») == 01- 𝑛3.9 := 𝑛3.4 # 𝑛1 𝑛4.9 := ⟦ a ↦ 𝜎3:Ξ», b ↦ Ξ¦.fact( n ↦ 𝜎5:Ξ» ), Ξ» ‍ L_mul ⟧ # 𝑛2 + stuck(L_if) + stuck(L_if) 𝑛2.7 := ⟦ a ↦ 𝜎1:Ξ», b ↦ Ξ¦.fact( n ↦ 𝜎3:Ξ» ), Ξ» ‍ L_mul ⟧ # 𝕄(ΞΎ.right) 𝔻(𝜎4:Ξ») == 01- 𝑛3.7 := 𝑛.10.2 # 𝑛1 𝑛4.7 := ⟦ a ↦ 𝜎1:Ξ», b ↦ Ξ¦.fact( n ↦ 𝜎3:Ξ» ), Ξ» ‍ L_mul ⟧ # 𝑛2 + stuck(L_if) +msec(31) +firings(11) +fps(355) ``` @@ -1401,14 +1475,26 @@ two under `a` and no operand line, since nothing was reduced for them, and they are not charged to `--max-firings`, which counts the firings the run made. The formation is compared with everything it carries, `ρ` included, so -a firing on another object is another firing. A firing cut by the mode on its -way to an answer keeps the cut, and the next firing of the same formation is -cut at its own site without reducing anything first. A firing that got stuck -keeps the Ξ» function it got stuck on, and the next firing of the same -formation gets stuck at its own site the same way, with nothing reduced -under it, as long as nothing new was answered in between. Once something -was, the formation is fired again, since an operand that could not be -brought down the first time may come down now. +a firing on another object is another firing, yet it may take the same answer +all the same: the run keeps every answer by the Ξ» name and what the operands +came down to as well, and a firing whose operands come down to the data, the +symbols and the normal forms of one already answered takes that answer once +they are down, minting nothing. An attribute read from the `Ο†` of an object +and then reached as a binding of it is read through two `ΞΎ`, each the object +minus the attribute being read, so it is two formations, but one firing, and +so one symbol. A symbol counts as the symbol it is, not as the datum every +symbol manufactures, so two firings over two symbols stay two. The protocol +writes such a firing with its operand lines and the answer lines of the one +it took the answer from, and `--max-firings` charges it like a firing made, +since a firing is charged as it starts bringing its operands down, which is +the only place a recursion widening inside its operands can be cut. A firing +cut by the mode on its way to an answer keeps the cut, and the next firing of +the same formation is cut at its own site without reducing anything first. A +firing that got stuck keeps the Ξ» function it got stuck on, and the next +firing of the same formation gets stuck at its own site the same way, with +nothing reduced under it, as long as nothing new was answered in between. +Once something was, the formation is fired again, since an operand that could +not be brought down the first time may come down now. The mode also walks a binding of the world once. Every dispatch on an object of the world copies it, and `--deep` walks every copy, so the tests of an @@ -1512,13 +1598,13 @@ ## Rewrite You can rewrite this expression with the help of [rules](#rule-structure) -defined in the `my-rule.yml` YAML file (here, the `!d` is a capturing group, -similar to regular expressions): +defined in the `my-rule.yml` YAML file (here, the `!d1` and `!B1` are capturing +groups, similar to regular expressions): ```yaml name: My custom rule -pattern: Ξ” ‍ !d -result: Ξ” ‍ 62-79-65 +pattern: ⟦ Ξ” ‍ !d1, !B1 ⟧ +result: ⟦ Ξ” ‍ 62-79-65, !B1 ⟧ ``` Then, rewrite: diff --git a/benchmark/Main.hs b/benchmark/Main.hs --- a/benchmark/Main.hs +++ b/benchmark/Main.hs @@ -8,6 +8,7 @@ import Compiled (compiled) import Control.Exception (evaluate) import Control.Monad (replicateM, replicateM_) +import qualified Data.List.NonEmpty as NE import qualified Data.Map.Strict as Map import Data.Maybe (fromMaybe) import Data.String (fromString) @@ -148,7 +149,7 @@ counters <- readLambdas "benchmark/accum.yaml" runBench "parse/phi" (parseExpressionThrows src) runBench "parse/xmir" (parseXMIRThrows xsrc >>= xmirToPhi) - runBench "rewrite/normalize" (rewrite expr (map (stepOf linked) normalizationRules) rewriteCtx) + runBench "rewrite/normalize" (hashExpression . fst . NE.last . fst <$> rewrite expr (map (stepOf linked) normalizationRules) rewriteCtx) runBench "print/sweet/multiline" (evaluate (length (printExpression' expr (SWEET, UNICODE, MULTILINE, defaultMargin)))) diff --git a/compiled/generated/Compiled.hs b/compiled/generated/Compiled.hs --- a/compiled/generated/Compiled.hs +++ b/compiled/generated/Compiled.hs @@ -50,7 +50,7 @@ -- The texts of the built-in rules of all four judgments this module is made of. sources :: [String] -sources = ["Rule {name = \"alpha\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\",BiVoid !t1,BiMeta \"B2\"]) (ArAlpha \945!i1 (ExMeta \"e1\")), result = ExApplication (ExFormation [BiMeta \"B1\",BiVoid !t1,BiMeta \"B2\"]) (ArTau !t1 (ExMeta \"e1\")), when = Just (And [Eq (CmpNum (MetaIndex \"i1\")) (CmpNum (Domain (BiMeta \"B1\"))),Not (Eq (CmpAttr !t1) (CmpAttr \961))]), where_ = Nothing, having = Nothing}", "Rule {name = \"amiss\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\"]) (ArAlpha \945!i1 (ExAny (Slot \"e\" 11))), result = ExTermination, when = Just (Not (Gt (CmpNum (Domain (BiMeta \"B1\"))) (CmpNum (MetaIndex \"i1\")))), where_ = Nothing, having = Nothing}", "Rule {name = \"copy\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\",BiVoid !t1,BiMeta \"B2\"]) (ArTau !t1 (ExMeta \"k1\")), result = ExFormation [BiMeta \"B1\",BiTau !t1 (ExMeta \"k1\"),BiMeta \"B2\"], when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"dc\", label = Nothing, description = Nothing, pattern = ExApplication ExTermination (ArTau !t (ExAny (Slot \"e\" 6))), result = ExTermination, when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"dca\", label = Nothing, description = Nothing, pattern = ExApplication ExTermination (ArAlpha \945!i (ExAny (Slot \"e\" 7))), result = ExTermination, when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"dd\", label = Nothing, description = Nothing, pattern = ExDispatch ExTermination !t, result = ExTermination, when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"dl\", label = Nothing, description = Nothing, pattern = ExFormation [BiMeta \"B1\",BiLambda (FnAny (Slot \"F\" 9)),BiMeta \"B2\"], result = ExTermination, when = Just (In [\916] [BiMeta \"B1\",BiMeta \"B2\"]), where_ = Nothing, having = Nothing}", "Rule {name = \"dot\", label = Nothing, description = Nothing, pattern = ExDispatch (ExFormation [BiMeta \"B1\",BiTau !t1 (ExMeta \"n1\"),BiMeta \"B2\"]) !t1, result = ExApplication (ExMeta \"e1\") (ArTau \961 (ExMeta \"e2\")), when = Just (Not (In [\916,\955] [BiMeta \"B1\",BiMeta \"B2\"])), where_ = Just [Extra {meta = ArgExpression (ExMeta \"e1\"), function = \"contextualize\", args = [ArgExpression (ExMeta \"n1\"),ArgExpression (ExFormation [BiMeta \"B1\",BiMeta \"B2\"])]},Extra {meta = ArgExpression (ExMeta \"e2\"), function = \"named\", args = [ArgExpression (ExFormation [BiMeta \"B1\",BiTau !t1 (ExMeta \"n1\"),BiMeta \"B2\"])]}], having = Nothing}", "Rule {name = \"miss\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\"]) (ArTau !t1 (ExAny (Slot \"e\" 10))), result = ExTermination, when = Just (And [Not (In [!t1] [BiMeta \"B1\"]),Not (Eq (CmpAttr !t1) (CmpAttr \961))]), where_ = Nothing, having = Nothing}", "Rule {name = \"null\", label = Nothing, description = Nothing, pattern = ExDispatch (ExFormation [BiMeta \"B1\",BiVoid !t1,BiMeta \"B2\"]) !t1, result = ExTermination, when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"over\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\",BiTau !t1 (ExMeta \"e1\"),BiMeta \"B2\"]) (ArTau !t1 (ExMeta \"e2\")), result = ExTermination, when = Just (Not (Eq (CmpAttr !t1) (CmpAttr \961))), where_ = Nothing, having = Nothing}", "Rule {name = \"overa\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\",BiTau !t1 (ExMeta \"e1\"),BiMeta \"B2\"]) (ArAlpha \945!i1 (ExMeta \"e2\")), result = ExTermination, when = Just (And [Eq (CmpNum (MetaIndex \"i1\")) (CmpNum (Domain (BiMeta \"B1\"))),Not (Eq (CmpAttr !t1) (CmpAttr \961))]), where_ = Nothing, having = Nothing}", "Rule {name = \"skip\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\"]) (ArTau \961 (ExMeta \"e1\")), result = ExFormation [BiMeta \"B1\"], when = Just (Not (In [\961] [BiMeta \"B1\"])), where_ = Nothing, having = Nothing}", "Rule {name = \"stay\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\",BiTau \961 (ExMeta \"e1\"),BiMeta \"B2\"]) (ArTau \961 (ExMeta \"e2\")), result = ExFormation [BiMeta \"B1\",BiTau \961 (ExMeta \"e1\"),BiMeta \"B2\"], when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"stop\", label = Nothing, description = Nothing, pattern = ExDispatch (ExFormation [BiMeta \"B1\"]) !t1, result = ExTermination, when = Just (Disjoint [!t1,\966,\955] [BiMeta \"B1\"]), where_ = Nothing, having = Nothing}", "ContextualizeRule {name = \"ca\", label = Nothing, match = ExApplication (ExMeta \"n1\") (ArTau !t1 (ExMeta \"e1\")), cmatch = ExMeta \"k1\", cresult = ExApplication (ExMeta \"n2\") (ArTau !t1 (ExMeta \"n3\")), premises = [Premise {result = \"n2\", operation = OpContextualize (ExMeta \"n1\") (ExMeta \"k1\")},Premise {result = \"n3\", operation = OpContextualize (ExMeta \"e1\") (ExMeta \"k1\")}]}", "ContextualizeRule {name = \"caa\", label = Nothing, match = ExApplication (ExMeta \"n1\") (ArAlpha \945!i1 (ExMeta \"e1\")), cmatch = ExMeta \"k1\", cresult = ExApplication (ExMeta \"n2\") (ArAlpha \945!i1 (ExMeta \"n3\")), premises = [Premise {result = \"n2\", operation = OpContextualize (ExMeta \"n1\") (ExMeta \"k1\")},Premise {result = \"n3\", operation = OpContextualize (ExMeta \"e1\") (ExMeta \"k1\")}]}", "ContextualizeRule {name = \"cd\", label = Nothing, match = ExDispatch (ExMeta \"n1\") !t1, cmatch = ExMeta \"k1\", cresult = ExDispatch (ExMeta \"n2\") !t1, premises = [Premise {result = \"n2\", operation = OpContextualize (ExMeta \"n1\") (ExMeta \"k1\")}]}", "ContextualizeRule {name = \"cf\", label = Nothing, match = ExFormation [BiMeta \"B1\"], cmatch = ExMeta \"k1\", cresult = ExFormation [BiMeta \"B1\"], premises = []}", "ContextualizeRule {name = \"cg\", label = Nothing, match = ExRoot, cmatch = ExMeta \"k1\", cresult = ExRoot, premises = []}", "ContextualizeRule {name = \"ct\", label = Nothing, match = ExTermination, cmatch = ExMeta \"k1\", cresult = ExTermination, premises = []}", "ContextualizeRule {name = \"cxi\", label = Nothing, match = ExXi, cmatch = ExMeta \"k1\", cresult = ExMeta \"k1\", premises = []}", "MorphRule {name = \"dead\", label = Nothing, match = ExTermination, ematch = ExMeta \"e1\", nresult = ExTermination, when = Nothing, premises = []}", "MorphRule {name = \"ma\", label = Nothing, match = ExApplication (ExMeta \"n1\") (ArTau !t1 (ExMeta \"k1\")), ematch = ExMeta \"e1\", nresult = ExMeta \"n4\", when = Nothing, premises = [Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")},Premise {result = \"n3\", operation = OpNormalize (ExApplication (ExMeta \"n2\") (ArTau !t1 (ExMeta \"k1\")))},Premise {result = \"n4\", operation = OpMorph (ExMeta \"n3\") (ExMeta \"e1\")}]}", "MorphRule {name = \"maa\", label = Nothing, match = ExApplication (ExMeta \"n1\") (ArAlpha \945!i1 (ExMeta \"k1\")), ematch = ExMeta \"e1\", nresult = ExMeta \"n4\", when = Nothing, premises = [Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")},Premise {result = \"n3\", operation = OpNormalize (ExApplication (ExMeta \"n2\") (ArAlpha \945!i1 (ExMeta \"k1\")))},Premise {result = \"n4\", operation = OpMorph (ExMeta \"n3\") (ExMeta \"e1\")}]}", "MorphRule {name = \"maad\", label = Nothing, match = ExApplication (ExAny (Slot \"n\" 0)) (ArAlpha \945!i (ExMeta \"n1\")), ematch = ExMeta \"e1\", nresult = ExMeta \"n2\", when = Just (Not (Absolute (ExMeta \"n1\"))), premises = [Premise {result = \"n2\", operation = OpMorph ExTermination (ExMeta \"e1\")}]}", "MorphRule {name = \"mad\", label = Nothing, match = ExApplication (ExAny (Slot \"n\" 0)) (ArTau !t (ExMeta \"n1\")), ematch = ExMeta \"e1\", nresult = ExMeta \"n2\", when = Just (Not (Absolute (ExMeta \"n1\"))), premises = [Premise {result = \"n2\", operation = OpMorph ExTermination (ExMeta \"e1\")}]}", "MorphRule {name = \"md\", label = Nothing, match = ExDispatch (ExMeta \"n1\") !t1, ematch = ExMeta \"e1\", nresult = ExMeta \"n4\", when = Just (Not (IsFormation (ExMeta \"n1\"))), premises = [Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")},Premise {result = \"n3\", operation = OpNormalize (ExDispatch (ExMeta \"n2\") !t1)},Premise {result = \"n4\", operation = OpMorph (ExMeta \"n3\") (ExMeta \"e1\")}]}", "MorphRule {name = \"mf\", label = Nothing, match = ExFormation [BiMeta \"B1\"], ematch = ExMeta \"e1\", nresult = ExFormation [BiMeta \"B1\"], when = Nothing, premises = []}", "MorphRule {name = \"mg\", label = Nothing, match = ExRoot, ematch = ExRoot, nresult = ExMeta \"n1\", when = Nothing, premises = [Premise {result = \"n1\", operation = OpMorph ExTermination ExRoot}]}", "MorphRule {name = \"ml\", label = Just \"\\\\lambda\", match = ExDispatch (ExFormation [BiMeta \"B1\",BiLambda (FnMeta \"F1\"),BiMeta \"B2\"]) !t1, ematch = ExMeta \"e1\", nresult = ExMeta \"n3\", when = Nothing, premises = [Premise {result = \"n1\", operation = OpEvaluate (ExFormation [BiMeta \"B1\",BiLambda (FnMeta \"F1\"),BiMeta \"B2\"]) (ExMeta \"e1\")},Premise {result = \"n2\", operation = OpNormalize (ExDispatch (ExMeta \"n1\") !t1)},Premise {result = \"n3\", operation = OpMorph (ExMeta \"n2\") (ExMeta \"e1\")}]}", "MorphRule {name = \"mphi\", label = Just \"\\\\varphi\", match = ExDispatch (ExFormation [BiMeta \"B1\"]) !t1, ematch = ExMeta \"e1\", nresult = ExMeta \"n2\", when = Just (And [In [\966] [BiMeta \"B1\"],Disjoint [!t1,\955] [BiMeta \"B1\"]]), premises = [Premise {result = \"n1\", operation = OpNormalize (ExDispatch (ExDispatch (ExFormation [BiMeta \"B1\"]) \966) !t1)},Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")}]}", "MorphRule {name = \"universe\", label = Just \"\\\\Phi\", match = ExRoot, ematch = ExMeta \"e1\", nresult = ExMeta \"n2\", when = Just (Not (Eq (CmpExpr (ExMeta \"e1\")) (CmpExpr ExRoot))), premises = [Premise {result = \"n1\", operation = OpNormalize (ExMeta \"e1\")},Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")}]}", "MorphRule {name = \"xi\", label = Nothing, match = ExXi, ematch = ExMeta \"e1\", nresult = ExMeta \"n1\", when = Nothing, premises = [Premise {result = \"n1\", operation = OpMorph ExTermination (ExMeta \"e1\")}]}", "DataizeRule {name = \"box\", label = Nothing, match = ExFormation [BiMeta \"B1\",BiTau \966 (ExMeta \"e2\"),BiMeta \"B2\"], ematch = ExMeta \"e1\", dresult = BtMeta \"d1\", when = Just (Disjoint [\916,\955] [BiMeta \"B1\",BiMeta \"B2\"]), premises = [Premise {result = \"e3\", operation = OpContextualize (ExMeta \"e2\") (ExFormation [BiMeta \"B1\",BiTau \966 (ExMeta \"e2\"),BiMeta \"B2\"])},Premise {result = \"n1\", operation = OpNormalize (ExMeta \"e3\")},Premise {result = \"d1\", operation = OpDataize (ExMeta \"n1\") (ExMeta \"e1\")}]}", "DataizeRule {name = \"delta\", label = Just \"\\\\Delta\", match = ExFormation [BiMeta \"B1\",BiDelta (BtMeta \"d1\"),BiMeta \"B2\"], ematch = ExMeta \"e1\", dresult = BtMeta \"d1\", when = Nothing, premises = []}", "DataizeRule {name = \"fire\", label = Nothing, match = ExFormation [BiMeta \"B1\",BiLambda (FnMeta \"F1\"),BiMeta \"B2\"], ematch = ExMeta \"e1\", dresult = BtMeta \"d1\", when = Nothing, premises = [Premise {result = \"n1\", operation = OpEvaluate (ExFormation [BiMeta \"B1\",BiLambda (FnMeta \"F1\"),BiMeta \"B2\"]) (ExMeta \"e1\")},Premise {result = \"d1\", operation = OpDataize (ExMeta \"n1\") (ExMeta \"e1\")}]}", "DataizeRule {name = \"none\", label = Nothing, match = ExFormation [BiMeta \"B1\"], ematch = ExMeta \"e1\", dresult = BtMeta \"d1\", when = Just (Disjoint [\916,\955,\966] [BiMeta \"B1\"]), premises = [Premise {result = \"d1\", operation = OpDataize ExTermination (ExMeta \"e1\")}]}", "DataizeRule {name = \"norm\", label = Nothing, match = ExMeta \"n1\", ematch = ExMeta \"e1\", dresult = BtMeta \"d1\", when = Just (And [Not (IsFormation (ExMeta \"n1\")),Not (Eq (CmpExpr (ExMeta \"n1\")) (CmpExpr ExTermination))]), premises = [Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")},Premise {result = \"d1\", operation = OpDataize (ExMeta \"n2\") (ExMeta \"e1\")}]}"] +sources = ["Rule {name = \"alpha\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\",BiVoid !t1,BiMeta \"B2\"]) (ArAlpha \945!i1 (ExMeta \"e1\")), result = ExApplication (ExFormation [BiMeta \"B1\",BiVoid !t1,BiMeta \"B2\"]) (ArTau !t1 (ExMeta \"e1\")), when = Just (And [Eq (CmpNum (MetaIndex \"i1\")) (CmpNum (Domain (BiMeta \"B1\"))),Not (Eq (CmpAttr !t1) (CmpAttr \961))]), where_ = Nothing, having = Nothing}", "Rule {name = \"amiss\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\"]) (ArAlpha \945!i1 (ExAny (Slot \"e\" 11))), result = ExTermination, when = Just (Not (Gt (CmpNum (Domain (BiMeta \"B1\"))) (CmpNum (MetaIndex \"i1\")))), where_ = Nothing, having = Nothing}", "Rule {name = \"copy\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\",BiVoid !t1,BiMeta \"B2\"]) (ArTau !t1 (ExMeta \"k1\")), result = ExFormation [BiMeta \"B1\",BiTau !t1 (ExMeta \"k1\"),BiMeta \"B2\"], when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"dc\", label = Nothing, description = Nothing, pattern = ExApplication ExTermination (ArTau !t (ExAny (Slot \"e\" 6))), result = ExTermination, when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"dca\", label = Nothing, description = Nothing, pattern = ExApplication ExTermination (ArAlpha \945!i (ExAny (Slot \"e\" 7))), result = ExTermination, when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"dd\", label = Nothing, description = Nothing, pattern = ExDispatch ExTermination !t, result = ExTermination, when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"dl\", label = Nothing, description = Nothing, pattern = ExFormation [BiMeta \"B1\",BiLambda (FnAny (Slot \"F\" 9)),BiMeta \"B2\"], result = ExTermination, when = Just (In [\916] [BiMeta \"B1\",BiMeta \"B2\"]), where_ = Nothing, having = Nothing}", "Rule {name = \"dot\", label = Nothing, description = Nothing, pattern = ExDispatch (ExFormation [BiMeta \"B1\",BiTau !t1 (ExMeta \"n1\"),BiMeta \"B2\"]) !t1, result = ExApplication (ExMeta \"e1\") (ArTau \961 (ExMeta \"e2\")), when = Just (Not (In [\916,\955] [BiMeta \"B1\",BiMeta \"B2\"])), where_ = Just [Extra {meta = ArgExpression (ExMeta \"e1\"), function = \"contextualize\", args = [ArgExpression (ExMeta \"n1\"),ArgExpression (ExFormation [BiMeta \"B1\",BiMeta \"B2\"])]},Extra {meta = ArgExpression (ExMeta \"e2\"), function = \"named\", args = [ArgExpression (ExFormation [BiMeta \"B1\",BiTau !t1 (ExMeta \"n1\"),BiMeta \"B2\"])]}], having = Nothing}", "Rule {name = \"miss\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\"]) (ArTau !t1 (ExAny (Slot \"e\" 10))), result = ExTermination, when = Just (And [Not (In [!t1] [BiMeta \"B1\"]),Not (Eq (CmpAttr !t1) (CmpAttr \961))]), where_ = Nothing, having = Nothing}", "Rule {name = \"null\", label = Nothing, description = Nothing, pattern = ExDispatch (ExFormation [BiMeta \"B1\",BiVoid !t1,BiMeta \"B2\"]) !t1, result = ExTermination, when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"over\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\",BiTau !t1 (ExMeta \"e1\"),BiMeta \"B2\"]) (ArTau !t1 (ExMeta \"e2\")), result = ExTermination, when = Just (Not (Eq (CmpAttr !t1) (CmpAttr \961))), where_ = Nothing, having = Nothing}", "Rule {name = \"overa\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\",BiTau !t1 (ExMeta \"e1\"),BiMeta \"B2\"]) (ArAlpha \945!i1 (ExMeta \"e2\")), result = ExTermination, when = Just (And [Eq (CmpNum (MetaIndex \"i1\")) (CmpNum (Domain (BiMeta \"B1\"))),Not (Eq (CmpAttr !t1) (CmpAttr \961))]), where_ = Nothing, having = Nothing}", "Rule {name = \"skip\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\"]) (ArTau \961 (ExMeta \"e1\")), result = ExFormation [BiMeta \"B1\"], when = Just (Not (In [\961] [BiMeta \"B1\"])), where_ = Nothing, having = Nothing}", "Rule {name = \"stay\", label = Nothing, description = Nothing, pattern = ExApplication (ExFormation [BiMeta \"B1\",BiTau \961 (ExMeta \"e1\"),BiMeta \"B2\"]) (ArTau \961 (ExMeta \"e2\")), result = ExFormation [BiMeta \"B1\",BiTau \961 (ExMeta \"e1\"),BiMeta \"B2\"], when = Nothing, where_ = Nothing, having = Nothing}", "Rule {name = \"stop\", label = Nothing, description = Nothing, pattern = ExDispatch (ExFormation [BiMeta \"B1\"]) !t1, result = ExTermination, when = Just (Disjoint [!t1,\966,\955] [BiMeta \"B1\"]), where_ = Nothing, having = Nothing}", "ContextualizeRule {name = \"ca\", label = Nothing, match = ExApplication (ExMeta \"n1\") (ArTau !t1 (ExMeta \"e1\")), cmatch = ExMeta \"k1\", cresult = ExApplication (ExMeta \"n2\") (ArTau !t1 (ExMeta \"n3\")), premises = [Premise {result = \"n2\", operation = OpContextualize (ExMeta \"n1\") (ExMeta \"k1\")},Premise {result = \"n3\", operation = OpContextualize (ExMeta \"e1\") (ExMeta \"k1\")}]}", "ContextualizeRule {name = \"caa\", label = Nothing, match = ExApplication (ExMeta \"n1\") (ArAlpha \945!i1 (ExMeta \"e1\")), cmatch = ExMeta \"k1\", cresult = ExApplication (ExMeta \"n2\") (ArAlpha \945!i1 (ExMeta \"n3\")), premises = [Premise {result = \"n2\", operation = OpContextualize (ExMeta \"n1\") (ExMeta \"k1\")},Premise {result = \"n3\", operation = OpContextualize (ExMeta \"e1\") (ExMeta \"k1\")}]}", "ContextualizeRule {name = \"cd\", label = Nothing, match = ExDispatch (ExMeta \"n1\") !t1, cmatch = ExMeta \"k1\", cresult = ExDispatch (ExMeta \"n2\") !t1, premises = [Premise {result = \"n2\", operation = OpContextualize (ExMeta \"n1\") (ExMeta \"k1\")}]}", "ContextualizeRule {name = \"cf\", label = Nothing, match = ExFormation [BiMeta \"B1\"], cmatch = ExMeta \"k1\", cresult = ExFormation [BiMeta \"B1\"], premises = []}", "ContextualizeRule {name = \"cg\", label = Nothing, match = ExRoot, cmatch = ExMeta \"k1\", cresult = ExRoot, premises = []}", "ContextualizeRule {name = \"ct\", label = Nothing, match = ExTermination, cmatch = ExMeta \"k1\", cresult = ExTermination, premises = []}", "ContextualizeRule {name = \"cxi\", label = Nothing, match = ExXi, cmatch = ExMeta \"k1\", cresult = ExMeta \"k1\", premises = []}", "MorphRule {name = \"dead\", label = Nothing, match = ExTermination, ematch = ExMeta \"e1\", nresult = ExTermination, when = Nothing, premises = []}", "MorphRule {name = \"ma\", label = Nothing, match = ExApplication (ExMeta \"n1\") (ArTau !t1 (ExMeta \"k1\")), ematch = ExMeta \"e1\", nresult = ExMeta \"n4\", when = Nothing, premises = [Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")},Premise {result = \"n3\", operation = OpNormalize (ExApplication (ExMeta \"n2\") (ArTau !t1 (ExMeta \"k1\")))},Premise {result = \"n4\", operation = OpMorph (ExMeta \"n3\") (ExMeta \"e1\")}]}", "MorphRule {name = \"maa\", label = Nothing, match = ExApplication (ExMeta \"n1\") (ArAlpha \945!i1 (ExMeta \"k1\")), ematch = ExMeta \"e1\", nresult = ExMeta \"n4\", when = Nothing, premises = [Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")},Premise {result = \"n3\", operation = OpNormalize (ExApplication (ExMeta \"n2\") (ArAlpha \945!i1 (ExMeta \"k1\")))},Premise {result = \"n4\", operation = OpMorph (ExMeta \"n3\") (ExMeta \"e1\")}]}", "MorphRule {name = \"maad\", label = Nothing, match = ExApplication (ExAny (Slot \"n\" 0)) (ArAlpha \945!i (ExMeta \"n1\")), ematch = ExMeta \"e1\", nresult = ExMeta \"n2\", when = Just (Not (Absolute (ExMeta \"n1\"))), premises = [Premise {result = \"n2\", operation = OpMorph ExTermination (ExMeta \"e1\")}]}", "MorphRule {name = \"mad\", label = Nothing, match = ExApplication (ExAny (Slot \"n\" 0)) (ArTau !t (ExMeta \"n1\")), ematch = ExMeta \"e1\", nresult = ExMeta \"n2\", when = Just (Not (Absolute (ExMeta \"n1\"))), premises = [Premise {result = \"n2\", operation = OpMorph ExTermination (ExMeta \"e1\")}]}", "MorphRule {name = \"md\", label = Nothing, match = ExDispatch (ExMeta \"n1\") !t1, ematch = ExMeta \"e1\", nresult = ExMeta \"n4\", when = Just (Not (IsFormation (ExMeta \"n1\"))), premises = [Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")},Premise {result = \"n3\", operation = OpNormalize (ExDispatch (ExMeta \"n2\") !t1)},Premise {result = \"n4\", operation = OpMorph (ExMeta \"n3\") (ExMeta \"e1\")}]}", "MorphRule {name = \"mf\", label = Nothing, match = ExFormation [BiMeta \"B1\"], ematch = ExMeta \"e1\", nresult = ExFormation [BiMeta \"B1\"], when = Nothing, premises = []}", "MorphRule {name = \"mg\", label = Nothing, match = ExRoot, ematch = ExRoot, nresult = ExMeta \"n1\", when = Nothing, premises = [Premise {result = \"n1\", operation = OpMorph ExTermination ExRoot}]}", "MorphRule {name = \"ml\", label = Just \"\\\\lambda\", match = ExDispatch (ExFormation [BiMeta \"B1\",BiLambda (FnMeta \"F1\"),BiMeta \"B2\"]) !t1, ematch = ExMeta \"e1\", nresult = ExMeta \"n3\", when = Nothing, premises = [Premise {result = \"n1\", operation = OpEvaluate (ExFormation [BiMeta \"B1\",BiLambda (FnMeta \"F1\"),BiMeta \"B2\"]) (ExMeta \"e1\")},Premise {result = \"n2\", operation = OpNormalize (ExDispatch (ExMeta \"n1\") !t1)},Premise {result = \"n3\", operation = OpMorph (ExMeta \"n2\") (ExMeta \"e1\")}]}", "MorphRule {name = \"mphi\", label = Just \"\\\\varphi\", match = ExDispatch (ExFormation [BiMeta \"B1\"]) !t1, ematch = ExMeta \"e1\", nresult = ExMeta \"n2\", when = Just (And [In [\966] [BiMeta \"B1\"],Disjoint [!t1,\955] [BiMeta \"B1\"]]), premises = [Premise {result = \"n1\", operation = OpNormalize (ExDispatch (ExDispatch (ExFormation [BiMeta \"B1\"]) \966) !t1)},Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")}]}", "MorphRule {name = \"universe\", label = Just \"\\\\Phi\", match = ExRoot, ematch = ExMeta \"e1\", nresult = ExMeta \"n2\", when = Just (Not (Eq (CmpExpr (ExMeta \"e1\")) (CmpExpr ExRoot))), premises = [Premise {result = \"n1\", operation = OpNormalize (ExMeta \"e1\")},Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")}]}", "MorphRule {name = \"xi\", label = Nothing, match = ExXi, ematch = ExMeta \"e1\", nresult = ExMeta \"n1\", when = Nothing, premises = [Premise {result = \"n1\", operation = OpMorph ExTermination (ExMeta \"e1\")}]}", "DataizeRule {name = \"box\", label = Nothing, match = ExFormation [BiMeta \"B1\",BiTau \966 (ExMeta \"e2\"),BiMeta \"B2\"], ematch = ExMeta \"e1\", dresult = BtMeta \"d1\", when = Just (Disjoint [\916,\955] [BiMeta \"B1\",BiMeta \"B2\"]), premises = [Premise {result = \"e3\", operation = OpContextualize (ExMeta \"e2\") (ExFormation [BiMeta \"B1\",BiTau \966 (ExMeta \"e2\"),BiMeta \"B2\"])},Premise {result = \"n1\", operation = OpNormalize (ExMeta \"e3\")},Premise {result = \"d1\", operation = OpDataize (ExMeta \"n1\") (ExMeta \"e1\")}]}", "DataizeRule {name = \"delta\", label = Just \"\\\\Delta\", match = ExFormation [BiMeta \"B1\",BiDelta (BtMeta \"d1\"),BiMeta \"B2\"], ematch = ExMeta \"e1\", dresult = BtMeta \"d1\", when = Just (Disjoint [\955] [BiMeta \"B1\",BiMeta \"B2\"]), premises = []}", "DataizeRule {name = \"fire\", label = Nothing, match = ExFormation [BiMeta \"B1\",BiLambda (FnMeta \"F1\"),BiMeta \"B2\"], ematch = ExMeta \"e1\", dresult = BtMeta \"d1\", when = Just (Disjoint [\916] [BiMeta \"B1\",BiMeta \"B2\"]), premises = [Premise {result = \"n1\", operation = OpEvaluate (ExFormation [BiMeta \"B1\",BiLambda (FnMeta \"F1\"),BiMeta \"B2\"]) (ExMeta \"e1\")},Premise {result = \"d1\", operation = OpDataize (ExMeta \"n1\") (ExMeta \"e1\")}]}", "DataizeRule {name = \"none\", label = Nothing, match = ExFormation [BiMeta \"B1\"], ematch = ExMeta \"e1\", dresult = BtMeta \"d1\", when = Just (Disjoint [\916,\955,\966] [BiMeta \"B1\"]), premises = [Premise {result = \"d1\", operation = OpDataize ExTermination (ExMeta \"e1\")}]}", "DataizeRule {name = \"norm\", label = Nothing, match = ExMeta \"n1\", ematch = ExMeta \"e1\", dresult = BtMeta \"d1\", when = Just (And [Not (IsFormation (ExMeta \"n1\")),Not (Eq (CmpExpr (ExMeta \"n1\")) (CmpExpr ExTermination))]), premises = [Premise {result = \"n2\", operation = OpMorph (ExMeta \"n1\") (ExMeta \"e1\")},Premise {result = \"d1\", operation = OpDataize (ExMeta \"n2\") (ExMeta \"e1\")}]}"] -- Whether the term is a normal form: no built-in rule of normalization -- matches anywhere inside it. @@ -487,9 +487,10 @@ dataizationDelta term _ = [ In.Concludes (In.Answered (D.Dataization, "delta") x6) | ExFormation x1 <- [term] - , (_, x3) <- M.splits x1 - , (x4 : _) <- [x3] + , (x2, x3) <- M.splits x1 + , (x4 : x5) <- [x3] , BiDelta x6 <- [x4] + , not (any (`Ru.presentIn` concat [x2, x5]) [AtLambda]) ] -- The dataization rule 'fire'. @@ -501,6 +502,7 @@ , (x4 : x5) <- [x3] , BiLambda x6 <- [x4] , M.named x6 + , not (any (`Ru.presentIn` concat [x2, x5]) [AtDelta]) ] -- The dataization rule 'none'. diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino -version: 0.0.145 +version: 0.0.147 license: MIT synopsis: Command-Line Manipulator of πœ‘-Calculus Expressions description: Please see the README on GitHub at diff --git a/resources/dataization/delta.yaml b/resources/dataization/delta.yaml --- a/resources/dataization/delta.yaml +++ b/resources/dataization/delta.yaml @@ -6,3 +6,7 @@ match: ⟦𝐡1, Ξ” ‍ 𝛿1, 𝐡2⟧ universe: 𝑒1 conclusion: 𝛿1 +when: + disjoint: + - [Ξ»] + - [𝐡1, 𝐡2] diff --git a/resources/dataization/fire.yaml b/resources/dataization/fire.yaml --- a/resources/dataization/fire.yaml +++ b/resources/dataization/fire.yaml @@ -5,6 +5,10 @@ match: ⟦𝐡1, Ξ» ‍ 𝑓1, 𝐡2⟧ universe: 𝑒1 conclusion: 𝛿1 +when: + disjoint: + - [Ξ”] + - [𝐡1, 𝐡2] premises: - n-result: 𝑛1 evaluate: diff --git a/src/Bytes.hs b/src/Bytes.hs --- a/src/Bytes.hs +++ b/src/Bytes.hs @@ -67,9 +67,7 @@ | c >= 'A' && c <= 'F' = fromIntegral (ord c - ord 'A' + 10) | c >= 'a' && c <= 'f' = fromIntegral (ord c - ord 'a' + 10) | otherwise = error ("Invalid hex digit: " ++ [c]) -hexByte bt = case readHex bt of - [(hex, "")] -> fromIntegral (hex :: Integer) - _ -> error $ "Invalid hex byte; " ++ bt +hexByte bt = error $ "Invalid hex byte; " ++ bt word8ToBytes :: [Word8] -> Bytes word8ToBytes [] = BtEmpty diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs --- a/src/CLI/Helpers.hs +++ b/src/CLI/Helpers.hs @@ -12,7 +12,7 @@ import CLI.Types import CLI.Validators (invalidCLIArguments) import CST (EXPRESSION) -import Canonizer (canonize, canonizeExpr) +import Canonizer (canonizeExpr, lambdaNames) import Compiled (compiled) import Control.Exception import Control.Monad ((>=>)) @@ -27,6 +27,7 @@ import Encoding import Engine (Engine, fresh, yaml) import Files (ensuredFile, overwrite) +import qualified Filter as F import Functions (buildFunctions, execFunctions) import GHC.Clock (getMonotonicTime) import LaTeX (LatexContext (LatexContext), defaultMeetLength, defaultMeetPopularity, expressionToLaTeX, rewrittensToLatex) @@ -38,13 +39,13 @@ import Parser (parseExpressionThrows) import qualified Printer as P import qualified Random as R -import Rewriter (Rewritten, Rewrittens', stepHeaders) +import Rewriter (Rewrittens', stepHeaders) import Sugar (SugarType (SALTY), withoutRho) import System.Directory (createDirectoryIfMissing) import System.FilePath (takeDirectory, takeExtension) import System.IO (Handle, IOMode (WriteMode), getContents', hClose, hSetEncoding, openFile, utf8) import Text.Printf (printf) -import XMIR (Atoms, expressionToXMIR, parseXMIRThrows, printXMIR, xmirAtoms, xmirToPhi) +import XMIR (Atoms, expressionToXMIR, parseXMIRThrows, printXMIR, renameAtoms, xmirAtoms, xmirToPhi) import Yaml (normalizationRules) import qualified Yaml as Y @@ -54,14 +55,16 @@ justMeetLength :: Maybe Int -> Int justMeetLength = fromMaybe defaultMeetLength -saveStepFunc :: Maybe FilePath -> PrintContext -> IO SaveStepFunc -saveStepFunc stepsDir ctx@PrintCtx{..} = do +saveStepFunc :: Maybe FilePath -> PrintContext -> [Expression] -> [Expression] -> IO SaveStepFunc +saveStepFunc stepsDir ctx@PrintCtx{..} included excluded = do counter <- newIORef (0 :: Int) let ioToExt :: String ioToExt | _outputFormat == LATEX = "tex" | otherwise = show _outputFormat - render = printInFormat ctx + render expr = do + shown <- F.include' expr included + printInFormat ctx ((if _canonize then canonizeExpr else id) (F.exclude' shown excluded)) save :: SaveStepFunc save expr = do step <- atomicModifyIORef' counter (\value -> (value + 1, value + 1)) @@ -165,10 +168,8 @@ printRewrittens :: PrintContext -> Rewrittens' -> IO String printRewrittens ctx@PrintCtx{..} rewrittens@(chain, _) | _outputFormat == LATEX && _sequence = rewrittensToLatex rewrittens (printCtxToLatexCtx ctx) - | otherwise = withHeaders <$> mapM (printFocused ctx . fst) (canonized chain) + | otherwise = withHeaders <$> mapM (printAnswer ctx . fst) chain where - canonized :: [Rewritten] -> [Rewritten] - canonized = if _canonize then canonize else id withHeaders :: [String] -> String withHeaders rendered | _headers && _sequence = intercalate "\n" (zipWith prefixed (stepHeaders chain) rendered) @@ -178,7 +179,12 @@ prefixed = printf "\n%s\n%s" printAnswer :: PrintContext -> Expression -> IO String -printAnswer ctx@PrintCtx{..} expr = printFocused ctx (if _canonize then canonizeExpr expr else expr) +printAnswer ctx@PrintCtx{..} expr + | _canonize = printFocused ctx{_xmirCtx = renameAtoms (zip (lambdaNames expr) (lambdaNames canonized)) _xmirCtx} canonized + | otherwise = printFocused ctx expr + where + canonized :: Expression + canonized = canonizeExpr expr printFocused :: PrintContext -> Expression -> IO String printFocused ctx@PrintCtx{..} expr @@ -198,7 +204,24 @@ LATEX -> pure (expressionToLaTeX expr (printCtxToLatexCtx ctx)) printPhi :: PrintContext -> Expression -> String -printPhi ctx@PrintCtx{..} expr = P.printExpressionWith (hidden ctx) expr (_sugar, UNICODE, _line, _margin) +printPhi PrintCtx{..} expr = P.printExpression' (if _hideRho then rholess expr else expr) (_sugar, UNICODE, _line, _margin) + where + rholess :: Expression -> Expression + rholess (ExFormation bds) = ExFormation [binding bd | bd <- bds, not (rho bd)] + rholess (ExDispatch inner attr) = ExDispatch (rholess inner) attr + rholess (ExApplication inner (ArTau AtRho _)) = rholess inner + rholess (ExApplication inner (ArTau attr arg)) = ExApplication (rholess inner) (ArTau attr (rholess arg)) + rholess (ExApplication inner (ArAlpha alpha arg)) = ExApplication (rholess inner) (ArAlpha alpha (rholess arg)) + rholess (ExPhiMeet prefix idx inner) = ExPhiMeet prefix idx (rholess inner) + rholess (ExPhiAgain prefix idx inner) = ExPhiAgain prefix idx (rholess inner) + rholess other = other + binding :: Binding -> Binding + binding (BiTau attr inner) = BiTau attr (rholess inner) + binding other = other + rho :: Binding -> Bool + rho (BiTau AtRho _) = True + rho (BiVoid AtRho) = True + rho _ = False hidden :: PrintContext -> SugarType -> EXPRESSION -> EXPRESSION hidden PrintCtx{..} sugar diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs --- a/src/CLI/Parsers.hs +++ b/src/CLI/Parsers.hs @@ -249,8 +249,9 @@ <> help "Path to the YAML file of Ξ» functions this run may fire, each entry keyed by a regular expression \ \over Ξ» names under \"Ξ»\", naming the operands it brings down to data under \"dataize\", the ones \ - \it reduces to a normal form under \"morph\" and the terms of those it stands the data of into \ - \unknowns under \"symbolize\", and answering with the term under \"𝑛\"" + \it reduces to a normal form under \"morph\", the terms it rewrites by rules of its own under \ + \\"rewrite\", the terms of those it stands the data of into unknowns under \"symbolize\" and the \ + \pairs of branches it joins into one term under \"join\", and answering with the term under \"𝑛\"" ) ) diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -73,7 +73,7 @@ printCtx = toPrintCtx xmirCtx foc exclude = (`F.exclude` excluded) include = (`F.include` included) - save <- saveStepFunc _stepsDir printCtx + save <- saveStepFunc _stepsDir printCtx included excluded let steps = map (stepOf linked) rules (rewrittens, exceeded) <- rewrite expr steps (RewriteContext loc _maxDepth _maxCycles _depthSensitive Nothing (building linked) linked._normal (every steps) _must _breakpoint save) rewrittens' <- exclude <$> include (if _sequence then NE.toList rewrittens else [NE.last rewrittens]) @@ -86,6 +86,9 @@ when (_inPlace && isNothing _inputFile) (invalidCLIArguments "The option --in-place requires an input file") when (_inPlace && isJust _targetFile) (invalidCLIArguments "The options --in-place and --target cannot be used together") when (_inPlace && _outputFormat /= PHI) (invalidCLIArguments "The option --in-place can only be used together with --output=phi") + when (_inPlace && _sequence) (invalidCLIArguments "The options --in-place and --sequence cannot be used together, since the file must keep one program") + when (_inPlace && _focus /= "Q") (invalidCLIArguments "The options --in-place and --focus cannot be used together, since the file must keep the whole program") + when (_inPlace && not (null _show)) (invalidCLIArguments "The options --in-place and --show cannot be used together, since the file must keep the whole program") when (_update && _inPlace) (invalidCLIArguments "The options --update and --in-place cannot be used together") when (_update && isNothing _targetFile) (invalidCLIArguments "The option --update requires --target") when (_update && isNothing _inputFile) (invalidCLIArguments "The option --update requires an input file") @@ -168,7 +171,7 @@ let printCtx = toPrintCtx atoms foc exclude = (`F.exclude` excluded) include = (`F.include` included) - save <- saveStepFunc _stepsDir printCtx + save <- saveStepFunc _stepsDir printCtx included excluded tally <- tallied _maxFirings memo <- memoized _acyclic linked <- engine @@ -247,7 +250,7 @@ let printCtx = toPrintCtx atoms foc exclude = (`F.exclude` excluded) include = (`F.include` included) - save <- saveStepFunc _stepsDir printCtx + save <- saveStepFunc _stepsDir printCtx included excluded tally <- tallied _maxFirings memo <- memoized _acyclic linked <- engine @@ -261,12 +264,19 @@ heading record printCtx Morphing aiming._locator morph universe (started universe) aiming ) + printed <- + if _quiet + then pure Nothing + else do + answer <- (`F.exclude'` excluded) <$> F.include' (if foc == ExRoot then morphed else maybe morphed fst (lastMaybe chain)) included + validateXmirTopLevel _outputFormat answer + Just <$> printAnswer printCtx answer when _sequence (include chain >>= \shown -> printRewrittens printCtx (exclude shown, False) >>= putStrLn) - unless _quiet $ do - answer <- (`F.exclude'` excluded) <$> F.include' morphed included - validateXmirTopLevel _outputFormat answer - printAnswer printCtx answer >>= putStrLn + mapM_ putStrLn printed where + lastMaybe :: [a] -> Maybe a + lastMaybe [] = Nothing + lastMaybe items = Just (last items) validateOpts :: IO () validateOpts = do validateLatexOptions @@ -327,6 +337,7 @@ when (selected == 0 && null _rules && not _normalize) (invalidCLIArguments "Either --rule, --normalize, --morph, --dataize or --contextualize must be specified") when (selected > 1) (invalidCLIArguments "Only one of --morph, --dataize or --contextualize can be specified") when (selected == 1 && not (null _rules)) (invalidCLIArguments "The --rule option cannot be used together with --morph, --dataize or --contextualize") + when (selected == 1 && _normalize) (invalidCLIArguments "The --normalize option cannot be used together with --morph, --dataize or --contextualize") runMerge :: OptsMerge -> IO () runMerge OptsMerge{..} = do @@ -370,6 +381,7 @@ runMatch :: OptsMatch -> IO () runMatch OptsMatch{..} = do + when (isJust _when && isNothing _pattern) (invalidCLIArguments "The option --when requires --pattern, since there is nothing to check it against") setStdGen (mkStdGen _seed) input <- readInput _inputFile expr <- parseInput input PHI diff --git a/src/CLI/Validators.hs b/src/CLI/Validators.hs --- a/src/CLI/Validators.hs +++ b/src/CLI/Validators.hs @@ -8,7 +8,9 @@ import Control.Exception import Control.Monad (forM_, when, (>=>)) import Data.Foldable (for_) +import Data.List (isPrefixOf) import Data.Maybe (isJust) +import Misc (fqnToAttrs) import Must import Parser (parseExpressionThrows) import Printer @@ -37,7 +39,7 @@ validateNoOverlap :: String -> [Expression] -> String -> [Expression] -> IO () validateNoOverlap showOpt shown hideOpt hidden = for_ shown $ \shown' -> - for_ hidden $ \hidden' -> + for_ hidden $ \hidden' -> do when (printExpression shown' == printExpression hidden') $ invalidCLIArguments ( printf @@ -46,6 +48,19 @@ (printExpression shown') hideOpt ) + when (inside (fqnToAttrs shown') (fqnToAttrs hidden')) $ + invalidCLIArguments + ( printf + "The --%s locator '%s' lies inside the --%s locator '%s', which would hide it from the result" + showOpt + (printExpression shown') + hideOpt + (printExpression hidden') + ) + where + inside :: Maybe [Attribute] -> Maybe [Attribute] -> Bool + inside (Just inner) (Just outer) = length outer < length inner && outer `isPrefixOf` inner + inside _ _ = False validateLatexOptions :: IOFormat -> [(Bool, String)] -> [(Maybe String, String)] -> [(Maybe Int, String)] -> IO () validateLatexOptions LATEX _ _ _ = pure () diff --git a/src/CST.hs b/src/CST.hs --- a/src/CST.hs +++ b/src/CST.hs @@ -263,6 +263,8 @@ expressionToCSTFrom tabs expr = toCST expr (tabs, EOL) sweetNumber :: Bytes -> Bool +sweetNumber (BtMeta _) = False +sweetNumber (BtAny _) = False sweetNumber bts | btsSize bts /= 8 = False sweetNumber bts = case btsToNum bts of @@ -270,7 +272,9 @@ _ -> True sweetString :: Bytes -> Bool -sweetString = btsIsUtf8 +sweetString (BtMeta _) = False +sweetString (BtAny _) = False +sweetString bts = btsIsUtf8 bts sweetCollapsible :: Expression -> Bool sweetCollapsible (DataNumber bts) = sweetNumber bts @@ -365,27 +369,39 @@ in if length ts' == 1 && dataPrimitive obj && sweetCollapsible obj then applicationToPrimitive obj tabs rs else - if null exs + if length ts' > 1 && null exs && dataPrimitive obj && sweetCollapsible obj then EX_APPLICATION - ex' + (applicationToPrimitive obj tabs rs) NO_SPACE eol (TAB next) - (AA_TAUS (toCST ts (next, eol) :: BINDING)) + (AA_TAUS (toCST (drop 1 ts') (next, eol) :: BINDING)) eol (TAB tabs) next else - EX_APPLICATION - ex' - NO_SPACE - eol - (TAB next) - (AA_EXPRS (toCST exs (next, eol))) - eol - (TAB tabs) - next + if null exs + then + EX_APPLICATION + ex' + NO_SPACE + eol + (TAB next) + (AA_TAUS (toCST ts (next, eol) :: BINDING)) + eol + (TAB tabs) + next + else + EX_APPLICATION + ex' + NO_SPACE + eol + (TAB next) + (AA_EXPRS (toCST exs (next, eol))) + eol + (TAB tabs) + next where primitives :: [T.Text] primitives = ["number", "string"] diff --git a/src/Canonizer.hs b/src/Canonizer.hs --- a/src/Canonizer.hs +++ b/src/Canonizer.hs @@ -1,7 +1,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Canonizer (canonize, canonizeExpr) where +module Canonizer (canonize, canonizeExpr, lambdaNames) where import AST import qualified Data.Text as T @@ -50,6 +50,20 @@ canonizeArgument (ArAlpha alpha expr) idx = let (expr', idx') = canonizeExpression expr idx in (ArAlpha alpha expr', idx') + +lambdaNames :: Expression -> [T.Text] +lambdaNames (ExFormation bds) = concatMap named bds + where + named :: Binding -> [T.Text] + named (BiLambda (Function name)) = [name] + named (BiTau _ expr) = lambdaNames expr + named _ = [] +lambdaNames (ExDispatch expr _) = lambdaNames expr +lambdaNames (ExApplication expr (ArTau _ arg)) = lambdaNames expr ++ lambdaNames arg +lambdaNames (ExApplication expr (ArAlpha _ arg)) = lambdaNames expr ++ lambdaNames arg +lambdaNames (ExPhiMeet _ _ expr) = lambdaNames expr +lambdaNames (ExPhiAgain _ _ expr) = lambdaNames expr +lambdaNames _ = [] canonizeExpr :: Expression -> Expression canonizeExpr expr = fst (canonizeExpression expr 1) diff --git a/src/Condition.hs b/src/Condition.hs --- a/src/Condition.hs +++ b/src/Condition.hs @@ -6,6 +6,7 @@ module Condition (parseCondition, parseConditionThrows) where +import AST (Attribute (AtDelta, AtLambda)) import Control.Exception (Exception) import Data.Void (Void) import Misc (orThrow) @@ -42,6 +43,9 @@ comma :: Parser String comma = symbol "," +several :: Parser a -> Parser [a] +several item = choice [try (between (symbol "[") (symbol "]") (item `sepBy1` comma)), pure <$> item] + number :: Parser Y.Number number = choice @@ -59,13 +63,10 @@ , do sign <- optional (choice [char '-', char '+']) unsigned <- lexeme L.decimal - return - ( Y.Literal - ( case sign of - Just '-' -> negate unsigned - _ -> unsigned - ) - ) + let signed = if sign == Just '-' then negate unsigned else unsigned :: Integer + if signed < toInteger (minBound :: Int) || signed > toInteger (maxBound :: Int) + then fail (printf "the literal %d does not fit into Int" signed) + else return (Y.Literal (fromInteger signed)) ] comparable :: Parser Y.Comparable @@ -91,11 +92,11 @@ return (Y.Or args) , do _ <- symbol "in" >> lparen - attr <- _attribute phiParser + attrs <- several (choice [AtLambda <$ symbol "Ξ»", AtDelta <$ symbol "Ξ”", _attribute phiParser]) _ <- comma - bd <- _binding phiParser + bds <- several (_binding phiParser) _ <- rparen - return (Y.In [attr] [bd]) + return (Y.In attrs bds) , do _ <- symbol "not" >> lparen cond <- condition diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -38,10 +38,15 @@ result <- try (dataize' (expr, (universe, Nothing) :| []) universe state ctx) case result of Right ((bytes, seq), state') -> pure (Dataized bytes, reverse seq, state') - Left (StuckAt func seq parked) | _partial -> pure (Residual (fst (NE.head seq)), reverse (NE.toList seq), parked{_stuck = Just func}) - Left (OutOfStepsAt _ seq parked) | _partial -> pure (Residual (fst (NE.head seq)), reverse (NE.toList seq), parked) - Left (LoopingAt _ seq parked) | _partial -> pure (Residual (fst (NE.head seq)), reverse (NE.toList seq), parked) + Left (StuckAt func seq parked) | _partial -> residual seq parked{_stuck = Just func} + Left (OutOfStepsAt _ seq parked) | _partial -> residual seq parked + Left (LoopingAt _ seq parked) | _partial -> residual seq parked Left failure -> throwIO (failure :: ReduceException) + where + residual :: NonEmpty Rewritten -> State -> IO (Outcome, [Rewritten], State) + residual seq parked = do + residue <- locatedExpression _locator (fst (NE.head seq)) + pure (Residual residue, reverse (NE.toList seq), parked) dataize' :: Dataizable -> Expression -> State -> ReduceContext -> IO (Dataized, State) dataize' (expr, seq) univ state caller = do diff --git a/src/Deps.hs b/src/Deps.hs --- a/src/Deps.hs +++ b/src/Deps.hs @@ -17,7 +17,7 @@ import GHC.Clock (getMonotonicTime) import Logger (logDebug, logInfo) import Matcher -import Printer (printBytes, printFunction) +import Printer (printAttribute, printFunction) import System.Directory (createDirectoryIfMissing) import System.FilePath import System.IO (Handle, hPutStrLn) @@ -98,6 +98,7 @@ | EvStuckOn Int T.Text | EvStarved Int Int Judgment Expression | EvTimeout Int Int Judgment Expression + | EvSpent Int Int Judgment Expression | EvData Int T.Text Expression (Either Int Bytes) | EvTerm Int T.Text Expression Expression | EvSymbolize Int T.Text Expression Expression @@ -106,6 +107,7 @@ | EvJoined Int Int (Int, Int) | EvTerminate Int (Maybe (Either Int Bytes)) T.Text T.Text | EvMinted Int Int [Either Int Bytes] + | EvDeferred Int Int Judgment Expression (Maybe Expression) Expression | EvBuilt Int Expression | EvAnswer Int Expression @@ -121,6 +123,7 @@ record (EvStuck depth key judgment self) = EvStuck depth key judgment (term self) record (EvStarved depth limit judgment site) = EvStarved depth limit judgment (term site) record (EvTimeout depth limit judgment site) = EvTimeout depth limit judgment (term site) + record (EvSpent depth limit judgment site) = EvSpent depth limit judgment (term site) record (EvData depth spelling operand value) = EvData depth spelling (term operand) (datum value) record (EvTerm depth spelling operand value) = EvTerm depth spelling (term operand) (term value) record (EvSymbolize depth spelling source value) = EvSymbolize depth spelling (term source) (term value) @@ -129,6 +132,7 @@ record (EvJoined depth fresh (one, two)) = EvJoined depth (symbol fresh) (symbol one, symbol two) record (EvTerminate depth condition side raising) = EvTerminate depth (fmap datum condition) side raising record (EvMinted depth sym operands) = EvMinted depth (symbol sym) (map datum operands) + record (EvDeferred depth sym judgment copy call site) = EvDeferred depth (symbol sym) judgment (term copy) (fmap term call) (term site) record (EvBuilt depth value) = EvBuilt depth (term value) record (EvAnswer depth value) = EvAnswer depth (term value) record other = other @@ -216,6 +220,9 @@ written (EvTimeout depth limit judgment site) protocol = do locator <- render site pure (protocol, Just (indented depth (printf "timeout(%d) # %s(%s)" limit (letter judgment) locator))) + written (EvSpent depth limit judgment site) protocol = do + locator <- render site + pure (protocol, Just (indented depth (printf "spent(%d) # %s(%s)" limit (letter judgment) locator))) written (EvData depth spelling operand value) protocol = do datum <- spelled value line <- commented (printf "%s := %s" (labelled protocol depth spelling) datum) Dataization operand @@ -223,7 +230,7 @@ where spelled :: Either Int Bytes -> IO String spelled (Left symbol) = printf "𝔻(%s)" <$> render (standing symbol) - spelled (Right bytes) = pure (printBytes bytes) + spelled (Right bytes) = render (ExBytes bytes) written (EvTerm depth spelling operand term) protocol = do let naming = labelled protocol depth spelling (protocol', value) <- valued protocol naming term @@ -236,7 +243,8 @@ pure (protocol', Just (indented depth line)) written (EvKnown depth symbol bytes) protocol = do form <- render (standing symbol) - pure (protocol, Just (indented depth (printf "𝔻(%s) == %s" form (printBytes bytes)))) + value <- render (ExBytes bytes) + pure (protocol, Just (indented depth (printf "𝔻(%s) == %s" form value))) written (EvJoin depth spelling (left, right) term) protocol = do let naming = labelled protocol depth spelling (protocol', value) <- valued protocol naming term @@ -252,8 +260,12 @@ where spelled :: Either Int Bytes -> IO String spelled (Left symbol) = printf "𝔻(%s)" <$> render (standing symbol) - spelled (Right bytes) = pure (printBytes bytes) + spelled (Right bytes) = render (ExBytes bytes) written EvMinted{} protocol = pure (protocol, Nothing) + written (EvDeferred depth symbol judgment copy call site) protocol = do + form <- render (fromMaybe copy call) + locator <- render site + pure (protocol, Just (indented depth (printf "deferred(%s) := %s # %s(%s)" (printFunction (FnSymbol symbol)) form (letter judgment) locator))) written (EvBuilt depth term) protocol = do value <- borrowed protocol term pure (protocol, Just (indented depth (printf "%s.1 := %s # %s" (labelled protocol depth answer) value (T.unpack answer)))) @@ -356,6 +368,10 @@ locator <- render site let (kept, closers) = closed depth nesting._closing pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "" limit (opened judgment) (escapeXML locator))]) + elements (EvSpent depth limit judgment site) nesting = do + locator <- render site + let (kept, closers) = closed depth nesting._closing + pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "" limit (opened judgment) (escapeXML locator))]) elements (EvData depth spelling _ value) nesting = do record <- stood value pure (nesting{_closing = kept}, closers ++ [indentedXml depth record]) @@ -365,7 +381,9 @@ stood (Left symbol) = do form <- render (standing symbol) pure (printf "%s" (escapeXML (labelled nesting depth spelling)) (escapeXMLText form)) - stood (Right bytes) = pure (printf "%s" (escapeXML (labelled nesting depth spelling)) (escapeXMLText (printBytes bytes))) + stood (Right bytes) = do + form <- render (ExBytes bytes) + pure (printf "%s" (escapeXML (labelled nesting depth spelling)) (escapeXMLText form)) elements (EvTerm depth spelling _ term) nesting = do body <- render term let (kept, closers) = closed depth nesting._closing @@ -374,12 +392,10 @@ body <- render term let (kept, closers) = closed depth nesting._closing pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "%s" (escapeXML (labelled nesting depth spelling)) (escapeXMLText body))]) - elements (EvKnown depth symbol bytes) nesting = - pure (nesting{_closing = kept}, closers ++ [indentedXml depth known]) - where - (kept, closers) = closed depth nesting._closing - known :: String - known = printf "%s" (sigma symbol) (escapeXMLText (printBytes bytes)) + elements (EvKnown depth symbol bytes) nesting = do + value <- render (ExBytes bytes) + let (kept, closers) = closed depth nesting._closing + pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "%s" (sigma symbol) (escapeXMLText value))]) elements (EvJoin depth spelling _ term) nesting = do body <- render term let (kept, closers) = closed depth nesting._closing @@ -390,26 +406,45 @@ (kept, closers) = closed depth nesting._closing joint :: String joint = printf "%s %s" (sigma fresh) (sigma one) (sigma two) - elements (EvTerminate depth condition side _) nesting = + elements (EvTerminate depth condition side _) nesting = do + terminal <- case condition of + Just (Left symbol) -> pure (printf "" (sigma symbol) (quoted side)) + Just (Right bytes) -> printf "%s" (quoted side) . escapeXMLText <$> render (ExBytes bytes) + Nothing -> pure (printf "" (quoted side)) + let (kept, closers) = closed depth nesting._closing pure (nesting{_closing = kept}, closers ++ [indentedXml depth terminal]) - where - (kept, closers) = closed depth nesting._closing - terminal :: String - terminal = case condition of - Just (Left symbol) -> printf "" (sigma symbol) (quoted side) - Just (Right bytes) -> printf "%s" (quoted side) (escapeXMLText (printBytes bytes)) - Nothing -> printf "" (quoted side) - elements (EvMinted depth symbol operands) nesting = + elements (EvMinted depth symbol operands) nesting = do + spelledOperands <- mapM spelled operands + let (kept, closers) = closed depth nesting._closing + mint :: String + mint + | null operands = printf "" (sigma symbol) + | otherwise = printf "%s" (sigma symbol) (escapeXMLText (unwords spelledOperands)) pure (nesting{_closing = kept}, closers ++ [indentedXml depth mint]) where - (kept, closers) = closed depth nesting._closing - mint :: String - mint - | null operands = printf "" (sigma symbol) - | otherwise = printf "%s" (sigma symbol) (escapeXMLText (unwords (map spelled operands))) - spelled :: Either Int Bytes -> String - spelled (Left fresh) = sigma fresh - spelled (Right bytes) = printBytes bytes + spelled :: Either Int Bytes -> IO String + spelled (Left fresh) = pure (sigma fresh) + spelled (Right bytes) = render (ExBytes bytes) + elements (EvDeferred depth symbol judgment copy call site) nesting = do + form <- render copy + locator <- render site + (origin, given) <- maybe (pure ("", "")) called call + let (kept, closers) = closed depth nesting._closing + pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "%s%s" (sigma symbol) (opened judgment) (escapeXML locator) origin given (escapeXMLText form))]) + where + called :: Expression -> IO (String, String) + called term = do + let (object, arguments) = invoked term + path <- render object + pure (printf " of=\"%s\"" (escapeXML path), printf "%s" (concat arguments)) + invoked :: Expression -> (Expression, [String]) + invoked (ExApplication term (ArTau attr value)) = + let (object, arguments) = invoked term + in (object, arguments ++ [printf "%s" (escapeXML (printAttribute attr)) (escapeXMLText (valued value))]) + invoked term = (term, []) + valued :: Expression -> String + valued (ExFormation [BiLambda (FnSymbol idx)]) = sigma idx + valued _ = "?" elements (EvBuilt depth term) nesting = do body <- render term let (kept, closers) = closed depth nesting._closing diff --git a/src/Evaluate.hs b/src/Evaluate.hs --- a/src/Evaluate.hs +++ b/src/Evaluate.hs @@ -19,7 +19,7 @@ import Engine (Engine (..)) import Lambdas (Lambda (..), Meta (..), joined, matched, minted, symbolized) import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot) -import Morph (Answer, Kept (..), ReduceContext (..), ReduceException (..), Steps (..), charged, counted, deeper, enter, isLambda, lambda, morph', morphing, normalized, recalled, retained, starved, unparked) +import Morph (Answer, Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), charged, counted, deeper, enter, isLambda, lambda, morphing, normalized, recalled, remember, remembered, retained, settled, starved, unparked) import Printer (printFunction) import Rule (RuleContext (RuleContext), matchExpressionWithRule') import Text.Printf (printf) @@ -69,11 +69,10 @@ let ctx = caller{_nesting = caller._nesting + 1} outcome <- try $ do (bound, dataized, conditions) <- foldM (down ctx) (substEmpty, state, []) entry._dataized - (bound', morphed) <- foldM (through ctx) (bound, dataized) entry._morphed - rewrote <- foldM (reshaped ctx) bound' entry._rewritten - (bound'', stood) <- foldM (masked ctx) (rewrote, morphed) entry._symbolized - (bound''', forked) <- foldM (paired ctx (listToMaybe (reverse conditions))) (bound'', stood) entry._paired - answered ctx entry (reverse conditions) bound''' forked + (bound', morphed, normals) <- foldM (through ctx) (bound, dataized, []) entry._morphed + let firing = Firing func (reverse conditions) (reverse normals) + known <- remembered caller._memo firing + maybe (worked ctx entry firing bound' morphed) (\answer -> (answer, morphed) <$ shown ctx._nesting answer) known case outcome of Right (answer, state') -> do retained caller._memo form stamp (Answered answer) @@ -83,6 +82,18 @@ mapM_ (retained caller._memo form stamp) (kept (exhausted' /= exhausted) failure) mapM_ (caller._saveEval . EvStuckOn (caller._nesting + 1)) (stranded failure) throwIO failure + worked :: ReduceContext -> Lambda -> Firing -> Subst -> State -> IO (Answer, State) + worked ctx entry firing@(Firing _ operands _) bound state' = do + rewrote <- foldM (reshaped ctx) bound entry._rewritten + (bound', stood) <- foldM (masked ctx) (rewrote, state') entry._symbolized + (bound'', forked) <- foldM (paired ctx (listToMaybe operands)) (bound', stood) entry._paired + (answer, state'') <- answered ctx entry operands bound'' forked + remember caller._memo firing answer + pure (answer, state'') + shown :: Int -> Answer -> IO () + shown depth (built, normal) = do + caller._saveEval (EvBuilt depth built) + caller._saveEval (EvAnswer depth normal) kept :: Bool -> ReduceException -> Maybe Kept kept _ (Looping term) = Just (Looped term) kept _ (LoopingAt term _ _) = Just (Looped term) @@ -97,11 +108,10 @@ stranded (StuckAt name _ _) = Just name stranded _ = Nothing told :: Kept -> IO (Expression, State) - told (Answered (built, normal)) = do + told (Answered answer) = do caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site) - caller._saveEval (EvBuilt (caller._nesting + 1) built) - caller._saveEval (EvAnswer (caller._nesting + 1) normal) - pure (normal, state) + shown (caller._nesting + 1) answer + pure (snd answer, state) told (Looped term) = do caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site) mapM_ (\mode -> caller._saveEval (EvLooped (caller._nesting + 1) caller._judgment mode term caller._site)) caller._acyclic @@ -121,13 +131,13 @@ ctx._saveEval (EvData ctx._nesting meta._spelling term datum) bound' <- bind meta (MvBytes bytes) bound pure (bound', state'', datum : conditions) - through :: ReduceContext -> (Subst, State) -> (Meta, Expression) -> IO (Subst, State) - through ctx (bound, state') (meta, term) = do + through :: ReduceContext -> (Subst, State, [Expression]) -> (Meta, Expression) -> IO (Subst, State, [Expression]) + through ctx (bound, state', normals) (meta, term) = do placed <- operand term (normal, state'') <- morphing univ ctx placed state' ctx._saveEval (EvTerm ctx._nesting meta._spelling term normal) bound' <- bind meta (MvExpression normal) bound - pure (bound', state'') + pure (bound', state'', normal : normals) reshaped :: ReduceContext -> Subst -> (Meta, (Meta, [Y.Rule])) -> IO Subst reshaped ctx bound (meta, (source, rules)) = do term <- buildExpressionThrows (ExMeta source._name) bound @@ -261,12 +271,6 @@ parked _ (StuckAt func _ _) = throwIO (Stuck func) parked _ (OutOfStepsAt budget _ _) = throwIO (OutOfSteps budget) parked _ failure = throwIO failure - -settled :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) -settled term univ state ctx = do - (normal, _) <- normalized term ((univ, Nothing) :| []) ctx - ((morphed, _), state') <- morph' (normal, (univ, Nothing) :| []) univ state ctx - pure (morphed, state') saturated :: Expression -> [Binding] -> Maybe (T.Text, Expression) saturated term bds = case lambda bds of diff --git a/src/Files.hs b/src/Files.hs --- a/src/Files.hs +++ b/src/Files.hs @@ -1,14 +1,15 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT module Files (FsException (..), ensuredFile, allPathsIn, overwrite) where -import Control.Exception (Exception, onException, throwIO) +import Control.Exception (Exception, IOException, catch, onException, throwIO) import Control.Monad (forM, when) -import System.Directory (copyPermissions, createDirectoryIfMissing, doesDirectoryExist, doesFileExist, listDirectory, pathIsSymbolicLink, removeFile, renameFile) +import System.Directory (canonicalizePath, copyPermissions, createDirectoryIfMissing, doesDirectoryExist, doesFileExist, listDirectory, pathIsSymbolicLink, removeFile, renameFile) import System.FilePath (takeDirectory, takeFileName, ()) import System.IO (Handle, hClose, hPutStr, hSetEncoding, openTempFileWithDefaultPermissions, utf8) import Text.Printf (printf) @@ -28,13 +29,15 @@ if exists then pure pth else throwIO (FileDoesNotExist pth) overwrite :: FilePath -> String -> IO () -overwrite file content = do +overwrite path content = do + link <- pathIsSymbolicLink path `catch` \(_ :: IOException) -> pure False + file <- if link then canonicalizePath path else pure path createDirectoryIfMissing True (takeDirectory file) (temp, handle) <- openTempFileWithDefaultPermissions (takeDirectory file) (takeFileName file) - replace temp handle `onException` (hClose handle >> removeFile temp) + replace file temp handle `onException` (hClose handle >> removeFile temp) where - replace :: FilePath -> Handle -> IO () - replace temp handle = do + replace :: FilePath -> FilePath -> Handle -> IO () + replace file temp handle = do hSetEncoding handle utf8 hPutStr handle content hClose handle diff --git a/src/Functions.hs b/src/Functions.hs --- a/src/Functions.hs +++ b/src/Functions.hs @@ -7,13 +7,16 @@ import AST import Builder -import Bytes (btsSize, btsToNum, btsToUnescapedStr, numToBts, strToBts) +import Bytes (btsConcat, btsSize, btsToNum, btsToUnescapedStr, numToBts, strToBts) import Contextualize (contextualize) import Control.Exception (throwIO) import Control.Monad (when) import qualified Data.ByteString.Char8 as B import Data.Functor import qualified Data.Set as Set +import qualified Data.Text as T +import qualified Data.Text.Encoding as T +import qualified Data.Text.Encoding.Error as T import Deps import Logger (logDebug) import Matcher @@ -97,14 +100,20 @@ expr' <- buildExpressionThrows expr subst case expr' of DataObject _ bytes -> pure (TeBytes bytes) - ExFormation [BiDelta bytes, BiVoid AtRho] -> pure (TeBytes bytes) + ExApplication (BaseObject "bytes") (ArTau AtPhi (ExFormation bds)) | Just bytes <- delta bds -> pure (TeBytes bytes) + ExFormation bds | Just bytes <- delta bds -> pure (TeBytes bytes) _ -> throwIO (userError "Only data objects and bytes are supported by 'dataize' function now") + where + delta :: [Binding] -> Maybe Bytes + delta bds = case filter (/= BiVoid AtRho) bds of + [BiDelta bytes] -> Just bytes + _ -> Nothing _dataize _ _ = throwIO (userError "Function dataize() requires exactly 1 argument as expression or bytes") _concat :: BuildTermMethod _concat args subst = do - args' <- traverse (`argToString` subst) args - pure (TeExpression (DataString (strToBts (concat args')))) + args' <- traverse (`argToBytes` subst) args + pure (TeExpression (DataString (foldl btsConcat BtEmpty args'))) _sed :: BuildTermMethod _sed args subst = do @@ -113,11 +122,11 @@ traverse ( \arg -> do bts <- argToString arg subst - pure (B.pack bts) + pure (T.encodeUtf8 (T.pack bts)) ) args res <- sed first rest - pure (TeExpression (DataString (strToBts (B.unpack res)))) + pure (TeExpression (DataString (strToBts (T.unpack (T.decodeUtf8With T.lenientDecode res))))) where sed :: B.ByteString -> [B.ByteString] -> IO B.ByteString sed tgt [] = pure tgt diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -372,7 +372,7 @@ toLaTeX CO_ABSOLUTE{..} = CO_ABSOLUTE (toLaTeX expr) belongs toLaTeX CO_NOT{..} = CO_NOT (toLaTeX condition) toLaTeX CO_COMPARE{..} = CO_COMPARE (toLaTeX left) equal (toLaTeX right) - toLaTeX CO_MATCHES{..} = CO_MATCHES regex (toLaTeX expr) + toLaTeX CO_MATCHES{..} = CO_MATCHES (T.unpack (toLaTeX (T.pack regex))) (toLaTeX expr) toLaTeX CO_PART_OF{..} = CO_PART_OF (toLaTeX expr) (toLaTeX binding) toLaTeX CO_DISJOINT{..} = CO_DISJOINT (map toLaTeX attrs) (map toLaTeX groups) toLaTeX CO_SUBSET{..} = CO_SUBSET (map toLaTeX attrs) belongs (map toLaTeX groups) diff --git a/src/Lambdas.hs b/src/Lambdas.hs --- a/src/Lambdas.hs +++ b/src/Lambdas.hs @@ -25,9 +25,11 @@ import Control.Exception (Exception, throwIO) import Control.Monad (void) import Data.Aeson (FromJSON (parseJSON), Key, Object, Value (Object), withObject, (.!=), (.:), (.:?)) -import Data.List (find) +import Data.Char (isDigit) +import Data.List (find, sortOn) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map +import Data.Maybe (listToMaybe) import Data.Text (Text) import qualified Data.Text as T import Data.Text.Encoding (encodeUtf8) @@ -83,12 +85,16 @@ sigmas (T.unpack key) lambda._answer dataless (T.unpack key) lambda._answer earlier (T.unpack key) lambda + once (T.unpack key) lambda + mapM_ (metaless (T.unpack key) "dataize") lambda._dataized + mapM_ (metaless (T.unpack key) "morph") lambda._morphed + answered (T.unpack key) lambda pure lambda where operands :: Text -> (Text -> Yaml.Parser Meta) -> Object -> Key -> Yaml.Parser [(Meta, Expression)] operands key kind entry name = do mapping <- entry .:? name .!= (Map.empty :: Map Text Expression) - mapM bound (Map.toAscList mapping) + mapM bound (numbered mapping) where bound :: (Text, Expression) -> Yaml.Parser (Meta, Expression) bound (meta, term) = do @@ -105,7 +111,7 @@ pairs :: String -> Object -> Yaml.Parser [(Meta, (Meta, Meta))] pairs key entry = do mapping <- entry .:? "join" .!= (Map.empty :: Map Text [Text]) - mapM joins (Map.toAscList mapping) + mapM joins (numbered mapping) where joins :: (Text, [Text]) -> Yaml.Parser (Meta, (Meta, Meta)) joins (meta, [left, right]) = do @@ -122,7 +128,7 @@ rewrites :: String -> Object -> Yaml.Parser [(Meta, (Meta, [Y.Rule]))] rewrites key entry = do mapping <- entry .:? "rewrite" .!= (Map.empty :: Map Text Object) - mapM line (Map.toAscList mapping) + mapM line (numbered mapping) where line :: (Text, Object) -> Yaml.Parser (Meta, (Meta, [Y.Rule])) line (meta, body) = do @@ -186,14 +192,63 @@ key ) sigmas :: String -> Expression -> Yaml.Parser () - sigmas key answer = case [kind | Slot kind _ <- slots answer, kind /= "S"] of + sigmas key answer = case ([kind | Slot kind _ <- slots answer, kind /= "S"], symbols answer) of + ([], []) -> pure () + (kind : _, _) -> fail (printf "The anonymous meta '!%s' cannot be referenced in the '𝑛' of Ξ» function '%s'" (T.unpack kind) key) + (_, idx : _) -> fail (printf "The '𝑛' of Ξ» function '%s' writes the numbered symbol '𝜎%d', while only a bare 𝜎 mints a fresh one" key idx) + once :: String -> Lambda -> Yaml.Parser () + once key lambda = case twice [] bound of + Nothing -> pure () + Just meta -> fail (printf "The meta '%s' of Ξ» function '%s' is bound by more than one line, while each meta may be bound once" (T.unpack meta) key) + where + bound :: [Text] + bound = + map (_spelling . fst) lambda._morphed + ++ map (_spelling . fst) lambda._rewritten + ++ map (_spelling . fst) lambda._symbolized + ++ map (_spelling . fst) lambda._paired + twice :: [Text] -> [Text] -> Maybe Text + twice _ [] = Nothing + twice seen (meta : rest) + | meta `elem` seen = Just meta + | otherwise = twice (meta : seen) rest + metaless :: String -> String -> (Meta, Expression) -> Yaml.Parser () + metaless key block (meta, term) = case metas term of [] -> pure () - kind : _ -> fail (printf "The anonymous meta '!%s' cannot be referenced in the '𝑛' of Ξ» function '%s'" (T.unpack kind) key) + name : _ -> + fail + ( printf + "The operand '%s' of '%s' of Ξ» function '%s' reads the meta '%s', while only a path from '$' can be reduced there" + (T.unpack meta._spelling) + block + key + (T.unpack name) + ) + answered :: String -> Lambda -> Yaml.Parser () + answered key lambda = case filter (`notElem` ("S" : known)) (metas lambda._answer) of + [] -> pure () + name : _ -> fail (printf "The '𝑛' of Ξ» function '%s' reads the meta '%s' that no block binds" key (T.unpack name)) + where + known :: [Text] + known = + map (_name . fst) lambda._dataized + ++ map (_name . fst) lambda._morphed + ++ map (_name . fst) lambda._rewritten + ++ map (_name . fst) lambda._symbolized + ++ map (_name . fst) lambda._paired dataless :: String -> Expression -> Yaml.Parser () dataless key answer | computes answer = fail (printf "The '𝑛' of Ξ» function '%s' reads data, while a symbolic answer may mention nothing but 𝜎" key) | otherwise = pure () +numbered :: Map Text a -> [(Text, a)] +numbered = sortOn (order . fst) . Map.toList + where + order :: Text -> (Text, Integer) + order meta = case T.takeWhileEnd isDigit meta of + digits | T.null digits -> (meta, 0) + digits -> (T.dropWhileEnd isDigit meta, read (T.unpack digits)) + computes :: Expression -> Bool computes = goExpr where @@ -244,6 +299,7 @@ throwIO (BrokenLambdas path (printf "the key '%s' is not a regular expression: %s" (T.unpack key) failure)) overlaps :: FilePath -> [(Regex, Lambda)] -> IO () + overlaps _ [_] = pure () overlaps file registered = mapM (spoken . snd) registered >>= check where spoken :: Lambda -> IO (Lambda, Language) @@ -331,6 +387,12 @@ taking :: (Expression, Joining) -> (Expression, [(Int, (Int, Int))], Int) taking (term, (spent', _, made)) = (term, reverse made, spent') goExpr :: Expression -> Expression -> Joining -> Maybe (Expression, Joining) + goExpr one@(ExFormation _) two@(ExFormation _) joining + | bare one /= bare two = do + mine <- ending one + theirs <- ending two + (bd, joining') <- goBinding mine theirs joining + pure (ExFormation [bd], joining') goExpr (ExFormation one) (ExFormation two) joining = do (bds, joining') <- goBindings one two joining pure (ExFormation bds, joining') @@ -372,6 +434,13 @@ goBinding one two joining | one == two = Just (one, joining) | otherwise = Nothing + bare :: Expression -> Bool + bare (ExFormation [BiLambda (FnSymbol _)]) = True + bare _ = False + ending :: Expression -> Maybe Binding + ending (ExFormation [bd@(BiLambda (FnSymbol _))]) = Just bd + ending (ExFormation bds) = listToMaybe [body | BiTau AtPhi body <- bds] >>= ending + ending _ = Nothing goArgument :: Argument -> Argument -> Joining -> Maybe (Argument, Joining) goArgument (ArTau attr one) (ArTau attr' two) joining | attr == attr' = do diff --git a/src/Language.hs b/src/Language.hs --- a/src/Language.hs +++ b/src/Language.hs @@ -134,8 +134,8 @@ collect done ('\\' : rest) = do (span', left) <- escape rest case (span', left) of - (Span [(low, _)], '-' : high : after) - | high /= ']' -> ranged done low (high : after) + (Span [(low, top)], '-' : high : after) + | low == top && high /= ']' -> ranged done low (high : after) _ -> collect (span' : done) left collect done (low : '-' : high : rest) | high /= ']' = ranged done low (high : rest) diff --git a/src/Margin.hs b/src/Margin.hs --- a/src/Margin.hs +++ b/src/Margin.hs @@ -25,7 +25,7 @@ withMargin' _ ex@EX_FORMATION{binding = BI_EMPTY{}} = ex withMargin' (extra, margin) ex@EX_FORMATION{tab = tab@(TAB indent), ..} = let single = toSingleLine ex - ex' = EX_FORMATION lsb EOL tab (withMargin' (indent, margin) binding) EOL tab' rsb + ex' = EX_FORMATION lsb EOL tab (withMargin' (2 * indent, margin) binding) EOL tab' rsb in if lengthOf single + extra <= margin then single else ex' withMargin' _ num@EX_NUMBER{} = num withMargin' _ str@EX_STRING{} = str @@ -41,7 +41,7 @@ main = withMargin' cfg expr singleMain = toSingleLine main extra' = T.length (last (T.lines (render main))) + 4 - arg' = withMargin' (indt, margin) argument + arg' = withMargin' (2 * indt, margin) argument singleArg = toSingleLine arg' in if | lengthOf single + extra <= margin -> single diff --git a/src/Merge.hs b/src/Merge.hs --- a/src/Merge.hs +++ b/src/Merge.hs @@ -39,15 +39,19 @@ | otherwise = throwIO (CanNotMergeBinding x y) mergeBindings :: [Binding] -> [Binding] -> IO [Binding] -mergeBindings xs ys = do - let as = attributesFromBindings' xs - bs = attributesFromBindings' ys - xs' = [x | x <- xs, attributeFromBinding x `notElem` bs] - ys' = [y | y <- ys, attributeFromBinding y `notElem` as] - collisions = [(x, y) | x <- xs, y <- ys, attributeFromBinding x == attributeFromBinding y] - ws <- mapM (uncurry mergeBinding) collisions - pure (unmarked (xs' <> ys' <> ws)) +mergeBindings xs ys = unmarked <$> anchored xs ys where + anchored :: [Binding] -> [Binding] -> IO [Binding] + anchored [] rest = pure rest + anchored (x : more) rest = case break (same x) rest of + (before, y : after) -> do + let later = attributesFromBindings' more + (pending, ahead) = (filter ((`elem` later) . attributeFromBinding) before, filter ((`notElem` later) . attributeFromBinding) before) + united <- mergeBinding x y + (ahead <>) . (united :) <$> anchored more (pending <> after) + (_, []) -> (x :) <$> anchored more rest + same :: Binding -> Binding -> Bool + same x y = attributeFromBinding x == attributeFromBinding y unmarked :: [Binding] -> [Binding] unmarked bindings | any marker xs == any marker ys = bindings diff --git a/src/Morph.hs b/src/Morph.hs --- a/src/Morph.hs +++ b/src/Morph.hs @@ -5,19 +5,21 @@ {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} {-# OPTIONS_GHC -Wno-unused-record-wildcards #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Morph (Answer, Deadline (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, FiringFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), boxed, charged, counted, deeper, emptyState, enter, entering, execBuildTerm, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, parking, recalled, retained, starved, tallied, timed, universed, unparked) where +module Morph (Answer, Deadline (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, FiringFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), boxed, charged, counted, deeper, emptyState, enter, entering, execBuildTerm, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, parking, recalled, remember, remembered, retained, settled, starved, tallied, timed, universed, unparked) where import AST import Builder (buildExpressionThrows, pathOf) import Control.Applicative ((<|>)) import Control.Exception (Exception, SomeException, catch, evaluate, throwIO, try) import Control.Monad (unless, when) +import Data.Bifunctor (first) import Data.IORef (IORef, modifyIORef', newIORef, readIORef, writeIORef) import Data.List (find, partition) import Data.List.NonEmpty (NonEmpty (..)) @@ -26,11 +28,11 @@ import Data.Maybe (fromMaybe, isJust, listToMaybe) import qualified Data.Set as Set import qualified Data.Text as T -import Deps (Acyclic (..), BuildTermFunc, BuildTermMethod, Evaluation (..), Judgment (..), SaveEvalFunc, SaveStepFunc, State (..), Term (..), dontSaveStep, renumbered) +import Deps (Acyclic (..), BuildTermFunc, BuildTermMethod, Evaluation (..), Judgment (..), SaveEvalFunc, SaveStepFunc, State (..), Term (..), dontSaveEval, dontSaveStep, renumbered) import Engine (Engine (..)) import GHC.Clock (getMonotonicTime) import qualified Inference as In -import Lambdas (Lambdas) +import Lambdas (Lambdas, emptyLambdas) import Locator (locatedExpression, withLocatedExpression) import Matcher (substEmpty) import Must (Must (..)) @@ -70,10 +72,13 @@ , _until :: Double } -data Memo = Memo (IORef (Store (Int, Kept))) (IORef Int) (IORef Int) (IORef (Set.Set (Expression, Attribute))) +data Memo = Memo (IORef (Store (Int, Kept))) (IORef (Map.Map Firing Answer)) (IORef Int) (IORef Int) (IORef (Set.Set (Expression, Attribute))) type Answer = (Expression, Expression) +data Firing = Firing T.Text [Either Int Bytes] [Expression] + deriving (Eq, Ord) + data Kept = Answered Answer | Looped Expression @@ -81,6 +86,8 @@ type Store answer = Map.Map Int [(Expression, answer)] +data Frame = Frame (IORef Expression) (IORef Expression) Expression (Maybe Attribute) + data ReduceContext = ReduceContext { _locator :: Expression , _site :: Expression @@ -157,7 +164,7 @@ where starve :: Maybe Memo -> IO () starve Nothing = pure () - starve (Just (Memo _ _ exhausted _)) = modifyIORef' exhausted (+ 1) + starve (Just (Memo _ _ _ exhausted _)) = modifyIORef' exhausted (+ 1) tallied :: Maybe Int -> IO (Maybe Tally) tallied = traverse (\cap -> Tally cap <$> newIORef 0) @@ -173,7 +180,9 @@ billed :: Tally -> IO () billed (Tally cap count) = do fired <- readIORef count - when (fired >= cap) (throwIO (OutOfSteps (Firings cap))) + when (fired >= cap) $ do + ctx._saveEval (EvSpent ctx._nesting cap ctx._judgment ctx._site) + throwIO (OutOfSteps (Firings cap)) writeIORef count (fired + 1) clocked :: ReduceContext -> IO () @@ -190,12 +199,12 @@ throwIO (OutOfTime cap) memoized :: Maybe Acyclic -> IO (Maybe Memo) -memoized (Just Plausible) = Just <$> (Memo <$> newIORef Map.empty <*> newIORef 0 <*> newIORef 0 <*> newIORef Set.empty) +memoized (Just Plausible) = Just <$> (Memo <$> newIORef Map.empty <*> newIORef Map.empty <*> newIORef 0 <*> newIORef 0 <*> newIORef Set.empty) memoized _ = pure Nothing recalled :: Maybe Memo -> Expression -> Int -> IO (Maybe Kept) recalled Nothing _ _ = pure Nothing -recalled (Just (Memo store answers _ _)) form spent = do +recalled (Just (Memo store _ answers _ _)) form spent = do kept <- readIORef store count <- readIORef answers let live = [known | (term, (stamp, known)) <- Map.findWithDefault [] (hashExpression form) kept, term == form, current count stamp known] @@ -210,27 +219,34 @@ counted :: Maybe Memo -> IO Int counted Nothing = pure 0 -counted (Just (Memo _ answers _ _)) = readIORef answers +counted (Just (Memo _ _ answers _ _)) = readIORef answers starved :: Maybe Memo -> IO Int starved Nothing = pure 0 -starved (Just (Memo _ _ exhausted _)) = readIORef exhausted +starved (Just (Memo _ _ _ exhausted _)) = readIORef exhausted retained :: Maybe Memo -> Expression -> Int -> Kept -> IO () retained Nothing _ _ _ = pure () -retained (Just (Memo store answers _ _)) form stamp kept = do +retained (Just (Memo store _ _ _ _)) form stamp kept = modifyIORef' store (Map.insertWith (++) (hashExpression form) [(form, (stamp, kept))]) - case kept of - Answered _ -> modifyIORef' answers (+ 1) - _ -> pure () +remembered :: Maybe Memo -> Firing -> IO (Maybe Answer) +remembered Nothing _ = pure Nothing +remembered (Just (Memo _ firings _ _ _)) firing = Map.lookup firing <$> readIORef firings + +remember :: Maybe Memo -> Firing -> Answer -> IO () +remember Nothing _ _ = pure () +remember (Just (Memo _ firings answers _ _)) firing answer = do + modifyIORef' firings (Map.insert firing answer) + modifyIORef' answers (+ 1) + visited :: Maybe Memo -> Expression -> Attribute -> IO Bool visited Nothing _ _ = pure False -visited (Just (Memo _ _ _ walked)) object attr = Set.member (object, attr) <$> readIORef walked +visited (Just (Memo _ _ _ _ walked)) object attr = Set.member (object, attr) <$> readIORef walked visit :: Maybe Memo -> Expression -> Attribute -> IO () visit Nothing _ _ = pure () -visit (Just (Memo _ _ _ walked)) object attr = modifyIORef' walked (Set.insert (object, attr)) +visit (Just (Memo _ _ _ _ walked)) object attr = modifyIORef' walked (Set.insert (object, attr)) parking :: NonEmpty Rewritten -> State -> IO a -> IO a parking seq state action = action `catch` rethrow @@ -303,19 +319,39 @@ isLambda _ = False morph' :: Morphed -> Expression -> State -> ReduceContext -> IO (Morphed, State) -morph' (expr, seq) univ state caller = do - ctx <- deeper =<< entering expr =<< universed univ caller{_judgment = Morphing} - parking seq state $ do - reached <- inferred expr univ state ctx ctx._engine._morphing - case reached of - Just (In.Answered step built, state') -> do - seq' <- leadsTo seq step built ctx - pure ((built, seq'), state') - Just (In.Onward way built world, state') -> do - (morphed, state'') <- onward seq state' way built ctx - morph' morphed world state'' ctx - Nothing -> throwIO (Unmorphable expr) +morph' start univ state entry = go start univ state entry + where + go :: Morphed -> Expression -> State -> ReduceContext -> IO (Morphed, State) + go (expr, seq) univ state caller = do + ctx <- deeper =<< entering expr =<< universed univ caller{_judgment = Morphing} + parking seq state $ do + reached <- inferred expr univ state ctx ctx._engine._morphing + case reached of + Just (In.Answered step built, state') -> do + seq' <- leadsTo seq step built ctx + pure ((built, seq'), state') + Just (In.Onward way built world, state') -> do + (walked, state'') <- prewalked way built univ state' ctx{_steps = entry._steps} + (morphed, state''') <- onward seq state'' way walked ctx + go morphed world state''' ctx + Nothing -> throwIO (Unmorphable expr) +prewalked :: In.Way -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) +prewalked (In.Normalized _) expr univ state ctx + | ctx._deep = go expr + where + go :: Expression -> IO (Expression, State) + go (ExDispatch target@(ExDispatch _ _) attr) = first (`ExDispatch` attr) <$> go target + go (ExDispatch form@(ExFormation bds) attr) + | attr /= AtRho && reading attr bds && all tau bds = first (`ExDispatch` attr) <$> deepened (Just attr) form univ state ctx + go term = pure (term, state) + tau :: Binding -> Bool + tau (BiTau _ _) = True + tau _ = False + reading :: Attribute -> [Binding] -> Bool + reading attr bds = maybe False (not . closed) (listToMaybe [body | BiTau attr' body <- bds, attr' == attr]) +prewalked _ expr _ state _ = pure (expr, state) + morph :: Expression -> State -> ReduceContext -> IO (Expression, [Rewritten], State) morph universe state caller@ReduceContext{..} = do ctx <- universed universe caller @@ -342,45 +378,139 @@ walked walker morphed seq state' | not _deep = pure (morphed, reverse (NE.toList seq), state') | otherwise = do - (deep, state'') <- deepened morphed universe state' walker + (deep, state'') <- deepened Nothing morphed universe state' walker seq' <- leadsTo seq (Morphing, "deep") deep walker pure (deep, reverse (NE.toList seq'), state'') -deepened :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) -deepened expr univ state ctx = step (if ctx._jobs > 1 then spread else parts) (Just ctx._site) Nothing ExXi expr state ctx +deepened :: Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) +deepened focus expr univ state ctx = do + world <- newIORef (fromMaybe univ ctx._universe) + case focus of + Just attr -> do + (store, path) <- home Nothing world expr + body <- held (ExDispatch path attr) store + (entered, state') <- sibling Nothing (Frame world store path (Just attr)) body state ctx + when (entered /= body) (stored store (ExDispatch path attr) entered) + (,state') <$> held path store + Nothing -> step (if ctx._jobs > 1 then spread else parts) (Just ctx._site) Nothing (Frame world world ctx._site Nothing) expr state ctx where - go :: Maybe Expression -> Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) + go :: Maybe Expression -> Maybe Attribute -> Frame -> Expression -> State -> ReduceContext -> IO (Expression, State) go = step parts - step :: (Maybe Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)) -> Maybe Expression -> Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) - step walk standing dispatched context term state' caller = do + step :: (Maybe Expression -> Frame -> Expression -> State -> ReduceContext -> IO (Expression, State)) -> Maybe Expression -> Maybe Attribute -> Frame -> Expression -> State -> ReduceContext -> IO (Expression, State) + step walk standing dispatched frame@(Frame world _ _ _) term state' caller = do let here = sited standing caller ctx' <- deeper here - (walked, walkedState) <- walk standing context term state' here - placed <- ctx._engine._contextualize walked context - (answer, answered) <- ctx'._fire dispatched placed univ walkedState ctx' - pure (fromMaybe walked answer, answered) + copy <- deferrable dispatched world term state' here + case copy of + Just form -> deferred form state' here + Nothing -> do + (walked, walkedState) <- walk standing frame term state' here + placed <- ctx._engine._contextualize walked =<< context frame + current <- readIORef world + (answer, answered) <- ctx'._fire dispatched placed current walkedState ctx'{_universe = Just current} + mapM_ (noted here._site frame walked) answer + pure (fromMaybe walked answer, answered) + deferrable :: Maybe Attribute -> IORef Expression -> Expression -> State -> ReduceContext -> IO (Maybe Expression) + deferrable dispatched world form@(ExFormation bds) state' caller + | boxed bds && not (any abstract bds) && any code bds && maybe True (\attr -> not (any (named attr) bds)) dispatched = do + current <- readIORef world + known <- mapM (resolved current form state' caller) bds + pure (if any bare known then Just (ExFormation known) else Nothing) + deferrable _ _ _ _ _ = pure Nothing + code :: Binding -> Bool + code (BiTau AtPhi (ExFormation _)) = False + code (BiTau AtPhi _) = True + code _ = False + bare :: Binding -> Bool + bare (BiTau attr (ExFormation [BiLambda (FnSymbol _)])) = attr /= AtPhi && attr /= AtRho + bare _ = False + resolved :: Expression -> Expression -> State -> ReduceContext -> Binding -> IO Binding + resolved current form state' caller bd@(BiTau attr body@(ExDispatch _ _)) + | attr /= AtPhi && attr /= AtRho = do + placed <- ctx._engine._contextualize body (scope attr form) + outcome <- try (settled placed current state' (reading current caller)) + case outcome of + Right (made@(ExFormation [BiLambda (FnSymbol _)]), _) -> pure (BiTau attr made) + Left (OutOfTime cap) -> expired caller cap + _ -> pure bd + resolved _ _ _ _ bd = pure bd + reading :: Expression -> ReduceContext -> ReduceContext + reading current caller = + caller + { _universe = Just current + , _symbolic = emptyLambdas + , _memo = Nothing + , _tally = Nothing + , _acyclic = Nothing + , _deep = False + , _saveStep = dontSaveStep + , _saveEval = dontSaveEval + } + deferred :: Expression -> State -> ReduceContext -> IO (Expression, State) + deferred copy state' caller = do + caller._saveEval (EvDeferred caller._nesting fresh caller._judgment copy (called copy) caller._site) + pure (ExFormation [BiLambda (FnSymbol fresh)], state'{_minted = fresh}) + where + fresh :: Int + fresh = state'._minted + 1 + called :: Expression -> Maybe Expression + called copy@(ExFormation bds) = do + (path, declared) <- origin copy + pure (foldl ExApplication path [ArTau attr value | BiTau attr value <- bds, attr /= AtRho, BiVoid attr `elem` declared]) + called _ = Nothing + origin :: Expression -> Maybe (Expression, [Binding]) + origin (ExFormation bds) = do + parent <- case filter ((== Just AtRho) . attributeFromBinding) bds of + [] -> Just ExRoot + [BiTau AtRho form@(ExFormation _)] -> fst <$> origin form + [BiTau AtRho path] -> Just (erased path) + _ -> Nothing + ExFormation siblings <- located parent (fromMaybe univ ctx._universe) + chosen bds [(ExDispatch parent attr, declared) | BiTau attr (ExFormation declared) <- siblings, attr /= AtRho, fits declared] + where + fits :: [Binding] -> Bool + fits declared = all (`elem` map attributeFromBinding declared) [attributeFromBinding bd | bd <- bds, attributeFromBinding bd /= Just AtRho] + origin _ = Nothing + chosen :: [Binding] -> [(Expression, [Binding])] -> Maybe (Expression, [Binding]) + chosen _ [] = Nothing + chosen bds candidates = case [candidate | candidate <- candidates, agreed candidate == maximum (map agreed candidates)] of + [one] -> Just one + _ -> Nothing + where + agreed :: (Expression, [Binding]) -> (Int, Int) + agreed (_, declared) = (length [attr | BiTau attr _ <- bds, BiVoid attr `elem` declared], length (filter (`elem` declared) bds)) sited :: Maybe Expression -> ReduceContext -> ReduceContext sited Nothing caller = caller sited (Just loc) caller = caller{_site = loc} - parts :: Maybe Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) + parts :: Maybe Expression -> Frame -> Expression -> State -> ReduceContext -> IO (Expression, State) parts _ _ term@(ExFormation bds) state' _ | any abstract bds = pure (term, state') - parts standing _ form@(ExFormation bds) state' caller = do - (entered, state'') <- bindings standing (synonym caller._universe form) bds bds state' caller - pure (ExFormation entered, state'') - parts _ context (ExDispatch target attr) state' caller = do - (entered, state'') <- go Nothing (Just attr) context target state' caller + parts standing (Frame world _ _ _) form@(ExFormation bds) state' caller = do + (store, path) <- home standing world form + state'' <- bindings standing (synonym caller._universe form) (Frame world store path Nothing) [attr | BiTau attr _ <- bds, attr /= AtRho] state' caller + entered <- held path store + pure (entered, state'') + parts _ frame (ExDispatch target attr) state' caller = do + (entered, state'') <- go Nothing (Just attr) frame target state' caller pure (ExDispatch entered attr, state'') - parts _ context (ExApplication target arg) state' caller = do - (entered, state'') <- go Nothing Nothing context target state' caller - (applied, state''') <- argument context arg state'' caller + parts _ frame (ExApplication target arg) state' caller = do + (entered, state'') <- go Nothing Nothing frame target state' caller + (applied, state''') <- argument (go Nothing Nothing) frame arg state'' caller pure (ExApplication entered applied, state''') parts _ _ term state' _ = pure (term, state') + sibling :: Maybe Attribute -> Frame -> Expression -> State -> ReduceContext -> IO (Expression, State) + sibling dispatched frame term@(ExDispatch ExXi attr) state' caller + | attr /= AtRho = go Nothing dispatched frame term state' caller + sibling _ frame (ExDispatch target attr) state' caller = first (`ExDispatch` attr) <$> sibling (Just attr) frame target state' caller + sibling _ frame (ExApplication target arg) state' caller = do + (entered, state'') <- sibling Nothing frame target state' caller + first (ExApplication entered) <$> argument (sibling Nothing) frame arg state'' caller + sibling _ _ term state' _ = pure (term, state') abstract :: Binding -> Bool abstract (BiVoid _) = True abstract _ = False - spread :: Maybe Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) - spread standing _ form@(ExFormation bds) state' caller + spread :: Maybe Expression -> Frame -> Expression -> State -> ReduceContext -> IO (Expression, State) + spread standing (Frame world _ _ _) form@(ExFormation bds) state' caller | not (any abstract bds) = do jobs <- mapM (planned (synonym caller._universe form)) (zip [1 ..] bds) (entered, _, state'') <- pooled caller._jobs jobs gathered ([], 0, state') @@ -402,8 +532,10 @@ tau <- tausOf idx tally <- tallied (fmap (\(Tally cap _) -> cap) caller._tally) memo <- memoized caller._acyclic + copy <- newIORef =<< readIORef world + (store, path) <- home standing copy form let own = caller{_jobs = 1, _tally = tally, _memo = memo, _saveEval = modifyIORef' buffer . (:), _buildTerm = minting tau caller._buildTerm} - outcome <- try (go (fmap (`ExDispatch` attr) standing) Nothing (scope attr bds) body state' own) + outcome <- try (go (fmap (`ExDispatch` attr) standing) Nothing (Frame copy store path (Just attr)) body state' own) records <- reverse <$> readIORef buffer pure (records, fmap (\(term, walked) offset -> (BiTau attr (lifted floor' offset term), Just (moved offset walked))) outcome) moved :: Int -> State -> State @@ -417,25 +549,64 @@ mapM_ (caller._saveEval . renumbered floor' offset) records (bd, walked) <- either throwIO (pure . ($ offset)) outcome pure (bd : done, maybe offset (\after -> after._minted - floor') walked, fromMaybe current walked) - spread standing context term state' caller = parts standing context term state' caller + spread standing frame term state' caller = parts standing frame term state' caller minting :: IO T.Text -> BuildTermFunc -> BuildTermFunc minting tau build func | func == "random-tau" = \args subst -> if null args then TeAttribute . AtLabel <$> tau else build func args subst | otherwise = build func - bindings :: Maybe Expression -> Maybe (Expression, [Attribute]) -> [Binding] -> [Binding] -> State -> ReduceContext -> IO ([Binding], State) - bindings _ _ _ [] state' _ = pure ([], state') - bindings standing alias whole (BiTau attr body : rest) state' caller - | attr /= AtRho = do - new <- if closed body then fresh alias attr caller else pure True - (entered, state'') <- - if new - then go (fmap (`ExDispatch` attr) standing) Nothing (scope attr whole) body state' caller - else pure (body, state') - (others, state''') <- bindings standing alias whole rest state'' caller - pure (BiTau attr entered : others, state''') - bindings standing alias whole (bd : rest) state' caller = do - (others, state'') <- bindings standing alias whole rest state' caller - pure (bd : others, state'') + bindings :: Maybe Expression -> Maybe (Expression, [Attribute]) -> Frame -> [Attribute] -> State -> ReduceContext -> IO State + bindings _ _ _ [] state' _ = pure state' + bindings standing alias frame@(Frame world store path _) (attr : rest) state' caller = do + body <- held (ExDispatch path attr) store + new <- if closed body then fresh alias attr caller else pure True + state'' <- + if new + then do + (entered, walked) <- go (fmap (`ExDispatch` attr) standing) Nothing (Frame world store path (Just attr)) body state' caller + walked <$ when (entered /= body) (stored store (ExDispatch path attr) entered) + else pure state' + bindings standing alias frame rest state'' caller + home :: Maybe Expression -> IORef Expression -> Expression -> IO (IORef Expression, Expression) + home (Just path) world form = do + placed <- put path form <$> readIORef world + case placed of + Just whole -> (world, path) <$ writeIORef world whole + Nothing -> home Nothing world form + home Nothing _ form = (,ExRoot) <$> newIORef form + context :: Frame -> IO Expression + context (Frame _ _ _ Nothing) = pure ExXi + context (Frame _ store path (Just attr)) = scope attr <$> held path store + noted :: Expression -> Frame -> Expression -> Expression -> IO () + noted site frame@(Frame world _ _ _) walked answer = case address frame walked of + Just (store, path@(ExDispatch _ _)) + | store /= world || not (above path site) -> stored store path answer + _ -> pure () + address :: Frame -> Expression -> Maybe (IORef Expression, Expression) + address (Frame world _ _ _) ExRoot = Just (world, ExRoot) + address (Frame _ store path (Just _)) ExXi = Just (store, path) + address frame (ExDispatch target attr) = fmap (`ExDispatch` attr) <$> address frame target + address _ _ = Nothing + above :: Expression -> Expression -> Bool + above path (ExDispatch target _) = path == target || above path target + above _ _ = False + held :: Expression -> IORef Expression -> IO Expression + held path store = readIORef store >>= maybe (throwIO (userError (printf "The deep walk lost the object at %s" (printExpression path)))) pure . located path + stored :: IORef Expression -> Expression -> Expression -> IO () + stored store path value = modifyIORef' store (\whole -> fromMaybe whole (put path value whole)) + put :: Expression -> Expression -> Expression -> Maybe Expression + put ExRoot value _ = Just value + put (ExDispatch path attr) value whole = case located path whole of + Just (ExFormation bds) + | attr /= AtRho && not (any abstract bds) && any (named attr) bds -> + put path (ExFormation (map (\bd -> if named attr bd then BiTau attr value else bd) bds)) whole + _ -> Nothing + put _ _ _ = Nothing + located :: Expression -> Expression -> Maybe Expression + located ExRoot whole = Just whole + located (ExDispatch path attr) whole = case located path whole of + Just (ExFormation bds) -> listToMaybe [body | BiTau attr' body <- bds, attr' == attr] + _ -> Nothing + located _ _ = Nothing synonym :: Maybe Expression -> Expression -> Maybe (Expression, [Attribute]) synonym Nothing _ = Nothing synonym (Just world) form = case pathOf world form of @@ -443,13 +614,13 @@ ExFormation _ -> Nothing name -> Just (erased name, supplied name) where - erased :: Expression -> Expression - erased (ExApplication target _) = erased target - erased (ExDispatch target attr) = ExDispatch (erased target) attr - erased other = other supplied :: Expression -> [Attribute] supplied (ExApplication target (ArTau attr _)) = attr : supplied target supplied _ = [] + erased :: Expression -> Expression + erased (ExApplication target _) = erased target + erased (ExDispatch target attr) = ExDispatch (erased target) attr + erased other = other fresh :: Maybe (Expression, [Attribute]) -> Attribute -> ReduceContext -> IO Bool fresh (Just (object, filled)) attr caller | attr `notElem` filled = do @@ -457,26 +628,27 @@ unless seen (visit caller._memo object attr) pure (not seen) fresh _ _ _ = pure True - closed :: Expression -> Bool - closed ExXi = False - closed (ExDispatch target _) = closed target - closed (ExApplication target (ArTau _ arg)) = closed target && closed arg - closed (ExApplication target (ArAlpha _ arg)) = closed target && closed arg - closed _ = True - scope :: Attribute -> [Binding] -> Expression - scope attr bds = ExFormation (filter (not . named) bds) - where - named :: Binding -> Bool - named (BiTau attr' _) = attr' == attr - named _ = False - argument :: Expression -> Argument -> State -> ReduceContext -> IO (Argument, State) - argument context (ArTau attr arg) state' caller = do - (entered, state'') <- go Nothing Nothing context arg state' caller + scope :: Attribute -> Expression -> Expression + scope attr (ExFormation bds) = ExFormation (filter (not . named attr) bds) + scope _ other = other + named :: Attribute -> Binding -> Bool + named attr (BiTau attr' _) = attr' == attr + named _ _ = False + argument :: (Frame -> Expression -> State -> ReduceContext -> IO (Expression, State)) -> Frame -> Argument -> State -> ReduceContext -> IO (Argument, State) + argument walk frame (ArTau attr arg) state' caller = do + (entered, state'') <- walk frame arg state' caller pure (ArTau attr entered, state'') - argument context (ArAlpha alpha arg) state' caller = do - (entered, state'') <- go Nothing Nothing context arg state' caller + argument walk frame (ArAlpha alpha arg) state' caller = do + (entered, state'') <- walk frame arg state' caller pure (ArAlpha alpha entered, state'') +closed :: Expression -> Bool +closed ExXi = False +closed (ExDispatch target _) = closed target +closed (ExApplication target (ArTau _ arg)) = closed target && closed arg +closed (ExApplication target (ArAlpha _ arg)) = closed target && closed arg +closed _ = True + inferred :: Expression -> Expression -> State -> ReduceContext -> [In.Inference value] -> IO (Maybe (In.Conclusion value, State)) inferred expr univ state ctx rules = do ordered <- if ctx._shuffle then shuffle rules else pure rules @@ -548,6 +720,12 @@ extended attr normal = case ctx._universe of Just (ExFormation bds) -> Just (ExFormation (BiTau attr normal : bds)) _ -> Nothing + +settled :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) +settled term univ state ctx = do + (normal, _) <- normalized term ((univ, Nothing) :| []) ctx + ((morphed, _), state') <- morph' (normal, (univ, Nothing) :| []) univ state ctx + pure (morphed, state') morphing :: Expression -> ReduceContext -> Expression -> State -> IO (Expression, State) morphing univ ctx expr state = do diff --git a/src/Parser.hs b/src/Parser.hs --- a/src/Parser.hs +++ b/src/Parser.hs @@ -26,6 +26,7 @@ import Control.Monad (guard, when) import Data.Char (isAsciiLower, isAsciiUpper, isDigit) import Data.Scientific (toRealFloat) +import qualified Data.Set as Set import qualified Data.Text as T import Data.Void import GHC.Char @@ -35,7 +36,6 @@ import Text.Megaparsec.Char import qualified Text.Megaparsec.Char.Lexer as L import Text.Printf (printf) -import Text.Read (readMaybe) type Parser = Parsec Void String @@ -147,9 +147,10 @@ sigma = metaVar 'S' "𝜎" >>= either (pure . FnFresh) numbered where numbered :: T.Text -> Parser Function - numbered named = case readMaybe (T.unpack (T.drop 1 named)) of - Just idx -> pure (FnSymbol idx) - Nothing -> fail (printf "the symbol '%s' is numbered by something that is not an integer" (T.unpack named)) + numbered named = case T.unpack (T.drop 1 named) of + digits@(first : _) + | all isDigit digits && first /= '0' && (read digits :: Integer) <= toInteger (maxBound :: Int) -> pure (FnSymbol (read digits)) + _ -> fail (printf "the symbol '%s' is not numbered by a positive integer without leading zeros that fits into Int" (T.unpack named)) byte :: Parser String byte = do @@ -357,10 +358,15 @@ alpha = do _ <- choice [symbol "~", symbol "Ξ±"] choice - [ Alpha <$> lexeme L.decimal + [ lexeme L.decimal >>= ranged , either AlAny AlMeta <$> indexVar ] "alpha" + where + ranged :: Integer -> Parser Alpha + ranged idx + | idx > toInteger (maxBound :: Int) = fail (printf "the index of 'Ξ±%d' is too big, while it must fit into %d" idx (maxBound :: Int)) + | otherwise = pure (Alpha (fromInteger idx)) argument :: Parser Argument argument = @@ -381,12 +387,18 @@ choice [ rsb >> return [] , do - bs <- binding `sepBy1` symbol "," - rsb >> return bs + bs <- ((,) <$> getOffset <*> binding) `sepBy1` symbol "," + either (parseError . FancyError (repeating [] bs) . Set.singleton . ErrorFail) (const (pure ())) (uniqueBindings (map snd bs)) + rsb >> return (map snd bs) ] where rsb :: Parser String rsb = choice [symbol "]]", symbol "⟧"] + repeating :: [Attribute] -> [(Int, Binding)] -> Int + repeating _ [] = 0 + repeating seen ((offset, bd) : rest) + | any (`elem` seen) (attributesFromBindings [bd]) = offset + | otherwise = repeating (seen ++ attributesFromBindings [bd]) rest exHead :: Parser Expression exHead = diff --git a/src/Printer.hs b/src/Printer.hs --- a/src/Printer.hs +++ b/src/Printer.hs @@ -115,7 +115,15 @@ printSubst (Subst mp) config = intercalate "\n" - (map (\(key, value) -> printMeta key <> " >> " <> printMetaValue value config) (Map.toList mp)) + (map (\(key, value) -> numbered key <> " >> " <> printMetaValue value config) (Map.toList mp)) + where + numbered :: Meta -> String + numbered anon@(Anon slot@(Slot kind _)) + | length kin > 1 = printMeta anon <> "#" <> show (length (takeWhile (/= slot) kin) + 1) + where + kin :: [Slot] + kin = [other | Anon other@(Slot kind' _) <- Map.keys mp, kind' == kind] + numbered other = printMeta other printSubsts' :: [Subst] -> PrintConfig -> String printSubsts' [] _ = "------" diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -320,4 +320,7 @@ where macro :: String -> Text macro "evaluate" = "\\phinoEvaluate" - macro name = "\\" <> T.pack name + macro name = "\\" <> T.concat (zipWith camel [0 :: Int ..] (T.splitOn "-" (T.pack name))) + camel :: Int -> Text -> Text + camel 0 part = part + camel _ part = T.toTitle part diff --git a/src/Replacer.hs b/src/Replacer.hs --- a/src/Replacer.hs +++ b/src/Replacer.hs @@ -40,7 +40,7 @@ replaceExpression' :: ReplaceExpressionFunc' replaceExpression' state@(expr, ptns@(ptn : _ptns), repls@(repl : _repls)) | inert expr && not (inert ptn) = state - | expr == ptn = replaceExpression' (repl expr, _ptns, _repls) + | expr == ptn = let (ptns', repls') = swallowed expr (_ptns, _repls) in replaceExpression' (repl expr, ptns', repls') | otherwise = case expr of ExDispatch inner attr -> let (expr', ptns', repls') = replaceExpression' (inner, ptns, repls) @@ -88,6 +88,24 @@ (arg', ptns'', repls'') = replaceArgument (arg, ptns', repls') replaceExpressionFast' in (ExApplication expr' arg', ptns'', repls'') _ -> state + +swallowed :: Expression -> ([Expression], [Expression -> Expression]) -> ([Expression], [Expression -> Expression]) +swallowed replaced = go [] + where + go :: [Expression] -> ([Expression], [Expression -> Expression]) -> ([Expression], [Expression -> Expression]) + go dropped (ptn : ptns, _ : repls) + | length (filter (== ptn) dropped) < sum (map (occurrences ptn) (children replaced)) = go (ptn : dropped) (ptns, repls) + go _ pending = pending + occurrences :: Expression -> Expression -> Int + occurrences ptn term = (if term == ptn then 1 else 0) + sum (map (occurrences ptn) (children term)) + children :: Expression -> [Expression] + children (ExFormation bds) = [inner | BiTau _ inner <- bds] + children (ExDispatch inner _) = [inner] + children (ExApplication inner (ArTau _ arg)) = [inner, arg] + children (ExApplication inner (ArAlpha _ arg)) = [inner, arg] + children (ExPhiMeet _ _ inner) = [inner] + children (ExPhiAgain _ _ inner) = [inner] + children _ = [] replaceExpression :: ReplaceExpressionFunc replaceExpression state = diff --git a/src/Rewriter.hs b/src/Rewriter.hs --- a/src/Rewriter.hs +++ b/src/Rewriter.hs @@ -17,7 +17,7 @@ import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Map.Strict as Map -import Data.Maybe (fromMaybe) +import Data.Maybe (fromMaybe, isNothing) import Data.Set (Set) import qualified Data.Set as Set import Deps @@ -156,7 +156,9 @@ applied ctx expr = R.matchExpressionWithRule expr rule ctx >>= \case [] -> pure Nothing - matched -> Just <$> tryBuildAndReplaceFast (expr, rule.pattern, rule.result, matched) + matched + | isNothing rule.when -> Just <$> tryBuildAndReplaceFast (expr, rule.pattern, rule.result, matched) + | otherwise -> Just <$> buildAndReplace' (expr, rule.pattern, rule.result, matched) replaceExpression direct :: String -> Bool -> (Maybe Expression -> Expression -> [Expression]) -> Step direct name redex rewritten = Step name applied @@ -235,8 +237,8 @@ applicable _ [] _ = pure False applicable expression (rule : rest) ctx@RewriteContext{..} = _applied rule (RuleContext _buildTerm _universe _normal) expression >>= \case - Nothing -> applicable expression rest ctx - Just _ -> pure True + Just changed | changed /= expression -> pure True + _ -> applicable expression rest ctx rewrite :: Expression -> [Step] -> RewriteContext -> IO Rewrittens rewrite expr rules ctx@RewriteContext{..} = do diff --git a/src/Rule.hs b/src/Rule.hs --- a/src/Rule.hs +++ b/src/Rule.hs @@ -20,12 +20,12 @@ import Control.Exception (Exception (displayException)) import Control.Exception.Base (SomeException, try) import Control.Monad (when) -import qualified Data.ByteString.Char8 as B import Data.Foldable (foldlM) import Data.List (foldl', intersect, nub) import qualified Data.Map.Strict as M import Data.Maybe (catMaybes) import qualified Data.Text as T +import qualified Data.Text.Encoding as T import Deps (BuildTermFunc, BuildTermMethod, Term (..)) import Functions (buildTerm, nameOf) import GHC.IO (unsafePerformIO) @@ -175,22 +175,35 @@ _nf :: Expression -> Subst -> RuleContext -> IO [Subst] _nf (ExMeta meta) (Subst mp) ctx = case M.lookup (Named meta) mp of + Just (MvExpression expr) | bound expr -> pure [Subst mp | _normal ctx expr] Just (MvExpression expr) -> _nf expr (Subst mp) ctx _ -> pure [] _nf (ExAny slot) (Subst mp) ctx = case M.lookup (Anon slot) mp of + Just (MvExpression expr) | bound expr -> pure [Subst mp | _normal ctx expr] Just (MvExpression expr) -> _nf expr (Subst mp) ctx _ -> pure [] -_nf expr subst ctx = pure [subst | _normal ctx expr] +_nf expr subst ctx = do + built <- buildExpressionThrows expr subst + pure [subst | _normal ctx built] _absolute :: Expression -> Subst -> RuleContext -> IO [Subst] _absolute (ExMeta meta) (Subst mp) ctx = case M.lookup (Named meta) mp of + Just (MvExpression expr) | bound expr -> pure [Subst mp | xiFree expr] Just (MvExpression expr) -> _absolute expr (Subst mp) ctx _ -> pure [] _absolute (ExAny slot) (Subst mp) ctx = case M.lookup (Anon slot) mp of + Just (MvExpression expr) | bound expr -> pure [Subst mp | xiFree expr] Just (MvExpression expr) -> _absolute expr (Subst mp) ctx _ -> pure [] -_absolute expr subst _ = pure [subst | xiFree expr] +_absolute expr subst _ = do + built <- buildExpressionThrows expr subst + pure [subst | xiFree built] +bound :: Expression -> Bool +bound (ExMeta _) = False +bound (ExAny _) = False +bound _ = True + xiFree :: Expression -> Bool xiFree (ExFormation _) = True xiFree ExRoot = True @@ -216,7 +229,7 @@ _ -> pure [] _matches pat expr subst ctx = do (TeBytes tgt) <- _buildTerm ctx "dataize" [Y.ArgExpression expr] subst - matched <- match (B.pack pat) (B.pack (btsToUnescapedStr tgt)) + matched <- match (T.encodeUtf8 (T.pack pat)) (T.encodeUtf8 (T.pack (btsToUnescapedStr tgt))) pure [subst | matched] _partOf :: Expression -> Binding -> Subst -> RuleContext -> IO [Subst] diff --git a/src/XMIR.hs b/src/XMIR.hs --- a/src/XMIR.hs +++ b/src/XMIR.hs @@ -15,10 +15,12 @@ , parseXMIRThrows , xmirToPhi , xmirAtoms + , renameAtoms , Atoms , defaultXmirContext , escapeXML , escapeXMLText + , xmirTime , XmirContext (XmirContext) ) where @@ -26,18 +28,17 @@ import AST import Bytes (btsIsUtf8, btsSize, btsToNum, btsToStr, bytesToBts) import Control.Exception (Exception (displayException), throwIO) -import Control.Monad (unless) +import Control.Monad (unless, when) import Data.Bifunctor (bimap) import Data.Char (isAsciiLower, isDigit) import Data.Foldable (foldlM) -import Data.List (groupBy, intercalate) +import Data.List (find, groupBy, intercalate, nub) import qualified Data.Map as M -import Data.Maybe (catMaybes) +import Data.Maybe (catMaybes, fromMaybe) import qualified Data.Text as T import qualified Data.Text.Lazy as TL import qualified Data.Text.Lazy.Builder as TB -import Data.Time (UTCTime, diffUTCTime, getCurrentTime) -import Data.Time.Clock.POSIX (utcTimeToPOSIXSeconds) +import Data.Time (UTCTime (utctDayTime), diffTimeToPicoseconds, diffUTCTime, getCurrentTime) import Data.Time.Format (defaultTimeLocale, formatTime) import Data.Version (showVersion) import Development.GitRev (gitHash) @@ -143,17 +144,18 @@ , bts ] ) -expression app@(ExApplication _ (ArTau AtRho _)) _ = throwIO (UnsupportedExpression app) -expression (ExApplication expr arg) ctx = do +expression app@(ExApplication expr (ArTau AtRho _)) ctx@XmirContext{..} + | _hideRho = expression expr ctx + | otherwise = throwIO (UnsupportedExpression app) +expression app@(ExApplication expr arg) ctx = do (base, children) <- expression expr ctx + when (null base) (throwIO (UnsupportedExpression app)) (base', children') <- expression texpr ctx let attrs = if null base' then [("as", as)] else [("as", as), ("base", base')] - if null base && not (null children) - then pure ("", [object [] (children ++ [object attrs children'])]) - else pure (base, children ++ [object attrs children']) + pure (base, children ++ [object attrs children']) where (as, texpr) = case arg of ArTau attr value -> (printAttribute attr, value) @@ -195,6 +197,8 @@ ExApplication _ _ -> programToXMIR expr ctx ExDispatch _ _ -> programToXMIR expr ctx ExRoot -> programToXMIR expr ctx + ExTermination -> programToXMIR expr ctx + ExXi -> programToXMIR expr ctx _ -> throwIO (UnsupportedTopExpression expr) expressionToXMIR expr@(ExFormation bds) ctx = documentWith ctx [] expr rootNodes @@ -258,7 +262,7 @@ [ ("author", "phino") , ("dob", formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" now) , ("ms", show ms) - , ("time", time now) + , ("time", xmirTime now) , ("version", showVersion version) , ("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance") , ("xsi:noNamespaceSchemaLocation", "https://raw.githubusercontent.com/objectionary/eo/refs/heads/gh-pages/XMIR.xsd") @@ -295,15 +299,16 @@ ) ] ) - time :: UTCTime -> String - time stamp = - let base = formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" stamp - posix = utcTimeToPOSIXSeconds stamp - fractional :: Double - fractional = realToFrac posix - fromInteger (floor posix) - nanos = floor (fractional * 1_000_000_000) :: Int - in base ++ "." ++ printf "%09d" nanos ++ "Z" +xmirTime :: UTCTime -> String +xmirTime stamp = + formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" stamp + ++ printf ".%09dZ" ((diffTimeToPicoseconds (utctDayTime stamp) `div` 1_000) `mod` 1_000_000_000) + +renameAtoms :: [(T.Text, T.Text)] -> XmirContext -> XmirContext +renameAtoms renames ctx@XmirContext{..} = + ctx{_atoms = M.fromList [(new, atom) | (old, new) <- renames, Just atom <- [M.lookup old _atoms]]} + escapeXML :: String -> String escapeXML = concatMap escapeChar where @@ -321,6 +326,7 @@ escapeChar :: Char -> String escapeChar '&' = "&" escapeChar '<' = "<" + escapeChar '>' = ">" escapeChar ch = [ch] indent :: Int -> TB.Builder @@ -419,6 +425,7 @@ xmirToPhi :: Document -> IO Expression xmirToPhi xmir = let doc = C.fromDocument xmir + derived = derivedNames xmir in case C.node doc of NodeElement el | nameLocalName (elementName el) == "object" -> do @@ -432,20 +439,21 @@ , let heads = meta C.$/ C.element (toName "head") C.&/ C.content , heads == ["package"] , tail' <- meta C.$/ C.element (toName "tail") C.&/ C.content - , t <- T.splitOn "." tail' + , t <- T.splitOn "." (T.strip tail') ] + mapM_ (`toAttr` doc) pckg if bareRoot o then if null pckg - then xmirToFormation o [] + then xmirToFormation derived o [] else throwIO (InvalidXMIRFormat "A with package must hold a named " doc) else if null pckg then do - bd <- xmirToFormationBinding o [] + bd <- xmirToFormationBinding derived o [] pure (ExFormation [bd]) else do - obj <- xmirToFormationBinding o [] + obj <- xmirToFormationBinding derived o [] let bd = foldr (\part acc -> BiTau (AtLabel (T.pack part)) (ExFormation [acc, BiLambda (Function "Package")])) obj pckg pure (ExFormation [bd]) | otherwise -> throwIO (InvalidXMIRFormat "Expected single element" doc) @@ -454,17 +462,17 @@ bareRoot :: C.Cursor -> Bool bareRoot o = not (any (`hasAttr` o) ["name", "base", "as"]) -xmirToFormationBinding :: C.Cursor -> [String] -> IO Binding -xmirToFormationBinding cur fqn +xmirToFormationBinding :: Derived -> C.Cursor -> [String] -> IO Binding +xmirToFormationBinding derived cur fqn | not (hasAttr "name" cur) = throwIO (InvalidXMIRFormat "Formation children must have @name attribute" cur) | not (hasAttr "base" cur) = do name <- getAttr "name" cur case name of - "Ξ»" -> BiLambda . Function <$> lambdaName cur fqn + "Ξ»" -> BiLambda . Function <$> lambdaName derived cur fqn ('Ξ±' : _) -> throwIO (InvalidXMIRFormat "Formation child @name can't start with Ξ±" cur) - "Ο†" -> BiTau AtPhi <$> xmirToFormation cur (name : fqn) - "ρ" -> BiTau AtRho <$> xmirToFormation cur (name : fqn) - _ -> BiTau (AtLabel (T.pack name)) <$> xmirToFormation cur (name : fqn) + "Ο†" -> BiTau AtPhi <$> xmirToFormation derived cur (name : fqn) + "ρ" -> BiTau AtRho <$> xmirToFormation derived cur (name : fqn) + _ -> BiTau (AtLabel (T.pack name)) <$> xmirToFormation derived cur (name : fqn) | otherwise = do name <- getAttr "name" cur base <- getAttr "base" cur @@ -476,17 +484,49 @@ case base of "βˆ…" -> pure (BiVoid attr) _ -> do - expr <- xmirToExpression cur fqn + expr <- xmirToExpression derived cur fqn pure (BiTau attr expr) -lambdaName :: C.Cursor -> [String] -> IO T.Text -lambdaName cur fqn +type Derived = M.Map [String] T.Text + +lambdaName :: Derived -> C.Cursor -> [String] -> IO T.Text +lambdaName derived cur fqn | hasText cur = T.strip . T.pack <$> getText cur - | otherwise = pure (T.pack (intercalate "_" ("L" : map (map spell) (reverse fqn)))) + | otherwise = pure (M.findWithDefault (spelled fqn) fqn derived) + +spelled :: [String] -> T.Text +spelled fqn = T.pack (intercalate "_" ("L" : map (map spell) (reverse fqn))) where spell :: Char -> Char spell ch = if isDigit ch || isAsciiLower ch || ch == '_' || ch == 'Ο†' then ch else '_' +derivedNames :: Document -> Derived +derivedNames xmir = snd (foldl assign ([], M.empty) paths) + where + paths :: [[String]] + paths = + nub + [ lambdaPath cur + | cur <- C.fromDocument xmir C.$// C.element (toName "o") C.>=> C.attributeIs (toName "name") "Ξ»" + , not (hasText cur) + ] + bases :: [T.Text] + bases = map spelled paths + assign :: ([T.Text], Derived) -> [String] -> ([T.Text], Derived) + assign (used, names) path = + let base = spelled path + name = fromMaybe base (find (\candidate -> candidate `notElem` used && (candidate == base || candidate `notElem` bases)) (base : [base <> T.pack ('_' : show n) | n <- [2 :: Int ..]])) + in (name : used, M.insert path name names) + +lambdaPath :: C.Cursor -> [String] +lambdaPath cur = + [ T.unpack label + | enclosing <- cur C.$| (C.ancestor C.>=> C.element (toName "o")) + , not (hasAttr "base" enclosing) + , not (hasAttr "as" enclosing) + , label <- C.attribute (toName "name") enclosing + ] + xmirAtoms :: Document -> IO Atoms xmirAtoms xmir = M.fromList <$> mapM entry markers where @@ -496,36 +536,30 @@ C.$// C.element (toName "o") C.>=> C.attributeIs (toName "name") "Ξ»" C.>=> C.check (hasAttr "atom") + derived :: Derived + derived = derivedNames xmir entry :: C.Cursor -> IO (T.Text, String) entry cur = do - name <- lambdaName cur (locator cur) + name <- lambdaName derived cur (lambdaPath cur) atom <- getAttr "atom" cur pure (name, atom) - locator :: C.Cursor -> [String] - locator cur = - [ T.unpack label - | enclosing <- cur C.$| (C.ancestor C.>=> C.element (toName "o")) - , not (hasAttr "base" enclosing) - , not (hasAttr "as" enclosing) - , label <- C.attribute (toName "name") enclosing - ] -xmirToFormation :: C.Cursor -> [String] -> IO Expression -xmirToFormation cur fqn = do +xmirToFormation :: Derived -> C.Cursor -> [String] -> IO Expression +xmirToFormation derived cur fqn = do bds <- concat <$> mapM binding (groupBy (\left right -> not (nested left) && not (nested right)) (C.child cur)) ExFormation <$> uniqueBindings' bds where nested :: C.Cursor -> Bool nested node = not (null (C.element (toName "o") node)) binding :: [C.Cursor] -> IO [Binding] - binding [node] | nested node = pure <$> xmirToFormationBinding node fqn + binding [node] | nested node = pure <$> xmirToFormationBinding derived node fqn binding nodes = pure [BiDelta (bytesToBts (T.unpack text)) | not (T.null text)] where text :: T.Text text = T.strip (T.concat [content | NodeContent content <- map C.node nodes]) -xmirToExpression :: C.Cursor -> [String] -> IO Expression -xmirToExpression cur fqn +xmirToExpression :: Derived -> C.Cursor -> [String] -> IO Expression +xmirToExpression derived cur fqn | hasAttr "base" cur = do base <- getAttr "base" cur case base of @@ -537,10 +571,10 @@ in case args of [] -> throwIO (InvalidXMIRFormat (printf "Element with @base='%s' must have at least one child" base) cur) arg : args' -> do - expr <- xmirToExpression arg fqn + expr <- xmirToExpression derived arg fqn attr <- toAttr rest cur let disp = ExDispatch expr attr - xmirToApplication disp args' fqn + xmirToApplication derived disp args' fqn "ΞΎ" -> if null (cur C.$/ C.element (toName "o")) then pure ExXi @@ -549,12 +583,12 @@ if null (cur C.$/ C.element (toName "o")) then pure ExRoot else throwIO (InvalidXMIRFormat "Application of 'Ξ¦' is illegal in XMIR" cur) - "βŠ₯" -> xmirToApplication ExTermination (cur C.$/ C.element (toName "o")) fqn + "βŠ₯" -> xmirToApplication derived ExTermination (cur C.$/ C.element (toName "o")) fqn 'βŠ₯' : '.' : rest -> xmirToExpression' ExTermination "βŠ₯" 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 = xmirToFormation cur fqn + | otherwise = xmirToFormation derived cur fqn where xmirToExpression' :: Expression -> String -> String -> C.Cursor -> [String] -> IO Expression xmirToExpression' start symbol rst c names = @@ -566,10 +600,10 @@ (\acc part -> ExDispatch acc <$> toAttr (T.unpack part) c) start (T.splitOn "." (T.pack rst)) - xmirToApplication head' (c C.$/ C.element (toName "o")) names + xmirToApplication derived head' (c C.$/ C.element (toName "o")) names -xmirToApplication :: Expression -> [C.Cursor] -> [String] -> IO Expression -xmirToApplication = xmirToApplication' 0 +xmirToApplication :: Derived -> Expression -> [C.Cursor] -> [String] -> IO Expression +xmirToApplication derived = xmirToApplication' 0 where xmirToApplication' :: Int -> Expression -> [C.Cursor] -> [String] -> IO Expression xmirToApplication' _ expr [] _ = pure expr @@ -578,7 +612,7 @@ | hasAttr "name" arg = throwIO (InvalidXMIRFormat "Application argument can't have @name attribute" arg) | 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")) + bds <- mapM (\node -> xmirToFormationBinding derived node fqn) (arg C.$/ C.element (toName "o")) key <- asToKey arg idx pure (ExApplication expr (mkArg key (ExFormation bds))) | not (hasAttr "base" arg) && hasText arg = do @@ -587,7 +621,7 @@ pure (ExApplication expr (mkArg key (ExFormation [BiDelta (bytesToBts bytes)]))) | otherwise = do key <- asToKey arg idx - arg' <- xmirToExpression arg fqn + arg' <- xmirToExpression derived arg fqn pure (ExApplication expr (mkArg key arg')) app' <- app xmirToApplication' (idx + 1) app' args fqn diff --git a/src/Yaml.hs b/src/Yaml.hs --- a/src/Yaml.hs +++ b/src/Yaml.hs @@ -18,6 +18,8 @@ import qualified Data.Aeson.KeyMap as KeyMap import qualified Data.ByteString as BS import Data.FileEmbed (embedDir) +import Data.Maybe (fromMaybe) +import Data.Scientific (isInteger) import Data.Text (Text, unpack) import Data.Yaml (Parser) import qualified Data.Yaml as Yaml @@ -80,8 +82,9 @@ , Domain <$> o .: "domain" ] Number num - | toRational (round num :: Integer) == toRational num -> pure (Literal (round num)) - | otherwise -> fail (printf "Expected an integer, got a fractional number %s" (show num)) + | toRational (round num :: Integer) /= toRational num -> fail (printf "Expected an integer, got a fractional number %s" (show num)) + | (round num :: Integer) < toInteger (minBound :: Int) || (round num :: Integer) > toInteger (maxBound :: Int) -> fail (printf "The literal %s does not fit into Int" (show num)) + | otherwise -> pure (Literal (round num)) String txt -> case parseIndex (unpack txt) of Right (Right mt) -> pure (MetaIndex mt) Right (Left slot) -> pure (AnyIndex slot) @@ -90,6 +93,9 @@ fail "Expected a numerable expression (object, number or index meta)" instance FromJSON Comparable where + parseJSON (Number num) + | isInteger num && ((round num :: Integer) < toInteger (minBound :: Int) || (round num :: Integer) > toInteger (maxBound :: Int)) = + fail (printf "The literal %s does not fit into Int" (show num)) parseJSON v = asum [ CmpAttr <$> parseJSON v @@ -190,7 +196,21 @@ referenceless rule.name "when" rule.when referenceless rule.name "where" rule.where_ referenceless rule.name "having" rule.having + targets rule (metas rule.pattern) (fromMaybe [] rule.where_) pure rule + where + targets :: Rule -> [Text] -> [Extra] -> Parser () + targets _ _ [] = pure () + targets rule known (extra : rest) = case extra.meta of + ArgExpression (ExMeta bound) -> fresh rule known bound >> targets rule (bound : known) rest + ArgAttribute (AtMeta bound) -> fresh rule known bound >> targets rule (bound : known) rest + ArgBinding (BiMeta bound) -> fresh rule known bound >> targets rule (bound : known) rest + ArgBytes (BtMeta bound) -> fresh rule known bound >> targets rule (bound : known) rest + _ -> fail (printf "The rule '%s' has a 'where' step whose 'meta' is not a meta, while only a meta can take its result" rule.name) + fresh :: Rule -> [Text] -> Text -> Parser () + fresh rule known bound + | bound `elem` known = fail (printf "The rule '%s' has a 'where' step that binds the meta '%s' again, while it is already bound" rule.name (unpack bound)) + | otherwise = pure () data Number = MetaIndex Text diff --git a/test/BytesSpec.hs b/test/BytesSpec.hs --- a/test/BytesSpec.hs +++ b/test/BytesSpec.hs @@ -253,8 +253,8 @@ , btsEqual (BtOne "bf") (BtOne "BF") `shouldBe` True ) , - ( "decodes a single hex character via the fallback numeric reader" - , btsEqual (BtOne "5") (BtOne "05") `shouldBe` True + ( "rejects a hex byte with more than two digits" + , evaluate (btsToUnescapedStr (BtOne "100")) `shouldThrow` anyErrorCall ) , ( "errors out on a hex digit that isn't 0-9, a-f or A-F" diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -226,9 +226,25 @@ , ["rewrite", "--flat", "--sweet", "--hide-rho"] , ["⟦ x(y) ↦ 42:a ⟧"] ) + , + ( "prints a lone void as the term without the rho would be printed" + , "⟦ a ↦ ⟦ x ↦ ⟦ ρ ↦ ΞΎ, y ↦ βˆ… ⟧ ⟧ ⟧" + , ["rewrite", "--sweet", "--hide-rho"] + , ["⟦ x(y) ↦ ⟦⟧ ⟧:a"] + ) + , + ( "indents the body as the term without the rho would be indented" + , "⟦ a ↦ ⟦ x ↦ ⟦ ρ ↦ βˆ…, b ↦ ⟦ c ↦ βˆ…, ρ ↦ βˆ… ⟧ ⟧ ⟧ ⟧" + , ["rewrite", "--sweet", "--hide-rho", "--margin=3"] + , ["⟦\n b(c) ↦ ⟦⟧\n⟧:x:a"] + ) ] (\(desc, input, args, expected) -> it desc (withStdin input (testCLISucceeded args expected))) + it "keeps a data literal sugared when it is applied to more arguments" $ + withStdin "⟦ i ↦ 42(z ↦ ΞΎ.f), s ↦ \"Hello\"(z ↦ ΞΎ.f) ⟧" $ + testCLISucceeded ["rewrite", "--sweet", "--flat"] ["⟦ i ↦ 42( z ↦ f ), s ↦ \"Hello\"( z ↦ f ) ⟧"] + it "prints the one-binding sugar after inline voids with --sweet" $ withStdin "[[ x(y) -> [[ a -> 42 ]] ]]" $ testCLISucceeded ["rewrite", "--sweet"] ["⟦ x(y) ↦ 42:a ⟧"] @@ -246,6 +262,16 @@ testCLISucceeded ["rewrite", "--log-level=" ++ flagValue] ["⟧"] ) + describe "--log-level prints nothing below its level" $ + forM_ + [("NONE", ["[DEBUG]", "[INFO]"]), ("ERROR", ["[DEBUG]", "[INFO]"]), ("INFO", ["[DEBUG]"])] + ( \(level, hidden) -> + it ("--log-level=" ++ level) $ + withStdin "[[]]" $ do + (out, _) <- withStdout (try (runCLI ["rewrite", "--log-level=" ++ level]) :: IO (Either ExitCode ())) + forM_ hidden (out `shouldNotContain`) + ) + it "fails on an unrecognized --log-level value" $ withStdin "[[]]" $ testCLIFailed ["rewrite", "--log-level=verbose"] ["unknown log-level: verbose"] @@ -311,6 +337,24 @@ , ["--update requires an input file"] ) , + ( "when --sequence is used with --in-place" + , "[[ ]]" + , ["rewrite", "--sequence", "--in-place", "input.phi"] + , ["--in-place and --sequence cannot be used together"] + ) + , + ( "when --focus is used with --in-place" + , "[[ ]]" + , ["rewrite", "--focus=Q.y", "--in-place", "input.phi"] + , ["--in-place and --focus cannot be used together"] + ) + , + ( "when --show is used with --in-place" + , "[[ ]]" + , ["rewrite", "--show=Q.y", "--in-place", "input.phi"] + , ["--in-place and --show cannot be used together"] + ) + , ( "when --update is used with --in-place" , "[[ ]]" , ["rewrite", "--update", "--in-place", "input.phi"] @@ -378,6 +422,7 @@ , ["[ERROR]:", "Only dispatch expression started with Ξ¦ (or Q) can be used in --show"] ) , ("with --show overlapping --hide", ["rewrite", "--show=Q.x", "--hide=Q.x"], ["[ERROR]:", "The --show locator 'Ξ¦.x' is also listed in --hide"]) + , ("with --hide of an ancestor of --show", ["rewrite", "--show=Q.y.z", "--hide=Q.y"], ["[ERROR]:", "The --show locator 'Ξ¦.y.z' lies inside the --hide locator 'Ξ¦.y'"]) , ("with --meet-popularity < 0", ["rewrite", "--meet-popularity=-1"], ["[ERROR]:", "--meet-popularity must be positive"]) , ("with --meet-popularity > 100", ["rewrite", "--meet-popularity=102"], ["[ERROR]:", "--meet-popularity must be <= 100"]) , @@ -447,6 +492,18 @@ doesFileExist (dir ++ "/00001.phi") `shouldReturn` True doesFileExist (dir ++ "/00003.phi") `shouldReturn` True + it "gives the saved steps the --canonize and --hide of the printed ones" $ + withTempDirectory "phino-steps-filtered" $ \dir -> + withStdin "[[ m -> [[ x -> [[ L> Plus ]], y -> $.x ]].y, k -> [[ L> Minus ]] ]]" $ do + testCLISucceeded + ["rewrite", "--normalize", "--hide=Q.k", "--canonize", "--steps-dir=" ++ dir, "--flat"] + ["Fn1"] + files <- listDirectory dir + null files `shouldBe` False + saved <- mapM (\file -> readFile (dir ++ "/" ++ file)) files + concat saved `shouldNotContain` "Minus" + concat saved `shouldNotContain` "Plus" + it "saves dataize steps to dir with --steps-dir" $ withTempDirectory "phino-steps-dataize" $ \dir -> withStdin "[[ bytes ↦ ⟦ Ο† ↦ βˆ… ⟧, number(Ο†) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ do @@ -880,7 +937,7 @@ withStdin "[[ app -> [[]] ]]" $ testCLISucceeded ["rewrite", "--output=xmir", "--omit-comments", "--sweet", "--flat"] - [" [[ app -> [[]] ]]"] + [" [[ app -> [[]] ]]"] it "print expression in listing in XMIRs with --sequence" $ withStdin "[[ x -> \"foo\" ]]" $ @@ -1106,10 +1163,31 @@ , "⟦ x ↦ βˆ…, y ↦ x ⟧( x ↦ 42-:Ξ” ).y" ] + it "finishes under --depth-sensitive when the only match left would not change the term" $ + withTempFileContent "phino-fixpoint.yaml" "name: fix\npattern: '[[ x -> !e1, !B1 ]]'\nresult: '[[ x -> Q, !B1 ]]'\n" $ \fix -> + withStdin "[[ x -> $ ]]" $ + testCLISucceeded ["rewrite", "--rule=" ++ fix, "--max-depth=1", "--depth-sensitive", "--flat"] ["⟦ x ↦ Ξ¦ ⟧"] + + describe "morph --focus under --locator" $ do + it "finds the same object for the steps and for the answer" $ + withStdin "⟦ t ↦ ⟦ a ↦ ⟦ Ξ” ‍ 01- ⟧ ⟧, a ↦ ⟦ Ξ” ‍ 02- ⟧ ⟧" $ do + (out, _) <- withStdout (runCLI ["morph", "--locator=Q.t", "--focus=Q.a", "--flat", "--sequence"]) + filter (not . null) (lines out) `shouldSatisfy` all (== "⟦ Ξ” ‍ 02- ⟧") + it "prints the answer when --focus names the object at --locator" $ + withStdin "⟦ t ↦ ⟦ a ↦ ⟦ Ξ” ‍ 01- ⟧ ⟧ ⟧" $ + testCLISucceeded ["morph", "--locator=Q.t", "--focus=Q.t", "--flat", "--sequence"] ["⟦ a ↦ ⟦ Ξ” ‍ 01- ⟧ ⟧"] + it "fails on a --focus it cannot find before it prints any step" $ + withStdin "⟦ t ↦ ⟦ a ↦ ⟦ Ξ” ‍ 01- ⟧ ⟧ ⟧" $ do + (out, _) <- withStdout (try (runCLI ["morph", "--locator=Q.t", "--focus=Q.nope", "--flat", "--sequence"]) :: IO (Either ExitCode ())) + out `shouldNotContain` "⟦ t ↦" + describe "dataize" $ do it "prints help" $ testCLISucceeded ["dataize", "--help"] ["Dataize the πœ‘-expression"] + it "names every block of a --symbolic entry in its help" $ + testCLISucceeded ["dataize", "--help"] ["\"dataize\"", "\"morph\"", "\"rewrite\"", "\"symbolize\"", "\"join\""] + it "dataizes simple expression" $ withStdin "[[ D> 01- ]]" $ testCLISucceeded ["dataize"] ["01-"] @@ -1165,7 +1243,7 @@ withStdin circling $ testCLISucceeded ["dataize", "--locator=Q.t", "--acyclic=proven", "--partial", "--max-steps=4000", "--flat", "--hide-rho"] - ["⟦ cyc ↦ ⟦ x ↦ βˆ…, Ο† ↦ Ξ¦.cyc( Ξ±0 ↦ ΞΎ.x ) ⟧, t ↦ Ξ¦.cyc( Ξ±0 ↦ ⟦⟧ ) ⟧"] + ["Ξ¦.cyc( Ξ±0 ↦ ⟦⟧ )"] it "writes the cut to the protocol where the formation would have opened" $ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do @@ -1296,6 +1374,20 @@ testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] [] records <- readProtocol path lines records `shouldContain` [" "] + forM_ + [ ("textXXXXXX.txt", " 𝛿1.1 := 01-02-..(8b)..-0B-0C # 𝔻(ΞΎ.arg)") + , ("XMLXXXXXX.xml", " 01-02-..(8b)..-0B-0C") + ] + ( \(template, line) -> + it ("cuts a long datum a firing came down to, as " ++ line) $ + withTempFile template $ \(path, stream) -> do + hClose stream + withLambdasOf (T.pack "- Ξ»: L_outer\n dataize:\n 𝛿1: ΞΎ.arg\n 𝑛: ⟦ Ξ» ‍ 𝜎 ⟧\n") $ \outer -> + withStdin "⟦ x ↦ ⟦ arg ↦ ⟦ Ξ” ‍ 01-02-03-04-05-06-07-08-09-0A-0B-0C ⟧, Ξ» ‍ L_outer ⟧ ⟧" $ + testCLISucceeded ["dataize", "--symbolic=" ++ outer, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] [] + records <- readProtocol path + lines records `shouldContain` [line] + ) it "folds a long formation under the width given as the value" $ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream @@ -1492,6 +1584,22 @@ , " 𝑛.1.2 := 𝜎1:Ξ»:z # 𝕄(𝑛.1.1)" ] + it "writes a deferred copy as a call of the object of the world it was made of" $ + withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do + hClose stream + withStdin "⟦ box(x) ↦ ⟦ Ο† ↦ x.next ⟧, y ↦ Ξ¦.box( x ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ) ⟧" $ + testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readProtocol path + lines records `shouldContain` [" deferred(𝜎2) := Ξ¦.box( x ↦ 𝜎1:Ξ» ) # 𝕄(Ξ¦.y)"] + + it "writes a deferred copy as it stands when the world declares no object it was made of" $ + withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do + hClose stream + withStdin "⟦ wrap(v) ↦ ⟦⟧, y ↦ Ξ¦.wrap( v ↦ ⟦ b(x) ↦ ⟦ Ο† ↦ x.next ⟧ ⟧ ).v.b( x ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ) ⟧" $ + testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readProtocol path + lines records `shouldContain` [" deferred(𝜎2) := ⟦ x ↦ 𝜎1:Ξ», Ο† ↦ x.next ⟧ # 𝕄(Ξ¦.y)"] + it "writes a told stall to the XML protocol" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do hClose stream @@ -1519,6 +1627,19 @@ records <- readProtocol path lines records `shouldContain` [" "] + forM_ + [("XMLXXXXXX.xml", " + it ("writes a spent firing budget to the protocol as " ++ record) $ + withTempFile template $ \(path, stream) -> do + hClose stream + loopingLambdas $ \endless -> + withStdin "⟦ @ ↦ ⟦ Ξ» ‍ L_loop ⟧ ⟧" $ + testCLIFailed ["dataize", "--symbolic=" ++ endless, "--max-steps=400", "--max-firings=5", "--protocol=" ++ path] ["--max-firings=5"] + records <- readProtocol path + any (record `isInfixOf`) (lines records) `shouldBe` True + ) + it "keeps the lines of a run that fails" $ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream @@ -1776,6 +1897,60 @@ , "" ] + it "writes the copy a deferred symbol stands for as an element of its own" $ + withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do + hClose stream + withStdin "⟦ box(x) ↦ ⟦ Ο† ↦ x.next ⟧, y ↦ Ξ¦.box( x ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ) ⟧" $ + testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readProtocol path + lines records + `shouldBe` [ "" + , "" + , " 𝜎1⟦ x ↦ 𝜎1:Ξ», Ο† ↦ x.next ⟧" + , "" + ] + + it "names the object a deferred copy was made of through the formation its ρ holds" $ + withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do + hClose stream + withStdin "⟦ joined(items) ↦ ⟦ Ο† ↦ step( tup ↦ items ), step(ρ, tup) ↦ ⟦ Ο† ↦ tup.next ⟧ ⟧, y ↦ Ξ¦.joined( items ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ).Ο† ⟧" $ + testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readProtocol path + lines records `shouldContain` [" 𝜎1⟦ tup ↦ 𝜎1:Ξ», Ο† ↦ tup.next ⟧"] + + it "names the object a deferred copy was made of after the walk wrote an answer into its ρ" $ + withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do + hClose stream + withLambdasOf (T.pack "- Ξ»: L_dataized\n dataize:\n 𝛿1: $.target\n 𝑛: Ξ¦.bytes( Ο† ↦ ⟦ Ξ» ‍ 𝜎 ⟧ )\n") $ \dataized -> + withStdin "⟦ bytes(Ο†) ↦ ⟦⟧, dataized(target) ↦ L_dataized:Ξ», joined(items) ↦ ⟦ Ο† ↦ step( tup ↦ items, s ↦ sep ), sep ↦ Ξ¦.dataized( target ↦ items ), step(ρ, tup, s) ↦ ⟦ Ο† ↦ tup.next ⟧ ⟧, y ↦ Ξ¦.joined( items ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ).Ο† ⟧" $ + testCLISucceeded ["morph", "--deep", "--symbolic=" ++ dataized, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readProtocol path + lines records `shouldContain` [" 𝜎1?⟦ tup ↦ 𝜎1:Ξ», s ↦ 𝜎2:Ξ»:Ο†, Ο† ↦ tup.next ⟧"] + + it "writes a question mark for an argument of a deferred copy that is no bare symbol" $ + withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do + hClose stream + withStdin "⟦ box(x, w) ↦ ⟦ Ο† ↦ x.next ⟧, y ↦ Ξ¦.box( x ↦ ⟦ Ξ» ‍ 𝜎1 ⟧, w ↦ ⟦ z ↦ Ξ¦ ⟧ ) ⟧" $ + testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readProtocol path + lines records `shouldContain` [" 𝜎1?⟦ x ↦ 𝜎1:Ξ», w ↦ Ξ¦:z, Ο† ↦ x.next ⟧"] + + it "writes the object a deferred copy was made of whatever --abridged says" $ + withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do + hClose stream + withStdin "⟦ joined(items) ↦ ⟦ Ο† ↦ step( tup ↦ items ), step(ρ, tup) ↦ ⟦ Ο† ↦ tup.next ⟧ ⟧, y ↦ Ξ¦.joined( items ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ).Ο† ⟧" $ + testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--abridged=20", "--quiet", "--sweet", "--hide-rho"] [] + records <- readProtocol path + lines records `shouldContain` [" 𝜎1⟦ Ο† ↦ tup.next, +1 ⟧"] + + it "writes no object for a deferred copy of a formation the world does not declare" $ + withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do + hClose stream + withStdin "⟦ wrap(v) ↦ ⟦⟧, y ↦ Ξ¦.wrap( v ↦ ⟦ b(x) ↦ ⟦ Ο† ↦ x.next ⟧ ⟧ ).v.b( x ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ) ⟧" $ + testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readProtocol path + lines records `shouldContain` [" ⟦ x ↦ 𝜎1:Ξ», Ο† ↦ x.next ⟧"] + it "writes no 'minted' element for a firing minting nothing" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do hClose stream @@ -1986,17 +2161,16 @@ withStdin "[[ bytes ↦ ⟦ Ο† ↦ βˆ… ⟧, number(Ο†) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ testCLISucceeded ["dataize", symbolic, "--partial"] ["40-45-00-00-00-00-00-00"] - it "prints the residual to XMIR, with its real listing by default" $ + it "prints the residual at --locator, which XMIR has no top level for" $ withStdin wrapped $ - testCLISucceeded - ["dataize", symbolic, "--partial", "--locator=Q.app", "--output=xmir"] - ["L_number_nope", "", "⟦"] + testCLIFailed + ["dataize", symbolic, "--partial", "--locator=Q.app", "--output=xmir", "--hide-rho"] + ["[ERROR]:", "its top level must be a single binding"] - it "honors --hide-rho and --omit-listing when printing the residual to XMIR" $ - withStdin wrapped $ - testCLISucceeded - ["dataize", symbolic, "--partial", "--locator=Q.app", "--output=xmir", "--hide-rho", "--omit-listing"] - ["L_number_nope", "line(s)"] + it "prints the residual at --locator, not the whole program" $ + withStdin wrapped $ do + (out, _) <- withStdout (runCLI ["dataize", symbolic, "--partial", "--locator=Q.app", "--hide-rho", "--flat"]) + lines out `shouldBe` ["⟦ Ξ» ‍ L_number_nope ⟧"] it "cannot print a residual of several top bindings as XMIR" $ withStdin dispatched $ @@ -2557,6 +2731,13 @@ ["[ERROR]:", "Only dispatch expression started with Ξ¦ (or Q) can be used in --locator"] describe "explain" $ do + forM_ + ["--morph", "--dataize", "--contextualize"] + ( \judgment -> + it ("refuses --normalize together with " ++ judgment) $ + testCLIFailed ["explain", judgment, "--normalize"] ["The --normalize option cannot be used together with"] + ) + it "prints help" $ testCLISucceeded ["explain", "--help"] @@ -2704,6 +2885,13 @@ ["merge", "--input=xmir", "--output=xmir", file] ["L_number_plus"] + it "keeps the type of an atom of XMIR under --canonize" $ do + let xmir = "" + withTempFileContent "phino-canonized-atom.xmir" xmir $ \file -> + testCLISucceeded + ["rewrite", "--input=xmir", "--output=xmir", "--canonize", file] + ["Fn1"] + it "reproduces the same output for the same --seed" $ do let args = [ "merge" @@ -2767,6 +2955,10 @@ withStdin "[[]]" $ testCLISucceeded ["match", "--log-level=debug"] ["[DEBUG]: The --pattern is not provided, no substitutions are built"] + it "refuses --when without --pattern" $ + withStdin "[[]]" $ + testCLIFailed ["match", "--when=bogus"] ["The option --when requires --pattern"] + it "reproduces the same output for the same --seed" $ do dir <- getTemporaryDirectory let file = dir ++ "/phino-match-seed-test.phi" @@ -2784,9 +2976,17 @@ firstRun `shouldBe` secondRun removeFile file + it "numbers two anonymous captures of one kind, so they stay apart" $ + withStdin "[[ a -> [[ ]], b -> Q ]]" $ + testCLISucceeded ["match", "--pattern=[[ !t -> !e, !t -> !e ]]"] ["e#1 >> ⟦⟧\ne#2 >> Ξ¦\nt#1 >> a\nt#2 >> b"] + it "prints many substitutions" $ withStdin "[[ x -> Q.x, y -> Q.y ]]" $ testCLISucceeded ["match", "--pattern=Q.!t"] ["t >> x\n------\nt >> y"] + + it "does not match a length against a literal that wraps around Int" $ + withStdin "[[ a -> $, b -> Q ]]" $ + testCLIFailed ["match", "--pattern=[[ !B1 ]]", "--when=eq(length(!B1),18446744073709551618)"] ["no substitutions are built"] it "builds substitutions with conditions" $ withStdin "[[ x -> Q.y ]].x" $ diff --git a/test/ConditionSpec.hs b/test/ConditionSpec.hs --- a/test/ConditionSpec.hs +++ b/test/ConditionSpec.hs @@ -5,7 +5,7 @@ module ConditionSpec where -import AST (Attribute (AtLabel, AtMeta), Binding (BiMeta), Expression (ExDispatch, ExMeta, ExRoot)) +import AST (Attribute (AtDelta, AtLabel, AtLambda, AtMeta), Binding (BiMeta), Expression (ExDispatch, ExMeta, ExRoot)) import Condition import Control.Exception (SomeException) import Control.Monad (forM_) @@ -43,6 +43,9 @@ , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExRoot (AtLabel "x"))]) , ("and(matches(\"hi\", !e1),part-of(!e1, !B1))", Y.And [Y.Matches "hi" (ExMeta "e1"), Y.PartOf (ExMeta "e1") (BiMeta "B1")]) , ("not(formation(!n1))", Y.Not (Y.IsFormation (ExMeta "n1"))) + , ("in(Ξ”, !B1)", Y.In [AtDelta] [BiMeta "B1"]) + , ("in(Ξ», !B1)", Y.In [AtLambda] [BiMeta "B1"]) + , ("in([Ξ”, Ξ»], [!B1, !B2])", Y.In [AtDelta, AtLambda] [BiMeta "B1", BiMeta "B2"]) ] (\(expr, res) -> it expr (parseCondition expr `shouldBe` Right res)) diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -102,6 +102,13 @@ it "still fires on a non-formation, non-termination normal form" $ do substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (dataizeRule "norm")) rctx null substs `shouldBe` False + forM_ + ["delta", "fire"] + ( \name -> + it ("leaves '" ++ name ++ "' off a formation holding both Ξ” and Ξ»") $ do + substs <- matchExpressionWithRule' [substEmpty] (ExFormation [BiDelta (BtOne "01"), BiLambda (Function "Foo")]) (asRule (dataizeRule name)) rctx + substs `shouldBe` [] + ) describe "dataize" $ do let resources = "test-resources/dataization-packs" diff --git a/test/DepsSpec.hs b/test/DepsSpec.hs --- a/test/DepsSpec.hs +++ b/test/DepsSpec.hs @@ -5,13 +5,13 @@ module DepsSpec where -import AST (Binding (BiLambda), Bytes (BtOne), Expression (ExFormation, ExRoot, ExXi), Function (FnSymbol), symbols) +import AST (Argument (ArTau), Attribute (AtLabel), Binding (BiLambda, BiTau), Bytes (BtOne), Expression (ExApplication, ExDispatch, ExFormation, ExRoot, ExXi), Function (FnSymbol), symbols) import Control.Exception (bracket) import Control.Monad (replicateM_, when) import Data.IORef (modifyIORef', newIORef, readIORef) import Data.List (isInfixOf, isPrefixOf) import Data.Time.Clock.POSIX (getPOSIXTime) -import Deps (Evaluation (EvFiring, EvFormation, EvJoined, EvMinted, EvRun, EvTerm), Judgment (Morphing), Nesting (..), Protocol (..), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, renumbered, saveStep) +import Deps (Evaluation (EvDeferred, EvFiring, EvFormation, EvJoined, EvMinted, EvRun, EvTerm), Judgment (Morphing), Nesting (..), Protocol (..), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, renumbered, saveStep) import Fixtures (readUtf8) import GHC.Clock (getMonotonicTime) import Logger (LogLevel (DEBUG, ERROR, INFO), setLogConfig) @@ -115,6 +115,14 @@ it "does not change the depth a record stands at" $ case renumbered 0 9 (EvJoined 7 1 (2, 3)) of EvJoined depth fresh pair -> (depth, fresh, pair) `shouldBe` (7, 10, (11, 12)) + _ -> expectationFailure "The record did not stay the record it was" + it "raises the symbol a deferred copy stands for and the symbols it carries above the floor" $ + case renumbered 2 5 (EvDeferred 3 4 Morphing (ExFormation [BiTau (AtLabel "x") (ExFormation [BiLambda (FnSymbol 1)]), BiTau (AtLabel "y") (ExFormation [BiLambda (FnSymbol 3)])]) Nothing ExXi) of + EvDeferred _ fresh _ copy _ _ -> (fresh, symbols copy) `shouldBe` (9, [1, 8]) + _ -> expectationFailure "The record did not stay the record it was" + it "raises the symbols the call a deferred copy stands for carries above the floor" $ + case renumbered 2 5 (EvDeferred 3 4 Morphing (ExFormation []) (Just (ExApplication (ExDispatch ExRoot (AtLabel "box")) (ArTau (AtLabel "x") (ExFormation [BiLambda (FnSymbol 7)])))) ExXi) of + EvDeferred _ _ _ _ call _ -> fmap symbols call `shouldBe` Just [12] _ -> expectationFailure "The record did not stay the record it was" describe "perSecond" $ do diff --git a/test/FilesSpec.hs b/test/FilesSpec.hs --- a/test/FilesSpec.hs +++ b/test/FilesSpec.hs @@ -14,10 +14,12 @@ import System.Directory ( createDirectoryIfMissing , createDirectoryLink + , createFileLink , executable , getPermissions , getTemporaryDirectory , listDirectory + , pathIsSymbolicLink , removeDirectoryRecursive , setOwnerExecutable , setPermissions @@ -66,6 +68,17 @@ BS.writeFile (dir "lonely.phi") BS.empty void (try (overwrite (dir "lonely.phi") (replicate 100000 'Ο‰' ++ error "broken tail")) :: IO (Either ErrorCall ())) listDirectory dir `shouldReturn` ["lonely.phi"] + it "writes through a symbolic link and keeps the link" $ withScratchDir $ \dir -> do + let real = dir "real.phi" + link = dir "link.phi" + BS.writeFile real (TE.encodeUtf8 (T.pack "{⟦ old ↦ βˆ… ⟧}")) + if os == "mingw32" + then pendingWith "Windows does not create file symbolic links without elevated privileges" + else do + createFileLink real link + overwrite link "{⟦ new ↦ βˆ… ⟧}" + TE.decodeUtf8 <$> BS.readFile real `shouldReturn` T.pack "{⟦ new ↦ βˆ… ⟧}" + pathIsSymbolicLink link `shouldReturn` True it "keeps the executable permission of the replaced file" $ withScratchDir $ \dir -> do let path = dir "script.sh" BS.writeFile path BS.empty diff --git a/test/FunctionsSpec.hs b/test/FunctionsSpec.hs --- a/test/FunctionsSpec.hs +++ b/test/FunctionsSpec.hs @@ -80,6 +80,12 @@ it "extracts bytes from a data-object expression" $ do term <- buildTerm "dataize" [ArgExpression (DataNumber (numToBts 5))] substEmpty expectBytes term (numToBts 5) + it "extracts bytes from a bare formation of data" $ do + term <- buildTerm "dataize" [ArgExpression (ExFormation [BiDelta (numToBts 1)])] substEmpty + expectBytes term (numToBts 1) + it "extracts bytes from an application of Ξ¦.bytes" $ do + term <- buildTerm "dataize" [ArgExpression (ExApplication (ExDispatch ExRoot (AtLabel "bytes")) (ArTau AtPhi (ExFormation [BiDelta (numToBts 1)])))] substEmpty + expectBytes term (numToBts 1) describe "size" $ it "counts the bindings bound to a meta" $ do @@ -106,10 +112,22 @@ , \term -> expectExpression term (DataString (strToBts "foobar")) ) , + ( "concat joins the bytes of a number that is not UTF-8" + , "concat" + , [ArgExpression (DataString (strToBts "a")), ArgExpression (DataNumber (numToBts 0.5))] + , \term -> expectExpression term (DataString (BtMany ["61", "3F", "E0", "00", "00", "00", "00", "00", "00"])) + ) + , ( "sed replaces every occurrence with the 'g' flag" , "sed" , [ArgExpression (DataString (strToBts "hello")), ArgExpression (DataString (strToBts "s/l/L/g"))] , \term -> expectExpression term (DataString (strToBts "heLLo")) + ) + , + ( "sed keeps every character above U+00FF" + , "sed" + , [ArgExpression (DataString (strToBts "a Ρ„ πœ‘")), ArgExpression (DataString (strToBts "s/a/b/g"))] + , \term -> expectExpression term (DataString (strToBts "b Ρ„ πœ‘")) ) , ( "sed replaces only the first occurrence without the 'g' flag" diff --git a/test/LaTeXSpec.hs b/test/LaTeXSpec.hs --- a/test/LaTeXSpec.hs +++ b/test/LaTeXSpec.hs @@ -121,6 +121,7 @@ , ("empty (Or [])", Y.Or [], "{ }") , ("normal form", Y.NF (ExMeta "n"), "{ \\isnormal{ n } }") , ("matches", Y.Matches "abc" (ExMeta "n"), "{ matches\\lparen abc, n \\rparen }") + , ("matches with a regex LaTeX would read", Y.Matches "^a_b$" (ExMeta "n"), "{ matches\\lparen \\char94{}a\\char95{}b\\char36{}, n \\rparen }") , ("part-of", Y.PartOf (ExMeta "n") (BiVoid AtRho), "{ part-of\\lparen n, \\phiTerminal{\\rho} -> ? \\rparen }") , ("compare equal", Y.Eq (Y.CmpAttr AtRho) (Y.CmpAttr AtPhi), "{ \\phiTerminal{\\rho} = @ }") , ("compare greater", Y.Gt (Y.CmpNum (Y.Literal 3)) (Y.CmpNum (Y.Literal 4)), "{ 3 > 4 }") @@ -241,6 +242,11 @@ , " \\phiDataize |07-| : D{.}" , "\\end{phiquation}" ] + + it "renders a 'where' function with a hyphen as a valid macro" $ do + ptn <- parseExpressionThrows "Q.x" + explainRules [Y.Rule "rt" Nothing Nothing ptn ptn Nothing (Just [Y.Extra (Y.ArgAttribute (AtMeta "t1")) "random-tau" []]) Nothing] + `shouldContain` "\\randomTau{" it "prefixes each step with a '% === Step' header when '_headers' is set" $ do step1 <- parseExpressionThrows "[[ x -> Q.y ]]" diff --git a/test/LambdasSpec.hs b/test/LambdasSpec.hs --- a/test/LambdasSpec.hs +++ b/test/LambdasSpec.hs @@ -59,6 +59,10 @@ known <- lambdasOf (entry "L_number_plus") answering known "L_number_plus_twice" `shouldBe` Nothing + it "reads a single key that no other key is compared with, even an anchored one" $ do + known <- lambdasOf (entry "^L_a$") + answering known "L_a" `shouldBe` Just "^L_a$" + it "cannot read a Ξ» function no entry answers" $ do known <- lambdasOf (entry "L_number_plus") answering known "L_bytes_not" `shouldBe` Nothing @@ -67,6 +71,14 @@ known <- lambdasOf "- Ξ»: L_pair\n dataize:\n 𝛿2: $.x\n 𝛿1: $.ρ\n 𝑛: ⟦ Ξ» ‍ 𝜎 ⟧\n" map (_spelling . fst) (maybe [] _dataized (matched known "L_pair")) `shouldBe` ["𝛿1", "𝛿2"] + it "reads the operands of 'dataize' in numeric order past nine" $ do + known <- lambdasOf "- Ξ»: L_pair\n dataize:\n 𝛿10: $.b\n 𝛿9: $.a\n 𝛿1: $.ρ\n 𝑛: ⟦ Ξ» ‍ 𝜎 ⟧\n" + map (_spelling . fst) (maybe [] _dataized (matched known "L_pair")) `shouldBe` ["𝛿1", "𝛿9", "𝛿10"] + + it "reads a 'symbolize' line that stands the term of line nine as line ten" $ do + known <- lambdasOf "- Ξ»: L_pair\n morph:\n 𝑛1: $.x\n symbolize:\n 𝑛9: 𝑛1\n 𝑛10: 𝑛9\n 𝑛: 𝑛10\n" + map (_spelling . fst) (maybe [] _symbolized (matched known "L_pair")) `shouldBe` ["𝑛9", "𝑛10"] + it "reads a meta under both the name it is spelled with and the name it binds" $ do known <- lambdasOf "- Ξ»: L_pair\n dataize:\n 𝛿1: $.ρ\n 𝑛: ⟦ Ξ» ‍ 𝜎 ⟧\n" map (_name . fst) (maybe [] _dataized (matched known "L_pair")) `shouldBe` ["d1"] @@ -141,7 +153,7 @@ , entry "L_[a-z]+_plus" <> entry "L_number_[a-z]+" , "such as 'L_number_plus'" ) - , ("a key with a back reference phino cannot compare", entry "L_(a)\\1", "cannot be compared") + , ("a key with a back reference phino cannot compare", entry "L_(a)\\1" <> entry "L_b", "cannot be compared") , ("a key which is no regular expression", entry "L_[pair", "is not a regular expression") , ("an operand of 'dataize' which is no bytes meta", "- Ξ»: L_pair\n dataize:\n 𝑛1: $.x\n 𝑛: ⟦ Ξ» ‍ 𝜎 ⟧\n", "is not a bytes meta") , ("an operand of 'morph' which is no expression meta", "- Ξ»: L_pair\n morph:\n 𝛿1: $.x\n 𝑛: ⟦ Ξ» ‍ 𝜎 ⟧\n", "is not an expression meta") @@ -151,6 +163,8 @@ , ("an operand of 'symbolize' standing the term of a line below it", "- Ξ»: L_pair\n morph:\n 𝑛1: $.x\n symbolize:\n 𝑛2: 𝑛3\n 𝑛3: 𝑛1\n 𝑛: 𝑛2\n", "names no meta") , ("an operand referencing a meta the entry never matched", "- Ξ»: L_pair\n dataize:\n 𝛿1: '!n'\n 𝑛: ⟦ Ξ» ‍ 𝜎 ⟧\n", "cannot be referenced") , ("an answer reading the data its operands came down to", "- Ξ»: L_pair\n dataize:\n 𝛿1: $.ρ\n 𝑛: ⟦ Ξ” ‍ 𝛿1 ⟧\n", "reads data") + , ("a meta bound by 'morph' and again by 'symbolize'", "- Ξ»: L_pair\n morph:\n 𝑛1: $.x\n symbolize:\n 𝑛1: 𝑛1\n 𝑛: 𝑛1\n", "The meta '𝑛1' of Ξ» function 'L_pair' is bound by more than one line") + , ("an answer writing a numbered symbol", "- Ξ»: L_pair\n 𝑛: '⟦ a ↦ ⟦ Ξ» ‍ 𝜎1 ⟧, b ↦ ⟦ Ξ» ‍ 𝜎 ⟧ ⟧'\n", "writes the numbered symbol '𝜎1'") , ("an answer carrying an anonymous meta of another kind", "- Ξ»: L_pair\n 𝑛: '⟦ Ο† ↦ !n ⟧'\n", "cannot be referenced") , ("a 'join' line joining one meta alone", "- Ξ»: L_fork\n morph:\n 𝑛1: $.then\n join:\n 𝑛2: [𝑛1]\n 𝑛: 𝑛2\n", "must join exactly two metas") , ("a 'join' line joining three metas", "- Ξ»: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n 𝑛3: $.c\n join:\n 𝑛4: [𝑛1, 𝑛2, 𝑛3]\n 𝑛: 𝑛4\n", "must join exactly two metas") @@ -168,6 +182,9 @@ , ("a rule of 'rewrite' writing a symbol nobody minted", rewriting " 𝑛2:\n of: 𝑛1\n rules:\n - name: naming\n pattern: ⟦ Ο† ↦ 𝑒1 ⟧\n result: ⟦ Ξ» ‍ 𝜎1 ⟧\n 𝑛: 𝑛2\n", "writes a symbol 𝜎 into its result") , ("a rule of 'rewrite' reading a meta it never binds", rewriting " 𝑛2:\n of: 𝑛1\n rules:\n - name: unbound\n pattern: ⟦ Ο† ↦ 𝑒1 ⟧\n result: ⟦ Ο† ↦ 𝑒2 ⟧\n 𝑛: 𝑛2\n", "reads the meta 'e2' it never binds") , ("a rule of 'rewrite' with no result", rewriting " 𝑛2:\n of: 𝑛1\n rules:\n - name: empty\n pattern: ⟦ Ο† ↦ 𝑒1 ⟧\n 𝑛: 𝑛2\n", "cannot be read") + , ("an answer naming a meta no block binds", "- Ξ»: L_pair\n dataize:\n 𝛿1: $.ρ\n 𝑛: 𝑛7\n", "reads the meta 'n7' that no block binds") + , ("an operand of 'dataize' reading a meta", "- Ξ»: L_pair\n dataize:\n 𝛿1: 𝑛5\n 𝑛: ⟦ Ξ» ‍ 𝜎 ⟧\n", "of 'dataize' of Ξ» function 'L_pair' reads the meta 'n5'") + , ("an operand of 'morph' reading a meta", "- Ξ»: L_pair\n morph:\n 𝑛1: $.x.𝜏1\n 𝑛: 𝑛1\n", "of 'morph' of Ξ» function 'L_pair' reads the meta 't1'") , ("a 'symbolize' line standing what a 'join' line made", "- Ξ»: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n symbolize:\n 𝑛5: 𝑛3\n join:\n 𝑛3: [𝑛1, 𝑛2]\n 𝑛: 𝑛5\n", "names no meta bound by 'morph' or by a line above it") ] ( \(desc, text, message) -> @@ -302,6 +319,21 @@ made <- joining "⟦ Ο† ↦ ⟦ Ξ» ‍ 𝜎1 ⟧, ρ ↦ ⟦ x ↦ ⟦ Ξ” ‍ 00- ⟧ ⟧ ⟧" "⟦ Ο† ↦ ⟦ Ξ» ‍ 𝜎2 ⟧, ρ ↦ ⟦ y ↦ ⟦ Ξ” ‍ FF- ⟧ ⟧ ⟧" 4 made `shouldBe` Just (term, [(5, (1, 2))], 5) + it "joins a bare symbol with the symbol the Ο† chain of a formation ends in" $ do + term <- parseExpressionThrows "⟦ Ξ» ‍ 𝜎5 ⟧" + made <- joining "⟦ Ο† ↦ ⟦ Ο† ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ⟧, eq ↦ ⟦ b ↦ βˆ… ⟧ ⟧" "⟦ Ξ» ‍ 𝜎2 ⟧" 4 + made `shouldBe` Just (term, [(5, (1, 2))], 5) + + it "joins a formation with a bare symbol standing first" $ do + term <- parseExpressionThrows "⟦ Ξ» ‍ 𝜎8 ⟧" + made <- joining "⟦ Ξ» ‍ 𝜎3 ⟧" "⟦ Ο† ↦ ⟦ Ξ» ‍ 𝜎6 ⟧, neg ↦ ⟦⟧ ⟧" 7 + made `shouldBe` Just (term, [(8, (3, 6))], 8) + + it "mints nothing for a bare symbol the Ο† chain of a formation ends in" $ do + term <- parseExpressionThrows "⟦ Ξ» ‍ 𝜎2 ⟧" + made <- joining "⟦ Ο† ↦ ⟦ Ξ» ‍ 𝜎2 ⟧, m ↦ ⟦⟧ ⟧" "⟦ Ξ» ‍ 𝜎2 ⟧" 4 + made `shouldBe` Just (term, [], 4) + it "joins two branches differing in their ρ alone" $ do term <- parseExpressionThrows "⟦ Ο† ↦ ⟦ Ξ» ‍ 𝜎1 ⟧, ρ ↦ ⟦ x ↦ ⟦ Ξ” ‍ 00- ⟧ ⟧ ⟧" made <- joining "⟦ Ο† ↦ ⟦ Ξ» ‍ 𝜎1 ⟧, ρ ↦ ⟦ x ↦ ⟦ Ξ” ‍ 00- ⟧ ⟧ ⟧" "⟦ Ο† ↦ ⟦ Ξ» ‍ 𝜎1 ⟧, ρ ↦ ⟦ y ↦ ⟦ Ξ” ‍ FF- ⟧ ⟧ ⟧" 4 @@ -314,6 +346,9 @@ , ("two branches one of which carries a binding more", "⟦ Ο† ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ⟧", "⟦ Ο† ↦ ⟦ Ξ» ‍ 𝜎2 ⟧, x ↦ ⟦⟧ ⟧") , ("two branches binding their symbols under different attributes", "⟦ a ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ⟧", "⟦ b ↦ ⟦ Ξ» ‍ 𝜎2 ⟧ ⟧") , ("two branches of different forma", "Ξ¦.number( Ο† ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ )", "Ξ¦.bool( Ο† ↦ ⟦ Ξ» ‍ 𝜎2 ⟧ )") + , ("a bare symbol with a formation whose Ο† chain ends in a datum", "⟦ Ξ» ‍ 𝜎1 ⟧", "⟦ Ο† ↦ ⟦ Ξ” ‍ 00- ⟧, x ↦ ⟦⟧ ⟧") + , ("a bare symbol with a formation carrying no Ο†", "⟦ a ↦ ⟦ Ξ» ‍ 𝜎2 ⟧ ⟧", "⟦ Ξ» ‍ 𝜎1 ⟧") + , ("a bare symbol with an application", "⟦ Ξ» ‍ 𝜎1 ⟧", "Ξ¦.number( Ο† ↦ ⟦ Ξ» ‍ 𝜎2 ⟧ )") ] ( \(desc, left, right) -> it ("cannot join " ++ desc) $ do diff --git a/test/LanguageSpec.hs b/test/LanguageSpec.hs --- a/test/LanguageSpec.hs +++ b/test/LanguageSpec.hs @@ -33,6 +33,8 @@ , ("L_a{,2}", "L_a\\{,2}", Just "L_a{,2}") , ("", "x?", Just "") , ("L_Γ©+", "L_[^a-z]", Just "L_Γ©") + , ("L_[\\d-z]", "L_A", Nothing) + , ("L_[\\d-z]", "L_-", Just "L_-") ] ( \(first, second, answer) -> it ("tells what '" <> show first <> "' and '" <> show second <> "' both match") $ diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs --- a/test/ParserSpec.hs +++ b/test/ParserSpec.hs @@ -10,7 +10,7 @@ import AST import Control.Exception (SomeException, displayException, try) import Control.Monad (forM_) -import Data.Either (isLeft, isRight) +import Data.Either (fromLeft, isLeft, isRight) import Data.List (isInfixOf) import Files (allPathsIn) import Parser @@ -408,6 +408,10 @@ , ("123", Nothing) , ("", Nothing) ] + + it "points at the binding that repeats an attribute, not past the formation" $ + fromLeft "" (parseExpression "⟦\n a ↦ ΞΎ,\n b ↦ ΞΎ,\n b ↦ Ξ¦\n⟧\n\n\n") + `shouldSatisfy` isInfixOf "expression:4:3:" describe "parse number" $ test diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs --- a/test/PrinterSpec.hs +++ b/test/PrinterSpec.hs @@ -15,7 +15,7 @@ import Parser (parseExpression) import Printer import Sugar (SugarType (..)) -import Test.Hspec (Spec, describe, it, shouldBe, shouldContain, shouldNotContain) +import Test.Hspec (Spec, describe, expectationFailure, it, shouldBe, shouldContain, shouldNotContain, shouldSatisfy) import Yaml (ExtraArgument (..)) spec :: Spec @@ -67,6 +67,17 @@ parseExpression (printExpression' expr (SWEET, ASCII, SINGLELINE, defaultMargin)) `shouldBe` Right expr ) + describe "printExpression writes data with meta bytes in full instead of crashing" $ + forM_ + [ ("a number, sweet", DataNumber (BtMeta "d1"), SWEET) + , ("a number, salty", DataNumber (BtMeta "d1"), SALTY) + , ("a string, sweet", DataString (BtMeta "d1"), SWEET) + , ("a string, salty", DataString (BtMeta "d1"), SALTY) + ] + ( \(desc, expr, sugar) -> + it desc (printExpression' expr (sugar, UNICODE, SINGLELINE, defaultMargin) `shouldContain` "𝛿1") + ) + describe "printExpression with SWEET UNICODE renders the pretty function meta" $ it "meta lambda becomes 𝑓" $ printExpression' (ExFormation [BiLambda (FnMeta "F")]) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "𝑓:Ξ»" @@ -160,6 +171,11 @@ (SALTY, UNICODE, SINGLELINE, defaultMargin) number `shouldNotContain` "as-bytes" str `shouldNotContain` "as-bytes" + + it "keeps every line of a deep formation within --margin, counting indentation in columns" $ + case parseExpression "⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ⟦ d ↦ ⟦ e ↦ ⟦ x ↦ ΞΎ.yyyyyyyy, z ↦ ΞΎ.w ⟧ ⟧ ⟧ ⟧ ⟧ ⟧" of + Right deep -> maximum (map length (lines (printExpression' deep (SALTY, UNICODE, MULTILINE, 36)))) `shouldSatisfy` (<= 36) + Left err -> expectationFailure err describe "printExpression keeps a compressed meet atomic under a narrow margin" $ it "renders the meet body on a single line even when the margin wraps its parent" $ do diff --git a/test/XMIRSpec.hs b/test/XMIRSpec.hs --- a/test/XMIRSpec.hs +++ b/test/XMIRSpec.hs @@ -16,6 +16,7 @@ import Data.List (intercalate) import Data.Map qualified as M import Data.Text qualified as T +import Data.Time.Clock.POSIX (posixSecondsToUTCTime) import Data.Yaml qualified as Yaml import Files (allPathsIn) import GHC.Generics (Generic) @@ -25,7 +26,7 @@ import Test.Hspec (Spec, anyException, describe, expectationFailure, it, runIO, shouldBe, shouldContain, shouldNotContain, shouldReturn, shouldThrow) import Text.XML (Document (..), Element (..), Node (NodeElement), Prologue (..)) import Text.XML.Cursor qualified as C -import XMIR (XmirContext (XmirContext), defaultXmirContext, escapeXML, expressionToXMIR, parseXMIRThrows, printXMIR, toName, xmirAtoms, xmirToPhi) +import XMIR (XmirContext (XmirContext), defaultXmirContext, escapeXML, expressionToXMIR, parseXMIRThrows, printXMIR, toName, xmirAtoms, xmirTime, xmirToPhi) data ParsePack = ParsePack { failure :: Maybe Bool @@ -205,6 +206,8 @@ [ "[[ x -> ? ]]" , "[[ ^ -> 5 ]]" , "[[ x -> 4, L> L_number_plus, ^ -> [[ y -> 5 ]] ]]" + , "[[ a -> T ]]" + , "[[ a -> $ ]]" ] ( \phi' -> it phi' $ do expr <- parseExpressionThrows phi' @@ -214,11 +217,14 @@ back `shouldBe` expr ) - describe "derived Ξ» function name" $ + describe "derived Ξ» function name" $ do it "spells itself in the alphabet the parser accepts" $ do doc <- parseXMIRThrows "" expr <- xmirToPhi doc parseExpressionThrows (printExpression expr) `shouldReturn` expr + it "stays unique when two paths spell alike, and keeps the type of each atom" $ do + doc <- parseXMIRThrows "" + xmirAtoms doc `shouldReturn` M.fromList [("L_top_as_int", "Ξ¦.number"), ("L_top_as_int_2", "Ξ¦.string")] describe "atom result types in XMIR" $ do let atom :: String @@ -244,13 +250,17 @@ ) `shouldReturn` M.fromList [("Foo", "?")] - describe "--hide-rho in XMIR" $ + describe "--hide-rho in XMIR" $ do it "drops every bound ρ from the printed document" $ do expr <- parseExpressionThrows "[[ x -> 4, ^ -> [[ y -> 5 ]] ]]" doc <- expressionToXMIR expr (XmirContext True False True (const "") M.empty) let printed = printXMIR doc printed `shouldContain` "name=\"x\"" printed `shouldNotContain` "name=\"ρ\"" + it "drops an application argument bound to ρ instead of refusing it" $ do + expr <- parseExpressionThrows "[[ m -> Q.a(^ -> [[]]) ]]" + doc <- expressionToXMIR expr (XmirContext True False True (const "") M.empty) + printXMIR doc `shouldContain` "base=\"Ξ¦.a\"" describe "prohibit to convert to XMIR" $ forM_ @@ -260,7 +270,6 @@ , "\"Hello\"" , "Q" , "$" - , "[[ x -> T ]]" , "[[ x -> [[ !t1 -> 5 ]] ]]" , "[[ org -> [[ z -> ?, L> Package ]] ]]" ] @@ -308,7 +317,7 @@ [ ( "explains an unsupported top-level expression" , do - expr <- parseExpressionThrows "[[ x -> $ ]]" + expr <- parseExpressionThrows "[[ x -> !e1 ]]" try (void (expressionToXMIR expr defaultXmirContext)) :: IO (Either SomeException ()) , ["XMIR does not support such top-level expression"] ) @@ -327,6 +336,13 @@ , ["XMIR does not support such expression", "ρ ↦"] ) , + ( "refuses an application of a formation, which XMIR has no shape for" + , do + expr <- parseExpressionThrows "[[ x -> [[ a -> ? ]](a -> Q.y) ]]" + try (void (expressionToXMIR expr defaultXmirContext)) :: IO (Either SomeException ()) + , ["XMIR does not support such expression", "a ↦ Ξ¦.y"] + ) + , ( "explains an unsupported binding" , try (void (expressionToXMIR (ExFormation [BiTau (AtLabel "x") (ExFormation [BiMeta "n", BiVoid AtRho]), BiVoid AtRho]) defaultXmirContext)) :: IO (Either SomeException ()) @@ -351,6 +367,12 @@ Left err -> mapM_ (displayException err `shouldContain`) messages Right () -> expectationFailure "expected an exception" ) + + describe "xmirTime" $ do + it "keeps every nanosecond of the time" $ + xmirTime (posixSecondsToUTCTime 1790000000.123456789) `shouldBe` "2026-09-21T14:13:20.123456789Z" + it "never carries the fraction past nine digits" $ + xmirTime (posixSecondsToUTCTime 1790000000.99999995) `shouldBe` "2026-09-21T14:13:20.999999950Z" describe "escapeXML" $ it "escapes an apostrophe alongside the other reserved characters" $ diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs --- a/test/YamlSpec.hs +++ b/test/YamlSpec.hs @@ -74,6 +74,18 @@ it ("rejects " ++ desc) (unless valid (expectationFailure ("expected rejection for: " ++ yaml))) ) + it "rejects a condition literal that does not fit into Int" $ + (decodeYaml' "name: big\npattern: '⟦ 𝐡1 ⟧'\nresult: '⟦ 𝐡1 ⟧'\nwhen:\n eq: [{length: '𝐡1'}, 18446744073709551617]" :: Either Yaml.ParseException Rule) + `shouldSatisfy` failsWith "does not fit into Int" + + it "rejects a 'where' step that binds a meta the pattern already binds" $ + (decodeYaml' "name: again\npattern: '⟦ x ↦ 𝑒1 ⟧'\nresult: '⟦ x ↦ 𝑒1 ⟧'\nwhere:\n - meta: '𝑒1'\n function: concat\n args: ['\"a\"']" :: Either Yaml.ParseException Rule) + `shouldSatisfy` failsWith "binds the meta 'e1' again" + + it "rejects a 'where' step whose meta is not a meta" $ + (decodeYaml' "name: nometa\npattern: '⟦ x ↦ 𝑒1 ⟧'\nresult: '⟦ x ↦ 𝑒1 ⟧'\nwhere:\n - meta: 'z'\n function: concat\n args: ['\"a\"']" :: Either Yaml.ParseException Rule) + `shouldSatisfy` failsWith "whose 'meta' is not a meta" + it "rejects an 'e-match' in a rewriting rule" $ (decodeYaml' "name: kvz\npattern: '⟦ 𝜏1 ↦ 𝑒1 ⟧'\ne-match: '𝑒2'\nresult: '𝑒2'" :: Either Yaml.ParseException Rule) `shouldSatisfy` failsWith "The rule 'kvz' carries an 'e-match'"