{-# 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
  [(Var, LocSpecType, Equation)]
-> Lookup [(Var, LocSpecType, Equation)]
forall a. a -> Either [Error] a
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 ((LocSymbol, Maybe SpecType, Var, CoreExpr)
 -> (Var, LocSpecType, Equation))
-> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
-> [(Var, LocSpecType, Equation)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(LocSymbol, Maybe SpecType, Var, CoreExpr)]
wiDefs [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
-> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
-> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
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 (LocSymbol -> (LocSymbol, Maybe SpecType, Var, CoreExpr))
-> [LocSymbol] -> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
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                      = HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (BareSpec -> HashSet LocSymbol
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 (LocSymbol -> Symbol
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
|| Symbol -> Bool
forall a. Symbolic a => a -> Bool
isMethod (LocSymbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol LocSymbol
x) Bool -> Bool -> Bool
|| Symbol -> Bool
forall a. Symbolic a => a -> Bool
isDictionary (LocSymbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol LocSymbol
x)
                   then (LocSymbol
x, LocSpecType -> SpecType
forall a. Located a -> a
val (LocSpecType -> SpecType) -> Maybe LocSpecType -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> [(Var, LocSpecType)] -> Maybe LocSpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
v [(Var, LocSpecType)]
sigs, Var
v, CoreExpr
e)
                   else Error -> (LocSymbol, Maybe SpecType, Var, CoreExpr)
forall a e. Exception e => e -> a
Ex.throw (Error -> (LocSymbol, Maybe SpecType, Var, CoreExpr))
-> Error -> (LocSymbol, Maybe SpecType, Var, CoreExpr)
forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Char] -> Error
mkError LocSymbol
x ([Char]
"Lifted functions must be exported; please export " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Show a => a -> [Char]
show Var
v)
  Maybe (Var, CoreExpr)
Nothing     -> Error -> (LocSymbol, Maybe SpecType, Var, CoreExpr)
forall a e. Exception e => e -> a
Ex.throw (Error -> (LocSymbol, Maybe SpecType, Var, CoreExpr))
-> Error -> (LocSymbol, Maybe SpecType, Var, CoreExpr)
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       = Env -> ModName -> SourcePos -> LocSpecType -> LocSpecType
forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
Bare.qualifyTop Env
env ModName
name (LocSpecType -> SourcePos
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 (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)

mkError :: LocSymbol -> String -> Error
mkError :: LocSymbol -> [Char] -> Error
mkError LocSymbol
x [Char]
str = SrcSpan -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ LocSymbol -> SourcePos
forall a. Located a -> SourcePos
loc LocSymbol
x) (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
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 = aty at `strengthenRes` F.subst su ref},  Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
F.mkEquation (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
sym) [(Symbol, Sort)]
xts (Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
F.subst Subst
su Expr
le) Sort
out)
  where
    rt :: SpecType
rt    = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar RReft -> SpecType)
-> (SpecType -> RTypeRep RTyCon RTyVar RReft)
-> SpecType
-> SpecType
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_vars :: [(RTVar RTyVar (RRType ()), RReft)]
ty_preds :: [PVar (RRType ())]
ty_binds :: [Symbol]
ty_info :: [RFInfo]
ty_refts :: [RReft]
ty_args :: [SpecType]
ty_res :: SpecType
ty_vars :: forall c tv r. RTypeRep c tv r -> [(RTVar tv (RType c tv ()), r)]
ty_preds :: forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_binds :: forall c tv r. RTypeRep c tv r -> [Symbol]
ty_info :: forall c tv r. RTypeRep c tv r -> [RFInfo]
ty_refts :: forall c tv r. RTypeRep c tv r -> [r]
ty_args :: forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_res :: forall c tv r. RTypeRep c tv r -> RType c tv r
..} ->
                RTypeRep RTyCon RTyVar RReft
