Corrected computation of prosodics

Added prod_i3 case to transform_proof

Updated check_proofs to output percentages (rather than ratios)

chart.pl

@@ -1288,15 +1288,18 @@
 	!,
 	select(Index, [A|As], Bs),
 	stored(Index, _, J, K, _, data(ProsD,_,_,_,_,_,_,_)),
+	justification(Index, Just),
+	Just =.. [_|Args],
+	reconstruct_pros(ProsD, Args, Pros1),
   (
         I = J
   ->
-	justification(Index, Just),
-	Just =.. [_|Args],
-	reconstruct_pros(ProsD, Args, Pros)
+        /* the stored item spans the complete string */
+        Pros = Pros1
   ;
-        /* special case for prod_i3 */
-        Pros = p(0,Pros0,ProsD),
+        /* special case for prod_i3; the stored item spans only a postfix */
+        /* we therefore compute the missing prefix from the other premisses */
+        Pros = p(0,Pros0,Pros1),
         reconstruct_pros(I-J, Bs, Pros0)
   ).
 
@@ -1312,7 +1315,8 @@
 	Just2 =.. [_|Args2],
 	reconstruct_pros(ProsL0, Args1, ProsL),
 	reconstruct_pros(ProsR0, Args2, ProsR).
-reconstruct_pros(Pros, _, Pros).
+reconstruct_pros(Pros, _, Pros) :-
+	format(user_error, '~N{Warning: failed to reconstruct prosodics for "~w"}~n', [Pros]).
 
 
 % = coherent_item(+Left, +Right, +Data)
@@ -1681,7 +1685,6 @@
 		    Prob is Prob0 + Prob3]).
 
 % = product rules
-% to test: maybe it is reasonable to require all stacks to be empty.
 
 inference(prod_e, [item(p(0,dr(0,X,Y),dia(0,box(0,Y))), I, J, data(Pros0,Sem0,Prob,H,SetA,SetB,SetC,SetD))],
 	           item(X, I, J, data(Pros,appl(pi1(Sem0),pi2(Sem0)),Prob,H,SetA,SetB,SetC,SetD)),

chart_cr.pl

@@ -1288,15 +1288,18 @@
 	!,
 	select(Index, [A|As], Bs),
 	stored(Index, _, J, K, _, data(ProsD,_,_,_,_,_,_,_)),
+	justification(Index, Just),
+	Just =.. [_|Args],
+	reconstruct_pros(ProsD, Args, Pros1),
   (
         I = J
   ->
-	justification(Index, Just),
-	Just =.. [_|Args],
-	reconstruct_pros(ProsD, Args, Pros)
+        /* the stored item spans the complete string */
+        Pros = Pros1
   ;
-        /* special case for prod_i3 */
-        Pros = p(0,Pros0,ProsD),
+        /* special case for prod_i3; the stored item spans only a postfix */
+        /* we therefore compute the missing prefix from the other premisses */
+        Pros = p(0,Pros0,Pros1),
         reconstruct_pros(I-J, Bs, Pros0)
   ).
 
@@ -1312,7 +1315,8 @@
 	Just2 =.. [_|Args2],
 	reconstruct_pros(ProsL0, Args1, ProsL),
 	reconstruct_pros(ProsR0, Args2, ProsR).
-reconstruct_pros(Pros, _, Pros).
+reconstruct_pros(Pros, _, Pros) :-
+	format(user_error, '~N{Warning: failed to reconstruct prosodics for "~w"}~n', [Pros]).
 
 
 % = coherent_item(+Left, +Right, +Data)
@@ -1681,7 +1685,6 @@
 		    Prob is Prob0 + Prob3]).
 
 % = product rules
-% to test: maybe it is reasonable to require all stacks to be empty.
 
 inference(prod_e, [item(p(0,dr(0,X,Y),dia(0,box(0,Y))), I, J, data(Pros0,Sem0,Prob,H,SetA,SetB,SetC,SetD))],
 	           item(X, I, J, data(Pros,appl(pi1(Sem0),pi2(Sem0)),Prob,H,SetA,SetB,SetC,SetD)),

chart_lp.pl

@@ -1288,15 +1288,18 @@
 	!,
 	select(Index, [A|As], Bs),
 	stored(Index, _, J, K, _, data(ProsD,_,_,_,_,_,_,_)),
+	justification(Index, Just),
+	Just =.. [_|Args],
+	reconstruct_pros(ProsD, Args, Pros1),
   (
         I = J
   ->
-	justification(Index, Just),
-	Just =.. [_|Args],
-	reconstruct_pros(ProsD, Args, Pros)
+        /* the stored item spans the complete string */
+        Pros = Pros1
   ;
-        /* special case for prod_i3 */
-        Pros = p(0,Pros0,ProsD),
+        /* special case for prod_i3; the stored item spans only a postfix */
+        /* we therefore compute the missing prefix from the other premisses */
+        Pros = p(0,Pros0,Pros1),
         reconstruct_pros(I-J, Bs, Pros0)
   ).
 
@@ -1312,7 +1315,8 @@
 	Just2 =.. [_|Args2],
 	reconstruct_pros(ProsL0, Args1, ProsL),
 	reconstruct_pros(ProsR0, Args2, ProsR).
-reconstruct_pros(Pros, _, Pros).
+reconstruct_pros(Pros, _, Pros) :-
+	format(user_error, '~N{Warning: failed to reconstruct prosodics for "~w"}~n', [Pros]).
 
 
 % = coherent_item(+Left, +Right, +Data)
@@ -1681,7 +1685,6 @@
 		    Prob is Prob0 + Prob3]).
 
 % = product rules
-% to test: maybe it is reasonable to require all stacks to be empty.
 
 inference(prod_e, [item(p(0,dr(0,X,Y),dia(0,box(0,Y))), I, J, data(Pros0,Sem0,Prob,H,SetA,SetB,SetC,SetD))],
 	           item(X, I, J, data(Pros,appl(pi1(Sem0),pi2(Sem0)),Prob,H,SetA,SetB,SetC,SetD)),

check_proofs.pl

@@ -60,8 +60,8 @@
 
 all_strange_proofs([], Strange, Total) :-
 	Normal is Total - Strange,
-	NPct is Normal/Total,
-	SPct is Strange/Total,
+	NPct is (Normal/Total)*100,
+	SPct is (Strange/Total)*100,
 	format('~N**TOTAL**~nNormal : ~D (~w%)~nStrange: ~D (~w%)~nTotal  : ~D~2n', [Normal,NPct,Strange,SPct,Total]).
 
 all_strange_proofs([F|Fs], Strange0, Total0) :-
@@ -72,8 +72,8 @@
 	findall(N, proof(N, _), ProofList),
 	strange_proofs(ProofList, 0, ST, 0, TT, Ss, []),
 	Normal is TT - ST,
-	NPct is Normal/TT,
-	SPct is ST/TT,
+	NPct is (Normal/TT)*100,
+	SPct is (ST/TT)*100,
 	Total is Total0 + TT,
 	Strange is Strange0 + ST,
 	format('~N**~w**~nNormal : ~D (~w%)~nStrange: ~D (~w%)~nTotal  : ~D~2n', [F,Normal,NPct,ST,SPct,TT]),
@@ -84,8 +84,8 @@
 	findall(N, proof(N, _), ProofList),
 	strange_proofs(ProofList, 0, ST, 0, TT, Ss, []),
 	Normal is TT - ST,
-	NPct is Normal/TT,
-	SPct is ST/TT,
+	NPct is (Normal/TT)*100,
+	SPct is (ST/TT)*100,
 	format('~NNormal : ~D (~w%)~nStrange: ~D (~w%)~nTotal  : ~D~2n', [Normal,NPct,ST,SPct,TT]),
 	print_list(Ss).
 

grail_light.pl

@@ -1287,15 +1287,18 @@
 	!,
 	select(Index, [A|As], Bs),
 	stored(Index, _, J, K, _, data(ProsD,_,_,_,_,_,_,_)),
+	justification(Index, Just),
+	Just =.. [_|Args],
+	reconstruct_pros(ProsD, Args, Pros1),
   (
         I = J
   ->
-	justification(Index, Just),
-	Just =.. [_|Args],
-	reconstruct_pros(ProsD, Args, Pros)
+        /* the stored item spans the complete string */
+        Pros = Pros1
   ;
-        /* special case for prod_i3 */
-        Pros = p(0,Pros0,ProsD),
+        /* special case for prod_i3; the stored item spans only a postfix */
+        /* we therefore compute the missing prefix from the other premisses */
+        Pros = p(0,Pros0,Pros1),
         reconstruct_pros(I-J, Bs, Pros0)
   ).
 
@@ -1311,7 +1314,8 @@
 	Just2 =.. [_|Args2],
 	reconstruct_pros(ProsL0, Args1, ProsL),
 	reconstruct_pros(ProsR0, Args2, ProsR).
-reconstruct_pros(Pros, _, Pros).
+reconstruct_pros(Pros, _, Pros) :-
+	format(user_error, '~N{Warning: failed to reconstruct prosodics for "~w"}~n', [Pros]).
 
 
 % = coherent_item(+Left, +Right, +Data)
@@ -1680,7 +1684,6 @@
 		    Prob is Prob0 + Prob3]).
 
 % = product rules
