{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-dodgy-imports #-}
{-# OPTIONS_GHC -Wno-unused-top-binds #-}
module Language.Haskell.Liquid.Bare.Elaborate
( fixExprToHsExpr
, elaborateSpecType
)
where
import qualified Language.Fixpoint.Types as F
import Liquid.GHC.API hiding (panic, varName)
import qualified Language.Haskell.Liquid.GHC.Misc
as GM
import Language.Haskell.Liquid.Types.Types
import Language.Haskell.Liquid.Types.RefType
( ofType )
import qualified Data.List as L
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Control.Monad.Free
#if MIN_VERSION_recursion_schemes(5,2,0)
import Data.Fix hiding (hylo)
import Data.Functor.Foldable hiding (Fix)
#else
import Data.Functor.Foldable
#endif
import Data.Char ( isUpper )
import GHC.Types.Name.Occurrence
import qualified Liquid.GHC.API as Ghc
(noExtField)
import Data.Default ( def )
import qualified Data.Maybe as Mb
data RTypeF c tv r f
= RVarF {
forall c tv r f. RTypeF c tv r f -> tv
rtf_var :: !tv
, forall c tv r f. RTypeF c tv r f -> r
rtf_reft :: !r
}
| RFunF {
forall c tv r f. RTypeF c tv r f -> Symbol
rtf_bind :: !F.Symbol
, forall c tv r f. RTypeF c tv r f -> RFInfo
rtf_rinfo :: !RFInfo
, forall c tv r f. RTypeF c tv r f -> f
rtf_in :: !f
, forall c tv r f. RTypeF c tv r f -> f
rtf_out :: !f
, rtf_reft :: !r
}
| RAllTF {
forall c tv r f. RTypeF c tv r f -> RTVU c tv
rtf_tvbind :: !(RTVU c tv)
, forall c tv r f. RTypeF c tv r f -> f
rtf_ty :: !f
, forall c tv r f. RTypeF c tv r f -> r
rtf_ref :: !r
}
| RAllPF {
forall c tv r f. RTypeF c tv r f -> PVU c tv
rtf_pvbind :: !(PVU c tv)
, rtf_ty :: !f
}
| RAppF {
forall c tv r f. RTypeF c tv r f -> c
rtf_tycon :: !c
, forall c tv r f. RTypeF c tv r f -> [f]
rtf_args :: ![f]
, forall c tv r f. RTypeF c tv r f -> [RTPropF c tv f]
rtf_pargs :: ![RTPropF c tv f]
, rtf_reft :: !r
}
| RAllEF {
rtf_bind :: !F.Symbol
, forall c tv r f. RTypeF c tv r f -> f
rtf_allarg :: !f
, rtf_ty :: !f
}
| RExF {
rtf_bind :: !F.Symbol
, forall c tv r f. RTypeF c tv r f -> f
rtf_exarg :: !f
, rtf_ty :: !f
}
| RExprArgF (F.Located F.Expr)
| RAppTyF{
forall c tv r f. RTypeF c tv r f -> f
rtf_arg :: !f
, forall c tv r f. RTypeF c tv r f -> f
rtf_res :: !f
, rtf_reft :: !r
}
| RRTyF {
forall c tv r f. RTypeF c tv r f -> [(Symbol, f)]
rtf_env :: ![(F.Symbol, f)]
, rtf_ref :: !r
, forall c tv r f. RTypeF c tv r f -> Oblig
rtf_obl :: !Oblig
, rtf_ty :: !f
}
| RHoleF r
deriving ((forall a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b)
-> (forall a b. a -> RTypeF c tv r b -> RTypeF c tv r a)
-> Functor (RTypeF c tv r)
forall a b. a -> RTypeF c tv r b -> RTypeF c tv r a
forall a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b
forall c tv r a b. a -> RTypeF c tv r b -> RTypeF c tv r a
forall c tv r a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall c tv r a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b
fmap :: forall a b. (a -> b) -> RTypeF c tv r a -> RTypeF c tv r b
$c<$ :: forall c tv r a b. a -> RTypeF c tv r b -> RTypeF c tv r a
<$ :: forall a b. a -> RTypeF c tv r b -> RTypeF c tv r a
Functor)
type RTPropF c tv f = Ref (RType c tv ()) f
type SpecTypeF = RTypeF RTyCon RTyVar RReft
type PartialSpecType = Free SpecTypeF ()
type instance Base (RType c tv r) = RTypeF c tv r
instance Recursive (RType c tv r) where
project :: RType c tv r -> Base (RType c tv r) (RType c tv r)
project (RVar tv
var r
reft ) = tv -> r -> RTypeF c tv r (RType c tv r)
forall c tv r f. tv -> r -> RTypeF c tv r f
RVarF tv
var r
reft
project (RFun Symbol
bind RFInfo
i RType c tv r
tin RType c tv r
tout r
reft) = Symbol
-> RFInfo
-> RType c tv r
-> RType c tv r
-> r
-> RTypeF c tv r (RType c tv r)
forall c tv r f. Symbol -> RFInfo -> f -> f -> r -> RTypeF c tv r f
RFunF Symbol
bind RFInfo
i RType c tv r
tin RType c tv r
tout r
reft
project (RAllT RTVU c tv
tvbind RType c tv r
ty r
ref ) = RTVU c tv -> RType c tv r -> r -> RTypeF c tv r (RType c tv r)
forall c tv r f. RTVU c tv -> f -> r -> RTypeF c tv r f
RAllTF RTVU c tv
tvbind RType c tv r
ty r
ref
project (RAllP PVU c tv
pvbind RType c tv r
ty ) = PVU c tv -> RType c tv r -> RTypeF c tv r (RType c tv r)
forall c tv r f. PVU c tv -> f -> RTypeF c tv r f
RAllPF PVU c tv
pvbind RType c tv r
ty
project (RApp c
c [RType c tv r]
args [RTProp c tv r]
pargs r
reft ) = c
-> [RType c tv r]
-> [RTProp c tv r]
-> r
-> RTypeF c tv r (RType c tv r)
forall c tv r f.
c -> [f] -> [RTPropF c tv f] -> r -> RTypeF c tv r f
RAppF c
c [RType c tv r]
args [RTProp c tv r]
pargs r
reft
project (RAllE Symbol
bind RType c tv r
allarg RType c tv r
ty ) = Symbol
-> RType c tv r -> RType c tv r -> RTypeF c tv r (RType c tv r)
forall c tv r f. Symbol -> f -> f -> RTypeF c tv r f
RAllEF Symbol
bind RType c tv r
allarg RType c tv r
ty
project (REx Symbol
bind RType c tv r
exarg RType c tv r
ty ) = Symbol
-> RType c tv r -> RType c tv r -> RTypeF c tv r (RType c tv r)
forall c tv r f. Symbol -> f -> f -> RTypeF c tv r f
RExF Symbol
bind RType c tv r
exarg RType c tv r
ty
project (RExprArg Located Expr
e ) = Located Expr -> RTypeF c tv r (RType c tv r)
forall c tv r f. Located Expr -> RTypeF c tv r f
RExprArgF Located Expr
e
project (RAppTy RType c tv r
arg RType c tv r
res r
reft ) = RType c tv r -> RType c tv r -> r -> RTypeF c tv r (RType c tv r)
forall c tv r f. f -> f -> r -> RTypeF c tv r f
RAppTyF RType c tv r
arg RType c tv r
res r
reft
project (RRTy [(Symbol, RType c tv r)]
env r
ref Oblig
obl RType c tv r
ty ) = [(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RTypeF c tv r (RType c tv r)
forall c tv r f.
[(Symbol, f)] -> r -> Oblig -> f -> RTypeF c tv r f
RRTyF [(Symbol, RType c tv r)]
env r
ref Oblig
obl RType c tv r
ty
project (RHole r
r ) = r -> RTypeF c tv r (RType c tv r)
forall c tv r f. r -> RTypeF c tv r f
RHoleF r
r
instance Corecursive (RType c tv r) where
embed :: Base (RType c tv r) (RType c tv r) -> RType c tv r
embed (RVarF tv
var r
reft ) = tv -> r -> RType c tv r
forall c tv r. tv -> r -> RType c tv r
RVar tv
var r
reft
embed (RFunF Symbol
bind RFInfo
i RType c tv r
tin RType c tv r
tout r
reft) = Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
bind RFInfo
i RType c tv r
tin RType c tv r
tout r
reft
embed (RAllTF RTVU c tv
tvbind RType c tv r
ty r
ref ) = RTVU c tv -> RType c tv r -> r -> RType c tv r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
tvbind RType c tv r
ty r
ref
embed (RAllPF PVU c tv
pvbind RType c tv r
ty ) = PVU c tv -> RType c tv r -> RType c tv r
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
pvbind RType c tv r
ty
embed (RAppF c
c [RType c tv r]
args [RTPropF c tv (RType c tv r)]
pargs r
reft ) = c
-> [RType c tv r]
-> [RTPropF c tv (RType c tv r)]
-> r
-> RType c tv r
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv r]
args [RTPropF c tv (RType c tv r)]
pargs r
reft
embed (RAllEF Symbol
bind RType c tv r
allarg RType c tv r
ty ) = Symbol -> RType c tv r -> RType c tv r -> RType c tv r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
bind RType c tv r
allarg RType c tv r
ty
embed (RExF Symbol
bind RType c tv r
exarg RType c tv r
ty ) = Symbol -> RType c tv r -> RType c tv r -> RType c tv r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
bind RType c tv r
exarg RType c tv r
ty
embed (RExprArgF Located Expr
e ) = Located Expr -> RType c tv r
forall c tv r. Located Expr -> RType c tv r
RExprArg Located Expr
e
embed (RAppTyF RType c tv r
arg RType c tv r
res r
reft ) = RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv r
arg RType c tv r
res r
reft
embed (RRTyF [(Symbol, RType c tv r)]
env r
ref Oblig
obl RType c tv r
ty ) = [(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, RType c tv r)]
env r
ref Oblig
obl RType c tv r
ty
embed (RHoleF r
r ) = r -> RType c tv r
forall c tv r. r -> RType c tv r
RHole r
r
specTypeToPartial :: forall a . SpecType -> SpecTypeF (Free SpecTypeF a)
specTypeToPartial :: forall a.
RType RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial = (RTypeF
RTyCon
RTyVar
RReft
(SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a))
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a))
-> (RType RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft))
-> RType RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
forall (f :: * -> *) b a.
Functor f =>
(f b -> b) -> (a -> f a) -> a -> b
hylo ((SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
-> Free (RTypeF RTyCon RTyVar RReft) a)
-> RTypeF
RTyCon
RTyVar
RReft
(SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a))
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
forall a b.
(a -> b)
-> RTypeF RTyCon RTyVar RReft a -> RTypeF RTyCon RTyVar RReft b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
-> Free (RTypeF RTyCon RTyVar RReft) a
forall a.
RTypeF RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a)
-> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap) RType RTyCon RTyVar RReft
-> Base (RType RTyCon RTyVar RReft) (RType RTyCon RTyVar RReft)
RType RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft)
forall t. Recursive t => t -> Base t t
project
plugType :: SpecType -> PartialSpecType -> SpecType
plugType :: RType RTyCon RTyVar RReft
-> PartialSpecType -> RType RTyCon RTyVar RReft
plugType RType RTyCon RTyVar RReft
t = Fix (RTypeF RTyCon RTyVar RReft) -> RType RTyCon RTyVar RReft
forall s t. (Recursive s, Corecursive t, Base s ~ Base t) => s -> t
refix (Fix (RTypeF RTyCon RTyVar RReft) -> RType RTyCon RTyVar RReft)
-> (PartialSpecType -> Fix (RTypeF RTyCon RTyVar RReft))
-> PartialSpecType
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PartialSpecType -> Fix (RTypeF RTyCon RTyVar RReft)
f
where
f :: PartialSpecType -> Fix (RTypeF RTyCon RTyVar RReft)
f = (RTypeF RTyCon RTyVar RReft (Fix (RTypeF RTyCon RTyVar RReft))
-> Fix (RTypeF RTyCon RTyVar RReft))
-> (PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
-> PartialSpecType
-> Fix (RTypeF RTyCon RTyVar RReft)
forall (f :: * -> *) b a.
Functor f =>
(f b -> b) -> (a -> f a) -> a -> b
hylo RTypeF RTyCon RTyVar RReft (Fix (RTypeF RTyCon RTyVar RReft))
-> Fix (RTypeF RTyCon RTyVar RReft)
forall (f :: * -> *). f (Fix f) -> Fix f
Fix ((PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
-> PartialSpecType -> Fix (RTypeF RTyCon RTyVar RReft))
-> (PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType)
-> PartialSpecType
-> Fix (RTypeF RTyCon RTyVar RReft)
forall a b. (a -> b) -> a -> b
$ \case
Pure ()
_ -> RType RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall a.
RType RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial RType RTyCon RTyVar RReft
t
Free RTypeF RTyCon RTyVar RReft PartialSpecType
res -> RTypeF RTyCon RTyVar RReft PartialSpecType
res
collectSpecTypeBinders :: SpecType -> ([F.Symbol], [F.Symbol])
collectSpecTypeBinders :: RType RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders = (Base
(RType RTyCon RTyVar RReft)
(RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
-> ([Symbol], [Symbol]))
-> RType RTyCon RTyVar RReft -> ([Symbol], [Symbol])
forall t a. Recursive t => (Base t (t, a) -> a) -> t -> a
forall a.
(Base (RType RTyCon RTyVar RReft) (RType RTyCon RTyVar RReft, a)
-> a)
-> RType RTyCon RTyVar RReft -> a
para ((Base
(RType RTyCon RTyVar RReft)
(RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
-> ([Symbol], [Symbol]))
-> RType RTyCon RTyVar RReft -> ([Symbol], [Symbol]))
-> (Base
(RType RTyCon RTyVar RReft)
(RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
-> ([Symbol], [Symbol]))
-> RType RTyCon RTyVar RReft
-> ([Symbol], [Symbol])
forall a b. (a -> b) -> a -> b
$ \case
RFunF Symbol
bind RFInfo
_ (RType RTyCon RTyVar RReft
tin, ([Symbol], [Symbol])
_) (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) RReft
_ | RType RTyCon RTyVar RReft -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin -> ([Symbol]
bs, [Symbol]
abs')
| Bool
otherwise -> (Symbol
bind Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
RAllEF Symbol
b (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) -> (Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
RAllTF (RTVar (RTV TyVar
ab) RTVInfo (RType RTyCon RTyVar ())
_) (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) RReft
_ -> ([Symbol]
bs, TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyVar
ab Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
abs')
RExF Symbol
b (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) -> (Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, [Symbol]
abs')
RAppTyF (RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) RReft
_ -> ([Symbol]
bs, [Symbol]
abs')
RRTyF [(Symbol, (RType RTyCon RTyVar RReft, ([Symbol], [Symbol])))]
_ RReft
_ Oblig
_ (RType RTyCon RTyVar RReft
_, ([Symbol]
bs, [Symbol]
abs')) -> ([Symbol]
bs, [Symbol]
abs')
Base
(RType RTyCon RTyVar RReft)
(RType RTyCon RTyVar RReft, ([Symbol], [Symbol]))
_ -> ([], [])
buildHsExpr :: LHsExpr GhcPs -> SpecType -> LHsExpr GhcPs
buildHsExpr :: LHsExpr GhcPs -> RType RTyCon RTyVar RReft -> LHsExpr GhcPs
buildHsExpr LHsExpr GhcPs
result = (Base
(RType RTyCon RTyVar RReft)
(RType RTyCon RTyVar RReft, LHsExpr GhcPs)
-> LHsExpr GhcPs)
-> RType RTyCon RTyVar RReft -> LHsExpr GhcPs
forall t a. Recursive t => (Base t (t, a) -> a) -> t -> a
forall a.
(Base (RType RTyCon RTyVar RReft) (RType RTyCon RTyVar RReft, a)
-> a)
-> RType RTyCon RTyVar RReft -> a
para ((Base
(RType RTyCon RTyVar RReft)
(RType RTyCon RTyVar RReft, LHsExpr GhcPs)
-> LHsExpr GhcPs)
-> RType RTyCon RTyVar RReft -> LHsExpr GhcPs)
-> (Base
(RType RTyCon RTyVar RReft)
(RType RTyCon RTyVar RReft, LHsExpr GhcPs)
-> LHsExpr GhcPs)
-> RType RTyCon RTyVar RReft
-> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ \case
RFunF Symbol
bind RFInfo
_ (RType RTyCon RTyVar RReft
tin, GenLocated SrcSpanAnnA (HsExpr GhcPs)
_) (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) RReft
_
| RType RTyCon RTyVar RReft -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
| Bool
otherwise -> [LPat GhcPs] -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (p :: Pass).
(IsPass p, XMG (GhcPass p) (LHsExpr (GhcPass p)) ~ Origin) =>
[LPat (GhcPass p)] -> LHsExpr (GhcPass p) -> LHsExpr (GhcPass p)
mkHsLam [IdP GhcPs -> LPat GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LPat (GhcPass p)
nlVarPat (Symbol -> RdrName
varSymbolToRdrName Symbol
bind)] LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
RAllEF Symbol
_ (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsExpr GhcPs))
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
RAllTF RTVar RTyVar (RType RTyCon RTyVar ())
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) RReft
_ -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
RExF Symbol
_ (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsExpr GhcPs))
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
RAppTyF (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsExpr GhcPs))
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) RReft
_ -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
RRTyF [(Symbol,
(RType RTyCon RTyVar RReft,
GenLocated SrcSpanAnnA (HsExpr GhcPs)))]
_ RReft
_ Oblig
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsExpr GhcPs)
res) -> LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
res
Base
(RType RTyCon RTyVar RReft)
(RType RTyCon RTyVar RReft, LHsExpr GhcPs)
_ -> LHsExpr GhcPs
result
canonicalizeDictBinder
:: F.Subable a => [F.Symbol] -> (a, [F.Symbol]) -> (a, [F.Symbol])
canonicalizeDictBinder :: forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [] (a
e', [Symbol]
bs') = (a
e', [Symbol]
bs')
canonicalizeDictBinder [Symbol]
bs (a
e', [] ) = (a
e', [Symbol]
bs)
canonicalizeDictBinder [Symbol]
bs (a
e', [Symbol]
bs') = ([Symbol] -> [Symbol] -> a -> a
forall a. Subable a => [Symbol] -> [Symbol] -> a -> a
renameDictBinder [Symbol]
bs [Symbol]
bs' a
e', [Symbol]
bs)
where
renameDictBinder :: (F.Subable a) => [F.Symbol] -> [F.Symbol] -> a -> a
renameDictBinder :: forall a. Subable a => [Symbol] -> [Symbol] -> a -> a
renameDictBinder [] [Symbol]
_ = a -> a
forall a. a -> a
id
renameDictBinder [Symbol]
_ [] = a -> a
forall a. a -> a
id
renameDictBinder [Symbol]
canonicalDs [Symbol]
ds = (Symbol -> Symbol) -> a -> a
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa ((Symbol -> Symbol) -> a -> a) -> (Symbol -> Symbol) -> a -> a
forall a b. (a -> b) -> a -> b
$ \Symbol
x -> Symbol -> Symbol -> HashMap Symbol Symbol -> Symbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
x Symbol
x HashMap Symbol Symbol
tbl
where tbl :: HashMap Symbol Symbol
tbl = [Char] -> HashMap Symbol Symbol -> HashMap Symbol Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"TBL" (HashMap Symbol Symbol -> HashMap Symbol Symbol)
-> HashMap Symbol Symbol -> HashMap Symbol Symbol
forall a b. (a -> b) -> a -> b
$ [(Symbol, Symbol)] -> HashMap Symbol Symbol
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
ds [Symbol]
canonicalDs)
elaborateSpecType
:: (CoreExpr -> F.Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> TcRn SpecType
elaborateSpecType :: (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft)
elaborateSpecType CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplifier RType RTyCon RTyVar RReft
t = TcRn (RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft)
forall a. TcM a -> TcM a
GM.withWiredIn (TcRn (RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft))
-> TcRn (RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft)
forall a b. (a -> b) -> a -> b
$ do
(RType RTyCon RTyVar RReft
t', [Symbol]
xs) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' (() -> PartialSpecType
forall a. a -> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplifier RType RTyCon RTyVar RReft
t
case [Symbol]
xs of
Symbol
_ : [Symbol]
_ -> Maybe SrcSpan -> [Char] -> TcRn (RType RTyCon RTyVar RReft)
forall a. Maybe SrcSpan -> [Char] -> a
panic
Maybe SrcSpan
forall a. Maybe a
Nothing
[Char]
"elaborateSpecType: invariant broken. substitution list for dictionary is not completely consumed"
[Symbol]
_ -> RType RTyCon RTyVar RReft -> TcRn (RType RTyCon RTyVar RReft)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RType RTyCon RTyVar RReft
t'
elaborateSpecType'
:: PartialSpecType
-> (CoreExpr -> F.Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> TcRn (SpecType, [F.Symbol])
elaborateSpecType' :: PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
t =
case [Char] -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"elaborateSpecType'" RType RTyCon RTyVar RReft
t of
RVar (RTV TyVar
tv) (MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_oldE)) Predicate
p) -> do
(Reft, RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> ([Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
(Reft
reft, RType RTyCon RTyVar RReft
t)
((RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RType RTyCon RTyVar RReft
t, []))
(\[Symbol]
bs' Expr
ee -> (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTyVar -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. tv -> r -> RType c tv r
RVar (TyVar -> RTyVar
RTV TyVar
tv) (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
ee)) Predicate
p), [Symbol]
bs'))
RFun Symbol
bind RFInfo
i RType RTyCon RTyVar RReft
tin RType RTyCon RTyVar RReft
tout ureft :: RReft
ureft@(MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_oldE)) Predicate
p) -> do
let partialFunTp :: PartialSpecType
partialFunTp =
RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (Symbol
-> RFInfo
-> PartialSpecType
-> PartialSpecType
-> RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall c tv r f. Symbol -> RFInfo -> f -> f -> r -> RTypeF c tv r f
RFunF Symbol
bind RFInfo
i (RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall a.
RTypeF RTyCon RTyVar RReft (Free (RTypeF RTyCon RTyVar RReft) a)
-> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap (RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType)
-> RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall a b. (a -> b) -> a -> b
$ RType RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall a.
RType RTyCon RTyVar RReft
-> SpecTypeF (Free (RTypeF RTyCon RTyVar RReft) a)
specTypeToPartial RType RTyCon RTyVar RReft
tin) (() -> PartialSpecType
forall a. a -> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) RReft
ureft) :: PartialSpecType
partialTp' :: PartialSpecType
partialTp' = PartialSpecType
partialTp PartialSpecType -> PartialSpecType -> PartialSpecType
forall a b.
Free (RTypeF RTyCon RTyVar RReft) a
-> Free (RTypeF RTyCon RTyVar RReft) b
-> Free (RTypeF RTyCon RTyVar RReft) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PartialSpecType
partialFunTp :: PartialSpecType
(RType RTyCon RTyVar RReft
eTin , [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
tin
(RType RTyCon RTyVar RReft
eTout, [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp' CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
tout
let buildRFunContTrivial :: TcRn (RType RTyCon RTyVar RReft, [Symbol])
buildRFunContTrivial
| RType RTyCon RTyVar RReft -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin, Symbol
dictBinder : [Symbol]
bs0' <- [Symbol]
bs' = do
let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
[Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs0')
(RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( [Char] -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RFunTrivial0"
(RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Symbol
-> RFInfo
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
dictBinder RFInfo
i RType RTyCon RTyVar RReft
eTin RType RTyCon RTyVar RReft
eToutRenamed RReft
ureft
, [Symbol]
canonicalBinders
)
| Bool
otherwise = do
let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
[Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs')
(RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( [Char] -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RFunTrivial1" (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Symbol
-> RFInfo
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
bind RFInfo
i RType RTyCon RTyVar RReft
eTin RType RTyCon RTyVar RReft
eToutRenamed RReft
ureft
, [Symbol]
canonicalBinders
)
buildRFunCont :: [Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol])
buildRFunCont [Symbol]
bs'' Expr
ee
| RType RTyCon RTyVar RReft -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin, Symbol
dictBinder : [Symbol]
bs0' <- [Symbol]
bs' = do
let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
[Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs0')
(Expr
eeRenamed, [Symbol]
canonicalBinders') =
[Symbol] -> (Expr, [Symbol]) -> (Expr, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
canonicalBinders (Expr
ee, [Symbol]
bs'')
(RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( Symbol
-> RFInfo
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
dictBinder RFInfo
i
RType RTyCon RTyVar RReft
eTin
RType RTyCon RTyVar RReft
eToutRenamed
(Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
, [Symbol]
canonicalBinders'
)
| Bool
otherwise = do
let (RType RTyCon RTyVar RReft
eToutRenamed, [Symbol]
canonicalBinders) =
[Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTout, [Symbol]
bs')
(Expr
eeRenamed, [Symbol]
canonicalBinders') =
[Symbol] -> (Expr, [Symbol]) -> (Expr, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
canonicalBinders (Expr
ee, [Symbol]
bs'')
(RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( Symbol
-> RFInfo
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
bind RFInfo
i
RType RTyCon RTyVar RReft
eTin
RType RTyCon RTyVar RReft
eToutRenamed
(Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
, [Symbol]
canonicalBinders'
)
(Reft, RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> ([Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft (Reft
reft, RType RTyCon RTyVar RReft
t) TcRn (RType RTyCon RTyVar RReft, [Symbol])
buildRFunContTrivial [Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol])
buildRFunCont
RAllT (RTVar RTyVar
tv RTVInfo (RType RTyCon RTyVar ())
ty) RType RTyCon RTyVar RReft
tout ureft :: RReft
ureft@(MkUReft ref :: Reft
ref@(F.Reft (Symbol
vv, Expr
_oldE)) Predicate
p) -> do
(RType RTyCon RTyVar RReft
eTout, [Symbol]
bs) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType'
(PartialSpecType
partialTp PartialSpecType -> PartialSpecType -> PartialSpecType
forall a b.
Free (RTypeF RTyCon RTyVar RReft) a
-> Free (RTypeF RTyCon RTyVar RReft) b
-> Free (RTypeF RTyCon RTyVar RReft) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (RTVar RTyVar (RType RTyCon RTyVar ())
-> PartialSpecType
-> RReft
-> RTypeF RTyCon RTyVar RReft PartialSpecType
forall c tv r f. RTVU c tv -> f -> r -> RTypeF c tv r f
RAllTF (RTyVar
-> RTVInfo (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RType RTyCon RTyVar ())
ty) (() -> PartialSpecType
forall a. a -> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) RReft
ureft))
CoreExpr -> Expr
coreToLogic
CoreExpr -> TcRn CoreExpr
simplify
RType RTyCon RTyVar RReft
tout
(Reft, RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> ([Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
(Reft
ref, RTyVar -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
tv RReft
forall a. Monoid a => a
mempty)
((RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTVar RTyVar (RType RTyCon RTyVar ())
-> RType RTyCon RTyVar RReft -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (RTyVar
-> RTVInfo (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RType RTyCon RTyVar ())
ty) RType RTyCon RTyVar RReft
eTout RReft
ureft, [Symbol]
bs))
(\[Symbol]
bs' Expr
ee ->
let (Expr
eeRenamed, [Symbol]
canonicalBinders) =
[Symbol] -> (Expr, [Symbol]) -> (Expr, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (Expr
ee, [Symbol]
bs')
in (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( RTVar RTyVar (RType RTyCon RTyVar ())
-> RType RTyCon RTyVar RReft -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (RTyVar
-> RTVInfo (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
tv RTVInfo (RType RTyCon RTyVar ())
ty) RType RTyCon RTyVar RReft
eTout (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
, [Symbol]
canonicalBinders
)
)
RAllP PVU RTyCon RTyVar
pvbind RType RTyCon RTyVar RReft
tout -> do
(RType RTyCon RTyVar RReft
eTout, [Symbol]
bts') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType'
(PartialSpecType
partialTp PartialSpecType -> PartialSpecType -> PartialSpecType
forall a b.
Free (RTypeF RTyCon RTyVar RReft) a
-> Free (RTypeF RTyCon RTyVar RReft) b
-> Free (RTypeF RTyCon RTyVar RReft) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RTypeF RTyCon RTyVar RReft PartialSpecType -> PartialSpecType
forall (f :: * -> *) a. f (Free f a) -> Free f a
Free (PVU RTyCon RTyVar
-> PartialSpecType -> RTypeF RTyCon RTyVar RReft PartialSpecType
forall c tv r f. PVU c tv -> f -> RTypeF c tv r f
RAllPF PVU RTyCon RTyVar
pvbind (() -> PartialSpecType
forall a. a -> Free (RTypeF RTyCon RTyVar RReft) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())))
CoreExpr -> Expr
coreToLogic
CoreExpr -> TcRn CoreExpr
simplify
RType RTyCon RTyVar RReft
tout
(RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PVU RTyCon RTyVar
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU RTyCon RTyVar
pvbind RType RTyCon RTyVar RReft
eTout, [Symbol]
bts')
RApp RTyCon
tycon [RType RTyCon RTyVar RReft]
args [RTProp RTyCon RTyVar RReft]
pargs ureft :: RReft
ureft@(MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_)) Predicate
p)
| RTyCon -> Bool
forall c. TyConable c => c -> Bool
isClass RTyCon
tycon -> (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RType RTyCon RTyVar RReft
t, [])
| Bool
otherwise -> do
[RType RTyCon RTyVar RReft]
args' <- (RType RTyCon RTyVar RReft -> TcRn (RType RTyCon RTyVar RReft))
-> [RType RTyCon RTyVar RReft]
-> IOEnv (Env TcGblEnv TcLclEnv) [RType RTyCon RTyVar RReft]
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
(((RType RTyCon RTyVar RReft, [Symbol])
-> RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft)
forall a b.
(a -> b)
-> IOEnv (Env TcGblEnv TcLclEnv) a
-> IOEnv (Env TcGblEnv TcLclEnv) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RType RTyCon RTyVar RReft, [Symbol]) -> RType RTyCon RTyVar RReft
forall a b. (a, b) -> a
fst (TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft))
-> (RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify)
[RType RTyCon RTyVar RReft]
args
(Reft, RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> ([Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
(Reft
reft, RType RTyCon RTyVar RReft
t)
((RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTyCon
-> [RType RTyCon RTyVar RReft]
-> [RTProp RTyCon RTyVar RReft]
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
tycon [RType RTyCon RTyVar RReft]
args' [RTProp RTyCon RTyVar RReft]
pargs RReft
ureft, []))
(\[Symbol]
bs' Expr
ee ->
(RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTyCon
-> [RType RTyCon RTyVar RReft]
-> [RTProp RTyCon RTyVar RReft]
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
tycon [RType RTyCon RTyVar RReft]
args' [RTProp RTyCon RTyVar RReft]
pargs (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
ee)) Predicate
p), [Symbol]
bs')
)
RAppTy RType RTyCon RTyVar RReft
arg RType RTyCon RTyVar RReft
res ureft :: RReft
ureft@(MkUReft reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
_)) Predicate
p) -> do
(RType RTyCon RTyVar RReft
eArg, [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
arg
(RType RTyCon RTyVar RReft
eRes, [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
res
let (RType RTyCon RTyVar RReft
eResRenamed, [Symbol]
canonicalBinders) =
[Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eRes, [Symbol]
bs')
(Reft, RType RTyCon RTyVar RReft)
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
-> ([Symbol] -> Expr -> TcRn (RType RTyCon RTyVar RReft, [Symbol]))
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft
(Reft
reft, RType RTyCon RTyVar RReft
t)
((RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType RTyCon RTyVar RReft
eArg RType RTyCon RTyVar RReft
eResRenamed RReft
ureft, [Symbol]
canonicalBinders))
(\[Symbol]
bs'' Expr
ee ->
let (Expr
eeRenamed, [Symbol]
canonicalBinders') =
[Symbol] -> (Expr, [Symbol]) -> (Expr, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
canonicalBinders (Expr
ee, [Symbol]
bs'')
in (RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType RTyCon RTyVar RReft
eArg RType RTyCon RTyVar RReft
eResRenamed (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
vv, Expr
eeRenamed)) Predicate
p)
, [Symbol]
canonicalBinders'
)
)
RAllE Symbol
bind RType RTyCon RTyVar RReft
allarg RType RTyCon RTyVar RReft
ty -> do
(RType RTyCon RTyVar RReft
eAllarg, [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
allarg
(RType RTyCon RTyVar RReft
eTy , [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
ty
let (RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders) = [Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTy, [Symbol]
bs')
(RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Symbol
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
bind RType RTyCon RTyVar RReft
eAllarg RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders)
REx Symbol
bind RType RTyCon RTyVar RReft
allarg RType RTyCon RTyVar RReft
ty -> do
(RType RTyCon RTyVar RReft
eAllarg, [Symbol]
bs ) <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
allarg
(RType RTyCon RTyVar RReft
eTy , [Symbol]
bs') <- PartialSpecType
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> RType RTyCon RTyVar RReft
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
elaborateSpecType' PartialSpecType
partialTp CoreExpr -> Expr
coreToLogic CoreExpr -> TcRn CoreExpr
simplify RType RTyCon RTyVar RReft
ty
let (RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders) = [Symbol]
-> (RType RTyCon RTyVar RReft, [Symbol])
-> (RType RTyCon RTyVar RReft, [Symbol])
forall a. Subable a => [Symbol] -> (a, [Symbol]) -> (a, [Symbol])
canonicalizeDictBinder [Symbol]
bs (RType RTyCon RTyVar RReft
eTy, [Symbol]
bs')
(RType RTyCon RTyVar RReft, [Symbol])
-> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Symbol
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
bind RType RTyCon RTyVar RReft
eAllarg RType RTyCon RTyVar RReft
eTyRenamed, [Symbol]
canonicalBinders)
RExprArg Located Expr
_ -> Maybe SrcSpan
-> [Char] -> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"RExprArg should not appear here"
RHole RReft
_ -> Maybe SrcSpan
-> [Char] -> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"RHole should not appear here"
RRTy{} -> Maybe SrcSpan
-> [Char] -> TcRn (RType RTyCon RTyVar RReft, [Symbol])
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"Not sure how to elaborate RRTy" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RType RTyCon RTyVar RReft -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp RType RTyCon RTyVar RReft
t)
where
boolType :: RType RTyCon RTyVar RReft
boolType = RTyCon
-> [RType RTyCon RTyVar RReft]
-> [RTProp RTyCon RTyVar RReft]
-> RReft
-> RType RTyCon RTyVar RReft
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (TyCon -> [PVU RTyCon RTyVar] -> TyConInfo -> RTyCon
RTyCon TyCon
boolTyCon [] TyConInfo
forall a. Default a => a
def) [] [] RReft
forall a. Monoid a => a
mempty :: SpecType
elaborateReft
:: (F.PPrint a)
=> (F.Reft, SpecType)
-> TcRn a
-> ([F.Symbol] -> F.Expr -> TcRn a)
-> TcRn a
elaborateReft :: forall a.
PPrint a =>
(Reft, RType RTyCon RTyVar RReft)
-> TcRn a -> ([Symbol] -> Expr -> TcRn a) -> TcRn a
elaborateReft (reft :: Reft
reft@(F.Reft (Symbol
vv, Expr
e)), RType RTyCon RTyVar RReft
vvTy) TcRn a
trivial [Symbol] -> Expr -> TcRn a
nonTrivialCont =
if Reft -> Bool
isTrivial' Reft
reft
then TcRn a
trivial
else do
let
querySpecType :: RType RTyCon RTyVar RReft
querySpecType =
RType RTyCon RTyVar RReft
-> PartialSpecType -> RType RTyCon RTyVar RReft
plugType (RFInfo
-> Symbol
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall r c tv.
Monoid r =>
RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' (Bool -> RFInfo
classRFInfo Bool
True) Symbol
vv RType RTyCon RTyVar RReft
vvTy RType RTyCon RTyVar RReft
boolType) PartialSpecType
partialTp :: SpecType
([Symbol]
origBinders, [Symbol]
origTyBinders) = [Char] -> ([Symbol], [Symbol]) -> ([Symbol], [Symbol])
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"collectSpecTypeBinders"
(([Symbol], [Symbol]) -> ([Symbol], [Symbol]))
-> ([Symbol], [Symbol]) -> ([Symbol], [Symbol])
forall a b. (a -> b) -> a -> b
$ RType RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders RType RTyCon RTyVar RReft
querySpecType
hsExpr :: LHsExpr GhcPs
hsExpr =
LHsExpr GhcPs -> RType RTyCon RTyVar RReft -> LHsExpr GhcPs
buildHsExpr (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr ([Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Symbol]
origBinders) Expr
e)
RType RTyCon RTyVar RReft
querySpecType :: LHsExpr GhcPs
exprWithTySigs :: GenLocated SrcSpanAnnA (HsExpr GhcPs)
exprWithTySigs = HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a an. a -> LocatedAn an a
noLocA (HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs))
-> HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ XExprWithTySig GhcPs
-> LHsExpr GhcPs -> LHsSigWcType (NoGhcTc GhcPs) -> HsExpr GhcPs
forall p.
XExprWithTySig p
-> LHsExpr p -> LHsSigWcType (NoGhcTc p) -> HsExpr p
ExprWithTySig
XExprWithTySig GhcPs
EpAnn [AddEpAnn]
forall a. EpAnn a
noAnn
LHsExpr GhcPs
hsExpr
(LHsType GhcPs -> LHsSigWcType GhcPs
hsTypeToHsSigWcType (RType RTyCon RTyVar RReft -> LHsType GhcPs
specTypeToLHsType RType RTyCon RTyVar RReft
querySpecType))
CoreExpr
eeWithLamsCore <- LHsExpr GhcPs -> TcRn CoreExpr
GM.elabRnExpr LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
exprWithTySigs
CoreExpr
eeWithLamsCore' <- CoreExpr -> TcRn CoreExpr
simplify CoreExpr
eeWithLamsCore
let
([Symbol]
_, [Symbol]
tyBinders) =
RType RTyCon RTyVar RReft -> ([Symbol], [Symbol])
collectSpecTypeBinders
(RType RTyCon RTyVar RReft -> ([Symbol], [Symbol]))
-> (CoreExpr -> RType RTyCon RTyVar RReft)
-> CoreExpr
-> ([Symbol], [Symbol])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> RType RTyCon RTyVar RReft
forall r. Monoid r => Type -> RRType r
ofType
(Type -> RType RTyCon RTyVar RReft)
-> (CoreExpr -> Type) -> CoreExpr -> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
exprType
(CoreExpr -> ([Symbol], [Symbol]))
-> CoreExpr -> ([Symbol], [Symbol])
forall a b. (a -> b) -> a -> b
$ CoreExpr
eeWithLamsCore'
substTy' :: [(Symbol, Symbol)]
substTy' = [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
tyBinders [Symbol]
origTyBinders
eeWithLams :: Expr
eeWithLams =
CoreExpr -> Expr
coreToLogic ([Char] -> CoreExpr -> CoreExpr
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"eeWithLamsCore" CoreExpr
eeWithLamsCore')
([Symbol]
bs', Expr
ee) = [Char] -> ([Symbol], Expr) -> ([Symbol], Expr)
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"grabLams" (([Symbol], Expr) -> ([Symbol], Expr))
-> ([Symbol], Expr) -> ([Symbol], Expr)
forall a b. (a -> b) -> a -> b
$ ([Symbol], Expr) -> ([Symbol], Expr)
grabLams ([], Expr
eeWithLams)
([Symbol]
dictbs, [Symbol]
nondictbs) =
(Symbol -> Bool) -> [Symbol] -> ([Symbol], [Symbol])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Symbol -> Symbol -> Bool
F.isPrefixOfSym Symbol
"$d") [Symbol]
bs'
subst :: [(Symbol, Symbol)]
subst = if [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
nondictbs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
origBinders
then [Char] -> [(Symbol, Symbol)] -> [(Symbol, Symbol)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"SUBST" ([(Symbol, Symbol)] -> [(Symbol, Symbol)])
-> [(Symbol, Symbol)] -> [(Symbol, Symbol)]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Symbol] -> [Symbol]
forall a. [a] -> [a]
L.reverse [Symbol]
nondictbs) [Symbol]
origBinders
else Maybe SrcSpan -> [Char] -> [(Symbol, Symbol)]
forall a. Maybe SrcSpan -> [Char] -> a
panic
Maybe SrcSpan
forall a. Maybe a
Nothing
[Char]
"Oops, Ghc gave back more/less binders than I expected"
a
ret <- [Symbol] -> Expr -> TcRn a
nonTrivialCont
[Symbol]
dictbs
( (Symbol -> Symbol) -> Expr -> Expr
renameBinderCoerc (\Symbol
x -> Symbol -> Maybe Symbol -> Symbol
forall a. a -> Maybe a -> a
Mb.fromMaybe Symbol
x (Symbol -> [(Symbol, Symbol)] -> Maybe Symbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Symbol
x [(Symbol, Symbol)]
substTy'))
(Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Symbol) -> Expr -> Expr
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa (\Symbol
x -> Symbol -> Maybe Symbol -> Symbol
forall a. a -> Maybe a -> a
Mb.fromMaybe Symbol
x (Symbol -> [(Symbol, Symbol)] -> Maybe Symbol
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Symbol
x [(Symbol, Symbol)]
subst))
(Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
F.notracepp
( [Char]
"elaborated: subst "
[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Symbol)] -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp [(Symbol, Symbol)]
substTy'
[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" "
[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RType RTyCon RTyVar RReft -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp
(Type -> RType RTyCon RTyVar RReft
forall r. Monoid r => Type -> RRType r
ofType (Type -> RType RTyCon RTyVar RReft)
-> Type -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
eeWithLamsCore' :: SpecType)
)
Expr
ee
)
a -> TcRn a
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> a -> a
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"result" a
ret)
isTrivial' :: F.Reft -> Bool
isTrivial' :: Reft -> Bool
isTrivial' (F.Reft (Symbol
_, Expr
F.PTrue)) = Bool
True
isTrivial' Reft
_ = Bool
False
grabLams :: ([F.Symbol], F.Expr) -> ([F.Symbol], F.Expr)
grabLams :: ([Symbol], Expr) -> ([Symbol], Expr)
grabLams ([Symbol]
bs, F.ELam (Symbol
b, Sort
_) Expr
e) = ([Symbol], Expr) -> ([Symbol], Expr)
grabLams (Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
bs, Expr
e)
grabLams ([Symbol], Expr)
bse = ([Symbol], Expr)
bse
renameBinderCoerc :: (F.Symbol -> F.Symbol) -> F.Expr -> F.Expr
renameBinderCoerc :: (Symbol -> Symbol) -> Expr -> Expr
renameBinderCoerc Symbol -> Symbol
f = Expr -> Expr
rename
where
renameSort :: Sort -> Sort
renameSort = (Symbol -> Symbol) -> Sort -> Sort
renameBinderSort Symbol -> Symbol
f
rename :: Expr -> Expr
rename e' :: Expr
e'@(F.ESym SymConst
_ ) = Expr
e'
rename e' :: Expr
e'@(F.ECon Constant
_ ) = Expr
e'
rename e' :: Expr
e'@(F.EVar Symbol
_ ) = Expr
e'
rename ( F.EApp Expr
e0 Expr
e1 ) = Expr -> Expr -> Expr
F.EApp (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
rename ( F.ENeg Expr
e0 ) = Expr -> Expr
F.ENeg (Expr -> Expr
rename Expr
e0)
rename ( F.EBin Bop
bop Expr
e0 Expr
e1 ) = Bop -> Expr -> Expr -> Expr
F.EBin Bop
bop (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
rename ( F.EIte Expr
e0 Expr
e1 Expr
e2 ) = Expr -> Expr -> Expr -> Expr
F.EIte (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1) (Expr -> Expr
rename Expr
e2)
rename ( F.ECst Expr
e' Sort
t ) = Expr -> Sort -> Expr
F.ECst (Expr -> Expr
rename Expr
e') (Sort -> Sort
renameSort Sort
t)
rename ( F.PAnd [Expr]
es ) = [Expr] -> Expr
F.PAnd (Expr -> Expr
rename (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
rename ( F.POr [Expr]
es ) = [Expr] -> Expr
F.POr (Expr -> Expr
rename (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
rename ( F.PNot Expr
e' ) = Expr -> Expr
F.PNot (Expr -> Expr
rename Expr
e')
rename ( F.PImp Expr
e0 Expr
e1 ) = Expr -> Expr -> Expr
F.PImp (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
rename ( F.PIff Expr
e0 Expr
e1 ) = Expr -> Expr -> Expr
F.PIff (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
rename ( F.PAtom Brel
brel Expr
e0 Expr
e1) = Brel -> Expr -> Expr -> Expr
F.PAtom Brel
brel (Expr -> Expr
rename Expr
e0) (Expr -> Expr
rename Expr
e1)
rename (F.ECoerc Sort
_ Sort
_ Expr
e') = Expr -> Expr
rename Expr
e'
rename Expr
e = Maybe SrcSpan -> [Char] -> Expr
forall a. Maybe SrcSpan -> [Char] -> a
panic
Maybe SrcSpan
forall a. Maybe a
Nothing
([Char]
"renameBinderCoerc: Not sure how to handle the expression " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Expr
e)
renameBinderSort :: (F.Symbol -> F.Symbol) -> F.Sort -> F.Sort
renameBinderSort :: (Symbol -> Symbol) -> Sort -> Sort
renameBinderSort Symbol -> Symbol
f = Sort -> Sort
rename
where
rename :: Sort -> Sort
rename Sort
F.FInt = Sort
F.FInt
rename Sort
F.FReal = Sort
F.FReal
rename Sort
F.FNum = Sort
F.FNum
rename Sort
F.FFrac = Sort
F.FFrac
rename ( F.FObj Symbol
s ) = Symbol -> Sort
F.FObj (Symbol -> Symbol
f Symbol
s)
rename t' :: Sort
t'@(F.FVar Int
_ ) = Sort
t'
rename ( F.FFunc Sort
t0 Sort
t1) = Sort -> Sort -> Sort
F.FFunc (Sort -> Sort
rename Sort
t0) (Sort -> Sort
rename Sort
t1)
rename ( F.FAbs Int
x Sort
t') = Int -> Sort -> Sort
F.FAbs Int
x (Sort -> Sort
rename Sort
t')
rename t' :: Sort
t'@(F.FTC FTycon
_ ) = Sort
t'
rename ( F.FApp Sort
t0 Sort
t1 ) = Sort -> Sort -> Sort
F.FApp (Sort -> Sort
rename Sort
t0) (Sort -> Sort
rename Sort
t1)
mkHsTyConApp :: IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
mkHsTyConApp :: IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
mkHsTyConApp IdP GhcPs
tyconId [LHsType GhcPs]
tyargs = PromotionFlag
-> LexicalFixity
-> IdP GhcPs
-> [LHsTypeArg GhcPs]
-> LHsType GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
PromotionFlag
-> LexicalFixity
-> IdP (GhcPass p)
-> [LHsTypeArg (GhcPass p)]
-> LHsType (GhcPass p)
nlHsTyConApp PromotionFlag
NotPromoted LexicalFixity
Prefix IdP GhcPs
tyconId ((GenLocated SrcSpanAnnA (HsType GhcPs)
-> HsArg
(GenLocated SrcSpanAnnA (HsType GhcPs))
(GenLocated SrcSpanAnnA (HsType GhcPs)))
-> [GenLocated SrcSpanAnnA (HsType GhcPs)]
-> [HsArg
(GenLocated SrcSpanAnnA (HsType GhcPs))
(GenLocated SrcSpanAnnA (HsType GhcPs))]
forall a b. (a -> b) -> [a] -> [b]
map GenLocated SrcSpanAnnA (HsType GhcPs)
-> HsArg
(GenLocated SrcSpanAnnA (HsType GhcPs))
(GenLocated SrcSpanAnnA (HsType GhcPs))
forall tm ty. tm -> HsArg tm ty
HsValArg [LHsType GhcPs]
[GenLocated SrcSpanAnnA (HsType GhcPs)]
tyargs)
fixExprToHsExpr :: S.HashSet F.Symbol -> F.Expr -> LHsExpr GhcPs
fixExprToHsExpr :: HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
_ (F.ECon Constant
c) = Constant -> LHsExpr GhcPs
constantToHsExpr Constant
c
fixExprToHsExpr HashSet Symbol
env (F.EVar Symbol
x)
| Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Types.[]" = [Char] -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"Empty" (LHsExpr GhcPs -> LHsExpr GhcPs) -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"[]"))
| Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Types.:" = [Char] -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"Cons" (LHsExpr GhcPs -> LHsExpr GhcPs) -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
":"))
| Bool
otherwise = [Char] -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"Var" (LHsExpr GhcPs -> LHsExpr GhcPs) -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (HashSet Symbol -> Symbol -> RdrName
symbolToRdrName HashSet Symbol
env Symbol
x)
fixExprToHsExpr HashSet Symbol
env (F.EApp Expr
e0 Expr
e1) =
LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
env (F.ENeg Expr
e) =
LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (Name -> RdrName
nameRdrName Name
negateName)) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e)
fixExprToHsExpr HashSet Symbol
env (F.EBin Bop
bop Expr
e0 Expr
e1) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
(LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (Bop -> LHsExpr GhcPs
bopToHsExpr Bop
bop) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0))
(HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
env (F.EIte Expr
p Expr
e0 Expr
e1) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
nlHsIf (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
p)
(HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0)
(HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
env (F.ECst Expr
e0 Sort
_ ) = HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0
fixExprToHsExpr HashSet Symbol
_ (F.PAnd [] ) = IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar IdP GhcPs
RdrName
true_RDR
fixExprToHsExpr HashSet Symbol
env (F.PAnd (Expr
e : [Expr]
es)) = (Expr
-> GenLocated SrcSpanAnnA (HsExpr GhcPs)
-> GenLocated SrcSpanAnnA (HsExpr GhcPs))
-> GenLocated SrcSpanAnnA (HsExpr GhcPs)
-> [Expr]
-> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr Expr -> GenLocated SrcSpanAnnA (HsExpr GhcPs) -> LHsExpr GhcPs
Expr
-> GenLocated SrcSpanAnnA (HsExpr GhcPs)
-> GenLocated SrcSpanAnnA (HsExpr GhcPs)
f (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e) [Expr]
es
where
f :: Expr -> GenLocated SrcSpanAnnA (HsExpr GhcPs) -> LHsExpr GhcPs
f Expr
x GenLocated SrcSpanAnnA (HsExpr GhcPs)
acc = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar IdP GhcPs
RdrName
and_RDR) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
x)) LHsExpr GhcPs
GenLocated SrcSpanAnnA (HsExpr GhcPs)
acc
fixExprToHsExpr HashSet Symbol
env (F.POr [Expr]
es) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
(IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (Module -> FastString -> RdrName
varQual_RDR Module
dATA_FOLDABLE ([Char] -> FastString
fsLit [Char]
"or")))
([LHsExpr GhcPs] -> LHsExpr GhcPs
nlList ([LHsExpr GhcPs] -> LHsExpr GhcPs)
-> [LHsExpr GhcPs] -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env (Expr -> GenLocated SrcSpanAnnA (HsExpr GhcPs))
-> [Expr] -> [GenLocated SrcSpanAnnA (HsExpr GhcPs)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
fixExprToHsExpr HashSet Symbol
env (F.PIff Expr
e0 Expr
e1) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
(LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"<=>"))) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0)
)
(HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
env (F.PNot Expr
e) =
LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar IdP GhcPs
RdrName
not_RDR) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e)
fixExprToHsExpr HashSet Symbol
env (F.PAtom Brel
brel Expr
e0 Expr
e1) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
(LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (Brel -> LHsExpr GhcPs
brelToHsExpr Brel
brel) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0))
(HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
env (F.PImp Expr
e0 Expr
e1) = LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp
(LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
forall (id :: Pass).
LHsExpr (GhcPass id)
-> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id)
mkHsApp (IdP GhcPs -> LHsExpr GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
IdP (GhcPass p) -> LHsExpr (GhcPass p)
nlHsVar (FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"==>"))) (HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e0)
)
(HashSet Symbol -> Expr -> LHsExpr GhcPs
fixExprToHsExpr HashSet Symbol
env Expr
e1)
fixExprToHsExpr HashSet Symbol
_ Expr
e =
Maybe SrcSpan -> [Char] -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"toGhcExpr: Don't know how to handle " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. Show a => a -> [Char]
show Expr
e)
constantToHsExpr :: F.Constant -> LHsExpr GhcPs
constantToHsExpr :: Constant -> LHsExpr GhcPs
constantToHsExpr (F.I Integer
i) =
HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a an. a -> LocatedAn an a
noLocA (XOverLitE GhcPs -> HsOverLit GhcPs -> HsExpr GhcPs
forall p. XOverLitE p -> HsOverLit p -> HsExpr p
HsOverLit XOverLitE GhcPs
EpAnn NoEpAnns
forall a. EpAnn a
noAnn (IntegralLit -> HsOverLit GhcPs
mkHsIntegral (Integer -> IntegralLit
forall a. Integral a => a -> IntegralLit
mkIntegralLit Integer
i)))
constantToHsExpr (F.R Double
d) =
HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a an. a -> LocatedAn an a
noLocA (XOverLitE GhcPs -> HsOverLit GhcPs -> HsExpr GhcPs
forall p. XOverLitE p -> HsOverLit p -> HsExpr p
HsOverLit XOverLitE GhcPs
EpAnn NoEpAnns
forall a. EpAnn a
noAnn (FractionalLit -> HsOverLit GhcPs
mkHsFractional (Rational -> FractionalLit
mkTHFractionalLit (Double -> Rational
forall a. Real a => a -> Rational
toRational Double
d))))
constantToHsExpr Constant
_ =
Maybe SrcSpan -> [Char] -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"constantToHsExpr: Not sure how to handle constructor L"
bopToHsExpr :: F.Bop -> LHsExpr GhcPs
bopToHsExpr :: Bop -> LHsExpr GhcPs
bopToHsExpr Bop
bop = HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a an. a -> LocatedAn an a
noLocA (XVar GhcPs -> LIdP GhcPs -> HsExpr GhcPs
forall p. XVar p -> LIdP p -> HsExpr p
HsVar XVar GhcPs
NoExtField
Ghc.noExtField (RdrName -> GenLocated SrcSpanAnnN RdrName
forall a an. a -> LocatedAn an a
noLocA (Bop -> RdrName
f Bop
bop)))
where
f :: Bop -> RdrName
f Bop
F.Plus = RdrName
plus_RDR
f Bop
F.Minus = RdrName
minus_RDR
f Bop
F.Times = RdrName
times_RDR
f Bop
F.Div = FastString -> RdrName
mkVarUnqual ([Char] -> FastString
fsLit [Char]
"/")
f Bop
F.Mod = FastString -> RdrName
GM.prependGHCRealQual ([Char] -> FastString
fsLit [Char]
"mod")
f Bop
F.RTimes = RdrName
times_RDR
f Bop
F.RDiv = FastString -> RdrName
GM.prependGHCRealQual ([Char] -> FastString
fsLit [Char]
"/")
brelToHsExpr :: F.Brel -> LHsExpr GhcPs
brelToHsExpr :: Brel -> LHsExpr GhcPs
brelToHsExpr Brel
brel = HsExpr GhcPs -> GenLocated SrcSpanAnnA (HsExpr GhcPs)
forall a an. a -> LocatedAn an a
noLocA (XVar GhcPs -> LIdP GhcPs -> HsExpr GhcPs
forall p. XVar p -> LIdP p -> HsExpr p
HsVar XVar GhcPs
NoExtField
Ghc.noExtField (RdrName -> GenLocated SrcSpanAnnN RdrName
forall a an. a -> LocatedAn an a
noLocA (Brel -> RdrName
f Brel
brel)))
where
f :: Brel -> RdrName
f Brel
F.Eq = FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"==")
f Brel
F.Gt = RdrName
gt_RDR
f Brel
F.Lt = RdrName
lt_RDR
f Brel
F.Ge = RdrName
ge_RDR
f Brel
F.Le = RdrName
le_RDR
f Brel
F.Ne = FastString -> RdrName
mkVarUnqual ([Char] -> FastString
mkFastString [Char]
"/=")
f Brel
_ = Maybe SrcSpan -> [Char] -> RdrName
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"brelToExpr: Unsupported operation"
symbolToRdrNameNs :: NameSpace -> F.Symbol -> RdrName
symbolToRdrNameNs :: NameSpace -> Symbol -> RdrName
symbolToRdrNameNs NameSpace
ns Symbol
x
| Symbol -> Bool
F.isNonSymbol Symbol
modName = NameSpace -> FastString -> RdrName
mkUnqual NameSpace
ns ([Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
s))
| Bool
otherwise = NameSpace -> (FastString, FastString) -> RdrName
mkQual
NameSpace
ns
([Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
modName), [Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
s))
where (Symbol
modName, Symbol
s) = Symbol -> (Symbol, Symbol)
GM.splitModuleName Symbol
x
varSymbolToRdrName :: F.Symbol -> RdrName
varSymbolToRdrName :: Symbol -> RdrName
varSymbolToRdrName = NameSpace -> Symbol -> RdrName
symbolToRdrNameNs NameSpace
varName
symbolToRdrName :: S.HashSet F.Symbol -> F.Symbol -> RdrName
symbolToRdrName :: HashSet Symbol -> Symbol -> RdrName
symbolToRdrName HashSet Symbol
env Symbol
x
| Symbol -> Bool
F.isNonSymbol Symbol
modName = NameSpace -> FastString -> RdrName
mkUnqual NameSpace
ns ([Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
s))
| Bool
otherwise = NameSpace -> (FastString, FastString) -> RdrName
mkQual
NameSpace
ns
([Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
modName), [Char] -> FastString
mkFastString (Symbol -> [Char]
F.symbolString Symbol
s))
where
(Symbol
modName, Symbol
s) = Symbol -> (Symbol, Symbol)
GM.splitModuleName Symbol
x
ns :: NameSpace
ns | Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x HashSet Symbol
env), Just (Char
c, Symbol
_) <- Symbol -> Maybe (Char, Symbol)
F.unconsSym Symbol
s, Char -> Bool
isUpper Char
c = NameSpace
dataName
| Bool
otherwise = NameSpace
varName
specTypeToLHsType :: SpecType -> LHsType GhcPs
specTypeToLHsType :: RType RTyCon RTyVar RReft -> LHsType GhcPs
specTypeToLHsType =
((RTypeF
RTyCon
RTyVar
RReft
(RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
-> GenLocated SrcSpanAnnA (HsType GhcPs))
-> (RType RTyCon RTyVar RReft
-> RTypeF
RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft)))
-> RType RTyCon RTyVar RReft
-> LHsType GhcPs)
-> (RType RTyCon RTyVar RReft
-> RTypeF
RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft)))
-> (RTypeF
RTyCon
RTyVar
RReft
(RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
-> GenLocated SrcSpanAnnA (HsType GhcPs))
-> RType RTyCon RTyVar RReft
-> LHsType GhcPs
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((forall c.
RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft, c)
-> (RType RTyCon RTyVar RReft, RTypeF RTyCon RTyVar RReft c))
-> (forall d.
Identity (RTypeF RTyCon RTyVar RReft d)
-> RTypeF RTyCon RTyVar RReft (Identity d))
-> (RTypeF
RTyCon
RTyVar
RReft
(RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
-> GenLocated SrcSpanAnnA (HsType GhcPs))
-> (RType RTyCon RTyVar RReft
-> RTypeF
RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft)))
-> RType RTyCon RTyVar RReft
-> GenLocated SrcSpanAnnA (HsType GhcPs)
forall (w :: * -> *) (f :: * -> *) (m :: * -> *) b a.
(Comonad w, Functor f, Monad m) =>
(forall c. f (w c) -> w (f c))
-> (forall d. m (f d) -> f (m d))
-> (f (w b) -> b)
-> (a -> f (m a))
-> a
-> b
ghylo (forall t a. Corecursive t => Base t (t, a) -> (t, Base t a)
distPara @SpecType) Identity (RTypeF RTyCon RTyVar RReft d)
-> RTypeF RTyCon RTyVar RReft (Identity d)
forall d.
Identity (RTypeF RTyCon RTyVar RReft d)
-> RTypeF RTyCon RTyVar RReft (Identity d)
forall (f :: * -> *) a.
Functor f =>
Identity (f a) -> f (Identity a)
distAna) ((RType RTyCon RTyVar RReft -> Identity (RType RTyCon RTyVar RReft))
-> RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft)
-> RTypeF
RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft))
forall a b.
(a -> b)
-> RTypeF RTyCon RTyVar RReft a -> RTypeF RTyCon RTyVar RReft b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RType RTyCon RTyVar RReft -> Identity (RType RTyCon RTyVar RReft)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft)
-> RTypeF
RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft)))
-> (RType RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft))
-> RType RTyCon RTyVar RReft
-> RTypeF
RTyCon RTyVar RReft (Identity (RType RTyCon RTyVar RReft))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType RTyCon RTyVar RReft
-> Base (RType RTyCon RTyVar RReft) (RType RTyCon RTyVar RReft)
RType RTyCon RTyVar RReft
-> RTypeF RTyCon RTyVar RReft (RType RTyCon RTyVar RReft)
forall t. Recursive t => t -> Base t t
project) ((RTypeF
RTyCon
RTyVar
RReft
(RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
-> GenLocated SrcSpanAnnA (HsType GhcPs))
-> RType RTyCon RTyVar RReft -> LHsType GhcPs)
-> (RTypeF
RTyCon
RTyVar
RReft
(RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
-> GenLocated SrcSpanAnnA (HsType GhcPs))
-> RType RTyCon RTyVar RReft
-> LHsType GhcPs
forall a b. (a -> b) -> a -> b
$ \case
RVarF (RTV TyVar
tv) RReft
_ -> PromotionFlag -> IdP GhcPs -> LHsType GhcPs
forall (p :: Pass) a.
IsSrcSpanAnn p a =>
PromotionFlag -> IdP (GhcPass p) -> LHsType (GhcPass p)
nlHsTyVar
PromotionFlag
NotPromoted
(NameSpace -> Symbol -> RdrName
symbolToRdrNameNs NameSpace
tvName (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyVar
tv))
RFunF Symbol
_ RFInfo
_ (RType RTyCon RTyVar RReft
tin, GenLocated SrcSpanAnnA (HsType GhcPs)
tin') (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
tout) RReft
_
| RType RTyCon RTyVar RReft -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType RTyCon RTyVar RReft
tin -> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a an. a -> LocatedAn an a
noLocA (HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs))
-> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a b. (a -> b) -> a -> b
$ XQualTy GhcPs -> LHsContext GhcPs -> LHsType GhcPs -> HsType GhcPs
forall pass.
XQualTy pass -> LHsContext pass -> LHsType pass -> HsType pass
HsQualTy XQualTy GhcPs
NoExtField
Ghc.noExtField ([GenLocated SrcSpanAnnA (HsType GhcPs)]
-> LocatedAn AnnContext [GenLocated SrcSpanAnnA (HsType GhcPs)]
forall a an. a -> LocatedAn an a
noLocA [GenLocated SrcSpanAnnA (HsType GhcPs)
tin']) LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tout
| Bool
otherwise -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tin' LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tout
RAllTF (RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value -> (RTV TyVar
tv)) (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
t) RReft
_ -> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a an. a -> LocatedAn an a
noLocA (HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs))
-> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a b. (a -> b) -> a -> b
$ XForAllTy GhcPs
-> HsForAllTelescope GhcPs -> LHsType GhcPs -> HsType GhcPs
forall pass.
XForAllTy pass
-> HsForAllTelescope pass -> LHsType pass -> HsType pass
HsForAllTy
XForAllTy GhcPs
NoExtField
Ghc.noExtField
(EpAnnForallTy
-> [LHsTyVarBndr Specificity GhcPs] -> HsForAllTelescope GhcPs
forall (p :: Pass).
EpAnnForallTy
-> [LHsTyVarBndr Specificity (GhcPass p)]
-> HsForAllTelescope (GhcPass p)
mkHsForAllInvisTele EpAnnForallTy
forall a. EpAnn a
noAnn [HsTyVarBndr Specificity GhcPs
-> LocatedAn AnnListItem (HsTyVarBndr Specificity GhcPs)
forall a an. a -> LocatedAn an a
noLocA (HsTyVarBndr Specificity GhcPs
-> LocatedAn AnnListItem (HsTyVarBndr Specificity GhcPs))
-> HsTyVarBndr Specificity GhcPs
-> LocatedAn AnnListItem (HsTyVarBndr Specificity GhcPs)
forall a b. (a -> b) -> a -> b
$ XUserTyVar GhcPs
-> Specificity -> LIdP GhcPs -> HsTyVarBndr Specificity GhcPs
forall flag pass.
XUserTyVar pass -> flag -> LIdP pass -> HsTyVarBndr flag pass
UserTyVar XUserTyVar GhcPs
EpAnn [AddEpAnn]
forall a. EpAnn a
noAnn Specificity
SpecifiedSpec (RdrName -> GenLocated SrcSpanAnnN RdrName
forall a an. a -> LocatedAn an a
noLocA (RdrName -> GenLocated SrcSpanAnnN RdrName)
-> RdrName -> GenLocated SrcSpanAnnN RdrName
forall a b. (a -> b) -> a -> b
$ NameSpace -> Symbol -> RdrName
symbolToRdrNameNs NameSpace
tvName (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyVar
tv))])
LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
t
RAllPF PVU RTyCon RTyVar
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
ty) -> GenLocated SrcSpanAnnA (HsType GhcPs)
ty
RAppF RTyCon { rtc_tc :: RTyCon -> TyCon
rtc_tc = TyCon
tc } [(RType RTyCon RTyVar RReft,
GenLocated SrcSpanAnnA (HsType GhcPs))]
ts [RTPropF
RTyCon
RTyVar
(RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))]
_ RReft
_ -> IdP GhcPs -> [LHsType GhcPs] -> LHsType GhcPs
mkHsTyConApp
(TyCon -> RdrName
forall thing. NamedThing thing => thing -> RdrName
getRdrName TyCon
tc)
[ LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
hst | (RType RTyCon RTyVar RReft
t, GenLocated SrcSpanAnnA (HsType GhcPs)
hst) <- [(RType RTyCon RTyVar RReft,
GenLocated SrcSpanAnnA (HsType GhcPs))]
ts, RType RTyCon RTyVar RReft -> Bool
forall {c} {tv} {r}. RType c tv r -> Bool
notExprArg RType RTyCon RTyVar RReft
t ]
where
notExprArg :: RType c tv r -> Bool
notExprArg (RExprArg Located Expr
_) = Bool
False
notExprArg RType c tv r
_ = Bool
True
RAllEF Symbol
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
tin) (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
tout) -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tin LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tout
RExF Symbol
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
tin) (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
tout) -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsFunTy LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tin LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
tout
RAppTyF (RType RTyCon RTyVar RReft, GenLocated SrcSpanAnnA (HsType GhcPs))
_ (RExprArg Located Expr
_, GenLocated SrcSpanAnnA (HsType GhcPs)
_) RReft
_ ->
Maybe SrcSpan -> [Char] -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"RExprArg should not appear here"
RAppTyF (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
t) (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
t') RReft
_ -> LHsType GhcPs -> LHsType GhcPs -> LHsType GhcPs
forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
nlHsAppTy LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
t LHsType GhcPs
GenLocated SrcSpanAnnA (HsType GhcPs)
t'
RRTyF [(Symbol,
(RType RTyCon RTyVar RReft,
GenLocated SrcSpanAnnA (HsType GhcPs)))]
_ RReft
_ Oblig
_ (RType RTyCon RTyVar RReft
_, GenLocated SrcSpanAnnA (HsType GhcPs)
t) -> GenLocated SrcSpanAnnA (HsType GhcPs)
t
RHoleF RReft
_ -> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a an. a -> LocatedAn an a
noLocA (HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs))
-> HsType GhcPs -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a b. (a -> b) -> a -> b
$ XWildCardTy GhcPs -> HsType GhcPs
forall pass. XWildCardTy pass -> HsType pass
HsWildCardTy XWildCardTy GhcPs
NoExtField
Ghc.noExtField
RExprArgF Located Expr
_ ->
Maybe SrcSpan -> [Char] -> GenLocated SrcSpanAnnA (HsType GhcPs)
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Oops, specTypeToLHsType doesn't know how to handle RExprArg"