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
    -- hasMinMaxAbsE could be removed
    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

-- | Given an expression, eliminate all Min, Max, and Abs
-- occurences. This is done by:
-- 
-- When we come across a Min e1 e2:
-- 1) We have two cases
-- 1a) if e2 >= e1, then choose e1
-- 1b) if e1 >= e2, then choose e2
-- 2) So, we eliminate min and add two elements to the qualified list
-- 2a) Add e2 - e1 to the list of premises, call the eliminiator on e1 and e2
-- recursively, add any new premises from the recursive call to the list of premises,
-- set the qualified value of e1 from the recursive call to be the qualified value
-- in this case
-- 2b) similar to 2a
-- 
-- Max e1 e2 is similar to Min e1 e2
-- Abs is treated as Max e (-e)
-- 
-- If we come across any other operator, recursively call the eliminator on any
-- expressions, add any resulting premises, and set the qualified value to be
-- the operator called on the resulting Es 
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'), -- e2' >= 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')  -- e1' >= 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'), -- e1' >= e2'
          ([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')  -- e2' >= e1'
        ]
        |
        ([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
      [
        [                      --Min/Max should always be non-strict here
          ([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'), -- e2' > 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')  -- e1' > 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'), -- e1' > e2'
          ([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')  -- e2' > e1'
        ]
        |
        ([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)]
-- If we extractSafeE, then strictness does not matter

-- [[[[E]]]] where [[E]] = [e1 /\ (e2 \/ e3) /\ e4]
-- [[[e1 /\ (e2 \/ e3) /\ e4]] \/ [e1 /\ (e2 \/ e3) /\ e4]]
-- [[[[e1 /\ (e2 \/ e3) /\ e4]] \/ [e1 /\ (e2 \/ e3) /\ e4]] /\ [[[e1 /\ (e2 \/ e3) /\ e4]] \/ [e1 /\ (e2 \/ e3) /\ e4]]]
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 [[]]

-- | Translate the qualified Es list to a single expression
-- The qualified Es list is basically the following formula:
-- e >= 0 == (p1 >= 0 /\ p2 >= 0 /\ p3 >=0 -> q1 >= 0) /\ repeat...
-- where e is the expression passed to minMaxAbsEliminator
-- 
-- This can be rewritten to
-- (-p1 >= 0 \/ - p2 >= 0 \/ -p3 >= 0 \/ q1 >= 0)
-- This is incorrect, strictness is not dealt with correctly
-- qualifiedEsToCNF :: [([E],E)] -> E
-- qualifiedEsToCNF []               = undefined
-- qualifiedEsToCNF [([], q)]        = q
-- qualifiedEsToCNF [(ps, q)]        = EBinOp Max (buildPs ps) q
--   where
--     buildPs :: [E] -> E
--     buildPs []  = undefined
--     buildPs [p] = (EUnOp Negate p)
--     buildPs (p : ps) = EBinOp Max (EUnOp Negate p) (buildPs ps) 
-- qualifiedEsToCNF ((ps, q) : es) = EBinOp Min (qualifiedEsToCNF [(ps, q)]) (qualifiedEsToCNF es)

-- | Convert a list of qualified Es to a CNF represented as a list of lists
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
  )
  -- The negation of ps turns it into ps < 0, which is equivalent to -ps > 0

-- Disjunction of Conjunction of Disjunction 

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)
-- TODO:

-- Translate to this type
-- Vector (Differential (CN MPBall)) -> [[Differential (CN MPBall)]]
-- We'd give this type some domain

-- type EvalE = Vector (Differential (CN MPBall)) -> Differential (CN MPBall)
-- type EvalECNF = Vector (Differential (CN MPBall)) -> [[Differential (CN MPBall)]]