    {-# 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
    $c== :: Theorem -> Theorem -> Bool
    == :: Theorem -> Theorem -> Bool
    $c/= :: Theorem -> Theorem -> Bool
    /= :: 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
    $cshowsPrec :: Int -> Theorem -> ShowS
    showsPrec :: Int -> Theorem -> ShowS
    $cshow :: Theorem -> Var
    show :: Theorem -> Var
    $cshowList :: [Theorem] -> ShowS
    showList :: [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 a. (a -> a -> a) -> [a] -> a
    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 a. Eq a => a -> [a] -> 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 a. Eq a => a -> [a] -> 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 a. Eq a => a -> [a] -> 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 {t}. Eq t => (t -> t) -> t -> t
    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 {t}. Eq t => (t -> t) -> t -> t
    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 {t}. Eq t => (t -> t) -> t -> t
    iterateUntilFixpoint Theorem -> Theorem
    peephole
            )
        where
            iterateUntilFixpoint :: (t -> t) -> t -> t
    iterateUntilFixpoint t -> t
    s t
    t
                = [t] -> t
    forall {t}. Eq t => [t] -> t
    findFixpoint ((t -> t) -> t -> [t]
    forall a. (a -> a) -> a -> [a]
    iterate t -> t
    s t
    t)

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

            findFixpoint :: [t] -> t
    findFixpoint (t
    x1:xs :: [t]
    xs@(t
    x2:[t]
    _))
                | t
    x1 t -> t -> Bool
    forall a. Eq a => a -> a -> Bool
    == t
    x2  = t
    x2
                | Bool
    otherwise = [t] -> t
    findFixpoint [t]
    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