package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module UnivSource

Sourcemodule Level : sig ... end

Universes.

Sourcemodule LSet : sig ... end

Sets of universe levels

Sourcemodule Universe : sig ... end

Alias name.

Sourceval pr_uni : Universe.t -> Pp.t
Sourceval type0m_univ : Universe.t

The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0

Sourceval type0_univ : Universe.t
Sourceval type1_univ : Universe.t
Sourceval is_type0_univ : Universe.t -> bool
Sourceval is_type0m_univ : Universe.t -> bool
Sourceval is_univ_variable : Universe.t -> bool
Sourceval is_small_univ : Universe.t -> bool
Sourceval universe_level : Universe.t -> Level.t option

univ_level_mem l u Is l is mentioned in u ?

Sourceval univ_level_mem : Level.t -> Universe.t -> bool

univ_level_rem u v min removes u from v, resulting in min if v was exactly u.

Sourceval univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t
Constraints.
Sourcetype constraint_type = AcyclicGraph.constraint_type =
  1. | Lt
  2. | Le
  3. | Eq
Sourcetype univ_constraint = Level.t * constraint_type * Level.t
Sourcemodule Constraint : sig ... end
Sourceval empty_constraint : Constraint.t
Sourceval union_constraint : Constraint.t -> Constraint.t -> Constraint.t
Sourceval eq_constraint : Constraint.t -> Constraint.t -> bool
Sourcetype 'a constrained = 'a * Constraint.t

A value with universe Constraint.t.

Sourceval constraints_of : 'a constrained -> Constraint.t

Constrained

Sourcetype 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t

Enforcing Constraint.t.

Sourceval enforce_eq_level : Level.t constraint_function
Sourceval enforce_leq_level : Level.t constraint_function
Sourcetype explanation = (constraint_type * Level.t) list

Type explanation is used to decorate error messages to provide useful explanation why a given constraint is rejected. It is composed of a path of universes and relation kinds (r1,u1);..;(rn,un) means .. <(r1) u1 <(r2) ... <(rn) un (where <(ri) is the relation symbol denoted by ri, currently only < and <=). The lowest end of the chain is supposed known (see UniverseInconsistency exn). The upper end may differ from the second univ of UniverseInconsistency because all universes in the path are canonical. Note that each step does not necessarily correspond to an actual constraint, but reflect how the system stores the graph and may result from combination of several Constraint.t...

Sourcetype univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Lazy.t option
Sourceexception UniverseInconsistency of univ_inconsistency
Support for universe polymorphism
Sourcemodule LMap : sig ... end

Polymorphic maps from universe levels to 'a

Sourcetype 'a universe_map = 'a LMap.t
Substitution
Sourcetype universe_subst_fn = Level.t -> Universe.t
Sourcetype universe_level_subst_fn = Level.t -> Level.t
Sourcetype universe_subst = Universe.t universe_map

A full substitution, might involve algebraic universes

Sourcetype universe_level_subst = Level.t universe_map
Sourcemodule Variance : sig ... end
Universe instances
Sourcemodule Instance : sig ... end
Sourceval enforce_eq_instances : Instance.t constraint_function
Sourceval enforce_eq_variance_instances : Variance.t array -> Instance.t constraint_function
Sourceval enforce_leq_variance_instances : Variance.t array -> Instance.t constraint_function
Sourcetype 'a puniverses = 'a * Instance.t
Sourceval out_punivs : 'a puniverses -> 'a
Sourceval in_punivs : 'a -> 'a puniverses
Sourceval eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool

A vector of universe levels with universe Constraint.t, representing local universe variables and associated Constraint.t

Sourcemodule UContext : sig ... end
Sourcemodule AUContext : sig ... end
Sourcetype 'a univ_abstracted = {
  1. univ_abstracted_value : 'a;
  2. univ_abstracted_binder : AUContext.t;
}

A value with bound universe levels.

Sourceval map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted

Universe contexts (as sets)

A set of universes with universe Constraint.t. We linearize the set to a list after typechecking. Beware, representation could change.

Sourcemodule ContextSet : sig ... end
Sourcetype 'a in_universe_context = 'a * UContext.t

A value in a universe context (resp. context set).

Sourcetype 'a in_universe_context_set = 'a * ContextSet.t
Sourceval empty_level_subst : universe_level_subst
Sourceval is_empty_level_subst : universe_level_subst -> bool
Sourceval subst_univs_level_level : universe_level_subst -> Level.t -> Level.t

Substitution of universes.

Sourceval subst_univs_level_universe : universe_level_subst -> Universe.t -> Universe.t
Sourceval subst_univs_level_constraints : universe_level_subst -> Constraint.t -> Constraint.t
Sourceval subst_univs_level_abstract_universe_context : universe_level_subst -> AUContext.t -> AUContext.t
Sourceval subst_univs_level_instance : universe_level_subst -> Instance.t -> Instance.t

Level to universe substitutions.

Sourceval subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t

Only user in the kernel is template polymorphism. Ideally we get rid of this code if it goes away.

Sourceval subst_instance_instance : Instance.t -> Instance.t -> Instance.t

Substitution of instances

Sourceval subst_instance_universe : Instance.t -> Universe.t -> Universe.t
Sourceval make_instance_subst : Instance.t -> universe_level_subst

Creates u(0) ↦ 0; ...; u(n-1) ↦ n - 1 out of u(0); ...; u(n - 1)

Sourceval make_inverse_instance_subst : Instance.t -> universe_level_subst
Sourceval abstract_universes : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t

TODO: move universe abstraction out of the kernel

Sourceval make_abstract_instance : AUContext.t -> Instance.t
Sourceval compact_univ : Universe.t -> Universe.t * int list

compact_univ u remaps local variables in u such that their indices become consecutive. It returns the new universe and the mapping. Example: compact_univ (Var 0, i); (Prop, 0); (Var 2; j)) = (Var 0,i); (Prop, 0); (Var 1; j), 0; 2

Pretty-printing of universes.
Sourceval pr_constraint_type : constraint_type -> Pp.t
Sourceval pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t
Sourceval pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> UContext.t -> Pp.t
Sourceval pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> AUContext.t -> Pp.t
Sourceval pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
Sourceval explain_universe_inconsistency : (Level.t -> Pp.t) -> univ_inconsistency -> Pp.t
Sourceval pr_universe_level_subst : universe_level_subst -> Pp.t
Sourceval pr_universe_subst : universe_subst -> Pp.t
Hash-consing
Sourceval hcons_univ : Universe.t -> Universe.t
Sourceval hcons_constraints : Constraint.t -> Constraint.t
Sourceval hcons_universe_set : LSet.t -> LSet.t
Sourceval hcons_universe_context : UContext.t -> UContext.t
Sourceval hcons_abstract_universe_context : AUContext.t -> AUContext.t
Sourceval hcons_universe_context_set : ContextSet.t -> ContextSet.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct