{-# 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.DataDecl
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import qualified Language.Haskell.Liquid.Types.RefType
                                               as RT
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.Visitors
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 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 = sigsNew } BareSpec -> BareSpec -> BareSpec
forall a. Semigroup a => a -> a -> a
<> BareSpec
clsSpec, [(ClsInst, [DFunId])]
instmethods)
 where
  clsSpec :: BareSpec
clsSpec = BareSpec
forall a. Monoid a => a
mempty
    { dataDecls = clsDecls
    , reflects  = F.notracepp "reflects " $ S.fromList
                    (  fmap
                        ( fmap (updateLHNameSymbol GM.dropModuleNames)
                        . makeGHCLHNameLocatedFromId
                        . Ghc.instanceDFunId
                        . fst
                        )
                        instClss
                    ++ methods
                    )
    }
  clsDecls :: [DataDecl]
clsDecls                = [(Class, [(DFunId, Located (BareTypeV Symbol))])] -> [DataDecl]
makeClassDataDecl (HashMap Class [(DFunId, Located (BareTypeV Symbol))]
-> [(Class, [(DFunId, Located (BareTypeV Symbol))])]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Class [(DFunId, Located (BareTypeV Symbol))]
refinedMethods)
      -- class methods
  (HashMap Class [(DFunId, Located (BareTypeV Symbol))]
refinedMethods, [(Located LHName, Located (BareTypeV Symbol))]
sigsNew) = ((Located LHName, Located (BareTypeV Symbol))
 -> (HashMap Class [(DFunId, Located (BareTypeV Symbol))],
     [(Located LHName, Located (BareTypeV Symbol))])
 -> (HashMap Class [(DFunId, Located (BareTypeV Symbol))],
     [(Located LHName, Located (BareTypeV Symbol))]))
-> (HashMap Class [(DFunId, Located (BareTypeV Symbol))],
    [(Located LHName, Located (BareTypeV Symbol))])
-> [(Located LHName, Located (BareTypeV Symbol))]
-> (HashMap Class [(DFunId, Located (BareTypeV Symbol))],
    [(Located LHName, Located (BareTypeV Symbol))])
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Located LHName, Located (BareTypeV Symbol))
-> (HashMap Class [(DFunId, Located (BareTypeV Symbol))],
    [(Located LHName, Located (BareTypeV Symbol))])
-> (HashMap Class [(DFunId, Located (BareTypeV Symbol))],
    [(Located LHName, Located (BareTypeV Symbol))])
forall ty.
(Located LHName, ty)
-> (HashMap Class [(DFunId, ty)], [(Located LHName, ty)])
-> (HashMap Class [(DFunId, ty)], [(Located LHName, ty)])
grabClassSig (HashMap Class [(DFunId, Located (BareTypeV Symbol))]
forall a. Monoid a => a
mempty, [(Located LHName, Located (BareTypeV Symbol))]
forall a. Monoid a => a
mempty) (BareSpec -> [(Located LHName, Located (BareTypeV Symbol))]
forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
sigs BareSpec
spec)
  grabClassSig
    :: (F.Located LHName, ty)
    -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.Located LHName, ty)])
    -> (M.HashMap Ghc.Class [(Ghc.Id, ty)], [(F.Located LHName, ty)])
  grabClassSig :: forall ty.
(Located LHName, ty)
-> (HashMap Class [(DFunId, ty)], [(Located LHName, ty)])
-> (HashMap Class [(DFunId, ty)], [(Located LHName, ty)])
grabClassSig sigPair :: (Located LHName, ty)
sigPair@(Located LHName
lsym, ty
ref) (HashMap Class [(DFunId, ty)]
refs, [(Located LHName, ty)]
sigs') = case Maybe (Class, (DFunId, ty))
clsOp of
    Maybe (Class, (DFunId, ty))
Nothing         -> (HashMap Class [(DFunId, ty)]
refs, (Located LHName, ty)
sigPair (Located LHName, ty)
-> [(Located LHName, ty)] -> [(Located LHName, ty)]
forall a. a -> [a] -> [a]
: [(Located LHName, ty)]
sigs')
    Just (Class
cls, (DFunId, ty)
sig) -> ((Maybe [(DFunId, ty)] -> Maybe [(DFunId, ty)])
-> Class
-> HashMap Class [(DFunId, ty)]
-> HashMap Class [(DFunId, ty)]
forall k v.
(Eq k, Hashable k) =>
(Maybe v -> Maybe v) -> k -> HashMap k v -> HashMap k v
M.alter ((DFunId, ty) -> Maybe [(DFunId, ty)] -> Maybe [(DFunId, ty)]
forall {a}. a -> Maybe [a] -> Maybe [a]
merge (DFunId, ty)
sig) Class
cls HashMap Class [(DFunId, ty)]
refs, [(Located LHName, ty)]
sigs')
   where
    clsOp :: Maybe (Class, (DFunId, ty))
clsOp = do
      var <- ([Error] -> Maybe DFunId)
-> (DFunId -> Maybe DFunId)
-> Either [Error] DFunId
-> Maybe DFunId
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe DFunId -> [Error] -> Maybe DFunId
forall a b. a -> b -> a
const Maybe DFunId
forall a. Maybe a
Nothing) DFunId -> Maybe DFunId
forall a. a -> Maybe a
Just (Either [Error] DFunId -> Maybe DFunId)
-> Either [Error] DFunId -> Maybe DFunId
forall a b. (a -> b) -> a -> b
$ HasCallStack => Env -> Located LHName -> Either [Error] DFunId
Env -> Located LHName -> Either [Error] DFunId
Bare.lookupGhcIdLHName Env
env Located LHName
lsym
      cls <- Ghc.isClassOpId_maybe var
      pure (cls, (var, ref))
    merge :: a -> Maybe [a] -> Maybe [a]
merge a
sig Maybe [a]
v = case Maybe [a]
v of
      Maybe [a]
Nothing -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a
sig]
      Just [a]
vs -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just (a
sig a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
vs)
  methods :: [Located LHName]
methods = [ DFunId -> Located LHName
makeGHCLHNameLocatedFromId 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 (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ DFunId -> Symbol
forall t. NamedThing t => t -> Symbol
GM.simplesymbol DFunId
x)
    | Bool
otherwise           = Int -> Symbol -> Symbol
F.dropSym Int
2 (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ DFunId -> Symbol
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 (Symbol -> Symbol) -> (DFunId -> Symbol) -> DFunId -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DFunId -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DFunId -> Symbol) -> [DFunId] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Class -> [DFunId]
Ghc.classAllSelIds Class
cls
    , (DFunId
_, CoreExpr
e) <- Maybe (DFunId, CoreExpr) -> [(DFunId, CoreExpr)]
forall a. Maybe a -> [a]
Mb.maybeToList
      (Symbol -> [CoreBind] -> Maybe (DFunId, CoreExpr)
GM.findVarDefMethod
        (Symbol -> Symbol
GM.dropModuleNames (Symbol -> Symbol) -> (DFunId -> Symbol) -> DFunId -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DFunId -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DFunId -> Symbol) -> DFunId -> Symbol
forall a b. (a -> b) -> a -> b
$ ClsInst -> DFunId
Ghc.instanceDFunId ClsInst
inst)
        (GhcSrc -> [CoreBind]
_giCbs GhcSrc
src)
      )
    , let ms :: [DFunId]
ms = (DFunId -> Bool) -> [DFunId] -> [DFunId]
forall a. (a -> Bool) -> [a] -> [a]
filter (\DFunId
x -> DFunId -> Bool
forall a. Symbolic a => a -> Bool
GM.isMethod DFunId
x Bool -> Bool -> Bool
&& Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (DFunId -> Symbol
mkSymbol DFunId
x) [Symbol]
selIds)
                      (HashSet DFunId -> CoreExpr -> [DFunId]
forall a. CBVisitable a => HashSet DFunId -> a -> [DFunId]
freeVars HashSet DFunId
forall a. Monoid a => a
mempty CoreExpr
e)
    ]
  instClss :: [(Ghc.ClsInst, Ghc.Class)]
  instClss :: [(ClsInst, Class)]
