• API
• FAQ
• Tools
• Archive
SHARE
TWEET

# HM type inference/checking in Prolog

a guest Mar 22nd, 2015 343 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. % var(X).
2. % int(N).
3. % true.
4. % false.
6. % eq(E1,E2).
7. % if(B,E1,E2).
8. % pair(E1,E2).
9. % fst(E).
10. % snd(E).
11. % abs(X,E).
12. % app(E1,E2).
13. % let(X,E1,E2).
14.
15. bigstep(var(X),R,V) :-
16.     lookup(R,X,V).
17. bigstep(int(N),_,int(N)).
18. bigstep(bool(B),_,bool(B)).
20.     bigstep(N1,R,int(V1)),
21.     bigstep(N2,R,int(V2)),
22.     V is V1 + V2.
23. bigstep(eq(E1,E2),R,true) :-
24.     bigstep(E1,R,int(V)),
25.     bigstep(E2,R,int(V)).
26. bigstep(eq(E1,E2),R,false) :-
27.     bigstep(E1,R,int(V1)),
28.     bigstep(E2,R,int(V2)),
29.     V1 \== V2.
30. bigstep(if(B,E1,_),R,V) :-
31.     bigstep(B,R,true),
32.     bigstep(E1,R,V).
33. bigstep(if(B,_,E2),R,V) :-
34.     bigstep(B,R,false),
35.     bigstep(E2,R,V).
36. bigstep(pair(E1,E2),R,pair(V1,V2)) :-
37.     bigstep(E1,R,V1),
38.     bigstep(E2,R,V2).
39. bigstep(fst(E),R,V) :-
40.     bigstep(E,R,pair(V,_)).
41. bigstep(snd(E),R,V) :-
42.     bigstep(E,R,pair(_,V)).
43. bigstep(abs(X,E),R,clo(abs(X,E),R)).
44. bigstep(app(E1,E2),R,V) :-
45.     bigstep(E1,R,clo(abs(X,B),RLex)),
46.     bigstep(E2,R,V2),
47.     bigstep(B,[v(X,V2)|RLex],V).
48. bigstep(let(X,E1,E2),R,V) :-
49.     bigstep(E1,R,V1),
50.     bigstep(E2,[v(X,V1)|R],V).
51.
52. type(G,var(X),T) :-
53.     lookup(G,X,T).
54. type(_,int(_),int).
55. type(_,true,bool).
56. type(_,false,bool).
58.     type(G,N1,int),
59.     type(G,N2,int).
60. type(G,eq(N1,N2),bool) :-
61.     type(G,N1,int),
62.     type(G,N2,int).
63. type(G,if(B,N1,N2),T) :-
64.     type(G,B,bool),
65.     type(G,N1,T),
66.     type(G,N2,T).
67. type(G,pair(E1,E2),prod(T1,T2)) :-
68.     type(G,E1,T1),
69.     type(G,E2,T2).
70. type(G,fst(E),T) :-
71.     type(G,E,prod(T,_)).
72. type(G,snd(E),T) :-
73.     type(G,E,prod(_,T)).
74. type(G,abs(X,E),arrow(T1,T2)) :-
75.     type([v(X,T1)|G],E,T2).
76. type(G,app(E1,E2),X) :-
77.     type(G,E1,T1),
78.     type(G,E2,T2),
79.     T1 = arrow(T2,X).
80. type(G,let(X,E1,E2),T) :-
81.     type(G,E1,T1),
82.     type([v(X,T1)|G],E2,T).
83.
85. example2(app(E1,abs(x,add(var(x),int(1))))) :- example1(E1).
86. example3(app(E2,int(3))) :- example2(E2).
87. example4(let(f,abs(x,var(x)),pair(app(var(f),int(5)),app(var(f),true)))).
88. example5(abs(y,let(f,abs(x,var(y)),pair(app(var(f),int(5)),app(var(f),true))))).
89.
90. poly(G,var(X),I) :-
91.     lookup(G,X,scheme(B,T)),
92.     instantiate(B,T,I).
93. poly(_,int(_),int).
94. poly(_,true,bool).
95. poly(_,false,bool).
97.     poly(G,N1,int),
98.     poly(G,N2,int).
99. poly(G,eq(N1,N2),bool) :-
100.     poly(G,N1,int),
101.     poly(G,N2,int).
102. poly(G,if(B,N1,N2),T) :-
103.     poly(G,B,bool),
104.     poly(G,N1,T),
105.     poly(G,N2,T).
106. poly(G,pair(E1,E2),prod(T1,T2)) :-
107.     poly(G,E1,T1),
108.     poly(G,E2,T2).
109. poly(G,fst(E),T) :-
110.     poly(G,E,prod(T,_)).
111. poly(G,snd(E),T) :-
112.     poly(G,E,prod(_,T)).
113. poly(G,abs(X,E),arrow(T1,T2)) :-
114.     poly([v(X,scheme([],T1))|G],E,T2).
115. poly(G,app(E1,E2),X) :-
116.     poly(G,E1,T1),
117.     poly(G,E2,T2),
118.     T1 = arrow(T2,X).
119. poly(G,let(X,E1,E2),T) :-
120.     poly(G,E1,T1),
121.     term_variables(T1,T1Free),
122.     term_variables(G,GFree),
123.     subtract(T1Free,GFree,Vars),
124.     poly([v(X,scheme(Vars,T1))|G],E2,T).
125.
126. instantiate(Vars,T,I) :-
127.     copy_term(T,I),
128.     unify_bound(Vars,T,I), !.
129.
130. unify_bound(Vars,Var,_) :-
131.     var(Var),
132.     memberchk(Var,Vars).
133. unify_bound(Vars,Var1,Var2) :-
134.     var(Var1),
135.     \+ memberchk(Var1,Vars),
136.     Var1 = Var2.
137. unify_bound(Vars,arrow(A1,A2),arrow(B1,B2)) :-
138.     unify_bound(Vars,A1,B1),
139.     unify_bound(Vars,A2,B2).
140. unify_bound(Vars,pair(A1,A2),pair(B1,B2)) :-
141.     unify_bound(Vars,A1,B1),
142.     unify_bound(Vars,A2,B2).
143.
144. lookup(List,X,N) :-
145.     memberchk(v(X,N),List).
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.
Top