{-|
Module      : What4.Protocol.PolyRoot
Description : Representation for algebraic reals
Copyright   : (c) Galois Inc, 2016-2020
License     : BSD3
Maintainer  : jhendrix@galois.com

Defines a numeric data-type where each number is represented as the root of a
polynomial over a single variable.

This currently only defines operations for parsing the roots from the format
generated by Yices, and evaluating a polynomial over rational coefficients
to the rational derived from the closest double.
-}

{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
module What4.Protocol.PolyRoot
  ( Root
  , approximate
  , fromYicesText
  , parseYicesRoot
  ) where

import           Control.Applicative
import           Control.Lens
import qualified Data.Attoparsec.Text as Atto
import qualified Data.Map as Map
import           Data.Ratio
import           Data.Text (Text)
import qualified Data.Text as Text

import qualified Data.Vector as V
import           Prettyprinter as PP

atto_angle :: Atto.Parser a -> Atto.Parser a
atto_angle :: forall a. Parser a -> Parser a
atto_angle Parser a
p = Char -> Parser Char
Atto.char Char
'<' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser a
p forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
Atto.char Char
'>'

atto_paren :: Atto.Parser a -> Atto.Parser a
atto_paren :: forall a. Parser a -> Parser a
atto_paren Parser a
p = Char -> Parser Char
Atto.char Char
'(' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser a
p forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
Atto.char Char
')'

-- | A polynomial with one variable.
newtype SingPoly coef = SingPoly (V.Vector coef)
  deriving (forall a b. a -> SingPoly b -> SingPoly a
forall a b. (a -> b) -> SingPoly a -> SingPoly b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> SingPoly b -> SingPoly a
$c<$ :: forall a b. a -> SingPoly b -> SingPoly a
fmap :: forall a b. (a -> b) -> SingPoly a -> SingPoly b
$cfmap :: forall a b. (a -> b) -> SingPoly a -> SingPoly b
Functor, forall a. Eq a => a -> SingPoly a -> Bool
forall a. Num a => SingPoly a -> a
forall a. Ord a => SingPoly a -> a
forall m. Monoid m => SingPoly m -> m
forall a. SingPoly a -> Bool
forall a. SingPoly a -> Int
forall a. SingPoly a -> [a]
forall a. (a -> a -> a) -> SingPoly a -> a
forall m a. Monoid m => (a -> m) -> SingPoly a -> m
forall b a. (b -> a -> b) -> b -> SingPoly a -> b
forall a b. (a -> b -> b) -> b -> SingPoly a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => SingPoly a -> a
$cproduct :: forall a. Num a => SingPoly a -> a
sum :: forall a. Num a => SingPoly a -> a
$csum :: forall a. Num a => SingPoly a -> a
minimum :: forall a. Ord a => SingPoly a -> a
$cminimum :: forall a. Ord a => SingPoly a -> a
maximum :: forall a. Ord a => SingPoly a -> a
$cmaximum :: forall a. Ord a => SingPoly a -> a
elem :: forall a. Eq a => a -> SingPoly a -> Bool
$celem :: forall a. Eq a => a -> SingPoly a -> Bool
length :: forall a. SingPoly a -> Int
$clength :: forall a. SingPoly a -> Int
null :: forall a. SingPoly a -> Bool
$cnull :: forall a. SingPoly a -> Bool
toList :: forall a. SingPoly a -> [a]
$ctoList :: forall a. SingPoly a -> [a]
foldl1 :: forall a. (a -> a -> a) -> SingPoly a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SingPoly a -> a
foldr1 :: forall a. (a -> a -> a) -> SingPoly a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> SingPoly a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> SingPoly a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SingPoly a -> b
foldl :: forall b a. (b -> a -> b) -> b -> SingPoly a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SingPoly a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> SingPoly a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SingPoly a -> b
foldr :: forall a b. (a -> b -> b) -> b -> SingPoly a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> SingPoly a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> SingPoly a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SingPoly a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> SingPoly a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SingPoly a -> m
fold :: forall m. Monoid m => SingPoly m -> m
$cfold :: forall m. Monoid m => SingPoly m -> m
Foldable, Functor SingPoly
Foldable SingPoly
forall (t :: Type -> Type).
Functor t
-> Foldable t
-> (forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a.
Monad m =>
SingPoly (m a) -> m (SingPoly a)
forall (f :: Type -> Type) a.
Applicative f =>
SingPoly (f a) -> f (SingPoly a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> SingPoly a -> m (SingPoly b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> SingPoly a -> f (SingPoly b)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
SingPoly (m a) -> m (SingPoly a)
$csequence :: forall (m :: Type -> Type) a.
Monad m =>
SingPoly (m a) -> m (SingPoly a)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> SingPoly a -> m (SingPoly b)
$cmapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> SingPoly a -> m (SingPoly b)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
SingPoly (f a) -> f (SingPoly a)
$csequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
SingPoly (f a) -> f (SingPoly a)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> SingPoly a -> f (SingPoly b)
$ctraverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> SingPoly a -> f (SingPoly b)
Traversable, Int -> SingPoly coef -> ShowS
forall coef. Show coef => Int -> SingPoly coef -> ShowS
forall coef. Show coef => [SingPoly coef] -> ShowS
forall coef. Show coef => SingPoly coef -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SingPoly coef] -> ShowS
$cshowList :: forall coef. Show coef => [SingPoly coef] -> ShowS
show :: SingPoly coef -> String
$cshow :: forall coef. Show coef => SingPoly coef -> String
showsPrec :: Int -> SingPoly coef -> ShowS
$cshowsPrec :: forall coef. Show coef => Int -> SingPoly coef -> ShowS
Show)

instance (Ord coef, Num coef, Pretty coef) => Pretty (SingPoly coef) where
  pretty :: forall ann. SingPoly coef -> Doc ann
pretty (SingPoly Vector coef
v) =
    case forall a. (a -> Bool) -> Vector a -> Maybe Int
V.findIndex (forall a. Eq a => a -> a -> Bool
/= coef
0) Vector coef
v of
      Maybe Int
Nothing -> forall a ann. Pretty a => a -> Doc ann
pretty String
"0"
      Just Int
j -> forall {ann}. Int -> Doc ann
go (forall a. Vector a -> Int
V.length Vector coef
v forall a. Num a => a -> a -> a
- Int
1)
        where ppc :: a -> Doc ann
ppc a
c | a
c forall a. Ord a => a -> a -> Bool
< a
0 = forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty a
c)
                    | Bool
otherwise = forall a ann. Pretty a => a -> Doc ann
pretty a
c

              ppi :: a -> Doc ann
ppi a
1 = forall a ann. Pretty a => a -> Doc ann
pretty String
"*x"
              ppi a
i = forall a ann. Pretty a => a -> Doc ann
pretty String
"*x^" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty a
i

              go :: Int -> Doc ann
go Int
0 = forall {a} {ann}. (Ord a, Num a, Pretty a) => a -> Doc ann
ppc (Vector coef
v forall a. Vector a -> Int -> a
V.! Int
0)
              go Int
i | seq :: forall a b. a -> b -> b
seq Int
i Bool
False = forall a. HasCallStack => String -> a
error String
"pretty SingPoly"
                   | Int
i forall a. Eq a => a -> a -> Bool
== Int
j = forall {a} {ann}. (Ord a, Num a, Pretty a) => a -> Doc ann
ppc (Vector coef
v forall a. Vector a -> Int -> a
V.! Int
i) forall a. Semigroup a => a -> a -> a
<> forall {a} {ann}. (Eq a, Num a, Pretty a) => a -> Doc ann
ppi Int
i
                   | Vector coef
v forall a. Vector a -> Int -> a
V.! Int
i forall a. Eq a => a -> a -> Bool
== coef
0 = Int -> Doc ann
go (Int
iforall a. Num a => a -> a -> a
-Int
1)
                   | Bool
otherwise = forall {a} {ann}. (Ord a, Num a, Pretty a) => a -> Doc ann
ppc (Vector coef
v forall a. Vector a -> Int -> a
V.! Int
i) forall a. Semigroup a => a -> a -> a
<> forall {a} {ann}. (Eq a, Num a, Pretty a) => a -> Doc ann
ppi Int
i forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty String
"+" forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
go (Int
iforall a. Num a => a -> a -> a
-Int
1)

fromList :: [c] -> SingPoly c
fromList :: forall c. [c] -> SingPoly c
fromList = forall coef. Vector coef -> SingPoly coef
SingPoly forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Vector a
V.fromList

-- | Create a polyomial from a map from powers to coefficient.
fromMap :: (Eq c, Num c) => Map.Map Int c -> SingPoly c
fromMap :: forall c. (Eq c, Num c) => Map Int c -> SingPoly c
fromMap Map Int c
m0 = forall coef. Vector coef -> SingPoly coef
SingPoly (forall a. Int -> (Int -> a) -> Vector a
V.generate (Int
nforall a. Num a => a -> a -> a
+Int
1) Int -> c
f)
  where m :: Map Int c
m = forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (forall a. Eq a => a -> a -> Bool
/= c
0) Map Int c
m0
        (Int
n,c
_) = forall k a. Map k a -> (k, a)
Map.findMax Map Int c
m
        f :: Int -> c
f Int
i   = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault c
0 Int
i Map Int c
m

-- | Parse a positive monomial
pos_mono :: Integral c => Atto.Parser (c, Int)
pos_mono :: forall c. Integral c => Parser (c, Int)
pos_mono = (,) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Integral a => Parser a
Atto.decimal forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Parser Int
times_x
  where times_x :: Atto.Parser Int
        times_x :: Parser Int
times_x = (Char -> Parser Char
Atto.char Char
'*' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Char -> Parser Char
Atto.char Char
'x' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser Int
expon) forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Int
0

        -- Parse explicit exponent or return 1
        expon :: Atto.Parser Int
        expon :: Parser Int
expon = (Char -> Parser Char
Atto.char Char
'^' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall a. Integral a => Parser a
Atto.decimal) forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Int
1


-- | Parses a monomial and returns the coefficient and power
mono :: Integral c => Atto.Parser (c, Int)
mono :: forall c. Integral c => Parser (c, Int)
mono = forall a. Parser a -> Parser a
atto_paren (Char -> Parser Char
Atto.char Char
'-' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> (forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over forall s t a b. Field1 s t a b => Lens s t a b
_1 forall a. Num a => a -> a
negate forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall c. Integral c => Parser (c, Int)
pos_mono))
     forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> forall c. Integral c => Parser (c, Int)
pos_mono

parseYicesPoly :: Integral c => Atto.Parser (SingPoly c)
parseYicesPoly :: forall c. Integral c => Parser (SingPoly c)
parseYicesPoly = do
     (c
c,Int
p) <- forall c. Integral c => Parser (c, Int)
mono
     forall {c}. Integral c => Map Int c -> Parser Text (SingPoly c)
go (forall k a. k -> a -> Map k a
Map.singleton Int
p c
c)
  where go :: Map Int c -> Parser Text (SingPoly c)
go Map Int c
m = Map Int c -> Parser Text (SingPoly c)
next Map Int c
m forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall c. (Eq c, Num c) => Map Int c -> SingPoly c
fromMap Map Int c
m)
        next :: Map Int c -> Parser Text (SingPoly c)
next Map Int c
m = seq :: forall a b. a -> b -> b
seq Map Int c
m forall a b. (a -> b) -> a -> b
$ do
          Char
_ <- Char -> Parser Char
Atto.char Char
' ' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Char -> Parser Char
Atto.char Char
'+' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Char -> Parser Char
Atto.char Char
' '
          (c
c,Int
p) <- forall c. Integral c => Parser (c, Int)
mono
          Map Int c -> Parser Text (SingPoly c)
go (forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith forall a. Num a => a -> a -> a
(+) Int
p c
c Map Int c
m)


-- | Evaluate polynomial at a specific value.
--
-- Note that due to rounding, the result may not be exact when using
-- finite precision arithmetic.
eval :: forall c . Num c => SingPoly c -> c -> c
eval :: forall c. Num c => SingPoly c -> c -> c
eval (SingPoly Vector c
v) c
c = Int -> c -> c -> c
f Int
0 c
1 c
0
  where -- f takes an index, the current power, and the current sum.
        f :: Int -> c -> c -> c
        f :: Int -> c -> c -> c
f Int
i c
p c
s
          | seq :: forall a b. a -> b -> b
seq c
p forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq c
s forall a b. (a -> b) -> a -> b
$ Bool
False = forall a. HasCallStack => String -> a
error String
"internal error: Poly.eval"
          | Int
i forall a. Ord a => a -> a -> Bool
< forall a. Vector a -> Int
V.length Vector c
v = Int -> c -> c -> c
f (Int
iforall a. Num a => a -> a -> a
+Int
1) (c
p forall a. Num a => a -> a -> a
* c
c) (c
s forall a. Num a => a -> a -> a
+ c
p forall a. Num a => a -> a -> a
* (Vector c
v forall a. Vector a -> Int -> a
V.! Int
i))
          | Bool
otherwise = c
s

data Root c = Root { forall c. Root c -> SingPoly c
rootPoly :: !(SingPoly c)
                   , forall c. Root c -> c
rootLbound :: !c
                   , forall c. Root c -> c
rootUbound :: !c
                   }
  deriving (Int -> Root c -> ShowS
forall c. Show c => Int -> Root c -> ShowS
forall c. Show c => [Root c] -> ShowS
forall c. Show c => Root c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Root c] -> ShowS
$cshowList :: forall c. Show c => [Root c] -> ShowS
show :: Root c -> String
$cshow :: forall c. Show c => Root c -> String
showsPrec :: Int -> Root c -> ShowS
$cshowsPrec :: forall c. Show c => Int -> Root c -> ShowS
Show)

