content: {-# 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 = until (\x -> bsimpl' x == x) bsimpl'
    where
      bsimpl' = \case
        Ite _ (ConstB True) e _     -> bsimpl' e
        Ite _ (ConstB False) _ e    -> bsimpl' e
        Ite t c e1 e2               -> Ite t (bsimpl' c) (bsimpl' e1) (bsimpl' e2)
  
        Op1 _ Not (Op1 _ Not e)     -> bsimpl' e
        Op1 _ Not (ConstB True)     -> ConstB False
        Op1 _ Not (ConstB False)    -> ConstB True
        Op1 t o e                   -> Op1 t o (bsimpl' e)
  
        Op2 _ Or e (ConstB False)   -> bsimpl' e
        Op2 _ Or (ConstB False) e   -> bsimpl' e
        Op2 _ Or _ (ConstB True)    -> ConstB True
        Op2 _ Or (ConstB True) _    -> ConstB True
  
        Op2 _ And _ (ConstB False)  -> ConstB False
        Op2 _ And (ConstB False) _  -> ConstB False
        Op2 _ And e (ConstB True)   -> bsimpl' e
        Op2 _ And (ConstB True) e   -> bsimpl' e
  
        Op2 _ Eq e (ConstB False)   -> bsimpl' (Op1 Bool Not e)
        Op2 _ Eq (ConstB False) e   -> bsimpl' (Op1 Bool Not e)
        Op2 _ Eq e (ConstB True)    -> bsimpl' e
        Op2 _ Eq (ConstB True) e    -> bsimpl' e
  
        Op2 t o e1 e2               -> Op2 t o (bsimpl' e1) (bsimpl' e2)
  
        FunApp t f args             -> FunApp t f (map bsimpl' args)
  
        e                           -> e
  