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

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

import           Data.ByteString                       (ByteString)
import           Prelude                               hiding (error)
import           Language.Haskell.Liquid.GHC.TypeRep   () -- needed for Eq 'Type'
import           Language.Haskell.Liquid.GHC.API       hiding (Expr, Located)
-- import qualified Id 
import qualified Var
import qualified TyCon 
import           Coercion
import qualified Pair
-- import qualified Text.Printf as Printf
import qualified CoreSyn                               as C
import           IdInfo
import qualified Data.List                             as L
import           Data.Maybe                            (listToMaybe) 
import qualified Data.Text                             as T
import qualified Data.Char 
import qualified Text.Printf as Printf 
import           Data.Text.Encoding
import           Data.Text.Encoding.Error
import           Control.Monad.State
import           Control.Monad.Except
import           Control.Monad.Identity
import qualified Language.Fixpoint.Misc                as Misc 
import           Language.Fixpoint.Types               hiding (panic, Error, R, simplify)
import qualified Language.Fixpoint.Types               as F
import qualified Language.Haskell.Liquid.GHC.Misc      as GM


import           Language.Haskell.Liquid.Bare.Types 
import           Language.Haskell.Liquid.Bare.DataType 
import           Language.Haskell.Liquid.Bare.Misc     (simpleSymbolVar)
import           Language.Haskell.Liquid.GHC.Play
import           Language.Haskell.Liquid.Types.Types   --     hiding (GhcInfo(..), GhcSpec (..), LM)
import           Language.Haskell.Liquid.Types.RefType

import qualified Data.HashMap.Strict                   as M

logicType :: (Reftable r) => Type -> RRType r
logicType :: Type -> RRType r
logicType Type
τ      = RTypeRep RTyCon RTyVar r -> RRType r
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar r -> RRType r)
-> RTypeRep RTyCon RTyVar r -> RRType r
forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar r
t { ty_binds :: [Symbol]
ty_binds = [Symbol]
bs, ty_args :: [RRType r]
ty_args = [RRType r]
as, ty_refts :: [r]
ty_refts = [r]
rs}
  where
    t :: RTypeRep RTyCon RTyVar r
