{-
Author: George Karachalias <george.karachalias@cs.kuleuven.be>

The term equality oracle. The main export of the module is function `tmOracle'.
-}

{-# LANGUAGE CPP, MultiWayIf #-}

module TmOracle (

        -- re-exported from PmExpr
        PmExpr(..), PmLit(..), SimpleEq, ComplexEq, PmVarEnv, falsePmExpr,
        eqPmLit, filterComplex, isNotPmExprOther, runPmPprM, lhsExprToPmExpr,
        hsExprToPmExpr, pprPmExprWithParens,

        -- the term oracle
        tmOracle, TmState, initialTmState, solveOneEq, extendSubst, canDiverge,

        -- misc.
        toComplex, exprDeepLookup, pmLitType, flattenPmVarEnv
    ) where

#include "HsVersions.h"

import GhcPrelude

import PmExpr

import Id
import Name
import Type
import HsLit
import TcHsSyn
import MonadUtils
import Util

import NameEnv

{-
%************************************************************************
%*                                                                      *
                      The term equality oracle
%*                                                                      *
%************************************************************************
-}

-- | The type of substitutions.
type PmVarEnv = NameEnv PmExpr

-- | The environment of the oracle contains
--     1. A Bool (are there any constraints we cannot handle? (PmExprOther)).
--     2. A substitution we extend with every step and return as a result.
type TmOracleEnv = (Bool, PmVarEnv)

-- | Check whether a constraint (x ~ BOT) can succeed,
-- given the resulting state of the term oracle.
canDiverge :: Name -> TmState -> Bool
canDiverge :: Name -> TmState -> Bool
canDiverge x :: Name
x (standby :: [ComplexEq]
standby, (_unhandled :: Bool
_unhandled, env :: PmVarEnv
env))
  -- If the variable seems not evaluated, there is a possibility for
  -- constraint x ~ BOT to be satisfiable.
  | PmExprVar y :: Name
y <- PmVarEnv -> Name -> PmExpr
varDeepLookup PmVarEnv
env Name
x -- seems not forced
  -- If it is involved (directly or indirectly) in any equality in the
  -- worklist, we can assume that it is already indirectly evaluated,
  -- as a side-effect of equality checking. If not, then we can assume
  -- that the constraint is satisfiable.
  = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (ComplexEq -> Bool) -> [ComplexEq] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> ComplexEq -> Bool
isForcedByEq Name
x) [ComplexEq]
standby Bool -> Bool -> Bool
|| (ComplexEq -> Bool) -> [ComplexEq] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> ComplexEq -> Bool
isForcedByEq Name
y) [ComplexEq]
standby
  -- Variable x is already in WHNF so the constraint is non-satisfiable
  | Bool
otherwise = Bool
False

  where
    isForcedByEq :: Name -> ComplexEq -> Bool
    isForcedByEq :: Name -> ComplexEq -> Bool
isForcedByEq y :: Name
y (e1 :: PmExpr
e1, e2 :: PmExpr
e2) = Name -> PmExpr -> Bool
varIn Name
y PmExpr
e1 Bool -> Bool -> Bool
|| Name -> PmExpr -> Bool
varIn Name
y PmExpr
e2

-- | Check whether a variable is in the free variables of an expression
varIn :: Name -> PmExpr -> Bool
varIn :: Name -> PmExpr -> Bool
varIn x :: Name
x e :: PmExpr
e = case PmExpr
e of
  PmExprVar y :: Name
y    -> Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y
  PmExprCon _ es :: [PmExpr]
es -> (PmExpr -> Bool) -> [PmExpr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name
x Name -> PmExpr -> Bool
`varIn`) [PmExpr]
es
  PmExprLit _    -> Bool
False
  PmExprEq e1 :: PmExpr
e1 e2 :: PmExpr
e2 -> (Name
x Name -> PmExpr -> Bool
`varIn` PmExpr
e1) Bool -> Bool -> Bool
|| (Name
x Name -> PmExpr -> Bool
`varIn` PmExpr
e2)
  PmExprOther _  -> Bool
False

-- | Flatten the DAG (Could be improved in terms of performance.).
flattenPmVarEnv :: PmVarEnv -> PmVarEnv
flattenPmVarEnv :: PmVarEnv -> PmVarEnv
flattenPmVarEnv env :: PmVarEnv
env = (PmExpr -> PmExpr) -> PmVarEnv -> PmVarEnv
forall elt1 elt2. (elt1 -> elt2) -> NameEnv elt1 -> NameEnv elt2
mapNameEnv (PmVarEnv -> PmExpr -> PmExpr
exprDeepLookup PmVarEnv
env) PmVarEnv
env

-- | The state of the term oracle (includes complex constraints that cannot
-- progress unless we get more information).
type TmState = ([ComplexEq], TmOracleEnv)

-- | Initial state of the oracle.
initialTmState :: TmState
initialTmState :: TmState
initialTmState = ([], (Bool
False, PmVarEnv
forall a. NameEnv a
emptyNameEnv))

-- | Solve a complex equality (top-level).
solveOneEq :: TmState -> ComplexEq -> Maybe TmState
solveOneEq :: TmState -> ComplexEq -> Maybe TmState
solveOneEq solver_env :: TmState
solver_env@(_,(_,env :: PmVarEnv
env)) complex :: ComplexEq
complex
  = TmState -> ComplexEq -> Maybe TmState
solveComplexEq TmState
solver_env -- do the actual *merging* with existing state
  (ComplexEq -> Maybe TmState) -> ComplexEq -> Maybe TmState
forall a b. (a -> b) -> a -> b
$ ComplexEq -> ComplexEq
simplifyComplexEq               -- simplify as much as you can
  (ComplexEq -> ComplexEq) -> ComplexEq -> ComplexEq
forall a b. (a -> b) -> a -> b
$ PmVarEnv -> ComplexEq -> ComplexEq
applySubstComplexEq PmVarEnv
env ComplexEq
complex -- replace everything we already know

-- | Solve a complex equality.
-- Nothing => definitely unsatisfiable
-- Just tms => I have added the complex equality and added
--             it to the tmstate; the result may or may not be
--             satisfiable
solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
solveComplexEq solver_state :: TmState
solver_state@(standby :: [ComplexEq]
standby, (unhandled :: Bool
unhandled, env :: PmVarEnv
env)) eq :: ComplexEq
eq@(e1 :: PmExpr
e1, e2 :: PmExpr
e2) = case ComplexEq
eq of
  -- We cannot do a thing about these cases
  (PmExprOther _,_)            -> TmState -> Maybe TmState
forall a. a -> Maybe a
Just ([ComplexEq]
standby, (Bool
True, PmVarEnv
env))
  (_,PmExprOther _)            -> TmState -> Maybe TmState
forall a. a -> Maybe a
Just ([ComplexEq]
standby, (Bool
True, PmVarEnv
env))

  (PmExprLit l1 :: PmLit
l1, PmExprLit l2 :: PmLit
l2) -> case PmLit -> PmLit -> Bool
eqPmLit PmLit
l1 PmLit
l2 of
    -- See Note [Undecidable Equality for Overloaded Literals]
    True  -> TmState -> Maybe TmState
forall a. a -> Maybe a
Just TmState
solver_state
    False -> Maybe TmState
forall a. Maybe a
Nothing

  (PmExprCon c1 :: ConLike
c1 ts1 :: [PmExpr]
ts1, PmExprCon c2 :: ConLike
c2 ts2 :: [PmExpr]
ts2)
    | ConLike
c1 ConLike -> ConLike -> Bool
forall a. Eq a => a -> a -> Bool
== ConLike
c2  -> (TmState -> ComplexEq -> Maybe TmState)
-> TmState -> [ComplexEq] -> Maybe TmState
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m a) -> a -> [b] -> m a
foldlM TmState -> ComplexEq -> Maybe TmState
solveComplexEq TmState
solver_state ([PmExpr] -> [PmExpr] -> [ComplexEq]
forall a b. [a] -> [b] -> [(a, b)]
zip [PmExpr]
ts1 [PmExpr]
ts2)
    | Bool
otherwise -> Maybe TmState
forall a. Maybe a
Nothing
  (PmExprCon _ [], PmExprEq t1 :: PmExpr
t1 t2 :: PmExpr
t2)
    | PmExpr -> Bool
isTruePmExpr PmExpr
e1  -> TmState -> ComplexEq -> Maybe TmState
solveComplexEq TmState
solver_state (PmExpr
t1, PmExpr
t2)
    | PmExpr -> Bool
isFalsePmExpr PmExpr
e1 -> TmState -> Maybe TmState
forall a. a -> Maybe a
Just (ComplexEq
eqComplexEq -> [ComplexEq] -> [ComplexEq]
forall a. a -> [a] -> [a]
:[ComplexEq]
standby, (Bool
unhandled, PmVarEnv
env))
  (PmExprEq t1 :: PmExpr
t1 t2 :: PmExpr
t2, PmExprCon _ [])
    | PmExpr -> Bool
isTruePmExpr PmExpr
e2   -> TmState -> ComplexEq -> Maybe TmState
solveComplexEq TmState
solver_state (PmExpr
t1, PmExpr
t2)
    | PmExpr -> Bool
isFalsePmExpr PmExpr
e2  -> TmState -> Maybe TmState
forall a. a -> Maybe a
Just (ComplexEq
eqComplexEq -> [ComplexEq] -> [ComplexEq]
forall a. a -> [a] -> [a]
:[ComplexEq]
standby, (Bool
unhandled, PmVarEnv
env))

  (PmExprVar x :: Name
x, PmExprVar y :: Name
y)
    | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y    -> TmState -> Maybe TmState
forall a. a -> Maybe a
Just TmState
solver_state
    | Bool
otherwise -> Name -> PmExpr -> TmState -> Maybe TmState
extendSubstAndSolve Name
x PmExpr
e2 TmState
solver_state

  (PmExprVar x :: Name
x, _) -> Name -> PmExpr -> TmState -> Maybe TmState
extendSubstAndSolve Name
x PmExpr
e2 TmState
solver_state
  (_, PmExprVar x :: Name
x) -> Name -> PmExpr -> TmState -> Maybe TmState
extendSubstAndSolve Name
x PmExpr
e1 TmState
solver_state

  (PmExprEq _ _, PmExprEq _ _) -> TmState -> Maybe TmState
forall a. a -> Maybe a
Just (ComplexEq
eqComplexEq -> [ComplexEq] -> [ComplexEq]
forall a. a -> [a] -> [a]
:[ComplexEq]
standby, (Bool
unhandled, PmVarEnv
env))

  _ -> TmState -> Maybe TmState
forall a. a -> Maybe a
Just ([ComplexEq]
standby, (Bool
True, PmVarEnv
env)) -- I HATE CATCH-ALLS

-- | Extend the substitution and solve the (possibly updated) constraints.
extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState
extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState
extendSubstAndSolve x :: Name
x e :: PmExpr
e (standby :: [ComplexEq]
standby, (unhandled :: Bool
unhandled, env :: PmVarEnv
env))
  = (TmState -> ComplexEq -> Maybe TmState)
-> TmState -> [ComplexEq] -> Maybe TmState
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m a) -> a -> [b] -> m a
foldlM TmState -> ComplexEq -> Maybe TmState
solveComplexEq TmState
new_incr_state ((ComplexEq -> ComplexEq) -> [ComplexEq] -> [ComplexEq]
forall a b. (a -> b) -> [a] -> [b]
map ComplexEq -> ComplexEq
simplifyComplexEq [ComplexEq]
changed)
  where
    -- Apply the substitution to the worklist and partition them to the ones
    -- that had some progress and the rest. Then, recurse over the ones that
    -- had some progress. Careful about performance:
    -- See Note [Representation of Term Equalities] in deSugar/Check.hs
    (changed :: [ComplexEq]
changed, unchanged :: [ComplexEq]
unchanged) = (ComplexEq -> Either ComplexEq ComplexEq)
-> [ComplexEq] -> ([ComplexEq], [ComplexEq])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith (Name -> PmExpr -> ComplexEq -> Either ComplexEq ComplexEq
substComplexEq Name
x PmExpr
e) [ComplexEq]
standby
    new_incr_state :: TmState
new_incr_state       = ([ComplexEq]
unchanged, (Bool
unhandled, PmVarEnv -> Name -> PmExpr -> PmVarEnv
forall a. NameEnv a -> Name -> a -> NameEnv a
extendNameEnv PmVarEnv
env Name
x PmExpr
e))

-- | When we know that a variable is fresh, we do not actually have to
-- check whether anything changes, we know that nothing does. Hence,
-- `extendSubst` simply extends the substitution, unlike what
-- `extendSubstAndSolve` does.
extendSubst :: Id -> PmExpr -> TmState -> TmState
extendSubst :: Id -> PmExpr -> TmState -> TmState
extendSubst y :: Id
y e :: PmExpr
e (standby :: [ComplexEq]
standby, (unhandled :: Bool
unhandled, env :: PmVarEnv
env))
  | PmExpr -> Bool
isNotPmExprOther PmExpr
simpl_e
  = ([ComplexEq]
standby, (Bool
unhandled, PmVarEnv -> Name -> PmExpr -> PmVarEnv
forall a. NameEnv a -> Name -> a -> NameEnv a
extendNameEnv PmVarEnv
env Name
x PmExpr
simpl_e))
  | Bool
otherwise = ([ComplexEq]
standby, (Bool
True, PmVarEnv
env))
  where
    x :: Name
x = Id -> Name
idName Id
y
    simpl_e :: PmExpr
simpl_e = (PmExpr, Bool) -> PmExpr
forall a b. (a, b) -> a
fst ((PmExpr, Bool) -> PmExpr) -> (PmExpr, Bool) -> PmExpr
forall a b. (a -> b) -> a -> b
$ PmExpr -> (PmExpr, Bool)
simplifyPmExpr (PmExpr -> (PmExpr, Bool)) -> PmExpr -> (PmExpr, Bool)
forall a b. (a -> b) -> a -> b
$ PmVarEnv -> PmExpr -> PmExpr
exprDeepLookup PmVarEnv
env PmExpr
e

-- | Simplify a complex equality.
simplifyComplexEq :: ComplexEq -> ComplexEq
simplifyComplexEq :: ComplexEq -> ComplexEq
simplifyComplexEq (e1 :: PmExpr
e1, e2 :: PmExpr
e2) = ((PmExpr, Bool) -> PmExpr
forall a b. (a, b) -> a
fst ((PmExpr, Bool) -> PmExpr) -> (PmExpr, Bool) -> PmExpr
forall a b. (a -> b) -> a -> b
$ PmExpr -> (PmExpr, Bool)
simplifyPmExpr PmExpr
e1, (PmExpr, Bool) -> PmExpr
forall a b. (a, b) -> a
fst ((PmExpr, Bool) -> PmExpr) -> (PmExpr, Bool) -> PmExpr
forall a b. (a -> b) -> a -> b
$ PmExpr -> (PmExpr, Bool)
simplifyPmExpr PmExpr
e2)

-- | Simplify an expression. The boolean indicates if there has been any
-- simplification or if the operation was a no-op.
simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
-- See Note [Deep equalities]
simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
simplifyPmExpr e :: PmExpr
e = case PmExpr
e of
  PmExprCon c :: ConLike
c ts :: [PmExpr]
ts -> case (PmExpr -> (PmExpr, Bool)) -> [PmExpr] -> ([PmExpr], [Bool])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
mapAndUnzip PmExpr -> (PmExpr, Bool)
simplifyPmExpr [PmExpr]
ts of
                      (ts' :: [PmExpr]
ts', bs :: [Bool]
bs) -> (ConLike -> [PmExpr] -> PmExpr
PmExprCon ConLike
c [PmExpr]
ts', [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
bs)
  PmExprEq t1 :: PmExpr
t1 t2 :: PmExpr
t2 -> PmExpr -> PmExpr -> (PmExpr, Bool)
simplifyEqExpr PmExpr
t1 PmExpr
t2
  _other_expr :: PmExpr
_other_expr    -> (PmExpr
e, Bool
False) -- the others are terminals

-- | Simplify an equality expression. The equality is given in parts.
simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
-- See Note [Deep equalities]
simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
simplifyEqExpr e1 :: PmExpr
e1 e2 :: PmExpr
e2 = case (PmExpr
e1, PmExpr
e2) of
  -- Varables
  (PmExprVar x :: Name
x, PmExprVar y :: Name
y)
    | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y -> (PmExpr
truePmExpr, Bool
True)

  -- Literals
  (PmExprLit l1 :: PmLit
l1, PmExprLit l2 :: PmLit
l2) -> case PmLit -> PmLit -> Bool
eqPmLit PmLit
l1 PmLit
l2 of
    -- See Note [Undecidable Equality for Overloaded Literals]
    True  -> (PmExpr
truePmExpr,  Bool
True)
    False -> (PmExpr
falsePmExpr, Bool
True)

  -- Can potentially be simplified
  (PmExprEq {}, _) -> case (PmExpr -> (PmExpr, Bool)
simplifyPmExpr PmExpr
e1, PmExpr -> (PmExpr, Bool)
simplifyPmExpr PmExpr
e2) of
    ((e1' :: PmExpr
e1', True ), (e2' :: PmExpr
e2', _    )) -> PmExpr -> PmExpr -> (PmExpr, Bool)
simplifyEqExpr PmExpr
e1' PmExpr
e2'
    ((e1' :: PmExpr
e1', _    ), (e2' :: PmExpr
e2', True )) -> PmExpr -> PmExpr -> (PmExpr, Bool)
simplifyEqExpr PmExpr
e1' PmExpr
e2'
    ((e1' :: PmExpr
e1', False), (e2' :: PmExpr
e2', False)) -> (PmExpr -> PmExpr -> PmExpr
PmExprEq PmExpr
e1' PmExpr
e2', Bool
False) -- cannot progress
  (_, PmExprEq {}) -> case (PmExpr -> (PmExpr, Bool)
simplifyPmExpr PmExpr
e1, PmExpr -> (PmExpr, Bool)
simplifyPmExpr PmExpr
e2) of
    ((e1' :: PmExpr
e1', True ), (e2' :: PmExpr
e2', _    )) -> PmExpr -> PmExpr -> (PmExpr, Bool)
simplifyEqExpr PmExpr
e1' PmExpr
e2'
    ((e1' :: PmExpr
e1', _    ), (e2' :: PmExpr
e2', True )) -> PmExpr -> PmExpr -> (PmExpr, Bool)
simplifyEqExpr PmExpr
e1' PmExpr
e2'
    ((e1' :: PmExpr
e1', False), (e2' :: PmExpr
e2', False)) -> (PmExpr -> PmExpr -> PmExpr
PmExprEq PmExpr
e1' PmExpr
e2', Bool
False) -- cannot progress

  -- Constructors
  (PmExprCon c1 :: ConLike
c1 ts1 :: [PmExpr]
ts1, PmExprCon c2 :: ConLike
c2 ts2 :: [PmExpr]
ts2)
    | ConLike
c1 ConLike -> ConLike -> Bool
forall a. Eq a => a -> a -> Bool
== ConLike
c2 ->
        let (ts1' :: [PmExpr]
ts1', bs1 :: [Bool]
bs1) = (PmExpr -> (PmExpr, Bool)) -> [PmExpr] -> ([PmExpr], [Bool])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
mapAndUnzip PmExpr -> (PmExpr, Bool)
simplifyPmExpr [PmExpr]
ts1
            (ts2' :: [PmExpr]
ts2', bs2 :: [Bool]
bs2) = (PmExpr -> (PmExpr, Bool)) -> [PmExpr] -> ([PmExpr], [Bool])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
mapAndUnzip PmExpr -> (PmExpr, Bool)
simplifyPmExpr [PmExpr]
ts2
            (tss :: [PmExpr]
tss, _bss :: [Bool]
_bss) = (PmExpr -> PmExpr -> (PmExpr, Bool))
-> [PmExpr] -> [PmExpr] -> ([PmExpr], [Bool])
forall a b c d. (a -> b -> (c, d)) -> [a] -> [b] -> ([c], [d])
zipWithAndUnzip PmExpr -> PmExpr -> (PmExpr, Bool)
simplifyEqExpr [PmExpr]
ts1' [PmExpr]
ts2'
            worst_case :: PmExpr
worst_case  = PmExpr -> PmExpr -> PmExpr
PmExprEq (ConLike -> [PmExpr] -> PmExpr
PmExprCon ConLike
c1 [PmExpr]
ts1') (ConLike -> [PmExpr] -> PmExpr
PmExprCon ConLike
c2 [PmExpr]
ts2')
        in  if | Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
bs1 Bool -> Bool -> Bool
|| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
bs2) -> (PmExpr
worst_case, Bool
False) -- no progress
               | (PmExpr -> Bool) -> [PmExpr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PmExpr -> Bool
isTruePmExpr  [PmExpr]
tss  -> (PmExpr
truePmExpr, Bool
True)
               | (PmExpr -> Bool) -> [PmExpr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any PmExpr -> Bool
isFalsePmExpr [PmExpr]
tss  -> (PmExpr
falsePmExpr, Bool
True)
               | Bool
otherwise              -> (PmExpr
worst_case, Bool
False)
    | Bool
otherwise -> (PmExpr
falsePmExpr, Bool
True)

  -- We cannot do anything about the rest..
  _other_equality :: ComplexEq
_other_equality -> (PmExpr
original, Bool
False)

  where
    original :: PmExpr
original = PmExpr -> PmExpr -> PmExpr
PmExprEq PmExpr
e1 PmExpr
e2 -- reconstruct equality

-- | Apply an (un-flattened) substitution to a simple equality.
applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
applySubstComplexEq env :: PmVarEnv
env (e1 :: PmExpr
e1,e2 :: PmExpr
e2) = (PmVarEnv -> PmExpr -> PmExpr
exprDeepLookup PmVarEnv
env PmExpr
e1, PmVarEnv -> PmExpr -> PmExpr
exprDeepLookup PmVarEnv
env PmExpr
e2)

-- | Apply an (un-flattened) substitution to a variable.
varDeepLookup :: PmVarEnv -> Name -> PmExpr
varDeepLookup :: PmVarEnv -> Name -> PmExpr
varDeepLookup env :: PmVarEnv
env x :: Name
x
  | Just e :: PmExpr
e <- PmVarEnv -> Name -> Maybe PmExpr
forall a. NameEnv a -> Name -> Maybe a
lookupNameEnv PmVarEnv
env Name
x = PmVarEnv -> PmExpr -> PmExpr
exprDeepLookup PmVarEnv
env PmExpr
e -- go deeper
  | Bool
otherwise                  = Name -> PmExpr
PmExprVar Name
x          -- terminal
{-# INLINE varDeepLookup #-}

-- | Apply an (un-flattened) substitution to an expression.
exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
exprDeepLookup env :: PmVarEnv
env (PmExprVar x :: Name
x)    = PmVarEnv -> Name -> PmExpr
varDeepLookup PmVarEnv
env Name
x
exprDeepLookup env :: PmVarEnv
env (PmExprCon c :: ConLike
c es :: [PmExpr]
es) = ConLike -> [PmExpr] -> PmExpr
PmExprCon ConLike
c ((PmExpr -> PmExpr) -> [PmExpr] -> [PmExpr]
forall a b. (a -> b) -> [a] -> [b]
map (PmVarEnv -> PmExpr -> PmExpr
exprDeepLookup PmVarEnv
env) [PmExpr]
es)
exprDeepLookup env :: PmVarEnv
env (PmExprEq e1 :: PmExpr
e1 e2 :: PmExpr
e2) = PmExpr -> PmExpr -> PmExpr
PmExprEq (PmVarEnv -> PmExpr -> PmExpr
exprDeepLookup PmVarEnv
env PmExpr
e1)
                                               (PmVarEnv -> PmExpr -> PmExpr
exprDeepLookup PmVarEnv
env PmExpr
e2)
exprDeepLookup _   other_expr :: PmExpr
other_expr       = PmExpr
other_expr -- PmExprLit, PmExprOther

-- | External interface to the term oracle.
tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
tmOracle tm_state :: TmState
tm_state eqs :: [ComplexEq]
eqs = (TmState -> ComplexEq -> Maybe TmState)
-> TmState -> [ComplexEq] -> Maybe TmState
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m a) -> a -> [b] -> m a
foldlM TmState -> ComplexEq -> Maybe TmState
solveOneEq TmState
tm_state [ComplexEq]
eqs

-- | Type of a PmLit
pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :(
pmLitType :: PmLit -> Type
pmLitType (PmSLit   lit :: HsLit GhcTc
lit) = HsLit GhcTc -> Type
forall (p :: Pass). HsLit (GhcPass p) -> Type
hsLitType   HsLit GhcTc
lit
pmLitType (PmOLit _ lit :: HsOverLit GhcTc
lit) = HsOverLit GhcTc -> Type
overLitType HsOverLit GhcTc
lit

{- Note [Deep equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~
Solving nested equalities is the most difficult part. The general strategy
is the following:

  * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
    (e1 ~ e2) and then treated recursively.

  * Equalities of the form (False ~ (e1 ~ e2)) cannot be analyzed unless
    we know more about the inner equality (e1 ~ e2). That's exactly what
    `simplifyEqExpr' tries to do: It takes e1 and e2 and either returns
    truePmExpr, falsePmExpr or (e1' ~ e2') in case it is uncertain. Note
    that it is not e but rather e', since it may perform some
    simplifications deeper.
-}