content: {-# 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 (TyVarTy α)    x
    = RVar (rTyVar α) x
  makeRTypeBase (TyConApp c ts) x
    = rApp c ((`makeRTypeBase` mempty) <$> ts) [] x
  makeRTypeBase _              _
    = panic Nothing "RefType : makeRTypeBase"
  
  literalFRefType :: Literal -> RType RTyCon RTyVar F.Reft
  literalFRefType l
    = makeRTypeBase (literalType l) (literalFReft l)
  
  literalFReft :: Literal -> F.Reft
  literalFReft l = maybe mempty mkReft $ mkLit l
  
  mkReft :: F.Expr -> F.Reft
  mkReft = 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 tce l = (t, mkLit l)
    where
      t              = typeSort tce $ literalType l
  