{-# 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'
  , makeOpaqueReflMeasures
  , getReflDCs
  , varMeasures
  , getMeasVars
  , makeClassMeasureSpec
  -- , makeHaskellBounds
  , varLocSym
  ) where

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           Language.Haskell.Liquid.Types.DataDecl
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import qualified Language.Haskell.Liquid.Types.RefType as RT
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.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           Language.Haskell.Liquid.UX.Config
import Control.Monad (mapM)
import qualified Data.List as L

--------------------------------------------------------------------------------
makeHaskellMeasures :: Config -> GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec
                    -> [Measure (Located BareType) (Located LHName)]
--------------------------------------------------------------------------------
makeHaskellMeasures :: Config
-> GhcSrc
-> TycEnv
-> LogicMap
-> BareSpec
-> [Measure (Located BareType) (Located LHName)]
makeHaskellMeasures Config
cfg GhcSrc
src TycEnv
tycEnv LogicMap
lmap BareSpec
spec
          = SpecMeasure -> Measure (Located BareType) (Located LHName)
Bare.measureToBare (SpecMeasure -> Measure (Located BareType) (Located LHName))
-> [SpecMeasure] -> [Measure (Located BareType) (Located LHName)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecMeasure]
ms
  where
    ms :: [SpecMeasure]
ms    = Config
-> TycEnv
-> LogicMap
-> [(Var, CoreExpr)]
-> Located LHName
-> SpecMeasure
makeMeasureDefinition Config
cfg TycEnv
tycEnv LogicMap
lmap [(Var, CoreExpr)]
cbs (Located LHName -> SpecMeasure)
-> [Located LHName] -> [SpecMeasure]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located LHName]
mSyms
    cbs :: [(Var, CoreExpr)]
cbs   = [Bind Var] -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
Ghc.flattenBinds (GhcSrc -> [Bind Var]
_giCbs GhcSrc
src)
    mSyms :: [Located LHName]
mSyms = HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
S.toList (BareSpec -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.hmeas BareSpec
spec)

makeMeasureDefinition
  :: Config -> Bare.TycEnv -> LogicMap -> [(Ghc.Id, Ghc.CoreExpr)] -> Located LHName
  -> Measure LocSpecType Ghc.DataCon
makeMeasureDefinition :: Config
-> TycEnv
-> LogicMap
-> [(Var, CoreExpr)]
-> Located LHName
-> SpecMeasure
makeMeasureDefinition Config
cfg TycEnv
tycEnv LogicMap
lmap [(Var, CoreExpr)]
cbs Located LHName
x =
  case ((Var, CoreExpr) -> Bool)
-> [(Var, CoreExpr)] -> Maybe (Var, CoreExpr)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find ((Located LHName
x Located LHName -> Located LHName -> Bool
forall a. Eq a => a -> a -> Bool
==) (Located LHName -> Bool)
-> ((Var, CoreExpr) -> Located LHName) -> (Var, CoreExpr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Located LHName
makeGHCLHNameLocatedFromId (Var -> Located LHName)
-> ((Var, CoreExpr) -> Var) -> (Var, CoreExpr) -> Located LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, CoreExpr) -> Var
forall a b. (a, b) -> a
fst) [(Var, CoreExpr)]
cbs of
    Maybe (Var, CoreExpr)
Nothing ->
      Error -> SpecMeasure
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (Error -> SpecMeasure) -> Error -> SpecMeasure
forall a b. (a -> b) -> a -> b
$
        Located LHName -> String -> Error
errHMeas Located LHName
x String
"Cannot extract measure from haskell function"
    Just (Var
v, CoreExpr
cexp) -> Located LHName
-> LocSpecType
-> [DefV Symbol LocSpecType DataCon]
-> MeasureKind
-> UnSortedExprs
-> SpecMeasure
forall ty v bndr.
HasCallStack =>
Located LHName
-> ty
-> [DefV v ty bndr]
-> MeasureKind
-> UnSortedExprs
-> MeasureV v ty bndr
Ms.mkM Located LHName
vx LocSpecType
vinfo [DefV Symbol LocSpecType DataCon]
mdef MeasureKind
MsLifted (Bool -> Type -> [DefV Symbol LocSpecType DataCon] -> UnSortedExprs
makeUnSorted Bool
allowTC (Var -> Type
Ghc.varType Var
v) [DefV Symbol LocSpecType DataCon]
mdef)
                     where
                       vx :: Located LHName
vx           = HasCallStack => Module -> LHName -> LHName
Module -> LHName -> LHName
reflectLHName (HasDebugCallStack => Name -> Module
Name -> Module
Ghc.nameModule (Name -> Module) -> Name -> Module
forall a b. (a -> b) -> a -> b
$ Var -> Name
forall a. NamedThing a => a -> Name
Ghc.getName Var
v) (LHName -> LHName) -> Located LHName -> Located LHName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located LHName
x
                       mdef :: [DefV Symbol LocSpecType DataCon]
mdef         = Config
-> TycEnv
-> LogicMap
-> Located LHName
-> Var
-> CoreExpr
-> [DefV Symbol LocSpecType DataCon]
coreToDef' Config
cfg TycEnv
tycEnv LogicMap
lmap Located LHName
vx Var
v CoreExpr
cexp
                       vinfo :: LocSpecType
vinfo        = (Type -> SpecType) -> Var -> LocSpecType
forall a. (Type -> a) -> Var -> Located a
GM.varLocInfo (Bool -> Type -> SpecType
forall r. Reftable r => Bool -> Type -> RRType r
logicType Bool
allowTC) Var
v

    where allowTC :: Bool
allowTC = Config -> Bool
typeclass Config
cfg

makeUnSorted :: Bool -> Ghc.Type -> [Def LocSpecType Ghc.DataCon] -> UnSortedExprs
makeUnSorted :: Bool -> Type -> [DefV Symbol LocSpecType DataCon] -> UnSortedExprs
makeUnSorted Bool
allowTC Type
ty [DefV Symbol LocSpecType DataCon]
defs
  | Type -> Bool
isMeasureType Type
ta
  = UnSortedExprs
forall a. Monoid a => a
mempty
  | Bool
otherwise
  = (DefV Symbol LocSpecType DataCon -> UnSortedExpr)
-> [DefV Symbol LocSpecType DataCon] -> UnSortedExprs
forall a b. (a -> b) -> [a] -> [b]
map DefV Symbol LocSpecType DataCon -> UnSortedExpr
forall {ty} {ctor}. DefV Symbol ty ctor -> UnSortedExpr
defToUnSortedExpr [DefV Symbol LocSpecType DataCon]
defs
  where
    ta :: Type
ta = Type -> Type
go (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms Type
ty

    go :: Type -> Type
go (Ghc.ForAllTy ForAllTyBinder
_ Type
t) = Type -> Type
go Type
t
    go Ghc.FunTy{ ft_arg :: Type -> Type
Ghc.ft_arg = Type
p, ft_res :: Type -> Type
Ghc.ft_res = Type
t} | Type -> Bool
isErasable Type
p = Type -> Type
go Type
t
    go Ghc.FunTy{ ft_arg :: Type -> Type
Ghc.ft_arg = Type
t } = Type
t
    go Type
t                  = Type
t -- this should never happen!

    isMeasureType :: Type -> Bool
isMeasureType (Ghc.TyConApp TyCon
_ [Type]
ts) = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
Ghc.isTyVarTy [Type]
ts
    isMeasureType Type
_                   = Bool
False

    defToUnSortedExpr :: DefV Symbol ty ctor -> UnSortedExpr
defToUnSortedExpr DefV Symbol ty ctor
defn =
      (Symbol
xxSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:((Symbol, Maybe ty) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Maybe ty) -> Symbol) -> [(Symbol, Maybe ty)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DefV Symbol ty ctor -> [(Symbol, Maybe ty)]
forall v ty ctor. DefV v ty ctor -> [(Symbol, Maybe ty)]
binds DefV Symbol ty ctor
defn),
       Expr -> Body -> Expr
Ms.bodyPred (Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
F.eApps (Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol) -> LHName -> Symbol
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
F.val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ DefV Symbol ty ctor -> Located LHName
forall v ty ctor. DefV v ty ctor -> Located LHName
measure DefV Symbol ty ctor
defn) [Symbol -> Expr
forall a. Expression a => a -> Expr
F.expr Symbol
xx]) (DefV Symbol ty ctor -> Body
forall v ty ctor. DefV v ty ctor -> BodyV v
body DefV Symbol ty ctor
defn))

    xx :: Symbol
xx = Maybe Integer -> Symbol
F.vv (Maybe Integer -> Symbol) -> Maybe Integer -> Symbol
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
10000
    isErasable :: Type -> Bool
isErasable = if Bool
allowTC then Type -> Bool
GM.isEmbeddedDictType else Type -> Bool
Ghc.isClassPred

coreToDef' :: Config -> Bare.TycEnv -> LogicMap -> Located LHName -> Ghc.Var -> Ghc.CoreExpr
           -> [Def LocSpecType Ghc.DataCon]
coreToDef' :: Config
-> TycEnv
-> LogicMap
-> Located LHName
-> Var
-> CoreExpr
-> [DefV Symbol LocSpecType DataCon]
coreToDef' Config
cfg TycEnv
tycEnv LogicMap
lmap Located LHName
vx Var
v CoreExpr
defn =
  case TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> (String -> Error)
-> LogicM [DefV Symbol LocSpecType DataCon]
-> Either Error [DefV Symbol LocSpecType DataCon]
forall t.
TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> (String -> Error)
-> LogicM t
-> Either Error t
runToLogic TCEmb TyCon
embs LogicMap
lmap DataConMap
dm Config
cfg (Located LHName -> String -> Error
errHMeas Located LHName
vx) (Located LHName
-> Var -> CoreExpr -> LogicM [DefV Symbol LocSpecType DataCon]
forall r.
Reftable r =>
Located LHName
-> Var -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
coreToDef Located LHName
vx Var
v CoreExpr
defn) of
    Right [DefV Symbol LocSpecType DataCon]
l -> [DefV Symbol LocSpecType DataCon]
l
    Left Error
e  -> Error -> [DefV Symbol LocSpecType DataCon]
forall a e. (HasCallStack, 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 :: Located LHName -> String -> Error
errHMeas :: Located LHName -> String -> Error
errHMeas Located LHName
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
$ Located LHName -> SourcePos
forall a. Located a -> SourcePos
loc Located LHName
x) (LHName -> Doc
forall a. PPrint a => a -> Doc
pprint (LHName -> Doc) -> LHName -> Doc
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val Located LHName
x) (String -> Doc
text String
str)

--------------------------------------------------------------------------------
makeHaskellInlines :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec
                   -> [(LocSymbol, LMap)]
--------------------------------------------------------------------------------
makeHaskellInlines :: Config
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> BareSpec
-> [(LocSymbol, LMap)]
makeHaskellInlines Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap BareSpec
spec
         = Config
-> TCEmb TyCon
-> LogicMap
-> [(Var, CoreExpr)]
-> Located LHName
-> (LocSymbol, LMap)
makeMeasureInline Config
cfg TCEmb TyCon
embs LogicMap
lmap [(Var, CoreExpr)]
cbs (Located LHName -> (LocSymbol, LMap))
-> [Located LHName] -> [(LocSymbol, LMap)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located LHName]
inls
  where
    cbs :: [(Var, CoreExpr)]
cbs  = [Bind Var] -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
Ghc.flattenBinds (GhcSrc -> [Bind Var]
_giCbs GhcSrc
src)
    inls :: [Located LHName]
inls = HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
S.toList        (BareSpec -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.inlines BareSpec
spec)

makeMeasureInline
  :: Config -> F.TCEmb Ghc.TyCon -> LogicMap -> [(Ghc.Id, Ghc.CoreExpr)] -> Located LHName
  -> (LocSymbol, LMap)
