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

{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-x-partial #-}

module Language.Haskell.Liquid.Transforms.CoreToLogic
  ( coreToDef
  , coreToFun
  , coreToLogic
  , mkLit, mkI, mkS
  , runToLogic
  , runToLogicWithBoolBinds
  , logicType
  , inlineSpecType
  , measureSpecType
  , weakenResult
  , normalize
  ) where

import           Data.Bifunctor (first)
import           Data.ByteString                       (ByteString)
import           Prelude                               hiding (error)
import           Language.Haskell.Liquid.GHC.TypeRep   () -- needed for Eq 'Type'
import           Liquid.GHC.API       hiding (Expr, Located, get, panic)
import qualified Liquid.GHC.API       as Ghc
import qualified Liquid.GHC.API       as C
import qualified Data.List                             as L
import           Data.Maybe                            (listToMaybe)
import qualified Data.Text                             as T
import qualified Data.Char
import qualified Text.Printf as Printf
import           Data.Text.Encoding
import           Data.Text.Encoding.Error
import           Control.Monad.Except
import           Control.Monad.Identity
import qualified Language.Haskell.Liquid.Misc          as Misc
import           Language.Fixpoint.Types               hiding (panic, Error, R, simplify, isBool)
import qualified Language.Fixpoint.Types               as F
import qualified Language.Haskell.Liquid.GHC.Misc      as GM


import           Language.Haskell.Liquid.Bare.Types
import           Language.Haskell.Liquid.Bare.DataType
import           Language.Haskell.Liquid.Bare.Misc     (simpleSymbolVar)
import           Language.Haskell.Liquid.GHC.Play
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Types

import qualified Data.HashMap.Strict                   as M
import Control.Monad.Reader
import Language.Haskell.Liquid.UX.Config

logicType :: (Reftable r) => Bool -> Type -> RRType r
logicType :: forall r. Reftable r => Bool -> Type -> RRType r
logicType Bool
allowTC Type
τ      = RTypeRepV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r)
-> RTypeRepV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol RTyCon RTyVar r
t { ty_binds = bs, ty_info = is, ty_args = as, ty_refts = rs}
  where
    t :: RTypeRepV Symbol RTyCon RTyVar r
t            = RTypeV Symbol RTyCon RTyVar r -> RTypeRepV Symbol RTyCon RTyVar r
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (RTypeV Symbol RTyCon RTyVar r -> RTypeRepV Symbol RTyCon RTyVar r)
-> RTypeV Symbol RTyCon RTyVar r
-> RTypeRepV Symbol RTyCon RTyVar r
forall a b. (a -> b) -> a -> b
$ Type -> RTypeV Symbol RTyCon RTyVar r
forall r. Monoid r => Type -> RRType r
ofType Type
τ
    ([Symbol]
bs, [RFInfo]
is, [RTypeV Symbol RTyCon RTyVar r]
as, [r]
rs) = [(Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)]
-> ([Symbol], [RFInfo], [RTypeV Symbol RTyCon RTyVar r], [r])
forall t t1 t2 t3. [(t, t1, t2, t3)] -> ([t], [t1], [t2], [t3])
Misc.unzip4 ([(Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)]
 -> ([Symbol], [RFInfo], [RTypeV Symbol RTyCon RTyVar r], [r]))
-> [(Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)]
-> ([Symbol], [RFInfo], [RTypeV Symbol RTyCon RTyVar r], [r])
forall a b. (a -> b) -> a -> b
$ ((Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r) -> Bool)
-> [(Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)]
-> [(Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (RTypeV Symbol RTyCon RTyVar r -> Bool
forall {v} {t} {t1}. RTypeV v RTyCon t t1 -> Bool
isErasable' (RTypeV Symbol RTyCon RTyVar r -> Bool)
-> ((Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)
    -> RTypeV Symbol RTyCon RTyVar r)
-> (Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)
-> RTypeV Symbol RTyCon RTyVar r
forall t1 t2 t3 t4. (t1, t2, t3, t4) -> t3
Misc.thd4) ([(Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)]
 -> [(Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)])
-> [(Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)]
-> [(Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)]
forall a b. (a -> b) -> a -> b
$ [Symbol]
-> [RFInfo]
-> [RTypeV Symbol RTyCon RTyVar r]
-> [r]
-> [(Symbol, RFInfo, RTypeV Symbol RTyCon RTyVar r, r)]
forall t t1 t2 t3. [t] -> [t1] -> [t2] -> [t3] -> [(t, t1, t2, t3)]
Misc.zip4 (RTypeRepV Symbol RTyCon RTyVar r -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar r
t) (RTypeRepV Symbol RTyCon RTyVar r -> [RFInfo]
forall v c tv r. RTypeRepV v c tv r -> [RFInfo]
ty_info RTypeRepV Symbol RTyCon RTyVar r
t) (RTypeRepV Symbol RTyCon RTyVar r -> [RTypeV Symbol RTyCon RTyVar r]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar r
t) (RTypeRepV Symbol RTyCon RTyVar r -> [r]
forall v c tv r. RTypeRepV v c tv r -> [r]
ty_refts RTypeRepV Symbol RTyCon RTyVar r
t)
    isErasable' :: RTypeV v RTyCon t t1 -> Bool
isErasable'  = if Bool
allowTC then RTypeV v RTyCon t t1 -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isEmbeddedClass else RTypeV v RTyCon t t1 -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType

{- | [NOTE:inlineSpecType type]: the refinement depends on whether the result type is a Bool or not:
      CASE1: measure f@logic :: X -> Bool <=> f@haskell :: x:X -> {v:Bool | v <=> (f@logic x)}
     CASE2: measure f@logic :: X -> Y    <=> f@haskell :: x:X -> {v:Y    | v = (f@logic x)}
 -}
-- formerly: strengthenResult
inlineSpecType :: Bool -> Var -> SpecType
inlineSpecType :: Bool -> Id -> SpecType
inlineSpecType  Bool
allowTC Id
v = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType)
-> RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol RTyCon RTyVar RReft
rep {ty_res = res `strengthen` r , ty_binds = xs}
  where
    r :: RReft
r              = ReftV Symbol -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft (Expr -> ReftV Symbol
mkReft (LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
f ((Symbol, SpecType) -> Expr
forall {b} {b}. (b, b) -> ExprV b
mkA ((Symbol, SpecType) -> Expr) -> [(Symbol, SpecType)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
vxs))) PredicateV Symbol
forall a. Monoid a => a
mempty
    rep :: RTypeRepV Symbol RTyCon RTyVar RReft
rep            = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
t
    res :: SpecType
res            = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res RTypeRepV Symbol RTyCon RTyVar RReft
rep
    xs :: [Symbol]
xs             = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"x" :: String)) (Int -> Symbol) -> [Int] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..[Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Symbol] -> Int) -> [Symbol] -> Int
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar RReft
rep]
    vxs :: [(Symbol, SpecType)]
vxs            = ((Symbol, SpecType) -> Bool)
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (SpecType -> Bool
forall {v} {t} {t1}. RTypeV v RTyCon t t1 -> Bool
isErasable' (SpecType -> Bool)
-> ((Symbol, SpecType) -> SpecType) -> (Symbol, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd) ([(Symbol, SpecType)] -> [(Symbol, SpecType)])
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs (RTypeRepV Symbol RTyCon RTyVar RReft -> [SpecType]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar RReft
rep)
    isErasable' :: RTypeV v RTyCon t t1 -> Bool
isErasable'    = if Bool
allowTC then RTypeV v RTyCon t t1 -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isEmbeddedClass else RTypeV v RTyCon t t1 -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType
    f :: LocSymbol
f              = Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
v)
    t :: SpecType
t              = Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType (Id -> Type
GM.expandVarType Id
v) :: SpecType
    mkA :: (b, b) -> ExprV b
mkA            = b -> ExprV b
forall v. v -> ExprV v
EVar (b -> ExprV b) -> ((b, b) -> b) -> (b, b) -> ExprV b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b, b) -> b
forall a b. (a, b) -> a
fst
    mkReft :: Expr -> ReftV Symbol
mkReft         = if SpecType -> Bool
forall t t1. RType RTyCon t t1 -> Bool
isBool SpecType
res then Expr -> ReftV Symbol
forall a. Predicate a => a -> ReftV Symbol
propReft else Expr -> ReftV Symbol
forall a. Expression a => a -> ReftV Symbol
exprReft

-- | Refine types of measures: keep going until you find the last data con!
--   this code is a hack! we refine the last data constructor,
--   it got complicated to support both
--   1. multi parameter measures     (see tests/pos/HasElem.hs)
--   2. measures returning functions (fromReader :: Reader r a -> (r -> a) )
--   TODO: SIMPLIFY by dropping support for multi parameter measures

-- formerly: strengthenResult'
measureSpecType :: Bool -> Var -> SpecType
measureSpecType :: Bool -> Id -> SpecType
measureSpecType Bool
allowTC Id
v = ([Symbol] -> RReft) -> [Symbol] -> [Int] -> SpecType -> SpecType
forall {c} {r} {a} {v} {tv}.
(TyConable c, Reftable r, Show a) =>
([Symbol] -> r)
-> [Symbol] -> [a] -> RTypeV v c tv r -> RTypeV v c tv r
go [Symbol] -> RReft
forall {v}.
Monoid (PredicateV v) =>
[Symbol] -> UReftV v (ReftV Symbol)
mkT [] [(Int
1::Int)..] SpecType
st
  where
    mkReft :: Expr -> ReftV Symbol
mkReft | Bool
boolRes   = Expr -> ReftV Symbol
forall a. Predicate a => a -> ReftV Symbol
propReft
           | Bool
otherwise = Expr -> ReftV Symbol
forall a. Expression a => a -> ReftV Symbol
exprReft
    mkT :: [Symbol] -> UReftV v (ReftV Symbol)
mkT [Symbol]
xs          = ReftV Symbol -> PredicateV v -> UReftV v (ReftV Symbol)
forall v r. r -> PredicateV v -> UReftV v r
MkUReft (Expr -> ReftV Symbol
mkReft (Expr -> ReftV Symbol) -> Expr -> ReftV Symbol
forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
locSym (Symbol -> Expr
forall v. v -> ExprV v
EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse [Symbol]
xs)) PredicateV v
forall a. Monoid a => a
mempty
    locSym :: LocSymbol
