Porting some minisail changes to sail2 branch

This commit primarily changes how existential types are bound in
letbindings. Essentially, the constraints on both numeric and
existentially quantified types are lifted into the surrounding type
context automatically, so in

```
val f : nat -> nat

let x = f(3)
```

whereas x would have had type nat by default before, it'll now have
type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh
type variable). This has several advantages: x can be passed to
functions expecting an atom argument, such as a vector indexing
operation without any clunky cast functions - ex_int, ex_nat, and
ex_range are no longer required. The let 'x = something() syntax is
also less needed, and is now only really required when we specifically
want a name to refer to x's type. This changes slightly the nature of
the type pattern syntax---whereas previously it was used to cause an
existential to be destructured, it now just provides names for an
automatically destructured binding. Usually however, this just works
the same.

Also:

- Fixed an issue where the rewrite_split_fun_constr_pats rewriting
  pass didn't add type paramemters for newly added type variables in
  generated function parameters.

- Updated string_of_ functions in ast_util to reflect syntax changes

- Fixed a C compilation issue where elements of union type
  constructors were not being coerced between big integers and 64-bit
  integers where appropriate

- Type annotations in patterns now generalise, rather than restrict
  the type of the pattern. This should be safer and easier to handle
  in the various backends. I don't think any code we had was relying
  on this behaviour anyway.

- Add inequality operator to lib/flow.sail

- Fix an issue whereby top-level let bindings with annotations were
  checked incorrectly

5 files changed, 124 insertions, 96 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 97ce3896..09fc9fc9 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -486,7 +486,7 @@ let def_loc = function
 
 let string_of_id = function
   | Id_aux (Id v, _) -> v
-  | Id_aux (DeIid v, _) -> "(deinfix " ^ v ^ ")"
+  | Id_aux (DeIid v, _) -> "(operator " ^ v ^ ")"
 
 let id_of_kid = function
   | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
@@ -528,7 +528,7 @@ let string_of_base_effect_aux = function
 
 let string_of_base_kind_aux = function
   | BK_type -> "Type"
-  | BK_nat -> "Nat"
+  | BK_nat -> "Int"
   | BK_order -> "Order"
 
 let string_of_base_kind (BK_aux (bk, _)) = string_of_base_kind_aux bk
@@ -567,11 +567,11 @@ and string_of_typ_aux = function
   | Typ_id id -> string_of_id id
   | Typ_var kid -> string_of_kid kid
   | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")"
-  | Typ_app (id, args) -> string_of_id id ^ "<" ^ string_of_list ", " string_of_typ_arg args ^ ">"
+  | Typ_app (id, args) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")"
   | Typ_fn (typ_arg, typ_ret, eff) ->
      string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff
   | Typ_exist (kids, nc, typ) ->
-     "exist " ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ
+     "{" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}"
 and string_of_typ_arg = function
   | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg
 and string_of_typ_arg_aux = function
@@ -588,7 +588,7 @@ and string_of_n_constraint = function
   | NC_aux (NC_and (nc1, nc2), _) ->
      "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
   | NC_aux (NC_set (kid, ns), _) ->
-     string_of_kid kid ^ " IN {" ^ string_of_list ", " Big_int.to_string ns ^ "}"
+     string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}"
   | NC_aux (NC_true, _) -> "true"
   | NC_aux (NC_false, _) -> "false"
 
@@ -599,7 +599,7 @@ let string_of_annot = function
 
 let string_of_quant_item_aux = function
   | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid
-  | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> string_of_kind k ^ " " ^ string_of_kid kid
+  | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> "(" ^ string_of_kid kid ^ " :: " ^ string_of_kind k ^ ")"
   | QI_const constr -> string_of_n_constraint constr
 
 let string_of_quant_item = function
@@ -641,7 +641,7 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_app_infix (x, op, y) -> "(" ^ string_of_exp x ^ " " ^ string_of_id op ^ " " ^ string_of_exp y ^ ")"
   | E_tuple exps -> "(" ^ string_of_list ", " string_of_exp exps ^ ")"
   | E_case (exp, cases) ->
-     "switch " ^ string_of_exp exp ^ " { case " ^ string_of_list " case " string_of_pexp cases ^ "}"
+     "match " ^ string_of_exp exp ^ " { " ^ string_of_list ", " string_of_pexp cases ^ " }"
   | E_try (exp, cases) ->
      "try " ^ string_of_exp exp ^ " catch { case " ^ string_of_list " case " string_of_pexp cases ^ "}"
   | E_let (letbind, exp) -> "let " ^ string_of_letbind letbind ^ " in " ^ string_of_exp exp
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 398a0281..6e1083df 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -168,7 +168,7 @@ and sc_op = SC_and | SC_or
 
 and apat =
   | AP_tup of apat list
-  | AP_id of id
+  | AP_id of id * typ
   | AP_global of id * typ
   | AP_app of id * apat
   | AP_cons of apat * apat
@@ -202,8 +202,8 @@ let rec frag_rename from_id to_id = function
 
 let rec apat_bindings = function
   | AP_tup apats -> List.fold_left IdSet.union IdSet.empty (List.map apat_bindings apats)
-  | AP_id id -> IdSet.singleton id
-  | AP_global (id, typ) -> IdSet.empty
+  | AP_id (id, _) -> IdSet.singleton id
+  | AP_global (id, _) -> IdSet.empty
   | AP_app (id, apat) -> apat_bindings apat
   | AP_cons (apat1, apat2) -> IdSet.union (apat_bindings apat1) (apat_bindings apat2)
   | AP_nil -> IdSet.empty
@@ -211,8 +211,8 @@ let rec apat_bindings = function
 
 let rec apat_rename from_id to_id = function
   | AP_tup apats -> AP_tup (List.map (apat_rename from_id to_id) apats)
-  | AP_id id when Id.compare id from_id = 0 -> AP_id to_id
-  | AP_id id -> AP_id id
+  | AP_id (id, typ) when Id.compare id from_id = 0 -> AP_id (to_id, typ)
+  | AP_id (id, typ) -> AP_id (id, typ)
   | AP_global (id, typ) -> AP_global (id, typ)
   | AP_app (ctor, apat) -> AP_app (ctor, apat_rename from_id to_id apat)
   | AP_cons (apat1, apat2) -> AP_cons (apat_rename from_id to_id apat1, apat_rename from_id to_id apat2)
@@ -430,7 +430,7 @@ let rec pp_aexp = function
 
 and pp_apat = function
   | AP_wild -> string "_"
-  | AP_id id -> pp_id id
+  | AP_id (id, typ) -> pp_annot typ (pp_id id)
   | AP_global (id, _) -> pp_id id
   | AP_tup apats -> parens (separate_map (comma ^^ space) pp_apat apats)
   | AP_app (id, apat) -> pp_id id ^^ parens (pp_apat apat)
@@ -484,7 +484,7 @@ let rec split_block = function
 let rec anf_pat ?global:(global=false) (P_aux (p_aux, (l, _)) as pat) =
   match p_aux with
   | P_id id when global -> AP_global (id, pat_typ_of pat)
-  | P_id id -> AP_id id
+  | P_id id -> AP_id (id, pat_typ_of pat)
   | P_wild -> AP_wild
   | P_tup pats -> AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats)
   | P_app (id, [pat]) -> AP_app (id, anf_pat ~global:global pat)
@@ -1544,8 +1544,9 @@ let compile_funcall ctx id args typ =
   (List.rev !setup, final_ctyp, call, !cleanup)
 
 let rec compile_match ctx apat cval case_label =
+  prerr_endline ("Compiling match " ^ Pretty_print_sail.to_string (pp_apat apat) ^ " cval " ^ Pretty_print_sail.to_string (pp_cval cval));
   match apat, cval with
-  | AP_id pid, (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env ->
+  | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env ->
      [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label],
      []
   | AP_global (pid, typ), (frag, ctyp) ->
@@ -1558,15 +1559,21 @@ let rec compile_match ctx apat cval case_label =
           [iconvert (CL_id pid) global_ctyp id ctyp], []
        | _ -> c_error "Cannot compile global letbinding"
        end
-  | AP_id pid, (frag, ctyp) when is_ct_enum ctyp ->
+  | AP_id (pid, _), (frag, ctyp) when is_ct_enum ctyp ->
      begin match Env.lookup_id pid ctx.tc_env with
      | Unbound -> [idecl ctyp pid; icopy (CL_id pid) (frag, ctyp)], []
      | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], []
      end
-  | AP_id pid, _ ->
+  | AP_id (pid, typ), _ ->
      let ctyp = cval_ctyp cval in
-     let init, cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp pid], [iclear ctyp pid] in
-     [idecl ctyp pid] @ init @ [icopy (CL_id pid) cval], cleanup
+     let id_ctyp = ctyp_of_typ ctx typ in
+     let init, cleanup = if is_stack_ctyp id_ctyp then [], [] else [ialloc id_ctyp pid], [iclear id_ctyp pid] in
+     if ctyp_equal id_ctyp ctyp then
+       [idecl ctyp pid] @ init @ [icopy (CL_id pid) cval], cleanup
+     else
+       let gs = gensym () in
+       let gs_init, gs_cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp gs], [iclear ctyp gs] in
+       [idecl id_ctyp pid; idecl ctyp gs] @ init @ gs_init @ [icopy (CL_id gs) cval; iconvert (CL_id pid) id_ctyp gs ctyp] @ gs_cleanup, cleanup
   | AP_tup apats, (frag, ctyp) ->
      begin
        let get_tup n ctyp = (F_field (frag, "ztup" ^ string_of_int n), ctyp) in
@@ -2170,6 +2177,7 @@ let rec compile_def ctx = function
 
   | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) ->
      let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow (pat_ids pat) (anf exp))) in
+     prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp));
      let setup, ctyp, call, cleanup = compile_aexp ctx aexp in
      let fundef_label = label "fundef_fail_" in
      let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
@@ -3333,7 +3341,7 @@ let codegen_def ctx def =
   let lists = List.map (fun ctyp -> codegen_list ctx (unlist ctyp)) lists in
   let vectors = List.filter is_ct_vector (cdef_ctyps ctx def) in
   let vectors = List.map (fun ctyp -> codegen_vector ctx (unvector ctyp)) vectors in
-  (* prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); *)
+  prerr_endline (Pretty_print_sail.to_string (pp_cdef def));
   concat tups
   ^^ concat lists
   ^^ concat vectors
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 75668417..06ee1f65 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1092,13 +1092,14 @@ let generate_initialize_registers vs_ids (Defs defs) =
 let generate_enum_functions vs_ids (Defs defs) =
   let rec gen_enums = function
     | DEF_type (TD_aux (TD_enum (id, _, elems, _), _)) as enum :: defs ->
-       let enum_val_spec name typ =
-         mk_val_spec (VS_val_spec (mk_typschm (mk_typquant []) typ, name, (fun _ -> None), !opt_enum_casts))
+       let enum_val_spec name quants typ =
+         mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, (fun _ -> None), !opt_enum_casts))
        in
-       let enum_range = range_typ (nint 0) (nint (List.length elems - 1)) in
+       let range_constraint kid = nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1))) in
 
        (* Create a function that converts a number to an enum. *)
        let to_enum =
+         let kid = mk_kid "e" in
          let name = append_id id "_of_num" in
          let pexp n id =
            let pat =
@@ -1117,12 +1118,16 @@ let generate_enum_functions vs_ids (Defs defs) =
          let range = range_typ (nint 0) (nint (List.length elems - 1)) in
          if IdSet.mem name vs_ids then []
          else
