    {-# 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