summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
authorJon French2018-12-27 12:14:32 +0000
committerJon French2018-12-27 12:14:32 +0000
commit13169ab85604d926e5dae44202622ec445697793 (patch)
tree3871b08da2fbc518402814bcd94bcb9da7093ade /src/process_file.ml
parent9d2c973d97f10060344f623d8392f56a437b2d04 (diff)
pass typechecking environment around interpreter and rewriters
Diffstat (limited to 'src/process_file.ml')
-rw-r--r--src/process_file.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/process_file.ml b/src/process_file.ml
index 2dfd9571..344c7921 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -375,7 +375,7 @@ let rewrite_step defs (name,rewriter) =
| _ -> () in
defs
-let rewrite rewriters defs =
+let rewrite rewriters env defs =
try List.fold_left rewrite_step defs rewriters with
| Type_check.Type_error (l, err) ->
raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
@@ -385,10 +385,10 @@ let rewrite_undefined bitvectors = rewrite [("undefined", fun x -> Rewrites.rewr
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_c env ast =
ast
- |> rewrite Rewrites.rewrite_defs_c
- |> rewrite [("constant_fold", Constant_fold.rewrite_constant_function_calls)]
+ |> rewrite Rewrites.rewrite_defs_c env
+ |> rewrite [("constant_fold", Constant_fold.rewrite_constant_function_calls env)] env
let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter
let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check