{-# LANGUAGE NoMonomorphismRestriction, RecordWildCards
  , StandaloneDeriving, MultiParamTypeClasses, FunctionalDependencies
  , TypeSynonymInstances, FlexibleInstances, FlexibleContexts
  , UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving
  , OverloadedStrings, RankNTypes
  #-}
{-# OPTIONS -Wall #-}

module Codec.TPTP.Diff(Diffable(..),DiffResult(..),T0Diff,F0Diff,isSame,diffGenF,diffGenT,printSampleDiffs) where


-- Warning: This module is a MESS (but it seems to work :)).

import Prelude hiding ((<$>))

import Data.Generics
import Test.QuickCheck hiding((.&.))
import Codec.TPTP.Base
import Codec.TPTP.Pretty
import Prettyprinter
import Prettyprinter.Render.Terminal
import Control.Monad
import Control.Monad.Identity


text :: String -> Doc ann
text :: forall ann. String -> Doc ann
text = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty


data DiffResult d =
          Same -- ^ Both arguments are the same.
        | SameHead d -- ^ The arguments are recursive expressions of the same form, but their subterms differ. Return a \"decorated\" term that shows where the differences are
        | Differ d d -- ^ The arguments differ and are not of similar form (don't recurse)
        | DontCare
    deriving (DiffResult d -> DiffResult d -> Bool
(DiffResult d -> DiffResult d -> Bool)
-> (DiffResult d -> DiffResult d -> Bool) -> Eq (DiffResult d)
forall d. Eq d => DiffResult d -> DiffResult d -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall d. Eq d => DiffResult d -> DiffResult d -> Bool
== :: DiffResult d -> DiffResult d -> Bool
$c/= :: forall d. Eq d => DiffResult d -> DiffResult d -> Bool
/= :: DiffResult d -> DiffResult d -> Bool
Eq,Eq (DiffResult d)
Eq (DiffResult d) =>
(DiffResult d -> DiffResult d -> Ordering)
-> (DiffResult d -> DiffResult d -> Bool)
-> (DiffResult d -> DiffResult d -> Bool)
-> (DiffResult d -> DiffResult d -> Bool)
-> (DiffResult d -> DiffResult d -> Bool)
-> (DiffResult d -> DiffResult d -> DiffResult d)
-> (DiffResult d -> DiffResult d -> DiffResult d)
-> Ord (DiffResult d)
DiffResult d -> DiffResult d -> Bool
DiffResult d -> DiffResult d -> Ordering
DiffResult d -> DiffResult d -> DiffResult d
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall d. Ord d => Eq (DiffResult d)
forall d. Ord d => DiffResult d -> DiffResult d -> Bool
forall d. Ord d => DiffResult d -> DiffResult d -> Ordering
forall d. Ord d => DiffResult d -> DiffResult d -> DiffResult d
$ccompare :: forall d. Ord d => DiffResult d -> DiffResult d -> Ordering
compare :: DiffResult d -> DiffResult d -> Ordering
$c< :: forall d. Ord d => DiffResult d -> DiffResult d -> Bool
< :: DiffResult d -> DiffResult d -> Bool
$c<= :: forall d. Ord d => DiffResult d -> DiffResult d -> Bool
<= :: DiffResult d -> DiffResult d -> Bool
$c> :: forall d. Ord d => DiffResult d -> DiffResult d -> Bool
> :: DiffResult d -> DiffResult d -> Bool
$c>= :: forall d. Ord d => DiffResult d -> DiffResult d -> Bool
>= :: DiffResult d -> DiffResult d -> Bool
$cmax :: forall d. Ord d => DiffResult d -> DiffResult d -> DiffResult d
max :: DiffResult d -> DiffResult d -> DiffResult d
$cmin :: forall d. Ord d => DiffResult d -> DiffResult d -> DiffResult d
min :: DiffResult d -> DiffResult d -> DiffResult d
Ord,Int -> DiffResult d -> ShowS
[DiffResult d] -> ShowS
DiffResult d -> String
(Int -> DiffResult d -> ShowS)
-> (DiffResult d -> String)
-> ([DiffResult d] -> ShowS)
-> Show (DiffResult d)
forall d. Show d => Int -> DiffResult d -> ShowS
forall d. Show d => [DiffResult d] -> ShowS
forall d. Show d => DiffResult d -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall d. Show d => Int -> DiffResult d -> ShowS
showsPrec :: Int -> DiffResult d -> ShowS
$cshow :: forall d. Show d => DiffResult d -> String
show :: DiffResult d -> String
$cshowList :: forall d. Show d => [DiffResult d] -> ShowS
showList :: [DiffResult d] -> ShowS
Show,Typeable (DiffResult d)
Typeable (DiffResult d) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DiffResult d -> c (DiffResult d))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (DiffResult d))
-> (DiffResult d -> Constr)
-> (DiffResult d -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (DiffResult d)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (DiffResult d)))
-> ((forall b. Data b => b -> b) -> DiffResult d -> DiffResult d)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DiffResult d -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DiffResult d -> r)
-> (forall u. (forall d. Data d => d -> u) -> DiffResult d -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DiffResult d -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d))
-> Data (DiffResult d)
DiffResult d -> Constr
DiffResult d -> DataType
(forall b. Data b => b -> b) -> DiffResult d -> DiffResult d
forall d. Data d => Typeable (DiffResult d)
forall d. Data d => DiffResult d -> Constr
forall d. Data d => DiffResult d -> DataType
forall d.
Data d =>
(forall b. Data b => b -> b) -> DiffResult d -> DiffResult d
forall d u.
Data d =>
Int -> (forall d. Data d => d -> u) -> DiffResult d -> u
forall d u.
Data d =>
(forall d. Data d => d -> u) -> DiffResult d -> [u]
forall d r r'.
Data d =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DiffResult d -> r
forall d r r'.
Data d =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DiffResult d -> r
forall d (m :: * -> *).
(Data d, Monad m) =>
(forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d)
forall d (m :: * -> *).
(Data d, MonadPlus m) =>
(forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d)
forall d (c :: * -> *).
Data d =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (DiffResult d)
forall d (c :: * -> *).
Data d =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DiffResult d -> c (DiffResult d)
forall d (t :: * -> *) (c :: * -> *).
(Data d, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (DiffResult d))
forall d (t :: * -> * -> *) (c :: * -> *).
(Data d, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (DiffResult d))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DiffResult d -> u
forall u. (forall d. Data d => d -> u) -> DiffResult d -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DiffResult d -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DiffResult d -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (DiffResult d)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DiffResult d -> c (DiffResult d)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (DiffResult d))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (DiffResult d))
$cgfoldl :: forall d (c :: * -> *).
Data d =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DiffResult d -> c (DiffResult d)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DiffResult d -> c (DiffResult d)
$cgunfold :: forall d (c :: * -> *).
Data d =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (DiffResult d)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (DiffResult d)
$ctoConstr :: forall d. Data d => DiffResult d -> Constr
toConstr :: DiffResult d -> Constr
$cdataTypeOf :: forall d. Data d => DiffResult d -> DataType
dataTypeOf :: DiffResult d -> DataType
$cdataCast1 :: forall d (t :: * -> *) (c :: * -> *).
(Data d, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (DiffResult d))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (DiffResult d))
$cdataCast2 :: forall d (t :: * -> * -> *) (c :: * -> *).
(Data d, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (DiffResult d))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (DiffResult d))
$cgmapT :: forall d.
Data d =>
(forall b. Data b => b -> b) -> DiffResult d -> DiffResult d
gmapT :: (forall b. Data b => b -> b) -> DiffResult d -> DiffResult d
$cgmapQl :: forall d r r'.
Data d =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DiffResult d -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DiffResult d -> r
$cgmapQr :: forall d r r'.
Data d =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DiffResult d -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DiffResult d -> r
$cgmapQ :: forall d u.
Data d =>
(forall d. Data d => d -> u) -> DiffResult d -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> DiffResult d -> [u]
$cgmapQi :: forall d u.
Data d =>
Int -> (forall d. Data d => d -> u) -> DiffResult d -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DiffResult d -> u
$cgmapM :: forall d (m :: * -> *).
(Data d, Monad m) =>
(forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d)
$cgmapMp :: forall d (m :: * -> *).
(Data d, MonadPlus m) =>
(forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d)
$cgmapMo :: forall d (m :: * -> *).
(Data d, MonadPlus m) =>
(forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DiffResult d -> m (DiffResult d)
Data,Typeable,ReadPrec [DiffResult d]
ReadPrec (DiffResult d)
Int -> ReadS (DiffResult d)
ReadS [DiffResult d]
(Int -> ReadS (DiffResult d))
-> ReadS [DiffResult d]
-> ReadPrec (DiffResult d)
-> ReadPrec [DiffResult d]
-> Read (DiffResult d)
forall d. Read d => ReadPrec [DiffResult d]
forall d. Read d => ReadPrec (DiffResult d)
forall d. Read d => Int -> ReadS (DiffResult d)
forall d. Read d => ReadS [DiffResult d]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall d. Read d => Int -> ReadS (DiffResult d)
readsPrec :: Int -> ReadS (DiffResult d)
$creadList :: forall d. Read d => ReadS [DiffResult d]
readList :: ReadS [DiffResult d]
$creadPrec :: forall d. Read d => ReadPrec (DiffResult d)
readPrec :: ReadPrec (DiffResult d)
$creadListPrec :: forall d. Read d => ReadPrec [DiffResult d]
readListPrec :: ReadPrec [DiffResult d]
Read)

