diff options
| -rw-r--r-- | common/Determinism.v | 2 | ||||
| -rw-r--r-- | driver/Interp.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/common/Determinism.v b/common/Determinism.v index d0099ba9..7ea19663 100644 --- a/common/Determinism.v +++ b/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). diff --git a/driver/Interp.ml b/driver/Interp.ml index b16d2cae..f453af95 100644 --- a/driver/Interp.ml +++ b/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 |