Module LogicBuiltins

module LogicBuiltins: sig .. end

type category = Lang.lfun Qed.Logic.category 
type kind = 
| Z (*

integer

*)
| R (*

real

*)
| I of Ctypes.c_int (*

C-ints

*)
| F of Ctypes.c_float (*

C-floats

*)
| A (*

Abstract Data

*)
val kind_of_tau : Lang.tau -> kind
val add_builtin : string -> kind list -> Lang.lfun -> unit

Add a new builtin. This builtin will be shared with all created drivers

type driver 
val driver : driver Context.value
val create : id:string ->
?descr:string -> ?includes:string list -> unit -> driver

Create a new driver. leave the context empty.

val init : id:string -> ?descr:string -> ?includes:string list -> unit -> unit

Reset the context to a newly created driver

val id : driver -> string
val descr : driver -> string
val is_default : driver -> bool
val compare : driver -> driver -> int
val find_lib : string -> string

find a file in the includes of the current drivers

val dependencies : string -> string list

Of external theories. Raises Not_found if undefined

val add_library : string -> string list -> unit

Add a new library or update the dependencies of an existing one

val add_alias : source:Lexing.position ->
string -> kind list -> alias:string -> unit -> unit
val add_type : source:Lexing.position ->
string -> library:string -> ?link:string Lang.infoprover -> unit -> unit
val add_ctor : source:Lexing.position ->
string ->
kind list ->
library:string -> link:Qed.Engine.link Lang.infoprover -> unit -> unit
val add_logic : source:Lexing.position ->
kind ->
string ->
kind list ->
library:string ->
?category:category ->
link:Qed.Engine.link Lang.infoprover -> unit -> unit
val add_predicate : source:Lexing.position ->
string ->
kind list ->
library:string -> link:string Lang.infoprover -> unit -> unit
val add_option : driver_dir:string -> string -> string -> library:string -> string -> unit

add a value to an option (group, name)

val set_option : driver_dir:string -> string -> string -> library:string -> string -> unit

reset and add a value to an option (group, name)

type doption 
type sanitizer = driver_dir:string -> string -> string 
val create_option : sanitizer:sanitizer ->
string -> string -> doption

add_option_sanitizer ~driver_dir group name add a sanitizer for group group and option name

val get_option : doption -> library:string -> string list

return the values of option (group, name), return the empty list if not set

type builtin = 
| ACSLDEF
| LFUN of Lang.lfun
| HACK of (Lang.F.term list -> Lang.F.term)
val logic : Cil_types.logic_info -> builtin
val ctor : Cil_types.logic_ctor_info -> builtin
val constant : string -> builtin
val lookup : string -> kind list -> builtin
val hack : string -> (Lang.F.term list -> Lang.F.term) -> unit

Replace a logic definition or predicate by a built-in function. The LogicSemantics compilers will replace `Pcall` and `Tcall` instances of this symbol with the provided Qed function on terms.

val dump : unit -> unit