-- | Construct a root from a rational constant
rootFromRational :: Num c => c -> Root c
rootFromRational :: forall c. Num c => c -> Root c
rootFromRational c
r = Root { rootPoly :: SingPoly c
rootPoly = forall c. [c] -> SingPoly c
fromList [ forall a. Num a => a -> a
negate c
r, c
1 ]
                          , rootLbound :: c
rootLbound = c
r
                          , rootUbound :: c
rootUbound = c
r
                          }

instance (Ord c, Num c, Pretty c) => Pretty (Root c) where
  pretty :: forall ann. Root c -> Doc ann
pretty (Root SingPoly c
p c
l c
u) = forall ann. Doc ann
langle forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty SingPoly c
p forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
comma forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
bounds forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
rangle
    where bounds :: Doc ann
bounds = forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty c
l forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
comma forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty c
u)

-- | This either returns the root exactly, or it computes the closest double
-- precision approximation of the root.
--
-- Underneath the hood, this uses rational arithmetic to guarantee precision,
-- so this operation is relatively slow.  However, it is guaranteed to provide
-- an exact answer.
--
-- If performance is a concern, there are faster algorithms for computing this.
approximate :: Root Rational -> Rational
approximate :: Root Rational -> Rational
approximate Root Rational
r
    | Rational
