{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE FlexibleContexts          #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Language.Haskell.Liquid.Bare.Typeclass
  ( compileClasses
  , elaborateClassDcp
  , makeClassAuxTypes
  -- , makeClassSelectorSigs
  )
where

-- TODO: Handle typeclasses with a single method (newtype)

import           Control.Monad                 ( forM, guard )
import           Data.Bifunctor                (second)
import qualified Data.List                     as L
import qualified Data.HashSet                  as S
import           Data.Hashable                  ()
import qualified Data.Maybe                    as Mb
import qualified Language.Fixpoint.Types       as F
import qualified Language.Fixpoint.Misc        as Misc
import           Language.Haskell.Liquid.Bare.Elaborate
import qualified Language.Haskell.Liquid.GHC.Misc
                                               as GM
import qualified Liquid.GHC.API
                                               as Ghc
import qualified Language.Haskell.Liquid.Misc  as Misc
import           Language.Haskell.Liquid.Types
import qualified Language.Haskell.Liquid.Types.RefType
                                               as RT
import qualified Language.Haskell.Liquid.Bare.Types
                                               as Bare
import qualified Language.Haskell.Liquid.Bare.Resolve
                                               as Bare
import qualified Language.Haskell.Liquid.Measure
                                               as Ms
-- import           Language.Haskell.Liquid.Types.Types
import qualified Data.HashMap.Strict           as M



compileClasses
  :: GhcSrc
  -> Bare.Env
  -> (ModName, Ms.BareSpec)
  -> [(ModName, Ms.BareSpec)]
  -> (Ms.BareSpec, [(Ghc.ClsInst, [Ghc.Var])])
compileClasses :: GhcSrc
-> Env
-> (ModName, BareSpec)
-> [(ModName, BareSpec)]
-> (BareSpec, [(ClsInst, [DFunId])])
compileClasses GhcSrc
src Env
env (ModName
name, BareSpec
spec) [(ModName, BareSpec)]
rest =
  (BareSpec
spec { sigs :: [(LocSymbol, LocBareType)]
sigs = [(LocSymbol, LocBareType)]
sigsNew } forall a. Semigroup a => a -> a -> a
<> forall {ty} {bndr}. Spec ty bndr
clsSpec, [(ClsInst, [DFunId])]
instmethods)
 where
  clsSpec :: Spec ty bndr
clsSpec = forall a. Monoid a => a
mempty
    { dataDecls :: [DataDecl]
dataDecls = [DataDecl]
clsDecls
    , reflects :: HashSet LocSymbol
reflects  = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"reflects " forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
                    (  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
                        ( forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Symbol -> Symbol
GM.dropModuleNames
                        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol
                        forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClsInst -> DFunId
Ghc.instanceDFunId
                        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst
                        )
                        [(ClsInst, Class)]
instClss
                    forall a. [a] -> [a] -> [a]
++ [LocSymbol]
methods
                    )
    }
  clsDecls :: [DataDecl]
clsDecls                = [(Class, [(DFunId, LocBareType)])] -> [DataDecl]
makeClassDataDecl (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Class [(DFunId, LocBareType)]
refinedMethods)
      -- class methods
  (HashMap Class [(DFunId, LocBareType)]
refinedMethods, [(LocSymbol, LocBareType)]
sigsNew) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall ty.
(LocSymbol, ty)
-> (HashMap Class [(DFunId, ty)], [(LocSymbol, ty)])
-> (HashMap Class [(DFunId, ty)], [(LocSymbol, ty)])
grabClassSig (forall a. Monoid a => a
mempty, forall a. Monoid a => a
mempty) (forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs BareSpec
spec)
  grabClassSig
    :: (F.LocSymbol, ty)
    -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.LocSymbol, ty)])
    -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.LocSymbol, ty)])
  grabClassSig :: forall ty.
