|
|
|---|
|
|
|
|---|
Apply sexpr-rewriting to a function applied to some args, which are assumed to already be simplified.
In sexpr-rewriting (see sexpr-rewrite), when rewriting a function application, the arguments are first recursively rewritten, and then sexpr-rewrite-fncall is applied to simplify the function applied to those args. This works by matching the args to the rewrite rules associated with that function symbol (using sexpr-rewrite-try-rules) and then recursively rewriting the resulting RHS and substitution using sexpr-rewrite-sigma. If no rewrite rules are found, ground evaluation is done using sexpr-rewrite-ground.