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

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

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

import           Prelude                                       hiding (error, undefined)
import           Coercion
import           DataCon
import           CoreSyn
import           Type
import           TyCon
import           Var
import           Id                                           -- hiding (isExportedId)
import           Name        hiding (varName)
import           Control.Monad.State
import           Data.Maybe                                    (isNothing, fromMaybe, catMaybes)
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           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 (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Var
x,) (Type -> StateT CGInfo Identity SpecType
trueTy (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   Var -> StateT CGInfo Identity (Var, SpecType)
makeDataConTypes
       [(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'  Var -> StateT CGInfo Identity (Var, SpecType)
makeDataConTypes
       ([Symbol]
hs,[(Var, SpecType)]
f0)  <- [(Var, SpecType)]
-> StateT CGInfo Identity ([Symbol], [(Var, SpecType)])
forall t r c (f :: * -> *) tv.
(Symbolic t, Reftable r, TyConable c, Freshable f r) =>
[(t, RType c tv r)] -> f ([Symbol], [(t, RType c tv r)])
refreshHoles ([(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                           -- asserted refinements     (for defined vars)
       [(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                      -- default TOP reftype      (for exported vars without spec)
       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                            -- default TOP reftype      (for all vars)
       [(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                   -- data constructors
       [(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                           -- assumed refinements      (for imported vars)
       [(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                      -- assumed refinements      (for record selectors)
       [(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' ([(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)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp))                 -- assumed refinedments     (with `assume`)
       [(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' ([(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)])
-> [(Var, SpecType)] -> StateT CGInfo Identity [(Var, SpecType)]
forall a b. (a -> b) -> a -> b
$ (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)) -- constructor refinements  (for measures)
       [(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)                   -- internal refinements     (from Haskell measures)
       [(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 (f :: * -> *) t t t.
Functor f =>
(t -> f t) -> (t, t) -> f (t, t)
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 (f :: * -> *) t t t.
Functor f =>
(t -> f t) -> (t, t) -> f (t, t)
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' ([(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)]
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 :: [(Var, SpecType)]
dataConTys = [(Var, SpecType)]
f4 }
       [(Symbol, Sort)]
lt1s     <- 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 (CGInfo -> [(Symbol, Sort)])
-> StateT CGInfo Identity CGInfo
-> StateT CGInfo Identity [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
       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)
mapM ((SpecType -> StateT CGInfo Identity SpecType)
-> (Symbol, SpecType) -> StateT CGInfo Identity (Symbol, SpecType)
forall (f :: * -> *) t t t.
Functor f =>
(t -> f t) -> (t, t) -> f (t, t)
mapSndM SpecType -> StateT CGInfo Identity SpecType
forall (m :: * -> *) a. Freshable m a => a -> m a
true) [(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. [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. [a] -> Int -> a
!!Int
3) ([[(Symbol, SpecType)]]
bs[[(Symbol, SpecType)]] -> Int -> [(Symbol, SpecType)]
forall a. [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)]] -> [(Symbol, SpecType)])
-> [[(Symbol, SpecType)]] -> [(Symbol, SpecType)]
forall a b. (a -> b) -> a -> b
$ ([(Symbol, SpecType)]
rTrue[(Symbol, SpecType)]
-> [[(Symbol, SpecType)]] -> [[(Symbol, SpecType)]]
forall a. a -> [a] -> [a]
:[[(Symbol, SpecType)]] -> [[(Symbol, SpecType)]]
forall a. [a] -> [a]
tail [[(Symbol, SpecType)]]
bs)])
       CGEnv -> CG CGEnv
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ {invs :: RTyConInv
invs = [Located SpecType] -> RTyConInv
is ([Located SpecType]
invs1 [Located SpecType] -> [Located SpecType] -> [Located SpecType]
forall a. [a] -> [a] -> [a]
++ [Located SpecType]
invs2)}
  where
    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
    mapSndM :: (t -> f t) -> (t, t) -> f (t, t)
mapSndM t -> f t
f    = \(t
x,t
y) -> ((t
x,) (t -> (t, t)) -> f t -> f (t, t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> f t
f t
y)
    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
    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 

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 {- 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 :: Var -> CG (Var, SpecType)
makeDataConTypes :: Var -> StateT CGInfo Identity (Var, SpecType)
makeDataConTypes 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
<$> (Type -> StateT CGInfo Identity SpecType
trueTy (Type -> StateT CGInfo Identity SpecType)
-> Type -> StateT CGInfo Identity SpecType
forall a b. (a -> b) -> a -> b
$ 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 a c.
(Eq tv, Eq a, Eq c) =>
[RType c tv a] -> [Located (RType c tv RReft)]
simplify [RType RTyCon RTyVar ()]
invs, [(Var, SpecType)]
tys)
  where
    ([RType RTyCon RTyVar ()]
invs, [(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
$ [Maybe TyCon] -> [TyCon]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe TyCon] -> [TyCon]) -> [Maybe TyCon] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ (Var -> Maybe TyCon) -> [Var] -> [Maybe TyCon]
forall a b. (a -> b) -> [a] -> [b]
map 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
_ -> 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 (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 :: SpecType
ty_res = SpecType
tres}))
    where
      x :: Var
x      = DataCon -> Var
dataConWorkId DataCon
x'
      t :: SpecType
t      = 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
t
      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 (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' :: [(a, SpecType)] -> CG [(a, SpecType)]
refreshArgs' = ((a, SpecType) -> StateT CGInfo Identity (a, SpecType))
-> [(a, SpecType)] -> CG [(a, SpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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)


-- | 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 (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 :: SpanStack
-> REnv
-> SEnv Var
-> RDEnv
-> SEnv Sort
-> SEnv Sort
-> FEnv
-> HashSet Var
-> RTyConInv
-> RTyConInv
-> RTyConInv
-> REnv
-> REnv
-> REnv
-> TCEmb TyCon
-> TagEnv
-> Maybe Var
-> Maybe (HashMap Symbol SpecType)
-> HashMap Symbol CoreExpr
-> HashMap Var Expr
-> HEnv
-> LConstraint
-> Maybe (TError SpecType)
-> TargetInfo
-> Maybe Var
-> CGEnv
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 (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 (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
<$> Type -> StateT CGInfo Identity SpecType
trueTy (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
<$> Type -> StateT CGInfo Identity SpecType
trueTy (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 :: SEnv Sort
-> [SubC]
-> [WfC]
-> [FixSubC]
-> [FixWfC]
-> Integer
-> BindEnv
-> [Int]
-> AnnInfo (Annot SpecType)
-> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
-> TyConMap
-> [(Var, [Int])]
-> HashMap TyCon SpecType
-> HashMap Var [Located Expr]
-> HashSet Var
-> HashSet Var
-> HashSet Var
-> HashSet TyCon
-> TCEmb TyCon
-> Kuts
-> [HashSet KVar]
-> SEnv Sort
-> SEnv Sort
-> [DataDecl]
-> Bool
-> Bool
-> [TError SpecType]
-> KVProf
-> Int
-> HashMap Int SrcSpan
-> Bool
-> TargetInfo
-> [(Var, SpecType)]
-> Templates
-> CGInfo
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 :: BindEnv
binds      = BindEnv
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
  , holesMap :: HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
holesMap   = HashMap Var (HoleInfo (CGInfo, CGEnv) 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) ]
  , specDecr :: [(Var, [Int])]
specDecr   = GhcSpecTerm -> [(Var, [Int])]
gsDecr  GhcSpecTerm
tspc
  , 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
  , 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]
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 (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)