Step.hs

{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}

module Control.Monad.IMSOS.Rules.Step where

import Data.Comp.Multi.Ops      ((:+:)(..), (:<:))

import Control.Monad.IMSOS.Rules.Relations
import Data.Comp.ProjectionExt ((:<~), pr)
import Control.Monad.IMSOS.Monad (listen, get, MonadIMSOS)
import Control.Monad.IMSOS.Signatures
import Data.Kind (Type)
import Data.Comp.Multi.Term (Term)
import Control.Monad.Error.Class (MonadError(throwError))
import Data.Comp.Multi.Sum (inject)
import Data.Comp.Multi ( unTerm, project )
import Data.Maybe (isJust)
import Control.Applicative (Alternative(empty))

-- ───────────────────────────────────────────────
-- Rules
-- ───────────────────────────────────────────────

data StepRes (l :: Lang) (e :: Sort -> Rel) (i :: Type) where
  -- | the constraint on NoStep ensures only value operators are used
  -- forcing the use of NoStep and ValOps mechanisms to be consistent
  NoStep :: (IsValOp e l i f) => f (Term (Sig l)) i  -> StepRes l e i
  Step   :: (IsLangOp l i f)  => f (Term (Sig l)) i  -> StepRes l e i

-- |
-- StepDefined is the main class to define by users to express I-MSOS rules
-- instances are identified by `l` (language), `e` (relation) and `f` (operator)
-- the sort `i` of the operator is implicit
-- note that in StepDefined the order of the `e` and `l` is purposefully different
-- compared to the helper functions defined below
--
class
  StepDefined (l :: Lang) (t :: Type) (f :: Signature) where
  step :: forall i. f (TermL l) i -> SemMonad l (TaggedRel t i i) (StepRes l (TaggedRel t i) i)

premiseE :: forall t l i.
  ( StepAvailable t l i
  , HasRulesErrors (SemError l (TaggedRel t i i))
  , TaggedRel t i i `GivesSemanticsTo` l
  )
  => TermL l i -> SemMonad l (TaggedRel t i i) (TermL l i)
