-
Notifications
You must be signed in to change notification settings - Fork 3
/
pure_inference_modelScript.sml
3347 lines (3277 loc) · 150 KB
/
pure_inference_modelScript.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
open HolKernel Parse boolLib bossLib BasicProvers dep_rewrite goalStack;
open pairTheory arithmeticTheory integerTheory stringTheory optionTheory
listTheory alistTheory rich_listTheory finite_mapTheory pred_setTheory
sptreeTheory;
open mlmapTheory;
open pure_typingTheory pure_typingPropsTheory
pure_cexpTheory pure_configTheory pure_varsTheory pure_unificationTheory
pure_inference_commonTheory pure_inferenceTheory pure_inferencePropsTheory
pure_miscTheory pure_barendregtTheory;
val _ = new_theory "pure_inference_model";
(******************** Definitions ********************)
Datatype:
mconstraint = mUnify itype itype
| mInstantiate itype (num # itype)
| mImplicit itype (num set) itype
End
Type massumptions[pp] = ``:mlstring |-> num set``;
Definition get_massumptions_def:
get_massumptions (as : massumptions) x =
case FLOOKUP as x of NONE => {} | SOME xas => xas
End
Definition maunion_def:
maunion = FMERGE $UNION : massumptions -> massumptions -> massumptions
End
Definition massumptions_ok_def:
massumptions_ok (asms : massumptions) ⇔
∀k v x. FLOOKUP asms k = SOME v ∧ x ∈ v (* if assumption k |-> x is present *)
⇒ x ∉ BIGUNION (FRANGE (asms \\ k)) (* then x is unique *)
End
Definition new_vars_constraint_def[simp]:
new_vars_constraint (mUnify t1 t2) = pure_vars t1 ∪ pure_vars t2 ∧
new_vars_constraint (mImplicit t1 vars t2) = pure_vars t1 ∪ pure_vars t2 ∧
new_vars_constraint (mInstantiate t (vars, scheme)) = pure_vars t ∪ pure_vars scheme
End
Definition new_vars_def:
new_vars (asms : massumptions) cs t =
BIGUNION (FRANGE asms) ∪
BIGUNION (IMAGE new_vars_constraint cs) ∪
pure_vars t
End
Definition cvars_disjoint_def:
cvars_disjoint l ⇔ list_disjoint (MAP (λ(as,cs,t). new_vars as cs t) l)
End
Inductive minfer:
[~Var:]
(fresh ∉ mset
⇒ minfer (ns : exndef # typedefs) mset (pure_cexp$Var d x)
(FEMPTY |+ (x, {fresh})) {} (CVar fresh))
[~Tuple:]
(LENGTH es = LENGTH tys ∧
LENGTH ass = LENGTH css ∧
LIST_REL (λ(e,ty) (a,c). minfer ns mset e a c ty)
(ZIP (es,tys)) (ZIP (ass,css)) ∧
cvars_disjoint (ZIP (ass, ZIP (css, tys)))
⇒ minfer ns mset (Prim d (Cons «») es)
(FOLDR maunion FEMPTY ass) (BIGUNION (set css)) (Tuple tys))
[~Ret:]
(minfer ns mset e as cs ty
⇒ minfer ns mset (Prim d (Cons «Ret») [e])
as cs (M ty))
[~Bind:]
(minfer ns mset e1 as1 cs1 ty1 ∧
minfer ns mset e2 as2 cs2 ty2 ∧
cvars_disjoint [(as1,cs1,ty1);(as2,cs2,ty2)] ∧
f1 ∉ mset ∪ new_vars as1 cs1 ty1 ∪ new_vars as2 cs2 ty2 ∧
f2 ∉ mset ∪ new_vars as1 cs1 ty1 ∪ new_vars as2 cs2 ty2
⇒ minfer ns mset (Prim d (Cons «Bind») [e1;e2])
(maunion as1 as2)
({mUnify ty1 (M $ CVar f1); mUnify ty2 (Function (CVar f1) (M $ CVar f2))}
∪ cs1 ∪ cs2)
(M $ CVar f2))
[~Raise:]
(minfer ns mset e as cs ty ∧
f ∉ mset ∪ new_vars as cs ty
⇒ minfer ns mset (Prim d (Cons «Raise») [e])
as (mUnify (CVar f) (CVar f) INSERT mUnify ty Exception INSERT cs)
(M $ CVar f))
[~Handle:]
(minfer ns mset e1 as1 cs1 ty1 ∧
minfer ns mset e2 as2 cs2 ty2 ∧
cvars_disjoint [(as1,cs1,ty1);(as2,cs2,ty2)] ∧
f ∉ mset ∪ new_vars as1 cs1 ty1 ∪ new_vars as2 cs2 ty2
⇒ minfer ns mset (Prim d (Cons «Handle») [e1;e2])
(maunion as1 as2)
({mUnify ty1 (M $ CVar f); mUnify ty2 (Function Exception (M $ CVar f))}
∪ cs1 ∪ cs2)
(M $ CVar f))
[~Act:]
(minfer ns mset e as cs ty
⇒ minfer ns mset (Prim d (Cons «Act») [e])
as (mUnify ty (PrimTy Message) INSERT cs) (M StrTy))
[~Alloc:]
(minfer ns mset e1 as1 cs1 ty1 ∧
minfer ns mset e2 as2 cs2 ty2 ∧
cvars_disjoint [(as1,cs1,ty1);(as2,cs2,ty2)]
⇒ minfer ns mset (Prim d (Cons «Alloc») [e1;e2])
(maunion as1 as2)
(mUnify ty1 IntTy INSERT cs1 ∪ cs2)
(M $ Array ty2))
[~Length:]
(minfer ns mset e as cs ty ∧
fresh ∉ mset ∪ new_vars as cs ty
⇒ minfer ns mset (Prim d (Cons «Length») [e])
as (mUnify ty (Array $ CVar fresh) INSERT cs) (M IntTy))
[~Deref:]
(minfer ns mset e1 as1 cs1 ty1 ∧
minfer ns mset e2 as2 cs2 ty2 ∧
cvars_disjoint [(as1,cs1,ty1);(as2,cs2,ty2)] ∧
f ∉ mset ∪ new_vars as1 cs1 ty1 ∪ new_vars as2 cs2 ty2
⇒ minfer ns mset (Prim d (Cons «Deref») [e1;e2])
(maunion as1 as2)
({mUnify ty2 IntTy; mUnify ty1 (Array $ CVar f)} ∪ cs1 ∪ cs2)
(M $ CVar f))
[~Update:]
(minfer ns mset e1 as1 cs1 ty1 ∧
minfer ns mset e2 as2 cs2 ty2 ∧
minfer ns mset e3 as3 cs3 ty3 ∧
cvars_disjoint [(as1,cs1,ty1);(as2,cs2,ty2);(as3,cs3,ty3)] ∧
f ∉ mset ∪ new_vars as1 cs1 ty1 ∪ new_vars as2 cs2 ty2 ∪ new_vars as3 cs3 ty3
⇒ minfer ns mset (Prim d (Cons «Update») [e1;e2;e3])
(maunion as1 (maunion as2 as3))
({mUnify ty3 (CVar f); mUnify ty2 IntTy; mUnify ty1 (Array $ CVar f)}
∪ cs1 ∪ cs2 ∪ cs3)
(M Unit))
[~True:]
(minfer ns mset (Prim d (Cons «True») []) FEMPTY {} BoolTy)
[~False:]
(minfer ns mset (Prim d (Cons «False») []) FEMPTY {} BoolTy)
[~Exception:]
(LENGTH es = LENGTH tys ∧
LENGTH ass = LENGTH css ∧
LIST_REL (λ(e,ty) (a,c). minfer ns mset e a c ty)
(ZIP (es,tys)) (ZIP (ass,css)) ∧
cvars_disjoint (ZIP (ass, ZIP (css, tys))) ∧
ALOOKUP (FST ns) s = SOME arg_tys ∧
LENGTH arg_tys = LENGTH tys ∧
explode s ∉ monad_cns
⇒ minfer ns mset (Prim d (Cons s) es)
(FOLDR maunion FEMPTY ass)
(set (list$MAP2 (λt a. mUnify t (itype_of a)) tys arg_tys) ∪ BIGUNION (set css))
Exception)
[~Cons:]
(LENGTH es = LENGTH tys ∧
LENGTH ass = LENGTH css ∧
LIST_REL (λ(e,ty) (a,c). minfer ns mset e a c ty)
(ZIP (es,tys)) (ZIP (ass,css)) ∧
cvars_disjoint (ZIP (ass, ZIP (css, tys))) ∧
id < LENGTH (SND ns) ∧
EL id (SND ns) = (ar,cns) ∧
ALOOKUP cns cname = SOME arg_tys ∧
LENGTH arg_tys = LENGTH tys ∧
LENGTH freshes = ar ∧
EVERY (λf. f ∉ mset ∧
EVERY (λ(as,cs,ty). f ∉ new_vars as cs ty) (ZIP (ass,ZIP(css,tys)))) freshes ∧
explode cname ∉ monad_cns
⇒ minfer ns mset (Prim d (Cons cname) es)
(FOLDR maunion FEMPTY ass)
(set (MAP (λf. mUnify (CVar f) (CVar f)) freshes) ∪
set (list$MAP2
(λt a. mUnify t (isubst (MAP CVar freshes) $ itype_of a)) tys arg_tys) ∪
BIGUNION (set css))
(TypeCons id (MAP CVar freshes)))
[~AtomOp:]
(infer_atom_op (LENGTH es) aop = SOME (parg_tys, pret_ty) ∧
LENGTH es = LENGTH tys ∧
LENGTH ass = LENGTH css ∧
LIST_REL (λ(e,ty) (a,c). minfer ns mset e a c ty)
(ZIP (es,tys)) (ZIP (ass,css)) ∧
cvars_disjoint (ZIP (ass, ZIP (css, tys)))
⇒ minfer ns mset (Prim d (AtomOp aop) es)
(FOLDR maunion FEMPTY ass)
(set (list$MAP2 (λt a. mUnify t (PrimTy a)) tys parg_tys) ∪ BIGUNION (set css))
(PrimTy pret_ty))
[~Seq:]
(minfer ns mset e1 as1 cs1 ty1 ∧
minfer ns mset e2 as2 cs2 ty2 ∧
cvars_disjoint [(as1,cs1,ty1);(as2,cs2,ty2)]
⇒ minfer ns mset (Prim d Seq [e1;e2])
(maunion as1 as2) (cs1 ∪ cs2) ty2)
[~App:]
(¬NULL es ∧
LENGTH es = LENGTH tys ∧
LENGTH ass = LENGTH css ∧
LIST_REL (λ(e,ty) (a,c). minfer ns mset e a c ty)
(ZIP (es,tys)) (ZIP (ass,css)) ∧
minfer ns mset e fas fcs fty ∧
cvars_disjoint ((fas,fcs,fty)::ZIP (ass, ZIP (css, tys))) ∧
f ∉ mset ∧
EVERY (λ(as,cs,ty). f ∉ new_vars as cs ty) (ZIP (fas::ass,ZIP(fcs::css,fty::tys))) ∧
as = FOLDR maunion FEMPTY (fas::ass) ∧
cs = fcs ∪ BIGUNION (set css)
⇒ minfer ns mset (App d e es)
as (mUnify fty (iFunctions tys (CVar f)) INSERT cs) (CVar f))
[~Lam:]
(¬NULL xs ∧
minfer ns (set freshes ∪ mset) e as cs ty ∧
LENGTH freshes = LENGTH xs ∧
EVERY (λf. f ∉ mset ∪ new_vars as cs ty) freshes
⇒ minfer ns mset (Lam d xs e)
(FDIFF as (set xs))
(cs ∪ set (MAP (λf. mUnify (CVar f) (CVar f)) freshes) ∪
(BIGUNION $ set $ list$MAP2 (λf x.
IMAGE (λn. mUnify (CVar f) (CVar n)) (get_massumptions as x)) freshes xs))
(iFunctions (MAP CVar freshes) ty))
[~Let:]
(minfer ns mset e1 as1 cs1 ty1 ∧
minfer ns mset e2 as2 cs2 ty2 ∧
cvars_disjoint [(as1,cs1,ty1);(as2,cs2,ty2)]
⇒ minfer ns mset (Let d x e1 e2)
(maunion as1 (as2 \\ x))
(IMAGE (λn. mImplicit (CVar n) mset ty1) (get_massumptions as2 x) ∪ cs1 ∪ cs2)
ty2)
[~Letrec:]
(¬NULL fns ∧
LENGTH fns = LENGTH tys ∧
LENGTH ass = LENGTH css ∧
LIST_REL (λ((fn,e),ty) (a,c). minfer ns mset e a c ty)
(ZIP (fns,tys)) (ZIP (ass,css)) ∧
minfer ns mset e eas ecs ety ∧
cvars_disjoint ((eas,ecs,ety)::ZIP (ass, ZIP (css, tys))) ∧
as = FOLDR maunion FEMPTY ass ∧
cs = ecs ∪ BIGUNION (set css)
⇒ minfer ns mset (Letrec d fns e)
(FDIFF (maunion eas as) (set $ MAP FST fns))
(set (MAP (λt. mUnify t t) tys) ∪ cs ∪
(BIGUNION $ set $ list$MAP2 (λ(x,b) tyfn.
IMAGE (λn. mUnify (CVar n) tyfn) (get_massumptions as x)) fns tys) ∪
(BIGUNION $ set $ list$MAP2 (λ(x,b) tyfn.
IMAGE (λn. mImplicit (CVar n) mset tyfn) (get_massumptions eas x)) fns tys))
ety)
[~BoolCase:]
(minfer ns (f INSERT mset) e1 as1 cs1 ty1 ∧
minfer ns (f INSERT mset) e2 as2 cs2 ty2 ∧
minfer ns mset e eas ecs ety ∧
cvars_disjoint [(eas,ecs,ety);(as1,cs1,ty1);(as2,cs2,ty2)] ∧
f ∉ mset ∪ new_vars eas ecs ety ∪ new_vars as1 cs1 ty1 ∪ new_vars as2 cs2 ty2 ∧
{cn1; cn2} = {«True»;«False»}
⇒ minfer ns mset (Case d e v [(cn1,[],e1);(cn2,[],e2)] NONE)
(maunion eas (maunion as1 as2 \\ v))
(mUnify (CVar f) ety INSERT mUnify ety BoolTy INSERT mUnify ty1 ty2 INSERT
IMAGE (λn. mUnify (CVar n) (CVar f))
(get_massumptions as1 v ∪ get_massumptions as2 v) ∪
ecs ∪ cs1 ∪ cs2)
ty1)
[~TupleCase:]
(¬MEM v pvars ∧ ALL_DISTINCT pvars ∧
minfer ns (f INSERT set freshes ∪ mset) rest asrest csrest tyrest ∧
minfer ns mset e eas ecs ety ∧
cvars_disjoint [(eas,ecs,ety);(asrest,csrest,tyrest)] ∧
EVERY (λf.
f ∉ mset ∪ new_vars eas ecs ety ∪ new_vars asrest csrest tyrest)
(f::freshes) ∧
LENGTH pvars = LENGTH freshes ∧
pvar_cs =
list$MAP2
(λv t. IMAGE (λn. mUnify (CVar n) t) (get_massumptions asrest v))
(v::pvars) (MAP CVar $ f::freshes)
⇒ minfer ns mset (Case d e v [(«»,pvars,rest)] NONE)
(maunion eas (FDIFF asrest (set (v::pvars))))
(mUnify (CVar f) ety INSERT mUnify ety (Tuple $ MAP CVar freshes) INSERT
BIGUNION (set pvar_cs) ∪ ecs ∪ csrest)
tyrest)
[~ExceptionCase:]
(¬MEM v (FLAT (MAP (FST o SND) cases)) ∧
PERM (MAP (λ(cn,ts). (cn, LENGTH ts)) (FST ns))
(MAP (λ(cn,pvars,rest). (cn, LENGTH pvars)) cases) ∧
LENGTH cases = LENGTH tys ∧
LENGTH ass = LENGTH css ∧
LIST_REL (λ((cname,pvars,rest),ty) (a,c).
minfer ns (f INSERT mset) rest a c ty)
(ZIP (cases,tys)) (ZIP (ass,css)) ∧
EVERY (λ(cname,pvars,rest). ALL_DISTINCT pvars) cases ∧
minfer ns mset e eas ecs ety ∧
cvars_disjoint ((eas,ecs,ety)::ZIP (ass, ZIP (css, tys))) ∧
f ∉ mset ∧
EVERY (λ(as,cs,ty). f ∉ new_vars as cs ty)
(ZIP (eas::ass,ZIP(ecs::css,ety::tys))) ∧
LENGTH final_as = LENGTH final_cs ∧
LIST_REL (λ((cn,pvars,rest),as,cs) (as',cs').
∃schemes.
ALOOKUP (FST ns) cn = SOME schemes ∧
let pvar_cs = list$MAP2
(λv t. IMAGE (λn. mUnify (CVar n) t) (get_massumptions as v))
(v::pvars) (CVar f :: MAP itype_of schemes) in
as' = FDIFF as (v INSERT set pvars) ∧
cs' = BIGUNION (set pvar_cs) ∪ cs)
(ZIP (cases,ZIP (ass,css))) (ZIP (final_as,final_cs))
⇒ minfer ns mset (Case d e v cases NONE)
(FOLDR maunion FEMPTY (eas::final_as))
(mUnify (CVar f) ety INSERT mUnify ety Exception INSERT
set (MAP (λt. mUnify (HD tys) t) (TL tys)) ∪ ecs ∪ BIGUNION (set final_cs))
(HD tys))
[~CaseExhaustive:]
(¬MEM v (FLAT (MAP (FST o SND) cases)) ∧
oEL id (SND ns) = SOME (ar, cdefs) ∧
PERM (MAP (λ(cn,ts). (cn, LENGTH ts)) cdefs)
(MAP (λ(cn,pvars,rest). (cn, LENGTH pvars)) cases) ∧
LENGTH cases = LENGTH tys ∧
LENGTH ass = LENGTH css ∧
ar = LENGTH freshes ∧
LIST_REL (λ((cname,pvars,rest),ty) (a,c).
minfer ns (f INSERT set freshes ∪ mset) rest a c ty)
(ZIP (cases,tys))
(ZIP (ass,css)) ∧
EVERY (λ(cname,pvars,rest). ALL_DISTINCT pvars) cases ∧
minfer ns mset e eas ecs ety ∧
cvars_disjoint ((eas,ecs,ety)::ZIP (ass, ZIP (css, tys))) ∧
EVERY (λf. f ∉ mset ∧
EVERY (λ(as,cs,ty). f ∉ new_vars as cs ty)
(ZIP (eas::ass,ZIP(ecs::css,ety::tys))))
(f::freshes) ∧
LENGTH final_as = LENGTH final_cs ∧
LIST_REL (λ((cn,pvars,rest),as,cs) (as',cs').
∃schemes.
ALOOKUP cdefs cn = SOME schemes ∧
let pvar_cs =
list$MAP2
(λv t. IMAGE (λn. mUnify (CVar n) t) (get_massumptions as v))
(v::pvars)
(CVar f :: MAP (isubst (MAP CVar freshes) o itype_of) schemes)
in
as' = FDIFF as (v INSERT set pvars) ∧
cs' = BIGUNION (set pvar_cs) ∪ cs)
(ZIP (cases,ZIP (ass,css)))
(ZIP (final_as,final_cs))
⇒ minfer ns mset (Case d e v cases NONE)
(FOLDR maunion FEMPTY (eas::final_as))
(mUnify (CVar f) ety INSERT
mUnify ety (TypeCons id (MAP CVar freshes)) INSERT
set (MAP (λt. mUnify (HD tys) t) (TL tys)) ∪ ecs ∪
BIGUNION (set final_cs))
(HD tys))
[~CaseNonexhaustive:]
(¬MEM v (FLAT (MAP (FST o SND) cases)) ∧
oEL id (SND ns) = SOME (ar, cdefs) ∧
cases ≠ [] ∧ us_cn_ars ≠ [] ∧
PERM (MAP (λ(cn,ts). (cn, LENGTH ts)) cdefs)
(MAP (λ(cn,pvars,rest). (cn, LENGTH pvars)) cases ++ us_cn_ars) ∧
LENGTH cases = LENGTH tys ∧
LENGTH ass = LENGTH css ∧
ar = LENGTH freshes ∧
LIST_REL (λ((cname,pvars,rest),ty) (a,c).
minfer ns (f INSERT set freshes ∪ mset) rest a c ty)
(ZIP (cases,tys))
(ZIP (ass,css)) ∧
EVERY (λ(cname,pvars,rest). ALL_DISTINCT pvars) cases ∧
minfer ns mset e eas ecs ety ∧
minfer ns (f INSERT set freshes ∪ mset) usrest usas uscs usty ∧
cvars_disjoint ((eas,ecs,ety)::(usas,uscs,usty)::ZIP (ass, ZIP (css, tys))) ∧
EVERY (λf. f ∉ mset ∧
EVERY (λ(as,cs,ty). f ∉ new_vars as cs ty)
(ZIP (eas::usas::ass,ZIP(ecs::uscs::css,ety::usty::tys))))
(f::freshes) ∧
LENGTH final_as = LENGTH final_cs ∧
LIST_REL (λ((cn,pvars,rest),as,cs) (as',cs').
∃schemes.
ALOOKUP cdefs cn = SOME schemes ∧
let pvar_cs =
list$MAP2
(λv t. IMAGE (λn. mUnify (CVar n) t) (get_massumptions as v))
(v::pvars)
(CVar f :: MAP (isubst (MAP CVar freshes) o itype_of) schemes)
in
as' = FDIFF as (v INSERT set pvars) ∧
cs' = BIGUNION (set pvar_cs) ∪ cs)
(ZIP (cases,ZIP (ass,css)))
(ZIP (final_as,final_cs)) ∧
final_usas = usas \\ v ∧
final_uscs = IMAGE (λn. mUnify (CVar n) (CVar f)) (get_massumptions usas v) ∪ uscs
⇒ minfer ns mset (Case d e v cases (SOME (us_cn_ars, usrest)))
(FOLDR maunion FEMPTY (eas::final_usas::final_as))
(mUnify (CVar f) ety INSERT
mUnify ety (TypeCons id (MAP CVar freshes)) INSERT
set (MAP (λt. mUnify usty t) tys) ∪ ecs ∪
final_uscs ∪ BIGUNION (set final_cs))
usty)
End
(******************** Proof apparatus ********************)
Definition to_mconstraint_def[simp]:
to_mconstraint (Unify d t1 t2) = mUnify t1 t2 ∧
to_mconstraint (Instantiate d t sch) = mInstantiate t sch ∧
to_mconstraint (Implicit d t1 mono t2) = mImplicit t1 (domain mono) t2
End
Definition assumptions_rel_def:
assumptions_rel asms masms ⇔
map_ok asms ∧ cmp_of asms = var_cmp ∧
(∀s. FLOOKUP masms s = OPTION_MAP domain (lookup asms s)) ∧
(∀s aset. lookup asms s = SOME aset ⇒ wf aset)
End
Definition msubst_vars_def:
msubst_vars s vars = BIGUNION (IMAGE (pure_vars o pure_walkstar s o CVar) vars)
End
Definition mactivevars_def:
mactivevars (mUnify t1 t2) = pure_vars t1 ∪ pure_vars t2 ∧
mactivevars (mInstantiate t1 (vs,sch)) = pure_vars t1 ∪ pure_vars sch ∧
mactivevars (mImplicit t1 vs t2) = pure_vars t1 ∪ (vs ∩ pure_vars t2)
End
Definition mis_solveable_def:
mis_solveable (mUnify t1 t2) cs = T ∧
mis_solveable (mInstantiate t1 sch) cs = T ∧
mis_solveable (mImplicit t1 vs t2) cs = (
pure_vars t2 ∩ (BIGUNION $ IMAGE mactivevars ({mImplicit t1 vs t2} ∪ cs)) ⊆ vs)
End
Definition constraint_vars_def:
constraint_vars (mUnify t1 t2) = pure_vars t1 ∪ pure_vars t2 ∧
constraint_vars (mInstantiate t (vs,sch)) = pure_vars t ∪ pure_vars sch ∧
constraint_vars (mImplicit t1 vs t2) = pure_vars t1 ∪ vs ∪ pure_vars t2
End
Definition constraints_ok_def:
constraints_ok tds cs ⇔
∀c. c ∈ cs ⇒
(∀t1 t2. c = mUnify t1 t2 ⇒
itype_ok tds 0 t1 ∧ itype_ok tds 0 t2) ∧
(∀t1 vs t2. c = mInstantiate t1 (vs,t2) ⇒
itype_ok tds 0 t1 ∧ itype_ok tds vs t2) ∧
(∀t1 vs t2. c = mImplicit t1 vs t2 ⇒
itype_ok tds 0 t1 ∧ itype_ok tds 0 t2 ∧ FINITE vs)
End
(******************** Lemmas ********************)
Triviality maunion_comm:
∀x y. maunion x y = maunion y x
Proof
rw[maunion_def] >>
irule $ iffRL $ SIMP_RULE (srw_ss()) [combinTheory.COMM_DEF] FMERGE_COMM >>
rw[UNION_COMM]
QED
Theorem FDIFF_maunion:
FDIFF (maunion a b) s = maunion (FDIFF a s) (FDIFF b s)
Proof
rw[maunion_def, FDIFF_FMERGE]
QED
Theorem massumptions_ok_maunion:
∀as bs.
massumptions_ok as ∧ massumptions_ok bs ∧
DISJOINT (BIGUNION (FRANGE as)) (BIGUNION (FRANGE bs))
⇒ massumptions_ok (maunion as bs)
Proof
rw[massumptions_ok_def, DISJ_EQ_IMP] >>
gvs[IN_FRANGE_FLOOKUP, DOMSUB_FLOOKUP_THM, PULL_EXISTS,
maunion_def, FLOOKUP_FMERGE] >> rw[] >>
every_case_tac >> gvs[] >> metis_tac[DISJOINT_ALT]
QED
Theorem BIGUNION_FRANGE_maunion:
∀as bs.
BIGUNION (FRANGE (maunion as bs)) =
BIGUNION (FRANGE as) ∪ BIGUNION (FRANGE bs)
Proof
rw[] >> once_rewrite_tac[EXTENSION] >>
rw[] >> eq_tac >> rw[] >>
gvs[IN_FRANGE_FLOOKUP, PULL_EXISTS, maunion_def, FLOOKUP_FMERGE]
>- (every_case_tac >> gvs[] >> metis_tac[])
>- (
Cases_on `FLOOKUP bs k` >> gvs[]
>- (goal_assum drule >> qexists_tac `k` >> simp[])
>- (qexistsl_tac [`s ∪ x'`,`k`] >> simp[])
)
>- (
Cases_on `FLOOKUP as k` >> gvs[]
>- (goal_assum drule >> qexists_tac `k` >> simp[])
>- (qexistsl_tac [`s ∪ x'`,`k`] >> simp[UNION_COMM])
)
QED
Theorem LIST_TO_SET_get_assumptions:
∀as mas. assumptions_rel as mas ⇒
∀x. set (get_assumptions x as) = get_massumptions mas x
Proof
rw[EXTENSION, get_assumptions_def, get_massumptions_def] >>
gvs[assumptions_rel_def] >> CASE_TAC >> gvs[] >>
simp[miscTheory.toAList_domain]
QED
Triviality domain_list_insert_alt:
domain (list_insert xs t) = set xs ∪ domain t
Proof
rw[EXTENSION, domain_list_insert]
QED
Theorem FLOOKUP_maunion:
∀a b k.
FLOOKUP (maunion a b) k =
case FLOOKUP a k of
| NONE => FLOOKUP b k
| SOME av => SOME (case FLOOKUP b k of NONE => av | SOME bv => av ∪ bv)
Proof
rw[maunion_def, FLOOKUP_FMERGE] >> rpt CASE_TAC >> simp[]
QED
Theorem FLOOKUP_FOLDR_maunion:
∀ms base k.
FLOOKUP (FOLDR maunion base ms) k =
if k ∉ FDOM base ∧ ∀m. MEM m ms ⇒ k ∉ FDOM m then NONE
else SOME $
BIGUNION {s | FLOOKUP base k = SOME s ∨ ∃m. MEM m ms ∧ FLOOKUP m k = SOME s}
Proof
Induct >> rw[]
>- simp[FLOOKUP_DEF]
>- simp[FLOOKUP_DEF]
>- (gvs[maunion_def, FLOOKUP_FMERGE] >> gvs[FLOOKUP_DEF]) >>
gvs[maunion_def, FLOOKUP_FMERGE] >> gvs[FLOOKUP_DEF] >>
every_case_tac >> gvs[] >> rw[EXTENSION] >> metis_tac[]
QED
Theorem BIGUNION_FRANGE_FOLDR_maunion:
∀as ass a. MEM as ass ⇒ BIGUNION (FRANGE as) ⊆ BIGUNION (FRANGE (FOLDR maunion a ass))
Proof
rw[BIGUNION_SUBSET] >> rw[SUBSET_DEF] >>
gvs[IN_FRANGE_FLOOKUP, PULL_EXISTS, FLOOKUP_FOLDR_maunion, GSYM CONJ_ASSOC] >>
goal_assum drule >> qexists_tac `k` >> simp[] >>
gvs[FLOOKUP_DEF] >> metis_tac[]
QED
Triviality infer_bind_alt_def:
∀g f.
infer_bind g f = λs. case g s of Err e => Err e | OK ((a,b,c),s') => f (a,b,c) s'
Proof
rw[FUN_EQ_THM, infer_bind_def] >> rpt (CASE_TAC >> simp[])
QED
Theorem subst_vars_msubst_vars:
∀s vs. pure_wfs s ⇒
domain (subst_vars s vs) = msubst_vars s (domain vs)
Proof
rw[subst_vars_def, msubst_vars_def] >>
qsuff_tac
`∀m b.
domain (
foldi (λn u acc. union acc (freecvars (pure_walkstar s (CVar n)))) m b vs) =
BIGUNION (IMAGE
(pure_vars o pure_walkstar s o CVar o (λi. m + sptree$lrnext m * i))
(domain vs))
∪ domain b`
>- rw[Once lrnext_def, combinTheory.o_DEF] >>
qid_spec_tac `vs` >> Induct >> rw[foldi_def] >>
simp[pure_walkstar_alt, freecvars_def, domain_union]
>- (CASE_TAC >> simp[freecvars_pure_vars, domain_union, Once UNION_COMM]) >>
simp[IMAGE_IMAGE, combinTheory.o_DEF] >>
simp[lrnext_lrnext, lrnext_lrnext_2, LEFT_ADD_DISTRIB]
>- simp[AC UNION_ASSOC UNION_COMM] >>
qmatch_goalsub_abbrev_tac `BIGUNION A ∪ (BIGUNION B ∪ _ ∪ C) = C' ∪ _ ∪ _ ∪ _` >>
qsuff_tac `C = C'` >> rw[] >- simp[AC UNION_ASSOC UNION_COMM] >>
unabbrev_all_tac >> CASE_TAC >> simp[freecvars_pure_vars]
QED
Theorem msubst_vars_UNION:
msubst_vars s (a ∪ b) = msubst_vars s a ∪ msubst_vars s b
Proof
simp[msubst_vars_def]
QED
Theorem domain_activevars:
∀c. domain (activevars c) = mactivevars (to_mconstraint c)
Proof
Cases >> rw[activevars_def, mactivevars_def] >>
simp[domain_union, freecvars_pure_vars, domain_inter] >>
Cases_on `p` >> rw[activevars_def, mactivevars_def] >>
simp[domain_union, freecvars_pure_vars]
QED
Theorem is_solveable_mis_solveable:
∀c cs.
is_solveable c cs ⇔ mis_solveable (to_mconstraint c) (set $ MAP to_mconstraint cs)
Proof
Cases >> rw[is_solveable_def, mis_solveable_def] >>
DEP_REWRITE_TAC[domain_empty] >> rw[] >- (irule wf_difference >> simp[]) >>
simp[domain_difference, domain_inter, freecvars_pure_vars, SUBSET_DIFF_EMPTY] >>
qmatch_goalsub_abbrev_tac `FOLDL _ imp _` >>
qmatch_goalsub_abbrev_tac `mimp ∪ _` >>
qsuff_tac `domain (FOLDL (λacc c. union (activevars c) acc) imp cs) =
mimp ∪ (BIGUNION $ IMAGE mactivevars $ set $ MAP to_mconstraint cs)` >> simp[] >>
Induct_on `cs` using SNOC_INDUCT >> rw[FOLDL_SNOC, MAP_SNOC]
>- (unabbrev_all_tac >> gvs[domain_activevars]) >>
simp[domain_union, domain_activevars, LIST_TO_SET_SNOC, AC UNION_ASSOC UNION_COMM]
QED
Theorem constraints_ok_UNION:
constraints_ok ns (cs1 ∪ cs2) ⇔ constraints_ok ns cs1 ∧ constraints_ok ns cs2
Proof
simp[constraints_ok_def] >> eq_tac >> rw[] >> metis_tac[]
QED
val inferM_ss = simpLib.named_rewrites "inferM_ss"
[infer_bind_alt_def, infer_bind_def, infer_ignore_bind_def, fail_def,
return_def, fresh_var_def, fresh_vars_def, oreturn_def];
val _ = simpLib.register_frag inferM_ss;
val inferM_rws = SF inferM_ss;
Triviality infer_ignore_bind_simps[simp]:
(do _ <- ( λs. Err e) ; foo od = \s. Err e) ∧
(do _ <- ( λs. OK ((),s)) ; foo od = foo)
Proof
rw[FUN_EQ_THM, inferM_rws]
QED
fun print_tac s gs = (print (s ^ "\n"); ALL_TAC gs)
Theorem infer_minfer:
∀ns mset e n ty as cs m.
infer ns mset e n = OK ((ty,as,cs),m) ∧
namespace_ok ns ∧
(∀mvar. mvar ∈ domain mset ⇒ mvar < n) ⇒
∃mas.
assumptions_rel as mas ∧
minfer ns (domain mset) e mas (set (MAP to_mconstraint cs)) ty ∧
n ≤ m ∧
(new_vars mas (set (MAP to_mconstraint cs)) ty ⊆ { v | n ≤ v ∧ v < m})
Proof
recInduct infer_ind >> rw[infer_def]
>- ( (* Var *)
print_tac "Var" >>
last_x_assum mp_tac >> rw[inferM_rws] >>
qexists_tac `FEMPTY |+ (x, {n})` >> simp[assumptions_rel_def] >>
simp[lookup_singleton, FLOOKUP_UPDATE] >> rw[]
>- simp[wf_insert]
>- (
simp[Once minfer_cases] >> CCONTR_TAC >> gvs[] >>
last_x_assum drule >> simp[]
)
>- gvs[new_vars_def, pure_vars]
)
>- ( (* Tuple *)
print_tac "Tuple" >>
gvs[inferM_rws] >> every_case_tac >> gvs[] >> pairarg_tac >> gvs[] >>
ntac 2 $ pop_assum mp_tac >>
map_every qid_spec_tac [`m`,`n`,`tys`,`as`,`cs`] >>
Induct_on `es` >> rw[] >> simp[]
>- (
qexists_tac `FEMPTY` >> simp[assumptions_rel_def] >>
simp[Once minfer_cases, PULL_EXISTS] >>
qexistsl_tac [`[]`,`[]`] >> simp[cvars_disjoint_def, new_vars_def] >>
simp[list_disjoint_def, pure_vars]
) >>
every_case_tac >> gvs[] >>
last_x_assum drule >> strip_tac >> gvs[] >>
last_x_assum $ qspec_then `h` mp_tac >> simp[] >>
disch_then drule >> impl_tac >- (rw[] >> first_x_assum drule >> rw[]) >>
strip_tac >> gvs[] >> qexists_tac `maunion mas' mas` >> rw[]
>- (
gvs[assumptions_rel_def, aunion_def, PULL_FORALL] >> rpt gen_tac >>
DEP_REWRITE_TAC[cj 1 unionWith_thm, cj 2 unionWith_thm, lookup_unionWith] >>
simp[maunion_def, FLOOKUP_FMERGE] >>
every_case_tac >> gvs[] >> rw[] >>
simp[AC UNION_ASSOC UNION_COMM] >> metis_tac[wf_union, domain_union]
)
>- (
qpat_x_assum `minfer _ _ _ _ _ (Tuple _)` mp_tac >>
once_rewrite_tac[minfer_cases] >> simp[] >> strip_tac >> gvs[] >>
rename1 `set (_ cs) ∪ _` >>
qexistsl_tac [`mas'::ass`, `(set (MAP to_mconstraint cs)) :: css`] >>
gvs[cvars_disjoint_def] >>
once_rewrite_tac[CONS_APPEND] >> rewrite_tac[list_disjoint_append] >>
simp[MEM_MAP, EXISTS_PROD, PULL_EXISTS] >> rpt gen_tac >>
DEP_REWRITE_TAC[MEM_ZIP] >> DEP_REWRITE_TAC[cj 1 LENGTH_ZIP] >> simp[] >>
imp_res_tac LIST_REL_LENGTH >> gvs[] >> simp[PULL_EXISTS] >> rw[] >>
pop_assum mp_tac >> DEP_REWRITE_TAC[EL_ZIP] >> simp[] >> strip_tac >> gvs[] >>
irule SUBSET_DISJOINT >>
qexistsl_tac [`{v | r ≤ v ∧ v < m}`,`{v | n ≤ v ∧ v < r}`] >>
conj_tac >- rw[DISJOINT_ALT] >> gvs[] >>
irule SUBSET_TRANS >> goal_assum $ drule_at Any >>
simp[new_vars_def, BIGUNION_SUBSET, pure_vars, PULL_EXISTS] >> rw[]
>- (
simp[SUBSET_DEF] >> rw[] >> ntac 2 disj1_tac >>
gvs[IN_FRANGE_FLOOKUP, FLOOKUP_FOLDR_maunion, PULL_EXISTS,
GSYM CONJ_ASSOC, FLOOKUP_DEF] >>
rpt $ goal_assum $ drule_at Any >> simp[EL_MEM]
)
>- (
simp[SUBSET_DEF] >> rw[] >> disj1_tac >> disj2_tac >>
simp[PULL_EXISTS] >> rpt $ goal_assum drule >> simp[EL_MEM]
)
>- (
simp[SUBSET_DEF] >> rw[] >> disj2_tac >> simp[MEM_MAP, PULL_EXISTS] >>
goal_assum drule >> simp[EL_MEM]
)
)
>- (
gvs[new_vars_def, BIGUNION_FRANGE_maunion, GSYM CONJ_ASSOC, pure_vars] >> rw[] >>
rename1 `foo ⊆ _` >> gvs[SUBSET_DEF] >> rw[] >> first_x_assum drule >> rw[]
)
)
>- ( (* Ret *)
print_tac "Ret" >>
gvs[inferM_rws] >> Cases_on `es` >> gvs[] >> Cases_on `t` >> gvs[inferM_rws] >>
every_case_tac >> gvs[] >>
last_x_assum drule_all >> strip_tac >> simp[] >>
goal_assum drule >> simp[Once minfer_cases] >>
gvs[new_vars_def, pure_vars]
)
>- ( (* Bind *)
print_tac "Bind" >>
gvs[inferM_rws] >>
Cases_on `es` >> gvs[] >> Cases_on `t` >> gvs[] >>
Cases_on `t'` >> gvs[inferM_rws] >> every_case_tac >> gvs[] >>
first_x_assum drule_all >> strip_tac >> gvs[] >>
last_x_assum drule >> impl_tac
>- (rw[] >> last_x_assum drule >> simp[]) >>
strip_tac >> gvs[] >>
simp[Once minfer_cases, PULL_EXISTS] >>
ntac 2 $ goal_assum $ drule_at Any >> qexists_tac `r'` >> rw[]
>- (
gvs[assumptions_rel_def] >> simp[PULL_FORALL, aunion_def] >>
rpt gen_tac >> DEP_REWRITE_TAC[lookup_unionWith] >>
DEP_REWRITE_TAC[cj 1 unionWith_thm, cj 2 unionWith_thm] >> simp[] >>
simp[maunion_def, FLOOKUP_FMERGE] >>
every_case_tac >> gvs[] >> rw[] >>
metis_tac[wf_union, domain_union]
)
>- (rw[EXTENSION] >> eq_tac >> rw[] >> simp[])
>- (
simp[cvars_disjoint_def, DISJOINT_ALT] >> rw[] >> CCONTR_TAC >> gvs[SUBSET_DEF] >>
first_x_assum drule >> strip_tac >> first_x_assum drule >> strip_tac >> gvs[]
)
>- (CCONTR_TAC >> gvs[] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (
gvs[new_vars_def, BIGUNION_FRANGE_maunion, GSYM CONJ_ASSOC] >>
simp[new_vars_constraint_def, pure_vars] >>
rw[] >> rename1 `foo ⊆ _` >> gvs[SUBSET_DEF] >> rw[] >>
first_x_assum drule >> rw[]
)
)
>- ( (* Raise *)
print_tac "Raise" >>
gvs[inferM_rws] >>
Cases_on `es` >> gvs[] >> Cases_on `t` >> gvs[] >> every_case_tac >> gvs[] >>
first_x_assum drule_all >> strip_tac >> gvs[] >>
goal_assum drule >> simp[Once minfer_cases, PULL_EXISTS, GSYM CONJ_ASSOC] >>
goal_assum $ drule_at Any >> simp[] >> rw[]
>- (CCONTR_TAC >> gvs[] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[]) >>
gvs[new_vars_def, new_vars_constraint_def, pure_vars] >>
rw[] >> rename1 `foo ⊆ _` >> gvs[SUBSET_DEF] >> rw[] >>
first_x_assum drule >> rw[]
)
>- ( (* Handle *)
print_tac "Handle" >>
gvs[inferM_rws] >>
Cases_on `es` >> gvs[] >> Cases_on `t` >> gvs[] >>
Cases_on `t'` >> gvs[inferM_rws] >> every_case_tac >> gvs[] >>
first_x_assum drule_all >> strip_tac >> gvs[] >>
last_x_assum drule >> impl_tac
>- (rw[] >> last_x_assum drule >> simp[]) >>
strip_tac >> gvs[] >>
simp[Once minfer_cases, PULL_EXISTS] >>
ntac 2 $ goal_assum $ drule_at Any >> rw[]
>- (
gvs[assumptions_rel_def] >> simp[PULL_FORALL, aunion_def] >>
rpt gen_tac >> DEP_REWRITE_TAC[lookup_unionWith] >>
DEP_REWRITE_TAC[cj 1 unionWith_thm, cj 2 unionWith_thm] >> simp[] >>
simp[maunion_def, FLOOKUP_FMERGE] >>
every_case_tac >> gvs[] >> rw[] >>
metis_tac[wf_union, domain_union]
)
>- (rw[EXTENSION] >> eq_tac >> rw[] >> simp[])
>- (
simp[cvars_disjoint_def, DISJOINT_ALT] >> rw[] >> CCONTR_TAC >> gvs[SUBSET_DEF] >>
first_x_assum drule >> strip_tac >> first_x_assum drule >> strip_tac >> gvs[]
)
>- (CCONTR_TAC >> gvs[] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (
gvs[new_vars_def, BIGUNION_FRANGE_maunion, GSYM CONJ_ASSOC] >>
simp[new_vars_constraint_def, pure_vars] >>
rw[] >> rename1 `foo ⊆ _` >> gvs[SUBSET_DEF] >> rw[] >>
first_x_assum drule >> rw[]
)
)
>- ( (* Act *)
print_tac "Act" >>
gvs[inferM_rws] >>
Cases_on `es` >> gvs[] >> Cases_on `t` >> gvs[] >> every_case_tac >> gvs[] >>
first_x_assum drule_all >> strip_tac >> gvs[] >>
goal_assum drule >> simp[Once minfer_cases, PULL_EXISTS, GSYM CONJ_ASSOC] >>
goal_assum $ drule_at Any >> simp[] >> rw[] >>
gvs[new_vars_def, new_vars_constraint_def, pure_vars]
)
>- ( (* Alloc *)
print_tac "Alloc" >>
gvs[inferM_rws] >>
Cases_on `es` >> gvs[] >> Cases_on `t` >> gvs[] >>
Cases_on `t'` >> gvs[inferM_rws] >> every_case_tac >> gvs[] >>
first_x_assum drule_all >> strip_tac >> gvs[] >>
last_x_assum drule >> impl_tac
>- (rw[] >> last_x_assum drule >> simp[]) >>
strip_tac >> gvs[] >>
simp[Once minfer_cases, PULL_EXISTS] >>
ntac 2 $ goal_assum $ drule_at Any >> rw[]
>- (
gvs[assumptions_rel_def] >> simp[PULL_FORALL, aunion_def] >>
rpt gen_tac >> DEP_REWRITE_TAC[lookup_unionWith] >>
DEP_REWRITE_TAC[cj 1 unionWith_thm, cj 2 unionWith_thm] >> simp[] >>
simp[maunion_def, FLOOKUP_FMERGE] >>
every_case_tac >> gvs[] >> rw[] >>
metis_tac[wf_union, domain_union]
)
>- (
simp[cvars_disjoint_def, DISJOINT_ALT] >> rw[] >> CCONTR_TAC >> gvs[SUBSET_DEF] >>
first_x_assum drule >> strip_tac >> first_x_assum drule >> strip_tac >> gvs[]
)
>- (
gvs[new_vars_def, BIGUNION_FRANGE_maunion, GSYM CONJ_ASSOC] >>
simp[new_vars_constraint_def, pure_vars] >>
rw[] >> rename1 `foo ⊆ _` >> gvs[SUBSET_DEF] >> rw[] >>
first_x_assum drule >> rw[]
)
)
>- ( (* Length *)
print_tac "Length" >>
gvs[inferM_rws] >>
Cases_on `es` >> gvs[] >> Cases_on `t` >> gvs[] >> every_case_tac >> gvs[] >>
first_x_assum drule_all >> strip_tac >> gvs[] >>
goal_assum drule >> simp[Once minfer_cases, PULL_EXISTS, GSYM CONJ_ASSOC] >>
goal_assum $ drule_at Any >> irule_at Any EQ_REFL >> rw[]
>- (CCONTR_TAC >> gvs[] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (
gvs[new_vars_def, BIGUNION_FRANGE_maunion, GSYM CONJ_ASSOC] >>
simp[new_vars_constraint_def, pure_vars] >>
rw[] >> rename1 `foo ⊆ _` >> gvs[SUBSET_DEF] >> rw[] >>
first_x_assum drule >> rw[]
)
)
>- ( (* Deref *)
print_tac "Deref" >>
gvs[inferM_rws] >>
Cases_on `es` >> gvs[] >> Cases_on `t` >> gvs[] >>
Cases_on `t'` >> gvs[inferM_rws] >> every_case_tac >> gvs[] >>
first_x_assum drule_all >> strip_tac >> gvs[] >>
last_x_assum drule >> impl_tac
>- (rw[] >> last_x_assum drule >> simp[]) >>
strip_tac >> gvs[] >>
simp[Once minfer_cases, PULL_EXISTS] >>
ntac 2 $ goal_assum $ drule_at Any >> rw[]
>- (
gvs[assumptions_rel_def] >> simp[PULL_FORALL, aunion_def] >>
rpt gen_tac >> DEP_REWRITE_TAC[lookup_unionWith] >>
DEP_REWRITE_TAC[cj 1 unionWith_thm, cj 2 unionWith_thm] >> simp[] >>
simp[maunion_def, FLOOKUP_FMERGE] >>
every_case_tac >> gvs[] >> rw[] >>
metis_tac[wf_union, domain_union]
)
>- (rw[EXTENSION] >> eq_tac >> rw[] >> simp[])
>- (
simp[cvars_disjoint_def, DISJOINT_ALT] >> rw[] >> CCONTR_TAC >> gvs[SUBSET_DEF] >>
first_x_assum drule >> strip_tac >> first_x_assum drule >> strip_tac >> gvs[]
)
>- (CCONTR_TAC >> gvs[] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (
gvs[new_vars_def, BIGUNION_FRANGE_maunion, GSYM CONJ_ASSOC] >>
simp[new_vars_constraint_def, pure_vars] >>
rw[] >> rename1 `foo ⊆ _` >> gvs[SUBSET_DEF] >> rw[] >>
first_x_assum drule >> rw[]
)
)
>- ( (* Update *)
print_tac "Update" >>
gvs[inferM_rws] >>
Cases_on `es` >> gvs[] >> Cases_on `t` >> gvs[] >>
Cases_on `t'` >> gvs[inferM_rws] >> every_case_tac >> gvs[] >>
first_x_assum drule_all >> strip_tac >> gvs[] >>
first_x_assum drule >> impl_tac
>- (rw[] >> last_x_assum drule >> simp[]) >>
strip_tac >> gvs[] >>
first_x_assum drule >> impl_tac
>- (rw[] >> last_x_assum drule >> simp[]) >>
strip_tac >> gvs[] >>
simp[Once minfer_cases, PULL_EXISTS, GSYM CONJ_ASSOC] >>
ntac 3 $ goal_assum $ drule_at Any >> simp[] >>
qexists_tac `r''` >> rw[]
>- (
gvs[assumptions_rel_def] >> simp[PULL_FORALL, aunion_def] >>
rpt gen_tac >> DEP_REWRITE_TAC[lookup_unionWith] >>
DEP_REWRITE_TAC[cj 1 unionWith_thm, cj 2 unionWith_thm] >> simp[] >>
simp[maunion_def, FLOOKUP_FMERGE] >>
every_case_tac >> gvs[] >> rw[] >>
DEP_REWRITE_TAC[wf_union] >>
simp[domain_union, AC UNION_ASSOC UNION_COMM] >> metis_tac[]
)
>- (rw[EXTENSION] >> eq_tac >> rw[] >> simp[])
>- (
simp[cvars_disjoint_def, list_disjoint_alt_def, DISJOINT_ALT] >> rw[] >>
CCONTR_TAC >> gvs[SUBSET_DEF] >>
Cases_on `left` >> gvs[] >> Cases_on `t` >> gvs[]
>- (ntac 2 (first_x_assum drule >> strip_tac) >> gvs[])
>- (ntac 2 (first_x_assum drule >> strip_tac) >> gvs[]) >>
Cases_on `t'` >> gvs[] >>
first_x_assum drule >> strip_tac >> first_x_assum drule >> strip_tac >> gvs[]
)
>- (CCONTR_TAC >> gvs[] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (CCONTR_TAC >> gvs[SUBSET_DEF] >> first_x_assum drule >> simp[])
>- (
gvs[new_vars_def, BIGUNION_FRANGE_maunion, GSYM CONJ_ASSOC] >>
simp[new_vars_constraint_def, pure_vars] >>
rw[] >> rename1 `foo ⊆ _` >> gvs[SUBSET_DEF] >> rw[] >>
first_x_assum drule >> rw[]
)
)
>- ( (* True *)
print_tac "True" >>
gvs[inferM_rws] >> every_case_tac >> gvs[] >>
simp[Once minfer_cases, new_vars_def, pure_vars, assumptions_rel_def]
)
>- ( (* False *)
print_tac "False" >>
gvs[inferM_rws] >> every_case_tac >> gvs[] >>
simp[Once minfer_cases, new_vars_def, pure_vars, assumptions_rel_def]
)
>- ( (* Cons and Exception *)
print_tac "Cons/Exception" >>
gvs[inferM_rws] >> every_case_tac >> gvs[] >> pairarg_tac >> gvs[] >>
every_case_tac >> gvs[]
>- ( (* Exception *)
print_tac "Exception" >>
rename1 `_ = OK ((_,_,cs),_)` >>
qsuff_tac
`∃ass css.
LIST_REL (λ(e,ty) (a,c). minfer ns (domain mset) e a c ty)
(ZIP (es,tys)) (ZIP (ass,css)) ∧
assumptions_rel as (FOLDR maunion FEMPTY ass) ∧
BIGUNION (set css) = set (MAP to_mconstraint cs) ∧
cvars_disjoint (ZIP (ass, ZIP (css, tys))) ∧
new_vars (FOLDR maunion FEMPTY ass)
(BIGUNION (set css)) (iFunctions tys Exception) ⊆ {v | n ≤ v ∧ v < m} ∧
LENGTH es = LENGTH tys ∧ LENGTH ass = LENGTH css ∧
n ≤ m`
>- (
rw[] >> gvs[] >>
simp[Once minfer_cases, PULL_EXISTS] >>
rpt $ goal_assum $ drule_at Any >>
simp[MAP2_MAP, MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD] >>
simp[monad_cns_def] >>
gvs[new_vars_def, LIST_TO_SET_MAP, IMAGE_IMAGE,
combinTheory.o_DEF, LAMBDA_PROD, pure_vars] >>
simp[BIGUNION_SUBSET, PULL_EXISTS, GSYM implodeEQ,
mlstringTheory.implode_def] >>
gen_tac >> DEP_REWRITE_TAC[MEM_ZIP] >> simp[] >> strip_tac >> gvs[] >>
gvs[pure_vars_iFunctions, BIGUNION_SUBSET, MEM_MAP, PULL_EXISTS] >>
first_x_assum irule >> simp[EL_MEM]