Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix Haskell tuple rendering #92

Merged
merged 1 commit into from
Apr 20, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/main/scala/com/melvic/chi/ast/Proof.scala
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ object Proof {

final case class Infix(left: Proof, right: Proof) extends Proof

final case class Attribute(function: Proof, name: String) extends Proof
final case class Indexed(function: Proof, index: Int) extends Proof

def atomicVariable(name: String): Variable =
Variable(name, PUnit)
Expand Down
4 changes: 1 addition & 3 deletions src/main/scala/com/melvic/chi/eval/Prover.scala
Original file line number Diff line number Diff line change
Expand Up @@ -102,9 +102,7 @@ object Prover {
components: List[Proposition]
): Result[Proof] = {
def recurse(proof: Proof, components: List[Proposition], index: Int): Result[Proof] = {
// Note: this might be too Scala-specific. Make sure to handle for
// languages that do not support this syntax.
lazy val attr = Attribute(proof, "_" + index)
lazy val attr = Indexed(proof, index)

components match {
case Nil => Result.success(attr)
Expand Down
34 changes: 23 additions & 11 deletions src/main/scala/com/melvic/chi/output/ShowHaskell.scala
Original file line number Diff line number Diff line change
Expand Up @@ -31,12 +31,21 @@ class ShowHaskell(functionName: String) extends Display {
def showBodyProofWithLevel(proof: Proof, level: Option[Int]): String = {
val indent = this.indent(level.map(_ + 1).orElse(Some(1)))

def showLambda: Abstraction => String = {
case Abstraction(in, out) => s"\\${showBodyProof(in)} -> ${showBodyProof(out)}"
}

proof match {
case TUnit => "()"
case Variable(name, _) => name
case PConjunction(components) => s"(${Utils.toCSV(components.map(showBodyProof))})"
case PRight(proof) => s"Right ${showBodyProof(proof)}"
case PLeft(proof) => s"Left ${showBodyProof(proof)}"
case TUnit => "()"
case Variable(name, _) => name
case PConjunction(components) =>
def showParam: Proof => String = {
case abs: Abstraction => showLambda(abs)
case proof => showBodyProof(proof)
}
s"(${Utils.toCSV(components.map(showParam))})"
case PRight(proof) => s"Right ${showBodyProof(proof)}"
case PLeft(proof) => s"Left ${showBodyProof(proof)}"
case EitherMatch(name, EitherCases(Abstraction(leftIn, leftOut), Abstraction(rightIn, rightOut))) =>
val leftCase = s"Left ${showBodyProof(leftIn)} -> ${showBodyProof(leftOut)}"
val rightCase = s"Right ${showBodyProof(rightIn)} -> ${showBodyProof(rightOut)}"
Expand All @@ -46,14 +55,17 @@ class ShowHaskell(functionName: String) extends Display {
case Application(function, params) =>
def showParam(param: Proof): String =
param match {
case Abstraction(in, out) => s"(\\${showBodyProof(in)} -> ${showBodyProof(out)})"
case app: Application => s"(${showBodyProof(app)})"
case left: PLeft => s"(${showBodyProof(left)})"
case right: PRight => s"(${showBodyProof(right)})"
case _ => showBodyProof(param)
case abs: Abstraction => s"(${showLambda(abs)})"
case app: Application => s"(${showBodyProof(app)})"
case left: PLeft => s"(${showBodyProof(left)})"
case right: PRight => s"(${showBodyProof(right)})"
case _ => showBodyProof(param)
}
s"${showBodyProof(function)} ${params.map(showParam).mkString(" ")}"
case Attribute(proof, name) => s"${showProof(proof)}.$name"
// For now, we can only retrieve the 1st and 2nd element of a tuple
case Indexed(proof, index) =>
val function = if (index == 1) "fst" else "snd"
showBodyProofWithLevel(Proof.applyOne(Proof.atomicVariable(function), proof), level)
}
}

Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/com/melvic/chi/output/ShowScala.scala
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ class ShowScala extends Display {
s"$functionString($nextLine${params.map(showProofWithLevel(_, nextLevel)).mkString(", " + nextLine)}$nextLine$indent)"
case Infix(left, right) =>
s"${showProof(left)}.${showProof(right)}"
case Attribute(proof, name) => s"${showProof(proof)}.$name"
case Indexed(proof, index) => s"${showProof(proof)}._$index"
}

s"$indent$proofString"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,11 @@ class HaskellFunctionsSpec extends BaseSpec {
)
}

"component of a product consequent" should "be accessible if the function is applied" in {
test("foo :: (a -> (c, b)) -> a -> c", "foo f a = fst (f a)")
test("foo :: (a -> (a, b)) -> (a -> a, a -> b)", "foo f = (\\a -> a, \\a -> snd (f a))")
}

"either over tuples" should "deconstruct the tuples" in {
generateAndShowWithInfo("foo :: Either (a, b) a -> a") should be(
output(
Expand Down