pgm_main.ml 3.29 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
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

let files = ref []
let parse_only = ref false
let type_only = ref false
let debug = ref false
let loadpath = ref []

let () = 
  Arg.parse 
    ["--parse-only", Arg.Set parse_only, "stops after parsing";
     "--type-only", Arg.Set type_only, "stops after type-checking";
     "--debug", Arg.Set debug, "sets the debug flag";
     "-I", Arg.String (fun s -> loadpath := s :: !loadpath), 
       "<dir>  adds dir to the loadpath";
    ]
    (fun f -> files := f :: !files)
    "usage: whyl [options] files..."

let rec report fmt = function
  | Lexer.Error e ->
      fprintf fmt "lexical error: %a" Lexer.report e;
45
46
  | Pgm_lexer.Error e ->
      fprintf fmt "lexical error: %a" Pgm_lexer.report e;
47
48
49
50
51
52
  | Loc.Located (loc, e) ->
      fprintf fmt "%a%a" Loc.report_position loc report e
  | Parsing.Parse_error ->
      fprintf fmt "syntax error"
  | Typing.Error e ->
      Typing.report fmt e
53
54
  | Pgm_typing.Error e ->
      Pgm_typing.report fmt e
55
56
  | Denv.Error e ->
      Denv.report fmt e
57
  | e ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
58
59
      raise e
(*       fprintf fmt "anomaly: %s" (Printexc.to_string e) *)
60

61
62
63
64
65
open Pgm_ptree
open Theory

let env = Env.create_env (Typing.retrieve !loadpath)

66
67
68
69
let type_file file =
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
70
  let p = Pgm_lexer.parse_file lb in 
71
72
  close_in c;
  if !parse_only then raise Exit;
73
  let uc = Theory.create_theory (Ident.id_fresh "Pgm") in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
74
75
  let th = Env.find_theory env ["programs"] "Prelude" in
  let uc = Theory.use_export uc th in
76
  let uc, dl = Pgm_typing.file env uc p in
77
  if !type_only then raise Exit;
78
  let th = Pgm_wp.file uc dl in
79
  printf "%a@." Pretty.print_theory th;
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
  ()

let handle_file file =
  try
    type_file file
  with Exit -> 
    ()

let () =
  try
    List.iter handle_file !files
  with e when not !debug ->
    eprintf "%a@." report e;
    exit 1

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