{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE StandaloneDeriving        #-}

{-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1.
{-# OPTIONS_GHC -Wno-orphans #-}

module Language.Haskell.Liquid.GHC.TypeRep (
  mkTyArg, 

  showTy
  ) where

import           Language.Haskell.Liquid.GHC.Misc (showPpr)
import           Liquid.GHC.API as Ghc hiding (mkTyArg, showPpr, panic)
import           Language.Fixpoint.Types (symbol)

-- e368f3265b80aeb337fbac3f6a70ee54ab14edfd

mkTyArg :: TyVar -> TyVarBinder
mkTyArg :: TyVar -> TyVarBinder
mkTyArg TyVar
v = TyVar -> ForAllTyFlag -> TyVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
v ForAllTyFlag
Required

instance Eq Type where
  Mult
t1 == :: Mult -> Mult -> Bool
== Mult
t2 = Mult -> Mult -> Bool
eqType' Mult
t1 Mult
t2

eqType' :: Type -> Type -> Bool 
eqType' :: Mult -> Mult -> Bool
eqType' (LitTy TyLit
l1) (LitTy TyLit
l2) 
  = TyLit
l1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
l2  
eqType' (CoercionTy Coercion
_c1) (CoercionTy Coercion
_c2) = Bool
True
eqType'(CastTy Mult
t1 Coercion
_c1) (CastTy Mult
t2 Coercion
_c2) = Mult -> Mult -> Bool
eqType' Mult
t1 Mult
t2
eqType' (FunTy FunTyFlag
a1 Mult
m1 Mult
t11 Mult
t12) (FunTy FunTyFlag
a2 Mult
m2 Mult
t21 Mult
t22)
  = FunTyFlag
a1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
a2 Bool -> Bool -> Bool
&& Mult
m1 Mult -> Mult -> Bool
forall a. Eq a => a -> a -> Bool
== Mult
m2 Bool -> Bool -> Bool
&& Mult -> Mult -> Bool
eqType' Mult
t11 Mult
t21 Bool -> Bool -> Bool
&& Mult -> Mult -> Bool
eqType' Mult
t12 Mult
t22  
eqType' (ForAllTy (Bndr TyVar
v1 ForAllTyFlag
_) Mult
t1) (ForAllTy (Bndr TyVar
v2 ForAllTyFlag
_) Mult
t2) 
  = Mult -> Mult -> Bool
eqType' Mult
t1 (TyVar -> Mult -> Mult -> Mult
substType TyVar
v2 (TyVar -> Mult
TyVarTy TyVar
v1) Mult
t2)
eqType' (TyVarTy TyVar
v1) (TyVarTy TyVar
v2) 
  = TyVar
v1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v2 
eqType' (AppTy Mult
t11 Mult
t12) (AppTy Mult
t21 Mult
t22) 
  = Mult -> Mult -> Bool
eqType' Mult
t11 Mult
t21 Bool -> Bool -> Bool
&& Mult -> Mult -> Bool
eqType' Mult
t12 Mult
t22  
eqType' (TyConApp TyCon
c1 [Mult]
ts1) (TyConApp TyCon
c2 [Mult]
ts2) 
  = TyCon
c1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
c2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Mult -> Mult -> Bool) -> [Mult] -> [Mult] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Mult -> Mult -> Bool
eqType' [Mult]
ts1 [Mult]
ts2) 
eqType' Mult
_ Mult
_ 
  = Bool
False 


deriving instance (Eq tyvar, Eq argf) => Eq (VarBndr tyvar argf)

