phino-0.0.141: src/Matcher.hs

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

-- The goal of the module is to traverse given AST and build substitutions
-- from meta variables to appropriate meta values
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)

-- Meta value
-- The right part of substitution
data MetaValue
  = MvAttribute Attribute -- !t
  | MvIndex Int -- α𝑖
  | MvBytes Bytes -- !b
  | MvBindings [Binding] -- !B
  | MvFunction Function -- !F
  | MvExpression Expression -- !e
  deriving (Eq, Show)

-- The left-hand side of a substitution: a meta-variable the rule author named
-- and may reference from a result, or an anonymous slot that only the pattern
-- it was written in can address
data Meta
  = Named Text
  | Anon Slot
  deriving (Eq, Ord, Show)

-- Substitution
-- Shows the match of meta variable to meta value
newtype Subst = Subst (Map Meta MetaValue)
  deriving (Eq, Show)

-- A way to match a pattern expression against a target expression, yielding
-- the substitutions under which they agree.
type MatchExpressionFunc = Expression -> Expression -> [Subst]

-- Empty substitution
substEmpty :: Subst
substEmpty = Subst Map.empty

-- Singleton substitution with one (key -> value) pair
substSingle :: Text -> MetaValue -> Subst
substSingle key value = Subst (Map.singleton (Named key) value)

-- Singleton substitution binding one anonymous slot
substSlot :: Slot -> MetaValue -> Subst
substSlot slot value = Subst (Map.singleton (Anon slot) value)

-- Combine two substitutions into a single one
-- Fails if values by the same keys are not equal
combine :: Subst -> Subst -> Maybe Subst
combine (Subst a) (Subst b) = go (Map.toList b) a
  where
    go :: [(Meta, MetaValue)] -> Map Meta MetaValue -> Maybe Subst
    go [] acc = Just (Subst acc)
    go ((key, value) : rest) acc = case Map.lookup key acc of
      Just found
        | found == value -> go rest acc
        | otherwise -> Nothing
      Nothing -> go rest (Map.insert key value acc)

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

matchAttribute :: Attribute -> Attribute -> [Subst]
matchAttribute (AtMeta meta) tgt = [substSingle meta (MvAttribute tgt)]
matchAttribute (AtAny slot) tgt = [substSlot slot (MvAttribute tgt)]
matchAttribute ptn tgt
  | ptn == tgt = [substEmpty]
  | otherwise = []

matchAlpha :: Alpha -> Alpha -> [Subst]
matchAlpha (AlMeta meta) (Alpha idx) = [substSingle meta (MvIndex idx)]
matchAlpha (AlAny slot) (Alpha idx) = [substSlot slot (MvIndex idx)]
matchAlpha ptn tgt
  | ptn == tgt = [substEmpty]
  | otherwise = []

-- A λ meta stands for any λ name at all — an ordinary one and a symbol alike,
-- since a symbol is a name nothing answers and not a variable of the rule
-- language (see 'FnSymbol'). Every other pair matches only itself.
matchFunction :: Function -> Function -> [Subst]
matchFunction (FnMeta meta) tgt
  | named tgt = [substSingle meta (MvFunction tgt)]
matchFunction (FnAny slot) tgt
  | named tgt = [substSlot slot (MvFunction tgt)]
matchFunction ptn tgt
  | ptn == tgt = [substEmpty]
  | otherwise = []

-- Whether a λ function is a name a program wrote rather than a meta-variable
-- a rule wrote.
named :: Function -> Bool
named (Function _) = True
named (FnSymbol _) = True
named _ = False

matchBinding :: Binding -> Binding -> [Subst]
matchBinding (BiVoid pattr) (BiVoid tattr) = matchAttribute pattr tattr
matchBinding (BiDelta (BtMeta meta)) (BiDelta tdata) = [substSingle meta (MvBytes tdata)]
matchBinding (BiDelta (BtAny slot)) (BiDelta tdata) = [substSlot slot (MvBytes tdata)]
matchBinding (BiDelta pdata) (BiDelta tdata)
  | pdata == tdata = [substEmpty]
  | otherwise = []
