pgm_main.ml 2.65 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
7 8 9 10 11 12 13 14 15 16 17 18
(*    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
let retrieve penv file c =
39 40
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
41
  let ml = Pgm_lexer.parse_file lb in
42
  if Debug.test_flag Typing.debug_parse_only then
43 44
    Mnm.empty
  else
45
    let type_only = Debug.test_flag Typing.debug_type_only in
46 47
    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
*)