tsoding / Noq

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

Semantics of `all` strategy #11

Open wiebecommajonas opened 2 years ago

wiebecommajonas commented 2 years ago

Description

The all strategy should really not throw an error when not match is found.

Reasoning

'All' matches are semantically just a list of matches. So if no match is found, 'all matches' is just an empty list. Applying every match in an empty list is thus properly defined and needs no different treatment.

This also allows 'conditional' (stretching the meaning of the word) application.

Example

and_f :: and(bool(false), bool(_)) = bool(false)
and_t :: and(bool(true), bool(true)) = bool(true)

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

and(bool(true), bool(false)) {
    and_t | all
    and_f | all
    basic_comm | all
    and_f | all
}

Known issues

This could lead to issues where rule applications following an 'all' application expect the order of matches to be a specific way.