preFront.ml 2.03 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
open Printf

let read_whole_file filename =

  (* Open the file in text mode, so that (under Windows) CRLF is converted to LF.
     This guarantees that one byte is one character and seems to be required in
     order to report accurate positions. *)

  let channel = open_in filename in

  (* The standard library functions [pos_in] and [seek_in] do not work correctly
     when CRLF conversion is being performed, so we abandon their use. (They were
     used to go and extract the text of semantic actions.) Instead we load the
     entire file into memory up front, and work with a string. *)

  (* The standard library function [in_channel_length] does not work correctly
     when CRLF conversion is being performed, so we do not use it to read the
     whole file. And the standard library function [Buffer.add_channel] uses
     [really_input] internally, so we cannot use it either. Bummer. *)

POTTIER Francois's avatar
POTTIER Francois committed
21
  let s = IO.exhaust channel in
22
  close_in channel;
POTTIER Francois's avatar
POTTIER Francois committed
23
  s
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46

let load_partial_grammar filename =
  let validExt = if Settings.coq then ".vy" else ".mly" in
  if Filename.check_suffix filename validExt then
    Error.set_filename filename
  else
    Error.error [] (sprintf "argument file names should end in %s. \"%s\" is not accepted." validExt filename);
  try

    let contents = read_whole_file filename in
    Error.file_contents := Some contents;
    let lexbuf = Lexing.from_string contents in
    lexbuf.Lexing.lex_curr_p <-
	{ 
	  Lexing.pos_fname = filename; 
	  Lexing.pos_lnum  = 1;
	  Lexing.pos_bol   = 0; 
	  Lexing.pos_cnum  = 0
	};
    let grammar =
      { (Parser.grammar Lexer.main lexbuf) with ConcreteSyntax.pg_filename = filename }
    in
    Error.file_contents := None;
47
    grammar
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66

  with Sys_error msg ->
    Error.error [] msg

let partial_grammars = 
  List.map load_partial_grammar Settings.filenames

let () =
  Time.tick "Lexing and parsing"

let parameterized_grammar = 
  PartialGrammar.join_partial_grammars partial_grammars

let grammar = 
  ParameterizedGrammar.expand parameterized_grammar

let () =
  Time.tick "Joining and expanding"