(LocSymbol, ty)
-> (HashMap Class [(DFunId, ty)], [(LocSymbol, ty)])
-> (HashMap Class [(DFunId, ty)], [(LocSymbol, ty)])
grabClassSig sigPair :: (LocSymbol, ty)
sigPair@(LocSymbol
lsym, ty
ref) (HashMap Class [(DFunId, ty)]
refs, [(LocSymbol, ty)]
sigs') = case Maybe (Class, (DFunId, ty))
clsOp of
    Maybe (Class, (DFunId, ty))
Nothing         -> (HashMap Class [(DFunId, ty)]
refs, (LocSymbol, ty)
sigPair forall a. a -> [a] -> [a]
: [(LocSymbol, ty)]
sigs')
    Just (Class
cls, (DFunId, ty)
sig) -> (forall k v.
(Eq k, Hashable k) =>
(Maybe v -> Maybe v) -> k -> HashMap k v -> HashMap k v
M.alter (forall {a}. a -> Maybe [a] -> Maybe [a]
merge (DFunId, ty)
sig) Class
cls HashMap Class [(DFunId, ty)]
refs, [(LocSymbol, ty)]
sigs')
   where
    clsOp :: Maybe (Class, (DFunId, ty))
clsOp = do
      DFunId
var <- forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"grabClassSig" LocSymbol
lsym
      Class
cls <- DFunId -> Maybe Class
Ghc.isClassOpId_maybe DFunId
var
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Class
cls, (DFunId
var, ty
ref))
    merge :: a -> Maybe [a] -> Maybe [a]
merge a
sig Maybe [a]
v = case Maybe [a]
v of
      Maybe [a]
Nothing -> forall a. a -> Maybe a
Just [a
sig]
      Just [a]
vs -> forall a. a -> Maybe a
Just (a
sig forall a. a -> [a] -> [a]
: [a]
vs)
  methods :: [LocSymbol]
methods = [ forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol DFunId
x | (ClsInst
_, [DFunId]
xs) <- [(ClsInst, [DFunId])]
instmethods, DFunId
x <- [DFunId]
xs ]
      -- instance methods

  mkSymbol :: DFunId -> Symbol
mkSymbol DFunId
x
    | DFunId -> Bool
Ghc.isDictonaryId DFunId
x = Symbol -> Symbol -> Symbol
F.mappendSym Symbol
"$" (Int -> Symbol -> Symbol
F.dropSym Int
2 forall a b. (a -> b) -> a -> b
$ forall t. NamedThing t => t -> Symbol
GM.simplesymbol DFunId
x)
    | Bool
otherwise           = Int -> Symbol -> Symbol
F.dropSym Int
2 forall a b. (a -> b) -> a -> b
$ forall t. NamedThing t => t -> Symbol
GM.simplesymbol DFunId
x

  instmethods :: [(Ghc.ClsInst, [Ghc.Var])]
  instmethods :: [(ClsInst, [DFunId])]
instmethods =
    [ (ClsInst
inst, [DFunId]
ms)
    | (ClsInst
inst, Class
cls) <- [(ClsInst, Class)]
instClss
    , let selIds :: [Symbol]
selIds = Symbol -> Symbol
GM.dropModuleNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Class -> [DFunId]
Ghc.classAllSelIds Class
cls
    , (DFunId
_, CoreExpr
e) <- forall a. Maybe a -> [a]
Mb.maybeToList
      (Symbol -> [CoreBind] -> Maybe (DFunId, CoreExpr)
GM.findVarDefMethod
        (Symbol -> Symbol
GM.dropModuleNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol forall a b. (a -> b) -> a -> b
$ ClsInst -> DFunId
Ghc.instanceDFunId ClsInst
inst)
        (GhcSrc -> [CoreBind]
_giCbs GhcSrc
src)
      )
    , let ms :: [DFunId]
ms = forall a. (a -> Bool) -> [a] -> [a]
filter (\DFunId
x -> forall a. Symbolic a => a -> Bool
GM.isMethod DFunId
x Bool -> Bool -> Bool
&& forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (DFunId -> Symbol
mkSymbol DFunId
x) [Symbol]
selIds)
                      (forall a. CBVisitable a => HashSet DFunId -> a -> [DFunId]
freeVars forall a. Monoid a => a
mempty CoreExpr
e)
    ]
  instClss :: [(Ghc.ClsInst, Ghc.Class)]
  instClss :: [(ClsInst, Class)]
instClss =
    [ (ClsInst
inst, Class
cls)
    | ClsInst
inst <- forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Maybe a -> [a]
Mb.maybeToList forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSrc -> Maybe [ClsInst]
_gsCls forall a b. (a -> b) -> a -> b
$ GhcSrc
src
    , forall unit. GenModule unit -> ModuleName
Ghc.moduleName (HasDebugCallStack => Name -> Module
Ghc.nameModule (forall a. NamedThing a => a -> Name
Ghc.getName ClsInst
inst)) forall a. Eq a => a -> a -> Bool
== ModName -> ModuleName
getModName ModName
name
    , let cls :: Class
cls = ClsInst -> Class
Ghc.is_cls ClsInst
inst
    , Class
cls forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Class]
refinedClasses
    ]
  refinedClasses :: [Ghc.Class]
  refinedClasses :: [Class]
refinedClasses =
    forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe DataDecl -> Maybe Class
resolveClassMaybe [DataDecl]
clsDecls
      forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe DataDecl -> Maybe Class
resolveClassMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(ModName, BareSpec)]
rest
  resolveClassMaybe :: DataDecl -> Maybe Ghc.Class
  resolveClassMaybe :: DataDecl -> Maybe Class
resolveClassMaybe DataDecl
d =
    forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env
                         ModName
name
                         [Char]
"resolveClassMaybe"
                         (DataName -> LocSymbol
dataNameSymbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> DataName
tycName forall a b. (a -> b) -> a -> b
$ DataDecl
d)
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TyCon -> Maybe Class
Ghc.tyConClass_maybe


-- a list of class with user defined refinements
makeClassDataDecl :: [(Ghc.Class, [(Ghc.Id, LocBareType)])] -> [DataDecl]
makeClassDataDecl :: [(Class, [(DFunId, LocBareType)])] -> [DataDecl]
makeClassDataDecl = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Class -> [(DFunId, LocBareType)] -> DataDecl
classDeclToDataDecl)

