Monoid.idr

import Language.Reflection.Elab

namespace Tactics

  ||| Restrict a polymorphic type to () for contexts where it doesn't
  ||| matter. This is nice for sticking `debug` in a context where
  ||| Idris can't solve the type.
  simple : {m : Type -> Type} -> m () -> m ()
  simple x = x

  ||| Replace the current goal with one that's definitionally
  ||| equal. Return the name of the new goal, and ensure that it's
  ||| focused.
  |||
  ||| @ newGoal A type that is equivalent to the current goal
  equiv : (newGoal : Raw) -> Elab TTName
  equiv newGoal = do h <- gensym "goal"
                     claim h newGoal
                     fill (Var h); solve
                     focus h
                     return h

  ||| Remember a term built with elaboration for later use. If the
  ||| current goal is `h`, then `remember n ty` puts a fresh hole at
  ||| the front of the queue, with the old goal `h` second. The
  ||| contents of this hole end up let-bound in the scope of
  ||| `h`. Return the name of the new hole, in case it will be used
  ||| later.
  |||
  ||| @ n the name to be used to save the term
  ||| @ ty the type to inhabit
  remember : (n : TTName) -> (ty : Raw) -> Elab TTName
  remember n ty = do todo <- gensym "rememberThis"
                     claim todo ty
                     letbind n ty (Var todo)
                     focus todo
                     return todo

||| A representation of monoids with proofs
class IsMonoid a where
    neut : a
    op : a -> a -> a
    neutLeftId : (x : a) -> neut `op` x = x
    neutRightId : (x : a) -> x `op` neut = x
    assoc : (x, y, z : a) -> op x (op y z) = op (op x y) z

instance IsMonoid () where
    neut = ()
    op () () = ()
    neutLeftId () = Refl
    neutRightId () = Refl
    assoc () () () = Refl

instance IsMonoid Nat where
    neut = Z
    op = plus
    neutLeftId _ = Refl
    neutRightId = plusZeroRightNeutral
    assoc = plusAssociative

instance [multMonoid] IsMonoid Nat where
    neut = 1
    op = mult
    neutLeftId = multOneLeftNeutral
    neutRightId = multOneRightNeutral
    assoc = multAssociative

||| An abstract characterization of a monoidal expression as a syntax tree
data MonoidExpr a =
  NEUT | VAR a | OP (MonoidExpr a) (MonoidExpr a)

||| Recover a monoid value from a reflected tree
interpExpr : (IsMonoid a) => MonoidExpr a  -> a
interpExpr NEUT = neut
interpExpr (VAR x) = x
interpExpr (OP x y) = op (interpExpr x) (interpExpr y)

||| We can also interpret lists using the monoid operations
interpList : (IsMonoid a) => List a -> a
interpList [] = neut
interpList (x :: xs) = op x $ interpList xs

||| Normalize a monoid expression into a list
flattenExpr : MonoidExpr a -> List a
flattenExpr NEUT = []
flattenExpr (VAR x) = [x]
flattenExpr (OP x y) = flattenExpr x ++ flattenExpr y

||| List appending is justified using monoid associativity
opAppend : (IsMonoid a) => (xs, ys : List a) ->
           op (interpList xs) (interpList ys) = interpList (xs ++ ys)
opAppend [] ys = neutLeftId _
opAppend (x :: xs) ys =
  rewrite sym $ opAppend xs ys in
  sym $ assoc x (interpList xs) (interpList ys)

||| Flattening and interpretation commute
flattenOk : (IsMonoid a) => (e : MonoidExpr a) -> interpExpr e = interpList (flattenExpr e)
flattenOk NEUT = Refl
flattenOk (VAR x) = sym $ neutRightId x
flattenOk (OP x y) =
    rewrite flattenOk x in
    rewrite flattenOk y in
    opAppend (flattenExpr x) (flattenExpr y)


||| Flattening preserves interpretation according to the monoid laws
monoidReflection : (IsMonoid a) => (x, y : MonoidExpr a) ->
                   interpList (flattenExpr x) = interpList (flattenExpr y) ->
                   interpExpr x = interpExpr y
monoidReflection x y prf = rewrite flattenOk x in
                           rewrite flattenOk y in
                           prf

