Fix a series of errors leading to the first ARM instruction not running.

Including:
Correct loss of constraints between declared constraints, pattern constraints and expression body constraints
Handle insertion of dependent parameters in the case of unit parameters
Add a case to how ifields are translated to permit numbers as well as bits and bitvectors
Expand interpreter to actually handle user-defined functions on the left had side of the assignment expression.

3 files changed, 45 insertions, 8 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 11eaa625..50158ff6 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1851,8 +1851,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
               (fun v lm le -> (Value v,lm,le))
               (fun a -> 
 		(match a with
-		  | (Action (Write_reg regf range value) stack) -> (Action (Write_reg regf range value) stack)
-		  | (Action (Write_mem id a range value) stack) -> (Action (Write_mem id a range value) stack)
+		  | (Action (Write_reg regf range value) stack) -> a
+		  | (Action (Write_mem id a_ range value) stack) -> a
 		  | _ -> update_stack a (add_to_top_frame 
 					   (fun e env -> 
                                              let (ev,env') = (to_exp mode env v) in
@@ -1880,7 +1880,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			(add_to_top_frame (fun e env-> (E_aux (E_block(e::exps)) (l,tannot), env))))
     end
 
-and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv))) =
+and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) 
+  : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv))) =
    let (Env defs instrs lets regs ctors subregs aliases) = t_level in
   let (typ,tag,ncs,ef) = match annot with 
     | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
@@ -2005,7 +2006,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		      l_env l_mem [] exps) with
       | (Value v,lm,le) ->
         (match tag with
-        | Tag_extern ->
+        | Tag_extern _ ->
           let request = (Action (Write_mem id v Nothing value) 
                            (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env lm Top),
 			 lm,l_env) in
@@ -2015,6 +2016,30 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
              Just (fun e env->
                let (parms,env) = (to_exps mode env (match v with | V_tuple vs -> vs | v -> [v] end)) in
 	       (LEXP_aux (LEXP_memory id parms) (l,annot), env)))
+	| Tag_global ->
+          let name = get_id id in 
+	  (match find_function defs id with
+	    | Just(funcls) -> 
+              (match find_funcl funcls (V_tuple [v;value]) with
+		| [] -> ((Error l ("No matching pattern for function " ^ name ^
+				      " on value " ^ (string_of_value v)),l_mem,l_env),Nothing)
+		| [(env,used_unknown,exp)] -> 
+		  (match (if mode.eager_eval 
+		          then (interp_main mode t_level env emem exp)
+		          else (debug_out (Just name) (Just v) exp t_level emem env)) with
+		    | (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing)
+		    | (Action action stack,lm,le) ->
+		      (((update_stack (Action action stack) 
+			  (fun stack -> (Hole_frame (id_of_string "0") 
+					   (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
+					   t_level l_env l_mem stack))), l_mem,l_env), Nothing)
+		    | (e,lm,le) -> ((e,lm,le),Nothing) end)
+                | multi_matches ->
+                  let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in
+                  (interp_main mode t_level l_env l_mem (E_aux (E_block lets) (l,annot)), Nothing)
+               end)
+            | Nothing -> 
+	      ((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end)
          end)
       | (Action a s,lm, le) -> 
 	((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) env -> (LEXP_aux (LEXP_memory id es) (l,annot), env)))
@@ -2151,7 +2176,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	     ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
            | _ -> ((Action a s,lm,le), Just (next_builder lexp_builder)) end)
          | e -> e end)
-        | _ -> ((Error l "Vector access must be a number",lm,le),Nothing) end)
+        | v -> ((Error l ("Vector access must be a number given " ^ (string_of_value v)),lm,le),Nothing) end)
       | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector lexp e) (l,annot), env)))
       | e -> (e,Nothing) end
     | LEXP_vector_range lexp exp1 exp2  ->
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 94f5abc6..e4d12ac9 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -459,13 +459,23 @@ val instruction_to_istate : context -> instruction -> instruction_state
 let instruction_to_istate (top_level:context) (((name, parms, _) as instr):instruction) : instruction_state  = 
   let mode = make_mode true false in
   let get_value (name,typ,v) = 
-    let (e,_) = Interp.to_exp mode Interp.eenv (intern_ifield_value v) in e in
-    (Interp.Thunk_frame
+    let vec = intern_ifield_value v in
+    let v = match vec with
+      | Interp.V_vector start dir bits ->
+	match typ with
+	  | Bit -> match bits with | [b] -> b | _ -> Assert_extra.failwith "Expected a bitvector of length 1" end
+	  | Range _ -> Interp_lib.to_num Interp_lib.Signed vec
+	  | _ -> vec
+       end 
+    end in
+    let (e,_) = Interp.to_exp mode Interp.eenv v in e 
+  in
+  (Interp.Thunk_frame
        (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) 
 		 [(E_aux (E_app (Id_aux (Id name) Interp_ast.Unknown) (List.map get_value parms))
 		        (Interp_ast.Unknown,Interp.ctor_annot (T_id "ast")) (*This type shouldn't be hard-coded*))])
 	      (Interp_ast.Unknown,Nothing))
-       top_level Interp.eenv Interp.emem Interp.Top) 
+       top_level Interp.eenv Interp.emem Interp.Top)
 
 let rec interp_to_outcome mode thunk = 
   match thunk () with
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index ae29a2e9..3b83dd89 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -349,12 +349,14 @@ val initial_instruction_state : context -> string -> list register_value -> inst
 (*Type representint the constructor parameters in instruction, other is a type not representable externally*)
 type instr_parm_typ = 
   | Bit (*A single bit, represented as a one element Bitvector as a value*)
+  | Range of maybe int (*Internall represented as a number, externally as a bitvector of length int *)
   | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
   | Bvector of maybe int (* A bitvector type, with length when statically known *)
 
 let instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with
   | (Bit,Bit) -> true
   | (Other,Other) -> true
+  | (Range i1,Range i2) -> i1 = i2
   | (Bvector i1,Bvector i2) -> i1 = i2
   | _ -> false
 end