Skip to content

Commit

Permalink
Fix proof search and intention tests
Browse files Browse the repository at this point in the history
  • Loading branch information
alex999990009 committed Nov 22, 2024
1 parent 17f11a4 commit 70766d3
Show file tree
Hide file tree
Showing 4 changed files with 51 additions and 37 deletions.
19 changes: 19 additions & 0 deletions src/test/kotlin/org/arend/intention/BaseIntentionTest.kt
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
package org.arend.intention

import org.arend.quickfix.QuickFixTestBase
import org.arend.util.ArendBundle

class BaseIntentionTest : QuickFixTestBase() {
fun `test wrap in goal with the end marker`() {
configure("""
\data List
| nil
| cons Nat List
\func plus (a b : Prelude.Nat) => a Nat.+ b
\func lol => {-selection-}cons (plus 2 3) (cons (plus 2 3) nil){-caret-}{-end_selection-}
""")
assertNotNull(myFixture.findSingleIntention(ArendBundle.message("arend.expression.wrapInGoal")))
}
}
15 changes: 1 addition & 14 deletions src/test/kotlin/org/arend/intention/WrapInGoalIntentionTest.kt
Original file line number Diff line number Diff line change
Expand Up @@ -37,17 +37,4 @@ class WrapInGoalIntentionTest: QuickFixTestBase() {
| suc a => a
})}
""")

fun `test with end marker`() {
configure("""
\data List
| nil
| cons Nat List
\func plus (a b : Prelude.Nat) => a Nat.+ b
\func lol => {-selection-}cons (plus 2 3) (cons (plus 2 3) nil){-caret-}{-end_selection-}
""")
assertNotNull(myFixture.findSingleIntention(fixName))
}
}
}
31 changes: 31 additions & 0 deletions src/test/kotlin/org/arend/search/ArendProofSearchInsertTest.kt
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
package org.arend.search

import org.arend.ArendTestBase
import org.arend.fileTreeFromText
import org.arend.search.proof.ProofSearchUI.Companion.insertDefinition
import org.arend.search.proof.generateProofSearchResults

class ArendProofSearchInsertTest : ArendTestBase() {
fun testCheckInsert() {
val result = fileTreeFromText("""
\data Bool
\func foo : Nat -> Bool => {?}
\func lol => {-caret-}
""".trimIndent())
result.createAndOpenFileWithCaretMarker()
val caret = myFixture.editor.caretModel.currentCaret

typecheck()
val results = generateProofSearchResults(project, "Nat").filterNotNull().toList()
assertTrue(results.size == 1)

insertDefinition(project, results[0].def, caret)
myFixture.checkResult("""
\data Bool
\func foo : Nat -> Bool => {?}
\func lol => (foo)
""".trimIndent())
}
}
23 changes: 0 additions & 23 deletions src/test/kotlin/org/arend/search/ArendProofSearchTest.kt
Original file line number Diff line number Diff line change
Expand Up @@ -155,29 +155,6 @@ class ArendProofSearchTest : ArendTestBase() {
| <=-antisymmetric {x y : Nat} : x <= y -> y <= x -> x = y
}
""", "_ <= _ -> _ <= _ -> _ = _")

fun testCheckInsert() {
val result = fileTreeFromText("""
\data Bool
\func foo : Nat -> Bool => {?}
\func lol => {-caret-}
""".trimIndent())
result.createAndOpenFileWithCaretMarker()
val caret = myFixture.editor.caretModel.currentCaret

typecheck()
val results = generateProofSearchResults(project, "Nat").filterNotNull().toList()
assertTrue(results.size == 1)

insertDefinition(project, results[0].def, caret)
myFixture.checkResult("""
\data Bool
\func foo : Nat -> Bool => {?}
\func lol => (foo)
""".trimIndent())
}
}


Expand Down

0 comments on commit 70766d3

Please sign in to comment.