Fix rewriter issues

Allow pat_lits rewrite to map L_unit to wildcard patterns, rather than
introducing eq_unit tests as guards.

Add a fold_function and fold_funcl functions in rewriter.ml that apply
the pattern and expression algebras to top-level functions, which
means that they correctly get applied to top-level function patterns
when they are used. Currently modifying the re-writing passes to do
this introduces some bugs which needs investigated further. The
current situation is that top-level patterns and patterns elsewhere
are often treated differently because rewrite_exp doesn't (and indeed
cannot, due to how the re-writer is structured) rewrite top level
patterns.

Fix pattern completeness check for unit literals

Fix a bug in Sail->ANF transform where blocks were always annotated
with type unit incorrectly. This caused issues in pattern literal
re-writes where the guard was a block returning a boolean. A test case
for this is added as test/c/and_block.sail.

Fix a bug caused by nested polymorphic function calls and matching in
top-level patterns. Test case is test/c/tl_poly_match.sail.

Pass location info through codegen_conversion for better error
reporting

1 files changed, 3 insertions, 0 deletions

diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index c6fb5308..d54bbd3f 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -91,6 +91,9 @@ let is_wild = function
 
 let rec generalize ctx (P_aux (p_aux, _) as pat) =
   match p_aux with
+  | P_lit (L_aux (L_unit, _)) ->
+     (* Unit pattern always matches on unit, so generalize to wildcard *)
+     GP_wild
   | P_lit lit -> GP_lit lit
   | P_wild -> GP_wild
   | P_or (pat1, pat2) -> GP_or (generalize ctx pat1, generalize ctx pat2)