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

{- | [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 = forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft
rep {ty_res :: SpecType
ty_res = SpecType
res forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` RReft
r , ty_binds :: [Symbol]
ty_binds = [Symbol]
xs}
  where
    r :: RReft
r              = forall r. r -> Predicate -> UReft r
MkUReft (Expr -> Reft
mkReft (LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
f (forall {b}. (Symbol, b) -> Expr
mkA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
vxs))) forall a. Monoid a => a
mempty
    rep :: RTypeRep RTyCon RTyVar RReft
rep            = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t
    res :: SpecType
res            = forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
rep
    xs :: [Symbol]
xs             = forall a. Show a => Symbol -> a -> Symbol
intSymbol (forall a. Symbolic a => a -> Symbol
symbol (String
"x" :: String)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
rep]
    vxs :: [(Symbol, SpecType)]
vxs            = forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall {t} {t1}. RType RTyCon t t1 -> Bool
isErasable' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs (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 forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass else forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType
    f :: LocSymbol
f              = forall a. a -> Located a
dummyLoc (forall a. Symbolic a => a -> Symbol
symbol Id
v)
    t :: SpecType
t              = forall r. Monoid r => Type -> RRType r
ofType (Id -> Type
GM.expandVarType Id
v) :: SpecType
    mkA :: (Symbol, b) -> Expr
mkA            = Symbol -> Expr
EVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst
    mkReft :: Expr -> Reft
mkReft         = if forall {t} {t1}. RType RTyCon t t1 -> Bool
isBool SpecType
res then forall a. Predicate a => a -> Reft
propReft else 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 = 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   = forall a. Predicate a => a -> Reft
propReft
           | Bool
otherwise = forall a. Expression a => a -> Reft
exprReft
    mkT :: [Symbol] -> RReft
mkT [Symbol]
xs          = forall r. r -> Predicate -> UReft r
MkUReft (Expr -> Reft
mkReft forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
locSym (Symbol -> Expr
EVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> [a]
reverse [Symbol]
xs)) forall a. Monoid a => a
mempty
    locSym :: LocSymbol
locSym          = forall a. a -> Located a
dummyLoc (forall a. Symbolic a => a -> Symbol
symbol Id
v)
    st :: SpecType
st              = forall r. Monoid r => Type -> RRType r
ofType (Id -> Type
GM.expandVarType Id
v) :: SpecType
    boolRes :: Bool
boolRes         =  forall {t} {t1}. RType RTyCon t t1 -> Bool
isBool forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep 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)    = 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)      = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
p forall a b. (a -> b) -> a -> b
$ ([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 forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass else forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType) RType c tv r
t1           = 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)
     | forall {c} {tv} {r}. RType c tv r -> Bool
hasRApps RType c tv r
t               = 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'forall a. a -> [a] -> [a]
:[Symbol]
args) (forall a. [a] -> [a]
tail [a]
i) RType c tv r
t2) r
r
                                       where x' :: Symbol
x' = forall a. Show a => Symbol -> a -> Symbol
intSymbol (forall a. Symbolic a => a -> Symbol
symbol (String
"x" :: String)) (forall a. [a] -> a
head [a]
i)
    go [Symbol] -> r
f [Symbol]
args [a]
_ RType c tv r
t                = RType c tv r
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` [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 = forall a. PPrint a => String -> a -> a
F.notracepp String
msg SpecType
t'
  where
    msg :: String
msg          = String
"weakenResult v =" forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> String
GM.showPpr Id
v forall a. [a] -> [a] -> [a]
++ String
" t = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp SpecType
t
    t' :: SpecType
t'           = forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft
rep { ty_res :: SpecType
ty_res = forall c tv.
(Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
mapExprReft Symbol -> Expr -> Expr
weaken (forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
rep) }
    rep :: RTypeRep RTyCon RTyVar RReft
rep          = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. a -> Maybe a
Just Expr
vE forall a. Eq a => a -> a -> Bool
/=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Expr -> Maybe Expr
isSingletonExpr Symbol
x) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
dropWhile ((if Bool
allowTC then forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass else forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Symbol, SpecType)]
xts
    xts :: [(Symbol, SpecType)]
xts          = forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
rep) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
rep)
    vF :: LocSymbol
vF           = forall a. a -> Located a
dummyLoc (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  <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets LState -> String -> Error
lsError
  forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String -> Error
fmkError String
str

getState :: LogicM LState
getState :: LogicM LState
getState = 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 = 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
  = forall s a. State s a -> s -> a
evalState (forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT LogicM t
m) 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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoreAlt]
litAlts) = forall a. LocSymbol -> String -> a
measureFail LocSymbol
locSym String
"Cannot lift definition with literal alternatives"
  | Bool
otherwise          = do
      [Def (Located (RRType r)) DataCon]
d1s <- forall a. PPrint a => String -> a -> a
F.notracepp String
"coreAltDefs-1" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 <- forall a. PPrint a => String -> a -> a
F.notracepp String
"coreAltDefs-2" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>       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
      forall (m :: * -> *) a. Monad m => a -> m a
return ([Def (Located (RRType r)) DataCon]
d1s forall a. [a] -> [a] -> [a]
++ [Def (Located (RRType r)) DataCon]
d2s)
  where
    myArgs :: [Id]
myArgs   = 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreAlt]
alts)
    defExpr :: Maybe CoreExpr
