|
| 1 | +{-# LANGUAGE RankNTypes #-} |
| 2 | + |
| 3 | +------------------------------------------------------------------------------ |
| 4 | +-- | Things that belong in the future release of refinery v5. |
| 5 | +module Refinery.Future |
| 6 | + ( runStreamingTacticT |
| 7 | + , hoistListT |
| 8 | + , consume |
| 9 | + ) where |
| 10 | + |
| 11 | +import Control.Applicative |
| 12 | +import Control.Monad (ap, (>=>)) |
| 13 | +import Control.Monad.State.Lazy (runStateT) |
| 14 | +import Control.Monad.Trans |
| 15 | +import Data.Either (isRight) |
| 16 | +import Data.Functor ((<&>)) |
| 17 | +import Data.Tuple (swap) |
| 18 | +import Refinery.ProofState |
| 19 | +import Refinery.Tactic.Internal |
| 20 | + |
| 21 | + |
| 22 | + |
| 23 | +hoistElem :: Functor m => (forall x. m x -> n x) -> Elem m a -> Elem n a |
| 24 | +hoistElem _ Done = Done |
| 25 | +hoistElem f (Next a lt) = Next a $ hoistListT f lt |
| 26 | + |
| 27 | + |
| 28 | +hoistListT :: Functor m => (forall x. m x -> n x) -> ListT m a -> ListT n a |
| 29 | +hoistListT f t = ListT $ f $ fmap (hoistElem f) $ unListT t |
| 30 | + |
| 31 | + |
| 32 | +consume :: Monad m => ListT m a -> (a -> m ()) -> m () |
| 33 | +consume lt f = unListT lt >>= \case |
| 34 | + Done -> pure () |
| 35 | + Next a lt' -> f a >> consume lt' f |
| 36 | + |
| 37 | + |
| 38 | +newHole :: MonadExtract meta ext err s m => s -> m (s, (meta, ext)) |
| 39 | +newHole = fmap swap . runStateT hole |
| 40 | + |
| 41 | +runStreamingTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> ListT m (Either err (Proof s meta jdg ext)) |
| 42 | +runStreamingTacticT t j s = streamProofs s $ fmap snd $ proofState t j |
| 43 | + |
| 44 | +data Elem m a |
| 45 | + = Done |
| 46 | + | Next a (ListT m a) |
| 47 | + deriving stock Functor |
| 48 | + |
| 49 | + |
| 50 | +point :: Applicative m => a -> Elem m a |
| 51 | +point a = Next a $ ListT $ pure Done |
| 52 | + |
| 53 | +newtype ListT m a = ListT { unListT :: m (Elem m a) } |
| 54 | + |
| 55 | +cons :: (Applicative m) => a -> ListT m a -> ListT m a |
| 56 | +cons x xs = ListT $ pure $ Next x xs |
| 57 | + |
| 58 | +instance Functor m => Functor (ListT m) where |
| 59 | + fmap f (ListT xs) = ListT $ xs <&> \case |
| 60 | + Done -> Done |
| 61 | + Next a xs -> Next (f a) (fmap f xs) |
| 62 | + |
| 63 | +instance (Monad m) => Applicative (ListT m) where |
| 64 | + pure = return |
| 65 | + (<*>) = ap |
| 66 | + |
| 67 | +instance (Monad m) => Alternative (ListT m) where |
| 68 | + empty = ListT $ pure Done |
| 69 | + (ListT xs) <|> (ListT ys) = |
| 70 | + ListT $ xs >>= \case |
| 71 | + Done -> ys |
| 72 | + Next x xs -> pure (Next x (xs <|> ListT ys)) |
| 73 | + |
| 74 | +instance (Monad m) => Monad (ListT m) where |
| 75 | + return a = cons a empty |
| 76 | + (ListT xs) >>= k = |
| 77 | + ListT $ xs >>= \case |
| 78 | + Done -> pure Done |
| 79 | + Next x xs -> unListT $ k x <|> (xs >>= k) |
| 80 | + |
| 81 | + |
| 82 | +instance MonadTrans ListT where |
| 83 | + lift m = ListT $ fmap (\x -> Next x empty) m |
| 84 | + |
| 85 | + |
| 86 | +interleaveT :: (Monad m) => Elem m a -> Elem m a -> Elem m a |
| 87 | +interleaveT xs ys = |
| 88 | + case xs of |
| 89 | + Done -> ys |
| 90 | + Next x xs -> Next x $ ListT $ fmap (interleaveT ys) $ unListT xs |
| 91 | + |
| 92 | +-- ys <&> \case |
| 93 | +-- Done -> Next x xs |
| 94 | +-- Next y ys -> Next x (cons y (interleaveT xs ys)) |
| 95 | + |
| 96 | +force :: (Monad m) => Elem m a -> m [a] |
| 97 | +force = \case |
| 98 | + Done -> pure [] |
| 99 | + Next x xs' -> (x:) <$> (unListT xs' >>= force) |
| 100 | + |
| 101 | +ofList :: Monad m => [a] -> Elem m a |
| 102 | +ofList [] = Done |
| 103 | +ofList (x:xs) = Next x $ ListT $ pure $ ofList xs |
| 104 | + |
| 105 | +streamProofs :: forall ext err s m goal meta. (MonadExtract meta ext err s m) => s -> ProofStateT ext ext err s m goal -> ListT m (Either err (Proof s meta goal ext)) |
| 106 | +streamProofs s p = ListT $ go s [] pure p |
| 107 | + where |
| 108 | + go :: s -> [(meta, goal)] -> (err -> m err) -> ProofStateT ext ext err s m goal -> m (Elem m (Either err (Proof s meta goal ext))) |
| 109 | + go s goals _ (Subgoal goal k) = do |
| 110 | + (s', (meta, h)) <- newHole s |
| 111 | + -- Note [Handler Reset]: |
| 112 | + -- We reset the handler stack to avoid the handlers leaking across subgoals. |
| 113 | + -- This would happen when we had a handler that wasn't followed by an error call. |
| 114 | + -- pair >> goal >>= \g -> (handler_ $ \_ -> traceM $ "Handling " <> show g) <|> failure "Error" |
| 115 | + -- We would see the "Handling a" message when solving for b. |
| 116 | + go s' (goals ++ [(meta, goal)]) pure $ k h |
| 117 | + go s goals handlers (Effect m) = m >>= go s goals handlers |
| 118 | + go s goals handlers (Stateful f) = |
| 119 | + let (s', p) = f s |
| 120 | + in go s' goals handlers p |
| 121 | + go s goals handlers (Alt p1 p2) = |
| 122 | + unListT $ ListT (go s goals handlers p1) <|> ListT (go s goals handlers p2) |
| 123 | + go s goals handlers (Interleave p1 p2) = |
| 124 | + interleaveT <$> go s goals handlers p1 <*> go s goals handlers p2 |
| 125 | + go s goals handlers (Commit p1 p2) = do |
| 126 | + solns <- force =<< go s goals handlers p1 |
| 127 | + if any isRight solns then pure $ ofList solns else go s goals handlers p2 |
| 128 | + go _ _ _ Empty = pure Done |
| 129 | + go _ _ handlers (Failure err _) = do |
| 130 | + annErr <- handlers err |
| 131 | + pure $ point $ Left annErr |
| 132 | + go s goals handlers (Handle p h) = |
| 133 | + -- Note [Handler ordering]: |
| 134 | + -- If we have multiple handlers in scope, then we want the handlers closer to the error site to |
| 135 | + -- run /first/. This allows the handlers up the stack to add their annotations on top of the |
| 136 | + -- ones lower down, which is the behavior that we desire. |
| 137 | + -- IE: for @handler f >> handler g >> failure err@, @g@ ought to be run before @f@. |
| 138 | + go s goals (h >=> handlers) p |
| 139 | + go s goals _ (Axiom ext) = pure $ point $ Right (Proof ext s goals) |
| 140 | + |
0 commit comments