{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}

-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT

module Rule (RuleContext (..), Step (..), domainOf, isFormation, isNF, matchExpressionWithRule, matchExpressionWithRule', meetCondition, normal, normalHeld, normalWith, presentIn, redex, xiFree) where

import AST
import Builder
  ( buildAttribute
  , buildBindingThrows
  , buildBindingUnchecked
  , buildExpression
  , buildExpressionThrows
  )
import Bytes (btsToUnescapedStr)
import Control.Exception (Exception (displayException), throwIO)
import Control.Exception.Base (SomeException, try)
import Control.Monad (when)
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)
import Logger (logDebug)
import Matcher
import Printer
import Regexp (match)
import Text.Printf (printf)
import Yaml (normalizationRules)
import qualified Yaml as Y

data RuleContext = RuleContext
  { RuleContext -> BuildTermFunc
_buildTerm :: BuildTermFunc
  , RuleContext -> Maybe Expression
_universe :: Maybe Expression
  , RuleContext -> Expression -> Bool
_normal :: Expression -> Bool
  }

data Step = Step
  { Step -> String
_name :: String
  , Step
-> RuleContext
-> Expression
-> IO (Maybe (Expression, [(Expression, Expression)]))
_applied :: RuleContext -> Expression -> IO (Maybe (Expression, [(Expression, Expression)]))
  }

matchesAnyNormalizationRule :: Expression -> RuleContext -> Bool
matchesAnyNormalizationRule :: Expression -> RuleContext -> Bool
matchesAnyNormalizationRule Expression
expr RuleContext
ctx = Expression -> [Rule] -> RuleContext -> Bool
matchesAnyNormalizationRule' Expression
expr [Rule]
normalizationRules RuleContext
ctx
  where
    matchesAnyNormalizationRule' :: Expression -> [Y.Rule] -> RuleContext -> Bool
    matchesAnyNormalizationRule' :: Expression -> [Rule] -> RuleContext -> Bool
matchesAnyNormalizationRule' Expression
_ [] RuleContext
_ = Bool
False
    matchesAnyNormalizationRule' Expression
expr (Rule
rule : [Rule]
rules) RuleContext
ctx =
      let matched :: [Subst]
matched = IO [Subst] -> [Subst]
forall a. IO a -> a
unsafePerformIO (MatchExpressionFunc
-> [Subst] -> Expression -> Rule -> RuleContext -> IO [Subst]
admitted (Rule -> MatchExpressionFunc
deep Rule
rule) [Subst
substEmpty] Expression
expr Rule
rule RuleContext
ctx)
       in Bool -> Bool
not ([Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
matched) Bool -> Bool -> Bool
|| Expression -> [Rule] -> RuleContext -> Bool
matchesAnyNormalizationRule' Expression
expr [Rule]
rules RuleContext
ctx

isNF :: Expression -> RuleContext -> Bool
isNF :: Expression -> RuleContext -> Bool
isNF Expression
expr RuleContext
ctx = (Expression -> Bool) -> Expression -> Bool
normalWith (Expression -> RuleContext -> Bool
`matchesAnyNormalizationRule` RuleContext
ctx) Expression
expr

normal :: Expression -> Bool
normal :: Expression -> Bool
normal Expression
expr = Expression -> RuleContext -> Bool
isNF Expression
expr (BuildTermFunc
-> Maybe Expression -> (Expression -> Bool) -> RuleContext
RuleContext BuildTermFunc
buildTerm Maybe Expression
forall a. Maybe a
Nothing Expression -> Bool
normal)

normalWith :: (Expression -> Bool) -> Expression -> Bool
normalWith :: (Expression -> Bool) -> Expression -> Bool
normalWith Expression -> Bool
_ Expression
ExXi = Bool
True
normalWith Expression -> Bool
_ Expression
ExRoot = Bool
True
normalWith Expression -> Bool
_ Expression
ExTermination = Bool
True
normalWith Expression -> Bool
_ (ExDispatch Expression
ExXi Attribute
_) = Bool
True
normalWith Expression -> Bool
_ (ExDispatch Expression
ExRoot Attribute
_) = Bool
True
normalWith Expression -> Bool
_ (ExDispatch Expression
ExTermination Attribute
_) = Bool
False
normalWith Expression -> Bool
_ (ExApplication Expression
ExTermination Argument
_) = Bool
False
normalWith Expression -> Bool
_ (ExFormation []) = Bool
True
normalWith Expression -> Bool
matching (ExFormation [Binding]
bds) = [Binding] -> Bool
normalBindings [Binding]
bds Bool -> Bool -> Bool
|| Bool -> Bool
not (Expression -> Bool
matching ([Binding] -> Expression
ExFormation [Binding]
bds))
  where
    normalBindings :: [Binding] -> Bool
    normalBindings :: [Binding] -> Bool
normalBindings [Binding]
bds = (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Binding -> Bool
inert [Binding]
bds Bool -> Bool -> Bool
&& Bool -> Bool
not ((Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Binding -> Bool
delta [Binding]
bds Bool -> Bool -> Bool
&& (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Binding -> Bool
lambda [Binding]
bds)
    inert :: Binding -> Bool
    inert :: Binding -> Bool
inert (BiDelta Bytes
_) = Bool
True
    inert (BiVoid Attribute
_) = Bool
True
    inert (BiLambda Function
_) = Bool
True
    inert Binding
_ = Bool
False
    delta :: Binding -> Bool
    delta :: Binding -> Bool
delta (BiDelta Bytes
_) = Bool
True
    delta Binding
_ = Bool
False
    lambda :: Binding -> Bool
    lambda :: Binding -> Bool
lambda (BiLambda Function
_) = Bool
True
    lambda Binding
_ = Bool
False
normalWith Expression -> Bool
matching Expression
expr = Bool -> Bool
not (Expression -> Bool
matching Expression
expr)

normalHeld :: (Expression -> Bool) -> Expression -> Bool
normalHeld :: (Expression -> Bool) -> Expression -> Bool
normalHeld Expression -> Bool
_ (ExMeta Text
_) = Bool
False
normalHeld Expression -> Bool
_ (ExAny Slot
_) = Bool
False
normalHeld Expression -> Bool
test Expression
expr = Expression -> Bool
test Expression
expr

_or :: [Y.Condition] -> Subst -> RuleContext -> IO [Subst]
_or :: [Condition] -> Subst -> RuleContext -> IO [Subst]
_or [Condition]
conds Subst
subst RuleContext
ctx = Maybe SomeException -> [Condition] -> IO [Subst]
loop Maybe SomeException
forall a. Maybe a
Nothing [Condition]
conds
  where
    loop :: Maybe SomeException -> [Y.Condition] -> IO [Subst]
    loop :: Maybe SomeException -> [Condition] -> IO [Subst]
loop Maybe SomeException
raised [] = IO [Subst]
-> (SomeException -> IO [Subst])
-> Maybe SomeException
-> IO [Subst]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []) SomeException -> IO [Subst]
forall e a. Exception e => e -> IO a
throwIO Maybe SomeException
raised
    loop Maybe SomeException
raised (Condition
cond : [Condition]
rest) = do
      Either SomeException [Subst]
met <- IO [Subst] -> IO (Either SomeException [Subst])
forall e a. Exception e => IO a -> IO (Either e a)
try (Condition -> Subst -> RuleContext -> IO [Subst]
meetCondition' Condition
cond Subst
subst RuleContext
ctx) :: IO (Either SomeException [Subst])
      case Either SomeException [Subst]
met of
        Right [] -> Maybe SomeException -> [Condition] -> IO [Subst]
loop Maybe SomeException
raised [Condition]
rest
        Right [Subst]
mets -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst]
mets
        Left SomeException
err -> do
          String -> IO ()
logDebug (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Condition %s raised and was treated as not met: %s" (Condition -> String
forall a. Show a => a -> String
show Condition
cond) (SomeException -> String
forall e. Exception e => e -> String
displayException SomeException
err))
          Maybe SomeException -> [Condition] -> IO [Subst]
loop (SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just SomeException
err) [Condition]
rest

_and :: [Y.Condition] -> Subst -> RuleContext -> IO [Subst]
_and :: [Condition] -> Subst -> RuleContext -> IO [Subst]
_and [] Subst
subst RuleContext
_ = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst]
_and (Condition
cond : [Condition]
rest) Subst
subst RuleContext
ctx = do
  [Subst]
