Remove unused internal AST nodes

E_internal_cast, E_sizeof_internal, E_internal_exp,
E_internal_exp_user, E_comment, and E_comment_struc were all
unused. For a lem based interpreter, we want to be able to compile it
to iUsabelle, and due to slowness inherent in Isabelle's datatype
package we want to remove unused constructors in our AST type.

Also remove the lem_ast backend - it's heavily bitrotted, and for
loading the ARM ast into the interpreter it's just not viable to use
this approach as it just doesn't scale. We really need a way to be
able to serialise and deserialise the AST efficiently in Lem.

17 files changed, 33 insertions, 787 deletions

diff --git a/src/anf.ml b/src/anf.ml
index 2cb9da17..d0803d4f 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -696,9 +696,5 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
      (* We don't compile E_nondet nodes *)
      failwith "encountered E_nondet node when converting to ANF"
 
-  | E_comment _ | E_comment_struc _ ->
-     (* comment AST nodes not-supported *)
-     failwith "encountered E_comment or E_comment_struc node when converting to ANF"
-
-  | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_plet _ | E_internal_return _ | E_internal_exp_user _ ->
+  | E_internal_return _ | E_internal_plet _ ->
      failwith "encountered unexpected internal node when converting to ANF"
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 86457e8f..3f5e92a1 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -419,12 +419,6 @@ and map_exp_annot_aux f = function
   | E_throw exp -> E_throw (map_exp_annot f exp)
   | E_return exp -> E_return (map_exp_annot f exp)
   | E_assert (test, msg) -> E_assert (map_exp_annot f test, map_exp_annot f msg)
-  | E_internal_cast (annot, exp) -> E_internal_cast (f annot, map_exp_annot f exp)
-  | E_internal_exp annot -> E_internal_exp (f annot)
-  | E_sizeof_internal annot -> E_sizeof_internal (f annot)
-  | E_internal_exp_user (annot1, annot2) -> E_internal_exp_user (f annot1, f annot2)
-  | E_comment str -> E_comment str
-  | E_comment_struc exp -> E_comment_struc (map_exp_annot f exp)
   | E_internal_value v -> E_internal_value v
   | E_var (lexp, exp1, exp2) -> E_var (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2)
   | E_internal_plet (pat, exp1, exp2) -> E_internal_plet (map_pat_annot f pat, map_exp_annot f exp1, map_exp_annot f exp2)
@@ -524,9 +518,7 @@ let def_loc = function
   | DEF_fixity (_, _, Id_aux (_, l))
   | DEF_overload (Id_aux (_, l), _) ->
     l
-  | DEF_internal_mutrec _
-  | DEF_comm _ ->
-    Parse_ast.Unknown
+  | DEF_internal_mutrec _ -> Parse_ast.Unknown
 
 let string_of_id = function
   | Id_aux (Id v, _) -> v
@@ -720,12 +712,6 @@ let rec string_of_exp (E_aux (exp, _)) =
      "{ " ^ string_of_exp exp ^ " with " ^ string_of_list "; " string_of_fexp fexps ^ " }"
   | E_record (FES_aux (FES_Fexps (fexps, _), _)) ->
      "{ " ^ string_of_list "; " string_of_fexp fexps ^ " }"
-  | E_internal_cast _ -> "INTERNAL CAST"
-  | E_internal_exp _ -> "INTERNAL EXP"
-  | E_sizeof_internal _ -> "INTERNAL SIZEOF"
-  | E_internal_exp_user _ -> "INTERNAL EXP USER"
-  | E_comment _ -> "INTERNAL COMMENT"
-  | E_comment_struc _ -> "INTERNAL COMMENT STRUC"
   | E_var _ -> "INTERNAL LET"
   | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")"
   | E_internal_plet (pat, exp, body) -> "internal_plet " ^ string_of_pat pat ^ " = " ^ string_of_exp exp ^ " in " ^ string_of_exp body
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 7886fe6b..d7a0c878 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -570,7 +570,6 @@ let nexp_subst_fns substs =
       | E_id _
       | E_ref _
       | E_lit _
-      | E_comment _
       | E_internal_value _
         -> re e
       | E_sizeof ne -> begin
@@ -580,10 +579,6 @@ let nexp_subst_fns substs =
          | _ -> re (E_sizeof ne')
       end
       | E_constraint nc -> re (E_constraint (subst_nc substs nc))
-      | E_internal_exp (l,annot) -> re (E_internal_exp (l, s_tannot annot))
-      | E_sizeof_internal (l,annot) -> re (E_sizeof_internal (l, s_tannot annot))
-      | E_internal_exp_user ((l1,annot1),(l2,annot2)) ->
-         re (E_internal_exp_user ((l1, s_tannot annot1),(l2, s_tannot annot2)))
       | E_cast (t,e') -> re (E_cast (s_t t, s_exp e'))
       | E_app (id,es) -> re (E_app (id, List.map s_exp es))
       | E_app_infix (e1,id,e2) -> re (E_app_infix (s_exp e1,id,s_exp e2))
@@ -608,8 +603,6 @@ let nexp_subst_fns substs =
       | E_exit e -> re (E_exit (s_exp e))
       | E_return e -> re (E_return (s_exp e))
       | E_assert (e1,e2) -> re (E_assert (s_exp e1,s_exp e2))
-      | E_internal_cast ((l,ann),e) -> re (E_internal_cast ((l,s_tannot ann),s_exp e))
-      | E_comment_struc e -> re (E_comment_struc e)
       | E_var (le,e1,e2) -> re (E_var (s_lexp le, s_exp e1, s_exp e2))
       | E_internal_plet (p,e1,e2) -> re (E_internal_plet (s_pat p, s_exp e1, s_exp e2))
       | E_internal_return e -> re (E_internal_return (s_exp e))
@@ -1247,10 +1240,6 @@ let split_defs all_errors splits defs =
        with Not_found -> exp),assigns
     | E_lit _
     | E_sizeof _
