-
Notifications
You must be signed in to change notification settings - Fork 6
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
Idris2 pretty printer initial support #208
base: master
Are you sure you want to change the base?
Conversation
|
||
NamesRestrictions where | ||
reservedKeywords = fromList [ | ||
"**", ",", "->", ".", "..", ".[|", ":", "; _", ";", "<-", "=", "=>", "%", "=", "===", "!", "&", "|", |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"; _"
looks like a very interesting reversed keyword, at least because it contains a single space symbol. In what cases would it ever be needed here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
BTW, ===
is not reversed, you can declare your own function with this name, the same as Bool
. But privitives like Integer
, {Int, Bits}{8, 16, 32, 64}
, Char
, String
and %World
should be added.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also, Lazy
is also almost a keyword along with Delay
and Force
, despite it still can be a name of a namespace and module
|
||
public export | ||
data LanguageToCondition : (l : SupportedLanguage) -> FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type | ||
where |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you please put where
in the line with data
if it fits the line length
rawNewName : Fuel -> (l : SupportedLanguage) -> (Fuel -> Gen MaybeEmpty String) => | ||
(funs : Funs) -> (vars : Vars) -> (names : UniqNames l funs vars) -> | ||
Gen MaybeEmpty (s ** NameIsNew l funs vars names s) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please put l
after auto-implicits, it's better for auto-implicits that do not depend on other arguments to go first
|
||
export | ||
genNewName : Fuel -> (Fuel -> Gen MaybeEmpty String) => | ||
genNewName : {l : SupportedLanguage} -> Fuel -> Gen MaybeEmpty String -> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is it so nesessary to make existing Fuel -> Gen MaybeEmpty String
argument to be not-autoimplicit? It's okay in case when every or almost every usage needs to set this explicitly, but it this the case? I see that in some places alphaNames
are used, but it seems that in other cases auto-implicit still can be used. Am I wrong?
Additionally, please, put l
after the fuel and auto-implicits to make all generators' signatures to look more or less uniformly
isFunInfix @{JustNew @{ss} _} i = isFunInfix @{ss} i | ||
isFunInfix @{NewFun {isInfix} _} Here = isInfix | ||
isFunInfix @{NewFun @{ss} s} (There i) = isFunInfix @{ss} i | ||
isFunInfix @{NewVar @{ss} s} i = isFunInfix @{ss} i | ||
|
||
isFunPure : UniqNames l funs vars -> IndexIn funs -> Bool |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe, signatures of existing projection functions like varName
, funName
and isFunInfix
should be changed like in this function, i.e. passing UniqNames
explicitly
AddFun True True "+" ([< Int', Int'] ==> Just Int') {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Int' ** Refl) True)} | ||
AddFun True True "*" ([< Int', Int'] ==> Just Int') {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Int' ** Refl) True)} | ||
AddFun True True "-" ([< Int', Int'] ==> Just Int') {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Int' ** Refl) True)} | ||
AddFun True True "<" ([< Int', Int'] ==> Just Bool') {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Bool' ** Refl) True)} | ||
AddFun True True "<=" ([< Int', Int'] ==> Just Bool') {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Bool' ** Refl) True)} | ||
AddFun True True "==" ([< Int', Int'] ==> Just Bool') {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Bool' ** Refl) True)} | ||
AddFun True True "||" ([< Bool', Bool'] ==> Just Bool') {lCond = Idris2Cond (IsInfix (Bool' ** Bool' ** Just Bool' ** Refl) True)} | ||
AddFun True True "&&" ([< Bool', Bool'] ==> Just Bool') {lCond = Idris2Cond (IsInfix (Bool' ** Bool' ** Just Bool' ** Refl) True)} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can't these Idris2Cond ...
expressions be found with %search
?
No description provided.