Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.