t            = RRType r -> RTypeRep RTyCon RTyVar r
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (RRType r -> RTypeRep RTyCon RTyVar r)
-> RRType r -> RTypeRep RTyCon RTyVar r
forall a b. (a -> b) -> a -> b
$ Type -> RRType r
forall r. Monoid r => Type -> RRType r
ofType Type
τ
    ([Symbol]
bs, [RRType r]
as, [r]
rs) = [(Symbol, RRType r, r)] -> ([Symbol], [RRType r], [r])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([(Symbol, RRType r, r)] -> ([Symbol], [RRType r], [r]))
-> [(Symbol, RRType r, r)] -> ([Symbol], [RRType r], [r])
forall a b. (a -> b) -> a -> b
$ ((Symbol, RRType r, r) -> Bool)
-> [(Symbol, RRType r, r)] -> [(Symbol, RRType r, r)]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (RRType r -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType (RRType r -> Bool)
-> ((Symbol, RRType r, r) -> RRType r)
-> (Symbol, RRType r, r)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, RRType r, r) -> RRType r
forall a b c. (a, b, c) -> b
Misc.snd3) ([(Symbol, RRType r, r)] -> [(Symbol, RRType r, r)])
-> [(Symbol, RRType r, r)] -> [(Symbol, RRType r, r)]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [RRType r] -> [r] -> [(Symbol, RRType r, r)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 (RTypeRep RTyCon RTyVar r -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar r
t) (RTypeRep RTyCon RTyVar r -> [RRType r]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar r
t) (RTypeRep RTyCon RTyVar r -> [r]
forall c tv r. RTypeRep c tv r -> [r]
ty_refts RTypeRep RTyCon RTyVar r
t)

{- | [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 :: Var -> SpecType
inlineSpecType :: Var -> SpecType
inlineSpecType Var
v = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar RReft -> SpecType)
-> RTypeRep RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft
rep {ty_res :: SpecType
ty_res = SpecType
res SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` RReft
r , ty_binds :: [Symbol]
ty_binds = [Symbol]
xs}
  where
    r :: RReft
r              = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft (Expr -> Reft
mkR (LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
f ((Symbol, SpecType) -> Expr
forall b. (Symbol, b) -> Expr
mkA ((Symbol, SpecType) -> Expr) -> [(Symbol, SpecType)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
vxs))) Predicate
forall a. Monoid a => a
mempty
    rep :: RTypeRep RTyCon RTyVar RReft
rep            = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t
    res :: SpecType
res            = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
rep
    xs :: [Symbol]
xs             = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"x" :: String)) (Int -> Symbol) -> [Int] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..[Symbol] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Symbol] -> Int) -> [Symbol] -> Int
forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
rep]
    vxs :: [(Symbol, SpecType)]
vxs            = ((Symbol, SpecType) -> Bool)
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (SpecType -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType (SpecType -> Bool)
-> ((Symbol, SpecType) -> SpecType) -> (Symbol, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd) ([(Symbol, SpecType)] -> [(Symbol, SpecType)])
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
rep)
    f :: LocSymbol
f              = Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
v)
    t :: SpecType
t              = Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType (Var -> Type
GM.expandVarType Var
v) :: SpecType
    mkA :: (Symbol, b) -> Expr
mkA            = Symbol -> Expr
EVar (Symbol -> Expr) -> ((Symbol, b) -> Symbol) -> (Symbol, b) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, b) -> Symbol
forall a b. (a, b) -> a
fst 
    mkR :: Expr -> Reft
mkR            = if SpecType -> Bool
forall t t1. RType RTyCon t t1 -> Bool
isBool SpecType
res then Expr -> Reft
forall a. Predicate a => a -> Reft
propReft else Expr -> Reft
forall a. Expression a => a -> Reft
exprReft 

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

-- formerly: strengthenResult'
measureSpecType :: Var -> SpecType
measureSpecType :: Var -> SpecType
measureSpecType Var
v = ([Symbol] -> RReft)
-> [Symbol] -> [Integer] -> SpecType -> SpecType
forall c r a tv.
(TyConable c, Reftable r, Show a) =>
([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType c tv r
go [Symbol] -> RReft
mkT [] [Integer
1..] SpecType
t
  where 
    mkR :: Expr -> Reft
mkR | Bool
boolRes   = Expr -> Reft
forall a. Predicate a => a -> Reft
propReft 
        | Bool
otherwise = Expr -> Reft
forall a. Expression a => a -> Reft
exprReft  
    mkT :: [Symbol] -> RReft
mkT [Symbol]
xs          = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft (Expr -> Reft
mkR (Expr -> Reft) -> Expr -> Reft
forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
f (Symbol -> Expr
EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse [Symbol]
xs)) Predicate
forall a. Monoid a => a
mempty
    f :: LocSymbol
f               = Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
v) 
    t :: SpecType
t               = Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType (Var -> Type
GM.expandVarType Var
v) :: SpecType
    boolRes :: Bool
boolRes         =  SpecType -> Bool
forall t t1. RType RTyCon t t1 -> Bool
isBool (SpecType -> Bool) -> SpecType -> Bool
forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res (RTypeRep RTyCon RTyVar RReft -> SpecType)
-> RTypeRep RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t 

    go :: ([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i (RAllT RTVU c tv
a RType c tv r
t r
r)    = RTVU c tv -> RType c tv r -> r -> RType c tv r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a (([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i RType c tv r
t) r
r 
    go [Symbol] -> r
f [Symbol]
args [a]
i (RAllP PVU c tv
p RType c tv r
t)      = PVU c tv -> RType c tv r -> RType c tv r
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU c tv
p (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ ([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i RType c tv r
t
    go [Symbol] -> r
f [Symbol]
args [a]
i (RFun Symbol
x RType c tv r
t1 RType c tv r
t2 r
r)
     | RType c tv r -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType c tv r
t1           = Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RType c tv r
t1 (([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType c tv r
go [Symbol] -> r
f [Symbol]
args [a]
i RType c tv r
t2) r
r
    go [Symbol] -> r
f [Symbol]
args [a]
i t :: RType c tv r
t@(RFun Symbol
_ RType c tv r
t1 RType c tv r
t2 r
r)
     | RType c tv r -> Bool
forall c tv r. RType c tv r -> Bool
hasRApps RType c tv r
t               = Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x' RType c tv r
t1 (([Symbol] -> r) -> [Symbol] -> [a] -> RType c tv r -> RType c tv r
go [Symbol] -> r
f (Symbol
x'Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
args) ([a] -> [a]
forall a. [a] -> [a]
tail [a]
i) RType c tv r
t2) r
r
                                       where x' :: Symbol
x' = Symbol -> a -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"x" :: String)) ([a] -> a
forall a. [a] -> a
head [a]
i)
    go [Symbol] -> r
f [Symbol]
args [a]
_ RType c tv r
t                = RType c tv r
t RType c tv r -> r -> RType c tv r
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` [Symbol] -> r
f [Symbol]
args

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

type LogicM = ExceptT Error (StateT LState Identity)

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

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

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

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

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

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

    -- mkAlt :: LocSymbol -> (Expr -> Body) -> [Var] -> Var -> (C.AltCon, [Var], C.CoreExpr)
    mkAlt :: LocSymbol
-> (Expr -> Body)
-> p
-> Var
-> CoreAlt
-> ExceptT
     Error (StateT LState Identity) (Def (Located (RRType r)) DataCon)
mkAlt LocSymbol
x Expr -> Body
ctor p
_args Var
dx (C.DataAlt DataCon
d, [Var]
xs, CoreExpr
e)
      = LocSymbol
-> DataCon
-> Maybe (Located (RRType r))
-> [(Symbol, Maybe (Located (RRType r)))]
-> Body
-> Def (Located (RRType r)) DataCon
forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
x {- (toArgs id args) -} DataCon
d (Located (RRType r) -> Maybe (Located (RRType r))
forall a. a -> Maybe a
Just (Located (RRType r) -> Maybe (Located (RRType r)))
-> Located (RRType r) -> Maybe (Located (RRType r))
forall a b. (a -> b) -> a -> b
$ Var -> Located (RRType r)
forall r. Reftable r => Var -> Located (RRType r)
varRType Var
dx) ((Located (RRType r) -> Maybe (Located (RRType r)))
-> [Var] -> [(Symbol, Maybe (Located (RRType r)))]
forall r b.
Reftable r =>
(Located (RRType r) -> b) -> [Var] -> [(Symbol, b)]
toArgs Located (RRType r) -> Maybe (Located (RRType r))
forall a. a -> Maybe a
Just [Var]
xs') 
      (Body -> Def (Located (RRType r)) DataCon)
-> (Expr -> Body) -> Expr -> Def (Located (RRType r)) DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Body
ctor 
      (Expr -> Body) -> (Expr -> Expr) -> Expr -> Body
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
`subst1` (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
dx, LocSymbol -> [Expr] -> Expr
F.mkEApp (DataCon -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol DataCon
d) (Var -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (Var -> Expr) -> [Var] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs'))) 
     (Expr -> Def (Located (RRType r)) DataCon)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT
     Error (StateT LState Identity) (Def (Located (RRType r)) DataCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
e
      where xs' :: [Var]
xs' = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Var -> Bool) -> Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Bool
GM.isEvVar) [Var]
xs
    mkAlt LocSymbol
_ Expr -> Body
_ p
_ Var
_ CoreAlt
alt 
      = String
-> ExceptT
     Error (StateT LState Identity) (Def (Located (RRType r)) DataCon)
forall a. String -> LogicM a
throw (String
 -> ExceptT
      Error (StateT LState Identity) (Def (Located (RRType r)) DataCon))
-> String
-> ExceptT
     Error (StateT LState Identity) (Def (Located (RRType r)) DataCon)
forall a b. (a -> b) -> a -> b
$ String
"Bad alternative" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreAlt -> String
forall a. Outputable a => a -> String
GM.showPpr CoreAlt
alt

    mkDef :: LocSymbol
-> (Expr -> Body)
-> p
-> Var
-> Maybe [(ctor, b, [Type])]
-> Maybe CoreExpr
-> ExceptT
     Error (StateT LState Identity) [Def (Located (RRType r)) ctor]
mkDef LocSymbol
x Expr -> Body
ctor p
_args Var
dx (Just [(ctor, b, [Type])]
dtss) (Just CoreExpr
e) = do  
      Body
eDef   <- Expr -> Body
ctor (Expr -> Body)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Body
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
e
      -- let ys  = toArgs id args
      let dxt :: Maybe (Located (RRType r))
dxt = Located (RRType r) -> Maybe (Located (RRType r))
forall a. a -> Maybe a
Just (Var -> Located (RRType r)
forall r. Reftable r => Var -> Located (RRType r)
varRType Var
dx)
      [Def (Located (RRType r)) ctor]
-> ExceptT
     Error (StateT LState Identity) [Def (Located (RRType r)) ctor]
forall (m :: * -> *) a. Monad m => a -> m a
return  [ LocSymbol
-> ctor
-> Maybe (Located (RRType r))
-> [(Symbol, Maybe (Located (RRType r)))]
-> Body
-> Def (Located (RRType r)) ctor
forall ty ctor.
LocSymbol
-> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
Def LocSymbol
x {- ys -} ctor
d Maybe (Located (RRType r))
dxt (LocSymbol -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]
forall r.
Monoid r =>
LocSymbol -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]
defArgs LocSymbol
x [Type]
ts) Body
eDef | (ctor
d, b
_, [Type]
ts) <- [(ctor, b, [Type])]
dtss ]
    
    mkDef LocSymbol
_ Expr -> Body
_ p
_ Var
_ Maybe [(ctor, b, [Type])]
_ Maybe CoreExpr
_ = 
      [Def (Located (RRType r)) ctor]
-> ExceptT
     Error (StateT LState Identity) [Def (Located (RRType r)) ctor]
forall (m :: * -> *) a. Monad m => a -> m a
return [] 

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

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

coreToDef :: Reftable r => LocSymbol -> Var -> C.CoreExpr
          -> LogicM [Def (Located (RRType r)) DataCon]
coreToDef :: LocSymbol
-> Var -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
coreToDef LocSymbol
x Var
_ CoreExpr
e                   = [Var] -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
forall r.
Reftable r =>
[Var] -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
go [] (CoreExpr -> LogicM [Def (Located (RRType r)) DataCon])
-> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
inlinePreds (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e
  where
    go :: [Var] -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
go [Var]
args   (C.Lam  Var
x CoreExpr
e)        = [Var] -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
go (Var
xVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
args) CoreExpr
e
    go [Var]
args   (C.Tick Tickish Var
_ CoreExpr
e)        = [Var] -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
go [Var]
args CoreExpr
e
    go (Var
z:[Var]
zs) (C.Case CoreExpr
_ Var
y Type
t [CoreAlt]
alts) = LocSymbol
-> Var
-> [Var]
-> Var
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
forall r.
Reftable r =>
LocSymbol
-> Var
-> [Var]
-> Var
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
coreAltToDef LocSymbol
x Var
z [Var]
zs Var
y Type
t [CoreAlt]
alts 
    go (Var
z:[Var]
zs) CoreExpr
e                   
      | Just Type
t <- Var -> Maybe Type
isMeasureArg Var
z  = LocSymbol
-> Var
-> [Var]
-> Var
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
forall r.
Reftable r =>
LocSymbol
-> Var
-> [Var]
-> Var
-> Type
-> [CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
coreAltToDef LocSymbol
x Var
z [Var]
zs Var
z Type
t [(AltCon
C.DEFAULT, [], CoreExpr
e)]
    go [Var]
_ CoreExpr
_                        = LocSymbol -> String -> LogicM [Def (Located (RRType r)) DataCon]
forall a. LocSymbol -> String -> a
measureFail LocSymbol
x String
"Does not have a case-of at the top-level" 

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

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

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


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

coreToFun :: LocSymbol -> Var -> C.CoreExpr ->  LogicM ([Var], Either Expr Expr)
coreToFun :: LocSymbol -> Var -> CoreExpr -> LogicM ([Var], Either Expr Expr)
coreToFun LocSymbol
_ Var
_v CoreExpr
e = [Var] -> CoreExpr -> LogicM ([Var], Either Expr Expr)
forall a.
[Var]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Var], Either a Expr)
go [] (CoreExpr -> LogicM ([Var], Either Expr Expr))
-> CoreExpr -> LogicM ([Var], Either Expr Expr)
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
normalize CoreExpr
e
  where
    go :: [Var]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Var], Either a Expr)
go [Var]
acc (C.Lam Var
x CoreExpr
e)  | Var -> Bool
isTyVar    Var
x = [Var]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Var], Either a Expr)
go [Var]
acc CoreExpr
e
    go [Var]
