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

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

-- | This module contains the code that DOES reflection; i.e. converts Haskell
--   definitions into refinements.

module Language.Haskell.Liquid.Bare.Axiom ( makeHaskellAxioms, wiredReflects ) where

import Prelude hiding (error)
import Prelude hiding (mapM)
import qualified Control.Exception         as Ex

-- import           Control.Monad.Except      hiding (forM, mapM)
-- import           Control.Monad.State       hiding (forM, mapM)
import qualified Text.PrettyPrint.HughesPJ as PJ -- (text)
import qualified Data.HashSet              as S
import qualified Data.Maybe                as Mb
import Control.Monad.Trans.State.Lazy (runState, get, put)

import           Language.Fixpoint.Misc
import qualified Language.Haskell.Liquid.Measure as Ms
import qualified Language.Fixpoint.Types as F
import qualified Liquid.GHC.API as Ghc
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Transforms.CoreToLogic
import           Language.Haskell.Liquid.GHC.Misc
import           Language.Haskell.Liquid.Types

import           Language.Haskell.Liquid.Bare.Resolve as Bare
import           Language.Haskell.Liquid.Bare.Types   as Bare

-----------------------------------------------------------------------------------------------
makeHaskellAxioms :: Config -> GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> LogicMap -> GhcSpecSig -> Ms.BareSpec
                  -> Bare.Lookup [(Ghc.Var, LocSpecType, F.Equation)]
-----------------------------------------------------------------------------------------------
makeHaskellAxioms :: Config
-> GhcSrc
-> Env
-> TycEnv
-> ModName
-> LogicMap
-> GhcSpecSig
-> BareSpec
-> Lookup [(Var, LocSpecType, Equation)]
makeHaskellAxioms Config
cfg GhcSrc
src Env
env TycEnv
tycEnv ModName
name LogicMap
lmap GhcSpecSig
spSig BareSpec
spec = do
  [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
wiDefs     <- Config
-> Env
-> ModName
-> GhcSpecSig
-> Lookup [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
wiredDefs Config
cfg Env
env ModName
name GhcSpecSig
spSig
  let refDefs :: [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
refDefs = GhcSrc
-> GhcSpecSig
-> BareSpec
-> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
getReflectDefs GhcSrc
src GhcSpecSig
spSig BareSpec
spec
  forall (m :: * -> *) a. Monad m => a -> m a
return (Env
-> TycEnv
-> ModName
-> LogicMap
-> (LocSymbol, Maybe SpecType, Var, CoreExpr)
-> (Var, LocSpecType, Equation)
makeAxiom Env
env TycEnv
tycEnv ModName
name LogicMap
lmap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(LocSymbol, Maybe SpecType, Var, CoreExpr)]
wiDefs forall a. [a] -> [a] -> [a]
++ [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
refDefs))

getReflectDefs :: GhcSrc -> GhcSpecSig -> Ms.BareSpec
               -> [(LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)]
getReflectDefs :: GhcSrc
-> GhcSpecSig
-> BareSpec
-> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
getReflectDefs GhcSrc
src GhcSpecSig
sig BareSpec
spec = [CoreBind]
-> [(Var, LocSpecType)]
-> LocSymbol
-> (LocSymbol, Maybe SpecType, Var, CoreExpr)
findVarDefType [CoreBind]
cbs [(Var, LocSpecType)]
sigs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
xs
  where
    sigs :: [(Var, LocSpecType)]
sigs                    = GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
sig
    xs :: [LocSymbol]
xs                      = forall a. HashSet a -> [a]
S.toList (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects BareSpec
spec)
    cbs :: [CoreBind]
cbs                     = GhcSrc -> [CoreBind]
_giCbs GhcSrc
src

findVarDefType :: [Ghc.CoreBind] -> [(Ghc.Var, LocSpecType)] -> LocSymbol
               -> (LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)
findVarDefType :: [CoreBind]
-> [(Var, LocSpecType)]
-> LocSymbol
-> (LocSymbol, Maybe SpecType, Var, CoreExpr)
findVarDefType [CoreBind]
cbs [(Var, LocSpecType)]
sigs LocSymbol
x = case Symbol -> [CoreBind] -> Maybe (Var, CoreExpr)
findVarDefMethod (forall a. Located a -> a
val LocSymbol
x) [CoreBind]
cbs of
  -- YL: probably ok even without checking typeclass flag since user cannot
  -- manually reflect internal names
  Just (Var
v, CoreExpr
e) -> if Var -> Bool
GM.isExternalId Var
v Bool -> Bool -> Bool
|| forall a. Symbolic a => a -> Bool
isMethod (forall a. Symbolic a => a -> Symbol
F.symbol LocSymbol
x) Bool -> Bool -> Bool
|| forall a. Symbolic a => a -> Bool
isDictionary (forall a. Symbolic a => a -> Symbol
F.symbol LocSymbol
x)
                   then (LocSymbol
x, forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
v [(Var, LocSpecType)]
sigs, Var
v, CoreExpr
e)
                   else forall a e. Exception e => e -> a
Ex.throw forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Char] -> Error
mkError LocSymbol
x ([Char]
"Lifted functions must be exported; please export " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Var
v)
  Maybe (Var, CoreExpr)
Nothing     -> forall a e. Exception e => e -> a
Ex.throw forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Char] -> Error
mkError LocSymbol
x [Char]
"Cannot lift haskell function"

--------------------------------------------------------------------------------
makeAxiom :: Bare.Env -> Bare.TycEnv -> ModName -> LogicMap
          -> (LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)
          -> (Ghc.Var, LocSpecType, F.Equation)
--------------------------------------------------------------------------------
makeAxiom :: Env
-> TycEnv
-> ModName
-> LogicMap
-> (LocSymbol, Maybe SpecType, Var, CoreExpr)
-> (Var, LocSpecType, Equation)
makeAxiom Env
env TycEnv
tycEnv ModName
name LogicMap
lmap (LocSymbol
x, Maybe SpecType
mbT, Var
v, CoreExpr
def)
            = (Var
v, LocSpecType
t, Equation
e)
  where
    t :: LocSpecType
t       = forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
Bare.qualifyTop Env
env ModName
name (forall a. Located a -> SourcePos
F.loc LocSpecType
t0) LocSpecType
t0
    (LocSpecType
t0, Equation
e) = Bool
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> LocSymbol
-> Maybe SpecType
-> Var
-> CoreExpr
-> (LocSpecType, Equation)
makeAssumeType Bool
allowTC TCEmb TyCon
embs LogicMap
lmap DataConMap
dm LocSymbol
x Maybe SpecType
mbT Var
v CoreExpr
def
    embs :: TCEmb TyCon
embs    = TycEnv -> TCEmb TyCon
Bare.tcEmbs       TycEnv
tycEnv
    dm :: DataConMap
dm      = TycEnv -> DataConMap
Bare.tcDataConMap TycEnv
tycEnv
    allowTC :: Bool
allowTC = Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig Env
env)

mkError :: LocSymbol -> String -> Error
mkError :: LocSymbol -> [Char] -> Error
mkError LocSymbol
x [Char]
str = forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc LocSymbol
x) (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSymbol
x) ([Char] -> Doc
PJ.text [Char]
str)

makeAssumeType
  :: Bool -- ^ typeclass enabled
  -> F.TCEmb Ghc.TyCon -> LogicMap -> DataConMap -> LocSymbol -> Maybe SpecType
  -> Ghc.Var -> Ghc.CoreExpr
  -> (LocSpecType, F.Equation)
makeAssumeType :: Bool
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> LocSymbol
-> Maybe SpecType
-> Var
-> CoreExpr
-> (LocSpecType, Equation)
makeAssumeType Bool
allowTC TCEmb TyCon
tce LogicMap
lmap DataConMap
dm LocSymbol
sym Maybe SpecType
mbT Var
v CoreExpr
def
  = (LocSymbol
sym {val :: SpecType
val = AxiomType -> SpecType
aty AxiomType
at SpecType -> Reft -> SpecType
`strengthenRes` forall a. Subable a => Subst -> a -> a
F.subst Subst
su Reft
ref},  Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
F.mkEquation (forall a. Located a -> a
val LocSymbol
sym) [(Symbol, Sort)]
xts (forall a. Subable a => Subst -> a -> a
F.subst Subst
su Expr
le) Sort
out)
  where
    rt :: SpecType
