{-# 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)