{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections #-}
module Language.Haskell.Liquid.Bare.Measure
( makeHaskellMeasures
, makeHaskellInlines
, makeHaskellDataDecls
, makeMeasureSelectors
, makeMeasureSpec
, makeMeasureSpec'
, varMeasures
, makeClassMeasureSpec
) 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 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 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 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
import Control.Monad (mapM)
makeHaskellMeasures :: Bool -> GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec
-> [Measure (Located BareType) LocSymbol]
makeHaskellMeasures :: Bool
-> GhcSrc
-> TycEnv
-> LogicMap
-> BareSpec
-> [Measure (Located BareType) LocSymbol]
makeHaskellMeasures Bool
allowTC GhcSrc
src TycEnv
tycEnv LogicMap
lmap BareSpec
spec
= SpecMeasure -> Measure (Located BareType) LocSymbol
Bare.measureToBare (SpecMeasure -> Measure (Located BareType) LocSymbol)
-> [SpecMeasure] -> [Measure (Located BareType) LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecMeasure]
ms
where
ms :: [SpecMeasure]
ms = Bool
-> TycEnv -> LogicMap -> [CoreBind] -> LocSymbol -> SpecMeasure
makeMeasureDefinition Bool
allowTC TycEnv
tycEnv LogicMap
lmap [CoreBind]
cbs (LocSymbol -> SpecMeasure) -> [LocSymbol] -> [SpecMeasure]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
mSyms
cbs :: [CoreBind]
cbs = [CoreBind] -> [CoreBind]
nonRecCoreBinds (GhcSrc -> [CoreBind]
_giCbs GhcSrc
src)
mSyms :: [LocSymbol]
mSyms = HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas BareSpec
spec)
makeMeasureDefinition :: Bool -> Bare.TycEnv -> LogicMap -> [Ghc.CoreBind] -> LocSymbol
-> Measure LocSpecType Ghc.DataCon
makeMeasureDefinition :: Bool
-> TycEnv -> LogicMap -> [CoreBind] -> LocSymbol -> SpecMeasure
makeMeasureDefinition Bool
allowTC TycEnv
tycEnv LogicMap
lmap [CoreBind]
cbs LocSymbol
x =
case Symbol -> [CoreBind] -> Maybe (TyCoVar, CoreExpr)
GM.findVarDef (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) [CoreBind]
cbs of
Maybe (TyCoVar, CoreExpr)
Nothing -> Error -> SpecMeasure
forall a e. Exception e => e -> a
Ex.throw (Error -> SpecMeasure) -> Error -> SpecMeasure
forall a b. (a -> b) -> a -> b
$ LocSymbol -> String -> Error
errHMeas LocSymbol
x String
"Cannot extract measure from haskell function"
Just (TyCoVar
v, CoreExpr
cexp) -> LocSymbol
-> LocSpecType
-> [Def LocSpecType DataCon]
-> MeasureKind
-> UnSortedExprs
-> SpecMeasure
forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
Ms.mkM LocSymbol
vx LocSpecType
vinfo [Def LocSpecType DataCon]
mdef MeasureKind
MsLifted (Bool -> Type -> [Def LocSpecType DataCon] -> UnSortedExprs
makeUnSorted Bool
allowTC (TyCoVar -> Type
Ghc.varType TyCoVar
v) [Def LocSpecType DataCon]
mdef)
where
vx :: LocSymbol
vx = LocSymbol -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
x (TyCoVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCoVar
v)
mdef :: [Def LocSpecType DataCon]
mdef = Bool
-> TycEnv
-> LogicMap
-> LocSymbol
-> TyCoVar
-> CoreExpr
-> [Def LocSpecType DataCon]
coreToDef' Bool
allowTC TycEnv
tycEnv LogicMap
lmap LocSymbol
vx TyCoVar
v CoreExpr
cexp
vinfo :: LocSpecType
vinfo = (Type -> SpecType) -> TyCoVar -> LocSpecType
forall a. (Type -> a) -> TyCoVar -> Located a
GM.varLocInfo (Bool -> Type -> SpecType
forall r. Reftable r => Bool -> Type -> RRType r
logicType Bool
allowTC) TyCoVar
v
makeUnSorted :: Bool -> Ghc.Type -> [Def LocSpecType Ghc.DataCon] -> UnSortedExprs
makeUnSorted :: Bool -> Type -> [Def LocSpecType DataCon] -> UnSortedExprs
makeUnSorted Bool
allowTC Type
ty [Def LocSpecType DataCon]
defs
| Type -> Bool
isMeasureType Type
ta
= UnSortedExprs
forall a. Monoid a => a
mempty
| Bool
otherwise
= (Def LocSpecType DataCon -> UnSortedExpr)
-> [Def LocSpecType DataCon] -> UnSortedExprs
forall a b. (a -> b) -> [a] -> [b]
map Def LocSpecType DataCon -> UnSortedExpr
forall {ty} {ctor}. Def ty ctor -> UnSortedExpr
defToUnSortedExpr [Def LocSpecType DataCon]
defs
where
ta :: Type
ta = Type -> Type
go (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms Type
ty
go :: Type -> Type
go (Ghc.ForAllTy ForAllTyBinder
_ Type
t) = Type -> Type
go Type
t
go Ghc.FunTy{ ft_arg :: Type -> Type
Ghc.ft_arg = Type
p, ft_res :: Type -> Type
Ghc.ft_res = Type
t} | Type -> Bool
isErasable Type
p = Type -> Type
go Type
t
go Ghc.FunTy{ ft_arg :: Type -> Type
Ghc.ft_arg = Type
t } = Type
t
go Type
t = Type
t
isMeasureType :: Type -> Bool
isMeasureType (Ghc.TyConApp TyCon
_ [Type]
ts) = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
Ghc.isTyVarTy [Type]
ts
isMeasureType Type
_ = Bool
False
defToUnSortedExpr :: Def ty ctor -> UnSortedExpr
defToUnSortedExpr Def ty ctor
defn = (Symbol
xxSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:((Symbol, Maybe ty) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Maybe ty) -> Symbol) -> [(Symbol, Maybe ty)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Def ty ctor -> [(Symbol, Maybe ty)]
forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def ty ctor
defn),
Expr -> Body -> Expr
Ms.bodyPred (LocSymbol -> [Expr] -> Expr
F.mkEApp (Def ty ctor -> LocSymbol
forall ty ctor. Def ty ctor -> LocSymbol
measure Def ty ctor
defn) [Symbol -> Expr
forall a. Expression a => a -> Expr
F.expr Symbol
xx]) (Def ty ctor -> Body
forall ty ctor. Def ty ctor -> Body
body Def ty ctor
defn))
xx :: Symbol
xx = Maybe Integer -> Symbol
F.vv (Maybe Integer -> Symbol) -> Maybe Integer -> Symbol
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
10000
isErasable :: Type -> Bool
isErasable = if Bool
allowTC then Type -> Bool
GM.isEmbeddedDictType else Type -> Bool
Ghc.isClassPred
coreToDef' :: Bool -> Bare.TycEnv -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
-> [Def LocSpecType Ghc.DataCon]
coreToDef' :: Bool
-> TycEnv
-> LogicMap
-> LocSymbol
-> TyCoVar
-> CoreExpr
-> [Def LocSpecType DataCon]
coreToDef' Bool
allowTC TycEnv
tycEnv LogicMap
lmap LocSymbol
vx TyCoVar
v CoreExpr
defn =
case TCEmb TyCon
-> LogicMap
-> DataConMap
-> (String -> Error)
-> LogicM [Def LocSpecType DataCon]
-> Either Error [Def LocSpecType DataCon]
forall t.
TCEmb TyCon
-> LogicMap
-> DataConMap
-> (String -> Error)
-> LogicM t
-> Either Error t
runToLogic TCEmb TyCon
embs LogicMap
lmap DataConMap
dm (LocSymbol -> String -> Error
errHMeas LocSymbol
vx) (Bool
-> LocSymbol
-> TyCoVar
-> CoreExpr
-> LogicM [Def LocSpecType DataCon]
forall r.
Reftable r =>
Bool
-> LocSymbol
-> TyCoVar
-> CoreExpr
-> LogicM [Def (Located (RRType r)) DataCon]
coreToDef Bool
allowTC LocSymbol
vx TyCoVar
v CoreExpr
defn) of
Right [Def LocSpecType DataCon]
l -> [Def LocSpecType DataCon]
l
Left Error
e -> Error -> [Def LocSpecType DataCon]
forall a e. Exception e => e -> a
Ex.throw Error
e
where
embs :: TCEmb TyCon
embs = TycEnv -> TCEmb TyCon
Bare.tcEmbs TycEnv
tycEnv
dm :: DataConMap
dm = TycEnv -> DataConMap
Bare.tcDataConMap TycEnv
tycEnv
errHMeas :: LocSymbol -> String -> Error
errHMeas :: LocSymbol -> String -> Error
errHMeas LocSymbol
x String
str = SrcSpan -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ LocSymbol -> SourcePos
forall a. Located a -> SourcePos
loc LocSymbol
x) (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) (String -> Doc
text String
str)
makeHaskellInlines :: Bool -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec
-> [(LocSymbol, LMap)]
makeHaskellInlines :: Bool
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> BareSpec
-> [(LocSymbol, LMap)]
makeHaskellInlines Bool
allowTC GhcSrc
src TCEmb TyCon
embs LogicMap
lmap BareSpec
spec
= Bool
-> TCEmb TyCon
-> LogicMap
-> [CoreBind]
-> LocSymbol
-> (LocSymbol, LMap)
makeMeasureInline Bool
allowTC TCEmb TyCon
embs LogicMap
lmap [CoreBind]
cbs (LocSymbol -> (LocSymbol, LMap))
-> [LocSymbol] -> [(LocSymbol, LMap)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
inls
where
cbs :: [CoreBind]
cbs = [CoreBind] -> [CoreBind]
nonRecCoreBinds (GhcSrc -> [CoreBind]
_giCbs GhcSrc
src)
inls :: [LocSymbol]
inls = HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.inlines BareSpec
spec)
makeMeasureInline :: Bool -> F.TCEmb Ghc.TyCon -> LogicMap -> [Ghc.CoreBind] -> LocSymbol
-> (LocSymbol, LMap)
makeMeasureInline :: Bool
-> TCEmb TyCon
-> LogicMap
-> [CoreBind]
-> LocSymbol
-> (LocSymbol, LMap)
makeMeasureInline Bool
allowTC TCEmb TyCon
embs LogicMap
lmap [CoreBind]
cbs LocSymbol
x =
case Symbol -> [CoreBind] -> Maybe (TyCoVar, CoreExpr)
GM.findVarDef (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) [CoreBind]
cbs of
Maybe (TyCoVar, CoreExpr)
Nothing -> Error -> (LocSymbol, LMap)
forall a e. Exception e => e -> a
Ex.throw (Error -> (LocSymbol, LMap)) -> Error -> (LocSymbol, LMap)
forall a b. (a -> b) -> a -> b
$ LocSymbol -> String -> Error
errHMeas LocSymbol
x String
"Cannot inline haskell function"
Just (TyCoVar
v, CoreExpr
defn) -> (LocSymbol
vx, Bool
-> TCEmb TyCon
-> Maybe DataConMap
-> LogicMap
-> LocSymbol
-> TyCoVar
-> CoreExpr
-> (([TyCoVar], Either Expr Expr) -> LMap)
-> LMap
forall a.
Bool
-> TCEmb TyCon
-> Maybe DataConMap
-> LogicMap
-> LocSymbol
-> TyCoVar
-> CoreExpr
-> (([TyCoVar], Either Expr Expr) -> a)
-> a
coreToFun' Bool
allowTC TCEmb TyCon
embs Maybe DataConMap
forall a. Maybe a
Nothing LogicMap
lmap LocSymbol
vx TyCoVar
v CoreExpr
defn ([TyCoVar], Either Expr Expr) -> LMap
forall {a}. Symbolic a => ([a], Either Expr Expr) -> LMap
ok)
where
vx :: LocSymbol
vx = LocSymbol -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
x (TyCoVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCoVar
v)
ok :: ([a], Either Expr Expr) -> LMap
ok ([a]
xs, Either Expr Expr
e) = LocSymbol -> [Symbol] -> Expr -> LMap
LMap LocSymbol
vx (a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (a -> Symbol) -> [a] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs) ((Expr -> Expr) -> (Expr -> Expr) -> Either Expr Expr -> Expr
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Expr -> Expr
forall a. a -> a
id Expr -> Expr
forall a. a -> a
id Either Expr Expr
e)
coreToFun' :: Bool -> F.TCEmb Ghc.TyCon -> Maybe Bare.DataConMap -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
-> (([Ghc.Var], Either F.Expr F.Expr) -> a) -> a
coreToFun' :: forall a.
Bool
-> TCEmb TyCon
-> Maybe DataConMap
-> LogicMap
-> LocSymbol
-> TyCoVar
-> CoreExpr
-> (([TyCoVar], Either Expr Expr) -> a)
-> a
coreToFun' Bool
allowTC TCEmb TyCon
embs Maybe DataConMap
dmMb LogicMap
lmap LocSymbol
x TyCoVar
v CoreExpr
defn ([TyCoVar], Either Expr Expr) -> a
ok = (Error -> a)
-> (([TyCoVar], Either Expr Expr) -> a)
-> Either Error ([TyCoVar], Either Expr Expr)
-> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Error -> a
forall a e. Exception e => e -> a
Ex.throw ([TyCoVar], Either Expr Expr) -> a
ok Either Error ([TyCoVar], Either Expr Expr)
act
where
act :: Either Error ([TyCoVar], Either Expr Expr)
act = TCEmb TyCon
-> LogicMap
-> DataConMap
-> (String -> Error)
-> LogicM ([TyCoVar], Either Expr Expr)
-> Either Error ([TyCoVar], Either Expr Expr)
forall t.
TCEmb TyCon
-> LogicMap
-> DataConMap
-> (String -> Error)
-> LogicM t
-> Either Error t
runToLogic TCEmb TyCon
embs LogicMap
lmap DataConMap
dm String -> Error
err LogicM ([TyCoVar], Either Expr Expr)
xFun
xFun :: LogicM ([TyCoVar], Either Expr Expr)
xFun = Bool
-> LocSymbol
-> TyCoVar
-> CoreExpr
-> LogicM ([TyCoVar], Either Expr Expr)
coreToFun Bool
allowTC LocSymbol
x TyCoVar
v CoreExpr
defn
err :: String -> Error
err = LocSymbol -> String -> Error
errHMeas LocSymbol
x
dm :: DataConMap
dm = DataConMap -> Maybe DataConMap -> DataConMap
forall a. a -> Maybe a -> a
Mb.fromMaybe DataConMap
forall a. Monoid a => a
mempty Maybe DataConMap
dmMb
nonRecCoreBinds :: [Ghc.CoreBind] -> [Ghc.CoreBind]
nonRecCoreBinds :: [CoreBind] -> [CoreBind]
nonRecCoreBinds = (CoreBind -> [CoreBind]) -> [CoreBind] -> [CoreBind]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CoreBind -> [CoreBind]
forall {b}. Bind b -> [Bind b]
go
where
go :: Bind b -> [Bind b]
go cb :: Bind b
cb@(Ghc.NonRec b
_ Expr b
_) = [Bind b
cb]
go (Ghc.Rec [(b, Expr b)]
xes) = [b -> Expr b -> Bind b
forall b. b -> Expr b -> Bind b
Ghc.NonRec b
x Expr b
e | (b
x, Expr b
e) <- [(b, Expr b)]
xes]
makeHaskellDataDecls :: Config -> ModName -> Ms.BareSpec -> [Ghc.TyCon]
-> [DataDecl]
makeHaskellDataDecls :: Config -> ModName -> BareSpec -> [TyCon] -> [DataDecl]
makeHaskellDataDecls Config
cfg ModName
name BareSpec
spec [TyCon]
tcs
| Config -> Bool
forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg = BareSpec -> [DataDecl] -> [DataDecl]
Bare.dataDeclSize BareSpec
spec
([DataDecl] -> [DataDecl])
-> ([TyCon] -> [DataDecl]) -> [TyCon] -> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((TyCon, DataName), HasDataDecl) -> Maybe DataDecl)
-> [((TyCon, DataName), HasDataDecl)] -> [DataDecl]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe ((TyCon, DataName), HasDataDecl) -> Maybe DataDecl
tyConDataDecl
([((TyCon, DataName), HasDataDecl)] -> [DataDecl])
-> ([TyCon] -> [((TyCon, DataName), HasDataDecl)])
-> [TyCon]
-> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TyCon, DataName) -> HasDataDecl)
-> [(TyCon, DataName)] -> [((TyCon, DataName), HasDataDecl)]
forall a b. (a -> b) -> [a] -> [(a, b)]
zipMap (ModName -> BareSpec -> TyCon -> HasDataDecl
hasDataDecl ModName
name BareSpec
spec (TyCon -> HasDataDecl)
-> ((TyCon, DataName) -> TyCon) -> (TyCon, DataName) -> HasDataDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon, DataName) -> TyCon
forall a b. (a, b) -> a
fst)
([(TyCon, DataName)] -> [((TyCon, DataName), HasDataDecl)])
-> ([TyCon] -> [(TyCon, DataName)])
-> [TyCon]
-> [((TyCon, DataName), HasDataDecl)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TyCon] -> [(TyCon, DataName)]
liftableTyCons
([TyCon] -> [(TyCon, DataName)])
-> ([TyCon] -> [TyCon]) -> [TyCon] -> [(TyCon, DataName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon -> Bool) -> [TyCon] -> [TyCon]
forall a. (a -> Bool) -> [a] -> [a]
filter TyCon -> Bool
isReflectableTyCon
([TyCon] -> [DataDecl]) -> [TyCon] -> [DataDecl]
forall a b. (a -> b) -> a -> b
$ [TyCon]
tcs
| Bool
otherwise = []
isReflectableTyCon :: Ghc.TyCon -> Bool
isReflectableTyCon :: TyCon -> Bool
isReflectableTyCon = TyCon -> Bool
Ghc.isFamInstTyCon (TyCon -> Bool) -> (TyCon -> Bool) -> TyCon -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
.||. TyCon -> Bool
Ghc.isVanillaAlgTyCon
liftableTyCons :: [Ghc.TyCon] -> [(Ghc.TyCon, DataName)]
liftableTyCons :: [TyCon] -> [(TyCon, DataName)]
liftableTyCons
= String -> [(TyCon, DataName)] -> [(TyCon, DataName)]
forall a. PPrint a => String -> a -> a
F.notracepp String
"LiftableTCs 3"
([(TyCon, DataName)] -> [(TyCon, DataName)])
-> ([TyCon] -> [(TyCon, DataName)])
-> [TyCon]
-> [(TyCon, DataName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon -> Maybe DataName) -> [TyCon] -> [(TyCon, DataName)]
forall a b. (a -> Maybe b) -> [a] -> [(a, b)]
zipMapMaybe (Bool -> TyCon -> Maybe DataName
tyConDataName Bool
True)
([TyCon] -> [(TyCon, DataName)])
-> ([TyCon] -> [TyCon]) -> [TyCon] -> [(TyCon, DataName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [TyCon] -> [TyCon]
forall a. PPrint a => String -> a -> a
F.notracepp String
"LiftableTCs 2"
([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon -> Bool) -> [TyCon] -> [TyCon]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TyCon -> Bool) -> TyCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Bool
Ghc.isBoxedTupleTyCon)
([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [TyCon] -> [TyCon]
forall a. PPrint a => String -> a -> a
F.notracepp String
"LiftableTCs 1"
zipMap :: (a -> b) -> [a] -> [(a, b)]
zipMap :: forall a b. (a -> b) -> [a] -> [(a, b)]
zipMap a -> b
f [a]
xs = [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
xs ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f [a]
xs)
zipMapMaybe :: (a -> Maybe b) -> [a] -> [(a, b)]
zipMapMaybe :: forall a b. (a -> Maybe b) -> [a] -> [(a, b)]
zipMapMaybe a -> Maybe b
f = (a -> Maybe (a, b)) -> [a] -> [(a, b)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (\a
x -> (a
x, ) (b -> (a, b)) -> Maybe b -> Maybe (a, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
x)
hasDataDecl :: ModName -> Ms.BareSpec -> Ghc.TyCon -> HasDataDecl
hasDataDecl :: ModName -> BareSpec -> TyCon -> HasDataDecl
hasDataDecl ModName
modName BareSpec
spec
= \TyCon
tc -> String -> HasDataDecl -> HasDataDecl
forall a. PPrint a => String -> a -> a
F.notracepp (TyCon -> String
msg TyCon
tc) (HasDataDecl -> HasDataDecl) -> HasDataDecl -> HasDataDecl
forall a b. (a -> b) -> a -> b
$ HasDataDecl
-> Maybe DataName
-> HashMap (Maybe DataName) HasDataDecl
-> HasDataDecl
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault HasDataDecl
defn (TyCon -> Maybe DataName
tcName TyCon
tc) HashMap (Maybe DataName) HasDataDecl
decls
where
msg :: TyCon -> String
msg TyCon
tc = String
"hasDataDecl " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe DataName -> String
forall a. Show a => a -> String
show (TyCon -> Maybe DataName
tcName TyCon
tc)
defn :: HasDataDecl
defn = Maybe SizeFun -> HasDataDecl
NoDecl Maybe SizeFun
forall a. Maybe a
Nothing
tcName :: TyCon -> Maybe DataName
tcName = (DataName -> DataName) -> Maybe DataName -> Maybe DataName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ModName -> DataName -> DataName
qualifiedDataName ModName
modName) (Maybe DataName -> Maybe DataName)
-> (TyCon -> Maybe DataName) -> TyCon -> Maybe DataName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> TyCon -> Maybe DataName
tyConDataName Bool
True
dcName :: DataDecl -> DataName
dcName = ModName -> DataName -> DataName
qualifiedDataName ModName
modName (DataName -> DataName)
-> (DataDecl -> DataName) -> DataDecl -> DataName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> DataName
tycName
decls :: HashMap (Maybe DataName) HasDataDecl
decls = [(Maybe DataName, HasDataDecl)]
-> HashMap (Maybe DataName) HasDataDecl
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (DataName -> Maybe DataName
forall a. a -> Maybe a
Just DataName
dn, DataDecl -> HasDataDecl
hasDecl DataDecl
d)
| DataDecl
d <- BareSpec -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.dataDecls BareSpec
spec
, let dn :: DataName
dn = DataDecl -> DataName
dcName DataDecl
d]
qualifiedDataName :: ModName -> DataName -> DataName
qualifiedDataName :: ModName -> DataName -> DataName
qualifiedDataName ModName
modName (DnName LocSymbol
lx) = LocSymbol -> DataName
DnName (ModName -> Symbol -> Symbol
qualifyModName ModName
modName (Symbol -> Symbol) -> LocSymbol -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSymbol
lx)
qualifiedDataName ModName
modName (DnCon LocSymbol
lx) = LocSymbol -> DataName
DnCon (ModName -> Symbol -> Symbol
qualifyModName ModName
modName (Symbol -> Symbol) -> LocSymbol -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSymbol
lx)
tyConDataDecl :: ((Ghc.TyCon, DataName), HasDataDecl) -> Maybe DataDecl
tyConDataDecl :: ((TyCon, DataName), HasDataDecl) -> Maybe DataDecl
tyConDataDecl ((TyCon, DataName)
_, HasDataDecl
HasDecl)
= Maybe DataDecl
forall a. Maybe a
Nothing
tyConDataDecl ((TyCon
tc, DataName
dn), NoDecl Maybe SizeFun
szF)
= DataDecl -> Maybe DataDecl
forall a. a -> Maybe a
Just (DataDecl -> Maybe DataDecl) -> DataDecl -> Maybe DataDecl
forall a b. (a -> b) -> a -> b
$ DataDecl
{ tycName :: DataName
tycName = DataName
dn
, tycTyVars :: [Symbol]
tycTyVars = TyCoVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (TyCoVar -> Symbol) -> [TyCoVar] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [TyCoVar]
GM.tyConTyVarsDef TyCon
tc
, tycPVars :: [PVar BSort]
tycPVars = []
, tycDCons :: Maybe [DataCtor]
tycDCons = [DataCtor] -> Maybe [DataCtor]
forall a. a -> Maybe a
Just (TyCon -> [DataCtor]
decls TyCon
tc)
, tycSrcPos :: SourcePos
tycSrcPos = TyCon -> SourcePos
forall a. NamedThing a => a -> SourcePos
GM.getSourcePos TyCon
tc
, tycSFun :: Maybe SizeFun
tycSFun = Maybe SizeFun
szF
, tycPropTy :: Maybe BareType
tycPropTy = Maybe BareType
forall a. Maybe a
Nothing
, tycKind :: DataDeclKind
tycKind = DataDeclKind
DataReflected
}
where decls :: TyCon -> [DataCtor]
decls = (DataCon -> DataCtor) -> [DataCon] -> [DataCtor]
forall a b. (a -> b) -> [a] -> [b]
map DataCon -> DataCtor
dataConDecl ([DataCon] -> [DataCtor])
-> (TyCon -> [DataCon]) -> TyCon -> [DataCtor]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> [DataCon]
Ghc.tyConDataCons
tyConDataName :: Bool -> Ghc.TyCon -> Maybe DataName
tyConDataName :: Bool -> TyCon -> Maybe DataName
tyConDataName Bool
full TyCon
tc
| Bool
vanillaTc = DataName -> Maybe DataName
forall a. a -> Maybe a
Just (LocSymbol -> DataName
DnName (Symbol -> Symbol
post (Symbol -> Symbol) -> (TyCon -> Symbol) -> TyCon -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (TyCon -> Symbol) -> Located TyCon -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> Located TyCon
forall a. NamedThing a => a -> Located a
GM.locNamedThing TyCon
tc))
| DataCon
d:[DataCon]
_ <- [DataCon]
dcs = DataName -> Maybe DataName
forall a. a -> Maybe a
Just (LocSymbol -> DataName
DnCon (Symbol -> Symbol
post (Symbol -> Symbol) -> (DataCon -> Symbol) -> DataCon -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DataCon -> Symbol) -> Located DataCon -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCon -> Located DataCon
forall a. NamedThing a => a -> Located a
GM.locNamedThing DataCon
d ))
| Bool
otherwise = Maybe DataName
forall a. Maybe a
Nothing
where
post :: Symbol -> Symbol
post = if Bool
full then Symbol -> Symbol
forall a. a -> a
id else Symbol -> Symbol
GM.dropModuleNamesAndUnique
vanillaTc :: Bool
vanillaTc = TyCon -> Bool
Ghc.isVanillaAlgTyCon TyCon
tc
dcs :: [DataCon]
dcs = (DataCon -> Symbol) -> [DataCon] -> [DataCon]
forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (TyCon -> [DataCon]
Ghc.tyConDataCons TyCon
tc)
dataConDecl :: Ghc.DataCon -> DataCtor
dataConDecl :: DataCon -> DataCtor
dataConDecl DataCon
d = LocSymbol
-> [Symbol]
-> [BareType]
-> [(Symbol, BareType)]
-> Maybe BareType
-> DataCtor
DataCtor LocSymbol
dx (TyCoVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (TyCoVar -> Symbol) -> [TyCoVar] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyCoVar]
as) [] [(Symbol, BareType)]
xts Maybe BareType
outT
where
isGadt :: Bool
isGadt = Bool -> Bool
not (DataCon -> Bool
Ghc.isVanillaDataCon DataCon
d)
xts :: [(Symbol, BareType)]
xts = [(Maybe DataConMap -> DataCon -> Int -> Symbol
Bare.makeDataConSelector Maybe DataConMap
forall a. Maybe a
Nothing DataCon
d Int
i, Type -> BareType
forall r. Monoid r => Type -> BRType r
RT.bareOfType Type
t) | (Int
i, Type
t) <- [(Int, Type)]
its ]
dx :: LocSymbol
dx = DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DataCon -> Symbol) -> Located DataCon -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCon -> Located DataCon
forall a. NamedThing a => a -> Located a
GM.locNamedThing DataCon
d
its :: [(Int, Type)]
its = [Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [Type]
ts
([TyCoVar]
as,[Type]
_ps,[Type]
ts,Type
ty) = DataCon -> ([TyCoVar], [Type], [Type], Type)
Ghc.dataConSig DataCon
d
outT :: Maybe BareType
outT = BareType -> Maybe BareType
forall a. a -> Maybe a
Just (Type -> BareType
forall r. Monoid r => Type -> BRType r
RT.bareOfType Type
ty :: BareType)
_outT :: Maybe BareType
_outT :: Maybe BareType
_outT
| Bool
isGadt = BareType -> Maybe BareType
forall a. a -> Maybe a
Just (Type -> BareType
forall r. Monoid r => Type -> BRType r
RT.bareOfType Type
ty)
| Bool
otherwise = Maybe BareType
forall a. Maybe a
Nothing
makeMeasureSelectors :: Config -> Bare.DataConMap -> Located DataConP -> [Measure SpecType Ghc.DataCon]
makeMeasureSelectors :: Config
-> DataConMap -> Located DataConP -> [Measure SpecType DataCon]
makeMeasureSelectors Config
cfg DataConMap
dm (Loc SourcePos
l SourcePos
l' DataConP
c)
= Bool -> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall m. Monoid m => Bool -> m -> m
Misc.condNull (Config -> Bool
forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg) (Measure SpecType DataCon
checker Measure SpecType DataCon
-> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall a. a -> [a] -> [a]
: (((Symbol, SpecType), Int) -> Maybe (Measure SpecType DataCon))
-> [((Symbol, SpecType), Int)] -> [Measure SpecType DataCon]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe ((Symbol, SpecType), Int) -> Maybe (Measure SpecType DataCon)
forall {a} {t} {t1} {t2}.
((a, RType t t1 t2), Int) -> Maybe (Measure SpecType DataCon)
go' [((Symbol, SpecType), Int)]
fields)
[Measure SpecType DataCon]
-> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall a. [a] -> [a] -> [a]
++ Bool -> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall m. Monoid m => Bool -> m -> m
Misc.condNull Bool
autofields ((((Symbol, SpecType), Int) -> Maybe (Measure SpecType DataCon))
-> [((Symbol, SpecType), Int)] -> [Measure SpecType DataCon]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe ((Symbol, SpecType), Int) -> Maybe (Measure SpecType DataCon)
forall {t} {t1} {t2}.
((Symbol, RType t t1 t2), Int) -> Maybe (Measure SpecType DataCon)
go [((Symbol, SpecType), Int)]
fields)
where
dc :: DataCon
dc = DataConP -> DataCon
dcpCon DataConP
c
isGadt :: Bool
isGadt = DataConP -> Bool
dcpIsGadt DataConP
c
xts :: [(Symbol, SpecType)]
xts = DataConP -> [(Symbol, SpecType)]
dcpTyArgs DataConP
c
autofields :: Bool
autofields = Bool -> Bool
not Bool
isGadt
go :: ((Symbol, RType t t1 t2), Int) -> Maybe (Measure SpecType DataCon)
go ((Symbol
x, RType t t1 t2
t), Int
i)
| RType t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RType t t1 t2
t Bool -> Bool -> Bool
&& Bool -> Bool
not (Config -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag Config
cfg)
= Maybe (Measure SpecType DataCon)
forall a. Maybe a
Nothing
| Bool
otherwise
= Measure SpecType DataCon -> Maybe (Measure SpecType DataCon)
forall a. a -> Maybe a
Just (Measure SpecType DataCon -> Maybe (Measure SpecType DataCon))
-> Measure SpecType DataCon -> Maybe (Measure SpecType DataCon)
forall a b. (a -> b) -> a -> b
$ LocSymbol
-> SpecType -> DataCon -> Int -> Int -> Measure SpecType DataCon
forall a1.
Show a1 =>
LocSymbol
-> SpecType -> DataCon -> Int -> a1 -> Measure SpecType DataCon
makeMeasureSelector (SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' Symbol
x) (Int -> SpecType
projT Int
i) DataCon
dc Int
n Int
i
go' :: ((a, RType t t1 t2), Int) -> Maybe (Measure SpecType DataCon)
go' ((a
_,RType t t1 t2
t), Int
i)
| RType t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RType t t1 t2
t Bool -> Bool -> Bool
&& Bool -> Bool
not (Config -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag Config
cfg)
= Maybe (Measure SpecType DataCon)
forall a. Maybe a
Nothing
| Bool
otherwise
= Measure SpecType DataCon -> Maybe (Measure SpecType DataCon)
forall a. a -> Maybe a
Just (Measure SpecType DataCon -> Maybe (Measure SpecType DataCon))
-> Measure SpecType DataCon -> Maybe (Measure SpecType DataCon)
forall a b. (a -> b) -> a -> b
$ LocSymbol
-> SpecType -> DataCon -> Int -> Int -> Measure SpecType DataCon
forall a1.
Show a1 =>
LocSymbol
-> SpecType -> DataCon -> Int -> a1 -> Measure SpecType DataCon
makeMeasureSelector (SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (Maybe DataConMap -> DataCon -> Int -> Symbol
Bare.makeDataConSelector (DataConMap -> Maybe DataConMap
forall a. a -> Maybe a
Just DataConMap
dm) DataCon
dc Int
i)) (Int -> SpecType
projT Int
i) DataCon
dc Int
n Int
i
fields :: [((Symbol, SpecType), Int)]
fields = [(Symbol, SpecType)] -> [Int] -> [((Symbol, SpecType), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. [a] -> [a]
reverse [(Symbol, SpecType)]
xts) [Int
1..]
n :: Int
n = [(Symbol, SpecType)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, SpecType)]
xts
checker :: Measure SpecType DataCon
checker = LocSymbol -> SpecType -> DataCon -> Int -> Measure SpecType DataCon
makeMeasureChecker (SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (DataCon -> Symbol
Bare.makeDataConChecker DataCon
dc)) SpecType
checkT DataCon
dc Int
n
projT :: Int -> SpecType
projT Int
i = Bool -> DataCon -> Int -> DataConSel -> SpecType
dataConSel Bool
permitTC DataCon
dc Int
n (Int -> DataConSel
Proj Int
i)
checkT :: SpecType
checkT = Bool -> DataCon -> Int -> DataConSel -> SpecType
dataConSel Bool
permitTC DataCon
dc Int
n DataConSel
Check
permitTC :: Bool
permitTC = Config -> Bool
typeclass Config
cfg
dataConSel :: Bool -> Ghc.DataCon -> Int -> DataConSel -> SpecType
dataConSel :: Bool -> DataCon -> Int -> DataConSel -> SpecType
dataConSel Bool
permitTC DataCon
dc Int
n DataConSel
Check = [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [PVar (RType RTyCon RTyVar ())]
-> [(Symbol, RFInfo, SpecType, RReft)]
-> SpecType
-> SpecType
forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow ((RTVar RTyVar (RType RTyCon RTyVar ())
-> (RTVar RTyVar (RType RTyCon RTyVar ()), RReft))
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
forall a b. (a -> b) -> [a] -> [b]
map (, RReft
forall a. Monoid a => a
mempty) [RTVar RTyVar (RType RTyCon RTyVar ())]
as) [] [(Symbol, RFInfo, SpecType, RReft)
xt] SpecType
bareBool
where
([RTVar RTyVar (RType RTyCon RTyVar ())]
as, [SpecType]
_, (Symbol, RFInfo, SpecType, RReft)
xt) = Bool
-> DataCon
-> Int
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [SpecType],
(Symbol, RFInfo, SpecType, RReft))
forall r.
(Reftable (RTProp RTyCon RTyVar r), PPrint r, Reftable r) =>
Bool
-> DataCon
-> Int
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [RRType r],
(Symbol, RFInfo, RRType r, r))
bkDataCon Bool
permitTC DataCon
dc Int
n
dataConSel Bool
permitTC DataCon
dc Int
n (Proj Int
i) = [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [PVar (RType RTyCon RTyVar ())]
-> [(Symbol, RFInfo, SpecType, RReft)]
-> SpecType
-> SpecType
forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow ((RTVar RTyVar (RType RTyCon RTyVar ())
-> (RTVar RTyVar (RType RTyCon RTyVar ()), RReft))
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
forall a b. (a -> b) -> [a] -> [b]
map (, RReft
forall a. Monoid a => a
mempty) [RTVar RTyVar (RType RTyCon RTyVar ())]
as) [] [(Symbol, RFInfo, SpecType, RReft)
xt] (RReft -> RReft
forall a. Monoid a => a
mempty (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
ti)
where
ti :: SpecType
ti = SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
Mb.fromMaybe SpecType
forall {a}. a
err (Maybe SpecType -> SpecType) -> Maybe SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ Int -> [SpecType] -> Maybe SpecType
forall a. Int -> [a] -> Maybe a
Misc.getNth (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [SpecType]
ts
([RTVar RTyVar (RType RTyCon RTyVar ())]
as, [SpecType]
ts, (Symbol, RFInfo, SpecType, RReft)
xt) = Bool
-> DataCon
-> Int
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [SpecType],
(Symbol, RFInfo, SpecType, RReft))
forall r.
(Reftable (RTProp RTyCon RTyVar r), PPrint r, Reftable r) =>
Bool
-> DataCon
-> Int
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [RRType r],
(Symbol, RFInfo, RRType r, r))
bkDataCon Bool
permitTC DataCon
dc Int
n
err :: a
err = Maybe SrcSpan -> String -> a
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"DataCon " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DataCon -> String
forall a. Show a => a -> String
show DataCon
dc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"does not have " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" fields"
bkDataCon :: (F.Reftable (RTProp RTyCon RTyVar r), PPrint r, F.Reftable r) => Bool -> Ghc.DataCon -> Int -> ([RTVar RTyVar RSort], [RRType r], (F.Symbol, RFInfo, RRType r, r))
bkDataCon :: forall r.
(Reftable (RTProp RTyCon RTyVar r), PPrint r, Reftable r) =>
Bool
-> DataCon
-> Int
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [RRType r],
(Symbol, RFInfo, RRType r, r))
bkDataCon Bool
permitTC DataCon
dcn Int
nFlds = ([RTVar RTyVar (RType RTyCon RTyVar ())]
forall {s}. [RTVar RTyVar s]
as, [RRType r]
ts, (Symbol
F.dummySymbol, Bool -> RFInfo
classRFInfo Bool
permitTC, RRType r
t, r
forall a. Monoid a => a
mempty))
where
ts :: [RRType r]
ts = Type -> RRType r
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> RRType r) -> [Type] -> [RRType r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
Misc.takeLast Int
nFlds ((Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
Ghc.irrelevantMult [Scaled Type]
_ts)
t :: RRType r
t =
Type -> RRType r
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> RRType r) -> Type -> RRType r
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type
Ghc.mkTyConApp TyCon
tc [Type]
tArgs'
as :: [RTVar RTyVar s]
as = RTyVar -> RTVar RTyVar s
forall tv s. tv -> RTVar tv s
makeRTVar (RTyVar -> RTVar RTyVar s)
-> (TyCoVar -> RTyVar) -> TyCoVar -> RTVar RTyVar s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCoVar -> RTyVar
RT.rTyVar (TyCoVar -> RTVar RTyVar s) -> [TyCoVar] -> [RTVar RTyVar s]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([TyCoVar]
αs [TyCoVar] -> [TyCoVar] -> [TyCoVar]
forall a. [a] -> [a] -> [a]
++ [TyCoVar]
αs')
(([TyCoVar]
αs,[TyCoVar]
αs',[EqSpec]
_,[Type]
_,[Scaled Type]
_ts,Type
_t), Type
_t0) = DataCon
-> (([TyCoVar], [TyCoVar], [EqSpec], [Type], [Scaled Type], Type),
Type)
hammer DataCon
dcn
tArgs' :: [Type]
tArgs' = Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
take (Int
nArgs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nVars) [Type]
tArgs [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ (TyCoVar -> Type
Ghc.mkTyVarTy (TyCoVar -> Type) -> [TyCoVar] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyCoVar]
αs)
nVars :: Int
nVars = [TyCoVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyCoVar]
αs
nArgs :: Int
nArgs = [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tArgs
(TyCon
tc, [Type]
tArgs) = (TyCon, [Type]) -> Maybe (TyCon, [Type]) -> (TyCon, [Type])
forall a. a -> Maybe a -> a
Mb.fromMaybe (TyCon, [Type])
forall {a}. a
err ((() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
Ghc.splitTyConApp_maybe Type
_t)
err :: b
err = DataCon -> String -> b
forall a b. NamedThing a => a -> String -> b
GM.namedPanic DataCon
dcn (String
"Cannot split result type of DataCon " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DataCon -> String
forall a. Show a => a -> String
show DataCon
dcn)
hammer :: DataCon
-> (([TyCoVar], [TyCoVar], [EqSpec], [Type], [Scaled Type], Type),
Type)
hammer DataCon
dc = (DataCon
-> ([TyCoVar], [TyCoVar], [EqSpec], [Type], [Scaled Type], Type)
Ghc.dataConFullSig DataCon
dc, TyCoVar -> Type
Ghc.varType (TyCoVar -> Type) -> (DataCon -> TyCoVar) -> DataCon -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> TyCoVar
Ghc.dataConWorkId (DataCon -> Type) -> DataCon -> Type
forall a b. (a -> b) -> a -> b
$ DataCon
dc)
data DataConSel = Check | Proj Int
bareBool :: SpecType
bareBool :: SpecType
bareBool = RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (TyCon -> [PVar (RType RTyCon RTyVar ())] -> TyConInfo -> RTyCon
RTyCon TyCon
Ghc.boolTyCon [] TyConInfo
forall a. Default a => a
def) [] [] RReft
forall a. Monoid a => a
mempty
makeMeasureSelector :: (Show a1) => LocSymbol -> SpecType -> Ghc.DataCon -> Int -> a1 -> Measure SpecType Ghc.DataCon
makeMeasureSelector :: forall a1.
Show a1 =>
LocSymbol
-> SpecType -> DataCon -> Int -> a1 -> Measure SpecType DataCon
makeMeasureSelector LocSymbol
x SpecType
s DataCon
dc Int
n a1
i = M { msName :: LocSymbol
msName = LocSymbol
x, msSort :: SpecType
msSort = SpecType
s, msEqns :: [Def SpecType DataCon]
msEqns = [Def SpecType DataCon
forall {ty}. Def ty DataCon
eqn], msKind :: MeasureKind
msKind = MeasureKind
MsSelector, msUnSorted :: UnSortedExprs
msUnSorted = UnSortedExprs
forall a. Monoid a => a
mempty}
where
eqn :: Def ty DataCon
eqn = LocSymbol
-> DataCon
-> Maybe ty
-> [(Symbol, Maybe ty)]
-> Body
-> Def ty DataCon
forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
x DataCon
dc Maybe ty
forall a. Maybe a
Nothing [(Symbol, Maybe ty)]
forall {a}. [(Symbol, Maybe a)]
args (Expr -> Body
E (Symbol -> Expr
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ a1 -> Symbol
forall {a}. Show a => a -> Symbol
mkx a1
i))
args :: [(Symbol, Maybe a)]
args = (, Maybe a
forall a. Maybe a
Nothing) (Symbol -> (Symbol, Maybe a))
-> (Int -> Symbol) -> Int -> (Symbol, Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Symbol
forall {a}. Show a => a -> Symbol
mkx (Int -> (Symbol, Maybe a)) -> [Int] -> [(Symbol, Maybe a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1 .. Int
n]
mkx :: a -> Symbol
mkx a
j = String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String
"xx" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
j)
makeMeasureChecker :: LocSymbol -> SpecType -> Ghc.DataCon -> Int -> Measure SpecType Ghc.DataCon
makeMeasureChecker :: LocSymbol -> SpecType -> DataCon -> Int -> Measure SpecType DataCon
makeMeasureChecker LocSymbol
x SpecType
s0 DataCon
dc Int
n = M { msName :: LocSymbol
msName = LocSymbol
x, msSort :: SpecType
msSort = SpecType
s, msEqns :: [Def SpecType DataCon]
msEqns = Def SpecType DataCon
forall {ty}. Def ty DataCon
eqn Def SpecType DataCon
-> [Def SpecType DataCon] -> [Def SpecType DataCon]
forall a. a -> [a] -> [a]
: (DataCon -> Def SpecType DataCon
forall {ty}. DataCon -> Def ty DataCon
eqns (DataCon -> Def SpecType DataCon)
-> [DataCon] -> [Def SpecType DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DataCon -> Bool) -> [DataCon] -> [DataCon]
forall a. (a -> Bool) -> [a] -> [a]
filter (DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
/= DataCon
dc) [DataCon]
dcs), msKind :: MeasureKind
msKind = MeasureKind
MsChecker, msUnSorted :: UnSortedExprs
msUnSorted = UnSortedExprs
forall a. Monoid a => a
mempty }
where
s :: SpecType
s = String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp (String
"makeMeasureChecker: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LocSymbol -> String
forall a. Show a => a -> String
show LocSymbol
x) SpecType
s0
eqn :: Def ty DataCon
eqn = LocSymbol
-> DataCon
-> Maybe ty
-> [(Symbol, Maybe ty)]
-> Body
-> Def ty DataCon
forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
x DataCon
dc Maybe ty
forall a. Maybe a
Nothing ((, Maybe ty
forall a. Maybe a
Nothing) (Symbol -> (Symbol, Maybe ty))
-> (Int -> Symbol) -> Int -> (Symbol, Maybe ty)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Symbol
forall {a}. Show a => a -> Symbol
mkx (Int -> (Symbol, Maybe ty)) -> [Int] -> [(Symbol, Maybe ty)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1 .. Int
n]) (Expr -> Body
P Expr
F.PTrue)
eqns :: DataCon -> Def ty DataCon
eqns DataCon
d = LocSymbol
-> DataCon
-> Maybe ty
-> [(Symbol, Maybe ty)]
-> Body
-> Def ty DataCon
forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
x DataCon
d Maybe ty
forall a. Maybe a
Nothing ((, Maybe ty
forall a. Maybe a
Nothing) (Symbol -> (Symbol, Maybe ty))
-> (Int -> Symbol) -> Int -> (Symbol, Maybe ty)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Symbol
forall {a}. Show a => a -> Symbol
mkx (Int -> (Symbol, Maybe ty)) -> [Int] -> [(Symbol, Maybe ty)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1 .. DataCon -> Int
nArgs DataCon
d]) (Expr -> Body
P Expr
F.PFalse)
nArgs :: DataCon -> Int
nArgs DataCon
d = [Scaled Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DataCon -> [Scaled Type]
Ghc.dataConOrigArgTys DataCon
d)
mkx :: a -> Symbol
mkx a
j = String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String
"xx" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
j)
dcs :: [DataCon]
dcs = TyCon -> [DataCon]
Ghc.tyConDataCons (DataCon -> TyCon
Ghc.dataConTyCon DataCon
dc)
makeMeasureSpec' :: Bool -> MSpec SpecType Ghc.DataCon -> ([(Ghc.Var, SpecType)], [(LocSymbol, RRType F.Reft)])
makeMeasureSpec' :: Bool
-> MSpec SpecType DataCon
-> ([(TyCoVar, SpecType)], [(LocSymbol, RRType Reft)])
makeMeasureSpec' Bool
allowTC MSpec SpecType DataCon
mspec0 = ([(TyCoVar, SpecType)]
ctorTys, [(LocSymbol, RRType Reft)]
measTys)
where
ctorTys :: [(TyCoVar, SpecType)]
ctorTys = (RRType Reft -> SpecType)
-> (TyCoVar, RRType Reft) -> (TyCoVar, SpecType)
forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd RRType Reft -> SpecType
forall c tv a. RType c tv a -> RType c tv (UReft a)
RT.uRType ((TyCoVar, RRType Reft) -> (TyCoVar, SpecType))
-> [(TyCoVar, RRType Reft)] -> [(TyCoVar, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyCoVar, RRType Reft)]
ctorTys0
([(TyCoVar, RRType Reft)]
ctorTys0, [(LocSymbol, RRType Reft)]
measTys) = Bool
-> MSpec (RRType Reft) DataCon
-> ([(TyCoVar, RRType Reft)], [(LocSymbol, RRType Reft)])
Ms.dataConTypes Bool
allowTC MSpec (RRType Reft) DataCon
mspec
mspec :: MSpec (RRType Reft) DataCon
mspec = (SpecType -> RRType Reft)
-> MSpec SpecType DataCon -> MSpec (RRType Reft) DataCon
forall a b c. (a -> b) -> MSpec a c -> MSpec b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((RReft -> Reft) -> SpecType -> RRType Reft
forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft RReft -> Reft
forall r. UReft r -> r
ur_reft) MSpec SpecType DataCon
mspec0
makeMeasureSpec :: Bare.Env -> Bare.SigEnv -> ModName -> (ModName, Ms.BareSpec) ->
Bare.Lookup (Ms.MSpec SpecType Ghc.DataCon)
makeMeasureSpec :: Env
-> SigEnv
-> ModName
-> (ModName, BareSpec)
-> Lookup (MSpec SpecType DataCon)
makeMeasureSpec Env
env SigEnv
sigEnv ModName
myName (ModName
name, BareSpec
spec)
= Env
-> ModName
-> MSpec SpecType LocSymbol
-> Lookup (MSpec SpecType DataCon)
forall t.
Env -> ModName -> MSpec t LocSymbol -> Lookup (MSpec t DataCon)
mkMeasureDCon Env
env ModName
name
(MSpec SpecType LocSymbol -> Lookup (MSpec SpecType DataCon))
-> (BareSpec -> MSpec SpecType LocSymbol)
-> BareSpec
-> Lookup (MSpec SpecType DataCon)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> ModName -> MSpec BareType LocSymbol -> MSpec SpecType LocSymbol
mkMeasureSort Env
env ModName
name
(MSpec BareType LocSymbol -> MSpec SpecType LocSymbol)
-> (BareSpec -> MSpec BareType LocSymbol)
-> BareSpec
-> MSpec SpecType LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located BareType -> BareType)
-> MSpec (Located BareType) LocSymbol -> MSpec BareType LocSymbol
forall a b c. (a -> b) -> MSpec a c -> MSpec b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Located BareType -> BareType
forall a. Located a -> a
val
(MSpec (Located BareType) LocSymbol -> MSpec BareType LocSymbol)
-> (BareSpec -> MSpec (Located BareType) LocSymbol)
-> BareSpec
-> MSpec BareType LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv
-> ModName
-> ModName
-> BareSpec
-> MSpec (Located BareType) LocSymbol
bareMSpec Env
env SigEnv
sigEnv ModName
myName ModName
name
(BareSpec -> Lookup (MSpec SpecType DataCon))
-> BareSpec -> Lookup (MSpec SpecType DataCon)
forall a b. (a -> b) -> a -> b
$ BareSpec
spec
bareMSpec :: Bare.Env -> Bare.SigEnv -> ModName -> ModName -> Ms.BareSpec -> Ms.MSpec LocBareType LocSymbol
bareMSpec :: Env
-> SigEnv
-> ModName
-> ModName
-> BareSpec
-> MSpec (Located BareType) LocSymbol
bareMSpec Env
env SigEnv
sigEnv ModName
myName ModName
name BareSpec
spec = [Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) ()]
-> [Measure (Located BareType) LocSymbol]
-> MSpec (Located BareType) LocSymbol
forall t.
[Measure t LocSymbol]
-> [Measure t ()] -> [Measure t LocSymbol] -> MSpec t LocSymbol
Ms.mkMSpec [Measure (Located BareType) LocSymbol]
ms [Measure (Located BareType) ()]
cms [Measure (Located BareType) LocSymbol]
ims
where
cms :: [Measure (Located BareType) ()]
cms = String
-> [Measure (Located BareType) ()]
-> [Measure (Located BareType) ()]
forall a. PPrint a => String -> a -> a
F.notracepp String
"CMS" ([Measure (Located BareType) ()]
-> [Measure (Located BareType) ()])
-> [Measure (Located BareType) ()]
-> [Measure (Located BareType) ()]
forall a b. (a -> b) -> a -> b
$ (Measure (Located BareType) () -> Bool)
-> [Measure (Located BareType) ()]
-> [Measure (Located BareType) ()]
forall a. (a -> Bool) -> [a] -> [a]
filter Measure (Located BareType) () -> Bool
forall {ctor}. Measure (Located BareType) ctor -> Bool
inScope1 ([Measure (Located BareType) ()]
-> [Measure (Located BareType) ()])
-> [Measure (Located BareType) ()]
-> [Measure (Located BareType) ()]
forall a b. (a -> b) -> a -> b
$ BareSpec -> [Measure (Located BareType) ()]
forall ty bndr. Spec ty bndr -> [Measure ty ()]
Ms.cmeasures BareSpec
spec
ms :: [Measure (Located BareType) LocSymbol]
ms = String
-> [Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol]
forall a. PPrint a => String -> a -> a
F.notracepp String
"UMS" ([Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol])
-> [Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol]
forall a b. (a -> b) -> a -> b
$ (Measure (Located BareType) LocSymbol -> Bool)
-> [Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol]
forall a. (a -> Bool) -> [a] -> [a]
filter Measure (Located BareType) LocSymbol -> Bool
inScope2 ([Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol])
-> [Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol]
forall a b. (a -> b) -> a -> b
$ Measure (Located BareType) LocSymbol
-> Measure (Located BareType) LocSymbol
expMeas (Measure (Located BareType) LocSymbol
-> Measure (Located BareType) LocSymbol)
-> [Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure (Located BareType) LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.measures BareSpec
spec
ims :: [Measure (Located BareType) LocSymbol]
ims = String
-> [Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol]
forall a. PPrint a => String -> a -> a
F.notracepp String
"IMS" ([Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol])
-> [Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol]
forall a b. (a -> b) -> a -> b
$ (Measure (Located BareType) LocSymbol -> Bool)
-> [Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol]
forall a. (a -> Bool) -> [a] -> [a]
filter Measure (Located BareType) LocSymbol -> Bool
inScope2 ([Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol])
-> [Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol]
forall a b. (a -> b) -> a -> b
$ Measure (Located BareType) LocSymbol
-> Measure (Located BareType) LocSymbol
expMeas (Measure (Located BareType) LocSymbol
-> Measure (Located BareType) LocSymbol)
-> [Measure (Located BareType) LocSymbol]
-> [Measure (Located BareType) LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure (Located BareType) LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.imeasures BareSpec
spec
expMeas :: Measure (Located BareType) LocSymbol
-> Measure (Located BareType) LocSymbol
expMeas = Env
-> ModName
-> BareRTEnv
-> Measure (Located BareType) LocSymbol
-> Measure (Located BareType) LocSymbol
expandMeasure Env
env ModName
name BareRTEnv
rtEnv
rtEnv :: BareRTEnv
rtEnv = SigEnv -> BareRTEnv
Bare.sigRTEnv SigEnv
sigEnv
force :: Bool
force = ModName
name ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
myName
inScope1 :: Measure (Located BareType) ctor -> Bool
inScope1 Measure (Located BareType) ctor
z = String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
F.notracepp (String
"inScope1: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LocSymbol -> String
forall a. PPrint a => a -> String
F.showpp (Measure (Located BareType) ctor -> LocSymbol
forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure (Located BareType) ctor
z)) (Bool
force Bool -> Bool -> Bool
|| Measure (Located BareType) ctor -> Bool
forall {ctor}. Measure (Located BareType) ctor -> Bool
okSort Measure (Located BareType) ctor
z)
inScope2 :: Measure (Located BareType) LocSymbol -> Bool
inScope2 Measure (Located BareType) LocSymbol
z = String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
F.notracepp (String
"inScope2: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LocSymbol -> String
forall a. PPrint a => a -> String
F.showpp (Measure (Located BareType) LocSymbol -> LocSymbol
forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure (Located BareType) LocSymbol
z)) (Bool
force Bool -> Bool -> Bool
|| (Measure (Located BareType) LocSymbol -> Bool
forall {ctor}. Measure (Located BareType) ctor -> Bool
okSort Measure (Located BareType) LocSymbol
z Bool -> Bool -> Bool
&& Measure (Located BareType) LocSymbol -> Bool
forall {ty}. Measure ty LocSymbol -> Bool
okCtors Measure (Located BareType) LocSymbol
z))
okSort :: Measure (Located BareType) ctor -> Bool
okSort = Env -> ModName -> Located BareType -> Bool
Bare.knownGhcType Env
env ModName
name (Located BareType -> Bool)
-> (Measure (Located BareType) ctor -> Located BareType)
-> Measure (Located BareType) ctor
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Measure (Located BareType) ctor -> Located BareType
forall ty ctor. Measure ty ctor -> ty
msSort
okCtors :: Measure ty LocSymbol -> Bool
okCtors = (Def ty LocSymbol -> Bool) -> [Def ty LocSymbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Env -> ModName -> LocSymbol -> Bool
Bare.knownGhcDataCon Env
env ModName
name (LocSymbol -> Bool)
-> (Def ty LocSymbol -> LocSymbol) -> Def ty LocSymbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Def ty LocSymbol -> LocSymbol
forall ty ctor. Def ty ctor -> ctor
ctor) ([Def ty LocSymbol] -> Bool)
-> (Measure ty LocSymbol -> [Def ty LocSymbol])
-> Measure ty LocSymbol
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Measure ty LocSymbol -> [Def ty LocSymbol]
forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns
mkMeasureDCon :: Bare.Env -> ModName -> Ms.MSpec t LocSymbol -> Bare.Lookup (Ms.MSpec t Ghc.DataCon)
mkMeasureDCon :: forall t.
Env -> ModName -> MSpec t LocSymbol -> Lookup (MSpec t DataCon)
mkMeasureDCon Env
env ModName
name MSpec t LocSymbol
m = do
let ns :: [LocSymbol]
ns = MSpec t LocSymbol -> [LocSymbol]
forall t. MSpec t LocSymbol -> [LocSymbol]
measureCtors MSpec t LocSymbol
m
[DataCon]
dcs <- (LocSymbol -> Either [Error] DataCon)
-> [LocSymbol] -> Either [Error] [DataCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> ModName -> String -> LocSymbol -> Either [Error] DataCon
Bare.lookupGhcDataCon Env
env ModName
name String
"measure-datacon") [LocSymbol]
ns
MSpec t DataCon -> Lookup (MSpec t DataCon)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (MSpec t DataCon -> Lookup (MSpec t DataCon))
-> MSpec t DataCon -> Lookup (MSpec t DataCon)
forall a b. (a -> b) -> a -> b
$ MSpec t LocSymbol -> [(Symbol, DataCon)] -> MSpec t DataCon
forall t.
MSpec t LocSymbol -> [(Symbol, DataCon)] -> MSpec t DataCon
mkMeasureDCon_ MSpec t LocSymbol
m ([Symbol] -> [DataCon] -> [(Symbol, DataCon)]
forall a b. [a] -> [b] -> [(a, b)]
zip (LocSymbol -> Symbol
forall a. Located a -> a
val (LocSymbol -> Symbol) -> [LocSymbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
ns) [DataCon]
dcs)
mkMeasureDCon_ :: Ms.MSpec t LocSymbol -> [(F.Symbol, Ghc.DataCon)] -> Ms.MSpec t Ghc.DataCon
mkMeasureDCon_ :: forall t.
MSpec t LocSymbol -> [(Symbol, DataCon)] -> MSpec t DataCon
mkMeasureDCon_ MSpec t LocSymbol
m [(Symbol, DataCon)]
ndcs = MSpec t DataCon
m' {Ms.ctorMap = cm'}
where
m' :: MSpec t DataCon
m' = (LocSymbol -> DataCon) -> MSpec t LocSymbol -> MSpec t DataCon
forall a b. (a -> b) -> MSpec t a -> MSpec t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Symbol -> DataCon
tx(Symbol -> DataCon)
-> (LocSymbol -> Symbol) -> LocSymbol -> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
.LocSymbol -> Symbol
forall a. Located a -> a
val) MSpec t LocSymbol
m
cm' :: HashMap Symbol [Def t DataCon]
cm' = (Symbol -> Symbol)
-> HashMap Symbol [Def t DataCon] -> HashMap Symbol [Def t DataCon]
forall k2 k1 v.
(Eq k2, Hashable k2) =>
(k1 -> k2) -> HashMap k1 v -> HashMap k2 v
Misc.hashMapMapKeys (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DataCon -> Symbol) -> (Symbol -> DataCon) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> DataCon
tx) (HashMap Symbol [Def t DataCon] -> HashMap Symbol [Def t DataCon])
-> HashMap Symbol [Def t DataCon] -> HashMap Symbol [Def t DataCon]
forall a b. (a -> b) -> a -> b
$ MSpec t DataCon -> HashMap Symbol [Def t DataCon]
forall ty ctor. MSpec ty ctor -> HashMap Symbol [Def ty ctor]
Ms.ctorMap MSpec t DataCon
m'
tx :: Symbol -> DataCon
tx = HashMap Symbol DataCon -> Symbol -> DataCon
forall k v.
(?callStack::CallStack, Eq k, Show k, Hashable k) =>
HashMap k v -> k -> v
Misc.mlookup ([(Symbol, DataCon)] -> HashMap Symbol DataCon
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Symbol, DataCon)]
ndcs)
measureCtors :: Ms.MSpec t LocSymbol -> [LocSymbol]
measureCtors :: forall t. MSpec t LocSymbol -> [LocSymbol]
measureCtors = [LocSymbol] -> [LocSymbol]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([LocSymbol] -> [LocSymbol])
-> (MSpec t LocSymbol -> [LocSymbol])
-> MSpec t LocSymbol
-> [LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Def t LocSymbol -> LocSymbol) -> [Def t LocSymbol] -> [LocSymbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Def t LocSymbol -> LocSymbol
forall ty ctor. Def ty ctor -> ctor
ctor ([Def t LocSymbol] -> [LocSymbol])
-> (MSpec t LocSymbol -> [Def t LocSymbol])
-> MSpec t LocSymbol
-> [LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Def t LocSymbol]] -> [Def t LocSymbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Def t LocSymbol]] -> [Def t LocSymbol])
-> (MSpec t LocSymbol -> [[Def t LocSymbol]])
-> MSpec t LocSymbol
-> [Def t LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Symbol [Def t LocSymbol] -> [[Def t LocSymbol]]
forall k v. HashMap k v -> [v]
M.elems (HashMap Symbol [Def t LocSymbol] -> [[Def t LocSymbol]])
-> (MSpec t LocSymbol -> HashMap Symbol [Def t LocSymbol])
-> MSpec t LocSymbol
-> [[Def t LocSymbol]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MSpec t LocSymbol -> HashMap Symbol [Def t LocSymbol]
forall ty ctor. MSpec ty ctor -> HashMap Symbol [Def ty ctor]
Ms.ctorMap
mkMeasureSort :: Bare.Env -> ModName -> Ms.MSpec BareType LocSymbol
-> Ms.MSpec SpecType LocSymbol
mkMeasureSort :: Env
-> ModName -> MSpec BareType LocSymbol -> MSpec SpecType LocSymbol
mkMeasureSort Env
env ModName
name (Ms.MSpec HashMap Symbol [Def BareType LocSymbol]
c HashMap LocSymbol (Measure BareType LocSymbol)
mm HashMap LocSymbol (Measure BareType ())
cm [Measure BareType LocSymbol]
im) =
HashMap Symbol [Def SpecType LocSymbol]
-> HashMap LocSymbol (Measure SpecType LocSymbol)
-> HashMap LocSymbol (Measure SpecType ())
-> [Measure SpecType LocSymbol]
-> MSpec SpecType LocSymbol
forall ty ctor.
HashMap Symbol [Def ty ctor]
-> HashMap LocSymbol (Measure ty ctor)
-> HashMap LocSymbol (Measure ty ())
-> [Measure ty ctor]
-> MSpec ty ctor
Ms.MSpec ((Def BareType LocSymbol -> Def SpecType LocSymbol)
-> [Def BareType LocSymbol] -> [Def SpecType LocSymbol]
forall a b. (a -> b) -> [a] -> [b]
map Def BareType LocSymbol -> Def SpecType LocSymbol
forall ctor. Def BareType ctor -> Def SpecType ctor
txDef ([Def BareType LocSymbol] -> [Def SpecType LocSymbol])
-> HashMap Symbol [Def BareType LocSymbol]
-> HashMap Symbol [Def SpecType LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Symbol [Def BareType LocSymbol]
c) (Measure BareType LocSymbol -> Measure SpecType LocSymbol
forall ctor. Measure BareType ctor -> Measure SpecType ctor
tx (Measure BareType LocSymbol -> Measure SpecType LocSymbol)
-> HashMap LocSymbol (Measure BareType LocSymbol)
-> HashMap LocSymbol (Measure SpecType LocSymbol)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap LocSymbol (Measure BareType LocSymbol)
mm) (Measure BareType () -> Measure SpecType ()
forall ctor. Measure BareType ctor -> Measure SpecType ctor
tx (Measure BareType () -> Measure SpecType ())
-> HashMap LocSymbol (Measure BareType ())
-> HashMap LocSymbol (Measure SpecType ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap LocSymbol (Measure BareType ())
cm) (Measure BareType LocSymbol -> Measure SpecType LocSymbol
forall ctor. Measure BareType ctor -> Measure SpecType ctor
tx (Measure BareType LocSymbol -> Measure SpecType LocSymbol)
-> [Measure BareType LocSymbol] -> [Measure SpecType LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Measure BareType LocSymbol]
im)
where
ofMeaSort :: F.SourcePos -> BareType -> SpecType
ofMeaSort :: SourcePos -> BareType -> SpecType
ofMeaSort SourcePos
l = Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> SpecType
Bare.ofBareType Env
env ModName
name SourcePos
l Maybe [PVar BSort]
forall a. Maybe a
Nothing
tx :: Measure BareType ctor -> Measure SpecType ctor
tx :: forall ctor. Measure BareType ctor -> Measure SpecType ctor
tx (M LocSymbol
n BareType
s [Def BareType ctor]
eqs MeasureKind
k UnSortedExprs
u) = LocSymbol
-> SpecType
-> [Def SpecType ctor]
-> MeasureKind
-> UnSortedExprs
-> Measure SpecType ctor
forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
M LocSymbol
n (SourcePos -> BareType -> SpecType
ofMeaSort SourcePos
l BareType
s) (Def BareType ctor -> Def SpecType ctor
forall ctor. Def BareType ctor -> Def SpecType ctor
txDef (Def BareType ctor -> Def SpecType ctor)
-> [Def BareType ctor] -> [Def SpecType ctor]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Def BareType ctor]
eqs) MeasureKind
k UnSortedExprs
u where l :: SourcePos
l = LocSymbol -> SourcePos
forall a. Loc a => a -> SourcePos
GM.fSourcePos LocSymbol
n
txDef :: Def BareType ctor -> Def SpecType ctor
txDef :: forall ctor. Def BareType ctor -> Def SpecType ctor
txDef Def BareType ctor
d = (BareType -> SpecType) -> Def BareType ctor -> Def SpecType ctor
forall a b c. (a -> b) -> Def a c -> Def b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SourcePos -> BareType -> SpecType
ofMeaSort SourcePos
l) Def BareType ctor
d where l :: SourcePos
l = LocSymbol -> SourcePos
forall a. Loc a => a -> SourcePos
GM.fSourcePos (Def BareType ctor -> LocSymbol
forall ty ctor. Def ty ctor -> LocSymbol
measure Def BareType ctor
d)
expandMeasure :: Bare.Env -> ModName -> BareRTEnv -> BareMeasure -> BareMeasure
expandMeasure :: Env
-> ModName
-> BareRTEnv
-> Measure (Located BareType) LocSymbol
-> Measure (Located BareType) LocSymbol
expandMeasure Env
env ModName
name BareRTEnv
rtEnv Measure (Located BareType) LocSymbol
m = Measure (Located BareType) LocSymbol
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 :: forall t.
Env -> ModName -> BareRTEnv -> Def t LocSymbol -> Def t LocSymbol
expandMeasureDef Env
env ModName
name BareRTEnv
rtEnv Def t LocSymbol
d = Def t LocSymbol
d
{ body = F.notracepp msg $ Bare.qualifyExpand env name rtEnv l bs (body d) }
where
l :: SourcePos
l = LocSymbol -> SourcePos
forall a. Located a -> SourcePos
loc (Def t LocSymbol -> LocSymbol
forall ty ctor. Def ty ctor -> LocSymbol
measure Def t LocSymbol
d)
bs :: [Symbol]
bs = (Symbol, Maybe t) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Maybe t) -> Symbol) -> [(Symbol, Maybe t)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Def t LocSymbol -> [(Symbol, Maybe t)]
forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def t LocSymbol
d
msg :: String
msg = String
"QUALIFY-EXPAND-BODY" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([Symbol], Body) -> String
forall a. PPrint a => a -> String
F.showpp ([Symbol]
bs, Def t LocSymbol -> Body
forall ty ctor. Def ty ctor -> Body
body Def t LocSymbol
d)
varMeasures :: (Monoid r) => Bare.Env -> [(F.Symbol, Located (RRType r))]
varMeasures :: forall r. Monoid r => Env -> [(Symbol, Located (RRType r))]
varMeasures Env
env =
[ (TyCoVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCoVar
v, TyCoVar -> Located (RRType r)
forall r. Monoid r => TyCoVar -> Located (RRType r)
varSpecType TyCoVar
v)
| TyCoVar
v <- Env -> [TyCoVar]
knownVars Env
env
, TyCoVar -> Bool
GM.isDataConId TyCoVar
v
, Type -> Bool
isSimpleType (TyCoVar -> Type
Ghc.varType TyCoVar
v) ]
knownVars :: Bare.Env -> [Ghc.Var]
knownVars :: Env -> [TyCoVar]
knownVars Env
env = [ TyCoVar
v | (Symbol
_, [(Symbol, TyThing)]
xThings) <- HashMap Symbol [(Symbol, TyThing)]
-> [(Symbol, [(Symbol, TyThing)])]
forall k v. HashMap k v -> [(k, v)]
M.toList (Env -> HashMap Symbol [(Symbol, TyThing)]
Bare._reTyThings Env
env)
, (Symbol
_,Ghc.AnId TyCoVar
v) <- [(Symbol, TyThing)]
xThings
]
varSpecType :: (Monoid r) => Ghc.Var -> Located (RRType r)
varSpecType :: forall r. Monoid r => TyCoVar -> Located (RRType r)
varSpecType = (TyCoVar -> RRType r) -> Located TyCoVar -> Located (RRType r)
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> RRType r
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> RRType r) -> (TyCoVar -> Type) -> TyCoVar -> RRType r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCoVar -> Type
Ghc.varType) (Located TyCoVar -> Located (RRType r))
-> (TyCoVar -> Located TyCoVar) -> TyCoVar -> Located (RRType r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCoVar -> Located TyCoVar
forall a. NamedThing a => a -> Located a
GM.locNamedThing
isSimpleType :: Ghc.Type -> Bool
isSimpleType :: Type -> Bool
isSimpleType = Sort -> Bool
isFirstOrder (Sort -> Bool) -> (Type -> Sort) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> Type -> Sort
RT.typeSort TCEmb TyCon
forall a. Monoid a => a
mempty
makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t
-> [(LocSymbol, CMeasure (RType c tv r2))]
makeClassMeasureSpec :: forall c tv r2 t.
MSpec (RType c tv (UReft r2)) t
-> [(LocSymbol, CMeasure (RType c tv r2))]
makeClassMeasureSpec Ms.MSpec{[Measure (RType c tv (UReft r2)) t]
HashMap LocSymbol (Measure (RType c tv (UReft r2)) t)
HashMap LocSymbol (Measure (RType c tv (UReft r2)) ())
HashMap Symbol [Def (RType c tv (UReft r2)) t]
ctorMap :: forall ty ctor. MSpec ty ctor -> HashMap Symbol [Def ty ctor]
ctorMap :: HashMap Symbol [Def (RType c tv (UReft r2)) t]
measMap :: HashMap LocSymbol (Measure (RType c tv (UReft r2)) t)
cmeasMap :: HashMap LocSymbol (Measure (RType c tv (UReft r2)) ())
imeas :: [Measure (RType c tv (UReft r2)) t]
measMap :: forall ty ctor.
MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor)
cmeasMap :: forall ty ctor. MSpec ty ctor -> HashMap LocSymbol (Measure ty ())
imeas :: forall ty ctor. MSpec ty ctor -> [Measure ty ctor]
..} = Measure (RType c tv (UReft r2)) ()
-> (LocSymbol, CMeasure (RType c tv r2))
forall {c} {tv} {r2} {ctor}.
Measure (RType c tv (UReft r2)) ctor
-> (LocSymbol, CMeasure (RType c tv r2))
tx (Measure (RType c tv (UReft r2)) ()
-> (LocSymbol, CMeasure (RType c tv r2)))
-> [Measure (RType c tv (UReft r2)) ()]
-> [(LocSymbol, CMeasure (RType c tv r2))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap LocSymbol (Measure (RType c tv (UReft r2)) ())
-> [Measure (RType c tv (UReft r2)) ()]
forall k v. HashMap k v -> [v]
M.elems HashMap LocSymbol (Measure (RType c tv (UReft r2)) ())
cmeasMap
where
tx :: Measure (RType c tv (UReft r2)) ctor
-> (LocSymbol, CMeasure (RType c tv r2))
tx (M LocSymbol
n RType c tv (UReft r2)
s [Def (RType c tv (UReft r2)) ctor]
_ MeasureKind
_ UnSortedExprs
_) = (LocSymbol
n, LocSymbol -> RType c tv r2 -> CMeasure (RType c tv r2)
forall ty. LocSymbol -> ty -> CMeasure ty
CM LocSymbol
n ((UReft r2 -> r2) -> RType c tv (UReft r2) -> RType c tv r2
forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft UReft r2 -> r2
forall r. UReft r -> r
ur_reft RType c tv (UReft r2)
s))