{-# 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 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 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 = forall a. HashSet a -> [a]
S.toList (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 (forall a. Located a -> a
val LocSymbol
x) [CoreBind]
cbs of
    Maybe (TyCoVar, CoreExpr)
Nothing        -> forall a e. Exception e => e -> a
Ex.throw 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) -> forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
Ms.mkM LocSymbol
vx Located SpecType
vinfo [Def (Located SpecType) DataCon]
mdef MeasureKind
MsLifted (Bool -> Type -> [Def (Located SpecType) DataCon] -> UnSortedExprs
makeUnSorted Bool
allowTC (TyCoVar -> Type
Ghc.varType TyCoVar
v) [Def (Located SpecType) DataCon]
mdef)
                     where
                       vx :: LocSymbol
vx           = forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
x (forall a. Symbolic a => a -> Symbol
F.symbol TyCoVar
v)
                       mdef :: [Def (Located SpecType) DataCon]
mdef         = Bool
-> TycEnv
-> LogicMap
-> LocSymbol
-> TyCoVar
-> CoreExpr
-> [Def (Located SpecType) DataCon]
coreToDef' Bool
allowTC TycEnv
tycEnv LogicMap
lmap LocSymbol
vx TyCoVar
v CoreExpr
cexp
                       vinfo :: Located SpecType
vinfo        = forall a. (Type -> a) -> TyCoVar -> Located a
GM.varLocInfo (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 (Located SpecType) DataCon] -> UnSortedExprs
makeUnSorted Bool
allowTC Type
ty [Def (Located SpecType) DataCon]
defs
  | Type -> Bool
isMeasureType Type
ta
  = forall a. Monoid a => a
mempty
  | Bool
otherwise
  = forall a b. (a -> b) -> [a] -> [b]
map forall {ty} {ctor}. Def ty ctor -> ([Symbol], Expr)
defToUnSortedExpr [Def (Located SpecType) DataCon]
defs
  where
    ta :: Type
ta = Type -> Type
go forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms Type
ty

    go :: Type -> Type
go (Ghc.ForAllTy TyCoVarBinder
_ 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) = 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 -> ([Symbol], Expr)
defToUnSortedExpr Def ty ctor
defn = (Symbol
xxforall a. a -> [a] -> [a]
:(forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def ty ctor
defn),
                             Expr -> Body -> Expr
Ms.bodyPred (LocSymbol -> [Expr] -> Expr
F.mkEApp (forall ty ctor. Def ty ctor -> LocSymbol
measure Def ty ctor
defn) [forall a. Expression a => a -> Expr
F.expr Symbol
xx]) (forall ty ctor. Def ty ctor -> Body
body Def ty ctor
defn))

    xx :: Symbol
xx = Maybe Integer -> Symbol
F.vv forall a b. (a -> b) -> a -> b
$ 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 (Located SpecType) DataCon]
coreToDef' Bool
allowTC TycEnv
tycEnv LogicMap
lmap LocSymbol
vx TyCoVar
v CoreExpr
defn =
  case 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) (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 (Located SpecType) DataCon]
l -> [Def (Located SpecType) DataCon]
l
    Left Error
