{-# OPTIONS_GHC -fglasgow-exts #-}

module Language.Haskell.FreeTheorems.Theorems.Simplify
	( simplify
        , simplifyUnfoldedLift
 	)
where

import Data.Generics
import Data.Generics.Aliases
import Data.Generics.Schemes
import Data.Generics.Text (gshow)

import Language.Haskell.FreeTheorems.Theorems

simplify :: Formula -> Formula
simplify :: Formula -> Formula
simplify Formula
f = forall d. Data d => d -> d
gsimplify Formula
f

simplifyUnfoldedLift :: UnfoldedLift -> UnfoldedLift
simplifyUnfoldedLift :: UnfoldedLift -> UnfoldedLift
simplifyUnfoldedLift UnfoldedLift
l = forall d. Data d => d -> d
gsimplify UnfoldedLift
l


-- Generics stuff:

type ScopeInfo = [TermVariable]

gsimplify :: Data d => (d -> d)
gsimplify :: forall d. Data d => d -> d
gsimplify = (ScopeInfo -> forall d. Data d => d -> d)
-> ScopeInfo -> forall d. Data d => d -> d
everywhereScoped (\ScopeInfo
s -> forall a. a -> a
id
				    forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` Term -> Term
simplifyTerm
                                    forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` Predicate -> Predicate
simplifyPredicate
                                    forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` ScopeInfo -> Formula -> Formula
simplifyFormula ScopeInfo
s
			     ) []

everywhereScoped :: (ScopeInfo -> GenericT) -> ScopeInfo -> GenericT
everywhereScoped :: (ScopeInfo -> forall d. Data d => d -> d)
-> ScopeInfo -> forall d. Data d => d -> d
everywhereScoped = forall ctx.
(ctx -> GenericQ ctx)
-> (ctx -> forall d. Data d => d -> d)
-> ctx
-> forall d. Data d => d -> d
everywhereContext ScopeInfo -> GenericQ ScopeInfo
gupdateScope

-- Remember variables in scope

gupdateScope :: (ScopeInfo -> GenericQ ScopeInfo)
gupdateScope :: ScopeInfo -> GenericQ ScopeInfo
gupdateScope ScopeInfo
s = ScopeInfo
s forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
`mkQ` forall a b c. (a -> b -> c) -> b -> a -> c
flip Formula -> ScopeInfo -> ScopeInfo
updateScopeFormula ScopeInfo
s

-- This will remember all variables currently in scope
updateScopeFormula :: Formula -> ScopeInfo -> ScopeInfo
updateScopeFormula :: Formula -> ScopeInfo -> ScopeInfo
updateScopeFormula (ForallFunctions (Left  TermVariable
tv) (TypeExpression, TypeExpression)
_ [Restriction]
_ Formula
_) = (TermVariable
tv:)
updateScopeFormula (ForallFunctions (Right TermVariable
tv) (TypeExpression, TypeExpression)
_ [Restriction]
_ Formula
_) = (TermVariable
tv:)
updateScopeFormula (ForallVariables TermVariable
tv TypeExpression
_ Formula
_)           = (TermVariable
tv:)
updateScopeFormula Formula
_                                  = forall a. a -> a
id


-- Simplificatoins

simplifyFormula :: ScopeInfo -> Formula -> Formula

-- Remove unused quantified variables
simplifyFormula :: ScopeInfo -> Formula -> Formula
simplifyFormula	ScopeInfo
_ (ForallVariables TermVariable
tv TypeExpression
_ Formula
f) | Bool -> Bool
not (TermVariable
tv forall a a1. (Typeable a, Data a1, Eq a) => a -> a1 -> Bool
`occursIn` Formula
f) = Formula
f
 
-- ∀v.f v == g v ⇒ f == g
simplifyFormula	ScopeInfo
_ (ForallVariables TermVariable
tv TypeExpression
_ (Predicate (Term
t1 `IsEqual` Term
t2)))
                                           | Just (Term
f1,Term
v1) <- Term -> Maybe (Term, Term)
toFunApp Term
t1
                                           , Just (Term
f2,Term
v2) <- Term -> Maybe (Term, Term)
toFunApp Term
t2
                                           , Term
v1 forall a. Eq a => a -> a -> Bool
== Term
v2
				           , (TermVariable -> Term
TermVar TermVariable
tv) forall a. Eq a => a -> a -> Bool
== Term
v1
                                           = forall d. Data d => d -> d
gsimplify forall a b. (a -> b) -> a -> b
$ Predicate -> Formula
Predicate (Term
f1 Term -> Term -> Predicate
`IsEqual` Term
f2)
 
-- Find definitions, and apply as far as possible
simplifyFormula ScopeInfo
s (ForallVariables TermVariable
tv TypeExpression
t Formula
f) | [Term
def] <- TermVariable -> GenericQ [Term]
possibleDefs TermVariable
tv Formula
f
		  	                   = forall d. Data d => d -> d
gsimplify forall a b. (a -> b) -> a -> b
$ -- Will loop if the definition
                                                         -- would not remove itself
					        TermVariable -> TypeExpression -> Formula -> Formula
ForallVariables TermVariable
tv TypeExpression
t
                                                (ScopeInfo -> Term -> Term -> forall d. Data d => d -> d
replaceTerm ScopeInfo
s (TermVariable -> Term
TermVar TermVariable
tv) Term
def Formula
f)
-- Remove empty Implication
simplifyFormula ScopeInfo
_ (Implication (Predicate Predicate
IsTrue) Formula
f) 
                                           = Formula
f

-- Nothing to optimize
simplifyFormula ScopeInfo
_ Formula
f                        = Formula
f

simplifyPredicate :: Predicate -> Predicate

-- Remove tautologies
simplifyPredicate :: Predicate -> Predicate
simplifyPredicate (IsEqual Term
t1 Term
t2) | Term
t1 forall a. Eq a => a -> a -> Bool
== Term
t2
                                  = Predicate
IsTrue

{- This is wrong: The variable might be constrained:

-- Eta reduction on both sides of an equality
simplifyPredicate (IsEqual t1 t2) | Just (f1,v1) <- toFunApp t1
                                  , Just (f2,v2) <- toFunApp t2
                                  , v1 == v2
                                  = gsimplify (IsEqual f1 f2) -- run simplification again
-}

-- Nothing to optimize
simplifyPredicate Predicate
p               = Predicate
p


simplifyTerm :: Term -> Term

-- Simplify function concatenations
simplifyTerm :: Term -> Term
simplifyTerm (TermComp [Term
f]) = Term
f
simplifyTerm (TermComp (Term
f : (TermComp [Term]
fs) : [Term]
r))
                            = forall d. Data d => d -> d
gsimplify ([Term] -> Term
TermComp (Term
fforall a. a -> [a] -> [a]
:[Term]
fs forall a. [a] -> [a] -> [a]
++ [Term]
r))

-- Nothing to optimize
simplifyTerm Term
t                = Term
t
	

-- Actions

replaceTerm :: ScopeInfo -> Term -> Term -> GenericT
replaceTerm :: ScopeInfo -> Term -> Term -> forall d. Data d => d -> d
replaceTerm ScopeInfo
s0 Term
t Term
def = (ScopeInfo -> forall d. Data d => d -> d)
-> ScopeInfo -> forall d. Data d => d -> d
everywhereScoped (\ScopeInfo
s -> forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT (ScopeInfo -> Term -> Term
repl ScopeInfo
s)) ScopeInfo
s0
  where repl :: ScopeInfo -> Term -> Term
        repl :: ScopeInfo -> Term -> Term
repl ScopeInfo
s Term
term | Term
term forall a. Eq a => a -> a -> Bool
== Term
t
                    , forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ScopeInfo
s)) Term
def)
                    = Term
def
                    | Bool
otherwise
                    = Term
term

-- Inspections

toFunApp :: Term -> Maybe (Term, Term)
toFunApp :: Term -> Maybe (Term, Term)
toFunApp (TermApp Term
f Term
v) | Just (Term
fs,Term
v') <- Term -> Maybe (Term, Term)
toFunApp Term
v
                       = forall a. a -> Maybe a
Just ([Term] -> Term
TermComp [Term
f,Term
fs],Term
v')
toFunApp (TermApp Term
f Term
v) = forall a. a -> Maybe a
Just (Term
f,Term
v)
toFunApp Term
_             = forall a. Maybe a
Nothing

occursIn :: (Typeable a, Data a1, Eq a) => a -> a1 -> Bool
a
e occursIn :: forall a a1. (Typeable a, Data a1, Eq a) => a -> a1 -> Bool
`occursIn` a1
e' = forall b. Typeable b => (b -> Bool) -> GenericQ Bool
gAny (forall a. Eq a => a -> a -> Bool
==a
e) a1
e'

possibleDefs :: TermVariable -> GenericQ [Term]
possibleDefs :: TermVariable -> GenericQ [Term]
possibleDefs TermVariable
tv a
a = forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) (forall a. a -> a
id forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
`mkQ` Predicate -> [Term] -> [Term]
test) a
a []
  where test :: Predicate -> [Term] -> [Term]
test (Term
t1 `IsEqual` Term
t2) | Term
t1 forall a. Eq a => a -> a -> Bool
== (TermVariable -> Term
TermVar TermVariable
tv) = (Term
t2:)
                               | Term
t2 forall a. Eq a => a -> a -> Bool
== (TermVariable -> Term
TermVar TermVariable
tv) = (Term
t1:)
        test Predicate
_                 =  forall a. a -> a
id

-- Generic functions

gAny :: Typeable b => (b -> Bool) -> GenericQ Bool
gAny :: forall b. Typeable b => (b -> Bool) -> GenericQ Bool
gAny b -> Bool
p = forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything Bool -> Bool -> Bool
(||) (Bool
False forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
`mkQ` b -> Bool
p)

-- | Extend version of 'everywhere', which keeps information about the context around
everywhereContext :: (ctx -> GenericQ ctx) -> 
	             (ctx -> GenericT) ->
                      ctx ->
		      GenericT
everywhereContext :: forall ctx.
(ctx -> GenericQ ctx)
-> (ctx -> forall d. Data d => d -> d)
-> ctx
-> forall d. Data d => d -> d
everywhereContext ctx -> GenericQ ctx
ctxUpdate ctx -> forall d. Data d => d -> d
f ctx
ctx a
d
	= let ctx' :: ctx
ctx' = ctx -> GenericQ ctx
ctxUpdate ctx
ctx a
d
          in ctx -> forall d. Data d => d -> d
f ctx
ctx (forall a. Data a => (forall d. Data d => d -> d) -> a -> a
gmapT (forall ctx.
(ctx -> GenericQ ctx)
-> (ctx -> forall d. Data d => d -> d)
-> ctx
-> forall d. Data d => d -> d
everywhereContext ctx -> GenericQ ctx
ctxUpdate ctx -> forall d. Data d => d -> d
f ctx
ctx') a
d)