diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 54 |
1 files changed, 29 insertions, 25 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 273979cf..0601bfab 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -40,8 +40,6 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Type_internal - type out_type = | Lem_ast_out | Lem_out of string option @@ -57,7 +55,7 @@ let get_lexbuf fn = let parse_file (f : string) : Parse_ast.defs = let scanbuf = get_lexbuf f in - let type_names = + let type_names = try Pre_parser.file Pre_lexer.token scanbuf with @@ -81,27 +79,35 @@ let parse_file (f : string) : Parse_ast.defs = | Lexer.LexError(s,p) -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) + (*Should add a flag to say whether we want to consider Oinc or Odec the default order *) -let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)= - Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs - -let initi_check_ast (defs : Type_internal.tannot Ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)= - Initial_check_full_ast.to_checked_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs - -let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs * Type_check.envs = - let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env; - Type_internal.nabbrevs = Envmap.empty; - Type_internal.namesch = Envmap.empty; Type_internal.enum_env = Envmap.empty; - Type_internal.rec_env = []; Type_internal.alias_env = Envmap.empty; - Type_internal.default_o = - {Type_internal.order = (match o with | (Ast.Ord_aux(Ast.Ord_inc,_)) -> Type_internal.Oinc - | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec - | _ -> Type_internal.Oinc)};} in - Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob,Envmap.empty)) defs - -let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs -let rewrite_ast_lem (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs_lem defs -let rewrite_ast_ocaml (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs_ocaml defs +let convert_ast (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast defs + +let load_file env f = + let ast = parse_file f in + let ast = convert_ast ast in + Type_check.check env ast + +let opt_new_typecheck = ref false +let opt_just_check = ref false +let opt_ddump_tc_ast = ref false +let opt_dno_cast = ref false + +let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t = + let ienv = if !opt_dno_cast then Type_check.Env.no_casts Type_check.initial_env else Type_check.initial_env in + let ast, env = Type_check.check ienv defs in + let () = if !opt_ddump_tc_ast then Pretty_print.pp_defs stdout ast else () in + let () = if !opt_just_check then exit 0 else () in + (ast, env) + +let monomorphise_ast locs ast = + let ast = Monomorphise.split_defs locs ast in + let ienv = Type_check.Env.no_casts Type_check.initial_env in + Type_check.check ienv ast + +let rewrite_ast (defs: Type_check.tannot Ast.defs) = Rewriter.rewrite_defs defs +let rewrite_ast_lem (defs: Type_check.tannot Ast.defs) = Rewriter.rewrite_defs_lem defs +let rewrite_ast_ocaml (defs: Type_check.tannot Ast.defs) = Rewriter.rewrite_defs_ocaml defs let open_output_with_check file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in @@ -217,10 +223,8 @@ let output1 libpath out_arg filename defs = Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z"; "Sail_values"; lib]; close_output_with_check ext_o - let output libpath out_arg files = List.iter (fun (f, defs) -> output1 libpath out_arg f defs) files - |