location_vars_to_program

get_program_for_output_var(_,M0,M0,_,_,_,_,_,[],[]).

get_program_for_output_var(Library,M0,ProgramLine,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,UsedLVars,[Assignment|T]) :-
    get_variable_value_from_bindings(Bindings, Root, ProBValue),
    ProBValue = int(ProgramLine),
    atom_concat(lo,_,Root) ,
    % get the output location mapped to this line of the program
    get_location_var_node_by_info_term(LocationVarsOut,synthesis(program_line(ProgramLine)),RootNode) ,
    % and get the corresponding machine var using the info term synthesis/2
    get_texpr_info(RootNode,RootInfo) ,
    member(synthesis(machinevar,MachineVar),RootInfo) ,
    member(b(identifier(MachineVar),MachineVarType,MachineVarInfo),CurrentVars) ,
    location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,Root,TempUsedLVars,AST) ,
    prime_identifier(b(identifier(MachineVar),MachineVarType,MachineVarInfo),PrimedVar) ,
    Assignment = b(equal(PrimedVar,AST),pred,[]) ,
    NProgramLine is ProgramLine - 1 ,
    get_program_for_output_var(Library,M0,NProgramLine,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,R,T) ,
    append(TempUsedLVars,R,UsedLVars).

get_variable_value_from_bindings(Bindings, VarName, Value) :-
    member(binding(VarName, Value, _), Bindings).

get_variable_value_from_bindings(Bindings, VarName, Value) :-
    member(bind(VarName, Value), Bindings).

get_varname_for_input_enumeration([],_,_) :- fail.

get_varname_for_input_enumeration([LocationVar|_],Value,VarName) :-
    LocationVar = b(_,_,Info) ,
    member(synthesis(input(Value)),Info) ,
    member(synthesis(machinevar,VarName),Info) , !.

get_varname_for_input_enumeration([_|T],Value,VarName) :-
    get_varname_for_input_enumeration(T,Value,VarName).

location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,LocationVarName,[LocationVarNode|RUsedLVars],IfThenElseAst) :-
    LocationVarNode = b(identifier(LocationVarName),_,Info) ,
    member(LocationVarNode,LocationVarsOut) ,
    subset([synthesis(type,Type),synthesis(Component,output)],Info) ,
    atom_concat(if_then_else,_,Component) , ! ,
    % find the location variable of the statement's condition
    get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,condition),b(identifier(ConditionName),_,_)) ,
    location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,ConditionName,ConditionUsedLVars,ConditionAst) ,
    % find location variables for truth and falsity outputs of the if_then_else statement
    get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,true_out),b(identifier(TrueOutName),_,_)) ,
    location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,TrueOutName,TrueOutUsedLVars,TrueOutAst) ,
    get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,false_out),b(identifier(FalseOutName),_,_)) ,
    location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,FalseOutName,FalseOutUsedLVars,FalseOutAst) ,
    append([ConditionUsedLVars,TrueOutUsedLVars,FalseOutUsedLVars],RUsedLVars) ,
    IfThenElseAst = b(if_then_else(ConditionAst,TrueOutAst,FalseOutAst),Type,[]).

location_to_ast(_,_,_,LocationVarsOut,_,_,LocationVarName,[LocationVarNode],IdNode) :-
    LocationVarNode = b(identifier(LocationVarName),_,Info) ,
    member(LocationVarNode,LocationVarsOut) ,
    (subset([synthesis(_,output),synthesis(machineconstant,IdNode)],Info) ;
    subset([synthesis(_,output),synthesis(operationparameter,IdNode)],Info)) , !.

location_to_ast(_,_,_,LocationVarsOut,_,_,LocationVarName,[LocationVarNode],AST) :-
    LocationVarNode = b(identifier(LocationVarName),_,Info) ,
    member(LocationVarNode,LocationVarsOut) ,
    subset([synthesis(ConstantName,output),synthesis(type,Type)],Info) ,
    atom_concat(constant_set,_,ConstantName) , ! ,
    % export as infinite set
    get_single_constant_or_set_operator_id(Type,_,AST).

location_to_ast(_,_,_,LocationVarsOut,_,_,LocationVarName,[LocationVarNode],Node) :-
    LocationVarNode = b(identifier(LocationVarName),_,Info) ,
    member(LocationVarNode,LocationVarsOut) ,
    member(synthesis(ConstantName,output),Info) ,
    member(synthesis(ParamType,ParamName),Info) ,
    (ParamType = param_single ; ParamType = param_set) ,
    atom_concat(constant,_,ConstantName) , ! ,
    member(synthesis(type,Type),Info) ,
    (Type = set(global(Independent)) ; Type = global(Independent)) ,
    (ParamType = param_set
    -> Node = b(set_extension([b(identifier(ParamName),global(Independent),Info)]),set(global(Independent)),Info)
    ; ParamType = param_single ,
    Node = b(identifier(ParamName),global(Independent),Info)).

location_to_ast(_,_,_,LocationVarsOut,_,Bindings,LocationVarName,[LocationVarNode],Node) :-
    LocationVarNode = b(identifier(LocationVarName),_,Info) ,
    member(LocationVarNode,LocationVarsOut) ,
    member(synthesis(ConstantName,output),Info) ,
    atom_concat(constant,_,ConstantName) , ! ,
    % get constant solution, either integer or boolean
    get_variable_value_from_bindings(Bindings, ConstantName, ProBValue),
    member(synthesis(type,Type),Info) ,
    Node = b(value(ProBValue),Type,Info).

