{-# OPTIONS -w #-}

module Lambdabot.Plugin.Haskell.Free.Theorem where

import Lambdabot.Plugin.Haskell.Free.Type
import Lambdabot.Plugin.Haskell.Free.Expr
import Lambdabot.Plugin.Haskell.Free.Util

import Prelude hiding ((<>))

data Theorem
    = ThForall Var Type Theorem
    | ThImplies Theorem Theorem
    | ThEqual Expr Expr
    | ThAnd Theorem Theorem
        deriving (Theorem -> Theorem -> Bool
(Theorem -> Theorem -> Bool)
-> (Theorem -> Theorem -> Bool) -> Eq Theorem
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Theorem -> Theorem -> Bool
$c/= :: Theorem -> Theorem -> Bool
== :: Theorem -> Theorem -> Bool
$c== :: Theorem -> Theorem -> Bool
Eq,Int -> Theorem -> ShowS
[Theorem] -> ShowS
Theorem -> Var
(Int -> Theorem -> ShowS)
-> (Theorem -> Var) -> ([Theorem] -> ShowS) -> Show Theorem
forall a.
(Int -> a -> ShowS) -> (a -> Var) -> ([a] -> ShowS) -> Show a
showList :: [Theorem] -> ShowS
$cshowList :: [Theorem] -> ShowS
show :: Theorem -> Var
$cshow :: Theorem -> Var
showsPrec :: Int -> Theorem -> ShowS
$cshowsPrec :: Int -> Theorem -> ShowS
Show)

precIMPLIES, precAND :: Int
precIMPLIES :: Int
precIMPLIES = Int
5
precAND :: Int
precAND = Int
3

instance Pretty Theorem where
    prettyP :: Int -> Theorem -> Doc
prettyP Int
p Theorem
t = Int -> Bool -> Theorem -> Doc
prettyTheorem Int
p Bool
False Theorem
t


prettyTheorem :: Int -> Bool -> Theorem -> Doc
prettyTheorem :: Int -> Bool -> Theorem -> Doc
prettyTheorem Int
p Bool
fa th :: Theorem
th@(ThForall Var
v Type
t Theorem
p1)
    | Bool
fa        = Int -> [Var] -> Theorem -> Doc
prettyForall Int
p [Var
v] Theorem
p1
    | Bool
otherwise = Int -> Theorem -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyP Int
p Theorem
p1
prettyTheorem Int
p Bool
fa (ThImplies Theorem
p1 Theorem
p2)
    = Bool -> Doc -> Doc
prettyParenIndent (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
precIMPLIES) (
        Int -> Bool -> Theorem -> Doc
prettyTheorem (Int
precIMPLIESInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Bool
True Theorem
p1
        Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest (-Int
1) (Var -> Doc
text Var
"=>")
        Doc -> Doc -> Doc
$$ Int -> Bool -> Theorem -> Doc
prettyTheorem Int
precIMPLIES Bool
fa Theorem
p2
    )
prettyTheorem Int
_ Bool
_ (ThEqual Expr
e1 Expr
e2)
    = Int -> Expr -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyP Int
0 Expr
e1 Doc -> Doc -> Doc
<+> Var -> Doc
text Var
"=" Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyP Int
0 Expr
e2
prettyTheorem Int
p Bool
fa (ThAnd Theorem
e1 Theorem
e2)
    = Bool -> Doc -> Doc
prettyParenIndent (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
precAND) (
        Int -> Bool -> Theorem -> Doc
prettyTheorem (Int
precANDInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Bool
fa Theorem
e1 Doc -> Doc -> Doc
$$ Var -> Doc
text Var
"&&"
        Doc -> Doc -> Doc
$$ Int -> Bool -> Theorem -> Doc
prettyTheorem Int
precAND Bool
fa Theorem
e2
    )

prettyForall :: Int -> [Var] -> Theorem -> Doc
prettyForall :: Int -> [Var] -> Theorem -> Doc
prettyForall Int
p [Var]
vs (ThForall Var
v Type
t Theorem
p1)
    = Int -> [Var] -> Theorem -> Doc
prettyForall Int
p (Var
vVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
vs) Theorem
p1
prettyForall Int
p [Var]
vs Theorem
th
    = Doc -> Doc
parens (
        Var -> Doc
text Var
"forall" Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep [ Var -> Doc
text Var
v | Var
v <- [Var] -> [Var]
forall a. [a] -> [a]
reverse [Var]
vs ] Doc -> Doc -> Doc
<> Var -> Doc
text Var
"."
        Doc -> Doc -> Doc
<+> Int -> Bool -> Theorem -> Doc
prettyTheorem Int
0 Bool
True Theorem
th
    )

varInTheorem :: Var -> Theorem -> Bool
varInTheorem :: Var -> Theorem -> Bool
varInTheorem Var
v (ThForall Var
v' Type
t Theorem
p)
    = Var
v Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
/= Var
v' Bool -> Bool -> Bool
&& Var -> Theorem -> Bool
varInTheorem Var
v Theorem
p
varInTheorem Var
v (ThImplies Theorem
p1 Theorem
p2)
    = Var -> Theorem -> Bool
varInTheorem Var
v Theorem
p1 Bool -> Bool -> Bool
|| Var -> Theorem -> Bool
varInTheorem Var
v Theorem
p2
varInTheorem Var
v (ThEqual Expr
e1 Expr
e2)
    = Var -> Expr -> Bool
varInExpr Var
v Expr
e1 Bool -> Bool -> Bool
|| Var -> Expr -> Bool
varInExpr Var
v Expr
e2
varInTheorem Var
v (ThAnd Theorem
e1 Theorem
e2)
    = Var -> Theorem -> Bool
varInTheorem Var
v Theorem
e1 Bool -> Bool -> Bool
|| Var -> Theorem -> Bool
varInTheorem Var
v Theorem
e2

applySimplifierTheorem :: (Theorem -> Theorem) -> (Theorem -> Theorem)
applySimplifierTheorem :: (Theorem -> Theorem) -> Theorem -> Theorem
applySimplifierTheorem Theorem -> Theorem
s (ThForall Var
v Type
t Theorem
p)
    = Var -> Type -> Theorem -> Theorem
ThForall Var
v Type
t (Theorem -> Theorem
s Theorem
p)
applySimplifierTheorem Theorem -> Theorem
s (ThImplies Theorem
p1 Theorem
p2)
    = Theorem -> Theorem -> Theorem
ThImplies (Theorem -> Theorem
s Theorem
p1) (Theorem -> Theorem
s Theorem
p2)
applySimplifierTheorem Theorem -> Theorem
s p :: Theorem
p@(ThEqual Expr
_ Expr
_)
    = Theorem
p
applySimplifierTheorem Theorem -> Theorem
s p :: Theorem
p@(ThAnd Theorem
p1 Theorem
p2)
    = Theorem -> Theorem -> Theorem
ThAnd (Theorem -> Theorem
s Theorem
p1) (Theorem -> Theorem
s Theorem
p2)

peepholeSimplifyTheorem :: Theorem -> Theorem
peepholeSimplifyTheorem :: Theorem -> Theorem
peepholeSimplifyTheorem
    = Theorem -> Theorem
peepholeSimplifyTheorem' (Theorem -> Theorem) -> (Theorem -> Theorem) -> Theorem -> Theorem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Theorem -> Theorem) -> Theorem -> Theorem
applySimplifierTheorem Theorem -> Theorem
peepholeSimplifyTheorem

peepholeSimplifyTheorem' :: Theorem -> Theorem
peepholeSimplifyTheorem' :: Theorem -> Theorem
peepholeSimplifyTheorem' (ThForall Var
v Type
t Theorem
p)
    = case Var -> Theorem -> Bool
varInTheorem Var
v Theorem
p of
            Bool
True  -> Var -> Type -> Theorem -> Theorem
ThForall Var
v Type
t Theorem
p
            Bool
False -> Theorem
p
peepholeSimplifyTheorem' p :: Theorem
p@(ThAnd Theorem
e1 Theorem
e2)
    = (Theorem -> Theorem -> Theorem) -> [Theorem] -> Theorem
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Theorem -> Theorem -> Theorem
ThAnd (Theorem -> [Theorem] -> [Theorem]
flattenAnd Theorem
e1 ([Theorem] -> [Theorem])
-> ([Theorem] -> [Theorem]) -> [Theorem] -> [Theorem]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Theorem -> [Theorem] -> [Theorem]
flattenAnd Theorem
e2 ([Theorem] -> [Theorem]) -> [Theorem] -> [Theorem]
forall a b. (a -> b) -> a -> b
$ [])
    where
        flattenAnd :: Theorem -> [Theorem] -> [Theorem]
flattenAnd (ThAnd Theorem
e1 Theorem
e2) = Theorem -> [Theorem] -> [Theorem]
flattenAnd Theorem
e1 ([Theorem] -> [Theorem])
-> ([Theorem] -> [Theorem]) -> [Theorem] -> [Theorem]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Theorem -> [Theorem] -> [Theorem]
flattenAnd Theorem
e2
        flattenAnd Theorem
e = (Theorem
eTheorem -> [Theorem] -> [Theorem]
forall a. a -> [a] -> [a]
:)
peepholeSimplifyTheorem' Theorem
p
    = Theorem
p

peepholeSimplifyExpr :: Expr -> Expr
peepholeSimplifyExpr :: Expr -> Expr
peepholeSimplifyExpr
    = Expr -> Expr
peepholeSimplifyExpr' (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> Expr -> Expr
applySimplifierExpr Expr -> Expr
peepholeSimplifyExpr

peepholeSimplifyExpr' :: Expr -> Expr
peepholeSimplifyExpr' :: Expr -> Expr
peepholeSimplifyExpr' (EApp (EBuiltin Builtin
BId) Expr
e2)
    = Expr