met <- Condition -> Subst -> RuleContext -> IO [Subst]
meetCondition' Condition
cond Subst
subst RuleContext
ctx
  if [Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
met
    then [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    else [Condition] -> Subst -> RuleContext -> IO [Subst]
_and [Condition]
rest Subst
subst RuleContext
ctx

_not :: Y.Condition -> Subst -> RuleContext -> IO [Subst]
_not :: Condition -> Subst -> RuleContext -> IO [Subst]
_not Condition
cond Subst
subst RuleContext
ctx = do
  [Subst]
met <- Condition -> Subst -> RuleContext -> IO [Subst]
meetCondition' Condition
cond Subst
subst RuleContext
ctx
  [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | [Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
met]

_in :: [Attribute] -> [Binding] -> Subst -> RuleContext -> IO [Subst]
_in :: [Attribute] -> [Binding] -> Subst -> RuleContext -> IO [Subst]
_in [Attribute]
attrs [Binding]
bindings Subst
subst RuleContext
_ =
  case ((Attribute -> Either String Attribute)
-> [Attribute] -> Either String [Attribute]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Attribute -> Subst -> Either String Attribute
`buildAttribute` Subst
subst) [Attribute]
attrs, (Binding -> Either String [Binding])
-> [Binding] -> Either String [[Binding]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Binding -> Subst -> Either String [Binding]
`buildBindingUnchecked` Subst
subst) [Binding]
bindings) of
    (Right [Attribute]
attrs', Right [[Binding]]
bdss) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | (Attribute -> Bool) -> [Attribute] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Attribute -> [Binding] -> Bool
`presentIn` [[Binding]] -> [Binding]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Binding]]
bdss) [Attribute]
attrs']
    (Either String [Attribute]
_, Either String [[Binding]]
_) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

numToInt :: Y.Number -> Subst -> Maybe Int
numToInt :: Number -> Subst -> Maybe Int
numToInt (Y.MetaIndex Text
meta) (Subst Map Meta MetaValue
mp) = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Text -> Meta
Named Text
meta) Map Meta MetaValue
mp of
  Just (MvIndex Int
idx) -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
idx
  Maybe MetaValue
_ -> Maybe Int
forall a. Maybe a
Nothing
numToInt (Y.Length (BiMeta Text
meta)) (Subst Map Meta MetaValue
mp) = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Text -> Meta
Named Text
meta) Map Meta MetaValue
mp of
  Just (MvBindings [Binding]
bds) -> Int -> Maybe Int
forall a. a -> Maybe a
Just ([Binding] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Binding]
bds)
  Maybe MetaValue
_ -> Maybe Int
forall a. Maybe a
Nothing
numToInt (Y.Domain (BiMeta Text
meta)) (Subst Map Meta MetaValue
mp) = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Text -> Meta
Named Text
meta) Map Meta MetaValue
mp of
  Just (MvBindings [Binding]
bds) -> Int -> Maybe Int
forall a. a -> Maybe a
Just ([Binding] -> Int
domainOf [Binding]
bds)
  Maybe MetaValue
_ -> Maybe Int
forall a. Maybe a
Nothing
numToInt (Y.Literal Int
num) Subst
_ = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
num
numToInt Number
_ Subst
_ = Maybe Int
forall a. Maybe a
Nothing

domainOf :: [Binding] -> Int
domainOf :: [Binding] -> Int
domainOf = [Binding] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Binding] -> Int) -> ([Binding] -> [Binding]) -> [Binding] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Binding -> Bool) -> [Binding] -> [Binding]
forall a. (a -> Bool) -> [a] -> [a]
filter Binding -> Bool
notAsset
  where
    notAsset :: Binding -> Bool
    notAsset :: Binding -> Bool
notAsset (BiDelta Bytes
_) = Bool
False
    notAsset (BiLambda Function
_) = Bool
False
    notAsset (BiVoid Attribute
AtRho) = Bool
False
    notAsset (BiTau Attribute
AtRho Expression
_) = Bool
False
    notAsset Binding
_ = Bool
True

_eq :: Y.Comparable -> Y.Comparable -> Subst -> RuleContext -> IO [Subst]
_eq :: Comparable -> Comparable -> Subst -> RuleContext -> IO [Subst]
_eq (Y.CmpNum Number
left) (Y.CmpNum Number
right) Subst
subst RuleContext
_ = case (Number -> Subst -> Maybe Int
numToInt Number
left Subst
subst, Number -> Subst -> Maybe Int
numToInt Number
right Subst
subst) of
  (Just Int
left_, Just Int
right_) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Int
left_ Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
right_]
  (Maybe Int
_, Maybe Int
_) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
_eq (Y.CmpAttr Attribute
left) (Y.CmpAttr Attribute
right) Subst
subst RuleContext
_ = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Attribute -> Attribute -> Subst -> Bool
compareAttrs Attribute
left Attribute
right Subst
subst]
  where
    compareAttrs :: Attribute -> Attribute -> Subst -> Bool
    compareAttrs :: Attribute -> Attribute -> Subst -> Bool
compareAttrs (AtMeta Text
left) (AtMeta Text
right) (Subst Map Meta MetaValue
mp) = case (Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Text -> Meta
Named Text
left) Map Meta MetaValue
mp, Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Text -> Meta
Named Text
right) Map Meta MetaValue
mp) of
      (Just (MvAttribute Attribute
left'), Just (MvAttribute Attribute
right')) -> Attribute -> Attribute -> Subst -> Bool
compareAttrs Attribute
left' Attribute
right' (Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
mp)
      (Maybe MetaValue, Maybe MetaValue)
_ -> Bool
False
    compareAttrs Attribute
attr (AtMeta Text
meta) (Subst Map Meta MetaValue
mp) = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Text -> Meta
Named Text
meta) Map Meta MetaValue
mp of
      Just (MvAttribute Attribute
found) -> Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
found
      Maybe MetaValue
_ -> Bool
False
    compareAttrs (AtMeta Text
meta) Attribute
attr (Subst Map Meta MetaValue
mp) = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Text -> Meta
Named Text
meta) Map Meta MetaValue
mp of
      Just (MvAttribute Attribute
found) -> Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
found
      Maybe MetaValue
_ -> Bool
False
    compareAttrs Attribute
left Attribute
right Subst
_ = Attribute
right Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
left
_eq (Y.CmpExpr Expression
left) (Y.CmpExpr Expression
right) Subst
subst RuleContext
_ =
  case (Expression -> Subst -> Built Expression
buildExpression Expression
left Subst
subst, Expression -> Subst -> Built Expression
buildExpression Expression
right Subst
subst) of
    (Right Expression
left', Right Expression
right') -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Expression
left' Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
right']
    (Built Expression
_, Built Expression
_) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
_eq Comparable
_ Comparable
_ Subst
_ RuleContext
_ = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

_gt :: Y.Comparable -> Y.Comparable -> Subst -> RuleContext -> IO [Subst]
_gt :: Comparable -> Comparable -> Subst -> RuleContext -> IO [Subst]
_gt (Y.CmpNum Number
left) (Y.CmpNum Number
right) Subst
subst RuleContext
_ = case (Number -> Subst -> Maybe Int
numToInt Number
left Subst
subst, Number -> Subst -> Maybe Int
numToInt Number
right Subst
subst) of
  (Just Int
left_, Just Int
right_) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Int
left_ Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
right_]
  (Maybe Int
_, Maybe Int
_) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
_gt Comparable
_ Comparable
_ Subst
_ RuleContext
_ = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

_nf :: Expression -> Subst -> RuleContext -> IO [Subst]
_nf :: Expression -> Subst -> RuleContext -> IO [Subst]
_nf (ExMeta Text
meta) (Subst Map Meta MetaValue
mp) RuleContext
ctx = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Text -> Meta
Named Text
meta) Map Meta MetaValue
mp of
  Just (MvExpression Expression
expr) | Expression -> Bool
bound Expression
expr -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
mp | RuleContext -> Expression -> Bool
_normal RuleContext
ctx Expression
expr]
  Just (MvExpression Expression
expr) -> Expression -> Subst -> RuleContext -> IO [Subst]
_nf Expression
expr (Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
mp) RuleContext
ctx
  Maybe MetaValue