location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,LocationVarName,[LocationVarNode|RUsedLVars],AstNode) :-
    LocationVarNode = b(identifier(LocationVarName),_,InfoOut) ,
    member(LocationVarNode,LocationVarsOut) ,
    subset([synthesis(Component,output),synthesis(type,Type)],InfoOut) ,
    synthesis_util:delete_numbers_from_atom(Component,ComponentName) ,
    member(ComponentName,[negation,card,size,max,min,general_union,general_intersection,reverse,range,domain,skip,convert_bool,first,last]) , ! ,
    % find input location variables
    get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,input),b(identifier(InName),_,_)) ,
    location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,InName,RUsedLVars,InputAST) ,
    Node =.. [ComponentName,InputAST] ,
    single_input_location_to_ast_aux(ComponentName,b(Node,Type,InfoOut),InputAST,AstNode).

location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,LocationVarName,UsedLVars,AST) :-
    LocationVarNode = b(identifier(LocationVarName),_Type,InfoOut) ,
    member(LocationVarNode,LocationVarsOut) , ! ,
    member(synthesis(Component,output),InfoOut) ,
    % find input location variables
    get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,left_input),b(identifier(InName1),_,_)) ,
    get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,right_input),b(identifier(InName2),_,_)) ,
    location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,InName1,
    LeftUsedLVars,LeftInputAST) ,
    location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,InName2,
    RightUsedLVars,RightInputAST) ,
    synthesis_util:delete_numbers_from_atom(Component,ComponentName) ,
    % get the type from the output nodes information
    member(synthesis(type,Type),InfoOut) ,
    Node =.. [ComponentName,LeftInputAST,RightInputAST] ,
    append([[LocationVarNode],LeftUsedLVars,RightUsedLVars],UsedLVars) ,
    set_type(b(Node,Type,InfoOut),AST).

location_to_ast(_,CurrentVars,LocationVarsIn,_,Parameter,Bindings,LocationVarName,[],b(identifier(VarName),Type,Info)) :-
    get_variable_value_from_bindings(Bindings, LocationVarName, ProBValue),
    ProBValue = int(Value),
    Value < Parameter , ! ,
    get_varname_for_input_enumeration(LocationVarsIn,Value,VarName) ,
    member(b(identifier(VarName),Type,Info),CurrentVars).

location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,LocationVarName,UsedLVars,AST) :-
    get_variable_value_from_bindings(Bindings, LocationVarName, ProBValue),
    ProBValue = int(Value),
    Value >= Parameter ,
    % temporary output variable
    LocationOut = b(identifier(LocationOutName),_,_) ,
    % get output defined at corresponding location
    get_variable_value_from_bindings(Bindings, LocationOutName, ProBValue),
    ProBValue = int(Value),
    LocationVarName \= LocationOutName ,
    member(LocationOut,LocationVarsOut) ,
    location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,
    LocationOutName,UsedLVars,AST).

location_vars_to_program(Library,Type,CurrentVars,LocationVars,M1,Parameter,solution(Bindings),UsedLVars,AST) :-
    % split by temporary input and output variables
    findall(Out,(member(Out,LocationVars) , Out = b(identifier(Name),_,_) ,
    atom_concat(lo,_,Name)),LocationVarsOut) ,
    delete(LocationVars,LocationVarsOut,LocationVarsIn) ,
    % get output location variable defined in the last program line
    (location_vars_to_program_aux(Type,M1,Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,UsedLVars,AST)
    -> true ; synthesis_log(location_vars_to_program_and_fail(Type,Library,LocationVarsIn,LocationVarsOut,Parameter,Bindings))) , !.

location_vars_to_program_aux(action,M1,Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,UsedLVars,AST) :-
    length(CurrentVars,OutputAmount) ,
    M0 is M1 - OutputAmount ,
    % Translate the program of each output variable and conjunct them. For constraint solving we need
    % conjunctions which are replaced with parallel executions after finding the final solution.
    get_program_for_output_var(Library,M0,M1,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,TempUsedLVars,ASTList) ,
    remove_dups(TempUsedLVars,UsedLVars) ,
    conjunct_predicates(ASTList,AST).

location_vars_to_program_aux(Type,M1,Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,UsedLVars,AST) :-
    Type \= action ,
    % Output values of the program are also located to the last line (root), but we want to find the output
    % location variable. Here, we just have one output whose location variable is named 'lo0'.
    get_variable_value_from_bindings(Bindings, Root, ProBValue),
    ProBValue = int(M1),
    atom_concat(lo,Suffix,Root) , \+atom_concat(value,_,Suffix) ,
    location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,Root,UsedLVars,AST).

set_type(b(member(b(Elm,EType,EInfo),Set),NodeType,MInfo),b(member(b(Elm,EType,EInfo),NSet),NodeType,MInfo)) :-
    set_type_aux(EType,Set,NSet).

set_type(b(Node,Type,Info),b(NewNode,Type,Info)) :-
    Node =.. [Head,Arg] , Head \= identifier ,
    set_type(Arg,NArg) ,
    NewNode =.. [Head,NArg].

set_type(b(Node,Type,Info),b(NewNode,Type,Info)) :-
    Node =.. [Head,Arg1,Arg2] ,
    set_type(Arg1,NArg1) ,
    set_type(Arg2,NArg2) ,
    NewNode =.. [Head,NArg1,NArg2].

set_type(Node,Node).

set_type_aux(Type,b(set_extension(Set),_,SInfo),b(set_extension(NSet),set(Type),SInfo)) :-
    maplist(set_type_aux(Type),Set,NSet).

set_type_aux(Type,b(Node,_,Info),b(Node,Type,Info)).

single_input_location_to_ast_aux(skip,b(_,_,Info),ComponentAstNode,ComponentAstNodeWithInfo) :-
    add_texpr_infos(ComponentAstNode,Info,ComponentAstNodeWithInfo).

single_input_location_to_ast_aux(Component,AstNode,_,AstNode) :-
    Component \= skip.