{-# 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, Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)]
-> (Spec Symbol BareType, [(ClsInst, [Var])])
compileClasses GhcSrc
src Env
env (ModName
name, Spec Symbol BareType
spec) [(ModName, Spec Symbol BareType)]
rest =
  (Spec Symbol BareType
spec { sigs = sigsNew } Spec Symbol BareType
-> Spec Symbol BareType -> Spec Symbol BareType
forall a. Semigroup a => a -> a -> a
<> Spec Symbol BareType
clsSpec, [(ClsInst, [Var])]
instmethods)
 where
  clsSpec :: Spec Symbol BareType
clsSpec = Spec Symbol BareType
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, [(Var, Located BareType)])] -> [DataDecl]
makeClassDataDecl (HashMap Class [(Var, Located BareType)]
-> [(Class, [(Var, Located BareType)])]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Class [(Var, Located BareType)]
refinedMethods)
      -- class methods
  (HashMap Class [(Var, Located BareType)]
refinedMethods, [(Located LHName, Located BareType)]
sigsNew) = ((Located LHName, Located BareType)
 -> (HashMap Class [(Var, Located BareType)],
     [(Located LHName, Located BareType)])
 -> (HashMap Class [(Var, Located BareType)],
     [(Located LHName, Located BareType)]))
-> (HashMap Class [(Var, Located BareType)],
    [(Located LHName, Located BareType)])
-> [(Located LHName, Located BareType)]
-> (HashMap Class [(Var, Located BareType)],
    [(Located LHName, Located BareType)])
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 BareType)
-> (HashMap Class [(Var, Located BareType)],
    [(Located LHName, Located BareType)])
-> (HashMap Class [(Var, Located BareType)],
    [(Located LHName, Located BareType)])
forall ty.
(Located LHName, ty)
-> (HashMap Class [(Var, ty)], [(Located LHName, ty)])
-> (HashMap Class [(Var, ty)], [(Located LHName, ty)])
grabClassSig (HashMap Class [(Var, Located BareType)]
forall a. Monoid a => a
mempty, [(Located LHName, Located BareType)]
forall a. Monoid a => a
mempty) (Spec Symbol BareType -> [(Located LHName, Located BareType)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
sigs Spec Symbol BareType
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 [(Var, ty)], [(Located LHName, ty)])
-> (HashMap Class [(Var, ty)], [(Located LHName, ty)])
grabClassSig sigPair :: (Located LHName, ty)
sigPair@(Located LHName
lsym, ty
ref) (HashMap Class [(Var, ty)]
refs, [(Located LHName, ty)]
sigs') = case Maybe (Class, (Var, ty))
clsOp of
    Maybe (Class, (Var, ty))
Nothing         -> (HashMap Class [(Var, 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, (Var, ty)
sig) -> ((Maybe [(Var, ty)] -> Maybe [(Var, ty)])
-> Class -> HashMap Class [(Var, ty)] -> HashMap Class [(Var, ty)]
forall k v.
Hashable k =>
(Maybe v -> Maybe v) -> k -> HashMap k v -> HashMap k v
M.alter ((Var, ty) -> Maybe [(Var, ty)] -> Maybe [(Var, ty)]
forall {a}. a -> Maybe [a] -> Maybe [a]
merge (Var, ty)
sig) Class
cls HashMap Class [(Var, ty)]
refs, [(Located LHName, ty)]
sigs')
   where
    clsOp :: Maybe (Class, (Var, ty))
clsOp = do
      var <- ([Error] -> Maybe Var)
-> (Var -> Maybe Var) -> Either [Error] Var -> Maybe Var
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe Var -> [Error] -> Maybe Var
forall a b. a -> b -> a
const Maybe Var
forall a. Maybe a
Nothing) Var -> Maybe Var
forall a. a -> Maybe a
Just (Either [Error] Var -> Maybe Var)
-> Either [Error] Var -> Maybe Var
forall a b. (a -> b) -> a -> b
$ HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
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 = [ Var -> Located LHName
makeGHCLHNameLocatedFromId Var
x | (ClsInst
_, [Var]
xs) <- [(ClsInst, [Var])]
instmethods, Var
x <- [Var]
xs ]
      -- instance methods

  mkSymbol :: Var -> Symbol
mkSymbol Var
x
    | Var -> Bool
Ghc.isDictonaryId Var
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
$ Var -> Symbol
forall t. NamedThing t => t -> Symbol
GM.simplesymbol Var
x)
    | Bool
otherwise           = Int -> Symbol -> Symbol
F.dropSym Int
2 (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall t. NamedThing t => t -> Symbol
GM.simplesymbol Var
x

  instmethods :: [(Ghc.ClsInst, [Ghc.Var])]
  instmethods :: [(ClsInst, [Var])]
instmethods =
    [ (ClsInst
inst, [Var]
ms)
    | (ClsInst
inst, Class
cls) <- [(ClsInst, Class)]
instClss
    , let selIds :: [Symbol]
selIds = Symbol -> Symbol
GM.dropModuleNames (Symbol -> Symbol) -> (Var -> Symbol) -> Var -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Class -> [Var]
Ghc.classAllSelIds Class
cls
    , (Var
_, CoreExpr
e) <- Maybe (Var, CoreExpr) -> [(Var, CoreExpr)]
forall a. Maybe a -> [a]
Mb.maybeToList
      (Symbol -> [CoreBind] -> Maybe (Var, CoreExpr)
GM.findVarDefMethod
        (Symbol -> Symbol
GM.dropModuleNames (Symbol -> Symbol) -> (Var -> Symbol) -> Var -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> Var -> Symbol
forall a b. (a -> b) -> a -> b
$ ClsInst -> Var
Ghc.instanceDFunId ClsInst
inst)
        (GhcSrc -> [CoreBind]
_giCbs GhcSrc
src)
      )
    , let ms :: [Var]
ms = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Var
x -> Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isMethod Var
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 (Var -> Symbol
mkSymbol Var
x) [Symbol]
selIds)
                      (HashSet Var -> CoreExpr -> [Var]
forall a. CBVisitable a => HashSet Var -> a -> [Var]
freeVars HashSet Var
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, Spec Symbol BareType) -> [Class])
-> [(ModName, Spec Symbol BareType)] -> [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, Spec Symbol BareType) -> [DataDecl])
-> (ModName, Spec Symbol BareType)
-> [Class]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec Symbol BareType -> [DataDecl]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
dataDecls (Spec Symbol BareType -> [DataDecl])
-> ((ModName, Spec Symbol BareType) -> Spec Symbol BareType)
-> (ModName, Spec Symbol BareType)
-> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec Symbol BareType) -> Spec Symbol BareType
forall a b. (a, b) -> b
snd) [(ModName, Spec Symbol BareType)]
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, [(Var, Located BareType)])] -> [DataDecl]
makeClassDataDecl = ((Class, [(Var, Located BareType)]) -> DataDecl)
-> [(Class, [(Var, Located BareType)])] -> [DataDecl]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Class -> [(Var, Located BareType)] -> DataDecl)
-> (Class, [(Var, Located BareType)]) -> DataDecl
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Class -> [(Var, Located BareType)] -> 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 -> [(Var, Located BareType)] -> DataDecl
classDeclToDataDecl Class
cls [(Var, Located BareType)]
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 BareType]
tycDCons  = [DataCtorP BareType] -> Maybe [DataCtorP BareType]
forall a. a -> Maybe a
Just [DataCtorP BareType
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 BareType
tycPropTy = Maybe BareType
forall a. Maybe a
Nothing
  , tycKind :: DataDeclKind
tycKind   = DataDeclKind
DataUser
  }
 where
  dctor :: DataCtorP BareType
