summaryrefslogtreecommitdiff
path: root/src/process_file.mli
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-07-21 16:49:40 +0100
committerAlasdair Armstrong2017-07-21 16:49:40 +0100
commitb7b6ebc7da062141369d85cd263f1b07561cd396 (patch)
treee5aff5fb55d846bd7d5d25fb42098a283218a545 /src/process_file.mli
parent74f0ba28f7ca4eeff467eb938b919fab6e234f47 (diff)
parentffed37084cd0d529a5be98266ed4946cd251e645 (diff)
Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into sail_new_tc
Diffstat (limited to 'src/process_file.mli')
-rw-r--r--src/process_file.mli11
1 files changed, 6 insertions, 5 deletions
diff --git a/src/process_file.mli b/src/process_file.mli
index b3748145..c966367b 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -42,10 +42,11 @@
val parse_file : string -> Parse_ast.defs
val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t * Ast.order
-val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal.Envmap.t -> Ast.order -> Type_internal.tannot Ast.defs * Type_check.envs
-val rewrite_ast: Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
-val rewrite_ast_lem : Type_check.envs -> Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
-val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
+val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal.Envmap.t -> Ast.order -> Type_check_new.tannot Ast.defs * Type_check_new.Env.t
+val rewrite_ast: Type_check_new.tannot Ast.defs -> Type_check_new.tannot Ast.defs
+val rewrite_ast_lem : Type_check_new.tannot Ast.defs -> Type_check_new.tannot Ast.defs
+val rewrite_ast_ocaml : Type_check_new.tannot Ast.defs -> Type_check_new.tannot Ast.defs
+
val load_file : Type_check_new.Env.t -> string -> Type_check_new.tannot Ast.defs * Type_check_new.Env.t
val opt_new_typecheck : bool ref
@@ -62,7 +63,7 @@ type out_type =
val output :
string -> (* The path to the library *)
out_type -> (* Backend kind *)
- (string * Type_internal.tannot Ast.defs) list -> (*File names paired with definitions *)
+ (string * Type_check_new.tannot Ast.defs) list -> (*File names paired with definitions *)
unit
(** [always_replace_files] determines whether Sail only updates modified files.