From 0d12cebc11c5beb779209bd290647f6bf58fc3e3 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 8 Feb 2019 13:02:44 +0000
Subject: Rewrite type definitions in rewrite_nexp_ids

For example, in

  type xlen : Int = 64
  type xlenbits = bits(xlen)

rewrite the 'xlen' in the definition of 'xlenbits' to the constant 64 in
order to simplify Lem generation.  In order to facilitate this, pass
through the global typing environment to the rewriting steps (in the AST
itself, type definitions don't carry annotations with environments).
---
 src/process_file.ml | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'src/process_file.ml')

diff --git a/src/process_file.ml b/src/process_file.ml
index 94a6cd3e..52e0cd08 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -378,9 +378,9 @@ let output libpath out_arg files =
       output1 libpath out_arg f type_env defs)
     files
 
-let rewrite_step n total defs (name, rewriter) =
+let rewrite_step n total env defs (name, rewriter) =
   let t = Profile.start () in
-  let defs = rewriter defs in
+  let defs = rewriter env defs in
   Profile.finish ("rewrite " ^ name) t;
   let _ = match !(opt_ddump_rewrite_ast) with
     | Some (f, i) ->
@@ -396,20 +396,20 @@ let rewrite_step n total defs (name, rewriter) =
   Util.progress "Rewrite " name n total;
   defs
 
-let rewrite rewriters defs =
+let rewrite env rewriters defs =
   let total = List.length rewriters in
-  try snd (List.fold_left (fun (n, defs) rw -> n + 1, rewrite_step n total defs rw) (1, defs) rewriters) with
+  try snd (List.fold_left (fun (n, defs) rw -> n + 1, rewrite_step n total env defs rw) (1, defs) rewriters) with
   | Type_check.Type_error (_, l, err) ->
      raise (Reporting.err_typ l (Type_error.string_of_type_error err))
 
-let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
-let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem
-let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_coq
-let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml
-let rewrite_ast_c ast =
+let rewrite_ast env = rewrite env [("initial", fun _ -> Rewriter.rewrite_defs)]
+let rewrite_ast_lem env = rewrite env Rewrites.rewrite_defs_lem
+let rewrite_ast_coq env = rewrite env Rewrites.rewrite_defs_coq
+let rewrite_ast_ocaml env = rewrite env Rewrites.rewrite_defs_ocaml
+let rewrite_ast_c env ast =
   ast
-  |> rewrite Rewrites.rewrite_defs_c
-  |> rewrite [("constant_fold", Constant_fold.rewrite_constant_function_calls)]
+  |> rewrite env Rewrites.rewrite_defs_c
+  |> rewrite env [("constant_fold", fun _ -> Constant_fold.rewrite_constant_function_calls)]
 
-let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter
-let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check
+let rewrite_ast_interpreter env = rewrite env Rewrites.rewrite_defs_interpreter
+let rewrite_ast_check env = rewrite env Rewrites.rewrite_defs_check
-- 
cgit v1.2.3