diff options
Diffstat (limited to 'src/lem_interp')
| -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)) |