showTy :: Type -> String 
showTy :: Mult -> [Char]
showTy (TyConApp TyCon
c [Mult]
ts) = [Char]
"(RApp   " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TyCon -> [Char]
forall a. Outputable a => a -> [Char]
showPpr TyCon
c [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
sep' [Char]
", " (Mult -> [Char]
showTy (Mult -> [Char]) -> [Mult] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Mult]
ts) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (AppTy Mult
t1 Mult
t2)   = [Char]
"(TAppTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Mult -> [Char]
showTy Mult
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Mult -> [Char]
showTy Mult
t2) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")" 
showTy (TyVarTy TyVar
v)   = [Char]
"(RVar " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v)  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")" 
showTy (ForAllTy (Bndr TyVar
v ForAllTyFlag
_) Mult
t)  = [Char]
"ForAllTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
". (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++  Mult -> [Char]
showTy Mult
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (FunTy FunTyFlag
af Mult
_m1 Mult
t1 Mult
t2) = [Char]
"FunTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FunTyFlag -> [Char]
forall a. Outputable a => a -> [Char]
showPpr FunTyFlag
af [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Mult -> [Char]
showTy Mult
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
". (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++  Mult -> [Char]
showTy Mult
t2 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (CastTy Mult
_ Coercion
_)    = [Char]
"CastTy"
showTy (CoercionTy Coercion
_)  = [Char]
"CoercionTy"
showTy (LitTy TyLit
_)       = [Char]
"LitTy"

sep' :: String -> [String] -> String
sep' :: [Char] -> [[Char]] -> [Char]
sep' [Char]
_ [[Char]
x] = [Char]
x
sep' [Char]
_ []  = []
sep' [Char]
s ([Char]
x:[[Char]]
xs) = [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
sep' [Char]
s [[Char]]
xs 



-------------------------------------------------------------------------------
-- | GHC Type Substitutions ---------------------------------------------------
-------------------------------------------------------------------------------

substType :: TyVar -> Type -> Type -> Type
substType :: TyVar -> Mult -> Mult -> Mult
substType TyVar
x Mult
tx (TyConApp TyCon
c [Mult]
ts) 
  = TyCon -> [Mult] -> Mult
TyConApp TyCon
c (TyVar -> Mult -> Mult -> Mult
substType TyVar
x Mult
tx (Mult -> Mult) -> [Mult] -> [Mult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Mult]
ts)
substType TyVar
x Mult
tx (AppTy Mult
t1 Mult
t2)   
  = Mult -> Mult -> Mult
AppTy (TyVar -> Mult -> Mult -> Mult
substType TyVar
x Mult
tx Mult
t1) (TyVar -> Mult -> Mult -> Mult
substType TyVar
x Mult
tx Mult
t2)
substType TyVar
x Mult
tx (TyVarTy TyVar
y)   
  | TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
y
  = Mult
tx 
  | Bool
otherwise
  = TyVar -> Mult
TyVarTy TyVar
y 
substType TyVar
x Mult
tx (FunTy FunTyFlag
aaf Mult
m Mult
t1 Mult
t2)
  = FunTyFlag -> Mult -> Mult -> Mult -> Mult
FunTy FunTyFlag
aaf Mult
m (TyVar -> Mult -> Mult -> Mult
substType TyVar
x Mult
tx Mult
t1) (TyVar -> Mult -> Mult -> Mult
substType TyVar
x Mult
tx Mult
t2)
substType TyVar
x Mult
tx f :: Mult
f@(ForAllTy b :: TyVarBinder
b@(Bndr TyVar
y ForAllTyFlag
_) Mult
t)  
  | TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
y 
  = Mult
f
  | Bool
otherwise 
  = TyVarBinder -> Mult -> Mult
ForAllTy TyVarBinder
b (TyVar -> Mult -> Mult -> Mult
substType TyVar
x Mult
tx Mult
t)
substType TyVar
x Mult
tx (CastTy Mult
t Coercion
c)    
  = let ss :: Subst
ss = Subst -> VarSet -> Subst
extendSubstInScopeSet ([TyVar] -> [Mult] -> Subst
HasDebugCallStack => [TyVar] -> [Mult] -> Subst
zipTvSubst [TyVar
x] [Mult
tx]) (Coercion -> VarSet
tyCoVarsOfCo Coercion
c)
     in Mult -> Coercion -> Mult
CastTy (TyVar -> Mult -> Mult -> Mult
substType TyVar
x Mult
tx Mult
t) (HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo Subst
ss Coercion
c)
substType TyVar
x Mult
tx (CoercionTy Coercion
c)  
  = let ss :: Subst
ss = Subst -> VarSet -> Subst
extendSubstInScopeSet ([TyVar] -> [Mult] -> Subst
HasDebugCallStack => [TyVar] -> [Mult] -> Subst
zipTvSubst [TyVar
x] [Mult
tx]) (Coercion -> VarSet
tyCoVarsOfCo Coercion
c)
     in Coercion -> Mult
CoercionTy (Coercion -> Mult) -> Coercion -> Mult
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo Subst
ss Coercion
c
substType TyVar
_ Mult
_  (LitTy TyLit
l)
  = TyLit -> Mult
LitTy TyLit
l