{-# 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 = 5
precAND :: Int
precAND = 3

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


prettyTheorem :: Int -> Bool -> Theorem -> Doc
prettyTheorem :: Int -> Bool -> Theorem -> Doc
prettyTheorem p :: Int
p fa :: Bool
fa th :: Theorem
th@(ThForall v :: String
v t :: Type
t p1 :: 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 p :: Int
p fa :: Bool
fa (ThImplies p1 :: Theorem
p1 p2 :: 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
+1) Bool
True Theorem
p1
        Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest (-1) (String -> Doc
text "=>")
        Doc -> Doc -> Doc
$$ Int -> Bool -> Theorem -> Doc
prettyTheorem Int
precIMPLIES Bool
fa Theorem
p2
    )
prettyTheorem _ _ (ThEqual e1 :: Expr
e1 e2 :: Expr
e2)
    = Int -> Expr -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyP 0 Expr
e1 Doc -> Doc -> Doc
<+> String -> Doc
text "=" Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyP 0 Expr
e2
prettyTheorem p :: Int
p fa :: Bool
fa (ThAnd e1 :: Theorem
e1 e2 :: 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
+1) Bool
fa Theorem
e1 Doc -> Doc -> Doc
$$ String -> Doc
text "&&"
        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 p :: Int
p vs :: [String]
vs (ThForall v :: String
v t :: Type
t p1 :: Theorem
p1)
    = Int -> [String] -> Theorem -> Doc
prettyForall Int
p (String
vString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
vs) Theorem
p1
prettyForall p :: Int
p vs :: [String]
vs th :: Theorem
th
    = Doc -> Doc
parens (
        String -> Doc
text "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 "."
        Doc -> Doc -> Doc
<+> Int -> Bool -> Theorem -> Doc
prettyTheorem 0 Bool
True Theorem
th
    )

varInTheorem :: Var -> Theorem -> Bool
varInTheorem :: String -> Theorem -> Bool
varInTheorem v :: String
v (ThForall v' :: String
v' t :: Type
t p :: 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 v :: String
v (ThImplies p1 :: Theorem
p1 p2 :: Theorem
p2)
    = String -> Theorem -> Bool
varInTheorem String
v Theorem
p1 Bool -> Bool -> Bool
|| String -> Theorem -> Bool
varInTheorem String
v Theorem
p2
varInTheorem v :: String
v (ThEqual e1 :: Expr
e1 e2 :: Expr
e2)
    = String -> Expr -> Bool
varInExpr String
v Expr
e1 Bool -> Bool -> Bool
|| String -> Expr -> Bool
varInExpr String
v Expr
e2
varInTheorem v :: String
v (ThAnd e1 :: Theorem
e1 e2 :: 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 s :: Theorem -> Theorem
s (ThForall v :: String
v t :: Type
t p :: Theorem
p)
    = String -> Type -> Theorem -> Theorem
ThForall String
v Type
t (Theorem -> Theorem
s Theorem
p)
applySimplifierTheorem s :: Theorem -> Theorem
s (ThImplies p1 :: Theorem
p1 p2 :: Theorem
p2)
    = Theorem -> Theorem -> Theorem
ThImplies (Theorem -> Theorem
s Theorem
p1) (Theorem -> Theorem
s Theorem
p2)
applySimplifierTheorem s :: Theorem -> Theorem
s p :: Theorem
p@(ThEqual _ _)
    = Theorem
p
applySimplifierTheorem s :: Theorem -> Theorem
s p :: Theorem
p@(ThAnd p1 :: Theorem
p1 p2 :: 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 v :: String
v t :: Type
t p :: Theorem
p)
    = case String -> Theorem -> Bool
varInTheorem String
v Theorem
p of
            True  -> String -> Type -> Theorem -> Theorem
ThForall String
v Type
t Theorem
p
            False -> Theorem
p
peepholeSimplifyTheorem' p :: Theorem
p@(ThAnd e1 :: Theorem
e1 e2 :: 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 e1 :: Theorem
e1 e2 :: 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 e :: Theorem
e = (Theorem
eTheorem -> [Theorem] -> [Theorem]
forall a. a -> [a] -> [a]
:)
peepholeSimplifyTheorem' p :: 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 BId) e2 :: Expr
e2)
    = Expr
e2
peepholeSimplifyExpr' (EApp (EBuiltin (BMap _)) (EBuiltin BId))
    = Builtin -> Expr
EBuiltin Builtin
BId
peepholeSimplifyExpr' e :: Expr
e
    = Expr
e

foldEquality :: Theorem -> Theorem
foldEquality :: Theorem -> Theorem
foldEquality p :: Theorem
p@(ThForall _ _ _)
    = case Theorem -> [(String, Type)] -> Maybe Theorem
foldEquality' Theorem
p [] of
        Just p' :: Theorem
p' -> Theorem
p'
        Nothing -> (Theorem -> Theorem) -> Theorem -> Theorem
applySimplifierTheorem Theorem -> Theorem
foldEquality Theorem
p
    where
        foldEquality' :: Theorem -> [(String, Type)] -> Maybe Theorem
foldEquality' (ThForall v :: String
v t :: Type
t p :: Theorem
p) vts :: [(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 v :: String
v) e2 :: Expr
e2) p :: Theorem
p) vts :: [(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 e1 :: Expr
e1 (EVar v :: String
v)) p :: Theorem
p) vts :: [(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' _ vts :: [(String, Type)]
vts
            = Maybe Theorem
forall a. Maybe a
Nothing

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

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

tryCurrying :: Theorem -> Theorem
tryCurrying :: Theorem -> Theorem
tryCurrying p :: Theorem
p@(ThForall _ _ _)
    = case Theorem -> [(String, Type)] -> Maybe Theorem
tryCurrying' Theorem
p [] of
        Just p' :: Theorem
p' -> Theorem
p'
        Nothing -> (Theorem -> Theorem) -> Theorem -> Theorem
applySimplifierTheorem Theorem -> Theorem
tryCurrying Theorem
p
    where
        tryCurrying' :: Theorem -> [(String, Type)] -> Maybe Theorem
tryCurrying' (ThForall v :: String
v t :: Type
t p :: Theorem
p) vts :: [(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 e1 :: Expr
e1 e2 :: Expr
e2) vts :: [(String, Type)]
vts
            = case (ExprCtx -> Expr -> (ExprCtx, Expr)
traverseRight ExprCtx
ECDot Expr
e1, ExprCtx -> Expr -> (ExprCtx, Expr)
traverseRight ExprCtx
ECDot Expr
e2) of
                ((ctx1 :: ExprCtx
ctx1, EVar v1 :: String
v1), (ctx2 :: ExprCtx
ctx2, EVar v2 :: 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))
                _       -> Maybe Theorem
forall a. Maybe a
Nothing
        tryCurrying' _ _
            = Maybe Theorem
forall a. Maybe a
Nothing

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

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

tryCurrying p :: 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 s :: p -> p
s t :: 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 t :: 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 (x1 :: p
x1:xs :: [p]
xs@(x2 :: p
x2:_))
            | 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 v :: String
v e :: Expr
e (ThForall f :: String
f t :: Type
t p :: Theorem
p)
    = String -> Type -> Theorem -> Theorem
ThForall String
f Type
t (String -> Expr -> Theorem -> Theorem
theoremSubst String
v Expr
e Theorem
p)
theoremSubst v :: String
v e :: Expr
e (ThImplies p1 :: Theorem
p1 p2 :: 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 v :: String
v e :: Expr
e (ThEqual e1 :: Expr
e1 e2 :: 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 v :: String
v e :: Expr
e (ThAnd p1 :: Theorem
p1 p2 :: 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