isSame :: forall t. DiffResult t -> Bool
isSame :: forall t. DiffResult t -> Bool
isSame DiffResult t
Same = Bool
True
isSame DiffResult t
_ = Bool
False

-- | Abstraction for diff'ing [predicate symbol|function symbol|gdata] applications
-- Suggestive variable names for the case of function symbol applications
handleAppExpr :: (Eq str) =>
                (term -> term -> termfix DiffResult) -- ^ the diff function

              -> (DiffResult a -> termfix DiffResult) -- ^ newtype wrapper
              -> (termfix DiffResult -> DiffResult a) -- ^ newtype unwrapper

              -> (str -> [termfix DiffResult] -> b) -- ^ Application expression constructor

              -> str -- ^ First funsym
              -> [term] -- ^ First args

              -> str -- ^ Second funsum
              -> [term] -- ^ Second args

              -> DiffResult b
handleAppExpr :: forall str term (termfix :: (* -> *) -> *) a b.
Eq str =>
(term -> term -> termfix DiffResult)
-> (DiffResult a -> termfix DiffResult)
-> (termfix DiffResult -> DiffResult a)
-> (str -> [termfix DiffResult] -> b)
-> str
-> [term]
-> str
-> [term]
-> DiffResult b
handleAppExpr term -> term -> termfix DiffResult
recFun DiffResult a -> termfix DiffResult
newtypewrapper termfix DiffResult -> DiffResult a
newtypeunwrapper str -> [termfix DiffResult] -> b
constr str
x1 [term]
args1 str
x2 [term]
args2 =
                 -- recurse if heads and arities agree
                 case (str
x1str -> str -> Bool
forall a. Eq a => a -> a -> Bool
==str
x2 Bool -> Bool -> Bool
&& [term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [term]
args1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [term]
args2) of
                   Bool
True ->
                       let
                           rec' :: [termfix DiffResult]
rec' = (term -> term -> termfix DiffResult)
-> [term] -> [term] -> [termfix DiffResult]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith term -> term -> termfix DiffResult
recFun [term]
args1 [term]
args2
                       in
                         case (termfix DiffResult -> Bool) -> [termfix DiffResult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (DiffResult a -> Bool
forall t. DiffResult t -> Bool
isSame (DiffResult a -> Bool)
-> (termfix DiffResult -> DiffResult a)
-> termfix DiffResult
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. termfix DiffResult -> DiffResult a
newtypeunwrapper) [termfix DiffResult]
rec' of
                           Bool
True -> DiffResult b
forall d. DiffResult d
Same
                           Bool
False -> b -> DiffResult b
forall d. d -> DiffResult d
SameHead (str -> [termfix DiffResult] -> b
constr str
x1 [termfix DiffResult]
rec')

                   Bool
False ->
                       b -> b -> DiffResult b
forall d. d -> d -> DiffResult d
Differ (str -> [termfix DiffResult] -> b
constr str
x1 ((term -> termfix DiffResult) -> [term] -> [termfix DiffResult]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (termfix DiffResult -> term -> termfix DiffResult
forall a b. a -> b -> a
const (termfix DiffResult -> term -> termfix DiffResult)
-> (DiffResult a -> termfix DiffResult)
-> DiffResult a
-> term
-> termfix DiffResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiffResult a -> termfix DiffResult
newtypewrapper (DiffResult a -> term -> termfix DiffResult)
-> DiffResult a -> term -> termfix DiffResult
forall a b. (a -> b) -> a -> b
$ DiffResult a
forall d. DiffResult d
DontCare) [term]
args1))
                              (str -> [termfix DiffResult] -> b
constr str
x2 ((term -> termfix DiffResult) -> [term] -> [termfix DiffResult]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (termfix DiffResult -> term -> termfix DiffResult
forall a b. a -> b -> a
const (termfix DiffResult -> term -> termfix DiffResult)
-> (DiffResult a -> termfix DiffResult)
-> DiffResult a
-> term
-> termfix DiffResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiffResult a -> termfix DiffResult
newtypewrapper (DiffResult a -> term -> termfix DiffResult)
-> DiffResult a -> term -> termfix DiffResult
forall a b. (a -> b) -> a -> b
$ DiffResult a
forall d. DiffResult d
DontCare) [term]
args2))

handleBinExpr ::
                 (Eq op) =>
                 (term -> term -> termfix DiffResult)

                 -> (DiffResult a -> termfix DiffResult) -- ^ NT wrapper
                 -> (termfix DiffResult -> DiffResult a) -- ^ NT unwrapepr

                 -> (termfix DiffResult -> op -> termfix DiffResult -> b) -- ^ constructor

                 -> term
                 -> op
                 -> term

                 -> term
                 -> op
                 -> term

                 -> DiffResult b
handleBinExpr :: forall op term (termfix :: (* -> *) -> *) a b.
Eq op =>
(term -> term -> termfix DiffResult)
-> (DiffResult a -> termfix DiffResult)
-> (termfix DiffResult -> DiffResult a)
-> (termfix DiffResult -> op -> termfix DiffResult -> b)
-> term
-> op
-> term
-> term
-> op
-> term
-> DiffResult b
handleBinExpr term -> term -> termfix DiffResult
recFun DiffResult a -> termfix DiffResult
newtypewrapper termfix DiffResult -> DiffResult a
newtypeunwrapper termfix DiffResult -> op -> termfix DiffResult -> b
constr term
l1 op
op1 term
r1 term
l2 op
op2 term
r2 =
    case op
op1op -> op -> Bool
forall a. Eq a => a -> a -> Bool
==op
op2 of
      Bool
True ->
          let
              recl :: termfix DiffResult
recl = term -> term -> termfix DiffResult
recFun term
l1 term
l2
              recr :: termfix DiffResult
recr = term -> term -> termfix DiffResult
recFun term
r1 term
r2
          in
            case (termfix DiffResult -> DiffResult a
newtypeunwrapper termfix DiffResult
recl,termfix DiffResult -> DiffResult a
newtypeunwrapper termfix DiffResult
recr) of
              (DiffResult a
Same,DiffResult a
Same) -> DiffResult b
forall d. DiffResult d
Same
              (DiffResult a
_,DiffResult a
_)       -> b -> DiffResult b
forall d. d -> DiffResult d
SameHead (termfix DiffResult -> op -> termfix DiffResult -> b
constr termfix DiffResult
recl op
op1 termfix DiffResult
recr)

      Bool
False ->
          let dc :: termfix DiffResult
dc = DiffResult a -> termfix DiffResult
newtypewrapper DiffResult a
forall d. DiffResult d
DontCare

          in b -> b -> DiffResult b
forall d. d -> d -> DiffResult d
Differ (termfix DiffResult -> op -> termfix DiffResult -> b
constr termfix DiffResult
dc op
op1 termfix DiffResult
dc)
                    (termfix DiffResult -> op -> termfix DiffResult -> b
constr termfix DiffResult
dc op
op2 termfix DiffResult
dc)

handleUnary ::
                 (term -> term -> termfix DiffResult)

                 -> (DiffResult a -> termfix DiffResult) -- ^ NT wrapper
                 -> (termfix DiffResult -> DiffResult a) -- ^ NT unwrapepr

                 -> (termfix DiffResult -> b) -- ^ constructor

                 -> term

                 -> term

                 -> DiffResult b

handleUnary :: forall term (termfix :: (* -> *) -> *) a b.
(term -> term -> termfix DiffResult)
-> (DiffResult a -> termfix DiffResult)
-> (termfix DiffResult -> DiffResult a)
-> (termfix DiffResult -> b)
-> term
-> term
-> DiffResult b
handleUnary term -> term -> termfix DiffResult
recFun DiffResult a -> termfix DiffResult
_ termfix DiffResult -> DiffResult a
newtypeunwrapper termfix DiffResult -> b
constr term
r1 term
r2 =
          let
              rec' :: termfix DiffResult
rec' = term -> term -> termfix DiffResult
recFun term
r1 term
r2
          in
            case termfix DiffResult -> DiffResult a
newtypeunwrapper termfix DiffResult
rec' of
              DiffResult a
Same -> DiffResult b
forall d. DiffResult d
Same
              DiffResult a
_    -> b -> DiffResult b
forall d. d -> DiffResult d
SameHead (termfix DiffResult -> b
constr termfix DiffResult
rec')



handleLeaf ::
              (Eq a) =>
              (a -> d) -> a -> a -> DiffResult d
handleLeaf :: forall a d. Eq a => (a -> d) -> a -> a -> DiffResult d
handleLeaf a -> d
constr a
x1 a
x2 =
    if a
x1a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==a
x2
    then DiffResult d
forall d. DiffResult d
Same
    else d -> d -> DiffResult d
forall d. d -> d -> DiffResult d
Differ (a -> d
constr a
x1) (a -> d
constr a
x2)



-- runDiffTerm :: Term
--                -> Term
--                -> DiffResult (Term0 (T DiffResult))
-- runDiffTerm t1 t2 = runT (diffTerm t1 t2)

diffTerm :: Term -> Term -> T DiffResult
diffTerm :: Term -> Term -> T DiffResult
diffTerm (T (Identity Term0 Term
t1)) (T (Identity Term0 Term
t2)) = DiffResult (Term0 (T DiffResult)) -> T DiffResult
forall (c :: * -> *). c (Term0 (T c)) -> T c
T (DiffResult (Term0 (T DiffResult)) -> T DiffResult)
-> DiffResult (Term0 (T DiffResult)) -> T DiffResult
forall a b. (a -> b) -> a -> b
$
    case (Term0 Term
t1,Term0 Term
t2) of
      (FunApp AtomicWord
x1 [Term]
args1,FunApp AtomicWord
x2 [Term]
args2) -> (Term -> Term -> T DiffResult)
-> (DiffResult (Term0 (T DiffResult)) -> T DiffResult)
-> (T DiffResult -> DiffResult (Term0 (T DiffResult)))
-> (AtomicWord -> [T DiffResult] -> Term0 (T DiffResult))
-> AtomicWord
-> [Term]
-> AtomicWord
-> [Term]
-> DiffResult (Term0 (T DiffResult))
forall str term (termfix :: (* -> *) -> *) a b.
Eq str =>
(term -> term -> termfix DiffResult)
-> (DiffResult a -> termfix DiffResult)
-> (termfix DiffResult -> DiffResult a)
-> (str -> [termfix DiffResult] -> b)
-> str
-> [term]
-> str
-> [term]
-> DiffResult b
handleAppExpr Term -> Term -> T DiffResult
diffTerm DiffResult (Term0 (T DiffResult)) -> T DiffResult
forall (c :: * -> *). c (Term0 (T c)) -> T c
T T DiffResult -> DiffResult (Term0 (T DiffResult))
forall (c :: * -> *). T c -> c (Term0 (T c))
runT AtomicWord -> [T DiffResult] -> Term0 (T DiffResult)
forall term. AtomicWord -> [term] -> Term0 term
FunApp AtomicWord
x1 [Term]
args1 AtomicWord
x2 [Term]
args2
      (Var V
x1,Var V
x2) -> (V -> Term0 (T DiffResult))
-> V -> V -> DiffResult (Term0 (T DiffResult))
forall a d. Eq a => (a -> d) -> a -> a -> DiffResult d
handleLeaf V -> Term0 (T DiffResult)
forall term. V -> Term0 term
Var V
x1 V
x2
      (DistinctObjectTerm String
x1, DistinctObjectTerm String
x2) -> (String -> Term0 (T DiffResult))
-> String -> String -> DiffResult (Term0 (T DiffResult))
forall a d. Eq a => (a -> d) -> a -> a -> DiffResult d
handleLeaf String -> Term0 (T DiffResult)
forall term. String -> Term0 term
DistinctObjectTerm String
x1 String
x2
      (NumberLitTerm Rational
x1, NumberLitTerm Rational
x2) -> (Rational -> Term0 (T DiffResult))
-> Rational -> Rational -> DiffResult (Term0 (T DiffResult))
forall a d. Eq a => (a -> d) -> a -> a -> DiffResult d
handleLeaf Rational -> Term0 (T DiffResult)
forall term. Rational -> Term0 term
NumberLitTerm Rational
x1 Rational
x2
      (Term0 Term, Term0 Term)
_ -> let plug :: Term0 a1 -> Term0 (T DiffResult)
plug=T DiffResult -> Term0 a1 -> Term0 (T DiffResult)
forall a a1. a -> Term0 a1 -> Term0 a
plugSubterms (DiffResult (Term0 (T DiffResult)) -> T DiffResult
forall (c :: * -> *). c (Term0 (T c)) -> T c
T DiffResult (Term0 (T DiffResult))
forall d. DiffResult d
DontCare) in Term0 (T DiffResult)
-> Term0 (T DiffResult) -> DiffResult (Term0 (T DiffResult))
forall d. d -> d -> DiffResult d
Differ (Term0 Term -> Term0 (T DiffResult)
forall {a1}. Term0 a1 -> Term0 (T DiffResult)
plug Term0 Term
t1) (Term0 Term -> Term0 (T DiffResult)
forall {a1}. Term0 a1 -> Term0 (T DiffResult)
plug Term0 Term
t2)

plugSubterms :: forall a a1. a -> Term0 a1 -> Term0 a
plugSubterms :: forall a a1. a -> Term0 a1 -> Term0 a
plugSubterms a
p Term0 a1
t = case Term0 a1
t of
                            FunApp AtomicWord
x1 [a1]
args -> AtomicWord -> [a] -> Term0 a
forall term. AtomicWord -> [term] -> Term0 term
FunApp AtomicWord
x1 ((a1 -> a) -> [a1] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> a1 -> a
forall a b. a -> b -> a
const a
p) [a1]
args)
                            DistinctObjectTerm String
x1 -> String -> Term0 a
forall term. String -> Term0 term
DistinctObjectTerm String
x1
                            NumberLitTerm Rational
x1 -> Rational -> Term0 a
forall term. Rational -> Term0 term
NumberLitTerm Rational
x1
                            Var V
x1 -> V -> Term0 a
forall term. V -> Term0 term
Var V
x1

plugSubformulae :: forall a formula a1 t.
                   a -> formula -> Formula0 a1 t -> Formula0 a formula
plugSubformulae :: forall a formula a1 t.
a -> formula -> Formula0 a1 t -> Formula0 a formula
plugSubformulae a
pt formula
pf Formula0 a1 t
f = case Formula0 a1 t
f of
                               Quant Quant
q [V]
vars t
_ -> Quant -> [V] -> formula -> Formula0 a formula
forall term formula.
Quant -> [V] -> formula -> Formula0 term formula
Quant Quant
q [V]
vars formula
pf
                               PredApp AtomicWord
x1 [a1]
args -> AtomicWord -> [a] -> Formula0 a formula
forall term formula. AtomicWord -> [term] -> Formula0 term formula
PredApp AtomicWord
x1 ((a1 -> a) -> [a1] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> a1 -> a
forall a b. a -> b -> a
const a
pt) [a1]
args)
                               BinOp t
_ BinOp
b t
_ -> formula -> BinOp -> formula -> Formula0 a formula
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp formula
pf BinOp
b formula
pf
                               InfixPred a1
_ InfixPred
b a1
_ -> a -> InfixPred -> a -> Formula0 a formula
forall term formula.
term -> InfixPred -> term -> Formula0 term formula
InfixPred a
pt InfixPred
b a
pt
                               (:~:) t
_ -> formula -> Formula0 a formula
forall term formula. formula -> Formula0 term formula
(:~:) formula
pf



diffFormula :: Formula -> Formula -> F DiffResult
diffFormula :: Formula -> Formula -> F DiffResult
diffFormula (F (Identity Formula0 Term Formula
f1)) (F (Identity Formula0 Term Formula
f2)) = DiffResult (Formula0 (T DiffResult) (F DiffResult)) -> F DiffResult
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F (DiffResult (Formula0 (T DiffResult) (F DiffResult))
 -> F DiffResult)
-> DiffResult (Formula0 (T DiffResult) (F DiffResult))
-> F DiffResult
forall a b. (a -> b) -> a -> b
$
    case (Formula0 Term Formula
f1,Formula0 Term Formula
f2) of
      ( Quant Quant
q1 [V]
vars1 Formula
g1
       ,Quant Quant
q2 [V]
vars2 Formula
g2) ->
          case (Quant
q1Quant -> Quant -> Bool
forall a. Eq a => a -> a -> Bool
==Quant
q2, [V]
vars1[V] -> [V] -> Bool
forall a. Eq a => a -> a -> Bool
==[V]
vars2) of
            (Bool
True,Bool
True) -> (Formula -> Formula -> F DiffResult)
-> (DiffResult (Formula0 (T DiffResult) (F DiffResult))
    -> F DiffResult)
-> (F DiffResult
    -> DiffResult (Formula0 (T DiffResult) (F DiffResult)))
-> (F DiffResult -> Formula0 (T DiffResult) (F DiffResult))
-> Formula
-> Formula
-> DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall term (termfix :: (* -> *) -> *) a b.
(term -> term -> termfix DiffResult)
-> (DiffResult a -> termfix DiffResult)
-> (termfix DiffResult -> DiffResult a)
-> (termfix DiffResult -> b)
-> term
-> term
-> DiffResult b
handleUnary Formula -> Formula -> F DiffResult
diffFormula DiffResult (Formula0 (T DiffResult) (F DiffResult)) -> F DiffResult
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F F DiffResult -> DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall (c :: * -> *). F c -> c (Formula0 (T c) (F c))
runF (Quant
-> [V] -> F DiffResult -> Formula0 (T DiffResult) (F DiffResult)
forall term formula.
Quant -> [V] -> formula -> Formula0 term formula
Quant Quant
q1 [V]
vars1) Formula
g1 Formula
g2
            (Bool, Bool)
_ -> Formula0 (T DiffResult) (F DiffResult)
-> Formula0 (T DiffResult) (F DiffResult)
-> DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall d. d -> d -> DiffResult d
Differ (Quant
-> [V] -> F DiffResult -> Formula0 (T DiffResult) (F DiffResult)
forall term formula.
Quant -> [V] -> formula -> Formula0 term formula
Quant Quant
q1 [V]
vars1 (DiffResult (Formula0 (T DiffResult) (F DiffResult)) -> F DiffResult
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall d. DiffResult d
DontCare))
                       (Quant
-> [V] -> F DiffResult -> Formula0 (T DiffResult) (F DiffResult)
forall term formula.
Quant -> [V] -> formula -> Formula0 term formula
Quant Quant
q2 [V]
vars2 (DiffResult (Formula0 (T DiffResult) (F DiffResult)) -> F DiffResult
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall d. DiffResult d
DontCare))


      ( BinOp Formula
l1 BinOp
op1 Formula
r1
       ,BinOp Formula
l2 BinOp
op2 Formula
r2 ) -> (Formula -> Formula -> F DiffResult)
-> (DiffResult (Formula0 (T DiffResult) (F DiffResult))
    -> F DiffResult)
-> (F DiffResult
    -> DiffResult (Formula0 (T DiffResult) (F DiffResult)))
-> (F DiffResult
    -> BinOp -> F DiffResult -> Formula0 (T DiffResult) (F DiffResult))
-> Formula
-> BinOp
-> Formula
-> Formula
-> BinOp
-> Formula
-> DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall op term (termfix :: (* -> *) -> *) a b.
Eq op =>
(term -> term -> termfix DiffResult)
-> (DiffResult a -> termfix DiffResult)
-> (termfix DiffResult -> DiffResult a)
-> (termfix DiffResult -> op -> termfix DiffResult -> b)
-> term
-> op
-> term
-> term
-> op
-> term
-> DiffResult b
handleBinExpr Formula -> Formula -> F DiffResult
diffFormula DiffResult (Formula0 (T DiffResult) (F DiffResult)) -> F DiffResult
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F F DiffResult -> DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall (c :: * -> *). F c -> c (Formula0 (T c) (F c))
runF F DiffResult
-> BinOp -> F DiffResult -> Formula0 (T DiffResult) (F DiffResult)
forall term formula.
formula -> BinOp -> formula -> Formula0 term formula
BinOp Formula
l1 BinOp
op1 Formula
r1 Formula
l2 BinOp
op2 Formula
r2

      ( InfixPred Term
l1 InfixPred
op1 Term
r1
       ,InfixPred Term
l2 InfixPred
op2 Term
r2 ) -> (Term -> Term -> T DiffResult)
-> (DiffResult (Term0 (T DiffResult)) -> T DiffResult)
-> (T DiffResult -> DiffResult (Term0 (T DiffResult)))
-> (T DiffResult
    -> InfixPred
    -> T DiffResult
    -> Formula0 (T DiffResult) (F DiffResult))
-> Term
-> InfixPred
-> Term
-> Term
-> InfixPred
-> Term
-> DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall op term (termfix :: (* -> *) -> *) a b.
Eq op =>
(term -> term -> termfix DiffResult)
-> (DiffResult a -> termfix DiffResult)
-> (termfix DiffResult -> DiffResult a)
-> (termfix DiffResult -> op -> termfix DiffResult -> b)
-> term
-> op
-> term
-> term
-> op
-> term
-> DiffResult b
handleBinExpr Term -> Term -> T DiffResult
diffTerm DiffResult (Term0 (T DiffResult)) -> T DiffResult
forall (c :: * -> *). c (Term0 (T c)) -> T c
T T DiffResult -> DiffResult (Term0 (T DiffResult))
forall (c :: * -> *). T c -> c (Term0 (T c))
runT T DiffResult
-> InfixPred
-> T DiffResult
-> Formula0 (T DiffResult) (F DiffResult)
forall term formula.
term -> InfixPred -> term -> Formula0 term formula
InfixPred Term
l1 InfixPred
op1 Term
r1 Term
l2 InfixPred
op2 Term
r2

      ( (:~:) Formula
g1
       ,(:~:) Formula
g2 ) -> (Formula -> Formula -> F DiffResult)
-> (DiffResult (Formula0 (T DiffResult) (F DiffResult))
    -> F DiffResult)
-> (F DiffResult
    -> DiffResult (Formula0 (T DiffResult) (F DiffResult)))
-> (F DiffResult -> Formula0 (T DiffResult) (F DiffResult))
-> Formula
-> Formula
-> DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall term (termfix :: (* -> *) -> *) a b.
(term -> term -> termfix DiffResult)
-> (DiffResult a -> termfix DiffResult)
-> (termfix DiffResult -> DiffResult a)
-> (termfix DiffResult -> b)
-> term
-> term
-> DiffResult b
handleUnary Formula -> Formula -> F DiffResult
diffFormula DiffResult (Formula0 (T DiffResult) (F DiffResult)) -> F DiffResult
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F F DiffResult -> DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall (c :: * -> *). F c -> c (Formula0 (T c) (F c))
runF F DiffResult -> Formula0 (T DiffResult) (F DiffResult)
forall term formula. formula -> Formula0 term formula
(:~:) Formula
g1 Formula
g2


      ( PredApp AtomicWord
x1 [Term]
args1
       ,PredApp AtomicWord
x2 [Term]
args2 ) -> (Term -> Term -> T DiffResult)
-> (DiffResult (Term0 (T DiffResult)) -> T DiffResult)
-> (T DiffResult -> DiffResult (Term0 (T DiffResult)))
-> (AtomicWord
    -> [T DiffResult] -> Formula0 (T DiffResult) (F DiffResult))
-> AtomicWord
-> [Term]
-> AtomicWord
-> [Term]
-> DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall str term (termfix :: (* -> *) -> *) a b.
Eq str =>
(term -> term -> termfix DiffResult)
-> (DiffResult a -> termfix DiffResult)
-> (termfix DiffResult -> DiffResult a)
-> (str -> [termfix DiffResult] -> b)
-> str
-> [term]
-> str
-> [term]
-> DiffResult b
handleAppExpr Term -> Term -> T DiffResult
diffTerm DiffResult (Term0 (T DiffResult)) -> T DiffResult
forall (c :: * -> *). c (Term0 (T c)) -> T c
T T DiffResult -> DiffResult (Term0 (T DiffResult))
forall (c :: * -> *). T c -> c (Term0 (T c))
runT AtomicWord
-> [T DiffResult] -> Formula0 (T DiffResult) (F DiffResult)
forall term formula. AtomicWord -> [term] -> Formula0 term formula
PredApp AtomicWord
x1 [Term]
args1 AtomicWord
x2 [Term]
args2

      (Formula0 Term Formula, Formula0 Term Formula)
_ -> let plug :: Formula0 a1 t -> Formula0 (T DiffResult) (F DiffResult)
plug=T DiffResult
-> F DiffResult
-> Formula0 a1 t
-> Formula0 (T DiffResult) (F DiffResult)
forall a formula a1 t.
a -> formula -> Formula0 a1 t -> Formula0 a formula
plugSubformulae (DiffResult (Term0 (T DiffResult)) -> T DiffResult
forall (c :: * -> *). c (Term0 (T c)) -> T c
T DiffResult (Term0 (T DiffResult))
forall d. DiffResult d
DontCare) (DiffResult (Formula0 (T DiffResult) (F DiffResult)) -> F DiffResult
forall (c :: * -> *). c (Formula0 (T c) (F c)) -> F c
F DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall d. DiffResult d
DontCare) in Formula0 (T DiffResult) (F DiffResult)
-> Formula0 (T DiffResult) (F DiffResult)
-> DiffResult (Formula0 (T DiffResult) (F DiffResult))
forall d. d -> d -> DiffResult d
Differ (Formula0 Term Formula -> Formula0 (T DiffResult) (F DiffResult)
forall {a1} {t}.
Formula0 a1 t -> Formula0 (T DiffResult) (F DiffResult)
plug Formula0 Term Formula
f1) (Formula0 Term Formula -> Formula0 (T DiffResult) (F DiffResult)
forall {a1} {t}.
Formula0 a1 t -> Formula0 (T DiffResult) (F DiffResult)
plug Formula0 Term Formula
f2)


instance {-# OVERLAPPING #-} Show (T DiffResult) where
    show :: T DiffResult -> String
show (T DiffResult (Term0 (T DiffResult))
t) = DiffResult (Term0 (T DiffResult)) -> String
forall a. Show a => a -> String
show DiffResult (Term0 (T DiffResult))
t

instance {-# OVERLAPPING #-} Show (F DiffResult) where
    show :: F DiffResult -> String
show (F DiffResult (Formula0 (T DiffResult) (F DiffResult))
f) = DiffResult (Formula0 (T DiffResult) (F DiffResult)) -> String
forall a. Show a => a -> String
show DiffResult (Formula0 (T DiffResult) (F DiffResult))
f

type T0Diff = DiffResult (Term0 (T DiffResult))
type F0Diff = DiffResult (Formula0 (T DiffResult) (F DiffResult))


wildcard :: AtomicWord
wildcard :: AtomicWord
wildcard = AtomicWord
"_"

instance PrettyAnsi (WithEnclosing T0Diff) where
    prettyAnsi :: WithEnclosing (DiffResult (Term0 (T DiffResult))) -> Doc AnsiStyle
prettyAnsi = WithEnclosing (DiffResult (Term0 (T DiffResult))) -> Doc AnsiStyle
forall t.
PrettyAnsi (WithEnclosing t) =>
WithEnclosing (DiffResult t) -> Doc AnsiStyle
prettyHelper --(plugSubterms (fApp wildcard []))

instance PrettyAnsi (WithEnclosing F0Diff) where
    prettyAnsi :: WithEnclosing (DiffResult (Formula0 (T DiffResult) (F DiffResult)))
-> Doc AnsiStyle
prettyAnsi = WithEnclosing (DiffResult (Formula0 (T DiffResult) (F DiffResult)))
-> Doc AnsiStyle
forall t.
PrettyAnsi (WithEnclosing t) =>
WithEnclosing (DiffResult t) -> Doc AnsiStyle
prettyHelper --(plugSubformulae (fApp wildcard []) (pApp wildcard []))

prettyHelper :: forall t.
                (PrettyAnsi (WithEnclosing t)) =>
                WithEnclosing (DiffResult t) -> Doc AnsiStyle
prettyHelper :: forall t.
PrettyAnsi (WithEnclosing t) =>
WithEnclosing (DiffResult t) -> Doc AnsiStyle
prettyHelper (WithEnclosing Enclosing
_ DiffResult t
d) =
        let
            pwe :: a -> Doc AnsiStyle
pwe = WithEnclosing a -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (WithEnclosing a -> Doc AnsiStyle)
-> (a -> WithEnclosing a) -> a -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enclosing -> a -> WithEnclosing a
forall a. Enclosing -> a -> WithEnclosing a
WithEnclosing Enclosing
EnclNothing
        in
          case DiffResult t
d of
                 DiffResult t
DontCare -> AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
colorDull Color
White)(Doc AnsiStyle -> Doc AnsiStyle)
-> (AtomicWord -> Doc AnsiStyle) -> AtomicWord -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
.AtomicWord -> Doc AnsiStyle
forall a ann. Pretty a => a -> Doc ann
forall ann. AtomicWord -> Doc ann
pretty (AtomicWord -> Doc AnsiStyle) -> AtomicWord -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ AtomicWord
wildcard
                 DiffResult t
Same -> AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
colorDull Color
Green)(Doc AnsiStyle -> Doc AnsiStyle)
-> (String -> Doc AnsiStyle) -> String -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
.String -> Doc AnsiStyle
forall ann. String -> Doc ann
text (String -> Doc AnsiStyle) -> String -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ String
"Same"
                 SameHead t
x -> AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Blue) (Doc AnsiStyle -> Doc AnsiStyle)
-> ([Doc AnsiStyle] -> Doc AnsiStyle)
-> [Doc AnsiStyle]
-> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc AnsiStyle
-> Doc AnsiStyle
-> Doc AnsiStyle
-> [Doc AnsiStyle]
-> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep (String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
"{ SameHead ") (String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
"}") Doc AnsiStyle
forall ann. Doc ann
semi ([Doc AnsiStyle] -> Doc AnsiStyle)
-> [Doc AnsiStyle] -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$
                              [  t -> Doc AnsiStyle
forall {a}. PrettyAnsi (WithEnclosing a) => a -> Doc AnsiStyle
pwe t
x
                              ]



                 Differ t
x t
y -> AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. ann -> Doc ann -> Doc ann
annotate (Color -> AnsiStyle
color Color
Red) (Doc AnsiStyle -> Doc AnsiStyle)
-> ([Doc AnsiStyle] -> Doc AnsiStyle)
-> [Doc AnsiStyle]
-> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc AnsiStyle
-> Doc AnsiStyle
-> Doc AnsiStyle
-> [Doc AnsiStyle]
-> Doc AnsiStyle
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep (String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
"{ Differ ") Doc AnsiStyle
forall ann. Doc ann
rbrace (String -> Doc AnsiStyle
forall ann. String -> Doc ann
text String
"; ") ([Doc AnsiStyle] -> Doc AnsiStyle)
-> [Doc AnsiStyle] -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$

                              [ t -> Doc AnsiStyle
forall {a}. PrettyAnsi (WithEnclosing a) => a -> Doc AnsiStyle
pwe t
x
                              , t -> Doc AnsiStyle
forall {a}. PrettyAnsi (WithEnclosing a) => a -> Doc AnsiStyle
pwe t
y
                              ]

deriving instance PrettyAnsi (T DiffResult)

deriving instance PrettyAnsi (F DiffResult)

instance PrettyAnsi (WithEnclosing (T DiffResult)) where
    prettyAnsi :: WithEnclosing (T DiffResult) -> Doc AnsiStyle
prettyAnsi (WithEnclosing Enclosing
x (T DiffResult (Term0 (T DiffResult))
y)) = WithEnclosing (DiffResult (Term0 (T DiffResult))) -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (Enclosing
-> DiffResult (Term0 (T DiffResult))
-> WithEnclosing (DiffResult (Term0 (T DiffResult)))
forall a. Enclosing -> a -> WithEnclosing a
WithEnclosing Enclosing
x DiffResult (Term0 (T DiffResult))
y)

instance PrettyAnsi (WithEnclosing (F DiffResult)) where
    prettyAnsi :: WithEnclosing (F DiffResult) -> Doc AnsiStyle
prettyAnsi (WithEnclosing Enclosing
x (F DiffResult (Formula0 (T DiffResult) (F DiffResult))
y)) = WithEnclosing (DiffResult (Formula0 (T DiffResult) (F DiffResult)))
-> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (Enclosing
-> DiffResult (Formula0 (T DiffResult) (F DiffResult))
-> WithEnclosing
     (DiffResult (Formula0 (T DiffResult) (F DiffResult)))
forall a. Enclosing -> a -> WithEnclosing a
WithEnclosing Enclosing
x DiffResult (Formula0 (T DiffResult) (F DiffResult))
y)

instance PrettyAnsi (T0Diff) where
    prettyAnsi :: DiffResult (Term0 (T DiffResult)) -> Doc AnsiStyle
prettyAnsi = WithEnclosing (DiffResult (Term0 (T DiffResult))) -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (WithEnclosing (DiffResult (Term0 (T DiffResult)))
 -> Doc AnsiStyle)
-> (DiffResult (Term0 (T DiffResult))
    -> WithEnclosing (DiffResult (Term0 (T DiffResult))))
-> DiffResult (Term0 (T DiffResult))
-> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enclosing
-> DiffResult (Term0 (T DiffResult))
-> WithEnclosing (DiffResult (Term0 (T DiffResult)))
forall a. Enclosing -> a -> WithEnclosing a
WithEnclosing Enclosing
EnclNothing

instance PrettyAnsi (F0Diff) where
    prettyAnsi :: DiffResult (Formula0 (T DiffResult) (F DiffResult))
-> Doc AnsiStyle
prettyAnsi = WithEnclosing (DiffResult (Formula0 (T DiffResult) (F DiffResult)))
-> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (WithEnclosing
   (DiffResult (Formula0 (T DiffResult) (F DiffResult)))
 -> Doc AnsiStyle)
-> (DiffResult (Formula0 (T DiffResult) (F DiffResult))
    -> WithEnclosing
         (DiffResult (Formula0 (T DiffResult) (F DiffResult))))
-> DiffResult (Formula0 (T DiffResult) (F DiffResult))
-> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enclosing
-> DiffResult (Formula0 (T DiffResult) (F DiffResult))
-> WithEnclosing
     (DiffResult (Formula0 (T DiffResult) (F DiffResult)))
forall a. Enclosing -> a -> WithEnclosing a
WithEnclosing Enclosing
EnclNothing

-- instance PrettyAnsi (DiffResult (T DiffResult)) where
--     prettyAnsi = prettyAnsi . WithEnclosing EnclNothing . T

-- instance PrettyAnsi (DiffResult (T DiffResult) (F DiffResult)) where
--     prettyAnsi = prettyAnsi . WithEnclosing EnclNothing . F


-- runFormulaDiff :: Formula
--                   -> Formula
--                   -> DiffResult
--                        (Formula0 (T DiffResult) (F DiffResult))
-- runFormulaDiff a b = runF (diffFormula a b)

-- | Less random generator for generating formulae suitable for testing diff
diffGenF :: Gen Formula
diffGenF :: Gen Formula
diffGenF = (Int -> Gen Formula) -> Gen Formula
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen Formula
go
            where
              go :: Int -> Gen Formula
go Int
0 = Formula -> Gen Formula
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> Gen Formula) -> Formula -> Gen Formula
forall a b. (a -> b) -> a -> b
$ AtomicWord -> [Term] -> Formula
forall (c :: * -> *). Pointed c => AtomicWord -> [T c] -> F c
pApp AtomicWord
"Truth" []
              go Int
