sig
val pretty : Wp.Conditions.sequent Qed.Plib.printer
val dump : Wp.Conditions.bundle Qed.Plib.printer
val dump_bundle :
?clause:string ->
?goal:Wp.Lang.F.pred -> Wp.Conditions.bundle Qed.Plib.printer
val dump_sequence :
?clause:string ->
?goal:Wp.Lang.F.pred -> Wp.Conditions.sequence Qed.Plib.printer
type env = Wp.Plang.Env.t
val alloc_hyp :
Wp.Plang.pool ->
(Wp.Lang.F.var -> unit) -> Wp.Conditions.sequence -> unit
val alloc_seq :
Wp.Plang.pool -> (Wp.Lang.F.var -> unit) -> Wp.Conditions.sequent -> unit
class engine :
#Wp.Plang.engine ->
object
method mark : Wp.Lang.F.marks -> Wp.Conditions.step -> unit
method name : Wp.Pcond.env -> Wp.Lang.F.term -> string
method pp_block :
clause:string -> Wp.Conditions.sequence Qed.Plib.printer
method pp_clause : string Qed.Plib.printer
method pp_comment : string Qed.Plib.printer
method pp_condition :
step:Wp.Conditions.step -> Wp.Conditions.condition Qed.Plib.printer
method pp_core : Wp.Lang.F.term Qed.Plib.printer
method pp_definition :
Stdlib.Format.formatter -> string -> Wp.Lang.F.term -> unit
method pp_esequent :
Wp.Pcond.env -> Wp.Conditions.sequent Qed.Plib.printer
method pp_goal : Wp.Lang.F.pred Qed.Plib.printer
method pp_intro :
step:Wp.Conditions.step ->
clause:string -> ?dot:string -> Wp.Lang.F.pred Qed.Plib.printer
method pp_name : string Qed.Plib.printer
method pp_property : Property.t Qed.Plib.printer
method pp_sequence :
clause:string -> Wp.Conditions.sequence Qed.Plib.printer
method pp_sequent : Wp.Conditions.sequent Qed.Plib.printer
method pp_step : Wp.Conditions.step Qed.Plib.printer
method pp_stmt : string Qed.Plib.printer
method pp_warning : Wp.Warning.t Qed.Plib.printer
end
class state :
object
method bind : Lang.F.var -> string
method callstyle : Qed.Engine.callstyle
method clear : unit
method datatype : Lang.ADT.t -> string
method domain : Wp.Lang.F.Vars.t
method e_false : Qed.Engine.cmode -> string
method e_true : Qed.Engine.cmode -> string
method env : Plang.Env.t
method field : Lang.Field.t -> string
method find : Lang.F.var -> string
method get_iformat : Plang.iformat
method get_rformat : Plang.rformat
method global : (unit -> unit) -> unit
method is_atomic : Lang.F.term -> bool
method is_atomic_lv : Sigs.s_lval -> bool
method label_at : id:int -> Wp.Pcfg.label
method link : Lang.Fun.t -> Qed.Engine.link
method local : (unit -> unit) -> unit
method lookup : Lang.F.term -> Qed.Engine.scope
method marks : Plang.Env.t * Lang.F.marks
method mode : Qed.Engine.mode
method op_add : Qed.Engine.amode -> Qed.Engine.op
method op_and : Qed.Engine.cmode -> Qed.Engine.op
method op_div : Qed.Engine.amode -> Qed.Engine.op
method op_eq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method op_equal : Qed.Engine.cmode -> Qed.Engine.op
method op_equiv : Qed.Engine.cmode -> Qed.Engine.op
method op_imply : Qed.Engine.cmode -> Qed.Engine.op
method op_leq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method op_lt : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method op_minus : Qed.Engine.amode -> Qed.Engine.op
method op_mod : Qed.Engine.amode -> Qed.Engine.op
method op_mul : Qed.Engine.amode -> Qed.Engine.op
method op_neq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op
method op_not : Qed.Engine.cmode -> Qed.Engine.op
method op_noteq : Qed.Engine.cmode -> Qed.Engine.op
method op_or : Qed.Engine.cmode -> Qed.Engine.op
method op_real_of_int : Qed.Engine.op
method op_scope : Qed.Engine.amode -> string option
method op_spaced : string -> bool
method op_sub : Qed.Engine.amode -> Qed.Engine.op
method pp_addr : Format.formatter -> Sigs.s_lval -> unit
method pp_apply :
Qed.Engine.cmode -> Lang.F.term -> Lang.F.term list Qed.Plib.printer
method pp_array : Lang.F.tau Qed.Plib.printer
method pp_array_cst :
Format.formatter -> Lang.F.tau -> Lang.F.term -> unit
method pp_array_get :
Format.formatter -> Lang.F.term -> Lang.F.term -> unit
method pp_array_set :
Format.formatter -> Lang.F.term -> Lang.F.term -> Lang.F.term -> unit
method pp_at : Stdlib.Format.formatter -> Wp.Pcfg.label -> unit
method pp_atom : Lang.F.term Qed.Plib.printer
method pp_chunk : Format.formatter -> string -> unit
method pp_conditional :
Format.formatter -> Lang.F.term -> Lang.F.term -> Lang.F.term -> unit
method pp_datatype : Lang.ADT.t -> Lang.F.tau list Qed.Plib.printer
method pp_def_fields :
(Lang.Field.t * Lang.F.term) list Qed.Plib.printer
method pp_equal : Lang.F.term Qed.Plib.printer2
method pp_exists : Lang.F.tau -> string list Qed.Plib.printer
method pp_expr : Lang.F.tau -> Lang.F.term Qed.Plib.printer
method pp_farray : Lang.F.tau Qed.Plib.printer2
method pp_flow : Lang.F.term Qed.Plib.printer
method pp_forall : Lang.F.tau -> string list Qed.Plib.printer
method pp_fun :
Qed.Engine.cmode -> Lang.Fun.t -> Lang.F.term list Qed.Plib.printer
method pp_get_field :
Format.formatter -> Lang.F.term -> Lang.Field.t -> unit
method pp_host : Format.formatter -> Sigs.s_host -> unit
method pp_imply :
Format.formatter -> Lang.F.term list -> Lang.F.term -> unit
method pp_init : Format.formatter -> Sigs.s_lval -> unit
method pp_int : Qed.Engine.amode -> Z.t Qed.Plib.printer
method pp_label : Format.formatter -> Pcfg.label -> unit
method pp_lambda : (string * Lang.F.tau) list Qed.Plib.printer
method pp_let :
Format.formatter -> Qed.Engine.pmode -> string -> Lang.F.term -> unit
method pp_lval : Format.formatter -> Sigs.s_lval -> unit
method pp_not : Lang.F.term Qed.Plib.printer
method pp_noteq : Lang.F.term Qed.Plib.printer2
method pp_offset : Format.formatter -> Sigs.s_offset list -> unit
method pp_ofs : Format.formatter -> Sigs.s_offset -> unit
method pp_pred : Format.formatter -> Lang.F.pred -> unit
method pp_prop : Lang.F.term Qed.Plib.printer
method pp_real : Q.t Qed.Plib.printer
method pp_repr : Lang.F.term Qed.Plib.printer
method pp_sort : Lang.F.term Qed.Plib.printer
method pp_subtau : Lang.F.tau Qed.Plib.printer
method pp_tau : Lang.F.tau Qed.Plib.printer
method pp_term : Lang.F.term Qed.Plib.printer
method pp_times : Format.formatter -> Z.t -> Lang.F.term -> unit
method pp_tvar : int Qed.Plib.printer
method pp_update :
Wp.Pcfg.label -> Stdlib.Format.formatter -> Wp.Sigs.update -> unit
method pp_value : Stdlib.Format.formatter -> Wp.Lang.F.term -> unit
method pp_var : string Qed.Plib.printer
method sanitize : string -> string
method sanitize_field : string -> string
method sanitize_fun : string -> string
method sanitize_type : string -> string
method scope : Plang.Env.t -> (unit -> unit) -> unit
method set_domain : Wp.Lang.F.Vars.t -> unit
method set_env : Plang.Env.t -> unit
method set_iformat : Plang.iformat -> unit
method set_rformat : Plang.rformat -> unit
method set_sequence : Wp.Conditions.sequence -> unit
method shareable : Lang.F.term -> bool
method shared : Lang.F.term -> bool
method subterms : (Lang.F.term -> unit) -> Lang.F.term -> unit
method t_atomic : Lang.F.tau -> bool
method t_bool : string
method t_int : string
method t_prop : string
method t_real : string
method updates : Wp.Pcfg.label Wp.Sigs.sequence -> Wp.Sigs.update Bag.t
method with_mode : Qed.Engine.mode -> (Qed.Engine.mode -> unit) -> unit
end
class seqengine :
#Wp.Pcond.state ->
object
method get_state : bool
method mark : Lang.F.marks -> Conditions.step -> unit
method name : env -> Lang.F.term -> string
method pp_block : clause:string -> Conditions.sequence Qed.Plib.printer
method pp_clause : string Qed.Plib.printer
method pp_comment : string Qed.Plib.printer
method pp_condition :
step:Conditions.step -> Conditions.condition Qed.Plib.printer
method pp_core : Lang.F.term Qed.Plib.printer
method pp_definition :
Format.formatter -> string -> Lang.F.term -> unit
method pp_esequent : env -> Conditions.sequent Qed.Plib.printer
method pp_goal : Lang.F.pred Qed.Plib.printer
method pp_intro :
step:Conditions.step ->
clause:string -> ?dot:string -> Lang.F.pred Qed.Plib.printer
method pp_name : string Qed.Plib.printer
method pp_property : Property.t Qed.Plib.printer
method pp_sequence :
clause:string -> Conditions.sequence Qed.Plib.printer
method pp_sequent : Conditions.sequent Qed.Plib.printer
method pp_step : Conditions.step Qed.Plib.printer
method pp_stmt : string Qed.Plib.printer
method pp_warning : Warning.t Qed.Plib.printer
method set_goal : Wp.Lang.F.pred -> unit
method set_sequence : Wp.Conditions.sequence -> unit
method set_sequent : Wp.Conditions.sequent -> unit
method set_state : bool -> unit
end
end