summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-08-02 16:48:36 +0100
committerAlasdair Armstrong2019-08-02 16:48:36 +0100
commit8b1c4ce0c3659020e0f2a2e04d70798931dc9b63 (patch)
tree635bf2f722f7cf5ecf6dd11b560ca1d96a32623b /src/pretty_print_lem.ml
parent94e2f401263c7efc69f7d2b731827dc41bd8c1b8 (diff)
Fix all warnings (except for two lem warnings)
Remove P_record as it's never been implemented in parser/typechecker/rewriter, and is not likely to be. This also means we can get rid of some ugliness with the fpat and mfpat types. Stubs for P_or and P_not are left as they still may get added to ASL and we might want to support them, although there are good reasons to keep our patterns simple. The lem warning for while -> while0 for ocaml doesn't matter because it's only used in lem, and the 32-bit number warning is just noise.
Diffstat (limited to 'src/pretty_print_lem.ml')
-rw-r--r--src/pretty_print_lem.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 1367d9eb..d399ec29 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -549,6 +549,7 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
| P_cons (p,p') -> doc_op (string "::") (doc_pat_lem ctxt true p) (doc_pat_lem ctxt true p')
| P_string_append _ -> unreachable l __POS__ "Lem doesn't support string append patterns"
| P_not _ -> unreachable l __POS__ "Lem doesn't support not patterns"
+ | P_or _ -> unreachable l __POS__ "Lem doesn't support or patterns"
let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with
| Typ_tup ts -> List.exists typ_needs_printed ts