{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}

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

module Matcher where

import AST
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (catMaybes)
import Data.Text (Text)

data MetaValue
  = MvAttribute Attribute
  | MvIndex Int
  | MvBytes Bytes
  | MvBindings [Binding]
  | MvFunction Function
  | MvExpression Expression
  deriving (MetaValue -> MetaValue -> Bool
(MetaValue -> MetaValue -> Bool)
-> (MetaValue -> MetaValue -> Bool) -> Eq MetaValue
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaValue -> MetaValue -> Bool
== :: MetaValue -> MetaValue -> Bool
$c/= :: MetaValue -> MetaValue -> Bool
/= :: MetaValue -> MetaValue -> Bool
Eq, Int -> MetaValue -> ShowS
[MetaValue] -> ShowS
MetaValue -> String
(Int -> MetaValue -> ShowS)
-> (MetaValue -> String)
-> ([MetaValue] -> ShowS)
-> Show MetaValue
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MetaValue -> ShowS
showsPrec :: Int -> MetaValue -> ShowS
$cshow :: MetaValue -> String
show :: MetaValue -> String
$cshowList :: [MetaValue] -> ShowS
showList :: [MetaValue] -> ShowS
Show)

data Meta
  = Named Text
  | Anon Slot
  deriving (Meta -> Meta -> Bool
(Meta -> Meta -> Bool) -> (Meta -> Meta -> Bool) -> Eq Meta
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Meta -> Meta -> Bool
== :: Meta -> Meta -> Bool
$c/= :: Meta -> Meta -> Bool
/= :: Meta -> Meta -> Bool
Eq, Eq Meta
Eq Meta =>
(Meta -> Meta -> Ordering)
-> (Meta -> Meta -> Bool)
-> (Meta -> Meta -> Bool)
-> (Meta -> Meta -> Bool)
-> (Meta -> Meta -> Bool)
-> (Meta -> Meta -> Meta)
-> (Meta -> Meta -> Meta)
-> Ord Meta
Meta -> Meta -> Bool
Meta -> Meta -> Ordering
Meta -> Meta -> Meta
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Meta -> Meta -> Ordering
compare :: Meta -> Meta -> Ordering
$c< :: Meta -> Meta -> Bool
< :: Meta -> Meta -> Bool
$c<= :: Meta -> Meta -> Bool
<= :: Meta -> Meta -> Bool
$c> :: Meta -> Meta -> Bool
> :: Meta -> Meta -> Bool
$c>= :: Meta -> Meta -> Bool
>= :: Meta -> Meta -> Bool
$cmax :: Meta -> Meta -> Meta
max :: Meta -> Meta -> Meta
$cmin :: Meta -> Meta -> Meta
min :: Meta -> Meta -> Meta
Ord, Int -> Meta -> ShowS
[Meta] -> ShowS
Meta -> String
(Int -> Meta -> ShowS)
-> (Meta -> String) -> ([Meta] -> ShowS) -> Show Meta
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Meta -> ShowS
showsPrec :: Int -> Meta -> ShowS
$cshow :: Meta -> String
show :: Meta -> String
$cshowList :: [Meta] -> ShowS
showList :: [Meta] -> ShowS
Show)

newtype Subst = Subst (Map Meta MetaValue)
  deriving (Subst -> Subst -> Bool
(Subst -> Subst -> Bool) -> (Subst -> Subst -> Bool) -> Eq Subst
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Subst -> Subst -> Bool
== :: Subst -> Subst -> Bool
$c/= :: Subst -> Subst -> Bool
/= :: Subst -> Subst -> Bool
Eq, Int -> Subst -> ShowS
[Subst] -> ShowS
Subst -> String
(Int -> Subst -> ShowS)
-> (Subst -> String) -> ([Subst] -> ShowS) -> Show Subst
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Subst -> ShowS
showsPrec :: Int -> Subst -> ShowS
$cshow :: Subst -> String
show :: Subst -> String
$cshowList :: [Subst] -> ShowS
showList :: [Subst] -> ShowS
Show)

type MatchExpressionFunc = Expression -> Expression -> [Subst]

substEmpty :: Subst
substEmpty :: Subst
substEmpty = Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
forall k a. Map k a
Map.empty

substSingle :: Text -> MetaValue -> Subst
substSingle :: Text -> MetaValue -> Subst
substSingle Text
key MetaValue
value = Map Meta MetaValue -> Subst
Subst (Meta -> MetaValue -> Map Meta MetaValue
forall k a. k -> a -> Map k a
Map.singleton (Text -> Meta
Named Text
key) MetaValue
value)

