package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Library
Module
Module type
Parameter
Class
Class type
module M = Model
module MapString : sig ... end
type prover = {
  1. id : int;
  2. name : string;
  3. version : string;
  4. timelimit : int;
  5. steplimit : int;
  6. memlimit : int;
}
val prover_to_yojson : prover -> Yojson.Safe.t
val pp_prover : Ppx_deriving_runtime.Format.formatter -> prover -> Ppx_deriving_runtime.unit
val show_prover : prover -> Ppx_deriving_runtime.string
type result = {
  1. status : string;
  2. time : string;
  3. steps : int;
}
val result_to_yojson : result -> Yojson.Safe.t
val pp_result : Ppx_deriving_runtime.Format.formatter -> result -> Ppx_deriving_runtime.unit
val show_result : result -> Ppx_deriving_runtime.string
type proof = {
  1. prover_id : string;
  2. result : result;
}
val proof_to_yojson : proof -> Yojson.Safe.t
val pp_proof : Ppx_deriving_runtime.Format.formatter -> proof -> Ppx_deriving_runtime.unit
type goal = {
  1. name : string;
  2. expl : string;
  3. proved : bool;
  4. proofs : proof list;
  5. transf : transf option;
}
and transf = {
  1. name : string;
  2. goals : goal list;
}
val goal_to_yojson : goal -> Yojson.Safe.t
val transf_to_yojson : transf -> Yojson.Safe.t
val pp_goal : Ppx_deriving_runtime.Format.formatter -> goal -> Ppx_deriving_runtime.unit
val pp_transf : Ppx_deriving_runtime.Format.formatter -> transf -> Ppx_deriving_runtime.unit
val show_transf : transf -> Ppx_deriving_runtime.string
type theory = {
  1. name : string;
  2. proved : bool;
  3. goals : goal list;
}
val theory_to_yojson : theory -> Yojson.Safe.t
val pp_theory : Ppx_deriving_runtime.Format.formatter -> theory -> Ppx_deriving_runtime.unit
val show_theory : theory -> Ppx_deriving_runtime.string
type file = {
  1. format : string;
  2. theory : theory list;
}
val file_to_yojson : file -> Yojson.Safe.t
val pp_file : Ppx_deriving_runtime.Format.formatter -> file -> Ppx_deriving_runtime.unit
type why3session = {
  1. shape_version : string;
  2. provers : prover list;
  3. file : file;
}
val why3session_to_yojson : why3session -> Yojson.Safe.t
val pp_why3session : Ppx_deriving_runtime.Format.formatter -> why3session -> Ppx_deriving_runtime.unit
val show_why3session : why3session -> Ppx_deriving_runtime.string
val mk_prover : int -> string -> string -> int -> int -> int -> prover
val mk_result : string -> string -> int -> result
val mk_proof : string -> result -> proof
val mk_goal : ?proofs:proof list -> ?transf:transf -> string -> string -> bool -> goal
val mk_transf : string -> goal list -> transf
val mk_theory : ?goals:goal list -> string -> bool -> theory
val mk_file : ?theory:theory list -> string -> file
val mk_why3session : ?provers:prover list -> string -> file -> why3session
val doit : Xmlm.signal -> unit
val is_tag : Tools.String.t -> [> `El_start of ('a * Tools.String.t) * 'b ] -> bool
val is_end : [> `El_end ] -> bool
val skip : Tools.String.t -> Xmlm.signal Stdlib.ref -> Xmlm.input -> unit
val extract_attributes : Xmlm.attribute list -> string MapString.t
val extract_cb : ('a -> 'b) -> 'c -> MapString.key -> 'd MapString.t -> 'e
val extract_int : MapString.key -> string MapString.t -> int
val extract_bool : MapString.key -> string MapString.t -> bool
val extract_string : MapString.key -> string MapString.t -> string
val extract_prover : Xmlm.signal -> prover
val extract_provers : Xmlm.signal Stdlib.ref -> Xmlm.input -> prover list
val extract_result : Xmlm.signal Stdlib.ref -> Xmlm.input -> result
val extract_proof : Xmlm.signal Stdlib.ref -> Xmlm.input -> proof
val extract_proofs : Xmlm.signal Stdlib.ref -> Xmlm.input -> proof list
val extract_goal : Xmlm.signal Stdlib.ref -> Xmlm.input -> goal
val extract_trans : Xmlm.signal Stdlib.ref -> Xmlm.input -> transf
val extract_goals : Xmlm.signal Stdlib.ref -> Xmlm.input -> goal list
val extract_theory : Xmlm.signal Stdlib.ref -> Xmlm.input -> theory
val extract_theories : Xmlm.signal Stdlib.ref -> Xmlm.input -> theory list
val to_whysession : Stdlib.in_channel -> why3session
type status =
  1. | Ssuccessful
  2. | Sfail of int
val status_to_yojson : status -> Yojson.Safe.t
val pp_status : Ppx_deriving_runtime.Format.formatter -> status -> Ppx_deriving_runtime.unit
val show_status : status -> Ppx_deriving_runtime.string
type res = {
  1. name : string;
  2. total : int;
  3. status : status;
}
val res_to_yojson : res -> Yojson.Safe.t
val pp_res : Ppx_deriving_runtime.Format.formatter -> res -> Ppx_deriving_runtime.unit
type kind =
  1. | Kvariable of string
  2. | Kasset of string
  3. | KassetField of string * string
  4. | KenumField of string * string
  5. | KentryPostcond of string * string
  6. | KentryInv of string * string
val kind_to_yojson : kind -> Yojson.Safe.t
val pp_kind : Ppx_deriving_runtime.Format.formatter -> kind -> Ppx_deriving_runtime.unit
type item = {
  1. id : string;
  2. kind : kind;
  3. formula : string option;
  4. res : res;
}
val item_to_yojson : item -> Yojson.Safe.t
val pp_item : Ppx_deriving_runtime.Format.formatter -> item -> Ppx_deriving_runtime.unit
type report = {
  1. name : string;
  2. items : item list;
}
val report_to_yojson : report -> Yojson.Safe.t
val _ : Yojson.Safe.t -> report Ppx_deriving_yojson_runtime.error_or
val pp_report : Ppx_deriving_runtime.Format.formatter -> report -> Ppx_deriving_runtime.unit
val show_report : report -> Ppx_deriving_runtime.string
val mk_res : string -> int -> status -> res
val mk_item : string -> kind -> string option -> res -> item
val mk_report : ?items:item list -> string -> report
val extract : M.model -> why3session -> report
val process : M.model -> string -> unit