module Lang: sig
.. end
Logic Language based on Qed
Library
type
library = string
type 'a
infoprover = {
|
altergo : 'a ; |
|
why3 : 'a ; |
|
coq : 'a ; |
}
generic way to have different informations for the provers
val infoprover : 'a -> 'a infoprover
same information for all the provers
Naming
Unique identifiers.
val comp_id : Cil_types.compinfo -> string
val field_id : Cil_types.fieldinfo -> string
val type_id : Cil_types.logic_type_info -> string
val logic_id : Cil_types.logic_info -> string
val lemma_id : string -> string
Symbols
type
adt = private
type
mdt = string extern
name to print to the provers
type 'a
extern = {
}
type
fields = {
|
mutable fields : field list ; |
}
type
field =
type
tau = (field, adt) Qed.Logic.datatype
type
lfun =
type
model = {
|
m_category : lfun Qed.Logic.category ; |
|
m_params : Qed.Logic.sort list ; |
|
m_resort : Qed.Logic.sort ; |
|
m_result : tau option ; |
|
m_source : source ; |
}
type
source =
| |
Generated of string |
| |
Extern of Qed.Engine.link extern |
val builtin_type : name:string -> link:string infoprover -> library:string -> unit
val is_builtin_type : name:string -> tau -> bool
val datatype : library:string -> string -> adt
val record : link:string infoprover ->
library:string -> (string * tau) list -> adt
val atype : Cil_types.logic_type_info -> adt
val comp : Cil_types.compinfo -> adt
val field : adt -> string -> field
val fields_of_adt : adt -> field list
val fields_of_tau : tau -> field list
val fields_of_field : field -> field list
type
balance =
val extern_s : library:library ->
?link:Qed.Engine.link infoprover ->
?category:lfun Qed.Logic.category ->
?params:Qed.Logic.sort list ->
?sort:Qed.Logic.sort -> ?result:tau -> string -> lfun
val extern_f : library:library ->
?link:Qed.Engine.link infoprover ->
?balance:balance ->
?category:lfun Qed.Logic.category ->
?params:Qed.Logic.sort list ->
?sort:Qed.Logic.sort ->
?result:tau ->
('a, Format.formatter, unit, lfun) Pervasives.format4 -> 'a
balance just give a default when link is not specified
val extern_p : library:library ->
?bool:string ->
?prop:string ->
?link:Qed.Engine.link infoprover ->
?params:Qed.Logic.sort list -> unit -> lfun
val extern_fp : library:library ->
?params:Qed.Logic.sort list ->
?link:string infoprover -> string -> lfun
val generated_f : ?category:lfun Qed.Logic.category ->
?params:Qed.Logic.sort list ->
?sort:Qed.Logic.sort ->
?result:tau ->
('a, Format.formatter, unit, lfun) Pervasives.format4 -> 'a
val generated_p : string -> lfun
Sorting and Typing
val tau_of_comp : Cil_types.compinfo -> tau
val tau_of_object : Wp.Ctypes.c_object -> tau
val tau_of_ctype : Cil_types.typ -> tau
val tau_of_ltype : Cil_types.logic_type -> tau
val tau_of_return : Cil_types.logic_info -> tau
val tau_of_lfun : lfun -> tau
val tau_of_field : field -> tau
val tau_of_record : field -> tau
val array : tau -> tau
val farray : tau -> tau -> tau
val pointer : (Cil_types.typ -> tau) Wp.Context.value
type of pointers
val poly : string list Wp.Context.value
polymorphism
val parameters : (lfun -> Qed.Logic.sort list) -> unit
definitions
val name_of_lfun : lfun -> string
val name_of_field : field -> string
module ADT: Logic.Data
with type t = adt
module Field: Logic.Field
with type t = field
module Fun: Logic.Function
with type t = lfun
class virtual idprinting :
object
.. end
module F: sig
.. end
module N: sig
.. end
Fresh Variables and Constraints
type
gamma
val new_pool : ?copy:F.pool -> ?vars:F.Vars.t -> unit -> F.pool
val new_gamma : ?copy:gamma -> unit -> gamma
val local : ?pool:F.pool ->
?vars:F.Vars.t -> ?gamma:gamma -> ('a -> 'b) -> 'a -> 'b
val freshvar : ?basename:string -> F.tau -> F.var
val freshen : F.var -> F.var
val assume : F.pred -> unit
val without_assume : ('a -> 'b) -> 'a -> 'b
val epsilon : ?basename:string ->
F.tau -> (F.term -> F.pred) -> F.term
val hypotheses : gamma -> F.pred list
val variables : gamma -> F.var list
val get_pool : unit -> F.pool
val get_gamma : unit -> gamma
val get_hypotheses : unit -> F.pred list
val get_variables : unit -> F.var list
Alpha Conversion
module Alpha: sig
.. end
Substitution
module Subst: sig
.. end