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

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

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

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

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



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

  mkSymbol :: DFunId -> Symbol
mkSymbol DFunId
x
    | DFunId -> Bool
Ghc.isDictonaryId DFunId
x = Symbol -> Symbol -> Symbol
F.mappendSym Symbol
"$" (Int -> Symbol -> Symbol
F.dropSym Int
2 (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 ((() :: Constraint) => 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 ty bndr. Spec ty bndr -> [DataDecl]
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 =
    Env -> ModName -> [Char] -> LocSymbol -> Maybe TyCon
forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env
                         ModName
name
                         [Char]
"resolveClassMaybe"
                         (DataName -> LocSymbol
dataNameSymbol (DataName -> LocSymbol)
-> (DataDecl -> DataName) -> DataDecl -> LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> DataName
tycName (DataDecl -> LocSymbol) -> DataDecl -> LocSymbol
forall a b. (a -> b) -> a -> b
$ 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, LocBareType)])] -> [DataDecl]
makeClassDataDecl = ((Class, [(DFunId, LocBareType)]) -> DataDecl)
-> [(Class, [(DFunId, LocBareType)])] -> [DataDecl]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Class -> [(DFunId, LocBareType)] -> DataDecl)
-> (Class, [(DFunId, LocBareType)]) -> DataDecl
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Class -> [(DFunId, LocBareType)] -> DataDecl
classDeclToDataDecl)

-- TODO: I should have the knowledge to construct DataConP manually than
-- following the rather unwieldy pipeline: Resolved -> Unresolved -> Resolved.
-- maybe this should be fixed right after the GHC API refactoring?
classDeclToDataDecl :: Ghc.Class -> [(Ghc.Id, LocBareType)] -> DataDecl
classDeclToDataDecl :: Class -> [(DFunId, LocBareType)] -> DataDecl
classDeclToDataDecl Class
cls [(DFunId, LocBareType)]
refinedIds = DataDecl
  { tycName :: DataName
tycName   = LocSymbol -> DataName
DnName (Class -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Class -> Symbol) -> Located Class -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Class -> Located Class
forall a. NamedThing a => a -> Located a
GM.locNamedThing Class
cls)
  , tycTyVars :: [Symbol]
tycTyVars = [Symbol]
tyVars
  , tycPVars :: [PVar BSort]
tycPVars  = []
  , tycDCons :: Maybe [DataCtor]
tycDCons  = [DataCtor] -> Maybe [DataCtor]
forall a. a -> Maybe a
Just [DataCtor
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 SizeFun
tycSFun   = Maybe SizeFun
forall a. Maybe a
Nothing
  , tycPropTy :: Maybe BareType
tycPropTy = Maybe BareType
forall a. Maybe a
Nothing
  , tycKind :: DataDeclKind
tycKind   = DataDeclKind
DataUser
  }
 where
  dctor :: DataCtor
