diff options
| -rw-r--r-- | src/process_file.ml | 30 | ||||
| -rw-r--r-- | src/process_file.mli | 1 | ||||
| -rw-r--r-- | src/type_check.ml | 2 |
3 files changed, 19 insertions, 14 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 0601bfab..315e44bb 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -45,16 +45,17 @@ type out_type = | Lem_out of string option | Ocaml_out of string option -let get_lexbuf fn = - let lexbuf = Lexing.from_channel (open_in fn) in - lexbuf.Lexing.lex_curr_p <- { Lexing.pos_fname = fn; - Lexing.pos_lnum = 1; - Lexing.pos_bol = 0; - Lexing.pos_cnum = 0; }; - lexbuf +let get_lexbuf f = + let in_chan = open_in f in + let lexbuf = Lexing.from_channel in_chan in + lexbuf.Lexing.lex_curr_p <- { Lexing.pos_fname = f; + Lexing.pos_lnum = 1; + Lexing.pos_bol = 0; + Lexing.pos_cnum = 0; }; + lexbuf, in_chan let parse_file (f : string) : Parse_ast.defs = - let scanbuf = get_lexbuf f in + let scanbuf, in_chan = get_lexbuf f in let type_names = try Pre_parser.file Pre_lexer.token scanbuf @@ -67,13 +68,15 @@ let parse_file (f : string) : Parse_ast.defs = | Lexer.LexError(s,p) -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) in let () = Lexer.custom_type_names := !Lexer.custom_type_names @ type_names in - let lexbuf = get_lexbuf f in + close_in in_chan; + let lexbuf, in_chan = get_lexbuf f in try - Parser.file Lexer.token lexbuf + let ast = Parser.file Lexer.token lexbuf in + close_in in_chan; ast with | Parsing.Parse_error -> let pos = Lexing.lexeme_start_p lexbuf in - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main"))) + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main"))) | Parse_ast.Parse_error_locn(l,m) -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))) | Lexer.LexError(s,p) -> @@ -83,9 +86,10 @@ let parse_file (f : string) : Parse_ast.defs = (*Should add a flag to say whether we want to consider Oinc or Odec the default order *) let convert_ast (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast defs +let load_file_no_check f = convert_ast (parse_file f) + let load_file env f = - let ast = parse_file f in - let ast = convert_ast ast in + let ast = convert_ast (parse_file f) in Type_check.check env ast let opt_new_typecheck = ref false diff --git a/src/process_file.mli b/src/process_file.mli index b15523bb..6defc7ba 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -48,6 +48,7 @@ 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_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val load_file_no_check : string -> unit Ast.defs val load_file : Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t val opt_new_typecheck : bool ref diff --git a/src/type_check.ml b/src/type_check.ml index a413451f..c270287f 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1694,7 +1694,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ begin let (start, len, ord, vtyp) = destructure_vec_typ l env typ in let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in - match len with + match nexp_simp len with | Nexp_aux (Nexp_constant lenc, _) -> if List.length vec = lenc then annot_exp (E_vector checked_items) typ else typ_error l "List length didn't match" (* FIXME: improve error message *) |