{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3209","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3209/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3209/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3209/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/3209","id":158951792,"number":3209,"title":"Parsing preorder reasoning expressions takes very, very long!","user":{"login":"nicolabotta","id":2726946,"avatar_url":"https://avatars.githubusercontent.com/u/2726946?v=3","gravatar_id":"","url":"https://api.github.com/users/nicolabotta","html_url":"https://github.com/nicolabotta","followers_url":"https://api.github.com/users/nicolabotta/followers","following_url":"https://api.github.com/users/nicolabotta/following{/other_user}","gists_url":"https://api.github.com/users/nicolabotta/gists{/gist_id}","starred_url":"https://api.github.com/users/nicolabotta/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nicolabotta/subscriptions","organizations_url":"https://api.github.com/users/nicolabotta/orgs","repos_url":"https://api.github.com/users/nicolabotta/repos","events_url":"https://api.github.com/users/nicolabotta/events{/privacy}","received_events_url":"https://api.github.com/users/nicolabotta/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/A-Confirmed","name":"A-Confirmed","color":"fbca04"},{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/C-Moderate%20Effort","name":"C-Moderate Effort","color":"006b75"},{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/S-Major","name":"S-Major","color":"b60205"},{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/U-Parser","name":"U-Parser","color":"d4c5f9"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2016-06-07T15:23:42Z","updated_at":"2016-06-07T16:51:41Z","closed_at":null,"body":"With 0.11.2-git:fc3e88c and on my machine, it takes almost 5 minutes for\r\n```\r\n> import Syntax.PreorderReasoning\r\n> %default total\r\n> multDistributesOverPlusRightEq : {x, y, z : Fraction} -> x * (y + z) `Eq` (x * y) + (x * z)\r\n> multDistributesOverPlusRightEq {x = (m, d')} {y = (n, e')} {z = (o, f')} = \r\n>   let d       =  toNat d' in\r\n>   let e       =  toNat e' in\r\n>   let f       =  toNat f' in\r\n>     ( (m * (n * f + o * e)) * (toNat ((d' * e') * (d' * f'))) )\r\n>   ={ cong {f = \\ ZUZU => (m * (n * f + o * e)) * ZUZU} toNatMultLemma }=\r\n>     ( (m * (n * f + o * e)) * ((toNat (d' * e')) * (toNat (d' * f'))) )\r\n>   ={ cong {f = \\ ZUZU => (m * (n * f + o * e)) * (ZUZU * (toNat (d' * f')))} toNatMultLemma }=\r\n>     ( (m * (n * f + o * e)) * ((d * e) * (toNat (d' * f'))) )  \r\n>   ={ cong {f = \\ ZUZU => (m * (n * f + o * e)) * ((d * e) * ZUZU)} toNatMultLemma }=\r\n>     ( (m * (n * f + o * e)) * ((d * e) * (d * f)) )  \r\n>   ={ cong {f = \\ ZUZU => (m * (n * f + o * e)) * ZUZU} (multFlipCentre d e d f) }=\r\n>     ( (m * (n * f + o * e)) * ((d * d) * (e * f)) )  \r\n>   ={ cong {f = \\ ZUZU => (m * (n * f + o * e)) * ZUZU} (sym (multAssociative d d (e * f))) }=\r\n>     ( (m * (n * f + o * e)) * (d * (d * (e * f))) )  \r\n>   ={ multAssociative (m * (n * f + o * e)) d (d * (e * f)) }=\r\n>     ( ((m * (n * f + o * e)) * d) * (d * (e * f)) )  \r\n>   ={ cong {f = \\ ZUZU => (ZUZU * d) * (d * (e * f))} (multDistributesOverPlusRight m (n * f) (o * e)) }=\r\n>     ( ((m * (n * f) + m * (o * e)) * d) * (d * (e * f)) )\r\n>   ={ cong {f = \\ ZUZU => ((ZUZU + m * (o * e)) * d) * (d * (e * f))} (multAssociative m n f) }=\r\n>     ( (((m * n) * f + m * (o * e)) * d) * (d * (e * f)) )\r\n>   ={ cong {f = \\ ZUZU => (((m * n) * f + ZUZU) * d) * (d * (e * f))} (multAssociative m o e) }=  \r\n>     ( (((m * n) * f + (m * o) * e) * d) * (d * (e * f)) )\r\n>   ={ cong {f = \\ ZUZU => ZUZU * (d * (e * f))} (multDistributesOverPlusLeft ((m * n) * f) ((m * o) * e) d)}=  \r\n>     ( (((m * n) * f) * d + ((m * o) * e) * d) * (d * (e * f)) )\r\n>   ={ cong {f = \\ ZUZU => (ZUZU + ((m * o) * e) * d) * (d * (e * f))} (sym (multAssociative (m * n) f d)) }=\r\n>     ( ((m * n) * (f * d) + ((m * o) * e) * d) * (d * (e * f)) )\r\n>   ={ cong {f = \\ ZUZU => ((m * n) * (f * d) + ZUZU) * (d * (e * f))} (sym (multAssociative (m * o) e d)) }=  \r\n>     ( ((m * n) * (f * d) + (m * o) * (e * d)) * (d * (e * f)) )\r\n>   ={ cong {f = \\ ZUZU => ((m * n) * (f * d) + (m * o) * ZUZU) * (d * (e * f))} (multCommutative e d) }=\r\n>     ( ((m * n) * (f * d) + (m * o) * (d * e)) * (d * (e * f)) )\r\n>   ={ cong {f = \\ ZUZU => ((m * n) * ZUZU + (m * o) * (d * e)) * (d * (e * f))} (multCommutative f d) }=\r\n>     ( ((m * n) * (d * f) + (m * o) * (d * e)) * (d * (e * f)) )\r\n>   ={ cong {f = \\ ZUZU => ((m * n) * (d * f) + (m * o) * (d * e)) * (d * ZUZU)} (sym toNatMultLemma) }=  \r\n>     ( ((m * n) * (d * f) + (m * o) * (d * e)) * (d * (toNat (e' * f'))) )\r\n>   ={ cong {f = \\ ZUZU => ((m * n) * (d * f) + (m * o) * (d * e)) * ZUZU}  (sym toNatMultLemma) }=  \r\n>     ( ((m * n) * (d * f) + (m * o) * (d * e)) * (toNat (d' * (e' * f'))) )\r\n>   ={ cong {f = \\ ZUZU => ((m * n) * (d * f) + (m * o) * ZUZU) * (toNat (d' * (e' * f')))} \r\n>           (sym toNatMultLemma) }=\r\n>     ( ((m * n) * (d * f) + (m * o) * (toNat (d' * e'))) * (toNat (d' * (e' * f'))) )\r\n>   ={ cong {f = \\ ZUZU => ((m * n) * ZUZU + (m * o) * (toNat (d' * e'))) * (toNat (d' * (e' * f')))} \r\n>           (sym toNatMultLemma) }=\r\n>     ( ((m * n) * (toNat (d' * f')) + (m * o) * (toNat (d' * e'))) * (toNat (d' * (e' * f'))) )\r\n>   QED\r\n```\r\nto fail to type check:\r\n```\r\n$ time idris --check Gugu.lidr\r\nGugu.lidr:3:32:When checking type of Main.multDistributesOverPlusRightEq:\r\nNo such variable Fraction\r\n\r\nreal\t4m44.659s\r\nuser\t4m43.536s\r\nsys\t0m1.292s\r\n```\r\n! Thus, parsing proofs based on preorder reasoning does not scale up anymore. Slightly longer expressions yield unacceptable type checking times. \r\n\r\nAs shown in #3208, this is the major reason for the extremely long type checking times originally reported in #3197.\r\n\r\nI have been routinely type checking this and similar examples (with suitable `import` directives) since months but, if I am not mistaken, the issue has come up (or worsened) only recently.\r\n\r\nAny idea how to circumvent this problem? Thanks, Nicola "},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/224343173","html_url":"https://github.com/idris-lang/Idris-dev/issues/3209#issuecomment-224343173","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3209","id":224343173,"user":{"login":"nicolabotta","id":2726946,"avatar_url":"https://avatars.githubusercontent.com/u/2726946?v=3","gravatar_id":"","url":"https://api.github.com/users/nicolabotta","html_url":"https://github.com/nicolabotta","followers_url":"https://api.github.com/users/nicolabotta/followers","following_url":"https://api.github.com/users/nicolabotta/following{/other_user}","gists_url":"https://api.github.com/users/nicolabotta/gists{/gist_id}","starred_url":"https://api.github.com/users/nicolabotta/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nicolabotta/subscriptions","organizations_url":"https://api.github.com/users/nicolabotta/orgs","repos_url":"https://api.github.com/users/nicolabotta/repos","events_url":"https://api.github.com/users/nicolabotta/events{/privacy}","received_events_url":"https://api.github.com/users/nicolabotta/received_events","type":"User","site_admin":false},"created_at":"2016-06-07T16:51:40Z","updated_at":"2016-06-07T16:51:40Z","body":"@ahmadsalim You are right: in the original `FractionEqProperties.lidr` file we also had proofs with long chains of `let ... in` expressions and they had negligible effects on the parsing time. But, `let`clauses are not analysed for erasure, see #2837. Thus, if I was to avoid the preorder reasoning syntax, I would rather use an idiom based on `where`clauses and `trans` rather then `let`. \r\n\r\nOn the other hand, I do not like the idea of sacrificing readability for the sake of type checking time and I think that, in principle, proofs should be easy to read for humans (in  fact, I always tend to explicitely add to my proofs trivial steps (steps that can be implemented in terms of `Refl` alone) for the human reader and it could be that some of the troubles I am experiencing are a consequence of this habit). \r\n\r\nThus, the question here is whether parsing preorder reasoning proofs can be significantly improved or not. In the first case, I am happy to wait until this is done (if it is not going to take years). On the other hand, if the misbehavior reported in this thread turns out to be a symptom of a more fundamental problem (e.g. parsing time more than linear in the length of proofs), then it would probably be meaningful to issue some warning or recommendation against using preorder reasoning in all but very short proofs. "}}
{"actor":{"display_login":"nicolabotta"}}