-- |
-- Module      : Conjure.Reason
-- Copyright   : (c) 2021-2024 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)
--
-- This module re-exports some functions from "Test.Speculate"
-- along with a few additional utilities.
module Conjure.Reason
  ( Thy
  , rules
  , equations
  , invalid
  , canReduceTo
  , printThy
  , closureLimit
  , doubleCheck
  , normalize
  , theoryFromAtoms
  , isRootNormalC
  , isRootNormalE
  , isCommutative
  , commutativeOperators
  )
where

import Test.Speculate.Reason
  ( Thy
  , rules
  , equations
  , invalid
  , canReduceTo
  , printThy
  , closureLimit
  , doubleCheck
  , normalize
  )
import Test.Speculate.Engine (theoryFromAtoms)
import Conjure.Expr
import qualified Data.Express.Triexpr as T

--- normality checks ---

isRootNormal :: Thy -> Expr -> Bool
isRootNormal :: Thy -> Expr -> Bool
isRootNormal Thy
thy Expr
e  =  [(Expr, [(Expr, Expr)], Expr)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Expr, [(Expr, Expr)], Expr)] -> Bool)
-> [(Expr, [(Expr, Expr)], Expr)] -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Triexpr Expr -> [(Expr, [(Expr, Expr)], Expr)]
forall a. Expr -> Triexpr a -> [(Expr, [(Expr, Expr)], a)]
T.lookup Expr
e Triexpr Expr
trie
  where
  trie :: Triexpr Expr
trie  =  [(Expr, Expr)] -> Triexpr Expr
forall a. [(Expr, a)] -> Triexpr a
T.fromList (Thy -> [(Expr, Expr)]
rules Thy
thy)

-- the logic of this function is a bit twisted for performance
-- but nevertheless correct
isRootNormalC :: Thy -> Expr -> Bool
isRootNormalC :: Thy -> Expr -> Bool
isRootNormalC Thy
thy Expr
e | Bool -> Bool
not (Thy -> Expr -> Bool
isRootNormal Thy
thy Expr
e)  =  Bool
False
isRootNormalC Thy
thy (Expr
ef :$ Expr
ex :$ Expr
ey)
  | Expr
ex Expr -> Expr -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr
ey  =  Bool
True
  | Bool -> Bool
not (Thy -> Expr -> Bool
isCommutative Thy
thy Expr
ef)  =  Bool
True
  | Thy -> Expr -> Bool
isRootNormal Thy
thy (Expr
ef Expr -> Expr -> Expr
:$ Expr
ey Expr -> Expr -> Expr
:$ Expr
ex)  =  Bool
False
isRootNormalC Thy
_ Expr
_  =  Bool
True

isRootNormalE :: Thy -> Expr -> Bool
isRootNormalE :: Thy -> Expr -> Bool
isRootNormalE Thy
thy Expr
e  =  Thy -> Expr -> Bool
isRootNormal Thy
thy Expr
e
                    Bool -> Bool -> Bool
&&  [Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr
e Expr -> Expr -> Bool
->-) [Expr
e2 Expr -> [(Expr, Expr)] -> Expr
//- [(Expr, Expr)]
bs | (Expr
_,[(Expr, Expr)]
bs,Expr
e2) <- Expr -> Triexpr Expr -> [(Expr, [(Expr, Expr)], Expr)]
forall a. Expr -> Triexpr a -> [(Expr, [(Expr, Expr)], a)]
T.lookup Expr
e Triexpr Expr
trie])
  where
  trie :: Triexpr Expr
trie  =  [(Expr, Expr)] -> Triexpr Expr
forall a. [(Expr, a)] -> Triexpr a
T.fromList ([(Expr, Expr)] -> Triexpr Expr) -> [(Expr, Expr)] -> Triexpr Expr
forall a b. (a -> b) -> a -> b
$ Thy -> [(Expr, Expr)]
equations Thy
thy [(Expr, Expr)] -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. [a] -> [a] -> [a]
++ ((Expr, Expr) -> (Expr, Expr)) -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> (Expr, Expr)
forall a b. (a, b) -> (b, a)
swap (Thy -> [(Expr, Expr)]
equations Thy
thy)
  ->- :: Expr -> Expr -> Bool
(->-)  =  Thy -> Expr -> Expr -> Bool
canReduceTo Thy
thy

isCommutative :: Thy -> Expr -> Bool
isCommutative :: Thy -> Expr -> Bool
isCommutative Thy
thy Expr
eo  =  Expr
eo Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Thy -> [Expr]
commutativeOperators Thy
thy

commutativeOperators :: Thy -> [Expr]
commutativeOperators :: Thy -> [Expr]
commutativeOperators Thy
thy  =  [ Expr
ef
                             | (Expr
ef :$ Expr
ex :$ Expr
ey, Expr
ef' :$ Expr
ey' :$ Expr
ex') <- Thy -> [(Expr, Expr)]
equations Thy
thy
                             , Expr
ef Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ef'
                             , Expr
ex Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ex'
                             , Expr
ey Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ey'
                             ]