diff options
Diffstat (limited to 'src/pretty_print_common.ml')
| -rw-r--r-- | src/pretty_print_common.ml | 37 |
1 files changed, 28 insertions, 9 deletions
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index 973797fb..bad03034 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -49,11 +49,13 @@ (**************************************************************************) open Ast +open Big_int open PPrint let pipe = string "|" let arrow = string "->" let dotdot = string ".." +let coloncolon = string "::" let coloneq = string ":=" let lsquarebar = string "[|" let rsquarebar = string "|]" @@ -74,7 +76,7 @@ let comma_sp = comma ^^ space let colon_sp = spaces colon let doc_var (Kid_aux(Var v,_)) = string v -let doc_int i = string (string_of_int i) +let doc_int i = string (string_of_big_int i) let doc_op symb a b = infix 2 1 symb a b let doc_unop symb a = prefix 2 1 symb a @@ -119,7 +121,7 @@ let doc_ord (Ord_aux(o,_)) = match o with | Ord_inc -> string "inc" | Ord_dec -> string "dec" -let doc_typ, doc_atomic_typ, doc_nexp = +let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = (* following the structure of parser for precedence *) let rec typ ty = fn_typ ty and fn_typ ((Typ_aux (t, _)) as ty) = match t with @@ -127,12 +129,15 @@ let doc_typ, doc_atomic_typ, doc_nexp = separate space [tup_typ arg; arrow; fn_typ ret; string "effect"; doc_effects efct] | _ -> tup_typ ty and tup_typ ((Typ_aux (t, _)) as ty) = match t with + | Typ_exist (kids, nc, ty) -> + separate space [string "exist"; separate_map space doc_var kids ^^ comma; nexp_constraint nc ^^ dot; typ ty] | Typ_tup typs -> parens (separate_map comma_sp app_typ typs) | _ -> app_typ ty and app_typ ((Typ_aux (t, _)) as ty) = match t with (*TODO Need to un bid-endian-ify this here, since both can transform to the shorthand, especially with <: and :> *) (* Special case simple vectors to improve legibility * XXX we assume big-endian here, as usual *) +(* | Typ_app(Id_aux (Id "vector", _), [ Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _); Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _); @@ -167,10 +172,11 @@ let doc_typ, doc_atomic_typ, doc_nexp = Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _); Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) -> (doc_id id) ^^ (brackets (if n' = m_nexp then nexp m_nexp else doc_op colon (nexp m_nexp) (nexp n_n))) + *) | Typ_app(Id_aux (Id "range", _), [ Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _); Typ_arg_aux(Typ_arg_nexp m, _);]) -> - (squarebars (if n = 0 then nexp m else doc_op colon (doc_int n) (nexp m))) + (squarebars (if eq_big_int n zero_big_int then nexp m else doc_op colon (doc_int n) (nexp m))) | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> (squarecolons (nexp n)) | Typ_app(id,args) -> @@ -180,7 +186,6 @@ let doc_typ, doc_atomic_typ, doc_nexp = and atomic_typ ((Typ_aux (t, _)) as ty) = match t with | Typ_id id -> doc_id id | Typ_var v -> doc_var v - | Typ_wild -> underscore | Typ_app _ | Typ_tup _ | Typ_fn _ -> (* exhaustiveness matters here to avoid infinite loops * if we add a new Typ constructor *) @@ -192,7 +197,6 @@ let doc_typ, doc_atomic_typ, doc_nexp = | Typ_arg_typ t -> app_typ t | Typ_arg_nexp n -> nexp n | Typ_arg_order o -> doc_ord o - | Typ_arg_effect e -> doc_effects e (* same trick to handle precedence of nexp *) and nexp ne = sum_typ ne @@ -215,13 +219,28 @@ let doc_typ, doc_atomic_typ, doc_nexp = | _ -> atomic_nexp_typ ne and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_var v -> doc_var v - | Nexp_id i -> doc_id i - | Nexp_constant i -> doc_int i + | Nexp_id i -> braces (doc_id i) + | Nexp_constant i -> if lt_big_int i zero_big_int then parens(doc_int i) else doc_int i | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _-> group (parens (nexp ne)) - (* expose doc_typ, doc_atomic_typ and doc_nexp *) - in typ, atomic_typ, nexp + and nexp_constraint (NC_aux(nc,_)) = match nc with + | NC_equal(n1,n2) -> doc_op equals (nexp n1) (nexp n2) + | NC_not_equal (n1, n2) -> doc_op (string "!=") (nexp n1) (nexp n2) + | NC_bounded_ge(n1,n2) -> doc_op (string ">=") (nexp n1) (nexp n2) + | NC_bounded_le(n1,n2) -> doc_op (string "<=") (nexp n1) (nexp n2) + | NC_set(v,bounds) -> + doc_op (string "IN") (doc_var v) + (braces (separate_map comma_sp doc_int bounds)) + | NC_or (nc1, nc2) -> + parens (separate space [nexp_constraint nc1; string "|"; nexp_constraint nc2]) + | NC_and (nc1, nc2) -> + separate space [nexp_constraint nc1; string "&"; nexp_constraint nc2] + | NC_true -> string "true" + | NC_false -> string "false" + + (* expose doc_typ, doc_atomic_typ, doc_nexp and doc_nexp_constraint *) + in typ, atomic_typ, nexp, nexp_constraint let pp_format_id (Id_aux(i,_)) = match i with |