dctor = [Char] -> DataCtorP BareType -> DataCtorP BareType
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 :: [BareType]
dcTheta  = []
                   , dcFields :: [(LHName, BareType)]
dcFields = [(LHName, BareType)]
fields
                   , dcResult :: Maybe BareType
dcResult = Maybe BareType
forall a. Maybe a
Nothing
                   }

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

  fields :: [(LHName, BareType)]
fields = (Var -> (LHName, BareType)) -> [Var] -> [(LHName, BareType)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var -> (LHName, BareType)
attachRef [Var]
classIds
  attachRef :: Var -> (LHName, BareType)
attachRef Var
sid
    | Just Located BareType
ref <- Var -> [(Var, Located BareType)] -> Maybe (Located BareType)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Var
sid [(Var, Located BareType)]
refinedIds
    = (Var -> LHName
makeGHCLHNameFromId Var
sid, [(Symbol, Symbol)] -> BareType -> BareType
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
RT.subts [(Symbol, Symbol)]
tyVarSubst (Located BareType -> BareType
forall a. Located a -> a
F.val Located BareType
ref))
    | Bool
otherwise
    = (Var -> LHName
makeGHCLHNameFromId Var
sid, Type -> BareType
forall r. IsReft r => Type -> BRType r
RT.bareOfType (Type -> BareType) -> (Var -> Type) -> Var -> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
dropTheta (Type -> Type) -> (Var -> Type) -> Var -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type
Ghc.varType (Var -> BareType) -> Var -> BareType
forall a b. (a -> b) -> a -> b
$ Var
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 = ([Var], Type, Type) -> Type
forall a b c. (a, b, c) -> c
Misc.thd3 (([Var], Type, Type) -> Type)
-> (Type -> ([Var], Type, Type)) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ([Var], Type, Type)
Ghc.tcSplitMethodTy

  classIds :: [Var]
classIds  = Class -> [Var]
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 -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> DataConP
-> TcRn (DataConP, DataConP)
elaborateClassDcp CoreExpr -> ExprBV Symbol Symbol
coreToLg CoreExpr -> TcRn CoreExpr
simplifier DataConP
dcp = do
  t' <- ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
 -> [Maybe RReft] -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
-> [Maybe RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> Maybe RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [Maybe RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> Maybe RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
addCoherenceOblig) [Maybe RReft]
prefts
    ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
 -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
-> IOEnv
     (Env TcGblEnv TcLclEnv) [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> IOEnv
     (Env TcGblEnv TcLclEnv) [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> IOEnv
         (Env TcGblEnv TcLclEnv)
         (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> IOEnv
     (Env TcGblEnv TcLclEnv) [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
fts ((CoreExpr -> ExprBV Symbol Symbol)
-> (CoreExpr -> TcRn CoreExpr)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> IOEnv
     (Env TcGblEnv TcLclEnv) (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
elaborateSpecType CoreExpr -> ExprBV Symbol Symbol
coreToLg CoreExpr -> TcRn CoreExpr
simplifier)
  let ts' = Symbol
-> HashSet Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
elaborateMethod (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataCon
dc) ([Symbol] -> HashSet Symbol
forall 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) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
t'
  pure
    ( dcp { dcpTyArgs = zip xs (stripPred <$> ts') }
    , dcp { dcpTyArgs = fmap (\(LHName
x, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) -> (LHName
x, Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
strengthenTy (LHName -> Symbol
lhNameToResolvedSymbol LHName
x) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)) (zip xs t') }
    )
 where
  addCoherenceOblig :: SpecType -> Maybe RReft -> SpecType
  addCoherenceOblig :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> Maybe RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
addCoherenceOblig RTypeBV Symbol Symbol RTyCon RTyVar RReft
t Maybe RReft
Nothing  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  addCoherenceOblig RTypeBV Symbol Symbol RTyCon RTyVar RReft
t (Just RReft
r) = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
rrep
    { ty_res = res `RT.strengthen` r
    }
   where
    rrep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
rrep = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
    res :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
res  = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res RTypeRepBV Symbol 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 ([RTypeBV Symbol Symbol RTyCon RTyVar RReft] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
fts)
      ([Maybe RReft] -> [Maybe RReft]) -> [Maybe RReft] -> [Maybe RReft]
forall a b. (a -> b) -> a -> b
$  ([ReftBV Symbol Symbol] -> Maybe RReft)
-> [[ReftBV Symbol 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)
-> ([ReftBV Symbol Symbol] -> RReft)
-> [ReftBV Symbol Symbol]
-> Maybe RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft)
-> PredicateBV Symbol Symbol -> ReftBV Symbol Symbol -> RReft
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft PredicateBV Symbol Symbol
forall a. Monoid a => a
mempty (ReftBV Symbol Symbol -> RReft)
-> ([ReftBV Symbol Symbol] -> ReftBV Symbol Symbol)
-> [ReftBV Symbol Symbol]
-> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ReftBV Symbol Symbol] -> ReftBV Symbol Symbol
forall a. Monoid a => [a] -> a
mconcat) [[ReftBV Symbol 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 :: [[ReftBV Symbol Symbol]]
preftss = (([([Var], [Var])] -> [ReftBV Symbol Symbol])
-> [[([Var], [Var])]] -> [[ReftBV Symbol Symbol]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([([Var], [Var])] -> [ReftBV Symbol Symbol])
 -> [[([Var], [Var])]] -> [[ReftBV Symbol Symbol]])
-> ((([Var], [Var]) -> ReftBV Symbol Symbol)
    -> [([Var], [Var])] -> [ReftBV Symbol Symbol])
-> (([Var], [Var]) -> ReftBV Symbol Symbol)
-> [[([Var], [Var])]]
-> [[ReftBV Symbol Symbol]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Var], [Var]) -> ReftBV Symbol Symbol)
-> [([Var], [Var])] -> [ReftBV Symbol Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (([Var] -> [Var] -> ReftBV Symbol Symbol)
-> ([Var], [Var]) -> ReftBV Symbol Symbol
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Symbol -> [Var] -> [Var] -> ReftBV Symbol Symbol
forall s. Symbolic s => s -> [Var] -> [Var] -> ReftBV Symbol Symbol
GM.coherenceObligToRef Symbol
recsel))
                          (Class -> [[([Var], [Var])]]
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 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
resTy    = DataConP -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
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, [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts) = [(LHName, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> ([LHName], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
forall a b. [(a, b)] -> ([a], [b])
unzip (DataConP -> [(LHName, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
dcpTyArgs DataConP
dcp)
  fts :: [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
fts      = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
fullTy (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
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 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
stripPred = ([(SpecRTVar, RReft)], [PVar RSort],
 [(RTyCon, [RTypeBV Symbol Symbol RTyCon RTyVar RReft])],
 RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall t t1 t2 t3. (t, t1, t2, t3) -> t3
Misc.fourth4 (([(SpecRTVar, RReft)], [PVar RSort],
  [(RTyCon, [RTypeBV Symbol Symbol RTyCon RTyVar RReft])],
  RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> ([(SpecRTVar, RReft)], [PVar RSort],
        [(RTyCon, [RTypeBV Symbol Symbol RTyCon RTyVar RReft])],
        RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([(SpecRTVar, RReft)], [PVar RSort],
    [(RTyCon, [RTypeBV Symbol Symbol RTyCon RTyVar RReft])],
    RTypeBV Symbol Symbol RTyCon RTyVar RReft)
bkUnivClass
  fullTy :: SpecType -> SpecType
  fullTy :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
fullTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t = [(SpecRTVar, RReft)]
-> [PVar RSort]
-> [(Symbol, RFInfo, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
     RReft)]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall tv b v c r.
[(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> [(b, RFInfo, RTypeBV b v c tv r, r)]
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
mkArrow
    [(SpecRTVar, RReft)]
forall {s}. [(RTVar RTyVar s, RReft)]
tvars
    []
    [ ( Symbol
recsel{- F.symbol dc-}
      , Bool -> RFInfo
classRFInfo Bool
True
      , RTypeBV Symbol Symbol RTyCon RTyVar RReft
resTy
      , RReft
forall a. Monoid a => a
mempty
      )
    ]
    RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  -- YL: is this redundant if we already have strengthenClassSel?
  strengthenTy :: F.Symbol -> SpecType -> SpecType
  strengthenTy :: Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
strengthenTy Symbol
x RTypeBV Symbol Symbol RTyCon RTyVar RReft
t = [(SpecRTVar, RReft)]
-> [PVar RSort]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall (t :: * -> *) (t1 :: * -> *) tv b v c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RTypeBV b v c tv (NoReftB b)), r)
-> t1 (PVarBV b v (RTypeBV b v c tv (NoReftB b)))
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
mkUnivs [(SpecRTVar, RReft)]
tvs [PVar RSort]
pvs (Symbol
-> RFInfo
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
z RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
clas (RTypeBV Symbol Symbol RTyCon RTyVar RReft
t' RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`RT.strengthen` RReft
mt) RReft
r)
   where
    ([(SpecRTVar, RReft)]
tvs, [PVar RSort]
pvs, RFun Symbol
z RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
clas RTypeBV Symbol Symbol RTyCon RTyVar RReft
t' RReft
r) = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([(SpecRTVar, RReft)], [PVar RSort],
    RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall b v tv c r.
RTypeBV b v tv c r
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkUniv RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
    vv :: ReftBind RReft
vv = RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ReftBind RReft
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBind r
rTypeValueVar RTypeBV Symbol Symbol RTyCon RTyVar RReft
t'
    mt :: RReft
mt = (Symbol, ExprBV Symbol Symbol) -> RReft
RT.uReft (Symbol
vv, Brel
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. Brel -> ExprBV b v -> ExprBV b v -> ExprBV b v
F.PAtom Brel
F.Eq (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
vv) (ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.EApp (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
x) (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
z)))


elaborateMethod :: F.Symbol -> S.HashSet F.Symbol -> SpecType -> SpecType
elaborateMethod :: Symbol
-> HashSet Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
elaborateMethod Symbol
dc HashSet Symbol
methods RTypeBV Symbol Symbol RTyCon RTyVar RReft
st = (Symbol -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv.
(b -> ExprBV b v -> ExprBV b v)
-> RTypeBV b v c tv (RReftBV b v) -> RTypeBV b v c tv (RReftBV b v)
mapExprReft
  (\Symbol
_ -> Symbol
-> Symbol
-> HashSet Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
substClassOpBinding Symbol
tcbindSym Symbol
dc HashSet Symbol
methods)
  RTypeBV Symbol Symbol RTyCon RTyVar RReft
st
 where
  tcbindSym :: Symbol
tcbindSym = RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Symbol
grabtcbind RTypeBV Symbol Symbol RTyCon RTyVar RReft
st
  grabtcbind :: SpecType -> F.Symbol
  grabtcbind :: RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Symbol
grabtcbind RTypeBV Symbol Symbol RTyCon RTyVar RReft
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], [RTypeBV Symbol Symbol RTyCon RTyVar RReft],
 [RReft])
-> [Symbol]
forall t t1 t2 t3. (t, t1, t2, t3) -> t
Misc.fst4 (([Symbol], [RFInfo], [RTypeBV Symbol Symbol RTyCon RTyVar RReft],
  [RReft])
 -> [Symbol])
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> ([Symbol], [RFInfo],
        [RTypeBV Symbol Symbol RTyCon RTyVar RReft], [RReft]))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Symbol], [RFInfo], [RTypeBV Symbol Symbol RTyCon RTyVar RReft],
  [RReft]),
 RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> ([Symbol], [RFInfo],
    [RTypeBV Symbol Symbol RTyCon RTyVar RReft], [RReft])
forall a b. (a, b) -> a
fst ((([Symbol], [RFInfo], [RTypeBV Symbol Symbol RTyCon RTyVar RReft],
   [RReft]),
  RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> ([Symbol], [RFInfo],
     [RTypeBV Symbol Symbol RTyCon RTyVar RReft], [RReft]))
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> (([Symbol], [RFInfo],
         [RTypeBV Symbol Symbol RTyCon RTyVar RReft], [RReft]),
        RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([Symbol], [RFInfo],
    [RTypeBV Symbol Symbol RTyCon RTyVar RReft], [RReft])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> (([Symbol], [RFInfo],
     [RTypeBV Symbol Symbol RTyCon RTyVar RReft], [RReft]),
    RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall b v t t1 a.
RTypeBV b v t t1 a
-> (([b], [RFInfo], [RTypeBV b v t t1 a], [a]), RTypeBV b v t t1 a)
bkArrow (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> (([Symbol], [RFInfo],
      [RTypeBV Symbol Symbol RTyCon RTyVar RReft], [RReft]),
     RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> (([Symbol], [RFInfo],
     [RTypeBV Symbol Symbol RTyCon RTyVar RReft], [RReft]),
    RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(SpecRTVar, RReft)], [PVar RSort],
 RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b c. (a, b, c) -> c
Misc.thd3 (([(SpecRTVar, RReft)], [PVar RSort],
  RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> ([(SpecRTVar, RReft)], [PVar RSort],
        RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([(SpecRTVar, RReft)], [PVar RSort],
    RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall b v tv c r.
RTypeBV b v tv c r
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkUniv (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol])
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol]
forall a b. (a -> b) -> a -> b
$ RTypeBV Symbol Symbol RTyCon RTyVar RReft
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]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp RTypeBV Symbol Symbol RTyCon RTyVar RReft
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
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
substClassOpBinding Symbol
tcbind Symbol
dc HashSet Symbol
methods = ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go
 where
  go :: F.Expr -> F.Expr
  go :: ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go (F.EApp ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1)
    | F.EVar Symbol
x <- ExprBV Symbol Symbol
e0, F.EVar Symbol
y <- ExprBV Symbol Symbol
e1, Symbol
y Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
tcbind, Symbol -> HashSet Symbol -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member Symbol
x HashSet Symbol
methods = Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar
      (Symbol
x Symbol -> Symbol -> Symbol
`F.suffixSymbol` Symbol
dc)
    | Bool
otherwise = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.EApp (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1)
  go (F.ENeg ExprBV Symbol Symbol
e          ) = ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v
F.ENeg (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e)
  go (F.EBin Bop
bop ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1  ) = Bop
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. Bop -> ExprBV b v -> ExprBV b v -> ExprBV b v
F.EBin Bop
bop (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1)
  go (F.EIte ExprBV Symbol Symbol
e0  ExprBV Symbol Symbol
e1 ExprBV Symbol Symbol
e2  ) = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v -> ExprBV b v
F.EIte (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e2)
  go (F.ECst ExprBV Symbol Symbol
e0     Sort
s   ) = ExprBV Symbol Symbol -> Sort -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> Sort -> ExprBV b v
F.ECst (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) Sort
s
  go (F.ELam (Symbol
x, Sort
t) ExprBV Symbol Symbol
body) = (Symbol, Sort) -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. (b, Sort) -> ExprBV b v -> ExprBV b v
F.ELam (Symbol
x, Sort
t) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
body)
  go (F.PAnd [ExprBV Symbol Symbol]
es         ) = [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. [ExprBV b v] -> ExprBV b v
F.PAnd (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> [ExprBV Symbol Symbol] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
es)
  go (F.POr  [ExprBV Symbol Symbol]
es         ) = [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. [ExprBV b v] -> ExprBV b v
F.POr (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> [ExprBV Symbol Symbol] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
es)
  go (F.PNot ExprBV Symbol Symbol
e          ) = ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v
F.PNot (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e)
  go (F.PImp ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1      ) = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.PImp (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1)
  go (F.PIff ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1      ) = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.PIff (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1)
  go (F.PAtom Brel
brel ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1) = Brel
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. Brel -> ExprBV b v -> ExprBV b v -> ExprBV b v
F.PAtom Brel
brel (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1)
  -- a catch-all binding is not a good idea
  go ExprBV Symbol Symbol
e                    = ExprBV Symbol 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 b v c tv r. tv -> r -> RTypeBV b 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 b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b 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 (RTypeBV Symbol Symbol c tv (NoReftB Symbol))
info) RType c tv r
tres r
r <- RType c tv r
t
  = RTVar tv (RTypeBV Symbol Symbol c tv (NoReftB Symbol))
-> RType c tv r -> r -> RType c tv r
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT (tv
-> RTVInfo (RTypeBV Symbol Symbol c tv (NoReftB Symbol))
-> RTVar tv (RTypeBV Symbol Symbol c tv (NoReftB Symbol))
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar (tv -> tv
rename tv
tv) RTVInfo (RTypeBV Symbol Symbol c tv (NoReftB Symbol))
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 PVUBV Symbol Symbol c tv
b RType c tv r
tres <- RType c tv r
t
  = PVUBV Symbol Symbol c tv -> RType c tv r -> RType c tv r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP ((tv -> tv)
-> RTypeBV Symbol Symbol c tv (NoReftB Symbol)
-> RTypeBV Symbol Symbol c tv (NoReftB Symbol)
forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename (RTypeBV Symbol Symbol c tv (NoReftB Symbol)
 -> RTypeBV Symbol Symbol c tv (NoReftB Symbol))
-> PVUBV Symbol Symbol c tv -> PVUBV Symbol Symbol c tv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVUBV Symbol 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 [RTPropBV Symbol Symbol c tv r]
tps r
r <- RType c tv r
t
  -- TODO: handle rtprop properly
  = c
-> [RType c tv r]
-> [RTPropBV Symbol Symbol c tv r]
-> r
-> RType c tv r
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b 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) [RTPropBV Symbol 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 b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b 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 b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b 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 (ExprBV Symbol 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 b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b 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 b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b 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 :: (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> [Located DataConP]
-> [(ClsInst, [Var])]
-> TcRn [(Var, LocSpecType)]
makeClassAuxTypes RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> IOEnv
     (Env TcGblEnv TcLclEnv) (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
elab [Located DataConP]
dcps [(ClsInst, [Var])]
xs = ((Located DataConP, ClsInst, [Var]) -> TcRn [(Var, LocSpecType)])
-> [(Located DataConP, ClsInst, [Var])]
-> TcRn [(Var, LocSpecType)]
forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(a -> m [b]) -> t a -> m [b]
Misc.concatMapM ((RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> (Located DataConP, ClsInst, [Var]) -> TcRn [(Var, LocSpecType)]
makeClassAuxTypesOne RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> IOEnv
     (Env TcGblEnv TcLclEnv) (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
elab) [(Located DataConP, ClsInst, [Var])]
dcpInstMethods
  where
    dcpInstMethods :: [(Located DataConP, ClsInst, [Var])]
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 :: (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> (Located DataConP, ClsInst, [Var]) -> TcRn [(Var, LocSpecType)]
makeClassAuxTypesOne RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> IOEnv
     (Env TcGblEnv TcLclEnv) (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
elab (Located DataConP
ldcp, ClsInst
inst, [Var]
methods) =
  [Var]
-> (Var -> IOEnv (Env TcGblEnv TcLclEnv) (Var, LocSpecType))
-> TcRn [(Var, LocSpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Var]
methods ((Var -> IOEnv (Env TcGblEnv TcLclEnv) (Var, LocSpecType))
 -> TcRn [(Var, LocSpecType)])
-> (Var -> IOEnv (Env TcGblEnv TcLclEnv) (Var, LocSpecType))
-> TcRn [(Var, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ \Var
method -> do
    let (RTypeBV Symbol Symbol RTyCon RTyVar RReft
headlessSig, Maybe RReft
preft) =
          case Symbol
-> [(Symbol,
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft, Maybe RReft))]
-> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft, Maybe RReft)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup (Var -> Symbol
mkSymbol Var
method) [(Symbol,
  (RTypeBV Symbol Symbol RTyCon RTyVar RReft, Maybe RReft))]
yts' of
            Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft, Maybe RReft)
Nothing ->
              Maybe SrcSpan
-> [Char]
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft, 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 (Var -> Symbol
mkSymbol Var
method) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)] -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
yts)
            Just (RTypeBV Symbol Symbol RTyCon RTyVar RReft, Maybe RReft)
sig -> (RTypeBV Symbol Symbol RTyCon RTyVar RReft, Maybe RReft)
sig
        -- dict binder will never be changed because we optimized PAnd[]
        -- lq0 lq1 ...
            --
        ptys :: [(Symbol, RFInfo, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
  RReft)]
ptys    = [(Maybe Integer -> Symbol
F.vv (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i), Bool -> RFInfo
classRFInfo Bool
True, RTypeBV Symbol Symbol RTyCon RTyVar RReft
pty, RReft
forall a. Monoid a => a
mempty) | (Integer
i,RTypeBV Symbol Symbol RTyCon RTyVar RReft
pty) <- [Integer]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [(Integer, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0,Integer
1..] [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
isPredSpecTys]
        fullSig :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
fullSig =
          [(SpecRTVar, RReft)]
-> [PVar RSort]
-> [(Symbol, RFInfo, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
     RReft)]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall tv b v c r.
[(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> [(b, RFInfo, RTypeBV b v c tv r, r)]
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
mkArrow
            [(SpecRTVar
bRTV, RReft
forall a. Monoid a => a
mempty) | SpecRTVar
bRTV <- [SpecRTVar]
forall {s}. [RTVar RTyVar s]
isRTvs]
            []
            [(Symbol, RFInfo, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
  RReft)]
ptys (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          [(RTyVar, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall {r} {c} {tv} {b} {v}.
(IsReft r, TyConable c, FreeVar c tv,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b))),
 Binder b, Hashable tv) =>
[(tv, RTypeBV b v c tv r)]
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
subst ([RTyVar]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [(RTyVar, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RTyVar]
clsTvs [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
isSpecTys) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$
          RTypeBV Symbol Symbol RTyCon RTyVar RReft
headlessSig
    elaboratedSig  <- (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> Maybe RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> Maybe RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b c. (a -> b -> c) -> b -> a -> c
flip RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> Maybe RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
addCoherenceOblig Maybe RReft
preft (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> IOEnv
     (Env TcGblEnv TcLclEnv) (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> IOEnv
     (Env TcGblEnv TcLclEnv) (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
elab RTypeBV Symbol Symbol RTyCon RTyVar RReft
fullSig

    let retSig =  (Symbol -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv.
(b -> ExprBV b v -> ExprBV b v)
-> RTypeBV b v c tv (RReftBV b v) -> RTypeBV b v c tv (RReftBV b v)
mapExprReft (\Symbol
_ -> Symbol
-> HashMap Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
substAuxMethod Symbol
dfunSym HashMap Symbol Symbol
methodsSet) ([Char]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"elaborated" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr Var
method) RTypeBV Symbol Symbol RTyCon RTyVar RReft
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. 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
$ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [RTyVar]
forall tv c r. Eq tv => RType c tv r -> [tv]
RT.allTyVars' ([Char]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"new-type" RTypeBV Symbol Symbol RTyCon RTyVar RReft
retSig)) ([Char] -> [RTyVar] -> [RTyVar]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"ghc-type-vars" (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [RTyVar]
forall tv c r. Eq tv => RType c tv r -> [tv]
RT.allTyVars' (([Char]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"ghc-type" (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Type -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r. IsReft r => Type -> RRType r
RT.ofType (Var -> Type
Ghc.varType Var
method)) :: SpecType)))
        cosub  = [(Symbol, Sort)] -> HashMap Symbol Sort
forall k v. 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 (Var -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol Var
b)) |  (RTyVar
a,RTV Var
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. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault RTyVar
x RTyVar
x HashMap RTyVar RTyVar
tysub
        subbedTy = (RReft -> RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r1 r2 b v c tv.
(r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft (HashMap Symbol Sort -> RReft -> RReft
Bare.coSubRReft HashMap Symbol Sort
cosub) ((RTyVar -> RTyVar)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs RTyVar -> RTyVar
tysubf RTypeBV Symbol Symbol RTyCon RTyVar RReft
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)
    ([Var]
_,[Type]
predTys,Class
_,[Type]
_) = ClsInst -> ([Var], [Type], Class, [Type])
Ghc.instanceSig ClsInst
inst
    dfunApped :: ExprBV Symbol Symbol
dfunApped = LocSymbol -> [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall v b. Located v -> [ExprBV b v] -> ExprBV b v
F.mkEApp LocSymbol
dfunSymL [Symbol -> ExprBV Symbol Symbol
forall a. Symbolic a => a -> ExprBV Symbol Symbol
F.eVar (Symbol -> ExprBV Symbol Symbol) -> Symbol -> ExprBV Symbol 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, RTypeBV Symbol Symbol RTyCon RTyVar RReft)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
yts) ([Maybe RReft] -> [Maybe RReft]) -> [Maybe RReft] -> [Maybe RReft]
forall a b. (a -> b) -> a -> b
$ ([ReftBV Symbol Symbol] -> Maybe RReft)
-> [[ReftBV Symbol 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)
-> ([ReftBV Symbol Symbol] -> Maybe RReft)
-> [ReftBV Symbol 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)
-> ([ReftBV Symbol Symbol] -> RReft)
-> [ReftBV Symbol Symbol]
-> Maybe RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft)
-> PredicateBV Symbol Symbol -> ReftBV Symbol Symbol -> RReft
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft PredicateBV Symbol Symbol
forall a. Monoid a => a
mempty (ReftBV Symbol Symbol -> RReft)
-> ([ReftBV Symbol Symbol] -> ReftBV Symbol Symbol)
-> [ReftBV Symbol Symbol]
-> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ReftBV Symbol Symbol] -> ReftBV Symbol Symbol
forall a. Monoid a => [a] -> a
mconcat) [[ReftBV Symbol 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 :: [[ReftBV Symbol Symbol]]
preftss = [Char] -> [[ReftBV Symbol Symbol]] -> [[ReftBV Symbol Symbol]]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"preftss" ([[ReftBV Symbol Symbol]] -> [[ReftBV Symbol Symbol]])
-> [[ReftBV Symbol Symbol]] -> [[ReftBV Symbol Symbol]]
forall a b. (a -> b) -> a -> b
$ (([([Var], [Var])] -> [ReftBV Symbol Symbol])
-> [[([Var], [Var])]] -> [[ReftBV Symbol Symbol]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap(([([Var], [Var])] -> [ReftBV Symbol Symbol])
 -> [[([Var], [Var])]] -> [[ReftBV Symbol Symbol]])
-> ((([Var], [Var]) -> ReftBV Symbol Symbol)
    -> [([Var], [Var])] -> [ReftBV Symbol Symbol])
-> (([Var], [Var]) -> ReftBV Symbol Symbol)
-> [[([Var], [Var])]]
-> [[ReftBV Symbol Symbol]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(([Var], [Var]) -> ReftBV Symbol Symbol)
-> [([Var], [Var])] -> [ReftBV Symbol Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (([Var] -> [Var] -> ReftBV Symbol Symbol)
-> ([Var], [Var]) -> ReftBV Symbol Symbol
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprBV Symbol Symbol -> [Var] -> [Var] -> ReftBV Symbol Symbol
GM.coherenceObligToRefE ExprBV Symbol Symbol
dfunApped)) (Class -> [[([Var], [Var])]]
GM.buildCoherenceOblig Class
cls)
    yts' :: [(Symbol,
  (RTypeBV Symbol Symbol RTyCon RTyVar RReft, Maybe RReft))]
yts' = [Symbol]
-> [(RTypeBV Symbol Symbol RTyCon RTyVar RReft, Maybe RReft)]
-> [(Symbol,
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft, Maybe RReft))]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft) -> Symbol)
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
yts) ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [Maybe RReft]
-> [(RTypeBV Symbol Symbol RTyCon RTyVar RReft, Maybe RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a, b) -> b
snd ((Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
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 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> Maybe RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
addCoherenceOblig RTypeBV Symbol Symbol RTyCon RTyVar RReft
t Maybe RReft
Nothing = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
    addCoherenceOblig RTypeBV Symbol Symbol RTyCon RTyVar RReft
t (Just RReft
r) = [Char]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"SCSel" (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
    -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
rrep {ty_res = res `RT.strengthen` r}
      where rrep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
rrep = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
            res :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
res  = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res RTypeRepBV Symbol 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. Hashable k => [(k, v)] -> HashMap k v
M.fromList ([Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
clsMethods) (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
methods))
    -- core rewriting mark1: dfunId
    -- ()
    dfunSymL :: LocSymbol
dfunSymL = Var -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol (Var -> LocSymbol) -> Var -> LocSymbol
forall a b. (a -> b) -> a -> b
$ ClsInst -> Var
Ghc.instanceDFunId ClsInst
inst
    dfunSym :: Symbol
dfunSym = LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
dfunSymL
    ([Var]
isTvs, [Type]
isPredTys, Class
_, [Type]
isTys) = ClsInst -> ([Var], [Type], Class, [Type])
Ghc.instanceSig ClsInst
inst
    isSpecTys :: [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
isSpecTys = Type -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r. IsReft r => Type -> RRType r
RT.ofType (Type -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> [Type] -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
isTys
    isPredSpecTys :: [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
isPredSpecTys = Type -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r. IsReft r => Type -> RRType r
RT.ofType (Type -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> [Type] -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
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)
-> (Var -> RTyVar) -> Var -> RTVar RTyVar s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> RTyVar
RT.rTyVar (Var -> RTVar RTyVar s) -> [Var] -> [RTVar RTyVar s]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
isTvs
    dcp :: DataConP
dcp = Located DataConP -> DataConP
forall a. Located a -> a
F.val Located DataConP
ldcp
    -- Monoid.mappend, ...
    clsMethods :: [Var]
clsMethods = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Var
x -> Symbol -> Symbol
GM.dropModuleNames (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Var -> Symbol) -> [Var] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var -> Symbol
mkSymbol [Var]
methods) ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$
      Class -> [Var]
Ghc.classAllSelIds (ClsInst -> Class
Ghc.is_cls ClsInst
inst)
    yts :: [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
yts = [(LHName -> Symbol
lhNameToResolvedSymbol LHName
y, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) | (LHName
y, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) <- DataConP -> [(LHName, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
dcpTyArgs DataConP
dcp]
    mkSymbol :: Var -> Symbol
mkSymbol Var
x
      | -- F.notracepp ("isDictonaryId:" ++ GM.showPpr x) $
        Var -> Bool
Ghc.isDictonaryId Var
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
$ Var -> Symbol
forall t. NamedThing t => t -> Symbol
GM.simplesymbol Var
x)
      | Bool
otherwise = Int -> Symbol -> Symbol
F.dropSym Int
2 (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall t. NamedThing t => t -> Symbol
GM.simplesymbol Var
x
        -- res = dcpTyRes dcp
    clsTvs :: [RTyVar]
clsTvs = DataConP -> [RTyVar]
dcpFreeTyVars DataConP
dcp
        -- copy/pasted from Bare/Class.hs
    subst :: [(tv, RTypeBV b v c tv r)]
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
subst [] RTypeBV b v c tv r
t = RTypeBV b v c tv r
t
    subst ((tv
a, RTypeBV b v c tv r
ta):[(tv, RTypeBV b v c tv r)]
su) RTypeBV b v c tv r
t = (tv, RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
forall tv r c b v.
(Eq tv, Hashable tv, IsReft r, TyConable c, Binder b,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b)))) =>
(tv, RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
RT.subsTyVarMeet' (tv
a, RTypeBV b v c tv r
ta) ([(tv, RTypeBV b v c tv r)]
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
subst [(tv, RTypeBV b v c tv r)]
su RTypeBV b v c tv r
t)

substAuxMethod :: F.Symbol -> M.HashMap F.Symbol F.Symbol -> F.Expr -> F.Expr
substAuxMethod :: Symbol
-> HashMap Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
substAuxMethod Symbol
dfun HashMap Symbol Symbol
methods = [Char] -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"substAuxMethod" (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go
  where go :: F.Expr -> F.Expr
        go :: ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go (F.EApp ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1)
          | F.EVar Symbol
x <- [Char] -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"e0" ExprBV Symbol Symbol
e0
          , (F.EVar Symbol
dfun_mb, [ExprBV Symbol Symbol]
args)  <- ExprBV Symbol Symbol
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
forall b v. ExprBV b v -> (ExprBV b v, [ExprBV b v])
F.splitEApp ExprBV Symbol 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. 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)
           = ExprBV Symbol Symbol
-> [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> [ExprBV b v] -> ExprBV b v
F.eApps (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
method) [ExprBV Symbol Symbol]
args
          | Bool
otherwise
          = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.EApp (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1)
        go (F.ENeg ExprBV Symbol Symbol
e) = ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v
F.ENeg (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e)
        go (F.EBin Bop
bop ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1) = Bop
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. Bop -> ExprBV b v -> ExprBV b v -> ExprBV b v
F.EBin Bop
bop (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1)
        go (F.EIte ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1 ExprBV Symbol Symbol
e2) = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v -> ExprBV b v
F.EIte (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e2)
        go (F.ECst ExprBV Symbol Symbol
e0 Sort
s) = ExprBV Symbol Symbol -> Sort -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> Sort -> ExprBV b v
F.ECst (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) Sort
s
        go (F.ELam (Symbol
x, Sort
t) ExprBV Symbol Symbol
body) = (Symbol, Sort) -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. (b, Sort) -> ExprBV b v -> ExprBV b v
F.ELam (Symbol
x, Sort
t) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
body)
        go (F.PAnd [ExprBV Symbol Symbol]
es) = [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. [ExprBV b v] -> ExprBV b v
F.PAnd (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> [ExprBV Symbol Symbol] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
es)
        go (F.POr [ExprBV Symbol Symbol]
es) = [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. [ExprBV b v] -> ExprBV b v
F.POr (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> [ExprBV Symbol Symbol] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
es)
        go (F.PNot ExprBV Symbol Symbol
e) = ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v
F.PNot (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e)
        go (F.PImp ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1) = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.PImp (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1)
        go (F.PIff ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1) = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.PIff (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1)
        go (F.PAtom Brel
brel ExprBV Symbol Symbol
e0 ExprBV Symbol Symbol
e1) = Brel
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. Brel -> ExprBV b v -> ExprBV b v -> ExprBV b v
F.PAtom Brel
brel (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e0) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1)
        go ExprBV Symbol Symbol
e = [Char] -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"LEAF" ExprBV Symbol Symbol
e