gen_graph.py 1.47 KB
Newer Older
Benoit Viguier's avatar
WIP  
Benoit Viguier committed
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
#!/usr/bin/env python3

import os

def save(fn, z):
    d = open(fn, 'w', encoding="utf-8")
    d.write(z)
    d.close()

def main():

    # MAIN
    list_parse = []
    dirs = ['Gen', 'Libs', 'ListsOp', 'Low', 'Mid']
    for dir in dirs:
        coqfiles = os.listdir(dir)
        for coqfile in coqfiles:
            if coqfile[-2:] == '.v':
                list_parse.append(dir + '.' + coqfile[:-2])

    requires = ''
    prints = 'Print FileDependGraph \n'
    for cq in list_parse:
        requires += 'Require Import Tweetnacl.'+ cq + '.\n'
        prints += '\t' + cq + '\n'

    output = requires + '\n'
    output += 'Require dpdgraph.dpdgraph.\n'
Benoit Viguier's avatar
Benoit Viguier committed
29
    output += 'Set DependGraph File "main.dpd".\n'
Benoit Viguier's avatar
WIP  
Benoit Viguier committed
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
    output += prints + '.\n'
    # print(list_parse)
    print(output)
    save('gen_graph_main.v', output)


    # High
    list_parse = []
    dirs = ['High']
    for dir in dirs:
        coqfiles = os.listdir(dir)
        for coqfile in coqfiles:
            if coqfile[-2:] == '.v':
                list_parse.append(dir + '.' + coqfile[:-2])
    requires = ''
    prints = 'Print FileDependGraph \n'
    for cq in list_parse:
        requires += 'Require Import Tweetnacl.'+ cq + '.\n'
        prints += '\t' + cq + '\n'

    output = requires + '\n'
    output += 'Require dpdgraph.dpdgraph.\n'
Benoit Viguier's avatar
Benoit Viguier committed
52
    output += 'Set DependGraph File "high.dpd".\n'
Benoit Viguier's avatar
WIP  
Benoit Viguier committed
53
54
55
56
57
58
59
60
    output += prints + '.\n'
    # print(list_parse)
    print(output)
    save('gen_graph_high.v', output)


if __name__ == '__main__':
    main()