package why3

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type fformat = string

type filename = string

type extension = string

type pathname = string list

type env

val env_tag : env -> Weakhtbl.tag

module Wenv : sig ... end

val create_env : filename list -> env

val get_loadpath : env -> filename list

type 'a language

val base_language : Theory.theory Wstdlib.Mstr.t language

val register_language : 'a language -> ('b -> 'a) -> 'b language

val add_builtin : 'a language -> (pathname -> 'a) -> unit

val base_language_builtin : pathname -> Theory.theory Wstdlib.Mstr.t

type !'a format_parser = env -> pathname -> filename -> in_channel -> 'a

exception KnownFormat of fformat

val register_format : 
  desc:Pp.formatted ->
  'a language ->
  fformat ->
  extension list ->
  'a format_parser ->
  unit

val list_formats : 
  'a language ->
  (fformat * extension list * Pp.formatted) list

val get_format : ?format:fformat -> string -> fformat

exception InvalidFormat of fformat

exception UnknownFormat of fformat

exception UnknownExtension of extension

exception UnspecifiedFormat

val read_channel : 
  ?format:fformat ->
  'a language ->
  env ->
  filename ->
  in_channel ->
  'a

val read_file : 
  ?format:fformat ->
  'a language ->
  env ->
  filename ->
  'a * fformat

exception LibraryNotFound of pathname

exception LibraryConflict of pathname

exception AmbiguousPath of filename * filename

val read_library : 'a language -> env -> pathname -> 'a

val locate_library : env -> pathname -> filename

exception TheoryNotFound of pathname * string

val read_theory : env -> pathname -> string -> Theory.theory