Fix all warnings (except for two lem warnings)

Remove P_record as it's never been implemented in
parser/typechecker/rewriter, and is not likely to be. This also means
we can get rid of some ugliness with the fpat and mfpat types. Stubs
for P_or and P_not are left as they still may get added to ASL and we
might want to support them, although there are good reasons to keep
our patterns simple.

The lem warning for while -> while0 for ocaml doesn't matter because
it's only used in lem, and the 32-bit number warning is just noise.

17 files changed, 31 insertions, 179 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index ac3c6d2b..4c6a583b 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -593,7 +593,6 @@ and map_pat_annot_aux f = function
   | P_id id -> P_id id
   | P_var (pat, tpat) -> P_var (map_pat_annot f pat, tpat)
   | P_app (id, pats) -> P_app (id, List.map (map_pat_annot f) pats)
-  | P_record (fpats, b) -> P_record (List.map (map_fpat_annot f) fpats, b)
   | P_tup pats -> P_tup (List.map (map_pat_annot f) pats)
   | P_list pats -> P_list (List.map (map_pat_annot f) pats)
   | P_vector_concat pats -> P_vector_concat (List.map (map_pat_annot f) pats)
@@ -619,7 +618,6 @@ and map_mpat_annot_aux f = function
   | MP_lit lit -> MP_lit lit
   | MP_id id -> MP_id id
   | MP_app (id, mpats) -> MP_app (id, List.map (map_mpat_annot f) mpats)
-  | MP_record (fmpats, b) -> MP_record (List.map (map_mfpat_annot f) fmpats, b)
   | MP_tup mpats -> MP_tup (List.map (map_mpat_annot f) mpats)
   | MP_list mpats -> MP_list (List.map (map_mpat_annot f) mpats)
   | MP_vector_concat mpats -> MP_vector_concat (List.map (map_mpat_annot f) mpats)
@@ -629,8 +627,6 @@ and map_mpat_annot_aux f = function
   | MP_typ (mpat, typ) -> MP_typ (map_mpat_annot f mpat, typ)
   | MP_as (mpat, id) -> MP_as (map_mpat_annot f mpat, id)
 
-and map_fpat_annot f (FP_aux (FP_Fpat (id, pat), annot)) = FP_aux (FP_Fpat (id, map_pat_annot f pat), f annot)
-and map_mfpat_annot f (MFP_aux (MFP_mpat (id, mpat), annot)) = MFP_aux (MFP_mpat (id, map_mpat_annot f mpat), f annot)
 and map_letbind_annot f (LB_aux (lb, annot)) = LB_aux (map_letbind_annot_aux f lb, f annot)
 and map_letbind_annot_aux f = function
   | LB_val (pat, exp) -> LB_val (map_pat_annot f pat, map_exp_annot f exp)
@@ -998,7 +994,6 @@ and string_of_pat (P_aux (pat, l)) =
   | P_as (pat, id) -> "(" ^ string_of_pat pat ^ " as " ^ string_of_id id ^ ")"
   | P_string_append [] -> "\"\""
   | P_string_append pats -> string_of_list " ^ " string_of_pat pats
-  | P_record _ -> "PAT"
 
 and string_of_mpat (MP_aux (pat, l)) =
   match pat with
@@ -1013,7 +1008,6 @@ and string_of_mpat (MP_aux (pat, l)) =
   | MP_string_append pats -> string_of_list " ^ " string_of_mpat pats
   | MP_typ (mpat, typ) -> "(" ^ string_of_mpat mpat ^ " : " ^ string_of_typ typ ^ ")"
   | MP_as (mpat, id) -> "((" ^ string_of_mpat mpat ^ ") as " ^ string_of_id id ^ ")"
-  | _ -> "MPAT"
 
 and string_of_lexp (LEXP_aux (lexp, _)) =
   match lexp with
@@ -1051,13 +1045,9 @@ let rec pat_ids (P_aux (pat_aux, _)) =
      List.fold_right IdSet.union (List.map pat_ids pats) IdSet.empty
   | P_cons (pat1, pat2) ->
      IdSet.union (pat_ids pat1) (pat_ids pat2)
-  | P_record (fpats, _) ->
-     List.fold_right IdSet.union (List.map fpat_ids fpats) IdSet.empty
   | P_string_append pats ->
      List.fold_right IdSet.union (List.map pat_ids pats) IdSet.empty
 
-and fpat_ids (FP_aux (FP_Fpat (_, pat), _)) = pat_ids pat
-
 let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) =
   match (List.fold_right
            (fun (FCL_aux (FCL_Funcl (id, _), _)) id' ->
@@ -1770,7 +1760,6 @@ let rec locate_pat : 'a. (l -> l) -> 'a pat -> 'a pat = fun f (P_aux (p_aux, (l,
     | P_id id -> P_id (locate_id f id)
     | P_var (pat, typ_pat) -> P_var (locate_pat f pat, locate_typ_pat f typ_pat)
     | P_app (id, pats) -> P_app (locate_id f id, List.map (locate_pat f) pats)
-    | P_record (fpats, semi) -> P_record (List.map (locate_fpat f) fpats, semi)
     | P_vector pats -> P_vector (List.map (locate_pat f) pats)
     | P_vector_concat pats -> P_vector_concat (List.map (locate_pat f) pats)
     | P_tup pats -> P_tup (List.map (locate_pat f) pats)
@@ -1780,9 +1769,6 @@ let rec locate_pat : 'a. (l -> l) -> 'a pat -> 'a pat = fun f (P_aux (p_aux, (l,
   in
   P_aux (p_aux, (f l, annot))
 
-and locate_fpat : 'a. (l -> l) -> 'a fpat -> 'a fpat = fun f (FP_aux (FP_Fpat (id, pat), (l, annot))) ->
-  FP_aux (FP_Fpat (locate_id f id, locate_pat f pat), (f l, annot))
-
 let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, annot))) ->
   let e_aux = match e_aux with
     | E_block exps -> E_block (List.map (locate f) exps)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index ee8fdf13..f6bf1fcc 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -343,7 +343,6 @@ val map_pexp_annot : ('a annot -> 'b annot) -> 'a pexp -> 'b pexp
 val map_lexp_annot : ('a annot -> 'b annot) -> 'a lexp -> 'b lexp
 val map_letbind_annot : ('a annot -> 'b annot) -> 'a letbind -> 'b letbind
 val map_mpat_annot : ('a annot -> 'b annot) -> 'a mpat -> 'b mpat
