forked from jrh13/hol-light
-
Notifications
You must be signed in to change notification settings - Fork 2
/
calc_num.ml.patch
105 lines (105 loc) · 3.82 KB
/
calc_num.ml.patch
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
383c383
< Array.of_list(map STANDARDIZE l1),Array.of_list l2 in
---
> Array.fromList(map STANDARDIZE l1),Array.fromList l2 in
386c386
< Array.of_list(map STANDARDIZE l1),Array.of_list l2 in
---
> Array.fromList(map STANDARDIZE l1),Array.fromList l2 in
393,394c393,394
< let th1 = Array.get add_clauses ind
< and fl = Array.get add_flags ind in
---
> let th1 = Array.sub add_clauses ind
> and fl = Array.sub add_flags ind in
412,413c412,413
< let th1 = Array.get adc_clauses ind
< and fl = Array.get adc_flags ind in
---
> let th1 = Array.sub adc_clauses ind
> and fl = Array.sub adc_flags ind in
452c452
< and pths_1 = (Array.of_list o CONJUNCTS o STANDARDIZE o prove)
---
> and pths_1 = (Array.fromList o CONJUNCTS o STANDARDIZE o prove)
509c509
< and pths_0 = (Array.of_list o CONJUNCTS o STANDARDIZE o prove)
---
> and pths_0 = (Array.fromList o CONJUNCTS o STANDARDIZE o prove)
575c575
< let th2 = Array.get pths_0 i in
---
> let th2 = Array.sub pths_0 i in
579c579
< let th2 = Array.get pths_1 i in
---
> let th2 = Array.sub pths_1 i in
628c628
< and puths_1 = (Array.of_list o CONJUNCTS o STANDARDIZE o prove)
---
> and puths_1 = (Array.fromList o CONJUNCTS o STANDARDIZE o prove)
686,688c686,688
< let puths_2 = Array.of_list
< (map (fun i -> let th1 = Array.get puths_1 (i mod 16)
< and th2 = Array.get puths_1 (i / 16) in
---
> let puths_2 = Array.fromList
> (map (fun i -> let th1 = Array.sub puths_1 (i mod 16)
> and th2 = Array.sub puths_1 (i / 16) in
713c713
< (Array.get puths_2 (16 * j + i)) in
---
> (Array.sub puths_2 (16 * j + i)) in
721c721
< (Array.get puths_1 i) in
---
> (Array.sub puths_1 i) in
1054c1054
< Int l */ Int l <= Int k then
---
> Int l */ Int l <=/ Int k then
1130c1130
< if Pervasives.compare mtm ntm = 0 then
---
> if mtm = ntm then
1172c1172
< if Pervasives.compare mtm ntm = 0 then
---
> if mtm = ntm then
1506,1541d1505
<
< (* ------------------------------------------------------------------------- *)
< (* Computation of (a EXP k) MOD n keeping intermediates reduced *)
< (* ------------------------------------------------------------------------- *)
<
< let EXP_MOD_CONV =
< let [pth_0; pth_even; pth_odd] = (CONJUNCTS o prove)
< (`(a EXP 0) MOD n = 1 MOD n /\
< (a EXP (NUMERAL(BIT0 k))) MOD n =
< ((a EXP (NUMERAL k) MOD n) EXP 2) MOD n /\
< (a EXP (NUMERAL(BIT1 k))) MOD n =
< (a * ((a EXP (NUMERAL k) MOD n) EXP 2) MOD n) MOD n`,
< REWRITE_TAC[EXP; EXP_2] THEN REWRITE_TAC[BIT0; BIT1; NUMERAL] THEN
< REWRITE_TAC[EXP; EXP_ADD] THEN CONV_TAC MOD_DOWN_CONV THEN
< REWRITE_TAC[]) in
< let conv_zero = GEN_REWRITE_CONV I [MOD_ZERO]
< and conv_0 = GEN_REWRITE_CONV I [pth_0]
< and conv_even = GEN_REWRITE_CONV I [pth_even]
< and conv_odd = GEN_REWRITE_CONV I [pth_odd] in
< let rec conv tm =
< ((conv_0 THENC NUM_MOD_CONV) ORELSEC
< (conv_even THENC
< LAND_CONV(LAND_CONV conv THENC NUM_EXP_CONV) THENC
< NUM_MOD_CONV) ORELSEC
< (conv_odd THENC
< LAND_CONV(RAND_CONV(LAND_CONV(LAND_CONV conv THENC NUM_EXP_CONV) THENC
< NUM_MOD_CONV) THENC
< NUM_MULT_CONV) THENC
< NUM_MOD_CONV)) tm in
< let fullconv = (conv_zero THENC NUM_EXP_CONV) ORELSEC conv in
< fun tm ->
< match tm with
< Comb(Comb(Const("MOD",_),
< Comb(Comb(Const("EXP",_),m),k)),n)
< when is_numeral m && is_numeral k && is_numeral n -> fullconv tm
< | _ -> failwith "EXP_MOD_CONV";;