Module Lang

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 
| Mtype of mdt (*

External type

*)
| Mrecord of mdt * fields (*

External record-type

*)
| Atype of Cil_types.logic_type_info (*

Logic Type

*)
| Comp of Cil_types.compinfo (*

C-code struct or union

*)
type mdt = string extern 

name to print to the provers

name to print to the provers

type 'a extern = {
   ext_id : int;
   ext_link : 'a infoprover;
   ext_library : library; (*

a library which it depends on

a library which it depends on

*)
   ext_debug : string; (*

just for printing during debugging

just for printing during debugging

*)
}
type fields = {
   mutable fields : field list;
}
type field = 
| Mfield of mdt * fields * string * tau
| Cfield of Cil_types.fieldinfo
type tau = (field, adt) Qed.Logic.datatype 
type lfun = 
| ACSL of Cil_types.logic_info (*

Registered in Definition.t, only

Registered in Definition.t, only

*)
| CTOR of Cil_types.logic_ctor_info (*

Not registered in Definition.t directly converted/printed

Not registered in Definition.t, directly converted/printed

*)
| Model of model (*

Generated or External function

*)
type model = {
   m_category : lfun Qed.Logic.category;
   m_params : Qed.Logic.sort list;
   m_result : Qed.Logic.sort;
   m_typeof : tau option list -> tau;
   m_source : source;
}
type source = 
| Generated of string
| Extern of Qed.Engine.link extern
val mem_builtin_type : name:string -> bool
val set_builtin_type : name:string -> link:string infoprover -> library:string -> unit
val get_builtin_type : name:string -> link:string infoprover -> library:string -> adt
val is_builtin : Cil_types.logic_type_info -> bool
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 = 
| Nary
| Left
| Right
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 ->
?typecheck:(tau option list -> 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 ->
?typecheck:(tau option list -> tau) ->
('a, Stdlib.Format.formatter, unit, lfun) Stdlib.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, Stdlib.Format.formatter, unit, lfun) Stdlib.format4 -> 'a
val generated_p : string -> lfun

Sorting and Typing

val tau_of_comp : Cil_types.compinfo -> tau
val tau_of_object : 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 option list -> tau
val tau_of_field : field -> tau
val tau_of_record : field -> tau
val t_int : tau
val t_real : tau
val t_bool : tau
val t_prop : tau
val t_addr : unit -> tau
val t_array : tau -> tau
val t_farray : tau -> tau -> tau
val t_datatype : adt -> tau list -> tau
val pointer : (Cil_types.typ -> tau) Context.value

type of pointers

val floats : (Ctypes.c_float -> tau) Context.value

type of floats

val poly : string list Context.value

polymorphism

val parameters : (lfun -> Qed.Logic.sort list) -> unit

definitions

val name_of_lfun : lfun -> string
val name_of_field : field -> string

Logic Formulae

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 has_gamma : unit -> bool
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

Simplifiers

exception Contradiction
class type simplifier = object .. end