-- | 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 = Var -> LHName
makeGHCLHNameFromId (Var -> LHName) -> (DataCon -> Var) -> DataCon -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Var
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 Var
α) = LocSymbol -> BTyVar
BTV (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> Located Var -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> Located Var
forall a. NamedThing a => a -> Located a
locNamedThing Var
α)

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 = RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
forall {r}.
RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go
  where
    -- go :: RType c1 tv1 r -> RType c2 tv2 r
    go :: RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go (RVar tv1
α r
r)          = tv2 -> r -> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar  (tv1 -> tv2
vF tv1
α) r
r
    go (RAllT RTVUBV Symbol Symbol c1 tv1
α RTypeBV Symbol Symbol c1 tv1 r
t r
r)       = RTVUBV Symbol Symbol c2 tv2
-> RTypeBV Symbol Symbol c2 tv2 r
-> r
-> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT (RTVUBV Symbol Symbol c1 tv1 -> RTVUBV Symbol Symbol c2 tv2
goRTV RTVUBV Symbol Symbol c1 tv1
α) (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t) r
r
    go (RAllP PVUBV Symbol Symbol c1 tv1
π RTypeBV Symbol Symbol c1 tv1 r
t)         = PVUBV Symbol Symbol c2 tv2
-> RTypeBV Symbol Symbol c2 tv2 r -> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP (PVUBV Symbol Symbol c1 tv1 -> PVUBV Symbol Symbol c2 tv2
goPV  PVUBV Symbol Symbol c1 tv1
π) (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t)
    go (RFun Symbol
x RFInfo
i RTypeBV Symbol Symbol c1 tv1 r
t RTypeBV Symbol Symbol c1 tv1 r
t' r
r)   = Symbol
-> RFInfo
-> RTypeBV Symbol Symbol c2 tv2 r
-> RTypeBV Symbol Symbol c2 tv2 r
-> r
-> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun   Symbol
x RFInfo
i      (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t) (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t') r
r
    go (RAllE Symbol
x RTypeBV Symbol Symbol c1 tv1 r
t RTypeBV Symbol Symbol c1 tv1 r
t')      = Symbol
-> RTypeBV Symbol Symbol c2 tv2 r
-> RTypeBV Symbol Symbol c2 tv2 r
-> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllE Symbol
x         (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t) (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t')
    go (REx Symbol
x RTypeBV Symbol Symbol c1 tv1 r
t RTypeBV Symbol Symbol c1 tv1 r
t')        = Symbol
-> RTypeBV Symbol Symbol c2 tv2 r
-> RTypeBV Symbol Symbol c2 tv2 r
-> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
REx   Symbol
x         (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t) (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t')
    go (RAppTy RTypeBV Symbol Symbol c1 tv1 r
t RTypeBV Symbol Symbol c1 tv1 r
t' r
r)     = RTypeBV Symbol Symbol c2 tv2 r
-> RTypeBV Symbol Symbol c2 tv2 r
-> r
-> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy          (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t) (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t') r
r
    go (RApp c1
c [RTypeBV Symbol Symbol c1 tv1 r]
ts [RTPropBV Symbol Symbol c1 tv1 r]
rs r
r)    = c2
-> [RTypeBV Symbol Symbol c2 tv2 r]
-> [RTPropBV Symbol Symbol c2 tv2 r]
-> r
-> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp  (c1 -> c2
cF c1
c)    (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r)
-> [RTypeBV Symbol Symbol c1 tv1 r]
-> [RTypeBV Symbol Symbol c2 tv2 r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV Symbol Symbol c1 tv1 r]
ts) (RTPropBV Symbol Symbol c1 tv1 r -> RTPropBV Symbol Symbol c2 tv2 r
goRTP (RTPropBV Symbol Symbol c1 tv1 r
 -> RTPropBV Symbol Symbol c2 tv2 r)
-> [RTPropBV Symbol Symbol c1 tv1 r]
-> [RTPropBV Symbol Symbol c2 tv2 r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropBV Symbol Symbol c1 tv1 r]
rs) r
r
    go (RRTy [(Symbol, RTypeBV Symbol Symbol c1 tv1 r)]
xts r
r Oblig
o RTypeBV Symbol Symbol c1 tv1 r
t)    = [(Symbol, RTypeBV Symbol Symbol c2 tv2 r)]
-> r
-> Oblig
-> RTypeBV Symbol Symbol c2 tv2 r
-> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RRTy  ((RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r)
-> (Symbol, RTypeBV Symbol Symbol c1 tv1 r)
-> (Symbol, RTypeBV Symbol 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 RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go ((Symbol, RTypeBV Symbol Symbol c1 tv1 r)
 -> (Symbol, RTypeBV Symbol Symbol c2 tv2 r))
-> [(Symbol, RTypeBV Symbol Symbol c1 tv1 r)]
-> [(Symbol, RTypeBV Symbol Symbol c2 tv2 r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeBV Symbol Symbol c1 tv1 r)]
xts) r
r Oblig
o (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t)
    go (RExprArg Located (ExprBV Symbol Symbol)
e)        = Located (ExprBV Symbol Symbol) -> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg Located (ExprBV Symbol Symbol)
e
    go (RHole r
r)           = r -> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r. r -> RTypeBV b 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 :: RTPropBV Symbol Symbol c1 tv1 r -> RTPropBV Symbol Symbol c2 tv2 r
goRTP (RProp [(Symbol, RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol))]
s (RHole r
r)) = [(Symbol, RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol))]
-> RTypeBV Symbol Symbol c2 tv2 r
-> RTPropBV Symbol Symbol c2 tv2 r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp ((RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol)
 -> RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol))
-> (Symbol, RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol))
-> (Symbol, RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol))
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol)
-> RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol)
forall {r}.
RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go' ((Symbol, RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol))
 -> (Symbol, RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol)))
-> [(Symbol, RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol))]
-> [(Symbol, RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol))]
s) (r -> RTypeBV Symbol Symbol c2 tv2 r
forall b v c tv r. r -> RTypeBV b v c tv r
RHole r
r)
    goRTP (RProp [(Symbol, RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol))]
s RTypeBV Symbol Symbol c1 tv1 r
t)         = [(Symbol, RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol))]
-> RTypeBV Symbol Symbol c2 tv2 r
-> RTPropBV Symbol Symbol c2 tv2 r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp ((RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol)
 -> RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol))
-> (Symbol, RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol))
-> (Symbol, RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol))
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol)
-> RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol)
forall {r}.
RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go' ((Symbol, RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol))
 -> (Symbol, RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol)))
-> [(Symbol, RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol))]
-> [(Symbol, RTypeBV Symbol Symbol c2 tv2 (NoReftB Symbol))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeBV Symbol Symbol c1 tv1 (NoReftB Symbol))]
s) (RTypeBV Symbol Symbol c1 tv1 r -> RTypeBV Symbol Symbol c2 tv2 r
go RTypeBV Symbol Symbol c1 tv1 r
t)

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