{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE OverloadedStrings         #-}

-- | This module defines the representation of Subtyping and WF Constraints,
--   and the code for syntax-directed constraint generation.

module Language.Haskell.Liquid.Constraint.Init (
    initEnv ,
    initCGI,
    ) where

import           Prelude                                       hiding (error, undefined)
import           Control.Monad.State
import           Data.Maybe                                    (isNothing, fromMaybe, catMaybes, mapMaybe)
import qualified Data.HashMap.Strict                           as M
import qualified Data.HashSet                                  as S
import qualified Data.List                                     as L
import           Data.Bifunctor
import qualified Language.Fixpoint.Types                       as F

import qualified Language.Haskell.Liquid.UX.CTags              as Tg
import           Language.Haskell.Liquid.Constraint.Fresh
import           Language.Haskell.Liquid.Constraint.Env
import           Language.Haskell.Liquid.WiredIn               (dictionaryVar)
import qualified Language.Haskell.Liquid.GHC.SpanStack         as Sp
import           Language.Haskell.Liquid.GHC.Misc             ( idDataConM, hasBaseTypeVar, isDataConId) -- dropModuleNames, simplesymbol)
import           Liquid.GHC.API               as Ghc
import           Language.Haskell.Liquid.Misc
import           Language.Fixpoint.Misc
import           Language.Haskell.Liquid.Constraint.Types

import           Language.Haskell.Liquid.Types hiding (binds, Loc, loc, freeTyVars, Def)

--------------------------------------------------------------------------------
initEnv :: TargetInfo -> CG CGEnv
--------------------------------------------------------------------------------
initEnv :: TargetInfo -> CG CGEnv
initEnv TargetInfo
info
  = do let tce :: TCEmb TyCon
tce   = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (TargetSpec -> GhcSpecNames
gsName TargetSpec
sp)
       let fVars :: [Var]
fVars = TargetSrc -> [Var]
giImpVars (TargetInfo -> TargetSrc
giSrc TargetInfo
info)
       let dcs :: [Var]
dcs   = forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isConLikeId (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecNames -> [(Symbol, Var)]
gsFreeSyms (TargetSpec -> GhcSpecNames
gsName TargetSpec
sp))
       let dcs' :: [Var]
dcs'  = forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isConLikeId [Var]
fVars
       [(Var, SpecType)]
defaults <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Var]
fVars forall a b. (a -> b) -> a -> b
$ \Var
x -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Var
x,) (Bool -> Type -> CG SpecType
trueTy Bool
allowTC forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x)
       [(Var, SpecType)]
dcsty    <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Var]
dcs   (Bool -> Var -> StateT CGInfo Identity (Var, SpecType)
makeDataConTypes Bool
allowTC)
       [(Var, SpecType)]
dcsty'   <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Var]
dcs'  (Bool -> Var -> StateT CGInfo Identity (Var, SpecType)
makeDataConTypes Bool
allowTC)
       ([Symbol]
hs,[(Var, SpecType)]
f0)  <- forall t r c (f :: * -> *) tv.
(Symbolic t, Reftable r, TyConable c, Freshable f r) =>
Bool -> [(t, RType c tv r)] -> f ([Symbol], [(t, RType c tv r)])
refreshHoles Bool
allowTC forall a b. (a -> b) -> a -> b
$ TargetInfo -> [(Var, SpecType)]
grty TargetInfo
info                           -- asserted refinements     (for defined vars)
       [(Var, SpecType)]
f0''     <- forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TargetInfo -> StateT CGInfo Identity [(Var, SpecType)]
grtyTop TargetInfo
info                      -- default TOP reftype      (for exported vars without spec)
       let f0' :: [(Var, SpecType)]
f0'   = if Config -> Bool
notruetypes forall a b. (a -> b) -> a -> b
$ forall t. HasConfig t => t -> Config
getConfig TargetSpec
sp then [] else [(Var, SpecType)]
f0''
       [(Var, SpecType)]
f1       <- forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs'   [(Var, SpecType)]
defaults                            -- default TOP reftype      (for all vars)
       [(Var, SpecType)]
f1'      <- forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' forall a b. (a -> b) -> a -> b
$ [(Var, SpecType)] -> [(Var, SpecType)]
makeExactDc [(Var, SpecType)]
dcsty                   -- data constructors
       [(Var, SpecType)]
f2       <- forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' forall a b. (a -> b) -> a -> b
$ TargetInfo -> [(Var, SpecType)]
assm TargetInfo
info                           -- assumed refinements      (for imported vars)
       [(Var, SpecType)]
f3'      <- forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TargetInfo -> StateT CGInfo Identity [(Var, SpecType)]
recSelectorsTy TargetInfo
info                      -- assumed refinements      (for record selectors)
       [(Var, SpecType)]
f3       <- forall {a}. [(a, SpecType)] -> [(a, SpecType)]
addPolyInfo' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' (forall {a} {a} {c}. (a -> [(a, Located c)]) -> a -> [(a, c)]
vals GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp))                 -- assumed refinedments     (with `assume`)
       [(Var, SpecType)]
f40      <- [(Var, SpecType)] -> [(Var, SpecType)]
makeExactDc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' (forall {a} {a} {c}. (a -> [(a, Located c)]) -> a -> [(a, c)]
vals GhcSpecData -> [(Var, LocSpecType)]
gsCtors (TargetSpec -> GhcSpecData
gsData TargetSpec
sp)) -- constructor refinements  (for measures)
       [(Var, SpecType)]
