env.mli 2.44 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
21 22 23 24 25 26 27 28 29

(** Environment *)

type env

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

val create_env : retrieve_theory -> env

MARCHE Claude's avatar
MARCHE Claude committed
30
(** ??? *)
Andrei Paskevich's avatar
Andrei Paskevich committed
31 32 33 34 35 36
val find_theory : env -> string list -> string -> theory

val env_tag : env -> int

exception TheoryNotFound of string list * string

37 38 39 40 41

(** Parsers *)

type parse_only   = env -> string -> in_channel -> unit
type read_channel = env -> string -> in_channel -> theory Mnm.t
42
type error_report = Format.formatter -> exn -> unit
43 44

val register_parser :
45
  string -> string list -> parse_only -> read_channel -> error_report -> unit
46 47 48 49 50 51 52 53 54
  (** [register_parser name extensions f1 f2] registers a new parser
      under name [name], for files with extensions in list [extensions];
      [f1] is the function to perform parsing only;
      [f2] is the function to retrieve a list of theories from a channel *)

val parse_only   : ?name:string -> parse_only

val read_channel : ?name:string -> read_channel

55 56
val report : ?name:string -> string -> error_report

57 58
exception UnknownParser of string (* parser name *)

59 60
val list_formats : unit -> (string * string list) list