{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# OPTIONS_GHC -Wno-x-partial #-}

-- | 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 (foldM, forM)
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.Fixpoint.Misc
import           Language.Haskell.Liquid.Constraint.Types

import           Language.Haskell.Liquid.Types.Dictionaries
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Fresh
import           Language.Haskell.Liquid.Types.Literals
import           Language.Haskell.Liquid.Types.Meet
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types hiding (binds)
import           Language.Haskell.Liquid.Types.Visitors
import           Language.Haskell.Liquid.UX.Config

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

    makeExactDc :: [(Var, SpecType)] -> [(Var, SpecType)]
makeExactDc [(Var, SpecType)]
dcs = if TargetInfo -> Bool
forall t. HasConfig t => t -> Bool
exactDCFlag TargetInfo
info then ((Var, SpecType) -> (Var, SpecType))
-> [(Var, SpecType)] -> [(Var, SpecType)]
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 = [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [PVarV Symbol (RType RTyCon RTyVar ())] -> SpecType -> SpecType
forall (t :: * -> *) (t1 :: * -> *) tv v c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RTypeV v c tv ()), r)
-> t1 (PVarV v (RTypeV v c tv ()))
-> RTypeV v c tv r
-> RTypeV v c tv r
mkUnivs ((RTVar RTyVar (RType RTyCon RTyVar ()), RReft)
-> (RTVar RTyVar (RType RTyCon RTyVar ()), RReft)
forall {a} {b}. (RTVar RTyVar a, b) -> (RTVar RTyVar a, b)
go ((RTVar RTyVar (RType RTyCon RTyVar ()), RReft)
 -> (RTVar RTyVar (RType RTyCon RTyVar ()), RReft))
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
as) [PVarV Symbol (RType RTyCon RTyVar ())]
ps SpecType
t'
  where
    ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
as, [PVarV Symbol (RType RTyCon RTyVar ())]
ps, SpecType
t') = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
    [PVarV Symbol (RType RTyCon RTyVar ())], SpecType)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv SpecType
t
    pos :: Positions RTyVar
