2:- module(betaConversionDRT,[betaConvert/2]).    3
    4:- use_module(boxer(alphaConversionDRT),[alphaConvertDRS/2]).    5:- use_module(boxer(mergeDRT),[mergeDrs/2]).    6:- use_module(semlib(errors),[warning/2]).    7:- use_module(semlib(options),[option/2]).    8
    9
   10/* ========================================================================
   11   Beta-Conversion (introducing stack)
   12======================================================================== */
   13
   14betaConvert(X,Y):- betaConvert(X,Y,[]), !.
   15
   16betaConvert(X,X):- warning('beta-conversion failed for ~p',[X]).
   17
   18
   19/* ========================================================================
   20   Beta-Conversion (core stuff)
   21======================================================================== */
   22
   23betaConvert(X,Y,[]):- var(X), !, Y=X.
   24
   25betaConvert(X,Y,L):-  var(X), !, wrapArguments(L,X,Y).
   26
   27betaConvert(app(Functor,Argument),Result,Stack):- 
   28   nonvar(Functor), !,
   29   alphaConvertDRS(Functor,Converted),
   30   betaConvert(Argument,ConArg),               %%% much faster this way!
   31   betaConvert(Converted,Result,[ConArg|Stack]).
   32
   33betaConvert(lam(X,Formula),Result,[X|Stack]):- !,
   34   betaConvert(Formula,Result,Stack).
   35
   36betaConvert(lam(X,Formula),lam(X,Result),[]):- !,
   37   betaConvert(Formula,Result).
   38
   39betaConvert(merge(B1,B2),Result,[]):- !,
   40   betaConvert(B1,K1),
   41   betaConvert(B2,K2),
   42   mergeDrs(merge(K1,K2),Result).
   43
   44betaConvert(sdrs([],C),sdrs([],C),[]):- !.
   45
   46betaConvert(sdrs([B1|L1],C1),Result,[]):- !,
   47   betaConvert(B1,B2),
   48   betaConvert(sdrs(L1,C1),sdrs(L2,C2)),
   49   mergeDrs(sdrs([B2|L2],C2),Result).
   50
   51betaConvert(lab(X,B1),lab(X,B2),[]):- !,
   52   betaConvert(B1,B2).
   53
   54betaConvert(sub(B1,B3),sub(B2,B4),[]):- !,
   55   betaConvert(B1,B2),
   56   betaConvert(B3,B4).
   57
   58betaConvert(B1:drs(D1,C1),B1:drs(D2,C3),[]):- 
   59   option('--elimeq',true),
   60   select(_:[]:eq(X1,Y1),C1,C2),
   61   select(B2:[]:Y2,D1,D2), B1==B2, Y1==Y2, !, X1=Y1,
   62   betaConvertConditions(C2,C3).
   63
   64betaConvert(B:drs(D,C1),B:drs(D,C2),[]):- !, 
   65   betaConvertConditions(C1,C2).
   66
   67betaConvert(alfa(T,B1,B2),Result,[]):- !, 
   68   betaConvert(B1,K1), 
   69   betaConvert(B2,K2),
   70   mergeDrs(alfa(T,K1,K2),Result).
   71
   72betaConvert(app(B1,B2),app(K1,K2),[]):- !, 
   73   betaConvert(B1,K1), 
   74   betaConvert(B2,K2).
   75
   76betaConvert(X,Y,L):- !,  
   77   wrapArguments(L,X,Y).
   78
   79
   80/* ========================================================================
   81   Beta-Convert DRS Conditions
   82======================================================================== */
   83
   84betaConvertConditions([],[]).
   85
   86betaConvertConditions([B:I:C1|L1],[B:I:C2|L2]):- !,
   87   betaConvertCond(C1,C2),
   88   betaConvertConditions(L1,L2).
   89
   90
   91/* ========================================================================
   92   Beta-Convert DRS Condition
   93======================================================================== */
   94
   95betaConvertCond(not(A1),not(B1)):- !, betaConvert(A1,B1).
   96betaConvertCond(pos(A1),pos(B1)):- !, betaConvert(A1,B1).
   97betaConvertCond(nec(A1),nec(B1)):- !, betaConvert(A1,B1).
   98betaConvertCond(prop(X,A1),prop(X,B1)):- !, betaConvert(A1,B1).
   99betaConvertCond(or(A1,A2),or(B1,B2)):- !, betaConvert(A1,B1), betaConvert(A2,B2).
  100betaConvertCond(imp(A1,A2),imp(B1,B2)):- !, betaConvert(A1,B1), betaConvert(A2,B2).
  101betaConvertCond(duplex(T,A1,X,A2),duplex(T,B1,X,B2)):- !, betaConvert(A1,B1), betaConvert(A2,B2).
  102betaConvertCond(C,C).
  103
  104
  105/* ========================================================================
  106   Wrapping arguments from stack
  107======================================================================== */
  108
  109wrapArguments([],X,X).
  110
  111wrapArguments([A|L],X,Y):- wrapArguments(L,app(X,A),Y)