_ -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
_nf (ExAny Slot
slot) (Subst Map Meta MetaValue
mp) RuleContext
ctx = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Slot -> Meta
Anon Slot
slot) Map Meta MetaValue
mp of
  Just (MvExpression Expression
expr) | Expression -> Bool
bound Expression
expr -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
mp | RuleContext -> Expression -> Bool
_normal RuleContext
ctx Expression
expr]
  Just (MvExpression Expression
expr) -> Expression -> Subst -> RuleContext -> IO [Subst]
_nf Expression
expr (Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
mp) RuleContext
ctx
  Maybe MetaValue
_ -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
_nf Expression
expr Subst
subst RuleContext
ctx = do
  Expression
built <- Expression -> Subst -> IO Expression
buildExpressionThrows Expression
expr Subst
subst
  [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | RuleContext -> Expression -> Bool
_normal RuleContext
ctx Expression
built]

_absolute :: Expression -> Subst -> RuleContext -> IO [Subst]
_absolute :: Expression -> Subst -> RuleContext -> IO [Subst]
_absolute (ExMeta Text
meta) (Subst Map Meta MetaValue
mp) RuleContext
ctx = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Text -> Meta
Named Text
meta) Map Meta MetaValue
mp of
  Just (MvExpression Expression
expr) | Expression -> Bool
bound Expression
expr -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
mp | Expression -> Bool
xiFree Expression
expr]
  Just (MvExpression Expression
expr) -> Expression -> Subst -> RuleContext -> IO [Subst]
_absolute Expression
expr (Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
mp) RuleContext
ctx
  Maybe MetaValue
_ -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
_absolute (ExAny Slot
slot) (Subst Map Meta MetaValue
mp) RuleContext
ctx = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Slot -> Meta
Anon Slot
slot) Map Meta MetaValue
mp of
  Just (MvExpression Expression
expr) | Expression -> Bool
bound Expression
expr -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
mp | Expression -> Bool
xiFree Expression
expr]
  Just (MvExpression Expression
expr) -> Expression -> Subst -> RuleContext -> IO [Subst]
_absolute Expression
expr (Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
mp) RuleContext
ctx
  Maybe MetaValue
_ -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
_absolute Expression
expr Subst
subst RuleContext
_ = do
  Expression
built <- Expression -> Subst -> IO Expression
buildExpressionThrows Expression
expr Subst
subst
  [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Expression -> Bool
xiFree Expression
built]

bound :: Expression -> Bool
bound :: Expression -> Bool
bound (ExMeta Text
_) = Bool
False
bound (ExAny Slot
_) = Bool
False
bound Expression
_ = Bool
True

xiFree :: Expression -> Bool
xiFree :: Expression -> Bool
xiFree (ExFormation [Binding]
_) = Bool
True
xiFree Expression
ExRoot = Bool
True
xiFree Expression
ExTermination = Bool
True
xiFree (ExApplication Expression
e (ArTau Attribute
_ Expression
te)) = Expression -> Bool
xiFree Expression
e Bool -> Bool -> Bool
&& Expression -> Bool
xiFree Expression
te
xiFree (ExApplication Expression
e (ArAlpha Alpha
_ Expression
te)) = Expression -> Bool
xiFree Expression
e Bool -> Bool -> Bool
&& Expression -> Bool
xiFree Expression
te
xiFree (ExDispatch Expression
e Attribute
_) = Expression -> Bool
xiFree Expression
e
xiFree Expression
_ = Bool
False

_isFormation :: Expression -> Subst -> RuleContext -> IO [Subst]
_isFormation :: Expression -> Subst -> RuleContext -> IO [Subst]
_isFormation (ExMeta Text
meta) (Subst Map Meta MetaValue
mp) RuleContext
ctx = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Text -> Meta
Named Text
meta) Map Meta MetaValue
mp of
  Just (MvExpression Expression
expr) -> Expression -> Subst -> RuleContext -> IO [Subst]
_isFormation Expression
expr (Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
mp) RuleContext
ctx
  Maybe MetaValue
_ -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
_isFormation Expression
expr Subst
subst RuleContext
_ = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Expression -> Bool
isFormation Expression
expr]

isFormation :: Expression -> Bool
isFormation :: Expression -> Bool
isFormation (ExFormation [Binding]
_) = Bool
True
isFormation Expression
_ = Bool
False

_matches :: String -> Expression -> Subst -> RuleContext -> IO [Subst]
_matches :: String -> Expression -> Subst -> RuleContext -> IO [Subst]
_matches String
pat (ExMeta Text
meta) (Subst Map Meta MetaValue
mp) RuleContext
ctx = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Text -> Meta
Named Text
meta) Map Meta MetaValue
mp of
  Just (MvExpression Expression
expr) -> String -> Expression -> Subst -> RuleContext -> IO [Subst]
_matches String
pat Expression
expr (Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
mp) RuleContext
ctx
  Maybe MetaValue
_ -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
_matches String
pat Expression
expr Subst
subst RuleContext
ctx = do
  (TeBytes Bytes
tgt) <- RuleContext -> BuildTermFunc
_buildTerm RuleContext
ctx String
"dataize" [Expression -> ExtraArgument
Y.ArgExpression Expression
expr] Subst
subst
  Bool
matched <- ByteString -> ByteString -> IO Bool
match (Text -> ByteString
T.encodeUtf8 (String -> Text
T.pack String
pat)) (Text -> ByteString
T.encodeUtf8 (String -> Text
T.pack (Bytes -> String
btsToUnescapedStr Bytes
tgt)))
  [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Bool
matched]

_partOf :: Expression -> Binding -> Subst -> RuleContext -> IO [Subst]
_partOf :: Expression -> Binding -> Subst -> RuleContext -> IO [Subst]
_partOf Expression
exp Binding
bd Subst
subst RuleContext
_ = do
  Expression
exp' <- Expression -> Subst -> IO Expression
buildExpressionThrows Expression
exp Subst
subst
  [Binding]
