{-# LANGUAGE TupleSections #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LambdaCase #-}
module PropaFP.Parsers.Smt where
import MixedTypesNumPrelude hiding (unzip)
import qualified Prelude as P
import System.IO.Unsafe
import PropaFP.Expression
import qualified PropaFP.Parsers.Lisp.Parser as LP
import qualified PropaFP.Parsers.Lisp.DataTypes as LD
import Data.Char (digitToInt)
import Data.Word
import qualified Data.ByteString.Lazy as B
import Data.Binary.Get
import Data.Maybe (mapMaybe)
import PropaFP.VarMap
import PropaFP.DeriveBounds
import PropaFP.EliminateFloats
import PropaFP.Eliminator (minMaxAbsEliminatorECNF, minMaxAbsEliminator)
import Data.List (nub, sort, isPrefixOf, sortBy, partition, foldl')
import Data.List.NonEmpty (unzip)
import Control.Arrow ((&&&))
import Debug.Trace
import PropaFP.Translators.DReal (formulaAndVarMapToDReal)
import Text.Regex.TDFA ( (=~) )
import Data.Ratio
import PropaFP.DeriveBounds
import qualified Data.Map as M
import AERN2.MP (endpoints, mpBallP, prec)
data ParsingMode = Why3 | CNF
parser :: String -> [LD.Expression]
parser :: String -> [Expression]
parser = [Expression] -> [Expression]
LP.analyzeExpressionSequence ([Expression] -> [Expression])
-> (String -> [Expression]) -> String -> [Expression]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [Expression]
LP.parseSequence ([String] -> [Expression])
-> (String -> [String]) -> String -> [Expression]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
LP.tokenize
parseSMT2 :: FilePath -> IO [LD.Expression]
parseSMT2 :: String -> IO [Expression]
parseSMT2 String
filePath = (String -> [Expression]) -> IO String -> IO [Expression]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> [Expression]
parser (IO String -> IO [Expression]) -> IO String -> IO [Expression]
forall a b. (a -> b) -> a -> b
$ String -> IO String
P.readFile String
filePath
findAssertions :: [LD.Expression] -> [LD.Expression]
findAssertions :: [Expression] -> [Expression]
findAssertions [] = []
findAssertions ((LD.Application (LD.Variable String
"assert") [Expression
operands]) : [Expression]
expressions) = Expression
operands Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression] -> [Expression]
findAssertions [Expression]
expressions
findAssertions (Expression
e : [Expression]
expressions) = [Expression] -> [Expression]
findAssertions [Expression]
expressions
findFunctionInputsAndOutputs :: [LD.Expression] -> [(String, ([String], String))]
findFunctionInputsAndOutputs :: [Expression] -> [(String, ([String], String))]
findFunctionInputsAndOutputs [] = []
findFunctionInputsAndOutputs ((LD.Application (LD.Variable String
"declare-fun") [LD.Variable String
fName, Expression
fInputsAsExpressions, LD.Variable String
fOutputs]) : [Expression]
expressions) =
(String
fName, (Expression -> [String]
expressionInputsAsString Expression
fInputsAsExpressions, String
fOutputs)) (String, ([String], String))
-> [(String, ([String], String))] -> [(String, ([String], String))]
forall a. a -> [a] -> [a]
: [Expression] -> [(String, ([String], String))]
findFunctionInputsAndOutputs [Expression]
expressions
where
expressionInputsAsString :: LD.Expression -> [String]
expressionInputsAsString :: Expression -> [String]
expressionInputsAsString (LD.Application (LD.Variable String
inputTypeAsString) [Expression]
remainingInputsAsExpression) = String
inputTypeAsString String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Expression -> [String]) -> [Expression] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expression -> [String]
expressionInputsAsString [Expression]
remainingInputsAsExpression
expressionInputsAsString (LD.Variable String
inputTypeAsString) = [String
inputTypeAsString]
expressionInputsAsString Expression
_ = []
findFunctionInputsAndOutputs (Expression
_ : [Expression]
expressions) = [Expression] -> [(String, ([String], String))]
findFunctionInputsAndOutputs [Expression]
expressions
findDeclarations :: [LD.Expression] -> [LD.Expression]
findDeclarations :: [Expression] -> [Expression]
findDeclarations [] = []
findDeclarations (declaration :: Expression
declaration@(LD.Application (LD.Variable String
"declare-fun") [Expression]
_) : [Expression]
expressions) = Expression
declaration Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression] -> [Expression]
findDeclarations [Expression]
expressions
findDeclarations (Expression
_ : [Expression]
expressions) = [Expression] -> [Expression]
findDeclarations [Expression]
expressions
findVariables :: [LD.Expression] -> [(String, String)]
findVariables :: [Expression] -> [(String, String)]
findVariables [] = []
findVariables (LD.Application (LD.Variable String
"declare-const") [LD.Variable String
varName, LD.Variable String
varType] : [Expression]
expressions)
= (String
varName, String
varType) (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [Expression] -> [(String, String)]
findVariables [Expression]
expressions
findVariables (LD.Application (LD.Variable String
"declare-fun") [LD.Variable String
varName, Expression
LD.Null, LD.Variable String
varType] : [Expression]
expressions)
= (String
varName, String
varType) (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [Expression] -> [(String, String)]
findVariables [Expression]
expressions
findVariables (Expression
_ : [Expression]
expressions) = [Expression] -> [(String, String)]
findVariables [Expression]
expressions
findIntegerVariables :: [(String, String)] -> [(String, VarType)]
findIntegerVariables :: [(String, String)] -> [(String, VarType)]
findIntegerVariables [] = []
findIntegerVariables ((String
v,String
t) : [(String, String)]
vs) =
if String
"Int" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
t Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| String
"int" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
t
then (String
v, VarType
Integer) (String, VarType) -> [(String, VarType)] -> [(String, VarType)]
forall a. a -> [a] -> [a]
: [(String, String)] -> [(String, VarType)]
findIntegerVariables [(String, String)]
vs
else [(String, String)] -> [(String, VarType)]
findIntegerVariables [(String, String)]
vs
findGoalsInAssertions :: [LD.Expression] -> [LD.Expression]
findGoalsInAssertions :: [Expression] -> [Expression]
findGoalsInAssertions [] = []
findGoalsInAssertions ((LD.Application (LD.Variable String
operator) [Expression]
operands) : [Expression]
assertions) =
if String
operator String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
"not"
then [Expression] -> Expression
forall a. [a] -> a
head [Expression]
operands Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression] -> [Expression]
findGoalsInAssertions [Expression]
assertions
else [Expression] -> [Expression]
findGoalsInAssertions [Expression]
assertions
findGoalsInAssertions (Expression
_ : [Expression]
assertions) = [Expression] -> [Expression]
findGoalsInAssertions [Expression]
assertions
takeGoalFromAssertions :: [LD.Expression] -> (LD.Expression, [LD.Expression])
takeGoalFromAssertions :: [Expression] -> (Expression, [Expression])
takeGoalFromAssertions [Expression]
asserts = (Expression
goal, [Expression]
assertsWithoutGoal)
where
numberOfAssertions :: Integer
numberOfAssertions = [Expression] -> Integer
forall (t :: * -> *) a. Foldable t => t a -> Integer
length [Expression]
asserts
goal :: Expression
goal = [Expression] -> Expression
forall a. [a] -> a
last [Expression]
asserts
assertsWithoutGoal :: [Expression]
assertsWithoutGoal = Integer -> [Expression] -> [Expression]
forall n a. CanBeInteger n => n -> [a] -> [a]
take (Integer
numberOfAssertions Integer -> Integer -> SubType Integer Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
1) [Expression]
asserts
parseFCompOp :: String -> Maybe (E -> E -> F)
parseFCompOp :: String -> Maybe (E -> E -> F)
parseFCompOp String
operator =
case String
operator of
String
n
| String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
">=", String
"fp.geq", String
"oge", String
"oge__logic"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^bool_ge$|^bool_ge[0-9]+$" :: Bool) -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Ge
| String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
">", String
"fp.gt", String
"ogt", String
"ogt__logic"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^bool_gt$|^bool_gt[0-9]+$" :: Bool) -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Gt
| String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"<=", String
"fp.leq", String
"ole", String
"ole__logic"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^bool_le$|^bool_le[0-9]+$" :: Bool) -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Le
| String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"<", String
"fp.lt", String
"olt", String
"olt__logic"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^bool_lt$|^bool_lt[0-9]+$" :: Bool) -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Lt
| String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"=", String
"fp.eq"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^bool_eq$|^bool_eq[0-9]+$|^user_eq$|^user_eq[0-9]+$" :: Bool) -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Eq
| String
"bool_neq" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
n -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ \E
e1 E
e2 -> F -> F
FNot (Comp -> E -> E -> F
FComp Comp
Eq E
e1 E
e2)
String
_ -> Maybe (E -> E -> F)
forall a. Maybe a
Nothing
parseIte :: Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
cond Expression
thenTerm Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs Maybe (E -> F)
Nothing =
case Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
cond [(String, ([String], String))]
functionsWithInputsAndOutputs of
Just F
condF ->
case (Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
thenTerm [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs) of
(Just F
thenTermF, Just F
elseTermF) ->
F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And
(Conn -> F -> F -> F
FConn Conn
Impl F
condF F
thenTermF)
(Conn -> F -> F -> F
FConn Conn
Impl (F -> F
FNot F
condF) F
elseTermF)
(Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
Maybe F
Nothing -> Maybe F
forall a. Maybe a
Nothing
parseIte Expression
cond Expression
thenTerm Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs (Just E -> F
compTerm) =
case Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
cond [(String, ([String], String))]
functionsWithInputsAndOutputs of
(Just F
condF) ->
case (Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
thenTerm [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs) of
(Just E
thenTermE, Just E
elseTermE) ->
F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And
(Conn -> F -> F -> F
FConn Conn
Impl F
condF (E -> F
compTerm E
thenTermE))
(Conn -> F -> F -> F
FConn Conn
Impl (F -> F
FNot F
condF) (E -> F
compTerm E
elseTermE))
(Just E
thenTermE, Maybe E
_) ->
case Expression
elseTerm of
LD.Application (LD.Variable String
"ite") [Expression
elseCond, Expression
elseThenTerm, Expression
elseElseTerm] ->
case Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
elseCond Expression
elseThenTerm Expression
elseElseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just E -> F
compTerm) of
Just F
elseTermF -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$
Conn -> F -> F -> F
FConn Conn
And
(Conn -> F -> F -> F
FConn Conn
Impl F
condF (E -> F
compTerm E
thenTermE))
(Conn -> F -> F -> F
FConn Conn
Impl (F -> F
FNot F
condF) F
elseTermF)
Maybe F
_ -> Maybe F
forall a. Maybe a
Nothing
Expression
_ -> Maybe F
forall a. Maybe a
Nothing
(Maybe E
_, Just E
elseTermE) ->
case Expression
thenTerm of
LD.Application (LD.Variable String
"ite") [Expression
thenCond, Expression
thenThenTerm, Expression
thenElseTerm] ->
case Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
thenCond Expression
thenThenTerm Expression
thenElseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just E -> F
compTerm) of
Just F
thenTermF -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$
Conn -> F -> F -> F
FConn Conn
And
(Conn -> F -> F -> F
FConn Conn
Impl F
condF F
thenTermF)
(Conn -> F -> F -> F
FConn Conn
Impl (F -> F
FNot F
condF) (E -> F
compTerm E
elseTermE))
Maybe F
_ -> Maybe F
forall a. Maybe a
Nothing
Expression
_ -> Maybe F
forall a. Maybe a
Nothing
(Maybe E
_, Maybe E
_) ->
case (Expression
thenTerm, Expression
elseTerm) of
(LD.Application (LD.Variable String
"ite") [Expression
thenCond, Expression
thenThenTerm, Expression
thenElseTerm], LD.Application (LD.Variable String
"ite") [Expression
elseCond, Expression
elseThenTerm, Expression
elseElseTerm]) ->
case (Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
thenCond Expression
thenThenTerm Expression
thenElseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just E -> F
compTerm), Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
elseCond Expression
elseThenTerm Expression
elseElseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just E -> F
compTerm)) of
(Just F
thenTermF, Just F
elseTermF) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$
Conn -> F -> F -> F
FConn Conn
And
(Conn -> F -> F -> F
FConn Conn
Impl F
condF F
thenTermF)
(Conn -> F -> F -> F
FConn Conn
Impl (F -> F
FNot F
condF) F
elseTermF)
(Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
(Expression
_, Expression
_) -> Maybe F
forall a. Maybe a
Nothing
Maybe F
Nothing -> Maybe F
forall a. Maybe a
Nothing
termToF :: LD.Expression -> [(String, ([String], String))] -> Maybe F
termToF :: Expression -> [(String, ([String], String))] -> Maybe F
termToF (LD.Application (LD.Variable String
operator) [Expression
op]) [(String, ([String], String))]
functionsWithInputsAndOutputs =
case Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op [(String, ([String], String))]
functionsWithInputsAndOutputs of
Just E
e ->
case String
operator of
String
"fp.isFinite32" ->
let maxFloat :: MulType Rational Integer
maxFloat = (Rational
2.0 Rational -> Rational -> SubType Rational Rational
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- (Integer
1Integer -> Integer -> DivType Integer Integer
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/(Integer
2Integer -> Integer -> PowType Integer Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
23))) Rational -> Integer -> MulType Rational Integer
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
* (Integer
2Integer -> Integer -> PowType Integer Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
127)
minFloat :: NegType Rational
minFloat = Rational -> NegType Rational
forall t. CanNeg t => t -> NegType t
negate Rational
maxFloat
in
F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Le (Rational -> E
Lit Rational
minFloat) E
e) (Comp -> E -> E -> F
FComp Comp
Le E
e (Rational -> E
Lit Rational
maxFloat))
String
"fp.isFinite64" ->
let maxFloat :: MulType Rational Integer
maxFloat = (Rational
2.0 Rational -> Rational -> SubType Rational Rational
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- (Integer
1Integer -> Integer -> DivType Integer Integer
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/(Integer
2Integer -> Integer -> PowType Integer Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
52))) Rational -> Integer -> MulType Rational Integer
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
* (Integer
2Integer -> Integer -> PowType Integer Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
1023)
minFloat :: NegType Rational
minFloat = Rational -> NegType Rational
forall t. CanNeg t => t -> NegType t
negate Rational
maxFloat
in
F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Le (Rational -> E
Lit Rational
minFloat) E
e) (Comp -> E -> E -> F
FComp Comp
Le E
e (Rational -> E
Lit Rational
maxFloat))
String
_ -> Maybe F
forall a. Maybe a
Nothing
Maybe E
Nothing ->
case Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
op [(String, ([String], String))]
functionsWithInputsAndOutputs of
Just F
f ->
case String
operator of
String
"not" -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ F -> F
FNot F
f
String
_ -> Maybe F
forall a. Maybe a
Nothing
Maybe F
_ -> Maybe F
forall a. Maybe a
Nothing
termToF (LD.Application (LD.Variable String
operator) [Expression
op1, Expression
op2]) [(String, ([String], String))]
functionsWithInputsAndOutputs =
case (Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op1 [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
(Just E
e1, Just E
e2) ->
case String -> Maybe (E -> E -> F)
parseFCompOp String
operator of
Just E -> E -> F
fCompOp -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ E -> E -> F
fCompOp E
e1 E
e2
Maybe (E -> E -> F)
_ -> Maybe F
forall a. Maybe a
Nothing
(Maybe E
_, Maybe E
_) ->
case (Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
op1 [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
(Just F
f1, Just F
f2) ->
case String
operator of
String
"and" -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And F
f1 F
f2
String
"or" -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Or F
f1 F
f2
String
"=>" -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Impl F
f1 F
f2
String
"=" -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Conn -> F -> F -> F
FConn Conn
Impl F
f1 F
f2) (Conn -> F -> F -> F
FConn Conn
Impl F
f2 F
f1)
String
n
| String
"bool_eq" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
n -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Conn -> F -> F -> F
FConn Conn
Impl F
f1 F
f2) (Conn -> F -> F -> F
FConn Conn
Impl F
f2 F
f1)
| String
"bool_neq" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
n -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ F -> F
FNot (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Conn -> F -> F -> F
FConn Conn
Impl F
f1 F
f2) (Conn -> F -> F -> F
FConn Conn
Impl F
f2 F
f1)
| String
"user_eq" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
n -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Conn -> F -> F -> F
FConn Conn
Impl F
f1 F
f2) (Conn -> F -> F -> F
FConn Conn
Impl F
f2 F
f1)
String
_ -> Maybe F
forall a. Maybe a
Nothing
(Maybe F
_, Maybe F
_) ->
case (Expression
op1, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
(LD.Application (LD.Variable String
"ite") [Expression
cond, Expression
thenTerm, Expression
elseTerm], Just E
e2) ->
case String -> Maybe (E -> E -> F)
parseFCompOp String
operator of
Just E -> E -> F
fCompOp -> Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
cond Expression
thenTerm Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just (\E
e -> E -> E -> F
fCompOp E
e E
e2))
Maybe (E -> E -> F)
Nothing -> Maybe F
forall a. Maybe a
Nothing
(Expression
_, Maybe E
_) ->
case (Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op1 [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression
op2) of
(Just E
e1, LD.Application (LD.Variable String
"ite") [Expression
cond, Expression
thenTerm, Expression
elseTerm]) ->
case String -> Maybe (E -> E -> F)
parseFCompOp String
operator of
Just E -> E -> F
fCompOp -> Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
cond Expression
thenTerm Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just (\E
e -> E -> E -> F
fCompOp E
e1 E
e))
Maybe (E -> E -> F)
Nothing -> Maybe F
forall a. Maybe a
Nothing
(Maybe E
_, Expression
_) -> Maybe F
forall a. Maybe a
Nothing
termToF (LD.Application (LD.Variable String
"ite") [Expression
cond, Expression
thenTerm, Expression
elseTerm]) [(String, ([String], String))]
functionsWithInputsAndOutputs =
Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
cond Expression
thenTerm Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs Maybe (E -> F)
forall a. Maybe a
Nothing
termToF (LD.Variable String
"true") [(String, ([String], String))]
functionsWithInputsAndOutputs = F -> Maybe F
forall a. a -> Maybe a
Just F
FTrue
termToF (LD.Variable String
"false") [(String, ([String], String))]
functionsWithInputsAndOutputs = F -> Maybe F
forall a. a -> Maybe a
Just F
FFalse
termToF Expression
_ [(String, ([String], String))]
_ = Maybe F
forall a. Maybe a
Nothing
termToE :: LD.Expression -> [(String, ([String], String))] -> Maybe E
termToE :: Expression -> [(String, ([String], String))] -> Maybe E
termToE (LD.Application (LD.Variable String
"*") [LD.Number Rational
4, LD.Application (LD.Variable String
"atan") [LD.Number Rational
1]]) [(String, ([String], String))]
functionsWithInputsAndOutputs = E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ E
Pi
termToE (LD.Variable String
"true") [(String, ([String], String))]
functionsWithInputsAndOutputs = Maybe E
forall a. Maybe a
Nothing
termToE (LD.Variable String
"false") [(String, ([String], String))]
functionsWithInputsAndOutputs = Maybe E
forall a. Maybe a
Nothing
termToE (LD.Variable String
var) [(String, ([String], String))]
functionsWithInputsAndOutputs = E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ String -> E
Var String
var
termToE (LD.Number Rational
num) [(String, ([String], String))]
functionsWithInputsAndOutputs = E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit Rational
num
termToE (LD.Application (LD.Variable String
"to_int_rne") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
RoundToInteger RoundingMode
RNE (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"to_int_rtp") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
RoundToInteger RoundingMode
RTP (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"to_int_rtn") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
RoundToInteger RoundingMode
RTN (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"to_int_rtz") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
RoundToInteger RoundingMode
RTZ (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"to_int_rna") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
RoundToInteger RoundingMode
RNA (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float32_rne") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float32 RoundingMode
RNE (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float32_rtp") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float32 RoundingMode
RTP (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float32_rtn") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float32 RoundingMode
RTN (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float32_rtz") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float32 RoundingMode
RTZ (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float32_rna") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float32 RoundingMode
RNA (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float64_rne") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float64 RoundingMode
RNE (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float64_rtp") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float64 RoundingMode
RTP (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float64_rtn") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float64 RoundingMode
RTN (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float64_rtz") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float64 RoundingMode
RTZ (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float64_rna") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float64 RoundingMode
RNA (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
operator) [Expression
op]) [(String, ([String], String))]
functionsWithInputsAndOutputs =
case Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op [(String, ([String], String))]
functionsWithInputsAndOutputs of
Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
Just E
e -> case String
operator of
String
n
| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^real_pi$|^real_pi[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just E
Pi
| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^abs$|^abs[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Abs E
e
| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^sin$|^sin[0-9]+$|^real_sin$|^real_sin[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Sin E
e
| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^cos$|^cos[0-9]+$|^real_cos$|^real_cos[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Cos E
e
| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^sqrt$|^sqrt[0-9]+$|^real_square_root$|^real_square_root[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Sqrt E
e
| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^fp.to_real$|^fp.to_real[0-9]+$|^to_real$|^to_real[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just E
e
String
"-" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Negate E
e
String
"from_int" -> E -> Maybe E
forall a. a -> Maybe a
Just E
e
String
"fp.abs" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Abs E
e
String
"fp.neg" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Negate E
e
String
"fp.isNormal" -> Maybe E
forall a. Maybe a
Nothing
String
"fp.isSubnormal" -> Maybe E
forall a. Maybe a
Nothing
String
"fp.isZero" -> Maybe E
forall a. Maybe a
Nothing
String
"fp.isNaN" -> Maybe E
forall a. Maybe a
Nothing
String
"fp.isPositive" -> Maybe E
forall a. Maybe a
Nothing
String
"fp.isNegative" -> Maybe E
forall a. Maybe a
Nothing
String
"fp.isIntegral32" -> Maybe E
forall a. Maybe a
Nothing
String
"fp.isIntegral64" -> Maybe E
forall a. Maybe a
Nothing
String
_ -> Maybe E
forall a. Maybe a
Nothing
where
deriveTypeForOneArgFunctions :: String -> (E -> E) -> E -> Maybe E
deriveTypeForOneArgFunctions :: String -> (E -> E) -> E -> Maybe E
deriveTypeForOneArgFunctions String
functionName E -> E
functionAsExpression E
functionArg =
let
(Maybe [String]
mInputTypes, Maybe String
mOutputType) = Maybe ([String], String) -> (Maybe [String], Maybe String)
forall (f :: * -> *) a b. Functor f => f (a, b) -> (f a, f b)
unzip (Maybe ([String], String) -> (Maybe [String], Maybe String))
-> Maybe ([String], String) -> (Maybe [String], Maybe String)
forall a b. (a -> b) -> a -> b
$ String
-> [(String, ([String], String))] -> Maybe ([String], String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
functionName [(String, ([String], String))]
functionsWithInputsAndOutputs
newFunctionArg :: E
newFunctionArg = E
functionArg
mNewFunctionAsExpression :: Maybe (E -> E)
mNewFunctionAsExpression =
case Maybe String
mOutputType of
Just String
outputType ->
case String
outputType of
String
"Real" -> (E -> E) -> Maybe (E -> E)
forall a. a -> Maybe a
Just E -> E
functionAsExpression
String
"Int" -> (E -> E) -> Maybe (E -> E)
forall a. a -> Maybe a
Just E -> E
functionAsExpression
String
_ -> Maybe (E -> E)
forall a. Maybe a
Nothing
Maybe String
Nothing -> (E -> E) -> Maybe (E -> E)
forall a. a -> Maybe a
Just E -> E
functionAsExpression
in
case Maybe (E -> E)
mNewFunctionAsExpression of
Just E -> E
newFunctionAsExpression -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ E -> E
newFunctionAsExpression E
newFunctionArg
Maybe (E -> E)
Nothing -> Maybe E
forall a. Maybe a
Nothing
termToE (LD.Application (LD.Variable String
"min") [Expression
p1, Expression
p2]) [(String, ([String], String))]
functionsWithInputsAndOutputs = BinOp -> E -> E -> E
EBinOp BinOp
Min (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p1 [(String, ([String], String))]
functionsWithInputsAndOutputs Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p2 [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"max") [Expression
p1, Expression
p2]) [(String, ([String], String))]
functionsWithInputsAndOutputs = BinOp -> E -> E -> E
EBinOp BinOp
Max (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p1 [(String, ([String], String))]
functionsWithInputsAndOutputs Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p2 [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
operator) [Expression
op1, Expression
op2]) [(String, ([String], String))]
functionsWithInputsAndOutputs =
case (Expression -> Maybe RoundingMode
parseRoundingMode Expression
op1, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
(Just RoundingMode
roundingMode, Just E
e) ->
case String
operator of
String
n
| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^round$|^round[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float RoundingMode
roundingMode E
e
| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^to_int$|^to_int[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
RoundToInteger RoundingMode
roundingMode E
e
| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^of_int$|^of_int[0-9]+$" :: Bool) ->
case String
-> [(String, ([String], String))] -> Maybe ([String], String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
n [(String, ([String], String))]
functionsWithInputsAndOutputs of
Just ([String]
_, String
outputType) ->
case String
outputType of
String
o
| String
o String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float32", String
"single"] -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float32 RoundingMode
roundingMode E
e
| String
o String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float64", String
"double"] -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float64 RoundingMode
roundingMode E
e
| String
o String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Real", String
"real"] -> E -> Maybe E
forall a. a -> Maybe a
Just E
e
String
_ -> Maybe E
forall a. Maybe a
Nothing
Maybe ([String], String)
_ -> Maybe E
forall a. Maybe a
Nothing
String
"fp.roundToIntegral" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
RoundToInteger RoundingMode
roundingMode E
e
String
_ -> Maybe E
forall a. Maybe a
Nothing
(Maybe RoundingMode, Maybe E)
_ ->
case (Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op1 [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
(Just E
e1, Just E
e2) ->
case String
operator of
String
n
| String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"+", String
"oadd", String
"oadd__logic"] -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Add E
e1 E
e2
| String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"-", String
"osubtract", String
"osubtract__logic"] -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2
| String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"*", String
"omultiply", String
"omultiply__logic"] -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Mul E
e1 E
e2
| String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"/", String
"odivide", String
"odivide__logic"] -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Div E
e1 E
e2
| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^pow$|^pow[0-9]+$|^power$|^power[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Pow E
e1 E
e2
| String
n String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
"^" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Pow E
e1 E
e2
| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^mod$|^mod[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Mod E
e1 E
e2
String
_ -> Maybe E
forall a. Maybe a
Nothing
(Maybe E
_, Maybe E
_) -> Maybe E
forall a. Maybe a
Nothing
termToE (LD.Application (LD.Variable String
"fp") [LD.Variable String
sSign, LD.Variable String
sExponent, LD.Variable String
sMantissa]) [(String, ([String], String))]
functionsWithInputsAndOutputs =
let
bSign :: String
bSign = Integer -> String -> String
forall n a. CanBeInteger n => n -> [a] -> [a]
drop Integer
2 String
sSign
bExponent :: String
bExponent = Integer -> String -> String
forall n a. CanBeInteger n => n -> [a] -> [a]
drop Integer
2 String
sExponent
bMantissa :: String
bMantissa = Integer -> String -> String
forall n a. CanBeInteger n => n -> [a] -> [a]
drop Integer
2 String
sMantissa
bFull :: String
bFull = String
bSign String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bExponent String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bMantissa
readBits :: String -> Integer -> Integer
readBits :: String -> Integer -> Integer
readBits [] Integer
_ = Integer
0
readBits (Char
bit : String
bits) Integer
digit = Char -> Int
digitToInt Char
bit Int -> Integer -> MulType Int Integer
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
* (Integer
2 Integer -> Integer -> PowType Integer Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^ (Integer
digit Integer -> Integer -> SubType Integer Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
1)) Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ String -> Integer -> Integer
readBits String
bits (Integer
digit Integer -> Integer -> SubType Integer Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
1)
bitsToWord8 :: String -> [Word8]
bitsToWord8 :: String -> [Word8]
bitsToWord8 String
bits =
let wordS :: String
wordS = Integer -> String -> String
forall n a. CanBeInteger n => n -> [a] -> [a]
take Integer
8 String
bits
rem :: String
rem = Integer -> String -> String
forall n a. CanBeInteger n => n -> [a] -> [a]
drop Integer
8 String
bits
wordV :: Integer
wordV = String -> Integer -> Integer
readBits String
wordS Integer
8
in
Integer -> Word8
forall a. Num a => Integer -> a
P.fromInteger Integer
wordV Word8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
: String -> [Word8]
bitsToWord8 String
rem
bsFloat :: ByteString
bsFloat = [Word8] -> ByteString
B.pack ([Word8] -> ByteString) -> [Word8] -> ByteString
forall a b. (a -> b) -> a -> b
$ String -> [Word8]
bitsToWord8 String
bFull
in
if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"01") String
bFull
then
case String -> Integer
forall (t :: * -> *) a. Foldable t => t a -> Integer
length String
bFull of
Integer
32 -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit (Rational -> E) -> Rational -> E
forall a b. (a -> b) -> a -> b
$ Float -> Rational
forall a. Real a => a -> Rational
toRational (Float -> Rational) -> Float -> Rational
forall a b. (a -> b) -> a -> b
$ Get Float -> ByteString -> Float
forall a. Get a -> ByteString -> a
runGet Get Float
getFloatbe ByteString
bsFloat
Integer
64 -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit (Rational -> E) -> Rational -> E
forall a b. (a -> b) -> a -> b
$ Double -> Rational
forall a. Real a => a -> Rational
toRational (Double -> Rational) -> Double -> Rational
forall a b. (a -> b) -> a -> b
$ Get Double -> ByteString -> Double
forall a. Get a -> ByteString -> a
runGet Get Double
getDoublebe ByteString
bsFloat
Integer
_ -> Maybe E
forall a. Maybe a
Nothing
else Maybe E
forall a. Maybe a
Nothing
termToE (LD.Application (LD.Variable String
operator) [Expression
roundingMode, Expression
op1, Expression
op2]) [(String, ([String], String))]
functionsWithInputsAndOutputs =
case (Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op1 [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
(Just E
e1, Just E
e2) ->
case Expression -> Maybe RoundingMode
parseRoundingMode Expression
roundingMode of
Just RoundingMode
mode ->
case String
operator of
String
"fp.add" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Add E
e1 E
e2
String
"fp.sub" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2
String
"fp.mul" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Mul E
e1 E
e2
String
"fp.div" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Div E
e1 E
e2
String
_ -> Maybe E
forall a. Maybe a
Nothing
Maybe RoundingMode
Nothing -> Maybe E
forall a. Maybe a
Nothing
(Maybe E
_, Maybe E
_) -> Maybe E
forall a. Maybe a
Nothing
termToE Expression
_ [(String, ([String], String))]
_ = Maybe E
forall a. Maybe a
Nothing
collapseOrs :: [LD.Expression] -> [LD.Expression]
collapseOrs :: [Expression] -> [Expression]
collapseOrs = (Expression -> Expression) -> [Expression] -> [Expression]
forall a b. (a -> b) -> [a] -> [b]
map Expression -> Expression
collapseOr
collapseOr :: LD.Expression -> LD.Expression
collapseOr :: Expression -> Expression
collapseOr orig :: Expression
orig@(LD.Application (LD.Variable String
"or") [LD.Application (LD.Variable String
"<") [Expression]
args1, LD.Application (LD.Variable String
"=") [Expression]
args2]) =
if [Expression]
args1 [Expression] -> [Expression] -> Bool
forall a. Eq a => a -> a -> Bool
P.== [Expression]
args2
then Expression -> [Expression] -> Expression
LD.Application (String -> Expression
LD.Variable String
"<=") [Expression]
args1
else Expression
orig
collapseOr orig :: Expression
orig@(LD.Application (LD.Variable String
"or") [LD.Application (LD.Variable String
"=") [Expression]
args1, LD.Application (LD.Variable String
"<") [Expression]
args2]) =
if [Expression]
args1 [Expression] -> [Expression] -> Bool
forall a. Eq a => a -> a -> Bool
P.== [Expression]
args2
then Expression -> [Expression] -> Expression
LD.Application (String -> Expression
LD.Variable String
"<=") [Expression]
args1
else Expression
orig
collapseOr orig :: Expression
orig@(LD.Application (LD.Variable String
"or") [LD.Application (LD.Variable String
">") [Expression]
args1, LD.Application (LD.Variable String
"=") [Expression]
args2]) =
if [Expression]
args1 [Expression] -> [Expression] -> Bool
forall a. Eq a => a -> a -> Bool
P.== [Expression]
args2
then Expression -> [Expression] -> Expression
LD.Application (String -> Expression
LD.Variable String
">=") [Expression]
args1
else Expression
orig
collapseOr orig :: Expression
orig@(LD.Application (LD.Variable String
"or") [LD.Application (LD.Variable String
"=") [Expression]
args1, LD.Application (LD.Variable String
">") [Expression]
args2]) =
if [Expression]
args1 [Expression] -> [Expression] -> Bool
forall a. Eq a => a -> a -> Bool
P.== [Expression]
args2
then Expression -> [Expression] -> Expression
LD.Application (String -> Expression
LD.Variable String
">=") [Expression]
args1
else Expression
orig
collapseOr (LD.Application Expression
operator [Expression]
args) = Expression -> [Expression] -> Expression
LD.Application Expression
operator ([Expression] -> [Expression]
collapseOrs [Expression]
args)
collapseOr Expression
e = Expression
e
eliminateKnownFunctionGuards :: [LD.Expression] -> [LD.Expression]
eliminateKnownFunctionGuards :: [Expression] -> [Expression]
eliminateKnownFunctionGuards = (Expression -> Expression) -> [Expression] -> [Expression]
forall a b. (a -> b) -> [a] -> [b]
map Expression -> Expression
eliminateKnownFunctionGuard
eliminateKnownFunctionGuard :: LD.Expression -> LD.Expression
eliminateKnownFunctionGuard :: Expression -> Expression
eliminateKnownFunctionGuard orig :: Expression
orig@(LD.Application operator :: Expression
operator@(LD.Variable String
var) args :: [Expression]
args@(Expression
guardedFunction : [Expression]
_)) =
let
knownGuardsRegex :: String
knownGuardsRegex =
String
"^real_sin__function_guard$|^real_sin__function_guard[0-9]+$|" String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"^real_cos__function_guard$|^real_cos__function_guard[0-9]+$|" String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"^real_square_root__function_guard$|^real_square_root__function_guard[0-9]+$|" String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"^real_pi__function_guard$|^real_pi__function_guard[0-9]+$"
in
if (String
var String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
knownGuardsRegex :: Bool)
then String -> Expression
LD.Variable String
"true"
else Expression -> [Expression] -> Expression
LD.Application Expression
operator ([Expression] -> [Expression]
eliminateKnownFunctionGuards [Expression]
args)
eliminateKnownFunctionGuard (LD.Application Expression
operator [Expression]
args) = Expression -> [Expression] -> Expression
LD.Application Expression
operator ([Expression] -> [Expression]
eliminateKnownFunctionGuards [Expression]
args)
eliminateKnownFunctionGuard Expression
e = Expression
e
termsToF :: [LD.Expression] -> [(String, ([String], String))] -> [F]
termsToF :: [Expression] -> [(String, ([String], String))] -> [F]
termsToF [Expression]
es [(String, ([String], String))]
fs = (Expression -> Maybe F) -> [Expression] -> [F]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Expression -> [(String, ([String], String))] -> Maybe F
`termToF` [(String, ([String], String))]
fs) [Expression]
es
determineFloatTypeE :: E -> [(String, String)] -> Maybe E
determineFloatTypeE :: E -> [(String, String)] -> Maybe E
determineFloatTypeE (EBinOp BinOp
op E
e1 E
e2) [(String, String)]
varTypeMap = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e1 [(String, String)]
varTypeMap of
Just E
p1 ->
case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e2 [(String, String)]
varTypeMap of
Just E
p2 -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
op E
p1 E
p2
Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE (EUnOp UnOp
op E
e) [(String, String)]
varTypeMap = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
op E
p
Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE (PowI E
e Integer
i) [(String, String)]
varTypeMap = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ E -> Integer -> E
PowI E
p Integer
i
Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE (Float RoundingMode
r E
e) [(String, String)]
varTypeMap = case Maybe String
mVariableType of
Just String
variableType ->
case String
variableType of
String
t
| String
t String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float32", String
"single"] ->
case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float32 RoundingMode
r E
p
Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
| String
t String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float64", String
"double"] ->
case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float64 RoundingMode
r E
p
Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
String
_ -> Maybe E
forall a. Maybe a
Nothing
Maybe String
Nothing -> Maybe E
forall a. Maybe a
Nothing
where
allVars :: [String]
allVars = E -> [String]
findVariablesInExpressions E
e
knownVarsWithPrecision :: [(String, Integer)]
knownVarsWithPrecision = E -> [(String, Integer)]
knownFloatVars E
e
knownVars :: [String]
knownVars = ((String, Integer) -> String) -> [(String, Integer)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Integer) -> String
forall a b. (a, b) -> a
fst [(String, Integer)]
knownVarsWithPrecision
unknownVars :: [String]
unknownVars = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
knownVars) [String]
allVars
mVariableType :: Maybe String
mVariableType = [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [String]
unknownVars [(String, String)]
varTypeMap [(String, Integer)]
knownVarsWithPrecision Maybe String
forall a. Maybe a
Nothing
determineFloatTypeE (Float32 RoundingMode
r E
e) [(String, String)]
varTypeMap = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float32 RoundingMode
r E
p
Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE (Float64 RoundingMode
r E
e) [(String, String)]
varTypeMap = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float64 RoundingMode
r E
p
Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE (RoundToInteger RoundingMode
r E
e) [(String, String)]
varTypeMap = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
RoundToInteger RoundingMode
r E
p
Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE E
Pi [(String, String)]
_ = E -> Maybe E
forall a. a -> Maybe a
Just E
Pi
determineFloatTypeE (Var String
v) [(String, String)]
varTypeMap = case String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
v [(String, String)]
varTypeMap of
Just String
variableType ->
case String
variableType of
String
_ -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ String -> E
Var String
v
Maybe String
_ -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ String -> E
Var String
v
determineFloatTypeE (Lit Rational
n) [(String, String)]
_ = E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit Rational
n
determineFloatTypeF :: F -> [(String, String)] -> Maybe F
determineFloatTypeF :: F -> [(String, String)] -> Maybe F
determineFloatTypeF (FComp Comp
op E
e1 E
e2) [(String, String)]
varTypeMap = case (E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e1 [(String, String)]
varTypeMap, E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e2 [(String, String)]
varTypeMap) of
(Just E
p1, Just E
p2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
op E
p1 E
p2
(Maybe E
_, Maybe E
_) -> Maybe F
forall a. Maybe a
Nothing
determineFloatTypeF (FConn Conn
op F
f1 F
f2) [(String, String)]
varTypeMap = case (F -> [(String, String)] -> Maybe F
determineFloatTypeF F
f1 [(String, String)]
varTypeMap, F -> [(String, String)] -> Maybe F
determineFloatTypeF F
f2 [(String, String)]
varTypeMap) of
(Just F
p1, Just F
p2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
op F
p1 F
p2
(Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
determineFloatTypeF (FNot F
f) [(String, String)]
varTypeMap = case F -> [(String, String)] -> Maybe F
determineFloatTypeF F
f [(String, String)]
varTypeMap of
Just F
p -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ F -> F
FNot F
p
Maybe F
Nothing -> Maybe F
forall a. Maybe a
Nothing
determineFloatTypeF F
FTrue [(String, String)]
_ = F -> Maybe F
forall a. a -> Maybe a
Just F
FTrue
determineFloatTypeF F
FFalse [(String, String)]
_ = F -> Maybe F
forall a. a -> Maybe a
Just F
FFalse
findVariableType :: [String] -> [(String, String)] -> [(String, Integer)] -> Maybe String -> Maybe String
findVariableType :: [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [] [(String, String)]
_ [] Maybe String
mFoundType = Maybe String
mFoundType
findVariableType [] [(String, String)]
_ ((String
_, Integer
precision) : [(String, Integer)]
vars) Maybe String
mFoundType =
case Maybe String
mFoundType of
Just String
t ->
if (String
t String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float32", String
"single"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& Integer
precision Integer -> Integer -> EqCompareType Integer Integer
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Integer
32) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| ((String
t String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float64", String
"double"]) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& (Integer
precision Integer -> Integer -> EqCompareType Integer Integer
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Integer
64))
then [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [] [] [(String, Integer)]
vars Maybe String
mFoundType
else Maybe String
forall a. Maybe a
Nothing
Maybe String
Nothing ->
case Integer
precision of
Integer
32 -> [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [] [] [(String, Integer)]
vars (String -> Maybe String
forall a. a -> Maybe a
Just String
"Float32")
Integer
64 -> [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [] [] [(String, Integer)]
vars (String -> Maybe String
forall a. a -> Maybe a
Just String
"Float64")
Integer
_ -> Maybe String
forall a. Maybe a
Nothing
findVariableType (String
v: [String]
vs) [(String, String)]
varTypeMap [(String, Integer)]
knownVarsWithPrecision Maybe String
mFoundType =
case String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
v [(String, String)]
varTypeMap of
Just String
t ->
if String
"Int" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
t then
[String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [String]
vs [(String, String)]
varTypeMap [(String, Integer)]
knownVarsWithPrecision Maybe String
mFoundType
else
case Maybe String
mFoundType of
Just String
f -> if String
f String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
t then [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [String]
vs [(String, String)]
varTypeMap [(String, Integer)]
knownVarsWithPrecision (String -> Maybe String
forall a. a -> Maybe a
Just String
t) else Maybe String
forall a. Maybe a
Nothing
Maybe String
Nothing -> [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [String]
vs [(String, String)]
varTypeMap [(String, Integer)]
knownVarsWithPrecision (String -> Maybe String
forall a. a -> Maybe a
Just String
t)
Maybe String
Nothing -> Maybe String
forall a. Maybe a
Nothing
knownFloatVars :: E -> [(String, Integer)]
knownFloatVars :: E -> [(String, Integer)]
knownFloatVars E
e = [(String, Integer)] -> [(String, Integer)]
removeConflictingVars ([(String, Integer)] -> [(String, Integer)])
-> ([(String, Integer)] -> [(String, Integer)])
-> [(String, Integer)]
-> [(String, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, Integer)] -> [(String, Integer)]
forall a. Eq a => [a] -> [a]
nub ([(String, Integer)] -> [(String, Integer)])
-> [(String, Integer)] -> [(String, Integer)]
forall a b. (a -> b) -> a -> b
$ E -> [(String, Integer)]
findAllFloatVars E
e
where
removeConflictingVars :: [(String, Integer)] -> [(String, Integer)]
removeConflictingVars :: [(String, Integer)] -> [(String, Integer)]
removeConflictingVars [] = []
removeConflictingVars ((String
v, Integer
t) : [(String, Integer)]
vs) =
if String
v String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((String, Integer) -> String) -> [(String, Integer)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Integer) -> String
forall a b. (a, b) -> a
fst [(String, Integer)]
vs
then [(String, Integer)] -> [(String, Integer)]
removeConflictingVars ([(String, Integer)] -> [(String, Integer)])
-> [(String, Integer)] -> [(String, Integer)]
forall a b. (a -> b) -> a -> b
$ ((String, Integer) -> Bool)
-> [(String, Integer)] -> [(String, Integer)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(String
v', Integer
_) -> String
v String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
/= String
v') [(String, Integer)]
vs
else (String
v, Integer
t) (String, Integer) -> [(String, Integer)] -> [(String, Integer)]
forall a. a -> [a] -> [a]
: [(String, Integer)] -> [(String, Integer)]
removeConflictingVars [(String, Integer)]
vs
findAllFloatVars :: E -> [(String, Integer)]
findAllFloatVars (EBinOp BinOp
_ E
e1 E
e2) = E -> [(String, Integer)]
knownFloatVars E
e1 [(String, Integer)] -> [(String, Integer)] -> [(String, Integer)]
forall a. [a] -> [a] -> [a]
++ E -> [(String, Integer)]
knownFloatVars E
e2
findAllFloatVars (EUnOp UnOp
_ E
e) = E -> [(String, Integer)]
knownFloatVars E
e
findAllFloatVars (PowI E
e Integer
_) = E -> [(String, Integer)]
knownFloatVars E
e
findAllFloatVars (Float RoundingMode
_ E
e) = E -> [(String, Integer)]
knownFloatVars E
e
findAllFloatVars (Float32 RoundingMode
_ (Var String
v)) = [(String
v, Integer
32)]
findAllFloatVars (Float64 RoundingMode
_ (Var String
v)) = [(String
v, Integer
64)]
findAllFloatVars (Float32 RoundingMode
_ E
e) = E -> [(String, Integer)]
knownFloatVars E
e
findAllFloatVars (Float64 RoundingMode
_ E
e) = E -> [(String, Integer)]
knownFloatVars E
e
findAllFloatVars (RoundToInteger RoundingMode
_ E
e) = E -> [(String, Integer)]
knownFloatVars E
e
findAllFloatVars (Var String
_) = []
findAllFloatVars (Lit Rational
_) = []
findAllFloatVars E
Pi = []
findVariablesInFormula :: F -> [String]
findVariablesInFormula :: F -> [String]
findVariablesInFormula F
f = [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ F -> [String]
findVars F
f
where
findVars :: F -> [String]
findVars (FConn Conn
_ F
f1 F
f2) = F -> [String]
findVars F
f1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ F -> [String]
findVars F
f2
findVars (FComp Comp
_ E
e1 E
e2) = E -> [String]
findVariablesInExpressions E
e1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ E -> [String]
findVariablesInExpressions E
e2
findVars (FNot F
f1) = F -> [String]
findVars F
f1
findVars F
FTrue = []
findVars F
FFalse = []
findVariablesInExpressions :: E -> [String]
findVariablesInExpressions :: E -> [String]
findVariablesInExpressions (EBinOp BinOp
_ E
e1 E
e2) = E -> [String]
findVariablesInExpressions E
e1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ E -> [String]
findVariablesInExpressions E
e2
findVariablesInExpressions (EUnOp UnOp
_ E
e) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (PowI E
e Integer
_) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (Float RoundingMode
_ E
e) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (Float32 RoundingMode
_ E
e) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (Float64 RoundingMode
_ E
e) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (RoundToInteger RoundingMode
_ E
e) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (Var String
v) = [String
v]
findVariablesInExpressions (Lit Rational
_) = []
findVariablesInExpressions E
Pi = []
parseRoundingMode :: LD.Expression -> Maybe RoundingMode
parseRoundingMode :: Expression -> Maybe RoundingMode
parseRoundingMode (LD.Variable String
mode) =
case String
mode of
String
m
| String
m String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"RNE", String
"NearestTiesToEven"] -> RoundingMode -> Maybe RoundingMode
forall a. a -> Maybe a
Just RoundingMode
RNE
| String
m String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"RTP", String
"Up"] -> RoundingMode -> Maybe RoundingMode
forall a. a -> Maybe a
Just RoundingMode
RTP
| String
m String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"RTN", String
"Down"] -> RoundingMode -> Maybe RoundingMode
forall a. a -> Maybe a
Just RoundingMode
RTN
| String
m String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"RTZ", String
"ToZero"] -> RoundingMode -> Maybe RoundingMode
forall a. a -> Maybe a
Just RoundingMode
RTZ
| String
m String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"RNA"] -> RoundingMode -> Maybe RoundingMode
forall a. a -> Maybe a
Just RoundingMode
RNA
String
_ -> Maybe RoundingMode
forall a. Maybe a
Nothing
parseRoundingMode Expression
_ = Maybe RoundingMode
forall a. Maybe a
Nothing
processVC :: [LD.Expression] -> Maybe (F, [(String, String)])
processVC :: [Expression] -> Maybe (F, [(String, String)])
processVC [Expression]
parsedExpressions =
(F, [(String, String)]) -> Maybe (F, [(String, String)])
forall a. a -> Maybe a
Just ([F] -> F
foldAssertionsF [F]
assertionsF, [(String, String)]
variablesWithTypes)
where
assertions :: [Expression]
assertions = [Expression] -> [Expression]
findAssertions [Expression]
parsedExpressions
assertionsF :: [F]
assertionsF = (F -> Maybe F) -> [F] -> [F]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (F -> [(String, String)] -> Maybe F
`determineFloatTypeF` [(String, String)]
variablesWithTypes) ([F] -> [F]) -> [F] -> [F]
forall a b. (a -> b) -> a -> b
$ ([Expression] -> [(String, ([String], String))] -> [F]
termsToF ([Expression] -> [(String, ([String], String))] -> [F])
-> ([Expression] -> [Expression])
-> [Expression]
-> [(String, ([String], String))]
-> [F]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expression] -> [Expression]
eliminateKnownFunctionGuards ([Expression] -> [Expression])
-> ([Expression] -> [Expression]) -> [Expression] -> [Expression]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expression] -> [Expression]
collapseOrs) [Expression]
assertions [(String, ([String], String))]
functionsWithInputsAndOutputs
variablesWithTypes :: [(String, String)]
variablesWithTypes = [Expression] -> [(String, String)]
findVariables [Expression]
parsedExpressions
functionsWithInputsAndOutputs :: [(String, ([String], String))]
functionsWithInputsAndOutputs = [Expression] -> [(String, ([String], String))]
findFunctionInputsAndOutputs [Expression]
parsedExpressions
foldAssertionsF :: [F] -> F
foldAssertionsF :: [F] -> F
foldAssertionsF [] = String -> F
forall a. HasCallStack => String -> a
error String
"processVC - foldAssertionsF: Empty list given"
foldAssertionsF [F
f] = F
f
foldAssertionsF (F
f : [F]
fs) = Conn -> F -> F -> F
FConn Conn
And F
f ([F] -> F
foldAssertionsF [F]
fs)
symbolicallySubstitutePiVars :: F -> F
symbolicallySubstitutePiVars :: F -> F
symbolicallySubstitutePiVars F
f = [String] -> F -> F
substVarsWithPi [String]
piVars F
f
where
piVars :: [String]
piVars = [String] -> [String]
forall a. Eq a => [a] -> [a]
nub (F -> [String]
aux F
f)
substVarsWithPi :: [String] -> F -> F
substVarsWithPi :: [String] -> F -> F
substVarsWithPi [] F
f' = F
f'
substVarsWithPi (String
v : [String]
_) F
f' = String -> F -> E -> F
substVarFWithE String
v F
f' E
Pi
aux :: F -> [String]
aux :: F -> [String]
aux (FConn Conn
And F
f1 F
f2) = F -> [String]
aux F
f1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ F -> [String]
aux F
f2
aux (FComp Comp
Lt (EBinOp BinOp
Div (Lit Rational
numer) (Lit Rational
denom)) (Var String
var)) =
[String
var |
(String
var String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^pi$|^pi[0-9]+$" :: Bool) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&&
Rational
DivType Rational Rational
lb Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= (Rational
7074237752028440.0 Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
2251799813685248.0) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&&
String -> F -> Bool
hasUB String
var F
f]
where
lb :: DivType Rational Rational
lb = Rational
numer Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
denom
aux (FComp {}) = []
aux (FConn {}) = []
aux (FNot F
_) = []
aux F
FTrue = []
aux F
FFalse = []
hasUB :: String -> F -> Bool
hasUB :: String -> F -> Bool
hasUB String
piVar (FComp Comp
Lt (Var String
otherVar) (EBinOp BinOp
Div (Lit Rational
numer) (Lit Rational
denom))) =
String
piVar String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
otherVar Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& Rational
DivType Rational Rational
ub Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
<= (Rational
7074237752028441.0 Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
2251799813685248.0)
where
ub :: DivType Rational Rational
ub = Rational
numer Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
denom
hasUB String
piVar (FConn Conn
And F
f1 F
f2) = String -> F -> Bool
hasUB String
piVar F
f1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| String -> F -> Bool
hasUB String
piVar F
f2
hasUB String
_ (FComp {}) = Bool
False
hasUB String
_ (FConn {}) = Bool
False
hasUB String
_ (FNot F
_) = Bool
False
hasUB String
_ F
FTrue = Bool
False
hasUB String
_ F
FFalse = Bool
False
deriveVCRanges :: F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges :: F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges F
vc [(String, String)]
varsWithTypes =
case F -> [String] -> Bool -> Maybe F
filterOutVars F
simplifiedF [String]
underivableVariables Bool
False of
Just F
filteredF -> (F, TypedVarMap) -> Maybe (F, TypedVarMap)
forall a. a -> Maybe a
Just (F
filteredF, TypedVarMap -> TypedVarMap
safelyRoundTypedVarMap TypedVarMap
typedDerivedVarMap)
Maybe F
Nothing -> Maybe (F, TypedVarMap)
forall a. Maybe a
Nothing
where
integerVariables :: [(String, VarType)]
integerVariables = [(String, String)] -> [(String, VarType)]
findIntegerVariables [(String, String)]
varsWithTypes
(F
simplifiedFUnchecked, VarMap
derivedVarMapUnchecked, [String]
underivableVariables) = F -> (F, VarMap, [String])
deriveBoundsAndSimplify F
vc
([Any]
piVars, VarMap
derivedVarMap) = ([], VarMap
derivedVarMapUnchecked)
typedDerivedVarMap :: TypedVarMap
typedDerivedVarMap = VarMap -> [(String, VarType)] -> TypedVarMap
unsafeVarMapToTypedVarMap VarMap
derivedVarMap [(String, VarType)]
integerVariables
safelyRoundTypedVarMap :: TypedVarMap -> TypedVarMap
safelyRoundTypedVarMap [] = []
safelyRoundTypedVarMap ((TypedVar (String
varName, (Rational
leftBound, Rational
rightBound)) VarType
Real) : TypedVarMap
vars) =
let
leftBoundRoundedDown :: Rational
leftBoundRoundedDown = MPFloat -> Rational
forall t. CanBeRational t => t -> Rational
rational (MPFloat -> Rational) -> (MPBall -> MPFloat) -> MPBall -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MPFloat, MPFloat) -> MPFloat
forall a b. (a, b) -> a
fst ((MPFloat, MPFloat) -> MPFloat)
-> (MPBall -> (MPFloat, MPFloat)) -> MPBall -> MPFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MPBall -> (MPFloat, MPFloat)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints (MPBall -> Rational) -> MPBall -> Rational
forall a b. (a -> b) -> a -> b
$ Precision -> Rational -> MPBall
forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP (Integer -> Precision
prec Integer
23) Rational
leftBound
rightBoundRoundedUp :: Rational
rightBoundRoundedUp = MPFloat -> Rational
forall t. CanBeRational t => t -> Rational
rational (MPFloat -> Rational) -> (MPBall -> MPFloat) -> MPBall -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MPFloat, MPFloat) -> MPFloat
forall a b. (a, b) -> b
snd ((MPFloat, MPFloat) -> MPFloat)
-> (MPBall -> (MPFloat, MPFloat)) -> MPBall -> MPFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MPBall -> (MPFloat, MPFloat)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints (MPBall -> Rational) -> MPBall -> Rational
forall a b. (a -> b) -> a -> b
$ Precision -> Rational -> MPBall
forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP (Integer -> Precision
prec Integer
23) Rational
rightBound
newBound :: TypedVarInterval
newBound = (String, (Rational, Rational)) -> VarType -> TypedVarInterval
TypedVar (String
varName, (Rational
leftBoundRoundedDown, Rational
rightBoundRoundedUp)) VarType
Real
in
TypedVarInterval
newBound TypedVarInterval -> TypedVarMap -> TypedVarMap
forall a. a -> [a] -> [a]
: TypedVarMap -> TypedVarMap
safelyRoundTypedVarMap TypedVarMap
vars
safelyRoundTypedVarMap (vi :: TypedVarInterval
vi@(TypedVar (String, (Rational, Rational))
_ VarType
Integer) : TypedVarMap
vars) = TypedVarInterval
vi TypedVarInterval -> TypedVarMap -> TypedVarMap
forall a. a -> [a] -> [a]
: TypedVarMap -> TypedVarMap
safelyRoundTypedVarMap TypedVarMap
vars
simplifiedF :: F
simplifiedF = F
simplifiedFUnchecked
findRealPiVars :: VarMap -> ([String], VarMap)
findRealPiVars :: VarMap -> ([String], VarMap)
findRealPiVars [] = ([], [])
findRealPiVars (varWithBounds :: (String, (Rational, Rational))
varWithBounds@(String
var, (Rational
l, Rational
r)) : VarMap
vars) =
if
(String
var String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^pi$|^pi[0-9]+$" :: Bool) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&&
Rational
l Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= (Rational
7074237752028440.0 Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
2251799813685248.0) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& Rational
r Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
<= (Rational
7074237752028441.0 Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
2251799813685248.0) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&&
(String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
var [(String, String)]
varsWithTypes Maybe String
-> Maybe String -> EqCompareType (Maybe String) (Maybe String)
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String -> Maybe String
forall a. a -> Maybe a
Just String
"Real")
then (\([String]
foundPiVars, VarMap
varMapWithoutPi) -> ((String
var String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
foundPiVars), VarMap
varMapWithoutPi)) (([String], VarMap) -> ([String], VarMap))
-> ([String], VarMap) -> ([String], VarMap)
forall a b. (a -> b) -> a -> b
$ VarMap -> ([String], VarMap)
findRealPiVars VarMap
vars
else (\([String]
foundPiVars, VarMap
varMapWithoutPi) -> ([String]
foundPiVars, ((String, (Rational, Rational))
varWithBounds (String, (Rational, Rational)) -> VarMap -> VarMap
forall a. a -> [a] -> [a]
: VarMap
varMapWithoutPi))) (([String], VarMap) -> ([String], VarMap))
-> ([String], VarMap) -> ([String], VarMap)
forall a b. (a -> b) -> a -> b
$ VarMap -> ([String], VarMap)
findRealPiVars VarMap
vars
substVarsWithPi :: [String] -> F -> F
substVarsWithPi :: [String] -> F -> F
substVarsWithPi [] F
f = F
f
substVarsWithPi (String
v : [String]
_) F
f = String -> F -> E -> F
substVarFWithE String
v F
f E
Pi
filterOutVars :: F -> [String] -> Bool -> Maybe F
filterOutVars :: F -> [String] -> Bool -> Maybe F
filterOutVars (FConn Conn
And F
f1 F
f2) [String]
vars Bool
False =
case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
False, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
False) of
(Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And F
ff1 F
ff2
(Just F
ff1, Maybe F
_) -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff1
(Maybe F
_, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff2
(Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
filterOutVars (FConn Conn
Or F
f1 F
f2) [String]
vars Bool
False =
case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
False, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
False) of
(Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Or F
ff1 F
ff2
(Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
filterOutVars (FConn Conn
Impl F
f1 F
f2) [String]
vars Bool
False =
case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
False, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
False) of
(Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Impl F
ff1 F
ff2
(Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
filterOutVars (FConn Conn
And F
f1 F
f2) [String]
vars Bool
True =
case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
True, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
True) of
(Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And F
ff1 F
ff2
(Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
filterOutVars (FConn Conn
Or F
f1 F
f2) [String]
vars Bool
True =
case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
True, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
True) of
(Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Or F
ff1 F
ff2
(Just F
ff1, Maybe F
_) -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff1
(Maybe F
_, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff2
(Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
filterOutVars (FConn Conn
Impl F
f1 F
f2) [String]
vars Bool
True =
case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
True, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
True) of
(Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Impl F
ff1 F
ff2
(Just F
ff1, Maybe F
_) -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff1
(Maybe F
_, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff2
(Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
filterOutVars (FNot F
f) [String]
vars Bool
isNegated = F -> F
FNot (F -> F) -> Maybe F -> Maybe F
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> F -> [String] -> Bool -> Maybe F
filterOutVars F
f [String]
vars (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
isNegated)
filterOutVars (FComp Comp
op E
e1 E
e2) [String]
vars Bool
_isNegated =
if [String] -> E -> Bool
eContainsVars [String]
vars E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| [String] -> E -> Bool
eContainsVars [String]
vars E
e2
then Maybe F
forall a. Maybe a
Nothing
else F -> Maybe F
forall a. a -> Maybe a
Just (Comp -> E -> E -> F
FComp Comp
op E
e1 E
e2)
filterOutVars F
FTrue [String]
_ Bool
_ = F -> Maybe F
forall a. a -> Maybe a
Just F
FTrue
filterOutVars F
FFalse [String]
_ Bool
_ = F -> Maybe F
forall a. a -> Maybe a
Just F
FFalse
eContainsVars :: [String] -> E -> Bool
eContainsVars :: [String] -> E -> Bool
eContainsVars [String]
vars (Var String
var) = String
var String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
vars
eContainsVars [String]
_ (Lit Rational
_) = Bool
False
eContainsVars [String]
_ E
Pi = Bool
False
eContainsVars [String]
vars (EBinOp BinOp
_ E
e1 E
e2) = [String] -> E -> Bool
eContainsVars [String]
vars E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| [String] -> E -> Bool
eContainsVars [String]
vars E
e2
eContainsVars [String]
vars (EUnOp UnOp
_ E
e) = [String] -> E -> Bool
eContainsVars [String]
vars E
e
eContainsVars [String]
vars (PowI E
e Integer
_) = [String] -> E -> Bool
eContainsVars [String]
vars E
e
eContainsVars [String]
vars (Float32 RoundingMode
_ E
e) = [String] -> E -> Bool
eContainsVars [String]
vars E
e
eContainsVars [String]
vars (Float64 RoundingMode
_ E
e) = [String] -> E -> Bool
eContainsVars [String]
vars E
e
eContainsVars [String]
vars (Float RoundingMode
_ E
e) = [String] -> E -> Bool
eContainsVars [String]
vars E
e
eContainsVars [String]
vars (RoundToInteger RoundingMode
_ E
e) = [String] -> E -> Bool
eContainsVars [String]
vars E
e
fContainsVars :: [String] -> F -> Bool
fContainsVars :: [String] -> F -> Bool
fContainsVars [String]
vars (FConn Conn
_ F
f1 F
f2) = [String] -> F -> Bool
fContainsVars [String]
vars F
f1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| [String] -> F -> Bool
fContainsVars [String]
vars F
f2
fContainsVars [String]
vars (FComp Comp
_ E
e1 E
e2) = [String] -> E -> Bool
eContainsVars [String]
vars E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| [String] -> E -> Bool
eContainsVars [String]
vars E
e2
fContainsVars [String]
vars (FNot F
f) = [String] -> F -> Bool
fContainsVars [String]
vars F
f
fContainsVars [String]
_ F
FTrue = Bool
False
fContainsVars [String]
_ F
FFalse = Bool
False
inequalityEpsilon :: Rational
inequalityEpsilon :: Rational
inequalityEpsilon = Rational
0.000000001
findVarEqualities :: F -> [(String, E)]
findVarEqualities :: F -> [(String, E)]
findVarEqualities (FConn Conn
And F
f1 F
f2) = F -> [(String, E)]
findVarEqualities F
f1 [(String, E)] -> [(String, E)] -> [(String, E)]
forall a. [a] -> [a] -> [a]
++ F -> [(String, E)]
findVarEqualities F
f2
findVarEqualities FConn {} = []
findVarEqualities (FComp Comp
Eq (Var String
v) E
e2) = [(String
v, E
e2)]
findVarEqualities (FComp Comp
Eq E
e1 (Var String
v)) = [(String
v, E
e1)]
findVarEqualities FComp {} = []
findVarEqualities (FNot F
_) = []
findVarEqualities F
FTrue = []
findVarEqualities F
FFalse = []
filterOutCircularVarEqualities :: [(String, E)] -> [(String, E)]
filterOutCircularVarEqualities :: [(String, E)] -> [(String, E)]
filterOutCircularVarEqualities = ((String, E) -> Bool) -> [(String, E)] -> [(String, E)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(String
v, E
e) -> String
v String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` E -> [String]
findVariablesInExpressions E
e)
filterOutDuplicateVarEqualities :: [(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities :: [(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities [] = []
filterOutDuplicateVarEqualities ((String
v, E
e) : [(String, E)]
vs) =
case ((String, E) -> Bool)
-> [(String, E)] -> ([(String, E)], [(String, E)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(String
v',E
_) -> String
v String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
v') [(String, E)]
vs of
([], [(String, E)]
_) -> (String
v, E
e) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: [(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities [(String, E)]
vs
([(String, E)]
matchingEqualities, [(String, E)]
otherEqualities) ->
let shortestVarEquality :: (String, E)
shortestVarEquality = [(String, E)] -> (String, E)
forall a. [a] -> a
head ([(String, E)] -> (String, E)) -> [(String, E)] -> (String, E)
forall a b. (a -> b) -> a -> b
$ ((String, E) -> (String, E) -> Ordering)
-> [(String, E)] -> [(String, E)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(String
_, E
e1) (String
_, E
e2) -> Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
P.compare (E -> Integer
lengthE E
e1) (E -> Integer
lengthE E
e2)) ([(String, E)] -> [(String, E)]) -> [(String, E)] -> [(String, E)]
forall a b. (a -> b) -> a -> b
$ (String
v, E
e) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: [(String, E)]
matchingEqualities
in (String, E)
shortestVarEquality (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: [(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities [(String, E)]
otherEqualities
substAllEqualities :: F -> F
substAllEqualities :: F -> F
substAllEqualities = F -> F
recursivelySubstVars
where
recursivelySubstVars :: F -> F
recursivelySubstVars f :: F
f@(FConn Conn
Impl F
context F
_) =
case [(String, E)]
filteredVarEqualities of
[] -> F
f
[(String, E)]
_ -> if F
f F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
substitutedF then F
f else F -> F
recursivelySubstVars (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> F
simplifyF (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F
substitutedF
where
substitutedF :: F
substitutedF = [(String, E)] -> F -> F
substVars [(String, E)]
filteredVarEqualities F
f
filteredVarEqualities :: [(String, E)]
filteredVarEqualities = ([(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities ([(String, E)] -> [(String, E)])
-> ([(String, E)] -> [(String, E)])
-> [(String, E)]
-> [(String, E)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, E)] -> [(String, E)]
filterOutCircularVarEqualities) [(String, E)]
varEqualities
varEqualities :: [(String, E)]
varEqualities = F -> [(String, E)]
findVarEqualities F
context
recursivelySubstVars F
f =
case [(String, E)]
filteredVarEqualities of
[] -> F
f
[(String, E)]
_ -> if F
f F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
substitutedF then F
f else F -> F
recursivelySubstVars (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> F
simplifyF (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F
substitutedF
where
substitutedF :: F
substitutedF = [(String, E)] -> F -> F
substVars [(String, E)]
filteredVarEqualities F
f
filteredVarEqualities :: [(String, E)]
filteredVarEqualities = ([(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities ([(String, E)] -> [(String, E)])
-> ([(String, E)] -> [(String, E)])
-> [(String, E)]
-> [(String, E)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, E)] -> [(String, E)]
filterOutCircularVarEqualities) [(String, E)]
varEqualities
varEqualities :: [(String, E)]
varEqualities = F -> [(String, E)]
findVarEqualities F
f
substVars :: [(String, E)] -> F -> F
substVars [] F
f = F
f
substVars ((String
v, E
e) : [(String, E)]
_) F
f = String -> F -> E -> F
substVarFWithE String
v F
f E
e
addVarMapBoundsToF :: F -> TypedVarMap -> F
addVarMapBoundsToF :: F -> TypedVarMap -> F
addVarMapBoundsToF F
f [] = F
f
addVarMapBoundsToF F
f (TypedVar (String
v, (Rational
l, Rational
r)) VarType
_ : TypedVarMap
vm) = Conn -> F -> F -> F
FConn Conn
And F
boundAsF (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F -> TypedVarMap -> F
addVarMapBoundsToF F
f TypedVarMap
vm
where
boundAsF :: F
boundAsF = Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Ge (String -> E
Var String
v) (Rational -> E
Lit Rational
l)) (Comp -> E -> E -> F
FComp Comp
Le (String -> E
Var String
v) (Rational -> E
Lit Rational
r))
eliminateFloatsAndSimplifyVC :: F -> TypedVarMap -> Bool -> FilePath -> IO F
eliminateFloatsAndSimplifyVC :: F -> TypedVarMap -> Bool -> String -> IO F
eliminateFloatsAndSimplifyVC F
vc TypedVarMap
typedVarMap Bool
strengthenVC String
fptaylorPath =
do
F
vcWithoutFloats <- F -> VarMap -> Bool -> String -> IO F
eliminateFloatsF F
vc (TypedVarMap -> VarMap
typedVarMapToVarMap TypedVarMap
typedVarMap) Bool
strengthenVC String
fptaylorPath
let typedVarMapAsMap :: Map String (Maybe Rational, Maybe Rational)
typedVarMapAsMap = [(String, (Maybe Rational, Maybe Rational))]
-> Map String (Maybe Rational, Maybe Rational)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(String, (Maybe Rational, Maybe Rational))]
-> Map String (Maybe Rational, Maybe Rational))
-> [(String, (Maybe Rational, Maybe Rational))]
-> Map String (Maybe Rational, Maybe Rational)
forall a b. (a -> b) -> a -> b
$ (TypedVarInterval -> (String, (Maybe Rational, Maybe Rational)))
-> TypedVarMap -> [(String, (Maybe Rational, Maybe Rational))]
forall a b. (a -> b) -> [a] -> [b]
map (\(TypedVar (String
varName, (Rational
leftBound, Rational
rightBound)) VarType
_) -> (String
varName, (Rational -> Maybe Rational
forall a. a -> Maybe a
Just Rational
leftBound, Rational -> Maybe Rational
forall a. a -> Maybe a
Just Rational
rightBound))) TypedVarMap
typedVarMap
let simplifiedVCWithoutFloats :: F
simplifiedVCWithoutFloats = (F -> F
simplifyF (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String (Maybe Rational, Maybe Rational) -> F -> F
evalF_comparisons Map String (Maybe Rational, Maybe Rational)
typedVarMapAsMap) F
vcWithoutFloats
F -> IO F
forall (m :: * -> *) a. Monad m => a -> m a
return F
simplifiedVCWithoutFloats
parseVCToF :: FilePath -> FilePath -> IO (Maybe (F, TypedVarMap))
parseVCToF :: String -> String -> IO (Maybe (F, TypedVarMap))
parseVCToF String
filePath String
fptaylorPath =
do
[Expression]
parsedFile <- String -> IO [Expression]
parseSMT2 String
filePath
case [Expression] -> Maybe (F, [(String, String)])
processVC [Expression]
parsedFile of
Just (F
vc, [(String, String)]
varTypes) ->
let
simplifiedVC :: F
simplifiedVC = (F -> F
symbolicallySubstitutePiVars (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> F
substAllEqualities (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> F
simplifyF) F
vc
mDerivedVCWithRanges :: Maybe (F, TypedVarMap)
mDerivedVCWithRanges = F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges F
simplifiedVC [(String, String)]
varTypes
in
case Maybe (F, TypedVarMap)
mDerivedVCWithRanges of
Just (F
derivedVC, TypedVarMap
derivedRanges) ->
do
let strengthenVC :: Bool
strengthenVC = Bool
False
F
vcWithoutFloats <- F -> VarMap -> Bool -> String -> IO F
eliminateFloatsF F
derivedVC (TypedVarMap -> VarMap
typedVarMapToVarMap TypedVarMap
derivedRanges) Bool
strengthenVC String
fptaylorPath
let vcWithoutFloatsWithBounds :: F
vcWithoutFloatsWithBounds = F -> TypedVarMap -> F
addVarMapBoundsToF F
vcWithoutFloats TypedVarMap
derivedRanges
case F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges F
vcWithoutFloatsWithBounds [(String, String)]
varTypes of
Just (F
simplifiedVCWithoutFloats, TypedVarMap
finalDerivedRanges) -> Maybe (F, TypedVarMap) -> IO (Maybe (F, TypedVarMap))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (F, TypedVarMap) -> IO (Maybe (F, TypedVarMap)))
-> Maybe (F, TypedVarMap) -> IO (Maybe (F, TypedVarMap))
forall a b. (a -> b) -> a -> b
$ (F, TypedVarMap) -> Maybe (F, TypedVarMap)
forall a. a -> Maybe a
Just (F
simplifiedVCWithoutFloats, TypedVarMap
finalDerivedRanges)
Maybe (F, TypedVarMap)
Nothing -> String -> IO (Maybe (F, TypedVarMap))
forall a. HasCallStack => String -> a
error String
"Error deriving bounds again after floating-point elimination"
Maybe (F, TypedVarMap)
Nothing -> Maybe (F, TypedVarMap) -> IO (Maybe (F, TypedVarMap))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (F, TypedVarMap)
forall a. Maybe a
Nothing
Maybe (F, [(String, String)])
Nothing -> Maybe (F, TypedVarMap) -> IO (Maybe (F, TypedVarMap))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (F, TypedVarMap)
forall a. Maybe a
Nothing
parseVCToSolver :: FilePath -> FilePath -> (F -> TypedVarMap -> String) -> Bool -> IO (Maybe String)
parseVCToSolver :: String
-> String
-> (F -> TypedVarMap -> String)
-> Bool
-> IO (Maybe String)
parseVCToSolver String
filePath String
fptaylorPath F -> TypedVarMap -> String
proverTranslator Bool
negateVC =
do
[Expression]
parsedFile <- String -> IO [Expression]
parseSMT2 String
filePath
case [Expression] -> Maybe (F, [(String, String)])
processVC [Expression]
parsedFile of
Just (F
vc, [(String, String)]
varTypes) ->
let
simplifiedVC :: F
simplifiedVC = (F -> F
substAllEqualities (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> F
simplifyF) F
vc
mDerivedVCWithRanges :: Maybe (F, TypedVarMap)
mDerivedVCWithRanges = F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges F
simplifiedVC [(String, String)]
varTypes
in
case Maybe (F, TypedVarMap)
mDerivedVCWithRanges of
Just (F
derivedVC, TypedVarMap
derivedRanges) ->
do
let strengthenVC :: Bool
strengthenVC = Bool
False
F
vcWithoutFloats <- F -> VarMap -> Bool -> String -> IO F
eliminateFloatsF F
derivedVC (TypedVarMap -> VarMap
typedVarMapToVarMap TypedVarMap
derivedRanges) Bool
strengthenVC String
fptaylorPath
let vcWithoutFloatsWithBounds :: F
vcWithoutFloatsWithBounds = F -> TypedVarMap -> F
addVarMapBoundsToF F
vcWithoutFloats TypedVarMap
derivedRanges
case F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges F
vcWithoutFloatsWithBounds [(String, String)]
varTypes of
Just (F
simplifiedVCWithoutFloats, TypedVarMap
finalDerivedRanges) ->
Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> IO (Maybe String))
-> Maybe String -> IO (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just (
F -> TypedVarMap -> String
proverTranslator
(
if Bool
negateVC
then
case F
simplifiedVCWithoutFloats of
FNot F
f -> F
f
F
_ -> F -> F
FNot F
simplifiedVCWithoutFloats
else F
simplifiedVCWithoutFloats
)
TypedVarMap
finalDerivedRanges
)
Maybe (F, TypedVarMap)
Nothing -> String -> IO (Maybe String)
forall a. HasCallStack => String -> a
error String
"Error deriving bounds again after floating-point elimination"
Maybe (F, TypedVarMap)
Nothing -> Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
Maybe (F, [(String, String)])
Nothing -> Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing