{-# LANGUAGE OverloadedStrings #-}

module Language.Haskell.Liquid.Types.Literals
  ( literalFRefType
  , literalFReft
  , literalConst
  , mkI, mkS
  ) where

import Prelude hiding (error)
import Language.Haskell.Liquid.GHC.TypeRep ()
import Liquid.GHC.API hiding (panic)

import Language.Haskell.Liquid.Types.Errors
import Language.Haskell.Liquid.Types.RType
import Language.Haskell.Liquid.Types.RefType
import Language.Haskell.Liquid.Transforms.CoreToLogic (mkLit, mkI, mkS)

import qualified Language.Fixpoint.Types as F

---------------------------------------------------------------
----------------------- Typing Literals -----------------------
---------------------------------------------------------------

makeRTypeBase :: Monoid r => Type -> r -> RType RTyCon RTyVar r
makeRTypeBase :: forall r. Monoid r => Type -> r -> RType RTyCon RTyVar r
makeRTypeBase (TyVarTy Var
α)    r
x
  = RTyVar -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar (Var -> RTyVar
rTyVar Var
α) r
x
makeRTypeBase (TyConApp TyCon
c [Type]
ts) r
x
  = TyCon
-> [RTypeBV Symbol Symbol RTyCon RTyVar r]
-> [RTProp RTyCon RTyVar r]
-> r
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c ((Type -> r -> RTypeBV Symbol Symbol RTyCon RTyVar r
forall r. Monoid r => Type -> r -> RType RTyCon RTyVar r
`makeRTypeBase` r
forall a. Monoid a => a
mempty) (Type -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> [Type] -> [RTypeBV Symbol Symbol RTyCon RTyVar r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts) [] r
x
makeRTypeBase Type
_              r
_
  = Maybe SrcSpan -> String -> RTypeBV Symbol Symbol RTyCon RTyVar r
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"RefType : makeRTypeBase"

literalFRefType :: Literal -> RType RTyCon RTyVar F.Reft
literalFRefType :: Literal -> RType RTyCon RTyVar (ReftBV Symbol Symbol)
literalFRefType Literal
l
  = Type
-> ReftBV Symbol Symbol
-> RType RTyCon RTyVar (ReftBV Symbol Symbol)
forall r. Monoid r => Type -> r -> RType RTyCon RTyVar r
makeRTypeBase (Literal -> Type
literalType Literal
l) (Literal -> ReftBV Symbol Symbol
literalFReft Literal
l)

literalFReft :: Literal -> F.Reft
literalFReft :: Literal -> ReftBV Symbol Symbol
literalFReft Literal
l = ReftBV Symbol Symbol
-> (ExprBV Symbol Symbol -> ReftBV Symbol Symbol)
-> Maybe (ExprBV Symbol Symbol)
-> ReftBV Symbol Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReftBV Symbol Symbol
forall a. Monoid a => a
mempty ExprBV Symbol Symbol -> ReftBV Symbol Symbol
mkReft (Maybe (ExprBV Symbol Symbol) -> ReftBV Symbol Symbol)
-> Maybe (ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ Literal -> Maybe (ExprBV Symbol Symbol)
mkLit Literal
l

mkReft :: F.Expr -> F.Reft
mkReft :: ExprBV Symbol Symbol -> ReftBV Symbol Symbol
mkReft = ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Expression a => a -> ReftBV Symbol Symbol
F.exprReft

-- | `literalConst` returns `Nothing` for unhandled lits because
--    otherwise string-literals show up as global int-constants
--    which blow up qualifier instantiation.

literalConst :: F.TCEmb TyCon -> Literal -> (F.Sort, Maybe F.Expr)
literalConst :: TCEmb TyCon -> Literal -> (Sort, Maybe (ExprBV Symbol Symbol))
literalConst TCEmb TyCon
tce Literal
l = (Sort
t, Literal -> Maybe (ExprBV Symbol Symbol)
mkLit Literal
l)
  where
    t :: Sort
t              = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce (Type -> Sort) -> Type -> Sort
forall a b. (a -> b) -> a -> b
$ Literal -> Type
literalType Literal
l