-- | This module contains functions that convert things
--   to their `Bare` versions, e.g. SpecType -> BareType etc.

module Language.Haskell.Liquid.Bare.ToBare
  ( -- * Types
    specToBare

    -- * Measures
  , measureToBare
  )
  where

import           Data.Bifunctor

import           Language.Fixpoint.Misc (mapSnd)
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.GHC.Misc
import           Liquid.GHC.API
import           Language.Haskell.Liquid.Types
-- import           Language.Haskell.Liquid.Measure
-- import           Language.Haskell.Liquid.Types.RefType

--------------------------------------------------------------------------------
specToBare :: SpecType -> BareType
--------------------------------------------------------------------------------
specToBare :: SpecType -> BareType
specToBare = forall c1 c2 tv1 tv2 r.
(c1 -> c2) -> (tv1 -> tv2) -> RType c1 tv1 r -> RType c2 tv2 r
txRType RTyCon -> BTyCon
specToBareTC RTyVar -> BTyVar
specToBareTV

-- specToBare t = F.tracepp ("specToBare t2 = " ++ F.showpp t2)  t1
  -- where
    -- t1       = bareOfType . toType $ t
    -- t2       = _specToBare           t


--------------------------------------------------------------------------------
measureToBare :: SpecMeasure -> BareMeasure
--------------------------------------------------------------------------------
measureToBare :: SpecMeasure -> BareMeasure
measureToBare = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> BareType
specToBare) DataCon -> LocSymbol
dataConToBare

dataConToBare :: DataCon -> LocSymbol
dataConToBare :: DataCon -> LocSymbol
dataConToBare DataCon
d = Symbol -> Symbol
dropModuleNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. NamedThing a => a -> Located a
locNamedThing DataCon
d
  where
    _msg :: [Char]
_msg  = [Char]
"dataConToBare dc = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show DataCon
d forall a. [a] -> [a] -> [a]
++ [Char]
" v = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TyVar
v forall a. [a] -> [a] -> [a]
++ [Char]
" vx = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Symbol
vx
    v :: TyVar
v     = DataCon -> TyVar
dataConWorkId DataCon
d
    vx :: Symbol
vx    = forall a. Symbolic a => a -> Symbol
F.symbol TyVar
v

specToBareTC :: RTyCon -> BTyCon
specToBareTC :: RTyCon -> BTyCon
specToBareTC = TyCon -> BTyCon
tyConBTyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTyCon -> TyCon
rtc_tc

specToBareTV :: RTyVar -> BTyVar
specToBareTV :: RTyVar -> BTyVar
specToBareTV (RTV TyVar
α) = Symbol -> BTyVar
BTV (forall a. Symbolic a => a -> Symbol
F.symbol TyVar
α)

txRType :: (c1 -> c2) -> (tv1 -> tv2) -> RType c1 tv1 r -> RType c2 tv2 r
txRType :: forall c1 c2 tv1 tv2 r.
(c1 -> c2) -> (tv1 -> tv2) -> RType c1 tv1 r -> RType c2 tv2 r
txRType c1 -> c2
cF tv1 -> tv2
vF = forall {r}. RType c1 tv1 r -> RType c2 tv2 r
go
  where
    -- go :: RType c1 tv1 r -> RType c2 tv2 r
    go :: RType c1 tv1 r -> RType c2 tv2 r
go (RVar tv1
α r
r)          = forall c tv r. tv -> r -> RType c tv r
RVar  (tv1 -> tv2
vF tv1
α) r
r
    go (RAllT RTVU c1 tv1
α RType c1 tv1 r
t r
r)       = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (RTVU c1 tv1 -> RTVU c2 tv2
goRTV RTVU c1 tv1
α) (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t) r
r
    go (RAllP PVU c1 tv1
π RType c1 tv1 r
t)         = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP (PVU c1 tv1 -> PVU c2 tv2
goPV  PVU c1 tv1
π) (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t)
    go (RFun Symbol
x RFInfo
i RType c1 tv1 r
t RType c1 tv1 r
t' r
r)   = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun   Symbol
x RFInfo
i      (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t) (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t') r
r
    go (RAllE Symbol
x RType c1 tv1 r
t RType c1 tv1 r
t')      = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x         (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t) (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t')
    go (REx Symbol
x RType c1 tv1 r
t RType c1 tv1 r
t')        = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx   Symbol
x         (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t) (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t')
    go (RAppTy RType c1 tv1 r
t RType c1 tv1 r
t' r
r)     = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy          (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t) (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t') r
r
    go (RApp c1
c [RType c1 tv1 r]
ts [RTProp c1 tv1 r]
rs r
r)    = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp  (c1 -> c2
cF c1
c)    (RType c1 tv1 r -> RType c2 tv2 r
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c1 tv1 r]
ts) (RTProp c1 tv1 r -> RTProp c2 tv2 r
goRTP forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTProp c1 tv1 r]
rs) r
r
    go (RRTy [(Symbol, RType c1 tv1 r)]
xts r
r Oblig
o RType c1 tv1 r
t)    = forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy  (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd RType c1 tv1 r -> RType c2 tv2 r
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c1 tv1 r)]
xts) r
r Oblig
o (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t)
    go (RExprArg Located Expr
e)        = forall c tv r. Located Expr -> RType c tv r
RExprArg Located Expr
e
    go (RHole r
r)           = forall c tv r. r -> RType c tv r
RHole r
r

    -- go' :: RType c1 tv1 () -> RType c2 tv2 ()
    go' :: RType c1 tv1 r -> RType c2 tv2 r