rt    = forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            (\trep :: RTypeRep RTyCon RTyVar RReft
trep@RTypeRep{[(RTVar RTyVar (RRType ()), RReft)]
[Symbol]
[RReft]
[SpecType]
[PVar (RRType ())]
[RFInfo]
SpecType
ty_res :: forall c tv r. RTypeRep c tv r -> RType c tv r
ty_args :: forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_refts :: forall c tv r. RTypeRep c tv r -> [r]
ty_info :: forall c tv r. RTypeRep c tv r -> [RFInfo]
ty_binds :: forall c tv r. RTypeRep c tv r -> [Symbol]
ty_preds :: forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_vars :: forall c tv r. RTypeRep c tv r -> [(RTVar tv (RType c tv ()), r)]
ty_res :: SpecType
ty_args :: [SpecType]
ty_refts :: [RReft]
ty_info :: [RFInfo]
ty_binds :: [Symbol]
ty_preds :: [PVar (RRType ())]
ty_vars :: [(RTVar RTyVar (RRType ()), RReft)]
..} ->
                RTypeRep RTyCon RTyVar RReft
trep{ty_info :: [RFInfo]
ty_info = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\RFInfo
i -> RFInfo
i{permitTC :: Maybe Bool
permitTC = forall a. a -> Maybe a
Just Bool
allowTC}) [RFInfo]
ty_info}) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
Mb.fromMaybe (forall r. Monoid r => Type -> RRType r
ofType Type
τ) Maybe SpecType
mbT
    τ :: Type
τ     = Var -> Type
Ghc.varType Var
v
    at :: AxiomType
at    = Bool -> LocSymbol -> SpecType -> AxiomType
axiomType Bool
allowTC LocSymbol
sym SpecType
rt
    out :: Sort
out   = forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RRType ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce forall a b. (a -> b) -> a -> b
$ AxiomType -> SpecType
ares AxiomType
at
    xArgs :: [Expr]
xArgs = Symbol -> Expr
F.EVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomType -> [(Symbol, SpecType)]
aargs AxiomType
at
    _msg :: [Char]
_msg  = [[Char]] -> [Char]
unwords [forall a. PPrint a => a -> [Char]
showpp LocSymbol
sym, forall a. PPrint a => a -> [Char]
showpp Maybe SpecType
mbT]
    le :: Expr
le    = case forall t.
[Var]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> ([Char] -> Error)
-> LogicM t
-> Either Error t
runToLogicWithBoolBinds [Var]
bbs TCEmb TyCon
tce LogicMap
lmap DataConMap
dm forall {t}. [Char] -> TError t
mkErr (Bool -> CoreExpr -> LogicM Expr
coreToLogic Bool
allowTC CoreExpr
def') of
              Right Expr
e -> Expr
e
              Left  Error
e -> forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing (forall a. Show a => a -> [Char]
show Error
e)
    ref :: Reft
ref        = (Symbol, Expr) -> Reft
F.Reft (Symbol
F.vv_, Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Eq (Symbol -> Expr
F.EVar Symbol
F.vv_) Expr
le)
    mkErr :: [Char] -> TError t
mkErr [Char]
s    = forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc LocSymbol
sym) (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSymbol
sym) ([Char] -> Doc
PJ.text [Char]
s)
    bbs :: [Var]
bbs        = forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isBoolBind [Var]
xs
    ([Var]
xs, CoreExpr
def') = forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"grabBody" forall a b. (a -> b) -> a -> b
$ Bool -> Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Bool
allowTC (Type -> Type
Ghc.expandTypeSynonyms Type
τ) forall a b. (a -> b) -> a -> b
$ forall a. Simplify a => Bool -> a -> a
normalize Bool
allowTC CoreExpr
def
    su :: Subst
su         = [(Symbol, Expr)] -> Subst
F.mkSubst  forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Symbolic a => a -> Symbol
F.symbol     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs) [Expr]
xArgs
                           forall a. [a] -> [a] -> [a]
++ forall a b. [a] -> [b] -> [(a, b)]
zip (forall t. NamedThing t => t -> Symbol
simplesymbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs) [Expr]
xArgs
    xts :: [(Symbol, Sort)]
xts        = [(forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x, TCEmb TyCon -> SpecType -> Sort
rTypeSortExp TCEmb TyCon
tce SpecType
t) | (Symbol
x, SpecType
t) <- AxiomType -> [(Symbol, SpecType)]
aargs AxiomType
at]

rTypeSortExp :: F.TCEmb Ghc.TyCon -> SpecType -> F.Sort
rTypeSortExp :: TCEmb TyCon -> SpecType -> Sort
rTypeSortExp TCEmb TyCon
tce = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
Ghc.expandTypeSynonyms forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False

grabBody :: Bool -- ^ typeclass enabled
         -> Ghc.Type -> Ghc.CoreExpr -> ([Ghc.Var], Ghc.CoreExpr)
grabBody :: Bool -> Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Bool
allowTC (Ghc.ForAllTy TyCoVarBinder
_ Type
ty) CoreExpr
e
  = Bool -> Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Bool
allowTC Type
ty CoreExpr
e
grabBody allowTC :: Bool
allowTC@Bool
False Ghc.FunTy{ ft_arg :: Type -> Type
Ghc.ft_arg = Type
tx, ft_res :: Type -> Type
Ghc.ft_res = Type
t} CoreExpr
e | Type -> Bool
Ghc.isClassPred Type
tx
  = Bool -> Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Bool
allowTC Type
t CoreExpr
e
grabBody allowTC :: Bool
allowTC@Bool
True Ghc.FunTy{ ft_arg :: Type -> Type
Ghc.ft_arg = Type
tx, ft_res :: Type -> Type
Ghc.ft_res = Type
t} CoreExpr
e | Type -> Bool
isEmbeddedDictType Type
tx
  = Bool -> Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Bool
allowTC Type
t CoreExpr
e
grabBody Bool
allowTC torig :: Type
torig@Ghc.FunTy {} (Ghc.Let (Ghc.NonRec Var
x CoreExpr
e) CoreExpr
body)
  = Bool -> Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Bool