-    | E_internal_exp _
-    | E_sizeof_internal _
-    | E_internal_exp_user _
-    | E_comment _
     | E_constraint _
       -> exp,assigns
     | E_cast (t,e') ->
@@ -1433,11 +1422,6 @@ let split_defs all_errors splits defs =
     | E_assert (e1,e2) ->
        let e1',e2',assigns = non_det_exp_2 e1 e2 in
        re (E_assert (e1',e2')) assigns
-    | E_internal_cast (ann,e) ->
-       let e',assigns = const_prop_exp ref_vars substs assigns e in
-       re (E_internal_cast (ann,e')) assigns
-    (* TODO: should I substitute or anything here?  Is it even used? *)
-    | E_comment_struc e -> re (E_comment_struc e) assigns
 
     | E_app_infix _
     | E_var _
@@ -1943,10 +1927,6 @@ let split_defs all_errors splits defs =
         | E_id _
         | E_lit _
         | E_sizeof _
-        | E_internal_exp _
-        | E_sizeof_internal _
-        | E_internal_exp_user _
-        | E_comment _
         | E_constraint _
         | E_ref _
         | E_internal_value _
@@ -1984,8 +1964,6 @@ let split_defs all_errors splits defs =
         | E_try (e,cases) -> re (E_try (map_exp e, List.concat (List.map map_pexp cases)))
         | E_return e -> re (E_return (map_exp e))
         | E_assert (e1,e2) -> re (E_assert (map_exp e1,map_exp e2))
-        | E_internal_cast (ann,e) -> re (E_internal_cast (ann,map_exp e))
-        | E_comment_struc e -> re (E_comment_struc e)
         | E_var (le,e1,e2) -> re (E_var (map_lexp le, map_exp e1, map_exp e2))
         | E_internal_plet (p,e1,e2) -> re (E_internal_plet (check_single_pat p, map_exp e1, map_exp e2))
         | E_internal_return e -> re (E_internal_return (map_exp e))
@@ -2091,7 +2069,6 @@ let split_defs all_errors splits defs =
       | DEF_spec _
       | DEF_default _
       | DEF_reg_dec _
-      | DEF_comm _
       | DEF_overload _
       | DEF_fixity _
       | DEF_internal_mutrec _
@@ -3140,18 +3117,12 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
     | E_assert (e1,_) -> analyse_exp fn_id env assigns e1
 
     | E_app_infix _
-    | E_internal_cast _
-    | E_internal_exp _
-    | E_sizeof_internal _
-    | E_internal_exp_user _
-    | E_comment _
-    | E_comment_struc _
     | E_internal_plet _
     | E_internal_return _
     | E_internal_value _
       -> raise (Reporting_basic.err_unreachable l
                   ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp))
-       
+
     | E_var (lexp,e1,e2) ->
        (* Really we ought to remove the assignment after e2 *)
        let d1,assigns,r1 = analyse_exp fn_id env assigns e1 in
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 8f0c0386..7c3985ae 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -48,5 +48,4 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
-include Pretty_print_lem_ast
 include Pretty_print_lem
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index b459926b..2aaf5318 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -52,5 +52,4 @@ open Ast
 open Type_check
 
 (* Prints on formatter the defs as Lem Ast nodes *)
-val pp_lem_defs : Format.formatter -> tannot defs -> unit
 val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 74e97a29..d2b140cd 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1296,9 +1296,7 @@ let doc_exp_lem, doc_let_lem =
           parens (doc_typ ctxt (typ_of r))] in
       align (parens (string "early_return" ^//^ expV true r ^//^ ta))
     | E_constraint nc -> wrap_parens (doc_nc_exp ctxt nc)
-    | E_comment _ | E_comment_struc _ -> empty
-    | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _
-    | E_internal_exp_user _ | E_internal_value _ ->
+    | E_internal_value _ ->
       raise (Reporting_basic.err_unreachable l
         "unsupported internal expression encountered while pretty-printing")
   and if_exp ctxt (elseif : bool) c t e =
@@ -1918,10 +1916,6 @@ let rec doc_def unimplemented def =
 
   | DEF_kind _ -> empty
 
-  | DEF_comm (DC_comm s) -> comment (string s)
-  | DEF_comm (DC_comm_struct d) -> comment (doc_def unimplemented d)
-
-
 let find_exc_typ defs =
   let is_exc_typ_def = function
     | DEF_type td -> string_of_id (id_of_type_def td) = "exception"
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 9897bb7c..99ab2b54 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -164,6 +164,13 @@ let is_regtyp (Typ_aux (typ, _)) env = match typ with
   | Typ_app(id, _) when string_of_id id = "register" -> true
   | _ -> false
 
+let lemnum default n =
+  if Big_int.less_equal Big_int.zero n && Big_int.less_equal n (Big_int.of_int 128) then
+    "int" ^ Big_int.to_string n
+  else if Big_int.greater_equal n Big_int.zero then
+    default n
+  else ("(int0 - " ^ (default (Big_int.abs n)) ^ ")")
+
 let doc_nexp_lem nexp =
   let nice_kid kid =
     let (Kid_aux (Var kid,l)) = orig_kid kid in
@@ -178,7 +185,7 @@ let doc_nexp_lem nexp =
        match nexp with
        | Nexp_id id -> string_of_id id
        | Nexp_var kid -> string_of_id (id_of_kid (nice_kid kid))
-       | Nexp_constant i -> Pretty_print_lem_ast.lemnum Big_int.to_string i
+       | Nexp_constant i -> lemnum Big_int.to_string i
        | Nexp_times (n1, n2) -> mangle_nexp n1 ^ "_times_" ^ mangle_nexp n2
        | Nexp_sum (n1, n2) -> mangle_nexp n1 ^ "_plus_" ^ mangle_nexp n2
        | Nexp_minus (n1, n2) -> mangle_nexp n1 ^ "_minus_" ^ mangle_nexp n2
@@ -917,9 +924,7 @@ let doc_exp_lem, doc_let_lem =
           parens (doc_typ_lem (typ_of r))] in
       align (parens (string "early_return" ^//^ expV true r ^//^ ta))
     | E_constraint _ -> string "true"
-    | E_comment _ | E_comment_struc _ -> empty
-    | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _
-    | E_internal_exp_user _ | E_internal_value _ ->
+    | E_internal_value _ ->
       raise (Reporting_basic.err_unreachable l
         "unsupported internal expression encountered while pretty-printing")
   and if_exp ctxt (elseif : bool) c t e =
@@ -1386,10 +1391,6 @@ let rec doc_def_lem def =
 
   | DEF_kind _ -> empty
 
-  | DEF_comm (DC_comm s) -> comment (string s)
-  | DEF_comm (DC_comm_struct d) -> comment (doc_def_lem d)
-
-
 let find_exc_typ defs =
   let is_exc_typ_def = function
     | DEF_type td -> string_of_id (id_of_type_def td) = "exception"
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
deleted file mode 100644
index 24b28eac..00000000
--- a/src/pretty_print_lem_ast.ml
+++ /dev/null
@@ -1,616 +0,0 @@
-(**************************************************************************)
-(*     Sail                                                               *)
-(*                                                                        *)
-(*  Copyright (c) 2013-2017                                               *)
-(*    Kathyrn Gray                                                        *)
-(*    Shaked Flur                                                         *)
-(*    Stephen Kell                                                        *)
-(*    Gabriel Kerneis                                                     *)
-(*    Robert Norton-Wright                                                *)
-(*    Christopher Pulte                                                   *)
-(*    Peter Sewell                                                        *)
-(*    Alasdair Armstrong                                                  *)
-(*    Brian Campbell                                                      *)
-(*    Thomas Bauereiss                                                    *)
-(*    Anthony Fox                                                         *)
-(*    Jon French                                                          *)
-(*    Dominic Mulligan                                                    *)
-(*    Stephen Kell                                                        *)
-(*    Mark Wassell                                                        *)
-(*                                                                        *)
-(*  All rights reserved.                                                  *)
-(*                                                                        *)
-(*  This software was developed by the University of Cambridge Computer   *)
-(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
-(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
-(*                                                                        *)
-(*  Redistribution and use in source and binary forms, with or without    *)
-(*  modification, are permitted provided that the following conditions    *)
-(*  are met:                                                              *)
-(*  1. Redistributions of source code must retain the above copyright     *)
-(*     notice, this list of conditions and the following disclaimer.      *)
-(*  2. Redistributions in binary form must reproduce the above copyright  *)
-(*     notice, this list of conditions and the following disclaimer in    *)
-(*     the documentation and/or other materials provided with the         *)
-(*     distribution.                                                      *)
-(*                                                                        *)
-(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
-(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
-(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
-(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
-(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
-(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
-(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
-(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
-(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
-(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
-(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
-(*  SUCH DAMAGE.                                                          *)
-(**************************************************************************)
-
-open Type_check
-open Ast
-open Format
-open Pretty_print_common
-
-(****************************************************************************
- * annotated source to Lem ast pretty printer
-****************************************************************************)
-
-let rec list_pp i_format l_format =
-  fun ppf l ->
-    match l with
-    | [] -> fprintf ppf ""
-    | [i] -> fprintf ppf "%a" l_format i
-    | i::is -> fprintf ppf "%a%a" i_format i (list_pp i_format l_format) is
-
-let pp_option_lem some_format =
-  fun ppf opt ->
-    match opt with
-    | Some a -> fprintf ppf "(Just %a)" some_format a
-    | None -> fprintf ppf "Nothing"
-
-let pp_bool_lem ppf b = fprintf ppf (if b then "true" else "false")
-
-let kwd ppf s = fprintf ppf "%s" s
-let base ppf s = fprintf ppf "%s" s
-let quot_string ppf s = fprintf ppf "\"%s\"" s
-
-let lemnum default n =
-  if Big_int.less_equal Big_int.zero n && Big_int.less_equal n (Big_int.of_int 128) then
-    "int" ^ Big_int.to_string n
-  else if Big_int.greater_equal n Big_int.zero then
-    default n
-  else ("(int0 - " ^ (default (Big_int.abs n)) ^ ")")
-
-let pp_format_id (Id_aux(i,_)) =
-  match i with
-  | Id(i) -> i
-  | DeIid(x) -> "(deinfix " ^ x ^ ")"
-
-let pp_format_var (Kid_aux(Var v,_)) = v
-
-let rec pp_format_l_lem = function
-  | Parse_ast.Unknown -> "Unknown"
-  | _ -> "Unknown"(*
-  | Parse_ast.Int(s,None) -> "(Int \"" ^ s ^ "\" Nothing)"
-  | Parse_ast.Int(s,(Some l)) -> "(Int \"" ^  s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))"
-  | Parse_ast.Range(p1,p2) -> "(Range \"" ^ p1.Lexing.pos_fname ^ "\" " ^
-                               (string_of_int p1.Lexing.pos_lnum) ^ " " ^
-                               (string_of_int (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) ^ " " ^
-                               (string_of_int p2.Lexing.pos_lnum) ^ " " ^
-                              (string_of_int (p2.Lexing.pos_cnum - p2.Lexing.pos_bol)) ^ ")"
-  | Parse_ast.Generated l -> "(Generated " ^ (pp_format_l_lem l) ^ ")"
-  | _ -> "Unknown"*)
-
-let pp_lem_l ppf l = base ppf (pp_format_l_lem l)
-
-let pp_format_id_lem (Id_aux(i,l)) =
-  "(Id_aux " ^
-    (match i with
-      | Id(i) -> "(Id \"" ^ i ^ "\")"
-      | DeIid(x) -> "(DeIid \"" ^ x ^ "\")") ^ " " ^
-   (pp_format_l_lem l) ^ ")"
-
-let pp_lem_id ppf id = base ppf (pp_format_id_lem id)
-
-let pp_format_var_lem (Kid_aux(Var v,l)) = "(Kid_aux (Var \"" ^ v ^ "\") " ^ (pp_format_l_lem l) ^ ")"
-
-let pp_lem_var ppf var = base ppf (pp_format_var_lem var)
-
-let pp_format_bkind_lem (BK_aux(k,l)) =
-  "(BK_aux " ^
-  (match k with
-    | BK_type -> "BK_type"
-    | BK_int -> "BK_int"
-    | BK_order -> "BK_order") ^ " " ^
-  (pp_format_l_lem l) ^ ")"
-
-let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk)
-
-let pp_format_kind_lem (K_aux(K_kind(klst),l)) =
-  "(K_aux (K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "]) " ^ (pp_format_l_lem l) ^ ")"
-
-let pp_lem_kind ppf k = base ppf (pp_format_kind_lem k)
-
-let rec pp_format_typ_lem (Typ_aux(t,l)) =
-  "(Typ_aux " ^
-  (match t with
-    | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")"
-    | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")"
-    | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^
-                              pp_format_typ_lem ret ^ " " ^
-                              (pp_format_effects_lem efct) ^ ")"
-    | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])"
-    | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])"
-    | Typ_exist(kids,nc,typ) -> "(Typ_exist [" ^ list_format ";" pp_format_var_lem kids ^ "] " ^ pp_format_nexp_constraint_lem nc ^ " " ^ pp_format_typ_lem typ ^ ")") ^ " " ^
-    (pp_format_l_lem l) ^ ")"
-and pp_format_nexp_lem (Nexp_aux(n,l)) =
-  "(Nexp_aux " ^
-  (match n with
-   | Nexp_id(i) -> "(Nexp_id " ^ pp_format_id_lem i ^ ")"
-   | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
-   | Nexp_app(op,args) -> "(Nexp_app [" ^ Util.string_of_list ", " pp_format_nexp_lem args ^ "])"
-   | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum Big_int.to_string i) ^ ")"
-   | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
-   | Nexp_minus(n1,n2) -> "(Nexp_minus " ^ (pp_format_nexp_lem n1)^ " " ^ (pp_format_nexp_lem n2) ^ ")"
-   | Nexp_times(n1,n2) -> "(Nexp_times " ^  (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
-   | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")"
-   | Nexp_neg(n1) -> "(Nexp_neg " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^
-  (pp_format_l_lem l) ^ ")"
-and pp_format_ord_lem (Ord_aux(o,l)) =
-  "(Ord_aux " ^
-  (match o with
-    | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")"
-    | Ord_inc -> "Ord_inc"
-    | Ord_dec -> "Ord_dec") ^ " " ^
-   (pp_format_l_lem l) ^ ")"
-and pp_format_base_effect_lem (BE_aux(e,l)) =
-  "(BE_aux " ^
-  (match e with
-    | BE_rreg -> "BE_rreg"
-    | BE_wreg -> "BE_wreg"
-    | BE_rmem -> "BE_rmem"
-    | BE_rmemt -> "BE_rmemt"
-    | BE_wmem -> "BE_wmem"
-    | BE_wmv  -> "BE_wmv"
-    | BE_wmvt  -> "BE_wmvt"
-    | BE_eamem -> "BE_eamem"
-    | BE_exmem -> "BE_exmem"
-    | BE_barr -> "BE_barr"
-    | BE_depend -> "BE_depend"
-    | BE_undef -> "BE_undef"
-    | BE_unspec -> "BE_unspec"
-    | BE_nondet -> "BE_nondet"
-    (*| BE_lset -> "BE_lset"
-    | BE_lret -> "BE_lret"*)
-    | BE_escape -> "BE_escape") ^ " " ^
-  (pp_format_l_lem l) ^ ")"
-and pp_format_effects_lem (Effect_aux(e,l)) =
-  "(Effect_aux " ^
-  (match e with
-  | Effect_set(efcts) ->
-    "(Effect_set [" ^
-      (list_format "; " pp_format_base_effect_lem efcts) ^ " ])") ^ " " ^
-  (pp_format_l_lem l) ^ ")"
-and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) =
-  "(Typ_arg_aux " ^
-  (match t with
-   | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")"
-   | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")"
-   | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")") ^ " " ^
-  (pp_format_l_lem l) ^ ")"
-and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
-  "(NC_aux " ^
-  (match nc with
-  | NC_equal(n1,n2) -> "(NC_equal " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
-  | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
-  | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
-  | NC_not_equal(n1,n2) -> "(NC_not_equal " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
-  | NC_or(nc1,nc2) -> "(NC_or " ^ pp_format_nexp_constraint_lem nc1 ^ " " ^ pp_format_nexp_constraint_lem nc2 ^ ")"
-  | NC_and(nc1,nc2) -> "(NC_and " ^ pp_format_nexp_constraint_lem nc1 ^ " " ^ pp_format_nexp_constraint_lem nc2 ^ ")"
-  | NC_true -> "NC_true"
-  | NC_false -> "NC_false"
-  | NC_set(id,bounds) -> "(NC_set " ^
-    pp_format_var_lem id ^
-      " [" ^
-      list_format "; " Big_int.to_string bounds ^
-      "])") ^ " " ^
-  (pp_format_l_lem l) ^ ")"
-
-let pp_lem_typ ppf t = base ppf (pp_format_typ_lem t)
-let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n)
-let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o)
-let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e)
-let pp_lem_beffect ppf be = base ppf (pp_format_base_effect_lem be)
-let pp_lem_loop ppf l =
-  let l_str = match l with
-  | While -> "While"
-  | Until -> "Until" in
-  base ppf l_str
-let pp_lem_prec ppf p =
-  let p_str = match p with
-  | Infix -> "Infix"
-  | InfixL -> "InfixL"
-  | InfixR -> "InfixR" in
-  base ppf p_str
-
-let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc)
-
-let pp_format_qi_lem (QI_aux(qi,lq)) =
-  "(QI_aux " ^
-  (match qi with
-  | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint_lem n_const ^ ")"
-  | QI_id(KOpt_aux(ki,lk)) ->
-    "(QI_id (KOpt_aux " ^
-    (match ki with
-    | KOpt_none(var) -> "(KOpt_none " ^ pp_format_var_lem var ^ ")"
-    | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ " " ^
-      (pp_format_l_lem lk) ^ "))") ^ " " ^
-  (pp_format_l_lem lq) ^ ")"
-
-let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi)
-
-let pp_format_typquant_lem (TypQ_aux(tq,l)) =
-  "(TypQ_aux " ^
-  (match tq with
-  | TypQ_no_forall -> "TypQ_no_forall"
-  | TypQ_tq(qlist) ->
-    "(TypQ_tq [" ^
-    (list_format "; " pp_format_qi_lem qlist) ^
-    "])") ^ " " ^
-  (pp_format_l_lem l) ^ ")"
-
-let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq)
-
-let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),l)) =
-  "(TypSchm_aux (TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ") " ^
-                (pp_format_l_lem l) ^ ")"
-
-let pp_lem_typscm ppf ts = base ppf (pp_format_typscm_lem ts)
-
-let pp_format_lit_lem (L_aux(lit,l)) =
-  "(L_aux " ^
-  (match lit with
-  | L_unit -> "L_unit"
-  | L_zero -> "L_zero"
-  | L_one -> "L_one"
-  | L_true -> "L_true"
-  | L_false -> "L_false"
-  | L_num(i) -> "(L_num " ^ (lemnum Big_int.to_string i) ^ ")"
-  | L_hex(n) -> "(L_hex \"" ^ n ^ "\")"
-  | L_bin(n) -> "(L_bin \"" ^ n ^ "\")"
-  | L_undef -> "L_undef"
-  | L_string(s) -> "(L_string \"" ^ s ^ "\")"
-  | L_real(s) -> "(L_real \"" ^ s ^ "\")") ^ " " ^
-  (pp_format_l_lem l) ^ ")"
-
-let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l)
-
-
-let tag_id id env =
-  if Env.is_extern id env "lem_ast" then
-    "Tag_extern (Just \"" ^ Ast_util.string_of_id id ^ "\")"
-  else if Env.is_union_constructor id env then
-    "Tag_ctor"
-  else
-    "Tag_empty"
-
-let pp_format_annot ?tag:(t="Tag_empty") = function
-  | None -> "Nothing"
-  | Some (_, typ, eff) ->
-     "(Just ("
-     ^ pp_format_typ_lem typ ^ ", "
-     ^ t ^ ", "
-     ^ "[], "
-     ^ pp_format_effects_lem eff ^ ", "
-     ^ pp_format_effects_lem eff
-     ^ "))"
-
-let pp_annot ppf ant = base ppf (pp_format_annot ant)
-
-let pp_annot_tag tag ppf ant = base ppf (pp_format_annot ~tag:tag ant)
-
-let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
-  "(P_aux " ^
-  (match p with
-  | P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")"
-  | P_wild -> "P_wild"
-  | P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")"
-  | P_var(pat,_) -> "(P_var " ^ pp_format_pat_lem pat ^ ")" (* FIXME *)
-  | P_as(pat,id) -> "(P_as " ^ pp_format_pat_lem pat ^ " " ^ pp_format_id_lem id ^ ")"
-  | P_typ(typ,pat) -> "(P_typ " ^ pp_format_typ_lem typ ^ " " ^ pp_format_pat_lem pat ^ ")"
-  | P_app(id,pats) -> "(P_app " ^ pp_format_id_lem id ^ " [" ^
-                      list_format "; " pp_format_pat_lem pats ^ "])"
-  | P_record(fpats,_) -> "(P_record [" ^
-                       list_format "; " (fun (FP_aux(FP_Fpat(id,fpat),_)) ->
-                                          "(FP_Fpat " ^ pp_format_id_lem id ^ " " ^ pp_format_pat_lem fpat ^ ")") fpats
-                       ^ "])"
-  | P_vector(pats) -> "(P_vector [" ^ list_format "; " pp_format_pat_lem pats ^ "])"
-  | P_vector_concat(pats) -> "(P_vector_concat [" ^ list_format "; " pp_format_pat_lem pats ^ "])"
-  | P_tup(pats) -> "(P_tup [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
-  | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
-  | P_cons(pat,pat') -> "(P_cons " ^ pp_format_pat_lem pat ^ " " ^ pp_format_pat_lem pat' ^ ")") ^
-  " (" ^ pp_format_l_lem l ^ ", " ^ pp_format_annot annot ^ "))"
-
-let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p)
-
-let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) =
-  let print_lb ppf lb =
-    match lb with
-      | LB_val(pat,exp) ->
-        fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val" pp_lem_pat pat  pp_lem_exp exp in
-  fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot
-
-and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) =
-  let env = env_of exp in
-  let print_e ppf e =
-    match e with
-    | E_block(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]"
-      kwd "(E_block"
-      (list_pp pp_semi_lem_exp pp_lem_exp) exps
-      kwd ")" pp_lem_l l pp_annot annot
-    | E_nondet(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]"
-      kwd "(E_nondet"
-      (list_pp pp_semi_lem_exp pp_lem_exp) exps
-      kwd ")" pp_lem_l l pp_annot annot
-    | E_id(id) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_id" pp_lem_id id pp_lem_l l (pp_annot_tag (tag_id id env)) annot
-    | E_ref(id) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_ref" pp_lem_id id pp_lem_l l (pp_annot_tag (tag_id id env)) annot
-    | E_lit(lit) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_lit" pp_lem_lit lit pp_lem_l l pp_annot annot
-    | E_cast(typ,exp) ->
-      fprintf ppf "@[<0>(E_aux (E_cast %a %a) (%a, %a))@]" pp_lem_typ typ pp_lem_exp exp pp_lem_l l pp_annot annot
-    | E_internal_cast((_,None),e) -> pp_lem_exp ppf e
-    | E_app(f,args) -> fprintf ppf "@[<0>(E_aux (E_app %a [%a]) (%a, %a))@]"
-                         pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args pp_lem_l l (pp_annot_tag (tag_id f env)) annot
-    | E_app_infix(l',op,r) -> fprintf ppf "@[<0>(E_aux (E_app_infix %a %a %a) (%a, %a))@]"
-                                pp_lem_exp l' pp_lem_id op pp_lem_exp r pp_lem_l l pp_annot annot
-    | E_tuple(exps) -> fprintf ppf "@[<0>(E_aux (E_tuple [%a]) (%a, %a))@]"
-                         (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
-    | E_if(c,t,e) -> fprintf ppf "@[<0>(E_aux (E_if %a @[<1>%a@] @[<1> %a@]) (%a, %a))@]"
-                       pp_lem_exp c pp_lem_exp t pp_lem_exp e pp_lem_l l pp_annot annot
-    | E_for(id,exp1,exp2,exp3,order,exp4) ->
-      fprintf ppf "@[<0>(E_aux (E_for %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]"
-        pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3
-        pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot
-    | E_loop(loop,cond,body) ->
-      fprintf ppf "@[<0>(E_aux (E_loop %a %a @ @[<1> %a @]) (%a, %a))@]"
-        pp_lem_loop loop pp_lem_exp cond pp_lem_exp body pp_lem_l l pp_annot annot
-    | E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]"
-                          kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
-    | E_vector_access(v,e) ->
-      fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]"
-        kwd "E_vector_access" pp_lem_exp v pp_lem_exp e pp_lem_l l pp_annot annot
-    | E_vector_subrange(v,e1,e2) ->
-      fprintf ppf "@[<0>(E_aux (E_vector_subrange %a %a %a) (%a, %a))@]"
-        pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot
-    | E_vector_update(v,e1,e2) ->
-      fprintf ppf "@[<0>(E_aux (E_vector_update %a %a %a) (%a, %a))@]"
-        pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot
-    | E_vector_update_subrange(v,e1,e2,e3) ->
-      fprintf ppf "@[<0>(E_aux (E_vector_update_subrange %a %a %a %a) (%a, %a))@]"
-        pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 pp_lem_l l pp_annot annot
-    | E_vector_append(v1,v2) ->
-      fprintf ppf "@[<0>(E_aux (E_vector_append %a %a) (%a, %a))@]"
-        pp_lem_exp v1 pp_lem_exp v2 pp_lem_l l pp_annot annot
-    | E_list(exps) -> fprintf ppf "@[<0>(E_aux (E_list [%a]) (%a, %a))@]"
-                        (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
-    | E_cons(e1,e2) -> fprintf ppf "@[<0>(E_aux (E_cons %a %a) (%a, %a))@]"
-                         pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot
-    | E_record(FES_aux(FES_Fexps(fexps,_),(fl,fannot))) ->
-      fprintf ppf "@[<0>(E_aux (E_record (FES_aux (FES_Fexps [%a] false) (%a,%a))) (%a, %a))@]"
-        (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps pp_lem_l fl pp_annot fannot pp_lem_l l pp_annot annot
-    | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),(fl,fannot)))) ->
-      fprintf ppf "@[<0>(E_aux (E_record_update %a (FES_aux (FES_Fexps [%a] false) (%a,%a))) (%a,%a))@]"
-        pp_lem_exp exp (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps
-        pp_lem_l fl pp_annot fannot pp_lem_l l pp_annot annot
-    | E_field(fexp,id) -> fprintf ppf "@[<0>(E_aux (E_field %a %a) (%a, %a))@]"
-                            pp_lem_exp fexp pp_lem_id id pp_lem_l l pp_annot annot
-    | E_case(exp,pexps) ->
-      fprintf ppf "@[<0>(E_aux (E_case %a [%a]) (%a, %a))@]"
-        pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot
-    | E_try(exp,pexps) ->
-      fprintf ppf "@[<0>(E_aux (E_try %a [%a]) (%a, %a))@]"
-        pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot
-    | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (E_let %a %a) (%a, %a))@]"
-                          pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot
-    | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (E_assign %a %a) (%a, %a))@]"
-                              pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot
-    | E_sizeof nexp ->
-      fprintf ppf "@[<0>(E_aux (E_sizeof %a) (%a, %a))@]" pp_lem_nexp nexp pp_lem_l l pp_annot annot
-    | E_constraint nc ->
-      fprintf ppf "@[<0>(E_aux (E_constraint %a) (%a, %a))@]" pp_lem_nexp_constraint nc pp_lem_l l pp_annot annot
-    | E_exit exp ->
-      fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
-    | E_throw exp ->
-      fprintf ppf "@[<0>(E_aux (E_throw %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
-    | E_return exp ->
-      fprintf ppf "@[<0>(E_aux (E_return %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
-    | E_assert(c,msg) ->
-      fprintf ppf "@[<0>(E_aux (E_assert %a %a) (%a, %a))@]" pp_lem_exp c pp_lem_exp msg pp_lem_l l pp_annot annot
-    | E_comment _ | E_comment_struc _ ->
-      fprintf ppf "@[(E_aux (E_lit (L_aux L_unit %a)) (%a,%a))@]" pp_lem_l l pp_lem_l l pp_annot annot
-    | E_internal_cast _ | E_internal_exp _ ->
-      raise (Reporting_basic.err_unreachable l "Found internal cast or exp")
-    | E_internal_exp_user _ -> (raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_exp_user"))
-    | E_sizeof_internal _ -> (raise (Reporting_basic.err_unreachable l "Internal sizeof not removed"))
-    | E_var (lexp,exp1,exp2) ->
-      fprintf ppf "@[<0>(E_aux (E_var %a %a %a) (%a, %a))@]"
-        pp_lem_lexp lexp pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_l l pp_annot annot
-    | E_internal_return exp ->
-      fprintf ppf "@[<0>(E_aux (E_internal_return %a) (%a, %a))@]"
-        pp_lem_exp exp pp_lem_l l pp_annot annot
-    | E_internal_plet (pat,exp1,exp2) ->
-      fprintf ppf "@[<0>(E_aux (E_internal_plet %a %a %a) (%a, %a))@]"
-        pp_lem_pat pat pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_l l pp_annot annot
-    | E_internal_value _ -> raise (Reporting_basic.err_unreachable l "Found internal_value")
-  in
-  print_e ppf e
-
-and pp_semi_lem_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_lem_exp e kwd ";"
-
-and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),(l,annot))) =
-  fprintf ppf "@[<1>(FE_aux (FE_Fexp %a %a) (%a, %a))@]" pp_lem_id id pp_lem_exp exp pp_lem_l l pp_annot annot
-and pp_semi_lem_fexp ppf fexp = fprintf ppf "@[<1>%a %a@]" pp_lem_fexp fexp kwd ";"
-
-and pp_lem_case ppf = function
-| Pat_aux(Pat_exp(pat,exp),(l,annot)) ->
-  fprintf ppf "@[<1>(Pat_aux (Pat_exp %a@ %a) (%a, %a))@]" pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot
-| Pat_aux(Pat_when(pat,guard,exp),(l,annot)) ->
-  fprintf ppf "@[<1>(Pat_aux (Pat_when %a@ %a %a) (%a, %a))@]" pp_lem_pat pat pp_lem_exp guard pp_lem_exp exp pp_lem_l l pp_annot annot
-and pp_semi_lem_case ppf case = fprintf ppf "@[<1>%a %a@]" pp_lem_case case kwd ";"
-
-and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) =
-  let print_le ppf lexp =
-    match lexp with
-    | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
-    | LEXP_deref exp ->
-       fprintf ppf "(LEXP_deref %a)" pp_lem_exp exp
-    | LEXP_memory(id,args) ->
-       fprintf ppf "(LEXP_memory %a [%a])" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
-    | LEXP_cast(typ,id) -> fprintf ppf "(LEXP_cast %a %a)" pp_lem_typ typ pp_lem_id id
-    | LEXP_tup tups -> fprintf ppf "(LEXP_tup [%a])" (list_pp pp_semi_lem_lexp pp_lem_lexp) tups
-    | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
-    | LEXP_vector_range(v,e1,e2) ->
-       fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v  pp_lem_exp e1 pp_lem_exp e2
-    | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id
-  in
-  fprintf ppf "@[(LEXP_aux %a (%a, %a))@]" print_le lexp pp_lem_l l pp_annot annot
-and pp_semi_lem_lexp ppf le = fprintf ppf "@[<1>%a%a@]" pp_lem_lexp le kwd ";"
-
-let pp_semi_lem_id ppf id = fprintf ppf "@[<1>%a%a@]" pp_lem_id id kwd ";"
-
-let pp_lem_default ppf (DT_aux(df,l)) =
-  let print_de ppf df =
-    match df with
-      | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var
-      | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
-      | DT_order(ord) -> fprintf ppf "@[<0>(DT_order %a)@]" pp_lem_ord ord
-  in
-  fprintf ppf "@[<0>(DT_aux %a %a)@]" print_de df pp_lem_l l
-
-(* FIXME *)
-let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
-  let print_spec ppf (VS_val_spec(ts, id, ext_opt, is_cast)) =
-    fprintf ppf "@[<0>(%a %a %a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id (pp_option_lem quot_string) None pp_bool_lem is_cast
-  in
-  fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot
-
-let pp_lem_namescm ppf (Name_sect_aux(ns,l)) =
-  match ns with
-  | Name_sect_none -> fprintf ppf "(Name_sect_aux Name_sect_none %a)" pp_lem_l l
-  | Name_sect_some(s) -> fprintf ppf "(Name_sect_aux (Name_sect_some \"%s\") %a)" s pp_lem_l l
-
-let rec pp_lem_range ppf (BF_aux(r,l)) =
-  match r with
-  | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" (Big_int.to_int i) pp_lem_l l
-  | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" (Big_int.to_int i1) (Big_int.to_int i2) pp_lem_l l
-  | BF_concat(ir1,ir2) -> fprintf ppf "(BF_aux (BF_concat %a %a) %a)" pp_lem_range ir1 pp_lem_range ir2 pp_lem_l l
-
-let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
-  let print_td ppf td =
-    match td with
-      | TD_abbrev(id,namescm,typschm) ->
-        fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
-      | TD_record(id,nm,typq,fs,_) ->
-        let f_pp ppf (typ,id) =
-          fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
-        fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
-          kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
-      | TD_variant(id,nm,typq,ar,_) ->
-        let a_pp ppf (Tu_aux(Tu_ty_id(typ,id),l)) =
-          fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]"
-                  pp_lem_typ typ pp_lem_id id pp_lem_l l
-        in
-        fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
-          kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar
-      | TD_enum(id,ns,enums,_) ->
-        let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
-        fprintf ppf "@[<0>(%a %a %a [%a] false)@]"
-          kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
-      | TD_bitfield(id,typ,rs) ->
-        let pp_rid ppf (id, r) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
-        let pp_rids = (list_pp pp_rid pp_rid) in
-        fprintf ppf "@[<0>(%a %a %a [%a])@]"
-          kwd "TD_bitfield" pp_lem_id id pp_lem_typ typ pp_rids rs
-  in
-  fprintf ppf "@[<0>(TD_aux %a (%a, %a))@]" print_td td pp_lem_l l pp_annot annot
-
-let pp_lem_kindef ppf (KD_aux(kd,(l,annot))) =
-  let print_kd ppf kd =
-    match kd with
-    | KD_nabbrev(kind,id,namescm,n) ->
-      fprintf ppf "@[<0>(KD_nabbrev %a %a %a %a)@]"
-        pp_lem_kind kind pp_lem_id id pp_lem_namescm namescm pp_lem_nexp n
-  in
-  fprintf ppf "@[<0>(KD_aux %a (%a, %a))@]" print_kd kd pp_lem_l l pp_annot annot
-
-let pp_lem_rec ppf (Rec_aux(r,l)) =
-  match r with
-  | Rec_nonrec -> fprintf ppf "(Rec_aux Rec_nonrec %a)" pp_lem_l l
-  | Rec_rec -> fprintf ppf "(Rec_aux Rec_rec %a)" pp_lem_l l
-
-let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,l)) =
-  match t with
-  | Typ_annot_opt_some(tq,typ) ->
-    fprintf ppf "(Typ_annot_opt_aux (Typ_annot_opt_some %a %a) %a)" pp_lem_typquant tq pp_lem_typ typ pp_lem_l l
-  | Typ_annot_opt_none ->
-    fprintf ppf "(Typ_annot_opt_aux (Typ_annot_opt_none) %a)" pp_lem_l l
-
-let pp_lem_effects_opt ppf (Effect_opt_aux(e,l)) =
-  match e with
-  | Effect_opt_pure -> fprintf ppf "(Effect_opt_aux Effect_opt_pure %a)" pp_lem_l l
-  | Effect_opt_effect e -> fprintf ppf "(Effect_opt_aux (Effect_opt_effect %a) %a)" pp_lem_effects e pp_lem_l l
-
-let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pexp),(l,annot))) =
-  fprintf ppf "@[<0>(FCL_aux (%a %a %a) (%a,%a))@]@\n"
-    kwd "FCL_Funcl" pp_lem_id id pp_lem_case pexp pp_lem_l l pp_annot annot
-
-let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) =
-  let pp_funcls ppf funcl = fprintf ppf "%a %a" pp_lem_funcl funcl kwd ";" in
-  fprintf ppf "@[<0>(FD_aux (%a %a %a %a [%a]) (%a, %a))@]"
-    kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls
-    pp_lem_l l pp_annot annot
-
-let pp_lem_aspec ppf (AL_aux(aspec,(l,annot))) =
-  let pp_reg_id ppf (RI_aux((RI_id ri),(l,annot))) =
-    fprintf ppf "@[<0>(RI_aux (RI_id %a) (%a,%a))@]" pp_lem_id ri pp_lem_l l pp_annot annot in
-  match aspec with
-    | AL_subreg(reg,subreg) ->
-      fprintf ppf "@[<0>(AL_aux (AL_subreg %a %a) (%a,%a))@]"
-        pp_reg_id reg pp_lem_id subreg pp_lem_l l pp_annot annot
-    | AL_bit(reg,ac) ->
-      fprintf ppf "@[<0>(AL_aux (AL_bit %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_exp ac pp_lem_l l pp_annot annot
-    | AL_slice(reg,b,e) ->
-      fprintf ppf "@[<0>(AL_aux (AL_slice %a %a %a) (%a,%a))@]"
-        pp_reg_id reg pp_lem_exp b pp_lem_exp e pp_lem_l l pp_annot annot
-    | AL_concat(f,s) ->
-      fprintf ppf "@[<0>(AL_aux (AL_concat %a %a) (%a,%a))@]" pp_reg_id f pp_reg_id s pp_lem_l l pp_annot annot
-
-let pp_lem_dec ppf (DEC_aux(reg,(l,annot))) =
-  match reg with
-  | DEC_reg(typ,id) ->
-    fprintf ppf "@[<0>(DEC_aux (DEC_reg %a %a) (%a,%a))@]" pp_lem_typ typ pp_lem_id id pp_lem_l l pp_annot annot
-  | DEC_alias(id,alias_spec) ->
-    fprintf ppf "@[<0>(DEC_aux (DEC_alias %a %a) (%a, %a))@]"
-      pp_lem_id id pp_lem_aspec alias_spec pp_lem_l l pp_annot annot
-  | DEC_typ_alias(typ,id,alias_spec) ->
-    fprintf ppf "@[<0>(DEC_aux (DEC_typ_alias %a %a %a) (%a, %a))@]"
-      pp_lem_typ typ pp_lem_id id pp_lem_aspec alias_spec pp_lem_l l pp_annot annot
-
-let rec pp_lem_def ppf d =
-  match d with
-  | DEF_default(df) -> fprintf ppf "(DEF_default %a);@\n" pp_lem_default df
-  | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a);@\n" pp_lem_spec v_spec
-  | DEF_overload(id,ids) -> fprintf ppf "(DEF_overload %a [%a]);@\n" pp_lem_id id (list_pp pp_semi_lem_id pp_lem_id) ids
-  | DEF_type(t_def) -> fprintf ppf "(DEF_type %a);@\n" pp_lem_typdef t_def
-  | DEF_kind(k_def) -> fprintf ppf "(DEF_kind %a);@\n" pp_lem_kindef k_def
-  | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);@\n" pp_lem_fundef f_def
-  | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind
-  | DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);@\n" pp_lem_dec dec
-  | DEF_comm d -> fprintf ppf ""
-  | DEF_fixity (prec, n, id) -> fprintf ppf "(DEF_fixity %a %s %a);@\n" pp_lem_prec prec (lemnum Big_int.to_string n) pp_lem_id id
-  | DEF_internal_mutrec f_defs -> List.iter (fun f_def -> pp_lem_def ppf (DEF_fundef f_def)) f_defs
-  | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs")
-
-let pp_lem_defs ppf (Defs(defs)) =
-  fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index d59bd132..f3556343 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -573,8 +573,6 @@ let rec doc_def def = group (match def with
      separate space [doc_prec prec; doc_int n; doc_id id]
   | DEF_overload (id, ids) ->
      separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
-  | DEF_comm (DC_comm s) -> string "TOPLEVEL"
-  | DEF_comm (DC_comm_struct d) -> string "TOPLEVEL"
   ) ^^ hardline
 
 let doc_defs (Defs(defs)) =
