module Language.Haskell.Liquid.Literals (
literalFRefType, literalFReft, literalConst
) where
import TypeRep
import Literal
import Language.Haskell.Liquid.Measure
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.RefType
import Language.Haskell.Liquid.CoreToLogic (mkLit)
import qualified Language.Fixpoint.Types as F
import qualified Data.Text as T
import qualified Data.Text.Encoding as T
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 l
= makeRTypeBase (literalType l) (literalFReft l)
literalFReft l = maybe mempty mkReft $ mkLit l
mkReft e = case e of
F.ESym (F.SL str) ->
F.meet (F.uexprReft e)
(F.reft "v" (F.PAtom F.Eq
(F.EApp (name strLen) [F.EVar "v"])
(F.ECon (F.I (fromIntegral (T.length str))))))
_ -> F.exprReft e
literalConst tce l = (sort, mkLit l)
where
sort = typeSort tce $ literalType l