module PropaFP.Eliminator where
import MixedTypesNumPrelude
import qualified Prelude as P
import Data.List
import PropaFP.Expression
minMaxAbsEliminatorF :: F -> F
minMaxAbsEliminatorF :: F -> F
minMaxAbsEliminatorF F
f' = F -> F
aux F
f'
where
aux :: F -> F
aux :: F -> F
aux F
fToElim =
case F
fToElim of
FConn Conn
conn F
f1 F
f2 -> Conn -> F -> F -> F
FConn Conn
conn (F -> F
aux F
f1) (F -> F
aux F
f2)
FComp Comp
comp E
e1 E
e2 ->
let
qualifiedE1s :: [([ESafe], ESafe)]
qualifiedE1s = ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (ESafe -> [([ESafe], ESafe)]) -> ESafe -> [([ESafe], ESafe)]
forall a b. (a -> b) -> a -> b
$ E -> ESafe
ENonStrict E
e1
qualifiedE2s :: [([ESafe], ESafe)]
qualifiedE2s = ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (ESafe -> [([ESafe], ESafe)]) -> ESafe -> [([ESafe], ESafe)]
forall a b. (a -> b) -> a -> b
$ E -> ESafe
ENonStrict E
e2
eListToConjunction :: [ESafe] -> F
eListToConjunction [] = [Char] -> F
forall a. HasCallStack => [Char] -> a
error [Char]
"undefined"
eListToConjunction [ENonStrict E
e] = Comp -> E -> E -> F
FComp Comp
Ge E
e (Rational -> E
Lit Rational
0.0)
eListToConjunction [EStrict E
e] = Comp -> E -> E -> F
FComp Comp
Gt E
e (Rational -> E
Lit Rational
0.0)
eListToConjunction (ESafe
e : [ESafe]
es) = Conn -> F -> F -> F
FConn Conn
And ([ESafe] -> F
eListToConjunction [ESafe
e]) ([ESafe] -> F
eListToConjunction [ESafe]
es)
fListToConjunction :: [F] -> F
fListToConjunction [] = [Char] -> F
forall a. HasCallStack => [Char] -> a
error [Char]
"undefined"
fListToConjunction [F
f] = F
f
fListToConjunction (F
f : [F]
fs) = Conn -> F -> F -> F
FConn Conn
And F
f ([F] -> F
fListToConjunction [F]
fs)
build :: ([ESafe], ESafe) -> [([ESafe], ESafe)] -> F
build :: ([ESafe], ESafe) -> [([ESafe], ESafe)] -> F
build ([ESafe], ESafe)
_ [] = [Char] -> F
forall a. HasCallStack => [Char] -> a
error [Char]
"Empty qualified list given in minMaxAbsEliminator"
build e1Q :: ([ESafe], ESafe)
e1Q@([ESafe]
e1C, ESafe
e1G) [([ESafe]
e2C, ESafe
e2G)] =
let
combinedL :: [ESafe]
combinedL = [ESafe]
e1C [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
e2C
combinedF :: F
combinedF = [ESafe] -> F
eListToConjunction ([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub [ESafe]
combinedL)
combinedG :: F
combinedG = Comp -> E -> E -> F
FComp Comp
comp (ESafe -> E
extractSafeE ESafe
e1G) (ESafe -> E
extractSafeE ESafe
e2G)
combinedQ :: F
combinedQ = Conn -> F -> F -> F
FConn Conn
Impl F
combinedF F
combinedG
in
if [ESafe] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ESafe]
combinedL
then F
combinedG
else F
combinedQ
build e1Q :: ([ESafe], ESafe)
e1Q@([ESafe]
e1C, ESafe
e1G) (([ESafe]
e2C, ESafe
e2G) : [([ESafe], ESafe)]
e2Qs) =
let
combinedL :: [ESafe]
combinedL = [ESafe]
e1C [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
e2C
combinedF :: F
combinedF = [ESafe] -> F
eListToConjunction ([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub [ESafe]
combinedL)
combinedG :: F
combinedG = Comp -> E -> E -> F
FComp Comp
comp (ESafe -> E
extractSafeE ESafe
e1G) (ESafe -> E
extractSafeE ESafe
e2G)
combinedQ :: F
combinedQ = Conn -> F -> F -> F
FConn Conn
Impl F
combinedF F
combinedG
in
if [ESafe] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ESafe]
combinedL
then F
combinedG
else Conn -> F -> F -> F
FConn Conn
And F
combinedQ (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ ([ESafe], ESafe) -> [([ESafe], ESafe)] -> F
build ([ESafe], ESafe)
e1Q [([ESafe], ESafe)]
e2Qs
combinedQualifiedEsAsF :: F
combinedQualifiedEsAsF = [F] -> F
fListToConjunction ([F] -> F) -> [F] -> F
forall a b. (a -> b) -> a -> b
$ (([ESafe], ESafe) -> F) -> [([ESafe], ESafe)] -> [F]
forall a b. (a -> b) -> [a] -> [b]
map (([ESafe], ESafe) -> [([ESafe], ESafe)] -> F
`build` [([ESafe], ESafe)]
qualifiedE2s) [([ESafe], ESafe)]
qualifiedE1s
in
F
combinedQualifiedEsAsF
FNot F
f -> F -> F
FNot (F -> F
aux F
f)
F
FTrue -> F
FTrue
F
FFalse -> F
FFalse
minMaxAbsEliminator :: ESafe -> [([ESafe],ESafe)]
minMaxAbsEliminator :: ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (ENonStrict (EBinOp BinOp
op E
e1 E
e2)) =
case BinOp
op of
BinOp
Min ->
[[([ESafe], ESafe)]] -> [([ESafe], ESafe)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[
[
([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub (([ESafe]
p1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
p2) [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub (ESafe -> E
extractSafeE ESafe
e2') (ESafe -> E
extractSafeE ESafe
e1'))]), ESafe
e1'),
([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub (([ESafe]
p2 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
p1) [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub (ESafe -> E
extractSafeE ESafe
e1') (ESafe -> E
extractSafeE ESafe
e2'))]), ESafe
e2')
]
|
([ESafe]
p1, ESafe
e1') <- [([ESafe], ESafe)]
branch1, ([ESafe]
p2, ESafe
e2') <- [([ESafe], ESafe)]
branch2
]
BinOp
Max ->
[[([ESafe], ESafe)]] -> [([ESafe], ESafe)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[
[
([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub (([ESafe]
p1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
p2) [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub (ESafe -> E
extractSafeE ESafe
e1') (ESafe -> E
extractSafeE ESafe
e2'))]), ESafe
e1'),
([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub (([ESafe]
p2 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
p1) [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub (ESafe -> E
extractSafeE ESafe
e2') (ESafe -> E
extractSafeE ESafe
e1'))]), ESafe
e2')
]
|
([ESafe]
p1, ESafe
e1') <- [([ESafe], ESafe)]
branch1, ([ESafe]
p2, ESafe
e2') <- [([ESafe], ESafe)]
branch2
]
BinOp
op' ->
[([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub ([ESafe]
p1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
p2), E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
op' (ESafe -> E
extractSafeE ESafe
e1') (ESafe -> E
extractSafeE ESafe
e2'))) | ([ESafe]
p1, ESafe
e1') <- [([ESafe], ESafe)]
branch1, ([ESafe]
p2, ESafe
e2') <- [([ESafe], ESafe)]
branch2]
where
branch1 :: [([ESafe], ESafe)]
branch1 = ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
ENonStrict E
e1)
branch2 :: [([ESafe], ESafe)]
branch2 = ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
ENonStrict E
e2)
minMaxAbsEliminator (ENonStrict (EUnOp UnOp
op E
e)) =
case UnOp
op of
UnOp
Abs ->
ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Max E
e (UnOp -> E -> E
EUnOp UnOp
Negate E
e)))
UnOp
op' ->
[([ESafe]
p, E -> ESafe
ENonStrict (UnOp -> E -> E
EUnOp UnOp
op' (ESafe -> E
extractSafeE ESafe
e'))) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
ENonStrict E
e)]
minMaxAbsEliminator (ENonStrict (PowI E
e Integer
i)) =
[([ESafe]
p, E -> ESafe
ENonStrict (E -> Integer -> E
PowI (ESafe -> E
extractSafeE ESafe
e') Integer
i)) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
ENonStrict E
e)]
minMaxAbsEliminator (ENonStrict (Float RoundingMode
mode E
e)) =
[([ESafe]
p, E -> ESafe
ENonStrict (RoundingMode -> E -> E
Float RoundingMode
mode (ESafe -> E
extractSafeE ESafe
e'))) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
ENonStrict E
e)]
minMaxAbsEliminator (ENonStrict (Float32 RoundingMode
mode E
e)) =
[([ESafe]
p, E -> ESafe
ENonStrict (RoundingMode -> E -> E
Float32 RoundingMode
mode (ESafe -> E
extractSafeE ESafe
e'))) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
ENonStrict E
e)]
minMaxAbsEliminator (ENonStrict (Float64 RoundingMode
mode E
e)) =
[([ESafe]
p, E -> ESafe
ENonStrict (RoundingMode -> E -> E
Float64 RoundingMode
mode (ESafe -> E
extractSafeE ESafe
e'))) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
ENonStrict E
e)]
minMaxAbsEliminator (ENonStrict (RoundToInteger RoundingMode
mode E
e)) =
[([ESafe]
p, E -> ESafe
ENonStrict (RoundingMode -> E -> E
RoundToInteger RoundingMode
mode (ESafe -> E
extractSafeE ESafe
e'))) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
ENonStrict E
e)]
minMaxAbsEliminator e :: ESafe
e@(ENonStrict (Lit Rational
_)) = [([],ESafe
e)]
minMaxAbsEliminator e :: ESafe
e@(ENonStrict (Var [Char]
_)) = [([],ESafe
e)]
minMaxAbsEliminator e :: ESafe
e@(ENonStrict E
Pi) = [([],ESafe
e)]
minMaxAbsEliminator (EStrict (EBinOp BinOp
op E
e1 E
e2)) =
case BinOp
op of
BinOp
Min ->
[[([ESafe], ESafe)]] -> [([ESafe], ESafe)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[
[
([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub (([ESafe]
p1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
p2) [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub (ESafe -> E
extractSafeE ESafe
e2') (ESafe -> E
extractSafeE ESafe
e1'))]), ESafe
e1'),
([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub (([ESafe]
p2 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
p1) [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub (ESafe -> E
extractSafeE ESafe
e1') (ESafe -> E
extractSafeE ESafe
e2'))]), ESafe
e2')
]
|
([ESafe]
p1, ESafe
e1') <- [([ESafe], ESafe)]
branch1, ([ESafe]
p2, ESafe
e2') <- [([ESafe], ESafe)]
branch2
]
BinOp
Max ->
[[([ESafe], ESafe)]] -> [([ESafe], ESafe)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[
[
([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub (([ESafe]
p1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
p2) [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub (ESafe -> E
extractSafeE ESafe
e1') (ESafe -> E
extractSafeE ESafe
e2'))]), ESafe
e1'),
([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub (([ESafe]
p2 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
p1) [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub (ESafe -> E
extractSafeE ESafe
e2') (ESafe -> E
extractSafeE ESafe
e1'))]), ESafe
e2')
]
|
([ESafe]
p1, ESafe
e1') <- [([ESafe], ESafe)]
branch1, ([ESafe]
p2, ESafe
e2') <- [([ESafe], ESafe)]
branch2
]
BinOp
op' ->
[([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub ([ESafe]
p1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
p2), E -> ESafe
EStrict (BinOp -> E -> E -> E
EBinOp BinOp
op' (ESafe -> E
extractSafeE ESafe
e1') (ESafe -> E
extractSafeE ESafe
e2'))) | ([ESafe]
p1, ESafe
e1') <- [([ESafe], ESafe)]
branch1, ([ESafe]
p2, ESafe
e2') <- [([ESafe], ESafe)]
branch2]
where
branch1 :: [([ESafe], ESafe)]
branch1 = ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
EStrict E
e1)
branch2 :: [([ESafe], ESafe)]
branch2 = ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
EStrict E
e2)
minMaxAbsEliminator (EStrict (EUnOp UnOp
op E
e)) =
case UnOp
op of
UnOp
Abs ->
ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
EStrict (BinOp -> E -> E -> E
EBinOp BinOp
Max E
e (UnOp -> E -> E
EUnOp UnOp
Negate E
e)))
UnOp
op' ->
[([ESafe]
p, E -> ESafe
EStrict (UnOp -> E -> E
EUnOp UnOp
op' (ESafe -> E
extractSafeE ESafe
e'))) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
EStrict E
e)]
minMaxAbsEliminator (EStrict (PowI E
e Integer
i)) =
[([ESafe]
p, E -> ESafe
EStrict (E -> Integer -> E
PowI (ESafe -> E
extractSafeE ESafe
e') Integer
i)) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
EStrict E
e)]
minMaxAbsEliminator (EStrict (Float RoundingMode
mode E
e)) =
[([ESafe]
p, E -> ESafe
EStrict (RoundingMode -> E -> E
Float RoundingMode
mode (ESafe -> E
extractSafeE ESafe
e'))) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
EStrict E
e)]
minMaxAbsEliminator (EStrict (Float32 RoundingMode
mode E
e)) =
[([ESafe]
p, E -> ESafe
EStrict (RoundingMode -> E -> E
Float32 RoundingMode
mode (ESafe -> E
extractSafeE ESafe
e'))) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
EStrict E
e)]
minMaxAbsEliminator (EStrict (Float64 RoundingMode
mode E
e)) =
[([ESafe]
p, E -> ESafe
EStrict (RoundingMode -> E -> E
Float64 RoundingMode
mode (ESafe -> E
extractSafeE ESafe
e'))) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
EStrict E
e)]
minMaxAbsEliminator (EStrict (RoundToInteger RoundingMode
mode E
e)) =
[([ESafe]
p, E -> ESafe
EStrict (RoundingMode -> E -> E
RoundToInteger RoundingMode
mode (ESafe -> E
extractSafeE ESafe
e'))) | ([ESafe]
p, ESafe
e') <- ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator (E -> ESafe
ENonStrict E
e)]
minMaxAbsEliminator e :: ESafe
e@(EStrict (Lit Rational
_)) = [([],ESafe
e)]
minMaxAbsEliminator e :: ESafe
e@(EStrict (Var [Char]
_)) = [([],ESafe
e)]
minMaxAbsEliminator e :: ESafe
e@(EStrict E
Pi) = [([],ESafe
e)]
minMaxAbsEliminatorECNF :: [[ESafe]] -> [[ESafe]]
minMaxAbsEliminatorECNF :: [[ESafe]] -> [[ESafe]]
minMaxAbsEliminatorECNF [[ESafe]]
ecnf = [[[ESafe]]] -> [[ESafe]]
and ([[[ESafe]]] -> [[ESafe]]) -> [[[ESafe]]] -> [[ESafe]]
forall a b. (a -> b) -> a -> b
$ ([[[ESafe]]] -> [[ESafe]]) -> [[[[ESafe]]]] -> [[[ESafe]]]
forall a b. (a -> b) -> [a] -> [b]
map [[[ESafe]]] -> [[ESafe]]
or (([ESafe] -> [[[ESafe]]]) -> [[ESafe]] -> [[[[ESafe]]]]
forall a b. (a -> b) -> [a] -> [b]
map ((ESafe -> [[ESafe]]) -> [ESafe] -> [[[ESafe]]]
forall a b. (a -> b) -> [a] -> [b]
map ([([ESafe], ESafe)] -> [[ESafe]]
qualifiedEsToCNF2 ([([ESafe], ESafe)] -> [[ESafe]])
-> (ESafe -> [([ESafe], ESafe)]) -> ESafe -> [[ESafe]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminator)) [[ESafe]]
ecnf)
where
and2 :: [a] -> [a] -> [a]
and2 = [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++)
or2 :: [[a]] -> [[a]] -> [[a]]
or2 [[a]]
ecnf1 [[a]]
ecnf2 = [[a]
d1 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
d2 | [a]
d1 <- [[a]]
ecnf1, [a]
d2 <- [[a]]
ecnf2]
and :: [[[ESafe]]] -> [[ESafe]]
and :: [[[ESafe]]] -> [[ESafe]]
and = ([[ESafe]] -> [[ESafe]] -> [[ESafe]])
-> [[ESafe]] -> [[[ESafe]]] -> [[ESafe]]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [[ESafe]] -> [[ESafe]] -> [[ESafe]]
forall a. [a] -> [a] -> [a]
and2 []
or :: [[[ESafe]]] -> [[ESafe]]
or :: [[[ESafe]]] -> [[ESafe]]
or = ([[ESafe]] -> [[ESafe]] -> [[ESafe]])
-> [[ESafe]] -> [[[ESafe]]] -> [[ESafe]]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [[ESafe]] -> [[ESafe]] -> [[ESafe]]
forall {a}. [[a]] -> [[a]] -> [[a]]
or2 [[]]
qualifiedEsToCNF2 :: [([ESafe],ESafe)] -> [[ESafe]]
qualifiedEsToCNF2 :: [([ESafe], ESafe)] -> [[ESafe]]
qualifiedEsToCNF2 =
(([ESafe], ESafe) -> [ESafe]) -> [([ESafe], ESafe)] -> [[ESafe]]
forall a b. (a -> b) -> [a] -> [b]
map
(\([ESafe]
ps,ESafe
q) ->
ESafe
q ESafe -> [ESafe] -> [ESafe]
forall a. a -> [a] -> [a]
: (ESafe -> ESafe) -> [ESafe] -> [ESafe]
forall a b. (a -> b) -> [a] -> [b]
map ESafe -> ESafe
negateSafeE [ESafe]
ps
)
qualifiedEsToDisjunction :: ([ESafe], ESafe) -> [ESafe]
qualifiedEsToDisjunction :: ([ESafe], ESafe) -> [ESafe]
qualifiedEsToDisjunction ([ESafe]
context, ESafe
goal) = ESafe
goal ESafe -> [ESafe] -> [ESafe]
forall a. a -> [a] -> [a]
: (ESafe -> ESafe) -> [ESafe] -> [ESafe]
forall a b. (a -> b) -> [a] -> [b]
map ESafe -> ESafe
negateSafeE [ESafe]
context
qualifiedEsToF :: [([ESafe], ESafe)] -> F
qualifiedEsToF :: [([ESafe], ESafe)] -> F
qualifiedEsToF [] = F
forall a. HasCallStack => a
undefined
qualifiedEsToF [([ESafe], ESafe)
qualifiedE] = ([ESafe], ESafe) -> F
qualifiedEToF ([ESafe], ESafe)
qualifiedE
qualifiedEsToF (([ESafe], ESafe)
qualifiedE : [([ESafe], ESafe)]
qualifiedEs) = Conn -> F -> F -> F
FConn Conn
And (([ESafe], ESafe) -> F
qualifiedEToF ([ESafe], ESafe)
qualifiedE) ([([ESafe], ESafe)] -> F
qualifiedEsToF [([ESafe], ESafe)]
qualifiedEs)
qualifiedEToF :: ([ESafe], ESafe) -> F
qualifiedEToF :: ([ESafe], ESafe) -> F
qualifiedEToF ([], ESafe
goal) = ESafe -> F
eSafeToF ESafe
goal
qualifiedEToF ([ESafe]
context, ESafe
goal) = Conn -> F -> F -> F
FConn Conn
Impl ([ESafe] -> F
aux [ESafe]
context) (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ ESafe -> F
eSafeToF ESafe
goal
where
aux :: [ESafe] -> F
aux [] = F
forall a. HasCallStack => a
undefined
aux [ESafe
c] = ESafe -> F
eSafeToF ESafe
c
aux (ESafe
c : [ESafe]
cs) = Conn -> F -> F -> F
FConn Conn
And (ESafe -> F
eSafeToF ESafe
c) ([ESafe] -> F
aux [ESafe]
cs)