diff options
| author | Peter Sewell | 2018-07-27 18:57:02 +0100 |
|---|---|---|
| committer | Peter Sewell | 2018-07-27 18:57:02 +0100 |
| commit | 3755e6701a9286677fd2f4ca40a16305b360f9d9 (patch) | |
| tree | 67766e537db5bb8dbfc6b59432b2786a88b76be3 /src/interpreter.ml | |
| parent | 2a35c6b9e1cfac8ce34ef6fa7c264cfea4139002 (diff) | |
| parent | e4af7c3090c93a129e99dd75f2a20d5a9d2f6920 (diff) | |
Merge branch 'sail2' of github.com:rems-project/sail into sail2
Diffstat (limited to 'src/interpreter.ml')
| -rw-r--r-- | src/interpreter.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/interpreter.ml b/src/interpreter.ml index e4f7faf0..9a1d0ed2 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -135,7 +135,7 @@ let is_false = function | (E_aux (E_internal_value (V_bool b), _)) -> b == false | _ -> false -let exp_of_value v = (E_aux (E_internal_value v, (Parse_ast.Unknown, None))) +let exp_of_value v = (E_aux (E_internal_value v, (Parse_ast.Unknown, Type_check.empty_tannot))) let value_of_exp = function | (E_aux (E_internal_value v, _)) -> v | _ -> failwith "value_of_exp coerction failed" @@ -589,7 +589,6 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) = | LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id)) and pattern_match env (P_aux (p_aux, _) as pat) value = - (* print_endline ("Matching: " ^ string_of_pat pat ^ " with " ^ string_of_value value |> Util.yellow |> Util.clear); *) match p_aux with | P_lit lit -> eq_value (value_of_lit lit) value, Bindings.empty | P_wild -> true, Bindings.empty |