
:- use_module(library(terms_vars),[varsbag/3]).
:- use_module(library(terms),[atom_concat/2]).
:- use_module(library(lists), [length/2,append/3,nocontainsx/2]).

:- set_prolog_flag(multi_arity_warnings, off).

compile_constr(Type, Constr) -->
        {
%            display((Type,Constr)), nl,
            copy_term(Constr, Diff),
%            display(1), nl,
            normalize(Diff, K, I, H),			% exec
%            display(2), nl,
            solve_constr(Type, K, I, H),		% exec
%           display(3), nl,
            varsbag(Constr, Vs, []),
%            display(4), nl,
            copy_term([Constr|Vs], [Constr_|Vs_]),
%            display(5), nl,
            dump_internal(Diff, Constr_, Cs)
%            display(6), nl,
%            display(Cs), nl
        },
        ctidy(Cs),
%            {display(7), nl},
        explicit_unifs(Vs_, Vs, []),
%            {display(8), nl},
        !.
compile_constr(_, _) --> 
%        {display('----- FAIL!!!!'), nl} , 
         [fail].

solve_constr(.<>., K, I, H) :- var_with_def(_, nz, K, I, H).
solve_constr(.=. , _, I, H) :- solve_lin(H, I).
solve_constr( .<., _, I, H) :- solve_ineq_lt(H, I).
solve_constr(.=<., _, I, H) :- solve_ineq_le(H, I).

explicit_unifs([], _, _) --> [].
explicit_unifs([V1|L1], [V2|L2], Sofar) -->
        ( {var(V1), nocontainsx(Sofar,V1) } -> % Free independent variable
            { V2 = V1 }
        ; [V2 = V1]
        ),
        explicit_unifs(L1, L2, [V1|Sofar]).


% ----------------------------------------------------------------------

compile_curried( Args, H) -->
  {
    %
    % the limit must correspond with solve_generic_N/K
    %
    build_call( 5, solve_generic, Args, H, Call)
  },
  [ Call ].

% reduce the amount of structure passing
%
build_call( Limit, Name, Args, H, Call) :-
  length(H, Len),
  ( Len =< Limit ->
     flatten_h( H, Hf, []),
     number_codes(Len, Lencs),
     atom_codes(LenAtm, Lencs),
     atom_concat([Name,'_',LenAtm], Fullname),
     append( Args, Hf, A),
     Call =.. [Fullname|A]
  ;
     atom_concat(Name, '_n', Fullname),
     append(Args, [H], A),
     Call =.. [Fullname,Len|A]
  ).

flatten_h( []) --> [].
flatten_h( [V*K|Vs]) --> [V,K], flatten_h( Vs).

% ------------------------------- compiler dumper -----------------------------

% DCG output of nonlinear stuff
%
compile_normalize( Exp, Ic, Hc) -->
  {
    copy_term( Exp, Copy), 		% isolate
    normalize( Copy, I, H),
    dump_internal( Copy-I-H, Exp-Ic-Hc, Cs)
  },
  ctidy( Cs).

% Compiler backend for the dumper
% Here we would only have to dump frozen_system
%
ctidy( []) --> [].
ctidy( [C|Cs]) -->
  ( { C = eqs(_,Dep,Indep) },
      ctidy_deps( Dep),
      ctidy_indeps( Indep)
  ; { C = cva(Var,Constr) },
      ctidy( Constr, Var)
  ),
  ctidy( Cs).

ctidy( float(F), V) -->
  { V = F }.				% exec
%
ctidy( clpr_frozen(Goals), V) -->
  ctidy_nonlin( Goals, V).
%
ctidy( cva(Attrib), V) --> 		% general case
  [ attach_attribute(V,Attrib) ].

ctidy_indeps( [])                      --> [].
ctidy_indeps( [indep(Var,Type,Nl)|Vs]) -->
  ctidy_indep( Type, Var),
  ctidy_nonlin( Nl, Var),
  ctidy_indeps( Vs).