-- TODO: I should have the knowledge to construct DataConP manually than
-- following the rather unwieldy pipeline: Resolved -> Unresolved -> Resolved.
-- maybe this should be fixed right after the GHC API refactoring?
classDeclToDataDecl :: Ghc.Class -> [(Ghc.Id, LocBareType)] -> DataDecl
classDeclToDataDecl :: Class -> [(DFunId, LocBareType)] -> DataDecl
classDeclToDataDecl Class
cls [(DFunId, LocBareType)]
refinedIds = DataDecl
  { tycName :: DataName
tycName   = LocSymbol -> DataName
DnName (forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. NamedThing a => a -> Located a
GM.locNamedThing Class
cls)
  , tycTyVars :: [Symbol]
tycTyVars = [Symbol]
tyVars
  , tycPVars :: [PVar BSort]
tycPVars  = []
  , tycDCons :: Maybe [DataCtor]
tycDCons  = forall a. a -> Maybe a
Just [DataCtor
dctor]
  , tycSrcPos :: SourcePos
tycSrcPos = forall a. Located a -> SourcePos
F.loc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedThing a => a -> Located a
GM.locNamedThing forall a b. (a -> b) -> a -> b
$ Class
cls
  , tycSFun :: Maybe SizeFun
tycSFun   = forall a. Maybe a
Nothing
  , tycPropTy :: Maybe BareType
tycPropTy = forall a. Maybe a
Nothing
  , tycKind :: DataDeclKind
tycKind   = DataDeclKind
DataUser
  }
 where
  dctor :: DataCtor
dctor = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"classDeclToDataDecl" DataCtor { dcName :: LocSymbol
dcName   = forall a. a -> Located a
F.dummyLoc forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol DataCon
classDc
    -- YL: same as class tyvars??
    -- Ans: it's been working so far so probably yes
                   , dcTyVars :: [Symbol]
dcTyVars = [Symbol]
tyVars
    -- YL: what is theta?
    -- Ans: where class constraints should go yet remain unused
    -- maybe should factor this out?
                   , dcTheta :: [BareType]
dcTheta  = []
                   , dcFields :: [(Symbol, BareType)]
dcFields = [(Symbol, BareType)]
fields
                   , dcResult :: Maybe BareType
dcResult = forall a. Maybe a
Nothing
                   }

  tyVars :: [Symbol]
tyVars = forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Class -> [DFunId]
Ghc.classTyVars Class
cls

  fields :: [(Symbol, BareType)]
fields = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DFunId -> (Symbol, BareType)
attachRef [DFunId]
classIds
  attachRef :: DFunId -> (Symbol, BareType)
attachRef DFunId
sid
    | Just LocBareType
ref <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup DFunId
sid [(DFunId, LocBareType)]
refinedIds
    = (forall a. Symbolic a => a -> Symbol
F.symbol DFunId
sid, forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
RT.subts [(Symbol, Symbol)]
tyVarSubst (forall a. Located a -> a
F.val LocBareType
ref))
    | Bool
otherwise
    = (forall a. Symbolic a => a -> Symbol
F.symbol DFunId
sid, forall r. Monoid r => Type -> BRType r
RT.bareOfType forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
dropTheta forall b c a. (b -> c) -> (a -> b) -> a -> c
. DFunId -> Type
Ghc.varType forall a b. (a -> b) -> a -> b
$ DFunId
sid)

  tyVarSubst :: [(Symbol, Symbol)]
tyVarSubst = [ (Symbol -> Symbol
GM.dropModuleUnique Symbol
v, Symbol
v) | Symbol
v <- [Symbol]
tyVars ]

  -- FIXME: dropTheta should not be needed as long as we
  -- handle classes and ordinary data types separately
  -- Might be helpful if we add an additional field for
  -- typeclasses
  dropTheta :: Ghc.Type -> Ghc.Type
  dropTheta :: Type -> Type
dropTheta = forall a b c. (a, b, c) -> c
Misc.thd3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ([DFunId], Type, Type)
Ghc.tcSplitMethodTy

  classIds :: [DFunId]
classIds  = Class -> [DFunId]
Ghc.classAllSelIds Class
cls
  classDc :: DataCon
classDc   = Class -> DataCon
Ghc.classDataCon Class
cls

-- | 'elaborateClassDcp' behaves differently from other datacon
--    functions. Each method type contains the full forall quantifiers
--    instead of having them chopped off
elaborateClassDcp
  :: (Ghc.CoreExpr -> F.Expr)
  -> (Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr)
  -> DataConP
  -> Ghc.TcRn (DataConP, DataConP)
elaborateClassDcp :: (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> DataConP
-> TcRn (DataConP, DataConP)
elaborateClassDcp CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier DataConP
dcp = do
  [SpecType]
t' <- forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SpecType -> Maybe RReft -> SpecType
addCoherenceOblig) [Maybe RReft]
prefts
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [SpecType]
fts ((CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr) -> SpecType -> TcRn SpecType
elaborateSpecType CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier)
  let ts' :: [SpecType]
ts' = Symbol -> HashSet Symbol -> SpecType -> SpecType
elaborateMethod (forall a. Symbolic a => a -> Symbol
F.symbol DataCon
dc) (forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Symbol]
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
t'
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( DataConP
dcp { dcpTyArgs :: [(Symbol, SpecType)]
dcpTyArgs = forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs (SpecType -> SpecType
stripPred forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts') }
    , DataConP
dcp { dcpTyArgs :: [(Symbol, SpecType)]
dcpTyArgs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Symbol
x, SpecType
t) -> (Symbol
x, Symbol -> SpecType -> SpecType
strengthenTy Symbol
x SpecType
t)) (forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [SpecType]
t') }
    )
 where
  addCoherenceOblig :: SpecType -> Maybe RReft -> SpecType
  addCoherenceOblig :: SpecType -> Maybe RReft -> SpecType
addCoherenceOblig SpecType
t Maybe RReft
Nothing  = SpecType
t
  addCoherenceOblig SpecType
t (Just RReft
r) = forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep RTypeRep RTyCon RTyVar RReft
rrep
    { ty_res :: SpecType
ty_res = SpecType
res forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` RReft
r
    }
   where
    rrep :: RTypeRep RTyCon RTyVar RReft
rrep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t
    res :: SpecType
res  = forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
rrep
  prefts :: [Maybe RReft]
prefts =
    forall a. [a] -> [a]
L.reverse
      forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
fts)
      forall a b. (a -> b) -> a -> b
$  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r. r -> Predicate -> UReft r
MkUReft forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => [a] -> a
mconcat) [[Reft]]
preftss
      forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat forall a. Maybe a
Nothing
  preftss :: [[Reft]]
preftss = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall s. Symbolic s => s -> [DFunId] -> [DFunId] -> Reft
GM.coherenceObligToRef Symbol
recsel))
                          (Class -> [[([DFunId], [DFunId])]]
GM.buildCoherenceOblig Class
cls)

  -- ugly, should have passed cls as an argument
  cls :: Class
cls      = forall a. HasCallStack => Maybe a -> a
Mb.fromJust forall a b. (a -> b) -> a -> b
$ TyCon -> Maybe Class
Ghc.tyConClass_maybe (DataCon -> TyCon
Ghc.dataConTyCon DataCon
dc)
  recsel :: Symbol
recsel   = forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
"lq$recsel" :: String)
  resTy :: SpecType
resTy    = DataConP -> SpecType
dcpTyRes DataConP
dcp
  dc :: DataCon
dc       = DataConP -> DataCon
dcpCon DataConP
dcp
  tvars :: [(RTVar RTyVar s, RReft)]
tvars    = (\RTyVar
x -> (forall tv s. tv -> RTVar tv s
makeRTVar RTyVar
x, forall a. Monoid a => a
mempty)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataConP -> [RTyVar]
dcpFreeTyVars DataConP
dcp
      -- check if the names are qualified
  ([Symbol]
xs, [SpecType]
ts) = forall a b. [(a, b)] -> ([a], [b])
unzip (DataConP -> [(Symbol, SpecType)]
dcpTyArgs DataConP
dcp)
  fts :: [SpecType]
fts      = SpecType -> SpecType
fullTy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts
      -- turns forall a b. (a -> b) -> f a -> f b into
      -- forall f. Functor f => forall a b. (a -> b) -> f a -> f b
  stripPred :: SpecType -> SpecType
  stripPred :: SpecType -> SpecType
stripPred = forall t t1 t2 t3. (t, t1, t2, t3) -> t3
Misc.fourth4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType
-> ([(SpecRTVar, RReft)], [PVar RSort], [(RTyCon, [SpecType])],
    SpecType)
bkUnivClass
  fullTy :: SpecType -> SpecType
  fullTy :: SpecType -> SpecType
fullTy SpecType
t = forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow
    forall {s}. [(RTVar RTyVar s, RReft)]
tvars
    []
    [ ( Symbol
recsel{- F.symbol dc-}
      , Bool -> RFInfo
classRFInfo Bool
True
      , SpecType
resTy
      , forall a. Monoid a => a
mempty
      )
    ]
    SpecType
t
  -- YL: is this redundant if we already have strengthenClassSel?
  strengthenTy :: F.Symbol -> SpecType -> SpecType
  strengthenTy :: Symbol -> SpecType -> SpecType
strengthenTy Symbol
x SpecType
t = forall (t :: * -> *) (t1 :: * -> *) tv c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RType c tv ()), r)
-> t1 (PVar (RType c tv ())) -> RType c tv r -> RType c tv r
mkUnivs [(SpecRTVar, RReft)]
tvs [PVar RSort]
pvs (forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
z RFInfo
i SpecType
clas (SpecType
t' forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` RReft
mt) RReft
r)
   where
    ([(SpecRTVar, RReft)]
tvs, [PVar RSort]
pvs, RFun Symbol
z RFInfo
i SpecType
clas SpecType
t' RReft
r) = 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
    vv :: Symbol
vv = forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar SpecType
t'
    mt :: RReft
mt = (Symbol, Expr) -> RReft
RT.uReft (Symbol
vv, Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Eq (Symbol -> Expr
F.EVar Symbol
vv) (Expr -> Expr -> Expr
F.EApp (Symbol -> Expr
F.EVar Symbol
x) (Symbol -> Expr
F.EVar Symbol
z)))


elaborateMethod :: F.Symbol -> S.HashSet F.Symbol -> SpecType -> SpecType
elaborateMethod :: Symbol -> HashSet Symbol -> SpecType -> SpecType
elaborateMethod Symbol
dc HashSet Symbol
methods SpecType
st = forall c tv.
(Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
mapExprReft
  (\Symbol
_ -> Symbol -> Symbol -> HashSet Symbol -> Expr -> Expr
substClassOpBinding Symbol
tcbindSym Symbol
dc HashSet Symbol
methods)
  SpecType
st
 where
  tcbindSym :: Symbol
tcbindSym = SpecType -> Symbol
grabtcbind SpecType
st
  grabtcbind :: SpecType -> F.Symbol
  grabtcbind :: SpecType -> Symbol
grabtcbind SpecType
t =
    forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"grabtcbind"
      forall a b. (a -> b) -> a -> b
$ case forall t t1 t2 t3. (t, t1, t2, t3) -> t
Misc.fst4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t t1 a.
RType t t1 a
-> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
bkArrow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a, b, c) -> c
Misc.thd3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv forall a b. (a -> b) -> a -> b
$ SpecType
t of
          Symbol
tcbind : [Symbol]
_ -> Symbol
tcbind
          []         -> forall a. Maybe SrcSpan -> [Char] -> a
impossible
            forall a. Maybe a
Nothing
            (  [Char]
"elaborateMethod: inserted dictionary binder disappeared:"
            forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
t
            )


-- Before: Functor.fmap ($p1Applicative $dFunctor)
-- After: Funcctor.fmap ($p1Applicative##GHC.Base.Applicative)
substClassOpBinding
  :: F.Symbol -> F.Symbol -> S.HashSet F.Symbol -> F.Expr -> F.Expr
substClassOpBinding :: Symbol -> Symbol -> HashSet Symbol -> Expr -> Expr
substClassOpBinding Symbol
tcbind Symbol
dc HashSet Symbol
methods = Expr -> Expr
go
 where
  go :: F.Expr -> F.Expr
  go :: Expr -> Expr
go (F.EApp Expr
e0 Expr
e1)
    | F.EVar Symbol
x <- Expr
e0, F.EVar Symbol
y <- Expr
e1, Symbol
y forall a. Eq a => a -> a -> Bool
== Symbol
tcbind, forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x HashSet Symbol
methods = Symbol -> Expr
F.EVar
      (Symbol
x Symbol -> Symbol -> Symbol
`F.suffixSymbol` Symbol
dc)
    | Bool
otherwise = Expr -> Expr -> Expr
F.EApp (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
  go (F.ENeg Expr
e          ) = Expr -> Expr
F.ENeg (Expr -> Expr
go Expr
e)
  go (F.EBin Bop
bop Expr
e0 Expr
e1  ) = Bop -> Expr -> Expr -> Expr
F.EBin Bop
bop (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
  go (F.EIte Expr
e0  Expr
e1 Expr
e2  ) = Expr -> Expr -> Expr -> Expr
F.EIte (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
  go (F.ECst Expr
e0     Sort
s   ) = Expr -> Sort -> Expr
F.ECst (Expr -> Expr
go Expr
e0) Sort
s
  go (F.ELam (Symbol
x, Sort
t) Expr
body) = (Symbol, Sort) -> Expr -> Expr
F.ELam (Symbol
x, Sort
t) (Expr -> Expr
go Expr
body)
  go (F.PAnd [Expr]
es         ) = [Expr] -> Expr
F.PAnd (Expr -> Expr
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
  go (F.POr  [Expr]
es         ) = [Expr] -> Expr
F.POr (Expr -> Expr
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
  go (F.PNot Expr
e          ) = Expr -> Expr
F.PNot (Expr -> Expr
go Expr
e)
  go (F.PImp Expr
e0 Expr
e1      ) = Expr -> Expr -> Expr
F.PImp (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
  go (F.PIff Expr
e0 Expr
e1      ) = Expr -> Expr -> Expr
F.PIff (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
  go (F.PAtom Brel
brel Expr
e0 Expr
e1) = Brel -> Expr -> Expr -> Expr
F.PAtom Brel
brel (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
  -- a catch-all binding is not a good idea
  go Expr
e                    = Expr
e


renameTvs :: (F.Symbolic tv, F.PPrint tv) => (tv -> tv) -> RType c tv r -> RType c tv r
renameTvs :: forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
t
  | RVar tv
tv r
r <- RType c tv r
t
  = forall c tv r. tv -> r -> RType c tv r
RVar (tv -> tv
rename tv
tv) r
r
  | RFun Symbol
b RFInfo
i RType c tv r
tin RType c tv r
tout r
r <- RType c tv r
t
  = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
b RFInfo
i (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
tin) (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
tout) r
r
  | RAllT (RTVar tv
tv RTVInfo (RType c tv ())
info) RType c tv r
tres r
r <- RType c tv r
t
  = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar (tv -> tv
rename tv
tv) RTVInfo (RType c tv ())
info) (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
tres) r
r
  | RAllP PVU c tv
b RType c tv r
tres <- RType c tv r
t
  = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVU c tv
b) (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
tres)
  | RApp c
tc [RType c tv r]
ts [RTProp c tv r]
tps r
r <- RType c tv r
t
  -- TODO: handle rtprop properly
  = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
tc (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv r]
ts) [RTProp c tv r]
tps r
r
  | RAllE Symbol
b RType c tv r
allarg RType c tv r
ty <- RType c tv r
t
  = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
b (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
allarg) (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
ty)
  | REx Symbol
b RType c tv r
exarg RType c tv r
ty <- RType c tv r
t
  = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
b   (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
exarg) (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
ty)
  | RExprArg Located Expr
_ <- RType c tv r
t
  = RType c tv r
t
  | RAppTy RType c tv r
arg RType c tv r
res r
r <- RType c tv r
t
  = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
arg) (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
res) r
r
  | RRTy [(Symbol, RType c tv r)]
env r
r Oblig
obl RType c tv r
ty <- RType c tv r
t
  = forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv r)]
env) r
r Oblig
obl (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
ty)
  | RHole r
_ <- RType c tv r
t
  = RType c tv r
t


makeClassAuxTypes ::
     (SpecType -> Ghc.TcRn SpecType)
  -> [F.Located DataConP]
  -> [(Ghc.ClsInst, [Ghc.Var])]
  -> Ghc.TcRn [(Ghc.Var, LocSpecType)]
makeClassAuxTypes :: (SpecType -> TcRn SpecType)
-> [Located DataConP]
-> [(ClsInst, [DFunId])]
-> TcRn [(DFunId, LocSpecType)]
makeClassAuxTypes SpecType -> TcRn SpecType
elab [Located DataConP]
dcps [(ClsInst, [DFunId])]
xs = forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(a -> m [b]) -> t a -> m [b]
Misc.concatMapM ((SpecType -> TcRn SpecType)
-> (Located DataConP, ClsInst, [DFunId])
-> TcRn [(DFunId, LocSpecType)]
makeClassAuxTypesOne SpecType -> TcRn SpecType
elab) [(Located DataConP, ClsInst, [DFunId])]
dcpInstMethods
  where
    dcpInstMethods :: [(Located DataConP, ClsInst, [DFunId])]
dcpInstMethods = do
      Located DataConP
dcp <- [Located DataConP]
dcps
      (ClsInst
inst, [DFunId]
methods) <- [(ClsInst, [DFunId])]
xs
      let dc :: DataCon
dc = DataConP -> DataCon
dcpCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
F.val forall a b. (a -> b) -> a -> b
$ Located DataConP
dcp
              -- YL: only works for non-newtype class
          dc' :: DataCon
dc' = Class -> DataCon
Ghc.classDataCon forall a b. (a -> b) -> a -> b
$ ClsInst -> Class
Ghc.is_cls ClsInst
inst
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ DataCon
dc forall a. Eq a => a -> a -> Bool
== DataCon
dc'
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Located DataConP
dcp, ClsInst
inst, [DFunId]
methods)

makeClassAuxTypesOne ::
     (SpecType -> Ghc.TcRn SpecType)
  -> (F.Located DataConP, Ghc.ClsInst, [Ghc.Var])
  -> Ghc.TcRn [(Ghc.Var, LocSpecType)]
makeClassAuxTypesOne :: (SpecType -> TcRn SpecType)
-> (Located DataConP, ClsInst, [DFunId])
-> TcRn [(DFunId, LocSpecType)]
makeClassAuxTypesOne SpecType -> TcRn SpecType
elab (Located DataConP
ldcp, ClsInst
inst, [DFunId]
methods) =
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DFunId]
methods forall a b. (a -> b) -> a -> b
$ \DFunId
method -> do
    let (SpecType
headlessSig, Maybe RReft
preft) =
          case forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup (DFunId -> Symbol
mkSymbol DFunId
method) [(Symbol, (SpecType, Maybe RReft))]
yts' of
            Maybe (SpecType, Maybe RReft)
Nothing ->
              forall a. Maybe SrcSpan -> [Char] -> a
impossible forall a. Maybe a
Nothing ([Char]
"makeClassAuxTypesOne : unreachable?" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (DFunId -> Symbol
mkSymbol DFunId
method) forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp [(Symbol, SpecType)]
yts)
            Just (SpecType, Maybe RReft)
sig -> (SpecType, Maybe RReft)
sig
        -- dict binder will never be changed because we optimized PAnd[]
        -- lq0 lq1 ...
            --
        ptys :: [(Symbol, RFInfo, SpecType, RReft)]
ptys    = [(Maybe Integer -> Symbol
F.vv (forall a. a -> Maybe a
Just Integer
i), Bool -> RFInfo
classRFInfo Bool
True, SpecType
pty, forall a. Monoid a => a
mempty) | (Integer
i,SpecType
pty) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0,Integer
1..] [SpecType]
isPredSpecTys]
        fullSig :: SpecType