i = [Gen Formula] -> Gen Formula
forall a. HasCallStack => [Gen a] -> Gen a
oneof
                  [
                   do
                     Int
ileft <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0,Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
                     (Formula -> Formula -> Formula)
-> Gen Formula -> Gen Formula -> Gen Formula
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Formula -> Formula -> Formula
forall (c :: * -> *). Pointed c => F c -> F c -> F c
(.&.) (Int -> Gen Formula -> Gen Formula
forall a. HasCallStack => Int -> Gen a -> Gen a
resize Int
ileft Gen Formula
diffGenF) (Int -> Gen Formula -> Gen Formula
forall a. HasCallStack => Int -> Gen a -> Gen a
resize (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
ileft) Gen Formula
diffGenF)
                  , let a :: Gen Term
a=Gen Term
diffGenT in (Term -> Term -> Formula) -> Gen Term -> Gen (Term -> Formula)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term -> Formula
forall (c :: * -> *). Pointed c => T c -> T c -> F c
(.=.) Gen Term
a Gen (Term -> Formula) -> Gen Term -> Gen Formula
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
`ap` Gen Term
a
                  ]

diffGenT :: Gen Term
diffGenT :: Gen Term
diffGenT = (Int -> Gen Term) -> Gen Term
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen Term
go
            where
              go :: Int -> Gen Term
