1 files changed, 168 insertions, 100 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index dca42c7b..7012e915 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -70,7 +70,7 @@ type ctx = {
 
 let string_of_parse_id_aux = function
   | P.Id v -> v
-  | P.DeIid v -> v
+  | P.Operator v -> v
 
 let string_of_parse_id (P.Id_aux (id, l)) = string_of_parse_id_aux id
 
@@ -93,7 +93,7 @@ let to_ast_id (P.Id_aux(id, l)) =
   else
     Id_aux ((match id with
              | P.Id x -> Id x
-             | P.DeIid x -> DeIid x),
+             | P.Operator x -> Operator x),
             l)
 
 let to_ast_var (P.Kid_aux (P.Var v, l)) = Kid_aux (Var v, l)
@@ -129,17 +129,18 @@ let format_kind_aux_list = function
   | [kind] -> string_of_kind_aux kind
   | kinds -> "(" ^ Util.string_of_list ", " string_of_kind_aux kinds ^ ")"
 
-let to_ast_kopt ctx (P.KOpt_aux (aux, l)) =
-  let aux, ctx = match aux with
-    | P.KOpt_none v ->
-       let v = to_ast_var v in
-       KOpt_kind (K_aux (K_int, gen_loc l), v), { ctx with kinds = KBindings.add v K_int ctx.kinds }
-    | P.KOpt_kind (k, v) ->
-       let v = to_ast_var v in
-       let k = to_ast_kind k in
-       KOpt_kind (k, v), { ctx with kinds = KBindings.add v (unaux_kind k) ctx.kinds }
+let to_ast_kopts ctx (P.KOpt_aux (aux, l)) =
+  let mk_kopt v k =
+    let v = to_ast_var v in
+    let k = to_ast_kind k in
+    KOpt_aux (KOpt_kind (k, v), l), { ctx with kinds = KBindings.add v (unaux_kind k) ctx.kinds }
   in
-  KOpt_aux (aux, l), ctx
+  match aux with
+  | P.KOpt_kind (attr, vs, None) ->
+     let k = P.K_aux (P.K_int, gen_loc l) in
+     List.fold_left (fun (kopts, ctx) v -> let kopt, ctx = mk_kopt v k in (kopt :: kopts, ctx)) ([], ctx) vs, attr
+  | P.KOpt_kind (attr, vs, Some k) ->
+     List.fold_left (fun (kopts, ctx) v -> let kopt, ctx = mk_kopt v k in (kopt :: kopts, ctx)) ([], ctx) vs, attr
 
 let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
   let aux = match aux with
@@ -171,7 +172,14 @@ let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
        end
     | P.ATyp_exist (kopts, nc, atyp) ->
        let kopts, ctx =
-         List.fold_right (fun kopt (kopts, ctx) -> let kopt, ctx = to_ast_kopt ctx kopt in (kopt :: kopts, ctx)) kopts ([], ctx)
+         List.fold_right (fun kopt (kopts, ctx) ->
+             let (kopts', ctx), attr = to_ast_kopts ctx kopt in
+             match attr with
+             | None ->
+                kopts' @ kopts, ctx
+             | Some attr ->
+                raise (Reporting.err_typ l (sprintf "Attribute %s cannot appear within an existential type" attr))
+           ) kopts ([], ctx)
        in
        Typ_exist (kopts, to_ast_constraint ctx nc, to_ast_typ ctx atyp)
     | P.ATyp_base (id, kind, nc) ->
@@ -224,14 +232,14 @@ and to_ast_order ctx (P.ATyp_aux (aux, l)) =
 
 and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) =
   let aux = match aux with
