forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
compilationLib.sml
1635 lines (1354 loc) · 57 KB
/
compilationLib.sml
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
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
Library for in-logic compilation of CakeML abstract syntax producing machine
code (for a variety of targets) using the CakeML compiler backend.
*)
structure compilationLib = struct
open preamble backendTheory
arm7_compileLib export_arm7Theory
arm8_compileLib export_arm8Theory
mips_compileLib export_mipsTheory
riscv_compileLib export_riscvTheory
ag32_compileLib export_ag32Theory
x64_compileLib export_x64Theory
mlstringSyntax presLangLib
val _ = Globals.max_print_depth := 20;
fun compilation_compset() =
let
val cs = wordsLib.words_compset();
val () = computeLib.extend_compset
[computeLib.Extenders [
basicComputeLib.add_basic_compset,
semanticsComputeLib.add_ast_compset,
backendComputeLib.add_backend_compset,
asmLib.add_asm_compset ]
] cs
in cs end;
fun allowing_rebinds f x = Feedback.trace ("Theory.allow_rebinds", 1) f x;
val zdefine = allowing_rebinds zDefine
val bare_compiler_cs = wordsLib.words_compset()
val () =
computeLib.extend_compset[
computeLib.Extenders[backendComputeLib.add_backend_compset]]
bare_compiler_cs
val bare_compiler_eval = computeLib.CBV_CONV bare_compiler_cs
fun REWR_CONV_BETA th tm = Thm.Beta (REWR_CONV th tm)
local
val uninteresting_consts =
[``ZERO``, ``BIT1``, ``BIT2``,``NUMERAL``,``CHR``,``int_of_num``,“int_neg”,
``n2w``];
in
fun interesting tm =
if TypeBase.is_constructor tm then false else
if can (first (fn pat => can (match_term pat) tm))
uninteresting_consts then false else true;
end
val output_ILs = ref (NONE : string option);
fun output_IL prog transform filename_suffix title =
case !output_ILs of
NONE => ()
| SOME filename =>
let
val fname = filename ^ "_" ^ filename_suffix
val _ = print "Writing file "
val _ = print fname
val _ = print " ... "
val strs = ("# " ^ title ^ "\n\n") :: transform prog
val _ = write_strs_to_file fname strs
val _ = print "done.\n"
in () end
(*
val _ = (output_ILs := SOME "hello")
lab_prog_def
|> concl |> rand |> find_terms is_const |> filter interesting
*)
val num_threads = ref 8
val chunk_size = ref 50
fun compile_to_data cs conf_def prog_def data_prog_name =
let
val () = computeLib.extend_compset
[computeLib.Defs [conf_def, prog_def]] cs
val eval = computeLib.CBV_CONV cs;
val conf_tm = lhs(concl conf_def)
val prog_tm = lhs(concl prog_def)
val to_flat_thm0 = timez "to_flat" eval ``to_flat ^conf_tm ^prog_tm``;
val (c,p) = to_flat_thm0 |> rconc |> dest_pair
val flat_conf_def = zdefine`flat_conf = ^c`;
val flat_prog_def = zdefine`flat_prog = ^p`;
val to_flat_thm =
to_flat_thm0 |> CONV_RULE(RAND_CONV(
FORK_CONV(REWR_CONV(SYM flat_conf_def),
REWR_CONV(SYM flat_prog_def))));
val () = computeLib.extend_compset [computeLib.Defs [flat_prog_def]] cs;
val _ = output_IL p flat_to_strs "flat.txt" "FlatLang"
val flat_conf_source_conf =
``flat_conf.source_conf``
|> (RAND_CONV(REWR_CONV flat_conf_def) THENC eval)
val flat_conf_clos_conf =
``flat_conf.clos_conf``
|> (RAND_CONV(REWR_CONV flat_conf_def) THENC eval)
val flat_conf_bvl_conf =
``flat_conf.bvl_conf``
|> (RAND_CONV(REWR_CONV flat_conf_def) THENC eval)
val to_clos_thm0 =
``to_clos ^conf_tm ^prog_tm``
|> (REWR_CONV to_clos_def THENC
RAND_CONV (REWR_CONV to_flat_thm) THENC
REWR_CONV LET_THM THENC
PAIRED_BETA_CONV)
|> timez "to_clos" (CONV_RULE(RAND_CONV(RAND_CONV eval)))
|> CONV_RULE(RAND_CONV(REWR_CONV_BETA LET_THM))
val (_,p) = to_clos_thm0 |> rconc |> dest_pair
val clos_prog_def = zdefine`clos_prog = ^p`;
val to_clos_thm =
to_clos_thm0 |> CONV_RULE(RAND_CONV(
RAND_CONV(REWR_CONV(SYM clos_prog_def))));
val () = computeLib.extend_compset [computeLib.Defs [clos_prog_def]] cs;
val _ = output_IL p clos_to_strs "clos.txt" "ClosLang"
val to_bvl_thm0 =
``to_bvl ^conf_tm ^prog_tm``
|> (REWR_CONV to_bvl_def THENC
RAND_CONV (REWR_CONV to_clos_thm) THENC
REWR_CONV LET_THM THENC
PAIRED_BETA_CONV THENC
PATH_CONV"rlr"(REWR_CONV flat_conf_clos_conf))
|> timez "to_bvl" (CONV_RULE(RAND_CONV eval))
val (c,rest) = to_bvl_thm0 |> rconc |> dest_pair
val (p,names) = dest_pair rest
val bvl_conf_def = zdefine`bvl_conf = ^c`;
val bvl_prog_def = zdefine`bvl_prog = ^p`;
val bvl_names_def = zdefine`bvl_names = ^names`;
val to_bvl_thm =
to_bvl_thm0 |> CONV_RULE(RAND_CONV(
FORK_CONV(REWR_CONV(SYM bvl_conf_def),
FORK_CONV(REWR_CONV(SYM bvl_prog_def),
REWR_CONV(SYM bvl_names_def)))));
val () = computeLib.extend_compset [computeLib.Defs
[bvl_prog_def,bvl_names_def]] cs;
val _ = output_IL p (bvl_to_strs names) "bvl.txt" "BVL"
val bvl_conf_clos_conf_start =
``bvl_conf.clos_conf.start``
|> (RAND_CONV(RAND_CONV(REWR_CONV bvl_conf_def)) THENC eval)
val bvl_conf_bvl_conf =
``bvl_conf.bvl_conf``
|> (RAND_CONV(REWR_CONV bvl_conf_def) THENC eval
THENC REWR_CONV flat_conf_bvl_conf)
val to_bvi_thm0 =
``to_bvi ^conf_tm ^prog_tm``
|> (REWR_CONV to_bvi_def THENC
RAND_CONV (REWR_CONV to_bvl_thm) THENC
REWR_CONV LET_THM THENC
PAIRED_BETA_CONV THENC
PATH_CONV"rlllr" (REWR_CONV bvl_conf_clos_conf_start) THENC
PATH_CONV"rllr"(REWR_CONV bvl_conf_bvl_conf))
val to_bvi_thm1 = to_bvi_thm0 |> CONV_RULE(RAND_CONV(
timez "to_bvi" eval))
val (c,rest) = to_bvi_thm1 |> rconc |> dest_pair
val (p,names) = rest |> dest_pair
val bvi_conf_def = zdefine`bvi_conf = ^c`;
val bvi_prog_def = zdefine`bvi_prog = ^p`;
val bvi_names_def = zdefine`bvi_names = ^names`;
val to_bvi_thm =
to_bvi_thm1 |> CONV_RULE(RAND_CONV(
FORK_CONV(REWR_CONV(SYM bvi_conf_def),
FORK_CONV(REWR_CONV(SYM bvi_prog_def),
REWR_CONV(SYM bvi_names_def)))));
val () = computeLib.extend_compset
[computeLib.Defs [bvi_prog_def,bvi_names_def]] cs;
val _ = output_IL p (bvi_to_strs names) "bvi.txt" "BVI"
val to_data_thm0 =
``to_data ^conf_tm ^prog_tm``
|> (REWR_CONV to_data_def THENC
RAND_CONV (REWR_CONV to_bvi_thm) THENC
REWR_CONV LET_THM THENC
PAIRED_BETA_CONV THENC
REWR_CONV_BETA LET_THM)
|> timez "to_data" (CONV_RULE(RAND_CONV(RAND_CONV eval)))
val (_,rest) = to_data_thm0 |> rconc |> dest_pair
val (p,names) = rest |> dest_pair
val _ = output_IL p (data_to_strs names) "data.txt" "DataLang"
val data_prog_def = allowing_rebinds (mk_abbrev data_prog_name) p
val to_data_thm =
to_data_thm0 |> CONV_RULE(RAND_CONV(
RAND_CONV(FORK_CONV(REWR_CONV(SYM data_prog_def),ALL_CONV))))
val () = computeLib.extend_compset [computeLib.Defs [data_prog_def]] cs;
val () = app delete_const
["flat_prog","clos_prog","bvl_prog","bvi_prog"]
in to_data_thm end
fun compile_to_word_0 data_prog_def to_data_thm =
let
val cs = compilation_compset()
val () =
computeLib.extend_compset [
computeLib.Extenders [
arm7_targetLib.add_arm7_encode_compset,
arm8_targetLib.add_arm8_encode_compset,
mips_targetLib.add_mips_encode_compset,
riscv_targetLib.add_riscv_encode_compset,
ag32_targetLib.add_ag32_encode_compset,
x64_targetLib.add_x64_encode_compset],
computeLib.Defs [
arm7_backend_config_def, arm7_names_def,
arm8_backend_config_def, arm8_names_def,
mips_backend_config_def, mips_names_def,
riscv_backend_config_def, riscv_names_def,
ag32_backend_config_def, ag32_names_def,
x64_backend_config_def, x64_names_def,
data_prog_def,
(* TODO: don't look up definition *)
definition "flat_conf_def",
definition "bvl_conf_def",
definition "bvi_conf_def"
]
] cs
val eval = computeLib.CBV_CONV cs;
val to_data_tm = to_data_thm |> concl |> lhs
val conf_tm = to_data_tm |> rator |> rand
val prog_tm = to_data_tm |> rand
fun ABBREV_CONV name tm = SYM (allowing_rebinds (mk_abbrev name) tm);
val to_word_0_thm = to_word_0_def
|> INST_TYPE [beta|->alpha]
|> ISPEC conf_tm |> SPEC prog_tm
|> REWRITE_RULE [LET_THM]
|> PURE_REWRITE_RULE [data_to_wordTheory.compile_0_def]
|> CONV_RULE (RAND_CONV (RAND_CONV (REWR_CONV to_data_thm)))
|> CONV_RULE (RAND_CONV (timez "data_to_word" eval))
|> CONV_RULE (PATH_CONV "rlr" (ABBREV_CONV "word_0_c"))
|> CONV_RULE (PATH_CONV "rrlr" (ABBREV_CONV "word_0_p"))
|> CONV_RULE (PATH_CONV "rrr" (ABBREV_CONV "word_0_names"))
in to_word_0_thm end;
fun compile_to_lab_new conf_tm word_0_tm lab_prog_name =
let
(* TODO: don't look up definition *)
val word_0_c_def = definition"word_0_c_def" handle HOL_ERR _ => TRUTH
val word_0_p_def = definition"word_0_p_def" handle HOL_ERR _ => TRUTH
val word_0_names_def = definition"word_0_names_def" handle HOL_ERR _ => TRUTH
val word_0_abbrevs = [word_0_c_def, word_0_p_def, word_0_names_def]
val cs = compilation_compset()
val () =
computeLib.extend_compset [
computeLib.Extenders [
arm7_targetLib.add_arm7_encode_compset,
arm8_targetLib.add_arm8_encode_compset,
mips_targetLib.add_mips_encode_compset,
riscv_targetLib.add_riscv_encode_compset,
ag32_targetLib.add_ag32_encode_compset,
x64_targetLib.add_x64_encode_compset],
computeLib.Defs ([
arm7_backend_config_def, arm7_names_def,
arm8_backend_config_def, arm8_names_def,
mips_backend_config_def, mips_names_def,
riscv_backend_config_def, riscv_names_def,
ag32_backend_config_def, ag32_names_def,
x64_backend_config_def, x64_names_def] @ word_0_abbrevs)
] cs
val eval = computeLib.CBV_CONV cs;
fun parl f = parlist (!num_threads) (!chunk_size) f
(* to_livesets_RHS partial expanded *)
val to_livesets_0_thm0 =
to_livesets_0_def |> ISPECL (map (lhs o concl) word_0_abbrevs)
|> (CONV_RULE o RAND_CONV)
(REWR_CONV LET_THM THENC PAIRED_BETA_CONV THENC
REWR_CONV LET_THM THENC BETA_CONV THENC
REWR_CONV LET_THM THENC PAIRED_BETA_CONV THENC
REWR_CONV LET_THM THENC
PATH_CONV "rlrraraalralrarllr" eval THENC
PATH_CONV"rlrraraalralralralralralrar"
(RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
(FIRST_CONV (map REWR_CONV (CONJUNCTS bool_case_thm)))))
val tm0 = to_livesets_0_thm0 |> rconc |> rand |> rand
val thm0 = el 2 word_0_abbrevs;
val tm1 = to_livesets_0_thm0 |> rconc |> rand
val (args,body) = tm1 |> rator |> rand |> dest_pabs
val word_to_word_fn_def = zdefine`word_to_word_fn ^args = ^body`;
val temp_defs = ["word_to_word_fn_def"];
val word_to_word_fn_eq =
word_to_word_fn_def
|> SPEC_ALL
|> PairRules.PABS args
|> CONV_RULE(LAND_CONV PairRules.PETA_CONV)
val word_to_word_fn = word_to_word_fn_eq|>concl|>lhs
val word_prog = thm0 |> rconc |> listSyntax.dest_list |> #1
val num_progs = length word_prog
fun eval_fn i n p =
let
val tm = mk_comb(word_to_word_fn,p)
val conv = RATOR_CONV(REWR_CONV word_to_word_fn_eq) THENC eval
in
conv tm
end;
val ths = time_with_size thms_size "inst,ssa,two-reg (par)"
(parl eval_fn) word_prog;
val thm1 =
tm1
|> (RATOR_CONV(RAND_CONV(REWR_CONV(SYM word_to_word_fn_eq))) THENC
RAND_CONV(REWR_CONV thm0) THENC map_ths_conv ths)
val word_prog0_def = allowing_rebinds (mk_abbrev "word_prog0") (thm1 |> rconc)
val temp_defs = (mk_abbrev_name"word_prog0")::temp_defs;
val thm1' = thm1 |> CONV_RULE(RAND_CONV(REWR_CONV(SYM word_prog0_def)))
(* to_livesets_0 expanded inst,ssa,two-reg *)
val to_livesets_0_thm1 =
to_livesets_0_thm0
|> CONV_RULE (RAND_CONV (
RAND_CONV(REWR_CONV thm1') THENC
BETA_CONV THENC
REWR_CONV LET_THM))
val tm2 = to_livesets_0_thm1 |> rconc |> rand
val (args,body) = tm2 |> rator |> rand |> dest_pabs
val clash_fn_def = zdefine`clash_fn ^args = ^body`;
val temp_defs = (mk_abbrev_name"clash_fn")::temp_defs;
val clash_fn_eq =
clash_fn_def
|> SPEC_ALL
|> PairRules.PABS args
|> CONV_RULE(LAND_CONV PairRules.PETA_CONV)
val clash_fn = clash_fn_eq|>concl|>lhs
val word_prog0 = thm1 |> rconc |> listSyntax.dest_list |> #1
fun eval_fn i n p =
let
val tm = mk_comb(clash_fn,p)
val conv = RATOR_CONV(REWR_CONV clash_fn_eq) THENC eval
in
conv tm
end
val ths = time_with_size thms_size "get_clash (par)"
(parl eval_fn) word_prog0;
val thm2 =
tm2
|> (RATOR_CONV(RAND_CONV(REWR_CONV(SYM clash_fn_eq))) THENC
RAND_CONV(REWR_CONV word_prog0_def) THENC map_ths_conv ths)
val to_livesets_0_thm =
to_livesets_0_thm1
|> CONV_RULE (RAND_CONV (
RAND_CONV(REWR_CONV thm2) THENC
BETA_CONV THENC
PATH_CONV"lrlr"eval))
val oracles =
to_livesets_0_thm
|> rconc |> pairSyntax.dest_pair |> #1
|> time_with_size term_size "external oracle" (reg_allocComputeLib.get_oracle reg_alloc.Irc)
val oracle_def = allowing_rebinds (mk_abbrev "oracle") oracles;
val wc =
``^conf_tm.word_to_word_conf
with col_oracle := oracle``
|> eval |> rconc
val word_prog1_def = allowing_rebinds (mk_abbrev "word_prog1") (thm2 |> rconc);
val temp_defs = (mk_abbrev_name"word_prog1") :: temp_defs
val args =
to_livesets_0_thm |> concl |> lhs |> strip_comb |> #2 |> hd |> pairSyntax.strip_pair
val to_livesets_0_thm' = to_livesets_0_thm |> CONV_RULE(RAND_CONV(
PATH_CONV"lrr"(REWR_CONV(SYM word_prog1_def))))
(* replace oracle in config *)
val to_livesets_0_oracle_thm =
to_livesets_0_invariant
|> Q.GEN `wc` |> SPEC wc
|> Q.GENL[`c`,`p`,`names`] |> ISPECL args
|> CONV_RULE ((RATOR_CONV eval) THENC BETA_CONV)
|> CONV_RULE(RAND_CONV(
REWR_CONV LET_THM THENC
RAND_CONV(REWR_CONV to_livesets_0_thm') THENC
PAIRED_BETA_CONV))
val args =
to_livesets_0_oracle_thm |> concl |> lhs |> strip_comb |> #2 |> hd |> pairSyntax.strip_pair
val LENGTH_word_prog0 =
listSyntax.mk_length(lhs(concl(word_prog0_def)))
|> (RAND_CONV(REWR_CONV word_prog0_def) THENC
listLib.LENGTH_CONV)
val LENGTH_word_prog1 =
listSyntax.mk_length(lhs(concl(word_prog1_def)))
|> (RAND_CONV(REWR_CONV word_prog1_def) THENC
listLib.LENGTH_CONV)
val oracle_list_def = allowing_rebinds (mk_abbrev "oracle_list") (oracle_def |> rconc |> rand);
val temp_defs = (mk_abbrev_name"oracle_list") :: temp_defs
val LENGTH_oracle_list =
listSyntax.mk_length(lhs(concl(oracle_list_def)))
|> (RAND_CONV(REWR_CONV oracle_list_def) THENC
listLib.LENGTH_CONV)
val LENGTH_oracle =
listSyntax.mk_length(lhs(concl(oracle_def)))
|> (RAND_CONV(REWR_CONV oracle_def) THENC
listLib.LENGTH_CONV)
val take_drop_oracle_lemma =
MATCH_MP backendTheory.TAKE_DROP_PAIR_LEMMA LENGTH_oracle
val MAP_ZIP_ZIP_lemma = MATCH_MP backendTheory.MAP_ZIP_ZIP
(LIST_CONJ [LENGTH_oracle, LENGTH_word_prog1, LENGTH_word_prog0])
val config_typ = type_of (hd args)
val config_ss = bool_ss ++ simpLib.type_ssfrag config_typ
val from_word_0_thm0 =
from_word_0_to_livesets_0
|> Q.GENL[`c`,`p`,`names`] |> ISPECL args
|> CONV_RULE (RAND_CONV (RAND_CONV (REWR_CONV to_livesets_0_oracle_thm)))
|> CONV_RULE (RAND_CONV
(REWR_CONV from_livesets_def
THENC REWR_CONV LET_THM THENC PAIRED_BETA_CONV))
|> CONV_RULE (RAND_CONV (RAND_CONV
(
RAND_CONV (RAND_CONV (eval)) THENC
RAND_CONV eval THENC
RATOR_CONV (RAND_CONV (REWR_CONV LENGTH_word_prog0)) THENC
REWR_CONV word_to_wordTheory.next_n_oracle_def
)))
|> CONV_RULE (RAND_CONV
(PATH_CONV "rllr" (ONCE_REWRITE_CONV [oracle_def]
THENC RAND_CONV listLib.LENGTH_CONV
THENC eval) THENC
PATH_CONV "r" (REWR_CONV (CONJUNCT1 boolTheory.bool_case_thm)
THENC REWR_CONV take_drop_oracle_lemma)))
|> CONV_RULE (RAND_CONV
(REWR_CONV LET_THM THENC PAIRED_BETA_CONV))
|> CONV_RULE (REPEATC (RAND_CONV (REWR_CONV_BETA LET_THM)))
|> CONV_RULE (PATH_CONV "rr" (REWR_CONV MAP_ZIP_ZIP_lemma))
|> CONV_RULE (PATH_CONV "rrlllrarararaararaa" (PAIRED_BETA_CONV THENC
PATH_CONV"llr"(REWR_CONV word_allocTheory.oracle_colour_ok_def)
))
val tm3 = from_word_0_thm0 |> rconc |> rand
val check_fn = tm3 |> funpow 3 rator |> rand
val check_fn_def = allowing_rebinds (mk_abbrev "check_fn") check_fn;
val temp_defs = (mk_abbrev_name"check_fn") :: temp_defs
fun eval_fn i n (a,b,c) =
let val tm = list_mk_comb(check_fn,[a,b,c])
in eval tm end
val oracle_els =
oracle_def |> rconc |> listSyntax.dest_list |> #1
val word_prog1_els =
word_prog1_def |> rconc |> listSyntax.dest_list |> #1
val word_prog0_els =
word_prog0_def |> rconc |> listSyntax.dest_list |> #1
val lss = zip3
(oracle_els, word_prog1_els, word_prog0_els)
val map3els = time_with_size thms_size "apply colour (par)"
(parl eval_fn) lss
val word_prog1_defs = make_abbrevs "word_prog1_el_" num_progs word_prog1_els []
val temp_defs = List.tabulate(num_progs,(fn i => mk_abbrev_name("word_prog1_el_"^(Int.toString(i+1))))) @ temp_defs
val word_prog1_thm =
word_prog1_def |> CONV_RULE(RAND_CONV(intro_abbrev (List.rev word_prog1_defs)))
val map3els' =
mapi (fn i =>
CONV_RULE(
LAND_CONV(
funpow 3 RATOR_CONV(REWR_CONV(SYM check_fn_def)) THENC
RATOR_CONV(RAND_CONV(REWR_CONV(SYM(List.nth(word_prog1_defs,i))))))))
map3els
local
val next_thm = ref map3els'
val remain = ref num_progs
(*
fun str n =
String.concat[Int.toString n,if n mod 10 = 0 then "\n" else " "]
*)
fun el_conv _ =
case !next_thm of [] => fail() | th :: rest =>
let
val () = next_thm := rest
(*
val () = Lib.say(str (!remain))
*)
val () = remain := !remain-1
in th end
in
val map3_conv = MAP3_CONV el_conv
end
val from_word_0_thm1 =
from_word_0_thm0
|> CONV_RULE(RAND_CONV(
RAND_CONV (
RATOR_CONV(RATOR_CONV(RATOR_CONV(RAND_CONV(REWR_CONV(SYM check_fn_def))))) THENC
RAND_CONV(REWR_CONV word_prog0_def) THENC
RATOR_CONV(RAND_CONV(REWR_CONV word_prog1_thm)) THENC
RATOR_CONV(RATOR_CONV(RAND_CONV(REWR_CONV oracle_def))) THENC
timez "check colour" map3_conv)))
val word_prog2_def = allowing_rebinds (mk_abbrev "word_prog2") (from_word_0_thm1 |> rconc |> rand);
val temp_defs = (mk_abbrev_name"word_prog2") :: temp_defs
val from_word_0_thm1' = from_word_0_thm1
|> CONV_RULE(RAND_CONV(RAND_CONV(REWR_CONV(SYM word_prog2_def))))
val () = computeLib.extend_compset[computeLib.Defs[word_prog2_def]] cs;
(* slow; cannot parallelise easily due to bitmaps accumulator *)
val from_word_thm =
from_word_0_thm1'
|> CONV_RULE(RAND_CONV(
REWR_CONV from_word_def THENC
REWR_CONV LET_THM THENC
RAND_CONV(timez "word_to_stack" eval) THENC
PAIRED_BETA_CONV THENC
REWR_CONV_BETA LET_THM))
(* stack_rawcall *)
val stack_to_lab_thmA =
from_word_thm
|> (CONV_RULE(RAND_CONV(
REWR_CONV from_stack_def THENC
RAND_CONV (RATOR_CONV eval) THENC
REWR_CONV_BETA LET_THM THENC
RATOR_CONV (RAND_CONV (REWR_CONV stack_to_labTheory.compile_def)))))
val stack_rawcall_compile =
(stack_to_lab_thmA |> concl |> rand |> rator |> rand |> rand);
val rawcall_thm = time_with_size (term_size o rand o concl) "stack_rawcall"
eval stack_rawcall_compile;
val stack_prog_def = allowing_rebinds (mk_abbrev "stack_prog") (rawcall_thm |> concl |> rand)
val temp_defs = (mk_abbrev_name"stack_prog") :: temp_defs
val () = computeLib.extend_compset[computeLib.Defs[stack_prog_def]] cs;
val rawcall_thm' =
rawcall_thm |> CONV_RULE (RAND_CONV (K (SYM stack_prog_def)))
val stack_to_lab_thmA' =
stack_to_lab_thmA
|> (CONV_RULE(PATH_CONV "rlrr" (K rawcall_thm') THENC
PATH_CONV "rlr" (REWR_CONV_BETA LET_THM)))
(* stack_alloc *)
val prog_comp_tm =
stack_allocTheory.prog_comp_def
|> SPEC_ALL |> concl |> lhs |> strip_comb |> #1
fun eval_fn i n p =
let val tm = mk_icomb(prog_comp_tm,p)
in eval tm end
val stack_prog_els =
stack_prog_def |> rconc |> listSyntax.dest_list |> #1
val ths = time_with_size thms_size "stack_alloc (par)"
(parl eval_fn) stack_prog_els;
val stack_to_lab_thm0 =
stack_to_lab_thmA'
|> (CONV_RULE(PATH_CONV "rlrr" (
REWR_CONV stack_allocTheory.compile_def THENC
FORK_CONV(eval,
RAND_CONV(REWR_CONV stack_prog_def) THENC
map_ths_conv ths) THENC
listLib.APPEND_CONV)))
val stack_alloc_prog_def =
allowing_rebinds (mk_abbrev "stack_alloc_prog") (stack_to_lab_thm0 |> rconc |> rator |> rand |> rand)
val temp_defs = (mk_abbrev_name"stack_alloc_prog") :: temp_defs
val stack_to_lab_thm1 =
stack_to_lab_thm0
|> CONV_RULE(
RAND_CONV(
RATOR_CONV (
RAND_CONV(
RAND_CONV(REWR_CONV(SYM stack_alloc_prog_def)) THENC
REWR_CONV_BETA LET_THM))))
val tm5 = stack_to_lab_thm1 |> rconc |> rator |> rand
val stack_remove_thm0 =
tm5 |>
timez "expand stack_remove_def"(
(RAND_CONV(
RATOR_CONV(RAND_CONV eval) THENC
funpow 3 RATOR_CONV(RAND_CONV bare_compiler_eval) THENC
funpow 4 RATOR_CONV(RAND_CONV eval) THENC
REWR_CONV stack_removeTheory.compile_def THENC
LAND_CONV eval)))
val tm6 = stack_remove_thm0 |> rconc |> rand |> rand
val prog_comp_n_tm = tm6 |> rator |> rand
fun eval_fn i n p =
let val tm = mk_comb(prog_comp_n_tm,p)
in eval tm end
val stack_alloc_prog_els =
stack_alloc_prog_def |> rconc |> listSyntax.dest_list |> #1
val ths = time_with_size thms_size "stack_remove (par)"
(parl eval_fn) stack_alloc_prog_els;
val stack_remove_thm =
stack_remove_thm0
|> CONV_RULE(RAND_CONV(
RAND_CONV(
RAND_CONV (
RAND_CONV(REWR_CONV stack_alloc_prog_def) THENC
map_ths_conv ths) THENC
listLib.APPEND_CONV)))
val stack_remove_prog_def =
allowing_rebinds (mk_abbrev "stack_remove_prog") (stack_remove_thm |> rconc |> rand);
val temp_defs = (mk_abbrev_name"stack_remove_prog") :: temp_defs
val stack_to_lab_thm2 =
stack_to_lab_thm1
|> CONV_RULE(RAND_CONV(
RATOR_CONV(
RAND_CONV(
REWR_CONV stack_remove_thm THENC
RAND_CONV(REWR_CONV(SYM stack_remove_prog_def)) THENC
REWR_CONV_BETA LET_THM THENC
RAND_CONV(RATOR_CONV(RAND_CONV eval)) THENC
REWR_CONV_BETA LET_THM THENC
RAND_CONV(REWR_CONV stack_namesTheory.compile_def)))))
val tm7 = stack_to_lab_thm2 |> rconc |> rator |> rand |> rand
val prog_comp_nm_tm = tm7 |> rator |> rand
fun eval_fn i n p =
let val tm = mk_comb(prog_comp_nm_tm,p)
in eval tm end
val stack_remove_prog_els =
stack_remove_prog_def |> rconc |> listSyntax.dest_list |> #1
val ths = time_with_size thms_size "stack_names (par)"
(parl eval_fn) stack_remove_prog_els;
val stack_names_thm0 =
tm7
|> (RAND_CONV(REWR_CONV stack_remove_prog_def) THENC
map_ths_conv ths)
val stack_names_prog_def =
allowing_rebinds (mk_abbrev "stack_names_prog") (stack_names_thm0 |> rconc);
val temp_defs = (mk_abbrev_name"stack_names_prog") :: temp_defs
val stack_names_thm = stack_names_thm0
|> CONV_RULE(RAND_CONV(REWR_CONV(SYM stack_names_prog_def)))
val stack_to_lab_thm3 =
stack_to_lab_thm2
|> CONV_RULE(RAND_CONV(RATOR_CONV(RAND_CONV(
RAND_CONV(REWR_CONV stack_names_thm)))))
val tm8 = stack_to_lab_thm3 |> rconc |> rator |> rand
val prog_to_section_tm = tm8 |> rator |> rand
fun eval_fn i n p =
let val tm = mk_comb(prog_to_section_tm,p)
in eval tm end
val stack_names_prog_els =
stack_names_prog_def |> rconc |> listSyntax.dest_list |> #1
val ths = time_with_size thms_size "stack_to_lab (par)"
(parl eval_fn) stack_names_prog_els;
val stack_to_lab_thm4 =
stack_to_lab_thm3
|> CONV_RULE(RAND_CONV(RATOR_CONV(RAND_CONV(
RAND_CONV(REWR_CONV stack_names_prog_def) THENC
map_ths_conv ths))))
val lab_prog_def = allowing_rebinds (mk_abbrev lab_prog_name) (stack_to_lab_thm4 |> rconc |> rator |> rand);
val stack_to_lab_thm =
stack_to_lab_thm4 |>
CONV_RULE(RAND_CONV(RATOR_CONV(RAND_CONV(REWR_CONV(SYM lab_prog_def)))))
val () = List.app delete_binding temp_defs
in stack_to_lab_thm end
fun compile_to_lab data_prog_def to_data_thm lab_prog_name =
let
val cs = compilation_compset()
val () =
computeLib.extend_compset [
computeLib.Extenders [
arm7_targetLib.add_arm7_encode_compset,
arm8_targetLib.add_arm8_encode_compset,
mips_targetLib.add_mips_encode_compset,
riscv_targetLib.add_riscv_encode_compset,
ag32_targetLib.add_ag32_encode_compset,
x64_targetLib.add_x64_encode_compset],
computeLib.Defs [
arm7_backend_config_def, arm7_names_def,
arm8_backend_config_def, arm8_names_def,
mips_backend_config_def, mips_names_def,
riscv_backend_config_def, riscv_names_def,
ag32_backend_config_def, ag32_names_def,
x64_backend_config_def, x64_names_def,
data_prog_def
]
] cs
val eval = computeLib.CBV_CONV cs;
fun parl f = parlist (!num_threads) (!chunk_size) f
val (_,[conf_tm,prog_tm]) =
to_data_thm |> concl |> lhs |> strip_comb
val to_livesets_thm0 =
``to_livesets ^conf_tm ^prog_tm``
|> (REWR_CONV to_livesets_def THENC
RAND_CONV (REWR_CONV to_data_thm) THENC
REWR_CONV LET_THM THENC PAIRED_BETA_CONV THENC
REWR_CONV LET_THM THENC PAIRED_BETA_CONV THENC
REWR_CONV LET_THM THENC BETA_CONV THENC
REWR_CONV_BETA LET_THM THENC
REWR_CONV LET_THM THENC BETA_CONV THENC
REWR_CONV LET_THM THENC PAIRED_BETA_CONV THENC
REWR_CONV LET_THM THENC
PATH_CONV "rlrraraalralrarllr" eval THENC
PATH_CONV"rlrraraalralralralralralrar"
(RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
(FIRST_CONV (map REWR_CONV (CONJUNCTS bool_case_thm)))))
val tm0 = to_livesets_thm0 |> rconc |> rand |> rand
val thm0 = timez "data_to_word" eval tm0;
val tm1 = to_livesets_thm0 |> rconc |> rand
val (args,body) = tm1 |> rator |> rand |> dest_pabs
val word_to_word_fn_def = zdefine`word_to_word_fn ^args = ^body`;
val temp_defs = ["word_to_word_fn_def"];
val word_to_word_fn_eq =
word_to_word_fn_def
|> SPEC_ALL
|> PairRules.PABS args
|> CONV_RULE(LAND_CONV PairRules.PETA_CONV)
val word_to_word_fn = word_to_word_fn_eq|>concl|>lhs
val word_prog = thm0 |> rconc |> listSyntax.dest_list |> #1
val num_progs = length word_prog
fun eval_fn i n p =
let
val tm = mk_comb(word_to_word_fn,p)
val conv = RATOR_CONV(REWR_CONV word_to_word_fn_eq) THENC eval
in
conv tm
end
val ths = time_with_size thms_size "inst,ssa,two-reg (par)"
(parl eval_fn) word_prog;
val thm1 =
tm1
|> (RATOR_CONV(RAND_CONV(REWR_CONV(SYM word_to_word_fn_eq))) THENC
RAND_CONV(REWR_CONV thm0) THENC map_ths_conv ths)
val word_prog0_def = allowing_rebinds (mk_abbrev "word_prog0") (thm1 |> rconc)
val temp_defs = (mk_abbrev_name"word_prog0")::temp_defs;
val thm1' = thm1 |> CONV_RULE(RAND_CONV(REWR_CONV(SYM word_prog0_def)))
val to_livesets_thm1 =
to_livesets_thm0
|> CONV_RULE (RAND_CONV (
RAND_CONV(REWR_CONV thm1') THENC
BETA_CONV THENC
REWR_CONV LET_THM))
val tm2 = to_livesets_thm1 |> rconc |> rand
val (args,body) = tm2 |> rator |> rand |> dest_pabs
val clash_fn_def = zdefine`clash_fn ^args = ^body`;
val temp_defs = (mk_abbrev_name"clash_fn")::temp_defs;
val clash_fn_eq =
clash_fn_def
|> SPEC_ALL
|> PairRules.PABS args
|> CONV_RULE(LAND_CONV PairRules.PETA_CONV)
val clash_fn = clash_fn_eq|>concl|>lhs
val word_prog0 = thm1 |> rconc |> listSyntax.dest_list |> #1
fun eval_fn i n p =
let
val tm = mk_comb(clash_fn,p)
val conv = RATOR_CONV(REWR_CONV clash_fn_eq) THENC eval
in
conv tm
end
val ths = time_with_size thms_size "get_clash (par)"
(parl eval_fn) word_prog0;
val thm2 =
tm2
|> (RATOR_CONV(RAND_CONV(REWR_CONV(SYM clash_fn_eq))) THENC
RAND_CONV(REWR_CONV word_prog0_def) THENC map_ths_conv ths)
val to_livesets_thm =
to_livesets_thm1
|> CONV_RULE (RAND_CONV (
RAND_CONV(REWR_CONV thm2) THENC
BETA_CONV THENC
PATH_CONV"lrlr"eval))
val oracles =
to_livesets_thm
|> rconc |> pairSyntax.dest_pair |> #1
|> time_with_size term_size "external oracle" (reg_allocComputeLib.get_oracle reg_alloc.Irc)
val oracle_def = allowing_rebinds (mk_abbrev "oracle") oracles;
val wc =
``^conf_tm.word_to_word_conf
with col_oracle := oracle``
|> eval |> rconc
val args = to_livesets_thm |> concl |> lhs |> strip_comb |> #2
val word_prog1_def = allowing_rebinds (mk_abbrev "word_prog1") (thm2 |> rconc);
val temp_defs = (mk_abbrev_name"word_prog1") :: temp_defs
val to_livesets_thm' =
to_livesets_thm
|> CONV_RULE(RAND_CONV(
PATH_CONV"lrr"(REWR_CONV(SYM word_prog1_def))))
val to_livesets_oracle_thm =
to_livesets_invariant
|> Q.GEN`wc` |> SPEC wc
|> Q.GENL[`c`,`p`] |> ISPECL args
|> CONV_RULE ((RATOR_CONV eval) THENC BETA_CONV)
|> CONV_RULE(RAND_CONV(
REWR_CONV LET_THM THENC
RAND_CONV(REWR_CONV to_livesets_thm') THENC
PAIRED_BETA_CONV))
val args = to_livesets_oracle_thm |> concl |> lhs |> strip_comb |> #2
val LENGTH_word_prog0 =
listSyntax.mk_length(lhs(concl(word_prog0_def)))
|> (RAND_CONV(REWR_CONV word_prog0_def) THENC
listLib.LENGTH_CONV)
val LENGTH_word_prog1 =
listSyntax.mk_length(lhs(concl(word_prog1_def)))
|> (RAND_CONV(REWR_CONV word_prog1_def) THENC
listLib.LENGTH_CONV)
val oracle_list_def = allowing_rebinds (mk_abbrev "oracle_list") (oracle_def |> rconc |> rand);
val temp_defs = (mk_abbrev_name"oracle_list") :: temp_defs
val LENGTH_oracle_list =
listSyntax.mk_length(lhs(concl(oracle_list_def)))
|> (RAND_CONV(REWR_CONV oracle_list_def) THENC
listLib.LENGTH_CONV)
val LENGTH_oracle =
listSyntax.mk_length(lhs(concl(oracle_def)))
|> (RAND_CONV(REWR_CONV oracle_def) THENC
listLib.LENGTH_CONV)
val take_drop_oracle_lemma =
MATCH_MP backendTheory.TAKE_DROP_PAIR_LEMMA LENGTH_oracle
val MAP_ZIP_ZIP_lemma = MATCH_MP backendTheory.MAP_ZIP_ZIP
(LIST_CONJ [LENGTH_oracle, LENGTH_word_prog1, LENGTH_word_prog0])
val args = to_livesets_oracle_thm |> concl |> lhs |> strip_comb |> #2
val config_typ = type_of (hd args)
val config_ss = bool_ss ++ simpLib.type_ssfrag config_typ
val compile_thm0 =
compile_oracle |> SYM
|> Q.GENL[`c`,`p`] |> ISPECL args
|> CONV_RULE (PATH_CONV "rr" (REWR_CONV to_livesets_oracle_thm))
|> CONV_RULE (RAND_CONV
(REWR_CONV from_livesets_def
THENC REWR_CONV LET_THM THENC PAIRED_BETA_CONV))
|> CONV_RULE (RAND_CONV (RAND_CONV
(
RAND_CONV (RAND_CONV (eval)) THENC
RAND_CONV eval THENC
RATOR_CONV (RAND_CONV (REWR_CONV LENGTH_word_prog0)) THENC
REWR_CONV word_to_wordTheory.next_n_oracle_def
)))
|> CONV_RULE (RAND_CONV
(PATH_CONV "rllr" (ONCE_REWRITE_CONV [oracle_def]
THENC RAND_CONV listLib.LENGTH_CONV
THENC eval) THENC
PATH_CONV "r" (REWR_CONV (CONJUNCT1 boolTheory.bool_case_thm)
THENC REWR_CONV take_drop_oracle_lemma)))
|> CONV_RULE (RAND_CONV
(REWR_CONV LET_THM THENC PAIRED_BETA_CONV))
|> CONV_RULE (REPEATC (RAND_CONV (REWR_CONV_BETA LET_THM)))
|> CONV_RULE (PATH_CONV "rr" (REWR_CONV MAP_ZIP_ZIP_lemma))
|> CONV_RULE (PATH_CONV "rrlllrarararaararaa" (PAIRED_BETA_CONV THENC
PATH_CONV"llr"(REWR_CONV word_allocTheory.oracle_colour_ok_def)
))
val tm3 = compile_thm0 |> rconc |> rand
val check_fn = tm3 |> funpow 3 rator |> rand
val check_fn_def = allowing_rebinds (mk_abbrev "check_fn") check_fn;
val temp_defs = (mk_abbrev_name"check_fn") :: temp_defs
fun eval_fn i n (a,b,c) =
let val tm = list_mk_comb(check_fn,[a,b,c])
in eval tm end
val oracle_els =
oracle_def |> rconc |> listSyntax.dest_list |> #1
val word_prog1_els =
word_prog1_def |> rconc |> listSyntax.dest_list |> #1
val word_prog0_els =
word_prog0_def |> rconc |> listSyntax.dest_list |> #1
val lss = zip3
(oracle_els, word_prog1_els, word_prog0_els)
val map3els = time_with_size thms_size "apply colour (par)"
(parl eval_fn) lss
val word_prog1_defs = make_abbrevs "word_prog1_el_" num_progs word_prog1_els []
val temp_defs = List.tabulate(num_progs,(fn i => mk_abbrev_name("word_prog1_el_"^(Int.toString(i+1))))) @ temp_defs
val word_prog1_thm =
word_prog1_def |> CONV_RULE(RAND_CONV(intro_abbrev (List.rev word_prog1_defs)))
val map3els' =
mapi (fn i =>
CONV_RULE(
LAND_CONV(
funpow 3 RATOR_CONV(REWR_CONV(SYM check_fn_def)) THENC
RATOR_CONV(RAND_CONV(REWR_CONV(SYM(List.nth(word_prog1_defs,i))))))))
map3els
local
val next_thm = ref map3els'
val remain = ref num_progs
(*
fun str n =
String.concat[Int.toString n,if n mod 10 = 0 then "\n" else " "]
*)
fun el_conv _ =
case !next_thm of [] => fail() | th :: rest =>
let
val () = next_thm := rest
(*
val () = Lib.say(str (!remain))
*)
val () = remain := !remain-1
in th end
in