e  -> 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 = forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc LocSymbol
x) (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ 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 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 = forall a. HashSet a -> [a]
S.toList        (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 (forall a. Located a -> a
val LocSymbol
x) [CoreBind]
cbs of
    Maybe (TyCoVar, CoreExpr)
Nothing        -> forall a e. Exception e => e -> a
Ex.throw 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, forall a.
Bool
-> TCEmb TyCon
-> Maybe DataConMap
-> LogicMap
-> LocSymbol
-> TyCoVar
-> CoreExpr
-> (([TyCoVar], Either Expr Expr) -> a)
-> a
coreToFun' Bool
allowTC TCEmb TyCon
embs forall a. Maybe a
Nothing LogicMap
lmap LocSymbol
vx TyCoVar
v CoreExpr
defn forall {a}. Symbolic a => ([a], Either Expr Expr) -> LMap
ok)
                     where
                       vx :: LocSymbol
vx         = forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
x (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 (forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs) (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> a
id 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 = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either 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  = 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   = forall a. a -> Maybe a -> a
Mb.fromMaybe forall a. Monoid a => a
mempty Maybe DataConMap
dmMb


nonRecCoreBinds :: [Ghc.CoreBind] -> [Ghc.CoreBind]
nonRecCoreBinds :: [CoreBind] -> [CoreBind]
nonRecCoreBinds            = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap 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)    = [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
  | forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg = BareSpec -> [DataDecl] -> [DataDecl]
Bare.dataDeclSize BareSpec
spec
                    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe ((TyCon, DataName), HasDataDecl) -> Maybe DataDecl
tyConDataDecl
                    -- . F.tracepp "makeHaskellDataDecls-3"
                    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [(a, b)]
zipMap   (ModName -> BareSpec -> TyCon -> HasDataDecl
hasDataDecl ModName
name BareSpec
spec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)
                    -- . F.tracepp "makeHaskellDataDecls-2"
                    forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TyCon] -> [(TyCon, DataName)]
liftableTyCons
                    -- . F.tracepp "makeHaskellDataDecls-1"
                    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter TyCon -> Bool
isReflectableTyCon
                    forall a b. (a -> b) -> a -> b
$ [TyCon]
tcs
  | Bool
otherwise       = []


isReflectableTyCon :: Ghc.TyCon -> Bool
isReflectableTyCon :: TyCon -> Bool
isReflectableTyCon  = TyCon -> Bool
Ghc.isFamInstTyCon forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
.||. TyCon -> Bool
Ghc.isVanillaAlgTyCon

liftableTyCons :: [Ghc.TyCon] -> [(Ghc.TyCon, DataName)]
liftableTyCons :: [TyCon] -> [(TyCon, DataName)]
liftableTyCons
  = forall a. PPrint a => String -> a -> a
F.notracepp String
"LiftableTCs 3"
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [(a, b)]
zipMapMaybe (Bool -> TyCon -> Maybe DataName
tyConDataName Bool
True)
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PPrint a => String -> a -> a
F.notracepp String
"LiftableTCs 2"
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter   (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Bool
Ghc.isBoxedTupleTyCon)
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a b. [a] -> [b] -> [(a, b)]
zip [a]
xs (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 = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (\a
x -> (a
x, ) 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 -> forall a. PPrint a => String -> a -> a
F.notracepp (TyCon -> String
msg TyCon
tc) forall a b. (a -> b) -> a -> b
$ 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 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (TyCon -> Maybe DataName
tcName TyCon
tc)
    defn :: HasDataDecl
defn         = Maybe SizeFun -> HasDataDecl
NoDecl forall a. Maybe a
Nothing
    tcName :: TyCon -> Maybe DataName
tcName       = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ModName -> DataName -> DataName
qualifiedDataName ModName
modName) 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  forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> DataName
tycName
    decls :: HashMap (Maybe DataName) HasDataDecl
decls        = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (forall a. a -> Maybe a
Just DataName
dn, DataDecl -> HasDataDecl
hasDecl DataDecl
d)
                                | DataDecl
d     <- 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 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 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)
  = forall a. Maybe a
Nothing
tyConDataDecl ((TyCon
tc, DataName
dn), NoDecl Maybe SizeFun
szF)
  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ DataDecl
      { tycName :: DataName
tycName   = DataName
dn
      , tycTyVars :: [Symbol]
tycTyVars = forall a. Symbolic a => a -> Symbol
F.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  = forall a. a -> Maybe a
Just (TyCon -> [DataCtor]
decls TyCon
tc)
      , tycSrcPos :: SourcePos
tycSrcPos = forall a. NamedThing a => a -> SourcePos
GM.getSourcePos TyCon
tc
      , tycSFun :: Maybe SizeFun
tycSFun   = Maybe SizeFun
szF
      , tycPropTy :: Maybe BareType
tycPropTy = forall a. Maybe a
Nothing
      , tycKind :: DataDeclKind
tycKind   = DataDeclKind
DataReflected
      }
      where decls :: TyCon -> [DataCtor]
decls = forall a b. (a -> b) -> [a] -> [b]
map DataCon -> DataCtor
dataConDecl 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  = forall a. a -> Maybe a
Just (LocSymbol -> DataName
DnName (Symbol -> Symbol
post forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. NamedThing a => a -> Located a
GM.locNamedThing TyCon
tc))
  | DataCon
d:[DataCon]
_ <- [DataCon]
dcs = forall a. a -> Maybe a
Just (LocSymbol -> DataName
DnCon  (Symbol -> Symbol
post forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. NamedThing a => a -> Located a
GM.locNamedThing DataCon
d ))
  | Bool
otherwise  = forall a. Maybe a
Nothing
  where
    post :: Symbol -> Symbol
post       = if Bool
full then forall a. a -> a
id else Symbol -> Symbol
GM.dropModuleNamesAndUnique
    vanillaTc :: Bool
vanillaTc  = TyCon -> Bool
Ghc.isVanillaAlgTyCon TyCon
tc
    dcs :: [DataCon]
dcs        = forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn 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 (forall a. Symbolic a => a -> Symbol
F.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 forall a. Maybe a
Nothing DataCon
d Int
i, forall r. Monoid r => Type -> BRType r
RT.bareOfType Type
t) | (Int
i, Type
t) <- [(Int, Type)]
its ]
    dx :: LocSymbol
dx            = forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. NamedThing a => a -> Located a
GM.locNamedThing DataCon
d
    its :: [(Int, Type)]
its           = 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          = forall a. a -> Maybe a
Just (forall r. Monoid r => Type -> BRType r
RT.bareOfType Type
ty :: BareType)
    _outT :: Maybe BareType
    _outT :: Maybe BareType
_outT
      | Bool
isGadt    = forall a. a -> Maybe a
Just (forall r. Monoid r => Type -> BRType r
RT.bareOfType Type
ty)
      | Bool
otherwise = 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)
  = forall m. Monoid m => Bool -> m -> m
