-- |
-- Module      : Conjure.Engine
-- Copyright   : (c) 2021-2025 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- An internal module of "Conjure",
-- a library for Conjuring function implementations
-- from tests or partial definitions.
-- (a.k.a.: functional inductive programming)
{-# LANGUAGE CPP, RecordWildCards, TupleSections #-}
module Conjure.Engine
  ( conjure
  , conjureFromSpec
  , conjure0
  , Results(..)
  , conjpure
  , conjpureFromSpec
  , conjpure0
  , candidateExprs
  , candidateDefns

  -- * settings
  , maxTests
  , maxSize
  , target

  -- * Advanced settings
  , maxRecursions
  , maxEquationSize
  , maxSearchTests
  , maxDeconstructionSize
  , maxConstantSize
  , maxPatternSize
  , maxPatternDepth

  -- * Debug options
  , showCandidates
  , showTheory
  , singlePattern
  , showTests
  , showPatterns
  , showDeconstructions
  , carryOn

  -- * Pruning options
  , dontRewrite
  , dontRequireDescent
  , omitAssortedPruning
  , omitEarlyTests
  , dontCopyBindings
  , nonAtomicNumbers
  , uniqueCandidates

  -- * other modules
  , module Data.Express
  , module Data.Express.Fixtures
  , module Conjure.Reason
  )
where

import Control.Monad (when)

import Data.Express
import Data.Express.Fixtures hiding ((-==-))

import Test.LeanCheck
import Test.LeanCheck.Tiers
import Test.LeanCheck.Error (errorToFalse)

import Conjure.Expr
import Conjure.Conjurable
import Conjure.Ingredient
import Conjure.Defn
import Conjure.Defn.Redundancy
import Conjure.Defn.Test
import Conjure.Red
import Conjure.Reason
import Conjure.Settings

import System.CPUTime (getCPUTime)


-- | Conjures an implementation of a partially defined function.
--
-- Takes a 'String' with the name of a function,
-- a partially-defined function from a conjurable type,
-- and a list of building blocks encoded as 'Expr's.
--
-- For example, given:
--
-- > factorial :: Int -> Int
-- > factorial 2  =  2
-- > factorial 3  =  6
-- > factorial 4  =  24
-- >
-- > ingredients :: [Ingredient]
-- > ingredients  =
-- >   [ con (0::Int)
-- >   , con (1::Int)
-- >   , fun "+" ((+) :: Int -> Int -> Int)
-- >   , fun "*" ((*) :: Int -> Int -> Int)
-- >   , fun "-" ((-) :: Int -> Int -> Int)
-- >   ]
--
-- The 'conjure' function does the following:
--
-- > > conjure "factorial" factorial ingredients
-- > factorial :: Int -> Int
-- > -- 0.1s, testing 4 combinations of argument values
-- > -- 0.8s, pruning with 27/65 rules
-- > -- ...  ...  ...  ...  ...  ...
-- > -- 0.9s, 35 candidates of size 6
-- > -- 0.9s, 167 candidates of size 7
-- > -- 0.9s, tested 95 candidates
-- > factorial 0  =  1
-- > factorial x  =  x * factorial (x - 1)
--
-- The ingredients list is defined with 'con' and 'fun'.
conjure :: Conjurable f => String -> f -> [Ingredient] -> IO ()
conjure :: forall f. Conjurable f => String -> f -> [Ingredient] -> IO ()
conjure String
nm f
f  =  String -> f -> (f -> Bool) -> [Ingredient] -> IO ()
forall f.
Conjurable f =>
String -> f -> (f -> Bool) -> [Ingredient] -> IO ()
conjure0 String
nm f
f (Bool -> f -> Bool
forall a b. a -> b -> a
const Bool
True)


-- | Conjures an implementation from a function specification.
--
-- This function works like 'conjure' but instead of receiving a partial definition
-- it receives a boolean filter / property about the function.
--
-- For example, given:
--
-- > squareSpec :: (Int -> Int) -> Bool
-- > squareSpec square  =  square 0 == 0
-- >                    && square 1 == 1
-- >                    && square 2 == 4
--
-- Then:
--
-- > > conjureFromSpec "square" squareSpec [fun "*" ((*) :: Int -> Int -> Int)]
-- > square :: Int -> Int
-- > -- 0.1s, pruning with 2/6 rules
-- > -- 0.1s, 1 candidates of size 1
-- > -- 0.1s, 0 candidates of size 2
-- > -- 0.1s, 1 candidates of size 3
-- > -- 0.1s, tested 2 candidates
-- > square x  =  x * x
--
-- This allows users to specify QuickCheck-style properties,
-- here is an example using LeanCheck:
--
-- > import Test.LeanCheck (holds, exists)
-- >
-- > squarePropertySpec :: (Int -> Int) -> Bool
-- > squarePropertySpec square  =  and
-- >   [ holds n $ \x -> square x >= x
-- >   , holds n $ \x -> square x >= 0
-- >   , exists n $ \x -> square x > x
-- >   ]  where  n = 60
conjureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Ingredient] -> IO ()
conjureFromSpec :: forall f.
Conjurable f =>
String -> (f -> Bool) -> [Ingredient] -> IO ()
conjureFromSpec String
nm f -> Bool
p  =  String -> f -> (f -> Bool) -> [Ingredient] -> IO ()
forall f.
Conjurable f =>
String -> f -> (f -> Bool) -> [Ingredient] -> IO ()
conjure0 String
nm f
forall a. HasCallStack => a
undefined f -> Bool
p


-- | Synthesizes an implementation from both a partial definition and a
--   function specification.
--
--   This works like the functions 'conjure' and 'conjureFromSpec' combined.
conjure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Ingredient] -> IO ()
conjure0 :: forall f.
Conjurable f =>
String -> f -> (f -> Bool) -> [Ingredient] -> IO ()
conjure0 String
nm f
f f -> Bool
p [Ingredient]
es  =  do
  -- the code section below became quite ugly with time and patches.
  -- it is still maintainable and readable as it is, but perhaps
  -- needs to be cleaned up and simplified
  Integer
t0 <- IO Integer
getCPUTime
  Expr -> IO ()
forall a. Show a => a -> IO ()
print (String -> f -> Expr
forall a. Typeable a => String -> a -> Expr
var ([String] -> String
forall a. HasCallStack => [a] -> a
head ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
nm) f
f)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Bndn] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bndn]
ts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    Integer -> String -> IO ()
putWithTimeSince Integer
t0 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"testing " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Bndn] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bndn]
ts) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" combinations of argument values"
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
showTests (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"{-"
      String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [Bndn] -> String
showDefn [Bndn]
ts
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-}"
  if [Bndn] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bndn]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& Bool -> Bool
errorToFalse (f -> Bool
p f
forall a. HasCallStack => a
undefined)
  then String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  =  error \"could not reify specification, suggestion: conjureFromSpec\"\n"
  else do
    Integer -> String -> IO ()
putWithTimeSince Integer
t0 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"pruning with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nRules String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nREs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" rules"
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
showTheory (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"{-"
      Thy -> IO ()
printThy Thy
thy
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-}"
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> ([Bndn] -> Bool) -> [Bndn] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bndn] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Bndn] -> Bool) -> [Bndn] -> Bool
forall a b. (a -> b) -> a -> b
$ Thy -> [Bndn]
invalid Thy
thy) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-- reasoning produced "
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Bndn] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> [Bndn]
invalid Thy
thy)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" incorrect properties,"
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" please re-run with more tests for faster results"
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
showTheory (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"{-"
        String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"invalid:"
        String -> IO ()
putStr   (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Bndn -> String) -> [Bndn] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Bndn -> String
showEq ([Bndn] -> [String]) -> [Bndn] -> [String]
forall a b. (a -> b) -> a -> b
$ Thy -> [Bndn]
invalid Thy
thy
        String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-}"
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
showPatterns (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
             ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Integer -> [String] -> String)
