archetype 1.2.12 · OCaml Package

module M = Model

module MapString : sig ... end

type prover = {

id : int;
name : string;
version : string;
timelimit : int;
steplimit : int;
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 = {

status : string;
time : string;
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 = {

prover_id : string;
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

val show_proof : proof -> Ppx_deriving_runtime.string

type goal = {

name : string;
expl : string;
proved : bool;
proofs : proof list;
transf : transf option;

}

and transf = {

name : string;
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 show_goal : goal -> Ppx_deriving_runtime.string

val pp_transf : 
  Ppx_deriving_runtime.Format.formatter ->
  transf ->
  Ppx_deriving_runtime.unit

val show_transf : transf -> Ppx_deriving_runtime.string

type theory = {

name : string;
proved : bool;
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 = {

format : string;
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

val show_file : file -> Ppx_deriving_runtime.string

type why3session = {

shape_version : string;
provers : prover list;
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 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 =

| Ssuccessful
| 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 = {

name : string;
total : int;
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

val show_res : res -> Ppx_deriving_runtime.string

type kind =

| Kvariable of string
| Kasset of string
| KassetField of string * string
| KenumField of string * string
| KentryPostcond of string * string
| 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

val show_kind : kind -> Ppx_deriving_runtime.string

type item = {

id : string;
kind : kind;
formula : string option;
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

val show_item : item -> Ppx_deriving_runtime.string

type report = {

name : string;
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

package archetype