back.ml 3.43 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(******************************************************************************)
(*                                                                            *)
(*                                   Menhir                                   *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*              Yann Régis-Gianas, PPS, Université Paris Diderot              *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU General Public License version 2, as described in the    *)
(*  file LICENSE.                                                             *)
(*                                                                            *)
(******************************************************************************)

14 15
(* Driver for the back-end. *)

16 17 18 19 20
(* Let [Interpret] handle the command line options [--interpret],
   [--interpret-error], [--compile-errors], [--compare-errors]. *)

let () =
  Interpret.run()
21

22 23 24 25
(* If [--list-errors] is set, produce a list of erroneous input sentences, then stop. *)

let () =
  if Settings.list_errors then begin
26
    let module L = LRijkstra.Run(struct
27 28
      (* Undocumented: if [--log-automaton 2] is set, be verbose. *)
      let verbose = Settings.logA >= 2
POTTIER Francois's avatar
POTTIER Francois committed
29
      (* For my own purposes, LRijkstra can print one line of statistics to a .csv file. *)
30
      let statistics = if false then Some "lr.csv" else None
31
    end) in
32 33 34
    exit 0
  end

35 36 37 38 39 40 41
(* Define an .ml file writer . *)

let write program =
  let module P = Printer.Make (struct
    let filename = Settings.base ^ ".ml"
    let f = open_out filename
    let locate_stretches =
42 43 44 45 46 47 48 49 50 51
      (* 2017/05/09: always include line number directives in generated .ml
         files. Indeed, they affect the semantics of [assert] instructions
         in the semantic actions. *)
      (* 2011/10/19: do not use [Filename.basename]. The line number
         directives that we insert in the [.ml] file must retain their full
         path. This does mean that the line number directives depend on how
         menhir is invoked -- e.g. [menhir foo/bar.mly] and [cd foo && menhir
         bar.mly] will produce different files. Nevertheless, this seems
         useful/reasonable. *)
      Some filename
52 53 54
  end) in
  P.program program

55 56 57 58 59 60 61 62 63 64 65 66
(* If requested, generate a .cmly file. *)

let () =
  if Settings.cmly then
    Cmly_write.write (Settings.base ^ ".cmly")

(* The following DEAD code forces [Cmly_read] to be typechecked. *)
let () =
  if false then
    let module R = Cmly_read.Read (struct let filename = "" end) in
    ()

67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84
(* Construct the code, using either the table-based or the code-based
   back-end, and pass it on to the printer. (This continuation-passing
   style is imposed by the fact that there is no conditional in ocaml's
   module language.) *)

let () =
  if Settings.coq then
    let module B = CoqBackend.Run (struct end) in
    let filename = Settings.base ^ ".v" in
    let f = open_out filename in
    B.write_all f;
    exit 0
  else
    if Settings.table then
      let module B = TableBackend.Run (struct end) in
      write B.program
    else
      let module B = CodeBackend.Run (struct end) in
85
      write (CodeInliner.inline B.program)
86 87 88 89

(* Write the interface file. *)

let () =
90
  Interface.write Front.grammar ()
91 92 93

let () =
  Time.tick "Printing"