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

{-# OPTIONS_GHC -Wno-orphans #-}

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

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


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

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

import Data.Ratio
import GHC.Base ((+#), (-#), (*#))

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

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

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

-- formerly: strengthenResult'
measureSpecType :: Bool -> Var -> SpecType
measureSpecType :: Bool -> CoreBndr -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
measureSpecType Bool
allowTC CoreBndr
v = ([Symbol] -> RReft)
-> [Symbol]
-> [Int]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall {c} {r} {a} {v} {tv}.
(TyConable c, Meet r, Show a) =>
([Symbol] -> r)
-> [Symbol]
-> [a]
-> RTypeBV Symbol v c tv r
-> RTypeBV Symbol v c tv r
go [Symbol] -> RReft
forall {b} {v}.
(Monoid (PredicateBV b v), Eq b) =>
[Symbol] -> UReftBV b v (ReftBV Symbol Symbol)
mkT [] [(Int
1::Int)..] RTypeBV Symbol Symbol RTyCon RTyVar RReft
st
  where
    mkReft :: Expr -> Reft
    mkReft :: ExprBV Symbol Symbol -> ReftBV Symbol Symbol
mkReft | Bool
boolRes   = ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Predicate a => a -> ReftBV Symbol Symbol
propReft
           | Bool
otherwise = ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Expression a => a -> ReftBV Symbol Symbol
exprReft
    mkT :: [Symbol] -> UReftBV b v (ReftBV Symbol Symbol)
mkT [Symbol]
xs          = ReftBV Symbol Symbol
-> PredicateBV b v -> UReftBV b v (ReftBV Symbol Symbol)
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft (ExprBV Symbol Symbol -> ReftBV Symbol Symbol
mkReft (ExprBV Symbol Symbol -> ReftBV Symbol Symbol)
-> ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ Located Symbol -> [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall v b. Located v -> [ExprBV b v] -> ExprBV b v
mkEApp Located Symbol
locSym (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
EVar (Symbol -> ExprBV Symbol Symbol)
-> [Symbol] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse [Symbol]
xs)) PredicateBV b v
forall a. Monoid a => a
mempty
    locSym :: Located Symbol
locSym          = Symbol -> Located Symbol
forall a. a -> Located a
dummyLoc (CoreBndr -> Symbol
forall a. Symbolic a => a -> Symbol
symbol CoreBndr
v)
    st :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
st              = Type -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r. IsReft r => Type -> RRType r
ofType (CoreBndr -> Type
GM.expandVarType CoreBndr
v) :: SpecType
    boolRes :: Bool
boolRes         =  RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool
forall t t1. RType RTyCon t t1 -> Bool
isBool (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool
forall a b. (a -> b) -> a -> b
$ RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep RTypeBV Symbol Symbol RTyCon RTyVar RReft
st

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

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


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

type LogicM = ExceptT Error (ReaderT LState Identity)

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

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

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

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

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

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

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

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

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

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

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

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

    inlinePreds :: Expr CoreBndr -> Expr CoreBndr
inlinePreds   = (CoreBndr -> Bool) -> Expr CoreBndr -> Expr CoreBndr
inlineCoreExpr (HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
eqType Type
boolTy (Type -> Bool) -> (CoreBndr -> Type) -> CoreBndr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreBndr -> Type
GM.expandVarType)

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


-- | 'isMeasureArg x' returns 'Just t' if 'x' is a valid argument for a measure.
isMeasureArg :: Var -> Maybe Type
isMeasureArg :: CoreBndr -> Maybe Type
isMeasureArg CoreBndr
x
  | Just TyCon
tc <- Maybe TyCon
tcMb
  , TyCon -> Bool
Ghc.isAlgTyCon TyCon
tc = [Char] -> Maybe Type -> Maybe Type
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"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                   = CoreBndr -> Type
GM.expandVarType CoreBndr
x
    tcMb :: Maybe TyCon
tcMb                = Type -> Maybe TyCon
tyConAppTyCon_maybe Type
t


varRType :: (IsReft r) => Var -> Located (RRType r)
varRType :: forall r. IsReft r => CoreBndr -> Located (RRType r)
varRType = (Type -> RRType r) -> CoreBndr -> Located (RRType r)
forall a. (Type -> a) -> CoreBndr -> Located a
GM.varLocInfo Type -> RRType r
forall r. IsReft r => Type -> RRType r
ofType

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


instance Show C.CoreExpr where
  show :: Expr CoreBndr -> [Char]
show = Expr CoreBndr -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr

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


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

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

checkBoolAlts :: [C.CoreAlt] -> LogicM (C.CoreExpr, C.CoreExpr)
checkBoolAlts :: [CoreAlt] -> LogicM (Expr CoreBndr, Expr CoreBndr)
checkBoolAlts [Alt (C.DataAlt DataCon
false) [] Expr CoreBndr
efalse, Alt (C.DataAlt DataCon
true) [] Expr CoreBndr
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
  = (Expr CoreBndr, Expr CoreBndr)
-> LogicM (Expr CoreBndr, Expr CoreBndr)
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr CoreBndr
efalse, Expr CoreBndr
etrue)

checkBoolAlts [Alt (C.DataAlt DataCon
true) [] Expr CoreBndr
etrue, Alt (C.DataAlt DataCon
false) [] Expr CoreBndr
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
  = (Expr CoreBndr, Expr CoreBndr)
-> LogicM (Expr CoreBndr, Expr CoreBndr)
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr CoreBndr
efalse, Expr CoreBndr
etrue)
checkBoolAlts [CoreAlt]
alts
  = [Char] -> LogicM (Expr CoreBndr, Expr CoreBndr)
forall a. [Char] -> LogicM a
throw ([Char]
"checkBoolAlts failed on " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [CoreAlt] -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr [CoreAlt]
alts)

-- @casesToLg v e alts@ transforms a case expression with scrutinee @e@ and
-- alternatives @alts@ into a logic expression. The variable @v@ is the binder
-- for the scrutinee in the case alternatives.
casesToLg :: Var -> Expr -> [C.CoreAlt] -> LogicM Expr
casesToLg :: CoreBndr
-> ExprBV Symbol Symbol
-> [CoreAlt]
-> ExceptT Error (ReaderT LState Identity) (ExprBV Symbol Symbol)
casesToLg CoreBndr
v ExprBV Symbol Symbol
e [CoreAlt]
alts = (CoreAlt
 -> ExceptT
      Error (ReaderT LState Identity) (AltCon, ExprBV Symbol Symbol))
-> [CoreAlt]
-> ExceptT
     Error (ReaderT LState Identity) [(AltCon, ExprBV Symbol Symbol)]
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 (ExprBV Symbol Symbol
-> CoreAlt
-> ExceptT
     Error (ReaderT LState Identity) (AltCon, ExprBV Symbol Symbol)
altToLg ExprBV Symbol Symbol
e) [CoreAlt]
normAlts ExceptT
  Error (ReaderT LState Identity) [(AltCon, ExprBV Symbol Symbol)]
-> ([(AltCon, ExprBV Symbol Symbol)]
    -> ExceptT Error (ReaderT LState Identity) (ExprBV Symbol Symbol))
-> ExceptT Error (ReaderT LState Identity) (ExprBV Symbol Symbol)
forall a b.
ExceptT Error (ReaderT LState Identity) a
-> (a -> ExceptT Error (ReaderT LState Identity) b)
-> ExceptT Error (ReaderT LState Identity) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(AltCon, ExprBV Symbol Symbol)]
-> ExceptT Error (ReaderT LState Identity) (ExprBV Symbol Symbol)
go
  where
    normAlts :: [CoreAlt]
normAlts       = [CoreAlt] -> [CoreAlt]
normalizeAlts [CoreAlt]
alts
    go :: [(C.AltCon, Expr)] -> LogicM Expr
    go :: [(AltCon, ExprBV Symbol Symbol)]
-> ExceptT Error (ReaderT LState Identity) (ExprBV Symbol Symbol)
go [(AltCon
_,ExprBV Symbol Symbol
p)]     = ExprBV Symbol Symbol
-> ExceptT Error (ReaderT LState Identity) (ExprBV Symbol Symbol)
forall a. a -> ExceptT Error (ReaderT LState Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExprBV Symbol Symbol
p ExprBV Symbol Symbol
-> (Variable (ExprBV Symbol Symbol),
    ExprBV
      (Variable (ExprBV Symbol Symbol))
      (Variable (ExprBV Symbol Symbol)))
-> ExprBV Symbol Symbol
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
`subst1` (Symbol, ExprBV Symbol Symbol)
(Variable (ExprBV Symbol Symbol),
 ExprBV
   (Variable (ExprBV Symbol Symbol))
   (Variable (ExprBV Symbol Symbol)))
su)
    go ((AltCon
d,ExprBV Symbol Symbol
p):[(AltCon, ExprBV Symbol Symbol)]
dps) = do c <- AltCon
-> ExprBV Symbol Symbol
-> ExceptT Error (ReaderT LState Identity) (ExprBV Symbol Symbol)
checkDataAlt AltCon
d ExprBV Symbol Symbol
e
                        e' <- go dps
                        return (EIte c p e' `subst1` su)
    go []          = Maybe SrcSpan
-> [Char]
-> ExceptT Error (ReaderT LState Identity) (ExprBV Symbol Symbol)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (CoreBndr -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan CoreBndr
v)) ([Char]
 -> ExceptT Error (ReaderT LState Identity) (ExprBV Symbol Symbol))
-> [Char]
-> ExceptT Error (ReaderT LState Identity) (ExprBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ [Char]
"Unexpected empty cases in casesToLg: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ExprBV Symbol Symbol -> [Char]
forall a. Show a => a -> [Char]
show ExprBV Symbol Symbol
e
    su :: (Symbol, ExprBV Symbol Symbol)
su             = (CoreBndr -> Symbol
forall a. Symbolic a => a -> Symbol
symbol CoreBndr
v, ExprBV Symbol Symbol
e)

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

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

altToLg :: Expr -> C.CoreAlt -> LogicM (C.AltCon, Expr)
altToLg :: ExprBV Symbol Symbol
-> CoreAlt
-> ExceptT
     Error (ReaderT LState Identity) (AltCon, ExprBV Symbol Symbol)
altToLg ExprBV Symbol Symbol
de (Alt a :: AltCon
a@(C.DataAlt DataCon
d) [CoreBndr]
xs Expr CoreBndr
e) = do
    p  <- Expr CoreBndr
-> ExceptT Error (ReaderT LState Identity) (ExprBV Symbol Symbol)
coreToLg Expr CoreBndr
e
    dm <- reader lsDCMap
    allowTC <- reader (typeclass . lsConfig)
    let su = [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
mkSubst ([(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol)
-> [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall a b. (a -> b) -> a -> b
$ [[(Symbol, ExprBV Symbol Symbol)]]
-> [(Symbol, ExprBV Symbol Symbol)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ DataConMap
-> ExprBV Symbol Symbol
-> DataCon
-> CoreBndr
-> Int
-> [(Symbol, ExprBV Symbol Symbol)]
dataConProj DataConMap
dm ExprBV Symbol Symbol
de DataCon
d CoreBndr
x Int
i | (CoreBndr
x, Int
i) <- [CoreBndr] -> [Int] -> [(CoreBndr, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((CoreBndr -> Bool) -> [CoreBndr] -> [CoreBndr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (CoreBndr -> Bool) -> CoreBndr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. if Bool
allowTC then CoreBndr -> Bool
GM.isEmbeddedDictVar else CoreBndr -> Bool
GM.isEvVar) [CoreBndr]
xs) [Int
1..]]
    return (a, subst su p)

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

dataConProj :: DataConMap -> Expr -> DataCon -> Var -> Int -> [(Symbol, Expr)]
dataConProj :: DataConMap
-> ExprBV Symbol Symbol
-> DataCon
-> CoreBndr
-> Int
-> [(Symbol, ExprBV Symbol Symbol)]
dataConProj DataConMap
dm ExprBV Symbol Symbol
de DataCon
d CoreBndr
x Int
i = [(CoreBndr -> Symbol
forall a. Symbolic a => a -> Symbol
symbol CoreBndr
x, ExprBV Symbol Symbol
t), (CoreBndr -> Symbol
forall t. NamedThing t => t -> Symbol
GM.simplesymbol CoreBndr
x, ExprBV Symbol Symbol
t)]
  where
    t :: ExprBV Symbol Symbol
t | DataCon -> Bool
primDataCon  DataCon
d  = ExprBV Symbol Symbol
de
      | Bool
otherwise       = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
EApp (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
EVar (Symbol -> ExprBV Symbol Symbol) -> Symbol -> ExprBV Symbol Symbol
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) ExprBV Symbol Symbol
de

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

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

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

    deList :: Expr -> [Expr]
    deList :: ExprBV Symbol Symbol -> [ExprBV Symbol Symbol]
deList (EApp (EApp (EVar Symbol
cons) ExprBV Symbol Symbol
e) ExprBV Symbol Symbol
es)
      | Symbol
cons Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show '(:))
      = ExprBV Symbol Symbol
eExprBV Symbol Symbol
-> [ExprBV Symbol Symbol] -> [ExprBV Symbol Symbol]
forall a. a -> [a] -> [a]
:ExprBV Symbol Symbol -> [ExprBV Symbol Symbol]
deList ExprBV Symbol Symbol
es
    deList (EVar Symbol
nil)
      | Symbol
nil Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show '[])
      = []
    deList ExprBV Symbol Symbol
e
      = [ExprBV Symbol Symbol
e]

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

makeApp :: Expr -> LogicMap -> Located Symbol-> [Expr] -> Expr
makeApp :: ExprBV Symbol Symbol
-> LogicMap
-> Located Symbol
-> [ExprBV Symbol Symbol]
-> ExprBV Symbol Symbol
makeApp ExprBV Symbol Symbol
_ LogicMap
_ Located Symbol
f [ExprBV Symbol Symbol
e]
  | Located Symbol -> Symbol
forall a. Located a -> a
val Located Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show 'negate)
  = ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v
ENeg ExprBV Symbol Symbol
e
  | Located Symbol -> Symbol
forall a. Located a -> a
val Located Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show 'fromInteger)
  , ECon Constant
c <- ExprBV Symbol Symbol
e
  = Constant -> ExprBV Symbol Symbol
forall b v. Constant -> ExprBV b v
ECon Constant
c
  | (Symbol
modName, Symbol
sym) <- Symbol -> (Symbol, Symbol)
GM.splitModuleName (Located Symbol -> Symbol
forall a. Located a -> a
val Located Symbol
f)
  , [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol ([Char]
"Ghci" :: String) Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
modName
  , Symbol
sym Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"len"
  = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
EApp (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
EVar Symbol
sym) ExprBV Symbol Symbol
e

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

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

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

brels :: M.HashMap Symbol Brel
brels :: HashMap Symbol Brel
brels = [(Symbol, Brel)] -> HashMap Symbol Brel
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [ ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show '(==)), Brel
Eq)
                   , ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show '(/=)), Brel
Ne)
                   , ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show '(>=)), Brel
Ge)
                   , ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show '(>)) , Brel
Gt)
                   , ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show '(<=)), Brel
Le)
                   , ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> [Char]
forall a. Show a => a -> [Char]
show '(<)) , Brel
Lt)
                   ]

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

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}. Expr b -> (Expr b, [Expr b])
go Expr t
exprt

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

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

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

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

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

mkLit :: Literal -> Maybe Expr
mkLit :: Literal -> Maybe (ExprBV Symbol Symbol)
mkLit (LitNumber LitNumType
_ Integer
n) = Integer -> Maybe (ExprBV Symbol Symbol)
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 (ExprBV Symbol Symbol)
mkR Rational
n
mkLit (LitDouble Rational
n)    = Rational -> Maybe (ExprBV Symbol Symbol)
mkR Rational
n
mkLit (LitString    ByteString
s) = ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just (ByteString -> ExprBV Symbol Symbol
mkS ByteString
s)
mkLit (LitChar   Char
c)    = Char -> Maybe (ExprBV Symbol Symbol)
mkC Char
c
mkLit Literal
_                 = Maybe (ExprBV Symbol Symbol)
forall a. Maybe a
Nothing -- ELit sym sort

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

mkR :: Rational -> Maybe Expr
mkR :: Rational -> Maybe (ExprBV Symbol Symbol)
mkR                    = ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just (ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol))
-> (Rational -> ExprBV Symbol Symbol)
-> Rational
-> Maybe (ExprBV Symbol Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> ExprBV Symbol Symbol
forall b v. Constant -> ExprBV b v
ECon (Constant -> ExprBV Symbol Symbol)
-> (Rational -> Constant) -> Rational -> ExprBV Symbol Symbol
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 -> Expr
mkS :: ByteString -> ExprBV Symbol Symbol
mkS = SymConst -> ExprBV Symbol Symbol
forall b v. SymConst -> ExprBV b v
ESym (SymConst -> ExprBV Symbol Symbol)
-> (ByteString -> SymConst) -> ByteString -> ExprBV Symbol Symbol
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 (ExprBV Symbol Symbol)
mkC                    = ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol)
forall a. a -> Maybe a
Just (ExprBV Symbol Symbol -> Maybe (ExprBV Symbol Symbol))
-> (Char -> ExprBV Symbol Symbol)
-> Char
-> Maybe (ExprBV Symbol Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> ExprBV Symbol Symbol
forall b v. Constant -> ExprBV b v
ECon (Constant -> ExprBV Symbol Symbol)
-> (Char -> Constant) -> Char -> ExprBV Symbol Symbol
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               = [Char] -> Text
T.pack ([Char] -> Text) -> (Char -> [Char]) -> Char -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> [Char]) -> (Char -> Int) -> Char -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
Data.Char.ord

ignoreVar :: Id -> Bool
ignoreVar :: CoreBndr -> Bool
ignoreVar CoreBndr
i = CoreBndr -> Symbol
simpleSymbolVar CoreBndr
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.
isBangInteger :: [C.CoreAlt] -> Bool
isBangInteger :: [CoreAlt] -> Bool
isBangInteger [Alt (C.DataAlt DataCon
s) [CoreBndr]
_ Expr CoreBndr
_, Alt (C.DataAlt DataCon
jp) [CoreBndr]
_ Expr CoreBndr
_, Alt (C.DataAlt DataCon
jn) [CoreBndr]
_ Expr CoreBndr
_]
  =  DataCon
s  DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
Ghc.integerISDataCon
  Bool -> Bool -> Bool
&& DataCon
jp DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
Ghc.integerIPDataCon
  Bool -> Bool -> Bool
&& DataCon
jn DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
Ghc.integerINDataCon
isBangInteger [CoreAlt]
_ = Bool
False

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

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

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

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

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

-- | 'normalizeCoreExpr allowTC e' simplifies the Core expression 'e' by:
--   1. inlining predicates (i.e. applications of measures that return Bool)
--   2. inlining ANF variables (i.e. variables that are introduced by the ANF transformation)
--   3. simplifying the expression by removing dead binders and applications of
--      type arguments and dictionaries.
--
-- The 'allowTC' flag controls whether type class dictionaries are considered erasable
-- and will be removed from the expression.
--
normalizeCoreExpr :: Bool -> CoreExpr -> CoreExpr
normalizeCoreExpr :: Bool -> Expr CoreBndr -> Expr CoreBndr
normalizeCoreExpr Bool
allowTC = Expr CoreBndr -> Expr CoreBndr
inline_preds (Expr CoreBndr -> Expr CoreBndr)
-> (Expr CoreBndr -> Expr CoreBndr)
-> Expr CoreBndr
-> Expr CoreBndr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr CoreBndr -> Expr CoreBndr
inline_anf (Expr CoreBndr -> Expr CoreBndr)
-> (Expr CoreBndr -> Expr CoreBndr)
-> Expr CoreBndr
-> Expr CoreBndr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Expr CoreBndr -> Expr CoreBndr
simplifyCoreExpr Bool
allowTC
  where
    inline_preds :: Expr CoreBndr -> Expr CoreBndr
inline_preds = (CoreBndr -> Bool) -> Expr CoreBndr -> Expr CoreBndr
inlineCoreExpr (HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
eqType Type
boolTy (Type -> Bool) -> (CoreBndr -> Type) -> CoreBndr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreBndr -> Type
GM.expandVarType)
    inline_anf :: Expr CoreBndr -> Expr CoreBndr
inline_anf   = (CoreBndr -> Bool) -> Expr CoreBndr -> Expr CoreBndr
inlineCoreExpr CoreBndr -> Bool
isANF

-- | 'simplifyCoreExpr allowTC e' simplifies the Core expression 'e' by removing
-- applications of type arguments and dictionaries, and by removing dead
-- binders.
--
-- The 'allowTC' flag controls whether type class dictionaries are considered
-- erasable.
--
-- If 'allowTC' is 'True', then type class dictionaries are considered erasable
-- and will be removed from the expression. If 'allowTC' is 'False', then type
-- class dictionaries are not considered erasable and will not be removed.
--
-- This function is used in 'normalizeCoreExpr' to simplify the Core expression
-- before inlining predicates and ANF variables.
--
-- The 'simplifyCoreExpr' function recursively traverses the Core expression and
-- applies the following simplifications:
--   1. It removes applications of type arguments (i.e. 'C.App e1 (C.Type _)').
--   2. It removes applications of variables that are considered erasable
--      (i.e. 'C.App e1 (C.Var v)' where 'v' is erasable).
--   3. It removes applications of lambda expressions where the binder is dead
--      (i.e. 'C.App (C.Lam x e) _' where 'x' is dead).
--   4. It removes lambda expressions where the binder is a type variable
--      (i.e. 'C.Lam x e' where 'x' is a type variable).
--   5. It removes lambda expressions where the binder is considered erasable
--      (i.e. 'C.Lam x e' where 'x' is erasable).
--   6. It removes non-recursive let bindings where the binder is considered
--      erasable (i.e. 'C.Let (C.NonRec x eb) e' where 'x' is erasable).
--   7. It removes recursive let bindings where all binders are considered
--      erasable (i.e. 'C.Let (C.Rec xes) e' where all 'x' in 'xes' are
--      erasable).
--   8. It simplifies case expressions that match on a boolean by checking if
--      the alternatives correspond to 'True' and 'False' and then substituting
--      the scrutinee with the appropriate alternative.
--   9. It simplifies case expressions by removing alternatives that correspond
--      to pattern match errors (i.e. 'isPatErrorAlt').
--   10. It recursively simplifies applications, casts, ticks, coercions, and
--       type expressions.
--
simplifyCoreExpr :: Bool -> CoreExpr -> CoreExpr
simplifyCoreExpr :: Bool -> Expr CoreBndr -> Expr CoreBndr
simplifyCoreExpr Bool
allowTC = Expr CoreBndr -> Expr CoreBndr
go
  where
    isDictOrErasable :: CoreBndr -> Bool
isDictOrErasable = if Bool
allowTC then CoreBndr -> Bool
GM.isEmbeddedDictVar else CoreBndr -> Bool
isErasable

    go :: CoreExpr -> CoreExpr
    go :: Expr CoreBndr -> Expr CoreBndr
go e :: Expr CoreBndr
e@(C.Var CoreBndr
_)
      = Expr CoreBndr
e
    go e :: Expr CoreBndr
e@(C.Lit Literal
_)
      = Expr CoreBndr
e
    go (C.App Expr CoreBndr
e1 (C.Type Type
_))
      = Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e1
    go (C.App Expr CoreBndr
e1 (C.Var CoreBndr
v))
      | CoreBndr -> Bool
isDictOrErasable CoreBndr
v
      = Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e1
    go (C.App (C.Lam CoreBndr
x Expr CoreBndr
e) Expr CoreBndr
_)
      | CoreBndr -> Bool
isDead CoreBndr
x
      = Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e
    go (C.App Expr CoreBndr
e1 Expr CoreBndr
e2)
      = Expr CoreBndr -> Expr CoreBndr -> Expr CoreBndr
forall b. Expr b -> Expr b -> Expr b
C.App (Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e1) (Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e2)
    go (C.Lam CoreBndr
x Expr CoreBndr
e)
      | CoreBndr -> Bool
isTyVar CoreBndr
x
      = Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e
    go (C.Lam CoreBndr
x Expr CoreBndr
e)
      | CoreBndr -> Bool
isDictOrErasable CoreBndr
x
      = Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e
    go (C.Lam CoreBndr
x Expr CoreBndr
e)
      = CoreBndr -> Expr CoreBndr -> Expr CoreBndr
forall b. b -> Expr b -> Expr b
C.Lam CoreBndr
x (Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e)
    go (C.Let (C.NonRec CoreBndr
x Expr CoreBndr
eb) Expr CoreBndr
e)
      | CoreBndr -> Bool
isDictOrErasable CoreBndr
x
      = Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e
      | Bool
otherwise
      = Bind CoreBndr -> Expr CoreBndr -> Expr CoreBndr
forall b. Bind b -> Expr b -> Expr b
C.Let (CoreBndr -> Expr CoreBndr -> Bind CoreBndr
forall b. b -> Expr b -> Bind b
C.NonRec CoreBndr
x (Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
eb)) (Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e)
    go (C.Let (C.Rec [(CoreBndr, Expr CoreBndr)]
xes) Expr CoreBndr
e)
      | ((CoreBndr, Expr CoreBndr) -> Bool)
-> [(CoreBndr, Expr CoreBndr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (CoreBndr -> Bool
isDictOrErasable (CoreBndr -> Bool)
-> ((CoreBndr, Expr CoreBndr) -> CoreBndr)
-> (CoreBndr, Expr CoreBndr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoreBndr, Expr CoreBndr) -> CoreBndr
forall a b. (a, b) -> a
fst) [(CoreBndr, Expr CoreBndr)]
xes
      = Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e
      | Bool
otherwise
      = Bind CoreBndr -> Expr CoreBndr -> Expr CoreBndr
forall b. Bind b -> Expr b -> Expr b
C.Let ([(CoreBndr, Expr CoreBndr)] -> Bind CoreBndr
forall b. [(b, Expr b)] -> Bind b
C.Rec (((CoreBndr, Expr CoreBndr) -> (CoreBndr, Expr CoreBndr))
-> [(CoreBndr, Expr CoreBndr)] -> [(CoreBndr, Expr CoreBndr)]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr CoreBndr -> Expr CoreBndr)
-> (CoreBndr, Expr CoreBndr) -> (CoreBndr, Expr CoreBndr)
forall a b. (a -> b) -> (CoreBndr, a) -> (CoreBndr, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr CoreBndr -> Expr CoreBndr
go) [(CoreBndr, Expr CoreBndr)]
xes)) (Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e)
    go (C.Case Expr CoreBndr
e CoreBndr
x Type
_t alts :: [CoreAlt]
alts@[Alt AltCon
_ [CoreBndr]
_ Expr CoreBndr
ee,CoreAlt
_,CoreAlt
_])
      | [CoreAlt] -> Bool
isBangInteger [CoreAlt]
alts
      = HashMap CoreBndr (Expr CoreBndr) -> Expr CoreBndr -> Expr CoreBndr
forall a. Subable a => HashMap CoreBndr (Expr CoreBndr) -> a -> a
sub (CoreBndr -> Expr CoreBndr -> HashMap CoreBndr (Expr CoreBndr)
forall k v. Hashable k => k -> v -> HashMap k v
M.singleton CoreBndr
x (Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e)) (Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
ee)
    go (C.Case Expr CoreBndr
e CoreBndr
x Type
t [CoreAlt]
alts)
      = Expr CoreBndr -> CoreBndr -> Type -> [CoreAlt] -> Expr CoreBndr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
C.Case (Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e) CoreBndr
x Type
t ([CoreAlt] -> Expr CoreBndr) -> [CoreAlt] -> Expr CoreBndr
forall a b. (a -> b) -> a -> b
$
         (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)
           [ AltCon -> [CoreBndr] -> Expr CoreBndr -> CoreAlt
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c [CoreBndr]
xs (Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
ealt) | Alt AltCon
c [CoreBndr]
xs Expr CoreBndr
ealt <- [CoreAlt]
alts ]
    go (C.Cast Expr CoreBndr
e Coercion
c)
      = Expr CoreBndr -> Coercion -> Expr CoreBndr
forall b. Expr b -> Coercion -> Expr b
C.Cast (Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e) Coercion
c
    go (C.Tick CoreTickish
_ Expr CoreBndr
e)
      = Expr CoreBndr -> Expr CoreBndr
go Expr CoreBndr
e
    go (C.Coercion Coercion
c)
      = Coercion -> Expr CoreBndr
forall b. Coercion -> Expr b
C.Coercion Coercion
c
    go (C.Type Type
t)
      = Type -> Expr CoreBndr
forall b. Type -> Expr b
C.Type Type
t

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