{-# 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 (\x :: 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 _ (ConstB True) e :: Expr
e _     -> Expr -> Expr
bsimpl' Expr
e
      Ite _ (ConstB False) _ e :: Expr
e    -> Expr -> Expr
bsimpl' Expr
e
      Ite t :: Type
t c :: Expr
c e1 :: Expr
e1 e2 :: 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 _ Not (Op1 _ Not e :: Expr
e)     -> Expr -> Expr
bsimpl' Expr
e
      Op1 _ Not (ConstB True)     -> Bool -> Expr
ConstB Bool
False
      Op1 _ Not (ConstB False)    -> Bool -> Expr
ConstB Bool
True
      Op1 t :: Type
t o :: Op1
o e :: Expr
e                   -> Type -> Op1 -> Expr -> Expr
Op1 Type
t Op1
o (Expr -> Expr
bsimpl' Expr
e)

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

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

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

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

      FunApp t :: Type
t f :: String
f args :: [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)

      e :: Expr
e                           -> Expr
e