Misc.condNull (forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg) (Measure SpecType DataCon
checker forall a. a -> [a] -> [a]
: forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe 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
 forall a. [a] -> [a] -> [a]
++ forall m. Monoid m => Bool -> m -> m
Misc.condNull Bool
autofields (forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe 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
      | forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RType t t1 t2
t Bool -> Bool -> Bool
&& Bool -> Bool
not (forall t. HasConfig t => t -> Bool
higherOrderFlag Config
cfg)
      = forall a. Maybe a
Nothing
      | Bool
otherwise
      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a1.
Show a1 =>
LocSymbol
-> SpecType -> DataCon -> Int -> a1 -> Measure SpecType DataCon
makeMeasureSelector (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
      | forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RType t t1 t2
t Bool -> Bool -> Bool
&& Bool -> Bool
not (forall t. HasConfig t => t -> Bool
higherOrderFlag Config
cfg)
      = forall a. Maybe a
Nothing
      | Bool
otherwise
      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a1.
Show a1 =>
LocSymbol
-> SpecType -> DataCon -> Int -> a1 -> Measure SpecType DataCon
makeMeasureSelector (forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (Maybe DataConMap -> DataCon -> Int -> Symbol
Bare.makeDataConSelector (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   = forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. [a] -> [a]
reverse [(Symbol, SpecType)]
xts) [Int
1..]
    n :: Int
n        = 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 (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    = 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 (forall a b. (a -> b) -> [a] -> [b]
map (, forall a. Monoid a => a
mempty) [RTVar RTyVar RSort]
as) [] [(Symbol, RFInfo, SpecType, RReft)
xt] SpecType
bareBool
  where
    ([RTVar RTyVar RSort]
as, [SpecType]
_, (Symbol, RFInfo, SpecType, RReft)
xt)          = {- traceShow ("dataConSel: " ++ show dc) $ -} forall r.
(Reftable (RTProp RTyCon RTyVar r), PPrint r, Reftable r) =>
Bool
-> DataCon
-> Int
-> ([RTVar RTyVar RSort], [RRType r],
    (Symbol, RFInfo, RRType r, r))
bkDataCon Bool
permitTC DataCon
dc Int
n

dataConSel Bool
permitTC DataCon
dc Int
n (Proj Int
i) = 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 (forall a b. (a -> b) -> [a] -> [b]
map (, forall a. Monoid a => a
mempty) [RTVar RTyVar RSort]
as) [] [(Symbol, RFInfo, SpecType, RReft)
xt] (forall a. Monoid a => a
mempty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
ti)
  where
    ti :: SpecType
ti                   = forall a. a -> Maybe a -> a
Mb.fromMaybe forall {a}. a
err forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> Maybe a
Misc.getNth (Int
iforall a. Num a => a -> a -> a
-Int
1) [SpecType]
ts
    ([RTVar RTyVar RSort]
as, [SpecType]
ts, (Symbol, RFInfo, SpecType, RReft)
xt)         = {- F.tracepp ("bkDatacon dc = " ++ F.showpp (dc, n)) $ -} forall r.
(Reftable (RTProp RTyCon RTyVar r), PPrint r, Reftable r) =>
Bool
-> DataCon
-> Int
-> ([RTVar RTyVar RSort], [RRType r],
    (Symbol, RFInfo, RRType r, r))
bkDataCon Bool
permitTC DataCon
dc Int
n
    err :: a
err                  = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ String
"DataCon " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show DataCon
dc forall a. [a] -> [a] -> [a]
++ String
"does not have " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i 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 RSort], [RRType r],
    (Symbol, RFInfo, RRType r, r))
bkDataCon Bool
permitTC DataCon
dcn Int
nFlds  = (forall {s}. [RTVar RTyVar s]
as, [RRType r]
ts, (Symbol
F.dummySymbol, Bool -> RFInfo
classRFInfo Bool
permitTC, RRType r
t, forall a. Monoid a => a
mempty))
  where
    ts :: [RRType r]
ts                = forall r. Monoid r => Type -> RRType r
RT.ofType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> [a] -> [a]
Misc.takeLast Int
nFlds (forall a b. (a -> b) -> [a] -> [b]
map forall a. Scaled a -> a
Ghc.irrelevantMult [Scaled Type]
_ts)
    t :: RRType r
t                 = -- Misc.traceShow ("bkDataConResult" ++ GM.showPpr (dc, _t, _t0)) $
                          forall r. Monoid r => Type -> RRType r
RT.ofType  forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type
Ghc.mkTyConApp TyCon
tc [Type]
tArgs'
    as :: [RTVar RTyVar s]
as                = forall tv s. tv -> RTVar tv s
makeRTVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCoVar -> RTyVar
RT.rTyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([TyCoVar]
αs 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'            = forall a. Int -> [a] -> [a]
take (Int
nArgs forall a. Num a => a -> a -> a
- Int
nVars) [Type]
tArgs forall a. [a] -> [a] -> [a]
++ (TyCoVar -> Type
Ghc.mkTyVarTy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyCoVar]
αs)
    nVars :: Int
nVars             = forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyCoVar]
αs
    nArgs :: Int
nArgs             = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tArgs
    (TyCon
tc, [Type]
tArgs)       = forall a. a -> Maybe a -> a
Mb.fromMaybe forall {a}. a
err (HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Ghc.splitTyConApp_maybe Type
_t)
    err :: b
err               = forall a b. NamedThing a => a -> String -> b
GM.namedPanic DataCon
dcn (String
"Cannot split result type of DataCon " forall a. [a] -> [a] -> [a]
++ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> TyCoVar
Ghc.dataConWorkId forall a b. (a -> b) -> a -> b
$ DataCon
dc)

data DataConSel = Check | Proj Int

bareBool :: SpecType
bareBool :: SpecType
bareBool = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (TyCon -> [RPVar] -> TyConInfo -> RTyCon
RTyCon TyCon
Ghc.boolTyCon [] forall a. Default a => a
def) [] [] 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 = [forall {ty}. Def ty DataCon
eqn], msKind :: MeasureKind
msKind = MeasureKind
MsSelector, msUnSorted :: UnSortedExprs
msUnSorted = forall a. Monoid a => a
mempty}
  where
    eqn :: Def ty DataCon
eqn                        = forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
x DataCon
dc forall a. Maybe a
Nothing forall {a}. [(Symbol, Maybe a)]
args (Expr -> Body
E (Symbol -> Expr
F.EVar forall a b. (a -> b) -> a -> b
$ forall {a}. Show a => a -> Symbol
mkx a1
i))
    args :: [(Symbol, Maybe a)]
args                       = (, forall a. Maybe a
Nothing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. Show a => a -> Symbol
mkx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1 .. Int
n]
    mkx :: a -> Symbol
mkx a
j                      = forall a. Symbolic a => a -> Symbol
F.symbol (String
"xx" forall a. [a] -> [a] -> [a]
++ 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 = forall {ty}. Def ty DataCon
eqn forall a. a -> [a] -> [a]
: (forall {ty}. DataCon -> Def ty DataCon
eqns forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= DataCon
dc) [DataCon]
dcs), msKind :: MeasureKind
msKind = MeasureKind
MsChecker, msUnSorted :: UnSortedExprs
msUnSorted = forall a. Monoid a => a
mempty }
  where
    s :: SpecType
s       = forall a. PPrint a => String -> a -> a
F.notracepp (String
"makeMeasureChecker: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LocSymbol
x) SpecType
s0
    eqn :: Def ty DataCon
eqn     = forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
x DataCon
dc forall a. Maybe a
Nothing ((, forall a. Maybe a
Nothing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. Show a => a -> Symbol
mkx 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  = forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
x DataCon
d  forall a. Maybe a
Nothing ((, forall a. Maybe a
Nothing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. Show a => a -> Symbol
mkx 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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length (DataCon -> [Scaled Type]
Ghc.dataConOrigArgTys DataCon
d)
    mkx :: a -> Symbol
mkx a
j   = forall a. Symbolic a => a -> Symbol
F.symbol (String
"xx" forall a. [a] -> [a] -> [a]
++ 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             = forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd forall c tv a. RType c tv a -> RType c tv (UReft a)
RT.uRType 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               = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft 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)
  = forall t.
Env -> ModName -> MSpec t LocSymbol -> Lookup (MSpec t DataCon)
mkMeasureDCon Env
env               ModName
name
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> ModName -> MSpec BareType LocSymbol -> MSpec SpecType LocSymbol
mkMeasureSort Env
env               ModName
name
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. Located a -> a
val
  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
  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 = 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        = forall a. PPrint a => String -> a -> a
F.notracepp String
"CMS" forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter forall {ctor}. Measure (Located BareType) ctor -> Bool
inScope1 forall a b. (a -> b) -> a -> b
$             forall ty bndr. Spec ty bndr -> [Measure ty ()]
Ms.cmeasures BareSpec
spec
    ms :: [Measure (Located BareType) LocSymbol]
ms         = forall a. PPrint a => String -> a -> a
F.notracepp String
"UMS" forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter Measure (Located BareType) LocSymbol -> Bool
inScope2 forall a b. (a -> b) -> a -> b
$ Measure (Located BareType) LocSymbol
-> Measure (Located BareType) LocSymbol
expMeas forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.measures  BareSpec
spec
    ims :: [Measure (Located BareType) LocSymbol]
ims        = forall a. PPrint a => String -> a -> a
F.notracepp String
"IMS" forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter Measure (Located BareType) LocSymbol -> Bool
inScope2 forall a b. (a -> b) -> a -> b
$ Measure (Located BareType) LocSymbol
-> Measure (Located BareType) LocSymbol
expMeas forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall a. Eq a => a -> a -> Bool
== ModName
myName
    inScope1 :: Measure (Located BareType) ctor -> Bool
inScope1 Measure (Located BareType) ctor
z = forall a. PPrint a => String -> a -> a
F.notracepp (String
"inScope1: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp (forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure (Located BareType) ctor
z)) (Bool
force Bool -> Bool -> 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 = forall a. PPrint a => String -> a -> a
F.notracepp (String
"inScope2: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp (forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure (Located BareType) LocSymbol
z)) (Bool
force Bool -> Bool -> Bool
|| (forall {ctor}. Measure (Located BareType) ctor -> Bool
okSort Measure (Located BareType) LocSymbol
z Bool -> Bool -> 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty ctor. Measure ty ctor -> ty
msSort
    okCtors :: Measure ty LocSymbol -> Bool
okCtors    = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Env -> ModName -> LocSymbol -> Bool
Bare.knownGhcDataCon Env
env ModName
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty ctor. Def ty ctor -> ctor
ctor) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall t. MSpec t LocSymbol -> [LocSymbol]
measureCtors MSpec t LocSymbol
m
  [DataCon]
dcs   <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> ModName -> String -> LocSymbol -> Lookup DataCon
Bare.lookupGhcDataCon Env
env ModName
name String
"measure-datacon") [LocSymbol]
ns
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t.
MSpec t LocSymbol -> [(Symbol, DataCon)] -> MSpec t DataCon
mkMeasureDCon_ MSpec t LocSymbol
m (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Located a -> a
val 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' {ctorMap :: HashMap Symbol [Def t DataCon]
Ms.ctorMap = HashMap Symbol [Def t DataCon]
cm'}
  where
    m' :: MSpec t DataCon
m'                = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Symbol -> DataCon
txforall b c a. (b -> c) -> (a -> b) -> a -> c
.forall a. Located a -> a
val) MSpec t LocSymbol
m
    cm' :: HashMap Symbol [Def t DataCon]
cm'               = forall k2 k1 v.
(Eq k2, Hashable k2) =>
(k1 -> k2) -> HashMap k1 v -> HashMap k2 v
Misc.hashMapMapKeys (forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> DataCon
tx) forall a b. (a -> b) -> a -> b
$ forall ty ctor. MSpec ty ctor -> HashMap Symbol [Def ty ctor]
Ms.ctorMap MSpec t DataCon
m'
    tx :: Symbol -> DataCon
tx                = forall k v.
(?callStack::CallStack, Eq k, Show k, Hashable k) =>
HashMap k v -> k -> v
Misc.mlookup (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 = forall a. Ord a => [a] -> [a]
Misc.sortNub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall ty ctor. Def ty ctor -> ctor
ctor forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [v]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) =
  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 (forall a b. (a -> b) -> [a] -> [b]
map forall ctor. Def BareType ctor -> Def SpecType ctor
txDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Symbol [Def BareType LocSymbol]
c) (forall ctor. Measure BareType ctor -> Measure SpecType ctor
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap LocSymbol (Measure BareType LocSymbol)
mm) (forall ctor. Measure BareType ctor -> Measure SpecType ctor
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap LocSymbol (Measure BareType ())
cm) (forall ctor. Measure BareType ctor -> Measure SpecType ctor
tx 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 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) = forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
M LocSymbol
n (SourcePos -> BareType -> SpecType
ofMeaSort SourcePos
l BareType
s) (forall ctor. Def BareType ctor -> Def SpecType ctor
txDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Def BareType ctor]
eqs) MeasureKind
k UnSortedExprs
u where l :: SourcePos
l = 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 = 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 = forall a. Loc a => a -> SourcePos
GM.fSourcePos (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 :: Located BareType
msSort = forall tv r c. (Eq tv, Monoid r) => RType c tv r -> RType c tv r
RT.generalize                   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty ctor. Measure ty ctor -> ty
msSort Measure (Located BareType) LocSymbol
m
  , msEqns :: [Def (Located BareType) LocSymbol]
msEqns = forall t.
Env -> ModName -> BareRTEnv -> Def t LocSymbol -> Def t LocSymbol
expandMeasureDef Env
env ModName
name BareRTEnv
rtEnv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns Measure (Located BareType) LocSymbol
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 :: Body
body  = forall a. PPrint a => String -> a -> a
F.notracepp String
msg forall a b. (a -> b) -> a -> b
$ forall a.
(PPrint a, Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [Symbol]
bs (forall ty ctor. Def ty ctor -> Body
body Def t LocSymbol
d) }
  where
    l :: SourcePos
l     = forall a. Located a -> SourcePos
loc (forall ty ctor. Def ty ctor -> LocSymbol
measure Def t LocSymbol
d)
    bs :: [Symbol]
bs    = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def t LocSymbol
d
    msg :: String
msg   = String
"QUALIFY-EXPAND-BODY" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp ([Symbol]
bs, 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 =
  [ (forall a. Symbolic a => a -> Symbol
F.symbol TyCoVar
v, 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)   <- forall k v. HashMap k v -> [(k, v)]
M.toList (Env -> TyThingMap
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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall r. Monoid r => Type -> RRType r
RT.ofType forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCoVar -> Type
Ghc.varType) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedThing a => a -> Located a
GM.locNamedThing

isSimpleType :: Ghc.Type -> Bool
isSimpleType :: Type -> Bool
isSimpleType = Sort -> Bool
isFirstOrder forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> Type -> Sort
RT.typeSort 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 Symbol [Def (RType c tv (UReft r2)) t]
HashMap LocSymbol (Measure (RType c tv (UReft r2)) t)
HashMap LocSymbol (Measure (RType c tv (UReft r2)) ())
imeas :: forall ty ctor. MSpec ty ctor -> [Measure ty ctor]
cmeasMap :: forall ty ctor. MSpec ty ctor -> HashMap LocSymbol (Measure ty ())
measMap :: forall ty ctor.
MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor)
imeas :: [Measure (RType c tv (UReft r2)) t]
cmeasMap :: HashMap LocSymbol (Measure (RType c tv (UReft r2)) ())
measMap :: HashMap LocSymbol (Measure (RType c tv (UReft r2)) t)
ctorMap :: HashMap Symbol [Def (RType c tv (UReft r2)) t]
ctorMap :: forall ty ctor. MSpec ty ctor -> HashMap Symbol [Def ty ctor]
..} = forall {c} {tv} {r2} {ctor}.
Measure (RType c tv (UReft r2)) ctor
-> (LocSymbol, CMeasure (RType c tv r2))
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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, forall ty. LocSymbol -> ty -> CMeasure ty
CM LocSymbol
n (forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft 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

-}