ITree.iter is not executable

I extract the semantics of Imp in your tutorial into ocaml code and use it to execute some simple Imp programs. It works well for usual programs. But for nonterminating programs, I got a stack-overflow. I read the extracted code and test the core functions used in the semantics one by one. I found a problem in the function ITree.iter from ITreeDefinition.v. Here is the extracted ocaml code.

type ('a, 'b) sum =
| Inl of 'a
| Inr of 'b

type ('e, 'r, 'itree) itreeF =
| RetF of 'r
| TauF of 'itree
| VisF of 'e * (__ -> 'itree)

type ('e, 'r) itree = ('e, 'r) __itree Lazy.t
and ('e, 'r) __itree =
| Go of ('e, 'r, ('e, 'r) itree) itreeF

(** val _observe :
    ('a1, 'a2) itree -> ('a1, 'a2, ('a1, 'a2) itree) itreeF **)

let _observe i =
  let Go _observe0 = Lazy.force i in _observe0

(** val observe :
    ('a1, 'a2) itree -> ('a1, 'a2, ('a1, 'a2) itree) itreeF **)

let observe =
  _observe

module ITree =
 struct
  (** val _bind :
      ('a2 -> ('a1, 'a3) itree) -> (('a1, 'a2) itree -> ('a1,
      'a3) itree) -> ('a1, 'a2, ('a1, 'a2) itree) itreeF ->
      ('a1, 'a3) itree **)

  let _bind k bind0 = function
  | RetF r -> k r
  | TauF t -> lazy (Go (TauF (bind0 t)))
  | VisF (e, h) ->
    lazy (Go (VisF (e, (fun x -> bind0 (h x)))))

  (** val bind' :
      ('a2 -> ('a1, 'a3) itree) -> ('a1, 'a2) itree -> ('a1,
      'a3) itree **)

  let rec bind' k t =
    _bind k (bind' k) (observe t)

  (** val _iter :
      (('a1, 'a2) itree -> ('a1, 'a2) itree) -> ('a3 -> ('a1,
      'a2) itree) -> ('a3, 'a2) sum -> ('a1, 'a2) itree **)

  let _iter tau iter_ = function
  | Inl i -> tau (iter_ i)
  | Inr r -> lazy (Go (RetF r))

  (** val iter :
      ('a3 -> ('a1, ('a3, 'a2) sum) itree) -> 'a3 -> ('a1,
      'a2) itree **)

  let rec iter step i =
    bind' (_iter (fun t -> lazy (Go (TauF t))) (iter step))
      (step i)
...

The extracted function iter got into an infinite loop when constructing infinite interaction trees. Ocaml evaluate the expression iter step i as follows (assume observe (step i) = RetF (Inl i)):

   iter step i
=> bind' (_iter (fun t -> lazy (Go (TauF t))) (iter step)) (step i)
=> _bind (_iter (fun t -> lazy (Go (TauF t))) (iter step)) (...) (RetF (Inl i))
=> _iter (fun t -> lazy (Go (TauF t))) (iter step) (Inl i)
=> (fun t -> lazy (Go (TauF t))) (iter step i)
=> ...

Because iter step i is not a lazy expression, Ocaml will evaluate it before applying function (fun t -> lazy (Go (TauF t))) on it, so a new iteration starts. It is obvious that the evaluation will never terminate because iter step i is exactly the origin expression, so a stack-overflow happens. It seems that the keyword "lazy" is put in the wrong place. So I modify the definition of function iter as follows:

  let _iter tau iter_ = function
  | Inl i -> lazy (tau (iter_ i))
  | Inr r -> lazy (Go (RetF r))

  let rec iter step i =
    bind' (_iter (fun t -> Go (TauF t)) (iter step))
      (step i)

It seems there is no diffference between the new definition and the original extracted function. However, this time the evaluation can terminate due to "lazy".

   iter step i
=> bind' (_iter (fun t -> Go (TauF t)) (iter step)) (step i)
=> _bind (_iter (fun t -> Go (TauF t)) (iter step)) (...) (RetF (Inl i))
=> _iter (fun t -> Go (TauF t)) (iter step) (Inl i)
=> lazy ((fun t -> Go (TauF t)) (lazy (iter step i)))
=> lazy (Go (TauF (lazy (iter step i))))

The new definition works well for constructing infinite interaction trees. However, the extracted semantics function eval_imp still cannot execute nonterminating programs. I guess there are other inexecutable functions in the libaray. I hope you can correct the definition of ITree.iter and other inexecutable functions in the source level so that the extracted code can be executable, though a lot more related definitions and proofs need modification.

DeepSpec / InteractionTrees

ITree.iter is not executable #182