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 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 show_result : result -> Ppx_deriving_runtime.string
type proof = {
  1. prover_id : string;
  2. result : result;
}
val proof_to_yojson : proof -> Yojson.Safe.t
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 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 show_theory : theory -> Ppx_deriving_runtime.string
type file = {
  1. format : string;
  2. theory : theory list;
}
val file_to_yojson : file -> Yojson.Safe.t
type why3session = {
  1. shape_version : string;
  2. provers : prover list;
  3. file : file;
}
val why3session_to_yojson : why3session -> Yojson.Safe.t
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 ref -> Xmlm.input -> unit
val extract_attributes : Xmlm.attribute list -> string MapString.t
val extract_cb : ('a -> 'b) -> 'b -> MapString.key -> 'a MapString.t -> 'b
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 ref -> Xmlm.input -> prover list
val extract_result : Xmlm.signal ref -> Xmlm.input -> result
val extract_proof : Xmlm.signal ref -> Xmlm.input -> proof
val extract_proofs : Xmlm.signal ref -> Xmlm.input -> proof list
val extract_goal : Xmlm.signal ref -> Xmlm.input -> goal
val extract_trans : Xmlm.signal ref -> Xmlm.input -> transf
val extract_goals : Xmlm.signal ref -> Xmlm.input -> goal list
val extract_theory : Xmlm.signal ref -> Xmlm.input -> theory
val extract_theories : Xmlm.signal ref -> Xmlm.input -> theory list
val to_whysession : in_channel -> why3session
type status =
  1. | Ssuccessful
  2. | Sfail of int
val status_to_yojson : status -> Yojson.Safe.t
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
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
type item = {
  1. id : string;
  2. kind : kind;
  3. formula : string option;
  4. res : res;
}
val item_to_yojson : item -> Yojson.Safe.t
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 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct