From 2725bc8aac309d408b1477fb67e47b54938c15d4 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 10 May 2024 01:45:49 +0100 Subject: [PATCH] Add attributes to sail_doc_backend output Rename _to_json to json_of_ to better match other usages Refactor Pretty_print_sail, adding a Pretty_print_sail.Printer functor which can be configured for different use cases. The module contains a include Printer (Default_print_config) so other code can just use Pretty_print_sail as before. The main use for this is in the documentation generation, as we want to be able to format code slightly differently than when we just dump the AST for debugging, e.g. re-introduce overloads. This is handled by the `resugar` flag in the pretty-printer config. The eventual ideal flow would be: constant-propagate -> pretty_print w/ resugar -> re-parse -> format_sail but we don't yet do the last two steps --- src/lib/ast_util.ml | 22 +- src/lib/ast_util.mli | 15 + src/lib/pretty_print_sail.ml | 1567 ++++++++++++----------- src/lib/type_check.ml | 7 +- src/lib/util.ml | 5 + src/lib/util.mli | 5 + src/sail_doc_backend/docinfo.ml | 231 ++-- src/sail_doc_backend/docinfo.mli | 10 +- src/sail_doc_backend/sail_plugin_doc.ml | 12 +- src/sail_latex_backend/latex.ml | 2 +- 10 files changed, 1033 insertions(+), 843 deletions(-) diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index f57707b28..f6a75552c 100644 --- a/src/lib/ast_util.ml +++ b/src/lib/ast_util.ml @@ -82,13 +82,33 @@ let rec string_of_attribute_data (AD_aux (aux, _)) = ^ " }" | AD_string s -> "\"" ^ s ^ "\"" | AD_num n -> Big_int.to_string n - | AD_list cs -> "[" ^ Util.string_of_list ", " string_of_attribute_data cs ^ "]" + | AD_list vs -> "[" ^ Util.string_of_list ", " string_of_attribute_data vs ^ "]" | AD_bool b -> string_of_bool b let string_of_attribute attr = function | None -> Printf.sprintf "$[%s]" attr | Some data -> Printf.sprintf "$[%s %s]" attr (string_of_attribute_data data) +let rec json_of_attribute_data (AD_aux (aux, _)) = + match aux with + | AD_object kvs -> `Assoc (List.map (fun (k, v) -> (k, json_of_attribute_data v)) kvs) + | AD_string s -> `String s + | AD_num n when Big_int.less_equal (Big_int.of_int min_int) n && Big_int.less_equal n (Big_int.of_int max_int) -> + `Int (Big_int.to_int n) + | AD_num n -> `String (Big_int.to_string n) + | AD_list vs -> `List (List.map json_of_attribute_data vs) + | AD_bool b -> `Bool b + +let attribute_data_object = function AD_aux (AD_object kvs, _) -> Some kvs | _ -> None + +let attribute_data_bool = function AD_aux (AD_bool b, _) -> Some b | _ -> None + +let attribute_data_string = function AD_aux (AD_string s, _) -> Some s | _ -> None + +let json_of_attribute attr = function + | None -> `String attr + | Some data -> `List [`String attr; json_of_attribute_data data] + let empty_uannot = { attrs = [] } let add_attribute l attr arg (annot : uannot) = { attrs = (l, attr, arg) :: annot.attrs } diff --git a/src/lib/ast_util.mli b/src/lib/ast_util.mli index 29339add2..e232693a0 100644 --- a/src/lib/ast_util.mli +++ b/src/lib/ast_util.mli @@ -78,12 +78,25 @@ module Big_int = Nat_big_num annotations {!Type_check.tannot}. *) type uannot +(** The empty annotation *) val empty_uannot : uannot +(** {2 Attributes} *) + val string_of_attribute : string -> attribute_data option -> string val string_of_attribute_data : attribute_data -> string +val json_of_attribute : string -> attribute_data option -> Yojson.Basic.t + +val json_of_attribute_data : attribute_data -> Yojson.Basic.t + +val attribute_data_object : attribute_data -> (string * attribute_data) list option + +val attribute_data_bool : attribute_data -> bool option + +val attribute_data_string : attribute_data -> string option + (** Add an attribute to an annotation. Attributes are attached to expressions in Sail via: {@sail[ $[attribute argument] expression @@ -118,6 +131,8 @@ val def_annot_map_loc : (l -> l) -> def_annot -> def_annot information with the various [locate_] functions in this module. *) val no_annot : l * uannot +(** {1 Generated locations} *) + (** [gen_loc l] takes a location l and generates a location which means 'generated/derived from location l'. This is useful for debugging errors that occur in generated code. *) diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml index 8d48a8b90..210567ad3 100644 --- a/src/lib/pretty_print_sail.ml +++ b/src/lib/pretty_print_sail.ml @@ -70,769 +70,825 @@ open Ast_defs open Ast_util open PPrint -let opt_use_heuristics = ref false -let opt_insert_braces = ref false - 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 | Operator op -> "operator " ^ op) - -let doc_kid kid = string (Ast_util.string_of_kid kid) - -let doc_attr attr arg = string (string_of_attribute attr arg) ^^ space - -let doc_def_annot def_annot = - (match def_annot.doc_comment with Some str -> string "/*!" ^^ string str ^^ string "*/" ^^ hardline | _ -> empty) - ^^ ( match def_annot.attrs with - | [] -> empty - | attrs -> separate_map hardline (fun (_, attr, arg) -> doc_attr attr arg) attrs ^^ hardline - ) - ^^ match def_annot.visibility with Private _ -> string "private" ^^ space | Public -> empty - -let doc_kopt_no_parens = function - | kopt when is_int_kopt kopt -> doc_kid (kopt_kid kopt) - | kopt when is_typ_kopt kopt -> separate space [doc_kid (kopt_kid kopt); colon; string "Type"] - | kopt -> separate space [doc_kid (kopt_kid kopt); colon; string "Bool"] - -let doc_kopt = function - | kopt when is_int_kopt kopt -> doc_kopt_no_parens kopt - | kopt -> parens (doc_kopt_no_parens kopt) - -let doc_int n = string (Big_int.to_string n) - -let doc_ord (Ord_aux (o, _)) = match o with Ord_inc -> string "inc" | Ord_dec -> string "dec" - -let rec doc_typ_pat (TP_aux (tpat_aux, _)) = - match tpat_aux with - | TP_wild -> string "_" - | TP_var kid -> doc_kid kid - | TP_app (f, tpats) -> doc_id f ^^ parens (separate_map (comma ^^ space) doc_typ_pat tpats) - -let rec doc_nexp 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_app (Id_aux (Operator op, _), [n1; n2]) -> separate space [atomic_nexp n1; string op; atomic_nexp n2] - | Nexp_app (_id, _nexps) -> string (string_of_nexp nexp) - (* This segfaults??!!!! - doc_id id ^^ (parens (separate_map (comma ^^ space) doc_nexp nexps)) - *) - | 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_if (i, t, e) -> separate space [string "if"; doc_nc i; string "then"; nexp1 t; string "else"; nexp1 e] - | _ -> nexp1 nexp - and nexp1 (Nexp_aux (n_aux, _) as nexp) = - match n_aux with - | Nexp_sum (n1, Nexp_aux (Nexp_neg n2, _)) | Nexp_minus (n1, n2) -> separate space [nexp1 n1; string "-"; nexp2 n2] - | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when Big_int.less c Big_int.zero -> - separate space [nexp1 n1; string "-"; doc_int (Big_int.abs c)] - | Nexp_sum (n1, n2) -> separate space [nexp1 n1; string "+"; nexp2 n2] - | _ -> nexp2 nexp - and nexp2 (Nexp_aux (n_aux, _) as nexp) = - match n_aux with Nexp_times (n1, n2) -> separate space [nexp2 n1; string "*"; nexp3 n2] | _ -> nexp3 nexp - and nexp3 (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 nexp - -and doc_nc 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_id id -> doc_id id - | 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_gt (n1, n2) -> nc_op ">" n1 n2 - | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2 - | NC_bounded_lt (n1, n2) -> nc_op "<" n1 n2 - | NC_set (nexp, ints) -> - separate space [doc_nexp nexp; string "in"; braces (separate_map (comma ^^ space) doc_int ints)] - | NC_app (id, args) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_typ_arg args) - | NC_var kid -> doc_kid kid - | NC_or _ | NC_and _ -> nc0 ~parenthesize:true nc - and nc0 ?(parenthesize = false) nc = - (* Rather than parens (nc0 x) we use nc0 ~parenthesize:true x, because if - we rewrite a disjunction as a set constraint, then we can - always omit the parens. *) - let parens' = if parenthesize then parens else fun x -> x in - let disjs = constraint_disj nc in - let collect_constants kid = function - | NC_aux (NC_equal (Nexp_aux (Nexp_var kid', _), Nexp_aux (Nexp_constant c, _)), _) when Kid.compare kid kid' = 0 - -> - Some c - | _ -> None +module type PRINT_CONFIG = sig + val insert_braces : bool + val resugar : bool +end + +module Printer (Config : PRINT_CONFIG) = struct + 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 | Operator op -> "operator " ^ op) + + let doc_kid kid = string (Ast_util.string_of_kid kid) + + let doc_attr attr arg = string (string_of_attribute attr arg) ^^ space + + let doc_def_annot def_annot = + (match def_annot.doc_comment with Some str -> string "/*!" ^^ string str ^^ string "*/" ^^ hardline | _ -> empty) + ^^ ( match def_annot.attrs with + | [] -> empty + | attrs -> separate_map hardline (fun (_, attr, arg) -> doc_attr attr arg) attrs ^^ hardline + ) + ^^ match def_annot.visibility with Private _ -> string "private" ^^ space | Public -> empty + + let doc_kopt_no_parens = function + | kopt when is_int_kopt kopt -> doc_kid (kopt_kid kopt) + | kopt when is_typ_kopt kopt -> separate space [doc_kid (kopt_kid kopt); colon; string "Type"] + | kopt -> separate space [doc_kid (kopt_kid kopt); colon; string "Bool"] + + let doc_kopt = function + | kopt when is_int_kopt kopt -> doc_kopt_no_parens kopt + | kopt -> parens (doc_kopt_no_parens kopt) + + let doc_int n = string (Big_int.to_string n) + + let doc_ord (Ord_aux (o, _)) = match o with Ord_inc -> string "inc" | Ord_dec -> string "dec" + + let rec doc_typ_pat (TP_aux (tpat_aux, _)) = + match tpat_aux with + | TP_wild -> string "_" + | TP_var kid -> doc_kid kid + | TP_app (f, tpats) -> doc_id f ^^ parens (separate_map (comma ^^ space) doc_typ_pat tpats) + + let rec doc_nexp 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_app (Id_aux (Operator op, _), [n1; n2]) -> separate space [atomic_nexp n1; string op; atomic_nexp n2] + | Nexp_app (_id, _nexps) -> string (string_of_nexp nexp) + (* This segfaults??!!!! + doc_id id ^^ (parens (separate_map (comma ^^ space) doc_nexp nexps)) + *) + | 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_if (i, t, e) -> separate space [string "if"; doc_nc i; string "then"; nexp1 t; string "else"; nexp1 e] + | _ -> nexp1 nexp + and nexp1 (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_sum (n1, Nexp_aux (Nexp_neg n2, _)) | Nexp_minus (n1, n2) -> + separate space [nexp1 n1; string "-"; nexp2 n2] + | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when Big_int.less c Big_int.zero -> + separate space [nexp1 n1; string "-"; doc_int (Big_int.abs c)] + | Nexp_sum (n1, n2) -> separate space [nexp1 n1; string "+"; nexp2 n2] + | _ -> nexp2 nexp + and nexp2 (Nexp_aux (n_aux, _) as nexp) = + match n_aux with Nexp_times (n1, n2) -> separate space [nexp2 n1; string "*"; nexp3 n2] | _ -> nexp3 nexp + and nexp3 (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 - match disjs with - | NC_aux (NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant c, _)), _) :: ncs -> begin - match Util.option_all (List.map (collect_constants kid) ncs) with - | None | Some [] -> parens' (separate_map (space ^^ bar ^^ space) nc1 disjs) - | Some cs -> separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int (c :: cs))] - end - | _ -> parens' (separate_map (space ^^ bar ^^ space) nc1 disjs) - and nc1 nc = - let conjs = constraint_conj nc in - separate_map (space ^^ string "&" ^^ space) atomic_nc conjs - in - atomic_nc (constraint_simp nc) - -and doc_typ ?(simple = false) (Typ_aux (typ_aux, l)) = - match typ_aux with - | Typ_id id -> doc_id id - | Typ_app (id, []) -> doc_id id - | Typ_app (Id_aux (Operator str, _), [x; y]) -> separate space [doc_typ_arg x; string str; doc_typ_arg y] - | Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 -> - string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs) - | Typ_app (id, typs) when Id.compare id (mk_id "atom_bool") = 0 -> - string "bool" ^^ parens (separate_map (string ", ") doc_typ_arg typs) - | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs) - | Typ_tuple typs -> parens (separate_map (string ", ") doc_typ typs) - | Typ_var kid -> doc_kid kid - (* Resugar set types like {|1, 2, 3|} *) - | Typ_exist - ( [kopt], - NC_aux (NC_set (Nexp_aux (Nexp_var kid1, _), ints), _), - Typ_aux (Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var kid2, _)), _)]), _) - ) - when Kid.compare (kopt_kid kopt) kid1 == 0 && Kid.compare kid1 kid2 == 0 && Id.compare (mk_id "atom") id == 0 -> - enclose (char '{') (char '}') (separate_map (string ", ") doc_int ints) - | Typ_exist (kopts, nc, typ) -> - braces (separate_map space doc_kopt kopts ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ) - | Typ_fn ([Typ_aux (Typ_tuple typs, _)], typ) -> - separate space [parens (doc_arg_typs typs); string "->"; doc_typ ~simple typ] - | Typ_fn (typs, typ) -> separate space [doc_arg_typs typs; string "->"; doc_typ ~simple typ] - | Typ_bidir (typ1, typ2) -> separate space [doc_typ typ1; string "<->"; doc_typ typ2] - | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown") - -and doc_typ_arg (A_aux (ta_aux, _)) = - match ta_aux with A_typ typ -> doc_typ typ | A_nexp nexp -> doc_nexp nexp | A_bool nc -> doc_nc nc - -and doc_arg_typs = function [typ] -> doc_typ typ | typs -> parens (separate_map (comma ^^ space) doc_typ typs) - -let doc_subst (IS_aux (subst_aux, _)) = - match subst_aux with - | IS_typ (kid, typ) -> doc_kid kid ^^ space ^^ equals ^^ space ^^ doc_typ typ - | IS_id (id1, id2) -> doc_id id1 ^^ space ^^ equals ^^ space ^^ doc_id id2 - -let doc_kind (K_aux (k, _)) = string (match k with K_int -> "Int" | K_type -> "Type" | K_bool -> "Bool") - -let doc_kopts = separate_map space doc_kopt - -let doc_quants quants = - let rec get_kopts = function - | QI_aux (QI_id kopt, _) :: qis -> kopt :: get_kopts qis - | _ :: qis -> get_kopts qis - | [] -> [] - in - let qi_nc (QI_aux (qi_aux, _)) = match qi_aux with QI_constraint nc -> [nc] | _ -> [] in - let kdoc = doc_kopts (get_kopts 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_param_quants quants = - let doc_qi_kopt (QI_aux (qi_aux, _)) = - match qi_aux with - | QI_id kopt when is_int_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"] - | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"] - | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Bool"] - | QI_constraint _ -> [] - in - let qi_nc (QI_aux (qi_aux, _)) = match qi_aux with QI_constraint nc -> [nc] | _ -> [] in - let kdoc = separate (comma ^^ space) (List.concat (List.map doc_qi_kopt quants)) in - let ncs = List.concat (List.map qi_nc quants) in - match ncs with - | [] -> parens kdoc - | [nc] -> parens kdoc ^^ comma ^^ space ^^ doc_nc nc - | nc :: ncs -> parens kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) - -let doc_binding ?(simple = false) ((TypQ_aux (tq_aux, _) as typq), typ) = - match tq_aux with - | TypQ_no_forall -> doc_typ ~simple typ - | TypQ_tq [] -> doc_typ ~simple typ - | TypQ_tq qs -> - if !opt_use_heuristics && String.length (string_of_typquant typq) > 60 then ( - let kopts, ncs = quant_split typq in - if ncs = [] then string "forall" ^^ space ^^ separate_map space doc_kopt kopts ^^ dot ^//^ doc_typ ~simple typ - else - string "forall" ^^ space ^^ separate_map space doc_kopt kopts ^^ comma - ^//^ separate_map (space ^^ string "&" ^^ space) doc_nc ncs - ^^ dot ^^ hardline ^^ doc_typ ~simple typ - ) - else string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ ~simple typ - -let doc_typschm ?(simple = false) (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding ~simple (typq, typ) - -let doc_typschm_typ (TypSchm_aux (TypSchm_ts (_, typ), _)) = doc_typ typ - -let doc_typquant (TypQ_aux (tq_aux, _)) = - match tq_aux with TypQ_no_forall -> None | TypQ_tq [] -> None | TypQ_tq qs -> Some (doc_param_quants qs) - -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 rec doc_pat (P_aux (p_aux, (_, uannot))) = - let wrap, attrs_doc = - match get_attributes uannot with - | [] -> ((fun x -> x), empty) - | _ -> (parens, concat_map (fun (_, attr, arg) -> doc_attr attr arg) (get_attributes uannot)) - in - let pat_doc = - match p_aux with - | P_id id -> doc_id id - | P_or (pat1, pat2) -> parens (doc_pat pat1 ^^ string " | " ^^ doc_pat pat2) - | P_not pat -> string "~" ^^ parens (doc_pat pat) - | P_tuple 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, _), TP_aux (TP_var kid, _)) when Id.compare (id_of_kid kid) id == 0 -> doc_kid kid - | P_var (pat, tpat) -> parens (separate space [doc_pat pat; string "as"; doc_typ_pat tpat]) - | P_vector pats -> brackets (separate_map (comma ^^ space) doc_pat pats) - | P_vector_concat pats -> parens (separate_map (space ^^ string "@" ^^ space) doc_pat pats) - | P_vector_subrange (id, n, m) -> - if Big_int.equal n m then doc_id id ^^ brackets (string (Big_int.to_string n)) - else doc_id id ^^ brackets (string (Big_int.to_string n) ^^ string ".." ^^ string (Big_int.to_string m)) - | P_wild -> string "_" - | P_as (pat, id) -> parens (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) - | P_list pats -> string "[|" ^^ separate_map (comma ^^ space) doc_pat pats ^^ string "|]" - | P_cons (hd_pat, tl_pat) -> parens (separate space [doc_pat hd_pat; string "::"; doc_pat tl_pat]) - | P_string_append [] -> string "\"\"" - | P_string_append pats -> parens (separate_map (string " ^ ") doc_pat pats) - | P_struct (fpats, fwild) -> - let fpats = List.map (fun (field, pat) -> separate space [doc_id field; equals; doc_pat pat]) fpats in - let fwild = match fwild with FP_wild _ -> [string "_"] | FP_no_wild -> [] in - let fpats = fpats @ fwild in - separate space [string "struct"; lbrace; separate (comma ^^ space) fpats; rbrace] - in - wrap (attrs_doc ^^ pat_doc) - -(* 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, 7)); - (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 "==", (Infix, 4)); - (mk_id "&", (InfixR, 3)); - (mk_id "|", (InfixR, 2)); - ] - in - ref (fixities' : (prec * int) Bindings.t) - -type 'a vector_update = VU_single of 'a exp * 'a exp | VU_range of 'a exp * 'a exp * 'a exp - -let rec get_vector_updates (E_aux (e_aux, _) as exp) = - match e_aux with - | E_vector_update (exp1, exp2, exp3) -> - let input, updates = get_vector_updates exp1 in - (input, updates @ [VU_single (exp2, exp3)]) - | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> - let input, updates = get_vector_updates exp1 in - (input, updates @ [VU_range (exp2, exp3, exp4)]) - | _ -> (exp, []) - -let rec doc_exp (E_aux (e_aux, (_, uannot)) as exp) = - concat_map (fun (_, attr, arg) -> doc_attr attr arg) (get_attributes uannot) - ^^ - match e_aux with - | E_block [] -> string "()" - | E_block exps -> group (lbrace ^^ nest 4 (hardline ^^ doc_block exps) ^^ hardline ^^ rbrace) - (* 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) - | E_if (if_exp, then_exp, (E_aux (E_if (_, _, _), _) as else_exp)) when !opt_insert_braces -> - separate space [string "if"; doc_exp if_exp; string "then"] - ^^ space ^^ doc_exp_as_block then_exp ^^ space ^^ string "else" ^^ space ^^ doc_exp else_exp - | E_if (if_exp, then_exp, else_exp) when !opt_insert_braces -> - separate space [string "if"; doc_exp if_exp; string "then"] - ^^ space ^^ doc_exp_as_block then_exp ^^ space ^^ string "else" ^^ space ^^ doc_exp_as_block else_exp - (* Various rules to try to format if blocks nicely based on content. - There's also an if rule in doc_block for { ... if . then .; ... } because it's - unambiguous there. *) - | 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, E_aux (E_block (_ :: _ as then_exps), _), E_aux (E_block (_ :: _ as else_exps), _)) -> - separate space [string "if"; doc_exp if_exp; string "then {"] - ^^ group (nest 4 (hardline ^^ doc_block then_exps) ^^ hardline) - ^^ string "} else {" - ^^ group (nest 4 (hardline ^^ doc_block else_exps) ^^ hardline ^^ rbrace) - | E_if (if_exp, E_aux (E_block (_ :: _ as then_exps), _), (E_aux (E_if _, _) as else_exp)) -> - separate space [string "if"; doc_exp if_exp; string "then {"] - ^^ group (nest 4 (hardline ^^ doc_block then_exps) ^^ hardline) - ^^ string "} else " ^^ doc_exp else_exp - | E_if (if_exp, E_aux (E_block (_ :: _ as then_exps), _), else_exp) -> - separate space [string "if"; doc_exp if_exp; string "then {"] - ^^ group (nest 4 (hardline ^^ doc_block then_exps) ^^ hardline) - ^^ string "} else" ^//^ doc_exp else_exp - | E_if (if_exp, then_exp, E_aux (E_block (_ :: _ as else_exps), _)) -> - group ((separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) ^/^ string "else {") - ^^ group (nest 4 (hardline ^^ doc_block else_exps) ^^ hardline ^^ rbrace) - | 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) -> doc_atomic_exp exp1 ^^ space ^^ string "::" ^^ space ^^ doc_exp exp2 - | E_struct fexps -> separate space [string "struct"; string "{"; doc_fexps fexps; string "}"] - | E_loop (While, measure, cond, exp) -> - separate space ([string "while"] @ doc_measure measure @ [doc_exp cond; string "do"; doc_exp exp]) - | E_loop (Until, measure, cond, exp) -> - separate space ([string "repeat"] @ doc_measure measure @ [doc_exp exp; string "until"; doc_exp cond]) - | E_struct_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_match (exp, pexps) -> separate space [string "match"; doc_exp exp; doc_pexps pexps] - | E_let (LB_aux (LB_val (pat, binding), _), exp) -> doc_let_style "let" (doc_pat pat) (doc_exp binding) exp - | E_internal_plet (pat, exp1, exp2) -> doc_let_style "internal_plet" (doc_pat pat) (doc_exp exp1) exp2 - | E_var (lexp, binding, exp) -> doc_let_style "var" (doc_lexp lexp) (doc_exp binding) exp - | E_assign (lexp, exp) -> separate space [doc_lexp lexp; equals; doc_exp exp] - | E_for (id, exp1, exp2, exp3, order, exp4) -> - 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; - ] - ) - ) + nexp0 nexp + + and doc_nc 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_id id -> doc_id id + | 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_gt (n1, n2) -> nc_op ">" n1 n2 + | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2 + | NC_bounded_lt (n1, n2) -> nc_op "<" n1 n2 + | NC_set (nexp, ints) -> + separate space [doc_nexp nexp; string "in"; braces (separate_map (comma ^^ space) doc_int ints)] + | NC_app (id, args) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_typ_arg args) + | NC_var kid -> doc_kid kid + | NC_or _ | NC_and _ -> nc0 ~parenthesize:true nc + and nc0 ?(parenthesize = false) nc = + (* Rather than parens (nc0 x) we use nc0 ~parenthesize:true x, because if + we rewrite a disjunction as a set constraint, then we can + always omit the parens. *) + let parens' = if parenthesize then parens else fun x -> x in + let disjs = constraint_disj nc in + let collect_constants kid = function + | NC_aux (NC_equal (Nexp_aux (Nexp_var kid', _), Nexp_aux (Nexp_constant c, _)), _) + when Kid.compare kid kid' = 0 -> + Some c + | _ -> None in - header ^^ space ^^ doc_exp exp4 - (* 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 (E_aux (E_lit (L_aux (L_unit, _)), _)) -> string "return()" - | 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] - | E_internal_assume (nc, exp) -> doc_let_style_general "internal_assume" (parens (doc_nc nc)) None exp - | _ -> doc_atomic_exp exp - -and doc_let_style keyword lhs rhs body = doc_let_style_general keyword lhs (Some rhs) body - -and doc_let_style_general keyword lhs rhs body = - (* Avoid staircases *) - let ( ^///^ ) = - match unaux_exp body with E_let _ | E_var _ | E_internal_plet _ | E_internal_assume _ -> ( ^/^ ) | _ -> ( ^//^ ) - in - match rhs with - | Some rhs -> group ((separate space [string keyword; lhs; equals] ^//^ rhs) ^/^ string "in") ^///^ doc_exp body - | None -> group ((string keyword ^//^ lhs) ^/^ string "in") ^///^ doc_exp body - -and doc_measure (Measure_aux (m_aux, _)) = - match m_aux with Measure_none -> [] | Measure_some exp -> [string "termination_measure"; braces (doc_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 -> 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 -> 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 -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]) - with Not_found -> parens (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_typ (typ, exp) -> separate space [doc_atomic_exp exp; colon; doc_typ typ] - | E_lit lit -> doc_lit lit - | 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 _ | E_vector_update_subrange _ -> - let input, updates = get_vector_updates exp in - let updates_doc = separate_map (comma ^^ space) doc_vector_update updates in - brackets (separate space [doc_exp input; string "with"; updates_doc]) - | E_internal_value v -> - if !Interactive.opt_interactive then string (Value.string_of_value v |> Util.green |> Util.clear) - else string (Value.string_of_value v) - | _ -> parens (doc_exp exp) - -and doc_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_let (LB_aux (LB_val (pat, binding), _), exp), _)] -> - separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block [exp] - | [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 - | E_aux (E_if (if_exp, then_exp, E_aux ((E_lit (L_aux (L_unit, _)) | E_block []), _)), _) :: exps -> - group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp]) - ^^ semi ^^ hardline ^^ doc_block exps - | [exp] -> doc_exp exp - | exp :: exps -> doc_exp exp ^^ semi ^^ hardline ^^ doc_block exps - -and doc_lexp (LE_aux (l_aux, _) as lexp) = - match l_aux with LE_typ (typ, id) -> separate space [doc_id id; colon; doc_typ typ] | _ -> doc_atomic_lexp lexp - -and doc_atomic_lexp (LE_aux (l_aux, _) as lexp) = - match l_aux with - | LE_id id -> doc_id id - | LE_deref exp -> lparen ^^ string "*" ^^ doc_atomic_exp exp ^^ rparen - | LE_tuple lexps -> lparen ^^ separate_map (comma ^^ space) doc_lexp lexps ^^ rparen - | LE_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id - | LE_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp) - | LE_vector_range (lexp, exp1, exp2) -> - doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2]) - | LE_vector_concat lexps -> parens (separate_map (string " @ ") doc_lexp lexps) - | LE_app (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] - -and doc_exp_as_block (E_aux (aux, _) as exp) = - match aux with - | E_block _ | E_lit _ -> doc_exp exp - | _ when !opt_insert_braces -> group (lbrace ^^ nest 4 (hardline ^^ doc_block [exp]) ^^ hardline ^^ rbrace) - | _ -> doc_exp exp - -and doc_vector_update = function - | VU_single (idx, value) -> begin - match (unaux_exp idx, unaux_exp value) with - | E_id id, E_id id' when Id.compare id id' == 0 -> doc_atomic_exp idx - | _, _ -> separate space [doc_atomic_exp idx; equals; doc_exp value] - end - | VU_range (high, low, value) -> - separate space [doc_atomic_exp high; string ".."; doc_atomic_exp low; equals; doc_exp value] - -let doc_funcl (FCL_aux (FCL_funcl (id, Pat_aux (pexp, _)), (def_annot, _))) = - doc_def_annot def_annot - ^^ - match pexp with - | Pat_exp (pat, exp) -> group (separate space [doc_id id; doc_pat pat; equals; doc_exp_as_block 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_as_block exp] + match disjs with + | NC_aux (NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant c, _)), _) :: ncs -> begin + match Util.option_all (List.map (collect_constants kid) ncs) with + | None | Some [] -> parens' (separate_map (space ^^ bar ^^ space) nc1 disjs) + | Some cs -> + separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int (c :: cs))] + end + | _ -> parens' (separate_map (space ^^ bar ^^ space) nc1 disjs) + and nc1 nc = + let conjs = constraint_conj nc in + separate_map (space ^^ string "&" ^^ space) atomic_nc conjs + in + atomic_nc (constraint_simp nc) + + and doc_typ (Typ_aux (typ_aux, l)) = + match typ_aux with + | Typ_id id -> doc_id id + | Typ_app (id, []) -> doc_id id + | Typ_app (Id_aux (Operator str, _), [x; y]) -> separate space [doc_typ_arg x; string str; doc_typ_arg y] + | Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 -> + string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs) + | Typ_app (id, typs) when Id.compare id (mk_id "atom_bool") = 0 -> + string "bool" ^^ parens (separate_map (string ", ") doc_typ_arg typs) + | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs) + | Typ_tuple typs -> parens (separate_map (string ", ") doc_typ typs) + | Typ_var kid -> doc_kid kid + (* Resugar set types like {|1, 2, 3|} *) + | Typ_exist + ( [kopt], + NC_aux (NC_set (Nexp_aux (Nexp_var kid1, _), ints), _), + Typ_aux (Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var kid2, _)), _)]), _) ) + when Kid.compare (kopt_kid kopt) kid1 == 0 && Kid.compare kid1 kid2 == 0 && Id.compare (mk_id "atom") id == 0 -> + enclose (char '{') (char '}') (separate_map (string ", ") doc_int ints) + | Typ_exist (kopts, nc, typ) -> + braces (separate_map space doc_kopt kopts ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ) + | Typ_fn ([Typ_aux (Typ_tuple typs, _)], typ) -> + separate space [parens (doc_arg_typs typs); string "->"; doc_typ typ] + | Typ_fn (typs, typ) -> separate space [doc_arg_typs typs; string "->"; doc_typ typ] + | Typ_bidir (typ1, typ2) -> separate space [doc_typ typ1; string "<->"; doc_typ typ2] + | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown") + + and doc_typ_arg (A_aux (ta_aux, _)) = + match ta_aux with A_typ typ -> doc_typ typ | A_nexp nexp -> doc_nexp nexp | A_bool nc -> doc_nc nc + + and doc_arg_typs = function [typ] -> doc_typ typ | typs -> parens (separate_map (comma ^^ space) doc_typ typs) + + let doc_subst (IS_aux (subst_aux, _)) = + match subst_aux with + | IS_typ (kid, typ) -> doc_kid kid ^^ space ^^ equals ^^ space ^^ doc_typ typ + | IS_id (id1, id2) -> doc_id id1 ^^ space ^^ equals ^^ space ^^ doc_id id2 + + let doc_kind (K_aux (k, _)) = string (match k with K_int -> "Int" | K_type -> "Type" | K_bool -> "Bool") + + let doc_kopts = separate_map space doc_kopt + + let doc_quants quants = + let rec get_kopts = function + | QI_aux (QI_id kopt, _) :: qis -> kopt :: get_kopts qis + | _ :: qis -> get_kopts qis + | [] -> [] + in + let qi_nc (QI_aux (qi_aux, _)) = match qi_aux with QI_constraint nc -> [nc] | _ -> [] in + let kdoc = doc_kopts (get_kopts 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_param_quants quants = + let doc_qi_kopt (QI_aux (qi_aux, _)) = + match qi_aux with + | QI_id kopt when is_int_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"] + | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"] + | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Bool"] + | QI_constraint _ -> [] + in + let qi_nc (QI_aux (qi_aux, _)) = match qi_aux with QI_constraint nc -> [nc] | _ -> [] in + let kdoc = separate (comma ^^ space) (List.concat (List.map doc_qi_kopt quants)) in + let ncs = List.concat (List.map qi_nc quants) in + match ncs with + | [] -> parens kdoc + | [nc] -> parens kdoc ^^ comma ^^ space ^^ doc_nc nc + | nc :: ncs -> parens 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 (_, typ), _)) = doc_typ typ + + let doc_typquant (TypQ_aux (tq_aux, _)) = + match tq_aux with TypQ_no_forall -> None | TypQ_tq [] -> None | TypQ_tq qs -> Some (doc_param_quants qs) + + 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_default (DT_aux (DT_order ord, _)) = separate space [string "default"; string "Order"; doc_ord ord] - -let doc_rec (Rec_aux (r, _)) = - match r with - | Rec_nonrec | Rec_rec -> empty - | Rec_measure (pat, exp) -> braces (doc_pat pat ^^ string " => " ^^ doc_exp exp) ^^ space - -let doc_fundef (FD_aux (FD_function (r, _, funcls), _)) = - match funcls with - | [] -> failwith "Empty function list" - | _ -> - let rec_pp = doc_rec r in - let sep = hardline ^^ string "and" ^^ space in - let clauses = separate_map sep doc_funcl funcls in - string "function" ^^ space ^^ rec_pp ^^ clauses - -let rec doc_mpat (MP_aux (mp_aux, _) as mpat) = - match mp_aux with - | MP_id id -> doc_id id - | MP_tuple pats -> lparen ^^ separate_map (comma ^^ space) doc_mpat pats ^^ rparen - | MP_lit lit -> doc_lit lit - | MP_vector pats -> brackets (separate_map (comma ^^ space) doc_mpat pats) - | MP_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_mpat pats - | MP_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_mpat pats) - | MP_list pats -> string "[|" ^^ separate_map (comma ^^ space) doc_mpat pats ^^ string "|]" - | _ -> string (string_of_mpat mpat) - -let doc_mpexp (MPat_aux (mpexp, _)) = - match mpexp with - | MPat_pat mpat -> doc_mpat mpat - | MPat_when (mpat, guard) -> doc_mpat mpat ^^ space ^^ string "if" ^^ space ^^ doc_exp guard - -let doc_mapcl (MCL_aux (cl, (def_annot, _))) = - doc_def_annot def_annot - ^^ - match cl with - | MCL_bidir (mpexp1, mpexp2) -> - let left = doc_mpexp mpexp1 in - let right = doc_mpexp mpexp2 in - separate space [left; string "<->"; right] - | MCL_forwards pexp -> string "forwards" ^^ space ^^ doc_pexp pexp - | MCL_backwards pexp -> string "backwards" ^^ space ^^ doc_pexp pexp - -let doc_mapdef (MD_aux (MD_mapping (id, _, mapcls), _)) = - match mapcls with - | [] -> failwith "Empty mapping" - | _ -> - let sep = string "," ^^ hardline in - let clauses = separate_map sep doc_mapcl mapcls in - string "mapping" ^^ space ^^ doc_id id ^^ space ^^ string "=" ^^ space ^^ surround 2 0 lbrace clauses rbrace - -let doc_dec (DEC_aux (reg, _)) = - match reg with - | DEC_reg (typ, id, opt_exp) -> ( - match opt_exp with - | None -> separate space [string "register"; doc_id id; colon; doc_typ typ] - | Some exp -> separate space [string "register"; doc_id id; colon; doc_typ typ; equals; doc_exp exp] - ) - -let doc_field (typ, id) = separate space [doc_id id; colon; doc_typ typ] - -let doc_union (Tu_aux (Tu_ty_id (typ, id), def_annot)) = - doc_def_annot def_annot ^^ separate space [doc_id id; colon; doc_typ typ] - -let rec doc_index_range (BF_aux (ir, _)) = - match ir with - | BF_single i -> doc_nexp i - | BF_range (i, j) -> doc_nexp i ^^ string ".." ^^ doc_nexp j - | BF_concat (i, j) -> parens (doc_index_range i ^^ space ^^ at ^^ space ^^ doc_index_range j) - -let doc_typ_arg_kind sep (A_aux (aux, _)) = - match aux with - | A_nexp _ -> space ^^ string sep ^^ space ^^ string "Int" - | A_bool _ -> space ^^ string sep ^^ space ^^ string "Bool" - | A_typ _ -> empty - -let doc_typdef (TD_aux (td, _)) = - match td with - | TD_abstract (id, kind) -> begin doc_op colon (concat [string "type"; space; doc_id id]) (doc_kind kind) end - | TD_abbrev (id, typq, typ_arg) -> begin - match doc_typquant typq with - | Some qdoc -> - doc_op equals - (concat [string "type"; space; doc_id id; qdoc; doc_typ_arg_kind "->" typ_arg]) - (doc_typ_arg typ_arg) - | None -> - doc_op equals (concat [string "type"; space; doc_id id; doc_typ_arg_kind ":" typ_arg]) (doc_typ_arg typ_arg) - 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_param_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 + let rec doc_pat (P_aux (p_aux, (_, uannot))) = + let wrap, attrs_doc = + match get_attributes uannot with + | [] -> ((fun x -> x), empty) + | _ -> (parens, concat_map (fun (_, attr, arg) -> doc_attr attr arg) (get_attributes uannot)) + in + let pat_doc = + match p_aux with + | P_id id -> doc_id id + | P_or (pat1, pat2) -> parens (doc_pat pat1 ^^ string " | " ^^ doc_pat pat2) + | P_not pat -> string "~" ^^ parens (doc_pat pat) + | P_tuple 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, _), TP_aux (TP_var kid, _)) when Id.compare (id_of_kid kid) id == 0 -> doc_kid kid + | P_var (pat, tpat) -> parens (separate space [doc_pat pat; string "as"; doc_typ_pat tpat]) + | P_vector pats -> brackets (separate_map (comma ^^ space) doc_pat pats) + | P_vector_concat pats -> parens (separate_map (space ^^ string "@" ^^ space) doc_pat pats) + | P_vector_subrange (id, n, m) -> + if Big_int.equal n m then doc_id id ^^ brackets (string (Big_int.to_string n)) + else doc_id id ^^ brackets (string (Big_int.to_string n) ^^ string ".." ^^ string (Big_int.to_string m)) + | P_wild -> string "_" + | P_as (pat, id) -> parens (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) + | P_list pats -> string "[|" ^^ separate_map (comma ^^ space) doc_pat pats ^^ string "|]" + | P_cons (hd_pat, tl_pat) -> parens (separate space [doc_pat hd_pat; string "::"; doc_pat tl_pat]) + | P_string_append [] -> string "\"\"" + | P_string_append pats -> parens (separate_map (string " ^ ") doc_pat pats) + | P_struct (fpats, fwild) -> + let fpats = List.map (fun (field, pat) -> separate space [doc_id field; equals; doc_pat pat]) fpats in + let fwild = match fwild with FP_wild _ -> [string "_"] | FP_no_wild -> [] in + let fpats = fpats @ fwild in + separate space [string "struct"; lbrace; separate (comma ^^ space) fpats; rbrace] + in + wrap (attrs_doc ^^ pat_doc) + + (* 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 [ - string "union"; - doc_id id; - doc_param_quants qs; - equals; - surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace; + (mk_id "^", (InfixR, 8)); + (mk_id "*", (InfixL, 7)); + (mk_id "/", (InfixL, 7)); + (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 "==", (Infix, 4)); + (mk_id "&", (InfixR, 3)); + (mk_id "|", (InfixR, 2)); ] - | TD_bitfield (id, typ, fields) -> - let doc_field (id, range) = separate space [doc_id id; colon; doc_index_range range] in - doc_op equals - (separate space [string "bitfield"; doc_id id; colon; doc_typ typ]) - (surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace) - -let doc_spec = - let doc_extern ext = - match ext with - | Some ext -> - let purity = if ext.pure then string "pure" ^^ space else string "monadic" ^^ space in - let docs = - List.map - (fun (backend, rep) -> string (backend ^ ":") ^^ space ^^ utf8string ("\"" ^ String.escaped rep ^ "\"")) - ext.bindings + in + ref (fixities' : (prec * int) Bindings.t) + + type 'a vector_update = VU_single of 'a exp * 'a exp | VU_range of 'a exp * 'a exp * 'a exp + + let rec get_vector_updates (E_aux (e_aux, _) as exp) = + match e_aux with + | E_vector_update (exp1, exp2, exp3) -> + let input, updates = get_vector_updates exp1 in + (input, updates @ [VU_single (exp2, exp3)]) + | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> + let input, updates = get_vector_updates exp1 in + (input, updates @ [VU_range (exp2, exp3, exp4)]) + | _ -> (exp, []) + + let get_overloaded_info uannot = + let open Util.Option_monad in + match get_attribute "overloaded" uannot with + | Some (_, Some arg) -> + let* obj = attribute_data_object arg in + let* name = Option.bind (List.assoc_opt "name" obj) attribute_data_string in + let* is_infix = Option.bind (List.assoc_opt "is_infix" obj) attribute_data_bool in + Some (name, is_infix) + | _ -> None + + let fix_binding pat binding = + (* If Config.resugar then turn `let x = (y : t) in ...` into `let x : t = y in ...` in some cases *) + match (pat, binding) with + | P_aux (P_id _, _), E_aux (E_typ (typ, exp), annot) when Config.resugar -> (P_aux (P_typ (typ, pat), annot), exp) + | _, _ -> (pat, binding) + + let rec doc_exp (E_aux (e_aux, (l, uannot)) as exp) = + let uannot, overloaded = + if Config.resugar then ( + match get_overloaded_info uannot with + | Some overloaded -> (remove_attribute "overloaded" uannot, Some overloaded) + | _ -> (uannot, None) + ) + else (uannot, None) + in + let uannot, is_setter = + if Config.resugar && Option.is_some (get_attribute "setter" uannot) then (remove_attribute "setter" uannot, true) + else (uannot, false) + in + concat_map (fun (_, attr, arg) -> doc_attr attr arg) (get_attributes uannot) + ^^ + match e_aux with + | E_block [] -> string "()" + | E_block exps -> group (lbrace ^^ nest 4 (hardline ^^ doc_block exps) ^^ hardline ^^ rbrace) + (* 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) + | E_if (if_exp, then_exp, (E_aux (E_if (_, _, _), _) as else_exp)) when Config.insert_braces -> + separate space [string "if"; doc_exp if_exp; string "then"] + ^^ space ^^ doc_exp_as_block then_exp ^^ space ^^ string "else" ^^ space ^^ doc_exp else_exp + | E_if (if_exp, then_exp, else_exp) when Config.insert_braces -> + separate space [string "if"; doc_exp if_exp; string "then"] + ^^ space ^^ doc_exp_as_block then_exp ^^ space ^^ string "else" ^^ space ^^ doc_exp_as_block else_exp + (* Various rules to try to format if blocks nicely based on content. + There's also an if rule in doc_block for { ... if . then .; ... } because it's + unambiguous there. *) + | 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, E_aux (E_block (_ :: _ as then_exps), _), E_aux (E_block (_ :: _ as else_exps), _)) -> + separate space [string "if"; doc_exp if_exp; string "then {"] + ^^ group (nest 4 (hardline ^^ doc_block then_exps) ^^ hardline) + ^^ string "} else {" + ^^ group (nest 4 (hardline ^^ doc_block else_exps) ^^ hardline ^^ rbrace) + | E_if (if_exp, E_aux (E_block (_ :: _ as then_exps), _), (E_aux (E_if _, _) as else_exp)) -> + separate space [string "if"; doc_exp if_exp; string "then {"] + ^^ group (nest 4 (hardline ^^ doc_block then_exps) ^^ hardline) + ^^ string "} else " ^^ doc_exp else_exp + | E_if (if_exp, E_aux (E_block (_ :: _ as then_exps), _), else_exp) -> + separate space [string "if"; doc_exp if_exp; string "then {"] + ^^ group (nest 4 (hardline ^^ doc_block then_exps) ^^ hardline) + ^^ string "} else" ^//^ doc_exp else_exp + | E_if (if_exp, then_exp, E_aux (E_block (_ :: _ as else_exps), _)) -> + group ((separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) ^/^ string "else {") + ^^ group (nest 4 (hardline ^^ doc_block else_exps) ^^ hardline ^^ rbrace) + | 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) -> doc_atomic_exp exp1 ^^ space ^^ string "::" ^^ space ^^ doc_exp exp2 + | E_struct fexps -> separate space [string "struct"; string "{"; doc_fexps fexps; string "}"] + | E_loop (While, measure, cond, exp) -> + separate space ([string "while"] @ doc_measure measure @ [doc_exp cond; string "do"; doc_exp exp]) + | E_loop (Until, measure, cond, exp) -> + separate space ([string "repeat"] @ doc_measure measure @ [doc_exp exp; string "until"; doc_exp cond]) + | E_struct_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_match (exp, pexps) -> separate space [string "match"; doc_exp exp; doc_pexps pexps] + | E_let (LB_aux (LB_val (pat, binding), _), exp) -> doc_let_style "let" (doc_pat pat) (doc_exp binding) exp + | E_internal_plet (pat, exp1, exp2) -> doc_let_style "internal_plet" (doc_pat pat) (doc_exp exp1) exp2 + | E_var (lexp, binding, exp) -> doc_let_style "var" (doc_lexp lexp) (doc_exp binding) exp + | E_assign (lexp, exp) -> separate space [doc_lexp lexp; equals; doc_exp exp] + | E_for (id, exp1, exp2, exp3, order, exp4) -> + 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 - equals ^^ space ^^ purity ^^ braces (separate (comma ^^ space) docs) - | None -> empty - in - function - | VS_aux (VS_val_spec (ts, id, ext), _) -> - string "val" ^^ space ^^ 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_loop_measures l = - separate_map - (comma ^^ break 1) - (function Loop (l, e) -> string (match l with While -> "while" | Until -> "until") ^^ space ^^ doc_exp e) - l - -let doc_scattered (SD_aux (sd_aux, _)) = - match sd_aux with - | SD_function (_, _, id) -> string "scattered" ^^ space ^^ string "function" ^^ space ^^ doc_id id - | SD_funcl funcl -> string "function" ^^ space ^^ string "clause" ^^ space ^^ doc_funcl funcl - | SD_end id -> string "end" ^^ space ^^ doc_id id - | SD_variant (id, TypQ_aux (TypQ_no_forall, _)) -> string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id - | SD_variant (id, TypQ_aux (TypQ_tq quants, _)) -> - string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id ^^ doc_param_quants quants - | SD_mapcl (id, mapcl) -> separate space [string "mapping clause"; doc_id id; equals; doc_mapcl mapcl] - | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_none, _)) -> separate space [string "scattered mapping"; doc_id id] - | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_some (typq, typ), _)) -> - separate space [string "scattered mapping"; doc_id id; colon; doc_binding (typq, typ)] - | SD_unioncl (id, tu) -> separate space [string "union clause"; doc_id id; equals; doc_union tu] - | SD_internal_unioncl_record (id, record_id, typq, fields) -> - let prefix = separate space [string "internal_union_record clause"; doc_id id; doc_id record_id] in - let params = - match typq with - | TypQ_aux (TypQ_no_forall, _) | TypQ_aux (TypQ_tq [], _) -> empty - | TypQ_aux (TypQ_tq qs, _) -> doc_param_quants qs - in - separate space - [prefix ^^ params; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] - | SD_enum id -> separate space [string "scattered enum"; doc_id id] - | SD_enumcl (id, member) -> separate space [string "enum clause"; doc_id id; equals; doc_id member] - -let doc_filter = function - | DEF_aux ((DEF_pragma ("file_start", _, _) | DEF_pragma ("file_end", _, _)), _) -> false - | _ -> true - -let rec doc_def_no_hardline (DEF_aux (aux, def_annot)) = - doc_def_annot def_annot - ^^ - match aux with - | DEF_default df -> doc_default df - | DEF_val v_spec -> doc_spec v_spec - | DEF_type t_def -> doc_typdef t_def - | DEF_fundef f_def -> doc_fundef f_def - | DEF_mapdef m_def -> doc_mapdef m_def - | DEF_constraint nc -> string "constraint" ^^ space ^^ doc_nc nc - | DEF_outcome (OV_aux (OV_outcome (id, typschm, args), _), defs) -> ( - string "outcome" ^^ space ^^ doc_id id ^^ space ^^ colon ^^ space ^^ doc_typschm typschm ^^ break 1 - ^^ (string "with" ^//^ separate_map (comma ^^ break 1) doc_kopt_no_parens args) - ^^ - match defs with - | [] -> empty - | _ -> break 1 ^^ (string "= {" ^//^ separate_map (hardline ^^ hardline) doc_def_no_hardline defs) ^/^ string "}" - ) - | DEF_instantiation (IN_aux (IN_id id, _), substs) -> ( - string "instantiation" ^^ space ^^ doc_id id - ^^ - match substs with - | [] -> empty - | _ -> (space ^^ string "with") ^//^ separate_map (comma ^^ break 1) doc_subst substs - ) - | DEF_impl funcl -> string "impl" ^^ space ^^ doc_funcl funcl - | DEF_let lbind -> string "let" ^^ space ^^ doc_letbind lbind - | DEF_internal_mutrec fundefs -> - (string "mutual {" ^//^ separate_map (hardline ^^ hardline) doc_fundef fundefs) ^^ hardline ^^ string "}" - | DEF_register dec -> doc_dec dec - | DEF_scattered sdef -> doc_scattered sdef - | DEF_measure (id, pat, exp) -> - string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_pat pat ^^ space ^^ equals ^/^ doc_exp exp - | DEF_loop_measures (id, measures) -> - string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_loop_measures measures - | DEF_pragma (pragma, arg, _) -> string ("$" ^ pragma ^ " " ^ arg) - | 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) -> - separate space - [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace] - -and doc_def def = group (doc_def_no_hardline def ^^ hardline) - -let doc_ast { defs; _ } = separate_map hardline doc_def (List.filter doc_filter defs) + header ^^ space ^^ doc_exp exp4 + (* 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 (E_aux (E_lit (L_aux (L_unit, _)), _)) -> string "return()" + | 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] + | E_internal_assume (nc, exp) -> doc_let_style_general "internal_assume" (parens (doc_nc nc)) None exp + | E_app (id, exps) -> begin + let handle_setter id otherwise = + if is_setter && List.length exps >= 2 then ( + let lexp = doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp (Util.butlast exps)) in + separate space [lexp; equals; doc_exp (Util.last exps)] + ) + else Lazy.force otherwise + in + match (overloaded, exps) with + | Some (name, true), [x; y] -> doc_exp (E_aux (E_app_infix (x, mk_id name, y), (l, uannot))) + | Some (name, false), _ -> + handle_setter (mk_id name) (lazy (doc_atomic_exp (E_aux (E_app (mk_id name, exps), (l, uannot))))) + | _, _ -> handle_setter id (lazy (doc_atomic_exp exp)) + end + | _ -> doc_atomic_exp exp + + and doc_let_style keyword lhs rhs body = doc_let_style_general keyword lhs (Some rhs) body + + and doc_let_style_general keyword lhs rhs body = + (* Avoid staircases *) + let ( ^///^ ) = + match unaux_exp body with E_let _ | E_var _ | E_internal_plet _ | E_internal_assume _ -> ( ^/^ ) | _ -> ( ^//^ ) + in + match rhs with + | Some rhs -> group ((separate space [string keyword; lhs; equals] ^//^ rhs) ^/^ string "in") ^///^ doc_exp body + | None -> group ((string keyword ^//^ lhs) ^/^ string "in") ^///^ doc_exp body + + and doc_measure (Measure_aux (m_aux, _)) = + match m_aux with Measure_none -> [] | Measure_some exp -> [string "termination_measure"; braces (doc_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 -> 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 -> 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 -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]) + with Not_found -> parens (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, (_, uannot)) as exp) = + match e_aux with + | E_typ (typ, exp) -> separate space [doc_atomic_exp exp; colon; doc_typ typ] + | E_lit lit -> doc_lit lit + | 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 _ | E_vector_update_subrange _ -> + let input, updates = get_vector_updates exp in + let updates_doc = separate_map (comma ^^ space) doc_vector_update updates in + brackets (separate space [doc_exp input; string "with"; updates_doc]) + | E_internal_value v -> + if !Interactive.opt_interactive then string (Value.string_of_value v |> Util.green |> Util.clear) + else string (Value.string_of_value v) + | _ -> parens (doc_exp exp) + + and doc_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, _)), _)] -> + let pat, binding = fix_binding pat binding in + separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps + | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), exp), _)] -> + let pat, binding = fix_binding pat binding in + separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block [exp] + | [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 + | E_aux (E_if (if_exp, then_exp, E_aux ((E_lit (L_aux (L_unit, _)) | E_block []), _)), _) :: exps -> + group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp]) + ^^ semi ^^ hardline ^^ doc_block exps + | [exp] -> doc_exp exp + | exp :: exps -> doc_exp exp ^^ semi ^^ hardline ^^ doc_block exps + + and doc_lexp (LE_aux (l_aux, _) as lexp) = + match l_aux with LE_typ (typ, id) -> separate space [doc_id id; colon; doc_typ typ] | _ -> doc_atomic_lexp lexp + + and doc_atomic_lexp (LE_aux (l_aux, _) as lexp) = + match l_aux with + | LE_id id -> doc_id id + | LE_deref exp -> lparen ^^ string "*" ^^ doc_atomic_exp exp ^^ rparen + | LE_tuple lexps -> lparen ^^ separate_map (comma ^^ space) doc_lexp lexps ^^ rparen + | LE_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id + | LE_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp) + | LE_vector_range (lexp, exp1, exp2) -> + doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2]) + | LE_vector_concat lexps -> parens (separate_map (string " @ ") doc_lexp lexps) + | LE_app (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] + + and doc_exp_as_block (E_aux (aux, _) as exp) = + match aux with + | E_block _ | E_lit _ -> doc_exp exp + | _ when Config.insert_braces -> group (lbrace ^^ nest 4 (hardline ^^ doc_block [exp]) ^^ hardline ^^ rbrace) + | _ -> doc_exp exp + + and doc_vector_update = function + | VU_single (idx, value) -> begin + match (unaux_exp idx, unaux_exp value) with + | E_id id, E_id id' when Id.compare id id' == 0 -> doc_atomic_exp idx + | _, _ -> separate space [doc_atomic_exp idx; equals; doc_exp value] + end + | VU_range (high, low, value) -> + separate space [doc_atomic_exp high; string ".."; doc_atomic_exp low; equals; doc_exp value] + + let doc_funcl (FCL_aux (FCL_funcl (id, Pat_aux (pexp, _)), (def_annot, _))) = + doc_def_annot def_annot + ^^ + match pexp with + | Pat_exp (pat, exp) -> group (separate space [doc_id id; doc_pat pat; equals; doc_exp_as_block 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_as_block exp; + ] + ) + + let doc_default (DT_aux (DT_order ord, _)) = separate space [string "default"; string "Order"; doc_ord ord] + + let doc_rec (Rec_aux (r, _)) = + match r with + | Rec_nonrec | Rec_rec -> empty + | Rec_measure (pat, exp) -> braces (doc_pat pat ^^ string " => " ^^ doc_exp exp) ^^ space + + let doc_fundef (FD_aux (FD_function (r, _, funcls), _)) = + match funcls with + | [] -> failwith "Empty function list" + | _ -> + let rec_pp = doc_rec r in + let sep = hardline ^^ string "and" ^^ space in + let clauses = separate_map sep doc_funcl funcls in + string "function" ^^ space ^^ rec_pp ^^ clauses + + let rec doc_mpat (MP_aux (mp_aux, _) as mpat) = + match mp_aux with + | MP_id id -> doc_id id + | MP_tuple pats -> lparen ^^ separate_map (comma ^^ space) doc_mpat pats ^^ rparen + | MP_lit lit -> doc_lit lit + | MP_vector pats -> brackets (separate_map (comma ^^ space) doc_mpat pats) + | MP_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_mpat pats + | MP_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_mpat pats) + | MP_list pats -> string "[|" ^^ separate_map (comma ^^ space) doc_mpat pats ^^ string "|]" + | _ -> string (string_of_mpat mpat) + + let doc_mpexp (MPat_aux (mpexp, _)) = + match mpexp with + | MPat_pat mpat -> doc_mpat mpat + | MPat_when (mpat, guard) -> doc_mpat mpat ^^ space ^^ string "if" ^^ space ^^ doc_exp guard + + let doc_mapcl (MCL_aux (cl, (def_annot, _))) = + doc_def_annot def_annot + ^^ + match cl with + | MCL_bidir (mpexp1, mpexp2) -> + let left = doc_mpexp mpexp1 in + let right = doc_mpexp mpexp2 in + separate space [left; string "<->"; right] + | MCL_forwards pexp -> string "forwards" ^^ space ^^ doc_pexp pexp + | MCL_backwards pexp -> string "backwards" ^^ space ^^ doc_pexp pexp + + let doc_mapdef (MD_aux (MD_mapping (id, _, mapcls), _)) = + match mapcls with + | [] -> failwith "Empty mapping" + | _ -> + let sep = string "," ^^ hardline in + let clauses = separate_map sep doc_mapcl mapcls in + string "mapping" ^^ space ^^ doc_id id ^^ space ^^ string "=" ^^ space ^^ surround 2 0 lbrace clauses rbrace + + let doc_dec (DEC_aux (reg, _)) = + match reg with + | DEC_reg (typ, id, opt_exp) -> ( + match opt_exp with + | None -> separate space [string "register"; doc_id id; colon; doc_typ typ] + | Some exp -> separate space [string "register"; doc_id id; colon; doc_typ typ; equals; doc_exp exp] + ) + + let doc_field (typ, id) = separate space [doc_id id; colon; doc_typ typ] + + let doc_union (Tu_aux (Tu_ty_id (typ, id), def_annot)) = + doc_def_annot def_annot ^^ separate space [doc_id id; colon; doc_typ typ] + + let rec doc_index_range (BF_aux (ir, _)) = + match ir with + | BF_single i -> doc_nexp i + | BF_range (i, j) -> doc_nexp i ^^ string ".." ^^ doc_nexp j + | BF_concat (i, j) -> parens (doc_index_range i ^^ space ^^ at ^^ space ^^ doc_index_range j) + + let doc_typ_arg_kind sep (A_aux (aux, _)) = + match aux with + | A_nexp _ -> space ^^ string sep ^^ space ^^ string "Int" + | A_bool _ -> space ^^ string sep ^^ space ^^ string "Bool" + | A_typ _ -> empty + + let doc_typdef (TD_aux (td, _)) = + match td with + | TD_abstract (id, kind) -> begin doc_op colon (concat [string "type"; space; doc_id id]) (doc_kind kind) end + | TD_abbrev (id, typq, typ_arg) -> begin + match doc_typquant typq with + | Some qdoc -> + doc_op equals + (concat [string "type"; space; doc_id id; qdoc; doc_typ_arg_kind "->" typ_arg]) + (doc_typ_arg typ_arg) + | None -> + doc_op equals (concat [string "type"; space; doc_id id; doc_typ_arg_kind ":" typ_arg]) (doc_typ_arg typ_arg) + 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_param_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_param_quants qs; + equals; + surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace; + ] + | TD_bitfield (id, typ, fields) -> + let doc_field (id, range) = separate space [doc_id id; colon; doc_index_range range] in + doc_op equals + (separate space [string "bitfield"; doc_id id; colon; doc_typ typ]) + (surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace) + + let doc_spec = + let doc_extern ext = + match ext with + | Some ext -> + let purity = if ext.pure then string "pure" ^^ space else string "monadic" ^^ space in + let docs = + List.map + (fun (backend, rep) -> string (backend ^ ":") ^^ space ^^ utf8string ("\"" ^ String.escaped rep ^ "\"")) + ext.bindings + in + equals ^^ space ^^ purity ^^ braces (separate (comma ^^ space) docs) + | None -> empty + in + function + | VS_aux (VS_val_spec (ts, id, ext), _) -> + string "val" ^^ space ^^ 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_loop_measures l = + separate_map + (comma ^^ break 1) + (function Loop (l, e) -> string (match l with While -> "while" | Until -> "until") ^^ space ^^ doc_exp e) + l + + let doc_scattered (SD_aux (sd_aux, _)) = + match sd_aux with + | SD_function (_, _, id) -> string "scattered" ^^ space ^^ string "function" ^^ space ^^ doc_id id + | SD_funcl funcl -> string "function" ^^ space ^^ string "clause" ^^ space ^^ doc_funcl funcl + | SD_end id -> string "end" ^^ space ^^ doc_id id + | SD_variant (id, TypQ_aux (TypQ_no_forall, _)) -> + string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id + | SD_variant (id, TypQ_aux (TypQ_tq quants, _)) -> + string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id ^^ doc_param_quants quants + | SD_mapcl (id, mapcl) -> separate space [string "mapping clause"; doc_id id; equals; doc_mapcl mapcl] + | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_none, _)) -> + separate space [string "scattered mapping"; doc_id id] + | SD_mapping (id, Typ_annot_opt_aux (Typ_annot_opt_some (typq, typ), _)) -> + separate space [string "scattered mapping"; doc_id id; colon; doc_binding (typq, typ)] + | SD_unioncl (id, tu) -> separate space [string "union clause"; doc_id id; equals; doc_union tu] + | SD_internal_unioncl_record (id, record_id, typq, fields) -> + let prefix = separate space [string "internal_union_record clause"; doc_id id; doc_id record_id] in + let params = + match typq with + | TypQ_aux (TypQ_no_forall, _) | TypQ_aux (TypQ_tq [], _) -> empty + | TypQ_aux (TypQ_tq qs, _) -> doc_param_quants qs + in + separate space + [prefix ^^ params; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] + | SD_enum id -> separate space [string "scattered enum"; doc_id id] + | SD_enumcl (id, member) -> separate space [string "enum clause"; doc_id id; equals; doc_id member] + + let doc_filter = function + | DEF_aux ((DEF_pragma ("file_start", _, _) | DEF_pragma ("file_end", _, _)), _) -> false + | _ -> true + + let rec doc_def_no_hardline (DEF_aux (aux, def_annot)) = + doc_def_annot def_annot + ^^ + match aux with + | DEF_default df -> doc_default df + | DEF_val v_spec -> doc_spec v_spec + | DEF_type t_def -> doc_typdef t_def + | DEF_fundef f_def -> doc_fundef f_def + | DEF_mapdef m_def -> doc_mapdef m_def + | DEF_constraint nc -> string "constraint" ^^ space ^^ doc_nc nc + | DEF_outcome (OV_aux (OV_outcome (id, typschm, args), _), defs) -> ( + string "outcome" ^^ space ^^ doc_id id ^^ space ^^ colon ^^ space ^^ doc_typschm typschm ^^ break 1 + ^^ (string "with" ^//^ separate_map (comma ^^ break 1) doc_kopt_no_parens args) + ^^ + match defs with + | [] -> empty + | _ -> + break 1 ^^ (string "= {" ^//^ separate_map (hardline ^^ hardline) doc_def_no_hardline defs) ^/^ string "}" + ) + | DEF_instantiation (IN_aux (IN_id id, _), substs) -> ( + string "instantiation" ^^ space ^^ doc_id id + ^^ + match substs with + | [] -> empty + | _ -> (space ^^ string "with") ^//^ separate_map (comma ^^ break 1) doc_subst substs + ) + | DEF_impl funcl -> string "impl" ^^ space ^^ doc_funcl funcl + | DEF_let lbind -> string "let" ^^ space ^^ doc_letbind lbind + | DEF_internal_mutrec fundefs -> + (string "mutual {" ^//^ separate_map (hardline ^^ hardline) doc_fundef fundefs) ^^ hardline ^^ string "}" + | DEF_register dec -> doc_dec dec + | DEF_scattered sdef -> doc_scattered sdef + | DEF_measure (id, pat, exp) -> + string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_pat pat ^^ space ^^ equals ^/^ doc_exp exp + | DEF_loop_measures (id, measures) -> + string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_loop_measures measures + | DEF_pragma (pragma, arg, _) -> string ("$" ^ pragma ^ " " ^ arg) + | 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) -> + separate space + [ + string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace; + ] + + and doc_def def = group (doc_def_no_hardline def ^^ hardline) + + let doc_ast { defs; _ } = separate_map hardline doc_def (List.filter doc_filter defs) +end (* This function is intended to reformat machine-generated Sail into something a bit more readable, it is not intended to be used as a general purpose formatter *) let reformat dir { defs; _ } = + let module Reformatter = Printer (struct + let insert_braces = true + let resugar = true + end) in let file_stack = ref [] in let pop () = @@ -853,7 +909,7 @@ let reformat dir { defs; _ } = let output_def def = match !file_stack with - | Some chan :: _ -> ToChannel.pretty 1. 120 chan (hardline ^^ doc_def def) + | Some chan :: _ -> ToChannel.pretty 1. 120 chan (hardline ^^ Reformatter.doc_def def) | None :: _ -> () | [] -> Reporting.unreachable Parse_ast.Unknown __POS__ "No file for definition" in @@ -877,9 +933,14 @@ let reformat dir { defs; _ } = | def -> output_def def in - opt_insert_braces := true; - List.iter format_def defs; - opt_insert_braces := false + List.iter format_def defs + +module Default_print_config : PRINT_CONFIG = struct + let insert_braces = false + let resugar = false +end + +include Printer (Default_print_config) let pp_ast f d = ToChannel.pretty 1. 80 f (doc_ast d) diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index b9c5dfcd7..9b9a364ca 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -2957,7 +2957,12 @@ and bind_assignment assign_l env (LE_aux (lexp_aux, (lexp_l, uannot)) as lexp) e in let has_typ v env = match Env.lookup_id v env with Local (Mutable, _) | Register _ -> true | _ -> false in match lexp_aux with - | LE_app (f, xs) -> (check_exp env (E_aux (E_app (f, xs @ [exp]), (lexp_l, uannot))) unit_typ, env) + | LE_app (f, xs) -> + ( check_exp env + (E_aux (E_app (f, xs @ [exp]), (lexp_l, add_attribute (gen_loc lexp_l) "setter" None uannot))) + unit_typ, + env + ) | LE_typ (typ_annot, _) -> Env.wf_typ ~at:lexp_l env typ_annot; let checked_exp = crule check_exp env exp typ_annot in diff --git a/src/lib/util.ml b/src/lib/util.ml index f7005bdf6..367f4be0a 100644 --- a/src/lib/util.ml +++ b/src/lib/util.ml @@ -120,6 +120,11 @@ let rec last_opt = function [x] -> Some x | _ :: xs -> last_opt xs | [] -> None let rec butlast = function [_] -> [] | x :: xs -> x :: butlast xs | [] -> [] +module Option_monad = struct + let ( let* ) = Option.bind + let ( let+ ) = Option.map +end + module Duplicate (S : Set.S) = struct type dups = No_dups of S.t | Has_dups of S.elt diff --git a/src/lib/util.mli b/src/lib/util.mli index da7cffea2..8e3eb7318 100644 --- a/src/lib/util.mli +++ b/src/lib/util.mli @@ -77,6 +77,11 @@ val last_opt : 'a list -> 'a option val butlast : 'a list -> 'a list +module Option_monad : sig + val ( let* ) : 'a option -> ('a -> 'b option) -> 'b option + val ( let+ ) : ('a -> 'b) -> 'a option -> 'b option +end + (** Mixed useful things *) module Duplicate (S : Set.S) : sig type dups = No_dups of S.t | Has_dups of S.elt diff --git a/src/sail_doc_backend/docinfo.ml b/src/sail_doc_backend/docinfo.ml index 83a04c4dc..3ba72797f 100644 --- a/src/sail_doc_backend/docinfo.ml +++ b/src/sail_doc_backend/docinfo.ml @@ -77,6 +77,11 @@ open Ast_defs open Ast_util open Parse_ast.Attribute_data +module Reformatter = Pretty_print_sail.Printer (struct + let insert_braces = true + let resugar = true +end) + (** In the case of latex, we generate files containing a sequence of commands that can simply be included. For other documentation targets with tooling that may consume the json output however, we @@ -94,13 +99,23 @@ type embedding = Plain | Base64 let embedding_string = function Plain -> "plain" | Base64 -> "base64" -let bindings_to_json b f = +let json_of_bindings b f = Bindings.bindings b |> List.map (fun (key, elem) -> (string_of_id key, f elem)) |> fun elements -> `Assoc elements -type location_or_raw = Raw of string | Location of string * int * int * int * int * int * int +type location_or_raw = + | Raw of string + | RawWithLocation of string * string * int * int * int * int * int * int + | Location of string * int * int * int * int * int * int -let location_or_raw_to_json = function +let json_of_location_or_raw = function | Raw s -> `String s + | RawWithLocation (s, fname, line1, bol1, char1, line2, bol2, char2) -> + `Assoc + [ + ("contents", `String s); + ("file", `String fname); + ("loc", `List [`Int line1; `Int bol1; `Int char1; `Int line2; `Int bol2; `Int char2]); + ] | Location (fname, line1, bol1, char1, line2, bol2, char2) -> `Assoc [("file", `String fname); ("loc", `List [`Int line1; `Int bol1; `Int char1; `Int line2; `Int bol2; `Int char2])] @@ -120,7 +135,7 @@ let hyper_loc l = type hyperlink = Function of id * hyper_location | Register of id * hyper_location -let hyperlink_to_json = function +let json_of_hyperlink = function | Function (id, (file, c1, c2)) -> `Assoc [ @@ -138,7 +153,7 @@ let hyperlink_to_json = function ("loc", `List [`Int c1; `Int c2]); ] -let hyperlinks_to_json = function [] -> `Null | links -> `List (List.map hyperlink_to_json links) +let json_of_hyperlinks = function [] -> `Null | links -> `List (List.map json_of_hyperlink links) let hyperlinks_from_def files def = let open Rewriter in @@ -190,18 +205,22 @@ let hyperlinks_from_def files def = !links -let rec pat_to_json (P_aux (aux, _)) = +let json_of_attributes = function + | [] -> [] + | attrs -> [("attributes", `List (List.map (fun (attr, data) -> json_of_attribute attr data) attrs))] + +let rec json_of_pat (P_aux (aux, _)) = let pat_type t = ("type", `String t) in - let seq_pat_json t pats = `Assoc [pat_type t; ("patterns", `List (List.map pat_to_json pats))] in + let seq_pat_json t pats = `Assoc [pat_type t; ("patterns", `List (List.map json_of_pat pats))] in match aux with | P_lit lit -> `Assoc [pat_type "literal"; ("value", `String (string_of_lit lit))] | P_wild -> `Assoc [pat_type "wildcard"] - | P_as (pat, id) -> `Assoc [pat_type "as"; ("pattern", pat_to_json pat); ("id", `String (string_of_id id))] - | P_typ (_, pat) -> pat_to_json pat + | P_as (pat, id) -> `Assoc [pat_type "as"; ("pattern", json_of_pat pat); ("id", `String (string_of_id id))] + | P_typ (_, pat) -> json_of_pat pat | P_id id -> `Assoc [pat_type "id"; ("id", `String (string_of_id id))] - | P_var (pat, _) -> `Assoc [pat_type "var"; ("pattern", pat_to_json pat)] + | P_var (pat, _) -> `Assoc [pat_type "var"; ("pattern", json_of_pat pat)] | P_app (id, pats) -> - `Assoc [pat_type "app"; ("id", `String (string_of_id id)); ("patterns", `List (List.map pat_to_json pats))] + `Assoc [pat_type "app"; ("id", `String (string_of_id id)); ("patterns", `List (List.map json_of_pat pats))] | P_vector pats -> seq_pat_json "vector" pats | P_vector_concat pats -> seq_pat_json "vector_concat" pats | P_vector_subrange (id, n, m) -> @@ -214,13 +233,13 @@ let rec pat_to_json (P_aux (aux, _)) = ] | P_tuple pats -> seq_pat_json "tuple" pats | P_list pats -> seq_pat_json "list" pats - | P_cons (pat_hd, pat_tl) -> `Assoc [pat_type "cons"; ("hd", pat_to_json pat_hd); ("tl", pat_to_json pat_tl)] + | P_cons (pat_hd, pat_tl) -> `Assoc [pat_type "cons"; ("hd", json_of_pat pat_hd); ("tl", json_of_pat pat_tl)] | P_string_append pats -> seq_pat_json "string_append" pats | P_struct (fpats, fwild) -> `Assoc [ pat_type "struct"; - ("fields", `Assoc (List.map (fun (field, pat) -> (string_of_id field, pat_to_json pat)) fpats)); + ("fields", `Assoc (List.map (fun (field, pat) -> (string_of_id field, json_of_pat pat)) fpats)); ("wildcard", `Bool (match fwild with FP_wild _ -> true | FP_no_wild -> false)); ] | P_or _ | P_not _ -> `Null @@ -234,27 +253,29 @@ type 'a function_clause_doc = { body_source : location_or_raw; comment : string option; splits : location_or_raw Bindings.t option; + attributes : (string * attribute_data option) list; } -let function_clause_doc_to_json docinfo = +let json_of_function_clause_doc docinfo = `Assoc ([ ("number", `Int docinfo.number); - ("source", location_or_raw_to_json docinfo.source); - ("pattern", pat_to_json docinfo.pat); + ("source", json_of_location_or_raw docinfo.source); + ("pattern", json_of_pat docinfo.pat); ] @ (match docinfo.wavedrom with Some w -> [("wavedrom", `String w)] | None -> []) @ (match docinfo.comment with Some s -> [("comment", `String s)] | None -> []) - @ (match docinfo.guard_source with Some s -> [("guard", location_or_raw_to_json s)] | None -> []) - @ [("body", location_or_raw_to_json docinfo.body_source)] - @ match docinfo.splits with Some s -> [("splits", bindings_to_json s location_or_raw_to_json)] | None -> [] + @ (match docinfo.guard_source with Some s -> [("guard", json_of_location_or_raw s)] | None -> []) + @ [("body", json_of_location_or_raw docinfo.body_source)] + @ (match docinfo.splits with Some s -> [("splits", json_of_bindings s json_of_location_or_raw)] | None -> []) + @ json_of_attributes docinfo.attributes ) type 'a function_doc = Multiple_clauses of 'a function_clause_doc list | Single_clause of 'a function_clause_doc -let function_doc_to_json = function - | Multiple_clauses docinfos -> `List (List.map function_clause_doc_to_json docinfos) - | Single_clause docinfo -> function_clause_doc_to_json docinfo +let json_of_function_doc = function + | Multiple_clauses docinfos -> `List (List.map json_of_function_clause_doc docinfos) + | Single_clause docinfo -> json_of_function_clause_doc docinfo type 'a mapping_clause_doc = { number : int; @@ -264,45 +285,67 @@ type 'a mapping_clause_doc = { right : 'a pat option; right_wavedrom : string option; body : location_or_raw option; + attributes : (string * attribute_data option) list; } -let mapping_clause_doc_to_json docinfo = +let json_of_mapping_clause_doc docinfo = `Assoc - ([("number", `Int docinfo.number); ("source", location_or_raw_to_json docinfo.source)] - @ (match docinfo.left with Some p -> [("left", pat_to_json p)] | None -> []) + ([("number", `Int docinfo.number); ("source", json_of_location_or_raw docinfo.source)] + @ (match docinfo.left with Some p -> [("left", json_of_pat p)] | None -> []) @ (match docinfo.left_wavedrom with Some w -> [("left_wavedrom", `String w)] | None -> []) - @ (match docinfo.right with Some p -> [("right", pat_to_json p)] | None -> []) + @ (match docinfo.right with Some p -> [("right", json_of_pat p)] | None -> []) @ (match docinfo.right_wavedrom with Some w -> [("right_wavedrom", `String w)] | None -> []) - @ match docinfo.body with Some s -> [("body", location_or_raw_to_json s)] | None -> [] + @ (match docinfo.body with Some s -> [("body", json_of_location_or_raw s)] | None -> []) + @ json_of_attributes docinfo.attributes ) type 'a mapping_doc = 'a mapping_clause_doc list -let mapping_doc_to_json docinfos = `List (List.map mapping_clause_doc_to_json docinfos) +let json_of_mapping_doc docinfos = `List (List.map json_of_mapping_clause_doc docinfos) -type valspec_doc = { source : location_or_raw; type_source : location_or_raw } +type valspec_doc = { + source : location_or_raw; + type_source : location_or_raw; + attributes : (string * attribute_data option) list; +} -let valspec_doc_to_json docinfo = - `Assoc [("source", location_or_raw_to_json docinfo.source); ("type", location_or_raw_to_json docinfo.type_source)] +let json_of_valspec_doc docinfo = + `Assoc + ([("source", json_of_location_or_raw docinfo.source); ("type", json_of_location_or_raw docinfo.type_source)] + @ json_of_attributes docinfo.attributes + ) -type typdef_doc = location_or_raw +type type_def_doc = location_or_raw -let typdef_doc_to_json = location_or_raw_to_json +let json_of_type_def_doc = json_of_location_or_raw -type register_doc = { source : location_or_raw; type_source : location_or_raw; exp_source : location_or_raw option } +type register_doc = { + source : location_or_raw; + type_source : location_or_raw; + exp_source : location_or_raw option; + attributes : (string * attribute_data option) list; +} -let register_doc_to_json docinfo = +let json_of_register_doc docinfo = `Assoc - ([("source", location_or_raw_to_json docinfo.source); ("type", location_or_raw_to_json docinfo.type_source)] - @ match docinfo.exp_source with None -> [] | Some source -> [("exp", location_or_raw_to_json source)] + ([("source", json_of_location_or_raw docinfo.source); ("type", json_of_location_or_raw docinfo.type_source)] + @ (match docinfo.exp_source with None -> [] | Some source -> [("exp", json_of_location_or_raw source)]) + @ json_of_attributes docinfo.attributes ) -type let_doc = { source : location_or_raw; exp_source : location_or_raw } +type let_doc = { + source : location_or_raw; + exp_source : location_or_raw; + attributes : (string * attribute_data option) list; +} -let let_doc_to_json docinfo = - `Assoc [("source", location_or_raw_to_json docinfo.source); ("exp", location_or_raw_to_json docinfo.exp_source)] +let json_of_let_doc docinfo = + `Assoc + ([("source", json_of_location_or_raw docinfo.source); ("exp", json_of_location_or_raw docinfo.exp_source)] + @ json_of_attributes docinfo.attributes + ) -let pair_to_json x_label f y_label g (x, y) = +let json_of_pair x_label f y_label g (x, y) = match (f x, g y) with | `Null, `Null -> `Null | x, `Null -> `Assoc [(x_label, x)] @@ -311,9 +354,9 @@ let pair_to_json x_label f y_label g (x, y) = type anchor_doc = { source : location_or_raw; comment : string option } -let anchor_doc_to_json docinfo = +let json_of_anchor_doc docinfo = `Assoc - ([("source", location_or_raw_to_json docinfo.source)] + ([("source", json_of_location_or_raw docinfo.source)] @ match docinfo.comment with Some c -> [("comment", `String c)] | None -> [] ) @@ -324,16 +367,16 @@ type 'a docinfo = { functions : ('a function_doc * hyperlink list) Bindings.t; mappings : ('a mapping_doc * hyperlink list) Bindings.t; valspecs : (valspec_doc * hyperlink list) Bindings.t; - typdefs : (typdef_doc * hyperlink list) Bindings.t; + type_defs : (type_def_doc * hyperlink list) Bindings.t; registers : (register_doc * hyperlink list) Bindings.t; lets : (let_doc * hyperlink list) Bindings.t; anchors : (anchor_doc * hyperlink list) Bindings.t; spans : location_or_raw Bindings.t; } -let span_to_json loc = `Assoc [("span", location_or_raw_to_json loc)] +let json_of_span loc = `Assoc [("span", json_of_location_or_raw loc)] -let docinfo_to_json docinfo = +let json_of_docinfo docinfo = let assoc = [("version", `Int docinfo_version)] @ ( match docinfo.git with @@ -344,21 +387,23 @@ let docinfo_to_json docinfo = ("embedding", `String (embedding_string docinfo.embedding)); ("hashes", `Assoc (List.map (fun (key, hash) -> (key, `Assoc [("md5", `String hash)])) docinfo.hashes)); ( "functions", - bindings_to_json docinfo.functions (pair_to_json "function" function_doc_to_json "links" hyperlinks_to_json) + json_of_bindings docinfo.functions (json_of_pair "function" json_of_function_doc "links" json_of_hyperlinks) ); ( "mappings", - bindings_to_json docinfo.mappings (pair_to_json "mapping" mapping_doc_to_json "links" hyperlinks_to_json) + json_of_bindings docinfo.mappings (json_of_pair "mapping" json_of_mapping_doc "links" json_of_hyperlinks) + ); + ("vals", json_of_bindings docinfo.valspecs (json_of_pair "val" json_of_valspec_doc "links" json_of_hyperlinks)); + ( "types", + json_of_bindings docinfo.type_defs (json_of_pair "type" json_of_type_def_doc "links" json_of_hyperlinks) ); - ("vals", bindings_to_json docinfo.valspecs (pair_to_json "val" valspec_doc_to_json "links" hyperlinks_to_json)); - ("types", bindings_to_json docinfo.typdefs (pair_to_json "type" typdef_doc_to_json "links" hyperlinks_to_json)); ( "registers", - bindings_to_json docinfo.registers (pair_to_json "register" register_doc_to_json "links" hyperlinks_to_json) + json_of_bindings docinfo.registers (json_of_pair "register" json_of_register_doc "links" json_of_hyperlinks) ); - ("lets", bindings_to_json docinfo.lets (pair_to_json "let" let_doc_to_json "links" hyperlinks_to_json)); + ("lets", json_of_bindings docinfo.lets (json_of_pair "let" json_of_let_doc "links" json_of_hyperlinks)); ( "anchors", - bindings_to_json docinfo.anchors (pair_to_json "anchor" anchor_doc_to_json "links" hyperlinks_to_json) + json_of_bindings docinfo.anchors (json_of_pair "anchor" json_of_anchor_doc "links" json_of_hyperlinks) ); - ("spans", bindings_to_json docinfo.spans span_to_json); + ("spans", json_of_bindings docinfo.spans json_of_span); ] in `Assoc assoc @@ -372,6 +417,7 @@ let git_command args = module type CONFIG = sig val embedding_mode : embedding option + val embed_with_location : bool end module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct @@ -381,6 +427,17 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct let doc_lexing_pos (p1 : Lexing.position) (p2 : Lexing.position) = match Config.embedding_mode with + | Some _ when Config.embed_with_location -> + RawWithLocation + ( Reporting.loc_range_to_src p1 p2 |> encode, + p1.pos_fname, + p1.pos_lnum, + p1.pos_bol, + p1.pos_cnum, + p2.pos_lnum, + p2.pos_bol, + p2.pos_cnum + ) | Some _ -> Raw (Reporting.loc_range_to_src p1 p2 |> encode) | None -> Location (p1.pos_fname, p1.pos_lnum, p1.pos_bol, p1.pos_cnum, p2.pos_lnum, p2.pos_bol, p2.pos_cnum) @@ -399,35 +456,38 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct ) def_annot.doc_comment - let docinfo_for_valspec (VS_aux (VS_val_spec ((TypSchm_aux (_, ts_l) as ts), _, _), vs_annot) as vs) = + let docinfo_for_valspec def_annot (VS_aux (VS_val_spec ((TypSchm_aux (_, ts_l) as ts), _, _), vs_annot) as vs) = { - source = doc_loc (fst vs_annot) Type_check.strip_val_spec Pretty_print_sail.doc_spec vs; - type_source = doc_loc ts_l (fun ts -> ts) Pretty_print_sail.doc_typschm ts; + source = doc_loc (fst vs_annot) Type_check.strip_val_spec Reformatter.doc_spec vs; + type_source = doc_loc ts_l (fun ts -> ts) Reformatter.doc_typschm ts; + attributes = List.map (fun (_, attr, data) -> (attr, data)) def_annot.attrs; } - let docinfo_for_typdef (TD_aux (_, annot) as td) = - doc_loc (fst annot) Type_check.strip_typedef Pretty_print_sail.doc_typdef td + let docinfo_for_type_def (TD_aux (_, annot) as td) = + doc_loc (fst annot) Type_check.strip_typedef Reformatter.doc_typdef td - let docinfo_for_register (DEC_aux (DEC_reg ((Typ_aux (_, typ_l) as typ), _, exp), rd_annot) as rd) = + let docinfo_for_register def_annot (DEC_aux (DEC_reg ((Typ_aux (_, typ_l) as typ), _, exp), rd_annot) as rd) = { - source = doc_loc (fst rd_annot) Type_check.strip_register Pretty_print_sail.doc_dec rd; - type_source = doc_loc typ_l (fun typ -> typ) Pretty_print_sail.doc_typ typ; + source = doc_loc (fst rd_annot) Type_check.strip_register Reformatter.doc_dec rd; + type_source = doc_loc typ_l (fun typ -> typ) Reformatter.doc_typ typ; exp_source = - Option.map (fun (E_aux (_, (l, _)) as exp) -> doc_loc l Type_check.strip_exp Pretty_print_sail.doc_exp exp) exp; + Option.map (fun (E_aux (_, (l, _)) as exp) -> doc_loc l Type_check.strip_exp Reformatter.doc_exp exp) exp; + attributes = List.map (fun (_, attr, data) -> (attr, data)) def_annot.attrs; } - let docinfo_for_let (LB_aux (LB_val (_, exp), annot) as lbind) = + let docinfo_for_let def_annot (LB_aux (LB_val (_, exp), annot) as lbind) = { - source = doc_loc (fst annot) Type_check.strip_letbind Pretty_print_sail.doc_letbind lbind; - exp_source = doc_loc (exp_loc exp) Type_check.strip_exp Pretty_print_sail.doc_exp exp; + source = doc_loc (fst annot) Type_check.strip_letbind Reformatter.doc_letbind lbind; + exp_source = doc_loc (exp_loc exp) Type_check.strip_exp Reformatter.doc_exp exp; + attributes = List.map (fun (_, attr, data) -> (attr, data)) def_annot.attrs; } let funcl_splits ~ast ~error_loc:l attrs exp = (* The constant propagation tends to strip away block formatting, so put it back to make the pretty_printed output a bit nicer. *) let pretty_printer = match exp with - | E_aux (E_block _, _) -> fun exp -> Pretty_print_sail.doc_block [exp] - | _ -> fun exp -> Pretty_print_sail.doc_exp exp + | E_aux (E_block _, _) -> fun exp -> Reformatter.doc_block [exp] + | _ -> fun exp -> Reformatter.doc_exp exp in match find_attribute_opt "split" attrs with | None -> None @@ -466,14 +526,14 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct (* Try to use the inner attributes if we have no outer attributes. *) let attrs = match outer_annot with None -> (fst annot).attrs | Some outer -> (fst outer).attrs in - let source = doc_loc (fst annot).loc Type_check.strip_funcl Pretty_print_sail.doc_funcl clause in + let source = doc_loc (fst annot).loc Type_check.strip_funcl Reformatter.doc_funcl clause in let pat, guard, exp = match pexp with | Pat_aux (Pat_exp (pat, exp), _) -> (pat, None, exp) | Pat_aux (Pat_when (pat, guard, exp), _) -> (pat, Some guard, exp) in let guard_source = - Option.map (fun exp -> doc_loc (exp_loc exp) Type_check.strip_exp Pretty_print_sail.doc_exp exp) guard + Option.map (fun exp -> doc_loc (exp_loc exp) Type_check.strip_exp Reformatter.doc_exp exp) guard in let body_source = match exp with @@ -487,9 +547,9 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct doc_lexing_pos { p1 with pos_cnum = p1.pos_bol } p2 | _, _ -> let block = Type_check.strip_exp exp :: List.map Type_check.strip_exp exps in - Raw (Pretty_print_sail.doc_block block |> Pretty_print_sail.to_string |> encode) + Raw (Reformatter.doc_block block |> Pretty_print_sail.to_string |> encode) end - | _ -> doc_loc (exp_loc exp) Type_check.strip_exp Pretty_print_sail.doc_exp exp + | _ -> doc_loc (exp_loc exp) Type_check.strip_exp Reformatter.doc_exp exp in let splits = funcl_splits ~ast ~error_loc:(pat_loc pat) attrs exp in @@ -503,6 +563,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct body_source; comment = Option.map encode comment; splits; + attributes = List.map (fun (_, attr, data) -> (attr, data)) attrs; } let included_clause files (FCL_aux (_, (clause_annot, _))) = included_loc files clause_annot.loc @@ -521,7 +582,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct match aux with Pat_exp (pat, body) -> (pat, body) | Pat_when (pat, _, body) -> (pat, body) let docinfo_for_mapcl n (MCL_aux (aux, (def_annot, _)) as clause) = - let source = doc_loc def_annot.loc Type_check.strip_mapcl Pretty_print_sail.doc_mapcl clause in + let source = doc_loc def_annot.loc Type_check.strip_mapcl Reformatter.doc_mapcl clause in let parse_wavedrom_attr = function Some (AD_aux (AD_string s, _)) -> Some s | Some _ | None -> None in let wavedrom_attr = Option.bind (find_attribute_opt "wavedrom" def_annot.attrs) parse_wavedrom_attr in @@ -536,12 +597,12 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct | MCL_forwards pexp -> let left, body = docinfo_for_pexp pexp in let left_wavedrom = Wavedrom.of_pattern ~labels:wavedrom_attr left in - let body = doc_loc (exp_loc body) Type_check.strip_exp Pretty_print_sail.doc_exp body in + let body = doc_loc (exp_loc body) Type_check.strip_exp Reformatter.doc_exp body in (Some left, left_wavedrom, None, None, Some body) | MCL_backwards pexp -> let right, body = docinfo_for_pexp pexp in let right_wavedrom = Wavedrom.of_pattern ~labels:wavedrom_attr right in - let body = doc_loc (exp_loc body) Type_check.strip_exp Pretty_print_sail.doc_exp body in + let body = doc_loc (exp_loc body) Type_check.strip_exp Reformatter.doc_exp body in (None, None, Some right, right_wavedrom, Some body) in @@ -553,6 +614,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct right; right_wavedrom = Option.map encode right_wavedrom; body; + attributes = List.map (fun (_, attr, data) -> (attr, data)) def_annot.attrs; } let included_mapping_clause files (MCL_aux (_, (def_annot, _))) = included_loc files def_annot.loc @@ -575,7 +637,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct functions = Bindings.empty; mappings = Bindings.empty; valspecs = Bindings.empty; - typdefs = Bindings.empty; + type_defs = Bindings.empty; registers = Bindings.empty; lets = Bindings.empty; anchors = Bindings.empty; @@ -615,17 +677,21 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct | _ when skipping skips -> (docinfo, skips) | DEF_val vs -> let id = id_of_val_spec vs in - ({ docinfo with valspecs = Bindings.add id (docinfo_for_valspec vs, links) docinfo.valspecs }, skips) + ({ docinfo with valspecs = Bindings.add id (docinfo_for_valspec def_annot vs, links) docinfo.valspecs }, skips) | DEF_type td -> let id = id_of_type_def td in - ({ docinfo with typdefs = Bindings.add id (docinfo_for_typdef td, links) docinfo.typdefs }, skips) + ({ docinfo with type_defs = Bindings.add id (docinfo_for_type_def td, links) docinfo.type_defs }, skips) | DEF_register rd -> let id = id_of_dec_spec rd in - ({ docinfo with registers = Bindings.add id (docinfo_for_register rd, links) docinfo.registers }, skips) + ( { docinfo with registers = Bindings.add id (docinfo_for_register def_annot rd, links) docinfo.registers }, + skips + ) | DEF_let (LB_aux (LB_val (pat, _), _) as letbind) -> let ids = pat_ids pat in ( IdSet.fold - (fun id docinfo -> { docinfo with lets = Bindings.add id (docinfo_for_let letbind, links) docinfo.lets }) + (fun id docinfo -> + { docinfo with lets = Bindings.add id (docinfo_for_let def_annot letbind, links) docinfo.lets } + ) ids docinfo, skips ) @@ -642,10 +708,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct | DEF_pragma ("anchor", arg, _) -> let links = hyperlinks files def in let anchor_info = - { - source = doc_loc l Type_check.strip_def Pretty_print_sail.doc_def def; - comment = def_annot.doc_comment; - } + { source = doc_loc l Type_check.strip_def Reformatter.doc_def def; comment = def_annot.doc_comment } in anchored := Bindings.add (mk_id arg) (anchor_info, links) !anchored | _ -> () diff --git a/src/sail_doc_backend/docinfo.mli b/src/sail_doc_backend/docinfo.mli index e137ed931..7bf4a1e4c 100644 --- a/src/sail_doc_backend/docinfo.mli +++ b/src/sail_doc_backend/docinfo.mli @@ -77,12 +77,20 @@ type 'a docinfo val hyperlinks_from_def : string list -> Type_check.tannot def -> hyperlink list -val docinfo_to_json : 'a docinfo -> Yojson.t +val json_of_hyperlink : hyperlink -> Yojson.Basic.t + +val json_of_docinfo : 'a docinfo -> Yojson.Basic.t type embedding = Plain | Base64 module type CONFIG = sig + (** If [Some] then the source code will be directly included in the + documentation info. *) val embedding_mode : embedding option + + (** If true, then we include both the source directly and a + reference using the location information. *) + val embed_with_location : bool end module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) : sig diff --git a/src/sail_doc_backend/sail_plugin_doc.ml b/src/sail_doc_backend/sail_plugin_doc.ml index defebc746..cefe20b21 100644 --- a/src/sail_doc_backend/sail_plugin_doc.ml +++ b/src/sail_doc_backend/sail_plugin_doc.ml @@ -70,6 +70,7 @@ open Libsail let opt_doc_format = ref "asciidoc" let opt_doc_files = ref [] let opt_doc_embed = ref None +let opt_doc_embed_with_location = ref false let opt_doc_compact = ref false let opt_doc_bundle = ref "doc.json" @@ -96,14 +97,19 @@ let doc_options = Arg.String (fun format -> opt_doc_embed := Some format), " Embed all documentation contents into the documentation bundle rather than referencing it" ); + ( "-doc_embed_with_location", + Arg.Set opt_doc_embed_with_location, + " When used with --doc-embed, include both the contents and locations" + ); ("-doc_compact", Arg.Unit (fun _ -> opt_doc_compact := true), " Use compact documentation format"); ("-doc_bundle", Arg.String (fun file -> opt_doc_bundle := file), " Name for documentation bundle file"); ] let output_docinfo doc_dir docinfo = let chan = open_out (Filename.concat doc_dir !opt_doc_bundle) in - let json = Docinfo.docinfo_to_json docinfo in - if !opt_doc_compact then Yojson.to_channel ~std:true chan json else Yojson.pretty_to_channel ~std:true chan json; + let json = Docinfo.json_of_docinfo docinfo in + if !opt_doc_compact then Yojson.Basic.to_channel ~std:true chan json + else Yojson.Basic.pretty_to_channel ~std:true chan json; output_char chan '\n'; close_out chan @@ -121,6 +127,7 @@ let doc_target _ _ out_file ast _ _ = if !opt_doc_format = "asciidoc" || !opt_doc_format = "adoc" then let module Config = struct let embedding_mode = embedding_option () + let embed_with_location = !opt_doc_embed_with_location end in let module Gen = Docinfo.Generator (Markdown.AsciidocConverter) (Config) in let docinfo = Gen.docinfo_for_ast ~files:!opt_doc_files ~hyperlinks:Docinfo.hyperlinks_from_def ast in @@ -128,6 +135,7 @@ let doc_target _ _ out_file ast _ _ = else if !opt_doc_format = "identity" then let module Config = struct let embedding_mode = embedding_option () + let embed_with_location = !opt_doc_embed_with_location end in let module Gen = Docinfo.Generator (Markdown.IdentityConverter) (Config) in let docinfo = Gen.docinfo_for_ast ~files:!opt_doc_files ~hyperlinks:Docinfo.hyperlinks_from_def ast in diff --git a/src/sail_latex_backend/latex.ml b/src/sail_latex_backend/latex.ml index 4680278b0..64eaa7886 100644 --- a/src/sail_latex_backend/latex.ml +++ b/src/sail_latex_backend/latex.ml @@ -388,7 +388,7 @@ let latex_loc ?(docstring = empty) no_loc l = | None -> docstring ^^ no_loc let doc_spec_simple (VS_aux (VS_val_spec (ts, id, ext), _)) = - Pretty_print_sail.doc_id id ^^ space ^^ colon ^^ space ^^ Pretty_print_sail.doc_typschm ~simple:true ts + Pretty_print_sail.doc_id id ^^ space ^^ colon ^^ space ^^ Pretty_print_sail.doc_typschm ts let latex_command ~docstring cat id no_loc l = state.this <- Some id;