bds <- Binding -> Subst -> IO [Binding]
buildBindingThrows Binding
bd Subst
subst
  [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Expression -> [Binding] -> Bool
partOf Expression
exp' [Binding]
bds]
  where
    partOf :: Expression -> [Binding] -> Bool
    partOf :: Expression -> [Binding] -> Bool
partOf Expression
_ [] = Bool
False
    partOf Expression
expr (BiTau Attribute
_ (ExFormation [Binding]
bds) : [Binding]
rest) = Expression
expr Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== [Binding] -> Expression
ExFormation [Binding]
bds Bool -> Bool -> Bool
|| Expression -> [Binding] -> Bool
partOf Expression
expr [Binding]
bds Bool -> Bool -> Bool
|| Expression -> [Binding] -> Bool
partOf Expression
expr [Binding]
rest
    partOf Expression
expr (BiTau Attribute
_ Expression
expr' : [Binding]
rest) = Expression
expr Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
expr' Bool -> Bool -> Bool
|| Expression -> [Binding] -> Bool
partOf Expression
expr [Binding]
rest
    partOf Expression
expr (Binding
_ : [Binding]
rest) = Expression -> [Binding] -> Bool
partOf Expression
expr [Binding]
rest

_disjoint :: [Attribute] -> [Binding] -> Subst -> RuleContext -> IO [Subst]
_disjoint :: [Attribute] -> [Binding] -> Subst -> RuleContext -> IO [Subst]
_disjoint [Attribute]
attrs [Binding]
bindings Subst
subst RuleContext
_ =
  case ((Attribute -> Either String Attribute)
-> [Attribute] -> Either String [Attribute]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Attribute -> Subst -> Either String Attribute
`buildAttribute` Subst
subst) [Attribute]
attrs, (Binding -> Either String [Binding])
-> [Binding] -> Either String [[Binding]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Binding -> Subst -> Either String [Binding]
`buildBindingUnchecked` Subst
subst) [Binding]
bindings) of
    (Right [Attribute]
attrs', Right [[Binding]]
bdss) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Bool -> Bool
not ((Attribute -> Bool) -> [Attribute] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Attribute -> [Binding] -> Bool
`presentIn` [[Binding]] -> [Binding]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Binding]]
bdss) [Attribute]
attrs')]
    (Either String [Attribute]
_, Either String [[Binding]]
_) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

presentIn :: Attribute -> [Binding] -> Bool
presentIn :: Attribute -> [Binding] -> Bool
presentIn Attribute
attr = (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Binding -> Bool
present
  where
    present :: Binding -> Bool
    present :: Binding -> Bool
present (BiTau Attribute
battr Expression
_) = Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
battr
    present (BiVoid Attribute
battr) = Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
battr
    present (BiLambda Function
_) = Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
AtLambda
    present (BiDelta Bytes
_) = Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
AtDelta
    present Binding
_ = Bool
False

meetCondition' :: Y.Condition -> Subst -> RuleContext -> IO [Subst]
meetCondition' :: Condition -> Subst -> RuleContext -> IO [Subst]
meetCondition' (Y.Or [Condition]
conds) = [Condition] -> Subst -> RuleContext -> IO [Subst]
_or [Condition]
conds
meetCondition' (Y.And [Condition]
conds) = [Condition] -> Subst -> RuleContext -> IO [Subst]
_and [Condition]
conds
meetCondition' (Y.Not Condition
cond) = Condition -> Subst -> RuleContext -> IO [Subst]
_not Condition
cond
meetCondition' (Y.In [Attribute]
attrs [Binding]
bds) = [Attribute] -> [Binding] -> Subst -> RuleContext -> IO [Subst]
_in [Attribute]
attrs [Binding]
bds
meetCondition' (Y.Eq Comparable
left Comparable
right) = Comparable -> Comparable -> Subst -> RuleContext -> IO [Subst]
_eq Comparable
left Comparable
right
meetCondition' (Y.Gt Comparable
left Comparable
right) = Comparable -> Comparable -> Subst -> RuleContext -> IO [Subst]
_gt Comparable
left Comparable
right
meetCondition' (Y.NF Expression
expr) = Expression -> Subst -> RuleContext -> IO [Subst]
_nf Expression
expr
meetCondition' (Y.Absolute Expression
expr) = Expression -> Subst -> RuleContext -> IO [Subst]
_absolute Expression
expr
meetCondition' (Y.Matches String
pat Expression
expr) = String -> Expression -> Subst -> RuleContext -> IO [Subst]
_matches String
pat Expression
expr
meetCondition' (Y.PartOf Expression
expr Binding
bd) = Expression -> Binding -> Subst -> RuleContext -> IO [Subst]
_partOf Expression
expr Binding
bd
meetCondition' (Y.Disjoint [Attribute]
attrs [Binding]
bds) = [Attribute] -> [Binding] -> Subst -> RuleContext -> IO [Subst]
_disjoint [Attribute]
attrs [Binding]
bds
meetCondition' (Y.IsFormation Expression
expr) = Expression -> Subst -> RuleContext -> IO [Subst]
_isFormation Expression
expr

meetCondition :: Y.Condition -> [Subst] -> RuleContext -> IO [Subst]
meetCondition :: Condition -> [Subst] -> RuleContext -> IO [Subst]
meetCondition Condition
_ [] RuleContext
_ = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
meetCondition Condition
cond (Subst
subst : [Subst]
rest) RuleContext
ctx = do
  Either SomeException [Subst]
met <- IO [Subst] -> IO (Either SomeException [Subst])
forall e a. Exception e => IO a -> IO (Either e a)
try (Condition -> Subst -> RuleContext -> IO [Subst]
meetCondition' Condition
cond Subst
subst RuleContext
ctx) :: IO (Either SomeException [Subst])
  case Either SomeException [Subst]
met of
    Right [Subst]
first -> do
      [Subst]
next <- Condition -> [Subst] -> RuleContext -> IO [Subst]
meetCondition Condition
cond [Subst]
rest RuleContext
ctx
      case [Subst]
first of
        [] -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst]
next
        Subst
sbt : [Subst]
_ -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
sbt Subst -> [Subst] -> [Subst]
forall a. a -> [a] -> [a]
: [Subst]
next)
    Left SomeException
err -> do
      String -> IO ()
logDebug (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Condition %s raised and was treated as not met: %s" (Condition -> String
forall a. Show a => a -> String
show Condition
cond) (SomeException -> String
forall e. Exception e => e -> String
displayException SomeException
err))
      Condition -> [Subst] -> RuleContext -> IO [Subst]
meetCondition Condition
cond [Subst]
rest RuleContext
ctx

meetMaybeCondition :: Maybe Y.Condition -> [Subst] -> RuleContext -> IO [Subst]
meetMaybeCondition :: Maybe Condition -> [Subst] -> RuleContext -> IO [Subst]
meetMaybeCondition Maybe Condition
Nothing [Subst]
substs RuleContext
_ = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst]
substs
meetMaybeCondition (Just Condition
cond) [Subst]
substs RuleContext
ctx = Condition -> [Subst] -> RuleContext -> IO [Subst]
meetCondition Condition
cond [Subst]
substs RuleContext
ctx

extraSubstitutions :: [Subst] -> Maybe [Y.Extra] -> RuleContext -> IO [Subst]
extraSubstitutions :: [Subst] -> Maybe [Extra] -> RuleContext -> IO [Subst]
extraSubstitutions [Subst]
substs Maybe [Extra]
extras RuleContext{Maybe Expression
BuildTermFunc
Expression -> Bool
_buildTerm :: RuleContext -> BuildTermFunc
_universe :: RuleContext -> Maybe Expression
_normal :: RuleContext -> Expression -> Bool
_buildTerm :: BuildTermFunc
_universe :: Maybe Expression
_normal :: Expression -> Bool
..} = case Maybe [Extra]
extras of
  Maybe [Extra]
Nothing -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst]
substs
  Just [Extra]
extras' -> do
    String -> IO ()
logDebug (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"Building %d sets of extra substitutions.." ([Subst] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Subst]
substs))
    [Maybe Subst]
res <-
      [IO (Maybe Subst)] -> IO [Maybe Subst]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
        [ (Maybe Subst -> Extra -> IO (Maybe Subst))
-> Maybe Subst -> [Extra] -> IO (Maybe Subst)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
            ( \Maybe Subst
maybeSubst Extra
extra -> case Maybe Subst
maybeSubst of
                Maybe Subst
Nothing -> Maybe Subst -> IO (Maybe Subst)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Subst
forall a. Maybe a
Nothing
                Just Subst
subst' -> do
                  let maybeName :: Maybe Text
maybeName = case Extra -> ExtraArgument
Y.meta Extra
extra of
                        Y.ArgExpression (ExMeta Text
name) -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
name
                        Y.ArgAttribute (AtMeta Text
name) -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
name
                        Y.ArgBinding (BiMeta Text
name) -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
name
                        Y.ArgBytes (BtMeta Text
name) -> Text -> Maybe Text
forall a. a -> Maybe a
Just Text
name
                        ExtraArgument
_ -> Maybe Text
forall a. Maybe a
Nothing
                      func :: String
func = Extra -> String
Y.function Extra
extra
                      args :: [ExtraArgument]
args = Extra -> [ExtraArgument]
Y.args Extra
extra
                  Term
term <- BuildTermFunc
built String
func [ExtraArgument]
args Subst
subst'
                  MetaValue
meta <- case Term
term of
                    TeExpression Expression
expr -> do
                      String -> IO ()
logDebug (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Function %s() returned expression:\n%s" String
func (Expression -> String
printExpression Expression
expr))
                      MetaValue -> IO MetaValue
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> MetaValue
MvExpression Expression
expr)
                    TeAttribute Attribute
attr -> do
                      String -> IO ()
logDebug (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Function %s() returned attribute: %s" String
func (Attribute -> String
printAttribute Attribute
attr))
                      MetaValue -> IO MetaValue
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Attribute -> MetaValue
MvAttribute Attribute
attr)
                    TeBytes Bytes
bytes -> do
                      String -> IO ()
logDebug (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Function %s() returned bytes: %s" String
func (Bytes -> String
printBytes Bytes
bytes))
                      MetaValue -> IO MetaValue
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bytes -> MetaValue
MvBytes Bytes
bytes)
                    TeBindings [Binding]
bds -> do
                      String -> IO ()
logDebug (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Function %s return bindings: %s" String
func (Expression -> String
printExpression ([Binding] -> Expression
ExFormation [Binding]
bds)))
                      MetaValue -> IO MetaValue
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Binding] -> MetaValue
MvBindings [Binding]
bds)
                  case Maybe Text
maybeName of
                    Just Text
name -> Maybe Subst -> IO (Maybe Subst)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst -> Subst -> Maybe Subst
combine (Text -> MetaValue -> Subst
substSingle Text
name MetaValue
meta) Subst
subst')
                    Maybe Text
_ -> Maybe Subst -> IO (Maybe Subst)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Subst
forall a. Maybe a
Nothing
            )
            (Subst -> Maybe Subst
forall a. a -> Maybe a
Just Subst
subst)
            [Extra]
extras'
        | Subst
subst <- [Subst]
substs
        ]
    String -> IO ()
