Represent external worlds by a coinductive type rather than an inductive type.

As noticed by R. Krebbers, an inductive type for external worlds implies that all sequences of program-world interactions are finite, which is not the case.

Author: xavierleroy

common/Determinism.v

@@ -36,7 +36,7 @@ Require Import Behaviors.
   that this external call succeeds, has result [r], and changes
   the world to [w]. *)
 
-Inductive world: Type :=
+CoInductive world: Type :=
   World (io: ident -> list eventval -> option (eventval * world))
         (vload: memory_chunk -> ident -> int -> option (eventval * world))
         (vstore: memory_chunk -> ident -> int -> eventval -> option world).

driver/Interp.ml

@@ -402,7 +402,7 @@ let do_inline_assembly txt sg ge w args m = None
 (* Implementing external functions producing observable events *)
 
 let rec world ge m =
-  Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m)
+  lazy (Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m))
 
 and world_io ge m id args =
   None