-    | P.ATyp_app (Id_aux (DeIid op, _) as id, [t1; t2]) ->
+    | P.ATyp_app (Id_aux (Operator op, _) as id, [t1; t2]) ->
        begin match op with
        | "==" -> NC_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
        | "!=" -> NC_not_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
        | ">=" -> NC_bounded_ge (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
        | "<=" -> NC_bounded_le (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
-       | ">" -> NC_bounded_ge (to_ast_nexp ctx t1, nsum (to_ast_nexp ctx t2) (nint 1))
-       | "<" -> NC_bounded_le (nsum (to_ast_nexp ctx t1) (nint 1), to_ast_nexp ctx t2)
+       | ">" -> NC_bounded_gt (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
+       | "<" -> NC_bounded_lt (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
        | "&" -> NC_and (to_ast_constraint ctx t1, to_ast_constraint ctx t2)
        | "|" -> NC_or (to_ast_constraint ctx t1, to_ast_constraint ctx t2)
        | _ ->
@@ -262,19 +270,25 @@ and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) =
   in
   NC_aux (aux, l)
 
-let to_ast_quant_item ctx (P.QI_aux (aux, l)) =
+let to_ast_quant_items ctx (P.QI_aux (aux, l)) =
   match aux with
-  | P.QI_const nc -> QI_aux (QI_const (to_ast_constraint ctx nc), l), ctx
+  | P.QI_constraint nc -> [QI_aux (QI_constraint (to_ast_constraint ctx nc), l)], ctx
   | P.QI_id kopt ->
-     let kopt, ctx = to_ast_kopt ctx kopt in
-     QI_aux (QI_id kopt, l), ctx
+     let (kopts, ctx), attr = to_ast_kopts ctx kopt in
+     match attr with
+     | Some "constant" ->
+        QI_aux (QI_constant kopts, l) :: List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts, ctx
+     | Some attr ->
+        raise (Reporting.err_typ l (sprintf "Unknown attribute %s" attr))
+     | None ->
+        List.map (fun kopt -> QI_aux (QI_id kopt, l)) kopts, ctx
 
 let to_ast_typquant ctx (P.TypQ_aux (aux, l)) =
   match aux with
   | P.TypQ_no_forall -> TypQ_aux (TypQ_no_forall, l), ctx
   | P.TypQ_tq quants ->
      let quants, ctx =
-       List.fold_left (fun (qis, ctx) qi -> let qi', ctx = to_ast_quant_item ctx qi in qi' :: qis, ctx) ([], ctx) quants
+       List.fold_left (fun (qis, ctx) qi -> let qis', ctx = to_ast_quant_items ctx qi in qis' @ qis, ctx) ([], ctx) quants
      in
      TypQ_aux (TypQ_tq (List.rev quants), l), ctx
 
@@ -324,11 +338,6 @@ let rec to_ast_pat ctx (P.P_aux (pat, l)) =
              if List.length pats == 1 && string_of_parse_id id = "~"
              then P_not (to_ast_pat ctx (List.hd pats))
              else P_app (to_ast_id id, List.map (to_ast_pat ctx) pats)
-          | P.P_record(fpats,_) ->
-             P_record(List.map
-                        (fun (P.FP_aux(P.FP_Fpat(id,fp),l)) ->
-                          FP_aux(FP_Fpat(to_ast_id id, to_ast_pat ctx fp),(l,())))
-                        fpats, false)
           | P.P_vector(pats) -> P_vector(List.map (to_ast_pat ctx) pats)
           | P.P_vector_concat(pats) -> P_vector_concat(List.map (to_ast_pat ctx) pats)
           | P.P_tup(pats) -> P_tup(List.map (to_ast_pat ctx) pats)
@@ -351,7 +360,6 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
       (match to_ast_fexps false ctx exps with
       | Some(fexps) -> E_record(fexps)
       | None -> E_block(List.map (to_ast_exp ctx) exps))
-    | P.E_nondet(exps) -> E_nondet(List.map (to_ast_exp ctx) exps)
     | P.E_id(id) -> E_id(to_ast_id id)
     | P.E_ref(id) -> E_ref(to_ast_id id)
     | P.E_lit(lit) -> E_lit(to_ast_lit lit)
@@ -367,8 +375,8 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
     | P.E_for(id,e1,e2,e3,atyp,e4) ->
       E_for(to_ast_id id,to_ast_exp ctx e1, to_ast_exp ctx e2,
             to_ast_exp ctx e3,to_ast_order ctx atyp, to_ast_exp ctx e4)
-    | P.E_loop (P.While, e1, e2) -> E_loop (While, to_ast_exp ctx e1, to_ast_exp ctx e2)
-    | P.E_loop (P.Until, e1, e2) -> E_loop (Until, to_ast_exp ctx e1, to_ast_exp ctx e2)
+    | P.E_loop (P.While, m, e1, e2) -> E_loop (While, to_ast_measure ctx m, to_ast_exp ctx e1, to_ast_exp ctx e2)
+    | P.E_loop (P.Until, m, e1, e2) -> E_loop (Until, to_ast_measure ctx m, to_ast_exp ctx e1, to_ast_exp ctx e2)
     | P.E_vector(exps) -> E_vector(List.map (to_ast_exp ctx) exps)
     | P.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp ctx vexp, to_ast_exp ctx exp)
     | P.E_vector_subrange(vex,exp1,exp2) ->
@@ -411,9 +419,20 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
          E_internal_return(to_ast_exp ctx exp)
        else
          raise (Reporting.err_general l "Internal return construct found without -dmagic_hash")
-    | _ -> raise (Reporting.err_unreachable l __POS__ "Unparsable construct in to_ast_exp")
+    | P.E_deref exp ->
+       E_app (Id_aux (Id "__deref", l), [to_ast_exp ctx exp])
     ), (l,()))
 
