-- | 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 qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.GHC.Misc
import           Liquid.GHC.API
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.Specs

--------------------------------------------------------------------------------
specToBare :: SpecType -> BareType
--------------------------------------------------------------------------------
specToBare :: SpecType -> BareType
specToBare = (RTyCon -> BTyCon) -> (RTyVar -> BTyVar) -> SpecType -> BareType
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 = (LocSpecType -> LocBareType)
-> (DataCon -> Located LHName) -> SpecMeasure -> BareMeasure
forall a b c d.
(a -> b) -> (c -> d) -> MeasureV Symbol a c -> MeasureV Symbol b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((SpecType -> BareType) -> LocSpecType -> LocBareType
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> BareType
specToBare) DataCon -> Located LHName
dataConToBare

dataConToBare :: DataCon -> F.Located LHName
dataConToBare :: DataCon -> Located LHName
dataConToBare DataCon
d = TyVar -> LHName
makeGHCLHNameFromId (TyVar -> LHName) -> (DataCon -> TyVar) -> DataCon -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> TyVar
dataConWorkId (DataCon -> LHName) -> Located DataCon -> Located LHName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCon -> Located DataCon
forall a. NamedThing a => a -> Located a
locNamedThing DataCon
d

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

specToBareTV :: RTyVar -> BTyVar
specToBareTV :: RTyVar -> BTyVar
specToBareTV (RTV TyVar
α) = LocSymbol -> BTyVar
BTV (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (TyVar -> Symbol) -> Located TyVar -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVar -> Located TyVar
forall a. NamedThing a => a -> Located a
locNamedThing 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 = RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
forall {r}. RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go
  where
    -- go :: RType c1 tv1 r -> RType c2 tv2 r
    go :: RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go (RVar tv1
α r
r)          = tv2 -> r -> RTypeV Symbol c2 tv2 r
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar  (tv1 -> tv2
vF tv1
α) r
r
    go (RAllT RTVUV Symbol c1 tv1
α RTypeV Symbol c1 tv1 r
t r
r)       = RTVUV Symbol c2 tv2
-> RTypeV Symbol c2 tv2 r -> r -> RTypeV Symbol c2 tv2 r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT (RTVUV Symbol c1 tv1 -> RTVUV Symbol c2 tv2
goRTV RTVUV Symbol c1 tv1
α) (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t) r
r
    go (RAllP PVUV Symbol c1 tv1
π RTypeV Symbol c1 tv1 r
t)         = PVUV Symbol c2 tv2
-> RTypeV Symbol c2 tv2 r -> RTypeV Symbol c2 tv2 r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP (PVUV Symbol c1 tv1 -> PVUV Symbol c2 tv2
goPV  PVUV Symbol c1 tv1
π) (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t)
    go (RFun Symbol
x RFInfo
i RTypeV Symbol c1 tv1 r
t RTypeV Symbol c1 tv1 r
t' r
r)   = Symbol
-> RFInfo
-> RTypeV Symbol c2 tv2 r
-> RTypeV Symbol c2 tv2 r
-> r
-> RTypeV Symbol c2 tv2 r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun   Symbol
x RFInfo
i      (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t) (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t') r
r
    go (RAllE Symbol
x RTypeV Symbol c1 tv1 r
t RTypeV Symbol c1 tv1 r
t')      = Symbol
-> RTypeV Symbol c2 tv2 r
-> RTypeV Symbol c2 tv2 r
-> RTypeV Symbol c2 tv2 r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
x         (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t) (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t')
    go (REx Symbol
x RTypeV Symbol c1 tv1 r
t RTypeV Symbol c1 tv1 r
t')        = Symbol
-> RTypeV Symbol c2 tv2 r
-> RTypeV Symbol c2 tv2 r
-> RTypeV Symbol c2 tv2 r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx   Symbol
x         (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t) (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t')
    go (RAppTy RTypeV Symbol c1 tv1 r
t RTypeV Symbol c1 tv1 r
t' r
r)     = RTypeV Symbol c2 tv2 r
-> RTypeV Symbol c2 tv2 r -> r -> RTypeV Symbol c2 tv2 r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy          (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t) (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t') r
r
    go (RApp c1
c [RTypeV Symbol c1 tv1 r]
ts [RTPropV Symbol c1 tv1 r]
rs r
r)    = c2
-> [RTypeV Symbol c2 tv2 r]
-> [RTPropV Symbol c2 tv2 r]
-> r
-> RTypeV Symbol c2 tv2 r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp  (c1 -> c2
cF c1
c)    (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r)
-> [RTypeV Symbol c1 tv1 r] -> [RTypeV Symbol c2 tv2 r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeV Symbol c1 tv1 r]
ts) (RTPropV Symbol c1 tv1 r -> RTPropV Symbol c2 tv2 r
goRTP (RTPropV Symbol c1 tv1 r -> RTPropV Symbol c2 tv2 r)
-> [RTPropV Symbol c1 tv1 r] -> [RTPropV Symbol c2 tv2 r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropV Symbol c1 tv1 r]
rs) r
r
    go (RRTy [(Symbol, RTypeV Symbol c1 tv1 r)]
xts r
r Oblig
o RTypeV Symbol c1 tv1 r
t)    = [(Symbol, RTypeV Symbol c2 tv2 r)]
-> r -> Oblig -> RTypeV Symbol c2 tv2 r -> RTypeV Symbol c2 tv2 r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy  ((RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r)
-> (Symbol, RTypeV Symbol c1 tv1 r)
-> (Symbol, RTypeV Symbol c2 tv2 r)
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go ((Symbol, RTypeV Symbol c1 tv1 r)
 -> (Symbol, RTypeV Symbol c2 tv2 r))
-> [(Symbol, RTypeV Symbol c1 tv1 r)]
-> [(Symbol, RTypeV Symbol c2 tv2 r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeV Symbol c1 tv1 r)]
xts) r
r Oblig
o (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t)
    go (RExprArg Located (ExprV Symbol)
e)        = Located (ExprV Symbol) -> RTypeV Symbol c2 tv2 r
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg Located (ExprV Symbol)
e
    go (RHole r
r)           = r -> RTypeV Symbol c2 tv2 r
forall v c tv r. r -> RTypeV v c tv r
RHole r
r

    -- go' :: RType c1 tv1 () -> RType c2 tv2 ()
    go' :: RType c1 tv1 r -> RType c2 tv2 r
go' = (c1 -> c2) -> (tv1 -> tv2) -> RType c1 tv1 r -> RType c2 tv2 r
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 :: RTPropV Symbol c1 tv1 r -> RTPropV Symbol c2 tv2 r
goRTP (RProp [(Symbol, RTypeV Symbol c1 tv1 ())]
s (RHole r
r)) = [(Symbol, RTypeV Symbol c2 tv2 ())]
-> RTypeV Symbol c2 tv2 r -> RTPropV Symbol c2 tv2 r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ((RTypeV Symbol c1 tv1 () -> RTypeV Symbol c2 tv2 ())
-> (Symbol, RTypeV Symbol c1 tv1 ())
-> (Symbol, RTypeV Symbol c2 tv2 ())
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RTypeV Symbol c1 tv1 () -> RTypeV Symbol c2 tv2 ()
forall {r}. RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go' ((Symbol, RTypeV Symbol c1 tv1 ())
 -> (Symbol, RTypeV Symbol c2 tv2 ()))
-> [(Symbol, RTypeV Symbol c1 tv1 ())]
-> [(Symbol, RTypeV Symbol c2 tv2 ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeV Symbol c1 tv1 ())]
s) (r -> RTypeV Symbol c2 tv2 r
forall v c tv r. r -> RTypeV v c tv r
RHole r
r)
    goRTP (RProp [(Symbol, RTypeV Symbol c1 tv1 ())]
s RTypeV Symbol c1 tv1 r
t)         = [(Symbol, RTypeV Symbol c2 tv2 ())]
-> RTypeV Symbol c2 tv2 r -> RTPropV Symbol c2 tv2 r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ((RTypeV Symbol c1 tv1 () -> RTypeV Symbol c2 tv2 ())
-> (Symbol, RTypeV Symbol c1 tv1 ())
-> (Symbol, RTypeV Symbol c2 tv2 ())
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RTypeV Symbol c1 tv1 () -> RTypeV Symbol c2 tv2 ()
forall {r}. RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go' ((Symbol, RTypeV Symbol c1 tv1 ())
 -> (Symbol, RTypeV Symbol c2 tv2 ()))
-> [(Symbol, RTypeV Symbol c1 tv1 ())]
-> [(Symbol, RTypeV Symbol c2 tv2 ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeV Symbol c1 tv1 ())]
s) (RTypeV Symbol c1 tv1 r -> RTypeV Symbol c2 tv2 r
go RTypeV Symbol c1 tv1 r
t)

    -- goRTV :: RTVU c1 tv1 -> RTVU c2 tv2
    goRTV :: RTVUV Symbol c1 tv1 -> RTVUV Symbol c2 tv2
goRTV = (c1 -> c2)
-> (tv1 -> tv2) -> RTVUV Symbol c1 tv1 -> RTVUV Symbol c2 tv2
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 :: PVUV Symbol c1 tv1 -> PVUV Symbol c2 tv2
goPV = (c1 -> c2)
-> (tv1 -> tv2) -> PVUV Symbol c1 tv1 -> PVUV Symbol c2 tv2
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 (RTypeV Symbol c1 tv1 ())
z) = tv2
-> RTVInfo (RTypeV Symbol c2 tv2 ())
-> RTVar tv2 (RTypeV Symbol c2 tv2 ())
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar (tv1 -> tv2
vF tv1
α) ((c1 -> c2)
-> (tv1 -> tv2)
-> RTypeV Symbol c1 tv1 ()
-> RTypeV Symbol c2 tv2 ()
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 (RTypeV Symbol c1 tv1 () -> RTypeV Symbol c2 tv2 ())
-> RTVInfo (RTypeV Symbol c1 tv1 ())
-> RTVInfo (RTypeV Symbol c2 tv2 ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTVInfo (RTypeV Symbol 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 RTypeV Symbol c1 tv1 ()
k Symbol
y [(RTypeV Symbol c1 tv1 (), Symbol, ExprV Symbol)]
txes) = Symbol
-> RTypeV Symbol c2 tv2 ()
-> Symbol
-> [(RTypeV Symbol c2 tv2 (), Symbol, ExprV Symbol)]
-> PVarV Symbol (RTypeV Symbol c2 tv2 ())
forall v t.
Symbol -> t -> Symbol -> [(t, Symbol, ExprV v)] -> PVarV v t
PV Symbol
sym RTypeV Symbol c2 tv2 ()
k' Symbol
y [(RTypeV Symbol c2 tv2 (), Symbol, ExprV Symbol)]
txes'
  where
    txes' :: [(RTypeV Symbol c2 tv2 (), Symbol, ExprV Symbol)]
txes'                  = [ (RTypeV Symbol c1 tv1 () -> RTypeV Symbol c2 tv2 ()
forall {r}. RType c1 tv1 r -> RType c2 tv2 r
tx RTypeV Symbol c1 tv1 ()
t, Symbol
x, ExprV Symbol
e) | (RTypeV Symbol c1 tv1 ()
t, Symbol
x, ExprV Symbol
e) <- [(RTypeV Symbol c1 tv1 (), Symbol, ExprV Symbol)]
txes]
    k' :: RTypeV Symbol c2 tv2 ()
k'                     = RTypeV Symbol c1 tv1 () -> RTypeV Symbol c2 tv2 ()
forall {r}. RType c1 tv1 r -> RType c2 tv2 r
tx RTypeV Symbol c1 tv1 ()
k
    tx :: RType c1 tv1 r -> RType c2 tv2 r
tx                     = (c1 -> c2) -> (tv1 -> tv2) -> RType c1 tv1 r -> RType c2 tv2 r
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