l0 forall a. Eq a => a -> a -> Bool
== Rational
u0       = Rational
l0
    | Rational
init_lval forall a. Eq a => a -> a -> Bool
== Rational
0 = Rational
l0
    | Rational
init_uval forall a. Eq a => a -> a -> Bool
== Rational
0 = Rational
u0
    | Rational
init_lval forall a. Ord a => a -> a -> Bool
< Rational
0 Bool -> Bool -> Bool
&& Rational
init_uval forall a. Ord a => a -> a -> Bool
> Rational
0 = Double -> Double -> Rational
bisect (forall a. Fractional a => Rational -> a
fromRational Rational
l0) (forall a. Fractional a => Rational -> a
fromRational Rational
u0)
    | Rational
init_lval forall a. Ord a => a -> a -> Bool
> Rational
0 Bool -> Bool -> Bool
&& Rational
init_uval forall a. Ord a => a -> a -> Bool
< Rational
0 = Double -> Double -> Rational
bisect (forall a. Fractional a => Rational -> a
fromRational Rational
u0) (forall a. Fractional a => Rational -> a
fromRational Rational
l0)
    | Bool
otherwise = forall a. HasCallStack => String -> a
error String
"Closest root given bad root."
  where p_rat :: SingPoly Rational
p_rat = forall c. Root c -> SingPoly c
rootPoly Root Rational
r
        l0 :: Rational