logDebug String
"Extra substitutions have been built"
    [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Maybe Subst] -> [Subst]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Subst]
res)
  where
    built :: String -> BuildTermMethod
    built :: BuildTermFunc
built String
"named" = Maybe Expression -> BuildTermMethod
nameOf Maybe Expression
_universe
    built String
func = BuildTermFunc
_buildTerm String
func

metasWithPrefix :: T.Text -> Expression -> [Expression]
metasWithPrefix :: Text -> Expression -> [Expression]
metasWithPrefix Text
prefix = [Expression] -> [Expression]
forall a. Eq a => [a] -> [a]
nub ([Expression] -> [Expression])
-> (Expression -> [Expression]) -> Expression -> [Expression]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression -> [Expression]
go
  where
    go :: Expression -> [Expression]
    go :: Expression -> [Expression]
go expr :: Expression
expr@(ExMeta Text
mt)
      | Text -> Text -> Bool
T.isPrefixOf Text
prefix Text
mt = [Expression
expr]
      | Bool
otherwise = []
    go expr :: Expression
expr@(ExAny (Slot Text
kind Int
_))
      | Text -> Text -> Bool
T.isPrefixOf Text
prefix Text
kind = [Expression
expr]
      | Bool
otherwise = []
    go (ExFormation [Binding]
bds) = (Binding -> [Expression]) -> [Binding] -> [Expression]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Binding -> [Expression]
goBinding [Binding]
bds
    go (ExApplication Expression
e Argument
arg) = Expression -> [Expression]
go Expression
e [Expression] -> [Expression] -> [Expression]
forall a. [a] -> [a] -> [a]
++ Argument -> [Expression]
goArgument Argument
arg
    go (ExDispatch Expression
e Attribute
_) = Expression -> [Expression]
go Expression
e
    go (ExPhiMeet Maybe String
_ Int
_ Expression
e) = Expression -> [Expression]
go Expression
e
    go (ExPhiAgain Maybe String
_ Int
_ Expression
e) = Expression -> [Expression]
go Expression
e
    go Expression
_ = []
    goBinding :: Binding -> [Expression]
    goBinding :: Binding -> [Expression]
goBinding (BiTau Attribute
_ Expression
e) = Expression -> [Expression]
go Expression
e
    goBinding Binding
_ = []
    goArgument :: Argument -> [Expression]
    goArgument :: Argument -> [Expression]
goArgument (ArTau Attribute
_ Expression
expr) = Expression -> [Expression]
go Expression
expr
    goArgument (ArAlpha Alpha
_ Expression
expr) = Expression -> [Expression]
go Expression
expr

matchExpressionWithRule :: Expression -> Y.Rule -> RuleContext -> IO [Subst]
matchExpressionWithRule :: Expression -> Rule -> RuleContext -> IO [Subst]
matchExpressionWithRule Expression
expr Rule
rule = MatchExpressionFunc
-> [Subst] -> Expression -> Rule -> RuleContext -> IO [Subst]
matchExpressionBy (Rule -> MatchExpressionFunc
deep Rule
rule) [Subst
substEmpty] Expression
expr Rule
rule

deep :: Y.Rule -> MatchExpressionFunc
deep :: Rule -> MatchExpressionFunc
deep Rule
rule Expression
ptn Expression
tgt
  | Bool -> Expression -> Expression -> Bool
reachable' (Rule -> Bool
redex Rule
rule) Expression
ptn Expression
tgt = Bool -> MatchExpressionFunc
matchExpressionDeep' (Rule -> Bool
redex Rule
rule) Expression
ptn Expression
tgt
  | Bool
otherwise = []

redex :: Y.Rule -> Bool
redex :: Rule -> Bool
redex Rule
rule = case Rule
rule.pattern of
  ExDispatch Expression
head' Attribute
_ -> Expression -> Bool
stuck Expression
head'
  ExApplication Expression
head' Argument
_ -> Expression -> Bool
stuck Expression
head'
  ExFormation [Binding]
bds -> (Attribute -> Bool) -> [Attribute] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Attribute -> [Attribute] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Binding -> [Attribute]) -> [Binding] -> [Attribute]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Binding -> [Attribute]
attribute [Binding]
bds [Attribute] -> [Attribute] -> [Attribute]
forall a. [a] -> [a] -> [a]
++ [Attribute]
-> (Condition -> [Attribute]) -> Maybe Condition -> [Attribute]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ([Binding] -> Condition -> [Attribute]
demanded [Binding]
bds) Rule
rule.when)) [Attribute
AtLambda, Attribute
AtDelta]
  Expression
_ -> Bool
False
  where
    stuck :: Expression -> Bool
    stuck :: Expression -> Bool
stuck (ExFormation [Binding]
_) = Bool
True
    stuck Expression
ExTermination = Bool
True
    stuck Expression
_ = Bool
False
    attribute :: Binding -> [Attribute]
    attribute :: Binding -> [Attribute]
attribute (BiLambda Function
_) = [Attribute
AtLambda]
    attribute (BiDelta Bytes
_) = [Attribute
AtDelta]
    attribute Binding
_ = []
    demanded :: [Binding] -> Y.Condition -> [Attribute]
    demanded :: [Binding] -> Condition -> [Attribute]
demanded [Binding]
bds (Y.In [Attribute]
attrs [Binding]
metas)
      | (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Binding
meta -> Binding -> Bool
isMeta Binding
meta Bool -> Bool -> Bool
&& Binding
meta Binding -> [Binding] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Binding]
bds) [Binding]
metas = [Attribute]
attrs
    demanded [Binding]
