fork download
copy 
  1. :- set_prolog_flag(verbose,silent).
  2. :- set_prolog_flag(occurs_check,true).
  3. :- op(500,yfx,$).
  4. :- prompt(_, '').
  5. :- use_module(library(readutil)).
  6.  
  7. %%%% IDEONE compatibility for mutually recursive predicates %%%%
  8. eqty/2.
  9. unify_oemap/2.
  10. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  11.  
  12. kind(KC,var(X),   K1) :- first(X:K,KC).
  13. kind(KC,F $ G,    K2) :- K2\==row, kind(KC,F,K1->K2),
  14.                          K1\==row, kind(KC,G,K1).
  15. kind(KC,A -> B,    o) :- kind(KC,A,o), kind(KC,B,o).
  16. kind(KC,{R},       o) :- kind(KC,R,row).
  17. kind(KC,[],      row).
  18. kind(KC,[X:T|R], row) :- kind(KC,T,o), kind(KC,R,row).
  19.  
  20. type(KC,C,var(X),     A) --> { first(X:S,C) }, inst_ty(KC,S,A).
  21. type(KC,C,lam(X,E),A->B) --> type(KC,[X:mono(A)|C],E,B),
  22.                              [ kind(KC,A->B,o) ].
  23. type(KC,C,X $ Y,      B) --> type(KC,C,X,A->B), type(KC,C,Y,A1),
  24.                              !, { eqty(A,A1) }. % note the cut !
  25. type(KC,C,let(X=E0,E),T) --> type(KC,C,E0,A),
  26.                              type(KC,[X:poly(C,A)|C],E,T).
  27. type(KC,C,{XEs},    {R}) --> { zip_with('=',Xs,Es,XEs) },
  28.                              type_many(KC,C,Es,Ts),
  29.                              { zip_with(':',Xs,Ts,R) }.
  30. type(KC,C,sel(L,X),   T) --> { first(X:T,R) }, type(KC,C,L,{R}).
  31.  
  32. first(K:V,[K1:V1|Xs]) :- K = K1, V=V1.
  33. first(K:V,[K1:V1|Xs]) :- K\==K1, first(K:V, Xs).
  34.  
  35. inst_ty(KC,poly(C,T),T2) --> { copy_term(t(C,T),t(C,T1)), 
  36.                                free_variables(T,Xs),
  37.                                free_variables(T1,Xs1) },
  38.                              samekinds(KC,Xs,Xs1), { T1=T2 }.
  39. inst_ty(KC,mono(T),   T) --> [].
  40.  
  41. samekinds(KC,[],    []    ) --> [].
  42. samekinds(KC,[X|Xs],[Y|Ys]) --> { X\==Y },
  43.                                 [ kind(KC,X,K), kind(KC,Y,K) ],
  44.                                 samekinds(KC,Xs,Ys).
  45. samekinds(KC,[X|Xs],[X|Ys]) --> [], samekinds(KC,Xs,Ys).
  46.  
  47. zip_with(F,[],    [],    []      ).
  48. zip_with(F,[X|Xs],[Y|Ys],[FXY|Ps]) :- FXY=..[F,X,Y],
  49.                                       zip_with(F,Xs,Ys,Ps).
  50.  
  51. type_many(KC,C,[],    []    ) --> [].
  52. type_many(KC,C,[E|Es],[T|Ts]) --> type(KC,C,E,T),
  53.                                   type_many(KC,C,Es,Ts).
  54.  
  55. variablize(var(X)) :- gensym(t,X).
  56.  
  57. infer_type(KC,C,E,T) :-
  58.   phrase( type(KC,C,E,T), Gs0 ),
  59.   copy_term(Gs0,Gs), 
  60.   (bagof(Ty,X^Y^member(kind(X,Ty,Y),Gs),Tys); Tys=[]),
  61.   free_variables(Tys,Xs),
  62.   maplist(variablize,Xs), % replace free tyvar to var(t)
  63.   maplist(call,Gs). % run all goals in Gs
  64.  
  65. ctx0([ 'Nat':mono(o)
  66.      , 'List':mono(o->o)
  67.      , 'Pair':mono(o->o->o)
  68.      | _
  69.      ],
  70.      [ 'Zero':mono(Nat)
  71.      , 'Succ':mono(Nat -> Nat)
  72.      , 'Nil' :poly([], List$A)
  73.      , 'Cons':poly([], A->((List$A)->(List$A)))
  74.      , 'Pair':poly([], A0->B0->Pair$A0$B0)
  75.      ])
  76.   :- Nat = var('Nat'), List = var('List'), Pair=var('Pair').
  77.  
  78. run(N,T) :- ctx0(KC,C),
  79.   Zero = var('Zero'), Succ = var('Succ'),
  80.   Cons = var('Cons'), Nil = var('Nil'),
  81.   Pair = var('Pair'),
  82.   E0 = let(id=lam(x,var(x)),var(id)$var(id)),     % A->A
  83.   E1 = lam(y,let(x=lam(z,var(y)),var(x)$var(x))), % A->A
  84.   E2 = {[z=lam(x,var(x))]},   % {[z:A->A]}
  85.   E3 = lam(r,sel(var(r),x)),  % {[x:A |R]} -> A
  86.   %E4: {[y:A,x:B |R]} -> Pair$A$B
  87.   E4 = lam(r,Pair$sel(var(r),y)$sel(var(r),x)),
  88.   %E5: {[x:(A->A),y:(B->B)]}
  89.   E5 = {[x=lam(x,var(x)),y=lam(x,var(x))]},
  90.   E6 = E4 $ E5, % Pair $ B->B $ A->A
  91.   %E7: {[y:A |R]} -> Pair $ A $ {[y:A| R]}
  92.   E7 = lam(r,Pair$sel(var(r),y)$var(r)),
  93.   E8 = E7 $ {[y=lam(x,var(x))]}, % Pair $ B->B $ {[y:(B->B)| R]}
  94.   E9 = E7 $ {[]},
  95.   E10 = {[]},
  96.   Es = [E0,E1,E2,E3,E4,E5,E6,E7,E8,E9,E10],
  97.   nth0(N,Es,E), infer_type(KC,C,E,T).
  98.  
  99.  
  100. % related paper:
  101. %
  102. % Membership-Constraints and Complexity in Logic Programming with Sets,
  103. % Frieder Stolzenburg (1996).
  104. % http://l...content-available-to-author-only...r.com/chapter/10.1007%2F978-94-009-0349-4_15
  105. % http://c...content-available-to-author-only...u.edu/viewdoc/summary?doi=10.1.1.54.8356
  106.  
  107. % more advanced notion of type equality at work
  108. eqty(A1,A2) :- (var(A1); var(A2)), !, A1=A2.
  109. eqty({R1},{R2}) :- !, unify_oemap(R1,R2). % permutation(R1,R2), !.
  110. eqty(A1->B1,A2->B2) :- !, eqty(A2,A1), !, eqty(B1,B2). % in case of subtyping
  111. eqty(A,A).
  112.  
  113. % set/map membership with extra-logical builtin \==
  114. % to cut down duplicate answers as sets
  115. memb(X,[X|_]).
  116. memb(X,[Y|L]) :- X \== Y, memb(X,L).
  117.  
  118. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  119. % once inspired by the idea of the paper,
  120. % finite map unification is just like this
  121. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  122.  
  123. % unify finite maps
  124. unify_map(A,B) :- submap_of(A,B), submap_of(B,A).
  125.  
  126. submap_of([], _).
  127. submap_of([X:V|R],M) :- first(X:V1,M), eqty(V,V1), submap_of(R,M).
  128.  
  129.  
  130. % finite map minus
  131. mapminus(A,[],A).
  132. mapminus([],_,[]).
  133. mapminus([X:V|Ps],B,C) :- first(X:V1,B), !, eqty(V,V1) -> mapminus(Ps,B,C).
  134. mapminus([X:V|Ps],B,[X:V|C]) :- mapminus(Ps,B,C).
  135.  
  136.  
  137.  
  138. % unify open ended maps with possibly uninstantiated variable tail at the end
  139. unify_oemap(A,B) :- ( var(A); var(B) ), !, A=B.
  140. unify_oemap(A,B) :-
  141.         split_heads(A,Xs-T1), make_map(Xs,M1),
  142.         split_heads(B,Ys-T2), make_map(Ys,M2),
  143.         unify_oe_map(M1-T1, M2-T2).
  144.  
  145. make_map(L,M) :- setof(X:V,first(X:V,L),M). % remove duplicates
  146. make_map([],[]).
  147.  
  148. split_heads([],[]-[]).
  149. split_heads([X:V|T],[X:V]-T) :- var(T), !, true.
  150. split_heads([X:V|Ps],[X:V|Hs]-T) :- split_heads(Ps,Hs-T).
  151.  
  152. % helper function for unify_oemap
  153. unify_oe_map(Xs-T1,Ys-T2) :- T1==[], T2==[], unify_map(Xs,Ys).
  154. unify_oe_map(Xs-T1,Ys-T2) :- T1==[], submap_of(Ys,Xs), mapminus(Xs,Ys,T2).
  155. unify_oe_map(Xs-T1,Ys-T2) :- T2==[], submap_of(Xs,Ys), mapminus(Ys,Xs,T1).
  156. unify_oe_map(Xs-T1,Ys-T2) :- 
  157.         mapminus(Ys,Xs,L1), append(L1,T,T1),
  158.         mapminus(Xs,Ys,L2), append(L2,T,T2).
  159.  
  160. %% ?- unify_oemap([z:string,y:bool|M1],[y:T,x:int|M2]).
  161. %% M1 = [x:int|_G1426],
  162. %% T = bool,
  163. %% M2 = [z:string|_G1426].
  164.  
  165. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  166.  
  167. main:-
  168. 	process,
  169. 	halt.
  170.  
  171. process:-
  172.     run(0,T0), print(T0), nl,
  173.     run(1,T1), print(T1), nl,
  174.     run(2,T2), print(T2), nl,
  175.     run(3,T3), print(T3), nl,
  176.     run(4,T4), print(T4), nl,
  177.     run(5,T5), print(T5), nl,
  178.     run(6,T6), print(T6), nl,
  179.     run(7,T7), print(T7), nl,
  180.     run(8,T8), print(T8), nl,
  181.     (run(9,T9) -> write("must fail but "), print(T9); print(fail) ), nl,
  182.     run(10,T10), print(T10), nl,
  183. 	true.
  184.  
  185. :- main.
  186.  
  187.  
  188.  
Success #stdin #stdout #stderr 0.04s 7936KB
comments (?)
stdin
copy 
Standard input is empty
stdout
copy 
_G1982->_G1982
_G2654->_G2654
{[z: (_G3700->_G3700)]}
{[x:_G4173|_G4187]}->_G4173
{[y:_G4704,x:_G4701|_G4814]}->var('Pair')$_G4704$_G4701
{[x: (_G5707->_G5707),y: (_G5734->_G5734)]}
var('Pair')$ (_G6508->_G6508)$ (_G6481->_G6481)
{[y:_G2363|_G2450]}->var('Pair')$_G2363${[y:_G2363|_G2450]}
var('Pair')$ (_G3434->_G3434)${[y: (_G3434->_G3434)]}
fail
{[]}
stderr
copy 
Warning: /home/5Jrulb/prog:12:
	Singleton variables: [K1,K]
Warning: /home/5Jrulb/prog:17:
	Singleton variables: [KC]
Warning: /home/5Jrulb/prog:18:
	Singleton variables: [X]
Warning: /home/5Jrulb/prog:32:
	Singleton variables: [Xs]
Warning: /home/5Jrulb/prog:33:
	Singleton variables: [V1]
Warning: /home/5Jrulb/prog:39:
	Singleton variables: [KC]
Warning: /home/5Jrulb/prog:41:
	Singleton variables: [KC]
Warning: /home/5Jrulb/prog:47:
	Singleton variables: [F]
Warning: /home/5Jrulb/prog:51:
	Singleton variables: [KC,C]
Warning: /home/5Jrulb/prog:78:
	Singleton variables: [Zero,Succ,Cons,Nil]
https://ideone.com/x13a5O
language:
Prolog (swi 7.6.4)
created:
7 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!