module Test.Extrapolate.Speculation
( theoryAndReprConds
, Thy
, Expr
, classesFromSchemasAndVariables
)
where
import Data.Monoid ((<>))
import Test.LeanCheck ((\/))
import Test.Speculate.Engine (theoryAndRepresentativesFromAtoms, classesFromSchemasAndVariables)
import Test.Speculate.Reason (Thy)
import Test.Extrapolate.Utils
import Test.Extrapolate.Expr
theoryAndReprsFromPropAndAtoms :: Int -> (Expr -> Expr -> Bool) -> [[Expr]] -> (Thy,[[Expr]])
theoryAndReprsFromPropAndAtoms maxConditionSize (===) ess =
theoryAndRepresentativesFromAtoms
maxConditionSize compareExpr (const True) (===) ess
where
compareExpr :: Expr -> Expr -> Ordering
compareExpr = compareComplexity <> lexicompareBy cmp
e1 `cmp` e2 | arity e1 == 0 && arity e2 /= 0 = LT
e1 `cmp` e2 | arity e1 /= 0 && arity e2 == 0 = GT
e1 `cmp` e2 = compareIndex (concat ess) e1 e2 <> e1 `compare` e2
theoryAndReprExprs :: Int -> (Expr -> Expr -> Bool) -> [[Expr]] -> (Thy,[Expr])
theoryAndReprExprs maxConditionSize (===) =
(\(thy,ess) -> (thy, concat $ take maxConditionSize ess))
. theoryAndReprsFromPropAndAtoms maxConditionSize (===)
theoryAndReprConds :: Int -> (Expr -> Expr -> Bool) -> [[Expr]] -> (Thy, [Expr])
theoryAndReprConds maxConditionSize (===) ess = (thy, filter (\c -> typ c == boolTy) es)
where
(thy,es) = theoryAndReprExprs maxConditionSize (===) ess