phino-0.0.144: compiled/generated/Compiled.hs
-- The built-in rules of phino, and the rules of '--rule' it was given, as
-- Haskell: this module is written by 'phino compile' and a build with the
-- flag 'compiled' links it in (#1617). The next 'phino compile' writes it
-- anew, so a change belongs to the rules of YAML and not to it.
module Compiled (compiled) where
import AST
import qualified Builder as B
import qualified Contextualize as C
import qualified Deps as D
import qualified Control.Exception as E
import qualified Engine as En
import qualified Inference as In
import qualified Matcher as M
import qualified Data.Map.Strict as Map
import qualified Rewriter as R
import qualified Rule as Ru
compiled :: Maybe En.Engine
compiled =
Just
En.Engine
{ En._normalization = normalization
, En._rules = steps
, En._normal = nf
, En._contextualize = \term context -> either E.throwIO pure (contextualize term context)
, En._morphing = morphings
, En._dataization = dataizations
, En._sources = sources
}
-- The steps of the built-in rules of normalization, in the order of the rules.
normalization :: [Ru.Step]
normalization = [stepAlpha, stepAmiss, stepCopy, stepDc, stepDca, stepDd, stepDl, stepDot, stepMiss, stepNull, stepOver, stepOvera, stepSkip, stepStay, stepStop]
-- The steps of every rule compiled, by the text of the rule.
steps :: Map.Map String Ru.Step
steps =
Map.fromList [("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}", stepAlpha), ("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}", stepAmiss), ("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}", stepCopy), ("Rule {name = \"dc\", label = Nothing, description = Nothing, pattern = ExApplication ExTermination (ArTau !t (ExAny (Slot \"e\" 6))), result = ExTermination, when = Nothing, where_ = Nothing, having = Nothing}", stepDc), ("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}", stepDca), ("Rule {name = \"dd\", label = Nothing, description = Nothing, pattern = ExDispatch ExTermination !t, result = ExTermination, when = Nothing, where_ = Nothing, having = Nothing}", stepDd), ("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}", stepDl), ("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}", stepDot), ("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}", stepMiss), ("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}", stepNull), ("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}", stepOver), ("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}", stepOvera), ("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}", stepSkip), ("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}", stepStay), ("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}", stepStop)]
-- The rules of 𝕄, in the order of their files.
morphings :: [In.Inference Expression]
morphings = [In.direct morphingDead, In.direct morphingMa, In.direct morphingMaa, In.direct morphingMaad, In.direct morphingMad, In.direct morphingMd, In.direct morphingMf, In.direct morphingMg, In.direct morphingMl, In.direct morphingMphi, In.direct morphingUniverse, In.direct morphingXi]
-- The rules of 𝔻, in the order of their files.
dataizations :: [In.Inference Bytes]
dataizations = [In.direct dataizationBox, In.direct dataizationDelta, In.direct dataizationFire, In.direct dataizationNone, In.direct dataizationNorm]
-- 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\")}]}"]
-- Whether the term is a normal form: no built-in rule of normalization
-- matches anywhere inside it.
nf :: Expression -> Bool
nf =
Ru.normalWith
( \term ->
M.anywhere True (not . null . rewriteAlpha Nothing) term
|| M.anywhere True (not . null . rewriteAmiss Nothing) term
|| M.anywhere True (not . null . rewriteCopy Nothing) term
|| M.anywhere True (not . null . rewriteDc Nothing) term
|| M.anywhere True (not . null . rewriteDca Nothing) term
|| M.anywhere True (not . null . rewriteDd Nothing) term
|| M.anywhere True (not . null . rewriteDl Nothing) term
|| M.anywhere True (not . null . rewriteDot Nothing) term
|| M.anywhere True (not . null . rewriteMiss Nothing) term
|| M.anywhere True (not . null . rewriteNull Nothing) term
|| M.anywhere True (not . null . rewriteOver Nothing) term
|| M.anywhere True (not . null . rewriteOvera Nothing) term
|| M.anywhere True (not . null . rewriteSkip Nothing) term
|| M.anywhere True (not . null . rewriteStay Nothing) term
|| M.anywhere True (not . null . rewriteStop Nothing) term
)
-- The Contextualization function 𝒞, the conclusion of the one rule matching
-- the term and the context.
contextualize :: Expression -> Expression -> Either C.ContextualizeException Expression
contextualize term context =
C.concluded
term
( concat
[ contextualizeCa term context
, contextualizeCaa term context
, contextualizeCd term context
, contextualizeCf term context
, contextualizeCg term context
, contextualizeCt term context
, contextualizeCxi term context
]
)
-- The rule 'alpha'.
stepAlpha :: Ru.Step
stepAlpha = R.direct "alpha" True rewriteAlpha
rewriteAlpha :: Maybe Expression -> Expression -> [Expression]
rewriteAlpha _ term =
[ ExApplication (B.formed (concat [x5, [BiVoid x9], x8])) (ArTau x9 x3)
| ExApplication x1 (ArAlpha x2 x3) <- [term]
, ExFormation x4 <- [x1]
, (x5, x6) <- M.splits x4
, (x7 : x8) <- [x6]
, BiVoid x9 <- [x7]
, Alpha x10 <- [x2]
, (x10 == (Ru.domainOf x5) && not (x9 == AtRho))
]
-- The rule 'amiss'.
stepAmiss :: Ru.Step
stepAmiss = R.direct "amiss" True rewriteAmiss
rewriteAmiss :: Maybe Expression -> Expression -> [Expression]
rewriteAmiss _ term =
[ ExTermination
| ExApplication x1 (ArAlpha x2 _) <- [term]
, ExFormation x4 <- [x1]
, Alpha x5 <- [x2]
, not ((Ru.domainOf x4) > x5)
]
-- The rule 'copy'.
stepCopy :: Ru.Step
stepCopy = R.direct "copy" True rewriteCopy
rewriteCopy :: Maybe Expression -> Expression -> [Expression]
rewriteCopy _ term =
[ B.formed (concat [x5, [BiTau x2 x3], x8])
| ExApplication x1 (ArTau x2 x3) <- [term]
, ExFormation x4 <- [x1]
, (x5, x6) <- M.splits x4
, (x7 : x8) <- [x6]
, BiVoid x9 <- [x7]
, x2 == x9
, Ru.xiFree x3
, Ru.normalHeld nf x3
]
-- The rule 'dc'.
stepDc :: Ru.Step
stepDc = R.direct "dc" True rewriteDc
rewriteDc :: Maybe Expression -> Expression -> [Expression]
rewriteDc _ term =
[ ExTermination
| ExApplication x1 (ArTau _ _) <- [term]
, ExTermination <- [x1]
]
-- The rule 'dca'.
stepDca :: Ru.Step
stepDca = R.direct "dca" True rewriteDca
rewriteDca :: Maybe Expression -> Expression -> [Expression]
rewriteDca _ term =
[ ExTermination
| ExApplication x1 (ArAlpha x2 _) <- [term]
, ExTermination <- [x1]
, Alpha _ <- [x2]
]
-- The rule 'dd'.
stepDd :: Ru.Step
stepDd = R.direct "dd" True rewriteDd
rewriteDd :: Maybe Expression -> Expression -> [Expression]
rewriteDd _ term =
[ ExTermination
| ExDispatch x1 _ <- [term]
, ExTermination <- [x1]
]
-- The rule 'dl'.
stepDl :: Ru.Step
stepDl = R.direct "dl" True rewriteDl
rewriteDl :: Maybe Expression -> Expression -> [Expression]
rewriteDl _ term =
[ ExTermination
| ExFormation x1 <- [term]
, (x2, x3) <- M.splits x1
, (x4 : x5) <- [x3]
, BiLambda x6 <- [x4]
, M.named x6
, all (`Ru.presentIn` concat [x2, x5]) [AtDelta]
]
-- The rule 'dot'.
stepDot :: Ru.Step
stepDot = R.direct "dot" True rewriteDot
rewriteDot :: Maybe Expression -> Expression -> [Expression]
rewriteDot universe term =
[ ExApplication e1 (ArTau AtRho e2)
| ExDispatch x1 x2 <- [term]
, ExFormation x3 <- [x1]
, (x4, x5) <- M.splits x3
, (x6 : x7) <- [x5]
, BiTau x8 x9 <- [x6]
, x2 == x8
, not (all (`Ru.presentIn` concat [x4, x7]) [AtDelta, AtLambda])
, Ru.normalHeld nf x9
, let e1 = either E.throw id (contextualize x9 (B.formed (concat [x4, x7])))
, let e2 = B.nameIn universe (B.formed (concat [x4, [BiTau x2 x9], x7]))
]
-- The rule 'miss'.
stepMiss :: Ru.Step
stepMiss = R.direct "miss" True rewriteMiss
rewriteMiss :: Maybe Expression -> Expression -> [Expression]
rewriteMiss _ term =
[ ExTermination
| ExApplication x1 (ArTau x2 _) <- [term]
, ExFormation x4 <- [x1]
, (not (all (`Ru.presentIn` concat [x4]) [x2]) && not (x2 == AtRho))
]
-- The rule 'null'.
stepNull :: Ru.Step
stepNull = R.direct "null" True rewriteNull
rewriteNull :: Maybe Expression -> Expression -> [Expression]
rewriteNull _ term =
[ ExTermination
| ExDispatch x1 x2 <- [term]
, ExFormation x3 <- [x1]
, (_, x5) <- M.splits x3
, (x6 : _) <- [x5]
, BiVoid x8 <- [x6]
, x2 == x8
]
-- The rule 'over'.
stepOver :: Ru.Step
stepOver = R.direct "over" True rewriteOver
rewriteOver :: Maybe Expression -> Expression -> [Expression]
rewriteOver _ term =
[ ExTermination
| ExApplication x1 (ArTau x2 _) <- [term]
, ExFormation x4 <- [x1]
, (_, x6) <- M.splits x4
, (x7 : _) <- [x6]
, BiTau x9 _ <- [x7]
, x2 == x9
, not (x2 == AtRho)
]
-- The rule 'overa'.
stepOvera :: Ru.Step
stepOvera = R.direct "overa" True rewriteOvera
rewriteOvera :: Maybe Expression -> Expression -> [Expression]
rewriteOvera _ term =
[ ExTermination
| ExApplication x1 (ArAlpha x2 _) <- [term]
, ExFormation x4 <- [x1]
, (x5, x6) <- M.splits x4
, (x7 : _) <- [x6]
, BiTau x9 _ <- [x7]
, Alpha x11 <- [x2]
, (x11 == (Ru.domainOf x5) && not (x9 == AtRho))
]
-- The rule 'skip'.
stepSkip :: Ru.Step
stepSkip = R.direct "skip" True rewriteSkip
rewriteSkip :: Maybe Expression -> Expression -> [Expression]
rewriteSkip _ term =
[ B.formed x4
| ExApplication x1 (ArTau x2 _) <- [term]
, x2 == AtRho
, ExFormation x4 <- [x1]
, not (all (`Ru.presentIn` concat [x4]) [AtRho])
]
-- The rule 'stay'.
stepStay :: Ru.Step
stepStay = R.direct "stay" True rewriteStay
rewriteStay :: Maybe Expression -> Expression -> [Expression]
rewriteStay _ term =
[ B.formed (concat [x5, [BiTau AtRho x10], x8])
| ExApplication x1 (ArTau x2 _) <- [term]
, x2 == AtRho
, ExFormation x4 <- [x1]
, (x5, x6) <- M.splits x4
, (x7 : x8) <- [x6]
, BiTau x9 x10 <- [x7]
, x9 == AtRho
]
-- The rule 'stop'.
stepStop :: Ru.Step
stepStop = R.direct "stop" True rewriteStop
rewriteStop :: Maybe Expression -> Expression -> [Expression]
rewriteStop _ term =
[ ExTermination
| ExDispatch x1 x2 <- [term]
, ExFormation x3 <- [x1]
, not (any (`Ru.presentIn` concat [x3]) [x2, AtPhi, AtLambda])
]
-- The contextualization rule 'ca'.
contextualizeCa :: Expression -> Expression -> [(String, Either C.ContextualizeException Expression)]
contextualizeCa term context =
[ ("ca", do { n2 <- contextualize x1 context; n3 <- contextualize x3 context; pure (ExApplication n2 (ArTau x2 n3)) })
| ExApplication x1 (ArTau x2 x3) <- [term]
]
-- The contextualization rule 'caa'.
contextualizeCaa :: Expression -> Expression -> [(String, Either C.ContextualizeException Expression)]
contextualizeCaa term context =
[ ("caa", do { n2 <- contextualize x1 context; n3 <- contextualize x3 context; pure (ExApplication n2 (ArAlpha (Alpha x4) n3)) })
| ExApplication x1 (ArAlpha x2 x3) <- [term]
, Alpha x4 <- [x2]
]
-- The contextualization rule 'cd'.
contextualizeCd :: Expression -> Expression -> [(String, Either C.ContextualizeException Expression)]
contextualizeCd term context =
[ ("cd", do { n2 <- contextualize x1 context; pure (ExDispatch n2 x2) })
| ExDispatch x1 x2 <- [term]
]
-- The contextualization rule 'cf'.
contextualizeCf :: Expression -> Expression -> [(String, Either C.ContextualizeException Expression)]
contextualizeCf term _ =
[ ("cf", Right (B.formed x1))
| ExFormation x1 <- [term]
]
-- The contextualization rule 'cg'.
contextualizeCg :: Expression -> Expression -> [(String, Either C.ContextualizeException Expression)]
contextualizeCg term _ =
[ ("cg", Right ExRoot)
| ExRoot <- [term]
]
-- The contextualization rule 'ct'.
contextualizeCt :: Expression -> Expression -> [(String, Either C.ContextualizeException Expression)]
contextualizeCt term _ =
[ ("ct", Right ExTermination)
| ExTermination <- [term]
]
-- The contextualization rule 'cxi'.
contextualizeCxi :: Expression -> Expression -> [(String, Either C.ContextualizeException Expression)]
contextualizeCxi term context =
[ ("cxi", Right context)
| ExXi <- [term]
]
-- The morphing rule 'dead'.
morphingDead :: Expression -> Expression -> [In.Premises Expression]
morphingDead term _ =
[ In.Concludes (In.Answered (D.Morphing, "dead") ExTermination)
| ExTermination <- [term]
]
-- The morphing rule 'ma'.
morphingMa :: Expression -> Expression -> [In.Premises Expression]
morphingMa term universe =
[ In.Morphs x1 universe (\n2 -> pure (In.Concludes (In.Onward (In.Normalized (D.Morphing, "ma")) (ExApplication n2 (ArTau x2 x3)) universe)))
| ExApplication x1 (ArTau x2 x3) <- [term]
, Ru.xiFree x3
, Ru.normalHeld nf x1
, Ru.normalHeld nf x3
]
-- The morphing rule 'maa'.
morphingMaa :: Expression -> Expression -> [In.Premises Expression]
morphingMaa term universe =
[ In.Morphs x1 universe (\n2 -> pure (In.Concludes (In.Onward (In.Normalized (D.Morphing, "maa")) (ExApplication n2 (ArAlpha (Alpha x4) x3)) universe)))
| ExApplication x1 (ArAlpha x2 x3) <- [term]
, Alpha x4 <- [x2]
, Ru.xiFree x3
, Ru.normalHeld nf x1
, Ru.normalHeld nf x3
]
-- The morphing rule 'maad'.
morphingMaad :: Expression -> Expression -> [In.Premises Expression]
morphingMaad term universe =
[ In.Concludes (In.Onward (In.Taken (D.Morphing, "maad")) ExTermination universe)
| ExApplication x1 (ArAlpha x2 x3) <- [term]
, Alpha _ <- [x2]
, not (Ru.xiFree x3)
, Ru.normalHeld nf x1
, Ru.normalHeld nf x3
]
-- The morphing rule 'mad'.
morphingMad :: Expression -> Expression -> [In.Premises Expression]
morphingMad term universe =
[ In.Concludes (In.Onward (In.Taken (D.Morphing, "mad")) ExTermination universe)
| ExApplication x1 (ArTau _ x3) <- [term]
, not (Ru.xiFree x3)
, Ru.normalHeld nf x1
, Ru.normalHeld nf x3
]
-- The morphing rule 'md'.
morphingMd :: Expression -> Expression -> [In.Premises Expression]
morphingMd term universe =
[ In.Morphs x1 universe (\n2 -> pure (In.Concludes (In.Onward (In.Normalized (D.Morphing, "md")) (ExDispatch n2 x2) universe)))
| ExDispatch x1 x2 <- [term]
, not (Ru.isFormation x1)
, Ru.normalHeld nf x1
]
-- The morphing rule 'mf'.
morphingMf :: Expression -> Expression -> [In.Premises Expression]
morphingMf term _ =
[ In.Concludes (In.Answered (D.Morphing, "mf") (B.formed x1))
| ExFormation x1 <- [term]
]
-- The morphing rule 'mg'.
morphingMg :: Expression -> Expression -> [In.Premises Expression]
morphingMg term universe =
[ In.Concludes (In.Onward (In.Taken (D.Morphing, "mg")) ExTermination ExRoot)
| ExRoot <- [universe]
, ExRoot <- [term]
]
-- The morphing rule 'ml'.
morphingMl :: Expression -> Expression -> [In.Premises Expression]
morphingMl term universe =
[ In.Evaluates (B.formed (concat [x4, [BiLambda x8], x7])) universe (\n1 -> pure (In.Concludes (In.Onward (In.Normalized (D.Morphing, "ml")) (ExDispatch n1 x2) universe)))
| ExDispatch x1 x2 <- [term]
, ExFormation x3 <- [x1]
, (x4, x5) <- M.splits x3
, (x6 : x7) <- [x5]
, BiLambda x8 <- [x6]
, M.named x8
]
-- The morphing rule 'mphi'.
morphingMphi :: Expression -> Expression -> [In.Premises Expression]
morphingMphi term universe =
[ In.Concludes (In.Onward (In.Normalized (D.Morphing, "mphi")) (ExDispatch (ExDispatch (B.formed x3) AtPhi) x2) universe)
| ExDispatch x1 x2 <- [term]
, ExFormation x3 <- [x1]
, (all (`Ru.presentIn` concat [x3]) [AtPhi] && not (any (`Ru.presentIn` concat [x3]) [x2, AtLambda]))
]
-- The morphing rule 'universe'.
morphingUniverse :: Expression -> Expression -> [In.Premises Expression]
morphingUniverse term universe =
[ In.Concludes (In.Onward (In.Named (D.Morphing, "universe")) universe universe)
| ExRoot <- [term]
, not (universe == ExRoot)
]
-- The morphing rule 'xi'.
morphingXi :: Expression -> Expression -> [In.Premises Expression]
morphingXi term universe =
[ In.Concludes (In.Onward (In.Taken (D.Morphing, "xi")) ExTermination universe)
| ExXi <- [term]
]
-- The dataization rule 'box'.
dataizationBox :: Expression -> Expression -> [In.Premises Bytes]
dataizationBox term universe =
[ In.Contextualizes x7 (B.formed (concat [x2, [BiTau AtPhi x7], x5])) (\e3 -> pure (In.Concludes (In.Onward (In.Normalized (D.Contextualization, "contextualize")) e3 universe)))
| ExFormation x1 <- [term]
, (x2, x3) <- M.splits x1
, (x4 : x5) <- [x3]
, BiTau x6 x7 <- [x4]
, x6 == AtPhi
, not (any (`Ru.presentIn` concat [x2, x5]) [AtDelta, AtLambda])
]
-- The dataization rule 'delta'.
dataizationDelta :: Expression -> Expression -> [In.Premises Bytes]
dataizationDelta term _ =
[ In.Concludes (In.Answered (D.Dataization, "delta") x6)
| ExFormation x1 <- [term]
, (_, x3) <- M.splits x1
, (x4 : _) <- [x3]
, BiDelta x6 <- [x4]
]
-- The dataization rule 'fire'.
dataizationFire :: Expression -> Expression -> [In.Premises Bytes]
dataizationFire term universe =
[ In.Evaluates (B.formed (concat [x2, [BiLambda x6], x5])) universe (\n1 -> pure (In.Concludes (In.Onward (In.Taken (D.Evaluation, "evaluate")) n1 universe)))
| ExFormation x1 <- [term]
, (x2, x3) <- M.splits x1
, (x4 : x5) <- [x3]
, BiLambda x6 <- [x4]
, M.named x6
]
-- The dataization rule 'none'.
dataizationNone :: Expression -> Expression -> [In.Premises Bytes]
dataizationNone term universe =
[ In.Concludes (In.Onward (In.Taken (D.Dataization, "dataize")) ExTermination universe)
| ExFormation x1 <- [term]
, not (any (`Ru.presentIn` concat [x1]) [AtDelta, AtLambda, AtPhi])
]
-- The dataization rule 'norm'.
dataizationNorm :: Expression -> Expression -> [In.Premises Bytes]
dataizationNorm term universe =
[ In.Concludes (In.Onward (In.Staged universe) term universe)
| (not (Ru.isFormation term) && not (term == ExTermination))
, Ru.normalHeld nf term
]