acc (C.Lam Var
x CoreExpr
e)  | Var -> Bool
isErasable Var
x = [Var]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Var], Either a Expr)
go [Var]
acc CoreExpr
e
    go [Var]
acc (C.Lam Var
x CoreExpr
e)  = [Var]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Var], Either a Expr)
go (Var
xVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
acc) CoreExpr
e
    go [Var]
acc (C.Tick Tickish Var
_ CoreExpr
e) = [Var]
-> CoreExpr
-> ExceptT Error (StateT LState Identity) ([Var], Either a Expr)
go [Var]
acc CoreExpr
e
    go [Var]
acc CoreExpr
e            = ([Var] -> [Var]
forall a. [a] -> [a]
reverse [Var]
acc,) (Either a Expr -> ([Var], Either a Expr))
-> (Expr -> Either a Expr) -> Expr -> ([Var], Either a Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Either a Expr
forall a b. b -> Either a b
Right (Expr -> ([Var], Either a Expr))
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) ([Var], Either a Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
e
    

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

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


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




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

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

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

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

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

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

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

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

altToLg :: Expr -> C.CoreAlt -> LogicM (C.AltCon, Expr)
altToLg :: Expr
-> CoreAlt -> ExceptT Error (StateT LState Identity) (AltCon, Expr)
altToLg Expr
de (a :: AltCon
a@(C.DataAlt DataCon
d), [Var]
xs, CoreExpr
e) = do 
  Expr
p  <- CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
e
  DataConMap
dm <- (LState -> DataConMap)
-> ExceptT Error (StateT LState Identity) DataConMap
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets LState -> DataConMap
lsDCMap
  let su :: Subst
su = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [[(Symbol, Expr)]] -> [(Symbol, Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ DataConMap -> Expr -> DataCon -> Var -> Int -> [(Symbol, Expr)]
dataConProj DataConMap
dm Expr
de DataCon
d Var
x Int
i | (Var
x, Int
i) <- [Var] -> [Int] -> [(Var, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Var -> Bool) -> Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Bool
GM.isEvVar) [Var]
xs) [Int
1..]]
  (AltCon, Expr)
-> ExceptT Error (StateT LState Identity) (AltCon, Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (AltCon
a, Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p)

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

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

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

coreToIte :: C.CoreExpr -> (C.CoreExpr, C.CoreExpr) -> LogicM Expr
coreToIte :: CoreExpr
-> (CoreExpr, CoreExpr)
-> ExceptT Error (StateT LState Identity) Expr
coreToIte CoreExpr
e (CoreExpr
efalse, CoreExpr
etrue)
  = do Expr
p  <- CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
e
       Expr
e1 <- CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
efalse
       Expr
e2 <- CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
etrue
       Expr -> ExceptT Error (StateT LState Identity) Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> ExceptT Error (StateT LState Identity) Expr)
-> Expr -> ExceptT Error (StateT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr -> Expr
EIte Expr
p Expr
e2 Expr
e1

toPredApp :: C.CoreExpr -> LogicM Expr
toPredApp :: CoreExpr -> ExceptT Error (StateT LState Identity) Expr
toPredApp CoreExpr
p = (Maybe Symbol, [CoreExpr])
-> ExceptT Error (StateT LState Identity) Expr
go ((Maybe Symbol, [CoreExpr])
 -> ExceptT Error (StateT LState Identity) Expr)
-> (CoreExpr -> (Maybe Symbol, [CoreExpr]))
-> CoreExpr
-> ExceptT Error (StateT LState Identity) Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoreExpr -> Maybe Symbol)
-> (CoreExpr, [CoreExpr]) -> (Maybe Symbol, [CoreExpr])
forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst CoreExpr -> Maybe Symbol
opSym ((CoreExpr, [CoreExpr]) -> (Maybe Symbol, [CoreExpr]))
-> (CoreExpr -> (CoreExpr, [CoreExpr]))
-> CoreExpr
-> (Maybe Symbol, [CoreExpr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> (CoreExpr, [CoreExpr])
forall t. Expr t -> (Expr t, [Expr t])
splitArgs (CoreExpr -> ExceptT Error (StateT LState Identity) Expr)
-> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
forall a b. (a -> b) -> a -> b
$ CoreExpr
p
  where
    opSym :: CoreExpr -> Maybe Symbol
opSym = (Symbol -> Symbol) -> Maybe Symbol -> Maybe Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Symbol -> Symbol
GM.dropModuleNames (Maybe Symbol -> Maybe Symbol)
-> (CoreExpr -> Maybe Symbol) -> CoreExpr -> Maybe Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> Maybe Symbol
tomaybesymbol
    go :: (Maybe Symbol, [CoreExpr])
-> ExceptT Error (StateT LState Identity) Expr
go (Just Symbol
f, [CoreExpr
e1, CoreExpr
e2])
      | Just Brel
rel <- Symbol -> HashMap Symbol Brel -> Maybe Brel
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
f HashMap Symbol Brel
brels
      = Brel -> Expr -> Expr -> Expr
PAtom Brel
rel (Expr -> Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
e1 ExceptT Error (StateT LState Identity) (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
e2
    go (Just Symbol
f, [CoreExpr
e])
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"not" :: String)
      = Expr -> Expr
PNot (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
e
    go (Just Symbol
f, [CoreExpr
e1, CoreExpr
e2])
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"||" :: String)
      = [Expr] -> Expr
POr ([Expr] -> Expr)
-> ExceptT Error (StateT LState Identity) [Expr]
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoreExpr -> ExceptT Error (StateT LState Identity) Expr)
-> [CoreExpr] -> ExceptT Error (StateT LState Identity) [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg [CoreExpr
e1, CoreExpr
e2]
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"&&" :: String)
      = [Expr] -> Expr
PAnd ([Expr] -> Expr)
-> ExceptT Error (StateT LState Identity) [Expr]
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoreExpr -> ExceptT Error (StateT LState Identity) Expr)
-> [CoreExpr] -> ExceptT Error (StateT LState Identity) [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg [CoreExpr
e1, CoreExpr
e2]
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"==>" :: String)
      = Expr -> Expr -> Expr
PImp (Expr -> Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
e1 ExceptT Error (StateT LState Identity) (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
e2
    go (Just Symbol
f, [CoreExpr
es])
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"or" :: String)
      = [Expr] -> Expr
POr  ([Expr] -> Expr) -> (Expr -> [Expr]) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
deList (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
es
      | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"and" :: String)
      = [Expr] -> Expr
PAnd ([Expr] -> Expr) -> (Expr -> [Expr]) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
deList (Expr -> Expr)
-> ExceptT Error (StateT LState Identity) Expr
-> ExceptT Error (StateT LState Identity) Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreExpr -> ExceptT Error (StateT LState Identity) Expr
coreToLg CoreExpr
es
    go (Maybe Symbol
_, [CoreExpr]
_)
      = CoreExpr -> ExceptT Error (StateT LState Identity) Expr
toLogicApp CoreExpr
p
    
    deList :: Expr -> [Expr]
    deList :: Expr -> [Expr]
deList (EApp (EApp (EVar Symbol
cons) Expr
e) Expr
es)
      | Symbol
cons Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Types.:" :: String)
      = Expr
eExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:Expr -> [Expr]
deList Expr
es 
    deList (EVar Symbol
nil)
      | Symbol
nil Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Types.[]" :: String)
      = [] 
    deList Expr
e 
      = [Expr
e]

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

makeApp :: Expr -> LogicMap -> Located Symbol-> [Expr] -> Expr
makeApp :: Expr -> LogicMap -> LocSymbol -> [Expr] -> Expr
makeApp Expr
_ LogicMap
_ LocSymbol
f [Expr
e] | LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"GHC.Num.negate" :: String)
  = Expr -> Expr
ENeg Expr
e

makeApp Expr
_ LogicMap
_ LocSymbol
f [Expr
e1, Expr
e2] | Just Bop
op <- Symbol -> HashMap Symbol Bop -> Maybe Bop
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
f) HashMap Symbol Bop
bops
  = Bop -> Expr -> Expr -> Expr
EBin Bop
op Expr
e1 Expr
e2

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

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

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

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

isCst :: Type -> Bool
isCst :: Type -> Bool
isCst (ForAllTy TyCoVarBinder
_ Type
t) = Type -> Bool
isCst Type
t
isCst (FunTy AnonArgFlag
_ Type
_ Type
_)    = Bool
False
isCst Type
_              = Bool
True


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

bops :: M.HashMap Symbol Bop
bops :: HashMap Symbol Bop
bops = [(Symbol, Bop)] -> HashMap Symbol Bop
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (String -> Symbol
numSymbol String
"+", Bop
Plus)
                  , (String -> Symbol
numSymbol String
"-", Bop
Minus)
                  , (String -> Symbol
numSymbol String
"*", Bop
Times)
                  , (String -> Symbol
numSymbol String
"/", Bop
Div)
                  , (String -> Symbol
realSymbol String
"/", Bop
Div)
                  , (String -> Symbol
numSymbol String
"%", Bop
Mod)
                  ]
  where
    numSymbol :: String -> Symbol
    numSymbol :: String -> Symbol