e2
peepholeSimplifyExpr' (EApp (EBuiltin (BMap Var
_)) (EBuiltin Builtin
BId))
    = Builtin -> Expr
EBuiltin Builtin
BId
peepholeSimplifyExpr' Expr
e
    = Expr
e

foldEquality :: Theorem -> Theorem
foldEquality :: Theorem -> Theorem
foldEquality p :: Theorem
p@(ThForall Var
_ Type
_ Theorem
_)
    = case Theorem -> [(Var, Type)] -> Maybe Theorem
foldEquality' Theorem
p [] of
        Just Theorem
p' -> Theorem
p'
        Maybe Theorem
Nothing -> (Theorem -> Theorem) -> Theorem -> Theorem
applySimplifierTheorem Theorem -> Theorem
foldEquality Theorem
p
    where
        foldEquality' :: Theorem -> [(Var, Type)] -> Maybe Theorem
foldEquality' (ThForall Var
v Type
t Theorem
p) [(Var, Type)]
vts
            = Theorem -> [(Var, Type)] -> Maybe Theorem
foldEquality' Theorem
p ((Var
v,Type
t)(Var, Type) -> [(Var, Type)] -> [(Var, Type)]
forall a. a -> [a] -> [a]
:[(Var, Type)]
vts)
        foldEquality' (ThImplies (ThEqual (EVar Var
