forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ml_progScript.sml
1171 lines (1039 loc) · 38.7 KB
/
ml_progScript.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
(*
Definitions and theorems supporting ml_progLib, which constructs a
CakeML program and its semantic environment.
*)
open preamble
open astTheory libTheory semanticPrimitivesTheory evaluateTheory
semanticPrimitivesPropsTheory evaluatePropsTheory;
open mlstringTheory integerTheory;
open namespaceTheory;
open alist_treeTheory;
val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
val _ = new_theory "ml_prog";
(* --- env operators --- *)
(* Functions write, write_cons, write_mod, empty_env, merge_env should
never be expanded by EVAL and are therefore defined using
zDefine. These should never be exanded by EVAL because that would
cause very slow appends. *)
val write_def = zDefine `
write name v (env:v sem_env) = env with v := nsBind name v env.v`;
val write_cons_def = zDefine `
write_cons n d (env:v sem_env) =
(env with c := nsAppend (nsSing n d) env.c)`
val empty_env_def = zDefine `
(empty_env:v sem_env) = <| v := nsEmpty ; c:= nsEmpty|>`;
val write_mod_def = zDefine `
write_mod mn (env:v sem_env) env2 =
env2 with <|
c := nsAppend (nsLift mn env.c) env2.c
; v := nsAppend (nsLift mn env.v) env2.v |>`
val merge_env_def = zDefine `
merge_env (env2:v sem_env) env1 =
<| v := nsAppend env2.v env1.v
; c := nsAppend env2.c env1.c|>`
(* the components of nsLookup are 'nicer' partial functions *)
val nsLookup_Short_def = zDefine `
nsLookup_Short ns nm = nsLookup ns (Short nm)`;
val nsLookup_Mod1_def = zDefine `
nsLookup_Mod1 ns = (case ns of Bind _ ms => ALOOKUP ms)`;
Theorem nsLookup_eq:
nsLookup ns (Short nm) = nsLookup_Short ns nm /\
nsLookup ns (Long mnm id) = (case nsLookup_Mod1 ns mnm of
NONE => NONE | SOME ns2 => nsLookup ns2 id)
Proof
fs [nsLookup_Short_def]
\\ Cases_on `ns`
\\ fs[nsLookup_Mod1_def, nsLookup_def]
QED
(* base facts about the partial functions *)
Theorem option_choice_f_apply:
option_choice_f f g x = OPTION_CHOICE (f x) (g x)
Proof
fs [option_choice_f_def]
QED
Theorem nsLookup_Short_Bind:
nsLookup_Short (Bind ss ms) = ALOOKUP ss
Proof
fs [nsLookup_Short_def, nsLookup_def, FUN_EQ_THM]
QED
Theorem nsLookup_Short_nsAppend:
nsLookup_Short (nsAppend ns1 ns2)
= option_choice_f (nsLookup_Short ns1) (nsLookup_Short ns2)
Proof
Cases_on `ns1` \\ Cases_on `ns2`
\\ fs [nsLookup_Short_Bind, nsAppend_def,
alookup_append_option_choice_f]
QED
Theorem nsLookup_Mod1_Bind:
nsLookup_Mod1 (Bind ss ms) nm = ALOOKUP ms nm
Proof
fs [nsLookup_Mod1_def]
QED
Theorem nsLookup_Mod1_nsAppend:
nsLookup_Mod1 (nsAppend ns1 ns2)
= option_choice_f (nsLookup_Mod1 ns1) (nsLookup_Mod1 ns2)
Proof
Cases_on `ns1` \\ Cases_on `ns2`
\\ fs [nsLookup_Mod1_def, nsAppend_def,
alookup_append_option_choice_f]
QED
Theorem nsLookup_Short_nsLift:
nsLookup_Short (nsLift mnm ns) = ALOOKUP []
Proof
Cases_on `ns` \\ fs [nsLift_def, nsLookup_Short_Bind]
QED
Theorem nsLookup_Mod1_nsLift:
nsLookup_Mod1 (nsLift mnm ns) = ALOOKUP [(mnm, ns)]
Proof
Cases_on `ns` \\ fs [nsLift_def, nsLookup_Mod1_def]
QED
Theorem nsLookup_pf_nsBind:
nsLookup_Short (nsBind n v ns)
= option_choice_f (ALOOKUP [(n, v)]) (nsLookup_Short ns) /\
nsLookup_Mod1 (nsBind n v ns) = nsLookup_Mod1 ns
Proof
Cases_on `ns`
\\ fs [nsLookup_Short_def,nsLookup_Mod1_def, FUN_EQ_THM,
write_def,nsLookup_def,nsBind_def,option_choice_f_def]
\\ rpt strip_tac
\\ fs [] \\ CASE_TAC \\ fs []
QED
(* equalities on these partial functions for the various env operators *)
Theorem nsLookup_write_eqs:
nsLookup_Short ((write n v env).c) = nsLookup_Short env.c /\
nsLookup_Mod1 ((write n v env).c) = nsLookup_Mod1 env.c /\
nsLookup_Mod1 ((write n v env).v) = nsLookup_Mod1 env.v /\
nsLookup_Short ((write n v env).v) = option_choice_f (ALOOKUP [(n, v)])
(nsLookup_Short env.v)
Proof
fs[write_def, nsLookup_pf_nsBind]
QED
Theorem nsLookup_write_cons_eqs:
nsLookup_Short ((write_cons n v env).v) = nsLookup_Short env.v /\
nsLookup_Mod1 ((write_cons n v env).v) = nsLookup_Mod1 env.v /\
nsLookup_Mod1 ((write_cons n v env).c) = nsLookup_Mod1 env.c /\
nsLookup_Short ((write_cons n v env).c) = option_choice_f (ALOOKUP [(n, v)])
(nsLookup_Short env.c)
Proof
fs[write_cons_def, nsLookup_pf_nsBind]
QED
Theorem nsLookup_merge_env_eqs:
nsLookup_Short ((merge_env env env2).v)
= option_choice_f (nsLookup_Short env.v) (nsLookup_Short env2.v) /\
nsLookup_Mod1 ((merge_env env env2).v)
= option_choice_f (nsLookup_Mod1 env.v) (nsLookup_Mod1 env2.v) /\
nsLookup_Short ((merge_env env env2).c)
= option_choice_f (nsLookup_Short env.c) (nsLookup_Short env2.c) /\
nsLookup_Mod1 ((merge_env env env2).c)
= option_choice_f (nsLookup_Mod1 env.c) (nsLookup_Mod1 env2.c)
Proof
fs[merge_env_def, nsLookup_Short_nsAppend, nsLookup_Mod1_nsAppend]
QED
Theorem nsLookup_write_mod_eqs:
nsLookup_Short ((write_mod mnm env env2).v) = nsLookup_Short env2.v /\
nsLookup_Mod1 ((write_mod mnm env env2).v)
= option_choice_f (ALOOKUP [(mnm, env.v)]) (nsLookup_Mod1 env2.v) /\
nsLookup_Short ((write_mod mnm env env2).c) = nsLookup_Short env2.c /\
nsLookup_Mod1 ((write_mod mnm env env2).c)
= option_choice_f (ALOOKUP [(mnm, env.c)]) (nsLookup_Mod1 env2.c)
Proof
fs[write_mod_def, nsLookup_Short_nsAppend, nsLookup_Mod1_nsAppend,
nsLookup_Short_nsLift, nsLookup_Mod1_nsLift,
alookup_empty_option_choice_f]
QED
Theorem nsLookup_empty_eqs:
nsLookup_Short empty_env.v = ALOOKUP [] /\
nsLookup_Mod1 empty_env.v = ALOOKUP [] /\
nsLookup_Short empty_env.c = ALOOKUP [] /\
nsLookup_Mod1 empty_env.c = ALOOKUP []
Proof
fs[empty_env_def, nsEmpty_def, nsLookup_Short_Bind, nsLookup_Mod1_def]
QED
(* nonsense theorem instantiated when env's are defined *)
Theorem nsLookup_eq_format:
!env:v sem_env.
(nsLookup_Short env.v = nsLookup_Short env.v) /\
(nsLookup_Short env.c = nsLookup_Short env.c) /\
(nsLookup_Mod1 env.v = nsLookup_Mod1 env.v) /\
(nsLookup_Mod1 env.c = nsLookup_Mod1 env.c)
Proof
rewrite_tac []
QED
(* some shorthands that are allowed to EVAL are below *)
val write_rec_def = Define `
write_rec funs env1 env =
FOLDR (\f env. write (FST f) (Recclosure env1 funs (FST f)) env) env funs`;
Theorem write_rec_thm:
write_rec funs env1 env =
env with v := build_rec_env funs env1 env.v
Proof
fs [write_rec_def,build_rec_env_def]
\\ qspec_tac (`Recclosure env1 funs`,`hh`)
\\ qspec_tac (`env`,`env`)
\\ Induct_on `funs` \\ fs [FORALL_PROD]
\\ fs [write_def]
QED
val write_conses_def = Define `
write_conses [] env = env /\
write_conses ((n,y)::xs) env =
write_cons n y (write_conses xs env)`;
val write_tdefs_def = Define `
write_tdefs n [] env = env /\
write_tdefs n ((x,_,condefs)::tds) env =
write_tdefs (n+1) tds (write_conses (REVERSE (build_constrs n condefs)) env)`
val write_conses_v = prove(
``!xs env. (write_conses xs env).v = env.v``,
Induct \\ fs [write_conses_def,FORALL_PROD,write_cons_def]);
val write_tdefs_lemma = prove(
``!tds env n.
write_tdefs n tds env =
merge_env <|v := nsEmpty; c := build_tdefs n tds|> env``,
Induct \\ fs [write_tdefs_def,merge_env_def,build_tdefs_def,FORALL_PROD]
\\ rw [write_conses_v]
\\ rewrite_tac [GSYM namespacePropsTheory.nsAppend_assoc]
\\ AP_TERM_TAC
\\ Q.SPEC_TAC (`REVERSE (build_constrs n p_2)`,`xs`)
\\ Induct \\ fs [write_conses_def,FORALL_PROD,write_cons_def]);
Theorem write_tdefs_thm:
write_tdefs n tds empty_env =
<|v := nsEmpty; c := build_tdefs n tds|>
Proof
fs [write_tdefs_lemma,empty_env_def,merge_env_def]
QED
val merge_env_write_conses = prove(
``!xs env. merge_env (write_conses xs env1) env2 =
write_conses xs (merge_env env1 env2)``,
Induct \\ fs [write_conses_def,FORALL_PROD]
\\ fs [write_cons_def,merge_env_def,sem_env_component_equality]);
val merge_env_write_tdefs = prove(
``!tds n env1 env2.
merge_env (write_tdefs n tds env1) env2 =
write_tdefs n tds (merge_env env1 env2)``,
Induct \\ fs [write_tdefs_def,FORALL_PROD,merge_env_write_conses]);
(* it's not clear if these are still needed, but ml_progComputeLib and
cfTacticsLib want them to be present. *)
Theorem nsLookup_nsAppend_Short[compute]:
(nsLookup (nsAppend e1 e2) (Short id) =
case nsLookup e1 (Short id) of
NONE =>
nsLookup e2 (Short id)
| SOME v => SOME v)
Proof
every_case_tac>>
Cases_on`nsLookup e2(Short id)`>>
fs[namespacePropsTheory.nsLookup_nsAppend_some,
namespacePropsTheory.nsLookup_nsAppend_none,id_to_mods_def]
QED
Theorem write_simp[compute]:
(write n v env).c = env.c /\
nsLookup (write n v env).v (Short q) =
if n = q then SOME v else nsLookup env.v (Short q)
Proof
IF_CASES_TAC>>fs[write_def,namespacePropsTheory.nsLookup_nsBind]
QED
Theorem write_cons_simp[compute]:
(write_cons n v env).v = env.v /\
nsLookup (write_cons n v env).c (Short q) =
if n = q then SOME v else nsLookup env.c (Short q)
Proof
IF_CASES_TAC>>fs[write_cons_def,namespacePropsTheory.nsLookup_nsBind]
QED
Theorem write_mod_simp[compute]:
(nsLookup (write_mod mn env env2).v (Short q) =
nsLookup env2.v (Short q)) ∧
(nsLookup (write_mod mn env env2).c (Short c) =
nsLookup env2.c (Short c)) ∧
(nsLookup (write_mod mn env env2).v (Long mn' r) =
if mn = mn' then nsLookup env.v r
else nsLookup env2.v (Long mn' r)) ∧
(nsLookup (write_mod mn env env2).c (Long mn' s) =
if mn = mn' then nsLookup env.c s
else nsLookup env2.c (Long mn' s))
Proof
rw[write_mod_def]
QED
Theorem empty_simp[compute]:
nsLookup empty_env.v q = NONE /\
nsLookup empty_env.c q = NONE
Proof
fs [empty_env_def]
QED
(* the components of nsLookup are 'nicer' partial functions *)
(* --- declarations --- *)
val Decls_def = Define `
Decls env s1 ds env2 s2 <=>
s1.clock = s2.clock /\
?ck1 ck2. evaluate_decs (s1 with clock := ck1) env ds =
(s2 with clock := ck2, Rval env2)`;
Theorem Decls_Dtype:
!env s tds env2 s2 locs.
Decls env s [Dtype locs tds] env2 s2 <=>
EVERY check_dup_ctors tds /\
s2 = s with <| next_type_stamp := (s.next_type_stamp + LENGTH tds) |> /\
env2 = write_tdefs s.next_type_stamp tds empty_env
Proof
SIMP_TAC std_ss [Decls_def,evaluate_decs_def]
\\ rw [] \\ eq_tac \\ rw [] \\ fs [bool_case_eq]
\\ rveq \\ fs [state_component_equality,write_tdefs_thm]
QED
Theorem Decls_Dexn:
!env s n l env2 s2 locs.
Decls env s [Dexn locs n l] env2 s2 <=>
s2 = s with <| next_exn_stamp := (s.next_exn_stamp + 1) |> /\
env2 = write_cons n (LENGTH l, ExnStamp s.next_exn_stamp) empty_env
Proof
SIMP_TAC std_ss [Decls_def,evaluate_decs_def,write_cons_def]
\\ rw [] \\ eq_tac \\ rw [] \\ fs [bool_case_eq]
\\ rveq \\ fs [state_component_equality,write_tdefs_thm]
\\ fs [nsBind_def,nsEmpty_def,nsSing_def,empty_env_def]
QED
Theorem Decls_Dtabbrev:
!env s x y z env2 s2 locs.
Decls env s [Dtabbrev locs x y z] env2 s2 <=>
s2 = s ∧ env2 = empty_env
Proof
fs [Decls_def,evaluate_decs_def]
\\ rw [] \\ eq_tac \\ rw [] \\ fs [bool_case_eq]
\\ rveq \\ fs [state_component_equality,empty_env_def]
QED
val eval_rel_def = Define `
eval_rel s1 env e s2 x <=>
s1.clock = s2.clock /\
?ck1 ck2.
evaluate (s1 with clock := ck1) env [e] =
(s2 with clock := ck2,Rval [x])`
Theorem eval_rel_alt:
eval_rel s1 env e s2 x <=>
s2.clock = s1.clock ∧
∃ck. evaluate (s1 with clock := ck) env [e] = (s2,Rval [x])
Proof
reverse eq_tac \\ rw [] \\ fs [eval_rel_def]
THEN1 (qexists_tac `ck` \\ fs [state_component_equality])
\\ drule evaluatePropsTheory.evaluate_set_clock \\ fs []
\\ disch_then (qspec_then `s2.clock` strip_assume_tac)
\\ rename [`evaluate (s1 with clock := ck) env [e]`]
\\ qexists_tac `ck` \\ fs [state_component_equality]
QED
val eval_list_rel_def = Define `
eval_list_rel s1 env e s2 x <=>
s1.clock = s2.clock /\
?ck1 ck2.
evaluate (s1 with clock := ck1) env e =
(s2 with clock := ck2,Rval x)`
val eval_match_rel_def = Define `
eval_match_rel s1 env v pats err_v s2 x <=>
s1.clock = s2.clock /\
?ck1 ck2.
evaluate_match
(s1 with clock := ck1) env v pats err_v =
(s2 with clock := ck2,Rval [x])`
(* Delays the write *)
Theorem Decls_Dlet:
!env s1 v e s2 env2 locs.
Decls env s1 [Dlet locs (Pvar v) e] env2 s2 <=>
?x. eval_rel s1 env e s2 x /\ (env2 = write v x empty_env) /\
every_exp (one_con_check env.c) e
Proof
simp [Decls_def,evaluate_decs_def,eval_rel_def]
\\ rw [] \\ eq_tac \\ rw [] \\ fs [bool_case_eq]
THEN1
(FULL_CASE_TAC
\\ Cases_on `r` \\ fs [pat_bindings_def,ALL_DISTINCT,MEM,
pmatch_def,combine_dec_result_def] \\ rveq \\ fs []
\\ imp_res_tac evaluate_sing \\ fs [] \\ rveq
\\ fs [write_def,empty_env_def] \\ asm_exists_tac \\ fs [])
\\ fs [pat_bindings_def,ALL_DISTINCT,MEM,
pmatch_def,combine_dec_result_def]
\\ qexists_tac `ck1` \\ qexists_tac `ck2`
\\ fs [write_def,empty_env_def]
QED
val FOLDR_LEMMA = Q.prove(
`!xs ys. FOLDR (\(x1,x2,x3) x4. (x1, f x1 x2 x3) :: x4) [] xs ++ ys =
FOLDR (\(x1,x2,x3) x4. (x1, f x1 x2 x3) :: x4) ys xs`,
Induct \\ FULL_SIMP_TAC (srw_ss()) [FORALL_PROD]);
(* Delays the write in build_rec_env *)
Theorem Decls_Dletrec:
!env s1 funs s2 env2 locs.
Decls env s1 [Dletrec locs funs] env2 s2 <=>
(s2 = s1) /\
ALL_DISTINCT (MAP (\(x,y,z). x) funs) /\
EVERY (λ(f,n,e). every_exp (one_con_check env.c) e) funs /\
(env2 = write_rec funs env empty_env)
Proof
simp [Decls_def,evaluate_decs_def,bool_case_eq,PULL_EXISTS]
\\ rw [] \\ eq_tac \\ rw [] \\ fs []
\\ fs [state_component_equality,write_rec_def]
\\ fs[write_def,write_rec_thm,empty_env_def,build_rec_env_def]
\\ rpt (pop_assum kall_tac)
\\ qspec_tac (`Recclosure env funs`,`xx`)
\\ qspec_tac (`nsEmpty:env_val`,`nn`)
\\ Induct_on `funs` \\ fs [FORALL_PROD]
\\ pop_assum (assume_tac o GSYM) \\ fs []
QED
Theorem Decls_Dmod:
Decls env1 s1 [Dmod mn ds] env2 s2 <=>
?s env.
Decls env1 s1 ds env s /\ s2 = s /\
env2 = write_mod mn env empty_env
Proof
fs [Decls_def,Decls_def,evaluate_decs_def,PULL_EXISTS,
combine_dec_result_def,write_mod_def,empty_env_def]
\\ rw [] \\ eq_tac \\ rw [] \\ fs [pair_case_eq,result_case_eq]
\\ rveq \\ fs [] \\ asm_exists_tac \\ fs []
QED
Theorem Decls_Dlocal:
Decls env st lds env2 st2
==> Decls (merge_env env2 env) st2 ds env3 st3
==> Decls env st [Dlocal lds ds] env3 st3
Proof
fs [Decls_def,evaluate_decs_def,extend_dec_env_def,merge_env_def]
\\ rw [pair_case_eq, result_case_eq]
\\ imp_res_tac evaluate_decs_set_clock
\\ fs [] \\ metis_tac []
QED
Theorem Decls_Denv:
∀env s1 v s2 env2.
Decls env s1 [Denv v] env2 s2 ⇔
∃env1 es.
declare_env s1.eval_state env = SOME (env1, es) ∧
s2 = s1 with eval_state := es ∧
env2 = write v env1 empty_env
Proof
rw[Decls_def, evaluate_decs_def]
\\ TOP_CASE_TAC
\\ PairCases_on`x`
\\ simp[write_def,empty_env_def,state_component_equality]
\\ rw[nsEmpty_def, nsSing_def, nsBind_def]
\\ rw[EQ_IMP_THM]
QED
Theorem Decls_NIL:
!env s n l env2 s2.
Decls env s [] env2 s2 <=>
s2 = s ∧ env2 = empty_env
Proof
fs [Decls_def,evaluate_decs_def,state_component_equality,empty_env_def]
\\ rw [] \\ eq_tac \\ rw []
QED
Theorem Decls_CONS:
!s1 s3 env1 d ds1 ds2 env3.
Decls env1 s1 (d::ds2) env3 s3 =
?envA envB s2.
Decls env1 s1 [d] envA s2 /\
Decls (merge_env envA env1) s2 ds2 envB s3 /\
env3 = merge_env envB envA
Proof
rw[Decls_def,PULL_EXISTS,evaluate_decs_def]
\\ reverse (rw[EQ_IMP_THM]) \\ fs []
THEN1
(once_rewrite_tac [evaluate_decs_cons]
\\ imp_res_tac evaluate_decs_add_to_clock \\ fs []
\\ first_x_assum (qspec_then `ck1'` assume_tac)
\\ qexists_tac `ck1+ck1'` \\ fs []
\\ fs [merge_env_def,extend_dec_env_def,combine_dec_result_def]
\\ fs [state_component_equality])
\\ pop_assum mp_tac
\\ once_rewrite_tac [evaluate_decs_cons]
\\ fs [pair_case_eq,result_case_eq] \\ rw [] \\ fs [PULL_EXISTS]
\\ Cases_on `r` \\ fs [combine_dec_result_def]
\\ rveq \\ fs []
\\ qexists_tac `env1'` \\ fs []
\\ qexists_tac `a` \\ fs []
\\ qexists_tac `s1' with clock := s3.clock` \\ fs [merge_env_def]
\\ qexists_tac `ck1` \\ fs [state_component_equality]
\\ qexists_tac `s1'.clock` \\ fs [state_component_equality]
\\ `(s1' with clock := s1'.clock) = s1'` by fs [state_component_equality]
\\ fs [extend_dec_env_def]
\\ fs [state_component_equality]
QED
Theorem merge_env_empty_env:
merge_env env empty_env = env /\
merge_env empty_env env = env
Proof
rw [merge_env_def,empty_env_def]
QED
Theorem merge_env_assoc:
merge_env env1 (merge_env env2 env3) = merge_env (merge_env env1 env2) env3
Proof
fs [merge_env_def]
QED
Theorem Decls_APPEND:
!s1 s3 env1 ds1 ds2 env3.
Decls env1 s1 (ds1 ++ ds2) env3 s3 =
?envA envB s2.
Decls env1 s1 ds1 envA s2 /\
Decls (merge_env envA env1) s2 ds2 envB s3 /\
env3 = merge_env envB envA
Proof
Induct_on `ds1` \\ fs [APPEND,Decls_NIL,merge_env_empty_env]
\\ once_rewrite_tac [Decls_CONS]
\\ fs [PULL_EXISTS,merge_env_assoc] \\ metis_tac []
QED
Theorem Decls_SNOC:
!s1 s3 env1 ds1 d env3.
Decls env1 s1 (SNOC d ds1) env3 s3 =
?envA envB s2.
Decls env1 s1 ds1 envA s2 /\
Decls (merge_env envA env1) s2 [d] envB s3 /\
env3 = merge_env envB envA
Proof
METIS_TAC [SNOC_APPEND, Decls_APPEND]
QED
Theorem Decls_set_eval_state:
Decls env1 s1 ds env2 s2 ∧ s1.eval_state = NONE ⇒
∀es.
Decls env1 (s1 with eval_state := es) ds env2
(s2 with eval_state := es)
Proof
rw [Decls_def]
\\ drule_then (qspec_then ‘es’ assume_tac) (CONJUNCTS eval_no_eval_simulation |> last)
\\ gvs []
\\ pop_assum $ irule_at Any
QED
(* The translator and CF tools use the following definition of ML_code
to build (and verify) an ML program within the logic. The goal is to
prove 'Decls' of the completed list of declarations. The program is
constructed one statement at a time, with facts about the resulting
environment built over time. There is a list of currently open blocks
(e.g. struct and local constructs) so that the contents of modules and
local objects can also be built up one statement at a time.
*)
Definition ML_code_env_def:
(ML_code_env env [] = env) ∧
(ML_code_env env ((comm, st, decls, res_env) :: bls)
= merge_env res_env (ML_code_env env bls))
End
Definition ML_code_def:
(ML_code env [] res_st <=> T) ∧
(ML_code env (((comment : string # string), st, decls, res_env) :: bls) res_st <=>
ML_code env bls st ∧
Decls (ML_code_env env bls) st decls res_env res_st)
End
(* retreive the Decls from a toplevel ML_code *)
Theorem ML_code_Decls:
ML_code env1 [(comm, st1, prog, env2)] st2 ==>
Decls env1 st1 prog env2 st2
Proof
fs [ML_code_def, ML_code_env_def]
QED
(* an empty program *)
local open primSemEnvTheory in
local
val init_env_tm =
``SND (THE (prim_sem_env (ARB:unit ffi_state)))``
|> (SIMP_CONV std_ss [primSemEnvTheory.prim_sem_env_eq] THENC EVAL)
|> concl |> rand
val init_state_tm =
``FST(THE (prim_sem_env (ffi:'ffi ffi_state)))``
|> (SIMP_CONV std_ss [primSemEnvTheory.prim_sem_env_eq] THENC EVAL)
|> concl |> rand
in
(* init_env_def should not be unpacked by EVAL. Queries will be handled
by the nsLookup_conv apparatus, which will use the pfun_eqs thm below. *)
val init_env_def = zDefine `
init_env = ^init_env_tm`;
val init_state_def = Define `
init_state ffi = ^init_state_tm`;
end
Theorem init_state_env_thm:
THE (prim_sem_env ffi) = (init_state ffi,init_env)
Proof
rewrite_tac[prim_sem_env_eq,THE_DEF,init_state_def,init_env_def]
QED
val nsLookup_init_env_pfun_eqs = save_thm("nsLookup_init_env_pfun_eqs",
[``nsLookup_Short init_env.c``, ``nsLookup_Short init_env.v``,
``nsLookup_Mod1 init_env.c``, ``nsLookup_Mod1 init_env.v``]
|> map (SIMP_CONV bool_ss
[init_env_def, nsLookup_Short_Bind, nsLookup_Mod1_def,
namespace_case_def, sem_env_accfupds, K_DEF])
|> LIST_CONJ);
end
Theorem ML_code_NIL:
ML_code init_env [(("Toplevel", ""), init_state ffi, [], empty_env)]
(init_state ffi)
Proof
fs [ML_code_def,Decls_NIL]
QED
(* opening and closing of modules *)
Theorem ML_code_new_block:
!comm2. ML_code inp_env ((comm, st, decls, env) :: bls) st2 ==>
let env2 = ML_code_env inp_env ((comm, st, decls, env) :: bls) in
ML_code inp_env ((comm2, st2, [], empty_env)
:: (comm, st, decls, env) :: bls) st2
Proof
fs [ML_code_def] \\ rw [Decls_NIL] \\ EVAL_TAC
QED
Theorem ML_code_close_module:
ML_code inp_env ((("Module", mn), m_i_st, m_decls, m_env)
:: (comm, st, decls, env) :: bls) st2
==> let env2 = write_mod mn m_env env
in ML_code inp_env ((comm, st, SNOC (Dmod mn m_decls) decls,
env2) :: bls) st2
Proof
rw [ML_code_def, ML_code_env_def]
\\ fs [SNOC_APPEND,Decls_APPEND]
\\ asm_exists_tac \\ fs [Decls_Dmod,PULL_EXISTS]
\\ asm_exists_tac
\\ fs [write_mod_def,merge_env_def,empty_env_def]
QED
Theorem ML_code_close_local:
ML_code inp_env ((("Local", ln2), l2_i_st, l2_decls, l2_env)
:: (("Local", ln1), l1_i_st, l1_decls, l1_env)
:: (comm, st, decls, env) :: bls) st2
==> let env2 = merge_env l2_env env
in ML_code inp_env ((comm, st, SNOC (Dlocal l1_decls l2_decls) decls,
env2) :: bls) st2
Proof
rw [ML_code_def, ML_code_env_def]
\\ fs [SNOC_APPEND,Decls_APPEND] \\ metis_tac [Decls_Dlocal]
QED
(* appending a Dtype *)
Theorem ML_code_Dtype:
!tds locs. ML_code inp_env ((comm, s1, prog, env2) :: bls) s2 ==>
EVERY check_dup_ctors tds ==>
let nts = s2.next_type_stamp in
let s3 = (s2 with next_type_stamp := nts + LENGTH tds) in
let env3 = write_tdefs nts tds env2 in
ML_code inp_env ((comm, s1, SNOC (Dtype locs tds) prog, env3) :: bls) s3
Proof
fs [ML_code_def,SNOC_APPEND,Decls_APPEND,Decls_Dtype,merge_env_empty_env]
\\ rw [] \\ rpt (asm_exists_tac \\ fs [])
\\ fs [merge_env_write_tdefs] \\ AP_TERM_TAC
\\ fs [merge_env_def,empty_env_def,sem_env_component_equality]
QED
(* appending a Dexn *)
Theorem ML_code_Dexn:
!n l locs. ML_code inp_env ((comm, s1, prog, env2) :: bls) s2 ==>
let nes = s2.next_exn_stamp in
let s3 = s2 with next_exn_stamp := nes + 1 in
let env3 = write_cons n (LENGTH l,ExnStamp nes) env2 in
ML_code inp_env ((comm, s1, SNOC (Dexn locs n l) prog, env3) :: bls) s3
Proof
fs [ML_code_def,SNOC_APPEND,Decls_APPEND,Decls_Dexn,merge_env_empty_env]
\\ rw [] \\ rpt (asm_exists_tac \\ fs [])
\\ fs [write_cons_def,merge_env_def,empty_env_def,sem_env_component_equality]
QED
(* appending a Dtabbrev *)
Theorem ML_code_Dtabbrev:
!x y z locs. ML_code inp_env ((comm, s1, prog, env2) :: bls) s2 ==>
ML_code inp_env ((comm, s1, SNOC (Dtabbrev locs x y z) prog, env2) :: bls)
s2
Proof
fs [ML_code_def,SNOC_APPEND,Decls_APPEND,Decls_Dtabbrev,merge_env_empty_env]
QED
(* appending a Letrec *)
val build_rec_env_APPEND = Q.prove(
`nsAppend (build_rec_env funs cl_env nsEmpty) add_to_env =
build_rec_env funs cl_env add_to_env`,
fs [build_rec_env_def] \\ qspec_tac (`Recclosure cl_env funs`,`xxx`)
\\ qspec_tac (`add_to_env`,`xs`)
\\ Induct_on `funs` \\ fs [FORALL_PROD]);
Theorem ML_code_Dletrec:
!fns locs. ML_code env0 ((comm, s1, prog, env2) :: bls) s2 ==>
ALL_DISTINCT (MAP (λ(x,y,z). x) fns) ==>
EVERY
(λ(f,n,e).
every_exp (one_con_check (merge_env env2 (ML_code_env env0 bls)).c) e) fns ==>
let code_env = ML_code_env env0 ((comm, s1, prog, env2) :: bls) in
let env3 = write_rec fns code_env env2 in
ML_code env0 ((comm, s1, SNOC (Dletrec locs fns) prog, env3) :: bls) s2
Proof
fs [ML_code_def,SNOC_APPEND,Decls_APPEND,Decls_Dletrec,ML_code_env_def]
\\ rw [] \\ asm_exists_tac
\\ fs [merge_env_def,write_rec_thm,empty_env_def,sem_env_component_equality]
\\ fs [build_rec_env_APPEND]
QED
(* appending a Let *)
Theorem ML_code_Dlet_var:
∀cenv e s3 x n locs. ML_code env0 ((comm, s1, prog, env1) :: bls) s2 ==>
eval_rel s2 cenv e s3 x ==>
cenv = ML_code_env env0 ((comm, s1, prog, env1) :: bls) ==>
every_exp (one_con_check (merge_env env1 (ML_code_env env0 bls)).c) e ==>
let env2 = write n x env1 in let s3_abbrev = s3 in
ML_code env0 ((comm, s1, SNOC (Dlet locs (Pvar n) e) prog, env2)
:: bls) s3_abbrev
Proof
fs [ML_code_def,ML_code_env_def,SNOC_APPEND,Decls_APPEND,Decls_Dlet]
\\ rw [] \\ asm_exists_tac \\ fs [PULL_EXISTS]
\\ fs [write_def,merge_env_def,empty_env_def,sem_env_component_equality]
QED
Theorem ML_code_Dlet_var_lit:
∀loc name l. ML_code env0 ((comm, s1, prog, env1)::bls) s2 ⇒
let env2 = write name (Litv l) env1 in let s3_abbrev = s2 in
ML_code env0 ((comm,s1,SNOC (Dlet loc (Pvar name) (Lit l)) prog,env2)::bls) s3_abbrev
Proof
rpt strip_tac
\\ irule ML_code_Dlet_var \\ fs []
\\ pop_assum $ irule_at Any
\\ fs [eval_rel_def,evaluateTheory.evaluate_def]
\\ fs [semanticPrimitivesTheory.state_component_equality]
QED
Theorem ML_code_Dlet_Fun:
∀n v e locs. ML_code env0 ((comm, s1, prog, env1) :: bls) s2 ==>
every_exp (one_con_check (merge_env env1 (ML_code_env env0 bls)).c) e ==>
let code_env = ML_code_env env0 ((comm, s1, prog, env1) :: bls) in
let v_abbrev = Closure code_env v e in
let env2 = write n v_abbrev env1 in
ML_code env0 ((comm, s1, SNOC (Dlet locs (Pvar n) (Fun v e)) prog,
env2) :: bls) s2
Proof
rw [] \\ imp_res_tac ML_code_Dlet_var
\\ fs [evaluate_def,state_component_equality,eval_rel_def]
QED
Theorem ML_code_Dlet_Var_Var:
∀n vname locs. ML_code env0 ((comm, s1, prog, env1) :: bls) s2 ==>
let cenv = ML_code_env env0 ((comm, s1, prog, env1) :: bls) in
∀x. nsLookup cenv.v vname = SOME x ==>
let env2 = write n x env1 in
ML_code env0 ((comm, s1, SNOC (Dlet locs (Pvar n) (Var vname)) prog, env2)
:: bls) s2
Proof
rw []
\\ irule (SIMP_RULE std_ss [LET_THM] ML_code_Dlet_var) \\ fs []
\\ first_x_assum $ irule_at $ Pos hd
\\ fs [eval_rel_def,evaluate_def,state_component_equality]
QED
Theorem ML_code_Dlet_Var_Ref_Var:
∀n vname locs. ML_code env0 ((comm, s1, prog, env1) :: bls) s2 ==>
let cenv = ML_code_env env0 ((comm, s1, prog, env1) :: bls) in
∀x. nsLookup cenv.v vname = SOME x ==>
let len = LENGTH s2.refs in
let loc = Loc len in
let env2 = write n loc env1 in
let s2_abbrev = s2 with refs := s2.refs ++ [Refv x] in
ML_code env0 ((comm, s1, SNOC (Dlet locs (Pvar n) (App Opref [Var vname])) prog, env2)
:: bls) s2_abbrev
Proof
rw []
\\ irule (SIMP_RULE std_ss [LET_THM] ML_code_Dlet_var) \\ fs []
\\ first_x_assum $ irule_at $ Pos hd
\\ fs [eval_rel_def,evaluate_def,state_component_equality,AllCaseEqs(),
do_app_def,store_alloc_def, isFpBool_def, getOpClass_def]
QED
(* appending an environment *)
Definition declare_env_rel_def:
declare_env_rel s2 env1 s3 envv ⇔
∃es.
declare_env s2.eval_state env1 = SOME (envv, es) ∧
s3 = s2 with eval_state := es
End
Theorem ML_code_Denv:
∀n cenv s3 envv.
ML_code env0 ((comm,s1,prog,env1)::bls) s2 ⇒
declare_env_rel s2 cenv s3 envv ⇒
cenv = ML_code_env env0 ((comm,s1,prog,env1)::bls) ⇒
let
env2 = write n envv env1;
s3_abbrev = s3
in
ML_code env0 ((comm,s1,SNOC (Denv n) prog,env2)::bls) s3_abbrev
Proof
rw[ML_code_def, SNOC_APPEND, Decls_APPEND, Decls_Denv,
declare_env_rel_def, ML_code_env_def]
\\ first_assum $ irule_at Any
\\ first_assum $ irule_at Any
\\ rw[write_def, merge_env_def, empty_env_def,
sem_env_component_equality]
QED
(* setting the eval_state *)
Theorem ML_code_set_eval_state: (* only supported at the top-level for simplicity *)
ML_code env0 [(comm,s1,prog,env1)] s2 ⇒
s1.eval_state = NONE ⇒
∀es. ML_code env0 [(comm,s1 with eval_state := SOME es,prog,env1)]
(s2 with eval_state := SOME es)
Proof
rw [ML_code_def]
\\ drule_all Decls_set_eval_state
\\ fs []
QED
(* lookup function definitions *)
val lookup_var_def = Define `
lookup_var name (env:v sem_env) = nsLookup env.v (Short name)`;
val lookup_cons_def = Define `
lookup_cons name (env:v sem_env) = nsLookup env.c name`;
(* the old lookup formulation worked via nsLookup/mod_defined,
and mod_defined is still used in various characteristic scripts
so we supply an eval theorem that maps to the new approach. *)
val mod_defined_def = zDefine `
mod_defined env n =
∃p1 p2 e3.
p1 ≠ [] ∧ id_to_mods n = p1 ++ p2 ∧
nsLookupMod env p1 = SOME e3`;
Theorem mod_defined_nsLookup_Mod1[compute]:
mod_defined env id = (case id of Short _ => F
| Long mn _ => (case nsLookup_Mod1 env mn of NONE => F | _ => T))
Proof
PURE_CASE_TAC \\ fs [id_to_mods_def, mod_defined_def]
\\ Cases_on `env`
\\ fs [Once EXISTS_LIST, nsLookupMod_def, nsLookup_Mod1_def]
\\ PURE_CASE_TAC \\ fs [Once EXISTS_LIST, nsLookupMod_def]
QED
(* theorems about old lookup functions *)
(* FIXME: everything below this line is unlikely to be needed. *)
val nsLookupMod_nsBind = Q.prove(`
p ≠ [] ⇒
nsLookupMod (nsBind k v env) p = nsLookupMod env p`,
Cases_on`env`>>fs[nsBind_def]>> Induct_on`p`>>
fs[nsLookupMod_def]);
Theorem nsLookup_write:
(nsLookup (write n v env).v (Short name) =
if n = name then SOME v else nsLookup env.v (Short name)) /\
(nsLookup (write n v env).v (Long mn lname) =
nsLookup env.v (Long mn lname)) /\
(nsLookup (write n v env).c a = nsLookup env.c a) /\
(mod_defined (write n v env).v x = mod_defined env.v x) /\
(mod_defined (write n v env).c x = mod_defined env.c x)
Proof
fs [write_def] \\ rw []
\\ metis_tac[nsLookupMod_nsBind,mod_defined_def]
QED
Theorem nsLookup_write_cons:
(nsLookup (write_cons n v env).v a = nsLookup env.v a) /\
(nsLookup (write_cons n d env).c (Short name) =
if name = n then SOME d else nsLookup env.c (Short name)) /\
(mod_defined (write_cons n d env).v x = mod_defined env.v x) /\
(mod_defined (write_cons n d env).c x = mod_defined env.c x) /\
(nsLookup (write_cons n d env).c (Long mn lname) =
nsLookup env.c (Long mn lname))
Proof
fs [write_cons_def] \\ rw [] \\
metis_tac[nsLookupMod_nsBind,mod_defined_def]
QED
Theorem nsLookup_empty:
(nsLookup empty_env.v a = NONE) /\
(nsLookup empty_env.c b = NONE) /\
(mod_defined empty_env.v x = F) /\
(mod_defined empty_env.c x = F)
Proof
rw[empty_env_def, nsLookup_def, mod_defined_def,
nsLookupMod_def] \\ Cases_on`p1` \\ fs[]
QED
val nsLookupMod_nsAppend = Q.prove(`
nsLookupMod (nsAppend env1 env2) p =
if p = [] then SOME (nsAppend env1 env2)
else
case nsLookupMod env1 p of
SOME v => SOME v
| NONE =>
if (∃p1 p2 e3. p1 ≠ [] ∧ p = p1 ++ p2 ∧ nsLookupMod env1 p1 = SOME e3) then NONE
else nsLookupMod env2 p`,
IF_CASES_TAC>-
fs[nsLookupMod_def]>>
BasicProvers.TOP_CASE_TAC>>
rw[]>>
TRY(Cases_on`nsLookupMod env2 p`)>>
fs[namespacePropsTheory.nsLookupMod_nsAppend_none,namespacePropsTheory.nsLookupMod_nsAppend_some]>>
metis_tac[option_CLAUSES]) |> GEN_ALL;
Theorem nsLookup_write_mod:
(nsLookup (write_mod mn env1 env2).v (Short n) =
nsLookup env2.v (Short n)) /\
(nsLookup (write_mod mn env1 env2).c (Short n) =
nsLookup env2.c (Short n)) /\
(mod_defined (write_mod mn env1 env2).v (Long mn' r) =
((mn = mn') \/ mod_defined env2.v (Long mn' r))) /\
(mod_defined (write_mod mn env1 env2).c (Long mn' r) =
if mn = mn' then T
else mod_defined env2.c (Long mn' r)) /\
(nsLookup (write_mod mn env1 env2).v (Long mn1 ln) =
if mn = mn1 then nsLookup env1.v ln else
nsLookup env2.v (Long mn1 ln)) /\
(nsLookup (write_mod mn env1 env2).c (Long mn1 ln) =
if mn = mn1 then nsLookup env1.c ln else
nsLookup env2.c (Long mn1 ln))
Proof
fs [write_mod_def,mod_defined_def] \\
EVAL_TAC \\
fs[GSYM nsLift_def,id_to_mods_def,nsLookupMod_nsAppend] \\
simp[] >> CONJ_TAC>>
(eq_tac
>-
(strip_tac>>
Cases_on`p1`>>fs[]>>
fs[namespacePropsTheory.nsLookupMod_nsLift]>>
Cases_on`mn=h`>>fs[]>>
qexists_tac`h::t`>>fs[])
>>
Cases_on`mn=mn'`>>fs[]
>-
(qexists_tac`[mn']`>>fs[namespacePropsTheory.nsLookupMod_nsLift,nsLookupMod_def])
>>
strip_tac>>
asm_exists_tac>>fs[namespacePropsTheory.nsLookupMod_nsLift,nsLookupMod_def]>>
Cases_on`p1`>>fs[]>> rw[]>>
Cases_on`p1'`>>fs[]>>
metis_tac[])
QED
Theorem nsLookup_merge_env:
(nsLookup (merge_env e1 e2).v (Short n) =
case nsLookup e1.v (Short n) of
| NONE => nsLookup e2.v (Short n)
| SOME x => SOME x) /\
(nsLookup (merge_env e1 e2).c (Short n) =
case nsLookup e1.c (Short n) of
| NONE => nsLookup e2.c (Short n)
| SOME x => SOME x) /\
(nsLookup (merge_env e1 e2).v (Long mn ln) =
case nsLookup e1.v (Long mn ln) of
| NONE => if mod_defined e1.v (Long mn ln) then NONE
else nsLookup e2.v (Long mn ln)
| SOME x => SOME x) /\
(nsLookup (merge_env e1 e2).c (Long mn ln) =
case nsLookup e1.c (Long mn ln) of