{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
module Refinery.Tactic
( TacticT
, runTacticT
, (<@>)
, try
, many_
, choice
, progress
, goal
, focus
, forSubgoals
, MonadExtract(..)
, MonadRule(..)
, RuleT
, rule
, MonadProvable(..)
, ProvableT(..)
, Provable
, runProvable
, Alt(..)
) where
import Data.Functor.Alt
import Control.Applicative
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State.Strict
import Control.Monad.Trans
import Control.Monad.IO.Class
import Control.Monad.Morph
import Data.Bifunctor
import Pipes.Core
import Pipes.Lift (runStateP)
import Refinery.ProofState
import Refinery.Tactic.Internal
(<@>) :: (MonadProvable jdg m) => TacticT jdg ext m () -> [TacticT jdg ext m ()] -> TacticT jdg ext m ()
t <@> ts = stateful t applyTac (ts ++ repeat (pure ()))
where
applyTac j = do
tac <- gets head
modify tail
hoist lift $ asRule j tac
try :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () -> TacticT jdg ext m ()
try t = t <!> pure ()
many_ :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () -> TacticT jdg ext m ()
many_ t = try (t >> many_ t)
goal :: (Monad m) => TacticT jdg ext m jdg
goal = TacticT $ get
choice :: (MonadProvable jdg m, MonadError err m) => err -> [TacticT jdg ext m a] -> TacticT jdg ext m a
choice err [] = throwError err
choice err (t:ts) = t <!> choice err ts
progress :: (MonadProvable jdg m, MonadError err m) => (jdg -> jdg -> Bool) -> err -> TacticT jdg ext m a -> TacticT jdg ext m a
progress eq err t = do
j <- goal
a <- t
j' <- goal
if j `eq` j' then pure a else throwError err
focus :: (MonadProvable jdg m, Monad m) => TacticT jdg ext m () -> Int -> TacticT jdg ext m () -> TacticT jdg ext m ()
focus t ix t' = stateful t applyTac 0
where
applyTac j = do
n <- get
put (n + 1)
hoist lift $ asRule j (if n == ix then t' else pure ())
forSubgoals :: (Monad m) => TacticT jdg ext m a -> (jdg -> m b) -> TacticT jdg ext m a
forSubgoals t f = TacticT $ StateT $ \j -> ProofStateT $
action >\\ (unProofStateT $ runStateT (unTacticT t) j)
where
action (a, j) = do
lift $ f j
request (a, j)
runTacticT :: (MonadExtract ext m) => TacticT jdg ext m () -> jdg -> m (ext, [jdg])
runTacticT (TacticT t) j =
fmap (second reverse) $ flip runStateT [] $ runEffect $ server +>> (hoist lift $ unProofStateT $ execStateT t j)
where
server :: (MonadExtract ext m) => jdg -> Server jdg ext (StateT [jdg] m) ext
server j = do
modify (j:)
h <- hole
respond h >>= server
class (Monad m) => MonadExtract ext m | m -> ext where
hole :: m ext
default hole :: (MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext
hole = lift hole
instance (MonadExtract ext m) => MonadExtract ext (Proxy a' a b' b m)
instance (MonadExtract ext m) => MonadExtract ext (StateT s m)
instance (MonadExtract ext m) => MonadExtract ext (ReaderT env m)
instance (MonadExtract ext m) => MonadExtract ext (ExceptT err m)
instance (MonadExtract ext m) => MonadExtract ext (RuleT jdg ext m)
rule :: (Monad m) => (jdg -> RuleT jdg ext m ext) -> TacticT jdg ext m ()
rule r = TacticT $ StateT $ \j -> ProofStateT $ (\j' -> request ((), j')) >\\ unRuleT (r j)