diff options
| author | Thomas Bauereiss | 2017-10-19 15:38:42 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-10-19 16:00:54 +0100 |
| commit | faa725a8f0211ca7bc7aeb48f41dbf93380324ff (patch) | |
| tree | 0bfe7408c38aaec5d7515e92a0fa2bc53799b67c /src | |
| parent | 3afeae4cec57fbeb7638e21e39301c18aa81b9d6 (diff) | |
Mangle names with '#' characters in Lem pretty-printing
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 7900e560..f135da4e 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -62,7 +62,7 @@ let is_number_char c = c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' || c = '6' || c = '7' || c = '8' || c = '9' -let fix_id remove_tick name = match name with +let rec fix_id remove_tick name = match name with | "assert" | "lsl" | "lsr" @@ -82,7 +82,9 @@ let fix_id remove_tick name = match name with | "integer" -> name ^ "'" | _ -> - if name.[0] = '\'' then + if String.contains name '#' then + fix_id remove_tick (String.concat "_" (Util.split_on_char '#' name)) + else if name.[0] = '\'' then let var = String.sub name 1 (String.length name - 1) in if remove_tick then var else (var ^ "'") else if is_number_char(name.[0]) then |