||| This tactic takes a reflected Idris expression and fills the
||| current hole with that expression's representation as a `MonoidExpr`
reifyExpr : Raw -> Elab ()
reifyExpr `(op {a=~a} @{~dict} ~x ~y) =
    do [(_, l), (_, r)] <- apply `(OP {a=~a})  [(False, 1), (False, 1)]
       solve
       focus l; reifyExpr x
       focus r; reifyExpr y
reifyExpr `(neut {a=~a} @{~dict}) = do fill `(NEUT {a=~a}); solve
reifyExpr tm = do [_, (_, h)] <- apply (Var `{VAR}) [(True, 0), (False, 1)]
                  solve
                  focus h; fill tm
                  solve
reifyExpr _ = empty -- for fast totality checking

||| Given a reflected IsMonoid type class instance dictionary, use it
||| to normalize a goal that is an equality of monoid expressions.
asMonoid : (dict : Raw) -> Elab ()
asMonoid dict =
    case !goalType of
      `((=) {A=~A} {B=~B} ~e1 ~e2) =>
         do l <- gensym "L"
            r <- gensym "R"

            remember l `(MonoidExpr ~A); reifyExpr e1
            remember r `(MonoidExpr ~B); reifyExpr e2

            equiv `((=) {A=~A} {B=~B}
                        (interpExpr {a=~A} @{~dict} ~(Var l))
                        (interpExpr {a=~B} @{~dict} ~(Var r)))

            [(_, h)] <-
              apply `(monoidReflection {a=~A} @{~dict} ~(Var l) ~(Var r)) [(True, 0)]

            solve
            focus h

||| Convert Nat addition expressions to monoid expressions, returning the
||| type class dictionary in order to get the right equalities.
natPlusAsMonoid : Elab Raw
natPlusAsMonoid =
    do cls <- gensym "cls"
       remember cls `(IsMonoid Nat); resolveTC `{natPlusAsMonoid}
       equiv (newTy (Var cls) !goalType)
       return (Var cls)

  where newTy : Raw -> Raw -> Raw
        newTy cls `(plus ~j ~k) = `(op {a=Nat} @{~cls} ~(newTy cls j) ~(newTy cls k))
        newTy cls `(Z) = `(neut {a=Nat} @{~cls})
        -- this next case is necessary to undo computation of plus's
        -- first arg and get it into a form that the monoid equality
        -- solver can figure out
        newTy cls `(S ~k) = `(op {a=Nat} @{~cls} 1 ~(newTy cls k))
        newTy cls (RApp f x) = RApp (newTy cls f) (newTy cls x)
        newTy cls (RBind n b tm) = RBind n (newTy cls <$> b) (newTy cls tm)
        newTy cls tm = tm


||| Convert Nat multiplication expressions to monoid expressions,
||| returning the type class dictionary used to get the right
||| equalities.
natMultAsMonoid : Elab Raw
natMultAsMonoid =
    do equiv (newTy !goalType)
       return `(multMonoid)

  where newTy : Raw -> Raw
        newTy `(mult ~j ~k) = `(op @{multMonoid} ~(newTy j) ~(newTy k))
        newTy `(S Z) = `(neut @{multMonoid})
        newTy (RApp f x) = RApp (newTy f) (newTy x)
        newTy (RBind n b tm) = RBind n (newTy <$> b) (newTy tm)
        newTy tm = tm

test1 : (IsMonoid a) =>
        (w,x,y,z : a) ->
        (( w `op` x) `op` (y `op` z)) = (w `op` (x `op` (y `op` (z `op` neut))))
test1 @{dict} w x y z = %runElab (asMonoid (Var `{dict}) *> search)


test2 : (x, y, z : Nat) ->
        plus (plus (plus z 13) z) (plus x (plus y Z)) = z `plus` (13 `plus` ((z `plus` x) `plus` y))
test2 x y z = %runElab (do dict <- natPlusAsMonoid
                           asMonoid dict
                           search)

test3 : (x,y,z : Nat) ->
        (x * ((y * 1) * x)) * 1 = x * y * x
test3 x y z = %runElab (do dict <- natMultAsMonoid
                           asMonoid dict
                           search)