{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}

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

module Rewriter (Seen, direct, every, fast, interpreted, rewrite, RewriteContext (..), Rewritten, Rewrittens, Rewrittens', seenInsert, seenMember, stepHeaders) where

import AST
import Builder
import Control.Exception (Exception, IOException, catch, displayException, throwIO)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe, isNothing)
import Data.Set (Set)
import qualified Data.Set as Set
import Deps
import Locator (locatedExpression, withLocatedExpression)
import Logger (logDebug)
import Matcher (Subst, sites)
import Must (Must (..), exceedsUpperBound, inRange)
import Printer (printExpression)
import Replacer (ReplaceExpressionFunc, replaceExpression, replaceExpressionFast)
import Rule (RuleContext (RuleContext), Step (..))
import qualified Rule as R
import Text.Printf (printf)
import qualified Yaml as Y

type RewriteState = (NonEmpty Rewritten, Expression, Seen, Bool, Maybe (Set Int))

type Seen = Map.Map Int [Expression]

seenMember :: Int -> Expression -> Seen -> Bool
seenMember :: Int -> Expression -> Seen -> Bool
seenMember Int
digest Expression
expr Seen
seen = Bool -> ([Expression] -> Bool) -> Maybe [Expression] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Expression -> [Expression] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Expression
expr) (Int -> Seen -> Maybe [Expression]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
digest Seen
seen)

seenInsert :: Int -> Expression -> Seen -> Seen
seenInsert :: Int -> Expression -> Seen -> Seen
seenInsert Int
digest Expression
expr = ([Expression] -> [Expression] -> [Expression])
-> Int -> [Expression] -> Seen -> Seen
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [Expression] -> [Expression] -> [Expression]
forall a. [a] -> [a] -> [a]
(++) Int
digest [Expression
expr]

type Rewritten = (Expression, Maybe (Judgment, String))

type Rewrittens = (NonEmpty Rewritten, Bool)

type Rewrittens' = ([Rewritten], Bool)

stepHeaders :: [Rewritten] -> [String]
stepHeaders :: [Rewritten] -> [String]
stepHeaders [Rewritten]
chain = (Int -> Rewritten -> Maybe Rewritten -> String)
-> [Int] -> [Rewritten] -> [Maybe Rewritten] -> [String]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Int -> Rewritten -> Maybe Rewritten -> String
header [Int
1 ..] [Rewritten]
chain (Maybe Rewritten
forall a. Maybe a
Nothing Maybe Rewritten -> [Maybe Rewritten] -> [Maybe Rewritten]
forall a. a -> [a] -> [a]
: (Rewritten -> Maybe Rewritten) -> [Rewritten] -> [Maybe Rewritten]
forall a b. (a -> b) -> [a] -> [b]
map Rewritten -> Maybe Rewritten
forall a. a -> Maybe a
Just [Rewritten]
chain)
  where
    header :: Int -> Rewritten -> Maybe Rewritten -> String
    header :: Int -> Rewritten -> Maybe Rewritten -> String
header Int
step Rewritten
_ Maybe Rewritten
Nothing = String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"=== Step #%d" Int
step
    header Int
step (Expression
current, Maybe (Judgment, String)
_) (Just (Expression
before, Maybe (Judgment, String)
rule)) =
      String -> Int -> String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf
        String
"=== Step #%d, Rule '%s', %dt -> %dt"
        Int
step
        (String
-> ((Judgment, String) -> String)
-> Maybe (Judgment, String)
-> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"?" (Judgment, String) -> String
forall a b. (a, b) -> b
snd Maybe (Judgment, String)
rule)
        (Expression -> Int
countNodes Expression
before)
        (Expression -> Int
countNodes Expression
current)

type ToReplace = (Expression, Expression, Expression, [Subst])

data RewriteContext = RewriteContext
  { RewriteContext -> Expression
_locator :: Expression
  , RewriteContext -> Int
_maxDepth :: Int
  , RewriteContext -> Int
_maxCycles :: Int
  , RewriteContext -> Bool
_depthSensitive :: Bool
  , RewriteContext -> Maybe Expression
_universe :: Maybe Expression
  , RewriteContext -> BuildTermFunc
_buildTerm :: BuildTermFunc
  , RewriteContext -> Expression -> Bool
_normal :: Expression -> Bool
  , RewriteContext -> Maybe Expression -> Expression -> Set Int
_matching :: Maybe Expression -> Expression -> Set Int
  , RewriteContext -> Must
_must :: Must
  , RewriteContext -> Maybe String
_breakpoint :: Maybe String
  , RewriteContext -> SaveStepFunc
_saveStep :: SaveStepFunc
  , RewriteContext -> SaveMadeFunc
_saveMade :: SaveMadeFunc
  }