dctor = [Char] -> DataCtor -> DataCtor
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"classDeclToDataDecl" DataCtor { dcName :: LocSymbol
dcName   = Symbol -> LocSymbol
forall a. a -> Located a
F.dummyLoc (Symbol -> LocSymbol) -> Symbol -> LocSymbol
forall a b. (a -> b) -> a -> b
$ 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 :: [(Symbol, BareType)]
dcFields = [(Symbol, BareType)]
fields
                   , dcResult :: Maybe BareType
dcResult = Maybe BareType
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 :: [(Symbol, BareType)]
fields = (DFunId -> (Symbol, BareType)) -> [DFunId] -> [(Symbol, BareType)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DFunId -> (Symbol, BareType)
attachRef [DFunId]
classIds
  attachRef :: DFunId -> (Symbol, BareType)
attachRef DFunId
sid
    | Just LocBareType
ref <- DFunId -> [(DFunId, LocBareType)] -> Maybe LocBareType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup DFunId
sid [(DFunId, LocBareType)]
refinedIds
    = (DFunId -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DFunId
sid, [(Symbol, Symbol)] -> BareType -> BareType
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
RT.subts [(Symbol, Symbol)]
tyVarSubst (LocBareType -> BareType
forall a. Located a -> a
F.val LocBareType
ref))
    | Bool
otherwise
    = (DFunId -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DFunId
sid, Type -> BareType
forall r. Monoid r => Type -> BRType r
RT.bareOfType (Type -> BareType) -> (DFunId -> Type) -> DFunId -> BareType
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 -> BareType) -> DFunId -> BareType
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 -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> DataConP
-> TcRn (DataConP, DataConP)
elaborateClassDcp CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier DataConP
dcp = do
  [SpecType]
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 -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> SpecType
-> IOEnv (Env TcGblEnv TcLclEnv) SpecType
elaborateSpecType CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier)
  let ts' :: [SpecType]
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]
xs) (SpecType -> SpecType) -> [SpecType] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
t'
  (DataConP, DataConP) -> TcRn (DataConP, DataConP)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( DataConP
dcp { dcpTyArgs = zip xs (stripPred <$> ts') }
    , DataConP
dcp { dcpTyArgs = fmap (\(Symbol
x, SpecType
t) -> (Symbol
x, Symbol -> SpecType -> SpecType
strengthenTy Symbol
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) = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep RTypeRep RTyCon RTyVar RReft
rrep
    { ty_res = res `RT.strengthen` r
    }
   where
    rrep :: RTypeRep RTyCon RTyVar RReft
rrep = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t
    res :: SpecType
res  = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep 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
$  ([Reft] -> Maybe RReft) -> [[Reft]] -> [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)
-> ([Reft] -> RReft) -> [Reft] -> Maybe RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reft -> Predicate -> RReft) -> Predicate -> Reft -> RReft
forall a b c. (a -> b -> c) -> b -> a -> c
flip Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft Predicate
forall a. Monoid a => a
mempty (Reft -> RReft) -> ([Reft] -> Reft) -> [Reft] -> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Reft] -> Reft
forall a. Monoid a => [a] -> a
mconcat) [[Reft]]
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 :: [[Reft]]
preftss = (([([DFunId], [DFunId])] -> [Reft])
-> [[([DFunId], [DFunId])]] -> [[Reft]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([([DFunId], [DFunId])] -> [Reft])
 -> [[([DFunId], [DFunId])]] -> [[Reft]])
-> ((([DFunId], [DFunId]) -> Reft)
    -> [([DFunId], [DFunId])] -> [Reft])
-> (([DFunId], [DFunId]) -> Reft)
-> [[([DFunId], [DFunId])]]
-> [[Reft]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([DFunId], [DFunId]) -> Reft) -> [([DFunId], [DFunId])] -> [Reft]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (([DFunId] -> [DFunId] -> Reft) -> ([DFunId], [DFunId]) -> Reft
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Symbol -> [DFunId] -> [DFunId] -> Reft
forall s. Symbolic s => s -> [DFunId] -> [DFunId] -> Reft
GM.coherenceObligToRef Symbol
recsel))
                          (Class -> [[([DFunId], [DFunId])]]
GM.buildCoherenceOblig Class
cls)

  -- ugly, should have passed cls as an argument
  cls :: Class
cls      = 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
  ([Symbol]
xs, [SpecType]
ts) = [(Symbol, SpecType)] -> ([Symbol], [SpecType])
forall a b. [(a, b)] -> ([a], [b])
unzip (DataConP -> [(Symbol, 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 c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow
    [(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 c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RType c tv ()), r)
-> t1 (PVar (RType c tv ())) -> RType c tv r -> RType c tv r
mkUnivs [(SpecRTVar, RReft)]
tvs [PVar RSort]
pvs (Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
z RFInfo
i SpecType
clas (SpecType
t' SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` RReft
mt) RReft
r)
   where
    ([(SpecRTVar, RReft)]
tvs, [PVar RSort]
pvs, RFun Symbol
z RFInfo
i SpecType
clas SpecType
t' RReft
r) = SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], SpecType)
forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv SpecType
t
    vv :: Symbol
vv = SpecType -> Symbol
forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar SpecType
t'
    mt :: RReft
mt = (Symbol, Expr) -> RReft
RT.uReft (Symbol
vv, Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Eq (Symbol -> Expr
F.EVar Symbol
vv) (Expr -> Expr -> Expr
F.EApp (Symbol -> Expr
F.EVar Symbol
x) (Symbol -> Expr
F.EVar Symbol
z)))


elaborateMethod :: F.Symbol -> S.HashSet F.Symbol -> SpecType -> SpecType
elaborateMethod :: Symbol -> HashSet Symbol -> SpecType -> SpecType
elaborateMethod Symbol
dc HashSet Symbol
methods SpecType
st = (Symbol -> Expr -> Expr) -> SpecType -> SpecType
forall c tv.
(Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
mapExprReft
  (\Symbol
_ -> Symbol -> Symbol -> HashSet Symbol -> Expr -> Expr
substClassOpBinding Symbol
tcbindSym Symbol
dc HashSet Symbol
methods)
  SpecType
st
 where
  tcbindSym :: Symbol
tcbindSym = SpecType -> Symbol
grabtcbind SpecType
st
  grabtcbind :: SpecType -> F.Symbol
  grabtcbind :: SpecType -> Symbol
grabtcbind SpecType
t =
    [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 t t1 a.
RType t t1 a
-> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType 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 tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType 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 -> Expr -> Expr
substClassOpBinding Symbol
tcbind Symbol
dc HashSet Symbol
methods = Expr -> Expr
go
 where
  go :: F.Expr -> F.Expr
  go :: Expr -> Expr
go (F.EApp Expr
e0 Expr
e1)
    | F.EVar Symbol
x <- Expr
e0, F.EVar Symbol
y <- Expr
e1, Symbol
y 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 -> Expr
F.EVar
      (Symbol
x Symbol -> Symbol -> Symbol
`F.suffixSymbol` Symbol
dc)
    | Bool
otherwise = Expr -> Expr -> Expr
F.EApp (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
  go (F.ENeg Expr
e          ) = Expr -> Expr
F.ENeg (Expr -> Expr
go Expr
e)
  go (F.EBin Bop
bop Expr
e0 Expr
e1  ) = Bop -> Expr -> Expr -> Expr
F.EBin Bop
bop (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
  go (F.EIte Expr
e0  Expr
e1 Expr
e2  ) = Expr -> Expr -> Expr -> Expr
F.EIte (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
  go (F.ECst Expr
e0     Sort
s   ) = Expr -> Sort -> Expr
F.ECst (Expr -> Expr
go Expr
e0) Sort
s
  go (F.ELam (Symbol
x, Sort
t) Expr
body) = (Symbol, Sort) -> Expr -> Expr
F.ELam (Symbol
x, Sort
t) (Expr -> Expr
go Expr
body)
  go (F.PAnd [Expr]
es         ) = [Expr] -> Expr
F.PAnd (Expr -> Expr
go (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
  go (F.POr  [Expr]
es         ) = [Expr] -> Expr
F.POr (Expr -> Expr
go (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
  go (F.PNot Expr
e          ) = Expr -> Expr
F.PNot (Expr -> Expr
go Expr
e)
  go (F.PImp Expr
e0 Expr
e1      ) = Expr -> Expr -> Expr
F.PImp (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
  go (F.PIff Expr
e0 Expr
e1      ) = Expr -> Expr -> Expr
F.PIff (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
  go (F.PAtom Brel
brel Expr
e0 Expr
e1) = Brel -> Expr -> Expr -> Expr
F.PAtom Brel
brel (Expr -> Expr
go Expr
e0) (Expr -> Expr
go Expr
e1)
  -- a catch-all binding is not a good idea
  go Expr
e                    = Expr
e


renameTvs :: (F.Symbolic tv, F.PPrint tv) => (tv -> tv) -> RType c tv r -> RType c tv r
renameTvs :: forall tv c r.
(Symbolic tv, PPrint tv) =>
(tv -> tv) -> RType c tv r -> RType c tv r
renameTvs tv -> tv
rename RType c tv r
t
  | RVar tv
tv r
r <- RType c tv r
t
  = tv -> r -> RType c tv r
forall c tv r. tv -> r -> RType c tv r
RVar (tv -> tv
rename tv
tv) r
r
  | RFun Symbol
b RFInfo
i RType c tv r
tin RType c tv r
tout r
r <- RType c tv r
t
  = Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
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 (RType c tv ())
info) RType c tv r
tres r
r <- RType c tv r
t
  = RTVar tv (RType c tv ()) -> RType c tv r -> r -> RType c tv r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (tv -> RTVInfo (RType c tv ()) -> RTVar tv (RType c tv ())
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar (tv -> tv
rename tv
tv) RTVInfo (RType 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 PVU c tv
b RType c tv r
tres <- RType c tv r
t
  = PVU c tv -> RType c tv r -> RType c tv r
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP ((tv -> tv) -> RType c tv () -> RType c tv ()
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 () -> RType c tv ()) -> PVU c tv -> PVU c tv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVU 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 [RTProp c tv r]
tps r
r <- RType c tv r
t
  -- TODO: handle rtprop properly
  = c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
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) [RTProp c tv r]
tps r
r
  | RAllE Symbol
b RType c tv r
allarg RType c tv r
ty <- RType c tv r
t
  = Symbol -> RType c tv r -> RType c tv r -> RType c tv r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
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 c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType 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 Expr
_ <- RType c tv r
t
  = RType c tv r
t
  | RAppTy RType c tv r
arg RType c tv r
res r
r <- RType c tv r
t
  = RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy ((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 c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType 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
      Located DataConP
dcp <- [Located DataConP]
dcps
      (ClsInst
inst, [DFunId]
methods) <- [(ClsInst, [DFunId])]
xs
      let dc :: DataCon
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' :: DataCon
dc' = Class -> DataCon
Ghc.classDataCon (Class -> DataCon) -> Class -> DataCon
forall a b. (a -> b) -> a -> b
$ ClsInst -> Class
Ghc.is_cls ClsInst
inst
      Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ DataCon
dc DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
dc'
      (Located DataConP, ClsInst, [DFunId])
-> [(Located DataConP, ClsInst, [DFunId])]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Located DataConP
dcp, ClsInst
inst, [DFunId]
methods)

makeClassAuxTypesOne ::
     (SpecType -> Ghc.TcRn SpecType)
  -> (F.Located DataConP, Ghc.ClsInst, [Ghc.Var])
  -> Ghc.TcRn [(Ghc.Var, LocSpecType)]
makeClassAuxTypesOne :: (SpecType -> 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 c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow
            ([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
    SpecType
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 :: SpecType
retSig =  (Symbol -> Expr -> Expr) -> SpecType -> SpecType
forall c tv.
(Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
mapExprReft (\Symbol
_ -> Symbol -> HashMap Symbol Symbol -> Expr -> Expr
substAuxMethod Symbol
dfunSym HashMap Symbol Symbol
methodsSet) ([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 :: HashMap RTyVar RTyVar
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]
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]
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
ofType (DFunId -> Type
Ghc.varType DFunId
method)) :: SpecType)))
        cosub :: HashMap Symbol Sort
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 -> RTyVar
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 :: SpecType
subbedTy = (RReft -> RReft) -> SpecType -> SpecType
forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft (HashMap Symbol Sort -> RReft -> RReft
Bare.coSubRReft HashMap Symbol Sort
cosub) ((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
    (DFunId, LocSpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) (DFunId, LocSpecType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DFunId
method, SpecType -> LocSpecType
forall a. a -> Located a
F.dummyLoc ([Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"vars:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Symbol] -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (RTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (RTyVar -> Symbol) -> [RTyVar] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> [RTyVar]
forall tv c r. Eq tv => RType c tv r -> [tv]
allTyVars' SpecType
subbedTy)) SpecType
subbedTy))

  -- "is" is used as a shorthand for instance, following the convention of the Ghc api
  where
    -- recsel = F.symbol ("lq$recsel" :: String)
    ([DFunId]
_,[Type]
predTys,Class
_,[Type]
_) = ClsInst -> ([DFunId], [Type], Class, [Type])
Ghc.instanceSig ClsInst
inst
    dfunApped :: Expr
dfunApped = LocSymbol -> [Expr] -> Expr
F.mkEApp LocSymbol
dfunSymL [Symbol -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (Symbol -> Expr) -> Symbol -> Expr
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
$ ([Reft] -> Maybe RReft) -> [[Reft]] -> [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)
-> ([Reft] -> Maybe RReft) -> [Reft] -> Maybe RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RReft -> Maybe RReft
forall a. a -> Maybe a
Just (RReft -> Maybe RReft)
-> ([Reft] -> RReft) -> [Reft] -> Maybe RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reft -> Predicate -> RReft) -> Predicate -> Reft -> RReft
forall a b c. (a -> b -> c) -> b -> a -> c
flip Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft Predicate
forall a. Monoid a => a
mempty (Reft -> RReft) -> ([Reft] -> Reft) -> [Reft] -> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Reft] -> Reft
forall a. Monoid a => [a] -> a
mconcat) [[Reft]]
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 :: [[Reft]]
preftss = [Char] -> [[Reft]] -> [[Reft]]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"preftss" ([[Reft]] -> [[Reft]]) -> [[Reft]] -> [[Reft]]
forall a b. (a -> b) -> a -> b
$ (([([DFunId], [DFunId])] -> [Reft])
-> [[([DFunId], [DFunId])]] -> [[Reft]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap(([([DFunId], [DFunId])] -> [Reft])
 -> [[([DFunId], [DFunId])]] -> [[Reft]])
-> ((([DFunId], [DFunId]) -> Reft)
    -> [([DFunId], [DFunId])] -> [Reft])
-> (([DFunId], [DFunId]) -> Reft)
-> [[([DFunId], [DFunId])]]
-> [[Reft]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(([DFunId], [DFunId]) -> Reft) -> [([DFunId], [DFunId])] -> [Reft]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (([DFunId] -> [DFunId] -> Reft) -> ([DFunId], [DFunId]) -> Reft
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Expr -> [DFunId] -> [DFunId] -> Reft
GM.coherenceObligToRefE Expr
dfunApped)) (Class -> [[([DFunId], [DFunId])]]
GM.buildCoherenceOblig Class
cls)
    yts' :: [(Symbol, (SpecType, Maybe RReft))]
yts' = [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)
-> (RTypeRep RTyCon RTyVar RReft -> SpecType)
-> RTypeRep RTyCon RTyVar RReft
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar RReft -> SpecType)
-> RTypeRep RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft
rrep {ty_res = res `strengthen` r}
      where rrep :: RTypeRep RTyCon RTyVar RReft
rrep = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t
            res :: SpecType
res  = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
rrep    -- (Monoid.mappend -> $cmappend##Int, ...)
    -- core rewriting mark2: do the same thing except they don't have to be symbols
    -- YL: poorly written. use a comprehension instead of assuming
    methodsSet :: HashMap Symbol Symbol
methodsSet = [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
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
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
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 = [(Symbol -> Symbol
GM.dropModuleNames Symbol
y, SpecType
t) | (Symbol
y, SpecType
t) <- DataConP -> [(Symbol, SpecType)]
dcpTyArgs DataConP
dcp]
    mkSymbol :: DFunId -> Symbol
mkSymbol DFunId
x
      | -- F.notracepp ("isDictonaryId:" ++ GM.showPpr x) $
        DFunId -> Bool
Ghc.isDictonaryId DFunId
x = Symbol -> Symbol -> Symbol
F.mappendSym Symbol
"$" (Int -> Symbol -> Symbol
F.dropSym Int
2 (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
subsTyVarMeet' (tv
a, RType c tv r
ta) ([(tv, RType c tv r)] -> RType c tv r -> RType c tv r
subst [(tv, RType c tv r)]
su RType c tv r
t)

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