why3 1.3.2 · OCaml Package

type constructor = Term.lsymbol * Term.lsymbol option list

type data_decl = Ty.tysymbol * constructor list

type ls_defn

type logic_decl = Term.lsymbol * ls_defn

val make_ls_defn : Term.lsymbol -> Term.vsymbol list -> Term.term -> logic_decl

val open_ls_defn : ls_defn -> Term.vsymbol list * Term.term

val open_ls_defn_cb : 
  ls_defn ->
  Term.vsymbol list
  * Term.term
  * (Term.lsymbol ->
  Term.vsymbol list ->
  Term.term ->
  logic_decl)

val ls_defn_axiom : ls_defn -> Term.term

val ls_defn_of_axiom : Term.term -> logic_decl option

val ls_defn_decrease : ls_defn -> int list

type call_set

type vs_graph

val create_call_set : unit -> call_set

val create_vs_graph : Term.vsymbol list -> vs_graph

val register_call : 
  call_set ->
  Ident.ident ->
  vs_graph ->
  Ident.ident ->
  Term.term list ->
  unit

val vs_graph_drop : vs_graph -> Term.vsymbol -> vs_graph

val vs_graph_let : vs_graph -> Term.term -> Term.vsymbol -> vs_graph

val vs_graph_pat : vs_graph -> Term.term -> Term.pattern -> vs_graph

val find_variant : exn -> call_set -> Ident.ident -> int list

type prsymbol = private {

pr_name : Ident.ident;

}

module Mpr : sig ... end

module Spr : sig ... end

module Hpr : sig ... end

module Wpr : sig ... end

val create_prsymbol : Ident.preid -> prsymbol

val pr_equal : prsymbol -> prsymbol -> bool

val pr_hash : prsymbol -> int

type ind_decl = Term.lsymbol * (prsymbol * Term.term) list

type ind_sign =

| Ind
| Coind

type ind_list = ind_sign * ind_decl list

type prop_kind =

| Plemma
| Paxiom
| Pgoal

type prop_decl = prop_kind * prsymbol * Term.term

type decl = private {

d_node : decl_node;
d_news : Ident.Sid.t;
d_tag : Weakhtbl.tag;

}

and decl_node = private

| Dtype of Ty.tysymbol
| Ddata of data_decl list
| Dparam of Term.lsymbol
| Dlogic of logic_decl list
| Dind of ind_list
| Dprop of prop_decl

module Mdecl : sig ... end

module Sdecl : sig ... end

module Wdecl : sig ... end

module Hdecl : sig ... end

val d_equal : decl -> decl -> bool

val d_hash : decl -> int

val create_ty_decl : Ty.tysymbol -> decl

val create_data_decl : data_decl list -> decl

val create_param_decl : Term.lsymbol -> decl

val create_logic_decl : logic_decl list -> decl

val create_ind_decl : ind_sign -> ind_decl list -> decl

val create_prop_decl : prop_kind -> prsymbol -> Term.term -> decl

val get_decl_syms : decl -> Ident.Sid.t

exception IllegalTypeAlias of Ty.tysymbol

exception NonPositiveTypeDecl of Ty.tysymbol * Term.lsymbol * Ty.ty

exception InvalidIndDecl of Term.lsymbol * prsymbol

exception NonPositiveIndDecl of Term.lsymbol * prsymbol * Term.lsymbol

exception NoTerminationProof of Term.lsymbol

exception BadLogicDecl of Term.lsymbol * Term.lsymbol

exception UnboundVar of Term.vsymbol

exception ClashIdent of Ident.ident

exception EmptyDecl

exception EmptyAlgDecl of Ty.tysymbol

exception EmptyIndDecl of Term.lsymbol

exception BadConstructor of Term.lsymbol

exception BadRecordField of Term.lsymbol

exception BadRecordCons of Term.lsymbol * Ty.tysymbol

exception BadRecordType of Term.lsymbol * Ty.tysymbol

exception BadRecordUnnamed of Term.lsymbol * Ty.tysymbol

exception RecordFieldMissing of Term.lsymbol

exception DuplicateRecordField of Term.lsymbol

val decl_map : (Term.term -> Term.term) -> decl -> decl

val decl_fold : ('a -> Term.term -> 'a) -> 'a -> decl -> 'a

val decl_map_fold : 
  ('a -> Term.term -> 'a * Term.term) ->
  'a ->
  decl ->
  'a * decl

module DeclTF : sig ... end

type known_map = decl Ident.Mid.t

val known_id : known_map -> Ident.ident -> unit

val known_add_decl : known_map -> decl -> known_map

val merge_known : known_map -> known_map -> known_map

exception KnownIdent of Ident.ident

exception UnknownIdent of Ident.ident

exception RedeclaredIdent of Ident.ident

exception NonFoundedTypeDecl of Ty.tysymbol

val find_constructors : known_map -> Ty.tysymbol -> constructor list

val find_inductive_cases : 
  known_map ->
  Term.lsymbol ->
  (prsymbol * Term.term) list

val find_logic_definition : known_map -> Term.lsymbol -> ls_defn option

val find_prop : known_map -> prsymbol -> Term.term

val find_prop_decl : known_map -> prsymbol -> prop_kind * Term.term

exception EmptyRecord

val parse_record : 
  known_map ->
  (Term.lsymbol * 'a) list ->
  Term.lsymbol * Term.lsymbol list * 'a Term.Mls.t

val make_record : 
  known_map ->
  (Term.lsymbol * Term.term) list ->
  Ty.ty ->
  Term.term

val make_record_update : 
  known_map ->
  Term.term ->
  (Term.lsymbol * Term.term) list ->
  Ty.ty ->
  Term.term

val make_record_pattern : 
  known_map ->
  (Term.lsymbol * Term.pattern) list ->
  Ty.ty ->
  Term.pattern

package why3