% MODULO CHE GESTISCE L'ATTRIBUTO QUANT


%-------------------------------------
% Marco Gavanelli
% 3 October 2003
%-------------------------------------

% This module defines an attribute that tells if a variable
% is quantified existentially or universally.

% It also applies Quantifier Restrictions.

% The possible quantifications are:
% exists (existentially quantified variable whose scope is a single implication)
% existsf (existentially quantified variable whose scope is the whole tuple)
% forall (universally quantified variable whose scope is a single implication)
% forallf (universally quantified variable whose scope is the whole tuple)

% The quantifier restrictions are imposed through the predicate st/1 (such that)
% They can be any predicate: be warned that they will be called if all the
% involved variables are quantified (existsf). Typically, you may want to impose
% quantifier restrictions that have the same syntax as clpfd constraints.

% Suggested use:
% 1. impose the quantification
% 2. impose the quantifier restrictions.
% (should also work the other way around, but probably less efficiently
% or with less complete inferences).

% Example, to impose that X and Y are universally quantified, and we
% have a quantifier restriction X<Y:
% ?- forall(X), forall(Y), st(X#<Y).
% forall(X),
% forall(Y),
% st(X,X#<Y),
% st(Y,X#<Y) ? 
% yes

% If all the variables in a quantifer restriction become quantified existsf
% the quantifier restriction becomes a constraint. E.g.:
% ?- forall(X), st(X#>0), existsf(Y), X=Y.
% Y = X,
% existsf(X),
% X in 1..sup,
% st(X,X#>0) ? 
%
% As you see, the program is not very smart in removing quantifier
% restrictions that have become constraints. This should be only an issue
% of efficiency.

% The program tries to make some (not very smart) check of entailment among
% quantifier restrictions to avoid imposing redundant restrictions. E.g.:
% ?- forall(X), st(X in 1..sup), st(X in 3..10).
% forall(X),
% st(X,X in 1..sup) ? 
% yes
%
% Currently, it considers only constraint "in". E.g.:
% ?- forall(X), st(X #>0), st(X in 3..10).
% forall(X),
% st(X,X#>0),
% st(X,X in 3..10) ? 
% yes
%
% and it is order dependent:
% ?- forall(X), st(X in 3..10), st(X in inf..50).
% forall(X),
% st(X,X in 3..10),
% st(X,X in inf..50) ? 
% yes

:- module(quant,
    [quant/2,
     set_term_quantification/2,
     get_quant/2,
     set_quant/2,
     is_term_quantified/2,
     is_unquantified/1,
     forall/1, forallf/1, exists/1, existsf/1,
     is_universal/1,
     is_existential/1,
     print_quant/0, print_quant/1          %FOR THE DEBUGGER
    ]).

:- use_module(library(chr)).
:- use_module(prolog_version).
%:- use_module(library(atts)).
:- use_module(library(lists)).
:- use_module(library(clpfd)).
:- use_module(library(terms)).
%:- use_module(domains).
%:-use_module(sets).
%:- writeln('CARICO REIFIED_UNIF DA QUANTIF').
:-use_module(reified_unif).
%:- writeln('CARICato REIFIED_UNIF DA QUANTIF').
%:- ensure_loaded(load_solver).
%:- writeln('CARICO solver DA QUANTIF').
:- use_module(solver).
%:- writeln('CARICato solver DA QUANTIF').
:- (is_dialect(swi) -> use_module(swi_specific) ; true).
:- use_module(sciff_options).

:- attribute(quant/1). %%% Needed by SICStus
% can be forall, exists (or free) or 
% forallf (forall flagged), existsf (exists flagged)

% Syntactic Sugar
% Let's skip one passage ....
forall(X):- put_atts(X, quant(forall)). %quant(X,forall).
forallf(X):- put_atts(X, quant(forallf)). %quant(X,forallf).
exists(X):- put_atts(X, quant(exists)). %quant(X,exists).
existsf(X):- put_atts(X, quant(existsf)), %quant(X,existsf),
    get_restrictions(X,Res),
    set_restriction_list(Res,X).


% Ver 1.1: Unification of quantifiers is given by the following rules
% unify_quant(+Q1,+Q2,-Qout)
unify_quant(X,X,X):- !.
unify_quant(forall,Y,Y):- !.
unify_quant(Y,forall,Y):- !.

unify_quant(forallf,Y,Y):- !.
unify_quant(Y,forallf,Y):- !.
unify_quant(existsf,_,existsf):- !.
unify_quant(_,existsf,existsf):- !.

% SICStus unification handler
verify_attributes(Var, Other, Goals) :-
        (get_atts(Var, quant(Da))
          ->    quant_handler(Var,Other,Goals,Da)
          ; Goals=[]).
%        (get_atts(Var, restrictions(Ra))
%          ->    restrictions_handler(Var,Other,GoalsRestr,Ra)
%          ; restrictions_handler(Var,Other,GoalsRestr,[])),
%        append(GoalsQuant,GoalsRestr,Goals).

quant_handler(_Var,Other,Goals,Da):-
        (   var(Other) ->                   % must be attributed then
            (   get_atts(Other, quant(Db)) -> %   has a quantification?
                    unify_quant(Da,Db,Dc),
                    put_atts(Other,quant(Dc)),
                    Goals = []          % NON FA NIENTE!
                ;   Goals = [],
                    put_atts(Other, quant(Da))% rescue intersection
                )
            ;   update_term_quantification(Other,Da),
                Goals = []
            ).

% SWI unification handler
attr_unify_hook(AttValue, Other):-
%quant_handler(_Var,Other,Goals,Da):-
    AttValue = quant(Da),
        (   var(Other) ->                   % must be attributed then
            (   get_atts(Other, quant(Db)) -> %   has a quantification?
                    unify_quant(Da,Db,Dc),
                    put_atts(Other,quant(Dc))
                ;   put_atts(Other, quant(Da))% rescue intersection
            )
            ;   update_term_quantification(Other,Da)
        ).

% This predicate is invoked by SICStus when the computation terminates
% to print the constraint store. We use it to print the quantification
% and the restrictions
attribute_goal(Var, T) :-     % interpretation as goal
    (get_atts(Var, quant(Q)), get_option(print_quant,on)
      ->    T =.. [Q,Var]
      ;     false             % if no attribute, fail (print nothing)
    ).


% Version for SWI
attribute_goals(Var, Out, Rest):-
    (get_atts(Var, quant(Q)), get_option(print_quant,on)
      ->    T =.. [Q,Var], [T|Rest]=Out
      ;     Out=Rest             % if no attribute, print nothing
    ).




%% MG 9 aug 09
%% The goal_expansion version was used in SICStus before adding the compatibility with SWI.
%% It could probably work, but there is probably some problem with modules.
%% we should probably remove module quantif and have only quant.pl and restrictions.pl
% goal_expansion(get_quant(X, Dom),_,_,get_atts(X, quant(Dom)),[]).
%% I restore the previous version, without goal_expansion
get_quant(X, Dom) :-
        get_atts(X, quant(Dom)).
% Reads or sets the quantification for a variable
/*quant(X, Dom) :- slightly slower
        var(Dom),
        var(X),!,
        get_atts(X, quant(Dom)).
quant(X,_Dom):- nonvar(X),!.
quant(X, Value) :-
    put_atts(X, quant(Value)).
*/
% set_quant(X,Dom): same as quant(X,Dom), but assumes that Dom is nonvar.
set_quant(X, Dom) :-
    (var(X)
      ->    put_atts(X, quant(Dom))
      ; true).
quant(X, Dom) :-
    (var(X)
      ->    (var(Dom)
             ->   get_atts(X, quant(Dom))
             ;    put_atts(X, quant(Dom))
            )
      ; true).

% update_term_quantiication(+Term,+Quantification),
% Updates the quantification for all the variables
% in a term. The difference wrt set_term_quantification/2
% is that set_... gives the new quantification
% to all the variables, while update_... uses a priority:
% existsf has higher priority than forallf
% Note that this problem come from not-allowed programs!
update_term_quantification(T,Q) :-
    var(T), !, update_quant(T,Q).
update_term_quantification(T,_) :-
    ground(T), !.
update_term_quantification([H|T],Q) :-!,
    update_term_quantification(H,Q),
    update_term_quantification(T,Q).
update_term_quantification(T,Q) :-
    T =.. [_|Args],
    update_term_quantification(Args,Q).

update_quant(T,Q):-
    (get_quant(T,Qold)
      ->    unify_quant(Q,Qold,Qnew)
      ;     Q=Qnew),
    set_quant(T,Qnew).


% Sets the quantification for all the variables
% in a term
set_term_quantification(T,Q) :-
    var(T), !, set_quant(T,Q).
set_term_quantification([],_):- !.
set_term_quantification(T,_) :-
    atom(T), !.
set_term_quantification([H|T],Q) :-!,
    set_term_quantification(H,Q),
    set_term_quantification(T,Q).
set_term_quantification(T,Q) :-
    T =.. [_|Args],
    set_term_quantification(Args,Q).

% Checks if all the variables in Term are
% quantified Quant
%is_term_quantified(?Term,+Quant)
is_term_quantified(Term,Quant):-
    var(Term),!,
    get_quant(Term,Quant).
is_term_quantified(Term,Quant):-
    functor(Term,_,N),
    is_quantified_arg(N,Term,Quant).

is_quantified_arg(0,_,_):- !.
is_quantified_arg(N,Term,Quant):-
    arg(N,Term,Xn),
    is_term_quantified(Xn,Quant),
    N1 is N-1,
    is_quantified_arg(N1,Term,Quant).

% Checks if all the variables in Term are
% unquantified
%is_unquantified(?Term)
is_unquantified(Term):-
    var(Term),!,
    \+ get_quant(Term,_).
is_unquantified(Term):-
    functor(Term,_,N),
    is_unquantified_arg(N,Term).

is_unquantified_arg(0,_):- !.
is_unquantified_arg(N,Term):-
    arg(N,Term,Xn),
    is_unquantified(Xn),
    N1 is N-1,
    is_unquantified_arg(N1,Term).

/*is_universal(X):- this version is slightly slower
    var(X), 
    (get_quant(X,forall) 
      ->    true 
      ;     get_quant(X,forallf)).*/

is_universal(X):-
    var(X),
    get_quant(X,Q),
    (Q=forall ; Q=forallf),!.

/*is_existential(X):- this version is slightly slower 
    var(X), 
    (get_quant(X,exists) 
      ->    true 
      ;     get_quant(X,existsf)).*/

is_existential(X):-
    var(X),
    get_quant(X,Q),
    (Q=exists ; Q=existsf),!.

%MG: 9 aug 09: Questo non ricordo perche' c'e`.
% Puo` darsi che nella stampa del termine sotto SICStus lui trovi clp_constraint
% e si rifiuti di stamparlo se non e` callable, per cui deve essere definito come
% predicato.
clp_constraint(A):-
    call(A).

% QUESTO NON FUNZIONA, PER CUI L'HO TOLTO.
%% quantif=[113,117,97,110,116,105,102]
%debugger_command_hook(unknown([113,117,97,110,116,105,102],Warning),Actions):-
%    Actions=true,
%    print_goal.
%
%debugger_command_hook(unknown(Line,Warning),Actions):-
%    write(unknown(Line,Warning)), nl, write('ancora'),
%    execution_state([show(Show),goal(_:G)]),
%        execution_state([goal(G)]), nl,
%    write('current goal: '), write(G).
%
%%debugger_command_hook(unknown([0'N|ArgCodes],_), Actions) :-
%%        Actions = true, % don't change the action variables
%%                    % [] would mean [print,ask] :-).
%%    name_current_subterm(ArgCodes).
%
%print_goal:-
%    execution_state(break_level(BL)),
%    write(break(BL)),
%    execution_state(break_level(BL),user:goal(G)),
%    write('current goal: '), write(G).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%55
%
% La seconda e` un po' piu` utile. Volevo estendere il debugger di Sicstus per
% visualizzare anche la quantificazione delle variabili e le quantifier
% restrictions. Non sono riuscito a fare quello che volevo, ma ho ottenuto
% un'approssimazione. Si usa cosi`:
% durante il trace (non il chr_trace!) hai un goal che puo` essere
% 
%          Call: modulo:predicato(A,B,C)
%
% e tu vuoi sapere come sono quantificate A, B e C. Allora fai un "b" (break
% level) e Sicstus ti permette di inserire un goal. Il goal da eseguire e`
% 
%         print_quant(modulo).
%
% o, se il modulo non c'e`, basta print_quant. Ho dovuto usare questa sintassi
% assurda per via del sistema dei moduli, che con i metapredicati diventa una
% pena. Lui dovrebbe stamparti la quantificazione di tutte le variabili che
% compaiono nel goal. A questo punto esci dal break level (^D in linux o ^Z in
% windows) e continui dov'eri.

print_quant:-
    print_quant(user).

print_quant(M):-
    execution_state(break_level(BL)),
    BL1 is BL-1,
    execution_state(break_level(BL1),M:goal(G)),
    print_quantified(G).

print_quantified(G):-
    var(G), get_quant(G,Q),!, write(Q), write('('), write(G), write(')'),
    restrictions:get_restrictions(G,R), write(R), nl.
print_quantified(G):-
    var(G),!, write('unquantified('), write(G), write(')\n').
print_quantified(G):-
    ground(G),!.
print_quantified(G):-
    functor(G,suspension,_),!.
print_quantified(G):-
    G =.. [_,X|Par],
    print_quantified(X),
    print_quantified(Par).