data RewriteException
  = MustBeGoing Must Int
  | MustStopBefore Must Int
  | StoppedOnLimit String Int
  | LoopingRewriting String String Int
  deriving (Show RewriteException
Typeable RewriteException
(Typeable RewriteException, Show RewriteException) =>
(RewriteException -> SomeException)
-> (SomeException -> Maybe RewriteException)
-> (RewriteException -> String)
-> Exception RewriteException
SomeException -> Maybe RewriteException
RewriteException -> String
RewriteException -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e) -> (e -> String) -> Exception e
$ctoException :: RewriteException -> SomeException
toException :: RewriteException -> SomeException
$cfromException :: SomeException -> Maybe RewriteException
fromException :: SomeException -> Maybe RewriteException
$cdisplayException :: RewriteException -> String
displayException :: RewriteException -> String
Exception)

instance Show RewriteException where
  show :: RewriteException -> String
show (MustBeGoing Must
mst Int
cnt) =
    String -> String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf
      String
"With option --must=%s it's expected rewriting cycles to be in range [%s], but rewriting stopped after %d cycles"
      (Must -> String
forall a. Show a => a -> String
show Must
mst)
      (Must -> String
forall a. Show a => a -> String
show Must
mst)
      Int
cnt
  show (MustStopBefore Must
mst Int
cnt) =
    String -> String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf
      String
"With option --must=%s it's expected rewriting cycles to be in range [%s], but rewriting has already reached %d cycles and is still going"
      (Must -> String
forall a. Show a => a -> String
show Must
mst)
      (Must -> String
forall a. Show a => a -> String
show Must
mst)
      Int
cnt
  show (StoppedOnLimit String
flg Int
lim) =
    String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf
      String
"With option --depth-sensitive it's expected rewriting iterations amount does not reach the limit: --%s=%d"
      String
flg
      Int
lim
  show (LoopingRewriting String
expr String
rul Int
stp) =
    String -> Int -> String -> String -> String
forall r. PrintfType r => String -> r
printf
      String
"On rewriting step '%d' of rule '%s' we got the same expression as we got at one of the previous step, it seems rewriting is looping\nExpression: %s"
      Int
stp
      String
rul
      String
expr

buildAndReplace' :: ToReplace -> ReplaceExpressionFunc -> IO (Expression, [(Expression, Expression)])
buildAndReplace' :: ToReplace
-> ReplaceExpressionFunc
-> IO (Expression, [(Expression, Expression)])
buildAndReplace' (Expression
expr, Expression
ptn, Expression
res, [Subst]
substs) ReplaceExpressionFunc
func = do
  [Expression]
ptns <- Expression -> [Subst] -> IO [Expression]
buildExpressionsThrows Expression
ptn [Subst]
substs
  [Expression]
repls <- Expression -> [Subst] -> IO [Expression]
buildExpressionsThrows Expression
res [Subst]
substs
  (Expression, [(Expression, Expression)])
-> IO (Expression, [(Expression, Expression)])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ReplaceExpressionFunc
func (Expression
expr, [Expression]
ptns, (Expression -> Expression -> Expression)
-> [Expression] -> [Expression -> Expression]
forall a b. (a -> b) -> [a] -> [b]
map Expression -> Expression -> Expression
forall a b. a -> b -> a
const [Expression]
repls), [Expression] -> [Expression] -> [(Expression, Expression)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Expression]
ptns [Expression]
repls)

tryBuildAndReplaceFast :: ToReplace -> IO (Expression, [(Expression, Expression)])
tryBuildAndReplaceFast :: ToReplace -> IO (Expression, [(Expression, Expression)])
tryBuildAndReplaceFast state :: ToReplace
state@(Expression
expr, ptn :: Expression
ptn@(ExFormation (Binding
_ : [Binding]
pbds)), res :: Expression
res@(ExFormation (Binding
_ : [Binding]
rbds)), [Subst]
substs)
  | Expression -> Expression -> Bool
fast Expression
ptn Expression
res = do
      String -> IO ()
logDebug String
"Applying fast replacing since 'pattern' and 'result' are suitable for this..."
      ToReplace
-> ReplaceExpressionFunc
-> IO (Expression, [(Expression, Expression)])
buildAndReplace' (Expression
expr, [Binding] -> Expression
ExFormation ([Binding] -> [Binding]
forall a. HasCallStack => [a] -> [a]
init [Binding]
pbds), [Binding] -> Expression
ExFormation ([Binding] -> [Binding]
forall a. HasCallStack => [a] -> [a]
init [Binding]
rbds), [Subst]
substs) ReplaceExpressionFunc
replaceExpressionFast
  | Bool
otherwise = do
      String -> IO ()
logDebug String
"Applying regular replacing..."
      ToReplace
-> ReplaceExpressionFunc
-> IO (Expression, [(Expression, Expression)])
buildAndReplace' ToReplace
state ReplaceExpressionFunc
replaceExpression
tryBuildAndReplaceFast ToReplace
state = ToReplace
-> ReplaceExpressionFunc
-> IO (Expression, [(Expression, Expression)])
buildAndReplace' ToReplace
state ReplaceExpressionFunc
replaceExpression