allowTC Type
torig (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var
x,CoreExpr
e) CoreExpr
body)
grabBody Bool
allowTC Ghc.FunTy{ ft_res :: Type -> Type
Ghc.ft_res = Type
t} (Ghc.Lam Var
x CoreExpr
e)
  = (Var
xforall a. a -> [a] -> [a]
:[Var]
xs, CoreExpr
e') where ([Var]
xs, CoreExpr
e') = Bool -> Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Bool
allowTC Type
t CoreExpr
e
grabBody Bool
allowTC Type
t (Ghc.Tick CoreTickish
_ CoreExpr
e)
  = Bool -> Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Bool
allowTC Type
t CoreExpr
e
grabBody Bool
allowTC ty :: Type
ty@Ghc.FunTy{} CoreExpr
e
  = ([Var]
txsforall a. [a] -> [a] -> [a]
++[Var]
xs, CoreExpr
e')
   where ([Type]
ts,Type
tr)  = Type -> ([Type], Type)
splitFun Type
ty
         ([Var]
xs, CoreExpr
e') = Bool -> Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Bool
allowTC Type
tr (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall b. Expr b -> Expr b -> Expr b
Ghc.App CoreExpr
e (forall b. Var -> Expr b
Ghc.Var forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
txs))
         txs :: [Var]
txs      = [ [Char] -> Type -> Var
stringVar ([Char]
"ls" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Arity
i) Type
t |  (Type
t,Arity
i) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
ts [(Arity
1::Int)..]]
grabBody Bool
_ Type
_ CoreExpr
e
  = ([], CoreExpr
e)

splitFun :: Ghc.Type -> ([Ghc.Type], Ghc.Type)
splitFun :: Type -> ([Type], Type)
splitFun = [Type] -> Type -> ([Type], Type)
go []
  where go :: [Type] -> Type -> ([Type], Type)
go [Type]
acc Ghc.FunTy{ ft_arg :: Type -> Type
Ghc.ft_arg = Type
tx, ft_res :: Type -> Type
Ghc.ft_res = Type
t} = [Type] -> Type -> ([Type], Type)
go (Type
txforall a. a -> [a] -> [a]
:[Type]
acc) Type
t
        go [Type]
acc Type
t                                           = (forall a. [a] -> [a]
reverse [Type]
acc, Type
t)


isBoolBind :: Ghc.Var -> Bool
isBoolBind :: Var -> Bool
isBoolBind Var
v = forall t t1. RType RTyCon t t1 -> Bool
isBool (forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep ((forall r. Monoid r => Type -> RRType r
ofType forall a b. (a -> b) -> a -> b
$ Var -> Type
Ghc.varType Var
v) :: RRType ()))

strengthenRes :: SpecType -> F.Reft -> SpecType
strengthenRes :: SpecType -> Reft -> SpecType
strengthenRes SpecType
st Reft
rf = forall {r} {c} {tv}. Reftable r => RType c tv r -> RType c tv r
go SpecType
st
  where
    go :: RType c tv r -> RType c tv r
go (RAllT RTVU c tv
a RType c tv r
t r
r)   = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a (RType c tv r -> RType c tv r
go RType c tv r
t) r
r
    go (RAllP PVU c tv
p RType c tv r
t)     = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
p forall a b. (a -> b) -> a -> b
$ RType c tv r -> RType c tv r
go RType c tv r
t
    go (RFun Symbol
x RFInfo
i RType c tv r
tx RType c tv r
t r
r) = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i RType c tv r
tx (RType c tv r -> RType c tv r
go RType c tv r
t) r
r
    go RType c tv r
t               =  RType c tv r
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. Reftable r => Reft -> r
F.ofReft Reft
rf

class Subable a where
  subst :: (Ghc.Var, Ghc.CoreExpr) -> a -> a

instance Subable Ghc.Var where
  subst :: (Var, CoreExpr) -> Var -> Var
subst (Var
x, CoreExpr
ex) Var
z
    | Var
x forall a. Eq a => a -> a -> Bool
== Var
z, Ghc.Var Var
y <- CoreExpr
ex = Var
y
    | Bool
otherwise           = Var
z

instance Subable Ghc.CoreExpr where
  subst :: (Var, CoreExpr) -> CoreExpr -> CoreExpr
subst (Var
x, CoreExpr
ex) (Ghc.Var Var
y)
    | Var
x forall a. Eq a => a -> a -> Bool
== Var
y    = CoreExpr
ex
    | Bool
otherwise = forall b. Var -> Expr b
Ghc.Var Var
y
  subst (Var, CoreExpr)
su (Ghc.App CoreExpr
f CoreExpr
e)
    = forall b. Expr b -> Expr b -> Expr b
Ghc.App (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
f) (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e)
  subst (Var, CoreExpr)
su (Ghc.Lam Var
x CoreExpr
e)
    = forall b. b -> Expr b -> Expr b
Ghc.Lam Var
x (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e)
  subst (Var, CoreExpr)
su (Ghc.Case CoreExpr
e Var
x Type
t [Alt Var]
alts)
    = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Ghc.Case (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e) Var
x Type
t (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Alt Var]
alts)
  subst (Var, CoreExpr)
su (Ghc.Let (Ghc.Rec [(Var, CoreExpr)]
xes) CoreExpr
e)
    = forall b. Bind b -> Expr b -> Expr b
Ghc.Let (forall b. [(b, Expr b)] -> Bind b
Ghc.Rec (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, CoreExpr)]
xes)) (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e)
  subst (Var, CoreExpr)
su (Ghc.Let (Ghc.NonRec Var
x CoreExpr
ex) CoreExpr
e)
    = forall b. Bind b -> Expr b -> Expr b
Ghc.Let (forall b. b -> Expr b -> Bind b
Ghc.NonRec Var
x (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
ex)) (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e)
  subst (Var, CoreExpr)
