# Coinductition fun times

## unsound1 test

* `!X: C1orC2`
* `X: C1orC2 if X: C1`
* `X: C1 if X: C2, X: C3`
* `X: C2 if X: C1`
* `X: C1` -- inductive cycle
* I believe today this gets cached, let's look into that
* `X: C3 if X: C3`
* failure
* `X: C1orC2 if X: C2`
* succeeds because of (incorrect) cache

### current state

* goal at depth 0, dfn 0: `!X: C1orC2`
* clause: `!X: C1orC2 if !X: C1`
* goal at depth 1, dfn 1: `!X: C1`
* clause: `!X: C1 if !X: C2, !X: C3`
* goal at depth 2, dfn 2: `!X: C2`
* clause: `!X: C2 if !X: C1`
* goal at depth 3: `!X: C1` -- inductive cycle
* result: Ok([]), with minimum 1
* result: Ok, with minimum 1, no cache
* goal at depth 2, dfn 3: `X: C3`
* result: Err(NoSolution), minimum INT_MAX
* result: Err(NoSolution), minimum 1

### Solution0

[description](https://github.com/rust-lang/chalk/issues/399#issuecomment-643420016)

* goal at depth 0, dfn 0: `!X: C1orC2`
* clause: `!X: C1orC2 if !X: C1`
* goal at depth 1, dfn 1: `!X: C1`
* iteration 0, intermediate result is `Ok`
* clause: `!X: C1 if !X: C2, !X: C3`
* goal at depth 2, dfn 2: `!X: C2`
* clause: `!X: C2 if !X: C1`
* goal at depth 3: `!X: C1`
* result: Ok([]), with minimum 1
* result: Ok, with minimum 1, no cache
* goal at depth 2, dfn 3: `X: C3`
* result: Err(NoSolution), minimum INT_MAX
* result: Err(NoSolution), minimum 1o
* iteration 1, intermediate result is `Err`
* clause: `!X: C1 if !X: C2, !X: C3`
* goal at depth 2, dfn 2: `!X: C2`
* clause: `!X: C2 if !X: C1`
* goal at depth 3: `!X: C1`
* result: Err, with minimum 1
* result: Err, with minimum 1, no cache
* goal at depth 2, dfn 3: `X: C3`
* result: Err(NoSolution), minimum INT_MAX
* result: Err(NoSolution), minimum 1o
* fixed point reached, we cache the following results:
* `X: C1` => error
* `X: C2` => error
* `X: C3` => error

XXX have to work out mixed cycles

## inner cycle test

[link](https://github.com/rust-lang/chalk/blob/3df6b429cbd801c5b4bf4b4ecc30732f59cba07a/tests/test/coinduction.rs#L433-L501)

C1andC2 :- C1, C2.
C1 :- C3.
C2 :- C5, C1.
C3 :- C4.
C3 :- C5.
C4 :- C1.
C5 :- C6.
C6 :- C2, C7.

graph TD
  C1andC2-->C1;
  C1andC2-->C2;
  C1-->C3;
  C3-.->C5;
  C3-.->C4;
  C4-->C1;
  C5-->C6;
  C2-->C5;
  C2-->C1;
  C6-->C7;
  C6-->C2;

* goal at depth 0, dfn 0: `C1andC2`
* clause: `C1andC2 :- C1, C2`
* goal at depth 1, dfn 1: `C1`
* clause: `C1 :- C3`
* iteration 0:
* goal at depth 2, dfn 2: `C3`
* clause: `C3 :- C5`
* goal at depth 3, dfn 3: `C5`
* iteration 0, result is Ok:
* clause: `C5 :- C6`
* goal at depth 4, dfn 4: `C6`
* clause: `C6 :- C2, C7`
* goal at depth 5, dfn 5: `C2`
* clause: `C2 :- C5, C1`
* goal at depth 6, dfn 6: `C5`
* cycle, coindutive
* result Ok, minimum 3, uncached
* goal at depth 6, dfn 7: `C1`
* cycle, coindutive
* result Ok, minimum 1, uncached
* result Ok, minimum 1, uncached
* goal at depth 5, dfn 8: `C7`
* no applicable clauses
* result: Error, **cached:**
* `C7 => error`
* result: Error, minimum 1, uncached
* iteration 0, result is Error:
* clause: `C5 :- C6`
* goal at depth 4, dfn 4: `C6`
* clause: `C6 :- C2, C7`
* goal at depth 5, dfn 5: `C2`
* clause: `C2 :- C5, C1`
* goal at depth 6, dfn 6: `C5`
* cycle, coindutive
* result Error, minimum 3, uncached
* result: Error, minimum 3, **cached from dfn 3:**
* `C5 => error` (dfn 3)
* `C6 => error` (dfn 4)
* `C2 => error` (dfn 5)
* clause: `C3 :- C4`
* goal at depth 3, dfn 3: `C4`
* clause: `C4 :- C1`
* goal: `C1`
* inductive cycle
* result Ok, minimum 1, uncached
* result: Ok, minimum 1, **cached from dfn 1:**
* `C1 => Ok` (dfn 1)
* `C3 => Ok` (dfn 2)
* `C4 => Ok` (dfn 3)
* goal at depth 1, dfn 1: `C2`
* cached: Error
* result: Error, **cached**:
* `C1andC2 => Error`

Final cache:

* `C1 => Ok`
* `C2 => error`
* `C3 => Ok`
* `C4 => Ok`
* `C5 => error`
* `C6 => error`
* `C7 => error`
* `C1andC2 => Error`

Question:

* Is it important to go all the way through to find the lowest minimum?