-val map_mfpat_annot : ('a annot -> 'b annot) -> 'a mfpat -> 'b mfpat
 val map_mpexp_annot : ('a annot -> 'b annot) -> 'a mpexp -> 'b mpexp
 val map_mapcl_annot : ('a annot -> 'b annot) -> 'a mapcl -> 'b mapcl
 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index ec3e1f24..1aebdbc2 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -338,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)
@@ -691,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)
diff --git a/src/interpreter.ml b/src/interpreter.ml
index a2cc17bf..6707bc0b 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -714,7 +714,6 @@ and pattern_match env (P_aux (p_aux, (l, _)) as pat) value =
        List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches)
      else
        false, Bindings.empty
-  | P_record _ -> assert false (* TODO *)
   | P_vector pats ->
      let matches = List.map2 (pattern_match env) pats (coerce_gv value) in
      List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches)
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 993cc4f5..bd36c262 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -475,9 +475,6 @@ let rec freshen_pat_bindings p =
     | P_app (id,args) ->
        let args',vs = List.split (List.map aux args) in
        mkp (P_app (id,args')),List.concat vs
-    | P_record (fpats,flag) ->
-       let fpats,vs = List.split (List.map auxr fpats) in
-       mkp (P_record (fpats,flag)),List.concat vs
     | P_vector ps ->
        let ps,vs = List.split (List.map aux ps) in
        mkp (P_vector ps),List.concat vs
@@ -497,9 +494,6 @@ let rec freshen_pat_bindings p =
        let p1,vs1 = aux p1 in
        let p2,vs2 = aux p2 in
        mkp (P_cons (p1, p2)), vs1@vs2
-  and auxr (FP_aux (FP_Fpat (id,p),(l,annot))) =
-    let p,vs = aux p in
-    FP_aux (FP_Fpat (id, p),(Generated l,annot)), vs
   in aux p
 
 (* This cuts off function bodies at false assertions that we may have produced
@@ -795,11 +789,7 @@ let split_defs target all_errors splits env defs =
            (* Todo: I am not proud of this abuse of relist - but creating a special
             * version of re just for two entries did not seem worth it
             *)
-          relist f (fun [p1'; p2'] -> ctx p1' p2') [p1; p2]
-        in
-        let fpat (FP_aux ((FP_Fpat (id,p),annot))) =
-          optmap (spl p)
-            (fun ps -> List.map (fun (p,sub,pchoices,ksub) -> FP_aux (FP_Fpat (id,p), annot), sub, pchoices, ksub) ps)
+          relist f (function [p1'; p2'] -> ctx p1' p2' | _ -> assert false) [p1; p2]
         in
         match p with
         | P_lit _
@@ -876,8 +866,6 @@ let split_defs target all_errors splits env defs =
            )
         | P_app (id,ps) ->
            relist spl (fun ps -> P_app (id,ps)) ps
-        | P_record (fps,flag) ->
-           relist fpat (fun fps -> P_record (fps,flag)) fps
         | P_vector ps ->
            relist spl (fun ps -> P_vector ps) ps
         | P_vector_concat ps ->
@@ -1528,17 +1516,12 @@ let rec pat_eq (P_aux (p1,_)) (P_aux (p2,_)) =
   | P_var (p1', tpat1), P_var (p2', tpat2) -> typ_pat_eq tpat1 tpat2 && pat_eq p1' p2'
   | P_app (id1,args1), P_app (id2,args2) ->
      Id.compare id1 id2 == 0 && forall2 pat_eq args1 args2
-  | P_record (fpats1, flag1), P_record (fpats2, flag2) ->
-     flag1 == flag2 && forall2 fpat_eq fpats1 fpats2
   | P_vector ps1, P_vector ps2
   | P_vector_concat ps1, P_vector_concat ps2
   | P_tup ps1, P_tup ps2
   | P_list ps1, P_list ps2 -> List.for_all2 pat_eq ps1 ps2
   | P_cons (p1',p1''), P_cons (p2',p2'') -> pat_eq p1' p2' && pat_eq p1'' p2''
   | _,_ -> false
-and fpat_eq (FP_aux (FP_Fpat (id1,p1),_)) (FP_aux (FP_Fpat (id2,p2),_)) =
-  Id.compare id1 id2 == 0 && pat_eq p1 p2
-
 
 
 module Analysis =
@@ -2023,6 +2006,8 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
          let env = add_arg_only_kids env typ_env typ new_deps in
          let t_deps, t_r, t_env = aux env (t,typs) in
          new_deps::t_deps, merge new_r t_r, t_env
+      | _ :: _, [] ->
+         Reporting.unreachable l __POS__ "Argument and type list in non_det_args had different lengths"
     in
     let deps, r, env = aux env (es,typs) in
     (deps, assigns, r, env)
@@ -2412,7 +2397,6 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions globals =
            kids kids in
          s,v,KidSet.fold (fun kid k -> KBindings.add kid (Have (s, ExtraSplits.empty)) k) kids k
       | P_app (_,pats) -> of_list pats
-      | P_record (fpats,_) -> of_list (List.map (fun (FP_aux (FP_Fpat (_,p),_)) -> p) fpats)
       | P_vector pats
       | P_vector_concat pats
       | P_string_append pats
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 1d2c3534..3147b7f4 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -218,7 +218,6 @@ pat_aux =  (* Pattern *)
  | P_id of id (* identifier *)
  | P_var of pat * atyp (* bind pat to type variable *)
  | P_app of id * (pat) list (* union constructor pattern *)
- | P_record of (fpat) list * bool (* struct pattern *)
  | P_vector of (pat) list (* vector pattern *)
  | P_vector_concat of (pat) list (* concatenated vector pattern *)
  | P_tup of (pat) list (* tuple pattern *)
@@ -392,7 +391,6 @@ type mpat_aux =  (* Mapping pattern. Mostly the same as normal patterns but only
  | MP_lit of lit
  | MP_id of id
  | MP_app of id * ( mpat) list
- | MP_record of ( mfpat) list * bool
  | MP_vector of ( mpat) list
  | MP_vector_concat of ( mpat) list
  | MP_tup of ( mpat) list
@@ -405,12 +403,6 @@ type mpat_aux =  (* Mapping pattern. Mostly the same as normal patterns but only
 and mpat =
  | MP_aux of ( mpat_aux) * l
 
-and mfpat_aux =  (* Mapping field pattern, why does this have to exist *)
- | MFP_mpat of id * mpat
-
-and mfpat =
- | MFP_aux of mfpat_aux * l
-
 type mpexp_aux =
  | MPat_pat of ( mpat)
  | MPat_when of ( mpat) * ( exp)
diff --git a/src/parser.mly b/src/parser.mly
index 4bc2e5c5..0b09468c 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -674,8 +674,6 @@ pat_string_append:
 pat1:
   | atomic_pat
     { $1 }
-  (* | atomic_pat Bar pat1
-    { mk_pat (P_or ($1, $3)) $startpos $endpos } *)
   | atomic_pat At pat_concat
     { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
   | atomic_pat ColonColon pat1
diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index 3de0058f..afda3e1a 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -68,7 +68,6 @@ type gpat =
   | GP_cons of gpat * gpat
   | GP_or of gpat * gpat
   | GP_app of (gpat Bindings.t)
-  | GP_record of (gpat Bindings.t)
   | GP_string_append of gpat list
 
 let rec string_of_gpat = function
@@ -82,7 +81,6 @@ let rec string_of_gpat = function
   | GP_or (gpat1, gpat2) -> string_of_gpat gpat1 ^ " | " ^ string_of_gpat gpat2
   | GP_app app ->
      Util.string_of_list "|" (fun (id, gpat) -> string_of_id id ^ string_of_gpat gpat) (Bindings.bindings app)
-  | GP_record _ -> "GP RECORD"
   | GP_string_append gpats -> Util.string_of_list " ^^ " string_of_gpat gpats
 
 let is_wild = function
@@ -135,15 +133,6 @@ let rec generalize ctx (P_aux (p_aux, (l, _)) as pat) =
        GP_app (Bindings.singleton f GP_wild)
      else
        GP_app (Bindings.singleton f (GP_tup gpats))
-  | P_record (fpats, flag) ->
-     let gfpats = List.concat (List.map (generalize_fpat ctx) fpats) in
-     GP_record (List.fold_left (fun m (fid, gpat) -> Bindings.add fid gpat m) Bindings.empty gfpats)
-
-and generalize_fpat ctx (FP_aux (FP_Fpat (field_id, pat), annot)) =
-  let gpat = generalize ctx pat in
-  if is_wild gpat then []
-  else
-    [(field_id, gpat)]
 
 let vector_pat bits =
   let bit_pat = function
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 5e8c7145..3d50d48c 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1150,7 +1150,6 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty
         "string append pattern found in Coq backend, should have been rewritten"
      | P_not _ -> unreachable l __POS__ "Coq backend doesn't support not patterns"
      | P_or _ -> unreachable l __POS__ "Coq backend doesn't support or patterns yet"
-     | P_record (_,_) -> empty (* TODO *)
 
 let contains_early_return exp =
   let e_app (f, args) =
@@ -1329,7 +1328,6 @@ let merge_new_tyvars ctxt old_env pat new_env =
     | P_list ps
     | P_string_append ps
       -> List.fold_left merge_pat m ps
-    | P_record (fps,_) -> unreachable l __POS__ "Coq backend doesn't support record patterns properly yet"
     | P_cons (p1,p2) -> merge_pat (merge_pat m p1) p2
   in
   let m,r = IdSet.fold remove_binding (pat_ids pat) (ctxt.kid_id_renames, ctxt.kid_id_renames_rev) in
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 1367d9eb..d399ec29 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -549,6 +549,7 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
   | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem ctxt true p) (doc_pat_lem ctxt true p')
   | P_string_append _ -> unreachable l __POS__ "Lem doesn't support string append patterns"
   | P_not _ -> unreachable l __POS__ "Lem doesn't support not patterns"
+  | P_or _ -> unreachable l __POS__ "Lem doesn't support or patterns"
 
 let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with
   | Typ_tup ts -> List.exists typ_needs_printed ts
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 5dbb6cd5..b3675263 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -345,7 +345,6 @@ let rec doc_pat (P_aux (p_aux, (l, _)) as pat) =
   | P_string_append [] -> string "\"\""
   | P_string_append pats ->
      parens (separate_map (string " ^ ") doc_pat pats)
-  | P_record _ -> raise (Reporting.err_unreachable l __POS__ "P_record passed to doc_pat")
 
 (* if_block_x is true if x should be printed like a block, i.e. with
    newlines. Blocks are automatically printed as blocks, so this
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 24261861..62870083 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -63,7 +63,6 @@ type 'a rewriters = {
     rewrite_defs : 'a rewriters -> 'a defs -> 'a defs;
   }
 
-let effect_of_fpat (FP_aux (_,(_,a))) = effect_of_annot a
 let effect_of_lexp (LEXP_aux (_,(_,a))) = effect_of_annot a
 let effect_of_fexp (FE_aux (_,(_,a))) = effect_of_annot a
 let effect_of_fexps fexps =
@@ -255,9 +254,6 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) =
   | P_as(pat,id) -> rewrap (P_as(rewrite pat, id))
   | P_typ(typ,pat) -> rewrap (P_typ(typ, rewrite pat))
   | P_app(id ,pats) -> rewrap (P_app(id, List.map rewrite pats))
-  | P_record(fpats,_) ->
-    rewrap (P_record(List.map (fun (FP_aux(FP_Fpat(id,pat),pannot)) -> FP_aux(FP_Fpat(id, rewrite pat), pannot)) fpats,
-                     false))
   | P_vector pats -> rewrap (P_vector(List.map rewrite pats))
   | P_vector_concat pats -> rewrap (P_vector_concat (List.map rewrite pats))
   | P_tup pats -> rewrap (P_tup (List.map rewrite pats))
@@ -442,7 +438,7 @@ let rewrite_defs_base_parallel j rewriters (Defs defs) =
        exit 1
   done;
   Defs (List.concat !rewritten)
-  
+
 let rewriters_base =
   {rewrite_exp = rewrite_exp;
    rewrite_pat = rewrite_pat;
@@ -454,7 +450,7 @@ let rewriters_base =
 
 let rewrite_defs (Defs defs) = rewrite_defs_base rewriters_base (Defs defs)
 
-type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
+type ('a,'pat,'pat_aux) pat_alg =
   { p_lit            : lit -> 'pat_aux
   ; p_wild           : 'pat_aux
   ; p_or             : 'pat * 'pat -> 'pat_aux
@@ -464,7 +460,6 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
   ; p_id             : id -> 'pat_aux
   ; p_var            : 'pat * typ_pat -> 'pat_aux
   ; p_app            : id * 'pat list -> 'pat_aux
-  ; p_record         : 'fpat list * bool -> 'pat_aux
   ; p_vector         : 'pat list -> 'pat_aux
   ; p_vector_concat  : 'pat list -> 'pat_aux
   ; p_tup            : 'pat list -> 'pat_aux
@@ -472,11 +467,9 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
   ; p_cons           : 'pat * 'pat -> 'pat_aux
   ; p_string_append  : 'pat list -> 'pat_aux
   ; p_aux            : 'pat_aux * 'a annot -> 'pat
-  ; fP_aux           : 'fpat_aux * 'a annot -> 'fpat
-  ; fP_Fpat          : id * 'pat -> 'fpat_aux
   }
 
-let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat_aux -> 'pat_aux =
+let rec fold_pat_aux (alg : ('a,'pat,'pat_aux) pat_alg) : 'a pat_aux -> 'pat_aux =
   function
   | P_lit lit           -> alg.p_lit lit
   | P_wild              -> alg.p_wild
@@ -487,7 +480,6 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat
   | P_as (p,id)         -> alg.p_as (fold_pat alg p, id)
   | P_typ (typ,p)       -> alg.p_typ (typ,fold_pat alg p)
   | P_app (id,ps)       -> alg.p_app (id,List.map (fold_pat alg) ps)
-  | P_record (ps,b)     -> alg.p_record (List.map (fold_fpat alg) ps, b)
   | P_vector ps         -> alg.p_vector (List.map (fold_pat alg) ps)
   | P_vector_concat ps  -> alg.p_vector_concat (List.map (fold_pat alg) ps)
   | P_tup ps            -> alg.p_tup (List.map (fold_pat alg) ps)
@@ -495,18 +487,12 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat
   | P_cons (ph,pt)      -> alg.p_cons (fold_pat alg ph, fold_pat alg pt)
   | P_string_append ps  -> alg.p_string_append (List.map (fold_pat alg) ps)
 
-and fold_pat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat -> 'pat =
+and fold_pat (alg : ('a,'pat,'pat_aux) pat_alg) : 'a pat -> 'pat =
   function
   | P_aux (pat,annot)   -> alg.p_aux (fold_pat_aux alg pat,annot)
-and fold_fpat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat_aux -> 'fpat_aux =
-  function
-  | FP_Fpat (id,pat)    -> alg.fP_Fpat (id,fold_pat alg pat)
-and fold_fpat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat -> 'fpat =
-  function
-  | FP_aux (fpat,annot) -> alg.fP_aux (fold_fpat_aux alg fpat,annot)
 
 (* identity fold from term alg to term alg *)
-let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
+let id_pat_alg : ('a,'a pat, 'a pat_aux) pat_alg =
   { p_lit            = (fun lit -> P_lit lit)
   ; p_wild           = P_wild
   ; p_or             = (fun (pat1, pat2) -> P_or(pat1, pat2))
@@ -516,7 +502,6 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
   ; p_id             = (fun id -> P_id id)
   ; p_var            = (fun (pat,tpat) -> P_var (pat,tpat))
   ; p_app            = (fun (id,ps) -> P_app (id,ps))
-  ; p_record         = (fun (ps,b) -> P_record (ps,b))
   ; p_vector         = (fun ps -> P_vector ps)
   ; p_vector_concat  = (fun ps -> P_vector_concat ps)
   ; p_tup            = (fun ps -> P_tup ps)
@@ -524,13 +509,11 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
   ; p_cons           = (fun (ph,pt) -> P_cons (ph,pt))
   ; p_string_append  = (fun (ps) -> P_string_append (ps))
   ; p_aux            = (fun (pat,annot) -> P_aux (pat,annot))
-  ; fP_aux           = (fun (fpat,annot) -> FP_aux (fpat,annot))
-  ; fP_Fpat          = (fun (id,pat) -> FP_Fpat (id,pat))
   }
 
 type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
-      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg =
+      'pat,'pat_aux) exp_alg =
   { e_block                  : 'exp list -> 'exp_aux
   ; e_id                     : id -> 'exp_aux
   ; e_ref                    : id -> 'exp_aux
@@ -588,7 +571,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
   ; pat_aux                  : 'pexp_aux * 'a annot -> 'pexp
   ; lB_val                   : 'pat * 'exp -> 'letbind_aux
   ; lB_aux                   : 'letbind_aux * 'a annot -> 'letbind
-  ; pat_alg                  : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
+  ; pat_alg                  : ('a,'pat,'pat_aux) pat_alg
   }
 
 let rec fold_exp_aux alg = function
@@ -755,7 +738,6 @@ let compute_pat_alg bot join =
   ; p_id             = (fun id -> (bot, P_id id))
   ; p_var            = (fun ((v,pat),kid) -> (v, P_var (pat,kid)))
   ; p_app            = (fun (id,ps) -> split_join (fun ps -> P_app (id,ps)) ps)
-  ; p_record         = (fun (ps,b) -> split_join (fun ps -> P_record (ps,b)) ps)
   ; p_vector         = split_join (fun ps -> P_vector ps)
   ; p_vector_concat  = split_join (fun ps -> P_vector_concat ps)
   ; p_tup            = split_join (fun ps -> P_tup ps)
@@ -763,8 +745,6 @@ let compute_pat_alg bot join =
   ; p_cons           = (fun ((vh,ph),(vt,pt)) -> (join vh vt, P_cons (ph,pt)))
   ; p_string_append  = split_join (fun ps -> P_string_append ps)
   ; p_aux            = (fun ((v,pat),annot) -> (v, P_aux (pat,annot)))
-  ; fP_aux           = (fun ((v,fpat),annot) -> (v, FP_aux (fpat,annot)))
-  ; fP_Fpat          = (fun (id,(v,pat)) -> (v, FP_Fpat (id,pat)))
   }
 
 let compute_exp_alg bot join =
@@ -862,7 +842,6 @@ let pure_pat_alg bot join =
   ; p_id             = (fun id -> bot)
   ; p_var            = (fun (v,kid) -> v)
   ; p_app            = (fun (id,ps) -> join_list ps)
-  ; p_record         = (fun (ps,b) -> join_list ps)
   ; p_vector         = join_list
   ; p_vector_concat  = join_list
   ; p_tup            = join_list
@@ -870,8 +849,6 @@ let pure_pat_alg bot join =
   ; p_string_append  = join_list
   ; p_cons           = (fun (vh,vt) -> join vh vt)
   ; p_aux            = (fun (v,annot) -> v)
-  ; fP_aux           = (fun (v,annot) -> v)
-  ; fP_Fpat          = (fun (id,v) -> v)
   }
 
 let pure_exp_alg bot join =
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 77974f86..85f00453 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -90,7 +90,7 @@ val rewrite_def : tannot rewriters -> tannot def -> tannot def
 val rewrite_fun : tannot rewriters -> tannot fundef -> tannot fundef
 
 (* the type of interpretations of pattern-matching expressions *)
-type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
+type ('a,'pat,'pat_aux) pat_alg =
   { p_lit            : lit -> 'pat_aux
   ; p_wild           : 'pat_aux
   ; p_or             : 'pat * 'pat -> 'pat_aux
@@ -100,7 +100,6 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
   ; p_id             : id -> 'pat_aux
   ; p_var            : 'pat * typ_pat -> 'pat_aux
   ; p_app            : id * 'pat list -> 'pat_aux
-  ; p_record         : 'fpat list * bool -> 'pat_aux
   ; p_vector         : 'pat list -> 'pat_aux
   ; p_vector_concat  : 'pat list -> 'pat_aux
   ; p_tup            : 'pat list -> 'pat_aux
@@ -108,15 +107,13 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
   ; p_cons           : 'pat * 'pat -> 'pat_aux
   ; p_string_append  : 'pat list -> 'pat_aux
   ; p_aux            : 'pat_aux * 'a annot -> 'pat
-  ; fP_aux           : 'fpat_aux * 'a annot -> 'fpat
-  ; fP_Fpat          : id * 'pat -> 'fpat_aux
   }
 (* fold over pat_aux expressions *)
 
 (* the type of interpretations of expressions *)
 type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
-      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg = 
+      'pat,'pat_aux) exp_alg =
  { e_block                  : 'exp list -> 'exp_aux
  ; e_id                     : id -> 'exp_aux
  ; e_ref                    : id -> 'exp_aux
@@ -174,63 +171,63 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
  ; pat_aux                  : 'pexp_aux * 'a annot -> 'pexp
  ; lB_val                   : 'pat * 'exp -> 'letbind_aux
  ; lB_aux                   : 'letbind_aux * 'a annot -> 'letbind
- ; pat_alg                  : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
+ ; pat_alg                  : ('a,'pat,'pat_aux) pat_alg
  }
 
 (* fold over patterns *)
-val fold_pat : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg -> 'a pat -> 'pat
+val fold_pat : ('a,'pat,'pat_aux) pat_alg -> 'a pat -> 'pat
 
 (* fold over expressions *)
 val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
-      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp
+      'pat,'pat_aux) exp_alg -> 'a exp -> 'exp
 
 val fold_letbind : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
-      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a letbind -> 'letbind
+      'pat,'pat_aux) exp_alg -> 'a letbind -> 'letbind
 
 val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
-      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp
+      'pat,'pat_aux) exp_alg -> 'a pexp -> 'pexp
 
 val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
-      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp
+      'pat,'pat_aux) exp_alg -> 'a pexp -> 'pexp
 
 val fold_funcl : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'a pexp,'pexp_aux,'letbind_aux,'letbind,
-      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a funcl -> 'a funcl
+      'pat,'pat_aux) exp_alg -> 'a funcl -> 'a funcl
 
 val fold_function : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default, 'a pexp,'pexp_aux,'letbind_aux,'letbind,
-      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a fundef -> 'a fundef
+      'pat,'pat_aux) exp_alg -> 'a fundef -> 'a fundef
 
-val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg
+val id_pat_alg : ('a,'a pat, 'a pat_aux) pat_alg
 val id_exp_alg :
   ('a,'a exp,'a exp_aux,'a lexp,'a lexp_aux,'a fexp,
   'a fexp_aux,
   'a opt_default_aux,'a opt_default,'a pexp,'a pexp_aux,
   'a letbind_aux,'a letbind,
-  'a pat,'a pat_aux,'a fpat,'a fpat_aux) exp_alg
+  'a pat,'a pat_aux) exp_alg
 
 val compute_pat_alg : 'b -> ('b -> 'b -> 'b) ->
-  ('a,('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) pat_alg
+  ('a,('b * 'a pat),('b * 'a pat_aux)) pat_alg
 
 val compute_exp_alg : 'b -> ('b -> 'b -> 'b) ->
   ('a,('b * 'a exp),('b * 'a exp_aux),('b * 'a lexp),('b * 'a lexp_aux),('b * 'a fexp),
   ('b * 'a fexp_aux),
   ('b * 'a opt_default_aux),('b * 'a opt_default),('b * 'a pexp),('b * 'a pexp_aux),
   ('b * 'a letbind_aux),('b * 'a letbind),
-  ('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) exp_alg
+  ('b * 'a pat),('b * 'a pat_aux)) exp_alg
 
-val pure_pat_alg : 'b -> ('b -> 'b -> 'b) -> ('a,'b,'b,'b,'b) pat_alg
+val pure_pat_alg : 'b -> ('b -> 'b -> 'b) -> ('a,'b,'b) pat_alg
 
 val pure_exp_alg : 'b -> ('b -> 'b -> 'b) ->
   ('a,'b,'b,'b,'b,'b,
   'b,'b,'b,
   'b,'b,
   'b,'b,
-  'b,'b,'b,'b) exp_alg
+  'b,'b) exp_alg
 
 val simple_annot : Parse_ast.l -> typ -> Parse_ast.l * tannot
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 87891b6d..89b49043 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -370,7 +370,6 @@ let remove_vector_concat_pat pat =
     ; p_id  = (fun id -> P_id id)
     ; p_var = (fun (pat,kid) -> P_var (pat true,kid))
     ; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
-    ; p_record = (fun (fpats,b) -> P_record (fpats, b))
     ; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps))
     ; p_vector_concat  = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps))
     ; p_tup            = (fun ps -> P_tup (List.map (fun p -> p false) ps))