su (Ghc.Cast CoreExpr
e CoercionR
t)
    = forall b. Expr b -> CoercionR -> Expr b
Ghc.Cast (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e) CoercionR
t
  subst (Var, CoreExpr)
su (Ghc.Tick CoreTickish
t CoreExpr
e)
    = forall b. CoreTickish -> Expr b -> Expr b
Ghc.Tick CoreTickish
t (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e)
  subst (Var, CoreExpr)
_ CoreExpr
e
    = CoreExpr
e

instance Subable Ghc.CoreAlt where
  subst :: (Var, CoreExpr) -> Alt Var -> Alt Var
subst (Var, CoreExpr)
su (Ghc.Alt AltCon
c [Var]
xs CoreExpr
e) = forall b. AltCon -> [b] -> Expr b -> Alt b
Ghc.Alt AltCon
c [Var]
xs (forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e)

data AxiomType = AT { AxiomType -> SpecType
aty :: SpecType, AxiomType -> [(Symbol, SpecType)]
aargs :: [(F.Symbol, SpecType)], AxiomType -> SpecType
ares :: SpecType }

-- | Specification for Haskell function
axiomType :: Bool -> LocSymbol -> SpecType -> AxiomType
axiomType :: Bool -> LocSymbol -> SpecType -> AxiomType
axiomType Bool
allowTC LocSymbol
s SpecType
st = SpecType -> [(Symbol, SpecType)] -> SpecType -> AxiomType
AT SpecType
to (forall a. [a] -> [a]
reverse [(Symbol, SpecType)]
xts) SpecType
res
  where
    (SpecType
to, (Arity
_,[(Symbol, SpecType)]
xts, Just SpecType
res)) = forall s a. State s a -> s -> (a, s)
runState (forall {m :: * -> *} {t}.
Monad m =>
RType RTyCon t RReft
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
go SpecType
st) (Arity
1,[], forall a. Maybe a
Nothing)
    go :: RType RTyCon t RReft
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
go (RAllT RTVU RTyCon t
a RType RTyCon t RReft
t RReft
r) = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU RTyCon t
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RType RTyCon t RReft
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
go RType RTyCon t RReft
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return RReft
r
    go (RAllP PVU RTyCon t
p RType RTyCon t RReft
t) = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU RTyCon t
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RType RTyCon t RReft
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
go RType RTyCon t RReft
t
    go (RFun Symbol
x RFInfo
i RType RTyCon t RReft
tx RType RTyCon t RReft
t RReft
r) | forall t t1. RType RTyCon t t1 -> Bool
isErasable RType RTyCon t RReft
tx = (\RType RTyCon t RReft
t' -> forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i RType RTyCon t RReft
tx RType RTyCon t RReft
t' RReft
r) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RType RTyCon t RReft
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
go RType RTyCon t RReft
t
    go (RFun Symbol
x RFInfo
ii RType RTyCon t RReft
tx RType RTyCon t RReft
t RReft
r) = do
      (Arity
i,[(Symbol, RType RTyCon t RReft)]
bs,Maybe (RType RTyCon t RReft)
mres) <- forall (m :: * -> *) s. Monad m => StateT s m s
get
      let x' :: Symbol
x' = Symbol -> Arity -> Symbol
unDummy Symbol
x Arity
i
      forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Arity
iforall a. Num a => a -> a -> a
+Arity
1, (Symbol
x', RType RTyCon t RReft
tx)forall a. a -> [a] -> [a]
:[(Symbol, RType RTyCon t RReft)]
bs,Maybe (RType RTyCon t RReft)
mres)
      RType RTyCon t RReft
t' <- RType RTyCon t RReft
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
go RType RTyCon t RReft
t
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x' RFInfo
ii RType RTyCon t RReft
tx RType RTyCon t RReft
t' RReft
r
    go RType RTyCon t RReft
t = do
      (Arity
i,[(Symbol, RType RTyCon t RReft)]
bs,Maybe (RType RTyCon t RReft)
_) <- forall (m :: * -> *) s. Monad m => StateT s m s
get
      let ys :: [Symbol]
