Commit 9bb47132 authored by Finn Teegen's avatar Finn Teegen

Fix unification operators in combination with Data contexts

parent bc9208bd
Subproject commit a2ff153129fb732e3af398388a9227279e997335
Subproject commit 0ed232ccc6909332e3e56be1b3cb34c22a629d99
Subproject commit 6f8a79e6f67a62e06a28daac96d6abb570b8228a
Subproject commit ee3fdd0ca253f3a48fe45e00a947caf997e54766
......@@ -1739,10 +1739,10 @@ transConstrEq(Suffix) :-
ConstrEqHnf_HA_HB_R_E2_E =.. [ConstrEqHnfOrg,HA,HB,R,E2,E],
(compileWithDebug ->
writeClause((ConstrEq_A_B_R_E0_E :-
traceCall('Prelude.=:='(A,B),Skip),
traceCall('Prelude.constrEq'(A,B),Skip),
hnf(A,HA,E0,E1), hnf(B,HB,E1,E2),
ConstrEqHnf_HA_HB_R_E2_E,
traceExit('Prelude.=:='(A,B),
traceExit('Prelude.constrEq'(A,B),
'Prelude.True',
E,Skip)))
; writeClause((ConstrEq_A_B_R_E0_E :- hnf(A,HA,E0,E1),hnf(B,HB,E1,E2),
......@@ -1767,7 +1767,7 @@ transConstrEq(Suffix) :-
writeClause((ConstrEqHnf_X_FAIL_E_E :- !)),
writeClause((ConstrEqHnf_A_B_R_E0_E :- number(A), !,
(A=B -> R='Prelude.True', E0=E
; prim_failure(partcall(2,'Prelude.=:=',[]),[A,B],R,E0,E))))),
; prim_failure(partcall(2,'Prelude.constrEq',[]),[A,B],R,E0,E))))),
appendAtom(genConstrEqHnfBody,Suffix,GenConstrEqHnfBody),
GenConstrEqHnfBody_1_NA =.. [GenConstrEqHnfBody,1,NA,A,B,EqBody],
writeClause((ConstrEqHnf_A_B_R_E0_E :-
......@@ -1777,12 +1777,12 @@ transConstrEq(Suffix) :-
(printConsFailure(no) -> true
; ConstrEqHnf_A_B_FAIL_E0_E =.. [ConstrEqHnf,A,B,R,E0,E],
writeClause((ConstrEqHnf_A_B_FAIL_E0_E :-
prim_failure(partcall(2,'Prelude.=:=',[]),[A,B],R,E0,E)))),
prim_failure(partcall(2,'Prelude.constrEq',[]),[A,B],R,E0,E)))),
nl,
GenConstrEqHnfBody_N_NA_Succ =..
[GenConstrEqHnfBody,N,NA,_,_,'Prelude.True'],
writeClause((GenConstrEqHnfBody_N_NA_Succ :- N>NA,!)),
appendAtom('Prelude.=:=',Suffix,Eq),
appendAtom('Prelude.constrEq',Suffix,Eq),
Eq_ArgA_ArgB =.. [Eq,ArgA,ArgB],
GenConstrEqHnfBody_N_NA_Eq =.. [GenConstrEqHnfBody,N,NA,A,B,Eq_ArgA_ArgB],
writeClause((GenConstrEqHnfBody_N_NA_Eq :- N=NA, !,
......@@ -1820,7 +1820,7 @@ transConstrEq(Suffix) :-
writeClause((BindDirect_X_T_R_E0_E :-
OccursNot_X_T, !, X=T, R='Prelude.True', E0=E)),
writeClause((BindDirect_X_T_R_E0_E :-
prim_failure(partcall(2,'Prelude.=:=',[]),[X,T],R,E0,E)))),
prim_failure(partcall(2,'Prelude.constrEq',[]),[X,T],R,E0,E)))),
nl,
Bind_X_T_E0_E =.. [Bind,X,T,'Prelude.True',E0,E],
writeClause((Bind_X_T_E0_E :- var(T), !, X=T, E0=E)),
......@@ -1841,7 +1841,7 @@ transConstrEq(Suffix) :-
functor(B,FB,NB), OccursNotArgs_1_NB_A_B, !,
functor(A,FB,NB), BindArgs_1_NB_A_B_R_E0_E)),
writeClause((Bind_A_B_R_E0_E :-
prim_failure(partcall(2,'Prelude.=:=',[]),[A,B],R,E0,E)))),
prim_failure(partcall(2,'Prelude.constrEq',[]),[A,B],R,E0,E)))),
nl,
OccursNotArgs_N_NA_A_B =.. [OccursNotArgs,N,NA,A,B],
OccursNotArgs_N1_NA_A_B =.. [OccursNotArgs,N1,NA,A,B],
......@@ -1887,9 +1887,9 @@ transConstrEq_hnf(Cons/Arity) :-
; gen_constrEq_hnf_body(Xs,Ys,Body),
writeClause((constrEq_hnf(CX,CY,E0,E) :- !, hnf(Body,_,E0,E)))).
gen_constrEq_hnf_body([X],[Y],'Prelude.=:='(X,Y)).
gen_constrEq_hnf_body([X],[Y],'Prelude.constrEq'(X,Y)).
gen_constrEq_hnf_body([X1,X2|Xs],[Y1,Y2|Ys],
'Prelude.&'('Prelude.=:='(X1,Y1),Body)) :-
'Prelude.&'('Prelude.constrEq'(X1,Y1),Body)) :-
gen_constrEq_hnf_body([X2|Xs],[Y2|Ys],Body).
......
......@@ -759,8 +759,6 @@ allUnboundVariables(Vs) :-
% (first argument must be the functional pattern):
:- block unifEq(?,?,?,-,?).
unifEq(A,B,R,E0,E):- user:hnf(A,HA,E0,E1), unifEq1(HA,B,R,E1,E).
% unifEq will have a useless dict argument first, so we remove that one
unifEq(_,A,B,R,E0,E):- unifEq(A,B,R,E0,E).
:- block unifEq1(?,?,?,-,?).
% In the following clause, we bind a functional pattern variable to the
......@@ -812,7 +810,7 @@ getControlVar(X,Below,[control(Y,YBelow,NewVar,NewConstraint)|_],NewX) :- X==Y,
% that is later executed.
((Below=inConstructorCall, YBelow=inConstructorCall)
-> (var(NewConstraint)
-> NewConstraint = 'Prelude.=:='(X,NewVar), NewX=X
-> NewConstraint = 'Prelude.constrEq'(X,NewVar), NewX=X
; NewX=NewVar)
; % multiple occurrence of a variable X, where one occurrence is in a
% function call, are replaced by an expression that
......@@ -825,11 +823,11 @@ getControlVar(X,Below,[control(Y,YBelow,NewVar,NewConstraint)|_],NewX) :- X==Y,
NewX=NewVar,
(var(NewConstraint)
-> NewVar = 'Prelude.&>'('Prelude.ifVar'(ShareVar,
'Prelude.=:='(ShareVar,'Prelude.()'),
'Prelude.=:='(CtrlVar,'Prelude.()')),X),
'Prelude.constrEq'(ShareVar,'Prelude.()'),
'Prelude.constrEq'(CtrlVar,'Prelude.()')),X),
NewConstraint = 'Prelude.ifVar'(CtrlVar,
'Prelude.True',
'Prelude.=:='(X,X))
'Prelude.constrEq'(X,X))
; true)).
getControlVar(X,Below,[_|L],NewVar) :- getControlVar(X,Below,L,NewVar).
......@@ -849,8 +847,8 @@ replaceMultipleVariablesInArgs([X|Args],Below,Vars,[NewArg|LinArgs]) :-
replaceMultipleVariablesInArgs([Arg|Args],Below,Vars,[Arg|LinArgs]) :-
% avoid repeating replacing already replaced variables
Arg = 'Prelude.&>'('Prelude.ifVar'(ShareVar,
'Prelude.=:='(ShareVar,'Prelude.()'),
'Prelude.=:='(_CtrlVar,'Prelude.()')),_),
'Prelude.constrEq'(ShareVar,'Prelude.()'),
'Prelude.constrEq'(_CtrlVar,'Prelude.()')),_),
!,
replaceMultipleVariablesInArgs(Args,Below,Vars,LinArgs).
replaceMultipleVariablesInArgs([Arg|Args],Below,Vars,[LinArg|LinArgs]) :-
......@@ -867,18 +865,18 @@ unifEqHnf(_,'FAIL'(Src),'FAIL'(Src),E,E) :- !.
unifEqHnf(A,B,R,E0,E) :-
number(A), !,
(A=B -> R='Prelude.True', E0=E
; prim_failure(partcall(2,'Prelude.=:<=',[]),[A,B],R,E0,E)).
; prim_failure(partcall(2,'Prelude.unifEq',[]),[A,B],R,E0,E)).
unifEqHnf(A,B,R,E0,E) :-
functor(A,FuncA,ArA), functor(B,FuncB,ArB), FuncA==FuncB, ArA==ArB, !,
genUnifEqHnfBody(1,ArA,A,B,Con), user:hnf(Con,R,E0,E).
unifEqHnf(A,B,R,E0,E) :-
prim_failure(partcall(2,'Prelude.=:<=',[]),[A,B],R,E0,E).
prim_failure(partcall(2,'Prelude.unifEq',[]),[A,B],R,E0,E).
genUnifEqHnfBody(N,Arity,_,_,'Prelude.True') :- N>Arity, !.
genUnifEqHnfBody(N,Arity,A,B,'Prelude.=:<='(ArgA,ArgB)):-
genUnifEqHnfBody(N,Arity,A,B,'Prelude.unifEq'(ArgA,ArgB)):-
N=Arity, !,
arg(N,A,ArgA), arg(N,B,ArgB).
genUnifEqHnfBody(N,Arity,A,B,'Prelude.&'('Prelude.=:<='(ArgA,ArgB),G)):-
genUnifEqHnfBody(N,Arity,A,B,'Prelude.&'('Prelude.unifEq'(ArgA,ArgB),G)):-
arg(N,A,ArgA), arg(N,B,ArgB),
N1 is N+1,
genUnifEqHnfBody(N1,Arity,A,B,G).
......@@ -890,8 +888,6 @@ genUnifEqHnfBody(N,Arity,A,B,'Prelude.&'('Prelude.=:<='(ArgA,ArgB),G)):-
:- block unifEqLinear(?,?,?,-,?).
unifEqLinear(A,B,R,E0,E):-
user:hnf(A,HA,E0,E1), unifEqLinear1(HA,B,R,E1,E).
% unifEqLinear will have a useless dict argument first, so we remove that one
unifEqLinear(_,A,HA,E0,E1):- unifEqLinear(A,HA,E0,E1).
:- block unifEqLinear1(?,?,?,-,?).
% In the following clause, we bind a function pattern variable to the
......@@ -921,18 +917,18 @@ unifEqLinearHnf(_,'FAIL'(Src),'FAIL'(Src),E,E) :- !.
unifEqLinearHnf(A,B,R,E0,E) :-
number(A), !,
(A=B -> R='Prelude.True', E0=E
; prim_failure(partcall(2,'Prelude.=:<<=',[]),[A,B],R,E0,E)).
; prim_failure(partcall(2,'Prelude.unifEqLinear',[]),[A,B],R,E0,E)).
unifEqLinearHnf(A,B,R,E0,E) :-
functor(A,FuncA,ArA), functor(B,FuncB,ArB), FuncA==FuncB, ArA==ArB, !,
genUnifEqLinearHnfBody(1,ArA,A,B,Con), user:hnf(Con,R,E0,E).
unifEqLinearHnf(A,B,R,E0,E) :-
prim_failure(partcall(2,'Prelude.=:<<=',[]),[A,B],R,E0,E).
prim_failure(partcall(2,'Prelude.unifEqLinear',[]),[A,B],R,E0,E).
genUnifEqLinearHnfBody(N,Arity,_,_,'Prelude.True') :- N>Arity, !.
genUnifEqLinearHnfBody(N,Arity,A,B,'Prelude.=:<<='(ArgA,ArgB)):-
genUnifEqLinearHnfBody(N,Arity,A,B,'Prelude.unifEqLinear'(ArgA,ArgB)):-
N=Arity, !,
arg(N,A,ArgA), arg(N,B,ArgB).
genUnifEqLinearHnfBody(N,Arity,A,B,'Prelude.&'('Prelude.=:<<='(ArgA,ArgB),G)):-
genUnifEqLinearHnfBody(N,Arity,A,B,'Prelude.&'('Prelude.unifEqLinear'(ArgA,ArgB),G)):-
arg(N,A,ArgA), arg(N,B,ArgB),
N1 is N+1,
genUnifEqLinearHnfBody(N1,Arity,A,B,G).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment