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

module Plugin.TypeCheck.Nat.Simple.Decode (
	-- * DECODE CT
	decodeAll, decode ) where

import Constraint (Ct)
import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon, typeNatLeqTyCon)
import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon)
import TyCoRep (Type(..), TyLit(..))
import Var (Var)
import Outputable (ppr, text, (<+>))
import Control.Applicative ((<|>))
import Control.Monad ((<=<))
import Control.Monad.Try (Try, throw, rights, Set)
import Data.Log (IsSDoc, fromSDoc)
import Data.Derivation.Expression (Exp(..), ExpType(..))
import Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq)

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

-- * DECODE
-- * BOOLEAN AND NUMBER

---------------------------------------------------------------------------
-- DECODE
---------------------------------------------------------------------------

decodeAll :: (Monoid w, IsSDoc w, Set w w) => [Ct] -> Try w w [Exp Var 'Boolean]
decodeAll :: [Ct] -> Try w w [Exp Var 'Boolean]
decodeAll = [Try w w (Exp Var 'Boolean)] -> Try w w [Exp Var 'Boolean]
forall w a. (Monoid w, Set w w) => [Try w w a] -> Try w w [a]
rights ([Try w w (Exp Var 'Boolean)] -> Try w w [Exp Var 'Boolean])
-> ([Ct] -> [Try w w (Exp Var 'Boolean)])
-> [Ct]
-> Try w w [Exp Var 'Boolean]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ct -> Try w w (Exp Var 'Boolean)
forall w. (Monoid w, IsSDoc w) => Ct -> Try w w (Exp Var 'Boolean)
decode (Ct -> Try w w (Exp Var 'Boolean))
-> [Ct] -> [Try w w (Exp Var 'Boolean)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>)

decode :: (Monoid w, IsSDoc w) => Ct -> Try w w (Exp Var 'Boolean)
decode :: Ct -> Try w w (Exp Var 'Boolean)
decode = (Type -> Type -> Try w w (Exp Var 'Boolean))
-> (Type, Type) -> Try w w (Exp Var 'Boolean)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Try w w (Exp Var 'Boolean)
forall w.
(Monoid w, IsSDoc w) =>
Type -> Type -> Try w w (Exp Var 'Boolean)
decodeTs ((Type, Type) -> Try w w (Exp Var 'Boolean))
-> (Ct -> Try w w (Type, Type)) -> Ct -> Try w w (Exp Var 'Boolean)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Ct -> Try w w (Type, Type)
forall w e. (Monoid w, IsSDoc e) => Ct -> Try e w (Type, Type)
unNomEq

decodeTs :: (Monoid w, IsSDoc w) => Type -> Type -> Try w w (Exp Var 'Boolean)
decodeTs :: Type -> Type -> Try w w (Exp Var 'Boolean)
decodeTs (TyVarTy Var
l) (TyVarTy Var
r) = Exp Var 'Boolean -> Try w w (Exp Var 'Boolean)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp Var 'Boolean -> Try w w (Exp Var 'Boolean))
-> Exp Var 'Boolean -> Try w w (Exp Var 'Boolean)
forall a b. (a -> b) -> a -> b
$ Var -> Exp Var Any
forall v (t :: ExpType). v -> Exp v t
Var Var
l Exp Var Any -> Exp Var Any -> Exp Var 'Boolean
forall v (t :: ExpType). Exp v t -> Exp v t -> Exp v 'Boolean
:== Var -> Exp Var Any
forall v (t :: ExpType). v -> Exp v t
Var Var
r
decodeTs Type
l Type
r = Exp Var 'Boolean -> Exp Var 'Boolean -> Exp Var 'Boolean
forall v (t :: ExpType). Exp v t -> Exp v t -> Exp v 'Boolean
(:==) (Exp Var 'Boolean -> Exp Var 'Boolean -> Exp Var 'Boolean)
-> Try w w (Exp Var 'Boolean)
-> Try w w (Exp Var 'Boolean -> Exp Var 'Boolean)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Try w w (Exp Var 'Boolean)
forall s e.
(Monoid s, IsSDoc e) =>
Type -> Try e s (Exp Var 'Boolean)
exBool Type
l Try w w (Exp Var 'Boolean -> Exp Var 'Boolean)
-> Try w w (Exp Var 'Boolean) -> Try w w (Exp Var 'Boolean)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Try w w (Exp Var 'Boolean)
forall s e.
(Monoid s, IsSDoc e) =>
Type -> Try e s (Exp Var 'Boolean)
exBool Type
r Try w w (Exp Var 'Boolean)
-> Try w w (Exp Var 'Boolean) -> Try w w (Exp Var 'Boolean)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Exp Var 'Number -> Exp Var 'Number -> Exp Var 'Boolean
forall v (t :: ExpType). Exp v t -> Exp v t -> Exp v 'Boolean
(:==) (Exp Var 'Number -> Exp Var 'Number -> Exp Var 'Boolean)
-> Try w w (Exp Var 'Number)
-> Try w w (Exp Var 'Number -> Exp Var 'Boolean)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Try w w (Exp Var 'Number)
forall s e.
(Monoid s, IsSDoc e) =>
Type -> Try e s (Exp Var 'Number)
exNum Type
l Try w w (Exp Var 'Number -> Exp Var 'Boolean)
-> Try w w (Exp Var 'Number) -> Try w w (Exp Var 'Boolean)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Try w w (Exp Var 'Number)
forall s e.
(Monoid s, IsSDoc e) =>
Type -> Try e s (Exp Var 'Number)
exNum Type
r

---------------------------------------------------------------------------
-- BOOLEAN AND NUMBER
---------------------------------------------------------------------------

exBool :: (Monoid s, IsSDoc e) => Type -> Try e s (Exp Var 'Boolean)
exBool :: Type -> Try e s (Exp Var 'Boolean)
exBool (TyVarTy Var
v) = Exp Var 'Boolean -> Try e s (Exp Var 'Boolean)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp Var 'Boolean -> Try e s (Exp Var 'Boolean))
-> Exp Var 'Boolean -> Try e s (Exp Var 'Boolean)
forall a b. (a -> b) -> a -> b
$ Var -> Exp Var 'Boolean
forall v (t :: ExpType). v -> Exp v t
Var Var
v
exBool (TyConApp TyCon
tc [])
	| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedFalseDataCon = Exp Var 'Boolean -> Try e s (Exp Var 'Boolean)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp Var 'Boolean -> Try e s (Exp Var 'Boolean))
-> Exp Var 'Boolean -> Try e s (Exp Var 'Boolean)
forall a b. (a -> b) -> a -> b
$ Bool -> Exp Var 'Boolean
forall v. Bool -> Exp v 'Boolean
Bool Bool
False
	| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon = Exp Var 'Boolean -> Try e s (Exp Var 'Boolean)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp Var 'Boolean -> Try e s (Exp Var 'Boolean))
-> Exp Var 'Boolean -> Try e s (Exp Var 'Boolean)
forall a b. (a -> b) -> a -> b
$ Bool -> Exp Var 'Boolean
forall v. Bool -> Exp v 'Boolean
Bool Bool
True
exBool (TyConApp TyCon
tc [Type
l, Type
r])
	| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatLeqTyCon = Exp Var 'Number -> Exp Var 'Number -> Exp Var 'Boolean
forall v. Exp v 'Number -> Exp v 'Number -> Exp v 'Boolean
(:<=) (Exp Var 'Number -> Exp Var 'Number -> Exp Var 'Boolean)
-> Try e s (Exp Var 'Number)
-> Try e s (Exp Var 'Number -> Exp Var 'Boolean)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Try e s (Exp Var 'Number)
forall s e.
(Monoid s, IsSDoc e) =>
Type -> Try e s (Exp Var 'Number)
exNum Type
l Try e s (Exp Var 'Number -> Exp Var 'Boolean)
-> Try e s (Exp Var 'Number) -> Try e s (Exp Var 'Boolean)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Try e s (Exp Var 'Number)
forall s e.
(Monoid s, IsSDoc e) =>
Type -> Try e s (Exp Var 'Number)
exNum Type
r
exBool Type
t = e -> Try e s (Exp Var 'Boolean)
forall w e a. Monoid w => e -> Try e w a
throw (e -> Try e s (Exp Var 'Boolean))
-> (SDoc -> e) -> SDoc -> Try e s (Exp Var 'Boolean)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> e
forall s. IsSDoc s => SDoc -> s
fromSDoc (SDoc -> Try e s (Exp Var 'Boolean))
-> SDoc -> Try e s (Exp Var 'Boolean)
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"exBool: not boolean:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t

exNum :: (Monoid s, IsSDoc e) => Type -> Try e s (Exp Var 'Number)
exNum :: Type -> Try e s (Exp Var 'Number)
exNum (TyVarTy Var
v) = Exp Var 'Number -> Try e s (Exp Var 'Number)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp Var 'Number -> Try e s (Exp Var 'Number))
-> Exp Var 'Number -> Try e s (Exp Var 'Number)
forall a b. (a -> b) -> a -> b
$ Var -> Exp Var 'Number
forall v (t :: ExpType). v -> Exp v t
Var Var
v
exNum (LitTy (NumTyLit Integer
n)) = Exp Var 'Number -> Try e s (Exp Var 'Number)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp Var 'Number -> Try e s (Exp Var 'Number))
-> Exp Var 'Number -> Try e s (Exp Var 'Number)
forall a b. (a -> b) -> a -> b
$ Integer -> Exp Var 'Number
forall v. Integer -> Exp v 'Number
Const Integer
n
exNum (TyConApp TyCon
tc [Type
l, Type
r])
	| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatAddTyCon = Exp Var 'Number -> Exp Var 'Number -> Exp Var 'Number
forall v. Exp v 'Number -> Exp v 'Number -> Exp v 'Number
(:+) (Exp Var 'Number -> Exp Var 'Number -> Exp Var 'Number)
-> Try e s (Exp Var 'Number)
-> Try e s (Exp Var 'Number -> Exp Var 'Number)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Try e s (Exp Var 'Number)
forall s e.
(Monoid s, IsSDoc e) =>
Type -> Try e s (Exp Var 'Number)
exNum Type
l Try e s (Exp Var 'Number -> Exp Var 'Number)
-> Try e s (Exp Var 'Number) -> Try e s (Exp Var 'Number)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Try e s (Exp Var 'Number)
forall s e.
(Monoid s, IsSDoc e) =>
Type -> Try e s (Exp Var 'Number)
exNum Type
r
	| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatSubTyCon = Exp Var 'Number -> Exp Var 'Number -> Exp Var 'Number
forall v. Exp v 'Number -> Exp v 'Number -> Exp v 'Number
(:-) (Exp Var 'Number -> Exp Var 'Number -> Exp Var 'Number)
-> Try e s (Exp Var 'Number)
-> Try e s (Exp Var 'Number -> Exp Var 'Number)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Try e s (Exp Var 'Number)
forall s e.
(Monoid s, IsSDoc e) =>
Type -> Try e s (Exp Var 'Number)
exNum Type
l Try e s (Exp Var 'Number -> Exp Var 'Number)
-> Try e s (Exp Var 'Number) -> Try e s (Exp Var 'Number)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Try e s (Exp Var 'Number)
forall s e.
(Monoid s, IsSDoc e) =>
Type -> Try e s (Exp Var 'Number)
exNum Type
r
exNum Type
t = e -> Try e s (Exp Var 'Number)
forall w e a. Monoid w => e -> Try e w a
throw (e -> Try e s (Exp Var 'Number))
-> (SDoc -> e) -> SDoc -> Try e s (Exp Var 'Number)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> e
forall s. IsSDoc s => SDoc -> s
fromSDoc (SDoc -> Try e s (Exp Var 'Number))
-> SDoc -> Try e s (Exp Var 'Number)
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"exNum: not number:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t