ys = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Symbol, RType RTyCon t RReft)]
bs
      let t' :: RType RTyCon t RReft
t' = forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen RType RTyCon t RReft
t (forall a. Symbolic a => LocSymbol -> [a] -> RReft
singletonApp LocSymbol
s [Symbol]
ys)
      forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Arity
i, [(Symbol, RType RTyCon t RReft)]
bs, forall a. a -> Maybe a
Just RType RTyCon t RReft
t')
      forall (m :: * -> *) a. Monad m => a -> m a
return RType RTyCon t RReft
t'
    isErasable :: RType RTyCon t t1 -> Bool
isErasable = if Bool
allowTC then forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass else forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType
unDummy :: F.Symbol -> Int -> F.Symbol
unDummy :: Symbol -> Arity -> Symbol
unDummy Symbol
x Arity
i
  | Symbol
x forall a. Eq a => a -> a -> Bool
/= Symbol
F.dummySymbol = Symbol
x
  | Bool
otherwise          = forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
"lq" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Arity
i)

singletonApp :: F.Symbolic a => LocSymbol -> [a] -> UReft F.Reft
singletonApp :: forall a. Symbolic a => LocSymbol -> [a] -> RReft
singletonApp LocSymbol
s [a]
ys = forall r. r -> Predicate -> UReft r
MkUReft Reft
r forall a. Monoid a => a
mempty
  where
    r :: Reft
r             = forall a. Expression a => a -> Reft
F.exprReft (LocSymbol -> [Expr] -> Expr
F.mkEApp LocSymbol
s (forall a. Symbolic a => a -> Expr
F.eVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
ys))


-------------------------------------------------------------------------------
-- | Hardcode imported reflected functions ------------------------------------
-------------------------------------------------------------------------------

wiredReflects :: Config -> Bare.Env -> ModName -> GhcSpecSig ->
                 Bare.Lookup [Ghc.Var]
wiredReflects :: Config -> Env -> ModName -> GhcSpecSig -> Lookup [Var]
wiredReflects Config
cfg Env
env ModName
name GhcSpecSig
sigs = do
  [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
vs <- Config
-> Env
-> ModName
-> GhcSpecSig
-> Lookup [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
wiredDefs Config
cfg Env
env ModName
name GhcSpecSig
sigs
  forall (m :: * -> *) a. Monad m => a -> m a
return [Var
v | (LocSymbol
_, Maybe SpecType
_, Var
v, CoreExpr
_) <- [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
vs]

wiredDefs :: Config -> Bare.Env -> ModName -> GhcSpecSig
          -> Bare.Lookup [(LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)]
wiredDefs :: Config
-> Env
-> ModName
-> GhcSpecSig
-> Lookup [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
wiredDefs Config
cfg Env
env ModName
name GhcSpecSig
spSig
  | Config -> Bool
reflection Config
cfg = do
    let x :: LocSymbol
x = forall a. a -> Located a
F.dummyLoc Symbol
functionComposisionSymbol
    Var
v    <- Env -> ModName -> [Char] -> LocSymbol -> Lookup Var
Bare.lookupGhcVar Env
env ModName
name [Char]
"wiredAxioms" LocSymbol
x
    forall (m :: * -> *) a. Monad m => a -> m a
return [ (LocSymbol
x, forall a. Located a -> a
F.val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
v (GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
spSig), Var
v, Var -> CoreExpr
makeCompositionExpression Var
v) ]
  | Bool
otherwise =
    forall (m :: * -> *) a. Monad m => a -> m a
return []

-------------------------------------------------------------------------------
-- | Expression Definitions of Prelude Functions ------------------------------
-- | NV: Currently Just Hacking Composition       -----------------------------
-------------------------------------------------------------------------------


makeCompositionExpression :: Ghc.Id -> Ghc.CoreExpr
makeCompositionExpression :: Var -> CoreExpr
makeCompositionExpression Var
gid
  =  Type -> CoreExpr
go forall a b. (a -> b) -> a -> b
$ Var -> Type
Ghc.varType forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => [Char] -> a -> a
F.notracepp ( -- tracing to find  the body of . from the inline spec,
                                      -- replace F.notrace with F.trace to print
      [Char]
"\nv = " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr Var
gid forall a. [a] -> [a] -> [a]
++
      [Char]
"\n realIdUnfolding = " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr (Var -> Unfolding
Ghc.realIdUnfolding Var
gid) forall a. [a] -> [a] -> [a]
++
      [Char]
"\n maybeUnfoldingTemplate . realIdUnfolding = " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr (Unfolding -> Maybe CoreExpr
Ghc.maybeUnfoldingTemplate forall a b. (a -> b) -> a -> b
$ Var -> Unfolding
Ghc.realIdUnfolding Var
gid ) forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_src . inlinePragInfo . Ghc.idInfo = "    forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> SourceText
Ghc.inl_src forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Ghc.idInfo Var
gid) forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_inline . inlinePragInfo . Ghc.idInfo = " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> InlineSpec
Ghc.inl_inline forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Ghc.idInfo Var
gid) forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_sat . inlinePragInfo . Ghc.idInfo = "    forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> Maybe Arity
Ghc.inl_sat forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Ghc.idInfo Var
gid) forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_act . inlinePragInfo . Ghc.idInfo = "    forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> Activation
Ghc.inl_act forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Ghc.idInfo Var
gid) forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_rule . inlinePragInfo . Ghc.idInfo = "   forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> RuleMatchInfo
Ghc.inl_rule forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Ghc.idInfo Var
gid) forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_rule rule = " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> RuleMatchInfo
Ghc.inl_rule forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Ghc.idInfo Var
gid) forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inline spec = " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> InlineSpec
Ghc.inl_inline forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Ghc.idInfo Var
gid)
     ) Var