substSlot :: Slot -> MetaValue -> Subst
substSlot :: Slot -> MetaValue -> Subst
substSlot Slot
slot MetaValue
value = Map Meta MetaValue -> Subst
Subst (Meta -> MetaValue -> Map Meta MetaValue
forall k a. k -> a -> Map k a
Map.singleton (Slot -> Meta
Anon Slot
slot) MetaValue
value)

combine :: Subst -> Subst -> Maybe Subst
combine :: Subst -> Subst -> Maybe Subst
combine (Subst Map Meta MetaValue
a) (Subst Map Meta MetaValue
b) = [(Meta, MetaValue)] -> Map Meta MetaValue -> Maybe Subst
go (Map Meta MetaValue -> [(Meta, MetaValue)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Meta MetaValue
b) Map Meta MetaValue
a
  where
    go :: [(Meta, MetaValue)] -> Map Meta MetaValue -> Maybe Subst
    go :: [(Meta, MetaValue)] -> Map Meta MetaValue -> Maybe Subst
go [] Map Meta MetaValue
acc = Subst -> Maybe Subst
forall a. a -> Maybe a
Just (Map Meta MetaValue -> Subst
Subst Map Meta MetaValue
acc)
    go ((Meta
key, MetaValue
value) : [(Meta, MetaValue)]
rest) Map Meta MetaValue
acc = case Meta -> Map Meta MetaValue -> Maybe MetaValue
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Meta
key Map Meta MetaValue
acc of
      Just MetaValue
found
        | MetaValue
found MetaValue -> MetaValue -> Bool
forall a. Eq a => a -> a -> Bool
== MetaValue
value -> [(Meta, MetaValue)] -> Map Meta MetaValue -> Maybe Subst
go [(Meta, MetaValue)]
rest Map Meta MetaValue
acc
        | Bool
otherwise -> Maybe Subst
forall a. Maybe a
Nothing
      Maybe MetaValue
Nothing -> [(Meta, MetaValue)] -> Map Meta MetaValue -> Maybe Subst
go [(Meta, MetaValue)]
rest (Meta -> MetaValue -> Map Meta MetaValue -> Map Meta MetaValue
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Meta
key MetaValue
value Map Meta MetaValue
acc)

combineMany :: [Subst] -> [Subst] -> [Subst]
combineMany :: [Subst] -> [Subst] -> [Subst]
combineMany [Subst]
xs [Subst]
xy = [Maybe Subst] -> [Subst]
forall a. [Maybe a] -> [a]
catMaybes [Subst -> Subst -> Maybe Subst
combine Subst
x Subst
y | Subst
x <- [Subst]
xs, Subst
y <- [Subst]
xy]

matchAttribute :: Attribute -> Attribute -> [Subst]
matchAttribute :: Attribute -> Attribute -> [Subst]
matchAttribute (AtMeta Text
meta) Attribute
tgt = [Text -> MetaValue -> Subst
substSingle Text
meta (Attribute -> MetaValue
MvAttribute Attribute
tgt)]
matchAttribute (AtAny Slot
slot) Attribute
tgt = [Slot -> MetaValue -> Subst
substSlot Slot
slot (Attribute -> MetaValue
MvAttribute Attribute
tgt)]
matchAttribute Attribute
ptn Attribute
tgt
  | Attribute
ptn Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
tgt = [Subst
substEmpty]
  | Bool
otherwise = []

matchAlpha :: Alpha -> Alpha -> [Subst]
matchAlpha :: Alpha -> Alpha -> [Subst]
matchAlpha (AlMeta Text
meta) (Alpha Int
idx) = [Text -> MetaValue -> Subst
substSingle Text
meta (Int -> MetaValue
MvIndex Int
idx)]
matchAlpha (AlAny Slot
slot) (Alpha Int
idx) = [Slot -> MetaValue -> Subst
substSlot Slot
slot (Int -> MetaValue
MvIndex Int
idx)]
matchAlpha Alpha
ptn Alpha
tgt
  | Alpha
ptn Alpha -> Alpha -> Bool
forall a. Eq a => a -> a -> Bool
== Alpha
tgt = [Subst
substEmpty]
  | Bool
otherwise = []

matchFunction :: Function -> Function -> [Subst]
matchFunction :: Function -> Function -> [Subst]
matchFunction (FnMeta Text
meta) Function
tgt
  | Function -> Bool
named Function
tgt = [Text -> MetaValue -> Subst
substSingle Text
meta (Function -> MetaValue
MvFunction Function
tgt)]
matchFunction (FnAny Slot
slot) Function
tgt
  | Function -> Bool
named Function
tgt = [Slot -> MetaValue -> Subst
substSlot Slot
slot (Function -> MetaValue
MvFunction Function
tgt)]
matchFunction Function
ptn Function
tgt
  | Function
ptn Function -> Function -> Bool
forall a. Eq a => a -> a -> Bool
== Function
tgt = [Subst
substEmpty]
  | Bool
otherwise = []

named :: Function -> Bool
named :: Function -> Bool
named (Function Text
_) = Bool
True
named (FnSymbol Int
_) = Bool
True
named Function
_ = Bool
False

matchBinding :: Binding -> Binding -> [Subst]
matchBinding :: Binding -> Binding -> [Subst]
matchBinding (BiVoid Attribute
pattr) (BiVoid Attribute
tattr) = Attribute -> Attribute -> [Subst]
matchAttribute Attribute
pattr Attribute
tattr
matchBinding (BiDelta (BtMeta Text
meta)) (BiDelta Bytes
tdata) = [Text -> MetaValue -> Subst
substSingle Text
meta (Bytes -> MetaValue
MvBytes Bytes
tdata)]
matchBinding (BiDelta (BtAny Slot
slot)) (BiDelta Bytes
tdata) = [Slot -> MetaValue -> Subst
substSlot Slot
slot (Bytes -> MetaValue
MvBytes Bytes
tdata)]
matchBinding (BiDelta Bytes
pdata) (BiDelta Bytes
tdata)
  | Bytes
pdata Bytes -> Bytes -> Bool
forall a. Eq a => a -> a -> Bool
== Bytes
tdata = [Subst
substEmpty]
  | Bool
otherwise = []
matchBinding (BiLambda Function
pFunc) (BiLambda Function
tFunc) = Function -> Function -> [Subst]
matchFunction Function
pFunc Function
tFunc
matchBinding (BiTau Attribute
pattr Expression
pexp) (BiTau Attribute
tattr Expression
texp) = [Subst] -> [Subst] -> [Subst]
combineMany (Attribute -> Attribute -> [Subst]
matchAttribute Attribute
pattr Attribute
tattr) (MatchExpressionFunc
matchExpression' Expression
pexp Expression
texp)
matchBinding Binding
_ Binding
_ = []

matchArgument :: Argument -> Argument -> [Subst]
matchArgument :: Argument -> Argument -> [Subst]
matchArgument (ArTau Attribute
pattr Expression
pexp) (ArTau Attribute
tattr Expression
texp) = [Subst] -> [Subst] -> [Subst]
combineMany (Attribute -> Attribute -> [Subst]
matchAttribute Attribute
pattr Attribute
tattr) (MatchExpressionFunc
matchExpression' Expression
pexp Expression
texp)
matchArgument (ArAlpha Alpha
palpha Expression
pexp) (ArAlpha Alpha
talpha Expression
texp) = [Subst] -> [Subst] -> [Subst]
combineMany (Alpha -> Alpha -> [Subst]
matchAlpha Alpha
palpha Alpha
talpha) (MatchExpressionFunc
matchExpression' Expression
pexp Expression
texp)
matchArgument Argument
_ Argument
_ = []

matchBindings :: [Binding] -> [Binding] -> [Subst]
matchBindings :: [Binding] -> [Binding] -> [Subst]
matchBindings [] [] = [Subst
substEmpty]
matchBindings [] [Binding]
_ = []
matchBindings ((BiMeta Text
name) : [Binding]
pbs) [Binding]
tbs = (MetaValue -> Subst) -> [Binding] -> [Binding] -> [Subst]
matchBindingsMeta (Text -> MetaValue -> Subst
substSingle Text
name) [Binding]
pbs [Binding]
tbs
matchBindings ((BiAny Slot
slot) : [Binding]
pbs) [Binding]
tbs = (MetaValue -> Subst) -> [Binding] -> [Binding] -> [Subst]
matchBindingsMeta (Slot -> MetaValue -> Subst
substSlot Slot
slot) [Binding]
pbs [Binding]
tbs
matchBindings (Binding
pb : [Binding]
pbs) (Binding
tb : [Binding]
tbs) = [Subst] -> [Subst] -> [Subst]
combineMany (Binding -> Binding -> [Subst]
matchBinding Binding
pb Binding
tb) ([Binding] -> [Binding] -> [Subst]
matchBindings [Binding]
pbs [Binding]
tbs)
matchBindings [Binding]
_ [Binding]
_ = []

matchBindingsMeta :: (MetaValue -> Subst) -> [Binding] -> [Binding] -> [Subst]
matchBindingsMeta :: (MetaValue -> Subst) -> [Binding] -> [Binding] -> [Subst]
matchBindingsMeta MetaValue -> Subst
bind [] [Binding]
tbs = [MetaValue -> Subst
bind ([Binding] -> MetaValue
MvBindings [Binding]
tbs)]
matchBindingsMeta MetaValue -> Subst
bind [Binding]
pbs [Binding]
tbs = [Binding] -> [Binding] -> [Subst]
go [] [Binding]
tbs
  where
    go :: [Binding] -> [Binding] -> [Subst]
    go :: [Binding] -> [Binding] -> [Subst]
go [Binding]
before [Binding]
after =
      [Maybe Subst] -> [Subst]
forall a. [Maybe a] -> [a]
catMaybes [Subst -> Subst -> Maybe Subst
combine (MetaValue -> Subst
bind ([Binding] -> MetaValue
MvBindings ([Binding] -> [Binding]
forall a. [a] -> [a]
reverse [Binding]
before))) Subst
subst | Subst
subst <- [Binding] -> [Binding] -> [Subst]
matchBindings [Binding]
pbs [Binding]
after]
        [Subst] -> [Subst] -> [Subst]
forall a. [a] -> [a] -> [a]
++ case [Binding]
after of
          [] -> []
          (Binding
tb : [Binding]
rest) -> [Binding] -> [Binding] -> [Subst]
go (Binding
tb Binding -> [Binding] -> [Binding]
forall a. a -> [a] -> [a]
: [Binding]
before) [Binding]
rest

matchExpression' :: MatchExpressionFunc
matchExpression' :: MatchExpressionFunc
matchExpression' (ExMeta Text
meta) Expression
tgt = [Text -> MetaValue -> Subst
substSingle Text
meta (Expression -> MetaValue
MvExpression Expression
tgt)]
matchExpression' (ExAny Slot
slot) Expression
tgt = [Slot -> MetaValue -> Subst
substSlot Slot
slot (Expression -> MetaValue
MvExpression Expression
tgt)]
matchExpression' Expression
ExXi Expression
ExXi = [Subst
substEmpty]
matchExpression' Expression
ExRoot Expression
ExRoot = [Subst
substEmpty]
matchExpression' Expression
ExTermination Expression
ExTermination = [Subst
substEmpty]
matchExpression' (ExFormation [Binding]
pbs) (ExFormation [Binding]
tbs) = [Binding] -> [Binding] -> [Subst]
matchBindings [Binding]
pbs [Binding]
tbs
matchExpression' (ExDispatch Expression
pexp Attribute
pattr) (ExDispatch Expression
texp Attribute
tattr) = [Subst] -> [Subst] -> [Subst]
combineMany (Attribute -> Attribute -> [Subst]
matchAttribute Attribute
pattr Attribute
tattr) (MatchExpressionFunc
matchExpression' (Attribute -> Attribute -> Expression -> Expression
pinned Attribute
pattr Attribute
tattr Expression
pexp) Expression
texp)
matchExpression' (ExApplication Expression
pexp parg :: Argument
parg@(ArTau Attribute
pattr Expression
_)) (ExApplication Expression
texp targ :: Argument
targ@(ArTau Attribute
tattr Expression
_)) = [Subst] -> [Subst] -> [Subst]
combineMany (MatchExpressionFunc
matchExpression' (Attribute -> Attribute -> Expression -> Expression
pinned Attribute
pattr Attribute
tattr Expression
pexp) Expression
texp) (Argument -> Argument -> [Subst]
matchArgument Argument
parg Argument
targ)
matchExpression' (ExApplication Expression
pexp Argument
parg) (ExApplication Expression
texp Argument
targ) = [Subst] -> [Subst] -> [Subst]
combineMany (MatchExpressionFunc
matchExpression' Expression
pexp Expression
texp) (Argument -> Argument -> [Subst]
matchArgument Argument
parg Argument
targ)
matchExpression' (ExPhiAgain Maybe String
prefix Int
idx Expression
expr) (ExPhiAgain Maybe String
prefix' Int
idx' Expression
expr')
  | Maybe String
prefix Maybe String -> Maybe String -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe String
prefix' Bool -> Bool -> Bool
&& Int
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
idx' = MatchExpressionFunc
matchExpression' Expression
expr Expression
expr'
  | Bool
otherwise = []
matchExpression' (ExPhiMeet Maybe String
prefix Int
idx Expression
expr) (ExPhiMeet Maybe String
prefix' Int
idx' Expression
expr')
  | Maybe String
prefix Maybe String -> Maybe String -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe String
prefix' Bool -> Bool -> Bool
&& Int
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
idx' = MatchExpressionFunc
matchExpression' Expression
expr Expression
expr'
  | Bool
otherwise = []
matchExpression' Expression
_ Expression
_ = []

pinned :: Attribute -> Attribute -> Expression -> Expression
pinned :: Attribute -> Attribute -> Expression -> Expression
pinned (AtMeta Text
meta) Attribute
tattr = Expression -> Expression
goExpr
  where
    goExpr :: Expression -> Expression
    goExpr :: Expression -> Expression
goExpr (ExFormation [Binding]
bds) = [Binding] -> Expression
ExFormation ((Binding -> Binding) -> [Binding] -> [Binding]
forall a b. (a -> b) -> [a] -> [b]
map Binding -> Binding
goBinding [Binding]
bds)
    goExpr (ExDispatch Expression
expr Attribute
attr) = Expression -> Attribute -> Expression
ExDispatch (Expression -> Expression
goExpr Expression
expr) (Attribute -> Attribute
goAttribute Attribute
attr)
    goExpr (ExApplication Expression
expr (ArTau Attribute
attr Expression
arg)) = Expression -> Argument -> Expression
ExApplication (Expression -> Expression
goExpr Expression
expr) (Attribute -> Expression -> Argument
ArTau (Attribute -> Attribute
goAttribute Attribute
attr) (Expression -> Expression
goExpr Expression
arg))
    goExpr (ExApplication Expression
expr (ArAlpha Alpha
alpha Expression
arg)) = Expression -> Argument -> Expression
ExApplication (Expression -> Expression
goExpr Expression
expr) (Alpha -> Expression -> Argument
ArAlpha Alpha
alpha (Expression -> Expression
goExpr Expression
arg))
    goExpr Expression
expr = Expression
expr
    goBinding :: Binding -> Binding
    goBinding :: Binding -> Binding
goBinding (BiTau Attribute
attr Expression
expr) = Attribute -> Expression -> Binding
BiTau (Attribute -> Attribute
goAttribute Attribute
attr) (Expression -> Expression
goExpr Expression
expr)
    goBinding (BiVoid Attribute
attr) = Attribute -> Binding
BiVoid (Attribute -> Attribute
goAttribute Attribute
attr)
    goBinding Binding
bd = Binding
bd
    goAttribute :: Attribute -> Attribute
    goAttribute :: Attribute -> Attribute
goAttribute (AtMeta Text
meta')
      | Text
meta' Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
meta = Attribute
tattr
    goAttribute Attribute
attr = Attribute
attr
pinned Attribute
_ Attribute
_ = Expression -> Expression
forall a. a -> a
id

matchExpressionDeep :: MatchExpressionFunc
matchExpressionDeep :: MatchExpressionFunc
matchExpressionDeep = Bool -> MatchExpressionFunc
matchExpressionDeep' Bool
False

matchExpressionDeep' :: Bool -> MatchExpressionFunc
matchExpressionDeep' :: Bool -> MatchExpressionFunc
matchExpressionDeep' Bool
redex Expression
ptn Expression
tgt = Expression -> [Subst] -> [Subst]
go Expression
tgt []
  where
    go :: Expression -> [Subst] -> [Subst]
    go :: Expression -> [Subst] -> [Subst]
go Expression
expr [Subst]
rest
      | Bool
redex Bool -> Bool -> Bool
&& Expression -> Bool
inert Expression
expr = [Subst]
rest
      | Expression -> Expression -> Bool
fitting Expression
ptn Expression
expr = MatchExpressionFunc
matchExpression' Expression
ptn Expression
expr [Subst] -> [Subst] -> [Subst]
forall a. [a] -> [a] -> [a]
++ Expression -> [Subst] -> [Subst]
below Expression
expr [Subst]
rest
      | Bool
otherwise = Expression -> [Subst] -> [Subst]
below Expression
expr [Subst]
rest
    below :: Expression -> [Subst] -> [Subst]
    below :: Expression -> [Subst] -> [Subst]
below (ExFormation [Binding]
bds) [Subst]
rest = (Binding -> [Subst] -> [Subst]) -> [Subst] -> [Binding] -> [Subst]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding -> [Subst] -> [Subst]
inside [Subst]
rest [Binding]
bds
    below (ExDispatch Expression
expr Attribute
_) [Subst]
rest = Expression -> [Subst] -> [Subst]
go Expression
expr [Subst]
rest
    below (ExApplication Expression
expr (ArTau Attribute
_ Expression
arg)) [Subst]
rest = Expression -> [Subst] -> [Subst]
go Expression
expr (Expression -> [Subst] -> [Subst]
go Expression
arg [Subst]
rest)
    below (ExApplication Expression
expr (ArAlpha Alpha
_ Expression
arg)) [Subst]
rest = Expression -> [Subst] -> [Subst]
go Expression
expr (Expression -> [Subst] -> [Subst]
go Expression
arg [Subst]
rest)
    below Expression
_ [Subst]
rest = [Subst]
rest
    inside :: Binding -> [Subst] -> [Subst]
    inside :: Binding -> [Subst] -> [Subst]
inside (BiTau Attribute
_ Expression
expr) [Subst]
rest = Expression -> [Subst] -> [Subst]
go Expression
expr [Subst]
rest
    inside Binding
_ [Subst]
rest = [Subst]
rest

matchExpression :: MatchExpressionFunc
matchExpression :: MatchExpressionFunc
matchExpression = MatchExpressionFunc
matchExpressionDeep

reachable :: Expression -> Expression -> Bool
reachable :: Expression -> Expression -> Bool
reachable = Bool -> Expression -> Expression -> Bool
reachable' Bool
False

reachable' :: Bool -> Expression -> Expression -> Bool
reachable' :: Bool -> Expression -> Expression -> Bool
reachable' Bool
redex Expression
ptn = Expression -> Bool
go
  where
    go :: Expression -> Bool
    go :: Expression -> Bool
go Expression
tgt
      | Bool
redex Bool -> Bool -> Bool
&& Expression -> Bool
inert Expression
tgt = Bool
False
      | Bool
otherwise =
          Expression -> Expression -> Bool
fitting Expression
ptn Expression
tgt Bool -> Bool -> Bool
|| case Expression
tgt of
            ExFormation [Binding]
bds -> (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Binding -> Bool
inside [Binding]
bds
            ExDispatch Expression
expr Attribute
_ -> Expression -> Bool
go Expression
expr
            ExApplication Expression
expr (ArTau Attribute
_ Expression
arg) -> Expression -> Bool
go Expression
expr Bool -> Bool -> Bool
|| Expression -> Bool
go Expression
arg
            ExApplication Expression
expr (ArAlpha Alpha
_ Expression
arg) -> Expression -> Bool
go Expression
expr Bool -> Bool -> Bool
|| Expression -> Bool
go Expression
arg
            Expression
_ -> Bool
False
    inside :: Binding -> Bool
    inside :: Binding -> Bool
inside (BiTau Attribute
_ Expression
expr) = Expression -> Bool
go Expression
expr
    inside Binding
_ = Bool
False

fitting :: Expression -> Expression -> Bool
fitting :: Expression -> Expression -> Bool
fitting = Expression -> Expression -> Bool
go
  where
    go :: Expression -> Expression -> Bool
    go :: Expression -> Expression -> Bool
go (ExMeta Text
_) Expression
_ = Bool
True
    go (ExAny Slot
_) Expression
_ = Bool
True
    go Expression
ExXi Expression
ExXi = Bool
True
    go Expression
ExRoot Expression
ExRoot = Bool
True
    go Expression
ExTermination Expression
ExTermination = Bool
True
    go (ExFormation [Binding]
pbs) (ExFormation [Binding]
tbs) = (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Binding
pbd -> Binding -> Bool
loose Binding
pbd Bool -> Bool -> Bool
|| (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Binding -> Binding -> Bool
kin Binding
pbd) [Binding]
tbs) [Binding]
pbs
    go (ExDispatch Expression
pexp Attribute
pattr) (ExDispatch Expression
texp Attribute
tattr) = Attribute -> Attribute -> Bool
same Attribute
pattr Attribute
tattr Bool -> Bool -> Bool
&& Expression -> Expression -> Bool
go Expression
pexp Expression
texp
    go (ExApplication Expression
pexp (ArTau Attribute
pattr Expression
_)) (ExApplication Expression
texp (ArTau Attribute
tattr Expression
_)) = Attribute -> Attribute -> Bool
same Attribute
pattr Attribute
tattr Bool -> Bool -> Bool
&& Expression -> Expression -> Bool
go Expression
pexp Expression
texp
    go (ExApplication Expression
pexp (ArAlpha Alpha
_ Expression
_)) (ExApplication Expression
texp (ArAlpha Alpha
_ Expression
_)) = Expression -> Expression -> Bool
go Expression
pexp Expression
texp
    go (ExPhiAgain{}) (ExPhiAgain{}) = Bool
True
    go (ExPhiMeet{}) (ExPhiMeet{}) = Bool
True
    go Expression
_ Expression
_ = Bool
False
    loose :: Binding -> Bool
    loose :: Binding -> Bool
loose (BiMeta Text
_) = Bool
True
    loose (BiAny Slot
_) = Bool
True
    loose Binding
_ = Bool
False
    kin :: Binding -> Binding -> Bool
    kin :: Binding -> Binding -> Bool
kin (BiTau Attribute
pattr Expression
_) (BiTau Attribute
tattr Expression
_) = Attribute -> Attribute -> Bool
same Attribute
pattr Attribute
tattr
    kin (BiVoid Attribute
pattr) (BiVoid Attribute
tattr) = Attribute -> Attribute -> Bool
same Attribute
pattr Attribute
tattr
    kin (BiLambda Function
_) (BiLambda Function
_) = Bool
True
    kin (BiDelta Bytes
_) (BiDelta Bytes
_) = Bool
True
    kin Binding
_ Binding
_ = Bool
False
    same :: Attribute -> Attribute -> Bool
    same :: Attribute -> Attribute -> Bool
same (AtMeta Text
_) Attribute
_ = Bool
True
    same (AtAny Slot
_) Attribute
_ = Bool
True
    same Attribute
pattr Attribute
tattr = Attribute
pattr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
tattr

sites :: forall a. Bool -> (Expression -> [a]) -> Expression -> [(Expression, a)]
sites :: forall a.
Bool -> (Expression -> [a]) -> Expression -> [(Expression, a)]
sites Bool
redex Expression -> [a]
rule Expression
tgt = Expression -> [(Expression, a)] -> [(Expression, a)]
go Expression
tgt []
  where
    go :: Expression -> [(Expression, a)] -> [(Expression, a)]
    go :: Expression -> [(Expression, a)] -> [(Expression, a)]
go Expression
expr [(Expression, a)]
rest
      | Bool
redex Bool -> Bool -> Bool
&& Expression -> Bool
inert Expression
expr = [(Expression, a)]
rest
      | Bool
otherwise = (a -> (Expression, a)) -> [a] -> [(Expression, a)]
forall a b. (a -> b) -> [a] -> [b]
map (Expression
expr,) (Expression -> [a]
rule Expression
expr) [(Expression, a)] -> [(Expression, a)] -> [(Expression, a)]
forall a. [a] -> [a] -> [a]
++ Expression -> [(Expression, a)] -> [(Expression, a)]
below Expression
expr [(Expression, a)]
rest
    below :: Expression -> [(Expression, a)] -> [(Expression, a)]
    below :: Expression -> [(Expression, a)] -> [(Expression, a)]
below (ExFormation [Binding]
bds) [(Expression, a)]
rest = (Binding -> [(Expression, a)] -> [(Expression, a)])
-> [(Expression, a)] -> [Binding] -> [(Expression, a)]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding -> [(Expression, a)] -> [(Expression, a)]
inside [(Expression, a)]
rest [Binding]
bds
    below (ExDispatch Expression
expr Attribute
_) [(Expression, a)]
rest = Expression -> [(Expression, a)] -> [(Expression, a)]
go Expression
expr [(Expression, a)]
rest
    below (ExApplication Expression
expr (ArTau Attribute
_ Expression
arg)) [(Expression, a)]
rest = Expression -> [(Expression, a)] -> [(Expression, a)]
go Expression
expr (Expression -> [(Expression, a)] -> [(Expression, a)]
go Expression
arg [(Expression, a)]
rest)
    below (ExApplication Expression
expr (ArAlpha Alpha
_ Expression
arg)) [(Expression, a)]
rest = Expression -> [(Expression, a)] -> [(Expression, a)]
go Expression
expr (Expression -> [(Expression, a)] -> [(Expression, a)]
go Expression
arg [(Expression, a)]
rest)
    below Expression
_ [(Expression, a)]
rest = [(Expression, a)]
rest
    inside :: Binding -> [(Expression, a)] -> [(Expression, a)]
    inside :: Binding -> [(Expression, a)] -> [(Expression, a)]
inside (BiTau Attribute
_ Expression
expr) [(Expression, a)]
rest = Expression -> [(Expression, a)] -> [(Expression, a)]
go Expression
expr [(Expression, a)]
rest
    inside Binding
_ [(Expression, a)]
rest = [(Expression, a)]
rest

hits :: forall a. [(Int, Bool, Maybe Expression -> Expression -> [a])] -> Maybe Expression -> Expression -> [Int]
hits :: forall a.
[(Int, Bool, Maybe Expression -> Expression -> [a])]
-> Maybe Expression -> Expression -> [Int]
hits [(Int, Bool, Maybe Expression -> Expression -> [a])]
rules Maybe Expression
universe Expression
tgt = [Expression]
-> [(Int, Bool, Maybe Expression -> Expression -> [a])] -> [Int]
go [Expression
tgt] [(Int, Bool, Maybe Expression -> Expression -> [a])]
rules
  where
    go :: [Expression] -> [(Int, Bool, Maybe Expression -> Expression -> [a])] -> [Int]
    go :: [Expression]
-> [(Int, Bool, Maybe Expression -> Expression -> [a])] -> [Int]
go [] [(Int, Bool, Maybe Expression -> Expression -> [a])]
_ = []
    go [Expression]
_ [] = []
    go (Expression
expr : [Expression]
rest) [(Int, Bool, Maybe Expression -> Expression -> [a])]
pending
      | Expression -> Bool
inert Expression
expr Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool
redex | (Int
_, Bool
redex, Maybe Expression -> Expression -> [a]
_) <- [(Int, Bool, Maybe Expression -> Expression -> [a])]
pending] = [Expression]
-> [(Int, Bool, Maybe Expression -> Expression -> [a])] -> [Int]
go [Expression]
rest [(Int, Bool, Maybe Expression -> Expression -> [a])]
pending
      | Bool
otherwise = case [Int
idx | (Int
idx, Bool
redex, Maybe Expression -> Expression -> [a]
rule) <- [(Int, Bool, Maybe Expression -> Expression -> [a])]
pending, Bool -> Bool
not (Bool
redex Bool -> Bool -> Bool
&& Expression -> Bool
inert Expression
expr), Bool -> Bool
not ([a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Maybe Expression -> Expression -> [a]
rule Maybe Expression
universe Expression
expr))] of
          [] -> [Expression]
-> [(Int, Bool, Maybe Expression -> Expression -> [a])] -> [Int]
go (Expression -> [Expression] -> [Expression]
below Expression
expr [Expression]
rest) [(Int, Bool, Maybe Expression -> Expression -> [a])]
pending
          [Int]
met -> [Int]
met [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Expression]
-> [(Int, Bool, Maybe Expression -> Expression -> [a])] -> [Int]
go (Expression -> [Expression] -> [Expression]
below Expression
expr [Expression]
rest) [(Int, Bool, Maybe Expression -> Expression -> [a])
rule | rule :: (Int, Bool, Maybe Expression -> Expression -> [a])
rule@(Int
idx, Bool
_, Maybe Expression -> Expression -> [a]
_) <- [(Int, Bool, Maybe Expression -> Expression -> [a])]
pending, Int
idx Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Int]
met]
    below :: Expression -> [Expression] -> [Expression]
    below :: Expression -> [Expression] -> [Expression]
below (ExFormation [Binding]
bds) [Expression]
rest = (Binding -> [Expression] -> [Expression])
-> [Expression] -> [Binding] -> [Expression]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding -> [Expression] -> [Expression]
inside [Expression]
rest [Binding]
bds
    below (ExDispatch Expression
expr Attribute
_) [Expression]
rest = Expression
expr Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression]
rest
    below (ExApplication Expression
expr (ArTau Attribute
_ Expression
arg)) [Expression]
rest = Expression
expr Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: Expression
arg Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression]
rest
    below (ExApplication Expression
expr (ArAlpha Alpha
_ Expression
arg)) [Expression]
rest = Expression
expr Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: Expression
arg Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression]
rest
    below Expression
