diff options
Diffstat (limited to 'src/pretty_print_common.ml')
| -rw-r--r-- | src/pretty_print_common.ml | 23 |
1 files changed, 20 insertions, 3 deletions
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index 39c5d97d..bd43c1a7 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -112,7 +112,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 @@ -120,6 +120,8 @@ 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 @@ -215,8 +217,23 @@ let doc_typ, doc_atomic_typ, doc_nexp = | 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, atomic_nexp_typ + and nexp_constraint (NC_aux(nc,_)) = match nc with + | NC_fixed(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_nat_set_bounded(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 |