diff options
| author | Brian Campbell | 2020-11-25 21:45:49 +0000 |
|---|---|---|
| committer | Brian Campbell | 2020-11-25 21:46:03 +0000 |
| commit | 3d0064a157a711f21d23f56dc2c423b2e3b1d74a (patch) | |
| tree | d9af47b782b8fee55c8a1a7a720d61710c82febb | |
| parent | 1c425ffde61d7dafa989a9c53df0eba6c0672248 (diff) | |
Fix Lem output for single element enum
| -rw-r--r-- | src/pretty_print_lem.ml | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/single_enum.sail | 10 |
2 files changed, 11 insertions, 1 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index e40de7aa..a6002f9a 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1263,7 +1263,7 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with | _ -> let rec range i j = if i > j then [] else i :: (range (i+1) j) in let nats = range 0 in - let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_lem_ctor enums) in + let enums_doc = group (pipe ^^ space ^^ separate_map (break 1 ^^ pipe ^^ space) doc_id_lem_ctor enums) in let typ_pp = (doc_op equals) (concat [string "type"; space; doc_id_lem_type id;]) (enums_doc) in diff --git a/test/typecheck/pass/single_enum.sail b/test/typecheck/pass/single_enum.sail new file mode 100644 index 00000000..7293c43a --- /dev/null +++ b/test/typecheck/pass/single_enum.sail @@ -0,0 +1,10 @@ +enum foo = { BAR } + +val f : foo -> int +function f BAR = 1 + +val g : foo -> int +function g x = match x { BAR => 1 } + +val h : int -> foo +function h _ = BAR |