Module Driver

module Driver: sig .. end
Memoized loading of drivers according to current WP options. Finally sets LogicBuiltins.driver and returns it.

type bal = [ `Default | `Left | `Nary | `Right ] 
type token = 
| EOF
| KEY of string
| BOOLEAN
| INTEGER
| REAL
| INT of Cil_types.ikind
| FLT of Cil_types.fkind
| KIND of LogicBuiltins.kind
| ID of string
| LINK of string
| RECLINK of (string * (string * bal)) list
| FIELD of string * string
val keywords : (string * token) list
val ident : input -> string
val newline : Lexing.lexbuf -> unit
val conv_bal : ([< `Default | `Left | `Nary | `Right ] as 'a) ->
string * 'a -> Qed.Engine.link
val __ocaml_lex_tables : Lexing.lex_tables
val tok : Lexing.lexbuf -> token
val __ocaml_lex_tok_rec : Lexing.lexbuf -> int -> token
val comment : Lexing.lexbuf -> token
val __ocaml_lex_comment_rec : Lexing.lexbuf -> int -> token
val value : input -> string
val __ocaml_lex_value_rec : Lexing.lexbuf -> int -> string
val string_val : Buffer.t -> Lexing.lexbuf -> string
val __ocaml_lex_string_val_rec : Buffer.t -> Lexing.lexbuf -> int -> string
val recstring : (string * string) list -> Lexing.lexbuf -> (string * string) list
val __ocaml_lex_recstring_rec : (string * string) list -> Lexing.lexbuf -> int -> (string * string) list
val recstring_bis : (string * string) list -> string -> Lexing.lexbuf -> (string * string) list
val __ocaml_lex_recstring_bis_rec : (string * string) list ->
string -> Lexing.lexbuf -> int -> (string * string) list
val recstring_ter : (string * string) list -> string -> Lexing.lexbuf -> (string * string) list
val __ocaml_lex_recstring_ter_rec : (string * string) list ->
string -> Lexing.lexbuf -> int -> (string * string) list
val recorstring : Lexing.lexbuf ->
[> `RecString of (string * string) list | `String of string ]
val __ocaml_lex_recorstring_rec : Lexing.lexbuf ->
int -> [> `RecString of (string * string) list | `String of string ]
val reclink : (string * (string * bal)) list ->
Lexing.lexbuf -> (string * (string * bal)) list
val __ocaml_lex_reclink_rec : (string * (string * bal)) list ->
Lexing.lexbuf -> int -> (string * (string * bal)) list
val reclink_bis : (string * (string * bal)) list ->
string -> Lexing.lexbuf -> (string * (string * bal)) list
val __ocaml_lex_reclink_bis_rec : (string * (string * bal)) list ->
string -> Lexing.lexbuf -> int -> (string * (string * bal)) list
val reclink_ter : (string * (string * bal)) list ->
string -> Lexing.lexbuf -> (string * (string * bal)) list
val __ocaml_lex_reclink_ter_rec : (string * (string * bal)) list ->
string -> Lexing.lexbuf -> int -> (string * (string * bal)) list
val bal : Lexing.lexbuf -> bal
val __ocaml_lex_bal_rec : Lexing.lexbuf -> int -> bal
val pretty : Format.formatter -> token -> unit
type input = {
   lexbuf : Lexing.lexbuf;
   mutable current : token;
}
val skip : input -> unit
val token : input -> token
val value : input -> string
val key : input -> string -> bool
val skipkey : input -> string -> unit
val noskipkey : input -> string -> unit
val ident : input -> string
val kind : input -> LogicBuiltins.kind
val parameter : input -> LogicBuiltins.kind
val parameters : input -> LogicBuiltins.kind list
val signature : input -> LogicBuiltins.kind list
val depend : input -> string list
val link : bal -> input -> Qed.Engine.link Lang.infoprover
val linkstring : input -> string Lang.infoprover
val input_string : input -> string
val op : 'a Qed.Logic.operator
val op_elt : input -> Lang.lfun Qed.Logic.element
val op_link : Lang.lfun Qed.Logic.operator ->
input ->
Lang.lfun Qed.Logic.category * Qed.Engine.link Lang.infoprover
val logic_link : input ->
Lang.lfun Qed.Logic.category * Qed.Engine.link Lang.infoprover
val parse : driver_dir:string -> string -> input -> unit
val load : ?feedback:bool -> string -> unit
val dkey : Log.category
val loaded : (Wp_parameters.Drivers.t * string list, LogicBuiltins.driver) Hashtbl.t
val load_driver : unit -> LogicBuiltins.driver
Memoized loading of drivers according to current WP options. Finally sets LogicBuiltins.driver and returns it.