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

{-# OPTIONS_GHC -Wno-orphans #-}

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

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, 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.State
import           Control.Monad.Except
import           Control.Monad.Identity
import qualified Language.Fixpoint.Misc                as Misc
import qualified Language.Haskell.Liquid.Misc          as Misc
import           Language.Fixpoint.Types               hiding (panic, Error, R, simplify)
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.Types   --     hiding (GhcInfo(..), GhcSpec (..), LM)
import           Language.Haskell.Liquid.Types.RefType

import qualified Data.HashMap.Strict                   as M

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

{- | [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 = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar RReft -> SpecType)
-> RTypeRep RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft
rep {ty_res = res `strengthen` r , ty_binds = xs}
  where
    r :: RReft
r              = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft (Expr -> Reft
mkReft (LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
f ((Symbol, SpecType) -> Expr
forall {b}. (Symbol, b) -> Expr
mkA ((Symbol, SpecType) -> Expr) -> [(Symbol, SpecType)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
vxs))) Predicate
forall a. Monoid a => a
mempty
    rep :: RTypeRep RTyCon RTyVar RReft
rep            = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t
    res :: SpecType
res            = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep 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
$ RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep 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 {t} {t1}. RType 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 (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
rep)
    isErasable' :: RType RTyCon t t1 -> Bool
isErasable'    = if Bool
allowTC then RType RTyCon t t1 -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass else RType RTyCon t t1 -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType
    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 :: (Symbol, b) -> Expr
mkA            = Symbol -> Expr
EVar (Symbol -> Expr) -> ((Symbol, b) -> Symbol) -> (Symbol, b) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, b) -> Symbol
forall a b. (a, b) -> a
fst
    mkReft :: Expr -> Reft
mkReft         = if SpecType -> Bool
forall {t} {t1}. RType RTyCon t t1 -> Bool
isBool SpecType
res then Expr -> Reft
forall a. Predicate a => a -> Reft
propReft else Expr -> Reft
forall a. Expression a => a -> Reft
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} {tv}.
(TyConable c, Reftable r, Show a) =>
([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType c tv r
go [Symbol] -> RReft
mkT [] [(Int
1::Int)..] SpecType
st
  where
    mkReft :: Expr -> Reft
mkReft | Bool
boolRes   = Expr -> Reft
forall a. Predicate a => a -> Reft
propReft
           | Bool
otherwise = Expr -> Reft
forall a. Expression a => a -> Reft
exprReft
    mkT :: [Symbol] -> RReft
mkT [Symbol]
xs          = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft (Expr -> Reft
mkReft (Expr -> Reft) -> Expr -> Reft
forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
locSym (Symbol -> Expr
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)) Predicate
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
$ RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res (RTypeRep RTyCon RTyVar RReft -> SpecType)
-> RTypeRep RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
st

    go :: ([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i (RAllT RTVU c tv
a RType c tv r
t r
r)    = RTVU c tv -> RType c tv r -> r -> RType c tv r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a (([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i RType c tv r
t) r
r
    go [Symbol] -> r
f [Symbol]
args [a]
i (RAllP PVU c tv
p RType c tv r
t)      = PVU c tv -> RType c tv r -> RType c tv r
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
p (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ ([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i RType c tv r
t
    go [Symbol] -> r
f [Symbol]
args [a]
i (RFun Symbol
x RFInfo
ii RType c tv r
t1 RType c tv r
t2 r
r)
     | (if Bool
allowTC then RType c tv r -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass else RType c tv r -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType) RType c tv r
t1           = Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
ii RType c tv r
t1 (([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i RType c tv r
t2) r
r
    go [Symbol] -> r
f [Symbol]
args [a]
i t :: RType c tv r
t@(RFun Symbol
_ RFInfo
ii RType c tv r
t1 RType c tv r
t2 r
r)
     | RType c tv r -> Bool
forall {c} {tv} {r}. RType c tv r -> Bool
hasRApps RType c tv r
t               = Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x' RFInfo
ii RType c tv r
t1 (([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType 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) RType 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]
_ RType c tv r
t                = RType c tv r
t RType c tv r -> r -> RType c tv r
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` [Symbol] -> r
f [Symbol]
args

    hasRApps :: RType c tv r -> Bool
hasRApps (RFun Symbol
_ RFInfo
_ RType c tv r
t1 RType c tv r
t2 r
_) = RType c tv r -> Bool
hasRApps RType c tv r
t1 Bool -> Bool -> Bool
|| RType c tv r -> Bool
hasRApps RType c tv r
t2
    hasRApps RApp {}          = Bool
True
    hasRApps RType 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'           = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar RReft -> SpecType)
-> RTypeRep RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft
rep { ty_res = mapExprReft weaken (ty_res rep) }
    rep :: RTypeRep RTyCon RTyVar RReft
rep          = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t
    weaken :: Symbol -> Expr -> Expr
weaken Symbol
x     = [Expr] -> Expr
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]
conjuncts
    vE :: Expr
vE           = LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
vF [Expr]
xs
    xs :: [Expr]
xs           = Symbol -> Expr
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 t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass else SpecType -> Bool
forall c t t1. TyConable c => RType 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 (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
rep) (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep 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 (StateT 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
  }

throw :: String -> LogicM a
throw :: forall a. String -> LogicM a
throw String
str = do
  String -> Error
fmkError  <- (LState -> String -> Error)
-> ExceptT Error (StateT LState Identity) (String -> Error)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets LState -> String -> Error
lsError
  Error -> LogicM a
forall a. Error -> ExceptT Error (StateT LState Identity) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error -> LogicM a) -> Error -> LogicM a
forall a b. (a -> b) -> a -> b
$ String -> Error
fmkError String
str

getState :: LogicM LState
getState :: LogicM LState
getState = LogicM LState
forall s (m :: * -> *). MonadState s m => m s
get

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

runToLogicWithBoolBinds
  :: [Var] -> TCEmb TyCon -> LogicMap -> DataConMap -> (String -> Error)
  -> LogicM t -> Either Error t
runToLogicWithBoolBinds :: forall t.
[Id]
-> TCEmb TyCon
-> LogicMap
-> DataConMap
-> (String -> Error)
-> LogicM t
-> Either Error t
runToLogicWithBoolBinds [Id]
xs TCEmb TyCon
tce LogicMap
lmap DataConMap
dm String -> Error
ferror LogicM t
m
  = State LState (Either Error t) -> LState -> Either Error t
forall s a. State s a -> s -> a
evalState (LogicM t -> State 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
      }

coreAltToDef :: (Reftable r) => Bool -> LocSymbol -> Var -> [Var] -> Var -> Type -> [C.CoreAlt]
             -> LogicM [Def (Located (RRType r)) DataCon]
coreAltToDef :: forall r.
Reftable r =>
Bool
-> LocSymbol
-> Id
-> [Id]
-> Id
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
coreAltToDef Bool
allowTC LocSymbol
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) = LocSymbol -> String -> LogicM [Def (Located (RRType r)) DataCon]
forall a. LocSymbol -> String -> a
measureFail LocSymbol
locSym String
"Cannot lift definition with literal alternatives"
  | Bool
otherwise          = do
      [Def (Located (RRType r)) DataCon]
d1s <- String
-> [Def (Located (RRType r)) DataCon]
-> [Def (Located (RRType r)) DataCon]
forall a. PPrint a => String -> a -> a
F.notracepp String
"coreAltDefs-1" ([Def (Located (RRType r)) DataCon]
 -> [Def (Located (RRType r)) DataCon])
-> LogicM [Def (Located (RRType r)) DataCon]
-> LogicM [Def (Located (RRType r)) DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoreAlt
 -> ExceptT
      Error (StateT LState Identity) (Def (Located (RRType r)) DataCon))
-> [CoreAlt] -> LogicM [Def (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 (LocSymbol
-> (Expr -> Body)
-> [Id]
-> Id
-> CoreAlt
-> ExceptT
     Error (StateT LState Identity) (Def (Located (RRType r)) DataCon)
forall {r} {p}.
Reftable r =>
LocSymbol
-> (Expr -> Body)
-> p
-> Id
-> CoreAlt
-> ExceptT
     Error (StateT LState Identity) (Def (Located (RRType r)) DataCon)
mkAlt LocSymbol
locSym Expr -> Body
cc [Id]
myArgs Id
z) [CoreAlt]
dataAlts
      [Def (Located (RRType r)) DataCon]
d2s <- String
-> [Def (Located (RRType r)) DataCon]
-> [Def (Located (RRType r)) DataCon]
forall a. PPrint a => String -> a -> a
F.notracepp String
"coreAltDefs-2" ([Def (Located (RRType r)) DataCon]
 -> [Def (Located (RRType r)) DataCon])
-> LogicM [Def (Located (RRType r)) DataCon]
-> LogicM [Def (Located (RRType r)) DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>       LocSymbol
-> (Expr -> Body)
-> [Id]
-> Id
-> Maybe [(DataCon, [Id], [Type])]
-> Maybe CoreExpr
-> LogicM [Def (Located (RRType r)) DataCon]
forall {r} {p} {ctor} {b}.
Reftable r =>
LocSymbol
-> (Expr -> Body)
-> p
-> Id
-> Maybe [(ctor, b, [Type])]
-> Maybe CoreExpr
-> ExceptT
     Error (StateT LState Identity) [Def (Located (RRType r)) ctor]
mkDef LocSymbol
locSym Expr -> Body
cc [Id]
myArgs Id
z  Maybe [(DataCon, [Id], [Type])]
defAlts Maybe CoreExpr
defExpr
      [Def (Located (RRType r)) DataCon]
-> LogicM [Def (Located (RRType r)) DataCon]
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Def (Located (RRType r)) DataCon]
d1s [Def (Located (RRType r)) DataCon]
-> [Def (Located (RRType r)) DataCon]
-> [Def (Located (RRType r)) DataCon]
forall a. [a] -> [a] -> [a]
++ [Def (Located (RRType r)) DataCon]
d2s)
  where
    myArgs :: [Id]
myArgs   = [Id] -> [Id]
forall a. [a] -> [a]
reverse [Id]
zs
    cc :: Expr -> Body
cc       = if Type -> Type -> Bool
eqType Type
t Type
boolTy then Expr -> Body
P else Expr -> Body
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 :: LocSymbol
-> (Expr -> Body)
-> p
-> Id
-> CoreAlt
-> ExceptT
     Error (StateT LState Identity) (Def (Located (RRType r)) DataCon)
mkAlt LocSymbol
x Expr -> Body
ctor p
_args Id
dx (Alt (C.DataAlt DataCon
d) [Id]
xs CoreExpr
e)
      = LocSymbol
-> DataCon
-> Maybe (Located (RRType r))
-> [(Symbol, Maybe (Located (RRType r)))]
-> Body
-> Def (Located (RRType r)) DataCon
forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
x {- (toArgs id args) -} DataCon
d (Located (RRType r) -> Maybe (Located (RRType r))
forall a. a -> Maybe a
Just (Located (RRType r) -> Maybe (Located (RRType r)))
-> Located (RRType r) -> Maybe (Located (RRType r))
forall a b. (a -> b) -> a -> b
$ Id -> Located (RRType r)
forall r. Reftable r => Id -> Located (RRType r)
varRType Id
dx) ((Located (RRType r) -> Maybe (Located (RRType r)))
-> [Id] -> [(Symbol, Maybe (Located (RRType r)))]
forall r b.
Reftable r =>
(Located (RRType r) -> b) -> [Id] -> [(Symbol, b)]
toArgs Located (RRType r) -> Maybe (Located (RRType r))
forall a. a -> Maybe a
Just [Id]
xs')
      (Body -> Def (Located (RRType r)) DataCon)
-> (Expr -> Body) -> Expr -> Def (Located (RRType r)) DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Body
ctor
      (Expr -> Body) -> (Expr -> Expr) -> Expr -> Body
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
`subst1` (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
dx, LocSymbol -> [Expr] -> Expr
F.mkEApp (DataCon -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol DataCon
d) (Id -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (Id -> Expr) -> [Id] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Id]
xs')))
     (Expr -> Def (Located (RRType r)) DataCon)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT
     Error (StateT LState Identity) (Def (Located (RRType r)) DataCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e
      where xs' :: [Id]
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
    mkAlt LocSymbol
_ Expr -> Body
_ p
_ Id
_ CoreAlt
alt
      = String
-> ExceptT
     Error (StateT LState Identity) (Def (Located (RRType r)) DataCon)
forall a. String -> LogicM a
throw (String
 -> ExceptT
      Error (StateT LState Identity) (Def (Located (RRType r)) DataCon))
-> String
-> ExceptT
     Error (StateT LState Identity) (Def (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 :: LocSymbol
-> (Expr -> Body)
-> p
-> Id
-> Maybe [(ctor, b, [Type])]
-> Maybe CoreExpr
-> ExceptT
     Error (StateT LState Identity) [Def (Located (RRType r)) ctor]
mkDef LocSymbol
x Expr -> Body
ctor p
_args Id
dx (Just [(ctor, b, [Type])]
dtss) (Just CoreExpr
e) = do
      Body
eDef   <- Expr -> Body
ctor (Expr -> Body)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Body
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e
      -- let ys  = toArgs id args
      let dxt :: Maybe (Located (RRType r))
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)
      [Def (Located (RRType r)) ctor]
-> ExceptT
     Error (StateT LState Identity) [Def (Located (RRType r)) ctor]
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return  [ LocSymbol
-> ctor
-> Maybe (Located (RRType r))
-> [(Symbol, Maybe (Located (RRType r)))]
-> Body
-> Def (Located (RRType r)) ctor
forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
x {- ys -} ctor
d Maybe (Located (RRType r))
dxt (LocSymbol -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]
forall r.
Monoid r =>
LocSymbol -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]
defArgs LocSymbol
x [Type]
ts) Body
eDef | (ctor
d, b
_, [Type]
ts) <- [(ctor, b, [Type])]
dtss ]

    mkDef LocSymbol
_ Expr -> Body
_ p
_ Id
_ Maybe [(ctor, b, [Type])]
_ Maybe CoreExpr
_ =
      [Def (Located (RRType r)) ctor]
-> ExceptT
     Error (StateT LState Identity) [Def (Located (RRType r)) ctor]
forall a. a -> ExceptT Error (StateT 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 => LocSymbol -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]
defArgs :: forall r.
Monoid r =>
LocSymbol -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]
defArgs LocSymbol
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 (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
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
. LocSymbol -> RRType r -> Located (RRType r)
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
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 => Bool -> LocSymbol -> Var -> C.CoreExpr
          -> LogicM [Def (Located (RRType r)) DataCon]
coreToDef :: forall r.
Reftable r =>
Bool
-> LocSymbol
-> Id
-> CoreExpr
-> LogicM [Def (Located (RRType r)) DataCon]
coreToDef Bool
allowTC LocSymbol
locSym Id
_                   = [Id] -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
forall {r}.
Reftable r =>
[Id] -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
go [] (CoreExpr -> LogicM [Def (Located (RRType r)) DataCon])
-> (CoreExpr -> CoreExpr)
-> CoreExpr
-> LogicM [Def (Located (RRType r)) DataCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> CoreExpr
inlinePreds (CoreExpr -> CoreExpr)
-> (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC
  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) = Bool
-> LocSymbol
-> Id
-> [Id]
-> Id
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
forall r.
Reftable r =>
Bool
-> LocSymbol
-> Id
-> [Id]
-> Id
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
coreAltToDef Bool
allowTC LocSymbol
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  = Bool
-> LocSymbol
-> Id
-> [Id]
-> Id
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
forall r.
Reftable r =>
Bool
-> LocSymbol
-> Id
-> [Id]
-> Id
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
coreAltToDef Bool
allowTC LocSymbol
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
_                        = LocSymbol -> String -> LogicM [Def (Located (RRType r)) DataCon]
forall a. LocSymbol -> String -> a
measureFail LocSymbol
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       :: LocSymbol -> String -> a
measureFail :: forall a. LocSymbol -> String -> a
measureFail LocSymbol
x String
msg = Maybe SrcSpan -> String -> a
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
sp String
e
  where
    sp :: Maybe SrcSpan
sp            = SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSymbol
x)
    e :: String
e             = String -> String -> String -> String
forall r. PrintfType r => String -> r
Printf.printf String
"Cannot create measure '%s': %s" (LocSymbol -> String
forall a. PPrint a => a -> String
F.showpp LocSymbol
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 :: Bool -> LocSymbol -> Var -> C.CoreExpr ->  LogicM ([Var], Either Expr Expr)
coreToFun :: Bool
-> LocSymbol -> Id -> CoreExpr -> LogicM ([Id], Either Expr Expr)
coreToFun Bool
allowTC LocSymbol
_ Id
_v = [Id] -> CoreExpr -> LogicM ([Id], Either Expr Expr)
forall {a}.
[Id]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Id], Either a Expr)
go [] (CoreExpr -> LogicM ([Id], Either Expr Expr))
-> (CoreExpr -> CoreExpr)
-> CoreExpr
-> LogicM ([Id], Either Expr Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
normalize Bool
allowTC
  where
    isE :: Id -> Bool
isE = if Bool
allowTC then Id -> Bool
GM.isEmbeddedDictVar else Id -> Bool
isErasable
    go :: [Id]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Id], Either a Expr)
go [Id]
acc (C.Lam Id
x CoreExpr
e)  | Id -> Bool
isTyVar    Id
x = [Id]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Id], Either a Expr)
go [Id]
acc CoreExpr
e
    go [Id]
acc (C.Lam Id
x CoreExpr
e)  | Id -> Bool
isE Id
x = [Id]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Id], Either a Expr)
go [Id]
acc CoreExpr
e
    go [Id]
acc (C.Lam Id
x CoreExpr
e)  = [Id]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Id], Either a Expr)
go (Id
xId -> [Id] -> [Id]
forall a. a -> [a] -> [a]
:[Id]
acc) CoreExpr
e
    go [Id]
acc (C.Tick CoreTickish
_ CoreExpr
e) = [Id]
-> CoreExpr
-> ExceptT Error (StateT 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 (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) ([Id], Either a Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e


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

coreToLogic :: Bool -> C.CoreExpr -> LogicM Expr
coreToLogic :: Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLogic Bool
allowTC CoreExpr
cb = Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC (Bool -> CoreExpr -> CoreExpr
forall a. Simplify a => Bool -> a -> a
normalize Bool
allowTC CoreExpr
cb)


coreToLg :: Bool -> C.CoreExpr -> LogicM Expr
coreToLg :: Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC  (C.Let (C.NonRec Id
x (C.Coercion Coercion
c)) CoreExpr
e)
  = Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC ((() :: Constraint) => Subst -> CoreExpr -> CoreExpr
Subst -> CoreExpr -> CoreExpr
C.substExpr (Subst -> Id -> Coercion -> Subst
C.extendCvSubst Subst
C.emptySubst Id
x Coercion
c) CoreExpr
e)
coreToLg Bool
allowTC  (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 (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) ((Symbol, Expr) -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e ExceptT Error (StateT LState Identity) ((Symbol, Expr) -> Expr)
-> ExceptT Error (StateT LState Identity) (Symbol, Expr)
-> ExceptT Error (StateT LState Identity) Expr
forall a b.
ExceptT Error (StateT LState Identity) (a -> b)
-> ExceptT Error (StateT LState Identity) a
-> ExceptT Error (StateT LState Identity) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>  Bool
-> Bind Id -> ExceptT Error (StateT LState Identity) (Symbol, Expr)
makesub Bool
allowTC Bind Id
b
coreToLg Bool
allowTC (C.Tick CoreTickish
_ CoreExpr
e)          = Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e
coreToLg Bool
allowTC (C.App (C.Var Id
v) CoreExpr
e)
  | Id -> Bool
ignoreVar Id
v                = Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e
coreToLg Bool
_allowTC (C.Var Id
x)
  | Id
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
falseDataConId        = Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PFalse
  | Id
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
trueDataConId         = Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PTrue
  | Bool
otherwise                  = LogicM LState
getState LogicM LState
-> (LState -> ExceptT Error (StateT LState Identity) Expr)
-> ExceptT Error (StateT LState Identity) Expr
forall a b.
ExceptT Error (StateT LState Identity) a
-> (a -> ExceptT Error (StateT LState Identity) b)
-> ExceptT Error (StateT LState Identity) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Id -> LogicMap -> ExceptT Error (StateT LState Identity) Expr
eVarWithMap Id
x (LogicMap -> ExceptT Error (StateT LState Identity) Expr)
-> (LState -> LogicMap)
-> LState
-> ExceptT Error (StateT LState Identity) Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LState -> LogicMap
lsSymMap
coreToLg Bool
allowTC e :: CoreExpr
e@(C.App CoreExpr
_ CoreExpr
_)         = Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
toPredApp Bool
allowTC CoreExpr
e
coreToLg Bool
allowTC (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 (StateT LState Identity) Expr)
-> ExceptT Error (StateT LState Identity) Expr
forall a b.
ExceptT Error (StateT LState Identity) a
-> (a -> ExceptT Error (StateT LState Identity) b)
-> ExceptT Error (StateT LState Identity) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool
-> CoreExpr
-> (CoreExpr, CoreExpr)
-> ExceptT Error (StateT LState Identity) Expr
coreToIte Bool
allowTC 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 Bool
allowTC (C.Case CoreExpr
e Id
b Type
_ [CoreAlt]
alts)   = do Expr
p <- Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e
                                            Bool
-> Id
-> Expr
-> [CoreAlt]
-> ExceptT Error (StateT LState Identity) Expr
casesToLg Bool
allowTC Id
b Expr
p [CoreAlt]
alts
coreToLg Bool
_ (C.Lit Literal
l)             = case Literal -> Maybe Expr
mkLit Literal
l of
                                          Maybe Expr
Nothing -> String -> ExceptT Error (StateT LState Identity) Expr
forall a. String -> LogicM a
throw (String -> ExceptT Error (StateT LState Identity) Expr)
-> String -> ExceptT Error (StateT 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 (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
i
coreToLg Bool
allowTC (C.Cast CoreExpr
e Coercion
c)          = do (Sort
s, Sort
t) <- Coercion -> LogicM (Sort, Sort)
coerceToLg Coercion
c
                                            Expr
e'     <- Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e
                                            Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t Expr
e')
-- elaboration reuses coretologic
-- TODO: fix this
coreToLg Bool
True (C.Lam Id
x CoreExpr
e) = do Expr
p     <- Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
True CoreExpr
e
                               TCEmb TyCon
tce   <- LState -> TCEmb TyCon
lsEmb (LState -> TCEmb TyCon)
-> LogicM LState
-> ExceptT Error (StateT LState Identity) (TCEmb TyCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LogicM LState
getState
                               Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ExceptT Error (StateT LState Identity) Expr)
-> Expr -> ExceptT Error (StateT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> Expr -> Expr
ELam (Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
x, TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce (Id -> Type
GM.expandVarType Id
x)) Expr
p
coreToLg Bool
_ e :: CoreExpr
e@(C.Lam Id
_ CoreExpr
_)        = String -> ExceptT Error (StateT LState Identity) Expr
forall a. String -> LogicM a
throw (String
"Cannot transform lambda abstraction to Logic:\t" 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
"\n\n Try using a helper function to remove the lambda.")
coreToLg Bool
_ CoreExpr
e                     = String -> ExceptT Error (StateT 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
  TCEmb TyCon
tce   <- (LState -> TCEmb TyCon)
-> ExceptT Error (StateT LState Identity) (TCEmb TyCon)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets LState -> TCEmb TyCon
lsEmb
  let tx :: Type -> Sort
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
  (Sort, Sort) -> LogicM (Sort, Sort)
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Sort, Sort) -> LogicM (Sort, Sort))
-> (Sort, Sort) -> LogicM (Sort, Sort)
forall a b. (a -> b) -> a -> b
$ String -> (Sort, Sort) -> (Sort, Sort)
forall a. PPrint a => String -> a -> a
F.notracepp String
"TYPE-EQ-TO-LOGIC" (Type -> Sort
tx Type
s, Type -> Sort
tx Type
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 (StateT 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 (StateT 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 :: Bool -> Var -> Expr -> [C.CoreAlt] -> LogicM Expr
casesToLg :: Bool
-> Id
-> Expr
-> [CoreAlt]
-> ExceptT Error (StateT LState Identity) Expr
casesToLg Bool
allowTC Id
v Expr
e [CoreAlt]
alts = (CoreAlt -> ExceptT Error (StateT LState Identity) (AltCon, Expr))
-> [CoreAlt]
-> ExceptT Error (StateT 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 (Bool
-> Expr
-> CoreAlt
-> ExceptT Error (StateT LState Identity) (AltCon, Expr)
altToLg Bool
allowTC Expr
e) [CoreAlt]
normAlts ExceptT Error (StateT LState Identity) [(AltCon, Expr)]
-> ([(AltCon, Expr)]
    -> ExceptT Error (StateT LState Identity) Expr)
-> ExceptT Error (StateT LState Identity) Expr
forall a b.
ExceptT Error (StateT LState Identity) a
-> (a -> ExceptT Error (StateT LState Identity) b)
-> ExceptT Error (StateT LState Identity) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(AltCon, Expr)] -> ExceptT Error (StateT LState Identity) Expr
go
  where
    normAlts :: [CoreAlt]
normAlts       = [CoreAlt] -> [CoreAlt]
normalizeAlts [CoreAlt]
alts
    go :: [(C.AltCon, Expr)] -> LogicM Expr
    go :: [(AltCon, Expr)] -> ExceptT Error (StateT LState Identity) Expr
go [(AltCon
_,Expr
p)]     = Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT 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 Expr
c <- AltCon -> Expr -> ExceptT Error (StateT LState Identity) Expr
checkDataAlt AltCon
d Expr
e
                        Expr
e' <- [(AltCon, Expr)] -> ExceptT Error (StateT LState Identity) Expr
go [(AltCon, Expr)]
dps
                        Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIte Expr
c Expr
p Expr
e' Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
`subst1` (Symbol, Expr)
su)
    go []          = Maybe SrcSpan
-> String -> ExceptT Error (StateT LState Identity) Expr
forall a. 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 (StateT LState Identity) Expr)
-> String -> ExceptT Error (StateT 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 (StateT LState Identity) Expr
checkDataAlt (C.DataAlt DataCon
d) Expr
e = Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ExceptT Error (StateT LState Identity) Expr)
-> Expr -> ExceptT Error (StateT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar (DataCon -> Symbol
makeDataConChecker DataCon
d)) Expr
e
checkDataAlt AltCon
C.DEFAULT     Expr
_ = Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PTrue
checkDataAlt (C.LitAlt Literal
l)  Expr
e
  | Just Expr
le <- Literal -> Maybe Expr
mkLit Literal
l       = Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EEq Expr
le Expr
e)
  | Bool
otherwise                = String -> ExceptT Error (StateT LState Identity) Expr
forall a. String -> LogicM a
throw (String -> ExceptT Error (StateT LState Identity) Expr)
-> String -> ExceptT Error (StateT 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 :: Bool -> Expr -> C.CoreAlt -> LogicM (C.AltCon, Expr)
altToLg :: Bool
-> Expr
-> CoreAlt
-> ExceptT Error (StateT LState Identity) (AltCon, Expr)
altToLg Bool
allowTC Expr
de (Alt a :: AltCon
a@(C.DataAlt DataCon
d) [Id]
xs CoreExpr
e) = do
  Expr
p  <- Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e
  DataConMap
dm <- (LState -> DataConMap)
-> ExceptT Error (StateT LState Identity) DataConMap
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets LState -> DataConMap
lsDCMap
  let su :: Subst
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..]]
  (AltCon, Expr)
-> ExceptT Error (StateT LState Identity) (AltCon, Expr)
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (AltCon
a, Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p)

altToLg Bool
allowTC Expr
_ (Alt AltCon
a [Id]
_ CoreExpr
e)
  = (AltCon
a, ) (Expr -> (AltCon, Expr))
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) (AltCon, Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC 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
EApp (Symbol -> Expr
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 :: Bool -> C.CoreExpr -> (C.CoreExpr, C.CoreExpr) -> LogicM Expr
coreToIte :: Bool
-> CoreExpr
-> (CoreExpr, CoreExpr)
-> ExceptT Error (StateT LState Identity) Expr
coreToIte Bool
allowTC CoreExpr
e (CoreExpr
efalse, CoreExpr
etrue)
  = do Expr
p  <- Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e
       Expr
e1 <- Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
efalse
       Expr
e2 <- Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
etrue
       Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ExceptT Error (StateT LState Identity) Expr)
-> Expr -> ExceptT Error (StateT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr -> Expr
EIte Expr
p Expr
e2 Expr
e1

toPredApp :: Bool -> C.CoreExpr -> LogicM Expr
toPredApp :: Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
toPredApp Bool
allowTC CoreExpr
p = (Maybe Symbol, [CoreExpr])
-> ExceptT Error (StateT LState Identity) Expr
go ((Maybe Symbol, [CoreExpr])
 -> ExceptT Error (StateT LState Identity) Expr)
-> (CoreExpr -> (Maybe Symbol, [CoreExpr]))
-> CoreExpr
-> ExceptT Error (StateT LState Identity) Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoreExpr -> Maybe Symbol)
-> (CoreExpr, [CoreExpr]) -> (Maybe Symbol, [CoreExpr])
forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst CoreExpr -> Maybe Symbol
opSym ((CoreExpr, [CoreExpr]) -> (Maybe Symbol, [CoreExpr]))
-> (CoreExpr -> (CoreExpr, [CoreExpr]))
-> CoreExpr
-> (Maybe Symbol, [CoreExpr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> CoreExpr -> (CoreExpr, [CoreExpr])
forall t. Bool -> Expr t -> (Expr t, [Expr t])
splitArgs Bool
allowTC (CoreExpr -> ExceptT Error (StateT LState Identity) Expr)
-> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ CoreExpr
p
  where
    opSym :: CoreExpr -> Maybe Symbol
opSym = (Symbol -> Symbol) -> Maybe Symbol -> Maybe Symbol
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Symbol -> Symbol
GM.dropModuleNamesAndUnique (Maybe Symbol -> Maybe Symbol)
-> (CoreExpr -> Maybe Symbol) -> CoreExpr -> Maybe Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> Maybe Symbol
tomaybesymbol
    go :: (Maybe Symbol, [CoreExpr])
-> ExceptT Error (StateT 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
PAtom Brel
rel (Expr -> Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e1 ExceptT Error (StateT LState Identity) (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall a b.
ExceptT Error (StateT LState Identity) (a -> b)
-> ExceptT Error (StateT LState Identity) a
-> ExceptT Error (StateT LState Identity) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC 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
"not" :: String)
      = Expr -> Expr
PNot (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"len" :: String)
      = Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar Symbol
"len") (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC 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
"||" :: String)
      = [Expr] -> Expr
POr ([Expr] -> Expr)
-> ExceptT Error (StateT LState Identity) [Expr]
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoreExpr -> ExceptT Error (StateT LState Identity) Expr)
-> [CoreExpr] -> ExceptT Error (StateT 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 (Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC) [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
"&&" :: String)
      = [Expr] -> Expr
PAnd ([Expr] -> Expr)
-> ExceptT Error (StateT LState Identity) [Expr]
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoreExpr -> ExceptT Error (StateT LState Identity) Expr)
-> [CoreExpr] -> ExceptT Error (StateT 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 (Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC) [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
"==>" :: String)
      = Expr -> Expr -> Expr
PImp (Expr -> Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e1 ExceptT Error (StateT LState Identity) (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall a b.
ExceptT Error (StateT LState Identity) (a -> b)
-> ExceptT Error (StateT LState Identity) a
-> ExceptT Error (StateT LState Identity) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e2
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"<=>" :: String)
      = Expr -> Expr -> Expr
PIff (Expr -> Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e1 ExceptT Error (StateT LState Identity) (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall a b.
ExceptT Error (StateT LState Identity) (a -> b)
-> ExceptT Error (StateT LState Identity) a
-> ExceptT Error (StateT LState Identity) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e2
    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
"or" :: String)
      = [Expr] -> Expr
POr  ([Expr] -> Expr) -> (Expr -> [Expr]) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
deList (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
es
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"and" :: String)
      = [Expr] -> Expr
PAnd ([Expr] -> Expr) -> (Expr -> [Expr]) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
deList (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
es
    go (Maybe Symbol
_, [CoreExpr]
_)
      = Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
toLogicApp Bool
allowTC 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 :: Bool -> C.CoreExpr -> LogicM Expr
toLogicApp :: Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
toLogicApp Bool
allowTC CoreExpr
e = do
  let (CoreExpr
f, [CoreExpr]
es) = Bool -> CoreExpr -> (CoreExpr, [CoreExpr])
forall t. Bool -> Expr t -> (Expr t, [Expr t])
splitArgs Bool
allowTC CoreExpr
e
  case CoreExpr
f of
    C.Var Id
_ -> do [Expr]
args <- (CoreExpr -> ExceptT Error (StateT LState Identity) Expr)
-> [CoreExpr] -> ExceptT Error (StateT 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 (Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC) [CoreExpr]
es
                  LogicMap
lmap <- LState -> LogicMap
lsSymMap (LState -> LogicMap)
-> LogicM LState -> ExceptT Error (StateT LState Identity) LogicMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LogicM LState
getState
                  Expr
def  <- (LocSymbol -> [Expr] -> Expr
`mkEApp` [Expr]
args) (LocSymbol -> Expr)
-> ExceptT Error (StateT LState Identity) LocSymbol
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (StateT LState Identity) LocSymbol
tosymbol CoreExpr
f
                  (\LocSymbol
x -> Expr -> LogicMap -> LocSymbol -> [Expr] -> Expr
makeApp Expr
def LogicMap
lmap LocSymbol
x [Expr]
args) (LocSymbol -> Expr)
-> ExceptT Error (StateT LState Identity) LocSymbol
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (StateT LState Identity) LocSymbol
tosymbol' CoreExpr
f
    CoreExpr
_       -> do Expr
fe   <- Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
f
                  [Expr]
args <- (CoreExpr -> ExceptT Error (StateT LState Identity) Expr)
-> [CoreExpr] -> ExceptT Error (StateT 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 (Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC) [CoreExpr]
es
                  Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ExceptT Error (StateT LState Identity) Expr)
-> Expr -> ExceptT Error (StateT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp Expr
fe [Expr]
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.Num.negate" :: String)
  = Expr -> Expr
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.Num.fromInteger" :: String)
  , ECon Constant
c <- Expr
e
  = Constant -> Expr
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
EApp (Symbol -> Expr
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
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.Num." :: String)) Symbol
sym) HashMap Symbol Bop
bops
  = Bop -> Expr -> Expr -> Expr
EBin Bop
op Expr
e1 Expr
e2

makeApp Expr
def LogicMap
lmap LocSymbol
f [Expr]
es
  = LogicMap -> LocSymbol -> [Expr] -> Expr -> Expr
eAppWithMap LogicMap
lmap LocSymbol
f [Expr]
es Expr
def
  -- where msg = "makeApp f = " ++ show f ++ " es = " ++ show es ++ " def = " ++ show def

eVarWithMap :: Id -> LogicMap -> LogicM Expr
eVarWithMap :: Id -> LogicMap -> ExceptT Error (StateT LState Identity) Expr
eVarWithMap Id
x LogicMap
lmap = do
  LocSymbol
f'     <- CoreExpr -> ExceptT Error (StateT LState Identity) LocSymbol
tosymbol' (Id -> CoreExpr
forall b. Id -> Expr b
C.Var Id
x :: C.CoreExpr)
  -- let msg = "eVarWithMap x = " ++ show x ++ " f' = " ++ show f'
  Expr -> ExceptT Error (StateT LState Identity) Expr
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ExceptT Error (StateT LState Identity) Expr)
-> Expr -> ExceptT Error (StateT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ LogicMap -> LocSymbol -> [Expr] -> Expr -> Expr
eAppWithMap LogicMap
lmap LocSymbol
f' [] (Id -> Expr
varExpr Id
x)

varExpr :: Var -> Expr
varExpr :: Id -> Expr
varExpr Id
x
  | Type -> Bool
isPolyCst Type
t = LocSymbol -> [Expr] -> Expr
mkEApp (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
s) []
  | Bool
otherwise   = Symbol -> Expr
EVar Symbol
s
  where
    t :: Type
t           = Id -> Type
GM.expandVarType Id
x
    s :: Symbol
s           = Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
x

isPolyCst :: Type -> Bool
isPolyCst :: Type -> Bool
isPolyCst (ForAllTy ForAllTyBinder
_ Type
t) = Type -> Bool
isCst Type
t
isPolyCst Type
_              = Bool
False

isCst :: Type -> Bool
isCst :: Type -> Bool
isCst (ForAllTy ForAllTyBinder
_ Type
t) = Type -> Bool
isCst Type
t
isCst FunTy{}        = Bool
False
isCst Type
_              = Bool
True


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
"==" :: String), Brel
Eq)
                   , (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"/=" :: String), Brel
Ne)
                   , (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
">=" :: String), Brel
Ge)
                   , (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
">" :: String) , Brel
Gt)
                   , (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"<=" :: String), Brel
Le)
                   , (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"<" :: String) , Brel
Lt)
                   ]

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
numSymbol String
"-", Bop
Minus)
                  , (String -> Symbol
numSymbol String
"*", Bop
Times)
                  , (String -> Symbol
numSymbol String
"/", Bop
Div)
                  , (String -> Symbol
realSymbol String
"/", Bop
Div)
                  , (String -> Symbol
numSymbol String
"%", Bop
Mod)
                  ]
  where
    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.Num."
    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.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 (StateT LState Identity) LocSymbol
tosymbol CoreExpr
e
 = case CoreExpr -> Maybe Symbol
tomaybesymbol CoreExpr
e of
    Just Symbol
x -> LocSymbol -> ExceptT Error (StateT LState Identity) LocSymbol
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol -> ExceptT Error (StateT LState Identity) LocSymbol)
-> LocSymbol -> ExceptT Error (StateT 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 (StateT 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 (StateT LState Identity) LocSymbol
tosymbol' (C.Var Id
x) = LocSymbol -> ExceptT Error (StateT LState Identity) LocSymbol
forall a. a -> ExceptT Error (StateT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol -> ExceptT Error (StateT LState Identity) LocSymbol)
-> LocSymbol -> ExceptT Error (StateT 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 (StateT 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 :: Bool -> C.CoreBind -> LogicM (Symbol, Expr)
makesub :: Bool
-> Bind Id -> ExceptT Error (StateT LState Identity) (Symbol, Expr)
makesub Bool
allowTC (C.NonRec Id
x CoreExpr
e) =  (Id -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Id
x,) (Expr -> (Symbol, Expr))
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) (Symbol, Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg Bool
allowTC CoreExpr
e
makesub Bool
_       Bind Id
_              = String -> ExceptT Error (StateT 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
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
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
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
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
. (() :: Constraint) => 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 b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd (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 b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd ((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)