{-# LANGUAGE OverloadedStrings #-}

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

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

       , charDataCon

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

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

       -- * Deriving classes
       , isDerivedInstance
       , derivingClasses
       ) where

import Prelude                                hiding (error)

-- import Language.Fixpoint.Misc           (mapSnd)
import Language.Haskell.Liquid.GHC.Misc
import qualified Liquid.GHC.API as Ghc
import Liquid.GHC.API (Var, Arity, TyVar, Bind(..), Boxity(..), Expr(..), ForAllTyFlag(Required))
import Language.Haskell.Liquid.Types.Errors
import Language.Haskell.Liquid.Types.Names
import Language.Haskell.Liquid.Types.RType
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.Config as F
import qualified Language.Fixpoint.Smt.Theories as F
import qualified Language.Fixpoint.Types as F
import           Data.Bifunctor (first)
import qualified Data.HashSet as S
import           Data.Maybe

import Language.Haskell.Liquid.GHC.TypeRep ()

-- | 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
sym  = Line
ln Line -> Line -> Bool
forall a. Eq a => a -> a -> Bool
== Line
ln' Bool -> Bool -> Bool
&& Line
ln Line -> Line -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Line
F.safePos Int
1 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
== Int -> Line
F.safePos Int
1
  where
    (Line
ln , Line
c)  = SourcePos -> (Line, Line)
spe (LocSymbol -> SourcePos
forall a. Located a -> SourcePos
loc LocSymbol
sym)
    (Line
ln', Line
c') = SourcePos -> (Line, Line)
spe (LocSymbol -> SourcePos
forall a. Located a -> SourcePos
locE LocSymbol
sym)
    spe :: SourcePos -> (Line, Line)
spe SourcePos
l    = (Line
x, Line
y) where (String
_, Line
x, Line
y) = SourcePos -> (String, 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 =
    (Symbol
selfSymbol,Sort
selfSort) (Symbol, Sort) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. a -> [a] -> [a]
:
    [(Int -> Symbol
forall a. Show a => a -> Symbol
pappSym Int
n, Int -> Sort
pappSort Int
n) | Int
n <- [Int
1..Int
pappArity]] [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++
    [(Symbol, Sort)]
wiredTheorySortedSyms
  where
    selfSort :: Sort
selfSort = Int -> Sort -> Sort
F.FAbs Int
1 (Int -> Sort
F.FVar Int
0)

wiredTheorySortedSyms :: [(F.Symbol, F.Sort)]
wiredTheorySortedSyms :: [(Symbol, Sort)]
wiredTheorySortedSyms =
    [ (Symbol
s, Sort
srt)
    | Symbol
s <- [Symbol]
wiredTheorySyms
    , let srt :: Sort
srt = TheorySymbol -> Sort
F.tsSort (TheorySymbol -> Sort) -> TheorySymbol -> Sort
forall a b. (a -> b) -> a -> b
$
                  TheorySymbol -> Maybe TheorySymbol -> TheorySymbol
forall a. a -> Maybe a -> a
fromMaybe (Maybe SrcSpan -> String -> TheorySymbol
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String
"unknown symbol: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show Symbol
s)) (Maybe TheorySymbol -> TheorySymbol)
-> Maybe TheorySymbol -> TheorySymbol
forall a b. (a -> b) -> a -> b
$
                    Symbol -> SEnv TheorySymbol -> Maybe TheorySymbol
forall a. Symbol -> SEnv a -> Maybe a
F.lookupSEnv Symbol
s (SMTSolver -> [DataDecl] -> SEnv TheorySymbol
F.theorySymbols SMTSolver
F.Z3 [])
    ]
  where
    wiredTheorySyms :: [Symbol]
wiredTheorySyms =
      [ Symbol
"Map_default"
      , Symbol
"Map_select"
      , Symbol
"Map_store"

      , Symbol
"Set_cup"
      , Symbol
"Set_cap"
      , Symbol
"Set_dif"
      , Symbol
"Set_sng"
      , Symbol
"Set_emp"
      , Symbol
"Set_empty"
      , Symbol
"Set_mem"
      , Symbol
"Set_sub"
      , Symbol
"Set_add"
      , Symbol
"Set_com"

      , Symbol
"Bag_count"
      , Symbol
"Bag_empty"
      , Symbol
"Bag_inter_min"
      , Symbol
"Bag_sng"
      , Symbol
"Bag_sub"
      , Symbol
"Bag_union"
      , Symbol
"Bag_union_max"

      , Symbol
"strLen"
      ]

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

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

dictionaryTyVar :: TyVar
dictionaryTyVar :: Var
dictionaryTyVar = String -> Var
stringTyVar String
"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 :: String
combineProofsName = String
"combineProofs"

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

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

maxArity :: Arity
maxArity :: Int
maxArity = Int
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]
: (Int -> ([TyConP], [DataConP]))
-> [Int] -> [([TyConP], [DataConP])]
forall a b. (a -> b) -> [a] -> [b]
map Int -> ([TyConP], [DataConP])
tupleTyDataCons [Int
2..Int
maxArity]

charDataCon :: Located DataConP
charDataCon :: Located DataConP
charDataCon = DataConP -> Located DataConP
forall a. a -> Located a
dummyLoc (SourcePos
-> DataCon
-> [RTyVar]
-> [PVar RSort]
-> [SpecType]
-> [(LHName, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
DataConP SourcePos
l0 DataCon
Ghc.charDataCon  [] [] [] [(Symbol -> LHName
makeGeneratedLogicLHName Symbol
"charX",SpecType
forall {tv}. RType RTyCon tv RReft
lt)] SpecType
forall {tv}. RType RTyCon tv RReft
lt Bool
False Symbol
wiredInName SourcePos
l0)
  where
    l0 :: SourcePos
l0 = String -> SourcePos
F.dummyPos String
"LH.Bare.charTyDataCons"
    c :: TyCon
c  = TyCon
Ghc.charTyCon
    lt :: RType RTyCon tv RReft
lt = TyCon
-> [RType RTyCon tv RReft]
-> [RTProp RTyCon tv RReft]
-> RReft
-> RType RTyCon tv RReft
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c [] [] RReft
forall a. Monoid a => a
mempty

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]
-> [(LHName, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
DataConP SourcePos
l0 DataCon
Ghc.nilDataCon  [Var -> RTyVar
RTV Var
tyv] [PVar RSort
p] [] []    SpecType
lt Bool
False Symbol
wiredInName SourcePos
l0
                   ,  SourcePos
-> DataCon
-> [RTyVar]
-> [PVar RSort]
-> [SpecType]
-> [(LHName, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
DataConP SourcePos
l0 DataCon
Ghc.consDataCon [Var -> RTyVar
RTV Var
tyv] [PVar RSort
p] [] [(LHName, SpecType)]
cargs SpecType
lt Bool
False Symbol
wiredInName SourcePos
l0])
    where
      l0 :: SourcePos
l0         = String -> SourcePos
F.dummyPos String
"LH.Bare.listTyDataCons"
      c :: TyCon
c          = TyCon
Ghc.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
-> RSort -> Symbol -> [(RSort, Symbol, ExprV Symbol)] -> PVar RSort
forall v t.
Symbol -> t -> Symbol -> [(t, Symbol, ExprV v)] -> PVarV v t
PV Symbol
"p" RSort
t (Maybe Integer -> Symbol
F.vv Maybe Integer
forall a. Maybe a
Nothing) [(RSort
t, Symbol
fld, Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
fld)]
      px :: RReft
px         = PVar RSort -> RReft
forall t. PVar t -> RReft
pdVarReft (PVar RSort -> RReft) -> PVar RSort -> RReft
forall a b. (a -> b) -> a -> b
$ Symbol
-> RSort -> Symbol -> [(RSort, Symbol, ExprV Symbol)] -> PVar RSort
forall v t.
Symbol -> t -> Symbol -> [(t, Symbol, ExprV v)] -> PVarV v t
PV Symbol
"p" RSort
t (Maybe Integer -> Symbol
F.vv Maybe Integer
forall a. Maybe a
Nothing) [(RSort
t, Symbol
fld, Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
xHead)]
      lt :: SpecType
lt         = TyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> 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 RReft
xt] [[(Symbol, RSort)] -> RReft -> RTProp RTyCon RTyVar RReft
forall τ r v c tv. [(Symbol, τ)] -> r -> Ref τ (RTypeV v c tv r)
rPropP [] (RReft -> RTProp RTyCon RTyVar RReft)
-> RReft -> RTProp RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ PVar RSort -> RReft
forall t. PVar t -> RReft
pdVarReft PVar RSort
p] RReft
forall a. Monoid a => a
mempty
      xt :: RType c RTyVar RReft
xt         = Var -> RType c RTyVar RReft
forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
tyv
      xst :: SpecType
xst        = TyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c [RTyVar -> RReft -> SpecType
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar (Var -> RTyVar
RTV Var
tyv) RReft
px] [[(Symbol, RSort)] -> RReft -> RTProp RTyCon RTyVar RReft
forall τ r v c tv. [(Symbol, τ)] -> r -> Ref τ (RTypeV v c tv r)
rPropP [] (RReft -> RTProp RTyCon RTyVar RReft)
-> RReft -> RTProp RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ PVar RSort -> RReft
forall t. PVar t -> RReft
pdVarReft PVar RSort
p] RReft
forall a. Monoid a => a
mempty
      cargs :: [(LHName, SpecType)]
cargs      = ((Symbol, SpecType) -> (LHName, SpecType))
-> [(Symbol, SpecType)] -> [(LHName, SpecType)]
forall a b. (a -> b) -> [a] -> [b]
map ((Symbol -> LHName) -> (Symbol, SpecType) -> (LHName, SpecType)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Symbol -> LHName
makeGeneratedLogicLHName) [(Symbol
xTail, SpecType
xst), (Symbol
xHead, SpecType
forall {c}. RType c RTyVar RReft
xt)]
      fsize :: SizeFun
fsize      = LocSymbol -> SizeFun
forall v. Located v -> SizeFunV v
SymSizeFun (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
"GHC.Types_LHAssumptions.len")

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

tupleTyDataCons :: Int -> ([TyConP] , [DataConP])
tupleTyDataCons :: Int -> ([TyConP], [DataConP])
tupleTyDataCons Int
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]
-> [(LHName, 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 []  [(LHName, SpecType)]
forall {c}. [(LHName, RType c RTyVar RReft)]
cargs  SpecType
lt Bool
False Symbol
wiredInName SourcePos
l0])
  where
    tyvarinfo :: VarianceInfo
tyvarinfo     = Int -> Variance -> VarianceInfo
forall a. Int -> a -> [a]
replicate Int
n     Variance
Covariant
    pdvarinfo :: VarianceInfo
pdvarinfo     = Int -> Variance -> VarianceInfo
forall a. Int -> a -> [a]
replicate (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Variance
Covariant
    l0 :: SourcePos
l0            = String -> SourcePos
F.dummyPos String
"LH.Bare.tupleTyDataCons"
    c :: TyCon
c             = Boxity -> Int -> TyCon
Ghc.tupleTyCon   Boxity
Boxed Int
n
    dc :: DataCon
dc            = Boxity -> Int -> DataCon
Ghc.tupleDataCon Boxity
Boxed Int
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          = String -> [Symbol]
mks String
"fld_Tuple"
    fld :: Symbol
fld           = Symbol
"fld_Tuple"
    Symbol
x1:[Symbol]
xs         = String -> [Symbol]
mks (String
"x_Tuple" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)
    ps :: [PVar RSort]
ps            = [Symbol] -> [RSort] -> [(Symbol, ExprV Symbol)] -> [PVar RSort]
forall t. [Symbol] -> [t] -> [(Symbol, ExprV Symbol)] -> [PVar t]
mkps [Symbol]
pnames (RSort
taRSort -> [RSort] -> [RSort]
forall a. a -> [a] -> [a]
:[RSort]
ts) ((Symbol
fld, Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
fld) (Symbol, ExprV Symbol)
-> [(Symbol, ExprV Symbol)] -> [(Symbol, ExprV Symbol)]
forall a. a -> [a] -> [a]
: [Symbol] -> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
flds (Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar (Symbol -> ExprV Symbol) -> [Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
flds))
    ups :: [UsedPVarV Symbol]
ups           = PVar RSort -> UsedPVarV Symbol
forall v t. PVarV v t -> UsedPVarV v
uPVar (PVar RSort -> UsedPVarV Symbol)
-> [PVar RSort] -> [UsedPVarV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar RSort]
ps
    pxs :: [PVar RSort]
pxs           = [Symbol] -> [RSort] -> [(Symbol, ExprV Symbol)] -> [PVar RSort]
forall t. [Symbol] -> [t] -> [(Symbol, ExprV Symbol)] -> [PVar t]
mkps [Symbol]
pnames (RSort
taRSort -> [RSort] -> [RSort]
forall a. a -> [a] -> [a]
:[RSort]
ts) ((Symbol
fld, Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
x1) (Symbol, ExprV Symbol)
-> [(Symbol, ExprV Symbol)] -> [(Symbol, ExprV Symbol)]
forall a. a -> [a] -> [a]
: [Symbol] -> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
flds (Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar (Symbol -> ExprV Symbol) -> [Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs))
    lt :: SpecType
lt            = TyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> 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)] -> RReft -> RTProp RTyCon RTyVar RReft
forall τ r v c tv. [(Symbol, τ)] -> r -> Ref τ (RTypeV v c tv r)
rPropP [] (RReft -> RTProp RTyCon RTyVar RReft)
-> (UsedPVarV Symbol -> RReft)
-> UsedPVarV Symbol
-> RTProp RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UsedPVarV Symbol -> RReft
forall t. PVar t -> RReft
pdVarReft (UsedPVarV Symbol -> RTProp RTyCon RTyVar RReft)
-> [UsedPVarV Symbol] -> [RTProp RTyCon RTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVarV Symbol]
ups) RReft
forall a. Monoid a => a
mempty
    xts :: [RTypeV v c RTyVar RReft]
xts           = (Var -> PVar RSort -> RTypeV v c RTyVar RReft)
-> [Var] -> [PVar RSort] -> [RTypeV v c RTyVar RReft]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Var
v PVar RSort
p -> RTyVar -> RReft -> RTypeV v c RTyVar RReft
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar (Var -> RTyVar
RTV Var
v) (PVar RSort -> RReft
forall t. PVar t -> RReft
pdVarReft PVar RSort
p)) [Var]
tvs [PVar RSort]
pxs
    cargs :: [(LHName, RType c RTyVar RReft)]
cargs         = ((Symbol, RType c RTyVar RReft) -> (LHName, RType c RTyVar RReft))
-> [(Symbol, RType c RTyVar RReft)]
-> [(LHName, RType c RTyVar RReft)]
forall a b. (a -> b) -> [a] -> [b]
map ((Symbol -> LHName)
-> (Symbol, RType c RTyVar RReft) -> (LHName, RType c RTyVar RReft)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Symbol -> LHName
makeGeneratedLogicLHName) ([(Symbol, RType c RTyVar RReft)]
 -> [(LHName, RType c RTyVar RReft)])
-> [(Symbol, RType c RTyVar RReft)]
-> [(LHName, RType c RTyVar RReft)]
forall a b. (a -> b) -> a -> b
$ [(Symbol, RType c RTyVar RReft)]
-> [(Symbol, RType c RTyVar RReft)]
forall a. [a] -> [a]
reverse ([(Symbol, RType c RTyVar RReft)]
 -> [(Symbol, RType c RTyVar RReft)])
-> [(Symbol, RType c RTyVar RReft)]
-> [(Symbol, RType c RTyVar RReft)]
forall a b. (a -> b) -> a -> b
$ (Symbol
x1, Var -> RType c RTyVar RReft
forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
tv) (Symbol, RType c RTyVar RReft)
-> [(Symbol, RType c RTyVar RReft)]
-> [(Symbol, RType c RTyVar RReft)]
forall a. a -> [a] -> [a]
: [Symbol]
-> [RType c RTyVar RReft] -> [(Symbol, RType c RTyVar RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [RType c RTyVar RReft]
forall {v} {c}. [RTypeV v c RTyVar RReft]
xts
    pnames :: [Symbol]
pnames        = String -> [Symbol]
mks_ String
"p"
    mks :: String -> [Symbol]
mks  String
x        = (\Int
i -> String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String
xString -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) (Int -> Symbol) -> [Int] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..Int
n]
    mks_ :: String -> [Symbol]
mks_ String
x        = (\Int
i -> String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String
xString -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) (Int -> Symbol) -> [Int] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
2..Int
n]


mkps :: [F.Symbol]
     -> [t] -> [(F.Symbol, F.Expr)] -> [PVar t]
mkps :: forall t. [Symbol] -> [t] -> [(Symbol, ExprV Symbol)] -> [PVar t]
mkps [Symbol]
ns (t
t:[t]
ts) ((Symbol
f,ExprV Symbol
x):[(Symbol, ExprV Symbol)]
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, ExprV Symbol)]
-> [(t, Symbol, ExprV Symbol)]
-> [PVar t]
-> [PVar t]
forall t.
[Symbol]
-> [t]
-> [(Symbol, ExprV Symbol)]
-> [(t, Symbol, ExprV Symbol)]
-> [PVar t]
-> [PVar t]
mkps_ [Symbol]
ns [t]
ts [(Symbol, ExprV Symbol)]
fxs [(t
t, Symbol
f, ExprV Symbol
x)] []
mkps [Symbol]
_  [t]
_      [(Symbol, ExprV Symbol)]
_           = Maybe SrcSpan -> String -> [PVar t]
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"Bare : mkps"

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


