preFront.ml 1.1 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
open Printf

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

11
    let contents = IO.read_whole_file filename in
12 13 14 15 16 17 18 19 20 21 22 23 24
    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;
25
    grammar
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44

  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"