{-# 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 Language.Haskell.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 

--------------------------------------------------------------------------------
makeHaskellMeasures :: GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec
                    -> [Measure (Located BareType) LocSymbol]
--------------------------------------------------------------------------------
makeHaskellMeasures :: GhcSrc
-> TycEnv
-> LogicMap
-> BareSpec
-> [Measure (Located BareType) LocSymbol]
makeHaskellMeasures 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    = TycEnv -> LogicMap -> [CoreBind] -> LocSymbol -> SpecMeasure
makeMeasureDefinition 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 :: Bare.TycEnv -> LogicMap -> [Ghc.CoreBind] -> LocSymbol 
                      -> Measure LocSpecType Ghc.DataCon
makeMeasureDefinition :: TycEnv -> LogicMap -> [CoreBind] -> LocSymbol -> SpecMeasure
makeMeasureDefinition TycEnv
tycEnv LogicMap
lmap [CoreBind]
cbs LocSymbol
x = 
  case Symbol -> [CoreBind] -> Maybe (Var, CoreExpr)
GM.findVarDef (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) [CoreBind]
cbs of
    Maybe (Var, 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 (Var
v, CoreExpr
def) -> LocSymbol
-> Located (RRType RReft)
-> [Def (Located (RRType RReft)) DataCon]
-> MeasureKind
-> UnSortedExprs
-> SpecMeasure
forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
Ms.mkM LocSymbol
vx Located (RRType RReft)
vinfo [Def (Located (RRType RReft)) DataCon]
mdef MeasureKind
MsLifted (Type -> [Def (Located (RRType RReft)) DataCon] -> UnSortedExprs
makeUnSorted (Var -> Type
Ghc.varType Var
v) [Def (Located (RRType RReft)) DataCon]
mdef) 
                     where 
                       vx :: LocSymbol
vx           = LocSymbol -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
x (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v)
                       mdef :: [Def (Located (RRType RReft)) DataCon]
mdef         = TycEnv
-> LogicMap
-> LocSymbol
-> Var
-> CoreExpr
-> [Def (Located (RRType RReft)) DataCon]
coreToDef' TycEnv
tycEnv LogicMap
lmap LocSymbol
vx Var
v CoreExpr
def
                       vinfo :: Located (RRType RReft)
vinfo        = (Type -> RRType RReft) -> Var -> Located (RRType RReft)
forall a. (Type -> a) -> Var -> Located a
GM.varLocInfo Type -> RRType RReft
forall r. Reftable r => Type -> RRType r
logicType Var
v

makeUnSorted :: Ghc.Type -> [Def LocSpecType Ghc.DataCon] -> UnSortedExprs
makeUnSorted :: Type -> [Def (Located (RRType RReft)) DataCon] -> UnSortedExprs
makeUnSorted Type
t [Def (Located (RRType RReft)) DataCon]
defs
  | Type -> Bool
isMeasureType Type
ta 
  = UnSortedExprs
forall a. Monoid a => a
mempty
  | Bool
otherwise
  = (Def (Located (RRType RReft)) DataCon -> ([Symbol], Expr))
-> [Def (Located (RRType RReft)) DataCon] -> UnSortedExprs
forall a b. (a -> b) -> [a] -> [b]
map Def (Located (RRType RReft)) DataCon -> ([Symbol], Expr)
forall ty ctor. Def ty ctor -> ([Symbol], Expr)
defToUnSortedExpr [Def (Located (RRType RReft)) 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
t

    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
Ghc.isClassPred 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 -> ([Symbol], Expr)
defToUnSortedExpr Def ty ctor
def = (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
def), 
                             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
def) [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
def)) 

    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

coreToDef' :: Bare.TycEnv -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr 
           -> [Def LocSpecType Ghc.DataCon] 
coreToDef' :: TycEnv
-> LogicMap
-> LocSymbol
-> Var
-> CoreExpr
-> [Def (Located (RRType RReft)) DataCon]
coreToDef' TycEnv
tycEnv LogicMap
lmap LocSymbol
vx Var
v CoreExpr
def = 
  case TCEmb TyCon
-> LogicMap
-> DataConMap
-> (String -> Error)
-> LogicM [Def (Located (RRType RReft)) DataCon]
-> Either Error [Def (Located (RRType RReft)) 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) (LocSymbol
-> Var -> CoreExpr -> LogicM [Def (Located (RRType RReft)) DataCon]
forall r.
Reftable r =>
LocSymbol
-> Var -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
coreToDef LocSymbol
vx Var
v CoreExpr
def) of
    Right [Def (Located (RRType RReft)) DataCon]
l -> [Def (Located (RRType RReft)) DataCon]
l
    Left Error
e  -> Error -> [Def (Located (RRType RReft)) 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 :: GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec 
                   -> [(LocSymbol, LMap)]
--------------------------------------------------------------------------------
makeHaskellInlines :: GhcSrc
-> TCEmb TyCon -> LogicMap -> BareSpec -> [(LocSymbol, LMap)]
makeHaskellInlines GhcSrc
src TCEmb TyCon
embs LogicMap
lmap BareSpec
spec 
         = TCEmb TyCon
-> LogicMap -> [CoreBind] -> LocSymbol -> (LocSymbol, LMap)
makeMeasureInline 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 :: F.TCEmb Ghc.TyCon -> LogicMap -> [Ghc.CoreBind] -> LocSymbol
                  -> (LocSymbol, LMap)
makeMeasureInline :: TCEmb TyCon
-> LogicMap -> [CoreBind] -> LocSymbol -> (LocSymbol, LMap)
makeMeasureInline TCEmb TyCon
embs LogicMap
lmap [CoreBind]
cbs LocSymbol
x = 
  case Symbol -> [CoreBind] -> Maybe (Var, CoreExpr)
GM.findVarDef (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) [CoreBind]
cbs of 
    Maybe (Var, 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 (Var
v, CoreExpr
def) -> (LocSymbol
vx, TCEmb TyCon
-> Maybe DataConMap
-> LogicMap
-> LocSymbol
-> Var
-> CoreExpr
-> (([Var], Either Expr Expr) -> LMap)
-> LMap
forall a.
TCEmb TyCon
-> Maybe DataConMap
-> LogicMap
-> LocSymbol
-> Var
-> CoreExpr
-> (([Var], Either Expr Expr) -> a)
-> a
coreToFun' TCEmb TyCon
embs Maybe DataConMap
forall a. Maybe a
Nothing LogicMap
lmap LocSymbol
vx Var
v CoreExpr
def ([Var], 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 (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
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' :: F.TCEmb Ghc.TyCon -> Maybe Bare.DataConMap -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
           -> (([Ghc.Var], Either F.Expr F.Expr) -> a) -> a
coreToFun' :: TCEmb TyCon
-> Maybe DataConMap
-> LogicMap
-> LocSymbol
-> Var
-> CoreExpr
-> (([Var], Either Expr Expr) -> a)
-> a
coreToFun' TCEmb TyCon
embs Maybe DataConMap
dmMb LogicMap
lmap LocSymbol
x Var
v CoreExpr
def ([Var], Either Expr Expr) -> a
ok = (Error -> a)
-> (([Var], Either Expr Expr) -> a)
-> Either Error ([Var], 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 ([Var], Either Expr Expr) -> a
ok Either Error ([Var], Either Expr Expr)
act 
  where 
    act :: Either Error ([Var], Either Expr Expr)
act  = TCEmb TyCon
-> LogicMap
-> DataConMap
-> (String -> Error)
-> LogicM ([Var], Either Expr Expr)
-> Either Error ([Var], 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 ([Var], Either Expr Expr)
xFun 
    xFun :: LogicM ([Var], Either Expr Expr)
xFun = LocSymbol -> Var -> CoreExpr -> LogicM ([Var], Either Expr Expr)
coreToFun LocSymbol
x Var
v CoreExpr
def  
    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 = (((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 :: (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 :: (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
mod 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
def (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)
    def :: HasDataDecl
def          = Maybe SizeFun -> HasDataDecl
NoDecl Maybe SizeFun
forall a. Maybe a
Nothing
    tcName :: TyCon -> Maybe DataName
tcName       = (DataName -> DataName) -> Maybe DataName -> Maybe DataName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ModName -> DataName -> DataName
qualifiedDataName ModName
mod) (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
mod  (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
mod (DnName LocSymbol
lx) = LocSymbol -> DataName
DnName (ModName -> Symbol -> Symbol
qualifyModName ModName
mod (Symbol -> Symbol) -> LocSymbol -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSymbol
lx)
qualifiedDataName ModName
mod (DnCon  LocSymbol
lx) = LocSymbol -> DataName
DnCon  (ModName -> Symbol -> Symbol
qualifyModName ModName
mod (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 :: DataName
-> [Symbol]
-> [PVar BSort]
-> [DataCtor]
-> SourcePos
-> Maybe SizeFun
-> Maybe BareType
-> DataDeclKind
-> DataDecl
DataDecl
      { tycName :: DataName
tycName   = DataName
dn
      , tycTyVars :: [Symbol]
tycTyVars = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Var]
GM.tyConTyVarsDef TyCon
tc
      , tycPVars :: [PVar BSort]
tycPVars  = []
      , tycDCons :: [DataCtor]
tycDCons  = 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 (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
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
    ([Var]
as,[Type]
_ps,[Type]
ts,Type
t)  = DataCon -> ([Var], [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
t :: 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
t)
      | 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 (RRType RReft) DataCon]
makeMeasureSelectors Config
cfg DataConMap
dm (Loc SourcePos
l SourcePos
l' DataConP
c)
  = (Bool
-> [Measure (RRType RReft) DataCon]
-> [Measure (RRType RReft) DataCon]
forall m. Monoid m => Bool -> m -> m
Misc.condNull (Config -> Bool
forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg) ([Measure (RRType RReft) DataCon]
 -> [Measure (RRType RReft) DataCon])
-> [Measure (RRType RReft) DataCon]
-> [Measure (RRType RReft) DataCon]
forall a b. (a -> b) -> a -> b
$ Measure (RRType RReft) DataCon
checker Measure (RRType RReft) DataCon
-> [Measure (RRType RReft) DataCon]
-> [Measure (RRType RReft) DataCon]
forall a. a -> [a] -> [a]
: [Maybe (Measure (RRType RReft) DataCon)]
-> [Measure (RRType RReft) DataCon]
forall a. [Maybe a] -> [a]
Mb.catMaybes (((Symbol, RRType RReft), Int)
-> Maybe (Measure (RRType RReft) DataCon)
forall a t t1 t2.
((a, RType t t1 t2), Int) -> Maybe (Measure (RRType RReft) DataCon)
go' (((Symbol, RRType RReft), Int)
 -> Maybe (Measure (RRType RReft) DataCon))
-> [((Symbol, RRType RReft), Int)]
-> [Maybe (Measure (RRType RReft) DataCon)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((Symbol, RRType RReft), Int)]
fields)) --  internal measures, needed for reflection
 [Measure (RRType RReft) DataCon]
-> [Measure (RRType RReft) DataCon]
-> [Measure (RRType RReft) DataCon]
forall a. [a] -> [a] -> [a]
++ (Bool
-> [Measure (RRType RReft) DataCon]
-> [Measure (RRType RReft) DataCon]
forall m. Monoid m => Bool -> m -> m
Misc.condNull (Bool
autofields)      ([Measure (RRType RReft) DataCon]
 -> [Measure (RRType RReft) DataCon])
-> [Measure (RRType RReft) DataCon]
-> [Measure (RRType RReft) DataCon]
forall a b. (a -> b) -> a -> b
$           [Maybe (Measure (RRType RReft) DataCon)]
-> [Measure (RRType RReft) DataCon]
forall a. [Maybe a] -> [a]
Mb.catMaybes (((Symbol, RRType RReft), Int)
-> Maybe (Measure (RRType RReft) DataCon)
forall t t1 t2.
((Symbol, RType t t1 t2), Int)
-> Maybe (Measure (RRType RReft) DataCon)
go  (((Symbol, RRType RReft), Int)
 -> Maybe (Measure (RRType RReft) DataCon))
-> [((Symbol, RRType RReft), Int)]
-> [Maybe (Measure (RRType RReft) DataCon)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((Symbol, RRType RReft), Int)]
fields)) --  user-visible measures.
  where
    dc :: DataCon
dc         = DataConP -> DataCon
dcpCon    DataConP
c 
    isGadt :: Bool
isGadt     = DataConP -> Bool
dcpIsGadt DataConP
c 
    xts :: [(Symbol, RRType RReft)]
xts        = DataConP -> [(Symbol, RRType RReft)]
dcpTyArgs DataConP
c
    autofields :: Bool
autofields = Bool -> Bool
not (Bool
isGadt)
    go :: ((Symbol, RType t t1 t2), Int)
-> Maybe (Measure (RRType RReft) 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 (RRType RReft) DataCon)
forall a. Maybe a
Nothing
      | Bool
otherwise
      = Measure (RRType RReft) DataCon
-> Maybe (Measure (RRType RReft) DataCon)
forall a. a -> Maybe a
Just (Measure (RRType RReft) DataCon
 -> Maybe (Measure (RRType RReft) DataCon))
-> Measure (RRType RReft) DataCon
-> Maybe (Measure (RRType RReft) DataCon)
forall a b. (a -> b) -> a -> b
$ LocSymbol
-> RRType RReft
-> DataCon
-> Int
-> Int
-> Measure (RRType RReft) DataCon
forall a1.
Show a1 =>
LocSymbol
-> RRType RReft
-> DataCon
-> Int
-> a1
-> Measure (RRType RReft) DataCon
makeMeasureSelector (SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' Symbol
x) (Int -> RRType RReft
projT Int
i) DataCon
dc Int
n Int
i

    go' :: ((a, RType t t1 t2), Int) -> Maybe (Measure (RRType RReft) 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 (RRType RReft) DataCon)
forall a. Maybe a
Nothing
      | Bool
otherwise
      = Measure (RRType RReft) DataCon
-> Maybe (Measure (RRType RReft) DataCon)
forall a. a -> Maybe a
Just (Measure (RRType RReft) DataCon
 -> Maybe (Measure (RRType RReft) DataCon))
-> Measure (RRType RReft) DataCon
-> Maybe (Measure (RRType RReft) DataCon)
forall a b. (a -> b) -> a -> b
$ LocSymbol
-> RRType RReft
-> DataCon
-> Int
-> Int
-> Measure (RRType RReft) DataCon
forall a1.
Show a1 =>
LocSymbol
-> RRType RReft
-> DataCon
-> Int
-> a1
-> Measure (RRType RReft) 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 -> RRType RReft
projT Int
i) DataCon
dc Int
n Int
i

    fields :: [((Symbol, RRType RReft), Int)]
fields   = [(Symbol, RRType RReft)]
-> [Int] -> [((Symbol, RRType RReft), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([(Symbol, RRType RReft)] -> [(Symbol, RRType RReft)]
forall a. [a] -> [a]
reverse [(Symbol, RRType RReft)]
xts) [Int
1..]
    n :: Int
n        = [(Symbol, RRType RReft)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RRType RReft)]
xts
    checker :: Measure (RRType RReft) DataCon
checker  = LocSymbol
-> RRType RReft -> DataCon -> Int -> Measure (RRType RReft) DataCon
makeMeasureChecker (SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (DataCon -> Symbol
Bare.makeDataConChecker DataCon
dc)) RRType RReft
checkT DataCon
dc Int
n
    projT :: Int -> RRType RReft
projT Int
i  = DataCon -> Int -> DataConSel -> RRType RReft
dataConSel DataCon
dc Int
n (Int -> DataConSel
Proj Int
i)
    checkT :: RRType RReft
checkT   = DataCon -> Int -> DataConSel -> RRType RReft
dataConSel DataCon
dc Int
n DataConSel
Check

dataConSel :: Ghc.DataCon -> Int -> DataConSel -> SpecType
dataConSel :: DataCon -> Int -> DataConSel -> RRType RReft
dataConSel DataCon
dc Int
n DataConSel
Check    = [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [PVar (RType RTyCon RTyVar ())]
-> [(Symbol, RRType RReft, RReft)]
-> [(Symbol, RRType RReft, RReft)]
-> RRType RReft
-> RRType RReft
forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RType c tv r, r)]
-> [(Symbol, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow ([RTVar RTyVar (RType RTyCon RTyVar ())]
-> [RReft] -> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RTVar RTyVar (RType RTyCon RTyVar ())]
as (RReft -> [RReft]
forall a. a -> [a]
repeat RReft
forall a. Monoid a => a
mempty)) [] [] [(Symbol, RRType RReft, RReft)
xt] RRType RReft
bareBool
  where
    ([RTVar RTyVar (RType RTyCon RTyVar ())]
as, [RRType RReft]
_, (Symbol, RRType RReft, RReft)
xt)          = {- traceShow ("dataConSel: " ++ show dc) $ -} DataCon
-> Int
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [RRType RReft],
    (Symbol, RRType RReft, RReft))
forall r.
(Reftable (RTProp RTyCon RTyVar r), PPrint r, Reftable r) =>
DataCon
-> Int
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [RRType r],
    (Symbol, RRType r, r))
bkDataCon DataCon
dc Int
n

dataConSel DataCon
dc Int
n (Proj Int
i) = [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [PVar (RType RTyCon RTyVar ())]
-> [(Symbol, RRType RReft, RReft)]
-> [(Symbol, RRType RReft, RReft)]
-> RRType RReft
-> RRType RReft
forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RType c tv r, r)]
-> [(Symbol, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow ([RTVar RTyVar (RType RTyCon RTyVar ())]
-> [RReft] -> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RTVar RTyVar (RType RTyCon RTyVar ())]
as (RReft -> [RReft]
forall a. a -> [a]
repeat RReft
forall a. Monoid a => a
mempty)) [] [] [(Symbol, RRType RReft, RReft)
xt] (RReft -> RReft
forall a. Monoid a => a
mempty (RReft -> RReft) -> RRType RReft -> RRType RReft
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RRType RReft
ti)
  where
    ti :: RRType RReft
ti                   = RRType RReft -> Maybe (RRType RReft) -> RRType RReft
forall a. a -> Maybe a -> a
Mb.fromMaybe RRType RReft
forall a. a
err (Maybe (RRType RReft) -> RRType RReft)
-> Maybe (RRType RReft) -> RRType RReft
forall a b. (a -> b) -> a -> b
$ Int -> [RRType RReft] -> Maybe (RRType RReft)
forall a. Int -> [a] -> Maybe a
Misc.getNth (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [RRType RReft]
ts
    ([RTVar RTyVar (RType RTyCon RTyVar ())]
as, [RRType RReft]
ts, (Symbol, RRType RReft, RReft)
xt)         = {- F.tracepp ("bkDatacon dc = " ++ F.showpp (dc, n)) $ -} DataCon
-> Int
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [RRType RReft],
    (Symbol, RRType RReft, RReft))
forall r.
(Reftable (RTProp RTyCon RTyVar r), PPrint r, Reftable r) =>
DataCon
-> Int
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [RRType r],
    (Symbol, RRType r, r))
bkDataCon 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) => Ghc.DataCon -> Int -> ([RTVar RTyVar RSort], [RRType r], (F.Symbol, RRType r, r))
bkDataCon :: DataCon
-> Int
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [RRType r],
    (Symbol, RRType r, r))
bkDataCon DataCon
dc Int
nFlds  = ([RTVar RTyVar (RType RTyCon RTyVar ())]
forall s. [RTVar RTyVar s]
as, [RRType r]
ts, (Symbol
F.dummySymbol, 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 [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)
-> (Var -> RTyVar) -> Var -> RTVar RTyVar s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> RTyVar
RT.rTyVar (Var -> RTVar RTyVar s) -> [Var] -> [RTVar RTyVar s]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Var]
αs [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
αs')
    (([Var]
αs,[Var]
αs',[EqSpec]
_,[Type]
_,[Type]
_ts,Type
_t), Type
_t0) = DataCon -> (([Var], [Var], [EqSpec], [Type], [Type], Type), Type)
hammer DataCon
dc
    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]
++ (Var -> Type
Ghc.mkTyVarTy (Var -> Type) -> [Var] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
αs)
    nVars :: Int
nVars             = [Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
αs
    nArgs :: Int
nArgs             = [Type] -> 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 (HasDebugCallStack => 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
dc (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
dc)
    hammer :: DataCon -> (([Var], [Var], [EqSpec], [Type], [Type], Type), Type)
hammer DataCon
dc         = (DataCon -> ([Var], [Var], [EqSpec], [Type], [Type], Type)
Ghc.dataConFullSig DataCon
dc, Var -> Type
Ghc.varType (Var -> Type) -> (DataCon -> Var) -> DataCon -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Var
Ghc.dataConWorkId (DataCon -> Type) -> DataCon -> Type
forall a b. (a -> b) -> a -> b
$ DataCon
dc)

data DataConSel = Check | Proj Int

bareBool :: SpecType
bareBool :: RRType RReft
bareBool = RTyCon
-> [RRType RReft]
-> [RTProp RTyCon RTyVar RReft]
-> RReft
-> RRType RReft
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 :: LocSymbol
-> RRType RReft
-> DataCon
-> Int
-> a1
-> Measure (RRType RReft) DataCon
makeMeasureSelector LocSymbol
x RRType RReft
s DataCon
dc Int
n a1
i = M :: forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
M { msName :: LocSymbol
msName = LocSymbol
x, msSort :: RRType RReft
msSort = RRType RReft
s, msEqns :: [Def (RRType RReft) DataCon]
msEqns = [Def (RRType RReft) 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
-> RRType RReft -> DataCon -> Int -> Measure (RRType RReft) DataCon
makeMeasureChecker LocSymbol
x RRType RReft
s0 DataCon
dc Int
n = M :: forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
M { msName :: LocSymbol
msName = LocSymbol
x, msSort :: RRType RReft
msSort = RRType RReft
s, msEqns :: [Def (RRType RReft) DataCon]
msEqns = Def (RRType RReft) DataCon
forall ty. Def ty DataCon
eqn Def (RRType RReft) DataCon
-> [Def (RRType RReft) DataCon] -> [Def (RRType RReft) DataCon]
forall a. a -> [a] -> [a]
: (DataCon -> Def (RRType RReft) DataCon
forall ty. DataCon -> Def ty DataCon
eqns (DataCon -> Def (RRType RReft) DataCon)
-> [DataCon] -> [Def (RRType RReft) 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 :: RRType RReft
s       = String -> RRType RReft -> RRType RReft
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) RRType RReft
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 = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DataCon -> [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' :: MSpec SpecType Ghc.DataCon -> ([(Ghc.Var, SpecType)], [(LocSymbol, RRType F.Reft)])
----------------------------------------------------------------------------------------------
makeMeasureSpec' :: MSpec (RRType RReft) DataCon
-> ([(Var, RRType RReft)], [(LocSymbol, RRType Reft)])
makeMeasureSpec' MSpec (RRType RReft) DataCon
mspec0 = ([(Var, RRType RReft)]
ctorTys, [(LocSymbol, RRType Reft)]
measTys) 
  where 
    ctorTys :: [(Var, RRType RReft)]
ctorTys             = (RRType Reft -> RRType RReft)
-> (Var, RRType Reft) -> (Var, RRType RReft)
forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd RRType Reft -> RRType RReft
forall c tv a. RType c tv a -> RType c tv (UReft a)
RT.uRType ((Var, RRType Reft) -> (Var, RRType RReft))
-> [(Var, RRType Reft)] -> [(Var, RRType RReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, RRType Reft)]
ctorTys0
    ([(Var, RRType Reft)]
ctorTys0, [(LocSymbol, RRType Reft)]
measTys) = MSpec (RRType Reft) DataCon
-> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)])
Ms.dataConTypes MSpec (RRType Reft) DataCon
mspec 
    mspec :: MSpec (RRType Reft) DataCon
mspec               = (RRType RReft -> RRType Reft)
-> MSpec (RRType RReft) DataCon -> MSpec (RRType Reft) DataCon
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((RReft -> Reft) -> RRType RReft -> 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 (RRType RReft) DataCon
mspec0

----------------------------------------------------------------------------------------------
makeMeasureSpec :: Bare.Env -> Bare.SigEnv -> ModName -> (ModName, Ms.BareSpec) -> Ms.MSpec SpecType Ghc.DataCon
----------------------------------------------------------------------------------------------
makeMeasureSpec :: Env
-> SigEnv
-> ModName
-> (ModName, BareSpec)
-> MSpec (RRType RReft) DataCon
makeMeasureSpec Env
env SigEnv
sigEnv ModName
myName (ModName
name, BareSpec
spec) 
  = Env
-> ModName
-> MSpec (RRType RReft) LocSymbol
-> MSpec (RRType RReft) DataCon
forall t. Env -> ModName -> MSpec t LocSymbol -> MSpec t DataCon
mkMeasureDCon Env
env               ModName
name 
  (MSpec (RRType RReft) LocSymbol -> MSpec (RRType RReft) DataCon)
-> (BareSpec -> MSpec (RRType RReft) LocSymbol)
-> BareSpec
-> MSpec (RRType RReft) DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> ModName
-> MSpec BareType LocSymbol
-> MSpec (RRType RReft) LocSymbol
mkMeasureSort Env
env               ModName
name 
  (MSpec BareType LocSymbol -> MSpec (RRType RReft) LocSymbol)
-> (BareSpec -> MSpec BareType LocSymbol)
-> BareSpec
-> MSpec (RRType RReft) LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located BareType -> BareType)
-> MSpec (Located BareType) LocSymbol -> MSpec BareType LocSymbol
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 -> MSpec (RRType RReft) DataCon)
-> BareSpec -> MSpec (RRType RReft) 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 -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (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 -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (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 -> Ms.MSpec t Ghc.DataCon
mkMeasureDCon :: Env -> ModName -> MSpec t LocSymbol -> MSpec t DataCon
mkMeasureDCon Env
env ModName
name MSpec t LocSymbol
m = MSpec t LocSymbol -> [(Symbol, DataCon)] -> MSpec t DataCon
forall t.
MSpec t LocSymbol -> [(Symbol, DataCon)] -> MSpec t DataCon
mkMeasureDCon_ MSpec t LocSymbol
m [ (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
n, LocSymbol -> DataCon
symDC LocSymbol
n) | LocSymbol
n <- MSpec t LocSymbol -> [LocSymbol]
forall t. MSpec t LocSymbol -> [LocSymbol]
measureCtors MSpec t LocSymbol
m ]
  where 
    symDC :: LocSymbol -> DataCon
symDC                = Env -> ModName -> String -> LocSymbol -> DataCon
Bare.lookupGhcDataCon Env
env ModName
name String
"measure-datacon"

mkMeasureDCon_ :: Ms.MSpec t LocSymbol -> [(F.Symbol, Ghc.DataCon)] -> Ms.MSpec t Ghc.DataCon
mkMeasureDCon_ :: 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'                = (LocSymbol -> DataCon) -> MSpec t LocSymbol -> MSpec t DataCon
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 :: 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 (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 (RRType RReft) 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 (RRType RReft) LocSymbol]
-> HashMap LocSymbol (Measure (RRType RReft) LocSymbol)
-> HashMap LocSymbol (Measure (RRType RReft) ())
-> [Measure (RRType RReft) LocSymbol]
-> MSpec (RRType RReft) 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 (RRType RReft) LocSymbol)
-> [Def BareType LocSymbol] -> [Def (RRType RReft) LocSymbol]
forall a b. (a -> b) -> [a] -> [b]
map Def BareType LocSymbol -> Def (RRType RReft) LocSymbol
forall ctor. Def BareType ctor -> Def (RRType RReft) ctor
txDef ([Def BareType LocSymbol] -> [Def (RRType RReft) LocSymbol])
-> HashMap Symbol [Def BareType LocSymbol]
-> HashMap Symbol [Def (RRType RReft) LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Symbol [Def BareType LocSymbol]
c) (Measure BareType LocSymbol -> Measure (RRType RReft) LocSymbol
forall ctor. Measure BareType ctor -> Measure (RRType RReft) ctor
tx (Measure BareType LocSymbol -> Measure (RRType RReft) LocSymbol)
-> HashMap LocSymbol (Measure BareType LocSymbol)
-> HashMap LocSymbol (Measure (RRType RReft) LocSymbol)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap LocSymbol (Measure BareType LocSymbol)
mm) (Measure BareType () -> Measure (RRType RReft) ()
forall ctor. Measure BareType ctor -> Measure (RRType RReft) ctor
tx (Measure BareType () -> Measure (RRType RReft) ())
-> HashMap LocSymbol (Measure BareType ())
-> HashMap LocSymbol (Measure (RRType RReft) ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap LocSymbol (Measure BareType ())
cm) (Measure BareType LocSymbol -> Measure (RRType RReft) LocSymbol
forall ctor. Measure BareType ctor -> Measure (RRType RReft) ctor
tx (Measure BareType LocSymbol -> Measure (RRType RReft) LocSymbol)
-> [Measure BareType LocSymbol]
-> [Measure (RRType RReft) 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 -> RRType RReft
ofMeaSort SourcePos
l = Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> RRType RReft
Bare.ofBareType Env
env ModName
name SourcePos
l Maybe [PVar BSort]
forall a. Maybe a
Nothing 

      tx :: Measure BareType ctor -> (Measure SpecType ctor)
      tx :: Measure BareType ctor -> Measure (RRType RReft) ctor
tx (M LocSymbol
n BareType
s [Def BareType ctor]
eqs MeasureKind
k UnSortedExprs
u) = LocSymbol
-> RRType RReft
-> [Def (RRType RReft) ctor]
-> MeasureKind
-> UnSortedExprs
-> Measure (RRType RReft) ctor
forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
M LocSymbol
n (SourcePos -> BareType -> RRType RReft
ofMeaSort SourcePos
l BareType
s) (Def BareType ctor -> Def (RRType RReft) ctor
forall ctor. Def BareType ctor -> Def (RRType RReft) ctor
txDef (Def BareType ctor -> Def (RRType RReft) ctor)
-> [Def BareType ctor] -> [Def (RRType RReft) 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 :: Def BareType ctor -> Def (RRType RReft) ctor
txDef Def BareType ctor
d = (BareType -> RRType RReft)
-> Def BareType ctor -> Def (RRType RReft) ctor
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SourcePos -> BareType -> RRType RReft
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 :: Located BareType
msSort = BareType -> BareType
forall tv r c. (Eq tv, Monoid r) => RType c tv r -> RType c tv r
RT.generalize                   (BareType -> BareType) -> Located BareType -> Located BareType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Measure (Located BareType) LocSymbol -> Located BareType
forall ty ctor. Measure ty ctor -> ty
msSort Measure (Located BareType) LocSymbol
m
  , msEqns :: [Def (Located BareType) LocSymbol]
msEqns = Env
-> ModName
-> BareRTEnv
-> Def (Located BareType) LocSymbol
-> Def (Located BareType) LocSymbol
forall t.
Env -> ModName -> BareRTEnv -> Def t LocSymbol -> Def t LocSymbol
expandMeasureDef Env
env ModName
name BareRTEnv
rtEnv (Def (Located BareType) LocSymbol
 -> Def (Located BareType) LocSymbol)
-> [Def (Located BareType) LocSymbol]
-> [Def (Located BareType) LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Measure (Located BareType) LocSymbol
-> [Def (Located BareType) LocSymbol]
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 :: 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  = String -> Body -> Body
forall a. PPrint a => String -> a -> a
F.notracepp String
msg (Body -> Body) -> Body -> Body
forall a b. (a -> b) -> a -> b
$ Env
-> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> Body -> Body
forall a.
(Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [Symbol]
bs (Def t LocSymbol -> Body
forall ty ctor. Def ty ctor -> Body
body Def t LocSymbol
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 :: Env -> [(Symbol, Located (RRType r))]
varMeasures Env
env = 
  [ (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v, Var -> Located (RRType r)
forall r. Monoid r => Var -> Located (RRType r)
varSpecType Var
v) 
      | Var
v <- Env -> [Var]
knownVars Env
env 
      , Var -> Bool
GM.isDataConId Var
v
      , Type -> Bool
isSimpleType (Var -> Type
Ghc.varType Var
v) ]

knownVars :: Bare.Env -> [Ghc.Var]
knownVars :: Env -> [Var]
knownVars Env
env = [ Var
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 Var
v) <- [(Symbol, TyThing)]
xThings 
                ]

varSpecType :: (Monoid r) => Ghc.Var -> Located (RRType r)
varSpecType :: Var -> Located (RRType r)
varSpecType = (Var -> RRType r) -> Located Var -> Located (RRType r)
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) -> (Var -> Type) -> Var -> RRType r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type
Ghc.varType) (Located Var -> Located (RRType r))
-> (Var -> Located Var) -> Var -> Located (RRType r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Located Var
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 :: 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]
..}) = 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 (splitForAllTys $ 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

-}