diff options
Diffstat (limited to 'src/pretty_print_sail.ml')
| -rw-r--r-- | src/pretty_print_sail.ml | 913 |
1 files changed, 442 insertions, 471 deletions
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 3868502b..930da39c 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -50,45 +50,146 @@ open Ast open Ast_util -open Big_int 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)) + +module Big_int = Nat_big_num + +let doc_op symb a b = infix 2 1 symb a b + +let doc_id (Id_aux (id_aux, _)) = + string (match id_aux with + | Id v -> v + | DeIid op -> "operator " ^ op) + +let doc_kid kid = string (Ast_util.string_of_kid kid) + +let doc_int n = string (Big_int.to_string n) + +let doc_ord (Ord_aux(o,_)) = match o with + | Ord_var v -> doc_kid v + | Ord_inc -> string "inc" + | Ord_dec -> string "dec" + +let rec doc_nexp = + let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_constant c -> string (Big_int.to_string c) + | Nexp_id id -> doc_id id + | Nexp_var kid -> doc_kid kid + | _ -> parens (nexp0 nexp) + and nexp0 (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_sum (n1, Nexp_aux (Nexp_neg n2, _)) | Nexp_minus (n1, n2) -> + separate space [nexp0 n1; string "-"; nexp1 n2] + | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when Big_int.less c Big_int.zero -> + separate space [nexp0 n1; string "-"; doc_int (Big_int.abs c)] + | Nexp_sum (n1, n2) -> separate space [nexp0 n1; string "+"; nexp1 n2] + | _ -> nexp1 nexp + and nexp1 (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_times (n1, n2) -> separate space [nexp1 n1; string "*"; nexp2 n2] + | _ -> nexp2 nexp + and nexp2 (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_neg n -> separate space [string "-"; atomic_nexp n] + | Nexp_exp n -> separate space [string "2"; string "^"; atomic_nexp n] + | _ -> atomic_nexp nexp + in + nexp0 + +let doc_nc = + let nc_op op n1 n2 = separate space [doc_nexp n1; string op; doc_nexp n2] in + let rec atomic_nc (NC_aux (nc_aux, _) as nc) = + match nc_aux with + | NC_true -> string "true" + | NC_false -> string "false" + | NC_equal (n1, n2) -> nc_op "=" n1 n2 + | NC_not_equal (n1, n2) -> nc_op "!=" n1 n2 + | NC_bounded_ge (n1, n2) -> nc_op ">=" n1 n2 + | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2 + | NC_set (kid, ints) -> + separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)] + | _ -> parens (nc0 nc) + and nc0 (NC_aux (nc_aux, _) as nc) = + match nc_aux with + | NC_or (c1, c2) -> separate space [nc0 c1; string "|"; nc1 c2] + | _ -> nc1 nc + and nc1 (NC_aux (nc_aux, _) as nc) = + match nc_aux with + | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2] + | _ -> atomic_nc nc + in + nc0 + +let rec doc_typ (Typ_aux (typ_aux, _)) = + match typ_aux with + | Typ_id id -> doc_id id + | Typ_app (id, []) -> doc_id id + | Typ_app (Id_aux (DeIid str, _), [x; y]) -> + separate space [doc_typ_arg x; doc_typ_arg y] + (* + | Typ_app (id, [_; len; _; Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]) when Id.compare (mk_id "vector") id == 0 && Id.compare (mk_id "bit") tid == 0-> + string "bits" ^^ parens (doc_typ_arg len) + *) + | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs) + | Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs) + | Typ_var kid -> doc_kid kid + (* Resugar set types like {|1, 2, 3|} *) + | Typ_exist ([kid1], NC_aux (NC_set (kid2, ints), _), Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _)) + when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 -> + enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints) + | Typ_exist (kids, nc, typ) -> + braces (separate_map space doc_kid kids ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ) + | Typ_fn (typ1, typ2, Effect_aux (Effect_set [], _)) -> + separate space [doc_typ typ1; string "->"; doc_typ typ2] + | Typ_fn (typ1, typ2, Effect_aux (Effect_set effs, _)) -> + let ocaml_eff = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) in + separate space [doc_typ typ1; string "->"; doc_typ typ2; string "effect"; ocaml_eff] +and doc_typ_arg (Typ_arg_aux (ta_aux, _)) = + match ta_aux with + | Typ_arg_typ typ -> doc_typ typ + | Typ_arg_nexp nexp -> doc_nexp nexp + | Typ_arg_order o -> doc_ord o + +let doc_quants quants = + let doc_qi_kopt (QI_aux (qi_aux, _)) = + match qi_aux with + | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid] + | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])] + | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])] + | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])] + | QI_const nc -> [] + in + let qi_nc (QI_aux (qi_aux, _)) = + match qi_aux with + | QI_const nc -> [nc] + | _ -> [] + in + let kdoc = separate space (List.concat (List.map doc_qi_kopt quants)) in + let ncs = List.concat (List.map qi_nc quants) in + match ncs with + | [] -> kdoc + | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc + | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) + + + +let doc_binding (TypQ_aux (tq_aux, _), typ) = + match tq_aux with + | TypQ_no_forall -> doc_typ typ + | TypQ_tq [] -> doc_typ typ + | TypQ_tq qs -> + string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ + +let doc_typschm (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding (typq, typ) + +let doc_typschm_typ (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = doc_typ typ + +let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = + match tq_aux with + | TypQ_no_forall -> None + | TypQ_tq [] -> None + | TypQ_tq qs -> Some (doc_quants qs) let doc_lit (L_aux(l,_)) = utf8string (match l with @@ -97,473 +198,343 @@ let doc_lit (L_aux(l,_)) = | L_one -> "bitone" | L_true -> "true" | L_false -> "false" - | L_num i -> string_of_big_int i + | 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 +let rec doc_pat (P_aux (p_aux, _) as pat) = + match p_aux with | P_id id -> doc_id id + | P_tup pats -> lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen + | P_typ (typ, pat) -> separate space [doc_pat pat; colon; doc_typ typ] + | P_lit lit -> doc_lit lit + (* P_var short form sugar *) | 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_internal_let _ | 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_internal_let (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) + doc_kid kid + | P_var (pat, kid) -> separate space [doc_pat pat; string "as"; doc_kid kid] + | P_vector pats -> brackets (separate_map (comma ^^ space) doc_pat pats) + | P_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_pat pats + | P_wild -> string "_" + | P_as (pat, id) -> separate space [doc_pat pat; string "as"; doc_id id] + | P_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_pat pats) + | _ -> string (string_of_pat pat) + +(* if_block_x is true if x should be printed like a block, i.e. with + newlines. Blocks are automatically printed as blocks, so this + returns false for them. *) +let if_block_then (E_aux (e_aux, _)) = + match e_aux with + | E_assign _ | E_if _ -> true + | _ -> false + +let if_block_else (E_aux (e_aux, _)) = + match e_aux with + | E_assign _ -> true + | _ -> false + +let fixities = + let fixities' = + List.fold_left + (fun r (x, y) -> Bindings.add x y r) + Bindings.empty + [ + (mk_id "^", (InfixR, 8)); + (mk_id "*", (InfixL, 7)); + (mk_id "+", (InfixL, 6)); + (mk_id "-", (InfixL, 6)); + (mk_id "!=", (Infix, 4)); + (mk_id ">", (Infix, 4)); + (mk_id "<", (Infix, 4)); + (mk_id ">=", (Infix, 4)); + (mk_id "<=", (Infix, 4)); + (mk_id "&", (InfixR, 3)); + (mk_id "|", (InfixR, 2)); + ] + in + ref (fixities' : (prec * int) Bindings.t) + +let rec doc_exp (E_aux (e_aux, _) as exp) = + match e_aux with + | E_block [] -> string "()" + | E_block [exp] -> doc_exp exp + | E_block exps -> surround 2 0 lbrace (doc_block exps) rbrace + | E_nondet exps -> assert false + (* This is mostly for the -convert option *) + | E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 -> + separate space [doc_atomic_exp x; string "/"; doc_atomic_exp y] + | E_app_infix _ -> doc_infix 0 exp + | E_tuple exps -> parens (separate_map (comma ^^ space) doc_exp exps) + + (* Various rules to try to format if blocks nicely based on content *) + | E_if (if_exp, then_exp, else_exp) when if_block_then then_exp && if_block_else else_exp -> + (separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) + ^/^ (string "else" ^//^ doc_exp else_exp) + | E_if (if_exp, then_exp, (E_aux (E_if _, _) as else_exp)) when if_block_then then_exp -> + (separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) + ^/^ (string "else" ^^ space ^^ doc_exp else_exp) + | E_if (if_exp, then_exp, else_exp) when if_block_else else_exp -> + (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp]) + ^^ space ^^ (string "else" ^//^ doc_exp else_exp) + | E_if (if_exp, then_exp, else_exp) when if_block_then then_exp -> + (separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) + ^/^ (string "else" ^^ space ^^ doc_exp else_exp) + | E_if (if_exp, then_exp, else_exp) -> + group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp]) + + | E_list exps -> string "[|" ^^ separate_map (comma ^^ space) doc_exp exps ^^ string "|]" + | E_cons (exp1, exp2) -> string "E_cons" + | E_record fexps -> separate space [string "record"; string "{"; doc_fexps fexps; string "}"] + | E_loop (While, cond, exp) -> + separate space [string "while"; doc_exp cond; string "do"; doc_exp exp] + | E_loop (Until, cond, exp) -> + separate space [string "repeat"; doc_exp exp; string "until"; doc_exp cond] + | E_record_update (exp, fexps) -> + separate space [string "{"; doc_exp exp; string "with"; doc_fexps fexps; string "}"] + | E_vector_append (exp1, exp2) -> separate space [doc_atomic_exp exp1; string "@"; doc_atomic_exp exp2] + | E_case (exp, pexps) -> + separate space [string "match"; doc_exp exp; doc_pexps pexps] + | E_let (LB_aux (LB_val (pat, binding), _), exp) -> + separate space [string "let"; doc_pat pat; equals; doc_exp binding; string "in"; doc_exp exp] | 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 + (doc_exp exp1) in + doc_op (string "in") le (doc_exp exp2) + | E_var (lexp, binding, exp) -> + separate space [string "var"; doc_lexp lexp; equals; doc_exp binding; string "in"; doc_exp exp] + | E_assign (lexp, exp) -> + separate space [doc_lexp lexp; equals; doc_exp exp] + | E_for (id, exp1, exp2, exp3, order, exp4) -> + begin + let header = + string "foreach" ^^ space ^^ + group (parens (separate (break 1) + [ doc_id id; + string "from " ^^ doc_atomic_exp exp1; + string "to " ^^ doc_atomic_exp exp2; + string "by " ^^ doc_atomic_exp exp3; + string "in " ^^ doc_ord order ])) + in + match exp4 with + | E_aux (E_block [_], _) -> header ^//^ doc_exp exp4 + | E_aux (E_block _, _) -> header ^^ space ^^ doc_exp exp4 + | _ -> header ^//^ doc_exp exp4 + end + (* Resugar an assert with an empty message *) + | E_throw exp -> string "throw" ^^ parens (doc_exp exp) + | E_try (exp, pexps) -> + separate space [string "try"; doc_exp exp; string "catch"; doc_pexps pexps] + | E_return exp -> string "return" ^^ parens (doc_exp exp) + | E_internal_return exp -> string "internal_return" ^^ parens (doc_exp exp) + | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 -> + separate space [string "2"; string "^"; doc_atomic_exp exp] + | _ -> doc_atomic_exp exp +and doc_infix n (E_aux (e_aux, _) as exp) = + match e_aux with + | E_app_infix (l, op, r) when n < 10 -> + begin + try + match Bindings.find op !fixities with + | (Infix, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r] + | (Infix, m) when m < n -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]) + | (InfixL, m) when m >= n -> separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r] + | (InfixL, m) when m < n -> parens (separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r]) + | (InfixR, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r] + | (InfixR, m) when m < n -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]) + | _ -> assert false + with + | Not_found -> + separate space [doc_atomic_exp l; doc_id op; doc_atomic_exp r] + end + | _ -> doc_atomic_exp exp +and doc_atomic_exp (E_aux (e_aux, _) as exp) = + match e_aux with + | E_cast (typ, exp) -> + separate space [doc_atomic_exp exp; colon; doc_typ typ] | 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_internal_let _ | 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_comment s -> comment (string s) - | E_comment_struc e -> comment (exp e) - (* - | E_internal_exp((l, Base((_,t),_,_,_,_,bindings))) -> (*TODO use bindings, and other params*) - (match t.t with - | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}]) - | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) -> - (match r.nexp with - | Nvar v -> utf8string v - | Nconst bi -> utf8string (Big_int.string_of_big_int bi) - | _ -> raise (Reporting_basic.err_unreachable l - ("Internal exp given vector without known length, instead given " ^ n_to_string r))) - | Tapp("implicit",[TA_nexp r]) -> - (match r.nexp with - | Nconst bi -> utf8string (Big_int.string_of_big_int bi) - | Nvar v -> utf8string v - | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given implicit without var or const")) - | _ -> raise (Reporting_basic.err_unreachable l ("Internal exp given non-vector, non-implicit " ^ t_to_string t))) - | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away")) - | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false - *) - | 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 + | E_id id -> doc_id id + | E_ref id -> string "ref" ^^ space ^^ doc_id id + | E_field (exp, id) -> doc_atomic_exp exp ^^ dot ^^ doc_id id + | E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid + | E_sizeof nexp -> string "sizeof" ^^ parens (doc_nexp nexp) + (* Format a function with a unit argument as f() rather than f(()) *) + | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> doc_id id ^^ string "()" + | E_app (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps) + | E_constraint nc -> string "constraint" ^^ parens (doc_nc nc) + | E_assert (exp1, E_aux (E_lit (L_aux (L_string "", _)), _)) -> string "assert" ^^ parens (doc_exp exp1) + | E_assert (exp1, exp2) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2) + | E_exit exp -> string "exit" ^^ parens (doc_exp exp) + | E_vector_access (exp1, exp2) -> doc_atomic_exp exp1 ^^ brackets (doc_exp exp2) + | E_vector_subrange (exp1, exp2, exp3) -> doc_atomic_exp exp1 ^^ brackets (separate space [doc_exp exp2; string ".."; doc_exp exp3]) + | E_vector exps -> brackets (separate_map (comma ^^ space) doc_exp exps) + | E_vector_update (exp1, exp2, exp3) -> + brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; equals; doc_exp exp3]) + | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> + brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4]) + | E_internal_value v -> string (Value.string_of_value v |> Util.green |> Util.clear) + | _ -> parens (doc_exp exp) +and doc_fexps (FES_aux (FES_Fexps (fexps, _), _)) = + separate_map (comma ^^ space) doc_fexp fexps +and doc_fexp (FE_aux (FE_Fexp (id, exp), _)) = + separate space [doc_id id; equals; doc_exp exp] +and doc_block = function + | [] -> string "()" + | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] -> + separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps + | [E_aux (E_var (lexp, binding, E_aux (E_block exps, _)), _)] -> + separate space [string "var"; doc_lexp lexp; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps + | [exp] -> doc_exp exp + | exp :: exps -> doc_exp exp ^^ semi ^^ hardline ^^ doc_block exps +and doc_lexp (LEXP_aux (l_aux, _) as lexp) = + match l_aux with + | LEXP_cast (typ, id) -> separate space [doc_id id; colon; doc_typ typ] + | _ -> doc_atomic_lexp lexp +and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) = + match l_aux 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 + | LEXP_deref exp -> lparen ^^ string "*" ^^ doc_atomic_exp exp ^^ rparen + | LEXP_tup lexps -> lparen ^^ separate_map (comma ^^ space) doc_lexp lexps ^^ rparen + | LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id + | LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp) + | LEXP_vector_range (lexp, exp1, exp2) -> doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2]) + | LEXP_memory (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps) + | _ -> parens (doc_lexp lexp) +and doc_pexps pexps = surround 2 0 lbrace (separate_map (comma ^^ hardline) doc_pexp pexps) rbrace +and doc_pexp (Pat_aux (pat_aux, _)) = + match pat_aux with + | Pat_exp (pat, exp) -> separate space [doc_pat pat; string "=>"; doc_exp exp] + | Pat_when (pat, wh, exp) -> + separate space [doc_pat pat; string "if"; doc_exp wh; string "=>"; doc_exp exp] +and doc_letbind (LB_aux (lb_aux, _)) = + match lb_aux with + | LB_val (pat, exp) -> + separate space [doc_pat pat; equals; doc_exp exp] + +let doc_funcl funcl = string "FUNCL" + +let doc_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp,_)), _)) = + match pexp with + | Pat_exp (pat,exp) -> + group (separate space [doc_id id; doc_pat pat; equals; doc_exp exp]) + | Pat_when (pat,wh,exp) -> + group (separate space [doc_id id; parens (separate space [doc_pat pat; string "if"; doc_exp wh]); string "="; doc_exp 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_kind(bk,v) -> string "DT_kind" (* separate space [string "default"; doc_bkind bk; doc_var v] *) + | DT_typ(ts,id) -> separate space [string "default"; doc_typschm ts; doc_id id] | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord] -let doc_spec (VS_aux(v,_)) = match v with - | 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]) - | _ -> failwith "Invalid valspec" - -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) - | TD_register(id,n1,n2,rs) -> - let doc_rid (r,id) = separate space [doc_range r; colon; doc_id id] ^^ semi in - let doc_rids = group (separate_map (break 1) doc_rid rs) in - doc_op equals - (string "typedef" ^^ space ^^ doc_id id) - (separate space [ - string "register bits"; - brackets (doc_nexp n1 ^^ colon ^^ doc_nexp n2); - braces doc_rids; - ]) - -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 doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), _)) = + match funcls with + | [] -> failwith "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 sep = hardline ^^ string "and" ^^ space in + let clauses = separate_map sep doc_funcl funcls in + string "function" ^^ space ^^ clauses 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 + | DEC_reg (typ, id) -> separate space [string "register"; doc_id id; colon; doc_typ typ] + | DEC_alias(id,alspec) -> string "ALIAS" + | DEC_typ_alias(typ,id,alspec) -> string "ALIAS" + +let doc_field (typ, id) = + separate space [doc_id id; colon; doc_typ typ] + +let doc_union (Tu_aux (tu, l)) = match tu with + | Tu_id id -> doc_id id + | Tu_ty_id (typ, id) -> separate space [doc_id id; colon; doc_typ typ] + +let doc_typdef (TD_aux(td,_)) = match td with + | TD_abbrev (id, _, typschm) -> + begin + match doc_typschm_quants typschm with + | Some qdoc -> + doc_op equals (concat [string "type"; space; doc_id id; space; qdoc]) (doc_typschm_typ typschm) + | None -> + doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm) + end + | TD_enum (id, _, ids, _) -> + separate space [string "enum"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace] + | TD_record (id, _, TypQ_aux (TypQ_no_forall, _), fields, _) | TD_record (id, _, TypQ_aux (TypQ_tq [], _), fields, _) -> + separate space [string "struct"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] + | TD_record (id, _, TypQ_aux (TypQ_tq qs, _), fields, _) -> + separate space [string "struct"; doc_id id; doc_quants qs; equals; + surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] + | TD_variant (id, _, TypQ_aux (TypQ_no_forall, _), unions, _) | TD_variant (id, _, TypQ_aux (TypQ_tq [], _), unions, _) -> + separate space [string "union"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] + | TD_variant (id, _, TypQ_aux (TypQ_tq qs, _), unions, _) -> + separate space [string "union"; doc_id id; doc_quants qs; equals; + surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] + | _ -> string "TYPEDEF" + +let doc_spec (VS_aux(v,_)) = + let doc_extern ext = + let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^ + utf8string ("\"" ^ String.escaped id ^ "\"")) (ext b) in + let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"]) in + if docs = [] then empty else equals ^^ space ^^ braces (separate (comma ^^ space) docs) + in + match v with + | VS_val_spec(ts,id,ext,is_cast) -> + string "val" ^^ space + ^^ (if is_cast then (string "cast" ^^ space) else empty) + ^^ doc_id id ^^ space + ^^ doc_extern ext + ^^ colon ^^ space + ^^ doc_typschm ts + +let doc_prec = function + | Infix -> string "infix" + | InfixL -> string "infixl" + | InfixR -> string "infixr" + +let doc_kind_def (KD_aux (KD_nabbrev (_, id, _, nexp), _)) = + separate space [string "integer"; doc_id id; equals; doc_nexp nexp] + +let rec doc_scattered (SD_aux (sd_aux, _)) = + match sd_aux with + | SD_scattered_function (_, _, _, id) -> + string "scattered" ^^ space ^^ string "function" ^^ space ^^ doc_id id + | SD_scattered_funcl funcl -> + string "function" ^^ space ^^ string "clause" ^^ space ^^ doc_funcl funcl + | SD_scattered_end id -> + string "end" ^^ space ^^ doc_id id + | _ -> string "SCATTERED" 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_kind k_def -> doc_kind_def k_def | DEF_fundef f_def -> doc_fundef f_def - | DEF_val lbind -> doc_let lbind + | DEF_val lbind -> string "let" ^^ space ^^ doc_letbind lbind + | DEF_internal_mutrec fundefs -> + (string "mutual {" ^//^ separate_map (hardline ^^ hardline) doc_fundef fundefs) + ^^ hardline ^^ string "}" | DEF_reg_dec dec -> doc_dec dec | DEF_scattered sdef -> doc_scattered sdef + | DEF_fixity (prec, n, id) -> + fixities := Bindings.add id (prec, Big_int.to_int n) !fixities; + separate space [doc_prec prec; doc_int n; doc_id id] | 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 + 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)) = 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); +let pp_defs f d = ToChannel.pretty 1. 80 f (doc_defs d) + +let pretty_sail f doc = ToChannel.pretty 1. 120 f doc + +let to_string doc = + let b = Buffer.create 120 in + ToBuffer.pretty 1. 120 b doc; Buffer.contents b |