instClss =
    [ (ClsInst
inst, Class
cls)
    | ClsInst
inst <- [[ClsInst]] -> [ClsInst]
forall a. Monoid a => [a] -> a
mconcat ([[ClsInst]] -> [ClsInst])
-> (GhcSrc -> [[ClsInst]]) -> GhcSrc -> [ClsInst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [ClsInst] -> [[ClsInst]]
forall a. Maybe a -> [a]
Mb.maybeToList (Maybe [ClsInst] -> [[ClsInst]])
-> (GhcSrc -> Maybe [ClsInst]) -> GhcSrc -> [[ClsInst]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSrc -> Maybe [ClsInst]
_gsCls (GhcSrc -> [ClsInst]) -> GhcSrc -> [ClsInst]
forall a b. (a -> b) -> a -> b
$ GhcSrc
src
    , GenModule Unit -> ModuleName
forall unit. GenModule unit -> ModuleName
Ghc.moduleName (HasDebugCallStack => Name -> GenModule Unit
Name -> GenModule Unit
Ghc.nameModule (ClsInst -> Name
forall a. NamedThing a => a -> Name
Ghc.getName ClsInst
inst)) ModuleName -> ModuleName -> Bool
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 Class -> [Class] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Class]
refinedClasses
    ]
  refinedClasses :: [Ghc.Class]
  refinedClasses :: [Class]
refinedClasses =
    (DataDecl -> Maybe Class) -> [DataDecl] -> [Class]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe DataDecl -> Maybe Class
resolveClassMaybe [DataDecl]
clsDecls
      [Class] -> [Class] -> [Class]
forall a. [a] -> [a] -> [a]
++ ((ModName, BareSpec) -> [Class])
-> [(ModName, BareSpec)] -> [Class]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((DataDecl -> Maybe Class) -> [DataDecl] -> [Class]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe DataDecl -> Maybe Class
resolveClassMaybe ([DataDecl] -> [Class])
-> ((ModName, BareSpec) -> [DataDecl])
-> (ModName, BareSpec)
-> [Class]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpec -> [DataDecl]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
dataDecls (BareSpec -> [DataDecl])
-> ((ModName, BareSpec) -> BareSpec)
-> (ModName, BareSpec)
-> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, BareSpec) -> BareSpec
forall a b. (a, b) -> b
snd) [(ModName, BareSpec)]
rest
  resolveClassMaybe :: DataDecl -> Maybe Ghc.Class
  resolveClassMaybe :: DataDecl -> Maybe Class
resolveClassMaybe DataDecl
d =
    ([Error] -> Maybe TyCon)
-> (TyCon -> Maybe TyCon) -> Either [Error] TyCon -> Maybe TyCon
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe TyCon -> [Error] -> Maybe TyCon
forall a b. a -> b -> a
const Maybe TyCon
forall a. Maybe a
Nothing) TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just (HasCallStack =>
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
Bare.lookupGhcTyConLHName (Env -> GHCTyLookupEnv
Bare.reTyLookupEnv Env
env) (Located LHName -> Either [Error] TyCon)
-> Located LHName -> Either [Error] TyCon
forall a b. (a -> b) -> a -> b
$ DataName -> Located LHName
dataNameSymbol (DataName -> Located LHName) -> DataName -> Located LHName
forall a b. (a -> b) -> a -> b
$ DataDecl -> DataName
forall v ty. DataDeclP v ty -> DataName
tycName DataDecl
d)
      Maybe TyCon -> (TyCon -> Maybe Class) -> Maybe Class
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
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, Located (BareTypeV Symbol))])] -> [DataDecl]
makeClassDataDecl = ((Class, [(DFunId, Located (BareTypeV Symbol))]) -> DataDecl)
-> [(Class, [(DFunId, Located (BareTypeV Symbol))])] -> [DataDecl]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Class -> [(DFunId, Located (BareTypeV Symbol))] -> DataDecl)
-> (Class, [(DFunId, Located (BareTypeV Symbol))]) -> DataDecl
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Class -> [(DFunId, Located (BareTypeV Symbol))] -> 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, Located (BareTypeV Symbol))] -> DataDecl
classDeclToDataDecl Class
cls [(DFunId, Located (BareTypeV Symbol))]
refinedIds = DataDecl
  { tycName :: DataName
tycName   = Located LHName -> DataName
DnName (Located LHName -> DataName) -> Located LHName -> DataName
forall a b. (a -> b) -> a -> b
$ Class -> Located LHName
forall a. (NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocated Class
cls
  , tycTyVars :: [Symbol]
tycTyVars = [Symbol]
tyVars
  , tycPVars :: [PVarV Symbol (BSortV Symbol)]
tycPVars  = []
  , tycDCons :: Maybe [DataCtorP (BareTypeV Symbol)]
tycDCons  = [DataCtorP (BareTypeV Symbol)]
-> Maybe [DataCtorP (BareTypeV Symbol)]
forall a. a -> Maybe a
Just [DataCtorP (BareTypeV Symbol)
dctor]
  , tycSrcPos :: SourcePos
tycSrcPos = Located Class -> SourcePos
forall a. Located a -> SourcePos
F.loc (Located Class -> SourcePos)
-> (Class -> Located Class) -> Class -> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Class -> Located Class
forall a. NamedThing a => a -> Located a
GM.locNamedThing (Class -> SourcePos) -> Class -> SourcePos
forall a b. (a -> b) -> a -> b
$ Class
cls
  , tycSFun :: Maybe (SizeFunV Symbol)
tycSFun   = Maybe (SizeFunV Symbol)
forall a. Maybe a
Nothing
  , tycPropTy :: Maybe (BareTypeV Symbol)
tycPropTy = Maybe (BareTypeV Symbol)
forall a. Maybe a
Nothing
  , tycKind :: DataDeclKind
tycKind   = DataDeclKind
DataUser
  }
 where
  dctor :: DataCtorP (BareTypeV Symbol)
dctor = [Char]
-> DataCtorP (BareTypeV Symbol) -> DataCtorP (BareTypeV Symbol)
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"classDeclToDataDecl"
    DataCtor { dcName :: Located LHName
dcName   = LHName -> Located LHName
forall a. a -> Located a
F.dummyLoc (LHName -> Located LHName) -> LHName -> Located LHName
forall a b. (a -> b) -> a -> b
$ Name -> Symbol -> LHName
makeGHCLHName (DataCon -> Name
forall a. NamedThing a => a -> Name
Ghc.getName DataCon
classDc) (DataCon -> Symbol
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 :: [BareTypeV Symbol]
dcTheta  = []
                   , dcFields :: [(LHName, BareTypeV Symbol)]
dcFields = [(LHName, BareTypeV Symbol)]
fields
                   , dcResult :: Maybe (BareTypeV Symbol)
dcResult = Maybe (BareTypeV Symbol)
forall a. Maybe a
Nothing
                   }

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

  fields :: [(LHName, BareTypeV Symbol)]
fields = (DFunId -> (LHName, BareTypeV Symbol))
-> [DFunId] -> [(LHName, BareTypeV Symbol)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DFunId -> (LHName, BareTypeV Symbol)
attachRef [DFunId]
classIds
  attachRef :: DFunId -> (LHName, BareTypeV Symbol)
attachRef DFunId
sid
    | Just Located (BareTypeV Symbol)
ref <- DFunId
-> [(DFunId, Located (BareTypeV Symbol))]
-> Maybe (Located (BareTypeV Symbol))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup DFunId
sid [(DFunId, Located (BareTypeV Symbol))]
refinedIds
    = (DFunId -> LHName
makeGHCLHNameFromId DFunId
sid, [(Symbol, Symbol)] -> BareTypeV Symbol -> BareTypeV Symbol
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
RT.subts [(Symbol, Symbol)]
tyVarSubst (Located (BareTypeV Symbol) -> BareTypeV Symbol
forall a. Located a -> a
F.val Located (BareTypeV Symbol)
ref))
    | Bool
otherwise
    = (DFunId -> LHName
makeGHCLHNameFromId DFunId
sid, Type -> BareTypeV Symbol
forall r. Monoid r => Type -> BRType r
RT.bareOfType (Type -> BareTypeV Symbol)
-> (DFunId -> Type) -> DFunId -> BareTypeV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
dropTheta (Type -> Type) -> (DFunId -> Type) -> DFunId -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DFunId -> Type
Ghc.varType (DFunId -> BareTypeV Symbol) -> DFunId -> BareTypeV Symbol
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 = ([DFunId], Type, Type) -> Type
forall a b c. (a, b, c) -> c
Misc.thd3 (([DFunId], Type, Type) -> Type)
-> (Type -> ([DFunId], Type, Type)) -> Type -> Type
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 -> ExprV Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> DataConP
-> TcRn (DataConP, DataConP)
elaborateClassDcp CoreExpr -> ExprV Symbol
coreToLg CoreExpr -> TcRn CoreExpr
simplifier DataConP
dcp = do
  t' <- ([SpecType] -> [Maybe RReft] -> [SpecType])
-> [Maybe RReft] -> [SpecType] -> [SpecType]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((SpecType -> Maybe RReft -> SpecType)
-> [SpecType] -> [Maybe RReft] -> [SpecType]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SpecType -> Maybe RReft -> SpecType
addCoherenceOblig) [Maybe RReft]
prefts
    ([SpecType] -> [SpecType])
-> IOEnv (Env TcGblEnv TcLclEnv) [SpecType]
-> IOEnv (Env TcGblEnv TcLclEnv) [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
-> (SpecType -> IOEnv (Env TcGblEnv TcLclEnv) SpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [SpecType]
fts ((CoreExpr -> ExprV Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> IOEnv (Env TcGblEnv TcLclEnv) SpecType
elaborateSpecType CoreExpr -> ExprV Symbol
coreToLg CoreExpr -> TcRn CoreExpr
simplifier)
  let ts' = Symbol -> HashSet Symbol -> SpecType -> SpecType
elaborateMethod (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataCon
dc) ([Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ (LHName -> Symbol) -> [LHName] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map LHName -> Symbol
lhNameToResolvedSymbol [LHName]
xs) (SpecType -> SpecType) -> [SpecType] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
t'
  pure
    ( dcp { dcpTyArgs = zip xs (stripPred <$> ts') }
    , dcp { dcpTyArgs = fmap (\(LHName
x, SpecType
t) -> (LHName
x, Symbol -> SpecType -> SpecType
strengthenTy (LHName -> Symbol
lhNameToResolvedSymbol LHName
x) SpecType
t)) (zip xs 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) = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep RTypeRepV Symbol RTyCon RTyVar RReft
rrep
    { ty_res = res `RT.strengthen` r
    }
   where
    rrep :: RTypeRepV Symbol RTyCon RTyVar RReft
rrep = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
t
    res :: SpecType
res  = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res RTypeRepV Symbol RTyCon RTyVar RReft
rrep
  prefts :: [Maybe RReft]
prefts =
    [Maybe RReft] -> [Maybe RReft]
forall a. [a] -> [a]
L.reverse
      ([Maybe RReft] -> [Maybe RReft])
-> ([Maybe RReft] -> [Maybe RReft])
-> [Maybe RReft]
-> [Maybe RReft]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Int -> [Maybe RReft] -> [Maybe RReft]
forall a. Int -> [a] -> [a]
take ([SpecType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
fts)
      ([Maybe RReft] -> [Maybe RReft]) -> [Maybe RReft] -> [Maybe RReft]
forall a b. (a -> b) -> a -> b
$  ([ReftV Symbol] -> Maybe RReft)
-> [[ReftV Symbol]] -> [Maybe RReft]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RReft -> Maybe RReft
forall a. a -> Maybe a
Just (RReft -> Maybe RReft)
-> ([ReftV Symbol] -> RReft) -> [ReftV Symbol] -> Maybe RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReftV Symbol -> PredicateV Symbol -> RReft)
-> PredicateV Symbol -> ReftV Symbol -> RReft
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReftV Symbol -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft PredicateV Symbol
forall a. Monoid a => a
mempty (ReftV Symbol -> RReft)
-> ([ReftV Symbol] -> ReftV Symbol) -> [ReftV Symbol] -> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ReftV Symbol] -> ReftV Symbol
forall a. Monoid a => [a] -> a
mconcat) [[ReftV Symbol]]
preftss
      [Maybe RReft] -> [Maybe RReft] -> [Maybe RReft]
forall a. [a] -> [a] -> [a]
++ Maybe RReft -> [Maybe RReft]
forall a. a -> [a]
repeat Maybe RReft
forall a. Maybe a
Nothing
  preftss :: [[ReftV Symbol]]
preftss = (([([DFunId], [DFunId])] -> [ReftV Symbol])
-> [[([DFunId], [DFunId])]] -> [[ReftV Symbol]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([([DFunId], [DFunId])] -> [ReftV Symbol])
 -> [[([DFunId], [DFunId])]] -> [[ReftV Symbol]])
-> ((([DFunId], [DFunId]) -> ReftV Symbol)
    -> [([DFunId], [DFunId])] -> [ReftV Symbol])
-> (([DFunId], [DFunId]) -> ReftV Symbol)
-> [[([DFunId], [DFunId])]]
-> [[ReftV Symbol]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([DFunId], [DFunId]) -> ReftV Symbol)
-> [([DFunId], [DFunId])] -> [ReftV Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (([DFunId] -> [DFunId] -> ReftV Symbol)
-> ([DFunId], [DFunId]) -> ReftV Symbol
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Symbol -> [DFunId] -> [DFunId] -> ReftV Symbol
forall s. Symbolic s => s -> [DFunId] -> [DFunId] -> ReftV Symbol
GM.coherenceObligToRef Symbol
recsel))
                          (Class -> [[([DFunId], [DFunId])]]
GM.buildCoherenceOblig Class
cls)

  -- ugly, should have passed cls as an argument
  cls :: Class
cls      = Maybe Class -> Class
forall a. HasCallStack => Maybe a -> a
Mb.fromJust (Maybe Class -> Class) -> Maybe Class -> Class
forall a b. (a -> b) -> a -> b
$ TyCon -> Maybe Class
Ghc.tyConClass_maybe (DataCon -> TyCon
Ghc.dataConTyCon DataCon
dc)
  recsel :: Symbol
recsel   = [Char] -> Symbol
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 -> (RTyVar -> RTVar RTyVar s
forall tv s. tv -> RTVar tv s
makeRTVar RTyVar
x, RReft
forall a. Monoid a => a
mempty)) (RTyVar -> (RTVar RTyVar s, RReft))
-> [RTyVar] -> [(RTVar RTyVar s, RReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataConP -> [RTyVar]
dcpFreeTyVars DataConP
dcp
      -- check if the names are qualified
  ([LHName]
xs, [SpecType]
ts) = [(LHName, SpecType)] -> ([LHName], [SpecType])
forall a b. [(a, b)] -> ([a], [b])
unzip (DataConP -> [(LHName, SpecType)]
dcpTyArgs DataConP
dcp)
  fts :: [SpecType]
fts      = SpecType -> SpecType
fullTy (SpecType -> SpecType) -> [SpecType] -> [SpecType]
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 = ([(SpecRTVar, RReft)], [PVar RSort], [(RTyCon, [SpecType])],
 SpecType)
-> SpecType
forall t t1 t2 t3. (t, t1, t2, t3) -> t3
Misc.fourth4 (([(SpecRTVar, RReft)], [PVar RSort], [(RTyCon, [SpecType])],
  SpecType)
 -> SpecType)
-> (SpecType
    -> ([(SpecRTVar, RReft)], [PVar RSort], [(RTyCon, [SpecType])],
        SpecType))
-> SpecType
-> SpecType
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 = [(SpecRTVar, RReft)]
-> [PVar RSort]
-> [(Symbol, RFInfo, SpecType, RReft)]
-> SpecType
-> SpecType
forall tv v c r.
[(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [(Symbol, RFInfo, RTypeV v c tv r, r)]
-> RTypeV v c tv r
-> RTypeV v c tv r
mkArrow
    [(SpecRTVar, RReft)]
forall {s}. [(RTVar RTyVar s, RReft)]
tvars
    []
    [ ( Symbol
recsel{- F.symbol dc-}
      , Bool -> RFInfo
classRFInfo Bool
True
      , SpecType
resTy
      , RReft
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 = [(SpecRTVar, RReft)] -> [PVar RSort] -> SpecType -> SpecType
forall (t :: * -> *) (t1 :: * -> *) tv v c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RTypeV v c tv ()), r)
-> t1 (PVarV v (RTypeV v c tv ()))
-> RTypeV v c tv r
-> RTypeV v c tv r
mkUnivs [(SpecRTVar, RReft)]
tvs [PVar RSort]
pvs (Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
z RFInfo
i SpecType
clas (SpecType
t' SpecType -> RReft -> SpecType
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v 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) = SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], SpecType)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv SpecType
t
    vv :: Symbol
vv = SpecType -> Symbol
forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar SpecType
t'
    mt :: RReft
mt = (Symbol, ExprV Symbol) -> RReft
RT.uReft (Symbol
vv, Brel -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
F.PAtom Brel
F.Eq (Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
vv) (ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
F.EApp (Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
x) (Symbol -> ExprV Symbol
forall v. v -> ExprV v
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 = (Symbol -> ExprV Symbol -> ExprV Symbol) -> SpecType -> SpecType
forall c tv.
(Symbol -> ExprV Symbol -> ExprV Symbol)
-> RType c tv RReft -> RType c tv RReft
mapExprReft
  (\Symbol
_ -> Symbol -> Symbol -> HashSet Symbol -> ExprV Symbol -> ExprV Symbol
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 =
    [Char] -> Symbol -> Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"grabtcbind"
      (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ case ([Symbol], [RFInfo], [SpecType], [RReft]) -> [Symbol]
forall t t1 t2 t3. (t, t1, t2, t3) -> t
Misc.fst4 (([Symbol], [RFInfo], [SpecType], [RReft]) -> [Symbol])
-> (SpecType -> ([Symbol], [RFInfo], [SpecType], [RReft]))
-> SpecType
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Symbol], [RFInfo], [SpecType], [RReft]), SpecType)
-> ([Symbol], [RFInfo], [SpecType], [RReft])
forall a b. (a, b) -> a
fst ((([Symbol], [RFInfo], [SpecType], [RReft]), SpecType)
 -> ([Symbol], [RFInfo], [SpecType], [RReft]))
-> (SpecType
    -> (([Symbol], [RFInfo], [SpecType], [RReft]), SpecType))
-> SpecType
-> ([Symbol], [RFInfo], [SpecType], [RReft])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> (([Symbol], [RFInfo], [SpecType], [RReft]), SpecType)
forall v t t1 a.
RTypeV v t t1 a
-> (([Symbol], [RFInfo], [RTypeV v t t1 a], [a]), RTypeV v t t1 a)
bkArrow (SpecType -> (([Symbol], [RFInfo], [SpecType], [RReft]), SpecType))
-> (SpecType -> SpecType)
-> SpecType
-> (([Symbol], [RFInfo], [SpecType], [RReft]), SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(SpecRTVar, RReft)], [PVar RSort], SpecType) -> SpecType
forall a b c. (a, b, c) -> c
Misc.thd3 (([(SpecRTVar, RReft)], [PVar RSort], SpecType) -> SpecType)
-> (SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], SpecType))
-> SpecType
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], SpecType)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv (SpecType -> [Symbol]) -> SpecType -> [Symbol]
forall a b. (a -> b) -> a -> b
$ SpecType
t of
          Symbol
tcbind : [Symbol]
_ -> Symbol
tcbind
          []         -> Maybe SrcSpan -> [Char] -> Symbol
forall a. Maybe SrcSpan -> [Char] -> a
impossible
            Maybe SrcSpan
forall a. Maybe a
Nothing
            (  [Char]
"elaborateMethod: inserted dictionary binder disappeared:"
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
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 -> ExprV Symbol -> ExprV Symbol
substClassOpBinding Symbol
tcbind Symbol
dc HashSet Symbol
methods = ExprV Symbol -> ExprV Symbol
go
 where
  go :: F.Expr -> F.Expr
  go :: ExprV Symbol -> ExprV Symbol
go (F.EApp ExprV Symbol
e0 ExprV Symbol
e1)
    | F.EVar Symbol
x <- ExprV Symbol
e0, F.EVar Symbol
y <- ExprV Symbol
e1, Symbol
y Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
tcbind, Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x HashSet Symbol
methods = Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar
      (Symbol
x Symbol -> Symbol -> Symbol
`F.suffixSymbol` Symbol
dc)
    | Bool
otherwise = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
F.EApp (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1)
  go (F.ENeg ExprV Symbol
e          ) = ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
F.ENeg (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e)
  go (F.EBin Bop
bop ExprV Symbol
e0 ExprV Symbol
e1  ) = Bop -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
F.EBin Bop
bop (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1)
  go (F.EIte ExprV Symbol
e0  ExprV Symbol
e1 ExprV Symbol
e2  ) = ExprV Symbol -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
F.EIte (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e2)
  go (F.ECst ExprV Symbol
e0     Sort
s   ) = ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
F.ECst (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) Sort
s
  go (F.ELam (Symbol
x, Sort
t) ExprV Symbol
body) = (Symbol, Sort) -> ExprV Symbol -> ExprV Symbol
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
F.ELam (Symbol
x, Sort
t) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
body)
  go (F.PAnd [ExprV Symbol]
es         ) = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
F.PAnd (ExprV Symbol -> ExprV Symbol
go (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
es)
  go (F.POr  [ExprV Symbol]
es         ) = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
F.POr (ExprV Symbol -> ExprV Symbol
go (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
es)
  go (F.PNot ExprV Symbol
e          ) = ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
F.PNot (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e)
  go (F.PImp ExprV Symbol
e0 ExprV Symbol
e1      ) = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
F.PImp (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1)
  go (F.PIff ExprV Symbol
e0 ExprV Symbol
e1      ) = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
F.PIff (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1)
  go (F.PAtom Brel
brel ExprV Symbol
e0 ExprV Symbol
e1) = Brel -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
F.PAtom Brel
brel (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1)
  -- a catch-all binding is not a good idea
  go ExprV Symbol
e                    = ExprV Symbol
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
  = tv -> r -> RType c tv r
forall v c tv r. tv -> r -> RTypeV v 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
  = Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
b RFInfo
i ((tv -> tv) -> RType c tv r -> RType c tv r
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) ((tv -> tv) -> RType c tv r -> RType c tv r
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 (RTypeV Symbol c tv ())
info) RType c tv r
tres r
r <- RType c tv r
t
  = RTVar tv (RTypeV Symbol c tv ())
-> RType c tv r -> r -> RType c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT (tv
-> RTVInfo (RTypeV Symbol c tv ())
-> RTVar tv (RTypeV Symbol c tv ())
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar (tv -> tv
rename tv
tv) RTVInfo (RTypeV Symbol c tv ())
info) ((tv -> tv) -> RType c tv r -> RType c tv r
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 PVUV Symbol c tv
b RType c tv r
tres <- RType c tv r
t
  = PVUV Symbol c tv -> RType c tv r -> RType c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP ((tv -> tv) -> RTypeV Symbol c tv () -> RTypeV Symbol c tv ()
forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename (RTypeV Symbol c tv () -> RTypeV Symbol c tv ())
-> PVUV Symbol c tv -> PVUV Symbol c tv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVUV Symbol c tv
b) ((tv -> tv) -> RType c tv r -> RType c tv r
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 [RTPropV Symbol c tv r]
tps r
r <- RType c tv r
t
  -- TODO: handle rtprop properly
  = c -> [RType c tv r] -> [RTPropV Symbol c tv r] -> r -> RType c tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp c
tc ((tv -> tv) -> RType c tv r -> RType c tv r
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 -> RType c tv r) -> [RType c tv r] -> [RType c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv r]
ts) [RTPropV Symbol c tv r]
tps r
r
  | RAllE Symbol
b RType c tv r
allarg RType c tv r
ty <- RType c tv r
t
  = Symbol -> RType c tv r -> RType c tv r -> RType c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
b ((tv -> tv) -> RType c tv r -> RType c tv r
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) ((tv -> tv) -> RType c tv r -> RType c tv r
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
  = Symbol -> RType c tv r -> RType c tv r -> RType c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx Symbol
b   ((tv -> tv) -> RType c tv r -> RType c tv r
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) ((tv -> tv) -> RType c tv r -> RType c tv r
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 (ExprV Symbol)
_ <- 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
  = RType c tv r -> RType c tv r -> r -> RType c tv r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy ((tv -> tv) -> RType c tv r -> RType c tv r
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) ((tv -> tv) -> RType c tv r -> RType c tv r
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
  = [(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy ((RType c tv r -> RType c tv r)
-> (Symbol, RType c tv r) -> (Symbol, RType c tv r)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((tv -> tv) -> RType c tv r -> RType c tv r
forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename) ((Symbol, RType c tv r) -> (Symbol, RType c tv r))
-> [(Symbol, RType c tv r)] -> [(Symbol, RType c tv r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv r)]
env) r
r Oblig
obl ((tv -> tv) -> RType c tv r -> RType c tv r
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 -> IOEnv (Env TcGblEnv TcLclEnv) SpecType)
-> [Located DataConP]
-> [(ClsInst, [DFunId])]
-> TcRn [(DFunId, LocSpecType)]
makeClassAuxTypes SpecType -> IOEnv (Env TcGblEnv TcLclEnv) SpecType
elab [Located DataConP]
dcps [(ClsInst, [DFunId])]
xs = ((Located DataConP, ClsInst, [DFunId])
 -> TcRn [(DFunId, LocSpecType)])
-> [(Located DataConP, ClsInst, [DFunId])]
-> TcRn [(DFunId, LocSpecType)]
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(a -> m [b]) -> t a -> m [b]
Misc.concatMapM ((SpecType -> IOEnv (Env TcGblEnv TcLclEnv) SpecType)
-> (Located DataConP, ClsInst, [DFunId])
-> TcRn [(DFunId, LocSpecType)]
makeClassAuxTypesOne SpecType -> IOEnv (Env TcGblEnv TcLclEnv) SpecType
elab) [(Located DataConP, ClsInst, [DFunId])]
dcpInstMethods
  where
    dcpInstMethods :: [(Located DataConP, ClsInst, [DFunId])]
dcpInstMethods = do
      dcp <- [Located DataConP]
dcps
      (inst, methods) <- xs
      let dc = DataConP -> DataCon
dcpCon (DataConP -> DataCon)
-> (Located DataConP -> DataConP) -> Located DataConP -> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located DataConP -> DataConP
forall a. Located a -> a
F.val (Located DataConP -> DataCon) -> Located DataConP -> DataCon
forall a b. (a -> b) -> a -> b
$ Located DataConP
dcp
              -- YL: only works for non-newtype class
          dc' = Class -> DataCon
Ghc.classDataCon (Class -> DataCon) -> Class -> DataCon
forall a b. (a -> b) -> a -> b
$ ClsInst -> Class
Ghc.is_cls ClsInst
inst
      guard $ dc == dc'
      pure (dcp, inst, methods)

makeClassAuxTypesOne ::
     (SpecType -> Ghc.TcRn SpecType)
  -> (F.Located DataConP, Ghc.ClsInst, [Ghc.Var])
  -> Ghc.TcRn [(Ghc.Var, LocSpecType)]
makeClassAuxTypesOne :: (SpecType -> IOEnv (Env TcGblEnv TcLclEnv) SpecType)
-> (Located DataConP, ClsInst, [DFunId])
-> TcRn [(DFunId, LocSpecType)]
makeClassAuxTypesOne SpecType -> IOEnv (Env TcGblEnv TcLclEnv) SpecType
elab (Located DataConP
ldcp, ClsInst
inst, [DFunId]
methods) =
  [DFunId]
-> (DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (DFunId, LocSpecType))
-> TcRn [(DFunId, LocSpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DFunId]
methods ((DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (DFunId, LocSpecType))
 -> TcRn [(DFunId, LocSpecType)])
-> (DFunId -> IOEnv (Env TcGblEnv TcLclEnv) (DFunId, LocSpecType))
-> TcRn [(DFunId, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ \DFunId
method -> do
    let (SpecType
headlessSig, Maybe RReft
preft) =
          case Symbol
-> [(Symbol, (SpecType, Maybe RReft))]
-> Maybe (SpecType, Maybe RReft)
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 ->
              Maybe SrcSpan -> [Char] -> (SpecType, Maybe RReft)
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"makeClassAuxTypesOne : unreachable?" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (DFunId -> Symbol
mkSymbol DFunId
method) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(Symbol, SpecType)] -> [Char]
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 (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i), Bool -> RFInfo
classRFInfo Bool
True, SpecType
pty, RReft
forall a. Monoid a => a
mempty) | (Integer
i,SpecType
pty) <- [Integer] -> [SpecType] -> [(Integer, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0,Integer
1..] [SpecType]
isPredSpecTys]
        fullSig :: SpecType
fullSig =
          [(SpecRTVar, RReft)]
-> [PVar RSort]
-> [(Symbol, RFInfo, SpecType, RReft)]
-> SpecType
-> SpecType
forall tv v c r.
[(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [(Symbol, RFInfo, RTypeV v c tv r, r)]
-> RTypeV v c tv r
-> RTypeV v c tv r
mkArrow
            ([SpecRTVar] -> [RReft] -> [(SpecRTVar, RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SpecRTVar]
forall {s}. [RTVar RTyVar s]
isRTvs (RReft -> [RReft]
forall a. a -> [a]
repeat RReft
forall a. Monoid a => a
mempty))
            []
            [(Symbol, RFInfo, SpecType, RReft)]
ptys (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          [(RTyVar, SpecType)] -> SpecType -> SpecType
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 ([RTyVar] -> [SpecType] -> [(RTyVar, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RTyVar]
clsTvs [SpecType]
isSpecTys) (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$
          SpecType
headlessSig
    elaboratedSig  <- (SpecType -> Maybe RReft -> SpecType)
-> Maybe RReft -> SpecType -> SpecType
forall a b c. (a -> b -> c) -> b -> a -> c
flip SpecType -> Maybe RReft -> SpecType
addCoherenceOblig Maybe RReft
preft (SpecType -> SpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) SpecType
-> IOEnv (Env TcGblEnv TcLclEnv) SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> IOEnv (Env TcGblEnv TcLclEnv) SpecType
elab SpecType
fullSig

    let retSig =  (Symbol -> ExprV Symbol -> ExprV Symbol) -> SpecType -> SpecType
forall c tv.
(Symbol -> ExprV Symbol -> ExprV Symbol)
-> RType c tv RReft -> RType c tv RReft
mapExprReft (\Symbol
_ -> Symbol -> HashMap Symbol Symbol -> ExprV Symbol -> ExprV Symbol
substAuxMethod Symbol
dfunSym HashMap Symbol Symbol
methodsSet) ([Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"elaborated" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DFunId -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr DFunId
method) SpecType
elaboratedSig)
    let tysub  = [Char] -> HashMap RTyVar RTyVar -> HashMap RTyVar RTyVar
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"tysub" (HashMap RTyVar RTyVar -> HashMap RTyVar RTyVar)
-> HashMap RTyVar RTyVar -> HashMap RTyVar RTyVar
forall a b. (a -> b) -> a -> b
$ [(RTyVar, RTyVar)] -> HashMap RTyVar RTyVar
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(RTyVar, RTyVar)] -> HashMap RTyVar RTyVar)
-> [(RTyVar, RTyVar)] -> HashMap RTyVar RTyVar
forall a b. (a -> b) -> a -> b
$ [RTyVar] -> [RTyVar] -> [(RTyVar, RTyVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Char] -> [RTyVar] -> [RTyVar]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"newtype-vars" ([RTyVar] -> [RTyVar]) -> [RTyVar] -> [RTyVar]
forall a b. (a -> b) -> a -> b
$ SpecType -> [RTyVar]
forall tv c r. Eq tv => RType c tv r -> [tv]
RT.allTyVars' ([Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"new-type" SpecType
retSig)) ([Char] -> [RTyVar] -> [RTyVar]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"ghc-type-vars" (SpecType -> [RTyVar]
forall tv c r. Eq tv => RType c tv r -> [tv]
RT.allTyVars' (([Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"ghc-type" (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ Type -> SpecType
forall r. Monoid r => Type -> RRType r
RT.ofType (DFunId -> Type
Ghc.varType DFunId
method)) :: SpecType)))
        cosub  = [(Symbol, Sort)] -> HashMap Symbol Sort
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (RTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol RTyVar
a, LocSymbol -> Sort
F.fObj (DFunId -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol DFunId
b)) |  (RTyVar
a,RTV DFunId
b) <- HashMap RTyVar RTyVar -> [(RTyVar, RTyVar)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap RTyVar RTyVar
tysub]
        tysubf RTyVar
x = [Char] -> RTyVar -> RTyVar
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"cosub:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ HashMap Symbol Sort -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp HashMap Symbol Sort
cosub) (RTyVar -> RTyVar) -> RTyVar -> RTyVar
forall a b. (a -> b) -> a -> b
$ RTyVar -> RTyVar -> HashMap RTyVar RTyVar -> RTyVar
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault RTyVar
x RTyVar
x HashMap RTyVar RTyVar
tysub
        subbedTy = (RReft -> RReft) -> SpecType -> SpecType
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft (HashMap Symbol Sort -> RReft -> RReft
Bare.coSubRReft HashMap Symbol Sort
cosub) ((RTyVar -> RTyVar) -> SpecType -> SpecType
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
    pure (method, F.dummyLoc (F.notracepp ("vars:" ++ F.showpp (F.symbol <$> RT.allTyVars' subbedTy)) 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 :: ExprV Symbol
dfunApped = LocSymbol -> [ExprV Symbol] -> ExprV Symbol
F.mkEApp LocSymbol
dfunSymL [Symbol -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
F.eVar (Symbol -> ExprV Symbol) -> Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Maybe Integer -> Symbol
F.vv (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i) | (Integer
i,Type
_) <- [Integer] -> [Type] -> [(Integer, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0,Integer
1..] [Type]
predTys]
    prefts :: [Maybe RReft]
prefts  = [Maybe RReft] -> [Maybe RReft]
forall a. [a] -> [a]
L.reverse ([Maybe RReft] -> [Maybe RReft])
-> ([Maybe RReft] -> [Maybe RReft])
-> [Maybe RReft]
-> [Maybe RReft]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Maybe RReft] -> [Maybe RReft]
forall a. Int -> [a] -> [a]
take ([(Symbol, SpecType)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, SpecType)]
yts) ([Maybe RReft] -> [Maybe RReft]) -> [Maybe RReft] -> [Maybe RReft]
forall a b. (a -> b) -> a -> b
$ ([ReftV Symbol] -> Maybe RReft)
-> [[ReftV Symbol]] -> [Maybe RReft]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> Maybe RReft -> Maybe RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"prefts" (Maybe RReft -> Maybe RReft)
-> ([ReftV Symbol] -> Maybe RReft) -> [ReftV Symbol] -> Maybe RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RReft -> Maybe RReft
forall a. a -> Maybe a
Just (RReft -> Maybe RReft)
-> ([ReftV Symbol] -> RReft) -> [ReftV Symbol] -> Maybe RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReftV Symbol -> PredicateV Symbol -> RReft)
-> PredicateV Symbol -> ReftV Symbol -> RReft
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReftV Symbol -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft PredicateV Symbol
forall a. Monoid a => a
mempty (ReftV Symbol -> RReft)
-> ([ReftV Symbol] -> ReftV Symbol) -> [ReftV Symbol] -> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ReftV Symbol] -> ReftV Symbol
forall a. Monoid a => [a] -> a
mconcat) [[ReftV Symbol]]
preftss [Maybe RReft] -> [Maybe RReft] -> [Maybe RReft]
forall a. [a] -> [a] -> [a]
++ Maybe RReft -> [Maybe RReft]
forall a. a -> [a]
repeat Maybe RReft
forall a. Maybe a
Nothing
    preftss :: [[ReftV Symbol]]
preftss = [Char] -> [[ReftV Symbol]] -> [[ReftV Symbol]]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"preftss" ([[ReftV Symbol]] -> [[ReftV Symbol]])
-> [[ReftV Symbol]] -> [[ReftV Symbol]]
forall a b. (a -> b) -> a -> b
$ (([([DFunId], [DFunId])] -> [ReftV Symbol])
-> [[([DFunId], [DFunId])]] -> [[ReftV Symbol]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap(([([DFunId], [DFunId])] -> [ReftV Symbol])
 -> [[([DFunId], [DFunId])]] -> [[ReftV Symbol]])
-> ((([DFunId], [DFunId]) -> ReftV Symbol)
    -> [([DFunId], [DFunId])] -> [ReftV Symbol])
-> (([DFunId], [DFunId]) -> ReftV Symbol)
-> [[([DFunId], [DFunId])]]
-> [[ReftV Symbol]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(([DFunId], [DFunId]) -> ReftV Symbol)
-> [([DFunId], [DFunId])] -> [ReftV Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (([DFunId] -> [DFunId] -> ReftV Symbol)
-> ([DFunId], [DFunId]) -> ReftV Symbol
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprV Symbol -> [DFunId] -> [DFunId] -> ReftV Symbol
GM.coherenceObligToRefE ExprV Symbol
dfunApped)) (Class -> [[([DFunId], [DFunId])]]
GM.buildCoherenceOblig Class
cls)
    yts' :: [(Symbol, (SpecType, Maybe RReft))]
yts' = [Symbol]
-> [(SpecType, Maybe RReft)] -> [(Symbol, (SpecType, Maybe RReft))]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Symbol, SpecType) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, SpecType) -> Symbol) -> [(Symbol, SpecType)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
yts) ([SpecType] -> [Maybe RReft] -> [(SpecType, Maybe RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd ((Symbol, SpecType) -> SpecType)
-> [(Symbol, SpecType)] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
yts) [Maybe RReft]
prefts)
    cls :: Class
cls = Maybe Class -> Class
forall a. HasCallStack => Maybe a -> a
Mb.fromJust (Maybe Class -> Class) -> (TyCon -> Maybe Class) -> TyCon -> Class
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Maybe Class
Ghc.tyConClass_maybe (TyCon -> Class) -> TyCon -> Class
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) = [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"SCSel" (SpecType -> SpecType)
-> (RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType)
-> RTypeRepV Symbol RTyCon RTyVar RReft
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType)
-> RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol RTyCon RTyVar RReft
rrep {ty_res = res `RT.strengthen` r}
      where rrep :: RTypeRepV Symbol RTyCon RTyVar RReft
rrep = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
t
            res :: SpecType
res  = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res RTypeRepV Symbol RTyCon RTyVar RReft
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 = [Char] -> HashMap Symbol Symbol -> HashMap Symbol Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"methodSet" (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 (DFunId -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DFunId -> Symbol) -> [DFunId] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DFunId]
clsMethods) (DFunId -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DFunId -> Symbol) -> [DFunId] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DFunId]
methods))
    -- core rewriting mark1: dfunId
    -- ()
    dfunSymL :: LocSymbol
dfunSymL = DFunId -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol (DFunId -> LocSymbol) -> DFunId -> LocSymbol
forall a b. (a -> b) -> a -> b
$ ClsInst -> DFunId
Ghc.instanceDFunId ClsInst
inst
    dfunSym :: Symbol
dfunSym = LocSymbol -> Symbol
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 = Type -> SpecType
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> SpecType) -> [Type] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
isTys
    isPredSpecTys :: [SpecType]
isPredSpecTys = Type -> SpecType
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> SpecType) -> [Type] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
isPredTys
    isRTvs :: [RTVar RTyVar s]
isRTvs = RTyVar -> RTVar RTyVar s
forall tv s. tv -> RTVar tv s
makeRTVar (RTyVar -> RTVar RTyVar s)
-> (DFunId -> RTyVar) -> DFunId -> RTVar RTyVar s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DFunId -> RTyVar
RT.rTyVar (DFunId -> RTVar RTyVar s) -> [DFunId] -> [RTVar RTyVar s]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DFunId]
isTvs
    dcp :: DataConP
dcp = Located DataConP -> DataConP
forall a. Located a -> a
F.val Located DataConP
ldcp
    -- Monoid.mappend, ...
    clsMethods :: [DFunId]
clsMethods = (DFunId -> Bool) -> [DFunId] -> [DFunId]
forall a. (a -> Bool) -> [a] -> [a]
filter (\DFunId
x -> Symbol -> Symbol
GM.dropModuleNames (DFunId -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DFunId
x) Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (DFunId -> Symbol) -> [DFunId] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DFunId -> Symbol
mkSymbol [DFunId]
methods) ([DFunId] -> [DFunId]) -> [DFunId] -> [DFunId]
forall a b. (a -> b) -> a -> b
$
      Class -> [DFunId]
Ghc.classAllSelIds (ClsInst -> Class
Ghc.is_cls ClsInst
inst)
    yts :: [(Symbol, SpecType)]
yts = [(LHName -> Symbol
lhNameToResolvedSymbol LHName
y, SpecType
t) | (LHName
y, SpecType
t) <- DataConP -> [(LHName, 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 (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ DFunId -> Symbol
forall t. NamedThing t => t -> Symbol
GM.simplesymbol DFunId
x)
      | Bool
otherwise = Int -> Symbol -> Symbol
F.dropSym Int
2 (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ DFunId -> Symbol
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 = (tv, RType c tv r) -> RType c tv r -> RType c tv r
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
RT.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 -> ExprV Symbol -> ExprV Symbol
substAuxMethod Symbol
dfun HashMap Symbol Symbol
methods = [Char] -> ExprV Symbol -> ExprV Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"substAuxMethod" (ExprV Symbol -> ExprV Symbol)
-> (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprV Symbol -> ExprV Symbol
go
  where go :: F.Expr -> F.Expr
        go :: ExprV Symbol -> ExprV Symbol
go (F.EApp ExprV Symbol
e0 ExprV Symbol
e1)
          | F.EVar Symbol
x <- [Char] -> ExprV Symbol -> ExprV Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"e0" ExprV Symbol
e0
          , (F.EVar Symbol
dfun_mb, [ExprV Symbol]
args)  <- ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
F.splitEApp ExprV Symbol
e1
          , Symbol
dfun_mb Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dfun
          , Just Symbol
method <- Symbol -> HashMap Symbol Symbol -> Maybe Symbol
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)
           = ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
F.eApps (Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
method) [ExprV Symbol]
args
          | Bool
otherwise
          = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
F.EApp (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1)
        go (F.ENeg ExprV Symbol
e) = ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
F.ENeg (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e)
        go (F.EBin Bop
bop ExprV Symbol
e0 ExprV Symbol
e1) = Bop -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
F.EBin Bop
bop (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1)
        go (F.EIte ExprV Symbol
e0 ExprV Symbol
e1 ExprV Symbol
e2) = ExprV Symbol -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
F.EIte (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e2)
        go (F.ECst ExprV Symbol
e0 Sort
s) = ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
F.ECst (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) Sort
s
        go (F.ELam (Symbol
x, Sort
t) ExprV Symbol
body) = (Symbol, Sort) -> ExprV Symbol -> ExprV Symbol
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
F.ELam (Symbol
x, Sort
t) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
body)
        go (F.PAnd [ExprV Symbol]
es) = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
F.PAnd (ExprV Symbol -> ExprV Symbol
go (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
es)
        go (F.POr [ExprV Symbol]
es) = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
F.POr (ExprV Symbol -> ExprV Symbol
go (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
es)
        go (F.PNot ExprV Symbol
e) = ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
F.PNot (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e)
        go (F.PImp ExprV Symbol
e0 ExprV Symbol
e1) = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
F.PImp (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1)
        go (F.PIff ExprV Symbol
e0 ExprV Symbol
e1) = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
F.PIff (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1)
        go (F.PAtom Brel
brel ExprV Symbol
e0 ExprV Symbol
e1) = Brel -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
F.PAtom Brel
brel (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e0) (ExprV Symbol -> ExprV Symbol
go ExprV Symbol
e1)
        go ExprV Symbol
e = [Char] -> ExprV Symbol -> ExprV Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"LEAF" ExprV Symbol
e