bds (Y.And [Condition]
conds) = (Condition -> [Attribute]) -> [Condition] -> [Attribute]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Binding] -> Condition -> [Attribute]
demanded [Binding]
bds) [Condition]
conds
    demanded [Binding]
bds (Y.Or (Condition
cond : [Condition]
conds)) = ([Attribute] -> Condition -> [Attribute])
-> [Attribute] -> [Condition] -> [Attribute]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\[Attribute]
attrs Condition
cond' -> [Attribute]
attrs [Attribute] -> [Attribute] -> [Attribute]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Binding] -> Condition -> [Attribute]
demanded [Binding]
bds Condition
cond') ([Binding] -> Condition -> [Attribute]
demanded [Binding]
bds Condition
cond) [Condition]
conds
    demanded [Binding]
_ Condition
_ = []
    isMeta :: Binding -> Bool
    isMeta :: Binding -> Bool
isMeta (BiMeta Text
_) = Bool
True
    isMeta Binding
_ = Bool
False

matchExpressionWithRule' :: [Subst] -> Expression -> Y.Rule -> RuleContext -> IO [Subst]
matchExpressionWithRule' :: [Subst] -> Expression -> Rule -> RuleContext -> IO [Subst]
matchExpressionWithRule' = MatchExpressionFunc
-> [Subst] -> Expression -> Rule -> RuleContext -> IO [Subst]
matchExpressionBy MatchExpressionFunc
matchExpression'

matchExpressionBy :: MatchExpressionFunc -> [Subst] -> Expression -> Y.Rule -> RuleContext -> IO [Subst]
matchExpressionBy :: MatchExpressionFunc
-> [Subst] -> Expression -> Rule -> RuleContext -> IO [Subst]
matchExpressionBy MatchExpressionFunc
matcher [Subst]
seed Expression
expr Rule
rule RuleContext
ctx = do
  [Subst]
when' <- MatchExpressionFunc
-> [Subst] -> Expression -> Rule -> RuleContext -> IO [Subst]
admitted MatchExpressionFunc
matcher [Subst]
seed Expression
expr Rule
rule RuleContext
ctx
  if [Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
when'
    then [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    else do
      String -> IO ()
logDebug (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Rule %s" Rule
rule.name)
      [Subst]
extended <- [Subst] -> Maybe [Extra] -> RuleContext -> IO [Subst]
extraSubstitutions [Subst]
when' Rule
rule.where_ RuleContext
ctx
      if [Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
extended
        then do
          String -> IO ()
logDebug String
"Substitution is empty after extending, maybe some metas are duplicated"
          [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        else do
          [Subst]
met <- Maybe Condition -> [Subst] -> RuleContext -> IO [Subst]
meetMaybeCondition Rule
rule.having [Subst]
extended RuleContext
ctx
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
met) (String -> IO ()
logDebug String
"The 'having' condition wasn't met")
          [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst]
met

admitted :: MatchExpressionFunc -> [Subst] -> Expression -> Y.Rule -> RuleContext -> IO [Subst]
admitted :: MatchExpressionFunc
-> [Subst] -> Expression -> Rule -> RuleContext -> IO [Subst]
admitted MatchExpressionFunc
matcher [Subst]
seed Expression
expr Rule
rule RuleContext
ctx =
  let ptn :: Expression
ptn = Rule
rule.pattern
      matched :: [Subst]
matched = [Subst] -> [Subst] -> [Subst]
combineMany [Subst]
seed (MatchExpressionFunc
matcher Expression
ptn Expression
expr)
   in if [Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
matched
        then do
          String -> IO ()
logDebug (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Pattern from rule '%s' was not matched:\n%s" Rule
rule.name (Expression -> PrintConfig -> String
printExpression' Expression
ptn PrintConfig
logPrintConfig))
          [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        else do
          [Subst]
inXiFree <- ([Subst] -> Expression -> IO [Subst])
-> [Subst] -> [Expression] -> IO [Subst]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\[Subst]
substs Expression
mt -> Condition -> [Subst] -> RuleContext -> IO [Subst]
meetCondition (Expression -> Condition
Y.Absolute Expression
mt) [Subst]
substs RuleContext
ctx) [Subst]
matched (Expression -> [Expression]
kMetas Expression
ptn)
          [Subst]
inNf <- ([Subst] -> Expression -> IO [Subst])
-> [Subst] -> [Expression] -> IO [Subst]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\[Subst]
substs Expression
mt -> Condition -> [Subst] -> RuleContext -> IO [Subst]
meetCondition (Expression -> Condition
Y.NF Expression
mt) [Subst]
substs RuleContext
ctx) [Subst]
inXiFree (Expression -> [Expression]
nfMetas Expression
ptn [Expression] -> [Expression] -> [Expression]
forall a. [a] -> [a] -> [a]
++ Expression -> [Expression]
kMetas Expression
ptn)
          if [Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
inNf
            then do
              String -> IO ()
logDebug String
"A '𝑛'/'𝑘' meta-variable is not in normal form, or a '𝑘' meta-variable is not xi-free"
              [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
            else do
              [Subst]
when' <- Maybe Condition -> [Subst] -> RuleContext -> IO [Subst]
meetMaybeCondition Rule
rule.when [Subst]
inNf RuleContext
ctx
              Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
when') (String -> IO ()
logDebug String
"The 'when' condition wasn't met")
              [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst]
when'
  where
    nfMetas :: Expression -> [Expression]
    nfMetas :: Expression -> [Expression]
nfMetas = Text -> Expression -> [Expression]
metasWithPrefix Text
"n"

    kMetas :: Expression -> [Expression]
    kMetas :: Expression -> [Expression]
kMetas = Text -> Expression -> [Expression]
metasWithPrefix Text
"k"