Frama-C:
Plug-ins:
Libraries:

Frama-C API - Polymorphic

Functor for polymorphic types with only 1 type variable.

  • before 26.0-Iron

    the functor had several additional values only used for Journalization that has been removed.

  • before 33.0-Arsenic

    the function names in the input module P were prefixed by mk_.

Parameters

module P : sig ... end

Signature

include Type.Polymorphic with type 'a poly = 'a P.t
type 'a poly = 'a P.t

Type of the polymorphic type (for instance 'a list). It must be instantiated before used. See function instantiate below.

val instantiate : 'a Type.t -> 'a poly Type.t * bool
  • returns

    the monomorphic instantiation of the polymorph type with the given type value. For instance, if 'a poly = 'a list, then instantiate int returns the type value int list.

val is_instance_of : 'a Type.t -> bool
  • returns

    true iff the given type value has been created from function instantiate above. For instance, is_instance_of (instantiate int) always returns true but is_instance_of int always returns false.

val get_instance : 'a poly Type.t -> 'a Type.t

get_instance ty returns the type value used to create the given monomorphic instantiation.

module Make (T : S) : S with type t = T.t poly

Create a datatype for a monomorphic instance of the polymorphic type.