Previous  Up  Next

Module Pdecl

module Pdecl: sig .. end

WhyML program declarations

Type declarations

type its_defn = private {
   itd_its : Ity.itysymbol;
   itd_fields : Expr.rsymbol list;
   itd_constructors : Expr.rsymbol list;
   itd_invariant : Term.term list; (*

The expression is a tuple where each elements corresponds to a field

*)
   itd_witness : Expr.expr option;
} 
val create_plain_record_decl : priv:bool ->
       mut:bool ->
       Ident.preid ->
       Ty.tvsymbol list ->
       (bool * Ity.pvsymbol) list ->
       Term.term list -> Expr.expr option -> its_defn

create_plain_record_decl ~priv ~mut id args fields invl witn creates a declaration for a non-recursive record type, possibly private and/or mutable. The known record fields are listed with their mutability status. The priv flag should be set to true for private records. The mut flag should be set to true to mark the new type as mutable even if it has no known mutable fields. This is the case for private mutable records with no known mutable fields, as well as for non-private records that have an invariant: marking such a type as mutable gives every value of this type a distinct identity, allowing us to track values with broken invariants. The invl parameter contains the list of invariant formulas that may only depend on free variables from fields. If the type is private, then every field occurring in invl must have an immutable type. The witn parameter provides an expression which computes a tuple that gives a witness for each field of a plain record type (can be None if there is no user witness). Abstract types are considered to be private records with no fields.

val create_rec_record_decl : Ity.itysymbol -> Ity.pvsymbol list -> its_defn

create_rec_record_decl its fields creates a declaration for a recursive record type. The type symbol should be created using Ity.create_itysymbol_rec. All fields must be immutable.

val create_plain_variant_decl : Ident.preid ->
       Ty.tvsymbol list ->
       (Ident.preid * (bool * Ity.pvsymbol) list) list -> its_defn

create_plain_variant_decl id args constructors creates a declaration for a non-recursive algebraic type. Each constructor field carries a Boolean flag denoting whether a projection function should be generated for this field. Any such field must be present in each constructor, so that the projection function is total.

val create_rec_variant_decl : Ity.itysymbol ->
       (Ident.preid * (bool * Ity.pvsymbol) list) list -> its_defn

create_rec_variant_decl id args constructors creates a declaration for a recursive algebraic type. The type symbol should be created using Ity.create_itysymbol_rec. Each constructor field carries a Boolean flag denoting whether a projection function should be generated for this field. Any such field must be present in each constructor, so that the projection function is total. All fields must be immutable.

val create_alias_decl : Ident.preid -> Ty.tvsymbol list -> Ity.ity -> its_defn

create_alias_decl id args def creates a new alias type declaration.

val create_range_decl : Ident.preid -> Number.int_range -> its_defn

create_range_decl id ir creates a new range type declaration.

val create_float_decl : Ident.preid -> Number.float_format -> its_defn

create_float_decl id fp creates a new float type declaration.

Module declarations

type pdecl = private {
   pd_node : pdecl_node;
   pd_pure : Decl.decl list;
   pd_meta : meta_decl list;
   pd_syms : Ident.Sid.t;
   pd_news : Ident.Sid.t;
   pd_tag : int;
} 
type pdecl_node = private
| PDtype of its_defn list
| PDlet of Expr.let_defn
| PDexn of Ity.xsymbol
| PDpure 
type meta_decl = Theory.meta * Theory.meta_arg list 
val axiom_of_invariant : its_defn -> Term.term

axiom_of_invariant itd returns a closed formula that postulates the type invariant of itd for all values of the type

val meta_depends : Theory.meta
val create_type_decl : its_defn list -> pdecl list
val create_let_decl : Expr.let_defn -> pdecl
val create_exn_decl : Ity.xsymbol -> pdecl
val create_pure_decl : Decl.decl -> pdecl

Built-in decls

val pd_int : pdecl
val pd_real : pdecl
val pd_equ : pdecl
val pd_ignore_term : pdecl
val pd_bool : pdecl
val pd_str : pdecl
val pd_tuple : int -> pdecl
val pd_func : pdecl
val pd_func_app : pdecl

Known identifiers

type known_map = pdecl Ident.Mid.t 
val known_id : known_map -> Ident.ident -> unit
val known_add_decl : known_map -> pdecl -> known_map
val merge_known : known_map -> known_map -> known_map
val find_its_defn : known_map -> Ity.itysymbol -> its_defn

Pretty-printing

val print_pdecl : Stdlib.Format.formatter -> pdecl -> unit