Module Wp.LogicBuiltins

type kind =
  1. | B
    (*

    boolean

    *)
  2. | Z
    (*

    integer

    *)
  3. | R
    (*

    real

    *)
  4. | I of Ctypes.c_int
    (*

    C-ints

    *)
  5. | F of Ctypes.c_float
    (*

    C-floats

    *)
  6. | A
    (*

    Abstract Data

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

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

val add_builtin_type : string -> Lang.adt Lang.extern -> unit

Add a new builtin type. Must be an extern or imported type. This builtin will be shared with all created drivers.

type driver
val driver : driver Context.value
val new_driver : id:string -> ?base:driver -> ?descr:string -> ?configure:(unit -> unit) -> unit -> driver

Creates a configured driver from an existing one. Default:

  • base: builtin WP driver
  • descr: id
  • includes:
  • configure: No-Op The configure is the only operation allowed to modify the content of the newly created driver. Except during static initialization of builtin driver.
val id : driver -> string
val descr : driver -> string
val is_default : driver -> bool
val compare : driver -> driver -> int
val add_type : ?loc:Frama_c_kernel.Fileloc.t -> string -> link:string -> unit
val add_alias : loc:Frama_c_kernel.Fileloc.t -> string -> kind list -> alias:string -> unit
val add_ctor : loc:Frama_c_kernel.Fileloc.t -> string -> kind list -> link:string -> unit
val add_logic : loc:Frama_c_kernel.Fileloc.t -> ?category:category -> kind -> string -> kind list -> link:string -> unit
val add_predicate : loc:Frama_c_kernel.Fileloc.t -> string -> kind list -> link:string -> unit
type builtin =
  1. | ACSLDEF
  2. | LFUN of Lang.lfun Lang.extern
  3. | HACK of Lang.F.term list -> Lang.F.term
type t_builtin =
  1. | ADT of Lang.adt Lang.extern
  2. | HACKT of Lang.F.tau list -> Lang.F.tau
val constant : string -> builtin
val lookup : string -> kind list -> builtin
val lookup_t : string -> t_builtin
val resolve_t : string -> Lang.tau list -> Lang.tau
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 hack_type : string -> (Lang.F.tau list -> Lang.F.tau) -> unit

Replace a logic type definition or predicate by a built-in type.

val is_builtin_type : string -> bool
val dump : unit -> unit