-> [Integer] -> [[String]] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Integer
i -> ((String
"-- allowed patterns of size " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n{-\n") String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> ([String] -> String) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"-}") (String -> String) -> ([String] -> String) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines) [Integer
1..]
             ([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ ([Bndn] -> String) -> [[[Bndn]]] -> [[String]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT [Bndn] -> String
showDefn
             ([[[Bndn]]] -> [[String]]) -> [[[Bndn]]] -> [[String]]
forall a b. (a -> b) -> a -> b
$ Results -> [[[Bndn]]]
patternss Results
results
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
showDeconstructions (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"{- List of allowed deconstructions:"
      String -> IO ()
putStr   (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Expr -> String) -> [Expr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> String
forall a. Show a => a -> String
show ([Expr] -> [String]) -> [Expr] -> [String]
forall a b. (a -> b) -> a -> b
$ Results -> [Expr]
deconstructions Results
results
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-}"
    Integer -> Int -> Int -> [([[Bndn]], [[Bndn]])] -> IO ()
pr Integer
t0 Int
1 Int
0 [([[Bndn]], [[Bndn]])]
rs
  where
  showEq :: Bndn -> String
showEq Bndn
eq  =  Expr -> String
showExpr (Bndn -> Expr
forall a b. (a, b) -> a
fst Bndn
eq) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" == " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr (Bndn -> Expr
forall a b. (a, b) -> b
snd Bndn
eq)
  pr :: Integer -> Int -> Int -> [([Defn], [Defn])] -> IO ()
  pr :: Integer -> Int -> Int -> [([[Bndn]], [[Bndn]])] -> IO ()
pr Integer
t0 Int
n Int
t []  =  do Integer -> String -> IO ()
putWithTimeSince Integer
t0 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"tested " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" candidates"
                      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  =  undefined  -- search exhausted\n"
  pr Integer
t0 Int
n Int
t (([[Bndn]]
is,[[Bndn]]
cs):[([[Bndn]], [[Bndn]])]
rs)  =  do
    let nc :: Int
nc  =  [[Bndn]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Bndn]]
cs
    Integer -> String -> IO ()
putWithTimeSince Integer
t0 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
nc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" candidates of size " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
showCandidates (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
      String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String
"{-"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ([Bndn] -> String) -> [[Bndn]] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map [Bndn] -> String
showDefn [[Bndn]]
cs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"-}"]
    case [[Bndn]]
is of
      []     ->  Integer -> Int -> Int -> [([[Bndn]], [[Bndn]])] -> IO ()
pr Integer
t0 (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nc) [([[Bndn]], [[Bndn]])]
rs
      ([Bndn]
_:[[Bndn]]
_)  ->  do Int -> [[Bndn]] -> [[Bndn]] -> IO ()
pr1 Int
t [[Bndn]]
is [[Bndn]]
cs
                    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
carryOn (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Integer -> Int -> Int -> [([[Bndn]], [[Bndn]])] -> IO ()
pr Integer
t0 (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nc) [([[Bndn]], [[Bndn]])]
rs
    where
    pr1 :: Int -> [[Bndn]] -> [[Bndn]] -> IO ()
pr1 Int
t [] [[Bndn]]
cs  =  () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    pr1 Int
t ([Bndn]
i:[[Bndn]]
is) [[Bndn]]
cs  =  do
      let ([[Bndn]]
cs',[[Bndn]]
cs'') = ([Bndn] -> Bool) -> [[Bndn]] -> ([[Bndn]], [[Bndn]])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break ([Bndn]
i[Bndn] -> [Bndn] -> Bool
forall a. Eq a => a -> a -> Bool
==) [[Bndn]]
cs
      let t' :: Int
t' = Int
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [[Bndn]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Bndn]]
cs' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
      Integer -> String -> IO ()
putWithTimeSince Integer
t0 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"tested " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
t' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" candidates"
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [Bndn] -> String
showDefn ([Bndn] -> String) -> [Bndn] -> String
forall a b. (a -> b) -> a -> b
$ Thy -> [Bndn] -> [Bndn]
normalizeDefn Thy
thy [Bndn]
i
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
carryOn (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> [[Bndn]] -> [[Bndn]] -> IO ()
pr1 Int
t' [[Bndn]]
is (Int -> [[Bndn]] -> [[Bndn]]
forall a. Int -> [a] -> [a]
drop Int
1 [[Bndn]]
cs'')
  rs :: [([[Bndn]], [[Bndn]])]
rs  =  [[[Bndn]]] -> [[[Bndn]]] -> [([[Bndn]], [[Bndn]])]
forall a b. [a] -> [b] -> [(a, b)]
zip [[[Bndn]]]
iss [[[Bndn]]]
css
  results :: Results
results  =  String -> f -> (f -> Bool) -> [Ingredient] -> Results
forall f.
Conjurable f =>
String -> f -> (f -> Bool) -> [Ingredient] -> Results
conjpure0 String
nm f
f f -> Bool
p [Ingredient]
es
  iss :: [[[Bndn]]]
iss  =  Results -> [[[Bndn]]]
implementationss Results
results
  css :: [[[Bndn]]]
css  =  Results -> [[[Bndn]]]
candidatess Results
results
  ts :: [Bndn]
ts   =  Results -> [Bndn]
bindings Results
results
  thy :: Thy
thy  =  Results -> Thy
theory Results
results
  nRules :: Int
nRules  =  [Bndn] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> [Bndn]
rules Thy
thy)
  nREs :: Int
nREs  =  [Bndn] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> [Bndn]
equations Thy
thy) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nRules
  -- we could avoid the following as most are called once
  -- but is nice to have a summary of which settings are used
  carryOn :: Bool
carryOn              =  [Ingredient] -> Bool
carryOnI [Ingredient]
es
  showTests :: Bool
showTests            =  [Ingredient] -> Bool
showTestsI [Ingredient]
es
  showTheory :: Bool
showTheory           =  [Ingredient] -> Bool
showTheoryI [Ingredient]
es
  showPatterns :: Bool
showPatterns         =  [Ingredient] -> Bool
showPatternsI [Ingredient]
es
  showCandidates :: Bool
showCandidates       =  [Ingredient] -> Bool
showCandidatesI [Ingredient]
es
  showDeconstructions :: Bool
showDeconstructions  =  [Ingredient] -> Bool
showDeconstructionsI [Ingredient]
es


-- | Results to the 'conjpure' family of functions.
-- This is for advanced users.
-- One is probably better-off using the 'conjure' family.
data Results = Results
  { Results -> [[[Bndn]]]
implementationss :: [[Defn]] -- ^ tiers of implementations
  , Results -> [[[Bndn]]]
candidatess :: [[Defn]]      -- ^ tiers of candidates
  , Results -> [Bndn]
bindings :: Defn             -- ^ test bindings used to verify candidates
  , Results -> Thy
theory :: Thy                -- ^ the underlying theory
  , Results -> [[[Bndn]]]
patternss :: [[Defn]]        -- ^ tiers of allowed patterns
  , Results -> [Expr]
deconstructions :: [Expr]    -- ^ the list of allowed deconstructions
  }


-- | Like 'conjure' but in the pure world.
--
-- The most important part of the result are the tiers of implementations
-- however results also include candidates, tests and the underlying theory.
conjpure :: Conjurable f => String -> f -> [Ingredient] -> Results
conjpure :: forall f. Conjurable f => String -> f -> [Ingredient] -> Results
conjpure String
nm f
f  =  String -> f -> (f -> Bool) -> [Ingredient] -> Results
forall f.
Conjurable f =>
String -> f -> (f -> Bool) -> [Ingredient] -> Results
conjpure0 String
nm f
f (Bool -> f -> Bool
forall a b. a -> b -> a
const Bool
True)

-- | Like 'conjureFromSpec' but in the pure world.  (cf. 'conjpure')
conjpureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Ingredient] -> Results
conjpureFromSpec :: forall f.
Conjurable f =>
String -> (f -> Bool) -> [Ingredient] -> Results
conjpureFromSpec String
nm f -> Bool
p  =  String -> f -> (f -> Bool) -> [Ingredient] -> Results
forall f.
Conjurable f =>
String -> f -> (f -> Bool) -> [Ingredient] -> Results
conjpure0 String
nm f
forall a. HasCallStack => a
undefined f -> Bool
p

-- | This is where the actual implementation resides.
-- The functions
-- 'conjpure', 'conjpureFromSpec', 'conjure' and 'conjureFromSpec'
-- all refer to this.
conjpure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Ingredient] -> Results
conjpure0 :: forall f.
Conjurable f =>
String -> f -> (f -> Bool) -> [Ingredient] -> Results
conjpure0 String
nm f
f f -> Bool
p [Ingredient]
es  =  Results
  { implementationss :: [[[Bndn]]]
implementationss  =  [[[Bndn]]]
implementationsT
  , candidatess :: [[[Bndn]]]
candidatess  =  [[[Bndn]]]
candidatesT
  , bindings :: [Bndn]
bindings  =  [Bndn]
tests
  , theory :: Thy
theory  =  Thy
thy
  , patternss :: [[[Bndn]]]
patternss  =  [[[Bndn]]]
patternss
  , deconstructions :: [Expr]
deconstructions  =  [Expr]
deconstructions
  }
  where
  implementationsT :: [[[Bndn]]]
implementationsT  =  ([Bndn] -> Bool) -> [[[Bndn]]] -> [[[Bndn]]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT [Bndn] -> Bool
implements [[[Bndn]]]
candidatesT
  implements :: [Bndn] -> Bool
implements [Bndn]
fx  =  [Bndn] -> Bool
defnApparentlyTerminates [Bndn]
fx
                 Bool -> Bool -> Bool
&& [Bndn] -> Bool
test [Bndn]
fx
                 Bool -> Bool -> Bool
&& Bool -> Bool
errorToFalse (f -> Bool
p (Int -> [Bndn] -> f
forall f. Conjurable f => Int -> [Bndn] -> f
cevl Int
maxRecursions [Bndn]
fx))
  candidatesT :: [[[Bndn]]]
candidatesT  =  (if Bool
uniqueCandidates then Int -> Int -> String -> f -> [[[Bndn]]] -> [[[Bndn]]]
forall f.
Conjurable f =>
Int -> Int -> String -> f -> [[[Bndn]]] -> [[[Bndn]]]
nubCandidates Int
maxTests Int
maxRecursions String
nm f
f else [[[Bndn]]] -> [[[Bndn]]]
forall a. a -> a
id)
               ([[[Bndn]]] -> [[[Bndn]]]) -> [[[Bndn]]] -> [[[Bndn]]]
forall a b. (a -> b) -> a -> b
$  (if Int
target Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Int -> [[[Bndn]]] -> [[[Bndn]]]
forall a. Int -> [[a]] -> [[a]]
targetiers Int
target else [[[Bndn]]] -> [[[Bndn]]]
forall a. a -> a
id)
               ([[[Bndn]]] -> [[[Bndn]]]) -> [[[Bndn]]] -> [[[Bndn]]]
forall a b. (a -> b) -> a -> b
$  (if Int
maxSize Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Int -> [[[Bndn]]] -> [[[Bndn]]]
forall a. Int -> [a] -> [a]
take Int
maxSize else [[[Bndn]]] -> [[[Bndn]]]
forall a. a -> a
id)
               ([[[Bndn]]] -> [[[Bndn]]]) -> [[[Bndn]]] -> [[[Bndn]]]
forall a b. (a -> b) -> a -> b
$  [[[Bndn]]]
candidatesTT
  ([[[Bndn]]]
candidatesTT, Thy
thy, [[[Bndn]]]
patternss, [Expr]
deconstructions)  =  String
-> f -> [Ingredient] -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
forall f.
Conjurable f =>
String
-> f -> [Ingredient] -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
candidateDefns String
nm f
f [Ingredient]
es

  test :: [Bndn] -> Bool
test [Bndn]
dfn  =  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
errorToFalse (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> Int -> [Bndn] -> Bool -> Expr -> Bool
forall a.
Typeable a =>
(Expr -> Expr) -> Int -> [Bndn] -> a -> Expr -> a
deval (f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f) Int
maxRecursions [Bndn]
dfn Bool
False)
            ([Expr] -> Bool) -> [Expr] -> Bool
forall a b. (a -> b) -> a -> b
$  [Expr -> Expr
funToVar Expr
lhs Expr -> Expr -> Expr
-==- Expr
rhs | (Expr
lhs, Expr
rhs) <- [Bndn]
tests]
  tests :: [Bndn]
tests  =  Int -> Int -> String -> f -> [Bndn]
forall f. Conjurable f => Int -> Int -> String -> f -> [Bndn]
conjureTestDefn Int
maxTests Int
maxSearchTests String
nm f
f
  -==- :: Expr -> Expr -> Expr
(-==-)  =  f -> Expr -> Expr -> Expr
forall f. Conjurable f => f -> Expr -> Expr -> Expr
conjureMkEquation f
f
  maxTests :: Int
maxTests  =  [Ingredient] -> Int
maxTestsI [Ingredient]
es
  (Int
target, Int
maxSize)  =  [Ingredient] -> (Int, Int)
targetAndMaxSizeI [Ingredient]
es
  maxRecursions :: Int
maxRecursions  =  [Ingredient] -> Int
maxRecursionsI [Ingredient]
es
  maxSearchTests :: Int
maxSearchTests  =  [Ingredient] -> Int
maxSearchTestsI [Ingredient]
es
  uniqueCandidates :: Bool
uniqueCandidates  =  [Ingredient] -> Bool
uniqueCandidatesI [Ingredient]
es


-- | Return apparently unique candidate definitions.
--
-- This function returns a trio:
--
-- 1. tiers of candidate definitions
-- 2. an equational theory
-- 3. a list of allowed deconstructions
candidateDefns :: Conjurable f => String -> f -> [Ingredient] -> ([[Defn]], Thy, [[Defn]], [Expr])
candidateDefns :: forall f.
Conjurable f =>
String
-> f -> [Ingredient] -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
candidateDefns String
nm f
f [Ingredient]
is  =  String
-> f -> [Ingredient] -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
candidateDefns' String
nm f
f [Ingredient]
is
  where
  candidateDefns' :: String
-> f -> [Ingredient] -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
candidateDefns'  =  if [Ingredient] -> Bool
singlePatternI [Ingredient]
is
                      then String
-> f -> [Ingredient] -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
forall f.
Conjurable f =>
String
-> f -> [Ingredient] -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
candidateDefns1
                      else String
-> f -> [Ingredient] -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
forall f.
Conjurable f =>
String
-> f -> [Ingredient] -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
candidateDefnsC


-- | Return apparently unique candidate definitions
--   where there is a single body.
candidateDefns1 :: Conjurable f => String -> f -> [Ingredient] -> ([[Defn]], Thy, [[Defn]], [Expr])
candidateDefns1 :: forall f.
Conjurable f =>
String
-> f -> [Ingredient] -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
candidateDefns1 String
nm f
f [Ingredient]
ps  =  ([[Expr]] -> [[[Bndn]]])
-> ([[Expr]], Thy, [[[Bndn]]], [Expr])
-> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
forall {t} {a} {b} {c} {d}.
(t -> a) -> (t, b, c, d) -> (a, b, c, d)
first4 ((Expr -> [Bndn]) -> [[Expr]] -> [[[Bndn]]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT Expr -> [Bndn]
forall {b}. b -> [(Expr, b)]
toDefn) (([[Expr]], Thy, [[[Bndn]]], [Expr])
 -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr]))
-> ([[Expr]], Thy, [[[Bndn]]], [Expr])
-> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
forall a b. (a -> b) -> a -> b
$ String -> f -> [Ingredient] -> ([[Expr]], Thy, [[[Bndn]]], [Expr])
forall f.
Conjurable f =>
String -> f -> [Ingredient] -> ([[Expr]], Thy, [[[Bndn]]], [Expr])
candidateExprs String
nm f
f [Ingredient]
ps
  where
  efxs :: Expr
efxs  =  String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
conjureVarApplication String
nm f
f
  toDefn :: b -> [(Expr, b)]
toDefn b
e  =  [(Expr
efxs, b
e)]
  first4 :: (t -> a) -> (t, b, c, d) -> (a, b, c, d)
first4 t -> a
f (t
x,b
y,c
z,d
w)  =  (t -> a
f t
x, b
y, c
z, d
w)


-- | Return apparently unique candidate bodies.
candidateExprs :: Conjurable f => String -> f -> [Ingredient] -> ([[Expr]], Thy, [[Defn]], [Expr])
candidateExprs :: forall f.
Conjurable f =>
String -> f -> [Ingredient] -> ([[Expr]], Thy, [[[Bndn]]], [Expr])
candidateExprs String
nm f
f [Ingredient]
is  =
  ( [[Expr]]
as [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ (Expr -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT (Expr -> [[Expr]] -> [[Expr]]
`enumerateFillings` [[Expr]]
recs) [[Expr]]
ts
  , Thy
thy
  , [[ [(Expr
efxs, Expr
eh)] ]]
  , [Expr]
deconstructions
  )
  where
  ps :: [Ingredient]
ps  =  [Ingredient] -> [Ingredient]
actual [Ingredient]
is  -- extract actual primitives
  es :: [Expr]
es  =  (Ingredient -> Expr) -> [Ingredient] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Ingredient -> Expr
forall a b. (a, b) -> a
fst [Ingredient]
ps
  ts :: [[Expr]]
ts | Expr -> TypeRep
typ Expr
efxs TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep
boolTy  =  Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
andE [[[Expr]]
cs, [[Expr]]
rs]
                           [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
orE  [[[Expr]]
cs, [[Expr]]
rs]
     | Bool
otherwise           =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Expr -> Bool
keepIf
                           ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts (f -> Expr
forall a. Conjurable a => a -> Expr
conjureIf f
f) [[[Expr]]
cs, [[Expr]]
as, [[Expr]]
rs]
                           [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts (f -> Expr
forall a. Conjurable a => a -> Expr
conjureIf f
f) [[[Expr]]
cs, [[Expr]]
rs, [[Expr]]
as]
  cs :: [[Expr]]
cs  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
False, Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
True])
      ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  Expr -> [[Expr]]
forN (Bool -> Expr
forall a. Typeable a => a -> Expr
hole (Bool
forall a. HasCallStack => a
undefined :: Bool))
  as :: [[Expr]]
as  =  Expr -> [[Expr]]
forN Expr
efxs
  rs :: [[Expr]]
rs  =  Expr -> [[Expr]]
forR Expr
efxs
  forN :: Expr -> [[Expr]]
forN Expr
h  =  Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]
enumerateAppsFor Expr
h Expr -> Bool
keep ([Expr] -> [[Expr]]) -> [Expr] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr]
exs [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es
  forR :: Expr -> [[Expr]]
forR Expr
h  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> (Expr
eh Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) (Expr -> [Expr]
holes Expr
e))
          ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]
enumerateAppsFor Expr
h Expr -> Bool
keep ([Expr] -> [[Expr]]) -> [Expr] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr]
exs [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr
eh]
  eh :: Expr
eh  =  Expr -> Expr
holeAsTypeOf Expr
efxs
  efxs :: Expr
efxs  =  String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
conjureVarApplication String
nm f
f
  (Expr
ef:[Expr]
exs)  =  Expr -> [Expr]
unfoldApp Expr
efxs
  keep :: Expr -> Bool
keep | Bool
rewrite    =  Thy -> Expr -> Bool
isRootNormalC Thy
thy (Expr -> Bool) -> (Expr -> Expr) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
fastMostGeneralVariation
       | Bool
otherwise  =  Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
  keepR :: Expr -> Bool
keepR | Bool
requireDescent  =  (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
descends Expr -> Expr -> Bool
isDecOf Expr
efxs
        | Bool
otherwise       =  Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
    where
    Expr
e isDecOf :: Expr -> Expr -> Bool
`isDecOf` Expr
e'  =  Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
                    [  ()
                    |  Expr
d <- [Expr]
deconstructions
                    ,  [Bndn]
m <- Maybe [Bndn] -> [[Bndn]]
forall a. Maybe a -> [a]
maybeToList (Expr
e Expr -> Expr -> Maybe [Bndn]
`match` Expr
d)
                    ,  (Bndn -> Bool) -> [Bndn] -> [Bndn]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Expr -> Expr -> Bool) -> Bndn -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
(/=)) [Bndn]
m [Bndn] -> [Bndn] -> Bool
forall a. Eq a => a -> a -> Bool
== [(Expr -> Expr
holeAsTypeOf Expr
e', Expr
e')]
                    ]

  deconstructions :: [Expr]
  deconstructions :: [Expr]
deconstructions  =  (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (f -> Int -> Expr -> Bool
forall f. Conjurable f => f -> Int -> Expr -> Bool
conjureIsDeconstruction f
f Int
maxTests)
                   ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$  (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
candidateDeconstructionsFrom
                   ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$  [[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Expr]] -> [Expr])
-> ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [[Expr]] -> [[Expr]]
forall a. Int -> [a] -> [a]
take Int
maxDeconstructionSize
                   ([[Expr]] -> [Expr]) -> [[Expr]] -> [Expr]
forall a b. (a -> b) -> a -> b
$  (Expr -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT Expr -> [[Expr]]
forN [[Expr]
hs]
    where
    hs :: [Expr]
hs  =  [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ f -> [Expr]
forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f

  recs :: [[Expr]]
recs  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Expr -> Bool
keepR
        ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
ef [Expr -> [[Expr]]
forN Expr
h | Expr
h <- f -> [Expr]
forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f]
  thy :: Thy
thy  =  (Expr -> Expr -> Bool) -> Thy -> Thy
doubleCheck Expr -> Expr -> Bool
(===)
       (Thy -> Thy) -> ([Expr] -> Thy) -> [Expr] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtoms Expr -> Expr -> Bool
(===) Int
maxEquationSize ([[Expr]] -> Thy) -> ([Expr] -> [[Expr]]) -> [Expr] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
:[]) ([Expr] -> [[Expr]]) -> ([Expr] -> [Expr]) -> [Expr] -> [[Expr]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub
       ([Expr] -> Thy) -> [Expr] -> Thy
forall a b. (a -> b) -> a -> b
$  [Ingredient] -> [Expr]
cjHoles (String -> f -> Ingredient
forall a. Conjurable a => String -> a -> Ingredient
fun String
nm f
fIngredient -> [Ingredient] -> [Ingredient]
forall a. a -> [a] -> [a]
:[Ingredient]
ps) [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
False, Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
True] [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es
  === :: Expr -> Expr -> Bool
(===)  =  [Ingredient] -> Int -> Expr -> Expr -> Bool
cjAreEqual (String -> f -> Ingredient
forall a. Conjurable a => String -> a -> Ingredient
fun String
nm f
fIngredient -> [Ingredient] -> [Ingredient]
forall a. a -> [a] -> [a]
:[Ingredient]
ps) Int
maxTests
  maxTests :: Int
maxTests               =  [Ingredient] -> Int
maxTestsI [Ingredient]
is
  maxEquationSize :: Int
maxEquationSize        =  [Ingredient] -> Int
maxEquationSizeI [Ingredient]
is
  maxDeconstructionSize :: Int
maxDeconstructionSize  =  [Ingredient] -> Int
maxDeconstructionSizeI [Ingredient]
is
  requireDescent :: Bool
requireDescent         =  [Ingredient] -> Bool
requireDescentI [Ingredient]
is
  rewrite :: Bool
rewrite                =  [Ingredient] -> Bool
rewriteI [Ingredient]
is


-- | Return apparently unique candidate definitions
--   using pattern matching.
candidateDefnsC :: Conjurable f => String -> f -> [Ingredient] -> ([[Defn]], Thy, [[Defn]], [Expr])
candidateDefnsC :: forall f.
Conjurable f =>
String
-> f -> [Ingredient] -> ([[[Bndn]]], Thy, [[[Bndn]]], [Expr])
candidateDefnsC String
nm f
f [Ingredient]
is =
  ( ([Bndn] -> Bool) -> [[[Bndn]]] -> [[[Bndn]]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT [Bndn] -> Bool
hasRedundant ([[[Bndn]]] -> [[[Bndn]]]) -> [[[Bndn]]] -> [[[Bndn]]]
forall a b. (a -> b) -> a -> b
$ ([Bndn] -> [[[Bndn]]]) -> [[[Bndn]]] -> [[[Bndn]]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT [Bndn] -> [[[Bndn]]]
fillingsFor [[[Bndn]]]
fss
  , Thy
thy
  , ([Expr] -> [Bndn]) -> [[[Expr]]] -> [[[Bndn]]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT ((Expr -> Bndn) -> [Expr] -> [Bndn]
forall a b. (a -> b) -> [a] -> [b]
map (,Expr
eh)) [[[Expr]]]
pats
  , [Expr]
deconstructions
  )
  where
  pats :: [[[Expr]]]
pats | Int
maxPatternSize Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0  =  Int -> [[[Expr]]] -> [[[Expr]]]
forall a. Int -> [a] -> [a]
take Int
maxPatternSize ([[[Expr]]] -> [[[Expr]]]) -> [[[Expr]]] -> [[[Expr]]]
forall a b. (a -> b) -> a -> b
$ Int -> [Expr] -> String -> f -> [[[Expr]]]
forall f.
Conjurable f =>
Int -> [Expr] -> String -> f -> [[[Expr]]]
conjurePats Int
maxPatternDepth [Expr]
es String
nm f
f
       | Bool
otherwise           =                        Int -> [Expr] -> String -> f -> [[[Expr]]]
forall f.
Conjurable f =>
Int -> [Expr] -> String -> f -> [[[Expr]]]
conjurePats Int
maxPatternDepth [Expr]
es String
nm f
f
  fss :: [[[Bndn]]]
fss  =  ([Expr] -> [[[Bndn]]]) -> [[[Expr]]] -> [[[Bndn]]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT [Expr] -> [[[Bndn]]]
ps2fss [[[Expr]]]
pats
  -- replaces the any guard symbol with a guard of the correct type
  ps :: [Ingredient]
ps  =  [Ingredient] -> [Ingredient]
actual [Ingredient]
is  -- extract actual ingredients/primitives from the list
  es :: [Expr]
es  =  [if Expr -> Bool
isGuardSymbol Expr
e then f -> Expr
forall a. Conjurable a => a -> Expr
conjureGuard f
f else Expr
e | (Expr
e,Reification
_) <- [Ingredient]
ps]

  eh :: Expr
eh  =  Expr -> Expr
holeAsTypeOf Expr
efxs
  efxs :: Expr
efxs  =  String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
conjureVarApplication String
nm f
f
  (Expr
ef:[Expr]
_)  =  Expr -> [Expr]
unfoldApp Expr
efxs

  unguardT :: [[Expr]] -> [[Expr]]
unguardT | (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr -> Bool
isGuardSymbol [Expr]
es  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT Expr -> Bool
isGuard
           | Bool
otherwise             =  [[Expr]] -> [[Expr]]
forall a. a -> a
id

  keep :: Expr -> Bool
keep | Bool
rewriting  =  Thy -> Expr -> Bool
isRootNormalC Thy
thy (Expr -> Bool) -> (Expr -> Expr) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
fastMostGeneralVariation
       | Bool
otherwise  =  Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True

  keepBndn :: Bndn -> Bool
keepBndn | Bool
rewriting  =  \b :: Bndn
b@(Expr
_,Expr
rhs) -> Bndn -> Bool
isBaseCase Bndn
b Bool -> Bool -> Bool
|| Expr -> Int
size (Thy -> Expr -> Expr
normalize Thy
thy Expr
rhs) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Expr -> Int
size Expr
rhs
           | Bool
otherwise  =  Bool -> Bndn -> Bool
forall a b. a -> b -> a
const Bool
True

  appsWith :: Expr -> [Expr] -> [[Expr]]
  appsWith :: Expr -> [Expr] -> [[Expr]]
appsWith Expr
eh [Expr]
vs  =  Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]
enumerateAppsFor Expr
eh Expr -> Bool
k ([Expr] -> [[Expr]]) -> [Expr] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr]
vs [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es
    where
    k :: Expr -> Bool
k Expr
e  =  Expr -> Bool
keepNumeric Expr
e Bool -> Bool -> Bool
&& Expr -> Bool
keepConstant Expr
e Bool -> Bool -> Bool
&& Expr -> Bool
keep Expr
e
    -- discards non-atomic numeric ground expressions such as 1 + 1
    keepNumeric :: Expr -> Bool
keepNumeric | Bool
atomicNumbers Bool -> Bool -> Bool
&& Expr -> Bool
isNumeric Expr
eh  =  \Expr
e -> Expr -> Bool
isFun Expr
e Bool -> Bool -> Bool
|| Expr -> Bool
isConst Expr
e Bool -> Bool -> Bool
|| Bool -> Bool
not (Expr -> Bool
isGround Expr
e)
                | Bool
otherwise                      =  Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
    -- discards big non-atomic ground expressions such as 1 + 1 or reverse [1,2]
    keepConstant :: Expr -> Bool
keepConstant | Int
maxConstantSize Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0  =  \Expr
e -> Expr -> Bool
isFun Expr
e Bool -> Bool -> Bool
|| Expr -> Bool
isConst Expr
e Bool -> Bool -> Bool
|| Bool -> Bool
not (Expr -> Bool
isGround Expr
e) Bool -> Bool -> Bool
|| Expr -> Int
size Expr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
maxConstantSize
                 | Bool
otherwise            =  Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True

  isRedundant :: [Bndn] -> Bool
isRedundant | Bool
adHocRedundancy  =  \[Bndn]
e -> [Bndn] -> Bool
isRedundantDefn [Bndn]
e Bool -> Bool -> Bool
|| (Expr -> Expr) -> [Bndn] -> Bool
isRedundantModuloRewriting (Thy -> Expr -> Expr
normalize Thy
thy) [Bndn]
e
              | Bool
otherwise        =  Bool -> [Bndn] -> Bool
forall a b. a -> b -> a
const Bool
False

  hasRedundant :: [Bndn] -> Bool
hasRedundant | Bool
adHocRedundancy  =  [Bndn] -> Bool
hasRedundantRecursion
               | Bool
otherwise        =  Bool -> [Bndn] -> Bool
forall a b. a -> b -> a
const Bool
False

  isNumeric :: Expr -> Bool
isNumeric  =  f -> Expr -> Bool
forall f. Conjurable f => f -> Expr -> Bool
conjureIsNumeric f
f

  -==- :: Expr -> Expr -> Expr
(-==-)  =  f -> Expr -> Expr -> Expr
forall f. Conjurable f => f -> Expr -> Expr -> Expr
conjureMkEquation f
f
  tests :: [Bndn]
tests  =  Int -> Int -> String -> f -> [Bndn]
forall f. Conjurable f => Int -> Int -> String -> f -> [Bndn]
conjureTestDefn Int
maxTests Int
maxSearchTests String
nm f
f
  exprExpr :: Expr -> Expr
exprExpr  =  f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f

  ps2fss :: [Expr] -> [[Defn]]
  ps2fss :: [Expr] -> [[[Bndn]]]
ps2fss [Expr]
pats  =  ([Bndn] -> Bool) -> [[[Bndn]]] -> [[[Bndn]]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT [Bndn] -> Bool
isRedundant
               ([[[Bndn]]] -> [[[Bndn]]])
-> ([[[Bndn]]] -> [[[Bndn]]]) -> [[[Bndn]]] -> [[[Bndn]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  [[[Bndn]]] -> [[[Bndn]]]
forall a. [[[a]]] -> [[[a]]]
products  -- alt: use delayedProducts
               ([[[Bndn]]] -> [[[Bndn]]]) -> [[[Bndn]]] -> [[[Bndn]]]
forall a b. (a -> b) -> a -> b
$  (Expr -> [[Bndn]]) -> [Expr] -> [[[Bndn]]]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> [[Bndn]]
p2eess [Expr]
pats
    -- delayedProducts makes the number of patterns counts as the size+1.
    where
    p2eess :: Expr -> [[Bndn]]
    -- the following guarded line is an optional optimization
    -- if the function is defined for the given pattern,
    -- simply use its return value as the only possible result
    p2eess :: Expr -> [[Bndn]]
p2eess Expr
pat | Bool
copyBindings Bool -> Bool -> Bool
&& f -> Expr -> Bool
forall f. Conjurable f => f -> Expr -> Bool
isGroundPat f
f Expr
pat  =  [[(Expr
pat, f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
toValPat f
f Expr
pat)]]
    p2eess Expr
pat  =  (Expr -> Bndn) -> [[Expr]] -> [[Bndn]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (Expr
pat,)
                ([[Expr]] -> [[Bndn]])
-> ([Expr] -> [[Expr]]) -> [Expr] -> [[Bndn]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Expr -> Bool
keepBase
                ([[Expr]] -> [[Expr]])
-> ([Expr] -> [[Expr]]) -> [Expr] -> [[Expr]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Expr -> [Expr] -> [[Expr]]
appsWith Expr
pat
                ([Expr] -> [[Expr]]) -> ([Expr] -> [Expr]) -> [Expr] -> [[Expr]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
drop Int
1 -- this excludes the function name itself
                ([Expr] -> [[Bndn]]) -> [Expr] -> [[Bndn]]
forall a b. (a -> b) -> a -> b
$  Expr -> [Expr]
vars Expr
pat [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr
eh | (([Expr], Expr) -> Bool) -> [([Expr], Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (([Expr] -> Expr -> Bool) -> ([Expr], Expr) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Expr] -> Expr -> Bool
forall {a}. Eq a => [a] -> Expr -> Bool
should) ([[Expr]] -> [Expr] -> [([Expr], Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[Expr]]
aess [Expr]
aes)]
      where
      keepBase :: Expr -> Bool
keepBase
        | Bool -> Bool
not Bool
earlyTests  =  Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
        | (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isVar (Expr -> [Expr]
unfoldApp Expr
pat)  =  Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
        | Bool
otherwise  =  \Expr
e -> Expr -> Bool
hasHole Expr
e Bool -> Bool -> Bool
|| Expr -> Bool
reallyKeepBase Expr
e
      reallyKeepBase :: Expr -> Bool
reallyKeepBase Expr
e  =  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
        [ Bool -> Bool
errorToFalse (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> Bool
forall a. Typeable a => a -> Expr -> a
eval Bool
False (Expr -> Bool) -> Expr -> Bool
forall a b. (a -> b) -> a -> b
$ (Expr
e Expr -> [Bndn] -> Expr
//- [Bndn]
bs) Expr -> Expr -> Expr
-==- Expr
rhs
        | (Expr
lhs,Expr
rhs) <- [Bndn]
tests
        -- filter test bindings that match the current pattern:
        , Just [Bndn]
bs <- [Expr
lhs Expr -> Expr -> Maybe [Bndn]
`matchArgs` Expr
pat]
        ]
      matchArgs :: Expr -> Expr -> Maybe [Bndn]
matchArgs Expr
efxs Expr
efys  =  [Expr] -> Expr
fold ((Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
exprExpr (Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
drop Int
1 (Expr -> [Expr]
unfoldApp Expr
efxs)))
                      Expr -> Expr -> Maybe [Bndn]
`match` [Expr] -> Expr
fold               (Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
drop Int
1 (Expr -> [Expr]
unfoldApp Expr
efys))

      -- computes whether we should include a recurse for this given argument
      -- numeric arguments additionally require 0 to be present as a case
      -- for recursion
      should :: [a] -> Expr -> Bool
should [a]
aes Expr
ae  =  [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub [a]
aes) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 Bool -> Bool -> Bool
&& Expr -> Bool
hasVar Expr
ae Bool -> Bool -> Bool
&& (Expr -> Bool
isApp Expr
ae Bool -> Bool -> Bool
|| Expr -> Bool
isUnbreakable Expr
ae)
      aes :: [Expr]
aes   =                  ([Expr] -> [Expr]
forall a. HasCallStack => [a] -> [a]
tail ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
unfoldApp (Expr -> [Expr]) -> (Expr -> Expr) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
rehole) Expr
pat
      aess :: [[Expr]]
aess  =  [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]]
transpose ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ (Expr -> [Expr]) -> [Expr] -> [[Expr]]
forall a b. (a -> b) -> [a] -> [b]
map ([Expr] -> [Expr]
forall a. HasCallStack => [a] -> [a]
tail ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
unfoldApp (Expr -> [Expr]) -> (Expr -> Expr) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
rehole) [Expr]
pats

  fillingsFor1 :: Bndn -> [[Bndn]]
  fillingsFor1 :: Bndn -> [[Bndn]]
fillingsFor1 (Expr
ep,Expr
er)  =  (Bndn -> Bool) -> [[Bndn]] -> [[Bndn]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Bndn -> Bool
keepBndn
                        ([[Bndn]] -> [[Bndn]])
-> ([[Expr]] -> [[Bndn]]) -> [[Expr]] -> [[Bndn]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  ([Expr] -> Bndn) -> [[[Expr]]] -> [[Bndn]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (\[Expr]
es -> (Expr
ep,Expr -> [Expr] -> Expr
fill Expr
er [Expr]
es))
                        ([[[Expr]]] -> [[Bndn]])
-> ([[Expr]] -> [[[Expr]]]) -> [[Expr]] -> [[Bndn]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  [[[Expr]]] -> [[[Expr]]]
forall a. [[[a]]] -> [[[a]]]
products
                        ([[[Expr]]] -> [[[Expr]]])
-> ([[Expr]] -> [[[Expr]]]) -> [[Expr]] -> [[[Expr]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Int -> [[Expr]] -> [[[Expr]]]
forall a. Int -> a -> [a]
replicate ([Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr] -> Int) -> [Expr] -> Int
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
holes Expr
er)
                        ([[Expr]] -> [[Bndn]]) -> [[Expr]] -> [[Bndn]]
forall a b. (a -> b) -> a -> b
$  Expr -> [[Expr]]
recs' Expr
ep

  fillingsFor :: Defn -> [[Defn]]
  fillingsFor :: [Bndn] -> [[[Bndn]]]
fillingsFor  =  [[[Bndn]]] -> [[[Bndn]]]
forall a. [[[a]]] -> [[[a]]]
products ([[[Bndn]]] -> [[[Bndn]]])
-> ([Bndn] -> [[[Bndn]]]) -> [Bndn] -> [[[Bndn]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bndn -> [[Bndn]]) -> [Bndn] -> [[[Bndn]]]
forall a b. (a -> b) -> [a] -> [b]
map Bndn -> [[Bndn]]
fillingsFor1

  keepR :: Expr -> Expr -> Bool
keepR Expr
ep | Bool
requireDescent  =  (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
descends Expr -> Expr -> Bool
isDecOf Expr
ep
           | Bool
otherwise       =  Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
    where
    Expr
e isDecOf :: Expr -> Expr -> Bool
`isDecOf` Expr
e'  =  Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
                    [  ()
                    |  Expr
d <- [Expr]
deconstructions
                    ,  [Bndn]
m <- Maybe [Bndn] -> [[Bndn]]
forall a. Maybe a -> [a]
maybeToList (Expr
e Expr -> Expr -> Maybe [Bndn]
`match` Expr
d)
                       -- h (_) is bound to e'
                    ,  Expr -> [Bndn] -> Maybe Expr
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Expr
h [Bndn]
m Maybe Expr -> Maybe Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e'
                       -- other than (h,e') we only accept (var,var)
                    ,  (Bndn -> Bool) -> [Bndn] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Expr
e1,Expr
e2) -> Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
h Bool -> Bool -> Bool
|| Expr -> Bool
isVar Expr
e2) [Bndn]
m
                    ]
      where
      h :: Expr
h = Expr -> Expr
holeAsTypeOf Expr
e'

  deconstructions :: [Expr]
  deconstructions :: [Expr]
deconstructions  =  (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (f -> Int -> Expr -> Bool
forall f. Conjurable f => f -> Int -> Expr -> Bool
conjureIsDeconstruction f
f Int
maxTests)
                   ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$  (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
candidateDeconstructionsFromHoled
                   ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$  [[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Expr]] -> [Expr])
-> ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [[Expr]] -> [[Expr]]
forall a. Int -> [a] -> [a]
take Int
maxDeconstructionSize
                   ([[Expr]] -> [Expr]) -> [[Expr]] -> [Expr]
forall a b. (a -> b) -> a -> b
$  [[Expr]] -> [[Expr]]
unguardT
                   ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  (Expr -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT (Expr -> [Expr] -> [[Expr]]
`appsWith` [Expr]
hs) [[Expr]
hs]
    where
    hs :: [Expr]
hs  =  [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ f -> [Expr]
forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f

  recs :: Expr -> [[Expr]]
  recs :: Expr -> [[Expr]]
recs Expr
ep  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (Expr -> Expr -> Bool
keepR Expr
ep)
           ([[Expr]] -> [[Expr]])
-> ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT (\Expr
e -> Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ep)
           ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  [Expr] -> [[Expr]]
recsV' ([Expr] -> [Expr]
forall a. HasCallStack => [a] -> [a]
tail (Expr -> [Expr]
vars Expr
ep))

  recsV :: [Expr] -> [[Expr]]
  recsV :: [Expr] -> [[Expr]]
recsV [Expr]
vs  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
vs) (Expr -> [Expr]
vars Expr
e))
            ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
ef [[[Expr]] -> [[Expr]]
unguardT ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr] -> [[Expr]]
appsWith Expr
h [Expr]
vs | Expr
h <- f -> [Expr]
forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f]

  -- like recs, but memoized
  recs' :: Expr -> [[Expr]]
  recs' :: Expr -> [[Expr]]
recs' Expr
ep  =  [[Expr]] -> Maybe [[Expr]] -> [[Expr]]
forall a. a -> Maybe a -> a
fromMaybe [[Expr]]
forall {a}. a
errRP (Maybe [[Expr]] -> [[Expr]]) -> Maybe [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ Expr -> [(Expr, [[Expr]])] -> Maybe [[Expr]]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Expr
ep [(Expr, [[Expr]])]
eprs
    where
    eprs :: [(Expr, [[Expr]])]
eprs = [(Expr
ep, Expr -> [[Expr]]
recs Expr
ep) | Expr
ep <- [[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Expr]]
possiblePats]

  possiblePats :: [[Expr]]
  possiblePats :: [[Expr]]
possiblePats  =  ([[Expr]] -> [Expr]) -> [[[Expr]]] -> [[Expr]]
forall a b. (a -> b) -> [a] -> [b]
map ([Expr] -> [Expr]
forall a. Ord a => [a] -> [a]
nubSort ([Expr] -> [Expr]) -> ([[Expr]] -> [Expr]) -> [[Expr]] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) ([[[Expr]]] -> [[Expr]]) -> [[[Expr]]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [[[Expr]]]
pats

  -- like recsV, but memoized
  recsV' :: [Expr] -> [[Expr]]
  recsV' :: [Expr] -> [[Expr]]
recsV' [Expr]
vs  =  [[Expr]] -> Maybe [[Expr]] -> [[Expr]]
forall a. a -> Maybe a -> a
fromMaybe [[Expr]]
forall {a}. a
errRV (Maybe [[Expr]] -> [[Expr]]) -> Maybe [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr] -> [([Expr], [[Expr]])] -> Maybe [[Expr]]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup ([Expr] -> [Expr]
forall a. Ord a => [a] -> [a]
nubSort [Expr]
vs) [([Expr], [[Expr]])]
evrs
    where
    evrs :: [([Expr], [[Expr]])]
evrs = [([Expr]
vs, [Expr] -> [[Expr]]
recsV [Expr]
vs) | [Expr]
vs <- ([[Expr]] -> [[Expr]]) -> [[[Expr]]] -> [[Expr]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [[Expr]] -> [[Expr]]
forall a. Ord a => [a] -> [a]
nubSort ([[[Expr]]] -> [[Expr]]) -> [[[Expr]]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ (Expr -> [Expr]) -> [[Expr]] -> [[[Expr]]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT ([Expr] -> [Expr]
forall a. Ord a => [a] -> [a]
nubSort ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
forall a. HasCallStack => [a] -> [a]
tail ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
vars) [[Expr]]
possiblePats]

  errRP :: a
errRP  =  String -> a
forall a. HasCallStack => String -> a
error String
"candidateDefnsC: unexpected pattern.  You have found a bug, please report it."
  errRV :: a
errRV  =  String -> a
forall a. HasCallStack => String -> a
error String
"candidateDefnsC: unexpected variables.  You have found a bug, please report it."

  thy :: Thy
thy  =  (Expr -> Expr -> Bool) -> Thy -> Thy
doubleCheck Expr -> Expr -> Bool
(===)
       (Thy -> Thy) -> ([Expr] -> Thy) -> [Expr] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtoms Expr -> Expr -> Bool
(===) Int
maxEquationSize ([[Expr]] -> Thy) -> ([Expr] -> [[Expr]]) -> [Expr] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
:[]) ([Expr] -> [[Expr]]) -> ([Expr] -> [Expr]) -> [Expr] -> [[Expr]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub
       ([Expr] -> Thy) -> [Expr] -> Thy
forall a b. (a -> b) -> a -> b
$  [Ingredient] -> [Expr]
cjHoles (String -> f -> Ingredient
forall a. Conjurable a => String -> a -> Ingredient
fun String
nm f
fIngredient -> [Ingredient] -> [Ingredient]
forall a. a -> [a] -> [a]
:[Ingredient]
ps) [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
False, Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
True] [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es
  === :: Expr -> Expr -> Bool
(===)  =  [Ingredient] -> Int -> Expr -> Expr -> Bool
cjAreEqual (String -> f -> Ingredient
forall a. Conjurable a => String -> a -> Ingredient
fun String
nm f
fIngredient -> [Ingredient] -> [Ingredient]
forall a. a -> [a] -> [a]
:[Ingredient]
ps) Int
maxTests
  isUnbreakable :: Expr -> Bool
isUnbreakable  =  f -> Expr -> Bool
forall f. Conjurable f => f -> Expr -> Bool
conjureIsUnbreakable f
f

  maxTests :: Int
maxTests               =  [Ingredient] -> Int
maxTestsI [Ingredient]
is
  maxSearchTests :: Int
maxSearchTests         =  [Ingredient] -> Int
maxSearchTestsI [Ingredient]
is
  maxEquationSize :: Int
maxEquationSize        =  [Ingredient] -> Int
maxEquationSizeI [Ingredient]
is
  maxConstantSize :: Int
maxConstantSize        =  [Ingredient] -> Int
maxConstantSizeI [Ingredient]
is
  maxDeconstructionSize :: Int
maxDeconstructionSize  =  [Ingredient] -> Int
maxDeconstructionSizeI [Ingredient]
is
  maxPatternDepth :: Int
maxPatternDepth        =  [Ingredient] -> Int
maxPatternDepthI [Ingredient]
is
  maxPatternSize :: Int
maxPatternSize         =  [Ingredient] -> Int
maxPatternSizeI [Ingredient]
is
  requireDescent :: Bool
requireDescent         =  [Ingredient] -> Bool
requireDescentI [Ingredient]
is
  earlyTests :: Bool
earlyTests             =  [Ingredient] -> Bool
earlyTestsI [Ingredient]
is
  copyBindings :: Bool
copyBindings           =  [Ingredient] -> Bool
copyBindingsI [Ingredient]
is
  adHocRedundancy :: Bool
adHocRedundancy        =  [Ingredient] -> Bool
assortedPruningI [Ingredient]
is -- TODO: rename
  atomicNumbers :: Bool
atomicNumbers          =  [Ingredient] -> Bool
atomicNumbersI [Ingredient]
is
  rewriting :: Bool
rewriting              =  [Ingredient] -> Bool
rewriteI [Ingredient]
is


-- | Checks if the given pattern is a ground pattern.
--
-- A pattern is a ground pattern when its arguments are fully defined
-- and evaluating the function returns a defined value.
--
-- This is to be used on values returned by conjurePats.
--
-- For now, this is only used on 'candidateDefnsC'.
isGroundPat :: Conjurable f => f -> Expr -> Bool
isGroundPat :: forall f. Conjurable f => f -> Expr -> Bool
isGroundPat f
f Expr
pat  =  Bool -> Bool
errorToFalse (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Expr -> Bool
forall a. Typeable a => a -> Expr -> a
eval Bool
False (Expr -> Bool) -> Expr -> Bool
forall a b. (a -> b) -> a -> b
$ Expr
gpat Expr -> Expr -> Expr
-==- Expr
gpat
  where
  gpat :: Expr
gpat  =  f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
toGroundPat f
f Expr
pat
  -==- :: Expr -> Expr -> Expr
(-==-)  =  f -> Expr -> Expr -> Expr
forall f. Conjurable f => f -> Expr -> Expr -> Expr
conjureMkEquation f
f


-- | Given a complete "pattern", i.e. application encoded as expr,
--   converts it from using a "variable" function,
--   to an actual "value" function.
--
-- This function is used on 'isGroundPat' and 'toValPat'
toGroundPat :: Conjurable f => f -> Expr -> Expr
toGroundPat :: forall a. Conjurable a => a -> Expr -> Expr
toGroundPat f
f Expr
pat  =  [Expr] -> Expr
foldApp (String -> f -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"f" f
f Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr] -> [Expr]
forall a. HasCallStack => [a] -> [a]
tail (Expr -> [Expr]
unfoldApp Expr
pat))

-- | Evaluates a pattern to its final value.
--
-- Only to be used when the function is defined for the given set of arguments.
--
-- For now, this is only used on 'candidateDefnsC'.
toValPat :: Conjurable f => f -> Expr -> Expr
toValPat :: forall a. Conjurable a => a -> Expr -> Expr
toValPat f
f  =  f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
toGroundPat f
f
-- NOTE: the use of conjureExpress above is a hack.
--       Here, one could have used a conjureVal function,
--       that lifts 'val' over 'Expr's.
--       However this function does not exist.


-- hardcoded filtering rules

keepIf :: Expr -> Bool
keepIf :: Expr -> Bool
keepIf (Value String
"if" Dynamic
_ :$ Expr
ep :$ Expr
ex :$ Expr
ey)
  | Expr
ex Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ey  =  Bool
False
  | Expr -> Bool
anormal Expr
ep  =  Bool
False
  | Bool
otherwise  =  case Expr -> Maybe Bndn
binding Expr
ep of
                  Just (Expr
v,Expr
e) -> Expr
v Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Expr -> [Expr]
values Expr
ex
                  Maybe Bndn
Nothing -> Bool
True
  where
  anormal :: Expr -> Bool
anormal (Value String
"==" Dynamic
_ :$ Expr
e1 :$ Expr
e2) | Expr -> Bool
isVar Expr
e2 Bool -> Bool -> Bool
|| Expr -> Bool
isConst Expr
e1  =  Bool
True
  anormal Expr
_                                                    =  Bool
False
  binding :: Expr -> Maybe (Expr,Expr)
  binding :: Expr -> Maybe Bndn
binding (Value String
"==" Dynamic
_ :$ Expr
e1 :$ Expr
e2) | Expr -> Bool
isVar Expr
e1   =  Bndn -> Maybe Bndn
forall a. a -> Maybe a
Just (Expr
e1,Expr
e2)
                                     | Expr -> Bool
isVar Expr
e2   =  Bndn -> Maybe Bndn
forall a. a -> Maybe a
Just (Expr
e2,Expr
e1)
  binding Expr
_                                       =  Maybe Bndn
forall a. Maybe a
Nothing
keepIf Expr
_  =  String -> Bool
forall a. HasCallStack => String -> a
error String
"Conjure.Engine.keepIf: not an if"


-- equality between candidates

nubCandidates :: Conjurable f => Int -> Int -> String -> f -> [[Defn]] -> [[Defn]]
nubCandidates :: forall f.
Conjurable f =>
Int -> Int -> String -> f -> [[[Bndn]]] -> [[[Bndn]]]
nubCandidates Int
maxTests Int
maxRecursions String
nm f
f  =
  ([Bndn] -> [Bndn] -> Bool) -> [[[Bndn]]] -> [[[Bndn]]]
forall a. (a -> a -> Bool) -> [[a]] -> [[a]]
discardLaterT (([Bndn] -> [Bndn] -> Bool) -> [[[Bndn]]] -> [[[Bndn]]])
-> ([Bndn] -> [Bndn] -> Bool) -> [[[Bndn]]] -> [[[Bndn]]]
forall a b. (a -> b) -> a -> b
$ Int -> Int -> String -> f -> [Bndn] -> [Bndn] -> Bool
forall f.
Conjurable f =>
Int -> Int -> String -> f -> [Bndn] -> [Bndn] -> Bool
equalModuloTesting Int
maxTests Int
maxRecursions String
nm f
f


--- tiers utils ---

productsWith :: ([a] -> a) -> [ [[a]] ] -> [[a]]
productsWith :: forall a. ([a] -> a) -> [[[a]]] -> [[a]]
productsWith [a] -> a
f  =  ([a] -> a) -> [[[a]]] -> [[a]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT [a] -> a
f ([[[a]]] -> [[a]]) -> ([[[a]]] -> [[[a]]]) -> [[[a]]] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[[a]]] -> [[[a]]]
forall a. [[[a]]] -> [[[a]]]
products
-- TODO: move productsWith to LeanCheck?

delayedProducts :: [ [[a]] ] -> [[ [a] ]]
delayedProducts :: forall a. [[[a]]] -> [[[a]]]
delayedProducts [[[a]]]
xsss  =  [[[a]]] -> [[[a]]]
forall a. [[[a]]] -> [[[a]]]
products [[[a]]]
xsss [[[a]]] -> Int -> [[[a]]]
forall a. [[a]] -> Int -> [[a]]
`addWeight` ([[[a]]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[[a]]]
xsss Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
-- TODO: move delayedProducts to LeanCheck?

delayedProductsWith :: ([a] -> a) -> [ [[a]] ] -> [[a]]
delayedProductsWith :: forall a. ([a] -> a) -> [[[a]]] -> [[a]]
delayedProductsWith [a] -> a
f [[[a]]]
xsss  =  ([a] -> a) -> [[[a]]] -> [[a]]
forall a. ([a] -> a) -> [[[a]]] -> [[a]]
productsWith [a] -> a
f [[[a]]]
xsss [[a]] -> Int -> [[a]]
forall a. [[a]] -> Int -> [[a]]
`addWeight` [[[a]]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[[a]]]
xsss
-- TODO: move delayedProductsWith to LeanCheck?

foldAppProducts :: Expr -> [ [[Expr]] ] -> [[Expr]]
foldAppProducts :: Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
ef  =  ([Expr] -> Expr) -> [[[Expr]]] -> [[Expr]]
forall a. ([a] -> a) -> [[[a]]] -> [[a]]
delayedProductsWith ([Expr] -> Expr
foldApp ([Expr] -> Expr) -> ([Expr] -> [Expr]) -> [Expr] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr
efExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:))

-- show time in seconds rounded to one decimal place
-- the argument is expected to be in picoseconds
showTime :: Integer -> String
showTime :: Integer -> String
showTime Integer
ps  =  Double -> String
forall a. Show a => a -> String
show Double
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"s"
  where
  s :: Double
s  =  Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
ds Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
10.0 -- seconds
  ds :: Integer
ds  =  Integer
ps Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
100000000000 -- deciseconds, * 10 / 1 000 000 000 000

-- beware of lazyness, this computes the time for evaluating msg!
putWithTimeSince :: Integer -> String -> IO ()
putWithTimeSince :: Integer -> String -> IO ()
putWithTimeSince Integer
start String
msg
  | Integer
start Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0   =  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg  -- negative start time indicates omit runtime
  | String
msg String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
msg  =  do  -- forces evaluation of msg!
                   Integer
end <- IO Integer
getCPUTime
                   String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
showTime (Integer
end Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
start) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg
  | Bool
otherwise   =  String -> IO ()
forall a. HasCallStack => String -> a
error String
"putWithTimeSince: the impossible happened (GHC/Compiler/Interpreter bug?!)"

-- consume tiers until a target is reached, then stop
targetiers :: Int -> [[a]] -> [[a]]
targetiers :: forall a. Int -> [[a]] -> [[a]]
targetiers Int
n [[a]]
xss
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0     =  []
  | Bool
otherwise  =  case [[a]]
xss of [] -> []
                              ([a]
xs:[[a]]
xss) -> [a]
xs [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: Int -> [[a]] -> [[a]]
forall a. Int -> [[a]] -> [[a]]
targetiers (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs) [[a]]
xss

normalizeDefn :: Thy -> Defn -> Defn
normalizeDefn :: Thy -> [Bndn] -> [Bndn]
normalizeDefn  =  (Bndn -> Bndn) -> [Bndn] -> [Bndn]
forall a b. (a -> b) -> [a] -> [b]
map ((Bndn -> Bndn) -> [Bndn] -> [Bndn])
-> (Thy -> Bndn -> Bndn) -> Thy -> [Bndn] -> [Bndn]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Bndn -> Bndn
normalizeBndn

-- This function is quite expensive to run with bad complexity,
-- but is fine on Conjure: candidates are at most a few dozen symbols long
-- and this function just runs once.
normalizeBndn :: Thy -> Bndn -> Bndn
normalizeBndn :: Thy -> Bndn -> Bndn
normalizeBndn Thy
thy (Expr
lhs, Expr
rhs)
  | Expr
ef Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expr -> [Expr]
vars Expr
rhs  =  (Expr
lhs, (Expr -> Expr) -> Expr -> Expr
mapInnerFirstOuterLast Expr -> Expr
commutsort Expr
rhs)
  | Bool
otherwise           =  (Expr
lhs, Expr
rhs)
  where
  Expr
ef:[Expr]
_  =  Expr -> [Expr]
unfoldApp Expr
lhs
  -- recursive calls come later in this ordering
  commutsort :: Expr -> Expr
commutsort (Expr
eo :$ Expr
ex :$ Expr
ey)
    | Thy -> Expr -> Bool
isCommutative Thy
thy Expr
eo  =  if (Expr
ef Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expr -> [Expr]
vars Expr
ex, Expr
ex)
                               (Bool, Expr) -> (Bool, Expr) -> Bool
forall a. Ord a => a -> a -> Bool
<= (Expr
ef Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expr -> [Expr]
vars Expr
ey, Expr
ey)
                               then Expr
eo Expr -> Expr -> Expr
:$ Expr
ex Expr -> Expr -> Expr
:$ Expr
ey
                               else Expr
eo Expr -> Expr -> Expr
:$ Expr
ey Expr -> Expr -> Expr
:$ Expr
ex
  commutsort Expr
e  =  Expr
e

boolTy :: TypeRep
boolTy :: TypeRep
boolTy  =  Expr -> TypeRep
typ Expr
b_