fast :: Expression -> Expression -> Bool
fast :: Expression -> Expression -> Bool
fast (ExFormation _pbds :: [Binding]
_pbds@(Binding
pbd : [Binding]
pbds)) (ExFormation _rbds :: [Binding]
_rbds@(Binding
rbd : [Binding]
rbds)) =
  [Binding] -> Bool
startsAndEndsWithMeta [Binding]
_pbds
    Bool -> Bool -> Bool
&& [Binding] -> Bool
startsAndEndsWithMeta [Binding]
_rbds
    Bool -> Bool -> Bool
&& Bool -> Bool
not ([Binding] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Binding] -> [Binding]
forall a. HasCallStack => [a] -> [a]
init [Binding]
pbds))
    Bool -> Bool -> Bool
&& Binding
pbd Binding -> Binding -> Bool
forall a. Eq a => a -> a -> Bool
== Binding
rbd
    Bool -> Bool -> Bool
&& [Binding] -> Binding
forall a. HasCallStack => [a] -> a
last [Binding]
pbds Binding -> Binding -> Bool
forall a. Eq a => a -> a -> Bool
== [Binding] -> Binding
forall a. HasCallStack => [a] -> a
last [Binding]
rbds
    Bool -> Bool -> Bool
&& Bool -> Bool
not ([Binding] -> Bool
hasMetaBindings ([Binding] -> [Binding]
forall a. HasCallStack => [a] -> [a]
init [Binding]
pbds))
    Bool -> Bool -> Bool
&& Bool -> Bool
not ([Binding] -> Bool
hasMetaBindings ([Binding] -> [Binding]
forall a. HasCallStack => [a] -> [a]
init [Binding]
rbds))
  where
    startsAndEndsWithMeta :: [Binding] -> Bool
    startsAndEndsWithMeta :: [Binding] -> Bool
startsAndEndsWithMeta [] = Bool
False
    startsAndEndsWithMeta bds :: [Binding]
bds@(Binding
bd : [Binding]
_) =
      [Binding] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Binding]
bds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
        Bool -> Bool -> Bool
&& Binding -> Bool
isMetaBinding Binding
bd
        Bool -> Bool -> Bool
&& Binding -> Bool
isMetaBinding ([Binding] -> Binding
forall a. HasCallStack => [a] -> a
last [Binding]
bds)
    hasMetaBindings :: [Binding] -> Bool
    hasMetaBindings :: [Binding] -> Bool
hasMetaBindings = (Bool -> Binding -> Bool) -> Bool -> [Binding] -> Bool
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Bool
acc Binding
bd -> Bool
acc Bool -> Bool -> Bool
|| Binding -> Bool
isMetaBinding Binding
bd) Bool
False
    isMetaBinding :: Binding -> Bool
    isMetaBinding :: Binding -> Bool
isMetaBinding = \case
      BiMeta Text
_ -> Bool
True
      BiAny Slot
_ -> Bool
True
      Binding
_ -> Bool
False
fast Expression
_ Expression
_ = Bool
False

interpreted :: Y.Rule -> Step
interpreted :: Rule -> Step
interpreted Rule
rule = String
-> (RuleContext
    -> Expression
    -> IO (Maybe (Expression, [(Expression, Expression)])))
-> Step
Step Rule
rule.name RuleContext
-> Expression
-> IO (Maybe (Expression, [(Expression, Expression)]))
applied
  where
    applied :: RuleContext -> Expression -> IO (Maybe (Expression, [(Expression, Expression)]))
    applied :: RuleContext
-> Expression
-> IO (Maybe (Expression, [(Expression, Expression)]))
applied RuleContext
ctx Expression
expr =
      Expression -> Rule -> RuleContext -> IO [Subst]
R.matchExpressionWithRule Expression
expr Rule
rule RuleContext
ctx IO [Subst]
-> ([Subst] -> IO (Maybe (Expression, [(Expression, Expression)])))
-> IO (Maybe (Expression, [(Expression, Expression)]))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        [] -> Maybe (Expression, [(Expression, Expression)])
-> IO (Maybe (Expression, [(Expression, Expression)]))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Expression, [(Expression, Expression)])
forall a. Maybe a
Nothing
        [Subst]
matched
          | Maybe Condition -> Bool
forall a. Maybe a -> Bool
isNothing Rule
rule.when Bool -> Bool -> Bool
&& Maybe Condition -> Bool
forall a. Maybe a -> Bool
isNothing Rule
rule.having -> (Expression, [(Expression, Expression)])
-> Maybe (Expression, [(Expression, Expression)])
forall a. a -> Maybe a
Just ((Expression, [(Expression, Expression)])
 -> Maybe (Expression, [(Expression, Expression)]))