@@ -386,8 +385,6 @@ let remove_vector_concat_pat pat =
               else P_aux (P_as (P_aux (pat,annot),fresh_id_v l),annot))
           | _ -> P_aux (pat,annot)
         )
-    ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot))
-    ; fP_Fpat = (fun (id,p) -> FP_Fpat (id,p false))
     } in
 
   let pat = (fold_pat name_vector_concat_roots pat) false in
@@ -504,8 +501,6 @@ let remove_vector_concat_pat pat =
     ; p_var            = (fun ((pat,decls),kid) -> (P_var (pat,kid),decls))
     ; p_app            = (fun (id,ps) -> let (ps,decls) = List.split ps in
                                          (P_app (id,ps),List.flatten decls))
-    ; p_record         = (fun (ps,b) -> let (ps,decls) = List.split ps in
-                                        (P_record (ps,b),List.flatten decls))
     ; p_vector         = (fun ps -> let (ps,decls) = List.split ps in
                                     (P_vector ps,List.flatten decls))
     ; p_vector_concat  = (fun ps -> let (ps,decls) = List.split ps in
@@ -518,8 +513,6 @@ let remove_vector_concat_pat pat =
                                     (P_string_append ps,List.flatten decls))
     ; p_cons           = (fun ((p,decls),(p',decls')) -> (P_cons (p,p'), decls @ decls'))
     ; p_aux            = (fun ((pat,decls),annot) -> p_aux ((pat,decls),annot))
-    ; fP_aux           = (fun ((fpat,decls),annot) -> (FP_aux (fpat,annot),decls))
-    ; fP_Fpat          = (fun (id,(pat,decls)) -> (FP_Fpat (id,pat),decls))
     } in
 
   let (pat,decls) = fold_pat unname_vector_concat_elements pat in
