diff options
| author | Peter Sewell | 2014-08-18 14:45:49 +0100 |
|---|---|---|
| committer | Peter Sewell | 2014-08-18 14:45:49 +0100 |
| commit | 21e83476d266fbd951d397ca3b58bf6385ab5f54 (patch) | |
| tree | baede2178ce710bae88c327f5e1d042de9f67600 /src | |
| parent | 8d24a0d871527e7f9e1d9c949ffb8ce5568d42e8 (diff) | |
make interp_exhaustive not take an interp_mode argument
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 4 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 2 |
2 files changed, 4 insertions, 2 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 4e4ca4ab..6ab8d41c 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -129,4 +129,6 @@ let rec ie_loop mode i_state = | Internal _ next -> (ie_loop mode next) end ;; -let interp_exhaustive mode i_state = ie_loop mode i_state +let interp_exhaustive i_state = + let mode = <| eager_eval = false; track_values = false |>in + ie_loop mode i_state diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index b1275d14..a7049633 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -71,7 +71,7 @@ val initial_instruction_state : context -> string -> list value -> instruction_s val interp : interp_mode -> instruction_state -> outcome (* Run the interpreter without external interaction, feeding in Unknown on all reads *) -val interp_exhaustive : interp_mode -> instruction_state -> list event +val interp_exhaustive : instruction_state -> list event (* As above, but will request register reads: outcome will only be rreg, done, or error *) val rr_interp_exhaustive : interp_mode -> instruction_state -> list event -> (outcome * (list event)) |