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.

1 files changed, 0 insertions, 616 deletions

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