@@ -697,8 +690,6 @@ let rec is_irrefutable_pattern (P_aux (p,ann)) =
   | P_app (f,args) ->
      Env.is_singleton_union_constructor f (env_of_annot ann) &&
        List.for_all is_irrefutable_pattern args
-  | P_record (fps,_) ->
-     List.for_all (fun (FP_aux (FP_Fpat (_,p),_)) -> is_irrefutable_pattern p) fps
   | P_vector ps
   | P_vector_concat ps
   | P_tup ps
@@ -749,8 +740,6 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
   | P_wild, _ -> Some []
   | P_app (Id_aux (id1,l1),args1), P_app (Id_aux (id2,_),args2) ->
     if id1 = id2 then subsumes_list subsumes_pat args1 args2 else None
-  | P_record (fps1,b1), P_record (fps2,b2) ->
-    if b1 = b2 then subsumes_list subsumes_fpat fps1 fps2 else None
   | P_vector pats1, P_vector pats2
   | P_vector_concat pats1, P_vector_concat pats2
   | P_tup pats1, P_tup pats2
@@ -766,8 +755,6 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
     | _ -> None)
   | _, P_wild -> if is_irrefutable_pattern pat1 then Some [] else None
   | _ -> None
-and subsumes_fpat (FP_aux (FP_Fpat (id1,pat1),_)) (FP_aux (FP_Fpat (id2,pat2),_)) =
-  if id1 = id2 then subsumes_pat pat1 pat2 else None
 
 (* A simple check for pattern disjointness; used for optimisation in the
    guarded pattern rewrite step *)
@@ -817,8 +804,6 @@ let rec pat_to_exp ((P_aux (pat,(l,annot))) as p_aux) =
   | P_typ (_,pat) -> pat_to_exp pat
   | P_id id -> rewrap (E_id id)
   | P_app (id,pats) -> rewrap (E_app (id, List.map pat_to_exp pats))
-  | P_record (fpats,b) ->
-      rewrap (E_record (List.map fpat_to_fexp fpats))
   | P_vector pats -> rewrap (E_vector (List.map pat_to_exp pats))
   | P_vector_concat pats -> begin
       let empty_vec = E_aux (E_vector [], (l,())) in
@@ -838,9 +823,6 @@ let rec pat_to_exp ((P_aux (pat,(l,annot))) as p_aux) =
       (List.fold_right string_append (List.map pat_to_exp pats) empty_string)
     end
 
-and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) =
-  FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot))
-
 let case_exp e t cs =
   let l = get_loc_exp e in
   let env = env_of e in
@@ -974,8 +956,6 @@ let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
     List.exists contains_bitvector_pat pats
 | P_cons (p,ps) -> contains_bitvector_pat p || contains_bitvector_pat ps
 | P_string_append (ps) -> List.exists contains_bitvector_pat ps
-| P_record (fpats,_) ->
-    List.exists (fun (FP_aux (FP_Fpat (_,pat),_)) -> contains_bitvector_pat pat) fpats
 
 let contains_bitvector_pexp = function
 | Pat_aux (Pat_exp (pat,_),_) | Pat_aux (Pat_when (pat,_,_),_) ->
