search

tsoding / Noq

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

Request for procedures #12

Open wiebecommajonas opened 2 years ago

wiebecommajonas commented 2 years ago

Description

A shaping applies rules 'at compile time' whereas a procedure would apply the rules 'at runtime'.

Example

Disclaimer: This example assumes the usage of the 'all' strategy as described in #11, because I could not come up with a different example.

eq_f :: eq(bool(true), bool(false)) = bool(false)
eq_t :: eq(bool(A), bool(A)) = bool(true)

basic_comm :: B(X, Y) = B(Y, X)

# eq_resolve :: eq(bool(A), bool(B)) {
#     eq_t | all
#     eq_f | all
#     basic_comm | all
#     eq_f | all
# }
# 
# result: eq(bool(A), bool(B))

proc eq_resolve :: eq(bool(A), bool(B)) {
    eq_t | all
    eq_f | all
    basic_comm | all
    eq_f | all
}

eq(bool(false), bool(true)) {
    eq_resolve | all
}

# expected result: bool(false)
rexim commented 12 months ago

I like the idea of reusable sequence of rule transformations. Not sure if I like it in a form you suggested, but I'll think about how I want to go about it. Thanks!