{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/417","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/417/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/417/comments","events_url":"https://api.github.com/repos/coq/coq/issues/417/events","html_url":"https://github.com/coq/coq/pull/417","id":204983994,"number":417,"title":"No cast surgery in let in","user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars2.githubusercontent.com/u/460771?v=3","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"labels":[{"id":485985791,"url":"https://api.github.com/repos/coq/coq/labels/cleanup","name":"cleanup","color":"0052cc","default":false}],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":13,"created_at":"2017-02-02T20:17:02Z","updated_at":"2017-04-03T13:23:50Z","closed_at":"2017-04-03T13:23:50Z","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/417","html_url":"https://github.com/coq/coq/pull/417","diff_url":"https://github.com/coq/coq/pull/417.diff","patch_url":"https://github.com/coq/coq/pull/417.patch"},"body":"Hi,\r\n\r\nHere is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than \"cast surgery\" to carry the optional type of a let-in (even more that Cast is now a type with many variants).\r\n\r\nFor the let-in, the most painful was undoubtly funind (phew).\r\n\r\nI used Option.smartmap rather than Option.map, every time it seemed sharing had to be preserved. (BTW, is there an interest - in term of efficiency - of keeping map and not binding map to smartmap?)\r\n\r\nI used an option type rather than a GHole trick by \"purity of methods\", even if it makes the code a bit more complex with all these Option.map and Option.fold_left. But since GHole is getting more and more complex these days, I thought a simple `None` would be clearer than the now intricate `GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)`.\r\n\r\nI did not move the decision of writing the type or not from detyping to constrextern. I leave it to specialists of UI to explore the possibility to keep the annotation in the term even for situations when it is not printed by default.\r\n\r\nAnswering a question from Emilio: there is a little local duplication of code because the LetIn stops to be factorized with Lambda and Prod in a couple of cases (but somehow this also helps readability by avoiding naming \"ty\" something which was the body of a LetIn).\r\n\r\nThere is another little duplication of code because of the call of a combinator to a Cast being replaced by two calls to the same combinator, once on the term, and once on the optional type.\r\n\r\nAnyway, one thing leading to another, I also cleaned a bit the types used in interning binders. At the end, this is where there is the higher number of non-trivial changes! See the logs of commits for details.\r\n\r\nI'm afraid that my time allocated on that is however elapsed so I'm stopping now and \"give the baby\" to someone else if he/she wants to do better. But it is also probably ok to be committed now if noone has specific comments requiring complex changes.\r\n\r\nThere are three small semantic changes on purpose:\r\n\r\nIn\r\n```coq\r\nRequire Import Utf8.\r\nCheck fun (x:nat) (y:=I) (z:nat) => y=y /\\ x=z.\r\n```\r\n\r\none gets the more conventional order:\r\n\r\n`λ (x : nat) (y:=I:True) (z : nat), y = y ∧ x = z`\r\n\r\nrather than:\r\n\r\n`λ (x : nat) (y:True:=I) (z : nat), y = y ∧ x = z`\r\n\r\nThen, the type of a let-in is explicitly recognized in notations which thus behave differently in corner cases involving a let in.\r\n\r\nE.g. in a notation such as\r\n\r\n```\r\nNotation \"'do' c 'as' a 'in' d\" := (let a := c in d) (at level 10).\r\nCheck (let a := I in I).\r\n(* before: do I : True as a in I *)\r\n(* after: do I as a in I *)\r\n\r\n```\r\n\r\nFinally, the message when 'pat is used at unsupported places is made uniform.\r\n\r\nHoping that I'm not forgetting anything important.\r\n\r\nYour servitor"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/291141306","html_url":"https://github.com/coq/coq/pull/417#issuecomment-291141306","issue_url":"https://api.github.com/repos/coq/coq/issues/417","id":291141306,"user":{"login":"maximedenes","id":647105,"avatar_url":"https://avatars2.githubusercontent.com/u/647105?v=3","gravatar_id":"","url":"https://api.github.com/users/maximedenes","html_url":"https://github.com/maximedenes","followers_url":"https://api.github.com/users/maximedenes/followers","following_url":"https://api.github.com/users/maximedenes/following{/other_user}","gists_url":"https://api.github.com/users/maximedenes/gists{/gist_id}","starred_url":"https://api.github.com/users/maximedenes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/maximedenes/subscriptions","organizations_url":"https://api.github.com/users/maximedenes/orgs","repos_url":"https://api.github.com/users/maximedenes/repos","events_url":"https://api.github.com/users/maximedenes/events{/privacy}","received_events_url":"https://api.github.com/users/maximedenes/received_events","type":"User","site_admin":false},"created_at":"2017-04-03T13:23:50Z","updated_at":"2017-04-03T13:23:50Z","body":"Merged in trunk, thanks!"}}
{"actor":{"display_login":"maximedenes"}}