locSym          = Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
v)
    st :: SpecType
st              = Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType (Id -> Type
GM.expandVarType Id
v) :: SpecType
    boolRes :: Bool
boolRes         =  SpecType -> Bool
forall t t1. RType RTyCon t t1 -> Bool
isBool (SpecType -> Bool) -> SpecType -> Bool
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res (RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType)
-> RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
st

    go :: ([Symbol] -> r)
-> [Symbol] -> [a] -> RTypeV v c tv r -> RTypeV v c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i (RAllT RTVUV v c tv
a RTypeV v c tv r
t r
r)    = RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV v c tv
a (([Symbol] -> r)
-> [Symbol] -> [a] -> RTypeV v c tv r -> RTypeV v c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i RTypeV v c tv r
t) r
r
    go [Symbol] -> r
f [Symbol]
args [a]
i (RAllP PVUV v c tv
p RTypeV v c tv r
t)      = PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV v c tv
p (RTypeV v c tv r -> RTypeV v c tv r)
-> RTypeV v c tv r -> RTypeV v c tv r
forall a b. (a -> b) -> a -> b
$ ([Symbol] -> r)
-> [Symbol] -> [a] -> RTypeV v c tv r -> RTypeV v c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i RTypeV v c tv r
t
    go [Symbol] -> r
f [Symbol]
args [a]
i (RFun Symbol
x RFInfo
ii RTypeV v c tv r
t1 RTypeV v c tv r
t2 r
r)
     | (if Bool
allowTC then RTypeV v c tv r -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isEmbeddedClass else RTypeV v c tv r -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType) RTypeV v c tv r
t1           = Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
ii RTypeV v c tv r
t1 (([Symbol] -> r)
-> [Symbol] -> [a] -> RTypeV v c tv r -> RTypeV v c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i RTypeV v c tv r
t2) r
r
    go [Symbol] -> r
f [Symbol]
args [a]
i t :: RTypeV v c tv r
t@(RFun Symbol
_ RFInfo
ii RTypeV v c tv r
t1 RTypeV v c tv r
t2 r
r)
     | RTypeV v c tv r -> Bool
forall {v} {c} {tv} {r}. RTypeV v c tv r -> Bool
hasRApps RTypeV v c tv r
t               = Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x' RFInfo
ii RTypeV v c tv r
t1 (([Symbol] -> r)
-> [Symbol] -> [a] -> RTypeV v c tv r -> RTypeV v c tv r
go [Symbol] -> r
f (Symbol
x'Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
args) ([a] -> [a]
forall a. HasCallStack => [a] -> [a]
tail [a]
i) RTypeV v c tv r
t2) r
r
                                       where x' :: Symbol
x' = Symbol -> a -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"x" :: String)) ([a] -> a
forall a. HasCallStack => [a] -> a
head [a]
i)
    go [Symbol] -> r
f [Symbol]
args [a]
_ RTypeV v c tv r
t                = RTypeV v c tv r
t RTypeV v c tv r -> r -> RTypeV v c tv r
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`strengthen` [Symbol] -> r
f [Symbol]
args

    hasRApps :: RTypeV v c tv r -> Bool
hasRApps (RFun Symbol
_ RFInfo
_ RTypeV v c tv r
t1 RTypeV v c tv r
t2 r
_) = RTypeV v c tv r -> Bool
hasRApps RTypeV v c tv r
t1 Bool -> Bool -> Bool
|| RTypeV v c tv r -> Bool
hasRApps RTypeV v c tv r
t2
    hasRApps RApp {}          = Bool
True
    hasRApps RTypeV v c tv r
_                = Bool
False


-- | 'weakenResult foo t' drops the singleton constraint `v = foo x y`
--   that is added, e.g. for measures in /strengthenResult'.
--   This should only be used _when_ checking the body of 'foo'
--   where the output, is, by definition, equal to the singleton.
weakenResult :: Bool -> Var -> SpecType -> SpecType
weakenResult :: Bool -> Id -> SpecType -> SpecType
weakenResult Bool
allowTC Id
v SpecType
t = String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp String
msg SpecType
t'
  where
    msg :: String
msg          = String
"weakenResult v =" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Outputable a => a -> String
GM.showPpr Id
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" t = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. PPrint a => a -> String
showpp SpecType
t
    t' :: SpecType
t'           = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType)
-> RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol RTyCon RTyVar RReft
rep { ty_res = mapExprReft weaken (ty_res rep) }
    rep :: RTypeRepV Symbol RTyCon RTyVar RReft
rep          = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
t
    weaken :: Symbol -> Expr -> Expr
weaken Symbol
x     = [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd ([Expr] -> Expr) -> (Expr -> [Expr]) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
vE Maybe Expr -> Maybe Expr -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Maybe Expr -> Bool) -> (Expr -> Maybe Expr) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Expr -> Maybe Expr
isSingletonExpr Symbol
x) ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts
    vE :: Expr
vE           = LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
vF [Expr]
xs
    xs :: [Expr]
xs           = Symbol -> Expr
forall v. v -> ExprV v
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
<$> ((Symbol, SpecType) -> Bool)
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile ((if Bool
allowTC then SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isEmbeddedClass else SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType) (SpecType -> Bool)
-> ((Symbol, SpecType) -> SpecType) -> (Symbol, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd) [(Symbol, SpecType)]
xts
    xts :: [(Symbol, SpecType)]
xts          = [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar RReft
rep) (RTypeRepV Symbol RTyCon RTyVar RReft -> [SpecType]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar RReft
rep)
    vF :: LocSymbol
vF           = Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
v)

type LogicM = ExceptT Error (ReaderT LState Identity)

data LState = LState
  { LState -> LogicMap
lsSymMap  :: LogicMap
  , LState -> String -> Error
lsError   :: String -> Error
  , LState -> TCEmb TyCon
lsEmb     :: TCEmb TyCon
  , LState -> [Id]
lsBools   :: [Var]
  , LState -> DataConMap
lsDCMap   :: DataConMap
  , LState -> Config
lsConfig  :: Config
  }

throw :: String -> LogicM a
throw :: forall a. String -> LogicM a
throw String
str = do
  fmkError  <- (LState -> String -> Error)
-> ExceptT Error (ReaderT LState Identity) (String -> Error)
forall a.
(LState -> a) -> ExceptT Error (ReaderT LState Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader LState -> String -> Error
lsError
  throwError $ fmkError str

getState :: LogicM LState
getState :: LogicM LState
getState = LogicM LState
forall r (m :: * -> *). MonadReader r m => m r
ask

runToLogic
  :: TCEmb TyCon -> LogicMap -> DataConMap -> Config -> (String -> Error)
  -> LogicM t -> Either Error t
runToLogic :: forall t.
TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> (String -> Error)
-> LogicM t
-> Either Error t
runToLogic = [Id]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> (String -> Error)
-> LogicM t
-> Either Error t
forall t.
[Id]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> (String -> Error)
-> LogicM t
-> Either Error t
runToLogicWithBoolBinds []

runToLogicWithBoolBinds
  :: [Var] -> TCEmb TyCon -> LogicMap -> DataConMap -> Config -> (String -> Error)
  -> LogicM t -> Either Error t
runToLogicWithBoolBinds :: forall t.
[Id]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> (String -> Error)
-> LogicM t
-> Either Error t
runToLogicWithBoolBinds [Id]
xs TCEmb TyCon
tce LogicMap
lmap DataConMap
dm Config
cfg String -> Error
ferror LogicM t
m
  = Reader LState (Either Error t) -> LState -> Either Error t
forall r a. Reader r a -> r -> a
runReader (LogicM t -> Reader LState (Either Error t)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT LogicM t
m) (LState -> Either Error t) -> LState -> Either Error t
forall a b. (a -> b) -> a -> b
$ LState
      { lsSymMap :: LogicMap
lsSymMap = LogicMap
lmap
      , lsError :: String -> Error
lsError  = String -> Error
ferror
      , lsEmb :: TCEmb TyCon
lsEmb    = TCEmb TyCon
tce
      , lsBools :: [Id]
lsBools  = [Id]
xs
      , lsDCMap :: DataConMap
lsDCMap  = DataConMap
dm
      , lsConfig :: Config
lsConfig = Config
cfg
      }

coreAltToDef :: (Reftable r) => Located LHName -> Var -> [Var] -> Var -> Type -> [C.CoreAlt]
             -> LogicM [Def (Located (RRType r)) DataCon]
coreAltToDef :: forall r.
Reftable r =>
Located LHName
-> Id
-> [Id]
-> Id
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
coreAltToDef Located LHName
locSym Id
z [Id]
zs Id
y Type
t [CoreAlt]
alts
  | Bool -> Bool
not ([CoreAlt] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoreAlt]
litAlts) = Located LHName
-> String -> LogicM [DefV Symbol (Located (RRType r)) DataCon]
forall a. Located LHName -> String -> a
measureFail Located LHName
locSym String
"Cannot lift definition with literal alternatives"
  | Bool
otherwise          = do
      d1s <- String
-> [DefV Symbol (Located (RRType r)) DataCon]
-> [DefV Symbol (Located (RRType r)) DataCon]
forall a. PPrint a => String -> a -> a
F.notracepp String
"coreAltDefs-1" ([DefV Symbol (Located (RRType r)) DataCon]
 -> [DefV Symbol (Located (RRType r)) DataCon])
-> LogicM [DefV Symbol (Located (RRType r)) DataCon]
-> LogicM [DefV Symbol (Located (RRType r)) DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoreAlt
 -> ExceptT
      Error
      (ReaderT LState Identity)
      (DefV Symbol (Located (RRType r)) DataCon))
-> [CoreAlt] -> LogicM [DefV Symbol (Located (RRType r)) DataCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Located LHName
-> (Expr -> BodyV Symbol)
-> [Id]
-> Id
-> CoreAlt
-> ExceptT
     Error
     (ReaderT LState Identity)
     (DefV Symbol (Located (RRType r)) DataCon)
forall {r} {v} {p}.
Reftable r =>
Located LHName
-> (Expr -> BodyV v)
-> p
-> Id
-> CoreAlt
-> ExceptT
     Error
     (ReaderT LState Identity)
     (DefV v (Located (RRType r)) DataCon)
mkAlt Located LHName
locSym Expr -> BodyV Symbol
forall {v}. ExprV v -> BodyV v
cc [Id]
myArgs Id
z) [CoreAlt]
dataAlts
      d2s <- F.notracepp "coreAltDefs-2" <$>       mkDef locSym cc myArgs z  defAlts defExpr
      return (d1s ++ d2s)
  where
    myArgs :: [Id]
myArgs   = [Id] -> [Id]
forall a. [a] -> [a]
reverse [Id]
zs
    cc :: ExprV v -> BodyV v
cc       = if Type -> Type -> Bool
eqType Type
t Type
boolTy then ExprV v -> BodyV v
forall {v}. ExprV v -> BodyV v
P else ExprV v -> BodyV v
forall {v}. ExprV v -> BodyV v
E
    defAlts :: Maybe [(DataCon, [Id], [Type])]
defAlts  = Type -> [AltCon] -> Maybe [(DataCon, [Id], [Type])]
GM.defaultDataCons (Id -> Type
GM.expandVarType Id
y) ((\(Alt AltCon
c [Id]
_ CoreExpr
_) -> AltCon
c) (CoreAlt -> AltCon) -> [CoreAlt] -> [AltCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreAlt]
alts)
    defExpr :: Maybe CoreExpr
defExpr  = [CoreExpr] -> Maybe CoreExpr
forall a. [a] -> Maybe a
listToMaybe [ CoreExpr
e |   (Alt AltCon
C.DEFAULT [Id]
_ CoreExpr
e) <- [CoreAlt]
alts ]
    dataAlts :: [CoreAlt]
dataAlts =             [ CoreAlt
a | a :: CoreAlt
a@(Alt (C.DataAlt DataCon
_) [Id]
_ CoreExpr
_) <- [CoreAlt]
alts ]
    litAlts :: [CoreAlt]
litAlts  =             [ CoreAlt
a | a :: CoreAlt
a@(Alt (C.LitAlt Literal
_) [Id]
_ CoreExpr
_) <- [CoreAlt]
alts ]

    -- mkAlt :: LocSymbol -> (Expr -> Body) -> [Var] -> Var -> (C.AltCon, [Var], C.CoreExpr)
    mkAlt :: Located LHName
-> (Expr -> BodyV v)
-> p
-> Id
-> CoreAlt
-> ExceptT
     Error
     (ReaderT LState Identity)
     (DefV v (Located (RRType r)) DataCon)
