-- | 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           DataCon
import           Data.Bifunctor

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

--------------------------------------------------------------------------------
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 = (Located SpecType -> Located BareType)
-> (DataCon -> LocSymbol) -> SpecMeasure -> BareMeasure
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((SpecType -> BareType) -> Located SpecType -> Located BareType
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 (Symbol -> Symbol) -> (DataCon -> Symbol) -> DataCon -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol) (DataCon -> Symbol) -> Located DataCon -> LocSymbol
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
  where
    _msg :: [Char]
_msg  = [Char]
"dataConToBare dc = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DataCon -> [Char]
forall a. Show a => a -> [Char]
show DataCon
d [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" v = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Id -> [Char]
forall a. Show a => a -> [Char]
show Id
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" vx = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
vx
    v :: Id
v     = DataCon -> Id
dataConWorkId DataCon
d
    vx :: Symbol
vx    = Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
v

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 Id
α) = Symbol -> BTyVar
BTV (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
α)

txRType :: (c1 -> c2) -> (tv1 -> tv2) -> RType c1 tv1 r -> RType c2 tv2 r
txRType :: (c1 -> c2) -> (tv1 -> tv2) -> RType c1 tv1 r -> RType c2 tv2 r
txRType c1 -> c2
cF tv1 -> tv2
vF = RType c1 tv1 r -> RType c2 tv2 r
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)          = tv2 -> r -> RType c2 tv2 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)       = RTVU c2 tv2 -> RType c2 tv2 r -> r -> RType c2 tv2 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)         = PVU c2 tv2 -> RType c2 tv2 r -> RType c2 tv2 r
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 (RImpF Symbol
x RType c1 tv1 r
t RType c1 tv1 r
t' r
r)     = Symbol -> RType c2 tv2 r -> RType c2 tv2 r -> r -> RType c2 tv2 r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RImpF  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') r
r
    go (RFun Symbol
x RType c1 tv1 r
t RType c1 tv1 r
t' r
r)     = Symbol -> RType c2 tv2 r -> RType c2 tv2 r -> r -> RType c2 tv2 r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun  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') r
r
    go (RAllE Symbol
x RType c1 tv1 r
t RType c1 tv1 r
t')      = Symbol -> RType c2 tv2 r -> RType c2 tv2 r -> RType c2 tv2 r
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')        = Symbol -> RType c2 tv2 r -> RType c2 tv2 r -> RType c2 tv2 r
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)     = RType c2 tv2 r -> RType c2 tv2 r -> r -> RType c2 tv2 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)    = c2 -> [RType c2 tv2 r] -> [RTProp c2 tv2 r] -> r -> RType c2 tv2 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 (RType c1 tv1 r -> RType c2 tv2 r)
-> [RType c1 tv1 r] -> [RType c2 tv2 r]
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 (RTProp c1 tv1 r -> RTProp c2 tv2 r)
-> [RTProp c1 tv1 r] -> [RTProp c2 tv2 r]
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)    = [(Symbol, RType c2 tv2 r)]
-> r -> Oblig -> RType c2 tv2 r -> RType c2 tv2 r
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy  ((RType c1 tv1 r -> RType c2 tv2 r)
-> (Symbol, RType c1 tv1 r) -> (Symbol, RType c2 tv2 r)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd RType c1 tv1 r -> RType c2 tv2 r
go ((Symbol, RType c1 tv1 r) -> (Symbol, RType c2 tv2 r))
-> [(Symbol, RType c1 tv1 r)] -> [(Symbol, RType c2 tv2 r)]
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)        = Located Expr -> RType c2 tv2 r
forall c tv r. Located Expr -> RType c tv r
RExprArg Located Expr
e
    go (RHole r
r)           = r -> RType c2 tv2 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' = (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 :: RTProp c1 tv1 r -> RTProp c2 tv2 r
goRTP (RProp [(Symbol, RType c1 tv1 ())]
s (RHole r
r)) = [(Symbol, RType c2 tv2 ())] -> RType c2 tv2 r -> RTProp c2 tv2 r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ((RType c1 tv1 () -> RType c2 tv2 ())
-> (Symbol, RType c1 tv1 ()) -> (Symbol, RType c2 tv2 ())
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd RType c1 tv1 () -> RType c2 tv2 ()
forall r. RType c1 tv1 r -> RType c2 tv2 r
go' ((Symbol, RType c1 tv1 ()) -> (Symbol, RType c2 tv2 ()))
-> [(Symbol, RType c1 tv1 ())] -> [(Symbol, RType c2 tv2 ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c1 tv1 ())]
s) (r -> RType c2 tv2 r
forall c tv r. r -> RType c tv r
RHole r
r)
    goRTP (RProp [(Symbol, RType c1 tv1 ())]
s RType c1 tv1 r
t)         = [(Symbol, RType c2 tv2 ())] -> RType c2 tv2 r -> RTProp c2 tv2 r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ((RType c1 tv1 () -> RType c2 tv2 ())
-> (Symbol, RType c1 tv1 ()) -> (Symbol, RType c2 tv2 ())
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd RType c1 tv1 () -> RType c2 tv2 ()
forall r. RType c1 tv1 r -> RType c2 tv2 r
go' ((Symbol, RType c1 tv1 ()) -> (Symbol, RType c2 tv2 ()))
-> [(Symbol, RType c1 tv1 ())] -> [(Symbol, RType c2 tv2 ())]
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 = (c1 -> c2) -> (tv1 -> tv2) -> RTVU c1 tv1 -> RTVU 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 :: PVU c1 tv1 -> PVU c2 tv2
goPV = (c1 -> c2) -> (tv1 -> tv2) -> PVU c1 tv1 -> PVU 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 :: (c1 -> c2) -> (tv1 -> tv2) -> RTVU c1 tv1 -> RTVU c2 tv2
txRTV c1 -> c2
cF tv1 -> tv2
vF (RTVar tv1
α RTVInfo (RType c1 tv1 ())
z) = tv2 -> RTVInfo (RType c2 tv2 ()) -> RTVU c2 tv2
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar (tv1 -> tv2
vF tv1
α) ((c1 -> c2) -> (tv1 -> tv2) -> RType c1 tv1 () -> RType 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 (RType c1 tv1 () -> RType c2 tv2 ())
-> RTVInfo (RType c1 tv1 ()) -> RTVInfo (RType c2 tv2 ())
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 :: (c1 -> c2) -> (tv1 -> tv2) -> PVU c1 tv1 -> PVU c2 tv2
txPV c1 -> c2
cF tv1 -> tv2
vF (PV Symbol
x PVKind (RType c1 tv1 ())
k Symbol
y [(RType c1 tv1 (), Symbol, Expr)]
txes) = Symbol
-> PVKind (RType c2 tv2 ())
-> Symbol
-> [(RType c2 tv2 (), Symbol, Expr)]
-> PVU c2 tv2
forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
x PVKind (RType c2 tv2 ())
k' Symbol
y [(RType c2 tv2 (), Symbol, Expr)]
txes'
  where
    txes' :: [(RType c2 tv2 (), Symbol, Expr)]
txes'                  = [ (RType c1 tv1 () -> RType c2 tv2 ()
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'                     = RType c1 tv1 () -> RType c2 tv2 ()
forall r. RType c1 tv1 r -> RType c2 tv2 r
tx (RType c1 tv1 () -> RType c2 tv2 ())
-> PVKind (RType c1 tv1 ()) -> PVKind (RType c2 tv2 ())
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                     = (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