From 87628141d98e58453495cddd0917853dd1e689d9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 10 Jun 2014 17:58:29 +0200 Subject: Providing the checker with its own version of the Univ file. I also took the opportunity to remove a lot of code not used by the checker. --- checker/univ.mli | 220 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 220 insertions(+) create mode 100644 checker/univ.mli (limited to 'checker/univ.mli') diff --git a/checker/univ.mli b/checker/univ.mli new file mode 100644 index 000000000..31ed0404c --- /dev/null +++ b/checker/univ.mli @@ -0,0 +1,220 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* int -> t + (** Create a new universe level from a unique identifier and an associated + module path. *) + +end + +type universe_level = Level.t +(** Alias name. *) + +(** Sets of universe levels *) +module LSet : Set.S with type elt = universe_level + +type universe_set = LSet.t + +module Universe : +sig + type t + (** Type of universes. A universe is defined as a set of level expressions. + A level expression is built from levels and successors of level expressions, i.e.: + le ::= l + n, n \in N. + + A universe is said atomic if it consists of a single level expression with + no increment, and algebraic otherwise (think the least upper bound of a set of + level expressions). + *) + + val equal : t -> t -> bool + (** Equality function on formal universes *) + + val make : Level.t -> t + (** Create a universe representing the given level. *) + +end + +type universe = Universe.t + +(** Alias name. *) + +val pr_uni : universe -> Pp.std_ppcmds + +(** 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 *) +val type0m_univ : universe +val type0_univ : universe +val type1_univ : universe + +val is_type0_univ : universe -> bool +val is_type0m_univ : universe -> bool +val is_univ_variable : universe -> bool + +val sup : universe -> universe -> universe +val super : universe -> universe + +(** {6 Graphs of universes. } *) + +type universes + +type 'a check_function = universes -> 'a -> 'a -> bool +val check_leq : universe check_function +val check_eq : universe check_function + +(** The initial graph of universes: Prop < Set *) +val initial_universes : universes + +(** {6 Constraints. } *) + +type constraint_type = Lt | Le | Eq +type univ_constraint = universe_level * constraint_type * universe_level + +module Constraint : Set.S with type elt = univ_constraint + +type constraints = Constraint.t + +val empty_constraint : constraints + +(** A value with universe constraints. *) +type 'a constrained = 'a * constraints + +(** Enforcing constraints. *) + +type 'a constraint_function = 'a -> 'a -> constraints -> constraints + +val enforce_leq : universe constraint_function + +(** {6 ... } *) +(** Merge of constraints in a universes graph. + The function [merge_constraints] merges a set of constraints in a given + universes graph. It raises the exception [UniverseInconsistency] if the + constraints are not satisfiable. *) + +(** 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 + constraints... +*) +type explanation = (constraint_type * universe) list +type univ_inconsistency = constraint_type * universe * universe * explanation + +exception UniverseInconsistency of univ_inconsistency + +val merge_constraints : constraints -> universes -> universes + +val check_constraints : constraints -> universes -> bool + +(** {6 Support for old-style sort-polymorphism } *) + +val subst_large_constraints : + (universe * universe) list -> universe -> universe + +(** {6 Support for universe polymorphism } *) + +(** Polymorphic maps from universe levels to 'a *) +module LMap : Map.S with type key = universe_level + +type 'a universe_map = 'a LMap.t + +(** {6 Substitution} *) + +type universe_subst_fn = universe_level -> universe +type universe_level_subst_fn = universe_level -> universe_level + +(** A full substitution, might involve algebraic universes *) +type universe_subst = universe universe_map +type universe_level_subst = universe_level universe_map + +val level_subst_of : universe_subst_fn -> universe_level_subst_fn + +(** {6 Universe instances} *) + +module Instance : +sig + type t + (** A universe instance represents a vector of argument universes + to a polymorphic definition (constant, inductive or constructor). *) + + val empty : t + val is_empty : t -> bool + + val equal : t -> t -> bool + (** Equality (note: instances are hash-consed, this is O(1)) *) + + val subst_fn : universe_level_subst_fn -> t -> t + (** Substitution by a level-to-level function. *) + + val subst : universe_level_subst -> t -> t + (** Substitution by a level-to-level function. *) + + val pr : t -> Pp.std_ppcmds + (** Pretty-printing, no comments *) + + val check_eq : t check_function + (** Check equality of instances w.r.t. a universe graph *) +end + +type universe_instance = Instance.t + +type 'a puniverses = 'a * universe_instance + +(** A vector of universe levels with universe constraints, + representiong local universe variables and associated constraints *) + +module UContext : +sig + type t + + val empty : t + + val instance : t -> Instance.t + val constraints : t -> constraints + +end + +type universe_context = UContext.t + +val empty_level_subst : universe_level_subst +val is_empty_level_subst : universe_level_subst -> bool + +(** Substitution of universes. *) +val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level +val subst_univs_level_universe : universe_level_subst -> universe -> universe + +(** Make a universe level substitution: the instances must match. *) +val make_universe_subst : Instance.t -> universe_context -> universe_level_subst +(** Get the instantiated graph. *) +val instantiate_univ_context : universe_level_subst -> universe_context -> constraints + +(** Level to universe substitutions. *) + +val is_empty_subst : universe_subst -> bool +val make_subst : universe_subst -> universe_subst_fn + +val subst_univs_universe : universe_subst_fn -> universe -> universe +val subst_univs_constraints : universe_subst_fn -> constraints -> constraints + +(** {6 Pretty-printing of universes. } *) + +val pr_universes : universes -> Pp.std_ppcmds -- cgit v1.2.3