liquidhaskell-0.8.0.5: 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 Data.List (foldl', partition)
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 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 :: ![ty] -- ^ Data type invariants
, 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 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) = 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 wrt wrts
woRType = combineDCTypes 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 :: (Foldable t, PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r))
=> Type -> t (RType RTyCon RTyVar r) -> RType RTyCon RTyVar r
combineDCTypes t = foldl' strengthenRefTypeGen (ofType t)
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 constroctors 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)
= {- traceShow "defRefType: " $ -} generalize $ mkArrow [] [] [] xts t'
where
xts = stitchArgs (fSrcSpan f) dc ({- tracepp ("FIELDS-XS" ++ showpp f) -} xs) ({- tracepp ("FIELDS-TS" ++ showpp f) -} ts)
t = fromMaybe (ofType tr) mt
t' = mkForAlls args $ refineWithCtorBody dc f (fst <$> args) body t
mkForAlls xts t = foldl' (\t (x, tx) -> RAllE x tx t) t xts
(ts, tr) = splitFunTys $ snd $ splitForAllTys tdc
stitchArgs :: (Monoid t1, Monoid r, PPrint a)
=> SrcSpan
-> a
-> [(t, Maybe (RType RTyCon RTyVar r))]
-> [Type]
-> [(t, RType RTyCon RTyVar r, t1)]
stitchArgs sp dc xs ts
| nXs == nTs = zipWith g xs $ ofType `fmap` ts
| otherwise = panicFieldNumMismatch sp dc nXs nTs
where
nXs = length xs
nTs = length ts
g (x, Just t) _ = (x, t, mempty)
g (x, _) t = (x, t, mempty)
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)