pos          = SpecType -> Positions RTyVar
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 && -}  RTVar RTyVar a -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar a
a RTyVar -> [RTyVar] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Positions RTyVar -> [RTyVar]
forall a. Positions a -> [a]
pneg Positions RTyVar
pos
               then (RTVar RTyVar a -> Bool -> RTVar RTyVar a
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,) (SpecType -> (Var, SpecType))
-> StateT CGInfo Identity SpecType
-> StateT CGInfo Identity (Var, SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Type -> StateT CGInfo Identity 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
  = ([RType RTyCon RTyVar ()] -> [LocSpecType]
forall {v} {tv} {v} {c} {a}.
(Reftable (UReftV v (ReftV Symbol)), Monoid (PredicateV v), Eq tv,
 Eq v, Eq c, Eq a) =>
[RTypeV v c tv a]
-> [Located (RTypeV v c tv (UReftV v (ReftV Symbol)))]
simplify [RType RTyCon RTyVar ()]
rsorts, [(Var, SpecType)]
tys)
  where
    ([RType RTyCon RTyVar ()]
rsorts, [(Var, SpecType)]
tys) = [(RType RTyCon RTyVar (), (Var, SpecType))]
-> ([RType RTyCon RTyVar ()], [(Var, SpecType)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(RType RTyCon RTyVar (), (Var, SpecType))]
 -> ([RType RTyCon RTyVar ()], [(Var, SpecType)]))
-> [(RType RTyCon RTyVar (), (Var, SpecType))]
-> ([RType RTyCon RTyVar ()], [(Var, SpecType)])
forall a b. (a -> b) -> a -> b
$ (TyCon -> [(RType RTyCon RTyVar (), (Var, SpecType))])
-> [TyCon] -> [(RType RTyCon RTyVar (), (Var, SpecType))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TyCon -> [(RType RTyCon RTyVar (), (Var, SpecType))]
go [TyCon]
tycons
    tycons :: [TyCon]
tycons      = [TyCon] -> [TyCon]
forall a. Eq a => [a] -> [a]
L.nub ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ (Var -> Maybe TyCon) -> [Var] -> [TyCon]
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
      | TyCon -> HashSet TyCon -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member TyCon
tycon HashSet TyCon
specenv =  (DataCon -> Integer -> (RType RTyCon RTyVar (), (Var, SpecType)))
-> [DataCon]
-> [Integer]
-> [(RType RTyCon RTyVar (), (Var, SpecType))]
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 :: [RTypeV v c tv a]
-> [Located (RTypeV v c tv (UReftV v (ReftV Symbol)))]
simplify [RTypeV v c tv a]
invs = RTypeV v c tv (UReftV v (ReftV Symbol))
-> Located (RTypeV v c tv (UReftV v (ReftV Symbol)))
forall a. a -> Located a
dummyLoc (RTypeV v c tv (UReftV v (ReftV Symbol))
 -> Located (RTypeV v c tv (UReftV v (ReftV Symbol))))
-> (RTypeV v c tv a -> RTypeV v c tv (UReftV v (ReftV Symbol)))
-> RTypeV v c tv a
-> Located (RTypeV v c tv (UReftV v (ReftV Symbol)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RTypeV v c tv (UReftV v (ReftV Symbol))
-> UReftV v (ReftV Symbol)
-> RTypeV v c tv (UReftV v (ReftV Symbol))
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`strengthen` UReftV v (ReftV Symbol)
forall {v}. Monoid (PredicateV v) => UReftV v (ReftV Symbol)
invariant) (RTypeV v c tv (UReftV v (ReftV Symbol))
 -> RTypeV v c tv (UReftV v (ReftV Symbol)))
-> (RTypeV v c tv a -> RTypeV v c tv (UReftV v (ReftV Symbol)))
-> RTypeV v c tv a
-> RTypeV v c tv (UReftV v (ReftV Symbol))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (a -> UReftV v (ReftV Symbol))
-> RTypeV v c tv a -> RTypeV v c tv (UReftV v (ReftV Symbol))
forall a b. (a -> b) -> RTypeV v c tv a -> RTypeV v c tv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (UReftV v (ReftV Symbol) -> a -> UReftV v (ReftV Symbol)
forall a b. a -> b -> a
const UReftV v (ReftV Symbol)
forall a. Monoid a => a
mempty) (RTypeV v c tv a
 -> Located (RTypeV v c tv (UReftV v (ReftV Symbol))))
-> [RTypeV v c tv a]
-> [Located (RTypeV v c tv (UReftV v (ReftV Symbol)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeV v c tv a] -> [RTypeV v c tv a]
forall a. Eq a => [a] -> [a]
L.nub [RTypeV v c tv a]
invs
    invariant :: UReftV v (ReftV Symbol)
invariant = ReftV Symbol -> PredicateV v -> UReftV v (ReftV Symbol)
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
F.vv_, Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
F.PAtom Brel
F.Ge (Symbol -> Expr
lenOf Symbol
F.vv_) (Constant -> Expr
forall v. Constant -> ExprV v
F.ECon (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Constant
F.I Integer
0)) ) PredicateV v
forall a. Monoid a => a
mempty

idTyCon :: Id -> Maybe TyCon
idTyCon :: Var -> Maybe TyCon
idTyCon = (DataCon -> TyCon) -> Maybe DataCon -> Maybe TyCon
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TyCon
dataConTyCon (Maybe DataCon -> Maybe TyCon)
-> (Var -> Maybe DataCon) -> Var -> Maybe TyCon
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
forall v. v -> ExprV v
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 = (SpecType -> RType RTyCon RTyVar ()
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv ()
toRSort (SpecType -> RType RTyCon RTyVar ())
-> SpecType -> RType RTyCon RTyVar ()
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res RTypeRepV Symbol RTyCon RTyVar RReft
trep, (Var
x, RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep RTypeRepV Symbol RTyCon RTyVar RReft
trep{ty_res = tres}))
    where
      x :: Var
x      = DataCon -> Var
dataConWorkId DataCon
x'
      st :: SpecType
st     = SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
fromMaybe (Maybe SrcSpan -> String -> SpecType
forall a. Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing String
"makeSizedDataCons: this should never happen") (Maybe SpecType -> SpecType) -> Maybe SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ Var -> [(Var, SpecType)] -> Maybe SpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Var
x [(Var, SpecType)]
dcts
      trep :: RTypeRepV Symbol RTyCon RTyVar RReft
trep   = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
st
      tres :: SpecType
tres   = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res RTypeRepV Symbol RTyCon RTyVar RReft
trep SpecType -> RReft -> SpecType
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`strengthen` ReftV Symbol -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
F.vv_, Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
F.PAtom Brel
F.Eq (Symbol -> Expr
lenOf Symbol
F.vv_) Expr
computelen)) PredicateV Symbol
forall a. Monoid a => a
mempty

      recarguments :: [(SpecType, Symbol)]
recarguments = ((SpecType, Symbol) -> Bool)
-> [(SpecType, Symbol)] -> [(SpecType, Symbol)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(SpecType
t,Symbol
_) -> SpecType -> RType RTyCon RTyVar ()
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv ()
toRSort SpecType
t RType RTyCon RTyVar () -> RType RTyCon RTyVar () -> Bool
forall a. Eq a => a -> a -> Bool
== SpecType -> RType RTyCon RTyVar ()
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv ()
toRSort SpecType
tres) ([SpecType] -> [Symbol] -> [(SpecType, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRepV Symbol RTyCon RTyVar RReft -> [SpecType]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar RReft
trep) (RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar RReft
trep))
      computelen :: Expr
computelen   = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
F.EBin Bop
F.Plus) (Constant -> Expr
forall v. Constant -> ExprV v
F.ECon (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Constant
F.I Integer
n) (Symbol -> Expr
lenOf (Symbol -> Expr)
-> ((SpecType, Symbol) -> Symbol) -> (SpecType, Symbol) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (SpecType, Symbol) -> Symbol
forall a b. (a, b) -> b
snd ((SpecType, Symbol) -> Expr) -> [(SpecType, Symbol)] -> [Expr]
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 = [(Var, SpecType)] -> [(Var, SpecType)] -> [(Var, SpecType)]
forall {a}.
(PPrint a, NamedThing a, Ord a) =>
[(a, SpecType)] -> [(a, SpecType)] -> [(a, SpecType)]
merge (((Var, SpecType) -> (Var, SpecType) -> Ordering)
-> [(Var, SpecType)] -> [(Var, SpecType)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (Var, SpecType) -> (Var, SpecType) -> Ordering
forall {a} {b} {b}. Ord a => (a, b) -> (a, b) -> Ordering
f [(Var, SpecType)]
xts) (((Var, SpecType) -> (Var, SpecType) -> Ordering)
-> [(Var, SpecType)] -> [(Var, SpecType)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (Var, SpecType) -> (Var, SpecType) -> Ordering
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
_) = a -> a -> Ordering
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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y    = (a
x, a -> SpecType -> a -> SpecType -> SpecType
forall {a} {a}.
(PPrint a, NamedThing a, NamedThing a) =>
a -> SpecType -> a -> SpecType -> SpecType
mXY a
x SpecType
tx a
y SpecType
ty) (a, SpecType) -> [(a, SpecType)] -> [(a, SpecType)]
forall a. a -> [a] -> [a]
: [(a, SpecType)] -> [(a, SpecType)] -> [(a, SpecType)]
merge [(a, SpecType)]
xs [(a, SpecType)]
ys
      | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<  a
y    = (a, SpecType)
xt (a, SpecType) -> [(a, SpecType)] -> [(a, SpecType)]
forall a. a -> [a] -> [a]
: [(a, SpecType)] -> [(a, SpecType)] -> [(a, SpecType)]
merge [(a, SpecType)]
xs ((a, SpecType)
yt (a, SpecType) -> [(a, SpecType)] -> [(a, SpecType)]
forall a. a -> [a] -> [a]
: [(a, SpecType)]
ys)
      | Bool
otherwise = (a, SpecType)
yt (a, SpecType) -> [(a, SpecType)] -> [(a, SpecType)]
forall a. a -> [a] -> [a]
: [(a, SpecType)] -> [(a, SpecType)] -> [(a, SpecType)]
merge ((a, SpecType)
xt (a, SpecType) -> [(a, SpecType)] -> [(a, SpecType)]
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 (a -> Doc
forall a. PPrint a => a -> Doc
F.pprint a
x) (a -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan a
x, SpecType
tx) (a -> SrcSpan
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' = ((a, SpecType) -> StateT CGInfo Identity (a, SpecType))
-> [(a, SpecType)] -> StateT CGInfo Identity [(a, SpecType)]
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 ((SpecType -> StateT CGInfo Identity SpecType)
-> (a, SpecType) -> StateT CGInfo Identity (a, SpecType)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (a, a) -> f (a, b)
traverse SpecType -> StateT CGInfo Identity SpecType
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 = (SpecType -> SpecType) -> (Var, SpecType) -> (Var, SpecType)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (TCEmb TyCon -> TyConMap -> SpecType -> SpecType
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 ((LocSpecType -> SpecType)
-> (Symbol, LocSpecType) -> (Symbol, SpecType)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second LocSpecType -> SpecType
forall a. Located a -> a
val ((Symbol, LocSpecType) -> (Symbol, SpecType))
-> [(Symbol, LocSpecType)] -> [(Symbol, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas (TargetSpec -> GhcSpecData
gsData TargetSpec
sp)) []
  , litEnv :: SEnv Sort
litEnv   = [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [(Symbol, Sort)]
lts
  , constEnv :: SEnv Sort
constEnv = [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [(Symbol, Sort)]
lt2s
  , fenv :: FEnv
fenv     =
      [(Symbol, Sort)] -> FEnv
initFEnv ([(Symbol, Sort)] -> FEnv) -> [(Symbol, Sort)] -> FEnv
forall a b. (a -> b) -> a -> b
$ [(Symbol, Sort)] -> [(Symbol, Sort)]
forall {a}. [(a, Sort)] -> [(a, Sort)]
filterHO ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ [[(Symbol, Sort)]] -> [(Symbol, Sort)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [(Symbol, Sort)]
forall a. [a]
tcb'
        , [(Symbol, Sort)]
lts
        , (LocSpecType -> Sort) -> (Symbol, LocSpecType) -> (Symbol, Sort)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (TCEmb TyCon -> SpecType -> Sort
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 -> Sort)
-> (LocSpecType -> SpecType) -> LocSpecType -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSpecType -> SpecType
forall a. Located a -> a
val) ((Symbol, LocSpecType) -> (Symbol, Sort))
-> [(Symbol, LocSpecType)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas (TargetSpec -> GhcSpecData
gsData TargetSpec
sp)
        , [(EquationV Symbol -> Symbol
forall v. EquationV v -> Symbol
F.eqName EquationV Symbol
e, EquationV Symbol -> Sort
forall v. EquationV v -> Sort
eqSort EquationV Symbol
e) | EquationV Symbol
e <- GhcSpecRefl -> [EquationV Symbol]
gsImpAxioms (TargetSpec -> GhcSpecRefl
gsRefl TargetSpec
sp)]
        ]
  , denv :: RDEnv
denv     = (LocSpecType -> SpecType) -> DEnv Var LocSpecType -> RDEnv
forall a b v. (a -> b) -> DEnv v a -> DEnv v b
dmapty LocSpecType -> SpecType
forall a. Located a -> a
val (DEnv Var LocSpecType -> RDEnv) -> DEnv Var LocSpecType -> RDEnv
forall a b. (a -> b) -> a -> b
$ GhcSpecSig -> DEnv Var LocSpecType
gsDicts (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp)
  , recs :: HashSet Var
recs     = HashSet Var
forall a. HashSet a
S.empty
  , invs :: RTyConInv
invs     = RTyConInv
forall a. Monoid a => a
mempty
  , rinvs :: RTyConInv
rinvs    = RTyConInv
forall a. Monoid a => a
mempty
  , ial :: RTyConInv
ial      = [(LocSpecType, LocSpecType)] -> RTyConInv
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    = Maybe Var
forall a. Maybe a
Nothing
  , trec :: Maybe (HashMap Symbol SpecType)
trec     = Maybe (HashMap Symbol SpecType)
forall a. Maybe a
Nothing
  , lcb :: HashMap Symbol CoreExpr
lcb      = HashMap Symbol CoreExpr
forall k v. HashMap k v
M.empty
  , forallcb :: HashMap Var Expr
forallcb = HashMap Var Expr
forall k v. HashMap k v
M.empty
  , holes :: HEnv
holes    = [Symbol] -> HEnv
fromListHEnv [Symbol]
hs
  , lcs :: LConstraint
lcs      = LConstraint
forall a. Monoid a => a
mempty
  , cerr :: Maybe (TError SpecType)
cerr     = Maybe (TError SpecType)
forall a. Maybe a
Nothing
  , cgInfo :: TargetInfo
cgInfo   = TargetInfo
info
  , cgVar :: Maybe Var
cgVar    = Maybe Var
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 TargetSpec -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag TargetSpec
sp then [(a, Sort)]
xs else ((a, Sort) -> Bool) -> [(a, Sort)] -> [(a, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Sort -> Bool
F.isFirstOrder (Sort -> Bool) -> ((a, Sort) -> Sort) -> (a, Sort) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Sort) -> Sort
forall a b. (a, b) -> b
snd) [(a, Sort)]
xs
      lts :: [(Symbol, Sort)]
lts         = [(Symbol, Sort)]
lt1s [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
lt2s
      tcb' :: [a]
tcb'        = []

-- | Constructs the sort of an equation
eqSort :: F.EquationV v -> F.Sort
eqSort :: forall v. EquationV v -> Sort
eqSort EquationV v
e  = ((Symbol, Sort) -> Sort -> Sort)
-> Sort -> [(Symbol, Sort)] -> Sort
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Sort -> Sort -> Sort
F.FFunc (Sort -> Sort -> Sort)
-> ((Symbol, Sort) -> Sort) -> (Symbol, Sort) -> Sort -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Sort
forall a b. (a, b) -> b
snd) (EquationV v -> Sort
forall v. EquationV v -> Sort
F.eqSort EquationV v
e) (EquationV v -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
F.eqArgs EquationV v
e)

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


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



grtyTop :: TargetInfo -> CG [(Var, SpecType)]
grtyTop :: TargetInfo -> StateT CGInfo Identity [(Var, SpecType)]
grtyTop TargetInfo
info     = [Var]
-> (Var -> StateT CGInfo Identity (Var, SpecType))
-> StateT CGInfo Identity [(Var, SpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Var]
topVs ((Var -> StateT CGInfo Identity (Var, SpecType))
 -> StateT CGInfo Identity [(Var, SpecType)])
-> (Var -> StateT CGInfo Identity (Var, SpecType))
-> StateT CGInfo Identity [(Var, SpecType)]
forall a b. (a -> b) -> a -> b
$ \Var
v -> (Var
v,) (SpecType -> (Var, SpecType))
-> StateT CGInfo Identity SpecType
-> StateT CGInfo Identity (Var, SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Type -> StateT CGInfo Identity SpecType
trueTy (Config -> Bool
typeclass (TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig TargetInfo
info)) (Var -> Type
varType Var
v)
  where
    topVs :: [Var]
topVs        = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isTop ([Var] -> [Var]) -> [Var] -> [Var]
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 Var -> HashSet Var -> Bool
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        = [Var] -> HashSet Var
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Var
v | (Var
v,LocSpecType
_) <- GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
sp [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs GhcSpecSig
sp [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs GhcSpecSig
sp [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsInSigs GhcSpecSig
sp]
    sp :: GhcSpecSig
sp           = TargetSpec -> GhcSpecSig
gsSig (TargetSpec -> GhcSpecSig)
-> (TargetInfo -> TargetSpec) -> TargetInfo -> GhcSpecSig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec (TargetInfo -> GhcSpecSig) -> TargetInfo -> GhcSpecSig
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 = [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv ([(Symbol, Sort)] -> SEnv Sort) -> [(Symbol, Sort)] -> SEnv Sort
forall a b. (a -> b) -> a -> b
$ [(Symbol, Sort)]
cbLits [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
measLits
  where
    cbLits :: [(Symbol, Sort)]
cbLits    = ((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Sort -> Bool
selF (Sort -> Bool)
-> ((Symbol, Sort) -> Sort) -> (Symbol, Sort) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Sort
forall a b. (a, b) -> b
snd) ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon -> TargetInfo -> [(Symbol, Sort)]
coreBindLits TCEmb TyCon
tce TargetInfo
info
    measLits :: [(Symbol, Sort)]
measLits  = ((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Sort -> Bool
selF (Sort -> Bool)
-> ((Symbol, Sort) -> Sort) -> (Symbol, Sort) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Sort
forall a b. (a, b) -> b
snd) ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ (Symbol, LocSpecType) -> (Symbol, Sort)
forall {f :: * -> *} {r}.
(Functor f, PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable r, Reftable (RTProp RTyCon RTyVar r)) =>
f (Located (RRType r)) -> f Sort
mkSort ((Symbol, LocSpecType) -> (Symbol, Sort))
-> [(Symbol, LocSpecType)] -> [(Symbol, Sort)]
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 :: f (Located (RRType r)) -> f Sort
mkSort    = (Located (RRType r) -> Sort) -> f (Located (RRType r)) -> f Sort
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SortedReft -> Sort
F.sr_sort (SortedReft -> Sort)
-> (Located (RRType r) -> SortedReft) -> Located (RRType r) -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> RRType r -> SortedReft
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 (RRType r -> SortedReft)
-> (Located (RRType r) -> RRType r)
-> Located (RRType r)
-> SortedReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RRType r) -> RRType r
forall a. Located a -> a
val)

initCGI :: Config -> TargetInfo -> CGInfo
initCGI :: Config -> TargetInfo -> CGInfo
initCGI Config
cfg TargetInfo
info = CGInfo {
    fEnv :: SEnv Sort
fEnv          = SEnv Sort
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         = FixBindEnv
forall a. BindEnv a
F.emptyBindEnv
  , localRewrites :: LocalRewritesEnv
localRewrites = LocalRewritesEnv
forall a. Monoid a => a
mempty
  , ebinds :: [Int]
ebinds        = []
  , annotMap :: AnnInfo (Annot SpecType)
annotMap      = HashMap SrcSpan [(Maybe Text, Annot SpecType)]
-> AnnInfo (Annot SpecType)
forall a. HashMap SrcSpan [(Maybe Text, a)] -> AnnInfo a
AI HashMap SrcSpan [(Maybe Text, Annot SpecType)]
forall k v. HashMap k v
M.empty
  , newTyEnv :: HashMap TyCon SpecType
newTyEnv      = [(TyCon, SpecType)] -> HashMap TyCon SpecType
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ((LocSpecType -> SpecType)
-> (TyCon, LocSpecType) -> (TyCon, SpecType)
forall a b. (a -> b) -> (TyCon, a) -> (TyCon, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LocSpecType -> SpecType
forall a. Located a -> a
val ((TyCon, LocSpecType) -> (TyCon, SpecType))
-> [(TyCon, LocSpecType)] -> [(TyCon, SpecType)]
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          = Kuts
forall a. Monoid a => a
mempty
  , kvPacks :: [HashSet KVar]
kvPacks       = [HashSet KVar]
forall a. Monoid a => a
mempty
  , cgLits :: SEnv Sort
cgLits        = (TargetSpec -> [(Symbol, LocSpecType)])
-> (Sort -> Bool) -> TargetInfo -> SEnv Sort
infoLits (GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas (GhcSpecData -> [(Symbol, LocSpecType)])
-> (TargetSpec -> GhcSpecData)
-> TargetSpec
-> [(Symbol, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecData
gsData) (Bool -> Sort -> Bool
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 (GhcSpecData -> [(Symbol, LocSpecType)])
-> (TargetSpec -> GhcSpecData)
-> TargetSpec
-> [(Symbol, LocSpecType)]
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     = [(Var, [Located Expr])] -> HashMap Var [Located Expr]
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 Var -> HashSet Var -> HashSet Var
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        = Config -> Bool
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     = HashMap Int SrcSpan
forall k v. HashMap k v
M.empty
  , autoSize :: HashSet TyCon
autoSize      = GhcSpecTerm -> HashSet TyCon
gsAutosize GhcSpecTerm
tspc
  , allowHO :: Bool
allowHO       = Config -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag Config
cfg
  , ghcI :: TargetInfo
ghcI          = TargetInfo
info
  , unsorted :: Templates
unsorted      = String -> Templates -> Templates
forall a. PPrint a => String -> a -> a
F.notracepp String
"UNSORTED" (Templates -> Templates) -> Templates -> Templates
forall a b. (a -> b) -> a -> b
$ [([Symbol], Expr)] -> Templates
F.makeTemplates ([([Symbol], Expr)] -> Templates)
-> [([Symbol], Expr)] -> Templates
forall a b. (a -> b) -> a -> b
$ GhcSpecData -> [([Symbol], Expr)]
gsUnsorted (GhcSpecData -> [([Symbol], Expr)])
-> GhcSpecData -> [([Symbol], Expr)]
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      = Maybe ([Int], [Sort], Sort) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe ([Int], [Sort], Sort) -> Bool)
-> (Sort -> Maybe ([Int], [Sort], Sort)) -> Sort -> Bool
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
  = [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. Ord a => [a] -> [a]
sortNub      ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ [ (SymConst -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol SymConst
x, Sort
F.strSort) | (Sort
_, Just (F.ESym SymConst
x)) <- [(Sort, Maybe Expr)]
lconsts ]    -- strings
                [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
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 (Literal -> (Sort, Maybe Expr))
-> [Literal] -> [(Sort, Maybe Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreBind] -> [Literal]
forall a. CBVisitable a => a -> [Literal]
literals (TargetSrc -> [CoreBind]
giCbs TargetSrc
src)
    dcons :: [Var]
dcons        = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isDCon ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$ GhcSpecNames -> [Var]
gsDataConIds (GhcSpecNames -> [Var]) -> GhcSpecNames -> [Var]
forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecNames
gsName (TargetSpec -> GhcSpecNames) -> TargetSpec -> GhcSpecNames
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSpec
giSpec TargetInfo
info
    dconToSort :: Var -> Sort
dconToSort   = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce (Type -> Sort) -> (Var -> Type) -> Var -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
expandTypeSynonyms (Type -> Type) -> (Var -> Type) -> Var -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type
varType
    dconToSym :: Var -> Symbol
dconToSym    = DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DataCon -> Symbol) -> (Var -> DataCon) -> Var -> 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)