@@ -1001,7 +981,6 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
     ; p_id  = (fun id -> P_id id)
     ; p_var = (fun (pat,kid) -> P_var (pat true,kid))
     ; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
-    ; p_record = (fun (fpats,b) -> P_record (fpats, b))
     ; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps))
     ; p_vector_concat  = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps))
     ; p_string_append  = (fun ps -> P_string_append (List.map (fun p -> p false) ps))
@@ -1018,8 +997,6 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
             P_aux (P_as (P_aux (pat,annot),fresh_id "b__" l), annot)
           | _ -> P_aux (pat,annot)
         )
-    ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot))
-    ; fP_Fpat = (fun (id,p) -> FP_Fpat (id,p false))
     } in
   let pat, env = bind_pat_no_guard env
     (strip_pat ((fold_pat name_bitvector_roots pat) false))
@@ -1153,8 +1130,6 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
     ; p_var            = (fun ((pat,gdls),kid) -> (P_var (pat,kid), gdls))
     ; p_app            = (fun (id,ps) -> let (ps,gdls) = List.split ps in
                                          (P_app (id,ps), flatten_guards_decls gdls))
-    ; p_record         = (fun (ps,b) -> let (ps,gdls) = List.split ps in
-                                        (P_record (ps,b), flatten_guards_decls gdls))
     ; p_vector         = (fun ps -> let (ps,gdls) = List.split ps in
                                     (P_vector ps, flatten_guards_decls gdls))
     ; p_vector_concat  = (fun ps -> let (ps,gdls) = List.split ps in
@@ -1174,8 +1149,6 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
                            | P_as (P_aux (P_vector ps, _), id), true ->
                              (P_aux (P_id id, annot), collect_guards_decls ps id t)
                            | _, _ -> (P_aux (pat,annot), gdls)))
-    ; fP_aux           = (fun ((fpat,gdls),annot) -> (FP_aux (fpat,annot), gdls))
-    ; fP_Fpat          = (fun (id,(pat,gdls)) -> (FP_Fpat (id,pat), gdls))
     } in
   fold_pat guard_bitvector_pat pat
 
@@ -2657,7 +2630,6 @@ let rec bindings_of_pat (P_aux (p_aux, p_annot) as pat) =
   match p_aux with
   | P_lit _ | P_wild -> []
   | P_id id -> [pat]
-  | P_record _ -> failwith "record patterns not yet implemented"
   (* we assume the type-checker has already checked the two sides have the same bindings *)
   | P_or (left, right) -> bindings_of_pat left
   | P_as (p, id) -> [annot_pat (P_id id) unk (env_of_pat p) (typ_of_pat p)]
@@ -2677,7 +2649,6 @@ let rec binding_typs_of_pat (P_aux (p_aux, p_annot) as pat) =
   match p_aux with
   | P_lit _ | P_wild -> []
   | P_id id -> [typ_of_pat pat]
-  | P_record _ -> failwith "record patterns not yet implemented"
   (* we assume the type-checker has already checked the two sides have the same bindings *)
   | P_or (left, right) -> binding_typs_of_pat left
   | P_as (p, id) -> [typ_of_pat p]
@@ -3093,8 +3064,6 @@ let rec rewrite_defs_pat_string_append env =
     | P_aux (P_var (inner_pat, typ_pat), p_annot) ->
        let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in
        P_aux (P_var (inner_pat, typ_pat), p_annot), guards, expr
-    | P_aux (P_record _, p_annot) ->
-       failwith "record patterns not yet implemented"
     | P_aux (P_vector pats, p_annot) ->
        let pats = List.map folder pats in
        P_aux (P_vector pats, p_annot), !guards_ref, !expr_ref
@@ -3235,8 +3204,6 @@ let rewrite_defs_mapping_patterns env =
     | P_aux (P_var (inner_pat, typ_pat), p_annot) ->
        let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in
        P_aux (P_var (inner_pat, typ_pat), p_annot), guards, expr
-    | P_aux (P_record _, p_annot) ->
-       failwith "record patterns not yet implemented"
     | P_aux (P_vector pats, p_annot) ->
        let pats = List.map folder pats in
        P_aux (P_vector pats, p_annot), !guards_ref, !expr_ref
@@ -3860,7 +3827,6 @@ let rec exp_of_mpat ((MP_aux (mpat, (l,annot))) as mp_aux) =
   | MP_lit lit                      -> E_aux (E_lit lit, (l,annot))
   | MP_id id                        -> E_aux (E_id id, (l,annot))
   | MP_app (id, args)               -> E_aux (E_app (id, (List.map exp_of_mpat args)), (l,annot))
-  | MP_record (mfpats, flag)        -> E_aux (E_record (fexps_of_mfpats mfpats flag (l,annot)), (l,annot))
   | MP_vector mpats                 -> E_aux (E_vector (List.map exp_of_mpat mpats), (l,annot))
   | MP_vector_concat mpats          -> List.fold_right concat_vectors (List.map (fun m -> strip_exp (exp_of_mpat m)) mpats) empty_vec
   | MP_tup mpats                    -> E_aux (E_tuple (List.map exp_of_mpat mpats), (l,annot))
@@ -3872,19 +3838,11 @@ let rec exp_of_mpat ((MP_aux (mpat, (l,annot))) as mp_aux) =
                                                     Pat_aux (Pat_exp (pat_of_mpat mpat, exp_of_mpat mpat), (l,annot))
                                                 ]), (l,annot)) (* TODO FIXME location information? *)
 
-
-and fexps_of_mfpats mfpats flag annot =
-  let fexp_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) =
-    FE_aux (FE_Fexp (id, exp_of_mpat mpat), annot)
-  in
-  List.map fexp_of_mfpat mfpats
-
 and pat_of_mpat (MP_aux (mpat, annot)) =
   match mpat with
   | MP_lit lit                      -> P_aux (P_lit lit, annot)
   | MP_id id                        -> P_aux (P_id id, annot)
   | MP_app (id, args)               -> P_aux (P_app (id, (List.map pat_of_mpat args)), annot)
