{"action":"created","issue":{"url":"https://api.github.com/repos/JonPRL/sml-red-jonprl/issues/1","labels_url":"https://api.github.com/repos/JonPRL/sml-red-jonprl/issues/1/labels{/name}","comments_url":"https://api.github.com/repos/JonPRL/sml-red-jonprl/issues/1/comments","events_url":"https://api.github.com/repos/JonPRL/sml-red-jonprl/issues/1/events","html_url":"https://github.com/JonPRL/sml-red-jonprl/issues/1","id":125771980,"number":1,"title":"Parser for developments","user":{"login":"jonsterling","id":55057,"avatar_url":"https://avatars.githubusercontent.com/u/55057?v=3","gravatar_id":"","url":"https://api.github.com/users/jonsterling","html_url":"https://github.com/jonsterling","followers_url":"https://api.github.com/users/jonsterling/followers","following_url":"https://api.github.com/users/jonsterling/following{/other_user}","gists_url":"https://api.github.com/users/jonsterling/gists{/gist_id}","starred_url":"https://api.github.com/users/jonsterling/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonsterling/subscriptions","organizations_url":"https://api.github.com/users/jonsterling/orgs","repos_url":"https://api.github.com/users/jonsterling/repos","events_url":"https://api.github.com/users/jonsterling/events{/privacy}","received_events_url":"https://api.github.com/users/jonsterling/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2016-01-09T17:55:33Z","updated_at":"2016-01-09T18:02:58Z","closed_at":null,"body":"We need to implement a parser for developments. The parser will still be a little tricky, because as it goes, it needs to accumulate parsing rules for declared operators (and eventually, custom notations—but we'll leave that for after the basics are done). The idea is that when a declaration like the following is parsed,\r\n\r\n````\r\nDef something[u:σ, v:τ](M : ({σ}[τ].τ)τ, ...) : τ = [\r\n  N\r\n].\r\n````\r\n\r\n... we need to remember how to parse applications of the `something` operator. So, in the future we must parse `something[u,v]` as `CUST (\"something\", [(u, σ), (v, τ)], arity)`, where `arity` is the representation of `({σ}[τ].τ, ...)τ`.\r\n\r\nThe parser will be slightly less tricky than the old one, since we're abandoning the old \"open-ended datatype\" approach to custom operators, so there's no need for side effects in the parser. Additionally, we always parse first to ASTs, and only then do we convert them to ABTs, which means that all our parsers will be significantly easier (since we do not need to assign identity to variables and symbols immediately).\r\n\r\nOther forms of declaration (like `Thm` and `Tac`) will do exactly the same thing as `Def`; in an evaluator for developments, we will separately execute `Thm` declarations."},"comment":{"url":"https://api.github.com/repos/JonPRL/sml-red-jonprl/issues/comments/170265777","html_url":"https://github.com/JonPRL/sml-red-jonprl/issues/1#issuecomment-170265777","issue_url":"https://api.github.com/repos/JonPRL/sml-red-jonprl/issues/1","id":170265777,"user":{"login":"jonsterling","id":55057,"avatar_url":"https://avatars.githubusercontent.com/u/55057?v=3","gravatar_id":"","url":"https://api.github.com/users/jonsterling","html_url":"https://github.com/jonsterling","followers_url":"https://api.github.com/users/jonsterling/followers","following_url":"https://api.github.com/users/jonsterling/following{/other_user}","gists_url":"https://api.github.com/users/jonsterling/gists{/gist_id}","starred_url":"https://api.github.com/users/jonsterling/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonsterling/subscriptions","organizations_url":"https://api.github.com/users/jonsterling/orgs","repos_url":"https://api.github.com/users/jonsterling/repos","events_url":"https://api.github.com/users/jonsterling/events{/privacy}","received_events_url":"https://api.github.com/users/jonsterling/received_events","type":"User","site_admin":false},"created_at":"2016-01-09T18:02:57Z","updated_at":"2016-01-09T18:02:57Z","body":"And previously, (though I'm not sure this is the right ticket in which to make this remark), we had the following hierarchy of forms of equivalence:\r\n\r\n- `α`-equivalence: in the logical framework\r\n- `δ`-equivalence: based on unfolding of definitions\r\n- `~`-equivalence (computational): based on the operational semantics\r\n- `=`-equivalence (behavioral): based on the types\r\n\r\nIn the new order, we remove the notion of `δ`-equivalence and subsume it under `~`-equivalence. It might be interesting to consider extending the ABT framework such that you can define real algebraic theories (as opposed to the \"free theory\" for a signature, with no equations). Then, we would have another kind of equivalence that everything must respect; however, I want to put off something like that for a while, since I don't have any use-case for it at the moment."}}