{"action":"created","issue":{"url":"https://api.github.com/repos/jonsterling/JonPRL/issues/147","labels_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/147/labels{/name}","comments_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/147/comments","events_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/147/events","html_url":"https://github.com/jonsterling/JonPRL/pull/147","id":96963664,"number":147,"title":"Added first order matching tactic ala [match goal with]","user":{"login":"jozefg","id":814961,"avatar_url":"https://avatars.githubusercontent.com/u/814961?v=3","gravatar_id":"","url":"https://api.github.com/users/jozefg","html_url":"https://github.com/jozefg","followers_url":"https://api.github.com/users/jozefg/followers","following_url":"https://api.github.com/users/jozefg/following{/other_user}","gists_url":"https://api.github.com/users/jozefg/gists{/gist_id}","starred_url":"https://api.github.com/users/jozefg/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jozefg/subscriptions","organizations_url":"https://api.github.com/users/jozefg/orgs","repos_url":"https://api.github.com/users/jozefg/repos","events_url":"https://api.github.com/users/jozefg/events{/privacy}","received_events_url":"https://api.github.com/users/jozefg/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2015-07-24T04:36:10Z","updated_at":"2015-07-24T17:47:32Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/jonsterling/JonPRL/pulls/147","html_url":"https://github.com/jonsterling/JonPRL/pull/147","diff_url":"https://github.com/jonsterling/JonPRL/pull/147.diff","patch_url":"https://github.com/jonsterling/JonPRL/pull/147.patch"},"body":"This pull request boils down into 3 separate components\r\n\r\n 1. Straightforward modifications to the parser in order to let `tactic_script.fun` parse terms. We need to parse full tactic scripts *and* terms for this tactic so I tweaked that functor to make such things possible.\r\n 2. Plumb everything through the tactic AST. This is actually kind of tricky because we need a notion of substitution to deal with branches of our match tactic. This is implemented by hand (see `branchSubst`)\r\n 3. Finally, aside from some simple glue the we have `src/prover/sequent_unify.fun`. This basically has one function\r\n\r\n``` sml\r\n     val unify : {goal : term, hyps : (name * term) list} * Sequent.t -> (name * term) list\r\n```\r\nIt hunts for a subset of the sequent so that it and the goal unify with `goal` and `hyps`. Furthermore, in the resulting unification each `name` in `hyps` is unified with the label of the hypothesis it unified with in the sequent. Open questions \r\n\r\n 1. Is `branchSubst` right? It's hard to implement such things bug free\r\n 2. How can we handle matching on terms with binders partially? Currently we can because a variable can only bind to a term with arity `0` so we have to write `lam(x.???)` but a variable won't unify if there are bound variables. I think we may need a special wildcard operator. Thoughts? "},"comment":{"url":"https://api.github.com/repos/jonsterling/JonPRL/issues/comments/124597132","html_url":"https://github.com/jonsterling/JonPRL/pull/147#issuecomment-124597132","issue_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/147","id":124597132,"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":"2015-07-24T17:47:32Z","updated_at":"2015-07-24T17:47:32Z","body":"OK—If you have an idea about how to implement this wildcard operator, feel free to do it if you want!"}}