Hugging Face's logo

Spaces:
delta-lab-ai
/
lean-refactor-arena
Running

App Files Community
lean-refactor-arena
File size: 2,868 Bytes
0115dcf
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
import Pantograph
import Test.Common

open Lean Pantograph Frontend

namespace Pantograph.Test.Frontend.Refactor

abbrev Test := Environment β†’ TestT IO Unit

deriving instance Repr, DecidableEq for FileMap

private def test_merge_file_map : Test := Ξ» _env ↦ do
  let src1 := "
set_option pp.explicit true
open Nat in
def f : Nat β†’ Nat := id
  ".trim
  let src2 := "
set_option pp.explicit true
open Nat in
def f : Nat β†’ Nat :=
  id
  ".trim
  let filemap1 := s!"{src1}\n{src2}".toFileMap
  let filemap2 := Refactor.mergeFileMap src1.toFileMap src2.toFileMap
  checkEq "result" filemap1 filemap2

example : Ξ£' f : Nat β†’ Nat, βˆ€ (n : Nat), f n = n := by
  constructor
  intro n; rfl

private def test_id : Test := Ξ» env ↦ do
  let src := "
set_option pp.explicit true
open Nat in
def f : Nat β†’ Nat := id
  "
  let expected := "
set_option pp.explicit true
open Nat in
def f : Nat β†’ Nat :=
  id
  ".trim
  let result ← runRefactor env src
  checkEq "result" result.trim expected

private def test_simple : Test := Ξ» env ↦ do
  let src := "
/-- S1 -/
def f : Nat β†’ Nat := sorry
theorem mystery (n : Nat) : f n = n := sorry
  "
  let expected := "
/-- S1  -/
def f_composite : { f : Nat β†’ Nat // βˆ€ (n : Nat), f n = n } :=
  sorry
  ".trim
  let result ← runRefactor env src
  checkEq "result" result.trim expected

private def test_invalid : Test := Ξ» env ↦ do
  let src := "
/-- S1 -/
def f : Nat β†’ Nat := sorry
theorem mystery (n : Nat) , f n = n := sorry
  "
  try
    let _ ← runRefactor env src
    fail "Should fail"
  catch ex : IO.Error =>
    checkEq "error" ex.toString s!"{defaultFileName}:4:25: error: unexpected token ','; expected ':'\n"

private def test_intercalating : Test := Ξ» env ↦ do
  let src := "
def f : Nat β†’ Nat := sorry
def helper (n : Nat) : Nat := n + 1
theorem mystery (n : Nat) : f n = helper n := sorry
  "
  let expected := "
def helper (n : Nat) : Nat :=
  n + 1
def f_composite : { f : Nat β†’ Nat // βˆ€ (n : Nat), f n = helper n } :=
  sorry
  ".trim
  let result ← runRefactor env src
  checkEq "result" result.trim expected

private def test_predicate : Test := Ξ» env ↦ do
  let src := "
def q : (Nat β†’ Nat) β†’ Prop := sorry
def p : (Nat β†’ Nat) β†’ Prop := sorry
theorem mystery : p Nat.succ := sorry
  "
  let expected := "
def q : (Nat β†’ Nat) β†’ Prop :=
  sorry
def p_composite : { p : (Nat β†’ Nat) β†’ Prop // p Nat.succ } :=
  sorry
  ".trim
  let result ← runRefactor env src
  checkEq "result" result.trim expected

def suite (env : Environment): List (String Γ— IO LSpec.TestSeq) :=
  let tests := [
    ("merge file map", test_merge_file_map),
    ("id", test_id),
    ("simple", test_simple),
    ("invalid", test_invalid),
    ("intercalating", test_intercalating),
    ("predicate", test_predicate),
  ]
  tests.map Ξ» (name, test) => (name, runTest $ test env)