v) Expr
e2) Theorem
p) [(Var, Type)]
vts
            | Var
v Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Var, Type) -> Var) -> [(Var, Type)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Type) -> Var
forall a b. (a, b) -> a
fst [(Var, Type)]
vts
                = [(Var, Type)] -> Theorem -> Maybe Theorem
foldEquality'' [(Var, Type)]
vts (Var -> Expr -> Theorem -> Theorem
theoremSubst Var
v Expr
e2 Theorem
p)
        foldEquality' (ThImplies (ThEqual Expr
e1 (EVar Var
v)) Theorem
p) [(Var, Type)]
vts
            | Var
v Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Var, Type) -> Var) -> [(Var, Type)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Type) -> Var
forall a b. (a, b) -> a
fst [(Var, Type)]
vts
                = [(Var, Type)] -> Theorem -> Maybe Theorem
foldEquality'' [(Var, Type)]
vts (Var -> Expr -> Theorem -> Theorem
theoremSubst Var
v Expr
e1 Theorem
p)
        foldEquality' Theorem
_ [(Var, Type)]
vts
            = Maybe Theorem
forall a. Maybe a
Nothing

        foldEquality'' :: [(Var, Type)] -> Theorem -> Maybe Theorem
foldEquality'' [] Theorem
e
            = Theorem -> Maybe Theorem
forall a. a -> Maybe a
Just Theorem
e
        foldEquality'' ((Var
v,Type
t):[(Var, Type)]
vts) Theorem
e
            = [(Var, Type)] -> Theorem -> Maybe Theorem