diff --git a/src/process_file.ml b/src/process_file.ml
index 6afbae3d..958720ea 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -52,7 +52,6 @@ open PPrint
 open Pretty_print_common
 
 type out_type =
-  | Lem_ast_out
   | Lem_out of string list
   | Coq_out of string list
 
@@ -330,28 +329,16 @@ let rec iterate (f : int -> unit) (n : int) : unit =
 
 let output1 libpath out_arg filename defs  =
   let f' = Filename.basename (Filename.chop_extension filename) in
-    match out_arg with
-      | Lem_ast_out ->
-	begin
-	  let (o, ext_o) = open_output_with_check (f' ^ ".lem") in
-	  Format.fprintf o "(* %s *)@\n" (generated_line filename);
-          Format.fprintf o "open import Interp_ast@\n";
-	  Format.fprintf o "open import Pervasives@\n";
-          Format.fprintf o "(*Supply common numeric constants at the right type to alleviate repeated calls to typeclass macro*)\n";
-          iterate (fun n -> Format.fprintf o "let int%i : integer = integerFromNat %i\n" (n - 1) (n - 1)) 129;
-          Format.fprintf o "let defs = ";
-	  Pretty_print.pp_lem_defs o defs;
-	  close_output_with_check ext_o
-	end
-      | Lem_out libs ->
-        output_lem f' libs defs
-      | Coq_out libs ->
-         output_coq f' libs defs
+  match out_arg with
+  | Lem_out libs ->
+     output_lem f' libs defs
+  | Coq_out libs ->
+     output_coq f' libs defs
 
 let output libpath out_arg files =
   List.iter
     (fun (f, defs) ->
-       output1 libpath out_arg f defs)
+      output1 libpath out_arg f defs)
     files
 
 let rewrite_step defs (name,rewriter) =