matchBinding (BiLambda pFunc) (BiLambda tFunc) = matchFunction pFunc tFunc
matchBinding (BiTau pattr pexp) (BiTau tattr texp) = combineMany (matchAttribute pattr tattr) (matchExpression' pexp texp)
matchBinding _ _ = []

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

-- Match bindings with ordering
matchBindings :: [Binding] -> [Binding] -> [Subst]
matchBindings [] [] = [substEmpty]
matchBindings [] _ = []
matchBindings ((BiMeta name) : pbs) tbs = matchBindingsMeta (substSingle name) pbs tbs
matchBindings ((BiAny slot) : pbs) tbs = matchBindingsMeta (substSlot slot) pbs tbs
matchBindings (pb : pbs) (tb : tbs) = combineMany (matchBinding pb tb) (matchBindings pbs tbs)
matchBindings _ _ = []

-- A meta binding stands for any leading run of the target bindings, so every
-- way of splitting the target into that run and the rest is tried. The rest is
-- carried down one binding at a time instead of being cut out of the target
-- anew at every index, which is what made a formation of N bindings cost N
-- walks of itself rather than one, and the run itself is put together only
-- where the pattern after it matched, so a split the pattern throws away costs
-- nothing to name. A meta binding with nothing after it takes the whole rest in
-- one step: the pattern is out of bindings, so the only split that matches is
-- the one leaving nothing behind (#1316).
matchBindingsMeta :: (MetaValue -> Subst) -> [Binding] -> [Binding] -> [Subst]
matchBindingsMeta bind [] tbs = [bind (MvBindings tbs)]
matchBindingsMeta bind pbs tbs = go [] tbs
  where
    go :: [Binding] -> [Binding] -> [Subst]
    go before after =
      catMaybes [combine (bind (MvBindings (reverse before))) subst | subst <- matchBindings pbs after]
        ++ case after of
          [] -> []
          (tb : rest) -> go (tb : before) rest

matchExpression' :: MatchExpressionFunc
matchExpression' (ExMeta meta) tgt = [substSingle meta (MvExpression tgt)]
matchExpression' (ExAny slot) tgt = [substSlot slot (MvExpression tgt)]
matchExpression' ExXi ExXi = [substEmpty]
matchExpression' ExRoot ExRoot = [substEmpty]
matchExpression' ExTermination ExTermination = [substEmpty]
matchExpression' (ExFormation pbs) (ExFormation tbs) = matchBindings pbs tbs
matchExpression' (ExDispatch pexp pattr) (ExDispatch texp tattr) = combineMany (matchAttribute pattr tattr) (matchExpression' (pinned pattr tattr pexp) texp)
matchExpression' (ExApplication pexp parg@(ArTau pattr _)) (ExApplication texp targ@(ArTau tattr _)) = combineMany (matchExpression' (pinned pattr tattr pexp) texp) (matchArgument parg targ)
matchExpression' (ExApplication pexp parg) (ExApplication texp targ) = combineMany (matchExpression' pexp texp) (matchArgument parg targ)
matchExpression' (ExPhiAgain prefix idx expr) (ExPhiAgain prefix' idx' expr')
  | prefix == prefix' && idx == idx' = matchExpression' expr expr'
  | otherwise = []
matchExpression' (ExPhiMeet prefix idx expr) (ExPhiMeet prefix' idx' expr')
  | prefix == prefix' && idx == idx' = matchExpression' expr expr'
  | otherwise = []
matchExpression' _ _ = []

