liquidhaskell-boot-0.9.12.2: src/Language/Haskell/Liquid/WiredIn.hs
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# 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 x = isWiredInLoc x || isWiredInName (val x) || isWiredInShape x
isWiredInLoc :: F.LocSymbol -> Bool
isWiredInLoc sym = ln == ln' && ln == F.safePos 1 && c == c' && c' == F.safePos 1
where
(ln , c) = spe (loc sym)
(ln', c') = spe (locE sym)
spe l = (x, y) where (_, x, y) = F.sourcePosElts l
isWiredInName :: F.Symbol -> Bool
isWiredInName x = x `S.member` wiredInNames
wiredInNames :: S.HashSet F.Symbol
wiredInNames = S.fromList [ "head", "tail", "fst", "snd", "len"]
isWiredInShape :: F.LocSymbol -> Bool
isWiredInShape x = any (`F.isPrefixOfSym` val x) [F.anfPrefix, F.tempPrefix, dcPrefix]
-- where s = val x
-- dcPrefix = "lqdc"
dcPrefix :: F.Symbol
dcPrefix = "lqdc"
wiredSortedSyms :: [(F.Symbol, F.Sort)]
wiredSortedSyms =
(selfSymbol,selfSort) :
[(pappSym n, pappSort n) | n <- [1..pappArity]] ++
wiredTheorySortedSyms
where
selfSort = F.FAbs 1 (F.FVar 0)
wiredTheorySortedSyms :: [(F.Symbol, F.Sort)]
wiredTheorySortedSyms =
[ (s, srt)
| s <- wiredTheorySyms
, let srt = F.tsSort $
fromMaybe (panic Nothing ("unknown symbol: " ++ show s)) $
F.lookupSEnv s (F.theorySymbols F.Z3)
]
where
wiredTheorySyms =
[ "Map_default"
, "Map_select"
, "Map_store"
, "Set_cup"
, "Set_cap"
, "Set_dif"
, "Set_sng"
, "Set_emp"
, "Set_empty"
, "Set_mem"
, "Set_sub"
, "Set_add"
, "Set_com"
, "Bag_count"
, "Bag_empty"
, "Bag_inter_min"
, "Bag_sng"
, "Bag_sub"
, "Bag_union"
, "Bag_union_max"
, "strLen"
]
--------------------------------------------------------------------------------
-- | LH Primitive TyCons -------------------------------------------------------
--------------------------------------------------------------------------------
dictionaryVar :: Var
dictionaryVar = stringVar "tmp_dictionary_var" (Ghc.ForAllTy (Ghc.Bndr dictionaryTyVar Required) $ Ghc.TyVarTy dictionaryTyVar)
dictionaryTyVar :: TyVar
dictionaryTyVar = stringTyVar "da"
dictionaryBind :: Bind Var
dictionaryBind = Rec [(v, Lam a $ App (Var v) (Type $ Ghc.TyVarTy a))]
where
v = dictionaryVar
a = dictionaryTyVar
-----------------------------------------------------------------------
-- | LH Primitive TyCons ----------------------------------------------
-----------------------------------------------------------------------
combineProofsName :: String
combineProofsName = "combineProofs"
proofTyConName :: F.Symbol
proofTyConName = "Proof"
--------------------------------------------------------------------------------
-- | Predicate Types for WiredIns ----------------------------------------------
--------------------------------------------------------------------------------
maxArity :: Arity
maxArity = 7
wiredTyCons :: [TyConP]
wiredTyCons = fst wiredTyDataCons
wiredDataCons :: [Located DataConP]
wiredDataCons = snd wiredTyDataCons
wiredTyDataCons :: ([TyConP] , [Located DataConP])
wiredTyDataCons = (concat tcs, dummyLoc <$> concat dcs)
where
(tcs, dcs) = unzip $ listTyDataCons : map tupleTyDataCons [2..maxArity]
charDataCon :: Located DataConP
charDataCon = dummyLoc (DataConP l0 Ghc.charDataCon [] [] [] [(makeGeneratedLogicLHName "charX",lt)] lt False wiredInName l0)
where
l0 = F.dummyPos "LH.Bare.charTyDataCons"
c = Ghc.charTyCon
lt = rApp c [] [] mempty
listTyDataCons :: ([TyConP] , [DataConP])
listTyDataCons = ( [TyConP l0 c [RTV tyv] [p] [Covariant] [Covariant] (Just fsize)]
, [DataConP l0 Ghc.nilDataCon [RTV tyv] [p] [] [] lt False wiredInName l0
, DataConP l0 Ghc.consDataCon [RTV tyv] [p] [] cargs lt False wiredInName l0])
where
l0 = F.dummyPos "LH.Bare.listTyDataCons"
c = Ghc.listTyCon
[tyv] = tyConTyVarsDef c
t = rVar tyv :: RSort
fld = "fldList"
xHead = "head"
xTail = "tail"
p = PV "p" t (F.vv Nothing) [(t, fld, F.EVar fld)]
px = pdVarReft $ PV "p" t (F.vv Nothing) [(t, fld, F.EVar xHead)]
lt = rApp c [xt] [rPropP [] $ pdVarReft p] mempty
xt = rVar tyv
xst = rApp c [RVar (RTV tyv) px] [rPropP [] $ pdVarReft p] mempty
cargs = map (first makeGeneratedLogicLHName) [(xTail, xst), (xHead, xt)]
fsize = SymSizeFun (dummyLoc "GHC.Types_LHAssumptions.len")
wiredInName :: F.Symbol
wiredInName = "WiredIn"
tupleTyDataCons :: Int -> ([TyConP] , [DataConP])
tupleTyDataCons n = ( [TyConP l0 c (RTV <$> tyvs) ps tyvarinfo pdvarinfo Nothing]
, [DataConP l0 dc (RTV <$> tyvs) ps [] cargs lt False wiredInName l0])
where
tyvarinfo = replicate n Covariant
pdvarinfo = replicate (n-1) Covariant
l0 = F.dummyPos "LH.Bare.tupleTyDataCons"
c = Ghc.tupleTyCon Boxed n
dc = Ghc.tupleDataCon Boxed n
tyvs@(tv:tvs) = tyConTyVarsDef c
(ta:ts) = (rVar <$> tyvs) :: [RSort]
flds = mks "fld_Tuple"
fld = "fld_Tuple"
x1:xs = mks ("x_Tuple" ++ show n)
ps = mkps pnames (ta:ts) ((fld, F.EVar fld) : zip flds (F.EVar <$> flds))
ups = uPVar <$> ps
pxs = mkps pnames (ta:ts) ((fld, F.EVar x1) : zip flds (F.EVar <$> xs))
lt = rApp c (rVar <$> tyvs) (rPropP [] . pdVarReft <$> ups) mempty
xts = zipWith (\v p -> RVar (RTV v) (pdVarReft p)) tvs pxs
cargs = map (first makeGeneratedLogicLHName) $ reverse $ (x1, rVar tv) : zip xs xts
pnames = mks_ "p"
mks x = (\i -> F.symbol (x++ show i)) <$> [1..n]
mks_ x = (\i -> F.symbol (x++ show i)) <$> [2..n]
mkps :: [F.Symbol]
-> [t] -> [(F.Symbol, F.Expr)] -> [PVar t]
mkps ns (t:ts) ((f,x):fxs) = reverse $ mkps_ ns ts fxs [(t, f, x)] []
mkps _ _ _ = panic Nothing "Bare : mkps"
mkps_ :: [F.Symbol]
-> [t]
-> [(F.Symbol, F.Expr)]
-> [(t, F.Symbol, F.Expr)]
-> [PVar t]
-> [PVar t]
mkps_ [] _ _ _ ps = ps
mkps_ (n:ns) (t:ts) ((f, x):xs) args ps = mkps_ ns ts xs (a:args) (p:ps)
where
p = PV n t (F.vv Nothing) args
a = (t, f, x)
mkps_ _ _ _ _ _ = panic Nothing "Bare : mkps_"
--------------------------------------------------------------------------------
isDerivedInstance :: Ghc.ClsInst -> Bool
--------------------------------------------------------------------------------
isDerivedInstance i = F.notracepp ("IS-DERIVED: " ++ F.showpp classSym)
$ S.member classSym derivingClassesSet
where
classSym = F.symbol . Ghc.is_cls $ i
derivingClassesSet :: S.HashSet F.Symbol
derivingClassesSet = S.fromList $ map F.symbol derivingClasses
derivingClasses :: [String]
derivingClasses =
[ show ''Eq
, show ''Ord
, show ''Enum
, show ''Show
, show ''Read
, show ''Monad
, show ''Applicative
, show ''Functor
, show ''Foldable
, show ''Traversable
, show ''Fractional
-- , "GHC.Enum.Bounded"
-- , "GHC.Base.Monoid"
]