summaryrefslogtreecommitdiff
path: root/src/process_file.mli
diff options
context:
space:
mode:
authorThomas Bauereiss2017-07-21 13:32:37 +0100
committerThomas Bauereiss2017-07-21 13:55:26 +0100
commitffed37084cd0d529a5be98266ed4946cd251e645 (patch)
tree5a3565c6a3dc5cccd6425c74e89fbabb22239d47 /src/process_file.mli
parentde99cb50d58423090b30976bdf4ac47dec0526d8 (diff)
Switch to new typechecker (almost)
Initial typecheck still uses previous typechecker
Diffstat (limited to 'src/process_file.mli')
-rw-r--r--src/process_file.mli10
1 files changed, 5 insertions, 5 deletions
diff --git a/src/process_file.mli b/src/process_file.mli
index 9620712a..23851138 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -42,10 +42,10 @@
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 opt_new_typecheck : bool ref
val opt_just_check : bool ref
@@ -61,7 +61,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.