l0 = forall c. Root c -> c
rootLbound Root Rational
r
        u0 :: Rational
u0 = forall c. Root c -> c
rootUbound Root Rational
r

        init_lval :: Rational
init_lval = forall c. Num c => SingPoly c -> c -> c
eval SingPoly Rational
p_rat Rational
l0
        init_uval :: Rational
init_uval = forall c. Num c => SingPoly c -> c -> c
eval SingPoly Rational
p_rat Rational
u0

        -- bisect takes a value that evaluates to a negative value under the 'p',
        -- and a value that evalautes to a positive value, and runs until it
        -- converges.
        bisect :: Double -> Double -> Rational
        bisect :: Double -> Double -> Rational
bisect Double
l Double
u   -- Stop if mid point is at bound.
                   | Double
m forall a. Eq a => a -> a -> Bool
== Double
l Bool -> Bool -> Bool
|| Double
m forall a. Eq a => a -> a -> Bool
== Double
u = forall a. Real a => a -> Rational
toRational forall a b. (a -> b) -> a -> b
$
                      -- Pick whichever bound is cl oser to root.
                      if Rational
l_val forall a. Ord a => a -> a -> Bool
<= Rational
u_val then Double
l else Double
u
                   | Rational
m_val forall a. Eq a => a -> a -> Bool
== Rational
0 = forall a. Real a => a -> Rational
toRational Double
m -- Stop if mid point is exact root.
                   | Rational
