-
Notifications
You must be signed in to change notification settings - Fork 2
/
typing.elpi
164 lines (114 loc) · 3.88 KB
/
typing.elpi
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
accumulate errors.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Typing of miniFP programs. (Figure 10.3)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
kind ty type.
type int, bool, string ty.
type tunit ty.
%type sum ty -> ty -> ty. % Sum types '*'
type lst ty -> ty. % Lists
type arr ty -> ty -> ty. % Functional arrow type
type bigarr ty -> ty -> ty. % Higherarity arrow type
%type utm ty. % untyped lambda terms
type typeof tm -> ty -> prop. % Top-level predicate
type type_constr constructor -> list ty -> ty -> prop.
type type_match ty -> list clause -> ty -> prop.
type type_match_rule ty -> clause -> ty -> prop.
% Literals
typeof (lit unit) tunit.
typeof (lit (i _I)) int.
typeof (lit (b _B)) bool.
typeof (lit (s _S)) string.
% Control flow
typeof (if_then_else P Q R) A :-
typeof P bool,
typeof Q A,
typeof R A.
typeof (fix M) A :- pi x\ typeof x A => typeof (M x) A2,
(A = A2, !; err_wrong_type (M x) A A2 (fix M), fail).
typeof (let M R) A :- typeof M B, pi x\ typeof x B => typeof (R x) A.
typeof (new R) B :- pi x\ typeof x A_ => typeof (R x) B.
typeof (tprint _T) tunit.
typeof (failwith T) A_ :- typeof T string.
% Abstractions and applications
typeof (lam R) (arr A B) :- pi x\ typeof x A => typeof (R x) B.
typeof (backslash R) (bigarr A B) :- pi x\ typeof x A => typeof (R x) B.
typeof (app M N) B :-
typeof M (arr A B),
typeof N A2,
(A = A2, !; err_wrong_type N A A2 (app M N), fail).
typeof (arobase M N) A :-
typeof M (bigarr B A),
typeof N B2,
(B = B2, !; err_wrong_type N B B2 (arobase M N), fail).
% Specials
type_spec add (arr int (arr int int)).
type_spec mul (arr int (arr int int)).
type_spec sub (arr int (arr int int)).
type_spec equal (arr A (arr A bool)).
type_spec and (arr bool (arr bool bool)).
type_spec or (arr bool (arr bool bool)).
type_spec seq (arr tunit (arr A A)).
type_args B [] B.
type_args (arr A B) [E|TL] C :-
typeof E A,
type_args B TL C.
typeof (special Spec Args) B :-
type_spec Spec A,
type_args A Args B.
% Variants
% builtins pairs
type t_pair ty -> ty -> ty.
type pair constructor.
type_constr pair [A, B] (t_pair A B).
% builtins lists
type t_list ty -> ty.
type list_cons constructor.
type list_empty constructor.
type_constr list_empty [] (t_list A_).
type_constr list_cons [A, (t_list A)] (t_list A).
type_check [] [].
type_check [E|TL] [Ty|TyL] :-
typeof E Ty,
type_check TL TyL.
typeof (variant Constr Args) A :-
type_constr Constr Typs A,
type_check Args Typs.
% Patterns
type_pat pany A_.
type_pat (plit I) A :- typeof (lit I) A.
type_pat (pvar T) A :- typeof T A.
type_pat (pnom N) A :- typeof N A.
type_pat (pbackslash R) (bigarr A B) :-
pi x\ typeof x A => type_pat (R x) B.
type_pat (parobase P T) B :-
type_pat P (bigarr A B),
typeof T A.
type_checkp [] [].
type_checkp [P|TL] [Ty|TyL] :-
type_pat P Ty,
type_checkp TL TyL.
type_pat (pvariant Constr Pats) A :-
type_constr Constr Typs A,
type_checkp Pats Typs.
% Matching
typeof (match Exp Rules) A :- typeof Exp B, type_match B Rules A.
type_match _ [] _.
type_match A (R::Rs) B :-
type_match_rule A R B, type_match A Rs B.
type_match_rule A (arr Pat Result) B :- type_pat Pat A, typeof Result B.
type_match_rule A (nab R) B :- pi x\ typeof x C_ => type_match_rule A (R x) B.
type_match_rule A (all R) B :- pi x\ typeof x C_ => type_match_rule A (R x) B.
% Rows
nth 0 (HD::_) HD.
nth N (_::TL) B :-
NM1 is N - 1,
nth NM1 TL B.
nth _N [] _B :- false.
typeof (select N Row) B :-
type_row Row TR, nth N TR B.
type_row (rowfix Row) TR :-
pi r \ type_row r TR => type_row (Row r) TR.
type_row (row (HD::TL)) (THD::TTL) :-
typeof HD THD, type_row (row TL) TTL.
type_row (row []) [].