-- |
-- Module      : Test.Speculate.Report
-- Copyright   : (c) 2016-2024 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of Speculate.
--
-- Report Speculate results.
module Test.Speculate.Report
  ( report
  )
where

import Test.Speculate.Expr
import Test.Speculate.Reason
import Test.Speculate.SemiReason
import Test.Speculate.CondReason
import Test.Speculate.Engine
import Test.Speculate.Sanity
import Test.Speculate.Args
import Test.Speculate.Utils
import Test.Speculate.Utils.Colour
import Test.Speculate.Pretty

import Data.Ratio ((%))
import Control.Monad (when,unless)
import Test.LeanCheck.Utils ((&&&&))

report :: Args -> IO ()
report :: Args -> IO ()
report args :: Args
args@Args {maxSize :: Args -> Int
maxSize = Int
sz, maxTests :: Args -> Int
maxTests = Int
n} = do
  let ti :: Instances
ti = Args -> Instances
computeInstances Args
args
  let ats :: [TypeRep]
ats = Args -> [TypeRep]
types Args
args
  let dss :: [Instances]
dss = Args -> [Instances]
atoms Args
args
  let (Thy
thy,[Instances]
ess) = (Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> Int
-> [Instances]
-> (Thy, [Instances])
theoryAndRepresentativesFromAtomsKeeping (Args -> Expr -> Bool
keepExpr Args
args) (Args -> Bool -> Bool
timeout Args
args (Bool -> Bool) -> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.: Instances -> Int -> Expr -> Expr -> Bool
equal Instances
ti Int
n) Int
sz [Instances]
dss
  let es :: Instances
es = Int -> [Instances] -> Instances
forall a. Int -> [[a]] -> [a]
uptoT Int
sz [Instances]
ess
  Args -> IO ()
putArgs Args
args
  -- TODO: somehow show the tail of dss, maybe use "..."
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
showConstants Args
args) (IO () -> IO ()) -> ([String] -> IO ()) -> [String] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> ([String] -> String) -> [String] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ (Expr -> String) -> Instances -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> String
forall a. Show a => a -> String
show ([Instances] -> Instances
forall a. HasCallStack => [a] -> a
head [Instances]
dss)
  Instances -> [TypeRep] -> IO ()
warnMissingInstances Instances
ti [TypeRep]
ats
  let ies :: [String]
ies = Instances -> Int -> [TypeRep] -> [String]
instanceErrors Instances
ti Int
n [TypeRep]
ats
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
ies) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    let pref :: String
pref | Args -> Bool
force Args
args = String
"Warning: "
             | Bool
otherwise  = String
"Error: "
    String -> IO ()
putStrLn (String -> IO ()) -> ([String] -> String) -> [String] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
pref String -> String -> String
forall a. [a] -> [a] -> [a]
++) ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ [String]
ies
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Args -> Bool
force Args
args) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      String -> IO ()
putStrLn String
"There were instance errors, refusing to run."
      String -> IO ()