-- The pattern with the attribute meta written in its place wherever the
-- meta stands in it, once the target has told which attribute that is. A
-- dispatch or an application names its attribute beside the formation it is
-- made of, as '⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧.𝜏1' does, and the formation is matched
-- first, so without it every binding of the formation would be tried as 𝜏1
-- and a substitution made for it before the attribute threw all but one away.
-- The matches are the ones the pattern has anyway, in the same order (#1453).
pinned :: Attribute -> Attribute -> Expression -> Expression
pinned (AtMeta meta) tattr = goExpr
  where
    goExpr :: Expression -> Expression
    goExpr (ExFormation bds) = ExFormation (map goBinding bds)
    goExpr (ExDispatch expr attr) = ExDispatch (goExpr expr) (goAttribute attr)
    goExpr (ExApplication expr (ArTau attr arg)) = ExApplication (goExpr expr) (ArTau (goAttribute attr) (goExpr arg))
    goExpr (ExApplication expr (ArAlpha alpha arg)) = ExApplication (goExpr expr) (ArAlpha alpha (goExpr arg))
    goExpr expr = expr
    goBinding :: Binding -> Binding
    goBinding (BiTau attr expr) = BiTau (goAttribute attr) (goExpr expr)
    goBinding (BiVoid attr) = BiVoid (goAttribute attr)
    goBinding bd = bd
    goAttribute :: Attribute -> Attribute
    goAttribute (AtMeta meta')
      | meta' == meta = tattr
    goAttribute attr = attr
pinned _ _ = id

-- Match expression with deep nested expression(s) matching
matchExpressionDeep :: MatchExpressionFunc
matchExpressionDeep = matchExpressionDeep' False

-- The same deep matching, told whether the pattern is a redex: one that
-- matches only at a place no 'inert' term holds. The matcher then never looks
-- inside an inert term, so a copy of an object an earlier normalization left
-- in normal form costs nothing to carry along, however big it is (#1453).
matchExpressionDeep' :: Bool -> MatchExpressionFunc
matchExpressionDeep' redex ptn tgt = go tgt []
  where
    go :: Expression -> [Subst] -> [Subst]
    go expr rest
      | redex && inert expr = rest
      | fitting ptn expr = matchExpression' ptn expr ++ below expr rest
      | otherwise = below expr rest
    below :: Expression -> [Subst] -> [Subst]
    below (ExFormation bds) rest = foldr inside rest bds
    below (ExDispatch expr _) rest = go expr rest
    below (ExApplication expr (ArTau _ arg)) rest = go expr (go arg rest)
    below (ExApplication expr (ArAlpha _ arg)) rest = go expr (go arg rest)
    below _ rest = rest
    inside :: Binding -> [Subst] -> [Subst]
    inside (BiTau _ expr) rest = go expr rest
    inside _ rest = rest

matchExpression :: MatchExpressionFunc
matchExpression = matchExpressionDeep

-- Whether the pattern could match at some place of the target where the deep
-- matcher looks, judged by the shape of each place alone: the constructors
-- down the head of the pattern, the attribute a dispatch or an application
-- names, and the kinds of bindings a formation of the pattern asks for. It
-- never says no where 'matchExpressionDeep' would find a match, and it walks
-- the target once without building a single substitution, so a rule whose
-- pattern fits nowhere in a term is told so without the deep matcher trying
-- it at every place of that term (#1453).
reachable :: Expression -> Expression -> Bool
reachable = reachable' False

-- The same judgement, told whether the pattern is a redex, in which case no
-- place inside an 'inert' term is looked at (see 'matchExpressionDeep'').
reachable' :: Bool -> Expression -> Expression -> Bool
reachable' redex ptn = go
  where
    go :: Expression -> Bool
    go tgt
      | redex && inert tgt = False
      | otherwise =
          fitting ptn tgt || case tgt of
            ExFormation bds -> any inside bds
            ExDispatch expr _ -> go expr
            ExApplication expr (ArTau _ arg) -> go expr || go arg
            ExApplication expr (ArAlpha _ arg) -> go expr || go arg
            _ -> False
    inside :: Binding -> Bool
    inside (BiTau _ expr) = go expr
    inside _ = False

-- Whether the pattern could match the target right at its root, judged by
-- shape alone: the constructors down the head of the pattern, the attribute a
-- dispatch or an application names, and the kinds of bindings a formation of
-- the pattern asks for. It never says no where 'matchExpression'' would find
-- a match (#1453).
fitting :: Expression -> Expression -> Bool
fitting = go
  where
    go :: Expression -> Expression -> Bool
    go (ExMeta _) _ = True
    go (ExAny _) _ = True
    go ExXi ExXi = True
    go ExRoot ExRoot = True
    go ExTermination ExTermination = True
    go (ExFormation pbs) (ExFormation tbs) = all (\pbd -> loose pbd || any (kin pbd) tbs) pbs
    go (ExDispatch pexp pattr) (ExDispatch texp tattr) = same pattr tattr && go pexp texp
    go (ExApplication pexp (ArTau pattr _)) (ExApplication texp (ArTau tattr _)) = same pattr tattr && go pexp texp
    go (ExApplication pexp (ArAlpha _ _)) (ExApplication texp (ArAlpha _ _)) = go pexp texp
    go (ExPhiAgain{}) (ExPhiAgain{}) = True
    go (ExPhiMeet{}) (ExPhiMeet{}) = True
    go _ _ = False
    loose :: Binding -> Bool
    loose (BiMeta _) = True
    loose (BiAny _) = True
    loose _ = False
    kin :: Binding -> Binding -> Bool
    kin (BiTau pattr _) (BiTau tattr _) = same pattr tattr
    kin (BiVoid pattr) (BiVoid tattr) = same pattr tattr
    kin (BiLambda _) (BiLambda _) = True
    kin (BiDelta _) (BiDelta _) = True
    kin _ _ = False
    same :: Attribute -> Attribute -> Bool
    same (AtMeta _) _ = True
    same (AtAny _) _ = True
    same pattr tattr = pattr == tattr