-% to test: maybe it is reasonable to require all stacks to be empty.
 
 inference(prod_e, [item(p(0,dr(0,X,Y),dia(0,box(0,Y))), I, J, data(Pros0,Sem0,Prob,H,SetA,SetB,SetC,SetD))],
 	           item(X, I, J, data(Pros,appl(pi1(Sem0),pi2(Sem0)),Prob,H,SetA,SetB,SetC,SetD)),

grail_light_cr.pl

@@ -1287,15 +1287,18 @@
 	!,
 	select(Index, [A|As], Bs),
 	stored(Index, _, J, K, _, data(ProsD,_,_,_,_,_,_,_)),
+	justification(Index, Just),
+	Just =.. [_|Args],
+	reconstruct_pros(ProsD, Args, Pros1),
   (
         I = J
   ->
-	justification(Index, Just),
-	Just =.. [_|Args],
-	reconstruct_pros(ProsD, Args, Pros)
+        /* the stored item spans the complete string */
+        Pros = Pros1
   ;
-        /* special case for prod_i3 */
-        Pros = p(0,Pros0,ProsD),
+        /* special case for prod_i3; the stored item spans only a postfix */
+        /* we therefore compute the missing prefix from the other premisses */
+        Pros = p(0,Pros0,Pros1),
         reconstruct_pros(I-J, Bs, Pros0)
   ).
 
@@ -1311,7 +1314,8 @@
 	Just2 =.. [_|Args2],
 	reconstruct_pros(ProsL0, Args1, ProsL),
 	reconstruct_pros(ProsR0, Args2, ProsR).
-reconstruct_pros(Pros, _, Pros).
+reconstruct_pros(Pros, _, Pros) :-
+	format(user_error, '~N{Warning: failed to reconstruct prosodics for "~w"}~n', [Pros]).
 
 
 % = coherent_item(+Left, +Right, +Data)
@@ -1680,7 +1684,6 @@
 		    Prob is Prob0 + Prob3]).
 
 % = product rules
-% to test: maybe it is reasonable to require all stacks to be empty.
 
 inference(prod_e, [item(p(0,dr(0,X,Y),dia(0,box(0,Y))), I, J, data(Pros0,Sem0,Prob,H,SetA,SetB,SetC,SetD))],
 	           item(X, I, J, data(Pros,appl(pi1(Sem0),pi2(Sem0)),Prob,H,SetA,SetB,SetC,SetD)),

transform_proof.pl

@@ -463,6 +463,19 @@
 	Proof1 = Mid,
 	Proof2 = Right
   ).
+transform_proof(rule(prod_i3, p(0,p(0,Pros1,Pros2),Pros3), p(0,p(0,A,B),C)-Sem, [Left,Mid1,Mid2,Right]), N, N,
+		rule(prod_i, p(0,p(0,Pros1,Pros2),Pros3), p(0,p(0,A,B),C)-Sem,
+		     [rule(prod_i, p(0,Pros1,Pros2), p(0,A,B)-true, [Proof1,Proof2]),
+		      Proof3])) :-
+	/* remove auxiliary hypothesis (of the form C/(A*B) or (A*B)\C) */
+	select(rule(NmA, Pros1, A-SA, PrmsA), [Left,Mid1,Mid2,Right], Rest0),
+	select(rule(NmB, Pros2, B-SB, PrmsB), Rest0, Rest1),
+	member(rule(NmC, Pros3, C-SC, PrmsC), Rest1),
+        !,
+	Proof1 = rule(NmA, Pros1, A-SA, PrmsA),
+	Proof2 = rule(NmB, Pros2, B-SB, PrmsB),
+	Proof3 = rule(NmC, Pros3, C-SC, PrmsC).
+
 transform_proof(rule(prod_e, Pros, FS,
 		     [rule(prod_c, _, _, [Proof1, Proof2])]),
 		N0, N,