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.

6 files changed, 88 insertions, 26 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 
diff --git a/src/type_check.ml b/src/type_check.ml
index c3e02746..1636d17f 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -266,29 +266,31 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 	| _ -> default)
     | P_app(id,pats) -> 
       let i = id_to_string id in
+      (*let _ = Printf.printf "checking constructor pattern %s\n" i in*)
       (match Envmap.apply t_env i with
 	| None | Some NoTyp | Some Overload _ -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined")
 	| Some(Base((params,t),Constructor,constraints,eft,bounds)) -> 
-          let t,constraints,_,_ = subst params t constraints eft in
+          let t,dec_cs,_,_ = subst params t constraints eft in
 	  (match t.t with
 	    | Tid id -> if pats = [] 
-	      then let t',constraints' = type_consistent (Patt l) d_env false t expect_t in
-		   (P_aux(p,(l,cons_tag_annot t' Constructor constraints)), Envmap.empty,constraints@constraints',nob,t')
+	      then let t',ret_cs = type_consistent (Patt l) d_env false t expect_t in
+		   (P_aux(p,(l,cons_tag_annot t' Constructor dec_cs)), Envmap.empty,dec_cs@ret_cs,nob,t')
 	      else typ_error l ("Constructor " ^ i ^ " does not expect arguments")
 	    | Tfn(t1,t2,IP_none,ef) ->
+	      let t',ret_cs = type_consistent (Patt l) d_env false t2 expect_t in
               (match pats with
               | [] -> let _ = type_consistent (Patt l) d_env false unit_t t1 in
-                      let t',constraints' = type_consistent (Patt l) d_env false t2 expect_t in
-                      (P_aux(P_app(id,[]),(l,cons_tag_annot t' Constructor constraints)), Envmap.empty,constraints@constraints',nob,t')
-              | [p] -> let (p',env,constraints,bounds,u) = check_pattern envs emp_tag t1 p in
-                       let t',constraints' = type_consistent (Patt l) d_env false t2 expect_t in
-                       (P_aux(P_app(id,[p']),(l,cons_tag_annot t' Constructor constraints)),env,constraints@constraints',bounds,t')
-              | pats -> let (pats',env,constraints,bounds,u) = 
+                      (P_aux(P_app(id,[]),(l,cons_tag_annot t' Constructor dec_cs)),
+		       Envmap.empty,dec_cs@ret_cs,nob,t')
+              | [p] -> let (p',env,p_cs,bounds,u) = check_pattern envs emp_tag t1 p in
+                       (P_aux(P_app(id,[p']),
+			      (l,cons_tag_annot t' Constructor dec_cs)),env,dec_cs@p_cs@ret_cs,bounds,t')
+              | pats -> let (pats',env,p_cs,bounds,u) = 
                           match check_pattern envs emp_tag t1 (P_aux(P_tup(pats),(l,annot))) with
                           | ((P_aux(P_tup(pats'),_)),env,constraints,bounds,u) -> (pats',env,constraints,bounds,u)
                           | _ -> assert false in
-                        let t',constraints' = type_consistent (Patt l) d_env false t2 expect_t in
-	                (P_aux(P_app(id,pats'),(l,cons_tag_annot t' Constructor constraints)),env,constraints@constraints',bounds,t'))
+	                (P_aux(P_app(id,pats'),
+			       (l,cons_tag_annot t' Constructor dec_cs)),env,dec_cs@p_cs@ret_cs,bounds,t'))
 	    | _ -> typ_error l ("Identifier " ^ i ^ " must be a union constructor"))
 	| Some(Base((params,t),tag,constraints,eft,bounds)) -> 
 	  typ_error l ("Identifier " ^ i ^ " used in pattern is not a union constructor"))
@@ -580,7 +582,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
     | E_app(id,parms) -> 
       let i = id_to_string id in
       let check_parms p_typ parms = (match parms with
-        | [] -> let (_,cs') = type_consistent (Expr l) d_env false unit_t p_typ in [],unit_t,cs',pure_e 
+        | [] | [(E_aux (E_lit (L_aux (L_unit,_)),_))] 
+	  -> let (_,cs') = type_consistent (Expr l) d_env false unit_t p_typ in [],unit_t,cs',pure_e 
         | [parm] -> let (parm',arg_t,t_env,cs',_,ef_p) = check_exp envs imp_param p_typ parm in [parm'],arg_t,cs',ef_p
         | parms -> 
           (match check_exp envs imp_param p_typ (E_aux (E_tuple parms,(l,NoTyp))) with
@@ -589,6 +592,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       in
       let coerce_parms arg_t parms expect_arg_t =
 	(match parms with
+	| [] | [(E_aux (E_lit (L_aux(L_unit, _)), _))] -> [],pure_e,[]
 	| [parm] -> 
 	  let _,cs,ef,parm' = type_coerce (Expr l) d_env false false arg_t parm expect_arg_t in [parm'],ef,cs
 	| parms ->
@@ -1705,8 +1709,9 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
   let check t_env tp_env imp_param =
     List.split
       (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) ->
-(*	let _ = Printf.printf "checking function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
+	(*let _ = Printf.printf "checking function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
 	let (pat',t_env',cs_p,b_env',t') = check_pattern (Env(d_env,t_env,b_env,tp_env)) Emp_local param_t pat in
+	(*let _ = Printf.printf "cs_p for %s %s\n" (id_to_string id) (constraints_to_string cs_p) in*)
 (*	let _ = Printf.printf "about to check that %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*)
 	let t', _ = type_consistent (Patt l) d_env false param_t t' in
 	let exp',_,_,cs_e,_,ef = 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 39550cd0..b8731422 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -220,10 +220,28 @@ let tag_to_string = function
   | Alias -> "Alias"
   | Spec -> "Spec"
 
+let rec constraint_to_string = function
+  | LtEq (co,nexp1,nexp2) ->
+    "LtEq(" ^ co_to_string co ^ ", " ^ n_to_string nexp1 ^ ", " ^ n_to_string nexp2 ^ ")"
+  | Eq (co,nexp1,nexp2) ->
+    "Eq(" ^ co_to_string co ^ ", " ^ n_to_string nexp1 ^ ", " ^ n_to_string nexp2 ^ ")"
+  | GtEq (co,nexp1,nexp2) ->
+    "GtEq(" ^ co_to_string co ^ ", " ^ n_to_string nexp1 ^ ", " ^ n_to_string nexp2 ^ ")"
+  | In(co,var,ints) -> "In of " ^ var
+  | InS(co,n,ints) -> "InS of " ^ n_to_string n
+  | CondCons(co,pats,exps) ->
+    "CondCons(" ^ co_to_string co ^ ", [" ^ constraints_to_string pats ^ "], [" ^ constraints_to_string exps ^ "])"
+  | BranchCons(co,consts) ->
+    "BranchCons(" ^ co_to_string co ^ ", [" ^ constraints_to_string consts ^ "])"
+and constraints_to_string = function
+  | [] -> ""
+  | [c] -> constraint_to_string c
+  | c::cs -> (constraint_to_string c) ^ "; " ^ (constraints_to_string cs)
+
 let rec tannot_to_string = function
   | NoTyp -> "No tannot"
   | Base((vars,t),tag,ncs,ef,bv) ->
-    "Tannot: type = " ^ (t_to_string t) ^ " tag = " ^ tag_to_string tag ^ " constraints = not printing effect = " ^ e_to_string ef ^ "boundv = not printing"
+    "Tannot: type = " ^ (t_to_string t) ^ " tag = " ^ tag_to_string tag ^ " constraints = " ^ constraints_to_string ncs ^ " effect = " ^ e_to_string ef ^ "boundv = not printing"
   | Overload(poly,_,variants) ->
     "Overloaded: poly = " ^ tannot_to_string poly
 
@@ -1932,6 +1950,7 @@ let rec type_consistent_internal co d_env widen t1 cs1 t2 cs2 =
 	     ({t=Tapp("range",[TA_nexp nu1;TA_nexp nu2])},
 	      csp@[LtEq(co,nu1,a1);LtEq(co,nu1,a2);LtEq(co,a1,nu2);LtEq(co,a2,nu2)]))
   | Tapp(id1,args1), Tapp(id2,args2) ->
+    (*let _ = Printf.printf "checking consistency of %s and %s\n" id1 id2 in*)
     let la1,la2 = List.length args1, List.length args2 in
     if id1=id2 && la1 = la2 
     then (t2,csp@(List.flatten (List.map2 (type_arg_eq co d_env widen) args1 args2)))
@@ -2321,7 +2340,7 @@ let rec simple_constraint_check in_env cs =
 	      | _ -> Some(Eq(co,n1',n2')))
 	  | _ -> Some(Eq(co,n1',n2')))) in
     (match contains_in_vars in_env n1, contains_in_vars in_env n2 with
-      | None,None ->	
+      | _,_ ->	
 	(match check_eq true n1 n2 with
 	  | None -> (check cs)
 	  | Some(c) -> c::(check cs))
@@ -2372,7 +2391,7 @@ let rec simple_constraint_check in_env cs =
       | [],[] -> check cs
       | _     -> CondCons(co,pats',exps')::(check cs))
   | BranchCons(co,branches)::cs ->
-(*    let _ = Printf.printf "Branchcons check length branches %i\n" (List.length branches) in*)
+    (*let _ = Printf.printf "Branchcons check length branches %i\n" (List.length branches) in*)
     let b' = check branches in
     if [] = b' 
     then check cs
@@ -2392,12 +2411,12 @@ let rec constraint_size = function
 let do_resolve_constraints = ref true
 
 let resolve_constraints cs = 
-(*  let _ = Printf.printf "called resolve constraints with %i constraints\n" (constraint_size cs) in*)
+  (*let _ = Printf.printf "called resolve constraints with %i constraints\n" (constraint_size cs) in*)
   if not !do_resolve_constraints
   then cs
   else
     let rec fix len cs =
-(*      let _ = Printf.printf "Calling simple constraint check, fix check point is %i\n" len in *)
+      (*let _ = Printf.printf "Calling simple constraint check, fix check point is %i\n" len in *)
       let cs' = simple_constraint_check (in_constraint_env cs) cs in
       let len' = constraint_size cs' in
       if len > len' then fix len' cs'
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 00d1faa1..adfd0cbe 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -167,6 +167,7 @@ val cons_bs_annot : t -> nexp_range list -> bounds_env -> tannot
 
 val t_to_string : t -> string
 val n_to_string : nexp -> string
+val constraints_to_string : nexp_range list -> string
 val tannot_to_string : tannot -> string
 val t_to_typ : t -> Ast.typ