+and to_ast_measure ctx (P.Measure_aux(m,l)) : unit internal_loop_measure =
+  let m = match m with
+    | P.Measure_none -> Measure_none
+    | P.Measure_some exp ->
+       if !opt_magic_hash then
+         Measure_some (to_ast_exp ctx exp)
+       else
+         raise (Reporting.err_general l "Internal loop termination measure found without -dmagic_hash")
+  in Measure_aux (m,l)
+
 and to_ast_lexp ctx (P.E_aux(exp,l) : P.exp) : unit lexp =
   let lexp = match exp with
     | P.E_id id -> LEXP_id (to_ast_id id)
@@ -522,52 +541,100 @@ let rec to_ast_range (P.BF_aux(r,l)) = (* TODO add check that ranges are sensibl
     | P.BF_concat(ir1,ir2) -> BF_concat(to_ast_range ir1, to_ast_range ir2)),
     l)
 
-let to_ast_type_union ctx (P.Tu_aux (P.Tu_ty_id (atyp, id), l)) =
-  let typ = to_ast_typ ctx atyp in
-  Tu_aux (Tu_ty_id (typ, to_ast_id id), l)
+let to_ast_type_union ctx = function
+  | P.Tu_aux (P.Tu_ty_id (atyp, id), l) ->
+     let typ = to_ast_typ ctx atyp in
+     Tu_aux (Tu_ty_id (typ, to_ast_id id), l)
+  | P.Tu_aux (_, l) ->
+     raise (Reporting.err_unreachable l __POS__ "Anonymous record type should have been rewritten by now")
 
 let add_constructor id typq ctx =
   let kinds = List.map (fun kopt -> unaux_kind (kopt_kind kopt)) (quant_kopts typq) in
   { ctx with type_constructors = Bindings.add id kinds ctx.type_constructors }
 
-let to_ast_typedef ctx (P.TD_aux (aux, l) : P.type_def) : unit type_def ctx_out =
-  let aux, ctx = match aux with
-    | P.TD_abbrev (id, typq, kind, typ_arg) ->
-       let id = to_ast_id id in
-       let typq, typq_ctx = to_ast_typquant ctx typq in
-       let kind = to_ast_kind kind in
-       let typ_arg = to_ast_typ_arg typq_ctx typ_arg (unaux_kind kind) in
-       TD_abbrev (id, typq, typ_arg),
-       add_constructor id typq ctx
-
-    | P.TD_record (id, typq, fields, _) ->
-       let id = to_ast_id id in
-       let typq, typq_ctx = to_ast_typquant ctx typq in
-       let fields = List.map (fun (atyp, id) -> to_ast_typ typq_ctx atyp, to_ast_id id) fields in
-       TD_record (id, typq, fields, false),
-       add_constructor id typq ctx
-
-    | P.TD_variant (id, typq, arms, _) ->
-       let id = to_ast_id id in
-       let typq, typq_ctx = to_ast_typquant ctx typq in
-       let arms = List.map (to_ast_type_union typq_ctx) arms in
-       TD_variant (id, typq, arms, false),
-       add_constructor id typq ctx
-
-    | P.TD_enum (id, enums, _) ->
-       let id = to_ast_id id in
-       let enums = List.map to_ast_id enums in
-       TD_enum (id, enums, false),
-       { ctx with type_constructors = Bindings.add id [] ctx.type_constructors }
+let anon_rec_constructor_typ record_id = function
+  | P.TypQ_aux (P.TypQ_no_forall, l) -> P.ATyp_aux (P.ATyp_id record_id, Generated l)
+  | P.TypQ_aux (P.TypQ_tq quants, l) ->
+     let rec quant_arg = function
+       | P.QI_aux (P.QI_id (P.KOpt_aux (P.KOpt_kind (_, vs, _), l)), _) ->
+          List.map (fun v -> P.ATyp_aux (P.ATyp_var v, Generated l)) vs
+       | P.QI_aux (P.QI_constraint _, _) -> []
+     in
+     match List.concat (List.map quant_arg quants) with
+     | [] -> P.ATyp_aux (P.ATyp_id record_id, Generated l)
+     | args -> P.ATyp_aux (P.ATyp_app (record_id, args), Generated l)
+
+let rec realise_union_anon_rec_types orig_union arms =
+  match orig_union with
+  | P.TD_variant (union_id, typq, _, flag) ->
+     begin match arms with
+     | [] -> []
+     | arm :: arms ->
+        match arm with
+        | (P.Tu_aux ((P.Tu_ty_id _), _)) -> (None, arm) :: realise_union_anon_rec_types orig_union arms
+        | (P.Tu_aux ((P.Tu_ty_anon_rec (fields, id)), l)) ->
+           let open Parse_ast in
+           let record_str = "_" ^ string_of_parse_id union_id ^ "_" ^ string_of_parse_id id ^ "_record" in
+           let record_id = Id_aux (Id record_str, Generated l) in
+           let new_arm = Tu_aux (Tu_ty_id (anon_rec_constructor_typ record_id typq, id), Generated l) in
+           let new_rec_def = TD_aux (TD_record (record_id, typq, fields, flag), Generated l) in
+           (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms)
+     end
+  | _ ->
+     raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Non union type-definition passed to realise_union_anon_rec_typs")
 
