{"action":"created","comment":{"url":"https://api.github.com/repos/mit-plv/bedrock2/pulls/comments/197267010","pull_request_review_id":130980277,"id":197267010,"node_id":"MDI0OlB1bGxSZXF1ZXN0UmV2aWV3Q29tbWVudDE5NzI2NzAxMA==","diff_hunk":"@@ -1,201 +1,453 @@\n-Require Import Coq.Lists.List.\n-Import ListNotations.\n-Require Import lib.LibTacticsMin.\n-Require Import riscv.util.BitWidths.\n-Require Import compiler.Common.\n-Require Import compiler.Tactics.\n-Require Import compiler.Op.\n-Require Import compiler.StateCalculus.\n-Require Import bbv.DepEqNat.\n-Require Import compiler.NameWithEq.\n-Require Import Coq.Program.Tactics.\n-Require Import compiler.Memory.\n-\n-Section ExprImp1.\n-\n-  Context {Bw: BitWidths}. (* bit width *)\n-\n-  Context {Name: NameWithEq}.\n-  Notation var := (@name Name).\n-  Existing Instance eq_name_dec.\n-  Context {FName : NameWithEq}.\n-  Notation func := (@name FName).\n-\n-\n-  Context {state: Type}.\n-  Context {stateMap: Map state var (word wXLEN)}.\n-  Context {vars: Type}.\n-  Context {varset: set vars var}.\n-\n-  Ltac state_calc := state_calc_generic (@name Name) (word wXLEN).\n-  Ltac set_solver := set_solver_generic (@name Name).\n-\n-  Inductive expr: Set :=\n-    | ELit(v: word wXLEN): expr\n-    | EVar(x: var): expr\n-    | EOp(op: binop)(e1 e2: expr): expr.\n-\n-  Inductive stmt: Set :=\n-    | SLoad(x: var)(addr: expr): stmt\n-    | SStore(addr val: expr): stmt\n-    | SSet(x: var)(e: expr): stmt\n-    | SIf(cond: expr)(bThen bElse: stmt): stmt\n-    | SWhile(cond: expr)(body: stmt): stmt\n-    | SSeq(s1 s2: stmt): stmt\n-    | SSkip: stmt\n-    | SCall(binds: list var)(f: func)(args: list expr).\n-\n-  Fixpoint eval_expr(st: state)(e: expr): option (word wXLEN) :=\n+Set Universe Polymorphism.\n+Unset Universe Minimization ToSet.\n+(* TODO: should we do this?","path":"src/ExprImp.v","position":51,"original_position":51,"commit_id":"2f41000821c54839b797d9915bcbf5cbc095a9cf","original_commit_id":"2f41000821c54839b797d9915bcbf5cbc095a9cf","user":{"login":"andres-erbsen","id":918403,"node_id":"MDQ6VXNlcjkxODQwMw==","avatar_url":"https://avatars0.githubusercontent.com/u/918403?v=4","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false},"body":"Non-universe-polymorphic definitions are depraceted, we use polymorphic ones. `Universe Minimization ToSet` is a backwards compatability mode for that.\r\n`Primitive Projections` means that you never need to destruct records to get something to typecheck.","created_at":"2018-06-21T20:29:00Z","updated_at":"2018-06-21T20:29:05Z","html_url":"https://github.com/mit-plv/bedrock2/pull/14#discussion_r197267010","pull_request_url":"https://api.github.com/repos/mit-plv/bedrock2/pulls/14","author_association":"NONE","_links":{"self":{"href":"https://api.github.com/repos/mit-plv/bedrock2/pulls/comments/197267010"},"html":{"href":"https://github.com/mit-plv/bedrock2/pull/14#discussion_r197267010"},"pull_request":{"href":"https://api.github.com/repos/mit-plv/bedrock2/pulls/14"}},"in_reply_to_id":197231747},"pull_request":{"url":"https://api.github.com/repos/mit-plv/bedrock2/pulls/14","id":196535248,"node_id":"MDExOlB1bGxSZXF1ZXN0MTk2NTM1MjQ4","html_url":"https://github.com/mit-plv/bedrock2/pull/14","diff_url":"https://github.com/mit-plv/bedrock2/pull/14.diff","patch_url":"https://github.com/mit-plv/bedrock2/pull/14.patch","issue_url":"https://api.github.com/repos/mit-plv/bedrock2/issues/14","number":14,"state":"open","locked":false,"title":"[do not merge] semantics-refactor","user":{"login":"samuelgruetter","id":2394355,"node_id":"MDQ6VXNlcjIzOTQzNTU=","avatar_url":"https://avatars2.githubusercontent.com/u/2394355?v=4","gravatar_id":"","url":"https://api.github.com/users/samuelgruetter","html_url":"https://github.com/samuelgruetter","followers_url":"https://api.github.com/users/samuelgruetter/followers","following_url":"https://api.github.com/users/samuelgruetter/following{/other_user}","gists_url":"https://api.github.com/users/samuelgruetter/gists{/gist_id}","starred_url":"https://api.github.com/users/samuelgruetter/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/samuelgruetter/subscriptions","organizations_url":"https://api.github.com/users/samuelgruetter/orgs","repos_url":"https://api.github.com/users/samuelgruetter/repos","events_url":"https://api.github.com/users/samuelgruetter/events{/privacy}","received_events_url":"https://api.github.com/users/samuelgruetter/received_events","type":"User","site_admin":false},"body":"creating a PR, hoping that it will let me comment on several commits at a time...","created_at":"2018-06-21T18:16:21Z","updated_at":"2018-06-21T20:29:05Z","closed_at":null,"merged_at":null,"merge_commit_sha":"5067d20a72c9f115096f3931e304949a75e43d61","assignee":null,"assignees":[],"requested_reviewers":[],"requested_teams":[],"labels":[],"milestone":null,"commits_url":"https://api.github.com/repos/mit-plv/bedrock2/pulls/14/commits","review_comments_url":"https://api.github.com/repos/mit-plv/bedrock2/pulls/14/comments","review_comment_url":"https://api.github.com/repos/mit-plv/bedrock2/pulls/comments{/number}","comments_url":"https://api.github.com/repos/mit-plv/bedrock2/issues/14/comments","statuses_url":"https://api.github.com/repos/mit-plv/bedrock2/statuses/2f41000821c54839b797d9915bcbf5cbc095a9cf","head":{"label":"mit-plv:semantics-refactor","ref":"semantics-refactor","sha":"2f41000821c54839b797d9915bcbf5cbc095a9cf","user":{"login":"mit-plv","id":11860253,"node_id":"MDEyOk9yZ2FuaXphdGlvbjExODYwMjUz","avatar_url":"https://avatars3.githubusercontent.com/u/11860253?v=4","gravatar_id":"","url":"https://api.github.com/users/mit-plv","html_url":"https://github.com/mit-plv","followers_url":"https://api.github.com/users/mit-plv/followers","following_url":"https://api.github.com/users/mit-plv/following{/other_user}","gists_url":"https://api.github.com/users/mit-plv/gists{/gist_id}","starred_url":"https://api.github.com/users/mit-plv/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mit-plv/subscriptions","organizations_url":"https://api.github.com/users/mit-plv/orgs","repos_url":"https://api.github.com/users/mit-plv/repos","events_url":"https://api.github.com/users/mit-plv/events{/privacy}","received_events_url":"https://api.github.com/users/mit-plv/received_events","type":"Organization","site_admin":false},"repo":{"id":135329184,"node_id":"MDEwOlJlcG9zaXRvcnkxMzUzMjkxODQ=","name":"bedrock2","full_name":"mit-plv/bedrock2","owner":{"login":"mit-plv","id":11860253,"node_id":"MDEyOk9yZ2FuaXphdGlvbjExODYwMjUz","avatar_url":"https://avatars3.githubusercontent.com/u/11860253?v=4","gravatar_id":"","url":"https://api.github.com/users/mit-plv","html_url":"https://github.com/mit-plv","followers_url":"https://api.github.com/users/mit-plv/followers","following_url":"https://api.github.com/users/mit-plv/following{/other_user}","gists_url":"https://api.github.com/users/mit-plv/gists{/gist_id}","starred_url":"https://api.github.com/users/mit-plv/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mit-plv/subscriptions","organizations_url":"https://api.github.com/users/mit-plv/orgs","repos_url":"https://api.github.com/users/mit-plv/repos","events_url":"https://api.github.com/users/mit-plv/events{/privacy}","received_events_url":"https://api.github.com/users/mit-plv/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/mit-plv/bedrock2","description":"Towards a low-level systems programming language with a verified compiler","fork":false,"url":"https://api.github.com/repos/mit-plv/bedrock2","forks_url":"https://api.github.com/repos/mit-plv/bedrock2/forks","keys_url":"https://api.github.com/repos/mit-plv/bedrock2/keys{/key_id}","collaborators_url":"https://api.github.com/repos/mit-plv/bedrock2/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/mit-plv/bedrock2/teams","hooks_url":"https://api.github.com/repos/mit-plv/bedrock2/hooks","issue_events_url":"https://api.github.com/repos/mit-plv/bedrock2/issues/events{/number}","events_url":"https://api.github.com/repos/mit-plv/bedrock2/events","assignees_url":"https://api.github.com/repos/mit-plv/bedrock2/assignees{/user}","branches_url":"https://api.github.com/repos/mit-plv/bedrock2/branches{/branch}","tags_url":"https://api.github.com/repos/mit-plv/bedrock2/tags","blobs_url":"https://api.github.com/repos/mit-plv/bedrock2/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/mit-plv/bedrock2/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/mit-plv/bedrock2/git/refs{/sha}","trees_url":"https://api.github.com/repos/mit-plv/bedrock2/git/trees{/sha}","statuses_url":"https://api.github.com/repos/mit-plv/bedrock2/statuses/{sha}","languages_url":"https://api.github.com/repos/mit-plv/bedrock2/languages","stargazers_url":"https://api.github.com/repos/mit-plv/bedrock2/stargazers","contributors_url":"https://api.github.com/repos/mit-plv/bedrock2/contributors","subscribers_url":"https://api.github.com/repos/mit-plv/bedrock2/subscribers","subscription_url":"https://api.github.com/repos/mit-plv/bedrock2/subscription","commits_url":"https://api.github.com/repos/mit-plv/bedrock2/commits{/sha}","git_commits_url":"https://api.github.com/repos/mit-plv/bedrock2/git/commits{/sha}","comments_url":"https://api.github.com/repos/mit-plv/bedrock2/comments{/number}","issue_comment_url":"https://api.github.com/repos/mit-plv/bedrock2/issues/comments{/number}","contents_url":"https://api.github.com/repos/mit-plv/bedrock2/contents/{+path}","compare_url":"https://api.github.com/repos/mit-plv/bedrock2/compare/{base}...{head}","merges_url":"https://api.github.com/repos/mit-plv/bedrock2/merges","archive_url":"https://api.github.com/repos/mit-plv/bedrock2/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/mit-plv/bedrock2/downloads","issues_url":"https://api.github.com/repos/mit-plv/bedrock2/issues{/number}","pulls_url":"https://api.github.com/repos/mit-plv/bedrock2/pulls{/number}","milestones_url":"https://api.github.com/repos/mit-plv/bedrock2/milestones{/number}","notifications_url":"https://api.github.com/repos/mit-plv/bedrock2/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/mit-plv/bedrock2/labels{/name}","releases_url":"https://api.github.com/repos/mit-plv/bedrock2/releases{/id}","deployments_url":"https://api.github.com/repos/mit-plv/bedrock2/deployments","created_at":"2018-05-29T17:15:22Z","updated_at":"2018-06-20T18:09:38Z","pushed_at":"2018-06-21T18:16:24Z","git_url":"git://github.com/mit-plv/bedrock2.git","ssh_url":"git@github.com:mit-plv/bedrock2.git","clone_url":"https://github.com/mit-plv/bedrock2.git","svn_url":"https://github.com/mit-plv/bedrock2","homepage":"","size":498,"stargazers_count":1,"watchers_count":1,"language":"Coq","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":0,"mirror_url":null,"archived":false,"open_issues_count":8,"license":{"key":"mit","name":"MIT License","spdx_id":"MIT","url":"https://api.github.com/licenses/mit","node_id":"MDc6TGljZW5zZTEz"},"forks":0,"open_issues":8,"watchers":1,"default_branch":"master"}},"base":{"label":"mit-plv:master","ref":"master","sha":"21e85c94e3b7a1f36388b503656739c803b6daf5","user":{"login":"mit-plv","id":11860253,"node_id":"MDEyOk9yZ2FuaXphdGlvbjExODYwMjUz","avatar_url":"https://avatars3.githubusercontent.com/u/11860253?v=4","gravatar_id":"","url":"https://api.github.com/users/mit-plv","html_url":"https://github.com/mit-plv","followers_url":"https://api.github.com/users/mit-plv/followers","following_url":"https://api.github.com/users/mit-plv/following{/other_user}","gists_url":"https://api.github.com/users/mit-plv/gists{/gist_id}","starred_url":"https://api.github.com/users/mit-plv/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mit-plv/subscriptions","organizations_url":"https://api.github.com/users/mit-plv/orgs","repos_url":"https://api.github.com/users/mit-plv/repos","events_url":"https://api.github.com/users/mit-plv/events{/privacy}","received_events_url":"https://api.github.com/users/mit-plv/received_events","type":"Organization","site_admin":false},"repo":{"id":135329184,"node_id":"MDEwOlJlcG9zaXRvcnkxMzUzMjkxODQ=","name":"bedrock2","full_name":"mit-plv/bedrock2","owner":{"login":"mit-plv","id":11860253,"node_id":"MDEyOk9yZ2FuaXphdGlvbjExODYwMjUz","avatar_url":"https://avatars3.githubusercontent.com/u/11860253?v=4","gravatar_id":"","url":"https://api.github.com/users/mit-plv","html_url":"https://github.com/mit-plv","followers_url":"https://api.github.com/users/mit-plv/followers","following_url":"https://api.github.com/users/mit-plv/following{/other_user}","gists_url":"https://api.github.com/users/mit-plv/gists{/gist_id}","starred_url":"https://api.github.com/users/mit-plv/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mit-plv/subscriptions","organizations_url":"https://api.github.com/users/mit-plv/orgs","repos_url":"https://api.github.com/users/mit-plv/repos","events_url":"https://api.github.com/users/mit-plv/events{/privacy}","received_events_url":"https://api.github.com/users/mit-plv/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/mit-plv/bedrock2","description":"Towards a low-level systems programming language with a verified compiler","fork":false,"url":"https://api.github.com/repos/mit-plv/bedrock2","forks_url":"https://api.github.com/repos/mit-plv/bedrock2/forks","keys_url":"https://api.github.com/repos/mit-plv/bedrock2/keys{/key_id}","collaborators_url":"https://api.github.com/repos/mit-plv/bedrock2/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/mit-plv/bedrock2/teams","hooks_url":"https://api.github.com/repos/mit-plv/bedrock2/hooks","issue_events_url":"https://api.github.com/repos/mit-plv/bedrock2/issues/events{/number}","events_url":"https://api.github.com/repos/mit-plv/bedrock2/events","assignees_url":"https://api.github.com/repos/mit-plv/bedrock2/assignees{/user}","branches_url":"https://api.github.com/repos/mit-plv/bedrock2/branches{/branch}","tags_url":"https://api.github.com/repos/mit-plv/bedrock2/tags","blobs_url":"https://api.github.com/repos/mit-plv/bedrock2/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/mit-plv/bedrock2/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/mit-plv/bedrock2/git/refs{/sha}","trees_url":"https://api.github.com/repos/mit-plv/bedrock2/git/trees{/sha}","statuses_url":"https://api.github.com/repos/mit-plv/bedrock2/statuses/{sha}","languages_url":"https://api.github.com/repos/mit-plv/bedrock2/languages","stargazers_url":"https://api.github.com/repos/mit-plv/bedrock2/stargazers","contributors_url":"https://api.github.com/repos/mit-plv/bedrock2/contributors","subscribers_url":"https://api.github.com/repos/mit-plv/bedrock2/subscribers","subscription_url":"https://api.github.com/repos/mit-plv/bedrock2/subscription","commits_url":"https://api.github.com/repos/mit-plv/bedrock2/commits{/sha}","git_commits_url":"https://api.github.com/repos/mit-plv/bedrock2/git/commits{/sha}","comments_url":"https://api.github.com/repos/mit-plv/bedrock2/comments{/number}","issue_comment_url":"https://api.github.com/repos/mit-plv/bedrock2/issues/comments{/number}","contents_url":"https://api.github.com/repos/mit-plv/bedrock2/contents/{+path}","compare_url":"https://api.github.com/repos/mit-plv/bedrock2/compare/{base}...{head}","merges_url":"https://api.github.com/repos/mit-plv/bedrock2/merges","archive_url":"https://api.github.com/repos/mit-plv/bedrock2/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/mit-plv/bedrock2/downloads","issues_url":"https://api.github.com/repos/mit-plv/bedrock2/issues{/number}","pulls_url":"https://api.github.com/repos/mit-plv/bedrock2/pulls{/number}","milestones_url":"https://api.github.com/repos/mit-plv/bedrock2/milestones{/number}","notifications_url":"https://api.github.com/repos/mit-plv/bedrock2/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/mit-plv/bedrock2/labels{/name}","releases_url":"https://api.github.com/repos/mit-plv/bedrock2/releases{/id}","deployments_url":"https://api.github.com/repos/mit-plv/bedrock2/deployments","created_at":"2018-05-29T17:15:22Z","updated_at":"2018-06-20T18:09:38Z","pushed_at":"2018-06-21T18:16:24Z","git_url":"git://github.com/mit-plv/bedrock2.git","ssh_url":"git@github.com:mit-plv/bedrock2.git","clone_url":"https://github.com/mit-plv/bedrock2.git","svn_url":"https://github.com/mit-plv/bedrock2","homepage":"","size":498,"stargazers_count":1,"watchers_count":1,"language":"Coq","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":0,"mirror_url":null,"archived":false,"open_issues_count":8,"license":{"key":"mit","name":"MIT License","spdx_id":"MIT","url":"https://api.github.com/licenses/mit","node_id":"MDc6TGljZW5zZTEz"},"forks":0,"open_issues":8,"watchers":1,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/mit-plv/bedrock2/pulls/14"},"html":{"href":"https://github.com/mit-plv/bedrock2/pull/14"},"issue":{"href":"https://api.github.com/repos/mit-plv/bedrock2/issues/14"},"comments":{"href":"https://api.github.com/repos/mit-plv/bedrock2/issues/14/comments"},"review_comments":{"href":"https://api.github.com/repos/mit-plv/bedrock2/pulls/14/comments"},"review_comment":{"href":"https://api.github.com/repos/mit-plv/bedrock2/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/mit-plv/bedrock2/pulls/14/commits"},"statuses":{"href":"https://api.github.com/repos/mit-plv/bedrock2/statuses/2f41000821c54839b797d9915bcbf5cbc095a9cf"}},"author_association":"CONTRIBUTOR"}}
{"actor":{"display_login":"andres-erbsen"}}