-           [ enum_val_spec name (function_typ enum_range (mk_typ (Typ_id id)) no_effect);
+           [ enum_val_spec name
+              [mk_qi_id BK_nat kid; mk_qi_nc (range_constraint kid)]
+              (function_typ (atom_typ (nvar kid)) (mk_typ (Typ_id id)) no_effect);
              mk_fundef [funcl] ]
        in
 
        (* Create a function that converts from an enum to a number. *)
        let from_enum =
+         let kid = mk_kid "e" in
+         let to_typ = mk_typ (Typ_exist ([kid], range_constraint kid, atom_typ (nvar kid))) in
          let name = prepend_id "num_of_" id in
          let pexp n id = mk_pexp (Pat_exp (mk_pat (P_id id), mk_lit_exp (L_num (Big_int.of_int n)))) in
          let funcl =
@@ -1132,22 +1137,8 @@ let generate_enum_functions vs_ids (Defs defs) =
          in
          if IdSet.mem name vs_ids then []
          else
-           [ enum_val_spec name (function_typ (mk_typ (Typ_id id)) enum_range no_effect);
+           [ enum_val_spec name [] (function_typ (mk_typ (Typ_id id)) to_typ no_effect);
              mk_fundef [funcl] ]
-         (* This is the simple way to generate this function, but the
-            rewriter and backends are all kinds of broken for function clause
-            patterns.
-         let name = prepend_id "num_of_" id in
-         let funcl n id =
-           mk_funcl name
-             (mk_pat (P_id id))
-             (mk_lit_exp (L_num (Big_int.of_int n)))
-         in
-         if IdSet.mem name vs_ids then []
-         else
-           [ enum_val_spec name (function_typ (mk_typ (Typ_id id)) enum_range no_effect);
-             mk_fundef (List.mapi funcl elems) ]
-          *)
        in
        enum :: to_enum @ from_enum @ gen_enums defs
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 80c339e6..7ea0dadc 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1961,15 +1961,23 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
         no_effect funcls
       in
       let fun_typ = function_typ args_typ ret_typ eff in
+      let quant_new_tyvars qis =
+        let quant_tyvars = List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item qis) in
+        let typ_tyvars = tyvars_of_typ fun_typ in
+        let new_tyvars = KidSet.diff typ_tyvars quant_tyvars in
+        List.map (mk_qi_id BK_nat) (KidSet.elements new_tyvars)
+      in
       let typquant = match typquant with
         | TypQ_aux (TypQ_tq qis, l) ->
            let qis =
              List.filter
                (fun qi -> KidSet.subset (tyvars_of_quant_item qi) (tyvars_of_typ fun_typ))
                qis
+             @ quant_new_tyvars qis
            in
            TypQ_aux (TypQ_tq qis, l)
-        | _ -> typquant
+        | _ ->
+           TypQ_aux (TypQ_tq (List.map (mk_qi_id BK_nat) (KidSet.elements (tyvars_of_typ fun_typ))), l)
       in
       let val_spec =
         VS_aux (VS_val_spec
@@ -3216,6 +3224,7 @@ let rewrite_defs_ocaml = [
   ("simple_assignments", rewrite_simple_assignments);
   ("remove_vector_concat", rewrite_defs_remove_vector_concat);
   ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats);
+  ("remove_numeral_pats", rewrite_defs_remove_numeral_pats);
   ("exp_lift_assign", rewrite_defs_exp_lift_assign);
   ("top_sort_defs", top_sort_defs);
   ("constraint", rewrite_constraint);
diff --git a/src/type_check.ml b/src/type_check.ml
index cc88c159..4b716ba8 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -167,6 +167,11 @@ let string_of_index_sort = function
      ^ string_of_list " & " (fun (x, y) -> string_of_nexp x ^ " <= " ^ string_of_nexp y) constraints
      ^ "}"
 
+let is_atom (Typ_aux (typ_aux, _)) =
+  match typ_aux with
+  | Typ_app (f, [_]) when string_of_id f = "atom" -> true
+  | _ -> false
+
 (**************************************************************************)
 (* 1. Substitutions                                                       *)
 (**************************************************************************)
@@ -865,11 +870,13 @@ end = struct
 
   let get_constraints env = env.constraints
 
-  let add_constraint (NC_aux (_, l) as constr) env =
+  let add_constraint (NC_aux (nc_aux, l) as constr) env =
     wf_constraint env constr;
     begin
       typ_print ("Adding constraint " ^ string_of_n_constraint constr);
-      { env with constraints = constr :: env.constraints }
+      match nc_aux with
+      | NC_true -> env
+      | _ -> { env with constraints = constr :: env.constraints }
     end
 
   let get_ret_typ env = env.ret_typ
@@ -942,7 +949,6 @@ end = struct
     }
 end
 
-
 let add_typquant (quant : typquant) (env : Env.t) : Env.t =
   let rec add_quant_item env = function
     | QI_aux (qi, _) -> add_quant_item_aux env qi
@@ -978,6 +984,12 @@ let destruct_exist env typ =
      Some (List.map snd fresh_kids, nc, typ)
   | _ -> None
 
+let add_existential kids nc env =
+  let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in
+  Env.add_constraint nc env
+
+let add_typ_vars kids env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids
+
 let is_exist = function
   | Typ_aux (Typ_exist (_, _, _), _) -> true
   | _ -> false
@@ -986,6 +998,41 @@ let exist_typ constr typ =
   let fresh_kid = fresh_existential () in
   mk_typ (Typ_exist ([fresh_kid], constr fresh_kid, typ fresh_kid))
 
+(** Destructure and canonicalise a numeric type into a list of type
+   variables, a constraint on those type variables, and an
+   N-expression that represents that numeric type in the
+   environment. For example:
+   - {'n, 'n <= 10. atom('n)} => ['n], 'n <= 10, 'n
+   - int => ['n], true, 'n (where x is fresh)
+   - atom('n) => [], true, 'n
+**)
+let destruct_numeric env typ =
+  let typ = Env.expand_synonyms env typ in
+  match destruct_exist env typ, typ with
+  | Some (kids, nc, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]), _)), _ when string_of_id id = "atom" ->
+     Some (kids, nc, nexp)
+  | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]), _) when string_of_id id = "atom" ->
+     Some ([], nc_true, nexp)
+  | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _) when string_of_id id = "range" ->
+     let kid = fresh_existential () in
+     Some ([kid], nc_and (nc_lteq lo (nvar kid)) (nc_lteq (nvar kid) hi), nvar kid)
+  | None, Typ_aux (Typ_id id, _) when string_of_id id = "nat" ->
+     let kid = fresh_existential () in
+     Some ([kid], nc_lteq (nint 0) (nvar kid), nvar kid)
+  | None, Typ_aux (Typ_id id, _) when string_of_id id = "int" ->
+     let kid = fresh_existential () in
+     Some ([kid], nc_true, nvar kid)
+  | _, _ -> None
+
+(** Pull an (potentially)-existentially qualified type into the global
+   typing environment **)
+let bind_existential typ env =
+  match destruct_numeric env typ with
+  | Some (kids, nc, nexp) -> atom_typ nexp, add_existential kids nc env
+  | None -> match destruct_exist env typ with
+            | Some (kids, nc, typ) -> typ, add_existential kids nc env
+            | None -> typ, env
+
 let destruct_vector env typ =
   let destruct_vector' = function
     | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _);
@@ -2432,6 +2479,7 @@ and bind_pat_no_guard env (P_aux (_,(l,_)) as pat) typ =
   | tpat, env, [] -> tpat, env
 
 and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) =
+  let (Typ_aux (typ_aux, _) as typ), env = bind_existential typ env in
   typ_print ("Binding " ^ string_of_pat pat ^  " to " ^ string_of_typ typ);
   let annot_pat pat typ = P_aux (pat, (l, Some (env, typ, no_effect))) in
   let switch_typ pat typ = match pat with
@@ -2458,34 +2506,8 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
        | Enum enum -> subtyp l env enum typ; annot_pat (P_id v) typ, env, []
      end
   | P_var (pat, typ_pat) ->
-     let typ = Env.expand_synonyms env typ in
-     let kid = Env.fresh_kid env in
-     let env, ex_typ = match destruct_exist env typ, typ with
-       | Some (kids, nc, ex_typ), _ ->
-          let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in
-          let env = Env.add_constraint nc env in
-          env, ex_typ
-       | None, Typ_aux (Typ_id id, _) when string_of_id id = "int" ->
-          Env.add_typ_var kid BK_nat env, atom_typ (nvar kid)
-       | None, Typ_aux (Typ_id id, _) when string_of_id id = "nat" ->
-          let env = Env.add_typ_var kid BK_nat env in
-          let env = Env.add_constraint (nc_gt (nvar kid) (nint 0)) env in
-          env, atom_typ (nvar kid)
-       | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _)
-            when string_of_id id = "range" ->
-          let env = Env.add_typ_var kid BK_nat env in
-          let env = Env.add_constraint (nc_lteq lo (nvar kid)) env in
-          let env = Env.add_constraint (nc_lteq (nvar kid) hi) env in
-          env, atom_typ (nvar kid)
-       | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _)]), _)
-            when string_of_id id = "atom" ->
-          let env = Env.add_typ_var kid BK_nat env in
-          let env = Env.add_constraint (nc_eq (nvar kid) n) env in
-          env, atom_typ (nvar kid)
-       | None, _ -> typ_error l ("Cannot bind type variable against non existential or numeric type")
-     in
-     let env = bind_typ_pat env typ_pat ex_typ in
-     let typed_pat, env, guards = bind_pat env pat ex_typ in
+     let env = bind_typ_pat env typ_pat typ in
+     let typed_pat, env, guards = bind_pat env pat typ in
      annot_pat (P_var (typed_pat, typ_pat)) typ, env, guards
   | P_wild -> annot_pat P_wild typ, env, []
   | P_cons (hd_pat, tl_pat) ->
@@ -2566,10 +2588,14 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
   | P_as (pat, id) ->
      let (typed_pat, env, guards) = bind_pat env pat typ in
      annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), Env.add_local id (Immutable, pat_typ_of typed_pat) env, guards
+  (* This is a special case for flow typing when we match a constant numeric literal. *)
+  | P_lit (L_aux (L_num n, _) as lit) when is_atom typ ->
+     let nexp = match destruct_atom_nexp env typ with Some n -> n | None -> assert false in
+     annot_pat (P_lit lit) (atom_typ (nconstant n)), Env.add_constraint (nc_eq nexp (nconstant n)) env, []
   | _ ->
      let (inferred_pat, env, guards) = infer_pat env pat in
-     match subtyp l env (pat_typ_of inferred_pat) typ with
-     | () -> switch_typ inferred_pat typ, env, guards
+     match subtyp l env typ (pat_typ_of inferred_pat) with
+     | () -> switch_typ inferred_pat (pat_typ_of inferred_pat), env, guards
      | exception (Type_error _ as typ_exn) ->
         match pat_aux with
         | P_lit lit ->
@@ -2979,27 +3005,17 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        let inferred_f = irule infer_exp env f in
        let inferred_t = irule infer_exp env t in
        let checked_step = crule check_exp env step int_typ in
-       match destruct_range (typ_of inferred_f), destruct_range (typ_of inferred_t) with
-       | None, _ -> typ_error l ("Type of " ^ string_of_exp f ^ " in foreach must be a range")
-       | _, None -> typ_error l ("Type of " ^ string_of_exp t ^ " in foreach must be a range")
-       (* | Some (l1, l2), Some (u1, u2) when prove env (nc_lteq l2 u1) ->
-          let loop_vtyp = exist_typ (fun e -> nc_and (nc_lteq l1 (nvar e)) (nc_lteq (nvar e) u2)) (fun e -> atom_typ (nvar e)) in
+       match destruct_numeric env (typ_of inferred_f), destruct_numeric env (typ_of inferred_t) with
+       | Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) ->
+          let loop_kid = mk_kid ("loop_" ^ string_of_id v) in
+          let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env (loop_kid :: kids1 @ kids2) in
+          let env = Env.add_constraint (nc_and nc1 nc2) env in
+          let env = Env.add_constraint (nc_and (nc_lteq nexp1 (nvar loop_kid)) (nc_lteq (nvar loop_kid) nexp2)) env in
+          let loop_vtyp = atom_typ (nvar loop_kid) in
           let checked_body = crule check_exp (Env.add_local v (Immutable, loop_vtyp) env) body unit_typ in
-          annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ *)
-       | Some (l1, l2), Some (u1, u2) when prove env (nc_lteq l2 u1) ->
-          let kid = mk_kid ("loop_" ^ string_of_id v) in
-          if KBindings.mem kid (Env.get_typ_vars env)
-          then typ_error l "Nested loop variables cannot have the same name"
-          else
-            begin
-              let env = Env.add_typ_var kid BK_nat env in
-              let env = Env.add_constraint (nc_and (nc_lteq l1 (nvar kid)) (nc_lteq (nvar kid) u2)) env in
-              let loop_vtyp = atom_typ (nvar kid) in
-              let checked_body = crule check_exp (Env.add_local v (Immutable, loop_vtyp) env) body unit_typ in
-              if not is_dec (* undo reverse direction in annoteded ast for downto loop *)
-              then annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ
-              else annot_exp (E_for (v, inferred_t, inferred_f, checked_step, ord, checked_body)) unit_typ
-            end
+          if not is_dec (* undo reverse direction in annotated ast for downto loop *)
+          then annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ
+          else annot_exp (E_for (v, inferred_t, inferred_f, checked_step, ord, checked_body)) unit_typ
        | _, _ -> typ_error l "Ranges in foreach overlap"
      end
   | E_if (cond, then_branch, else_branch) ->
@@ -3520,14 +3536,15 @@ and propagate_lexp_effect_aux = function
 (**************************************************************************)
 
 let check_letdef orig_env (LB_aux (letbind, (l, _))) =
+  typ_print "\nChecking top-level let";
   begin
     match letbind with
-    | LB_val (P_aux (P_typ (typ_annot, pat), _), bind) ->
+    | LB_val (P_aux (P_typ (typ_annot, _), _) as pat, bind) ->
        let checked_bind = propagate_exp_effect (crule check_exp orig_env (strip_exp bind) typ_annot) in
        let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) typ_annot in
        if (BESet.is_empty (effect_set (effect_of checked_bind)) || !opt_no_effects)
        then
-         [DEF_val (LB_aux (LB_val (P_aux (P_typ (typ_annot, tpat), (l, Some (orig_env, typ_annot, no_effect))), checked_bind), (l, None)))], env
+         [DEF_val (LB_aux (LB_val (tpat, checked_bind), (l, None)))], env
        else typ_error l ("Top-level definition with effects " ^ string_of_effect (effect_of checked_bind))
     | LB_val (pat, bind) ->
        let inferred_bind = propagate_exp_effect (irule infer_exp orig_env (strip_exp bind)) in
@@ -3650,7 +3667,10 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
   let (id, quants, typ, env) = match vs with
     | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _) as typschm, id, ext_opt, is_cast) ->
        typ_debug ("VS typschm: " ^ string_of_id id ^ ", " ^ string_of_typschm typschm);
-       let env = match ext_opt "smt" with Some op -> Env.add_smt_op id op env | None -> env in
+       let env = match (ext_opt "smt", ext_opt "#") with
+         | Some op, None -> Env.add_smt_op id op env
+         | _, _ -> env
+       in
        Env.wf_typ (add_typquant quants env) typ;
        typ_debug "CHECKED WELL-FORMED VAL SPEC";
        let env =