-    | P.TD_bitfield (id, typ, ranges) ->
-       let id = to_ast_id id in
-       let typ = to_ast_typ ctx typ in
-       let ranges = List.map (fun (id, range) -> (to_ast_id id, to_ast_range range)) ranges in
-       TD_bitfield (id, typ, ranges),
-       { ctx with type_constructors = Bindings.add id [] ctx.type_constructors }
-  in
-  TD_aux (aux, (l, ())), ctx
+let rec to_ast_typedef ctx (P.TD_aux (aux, l) : P.type_def) : unit type_def list ctx_out =
+  match aux with
+  | P.TD_abbrev (id, typq, kind, typ_arg) ->
+     let id = to_ast_id id in
+     let typq, typq_ctx = to_ast_typquant ctx typq in
+     let kind = to_ast_kind kind in
+     let typ_arg = to_ast_typ_arg typq_ctx typ_arg (unaux_kind kind) in
+     [TD_aux (TD_abbrev (id, typq, typ_arg), (l, ()))],
+     add_constructor id typq ctx
+
+  | P.TD_record (id, typq, fields, _) ->
+     let id = to_ast_id id in
+     let typq, typq_ctx = to_ast_typquant ctx typq in
+     let fields = List.map (fun (atyp, id) -> to_ast_typ typq_ctx atyp, to_ast_id id) fields in
+     [TD_aux (TD_record (id, typq, fields, false), (l, ()))],
+     add_constructor id typq ctx
+
+  | P.TD_variant (id, typq, arms, _) as union ->
+     (* First generate auxilliary record types for anonymous records in constructors *)
+     let records_and_arms = realise_union_anon_rec_types union arms in
+     let rec filter_records = function
+       | [] -> []
+       | Some x :: xs -> x :: filter_records xs
+       | None :: xs -> filter_records xs
+     in
+     let generated_records = filter_records (List.map fst records_and_arms) in
+     let generated_records, ctx =
+       List.fold_left (fun (prev, ctx) td -> let td, ctx = to_ast_typedef ctx td in prev @ td, ctx)
+         ([], ctx)
+         generated_records
+     in
+     let arms = List.map snd records_and_arms in
+     let union = Parse_ast.TD_variant (id, typq, arms, false) in
+     (* Now generate the AST union type *)
+     let id = to_ast_id id in
+     let typq, typq_ctx = to_ast_typquant ctx typq in
+     let arms = List.map (to_ast_type_union typq_ctx) arms in
+     [TD_aux (TD_variant (id, typq, arms, false), (l, ()))] @ generated_records,
+     add_constructor id typq ctx
+
+  | P.TD_enum (id, enums, _) ->
+     let id = to_ast_id id in
+     let enums = List.map to_ast_id enums in
+     [TD_aux (TD_enum (id, enums, false), (l, ()))],
+     { ctx with type_constructors = Bindings.add id [] ctx.type_constructors }
+
+  | P.TD_bitfield (id, typ, ranges) ->
+     let id = to_ast_id id in
+     let typ = to_ast_typ ctx typ in
+     let ranges = List.map (fun (id, range) -> (to_ast_id id, to_ast_range range)) ranges in
+     [TD_aux (TD_bitfield (id, typ, ranges), (l, ()))],
+     { ctx with type_constructors = Bindings.add id [] ctx.type_constructors }
 
 let to_ast_rec ctx (P.Rec_aux(r,l): P.rec_opt) : unit rec_opt =
   Rec_aux((match r with
@@ -619,11 +686,6 @@ let rec to_ast_mpat ctx (P.MP_aux(mpat,l)) =
       if mpats = []
       then MP_id (to_ast_id id)
       else MP_app(to_ast_id id, List.map (to_ast_mpat ctx) mpats)
-    | P.MP_record(mfpats,_) ->
-      MP_record(List.map
-                 (fun (P.MFP_aux(P.MFP_mpat(id,mfp),l)) ->
-              MFP_aux(MFP_mpat(to_ast_id id, to_ast_mpat ctx mfp),(l,())))
-                 mfpats, false)
     | P.MP_vector(mpats) -> MP_vector(List.map (to_ast_mpat ctx) mpats)
     | P.MP_vector_concat(mpats) -> MP_vector_concat(List.map (to_ast_mpat ctx) mpats)
     | P.MP_tup(mpats) -> MP_tup(List.map (to_ast_mpat ctx) mpats)
@@ -714,44 +776,50 @@ let to_ast_prec = function
   | P.InfixL -> InfixL
   | P.InfixR -> InfixR
 
-let to_ast_def ctx def : unit def ctx_out =
+let to_ast_loop_measure ctx = function
+  | P.Loop (P.While, exp) -> Loop (While, to_ast_exp ctx exp)
+  | P.Loop (P.Until, exp) -> Loop (Until, to_ast_exp ctx exp)
+
+let to_ast_def ctx def : unit def list ctx_out =
   match def with
   | P.DEF_overload (id, ids) ->
-     DEF_overload (to_ast_id id, List.map to_ast_id ids), ctx
+     [DEF_overload (to_ast_id id, List.map to_ast_id ids)], ctx
   | P.DEF_fixity (prec, n, op) ->
-     DEF_fixity (to_ast_prec prec, n, to_ast_id op), ctx
+     [DEF_fixity (to_ast_prec prec, n, to_ast_id op)], ctx
   | P.DEF_type(t_def) ->
-     let td, ctx = to_ast_typedef ctx t_def in
-     DEF_type td, ctx
+     let tds, ctx = to_ast_typedef ctx t_def in
+     List.map (fun td -> DEF_type td) tds, ctx
   | P.DEF_fundef(f_def) ->
      let fd = to_ast_fundef ctx f_def in
-     DEF_fundef fd, ctx
+     [DEF_fundef fd], ctx
   | P.DEF_mapdef(m_def) ->
      let md = to_ast_mapdef ctx m_def in
-     DEF_mapdef md, ctx
+     [DEF_mapdef md], ctx
   | P.DEF_val(lbind) ->
      let lb = to_ast_letbind ctx lbind in
-     DEF_val lb, ctx
+     [DEF_val lb], ctx
   | P.DEF_spec(val_spec) ->
      let vs,ctx = to_ast_spec ctx val_spec in
-     DEF_spec vs, ctx
+     [DEF_spec vs], ctx
   | P.DEF_default(typ_spec) ->
      let default,ctx = to_ast_default ctx typ_spec in
-     DEF_default default, ctx
+     [DEF_default default], ctx
   | P.DEF_reg_dec dec ->
      let d = to_ast_dec ctx dec in
-     DEF_reg_dec d, ctx
+     [DEF_reg_dec d], ctx
   | P.DEF_pragma (pragma, arg, l) ->
-     DEF_pragma (pragma, arg, l), ctx
+     [DEF_pragma (pragma, arg, l)], ctx
   | P.DEF_internal_mutrec _ ->
      (* Should never occur because of remove_mutrec *)
      raise (Reporting.err_unreachable P.Unknown __POS__
                                       "Internal mutual block found when processing scattered defs")
   | P.DEF_scattered sdef ->
      let sdef, ctx = to_ast_scattered ctx sdef in
-     DEF_scattered sdef, ctx
+     [DEF_scattered sdef], ctx
   | P.DEF_measure (id, pat, exp) ->
-     DEF_measure (to_ast_id id, to_ast_pat ctx pat, to_ast_exp ctx exp), ctx
+     [DEF_measure (to_ast_id id, to_ast_pat ctx pat, to_ast_exp ctx exp)], ctx
+  | P.DEF_loop_measures (id, measures) ->
+     [DEF_loop_measures (to_ast_id id, List.map (to_ast_loop_measure ctx) measures)], ctx
 
 let rec remove_mutrec = function
   | [] -> []
@@ -763,7 +831,7 @@ let rec remove_mutrec = function
 let to_ast ctx (P.Defs(defs)) =
   let defs = remove_mutrec defs in
   let defs, ctx =
-    List.fold_left (fun (defs, ctx) def -> let def, ctx = to_ast_def ctx def in (def :: defs, ctx)) ([], ctx) defs
+    List.fold_left (fun (defs, ctx) def -> let def, ctx = to_ast_def ctx def in (def @ defs, ctx)) ([], ctx) defs
   in
   Defs (List.rev defs), ctx
 
@@ -780,6 +848,7 @@ let initial_ctx = {
           ("list", [K_type]);
           ("register", [K_type]);
           ("range", [K_int; K_int]);
+          ("bitvector", [K_int; K_order]);
           ("vector", [K_int; K_order; K_type]);
           ("atom", [K_int]);
           ("implicit", [K_int]);
@@ -808,8 +877,8 @@ let constraint_of_string str =
   let atyp = Parser.typ_eof Lexer.token (Lexing.from_string str) in
   to_ast_constraint initial_ctx atyp
 
-let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> Some (string_of_id id)), false))
-let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> None), false))
+let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, [("_", string_of_id id)], false))
+let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, [], false))
 
 let quant_item_param = function
   | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
@@ -845,8 +914,7 @@ let undefined_builtin_val_specs =
    extern_of_string (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
    extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
    extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
-   (* Only used with lem_mwords *)
-   extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
+   extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> bitvector('n, dec) effect {undef}";
    extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"]
 
 let generate_undefineds vs_ids (Defs defs) =
@@ -863,8 +931,8 @@ let generate_undefineds vs_ids (Defs defs) =
   in
   let undefined_tu = function
     | Tu_aux (Tu_ty_id (Typ_aux (Typ_tup typs, _), id), _) ->
-       mk_exp (E_app (id, List.map (fun _ -> mk_lit_exp L_undef) typs))
-    | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef]))
+       mk_exp (E_app (id, List.map (fun typ -> mk_exp (E_cast (typ, mk_lit_exp L_undef))) typs))
+    | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_exp (E_cast (typ, mk_lit_exp L_undef))]))
   in
   let p_tup = function
     | [pat] -> pat
@@ -873,7 +941,7 @@ let generate_undefineds vs_ids (Defs defs) =
   let undefined_td = function
     | TD_enum (id, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let typschm = typschm_of_string ("unit -> " ^ string_of_id id ^ " effect {undef}") in
-       [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false));
+       [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, [], false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             (mk_pat (P_lit (mk_lit L_unit)))
                             (if !opt_fast_undefined && List.length ids > 0 then
@@ -883,7 +951,7 @@ let generate_undefineds vs_ids (Defs defs) =
                                               [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
     | TD_record (id, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in
-       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
+       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             pat
                             (mk_exp (E_record (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields)))]]
@@ -931,7 +999,7 @@ let generate_undefineds vs_ids (Defs defs) =
              (mk_exp (E_app (mk_id "internal_pick",
                              [mk_exp (E_list (List.map (make_constr typ_to_var) constr_args))]))) letbinds
        in
-       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
+       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                       pat
                       body]]
@@ -967,7 +1035,7 @@ 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 quants typ =
-         mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, (fun _ -> None), !opt_enum_casts))
+         mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, [], !opt_enum_casts))
        in
        let range_constraint kid = nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1))) in