diff --git a/pending-documentation.md b/pending-documentation.md index 88a7eea318b..5a76aac7b4d 100644 --- a/pending-documentation.md +++ b/pending-documentation.md @@ -156,3 +156,44 @@ rule bar(I) => I ``` This will rewrite `baz(0, foo)` to `foo`. First `baz(0, foo)` will be rewritten statically to `baz(0, foobar)`. Then the non-`macro` rule will apply (because the rule will have been rewritten to `rule baz(_, I) => I`). Then `foobar` will be rewritten statically after rewriting finishes to `foo` via the reverse form of the alias. + +## Other + +Backend features not yet given documentation: + +* Parser of KORE terms and definitions +* Term representation of K terms +* Hooked sorts and symbols +* Substituting a substitution into the RHS of a rule + * domain values + * functions + * variables + * symbols + * polymorphism + * hooks + * injection compaction + * overload compaction +* Pattern Matching / Unification of subject and LHS of rule + * domain values + * symbols + * side conditions + * and/or patterns + * list patterns + * nonlinear variables + * map/set patterns + * deterministic + * nondeterministic + * modulo injections + * modulo overloads +* Stepping + * initialization + * termination +* Print kore terms +* Equality/comparison of terms +* Owise rules +* Strategy #STUCK axiom +* User substitution + * binders + * kvar + +To get a complete list of hooks supported by K, you can run `grep -P -R "(?<=[^-])hook\([^)]*\)" k-distribution/include/builtin/ --include "*.k" -ho | sed 's/hook(//' | sed 's/)//' | sort | uniq | grep -v org.kframework`. All of these hooks will also eventually need documentation.