{-# 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 -> String
(Int -> Theorem -> ShowS)
-> (Theorem -> String) -> ([Theorem] -> ShowS) -> Show Theorem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Theorem] -> ShowS
$cshowList :: [Theorem] -> ShowS
show :: Theorem -> String
$cshow :: Theorem -> String
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 String
v Type
t Theorem
p1)
    | Bool
fa        = Int -> [String] -> Theorem -> Doc
prettyForall Int
p [String
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) (String -> Doc
text String
"=>")
        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
<+> String -> Doc
text String
"=" 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
$$ String -> Doc
text String
"&&"
        Doc -> Doc -> Doc
$$ Int -> Bool -> Theorem -> Doc
prettyTheorem Int
precAND Bool
fa Theorem
e2
    )

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

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

applySimplifierTheorem :: (Theorem -> Theorem) -> (Theorem -> Theorem)
applySimplifierTheorem :: (Theorem -> Theorem) -> Theorem -> Theorem
applySimplifierTheorem Theorem -> Theorem
s (ThForall String
v Type
t Theorem
p)
    = String -> Type -> Theorem -> Theorem
ThForall String
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 String
v Type
t Theorem
p)
    = case String -> Theorem -> Bool
varInTheorem String
v Theorem
p of
            Bool
True  -> String -> Type -> Theorem -> Theorem
ThForall String
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 String
_)) (EBuiltin Builtin
BId))
    = Builtin -> Expr
EBuiltin Builtin
BId
peepholeSimplifyExpr' Expr
e
    = Expr
e

foldEquality :: Theorem -> Theorem
foldEquality :: Theorem -> Theorem
foldEquality p :: Theorem
p@(ThForall String
_ Type
_ Theorem
_)
    = case Theorem -> [(String, 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 -> [(String, Type)] -> Maybe Theorem
foldEquality' (ThForall String
v Type
t Theorem
p) [(String, Type)]
vts
            = Theorem -> [(String, Type)] -> Maybe Theorem
foldEquality' Theorem
p ((String
v,Type
t)(String, Type) -> [(String, Type)] -> [(String, Type)]
forall a. a -> [a] -> [a]
:[(String, Type)]
vts)
        foldEquality' (ThImplies (ThEqual (EVar String
v) Expr
e2) Theorem
p) [(String, Type)]
vts
            | String
v String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((String, Type) -> String) -> [(String, Type)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Type) -> String
forall a b. (a, b) -> a
fst [(String, Type)]
vts
                = [(String, Type)] -> Theorem -> Maybe Theorem
foldEquality'' [(String, Type)]
vts (String -> Expr -> Theorem -> Theorem
theoremSubst String
v Expr
e2 Theorem
p)
        foldEquality' (ThImplies (ThEqual Expr
e1 (EVar String
v)) Theorem
p) [(String, Type)]
vts
            | String
v String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((String, Type) -> String) -> [(String, Type)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Type) -> String
forall a b. (a, b) -> a
fst [(String, Type)]
vts
                = [(String, Type)] -> Theorem -> Maybe Theorem
foldEquality'' [(String, Type)]
vts (String -> Expr -> Theorem -> Theorem
theoremSubst String
v Expr
e1 Theorem
p)
        foldEquality' Theorem
_ [(String, Type)]
vts
            = Maybe Theorem
forall a. Maybe a
Nothing

        foldEquality'' :: [(String, Type)] -> Theorem -> Maybe Theorem
foldEquality'' [] Theorem
e
            = Theorem -> Maybe Theorem
forall a. a -> Maybe a
Just Theorem
e
        foldEquality'' ((String
v,Type
t):[(String, Type)]
vts) Theorem
e
            = [(String, Type)] -> Theorem -> Maybe Theorem
foldEquality'' [(String, Type)]
vts (String -> Type -> Theorem -> Theorem
ThForall String
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 String
_ Type
_ Theorem
_)
    = case Theorem -> [(String, 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 -> [(String, Type)] -> Maybe Theorem
tryCurrying' (ThForall String
v Type
t Theorem
p) [(String, Type)]
vts
            = Theorem -> [(String, Type)] -> Maybe Theorem
tryCurrying' Theorem
p ((String
v,Type
t)(String, Type) -> [(String, Type)] -> [(String, Type)]
forall a. a -> [a] -> [a]
:[(String, Type)]
vts)
        tryCurrying' (ThEqual Expr
e1 Expr
e2) [(String, 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 String
v1), (ExprCtx
ctx2, EVar String
v2))
                    | String
v1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
v2 Bool -> Bool -> Bool
&& String
v1 String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((String, Type) -> String) -> [(String, Type)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Type) -> String
forall a b. (a, b) -> a
fst [(String, Type)]
vts
                        Bool -> Bool -> Bool
&& Bool -> Bool
not (String -> ExprCtx -> Bool
varInCtx String
v1 ExprCtx
ctx1) Bool -> Bool -> Bool
&& Bool -> Bool
not (String -> ExprCtx -> Bool
varInCtx String
v2 ExprCtx
ctx2)
                        -> [(String, Type)] -> Theorem -> Maybe Theorem
tryCurrying'' [(String, 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
_ [(String, 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 -> String -> Expr
EVarOp Fixity
FR Int
9 String
".") (ExprCtx -> Expr
untraverse ExprCtx
ctx)) Expr
e1
        tryCurrying'' :: [(String, Type)] -> Theorem -> Maybe Theorem
tryCurrying'' [] Theorem
e
            = Theorem -> Maybe Theorem
forall a. a -> Maybe a
Just Theorem
e
        tryCurrying'' ((String
v,Type
t):[(String, Type)]
vts) Theorem
e
            = [(String, Type)] -> Theorem -> Maybe Theorem
tryCurrying'' [(String, Type)]
vts (String -> Type -> Theorem -> Theorem
ThForall String
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 p. Eq p => (p -> p) -> p -> p
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 p. Eq p => (p -> p) -> p -> p
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 p. Eq p => (p -> p) -> p -> p
iterateUntilFixpoint Theorem -> Theorem
peephole
        )
    where
        iterateUntilFixpoint :: (p -> p) -> p -> p
iterateUntilFixpoint p -> p
s p
t
            = [p] -> p
forall p. Eq p => [p] -> p
findFixpoint ((p -> p) -> p -> [p]
forall a. (a -> a) -> a -> [a]
iterate p -> p
s p
t)

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

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

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

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