diff options
| author | Thomas Bauereiss | 2019-02-08 13:02:44 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-02-08 13:32:49 +0000 |
| commit | 0d12cebc11c5beb779209bd290647f6bf58fc3e3 (patch) | |
| tree | 84b77033d16f457e09317ce02ab59249879bf358 /src/process_file.mli | |
| parent | c2e69e8334cba2f0898c73bcb8ca6cce15858fbf (diff) | |
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).
Diffstat (limited to 'src/process_file.mli')
| -rw-r--r-- | src/process_file.mli | 14 |
1 files changed, 7 insertions, 7 deletions
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 |