MWU/config.py at master · OUPL/MWU · GitHub

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
##########################################################################################
#  This script is intended to make it easy to adjust the parameters of the MWU system    #
#    by propagating the correct values through the (verified) oracle, the OCaml shim     #
#    and the python interface.                                                           #
#                                                                                        #
#  Use: Adjust the values of STRATEGIES, NUM_ROUNDS and ETA below, then call             #
#       `python3 config.py`.                                                             #
#                                                                                        #
#  Restrictions:                                                                         #
#    - ETA : float, STRATEGIES : int, NUM_ROUNDS : int                                   #
#    - 0 < [STRATEGIES/NUM_ROUNDS/ETA]                                                   #
#    - ETA <= 1/2                                                                        #
#    - Very large values for STRATEGIES and NUM_ROUNDS may cause memory issues in Coq    #
#      due to the fact that Coq reperesents them in unary.                               #
#                                                                                        #
##########################################################################################


import math
import re
import fileinput
import sys


############################
# Parameters to propagate
############################
STRATEGIES = 10
NUM_ROUNDS = 80
NUM_EXAMPLES = 20
ETA = .375

############################
# String patterns for Coq
############################
strat_pattern_coq = re.compile('  Definition num_strategies :=*')
strat_string_coq = "  Definition num_strategies := " + str(STRATEGIES) + ".\n"

eta_pattern_coq = re.compile('  Definition eta :=*')
eta_string_coq = ("  Definition eta := dyadic.Dmake (" +
                    str(float.as_integer_ratio(ETA)[0]) + "%Z) (" +
                    str(int(math.log(float.as_integer_ratio(ETA)[1], 2))) + "%positive).\n")

round_pattern_coq = re.compile('  Definition num_rounds := N.of_nat*')
round_string_coq = ("  Definition num_rounds := N.of_nat " + str(NUM_ROUNDS) + ".\n")

#############################
# String patterns for OCaml
#############################
strat_pattern_ocaml = re.compile('let num_strats =*')
strat_string_ocaml = "let num_strats = " + str(STRATEGIES) + "\n"

round_pattern_ocaml = re.compile('let num_rounds =*')
round_string_ocaml = "let num_rounds = " + str(NUM_ROUNDS) + "\n"


#############################
# String patterns for Python
#############################
strat_pattern_python = re.compile('num_strats =*')
strat_string_python = "num_strats = " + str(STRATEGIES) + "\n"

round_pattern_python = re.compile('num_rounds =*')
round_string_python = "num_rounds = " + str(NUM_ROUNDS) + "\n"

example_pattern_python = re.compile('num_examples =*')
example_string_python = "num_examples = " + str(NUM_EXAMPLES) + "\n"

for line in fileinput.input(["oracleExtract.v", "./runtime/OTP.ml", "./runtime/envProc.py",
                             "./examples/classifier/OTP.ml", "./examples/classifier/envProc.py"],
                             inplace=1):
    if strat_pattern_coq.match(line) :
        line = strat_string_coq
    if eta_pattern_coq.match(line) :
        line = eta_string_coq
    if round_pattern_coq.match(line) :
        line = round_string_coq
    if strat_pattern_ocaml.match(line) :
        line = strat_string_ocaml
    if round_pattern_ocaml.match(line) :
        line = round_string_ocaml
    if strat_pattern_python.match(line) :
        line = strat_string_python
    if round_pattern_python.match(line) :
        line = round_string_python
    if example_pattern_python.match(line) :
        line = example_string_python
    sys.stdout.write(line)