makeMeasureInline :: Config
-> TCEmb TyCon
-> LogicMap
-> [(Var, CoreExpr)]
-> Located LHName
-> (LocSymbol, LMap)
makeMeasureInline Config
cfg TCEmb TyCon
embs LogicMap
lmap [(Var, CoreExpr)]
cbs Located LHName
x =
  case ((Var, CoreExpr) -> Bool)
-> [(Var, CoreExpr)] -> Maybe (Var, CoreExpr)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find ((Located LHName -> LHName
forall a. Located a -> a
val Located LHName
x LHName -> LHName -> Bool
forall a. Eq a => a -> a -> Bool
==) (LHName -> Bool)
-> ((Var, CoreExpr) -> LHName) -> (Var, CoreExpr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> LHName
makeGHCLHNameFromId (Var -> LHName)
-> ((Var, CoreExpr) -> Var) -> (Var, CoreExpr) -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, CoreExpr) -> Var
forall a b. (a, b) -> a
fst) [(Var, CoreExpr)]
cbs of
    Maybe (Var, CoreExpr)
Nothing        -> Error -> (LocSymbol, LMap)
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (Error -> (LocSymbol, LMap)) -> Error -> (LocSymbol, LMap)
forall a b. (a -> b) -> a -> b
$ Located LHName -> String -> Error
errHMeas Located LHName
x String
"Cannot inline haskell function"
    Just (Var
v, CoreExpr
defn) -> (LocSymbol
vx, Config
-> TCEmb TyCon
-> Maybe DataConMap
-> LogicMap
-> LocSymbol
-> Var
-> CoreExpr
-> (([Var], Either Expr Expr) -> LMap)
-> LMap
forall a.
Config
-> TCEmb TyCon
-> Maybe DataConMap
-> LogicMap
-> LocSymbol
-> Var
-> CoreExpr
-> (([Var], Either Expr Expr) -> a)
-> a
coreToFun' Config
cfg TCEmb TyCon
embs Maybe DataConMap
forall a. Maybe a
Nothing LogicMap
lmap LocSymbol
vx Var
v CoreExpr
defn ([Var], Either Expr Expr) -> LMap
forall {a} {v}.
Symbolic a =>
([a], Either (ExprV v) (ExprV v)) -> LMapV v
ok)
                     where
                       vx :: LocSymbol
vx         = Located LHName -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
F.atLoc Located LHName
x (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v)
                       ok :: ([a], Either (ExprV v) (ExprV v)) -> LMapV v
ok ([a]
xs, Either (ExprV v) (ExprV v)
e) = LocSymbol -> [Symbol] -> ExprV v -> LMapV v
forall v. LocSymbol -> [Symbol] -> ExprV v -> LMapV v
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) ((ExprV v -> ExprV v)
-> (ExprV v -> ExprV v) -> Either (ExprV v) (ExprV v) -> ExprV v
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ExprV v -> ExprV v
forall a. a -> a
id ExprV v -> ExprV v
forall a. a -> a
id Either (ExprV v) (ExprV v)
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' :: Config -> 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.
Config
-> TCEmb TyCon
-> Maybe DataConMap
-> LogicMap
-> LocSymbol
-> Var
-> CoreExpr
-> (([Var], Either Expr Expr) -> a)
-> a
coreToFun' Config
cfg TCEmb TyCon
embs Maybe DataConMap
dmMb LogicMap
lmap LocSymbol
x Var
v CoreExpr
defn ([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. (HasCallStack, 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
-> Config
-> (String -> Error)
-> LogicM ([Var], Either Expr Expr)
-> Either Error ([Var], Either Expr Expr)
forall t.
TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> (String -> Error)
-> LogicM t
-> Either Error t
runToLogic TCEmb TyCon
embs LogicMap
lmap DataConMap
dm Config
cfg String -> Error
forall {t}. String -> TError t
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
defn
    err :: String -> TError t
err  String
str = SrcSpan -> Doc -> Doc -> TError t
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)
    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


-------------------------------------------------------------------------------
makeHaskellDataDecls :: Config -> Ms.BareSpec -> [Ghc.TyCon]
                     -> [DataDecl]
--------------------------------------------------------------------------------
makeHaskellDataDecls :: Config -> BareSpec -> [TyCon] -> [DataDecl]
makeHaskellDataDecls Config
cfg BareSpec
spec [TyCon]
tcs
  | Config -> Bool
forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg = BareSpec -> [DataDecl] -> [DataDecl]
Bare.dataDeclSize BareSpec
spec
                    ([DataDecl] -> [DataDecl])
-> ([TyCon] -> [DataDecl]) -> [TyCon] -> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((TyCon, DataName), HasDataDecl) -> Maybe DataDecl)
-> [((TyCon, DataName), HasDataDecl)] -> [DataDecl]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe ((TyCon, DataName), HasDataDecl) -> Maybe DataDecl
tyConDataDecl
                    -- . F.tracepp "makeHaskellDataDecls-3"
                    ([((TyCon, DataName), HasDataDecl)] -> [DataDecl])
-> ([TyCon] -> [((TyCon, DataName), HasDataDecl)])
-> [TyCon]
-> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TyCon, DataName) -> HasDataDecl)
-> [(TyCon, DataName)] -> [((TyCon, DataName), HasDataDecl)]
forall a b. (a -> b) -> [a] -> [(a, b)]
zipMap   (BareSpec -> TyCon -> HasDataDecl
hasDataDecl 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 TyCon -> Maybe DataName
tyConDataName
  ([TyCon] -> [(TyCon, DataName)])
-> ([TyCon] -> [TyCon]) -> [TyCon] -> [(TyCon, DataName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [TyCon] -> [TyCon]
forall a. PPrint a => String -> a -> a
F.notracepp String
"LiftableTCs 2"
  ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon -> Bool) -> [TyCon] -> [TyCon]
forall a. (a -> Bool) -> [a] -> [a]
filter   (Bool -> Bool
not (Bool -> Bool) -> (TyCon -> Bool) -> TyCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Bool
Ghc.isBoxedTupleTyCon)
  ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [TyCon] -> [TyCon]
forall a. PPrint a => String -> a -> a
F.notracepp String
"LiftableTCs 1"
  -- . (`sortDiff` wiredInTyCons)
  -- . F.tracepp "LiftableTCs 0"

zipMap :: (a -> b) -> [a] -> [(a, b)]
zipMap :: forall a b. (a -> b) -> [a] -> [(a, b)]
zipMap a -> b
f [a]
xs = [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
xs ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f [a]
xs)

zipMapMaybe :: (a -> Maybe b) -> [a] -> [(a, b)]
zipMapMaybe :: forall a b. (a -> Maybe b) -> [a] -> [(a, b)]
zipMapMaybe a -> Maybe b
f = (a -> Maybe (a, b)) -> [a] -> [(a, b)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (\a
x -> (a
x, ) (b -> (a, b)) -> Maybe b -> Maybe (a, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
x)

hasDataDecl :: Ms.BareSpec -> Ghc.TyCon -> HasDataDecl
hasDataDecl :: BareSpec -> TyCon -> HasDataDecl
hasDataDecl BareSpec
spec
                 = \TyCon
tc -> String -> HasDataDecl -> HasDataDecl
forall a. PPrint a => String -> a -> a
F.notracepp (TyCon -> String
msg TyCon
tc) (HasDataDecl -> HasDataDecl) -> HasDataDecl -> HasDataDecl
forall a b. (a -> b) -> a -> b
$ HasDataDecl
-> Maybe DataName
-> HashMap (Maybe DataName) HasDataDecl
-> HasDataDecl
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault HasDataDecl
defn (TyCon -> Maybe DataName
tyConDataName 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
tyConDataName TyCon
tc)
    defn :: HasDataDecl
defn         = Maybe SizeFun -> HasDataDecl
NoDecl Maybe SizeFun
forall a. Maybe a
Nothing
    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 lname ty. Spec lname ty -> [DataDeclP lname ty]
Ms.dataDecls BareSpec
spec
                                , let dn :: DataName
dn = DataDecl -> DataName
forall v ty. DataDeclP v ty -> DataName
tycName DataDecl
d]

{-tyConDataDecl :: {tc:TyCon | isAlgTyCon tc} -> Maybe DataDecl @-}
tyConDataDecl :: ((Ghc.TyCon, DataName), HasDataDecl) -> Maybe DataDecl
tyConDataDecl :: ((TyCon, DataName), HasDataDecl) -> Maybe DataDecl
tyConDataDecl ((TyCon, DataName)
_, HasDataDecl
HasDecl)
  = Maybe DataDecl
forall a. Maybe a
Nothing
tyConDataDecl ((TyCon
tc, DataName
dn), NoDecl Maybe SizeFun
szF)
  = DataDecl -> Maybe DataDecl
forall a. a -> Maybe a
Just (DataDecl -> Maybe DataDecl) -> DataDecl -> Maybe DataDecl
forall a b. (a -> b) -> a -> b
$ DataDecl
      { tycName :: DataName
tycName   = DataName
dn
      , tycTyVars :: [Symbol]
tycTyVars = 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 :: [PVarV Symbol (BSortV Symbol)]
tycPVars  = []
      , tycDCons :: Maybe [DataCtorP BareType]
tycDCons  = [DataCtorP BareType] -> Maybe [DataCtorP BareType]
forall a. a -> Maybe a
Just (TyCon -> [DataCtorP BareType]
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 -> [DataCtorP BareType]
decls = (DataCon -> DataCtorP BareType)
-> [DataCon] -> [DataCtorP BareType]
forall a b. (a -> b) -> [a] -> [b]
map DataCon -> DataCtorP BareType
dataConDecl ([DataCon] -> [DataCtorP BareType])
-> (TyCon -> [DataCon]) -> TyCon -> [DataCtorP BareType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> [DataCon]
Ghc.tyConDataCons

tyConDataName :: Ghc.TyCon -> Maybe DataName
tyConDataName :: TyCon -> Maybe DataName
tyConDataName TyCon
tc
  | Bool
vanillaTc  = DataName -> Maybe DataName
forall a. a -> Maybe a
Just (DataName -> Maybe DataName) -> DataName -> Maybe DataName
forall a b. (a -> b) -> a -> b
$ Located LHName -> DataName
DnName (Located LHName -> DataName) -> Located LHName -> DataName
forall a b. (a -> b) -> a -> b
$ TyCon -> Located LHName
forall a. (NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocated TyCon
tc
  | DataCon
d:[DataCon]
_ <- [DataCon]
dcs = DataName -> Maybe DataName
forall a. a -> Maybe a
Just (DataName -> Maybe DataName) -> DataName -> Maybe DataName
forall a b. (a -> b) -> a -> b
$ Located LHName -> DataName
DnCon (Located LHName -> DataName) -> Located LHName -> DataName
forall a b. (a -> b) -> a -> b
$ DataCon -> Located LHName
forall a. (NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocated DataCon
d
  | Bool
otherwise  = Maybe DataName
forall a. Maybe a
Nothing
  where
    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 -> DataCtorP BareType
dataConDecl DataCon
d     = {- F.notracepp msg $ -} Located LHName
-> [Symbol]
-> [BareType]
-> [(LHName, BareType)]
-> Maybe BareType
-> DataCtorP BareType
forall ty.
Located LHName
-> [Symbol] -> [ty] -> [(LHName, ty)] -> Maybe ty -> DataCtorP ty
DataCtor Located LHName
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) [] [(LHName, 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 :: [(LHName, BareType)]
xts           = [(Symbol -> LHName
makeGeneratedLogicLHName (Symbol -> LHName) -> Symbol -> LHName
forall a b. (a -> b) -> a -> b
$ 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 :: Located LHName
dx            = DataCon -> Located LHName
forall a. (NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocated 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
ty)  = 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
ty :: BareType)
    _outT :: Maybe BareType
    _outT :: Maybe BareType
_outT
      | Bool
isGadt    = BareType -> Maybe BareType
forall a. a -> Maybe a
Just (Type -> BareType
forall r. Monoid r => Type -> BRType r
RT.bareOfType Type
ty)
      | Bool
otherwise = Maybe BareType
forall a. Maybe a
Nothing





--------------------------------------------------------------------------------
-- | 'makeMeasureSelectors' converts the 'DataCon's and creates the measures for
--   the selectors and checkers that then enable reflection.
--------------------------------------------------------------------------------

makeMeasureSelectors :: Config -> Bare.DataConMap -> Located DataConP -> [Measure SpecType Ghc.DataCon]
makeMeasureSelectors :: Config
-> DataConMap -> Located DataConP -> [Measure SpecType DataCon]
makeMeasureSelectors Config
cfg DataConMap
dm (Loc SourcePos
l SourcePos
l' DataConP
c)
  = Bool -> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall m. Monoid m => Bool -> m -> m
Misc.condNull (Config -> Bool
forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg) (Measure SpecType DataCon
checker Measure SpecType DataCon
-> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall a. a -> [a] -> [a]
: (((LHName, SpecType), Int) -> Maybe (Measure SpecType DataCon))
-> [((LHName, SpecType), Int)] -> [Measure SpecType DataCon]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe ((LHName, SpecType), Int) -> Maybe (Measure SpecType DataCon)
forall {a} {t} {t1} {t2}.
((a, RType t t1 t2), Int) -> Maybe (Measure SpecType DataCon)
go' [((LHName, SpecType), Int)]
fields) --  internal measures, needed for reflection
 [Measure SpecType DataCon]
-> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall a. [a] -> [a] -> [a]
++ Bool -> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall m. Monoid m => Bool -> m -> m
Misc.condNull Bool
autofields ((((LHName, SpecType), Int) -> Maybe (Measure SpecType DataCon))
-> [((LHName, SpecType), Int)] -> [Measure SpecType DataCon]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe ((LHName, SpecType), Int) -> Maybe (Measure SpecType DataCon)
forall {t} {t1} {t2}.
((LHName, RType t t1 t2), Int) -> Maybe (Measure SpecType DataCon)
go [((LHName, SpecType), Int)]
fields) --  user-visible measures.
  where
    dc :: DataCon
dc         = DataConP -> DataCon
dcpCon    DataConP
c
    isGadt :: Bool
isGadt     = DataConP -> Bool
dcpIsGadt DataConP
c
    xts :: [(LHName, SpecType)]
xts        = DataConP -> [(LHName, SpecType)]
dcpTyArgs DataConP
c
    autofields :: Bool
autofields = Bool -> Bool
not Bool
isGadt
    go :: ((LHName, RType t t1 t2), Int) -> Maybe (Measure SpecType DataCon)
go ((LHName
x, RType t t1 t2
t), Int
i)
      -- do not make selectors for functional fields
      | RType t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RType t t1 t2
t Bool -> Bool -> Bool
&& Bool -> Bool
not (Config -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag Config
cfg)
      = Maybe (Measure SpecType DataCon)
forall a. Maybe a
Nothing
      | Bool
otherwise
        -- TODO: Use as origin module the module where the measure is created
      = Measure SpecType DataCon -> Maybe (Measure SpecType DataCon)
forall a. a -> Maybe a
Just (Measure SpecType DataCon -> Maybe (Measure SpecType DataCon))
-> Measure SpecType DataCon -> Maybe (Measure SpecType DataCon)
forall a b. (a -> b) -> a -> b
$ Located LHName
-> SpecType -> DataCon -> Int -> Int -> Measure SpecType DataCon
forall a1.
Show a1 =>
Located LHName
-> SpecType -> DataCon -> Int -> a1 -> Measure SpecType DataCon
makeMeasureSelector (SourcePos -> SourcePos -> LHName -> Located LHName
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' LHName
x) (Int -> SpecType
projT Int
i) DataCon
dc Int
n Int
i

    go' :: ((a, RType t t1 t2), Int) -> Maybe (Measure SpecType DataCon)
go' ((a
_,RType t t1 t2
t), Int
i)
      -- do not make selectors for functional fields
      | RType t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RType t t1 t2
t Bool -> Bool -> Bool
&& Bool -> Bool
not (Config -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag Config
cfg)
      = Maybe (Measure SpecType DataCon)
forall a. Maybe a
Nothing
      | Bool
otherwise
      = Measure SpecType DataCon -> Maybe (Measure SpecType DataCon)
forall a. a -> Maybe a
Just (Measure SpecType DataCon -> Maybe (Measure SpecType DataCon))
-> Measure SpecType DataCon -> Maybe (Measure SpecType DataCon)
forall a b. (a -> b) -> a -> b
$ Located LHName
-> SpecType -> DataCon -> Int -> Int -> Measure SpecType DataCon
forall a1.
Show a1 =>
Located LHName
-> SpecType -> DataCon -> Int -> a1 -> Measure SpecType DataCon
makeMeasureSelector (SourcePos -> SourcePos -> LHName -> Located LHName
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (Symbol -> LHName
makeGeneratedLogicLHName (Symbol -> LHName) -> Symbol -> LHName
forall a b. (a -> b) -> a -> b
$ Maybe DataConMap -> DataCon -> Int -> Symbol
Bare.makeDataConSelector (DataConMap -> Maybe DataConMap
forall a. a -> Maybe a
Just DataConMap
dm) DataCon
dc Int
i)) (Int -> SpecType
projT Int
i) DataCon
dc Int
n Int
i

    fields :: [((LHName, SpecType), Int)]
fields   = [(LHName, SpecType)] -> [Int] -> [((LHName, SpecType), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([(LHName, SpecType)] -> [(LHName, SpecType)]
forall a. [a] -> [a]
reverse [(LHName, SpecType)]
xts) [Int
1..]
    n :: Int
n        = [(LHName, SpecType)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(LHName, SpecType)]
xts
    checker :: Measure SpecType DataCon
checker  = Located LHName
-> SpecType -> DataCon -> Int -> Measure SpecType DataCon
makeMeasureChecker (SourcePos -> SourcePos -> LHName -> Located LHName
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (Symbol -> LHName
makeGeneratedLogicLHName (Symbol -> LHName) -> Symbol -> LHName
forall a b. (a -> b) -> a -> b
$ DataCon -> Symbol
Bare.makeDataConChecker DataCon
dc)) SpecType
checkT DataCon
dc Int
n
    projT :: Int -> SpecType
projT Int
i  = Bool -> DataCon -> Int -> DataConSel -> SpecType
dataConSel Bool
permitTC DataCon
dc Int
n (Int -> DataConSel
Proj Int
i)
    checkT :: SpecType
checkT   = Bool -> DataCon -> Int -> DataConSel -> SpecType
dataConSel Bool
permitTC DataCon
dc Int
n DataConSel
Check
    permitTC :: Bool
permitTC = Config -> Bool
typeclass Config
cfg

dataConSel :: Bool -> Ghc.DataCon -> Int -> DataConSel -> SpecType
dataConSel :: Bool -> DataCon -> Int -> DataConSel -> SpecType
dataConSel Bool
permitTC DataCon
dc Int
n DataConSel
Check    = [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ()), RReftV Symbol)]
-> [PVarV Symbol (RTypeV Symbol RTyCon RTyVar ())]
-> [(Symbol, RFInfo, SpecType, RReftV Symbol)]
-> SpecType
-> SpecType
forall tv v c r.
[(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [(Symbol, RFInfo, RTypeV v c tv r, r)]
-> RTypeV v c tv r
-> RTypeV v c tv r
mkArrow ((RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())
 -> (RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ()), RReftV Symbol))
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())]
-> [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ()), RReftV Symbol)]
forall a b. (a -> b) -> [a] -> [b]
map (, RReftV Symbol
forall a. Monoid a => a
mempty) [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())]
as) [] [(Symbol, RFInfo, SpecType, RReftV Symbol)
xt] SpecType
bareBool
  where
    ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())]
as, [SpecType]
_, (Symbol, RFInfo, SpecType, RReftV Symbol)
xt)          = {- traceShow ("dataConSel: " ++ show dc) $ -} Bool
-> DataCon
-> Int
-> ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())], [SpecType],
    (Symbol, RFInfo, SpecType, RReftV Symbol))