diff --git a/src/process_file.mli b/src/process_file.mli
index a4e31890..ded20dd2 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -70,7 +70,6 @@ val opt_ddump_rewrite_ast : ((string * int) option) ref
 val opt_dno_cast : bool ref
 
 type out_type =
-  | Lem_ast_out
   | Lem_out of string list (* If present, the strings are files to open in the lem backend*)
   | Coq_out of string list (* If present, the strings are files to open in the coq backend*)
 
diff --git a/src/rewriter.ml b/src/rewriter.ml
index b67f9c49..0f8bb905 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -171,12 +171,8 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
     | E_let (lb,e) -> union_effects (effect_of_lb lb) (effect_of e)
     | E_assign (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e)
     | E_exit e | E_return e | E_throw e -> union_effects eff (effect_of e)
-    | E_sizeof _ | E_sizeof_internal _ | E_constraint _ -> no_effect
+    | E_sizeof _ | E_constraint _ -> no_effect
     | E_assert (c,m) -> union_effects eff (union_eff_exps [c; m])
-    | E_comment _ | E_comment_struc _ -> no_effect
-    | E_internal_cast (_,e) -> effect_of e
-    | E_internal_exp _ -> no_effect
-    | E_internal_exp_user _ -> no_effect
     | E_var (lexp,e1,e2) ->
       union_effects (effect_of_lexp lexp)
         (union_effects (effect_of e1) (effect_of e2))
