More interface update for connecting externally (interp_interface provides functions for connecting the interpreter to a memory model)

Also adding default values to index vectors for supporting sparse vectors/maps

6 files changed, 67 insertions, 29 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 2548bf19..95578d9f 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -354,7 +354,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
     | Parse_ast.E_for(id,e1,e2,e3,atyp,e4) -> 
       E_for(to_ast_id id,to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3,to_ast_order k_env atyp, to_ast_exp k_env e4)
     | Parse_ast.E_vector(exps) -> E_vector(List.map (to_ast_exp k_env) exps)
-    | Parse_ast.E_vector_indexed(iexps) -> E_vector_indexed(List.map (fun (i,e) -> (i,to_ast_exp k_env e)) iexps)
+    | Parse_ast.E_vector_indexed(iexps,default) -> E_vector_indexed(List.map (fun (i,e) -> (i,to_ast_exp k_env e)) iexps, Def_val_aux(Def_val_empty,(l,NoTyp))) (*TODO transform the default *)
     | Parse_ast.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp k_env vexp, to_ast_exp k_env exp)
     | Parse_ast.E_vector_subrange(vex,exp1,exp2) -> E_vector_subrange(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
     | Parse_ast.E_vector_update(vex,exp1,exp2) -> E_vector_update(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
diff --git a/src/lem_interp/Interp_interface.lem b/src/lem_interp/Interp_interface.lem
index 0767ea79..136078aa 100644
--- a/src/lem_interp/Interp_interface.lem
+++ b/src/lem_interp/Interp_interface.lem
@@ -4,49 +4,47 @@ type read_kind = Interp.read_kind
 type write_kind = Interp.write_kind
 type barrier_kind = Interp.barrier_kind
 
+type word8 = nat (* bounded at a byte, for when lem supports it*)
+
 type value = 
-| Bitvector of list nat (*Always 0 or 1; should this be a Word.bitSequence? *)
-| Bytevector of list (list nat) (* Should this be a list of Word.bitSequence? *)
+| Bitvector of list bool (* For register accesses *)
+| Bytevector of list word8 (* For memory accesses *)
 | Unknown
 
 type instruction_state = Interp.stack
 type context = Interp.top_level
 
-type reg_name = Interp.reg_form (*for now...*)
+type reg_name = 
+| Reg of string (*Name of the register, accessing the entire register*)
+| Reg_slice of string * integer * integer (*Name of the register, accessing from the first to second integer*)
+| Reg_field of string * string * integer * integer (*Name of the register, name of the field of the register accessed, the index range of the field*)
+| Reg_f_slice of string * string * integer * integer * integer * integer (* Same as above but only accessing from the third to the fourth integer of the field *)
 
 type outcome =
 | Read_mem of read_kind * value * (value -> instruction_state)
 | Write_mem of write_kind * value * value * (bool -> instruction_state)
 | Barrier of barrier_kind * instruction_state
-| Read_reg of reg_name * (value -> instruction_state) (*What about slicing?*)
+| Read_reg of reg_name * (value -> instruction_state) 
 | Write_reg of reg_name * value * instruction_state
 | Nondet_choice of list instruction_state
 | Internal of instruction_state
 | Done
 | Error of string
 
+type event = 
+| E_read_mem of read_kind * value
+| E_write_mem of write_kind * value
+| E_barrier of barrier_kind
+| E_read_reg of reg_name
+| E_write_reg of reg_name
+(*Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
+
+
 val build_context : Interp.defs Interp.tannot -> context
 val initial_instruction_state : context -> string -> value -> instruction_state
 
 type interp_mode = <| eager_eval : bool |>
-val interp : instruction_state -> interp_mode -> outcome
-
-val interp_exhaustive : instruction_state -> list outcome (*not sure what event was ment to be*)
-
-val intern_value : value -> Interp.value
-val extern_value : Interp.value -> value
-
-let build_context defs = Interp.to_top_env defs
-
-let intern_value v = match v with
-  | Bitvector bs -> Interp.V_vector 0 true (List.map (fun | 0 -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown)) 
-							  | _ -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown))) bs)
-  | Unknown -> Interp.V_unknown
+val interp : interp_mode -> instruction_state -> outcome
 
-let extern_value v = match v with
-  | Interp.V_vector _ true bits -> Bitvector (List.map (fun | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> 0
-							    | _ -> 1) bits)
-  | _ -> Unknown
+val interp_exhaustive : instruction_state -> list event
 
