{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Safe #-}
module Copilot.Theorem.IL.Transform ( bsimpl ) where
import Copilot.Theorem.IL.Spec
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