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

Extra builtins types: Word/Float/Char #12

Merged
merged 1 commit into from
Oct 29, 2020

Conversation

omelkonian
Copy link
Contributor

This introduces new built-in types for Data.Word.Word64, Double and Char without any fancy business for adding primitives (one can of course just postulate a function with the same name as the Haskell one).

Main.hs Outdated
Unit -> special Hs.UnitCon
Nat -> unqual "Integer"
Float -> unqual "Double"
Word64 -> qual "Data.Word" "Word64"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Having this qualified isn't very nice in the generated code. You anyway have to import Data.Word even to get the qualified version, so I see no strong reason to not simply use Word64.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be nice if we automatically inserted the necessary imports for built-in types, what do you think?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, why not. We are parsing the user imports, so it should be easy enough to check if it's already there. You probably also want to check that you don't have Word64 explicitly imported from another module. For checking whether or not it's used I guess the easiest solution is to traverse the generated Haskell code.

@omelkonian omelkonian force-pushed the extra-builtins-types branch from b7fa196 to dad724e Compare October 28, 2020 21:32
Copy link
Member

@UlfNorell UlfNorell left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice

@UlfNorell UlfNorell merged commit c75f829 into agda:master Oct 29, 2020
@omelkonian omelkonian deleted the extra-builtins-types branch October 29, 2020 12:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants