pgm_main.ml 2.65 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
19 20 21

(* main module for whyl *)

22
open Format
23
open Why
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
24
open Util
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
25
open Ident
26 27 28
open Ptree
open Pgm_ptree
open Pgm_module
29

30
let add_module ?(type_only=false) env penv lmod m =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
31
  let wp = not type_only in
32 33
  let id = m.mod_name in
  let uc = create_module (Ident.id_user id.id id.id_loc) in
34
  let uc = List.fold_left (Pgm_typing.decl ~wp env penv lmod) uc m.mod_decl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
35
  let m = close_module uc in
36
  Mnm.add id.id m lmod
37

38 39 40 41 42 43 44 45 46 47
let retrieve penv file c =
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
  let ml = Pgm_lexer.parse_file lb in
  if Debug.test_flag Typing.debug_parse_only then
    Mnm.empty
  else
    let type_only = Debug.test_flag Typing.debug_type_only in
    let env = Pgm_env.get_env penv in
    List.fold_left (add_module ~type_only env penv) Mnm.empty ml
48 49 50 51 52 53 54 55 56 57 58

let pgm_env_of_env =
  let h = Env.Wenv.create 17 in
  fun env -> 
    try 
      Env.Wenv.find h env 
    with Not_found -> 
      let penv = Pgm_env.create env retrieve in 
      Env.Wenv.set h env penv; 
      penv

59
let read_channel env file c =
60 61 62 63 64
  let penv = pgm_env_of_env env in
  let mm = retrieve penv file c in
  Mnm.fold 
    (fun _ m tm -> Theory.Mnm.add m.m_name.id_string m.m_th tm) 
    mm Theory.Mnm.empty
65

66
let () = Env.register_format "whyml" ["mlw"] read_channel
67 68

(*
69
Local Variables:
70
compile-command: "unset LANG; make -C ../.. testl"
71
End:
72
*)