{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Plugin.TypeCheck.Nat.Simple.TypeCheckWith (
	-- * TYPE CHECK WITH
	typeCheckWith ) where

import GhcPlugins (
	Plugin(..), defaultPlugin, Expr(..), mkUnivCo, Role(..),
	Outputable, ppr, text )
import TcPluginM (TcPluginM, tcPluginTrace)
import TcRnTypes (TcPlugin(..), TcPluginResult(..))
import Constraint (Ct)
import TcEvidence (EvTerm(..))
import TyCoRep (UnivCoProvenance(..))
import Control.Monad.Try (Try, gatherSuccess, throw, Set)
import Data.Bool (bool)
import Data.Log (IsSDoc, fromSDoc)
import Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq)

---------------------------------------------------------------------------

typeCheckWith :: (Monoid w, Outputable w, IsSDoc w, Set w w) =>
	String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) -> Plugin
typeCheckWith :: String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) -> Plugin
typeCheckWith String
hd [Ct] -> [Ct] -> Ct -> Try w w Bool
ck = Plugin
defaultPlugin { tcPlugin :: TcPlugin
tcPlugin = Maybe TcPlugin -> TcPlugin
forall a b. a -> b -> a
const (Maybe TcPlugin -> TcPlugin) -> Maybe TcPlugin -> TcPlugin
forall a b. (a -> b) -> a -> b
$ TcPlugin -> Maybe TcPlugin
forall a. a -> Maybe a
Just TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
TcPlugin {
	tcPluginInit :: TcPluginM ()
tcPluginInit = () -> TcPluginM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), tcPluginSolve :: () -> TcPluginSolver
tcPluginSolve = TcPluginSolver -> () -> TcPluginSolver
forall a b. a -> b -> a
const (TcPluginSolver -> () -> TcPluginSolver)
-> TcPluginSolver -> () -> TcPluginSolver
forall a b. (a -> b) -> a -> b
$ String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) -> TcPluginSolver
forall w.
(Monoid w, Outputable w, IsSDoc w, Set w w) =>
String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) -> TcPluginSolver
solve String
hd [Ct] -> [Ct] -> Ct -> Try w w Bool
ck,
	tcPluginStop :: () -> TcPluginM ()
tcPluginStop = TcPluginM () -> () -> TcPluginM ()
forall a b. a -> b -> a
const (TcPluginM () -> () -> TcPluginM ())
-> TcPluginM () -> () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ () -> TcPluginM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure () } }

solve :: (Monoid w, Outputable w, IsSDoc w, Set w w) =>
	String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) ->
	[Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
solve :: String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) -> TcPluginSolver
solve String
hd [Ct] -> [Ct] -> Ct -> Try w w Bool
ck [Ct]
gs [Ct]
ds [Ct]
ws = [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [(EvTerm, Ct)]
rs [] TcPluginResult -> TcPluginM () -> TcPluginM TcPluginResult
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> SDoc -> TcPluginM ()
tcPluginTrace String
hd (w -> SDoc
forall a. Outputable a => a -> SDoc
ppr w
lgs)
	where ([(EvTerm, Ct)]
rs, w
lgs) = [Try w w (EvTerm, Ct)] -> ([(EvTerm, Ct)], w)
forall w a. (Monoid w, Set w w) => [Try w w a] -> ([a], w)
gatherSuccess ([Try w w (EvTerm, Ct)] -> ([(EvTerm, Ct)], w))
-> [Try w w (EvTerm, Ct)] -> ([(EvTerm, Ct)], w)
forall a b. (a -> b) -> a -> b
$ String
-> ([Ct] -> [Ct] -> Ct -> Try w w Bool)
-> [Ct]
-> [Ct]
-> Ct
-> Try w w (EvTerm, Ct)
forall s e.
(Monoid s, IsSDoc e) =>
String
-> ([Ct] -> [Ct] -> Ct -> Try e s Bool)
-> [Ct]
-> [Ct]
-> Ct
-> Try e s (EvTerm, Ct)
result String
hd [Ct] -> [Ct] -> Ct -> Try w w Bool
ck [Ct]
gs [Ct]
ds (Ct -> Try w w (EvTerm, Ct)) -> [Ct] -> [Try w w (EvTerm, Ct)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Ct]
ws

result :: (Monoid s, IsSDoc e) =>
	String -> ([Ct] -> [Ct] -> Ct -> Try e s Bool) ->
	[Ct] -> [Ct] -> Ct -> Try e s (EvTerm, Ct)
result :: String
-> ([Ct] -> [Ct] -> Ct -> Try e s Bool)
-> [Ct]
-> [Ct]
-> Ct
-> Try e s (EvTerm, Ct)
result String
hd [Ct] -> [Ct] -> Ct -> Try e s Bool
ck [Ct]
gs [Ct]
ds Ct
w = Ct -> Try e s (Type, Type)
forall w e. (Monoid w, IsSDoc e) => Ct -> Try e w (Type, Type)
unNomEq Ct
w Try e s (Type, Type)
-> ((Type, Type) -> Try e s (EvTerm, Ct)) -> Try e s (EvTerm, Ct)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Type
l, Type
r) ->
	Try e s (EvTerm, Ct)
-> Try e s (EvTerm, Ct) -> Bool -> Try e s (EvTerm, Ct)
forall a. a -> a -> Bool -> a
bool (e -> Try e s (EvTerm, Ct)
forall w e a. Monoid w => e -> Try e w a
throw e
em) ((EvTerm, Ct) -> Try e s (EvTerm, Ct)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Type -> EvTerm
et Type
l Type
r, Ct
w)) (Bool -> Try e s (EvTerm, Ct))
-> Try e s Bool -> Try e s (EvTerm, Ct)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Ct] -> [Ct] -> Ct -> Try e s Bool
ck [Ct]
gs [Ct]
ds Ct
w
	where
	em :: e
em = SDoc -> e
forall s. IsSDoc s => SDoc -> s
fromSDoc (SDoc -> e) -> SDoc -> e
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"result: type checker: return False"
	et :: Type -> Type -> EvTerm
et = ((EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> (Coercion -> EvExpr) -> Coercion -> EvTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> EvExpr
forall b. Coercion -> Expr b
Coercion) (Coercion -> EvTerm) -> (Type -> Coercion) -> Type -> EvTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Type -> Coercion) -> Type -> EvTerm)
-> (Type -> Type -> Coercion) -> Type -> Type -> EvTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (String -> UnivCoProvenance
PluginProv String
hd) Role
Nominal