diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2017-11-20 18:43:31 +0100 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2017-11-22 11:14:46 +0100 |
| commit | 2db70092d63065be8a5902764e0d1d5f1ea01e6c (patch) | |
| tree | 478c124734b6444141378a1df22488f77b2102c7 /engine | |
| parent | 2a857da2a88855a6c9f0fa7e48a8700c1613e0c7 (diff) | |
Fix universe polymorphic Program obligations.
The universes of the obligations should all be non-algebraic as they
might appear in instances of other obligations and instances only take
non-algebraic universes as arguments.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/uState.ml | 3 | ||||
| -rw-r--r-- | engine/uState.mli | 5 |
2 files changed, 8 insertions, 0 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index dfea25dd0..01a479821 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -437,6 +437,9 @@ let make_flexible_variable ctx ~algebraic u = {ctx with uctx_univ_variables = uvars'; uctx_univ_algebraic = avars'} +let make_flexible_nonalgebraic ctx = + {ctx with uctx_univ_algebraic = Univ.LSet.empty} + let is_sort_variable uctx s = match s with | Sorts.Type u -> diff --git a/engine/uState.mli b/engine/uState.mli index b31e94b28..1c906fcb2 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -104,6 +104,11 @@ val add_global_univ : t -> Univ.Level.t -> t universe. Otherwise the variable is just made flexible. *) val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t +(** Turn all undefined flexible algebraic variables into simply flexible + ones. Can be used in case the variables might appear in universe instances + (typically for polymorphic program obligations). *) +val make_flexible_nonalgebraic : t -> t + val is_sort_variable : t -> Sorts.t -> Univ.Level.t option val normalize_variables : t -> Univ.universe_subst * t |