go Int
0 = [Term] -> Gen Term
forall a. HasCallStack => [a] -> Gen a
elements[V -> Term
forall (c :: * -> *). Pointed c => V -> T c
var V
"Z",AtomicWord -> [Term] -> Term
forall (c :: * -> *). Pointed c => AtomicWord -> [T c] -> T c
fApp AtomicWord
"1" []]

              go Int
i = [Gen Term] -> Gen Term
forall a. HasCallStack => [Gen a] -> Gen a
oneof
                  [
                    let a :: Gen Term
a=Int -> Gen Term -> Gen Term
forall a. HasCallStack => Int -> Gen a -> Gen a
resize (Int
iInt -> Int -> Int
forall a. Integral a => a -> a -> a
`div`Int
3) Gen Term
diffGenT in ([Term] -> Term) -> Gen [Term] -> Gen Term
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AtomicWord -> [Term] -> Term
forall (c :: * -> *). Pointed c => AtomicWord -> [T c] -> T c
fApp AtomicWord
"g") ([Gen Term] -> Gen [Term]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Gen Term
a,Gen Term
a,Gen Term
a])
                  , do
                     Int
ileft <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0,Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
                     ([Term] -> Term) -> Gen [Term] -> Gen Term
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AtomicWord -> [Term] -> Term
forall (c :: * -> *). Pointed c => AtomicWord -> [T c] -> T c
fApp AtomicWord
"f") ([Gen Term] -> Gen [Term]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Int -> Gen Term -> Gen Term
forall a. HasCallStack => Int -> Gen a -> Gen a
resize Int
ileft Gen Term
diffGenT,
                                                Int -> Gen Term -> Gen Term
forall a. HasCallStack => Int -> Gen a -> Gen a
resize (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
ileft) Gen Term
diffGenT])
                  ]