foldEquality'' [(Var, Type)]
vts (Var -> Type -> Theorem -> Theorem
ThForall Var
v Type
t Theorem
e)

foldEquality Theorem
p
    = (Theorem -> Theorem) -> Theorem -> Theorem
applySimplifierTheorem Theorem -> Theorem
foldEquality Theorem
p

tryCurrying :: Theorem -> Theorem
tryCurrying :: Theorem -> Theorem
tryCurrying p :: Theorem
p@(ThForall Var
_ Type
_ Theorem
_)
    = case Theorem -> [(Var, Type)] -> Maybe Theorem
tryCurrying' Theorem
p [] of
        Just Theorem
p' -> Theorem
p'
        Maybe Theorem
Nothing -> (Theorem -> Theorem) -> Theorem -> Theorem
applySimplifierTheorem Theorem -> Theorem
tryCurrying Theorem
p
    where
        tryCurrying' :: Theorem -> [(Var, Type)] -> Maybe Theorem
tryCurrying' (ThForall Var
v Type
t Theorem
p) [(Var, Type)]
vts
            = Theorem -> [(Var, Type)] -> Maybe Theorem
tryCurrying' Theorem
p ((Var
v,Type
t)(Var, Type) -> [(Var, Type)] -> [(Var, Type)]
forall a. a -> [a] -> [a]
:[(Var, Type)]
vts)
        tryCurrying' (ThEqual Expr
e1 Expr
e2) [(Var, Type)]
vts
            = case (ExprCtx -> Expr -> (ExprCtx, Expr)
traverseRight ExprCtx
ECDot Expr
e1, ExprCtx -> Expr -> (ExprCtx, Expr)
traverseRight ExprCtx
ECDot Expr
e2) of
                ((ExprCtx
ctx1, EVar Var
v1), (ExprCtx
ctx2, EVar Var
v2))
                    | Var
v1 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v2 Bool -> Bool -> Bool
&& Var
v1 Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Var, Type) -> Var) -> [(Var, Type)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Type) -> Var
forall a b. (a, b) -> a
fst [(Var, Type)]
vts
                        Bool -> Bool -> Bool
&& Bool -> Bool
not (Var -> ExprCtx -> Bool
varInCtx Var
v1 ExprCtx
ctx1) Bool -> Bool -> Bool
&& Bool -> Bool
not (Var -> ExprCtx -> Bool
varInCtx Var
v2 ExprCtx
ctx2)
                        -> [(Var, Type)] -> Theorem -> Maybe Theorem
tryCurrying'' [(Var, Type)]
vts (Expr -> Expr -> Theorem
ThEqual (ExprCtx -> Expr
untraverse ExprCtx
ctx1)
                                                      (ExprCtx -> Expr
untraverse ExprCtx
ctx2))
                ((ExprCtx, Expr), (ExprCtx, Expr))
_       -> Maybe Theorem
forall a. Maybe a
Nothing
        tryCurrying' Theorem
_ [(Var, Type)]
_
            = Maybe Theorem
forall a. Maybe a
Nothing

        traverseRight :: ExprCtx -> Expr -> (ExprCtx, Expr)
traverseRight ExprCtx
ctx (EApp Expr
e1 Expr
e2)
            = ExprCtx -> Expr -> (ExprCtx, Expr)
traverseRight (Expr -> ExprCtx -> ExprCtx
ECAppR Expr
e1 ExprCtx
ctx) Expr
e2
        traverseRight ExprCtx
ctx Expr
e
            = (ExprCtx
ctx, Expr
e)

        untraverse :: ExprCtx -> Expr
untraverse ExprCtx
ECDot = Builtin -> Expr
EBuiltin Builtin
BId
        untraverse (ECAppR Expr
e1 ExprCtx
ECDot)
            = Expr
e1
        untraverse (ECAppR Expr
e1 ExprCtx
ctx)
            = Expr -> Expr -> Expr
EApp (Expr -> Expr -> Expr
EApp (Fixity -> Int -> Var -> Expr
EVarOp Fixity
FR Int
9 Var
".") (ExprCtx -> Expr
untraverse ExprCtx
ctx)) Expr
e1
        tryCurrying'' :: [(Var, Type)] -> Theorem -> Maybe Theorem
