{-# LANGUAGE BlockArguments, OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Plugin.TypeCheck.Nat.Simple (
	-- * PLUGIN
	plugin ) where

import Prelude hiding (log)

import GhcPlugins (Plugin, Var, ppr)
import Control.Monad.Try (tell)
import Data.Log (Log, (.+.), fromSDoc, SDocStr)
import Data.Derivation.CanDerive (canDerive, givens, wanted)
import Plugin.TypeCheck.Nat.Simple.TypeCheckWith (typeCheckWith)
import Plugin.TypeCheck.Nat.Simple.Decode (decode, decodeAll)

type L = Log SDocStr Var

-- | > type L = Log SDocStr Var
--   >
--   > plugin :: Plugin
--   > plugin = typeCheckWith @L "Plugin.TypeCheck.Nat.Simple" \gs _ w ->
--   >	tell @L $ "givens: " .+. fromSDoc (ppr gs)
--   >	tell @L $ "wanted: " .+. fromSDoc (ppr w)
--   >	uncurry canDerive
--   >		=<< (,) <$> (givens =<< decodeAll gs) <*> (wanted =<< decode w)

plugin :: Plugin
plugin :: Plugin
plugin = String -> ([Ct] -> [Ct] -> Ct -> Try L L Bool) -> Plugin
forall w.
(Monoid w, Outputable w, IsSDoc w, Set w w) =>
String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) -> Plugin
typeCheckWith @L String
"Plugin.TypeCheck.Nat.Simple" \[Ct]
gs [Ct]
_ Ct
w -> do
	forall ws e. Set L ws => L -> Try e ws ()
forall w ws e. Set w ws => w -> Try e ws ()
tell @L (L -> Try L L ()) -> L -> Try L L ()
forall a b. (a -> b) -> a -> b
$ L
"givens: " L -> L -> L
forall s v. Log s v -> Log s v -> Log s v
.+. SDoc -> L
forall s. IsSDoc s => SDoc -> s
fromSDoc ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
gs)
	forall ws e. Set L ws => L -> Try e ws ()
forall w ws e. Set w ws => w -> Try e ws ()
tell @L (L -> Try L L ()) -> L -> Try L L ()
forall a b. (a -> b) -> a -> b
$ L
"wanted: " L -> L -> L
forall s v. Log s v -> Log s v -> Log s v
.+. SDoc -> L
forall s. IsSDoc s => SDoc -> s
fromSDoc (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
w)
	(Givens Var -> Wanted Var -> Try L L Bool)
-> (Givens Var, Wanted Var) -> Try L L Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Givens Var -> Wanted Var -> Try L L Bool
forall s v e.
(IsString s, Ord v) =>
Givens v -> Wanted v -> Try e (Log s v) Bool
canDerive
		((Givens Var, Wanted Var) -> Try L L Bool)
-> Try L L (Givens Var, Wanted Var) -> Try L L Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (,) (Givens Var -> Wanted Var -> (Givens Var, Wanted Var))
-> Try L L (Givens Var)
-> Try L L (Wanted Var -> (Givens Var, Wanted Var))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Exp Var 'Boolean] -> Try L L (Givens Var)
forall s v.
(IsString s, Ord v) =>
[Exp v 'Boolean] -> Try (Log s v) (Log s v) (Givens v)
givens ([Exp Var 'Boolean] -> Try L L (Givens Var))
-> Try L L [Exp Var 'Boolean] -> Try L L (Givens Var)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Ct] -> Try L L [Exp Var 'Boolean]
forall w.
(Monoid w, IsSDoc w, Set w w) =>
[Ct] -> Try w w [Exp Var 'Boolean]
decodeAll [Ct]
gs) Try L L (Wanted Var -> (Givens Var, Wanted Var))
-> Try L L (Wanted Var) -> Try L L (Givens Var, Wanted Var)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Exp Var 'Boolean -> Try L L (Wanted Var)
forall s v.
(IsString s, Ord v) =>
Exp v 'Boolean -> Try (Log s v) (Log s v) (Wanted v)
wanted (Exp Var 'Boolean -> Try L L (Wanted Var))
-> Try L L (Exp Var 'Boolean) -> Try L L (Wanted Var)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Ct -> Try L L (Exp Var 'Boolean)
forall w. (Monoid w, IsSDoc w) => Ct -> Try w w (Exp Var 'Boolean)
decode Ct
w)