numSymbol =  String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> (String -> String) -> String -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
forall a. [a] -> [a] -> [a]
(++) String
"GHC.Num."
    realSymbol :: String -> Symbol
    realSymbol :: String -> Symbol
realSymbol =  String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> (String -> String) -> String -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
forall a. [a] -> [a] -> [a]
(++) String
"GHC.Real."

splitArgs :: C.Expr t -> (C.Expr t, [C.Arg t])
splitArgs :: Expr t -> (Expr t, [Expr t])
splitArgs Expr t
e = (Expr t
f, [Expr t] -> [Expr t]
forall a. [a] -> [a]
reverse [Expr t]
es)
 where
    (Expr t
f, [Expr t]
es) = Expr t -> (Expr t, [Expr t])
forall t. Expr t -> (Expr t, [Expr t])
go Expr t
e

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

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

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

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

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

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

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

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

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

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

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

isBangInteger :: [C.CoreAlt] -> Bool 
isBangInteger :: [CoreAlt] -> Bool
isBangInteger [(C.DataAlt DataCon
s, [Var]
_, CoreExpr
_), (C.DataAlt DataCon
jp,[Var]
_,CoreExpr
_), (C.DataAlt DataCon
jn,[Var]
_,CoreExpr
_)] 
  =  DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCon
s  Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Integer.Type.S#" 
  Bool -> Bool -> Bool
&& DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCon
jp Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Integer.Type.Jp#" 
  Bool -> Bool -> Bool
&& DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCon
jn Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"GHC.Integer.Type.Jn#"  
isBangInteger [CoreAlt]
_ = Bool
False 

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

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

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

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

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

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

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

instance Simplify C.CoreExpr where
  simplify :: CoreExpr -> CoreExpr
simplify e :: CoreExpr
e@(C.Var Var
_)
    = CoreExpr
e
  simplify e :: CoreExpr
e@(C.Lit Literal
_)
    = CoreExpr
e
  simplify (C.App CoreExpr
e (C.Type Type
_))
    = CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e
  simplify (C.App CoreExpr
e (C.Var Var
dict))  | Var -> Bool
isErasable Var
dict
    = CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e
  simplify (C.App (C.Lam Var
x CoreExpr
e) CoreExpr
_)   | Var -> Bool
isDead Var
x
    = CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e
  simplify (C.App CoreExpr
e1 CoreExpr
e2)
    = CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
C.App (CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e1) (CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e2)
  simplify (C.Lam Var
x CoreExpr
e) | Var -> Bool
isTyVar Var
x
    = CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e
  simplify (C.Lam Var
x CoreExpr
e) | Var -> Bool
isErasable Var
x
    = CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e
  simplify (C.Lam Var
x CoreExpr
e)
    = Var -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
