-
Notifications
You must be signed in to change notification settings - Fork 27
/
clover_loader.py
35 lines (32 loc) · 1.5 KB
/
clover_loader.py
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
import os
import re
def dfy_annotation_iterator(base_path="Clover/dataset/Dafny/textbook_algo/"):
# Walk through all subdirectories of the given base path
for root, dirs, files in os.walk(base_path):
# Filter and process only files that end with '_annotation.dfy'
for file in files:
if file.endswith('_annotation.dfy') and not file.endswith('_no_sig_annotation.dfy'):
file_path = os.path.join(root, file)
# Open and read the content of the file
with open(file_path, 'r', encoding='utf-8') as f:
content = f.read()
to_trim = r'{[^{}]*}'
content = "### Spec: In Dafny, complete the following method.\n```dafny\n" + re.sub(to_trim, '{', content)
# Clean whitespace from end of prompt:
content = content.rstrip()
# Yield the content of the file
yield content
def get_groundtruth(base_path="Clover/dataset/Dafny/textbook_algo/"):
'''
Loads each ground-truth Dafny example.
'''
for root, dirs, files in os.walk(base_path):
for file in files:
if file.endswith('_strong.dfy'):
file_path = os.path.join(root, file)
with open(file_path, 'r', encoding='utf-8') as f:
content = f.read()
yield content.strip()
if __name__ == "__main__":
#print(next(dfy_annotation_iterator()))
print(next(get_groundtruth()))