@@ -312,7 +308,6 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   let rewrap e = E_aux (e,(l,annot)) in
   let rewrite = rewriters.rewrite_exp rewriters in
   match exp with
-  | E_comment _ | E_comment_struc _ -> rewrap exp
   | E_block exps -> rewrap (E_block (List.map rewrite exps))
   | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps))
   | E_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) ->
@@ -359,8 +354,6 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   | E_exit e -> rewrap (E_exit (rewrite e))
   | E_return e -> rewrap (E_return (rewrite e))
   | E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2))
-  | E_internal_cast (casted_annot,exp) ->
-    rewrap (E_internal_cast (casted_annot, rewrite exp))
   | E_var (lexp, e1, e2) ->
      rewrap (E_var (rewriters.rewrite_lexp rewriters lexp, rewriters.rewrite_exp rewriters e1, rewriters.rewrite_exp rewriters e2))
   | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced")
@@ -398,7 +391,7 @@ let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls
 let rewrite_def rewriters d = match d with
   | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), annot)) ->
      DEF_reg_dec (DEC_aux (DEC_config (id, typ, rewriters.rewrite_exp rewriters exp), annot))
-  | DEF_type _ | DEF_mapdef _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ | DEF_fixity _ -> d
+  | DEF_type _ | DEF_mapdef _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_overload _ | DEF_fixity _ -> d
   | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef)
   | DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs)
   | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