C.Lam Var
x (CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e)
  simplify (C.Let (C.NonRec Var
x CoreExpr
_) CoreExpr
e) | Var -> Bool
isErasable Var
x
    = CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e
  simplify (C.Let (C.Rec [(Var, CoreExpr)]
xes) CoreExpr
e)    | ((Var, CoreExpr) -> Bool) -> [(Var, CoreExpr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Var -> Bool
isErasable (Var -> Bool)
-> ((Var, CoreExpr) -> Var) -> (Var, CoreExpr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, CoreExpr) -> Var
forall a b. (a, b) -> a
fst) [(Var, CoreExpr)]
xes
    = CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e
  simplify (C.Let Bind Var
xes CoreExpr
e)
    = Bind Var -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
C.Let (Bind Var -> Bind Var
forall a. Simplify a => a -> a
simplify Bind Var
xes) (CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e)
  simplify (C.Case CoreExpr
e Var
x Type
_t alts :: [CoreAlt]
alts@[(AltCon
_,[Var]
_,CoreExpr
ee),CoreAlt
_,CoreAlt
_]) | [CoreAlt] -> Bool
isBangInteger [CoreAlt]
alts
    = String -> CoreExpr -> CoreExpr
forall a. Show a => String -> a -> a
Misc.traceShow (String
"To simplify case") (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ 
       HashMap Var CoreExpr -> CoreExpr -> CoreExpr
forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub (Var -> CoreExpr -> HashMap Var CoreExpr
forall k v. Hashable k => k -> v -> HashMap k v
M.singleton Var
x (CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e)) (CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
ee)
  simplify (C.Case CoreExpr
e Var
x Type
t [CoreAlt]
alts)
    = CoreExpr -> Var -> Type -> [CoreAlt] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
C.Case (CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e) Var
x Type
t ((CoreAlt -> Bool) -> [CoreAlt] -> [CoreAlt]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (CoreAlt -> Bool) -> CoreAlt -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreAlt -> Bool
forall t t1 t2. (t, t1, Expr t2) -> Bool
isUndefined) (CoreAlt -> CoreAlt
forall a. Simplify a => a -> a
simplify (CoreAlt -> CoreAlt) -> [CoreAlt] -> [CoreAlt]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CoreAlt]
alts))
  simplify (C.Cast CoreExpr
e Coercion
c)
    = CoreExpr -> Coercion -> CoreExpr
