Module Definitions

module Definitions: sig .. end

return type of an abstract function

Unique

type trigger = (Lang.F.var, Lang.lfun) Qed.Engine.ftrigger

type typedef = (Lang.F.tau, Lang.field, Lang.lfun) Qed.Engine.ftypedef

type cluster = {

	`c_id : string;`
	`c_title : string;`
	`c_position : Lexing.position option;`
	`mutable c_age : int;`
	`mutable c_records : Cil_types.compinfo list;`
	`mutable c_types : Cil_types.logic_type_info list;`
	`mutable c_symbols : dfun list;`
	`mutable c_lemmas : dlemma list;`

}

type dlemma = {

`l_name : string;`
`l_cluster : cluster;`
`l_assumed : bool;`
`l_types : int;`
`l_forall : Lang.F.var list;`
`l_triggers : trigger list list;`	`(*`	OR of AND-triggers	`*)`
`l_lemma : Lang.F.pred;`

}

type dfun = {

	`d_lfun : Lang.lfun;`
	`d_cluster : cluster;`
	`d_types : int;`
	`d_params : Lang.F.var list;`
	`d_definition : definition;`

}

type definition =

`\|`	`Logic of Lang.F.tau`	`(*`	return type of an abstract function	`*)`
`\|`	`Value of Lang.F.tau * recursion * Lang.F.term`
`\|`	`Predicate of recursion * Lang.F.pred`
`\|`	`Inductive of dlemma list`

type recursion =

`\|`	`Def`
`\|`	`Rec`

module Trigger: sig .. end

module Cluster: Model.Index(sig
type key = string 


type data = Definitions.cluster 


val name : string
val compare : String.t -> String.t -> int
val pretty : Format.formatter -> string -> unit
end)

module Symbol: Model.Index(sig
type key = Lang.lfun 


type data = Definitions.dfun 


val name : string
val compare : Lang.Fun.t -> Lang.Fun.t -> int
val pretty : Format.formatter -> Lang.Fun.t -> unit
end)

module Lemma: Model.Index(sig
type key = string 


type data = Definitions.dlemma 


val name : string
val compare : String.t -> String.t -> int
val pretty : Format.formatter -> string -> unit
end)

val touch : cluster -> unit

val compare_symbol : dfun -> dfun -> int

val compare_lemma : dlemma -> dlemma -> int

val define_symbol : Symbol.data -> unit

val update_symbol : Symbol.data -> unit

val find_lemma : LogicUsage.logic_lemma -> Lemma.data

raises Not_found

val compile_lemma : (LogicUsage.logic_lemma -> Lemma.data) ->
       LogicUsage.logic_lemma -> unit

val define_lemma : Lemma.data -> unit

val define_type : cluster -> Cil_types.logic_type_info -> unit

val parameters : Symbol.key -> Qed.Logic.sort list

val cluster_id : cluster -> string

Unique

val cluster_title : cluster -> string

val cluster_position : cluster -> Lexing.position option

val cluster_age : cluster -> int

val cluster_compare : cluster -> cluster -> int

val pp_cluster : Format.formatter -> cluster -> unit

val newcluster : id:string ->
       ?title:string -> ?position:Lexing.position -> unit -> cluster

val cluster : id:Cluster.key ->
       ?title:Cluster.key ->
       ?position:Lexing.position -> unit -> Cluster.data

val axiomatic : LogicUsage.axiomatic -> Cluster.data

val section : LogicUsage.logic_section -> Cluster.data

val compinfo : Cil_types.compinfo -> Cluster.data

val matrix : Ctypes.c_object -> Cluster.data

val call_fun : Symbol.key ->
       (Symbol.key -> Symbol.data) ->
       Lang.F.term list -> Lang.F.term

val call_pred : Symbol.key ->
       (Symbol.key -> Symbol.data) ->
       Lang.F.term list -> Lang.F.pred

module DT: Cil_datatype.Logic_type_info.Set

module DR: Cil_datatype.Compinfo.Set

module DS: Datatype.String.Set

module DF: FCSet.Make(Lang.Fun)

module DC: FCSet.Make(sig
type t = Definitions.cluster 


val compare : Definitions.cluster -> Definitions.cluster -> int
end)

type axioms = cluster * LogicUsage.logic_lemma list

class virtual visitor : DC.elt -> object .. end