@@ -548,12 +541,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; e_throw                  : 'exp -> 'exp_aux
   ; e_return                 : 'exp -> 'exp_aux
   ; e_assert                 : 'exp * 'exp -> 'exp_aux
-  ; e_internal_cast          : 'a annot * 'exp -> 'exp_aux
-  ; e_internal_exp           : 'a annot -> 'exp_aux
-  ; e_internal_exp_user      : 'a annot * 'a annot -> 'exp_aux
-  ; e_comment                : string -> 'exp_aux
-  ; e_comment_struc          : 'exp -> 'exp_aux
-  ; e_internal_let           : 'lexp * 'exp * 'exp -> 'exp_aux
+  ; e_var           : 'lexp * 'exp * 'exp -> 'exp_aux
   ; e_internal_plet          : 'pat * 'exp * 'exp -> 'exp_aux
   ; e_internal_return        : 'exp -> 'exp_aux
   ; e_internal_value         : Value.value -> 'exp_aux
@@ -622,15 +610,8 @@ let rec fold_exp_aux alg = function
   | E_throw e -> alg.e_throw (fold_exp alg e)
   | E_return e -> alg.e_return (fold_exp alg e)
   | E_assert(e1,e2) -> alg.e_assert (fold_exp alg e1, fold_exp alg e2)
