search

tsoding / Noq

Simple expression transformer that is not Coq.
MIT License
253 stars 24 forks source link

Display name of applied rules #6

Open Erk- opened 2 years ago

Erk- commented 2 years ago

When I was playing around with files and debugging my own code I thought it would be nice to have it show which rules were applied so I made a small patch for it.

Example

defined rule `div_sub_dist`
defined rule `div_sum_dist`
defined rule `pow`
apply square_of_sum => (A + B)^2
apply square        => (A + B)*(A + B)
apply mul_sum_dist  => (A + B)*A + (A + B)*B
apply mul_comm      => A*(A + B) + B*(A + B)
apply mul_sum_dist  => (A*A + A*B) + (B*A + B*B)
apply sum_assoc     => A*A + (A*B + (B*A + B*B))
apply sum_assoc     => A*A + ((A*B + B*A) + B*B)
apply mul_comm      => A*A + ((A*B + A*B) + B*B)
apply double_sum    => A*A + (2*(A*B) + B*B)
apply square        => A^2 + (2*(A*B) + B^2)
defined rule `square_of_sum`
defined rule `lim_def`
defined rule `lim_sum_dist`
apply examples/peano.noq:5:9 => 2 + 3
apply 3              => 2 + s(2)
apply 2              => s(1) + s(s(1))
apply 1              => s(s(0)) + s(s(s(0)))
apply sum            => s(s(0) + s(s(s(0))))
apply sum            => s(s(0 + s(s(s(0)))))
apply sum_id         => s(s(s(s(s(0)))))
apply examples/peano.noq:14:9 => 4 - 3
apply 4              => s(3) - 3
apply 3              => s(s(2)) - s(2)
apply 2              => s(s(s(1))) - s(s(1))
apply 1              => s(s(s(s(0)))) - s(s(s(0)))
apply sub            => s(s(s(0))) - s(s(0))
apply sub            => s(s(0)) - s(0)
apply sub            => s(0) - 0
apply sub_id         => s(0)

Know Issues

Using inline rules such as in der-square.noq will cause the alignment to be bad:

defined rule `der_def`
defined rule `square_def`
apply examples/der-square.noq:6:13 => der(square)
apply der_def        => lim(dx, 0, (square(x + dx) - square(x))/dx)
apply square_def     => lim(dx, 0, ((x + dx)^2 - x^2)/dx)
apply square_of_sum  => lim(dx, 0, ((x^2 + (2*(x*dx) + dx^2)) - x^2)/dx)
apply examples/der-square.noq:10:15 => lim(dx, 0, ((x^2 - x^2) + (2*(x*dx) + dx^2))/dx)
apply diff_id        => lim(dx, 0, (0 + (2*(x*dx) + dx^2))/dx)
apply sum_id         => lim(dx, 0, (2*(x*dx) + dx^2)/dx)
apply div_sum_dist   => lim(dx, 0, (2*(x*dx))/dx + dx^2/dx)
apply mul_assoc      => lim(dx, 0, ((2*x)*dx)/dx + dx^2/dx)
apply square         => lim(dx, 0, ((2*x)*dx)/dx + (dx*dx)/dx)
apply examples/der-square.noq:16:11 => lim(dx, 0, 2*x + dx)
apply lim_def        => apply_rule(0, dx, 0, 2*x + dx)
apply replace        => 2*x + 0
apply sum_comm       => 0 + 2*x
apply sum_id         => 2*x