printSampleDiffs :: IO ()
printSampleDiffs :: IO ()
printSampleDiffs = do
  [Formula]
xs <- Gen Formula -> IO [Formula]
forall a. Gen a -> IO [a]
sample' Gen Formula
diffGenF
  [Formula]
ys <- Gen Formula -> IO [Formula]
forall a. Gen a -> IO [a]
sample' Gen Formula
diffGenF

  let item :: Formula -> Formula -> Doc AnsiStyle
item Formula
x Formula
y = [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
vsep
                 [ String -> Doc AnsiStyle
forall ann. String -> Doc ann
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
50 Char
'=')
                 , Formula -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi Formula
x
                 , String -> Doc AnsiStyle
forall ann. String -> Doc ann
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
40 Char
'-')
                 , Formula -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi Formula
y
                 , String -> Doc AnsiStyle
forall ann. String -> Doc ann
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
40 Char
'-')
                 , F DiffResult -> Doc AnsiStyle
forall a. PrettyAnsi a => a -> Doc AnsiStyle
prettyAnsi (Formula -> Formula -> F DiffResult
diffFormula Formula
x Formula
y)
                 ]

  ((Formula, Formula) -> IO ()) -> [(Formula, Formula)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn (String -> IO ())
-> ((Formula, Formula) -> String) -> (Formula, Formula) -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc AnsiStyle -> String
forall a. PrettyAnsi a => a -> String
prettySimple (Doc AnsiStyle -> String)
-> ((Formula, Formula) -> Doc AnsiStyle)
-> (Formula, Formula)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Formula -> Formula -> Doc AnsiStyle)
-> (Formula, Formula) -> Doc AnsiStyle
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Formula -> Formula -> Doc AnsiStyle
item) ([Formula] -> [Formula] -> [(Formula, Formula)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Formula]
xs [Formula]
ys)

