diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-18 22:55:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-19 01:23:54 +0200 |
| commit | e2e41c94f1f965e8c7d8bd4a93b58774821c2273 (patch) | |
| tree | a56b3021616cc46179bc994e52503b91ff82096f /checker/univ.mli | |
| parent | 0315a5d93c2de996f5c91bd2af827d3984ec1ad8 (diff) | |
Fixing the checker w.r.t. wrongly used abstract universe contexts.
It seems we were not testing the checker on cumulative inductive types,
because judging from the code, it would just have exploded in anomalies.
Before this patch, the checker was mixing De Bruijn indices with named
variables, resulting in ill-formed universe contexts used throughout the
checking of cumulative inductive types.
This patch also gets rid of a lot of now dead code, and removes abstraction
breaking code from the checker.
Diffstat (limited to 'checker/univ.mli')
| -rw-r--r-- | checker/univ.mli | 30 |
1 files changed, 4 insertions, 26 deletions
diff --git a/checker/univ.mli b/checker/univ.mli index 01df46fa1..7f5aa7626 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -18,6 +18,8 @@ sig (** Create a new universe level from a unique identifier and an associated module path. *) + val var : int -> t + val pr : t -> Pp.std_ppcmds (** Pretty-printing *) @@ -179,6 +181,8 @@ sig val length : t -> int (** Compute the length of the instance *) + val of_array : Level.t array -> t + val append : t -> t -> t (** Append two universe instances *) end @@ -208,7 +212,6 @@ module AUContext : sig type t - val instance : t -> Instance.t val size : t -> int val instantiate : Instance.t -> t -> Constraint.t @@ -218,27 +221,6 @@ end type abstract_universe_context = AUContext.t -module CumulativityInfo : -sig - type t - - val make : universe_context * universe_context -> t - - val empty : t - - val univ_context : t -> universe_context - val subtyp_context : t -> universe_context - - val from_universe_context : universe_context -> universe_instance -> t - - val subtyping_other_instance : t -> universe_instance - - val subtyping_susbst : t -> universe_level_subst - -end - -type cumulativity_info = CumulativityInfo.t - module ACumulativityInfo : sig type t @@ -284,10 +266,6 @@ val subst_instance_universe : universe_instance -> universe -> universe (* val make_instance_subst : universe_instance -> universe_level_subst *) (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *) -(** Get the instantiated graph. *) -val instantiate_univ_context : abstract_universe_context -> universe_context -val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info - (** Build the relative instance corresponding to the context *) val make_abstract_instance : abstract_universe_context -> universe_instance |