diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-05 13:56:22 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-05 14:04:03 +0100 |
| commit | e849572cd2b242b34fbec6c3eaa42e7d2e7cc550 (patch) | |
| tree | 173fdd6bcb0d258985ffcdd125fcef0551dcb822 | |
| parent | c7026ec14f94875fc4b58951fa8bec628fcfac42 (diff) | |
Respect the transparent state of the current conversion on strong weak-head.
This fixes the previous patch in rare corner-cases where unification code was
relying on both kernel conversion and specific transparent state.
| -rw-r--r-- | kernel/cClosure.ml | 3 | ||||
| -rw-r--r-- | kernel/cClosure.mli | 3 | ||||
| -rw-r--r-- | kernel/reduction.ml | 2 |
3 files changed, 8 insertions, 0 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index b1181157e..4fd274ae1 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -91,6 +91,7 @@ module type RedFlagsSig = sig val red_add : reds -> red_kind -> reds val red_sub : reds -> red_kind -> reds val red_add_transparent : reds -> transparent_state -> reds + val red_transparent : reds -> transparent_state val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool val red_projection : reds -> projection -> bool @@ -164,6 +165,8 @@ module RedFlags = (struct let (l1,l2) = red.r_const in { red with r_const = Id.Pred.remove id l1, l2 } + let red_transparent red = red.r_const + let red_add_transparent red tr = { red with r_const = tr } diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 119b70e30..41db0af75 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -61,6 +61,9 @@ module type RedFlagsSig = sig (** Adds a reduction kind to a set *) val red_add_transparent : reds -> transparent_state -> reds + (** Retrieve the transparent state of the reduction flags *) + val red_transparent : reds -> transparent_state + (** Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds diff --git a/kernel/reduction.ml b/kernel/reduction.ml index a152a5c5f..6104f56c6 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -483,6 +483,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = Conversion check to rigid terms eventually implies full weak-head reduction, so instead of repeatedly performing small-step unfoldings, we perform reduction with all flags on. *) + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in let r1 = whd_stack (infos_with_reds infos all) def1 v1 in eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv | None -> @@ -499,6 +500,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (match unfold_reference infos fl2 with | Some def2 -> (** Symmetrical case of above. *) + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in let r2 = whd_stack (infos_with_reds infos all) def2 v2 in eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv | None -> |