putStrLn String
"Use `--force` or `args{force=true}` to ignore instance errors."
      String -> IO ()
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"exiting"
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
showTheory Args
args)       (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Thy -> String
showThy Thy
thy
  let shy :: Shy
shy = Instances -> Int -> Int -> Thy -> Instances -> Shy
semiTheoryFromThyAndReps Instances
ti Int
n (Args -> Int
maxVars Args
args) Thy
thy
          (Instances -> Shy) -> Instances -> Shy
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> Instances -> Instances
forall a. (a -> Bool) -> [a] -> [a]
filter (\Expr
e -> Expr -> Int
size Expr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Args -> Int
computeMaxSemiSize Args
args) Instances
es
  let chy :: Chy
chy = Instances -> Int -> Int -> Int -> Thy -> Instances -> Chy
conditionalTheoryFromThyAndReps Instances
ti Int
n (Args -> Int
maxVars Args
args) (Args -> Int
computeMaxCondSize Args
args) Thy
thy Instances
es
  let equations :: [Equation]
equations     = (Equation -> Bool) -> Instances -> Thy -> [Equation]
finalEquations     (Args -> Equation -> Bool
shouldShowEquation Args
args) Instances
ti                          Thy
thy
  let semiEquations :: [Equation]
semiEquations = (Equation -> Bool)
-> Instances -> (Expr -> Expr -> Bool) -> Shy -> [Equation]
finalSemiEquations (Args -> Equation -> Bool
shouldShowEquation Args
args) Instances
ti (Thy -> Expr -> Expr -> Bool
equivalentInstance Thy
thy) Shy
shy
  let condEquations :: [(Expr, Expr, Expr)]
condEquations = ((Expr, Expr, Expr) -> Bool) -> Chy -> [(Expr, Expr, Expr)]
finalCondEquations (Args -> (Expr, Expr, Expr) -> Bool
shouldShowConditionalEquation Args
args)                  Chy
chy
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
showEquations Args
args)        (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [Equation] -> String
prettyEquations [Equation]
equations
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
showSemiequations Args
args)    (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [Equation] -> String
prettySemiEquations [Equation]
semiEquations
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
reallyShowConditions Args
args) (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [(Expr, Expr, Expr)] -> String
prettyCondEquations [(Expr, Expr, Expr)]
condEquations
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
showCounts Args
args) (IO () -> IO ()) -> ([String] -> IO ()) -> [String] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> ([String] -> String) -> [String] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines
    ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$  [ String
"#-equations      = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Equation] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Equation]
equations)     | Args -> Bool
showEquations        Args
args ]
    [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"#-semi-equations = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Equation] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Equation]
semiEquations) | Args -> Bool
showSemiequations    Args
args ]
    [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"#-cond-equations = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([(Expr, Expr, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Expr, Expr, Expr)]
condEquations) | Args -> Bool
reallyShowConditions Args
args ]
  Instances -> Int -> [Int] -> Thy -> Instances -> IO ()
reportClassesFor Instances
ti Int
n (Args -> [Int]
showClassesFor Args
args) Thy
thy Instances
es
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
showDot Args
args) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
    Instances
-> [String] -> Bool -> Int -> Int -> Thy -> Instances -> IO ()
reportDot Instances
ti (Args -> [String]
onlyTypes Args
args) (Args -> Bool
quietDot Args
args) (Args -> Int
maxVars Args
args) Int
n Thy
thy Instances
es

putArgs :: Args -> IO ()
putArgs :: Args -> IO ()
putArgs Args
args = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
showArgs Args
args) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  let sz :: Int
sz = Args -> Int
maxSize Args
args
  let isz :: Int
isz = Args -> Int
computeMaxSemiSize Args
args
  let csz :: Int
csz = Args -> Int
computeMaxCondSize Args
args
  String -> Int -> IO ()
forall a. Show a => String -> a -> IO ()
putOpt String
"max expr size" Int
sz
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
isz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
sz) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> IO ()
forall a. Show a => String -> a -> IO ()
putOpt String
"  |- on ineqs" Int
isz
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
csz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
sz) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> IO ()
forall a. Show a => String -> a -> IO ()
putOpt String
"  |- on conds"  Int
csz
  case Args -> Maybe Int
maxDepth Args
args of
    Maybe Int
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Int
d  -> String -> String -> IO ()
forall a. Show a => String -> a -> IO ()
putOpt String
"max expr depth" (Int -> String
forall a. Show a => a -> String
show Int
d)
  String -> Int -> IO ()
forall a. Show a => String -> a -> IO ()
putOpt String
"max  #-tests" (Args -> Int
maxTests Args
args)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
showConditions Args
args) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
    String -> Int -> String -> IO ()
forall a. Show a => String -> a -> String -> IO ()
putOptSuffix String
"min  #-tests"  (Args -> Int -> Int
minTests Args
args (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Args -> Int
maxTests Args
args) String
"  (to consider p ==> q true)"
  String -> Int -> String -> IO ()
forall a. Show a => String -> a -> String -> IO ()
putOptSuffix String
"max  #-vars" (Args -> Int
maxVars Args
args) String
"  (for inequational and conditional laws)"
  case Args -> Maybe Double
evalTimeout Args
args of
    Maybe Double
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Double
t  -> String -> Double -> String -> IO ()
forall a. Show a => String -> a -> String -> IO ()
putOptSuffix String
"eval timeout" Double
t String
"s"
  String -> IO ()
putStrLn String
""
  where
  putOpt :: Show a => String -> a -> IO ()
  putOpt :: forall a. Show a => String -> a -> IO ()
putOpt  String
s a
x   = String -> a -> String -> IO ()
forall a. Show a => String -> a -> String -> IO ()
putOptSuffix String
s a
x String
""
  putOptSuffix :: Show a => String -> a -> String -> IO ()
  putOptSuffix :: forall a. Show a => String -> a -> String -> IO ()
putOptSuffix String
s a
x String
p = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
alignLeft Int
14 String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
alignRight Int
4 (a -> String
forall a. Show a => a -> String
show a
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
p

warnMissingInstances :: Instances -> [TypeRep] -> IO ()
warnMissingInstances :: Instances -> [TypeRep] -> IO ()
warnMissingInstances Instances
is [TypeRep]
ts = [String] -> IO ()
putLines
  ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$  [String
"Warning: no Listable instance for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show TypeRep
t String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
", variables of this type will not be considered"
     | TypeRep
t <- [TypeRep]
ts, Bool -> Bool
not (TypeRep -> Bool
isFunTy TypeRep
t), Bool -> Bool
not (Instances -> TypeRep -> Bool
isListableT Instances
is TypeRep
t)]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"Warning: no Eq instance for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show TypeRep
t String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
", equations of this type will not be considered"
     | TypeRep
t <- [TypeRep]
ts, Bool -> Bool
not (TypeRep -> Bool
isFunTy TypeRep
t), Bool -> Bool
not (Instances -> TypeRep -> Bool
isEqT Instances
is TypeRep
t)]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"Warning: no Ord instance for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show TypeRep
t String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
", inequations of this type will not be considered"
     | TypeRep
t <- [TypeRep]
ts, Bool -> Bool
not (TypeRep -> Bool
isFunTy TypeRep
t), Bool -> Bool
not (Instances -> TypeRep -> Bool
isOrdT Instances
is TypeRep
t)]

reportClassesFor :: Instances -> Int -> [Int] -> Thy -> [Expr] -> IO ()
reportClassesFor :: Instances -> Int -> [Int] -> Thy -> Instances -> IO ()
reportClassesFor Instances
ti Int
nTests [Int]
nVarss Thy
thy Instances
res = do
  (Int -> IO ()) -> [Int] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn (String -> IO ()) -> (Int -> String) -> Int -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines ([String] -> String) -> (Int -> [String]) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> String) -> Instances -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> String
forall a. Show a => a -> String
show (Instances -> [String]) -> (Int -> Instances) -> Int -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Instances
r) [Int]
nVarss
  (Int -> IO ()) -> [Int] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Int -> IO ()
pn [Int]
nVarss
  where
  pn :: Int -> IO ()
pn Int
0 = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Number of Eq schema classes: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Instances -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Instances -> Int) -> Instances -> Int
forall a b. (a -> b) -> a -> b
$ Int -> Instances
r Int
0)
  pn Int
n = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Number of Eq " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"-var classes: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Instances -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Instances -> Int) -> Instances -> Int
forall a b. (a -> b) -> a -> b
$ Int -> Instances
r Int
n)
  r :: Int -> Instances
r Int
0 = (Expr -> Bool) -> Instances -> Instances
forall a. (a -> Bool) -> [a] -> [a]
filter (Instances -> Expr -> Bool
isEq Instances
ti) Instances
res
  r Int
