{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Safe #-}

-- | Simplify IL expressions by partly evaluating operations on booleans.
module Copilot.Theorem.IL.Transform ( bsimpl ) where

import Copilot.Theorem.IL.Spec

-- | Simplify IL expressions by partly evaluating operations on booleans,
-- eliminating some boolean literals.
--
-- For example, an if-then-else in which the condition is literally the
-- constant True or the constant False can be reduced to an operation without
-- choice in which the appropriate branch of the if-then-else is used instead.
bsimpl :: Expr -> Expr
bsimpl :: Expr -> Expr
bsimpl = (Expr -> Bool) -> (Expr -> Expr) -> Expr -> Expr
forall a. (a -> Bool) -> (a -> a) -> a -> a
until (\Expr
x -> Expr -> Expr
bsimpl' Expr
x Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
x) Expr -> Expr
bsimpl'
  where
    bsimpl' :: Expr -> Expr
bsimpl' = \case
      Ite Type
_ (ConstB Bool
True) Expr
e Expr
_     -> Expr -> Expr
bsimpl' Expr
e
      Ite Type
_ (ConstB Bool
False) Expr
_ Expr
e    -> Expr -> Expr
bsimpl' Expr
e
      Ite Type
t Expr
c Expr
e1 Expr
e2               -> Type -> Expr -> Expr -> Expr -> Expr
Ite Type
t (Expr -> Expr
bsimpl' Expr
c) (Expr -> Expr
bsimpl' Expr
e1) (Expr -> Expr
bsimpl' Expr
e2)

      Op1 Type
_ Op1
Not (Op1 Type
_ Op1
Not Expr
e)     -> Expr -> Expr
bsimpl' Expr
e
      Op1 Type
_ Op1
Not (ConstB Bool
True)     -> Bool -> Expr
ConstB Bool
False
      Op1 Type
_ Op1
Not (ConstB Bool
False)    -> Bool -> Expr
ConstB Bool
True
      Op1 Type
t Op1
o Expr
e                   -> Type -> Op1 -> Expr -> Expr
Op1 Type
t Op1
o (Expr -> Expr
bsimpl' Expr
e)

      Op2 Type
_ Op2
Or Expr
e (ConstB Bool
False)   -> Expr -> Expr
bsimpl' Expr
e
      Op2 Type
_ Op2
Or (ConstB Bool
False) Expr
e   -> Expr -> Expr
bsimpl' Expr
e
      Op2 Type
_ Op2
Or Expr
_ (ConstB Bool
True)    -> Bool -> Expr
ConstB Bool
True
      Op2 Type
_ Op2
Or (ConstB Bool
True) Expr
_    -> Bool -> Expr
ConstB Bool
True

      Op2 Type
_ Op2
And Expr
_ (ConstB Bool
False)  -> Bool -> Expr
ConstB Bool
False
      Op2 Type
_ Op2
And (ConstB Bool
False) Expr
_  -> Bool -> Expr
ConstB Bool
False
      Op2 Type
_ Op2
And Expr
e (ConstB Bool
True)   -> Expr -> Expr
bsimpl' Expr
e
      Op2 Type
_ Op2
And (ConstB Bool
True) Expr
e   -> Expr -> Expr
bsimpl' Expr
e

      Op2 Type
_ Op2
Eq Expr
e (ConstB Bool
False)   -> Expr -> Expr
bsimpl' (Type -> Op1 -> Expr -> Expr
Op1 Type
Bool Op1
Not Expr
e)
      Op2 Type
_ Op2
Eq (ConstB Bool
False) Expr
e   -> Expr -> Expr
bsimpl' (Type -> Op1 -> Expr -> Expr
Op1 Type
Bool Op1
Not Expr
e)
      Op2 Type
_ Op2
Eq Expr
e (ConstB Bool
True)    -> Expr -> Expr
bsimpl' Expr
e
      Op2 Type
_ Op2
Eq (ConstB Bool
True) Expr
e    -> Expr -> Expr
bsimpl' Expr
e

      Op2 Type
t Op2
o Expr
e1 Expr
e2               -> Type -> Op2 -> Expr -> Expr -> Expr
Op2 Type
t Op2
o (Expr -> Expr
bsimpl' Expr
e1) (Expr -> Expr
bsimpl' Expr
e2)

      FunApp Type
t String
f [Expr]
args             -> Type -> String -> [Expr] -> Expr
FunApp Type
t String
f ((Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
bsimpl' [Expr]
args)

      Expr
e                           -> Expr
e