premiseE t = step @l @t t' >>= \case
  NoStep _  -> throwError (stepOnValueError (getRelID @(TaggedRel t i i)) t')
  Step t''  -> return (inject t'')
  where t' = unTerm t

premise :: forall t l i.
  ( StepAvailable t l i
  , TaggedRel t i i `GivesSemanticsTo` l
  )
  => TermL l i -> SemMonad l (TaggedRel t i i) (TermL l i)
premise t = step @l @t t' >>= \case
  NoStep _  -> empty
  Step t''  -> return (inject t'')
  where t' = unTerm t

notrans :: forall e l i f. (e i `GivesSemanticsTo` l, IsValOp e l i f)
  => f (TermL l) i -> SemMonad l (e i) (StepRes l e i)
notrans = return . NoStep

trans :: forall e l i f. (e i `GivesSemanticsTo` l, IsLangOp l i f)
  => f (TermL l) i -> SemMonad l (e i) (StepRes l e i)
trans = return . Step

steps :: forall (t :: Tag) l f i.
  ( TaggedRel t i i `GivesSemanticsTo` l
  , StepsAvailable t l i
  , IsValOp (TaggedRel t i) l i f )
    => TermL l i -> SemMonad l (TaggedRel t i i) (f (TermL l) i)
steps t | Just v <- toValue @f @t @l t = return v
        | otherwise                    = premise @t @l t >>= steps @t @l

stepsOrHalt :: forall (t :: Tag) h l f i.
  ( TaggedRel t i i `GivesSemanticsTo` l
  , StepsAvailable t l i
  , IsValOp (TaggedRel t i) l i f
  , h :<~ SemWriter l (TaggedRel t i i), Monoid h, Eq h
  )
    => TermL l i -> SemMonad l (TaggedRel t i i) (Either (TermL l i) (f (TermL l) i))
stepsOrHalt = stepsOrHaltWhen @t @l @f predicate
  where predicate _ _ w = pr @h w /= mempty

stepsOrHaltWhen :: forall (t :: Tag) l f i.
  ( TaggedRel t i i `GivesSemanticsTo` l
  , StepsAvailable t l i
  , IsValOp (TaggedRel t i) l i f
  )
    => (TermL l i -> SemState l (TaggedRel t i i) -> SemWriter l (TaggedRel t i i) -> Bool) -- predicate over an I-MSOS configuration
          -> TermL l i                                  -- consisting of term after step, state and writer values
          -> SemMonad l (TaggedRel t i i) (Either (TermL l i) (f (TermL l) i))
stepsOrHaltWhen predicate t
  | Just v <- toValue @f @t @l t = return $ Right v
  | otherwise = do
            (t', w) <- listen @(SemWriter l (TaggedRel t i i)) (premise @t @l t)
            s <- get @(SemState l (TaggedRel t i i))
            if predicate t' s w then return $ Left t'
                                else stepsOrHaltWhen @t @l predicate t'

instance
  ( StepDefined l e f
  , StepDefined l e g
  )
  => StepDefined l e (f :+: g) where
  step (Inl f) = step @l @e f
  step (Inr g) = step @l @e g


-- | A transition relation identifies which subsignature of a language's
-- signature identify the value operations of a particular sort 
-- this will be used to determine termination of computations
-- according to the relation
class (ValOps l e i :<: Sig l) =>
  HasValOps (l :: Lang) (e :: Sort -> Rel) (i :: Sort) where
    type ValOps l e i :: Signature

-- | ValOp are those terms that are built only from value operators
-- on the outermost level. 
-- Useful to build semantic entities. 
-- Only outermost operator is considered to support thunk-like values
type ValOp l e i = ValOps l e i (TermL l) i

-- | Tests whether a term is a ValOp and converts if possible 
toValue :: forall f t l i.
  (HasValOps l (TaggedRel t i) i, f :<: ValOps l (TaggedRel t i) i, f :<: Sig l) =>
    TermL l i -> Maybe (f (TermL l) i)
toValue = project @f

-- | Determine whether a term is constructed by a value constructor
-- of the relevant sort `i` (for a given `e` and `l`)
isValue :: forall t l i.
  (HasValOps l (TaggedRel t i) i)
  => TermL l i -> Bool
isValue = isJust . toValue @(ValOps l (TaggedRel t i) i) @t @l @i

-- ───────────────────────────────────────────────
-- Error handling
-- ───────────────────────────────────────────────

class HasRulesErrors e where
  ruleAssertionError      :: String -> e
  noApplicableRulesError  :: symb -> f (Term g) i -> e
  stepOnValueError        :: symb -> f (Term g) i -> e

instance (HasRulesErrors e, MonadError e (me e), Monoid w
         ,Traversable fl, Monad fl) =>
  MonadFail (MonadIMSOS r s w me e fl) where
  fail = throwError . ruleAssertionError @e

instance HasRulesErrors String where
  ruleAssertionError          = id
  noApplicableRulesError _ _  = "No rules applicable to term"
  stepOnValueError _ _        = "attempting to step on value term"

type StepAvailable t l i =
    ( RelID (TaggedRel t i i)
    , StepDefined l t (Sig l))

type StepsAvailable t l i =
    (StepAvailable t l i
    ,HasValOps l (TaggedRel t i) i)

type StepsTo t l i f =
  (StepsAvailable t l i
  ,IsValOp (TaggedRel t i) l i f)

type IsValOp e l i f =
  (f :<: ValOps l e i
  ,IsLangOp l i f)

type IsLangOp l i f =
  (f :<: Sig l)

type SharedSemEntities l (t :: Tag) i j =
  ( SemEntities l (TaggedRel t i i)
  , SemEntities l (TaggedRel t j j)
  , SemAlternative l (TaggedRel t i i) ~ SemAlternative l (TaggedRel t j j)
  , SemMonadError l (TaggedRel t i i)  ~ SemMonadError l (TaggedRel t j j)
  , SemError l (TaggedRel t i i)       ~ SemError l (TaggedRel t j j)
  , SemState l (TaggedRel t i i)       ~ SemState l (TaggedRel t j j)
  , SemWriter l (TaggedRel t i i)      ~ SemWriter l (TaggedRel t j j)
  , SemReader l (TaggedRel t i i)      ~ SemReader l (TaggedRel t j j)
  )