defExpr  = 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)
      = forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
x {- (toArgs id args) -} DataCon
d (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall r. Reftable r => Id -> Located (RRType r)
varRType Id
dx) (forall r b.
Reftable r =>
(Located (RRType r) -> b) -> [Id] -> [(Symbol, b)]
toArgs forall a. a -> Maybe a
Just [Id]
xs')
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Body
ctor
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Subable a => a -> (Symbol, Expr) -> a
`subst1` (forall a. Symbolic a => a -> Symbol
F.symbol Id
dx, LocSymbol -> [Expr] -> Expr
F.mkEApp (forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol DataCon
d) (forall a. Symbolic a => a -> Expr
F.eVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Id]
xs')))
     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e
      where xs' :: [Id]
xs' = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not 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
      = forall a. String -> LogicM a
throw forall a b. (a -> b) -> a -> b
$ String
"Bad alternative" forall a. [a] -> [a] -> [a]
++ 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e
      -- let ys  = toArgs id args
      let dxt :: Maybe (Located (RRType r))
dxt = forall a. a -> Maybe a
Just (forall r. Reftable r => Id -> Located (RRType r)
varRType Id
dx)
      forall (m :: * -> *) a. Monad m => a -> m a
return  [ 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 (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
_ =
      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 = [(forall a. Symbolic a => a -> Symbol
symbol Id
x, Located (RRType r) -> b
f forall a b. (a -> b) -> a -> b
$ 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     = 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 (forall a. Located a -> a
val LocSymbol
x)
    defRTyp :: Type -> Maybe (Located (RRType r))
defRTyp   = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
_                   = forall {r}.
Reftable r =>
[Id] -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
go [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> CoreExpr
inlinePreds forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
xforall 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) = 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  = 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 [forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
C.DEFAULT [] CoreExpr
e]
    go [Id]
_ CoreExpr
_                        = forall a. LocSymbol -> String -> a
measureFail LocSymbol
locSym String
"Does not have a case-of at the top-level"

    inlinePreds :: CoreExpr -> CoreExpr
inlinePreds   = forall a. Simplify a => (Id -> Bool) -> a -> a
inline (Type -> Type -> Bool
eqType Type
boolTy 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 = forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
sp String
e
  where
    sp :: Maybe SrcSpan
sp            = forall a. a -> Maybe a
Just (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSymbol
x)
    e :: String
e             = forall r. PrintfType r => String -> r
Printf.printf String
"Cannot create measure '%s': %s" (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 = forall a. PPrint a => String -> a -> a
F.notracepp String
"isMeasureArg" forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Type
t
  | Bool
otherwise           = 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 = forall a. (Type -> a) -> Id -> Located a
GM.varLocInfo 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 = forall {a}.
[Id]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Id], Either a Expr)
go [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
xforall 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            = (forall a. [a] -> [a]
reverse [Id]
acc,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e


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

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


coreToLg :: Bool -> C.CoreExpr -> LogicM Expr
coreToLg :: Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC  (C.Let (C.NonRec Id
x (C.Coercion Coercion
c)) CoreExpr
e)
  = Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC (HasDebugCallStack => 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 CoreBind
b CoreExpr
e)
  = forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>  Bool -> CoreBind -> LogicM (Symbol, Expr)
makesub Bool
allowTC CoreBind
b
coreToLg Bool
allowTC (C.Tick CoreTickish
_ CoreExpr
e)          = Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e
coreToLg Bool
allowTC (C.App (C.Var Id
v) CoreExpr
e)
  | Id -> Bool
ignoreVar Id
v                = Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e
coreToLg Bool
_allowTC (C.Var Id
x)
  | Id
x forall a. Eq a => a -> a -> Bool
== Id
falseDataConId        = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PFalse
  | Id
x forall a. Eq a => a -> a -> Bool
== Id
trueDataConId         = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PTrue
  | Bool
otherwise                  = LogicM LState
getState forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Id -> LogicMap -> LogicM Expr
eVarWithMap Id
x 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 -> LogicM 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> CoreExpr -> (CoreExpr, CoreExpr) -> LogicM 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 -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e
                                            Bool -> Id -> Expr -> [CoreAlt] -> LogicM 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 -> forall a. String -> LogicM a
throw forall a b. (a -> b) -> a -> b
$ String
"Bad Literal in measure definition" forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> String
GM.showPpr Literal
l
                                          Just Expr
i  -> 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 -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e
                                            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 -> LogicM Expr
coreToLg Bool
True CoreExpr
e
                               TCEmb TyCon
tce   <- LState -> TCEmb TyCon
lsEmb forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LogicM LState
getState
                               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> Expr -> Expr
ELam (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
_)        = forall a. String -> LogicM a
throw (String
"Cannot transform lambda abstraction to Logic:\t" forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> String
GM.showPpr CoreExpr
e forall a. [a] -> [a] -> [a]
++
                                            String
"\n\n Try using a helper function to remove the lambda.")
coreToLg Bool
_ CoreExpr
e                     = forall a. String -> LogicM a
throw (String
"Cannot transform to Logic:\t" forall a. [a] -> [a] -> [a]
++ 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 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   <- 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
expandTypeSynonyms
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall a. Eq a => a -> a -> Bool
== DataCon
falseDataCon, DataCon
true forall a. Eq a => a -> a -> Bool
== DataCon
trueDataCon
  = 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 forall a. Eq a => a -> a -> Bool
== DataCon
falseDataCon, DataCon
true forall a. Eq a => a -> a -> Bool
== DataCon
trueDataCon
  = forall (m :: * -> *) a. Monad m => a -> m a
return (CoreExpr
efalse, CoreExpr
etrue)
checkBoolAlts [CoreAlt]
alts
  = forall a. String -> LogicM a
throw (String
"checkBoolAlts failed on " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> String
GM.showPpr [CoreAlt]
alts)

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

checkDataAlt :: C.AltCon -> Expr -> LogicM Expr
checkDataAlt :: AltCon -> Expr -> LogicM Expr
checkDataAlt (C.DataAlt DataCon
d) Expr
e = forall (m :: * -> *) a. Monad m => a -> m a
return 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
_ = 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       = forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EEq Expr
le Expr
e)
  | Bool
otherwise                = forall a. String -> LogicM a
throw forall a b. (a -> b) -> a -> b
$ String
"Oops, not yet handled: checkDataAlt on Lit: " forall a. [a] -> [a] -> [a]
++ 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 forall a. [a] -> [a] -> [a]
++ [CoreAlt]
defAlts
  where
    ([CoreAlt]
defAlts, [CoreAlt]
ctorAlts) = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition forall {b}. Alt b -> Bool
isDefault [CoreAlt]
alts
    isDefault :: Alt b -> Bool
isDefault (Alt AltCon
c [b]
_ Expr b
_)   = AltCon
c forall a. Eq a => a -> a -> Bool
== AltCon
C.DEFAULT

altToLg :: Bool -> Expr -> C.CoreAlt -> LogicM (C.AltCon, Expr)
altToLg :: Bool -> Expr -> CoreAlt -> LogicM (AltCon, Expr)
altToLg Bool
allowTC Expr
de (Alt a :: AltCon
a@(C.DataAlt DataCon
d) [Id]
xs CoreExpr
e) = do
  Expr
p  <- Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e
  DataConMap
dm <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets LState -> DataConMap
lsDCMap
  let su :: Subst
su = [(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ 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) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not 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..]]
  forall (m :: * -> *) a. Monad m => a -> m a
return (AltCon
a, forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p)

altToLg Bool
allowTC Expr
_ (Alt AltCon
a [Id]
_ CoreExpr
e)
  = (AltCon
a, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM 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 = [(forall a. Symbolic a => a -> Symbol
symbol Id
x, Expr
t), (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 forall a b. (a -> b) -> a -> b
$ Maybe DataConMap -> DataCon -> Int -> Symbol
makeDataConSelector (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 forall a. Eq a => a -> a -> Bool
== DataCon
intDataCon

coreToIte :: Bool -> C.CoreExpr -> (C.CoreExpr, C.CoreExpr) -> LogicM Expr
coreToIte :: Bool -> CoreExpr -> (CoreExpr, CoreExpr) -> LogicM Expr
coreToIte Bool
allowTC CoreExpr
e (CoreExpr
efalse, CoreExpr
etrue)
  = do Expr
p  <- Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e
       Expr
e1 <- Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
efalse
       Expr
e2 <- Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
etrue
       forall (m :: * -> *) a. Monad m => a -> m a
return 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 -> LogicM Expr
toPredApp Bool
allowTC CoreExpr
p = (Maybe Symbol, [CoreExpr]) -> LogicM Expr
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst CoreExpr -> Maybe Symbol
opSym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Bool -> Expr t -> (Expr t, [Expr t])
splitArgs Bool
allowTC forall a b. (a -> b) -> a -> b
$ CoreExpr
p
  where
    opSym :: CoreExpr -> Maybe Symbol
opSym = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Symbol -> Symbol
GM.dropModuleNamesAndUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> Maybe Symbol
tomaybesymbol
    go :: (Maybe Symbol, [CoreExpr]) -> LogicM Expr
go (Just Symbol
f, [CoreExpr
e1, CoreExpr
e2])
      | Just Brel
rel <- 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e2
    go (Just Symbol
f, [CoreExpr
e])
      | Symbol
f forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol (String
"not" :: String)
      = Expr -> Expr
PNot forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e
      | Symbol
f forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol (String
"len" :: String)
      = Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar Symbol
"len") forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e
    go (Just Symbol
f, [CoreExpr
e1, CoreExpr
e2])
      | Symbol
f forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol (String
"||" :: String)
      = [Expr] -> Expr
POr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC) [CoreExpr
e1, CoreExpr
e2]
      | Symbol
f forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol (String
"&&" :: String)
      = [Expr] -> Expr
PAnd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC) [CoreExpr
e1, CoreExpr
e2]
      | Symbol
f forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol (String
"==>" :: String)
      = Expr -> Expr -> Expr
PImp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e2
      | Symbol
f forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol (String
"<=>" :: String)
      = Expr -> Expr -> Expr
PIff forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e2
    go (Just Symbol
f, [CoreExpr
es])
      | Symbol
f forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol (String
"or" :: String)
      = [Expr] -> Expr
POr  forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
deList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
es
      | Symbol
f forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol (String
"and" :: String)
      = [Expr] -> Expr
PAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
deList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
es
    go (Maybe Symbol
_, [CoreExpr]
_)
      = Bool -> CoreExpr -> LogicM Expr
toLogicApp Bool
allowTC CoreExpr
p

    deList :: Expr -> [Expr]
    deList :: Expr -> [Expr]
deList (EApp (EApp (EVar Symbol
cons) Expr
e) Expr
es)
      | Symbol
cons forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Types.:" :: String)
      = Expr
eforall a. a -> [a] -> [a]
:Expr -> [Expr]
deList Expr
es
    deList (EVar Symbol
nil)
      | Symbol
nil forall a. Eq a => a -> a -> Bool
== 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 -> LogicM Expr
toLogicApp Bool
allowTC CoreExpr
e = do
  let (CoreExpr
f, [CoreExpr]
es) = forall t. Bool -> Expr t -> (Expr t, [Expr t])
splitArgs Bool
allowTC CoreExpr
e
  case CoreExpr
f of
    C.Var Id
_ -> do [Expr]
args <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC) [CoreExpr]
es
                  LogicMap
lmap <- LState -> LogicMap
lsSymMap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LogicM LState
getState
                  Expr
def  <- (LocSymbol -> [Expr] -> Expr
`mkEApp` [Expr]
args) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> LogicM LocSymbol
tosymbol CoreExpr
f
                  (\LocSymbol
x -> Expr -> LogicMap -> LocSymbol -> [Expr] -> Expr
makeApp Expr
def LogicMap
lmap LocSymbol
x [Expr]
args) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> LogicM LocSymbol
tosymbol' CoreExpr
f
    CoreExpr
_       -> do Expr
fe   <- Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
f
                  [Expr]
args <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC) [CoreExpr]
es
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> 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]
  | forall a. Located a -> a
val LocSymbol
f forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Num.negate" :: String)
  = Expr -> Expr
ENeg Expr
e
  | forall a. Located a -> a
val LocSymbol
f forall a. Eq a => a -> a -> Bool
== 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 (forall a. Located a -> a
val LocSymbol
f)
  , forall a. Symbolic a => a -> Symbol
symbol (String
"Ghci" :: String) Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
modName
  , Symbol
sym 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 <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (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 (forall a. Located a -> a
val LocSymbol
f)
  , forall a. Symbolic a => a -> Symbol
symbol (String
"Ghci" :: String) Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
modName
  , Just Bop
op <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (Symbol -> Symbol -> Symbol
mappendSym (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 -> LogicM Expr
eVarWithMap Id
x LogicMap
lmap = do
  LocSymbol
f'     <- CoreExpr -> LogicM LocSymbol
tosymbol' (forall b. Id -> Expr b
C.Var Id
x :: C.CoreExpr)
  -- let msg = "eVarWithMap x = " ++ show x ++ " f' = " ++ show f'
  forall (m :: * -> *) a. Monad m => a -> m a
return 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 (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           = forall a. Symbolic a => a -> Symbol
symbol Id
x

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

isCst :: Type -> Bool
isCst :: Type -> Bool
isCst (ForAllTy TyCoVarBinder
_ 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 = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (forall a. Symbolic a => a -> Symbol
symbol (String
"==" :: String), Brel
Eq)
                   , (forall a. Symbolic a => a -> Symbol
symbol (String
"/=" :: String), Brel
Ne)
                   , (forall a. Symbolic a => a -> Symbol
symbol (String
">=" :: String), Brel
Ge)
                   , (forall a. Symbolic a => a -> Symbol
symbol (String
">" :: String) , Brel
Gt)
                   , (forall a. Symbolic a => a -> Symbol
symbol (String
"<=" :: String), Brel
Le)
                   , (forall a. Symbolic a => a -> Symbol
symbol (String
"<" :: String) , Brel
Lt)
                   ]

bops :: M.HashMap Symbol Bop
bops :: HashMap Symbol Bop
bops = 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 =  forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a] -> [a]
(++) String
"GHC.Num."
    realSymbol :: String -> Symbol
    realSymbol :: String -> Symbol
realSymbol =  forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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', forall a. [a] -> [a]
reverse [Expr t]
args)
 where
    (Expr t
exprt', [Expr t]
args) = 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
eforall 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) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
symbol Id
x
tomaybesymbol CoreExpr
_         = forall a. Maybe a
Nothing

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

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

makesub :: Bool -> C.CoreBind -> LogicM (Symbol, Expr)
makesub :: Bool -> CoreBind -> LogicM (Symbol, Expr)
makesub Bool
allowTC (C.NonRec Id
x CoreExpr
e) =  (forall a. Symbolic a => a -> Symbol
symbol Id
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> CoreExpr -> LogicM Expr
coreToLg Bool
allowTC CoreExpr
e
makesub Bool
_       CoreBind
_              = 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
_                 = forall a. Maybe a
Nothing -- ELit sym sort

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

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

mkS :: ByteString -> Maybe Expr
mkS :: ByteString -> Maybe Expr
mkS                    = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymConst -> Expr
ESym forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> SymConst
SL  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                    = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Expr
ECon forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Sort -> Constant
`F.L` Sort
F.charSort)  forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Text
repr
  where
    repr :: Char -> Text
repr               = String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show 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 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
_]
  =  (forall a. Symbolic a => a -> Symbol
symbol DataCon
s  forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Integer.Type.S#"  Bool -> Bool -> Bool
|| forall a. Symbolic a => a -> Symbol
symbol DataCon
s  forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Num.Integer.IS")
  Bool -> Bool -> Bool
&& (forall a. Symbolic a => a -> Symbol
symbol DataCon
jp forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Integer.Type.Jp#" Bool -> Bool -> Bool
|| forall a. Symbolic a => a -> Symbol
symbol DataCon
jp forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Num.Integer.IP")
  Bool -> Bool -> Bool
&& (forall a. Symbolic a => a -> Symbol
symbol DataCon
jn forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Integer.Type.Jn#" Bool -> Bool -> Bool
|| forall a. Symbolic a => a -> Symbol
symbol DataCon
jn 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 = forall a. PPrint a => String -> a -> a
F.notracepp String
msg 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: " forall a. [a] -> [a] -> [a]
++ 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 (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 (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdInfo -> OccInfo
occInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasDebugCallStack => 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
inline_anf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC
   where
    inline_preds :: a -> a
inline_preds = forall a. Simplify a => (Id -> Bool) -> a -> a
inline (Type -> Type -> Bool
eqType Type
boolTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
GM.expandVarType)
    inline_anf :: a -> a
inline_anf   = 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
_))
    = 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
    = 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
    = forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
allowTC (C.App CoreExpr
e1 CoreExpr
e2)
    = forall b. Expr b -> Expr b -> Expr b
C.App (forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e1) (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
    = 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
    = forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
allowTC (C.Lam Id
x CoreExpr
e)
    = forall b. b -> Expr b -> Expr b
C.Lam Id
x (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
    = forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
allowTC (C.Let (C.Rec [(Id, CoreExpr)]
xes) CoreExpr
e)    | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((if Bool
allowTC then Id -> Bool
GM.isEmbeddedDictVar else Id -> Bool
isErasable) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Id, CoreExpr)]
xes
    = forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
allowTC (C.Let CoreBind
xes CoreExpr
e)
    = forall b. Bind b -> Expr b -> Expr b
C.Let (forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreBind
xes) (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") $ 
       forall a. Subable a => HashMap Id CoreExpr -> a -> a
sub (forall k v. Hashable k => k -> v -> HashMap k v
M.singleton Id
x (forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e)) (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)
    = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
C.Case (forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e) Id
x Type
t (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreAlt -> Bool
isPatErrorAlt) (forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreAlt]
alts))
  simplify Bool
allowTC (C.Cast CoreExpr
e Coercion
c)
    = forall b. Expr b -> Coercion -> Expr b
C.Cast (forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e) Coercion
c
  simplify Bool
allowTC (C.Tick CoreTickish
_ CoreExpr
e)
    = forall a. Simplify a => Bool -> a -> a
simplify Bool
allowTC CoreExpr
e
  simplify Bool
_ (C.Coercion Coercion
c)
    = forall b. Coercion -> Expr b
C.Coercion Coercion
c
  simplify Bool
_ (C.Type Type
t)
    = 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
                               = forall a. Subable a => HashMap Id CoreExpr -> a -> a
sub (forall k v. Hashable k => k -> v -> HashMap k v
M.singleton Id
x (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
ex)) (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e)
  inline Id -> Bool
p (C.Let CoreBind
xes CoreExpr
e)       = forall b. Bind b -> Expr b -> Expr b
C.Let (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreBind
xes) (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e)
  inline Id -> Bool
p (C.App CoreExpr
e1 CoreExpr
e2)       = forall b. Expr b -> Expr b -> Expr b
C.App (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e1) (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e2)
  inline Id -> Bool
p (C.Lam Id
x CoreExpr
e)         = forall b. b -> Expr b -> Expr b
C.Lam Id
x (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) = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
C.Case (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e) Id
x Type
t (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreAlt]
alts)
  inline Id -> Bool
p (C.Cast CoreExpr
e Coercion
c)        = forall b. Expr b -> Coercion -> Expr b
C.Cast (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)        = forall b. CoreTickish -> Expr b -> Expr b
C.Tick CoreTickish
t (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e)
  inline Id -> Bool
_ (C.Var Id
x)           = forall b. Id -> Expr b
C.Var Id
x
  inline Id -> Bool
_ (C.Lit Literal
l)           = forall b. Literal -> Expr b
C.Lit Literal
l
  inline Id -> Bool
_ (C.Coercion Coercion
c)      = forall b. Coercion -> Expr b
C.Coercion Coercion
c
  inline Id -> Bool
_ (C.Type Type
t)          = forall b. Type -> Expr b
C.Type Type
t


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

  inline :: (Id -> Bool) -> CoreBind -> CoreBind
inline Id -> Bool
p (C.NonRec Id
x CoreExpr
e) = forall b. b -> Expr b -> Bind b
C.NonRec Id
x (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e)
  inline Id -> Bool
p (C.Rec [(Id, CoreExpr)]
xes)    = forall b. [(b, Expr b)] -> Bind b
C.Rec (forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p) 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) = forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Id]
xs (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) = forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [Id]
xs (forall a. Simplify a => (Id -> Bool) -> a -> a
inline Id -> Bool
p CoreExpr
e)