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