forall b. Expr b -> Coercion -> Expr b
C.Cast (CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e) Coercion
c
  simplify (C.Tick Tickish Var
_ CoreExpr
e)
    = CoreExpr -> CoreExpr
forall a. Simplify a => a -> a
simplify CoreExpr
e
  simplify (C.Coercion Coercion
c)
    = Coercion -> CoreExpr
forall b. Coercion -> Expr b
C.Coercion Coercion
c
  simplify (C.Type Type
t)
    = Type -> CoreExpr
forall b. Type -> Expr b
C.Type Type
t

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

isUndefined :: (t, t1, C.Expr t2) -> Bool
isUndefined :: (t, t1, Expr t2) -> Bool
isUndefined (t
_, t1
_, Expr t2
e) = Expr t2 -> Bool
forall b. Expr b -> Bool
isUndefinedExpr Expr t2
e
  where
   -- auto generated undefined case: (\_ -> (patError @type "error message")) void
   isUndefinedExpr :: Expr b -> Bool
isUndefinedExpr (C.App (C.Var Var
x) Expr b
_) | (Var -> String
forall a. Show a => a -> String
show Var
x) String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
perrors = Bool
True
   isUndefinedExpr (C.Let Bind b
_ Expr b
e) = Expr b -> Bool
isUndefinedExpr Expr b
e
   -- otherwise
   isUndefinedExpr Expr b
_ = Bool
False

   perrors :: [String]
perrors = [String
"Control.Exception.Base.patError"]


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

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

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