forall r.
(Reftable (RTProp RTyCon RTyVar r), PPrint r, Reftable r) =>
Bool
-> DataCon
-> Int
-> ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())], [RRType r],
    (Symbol, RFInfo, RRType r, r))
bkDataCon Bool
permitTC DataCon
dc Int
n

dataConSel Bool
permitTC DataCon
dc Int
n (Proj Int
i) = [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ()), RReftV Symbol)]
-> [PVarV Symbol (RTypeV Symbol RTyCon RTyVar ())]
-> [(Symbol, RFInfo, SpecType, RReftV Symbol)]
-> SpecType
-> SpecType
forall tv v c r.
[(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [(Symbol, RFInfo, RTypeV v c tv r, r)]
-> RTypeV v c tv r
-> RTypeV v c tv r
mkArrow ((RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())
 -> (RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ()), RReftV Symbol))
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())]
-> [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ()), RReftV Symbol)]
forall a b. (a -> b) -> [a] -> [b]
map (, RReftV Symbol
forall a. Monoid a => a
mempty) [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())]
as) [] [(Symbol, RFInfo, SpecType, RReftV Symbol)
xt] (RReftV Symbol -> RReftV Symbol
forall a. Monoid a => a
mempty (RReftV Symbol -> RReftV Symbol) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
ti)
  where
    ti :: SpecType
ti                   = SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
Mb.fromMaybe SpecType
forall {a}. a
err (Maybe SpecType -> SpecType) -> Maybe SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ Int -> [SpecType] -> Maybe SpecType
forall a. Int -> [a] -> Maybe a
Misc.getNth (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [SpecType]
ts
    ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())]
as, [SpecType]
ts, (Symbol, RFInfo, SpecType, RReftV Symbol)
xt)         = {- F.tracepp ("bkDatacon dc = " ++ F.showpp (dc, n)) $ -} Bool
-> DataCon
-> Int
-> ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())], [SpecType],
    (Symbol, RFInfo, SpecType, RReftV Symbol))
forall r.
(Reftable (RTProp RTyCon RTyVar r), PPrint r, Reftable r) =>
Bool
-> DataCon
-> Int
-> ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())], [RRType r],
    (Symbol, RFInfo, RRType r, r))
bkDataCon Bool
permitTC DataCon
dc Int
n
    err :: a
err                  = Maybe SrcSpan -> String -> a
forall a. HasCallStack => 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 :: (Reftable (RTProp RTyCon RTyVar r), PPrint r, 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 (RTypeV Symbol RTyCon RTyVar ())], [RRType r],
    (Symbol, RFInfo, RRType r, r))
bkDataCon Bool
permitTC DataCon
dcn Int
nFlds  = ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar ())]
forall {s}. [RTVar RTyVar s]
as, [RRType r]
ts, (Symbol
F.dummySymbol, Bool -> RFInfo
classRFInfo Bool
permitTC, RRType r
t, r
forall a. Monoid a => a
mempty))
  where
    ts :: [RRType r]
ts                = Type -> RRType r
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> RRType r) -> [Type] -> [RRType r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
Misc.takeLast Int
nFlds ((Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
Ghc.irrelevantMult [Scaled Type]
_ts)
    t :: RRType r
t                 = -- Misc.traceShow ("bkDataConResult" ++ GM.showPpr (dc, _t, _t0)) $
                          Type -> RRType r
forall r. Monoid r => Type -> RRType r
RT.ofType  (Type -> RRType r) -> Type -> RRType r
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type
Ghc.mkTyConApp TyCon
tc [Type]
tArgs'
    as :: [RTVar RTyVar s]
as                = RTyVar -> RTVar RTyVar s
forall tv s. tv -> RTVar tv s
makeRTVar (RTyVar -> RTVar RTyVar s)
-> (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]
_,[Scaled Type]
_ts,Type
_t), Type
_t0) = DataCon
-> (([Var], [Var], [EqSpec], [Type], [Scaled Type], Type), Type)
hammer DataCon
dcn
    tArgs' :: [Type]
