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