{"action":"opened","issue":{"url":"https://api.github.com/repos/gapt/gapt/issues/431","labels_url":"https://api.github.com/repos/gapt/gapt/issues/431/labels{/name}","comments_url":"https://api.github.com/repos/gapt/gapt/issues/431/comments","events_url":"https://api.github.com/repos/gapt/gapt/issues/431/events","html_url":"https://github.com/gapt/gapt/issues/431","id":114597005,"number":431,"title":"Visitor pattern for LK proofs","user":{"login":"loewenheim","id":7622248,"avatar_url":"https://avatars.githubusercontent.com/u/7622248?v=3","gravatar_id":"","url":"https://api.github.com/users/loewenheim","html_url":"https://github.com/loewenheim","followers_url":"https://api.github.com/users/loewenheim/followers","following_url":"https://api.github.com/users/loewenheim/following{/other_user}","gists_url":"https://api.github.com/users/loewenheim/gists{/gist_id}","starred_url":"https://api.github.com/users/loewenheim/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/loewenheim/subscriptions","organizations_url":"https://api.github.com/users/loewenheim/orgs","repos_url":"https://api.github.com/users/loewenheim/repos","events_url":"https://api.github.com/users/loewenheim/events{/privacy}","received_events_url":"https://api.github.com/users/loewenheim/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/gapt/gapt/labels/Enhancement","name":"Enhancement","color":"0052cc"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-11-02T13:48:28Z","updated_at":"2015-11-02T13:48:28Z","closed_at":null,"body":"We've been talking about maybe implementing a visitor class for LK proofs. I've written a bit of code:\r\n```scala\r\nclass lkVisitor {\r\n\r\n  def apply(proof: LKProof): LKProof = withOccConnector(proof)._1\r\n\r\n  def withOccConnector(proof: LKProof): (LKProof, OccConnector[HOLFormula]) = apply_(proof)\r\n\r\n  protected def apply_(proof: LKProof): (LKProof, OccConnector[HOLFormula]) = proof match {\r\n    case p @ InitialSequent(_) =>\r\n      visitInitialSequent(p)\r\n\r\n    case p @ WeakeningLeftRule( subProof, formula ) =>\r\n      visitWeakeningLeft(p)\r\n\r\n    case p @ WeakeningRightRule( subProof, formula ) =>\r\n      visitWeakeningRight(p)\r\n\r\n    case p @ ContractionLeftRule( subProof, formula ) =>\r\n      visitContractionLeft(p)\r\n\r\n    case p @ ContractionRightRule( subProof, formula ) =>\r\n      visitContractionRight(p)\r\n\r\n    case p @ CutRule( leftSubProof, aux1, rightSubProof, aux2 ) =>\r\n      visitCut(p)\r\n  }\r\n\r\n  protected def visitInitialSequent(proof: InitialSequent): (LKProof, OccConnector[HOLFormula]) = (proof, OccConnector(proof.endSequent))\r\n\r\n  protected def visitWeakeningLeft(proof: WeakeningLeftRule): (LKProof, OccConnector[HOLFormula]) = {\r\n    val (subProofNew, subConnector) = apply_(proof.subProof)\r\n    val proofNew = WeakeningLeftRule(subProofNew, proof.mainFormula)\r\n    val connector = (proofNew.getOccConnector * subConnector * proof.getOccConnector.inv) + (proofNew.mainIndices(0), proof.mainIndices(0))\r\n\r\n    (proofNew, connector)\r\n  }\r\n\r\n  protected def visitWeakeningRight(proof: WeakeningRightRule): (LKProof, OccConnector[HOLFormula]) = {\r\n    val (subProofNew, subConnector) = apply_(proof.subProof)\r\n    val proofNew = WeakeningRightRule(subProofNew, proof.mainFormula)\r\n    val connector = (proofNew.getOccConnector * subConnector * proof.getOccConnector.inv) + (proofNew.mainIndices(0), proof.mainIndices(0))\r\n\r\n    (proofNew, connector)\r\n  }\r\n\r\n  protected def visitContractionLeft(proof: ContractionLeftRule): (LKProof, OccConnector[HOLFormula]) = {\r\n    val (subProofNew, subConnector) = apply_(proof.subProof)\r\n    val List(aux1, aux2) = proof.auxIndices(0) map subConnector.child\r\n    val proofNew = ContractionLeftRule(subProofNew, aux1, aux2)\r\n    val connector = proofNew.getOccConnector * subConnector * proof.getOccConnector.inv\r\n\r\n    (proofNew, connector)\r\n  }\r\n\r\n  protected def visitContractionRight(proof: ContractionRightRule): (LKProof, OccConnector[HOLFormula]) = {\r\n    val (subProofNew, subConnector) = apply_(proof.subProof)\r\n    val List(aux1, aux2) = proof.auxIndices(0) map subConnector.child\r\n    val proofNew = ContractionRightRule(subProofNew, aux1, aux2)\r\n    val connector = proofNew.getOccConnector * subConnector * proof.getOccConnector.inv\r\n\r\n    (proofNew, connector)\r\n  }\r\n\r\n  protected def visitCut(proof: CutRule): (LKProof, OccConnector[HOLFormula]) = {\r\n    val (leftSubProofNew, leftSubConnector) = apply_(proof.leftSubProof)\r\n    val (rightSubProofNew, rightSubConnector) = apply_(proof.rightSubProof)\r\n    val (aux1, aux2) = (leftSubConnector.child(proof.aux1), rightSubConnector.child(proof.aux2))\r\n    val proofNew = CutRule(leftSubProofNew, aux1, rightSubProofNew, aux2)\r\n    val connector = (proofNew.getLeftOccConnector * leftSubConnector * proof.getLeftOccConnector.inv) + (proofNew.getRightOccConnector * rightSubConnector * proof.getRightOccConnector.inv)\r\n\r\n    (proofNew, connector)\r\n  }\r\n\r\n}\r\n```\r\n\r\n… and so on and so forth. What do you think, @gebner? Is this the way to go?"}}