-> IO (Expression, [(Expression, Expression)])
-> IO (Maybe (Expression, [(Expression, Expression)]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ToReplace -> IO (Expression, [(Expression, Expression)])
tryBuildAndReplaceFast (Expression
expr, Rule
rule.pattern, Rule
rule.result, [Subst]
matched)
          | Bool
otherwise -> (Expression, [(Expression, Expression)])
-> Maybe (Expression, [(Expression, Expression)])
forall a. a -> Maybe a
Just ((Expression, [(Expression, Expression)])
 -> Maybe (Expression, [(Expression, Expression)]))
-> IO (Expression, [(Expression, Expression)])
-> IO (Maybe (Expression, [(Expression, Expression)]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ToReplace
-> ReplaceExpressionFunc
-> IO (Expression, [(Expression, Expression)])
buildAndReplace' (Expression
expr, Rule
rule.pattern, Rule
rule.result, [Subst]
matched) ReplaceExpressionFunc
replaceExpression

direct :: String -> Bool -> (Maybe Expression -> Expression -> [Expression]) -> Step
direct :: String
-> Bool -> (Maybe Expression -> Expression -> [Expression]) -> Step
direct String
name Bool
redex Maybe Expression -> Expression -> [Expression]
rewritten = String
-> (RuleContext
    -> Expression
    -> IO (Maybe (Expression, [(Expression, Expression)])))
-> Step
Step String
name RuleContext
-> Expression
-> IO (Maybe (Expression, [(Expression, Expression)]))
applied
  where
    applied :: RuleContext -> Expression -> IO (Maybe (Expression, [(Expression, Expression)]))
    applied :: RuleContext
-> Expression
-> IO (Maybe (Expression, [(Expression, Expression)]))
applied (RuleContext BuildTermFunc
_ Maybe Expression
universe Expression -> Bool
_) Expression
expr = Maybe (Expression, [(Expression, Expression)])
-> IO (Maybe (Expression, [(Expression, Expression)]))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Expression, [(Expression, Expression)])
 -> IO (Maybe (Expression, [(Expression, Expression)])))
-> Maybe (Expression, [(Expression, Expression)])
-> IO (Maybe (Expression, [(Expression, Expression)]))
forall a b. (a -> b) -> a -> b
$ case Bool
-> (Expression -> [Expression])
-> Expression
-> [(Expression, Expression)]
forall a.
Bool -> (Expression -> [a]) -> Expression -> [(Expression, a)]
sites Bool
redex (Maybe Expression -> Expression -> [Expression]
rewritten Maybe Expression
universe) Expression
expr of
      [] -> Maybe (Expression, [(Expression, Expression)])
forall a. Maybe a
Nothing
      [(Expression, Expression)]
found -> (Expression, [(Expression, Expression)])
-> Maybe (Expression, [(Expression, Expression)])
forall a. a -> Maybe a
Just (ReplaceExpressionFunc
replaceExpression (Expression
expr, ((Expression, Expression) -> Expression)
-> [(Expression, Expression)] -> [Expression]
forall a b. (a -> b) -> [a] -> [b]
map (Expression, Expression) -> Expression
forall a b. (a, b) -> a
fst [(Expression, Expression)]
found, ((Expression, Expression) -> Expression -> Expression)
-> [(Expression, Expression)] -> [Expression -> Expression]
forall a b. (a -> b) -> [a] -> [b]
map (Expression -> Expression -> Expression
forall a b. a -> b -> a
const (Expression -> Expression -> Expression)
-> ((Expression, Expression) -> Expression)
-> (Expression, Expression)
-> Expression
-> Expression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expression, Expression) -> Expression
forall a b. (a, b) -> b
snd) [(Expression, Expression)]
found), [(Expression, Expression)]
found)

every :: [Step] -> Maybe Expression -> Expression -> Set Int
every :: [Step] -> Maybe Expression -> Expression -> Set Int
every [Step]
steps Maybe Expression
_ Expression
_ = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList ((Int -> Step -> Int) -> [Int] -> [Step] -> [Int]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Step -> Int
forall a b. a -> b -> a
const [Int
0 ..] [Step]
steps)

rewrite' :: RewriteState -> [(Int, Step)] -> Int -> RewriteContext -> IO RewriteState
rewrite' :: RewriteState
-> [(Int, Step)] -> Int -> RewriteContext -> IO RewriteState
rewrite' RewriteState
state [] Int
_ RewriteContext
_ = RewriteState -> IO RewriteState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RewriteState
state
rewrite' (NonEmpty Rewritten
rewrittens, Expression
located, Seen
unique, Bool
stop, Maybe (Set Int)
found) ((Int
idx, Step
rule) : [(Int, Step)]
rest) Int
iteration ctx :: RewriteContext
ctx@RewriteContext{Bool
Int
Maybe String
Maybe Expression
Expression
Must
BuildTermFunc
Maybe Expression -> Expression -> Set Int
Expression -> Bool
SaveStepFunc
SaveMadeFunc
$sel:_locator:RewriteContext :: RewriteContext -> Expression
$sel:_maxDepth:RewriteContext :: RewriteContext -> Int
$sel:_maxCycles:RewriteContext :: RewriteContext -> Int
$sel:_depthSensitive:RewriteContext :: RewriteContext -> Bool
$sel:_universe:RewriteContext :: RewriteContext -> Maybe Expression
$sel:_buildTerm:RewriteContext :: RewriteContext -> BuildTermFunc
$sel:_normal:RewriteContext :: RewriteContext -> Expression -> Bool
$sel:_matching:RewriteContext :: RewriteContext -> Maybe Expression -> Expression -> Set Int
$sel:_must:RewriteContext :: RewriteContext -> Must
$sel:_breakpoint:RewriteContext :: RewriteContext -> Maybe String
$sel:_saveStep:RewriteContext :: RewriteContext -> SaveStepFunc
$sel:_saveMade:RewriteContext :: RewriteContext -> SaveMadeFunc
_locator :: Expression
_maxDepth :: Int
_maxCycles :: Int
_depthSensitive :: Bool
_universe :: Maybe Expression
_buildTerm :: BuildTermFunc
_normal :: Expression -> Bool
_matching :: Maybe Expression -> Expression -> Set Int
_must :: Must
_breakpoint :: Maybe String
_saveStep :: SaveStepFunc
_saveMade :: SaveMadeFunc
..}
  | Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Int
idx Set Int
matched Bool -> Bool -> Bool
|| Maybe String
_breakpoint Maybe String -> Maybe String -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Maybe String
forall a. a -> Maybe a
Just (Step -> String
_name Step
rule) =
      RewriteState -> Int -> IO RewriteState
_rewrite (NonEmpty Rewritten
rewrittens, Expression
located, Seen
unique, Bool
stop, Set Int -> Maybe (Set Int)
forall a. a -> Maybe a
Just Set Int
matched) Int
1 IO RewriteState
-> (RewriteState -> IO RewriteState) -> IO RewriteState
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        state' :: RewriteState
state'@(NonEmpty Rewritten
_, Expression
_, Seen
_, Bool
True, Maybe (Set Int)
_) -> RewriteState -> IO RewriteState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RewriteState
state'
        RewriteState
state' -> RewriteState
-> [(Int, Step)] -> Int -> RewriteContext -> IO RewriteState
rewrite' RewriteState
state' [(Int, Step)]
rest Int
iteration RewriteContext
ctx
  | Bool
otherwise = RewriteState
-> [(Int, Step)] -> Int -> RewriteContext -> IO RewriteState
rewrite' (NonEmpty Rewritten
rewrittens, Expression
located, Seen
unique, Bool
stop, Set Int -> Maybe (Set Int)
forall a. a -> Maybe a
Just Set Int
matched) [(Int, Step)]
rest Int
iteration RewriteContext
ctx
  where
    matched :: Set Int
    matched :: Set Int
matched = Set Int -> Maybe (Set Int) -> Set Int
forall a. a -> Maybe a -> a
fromMaybe (Maybe Expression -> Expression -> Set Int
_matching Maybe Expression
_universe Expression
located) Maybe (Set Int)
found
    _rewrite :: RewriteState -> Int -> IO RewriteState
    _rewrite :: RewriteState -> Int -> IO RewriteState
_rewrite (_rewrittens :: NonEmpty Rewritten
_rewrittens@((Expression
current, Maybe (Judgment, String)
_) :| [Rewritten]
_), Expression
expression, Seen
_unique, Bool
_, Maybe (Set Int)
_found) Int
_count =
      let ruleName :: String
ruleName = Step -> String
_name Step
rule
       in if Int
_count Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
_maxDepth
            then do
              String -> IO ()
logDebug (String -> Int -> String -> String
forall r. PrintfType r => String -> r
printf String
"Max amount of rewriting cycles (%d) for rule '%s' has been reached, rewriting is stopped" Int
_maxDepth String
ruleName)
              if Bool
_depthSensitive
                then do
                  Bool
exhausted <- Expression -> [Step] -> RewriteContext -> IO Bool
applicable Expression
expression [Step
rule] RewriteContext
ctx
                  if Bool
exhausted
                    then RewriteException -> IO RewriteState
forall e a. Exception e => e -> IO a
throwIO (String -> Int -> RewriteException
StoppedOnLimit String
"max-depth" Int
_maxDepth)
                    else RewriteState -> IO RewriteState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NonEmpty Rewritten
_rewrittens, Expression
expression, Seen
_unique, Bool
False, Maybe (Set Int)
_found)
                else RewriteState -> IO RewriteState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NonEmpty Rewritten
_rewrittens, Expression
expression, Seen
_unique, Bool
False, Maybe (Set Int)
_found)
            else do
              String -> IO ()
logDebug (String -> String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"Starting rewriting cycle for rule '%s': %d out of %d" String
ruleName Int
_count Int
_maxDepth)
              Step
-> RuleContext
-> Expression
-> IO (Maybe (Expression, [(Expression, Expression)]))
_applied Step
rule (BuildTermFunc
-> Maybe Expression -> (Expression -> Bool) -> RuleContext
RuleContext BuildTermFunc
_buildTerm Maybe Expression
_universe Expression -> Bool
_normal) Expression
expression IO (Maybe (Expression, [(Expression, Expression)]))
-> (Maybe (Expression, [(Expression, Expression)])
    -> IO RewriteState)
-> IO RewriteState
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Maybe (Expression, [(Expression, Expression)])
Nothing -> do
                  String -> IO ()
