/*  Copyright (C) Wolfgang Menzel, Universität Hamburg, 2003-06-27

    This program is free software; you can redistribute it and/or
    modify it under the terms of the GNU General Public License
    as published by the Free Software Foundation; either version 2
    of the License, or (at your option) any later version.
*/

% a diagnostic engine based on constraint satisfaction
% for utterances with a fixed structure

% includes an error transformation from constraint violations
% to factual faults

:- [engl1].

:- nl.
:- write_ln('a simple constraint checker for fixed phrases with 
error transformation').
:- write_ln('call: ?- diagnose([these,man,are,happy],D)').
:- nl.

%%% structure identification %%%%%%%%%%%

% assign(+Words,+Variables,-Errorlist).
% call: assign([the,man,is,cool],[det,noun,verb,adv],Errors).
% tries to assign each word to a variable

assign([ ],[ ],[ ]).
   % all word in the input processed

assign([Word|Words],[Var|Vars],Err) :-
  category(Word,Cat),               % get the category of the next word
  true ==> cat(Var,Cat),            % check the category constraint
  features(Word,Feats),             % get the features of the next word
  clean_var(Var),                   % housekeeping in the database
  assert(vword(Var,Word)),          %
  assert(vcat(Var,Cat)),            % initializing the variable
  assert(vfeat(Var,Feats)),         %
  assign(Words,Vars,Err).           % recursive descent

assign([Word|Words],[Var|Vars],[cat(Word,Cat,Cats)|Err]) :-
  category(Word,Cat),               % get the category of the next word
  \+ true ==> cat(Var,Cat),         % check the category constraint
  findall(C,true ==> cat(Var,C),Cats),    % collect possible categories
  assign(Words,Vars,Err).           % recursive descend

% clean_var(Variable)
% resets a variable (to be used for housekeeping)

clean_var(Var) :-
  retractall(vword(Var,_)),
  retractall(vcat(Var,_)),
  retractall(vpos(Var,_)),
  retractall(vfeat(Var,_)).

% used(Variable)
% checks whether a variable received an assignment

used(Var) :-
  vword(Var,_).

%%% the diagnosis proper %%%%%%%%%%%%%%%%%%%%%%

% diagnose(+Input,-Diagnoses)
% takes a List of input word forms and returns several lists
% with diagnostic results

diagnose(WordList,Errors) :-
  vars(Vars),
  forall(member(Var,Vars),clean_var(Var)),  % reset all variables
  assign(WordList,Vars,AssignErrors),       % call the variable assignment
  check_constraints(ConstErrors),
  (ConstraintErrors=ConstErrors ;
     % error descriptions from the constraint check
     % are both, passed on directly
    transform_errors(ConstErrors,ConstraintErrors),
    ConstErrors\=ConstraintErrors),
     % and transformed to factual descriptions
    append(AssignErrors,ConstraintErrors,Errors).

% check_constraints(-ErrorDescription)
% applies all but cat-constraints
% returns a list of error descriptions

check_constraints(Err) :-
  findall(Conclusio,
      (Premise ==> Conclusio,
       \+ check_constraint(Premise,Conclusio)),
      Err).

% check_constraint(Premise,Conclusio)
% applies a single constraint as long as it is not
% a cat-constraint

check_constraint(_,cat(_,_)) :- !, true.
check_constraint(Prem,Concl) :-
  Prem -> Concl.


%%% the semantics of constraints %%%%%%%%%%%%%%

% lp(Variable1,Variable2)
% checks the linear precedence between two variables

lp(Var1,Var2) :-
  ((vpos(Var1,Pos1),
    vpos(Var2,Pos2)) ->
     Pos1 < Pos2 ; true).


% agreement(Variable1,Variable2,Feature)
% checks the agreement between two Variables with respect to
% a particular feature

agree(Var1,Var2,Feature) :-
   featurepos(Feature,Pos),
   ((vfeat(Var1,Feats1),
     vfeat(Var2,Feats2) ->
      nth1(Pos,Feats1,Feat),
      nth1(Pos,Feats2,Feat)) ; true ).

%%% the sketch of an error transformation module
%%% constraint violations --> factual error descriptions

% transform_errors(OldErrorList,NewErrorList)
% rule-error to factual-error transformation

transform_errors(Old,New) :-
  trans_errors(Old,Old,Int),
    % replace rule errors by factual errors
%  Old\=Int,
    % only if something changed ... ??? still necessary ?
  simplify(Int,New).
    % ... simplification rules are applied


% trans_errors(RemainingOldList,CompleteList,NewList)
% recursively descents over the old list but keeps the
% complete old list for checks to the left

trans_errors([ ],_,[ ]).

trans_errors([lp(X,Y)|Errors],Old,[lp(X,Y)|ErrorsNew]) :-
    % precedence errors are passed on unchanged
  trans_errors(Errors,Old,ErrorsNew).

trans_errors([agree(X,Y,F)|Errors],Old,
   [value(X,F,XV,YV),not(value(Y,F,YV,XV))|ErrorsNew]) :-
% an agreement error is transformed into a value error, provided
%   - there is no other agreement constraint to another used variable or
%   - the variable is involved in another constraint violation
% All checks have to be performed fully symmetrically!!!
% To prevent mutual neutralizing combinations of error hypotheses
% blocking predicates are inserted (not(...))
% They are removed in simplify later on.
  (\+ (_ ==> agree(X,Z1,F), Z1\=Y, used(Z1)) ,
     \+ (_ ==> agree(Z2,X,F), Z2\=Y, used(Z2)) ;
    _ ==> agree(X,Z,F), Z\=Y, used(Z), member(agree(X,Z,F),Old) ;
    _ ==> agree(Z,X,F), Z\=Y, used(Z), member(agree(Z,X,F),Old)) ,
     % checking all the above mentioned criteria
  vfeat(X,XFs),
  vfeat(Y,YFs),
  featurepos(F,P),
  nth1(P,XFs,XV),
  nth1(P,YFs,YV),
  trans_errors(Errors,Old,ErrorsNew).

trans_errors([agree(X,Y,F)|Errors],Old,
     % symmetrical clause
   [value(Y,F,YV,XV),not(value(X,F,XV,YV))|ErrorsNew]) :-
  (\+ (_ ==> agree(Y,Z1,F), Z1\=X, used(Z1)),
     \+ (_ ==> agree(Z2,Y,F), Z2\=X, used(Z2)) ;
    _ ==> agree(Y,Z,F), Z\=X, used(Z), member(agree(Y,Z,F),Old) ;
    _ ==> agree(Z,Y,F), Z\=X, used(Z), member(agree(Z,Y,F),Old)) ,
  vfeat(X,XFs),
  vfeat(Y,YFs),
  featurepos(F,P),
  nth1(P,XFs,XV),
  nth1(P,YFs,YV),
  trans_errors(Errors,Old,ErrorsNew).


% simplify(OldList,NewList)
% applies certain simplification rules


simplify([],[]).

simplify([Error|Errors],ErrorsNew) :-
      % double error descriptions: one can be removed
   Error \= not(_),
   member(Error,Errors),
   simplify(Errors,ErrorsNew).

simplify([Error|Errors],ErrorsNew) :-
      % double blocking marker: both must be removed
   Error = not(_),
   member(Error,Errors),
   remove(Error,Errors,ErrorsR),
   simplify(ErrorsR,ErrorsNew).

simplify([Error|Errors],[Error|ErrorsNew]) :-
      % an error description is kept, if it is not blocked
      % and no duplicate
   Error \= not(_),
   \+ member(Error,Errors),
   \+ member(not(Error),Errors),
   simplify(Errors,ErrorsNew).

% - kann wegfallen, wenn kein + und nicht doppelt
simplify([Error|Errors],ErrorsNew) :-
      % a blocker can be removed if their is no corresponding
      % error hypothesis and it is not a duplicate
   Error = not(Enot),
   \+ member(Error,Errors),
   \+ member(Enot,Errors),
   simplify(Errors,ErrorsNew).


% remove(Item,ListOld,ListNew)
% removes an Item from a List and returns the reduced list

remove(_,[],[]).

remove(Item,[Item|Rest],NewList) :-
   remove(Item,Rest,NewList).

remove(Item,[X|Xs],[X|Newlist]) :-
   Item\=X,
   remove(Item,Xs,Newlist).