{-# LANGUAGE OverloadedStrings #-}

module Language.Haskell.Liquid.WiredIn
       ( wiredTyCons
       , wiredDataCons
       , wiredSortedSyms

       -- * Constants for automatic proofs
       , dictionaryVar
       , dictionaryTyVar
       , dictionaryBind
       , proofTyConName
       , combineProofsName

       -- * Built in symbols
       , isWiredIn
       , isWiredInName
       , dcPrefix

       -- * Deriving classes 
       , isDerivedInstance 
       ) where

import Prelude                                hiding (error)
import Var

-- import Language.Fixpoint.Misc           (mapSnd)
import Language.Haskell.Liquid.GHC.Misc
import qualified Language.Haskell.Liquid.GHC.API as Ghc
import Language.Haskell.Liquid.Types.Types
import Language.Haskell.Liquid.Types.RefType
import Language.Haskell.Liquid.Types.Variance
import Language.Haskell.Liquid.Types.PredType

-- import Language.Fixpoint.Types hiding (panic)
import qualified Language.Fixpoint.Types as F
import qualified Data.HashSet as S 

import BasicTypes
-- import DataCon
-- import TyCon
import TysWiredIn

import Language.Haskell.Liquid.GHC.TypeRep ()
import CoreSyn hiding (mkTyArg)

-- | Horrible hack to support hardwired symbols like
--      `head`, `tail`, `fst`, `snd`
--   and other LH generated symbols that
--   *do not* correspond to GHC Vars and
--   *should not* be resolved to GHC Vars.

isWiredIn :: F.LocSymbol -> Bool
isWiredIn :: LocSymbol -> Bool
isWiredIn LocSymbol
x = LocSymbol -> Bool
isWiredInLoc LocSymbol
x  Bool -> Bool -> Bool
|| Symbol -> Bool
isWiredInName (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) Bool -> Bool -> Bool
|| LocSymbol -> Bool
isWiredInShape LocSymbol
x

isWiredInLoc :: F.LocSymbol -> Bool
isWiredInLoc :: LocSymbol -> Bool
isWiredInLoc LocSymbol
x  = Line
l Line -> Line -> Bool
forall a. Eq a => a -> a -> Bool
== Line
l' Bool -> Bool -> Bool
&& Line
l Line -> Line -> Bool
forall a. Eq a => a -> a -> Bool
== Line
0 Bool -> Bool -> Bool
&& Line
c Line -> Line -> Bool
forall a. Eq a => a -> a -> Bool
== Line
c' Bool -> Bool -> Bool
&& Line
c' Line -> Line -> Bool
forall a. Eq a => a -> a -> Bool
== Line
0
  where
    (Line
l , Line
c)  = SourcePos -> (Line, Line)
spe (LocSymbol -> SourcePos
forall a. Located a -> SourcePos
loc LocSymbol
x)
    (Line
l', Line
c') = SourcePos -> (Line, Line)
spe (LocSymbol -> SourcePos
forall a. Located a -> SourcePos
locE LocSymbol
x)
    spe :: SourcePos -> (Line, Line)
spe SourcePos
l    = (Line
x, Line
y) where (SourceName
_, Line
x, Line
y) = SourcePos -> (SourceName, Line, Line)
F.sourcePosElts SourcePos
l

isWiredInName :: F.Symbol -> Bool
isWiredInName :: Symbol -> Bool
isWiredInName Symbol
x = Symbol
x Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
wiredInNames

wiredInNames :: S.HashSet F.Symbol
wiredInNames :: HashSet Symbol
wiredInNames = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ Symbol
"head", Symbol
"tail", Symbol
"fst", Symbol
"snd", Symbol
"len"]

isWiredInShape :: F.LocSymbol -> Bool
isWiredInShape :: LocSymbol -> Bool
isWiredInShape LocSymbol
x = (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Symbol -> Bool
`F.isPrefixOfSym` (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x)) [Symbol
F.anfPrefix, Symbol
F.tempPrefix, Symbol
dcPrefix]
  -- where s        = val x
        -- dcPrefix = "lqdc"

dcPrefix :: F.Symbol
dcPrefix :: Symbol
dcPrefix = Symbol
"lqdc"

wiredSortedSyms :: [(F.Symbol, F.Sort)]
wiredSortedSyms :: [(Symbol, Sort)]
wiredSortedSyms = [(Line -> Symbol
forall a. Show a => a -> Symbol
pappSym Line
n, Line -> Sort
pappSort Line
n) | Line
n <- [Line
1..Line
pappArity]]

--------------------------------------------------------------------------------
-- | LH Primitive TyCons -------------------------------------------------------
--------------------------------------------------------------------------------

dictionaryVar :: Var
dictionaryVar :: Var
dictionaryVar   = SourceName -> Type -> Var
stringVar SourceName
"tmp_dictionary_var" (TyCoVarBinder -> Type -> Type
Ghc.ForAllTy (Var -> ArgFlag -> TyCoVarBinder
forall var argf. var -> argf -> VarBndr var argf
Ghc.Bndr Var
dictionaryTyVar ArgFlag
Required) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Var -> Type
Ghc.TyVarTy Var
dictionaryTyVar)

dictionaryTyVar :: TyVar
dictionaryTyVar :: Var
dictionaryTyVar = SourceName -> Var
stringTyVar SourceName
"da"

dictionaryBind :: Bind Var
dictionaryBind :: Bind Var
dictionaryBind = [(Var, Expr Var)] -> Bind Var
forall b. [(b, Expr b)] -> Bind b
Rec [(Var
v, Var -> Expr Var -> Expr Var
forall b. b -> Expr b -> Expr b
Lam Var
a (Expr Var -> Expr Var) -> Expr Var -> Expr Var
forall a b. (a -> b) -> a -> b
$ Expr Var -> Expr Var -> Expr Var
forall b. Expr b -> Expr b -> Expr b
App (Var -> Expr Var
forall b. Var -> Expr b
Var Var
v) (Type -> Expr Var
forall b. Type -> Expr b
Type (Type -> Expr Var) -> Type -> Expr Var
forall a b. (a -> b) -> a -> b
$ Var -> Type
Ghc.TyVarTy Var
a))]
  where
   v :: Var
v = Var
dictionaryVar
   a :: Var
a = Var
dictionaryTyVar

-----------------------------------------------------------------------
-- | LH Primitive TyCons ----------------------------------------------
-----------------------------------------------------------------------


combineProofsName :: String
combineProofsName :: SourceName
combineProofsName = SourceName
"combineProofs"

proofTyConName :: F.Symbol
proofTyConName :: Symbol
proofTyConName = Symbol
"Proof"

--------------------------------------------------------------------------------
-- | Predicate Types for WiredIns ----------------------------------------------
--------------------------------------------------------------------------------

maxArity :: Arity
maxArity :: Line
maxArity = Line
7

wiredTyCons :: [TyConP]
wiredTyCons :: [TyConP]
wiredTyCons  = ([TyConP], [Located DataConP]) -> [TyConP]
forall a b. (a, b) -> a
fst ([TyConP], [Located DataConP])
wiredTyDataCons

wiredDataCons :: [Located DataConP]
wiredDataCons :: [Located DataConP]
wiredDataCons = ([TyConP], [Located DataConP]) -> [Located DataConP]
forall a b. (a, b) -> b
snd ([TyConP], [Located DataConP])
wiredTyDataCons

wiredTyDataCons :: ([TyConP] , [Located DataConP])
wiredTyDataCons :: ([TyConP], [Located DataConP])
wiredTyDataCons = ([[TyConP]] -> [TyConP]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[TyConP]]
tcs, DataConP -> Located DataConP
forall a. a -> Located a
dummyLoc (DataConP -> Located DataConP) -> [DataConP] -> [Located DataConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[DataConP]] -> [DataConP]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[DataConP]]
dcs)
  where
    ([[TyConP]]
tcs, [[DataConP]]
dcs)  = [([TyConP], [DataConP])] -> ([[TyConP]], [[DataConP]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([([TyConP], [DataConP])] -> ([[TyConP]], [[DataConP]]))
-> [([TyConP], [DataConP])] -> ([[TyConP]], [[DataConP]])
forall a b. (a -> b) -> a -> b
$ ([TyConP], [DataConP])
listTyDataCons ([TyConP], [DataConP])
-> [([TyConP], [DataConP])] -> [([TyConP], [DataConP])]
forall a. a -> [a] -> [a]
: (Line -> ([TyConP], [DataConP]))
-> [Line] -> [([TyConP], [DataConP])]
forall a b. (a -> b) -> [a] -> [b]
map Line -> ([TyConP], [DataConP])
tupleTyDataCons [Line
2..Line
maxArity]

listTyDataCons :: ([TyConP] , [DataConP])
listTyDataCons :: ([TyConP], [DataConP])
listTyDataCons   = ( [(SourcePos
-> TyCon
-> [RTyVar]
-> [PVar RSort]
-> VarianceInfo
-> VarianceInfo
-> Maybe SizeFun
-> TyConP
TyConP SourcePos
l0 TyCon
c [Var -> RTyVar
RTV Var
tyv] [PVar RSort
p] [Variance
Covariant] [Variance
Covariant] (SizeFun -> Maybe SizeFun
forall a. a -> Maybe a
Just SizeFun
fsize))]
                   , [(SourcePos
-> DataCon
-> [RTyVar]
-> [PVar RSort]
-> [SpecType]
-> [(Symbol, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
DataConP SourcePos
l0 DataCon
nilDataCon  [Var -> RTyVar
RTV Var
tyv] [PVar RSort
p] [] []    SpecType
lt Bool
False Symbol
wiredInName SourcePos
l0)
                     ,(SourcePos
-> DataCon
-> [RTyVar]
-> [PVar RSort]
-> [SpecType]
-> [(Symbol, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
DataConP SourcePos
l0 DataCon
consDataCon [Var -> RTyVar
RTV Var
tyv] [PVar RSort
p] [] [(Symbol, SpecType)]
cargs SpecType
lt Bool
False Symbol
wiredInName SourcePos
l0)])
    where
      l0 :: SourcePos
l0         = SourceName -> SourcePos
F.dummyPos SourceName
"LH.Bare.listTyDataCons"
      c :: TyCon
c          = TyCon
listTyCon
      [Var
tyv]      = TyCon -> [Var]
tyConTyVarsDef TyCon
c
      t :: RSort
t          = Var -> RSort
forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
tyv :: RSort
      fld :: Symbol
fld        = Symbol
"fldList"
      xHead :: Symbol
xHead      = Symbol
"head"
      xTail :: Symbol
xTail      = Symbol
"tail"
      p :: PVar RSort
p          = Symbol
-> PVKind RSort -> Symbol -> [(RSort, Symbol, Expr)] -> PVar RSort
forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
"p" (RSort -> PVKind RSort
forall t. t -> PVKind t
PVProp RSort
t) (Maybe Integer -> Symbol
F.vv Maybe Integer
forall a. Maybe a
Nothing) [(RSort
t, Symbol
fld, Symbol -> Expr
F.EVar Symbol
fld)]
      px :: UReft Reft
px         = PVar RSort -> UReft Reft
forall t. PVar t -> UReft Reft
pdVarReft (PVar RSort -> UReft Reft) -> PVar RSort -> UReft Reft
forall a b. (a -> b) -> a -> b
$ Symbol
-> PVKind RSort -> Symbol -> [(RSort, Symbol, Expr)] -> PVar RSort
forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
"p" (RSort -> PVKind RSort
forall t. t -> PVKind t
PVProp RSort
t) (Maybe Integer -> Symbol
F.vv Maybe Integer
forall a. Maybe a
Nothing) [(RSort
t, Symbol
fld, Symbol -> Expr
F.EVar Symbol
xHead)]
      lt :: SpecType
lt         = TyCon
-> [SpecType]
-> [RTProp RTyCon RTyVar (UReft Reft)]
-> UReft Reft
-> SpecType
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c [SpecType
forall c. RType c RTyVar (UReft Reft)
xt] [[(Symbol, RSort)]
-> UReft Reft -> RTProp RTyCon RTyVar (UReft Reft)
forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [] (UReft Reft -> RTProp RTyCon RTyVar (UReft Reft))
-> UReft Reft -> RTProp RTyCon RTyVar (UReft Reft)
forall a b. (a -> b) -> a -> b
$ PVar RSort -> UReft Reft
forall t. PVar t -> UReft Reft
pdVarReft PVar RSort
p] UReft Reft
forall a. Monoid a => a
mempty
      xt :: RType c RTyVar (UReft Reft)
xt         = Var -> RType c RTyVar (UReft Reft)
forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
tyv
      xst :: SpecType
xst        = TyCon
-> [SpecType]
-> [RTProp RTyCon RTyVar (UReft Reft)]
-> UReft Reft
-> SpecType
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c [RTyVar -> UReft Reft -> SpecType
forall c tv r. tv -> r -> RType c tv r
RVar (Var -> RTyVar
RTV Var
tyv) UReft Reft
px] [[(Symbol, RSort)]
-> UReft Reft -> RTProp RTyCon RTyVar (UReft Reft)
forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [] (UReft Reft -> RTProp RTyCon RTyVar (UReft Reft))
-> UReft Reft -> RTProp RTyCon RTyVar (UReft Reft)
forall a b. (a -> b) -> a -> b
$ PVar RSort -> UReft Reft
forall t. PVar t -> UReft Reft
pdVarReft PVar RSort
p] UReft Reft
forall a. Monoid a => a
mempty
      cargs :: [(Symbol, SpecType)]
cargs      = [(Symbol
xTail, SpecType
xst), (Symbol
xHead, SpecType
forall c. RType c RTyVar (UReft Reft)
xt)]
      fsize :: SizeFun
fsize      = LocSymbol -> SizeFun
SymSizeFun (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
"len")

wiredInName :: F.Symbol
wiredInName :: Symbol
wiredInName = Symbol
"WiredIn"

tupleTyDataCons :: Int -> ([TyConP] , [DataConP])
tupleTyDataCons :: Line -> ([TyConP], [DataConP])
tupleTyDataCons Line
n = ( [(SourcePos
-> TyCon
-> [RTyVar]
-> [PVar RSort]
-> VarianceInfo
-> VarianceInfo
-> Maybe SizeFun
-> TyConP
TyConP   SourcePos
l0 TyCon
c  (Var -> RTyVar
RTV (Var -> RTyVar) -> [Var] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
tyvs) [PVar RSort]
ps VarianceInfo
tyvarinfo VarianceInfo
pdvarinfo Maybe SizeFun
forall a. Maybe a
Nothing)]
                    , [(SourcePos
-> DataCon
-> [RTyVar]
-> [PVar RSort]
-> [SpecType]
-> [(Symbol, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
DataConP SourcePos
l0 DataCon
dc (Var -> RTyVar
RTV (Var -> RTyVar) -> [Var] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
tyvs) [PVar RSort]
ps []  [(Symbol, SpecType)]
forall c. [(Symbol, RType c RTyVar (UReft Reft))]
cargs  SpecType
lt Bool
False Symbol
wiredInName SourcePos
l0)])
  where
    tyvarinfo :: VarianceInfo
tyvarinfo     = Line -> Variance -> VarianceInfo
forall a. Line -> a -> [a]
replicate Line
n     Variance
Covariant
    pdvarinfo :: VarianceInfo
pdvarinfo     = Line -> Variance -> VarianceInfo
forall a. Line -> a -> [a]
replicate (Line
nLine -> Line -> Line
forall a. Num a => a -> a -> a
-Line
1) Variance
Covariant
    l0 :: SourcePos
l0            = SourceName -> SourcePos
F.dummyPos SourceName
"LH.Bare.tupleTyDataCons"
    c :: TyCon
c             = Boxity -> Line -> TyCon
tupleTyCon   Boxity
Boxed Line
n
    dc :: DataCon
dc            = Boxity -> Line -> DataCon
tupleDataCon Boxity
Boxed Line
n
    tyvs :: [Var]
tyvs@(Var
tv:[Var]
tvs) = TyCon -> [Var]
tyConTyVarsDef TyCon
c
    (RSort
ta:[RSort]
ts)       = (Var -> RSort
forall r c. Monoid r => Var -> RType c RTyVar r
rVar (Var -> RSort) -> [Var] -> [RSort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
tyvs) :: [RSort]
    flds :: [Symbol]
flds          = SourceName -> [Symbol]
mks SourceName
"fld_Tuple"
    fld :: Symbol
fld           = Symbol
"fld_Tuple"
    Symbol
x1:[Symbol]
xs         = SourceName -> [Symbol]
mks (SourceName
"x_Tuple" SourceName -> SourceName -> SourceName
forall a. [a] -> [a] -> [a]
++ Line -> SourceName
forall a. Show a => a -> SourceName
show Line
n)
    ps :: [PVar RSort]
ps            = [Symbol] -> [RSort] -> [(Symbol, Expr)] -> [PVar RSort]
forall t. [Symbol] -> [t] -> [(Symbol, Expr)] -> [PVar t]
mkps [Symbol]
pnames (RSort
taRSort -> [RSort] -> [RSort]
forall a. a -> [a] -> [a]
:[RSort]
ts) ((Symbol
fld, Symbol -> Expr
F.EVar Symbol
fld) (Symbol, Expr) -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. a -> [a] -> [a]
: [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
flds (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
flds))
    ups :: [UsedPVar]
ups           = PVar RSort -> UsedPVar
forall t. PVar t -> UsedPVar
uPVar (PVar RSort -> UsedPVar) -> [PVar RSort] -> [UsedPVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar RSort]
ps
    pxs :: [PVar RSort]
pxs           = [Symbol] -> [RSort] -> [(Symbol, Expr)] -> [PVar RSort]
forall t. [Symbol] -> [t] -> [(Symbol, Expr)] -> [PVar t]
mkps [Symbol]
pnames (RSort
taRSort -> [RSort] -> [RSort]
forall a. a -> [a] -> [a]
:[RSort]
ts) ((Symbol
fld, Symbol -> Expr
F.EVar Symbol
x1) (Symbol, Expr) -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. a -> [a] -> [a]
: [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
flds (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs))
    lt :: SpecType
lt            = TyCon
-> [SpecType]
-> [RTProp RTyCon RTyVar (UReft Reft)]
-> UReft Reft
-> SpecType
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c (Var -> SpecType
forall r c. Monoid r => Var -> RType c RTyVar r
rVar (Var -> SpecType) -> [Var] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
tyvs) ([(Symbol, RSort)]
-> UReft Reft -> RTProp RTyCon RTyVar (UReft Reft)
forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [] (UReft Reft -> RTProp RTyCon RTyVar (UReft Reft))
-> (UsedPVar -> UReft Reft)
-> UsedPVar
-> RTProp RTyCon RTyVar (UReft Reft)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UsedPVar -> UReft Reft
forall t. PVar t -> UReft Reft
pdVarReft (UsedPVar -> RTProp RTyCon RTyVar (UReft Reft))
-> [UsedPVar] -> [RTProp RTyCon RTyVar (UReft Reft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
ups) UReft Reft
forall a. Monoid a => a
mempty
    xts :: [RType c RTyVar (UReft Reft)]
xts           = (Var -> PVar RSort -> RType c RTyVar (UReft Reft))
-> [Var] -> [PVar RSort] -> [RType c RTyVar (UReft Reft)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Var
v PVar RSort
p -> RTyVar -> UReft Reft -> RType c RTyVar (UReft Reft)
forall c tv r. tv -> r -> RType c tv r
RVar (Var -> RTyVar
RTV Var
v) (PVar RSort -> UReft Reft
forall t. PVar t -> UReft Reft
pdVarReft PVar RSort
p)) [Var]
tvs [PVar RSort]
pxs
    cargs :: [(Symbol, RType c RTyVar (UReft Reft))]
cargs         = [(Symbol, RType c RTyVar (UReft Reft))]
-> [(Symbol, RType c RTyVar (UReft Reft))]
forall a. [a] -> [a]
reverse ([(Symbol, RType c RTyVar (UReft Reft))]
 -> [(Symbol, RType c RTyVar (UReft Reft))])
-> [(Symbol, RType c RTyVar (UReft Reft))]
-> [(Symbol, RType c RTyVar (UReft Reft))]
forall a b. (a -> b) -> a -> b
$ (Symbol
x1, Var -> RType c RTyVar (UReft Reft)
forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
tv) (Symbol, RType c RTyVar (UReft Reft))
-> [(Symbol, RType c RTyVar (UReft Reft))]
-> [(Symbol, RType c RTyVar (UReft Reft))]
forall a. a -> [a] -> [a]
: [Symbol]
-> [RType c RTyVar (UReft Reft)]
-> [(Symbol, RType c RTyVar (UReft Reft))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [RType c RTyVar (UReft Reft)]
forall c. [RType c RTyVar (UReft Reft)]
xts
    pnames :: [Symbol]
pnames        = SourceName -> [Symbol]
mks_ SourceName
"p"
    mks :: SourceName -> [Symbol]
mks  SourceName
x        = (\Line
i -> SourceName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (SourceName
xSourceName -> SourceName -> SourceName
forall a. [a] -> [a] -> [a]
++ Line -> SourceName
forall a. Show a => a -> SourceName
show Line
i)) (Line -> Symbol) -> [Line] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Line
1..Line
n]
    mks_ :: SourceName -> [Symbol]
mks_ SourceName
x        = (\Line
i -> SourceName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (SourceName
xSourceName -> SourceName -> SourceName
forall a. [a] -> [a] -> [a]
++ Line -> SourceName
forall a. Show a => a -> SourceName
show Line
i)) (Line -> Symbol) -> [Line] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Line
2..Line
n]


mkps :: [F.Symbol]
     -> [t] -> [(F.Symbol, F.Expr)] -> [PVar t]
mkps :: [Symbol] -> [t] -> [(Symbol, Expr)] -> [PVar t]
mkps [Symbol]
ns (t
t:[t]
ts) ((Symbol
f,Expr
x):[(Symbol, Expr)]
fxs) = [PVar t] -> [PVar t]
forall a. [a] -> [a]
reverse ([PVar t] -> [PVar t]) -> [PVar t] -> [PVar t]
forall a b. (a -> b) -> a -> b
$ [Symbol]
-> [t]
-> [(Symbol, Expr)]
-> [(t, Symbol, Expr)]
-> [PVar t]
-> [PVar t]
forall t.
[Symbol]
-> [t]
-> [(Symbol, Expr)]
-> [(t, Symbol, Expr)]
-> [PVar t]
-> [PVar t]
mkps_ [Symbol]
ns [t]
ts [(Symbol, Expr)]
fxs [(t
t, Symbol
f, Expr
x)] []
mkps [Symbol]
_  [t]
_      [(Symbol, Expr)]
_           = Maybe SrcSpan -> SourceName -> [PVar t]
forall a. Maybe SrcSpan -> SourceName -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing SourceName
"Bare : mkps"

mkps_ :: [F.Symbol]
      -> [t]
      -> [(F.Symbol, F.Expr)]
      -> [(t, F.Symbol, F.Expr)]
      -> [PVar t]
      -> [PVar t]
mkps_ :: [Symbol]
-> [t]
-> [(Symbol, Expr)]
-> [(t, Symbol, Expr)]
-> [PVar t]
-> [PVar t]
mkps_ []     [t]
_       [(Symbol, Expr)]
_          [(t, Symbol, Expr)]
_    [PVar t]
ps = [PVar t]
ps
mkps_ (Symbol
n:[Symbol]
ns) (t
t:[t]
ts) ((Symbol
f, Expr
x):[(Symbol, Expr)]
xs) [(t, Symbol, Expr)]
args [PVar t]
ps = [Symbol]
-> [t]
-> [(Symbol, Expr)]
-> [(t, Symbol, Expr)]
-> [PVar t]
-> [PVar t]
forall t.
[Symbol]
-> [t]
-> [(Symbol, Expr)]
-> [(t, Symbol, Expr)]
-> [PVar t]
-> [PVar t]
mkps_ [Symbol]
ns [t]
ts [(Symbol, Expr)]
xs ((t, Symbol, Expr)
a(t, Symbol, Expr) -> [(t, Symbol, Expr)] -> [(t, Symbol, Expr)]
forall a. a -> [a] -> [a]
:[(t, Symbol, Expr)]
args) (PVar t
pPVar t -> [PVar t] -> [PVar t]
forall a. a -> [a] -> [a]
:[PVar t]
ps)
  where
    p :: PVar t
p                                   = Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
n (t -> PVKind t
forall t. t -> PVKind t
PVProp t
t) (Maybe Integer -> Symbol
F.vv Maybe Integer
forall a. Maybe a
Nothing) [(t, Symbol, Expr)]
args
    a :: (t, Symbol, Expr)
a                                   = (t
t, Symbol
f, Expr
x)
mkps_ [Symbol]
_     [t]
_       [(Symbol, Expr)]
_          [(t, Symbol, Expr)]
_    [PVar t]
_ = Maybe SrcSpan -> SourceName -> [PVar t]
forall a. Maybe SrcSpan -> SourceName -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing SourceName
"Bare : mkps_"


--------------------------------------------------------------------------------
isDerivedInstance :: Ghc.ClsInst -> Bool 
--------------------------------------------------------------------------------
isDerivedInstance :: ClsInst -> Bool
isDerivedInstance ClsInst
i = SourceName -> Bool -> Bool
forall a. PPrint a => SourceName -> a -> a
F.notracepp (SourceName
"IS-DERIVED: " SourceName -> SourceName -> SourceName
forall a. [a] -> [a] -> [a]
++ Symbol -> SourceName
forall a. PPrint a => a -> SourceName
F.showpp Symbol
classSym) 
                    (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
classSym HashSet Symbol
derivingClasses 
  where 
    classSym :: Symbol
classSym        = Class -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Class -> Symbol) -> (ClsInst -> Class) -> ClsInst -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClsInst -> Class
Ghc.is_cls (ClsInst -> Symbol) -> ClsInst -> Symbol
forall a b. (a -> b) -> a -> b
$ ClsInst
i
  
derivingClasses :: S.HashSet F.Symbol 
derivingClasses :: HashSet Symbol
derivingClasses = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList 
  [ Symbol
"GHC.Classes.Eq"
  , Symbol
"GHC.Classes.Ord"
  , Symbol
"GHC.Enum.Enum"
  , Symbol
"GHC.Show.Show"
  , Symbol
"GHC.Read.Read"
  , Symbol
"GHC.Base.Monad"
  , Symbol
"GHC.Base.Applicative"
  , Symbol
"GHC.Base.Functor"
  , Symbol
"Data.Foldable.Foldable"
  , Symbol
"Data.Traversable.Traversable"
  -- , "GHC.Enum.Bounded"
  -- , "GHC.Base.Monoid"
  ]