Fix the translation of cofix to fix

[mattam82]

This moves the head constructors's lazy of a cofixpoint definition to the toplevel of the fixpoint definition to avoid creating diverging functions in call-by-value semantics. See stedolan/malfunction#39 for an explanation of the problem with Coq's extraction which we mimicked.

[SkySkimmer]

What does this do on

CoInductive stream := Cons { head : nat; tail : stream }.

Definition mk n tail := {| head := n; tail := {| head := n; tail := tail |} |}.

CoFixpoint repeat n :=
  mk n (repeat n).

?

[stedolan]

I might be misreading this, but the change doesn't look correct to me. I think in the cases where remove_head_lazy fails to find a lazy to remove it should insert a force, e.g. to correctly compile the following:

CoFixpoint ones := {| head := 1; tail := ones |}.
CoFixpoint maybe_ones (b : bool) := if b then ones else {| head := 2; tail = maybe_ones b |}

maybe_ones should extract to:

let rec maybe_ones b = lazy (if b then force ones else lazy {head = 2; tail = maybe_ones b})

In general, the translation should be to wrap the entire body of a cofixpoint in lazy (force (...)), so that side-effects (i.e. nontermination) are delayed until the cofixpoint is inspected. force can then be pushed down, and if it reaches a lazy rewritten by force (lazy E) = E. If it doesn't reach a lazy, the force needs to remain present in the generated code.

[mattam82]

I might be misreading this, but the change doesn't look correct to me. I think in the cases where remove_head_lazy fails to find a lazy to remove it should insert a force, e.g. to correctly compile the following:

CoFixpoint ones := {| head := 1; tail := ones |}.
CoFixpoint maybe_ones (b : bool) := if b then ones else {| head := 2; tail = maybe_ones b |}

maybe_ones should extract to:

let rec maybe_ones b = lazy (if b then force ones else lazy {head = 2; tail = maybe_ones b})

Shouldn't it rather become:

let rec ones := lazy (Cons[(S[O]) ones]) 
let rec maybe_ones b = lazy (if b then force ones else {head = 2; tail = maybe_ones b})

(Note the else branch does not have another lazy in front)

In general, the translation should be to wrap the entire body of a cofixpoint in lazy (force (...)), so that side-effects (i.e. nontermination) are delayed until the cofixpoint is inspected. force can then be pushed down, and if it reaches a lazy rewritten by force (lazy E) = E. If it doesn't reach a lazy, the force needs to remain present in the generated code.

Yes, I agree.

I'll push the new code I have first, which also handles going under defined constants as the guard does and then correct it.

[mattam82]

I might be misreading this, but the change doesn't look correct to me. I think in the cases where remove_head_lazy fails to find a lazy to remove it should insert a force, e.g. to correctly compile the following:

CoFixpoint ones := {| head := 1; tail := ones |}.
CoFixpoint maybe_ones (b : bool) := if b then ones else {| head := 2; tail = maybe_ones b |}

maybe_ones should extract to:

let rec maybe_ones b = lazy (if b then force ones else lazy {head = 2; tail = maybe_ones b})

In general, the translation should be to wrap the entire body of a cofixpoint in lazy (force (...)), so that side-effects (i.e. nontermination) are delayed until the cofixpoint is inspected. force can then be pushed down, and if it reaches a lazy rewritten by force (lazy E) = E. If it doesn't reach a lazy, the force needs to remain present in the generated code.

With the latest definition in this branch I get:

Definition MetaCoq.TestSuite.erasure_live_test.maybe_ones.ones := let fix ones { struct 0 } := 
  lazy (Cons[(S[O]) ones]) in ones
Definition MetaCoq.TestSuite.erasure_live_test.maybe_ones.maybe_ones := let fix maybe_ones { struct 1 } := 
fun b => 
 lazy (match b with 
 | true => force MetaCoq.TestSuite.erasure_live_test.maybe_ones.ones
 | false => Cons[(S[(S[O])]) (maybe_ones b)]
  end)

Which looks fine to me! Indeed the general moto should be "Use a lazy (force to delay side effects to the time the fixpoint body is actually forced.