f5       <- forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' forall a b. (a -> b) -> a -> b
$ forall {a} {a} {c}. (a -> [(a, Located c)]) -> a -> [(a, c)]
vals GhcSpecSig -> [(Var, LocSpecType)]
gsInSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp)                   -- internal refinements     (from Haskell measures)
       [(Var, SpecType)]
fi       <- forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ [(Var
x,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. MethodType t -> Maybe t
getMethodType MethodType LocSpecType
mt | (Var
x, MethodType LocSpecType
mt) <- GhcSpecSig -> [(Var, MethodType LocSpecType)]
gsMethods forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecSig
gsSig forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSpec
giSpec TargetInfo
info ]
       ([LocSpecType]
invs1, [(Var, SpecType)]
f41) <- forall (m :: * -> *) b c a.
Applicative m =>
(b -> m c) -> (a, b) -> m (a, c)
mapSndM forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' forall a b. (a -> b) -> a -> b
$ [(Var, SpecType)]
-> HashSet TyCon -> [Var] -> ([LocSpecType], [(Var, SpecType)])
makeAutoDecrDataCons [(Var, SpecType)]
dcsty  (GhcSpecTerm -> HashSet TyCon
gsAutosize (TargetSpec -> GhcSpecTerm
gsTerm TargetSpec
sp)) [Var]
dcs
       ([LocSpecType]
invs2, [(Var, SpecType)]
f42) <- forall (m :: * -> *) b c a.
Applicative m =>
(b -> m c) -> (a, b) -> m (a, c)
mapSndM forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' forall a b. (a -> b) -> a -> b
$ [(Var, SpecType)]
-> HashSet TyCon -> [Var] -> ([LocSpecType], [(Var, SpecType)])
makeAutoDecrDataCons [(Var, SpecType)]
dcsty' (GhcSpecTerm -> HashSet TyCon
gsAutosize (TargetSpec -> GhcSpecTerm
gsTerm TargetSpec
sp)) [Var]
dcs'
       let f4 :: [(Var, SpecType)]
f4    = TCEmb TyCon
-> [(Var, SpecType)] -> [(Var, SpecType)] -> [(Var, SpecType)]
mergeDataConTypes TCEmb TyCon
tce (TCEmb TyCon
-> [(Var, SpecType)] -> [(Var, SpecType)] -> [(Var, SpecType)]
mergeDataConTypes TCEmb TyCon
tce [(Var, SpecType)]
f40 ([(Var, SpecType)]
f41 forall a. [a] -> [a] -> [a]
++ [(Var, SpecType)]
f42)) (forall a. (a -> Bool) -> [a] -> [a]
filter (Var -> Bool
isDataConId forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Var, SpecType)]
f2)
       let tx :: (Var, SpecType) -> (Symbol, SpecType)
tx    = forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTyConInv -> (Var, SpecType) -> (Var, SpecType)
addRInv RTyConInv
ialias forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> (Var, SpecType) -> (Var, SpecType)
predsUnify TargetSpec
sp
       [(Symbol, SpecType)]
f6       <- forall a b. (a -> b) -> [a] -> [b]
map (Var, SpecType) -> (Symbol, SpecType)
tx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. [(a, SpecType)] -> [(a, SpecType)]
addPolyInfo' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' (forall {a} {a} {c}. (a -> [(a, Located c)]) -> a -> [(a, c)]
vals GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp))
       let bs :: [[(Symbol, SpecType)]]
bs    = ((Var, SpecType) -> (Symbol, SpecType)
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[(Var, SpecType)]
f0 forall a. [a] -> [a] -> [a]
++ [(Var, SpecType)]
f0' forall a. [a] -> [a] -> [a]
++ [(Var, SpecType)]
fi, [(Var, SpecType)]
f1 forall a. [a] -> [a] -> [a]
++ [(Var, SpecType)]
f1', [(Var, SpecType)]
f2, [(Var, SpecType)]
f3 forall a. [a] -> [a] -> [a]
++ [(Var, SpecType)]
f3', [(Var, SpecType)]
f4, [(Var, SpecType)]
f5]
       forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { dataConTys :: [(Var, SpecType)]
dataConTys = [(Var, SpecType)]
f4 }
       [(Symbol, Sort)]
lt1s     <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGInfo -> SEnv Sort
cgLits)
       let lt2s :: [(Symbol, Sort)]
lt2s  = [ (forall a. Symbolic a => a -> Symbol
F.symbol Var
x, forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce SpecType
t) | (Var
x, SpecType
t) <- [(Var, SpecType)]
f1' ]
       let tcb :: [(Symbol, Sort)]
tcb   = forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Symbol, SpecType)]]
bs
       let cbs :: [CoreBind]
cbs   = TargetSrc -> [CoreBind]
giCbs forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSrc
giSrc forall a b. (a -> b) -> a -> b
$ TargetInfo
info
       [(Symbol, SpecType)]
rTrue   <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) b c a.
Applicative m =>
(b -> m c) -> (a, b) -> m (a, c)
mapSndM (forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC)) [(Symbol, SpecType)]
f6
       let γ0 :: CGEnv
γ0    = TargetSpec
-> [(Symbol, SpecType)]
-> [CoreBind]
-> [(Symbol, Sort)]
-> [(Symbol, Sort)]
-> [(Symbol, Sort)]
-> [(Symbol, SpecType)]
-> [(Symbol, SpecType)]
-> [Symbol]
-> TargetInfo
-> CGEnv
measEnv TargetSpec
sp (forall a. [a] -> a
head [[(Symbol, SpecType)]]
bs) [CoreBind]
cbs [(Symbol, Sort)]
tcb [(Symbol, Sort)]
lt1s [(Symbol, Sort)]
lt2s ([(Symbol, SpecType)]
f6 forall a. [a] -> [a] -> [a]
++ [[(Symbol, SpecType)]]
bsforall a. [a] -> Int -> a
!!Int
3) ([[(Symbol, SpecType)]]
bsforall a. [a] -> Int -> a
!!Int
5) [Symbol]
hs TargetInfo
info
       CGEnv
γ  <- CGEnv -> CGEnv
globalize forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
(+=) CGEnv
γ0 ( [(String
"initEnv", Symbol
x, SpecType
y) | (Symbol
x, SpecType
y) <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([(Symbol, SpecType)]
rTrueforall a. a -> [a] -> [a]
:forall a. [a] -> [a]
tail [[(Symbol, SpecType)]]
bs)])
       forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ {invs :: RTyConInv
invs = [LocSpecType] -> RTyConInv
is ([LocSpecType]
invs1 forall a. [a] -> [a] -> [a]
++ [LocSpecType]
invs2)}
  where
    allowTC :: Bool
allowTC      = Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig TargetInfo
info)
    sp :: TargetSpec
sp           = TargetInfo -> TargetSpec
giSpec TargetInfo
info
    ialias :: RTyConInv
ialias       = forall a. [(a, LocSpecType)] -> RTyConInv
mkRTyConIAl (GhcSpecData -> [(LocSpecType, LocSpecType)]
gsIaliases (TargetSpec -> GhcSpecData
gsData TargetSpec
sp))
    vals :: (a -> [(a, Located c)]) -> a -> [(a, c)]
vals a -> [(a, Located c)]
f       = forall a b. (a -> b) -> [a] -> [b]
map (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd forall a. Located a -> a
val) forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [(a, Located c)]
f
    is :: [LocSpecType] -> RTyConInv
is [LocSpecType]
autoinv   = [(Maybe Var, LocSpecType)] -> RTyConInv
mkRTyConInv    (GhcSpecData -> [(Maybe Var, LocSpecType)]
gsInvariants (TargetSpec -> GhcSpecData
gsData TargetSpec
sp) forall a. [a] -> [a] -> [a]
++ ((forall a. Maybe a
Nothing,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSpecType]
autoinv))
    addPolyInfo' :: [(a, SpecType)] -> [(a, SpecType)]
addPolyInfo' = if Config -> Bool
reflection (forall t. HasConfig t => t -> Config
getConfig TargetInfo
info) then forall a b. (a -> b) -> [a] -> [b]
map (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd SpecType -> SpecType
addPolyInfo) else forall a. a -> a
id

    makeExactDc :: [(Var, SpecType)] -> [(Var, SpecType)]
makeExactDc [(Var, SpecType)]
dcs = if forall t. HasConfig t => t -> Bool
exactDCFlag TargetInfo
info then forall a b. (a -> b) -> [a] -> [b]
map (Var, SpecType) -> (Var, SpecType)
strengthenDataConType [(Var, SpecType)]
dcs else [(Var, SpecType)]
dcs

addPolyInfo :: SpecType -> SpecType
addPolyInfo :: SpecType -> SpecType
addPolyInfo SpecType
t = forall (t :: * -> *) (t1 :: * -> *) tv c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RType c tv ()), r)
-> t1 (PVar (RType c tv ())) -> RType c tv r -> RType c tv r
mkUnivs (forall {a} {b}. (RTVar RTyVar a, b) -> (RTVar RTyVar a, b)
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
as) [PVar (RType RTyCon RTyVar ())]
ps SpecType
t'
  where
    ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
as, [PVar (RType RTyCon RTyVar ())]
ps, SpecType
t') = forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv SpecType
t
    pos :: Positions RTyVar
pos          = forall tv r. RType RTyCon tv r -> Positions tv
tyVarsPosition SpecType
t'
    go :: (RTVar RTyVar a, b) -> (RTVar RTyVar a, b)
go (RTVar RTyVar a
a,b
r) = if {- ty_var_value a `elem` ppos pos && -}  forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar a
a forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a. Positions a -> [a]
pneg Positions RTyVar
pos
               then (forall tv a. RTVar tv a -> Bool -> RTVar tv a
setRtvPol RTVar RTyVar a
a Bool
False,b
r)
               else (RTVar RTyVar a
a,b
r)

makeDataConTypes :: Bool -> Var -> CG (Var, SpecType)
makeDataConTypes :: Bool -> Var -> StateT CGInfo Identity (Var, SpecType)
makeDataConTypes Bool
allowTC Var
x = (Var
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Type -> CG SpecType
trueTy Bool
allowTC (Var -> Type
varType Var
x)

makeAutoDecrDataCons :: [(Id, SpecType)] -> S.HashSet TyCon -> [Id] -> ([LocSpecType], [(Id, SpecType)])
makeAutoDecrDataCons :: [(Var, SpecType)]
-> HashSet TyCon -> [Var] -> ([LocSpecType], [(Var, SpecType)])
makeAutoDecrDataCons [(Var, SpecType)]
dcts HashSet TyCon
specenv [Var]
dcs
  = (forall {tv} {a} {c}.
(Eq tv, Eq a, Eq c) =>
[RType c tv a] -> [Located (RType c tv RReft)]
simplify [RType RTyCon RTyVar ()]
rsorts, [(Var, SpecType)]
tys)
  where
    ([RType RTyCon RTyVar ()]
rsorts, [(Var, SpecType)]
tys) = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TyCon -> [(RType RTyCon RTyVar (), (Var, SpecType))]
go [TyCon]
tycons
    tycons :: [TyCon]
tycons      = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Var -> Maybe TyCon
idTyCon [Var]
dcs

    go :: TyCon -> [(RType RTyCon RTyVar (), (Var, SpecType))]
go TyCon
tycon
      | forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member TyCon
tycon HashSet TyCon
specenv =  forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ([(Var, SpecType)]
-> DataCon -> Integer -> (RType RTyCon RTyVar (), (Var, SpecType))
makeSizedDataCons [(Var, SpecType)]
dcts) (TyCon -> [DataCon]
tyConDataCons TyCon
tycon) [Integer
0..]
    go TyCon
_
      = []

    simplify :: [RType c tv a] -> [Located (RType c tv RReft)]
simplify [RType c tv a]
invs = forall a. a -> Located a
dummyLoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` RReft
invariant) forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Eq a => [a] -> [a]
L.nub [RType c tv a]
invs
    invariant :: RReft
invariant = forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
F.vv_, Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Ge (Symbol -> Expr
lenOf Symbol
F.vv_) (Constant -> Expr
F.ECon forall a b. (a -> b) -> a -> b
$ Integer -> Constant
F.I Integer
0)) ) forall a. Monoid a => a
mempty

idTyCon :: Id -> Maybe TyCon
idTyCon :: Var -> Maybe TyCon
idTyCon = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TyCon
dataConTyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Maybe DataCon
idDataConM

lenOf :: F.Symbol -> F.Expr
lenOf :: Symbol -> Expr
lenOf Symbol
x = LocSymbol -> [Expr] -> Expr
F.mkEApp LocSymbol
lenLocSymbol [Symbol -> Expr
F.EVar Symbol
x]

makeSizedDataCons :: [(Id, SpecType)] -> DataCon -> Integer -> (RSort, (Id, SpecType))
makeSizedDataCons :: [(Var, SpecType)]
-> DataCon -> Integer -> (RType RTyCon RTyVar (), (Var, SpecType))
makeSizedDataCons [(Var, SpecType)]
dcts DataCon
x' Integer
n = (forall c tv r. RType c tv r -> RType c tv ()
toRSort forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
trep, (Var
x, forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep RTypeRep RTyCon RTyVar RReft
trep{ty_res :: SpecType
ty_res = SpecType
tres}))
    where
      x :: Var
x      = DataCon -> Var
dataConWorkId DataCon
x'
      st :: SpecType
st     = forall a. a -> Maybe a -> a
fromMaybe (forall a. Maybe SrcSpan -> String -> a
impossible forall a. Maybe a
Nothing String
"makeSizedDataCons: this should never happen") forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Var
x [(Var, SpecType)]
dcts
      trep :: RTypeRep RTyCon RTyVar RReft
trep   = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
st
      tres :: SpecType
tres   = forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
trep forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
F.vv_, Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Eq (Symbol -> Expr
lenOf Symbol
F.vv_) Expr
computelen)) forall a. Monoid a => a
mempty

      recarguments :: [(SpecType, Symbol)]
recarguments = forall a. (a -> Bool) -> [a] -> [a]
filter (\(SpecType
t,Symbol
_) -> forall c tv r. RType c tv r -> RType c tv ()
toRSort SpecType
t forall a. Eq a => a -> a -> Bool
== forall c tv r. RType c tv r -> RType c tv ()
toRSort SpecType
tres) (forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep) (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep))
      computelen :: Expr
computelen   = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Bop -> Expr -> Expr -> Expr
F.EBin Bop
F.Plus) (Constant -> Expr
F.ECon forall a b. (a -> b) -> a -> b
$ Integer -> Constant
F.I Integer
n) (Symbol -> Expr
lenOf forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SpecType, Symbol)]
recarguments)

mergeDataConTypes ::  F.TCEmb TyCon -> [(Var, SpecType)] -> [(Var, SpecType)] -> [(Var, SpecType)]
mergeDataConTypes :: TCEmb TyCon
-> [(Var, SpecType)] -> [(Var, SpecType)] -> [(Var, SpecType)]
mergeDataConTypes TCEmb TyCon
tce [(Var, SpecType)]
xts [(Var, SpecType)]
yts = forall {a}.
(PPrint a, NamedThing a, Ord a) =>
[(a, SpecType)] -> [(a, SpecType)] -> [(a, SpecType)]
merge (forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy forall {a} {b} {b}. Ord a => (a, b) -> (a, b) -> Ordering
f [(Var, SpecType)]
xts) (forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy forall {a} {b} {b}. Ord a => (a, b) -> (a, b) -> Ordering
f [(Var, SpecType)]
yts)
  where
    f :: (a, b) -> (a, b) -> Ordering
f (a
x,b
_) (a
y,b
_) = forall a. Ord a => a -> a -> Ordering
compare a
x a
y
    merge :: [(a, SpecType)] -> [(a, SpecType)] -> [(a, SpecType)]
merge [] [(a, SpecType)]
ys = [(a, SpecType)]
ys
    merge [(a, SpecType)]
xs [] = [(a, SpecType)]
xs
    merge (xt :: (a, SpecType)
xt@(a
x, SpecType
tx):[(a, SpecType)]
xs) (yt :: (a, SpecType)
yt@(a
y, SpecType
ty):[(a, SpecType)]
ys)
      | a
x forall a. Eq a => a -> a -> Bool
== a
y    = (a
x, forall {a} {a}.
(PPrint a, NamedThing a, NamedThing a) =>
a -> SpecType -> a -> SpecType -> SpecType
mXY a
x SpecType
tx a
y SpecType
ty) forall a. a -> [a] -> [a]
: [(a, SpecType)] -> [(a, SpecType)] -> [(a, SpecType)]
merge [(a, SpecType)]
xs [(a, SpecType)]
ys
      | a
x forall a. Ord a => a -> a -> Bool
<  a
y    = (a, SpecType)
xt forall a. a -> [a] -> [a]
: [(a, SpecType)] -> [(a, SpecType)] -> [(a, SpecType)]
merge [(a, SpecType)]
xs ((a, SpecType)
yt forall a. a -> [a] -> [a]
: [(a, SpecType)]
ys)
      | Bool
otherwise = (a, SpecType)
yt forall a. a -> [a] -> [a]
: [(a, SpecType)] -> [(a, SpecType)] -> [(a, SpecType)]
merge ((a, SpecType)
xt forall a. a -> [a] -> [a]
: [(a, SpecType)]
xs) [(a, SpecType)]
ys
    mXY :: a -> SpecType -> a -> SpecType -> SpecType
mXY a
x SpecType
tx a
y SpecType
ty = TCEmb TyCon
-> Doc -> (SrcSpan, SpecType) -> (SrcSpan, SpecType) -> SpecType
meetVarTypes TCEmb TyCon
tce (forall a. PPrint a => a -> Doc
F.pprint a
x) (forall a. NamedThing a => a -> SrcSpan
getSrcSpan a
x, SpecType
tx) (forall a. NamedThing a => a -> SrcSpan
getSrcSpan a
y, SpecType
ty)

refreshArgs' :: [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' :: forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) b c a.
Applicative m =>
(b -> m c) -> (a, b) -> m (a, c)
mapSndM forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshArgs)


-- | TODO: All this *should* happen inside @Bare@ but appears
--   to happen after certain are signatures are @fresh@-ed,
--   which is why they are here.

-- NV : still some sigs do not get TyConInfo

predsUnify :: TargetSpec -> (Var, RRType RReft) -> (Var, RRType RReft)
predsUnify :: TargetSpec -> (Var, SpecType) -> (Var, SpecType)
predsUnify TargetSpec
sp = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> TyConMap -> RRType r -> RRType r
addTyConInfo TCEmb TyCon
tce TyConMap
tyi) -- needed to eliminate some @RPropH@
  where
    tce :: TCEmb TyCon
tce            = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (TargetSpec -> GhcSpecNames
gsName TargetSpec
sp)
    tyi :: TyConMap
tyi            = GhcSpecNames -> TyConMap
gsTyconEnv (TargetSpec -> GhcSpecNames
gsName TargetSpec
sp)


--------------------------------------------------------------------------------
measEnv :: TargetSpec
        -> [(F.Symbol, SpecType)]
        -> [CoreBind]
        -> [(F.Symbol, F.Sort)]
        -> [(F.Symbol, F.Sort)]
        -> [(F.Symbol, F.Sort)]
        -> [(F.Symbol, SpecType)]
        -> [(F.Symbol, SpecType)]
        -> [F.Symbol]
        -> TargetInfo
        -> CGEnv
--------------------------------------------------------------------------------
measEnv :: TargetSpec
-> [(Symbol, SpecType)]
-> [CoreBind]
-> [(Symbol, Sort)]
-> [(Symbol, Sort)]
-> [(Symbol, Sort)]
-> [(Symbol, SpecType)]
-> [(Symbol, SpecType)]
-> [Symbol]
-> TargetInfo
-> CGEnv
measEnv TargetSpec
sp [(Symbol, SpecType)]
xts [CoreBind]
cbs [(Symbol, Sort)]
_tcb [(Symbol, Sort)]
lt1s [(Symbol, Sort)]
lt2s [(Symbol, SpecType)]
asms [(Symbol, SpecType)]
itys [Symbol]
hs TargetInfo
info = CGE
  { cgLoc :: SpanStack
cgLoc    = SpanStack
Sp.empty
  , renv :: REnv
renv     = [(Symbol, SpecType)] -> [(Symbol, SpecType)] -> REnv
fromListREnv (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas (TargetSpec -> GhcSpecData
gsData TargetSpec
sp)) []
  , syenv :: SEnv Var
syenv    = forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv (GhcSpecNames -> [(Symbol, Var)]
gsFreeSyms (TargetSpec -> GhcSpecNames
gsName TargetSpec
sp))
  , litEnv :: SEnv Sort
litEnv   = forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [(Symbol, Sort)]
lts
  , constEnv :: SEnv Sort
constEnv = forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [(Symbol, Sort)]
lt2s
  , fenv :: FEnv
fenv     = [(Symbol, Sort)] -> FEnv
initFEnv forall a b. (a -> b) -> a -> b
$ forall {a}. [(a, Sort)] -> [(a, Sort)]
filterHO (forall a. [a]
tcb' forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
lts forall a. [a] -> [a] -> [a]
++ (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas (TargetSpec -> GhcSpecData
gsData TargetSpec
sp)))
  , denv :: RDEnv
denv     = forall a b v. (a -> b) -> DEnv v a -> DEnv v b
dmapty forall a. Located a -> a
val forall a b. (a -> b) -> a -> b
$ GhcSpecSig -> DEnv Var LocSpecType
gsDicts (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp)
  , recs :: HashSet Var
recs     = forall a. HashSet a
S.empty
  , invs :: RTyConInv
invs     = forall a. Monoid a => a
mempty
  , rinvs :: RTyConInv
rinvs    = forall a. Monoid a => a
mempty
  , ial :: RTyConInv
ial      = forall a. [(a, LocSpecType)] -> RTyConInv
mkRTyConIAl (GhcSpecData -> [(LocSpecType, LocSpecType)]
gsIaliases (TargetSpec -> GhcSpecData
gsData TargetSpec
sp))
  , grtys :: REnv
grtys    = [(Symbol, SpecType)] -> [(Symbol, SpecType)] -> REnv
fromListREnv [(Symbol, SpecType)]
xts  []
  , assms :: REnv
assms    = [(Symbol, SpecType)] -> [(Symbol, SpecType)] -> REnv
fromListREnv [(Symbol, SpecType)]
asms []
  , intys :: REnv
intys    = [(Symbol, SpecType)] -> [(Symbol, SpecType)] -> REnv
fromListREnv [(Symbol, SpecType)]
itys []
  , emb :: TCEmb TyCon
emb      = TCEmb TyCon
tce
  , tgEnv :: TagEnv
tgEnv    = [CoreBind] -> TagEnv
Tg.makeTagEnv [CoreBind]
cbs
  , tgKey :: Maybe Var
tgKey    = forall a. Maybe a
Nothing
  , trec :: Maybe (HashMap Symbol SpecType)
trec     = forall a. Maybe a
Nothing
  , lcb :: HashMap Symbol CoreExpr
lcb      = forall k v. HashMap k v
M.empty
  , forallcb :: HashMap Var Expr
forallcb = forall k v. HashMap k v
M.empty
  , holes :: HEnv
holes    = [Symbol] -> HEnv
fromListHEnv [Symbol]
hs
  , lcs :: LConstraint
lcs      = forall a. Monoid a => a
mempty
  , cerr :: Maybe (TError SpecType)
cerr     = forall a. Maybe a
Nothing
  , cgInfo :: TargetInfo
cgInfo   = TargetInfo
info
  , cgVar :: Maybe Var
cgVar    = forall a. Maybe a
Nothing
  }
  where
      tce :: TCEmb TyCon
tce         = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (TargetSpec -> GhcSpecNames
gsName TargetSpec
sp)
      filterHO :: [(a, Sort)] -> [(a, Sort)]
filterHO [(a, Sort)]
xs = if forall t. HasConfig t => t -> Bool
higherOrderFlag TargetSpec
sp then [(a, Sort)]
xs else forall a. (a -> Bool) -> [a] -> [a]
filter (Sort -> Bool
F.isFirstOrder forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(a, Sort)]
xs
      lts :: [(Symbol, Sort)]
lts         = [(Symbol, Sort)]
lt1s forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
lt2s
      tcb' :: [a]
tcb'        = []


assm :: TargetInfo -> [(Var, SpecType)]
assm :: TargetInfo -> [(Var, SpecType)]
assm = (TargetInfo -> [Var]) -> TargetInfo -> [(Var, SpecType)]
assmGrty (TargetSrc -> [Var]
giImpVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSrc
giSrc)

grty :: TargetInfo -> [(Var, SpecType)]
grty :: TargetInfo -> [(Var, SpecType)]
grty = (TargetInfo -> [Var]) -> TargetInfo -> [(Var, SpecType)]
assmGrty (TargetSrc -> [Var]
giDefVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSrc
giSrc)

assmGrty :: (TargetInfo -> [Var]) -> TargetInfo -> [(Var, SpecType)]
assmGrty :: (TargetInfo -> [Var]) -> TargetInfo -> [(Var, SpecType)]
assmGrty TargetInfo -> [Var]
f TargetInfo
info = [ (Var
x, forall a. Located a -> a
val LocSpecType
t) | (Var
x, LocSpecType
t) <- [(Var, LocSpecType)]
sigs, Var
x forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Var
xs ]
  where
    xs :: HashSet Var
xs          = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> [Var]
f             forall a b. (a -> b) -> a -> b
$ TargetInfo
info
    sigs :: [(Var, LocSpecType)]
sigs        = GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs  forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecSig
gsSig forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec forall a b. (a -> b) -> a -> b
$ TargetInfo
info


recSelectorsTy :: TargetInfo -> CG [(Var, SpecType)]
recSelectorsTy :: TargetInfo -> StateT CGInfo Identity [(Var, SpecType)]
recSelectorsTy TargetInfo
info = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Var]
topVs forall a b. (a -> b) -> a -> b
$ \Var
v -> (Var
v,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig TargetInfo
info)) (Var -> Type
varType Var
v)
  where
    topVs :: [Var]
topVs        = forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isTop forall a b. (a -> b) -> a -> b
$ TargetSrc -> [Var]
giDefVars (TargetInfo -> TargetSrc
giSrc TargetInfo
info)
    isTop :: Var -> Bool
isTop Var
v      = TargetSrc -> Var -> Bool
isExportedVar (TargetInfo -> TargetSrc
giSrc TargetInfo
info) Var
v Bool -> Bool -> Bool
&& Bool -> Bool
not (Var
v forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Var
sigVs) Bool -> Bool -> Bool
&&  Var -> Bool
isRecordSelector Var
v
    sigVs :: HashSet Var
sigVs        = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Var
v | (Var
v,LocSpecType
_) <- GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
sp forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs GhcSpecSig
sp forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs GhcSpecSig
sp forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsInSigs GhcSpecSig
sp]
    sp :: GhcSpecSig
sp           = TargetSpec -> GhcSpecSig
gsSig forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec forall a b. (a -> b) -> a -> b
$ TargetInfo
info



grtyTop :: TargetInfo -> CG [(Var, SpecType)]
grtyTop :: TargetInfo -> StateT CGInfo Identity [(Var, SpecType)]
grtyTop TargetInfo
info     = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Var]
topVs forall a b. (a -> b) -> a -> b
$ \Var
v -> (Var
v,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig TargetInfo
info)) (Var -> Type
varType Var
v)
  where
    topVs :: [Var]
topVs        = forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isTop forall a b. (a -> b) -> a -> b
$ TargetSrc -> [Var]
giDefVars (TargetInfo -> TargetSrc
giSrc TargetInfo
info)
    isTop :: Var -> Bool
isTop Var
v      = TargetSrc -> Var -> Bool
isExportedVar (TargetInfo -> TargetSrc
giSrc TargetInfo
info) Var
v Bool -> Bool -> Bool
&& Bool -> Bool
not (Var
v forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Var
sigVs) Bool -> Bool -> Bool
&& Bool -> Bool
not (Var -> Bool
isRecordSelector Var
v)
    sigVs :: HashSet Var
sigVs        = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Var
v | (Var
v,LocSpecType
_) <- GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
sp forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs GhcSpecSig
sp forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs GhcSpecSig
sp forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsInSigs GhcSpecSig
sp]
    sp :: GhcSpecSig
sp           = TargetSpec -> GhcSpecSig
gsSig forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec forall a b. (a -> b) -> a -> b
$ TargetInfo
info


infoLits :: (TargetSpec -> [(F.Symbol, LocSpecType)]) -> (F.Sort -> Bool) -> TargetInfo -> F.SEnv F.Sort
infoLits :: (TargetSpec -> [(Symbol, LocSpecType)])
-> (Sort -> Bool) -> TargetInfo -> SEnv Sort
infoLits TargetSpec -> [(Symbol, LocSpecType)]
litF Sort -> Bool
selF TargetInfo
info = forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv forall a b. (a -> b) -> a -> b
$ [(Symbol, Sort)]
cbLits forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
measLits
  where
    cbLits :: [(Symbol, Sort)]
cbLits    = forall a. (a -> Bool) -> [a] -> [a]
filter (Sort -> Bool
selF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ TCEmb TyCon -> TargetInfo -> [(Symbol, Sort)]
coreBindLits TCEmb TyCon
tce TargetInfo
info
    measLits :: [(Symbol, Sort)]
measLits  = forall a. (a -> Bool) -> [a] -> [a]
filter (Sort -> Bool
selF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall {r} {a}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
(a, Located (RRType r)) -> (a, Sort)
mkSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TargetSpec -> [(Symbol, LocSpecType)]
litF TargetSpec
spc
    spc :: TargetSpec
spc       = TargetInfo -> TargetSpec
giSpec TargetInfo
info
    tce :: TCEmb TyCon
tce       = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (TargetSpec -> GhcSpecNames
gsName TargetSpec
spc)
    mkSort :: (a, Located (RRType r)) -> (a, Sort)
mkSort    = forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (SortedReft -> Sort
F.sr_sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
tce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val)

initCGI :: Config -> TargetInfo -> CGInfo
initCGI :: Config -> TargetInfo -> CGInfo
initCGI Config
cfg TargetInfo
info = CGInfo {
    fEnv :: SEnv Sort
fEnv       = forall a. SEnv a
F.emptySEnv
  , hsCs :: [SubC]
hsCs       = []
  , hsWfs :: [WfC]
hsWfs      = []
  , fixCs :: [FixSubC]
fixCs      = []
  , fixWfs :: [FixWfC]
fixWfs     = []
  , freshIndex :: Integer
freshIndex = Integer
0
  , dataConTys :: [(Var, SpecType)]
dataConTys = []
  , binds :: FixBindEnv
binds      = forall a. BindEnv a
F.emptyBindEnv
  , ebinds :: [Int]
ebinds     = []
  , annotMap :: AnnInfo (Annot SpecType)
annotMap   = forall a. HashMap SrcSpan [(Maybe Text, a)] -> AnnInfo a
AI forall k v. HashMap k v
M.empty
  , newTyEnv :: HashMap TyCon SpecType
newTyEnv   = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyCon, LocSpecType)]
gsNewTypes (TargetSpec -> GhcSpecSig
gsSig TargetSpec
spc))
  , tyConInfo :: TyConMap
tyConInfo  = TyConMap
tyi
  , tyConEmbed :: TCEmb TyCon
tyConEmbed = TCEmb TyCon
tce
  , kuts :: Kuts
kuts       = forall a. Monoid a => a
mempty
  , kvPacks :: [HashSet KVar]
kvPacks    = forall a. Monoid a => a
mempty
  , cgLits :: SEnv Sort
cgLits     = (TargetSpec -> [(Symbol, LocSpecType)])
-> (Sort -> Bool) -> TargetInfo -> SEnv Sort
infoLits (GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecData
gsData) (forall a b. a -> b -> a
const Bool
True) TargetInfo
info
  , cgConsts :: SEnv Sort
cgConsts   = (TargetSpec -> [(Symbol, LocSpecType)])
-> (Sort -> Bool) -> TargetInfo -> SEnv Sort
infoLits (GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecData
gsData) Sort -> Bool
notFn        TargetInfo
info
  , cgADTs :: [DataDecl]
cgADTs     = GhcSpecNames -> [DataDecl]
gsADTs GhcSpecNames
nspc
  , termExprs :: HashMap Var [Located Expr]
termExprs  = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Var
v, [Located Expr]
es) | (Var
v, LocSpecType
_, [Located Expr]
es) <- GhcSpecSig -> [(Var, LocSpecType, [Located Expr])]
gsTexprs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
spc) ]
  , specLVars :: HashSet Var
specLVars  = GhcSpecVars -> HashSet Var
gsLvars (TargetSpec -> GhcSpecVars
gsVars TargetSpec
spc)
  , specLazy :: HashSet Var
specLazy   = Var
dictionaryVar forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
`S.insert` GhcSpecTerm -> HashSet Var
gsLazy GhcSpecTerm
tspc
  , specTmVars :: HashSet Var
specTmVars = GhcSpecTerm -> HashSet Var
gsNonStTerm GhcSpecTerm
tspc
  , tcheck :: Bool
tcheck     = forall t. HasConfig t => t -> Bool
terminationCheck Config
cfg
  , cgiTypeclass :: Bool
cgiTypeclass = Config -> Bool
typeclass Config
cfg
  , pruneRefs :: Bool
pruneRefs  = Config -> Bool
pruneUnsorted Config
cfg
  , logErrors :: [TError SpecType]
logErrors  = []
  , kvProf :: KVProf
kvProf     = KVProf
emptyKVProf
  , recCount :: Int
recCount   = Int
0
  , bindSpans :: HashMap Int SrcSpan
bindSpans  = forall k v. HashMap k v
M.empty
  , autoSize :: HashSet TyCon
autoSize   = GhcSpecTerm -> HashSet TyCon
gsAutosize GhcSpecTerm
tspc
  , allowHO :: Bool
allowHO    = forall t. HasConfig t => t -> Bool
higherOrderFlag Config
cfg
  , ghcI :: TargetInfo
ghcI       = TargetInfo
info
  , unsorted :: Templates
unsorted   = forall a. PPrint a => String -> a -> a
F.notracepp String
"UNSORTED" forall a b. (a -> b) -> a -> b
$ [([Symbol], Expr)] -> Templates
F.makeTemplates forall a b. (a -> b) -> a -> b
$ GhcSpecData -> [([Symbol], Expr)]
gsUnsorted forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecData
gsData TargetSpec
spc
  }
  where
    tce :: TCEmb TyCon
tce        = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds GhcSpecNames
nspc
    tspc :: GhcSpecTerm
tspc       = TargetSpec -> GhcSpecTerm
gsTerm TargetSpec
spc
    spc :: TargetSpec
spc        = TargetInfo -> TargetSpec
giSpec TargetInfo
info
    tyi :: TyConMap
tyi        = GhcSpecNames -> TyConMap
gsTyconEnv GhcSpecNames
nspc
    nspc :: GhcSpecNames
nspc       = TargetSpec -> GhcSpecNames
gsName TargetSpec
spc
    notFn :: Sort -> Bool
notFn      = forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Maybe ([Int], [Sort], Sort)
F.functionSort

coreBindLits :: F.TCEmb TyCon -> TargetInfo -> [(F.Symbol, F.Sort)]
coreBindLits :: TCEmb TyCon -> TargetInfo -> [(Symbol, Sort)]
coreBindLits TCEmb TyCon
tce TargetInfo
info
  = forall a. Ord a => [a] -> [a]
sortNub      forall a b. (a -> b) -> a -> b
$ [ (forall a. Symbolic a => a -> Symbol
F.symbol SymConst
x, Sort
F.strSort) | (Sort
_, Just (F.ESym SymConst
x)) <- [(Sort, Maybe Expr)]
lconsts ]    -- strings
                forall a. [a] -> [a] -> [a]
++ [ (Var -> Symbol
dconToSym Var
dc, Var -> Sort
dconToSort Var
dc) | Var
dc <- [Var]
dcons ]                  -- data constructors
  where
    src :: TargetSrc
src         = TargetInfo -> TargetSrc
giSrc TargetInfo
info
    lconsts :: [(Sort, Maybe Expr)]
lconsts      = TCEmb TyCon -> Literal -> (Sort, Maybe Expr)
literalConst TCEmb TyCon
tce forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. CBVisitable a => a -> [Literal]
literals (TargetSrc -> [CoreBind]
giCbs TargetSrc
src)
    dcons :: [Var]
dcons        = forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isDCon [Var]
freeVs
    freeVs :: [Var]
freeVs       = TargetSrc -> [Var]
giImpVars TargetSrc
src forall a. [a] -> [a] -> [a]
++ [Var]
freeSyms
    freeSyms :: [Var]
freeSyms     = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSpecNames -> [(Symbol, Var)]
gsFreeSyms forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecNames
gsName forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec forall a b. (a -> b) -> a -> b
$ TargetInfo
info
    dconToSort :: Var -> Sort
dconToSort   = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
expandTypeSynonyms forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type
varType
    dconToSym :: Var -> Symbol
dconToSym    = forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> DataCon
idDataCon
    isDCon :: Var -> Bool
isDCon Var
x     = Var -> Bool
isDataConId Var
x Bool -> Bool -> Bool
&& Bool -> Bool
not (Var -> Bool
hasBaseTypeVar Var
x)