-  | E_internal_cast (annot,e) -> alg.e_internal_cast (annot, fold_exp alg e)
-  | E_internal_exp annot -> alg.e_internal_exp annot
-  | E_sizeof_internal a -> raise (Reporting_basic.err_unreachable (Parse_ast.Unknown)
-      "E_sizeof_internal encountered during rewriting")
-  | E_internal_exp_user (annot1,annot2) -> alg.e_internal_exp_user (annot1,annot2)
-  | E_comment c -> alg.e_comment c
-  | E_comment_struc e -> alg.e_comment_struc (fold_exp alg e)
   | E_var (lexp,e1,e2) ->
-     alg.e_internal_let (fold_lexp alg lexp, fold_exp alg e1, fold_exp alg e2)
+     alg.e_var (fold_lexp alg lexp, fold_exp alg e1, fold_exp alg e2)
   | E_internal_plet (pat,e1,e2) ->
      alg.e_internal_plet (fold_pat alg.pat_alg pat, fold_exp alg e1, fold_exp alg e2)
   | E_internal_return e -> alg.e_internal_return (fold_exp alg e)
@@ -700,12 +681,7 @@ let id_exp_alg =
   ; e_throw = (fun e1 -> E_throw (e1))
   ; e_return = (fun e1 -> E_return e1)
   ; e_assert = (fun (e1,e2) -> E_assert(e1,e2)) 
-  ; e_internal_cast = (fun (a,e1) -> E_internal_cast (a,e1))
-  ; e_internal_exp = (fun a -> E_internal_exp a)
-  ; e_internal_exp_user = (fun (a1,a2) -> E_internal_exp_user (a1,a2))
-  ; e_comment = (fun c -> E_comment c)
-  ; e_comment_struc = (fun e -> E_comment_struc e)
-  ; e_internal_let = (fun (lexp, e2, e3) -> E_var (lexp,e2,e3))
+  ; e_var = (fun (lexp, e2, e3) -> E_var (lexp,e2,e3))
   ; e_internal_plet = (fun (pat, e1, e2) -> E_internal_plet (pat,e1,e2))
   ; e_internal_return = (fun e -> E_internal_return e)
   ; e_internal_value = (fun v -> E_internal_value v)
@@ -804,12 +780,7 @@ let compute_exp_alg bot join =
   ; e_throw = (fun (v1,e1) -> (v1, E_throw (e1)))
   ; e_return = (fun (v1,e1) -> (v1, E_return e1))
   ; e_assert = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_assert(e1,e2)) )
-  ; e_internal_cast = (fun (a,(v1,e1)) -> (v1, E_internal_cast (a,e1)))
-  ; e_internal_exp = (fun a -> (bot, E_internal_exp a))
-  ; e_internal_exp_user = (fun (a1,a2) -> (bot, E_internal_exp_user (a1,a2)))
-  ; e_comment = (fun c -> (bot, E_comment c))
-  ; e_comment_struc = (fun (v,e) -> (bot, E_comment_struc e)) (* ignore value by default, since it is comes from a comment *)
-  ; e_internal_let = (fun ((vl, lexp), (v2,e2), (v3,e3)) ->
+  ; e_var = (fun ((vl, lexp), (v2,e2), (v3,e3)) ->
     (join_list [vl;v2;v3], E_var (lexp,e2,e3)))
   ; e_internal_plet = (fun ((vp,pat), (v1,e1), (v2,e2)) ->
     (join_list [vp;v1;v2], E_internal_plet (pat,e1,e2)))
@@ -904,12 +875,7 @@ let pure_exp_alg bot join =
   ; e_throw = (fun v1 -> v1)
   ; e_return = (fun v1 -> v1)
   ; e_assert = (fun (v1,v2) -> join v1 v2)
-  ; e_internal_cast = (fun (a,v1) -> v1)
-  ; e_internal_exp = (fun a -> bot)
-  ; e_internal_exp_user = (fun (a1,a2) -> bot)
-  ; e_comment = (fun c -> bot)
-  ; e_comment_struc = (fun v -> bot)
-  ; e_internal_let = (fun (vl, v2, v3) -> join_list [vl;v2;v3])
+  ; e_var = (fun (vl, v2, v3) -> join_list [vl;v2;v3])
   ; e_internal_plet = (fun (vp, v1, v2) -> join_list [vp;v1;v2])
   ; e_internal_return = (fun v -> v)
   ; e_internal_value = (fun v -> bot)
diff --git a/src/rewriter.mli b/src/rewriter.mli
index edc93e5d..eed22376 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -139,12 +139,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; e_throw                  : 'exp -> 'exp_aux
  ; e_return                 : 'exp -> 'exp_aux
  ; e_assert                 : 'exp * 'exp -> 'exp_aux
- ; e_internal_cast          : 'a annot * 'exp -> 'exp_aux
- ; e_internal_exp           : 'a annot -> 'exp_aux
- ; e_internal_exp_user      : 'a annot * 'a annot -> 'exp_aux
- ; e_comment                : string -> 'exp_aux
- ; e_comment_struc          : 'exp -> 'exp_aux
- ; e_internal_let           : 'lexp * 'exp * 'exp -> 'exp_aux
+ ; e_var                    : 'lexp * 'exp * 'exp -> 'exp_aux
  ; e_internal_plet          : 'pat * 'exp * 'exp -> 'exp_aux
  ; e_internal_return        : 'exp -> 'exp_aux
  ; e_internal_value         : Value.value -> 'exp_aux
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 2faebf9c..c7e53e88 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -483,12 +483,7 @@ let rewrite_sizeof (Defs defs) =
     ; e_throw = (fun (e1,e1') -> (E_throw (e1), E_throw (e1')))
     ; e_return = (fun (e1,e1') -> (E_return e1, E_return e1'))
     ; e_assert = (fun ((e1,e1'),(e2,e2')) -> (E_assert(e1,e2), E_assert(e1',e2')) )
