diff options
| author | Alasdair Armstrong | 2019-01-22 18:04:16 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-01-22 18:11:12 +0000 |
| commit | 8258b81bf1485e3133fb4351413ed1f554717f43 (patch) | |
| tree | 29f95bca5a4b8f18f220b518bd3deb252d9030a9 /editors | |
| parent | 22bdcf2e58e0bc1e5f58b9fd3f462a3b380fad4a (diff) | |
Add a pragma for unrolling recursive functions
For example in RISC-V for the translation table walk:
$optimize unroll 2
val walk32 ...
function walk32 ...
would create two extra copies of the walk_32 function,
walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2
being recursive. Currently we only support the case where we have
$optimize unroll, directly followed by a valspec, then a function, but
this should be generalised in future.
This optimization nearly doubles the performance of RISC-V
It is implemented using a new Optimize.recheck rewrite that replaces
the ordinary recheck_defs pass. It uses a new typechecker
check_with_envs function that allows re-writes to utilise intermediate
typechecking environments to minimize the amount of AST checking that
occurs, for performance reasons.
Note that older Sail versions including the current OPAM release will
complain about the optimize pragma, so this cannot be used until they
become up to date with this change.
Diffstat (limited to 'editors')
| -rw-r--r-- | editors/sail-mode.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/editors/sail-mode.el b/editors/sail-mode.el index 38404f14..6dae0761 100644 --- a/editors/sail-mode.el +++ b/editors/sail-mode.el @@ -22,7 +22,7 @@ (defconst sail2-special '("_prove" "_not_prove" "create" "kill" "convert" "undefined" - "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$latex")) + "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$optimize" "$latex")) (defconst sail2-font-lock-keywords `((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face) |