logDebug (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Rule '%s' does not match, rewriting is stopped" String
ruleName)
                  if Maybe String
_breakpoint Maybe String -> Maybe String -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Maybe String
forall a. a -> Maybe a
Just String
ruleName Bool -> Bool -> Bool
&& String
ruleName String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String
fired | (Expression
_, Just (Judgment
_, String
fired)) <- NonEmpty Rewritten -> [Rewritten]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty Rewritten
_rewrittens]
                    then do
                      String -> IO ()
logDebug (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Rule '%s' is a breakpoint, dropping down all the previous rewritings..." String
ruleName)
                      RewriteState -> IO RewriteState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NonEmpty Rewritten
_rewrittens, Expression
expression, Seen
_unique, Bool
True, Maybe (Set Int)
_found)
                    else RewriteState -> IO RewriteState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NonEmpty Rewritten
_rewrittens, Expression
expression, Seen
_unique, Bool
False, Maybe (Set Int)
_found)
                Just (Expression
expr, [(Expression, Expression)]
rewritten) -> do
                  String -> IO ()
logDebug (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Rule '%s' has been matched and applied" String
ruleName)
                  if Expression
expression Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
expr
                    then do
                      String -> IO ()
logDebug (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Applied '%s', no changes made" String
ruleName)
                      RewriteState -> IO RewriteState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NonEmpty Rewritten
_rewrittens, Expression
expression, Seen
_unique, Bool
False, Maybe (Set Int)
_found)
                    else
                      let digest :: Int
digest = Expression -> Int
hashExpression Expression
expr
                       in if Int -> Expression -> Seen -> Bool
seenMember Int
digest Expression
expr Seen
_unique
                            then RewriteException -> IO RewriteState
forall e a. Exception e => e -> IO a
throwIO (String -> String -> Int -> RewriteException
LoopingRewriting (Expression -> String
printExpression Expression
expr) String
ruleName Int
_count)
                            else do
                              String -> IO ()
logDebug
                                ( String -> String -> Int -> Int -> String -> String
forall r. PrintfType r => String -> r
printf
                                    String
"Applied '%s' (%d nodes -> %d nodes)\n%s"
                                    String
ruleName
                                    (Expression -> Int
countNodes Expression
expression)
                                    (Expression -> Int
countNodes Expression
expr)
                                    (Expression -> String
printExpression Expression
expr)
                                )
                              Expression
updated <- Expression -> Expression -> Expression -> IO Expression
withLocatedExpression Expression
_locator Expression
expr Expression
current
                              SaveStepFunc
_saveStep Expression
updated
                              ((Expression, Expression) -> IO ())
-> [(Expression, Expression)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SaveMadeFunc -> (Expression, Expression) -> IO ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SaveMadeFunc
_saveMade) [(Expression
redex, Expression
object) | (redex :: Expression
redex@(ExApplication Expression
head' (ArTau Attribute
attr Expression
_)), object :: Expression
object@(ExFormation [Binding]
_)) <- [(Expression, Expression)]
rewritten, Attribute
attr Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Attribute
AtRho, Expression
object Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
/= Expression
head']
                              RewriteState -> Int -> IO RewriteState