_ [Expression]
rest = [Expression]
rest
    inside :: Binding -> [Expression] -> [Expression]
    inside :: Binding -> [Expression] -> [Expression]
inside (BiTau Attribute
_ Expression
expr) [Expression]
rest = Expression
expr Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression]
rest
    inside Binding
_ [Expression]
rest = [Expression]
rest

splits :: [Binding] -> [([Binding], [Binding])]
splits :: [Binding] -> [([Binding], [Binding])]
splits = [Binding] -> [Binding] -> [([Binding], [Binding])]
go []
  where
    go :: [Binding] -> [Binding] -> [([Binding], [Binding])]
    go :: [Binding] -> [Binding] -> [([Binding], [Binding])]
go [Binding]
before [Binding]
after =
      ([Binding] -> [Binding]
forall a. [a] -> [a]
reverse [Binding]
before, [Binding]
after) ([Binding], [Binding])
-> [([Binding], [Binding])] -> [([Binding], [Binding])]
forall a. a -> [a] -> [a]
: case [Binding]
after of
        [] -> []
        (Binding
bd : [Binding]
rest) -> [Binding] -> [Binding] -> [([Binding], [Binding])]
go (Binding
bd Binding -> [Binding] -> [Binding]
forall a. a -> [a] -> [a]
: [Binding]
before) [Binding]
rest