mlw_main.ml 2.15 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4
5
6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Util
23
open Mlw_module
24
25
26
27
28
29
30
31
32
open Mlw_typing

let read_channel env path file c =
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
  let ml = Lexer.parse_program_file lb in
  if Debug.test_flag Typing.debug_parse_only then
    Mstr.empty, Mstr.empty
  else
33
34
35
36
    let mm, tm =
      List.fold_left (add_theory_module env path) (Mstr.empty, Mstr.empty) ml
    in
    Mstr.iter (fun _ m ->
37
38
39
      Format.fprintf Format.err_formatter
        "@[<hov 2>module %a@\n%a@]@\nend@." Pretty.print_th m.mod_theory
        (Pp.print_list Pp.newline2 Mlw_pretty.print_pdecl) m.mod_decls;
40
41
      Format.pp_print_newline Format.err_formatter ()) mm;
    mm, tm
42
43

let library_of_env = Env.register_format "whyml-exp" ["mlx"] read_channel