liquidhaskell-0.8.2.2: src/Language/Haskell/Liquid/Measure.hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveGeneric #-}
module Language.Haskell.Liquid.Measure (
-- * Specifications
Spec (..)
, MSpec (..)
-- * Type Aliases
, BareSpec
, BareMeasure
, SpecMeasure
-- * Constructors
, mkM, mkMSpec, mkMSpec'
, qualifySpec
, dataConTypes
, defRefType
) where
import DataCon
import GHC hiding (Located)
import Outputable (Outputable)
import Prelude hiding (error)
import Text.PrettyPrint.HughesPJ hiding (first)
import Type
import Var
-- import Data.Serialize (Serialize)
import Data.Binary as B
import GHC.Generics
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import qualified Data.List as L
import Data.Maybe (fromMaybe, isNothing)
import Language.Fixpoint.Misc
import Language.Fixpoint.Types hiding (panic, R, DataDecl, SrcSpan)
import Language.Haskell.Liquid.GHC.Misc
-- import qualified Language.Haskell.Liquid.Misc as Misc
import Language.Haskell.Liquid.Types hiding (GhcInfo(..), GhcSpec (..))
import Language.Haskell.Liquid.Types.RefType
import Language.Haskell.Liquid.Types.Variance
import Language.Haskell.Liquid.Types.Bounds
import Language.Haskell.Liquid.UX.Tidy
-- MOVE TO TYPES
type BareSpec = Spec LocBareType LocSymbol
type BareMeasure = Measure LocBareType LocSymbol
type SpecMeasure = Measure LocSpecType DataCon
instance B.Binary BareSpec
data Spec ty bndr = Spec
{ measures :: ![Measure ty bndr] -- ^ User-defined properties for ADTs
, asmSigs :: ![(LocSymbol, ty)] -- ^ Assumed (unchecked) types; including reflected signatures
, sigs :: ![(LocSymbol, ty)] -- ^ Imported functions and types
, localSigs :: ![(LocSymbol, ty)] -- ^ Local type signatures
, reflSigs :: ![(LocSymbol, ty)] -- ^ Reflected type signatures
, invariants :: ![(Maybe LocSymbol, ty)] -- ^ Data type invariants; the Maybe is the generating measure
, ialiases :: ![(ty, ty)] -- ^ Data type invariants to be checked
, imports :: ![Symbol] -- ^ Loaded spec module names
, dataDecls :: ![DataDecl] -- ^ Predicated data definitions
, newtyDecls :: ![DataDecl] -- ^ Predicated new type definitions
, includes :: ![FilePath] -- ^ Included qualifier files
, aliases :: ![RTAlias Symbol BareType] -- ^ RefType aliases
, ealiases :: ![RTAlias Symbol Expr] -- ^ Expression aliases
, embeds :: !(TCEmb LocSymbol) -- ^ GHC-Tycon-to-fixpoint Tycon map
, qualifiers :: ![Qualifier] -- ^ Qualifiers in source/spec files
, decr :: ![(LocSymbol, [Int])] -- ^ Information on decreasing arguments
, lvars :: ![LocSymbol] -- ^ Variables that should be checked in the environment they are used
, lazy :: !(S.HashSet LocSymbol) -- ^ Ignore Termination Check in these Functions
, reflects :: !(S.HashSet LocSymbol) -- ^ Binders to reflect
, autois :: !(M.HashMap LocSymbol (Maybe Int)) -- ^ Automatically instantiate axioms in these Functions with maybe specified fuel
, hmeas :: !(S.HashSet LocSymbol) -- ^ Binders to turn into measures using haskell definitions
, hbounds :: !(S.HashSet LocSymbol) -- ^ Binders to turn into bounds using haskell definitions
, inlines :: !(S.HashSet LocSymbol) -- ^ Binders to turn into logic inline using haskell definitions
, autosize :: !(S.HashSet LocSymbol) -- ^ Type Constructors that get automatically sizing info
, pragmas :: ![Located String] -- ^ Command-line configurations passed in through source
, cmeasures :: ![Measure ty ()] -- ^ Measures attached to a type-class
, imeasures :: ![Measure ty bndr] -- ^ Mappings from (measure,type) -> measure
, classes :: ![RClass ty] -- ^ Refined Type-Classes
, termexprs :: ![(LocSymbol, [Located Expr])] -- ^ Terminating Conditions for functions
, rinstance :: ![RInstance ty]
, dvariance :: ![(LocSymbol, [Variance])] -- ^ ? Where do these come from ?!
, bounds :: !(RRBEnv ty)
, defs :: !(M.HashMap LocSymbol Symbol) -- ^ Temporary (?) hack to deal with dictionaries in specifications
-- see tests/pos/NatClass.hs
, axeqs :: ![AxiomEq] -- ^ AxiomEqualities used for Proof-By-Evaluation
} deriving (Generic)
qualifySpec :: Symbol -> Spec ty bndr -> Spec ty bndr
qualifySpec name sp = sp { sigs = [ (tx x, t) | (x, t) <- sigs sp]
, asmSigs = [ (tx x, t) | (x, t) <- asmSigs sp]
}
where
tx = fmap (qualifySymbol name)
mkM :: LocSymbol -> ty -> [Def ty bndr] -> Measure ty bndr
mkM name typ eqns
| all ((name ==) . measure) eqns
= M name typ eqns
| otherwise
= panic Nothing $ "invalid measure definition for " ++ show name
mkMSpec' :: Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor
mkMSpec' ms = MSpec cm mm M.empty []
where
cm = groupMap (symbol . ctor) $ concatMap eqns ms
mm = M.fromList [(name m, m) | m <- ms ]
mkMSpec :: [Measure t LocSymbol] -> [Measure t ()] -> [Measure t LocSymbol] -> MSpec t LocSymbol
mkMSpec ms cms ims = MSpec cm mm cmm ims
where
cm = groupMap (val . ctor) $ concatMap eqns (ms'++ims)
mm = M.fromList [(name m, m) | m <- ms' ]
cmm = M.fromList [(name m, m) | m <- cms ]
ms' = checkDuplicateMeasure ms
checkDuplicateMeasure :: [Measure ty ctor] -> [Measure ty ctor]
checkDuplicateMeasure ms
= case M.toList dups of
[] -> ms
(m,ms):_ -> uError $ err m (name <$> ms)
where
gms = group [(name m , m) | m <- ms]
dups = M.filter ((1 <) . length) gms
err m ms = ErrDupMeas (fSrcSpan m) (pprint (val m)) (fSrcSpan <$> ms)
-- printf "\nDuplicate Measure Definitions for %s\n%s" (showpp m) (showpp $ map (loc . name) ms)
-- err k1 k2 = ErrDupMeas (fSrcSpan k1) (pprint (val k1)) (fSrcSpan <$> [k1, k2])
-- MOVE TO TYPES
instance Monoid (Spec ty bndr) where
mappend s1 s2
= Spec { measures = measures s1 ++ measures s2
, asmSigs = asmSigs s1 ++ asmSigs s2
, sigs = sigs s1 ++ sigs s2
, localSigs = localSigs s1 ++ localSigs s2
, reflSigs = reflSigs s1 ++ reflSigs s2
, invariants = invariants s1 ++ invariants s2
, ialiases = ialiases s1 ++ ialiases s2
, imports = sortNub $ imports s1 ++ imports s2
, dataDecls = dataDecls s1 ++ dataDecls s2
, newtyDecls = newtyDecls s1 ++ newtyDecls s2
, includes = sortNub $ includes s1 ++ includes s2
, aliases = aliases s1 ++ aliases s2
, ealiases = ealiases s1 ++ ealiases s2
, qualifiers = qualifiers s1 ++ qualifiers s2
, decr = decr s1 ++ decr s2
, lvars = lvars s1 ++ lvars s2
, pragmas = pragmas s1 ++ pragmas s2
, cmeasures = cmeasures s1 ++ cmeasures s2
, imeasures = imeasures s1 ++ imeasures s2
, classes = classes s1 ++ classes s2
, termexprs = termexprs s1 ++ termexprs s2
, rinstance = rinstance s1 ++ rinstance s2
, dvariance = dvariance s1 ++ dvariance s2
, axeqs = axeqs s1 ++ axeqs s2
, embeds = M.union (embeds s1) (embeds s2)
, lazy = S.union (lazy s1) (lazy s2)
-- , axioms = S.union (axioms s1) (axioms s2)
, reflects = S.union (reflects s1) (reflects s2)
, hmeas = S.union (hmeas s1) (hmeas s2)
, hbounds = S.union (hbounds s1) (hbounds s2)
, inlines = S.union (inlines s1) (inlines s2)
, autosize = S.union (autosize s1) (autosize s2)
, bounds = M.union (bounds s1) (bounds s2)
, defs = M.union (defs s1) (defs s2)
, autois = M.union (autois s1) (autois s2)
}
mempty
= Spec { measures = []
, asmSigs = []
, sigs = []
, localSigs = []
, reflSigs = []
, invariants = []
, ialiases = []
, imports = []
, dataDecls = []
, newtyDecls = []
, includes = []
, aliases = []
, ealiases = []
, embeds = M.empty
, qualifiers = []
, decr = []
, lvars = []
, lazy = S.empty
, autois = M.empty
, hmeas = S.empty
-- , axioms = S.empty
, reflects = S.empty
, hbounds = S.empty
, inlines = S.empty
, autosize = S.empty
, pragmas = []
, cmeasures = []
, imeasures = []
, classes = []
, termexprs = []
, rinstance = []
, dvariance = []
, axeqs = []
, bounds = M.empty
, defs = M.empty
}
dataConTypes :: MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)])
dataConTypes s = (ctorTys, measTys)
where
measTys = [(name m, sort m) | m <- M.elems (measMap s) ++ imeas s]
ctorTys = concatMap makeDataConType (snd <$> M.toList (ctorMap s))
makeDataConType :: [Def (RRType Reft) DataCon] -> [(Var, RRType Reft)]
makeDataConType []
= []
makeDataConType ds | isNothing (dataConWrapId_maybe dc)
= [(woId, combineDCTypes "cdc0" t ts)]
where
dc = ctor (head ds)
woId = dataConWorkId dc
t = varType woId
ts = defRefType t <$> ds
makeDataConType ds
= [(woId, extend loci woRType wrRType), (wrId, extend loci wrRType woRType)]
where
(wo, wr) = L.partition isWorkerDef ds
dc = ctor $ head ds
loci = loc $ measure $ head ds
woId = dataConWorkId dc
wot = varType woId
wrId = dataConWrapId dc
wrt = varType wrId
wots = defRefType wot <$> wo
wrts = defRefType wrt <$> wr
wrRType = combineDCTypes "cdc1" wrt wrts
woRType = combineDCTypes "cdc2" wot wots
isWorkerDef def
-- types are missing for arguments, so definition came from a logical measure
-- and it is for the worker datacon
| any isNothing (snd <$> binds def)
= True
| otherwise
= length (binds def) == length (fst $ splitFunTys $ snd $ splitForAllTys wot)
extend :: SourcePos
-> RType RTyCon RTyVar Reft
-> RRType Reft
-> RType RTyCon RTyVar Reft
extend lc t1' t2
| Just su <- mapArgumens lc t1 t2
= t1 `strengthenResult` subst su (fromMaybe mempty (stripRTypeBase $ resultTy t2))
| otherwise
= t1
where
t1 = noDummySyms t1'
resultTy :: RType c tv r -> RType c tv r
resultTy = ty_res . toRTypeRep
strengthenResult :: Reftable r => RType c tv r -> r -> RType c tv r
strengthenResult t r = fromRTypeRep $ rep {ty_res = ty_res rep `strengthen` r}
where
rep = toRTypeRep t
noDummySyms :: (OkRT c tv r) => RType c tv r -> RType c tv r
noDummySyms t
| any isDummy (ty_binds rep)
= subst su $ fromRTypeRep $ rep{ty_binds = xs'}
| otherwise
= t
where
rep = toRTypeRep t
xs' = zipWith (\_ i -> symbol ("x" ++ show i)) (ty_binds rep) [1..]
su = mkSubst $ zip (ty_binds rep) (EVar <$> xs')
-- combineDCTypes :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r))
-- => Type -> [(RType RTyCon RTyVar r)] -> RType RTyCon RTyVar r
combineDCTypes :: String -> Type -> [RRType Reft] -> RRType Reft
combineDCTypes _msg t0 ts0 = L.foldl' strengthenRefTypeGen (ofType t) ts
where
(t, ts) = {- tracepp ("combineDCTypes " ++ msg) -} (t0, ts0)
mapArgumens :: SourcePos -> RRType Reft -> RRType Reft -> Maybe Subst
mapArgumens lc t1 t2 = go xts1' xts2'
where
xts1 = zip (ty_binds rep1) (ty_args rep1)
xts2 = zip (ty_binds rep2) (ty_args rep2)
rep1 = toRTypeRep t1
rep2 = toRTypeRep t2
xts1' = dropWhile canDrop xts1
xts2' = dropWhile canDrop xts2
canDrop (_, t) = isClassType t || isEqType t
go xs ys
| length xs == length ys && and (zipWith (==) (toRSort . snd <$> xts1') (toRSort . snd <$> xts2'))
= Just $ mkSubst $ zipWith (\y x -> (fst x, EVar $ fst y)) xts1' xts2'
| otherwise
= panic (Just $ sourcePosSrcSpan lc) ("The types for the wrapper and worker data constructors cannot be merged\n"
++ show t1 ++ "\n" ++ show t2 )
defRefType :: Type -> Def (RRType Reft) DataCon -> RRType Reft
defRefType tdc (Def f args dc mt xs body)
= notracepp ("defRefType: " ++ showpp f) $ generalize $ mkArrow as [] [] xts t'
where
xts = stitchArgs (fSrcSpan f) dc (notracepp ("FIELDS-XS: " ++ showpp f) xs) (notracepp ("FIELDS-TS: " ++ showpp f ++ " tdc = " ++ showpp tdc) ts)
t = fromMaybe (ofType tr) mt
t' = mkForAlls args $ refineWithCtorBody dc f (fst <$> args) body t
mkForAlls xts t = L.foldl' (\t (x, tx) -> RAllE x tx t) t xts
(αs, ts, tr) = splitType tdc
as = makeRTVar . rTyVar <$> αs
-- (αs,ps,dcTs,_) = dataConSig dc
-- (ts', tr) = splitFunTys $ snd $ splitForAllTys tdc
-- ts = Misc.takeLast (length dcTs) ts'
splitType :: Type -> ([TyVar],[Type], Type)
splitType t = (αs, ts, tr)
where
(αs, tb) = splitForAllTys t
(ts, tr) = splitFunTys tb
stitchArgs :: (Monoid t1, PPrint a)
=> SrcSpan
-> a
-> [(Symbol, Maybe (RRType Reft))]
-> [Type]
-> [(Symbol, RRType Reft, t1)]
stitchArgs sp dc allXs allTs
| nXs == nTs = (g (dummySymbol, Nothing) . ofType <$> pts)
++ zipWith g xs (ofType <$> ts)
| otherwise = panicFieldNumMismatch sp dc nXs nTs
where
(pts, ts) = L.partition (\t -> notracepp ("isPredTy: " ++ showpp t) $ isPredTy t) allTs
(_ , xs) = L.partition (coArg . snd) allXs
nXs = length xs
nTs = length ts
g (x, Just t) _ = (x, t, mempty)
g (x, _) t = (x, t, mempty)
coArg Nothing = False
coArg (Just t) = isPredTy . toType $ t
panicFieldNumMismatch :: (PPrint a, PPrint a1, PPrint a3)
=> SrcSpan -> a3 -> a1 -> a -> a2
panicFieldNumMismatch sp dc nXs nTs = panicDataCon sp dc msg
where
msg = "Requires" <+> pprint nTs <+> "fields but given" <+> pprint nXs
panicDataCon :: PPrint a1 => SrcSpan -> a1 -> Doc -> a
panicDataCon sp dc d
= panicError $ ErrDataCon sp (pprint dc) d
refineWithCtorBody :: Outputable a
=> a
-> LocSymbol
-> [Symbol]
-> Body
-> RType c tv Reft
-> RType c tv Reft
refineWithCtorBody dc f as body t =
case stripRTypeBase t of
Just (Reft (v, _)) ->
strengthen t $ Reft (v, bodyPred (mkEApp f (eVar <$> (as ++ [v]))) body)
Nothing ->
panic Nothing $ "measure mismatch " ++ showpp f ++ " on con " ++ showPpr dc
bodyPred :: Expr -> Body -> Expr
bodyPred fv (E e) = PAtom Eq fv e
bodyPred fv (P p) = PIff fv p
bodyPred fv (R v' p) = subst1 p (v', fv)