env.ml 4.78 KB
Newer Older
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é                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19 20
(*    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 Ident
21
open Theory
22 23 24 25 26 27

(** Environment *)

type env = {
  env_retrieve : retrieve_theory;
  env_memo     : (string list, theory Mnm.t) Hashtbl.t;
28
  env_tag      : Hashweak.tag;
29 30 31 32
}

and retrieve_theory = env -> string list -> theory Mnm.t

33 34 35 36 37 38 39 40 41
let create_memo () =
  let ht = Hashtbl.create 17 in
  Hashtbl.add ht [] Mnm.empty;
  ht

let create_env = let c = ref (-1) in fun retrieve -> {
  env_retrieve = retrieve;
  env_memo     = create_memo ();
  env_tag      = (incr c; Hashweak.create_tag !c) }
42 43 44

exception TheoryNotFound of string list * string

45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
let get_builtin s =
  if s = builtin_theory.th_name.id_string then builtin_theory else
  if s = highord_theory.th_name.id_string then highord_theory else
  match tuple_theory_name s with
  | Some n -> tuple_theory n
  | None -> raise (TheoryNotFound ([],s))

let find_builtin env s =
  let m = Hashtbl.find env.env_memo [] in
  try Mnm.find s m with Not_found ->
    let th = get_builtin s in
    let m = Mnm.add s th m in
    Hashtbl.replace env.env_memo [] m;
    th

let find_library env sl =
  try Hashtbl.find env.env_memo sl
Andrei Paskevich's avatar
Andrei Paskevich committed
62
  with Not_found ->
63 64 65 66 67 68 69 70 71
    Hashtbl.add env.env_memo sl Mnm.empty;
    let m = env.env_retrieve env sl in
    Hashtbl.replace env.env_memo sl m;
    m

let find_theory env sl s =
  if sl = [] then find_builtin env s
  else try Mnm.find s (find_library env sl)
  with Not_found -> raise (TheoryNotFound (sl, s))
72

73
let env_tag env = env.env_tag
74

75
module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end)
76 77 78

(** Parsers *)

79
type read_channel = env -> string -> in_channel -> theory Mnm.t
80

81 82 83
let read_channel_table = Hashtbl.create 17 (* parser name -> read_channel *)
let suffixes_table     = Hashtbl.create 17 (* suffix -> parser name *)

84
let register_format name suffixes rc =
85 86 87
  Hashtbl.add read_channel_table name rc;
  List.iter (fun s -> Hashtbl.add suffixes_table ("." ^ s) name) suffixes

88
exception NoFormat
89
exception UnknownExtension of string
90
exception UnknownFormat of string (* parser name *)
91

92
let parser_for_file ?format file = match format with
93 94
  | None ->
      begin try
95 96 97 98 99 100
        let ext =
          let s = Filename.chop_extension file in
          let n = String.length s in
          String.sub file n (String.length file - n)
        in
        try Hashtbl.find suffixes_table ext
101
        with Not_found -> raise (UnknownExtension ext)
102 103
      with Invalid_argument _ -> raise NoFormat end
  | Some n -> n
104 105 106

let find_parser table n =
  try Hashtbl.find table n
107
  with Not_found -> raise (UnknownFormat n)
108

109 110
let read_channel ?format env file ic =
  let n = parser_for_file ?format file in
111
  let rc = find_parser read_channel_table n in
112
  rc env file ic
113

114
let read_file ?format env file =
115
  let cin = open_in file in
116
  let m = read_channel ?format env file cin in
117 118 119
  close_in cin;
  m

120 121
let list_formats () =
  let h = Hashtbl.create 17 in
122
  let add s p =
123 124 125 126 127 128
    let l = try Hashtbl.find h p with Not_found -> [] in
    Hashtbl.replace h p (s :: l)
  in
  Hashtbl.iter add suffixes_table;
  Hashtbl.fold (fun p l acc -> (p, l) :: acc) h []

129
(* Exception reporting *)
130 131

let () = Exn_printer.register
132 133 134 135 136 137
  begin fun fmt exn -> match exn with
  | TheoryNotFound (sl, s) ->
      Format.fprintf fmt "Theory not found: %a.%s"
        (Pp.print_list Pp.dot Format.pp_print_string) sl s
  | UnknownFormat s ->
      Format.fprintf fmt "Unknown input format: %s" s
138 139 140 141
  | UnknownExtension s ->
      Format.fprintf fmt "Unknown file extension: %s" s
  | NoFormat ->
      Format.fprintf fmt "No input format given"
142 143
  | _ -> raise exn
  end
144