n = Instances -> Int -> Int -> Thy -> Instances -> Instances
distinctFromSchemas Instances
ti Int
nTests Int
n Thy
thy (Int -> Instances
r Int
0)

reportDot :: Instances -> [String] -> Bool -> Int -> Int -> Thy -> [Expr] -> IO ()
reportDot :: Instances
-> [String] -> Bool -> Int -> Int -> Thy -> Instances -> IO ()
reportDot Instances
ti [String]
onlyTypes Bool
quiet Int
nVars Int
n Thy
thy Instances
es = do
  let ces :: Instances
ces = Instances -> Int -> Int -> Thy -> Instances -> Instances
distinctFromSchemas Instances
ti Int
n Int
nVars Thy
thy
          (Instances -> Instances) -> Instances -> Instances
forall a b. (a -> b) -> a -> b
$ (if [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
onlyTypes
               then Instances -> Instances
forall a. a -> a
id
               else (Expr -> Bool) -> Instances -> Instances
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower) [String]
onlyTypes) (String -> Bool) -> (Expr -> String) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String) -> (Expr -> String) -> Expr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> String) -> (Expr -> TypeRep) -> Expr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> TypeRep
typ))
          (Instances -> Instances) -> Instances -> Instances
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> Instances -> Instances
forall a. (a -> Bool) -> [a] -> [a]
filter (Instances -> Expr -> Bool
isEqOrd Instances
ti) Instances
es
  let res :: [(Ratio Int, Expr)]
res = [(Instances -> Int -> Expr -> Ratio Int
trueRatio Instances
ti Int
n Expr
e, Expr
e) | Expr
e <- Instances
ces, Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep
boolTy]
  String -> IO ()
putStrLn String
"digraph G {"
  String -> IO ()
putStrLn String
"  rankdir = BT"
  String -> IO ()
putStrLn (String -> IO ()) -> (Instances -> String) -> Instances -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines
           ([String] -> String)
-> (Instances -> [String]) -> Instances -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> String) -> [Equation] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Equation -> String
showExprEdge
           ([Equation] -> [String])
-> (Instances -> [Equation]) -> Instances -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr -> Bool) -> Instances -> [Equation]
forall a. (a -> a -> Bool) -> [a] -> [(a, a)]
psortBy (Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
forall a b. (a -> b -> Bool) -> (a -> b -> Bool) -> a -> b -> Bool
&&&& Instances -> Int -> Expr -> Expr -> Bool
lessOrEqual Instances
ti Int
n)
           (Instances -> IO ()) -> Instances -> IO ()
forall a b. (a -> b) -> a -> b
$ Instances
ces
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
quiet (IO () -> IO ())
-> ([(Ratio Int, Expr)] -> IO ()) -> [(Ratio Int, Expr)] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ())
-> ([(Ratio Int, Expr)] -> String) -> [(Ratio Int, Expr)] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines
           ([String] -> String)
-> ([(Ratio Int, Expr)] -> [String])
-> [(Ratio Int, Expr)]
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Ratio Int, Expr) -> String) -> [(Ratio Int, Expr)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(Ratio Int
r,Expr
e) -> Expr -> String
showExprNode Expr
e
                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" [style=filled, fillcolor = \""
                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ratio Int -> Ratio Int -> String
forall {a} {a}.
(Integral a, Integral a) =>
Ratio a -> Ratio a -> String
showNodeColour (Instances -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Expr -> Instances
nubVars Expr
e) Int -> Int -> Ratio Int
forall a. Integral a => a -> a -> Ratio a
% (Int
nVarsInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2)) Ratio Int
r
                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\"]")
           ([(Ratio Int, Expr)] -> [String])
-> ([(Ratio Int, Expr)] -> [(Ratio Int, Expr)])
-> [(Ratio Int, Expr)]
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Ratio Int, Expr) -> Bool)
-> [(Ratio Int, Expr)] -> [(Ratio Int, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Ratio Int
r,Expr
e) -> Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep
boolTy)
           ([(Ratio Int, Expr)] -> IO ()) -> [(Ratio Int, Expr)] -> IO ()