trep{ty_info = fmap (\RFInfo
i -> RFInfo
i{permitTC = Just allowTC}) ty_info}) (RTypeRep RTyCon RTyVar RReft -> RTypeRep RTyCon RTyVar RReft)
-> (SpecType -> RTypeRep RTyCon RTyVar RReft)
-> SpecType
-> RTypeRep RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> Maybe SpecType -> SpecType
forall a. a -> Maybe a -> a
Mb.fromMaybe (Type -> SpecType
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   = TCEmb TyCon -> SpecType -> Sort
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RRType ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce (SpecType -> Sort) -> SpecType -> Sort
forall a b. (a -> b) -> a -> b
$ AxiomType -> SpecType
ares AxiomType
at
    xArgs :: [Expr]
xArgs = Symbol -> Expr
F.EVar (Symbol -> Expr)
-> ((Symbol, SpecType) -> Symbol) -> (Symbol, SpecType) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SpecType) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, SpecType) -> Expr) -> [(Symbol, SpecType)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomType -> [(Symbol, SpecType)]
aargs AxiomType
at
    _msg :: [Char]
_msg  = [[Char]] -> [Char]
unwords [LocSymbol -> [Char]
forall a. PPrint a => a -> [Char]
showpp LocSymbol
sym, Maybe SpecType -> [Char]
forall a. PPrint a => a -> [Char]
showpp Maybe SpecType
mbT]
    le :: Expr
le    = case [Var]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> ([Char] -> Error)
-> LogicM Expr
-> Either Error Expr
forall t.
[Var]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> ([Char] -> Error)
-> LogicM t
-> Either Error t
runToLogicWithBoolBinds [Var]
bbs TCEmb TyCon
tce LogicMap
lmap DataConMap
dm [Char] -> Error
forall {t}. [Char] -> TError t
mkErr (Bool -> CoreExpr -> LogicM Expr
coreToLogic Bool
allowTC CoreExpr
def') of
              Right Expr
e -> Expr
e
              Left  Error
e -> Maybe SrcSpan -> [Char] -> Expr
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (Error -> [Char]
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    = SrcSpan -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ LocSymbol -> SourcePos
forall a. Located a -> SourcePos
loc LocSymbol
sym) (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
sym) ([Char] -> Doc
PJ.text [Char]
s)
    bbs :: [Var]
bbs        = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isBoolBind [Var]
xs
    ([Var]
xs, CoreExpr
def') = [Char] -> ([Var], CoreExpr) -> ([Var], CoreExpr)
forall a. Outputable a => [Char] -> a -> a
GM.notracePpr [Char]
"grabBody" (([Var], CoreExpr) -> ([Var], CoreExpr))
-> ([Var], CoreExpr) -> ([Var], CoreExpr)
forall a b. (a -> b) -> a -> b
$ Bool -> Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Bool
allowTC (Type -> Type
Ghc.expandTypeSynonyms Type
τ) (CoreExpr -> ([Var], CoreExpr)) -> CoreExpr -> ([Var], CoreExpr)
forall a b. (a -> b) -> a -> b
$ Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
normalize Bool
allowTC CoreExpr
def
    su :: Subst
su         = [(Symbol, Expr)] -> Subst
F.mkSubst  ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol     (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs) [Expr]
xArgs
                           [(Symbol, Expr)] -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. [a] -> [a] -> [a]
++ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Var -> Symbol
forall t. NamedThing t => t -> Symbol
simplesymbol (Var -> Symbol) -> [Var] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs) [Expr]
xArgs
    xts :: [(Symbol, Sort)]
xts        = [(Symbol -> Symbol
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 (Type -> Sort) -> (SpecType -> Type) -> SpecType -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
Ghc.expandTypeSynonyms (Type -> Type) -> (SpecType -> Type) -> SpecType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> SpecType -> Type
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 ForAllTyBinder
_ 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 ((Var, CoreExpr) -> CoreExpr -> CoreExpr
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
xVar -> [Var] -> [Var]
forall 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]
txs[Var] -> [Var] -> [Var]
forall 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 ((CoreExpr -> CoreExpr -> CoreExpr)
-> CoreExpr -> [CoreExpr] -> CoreExpr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
Ghc.App CoreExpr
e (Var -> CoreExpr
forall b. Var -> Expr b
Ghc.Var (Var -> CoreExpr) -> [Var] -> [CoreExpr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
txs))
         txs :: [Var]
txs      = [ [Char] -> Type -> Var
stringVar ([Char]
"ls" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Arity -> [Char]
forall a. Show a => a -> [Char]
show Arity
i) Type
t |  (Type
t,Arity
i) <- [Type] -> [Arity] -> [(Type, Arity)]
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
txType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
acc) Type
t
        go [Type]
acc Type
t                                           = ([Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
acc, Type
t)


isBoolBind :: Ghc.Var -> Bool
isBoolBind :: Var -> Bool
isBoolBind Var
v = RRType () -> Bool
forall t t1. RType RTyCon t t1 -> Bool
isBool (RTypeRep RTyCon RTyVar () -> RRType ()
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res (RTypeRep RTyCon RTyVar () -> RRType ())
-> RTypeRep RTyCon RTyVar () -> RRType ()
forall a b. (a -> b) -> a -> b
$ RRType () -> RTypeRep RTyCon RTyVar ()
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep ((Type -> RRType ()
forall r. Monoid r => Type -> RRType r
ofType (Type -> RRType ()) -> Type -> RRType ()
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 = SpecType -> SpecType
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)   = RTVU 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 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)     = 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 PVU c tv
p (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
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) = 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
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 RType c tv r -> r -> RType c tv r
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` Reft -> r
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 Var -> Var -> Bool
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 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
y    = CoreExpr
ex
    | Bool
otherwise = Var -> CoreExpr
forall b. Var -> Expr b
Ghc.Var Var
y
  subst (Var, CoreExpr)
su (Ghc.App CoreExpr
f CoreExpr
e)
    = CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
Ghc.App ((Var, CoreExpr) -> CoreExpr -> CoreExpr
forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
f) ((Var, CoreExpr) -> CoreExpr -> CoreExpr
forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e)
  subst (Var, CoreExpr)
su (Ghc.Lam Var
x CoreExpr
e)
    = Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Ghc.Lam Var
x ((Var, CoreExpr) -> CoreExpr -> CoreExpr
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)
    = CoreExpr -> Var -> Type -> [Alt Var] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Ghc.Case ((Var, CoreExpr) -> CoreExpr -> CoreExpr
forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e) Var
x Type
t ((Var, CoreExpr) -> Alt Var -> Alt Var
forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su (Alt Var -> Alt Var) -> [Alt Var] -> [Alt Var]
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)
    = CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Ghc.Let ([(Var, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Ghc.Rec ((CoreExpr -> CoreExpr) -> (Var, CoreExpr) -> (Var, CoreExpr)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd ((Var, CoreExpr) -> CoreExpr -> CoreExpr
forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su) ((Var, CoreExpr) -> (Var, CoreExpr))
-> [(Var, CoreExpr)] -> [(Var, CoreExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, CoreExpr)]
xes)) ((Var, CoreExpr) -> CoreExpr -> CoreExpr
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)
    = CoreBind -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Ghc.Let (Var -> CoreExpr -> CoreBind
forall b. b -> Expr b -> Bind b
Ghc.NonRec Var
x ((Var, CoreExpr) -> CoreExpr -> CoreExpr
forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
ex)) ((Var, CoreExpr) -> CoreExpr -> CoreExpr
forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e)
  subst (Var, CoreExpr)
su (Ghc.Cast CoreExpr
e CoercionR
t)
    = CoreExpr -> CoercionR -> CoreExpr
forall b. Expr b -> CoercionR -> Expr b
Ghc.Cast ((Var, CoreExpr) -> CoreExpr -> CoreExpr
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)
    = CoreTickish -> CoreExpr -> CoreExpr
forall b. CoreTickish -> Expr b -> Expr b
Ghc.Tick CoreTickish
t ((Var, CoreExpr) -> CoreExpr -> CoreExpr
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) = AltCon -> [Var] -> CoreExpr -> Alt Var
forall b. AltCon -> [b] -> Expr b -> Alt b
Ghc.Alt AltCon
c [Var]
xs ((Var, CoreExpr) -> CoreExpr -> CoreExpr
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 ([(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. [a] -> [a]
reverse [(Symbol, SpecType)]
xts) SpecType
res
  where
    (SpecType
to, (Arity
_,[(Symbol, SpecType)]
xts, Just SpecType
res)) = State (Arity, [(Symbol, SpecType)], Maybe SpecType) SpecType
-> (Arity, [(Symbol, SpecType)], Maybe SpecType)
-> (SpecType, (Arity, [(Symbol, SpecType)], Maybe SpecType))
forall s a. State s a -> s -> (a, s)
runState (SpecType
-> State (Arity, [(Symbol, SpecType)], Maybe SpecType) SpecType
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,[], Maybe SpecType
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) = RTVU RTyCon t
-> RType RTyCon t RReft -> RReft -> RType RTyCon t RReft
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU RTyCon t
a (RType RTyCon t RReft -> RReft -> RType RTyCon t RReft)
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RReft -> RType RTyCon t RReft)
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 StateT
  (Arity, [(Symbol, RType RTyCon t RReft)],
   Maybe (RType RTyCon t RReft))
  m
  (RReft -> RType RTyCon t RReft)
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     RReft
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
forall a b.
StateT
  (Arity, [(Symbol, RType RTyCon t RReft)],
   Maybe (RType RTyCon t RReft))
  m
  (a -> b)
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     a
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RReft
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     RReft
forall a.
a
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     a
forall (m :: * -> *) a. Monad m => a -> m a
return RReft
r
    go (RAllP PVU RTyCon t
p RType RTyCon t RReft
t) = PVU RTyCon t -> RType RTyCon t RReft -> RType RTyCon t RReft
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU RTyCon t
p (RType RTyCon t RReft -> RType RTyCon t RReft)
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
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) | RType RTyCon t RReft -> Bool
forall t t1. RType RTyCon t t1 -> Bool
isErasable RType RTyCon t RReft
tx = (\RType RTyCon t RReft
t' -> Symbol
-> RFInfo
-> RType RTyCon t RReft
-> RType RTyCon t RReft
-> RReft
-> RType RTyCon t RReft
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) (RType RTyCon t RReft -> RType RTyCon t RReft)
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
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) <- StateT
  (Arity, [(Symbol, RType RTyCon t RReft)],
   Maybe (RType RTyCon t RReft))
  m
  (Arity, [(Symbol, RType RTyCon t RReft)],
   Maybe (RType RTyCon t RReft))
forall (m :: * -> *) s. Monad m => StateT s m s
get
      let x' :: Symbol
x' = Symbol -> Arity -> Symbol
unDummy Symbol
x Arity
i
      (Arity, [(Symbol, RType RTyCon t RReft)],
 Maybe (RType RTyCon t RReft))
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Arity
iArity -> Arity -> Arity
forall a. Num a => a -> a -> a
+Arity
1, (Symbol
x', RType RTyCon t RReft
tx)(Symbol, RType RTyCon t RReft)
-> [(Symbol, RType RTyCon t RReft)]
-> [(Symbol, RType RTyCon t RReft)]
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
      RType RTyCon t RReft
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
forall a.
a
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (RType RTyCon t RReft
 -> StateT
      (Arity, [(Symbol, RType RTyCon t RReft)],
       Maybe (RType RTyCon t RReft))
      m
      (RType RTyCon t RReft))
-> RType RTyCon t RReft
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     (RType RTyCon t RReft)
forall a b. (a -> b) -> a -> b
$ Symbol
-> RFInfo
-> RType RTyCon t RReft
-> RType RTyCon t RReft
-> RReft
-> RType RTyCon t RReft
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)
_) <- StateT
  (Arity, [(Symbol, RType RTyCon t RReft)],
   Maybe (RType RTyCon t RReft))
  m
  (Arity, [(Symbol, RType RTyCon t RReft)],
   Maybe (RType RTyCon t RReft))
forall (m :: * -> *) s. Monad m => StateT s m s
get
      let ys :: [Symbol]
ys = [Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ ((Symbol, RType RTyCon t RReft) -> Symbol)
-> [(Symbol, RType RTyCon t RReft)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, RType RTyCon t RReft) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, RType RTyCon t RReft)]
bs
      let t' :: RType RTyCon t RReft
t' = RType RTyCon t RReft -> RReft -> RType RTyCon t RReft
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen RType RTyCon t RReft
t (LocSymbol -> [Symbol] -> RReft
forall a. Symbolic a => LocSymbol -> [a] -> RReft
singletonApp LocSymbol
s [Symbol]
ys)
      (Arity, [(Symbol, RType RTyCon t RReft)],
 Maybe (RType RTyCon t RReft))
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Arity
i, [(Symbol, RType RTyCon t RReft)]
bs, RType RTyCon t RReft -> Maybe (RType RTyCon t RReft)
forall a. a -> Maybe a
Just 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)
forall a.
a
-> StateT
     (Arity, [(Symbol, RType RTyCon t RReft)],
      Maybe (RType RTyCon t RReft))
     m
     a
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 RType RTyCon t t1 -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass else RType RTyCon t t1 -> Bool
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 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol
F.dummySymbol = Symbol
x
  | Bool
otherwise          = [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
"lq" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Arity -> [Char]
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 = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft Reft
r Predicate
forall a. Monoid a => a
mempty
  where
    r :: Reft
r             = Expr -> Reft
forall a. Expression a => a -> Reft
F.exprReft (LocSymbol -> [Expr] -> Expr
F.mkEApp LocSymbol
s (a -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (a -> Expr) -> [a] -> [Expr]
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
  [Var] -> Lookup [Var]
forall a. a -> Either [Error] a
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 = Symbol -> LocSymbol
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
    [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
-> Lookup [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (LocSymbol
x, LocSpecType -> SpecType
forall a. Located a -> a
F.val (LocSpecType -> SpecType) -> Maybe LocSpecType -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> [(Var, LocSpecType)] -> Maybe LocSpecType
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 =
    [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
-> Lookup [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
forall a. a -> Either [Error] a
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 (Type -> CoreExpr) -> Type -> CoreExpr
forall a b. (a -> b) -> a -> b
$ Var -> Type
Ghc.varType (Var -> Type) -> Var -> Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Var -> Var
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 = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr Var
gid [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"\n realIdUnfolding = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Unfolding -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (Var -> Unfolding
Ghc.realIdUnfolding Var
gid) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"\n maybeUnfoldingTemplate . realIdUnfolding = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe CoreExpr -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (Unfolding -> Maybe CoreExpr
Ghc.maybeUnfoldingTemplate (Unfolding -> Maybe CoreExpr) -> Unfolding -> Maybe CoreExpr
forall a b. (a -> b) -> a -> b
$ Var -> Unfolding
Ghc.realIdUnfolding Var
gid ) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_src . inlinePragInfo . Ghc.idInfo = "    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SourceText -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> SourceText
Ghc.inl_src (InlinePragma -> SourceText) -> InlinePragma -> SourceText
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
gid) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_inline . inlinePragInfo . Ghc.idInfo = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ InlineSpec -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> InlineSpec
Ghc.inl_inline (InlinePragma -> InlineSpec) -> InlinePragma -> InlineSpec
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
gid) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_sat . inlinePragInfo . Ghc.idInfo = "    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe Arity -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> Maybe Arity
Ghc.inl_sat (InlinePragma -> Maybe Arity) -> InlinePragma -> Maybe Arity
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
gid) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_act . inlinePragInfo . Ghc.idInfo = "    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Activation -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> Activation
Ghc.inl_act (InlinePragma -> Activation) -> InlinePragma -> Activation
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
gid) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_rule . inlinePragInfo . Ghc.idInfo = "   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RuleMatchInfo -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> RuleMatchInfo
Ghc.inl_rule (InlinePragma -> RuleMatchInfo) -> InlinePragma -> RuleMatchInfo
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
gid) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inl_rule rule = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RuleMatchInfo -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> RuleMatchInfo
Ghc.inl_rule (InlinePragma -> RuleMatchInfo) -> InlinePragma -> RuleMatchInfo
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
gid) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      [Char]
"\n inline spec = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ InlineSpec -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (InlinePragma -> InlineSpec
Ghc.inl_inline (InlinePragma -> InlineSpec) -> InlinePragma -> InlineSpec
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
Ghc.inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
gid)
     ) Var
gid
   where
    go :: Type -> CoreExpr
go (Ghc.ForAllTy ForAllTyBinder
a (Ghc.ForAllTy ForAllTyBinder
b (Ghc.ForAllTy ForAllTyBinder
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 Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Ghc.Lam (ForAllTyBinder -> Var
forall tv argf. VarBndr tv argf -> tv
Ghc.binderVar ForAllTyBinder
a) (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$
           Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Ghc.Lam (ForAllTyBinder -> Var
forall tv argf. VarBndr tv argf -> tv
Ghc.binderVar ForAllTyBinder
b) (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$
           Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Ghc.Lam (ForAllTyBinder -> Var
forall tv argf. VarBndr tv argf -> tv
Ghc.binderVar ForAllTyBinder
c) (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$
           Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Ghc.Lam Var
f (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Ghc.Lam Var
g (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Ghc.Lam Var
x (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
Ghc.App (Var -> CoreExpr
forall b. Var -> Expr b
Ghc.Var Var
f) (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
Ghc.App (Var -> CoreExpr
forall b. Var -> Expr b
Ghc.Var Var
g) (Var -> CoreExpr
forall b. Var -> Expr b
Ghc.Var Var
x))
    go Type
_ = [Char] -> CoreExpr
forall a. HasCallStack => [Char] -> a
error [Char]
"Axioms.go"