Prefix.hs

{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- Copyright 2018, Ideas project team. This file is distributed under the
-- terms of the Apache License 2.0. For more information, see the files
-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-- Basic machinery for fully executing a strategy expression, or only
-- partially. Partial execution results in a prefix that keeps the current
-- locations in the strategy (a list of @Path@s) for continuing the execution
-- later on. A path can be used to reconstruct the sequence of steps already
-- performed (a so-called trace). Prefixes can be merged with the Monoid
-- operation.
--
-----------------------------------------------------------------------------

module Ideas.Common.Strategy.Prefix
   ( -- * Prefix
     Prefix, noPrefix, makePrefix, firstsOrdered
   , replayProcess
   , isEmptyPrefix, majorPrefix, searchModePrefix, prefixPaths
     -- * Path
   , Path, emptyPath, readPath, readPaths
   ) where

import Data.Char
import Data.List (intercalate)
import Data.Maybe
import Data.Monoid hiding ((<>))
import Data.Semigroup as Sem
import Ideas.Common.Classes
import Ideas.Common.Environment
import Ideas.Common.Rewriting.Term
import Ideas.Common.Rule
import Ideas.Common.Strategy.Choice
import Ideas.Common.Strategy.Process
import Ideas.Common.Strategy.Sequence
import Ideas.Common.Strategy.StrategyTree
import Ideas.Utils.Prelude (splitsWithElem, readM)

--------------------------------------------------------------------------------
-- Prefix datatype

data Prefix a = Prefix
   { getPaths  :: [Path]
   , remainder :: Menu (Rule a) (a, Environment, Prefix a)
   }

instance Show (Prefix a) where
   show = intercalate ";" . map show . prefixPaths

instance Sem.Semigroup (Prefix a) where
   (Prefix xs p) <> (Prefix ys q) = Prefix (xs ++ ys) (p .|. q)

instance Monoid (Prefix a) where
   mempty  = noPrefix
   mappend = (<>)

instance Firsts (Prefix a) where
   type Elem (Prefix a) = (Rule a, a, Environment)

   ready  = hasDone . remainder
   firsts = map reorder . bests . remainder

firstsOrdered :: (Rule a -> Rule a -> Ordering) -> Prefix a -> [((Rule a, a, Environment), Prefix a)]
firstsOrdered cmp = map reorder . bestsOrdered cmp . remainder

reorder :: (a, (b, env, c)) -> ((a, b, env), c)
reorder (x, (y, env, z)) = ((x, y, env), z)

--------------------------------------------------------------------------------
-- Constructing a prefix

-- | The error prefix (i.e., without a location in the strategy).
noPrefix :: Prefix a
noPrefix = Prefix [] empty

-- | Make a prefix from a core strategy and a start term.
makePrefix :: Process (Leaf a) -> a -> Prefix a
makePrefix = snd . replayProcess emptyPath

-- | Construct a prefix by replaying a path in a core strategy: the third
-- argument is the current term.
replayProcess :: Path -> Process (Leaf a) -> ([Rule a], a -> Prefix a)
replayProcess (Path is) = fromMaybe ([], const noPrefix) . replay [] is
 where
   replay acc path p =
      case path of
         []         -> return (reverse acc, createPrefix p)
         Input _:_  -> Nothing
         Index n:ns -> do
            (leaf, q) <- getByIndex n (menu p)
            case (leaf, ns) of
               (LeafRule r, _) -> replay (r:acc) ns q
               (LeafDyn d, Input t:ns2) -> do
                  a <- dynamicFromTerm d t
                  replay acc ns2 (treeToProcess a .*. q)
               _ -> Nothing

   createPrefix p = Prefix [Path is] . flip (rec []) p

   rec ns a = cut . onMenuWithIndex f doneMenu . menu
    where
      f n (LeafDyn d) p = fromMaybe empty $ do
         t <- dynamicToTerm d a
         s <- dynamicFromTerm d t
         return (rec (Input t:Index n:ns) a (treeToProcess s .*. p))
      f n (LeafRule r) p = choice
         [ r ?~> (b, env, mk b)
         | (b, env) <- transApply (transformation r) a
         ]
       where
         ms   = Index n:ns
         path = Path (is ++ reverse ms)
         mk b = Prefix [path] (rec ms b p)

         x ?~> y@(_, _, q)
            | isMinor r && stopped q = empty
            | otherwise = x |-> y

stopped :: Prefix a -> Bool
stopped = isEmpty . remainder

--------------------------------------------------------------------------------
-- Prefix fuctions

isEmptyPrefix :: Prefix a -> Bool
isEmptyPrefix = all (== emptyPath) . getPaths

-- | Transforms the prefix such that only major steps are kept in the remaining
-- strategy.
majorPrefix :: Prefix a -> Prefix a
majorPrefix prfx = prfx { remainder = onMenu f doneMenu (remainder prfx) }
 where
   f r (a, env, p)
      | isMajor r = r |-> (a, env, majorPrefix p)
      | otherwise = remainder (majorPrefix p)

-- | The searchModePrefix transformation changes the process in such a way that
--   all intermediate states can only be reached by one path. A prerequisite is
--   that symbols are unique (or only used once).
searchModePrefix :: Prefix a -> Prefix a
searchModePrefix prfx =
   prfx { remainder = rec (remainder (majorPrefix prfx)) }
 where
   rec m | hasDone m = doneMenu
         | otherwise = process (bests m)

   process [] = empty
   process ((r, (a, env, pr)):xs) =
      (r |-> (a, env, pr { remainder = rec (remainder pr) }))
      .|. process (concatMap (change r) xs)

   change y (r, pair) =
      bests (filterPrefix (/= y) r pair)

filterPrefix :: (Rule a -> Bool) -> Rule a -> (a, Environment, Prefix a) -> Menu (Rule a) (a, Environment, Prefix a)
filterPrefix cond = f
 where
   rec = onMenu f doneMenu
   f r (a, env, pr) = if cond r then r |-> (a, env, pr { remainder = rec (remainder pr) }) else empty

-- | Returns the current @Path@.
prefixPaths :: Prefix a -> [Path]
prefixPaths = getPaths

--------------------------------------------------------------------------------
-- Path

-- | A path encodes a location in a strategy. Paths are represented as a list
-- of integers and terms (the latter act as input for the dynamic strategies).
newtype Path = Path [PathItem]
   deriving Eq

data PathItem = Index Int | Input Term
   deriving Eq

instance Show PathItem where
   show (Index n) = show n
   show (Input t) = show t

instance Read PathItem where
   readsPrec n s =
      case dropWhile isSpace s of
         s2@(c:_) | isDigit c -> map (mapFirst Index) (readsPrec n s2)
         s2 -> map (mapFirst Input) (readsPrec n s2)

instance Show Path where
   show (Path is) = show is
   showList = (++) . intercalate ";" . map show

-- | The empty path.
emptyPath :: Path
emptyPath = Path []

readPath :: Monad m => String -> m Path
readPath = fmap Path . readM

readPaths :: Monad m => String -> m [Path]
readPaths = mapM readPath . splitsWithElem ';'