preFront.ml 1.75 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4 5
(* The front-end. *)

(* ------------------------------------------------------------------------- *)

(* Reading a grammar from a file. *)
6 7 8

let load_partial_grammar filename =
  let validExt = if Settings.coq then ".vy" else ".mly" in
POTTIER Francois's avatar
POTTIER Francois committed
9 10 11 12 13
  if not (Filename.check_suffix filename validExt) then
    Error.error [] (Printf.sprintf
      "argument file names should end in %s. \"%s\" is not accepted."
      validExt filename);
  Error.set_filename filename
14 15
  try

16
    let contents = IO.read_whole_file filename in
17 18 19 20 21 22 23 24 25 26 27 28 29
    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;
30
    grammar
31 32 33 34

  with Sys_error msg ->
    Error.error [] msg

POTTIER Francois's avatar
POTTIER Francois committed
35 36 37 38
(* ------------------------------------------------------------------------- *)

(* Read all of the grammar files that are named on the command line. *)

39 40 41 42 43 44
let partial_grammars = 
  List.map load_partial_grammar Settings.filenames

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

POTTIER Francois's avatar
POTTIER Francois committed
45 46 47 48
(* ------------------------------------------------------------------------- *)

(* If several grammar files were specified, merge them. *)

49 50 51
let parameterized_grammar = 
  PartialGrammar.join_partial_grammars partial_grammars

POTTIER Francois's avatar
POTTIER Francois committed
52 53 54 55 56
(* ------------------------------------------------------------------------- *)

(* Expand away all applications of parameterized nonterminal symbols, so as to
   obtain a grammar without parameterized nonterminal symbols. *)

57 58 59 60 61 62
let grammar = 
  ParameterizedGrammar.expand parameterized_grammar

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