ctidy_deps( [])                        --> [].
ctidy_deps( [dep(Var,Type,I,H,Nl)|Vs]) -->
  ctidy_dep( Type, I, H, Var),
  ctidy_nonlin( Nl, Var),
  ctidy_deps( Vs).

ctidy_nonlin( none,    _)   --> [].
ctidy_nonlin( nl(S,U), Var) -->
  ctidy_frozen_system( S),
  ctidy_frozen_user( U, Var).

ctidy_indep(    v, _) --> [].
ctidy_indep( l(t), V) --> compile_curried( [lt,0], [V*1]).
ctidy_indep( l(e), V) --> compile_curried( [le,0], [V*1]).
ctidy_indep(   nz, V) --> [ nonzero(V) ]. % Check this!

ctidy_dep( v,  I, H, V) -->
  ctidy_eq( H, I, V).
ctidy_dep( nz, I, H, V) -->
  ctidy_neq( H, I, V).
ctidy_dep( l(Type), I, H, _) -->
  ctidy_inequality( Type, H, I).

ctidy_inequality( e, H, I) -->
  compile_curried( [le,I], H).
ctidy_inequality( t, H, I) -->
  compile_curried( [lt,I], H).

ctidy_frozen_system( true)  --> !, [].
ctidy_frozen_system( (A,B)) --> !,
  ctidy_frozen_system( A),
  ctidy_frozen_system( B).
ctidy_frozen_system( Goal) -->
  ( {
      arg( 1, Goal, Mutex),
      var( Mutex),
      Mutex = dumped
    } ->
      ctidy_nonlin( Goal)
  ;
      []
  ).

ctidy_frozen_user( true, _) --> !, [].
ctidy_frozen_user( Goal, V) --> [ clpr_freeze(V,Goal) ].

% For the code below, please see the comment for the predicate 
% tidy_frozen_system_op/4 in file clp_dump.pl

%% Code for CLPQ
ctidy_nonlin('solver_q:solve_abs'(_,A,B,_))       --> [ solve_abs(A,B) ].
ctidy_nonlin('solver_q:solve_mix'(_,Mix,A,B,C,_)) --> [ solve_mix(Mix,A,B,C) ].
ctidy_nonlin('solver_q:solve_mult'(_,A,B,C,_))    --> [ solve_mult(A,B,C) ].
ctidy_nonlin('solver_q:solve_pow'(_,A,B,C,_))     --> [ solve_pow(A,B,C) ].
ctidy_nonlin('solver_q:solve_trig'(_,Trig,A,B,_)) --> [ solve_trig(Trig,A,B) ].

%% Code for CLPR
ctidy_nonlin('solver_r:solve_abs'(_,A,B,_))       --> [ solve_abs(A,B) ].
ctidy_nonlin('solver_r:solve_mix'(_,Mix,A,B,C,_)) --> [ solve_mix(Mix,A,B,C) ].
ctidy_nonlin('solver_r:solve_mult'(_,A,B,C,_))    --> [ solve_mult(A,B,C) ].
ctidy_nonlin('solver_r:solve_pow'(_,A,B,C,_))     --> [ solve_pow(A,B,C) ].
ctidy_nonlin('solver_r:solve_trig'(_,Trig,A,B,_)) --> [ solve_trig(Trig,A,B) ].

ctidy_eq( [X*K], I, V) -->
  {
    arith_zero( I),
    arith_zero( 1-K),
    !,
    X = V
  }.
ctidy_eq( H, I, V) -->
  compile_curried( [eq,I], [V* -1|H]).

%
% this pattern is produced by A=B/C
%
ctidy_neq( [X*K], I, V) -->
  {
    arith_zero( I),
    arith_zero( 1-K),
    !,
    X = V
  },
  [ nonzero(V) ].
ctidy_neq( H, I, V) -->
  compile_curried( [nz(V),I], H).

