@@ -138,6 +138,8 @@ pub enum PathKind {
138138 Unknown ,
139139 /// A path with at least one coinductive step. Such cycles hold.
140140 Coinductive ,
141+ /// A path which is treated as ambiguous.
142+ ForcedAmbiguity ,
141143}
142144
143145impl PathKind {
@@ -150,6 +152,9 @@ impl PathKind {
150152 /// to `max(self, rest)`.
151153 fn extend ( self , rest : PathKind ) -> PathKind {
152154 match ( self , rest) {
155+ ( PathKind :: ForcedAmbiguity , _) | ( _, PathKind :: ForcedAmbiguity ) => {
156+ PathKind :: ForcedAmbiguity
157+ }
153158 ( PathKind :: Coinductive , _) | ( _, PathKind :: Coinductive ) => PathKind :: Coinductive ,
154159 ( PathKind :: Unknown , _) | ( _, PathKind :: Unknown ) => PathKind :: Unknown ,
155160 ( PathKind :: Inductive , PathKind :: Inductive ) => PathKind :: Inductive ,
@@ -321,7 +326,10 @@ impl CycleHeads {
321326
322327 let path_from_entry = match step_kind {
323328 PathKind :: Coinductive => AllPathsToHeadCoinductive :: Yes ,
324- PathKind :: Unknown | PathKind :: Inductive => path_from_entry,
329+ // TODO
330+ PathKind :: Unknown | PathKind :: Inductive | PathKind :: ForcedAmbiguity => {
331+ path_from_entry
332+ }
325333 } ;
326334
327335 self . insert ( head, path_from_entry) ;
@@ -348,6 +356,7 @@ bitflags::bitflags! {
348356 const INDUCTIVE = 1 << 1 ;
349357 const UNKNOWN = 1 << 2 ;
350358 const COINDUCTIVE = 1 << 3 ;
359+ const FORCED_AMBIGUITY = 1 << 4 ;
351360 }
352361}
353362impl From < PathKind > for PathsToNested {
@@ -356,6 +365,7 @@ impl From<PathKind> for PathsToNested {
356365 PathKind :: Inductive => PathsToNested :: INDUCTIVE ,
357366 PathKind :: Unknown => PathsToNested :: UNKNOWN ,
358367 PathKind :: Coinductive => PathsToNested :: COINDUCTIVE ,
368+ PathKind :: ForcedAmbiguity => PathsToNested :: FORCED_AMBIGUITY ,
359369 }
360370 }
361371}
@@ -388,6 +398,22 @@ impl PathsToNested {
388398 self . insert ( PathsToNested :: COINDUCTIVE ) ;
389399 }
390400 }
401+ PathKind :: ForcedAmbiguity => {
402+ if self . intersects (
403+ PathsToNested :: EMPTY
404+ | PathsToNested :: INDUCTIVE
405+ | PathsToNested :: UNKNOWN
406+ | PathsToNested :: COINDUCTIVE ,
407+ ) {
408+ self . remove (
409+ PathsToNested :: EMPTY
410+ | PathsToNested :: INDUCTIVE
411+ | PathsToNested :: UNKNOWN
412+ | PathsToNested :: COINDUCTIVE ,
413+ ) ;
414+ self . insert ( PathsToNested :: FORCED_AMBIGUITY ) ;
415+ }
416+ }
391417 }
392418
393419 self
0 commit comments