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

Difference between Decidable and Equality #3173

Closed
ice1000 opened this Issue Aug 4, 2018 · 6 comments

Comments

Projects
None yet
3 participants
@ice1000
Copy link
Member

ice1000 commented Aug 4, 2018

With this code (which uses some declarations listed in #3172 ):

parseF : List ℂ  List Fmt
parseF [] = []
parseF (x ∷ xs) with xs | x ≟ '%'
...         | '%' ∷ xss | yes _ = lit '%' ∷ parseF xss
...         |  c  ∷ xss | yes _ = fmt c ∷ parseF xss
...         | [] | yes _ = lit '%' ∷ []
...         | _  | no  _ = lit x ∷ parseF xs

Agda complains about the termination of the function:

image

While the one using Equality checks:

parseF : List ℂ  List Fmt
parseF [] = []
parseF ('%' ∷ '%' ∷ cs) = lit '%' ∷ parseF cs
parseF ('%' ∷  c  ∷ cs) = fmt c ∷ parseF cs
parseF ( c  ∷  cs) = lit c ∷ parseF cs
@gallais

This comment has been minimized.

Copy link
Member

gallais commented Aug 4, 2018

The problem is not the difference between using a pattern vs. a decision procedure for equality
but the with xs which adds one level of indirection between xs and the recursive call. This
prevents Agda from seeing that the call is legal.

A solution would be to drop with xs entirely (not tested):

parseF : List ℂ  List Fmt
parseF [] = []
parseF (x ∷ xs) with x ≟ '%'
parseF (x ∷ '%' ∷ xss) | yes _ = lit '%' ∷ parseF xss
parseF (x ∷ c   ∷ xss) | yes _ = fmt c ∷ parseF xss
parseF (x ∷ [])        | yes _ = lit '%' ∷ []
...                    | no  _ = lit x ∷ parseF xs
@gallais

This comment has been minimized.

Copy link
Member

gallais commented Aug 4, 2018

Note that issues are probably not the best place to discuss these type of things:
they are used to track bugs and them getting fixed.

For questions, the mailing list (https://lists.chalmers.se/mailman/listinfo/agda) and stackoverflow are probably more appropriate

@ice1000

This comment has been minimized.

Copy link
Member Author

ice1000 commented Aug 4, 2018

I know, I thought it's a bug. Now it's clear, thanks for your explanation.

Is it expected that there's a difference between with with pattern and without with pattern? I think this sounds strange.

@andreasabel

This comment has been minimized.

Copy link
Contributor

andreasabel commented Aug 5, 2018

with creates an auxiliary function, and all kinds of mangling happens.
In your case there is no reason to do with xs, since you can use ordinary pattern matching.

@andreasabel andreasabel closed this Aug 5, 2018

@gallais

This comment has been minimized.

Copy link
Member

gallais commented Aug 6, 2018

Let me throw in the really good docs about with-abstraction which even include an
explanation of how they are elaborated away!

@ice1000

This comment has been minimized.

Copy link
Member Author

ice1000 commented Aug 6, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.