tArgs'            = Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
take (Int
nArgs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nVars) [Type]
tArgs [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ (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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
αs
    nArgs :: Int
nArgs             = [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tArgs
    (TyCon
tc, [Type]
tArgs)       = (TyCon, [Type]) -> Maybe (TyCon, [Type]) -> (TyCon, [Type])
forall a. a -> Maybe a -> a
Mb.fromMaybe (TyCon, [Type])
forall {a}. a
err (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
dcn (String
"Cannot split result type of DataCon " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DataCon -> String
forall a. Show a => a -> String
show DataCon
dcn)
    hammer :: DataCon
-> (([Var], [Var], [EqSpec], [Type], [Scaled Type], Type), Type)
hammer DataCon
dc         = (DataCon -> ([Var], [Var], [EqSpec], [Type], [Scaled 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 :: SpecType
bareBool = RTyCon
-> [SpecType]
-> [RTProp RTyCon RTyVar (RReftV Symbol)]
-> RReftV Symbol
-> SpecType
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp (TyCon
-> [PVarV Symbol (RTypeV Symbol RTyCon RTyVar ())]
-> TyConInfo
-> RTyCon
RTyCon TyCon
Ghc.boolTyCon [] TyConInfo
defaultTyConInfo) [] [] RReftV Symbol
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) => Located LHName -> SpecType -> Ghc.DataCon -> Int -> a1 -> Measure SpecType Ghc.DataCon
makeMeasureSelector :: forall a1.
Show a1 =>
Located LHName
-> SpecType -> DataCon -> Int -> a1 -> Measure SpecType DataCon
makeMeasureSelector Located LHName
x SpecType
s DataCon
dc Int
n a1
i = M { msName :: Located LHName
msName = Located LHName
x, msSort :: SpecType
msSort = SpecType
s, msEqns :: [DefV Symbol SpecType DataCon]
msEqns = [DefV Symbol SpecType DataCon
forall {ty}. DefV Symbol ty DataCon
eqn], msKind :: MeasureKind
msKind = MeasureKind
MsSelector, msUnSorted :: UnSortedExprs
msUnSorted = UnSortedExprs
forall a. Monoid a => a
mempty}
  where
    eqn :: DefV Symbol ty DataCon
eqn                        = Located LHName
-> DataCon
-> Maybe ty
-> [(Symbol, Maybe ty)]
-> Body
-> DefV Symbol ty DataCon
forall v ty ctor.
Located LHName
-> ctor
-> Maybe ty
-> [(Symbol, Maybe ty)]
-> BodyV v
-> DefV v ty ctor
Def Located LHName
x DataCon
dc Maybe ty
forall a. Maybe a
Nothing [(Symbol, Maybe ty)]
forall {a}. [(Symbol, Maybe a)]
args (Expr -> Body
forall v. ExprV v -> BodyV v
E (Symbol -> Expr
forall v. v -> ExprV v
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 :: Located LHName -> SpecType -> Ghc.DataCon -> Int -> Measure SpecType Ghc.DataCon
makeMeasureChecker :: Located LHName
-> SpecType -> DataCon -> Int -> Measure SpecType DataCon
makeMeasureChecker Located LHName
x SpecType
s0 DataCon
dc Int
n = M { msName :: Located LHName
msName = Located LHName
x, msSort :: SpecType
msSort = SpecType
s, msEqns :: [DefV Symbol SpecType DataCon]
msEqns = DefV Symbol SpecType DataCon
forall {v} {ty}. DefV v ty DataCon
eqn DefV Symbol SpecType DataCon
-> [DefV Symbol SpecType DataCon] -> [DefV Symbol SpecType DataCon]
forall a. a -> [a] -> [a]
: (DataCon -> DefV Symbol SpecType DataCon
forall {v} {ty}. DataCon -> DefV v ty DataCon
eqns (DataCon -> DefV Symbol SpecType DataCon)
-> [DataCon] -> [DefV Symbol SpecType DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DataCon -> Bool) -> [DataCon] -> [DataCon]
forall a. (a -> Bool) -> [a] -> [a]
filter (DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
/= DataCon
dc) [DataCon]
dcs), msKind :: MeasureKind
msKind = MeasureKind
MsChecker, msUnSorted :: UnSortedExprs
msUnSorted = UnSortedExprs
forall a. Monoid a => a
mempty }
  where
    s :: SpecType
s       = String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp (String
"makeMeasureChecker: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Located LHName -> String
forall a. Show a => a -> String
show Located LHName
x) SpecType
s0
    eqn :: DefV v ty DataCon
eqn     = Located LHName
-> DataCon
-> Maybe ty
-> [(Symbol, Maybe ty)]
-> BodyV v
-> DefV v ty DataCon
forall v ty ctor.
Located LHName
-> ctor
-> Maybe ty
-> [(Symbol, Maybe ty)]
-> BodyV v
-> DefV v ty ctor
Def Located LHName
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])       (ExprV v -> BodyV v
forall v. ExprV v -> BodyV v
P ExprV v
forall v. ExprV v
F.PTrue)
    eqns :: DataCon -> DefV v ty DataCon
eqns DataCon
d  = Located LHName
-> DataCon
-> Maybe ty
-> [(Symbol, Maybe ty)]
-> BodyV v
-> DefV v ty DataCon
forall v ty ctor.
Located LHName
-> ctor
-> Maybe ty
-> [(Symbol, Maybe ty)]
-> BodyV v
-> DefV v ty ctor
Def Located LHName
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]) (ExprV v -> BodyV v
forall v. ExprV v -> BodyV v
P ExprV v
forall v. ExprV v
F.PFalse)
    nArgs :: DataCon -> Int
nArgs DataCon
d = [Scaled Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DataCon -> [Scaled Type]
Ghc.dataConOrigArgTys DataCon
d)
    mkx :: a -> Symbol
mkx a
j   = String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String
"xx" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
j)
    dcs :: [DataCon]
dcs     = TyCon -> [DataCon]
Ghc.tyConDataCons (DataCon -> TyCon
Ghc.dataConTyCon DataCon
dc)


----------------------------------------------------------------------------------------------
makeMeasureSpec' :: Bool -> MSpec SpecType Ghc.DataCon -> ([(Ghc.Var, SpecType)], [(Located LHName, RRType F.Reft)])
----------------------------------------------------------------------------------------------
makeMeasureSpec' :: Bool
-> MSpec SpecType DataCon
-> ([(Var, SpecType)], [(Located LHName, RRType Reft)])
makeMeasureSpec' Bool
allowTC MSpec SpecType DataCon
mspec0 = ([(Var, SpecType)]
ctorTys, [(Located LHName, RRType Reft)]
measTys)
  where
    ctorTys :: [(Var, SpecType)]
ctorTys             = (RRType Reft -> SpecType) -> (Var, RRType Reft) -> (Var, SpecType)
forall a b. (a -> b) -> (Var, a) -> (Var, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RRType Reft -> SpecType
forall c tv a. RType c tv a -> RType c tv (UReft a)
RT.uRType ((Var, RRType Reft) -> (Var, SpecType))
-> [(Var, RRType Reft)] -> [(Var, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, RRType Reft)]
ctorTys0
    ([(Var, RRType Reft)]
ctorTys0, [(Located LHName, RRType Reft)]
measTys) = Bool
-> MSpec (RRType Reft) DataCon
-> ([(Var, RRType Reft)], [(Located LHName, RRType Reft)])
Ms.dataConTypes Bool
allowTC MSpec (RRType Reft) DataCon
mspec
    mspec :: MSpec (RRType Reft) DataCon
mspec               = (SpecType -> RRType Reft)
-> MSpec SpecType DataCon -> MSpec (RRType Reft) DataCon
forall a b c. (a -> b) -> MSpec a c -> MSpec b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((RReftV Symbol -> Reft) -> SpecType -> RRType Reft
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft RReftV Symbol -> Reft
forall v r. UReftV v r -> r
ur_reft) MSpec SpecType DataCon
mspec0

----------------------------------------------------------------------------------------------
makeMeasureSpec :: Bare.Env -> Bare.SigEnv -> ModName -> (ModName, Ms.BareSpec) ->
                   Bare.Lookup (Ms.MSpec SpecType Ghc.DataCon)
----------------------------------------------------------------------------------------------
makeMeasureSpec :: Env
-> SigEnv
-> ModName
-> (ModName, BareSpec)
-> Lookup (MSpec SpecType DataCon)
makeMeasureSpec Env
env SigEnv
sigEnv ModName
myName (ModName
name, BareSpec
spec)
  = Env
-> MSpec SpecType (Located LHName)
-> Lookup (MSpec SpecType DataCon)
forall t.
Env -> MSpec t (Located LHName) -> Lookup (MSpec t DataCon)
mkMeasureDCon Env
env
  (MSpec SpecType (Located LHName)
 -> Lookup (MSpec SpecType DataCon))
-> (BareSpec -> MSpec SpecType (Located LHName))
-> BareSpec
-> Lookup (MSpec SpecType DataCon)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> MSpec BareType (Located LHName)
-> MSpec SpecType (Located LHName)
mkMeasureSort Env
env
  (MSpec BareType (Located LHName)
 -> MSpec SpecType (Located LHName))
-> (BareSpec -> MSpec BareType (Located LHName))
-> BareSpec
-> MSpec SpecType (Located LHName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located BareType -> BareType)
-> MSpec (Located BareType) (Located LHName)
-> MSpec BareType (Located LHName)
forall a b c. (a -> b) -> MSpec a c -> MSpec b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Located BareType -> BareType
forall a. Located a -> a
val
  (MSpec (Located BareType) (Located LHName)
 -> MSpec BareType (Located LHName))
-> (BareSpec -> MSpec (Located BareType) (Located LHName))
-> BareSpec
-> MSpec BareType (Located LHName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv
-> ModName
-> ModName
-> BareSpec
-> MSpec (Located BareType) (Located LHName)
bareMSpec     Env
env SigEnv
sigEnv ModName
myName ModName
name
  (BareSpec -> Lookup (MSpec SpecType DataCon))
-> BareSpec -> Lookup (MSpec SpecType DataCon)
forall a b. (a -> b) -> a -> b
$ BareSpec
spec

--- Returns all the reflected symbols.
--- If Env is provided, the symbols are qualified using the environment.
getLocReflects :: Bare.ModSpecs -> S.HashSet F.Symbol
getLocReflects :: ModSpecs -> HashSet Symbol
getLocReflects = [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet Symbol] -> HashSet Symbol)
-> (ModSpecs -> [HashSet Symbol]) -> ModSpecs -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BareSpec -> HashSet Symbol) -> [BareSpec] -> [HashSet Symbol]
forall a b. (a -> b) -> [a] -> [b]
map BareSpec -> HashSet Symbol
forall {lname} {ty}. Spec lname ty -> HashSet Symbol
names ([BareSpec] -> [HashSet Symbol])
-> (ModSpecs -> [BareSpec]) -> ModSpecs -> [HashSet Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModSpecs -> [BareSpec]
forall k v. HashMap k v -> [v]
M.elems
  where
    names :: Spec lname ty -> HashSet Symbol
names Spec lname ty
modSpec = Spec lname ty -> HashSet Symbol
forall {lname} {ty}. Spec lname ty -> HashSet Symbol
unqualified Spec lname ty
modSpec
    unqualified :: Spec lname ty -> HashSet Symbol
unqualified Spec lname ty
modSpec = [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
S.unions
      [ (Located LHName -> Symbol)
-> HashSet (Located LHName) -> HashSet Symbol
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol)
-> (Located LHName -> LHName) -> Located LHName -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
val) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.reflects Spec lname ty
modSpec)
      , (LocSymbol -> Symbol) -> HashSet LocSymbol -> HashSet Symbol
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map LocSymbol -> Symbol
forall a. Located a -> a
val (HashSet LocSymbol -> HashSet Symbol)
-> HashSet LocSymbol -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ Spec lname ty -> HashSet LocSymbol
forall lname ty. Spec lname ty -> HashSet LocSymbol
Ms.privateReflects Spec lname ty
modSpec
      , [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol)
-> ((Located LHName, Located LHName) -> LHName)
-> (Located LHName, Located LHName)
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> ((Located LHName, Located LHName) -> Located LHName)
-> (Located LHName, Located LHName)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located LHName, Located LHName) -> Located LHName
forall a b. (a, b) -> b
snd ((Located LHName, Located LHName) -> Symbol)
-> [(Located LHName, Located LHName)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec lname ty -> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
Ms.asmReflectSigs Spec lname ty
modSpec)
      , [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol)
-> ((Located LHName, Located LHName) -> LHName)
-> (Located LHName, Located LHName)
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> ((Located LHName, Located LHName) -> Located LHName)
-> (Located LHName, Located LHName)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located LHName, Located LHName) -> Located LHName
forall a b. (a, b) -> a
fst ((Located LHName, Located LHName) -> Symbol)
-> [(Located LHName, Located LHName)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec lname ty -> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
Ms.asmReflectSigs Spec lname ty
modSpec)
      , (Located LHName -> Symbol)
-> HashSet (Located LHName) -> HashSet Symbol
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol)
-> (Located LHName -> LHName) -> Located LHName -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
val) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.inlines Spec lname ty
modSpec)
      , (Located LHName -> Symbol)
-> HashSet (Located LHName) -> HashSet Symbol
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol)
-> (Located LHName -> LHName) -> Located LHName -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
val) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.hmeas Spec lname ty
modSpec)
      ]

-- Get all the symbols that are defined in the logic, based on the environment and the specs.
getDefinedSymbolsInLogic :: Bare.Env -> Bare.MeasEnv -> Bare.ModSpecs -> S.HashSet F.Symbol
getDefinedSymbolsInLogic :: Env -> MeasEnv -> ModSpecs -> HashSet Symbol
getDefinedSymbolsInLogic Env
env MeasEnv
measEnv ModSpecs
specs =
  [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ((ModName -> BareSpec -> HashSet Symbol)
-> (ModName, BareSpec) -> HashSet Symbol
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ModName -> BareSpec -> HashSet Symbol
forall {p} {v} {ty}. p -> Spec v ty -> HashSet Symbol
getFromAxioms ((ModName, BareSpec) -> HashSet Symbol)
-> [(ModName, BareSpec)] -> [HashSet Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, BareSpec)]
specsList) -- reflections that ended up in equations
    HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
`S.union` ModSpecs -> HashSet Symbol
getLocReflects ModSpecs
specs -- reflected symbols
    HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
`S.union` HashSet Symbol
measVars -- Get the data constructors, ex. for Lit00.0
    HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
`S.union` [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
S.unions (BareSpec -> HashSet Symbol
forall {lname} {ty}. Spec lname ty -> HashSet Symbol
getDataDecls (BareSpec -> HashSet Symbol)
-> ((ModName, BareSpec) -> BareSpec)
-> (ModName, BareSpec)
-> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, BareSpec) -> BareSpec
forall a b. (a, b) -> b
snd ((ModName, BareSpec) -> HashSet Symbol)
-> [(ModName, BareSpec)] -> [HashSet Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, BareSpec)]
specsList) -- get the Predicated type defs, ex. for T1669.CSemigroup
    HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
`S.union` [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
S.unions (BareSpec -> HashSet Symbol
forall {lname} {ty}. Spec lname ty -> HashSet Symbol
getAliases (BareSpec -> HashSet Symbol)
-> ((ModName, BareSpec) -> BareSpec)
-> (ModName, BareSpec)
-> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, BareSpec) -> BareSpec
forall a b. (a, b) -> b
snd ((ModName, BareSpec) -> HashSet Symbol)
-> [(ModName, BareSpec)] -> [HashSet Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, BareSpec)]
specsList) -- aliases, ex. for T1738Lib.incr
  where
    specsList :: [(ModName, BareSpec)]
specsList = ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
specs
    getFromAxioms :: p -> Spec v ty -> HashSet Symbol
getFromAxioms p
_modName Spec v ty
spec = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$
      EquationV v -> Symbol
forall v. EquationV v -> Symbol
F.eqName (EquationV v -> Symbol) -> [EquationV v] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec v ty -> [EquationV v]
forall lname ty. Spec lname ty -> [EquationV lname]
Ms.axeqs Spec v ty
spec
    measVars :: HashSet Symbol
measVars     = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ (Symbol, Located (RRType Reft)) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Located (RRType Reft)) -> Symbol)
-> [(Symbol, Located (RRType Reft))] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> MeasEnv -> [(Symbol, Located (RRType Reft))]
getMeasVars Env
env MeasEnv
measEnv
    getDataDecls :: Spec v b -> HashSet Symbol
