Module AltErgoLib.Ty

Types

This module defines the representation of types.

Definition

type tvar = Dolmen.Std.Expr.ty_var

Type of type variable.

module TvSet : Stdlib.Set.S with type elt = tvar
module TvMap : Stdlib.Map.S with type key = tvar
type t =
  1. | Tint
    (*

    Integer numbers

    *)
  2. | Treal
    (*

    Real numbers

    *)
  3. | Tbool
    (*

    Booleans

    *)
  4. | Tvar of tvar
    (*

    Type variables

    *)
  5. | Tbitv of int
    (*

    Bitvectors of a given length

    *)
  6. | Text of t list * Dolmen.Std.Expr.ty_cst
    (*

    Abstract types applied to arguments. Text (args, s) is the application of the abstract type constructor s to arguments args.

    *)
  7. | Tfarray of t * t
    (*

    Functional arrays. TFarray (src,dst) maps values of type src to values of type dst.

    *)
  8. | Tadt of Dolmen.Std.Expr.ty_cst * t list
    (*

    Application of algebraic data types. Tadt (a, params) denotes the application of the polymorphic datatype a to the types parameters params.

    For instance the type of integer lists can be represented by the value Tadt (Hstring.make "list", [Tint] where the identifier list denotes a polymorphic ADT defined by the user with t_adt.

    *)
type adt_constr = {
  1. constr : Dolmen.Std.Expr.term_cst;
    (*

    constructor of an ADT type

    *)
  2. destrs : (Dolmen.Std.Expr.term_cst * t) list;
    (*

    the list of destructors associated with the constructor and their respective types

    *)
}
type type_body = adt_constr list

Bodies of types definitions.

module Set : Stdlib.Set.S with type elt = t

Sets of types

val assoc_destrs : Dolmen.Std.Expr.term_cst -> adt_constr list -> (Dolmen.Std.Expr.term_cst * t) list

assoc_destrs cons cases returns the list of destructors associated with the constructor cons in the ADT defined by cases.

  • raises Not_found

    if the constructor is not in the given list.

val type_body : Dolmen.Std.Expr.ty_cst -> t list -> type_body

Type inspection

val hash : t -> int

Hash function

val equal : t -> t -> bool

Equality function

val compare : t -> t -> int

Comparison function

val pp_smtlib : Stdlib.Format.formatter -> t -> unit

Printing function for types in smtlib2 format.

val print : Stdlib.Format.formatter -> t -> unit

Printing function for types (does not print the type of each fields for records).

val print_list : Stdlib.Format.formatter -> t list -> unit

Print function for lists of types (does not print the type of each fields for records).

val print_full : Stdlib.Format.formatter -> t -> unit

Print function including the record fields.

val vty_of : t -> TvSet.t

Returns the set of type variables that occur in a given type.

Building types

val tunit : t

The unit type.

val fresh_tvar : unit -> t

Wrap the fresh_var function to return a type.

val fresh_empty_text : unit -> t

Return a fesh abstract type.

val text : t list -> Dolmen.Std.Expr.ty_cst -> t

Apply the abstract type constructor to the list of type arguments given.

val t_adt : ?body: (Dolmen.Std.Expr.term_cst * (Dolmen.Std.Expr.term_cst * t) list) list option -> Dolmen.Std.Expr.ty_cst -> t list -> t

Create an algebraic datatype. The body is a list of constructors, where each constructor is associated with the list of its destructors with their respective types. If body is none, then no definition will be registered for this type. The second argument is the name of the type. The third one provides its list of arguments.

Substitutions

type subst = t TvMap.t

The type of substitution, i.e. maps from type variables identifiers to types.

val compare_subst : subst -> subst -> int

Comparison of substitutions.

val equal_subst : subst -> subst -> bool

Equality of substitutions.

val print_subst : Stdlib.Format.formatter -> subst -> unit

Print function for substitutions.

val esubst : subst

The empty substitution, a.k.a. the identity.

val apply_subst : subst -> t -> t

Substitution application.

Matching

exception TypeClash of t * t

Exception raised during matching. TypeClash (u, v) is raised when u and v could not be matched (u and v may be sub-types of the types being actually matched).

val matching : subst -> t -> t -> subst

Matching of types (non-destructive). matching pat t returns a substitution subst such that apply_subst subst pat is equal to t.

type goal_sort =
  1. | Cut
    (*

    Introduce a cut in a goal. Once the cut proved, it's added as a hypothesis.

    *)
  2. | Check
    (*

    Check if some intermediate assertion is prouvable

    *)
  3. | Thm
    (*

    The goal to be proved valid

    *)
  4. | Sat
    (*

    The goal to be proved satisfiable

    *)

Goal sort. Used in typed declarations.

val fresh_hypothesis_name : goal_sort -> string

create a fresh hypothesis name given a goal sort.

val is_local_hyp : string -> bool

Assuming a name generated by fresh_hypothesis_name, answers whether the name design a local hypothesis ?

val is_global_hyp : string -> bool

Assuming a name generated by fresh_hypothesis_name, does the name design a global hypothesis ?

val print_goal_sort : Stdlib.Format.formatter -> goal_sort -> unit

Print a goal sort

val reinit_decls : unit -> unit

Empties the decls cache