LayeredStep.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.LayeredStep 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 Control.Monad.Error.Class (MonadError(throwError))
import Control.Monad.IMSOS.LayeredTerms (Term, unTerm, inject, project)
import Data.Maybe (isJust)
import Control.Applicative (Alternative(empty))

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

data StepRes (l :: Lang) (e :: 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 l) i  -> StepRes l e i
  Step   :: (IsLangOp l i f)  => f (Term 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) (e :: Rel) (f :: Signature) where
  step :: forall i. f (Term l) i -> SemMonad l e (StepRes l e i)

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

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

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

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

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

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

stepsOrHaltWhen :: forall e l f i.
  ( e `GivesSemanticsTo` l
  , StepsAvailable e l i
  , IsValOp e l i f
  )
    => (Term l i -> SemState l e -> SemWriter l e -> Bool) -- predicate over an I-MSOS configuration
          -> Term l i                                  -- consisting of term after step, state and writer values
          -> SemMonad l e (Either (Term l i) (f (Term l) i))
stepsOrHaltWhen predicate t
  | Just v <- toValue @f @e @l t = return $ Right v
  | otherwise = do
            (t', w) <- listen @(SemWriter l e) (premise @e @l t)
            s <- get @(SemState l e)
            if predicate t' s w then return $ Left t'
                                else stepsOrHaltWhen @e @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 :<: SubSig l i, ValOps l e i :<: Sig l, HasSubSig l i) =>
  HasValOps (l :: Lang) (e :: 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 (Term l) i

-- | Tests whether a term is a ValOp and converts if possible 
toValue :: forall f e l i.
  (HasValOps l e i, f :<: ValOps l e i, f :<: SubSig l i) =>
    Term l i -> Maybe (f (Term 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 e l i.
  (HasValOps l e i)
  => Term l i -> Bool
isValue = isJust . toValue @(ValOps l e i) @e @l @i

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

class HasRulesErrors e where
  ruleAssertionError      :: String -> e
  noApplicableRulesError  :: symb -> f (Term l) i -> e
  stepOnValueError        :: symb -> f (Term l) 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 e l i =
    ( RelID e
    , StepDefined l e (SubSig l i))

type StepsAvailable e l i =
    (StepAvailable e l i
    ,HasSubSig l i
    ,HasValOps l e i)

type StepsTo e l i f =
  (StepsAvailable e l i
  ,IsValOp e 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
  ,f :<: SubSig l i
  ,HasSubSig l i)

type SharedSemEntities l (e :: Rel) (e' :: Rel) =
  ( SemEntities l e
  , SemEntities l e
  , SemAlternative l e ~ SemAlternative l e'
  , SemMonadError l e  ~ SemMonadError l e'
  , SemError l e       ~ SemError l e'
  , SemState l e       ~ SemState l e'
  , SemWriter l e      ~ SemWriter l e'
  , SemReader l e      ~ SemReader l e'
  )