summaryrefslogtreecommitdiff
path: root/src/pretty_print_sail.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-07-27 01:35:34 +0100
committerAlasdair Armstrong2017-07-27 01:35:34 +0100
commitac5587fb00cb7c3a14731b3d952ca7dedd7e4d3b (patch)
treec346017361982bfa45ff7f70c8b96caec9344845 /src/pretty_print_sail.ml
parente4d85d005f87f3260bddcd030e2a7e4957c1379c (diff)
Fixed pretty printer for existentials
Also fixed substitution functions so as to not substitute captured kind identifiers
Diffstat (limited to 'src/pretty_print_sail.ml')
-rw-r--r--src/pretty_print_sail.ml13
1 files changed, 0 insertions, 13 deletions
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 668e791c..e3aeaa40 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -58,19 +58,6 @@ let doc_bkind (BK_aux(k,_)) =
let doc_kind (K_aux(K_kind(klst),_)) =
separate_map (spaces arrow) doc_bkind klst
-let rec doc_nexp_constraint (NC_aux(nc,_)) = match nc with
- | NC_fixed(n1,n2) -> doc_op equals (doc_nexp n1) (doc_nexp n2)
- | NC_not_equal (n1, n2) -> doc_op (string "!=") (doc_nexp n1) (doc_nexp n2)
- | NC_bounded_ge(n1,n2) -> doc_op (string ">=") (doc_nexp n1) (doc_nexp n2)
- | NC_bounded_le(n1,n2) -> doc_op (string "<=") (doc_nexp n1) (doc_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 [doc_nexp_constraint nc1; string "|"; doc_nexp_constraint nc2])
- | NC_and (nc1, nc2) ->
- separate space [doc_nexp_constraint nc1; string "&"; doc_nexp_constraint nc2]
-
let doc_qi (QI_aux(qi,_)) = match qi with
| QI_const n_const -> doc_nexp_constraint n_const
| QI_id(KOpt_aux(ki,_)) ->