-- prop0 :: Formula -> Formula -> Property
-- prop0 f1 f2 = f1 /= f2 ==>

--               let res=diffFormula (pApp "foo" [] .&. f1)
--                                   (pApp "foo" [] .&. f2)

--               in collect res $ True

--                  -- case res of
--                  --   SameHead ((F Same) :&:
--                  --            (F (Differ f1

instance Functor DiffResult where
    fmap :: forall a b. (a -> b) -> DiffResult a -> DiffResult b
fmap a -> b
f DiffResult a
d = case DiffResult a
d of
                 DiffResult a
Same -> DiffResult b
forall d. DiffResult d
Same
                 SameHead a
x -> b -> DiffResult b
forall d. d -> DiffResult d
SameHead (a -> b
f a
x)
                 Differ a
x a
y -> b -> b -> DiffResult b
forall d. d -> d -> DiffResult d
Differ (a -> b
f a
x) (a -> b
f a
y)
                 DiffResult a
DontCare -> DiffResult b
forall d. DiffResult d
DontCare




class Diffable a b | a -> b where
    diff :: a -> a -> b

instance Diffable Formula (F DiffResult) where diff :: Formula -> Formula -> F DiffResult
diff = Formula -> Formula -> F DiffResult
diffFormula
instance Diffable Term (T DiffResult) where diff :: Term -> Term -> T DiffResult
diff = Term -> Term -> T DiffResult
diffTerm