go' = forall c1 c2 tv1 tv2 r.
(c1 -> c2) -> (tv1 -> tv2) -> RType c1 tv1 r -> RType c2 tv2 r
txRType c1 -> c2
cF tv1 -> tv2
vF

    -- goRTP :: RTProp c1 tv1 r -> RTProp c2 tv2 r
    goRTP :: RTProp c1 tv1 r -> RTProp c2 tv2 r
goRTP (RProp [(Symbol, RType c1 tv1 ())]
s (RHole r
r)) = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd forall {r}. RType c1 tv1 r -> RType c2 tv2 r
go' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c1 tv1 ())]
s) (forall c tv r. r -> RType c tv r
RHole r
r)
    goRTP (RProp [(Symbol, RType c1 tv1 ())]
s RType c1 tv1 r
t)         = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd forall {r}. RType c1 tv1 r -> RType c2 tv2 r
go' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c1 tv1 ())]
s) (RType c1 tv1 r -> RType c2 tv2 r
go RType c1 tv1 r
t)

    -- goRTV :: RTVU c1 tv1 -> RTVU c2 tv2
    goRTV :: RTVU c1 tv1 -> RTVU c2 tv2
goRTV = forall c1 c2 tv1 tv2.
(c1 -> c2) -> (tv1 -> tv2) -> RTVU c1 tv1 -> RTVU c2 tv2
txRTV c1 -> c2
cF tv1 -> tv2
vF

    -- goPV :: PVU c1 tv1 -> PVU c2 tv2
    goPV :: PVU c1 tv1 -> PVU c2 tv2
goPV = forall c1 c2 tv1 tv2.
(c1 -> c2) -> (tv1 -> tv2) -> PVU c1 tv1 -> PVU c2 tv2
txPV c1 -> c2
cF tv1 -> tv2
vF

txRTV :: (c1 -> c2) -> (tv1 -> tv2) -> RTVU c1 tv1 -> RTVU c2 tv2
txRTV :: forall c1 c2 tv1 tv2.
(c1 -> c2) -> (tv1 -> tv2) -> RTVU c1 tv1 -> RTVU c2 tv2
txRTV c1 -> c2
cF tv1 -> tv2
vF (RTVar tv1
α RTVInfo (RType c1 tv1 ())
z) = forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar (tv1 -> tv2
vF tv1
α) (forall c1 c2 tv1 tv2 r.
(c1 -> c2) -> (tv1 -> tv2) -> RType c1 tv1 r -> RType c2 tv2 r
txRType c1 -> c2
cF tv1 -> tv2
vF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTVInfo (RType c1 tv1 ())
z)

txPV :: (c1 -> c2) -> (tv1 -> tv2) -> PVU c1 tv1 -> PVU c2 tv2
txPV :: forall c1 c2 tv1 tv2.
(c1 -> c2) -> (tv1 -> tv2) -> PVU c1 tv1 -> PVU c2 tv2
txPV c1 -> c2
cF tv1 -> tv2
vF (PV Symbol
sym PVKind (RType c1 tv1 ())
k Symbol
y [(RType c1 tv1 (), Symbol, Expr)]
txes) = forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
sym PVKind (RType c2 tv2 ())
k' Symbol
y [(RType c2 tv2 (), Symbol, Expr)]
txes'
  where
    txes' :: [(RType c2 tv2 (), Symbol, Expr)]
txes'                  = [ (forall {r}. RType c1 tv1 r -> RType c2 tv2 r
tx RType c1 tv1 ()
t, Symbol
x, Expr
e) | (RType c1 tv1 ()
t, Symbol
x, Expr
e) <- [(RType c1 tv1 (), Symbol, Expr)]
txes]
    k' :: PVKind (RType c2 tv2 ())
k'                     = forall {r}. RType c1 tv1 r -> RType c2 tv2 r
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVKind (RType c1 tv1 ())
k
    tx :: RType c1 tv1 r -> RType c2 tv2 r
tx                     = forall c1 c2 tv1 tv2 r.
(c1 -> c2) -> (tv1 -> tv2) -> RType c1 tv1 r -> RType c2 tv2 r
txRType c1 -> c2
cF tv1 -> tv2
vF