-  | MP_record (mfpats, flag)        -> P_aux (P_record ((fpats_of_mfpats mfpats), flag), annot)
   | MP_vector mpats                 -> P_aux (P_vector (List.map pat_of_mpat mpats), annot)
   | MP_vector_concat mpats          -> P_aux (P_vector_concat (List.map pat_of_mpat mpats), annot)
   | MP_tup mpats                    -> P_aux (P_tup (List.map pat_of_mpat mpats), annot)
@@ -3894,12 +3852,6 @@ and pat_of_mpat (MP_aux (mpat, annot)) =
   | MP_typ (mpat, typ)              -> P_aux (P_typ (typ, pat_of_mpat mpat), annot)
   | MP_as (mpat, id)                -> P_aux (P_as (pat_of_mpat mpat, id), annot)
 
-and fpats_of_mfpats mfpats =
-  let fpat_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) =
-    FP_aux (FP_Fpat (id, pat_of_mpat mpat), annot)
-  in
-  List.map fpat_of_mfpat mfpats
-
 let rewrite_defs_realise_mappings _ (Defs defs) =
   let realise_mpexps forwards mpexp1 mpexp2 =
     let mpexp_pat, mpexp_exp =
@@ -4311,8 +4263,6 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
         let res_pats = subpats [p1;p2] rps in
         rp' @ List.map (function [rp1;rp2] -> RP_cons (rp1,rp2) | _ -> assert false) res_pats
   end
-  | P_record _ ->
-     raise (Reporting.err_unreachable (fst ann) __POS__ "Record pattern not supported")
   | P_or _ ->
      raise (Reporting.err_unreachable (fst ann) __POS__ "Or pattern not supported")
   | P_not _ ->
diff --git a/src/slice.ml b/src/slice.ml
index 1bbbca1e..427d5913 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -219,6 +219,7 @@ let add_def_to_graph graph def =
     | QI_id _ -> ()
     | QI_constraint nc ->
        IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (constraint_ids nc)
+    | QI_constant _ -> ()
   in
 
   let scan_typquant self (TypQ_aux (aux, _)) =
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 57e415a8..40855eec 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -175,9 +175,6 @@ let rec pat_bindings consider_var bound used (P_aux(p,(_,tannot))) =
   | P_app(id,pats) ->
     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
     list_fv bound (Nameset.add (string_of_id id) used) pats
-  | P_record(fpats,_) ->
-    List.fold_right (fun (Ast.FP_aux(Ast.FP_Fpat(_,p),_)) (b,n) ->
-        pat_bindings consider_var bound used p) fpats (bound,used)
   | P_vector pats | Ast.P_vector_concat pats | Ast.P_tup pats | Ast.P_list pats -> list_fv bound used pats
   | _ -> bound,used
 
@@ -738,12 +735,9 @@ let bindings_from_pat p =
     | P_tup ps
     | P_list ps
       -> List.concat (List.map aux_pat ps)
-    | P_record (fps,_) -> List.concat (List.map aux_fpat fps)
     | P_cons (p1,p2) -> aux_pat p1 @ aux_pat p2
-  and aux_fpat (FP_aux (FP_Fpat (_,p), _)) = aux_pat p
   in aux_pat p
 
-
 (* TODO: replace the below with solutions that don't depend so much on the
    structure of the environment. *)
 
@@ -794,15 +788,12 @@ let nexp_subst_fns substs =
     | P_as (p',id) -> re (P_as (s_pat p', id))
     | P_typ (ty,p') -> re (P_typ (s_t ty,s_pat p'))
     | P_app (id,ps) -> re (P_app (id, List.map s_pat ps))
-    | P_record (fps,flag) -> re (P_record (List.map s_fpat fps, flag))
     | P_vector ps -> re (P_vector (List.map s_pat ps))
     | P_vector_concat ps -> re (P_vector_concat (List.map s_pat ps))
     | P_string_append ps -> re (P_string_append (List.map s_pat ps))
     | P_tup ps -> re (P_tup (List.map s_pat ps))
     | P_list ps -> re (P_list (List.map s_pat ps))
     | P_cons (p1,p2) -> re (P_cons (s_pat p1, s_pat p2))
-  and s_fpat (FP_aux (FP_Fpat (id, p), (l,annot))) =
-    FP_aux (FP_Fpat (id, s_pat p), (l,s_tannot annot))
   in
   let rec s_exp (E_aux (e,(l,annot))) =
     let re e = E_aux (e,(l,s_tannot annot)) in
diff --git a/src/type_check.ml b/src/type_check.ml
index fb98ee1b..819143de 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -4672,7 +4672,9 @@ and propagate_pat_effect_aux = function
   | P_vector pats ->
      let p_pats = List.map propagate_pat_effect pats in
      P_vector p_pats, collect_effects_pat p_pats
+                                          (*
   | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented: Cannot propagate effect in pat")
+                                           *)
 
 and propagate_mpat_effect (MP_aux (mpat, annot)) =
   let p_mpat, eff = propagate_mpat_effect_aux mpat in
@@ -4708,7 +4710,6 @@ and propagate_mpat_effect_aux = function
   | MP_as (mpat, id) ->
      let p_mpat = propagate_mpat_effect mpat in
      MP_as (p_mpat, id), effect_of_mpat mpat
-  | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented: Cannot propagate effect in mpat")
 
 and propagate_letbind_effect (LB_aux (lb, (l, annot))) =
   let p_lb, eff = propagate_letbind_effect_aux lb in
@@ -5019,7 +5020,7 @@ let rec warn_if_unsafe_cast l env = function
   | typ when is_bit_typ typ -> ()
   | typ ->
      Reporting.warn ("Potentially unsafe cast involving " ^ string_of_typ typ) l ""
-     
+
 (* Checking a val spec simply adds the type as a binding in the
    context. We have to destructure the various kinds of val specs, but
    the difference is irrelevant for the typechecker. *)