summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKathy Gray2015-06-29 18:51:34 +0100
committerKathy Gray2015-06-29 18:51:34 +0100
commit01100e146e5c6ca2ed2697ff792af42ec37b6cc9 (patch)
tree5773d3249e2f4c9e3438f6ba8df467f78775b2a6
parent2e4be2314249c7c6d6222482cc3a37bef6ffb019 (diff)
Fix pattern match error
-rw-r--r--src/lem_interp/interp_lib.lem5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 83bee732..875907fe 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -77,12 +77,12 @@ let zeroi = integerFromNat 0
let onei = integerFromNat 1
let twoi = integerFromNat 2
-let is_unknown v = match v with
+let is_unknown v = match detaint v with
| V_unknown -> true
| _ -> false
end
-let is_undef v = match v with
+let is_undef v = match detaint v with
| V_lit (L_aux L_undef _) -> true
| _ -> false
end
@@ -141,6 +141,7 @@ let bit_to_bool b = match detaint b with
| V_lit (L_aux L_false _) -> false
| V_lit (L_aux L_one _) -> true
| V_lit (L_aux L_true _) -> true
+ | _ -> Assert_extra.failwith ("bit_to_bool given unexpected " ^ (string_of_value b))
end ;;
let bool_to_bit b = match b with
false -> V_lit (L_aux L_zero Unknown)