As-patterns

[ii8]

This closes #1529

[lukaszcz]

Thanks for submitting this! You can use make format to ensure that your code follows our formatting guidelines (so ormolu won't fail).

[ii8]

Struggling to install ormolu on my musl system, fixed it manually in the meantime. (nvm that wasn't it)

[paulcadman]

Struggling to install ormolu on my musl system, fixed it manually in the meantime. (nvm that wasn't it)

You should be able to run stack install ormolu from within the Juvix project to install ormolu. If not I can try to push the fix to your branch.

[ii8]

stack install ormolu

This reports Unable to find installation URLs for OS key: linux64-custom-musl-tinfo6. I did it on a different machine now, I'll figure this out at some point.

[paulcadman]

stack install ormolu

This reports Unable to find installation URLs for OS key: linux64-custom-musl-tinfo6. I did it on a different machine now, I'll figure this out at some point.

I don't think that stack works well with musl unfortunately. Please let us know if you need some help.

[janmasrovira]

Thanks for submitting this pr @ii8.

I have briefly looked at the code and I'd like to suggest some changes. Currently you've defined:

data PatternBind = PatternBind
  { _patBindName :: S.Symbol,
    _patBindPattern :: PatternArg
  }

and made it possible for the user to write:

asas : Nat → Nat;
asas p@p'@_ := p + p';

I don't think there is a point in allowing multiple as-patterns on the same pattern. For this reason, I think it would be better to modify PatternArg as follows:

data PatternArg = PatternArg
  { _patternArgIsImplicit :: IsImplicit,
    _patternArgName :: Maybe S.Symbol,
    _patternArgPattern :: Pattern
  }

Also, the name for implicit patterns should be outside of the braces. I.e.

im' : {A : Type} → (A × Nat) → ({B : Type} → B → B) → A;
im' {i@A} p@(a, zero) f := (f {A} ∘ fst) p;

should become

im' : {A : Type} → (A × Nat) → ({B : Type} → B → B) → A;
im' i@{A} p@(a, zero) f := (f {A} ∘ fst) p;

[ii8]

I don't think there is a point in allowing multiple as-patterns on the same pattern. For this reason, I think it would be better to modify PatternArg as follows:

Yes, I have thought about doing it like that, in fact I had written the exact code you suggested. I did it like this in the end because both agda and haskell allow a@b@c.

Also, the name for implicit patterns should be outside of the braces. I.e.

Same thing here, I followed agda which allows a@{b} and {a@b}.

I was indecisive myself on both of these, so I just picked the way agda does it and made the PR so I can get your opinion on it. If that knowledge doesn't change your opinion I'm happy to change the code.

[janmasrovira]

@ii8 In this particular case, we don't see enough reason to follow Haskell and Agda. We prefer to have it in the way that I proposed.

[ii8]

There is now a pattern name in PatternArg. The @ can now be used only before an opening parenthesis or brace. I've also disallowed aliasing like A@{B} where B is a variable because it's equally pointless and it would complicate type checking. With this in place it may be possible to eliminate PatternVariable completely from Pattern and instead desugar a to a@_ (the latter can't be written in source but I think you know what I mean.)

[janmasrovira]

Another consideration, currently x@(zero) is allowed but x@zero is not. I think they should both be allowed. Currently there is not much point in allowing alias for nullary constructors. But, when we have implicit arguments for constructors it may be useful. And of course the parentheses should not be required.

[janmasrovira]

@ii8 if you can solve the merge conflicts we'll merge the branch as it is. Otherwise we'll open a new pr

[ii8]

@janmasrovira sry, I've been a bit busy, I'm working on it now though. I'll do the minimum and then make a new pr for negative test cases and so on.

[janmasrovira]

@ii8 Thanks again for this contribution!