mkAlt Located LHName
x Expr -> BodyV v
ctor p
_args Id
dx (Alt (C.DataAlt DataCon
d) [Id]
xs CoreExpr
e)
      = do
          allowTC <- (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a.
(LState -> a) -> ExceptT Error (ReaderT LState Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader (Config -> Bool
typeclass (Config -> Bool) -> (LState -> Config) -> LState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LState -> Config
lsConfig)
          let xs' = (Id -> Bool) -> [Id] -> [Id]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Id -> Bool) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. if Bool
allowTC then Id -> Bool
GM.isEmbeddedDictVar else Id -> Bool
GM.isEvVar) [Id]
xs
          Def x {- (toArgs id args) -} d (Just $ varRType dx) (toArgs Just xs')
               . ctor
               . (`subst1` (F.symbol dx, F.mkEApp (GM.namedLocSymbol d) (F.eVar <$> xs')))
              <$> coreToLg e
    mkAlt Located LHName
_ Expr -> BodyV v
_ p
_ Id
_ CoreAlt
alt
      = String
-> ExceptT
     Error
     (ReaderT LState Identity)
     (DefV v (Located (RRType r)) DataCon)
forall a. String -> LogicM a
throw (String
 -> ExceptT
      Error
      (ReaderT LState Identity)
      (DefV v (Located (RRType r)) DataCon))
-> String
-> ExceptT
     Error
     (ReaderT LState Identity)
     (DefV v (Located (RRType r)) DataCon)
forall a b. (a -> b) -> a -> b
$ String
"Bad alternative" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreAlt -> String
forall a. Outputable a => a -> String
GM.showPpr CoreAlt
alt

    mkDef :: Located LHName
-> (Expr -> BodyV v)
-> p
-> Id
-> Maybe [(ctor, b, [Type])]
-> Maybe CoreExpr
-> ExceptT
     Error (ReaderT LState Identity) [DefV v (Located (RRType r)) ctor]
mkDef Located LHName
x Expr -> BodyV v
ctor p
_args Id
dx (Just [(ctor, b, [Type])]
dtss) (Just CoreExpr
e) = do
      eDef   <- Expr -> BodyV v
ctor (Expr -> BodyV v)
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) (BodyV v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e
      -- let ys  = toArgs id args
      let dxt = Located (RRType r) -> Maybe (Located (RRType r))
forall a. a -> Maybe a
Just (Id -> Located (RRType r)
forall r. Reftable r => Id -> Located (RRType r)
varRType Id
dx)
      return  [ Def x {- ys -} d dxt (defArgs x ts) eDef | (d, _, ts) <- dtss ]

    mkDef Located LHName
_ Expr -> BodyV v
_ p
_ Id
_ Maybe [(ctor, b, [Type])]
_ Maybe CoreExpr
_ =
      [DefV v (Located (RRType r)) ctor]
-> ExceptT
     Error (ReaderT LState Identity) [DefV v (Located (RRType r)) ctor]
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return []

toArgs :: Reftable r => (Located (RRType r) -> b) -> [Var] -> [(Symbol, b)]
toArgs :: forall r b.
Reftable r =>
(Located (RRType r) -> b) -> [Id] -> [(Symbol, b)]
toArgs Located (RRType r) -> b
f [Id]
args = [(Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
x, Located (RRType r) -> b
f (Located (RRType r) -> b) -> Located (RRType r) -> b
forall a b. (a -> b) -> a -> b
$ Id -> Located (RRType r)
forall r. Reftable r => Id -> Located (RRType r)
varRType Id
x) | Id
x <- [Id]
args]

defArgs :: Monoid r => Located LHName -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]
defArgs :: forall r.
Monoid r =>
Located LHName -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]
defArgs Located LHName
x     = (Integer -> Type -> (Symbol, Maybe (Located (RRType r))))
-> [Integer] -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Integer
i Type
t -> (Integer -> Symbol
defArg Integer
i, Type -> Maybe (Located (RRType r))
defRTyp Type
t)) [Integer
0..]
  where
    defArg :: Integer -> Symbol
defArg    = Symbol -> Integer -> Symbol
tempSymbol (LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol) -> LHName -> Symbol
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val Located LHName
x)
    defRTyp :: Type -> Maybe (Located (RRType r))
defRTyp   = Located (RRType r) -> Maybe (Located (RRType r))
forall a. a -> Maybe a
Just (Located (RRType r) -> Maybe (Located (RRType r)))
-> (Type -> Located (RRType r))
-> Type
-> Maybe (Located (RRType r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> RRType r -> Located (RRType r)
forall l b. Loc l => l -> b -> Located b
F.atLoc Located LHName
x (RRType r -> Located (RRType r))
-> (Type -> RRType r) -> Type -> Located (RRType r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> RRType r
forall r. Monoid r => Type -> RRType r
ofType

coreToDef :: Reftable r => Located LHName -> Var -> C.CoreExpr
          -> LogicM [Def (Located (RRType r)) DataCon]
coreToDef :: forall r.
Reftable r =>
Located LHName
-> Id -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
coreToDef Located LHName
locSym Id
_ CoreExpr
s              = do 
    allowTC <- (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a.
(LState -> a) -> ExceptT Error (ReaderT LState Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool)
-> (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a b. (a -> b) -> a -> b
$ Config -> Bool
typeclass (Config -> Bool) -> (LState -> Config) -> LState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LState -> Config
lsConfig
    go [] $ inlinePreds $ simplify allowTC s
  where
    go :: [Id] -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
go [Id]
args   (C.Lam  Id
x CoreExpr
e)        = [Id] -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
go (Id
xId -> [Id] -> [Id]
forall a. a -> [a] -> [a]
:[Id]
args) CoreExpr
e
    go [Id]
args   (C.Tick CoreTickish
_ CoreExpr
e)        = [Id] -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
go [Id]
args CoreExpr
e
    go (Id
z:[Id]
zs) (C.Case CoreExpr
_ Id
y Type
t [CoreAlt]
alts) = Located LHName
-> Id
-> [Id]
-> Id
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
forall r.
Reftable r =>
Located LHName
-> Id
-> [Id]
-> Id
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
coreAltToDef Located LHName
locSym Id
z [Id]
zs Id
y Type
t [CoreAlt]
alts
    go (Id
z:[Id]
zs) CoreExpr
e
      | Just Type
t <- Id -> Maybe Type
isMeasureArg Id
z  = Located LHName
-> Id
-> [Id]
-> Id
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
forall r.
Reftable r =>
Located LHName
-> Id
-> [Id]
-> Id
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
coreAltToDef Located LHName
locSym Id
z [Id]
zs Id
z Type
t [AltCon -> [Id] -> CoreExpr -> CoreAlt
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
C.DEFAULT [] CoreExpr
e]
    go [Id]
_ CoreExpr
_                        = Located LHName
-> String -> LogicM [Def (Located (RRType r)) DataCon]
forall a. Located LHName -> String -> a
measureFail Located LHName
locSym String
"Does not have a case-of at the top-level"

    inlinePreds :: CoreExpr -> CoreExpr
inlinePreds   = (Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline (Type -> Type -> Bool
eqType Type
boolTy (Type -> Bool) -> (Id -> Type) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
GM.expandVarType)

measureFail       :: Located LHName -> String -> a
measureFail :: forall a. Located LHName -> String -> a
measureFail Located LHName
x String
msg = Maybe SrcSpan -> String -> a
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
sp String
e
  where
    sp :: Maybe SrcSpan
sp            = SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
x)
    e :: String
e             = String -> String -> String -> String
forall r. PrintfType r => String -> r
Printf.printf String
"Cannot create measure '%s': %s" (Located LHName -> String
forall a. PPrint a => a -> String
F.showpp Located LHName
x) String
msg


-- | 'isMeasureArg x' returns 'Just t' if 'x' is a valid argument for a measure.
isMeasureArg :: Var -> Maybe Type
isMeasureArg :: Id -> Maybe Type
isMeasureArg Id
x
  | Just TyCon
tc <- Maybe TyCon
tcMb
  , TyCon -> Bool
Ghc.isAlgTyCon TyCon
tc = String -> Maybe Type -> Maybe Type
forall a. PPrint a => String -> a -> a
F.notracepp String
"isMeasureArg" (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
t
  | Bool
otherwise           = Maybe Type
forall a. Maybe a
Nothing
  where
    t :: Type
t                   = Id -> Type
GM.expandVarType Id
x
    tcMb :: Maybe TyCon
tcMb                = Type -> Maybe TyCon
tyConAppTyCon_maybe Type
t


varRType :: (Reftable r) => Var -> Located (RRType r)
varRType :: forall r. Reftable r => Id -> Located (RRType r)
varRType = (Type -> RRType r) -> Id -> Located (RRType r)
forall a. (Type -> a) -> Id -> Located a
GM.varLocInfo Type -> RRType r
forall r. Monoid r => Type -> RRType r
ofType

coreToFun :: LocSymbol -> Var -> C.CoreExpr ->  LogicM ([Var], Either Expr Expr)
coreToFun :: LocSymbol -> Id -> CoreExpr -> LogicM ([Id], Either Expr Expr)
coreToFun LocSymbol
_ Id
_v CoreExpr
s = do 
  allowTC <- (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a.
(LState -> a) -> ExceptT Error (ReaderT LState Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool)
-> (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a b. (a -> b) -> a -> b
$ Config -> Bool
typeclass (Config -> Bool) -> (LState -> Config) -> LState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LState -> Config
lsConfig
  go [] $ normalize allowTC s
  where
    go :: [Id]
-> CoreExpr
-> ExceptT Error (ReaderT LState Identity) ([Id], Either a Expr)
go [Id]
acc (C.Lam Id
x CoreExpr
e)  | Id -> Bool
isTyVar Id
x = [Id]
-> CoreExpr
-> ExceptT Error (ReaderT LState Identity) ([Id], Either a Expr)
go [Id]
acc CoreExpr
e
    go [Id]
acc (C.Lam Id
x CoreExpr
e)  = do 
      allowTC <- (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a.
(LState -> a) -> ExceptT Error (ReaderT LState Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool)
-> (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a b. (a -> b) -> a -> b
$ Config -> Bool
typeclass (Config -> Bool) -> (LState -> Config) -> LState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LState -> Config
lsConfig
      let isE = if Bool
allowTC then Id -> Bool
GM.isEmbeddedDictVar else Id -> Bool
isErasable
      if isE x then go acc e else go (x:acc) e
    go [Id]
acc (C.Tick CoreTickish
_ CoreExpr
e) = [Id]
-> CoreExpr
-> ExceptT Error (ReaderT LState Identity) ([Id], Either a Expr)
go [Id]
acc CoreExpr
e
    go [Id]
acc CoreExpr
e            = ([Id] -> [Id]
forall a. [a] -> [a]
reverse [Id]
acc,) (Either a Expr -> ([Id], Either a Expr))
-> (Expr -> Either a Expr) -> Expr -> ([Id], Either a Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Either a Expr
forall a b. b -> Either a b
Right (Expr -> ([Id], Either a Expr))
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) ([Id], Either a Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e


instance Show C.CoreExpr where
  show :: CoreExpr -> String
show = CoreExpr -> String
forall a. Outputable a => a -> String
GM.showPpr

coreToLogic :: C.CoreExpr -> LogicM Expr
coreToLogic :: CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLogic CoreExpr
cb = do
  allowTC <- (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a.
(LState -> a) -> ExceptT Error (ReaderT LState Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool)
-> (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a b. (a -> b) -> a -> b
$ Config -> Bool
typeclass (Config -> Bool) -> (LState -> Config) -> LState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LState -> Config
lsConfig
  coreToLg $ normalize allowTC cb


coreToLg :: C.CoreExpr -> LogicM Expr
coreToLg :: CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg (C.Let (C.NonRec Id
x (C.Coercion Coercion
c)) CoreExpr
e)
  = CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg (HasDebugCallStack => Subst -> CoreExpr -> CoreExpr
Subst -> CoreExpr -> CoreExpr
C.substExpr (Subst -> Id -> Coercion -> Subst
C.extendCvSubst Subst
C.emptySubst Id
x Coercion
c) CoreExpr
e)
coreToLg (C.Let Bind Id
b CoreExpr
e)
  = Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 (Expr -> (Symbol, Expr) -> Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) ((Symbol, Expr) -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e ExceptT Error (ReaderT LState Identity) ((Symbol, Expr) -> Expr)
-> ExceptT Error (ReaderT LState Identity) (Symbol, Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
forall a b.
ExceptT Error (ReaderT LState Identity) (a -> b)
-> ExceptT Error (ReaderT LState Identity) a
-> ExceptT Error (ReaderT LState Identity) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bind Id -> ExceptT Error (ReaderT LState Identity) (Symbol, Expr)
makesub Bind Id
b
coreToLg (C.Tick CoreTickish
_ CoreExpr
e)          = CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e
coreToLg (C.App (C.Var Id
v) CoreExpr
e)
  | Id -> Bool
ignoreVar Id
v                = CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e
coreToLg (C.Var Id
x)
  | Id
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
falseDataConId        = Expr -> ExceptT Error (ReaderT LState Identity) Expr
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
forall v. ExprV v
PFalse
  | Id
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
trueDataConId         = Expr -> ExceptT Error (ReaderT LState Identity) Expr
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
forall v. ExprV v
PTrue
  | Bool
otherwise                  = Id -> LogicMap -> Expr
eVarWithMap Id
x (LogicMap -> Expr) -> (LState -> LogicMap) -> LState -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LState -> LogicMap
lsSymMap (LState -> Expr)
-> LogicM LState -> ExceptT Error (ReaderT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LogicM LState
getState
coreToLg e :: CoreExpr
e@(C.App CoreExpr
_ CoreExpr
_)         = CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
toPredApp CoreExpr
e
coreToLg (C.Case CoreExpr
e Id
b Type
_ [CoreAlt]
alts)
  | Type -> Type -> Bool
eqType (Id -> Type
GM.expandVarType Id
b) Type
boolTy  = [CoreAlt] -> LogicM (CoreExpr, CoreExpr)
checkBoolAlts [CoreAlt]
alts LogicM (CoreExpr, CoreExpr)
-> ((CoreExpr, CoreExpr)
    -> ExceptT Error (ReaderT LState Identity) Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
forall a b.
ExceptT Error (ReaderT LState Identity) a
-> (a -> ExceptT Error (ReaderT LState Identity) b)
-> ExceptT Error (ReaderT LState Identity) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CoreExpr
-> (CoreExpr, CoreExpr)
-> ExceptT Error (ReaderT LState Identity) Expr
coreToIte CoreExpr
e
-- coreToLg (C.Lam x e)           = do p     <- coreToLg e
--                                     tce   <- lsEmb <$> getState
--                                     return $ ELam (symbol x, typeSort tce (GM.expandVarType x)) p
coreToLg (C.Case CoreExpr
e Id
b Type
_ [CoreAlt]
alts)   = do p <- CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e
                                    casesToLg b p alts
coreToLg (C.Lit Literal
l)             = case Literal -> Maybe Expr
mkLit Literal
l of
                                          Maybe Expr
Nothing -> String -> ExceptT Error (ReaderT LState Identity) Expr
forall a. String -> LogicM a
throw (String -> ExceptT Error (ReaderT LState Identity) Expr)
-> String -> ExceptT Error (ReaderT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ String
"Bad Literal in measure definition" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Literal -> String
forall a. Outputable a => a -> String
GM.showPpr Literal
l
                                          Just Expr
i  -> Expr -> ExceptT Error (ReaderT LState Identity) Expr
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
i
coreToLg (C.Cast CoreExpr
e Coercion
c)          = do (s, t) <- Coercion -> LogicM (Sort, Sort)
coerceToLg Coercion
c
                                    e'     <- coreToLg e
                                    return (ECoerc s t e')
-- elaboration reuses coretologic
-- TODO: fix this
coreToLg (C.Lam Id
x CoreExpr
e) = do p     <- CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e
                          tce   <- lsEmb <$> getState
                          return $ ELam (symbol x, typeSort tce (GM.expandVarType x)) p
coreToLg CoreExpr
e                     = String -> ExceptT Error (ReaderT LState Identity) Expr
forall a. String -> LogicM a
throw (String
"Cannot transform to Logic:\t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall a. Outputable a => a -> String
GM.showPpr CoreExpr
e)




coerceToLg :: Coercion -> LogicM (Sort, Sort)
coerceToLg :: Coercion -> LogicM (Sort, Sort)
coerceToLg = (Type, Type) -> LogicM (Sort, Sort)
typeEqToLg ((Type, Type) -> LogicM (Sort, Sort))
-> (Coercion -> (Type, Type)) -> Coercion -> LogicM (Sort, Sort)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> (Type, Type)
coercionTypeEq

coercionTypeEq :: Coercion -> (Type, Type)
coercionTypeEq :: Coercion -> (Type, Type)
coercionTypeEq Coercion
co
  | Ghc.Pair Type
s Type
t <- -- GM.tracePpr ("coercion-type-eq-1: " ++ GM.showPpr co) $
                       Coercion -> Pair Type
coercionKind Coercion
co
  = (Type
s, Type
t)

typeEqToLg :: (Type, Type) -> LogicM (Sort, Sort)
typeEqToLg :: (Type, Type) -> LogicM (Sort, Sort)
typeEqToLg (Type
s, Type
t) = do
  tce   <- (LState -> TCEmb TyCon)
-> ExceptT Error (ReaderT LState Identity) (TCEmb TyCon)
forall a.
(LState -> a) -> ExceptT Error (ReaderT LState Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader LState -> TCEmb TyCon
lsEmb
  let tx = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce (Type -> Sort) -> (Type -> Type) -> Type -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
expandTypeSynonyms
  return $ F.notracepp "TYPE-EQ-TO-LOGIC" (tx s, tx t)

checkBoolAlts :: [C.CoreAlt] -> LogicM (C.CoreExpr, C.CoreExpr)
checkBoolAlts :: [CoreAlt] -> LogicM (CoreExpr, CoreExpr)
checkBoolAlts [Alt (C.DataAlt DataCon
false) [] CoreExpr
efalse, Alt (C.DataAlt DataCon
true) [] CoreExpr
etrue]
  | DataCon
false DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
falseDataCon, DataCon
true DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
trueDataCon
  = (CoreExpr, CoreExpr) -> LogicM (CoreExpr, CoreExpr)
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoreExpr
efalse, CoreExpr
etrue)

checkBoolAlts [Alt (C.DataAlt DataCon
true) [] CoreExpr
etrue, Alt (C.DataAlt DataCon
false) [] CoreExpr
efalse]
  | DataCon
false DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
falseDataCon, DataCon
true DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
trueDataCon
  = (CoreExpr, CoreExpr) -> LogicM (CoreExpr, CoreExpr)
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoreExpr
efalse, CoreExpr
etrue)
checkBoolAlts [CoreAlt]
alts
  = String -> LogicM (CoreExpr, CoreExpr)
forall a. String -> LogicM a
throw (String
"checkBoolAlts failed on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [CoreAlt] -> String
forall a. Outputable a => a -> String
GM.showPpr [CoreAlt]
alts)

casesToLg :: Var -> Expr -> [C.CoreAlt] -> LogicM Expr
casesToLg :: Id
-> Expr
-> [CoreAlt]
-> ExceptT Error (ReaderT LState Identity) Expr
casesToLg Id
v Expr
e [CoreAlt]
alts = (CoreAlt -> ExceptT Error (ReaderT LState Identity) (AltCon, Expr))
-> [CoreAlt]
-> ExceptT Error (ReaderT LState Identity) [(AltCon, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Expr
-> CoreAlt
-> ExceptT Error (ReaderT LState Identity) (AltCon, Expr)
altToLg Expr
e) [CoreAlt]
normAlts ExceptT Error (ReaderT LState Identity) [(AltCon, Expr)]
-> ([(AltCon, Expr)]
    -> ExceptT Error (ReaderT LState Identity) Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
forall a b.
ExceptT Error (ReaderT LState Identity) a
-> (a -> ExceptT Error (ReaderT LState Identity) b)
-> ExceptT Error (ReaderT LState Identity) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(AltCon, Expr)] -> ExceptT Error (ReaderT LState Identity) Expr
go
  where
    normAlts :: [CoreAlt]
normAlts       = [CoreAlt] -> [CoreAlt]
normalizeAlts [CoreAlt]
alts
    go :: [(C.AltCon, Expr)] -> LogicM Expr
    go :: [(AltCon, Expr)] -> ExceptT Error (ReaderT LState Identity) Expr
go [(AltCon
_,Expr
p)]     = Expr -> ExceptT Error (ReaderT LState Identity) Expr
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
p Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
`subst1` (Symbol, Expr)
su)
    go ((AltCon
d,Expr
p):[(AltCon, Expr)]
dps) = do c <- AltCon -> Expr -> ExceptT Error (ReaderT LState Identity) Expr
checkDataAlt AltCon
d Expr
e
                        e' <- go dps
                        return (EIte c p e' `subst1` su)
    go []          = Maybe SrcSpan
-> String -> ExceptT Error (ReaderT LState Identity) Expr
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (Id -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Id
v)) (String -> ExceptT Error (ReaderT LState Identity) Expr)
-> String -> ExceptT Error (ReaderT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ String
"Unexpected empty cases in casesToLg: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e
    su :: (Symbol, Expr)
su             = (Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
v, Expr
e)

checkDataAlt :: C.AltCon -> Expr -> LogicM Expr
checkDataAlt :: AltCon -> Expr -> ExceptT Error (ReaderT LState Identity) Expr
checkDataAlt (C.DataAlt DataCon
d) Expr
e = Expr -> ExceptT Error (ReaderT LState Identity) Expr
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ExceptT Error (ReaderT LState Identity) Expr)
-> Expr -> ExceptT Error (ReaderT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar (DataCon -> Symbol
makeDataConChecker DataCon
d)) Expr
e
checkDataAlt AltCon
C.DEFAULT     Expr
_ = Expr -> ExceptT Error (ReaderT LState Identity) Expr
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
forall v. ExprV v
PTrue
checkDataAlt (C.LitAlt Literal
l)  Expr
e
  | Just Expr
le <- Literal -> Maybe Expr
mkLit Literal
l       = Expr -> ExceptT Error (ReaderT LState Identity) Expr
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EEq Expr
le Expr
e)
  | Bool
otherwise                = String -> ExceptT Error (ReaderT LState Identity) Expr
forall a. String -> LogicM a
throw (String -> ExceptT Error (ReaderT LState Identity) Expr)
-> String -> ExceptT Error (ReaderT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ String
"Oops, not yet handled: checkDataAlt on Lit: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Literal -> String
forall a. Outputable a => a -> String
GM.showPpr Literal
l

-- | 'altsDefault' reorders the CoreAlt to ensure that 'DEFAULT' is at the end.
normalizeAlts :: [C.CoreAlt] -> [C.CoreAlt]
normalizeAlts :: [CoreAlt] -> [CoreAlt]
normalizeAlts [CoreAlt]
alts      = [CoreAlt]
ctorAlts [CoreAlt] -> [CoreAlt] -> [CoreAlt]
forall a. [a] -> [a] -> [a]
++ [CoreAlt]
defAlts
  where
    ([CoreAlt]
defAlts, [CoreAlt]
ctorAlts) = (CoreAlt -> Bool) -> [CoreAlt] -> ([CoreAlt], [CoreAlt])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition CoreAlt -> Bool
forall {b}. Alt b -> Bool
isDefault [CoreAlt]
alts
    isDefault :: Alt b -> Bool
isDefault (Alt AltCon
c [b]
_ Expr b
_)   = AltCon
c AltCon -> AltCon -> Bool
forall a. Eq a => a -> a -> Bool
== AltCon
C.DEFAULT

altToLg :: Expr -> C.CoreAlt -> LogicM (C.AltCon, Expr)
altToLg :: Expr
-> CoreAlt
-> ExceptT Error (ReaderT LState Identity) (AltCon, Expr)
altToLg Expr
de (Alt a :: AltCon
a@(C.DataAlt DataCon
d) [Id]
xs CoreExpr
e) = do
  ctorReflected <- (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a.
(LState -> a) -> ExceptT Error (ReaderT LState Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader (Config -> Bool
forall t. HasConfig t => t -> Bool
exactDCFlag (Config -> Bool) -> (LState -> Config) -> LState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LState -> Config
lsConfig)
  if not ctorReflected && not (primDataCon d) then do
    throw $  "Cannot lift to logic the constructor `" ++ show d
          ++ "` consider enabling either --exactdc or --reflection"
  else do
    p  <- coreToLg e
    dm <- reader lsDCMap
    allowTC <- reader (typeclass . lsConfig)
    let su = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [[(Symbol, Expr)]] -> [(Symbol, Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ DataConMap -> Expr -> DataCon -> Id -> Int -> [(Symbol, Expr)]
dataConProj DataConMap
dm Expr
de DataCon
d Id
x Int
i | (Id
x, Int
i) <- [Id] -> [Int] -> [(Id, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Id -> Bool) -> [Id] -> [Id]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Id -> Bool) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. if Bool
allowTC then Id -> Bool
GM.isEmbeddedDictVar else Id -> Bool
GM.isEvVar) [Id]
xs) [Int
1..]]
    return (a, subst su p)

altToLg Expr
_ (Alt AltCon
a [Id]
_ CoreExpr
e)
  = (AltCon
a, ) (Expr -> (AltCon, Expr))
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) (AltCon, Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e

dataConProj :: DataConMap -> Expr -> DataCon -> Var -> Int -> [(Symbol, Expr)]
dataConProj :: DataConMap -> Expr -> DataCon -> Id -> Int -> [(Symbol, Expr)]
dataConProj DataConMap
dm Expr
de DataCon
d Id
x Int
i = [(Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
x, Expr
t), (Id -> Symbol
forall t. NamedThing t => t -> Symbol
GM.simplesymbol Id
x, Expr
t)]
  where
    t :: Expr
t | DataCon -> Bool
primDataCon  DataCon
d  = Expr
de
      | Bool
otherwise       = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Maybe DataConMap -> DataCon -> Int -> Symbol
makeDataConSelector (DataConMap -> Maybe DataConMap
forall a. a -> Maybe a
Just DataConMap
dm) DataCon
d Int
i) Expr
de

primDataCon :: DataCon -> Bool
primDataCon :: DataCon -> Bool
primDataCon DataCon
d = DataCon
d DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
intDataCon

coreToIte :: C.CoreExpr -> (C.CoreExpr, C.CoreExpr) -> LogicM Expr
coreToIte :: CoreExpr
-> (CoreExpr, CoreExpr)
-> ExceptT Error (ReaderT LState Identity) Expr
coreToIte CoreExpr
e (CoreExpr
efalse, CoreExpr
etrue)
  = do p  <- CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e
       e1 <- coreToLg efalse
       e2 <- coreToLg etrue
       return $ EIte p e2 e1

toPredApp :: C.CoreExpr -> LogicM Expr
toPredApp :: CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
toPredApp CoreExpr
p = do
  allowTC <- (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a.
(LState -> a) -> ExceptT Error (ReaderT LState Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader (Config -> Bool
typeclass (Config -> Bool) -> (LState -> Config) -> LState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LState -> Config
lsConfig)
  go . first opSym . splitArgs allowTC $ p
  where
    opSym :: CoreExpr -> Maybe Symbol
opSym = CoreExpr -> Maybe Symbol
tomaybesymbol
    go :: (Maybe Symbol, [CoreExpr])
-> ExceptT Error (ReaderT LState Identity) Expr
go (Just Symbol
f, [CoreExpr
e1, CoreExpr
e2])
      | Just Brel
rel <- Symbol -> HashMap Symbol Brel -> Maybe Brel
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
f HashMap Symbol Brel
brels
      = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
rel (Expr -> Expr -> Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e1 ExceptT Error (ReaderT LState Identity) (Expr -> Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) Expr
forall a b.
ExceptT Error (ReaderT LState Identity) (a -> b)
-> ExceptT Error (ReaderT LState Identity) a
-> ExceptT Error (ReaderT LState Identity) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e2
    go (Just Symbol
f, [CoreExpr
e])
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Classes.not" :: String)
      = Expr -> Expr
forall v. ExprV v -> ExprV v
PNot (Expr -> Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e
    go (Just Symbol
f, [CoreExpr
e1, CoreExpr
e2])
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Classes.||" :: String)
      = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr ([Expr] -> Expr)
-> ExceptT Error (ReaderT LState Identity) [Expr]
-> ExceptT Error (ReaderT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr)
-> [CoreExpr] -> ExceptT Error (ReaderT LState Identity) [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg [CoreExpr
e1, CoreExpr
e2]
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Classes.&&" :: String)
      = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd ([Expr] -> Expr)
-> ExceptT Error (ReaderT LState Identity) [Expr]
-> ExceptT Error (ReaderT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr)
-> [CoreExpr] -> ExceptT Error (ReaderT LState Identity) [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg [CoreExpr
e1, CoreExpr
e2]
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"Language.Haskell.Liquid.Prelude.==>" :: String)
      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp (Expr -> Expr -> Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e1 ExceptT Error (ReaderT LState Identity) (Expr -> Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) Expr
forall a b.
ExceptT Error (ReaderT LState Identity) (a -> b)
-> ExceptT Error (ReaderT LState Identity) a
-> ExceptT Error (ReaderT LState Identity) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e2
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"Language.Haskell.Liquid.Prelude.<=>" :: String)
      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff (Expr -> Expr -> Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e1 ExceptT Error (ReaderT LState Identity) (Expr -> Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) Expr
forall a b.
ExceptT Error (ReaderT LState Identity) (a -> b)
-> ExceptT Error (ReaderT LState Identity) a
-> ExceptT Error (ReaderT LState Identity) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e2
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Base.const" :: String)
      = CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e1
    go (Just Symbol
f, [CoreExpr
es])
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Internal.Data.Foldable.or" :: String)
      = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr  ([Expr] -> Expr) -> (Expr -> [Expr]) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
deList (Expr -> Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
es
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Internal.Data.Foldable.and" :: String)
      = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd ([Expr] -> Expr) -> (Expr -> [Expr]) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
deList (Expr -> Expr)
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
es
    go (Maybe Symbol
_, [CoreExpr]
_)
      = CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
toLogicApp CoreExpr
p

    deList :: Expr -> [Expr]
    deList :: Expr -> [Expr]
deList (EApp (EApp (EVar Symbol
cons) Expr
e) Expr
es)
      | Symbol
cons Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Types.:" :: String)
      = Expr
eExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:Expr -> [Expr]
deList Expr
es
    deList (EVar Symbol
nil)
      | Symbol
nil Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Types.[]" :: String)
      = []
    deList Expr
e
      = [Expr
e]

toLogicApp :: C.CoreExpr -> LogicM Expr
toLogicApp :: CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
toLogicApp CoreExpr
e = do
  allowTC <- (LState -> Bool) -> ExceptT Error (ReaderT LState Identity) Bool
forall a.
(LState -> a) -> ExceptT Error (ReaderT LState Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader (Config -> Bool
typeclass (Config -> Bool) -> (LState -> Config) -> LState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LState -> Config
lsConfig)
  let (f, es) = splitArgs allowTC e
  case f of
    C.Var Id
_ -> do args <- (CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr)
-> [CoreExpr] -> ExceptT Error (ReaderT LState Identity) [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg [CoreExpr]
es
                  lmap <- lsSymMap <$> getState
                  def  <- (`mkEApp` args) <$> tosymbol f
                  (\LocSymbol
x -> Expr -> LogicMap -> LocSymbol -> [Expr] -> Expr
makeApp Expr
def LogicMap
lmap LocSymbol
x [Expr]
args) <$> tosymbol' f
    CoreExpr
_       -> do fe   <- CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
f
                  args <- mapM coreToLg es
                  return $ foldl EApp fe args

makeApp :: Expr -> LogicMap -> Located Symbol-> [Expr] -> Expr
makeApp :: Expr -> LogicMap -> LocSymbol -> [Expr] -> Expr
makeApp Expr
_ LogicMap
_ LocSymbol
f [Expr
e]
  | LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Internal.Num.negate" :: String)
  = Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg Expr
e
  | LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Internal.Num.fromInteger" :: String)
  , ECon Constant
c <- Expr
e
  = Constant -> Expr
forall v. Constant -> ExprV v
ECon Constant
c
  | (Symbol
modName, Symbol
sym) <- Symbol -> (Symbol, Symbol)
GM.splitModuleName (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
f)
  , String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"Ghci" :: String) Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
modName
  , Symbol
sym Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"len"
  = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
sym) Expr
e

makeApp Expr
_ LogicMap
_ LocSymbol
f [Expr
e1, Expr
e2]
  | Just Bop
op <- Symbol -> HashMap Symbol Bop -> Maybe Bop
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
f) HashMap Symbol Bop
bops
  = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
op Expr
e1 Expr
e2
  -- Hack for typeclass support. (overriden == without Eq constraint defined at Ghci)
  | (Symbol
modName, Symbol
sym) <- Symbol -> (Symbol, Symbol)
GM.splitModuleName (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
f)
  , String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"Ghci" :: String) Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
modName
  , Just Bop
op <- Symbol -> HashMap Symbol Bop -> Maybe Bop
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (Symbol -> Symbol -> Symbol
mappendSym (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Internal.Num." :: String)) Symbol
sym) HashMap Symbol Bop
bops
  = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
op Expr
e1 Expr
e2

makeApp Expr
def LogicMap
lmap LocSymbol
f [Expr]
es =
    LogicMap -> Symbol -> [Expr] -> Expr -> Expr
eAppWithMap LogicMap
lmap (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
f) [Expr]
es Expr
def
  -- where msg = "makeApp f = " ++ show f ++ " es = " ++ show es ++ " def = " ++ show def

eVarWithMap :: Id -> LogicMap -> Expr
eVarWithMap :: Id -> LogicMap -> Expr
eVarWithMap Id
x LogicMap
lmap = do
    LogicMap -> Symbol -> [Expr] -> Expr -> Expr
eAppWithMap LogicMap
lmap (Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
x) [] (Symbol -> Expr
forall v. v -> ExprV v
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
x)

brels :: M.HashMap Symbol Brel
brels :: HashMap Symbol Brel
brels = [(Symbol, Brel)] -> HashMap Symbol Brel
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Classes.==" :: String), Brel
Eq)
                   , (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Classes./=" :: String), Brel
Ne)
                   , (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Classes.>=" :: String), Brel
Ge)
                   , (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Classes.>" :: String) , Brel
Gt)
                   , (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Classes.<=" :: String), Brel
Le)
                   , (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Classes.<" :: String) , Brel
Lt)
                   ]

-- bops is a map between GHC function names/symbols and binary operators
-- from the logic. We want GHC functions like +, -, etc. to map to the
-- corresponding operators. There are actually multiple sources for +, -,
-- they can come from GHC.Prim, GHC.Internal.Num, GHC.Internal.Real or
-- be an instance of Num for Int.
bops :: M.HashMap Symbol Bop
bops :: HashMap Symbol Bop
bops = [(Symbol, Bop)] -> HashMap Symbol Bop
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (String -> Symbol
numSymbol String
"+", Bop
Plus)
                  , (String -> Symbol
numIntSymbol String
"+", Bop
Plus)
                  , (String -> Symbol
primSymbol String
"+#", Bop
Plus)
                  , (String -> Symbol
numSymbol String
"-", Bop
Minus)
                  , (String -> Symbol
numIntSymbol String
"-", Bop
Minus)
                  , (String -> Symbol
primSymbol String
"-#", Bop
Minus)
                  , (String -> Symbol
numSymbol String
"*", Bop
Times)
                  , (String -> Symbol
numIntSymbol String
"*", Bop
Times)
                  , (String -> Symbol
primSymbol String
"*#", Bop
Times)
                  , (String -> Symbol
numSymbol String
"/", Bop
Div)
                  , (String -> Symbol
realSymbol String
"/", Bop
Div)
                  , (String -> Symbol
numSymbol String
"%", Bop
Mod)
                  ]
  where
    primSymbol :: String -> Symbol
    primSymbol :: String -> Symbol
primSymbol =  String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> (String -> String) -> String -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
forall a. [a] -> [a] -> [a]
(++) String
"GHC.Prim."
    numSymbol :: String -> Symbol
    numSymbol :: String -> Symbol
numSymbol =  String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> (String -> String) -> String -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
forall a. [a] -> [a] -> [a]
(++) String
"GHC.Internal.Num."
    numIntSymbol :: String -> Symbol
    numIntSymbol :: String -> Symbol
numIntSymbol = String -> Symbol
numSymbol (String -> Symbol) -> (String -> String) -> String -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
forall a. [a] -> [a] -> [a]
(++) String
"$fNumInt_$c"
    realSymbol :: String -> Symbol
    realSymbol :: String -> Symbol
realSymbol =  String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> (String -> String) -> String -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
forall a. [a] -> [a] -> [a]
(++) String
"GHC.Internal.Real."

splitArgs :: Bool -> C.Expr t -> (C.Expr t, [C.Arg t])
splitArgs :: forall t. Bool -> Expr t -> (Expr t, [Expr t])
splitArgs Bool
allowTC Expr t
exprt = (Expr t
exprt', [Expr t] -> [Expr t]
forall a. [a] -> [a]
reverse [Expr t]
args)
 where
    (Expr t
exprt', [Expr t]
args) = Expr t -> (Expr t, [Expr t])
forall {b}. Arg b -> (Arg b, [Arg b])
go Expr t
exprt

    go :: Arg b -> (Arg b, [Arg b])
go (C.App (C.Var Id
i) Arg b
e) | Id -> Bool
ignoreVar Id
i       = Arg b -> (Arg b, [Arg b])
go Arg b
e
    go (C.App Arg b
f (C.Var Id
v)) | if Bool
allowTC then Id -> Bool
GM.isEmbeddedDictVar Id
v else Id -> Bool
isErasable Id
v   = Arg b -> (Arg b, [Arg b])
go Arg b
f
    go (C.App Arg b
f Arg b
e) = (Arg b
f', Arg b
eArg b -> [Arg b] -> [Arg b]
forall a. a -> [a] -> [a]
:[Arg b]
es) where (Arg b
f', [Arg b]
es) = Arg b -> (Arg b, [Arg b])
go Arg b
f
    go Arg b
f           = (Arg b
f, [])

tomaybesymbol :: C.CoreExpr -> Maybe Symbol
tomaybesymbol :: CoreExpr -> Maybe Symbol
tomaybesymbol (C.Var Id
x) = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (Symbol -> Maybe Symbol) -> Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
x
tomaybesymbol CoreExpr
_         = Maybe Symbol
forall a. Maybe a
Nothing

tosymbol :: C.CoreExpr -> LogicM (Located Symbol)
tosymbol :: CoreExpr -> ExceptT Error (ReaderT LState Identity) LocSymbol
tosymbol CoreExpr
e
 = case CoreExpr -> Maybe Symbol
tomaybesymbol CoreExpr
e of
    Just Symbol
x -> LocSymbol -> ExceptT Error (ReaderT LState Identity) LocSymbol
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol -> ExceptT Error (ReaderT LState Identity) LocSymbol)
-> LocSymbol -> ExceptT Error (ReaderT LState Identity) LocSymbol
forall a b. (a -> b) -> a -> b
$ Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
x
    Maybe Symbol
_      -> String -> ExceptT Error (ReaderT LState Identity) LocSymbol
forall a. String -> LogicM a
throw (String
"Bad Measure Definition:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall a. Outputable a => a -> String
GM.showPpr CoreExpr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\t cannot be applied")

tosymbol' :: C.CoreExpr -> LogicM (Located Symbol)
tosymbol' :: CoreExpr -> ExceptT Error (ReaderT LState Identity) LocSymbol
tosymbol' (C.Var Id
x) = LocSymbol -> ExceptT Error (ReaderT LState Identity) LocSymbol
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol -> ExceptT Error (ReaderT LState Identity) LocSymbol)
-> LocSymbol -> ExceptT Error (ReaderT LState Identity) LocSymbol
forall a b. (a -> b) -> a -> b
$ Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Symbol -> LocSymbol) -> Symbol -> LocSymbol
forall a b. (a -> b) -> a -> b
$ Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
x
tosymbol' CoreExpr
e        = String -> ExceptT Error (ReaderT LState Identity) LocSymbol
forall a. String -> LogicM a
throw (String
"Bad Measure Definition:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall a. Outputable a => a -> String
GM.showPpr CoreExpr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\t cannot be applied")

makesub :: C.CoreBind -> LogicM (Symbol, Expr)
makesub :: Bind Id -> ExceptT Error (ReaderT LState Identity) (Symbol, Expr)
makesub (C.NonRec Id
x CoreExpr
e) = (Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
x,) (Expr -> (Symbol, Expr))
-> ExceptT Error (ReaderT LState Identity) Expr
-> ExceptT Error (ReaderT LState Identity) (Symbol, Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (ReaderT LState Identity) Expr
coreToLg CoreExpr
e
makesub Bind Id
_              = String -> ExceptT Error (ReaderT LState Identity) (Symbol, Expr)
forall a. String -> LogicM a
throw String
"Cannot make Logical Substitution of Recursive Definitions"

mkLit :: Literal -> Maybe Expr
mkLit :: Literal -> Maybe Expr
mkLit (LitNumber LitNumType
_ Integer
n) = Integer -> Maybe Expr
mkI Integer
n
-- mkLit (MachInt64  n)    = mkI n
-- mkLit (MachWord   n)    = mkI n
-- mkLit (MachWord64 n)    = mkI n
-- mkLit (LitInteger n _)  = mkI n
mkLit (LitFloat  Rational
n)    = Rational -> Maybe Expr
mkR Rational
n
mkLit (LitDouble Rational
n)    = Rational -> Maybe Expr
mkR Rational
n
mkLit (LitString    ByteString
s)    = ByteString -> Maybe Expr
mkS ByteString
s
mkLit (LitChar   Char
c)    = Char -> Maybe Expr
mkC Char
c
mkLit Literal
_                 = Maybe Expr
forall a. Maybe a
Nothing -- ELit sym sort

mkI :: Integer -> Maybe Expr
mkI :: Integer -> Maybe Expr
mkI = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> (Integer -> Expr) -> Integer -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Expr
forall v. Constant -> ExprV v
ECon (Constant -> Expr) -> (Integer -> Constant) -> Integer -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Constant
I

mkR :: Rational -> Maybe Expr
mkR :: Rational -> Maybe Expr
mkR                    = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr)
-> (Rational -> Expr) -> Rational -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Expr
forall v. Constant -> ExprV v
ECon (Constant -> Expr) -> (Rational -> Constant) -> Rational -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Constant
F.R (Double -> Constant)
-> (Rational -> Double) -> Rational -> Constant
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
forall a. Fractional a => Rational -> a
fromRational

mkS :: ByteString -> Maybe Expr
mkS :: ByteString -> Maybe Expr
mkS                    = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr)
-> (ByteString -> Expr) -> ByteString -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymConst -> Expr
forall v. SymConst -> ExprV v
ESym (SymConst -> Expr)
-> (ByteString -> SymConst) -> ByteString -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> SymConst
SL  (Text -> SymConst)
-> (ByteString -> Text) -> ByteString -> SymConst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OnDecodeError -> ByteString -> Text
decodeUtf8With OnDecodeError
lenientDecode

mkC :: Char -> Maybe Expr
mkC :: Char -> Maybe Expr
mkC                    = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> (Char -> Expr) -> Char -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Expr
forall v. Constant -> ExprV v
ECon (Constant -> Expr) -> (Char -> Constant) -> Char -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Sort -> Constant
`F.L` Sort
F.charSort)  (Text -> Constant) -> (Char -> Text) -> Char -> Constant
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Text
repr
  where
    repr :: Char -> Text
repr               = String -> Text
T.pack (String -> Text) -> (Char -> String) -> Char -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> String) -> (Char -> Int) -> Char -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
Data.Char.ord

ignoreVar :: Id -> Bool
ignoreVar :: Id -> Bool
ignoreVar Id
i = Id -> Symbol
simpleSymbolVar Id
i Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol
"I#", Symbol
"D#"]

-- | Tries to determine if a 'CoreAlt' maps to one of the 'Integer' type constructors.
-- We need the disjuction for GHC >= 9, where the Integer now comes from the \"ghc-bignum\" package,
-- and it has different names for the constructors.
isBangInteger :: [C.CoreAlt] -> Bool
isBangInteger :: [CoreAlt] -> Bool
isBangInteger [Alt (C.DataAlt DataCon
s) [Id]
_ CoreExpr
_, Alt (C.DataAlt DataCon
jp) [Id]
_ CoreExpr
_, Alt (C.DataAlt DataCon
jn) [Id]
_ CoreExpr
_]
  =  (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCon
s  Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Integer.Type.S#"  Bool -> Bool -> Bool
|| DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCon
s  Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Num.Integer.IS")
  Bool -> Bool -> Bool
&& (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCon
jp Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Integer.Type.Jp#" Bool -> Bool -> Bool
|| DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCon
jp Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Num.Integer.IP")
  Bool -> Bool -> Bool
&& (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCon
jn Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Integer.Type.Jn#" Bool -> Bool -> Bool
|| DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCon
jn Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Num.Integer.IN")
isBangInteger [CoreAlt]
_ = Bool
False

isErasable :: Id -> Bool
isErasable :: Id -> Bool
isErasable Id
v = String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
F.notracepp String
msg (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Id -> Bool
isGhcSplId Id
v Bool -> Bool -> Bool
&& Bool -> Bool
not (Id -> Bool
isDCId Id
v)
  where
    msg :: String
msg      = String
"isErasable: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Id, IdDetails) -> String
forall a. Outputable a => a -> String
GM.showPpr (Id
v, Id -> IdDetails
Ghc.idDetails Id
v)

isGhcSplId :: Id -> Bool
isGhcSplId :: Id -> Bool
isGhcSplId Id
v = Symbol -> Symbol -> Bool
isPrefixOfSym (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"$" :: String)) (Id -> Symbol
simpleSymbolVar Id
v)

isDCId :: Id -> Bool
isDCId :: Id -> Bool
isDCId Id
v = case Id -> IdDetails
Ghc.idDetails Id
v of
  DataConWorkId DataCon
_ -> Bool
True
  DataConWrapId DataCon
_ -> Bool
True
  IdDetails
_               -> Bool
False

isANF :: Id -> Bool
isANF :: Id -> Bool
isANF      Id
v = Symbol -> Symbol -> Bool
isPrefixOfSym (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"lq_anf" :: String)) (Id -> Symbol
simpleSymbolVar Id
v)

isDead :: Id -> Bool
isDead :: Id -> Bool
isDead     = OccInfo -> Bool
isDeadOcc (OccInfo -> Bool) -> (Id -> OccInfo) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdInfo -> OccInfo
occInfo (IdInfo -> OccInfo) -> (Id -> IdInfo) -> Id -> OccInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasDebugCallStack => Id -> IdInfo
Id -> IdInfo
Ghc.idInfo

class Simplify a where
  simplify :: Bool -> a -> a
  inline   :: (Id -> Bool) -> a -> a

  normalize :: Bool -> a -> a
  normalize Bool
allowTC = a -> a
inline_preds (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
inline_anf (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> a -> a
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC
   where
    inline_preds :: a -> a
inline_preds = (Id -> Bool) -> a -> a
forall a. Simplify a => (Id -> Bool) -> a -> a
inline (Type -> Type -> Bool
eqType Type
boolTy (Type -> Bool) -> (Id -> Type) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
GM.expandVarType)
    inline_anf :: a -> a
inline_anf   = (Id -> Bool) -> a -> a
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
isANF

instance Simplify C.CoreExpr where
  simplify :: Bool -> CoreExpr -> CoreExpr
simplify Bool
_ e :: CoreExpr
e@(C.Var Id
_)
    = CoreExpr
e
  simplify Bool
_ e :: CoreExpr
e@(C.Lit Literal
_)
    = CoreExpr
e
  simplify Bool
allowTC (C.App CoreExpr
e (C.Type Type
_))
    = Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
allowTC (C.App CoreExpr
e (C.Var Id
dict))  | (if Bool
allowTC then Id -> Bool
GM.isEmbeddedDictVar else Id -> Bool
isErasable) Id
dict
    = Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
allowTC (C.App (C.Lam Id
x CoreExpr
e) CoreExpr
_)   | Id -> Bool
isDead Id
x
    = Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
allowTC (C.App CoreExpr
e1 CoreExpr
e2)
    = CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
C.App (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e1) (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e2)
  simplify Bool
allowTC (C.Lam Id
x CoreExpr
e) | Id -> Bool
isTyVar Id
x
    = Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
allowTC (C.Lam Id
x CoreExpr
e) | (if Bool
allowTC then Id -> Bool
GM.isEmbeddedDictVar else Id -> Bool
isErasable) Id
x
    = Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
allowTC (C.Lam Id
x CoreExpr
e)
    = Id -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
C.Lam Id
x (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e)
  simplify Bool
allowTC (C.Let (C.NonRec Id
x CoreExpr
_) CoreExpr
e) | (if Bool
allowTC then Id -> Bool
GM.isEmbeddedDictVar else Id -> Bool
isErasable) Id
x
    = Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
allowTC (C.Let (C.Rec [(Id, CoreExpr)]
xes) CoreExpr
e)    | ((Id, CoreExpr) -> Bool) -> [(Id, CoreExpr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((if Bool
allowTC then Id -> Bool
GM.isEmbeddedDictVar else Id -> Bool
isErasable) (Id -> Bool) -> ((Id, CoreExpr) -> Id) -> (Id, CoreExpr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, CoreExpr) -> Id
forall a b. (a, b) -> a
fst) [(Id, CoreExpr)]
xes
    = Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
allowTC (C.Let Bind Id
xes CoreExpr
e)
    = Bind Id -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
C.Let (Bool -> Bind Id -> Bind Id
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC Bind Id
xes) (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e)
  simplify Bool
allowTC (C.Case CoreExpr
e Id
x Type
_t alts :: [CoreAlt]
alts@[Alt AltCon
_ [Id]
_ CoreExpr
ee,CoreAlt
_,CoreAlt
_]) | [CoreAlt] -> Bool
isBangInteger [CoreAlt]
alts
  -- XXX(matt): seems to be for debugging?
    = -- Misc.traceShow ("To simplify allowTC case") $
       HashMap Id CoreExpr -> CoreExpr -> CoreExpr
forall a. Subable a => HashMap Id CoreExpr -> a -> a
sub (Id -> CoreExpr -> HashMap Id CoreExpr
forall k v. Hashable k => k -> v -> HashMap k v
M.singleton Id
x (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e)) (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
ee)
  simplify Bool
allowTC (C.Case CoreExpr
e Id
x Type
t [CoreAlt]
alts)
    = CoreExpr -> Id -> Type -> [CoreAlt] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
C.Case (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e) Id
x Type
t ((CoreAlt -> Bool) -> [CoreAlt] -> [CoreAlt]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (CoreAlt -> Bool) -> CoreAlt -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreAlt -> Bool
isPatErrorAlt) (Bool -> CoreAlt -> CoreAlt
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC (CoreAlt -> CoreAlt) -> [CoreAlt] -> [CoreAlt]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreAlt]
alts))
  simplify Bool
allowTC (C.Cast CoreExpr
e Coercion
c)
    = CoreExpr -> Coercion -> CoreExpr
forall b. Expr b -> Coercion -> Expr b
C.Cast (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e) Coercion
c
  simplify Bool
allowTC (C.Tick CoreTickish
_ CoreExpr
e)
    = Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
_ (C.Coercion Coercion
c)
    = Coercion -> CoreExpr
forall b. Coercion -> Expr b
C.Coercion Coercion
c
  simplify Bool
_ (C.Type Type
t)
    = Type -> CoreExpr
forall b. Type -> Expr b
C.Type Type
t

  inline :: (Id -> Bool) -> CoreExpr -> CoreExpr
inline Id -> Bool
p (C.Let (C.NonRec Id
x CoreExpr
ex) CoreExpr
e) | Id -> Bool
p Id
x
                               = HashMap Id CoreExpr -> CoreExpr -> CoreExpr
forall a. Subable a => HashMap Id CoreExpr -> a -> a
sub (Id -> CoreExpr -> HashMap Id CoreExpr
forall k v. Hashable k => k -> v -> HashMap k v
M.singleton Id
x ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
ex)) ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e)
  inline Id -> Bool
p (C.Let Bind Id
xes CoreExpr
e)       = Bind Id -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
C.Let ((Id -> Bool) -> Bind Id -> Bind Id
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p Bind Id
xes) ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e)
  inline Id -> Bool
p (C.App CoreExpr
e1 CoreExpr
e2)       = CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
C.App ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e1) ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e2)
  inline Id -> Bool
p (C.Lam Id
x CoreExpr
e)         = Id -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
C.Lam Id
x ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e)
  inline Id -> Bool
p (C.Case CoreExpr
e Id
x Type
t [CoreAlt]
alts) = CoreExpr -> Id -> Type -> [CoreAlt] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
C.Case ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e) Id
x Type
t ((Id -> Bool) -> CoreAlt -> CoreAlt
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p (CoreAlt -> CoreAlt) -> [CoreAlt] -> [CoreAlt]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreAlt]
alts)
  inline Id -> Bool
p (C.Cast CoreExpr
e Coercion
c)        = CoreExpr -> Coercion -> CoreExpr
forall b. Expr b -> Coercion -> Expr b
C.Cast ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e) Coercion
c
  inline Id -> Bool
p (C.Tick CoreTickish
t CoreExpr
e)        = CoreTickish -> CoreExpr -> CoreExpr
forall b. CoreTickish -> Expr b -> Expr b
C.Tick CoreTickish
t ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e)
  inline Id -> Bool
_ (C.Var Id
x)           = Id -> CoreExpr
forall b. Id -> Expr b
C.Var Id
x
  inline Id -> Bool
_ (C.Lit Literal
l)           = Literal -> CoreExpr
forall b. Literal -> Expr b
C.Lit Literal
l
  inline Id -> Bool
_ (C.Coercion Coercion
c)      = Coercion -> CoreExpr
forall b. Coercion -> Expr b
C.Coercion Coercion
c
  inline Id -> Bool
_ (C.Type Type
t)          = Type -> CoreExpr
forall b. Type -> Expr b
C.Type Type
t


instance Simplify C.CoreBind where
  simplify :: Bool -> Bind Id -> Bind Id
simplify Bool
allowTC (C.NonRec Id
x CoreExpr
e) = Id -> CoreExpr -> Bind Id
forall b. b -> Expr b -> Bind b
C.NonRec Id
x (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e)
  simplify Bool
allowTC (C.Rec [(Id, CoreExpr)]
xes)    = [(Id, CoreExpr)] -> Bind Id
forall b. [(b, Expr b)] -> Bind b
C.Rec ((CoreExpr -> CoreExpr) -> (Id, CoreExpr) -> (Id, CoreExpr)
forall a b. (a -> b) -> (Id, a) -> (Id, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC) ((Id, CoreExpr) -> (Id, CoreExpr))
-> [(Id, CoreExpr)] -> [(Id, CoreExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Id, CoreExpr)]
xes )

  inline :: (Id -> Bool) -> Bind Id -> Bind Id
inline Id -> Bool
p (C.NonRec Id
x CoreExpr
e) = Id -> CoreExpr -> Bind Id
forall b. b -> Expr b -> Bind b
C.NonRec Id
x ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e)
  inline Id -> Bool
p (C.Rec [(Id, CoreExpr)]
xes)    = [(Id, CoreExpr)] -> Bind Id
forall b. [(b, Expr b)] -> Bind b
C.Rec ((CoreExpr -> CoreExpr) -> (Id, CoreExpr) -> (Id, CoreExpr)
forall a b. (a -> b) -> (Id, a) -> (Id, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p) ((Id, CoreExpr) -> (Id, CoreExpr))
-> [(Id, CoreExpr)] -> [(Id, CoreExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Id, CoreExpr)]
xes)

instance Simplify C.CoreAlt where
  simplify :: Bool -> CoreAlt -> CoreAlt
simplify Bool
allowTC (Alt AltCon
c [Id]
xs CoreExpr
e) = AltCon -> [Id] -> CoreExpr -> CoreAlt
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Id]
xs (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e)
    -- where xs   = F.tracepp _msg xs0
    --      _msg = "isCoVars? " ++ F.showpp [(x, isCoVar x, varType x) | x <- xs0]
  inline :: (Id -> Bool) -> CoreAlt -> CoreAlt
inline Id -> Bool
p (Alt AltCon
c [Id]
xs CoreExpr
e) = AltCon -> [Id] -> CoreExpr -> CoreAlt
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Id]
xs ((Id -> Bool) -> CoreExpr -> CoreExpr
forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e)