tryCurrying'' [] Theorem
e
            = Theorem -> Maybe Theorem
forall a. a -> Maybe a
Just Theorem
e
        tryCurrying'' ((Var
v,Type
t):[(Var, Type)]
vts) Theorem
e
            = [(Var, Type)] -> Theorem -> Maybe Theorem
tryCurrying'' [(Var, Type)]
vts (Var -> Type -> Theorem -> Theorem
ThForall Var
v Type
t Theorem
e)

tryCurrying Theorem
p
    = (Theorem -> Theorem) -> Theorem -> Theorem
applySimplifierTheorem Theorem -> Theorem
tryCurrying Theorem
p

theoremSimplify :: Theorem -> Theorem
theoremSimplify :: Theorem -> Theorem
theoremSimplify
    = (Theorem -> Theorem) -> Theorem -> Theorem
forall {a}. Eq a => (a -> a) -> a -> a
iterateUntilFixpoint
        (Theorem -> Theorem
foldEquality
        (Theorem -> Theorem) -> (Theorem -> Theorem) -> Theorem -> Theorem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Theorem -> Theorem) -> Theorem -> Theorem
forall {a}. Eq a => (a -> a) -> a -> a
iterateUntilFixpoint Theorem -> Theorem
peephole
        (Theorem -> Theorem) -> (Theorem -> Theorem) -> Theorem -> Theorem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Theorem -> Theorem
tryCurrying
        (Theorem -> Theorem) -> (Theorem -> Theorem) -> Theorem -> Theorem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Theorem -> Theorem) -> Theorem -> Theorem
forall {a}. Eq a => (a -> a) -> a -> a
iterateUntilFixpoint Theorem -> Theorem
peephole
        )
    where
        iterateUntilFixpoint :: (a -> a) -> a -> a
iterateUntilFixpoint a -> a
s a
t
            = [a] -> a
forall {a}. Eq a => [a] -> a
findFixpoint ((a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate a -> a
s a
t)

        peephole :: Theorem -> Theorem
peephole Theorem
t = [Theorem] -> Theorem
forall {a}. Eq a => [a] -> a
findFixpoint ((Theorem -> Theorem) -> Theorem -> [Theorem]
forall a. (a -> a) -> a -> [a]
iterate Theorem -> Theorem
peepholeSimplifyTheorem Theorem
t)

        findFixpoint :: [a] -> a
findFixpoint (a
x1:xs :: [a]
xs@(a
x2:[a]
_))
            | a
x1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x2  = a
x2
            | Bool
otherwise = [a] -> a
findFixpoint [a]
xs

theoremSubst :: Var -> Expr -> Theorem -> Theorem
theoremSubst :: Var -> Expr -> Theorem -> Theorem
theoremSubst Var
v Expr
e (ThForall Var
f Type
t Theorem
p)
    = Var -> Type -> Theorem -> Theorem
ThForall Var
f Type
t (Var -> Expr -> Theorem -> Theorem
theoremSubst Var
v Expr
e Theorem
p)
theoremSubst Var
v Expr
e (ThImplies Theorem
p1 Theorem
p2)
    = Theorem -> Theorem -> Theorem
ThImplies (Var -> Expr -> Theorem -> Theorem
theoremSubst Var
v Expr
e Theorem
p1) (Var -> Expr -> Theorem -> Theorem
theoremSubst Var
v Expr
e Theorem
p2)
theoremSubst Var
v Expr
e (ThEqual Expr
e1 Expr
e2)
    = Expr -> Expr -> Theorem
ThEqual (Var -> Expr -> Expr -> Expr
exprSubst Var
v Expr
e Expr
e1) (Var -> Expr -> Expr -> Expr
exprSubst Var
v Expr
e Expr
e2)
theoremSubst Var
v Expr
e (ThAnd Theorem
p1 Theorem
p2)
    = Theorem -> Theorem -> Theorem
ThAnd (Var -> Expr -> Theorem -> Theorem
theoremSubst Var
v Expr
e Theorem
p1) (Var -> Expr -> Theorem -> Theorem
theoremSubst Var
v Expr
e Theorem
p2)

-- vim: ts=4:sts=4:expandtab:ai