--------------------------------------------------------------------------------
isDerivedInstance :: Ghc.ClsInst -> Bool
--------------------------------------------------------------------------------
isDerivedInstance :: ClsInst -> Bool
isDerivedInstance ClsInst
i = String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
F.notracepp (String
"IS-DERIVED: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
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
derivingClassesSet
  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

derivingClassesSet :: S.HashSet F.Symbol
derivingClassesSet :: HashSet Symbol
derivingClassesSet = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ (String -> Symbol) -> [String] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol [String]
derivingClasses

derivingClasses :: [String]
derivingClasses :: [String]
derivingClasses =
  [ String
"GHC.Classes.Eq"
  , String
"GHC.Classes.Ord"
  , String
"GHC.Internal.Enum.Enum"
  , String
"GHC.Internal.Show.Show"
  , String
"GHC.Internal.Read.Read"
  , String
"GHC.Internal.Base.Monad"
  , String
"GHC.Internal.Base.Applicative"
  , String
"GHC.Internal.Base.Functor"
  , String
"GHC.Internal.Data.Foldable.Foldable"
  , String
"GHC.Internal.Data.Traversable.Traversable"
  , String
"GHC.Internal.Real.Fractional"
  -- , "GHC.Enum.Bounded"
  -- , "GHC.Base.Monoid"
  ]