diff options
| author | Florian Angeletti <florian.angeletti@inria.fr> | 2022-10-19 18:01:35 +0200 |
|---|---|---|
| committer | Florian Angeletti <florian.angeletti@inria.fr> | 2023-01-02 15:39:24 +0100 |
| commit | 36253e6200872c07e0ba7596d9dff642637bf3c7 (patch) | |
| tree | fca30b7065b3bb892d2539f1d6f3ff83e92673a3 /typing/printtyp.ml | |
| parent | 522f85f9e8653d8533f1060627fede891344905f (diff) | |
| download | ocaml-36253e6200872c07e0ba7596d9dff642637bf3c7.tar.gz | |
review: human id abstraction
Diffstat (limited to 'typing/printtyp.ml')
| -rw-r--r-- | typing/printtyp.ml | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/typing/printtyp.ml b/typing/printtyp.ml index 8c73898dfe..fa66a5a8ca 100644 --- a/typing/printtyp.ml +++ b/typing/printtyp.ml @@ -243,6 +243,18 @@ let with_hidden ids f = let updated = List.fold_left update !bound_in_recursion ids in protect_refs [ R(bound_in_recursion, updated )] f +let human_id id index = + if index = 0 then + Ident.name id + else + (* We print the most k-time overshadowed identifier as `name/(k+1)`. + This naming scheme has the advantage of creating a non-ambiguous gap + between the identifier in scope, which is printed as `name`, and the + most recent shadowed identifier, printed as `name/2`. + *) + let ordinal = index + 1 in + String.concat "/" [Ident.name id; string_of_int ordinal] + let indexed_name namespace id = let find namespace id env = match namespace with | Type -> Env.find_type_index id env @@ -268,9 +280,8 @@ let indexed_name namespace id = if Ident.same p id then Ident.name id else - String.concat "/" [Ident.name id; string_of_int (2 + n)] - | Some n, None -> - String.concat "/" [Ident.name id; string_of_int (1 + n)] + human_id id (1 + n) + | Some n, None -> human_id id n let ident_name namespace id = if not !enabled || fuzzy_id namespace id then |