bundles/menhirLib/menhir-20120123/src/back.ml

   1 (**************************************************************************)
   2 (*                                                                        *)
   3 (*  Menhir                                                                *)
   4 (*                                                                        *)
   5 (*  François Pottier, INRIA Rocquencourt                                  *)
   6 (*  Yann Régis-Gianas, PPS, Université Paris Diderot                      *)
   7 (*                                                                        *)
   8 (*  Copyright 2005-2008 Institut National de Recherche en Informatique    *)
   9 (*  et en Automatique. All rights reserved. This file is distributed      *)
  10 (*  under the terms of the Q Public License version 1.0, with the change  *)
  11 (*  described in file LICENSE.                                            *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* Driver for the back-end. *)
  16
  17 open UnparameterizedSyntax
  18
  19 (* Define an .ml file writer . *)
  20
  21 let write program =
  22   let module P = Printer.Make (struct
  23     let filename = Settings.base ^ ".ml"
  24     let f = open_out filename
  25     let locate_stretches =
  26       if Settings.infer then
  27         (* Typechecking should not fail at this stage. Omit #line directives. *)
  28         None
  29       else
  30         (* 2011/10/19: do not use [Filename.basename]. The [#] annotations that
  31            we insert in the [.ml] file must retain their full path. This does
  32            mean that the [#] annotations depend on how menhir is invoked -- e.g.
  33            [menhir foo/bar.mly] and [cd foo && menhir bar.mly] will produce
  34            different files. Nevertheless, this seems useful/reasonable. *)
  35         Some filename
  36     let raw_stretch_action = false
  37   end) in
  38   P.program program
  39
  40 (* Construct the code, using either the table-based or the code-based
  41    back-end, and pass it on to the printer. (This continuation-passing
  42    style is imposed by the fact that there is no conditional in ocaml's
  43    module language.) *)
  44
  45 let () =
  46   if Settings.coq then
  47     let module B = CoqBackend.Run (struct end) in
  48     let filename = Settings.base ^ ".v" in
  49     let f = open_out filename in
  50     B.write_all f;
  51     exit 0
  52   else
  53     if Settings.table then
  54       let module B = TableBackend.Run (struct end) in
  55       write B.program
  56     else
  57       let module B = CodeBackend.Run (struct end) in
  58       write (Inliner.inline B.program)
  59
  60 (* Write the interface file. *)
  61
  62 let () =
  63   Interface.write()
  64
  65 let () =
  66   Time.tick "Printing"
  67