_rewrite (Expression -> NonEmpty Rewritten
leadsTo Expression
updated, Expression
expr, Int -> Expression -> Seen -> Seen
seenInsert Int
digest Expression
expr Seen
_unique, Bool
False, Maybe (Set Int)
forall a. Maybe a
Nothing) (Int
_count Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
      where
        leadsTo :: Expression -> NonEmpty Rewritten
        leadsTo :: Expression -> NonEmpty Rewritten
leadsTo Expression
next =
          let (Expression
head', Maybe (Judgment, String)
_) :| [Rewritten]
rest = NonEmpty Rewritten
_rewrittens
           in (Expression
next, Maybe (Judgment, String)
forall a. Maybe a
Nothing) Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| (Expression
head', (Judgment, String) -> Maybe (Judgment, String)
forall a. a -> Maybe a
Just (Judgment
Normalization, Step -> String
_name Step
rule)) Rewritten -> [Rewritten] -> [Rewritten]
forall a. a -> [a] -> [a]
: [Rewritten]
rest

applicable :: Expression -> [Step] -> RewriteContext -> IO Bool
applicable :: Expression -> [Step] -> RewriteContext -> IO Bool
applicable Expression
_ [] RewriteContext
_ = Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
applicable Expression
expression (Step
rule : [Step]
rest) ctx :: RewriteContext
ctx@RewriteContext{Bool
Int
Maybe String
Maybe Expression
Expression
Must
BuildTermFunc
Maybe Expression -> Expression -> Set Int
Expression -> Bool
SaveStepFunc
SaveMadeFunc
$sel:_locator:RewriteContext :: RewriteContext -> Expression
$sel:_maxDepth:RewriteContext :: RewriteContext -> Int
$sel:_maxCycles:RewriteContext :: RewriteContext -> Int
$sel:_depthSensitive:RewriteContext :: RewriteContext -> Bool
$sel:_universe:RewriteContext :: RewriteContext -> Maybe Expression
$sel:_buildTerm:RewriteContext :: RewriteContext -> BuildTermFunc
$sel:_normal:RewriteContext :: RewriteContext -> Expression -> Bool
$sel:_matching:RewriteContext :: RewriteContext -> Maybe Expression -> Expression -> Set Int
$sel:_must:RewriteContext :: RewriteContext -> Must
$sel:_breakpoint:RewriteContext :: RewriteContext -> Maybe String
$sel:_saveStep:RewriteContext :: RewriteContext -> SaveStepFunc
$sel:_saveMade:RewriteContext :: RewriteContext -> SaveMadeFunc
_locator :: Expression
_maxDepth :: Int
_maxCycles :: Int
_depthSensitive :: Bool
_universe :: Maybe Expression
_buildTerm :: BuildTermFunc
_normal :: Expression -> Bool
_matching :: Maybe Expression -> Expression -> Set Int
_must :: Must
_breakpoint :: Maybe String
_saveStep :: SaveStepFunc
_saveMade :: SaveMadeFunc
..} = do
  Bool
applies <- (Step -> IO Bool
probe Step
rule IO Bool -> (IOException -> IO Bool) -> IO Bool
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` IOException -> IO Bool
onIOException) IO Bool -> (BuildException -> IO Bool) -> IO Bool
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` BuildException -> IO Bool
onBuildException
  case Bool
applies of
    Bool
True -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    Bool
False -> Expression -> [Step] -> RewriteContext -> IO Bool
applicable Expression
expression [Step]
rest RewriteContext
ctx
  where
    probe :: Step -> IO Bool
    probe :: Step -> IO Bool
probe Step
rule =
      Step
-> RuleContext
-> Expression
-> IO (Maybe (Expression, [(Expression, Expression)]))
_applied Step
rule (BuildTermFunc
-> Maybe Expression -> (Expression -> Bool) -> RuleContext
RuleContext BuildTermFunc
_buildTerm Maybe Expression
_universe Expression -> Bool
_normal) Expression
expression IO (Maybe (Expression, [(Expression, Expression)]))
-> (Maybe (Expression, [(Expression, Expression)]) -> IO Bool)
-> IO Bool
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just (Expression
changed, [(Expression, Expression)]
_) | Expression
changed Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
/= Expression
expression -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
        Maybe (Expression, [(Expression, Expression)])
_ -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
    onIOException :: IOException -> IO Bool
    onIOException :: IOException -> IO Bool
onIOException = IOException -> IO Bool
forall e. Exception e => e -> IO Bool
raised
    onBuildException :: BuildException -> IO Bool
    onBuildException :: BuildException -> IO Bool
onBuildException = BuildException -> IO Bool
forall e. Exception e => e -> IO Bool
raised
    raised :: Exception e => e -> IO Bool
    raised :: forall e. Exception e => e -> IO Bool
raised e
err
      | Bool
_depthSensitive = e -> IO Bool
forall e a. Exception e => e -> IO a
throwIO e
err
      | Bool
otherwise = do
          String -> IO ()
logDebug (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Rule '%s' raised and was treated as not applicable: %s" (Step -> String
_name Step
rule) (e -> String
forall e. Exception e => e -> String
displayException e
err))
          Expression -> [Step] -> RewriteContext -> IO Bool
applicable Expression
expression [Step]
rest RewriteContext
ctx

rewrite :: Expression -> [Step] -> RewriteContext -> IO Rewrittens
rewrite :: Expression -> [Step] -> RewriteContext -> IO Rewrittens
rewrite Expression
expr [Step]
rules ctx :: RewriteContext
ctx@RewriteContext{Bool
Int
Maybe String
Maybe Expression
Expression
Must
BuildTermFunc
Maybe Expression -> Expression -> Set Int
Expression -> Bool
SaveStepFunc
SaveMadeFunc
$sel:_locator:RewriteContext :: RewriteContext -> Expression
$sel:_maxDepth:RewriteContext :: RewriteContext -> Int
$sel:_maxCycles:RewriteContext :: RewriteContext -> Int
$sel:_depthSensitive:RewriteContext :: RewriteContext -> Bool
$sel:_universe:RewriteContext :: RewriteContext -> Maybe Expression
$sel:_buildTerm:RewriteContext :: RewriteContext -> BuildTermFunc
$sel:_normal:RewriteContext :: RewriteContext -> Expression -> Bool
$sel:_matching:RewriteContext :: RewriteContext -> Maybe Expression -> Expression -> Set Int
$sel:_must:RewriteContext :: RewriteContext -> Must
$sel:_breakpoint:RewriteContext :: RewriteContext -> Maybe String
$sel:_saveStep:RewriteContext :: RewriteContext -> SaveStepFunc
$sel:_saveMade:RewriteContext :: RewriteContext -> SaveMadeFunc
_locator :: Expression
_maxDepth :: Int
_maxCycles :: Int
_depthSensitive :: Bool
_universe :: Maybe Expression
_buildTerm :: BuildTermFunc
_normal :: Expression -> Bool
_matching :: Maybe Expression -> Expression -> Set Int
_must :: Must
_breakpoint :: Maybe String
_saveStep :: SaveStepFunc
_saveMade :: SaveMadeFunc
..} = do
  Expression
located <- Expression -> Expression -> IO Expression
locatedExpression Expression
_locator Expression
expr
  (NonEmpty Rewritten
rewrittens, Bool
exceeded) <- RewriteState -> Int -> IO Rewrittens
_rewrite ((Expression
expr, Maybe (Judgment, String)
forall a. Maybe a
Nothing) Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| [], Expression
located, Seen
forall k a. Map k a
Map.empty, Bool
False, Maybe (Set Int)
forall a. Maybe a
Nothing) Int
0
  Rewrittens -> IO Rewrittens
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NonEmpty Rewritten -> NonEmpty Rewritten
forall a. NonEmpty a -> NonEmpty a
NE.reverse NonEmpty Rewritten
rewrittens, Bool
exceeded)
  where
    _rewrite :: RewriteState -> Int -> IO Rewrittens
    _rewrite :: RewriteState -> Int -> IO Rewrittens
_rewrite state :: RewriteState
state@(rewrittens :: NonEmpty Rewritten
rewrittens@((Expression
current, Maybe (Judgment, String)
_) :| [Rewritten]
_), Expression
expression, Seen
_, Bool
_, Maybe (Set Int)
_) Int
count
      | Bool -> Bool
not (Must -> Int -> Bool
inRange Must
_must Int
count) Bool -> Bool -> Bool
&& Int
count Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Must -> Int -> Bool
exceedsUpperBound Must
_must Int
count = RewriteException -> IO Rewrittens
forall e a. Exception e => e -> IO a
throwIO (Must -> Int -> RewriteException
MustStopBefore Must
_must Int
count)
      | Int
count Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
_maxCycles Bool -> Bool -> Bool
&& Bool -> Bool
not (Must -> Int -> Bool
inRange Must
_must Int
count) = RewriteException -> IO Rewrittens
forall e a. Exception e => e -> IO a
throwIO (Must -> Int -> RewriteException
MustBeGoing Must
_must Int
count)
      | Int
count Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
_maxCycles = do
          String -> IO ()
logDebug (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"Max amount of rewriting cycles for all rules (%d) has been reached, rewriting is stopped" Int
_maxCycles)
          Bool
applies <- Expression -> [Step] -> RewriteContext -> IO Bool
applicable Expression
expression [Step]
rules RewriteContext
ctx
          if Bool
_depthSensitive Bool -> Bool -> Bool
&& Bool
applies
            then RewriteException -> IO Rewrittens
forall e a. Exception e => e -> IO a
throwIO (String -> Int -> RewriteException
StoppedOnLimit String
"max-cycles" Int
_maxCycles)
            else Rewrittens -> IO Rewrittens
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NonEmpty Rewritten
rewrittens, Bool
applies)
      | Bool
otherwise = do
          String -> IO ()
logDebug (String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"Starting rewriting cycle for all rules: %d out of %d" Int
count Int
_maxCycles)
          RewriteState
-> [(Int, Step)] -> Int -> RewriteContext -> IO RewriteState
rewrite' RewriteState
state ([Int] -> [Step] -> [(Int, Step)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Step]
rules) Int
count RewriteContext
ctx IO RewriteState -> (RewriteState -> IO Rewrittens) -> IO Rewrittens
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            (NonEmpty Rewritten
_, Expression
_, Seen
_, Bool
True, Maybe (Set Int)
_) -> Rewrittens -> IO Rewrittens
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Expression
expr, Maybe (Judgment, String)
forall a. Maybe a
Nothing) Rewritten -> [Rewritten] -> NonEmpty Rewritten
forall a. a -> [a] -> NonEmpty a
:| [], Bool
False)
            state' :: RewriteState
state'@(rewrittens' :: NonEmpty Rewritten
rewrittens'@((Expression
current', Maybe (Judgment, String)
_) :| [Rewritten]
_), Expression
_, Seen
_, Bool
False, Maybe (Set Int)
_) ->
              if NonEmpty Rewritten -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty Rewritten
rewrittens' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== NonEmpty Rewritten -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty Rewritten
rewrittens Bool -> Bool -> Bool
|| Expression
current' Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
current
                then do
                  String -> IO ()
logDebug String
"Rewriting is stopped since it has no effect"
                  if Bool -> Bool
not (Must -> Int -> Bool
inRange Must
_must Int
count)
                    then RewriteException -> IO Rewrittens
forall e a. Exception e => e -> IO a
throwIO (Must -> Int -> RewriteException
MustBeGoing Must
_must Int
count)
                    else Rewrittens -> IO Rewrittens
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NonEmpty Rewritten
rewrittens', Bool
False)
                else RewriteState -> Int -> IO Rewrittens
_rewrite RewriteState
state' (Int
count Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)