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.mli | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'src/process_file.mli')

diff --git a/src/process_file.mli b/src/process_file.mli
index f75f6687..0411464b 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -56,13 +56,13 @@ val clear_symbols : unit -> unit
 
 val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs
 val check_ast: Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
-val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_coq : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_c : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_interpreter : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast: Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_lem : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_coq : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_ocaml : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_c : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_interpreter : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 
 val load_file_no_check : (Arg.key * Arg.spec * Arg.doc) list -> Ast.order -> string -> unit Ast.defs
 val load_file : (Arg.key * Arg.spec * Arg.doc) list -> Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t
-- 
cgit v1.2.3