fullSig =
          forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow
            (forall a b. [a] -> [b] -> [(a, b)]
zip forall {s}. [RTVar RTyVar s]
isRTvs (forall a. a -> [a]
repeat forall a. Monoid a => a
mempty))
            []
            [(Symbol, RFInfo, SpecType, RReft)]
ptys forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          forall {tv} {r} {c}.
(Hashable tv, Reftable r, TyConable c, FreeVar c tv,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
[(tv, RType c tv r)] -> RType c tv r -> RType c tv r
subst (forall a b. [a] -> [b] -> [(a, b)]
zip [RTyVar]
clsTvs [SpecType]
isSpecTys) forall a b. (a -> b) -> a -> b
$
          SpecType
headlessSig
    SpecType
elaboratedSig  <- forall a b c. (a -> b -> c) -> b -> a -> c
flip SpecType -> Maybe RReft -> SpecType
addCoherenceOblig Maybe RReft
preft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> TcRn SpecType
elab SpecType
fullSig

    let retSig :: SpecType
retSig =  forall c tv.
(Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
mapExprReft (\Symbol
_ -> Symbol -> HashMap Symbol Symbol -> Expr -> Expr
substAuxMethod Symbol
dfunSym HashMap Symbol Symbol
methodsSet) (forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"elaborated" forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr DFunId
method) SpecType
elaboratedSig)
    let tysub :: HashMap RTyVar RTyVar
tysub  = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"tysub" forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"newtype-vars" forall a b. (a -> b) -> a -> b
$ forall tv c r. Eq tv => RType c tv r -> [tv]
allTyVars' (forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"new-type" SpecType
retSig)) (forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"ghc-type-vars" (forall tv c r. Eq tv => RType c tv r -> [tv]
allTyVars' ((forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"ghc-type" forall a b. (a -> b) -> a -> b
$ forall r. Monoid r => Type -> RRType r
ofType (DFunId -> Type
Ghc.varType DFunId
method)) :: SpecType)))
        cosub :: HashMap Symbol Sort
cosub  = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (forall a. Symbolic a => a -> Symbol
F.symbol RTyVar
a, LocSymbol -> Sort
F.fObj (forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol DFunId
b)) |  (RTyVar
a,RTV DFunId
b) <- forall k v. HashMap k v -> [(k, v)]
M.toList HashMap RTyVar RTyVar
tysub]
        tysubf :: RTyVar -> RTyVar
tysubf RTyVar
x = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"cosub:" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp HashMap Symbol Sort
cosub) forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault RTyVar
x RTyVar
x HashMap RTyVar RTyVar
tysub
        subbedTy :: SpecType
subbedTy = forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft (HashMap Symbol Sort -> RReft -> RReft
Bare.coSubRReft HashMap Symbol Sort
cosub) (forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs RTyVar -> RTyVar
tysubf SpecType
retSig)

    -- need to make the variable names consistent
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (DFunId
method, forall a. a -> Located a
F.dummyLoc (forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"vars:" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall tv c r. Eq tv => RType c tv r -> [tv]
allTyVars' SpecType
subbedTy)) SpecType
subbedTy))

  -- "is" is used as a shorthand for instance, following the convention of the Ghc api
  where
    -- recsel = F.symbol ("lq$recsel" :: String)
    ([DFunId]
_,[Type]
predTys,Class
_,[Type]
_) = ClsInst -> ([DFunId], [Type], Class, [Type])
Ghc.instanceSig ClsInst
inst
    dfunApped :: Expr
