-
Notifications
You must be signed in to change notification settings - Fork 21
/
rules2.rul
987 lines (871 loc) · 45.4 KB
/
rules2.rul
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
preamble "%include lhs2TeX.fmt\n%include afp.fmt"
-------------------------------------------------------------------------
-- Views
-------------------------------------------------------------------------
view to1 C9 EvK Ev =
let Cnstr =
in
viewset from9 = 9 I C9 10 11
viewset from8 = 8 from9
viewset fromQ4 = Q4 5 6 7 from8
viewset from4 = 4 fromQ4
viewset from3 = 3 from4
viewset from2 = 2 from3
viewset from1 = 1 from2
viewset fromK = K from1
viewset fromE = E fromK
viewset to9 = to8 9 I
viewset to8 = to7 8
viewset to7 = to6 7
viewset to6 = to5 6
viewset to5 = toQ4 5
viewset toQ4 = to4 Q4
viewset to4 = to3 4
viewset to3 = to2 3
viewset to2 = to1 2
viewset to1 = toK 1
viewset toK = toE K
viewset toEvK = toEv EvK
viewset toEv = toE Ev
viewset toE = E
viewset toIm = to4 Im
-------------------------------------------------------------------------
-- Expr
-------------------------------------------------------------------------
scheme expr
= (fiopt); (Gamma); (ICnstrk); (Cnstrk); (sigmak) :- (e) : (isigma); (sigma) ~> (ICnstr); (Cnstr); (Transl)
= fiopt; Gamma; sigmak :-...expr e : sigma ~> Cnstr; Transl
view 9 = fiopt; Gamma; sigmak :-...expr e : sigma ~> Cnstr; Transl
view I = Gamma; sigmak :-...expr e : sigma ~> Cnstr; Transl
view C9 = fiopt; Gamma; sigmak :-...expr e : sigma ~> Transl
view 4 Q4 Im4 = fiopt; Gamma; Cnstrk; sigmak :-...expr e : sigma ~> Cnstr
view 5 6 7 8 = fiopt; Gamma; sigmak :-...expr e : sigma ~> Cnstr
view Im = fiopt; Gamma; ICnstrk; sigmak :-...expr e : isigma ~> ICnstr
view 2 3 = Gamma; Cnstrk; sigmak :-...expr e : sigma ~> Cnstr
view K 1 = Gamma; sigmak :-...expr e : sigma
view E = Gamma :-...expr e : sigma
view Ev = Gamma :-...expr e : sigma ~> Transl
view EvK = Gamma; sigmak :-...expr e : sigma ~> Transl
rules expr.baseImpredE "Type rules for expressions" viewas E =
rule e_int = rule expr.base.e_int
rule e_id = rule expr.base.e_id
rule e_app = rule expr.base.e_app
rule e_lam = rule expr.base.e_lam
rule e_let = rule expr.base.e_let
rules expr.pred "Implicit parameter passing with expected type" viewas EvK =
rule e_id = rule expr.base.e_id
rule e_pred = rule expr.base.e_pred
rules expr.baseExplImpl "Implicit parameter type rules" viewas 9 I =
rule e_app = rule expr.base.e_app
rule e_lam = rule expr.base.e_lam
rules expr.baseExplImplEv "Type rules for expressions" viewas Ev =
rule e_int = rule expr.base.e_int
rule e_id = rule expr.base.e_id
rule e_app = rule expr.base.e_app
rule e_lam = rule expr.base.e_lam
rule e_let_tysig = rule expr.baseObs.e_let_tysig
rule e_pred = rule expr.base.e_pred
rules expr.prog "Program type rule" viewas 4 =
rule e_prog =
cond Gamma === (...) :-> forall ^ alpha.1 (.) alpha.1 -> (...) -> forall ^ alpha.n (.) alpha.n -> (alpha.1, (...), alpha.n), n `elem` [ 2(..) ]
judge expr strongFIOpts ; Gamma ; ([]) ; ([]) ; ANY :- e : _ ; sigma ~> _ ; _ ; Transl
-
judge expr _ ; _ ; _ ; _ ; _ :- e : _ ; sigma ~> _ ; _ ; Transl
rules expr.base "Expression type rules" =
rule e_int viewas fromE toEv Im =
judge fit fiopt ; Gamma :- Int <= (Cnstr..k sigma..k) : sigma ~> Cnstr ; CnstrEq ; coe viewas fromK
-
judge expr fiopt; Gamma; ICnstr..k; Cnstr..k; sigma..k :- int : Int; (viewas toEv = Int viewas fromK = sigma) ~> ICnstr..k; (Cnstr Cnstr..k); int
rule e_id viewas fromE toEvK Im =
judge fit fiopt ; Gamma :- (Cnstr..k sigma.ident) <= (Cnstr..k sigma..k) : sigma ~> Cnstr ; CnstrEq ; coe viewas EvK fromK
cond (ident :-> sigma.ident) `elem` Gamma
-
judge expr fiopt; Gamma; ICnstr..k; Cnstr..k; sigma..k :- ident
: sigma.ident
; (viewas E = sigma.ident viewas EvK fromK = sigma)
~> ICnstr..k; (Cnstr Cnstr..k) ; ((viewas fromK = coe ^^) ident)
rule e_app viewas fromE toEv Im =
judge pred ((pi.i.k :~> Transl.i.k)..._,Gamma) :- (Cnstr.3 pi.a.._) ~> Transl.a.._ : _ viewas from9
judge fit impredFIOpts ; Gamma :- (ICnstr.(3(..)2) isigma.f) <= (ICnstr.(3(..)2) (tvar -> sigma..k)) : _ ~> ICnstr.4 ; CnstrEq ; _ viewas Im
judge fit (viewas 4 = fiopt.a viewas from5 = instLFIOpts) ; Gamma :- isigma.a <= (ICnstr.2 tvar) : _ ~> ICnstr.3 ; CnstrEq ; _ viewas Im
judge expr fiopt.a
; ((viewas from9 = (pi.i.k :~> Transl.i.k)..._,) Gamma)
; ICnstr.1; Cnstr.2
; (viewas from1 = sigma.a viewas Im = tvarv)
:- e.2
: isigma.a
; (viewas toEv = sigma.a viewas fromK = _)
~> ICnstr.2; Cnstr.3 ; Transl.2
cond fiopt.a === if (...) then instLFIOpts else strongFIOpts viewas 4
judge expr fiopt; ((viewas from9 = (pi.i.k :~> Transl.i.k)..._,) Gamma)
; ICnstr..k; Cnstr..k
; ((viewas from9 = pvar =>)
(viewas to1 = ANY viewas from2 Im = tvarv) -> sigma.(viewas from9 = r).k
)
:- e.1
: isigma.f
; ((viewas from9 = pi.a.._ =>) sigma.a -> sigma)
~> ICnstr.1; Cnstr.2 ; Transl.1
cond (pi.i.k :~> Transl.i.k)..._ === inst.pi(pi.a.k._) viewas from9
judge fit fiopt; Gamma :- (pvar..k => tvarv..k) <= sigma..k : (pi.a.k._ => sigma.r.k) ~> Cnstr.1 ; CnstrEq ; _ viewas from9
cond (viewas from9 = pvar, pvar..k, tvarv..k,) tvarv "fresh" viewas from2 Im
-
judge expr fiopt; Gamma; ICnstr..k; Cnstr..k; sigma..k :- (e.1 ^^ e.2)
: (ICnstr.(4(..)2) sigma..k)
; ((viewas from2 = Cnstr.3) sigma)
~> ICnstr.(4(..)2)
; (viewas to8 = Cnstr.3 viewas from9 = Cnstr.(3(..)1))
; ((viewas from9 = \Transl.i.k._ ->) Transl.1 ^^ (viewas from9 = Transl.a.._ ^^) Transl.2)
rule e_lam viewas fromE toEv Im Im4 =
cond ICnstr.4.e === [c | c@(_ :-> sigma) <- ICnstr.4, sigma =/= _ [_] && sigma =/= tvarv ] viewas Im
judge taltGam (fioBindToTyAltsY, meetFIOpts) :- (ICnstr.3 Gamma.p) : ICnstr.4 viewas Im
judge expr fiopt; ((viewas from9 = (pi.i.p :~> Transl.i.p)..._,) (viewas toK Ev = i :-> sigma.i viewas from1 Im Im4 = Gamma.p), Gamma)
; (Cnstr.2 ICnstr.1 ICnstr..k)
; (viewas Im4 = Cnstr.1 ICnstr.4.e Cnstr.2 Cnstr..k viewas from2 = Cnstr.(2(..)1) Cnstr..k)
; sigma.r
:- e : isigma.e; sigma.e
~> ICnstr.3
; Cnstr.3
; Transl.e
cond (pi.i.p :~> Transl.i.p)..._ === inst.pi(pi.a.._) viewas from9
judge fit fiopt; Gamma
:- (ICnstr.4.e Cnstr.2 Cnstr..k ((viewas from9 = pvar =>) tvarv.1 -> tvarv.2)) <= (ICnstr.4.e Cnstr.2 Cnstr..k sigma..k)
: ((viewas from9 = pi.a.._ =>) sigma.p -> sigma.r)
~> Cnstr.1 ; CnstrEq ; _
viewas Im4
judge pat fiopt; Gamma; ([]); sigma.p :- p : _; Gamma.p ~> Cnstr.2 viewas from1 Im
judge fit fiopt; Gamma
:- ((viewas from9 = pvar =>) tvarv.1 -> tvarv.2) <= ((viewas Im = ICnstr..k) sigma..k)
: ((viewas from9 = pi.a.._ =>) sigma.p -> sigma.r)
~> (viewas Im = ICnstr.1 viewas from2 = Cnstr.1) ; CnstrEq ; _
viewas from2 Im
cond (viewas from9 = pvar,) tvarv.i "fresh" viewas from2 Im Im4
-
judge expr fiopt; Gamma
; ICnstrk; Cnstrk
; (viewas to1 = sigma..(viewas toK Ev = i viewas from1 Im = p)->sigma.r viewas from2 Im Im4 = sigma..k)
:- (\(viewas toK Ev = i viewas from1 Im Im4 = p) -> e)
: (ICnstr.4.e ICnstr.3 (sigma.p -> isigma.e))
; ((viewas from9 = Cnstr.(3(..)2) pi.a.._ =>)
Cnstr.3
(viewas toK Ev = sigma.i viewas from1 Im4 = sigma.p) -> sigma.e
)
~> (ICnstr.4.e ICnstr.3)
; Cnstr.3
; ((viewas from9 = \ Transl.i.p._ -> viewas Ev = )
\(viewas toK Ev = i viewas from1 Im = p) -> Transl.e)
rule e_let viewas fromE toEv Im Im4 =
judge expr fiopt
; ((viewas to4 Im Im4 = Gamma.sig viewas fromQ4 = Gamma.sig.exists)
(viewas fromE Im Im4 = , (viewas to2 Im = Gamma.p viewas 3 4 Im4 = Gamma.p.q viewas fromQ4 = Gamma.p.exists))
, Gamma
)
; (ICnstr.2.e ICnstr.1); Cnstr.1
; sigma..k
:- e : isigma; sigma ~> ICnstr.3; Cnstr.2; Transl.e
cond Gamma.p.exists === inst.exists(Gamma.p.q) viewas fromQ4
cond Gamma.p.q === [ i :-> forall alpha..._ (.) sigma
| (i :-> sigma) <- Cnstr.1 Gamma.p
, alpha..._ === ftv(sigma) `minusset` ftv(Cnstr.1 Gamma)
] viewas 3 4 Im4
judge quGam (ftv(Cnstr.1 Gamma)); CoVariant :- (Cnstr.1 Gamma.p) : Gamma.p.q viewas fromQ4
cond ICnstr.2.e === [c | c@(_ :-> sigma) <- ICnstr.2, sigma =/= _ [_] && sigma =/= tvarv ] viewas Im
judge taltGam (fioBindToTyAltsY, joinFIOpts) :- (ICnstr.1 Gamma.p) : ICnstr.2 viewas Im
cond Gamma.sig.exists === inst.exists(Gamma.sig) viewas fromQ4
judge decl ((viewas to4 Im Im4 = Gamma.sig viewas fromQ4 = Gamma.sig.exists), (viewas fromE Im Im4 = Gamma.p,) Gamma)
; (Cnstr.p ICnstr..k)
; ((viewas Im4 = ICnstr.2.e) Cnstr.p Cnstr..k)
:- d
: Gamma.sig ; Gamma.p
~> Cnstr.p ; ICnstr.1 ; Cnstr.1
; Transl.d
-
judge expr fiopt; Gamma
; ICnstr..k; Cnstr..k
; sigma..k
:- ((let) d ^^ (in) e)
: isigma
; sigma
~> ICnstr.3 ; Cnstr.2
; ((let) i (=) Transl.i (in) Transl.e)
rule e_pred viewas toEvK =
judge pred Gamma :- pi ~> Transl.pi : sigma.pi
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (pvar => sigmak) :- e : isigma; (pi => sigma) ~> ICnstr; Cnstr; Transl.e
-
judge expr fiopt; Gamma; ICnstrk; Cnstrk; sigmak :- e : isigma; sigma ~> ICnstr; Cnstr; (Transl.e Transl.pi)
rules expr.baseObs "Type rules for expressions (obsolete)" viewas Ev =
rule e_let =
judge expr fiopt
; ((viewas E = i :-> sigma.i viewas 1 2 = Gamma..p viewas 3 = Gamma..q viewas from4 = Gamma.exists.p) , Gamma)
; ICnstrk; Cnstr.2
; sigma..k
:- e : isigma; sigma ~> ICnstr; Cnstr.3; Transl
cond Gamma.exists.p (=) [ n :-> inst.exists(sigma) | (n :-> sigma) <- Gamma.q.p ] viewas from4
cond Gamma..q === [ i :-> forall ^ Vec(alpha) (.) sigma
| (i :-> sigma) <- Cnstr.(2(..)1) Gamma..p
, Vec(alpha) === ftv(sigma) `minusset` ftv(Cnstr.(2(..)1) Gamma)
] viewas 3
judge quGam (ftv(Cnstr.2 Gamma)); CoVariant :- (Cnstr.2 Gamma..p) : Gamma.q.p viewas fromQ4
judge expr strongFIOpts
; ((viewas from1 = Gamma..p viewas E = i :-> sigma.i), Gamma)
; ICnstr..k
; (Cnstr.1 Cnstr..k)
; sigma..p
:- e.i
: isigma; (viewas E = sigma.i viewas from1 = _) ~> ICnstr; Cnstr.2 ; Transl
judge pat strongFIOpts; Gamma; Cnstrk; ANY :- p : _; Gamma..p ~> Cnstr.1 viewas from1
-
judge expr fiopt; Gamma; ICnstr..k; Cnstr..k; sigma..k
:- ((let) (viewas toK toEv = i viewas from1 = p) (=) e.i ^^ (in) e)
: isigma; sigma ~> ICnstr; Cnstr.3; Transl
rule e_let_tysig =
judge expr fiopt
; ((viewas to2 Ev = i :-> sigma.i viewas from3 = Gamma..i)
(viewas from1 = , (viewas 1 2 = Gamma..p viewas 3 = Gamma..q viewas from4 = Gamma.exists.p))
, Gamma
)
; ICnstrk; Cnstr.2
; sigma..k
:- e : isigma; sigma ~> ICnstr; Cnstr.3; Transl.e
cond Gamma.exists.p (=) [ n :-> inst.exists(sigma) | (n :-> sigma) <- Gamma.q.p ] viewas from4
cond Gamma..q === [ i :-> forall ^ Vec(alpha) (.) sigma
| (i :-> sigma) <- Cnstr.(2(..)1) Gamma..p
, Vec(alpha) === ftv(sigma) `minusset` ftv(Cnstr.(2(..)1) Gamma)
] viewas 3
judge quGam (ftv(Cnstr.2 Gamma)); CoVariant :- (Cnstr.2 Gamma..p) : Gamma.q.p viewas fromQ4
judge expr strongFIOpts
; ((viewas to2 Ev = i :-> sigma.i viewas from3 = Gamma..i)
(viewas from1 = , (viewas from1 = Gamma..p))
, Gamma
)
; ICnstr..k
; (Cnstr.1 Cnstr..k)
; sigma..(viewas to2 = i viewas from3 = q)
:- e.i
: isigma
; (viewas to1 Ev = sigma.i viewas from2 = _) ~> ICnstr; Cnstr.2; Transl.i
cond Gamma..i === i :-> inst.exists(sigma..q) viewas from4
judge qu ([]); CoVariant :- sigma.i : sigma..q ~> _ viewas fromQ4
cond sigma..q === forall ^ Vec(alpha) (.) sigma.i viewas 3
cond sigma..j === ((alpha.j :-> tvarf.j)..._) sigma.i, tvarf.j "fresh" viewas 3
cond Vec(alpha) === ftv(sigma.i) viewas 3
judge pat strongFIOpts; Gamma; Cnstrk; sigma.i :- p : _; Gamma..p ~> Cnstr.1 viewas from1
cond p === i || p === i@(...) viewas from1
-
judge expr fiopt; Gamma
; ICnstr..k; Cnstr..k
; sigma..k
:- ((let) i :: sigma.i; (viewas toK Ev = i viewas from1 = p) (=) e.i ^^ (in) e)
: isigma
; sigma
~> ICnstr; Cnstr.3
; ((let) i (=) Transl.i ^^ (in) Transl.e)
rules expr.C "Type checking/inferencing for expression application with implicit parameters" =
rule app_impl = rule expr.app.e_app_impl_impl
rule app_expl = rule expr.app.e_app_impl_expl
rules expr.explimpl "Type rules for explicit implicit parameters" viewas from9 =
rule e_iapp =
judge expr strongFIOpts; Gamma; ICnstrk; Cnstrk; sigma.a :- e.2 : isigma; _ ~> ICnstr; Cnstr.2 ; Transl.2
judge fit predFIOpts; _ :- (pi.d => sigma.d) <= (pi.a => tvarv) : (_ => sigma.a) ~> _ ; CnstrEq ; _
cond pi.d :> sigma.d `elem` Gamma
judge expr implFIOpts; Gamma; ICnstrk; Cnstrk; (pi.2 => sigma..k) :- e.1 : isigma; (pi.a => sigma) ~> ICnstr; Cnstr.1 ; Transl.1
cond tvarv "fresh"
-
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (sigma..k) :- (e.1 ^^ (! e.2 <: pi.2 !)) : isigma; (Cnstr.2 sigma) ~> ICnstr; Cnstr.(2(..)1) ; (Transl.1 ^^ Transl.2)
rule e_ilam =
judge expr fiopt; ([pi.a :> p:sigma.a],Gamma..p,Gamma); ICnstrk; Cnstrk; sigma.r :- e : isigma; sigma.e ~> ICnstr; Cnstr.3 ; Transl.e
judge pat fiopt; Gamma; ([]); sigma.a :- p : _; Gamma..p ~> Cnstr.2
judge fit predFIOpts; _ :- (pi.d => sigma.d) <= (pi.a => tvarv.2) : (_ => sigma.a) ~> _ ; CnstrEq; _
cond pi.d :> sigma.d `elem` Gamma
judge fit implFIOpts; Gamma :- (pi => tvarv.1) <= sigma..k : (pi.a => sigma.r) ~> Cnstr.1 ; CnstrEq ; _
cond tvarv.1, tvarv.2 "fresh"
-
judge expr fiopt; Gamma; ICnstrk; Cnstrk; sigma..k :- (\(! p <: pi !) -> e) : isigma; (Cnstr.(3(..)2) pi.a => sigma.e) ~> ICnstr; Cnstr.(3(..)1) ; (\p -> Transl.e)
rules expr.proving "Proving for lambda expressions with implicit parameters" viewas from9 =
rule e_app_expl_known viewas from9 =
judge pred (Cnstr.(2(..)1) pi.2 :~> Transl.2,Gamma) :- Cnstr.2 pi.a ~> Transl.a : _
judge expr instLFIOpts; Gamma; ICnstrk; Cnstrk; sigma..pi :- e.2 : isigma; _ ~> ICnstr; Cnstr.2 ; Transl.2
judge pred Gamma :- pi.2 ~> _ : sigma..pi
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (pvar -> sigma..k) :- e.1 : isigma; (pi.a -> sigma) ~> ICnstr; Cnstr.1 ; Transl.1
-
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (sigma..k) :- (e.1 ^^ (! e.2 <~: pi.2 !)) : isigma; (Cnstr.2 sigma) ~> ICnstr; Cnstr.(2(..)1) ; (Transl.1 ^^ Transl.a)
rule e_app_expl_infer viewas from9 =
judge expr instLFIOpts; Gamma; ICnstrk; Cnstrk; sigma..pi :- e.2 : isigma; _ ~> ICnstr; Cnstr.2 ; Transl.2
judge pred Gamma :- Cnstr.1 pi.2 ~> _ : sigma..pi
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (pvar -> sigma..k) :- e.1 : isigma; (pvar..a -> sigma) ~> ICnstr; Cnstr.1 ; Transl.1
cond Cnstr.3 === pvar..a :-> pi.2 , pvar..r
cond pvar..r "fresh"
-
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (sigma..k) :- (e.1 ^^ (! e.2 <~: pi.2 !)) : isigma; (pvar..r -> Cnstr.2 sigma) ~> ICnstr; Cnstr.(3(..)1) ; (Transl.1 ^^ Transl.2)
rule e_app_impl_expl_infer viewas from9 =
judge pred (pi.a :~> Transl.a, Gamma) :- (Cnstr.2 pi.2) ~> Transl.2 : _
judge pred Gamma :- pi.a ~> Transl.a : sigma.a
judge expr instLFIOpts; Gamma; ICnstrk; Cnstrk; ANY :- e.2 : isigma; sigma.a ~> ICnstr; Cnstr.2 ; Transl.2
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (pvar -> sigma..k) :- e.1 : isigma; (pvar.1 -> sigma) ~> ICnstr; Cnstr.1 ; Transl.1
cond pvar..a "fresh"
cond Cnstr.3 === pvar.1 :-> pi.2 , pvar..a
-
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (pvar -> sigma..k) :- (e.1 ^^ (! e.2 !)) : isigma; (pvar..a -> Cnstr.2 sigma) ~> ICnstr; (Cnstr.3,Cnstr.(2(..)1)) ; (Transl.1 ^^ Transl.2)
rule e_app_expl_expl_known viewas from9 =
judge pred (pi.a :~> Transl.a, Gamma) :- (Cnstr.2 pi.2) ~> Transl.2 : _
judge pred Gamma :- pi.a ~> Transl.a : sigma.a
judge expr instLFIOpts; Gamma; ICnstrk; Cnstrk; ANY :- e.2 : isigma; sigma.a ~> ICnstr; Cnstr.2 ; Transl.2
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (pvar -> sigma..k) :- e.1 : isigma; (pi.2 -> sigma) ~> ICnstr; Cnstr.1 ; Transl.1
-
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (pvar -> sigma..k) :- (e.1 ^^ (! e.2 !)) : isigma; (Cnstr.2 sigma) ~> ICnstr; Cnstr.(2(..)1) ; (Transl.1 ^^ Transl.2)
rules expr.rec "Type checking for records" viewas from9 =
rule e_rec_ext viewas from8 =
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (Cnstr.(2(..)1) tvarv.e) :- e : isigma; sigma.e ~> ICnstr; Cnstr.3 ; Transl.e
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (Cnstr.1 tvarv.r) :- r : isigma; sigma.r ~> ICnstr; Cnstr.2 ; Transl.r
judge fit strongFIOpts; Gamma :- ((tvarv.r | l :: tvarv.e)) <= sigma..k : ((sigma.r.k | l :: sigma.e.k)) ~> Cnstr.1 ; CnstrEq ; _
cond tvarv.r, tvarv.e "fresh"
-
judge expr fiopt; Gamma; ICnstrk; Cnstrk; sigma..k :- ((r | l (=) e)) : isigma; ((Cnstr.3 sigma.r | l :: sigma.e)) ~> ICnstr; Cnstr.(3(..)1) ; ((Transl.r | l (=) Transl.e))
rule e_rec_upd viewas from8 =
judge expr fiopt; Gamma; ICnstrk; Cnstrk; (Cnstr.(2(..)1) tvarv.e) :- e : isigma; sigma.e ~> ICnstr; Cnstr.3 ; Transl.e
judge expr fiopt; Gamma; ICnstrk; Cnstrk; ((Cnstr.1 tvarv.r | l :: ANY)) :- r : isigma; ((sigma.r | l :: _)) ~> ICnstr; Cnstr.2 ; Transl.r
judge fit strongFIOpts; Gamma :- ((tvarv.r | l :: tvarv.e)) <= sigma..k : ((sigma.r.k | l :: sigma.e.k)) ~> Cnstr.1 ; CnstrEq ; _
cond tvarv.r, tvarv.e "fresh"
-
judge expr fiopt; Gamma; ICnstrk; Cnstrk; sigma..k :- ((r | l := e)) : isigma; ((Cnstr.3 sigma.r | l :: sigma.e)) ~> ICnstr; Cnstr.(3(..)1) ; ((Transl.r | l := Transl.e))
rule e_rec_sel viewas from8 =
judge expr fiopt; Gamma; ICnstrk; Cnstrk; ((ANY | l :: sigma..k)) :- r : isigma; ((_ | l :: sigma.e)) ~> ICnstr; Cnstr ; Transl.r
-
judge expr fiopt; Gamma; ICnstrk; Cnstrk; sigma..k :- (r (.) l) : isigma; sigma.e ~> ICnstr; Cnstr ; (Transl.r (.) l)
-------------------------------------------------------------------------
-- Decl
-------------------------------------------------------------------------
scheme decl
= (Gamma); (ICnstrk); (Cnstrk) :- (d) : (Gammasig) ; (Gammap) ~> (Cnstrp); (ICnstr); (Cnstr) ; (Transl)
= Gamma; ICnstrk; Cnstrk :-...decl d : Gammasig ; Gammap ~> Cnstrp ; ICnstr; Cnstr ; Transl
view 2 3 4 Im4 = Gamma; Cnstrk :-...decl d : Gammasig ; Gammap ~> Cnstrp ; Cnstr
view 1 = Gamma :-...decl d : Gammasig ; Gammap
view Im = Gamma; ICnstrk :-...decl d : Gammasig ; Gammap ~> Cnstrp ; ICnstr
view E = Gamma :-...decl d : Gammasig ; Gammap
rules decl "Declaration type rules" =
rule d_sig_val =
judge expr strongFIOpts
; Gamma
; ICnstr..k
; Cnstr..k
; (viewas to2 = sigma.i viewas 3 = sigma.i.tvarf viewas from4 = sigma.q)
:- e.i
: isigma
; (viewas to1 = sigma.identv viewas from2 = _) ~> ICnstr.1; Cnstr.2; Transl.i
cond Gamma.identv === [i :-> (viewas to2 = sigma.identv viewas 3 4 = sigma.q viewas fromQ4 = inst.exists(sigma.q))]
judge qu ([]); CoVariant :- sigma.identv : sigma.q ~> _ viewas fromQ4
cond sigma.q === forall ^ alpha..._ (.) sigma.i viewas 3 4
cond sigma.i.tvarf === ((alpha.j :-> tvarf.j)..._) sigma.identv, ^^^ tvarf.j "fresh" viewas 3
cond alpha..._ === ftv(sigma.identv) viewas 3 4
judge pat strongFIOpts; Gamma; ([]); sigma.identv :- p : _; Gamma.p ~> Cnstr.1 viewas from1
cond p === i || p === i@(...) viewas from1
-
judge decl Gamma ; ICnstr..k ; Cnstr..k
:- (identv :: sigma.identv; (viewas toK Ev = identv viewas from1 = p) (=) e.identv)
: Gamma.identv
; (viewas toE = [] viewas from1 = Gamma.p `minusset` Gamma.identv)
~> Cnstr.1 ; (ICnstr.1 ICnstr..k) ; Cnstr.2
; Transl
rule d_val =
judge expr weakFIOpts
; Gamma
; ICnstr..k
; Cnstr..k
; sigma.p
:- e.i
: isigma
; (viewas to1 = sigma.identv viewas from2 = _) ~> ICnstr.1; Cnstr.2; Transl.i
cond Gamma.identv === [identv :-> (viewas toE = sigma.identv viewas from1 = sigma.p)]
judge pat strongFIOpts; Gamma; ([]); tvarv :- p : sigma.p ; Gamma.p ~> Cnstr.1 viewas from1
cond tvarv "fresh" viewas from1
-
judge decl Gamma ; ICnstr..k ; Cnstr..k
:- ((viewas toK Ev = identv viewas from1 = p) (=) e.identv)
: ([])
; (Gamma.identv (viewas from1 = , Gamma.p))
~> Cnstr.1 ; (ICnstr.1 ICnstr..k) ; Cnstr.2
; Transl
-------------------------------------------------------------------------
-- Pat
-------------------------------------------------------------------------
scheme pat
= (fiopt); (Gamma); (Cnstrk); (sigmak) :- (p) : (sigma); (Gammap) ~> (Cnstr)
= fiopt; Gamma; Cnstrk; sigmak :-...pat p : sigma; Gammap ~> Cnstr
view C9 = fiopt; Gamma; sigmak :-...pat p : sigma; Gammap
view 9 = fiopt; Gamma; sigmak :-...pat p : sigma; Gammap ~> Cnstr
view I = sigmak :-...pat p : sigma; Gammap ~> Cnstr
view Im Im4 = fiopt; Gamma; Cnstrk; sigmak :-...pat p : sigma; Gammap ~> Cnstr
view 2 3 4 = Cnstrk; sigmak :-...pat p : sigma; Gammap ~> Cnstr
view 1 = sigmak :-...pat p : Gammap
view E = :-...pat p : sigma; Gammap
rules pat.baseImpred "Pattern type rules" viewas E 4 =
rule p_var = rule pat.base.p_var
rule p_prod = rule pat.base.p_prod
rules pat.base "Type checking/inferencing for pattern" =
rule p_apptop viewas from2 =
judge fit fiopt ; Gamma :- (Cnstr.1 sigma..k) <= sigma..d : sigma ~> Cnstr.2 ; CnstrEq ; coe
cond sigma..d -> () === sigma..p
judge pat fiopt; Gamma; Cnstr..k; _ :- p : sigma..p; Gamma..p ~> Cnstr.1
cond p === p.1 ^^ p.2 (...) p.n, n >= 1
-
judge pat fiopt; Gamma; Cnstr..k; sigma..k :- p : sigma; Gamma..p ~> Cnstr.(2(..)1)
rule p_app viewas from2 =
cond dom(Gamma.(p,1)) `intersect` dom(Gamma.(p,2)) (=) emptyset
judge pat fiopt; Gamma; Cnstr..k; sigma.1.a :- p.2 : _; Gamma.(p,2) ~> Cnstr.2
judge pat fiopt; Gamma; Cnstr..k; _ :- p.1 : (sigma..d -> (sigma.1.a, sigma.2.a, (...), sigma.n.a)); Gamma.(p,1) ~> Cnstr.1
-
judge pat fiopt; Gamma; Cnstr..k; _ :- (p.1 ^^ p.2) : (Cnstr.2 (sigma..d -> (sigma.2.a, (...), sigma.n.a))); (Gamma.(p,1) , Gamma.(p,2)) ~> Cnstr.(2(..)1)
rule p_var =
cond sigma..k /= ANY viewas 2
cond sigma === InstUnExists(sigma..k) viewas fromQ4
cond sigma === sigma..k viewas 1 2 3 4
cond tvarv "fresh" viewas from4
-
judge pat fiopt; Gamma; Cnstr..k; sigma..k :- i
: (viewas E to3 = sigma viewas from4 = tvarv)
; ([i :-> (viewas E to3 = sigma viewas from4 = tvarv)])
~> ((viewas E to3 = [] viewas from4 = [tvarv :-> sigma])
Cnstr..k
)
&
rule p_prod viewas to1 E 4 =
cond dom(Gamma.(p,1)) `intersect` dom(Gamma.(p,2)) (=) emptyset
judge pat fiopt; Gamma; Cnstr.1; sigma.2.k :- p.2 : sigma.2; Gamma.(p,2) ~> Cnstr.2
judge pat fiopt; Gamma; Cnstr..k; sigma.1.k :- p.1 : sigma.1; Gamma.(p,1) ~> Cnstr.1
-
judge pat fiopt; Gamma; Cnstr..k; ((sigma.1.k,sigma.2.k)) :- ((p.1,p.2)) : ((sigma.1,sigma.2)); (Gamma.(p,1) , Gamma.(p,2)) ~> Cnstr.2
&
rule p_con viewas from2 =
cond (unI :-> sigma..u) `elem` Gamma viewas from4
judge fit instFIOpts ; Gamma :- sigma..u <= (v.1 -> v.2) : sigma ~> _ ; CnstrEq ; coe viewas from4
cond v.i "fresh"
-
judge pat fiopt; Gamma; Cnstr..k; _ :- I : sigma; ((tvarv.1,tvarv.2,(...),tvarv.n) -> (tvarv.1,tvarv.2,(...),tvarv.n)) ~> ([]) viewas 2
judge pat fiopt; Gamma; Cnstr..k; _ :- I : sigma; ([]) ~> ([]) viewas from4
-------------------------------------------------------------------------
-- Fit
-------------------------------------------------------------------------
scheme fit
= (fiopt); (Gamma) :- (sigmal) <= (sigmar) : (sigma) ~> (Cnstr) ; (CnstrEq) ; (coe)
= fiopt; Gamma :-...fit sigmal <= sigmar : sigma ~> Cnstr ; CnstrEq ; coe
view 11 = fiopt; Gamma :-...fit sigmal <= sigmar : sigma ~> Cnstr ; CnstrEq ; coe
view C9 = fiopt; Gamma :-...fit sigmal <= sigmar : sigma ~> coe
view 9 = fiopt; Gamma :-...fit sigmal <= sigmar : sigma ~> Cnstr ; coe
view I = Gamma :-...fit sigmal <= sigmar : sigma ~> Cnstr ; coe
view 4 Im Im4 = fiopt :-...fit sigmal <= sigmar : sigma ~> Cnstr
view 2 3 = :-...fit sigmal <= sigmar : sigma ~> Cnstr
view 1 K EvK = :-...fit sigmal <= sigmar : sigma
rules fit.baseImpred4part1 "Rules for fitting (part1)" viewas 4 =
rule f_con = rule fit.base.f_con
rule f_any_l = rule fit.base.f_any_l
rule f_var_l1 = rule fit.bind.f_var_l1
rule f_var_im_l1 = rule fit.bindIm.f_var_im_l1
rule f_forall_l = rule fit.quant.f_forall_l
rule f_forall_r1 = rule fit.quant.f_forall_r1
rule f_forall_r2 = rule fit.quant.f_forall_r2
rules fit.baseImpred4part2 "Rules for fitting (part2)" viewas 4 =
rule f_arrow = rule fit.app.f_arrow
rule f_prod = rule fit.app.f_prod
rule f_var_l2 = rule fit.bind.f_var_l2
rule f_var_im_l2 = rule fit.bindIm.f_var_im_l2
rule f_alt_l1 = rule fit.bind.f_alt_l1
rule f_alt_l2 = rule fit.bind.f_alt_l2
rules fit.base "Rules for fit" =
rule f_con =
cond identc.1 === identc.2
-
judge fit fiopt; Gamma :- identc.1 <= identc.2 : identc.2 ~> ([]) ; ([]) ; id
rule f_any_l viewas from1 =
-
judge fit fiopt; Gamma :- ANY <= sigma : sigma ~> ([]) ; ([]) ; id
&
rule f_any_r viewas from1 =
-
judge fit fiopt; Gamma :- sigma <= ANY : sigma ~> ([]) ; ([]) ; id
rules fit.quant "Fitting/subsumption for quantified types" viewas from4 =
rule f_forall_l =
judge fit fiopt ; Gamma :- sigma.1.i <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
cond (_,sigma.1.i) === inst.tvarv(forall alpha..._ (.) sigma.1)
-
judge fit fiopt ; Gamma :- (forall alpha..._ (.) sigma.1) <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
rule f_forall_r1 =
judge fit fiopt ; Gamma :- sigma.1 <= sigma.2.i : sigma ~> Cnstr ; CnstrEq ; coe
cond (_,sigma.2.i) === inst.tvarv(forall alpha..._ (.) sigma.2)
-
judge fit (fioLeaveRInstY `elem` fiopt) ; Gamma :- sigma.1 <= (forall alpha..._ (.) sigma.2) : sigma ~> Cnstr ; CnstrEq ; coe
&
rule f_forall_r2 =
judge fit fiopt ; Gamma :- sigma.1 <= sigma.2.i : _ ~> Cnstr ; CnstrEq ; coe
cond (_,sigma.2.i) === inst.tvarf(forall alpha..._ (.) sigma.2)
-
judge fit (fioLeaveRInstN `elem` fiopt) ; Gamma :- sigma.1 <= (forall alpha..._ (.) sigma.2) : (Cnstr (forall alpha..._ (.) sigma.2)) ~> Cnstr ; CnstrEq ; coe
rule f_exists_l =
judge fit fiopt ; Gamma :- sigma.1.i <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
cond sigma.1.i === inst.exists(exists alpha..._ (.) sigma.1)
-
judge fit fiopt ; Gamma :- (exists alpha..._ (.) sigma.1) <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
rule f_exists_r1 =
judge fit fiopt ; Gamma :- sigma.1 <= sigma.2.i : sigma ~> Cnstr ; CnstrEq ; coe
cond sigma.2.i === inst.exists(exists alpha..._ (.) sigma.2)
-
judge fit (fioLeaveRInstY `elem` fiopt) ; Gamma :- sigma.1 <= (exists alpha..._ (.) sigma.2) : sigma ~> Cnstr ; CnstrEq ; coe
&
rule f_exists_r2 =
judge fit fiopt ; Gamma :- sigma.1 <= sigma.2.i : sigma ~> Cnstr ; CnstrEq ; coe
cond (tvarv..._,sigma.2.i) === inst.tvarv(exists alpha..._ (.) sigma.2)
-
judge fit (fioLeaveRInstN `elem` fiopt) ; Gamma :- sigma.1 <= (exists alpha..._ (.) sigma.2)
: (Cnstr (exists alpha..._ (.) sigma.2)) ~> (Cnstr restr.(tvarv..._).dom) ; CnstrEq ; coe
rules fit.bind "Fitting/subsumption for tvar binds" viewas 4 =
rule f_var_l1 =
-
judge fit (fioBindToTyAltsN, fioBindLFirstY `elem` fiopt) ; Gamma :- tvarv <= sigma : sigma ~> ([tvarv :-> sigma]) ; CnstrEq ; coe
rule f_var_l2 =
-
judge fit (fioBindToTyAltsN `elem` fiopt) ; Gamma :- tvarv <= sigma : sigma ~> ([tvarv :-> sigma]) ; CnstrEq ; coe
rule f_alt_l1 =
cond sigma === tvarv.2 [ talt.1.._, talt.2.._ ]
-
judge fit fiopt ; Gamma :- (tvarv.1 [ talt.1.._ ]) <= (tvarv.2 [ talt.2.._ ])
: sigma
~> ([tvarv.(1,2) :-> sigma]) ; CnstrEq ; coe
rule f_alt_l2 =
cond sigma === tvarv.1 [ sigma.2 :: tctxtS, talt.1.._ ]
-
judge fit fiopt ; Gamma :- (tvarv.1 [ talt.1.._ ]) <= sigma.2
: sigma
~> ([tvarv.1 :-> sigma]) ; CnstrEq ; coe
rules fit.bindIm "Fitting/subsumption for tvar binds, impredicative" viewas 4 =
rule f_var_im_l1 =
cond sigma /= _ [ _ ]
-
judge fit (fioBindToTyAltsY, fioBindLFirstY `elem` fiopt) ; Gamma :- tvarv <= sigma : (tvarv [ sigma :: tctxtS ]) ~> ([tvarv :-> tvarv [ sigma :: tctxtS ]]) ; CnstrEq ; coe
rule f_var_im_l2 =
cond sigma /= _ [ _ ]
-
judge fit (fioBindToTyAltsY `elem` fiopt) ; Gamma :- tvarv <= sigma : (tvarv [ sigma :: tctxtS ]) ~> ([tvarv :-> tvarv [ sigma :: tctxtS ]]) ; CnstrEq ; coe
rules fit.bindObs "Fitting/subsumption for tvar binds (obsolete)" viewas None =
rule f_bind_r1 =
judge fit fiopt ; Gamma :- sigma.1 <= sigma.2.i : _ ~> _ ; CnstrEq ; coe
-
judge fit fiopt ; Gamma :- sigma.1 <= (tvarv.2 // sigma.2.({(..),i,(..)})) : (tvarv.2 // sigma.2.({(..),i,(..)})) ~> _ ; CnstrEq ; coe
&
rule f_bind_r2 =
judge fit fiopt ; Gamma :- sigma.1 <= sigma.2.({j}) : _ ~> _ ; CnstrEq ; coe
cond {j} === emptyset
cond sigma (=) tvarv.2 // sigma.1, sigma.2.({i})
-
judge fit fiopt ; Gamma :- sigma.1 <= (tvarv.2 // sigma.2.({i})) : sigma ~> ([tvarv.1 :-> sigma]) ; CnstrEq ; coe
rule f_bind_l1 =
judge fit fiopt ; Gamma :- (forall ^ alpha (.) rho.1) <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
-
judge fit fiopt ; Gamma :- (tvarv.1 // forall ^ alpha (.) rho.1) <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
&
rule f_bind_l2 =
judge fit fiopt ; Gamma :- (forall ^ alpha (.) rho.2) <= sigma.1.j : _ ~> Cnstr..j ; CnstrEq ; coe
cond {j} `subset` {i}
cond sigma (=) tvarv.1 // forall ^ alpha (.) rho.2, sigma.1.({i} `minusset` {j})
-
judge fit fiopt ; Gamma :- (tvarv.1 // sigma.1.({i})) <= (forall ^ alpha (.) rho.2) : sigma ~> ([tvarv.1 :-> sigma] Cnstr..({j})) ; CnstrEq ; coe
rules fit.bindAltObs "Fitting/subsumption for tvar binds (obsolete)" viewas None =
rule f_var_l1 =
cond sigma /= _ // _
-
judge fit fioBindToTyAltsY ; Gamma :- tvarv <= sigma : (tvarv // sigma) ~> ([tvarv :-> tvarv // sigma]) ; CnstrEq ; coe
&
rule f_var_l2 =
-
judge fit fioBindToTyAltsN ; Gamma :- tvarv <= sigma : sigma ~> ([tvarv :-> sigma]) ; CnstrEq ; coe
rule f_forall_e =
judge elimb unifyFIOpts; tvarv..._ :- rho..i : rho ~> Cnstr.2
judge fit (fioBindToTyAltsY, meetFIOpts) ; Gamma :- rho..i <= sigma.2 : sigma ~> Cnstr.1 ; CnstrEq ; coe
cond (tvarv..._,rho..i) === inst.tvarv(alpha..._,rho.1)
-
judge fit meetFIOpts ; Gamma :- (forall ^ alpha..._ (.) rho.1) <= sigma.2 : (forall ^ (tvarv..._ `intersect` ftv(rho)) (.) rho) ~> (Cnstr.2 (Cnstr.1 restr.(tvarv..._).dom)) ; CnstrEq ; coe
rules fit.predSymmetric "Fitting/subsumption for predicates (impl/expl match)" viewas from9 =
rule f_pred_expl_impl =
judge fit fiopt; Gamma :- sigma.1 <= (pvar -> sigma.2) : sigma ~> Cnstr ; CnstrEq ; coe
cond Cnstr.1 === pvar.2 :-> pi.1 , pvar
cond pvar "fresh"
-
judge fit fiopt; Gamma :- (pi.1 -> sigma.1) <= (pvar.2 -> sigma.2) : (pi.1 -> sigma) ~> (Cnstr.1, Cnstr) ; CnstrEq ; (\n -> coe (_ ^^ n))
rule f_pred_impl_expl =
judge fit fiopt; (pi.2.i :~> Transl.pi, Gamma) :- (pvar -> sigma.1) <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
cond pi.2.i :~> Transl.pi === inst.pi(pi.2)
cond Cnstr.1 === pvar.1 :-> pi.2 , pvar
cond pvar "fresh"
-
judge fit fiopt; Gamma :- (pvar.1 -> sigma.1) <= (pi.2 -> sigma.2) : (pi.2 -> sigma) ~> (Cnstr.1, Cnstr) ; CnstrEq ; (\Transl.pi -> coe (_ ^^ Transl.pi))
rule f_pred_impl_impl =
judge fit fiopt; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
cond pvar.2.i :~> Transl.pi.._ === inst.pi(pvar.2)
-
judge fit fiopt; Gamma :- (pvar.1 -> sigma.1) <= (pvar.2 -> sigma.2) : (pvar.2 -> sigma) ~> (pvar.1 :-> pvar.2, Cnstr) ; CnstrEq ; (\Transl.pi.._ -> coe (_ ^^ Transl.pi.._))
rules fit.predAsymmetric "Fitting/subsumption for predicates (only impl or expl)" =
rule f_pred_expl_l =
judge pred Gamma :- (Cnstr pi.1) ~> Transl.1 : _
judge fit fiopt; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
-
judge fit fiopt; Gamma :- (pi.1 -> sigma.1) <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; (coe (_ Transl.1))
rule f_pred_expl_r =
judge fit fiopt; (pi.2.i :~> Transl.pi, Gamma) :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
cond pi.2.i :~> Transl.pi === inst.pi(pi.2)
-
judge fit fiopt; Gamma :- sigma.1 <= (pi.2 -> sigma.2) : (Cnstr pi.2 -> sigma) ~> Cnstr ; CnstrEq ; (\ Transl.pi -> coe _)
rule f_pred_impl_l =
judge fit fiopt; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
-
judge fit fiopt; Gamma :- (pvar -> sigma.1) <= sigma.2 : sigma ~> (pvar :-> pempty, Cnstr) ; CnstrEq ; coe
rule f_pred_impl_r =
judge fit fiopt; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
-
judge fit fiopt; Gamma :- sigma.1 <= (pvar -> sigma.2) : sigma ~> (pvar :-> pempty, Cnstr) ; CnstrEq ; coe
rules fit.app "Fitting/subsumption for type applications" viewas from4 =
rule f_arrow =
judge fit (fioLeaveRInstN, fioBindRFirstY, fioBindLFirstY, fiopt)
; Gamma :- (Cnstr.1 sigma.2.a) <= (Cnstr.1 sigma.1.a) : sigma..a ~> Cnstr.2 ; CnstrEq ; coe.a
judge fit fiopt; Gamma :- sigma.1.r <= sigma.2.r : sigma..r ~> Cnstr.1 ; CnstrEq ; coe.r
-
judge fit fiopt; Gamma :- (sigma.1.a -> sigma.1.r) <= (sigma.2.a -> sigma.2.r) : (sigma..a -> Cnstr.2 sigma..r)
~> Cnstr.(2(..)1) ; CnstrEq ; (\a -> coe.r (_ (coe.a ^^ a)))
rule f_prod =
judge fit fiopt; Gamma :- (Cnstr.1 sigma.1.l) <= (Cnstr.1 sigma.2.l) : sigma..l ~> Cnstr.2 ; CnstrEq ; coe.l
judge fit fiopt; Gamma :- sigma.1.r <= sigma.2.r : sigma..r ~> Cnstr.1 ; CnstrEq ; coe.r
-
judge fit fiopt; Gamma :- ((sigma.1.l,sigma.1.r)) <= ((sigma.2.l,sigma.2.r)) : ((sigma..l,Cnstr.2 sigma..r))
~> Cnstr.(2(..)1) ; CnstrEq ; ((let) (l,r) (=) _ (in) (coe.l ^^ l, coe.r ^^ r))
rules fit.rec "Fitting/subsumption for records" viewas from9 =
rule f_rec_empty =
-
judge fit fiopt; Gamma :- (()) <= (()) : (()) ~> ([]) ; CnstrEq ; id
rule f_rec_empty_r =
judge fit fiopt; Gamma :- r.1 <= (()) : r ~> Cnstr ; CnstrEq ; coe
-
judge fit fiopt; Gamma :- ((r.1 | l :: _)) <= (()) : r ~> Cnstr ; CnstrEq ; (coe (_ (-) l))
rule f_rec_ext_eq =
judge fit fiopt; Gamma :- (Cnstr.1 sigma.1) <= (Cnstr.1 sigma.2) : sigma ~> Cnstr.2 ; CnstrEq ; coe.sigma
judge fit fiopt; Gamma :- r.1 <= r.2 : r ~> Cnstr.1 ; CnstrEq ; coe.r
-
judge fit fiopt; Gamma :- ((r.1 | l :: sigma.1)) <= ((r.2 | l :: sigma.2)) : ((r | l :: sigma))
~> Cnstr.(1(..)2) ; CnstrEq ; ((let) r (=) _ (in) (coe.r (r (-) l) | l (=) coe.sigma (r(.)l)))
rule f_rec_ext_neq =
cond l.1 /= l.2
cond rvar "fresh"
-
judge fit fiopt; Gamma :- ((rvar.1 | l.1 :: sigma.1)) <= ((rvar.2 | l.2 :: sigma.2)) : ((rvar | l.1 :: sigma.1 , l.2 :: sigma.2))
~> (rvar.1 :-> (rvar | l.2 :: sigma.2), rvar.2 :-> (rvar | l.1 :: sigma.1)) ; CnstrEq ; id
rules fit.varGADT "Fitting/subsumption for type variables in GADT opening context" viewas from11 =
rule f_var_open =
-
judge fit fioAllowEqOpenY; Gamma :- tvar <= (tvare.e /=/ sigma) : sigma ~> (tvare.e :-> sigma) ; (tvar :-> tvar /=/ sigma) ; id
rules fit.gadt "Fitting/subsumption for GADT related types" viewas from11 =
rule f_eq_lr1 =
judge fit fiopt; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; Transl
-
judge fit fiopt; Gamma :- (tvare /=/ sigma.1) <= (tvare /=/ sigma.2) : (tvare /=/ sigma) ~> Cnstr ; CnstrEq ; Transl
&
rule f_eq_lr2 =
-
judge fit fiopt; Gamma :- (tvare /=/ sigma.1) <= (tvare /=/ sigma.2) : tvare ~> Cnstr ; CnstrEq ; Transl
rule f_eq_l =
judge fit fiopt; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; Transl
-
judge fit fiopt; Gamma :- (_ /=/ sigma.1) <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; Transl
&
rule f_eq_r =
judge fit fiopt; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; Transl
-
judge fit fiopt; Gamma :- sigma.1 <= (tvare /=/ sigma.2) : (tvare /=/ sigma) ~> Cnstr ; CnstrEq ; Transl
-------------------------------------------------------------------------
-- Meet
-------------------------------------------------------------------------
scheme meet
= (fiopt); (Gamma) :- (sigmal) <= (sigmar) : (sigma) ~> (Cnstr) ; (CnstrEq) ; (coe)
= fiopt :-...meet sigmal <+> sigmar : sigma ~> Cnstr
view Im = fiopt :-...meet sigmal <+> sigmar : sigma ~> Cnstr
rules meet "Rules for meet (variant of fit)" =
rule m_forall_l =
judge tboth tvarv.(<+>).._ :- sigma.m : sigma ~> _ ; _ ; Cnstr.2
judge meet fiopt ; Gamma :- sigma.1.i <= sigma.2 : sigma.m ~> Cnstr.1 ; CnstrEq ; coe
cond (tvarv.(<+>).._,sigma.1.i) === inst.(<+>)(forall alpha..._ (.) sigma.1)
-
judge meet fiopt ; Gamma :- (forall alpha..._ (.) sigma.1) <= sigma.2 : (forall tvarv.(<+>).._ (.) sigma) ~> Cnstr.(2(..)1) ; CnstrEq ; coe
rule m_exists_l viewas fromQ4 =
judge tboth tvarv.(<+>).._ :- sigma.m : sigma ~> _ ; Cnstr.j ; Cnstr.2
judge meet fiopt ; Gamma :- sigma.1.i <= sigma.2 : sigma.m ~> Cnstr.1 ; CnstrEq ; coe
cond (tvarv.(<+>).._,sigma.1.i) === inst.(<+>)(forall alpha..._ (.) sigma.1)
-
judge meet fiopt ; Gamma :- (forall alpha..._ (.) sigma.1) <= sigma.2 : (forall tvarv.(<+>).._ (.) Cnstr.j sigma) ~> Cnstr.(2(..)1) ; CnstrEq ; coe
rule m_both_l1 =
-
judge meet fiopt ; Gamma :- (tvarv /=/ ANY) <= sigma : (tvarv /=/ sigma) ~> (tvarv :-> tvarv /=/ sigma) ; CnstrEq ; coe
rule m_both_l2 =
judge meet fiopt ; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
-
judge meet fiopt ; Gamma :- (tvarv /=/ sigma.1) <= sigma.2 : (tvarv /=/ sigma) ~> (tvarv :-> tvarv /=/ sigma) ; CnstrEq ; coe
rule m_both_l3 =
judge meet fiopt ; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
-
judge meet fiopt ; Gamma :- (tvarv.1 /=/ sigma.1) <= (tvarv.2 /=/ sigma.2) : (tvarv.2 /=/ sigma) ~> (tvarv.(1,2) :-> tvarv.2 /=/ sigma) ; CnstrEq ; coe
rule m_alt_l2 =
cond sigma === tvarv.1 [ sigma.2 :: tctxtH, talt.1.._ ]
-
judge meet fiopt ; Gamma :- (tvarv.1 [ talt.1.._ ]) <= sigma.2
: sigma
~> ([tvarv.1 :-> sigma]) ; CnstrEq ; coe
-------------------------------------------------------------------------
-- Join
-------------------------------------------------------------------------
scheme join
= (fiopt); (Gamma) :- (sigmal) <= (sigmar) : (sigma) ~> (Cnstr) ; (CnstrEq) ; (coe)
= fiopt :-...join sigmal <-> sigmar : sigma ~> Cnstr
view Im = fiopt :-...join sigmal <-> sigmar : sigma ~> Cnstr
rules join "Rules for join (variant of fit)" =
rule j_forall_l =
judge tboth tvarv.(<->).._:- sigma.j : sigma ~> _ ; Cnstr.j ; Cnstr.2
judge join fiopt ; Gamma :- sigma.1.i <= sigma.2 : sigma.j ~> Cnstr.1 ; CnstrEq ; coe
cond (tvarv.(<->).._,sigma.1.i) === inst.(<->)(forall alpha..._ (.) sigma.1)
-
judge join fiopt ; Gamma :- (forall alpha..._ (.) sigma.1) <= sigma.2 : (forall tvarv.(<->).._ (.) Cnstr.j sigma) ~> Cnstr.(2(..)1) ; CnstrEq ; coe
rule j_exists_l viewas fromQ4 =
judge tboth tvarv.(<->).._:- sigma.j : sigma ~> _ ; Cnstr.j ; Cnstr.2
judge join fiopt ; Gamma :- sigma.1.i <= sigma.2 : sigma.j ~> Cnstr.1 ; CnstrEq ; coe
cond (tvarv.(<->).._,sigma.1.i) === inst.(<->)(forall alpha..._ (.) sigma.1)
-
judge join fiopt ; Gamma :- (forall alpha..._ (.) sigma.1) <= sigma.2 : (forall tvarv.(<->).._ (.) sigma) ~> Cnstr.(2(..)1) ; CnstrEq ; coe
-------------------------------------------------------------------------
-- Dispatch: fit, meet, join
-------------------------------------------------------------------------
scheme match
= (fiopt); (Gamma) :- (sigmal) <= (sigmar) : (sigma) ~> (Cnstr) ; (CnstrEq) ; (coe)
= fiopt :-...match sigmal <=> sigmar : sigma ~> Cnstr
view Im = fiopt :-...match sigmal <=> sigmar : sigma ~> Cnstr
rules match "Dispatch rules type matching, based on options" =
rule meet =
judge meet fiopt ; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
-
judge match (fioMeetY `elem` fiopt) ; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
rule join =
judge join fiopt ; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
-
judge match (fioJoinY `elem` fiopt) ; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
rule fit =
judge fit fiopt ; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
-
judge match fiopt ; Gamma :- sigma.1 <= sigma.2 : sigma ~> Cnstr ; CnstrEq ; coe
-------------------------------------------------------------------------
-- Quantify
-------------------------------------------------------------------------
scheme qu
= (bv); (coco) :- (sigma) : (sigmaq) ~> (fv)
= bv; coco :-...qu sigma : sigmaq ~> fv
view Q4 I 9 = bv; coco :-...qu sigma : sigmaq ~> fv
scheme quGam
= (bv); (coco) :- (Gamma) : (Gammaq)
= bv; coco :-...quGam Gamma : Gammaq
view Q4 I 9 = bv; coco :-...quGam Gamma : Gammaq
rules qu "Quantifier location inferencing" =
rule q_var_co =
cond v `notElem` bv
-
judge qu bv; CoVariant :- v : (forall ^ v(.)v) ~> ([v])
&
rule q_var_contra =
cond v `notElem` bv
-
judge qu bv; ContraVariant :- v : (exits ^ v(.)v) ~> ([v])
rule q_arrow =
cond v `elem` (fv.1 `intersect` fv.2) `minusset` bv
judge qu (v, bv); ContraVariant :- sigma.1 : sigma.1.q ~> fv.1
judge qu (v, bv); CoVariant :- sigma.2 : sigma.2.q ~> fv.2
-
judge qu bv; _ :- (sigma.1 -> sigma.2) : (forall ^ v (.) sigma.1.q -> sigma.2.q) ~> ((fv.1 `union` fv.2) `minusset` [v])
rule q_prod =
cond v `elem` (fv.1 `intersect` fv.2) `minusset` bv
judge qu (v, bv); CoVariant :- sigma.1 : sigma.1.q ~> fv.1
judge qu (v, bv); CoVariant :- sigma.2 : sigma.2.q ~> fv.2
-
judge qu bv; _ :- ((sigma.1,sigma.2)) : (exits ^ v (.) (sigma.1.q,sigma.2.q)) ~> ((fv.1 `union` fv.2) `minusset` [v])
rule q_app =
cond v `elem` (fv.1 `intersect` fv.2) `minusset` bv
judge qu (v, bv); CoContraVariant :- sigma.1 : sigma.1.q ~> fv.1
judge qu (v, bv); CoContraVariant :- sigma.2 : sigma.2.q ~> fv.2
cond Qu === if coco === CoVariant then forall else exists
cond coco `elem` {CoVariant, ContraVariant}
-
judge qu bv; coco :- (sigma.1 ^^ sigma.2) : (Qu v (.) sigma.1.q ^^ sigma.2.q) ~> ((fv.1 `union` fv.2) `minusset` [v])
rule q_quant =
cond v `notElem` bv
judge qu (v, bv); coco :- sigma : sigma..q ~> fv
-
judge qu bv; coco :- (Qu v (.) sigma) : (Qu v (.) sigma..q) ~> fv `minusset` [v]
rules quGam "Quantifier location inferencing for types in a Gamma" =
rule qg_cons =
judge qu bv; coco :- sigma : sigma..q ~> _
judge quGam bv; coco :- Gamma : Gammaq
-
judge quGam bv; coco :- ([ident :-> sigma,Gamma]) : ([ident :-> sigma..q,Gamma..q])
-------------------------------------------------------------------------
-- Predicates
-------------------------------------------------------------------------
scheme pred
= (Gamma) :- (pi) ~> (Transl) : (sigma)
= Gamma :-...pred pi ~> Transl : sigma
view I 9 C9 Ev EvK = Gamma :-...pred pi ~> Transl : sigma
view E = Gamma :-...pred pi : sigma
rules pred ".." viewas I 9 =
-------------------------------------------------------------------------
-- Type alternative elimination
-------------------------------------------------------------------------
scheme talt
= (fiopt) :- (isigma) : (sigma) ~> (ICnstr)
= fiopt :-...alt isigma : sigma ~> ICnstr
view Im = fiopt :-...alt isigma : sigma ~> ICnstr
rules talt "Type alternative elimination" =
rule ae_alts =
judge talt fiopt :- isigma.tctxtS : sigma ~> ICnstr.3
judge match fiopt ; Gamma :- (ICnstr.1 talt.tctxtS.._) <= isigma.tctxtH : isigma.tctxtS ~> ICnstr.2 ; CnstrEq ; coe
judge match fiopt ; Gamma :- (talt.tctxtH.._, talt.Qu.._) <= ANY : isigma.tctxtH ~> ICnstr.1 ; CnstrEq ; coe
cond | talt.tctxtH.._, talt.Qu.._ | > 0
cond tvarv [ talt.tctxtH.._, talt.Qu.._, talt.tctxtS.._ ] === isigma
-
judge talt fiopt :- isigma : sigma ~> ([tvarv :-> sigma] ICnstr.3)
rule ae_var =
cond tvarv [ _ ] === isigma
-
judge talt fiopt :- isigma : tvarv ~> ([])
rule ae_ty =
-
judge talt fiopt :- sigma : sigma ~> ([])
scheme taltGam
= (fiopt) :- (Gamma) : (ICnstr)
= fiopt :-...(Gamma alt) Gamma : ICnstr
view Im = fiopt :-...(Gamma alt) Gamma : ICnstr
rules taltGam "Type alternative elimination" =
rule aeg_cons =
judge taltGam fiopt :- (ICnstr.1 Gamma) : ICnstr.2
judge talt fiopt :- isigma : sigma ~> ICnstr.1
-
judge taltGam fiopt :- (i :-> sigma, Gamma) : (ICnstr.(2(..)1))
-------------------------------------------------------------------------
-- Type `both' elimination
-------------------------------------------------------------------------
scheme tboth
= (bv) :- (bsigma) : (sigma) ~> (sigmae) ; (Cnstr) ; (Cnstrr)
= bv :-...both bsigma : sigma ~> sigmae ; Cnstr ; Cnstrr
view Im = bv :-...both bsigma : sigma ~> sigmae ; Cnstr ; Cnstrr
rules tboth "Type `both' elimination" =
rule eb_any =
cond tvarv `elem` bv
-
judge tboth bv :- (tvarv /=/ ANY) : tvarv ~> tvarv; ([]) ; ([])
rule eb_var =
judge tboth bv :- sigma.b : sigma ~> tvarv.e ; Cnstr ; Cnstr.r
cond tvarv `elem` bv
-
judge tboth bv :- (tvarv /=/ sigma.b) : tvarv ~> tvarv; Cnstr ; ([tvarv.e :-> tvarv] Cnstr.r)
rule eb_ty =
judge tboth bv :- sigma.b : sigma ~> sigma.e ; Cnstr ; Cnstr.r
cond tvarv `elem` bv
-
judge tboth bv :- (tvarv /=/ sigma.b) : tvarv ~> sigma.e ; ([tvarv :-> sigma.e] Cnstr) ; Cnstr.r