-    ; e_internal_cast = (fun (a,(e1,e1')) -> (E_internal_cast (a,e1), E_internal_cast (a,e1')))
-    ; e_internal_exp = (fun a -> (E_internal_exp a, E_internal_exp a))
-    ; e_internal_exp_user = (fun (a1,a2) -> (E_internal_exp_user (a1,a2), E_internal_exp_user (a1,a2)))
-    ; e_comment = (fun c -> (E_comment c, E_comment c))
-    ; e_comment_struc = (fun (e,e') -> (E_comment_struc e, E_comment_struc e'))
-    ; e_internal_let = (fun ((lexp,lexp'), (e2,e2'), (e3,e3')) -> (E_var (lexp,e2,e3), E_var (lexp',e2',e3')))
+    ; e_var = (fun ((lexp,lexp'), (e2,e2'), (e3,e3')) -> (E_var (lexp,e2,e3), E_var (lexp',e2',e3')))
     ; e_internal_plet = (fun (pat, (e1,e1'), (e2,e2')) -> (E_internal_plet (pat,e1,e2), E_internal_plet (pat,e1',e2')))
     ; e_internal_return = (fun (e,e') -> (E_internal_return e, E_internal_return e'))
     ; e_internal_value = (fun v -> (E_internal_value v, E_internal_value v))
@@ -1908,7 +1903,7 @@ let rewrite_defs_early_return (Defs defs) =
     if is_return exp then E_return (E_aux (E_let (lb, ret_exp), annot))
     else E_let (lb, exp) in
 
-  let e_internal_let (lexp, exp1, exp2) =
+  let e_var (lexp, exp1, exp2) =
     let (E_aux (_, annot) as ret_exp2) = get_return exp2 in
     if is_return exp2 then
       E_return (E_aux (E_var (lexp, exp1, ret_exp2), annot))
@@ -1968,7 +1963,7 @@ let rewrite_defs_early_return (Defs defs) =
         let exp' =
           fold_exp
             { id_exp_alg with e_block = e_block; e_if = e_if; e_case = e_case;
-              e_let = e_let; e_internal_let = e_internal_let; e_app = e_app }
+              e_let = e_let; e_var = e_var; e_app = e_app }
             (add_final_return false exp) in
         (* Remove early return if we can pull it out completely, and rewrite
            remaining early returns to "early_return" calls *)
@@ -2785,8 +2780,6 @@ let rewrite_defs_letbind_effects =
        k (rewrap (E_sizeof nexp))
     | E_constraint nc ->
        k (rewrap (E_constraint nc))
-    | E_sizeof_internal annot ->
-       k (rewrap (E_sizeof_internal annot))
     | E_assign (lexp,exp1) ->
        n_lexp lexp (fun lexp ->
        n_exp_name exp1 (fun exp1 ->
@@ -2796,11 +2789,6 @@ let rewrite_defs_letbind_effects =
        n_exp_name exp1 (fun exp1 ->
        n_exp_name exp2 (fun exp2 ->
        k (rewrap (E_assert (exp1,exp2)))))
-    | E_internal_cast (annot',exp') ->
-       n_exp_name exp' (fun exp' ->
-       k (rewrap (E_internal_cast (annot',exp'))))
-    | E_internal_exp _ -> k exp
-    | E_internal_exp_user _ -> k exp
     | E_var (lexp,exp1,exp2) ->
        n_lexp lexp (fun lexp ->
        n_exp exp1 (fun exp1 ->
@@ -2810,11 +2798,6 @@ let rewrite_defs_letbind_effects =
        k (rewrap (E_internal_return exp1)))
     | E_internal_value v ->
        k (rewrap (E_internal_value v))
-    | E_comment str ->
-       k (rewrap (E_comment str))
-    | E_comment_struc exp' ->
-       n_exp exp' (fun exp' ->
-       k (rewrap (E_comment_struc exp')))
     | E_return exp' ->
        n_exp_name exp' (fun exp' ->
        k (rewrap (E_return exp')))
@@ -2886,7 +2869,7 @@ let rewrite_defs_internal_lets =
        then E_internal_plet (pat,exp',body)
        else E_let (lb,body) in
 
-  let e_internal_let = fun (lexp,exp1,exp2) ->
+  let e_var = fun (lexp,exp1,exp2) ->
     let paux, annot = match lexp with
     | LEXP_aux (LEXP_id id, annot) ->
        (P_id id, annot)
@@ -2898,7 +2881,7 @@ let rewrite_defs_internal_lets =
     else
       E_let (LB_aux (LB_val (P_aux (paux, annot), exp1), annot), exp2) in
 
-  let alg = { id_exp_alg with e_let = e_let; e_internal_let = e_internal_let } in
+  let alg = { id_exp_alg with e_let = e_let; e_var = e_var } in
   rewrite_defs_base
     { rewrite_exp = (fun _ exp -> fold_exp alg (propagate_exp_effect exp))
     ; rewrite_pat = rewrite_pat
diff --git a/src/sail.ml b/src/sail.ml
index 8cc60e2c..e698090e 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -59,7 +59,6 @@ let opt_interactive_script : string option ref = ref None
 let opt_print_version = ref false
 let opt_print_initial_env = ref false
 let opt_print_verbose = ref false
-let opt_print_lem_ast = ref false
 let opt_print_lem = ref false
 let opt_print_ocaml = ref false
 let opt_print_c = ref false
@@ -123,9 +122,6 @@ let options = Arg.align ([
   ( "-trace",
     Arg.Tuple [Arg.Set C_backend.opt_trace; Arg.Set Ocaml_backend.opt_trace_ocaml],
     " Instrument ouput with tracing");
-  ( "-lem_ast",
-    Arg.Set opt_print_lem_ast,
-    " output a Lem AST representation of the input");
   ( "-lem",
     Arg.Set opt_print_lem,
     " output a Lem translated version of the input");
@@ -301,9 +297,6 @@ let main() =
       (if !(opt_print_verbose)
        then ((Pretty_print_sail.pp_defs stdout) ast)
        else ());
-      (if !(opt_print_lem_ast)
-       then output "" Lem_ast_out [out_name,ast]
-       else ());
       (if !(opt_print_ocaml)
        then
          let ast_ocaml = rewrite_ast_ocaml ast in
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 04668989..9481d6b1 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -470,7 +470,6 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function
      List.fold_left Nameset.union Nameset.empty (List.map snd fvs)
   | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef
   | DEF_reg_dec rdec -> fv_of_rd consider_var rdec
-  | DEF_comm _ -> mt,mt
 
 let group_defs consider_scatter_as_one (Ast.Defs defs) =
   List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs
diff --git a/src/type_check.ml b/src/type_check.ml
index c73c7000..dbd01c56 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2538,7 +2538,7 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
   begin
     try
       typ_debug (lazy ("PERFORMING TYPE COERCION: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ));
-      subtyp l env (typ_of annotated_exp) typ; annotated_exp (* ; switch_typ annotated_exp typ *)
+      subtyp l env (typ_of annotated_exp) typ; annotated_exp
     with
     | Type_error (_, trigger) when Env.allow_casts env ->
        let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in
@@ -4454,10 +4454,6 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
   | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err ()
   | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err ()
   | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker")
-  | DEF_comm (DC_comm str) -> [DEF_comm (DC_comm str)], env
-  | DEF_comm (DC_comm_struct def) ->
-     let defs, env = check_def env def
-     in List.map (fun def -> DEF_comm (DC_comm_struct def)) defs, env
 
 and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
   fun env (Defs defs) ->