dfunApped = LocSymbol -> [Expr] -> Expr
F.mkEApp LocSymbol
dfunSymL [forall a. Symbolic a => a -> Expr
F.eVar forall a b. (a -> b) -> a -> b
$ Maybe Integer -> Symbol
F.vv (forall a. a -> Maybe a
Just Integer
i) | (Integer
i,Type
_) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0,Integer
1..] [Type]
predTys]
    prefts :: [Maybe RReft]
prefts  = forall a. [a] -> [a]
L.reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, SpecType)]
yts) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"prefts" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r. r -> Predicate -> UReft r
MkUReft forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => [a] -> a
mconcat) [[Reft]]
preftss forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat forall a. Maybe a
Nothing
    preftss :: [[Reft]]
preftss = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"preftss" forall a b. (a -> b) -> a -> b
$ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmapforall b c a. (b -> c) -> (a -> b) -> a -> c
.forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Expr -> [DFunId] -> [DFunId] -> Reft
GM.coherenceObligToRefE Expr
dfunApped)) (Class -> [[([DFunId], [DFunId])]]
GM.buildCoherenceOblig Class
cls)
    yts' :: [(Symbol, (SpecType, Maybe RReft))]
yts' = forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
yts) (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
yts) [Maybe RReft]
prefts)
    cls :: Class
cls = forall a. HasCallStack => Maybe a -> a
Mb.fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Maybe Class
Ghc.tyConClass_maybe forall a b. (a -> b) -> a -> b
$ DataCon -> TyCon
Ghc.dataConTyCon (DataConP -> DataCon
dcpCon DataConP
dcp)
    addCoherenceOblig  :: SpecType -> Maybe RReft -> SpecType
    addCoherenceOblig :: SpecType -> Maybe RReft -> SpecType
addCoherenceOblig SpecType
t Maybe RReft
Nothing = SpecType
t
    addCoherenceOblig SpecType
