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.

Sign up for GitHub

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

Jump to bottom

extend decimal notation to integers #1182

Merged
merged 9 commits into from
Jan 25, 2025
Merged

extend decimal notation to integers #1182

merged 9 commits into from
Jan 25, 2025

Conversation

fblanqui
Copy link
Member

@fblanqui fblanqui commented Jan 24, 2025 •
edited
Loading

  • change builtins necessary for parsing decimal numbers:
    ask for 0, 1, .., 10, +, * instead of 0 and +1 only
    a string of digit d1..dn is then interpreted in a more efficient way as dn+10*(dn-1+..)
  • this extends to integers if the builtin - is provided
  • remove the limit on integers that can be parsed

TODO:

  • add builtins for printing binary numbers in decimal notation
  • update bnf
  • allow the mapping of decimal notations to different types at the same time ?

@NotBad4U
Copy link
Member

When we use builtin notation +1 in two modules, such as Stdlib.Natand Stdlib.Z, the last module open is considered.
Should we also add a feature to support number notation with scope e.g. "1%Nat" and 1%Z"?

@fblanqui
Copy link
Member Author

That could be interesting. This is the topic of the last TODO item but I'm not going to do it in this PR.

@fblanqui fblanqui merged commit 22a95c4 into Deducteam:master Jan 25, 2025
2 of 22 checks passed
@fblanqui fblanqui deleted the int branch January 25, 2025 11:16
@fblanqui fblanqui restored the int branch January 25, 2025 11:28
@fblanqui fblanqui deleted the int branch January 25, 2025 11:31
This was referenced Jan 25, 2025
Merged
Merged
Merged
Closed
Closed
Merged
Merged
fblanqui added a commit to Deducteam/hol2dk that referenced this pull request Jan 31, 2025
@fblanqui
Fix command mk (#169)
4ce276c 
- fix and simplify the implementation of the command mk by introducing part.mk
- add command mkfile
- xlp.ml, mapping_nat.lp and mapping_N.lp: rename "1" into "unit" as integers are not valid identifiers anymore following Deducteam/lambdapi#1182
@fblanqui fblanqui mentioned this pull request Feb 4, 2025
Merged
fblanqui added a commit that referenced this pull request Feb 5, 2025
@fblanqui
fix verifications on some builtins (#1191)
c7f932b 
- Following #1182, rename "0" into "nat_zero" and "+1" into "nat_succ".
- Simplify code for handling the notation command.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@fblanqui @NotBad4U