module Language.Haskell.Liquid.Literals (
literalFRefType, literalFReft, literalConst
) where
import TypeRep
import Literal
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.RefType
import Language.Haskell.Liquid.CoreToLogic (mkLit)
import Language.Fixpoint.Types (exprReft)
import Data.Monoid
import Control.Applicative
makeRTypeBase (TyVarTy α) x
= RVar (rTyVar α) x
makeRTypeBase (TyConApp c ts) x
= rApp c ((`makeRTypeBase` mempty) <$> ts) [] x
makeRTypeBase _ _
= error "RefType : makeRTypeBase"
literalFRefType tce l
= makeRTypeBase (literalType l) (literalFReft tce l)
literalFReft tce = maybe mempty exprReft . snd . literalConst tce
literalConst tce l = (sort, mkLit l)
where
sort = typeSort tce $ literalType l