Add new type checking file. Small changes to type inference, temporary change to printing

5 files changed, 870 insertions, 11 deletions

diff --git a/src/lem_interp/extract.mllib b/src/lem_interp/extract.mllib
index 467a15ea..c0cfb441 100644
--- a/src/lem_interp/extract.mllib
+++ b/src/lem_interp/extract.mllib
@@ -7,6 +7,8 @@ Interp_lib
 Interp_interface
 Interp_inter_imp
 
+Type_check
+
 Pretty_interp
 Printing_functions
 Run_interp_model
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 4f5fb479..373b7ab2 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -941,11 +941,33 @@ let rec combine_typs ts =
     let t' = combine_typs ts in
     match (t,t') with 
       | (_,T_var _) -> t
-      | ((T_app "range" (T_args [T_arg_nexp (Ne_const n1); T_arg_nexp (Ne_const r1)])),
-         (T_app "range" (T_args [T_arg_nexp (Ne_const n2); T_arg_nexp (Ne_const r2)]))) ->
-        let (smaller,larger,larger_r) = if n1 < n2 then (n1,n2,r2) else (n2,n1,r1) in
-        let r = (larger + larger_r) - smaller in
-        T_app "range" (T_args [T_arg_nexp (Ne_const smaller); T_arg_nexp (Ne_const r)])
+      | ((T_app "range" (T_args [T_arg_nexp (Ne_const bot1); T_arg_nexp (Ne_const top1)])),
+         (T_app "range" (T_args [T_arg_nexp (Ne_const bot2); T_arg_nexp (Ne_const top2)]))) ->
+        let (smallest,largest) =
+          if bot1 <= bot2
+          then if top1 <= top2 then (bot1, top2) else (bot1, top1)
+          else if top1 <= top2 then (bot2, top2) else (bot2, top1) in
+        T_app "range" (T_args [T_arg_nexp (Ne_const smallest); T_arg_nexp (Ne_const largest)])
+      | ((T_app "atom" (T_args [T_arg_nexp (Ne_const a1);])), (T_app "atom" (T_args [T_arg_nexp (Ne_const a2);]))) ->
+        if a1 = a2
+        then t
+        else
+          let (smaller,larger) = if a1 < a2 then (a1,a2) else (a2,a1) in
+          T_app "range" (T_args [T_arg_nexp (Ne_const smaller); T_arg_nexp (Ne_const larger)])
+      | (T_app "range" (T_args [T_arg_nexp (Ne_const bot); T_arg_nexp (Ne_const top)]),
+         T_app "atom" (T_args [T_arg_nexp (Ne_const a)])) ->
+        if bot <= a && a <= top
+        then t
+        else if bot <= a && top <= a
+        then T_app "range" (T_args [T_arg_nexp (Ne_const bot); T_arg_nexp (Ne_const a)])
+        else T_app "range" (T_args [T_arg_nexp (Ne_const a); T_arg_nexp (Ne_const top)])
+      | (T_app "atom" (T_args [T_arg_nexp (Ne_const a)]),
+         T_app "range" (T_args [T_arg_nexp (Ne_const bot); T_arg_nexp (Ne_const top)])) ->
+        if bot <= a && a <= top
+        then t
+        else if bot <= a && top <= a
+        then T_app "range" (T_args [T_arg_nexp (Ne_const bot); T_arg_nexp (Ne_const a)])
+        else T_app "range" (T_args [T_arg_nexp (Ne_const a); T_arg_nexp (Ne_const top)])        
       | ((T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); 
                                    T_arg_order (Ord_aux o1 _); T_arg_typ t1])),
          (T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); 
@@ -980,12 +1002,12 @@ let rec val_typ v =
     | V_lit (L_aux lit _) ->
       match lit with
         | L_unit -> T_id "unit"
-        | L_true -> T_id "bool"
-        | L_false -> T_id "bool"
+        | L_true -> T_id "bit"
+        | L_false -> T_id "bit"
         | L_one -> T_id "bit"
         | L_zero -> T_id "bit"
         | L_string _ -> T_id "string"
-        | L_num n -> T_app "range" (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const 0)])
+        | L_num n -> T_app "atom" (T_args [T_arg_nexp (Ne_const n);])
         | L_undef -> T_var "fresh"
         | L_hex _ -> Assert_extra.failwith "literal hex not removed"
         | L_bin _ -> Assert_extra.failwith "literal bin not removed"
diff --git a/src/lem_interp/type_check.lem b/src/lem_interp/type_check.lem
new file mode 100644
index 00000000..ec8e46bc
--- /dev/null
+++ b/src/lem_interp/type_check.lem
@@ -0,0 +1,820 @@
+open import Pervasives
+import Map
+import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *)
+import Set_extra (* For 'to_list' because map only goes to set *)
+import List_extra (* For 'nth' and 'head' where we know that they cannot fail *)
+open import Show_extra (* for 'show' to convert nat to string) *)
+open import String_extra (* for chr *)
+import Assert_extra (*For failwith when partiality is known to be unreachable*)
+
+open import Sail_impl_base
+open import Interp_ast
+open import Interp_utilities
+open import Instruction_extractor
+
+type tannot = Interp_utilities.tannot
+
+(*Env of t counter, nexp counter, order counter, type env, order env, nexp env, nec env*)
+type envs = | Env of nat * nat * nat * map string (t * nec) * map string order * map string ne * map string nec
+
+let union_envs (orig_envs : envs) (branch_envs : list envs) : envs = orig_envs
+
+let t_fresh envs =
+  let (Env t_count ne_count o_count t_env o_env ne_env nec_env) = envs in
+  (T_var ("fresh_" ^ show t_count),(Env (t_count + 1) ne_count o_count t_env o_env ne_env nec_env))
+let nexp_fresh envs =
+  let (Env t_count ne_count o_count t_env o_env ne_env nec_env) = envs in
+  (Ne_var ("fresh_" ^ show ne_count),(Env t_count (ne_count + 1) o_count t_env o_env ne_env nec_env))
+let ord_fresh envs =
+  let (Env t_count ne_count o_count t_env o_env ne_env nec_env) = envs in
+  (Ord_aux (Ord_var (Kid_aux (Var ("fresh" ^ show o_count)) Unknown)) Unknown,
+   (Env t_count ne_count (o_count + 1) t_env o_env ne_env nec_env))
+
+let get_nexp envs n =
+  let (Env t_count ne_count o_count t_env o_env ne_env nec_env) = envs in
+  Map.lookup n ne_env
+let update_nexp envs n ne =
+  let (Env t_count ne_count o_count t_env o_env ne_env nec_env) = envs in
+  Env t_count ne_count o_count t_env o_env (Map.insert n ne ne_env) nec_env
+
+let get_typ envs t =
+  let (Env t_count ne_count o_count t_env o_env ne_env nec_env) = envs in
+  Map.lookup t t_env
+let update_t envs t ty nec =
+  let (Env t_count ne_count o_count t_env o_env ne_env nec_env) = envs in
+  Env t_count ne_count o_count (Map.insert t (ty, nec) t_env) o_env ne_env nec_env
+
+let get_ord (envs : envs) (o :string) =
+  let (Env t_count ne_count o_count t_env (o_env : map string order) ne_env nec_env) = envs in
+  Map.lookup o o_env
+let update_ord envs o ord =
+  let (Env t_count ne_count o_count t_env o_env ne_env nec_env) = envs in
+  Env t_count ne_count o_count t_env (Map.insert o ord o_env) ne_env nec_env
+
+let get_nec envs n =
+  let (Env t_count ne_count o_count t_env o_env ne_env nec_env) = envs in
+  Map.lookup nec_env n
+let update_nec envs n nc =
+  let (Env t_count ne_count o_count t_env o_env ne_env nec_env) = envs in
+  Env t_count ne_count o_count t_env o_env ne_env (Map.insert n nc nec_env)
+
+let rec typ_to_t envs (Typ_aux typ _) = match typ with
+ | Typ_wild -> T_var "fresh"
+ | Typ_id id -> T_id (get_id id)
+ | Typ_var (Kid_aux (Var kid) _) -> T_var kid
+ | Typ_fn ptyp rtyp effect -> T_fn (typ_to_t envs ptyp) (typ_to_t envs rtyp) effect
+ | Typ_tup typs -> T_tup (List.map (typ_to_t envs) typs)
+ | Typ_app id typ_args -> T_app (get_id id) (T_args [])
+end  
+
+let rec pow_i (i:integer) (n:integer) : integer =
+  match (natFromInteger n) with 
+  | 0 -> 1
+  | n -> i * (pow_i i (integerFromNat (n-1)))
+end
+let two_pow = pow_i 2
+
+let n_zero = Ne_const 0
+let n_one = Ne_const 1
+let n_two = Ne_const 2
+
+val debug_print : string -> unit
+declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s
+
+type triple = Yes | No | Maybe
+let triple_negate = function
+  | Yes   -> No
+  | No    -> Yes
+  | Maybe -> Maybe
+end
+
+
+(*Hand translated from Ocaml version*)
+
+let rec compare_nexps n1 n2 =
+  match (n1,n2) with 
+  | (Ne_unary Ne_inf, Ne_unary Ne_inf) -> EQ
+  | (Ne_unary Ne_inf, _              ) -> LT
+  | (_              , Ne_unary Ne_inf) -> GT
+  | (Ne_const n1, Ne_const n2) -> compare n1 n2
+  | (Ne_const _ , _          ) -> LT
+  | (_          , Ne_const _ ) -> GT
+  | (Ne_var i1  , Ne_var i2) -> compare i1 i2
+  | (Ne_var _   , _        ) -> LT
+  | (_          , Ne_var _ ) -> GT 
+  | (Ne_mult n0 n1, Ne_mult n2 n3) -> 
+    (match compare_nexps n0 n2 with
+      | EQ -> compare_nexps n1 n3
+      | a  -> a end)
+  | (Ne_mult _  _ , _          ) -> LT
+  | (_            , Ne_mult _ _) -> GT
+  | (Ne_add[n1;n12],Ne_add [n2;n22]) -> 
+    (match compare_nexps n1 n2 with
+      | EQ -> compare_nexps n12 n22 
+      | a -> a end)
+  | (Ne_add _   , _               ) -> LT
+  | (_          , Ne_add _        ) -> GT
+  | (Ne_minus n1 n12, Ne_minus n2 n22) ->
+    (match compare_nexps n1 n2 with
+      | EQ -> compare_nexps n12 n22
+      | a -> a end)
+  | (Ne_minus _ _  , _             ) -> LT
+  | (_             , Ne_minus _ _  ) -> GT
+  | (Ne_exp n1, Ne_exp n2) -> compare_nexps n1 n2
+  | (Ne_exp _ , _        ) -> LT
+  | (_        , Ne_exp _ ) -> GT
+  | (Ne_unary n1, Ne_unary n2) -> compare_nexps n1 n2
+  | (Ne_unary _ , _          ) -> LT
+  | (_          , Ne_unary _ ) -> GT
+  | (Ne_inf, Ne_inf) -> EQ
+  | (Ne_inf, _     ) -> LT
+  | (_     , Ne_inf) -> GT
+end
+
+let ~{ocaml} neLess b1 b2      = compare_nexps b1 b2 =  LT
+let ~{ocaml} neLessEq b1 b2    = compare_nexps b1 b2 <> GT
+let ~{ocaml} neGreater b1 b2   = compare_nexps b1 b2 =  GT
+let ~{ocaml} neGreaterEq b1 b2 = compare_nexps b1 b2 <> LT
+
+let inline {ocaml} neLess      = defaultLess
+let inline {ocaml} neLessEq    = defaultLessEq
+let inline {ocaml} neGreater   = defaultGreater
+let inline {ocaml} neGreaterEq = defaultGreaterEq
+
+instance (Ord ne)
+  let compare = compare_nexps
+  let (<)  = neLess
+  let (<=) = neLessEq
+  let (>)  = neGreater
+  let (>=) = neGreaterEq
+end
+
+let rec get_var n = match n with
+  | Ne_var _ -> Just n
+  | Ne_exp _ -> Just n
+  | Ne_unary n -> get_var n
+  | Ne_mult _ n1 -> get_var n1
+  | _ -> Nothing
+end
+
+let rec nexp_negative n =
+  match n with
+    | Ne_const i -> if i < 0 then Yes else No
+    | Ne_unary Ne_inf -> Yes
+    | Ne_inf -> No
+    | Ne_exp _ -> No
+    | Ne_var _  -> No
+    | Ne_mult n1 n2 -> (match (nexp_negative n1, nexp_negative n2) with
+        | (Yes,Yes) -> No
+        | (No, No) -> No
+        | (No, Yes) -> Yes
+        | (Yes, No) -> Yes
+        | _ -> Maybe end)
+    | Ne_add [n1;n2] -> (match (nexp_negative n1, nexp_negative n2) with
+        | (Yes,Yes) -> Yes
+        | (No, No) -> No
+        | _ -> Maybe end)
+    | _ -> Maybe
+end
+
+let negate = function
+  | Ne_const i -> Ne_const ((0-1) * i)
+  | n -> Ne_mult (Ne_const (0-1)) n
+end
+
+let increment_factor n i =
+  match n with
+  | Ne_var _ ->
+    (match i with
+     | Ne_const i -> 
+       let ni = i + 1 in
+       if ni = 0 then n_zero else Ne_mult (Ne_const ni) n
+    | _ -> Ne_mult (Ne_add [i; n_one]) n end)
+  | Ne_exp _-> 
+    (match i with
+     | Ne_const i -> 
+       let ni = i + 1 in
+       if ni = 0 then n_zero else Ne_mult (Ne_const ni) n
+    | _ -> Ne_mult (Ne_add [i; n_one]) n end)
+  | Ne_mult n1 n2 ->
+    (match (n1,i) with
+     | (Ne_const i2,Ne_const i) -> 
+      let ni = i + i2 in
+      if ni = 0 then n_zero else Ne_mult (Ne_const(i + i2)) n2
+     | _ -> Ne_mult (Ne_add [n1; i]) n2 end)
+  | _ -> n
+  end
+
+let get_factor = function
+  | Ne_var _  -> n_one
+  | Ne_mult n1 _  -> n1
+  | _ -> Assert_extra.failwith "get_factor argument not normalized"
+end
+
+let rec normalize_n_rec recur_ok n =
+  match n with
+  | Ne_const _ -> n
+  | Ne_var _ -> n
+  | Ne_inf -> n
+  | Ne_unary n -> 
+    let (n',to_recur,add_neg) =
+      (match n with
+       | Ne_const i -> (negate n,false,false)
+       | Ne_add [n1;n2] -> (Ne_add [negate n1; negate n2],true,false)
+       | Ne_minus n1 n2 -> (Ne_minus n2 n1,true,false)
+       | Ne_unary n -> (n,true,false)
+       | _ -> (n,true,true) end) in
+    if to_recur 
+    then (let n' = normalize_n_rec true n' in
+          if add_neg 
+          then negate n'
+          else n')
+    else n'
+  | Ne_exp n    -> 
+    let n' = normalize_n_rec true n in
+    (match n' with
+    | Ne_const i -> Ne_const (two_pow i)
+    | _ -> Ne_exp n' end)
+  | Ne_add [n1;n2] ->
+    let (n1',n2') = (normalize_n_rec true n1, normalize_n_rec true n2) in
+    (match (n1',n2', recur_ok) with
+     | (Ne_unary Ne_inf, Ne_inf,_) -> Assert_extra.failwith "Type inference should have failed"
+     | (Ne_inf, Ne_unary Ne_inf,_) -> Assert_extra.failwith "Type inference should have failed"
+     | (Ne_inf, _,_) -> Ne_inf
+     | (_, Ne_inf, _) -> Ne_inf
+     | (Ne_unary Ne_inf, _,_) -> Ne_unary Ne_inf
+     | (_, Ne_unary Ne_inf, _) -> Ne_unary Ne_inf 
+     | (Ne_const i1, Ne_const i2,_) -> Ne_const (i1 + i2)
+     | (Ne_add [n11;n12], Ne_const i, true) -> 
+       if (i = 0)
+       then n1' 
+       else normalize_n_rec false (Ne_add [n11; (normalize_n_rec false (Ne_add [n12; n2']))])
+     | (Ne_add [n11;n12], Ne_const i, false) ->
+       if i = 0 then n1'
+       else Ne_add [n11; (normalize_n_rec false (Ne_add [n12; n2']))]
+     | (Ne_const i, Ne_add[n21;n22], true) -> 
+       if i = 0 then n2' 
+       else normalize_n_rec false (Ne_add [n21; (normalize_n_rec false (Ne_add [n22; n1']))])
+    | (Ne_const i, Ne_add [n21;n22], false) ->
+      if (i = 0) then n2'
+      else Ne_add [n21; (normalize_n_rec false (Ne_add [n22; n1']))]
+    | (Ne_const i, _,_) -> if i = 0 then n2' else Ne_add [n2'; n1']
+    | (_, Ne_const i,_) -> if i = 0 then n1' else Ne_add [n1'; n2']
+    | (Ne_add [n11;n12], Ne_add[n21;n22], true) ->
+      (match compare_nexps n11 n21 with
+       | GT -> normalize_n_rec false (Ne_add [n21; (normalize_n_rec false (Ne_add [n22; n1']))])
+       | EQ -> 
+         (match compare_nexps n12 n22 with
+          | GT -> normalize_n_rec true (Ne_add [(Ne_mult n_two n11); (Ne_add [n12; n22])])
+          | EQ -> normalize_n_rec true (Ne_add [(Ne_mult n_two n11); (Ne_mult n_two n12)])
+          | _ -> normalize_n_rec true (Ne_add [(Ne_mult n_two n11); (Ne_add [n22; n12])]) end)
+      | _  -> normalize_n_rec false (Ne_add [n11; (normalize_n_rec false (Ne_add [n12; n2']))])end)
+    | (Ne_add[n11;n12], Ne_add[n21;n22], false) ->
+      (match compare_nexps n11 n21 with
+       | GT -> Ne_add [n21; (normalize_n_rec false (Ne_add [n22; n1']))]
+       | EQ  -> 
+         (match compare_nexps n12 n22 with
+          | GT -> normalize_n_rec true (Ne_add [(Ne_mult n_two n11); (Ne_add [n12; n22])])           
+          | EQ -> normalize_n_rec true (Ne_add [(Ne_mult n_two n11); (Ne_mult n_two n12)])
+          | _ -> normalize_n_rec true (Ne_add [(Ne_mult n_two n11); (Ne_add [n22; n12])]) end)
+       | _  -> Ne_add [n11; (normalize_n_rec false (Ne_add [n12; n2']))] end)
+    | (Ne_exp n11, Ne_exp n21,_) -> 
+      (match compare_nexps n11 n21 with
+      | GT -> Ne_add [n1'; n2']
+      | EQ -> Ne_exp (normalize_n_rec true (Ne_add [n11; n_one]))
+      | _ -> Ne_add [ n2'; n1'] end)
+    | (Ne_exp n11,Ne_add[n21;n22],_) ->
+      (match n21 with
+        | Ne_exp n211 ->
+          (match compare_nexps n11 n211 with
+           | GT -> Ne_add [n21; (normalize_n_rec true (Ne_add [n11; n22]))]
+           | EQ -> Ne_add [(Ne_exp (normalize_n_rec true (Ne_add [n11; n_one]))); n22]
+           | _ -> Ne_add [n1'; n2'] end)
+        | _ -> Ne_add [n1'; n2'] end)
+    | (Ne_add [n11;n12],Ne_exp n21,_) ->
+      (match n11 with
+       | Ne_exp n111 ->
+         (match compare_nexps n111 n21 with
+          | GT -> Ne_add [n2'; n1']
+          | EQ -> Ne_add [(Ne_exp (normalize_n_rec true (Ne_add [n111; n_one]))); n12]
+          | _ -> Ne_add [n11; (normalize_n_rec true (Ne_add [n2'; n12]))] end)
+        | _ -> Ne_add [n2'; n1'] end)
+    | _ -> 
+      (match (get_var n1', get_var n2') with
+      | (Just nv1,Just nv2) ->
+        (match compare_nexps nv1 nv2 with
+         | GT -> Ne_add [n1'; n2']
+         | EQ -> increment_factor n1' (get_factor n2')
+         |  _ -> Ne_add  [n2'; n1'] end)
+      | (Just (nv1),Nothing) -> Ne_add [n2'; n1']
+      | (Nothing,Just(nv2)) -> Ne_add [n1'; n2']
+      | _ -> (match (n1',n2') with
+          | (Ne_add[n11';n12'], _) -> 
+            (match compare_nexps n11' n2' with
+              | GT -> Ne_add [n11'; (normalize_n_rec true (Ne_add [n12'; n2']))]
+              | EQ -> Assert_extra.failwith "Neither term has var but are the same?"
+              | _ -> Ne_add [n2';n1'] end)
+          | (_, Ne_add[n21';n22']) ->
+            (match compare_nexps n1' n21' with
+              | GT -> Ne_add [n1'; n2']
+              | EQ -> Assert_extra.failwith "Unexpected equality"
+              | _ -> Ne_add [n21'; (normalize_n_rec true (Ne_add [n1'; n22']))] end)
+          | _ -> 
+            (match compare_nexps n1' n2' with
+              | GT -> Ne_add [n1'; n2']
+              | EQ -> normalize_n_rec true (Ne_mult n_two n1')
+              | _ -> Ne_add [n2'; n1'] end) end) end) end)
+  | Ne_minus n1 n2 ->
+    let (n1',n2') = (normalize_n_rec true n1, normalize_n_rec true n2) in
+    (match (n1',n2') with
+     | (Ne_unary Ne_inf, Ne_inf) -> Assert_extra.failwith "Type checker should have caught"
+     | (Ne_inf, Ne_unary Ne_inf) -> Assert_extra.failwith "Type checker should have caught"
+     | (Ne_inf, _) -> Ne_inf
+     | (_,Ne_unary Ne_inf) -> Ne_inf
+     | (Ne_unary Ne_inf, _) -> Ne_unary Ne_inf
+     | (_,Ne_inf) -> Ne_unary Ne_inf 
+     | (Ne_const i1, Ne_const i2) -> Ne_const (i1 - i2)
+     | (Ne_const i, _) -> 
+       if (i = 0) 
+       then normalize_n_rec true (negate n2') 
+       else normalize_n_rec true (Ne_add [(negate n2'); n1'])
+     | (_, Ne_const i) -> 
+       if (i = 0) 
+       then n1' 
+       else normalize_n_rec true (Ne_add [n1'; (Ne_const ((0 - 1) * i))])
+     | (_,_) -> 
+       (match compare_nexps n1 n2 with
+        |  EQ -> n_zero
+        |  GT -> Ne_add [n1'; (negate n2')]
+        | _ -> Ne_add [(negate n2'); n1'] end) end)
+  | Ne_mult n1 n2 ->
+    let (n1',n2') = (normalize_n_rec true n1, normalize_n_rec true n2) in
+    (match (n1',n2') with
+     | (Ne_unary Ne_inf,Ne_unary Ne_inf) -> Ne_inf
+     | (Ne_inf, Ne_const i) -> if i = 0 then Ne_const 0 else Ne_inf
+     | (Ne_const i, Ne_inf) -> if i = 0 then Ne_const 0 else Ne_inf
+     | (Ne_unary Ne_inf, Ne_const i) ->
+       if i = 0 then Ne_const 0
+       else if i < 0 then Ne_inf
+       else Ne_unary Ne_inf
+     | (Ne_const i, Ne_unary Ne_inf) ->
+       if i = 0 then Ne_const 0 
+       else if i < 0 then Ne_inf
+       else Ne_unary Ne_inf
+     | (Ne_unary Ne_inf, _) ->
+       (match nexp_negative n2 with
+        | Yes -> Ne_inf
+        | _ ->  Ne_unary Ne_inf end)
+     | (_, Ne_unary Ne_inf) ->
+       (match nexp_negative n1 with
+        | Yes -> Ne_inf
+        | _ ->  Ne_unary Ne_inf end)
+      | (Ne_inf, _) ->
+        (match nexp_negative n2 with
+        | Yes -> Ne_unary Ne_inf
+        | _  -> Ne_inf end)
+      | (_, Ne_inf) ->
+        (match nexp_negative n1 with
+        | Yes -> Ne_unary Ne_inf
+        | _  -> Ne_inf end)
+     | (Ne_const i1, Ne_const i2) -> Ne_const (i1 * i2)
+     | (Ne_const i1, Ne_exp n) ->
+       if i1 = 2
+       then Ne_exp (normalize_n_rec true (Ne_add [n;n_one]))
+       else Ne_mult n1' n2'
+     | (Ne_exp n, Ne_const i1) ->
+       if i1 = 2
+       then Ne_exp (normalize_n_rec true (Ne_add [n; n_one]))
+       else Ne_mult n2' n1'
+     | (Ne_mult _ _, Ne_var _) -> Ne_mult n1' n2'
+     | (Ne_exp n1, Ne_exp n2) -> Ne_exp (normalize_n_rec true (Ne_add [n1; n2]))
+     | (Ne_exp _, Ne_var _) -> Ne_mult n2' n1'
+     | (Ne_exp _, Ne_mult _ _) -> Ne_mult n2' n1'
+     | (Ne_var _, Ne_var _) ->
+      (match compare n1' n2' with
+      | EQ -> Ne_mult n1' n2'
+      | GT -> Ne_mult n1' n2'
+      | _ -> Ne_mult n2' n1' end)
+     | (Ne_const _, Ne_add [n21;n22]) ->
+       normalize_n_rec true (Ne_add [(Ne_mult n1' n21); (Ne_mult n1' n21)])
+     | (Ne_var _,Ne_add [n21;n22]) ->
+       normalize_n_rec true (Ne_add [(Ne_mult n1' n21); (Ne_mult n1' n21)])
+     | (Ne_exp _, Ne_add[n21;n22]) ->
+       normalize_n_rec true (Ne_add [(Ne_mult n1' n21); (Ne_mult n1' n21)])
+     | (Ne_mult _ _, Ne_add[n21;n22]) ->
+       normalize_n_rec true (Ne_add [(Ne_mult n1' n21); (Ne_mult n1' n21)])
+     | (Ne_add[n11;n12],Ne_const _) ->
+       normalize_n_rec true (Ne_add [(Ne_mult n11 n2'); (Ne_mult n12 n2')])
+     | (Ne_add [n11;n12],Ne_var _) ->
+       normalize_n_rec true (Ne_add [(Ne_mult n11 n2'); (Ne_mult n12 n2')])
+     | (Ne_add([n11;n12]), Ne_exp _) ->
+       normalize_n_rec true (Ne_add [(Ne_mult n11 n2'); (Ne_mult n12 n2')])
+     | (Ne_add [n11;n12], Ne_mult _ _) ->
+       normalize_n_rec true (Ne_add [(Ne_mult n11 n2'); (Ne_mult n12 n2')])
+     | (Ne_mult n11 n12 , Ne_const _) ->
+      normalize_n_rec false (Ne_mult (Ne_mult n11 n2') (Ne_mult n12 n2'))
+     | (Ne_const i1, _) ->
+       if (i1 = 0) then n1'
+       else if (i1 = 1) then n2'
+       else Ne_mult n1' n2'
+     | (_, Ne_const i1) ->
+       if (i1 = 0) then n2'
+       else if (i1 = 1) then n1'
+       else Ne_mult n2' n1'
+     | (Ne_add [n11;n12],Ne_add [n21;n22]) ->
+       normalize_n_rec true (Ne_add [(Ne_mult n11 n21);
+                                     (Ne_add [(Ne_mult n11 n22);
+                                              (Ne_add [(Ne_mult n12 n21); (Ne_mult n12 n22)])])])
+     | (Ne_mult _ _, Ne_exp _) -> Ne_mult n1' n2' 
+     | (Ne_var _, Ne_mult n1 n2) -> 
+       (match (get_var n1, get_var n2) with
+        | (Just(nv1),Just(nv2)) ->
+          (match compare_nexps nv1 nv2 with
+           | EQ    -> Ne_mult n1 (Ne_mult nv1 nv1)
+           | GT    -> Ne_mult (normalize_n_rec true (Ne_mult n1 n1')) n2
+           | _  -> Ne_mult n2' n1' end)
+        | _ -> Ne_mult (normalize_n_rec true (Ne_mult n1 n1')) n2 end)
+    | (Ne_var _, Ne_exp _) -> Ne_mult n2' n1'
+    | (Ne_mult _ _,Ne_mult n21 n22) -> Ne_mult (Ne_mult n21 n1') (Ne_mult n22 n1')
+    | _ -> Assert_extra.failwith "Normalize hit a case that should have been removed" end)
+end
+
+let normalize_nexp = normalize_n_rec true
+
+let rec range_in_range envs (recur1,recur2,recur3,recur4) act_bot act_top exp_bot exp_top =
+  let (act_bot,act_top,exp_bot,exp_top) =
+    if recur1 && recur2 && recur3 && recur4
+    then (normalize_nexp act_bot, normalize_nexp act_top, normalize_nexp exp_bot, normalize_nexp exp_top)
+    else (act_bot,act_top,exp_bot,exp_top)
+  in
+  match (act_bot,recur1,act_top,recur2,exp_bot,recur3,exp_top,recur4) with
+  | (Ne_var i, true, _,_, _,_, _,_) ->
+    (match get_nexp envs i with
+     | Just n -> range_in_range envs (false, recur2,recur3,recur4) n act_top exp_bot exp_top
+     | Nothing -> range_in_range envs (false,recur2,recur3,recur4) act_bot act_top exp_bot exp_top end)
+  | (_, _, Ne_var i, true, _, _, _, _) ->
+    (match get_nexp envs i with
+     | Just n -> range_in_range envs (recur1,false,recur3,recur4) act_bot n exp_bot exp_top
+     | Nothing -> range_in_range envs (recur1,false,recur3,recur4) act_bot act_top exp_bot exp_top end)
+  | (_,_,_,_,Ne_var i,true,_,_) ->
+    (match get_nexp envs i with
+     | Just n -> range_in_range envs (recur1,recur2,false,recur4) act_bot act_top n exp_top
+     | Nothing -> range_in_range envs (recur1,recur2,false,recur4) act_bot act_top exp_bot exp_top end)
+  | (_,_,_,_,_,_,Ne_var i,true) ->
+    (match get_nexp envs i with
+     | Just n -> range_in_range envs (recur1,recur2,recur3,false) act_bot act_top exp_bot n
+     | Nothing -> range_in_range envs (recur1,recur2,recur3,false) act_bot act_top exp_bot exp_top end)
+  | (Ne_const abi,_, Ne_const ati,_, Ne_const ebi,_, Ne_const ebt,_) ->
+    ebi <= abi && abi <= ebt && ati <= ebt
+  | (Ne_const abi,_, Ne_const ati,_, Ne_unary Ne_inf,_, Ne_inf,_) -> true
+  | (Ne_const abi,_, Ne_const ati,_, Ne_const ebi,_, Ne_inf,_) ->
+    ebi <= abi
+  | (Ne_const abi,_, Ne_const ati,_, Ne_unary Ne_inf,_, Ne_const ebt,_) ->
+    abi <= ebt && ati <= ebt
+  | (Ne_unary Ne_inf,_, Ne_inf,_, Ne_unary Ne_inf,_, Ne_inf,_) -> true
+end 
+  
+let rec single_in_range envs act exp_bot exp_top = 
+  let (act,exp_bot,exp_top) = (normalize_nexp act, normalize_nexp exp_bot, normalize_nexp exp_top) in
+  match (act,exp_bot,exp_top) with
+  | (Ne_const ai, Ne_const ebi, Ne_const eti) ->
+    ebi <= ai && ai <= eti
+  | (Ne_const _, Ne_unary Ne_inf, Ne_inf) -> true
+  | (Ne_const ai, Ne_const ebi, Ne_inf) -> ebi <= ai
+  | (Ne_const ai, Ne_unary Ne_inf, Ne_const eti) -> ai <= eti
+  end
+
+let make_new_range envs start length (Ord_aux order _) =
+  let is_inc = match order with
+    | Ord_inc -> true
+    | Ord_dec -> false
+    | Ord_var (Kid_aux (Var id) _) -> 
+      (match get_ord envs id with
+       | Just (Ord_aux Ord_inc _) -> true
+       | Just (Ord_aux Ord_dec _) -> false
+       | _ -> true (* Default direction is inc *) end) end in
+  let length_n = match (normalize_nexp length) with
+    | Ne_var i -> (match get_nexp envs i with
+        | Just n -> n
+        | Nothing -> Assert_extra.failwith "Vector type has no length" end)
+   | n -> n end in
+  let start_n = match (normalize_nexp start) with
+    | Ne_var i -> (match get_nexp envs i with
+        | Just n -> n
+        | Nothing -> if is_inc then Ne_const 0 else (Ne_minus length_n n_one) end)
+    | n -> n end in
+  if is_inc
+  then T_app "range" (T_args [T_arg_nexp start;T_arg_nexp (Ne_minus (Ne_add [start;length]) n_one)])
+  else T_app "range" (T_args [T_arg_nexp (Ne_add [(Ne_minus start_n length_n);n_one]); T_arg_nexp start])
+
+let consistent_eff eff1 eff2 = true
+
+let rec consistent_typ envs (typ_actual :t) (typ_allowed : t) =
+  match (typ_actual,typ_allowed) with
+  | (T_abbrev ta _, T_abbrev tb _) -> consistent_typ envs ta tb
+  | (T_abbrev ta _, t) -> consistent_typ envs ta t
+  | (t, T_abbrev tb _) -> consistent_typ envs t tb
+  | (T_id x, T_id y) -> (x=y, envs)
+  | (T_fn act_parms act_ret act_eff, T_fn all_parms all_ret all_eff) ->
+    let (consistent,envs) = consistent_typ envs act_parms all_parms in
+    if consistent
+    then let (consistent,envs) = consistent_typ envs act_ret all_ret in
+      if consistent
+      then (consistent_eff act_eff all_eff, envs)
+      else (false,envs)
+    else (false,envs)
+  | (T_tup act_tups, T_tup all_tups) ->
+    if List.length act_tups = List.length all_tups
+    then consistent_typ_list envs act_tups all_tups
+    else (false,envs)
+  | (T_app "range" (T_args [T_arg_nexp low;T_arg_nexp high]),
+     T_app "range" (T_args [T_arg_nexp all_low;T_arg_nexp all_high])) ->
+    (range_in_range envs (true,true,true,true) low high all_low all_high,envs)
+  | (T_app "range" (T_args [T_arg_nexp low;T_arg_nexp high]),
+     T_app "atom" (T_args [T_arg_nexp all])) ->
+    (false,envs)
+  | (T_app "atom" (T_args [T_arg_nexp act]), T_app "range" (T_args [T_arg_nexp low; T_arg_nexp high])) ->
+    (single_in_range envs act low high,envs)
+  | (T_app "atom" (T_args [T_arg_nexp act]), T_app "atom" (T_args [T_arg_nexp all])) ->
+    (false,envs)
+  | (T_app "vector" (T_args [T_arg_nexp start; T_arg_nexp size; T_arg_order dir; T_arg_typ t]),
+     T_app "vector" (T_args [T_arg_nexp sta;   T_arg_nexp sia ; T_arg_order da ; T_arg_typ ta])) ->
+    let (consistent,envs) = consistent_nexp envs start sta in
+    if consistent then
+      let (consistent,envs) = consistent_nexp envs size sia in
+      if consistent then
+        if dir = da
+        then consistent_typ envs t ta
+        else (false,envs)
+      else (false,envs)
+    else (false,envs)
+  | (T_app x (T_args args_act), T_app y (T_args args_all)) ->
+    if x = y && List.length args_act = List.length args_all
+    then consistent_typ_arg_list envs args_act args_all
+    else (false, envs)
+  | (T_var x, T_var y) -> (x = y,envs)
+  | _ -> (false,envs)
+end
+
+and
+  consistent_nexp envs n_acc n_all =
+  let (n_acc,n_all) = (normalize_nexp n_acc,normalize_nexp n_all) in
+  match (n_acc,n_all) with
+  | (Ne_const iac, Ne_const ial) -> (iac = ial, envs)
+  | (Ne_exp nac, Ne_exp nal) -> consistent_nexp envs nac nal
+  | (_, Ne_inf) -> (true,envs)
+  | (Ne_var i, _) -> (true,envs)
+  | (_, Ne_var i) -> (true,envs)
+  | _ -> (true,envs)
+end
+
+and consistent_typ_list envs t_accs t_alls =
+    match (t_accs,t_alls) with
+    | ([],[]) -> (true,envs)
+    | (t_acc::t_accs,t_all::t_alls) ->
+      let (consistent,envs) = consistent_typ envs t_acc t_all in
+      if consistent
+      then consistent_typ_list envs t_accs t_alls
+      else (false,envs)
+    | _ -> (false,envs)
+end
+
+and consistent_typ_arg_list envs t_accs t_alls =
+    let arg_check t_acc t_all =
+      match (t_acc,t_all) with
+      | (T_arg_typ tacc,T_arg_typ tall) -> consistent_typ envs tacc tall
+      | (T_arg_nexp nacc,T_arg_nexp nall) -> consistent_nexp envs nacc nall
+      | (T_arg_order oacc, T_arg_order oall) -> (oacc=oall,envs)
+      | (T_arg_effect eacc, T_arg_effect eall) -> (consistent_eff eacc eall, envs)
+    end in
+    match (t_accs,t_alls) with
+    | ([],[]) -> (true,envs)
+    | (ta::tas,t::ts) ->
+      let (consistent,envs) = arg_check ta t in
+      if consistent
+      then consistent_typ_arg_list envs tas ts
+      else (false,envs)
+    | _ -> (false,envs)
+end
+
+let mk_atom n = T_app "atom" (T_args [T_arg_nexp (Ne_const n)])
+
+let check_lit envs typ (L_aux lit loc) =
+  match lit with
+  | L_num n -> consistent_typ envs (mk_atom n) typ
+  | L_zero -> consistent_typ envs (T_id "bit") typ
+  | L_one -> consistent_typ envs (T_id "bit") typ
+  | L_string _ -> consistent_typ envs (T_id "string") typ
+  | L_undef -> (true,envs)
+  | _ -> (false,envs)
+end
+
+let rec check_exp envs ret_typ exp_typ (E_aux exp (l,annot)) =
+  let (typ,tag,ncs,effect,reffect) = match annot with 
+    | Nothing ->
+      (T_var "fresh_v", Tag_empty,[],(Effect_aux (Effect_set []) Unknown),(Effect_aux (Effect_set []) Unknown))
+    | Just(t, tag, ncs, ef,efr) -> (t,tag,ncs,ef,efr) end in
+  match exp with
+    | E_block exps -> check_block envs envs true ret_typ exp_typ exps
+    | E_nondet exps -> check_block envs envs false ret_typ exp_typ exps
+    | E_id id ->
+      (match get_typ envs (get_id id) with
+       | Just (t,necs) -> let (consistent,envs) = consistent_typ envs typ t in
+         if consistent
+         then consistent_typ envs typ exp_typ
+         else (false,envs)
+       | Nothing -> (false,envs) end)
+    | E_lit lit ->
+      let (consistent,envs) = check_lit envs exp_typ lit in
+      if consistent
+      then consistent_typ envs typ exp_typ
+      else (false,envs)
+    | E_cast typ exp ->
+      let t = typ_to_t envs typ in
+      let (consistent,envs) = check_exp envs ret_typ t exp in
+      if consistent
+      then consistent_typ envs t exp_typ
+      else (false,envs)
+    | E_app id exps -> (*Need to connect constraints for the function to new type variables in the parms and ret*)
+      (match get_typ envs (get_id id) with
+       | Just ((T_fn parms ret effects),necs) ->
+         (match (parms,exps) with
+          | (T_tup (_::_ as typs), (_::_ as exps)) ->
+            if List.length typs = List.length exps
+            then let (consistent,envs) = List.foldr (fun (exp,typ) (consistent,envs) ->
+                if consistent
+                then check_exp envs ret_typ typ exp
+                else (false,envs)) (true,envs) (List.zip exps typs) in
+              if consistent 
+              then consistent_typ envs ret exp_typ
+              else (false,envs)
+            else (false,envs)
+          | (T_id "unit", []) ->
+            consistent_typ envs ret exp_typ
+          | (T_id "unit", [E_aux (E_lit (L_aux L_unit _)) _]) ->
+            consistent_typ envs ret exp_typ
+          | _ -> (false,envs) end)
+       | _ -> (false, envs) end)
+   | E_app_infix lexp id rexp ->
+      (match get_typ envs (get_id id) with
+        | Just ((T_fn parms ret effects),necs) ->
+          (match parms with
+           | T_tup [ltyp;rtyp] ->
+             let (consistent,envs) = check_exp envs ret_typ ltyp lexp in
+             if consistent then
+               let (consistent,envs) = check_exp envs ret_typ rtyp rexp in
+               if consistent
+               then consistent_typ envs ret exp_typ
+               else (false,envs)
+             else (false,envs)
+           | _ -> (false,envs) end)
+       | _ -> (false, envs) end)
+    | E_tuple exps ->
+      (match (typ,exp_typ) with
+       | (T_tup typs, T_tup e_typs) ->
+         if List.length typs = List.length e_typs && List.length exps = List.length typs
+         then
+           let typ_list = List.zip typs e_typs in
+           let exp_typs_list = List.zip exps typ_list in
+           List.foldr (fun (exp, (typ,e_typ)) (consistent,envs) ->
+               if consistent
+               then let (consistent,envs) = check_exp envs ret_typ e_typ exp in
+                 consistent_typ envs typ e_typ
+               else (false,envs)) (true,envs) exp_typs_list
+         else (false,envs)
+       | _ -> (false,envs) end)
+    | E_if cond t_branch e_branch ->
+      let (consistent,envs) = check_exp envs ret_typ (T_id "bit") cond in
+      if consistent
+      then let (consistent,envs_t) = check_exp envs ret_typ exp_typ t_branch in
+        if consistent
+        then let (consistent,envs_e) = check_exp envs ret_typ exp_typ e_branch in
+          if consistent
+          then consistent_typ (union_envs envs [envs_t; envs_e]) typ exp_typ
+          else (false,envs)
+        else (false,envs)
+      else (false,envs)
+    | E_for id from to_ by ((Ord_aux o _) as order) exp -> (false,envs)
+    | E_vector exps ->
+      (match (typ,exp_typ) with
+       | (T_app "vector" (T_args [T_arg_nexp start; T_arg_nexp length; T_arg_order ord; T_arg_typ typ]),
+          T_app "vector" (T_args [T_arg_nexp strte; T_arg_nexp lenge; T_arg_order orde; T_arg_typ typ_e])) ->
+         let (consistent, envs) = consistent_nexp envs start strte in
+         if consistent then
+           let (consistent, envs) = consistent_nexp envs length lenge in
+           if consistent then
+             let (consistent,envs) = consistent_nexp envs (Ne_const (integerFromNat (List.length exps))) length in
+             if consistent then
+               List.foldr (fun exp (consistent,envs) ->
+                   if consistent
+                   then check_exp envs ret_typ exp_typ exp
+                   else (false,envs)) (true,envs) exps
+             else (false,envs)
+           else (false,envs)
+         else (false,envs)
+       | _ -> (false,envs) end)
+    | E_vector_indexed iexps default -> (false,envs)
+    | E_vector_access vexp aexp ->
+      let (fresh_start,envs) = nexp_fresh envs in
+      let (fresh_length, envs) = nexp_fresh envs in
+      let (fresh_order, envs) = ord_fresh envs in
+      let (consistent,envs) =
+        check_exp envs ret_typ (T_app "vector" (T_args [T_arg_nexp fresh_start; T_arg_nexp fresh_length;
+                                                        T_arg_order fresh_order; T_arg_typ typ])) vexp in
+      if consistent
+      then check_exp envs ret_typ (make_new_range envs fresh_start fresh_length fresh_order) aexp
+      else (false,envs)        
+    | E_vector_subrange vexp sexp eexp ->
+      let (fresh_start,envs) = nexp_fresh envs in
+      let (fresh_length,envs) = nexp_fresh envs in
+      let (fresh_order, envs) = ord_fresh envs in
+      (match (typ,exp_typ) with
+       | (T_app "vector" (T_args [T_arg_nexp sstart; T_arg_nexp sleng; T_arg_order ord; T_arg_typ typ]),
+          T_app "vector" (T_args [T_arg_nexp sse; T_arg_nexp sle; T_arg_order oe; T_arg_typ exp_typ])) ->
+         let (consistent,envs) =
+           check_exp envs ret_typ (T_app "vector" (T_args [T_arg_nexp fresh_start; T_arg_nexp fresh_length;
+                                                           T_arg_order fresh_order; T_arg_typ exp_typ])) vexp in
+         if consistent
+         then let range = make_new_range envs fresh_start fresh_length fresh_order in
+           let (consistent,envs) = check_exp envs ret_typ range sexp in
+           if consistent
+           then check_exp envs ret_typ range eexp (*TODO, make sure that the sub piece is build by the s and e terms*)
+           else (false,envs)
+         else (false,envs)
+       | _ -> (false,envs) end)
+    | E_vector_update vexp aexp nexp -> (false,envs)
+    | E_vector_update_subrange vexp sexp eexp nexp -> (false,envs)
+    | E_vector_append lexp rexp ->
+      (match (typ,exp_typ) with
+       | (T_app "vector" (T_args[T_arg_nexp start;T_arg_nexp length;T_arg_order dir;T_arg_typ t]),
+          T_app "vector" (T_args[T_arg_nexp ste; T_arg_nexp lee; T_arg_order dre; T_arg_typ te])) ->
+         let (startl,envs) = nexp_fresh envs in
+         let (lenl,envs) = nexp_fresh envs in
+         let (startr,envs) = nexp_fresh envs in
+         let (lenr,envs) = nexp_fresh envs in
+         let (consistent,envs) =
+           check_exp envs ret_typ (T_app "vector" (T_args [T_arg_nexp startl;T_arg_nexp lenl;
+                                                           T_arg_order dir; T_arg_typ te])) lexp in
+         if consistent then
+           let (consistent,envs) =
+             check_exp envs ret_typ (T_app "vector" (T_args [T_arg_nexp startr;T_arg_nexp lenr;
+                                                             T_arg_order dir; T_arg_typ te])) rexp in
+           if consistent then
+             let (consistent,envs) = consistent_typ envs typ exp_typ in
+             if consistent
+             then consistent_nexp envs (Ne_add [lenl; lenr]) lee
+             else (false,envs)
+           else (false,envs)
+         else (false,envs)
+       | _ -> (false,envs) end) 
+    | E_list exps ->
+      (match (typ,exp_typ) with
+       | (T_app "list" (T_args [T_arg_typ t]),T_app "list" (T_args [T_arg_typ te])) ->
+         let (consistent,envs) = List.foldr (fun exp (consistent,envs) ->
+             if consistent
+             then check_exp envs ret_typ te exp
+             else (false,envs)) (true,envs) exps in
+         if consistent
+         then consistent_typ envs t te
+         else (false,envs)
+       | _ -> (false,envs) end)
+    | E_cons hexp texp ->
+      (match (typ,exp_typ) with
+       | (T_app "list" (T_args [T_arg_typ t]),T_app "list" (T_args [T_arg_typ te])) ->
+         let (consistent,envs) = check_exp envs ret_typ te hexp in
+         if consistent
+         then let (consistent,envs) = check_exp envs ret_typ exp_typ texp in
+           if consistent
+           then consistent_typ envs t te
+           else (false,envs)
+         else (false,envs)
+       | _ -> (false,envs) end)
+    | E_record fexps -> (false,envs)
+    | E_record_update rexp fexps -> (false,envs)
+    | E_field exp id -> (false,envs)
+    | E_case exp pexps -> (false,envs)
+    | E_let lbind exp -> (false,envs)
+    | E_assign lexp exp -> (false,envs)
+    | E_sizeof nexp -> (false,envs)
+    | E_exit exp -> let (fresh_t,envs) = t_fresh envs in check_exp envs ret_typ fresh_t exp
+    | E_return exp -> check_exp envs ret_typ ret_typ exp
+    | E_assert cond mesg ->
+      let (consistent,envs) = check_exp envs ret_typ (T_id "bit") cond in
+      if consistent then
+        let (consistent,envs) = check_exp envs ret_typ (T_app "option" (T_args[T_arg_typ (T_id "string")])) mesg in
+        if consistent
+        then consistent_typ envs (T_id "unit") exp_typ
+        else (false,envs)
+      else (false,envs)
+    | E_internal_cast tannot exp -> (false,envs)
+    | E_internal_exp tannot -> (false,envs)
+    | E_sizeof_internal tannot -> (false,envs)
+    | E_internal_exp_user tannot tannot2 -> (false,envs)
+    | E_comment msg -> (true,envs)
+    | E_comment_struc exp -> (true,envs)
+    | E_internal_let lexp exp inexp -> (false,envs)
+    | E_internal_plet pat exp inexp -> (false,envs)
+    | E_internal_return exp -> (false,envs)
+end  
+
+and check_block orig_envs envs carry_variables_forward ret_typ exp_typ exps = (false,orig_envs)
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 52e34a38..e0a6edd3 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -65,14 +65,14 @@ let pp_format_var (Kid_aux(Var v,_)) = v
 
 let rec pp_format_l_lem = function
   | Parse_ast.Unknown -> "Unknown"
-  | _ -> "Unknown"
-(*  | Parse_ast.Int(s,None) -> "(Int \"" ^ s ^ "\" Nothing)"
+  (*| _ -> "Unknown"*)
+  | Parse_ast.Int(s,None) -> "(Int \"" ^ s ^ "\" Nothing)"
   | Parse_ast.Int(s,(Some l)) -> "(Int \"" ^  s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))"
   | Parse_ast.Range(p1,p2) -> "(Range \"" ^ p1.Lexing.pos_fname ^ "\" " ^
                                (string_of_int p1.Lexing.pos_lnum) ^ " " ^
                                (string_of_int (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) ^ " " ^
                                (string_of_int p2.Lexing.pos_lnum) ^ " " ^
-                               (string_of_int (p2.Lexing.pos_cnum - p2.Lexing.pos_bol)) ^ ")"*)
+                               (string_of_int (p2.Lexing.pos_cnum - p2.Lexing.pos_bol)) ^ ")"
 
 let pp_lem_l ppf l = base ppf (pp_format_l_lem l)
 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index a5c7e1c2..d3135b0b 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -3553,6 +3553,21 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                                   (l,simple_annot t2))) enums),
              (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
     | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))
+  | Tapp("vector", [TA_nexp _; TA_nexp size; _; TA_typ {t= Tid "bit"}]), Tid(i) ->
+    (match Envmap.apply d_env.enum_env i with
+     | Some(enums) ->
+       let num_enums = List.length enums in
+       (t2,[LtEq(co,Require,mk_sub (mk_2n size) n_one, mk_c_int num_enums)], pure_e,
+        E_aux(E_case (E_aux(E_app((Id_aux(Id "unsigned",l)),[e]),
+                            (l,
+                             tag_annot_efr (mk_range n_zero (mk_sub (mk_2n size) n_one)) (External (Some "unsigned"))
+                               (get_cummulative_effects (get_eannot e)))),
+                      List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)), (l,simple_annot t1)),
+                                                            E_aux(E_id(Id_aux(Id a,l)),
+                                                                  (l, tag_annot t2 (Enum num_enums)))),
+                                                    (l,simple_annot t2))) enums),
+              (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
+     | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))
   | Tapp("atom",[TA_nexp b1]),Tid(i) -> 
     (match Envmap.apply d_env.enum_env i with
       | Some(enums) ->