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

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;
44 45
  | Pgm_lexer.Error e ->
      fprintf fmt "lexical error: %a" Pgm_lexer.report e;
46 47 48 49 50 51
  | 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
52
  | e ->
53 54
      fprintf fmt "anomaly: %s" (Printexc.to_string e)

55 56 57 58 59
open Pgm_ptree
open Theory

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

60 61 62 63
let type_file file =
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
64
  let p = Pgm_lexer.parse_file lb in 
65 66
  close_in c;
  if !parse_only then raise Exit;
67 68 69 70
  let uc = Theory.create_theory (Ident.id_fresh "Pgm") in
  let _uc = 
    List.fold_left
      (fun uc d -> match d with
71
	 | Dlogic dl -> List.fold_left (Typing.add_decl env Mnm.empty) uc dl
72
	 | Dcode (id, e) -> ignore (Pgm_typing.code id e); uc)
73 74
      uc p
  in
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
  ()

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: 
*)