From 8258b81bf1485e3133fb4351413ed1f554717f43 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 22 Jan 2019 18:04:16 +0000
Subject: 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.
---
 src/rewrites.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/rewrites.ml')

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 8894f2c8..382f9c8f 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5129,7 +5129,7 @@ let rewrite_defs_c = [
   ("trivial_sizeof", rewrite_trivial_sizeof);
   ("sizeof", rewrite_sizeof);
   ("merge_function_clauses", merge_funcls);
-  ("recheck_defs", recheck_defs)
+  ("recheck_defs", Optimize.recheck)
   ]
 
 let rewrite_defs_interpreter = [
-- 
cgit v1.2.3