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 prover_of_yojson : Yojson.Safe.t -> prover Ppx_deriving_yojson_runtime.error_or
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 result_of_yojson : Yojson.Safe.t -> result Ppx_deriving_yojson_runtime.error_or
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 proof_of_yojson : Yojson.Safe.t -> proof Ppx_deriving_yojson_runtime.error_or
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 goal_of_yojson : Yojson.Safe.t -> goal Ppx_deriving_yojson_runtime.error_or
val transf_to_yojson : transf -> Yojson.Safe.t
val transf_of_yojson : Yojson.Safe.t -> transf Ppx_deriving_yojson_runtime.error_or
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 theory_of_yojson : Yojson.Safe.t -> theory Ppx_deriving_yojson_runtime.error_or
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 file_of_yojson : Yojson.Safe.t -> file Ppx_deriving_yojson_runtime.error_or
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 why3session_of_yojson : Yojson.Safe.t -> why3session Ppx_deriving_yojson_runtime.error_or
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) -> '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 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 status_of_yojson : Yojson.Safe.t -> status Ppx_deriving_yojson_runtime.error_or
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 res_of_yojson : Yojson.Safe.t -> res Ppx_deriving_yojson_runtime.error_or
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 kind_of_yojson : Yojson.Safe.t -> kind Ppx_deriving_yojson_runtime.error_or
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 item_of_yojson : Yojson.Safe.t -> item Ppx_deriving_yojson_runtime.error_or
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 report_of_yojson : Yojson.Safe.t -> report Ppx_deriving_yojson_runtime.error_or
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
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