package archetype

  1. Overview
  2. Docs

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