% == No, Emacs this is -*-Prolog-*- code, not what you thought... =============

% == NAMES ====================================================================

% -- sa_names(AST_IN, AST_OUT, ST) --------------------------------------------
%
% sa_names/3: do name analysis (replace identifiers by their dict. entry)

sa_names(fzn(preds(IP), vars(IV), constrs(IC), SOLVE),
	 fzn(preds(OP), vars(OV), constrs(OC), SOLVE), ST) :-
    sa_n_traverse(IP, OP, ST),  % predicates
    sa_n_traverse(IV, OV, ST),	% variables
    sa_n_traverse(IC, OC, ST).  % constraints

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

sa_n_traverse([], [], _ST) :- !.
sa_n_traverse([N|Ns], [NN|NNs], ST) :-
    sa_n(N, NN, ST), !,
    sa_n_traverse(Ns, NNs, ST).
sa_n_traverse([_|Ns], NNs, ST) :- !, % ignore failing nodes (beware!)
    sa_n_traverse(Ns, NNs, ST).

sa_n_traverse(N, NN, ST) :- sa_n(N, NN, ST). % non-list case


% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
%
% sa_n(AST_N_IN, AST_N_OUT, ST)
%
% arguments:
%  AST_N_IN         - input AST node
%  AST_N_OUT        - output AST node (same structure, rewritten)
%  ST               - symbol table (gets extended)
%
% handle all AST cases:
%  var(N,T,I,A)     - Name, Type, Initializer, Attrib -- variable declaration
%  lit(V,T)         - Value, Type -- literal with type
%  id(N)            - Name -- identifier
%  constraint(C,A)  - Constraint, Attrib -- constraint
%
% variables with an initializer are treated as SSA & will now stand for
% the literal in the initializer itself.

sa_n(var(N,T,[],A), V, ST) :- !,
    sa_attribs(A, AX, ST),
    V=var(N,T,[],AX),		% new AST node becomes ST entry value
    st_insert(ST, N, V).

sa_n(var(N,T,I,A), NI, ST) :-	% non-empty initializer
    sa_attribs(A, AX, ST),	% should ignore this?
    sa_n_traverse(I, NI, ST),	% parse initializer
    V=var(N,T,NI,AX),		% new AST node becomes ST entry value
    st_insert(ST, N, V).


sa_n(lit(E,array(T)), lit(NE, array(T)), ST) :-
    sa_n_traverse(E, NE, ST).
sa_n(lit(E,int), lit(E,int), _ST).
sa_n(lit(E,float), lit(E,float), _ST).
sa_n(lit(E,string), lit(E,string), _ST).


sa_n(id(N), V, ST) :- st_lookup(ST, N, V), !.
sa_n(id(N), V, ST) :- V=var(N,_,_,_), % type as yet unknown
		      st_insert(ST, N, V).


sa_n(constraint(CE, AT), constraint(NCE, AT), ST) :-
    CE=..[C|AS],
    sa_n_traverse(AS, NAS, ST),
    NCE=..[C|NAS].

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

% == TYPES ====================================================================

% -- sa_types(AST, ST) --------------------------------------------------------
%
% sa_types/2: do type analysis (traverse AST enforcing type correctness).
% as a side-effect, it will do type inference.

sa_types(fzn(_PS, vars(VS), constrs(CS), _S), ST) :-
    sa_t_traverse(VS, ST),
    sa_t_traverse(CS, ST).

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

sa_t_traverse([], _ST) :- !.
sa_t_traverse([N|Ns], ST) :-
    sa_t(N, ST), !,
    sa_t_traverse(Ns, ST).
sa_t_traverse([_|Ns], ST) :- !, % ignore failing nodes (beware!)
    sa_t_traverse(Ns, ST).

sa_t_traverse(N, ST) :- sa_t(N, ST). % non-list case

% -- sa_t(NODE, ST) -----------------------------------------------------------

sa_t(var(_N,T,I,_A), _ST) :- type(I,T).
sa_t(lit(E,T), _ST) :- type(lit(E,T), T).
sa_t(constraint(CE, _AT), ST) :-
    CE=..[_|AS],
    sa_t_traverse(AS, ST).

% =============================================================================

sa_attribs([A|As], [NA|NAs], ST) :-
    sa_attrib(A, NA, ST), !,
    sa_attribs(As, NAs, ST).
sa_attribs([_|As], NAs, ST) :-	% ignore unknown attributes
    sa_attribs(As, NAs, ST).
sa_attribs([], [], _).


sa_attrib(id(output_var), output, _).

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