forall a b. (a -> b) -> a -> b
$ [(Ratio Int, Expr)]
res
  String -> IO ()
putStrLn (String -> IO ())
-> ([(Ratio Int, Expr)] -> String) -> [(Ratio Int, Expr)] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines
           ([String] -> String)
-> ([(Ratio Int, Expr)] -> [String])
-> [(Ratio Int, Expr)]
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> String) -> Instances -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\Expr
e -> String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExprNode Expr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" [shape=box]")
           (Instances -> [String])
-> ([(Ratio Int, Expr)] -> Instances)
-> [(Ratio Int, Expr)]
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> Instances -> Instances
forall a. (a -> Bool) -> [a] -> [a]
filter Expr -> Bool
isEquation
           (Instances -> Instances)
-> ([(Ratio Int, Expr)] -> Instances)
-> [(Ratio Int, Expr)]
-> Instances
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Ratio Int, Expr) -> Expr) -> [(Ratio Int, Expr)] -> Instances
forall a b. (a -> b) -> [a] -> [b]
map (Ratio Int, Expr) -> Expr
forall a b. (a, b) -> b
snd
           ([(Ratio Int, Expr)] -> IO ()) -> [(Ratio Int, Expr)] -> IO ()
forall a b. (a -> b) -> a -> b
$ [(Ratio Int, Expr)]
res
--let rs = sort $ map fst ress
--putStrLn . unlines $ zipWith (\r1 r2 -> "\"" ++ show r1 ++ "\" -> \"" ++ show r2 ++ "\"") rs (tail rs)
--putStrLn . unlines $ map showRank $ classifySndByFst res
  String -> IO ()
putStrLn String
"}"
  where
--showRank (r,es) = "  { rank = same; " ++ "\"" ++ show r ++ "\""
--               ++ intercalate "; " (map showExprNode es)
--               ++ " }"
  showExprEdge :: Equation -> String
showExprEdge (Expr
e1,Expr
e2) = String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExprNode Expr
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExprNode Expr
e2
  showExprNode :: Expr -> String
showExprNode Expr
e
    | Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep
boolTy Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
quiet = let tre :: Ratio Int
tre = Instances -> Int -> Expr -> Ratio Int
trueRatio Instances
ti Int
n Expr
e
                                     in String
"\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr Expr
e
                                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ratio Int -> String
forall a. (Integral a, Show a) => Ratio a -> String
showRatio Ratio Int
tre
                                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Ratio Int -> Int
forall a. Integral a => Ratio a -> a
percent Ratio Int
tre) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"%\""
    | Bool
otherwise = String
"\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr Expr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\""
  showNodeColour :: Ratio a -> Ratio a -> String
showNodeColour Ratio a
varRatio Ratio a
trueRatio =
    Colour -> String
showRGB (Colour -> String) -> Colour -> String
forall a b. (a -> b) -> a -> b
$ Rational -> Rational -> Rational -> Colour
fromHSV (Colour -> Rational
hue0 Colour
blue) (Rational -> Rational
forall a. Integral a => Ratio a -> Ratio a
frac (Rational -> Rational) -> Rational -> Rational
forall a b. (a -> b) -> a -> b
$ Ratio a -> Rational
forall a b. (Integral a, Integral b) => Ratio a -> Ratio b
coerceRatio Ratio a
varRatio) Rational
1
        Colour -> Colour -> Colour
`mix` Rational -> Rational -> Rational -> Colour
fromHSV (Colour -> Rational
hue0 Colour
orange) (Rational
1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational -> Rational
forall a. Integral a => Ratio a -> Ratio a
frac (Ratio a -> Rational
forall a b. (Integral a, Integral b) => Ratio a -> Ratio b
coerceRatio Ratio a
trueRatio)) Rational
1
        Colour -> Colour -> Colour
`mix` Colour
white