fork download
copy 
  1. :- set_prolog_flag(verbose,silent).
  2. :- prompt(_, '').
  3. :- use_module(library(readutil)).
  4.  
  5. :- set_prolog_flag(occurs_check,true).
  6. :- op(500,xfy,$).
  7.  
  8. % STLC type system specification
  9.  
  10. type(C,var(X),      T1) :- first(X:T,C), instantiate(T,T1).                            
  11. type(C,lam(X,E),A -> B) :- type([X:mono(A)|C],E,B).                             
  12. type(C,X $ Y,        B) :- type(C,X,A -> B), type(C,Y,A).                               
  13. type(C,let(X=E0,E1), T) :- type(C,E0,A), type([X:poly(C,A)|C],E1,T).
  14.  
  15. instantiate(poly(C,T),T1) :- copy_term(t(C,T),t(C,T1)).                         
  16. instantiate(mono(T),T).
  17.  
  18. first(K:V,[K1:V1|_]) :- K = K1, V=V1.
  19. first(K:V,[K1:_|Xs]) :- K\==K1, first(K:V, Xs). % no cut but use var cmp
  20.  
  21. main:-
  22. 	process,
  23. 	halt.
  24.  
  25. type_and_print(C,E,T) :- type(C,E,T), print(E : T).
  26.  
  27. process:-
  28.     /* your code goes here */
  29. 	type_and_print([],lam(x,var(x)),_), nl,
  30. 	type_and_print([],lam(x,lam(y,var(y)$var(x))),_), nl,
  31. 	type_and_print([],let(id=lam(x,var(x)),var(id)$var(id)),_), nl,
  32. 	true.
  33.  
  34. :- main.
Success #stdin #stdout 0.04s 7424KB
comments (?)
stdin
copy 
Standard input is empty
stdout
copy 
lam(x,var(x)): (_G1482->_G1482)
lam(x,lam(y,var(y)$var(x))): (_G1512-> (_G1512->_G1524)->_G1524)
let(id=lam(x,var(x)),var(id)$var(id)): (_G1622->_G1622)
https://ideone.com/cI0oXR
HM type system specification using Prolog
language:
Prolog (swi 7.6.4)
created:
9 years ago
visibility:
public

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!