package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Archetype.Extract_wSource

Sourcemodule M = Model
Sourcemodule MapString : sig ... end
Sourcetype prover = {
  1. id : int;
  2. name : string;
  3. version : string;
  4. timelimit : int;
  5. steplimit : int;
  6. memlimit : int;
}
Sourceval prover_to_yojson : prover -> Yojson.Safe.t
Sourcetype result = {
  1. status : string;
  2. time : string;
  3. steps : int;
}
Sourceval result_to_yojson : result -> Yojson.Safe.t
Sourcetype proof = {
  1. prover_id : string;
  2. result : result;
}
Sourceval proof_to_yojson : proof -> Yojson.Safe.t
Sourcetype goal = {
  1. name : string;
  2. expl : string;
  3. proved : bool;
  4. proofs : proof list;
  5. transf : transf option;
}
Sourceand transf = {
  1. name : string;
  2. goals : goal list;
}
Sourceval goal_to_yojson : goal -> Yojson.Safe.t
Sourceval transf_to_yojson : transf -> Yojson.Safe.t
Sourcetype theory = {
  1. name : string;
  2. proved : bool;
  3. goals : goal list;
}
Sourceval theory_to_yojson : theory -> Yojson.Safe.t
Sourcetype file = {
  1. format : string;
  2. theory : theory list;
}
Sourceval file_to_yojson : file -> Yojson.Safe.t
Sourcetype why3session = {
  1. shape_version : string;
  2. provers : prover list;
  3. file : file;
}
Sourceval why3session_to_yojson : why3session -> Yojson.Safe.t
Sourceval mk_prover : int -> string -> string -> int -> int -> int -> prover
Sourceval mk_result : string -> string -> int -> result
Sourceval mk_proof : string -> result -> proof
Sourceval mk_goal : ?proofs:proof list -> ?transf:transf -> string -> string -> bool -> goal
Sourceval mk_transf : string -> goal list -> transf
Sourceval mk_theory : ?goals:goal list -> string -> bool -> theory
Sourceval mk_file : ?theory:theory list -> string -> file
Sourceval mk_why3session : ?provers:prover list -> string -> file -> why3session
Sourceval doit : Xmlm.signal -> unit
Sourceval is_tag : Tools.String.t -> [> `El_start of ('a * Tools.String.t) * 'b ] -> bool
Sourceval is_end : [> `El_end ] -> bool
Sourceval extract_attributes : Xmlm.attribute list -> string MapString.t
Sourceval extract_cb : ('a -> 'b) -> 'b -> MapString.key -> 'a MapString.t -> 'b
Sourceval extract_int : MapString.key -> string MapString.t -> int
Sourceval extract_bool : MapString.key -> string MapString.t -> bool
Sourceval extract_string : MapString.key -> string MapString.t -> string
Sourceval extract_prover : Xmlm.signal -> prover
Sourceval extract_provers : Xmlm.signal ref -> Xmlm.input -> prover list
Sourceval extract_result : Xmlm.signal ref -> Xmlm.input -> result
Sourceval extract_proof : Xmlm.signal ref -> Xmlm.input -> proof
Sourceval extract_proofs : Xmlm.signal ref -> Xmlm.input -> proof list
Sourceval extract_goal : Xmlm.signal ref -> Xmlm.input -> goal
Sourceval extract_trans : Xmlm.signal ref -> Xmlm.input -> transf
Sourceval extract_goals : Xmlm.signal ref -> Xmlm.input -> goal list
Sourceval extract_theory : Xmlm.signal ref -> Xmlm.input -> theory
Sourceval extract_theories : Xmlm.signal ref -> Xmlm.input -> theory list
Sourceval to_whysession : in_channel -> why3session
Sourcetype status =
  1. | Ssuccessful
  2. | Sfail of int
Sourceval status_to_yojson : status -> Yojson.Safe.t
Sourcetype res = {
  1. name : string;
  2. total : int;
  3. status : status;
}
Sourceval res_to_yojson : res -> Yojson.Safe.t
Sourcetype 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
Sourceval kind_to_yojson : kind -> Yojson.Safe.t
Sourcetype item = {
  1. id : string;
  2. kind : kind;
  3. formula : string option;
  4. res : res;
}
Sourceval item_to_yojson : item -> Yojson.Safe.t
Sourcetype report = {
  1. name : string;
  2. items : item list;
}
Sourceval report_to_yojson : report -> Yojson.Safe.t
Sourceval _ : Yojson.Safe.t -> report Ppx_deriving_yojson_runtime.error_or
Sourceval mk_res : string -> int -> status -> res
Sourceval mk_item : string -> kind -> string option -> res -> item
Sourceval mk_report : ?items:item list -> string -> report
Sourceval extract : M.model -> why3session -> report
Sourceval 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