-let initial_instruction_state top_level main arg = 
-  Interp.Frame Nothing (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [ intern_value arg ]) (Interp_ast.Unknown, Nothing)) top_level [] Interp.emem
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
new file mode 100644
index 00000000..8b7fdec3
--- /dev/null
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -0,0 +1,40 @@
+import Interp
+import Interp_lib
+open import Interp_interface
+
+val intern_value : value -> Interp.value
+val extern_value : Interp.value -> value
+
+let build_context defs = Interp.to_top_env defs
+
+let intern_value v = match v with
+  | Bitvector bs -> Interp.V_vector 0 true (List.map (fun | 0 -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown)) 
+							  | _ -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown))) bs)
+  | Unknown -> Interp.V_unknown
+end
+
+let extern_value v = match v with
+  | Interp.V_vector _ true bits -> Bitvector (List.map (fun | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> 0
+							    | _ -> 1) bits)
+  | _ -> Unknown
+end
+
+let initial_instruction_state top_level main arg = 
+  Interp.Frame Nothing (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [ intern_value arg ]) (Interp_ast.Unknown, Nothing)) top_level [] Interp.emem
+
+let interp mode i_state = 
+  match Interp.resume mode i_state None with
+  | Interp.Value _ -> Done
+  | Interp.Error l msg -> Error msg (*Todo, add the l information the string format*)
+  | Interp.Action a next_state ->
+    match a with
+    | Interp.Read_reg reg_form slice -> Read_reg reg_form (fun v -> Interp.add_answer_to_stack (intern_value v) next_state)
+    | Interp.Write_reg reg_form slice value -> Write_reg reg_form (extern_value value) next_state
+    | Interp.Read_mem (Id_aux (Id i) _) value slice 
+        (*Need to lookup the Mem function used to determine appropriate value, and possible appropriate read_kind *)
+      -> Read_mem Interp.Read_plain (extern_value value) (fun v -> Interp.add_answer_to_stack (intern_value v) next_state)
+    | Interp.Write_mem (Id_aux (id i) _) loc_val slice write_val ->
+      Write_mem Interp.Write_plain (extern_value loc_val) (extern_value write_val) next_state
+    | Interp.Call_extern id value -> (*Connect here to a list of external functions*)
+    end 
+  end
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index ecafc5f2..759e2f4a 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -236,7 +236,7 @@ and pp_exp ppf (E_aux(e,(_,annot))) =
     fprintf ppf "@[<0> %a %a (%a %a %a %a %a %a %a %a)@ @[<1>%a@]@]" 
       kwd "foreach " pp_id id kwd "from " pp_exp exp1 kwd " to " pp_exp exp2 kwd "by " pp_exp exp3 kwd "in" pp_ord order pp_exp exp4
   | E_vector(exps) -> fprintf ppf "@[<0>%a%a%a@]" kwd "[" (list_pp pp_comma_exp pp_exp) exps kwd "]"
-  | E_vector_indexed(iexps) -> 
+  | E_vector_indexed(iexps,default) -> 
     let iformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a%a@]" i kwd " = " pp_exp e kwd "," in
     let lformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a@]" i kwd " = " pp_exp e in
     fprintf ppf "@[<0> %a%a%a@]" kwd "[" (list_pp iformat lformat) iexps kwd "]"
@@ -666,7 +666,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
       fprintf ppf "@[<0>(E_aux (%a %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]" 
 	kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot
     | E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
-    | E_vector_indexed(iexps) -> 
+    | E_vector_indexed(iexps,default) -> (*TODO print out default when it is an nonempty*) 
       let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
       let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
       fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps pp_lem_l l pp_annot annot
diff --git a/src/type_check.ml b/src/type_check.ml
index 9dc5750f..218efb84 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -622,7 +622,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst 0});TA_nexp({nexp=Nconst (List.length es)});TA_ord({order=Oinc});TA_typ item_t])} in
       let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
       (e',t',t_env,cs@cs',effect)
-    | E_vector_indexed eis ->
+    | E_vector_indexed(eis,default) ->
       let item_t = match expect_t.t with
         | Tapp("vector",[base;rise;ord;TA_typ item_t]) -> item_t
         | _ -> new_t () in
@@ -639,7 +639,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 				 eis) ([],[],pure_e,first)) in
       let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst first});TA_nexp({nexp=Nconst (List.length eis)});
 				  TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in
-      let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector_indexed es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
+      let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector_indexed(es,default),(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
       (e',t',t_env,cs@cs',effect)
     | E_vector_access(vec,i) ->
       let base,rise,ord = new_n(),new_n(),new_o() in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 26a03d6a..abee5a9c 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1017,7 +1017,7 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
   | Tid("bit"),Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]) ->
     let cs = [Eq(co,r1,{nexp = Nconst 1})] in
     let t2' = {t = Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp {nexp=Nconst 1};TA_ord o;TA_typ {t=Tid "bit"}])} in
-    (t2',cs,E_aux(E_vector_indexed [(i,e)],(l,Base(([],t2),Emp_local,cs,pure_e))))
+    (t2',cs,E_aux(E_vector_indexed([(i,e)],Def_val_aux(Def_val_empty,(l,NoTyp))) ,(l,Base(([],t2),Emp_local,cs,pure_e))))
   | Tapp("vector",[TA_nexp ({nexp=Nconst i} as b1);TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") ->
     let cs = [Eq(co,r1,{nexp = Nconst 1})] in
     (t2,cs,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num i,l)),