Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

What is missing from the current name printing? #25

Open
favonia opened this issue Sep 17, 2018 · 8 comments
Open

What is missing from the current name printing? #25

favonia opened this issue Sep 17, 2018 · 8 comments
Assignees
Labels
bug Something isn't working

Comments

@favonia
Copy link
Contributor

favonia commented Sep 17, 2018

  1. Sometimes Name.pp is used and sometimes Pp.Env and Name.to_string are used. Needs to be consistent.
  2. We are still shadowing global names in the signature (including constructors, data types, etc).
  3. Handling of variables which already have suffixes is suboptimal.
  4. Unnamed variables should try x,y,z,w for expression variables and i, j, k for dimension variables.
@favonia favonia changed the title Avoid variable shadowing in pretty printing Avoid variable shadowing during pretty printing Sep 17, 2018
@jonsterling
Copy link
Contributor

LOL I was just trying to open this exact same ticket 😆

It's funny, it manages to not shadow just one variable, and everytihng else is shadowed. oops.

@jonsterling jonsterling added the bug Something isn't working label Sep 17, 2018
@favonia
Copy link
Contributor Author

favonia commented Sep 21, 2018

Proposal @jonsterling @ecavallo

  • A named variable a is printed as the first available in a, a₁, ..., a₉, a₁₀...
  • A named variable a₂ is printed as the first available in a₂, a₃, ..., a₉, a₁₀...
  • A named variable a₀₂ is printed as the first available in a₀₂, a₀₃, ..., a₀₉, a₀₁₀...
  • An unnamed variable is printed as the first available in x, x₁, ..., x₉, x₁₀...

@jonsterling
Copy link
Contributor

@favonia I think Evan and I agree this needs to be fixed, but don't care at all in what manner it is fixed 😆

@favonia
Copy link
Contributor Author

favonia commented Sep 21, 2018

@jonsterling For now, I have to simplify the scheme to:

  • A named variable a is printed as the first available in a, a₁, ..., a₉, a₁₀...
  • An unnamed variable is printed as the first available in x, x₁, ..., x₉, x₁₀...

because I would like to use a proper UTF-8 library to strip off the suffix. (I wonder if @freebroccolo knows an immortal choice of UTF-8 libraries.)

@jonsterling
Copy link
Contributor

@favonia We are already using an immortal utf-8 library (uuseg, uuseg_string)... But please, can we just do something simple? Even without the subscripts if it is easier. This (technically minor) issue is such that any fix at all would lead to a great improvement, so we really don't need to boil the ocean for it 😆

@favonia favonia changed the title Avoid variable shadowing during pretty printing What is missing for name printing to be immortal? Sep 21, 2018
@favonia
Copy link
Contributor Author

favonia commented Sep 21, 2018

@jonsterling Another subtlety is that we should also avoid shadowing names in the global signature (names of datatypes, constructors, etc).

@jonsterling
Copy link
Contributor

@favonia Yes, agreed!!

@favonia favonia changed the title What is missing for name printing to be immortal? What is missing from the current name printing? Sep 21, 2018
@ghost
Copy link

ghost commented Sep 21, 2018

Proposal @jonsterling @ecavallo

* A named variable `a` is printed as the first available in `a`, `a₁`, ..., `a₉`, `a₁₀`...

* A named variable `a₂` is printed as the first available in `a₂`, `a₃`, ..., `a₉`, `a₁₀`...

* A named variable `a₀₂` is printed as the first available in `a₀₂`, `a₀₃`, ..., `a₀₉`, `a₀₁₀`...

* An unnamed variable is printed as the first available in `x`, `x₁`, ..., `x₉`, `x₁₀`...

I agree with Jon that the current choice of libraries for unicode stuff is probably the best available.

Regarding pretty printing with the subscripts like this, I implemented something similar here. That algorithm cycles through the full alphabet ('a' - 'z') for each new subscript but it should be easy to change to just use one letter.

@favonia favonia transferred this issue from RedPRL/redtt Nov 27, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants