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

-- | 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 Language.Haskell.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


import IdInfo
import BasicTypes

-----------------------------------------------------------------------------------------------
makeHaskellAxioms :: Config -> GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> LogicMap -> GhcSpecSig -> Ms.BareSpec 
                  -> [(Ghc.Var, LocSpecType, F.Equation)]
-----------------------------------------------------------------------------------------------
makeHaskellAxioms :: Config
-> GhcSrc
-> Env
-> TycEnv
-> ModName
-> LogicMap
-> GhcSpecSig
-> BareSpec
-> [(Var, LocSpecType, Equation)]
makeHaskellAxioms Config
cfg GhcSrc
src Env
env TycEnv
tycEnv ModName
name LogicMap
lmap GhcSpecSig
spSig BareSpec
spec 
  = ((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
fmap (Env
-> TycEnv
-> ModName
-> LogicMap
-> (LocSymbol, Maybe SpecType, Var, CoreExpr)
-> (Var, LocSpecType, Equation)
makeAxiom Env
env TycEnv
tycEnv ModName
name LogicMap
lmap) 
         (Config
-> Env
-> ModName
-> GhcSpecSig
-> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
wiredDefs Config
cfg Env
env ModName
name GhcSpecSig
spSig [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
-> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
-> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
forall a. [a] -> [a] -> [a]
++ GhcSrc
-> GhcSpecSig
-> BareSpec
-> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
getReflectDefs GhcSrc
src GhcSpecSig
spSig BareSpec
spec) 

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)
findVarDef (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) [CoreBind]
cbs of
  Just (Var
v, CoreExpr
e) -> if Var -> Bool
Ghc.isExportedId Var
v
                   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 -> String -> Error
mkError LocSymbol
x (String
"Lifted functions must be exported; please export " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Var -> String
forall a. Show a => a -> String
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 -> String -> Error
mkError LocSymbol
x String
"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) = TCEmb TyCon
-> LogicMap
-> DataConMap
-> LocSymbol
-> Maybe SpecType
-> Var
-> CoreExpr
-> (LocSpecType, Equation)
makeAssumeType 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 

mkError :: LocSymbol -> String -> Error
mkError :: LocSymbol -> String -> Error
mkError LocSymbol
x String
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) (String -> Doc
PJ.text String
str)

makeAssumeType
  :: F.TCEmb Ghc.TyCon -> LogicMap -> DataConMap -> LocSymbol -> Maybe SpecType
  -> Ghc.Var -> Ghc.CoreExpr
  -> (LocSpecType, F.Equation)
makeAssumeType :: TCEmb TyCon
-> LogicMap
-> DataConMap
-> LocSymbol
-> Maybe SpecType
-> Var
-> CoreExpr
-> (LocSpecType, Equation)
makeAssumeType TCEmb TyCon
tce LogicMap
lmap DataConMap
dm LocSymbol
x Maybe SpecType
mbT Var
v CoreExpr
def
  = (LocSymbol
x {val :: SpecType
val = AxiomType -> SpecType
aty AxiomType
at SpecType -> Reft -> SpecType
`strengthenRes` Subst -> Reft -> Reft
forall a. Subable a => Subst -> a -> a
F.subst Subst
su Reft
ref},  Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
F.mkEquation (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) [(Symbol, Sort)]
xts (Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
F.subst Subst
su Expr
le) Sort
out)
  where
    t :: SpecType
t     = 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    = LocSymbol -> SpecType -> AxiomType
axiomType LocSymbol
x SpecType
t
    out :: Sort
out   = TCEmb TyCon -> SpecType -> Sort
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) 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 :: String
_msg  = [String] -> String
unwords [LocSymbol -> String
forall a. PPrint a => a -> String
showpp LocSymbol
x, Maybe SpecType -> String
forall a. PPrint a => a -> String
showpp Maybe SpecType
mbT]
    le :: Expr
le    = case [Var]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> (String -> Error)
-> LogicM Expr
-> Either Error Expr
forall t.
[Var]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> (String -> Error)
-> LogicM t
-> Either Error t
runToLogicWithBoolBinds [Var]
bbs TCEmb TyCon
tce LogicMap
lmap DataConMap
dm String -> Error
forall t. String -> TError t
mkErr (CoreExpr -> LogicM Expr
coreToLogic  CoreExpr
def') of
              Right Expr
e -> Expr
e
              Left  Error
e -> Maybe SrcSpan -> String -> Expr
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (Error -> String
forall a. Show a => a -> String
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 :: String -> TError t
mkErr String
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
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) (String -> Doc
PJ.text String
s)
    bbs :: [Var]
bbs        = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isBoolBind [Var]
xs
    ([Var]
xs, CoreExpr
def') = Type -> CoreExpr -> ([Var], CoreExpr)
grabBody (Type -> Type
Ghc.expandTypeSynonyms Type
τ) (CoreExpr -> ([Var], CoreExpr)) -> CoreExpr -> ([Var], CoreExpr)
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
normalize 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
. SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType

grabBody :: Ghc.Type -> Ghc.CoreExpr -> ([Ghc.Var], Ghc.CoreExpr)
grabBody :: Type -> CoreExpr -> ([Var], CoreExpr)
grabBody (Ghc.ForAllTy TyCoVarBinder
_ Type
t) CoreExpr
e 
  = Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Type
t CoreExpr
e 
grabBody (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 
  = Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Type
t CoreExpr
e 
grabBody (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') = Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Type
t CoreExpr
e
grabBody Type
t (Ghc.Tick Tickish Var
_ CoreExpr
e) 
  = Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Type
t CoreExpr
e
grabBody t :: Type
t@(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
t 
         ([Var]
xs, CoreExpr
e') = Type -> CoreExpr -> ([Var], CoreExpr)
grabBody Type
tr ((CoreExpr -> CoreExpr -> CoreExpr)
-> CoreExpr -> [CoreExpr] -> CoreExpr
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      = [ String -> Type -> Var
stringVar (String
"ls" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i) Type
t |  (Type
t,Integer
i) <- [Type] -> [Integer] -> [(Type, Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
ts [Integer
1..]]
grabBody 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 = RType RTyCon RTyVar () -> Bool
forall t t1. RType RTyCon t t1 -> Bool
isBool (RTypeRep RTyCon RTyVar () -> RType RTyCon RTyVar ()
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res (RTypeRep RTyCon RTyVar () -> RType RTyCon RTyVar ())
-> RTypeRep RTyCon RTyVar () -> RType RTyCon RTyVar ()
forall a b. (a -> b) -> a -> b
$ RType RTyCon RTyVar () -> RTypeRep RTyCon RTyVar ()
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep ((Type -> RType RTyCon RTyVar ()
forall r. Monoid r => Type -> RRType r
ofType (Type -> RType RTyCon RTyVar ()) -> Type -> RType RTyCon RTyVar ()
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
t Reft
r = SpecType -> SpecType
forall r c tv. Reftable r => RType c tv r -> RType c tv r
go SpecType
t 
  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 RType c tv r
tx RType c tv r
t r
r) = Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x 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
r 

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 Coercion
t)
    = CoreExpr -> Coercion -> CoreExpr
forall b. Expr b -> Coercion -> Expr b
Ghc.Cast ((Var, CoreExpr) -> CoreExpr -> CoreExpr
forall a. Subable a => (Var, CoreExpr) -> a -> a
subst (Var, CoreExpr)
su CoreExpr
e) Coercion
t
  subst (Var, CoreExpr)
su (Ghc.Tick Tickish Var
t CoreExpr
e)
    = Tickish Var -> CoreExpr -> CoreExpr
forall b. Tickish Var -> Expr b -> Expr b
Ghc.Tick Tickish Var
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 (AltCon
c, [Var]
xs, CoreExpr
e) = (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 :: LocSymbol -> SpecType -> AxiomType
axiomType :: LocSymbol -> SpecType -> AxiomType
axiomType LocSymbol
s SpecType
t = 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, (Int
_,[(Symbol, SpecType)]
xts, Just SpecType
res)) = State (Int, [(Symbol, SpecType)], Maybe SpecType) SpecType
-> (Int, [(Symbol, SpecType)], Maybe SpecType)
-> (SpecType, (Int, [(Symbol, SpecType)], Maybe SpecType))
forall s a. State s a -> s -> (a, s)
runState (SpecType
-> State (Int, [(Symbol, SpecType)], Maybe SpecType) SpecType
forall (m :: * -> *) c tv.
(Monad m, TyConable c) =>
RType c tv (UReft Reft)
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
go SpecType
t) (Int
1,[], Maybe SpecType
forall a. Maybe a
Nothing)
    go :: RType c tv (UReft Reft)
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
go (RAllT RTVU c tv
a RType c tv (UReft Reft)
t UReft Reft
r) = RTVU c tv
-> RType c tv (UReft Reft) -> UReft Reft -> RType c tv (UReft Reft)
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a (RType c tv (UReft Reft) -> UReft Reft -> RType c tv (UReft Reft))
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (UReft Reft -> RType c tv (UReft Reft))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RType c tv (UReft Reft)
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
go RType c tv (UReft Reft)
t StateT
  (Int, [(Symbol, RType c tv (UReft Reft))],
   Maybe (RType c tv (UReft Reft)))
  m
  (UReft Reft -> RType c tv (UReft Reft))
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (UReft Reft)
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UReft Reft
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (UReft Reft)
forall (m :: * -> *) a. Monad m => a -> m a
return UReft Reft
r 
    go (RAllP PVU c tv
p RType c tv (UReft Reft)
t) = PVU c tv -> RType c tv (UReft Reft) -> RType c tv (UReft Reft)
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
p (RType c tv (UReft Reft) -> RType c tv (UReft Reft))
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RType c tv (UReft Reft)
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
go RType c tv (UReft Reft)
t 
    go (RFun Symbol
x RType c tv (UReft Reft)
tx RType c tv (UReft Reft)
t UReft Reft
r) | RType c tv (UReft Reft) -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType c tv (UReft Reft)
tx = (\RType c tv (UReft Reft)
t' -> Symbol
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
-> UReft Reft
-> RType c tv (UReft Reft)
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RType c tv (UReft Reft)
tx RType c tv (UReft Reft)
t' UReft Reft
r) (RType c tv (UReft Reft) -> RType c tv (UReft Reft))
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RType c tv (UReft Reft)
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
go RType c tv (UReft Reft)
t
    go (RFun Symbol
x RType c tv (UReft Reft)
tx RType c tv (UReft Reft)
t UReft Reft
r) = do 
      (Int
i,[(Symbol, RType c tv (UReft Reft))]
bs,Maybe (RType c tv (UReft Reft))
res) <- StateT
  (Int, [(Symbol, RType c tv (UReft Reft))],
   Maybe (RType c tv (UReft Reft)))
  m
  (Int, [(Symbol, RType c tv (UReft Reft))],
   Maybe (RType c tv (UReft Reft)))
forall (m :: * -> *) s. Monad m => StateT s m s
get 
      let x' :: Symbol
x' = Symbol -> Int -> Symbol
unDummy Symbol
x Int
i 
      (Int, [(Symbol, RType c tv (UReft Reft))],
 Maybe (RType c tv (UReft Reft)))
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, (Symbol
x', RType c tv (UReft Reft)
tx)(Symbol, RType c tv (UReft Reft))
-> [(Symbol, RType c tv (UReft Reft))]
-> [(Symbol, RType c tv (UReft Reft))]
forall a. a -> [a] -> [a]
:[(Symbol, RType c tv (UReft Reft))]
bs,Maybe (RType c tv (UReft Reft))
res)
      RType c tv (UReft Reft)
t' <- RType c tv (UReft Reft)
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
go RType c tv (UReft Reft)
t 
      RType c tv (UReft Reft)
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
forall (m :: * -> *) a. Monad m => a -> m a
return (RType c tv (UReft Reft)
 -> StateT
      (Int, [(Symbol, RType c tv (UReft Reft))],
       Maybe (RType c tv (UReft Reft)))
      m
      (RType c tv (UReft Reft)))
-> RType c tv (UReft Reft)
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
forall a b. (a -> b) -> a -> b
$ Symbol
-> RType c tv (UReft Reft)
-> RType c tv (UReft Reft)
-> UReft Reft
-> RType c tv (UReft Reft)
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x' RType c tv (UReft Reft)
tx RType c tv (UReft Reft)
t' UReft Reft
r 
    go RType c tv (UReft Reft)
t = do 
      (Int
i,[(Symbol, RType c tv (UReft Reft))]
bs,Maybe (RType c tv (UReft Reft))
_) <- StateT
  (Int, [(Symbol, RType c tv (UReft Reft))],
   Maybe (RType c tv (UReft Reft)))
  m
  (Int, [(Symbol, RType c tv (UReft Reft))],
   Maybe (RType c tv (UReft Reft)))
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 c tv (UReft Reft)) -> Symbol)
-> [(Symbol, RType c tv (UReft Reft))] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, RType c tv (UReft Reft)) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, RType c tv (UReft Reft))]
bs
      let t' :: RType c tv (UReft Reft)
t' = RType c tv (UReft Reft) -> UReft Reft -> RType c tv (UReft Reft)
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen RType c tv (UReft Reft)
t (LocSymbol -> [Symbol] -> UReft Reft
forall a. Symbolic a => LocSymbol -> [a] -> UReft Reft
singletonApp LocSymbol
s [Symbol]
ys)
      (Int, [(Symbol, RType c tv (UReft Reft))],
 Maybe (RType c tv (UReft Reft)))
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int
i, [(Symbol, RType c tv (UReft Reft))]
bs, RType c tv (UReft Reft) -> Maybe (RType c tv (UReft Reft))
forall a. a -> Maybe a
Just RType c tv (UReft Reft)
t')
      RType c tv (UReft Reft)
-> StateT
     (Int, [(Symbol, RType c tv (UReft Reft))],
      Maybe (RType c tv (UReft Reft)))
     m
     (RType c tv (UReft Reft))
forall (m :: * -> *) a. Monad m => a -> m a
return RType c tv (UReft Reft)
t' 

unDummy :: F.Symbol -> Int -> F.Symbol
unDummy :: Symbol -> Int -> Symbol
unDummy Symbol
x Int
i
  | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol
F.dummySymbol = Symbol
x
  | Bool
otherwise          = String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String
"lq" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)

singletonApp :: F.Symbolic a => LocSymbol -> [a] -> UReft F.Reft
singletonApp :: LocSymbol -> [a] -> UReft Reft
singletonApp LocSymbol
s [a]
ys = Reft -> Predicate -> UReft Reft
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 
              -> [Ghc.Var]
wiredReflects :: Config -> Env -> ModName -> GhcSpecSig -> [Var]
wiredReflects Config
cfg Env
env ModName
name GhcSpecSig
sigs = [Var
v | (LocSymbol
_, Maybe SpecType
_, Var
v, CoreExpr
_) <- Config
-> Env
-> ModName
-> GhcSpecSig
-> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
wiredDefs Config
cfg Env
env ModName
name GhcSpecSig
sigs ]


wiredDefs :: Config -> Bare.Env -> ModName -> GhcSpecSig 
          -> [(LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)]
wiredDefs :: Config
-> Env
-> ModName
-> GhcSpecSig
-> [(LocSymbol, Maybe SpecType, Var, CoreExpr)]
wiredDefs Config
cfg Env
env ModName
name GhcSpecSig
spSig
  | Config -> Bool
reflection Config
cfg 
  = [ (LocSymbol, Maybe SpecType, Var, CoreExpr)
functionCompositionDef ]
  | Bool
otherwise
  = []
  where 
    functionCompositionDef :: (LocSymbol, Maybe SpecType, Var, CoreExpr)
functionCompositionDef = (LocSymbol
x, (LocSpecType -> SpecType) -> Maybe LocSpecType -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LocSpecType -> SpecType
forall a. Located a -> a
F.val (Maybe LocSpecType -> Maybe SpecType)
-> Maybe LocSpecType -> Maybe SpecType
forall a b. (a -> b) -> a -> 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)
    x :: LocSymbol
x = Symbol -> LocSymbol
forall a. a -> Located a
F.dummyLoc Symbol
functionComposisionSymbol
    v :: Var
v = Env -> ModName -> String -> LocSymbol -> Var
Bare.lookupGhcVar Env
env ModName
name String
"wiredAxioms" LocSymbol
x

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


makeCompositionExpression :: Ghc.Id -> Ghc.CoreExpr 
makeCompositionExpression :: Var -> CoreExpr
makeCompositionExpression Var
x 
  =  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
$ String -> Var -> Var
forall a. PPrint a => String -> a -> a
F.notracepp ( -- tracing to find  the body of . from the inline spec, 
                                      -- replace F.notrace with F.trace to print 
      String
"\nv = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Var -> String
forall a. Outputable a => a -> String
GM.showPpr Var
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
      String
"\n realIdUnfolding = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Unfolding -> String
forall a. Outputable a => a -> String
GM.showPpr (Var -> Unfolding
Ghc.realIdUnfolding Var
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
      String
"\n maybeUnfoldingTemplate . realIdUnfolding = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe CoreExpr -> String
forall a. Outputable a => a -> String
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
x ) String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
      String
"\n inl_src . inlinePragInfo . Ghc.idInfo = "    String -> String -> String
forall a. [a] -> [a] -> [a]
++ SourceText -> String
forall a. Outputable a => a -> String
GM.showPpr (InlinePragma -> SourceText
inl_src (InlinePragma -> SourceText) -> InlinePragma -> SourceText
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
      String
"\n inl_inline . inlinePragInfo . Ghc.idInfo = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ InlineSpec -> String
forall a. Outputable a => a -> String
GM.showPpr (InlinePragma -> InlineSpec
inl_inline (InlinePragma -> InlineSpec) -> InlinePragma -> InlineSpec
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
      String
"\n inl_sat . inlinePragInfo . Ghc.idInfo = "    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe Int -> String
forall a. Outputable a => a -> String
GM.showPpr (InlinePragma -> Maybe Int
inl_sat (InlinePragma -> Maybe Int) -> InlinePragma -> Maybe Int
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
      String
"\n inl_act . inlinePragInfo . Ghc.idInfo = "    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Activation -> String
forall a. Outputable a => a -> String
GM.showPpr (InlinePragma -> Activation
inl_act (InlinePragma -> Activation) -> InlinePragma -> Activation
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
      String
"\n inl_rule . inlinePragInfo . Ghc.idInfo = "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ RuleMatchInfo -> String
forall a. Outputable a => a -> String
GM.showPpr (InlinePragma -> RuleMatchInfo
inl_rule (InlinePragma -> RuleMatchInfo) -> InlinePragma -> RuleMatchInfo
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
      String
"\n inl_rule rule = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RuleMatchInfo -> String
forall a. Outputable a => a -> String
GM.showPpr (InlinePragma -> RuleMatchInfo
inl_rule (InlinePragma -> RuleMatchInfo) -> InlinePragma -> RuleMatchInfo
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
      String
"\n inline spec = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ InlineSpec -> String
forall a. Outputable a => a -> String
GM.showPpr (InlinePragma -> InlineSpec
inl_inline (InlinePragma -> InlineSpec) -> InlinePragma -> InlineSpec
forall a b. (a -> b) -> a -> b
$ IdInfo -> InlinePragma
inlinePragInfo (IdInfo -> InlinePragma) -> IdInfo -> InlinePragma
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> IdInfo
Var -> IdInfo
Ghc.idInfo Var
x)  
     ) Var
x 
   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 = String -> Type -> Var
stringVar String
"f" Type
tf 
            g :: Var
g = String -> Type -> Var
stringVar String
"g" Type
tg
            x :: Var
x = String -> Type -> Var
stringVar String
"x" Type
tx 
        in Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Ghc.Lam (TyCoVarBinder -> Var
forall tv argf. VarBndr tv argf -> tv
Ghc.binderVar TyCoVarBinder
a) (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ 
           Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Ghc.Lam (TyCoVarBinder -> Var
forall tv argf. VarBndr tv argf -> tv
Ghc.binderVar TyCoVarBinder
b) (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ 
           Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Ghc.Lam (TyCoVarBinder -> Var
forall tv argf. VarBndr tv argf -> tv
Ghc.binderVar TyCoVarBinder
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
_ = String -> CoreExpr
forall a. HasCallStack => String -> a
error String
"Axioms.go"