m_val forall a. Ord a => a -> a -> Bool
<  Rational
0 = Double -> Double -> Rational
bisect Double
m Double
u -- Use mid point as new lower bound
                   | Bool
otherwise  = Double -> Double -> Rational
bisect Double
l Double
m -- Use mid point as new upper bound.
          where m :: Double
m = (Double
l forall a. Num a => a -> a -> a
+ Double
u) forall a. Fractional a => a -> a -> a
/ Double
2
                m_val :: Rational
m_val = forall c. Num c => SingPoly c -> c -> c
eval SingPoly Rational
p_rat (forall a. Real a => a -> Rational
toRational Double
m)
                l_val :: Rational
l_val = forall a. Num a => a -> a
abs (forall c. Num c => SingPoly c -> c -> c
eval SingPoly Rational
p_rat (forall a. Real a => a -> Rational
toRational Double
l))
                u_val :: Rational
u_val = forall a. Num a => a -> a
abs (forall c. Num c => SingPoly c -> c -> c
eval SingPoly Rational
p_rat (forall a. Real a => a -> Rational
toRational Double
u))


atto_pair :: (a -> b -> r) -> Atto.Parser a -> Atto.Parser b -> Atto.Parser r
atto_pair :: forall a b r. (a -> b -> r) -> Parser a -> Parser b -> Parser r
atto_pair a -> b -> r
f Parser a
x Parser b
y = a -> b -> r
f forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser a
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (Char -> Parser Char
Atto.char Char
',' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Char -> Parser Char
Atto.char Char
' ' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> Parser b
y)

atto_sdecimal :: Integral c => Atto.Parser c
atto_sdecimal :: forall a. Integral a => Parser a
atto_sdecimal = Char -> Parser Char
Atto.char Char
'-' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> (forall a. Num a => a -> a
negate forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Integral a => Parser a
Atto.decimal)
              forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> forall a. Integral a => Parser a
Atto.decimal

atto_rational :: Integral c => Atto.Parser (Ratio c)
atto_rational :: forall c. Integral c => Parser (Ratio c)
atto_rational = forall a. Integral a => a -> a -> Ratio a
(%) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Integral a => Parser a
atto_sdecimal forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Parser Text c
denom
  where denom :: Parser Text c
denom = (Char -> Parser Char
Atto.char Char
'/' forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall a. Integral a => Parser a
Atto.decimal) forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure c
1

parseYicesRoot :: Atto.Parser (Root Rational)
parseYicesRoot :: Parser (Root Rational)
parseYicesRoot = forall a. Parser a -> Parser a
atto_angle (forall a b r. (a -> b -> r) -> Parser a -> Parser b -> Parser r
atto_pair forall c. SingPoly c -> (c, c) -> Root c
mkRoot (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Num a => Integer -> a
fromInteger forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall c. Integral c => Parser (SingPoly c)
parseYicesPoly) Parser (Rational, Rational)
parseBounds)
             forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> (forall c. Num c => c -> Root c
rootFromRational forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall c. Integral c => Parser (Ratio c)
atto_rational)
  where mkRoot :: SingPoly c -> (c, c) -> Root c
        mkRoot :: forall c. SingPoly c -> (c, c) -> Root c
mkRoot = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. SingPoly c -> c -> c -> Root c
Root
        parseBounds :: Atto.Parser (Rational, Rational)
        parseBounds :: Parser (Rational, Rational)
parseBounds = forall a. Parser a -> Parser a
atto_paren (forall a b r. (a -> b -> r) -> Parser a -> Parser b -> Parser r
atto_pair (,) forall c. Integral c => Parser (Ratio c)
atto_rational forall c. Integral c => Parser (Ratio c)
atto_rational)

-- | Convert text to a root
fromYicesText :: Text -> Maybe (Root Rational)
fromYicesText :: Text -> Maybe (Root Rational)
fromYicesText Text
t = forall {a}. IResult Text a -> Maybe a
resolve (forall a. Parser a -> Text -> Result a
Atto.parse Parser (Root Rational)
parseYicesRoot Text
t)
  where resolve :: IResult Text a -> Maybe a
resolve (Atto.Fail Text
_rem [String]
_ String
_msg) = forall a. Maybe a
Nothing
        resolve (Atto.Partial Text -> IResult Text a
f) =
          IResult Text a -> Maybe a
resolve (Text -> IResult Text a
f Text
Text.empty)
        resolve (Atto.Done Text
i a
r)
          | Text -> Bool
Text.null Text
i = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! a
r
          | Bool
otherwise = forall a. Maybe a
Nothing