Lazy recursive values

[mattam82]

The current check implemented to verify that recursive bindings are correct is, I think, too simplistic. It currently only accepts immediate functions or lazy, already at parsing time: https://github.com/stedolan/malfunction/blob/4227093923bfa917565c5194c9ebd586415bdadf/src/malfunction_parser.ml#L110

According to https://v2.ocaml.org/manual/letrecvalues.html, many more programs can be accepted on the right hand-side of a let rec. This causes a problem in particular for our extraction from Coq, where a typical pattern of definition can be:

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

CoFixpoint ones : stream := 
  let x := bla in {| head := x; tail := ones |}.

This gets translated to (in pseudo malfunction syntax): let rec ones = let x = bla in lazy (Cons x ones)

and is rejected. As Coq supports a kind of "positive" view of coinductives, and only optionally, by user choice, co-pattern matching, some cofixpoint definitions in the wild might actually compute a few things before calling the constructor. Of course any cofixpoint with at least one argument will be fine as it starts with a lambda.

But currently malfunction will also reject let rec ones_list = 1 :: ones_list which is accepted by OCaml. Is there any rationale for this? As for our application in Coq, this does not matter as one cannot produce such cyclic values from Coq: every let rec has at least one argument, except for the images of cofixpoints, but then the body's head must be a constructor.