2:- module(alphaConversionDRT,[alphaConvertDRS/2]).    3
    4:- use_module(library(lists),[member/2]).    5:- use_module(semlib(errors),[warning/2]).    6
    7
    8/*========================================================================
    9   Alpha Conversion (introducing substitutions)
   10========================================================================*/
   11
   12alphaConvertDRS(B1,B2):-
   13   alphaConvertDRS(B1,[]-_,[]-_,B2), !.
   14
   15
   16/*========================================================================
   17   Variable
   18========================================================================*/
   19
   20variable(X):- var(X), !.
   21variable(X):- functor(X,'$VAR',1), !.
   22
   23
   24/*========================================================================
   25   Alpha Conversion (terms)
   26========================================================================*/
   27
   28alphaConvertVar(X,Vars,New):-
   29   variable(X), !,
   30   (
   31      member(sub(Z,Y),Vars),           %%% BOUND
   32      X==Z, !,
   33      New=Y
   34   ;
   35      New=X                            %%% FREE
   36   ).
   37
   38alphaConvertVar(X,_,X).
   39
   40
   41/*========================================================================
   42   Alpha Conversion (DRSs)
   43========================================================================*/
   44
   45alphaConvertDRS(X1,Var-Var,Ptr-Ptr,X2):-
   46   variable(X1), !,
   47   alphaConvertVar(X1,Var,X2).
   48
   49alphaConvertDRS(lam(X,B1),Vars-Vars,Ptrs,lam(Y,B2)):- !,
   50   alphaConvertDRS(B1,[sub(X,Y)|Vars]-_,Ptrs,B2).
   51
   52alphaConvertDRS(B1:drs(D,C),Vars,Ptr1-Ptr2,B2:Drs):- !, 
   53   alphaConvertDRS(drs(D,C),Vars,[sub(B1,B2)|Ptr1]-Ptr2,Drs).
   54
   55alphaConvertDRS(drs([],[]),Vars-Vars,Ptr-Ptr,drs([],[])):- !.
   56
   57alphaConvertDRS(drs([],[B1:I:C1|Conds1]),Vars1-Vars2,Ptr1-Ptr3,drs([],[B2:I:C2|Conds2])):- !,
   58   alphaConvertVar(B1,Ptr1,B2),
   59   alphaConvertCondition(C1,Vars1,Ptr1-Ptr2,C2), 
   60   alphaConvertDRS(drs([],Conds1),Vars1-Vars2,Ptr2-Ptr3,drs([],Conds2)).
   61
   62alphaConvertDRS(drs([B1:I:Ref|L1],C1),Var1-Var2,Ptr1-Ptr2,drs([B2:I:New|L2],C2)):- !,
   63   alphaConvertVar(B1,Ptr1,B2),
   64   alphaConvertDRS(drs(L1,C1),[sub(Ref,New)|Var1]-Var2,Ptr1-Ptr2,drs(L2,C2)).
   65
   66alphaConvertDRS(alfa(Type,B1,B2),Var1-Var3,Ptr1-Ptr3,alfa(Type,B3,B4)):- !,
   67   alphaConvertDRS(B1,Var1-Var2,Ptr1-Ptr2,B3),
   68   alphaConvertDRS(B2,Var2-Var3,Ptr2-Ptr3,B4).
   69
   70alphaConvertDRS(merge(B1,B2),Var1-Var3,Ptr1-Ptr3,merge(B3,B4)):- !,
   71   alphaConvertDRS(B1,Var1-Var2,Ptr1-Ptr2,B3),
   72   alphaConvertDRS(B2,Var2-Var3,Ptr2-Ptr3,B4).
   73
   74alphaConvertDRS(app(E1,E2),Var-Var,Ptr1-Ptr3,app(E3,E4)):- !,
   75   alphaConvertDRS(E1,Var-_,Ptr1-Ptr2,E3),
   76   alphaConvertDRS(E2,Var-_,Ptr2-Ptr3,E4).
   77
   78alphaConvertDRS(sdrs([],[]),Var-Var,Ptr-Ptr,sdrs([],[])):- !.
   79
   80alphaConvertDRS(sdrs([],[I:C1|L1]),Var1-Var2,Ptr1-Ptr3,sdrs([],[I:C2|L2])):- !,
   81   alphaConvertCondition(C1,Var1,Ptr1-Ptr2,C2),
   82   alphaConvertDRS(sdrs([],L1),Var1-Var2,Ptr2-Ptr3,sdrs([],L2)).
   83
   84alphaConvertDRS(sdrs([B1|L1],C1),Var1-Var3,Ptr1-Ptr3,sdrs([B2|L2],C2)):- !,
   85   alphaConvertDRS(B1,Var1-Var2,Ptr1-Ptr2,B2),
   86   alphaConvertDRS(sdrs(L1,C1),Var2-Var3,Ptr2-Ptr3,sdrs(L2,C2)).
   87
   88alphaConvertDRS(lab(Ref,B1),Var1-[sub(Ref,New)|Var2],Ptr,lab(New,B2)):- !,
   89   alphaConvertDRS(B1,Var1-Var2,Ptr,B2).
   90
   91alphaConvertDRS(sub(B1,B2),Var1-Var3,Ptr1-Ptr3,sub(B3,B4)):- !,
   92   alphaConvertDRS(B1,Var1-Var2,Ptr1-Ptr2,B3),
   93   alphaConvertDRS(B2,Var2-Var3,Ptr2-Ptr3,B4).
   94
   95alphaConvertDRS(Sym,Vars-Vars,Ptr-Ptr,Sym):- atomic(Sym), !.
   96
   97alphaConvertDRS(U,_,_,_):- !,
   98   warning('Unknown DRS expression: ~p',[U]), fail.
   99
  100
  101/*========================================================================
  102   Alpha Conversion (DRS-Conditions)
  103========================================================================*/
  104
  105alphaConvertCondition(nec(B1),Vars,Ptr,nec(B2)):- !,
  106   alphaConvertDRS(B1,Vars-_,Ptr,B2).
  107
  108alphaConvertCondition(pos(B1),Vars,Ptr,pos(B2)):- !,
  109   alphaConvertDRS(B1,Vars-_,Ptr,B2).
  110
  111alphaConvertCondition(not(B1),Vars,Ptr,not(B2)):- !,
  112   alphaConvertDRS(B1,Vars-_,Ptr,B2).
  113
  114alphaConvertCondition(prop(X,B1),Vars,Ptr,prop(Y,B2)):- !,
  115   alphaConvertVar(X,Vars,Y),
  116   alphaConvertDRS(B1,Vars-_,Ptr,B2).
  117
  118alphaConvertCondition(imp(B1,B2),Var,Ptr1-Ptr3,imp(B3,B4)):- !,
  119   alphaConvertDRS(B1,Var -Var1,Ptr1-Ptr2,B3),
  120   alphaConvertDRS(B2,Var1-_,   Ptr2-Ptr3,B4).
  121
  122alphaConvertCondition(duplex(Type,B1,X,B2),Var,Ptr1-Ptr3,duplex(Type,B3,Y,B4)):- !,
  123   alphaConvertDRS(B1,Var-Var1,Ptr1-Ptr2,B3),
  124   alphaConvertVar(X,Var1,Y),
  125   alphaConvertDRS(B2,Var1-_,Ptr2-Ptr3,B4).
  126
  127alphaConvertCondition(or(B1,B2),Var,Ptr1-Ptr3,or(B3,B4)):- !,
  128   alphaConvertDRS(B1,Var-_,Ptr1-Ptr2,B3),
  129   alphaConvertDRS(B2,Var-_,Ptr2-Ptr3,B4).
  130
  131alphaConvertCondition(pred(Arg1,Sym,Type,Sense),Var,Ptr-Ptr,pred(Arg2,Sym,Type,Sense)):- !,
  132   alphaConvertVar(Arg1,Var,Arg2).
  133
  134alphaConvertCondition(rel(Arg1,Arg2,Sym),Var,Ptr-Ptr,rel(Arg3,Arg4,Sym)):- !,
  135   alphaConvertVar(Arg1,Var,Arg3),
  136   alphaConvertVar(Arg2,Var,Arg4).
  137
  138alphaConvertCondition(rel(Arg1,Arg2,'=',0),Var,Ptr,Rel):- !,
  139   warning('Unexpected relation symbol: ~p = ~p',[Arg1,Arg2]),
  140   alphaConvertCondition(eq(Arg1,Arg2),Var,Ptr,Rel).
  141
  142alphaConvertCondition(rel(Arg1,Arg2,Sym,Sense),Var,Ptr-Ptr,rel(Arg3,Arg4,Sym,Sense)):- !,
  143   alphaConvertVar(Arg1,Var,Arg3),
  144   alphaConvertVar(Arg2,Var,Arg4).
  145
  146alphaConvertCondition(role(Arg1,Arg2,Sym,Dir),Var,Ptr-Ptr,role(Arg3,Arg4,Sym,Dir)):- !,
  147   alphaConvertVar(Arg1,Var,Arg3),
  148   alphaConvertVar(Arg2,Var,Arg4).
  149
  150alphaConvertCondition(named(X,Sym,Type,Sense),Var,Ptr-Ptr,named(Y,Sym,Type,Sense)):- !,
  151   alphaConvertVar(X,Var,Y).
  152
  153alphaConvertCondition(card(X,Sym1,T),Vars,Ptr-Ptr,card(Y,Sym2,T)):- !,
  154   alphaConvertVar(X,Vars,Y),
  155   alphaConvertVar(Sym1,Vars,Sym2).
  156
  157alphaConvertCondition(timex(X,Sym),Vars,Ptr-Ptr,timex(Y,Sym)):- !,
  158   alphaConvertVar(X,Vars,Y).
  159
  160alphaConvertCondition(eq(X1,X2),Vars,Ptr-Ptr,eq(Y1,Y2)):- !,
  161   alphaConvertVar(X1,Vars,Y1),
  162   alphaConvertVar(X2,Vars,Y2).
  163
  164alphaConvertCondition(U,_,_,_):- !,
  165   warning('Unknown condition: ~p',[U]), fail