{-# LANGUAGE OverloadedStrings #-}
module Condition where
import Ast
import Builder (buildAttribute, buildBinding)
import Control.Exception (SomeException (SomeException), evaluate)
import Control.Exception.Base (try)
import Data.Aeson (FromJSON)
import qualified Data.ByteString.Char8 as B
import qualified Data.Map.Strict as M
import Functions (buildTermFromFunction)
import GHC.IO (unsafePerformIO)
import Logger (logDebug)
import Matcher
import Misc (allPathsIn, btsToUnescapedStr)
import Pretty (prettyExpression, prettySubsts)
import Regexp (match)
import Term (Term (TeBytes))
import Yaml (normalizationRules)
import qualified Yaml as Y
attrInBindings :: Attribute -> [Binding] -> Bool
attrInBindings :: Attribute -> [Binding] -> Bool
attrInBindings Attribute
attr (Binding
bd : [Binding]
bds) = Attribute -> Binding -> Bool
attrInBinding Attribute
attr Binding
bd Bool -> Bool -> Bool
|| Attribute -> [Binding] -> Bool
attrInBindings Attribute
attr [Binding]
bds
where
attrInBinding :: Attribute -> Binding -> Bool
attrInBinding :: Attribute -> Binding -> Bool
attrInBinding Attribute
attr (BiTau Attribute
battr Expression
_) = Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
battr
attrInBinding Attribute
attr (BiVoid Attribute
battr) = Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
battr
attrInBinding Attribute
AtLambda (BiLambda String
_) = Bool
True
attrInBinding Attribute
AtDelta (BiDelta Bytes
_) = Bool
True
attrInBinding Attribute
_ Binding
_ = Bool
False
attrInBindings Attribute
_ [Binding]
_ = Bool
False
compareAttrs :: Attribute -> Attribute -> Subst -> Bool
compareAttrs :: Attribute -> Attribute -> Subst -> Bool
compareAttrs (AtMeta String
left) (AtMeta String
right) Subst
_ = String
left String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
right
compareAttrs Attribute
attr (AtMeta String
meta) (Subst Map String MetaValue
mp) = case String -> Map String MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
meta Map String 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 String
meta) Attribute
attr (Subst Map String MetaValue
mp) = case String -> Map String MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
meta Map String 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
subst = Attribute
right Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
left
numToInt :: Y.Number -> Subst -> Maybe Integer
numToInt :: Number -> Subst -> Maybe Integer
numToInt (Y.Ordinal (AtMeta String
meta)) (Subst Map String MetaValue
mp) = case String -> Map String MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
meta Map String MetaValue
mp of
Just (MvAttribute (AtAlpha Integer
idx)) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
idx
Maybe MetaValue
_ -> Maybe Integer
forall a. Maybe a
Nothing
numToInt (Y.Ordinal (AtAlpha Integer
idx)) Subst
subst = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
idx
numToInt (Y.Length (BiMeta String
meta)) (Subst Map String MetaValue
mp) = case String -> Map String MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
meta Map String MetaValue
mp of
Just (MvBindings [Binding]
bds) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Int -> Integer
forall a. Integral a => a -> Integer
toInteger ([Binding] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Binding]
bds))
Maybe MetaValue
_ -> Maybe Integer
forall a. Maybe a
Nothing
numToInt (Y.Literal Integer
num) Subst
subst = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
num
numToInt Number
_ Subst
_ = Maybe Integer
forall a. Maybe a
Nothing
matchesAnyNormalizationRule :: Expression -> Bool
matchesAnyNormalizationRule :: Expression -> Bool
matchesAnyNormalizationRule Expression
expr = Expression -> [Rule] -> Bool
matchesAnyNormalizationRule' Expression
expr [Rule]
normalizationRules
where
matchesAnyNormalizationRule' :: Expression -> [Y.Rule] -> Bool
matchesAnyNormalizationRule' :: Expression -> [Rule] -> Bool
matchesAnyNormalizationRule' Expression
_ [] = Bool
False
matchesAnyNormalizationRule' Expression
expr (Rule
rule : [Rule]
rules) =
case IO (Maybe [Subst]) -> Maybe [Subst]
forall a. IO a -> a
unsafePerformIO (Expression -> Maybe Condition -> Program -> IO (Maybe [Subst])
matchProgramWithCondition (Rule -> Expression
Y.pattern Rule
rule) (Rule -> Maybe Condition
Y.when Rule
rule) (Expression -> Program
Program Expression
expr)) of
Just [Subst]
matched -> 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] -> Bool
matchesAnyNormalizationRule' Expression
expr [Rule]
rules
Maybe [Subst]
Nothing -> Expression -> [Rule] -> Bool
matchesAnyNormalizationRule' Expression
expr [Rule]
rules
isNF :: Expression -> Bool
isNF :: Expression -> Bool
isNF Expression
ExThis = Bool
True
isNF Expression
ExGlobal = Bool
True
isNF Expression
ExTermination = Bool
True
isNF (ExDispatch Expression
ExThis Attribute
_) = Bool
True
isNF (ExDispatch Expression
ExGlobal Attribute
_) = Bool
True
isNF (ExDispatch Expression
ExTermination Attribute
_) = Bool
False
isNF (ExApplication Expression
ExTermination Binding
_) = Bool
False
isNF (ExFormation []) = Bool
True
isNF (ExFormation [Binding]
bds) = [Binding] -> Bool
normalBindings [Binding]
bds Bool -> Bool -> Bool
|| Bool -> Bool
not (Expression -> Bool
matchesAnyNormalizationRule ([Binding] -> Expression
ExFormation [Binding]
bds))
where
normalBindings :: [Binding] -> Bool
normalBindings :: [Binding] -> Bool
normalBindings [] = Bool
True
normalBindings (Binding
bd : [Binding]
bds) =
let next :: Bool
next = [Binding] -> Bool
normalBindings [Binding]
bds
in case Binding
bd of
BiDelta Bytes
_ -> Bool
next
BiVoid Attribute
_ -> Bool
next
BiLambda String
_ -> Bool
next
Binding
_ -> Bool
False
isNF Expression
expr = Bool -> Bool
not (Expression -> Bool
matchesAnyNormalizationRule Expression
expr)
meetCondition' :: Y.Condition -> Subst -> IO [Subst]
meetCondition' :: Condition -> Subst -> IO [Subst]
meetCondition' (Y.Or []) Subst
subst = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst]
meetCondition' (Y.Or (Condition
cond : [Condition]
rest)) Subst
subst = do
[Subst]
met <- Condition -> Subst -> IO [Subst]
meetCondition' Condition
cond Subst
subst
if [Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
met
then Condition -> Subst -> IO [Subst]
meetCondition' ([Condition] -> Condition
Y.Or [Condition]
rest) Subst
subst
else [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst]
met
meetCondition' (Y.And []) Subst
subst = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst]
meetCondition' (Y.And (Condition
cond : [Condition]
rest)) Subst
subst = do
[Subst]
met <- Condition -> Subst -> IO [Subst]
meetCondition' Condition
cond Subst
subst
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 -> IO [Subst]
meetCondition' ([Condition] -> Condition
Y.And [Condition]
rest) Subst
subst
meetCondition' (Y.Not Condition
cond) Subst
subst = do
[Subst]
met <- Condition -> Subst -> IO [Subst]
meetCondition' Condition
cond Subst
subst
[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]
meetCondition' (Y.In Attribute
attr Binding
binding) Subst
subst =
case (Attribute -> Subst -> Maybe Attribute
buildAttribute Attribute
attr Subst
subst, Binding -> Subst -> Maybe [Binding]
buildBinding Binding
binding Subst
subst) of
(Just Attribute
attr, Just [Binding]
bds) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Attribute -> [Binding] -> Bool
attrInBindings Attribute
attr [Binding]
bds]
(Maybe Attribute
_, Maybe [Binding]
_) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
meetCondition' (Y.Alpha (AtAlpha Integer
_)) Subst
subst = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst]
meetCondition' (Y.Alpha (AtMeta String
name)) (Subst Map String MetaValue
mp) = case String -> Map String MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
name Map String MetaValue
mp of
Just (MvAttribute (AtAlpha Integer
_)) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Map String MetaValue -> Subst
Subst Map String MetaValue
mp]
Maybe MetaValue
_ -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
meetCondition' (Y.Alpha Attribute
_) Subst
_ = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
meetCondition' (Y.Eq (Y.CmpNum Number
left) (Y.CmpNum Number
right)) Subst
subst = case (Number -> Subst -> Maybe Integer
numToInt Number
left Subst
subst, Number -> Subst -> Maybe Integer
numToInt Number
right Subst
subst) of
(Just Integer
left_, Just Integer
right_) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Integer
left_ Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
right_]
(Maybe Integer
_, Maybe Integer
_) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
meetCondition' (Y.Eq (Y.CmpAttr Attribute
left) (Y.CmpAttr Attribute
right)) Subst
subst = [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]
meetCondition' (Y.Eq Comparable
_ Comparable
_) Subst
_ = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
meetCondition' (Y.NF (ExMeta String
meta)) (Subst Map String MetaValue
mp) = case String -> Map String MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
meta Map String MetaValue
mp of
Just (MvExpression Expression
expr Expression
_) -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Map String MetaValue -> Subst
Subst Map String MetaValue
mp | Expression -> Bool
isNF Expression
expr]
Maybe MetaValue
_ -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
meetCondition' (Y.NF Expression
expr) (Subst Map String MetaValue
mp) = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Map String MetaValue -> Subst
Subst Map String MetaValue
mp | Expression -> Bool
isNF Expression
expr]
meetCondition' (Y.XI (ExMeta String
meta)) (Subst Map String MetaValue
mp) = case String -> Map String MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
meta Map String MetaValue
mp of
Just (MvExpression Expression
expr Expression
_) -> Condition -> Subst -> IO [Subst]
meetCondition' (Expression -> Condition
Y.XI Expression
expr) (Map String MetaValue -> Subst
Subst Map String MetaValue
mp)
Maybe MetaValue
_ -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
meetCondition' (Y.XI (ExFormation [Binding]
_)) Subst
subst = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst]
meetCondition' (Y.XI Expression
ExThis) Subst
subst = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
meetCondition' (Y.XI Expression
ExGlobal) Subst
subst = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst]
meetCondition' (Y.XI (ExApplication Expression
expr (BiTau Attribute
attr Expression
texpr))) Subst
subst = do
[Subst]
onExpr <- Condition -> Subst -> IO [Subst]
meetCondition' (Expression -> Condition
Y.XI Expression
expr) Subst
subst
[Subst]
onTau <- Condition -> Subst -> IO [Subst]
meetCondition' (Expression -> Condition
Y.XI Expression
texpr) Subst
subst
[Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst
subst | Bool -> Bool
not ([Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
onExpr) Bool -> Bool -> Bool
&& Bool -> Bool
not ([Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
onTau)]
meetCondition' (Y.XI (ExDispatch Expression
expr Attribute
_)) Subst
subst = Condition -> Subst -> IO [Subst]
meetCondition' (Expression -> Condition
Y.XI Expression
expr) Subst
subst
meetCondition' (Y.Matches String
pat (ExMeta String
meta)) (Subst Map String MetaValue
mp) = case String -> Map String MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
meta Map String MetaValue
mp of
Just (MvExpression Expression
expr Expression
_) -> Condition -> Subst -> IO [Subst]
meetCondition' (String -> Expression -> Condition
Y.Matches String
pat Expression
expr) (Map String MetaValue -> Subst
Subst Map String MetaValue
mp)
Maybe MetaValue
_ -> [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
meetCondition' (Y.Matches String
pat Expression
expr) Subst
subst = do
(TeBytes Bytes
tgt) <- String -> [ExtraArgument] -> Subst -> Program -> IO Term
buildTermFromFunction String
"dataize" [Expression -> ExtraArgument
Y.ArgExpression Expression
expr] Subst
subst (Expression -> Program
Program Expression
expr)
Bool
matched <- ByteString -> ByteString -> IO Bool
match (String -> ByteString
B.pack String
pat) (String -> ByteString
B.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]
meetCondition :: Y.Condition -> [Subst] -> IO [Subst]
meetCondition :: Condition -> [Subst] -> IO [Subst]
meetCondition Condition
_ [] = [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
meetCondition Condition
cond (Subst
subst : [Subst]
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 -> IO [Subst]
meetCondition' Condition
cond Subst
subst) :: IO (Either SomeException [Subst])
case Either SomeException [Subst]
met of
Right [Subst]
first -> do
[Subst]
next <- Condition -> [Subst] -> IO [Subst]
meetCondition Condition
cond [Subst]
rest
if [Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
first
then [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Subst]
next
else [Subst] -> IO [Subst]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Subst] -> Subst
forall a. HasCallStack => [a] -> a
head [Subst]
first Subst -> [Subst] -> [Subst]
forall a. a -> [a] -> [a]
: [Subst]
next)
Left SomeException
_ -> Condition -> [Subst] -> IO [Subst]
meetCondition Condition
cond [Subst]
rest
matchProgramWithCondition :: Expression -> Maybe Y.Condition -> Program -> IO (Maybe [Subst])
matchProgramWithCondition :: Expression -> Maybe Condition -> Program -> IO (Maybe [Subst])
matchProgramWithCondition Expression
ptn Maybe Condition
condition Program
program =
let matched :: [Subst]
matched = Expression -> Program -> [Subst]
matchProgram Expression
ptn Program
program
in if [Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
matched
then 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
else case Maybe Condition
condition of
Maybe Condition
Nothing -> Maybe [Subst] -> IO (Maybe [Subst])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Subst] -> Maybe [Subst]
forall a. a -> Maybe a
Just [Subst]
matched)
Just Condition
cond -> do
[Subst]
met <- Condition -> [Subst] -> IO [Subst]
meetCondition Condition
cond [Subst]
matched
if [Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
met
then 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
else Maybe [Subst] -> IO (Maybe [Subst])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Subst] -> Maybe [Subst]
forall a. a -> Maybe a
Just [Subst]
met)