gid
   where
    go :: Type -> CoreExpr
go (Ghc.ForAllTy TyCoVarBinder
a (Ghc.ForAllTy TyCoVarBinder
b (Ghc.ForAllTy TyCoVarBinder
c Ghc.FunTy{ ft_arg :: Type -> Type
Ghc.ft_arg = Type
tf, ft_res :: Type -> Type
Ghc.ft_res = Ghc.FunTy { ft_arg :: Type -> Type
Ghc.ft_arg = Type
tg, ft_res :: Type -> Type
Ghc.ft_res = Type
tx}})))
      = let f :: Var
f = [Char] -> Type -> Var
stringVar [Char]
"f" Type
tf
            g :: Var
g = [Char] -> Type -> Var
stringVar [Char]
"g" Type
tg
            x :: Var
x = [Char] -> Type -> Var
stringVar [Char]
"x" Type
tx
        in forall b. b -> Expr b -> Expr b
Ghc.Lam (forall tv argf. VarBndr tv argf -> tv
Ghc.binderVar TyCoVarBinder
a) forall a b. (a -> b) -> a -> b
$
           forall b. b -> Expr b -> Expr b
Ghc.Lam (forall tv argf. VarBndr tv argf -> tv
Ghc.binderVar TyCoVarBinder
b) forall a b. (a -> b) -> a -> b
$
           forall b. b -> Expr b -> Expr b
Ghc.Lam (forall tv argf. VarBndr tv argf -> tv
Ghc.binderVar TyCoVarBinder
c) forall a b. (a -> b) -> a -> b
$
           forall b. b -> Expr b -> Expr b
Ghc.Lam Var
f forall a b. (a -> b) -> a -> b
$ forall b. b -> Expr b -> Expr b
Ghc.Lam Var
g forall a b. (a -> b) -> a -> b
$ forall b. b -> Expr b -> Expr b
Ghc.Lam Var
x forall a b. (a -> b) -> a -> b
$ forall b. Expr b -> Expr b -> Expr b
Ghc.App (forall b. Var -> Expr b
Ghc.Var Var
f) (forall b. Expr b -> Expr b -> Expr b
Ghc.App (forall b. Var -> Expr b
Ghc.Var Var
g) (forall b. Var -> Expr b
Ghc.Var Var
x))
    go Type
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Axioms.go"