{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
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)
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 = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isConLikeId ((Symbol, Var) -> Var
forall a b. (a, b) -> b
snd ((Symbol, Var) -> Var) -> [(Symbol, Var)] -> [Var]
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' = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isConLikeId [Var]
fVars
[(Var, SpecType)]
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)
[(Var, SpecType)]
dcsty <- [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]
dcs (Bool -> Var -> StateT CGInfo Identity (Var, SpecType)
makeDataConTypes Bool
allowTC)
[(Var, SpecType)]
dcsty' <- [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]
dcs' (Bool -> Var -> StateT CGInfo Identity (Var, SpecType)
makeDataConTypes Bool
allowTC)
([Symbol]
hs,[(Var, SpecType)]
f0) <- Bool
-> [(Var, SpecType)]
-> StateT CGInfo Identity ([Symbol], [(Var, SpecType)])
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 ([(Var, SpecType)]
-> StateT CGInfo Identity ([Symbol], [(Var, SpecType)]))
-> [(Var, SpecType)]
-> StateT CGInfo Identity ([Symbol], [(Var, SpecType)])
forall a b. (a -> b) -> a -> b
$ TargetInfo -> [(Var, SpecType)]
grty TargetInfo
info
[(Var, SpecType)]
f0'' <- [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' ([(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)])
-> StateT CGInfo Identity [(Var, SpecType)]
-> StateT CGInfo Identity [(Var, SpecType)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TargetInfo -> StateT CGInfo Identity [(Var, SpecType)]
grtyTop TargetInfo
info
let f0' :: [(Var, SpecType)]
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''
[(Var, SpecType)]
f1 <- [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' [(Var, SpecType)]
defaults
[(Var, SpecType)]
f1' <- [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' ([(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)])
-> [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a b. (a -> b) -> a -> b
$ [(Var, SpecType)] -> [(Var, SpecType)]
makeExactDc [(Var, SpecType)]
dcsty
[(Var, SpecType)]
f2 <- [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' ([(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)])
-> [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a b. (a -> b) -> a -> b
$ TargetInfo -> [(Var, SpecType)]
assm TargetInfo
info
[(Var, SpecType)]
f3' <- [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' ([(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)])
-> StateT CGInfo Identity [(Var, SpecType)]
-> StateT CGInfo Identity [(Var, SpecType)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TargetInfo -> StateT CGInfo Identity [(Var, SpecType)]
recSelectorsTy TargetInfo
info
[(Var, SpecType)]
f3 <- [(Var, SpecType)] -> [(Var, SpecType)]
forall {a}. [(a, SpecType)] -> [(a, SpecType)]
addPolyInfo' ([(Var, SpecType)] -> [(Var, SpecType)])
-> StateT CGInfo Identity [(Var, SpecType)]
-> StateT CGInfo Identity [(Var, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' ((GhcSpecSig -> [(Var, Located SpecType)])
-> GhcSpecSig -> [(Var, SpecType)]
forall {a} {a} {c}. (a -> [(a, Located c)]) -> a -> [(a, c)]
vals GhcSpecSig -> [(Var, Located SpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp))
[(Var, SpecType)]
f40 <- [(Var, SpecType)] -> [(Var, SpecType)]
makeExactDc ([(Var, SpecType)] -> [(Var, SpecType)])
-> StateT CGInfo Identity [(Var, SpecType)]
-> StateT CGInfo Identity [(Var, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' ((GhcSpecData -> [(Var, Located SpecType)])
-> GhcSpecData -> [(Var, SpecType)]
forall {a} {a} {c}. (a -> [(a, Located c)]) -> a -> [(a, c)]
vals GhcSpecData -> [(Var, Located SpecType)]
gsCtors (TargetSpec -> GhcSpecData
gsData TargetSpec
sp))
[(Var, SpecType)]
f5 <- [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' ([(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)])
-> [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a b. (a -> b) -> a -> b
$ (GhcSpecSig -> [(Var, Located SpecType)])
-> GhcSpecSig -> [(Var, SpecType)]
forall {a} {a} {c}. (a -> [(a, Located c)]) -> a -> [(a, c)]
vals GhcSpecSig -> [(Var, Located SpecType)]
gsInSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp)
[(Var, SpecType)]
fi <- [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' ([(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)])
-> [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a b. (a -> b) -> a -> b
$ [Maybe (Var, SpecType)] -> [(Var, SpecType)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Var, SpecType)] -> [(Var, SpecType)])
-> [Maybe (Var, SpecType)] -> [(Var, SpecType)]
forall a b. (a -> b) -> a -> b
$ [(Var
x,) (SpecType -> (Var, SpecType))
-> (Located SpecType -> SpecType)
-> Located SpecType
-> (Var, SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located SpecType -> SpecType
forall a. Located a -> a
val (Located SpecType -> (Var, SpecType))
-> Maybe (Located SpecType) -> Maybe (Var, SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MethodType (Located SpecType) -> Maybe (Located SpecType)
forall t. MethodType t -> Maybe t
getMethodType MethodType (Located SpecType)
mt | (Var
x, MethodType (Located SpecType)
mt) <- GhcSpecSig -> [(Var, MethodType (Located SpecType))]
gsMethods (GhcSpecSig -> [(Var, MethodType (Located SpecType))])
-> GhcSpecSig -> [(Var, MethodType (Located SpecType))]
forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecSig
gsSig (TargetSpec -> GhcSpecSig) -> TargetSpec -> GhcSpecSig
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSpec
giSpec TargetInfo
info ]
([Located SpecType]
invs1, [(Var, SpecType)]
f41) <- ([(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)])
-> ([Located SpecType], [(Var, SpecType)])
-> StateT CGInfo Identity ([Located SpecType], [(Var, SpecType)])
forall (m :: * -> *) b c a.
Applicative m =>
(b -> m c) -> (a, b) -> m (a, c)
mapSndM [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' (([Located SpecType], [(Var, SpecType)])
-> StateT CGInfo Identity ([Located SpecType], [(Var, SpecType)]))
-> ([Located SpecType], [(Var, SpecType)])
-> StateT CGInfo Identity ([Located SpecType], [(Var, SpecType)])
forall a b. (a -> b) -> a -> b
$ [(Var, SpecType)]
-> HashSet TyCon
-> [Var]
-> ([Located SpecType], [(Var, SpecType)])
makeAutoDecrDataCons [(Var, SpecType)]
dcsty (GhcSpecTerm -> HashSet TyCon
gsAutosize (TargetSpec -> GhcSpecTerm
gsTerm TargetSpec
sp)) [Var]
dcs
([Located SpecType]
invs2, [(Var, SpecType)]
f42) <- ([(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)])
-> ([Located SpecType], [(Var, SpecType)])
-> StateT CGInfo Identity ([Located SpecType], [(Var, SpecType)])
forall (m :: * -> *) b c a.
Applicative m =>
(b -> m c) -> (a, b) -> m (a, c)
mapSndM [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' (([Located SpecType], [(Var, SpecType)])
-> StateT CGInfo Identity ([Located SpecType], [(Var, SpecType)]))
-> ([Located SpecType], [(Var, SpecType)])
-> StateT CGInfo Identity ([Located SpecType], [(Var, SpecType)])
forall a b. (a -> b) -> a -> b
$ [(Var, SpecType)]
-> HashSet TyCon
-> [Var]
-> ([Located SpecType], [(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 [(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, SpecType) -> (Symbol, SpecType)
tx = (Var -> Symbol) -> (Var, SpecType) -> (Symbol, SpecType)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst 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
[(Symbol, SpecType)]
f6 <- ((Var, SpecType) -> (Symbol, SpecType))
-> [(Var, SpecType)] -> [(Symbol, SpecType)]
forall a b. (a -> b) -> [a] -> [b]
map (Var, SpecType) -> (Symbol, SpecType)
tx ([(Var, SpecType)] -> [(Symbol, SpecType)])
-> ([(Var, SpecType)] -> [(Var, SpecType)])
-> [(Var, SpecType)]
-> [(Symbol, SpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Var, SpecType)] -> [(Var, SpecType)]
forall {a}. [(a, SpecType)] -> [(a, SpecType)]
addPolyInfo' ([(Var, SpecType)] -> [(Symbol, SpecType)])
-> StateT CGInfo Identity [(Var, SpecType)]
-> StateT CGInfo Identity [(Symbol, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a. [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' ((GhcSpecSig -> [(Var, Located SpecType)])
-> GhcSpecSig -> [(Var, SpecType)]
forall {a} {a} {c}. (a -> [(a, Located c)]) -> a -> [(a, c)]
vals GhcSpecSig -> [(Var, Located SpecType)]
gsRefSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp))
let bs :: [[(Symbol, SpecType)]]
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]
(CGInfo -> CGInfo) -> StateT CGInfo Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> StateT CGInfo Identity ())
-> (CGInfo -> CGInfo) -> StateT CGInfo Identity ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { dataConTys = f4 }
[(Symbol, Sort)]
lt1s <- (CGInfo -> [(Symbol, Sort)])
-> StateT CGInfo Identity [(Symbol, Sort)]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv (SEnv Sort -> [(Symbol, Sort)])
-> (CGInfo -> SEnv Sort) -> CGInfo -> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGInfo -> SEnv Sort
cgLits)
let lt2s :: [(Symbol, Sort)]
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 :: [(Symbol, Sort)]
tcb = (SpecType -> Sort) -> (Symbol, SpecType) -> (Symbol, Sort)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (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 :: [CoreBind]
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
[(Symbol, SpecType)]
rTrue <- ((Symbol, SpecType) -> StateT CGInfo Identity (Symbol, SpecType))
-> [(Symbol, SpecType)]
-> StateT CGInfo Identity [(Symbol, 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)
-> (Symbol, SpecType) -> StateT CGInfo Identity (Symbol, SpecType)
forall (m :: * -> *) b c a.
Applicative m =>
(b -> m c) -> (a, b) -> m (a, c)
mapSndM (Bool -> SpecType -> StateT CGInfo Identity SpecType
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 ([[(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
CGEnv
γ <- CGEnv -> CGEnv
globalize (CGEnv -> CGEnv) -> CG CGEnv -> CG CGEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CGEnv -> (String, Symbol, SpecType) -> CG CGEnv)
-> CGEnv -> [(String, Symbol, SpecType)] -> CG CGEnv
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) <- [[(Symbol, SpecType)]] -> [(Symbol, SpecType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([(Symbol, SpecType)]
rTrue[(Symbol, SpecType)]
-> [[(Symbol, SpecType)]] -> [[(Symbol, SpecType)]]
forall a. a -> [a] -> [a]
:[[(Symbol, SpecType)]] -> [[(Symbol, SpecType)]]
forall a. HasCallStack => [a] -> [a]
tail [[(Symbol, SpecType)]]
bs)])
CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ {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 = [(Located SpecType, Located SpecType)] -> RTyConInv
forall a. [(a, Located SpecType)] -> RTyConInv
mkRTyConIAl (GhcSpecData -> [(Located SpecType, Located SpecType)]
gsIaliases (TargetSpec -> GhcSpecData
gsData TargetSpec
sp))
vals :: (a -> [(a, Located c)]) -> a -> [(a, c)]
vals a -> [(a, Located c)]
f = ((a, Located c) -> (a, c)) -> [(a, Located c)] -> [(a, c)]
forall a b. (a -> b) -> [a] -> [b]
map ((Located c -> c) -> (a, Located c) -> (a, c)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd Located c -> c
forall a. Located a -> a
val) ([(a, Located c)] -> [(a, c)])
-> (a -> [(a, Located c)]) -> a -> [(a, c)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [(a, Located c)]
f
is :: [Located SpecType] -> RTyConInv
is [Located SpecType]
autoinv = [(Maybe Var, Located SpecType)] -> RTyConInv
mkRTyConInv (GhcSpecData -> [(Maybe Var, Located SpecType)]
gsInvariants (TargetSpec -> GhcSpecData
gsData TargetSpec
sp) [(Maybe Var, Located SpecType)]
-> [(Maybe Var, Located SpecType)]
-> [(Maybe Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ ((Maybe Var
forall a. Maybe a
Nothing,) (Located SpecType -> (Maybe Var, Located SpecType))
-> [Located SpecType] -> [(Maybe Var, Located SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located SpecType]
autoinv))
addPolyInfo' :: [(a, SpecType)] -> [(a, SpecType)]
addPolyInfo' = if Config -> Bool
reflection (TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig TargetInfo
info) then ((a, SpecType) -> (a, SpecType))
-> [(a, SpecType)] -> [(a, SpecType)]
forall a b. (a -> b) -> [a] -> [b]
map ((SpecType -> SpecType) -> (a, SpecType) -> (a, SpecType)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd SpecType -> SpecType
addPolyInfo) else [(a, SpecType)] -> [(a, 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)]
-> [PVar (RType RTyCon RTyVar ())] -> SpecType -> SpecType
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 ((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) [PVar (RType RTyCon RTyVar ())]
ps SpecType
t'
where
([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
as, [PVar (RType RTyCon RTyVar ())]
ps, SpecType
t') = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVar (RType RTyCon RTyVar ())], SpecType)
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 = 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 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]
-> ([Located SpecType], [(Var, SpecType)])
makeAutoDecrDataCons [(Var, SpecType)]
dcts HashSet TyCon
specenv [Var]
dcs
= ([RType RTyCon RTyVar ()] -> [Located SpecType]
forall {tv} {c} {a}.
(Eq tv, Eq c, Eq a) =>
[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) = [(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 :: [RType c tv a] -> [Located (RType c tv RReft)]
simplify [RType c tv a]
invs = RType c tv RReft -> Located (RType c tv RReft)
forall a. a -> Located a
dummyLoc (RType c tv RReft -> Located (RType c tv RReft))
-> (RType c tv a -> RType c tv RReft)
-> RType c tv a
-> Located (RType c tv RReft)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RType c tv RReft -> RReft -> RType c tv RReft
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` RReft
invariant) (RType c tv RReft -> RType c tv RReft)
-> (RType c tv a -> RType c tv RReft)
-> RType c tv a
-> RType c tv RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> RReft) -> RType c tv a -> RType c tv RReft
forall a b. (a -> b) -> RType c tv a -> RType c tv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RReft -> a -> RReft
forall a b. a -> b -> a
const RReft
forall a. Monoid a => a
mempty) (RType c tv a -> Located (RType c tv RReft))
-> [RType c tv a] -> [Located (RType c tv RReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv a] -> [RType c tv a]
forall a. Eq a => [a] -> [a]
L.nub [RType c tv a]
invs
invariant :: RReft
invariant = Reft -> Predicate -> RReft
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 (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Constant
F.I Integer
0)) ) Predicate
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
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 c tv r. RType c tv r -> RType c tv ()
toRSort (SpecType -> RType RTyCon RTyVar ())
-> SpecType -> RType RTyCon RTyVar ()
forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
trep, (Var
x, RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep RTypeRep 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 :: RTypeRep RTyCon RTyVar RReft
trep = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
st
tres :: SpecType
tres = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
trep SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` Reft -> Predicate -> RReft
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)) Predicate
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 c tv r. RType c tv r -> RType c tv ()
toRSort SpecType
t RType RTyCon RTyVar () -> RType RTyCon RTyVar () -> Bool
forall a. Eq a => a -> a -> Bool
== SpecType -> RType RTyCon RTyVar ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort SpecType
tres) ([SpecType] -> [Symbol] -> [(SpecType, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep) (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep 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
F.EBin Bop
F.Plus) (Constant -> Expr
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 (m :: * -> *) b c a.
Applicative m =>
(b -> m c) -> (a, b) -> m (a, c)
mapSndM SpecType -> StateT CGInfo Identity SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshArgs)
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)
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 ((Located SpecType -> SpecType)
-> (Symbol, Located SpecType) -> (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 Located SpecType -> SpecType
forall a. Located a -> a
val ((Symbol, Located SpecType) -> (Symbol, SpecType))
-> [(Symbol, Located SpecType)] -> [(Symbol, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecData -> [(Symbol, Located SpecType)]
gsMeas (TargetSpec -> GhcSpecData
gsData TargetSpec
sp)) []
, syenv :: SEnv Var
syenv = [(Symbol, Var)] -> SEnv Var
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv (GhcSpecNames -> [(Symbol, Var)]
gsFreeSyms (TargetSpec -> GhcSpecNames
gsName 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)]
forall a. [a]
tcb' [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
lts [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ ((Located SpecType -> Sort)
-> (Symbol, Located SpecType) -> (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)
-> (Located SpecType -> SpecType) -> Located SpecType -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located SpecType -> SpecType
forall a. Located a -> a
val) ((Symbol, Located SpecType) -> (Symbol, Sort))
-> [(Symbol, Located SpecType)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecData -> [(Symbol, Located SpecType)]
gsMeas (TargetSpec -> GhcSpecData
gsData TargetSpec
sp)))
, denv :: RDEnv
denv = (Located SpecType -> SpecType)
-> DEnv Var (Located SpecType) -> RDEnv
forall a b v. (a -> b) -> DEnv v a -> DEnv v b
dmapty Located SpecType -> SpecType
forall a. Located a -> a
val (DEnv Var (Located SpecType) -> RDEnv)
-> DEnv Var (Located SpecType) -> RDEnv
forall a b. (a -> b) -> a -> b
$ GhcSpecSig -> DEnv Var (Located SpecType)
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 = [(Located SpecType, Located SpecType)] -> RTyConInv
forall a. [(a, Located SpecType)] -> RTyConInv
mkRTyConIAl (GhcSpecData -> [(Located SpecType, Located SpecType)]
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' = []
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, Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t) | (Var
x, Located SpecType
t) <- [(Var, Located SpecType)]
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, Located SpecType)]
sigs = GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs (GhcSpecSig -> [(Var, Located SpecType)])
-> (TargetInfo -> GhcSpecSig)
-> TargetInfo
-> [(Var, Located SpecType)]
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, Located SpecType)])
-> TargetInfo -> [(Var, Located SpecType)]
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,Located SpecType
_) <- GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs GhcSpecSig
sp [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, Located SpecType)]
gsAsmSigs GhcSpecSig
sp [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, Located SpecType)]
gsRefSigs GhcSpecSig
sp [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, Located SpecType)]
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,Located SpecType
_) <- GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs GhcSpecSig
sp [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, Located SpecType)]
gsAsmSigs GhcSpecSig
sp [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, Located SpecType)]
gsRefSigs GhcSpecSig
sp [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, Located SpecType)]
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, Located SpecType)])
-> (Sort -> Bool) -> TargetInfo -> SEnv Sort
infoLits TargetSpec -> [(Symbol, Located SpecType)]
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, Located SpecType) -> (Symbol, Sort)
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 ((Symbol, Located SpecType) -> (Symbol, Sort))
-> [(Symbol, Located SpecType)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TargetSpec -> [(Symbol, Located SpecType)]
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 = (Located (RRType r) -> Sort)
-> (a, Located (RRType r)) -> (a, Sort)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (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
, 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 ((Located SpecType -> SpecType)
-> (TyCon, Located SpecType) -> (TyCon, SpecType)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd Located SpecType -> SpecType
forall a. Located a -> a
val ((TyCon, Located SpecType) -> (TyCon, SpecType))
-> [(TyCon, Located SpecType)] -> [(TyCon, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyCon, Located SpecType)]
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, Located SpecType)])
-> (Sort -> Bool) -> TargetInfo -> SEnv Sort
infoLits (GhcSpecData -> [(Symbol, Located SpecType)]
gsMeas (GhcSpecData -> [(Symbol, Located SpecType)])
-> (TargetSpec -> GhcSpecData)
-> TargetSpec
-> [(Symbol, Located SpecType)]
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, Located SpecType)])
-> (Sort -> Bool) -> TargetInfo -> SEnv Sort
infoLits (GhcSpecData -> [(Symbol, Located SpecType)]
gsMeas (GhcSpecData -> [(Symbol, Located SpecType)])
-> (TargetSpec -> GhcSpecData)
-> TargetSpec
-> [(Symbol, Located SpecType)]
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, Located SpecType
_, [Located Expr]
es) <- GhcSpecSig -> [(Var, Located SpecType, [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 ]
[(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 ]
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]
freeVs
freeVs :: [Var]
freeVs = TargetSrc -> [Var]
giImpVars TargetSrc
src [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
freeSyms
freeSyms :: [Var]
freeSyms = ((Symbol, Var) -> Var) -> [(Symbol, Var)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Symbol, Var) -> Var
forall a b. (a, b) -> b
snd ([(Symbol, Var)] -> [Var])
-> (TargetInfo -> [(Symbol, Var)]) -> TargetInfo -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSpecNames -> [(Symbol, Var)]
gsFreeSyms (GhcSpecNames -> [(Symbol, Var)])
-> (TargetInfo -> GhcSpecNames) -> TargetInfo -> [(Symbol, Var)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecNames
gsName (TargetSpec -> GhcSpecNames)
-> (TargetInfo -> TargetSpec) -> TargetInfo -> GhcSpecNames
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec (TargetInfo -> [Var]) -> TargetInfo -> [Var]
forall a b. (a -> b) -> a -> b
$ 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)