Working towards evaluating with interp_exhaustive

3 files changed, 121 insertions, 82 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 2960f048..0490fca4 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -204,6 +204,15 @@ let rec to_data_constructors (Defs defs) =
     | _ -> to_data_constructors (Defs defs) end
    end
 
+(* Due to type checker, all variables should be in the environment unless an Unknown has matched a pattern,
+   so unfound identifiers propogate Unknown *)
+val in_venv : (list (id * value)) -> id -> value
+let rec in_venv env id =
+ match env with
+ | [] -> V_unknown
+ | (eid,value)::env -> if (get_id eid) = (get_id id) then value else in_venv env id
+ end 
+
 val in_env :forall 'a. (list (id * 'a)) -> id -> maybe 'a
 let rec in_env env id =
  match env with
@@ -473,7 +482,8 @@ let rec find_function (Defs defs) id =
     | _ -> find_function (Defs defs) id
     end end
 
-val match_pattern : pat tannot -> value -> bool * list (id * value)
+(* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
+val match_pattern : pat tannot -> value -> bool * bool * list (id * value)
 let rec match_pattern (P_aux p _) value =
   match p with 
   | P_lit(lit) -> 
@@ -483,112 +493,121 @@ let rec match_pattern (P_aux p _) value =
       | V_lit litv -> 
         if is_lit_vector litv then 
           let (V_vector n' inc' bits') = litV_to_vec litv in
-          if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l = r) && rest) true bits bits', [])
-          else (false,[])
-        else (false,[])
+          if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l = r) && rest) true bits bits',false, [])
+          else (false,false,[])
+        else (false,false,[])
       | V_vector n' inc' bits' -> 
-        if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l=r) && rest) true bits bits',[])
-        else (false,[])
-      | _ -> (false,[]) end
+        if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l=r) && rest) true bits bits',false,[])
+        else (false,false,[])
+      | V_unknown -> (true,true,[])
+      | _ -> (false,false,[]) end
     else
     match value with
-    | V_lit(litv) -> (lit = litv, [])
-    | _ -> (false,[])
+    | V_lit(litv) -> (lit = litv, false,[])
+    | V_unknown -> (true,true,[])
+    | _ -> (false,false,[])
     end
- | P_wild -> (true,[])
- | P_as pat id ->  let (matched_p,bounds) = match_pattern pat value in
+ | P_wild -> (true,false,[])
+ | P_as pat id ->  let (matched_p,used_unknown,bounds) = match_pattern pat value in
 		     if matched_p then
-		       (matched_p,(id,value)::bounds)
-		     else (false,[])
+		       (matched_p,used_unknown,(id,value)::bounds)
+		     else (false,false,[])
  | P_typ typ pat -> match_pattern pat value (* Might like to destructure against the type to get information *)
- | P_id id -> (true, [(id,value)])
+ | P_id id -> (true, false, [(id,value)])
  | P_app (Id_aux id _) pats -> 
    match value with
    | V_ctor (Id_aux cid _) t (V_tuple vals) -> 
      if (id = cid && ((List.length pats) = (List.length vals)))
      then foldr2
-          (fun pat value (matched_p,bounds) ->
+          (fun pat value (matched_p,used_unknown,bounds) ->
             if matched_p then
-              let (matched_p,new_bounds) = match_pattern pat value in
-              (matched_p, (new_bounds ++ bounds))
-            else (false,[])) (true,[]) pats vals
-     else (false,[])
-   | _ -> (false,[]) end
+              let (matched_p,used_unknown',new_bounds) = match_pattern pat value in
+              (matched_p, (used_unknown || used_unknown'), (new_bounds ++ bounds))
+            else (false,false,[])) (true,false,[]) pats vals
+     else (false,false,[])
+   | V_unknown -> (true,true,[])
+   | _ -> (false,false,[]) end
  | P_record fpats _ ->
    match value with
    | V_record t fvals ->
      List.foldr
-       (fun (FP_aux (FP_Fpat id pat) _) (matched_p,bounds) ->
+       (fun (FP_aux (FP_Fpat id pat) _) (matched_p,used_unknown,bounds) ->
          if matched_p then
-           let (matched_p,new_bounds) = match in_env fvals id with
-                                       | Nothing -> (false,[])
+           let (matched_p,used_unknown',new_bounds) = match in_env fvals id with
+                                       | Nothing -> (false,false,[])
                                        | Just v -> match_pattern pat v end in
-           (matched_p, (new_bounds ++ bounds))
-         else (false,[])) (true,[]) fpats
-   | _ -> (false,[])
+           (matched_p, (used_unknown || used_unknown'), (new_bounds ++ bounds))
+         else (false,false,[])) (true,false,[]) fpats
+   | V_unknown -> (true,true,[])
+   | _ -> (false,false,[])
    end           
  | P_vector pats ->
    match value with
    | V_vector n inc vals ->
      if ((List.length vals) = (List.length pats))
      then foldr2
-       (fun pat value (matched_p,bounds) -> 
+       (fun pat value (matched_p,used_unknown,bounds) -> 
 	 if matched_p then
-	   let (matched_p,new_bounds) = match_pattern pat value in
-	   (matched_p, (new_bounds ++ bounds)) 
-	 else (false,[]))
-       (true,[]) (if inc then pats else List.reverse pats) vals
-     else (false,[])
-   | _ -> (false,[])
+	   let (matched_p,used_unknown',new_bounds) = match_pattern pat value in
+	   (matched_p, (used_unknown||used_unknown'), (new_bounds ++ bounds)) 
+	 else (false,false,[]))
+       (true,false,[]) (if inc then pats else List.reverse pats) vals
+     else (false,false,[])
+   | V_unknown -> (true,true,[])
+   | _ -> (false,false,[])
      end
  | P_vector_indexed ipats ->
    match value with
    | V_vector n inc vals ->
      let v_len = if inc then list_length vals + n else n - list_length vals in
      List.foldr
-       (fun (i,pat) (matched_p,bounds) -> if matched_p && i < v_len then
-	   let (matched_p,new_bounds) = match_pattern pat (list_nth vals (if inc then i+n else i-n)) in
-	   (matched_p,new_bounds++bounds)
-         else (false,[]))
-       (true,[]) ipats
-   | _ -> (false, [])
+       (fun (i,pat) (matched_p,used_unknown,bounds) -> if matched_p && i < v_len then
+	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (list_nth vals (if inc then i+n else i-n)) in
+	   (matched_p,used_unknown||used_unknown',new_bounds++bounds)
+         else (false,false,[]))
+       (true,false,[]) ipats
+   | V_unknown -> (true,true,[])
+   | _ -> (false,false, [])
    end 
  | P_vector_concat pats ->
    match value with
    | V_vector n inc vals ->
-     let (matched_p,bounds,remaining_vals) =
+     let (matched_p,used_unknown,bounds,remaining_vals) =
        List.foldl 
-         (fun (matched_p,bounds,r_vals) (P_aux pat (l,Just(t,_,_,_))) ->
-	   let (matched_p,bounds',matcheds,r_vals) = vec_concat_match_plev pat r_vals inc l t in
-	   (matched_p,bounds' ++ bounds,r_vals)) (true,[],vals) pats in
-     if matched_p && ([] = remaining_vals) then (matched_p,bounds) else (false,[]) 
-   | _ -> (false, []) 
+         (fun (matched_p,used_unknown,bounds,r_vals) (P_aux pat (l,Just(t,_,_,_))) ->
+	   let (matched_p,used_unknown',bounds',matcheds,r_vals) = vec_concat_match_plev pat r_vals inc l t in
+	   (matched_p,(used_unknown || used_unknown'),bounds' ++ bounds,r_vals)) (true,false,[],vals) pats in
+     if matched_p && ([] = remaining_vals) then (matched_p,used_unknown,bounds) else (false,false,[]) 
+   | V_unknown -> (true,true,[])
+   | _ -> (false,false, []) 
    end
  | P_tup(pats) ->
    match value with 
    | V_tuple(vals) ->
      if ((List.length pats)= (List.length vals))
      then foldr2 
-       (fun pat v (matched_p,bounds) -> if matched_p then
-	   let (matched_p,new_bounds) = match_pattern pat v in
-	   (matched_p,bounds++new_bounds)
-	 else (false,[]))
-       (true,[]) pats vals
-     else (false,[])
-   | _ -> (false,[])
+       (fun pat v (matched_p,used_unknown,bounds) -> if matched_p then
+	   let (matched_p,used_unknown',new_bounds) = match_pattern pat v in
+	   (matched_p,used_unknown ||used_unknown', bounds++new_bounds)
+	 else (false,false,[]))
+       (true,false,[]) pats vals
+     else (false,false,[])
+   | V_unknown -> (true,true,[])
+   | _ -> (false,false,[])
      end 
  | P_list(pats) ->
    match value with 
    | V_list(vals) ->
      if ((List.length pats)= (List.length vals))
      then foldr2 
-       (fun pat v (matched_p,bounds) -> if matched_p then
-	   let (matched_p,new_bounds) = match_pattern pat v in
-	   (matched_p,bounds++new_bounds)
-	 else (false,[]))
-       (true,[]) pats vals
-     else (false,[])
-   | _ -> (false,[]) end
+       (fun pat v (matched_p,used_unknown,bounds) -> if matched_p then
+	   let (matched_p,used_unknown',new_bounds) = match_pattern pat v in
+	   (matched_p,used_unknown|| used_unknown', bounds++new_bounds)
+	 else (false,false,[]))
+       (true,false,[]) pats vals
+     else (false,false,[])
+   | V_unknown -> (true,true,[])
+   | _ -> (false,false,[]) end
  end 
 
 and vec_concat_match_plev pat r_vals inc l t =
@@ -601,40 +620,40 @@ and vec_concat_match_plev pat r_vals inc l t =
       | P_id id -> (match t with
 	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
 	    let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
-	    let (matched_p,bounds,matcheds,r_vals) = vec_concat_match wilds r_vals in
+	    let (matched_p,used_unknown,bounds,matcheds,r_vals) = vec_concat_match wilds r_vals in
 	    if matched_p 
-	    then (matched_p, (id,(V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds))::bounds,matcheds,r_vals)
-	    else (false,[],[],[])
+	    then (matched_p, used_unknown, (id,(V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds))::bounds,matcheds,r_vals)
+	    else (false,false,[],[],[])
 	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
-	    (false,[],[],[]) (*TODO see if can have some constraint bounds here*)
-	  | _ -> (false,[],[],[]) end)
+	    (false,false,[],[],[]) (*TODO see if can have some constraint bounds here*)
+	  | _ -> (false,false,[],[],[]) end)
       | P_wild -> (match t with
 	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
 	    let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
 	    vec_concat_match wilds r_vals 
 	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
-	    (false,[],[],[]) (*TODO see if can have some constraint bounds here*)
-	  | _ -> (false,[],[],[]) end)
+	    (false,false,[],[],[]) (*TODO see if can have some constraint bounds here*)
+	  | _ -> (false,false,[],[],[]) end)
       | P_as (P_aux pat (l',Just(t,_,_,_))) id -> 
-	let (matched_p, bounds,matcheds,r_vals) = vec_concat_match_plev pat r_vals inc l t in
+	let (matched_p, used_unknown, bounds,matcheds,r_vals) = vec_concat_match_plev pat r_vals inc l t in
 	if matched_p 
-	then (matched_p, ((id,V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds)::bounds),matcheds,r_vals)
-	else (false,[],[],[])	  
+	then (matched_p, used_unknown,((id,V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds)::bounds),matcheds,r_vals)
+	else (false,false,[],[],[])	  
       | P_typ _ (P_aux p (l',Just(t',_,_,_))) -> vec_concat_match_plev p r_vals inc l t
-      | _ -> (false,[],[],[]) end 
+      | _ -> (false,false,[],[],[]) end 
       (*TODO Need to support indexed here, skipping intermediate numbers but consumming r_vals, and as *)
 
 and vec_concat_match pats r_vals =
     match pats with
-    | [] -> (true,[],[],r_vals)
+    | [] -> (true,false,[],[],r_vals)
     | pat::pats -> match r_vals with
-      | [] -> (false,[],[],[])
+      | [] -> (false,false,[],[],[])
       | r::r_vals -> 
-	let (matched_p,new_bounds) = match_pattern pat r in
+	let (matched_p,used_unknown,new_bounds) = match_pattern pat r in
         if matched_p then 
-          let (matched_p,bounds,matcheds,r_vals) = vec_concat_match pats r_vals in
-          (matched_p, new_bounds++bounds,matcheds++[r],r_vals)
-        else (false,[],[],[]) end
+          let (matched_p,used_unknown',bounds,matcheds,r_vals) = vec_concat_match pats r_vals in
+          (matched_p, used_unknown||used_unknown',new_bounds++bounds,matcheds++[r],r_vals)
+        else (false,false,[],[],[]) end
     end
 
 
@@ -643,7 +662,7 @@ let rec find_funcl funcls value =
   match funcls with
   | [] -> Nothing
   | (FCL_aux (FCL_Funcl id pat exp) _)::funcls ->
-    let (is_matching,env) = match_pattern pat value in
+    let (is_matching,used_unknown,env) = match_pattern pat value in
     if is_matching then Just (env,exp) else find_funcl funcls value
   end
 
@@ -652,7 +671,7 @@ let rec find_case pexps value =
   match pexps with
   | [] -> Nothing
   | (Pat_aux (Pat_exp p e) _)::pexps -> 
-    let (is_matching,env) = match_pattern p value in
+    let (is_matching,used_unknown,env) = match_pattern p value in
     if is_matching then Just(env,e) else find_case pexps value
   end
 
@@ -1352,7 +1371,7 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
     match (interp_main mode t_level l_env l_mem exp) with
     | (Value v Tag_empty,lm,le) ->
       (match match_pattern pat v with
-      | (true,env) -> ((Value (V_lit (L_aux L_unit l)) Tag_empty, lm, env++l_env),Nothing)
+      | (true,used_unknown,env) -> ((Value (V_lit (L_aux L_unit l)) Tag_empty, lm, env++l_env),Nothing)
       | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
     | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e ->(LB_aux (LB_val_explicit t pat e) (l,annot)))))
     | e -> (e,Nothing) end
@@ -1360,7 +1379,7 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
     match (interp_main mode t_level l_env l_mem exp) with
     | (Value v Tag_empty,lm,le) ->
       (match match_pattern pat v with
-      | (true,env) -> ((Value (V_lit (L_aux L_unit l)) Tag_empty, lm, env++l_env),Nothing)
+      | (true,used_unknown,env) -> ((Value (V_lit (L_aux L_unit l)) Tag_empty, lm, env++l_env),Nothing)
       | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
     | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) (l,annot)))))
     | e -> (e,Nothing) end
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 03def81c..1eb16d9d 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -85,3 +85,22 @@ let rec interp_to_outcome mode thunk =
   end 
 
 let interp mode i_state = interp_to_outcome mode (fun _ -> Interp.resume mode i_state Nothing)
+
+let rec ie_loop mode i_state = 
+  match (interp mode i_state) with
+    | Done -> []
+    | Error msg -> [E_error msg]
+    | Read_reg reg i_state_fun -> 
+      (E_read_reg reg)::(ie_loop mode (i_state_fun Unknown))
+    | Write_reg reg value i_state->
+      (E_write_reg reg value)::(ie_loop mode i_state)
+    | Read_mem read_k loc i_state_fun ->
+      (E_read_mem read_k loc)::(ie_loop mode (i_state_fun Unknown))
+    | Write_mem write_k loc value i_state_fun ->
+      (E_write_mem write_k loc value)::(ie_loop mode (i_state_fun true))
+    | Internal next -> (ie_loop mode next)
+     end ;;
+  
+let interp_exhaustive i_state = 
+  let mode = <| Interp.eager_eval = true |> in
+  ie_loop mode i_state
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 00c22bbe..d102c1fe 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -36,10 +36,11 @@ type outcome =
 
 type event = 
 | E_read_mem of read_kind * value
-| E_write_mem of write_kind * value
+| E_write_mem of write_kind * value * value
 | E_barrier of barrier_kind
 | E_read_reg of reg_name
-| E_write_reg of reg_name
+| E_write_reg of reg_name * value
+| E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*)
 (*Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)