Interpret when an unknown is inserted into the program by interp_exhaustive

Short version of below; ready to hook interp_exhaustive up to something to test, but haven't yet.

If an unknown value influences a pattern match within an expression, each passing pattern is found and the bodies strung together into a block with let expressions to bind the variables.
In a function call, the cases are all collected but the support is not in place at the moment to evaluate them.
If an unknown is the result of the cond expression in an if, the then and else case become a block.
Unknowns within the interpreter propagate to more Unknowns; also for some but not all library functions yet.

1 files changed, 14 insertions, 5 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 5289be88..7d77224b 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -11,12 +11,19 @@ let ignore_sail x = V_lit (L_aux L_unit Unknown) ;;
 
 let compose f g x = f (V_tuple [g x]) ;;
 
-let is_one (V_lit (L_aux b lb)) = V_lit (L_aux (if b = L_one then L_true else L_false) lb) ;;
+let is_one v = match v with 
+  | V_lit (L_aux b lb) -> V_lit (L_aux (if b = L_one then L_true else L_false) lb)
+  | V_unknown -> V_unknown
+end ;;
 
-let lt_range (V_tuple[V_lit (L_aux (L_num l1) lr);V_lit (L_aux (L_num l2) ll);]) =
-  if l1 < l2
-  then V_lit (L_aux L_one Unknown)
-  else V_lit (L_aux L_zero Unknown)
+let lt_range (V_tuple[v1;v2]) = match (v1,v2) with 
+  | (V_lit (L_aux (L_num l1) lr),V_lit (L_aux (L_num l2) ll)) ->
+    if l1 < l2
+    then V_lit (L_aux L_one Unknown)
+    else V_lit (L_aux L_zero Unknown)
+  | (V_unknown,_) -> V_unknown
+  | (_,V_unknown) -> V_unknown
+end ;;
 
 let bit_to_bool b = match b with
     V_lit (L_aux L_zero _) -> false
@@ -84,6 +91,8 @@ let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
 let neq = compose neg eq ;;
 
 let arith_op op (V_tuple args) = match args with
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
   | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (op x y)) lx)
   end ;;
 let arith_op_vec op (V_tuple args) = match args with