getDataDecls Spec v b
spec = [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet Symbol] -> HashSet Symbol)
-> [HashSet Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$
      DataCtorP b -> HashSet Symbol
forall {b}. DataCtorP b -> HashSet Symbol
getFromDataCtor (DataCtorP b -> HashSet Symbol)
-> [DataCtorP b] -> [HashSet Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        [[DataCtorP b]] -> [DataCtorP b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (DataDeclP v b -> Maybe [DataCtorP b]
forall v ty. DataDeclP v ty -> Maybe [DataCtorP ty]
tycDCons (DataDeclP v b -> Maybe [DataCtorP b])
-> [DataDeclP v b] -> [[DataCtorP b]]
forall a b. (a -> Maybe b) -> [a] -> [b]
`Mb.mapMaybe` (Spec v b -> [DataDeclP v b]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
dataDecls Spec v b
spec [DataDeclP v b] -> [DataDeclP v b] -> [DataDeclP v b]
forall a. [a] -> [a] -> [a]
++ Spec v b -> [DataDeclP v b]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
newtyDecls Spec v b
spec))
    getFromDataCtor :: DataCtorP b -> HashSet Symbol
getFromDataCtor DataCtorP b
decl = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$
      (LHName -> Symbol) -> [LHName] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map LHName -> Symbol
lhNameToResolvedSymbol ([LHName] -> [Symbol]) -> [LHName] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val (DataCtorP b -> Located LHName
forall ty. DataCtorP ty -> Located LHName
dcName DataCtorP b
decl) LHName -> [LHName] -> [LHName]
forall a. a -> [a] -> [a]
: ((LHName, b) -> LHName
forall a b. (a, b) -> a
fst ((LHName, b) -> LHName) -> [(LHName, b)] -> [LHName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtorP b -> [(LHName, b)]
forall ty. DataCtorP ty -> [(LHName, ty)]
dcFields DataCtorP b
decl)
    getAliases :: Spec lname ty -> HashSet Symbol
getAliases Spec lname ty
spec = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol (ExprV lname) -> Symbol
forall x a. RTAlias x a -> Symbol
rtName (RTAlias Symbol (ExprV lname) -> Symbol)
-> (Located (RTAlias Symbol (ExprV lname))
    -> RTAlias Symbol (ExprV lname))
-> Located (RTAlias Symbol (ExprV lname))
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RTAlias Symbol (ExprV lname))
-> RTAlias Symbol (ExprV lname)
forall a. Located a -> a
val (Located (RTAlias Symbol (ExprV lname)) -> Symbol)
-> [Located (RTAlias Symbol (ExprV lname))] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
Ms.ealiases Spec lname ty
spec

-- Get the set of `DataCon`s (DCs) needed for the reflection of a given list of variables,
-- and which are not already present in the logic
getReflDCs :: Bare.MeasEnv -> [Ghc.Var] -> S.HashSet Ghc.DataCon
getReflDCs :: MeasEnv -> [Var] -> HashSet DataCon
getReflDCs MeasEnv
measEnv [Var]
vars = HashSet DataCon
dcsUndefinedInLogic
  where
    -- List of wired DCs that cannot be found in the measure environment as they are
    -- eliminated in the translation from core.
    -- Written as a list of symbols because that's easier than trying to get the corresponding DCs from GHC.
    wired :: HashSet Symbol
wired = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String -> Symbol) -> [String] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String
"GHC.Types.True", String
"GHC.Types.False", String
"GHC.Types.I#"]
    notWired :: a -> Bool
notWired a
dc = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Name -> Symbol
GM.qualifiedNameSymbol (a -> Name
forall a. NamedThing a => a -> Name
Ghc.getName a
dc) Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
wired
    -- Undefined ones are those that are not already defined in the measure environement and are not wired
    dcsUndefinedInLogic :: HashSet DataCon
dcsUndefinedInLogic = (DataCon -> Bool) -> HashSet DataCon -> HashSet DataCon
forall a. (a -> Bool) -> HashSet a -> HashSet a
S.filter DataCon -> Bool
forall {a}. NamedThing a => a -> Bool
notWired (HashSet DataCon -> HashSet DataCon)
-> HashSet DataCon -> HashSet DataCon
forall a b. (a -> b) -> a -> b
$ HashSet DataCon
allDCInUnfoldings HashSet DataCon -> HashSet DataCon -> HashSet DataCon
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` HashSet DataCon
definedDCs
    -- Get the defined DataCons from the measure environement
    definedDCs :: HashSet DataCon
definedDCs = [DataCon] -> HashSet DataCon
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([DataCon] -> HashSet DataCon) -> [DataCon] -> HashSet DataCon
forall a b. (a -> b) -> a -> b
$ (Var -> Maybe DataCon
GM.idDataConM (Var -> Maybe DataCon)
-> ((Var, LocSpecType) -> Var)
-> (Var, LocSpecType)
-> Maybe DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst) ((Var, LocSpecType) -> Maybe DataCon)
-> [(Var, LocSpecType)] -> [DataCon]
forall a b. (a -> Maybe b) -> [a] -> [b]
`Mb.mapMaybe` MeasEnv -> [(Var, LocSpecType)]
Bare.meDataCons MeasEnv
measEnv
    allDCInUnfoldings :: HashSet DataCon
allDCInUnfoldings = [Var] -> HashSet DataCon
getDCsOfUnfoldingOfVars [Var]
vars

----------------------------------------------------
-- Looks at the given list of equations and finds any undefined symbol in the logic,
-- for which we need to introduce an opaque reflection.
-- Returns the corresponding measures. Second part of the returned tuple is the information to save
-- to the `meOpaqueRefl` field of the measure environment.
makeOpaqueReflMeasures :: Bare.Env -> Bare.MeasEnv -> Bare.ModSpecs ->
              [(Ghc.Var, LocSpecType, F.Equation)] ->
              ([MSpec SpecType Ghc.DataCon], [(Ghc.Var, Measure LocBareType ctor)])
makeOpaqueReflMeasures :: forall ctor.
Env
-> MeasEnv
-> ModSpecs
-> [(Var, LocSpecType, Equation)]
-> ([MSpec SpecType DataCon],
    [(Var, Measure (Located BareType) ctor)])
makeOpaqueReflMeasures Env
env MeasEnv
measEnv ModSpecs
specs [(Var, LocSpecType, Equation)]
eqs =
  [(MSpec SpecType DataCon, (Var, Measure (Located BareType) ctor))]
-> ([MSpec SpecType DataCon],
    [(Var, Measure (Located BareType) ctor)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(MSpec SpecType DataCon, (Var, Measure (Located BareType) ctor))]
 -> ([MSpec SpecType DataCon],
     [(Var, Measure (Located BareType) ctor)]))
-> [(MSpec SpecType DataCon,
     (Var, Measure (Located BareType) ctor))]
-> ([MSpec SpecType DataCon],
    [(Var, Measure (Located BareType) ctor)])
forall a b. (a -> b) -> a -> b
$ Var
-> (MSpec SpecType DataCon, (Var, Measure (Located BareType) ctor))
forall ctor.
Var
-> (MSpec SpecType DataCon, (Var, Measure (Located BareType) ctor))
createMeasureForVar (Var
 -> (MSpec SpecType DataCon,
     (Var, Measure (Located BareType) ctor)))
-> [Var]
-> [(MSpec SpecType DataCon,
     (Var, Measure (Located BareType) ctor))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet Var -> [Var]
forall a. HashSet a -> [a]
S.toList (HashSet Var
varsUndefinedInLogic HashSet Var -> HashSet Var -> HashSet Var
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
`S.union` HashSet Var
requestedOpaqueRefl)
  where
    thisModule :: Module
thisModule = TcGblEnv -> Module
Ghc.tcg_mod (Env -> TcGblEnv
Bare.reTcGblEnv Env
env)
    -- Get the set of variables for the requested opaque reflections
    requestedOpaqueRefl :: HashSet Var
requestedOpaqueRefl = [HashSet Var] -> HashSet Var
forall a. Eq a => [HashSet a] -> HashSet a
S.unions
      ([HashSet Var] -> HashSet Var)
-> (ModSpecs -> [HashSet Var]) -> ModSpecs -> HashSet Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ModName, BareSpec) -> HashSet Var)
-> [(ModName, BareSpec)] -> [HashSet Var]
forall a b. (a -> b) -> [a] -> [b]
map ((Located LHName -> Var) -> HashSet (Located LHName) -> HashSet Var
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map Located LHName -> Var
getVar (HashSet (Located LHName) -> HashSet Var)
-> ((ModName, BareSpec) -> HashSet (Located LHName))
-> (ModName, BareSpec)
-> HashSet Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpec -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.opaqueReflects (BareSpec -> HashSet (Located LHName))
-> ((ModName, BareSpec) -> BareSpec)
-> (ModName, BareSpec)
-> HashSet (Located LHName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, BareSpec) -> BareSpec
forall a b. (a, b) -> b
snd)
      ([(ModName, BareSpec)] -> [HashSet Var])
-> (ModSpecs -> [(ModName, BareSpec)]) -> ModSpecs -> [HashSet Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList (ModSpecs -> HashSet Var) -> ModSpecs -> HashSet Var
forall a b. (a -> b) -> a -> b
$ ModSpecs
specs
    getVar :: Located LHName -> Var
getVar Located LHName
sym = case HasCallStack => Env -> Located LHName -> Lookup Var
Env -> Located LHName -> Lookup Var
Bare.lookupGhcIdLHName Env
env Located LHName
sym of
      Right Var
x -> Var
x
      Left [Error]
_ -> Maybe SrcSpan -> String -> Var
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
sym) String
"function to reflect not in scope"
    definedSymbols :: HashSet Symbol
definedSymbols = Env -> MeasEnv -> ModSpecs -> HashSet Symbol
getDefinedSymbolsInLogic Env
env MeasEnv
measEnv ModSpecs
specs
    undefinedInLogic :: a -> Bool
undefinedInLogic a
v = Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
v) HashSet Symbol
definedSymbols)
    -- Variables to consider
    varsUndefinedInLogic :: HashSet Var
varsUndefinedInLogic = [HashSet Var] -> HashSet Var
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet Var] -> HashSet Var) -> [HashSet Var] -> HashSet Var
forall a b. (a -> b) -> a -> b
$
      (Var -> Bool) -> HashSet Var -> HashSet Var
forall a. (a -> Bool) -> HashSet a -> HashSet a
S.filter Var -> Bool
forall {a}. Symbolic a => a -> Bool
undefinedInLogic (HashSet Var -> HashSet Var)
-> ((Var, LocSpecType, Equation) -> HashSet Var)
-> (Var, LocSpecType, Equation)
-> HashSet Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      (\(Var
v, LocSpecType
_, Equation
eq) -> Var -> Equation -> HashSet Var
getFreeVarsOfReflectionOfVar Var
v Equation
eq) ((Var, LocSpecType, Equation) -> HashSet Var)
-> [(Var, LocSpecType, Equation)] -> [HashSet Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, LocSpecType, Equation)]
eqs
    -- Main function: creates a (dummy) measure about a given variable
    createMeasureForVar :: Ghc.Var -> (MSpec SpecType Ghc.DataCon, (Ghc.Var, Measure LocBareType ctor))
    createMeasureForVar :: forall ctor.
Var
-> (MSpec SpecType DataCon, (Var, Measure (Located BareType) ctor))
createMeasureForVar Var
var =
      ([Measure SpecType DataCon] -> MSpec SpecType DataCon
forall ty. [Measure ty DataCon] -> MSpec ty DataCon
Ms.mkMSpec' [Measure SpecType DataCon
forall {v} {ctor}. MeasureV v SpecType ctor
smeas], (Var
var, MeasureV Symbol (Located BareType) ctor
forall {v} {ctor}. MeasureV v (Located BareType) ctor
bmeas))
      where
        locSym :: Located LHName
locSym = SourcePos -> LHName -> Located LHName
forall l b. Loc l => l -> b -> Located b
F.atLoc (LocSpecType -> SourcePos
forall a. Located a -> SourcePos
loc LocSpecType
specType) (HasCallStack => Module -> LHName -> LHName
Module -> LHName -> LHName
reflectLHName Module
thisModule (LHName -> LHName) -> LHName -> LHName
forall a b. (a -> b) -> a -> b
$ Var -> LHName
makeGHCLHNameFromId Var
var)
        specType :: LocSpecType
specType = Var -> LocSpecType
forall r. Monoid r => Var -> Located (RRType r)
varSpecType Var
var
        bareType :: Located BareType
bareType = Var -> Located BareType
forall r. Monoid r => Var -> Located (BRType r)
varBareType Var
var
        bmeas :: MeasureV v (Located BareType) ctor
bmeas = Located LHName
-> Located BareType
-> [DefV v (Located BareType) ctor]
-> MeasureKind
-> UnSortedExprs
-> MeasureV v (Located BareType) ctor
forall v ty ctor.
Located LHName
-> ty
-> [DefV v ty ctor]
-> MeasureKind
-> UnSortedExprs
-> MeasureV v ty ctor
M Located LHName
locSym Located BareType
bareType [] MeasureKind
MsReflect []
        smeas :: MeasureV v SpecType ctor
smeas = Located LHName
-> SpecType
-> [DefV v SpecType ctor]
-> MeasureKind
-> UnSortedExprs
-> MeasureV v SpecType ctor
forall v ty ctor.
Located LHName
-> ty
-> [DefV v ty ctor]
-> MeasureKind
-> UnSortedExprs
-> MeasureV v ty ctor
M Located LHName
locSym (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
specType) [] MeasureKind
MsReflect []

getUnfoldingOfVar :: Ghc.Var -> Maybe Ghc.CoreExpr
getUnfoldingOfVar :: Var -> Maybe CoreExpr
getUnfoldingOfVar = Unfolding -> Maybe CoreExpr
getExpr (Unfolding -> Maybe CoreExpr)
-> (Var -> Unfolding) -> Var -> Maybe CoreExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdInfo -> Unfolding
Ghc.realUnfoldingInfo (IdInfo -> Unfolding) -> (Var -> IdInfo) -> Var -> Unfolding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasDebugCallStack => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo
  where
    getExpr :: Ghc.Unfolding -> Maybe Ghc.CoreExpr
    getExpr :: Unfolding -> Maybe CoreExpr
getExpr (Ghc.CoreUnfolding CoreExpr
expr UnfoldingSource
_ Bool
_ UnfoldingCache
_ UnfoldingGuidance
_) = CoreExpr -> Maybe CoreExpr
forall a. a -> Maybe a
Just CoreExpr
expr
    getExpr Unfolding
_ = Maybe CoreExpr
forall a. Maybe a
Nothing

-- Get the set of "free" symbols in the (reflection of the) unfolding of a given variable.
-- Free symbols are those that are not already in the logic and that appear in
-- the reflection of the unfolding.
-- For this purpose, you need to give the variable naming the definition to reflect
-- and its corresponding equation in the logic.
getFreeVarsOfReflectionOfVar  :: Ghc.Var -> F.Equation -> S.HashSet Ghc.Var
getFreeVarsOfReflectionOfVar :: Var -> Equation -> HashSet Var
getFreeVarsOfReflectionOfVar Var
var Equation
eq =
    (Var -> Bool) -> HashSet Var -> HashSet Var
forall a. (a -> Bool) -> HashSet a -> HashSet a
S.filter (\Var
v -> Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
freeSymbolsInReflectedBody) HashSet Var
freeVarsInCoreExpr
  where
    reflExpr :: Maybe CoreExpr
reflExpr = Var -> Maybe CoreExpr
getUnfoldingOfVar Var
var
    getAllFreeVars :: CoreExpr -> [Var]
getAllFreeVars = (Var -> Bool) -> CoreExpr -> [Var]
Ghc.exprSomeFreeVarsList (Bool -> Var -> Bool
forall a b. a -> b -> a
const Bool
True)
    freeVarsInCoreExpr :: HashSet Var
freeVarsInCoreExpr = HashSet Var
-> (CoreExpr -> HashSet Var) -> Maybe CoreExpr -> HashSet Var
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HashSet Var
forall a. HashSet a
S.empty ([Var] -> HashSet Var
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Var] -> HashSet Var)
-> (CoreExpr -> [Var]) -> CoreExpr -> HashSet Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> [Var]
getAllFreeVars) Maybe CoreExpr
reflExpr
    freeSymbolsInReflectedBody :: HashSet Symbol
freeSymbolsInReflectedBody = Expr -> HashSet Symbol
F.exprSymbolsSet (Equation -> Expr
forall v. EquationV v -> ExprV v
F.eqBody Equation
eq)

-- Collect all the DataCon that appear in the unfolding of a given variable.
getDCsOfUnfoldingOfVars :: [Ghc.Var] -> S.HashSet Ghc.DataCon
getDCsOfUnfoldingOfVars :: [Var] -> HashSet DataCon
getDCsOfUnfoldingOfVars [Var]
vars = [HashSet DataCon] -> HashSet DataCon
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet DataCon] -> HashSet DataCon)
-> [HashSet DataCon] -> HashSet DataCon
forall a b. (a -> b) -> a -> b
$ CoreExpr -> HashSet DataCon
collectDataCons (CoreExpr -> HashSet DataCon) -> [CoreExpr] -> [HashSet DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> Maybe CoreExpr
getUnfoldingOfVar (Var -> Maybe CoreExpr) -> [Var] -> [CoreExpr]
forall a b. (a -> Maybe b) -> [a] -> [b]
`Mb.mapMaybe` [Var]
vars

-- Collect all DataCon that occur in case split alternatives of an expression
collectDataCons :: Ghc.CoreExpr -> S.HashSet Ghc.DataCon
collectDataCons :: CoreExpr -> HashSet DataCon
collectDataCons CoreExpr
expr = CoreExpr -> HashSet DataCon -> HashSet DataCon
forall {a}. Expr a -> HashSet DataCon -> HashSet DataCon
go CoreExpr
expr HashSet DataCon
forall a. HashSet a
S.empty
  where
    go :: Expr a -> HashSet DataCon -> HashSet DataCon
go (Ghc.Var Var
_) HashSet DataCon
acc = HashSet DataCon
acc
    go (Ghc.Lit Literal
_) HashSet DataCon
acc = HashSet DataCon
acc
    go (Ghc.App Expr a
f Expr a
e) HashSet DataCon
acc = Expr a -> HashSet DataCon -> HashSet DataCon
go Expr a
f (Expr a -> HashSet DataCon -> HashSet DataCon
go Expr a
e HashSet DataCon
acc)
    go (Ghc.Lam a
_ Expr a
e) HashSet DataCon
acc = Expr a -> HashSet DataCon -> HashSet DataCon
go Expr a
e HashSet DataCon
acc
    go (Ghc.Let Bind a
bind Expr a
e) HashSet DataCon
acc = Expr a -> HashSet DataCon -> HashSet DataCon
go Expr a
e (Bind a -> HashSet DataCon -> HashSet DataCon
goBind Bind a
bind HashSet DataCon
acc)
    go (Ghc.Case Expr a
e a
_ Type
_ [Alt a]
alts) HashSet DataCon
acc = (Alt a -> HashSet DataCon -> HashSet DataCon)
-> HashSet DataCon -> [Alt a] -> HashSet DataCon
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Alt a -> HashSet DataCon -> HashSet DataCon
goAlt (Expr a -> HashSet DataCon -> HashSet DataCon
go Expr a
e HashSet DataCon
acc) [Alt a]
alts
    go (Ghc.Cast Expr a
e CoercionR
_) HashSet DataCon
acc = Expr a -> HashSet DataCon -> HashSet DataCon
go Expr a
e HashSet DataCon
acc
    go (Ghc.Tick CoreTickish
_ Expr a
e) HashSet DataCon
acc = Expr a -> HashSet DataCon -> HashSet DataCon
go Expr a
e HashSet DataCon
acc
    go (Ghc.Type Type
_) HashSet DataCon
acc = HashSet DataCon
acc
    go (Ghc.Coercion CoercionR
_) HashSet DataCon
acc = HashSet DataCon
acc

    -- Special auxiliary function for `Alt` which is precisely where we get the datacons
    goAlt :: Alt a -> HashSet DataCon -> HashSet DataCon
goAlt (Ghc.Alt (Ghc.DataAlt DataCon
dc) [a]
_ Expr a
e) HashSet DataCon
acc = DataCon -> HashSet DataCon -> HashSet DataCon
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert DataCon
dc (Expr a -> HashSet DataCon -> HashSet DataCon
go Expr a
e HashSet DataCon
acc)
    goAlt (Ghc.Alt AltCon
_ [a]
_ Expr a
e) HashSet DataCon
acc = Expr a -> HashSet DataCon -> HashSet DataCon
go Expr a
e HashSet DataCon
acc

    goBind :: Bind a -> HashSet DataCon -> HashSet DataCon
goBind (Ghc.NonRec a
_ Expr a
e) HashSet DataCon
acc = Expr a -> HashSet DataCon -> HashSet DataCon
go Expr a
e HashSet DataCon
acc
    goBind (Ghc.Rec [(a, Expr a)]
binds) HashSet DataCon
acc = ((a, Expr a) -> HashSet DataCon -> HashSet DataCon)
-> HashSet DataCon -> [(a, Expr a)] -> HashSet DataCon
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Expr a -> HashSet DataCon -> HashSet DataCon
go (Expr a -> HashSet DataCon -> HashSet DataCon)
-> ((a, Expr a) -> Expr a)
-> (a, Expr a)
-> HashSet DataCon
-> HashSet DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Expr a) -> Expr a
forall a b. (a, b) -> b
snd) HashSet DataCon
acc [(a, Expr a)]
binds

bareMSpec :: Bare.Env -> Bare.SigEnv -> ModName -> ModName -> Ms.BareSpec -> Ms.MSpec LocBareType (Located LHName)
bareMSpec :: Env
-> SigEnv
-> ModName
-> ModName
-> BareSpec
-> MSpec (Located BareType) (Located LHName)
bareMSpec Env
env SigEnv
sigEnv ModName
myName ModName
name BareSpec
spec = [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) ()]
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
-> MSpec (Located BareType) (Located LHName)
forall t.
[Measure t (Located LHName)]
-> [Measure t ()]
-> [Measure t (Located LHName)]
-> [Measure t (Located LHName)]
-> MSpec t (Located LHName)
Ms.mkMSpec [Measure (Located BareType) (Located LHName)]
ms [Measure (Located BareType) ()]
cms [Measure (Located BareType) (Located LHName)]
ims [Measure (Located BareType) (Located LHName)]
oms
  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 {v} {ctor}. MeasureV v (Located BareType) ctor -> Bool
inScope ([Measure (Located BareType) ()]
 -> [Measure (Located BareType) ()])
-> [Measure (Located BareType) ()]
-> [Measure (Located BareType) ()]
forall a b. (a -> b) -> a -> b
$             BareSpec -> [Measure (Located BareType) ()]
forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
Ms.cmeasures BareSpec
spec
    ms :: [Measure (Located BareType) (Located LHName)]
ms         = String
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a. PPrint a => String -> a -> a
F.notracepp String
"UMS" ([Measure (Located BareType) (Located LHName)]
 -> [Measure (Located BareType) (Located LHName)])
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a b. (a -> b) -> a -> b
$ (Measure (Located BareType) (Located LHName) -> Bool)
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a. (a -> Bool) -> [a] -> [a]
filter Measure (Located BareType) (Located LHName) -> Bool
forall {v} {ctor}. MeasureV v (Located BareType) ctor -> Bool
inScope ([Measure (Located BareType) (Located LHName)]
 -> [Measure (Located BareType) (Located LHName)])
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a b. (a -> b) -> a -> b
$ Measure (Located BareType) (Located LHName)
-> Measure (Located BareType) (Located LHName)
expMeas (Measure (Located BareType) (Located LHName)
 -> Measure (Located BareType) (Located LHName))
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure (Located BareType) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
Ms.measures  BareSpec
spec
    ims :: [Measure (Located BareType) (Located LHName)]
ims        = String
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a. PPrint a => String -> a -> a
F.notracepp String
"IMS" ([Measure (Located BareType) (Located LHName)]
 -> [Measure (Located BareType) (Located LHName)])
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a b. (a -> b) -> a -> b
$ (Measure (Located BareType) (Located LHName) -> Bool)
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a. (a -> Bool) -> [a] -> [a]
filter Measure (Located BareType) (Located LHName) -> Bool
forall {v} {ctor}. MeasureV v (Located BareType) ctor -> Bool
inScope ([Measure (Located BareType) (Located LHName)]
 -> [Measure (Located BareType) (Located LHName)])
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a b. (a -> b) -> a -> b
$ Measure (Located BareType) (Located LHName)
-> Measure (Located BareType) (Located LHName)
expMeas (Measure (Located BareType) (Located LHName)
 -> Measure (Located BareType) (Located LHName))
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure (Located BareType) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
Ms.imeasures BareSpec
spec
    oms :: [Measure (Located BareType) (Located LHName)]
oms        = String
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a. PPrint a => String -> a -> a
F.notracepp String
"OMS" ([Measure (Located BareType) (Located LHName)]
 -> [Measure (Located BareType) (Located LHName)])
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a b. (a -> b) -> a -> b
$ (Measure (Located BareType) (Located LHName) -> Bool)
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a. (a -> Bool) -> [a] -> [a]
filter Measure (Located BareType) (Located LHName) -> Bool
forall {v} {ctor}. MeasureV v (Located BareType) ctor -> Bool
inScope ([Measure (Located BareType) (Located LHName)]
 -> [Measure (Located BareType) (Located LHName)])
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall a b. (a -> b) -> a -> b
$ Measure (Located BareType) (Located LHName)
-> Measure (Located BareType) (Located LHName)
expMeas (Measure (Located BareType) (Located LHName)
 -> Measure (Located BareType) (Located LHName))
-> [Measure (Located BareType) (Located LHName)]
-> [Measure (Located BareType) (Located LHName)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure (Located BareType) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
Ms.omeasures BareSpec
spec
    expMeas :: Measure (Located BareType) (Located LHName)
-> Measure (Located BareType) (Located LHName)
expMeas    = BareRTEnv
-> Measure (Located BareType) (Located LHName)
-> Measure (Located BareType) (Located LHName)
expandMeasure 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
    inScope :: MeasureV v (Located BareType) ctor -> Bool
inScope MeasureV v (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]
++ Located LHName -> String
forall a. PPrint a => a -> String
F.showpp (MeasureV v (Located BareType) ctor -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName MeasureV v (Located BareType) ctor
z)) (Bool
force Bool -> Bool -> Bool
||  MeasureV v (Located BareType) ctor -> Bool
forall {v} {ctor}. MeasureV v (Located BareType) ctor -> Bool
okSort MeasureV v (Located BareType) ctor
z)
    okSort :: MeasureV v (Located BareType) ctor -> Bool
okSort     = Env -> Located BareType -> Bool
Bare.knownGhcType Env
env (Located BareType -> Bool)
-> (MeasureV v (Located BareType) ctor -> Located BareType)
-> MeasureV v (Located BareType) ctor
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MeasureV v (Located BareType) ctor -> Located BareType
forall v ty ctor. MeasureV v ty ctor -> ty
msSort

mkMeasureDCon :: Bare.Env -> Ms.MSpec t (F.Located LHName) -> Bare.Lookup (Ms.MSpec t Ghc.DataCon)
mkMeasureDCon :: forall t.
Env -> MSpec t (Located LHName) -> Lookup (MSpec t DataCon)
mkMeasureDCon Env
env MSpec t (Located LHName)
m = do
  let ns :: [Located LHName]
ns = MSpec t (Located LHName) -> [Located LHName]
forall t. MSpec t (Located LHName) -> [Located LHName]
measureCtors MSpec t (Located LHName)
m
  dcs   <- (Located LHName -> Either [Error] DataCon)
-> [Located LHName] -> Either [Error] [DataCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (HasCallStack => Env -> Located LHName -> Either [Error] DataCon
Env -> Located LHName -> Either [Error] DataCon
Bare.lookupGhcDataConLHName Env
env) [Located LHName]
ns
  return $ mkMeasureDCon_ m (zip (val <$> ns) 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 (F.Located LHName) -> [(LHName, Ghc.DataCon)] -> Ms.MSpec t Ghc.DataCon
mkMeasureDCon_ :: forall t.
MSpec t (Located LHName) -> [(LHName, DataCon)] -> MSpec t DataCon
mkMeasureDCon_ MSpec t (Located LHName)
m [(LHName, DataCon)]
ndcs = (Located LHName -> DataCon)
-> MSpec t (Located LHName) -> MSpec t DataCon
forall a b. (a -> b) -> MSpec t a -> MSpec t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (LHName -> DataCon
tx (LHName -> DataCon)
-> (Located LHName -> LHName) -> Located LHName -> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
val) MSpec t (Located LHName)
m
  where
    tx :: LHName -> DataCon
tx                = HashMap LHName DataCon -> LHName -> DataCon
forall k v.
(HasCallStack, Eq k, Show k, Hashable k) =>
HashMap k v -> k -> v
Misc.mlookup ([(LHName, DataCon)] -> HashMap LHName DataCon
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(LHName, DataCon)]
ndcs)

measureCtors ::  Ms.MSpec t (F.Located LHName) -> [F.Located LHName]
measureCtors :: forall t. MSpec t (Located LHName) -> [Located LHName]
measureCtors = [Located LHName] -> [Located LHName]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([Located LHName] -> [Located LHName])
-> (MSpec t (Located LHName) -> [Located LHName])
-> MSpec t (Located LHName)
-> [Located LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DefV Symbol t (Located LHName) -> Located LHName)
-> [DefV Symbol t (Located LHName)] -> [Located LHName]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DefV Symbol t (Located LHName) -> Located LHName
forall v ty ctor. DefV v ty ctor -> ctor
ctor ([DefV Symbol t (Located LHName)] -> [Located LHName])
-> (MSpec t (Located LHName) -> [DefV Symbol t (Located LHName)])
-> MSpec t (Located LHName)
-> [Located LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[DefV Symbol t (Located LHName)]]
-> [DefV Symbol t (Located LHName)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[DefV Symbol t (Located LHName)]]
 -> [DefV Symbol t (Located LHName)])
-> (MSpec t (Located LHName) -> [[DefV Symbol t (Located LHName)]])
-> MSpec t (Located LHName)
-> [DefV Symbol t (Located LHName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap LHName [DefV Symbol t (Located LHName)]
-> [[DefV Symbol t (Located LHName)]]
forall k v. HashMap k v -> [v]
M.elems (HashMap LHName [DefV Symbol t (Located LHName)]
 -> [[DefV Symbol t (Located LHName)]])
-> (MSpec t (Located LHName)
    -> HashMap LHName [DefV Symbol t (Located LHName)])
-> MSpec t (Located LHName)
-> [[DefV Symbol t (Located LHName)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MSpec t (Located LHName)
-> HashMap LHName [DefV Symbol t (Located LHName)]
forall ty ctor. MSpec ty ctor -> HashMap LHName [Def ty ctor]
Ms.ctorMap

mkMeasureSort :: Bare.Env -> Ms.MSpec BareType (F.Located LHName)
              -> Ms.MSpec SpecType (F.Located LHName)
mkMeasureSort :: Env
-> MSpec BareType (Located LHName)
-> MSpec SpecType (Located LHName)
mkMeasureSort Env
env (Ms.MSpec HashMap LHName [Def BareType (Located LHName)]
c HashMap (Located LHName) (Measure BareType (Located LHName))
mm HashMap (Located LHName) (Measure BareType ())
cm [Measure BareType (Located LHName)]
im) =
  HashMap LHName [Def SpecType (Located LHName)]
-> HashMap (Located LHName) (Measure SpecType (Located LHName))
-> HashMap (Located LHName) (Measure SpecType ())
-> [Measure SpecType (Located LHName)]
-> MSpec SpecType (Located LHName)
forall ty ctor.
HashMap LHName [Def ty ctor]
-> HashMap (Located LHName) (Measure ty ctor)
-> HashMap (Located LHName) (Measure ty ())
-> [Measure ty ctor]
-> MSpec ty ctor
Ms.MSpec ((Def BareType (Located LHName) -> Def SpecType (Located LHName))
-> [Def BareType (Located LHName)]
-> [Def SpecType (Located LHName)]
forall a b. (a -> b) -> [a] -> [b]
map Def BareType (Located LHName) -> Def SpecType (Located LHName)
forall ctor. Def BareType ctor -> Def SpecType ctor
txDef ([Def BareType (Located LHName)]
 -> [Def SpecType (Located LHName)])
-> HashMap LHName [Def BareType (Located LHName)]
-> HashMap LHName [Def SpecType (Located LHName)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap LHName [Def BareType (Located LHName)]
c) (Measure BareType (Located LHName)
-> Measure SpecType (Located LHName)
forall ctor. Measure BareType ctor -> Measure SpecType ctor
tx (Measure BareType (Located LHName)
 -> Measure SpecType (Located LHName))
-> HashMap (Located LHName) (Measure BareType (Located LHName))
-> HashMap (Located LHName) (Measure SpecType (Located LHName))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap (Located LHName) (Measure BareType (Located LHName))
mm) (Measure BareType () -> Measure SpecType ()
forall ctor. Measure BareType ctor -> Measure SpecType ctor
tx (Measure BareType () -> Measure SpecType ())
-> HashMap (Located LHName) (Measure BareType ())
-> HashMap (Located LHName) (Measure SpecType ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap (Located LHName) (Measure BareType ())
cm) (Measure BareType (Located LHName)
-> Measure SpecType (Located LHName)
forall ctor. Measure BareType ctor -> Measure SpecType ctor
tx (Measure BareType (Located LHName)
 -> Measure SpecType (Located LHName))
-> [Measure BareType (Located LHName)]
-> [Measure SpecType (Located LHName)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Measure BareType (Located LHName)]
im)
    where
      ofMeaSort :: F.SourcePos -> BareType -> SpecType
      ofMeaSort :: SourcePos -> BareType -> SpecType
ofMeaSort SourcePos
l = HasCallStack =>
Env
-> SourcePos
-> Maybe [PVarV Symbol (BSortV Symbol)]
-> BareType
-> SpecType
Env
-> SourcePos
-> Maybe [PVarV Symbol (BSortV Symbol)]
-> BareType
-> SpecType
Bare.ofBareType Env
env SourcePos
l Maybe [PVarV Symbol (BSortV Symbol)]
forall a. Maybe a
Nothing

      tx :: Measure BareType ctor -> Measure SpecType ctor
      tx :: forall ctor. Measure BareType ctor -> Measure SpecType ctor
tx (M Located LHName
n BareType
s [DefV Symbol BareType ctor]
eqs MeasureKind
k UnSortedExprs
u) = Located LHName
-> SpecType
-> [DefV Symbol SpecType ctor]
-> MeasureKind
-> UnSortedExprs
-> MeasureV Symbol SpecType ctor
forall v ty ctor.
Located LHName
-> ty
-> [DefV v ty ctor]
-> MeasureKind
-> UnSortedExprs
-> MeasureV v ty ctor
M Located LHName
n (SourcePos -> BareType -> SpecType
ofMeaSort SourcePos
l BareType
s) (DefV Symbol BareType ctor -> DefV Symbol SpecType ctor
forall ctor. Def BareType ctor -> Def SpecType ctor
txDef (DefV Symbol BareType ctor -> DefV Symbol SpecType ctor)
-> [DefV Symbol BareType ctor] -> [DefV Symbol SpecType ctor]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DefV Symbol BareType ctor]
eqs) MeasureKind
k UnSortedExprs
u where l :: SourcePos
l = Located LHName -> SourcePos
forall a. Loc a => a -> SourcePos
GM.fSourcePos Located LHName
n

      txDef :: Def BareType ctor -> Def SpecType ctor
      txDef :: forall ctor. Def BareType ctor -> Def SpecType ctor
txDef Def BareType ctor
d = (BareType -> SpecType)
-> Def BareType ctor -> DefV Symbol SpecType ctor
forall a b c. (a -> b) -> DefV Symbol a c -> DefV Symbol b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SourcePos -> BareType -> SpecType
ofMeaSort SourcePos
l) Def BareType ctor
d                              where l :: SourcePos
l = Located LHName -> SourcePos
forall a. Loc a => a -> SourcePos
GM.fSourcePos (Def BareType ctor -> Located LHName
forall v ty ctor. DefV v ty ctor -> Located LHName
measure Def BareType ctor
d)



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

expandMeasure :: BareRTEnv -> BareMeasure -> BareMeasure
expandMeasure :: BareRTEnv
-> Measure (Located BareType) (Located LHName)
-> Measure (Located BareType) (Located LHName)
expandMeasure BareRTEnv
rtEnv Measure (Located BareType) (Located LHName)
m = Measure (Located BareType) (Located LHName)
m
  { msSort = RT.generalize <$> msSort m
  , msEqns = expandMeasureDef rtEnv <$> msEqns m
  }

expandMeasureDef :: BareRTEnv -> Def t (Located LHName) -> Def t (Located LHName)
expandMeasureDef :: forall t.
BareRTEnv -> Def t (Located LHName) -> Def t (Located LHName)
expandMeasureDef BareRTEnv
rtEnv Def t (Located LHName)
d = Def t (Located LHName)
d
  { body  = F.notracepp msg $ Bare.expand rtEnv l (body d) }
  where
    l :: SourcePos
l     = Located LHName -> SourcePos
forall a. Located a -> SourcePos
loc (Def t (Located LHName) -> Located LHName
forall v ty ctor. DefV v ty ctor -> Located LHName
measure Def t (Located LHName)
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 (Located LHName) -> [(Symbol, Maybe t)]
forall v ty ctor. DefV v ty ctor -> [(Symbol, Maybe ty)]
binds Def t (Located LHName)
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 (Located LHName) -> Body
forall v ty ctor. DefV v ty ctor -> BodyV v
body Def t (Located LHName)
d)

------------------------------------------------------------------------------
varMeasures :: (Monoid r) => Bare.Env -> [(F.Symbol, Located (RRType r))]
------------------------------------------------------------------------------
varMeasures :: forall r. Monoid r => 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]
Bare.reDataConIds Env
env
      , Var -> Bool
GM.isDataConId Var
v
      , Type -> Bool
isSimpleType (Var -> Type
Ghc.varType Var
v) ]

getMeasVars :: Bare.Env -> Bare.MeasEnv -> [(F.Symbol, Located (RRType F.Reft))]
getMeasVars :: Env -> MeasEnv -> [(Symbol, Located (RRType Reft))]
getMeasVars Env
env MeasEnv
measEnv = MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meSyms MeasEnv
measEnv -- ms'
                            [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
forall a. [a] -> [a] -> [a]
++ MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meClassSyms MeasEnv
measEnv -- cms'
                            [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
forall a. [a] -> [a] -> [a]
++ Env -> [(Symbol, Located (RRType Reft))]
forall r. Monoid r => Env -> [(Symbol, Located (RRType r))]
varMeasures Env
env

varSpecType :: (Monoid r) => Ghc.Var -> Located (RRType r)
varSpecType :: forall r. Monoid r => Var -> Located (RRType r)
varSpecType = (Var -> RRType r) -> Located Var -> Located (RRType r)
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> RRType r
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> RRType r) -> (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

varBareType :: (Monoid r) => Ghc.Var -> Located (BRType r)
varBareType :: forall r. Monoid r => Var -> Located (BRType r)
varBareType = (Var -> BRType r) -> Located Var -> Located (BRType r)
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> BRType r
forall r. Monoid r => Type -> BRType r
RT.bareOfType (Type -> BRType r) -> (Var -> Type) -> Var -> BRType r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type
Ghc.varType) (Located Var -> Located (BRType r))
-> (Var -> Located Var) -> Var -> Located (BRType r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Located Var
forall a. NamedThing a => a -> Located a
GM.locNamedThing

varLocSym :: Ghc.Var -> LocSymbol
varLocSym :: Var -> LocSymbol
varLocSym Var
v = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> Located Var -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> Located Var
forall a. NamedThing a => a -> Located a
GM.locNamedThing Var
v

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
                     -> [(Located LHName, CMeasure (RType c tv r2))]
makeClassMeasureSpec :: forall c tv r2 t.
MSpec (RType c tv (UReft r2)) t
-> [(Located LHName, CMeasure (RType c tv r2))]
makeClassMeasureSpec Ms.MSpec{[Measure (RType c tv (UReft r2)) t]
HashMap (Located LHName) (Measure (RType c tv (UReft r2)) t)
HashMap (Located LHName) (Measure (RType c tv (UReft r2)) ())
HashMap LHName [Def (RType c tv (UReft r2)) t]
ctorMap :: forall ty ctor. MSpec ty ctor -> HashMap LHName [Def ty ctor]
ctorMap :: HashMap LHName [Def (RType c tv (UReft r2)) t]
measMap :: HashMap (Located LHName) (Measure (RType c tv (UReft r2)) t)
cmeasMap :: HashMap (Located LHName) (Measure (RType c tv (UReft r2)) ())
imeas :: [Measure (RType c tv (UReft r2)) t]
imeas :: forall ty ctor. MSpec ty ctor -> [Measure ty ctor]
cmeasMap :: forall ty ctor.
MSpec ty ctor -> HashMap (Located LHName) (Measure ty ())
measMap :: forall ty ctor.
MSpec ty ctor -> HashMap (Located LHName) (Measure ty ctor)
..} = Measure (RType c tv (UReft r2)) ()
-> (Located LHName, CMeasure (RTypeV Symbol c tv r2))
forall {v} {v} {c} {tv} {v} {r2} {ctor}.
MeasureV v (RTypeV v c tv (UReftV v r2)) ctor
-> (Located LHName, CMeasure (RTypeV v c tv r2))
tx (Measure (RType c tv (UReft r2)) ()
 -> (Located LHName, CMeasure (RTypeV Symbol c tv r2)))
-> [Measure (RType c tv (UReft r2)) ()]
-> [(Located LHName, CMeasure (RTypeV Symbol c tv r2))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap (Located LHName) (Measure (RType c tv (UReft r2)) ())
-> [Measure (RType c tv (UReft r2)) ()]
forall k v. HashMap k v -> [v]
M.elems HashMap (Located LHName) (Measure (RType c tv (UReft r2)) ())
cmeasMap
  where
    tx :: MeasureV v (RTypeV v c tv (UReftV v r2)) ctor
-> (Located LHName, CMeasure (RTypeV v c tv r2))
tx (M Located LHName
n RTypeV v c tv (UReftV v r2)
s [DefV v (RTypeV v c tv (UReftV v r2)) ctor]
_ MeasureKind
_ UnSortedExprs
_) = (Located LHName
n, Located LHName -> RTypeV v c tv r2 -> CMeasure (RTypeV v c tv r2)
forall ty. Located LHName -> ty -> CMeasure ty
CM Located LHName
n ((UReftV v r2 -> r2)
-> RTypeV v c tv (UReftV v r2) -> RTypeV v c tv r2
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft UReftV v r2 -> r2
forall v r. UReftV v r -> r
ur_reft RTypeV v c tv (UReftV v 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

-}