liquidhaskell-0.8.10.1: src/Language/Haskell/Liquid/Bare/Measure.hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections #-}
-- | This module contains (most of) the code needed to lift Haskell entitites,
-- . code- (CoreBind), and data- (Tycon) definitions into the spec level.
module Language.Haskell.Liquid.Bare.Measure
( makeHaskellMeasures
, makeHaskellInlines
, makeHaskellDataDecls
, makeMeasureSelectors
, makeMeasureSpec
, makeMeasureSpec'
, varMeasures
, makeClassMeasureSpec
-- , makeHaskellBounds
) where
import Data.Default
import qualified Control.Exception as Ex
import Prelude hiding (mapM, error)
import Data.Bifunctor
import qualified Data.Maybe as Mb
import Text.PrettyPrint.HughesPJ (text)
-- import Text.Printf (printf)
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Language.Fixpoint.SortCheck (isFirstOrder)
import qualified Language.Fixpoint.Types as F
import Language.Haskell.Liquid.Transforms.CoreToLogic
import qualified Language.Fixpoint.Misc as Misc
import qualified Language.Haskell.Liquid.Misc as Misc
import Language.Haskell.Liquid.Misc ((.||.))
import qualified Language.Haskell.Liquid.GHC.API as Ghc
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import qualified Language.Haskell.Liquid.Types.RefType as RT
import Language.Haskell.Liquid.Types
-- import Language.Haskell.Liquid.Types.Bounds
import qualified Language.Haskell.Liquid.Measure as Ms
import qualified Language.Haskell.Liquid.Bare.Types as Bare
import qualified Language.Haskell.Liquid.Bare.Resolve as Bare
import qualified Language.Haskell.Liquid.Bare.Expand as Bare
import qualified Language.Haskell.Liquid.Bare.DataType as Bare
import qualified Language.Haskell.Liquid.Bare.ToBare as Bare
--------------------------------------------------------------------------------
makeHaskellMeasures :: GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec
-> [Measure (Located BareType) LocSymbol]
--------------------------------------------------------------------------------
makeHaskellMeasures src tycEnv lmap spec
= Bare.measureToBare <$> ms
where
ms = makeMeasureDefinition tycEnv lmap cbs <$> mSyms
cbs = nonRecCoreBinds (_giCbs src)
mSyms = S.toList (Ms.hmeas spec)
makeMeasureDefinition :: Bare.TycEnv -> LogicMap -> [Ghc.CoreBind] -> LocSymbol
-> Measure LocSpecType Ghc.DataCon
makeMeasureDefinition tycEnv lmap cbs x =
case GM.findVarDef (val x) cbs of
Nothing -> Ex.throw $ errHMeas x "Cannot extract measure from haskell function"
Just (v, def) -> Ms.mkM vx vinfo mdef MsLifted (makeUnSorted (Ghc.varType v) mdef)
where
vx = F.atLoc x (F.symbol v)
mdef = coreToDef' tycEnv lmap vx v def
vinfo = GM.varLocInfo logicType v
makeUnSorted :: Ghc.Type -> [Def LocSpecType Ghc.DataCon] -> UnSortedExprs
makeUnSorted t defs
| isMeasureType ta
= mempty
| otherwise
= map defToUnSortedExpr defs
where
ta = go $ Ghc.expandTypeSynonyms t
go (Ghc.ForAllTy _ t) = go t
go (Ghc.FunTy { Ghc.ft_arg = p, Ghc.ft_res = t}) | Ghc.isClassPred p = go t
go (Ghc.FunTy { Ghc.ft_arg = t }) = t
go t = t -- this should never happen!
isMeasureType (Ghc.TyConApp _ ts) = all Ghc.isTyVarTy ts
isMeasureType _ = False
defToUnSortedExpr def = (xx:(fst <$> binds def),
Ms.bodyPred (F.mkEApp (measure def) [F.expr xx]) (body def))
xx = F.vv $ Just 10000
coreToDef' :: Bare.TycEnv -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
-> [Def LocSpecType Ghc.DataCon]
coreToDef' tycEnv lmap vx v def =
case runToLogic embs lmap dm (errHMeas vx) (coreToDef vx v def) of
Right l -> l
Left e -> Ex.throw e
where
embs = Bare.tcEmbs tycEnv
dm = Bare.tcDataConMap tycEnv
errHMeas :: LocSymbol -> String -> Error
errHMeas x str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str)
--------------------------------------------------------------------------------
makeHaskellInlines :: GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec
-> [(LocSymbol, LMap)]
--------------------------------------------------------------------------------
makeHaskellInlines src embs lmap spec
= makeMeasureInline embs lmap cbs <$> inls
where
cbs = nonRecCoreBinds (_giCbs src)
inls = S.toList (Ms.inlines spec)
makeMeasureInline :: F.TCEmb Ghc.TyCon -> LogicMap -> [Ghc.CoreBind] -> LocSymbol
-> (LocSymbol, LMap)
makeMeasureInline embs lmap cbs x =
case GM.findVarDef (val x) cbs of
Nothing -> Ex.throw $ errHMeas x "Cannot inline haskell function"
Just (v, def) -> (vx, coreToFun' embs Nothing lmap vx v def ok)
where
vx = F.atLoc x (F.symbol v)
ok (xs, e) = LMap vx (F.symbol <$> xs) (either id id e)
-- | @coreToFun'@ takes a @Maybe DataConMap@: we need a proper map when lifting
-- measures and reflects (which have case-of, and hence, need the projection symbols),
-- but NOT when lifting inlines (which do not have case-of).
-- For details, see [NOTE:Lifting-Stages]
coreToFun' :: F.TCEmb Ghc.TyCon -> Maybe Bare.DataConMap -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
-> (([Ghc.Var], Either F.Expr F.Expr) -> a) -> a
coreToFun' embs dmMb lmap x v def ok = either Ex.throw ok act
where
act = runToLogic embs lmap dm err xFun
xFun = coreToFun x v def
err = errHMeas x
dm = Mb.fromMaybe mempty dmMb
nonRecCoreBinds :: [Ghc.CoreBind] -> [Ghc.CoreBind]
nonRecCoreBinds = concatMap go
where
go cb@(Ghc.NonRec _ _) = [cb]
go (Ghc.Rec xes) = [Ghc.NonRec x e | (x, e) <- xes]
-------------------------------------------------------------------------------
makeHaskellDataDecls :: Config -> ModName -> Ms.BareSpec -> [Ghc.TyCon]
-> [DataDecl]
--------------------------------------------------------------------------------
makeHaskellDataDecls cfg name spec tcs
| exactDCFlag cfg = Mb.mapMaybe tyConDataDecl
-- . F.tracepp "makeHaskellDataDecls-3"
. zipMap (hasDataDecl name spec . fst)
-- . F.tracepp "makeHaskellDataDecls-2"
. liftableTyCons
-- . F.tracepp "makeHaskellDataDecls-1"
. filter isReflectableTyCon
$ tcs
| otherwise = []
isReflectableTyCon :: Ghc.TyCon -> Bool
isReflectableTyCon = Ghc.isFamInstTyCon .||. Ghc.isVanillaAlgTyCon
liftableTyCons :: [Ghc.TyCon] -> [(Ghc.TyCon, DataName)]
liftableTyCons
= F.notracepp "LiftableTCs 3"
. zipMapMaybe (tyConDataName True)
. F.notracepp "LiftableTCs 2"
. filter (not . Ghc.isBoxedTupleTyCon)
. F.notracepp "LiftableTCs 1"
-- . (`sortDiff` wiredInTyCons)
-- . F.tracepp "LiftableTCs 0"
zipMap :: (a -> b) -> [a] -> [(a, b)]
zipMap f xs = zip xs (map f xs)
zipMapMaybe :: (a -> Maybe b) -> [a] -> [(a, b)]
zipMapMaybe f = Mb.mapMaybe (\x -> (x, ) <$> f x)
hasDataDecl :: ModName -> Ms.BareSpec -> Ghc.TyCon -> HasDataDecl
hasDataDecl mod spec
= \tc -> F.notracepp (msg tc) $ M.lookupDefault def (tcName tc) decls
where
msg tc = "hasDataDecl " ++ show (tcName tc)
def = NoDecl Nothing
tcName = fmap (qualifiedDataName mod) . tyConDataName True
dcName = qualifiedDataName mod . tycName
decls = M.fromList [ (Just dn, hasDecl d)
| d <- Ms.dataDecls spec
, let dn = dcName d]
qualifiedDataName :: ModName -> DataName -> DataName
qualifiedDataName mod (DnName lx) = DnName (qualifyModName mod <$> lx)
qualifiedDataName mod (DnCon lx) = DnCon (qualifyModName mod <$> lx)
{-tyConDataDecl :: {tc:TyCon | isAlgTyCon tc} -> Maybe DataDecl @-}
tyConDataDecl :: ((Ghc.TyCon, DataName), HasDataDecl) -> Maybe DataDecl
tyConDataDecl (_, HasDecl)
= Nothing
tyConDataDecl ((tc, dn), NoDecl szF)
= Just $ DataDecl
{ tycName = dn
, tycTyVars = F.symbol <$> GM.tyConTyVarsDef tc
, tycPVars = []
, tycDCons = decls tc
, tycSrcPos = GM.getSourcePos tc
, tycSFun = szF
, tycPropTy = Nothing
, tycKind = DataReflected
}
where decls = map dataConDecl . Ghc.tyConDataCons
tyConDataName :: Bool -> Ghc.TyCon -> Maybe DataName
tyConDataName full tc
| vanillaTc = Just (DnName ((post . F.symbol) <$> GM.locNamedThing tc))
| d:_ <- dcs = Just (DnCon ((post . F.symbol) <$> GM.locNamedThing d ))
| otherwise = Nothing
where
post = if full then id else GM.dropModuleNamesAndUnique
vanillaTc = Ghc.isVanillaAlgTyCon tc
dcs = Misc.sortOn F.symbol (Ghc.tyConDataCons tc)
dataConDecl :: Ghc.DataCon -> DataCtor
dataConDecl d = {- F.notracepp msg $ -} DataCtor dx (F.symbol <$> as) [] xts outT
where
isGadt = not (Ghc.isVanillaDataCon d)
-- msg = printf "dataConDecl (gadt = %s)" (show isGadt)
xts = [(Bare.makeDataConSelector Nothing d i, RT.bareOfType t) | (i, t) <- its ]
dx = F.symbol <$> GM.locNamedThing d
its = zip [1..] ts
(as,_ps,ts,t) = Ghc.dataConSig d
outT = Just (RT.bareOfType t :: BareType)
_outT :: Maybe BareType
_outT
| isGadt = Just (RT.bareOfType t)
| otherwise = Nothing
--------------------------------------------------------------------------------
-- | 'makeMeasureSelectors' converts the 'DataCon's and creates the measures for
-- the selectors and checkers that then enable reflection.
--------------------------------------------------------------------------------
makeMeasureSelectors :: Config -> Bare.DataConMap -> Located DataConP -> [Measure SpecType Ghc.DataCon]
makeMeasureSelectors cfg dm (Loc l l' c)
= (Misc.condNull (exactDCFlag cfg) $ checker : Mb.catMaybes (go' <$> fields)) -- internal measures, needed for reflection
++ (Misc.condNull (autofields) $ Mb.catMaybes (go <$> fields)) -- user-visible measures.
where
dc = dcpCon c
isGadt = dcpIsGadt c
xts = dcpTyArgs c
autofields = not (isGadt)
go ((x, t), i)
-- do not make selectors for functional fields
| isFunTy t && not (higherOrderFlag cfg)
= Nothing
| otherwise
= Just $ makeMeasureSelector (Loc l l' x) (projT i) dc n i
go' ((_,t), i)
-- do not make selectors for functional fields
| isFunTy t && not (higherOrderFlag cfg)
= Nothing
| otherwise
= Just $ makeMeasureSelector (Loc l l' (Bare.makeDataConSelector (Just dm) dc i)) (projT i) dc n i
fields = zip (reverse xts) [1..]
n = length xts
checker = makeMeasureChecker (Loc l l' (Bare.makeDataConChecker dc)) checkT dc n
projT i = dataConSel dc n (Proj i)
checkT = dataConSel dc n Check
dataConSel :: Ghc.DataCon -> Int -> DataConSel -> SpecType
dataConSel dc n Check = mkArrow (zip as (repeat mempty)) [] [] [xt] bareBool
where
(as, _, xt) = {- traceShow ("dataConSel: " ++ show dc) $ -} bkDataCon dc n
dataConSel dc n (Proj i) = mkArrow (zip as (repeat mempty)) [] [] [xt] (mempty <$> ti)
where
ti = Mb.fromMaybe err $ Misc.getNth (i-1) ts
(as, ts, xt) = {- F.tracepp ("bkDatacon dc = " ++ F.showpp (dc, n)) $ -} bkDataCon dc n
err = panic Nothing $ "DataCon " ++ show dc ++ "does not have " ++ show i ++ " fields"
-- bkDataCon :: DataCon -> Int -> ([RTVar RTyVar RSort], [SpecType], (Symbol, SpecType, RReft))
bkDataCon :: (F.Reftable (RTProp RTyCon RTyVar r), PPrint r, F.Reftable r) => Ghc.DataCon -> Int -> ([RTVar RTyVar RSort], [RRType r], (F.Symbol, RRType r, r))
bkDataCon dc nFlds = (as, ts, (F.dummySymbol, t, mempty))
where
ts = RT.ofType <$> Misc.takeLast nFlds _ts
t = -- Misc.traceShow ("bkDataConResult" ++ GM.showPpr (dc, _t, _t0)) $
RT.ofType $ Ghc.mkTyConApp tc tArgs'
as = makeRTVar . RT.rTyVar <$> (αs ++ αs')
((αs,αs',_,_,_ts,_t), _t0) = hammer dc
tArgs' = take (nArgs - nVars) tArgs ++ (Ghc.mkTyVarTy <$> αs)
nVars = length αs
nArgs = length tArgs
(tc, tArgs) = Mb.fromMaybe err (Ghc.splitTyConApp_maybe _t)
err = GM.namedPanic dc ("Cannot split result type of DataCon " ++ show dc)
hammer dc = (Ghc.dataConFullSig dc, Ghc.varType . Ghc.dataConWorkId $ dc)
data DataConSel = Check | Proj Int
bareBool :: SpecType
bareBool = RApp (RTyCon Ghc.boolTyCon [] def) [] [] mempty
{- | NOTE:Use DataconWorkId
dcWorkId :: forall a1 ... aN. (a1 ~ X1 ...) => T1 -> ... -> Tn -> T
checkT :: forall as. T -> Bool
projT t :: forall as. T -> t
-}
makeMeasureSelector :: (Show a1) => LocSymbol -> SpecType -> Ghc.DataCon -> Int -> a1 -> Measure SpecType Ghc.DataCon
makeMeasureSelector x s dc n i = M { msName = x, msSort = s, msEqns = [eqn], msKind = MsSelector, msUnSorted = mempty}
where
eqn = Def x dc Nothing args (E (F.EVar $ mkx i))
args = ((, Nothing) . mkx) <$> [1 .. n]
mkx j = F.symbol ("xx" ++ show j)
makeMeasureChecker :: LocSymbol -> SpecType -> Ghc.DataCon -> Int -> Measure SpecType Ghc.DataCon
makeMeasureChecker x s0 dc n = M { msName = x, msSort = s, msEqns = eqn : (eqns <$> filter (/= dc) dcs), msKind = MsChecker, msUnSorted = mempty }
where
s = F.notracepp ("makeMeasureChecker: " ++ show x) s0
eqn = Def x dc Nothing (((, Nothing) . mkx) <$> [1 .. n]) (P F.PTrue)
eqns d = Def x d Nothing (((, Nothing) . mkx) <$> [1 .. nArgs d]) (P F.PFalse)
nArgs d = length (Ghc.dataConOrigArgTys d)
mkx j = F.symbol ("xx" ++ show j)
dcs = Ghc.tyConDataCons (Ghc.dataConTyCon dc)
----------------------------------------------------------------------------------------------
makeMeasureSpec' :: MSpec SpecType Ghc.DataCon -> ([(Ghc.Var, SpecType)], [(LocSymbol, RRType F.Reft)])
----------------------------------------------------------------------------------------------
makeMeasureSpec' mspec0 = (ctorTys, measTys)
where
ctorTys = Misc.mapSnd RT.uRType <$> ctorTys0
(ctorTys0, measTys) = Ms.dataConTypes mspec
mspec = first (mapReft ur_reft) mspec0
----------------------------------------------------------------------------------------------
makeMeasureSpec :: Bare.Env -> Bare.SigEnv -> ModName -> (ModName, Ms.BareSpec) -> Ms.MSpec SpecType Ghc.DataCon
----------------------------------------------------------------------------------------------
makeMeasureSpec env sigEnv myName (name, spec)
= mkMeasureDCon env name
. mkMeasureSort env name
. first val
. bareMSpec env sigEnv myName name
$ spec
bareMSpec :: Bare.Env -> Bare.SigEnv -> ModName -> ModName -> Ms.BareSpec -> Ms.MSpec LocBareType LocSymbol
bareMSpec env sigEnv myName name spec = Ms.mkMSpec ms cms ims
where
cms = F.notracepp "CMS" $ filter inScope1 $ Ms.cmeasures spec
ms = F.notracepp "UMS" $ filter inScope2 $ expMeas <$> Ms.measures spec
ims = F.notracepp "IMS" $ filter inScope2 $ expMeas <$> Ms.imeasures spec
expMeas = expandMeasure env name rtEnv
rtEnv = Bare.sigRTEnv sigEnv
force = name == myName
inScope1 z = F.notracepp ("inScope1: " ++ F.showpp (msName z)) $ (force || okSort z)
inScope2 z = F.notracepp ("inScope2: " ++ F.showpp (msName z)) $ (force || (okSort z && okCtors z))
okSort = Bare.knownGhcType env name . msSort
okCtors = all (Bare.knownGhcDataCon env name . ctor) . msEqns
mkMeasureDCon :: Bare.Env -> ModName -> Ms.MSpec t LocSymbol -> Ms.MSpec t Ghc.DataCon
mkMeasureDCon env name m = mkMeasureDCon_ m [ (val n, symDC n) | n <- measureCtors m ]
where
symDC = Bare.lookupGhcDataCon env name "measure-datacon"
mkMeasureDCon_ :: Ms.MSpec t LocSymbol -> [(F.Symbol, Ghc.DataCon)] -> Ms.MSpec t Ghc.DataCon
mkMeasureDCon_ m ndcs = m' {Ms.ctorMap = cm'}
where
m' = fmap (tx.val) m
cm' = Misc.hashMapMapKeys (F.symbol . tx) $ Ms.ctorMap m'
tx = Misc.mlookup (M.fromList ndcs)
measureCtors :: Ms.MSpec t LocSymbol -> [LocSymbol]
measureCtors = Misc.sortNub . fmap ctor . concat . M.elems . Ms.ctorMap
mkMeasureSort :: Bare.Env -> ModName -> Ms.MSpec BareType LocSymbol
-> Ms.MSpec SpecType LocSymbol
mkMeasureSort env name (Ms.MSpec c mm cm im) =
Ms.MSpec (map txDef <$> c) (tx <$> mm) (tx <$> cm) (tx <$> im)
where
ofMeaSort :: F.SourcePos -> BareType -> SpecType
ofMeaSort l = Bare.ofBareType env name l Nothing
tx :: Measure BareType ctor -> (Measure SpecType ctor)
tx (M n s eqs k u) = M n (ofMeaSort l s) (txDef <$> eqs) k u where l = GM.fSourcePos n
txDef :: Def BareType ctor -> (Def SpecType ctor)
txDef d = first (ofMeaSort l) d where l = GM.fSourcePos (measure d)
--------------------------------------------------------------------------------
-- | Expand Measures -----------------------------------------------------------
--------------------------------------------------------------------------------
-- type BareMeasure = Measure LocBareType LocSymbol
expandMeasure :: Bare.Env -> ModName -> BareRTEnv -> BareMeasure -> BareMeasure
expandMeasure env name rtEnv m = m
{ msSort = RT.generalize <$> msSort m
, msEqns = expandMeasureDef env name rtEnv <$> msEqns m
}
expandMeasureDef :: Bare.Env -> ModName -> BareRTEnv -> Def t LocSymbol -> Def t LocSymbol
expandMeasureDef env name rtEnv d = d
{ body = F.notracepp msg $ Bare.qualifyExpand env name rtEnv l bs (body d) }
where
l = loc (measure d)
bs = fst <$> binds d
msg = "QUALIFY-EXPAND-BODY" ++ F.showpp (bs, body d)
------------------------------------------------------------------------------
varMeasures :: (Monoid r) => Bare.Env -> [(F.Symbol, Located (RRType r))]
------------------------------------------------------------------------------
varMeasures env =
[ (F.symbol v, varSpecType v)
| v <- knownVars env
, GM.isDataConId v
, isSimpleType (Ghc.varType v) ]
knownVars :: Bare.Env -> [Ghc.Var]
knownVars env = [ v | (_, xThings) <- M.toList (Bare._reTyThings env)
, (_,Ghc.AnId v) <- xThings
]
varSpecType :: (Monoid r) => Ghc.Var -> Located (RRType r)
varSpecType = fmap (RT.ofType . Ghc.varType) . GM.locNamedThing
isSimpleType :: Ghc.Type -> Bool
isSimpleType = isFirstOrder . RT.typeSort mempty
makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t
-> [(LocSymbol, CMeasure (RType c tv r2))]
makeClassMeasureSpec (Ms.MSpec {..}) = tx <$> M.elems cmeasMap
where
tx (M n s _ _ _) = (n, CM n (mapReft ur_reft s))
{-
expandMeasureBody :: Bare.Env -> ModName -> BareRTEnv -> SourcePos -> Body -> Body
expandMeasureBody env name rtEnv l (P p) = P (Bare.expandQualify env name rtEnv l p)
expandMeasureBody env name rtEnv l (R x p) = R x (Bare.expandQualify env name rtEnv l p)
expandMeasureBody env name rtEnv l (E e) = E (Bare.expandQualify env name rtEnv l e)
makeHaskellBounds :: F.TCEmb TyCon -> CoreProgram -> S.HashSet (Var, LocSymbol) -> BareM RBEnv -- TODO-REBARE
makeHaskellBounds embs cbs xs = do
lmap <- gets logicEnv
M.fromList <$> mapM (makeHaskellBound embs lmap cbs) (S.toList xs)
makeHaskellBound :: F.TCEmb TyCon
-> LogicMap
-> [Bind Var]
-> (Var, Located Symbol)
-> BareM (LocSymbol, RBound)
makeHaskellBound embs lmap cbs (v, x) =
case filter ((v `elem`) . GM.binders) cbs of
(NonRec v def:_) -> toBound v x <$> coreToFun' embs lmap x v def return
(Rec [(v, def)]:_) -> toBound v x <$> coreToFun' embs lmap x v def return
_ -> throwError $ errHMeas x "Cannot make bound of haskell function"
toBound :: Var -> LocSymbol -> ([Var], Either F.Expr F.Expr) -> (LocSymbol, RBound)
toBound v x (vs, Left p) = (x', Bound x' fvs ps xs p)
where
x' = capitalizeBound x
(ps', xs') = L.partition (hasBoolResult . varType) vs
(ps , xs) = (txp <$> ps', txx <$> xs')
txp v = (dummyLoc $ simpleSymbolVar v, RT.ofType $ varType v)
txx v = (dummyLoc $ symbol v, RT.ofType $ varType v)
fvs = (((`RVar` mempty) . RTV) <$> fst (splitForAllTys $ varType v)) :: [RSort]
toBound v x (vs, Right e) = toBound v x (vs, Left e)
capitalizeBound :: Located Symbol -> Located Symbol
capitalizeBound = fmap (symbol . toUpperHead . symbolString)
where
toUpperHead [] = []
toUpperHead (x:xs) = toUpper x:xs
-}