t (Just RReft
r) = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"SCSel" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft
rrep {ty_res :: SpecType
ty_res = SpecType
res forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` RReft
r}
      where rrep :: RTypeRep RTyCon RTyVar RReft
rrep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t
            res :: SpecType
res  = forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
rrep    -- (Monoid.mappend -> $cmappend##Int, ...)
    -- core rewriting mark2: do the same thing except they don't have to be symbols
    -- YL: poorly written. use a comprehension instead of assuming
    methodsSet :: HashMap Symbol Symbol
methodsSet = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"methodSet" forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DFunId]
clsMethods) (forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DFunId]
methods))
    -- core rewriting mark1: dfunId
    -- ()
    dfunSymL :: LocSymbol
dfunSymL = forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol forall a b. (a -> b) -> a -> b
$ ClsInst -> DFunId
Ghc.instanceDFunId ClsInst
inst
    dfunSym :: Symbol
dfunSym = forall a. Located a -> a
F.val LocSymbol
dfunSymL
    ([DFunId]
isTvs, [Type]
isPredTys, Class
_, [Type]
isTys) = ClsInst -> ([DFunId], [Type], Class, [Type])
Ghc.instanceSig ClsInst
inst
    isSpecTys :: [SpecType]
isSpecTys = forall r. Monoid r => Type -> RRType r
ofType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
isTys
    isPredSpecTys :: [SpecType]
isPredSpecTys = forall r. Monoid r => Type -> RRType r
ofType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
isPredTys
    isRTvs :: [RTVar RTyVar s]
isRTvs = forall tv s. tv -> RTVar tv s
makeRTVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. DFunId -> RTyVar
rTyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DFunId]
isTvs
    dcp :: DataConP
dcp = forall a. Located a -> a
F.val Located DataConP
ldcp
    -- Monoid.mappend, ...
    clsMethods :: [DFunId]
clsMethods = forall a. (a -> Bool) -> [a] -> [a]
filter (\DFunId
x -> Symbol -> Symbol
GM.dropModuleNames (forall a. Symbolic a => a -> Symbol
F.symbol DFunId
x) forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DFunId -> Symbol
mkSymbol [DFunId]
methods) forall a b. (a -> b) -> a -> b
$
      Class -> [DFunId]
Ghc.classAllSelIds (ClsInst -> Class
Ghc.is_cls ClsInst
inst)
    yts :: [(Symbol, SpecType)]
yts = [(Symbol -> Symbol
GM.dropModuleNames Symbol
y, SpecType
t) | (Symbol
y, SpecType
t) <- DataConP -> [(Symbol, SpecType)]
dcpTyArgs DataConP
dcp]
    mkSymbol :: DFunId -> Symbol
mkSymbol DFunId
x
      | -- F.notracepp ("isDictonaryId:" ++ GM.showPpr x) $
        DFunId -> Bool
Ghc.isDictonaryId DFunId
x = Symbol -> Symbol -> Symbol
F.mappendSym Symbol
"$" (Int -> Symbol -> Symbol
F.dropSym Int
2 forall a b. (a -> b) -> a -> b
$ forall t. NamedThing t => t -> Symbol
GM.simplesymbol DFunId
x)
      | Bool
otherwise = Int -> Symbol -> Symbol
F.dropSym Int
2 forall a b. (a -> b) -> a -> b
$ forall t. NamedThing t => t -> Symbol
GM.simplesymbol DFunId
x
        -- res = dcpTyRes dcp
    clsTvs :: [RTyVar]
clsTvs = DataConP -> [RTyVar]
dcpFreeTyVars DataConP
dcp
        -- copy/pasted from Bare/Class.hs
    subst :: [(tv, RType c tv r)] -> RType c tv r -> RType c tv r
subst [] RType c tv r
t = RType c tv r
t
    subst ((tv
a, RType c tv r
ta):[(tv, RType c tv r)]
su) RType c tv r
t = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet' (tv
a, RType c tv r
ta) ([(tv, RType c tv r)] -> RType c tv r -> RType c tv r
subst [(tv, RType c tv r)]
su RType c tv r
t)

substAuxMethod :: F.Symbol -> M.HashMap F.Symbol F.Symbol -> F.Expr -> F.Expr
substAuxMethod :: Symbol -> HashMap Symbol Symbol -> Expr -> Expr
substAuxMethod Symbol
dfun HashMap Symbol Symbol
methods = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"substAuxMethod" forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
go
  where go :: F.Expr -> F.Expr
        go :: Expr -> Expr
go (F.EApp Expr
e0 Expr
e1)
          | F.EVar Symbol
x <- forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"e0" Expr
e0
          , (F.EVar Symbol
dfun_mb, [Expr]
args)  <- Expr -> (Expr, [Expr])
F.splitEApp Expr
e1
          , Symbol
dfun_mb forall a. Eq a => a -> a -> Bool
== Symbol
dfun
          , Just Symbol
method <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol Symbol
methods
              -- Before: Functor.fmap ($p1Applicative $dFunctor)
              -- After: Funcctor.fmap ($p1Applicative##GHC.Base.Applicative)
           = Expr -> [Expr] -> Expr
F.eApps (Symbol -> Expr
F.EVar Symbol
method) [Expr]
args
          | Bool
otherwise
          = Expr -> Expr -> Expr
F.EApp (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
        go (F.ENeg Expr
e) = Expr -> Expr
F.ENeg (Expr -> Expr
go Expr
e)
        go (F.EBin Bop
bop Expr
e0 Expr
e1) = Bop -> Expr -> Expr -> Expr
F.EBin Bop
bop (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
        go (F.EIte Expr
e0 Expr
e1 Expr
e2) = Expr -> Expr -> Expr -> Expr
F.EIte (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
        go (F.ECst Expr
e0 Sort
s) = Expr -> Sort -> Expr
F.ECst (Expr -> Expr
go Expr
e0) Sort
s
        go (F.ELam (Symbol
x, Sort
t) Expr
body) = (Symbol, Sort) -> Expr -> Expr
F.ELam (Symbol
x, Sort
t) (Expr -> Expr
go Expr
body)
        go (F.PAnd [Expr]
es) = [Expr] -> Expr
F.PAnd (Expr -> Expr
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
        go (F.POr [Expr]
es) = [Expr] -> Expr
F.POr (Expr -> Expr
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
        go (F.PNot Expr
e) = Expr -> Expr
F.PNot (Expr -> Expr
go Expr
e)
        go (F.PImp Expr
e0 Expr
e1) = Expr -> Expr -> Expr
F.PImp (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
        go (F.PIff Expr
e0 Expr
e1) = Expr -> Expr -> Expr
F.PIff (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
        go (F.PAtom Brel
brel Expr
e0 Expr
e1) = Brel -> Expr -> Expr -> Expr
F.PAtom Brel
brel (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
        go Expr
e = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"LEAF" Expr
e