diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-03 20:02:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-03 23:39:01 +0200 |
| commit | 7002b3daca6da29eadf80019847630b8583c3daf (patch) | |
| tree | 9dcc3b618d33dd416805f70e878d71d007ddf4ff /kernel/univ.mli | |
| parent | 5de89439d459edd402328a1e437be4d8cd2e4f46 (diff) | |
Move to a representation of universe polymorphic constants using indices for variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 8f40bc5f8..655f87bb5 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -27,15 +27,14 @@ sig val equal : t -> t -> bool (** Equality function *) - (* val hash : t -> int *) - (** Hash function *) - val make : Names.DirPath.t -> int -> t (** Create a new universe level from a unique identifier and an associated module path. *) val pr : t -> Pp.std_ppcmds (** Pretty-printing *) + + val var : int -> t end type universe_level = Level.t @@ -370,11 +369,6 @@ val subst_univs_level_level : universe_level_subst -> universe_level -> universe val subst_univs_level_universe : universe_level_subst -> universe -> universe val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints -(** 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 empty_subst : universe_subst @@ -384,6 +378,21 @@ 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 +(** Substitution of instances *) +val subst_instance_instance : universe_instance -> universe_instance -> universe_instance +val subst_instance_universe : universe_instance -> universe -> universe +val subst_instance_constraints : universe_instance -> constraints -> constraints + +val make_instance_subst : universe_instance -> universe_level_subst +val make_inverse_instance_subst : universe_instance -> universe_level_subst + +val abstract_universes : bool -> universe_context -> universe_level_subst * universe_context + +(** Get the instantiated graph. *) +val instantiate_univ_context : universe_context -> universe_context + +val instantiate_univ_constraints : universe_instance -> universe_context -> constraints + (** {6 Pretty-printing of universes. } *) val pr_universes : universes -> Pp.std_ppcmds |