{"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":14,"created_at":"2016-06-07T15:23:42Z","updated_at":"2016-06-08T21:04:44Z","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/224727300","html_url":"https://github.com/idris-lang/Idris-dev/issues/3209#issuecomment-224727300","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3209","id":224727300,"user":{"login":"ahmadsalim","id":1647846,"avatar_url":"https://avatars.githubusercontent.com/u/1647846?v=3","gravatar_id":"","url":"https://api.github.com/users/ahmadsalim","html_url":"https://github.com/ahmadsalim","followers_url":"https://api.github.com/users/ahmadsalim/followers","following_url":"https://api.github.com/users/ahmadsalim/following{/other_user}","gists_url":"https://api.github.com/users/ahmadsalim/gists{/gist_id}","starred_url":"https://api.github.com/users/ahmadsalim/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ahmadsalim/subscriptions","organizations_url":"https://api.github.com/users/ahmadsalim/orgs","repos_url":"https://api.github.com/users/ahmadsalim/repos","events_url":"https://api.github.com/users/ahmadsalim/events{/privacy}","received_events_url":"https://api.github.com/users/ahmadsalim/received_events","type":"User","site_admin":false},"created_at":"2016-06-08T21:04:44Z","updated_at":"2016-06-08T21:04:44Z","body":"@nicolabotta So there are no changes in the parser in that commit, so maybe it is a previous commit or trifecta as you mentioned?"}}
{"actor":{"display_login":"ahmadsalim"}}