Removed legacy parser/lexer and pretty printer

1 files changed, 0 insertions, 536 deletions

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
deleted file mode 100644
index 38b9e134..00000000
--- a/src/pretty_print_sail.ml
+++ /dev/null
@@ -1,536 +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 Ast
-open Ast_util
-open PPrint
-open Pretty_print_common
-
-(****************************************************************************
- * PPrint-based source-to-source pretty printer
-****************************************************************************)
-
-let doc_bkind (BK_aux(k,_)) =
-  string (match k with
-  | BK_type -> "Type"
-  | BK_nat -> "Nat"
-  | BK_order -> "Order")
-
-let doc_kind (K_aux(K_kind(klst),_)) =
-  separate_map (spaces arrow) doc_bkind klst
-
-let doc_qi (QI_aux(qi,_)) = match qi with
-  | QI_const n_const -> doc_nexp_constraint n_const
-  | QI_id(KOpt_aux(ki,_)) ->
-    match ki with
-    | KOpt_none v -> doc_var v
-    | KOpt_kind(k,v) -> separate space [doc_kind k; doc_var v]
-
-(* typ_doc is the doc for the type being quantified *)
-let doc_typquant (TypQ_aux(tq,_)) typ_doc = match tq with
-  | TypQ_no_forall -> typ_doc
-  | TypQ_tq [] -> typ_doc
-  | TypQ_tq qlist ->
-    (* include trailing break because the caller doesn't know if tq is empty *)
-    doc_op dot
-      (separate space [string "forall"; separate_map comma_sp doc_qi qlist])
-      typ_doc
-
-let doc_typscm (TypSchm_aux(TypSchm_ts(tq,t),_)) =
-  (doc_typquant tq (doc_typ t))
-
-let doc_typscm_atomic (TypSchm_aux(TypSchm_ts(tq,t),_)) =
-  (doc_typquant tq (doc_atomic_typ t))
-
-let doc_lit (L_aux(l,_)) =
-  utf8string (match l with
-  | L_unit  -> "()"
-  | L_zero  -> "bitzero"
-  | L_one   -> "bitone"
-  | L_true  -> "true"
-  | L_false -> "false"
-  | L_num i -> Big_int.to_string i
-  | L_hex n -> "0x" ^ n
-  | L_bin n -> "0b" ^ n
-  | L_real r -> r
-  | L_undef -> "undefined"
-  | L_string s -> "\"" ^ String.escaped s ^ "\"")
-
-let doc_pat, doc_atomic_pat =
-  let rec pat pa = pat_colons pa
-  and pat_colons ((P_aux(p,l)) as pa) = match p with
-  (* XXX add leading indentation if not flat - we need to define our own
-   * combinator for that *)
-  | P_vector_concat pats  -> separate_map (space ^^ colon ^^ break 1) atomic_pat pats
-  | _ -> app_pat pa
-  and app_pat ((P_aux(p,l)) as pa) = match p with
-  | P_app(id, ((_ :: _) as pats)) -> doc_unop (doc_id id) (parens (separate_map comma_sp atomic_pat pats))
-  | _ -> atomic_pat pa
-  and atomic_pat ((P_aux(p,(l,annot))) as pa) = match p with
-  | P_lit lit  -> doc_lit lit
-  | P_wild -> underscore
-  | P_id id -> doc_id id
-  | P_var (P_aux (P_id id, _), kid) when Id.compare (id_of_kid kid) id == 0 ->
-     doc_var kid
-  | P_var(p,kid) -> parens (separate space [pat p; string "as"; doc_var kid])
-  | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id id])
-  | P_typ(typ,p) -> separate space [parens (doc_typ typ); atomic_pat p]
-  | P_app(id,[]) -> doc_id id
-  | P_record(fpats,_) -> braces (separate_map semi_sp fpat fpats)
-  | P_vector pats  -> brackets (separate_map comma_sp atomic_pat pats)
-  | P_tup pats  -> parens (separate_map comma_sp atomic_pat pats)
-  | P_list pats  -> squarebarbars (separate_map semi_sp atomic_pat pats)
-  | P_cons (pat1, pat2) -> separate space [atomic_pat pat1; coloncolon; pat pat2]
-  | P_app(_, _ :: _) | P_vector_concat _ ->
-      group (parens (pat pa))
-  and fpat (FP_aux(FP_Fpat(id,fpat),_)) = doc_op equals (doc_id id) (pat fpat)
-  and npat (i,p) = doc_op equals (doc_int i) (pat p)
-
-  (* expose doc_pat and doc_atomic_pat *)
-  in pat, atomic_pat
-
-let doc_exp, doc_let =
-  let rec exp e = group (or_exp e)
-  and or_exp ((E_aux(e,_)) as expr) = match e with
-  | E_app_infix(l,(Id_aux(Id ("|" | "||"),_) as op),r) ->
-      doc_op (doc_id op) (and_exp l) (or_exp r)
-  | _ -> and_exp expr
-  and and_exp ((E_aux(e,_)) as expr) = match e with
-  | E_app_infix(l,(Id_aux(Id ("&" | "&&"),_) as op),r) ->
-      doc_op (doc_id op) (eq_exp l) (and_exp r)
-  | _ -> eq_exp expr
-  and eq_exp ((E_aux(e,_)) as expr) = match e with
-  | E_app_infix(l,(Id_aux(Id (
-    (* XXX this is not very consistent - is the parser bogus here? *)
-      "=" | "==" | "!="
-    | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u"
-    | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u"
-    ),_) as op),r) ->
-      doc_op (doc_id op) (eq_exp l) (at_exp r)
-  (* XXX assignment should not have the same precedence as equal etc. *)
-  | E_assign(le,exp) -> doc_op coloneq (doc_lexp le) (at_exp exp)
-  | _ -> at_exp expr
-  and at_exp ((E_aux(e,_)) as expr) = match e with
-  | E_app_infix(l,(Id_aux(Id ("@" | "^^" | "^" | "~^"),_) as op),r) ->
-      doc_op (doc_id op) (cons_exp l) (at_exp r)
-  | _ -> cons_exp expr
-  and cons_exp ((E_aux(e,_)) as expr) = match e with
-  | E_vector_append(l,r) ->
-      doc_op colon (shift_exp l) (cons_exp r)
-  | E_cons(l,r) ->
-      doc_op coloncolon (shift_exp l) (cons_exp r)
-  | _ -> shift_exp expr
-  and shift_exp ((E_aux(e,_)) as expr) = match e with
-  | E_app_infix(l,(Id_aux(Id (">>" | ">>>" | "<<" | "<<<"),_) as op),r) ->
-      doc_op (doc_id op) (shift_exp l) (plus_exp r)
-  | _ -> plus_exp expr
-  and plus_exp ((E_aux(e,_)) as expr) = match e with
-  | E_app_infix(l,(Id_aux(Id ("+" | "-" | "+_s" | "-_s"),_) as op),r) ->
-      doc_op (doc_id op) (plus_exp l) (star_exp r)
-  | _ -> star_exp expr
-  and star_exp ((E_aux(e,_)) as expr) = match e with
-  | E_app_infix(l,(Id_aux(Id (
-      "*" | "/"
-    | "div" | "quot" | "quot_s" | "rem" | "mod"
-    | "*_s" | "*_si" | "*_u" | "*_ui"),_) as op),r) ->
-      doc_op (doc_id op) (star_exp l) (starstar_exp r)
-  | _ -> starstar_exp expr
-  and starstar_exp ((E_aux(e,_)) as expr) = match e with
-  | E_app_infix(l,(Id_aux(Id "**",_) as op),r) ->
-      doc_op (doc_id op) (starstar_exp l) (app_exp r)
-  | E_if _ | E_for _ | E_loop _ | E_let _
-  | E_var _ | E_internal_plet _ -> right_atomic_exp expr
-  | _ -> app_exp expr
-  and right_atomic_exp ((E_aux(e,_)) as expr) = match e with
-  (* Special case: omit "else ()" when the else branch is empty. *)
-  | E_if(c,t,E_aux(E_block [], _)) ->
-      string "if" ^^ space ^^ group (exp c) ^/^
-      string "then" ^^ space ^^ group (exp t)
-  | E_if(c,t,e) ->
-      string "if" ^^ space ^^ group (exp c) ^/^
-      string "then" ^^ space ^^ group (exp t) ^/^
-        string "else" ^^ space ^^ group (exp e)
-  | E_loop (While, c, e) ->
-     separate space [string "while"; atomic_exp c; string "do"] ^/^
-       exp e
-  | E_loop (Until, c, e) ->
-     (string "repeat"
-      ^/^ exp e)
-     ^/^ (string "until" ^^ space ^^ atomic_exp c)
-  | E_for(id,exp1,exp2,exp3,order,exp4) ->
-      string "foreach" ^^ space ^^
-      group (parens (
-        separate (break 1) [
-          doc_id id;
-          string "from " ^^ atomic_exp exp1;
-          string "to " ^^ atomic_exp exp2;
-          string "by " ^^ atomic_exp exp3;
-          string "in " ^^ doc_ord order
-        ]
-      )) ^/^
-      exp exp4
-  | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e)
-  | E_var (lexp, exp1, exp2) ->
-     let le =
-       prefix 2 1
-         (separate space [string "internal_let"; doc_lexp lexp; equals])
-         (exp exp1) in
-     doc_op (string "in") le (exp exp2)
-  | E_internal_plet (pat, exp1, exp2) ->
-     let le =
-       prefix 2 1
-         (separate space [string "internal_plet"; doc_pat pat; equals])
-         (exp exp1) in
-     doc_op (string "in") le (exp exp2)
-  | _ -> group (parens (exp expr))
-  and app_exp ((E_aux(e,_)) as expr) = match e with
-  | E_app(f,args) ->
-      (doc_id f) ^^ (parens (separate_map comma exp args))
-  | _ -> vaccess_exp expr
-  and vaccess_exp ((E_aux(e,_)) as expr) = match e with
-  | E_vector_access(v,e) ->
-      atomic_exp v ^^ brackets (exp e)
-  | E_vector_subrange(v,e1,e2) ->
-      atomic_exp v ^^ brackets (doc_op dotdot (exp e1) (exp e2))
-  | _ -> field_exp expr
-  and field_exp ((E_aux(e,_)) as expr) = match e with
-  | E_field(fexp,id) -> atomic_exp fexp ^^ dot ^^ doc_id id
-  | _ -> atomic_exp expr
-  and atomic_exp ((E_aux(e,_)) as expr) = match e with
-  (* Special case: an empty block is equivalent to unit, but { } would
-   * be parsed as a struct. *)
-  | E_block [] -> string "()"
-  | E_block exps ->
-      let exps_doc = separate_map (semi ^^ hardline) exp exps in
-      surround 2 1 lbrace exps_doc rbrace
-  | E_nondet exps ->
-    let exps_doc = separate_map (semi ^^ hardline) exp exps in
-    string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace)
-  | E_comment s -> string ("(*" ^ s ^ "*) ()")
-  | E_comment_struc e -> string "(*" ^^ exp e ^^ string "*) ()"
-  | E_id id -> doc_id id
-  | E_lit lit -> doc_lit lit
-  | E_cast(typ,e) -> prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp e))
-                            (*
-  | E_internal_cast((_,NoTyp),e) -> atomic_exp e
-  | E_internal_cast((_,Base((_,t),_,_,_,_,bindings)), (E_aux(_,(_,eannot)) as e)) ->
-      (match t.t,eannot with
-      (* XXX I don't understand why we can hide the internal cast here
-         AAA Because an internal cast between vectors is only generated to reset the base access;
-             the type checker generates far more than are needed and they're pruned off here, after constraint resolution *)
-      | Tapp("vector",[TA_nexp n1;_;_;_]),Base((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_,_,_)
-          when nexp_eq n1 n2 -> atomic_exp e
-      | _ -> prefix 2 1 (parens (doc_typ (t_to_typ t))) (group (atomic_exp e)))
-                             *)
-  | E_tuple exps ->
-      parens (separate_map comma exp exps)
-  | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
-      (* XXX E_record is not handled by parser currently
-         AAA The parser can't handle E_record due to ambiguity with blocks; initial_check looks for blocks that are all field assignments and converts *)
-      braces (separate_map semi_sp doc_fexp fexps)
-  | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
-      braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps))
-  | E_vector exps ->
-    let default_print _ = brackets (separate_map comma exp exps) in
-    (match exps with
-      | [] -> default_print ()
-      | E_aux(e,_)::es ->
-        (match e with
-          | E_lit (L_aux(L_one, _)) | E_lit (L_aux(L_zero, _)) ->
-            utf8string
-              ("0b" ^
-                  (List.fold_right (fun (E_aux( e,_)) rst ->
-                    (match e with
-                      | E_lit(L_aux(l, _)) ->
-                        ((match l with | L_one -> "1" | L_zero -> "0" | L_undef -> "u" | _ -> assert false) ^ rst)
-                      | _ -> assert false)) exps ""))
-          | _ -> default_print ()))
-  | E_vector_update(v,e1,e2) ->
-      brackets (doc_op (string "with") (exp v) (doc_op equals (atomic_exp e1) (exp e2)))
-  | E_vector_update_subrange(v,e1,e2,e3) ->
-      brackets (
-        doc_op (string "with") (exp v)
-        (doc_op equals (atomic_exp e1 ^^ colon ^^ atomic_exp e2) (exp e3)))
-  | E_list exps ->
-      squarebarbars (separate_map comma exp exps)
-  | E_try(e,pexps) ->
-      let opening = separate space [string "try"; exp e; string "catch"; lbrace] in
-      let cases = separate_map (break 1) doc_case pexps in
-      surround 2 1 opening cases rbrace
-  | E_case(e,pexps) ->
-      let opening = separate space [string "switch"; exp e; lbrace] in
-      let cases = separate_map (break 1) doc_case pexps in
-      surround 2 1 opening cases rbrace
-  | E_sizeof n ->
-     parens (separate space [string "sizeof"; doc_nexp n])
-  | E_constraint nc ->
-     string "constraint" ^^ parens (doc_nexp_constraint nc)
-  | E_exit e ->
-    separate space [string "exit"; atomic_exp e;]
-  | E_throw e ->
-    separate space [string "throw"; atomic_exp e;]
-  | E_return e ->
-    separate space [string "return"; atomic_exp e;]
-  | E_assert(c,m) ->
-    separate space [string "assert"; parens (separate comma [exp c; exp m])]
-  (* adding parens and loop for lower precedence *)
-  | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _)
-  | E_cons (_, _)|E_field (_, _)|E_assign (_, _)
-  | E_if _ | E_for _ | E_loop _ | E_let _
-  | E_var _ | E_internal_plet _
-  | E_vector_append _
-  | E_app_infix (_,
-    (* for every app_infix operator caught at a higher precedence,
-     * we need to wrap around with parens *)
-    (Id_aux(Id("|" | "||"
-    | "&" | "&&"
-    | "=" | "==" | "!="
-    | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u"
-    | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u"
-    | "@" | "^^" | "^" | "~^"
-    | ">>" | ">>>" | "<<" | "<<<"
-    | "+" | "-" | "+_s" | "-_s"
-    | "*" | "/"
-    | "div" | "quot" | "quot_s" | "rem" | "mod"
-    | "*_s" | "*_si" | "*_u" | "*_ui"
-    | "**"), _))
-    , _) ->
-      group (parens (exp expr))
-  (* XXX default precedence for app_infix? *)
-  | E_app_infix(l,op,r) ->
-      failwith ("unexpected app_infix operator " ^ (pp_format_id op))
-  (* doc_op (doc_id op) (exp l) (exp r) *)
-  | E_internal_return exp1 ->
-      separate space [string "internal_return"; exp exp1]
-  | _ -> failwith ("Cannot print: " ^ Ast_util.string_of_exp expr)
-  and let_exp (LB_aux(lb,_)) = match lb with
-  | LB_val(pat,e) ->
-      prefix 2 1
-        (separate space [string "let"; doc_atomic_pat pat; equals])
-        (atomic_exp e)
-
-  and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id id) (exp e)
-
-  and doc_case (Pat_aux (pexp, _)) =
-    match pexp with
-    | Pat_exp(pat, e) ->
-       doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp e))
-    | Pat_when(pat, guard, e) ->
-       doc_op arrow (separate space [string "case"; doc_atomic_pat pat; string "when"; exp guard]) (group (exp e))
-
-  (* lexps are parsed as eq_exp - we need to duplicate the precedence
-   * structure for them *)
-  and doc_lexp le = app_lexp le
-  and app_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with
-  | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma exp args)
-  | _ -> vaccess_lexp le
-  and vaccess_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with
-  | LEXP_vector(v,e) -> atomic_lexp v ^^ brackets (exp e)
-  | LEXP_vector_range(v,e1,e2) ->
-      atomic_lexp v ^^ brackets (exp e1 ^^ dotdot ^^ exp e2)
-  | _ -> field_lexp le
-  and field_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with
-  | LEXP_field(v,id) -> atomic_lexp v ^^ dot ^^ doc_id id
-  | _ -> atomic_lexp le
-  and atomic_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with
-  | LEXP_id id -> doc_id id
-  | LEXP_cast(typ,id) -> prefix 2 1 (parens (doc_typ typ)) (doc_id id)
-  | LEXP_memory _ | LEXP_vector _ | LEXP_vector_range _
-  | LEXP_field _ -> group (parens (doc_lexp le))
-  | LEXP_tup tups -> parens (separate_map comma doc_lexp tups)
-
-  (* expose doc_exp and doc_let *)
-  in exp, let_exp
-
-let doc_default (DT_aux(df,_)) = match df with
-  | DT_kind(bk,v) -> separate space [string "default"; doc_bkind bk; doc_var v]
-  | DT_typ(ts,id) -> separate space [string "default"; doc_typscm ts; doc_id id]
-  | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord]
-
-let doc_spec (VS_aux (VS_val_spec (ts, id, ext_opt, is_cast), _)) =
-  let cast_pp = if is_cast then [string "cast"] else [] in
-  (* This sail syntax only supports a single extern name, so just use the ocaml version *)
-  let extern_kwd_pp, id_pp = match ext_opt "ocaml" with
-    | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string (ext)))
-    | None -> [], doc_id id
-  in
-  separate space ([string "val"] @ cast_pp @ extern_kwd_pp @ [doc_typscm ts] @ [id_pp])
-
-let doc_namescm (Name_sect_aux(ns,_)) = match ns with
-  | Name_sect_none -> empty
-  (* include leading space because the caller doesn't know if ns is
-   * empty, and trailing break already added by the following equals *)
-  | Name_sect_some s -> space ^^ brackets (doc_op equals (string "name") (dquotes (string s)))
-
-let doc_type_union (Tu_aux(typ_u,_)) = match typ_u with
-  | Tu_ty_id(typ,id) -> separate space [doc_typ typ; doc_id id]
-  | Tu_id id -> doc_id id
-
-let doc_typdef (TD_aux(td,_)) = match td with
-  | TD_abbrev(id,nm,typschm) ->
-      doc_op equals (concat [string "typedef"; space; doc_id id; doc_namescm nm]) (doc_typscm typschm)
-  | TD_record(id,nm,typq,fs,_) ->
-      let f_pp (typ,id) = concat [doc_typ typ; space; doc_id id; semi] in
-      let fs_doc = group (separate_map (break 1) f_pp fs) in
-      doc_op equals
-        (concat [string "typedef"; space; doc_id id; doc_namescm nm])
-        (string "const struct" ^^ space ^^ doc_typquant typq (braces fs_doc))
-  | TD_variant(id,nm,typq,ar,_) ->
-      let ar_doc = group (separate_map (semi ^^ break 1) doc_type_union ar) in
-      doc_op equals
-        (concat [string "typedef"; space; doc_id id; doc_namescm nm])
-        (string "const union" ^^ space ^^ doc_typquant typq (braces ar_doc))
-  | TD_enum(id,nm,enums,_) ->
-      let enums_doc = group (separate_map (semi ^^ break 1) doc_id enums) in
-      doc_op equals
-        (concat [string "typedef"; space; doc_id id; doc_namescm nm])
-        (string "enumerate" ^^ space ^^ braces enums_doc)
-
-let doc_kindef (KD_aux(kd,_)) = match kd with
-  | KD_nabbrev(kind,id,nm,n) ->
-    doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (doc_nexp n)
-
-let doc_rec (Rec_aux(r,_)) = match r with
-  | Rec_nonrec -> empty
-  (* include trailing space because caller doesn't know if we return
-   * empty *)
-  | Rec_rec -> space ^^ string "rec"
-
-let doc_tannot_opt (Typ_annot_opt_aux(t,_)) = match t with
-  | Typ_annot_opt_some(tq,typ) -> space ^^ doc_typquant tq (doc_typ typ)
-  | Typ_annot_opt_none -> empty
-
-let doc_effects_opt (Effect_opt_aux(e,_)) = match e with
-  | Effect_opt_pure -> string "pure"
-  | Effect_opt_effect e -> doc_effects e
-
-let doc_funcl (FCL_aux(FCL_Funcl(id,pexp),_)) =
-  match pexp with
-  | Pat_aux (Pat_exp (pat,exp),_) ->
-     group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp exp))
-  | Pat_aux (Pat_when (pat,wh,exp),_) ->
-     group (doc_op equals (doc_id id ^^ space ^^ parens (separate space [doc_atomic_pat pat; string "when"; doc_exp wh]))
-              (doc_exp exp))
-
-let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) =
-  match fcls with
-  | [] -> failwith "FD_function with empty function list"
-  | _ ->
-      let sep = hardline ^^ string "and" ^^ space in
-      let clauses = separate_map sep doc_funcl fcls in
-      separate space ([string "function" ^^ doc_rec r ^^ doc_tannot_opt typa]@
-                      (match efa with
-                       | Effect_opt_aux (Effect_opt_pure,_) -> []
-                       | _ -> [string "effect";
-                               doc_effects_opt efa;])
-                      @[clauses])
-
-let doc_alias (AL_aux (alspec,_)) =
-  match alspec with
-    | AL_subreg((RI_aux (RI_id id,_)),subid) -> doc_id id ^^ dot ^^ doc_id subid
-    | AL_bit((RI_aux (RI_id id,_)),ac) -> doc_id id ^^ brackets (doc_exp ac)
-    | AL_slice((RI_aux (RI_id id,_)),b,e) -> doc_id id ^^ brackets (doc_op dotdot (doc_exp b) (doc_exp e))
-    | AL_concat((RI_aux (RI_id f,_)),(RI_aux (RI_id s,_))) -> doc_op colon (doc_id f) (doc_id s)
-
-let doc_dec (DEC_aux (reg,_)) =
-  match reg with
-    | DEC_reg(typ,id) -> separate space [string "register"; doc_typ typ; doc_id id]
-    | DEC_alias(id,alspec) ->
-        doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec)
-    | DEC_typ_alias(typ,id,alspec) ->
-        doc_op equals (string "register alias" ^^ space ^^ doc_typ typ) (doc_alias alspec)
-
-let doc_scattered (SD_aux (sdef, _)) = match sdef with
- | SD_scattered_function (r, typa, efa, id) ->
-     separate space ([
-       string "scattered function";
-       doc_rec r ^^ doc_tannot_opt typa;]@
-       (match efa with
-        | Effect_opt_aux (Effect_opt_pure,_) -> []
-        | _ -> [string "effect"; doc_effects_opt efa;])
-         @[doc_id id])
- | SD_scattered_variant (id, ns, tq) ->
-     doc_op equals
-       (string "scattered typedef" ^^ space ^^ doc_id id ^^ doc_namescm ns)
-       (string "const union" ^^ space ^^ (doc_typquant tq empty))
- | SD_scattered_funcl funcl ->
-     string "function clause" ^^ space ^^ doc_funcl funcl
- | SD_scattered_unioncl (id, tu) ->
-     separate space [string "union"; doc_id id;
-     string "member"; doc_type_union tu]
- | SD_scattered_end id -> string "end" ^^ space ^^ doc_id id
-
-let rec doc_def def = group (match def with
-  | DEF_default df -> doc_default df
-  | DEF_spec v_spec -> doc_spec v_spec
-  | DEF_type t_def -> doc_typdef t_def
-  | DEF_kind k_def -> doc_kindef k_def
-  | DEF_fundef f_def -> doc_fundef f_def
-  | DEF_val lbind -> doc_let lbind
-  | DEF_reg_dec dec -> doc_dec dec
-  | DEF_scattered sdef -> doc_scattered sdef
-  | DEF_overload (id, ids) ->
-      let ids_doc = group (separate_map (semi ^^ break 1) doc_id ids) in
-      string "overload" ^^ space ^^ doc_id id ^^ space ^^ brackets ids_doc
-  | DEF_comm (DC_comm s) -> comment (string s)
-  | DEF_comm (DC_comm_struct d) -> comment (doc_def d)
-  | DEF_fixity _ -> empty
-  | DEF_internal_mutrec _ -> failwith "Cannot print internal mutrec"
-  ) ^^ hardline
-
-let doc_defs (Defs(defs)) =
-  separate_map hardline doc_def defs
-
-let pp_defs f d = print f (doc_defs d)
-let pp_exp b e = to_buf b (doc_exp e)
-let pat_to_string p =
-  let b = Buffer.create 20 in
-  to_buf b (doc_pat p);
-  Buffer.contents b