{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RecordWildCards  #-}
{-# LANGUAGE TupleSections    #-}

-- | This module contains (most of) the code needed to lift Haskell entitites,
--   . code- (CoreBind), and data- (Tycon) definitions into the spec level.

module Language.Haskell.Liquid.Bare.Measure
  ( makeHaskellMeasures
  , makeHaskellInlines
  , makeHaskellDataDecls
  , makeMeasureSelectors
  , makeMeasureSpec
  , makeMeasureSpec'
  , varMeasures
  , makeClassMeasureSpec
  -- , makeHaskellBounds
  ) where

import Data.Default
import qualified Control.Exception as Ex
import Prelude hiding (mapM, error)
import Data.Bifunctor
import qualified Data.Maybe as Mb
import Text.PrettyPrint.HughesPJ (text)
-- import Text.Printf     (printf)

import qualified Data.HashMap.Strict as M
import qualified Data.HashSet        as S

import           Language.Fixpoint.SortCheck (isFirstOrder)
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Transforms.CoreToLogic
import qualified Language.Fixpoint.Misc                as Misc
import qualified Language.Haskell.Liquid.Misc          as Misc
import           Language.Haskell.Liquid.Misc             ((.||.))
import qualified Liquid.GHC.API       as Ghc
import qualified Language.Haskell.Liquid.GHC.Misc      as GM
import qualified Language.Haskell.Liquid.Types.RefType as RT
import           Language.Haskell.Liquid.Types
-- import           Language.Haskell.Liquid.Types.Bounds
import qualified Language.Haskell.Liquid.Measure       as Ms

import qualified Language.Haskell.Liquid.Bare.Types    as Bare
import qualified Language.Haskell.Liquid.Bare.Resolve  as Bare
import qualified Language.Haskell.Liquid.Bare.Expand   as Bare
import qualified Language.Haskell.Liquid.Bare.DataType as Bare
import qualified Language.Haskell.Liquid.Bare.ToBare   as Bare
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 -- this should never happen!

    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'@ takes a @Maybe DataConMap@: we need a proper map when lifting
--   measures and reflects (which have case-of, and hence, need the projection symbols),
--   but NOT when lifting inlines (which do not have case-of).
--   For details, see [NOTE:Lifting-Stages]

coreToFun' :: 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
                    -- . F.tracepp "makeHaskellDataDecls-3"
                    ([((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)
                    -- . F.tracepp "makeHaskellDataDecls-2"
                    ([(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
                    -- . F.tracepp "makeHaskellDataDecls-1"
                    ([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"
  -- . (`sortDiff` wiredInTyCons)
  -- . F.tracepp "LiftableTCs 0"

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 :: {tc:TyCon | isAlgTyCon tc} -> Maybe DataDecl @-}
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     = {- F.notracepp msg $ -} 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)
    -- msg           = printf "dataConDecl (gadt = %s)" (show isGadt)
    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' converts the 'DataCon's and creates the measures for
--   the selectors and checkers that then enable reflection.
--------------------------------------------------------------------------------

makeMeasureSelectors :: Config -> Bare.DataConMap -> Located DataConP -> [Measure SpecType Ghc.DataCon]
makeMeasureSelectors :: 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) --  internal measures, needed for reflection
 [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) --  user-visible measures.
  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)
      -- do not make selectors for functional fields
      | 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)
      -- do not make selectors for functional fields
      | 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)          = {- traceShow ("dataConSel: " ++ show dc) $ -} 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)         = {- F.tracepp ("bkDatacon dc = " ++ F.showpp (dc, n)) $ -} 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 :: DataCon -> Int -> ([RTVar RTyVar RSort], [SpecType], (Symbol, SpecType, RReft))
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                 = -- Misc.traceShow ("bkDataConResult" ++ GM.showPpr (dc, _t, _t0)) $
                          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


{- | NOTE:Use DataconWorkId

      dcWorkId :: forall a1 ... aN. (a1 ~ X1 ...) => T1 -> ... -> Tn -> T
      checkT   :: forall as. T -> Bool
      projT t  :: forall as. T -> t

-}

makeMeasureSelector :: (Show a1) => LocSymbol -> SpecType -> Ghc.DataCon -> Int -> a1 -> Measure SpecType Ghc.DataCon
makeMeasureSelector :: 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 env name m = mkMeasureDCon_ m [ (val n, symDC n) | n <- measureCtors m ]
--   where
--     symDC                = Bare.lookupGhcDataCon env name "measure-datacon"

mkMeasureDCon_ :: Ms.MSpec t LocSymbol -> [(F.Symbol, Ghc.DataCon)] -> Ms.MSpec t Ghc.DataCon
mkMeasureDCon_ :: 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)



--------------------------------------------------------------------------------
-- | Expand Measures -----------------------------------------------------------
--------------------------------------------------------------------------------
-- type BareMeasure = Measure LocBareType LocSymbol

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))


{-
expandMeasureBody :: Bare.Env -> ModName -> BareRTEnv -> SourcePos -> Body -> Body
expandMeasureBody env name rtEnv l (P   p) = P   (Bare.expandQualify env name rtEnv l p)
expandMeasureBody env name rtEnv l (R x p) = R x (Bare.expandQualify env name rtEnv l p)
expandMeasureBody env name rtEnv l (E   e) = E   (Bare.expandQualify env name rtEnv l e)


makeHaskellBounds :: F.TCEmb TyCon -> CoreProgram -> S.HashSet (Var, LocSymbol) -> BareM RBEnv  -- TODO-REBARE
makeHaskellBounds embs cbs xs = do
  lmap <- gets logicEnv
  M.fromList <$> mapM (makeHaskellBound embs lmap cbs) (S.toList xs)

makeHaskellBound :: F.TCEmb TyCon
                 -> LogicMap
                 -> [Bind Var]
                 -> (Var, Located Symbol)
                 -> BareM (LocSymbol, RBound)
makeHaskellBound embs lmap  cbs (v, x) =
  case filter ((v  `elem`) . GM.binders) cbs of
    (NonRec v def:_)   -> toBound v x <$> coreToFun' embs lmap x v def return
    (Rec [(v, def)]:_) -> toBound v x <$> coreToFun' embs lmap x v def return
    _                  -> throwError $ errHMeas x "Cannot make bound of haskell function"



toBound :: Var -> LocSymbol -> ([Var], Either F.Expr F.Expr) -> (LocSymbol, RBound)
toBound v x (vs, Left p) = (x', Bound x' fvs ps xs p)
  where
    x'         = capitalizeBound x
    (ps', xs') = L.partition (hasBoolResult . varType) vs
    (ps , xs)  = (txp <$> ps', txx <$> xs')
    txp v      = (dummyLoc $ simpleSymbolVar v, RT.ofType $ varType v)
    txx v      = (dummyLoc $ symbol v,          RT.ofType $ varType v)
    fvs        = (((`RVar` mempty) . RTV) <$> fst (splitForAllTyCoVars $ varType v)) :: [RSort]

toBound v x (vs, Right e) = toBound v x (vs, Left e)

capitalizeBound :: Located Symbol -> Located Symbol
capitalizeBound = fmap (symbol . toUpperHead . symbolString)
  where
    toUpperHead []     = []
    toUpperHead (x:xs) = toUpper x:xs

-}