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.
  5. % add(N1,N2).
  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)).
  19. bigstep(add(N1,N2),R,int(V)) :-
  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).
  57. type(G,add(N1,N2),int) :-
  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.  
  84. example1(abs(a,abs(b,add(int(2),app(var(a),add(var(b),int(3))))))).
  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).
  96. poly(G,add(N1,N2),int) :-
  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. OK, I Understand
Top