probvm_compiler

add_enumerated_identifier([],[],Env,Env) --> !.

add_enumerated_identifier([TId|Irest],[Value|Vrest],In,Out) -->
    {get_texpr_id(TId,Id), get_texpr_type(TId,Type),
    add_pre_identifier(Id,Value,In,Inter)},
    emit(enumerate(Type,Id,Value)),
    add_enumerated_identifier(Irest,Vrest,Inter,Out).

add_pre_identifier(Id,Value,cmp(Pre,Post),cmp([Id=Value|Pre],Post)).

add_values_to_set([],OrigSet,OrigSet) --> [].

add_values_to_set([Value|Rest],OrigSet,NewSet) -->
    emit(add_element(Value,OrigSet,InterSet)),
    add_values_to_set(Rest,InterSet,NewSet).

compile_check(TExpr,Env,CheckVar) -->
    {get_texpr_expr(TExpr,Expr)},
    compile_check2(Expr,Env,CheckVar).

compile_check2(truth,_Env,V) --> emit(V=pred_true),!.

compile_check2(falsity,_Env,V) --> emit(V=pred_false),!.

compile_check2(negation(E),Env,CheckVar) --> !,
    emit(check_negate(NVar,CheckVar)),
    compile_check(E,Env,NVar).

compile_check2(conjunct(LHS,RHS),Env,CheckVar) --> !,
    compile_check(LHS,Env,LVar),
    compile_check(RHS,Env,RVar),
    emit(check_conjunct(LVar,RVar,CheckVar)).

compile_check2(disjunct(LHS,RHS),Env,CheckVar) --> !,
    {b_interpreter_check:get_priority_of_boolean_expression2(disjunct(LHS,RHS),Prio)},
    compile_check(LHS,Env,LVar),
    compile_check(RHS,Env,RVar),
    emit(check_disjunct(Prio,LVar,RVar,CheckVar)).

compile_check2(equivalence(LHS,RHS),Env,CheckVar) --> !,
    compile_check(LHS,Env,LVar),
    compile_check(RHS,Env,RVar),
    emit(check_equiv(LVar,RVar,CheckVar)).

compile_check2(implication(LHS,RHS),Env,CheckVar) --> !,
    compile_check(LHS,Env,LVar),
    compile_check(RHS,Env,RVar),
    emit(check_impl(LVar,RVar,CheckVar)).

compile_check2(not_equal(LHS,RHS),Env,CheckVar) --> !,
    emit(check_negate(NVar,CheckVar)),
    compile_check2(equal(LHS,RHS),Env,NVar).

compile_check2(equal(LHS,RHS),Env,CheckVar) --> !,
    compile_expression(LHS,Env,LValue),
    compile_expression(RHS,Env,RValue),
    emit(check_equal(LValue,RValue,CheckVar)).

compile_check2(less(LHS,RHS),Env,CheckVar) --> !,
    compile_expression(LHS,Env,LValue),
    compile_expression(RHS,Env,RValue),
    emit(check_less(LValue,RValue,CheckVar)).

compile_check2(greater(LHS,RHS),Env,CheckVar) --> !,
    compile_expression(LHS,Env,LValue),
    compile_expression(RHS,Env,RValue),
    emit(check_less(RValue,LValue,CheckVar)).

compile_check2(member(Elem,Set),Env,CheckVar) -->
    { get_texpr_expr(Set,integer_set(INTSET)),
    integer_bounds(INTSET,Lower,Upper),!},
    compile_expression(Elem,Env,ElemValue),
    ( {Lower==none, Upper==none} ->
    pass
    ; {Lower==none} ->
    emit(check_less_equal(ElemValue,int(Upper),CheckVar))
    ; {Upper == none} ->
    emit(check_less_equal(int(Lower),ElemValue,CheckVar))
    ; {otherwise} ->
    emit(check_less_equal(ElemValue,int(Upper),CheckVar1)),
    emit(check_less_equal(int(Lower),ElemValue,CheckVar2)),
    emit(check_conjunct(CheckVar1,CheckVar2,CheckVar))).

compile_check2(member(Elem,Set),Env,CheckVar) -->
    compile_expression(Elem,Env,ElemValue),
    compile_expression(Set,Env,SetValue),
    emit(check_membership(ElemValue,SetValue,CheckVar)).

compile_expression(TExpr,Env,Value) -->
    {get_texpr_expr(TExpr,Expr)},
    compile_expression2(Expr,Env,Value).

compile_expression2(value(Val),_,Val) --> !.

compile_expression2(boolean_true,_,bool_true) --> !.

compile_expression2(boolean_false,_,bool_false) --> !.

compile_expression2(integer_set(SET),_,global_set(SET)) --> !.

compile_expression2(bool_set,_,[bool_true,bool_false]) --> !.

compile_expression2(empty_set,_,E) --> !, {empty_set(E)}.

compile_expression2(integer(Val),_,int(Val)) --> !.

compile_expression2(identifier(Id),Env,Value) --> !,
    { lookup_pre_identifier(Id,Env,V) ->
    Value=V
    ; lookup_global_constant(Id,V) ->
    Value=V
    ; b_global_set(Id) ->
    Value=global_set(Id)
}.

compile_expression2(add(L,R),Env,Value) --> !,
    compile_expression(L,Env,LValue),
    compile_expression(R,Env,RValue),
    emit(add(LValue,RValue,Value)).

compile_expression2(minus(L,R),Env,Value) --> !,
    compile_expression(L,Env,LValue),
    compile_expression(R,Env,RValue),
    emit(sub(LValue,RValue,Value)).

compile_expression2(function(Function,Arg),Env,Value) --> !,
    compile_expression(Function,Env,FValue),
    compile_expression(Arg,Env,AValue),
    emit(apply(FValue,AValue,Value)).

compile_expression2(set_subtraction(L,R),Env,Value) --> !,
    compile_expression(L,Env,LValue),
    compile_expression(R,Env,RValue),
    emit(set_minus(LValue,RValue,Value)).

compile_expression2(set_extension(List),Env,Value) --> !,
    compile_expression_l(List,Env,Values),
    ( {ground(Values)} ->
    {custom_explicit_sets:construct_avl(Values,Value)}
    ; {otherwise} ->
    {empty_set(Empty)},
    add_values_to_set(Values,Empty,Value)).

compile_expression2(empty_set,_Env,Value) --> !,
    {empty_set(Empty)},emit(Value=Empty).

compile_expression2(empty_sequence,Env,Value) --> !,
    compile_expression2(empty_set,Env,Value).

compile_expression2(comprehension_set(Params,Condition),Env,Value) --> !,
    {term_variables(Env,EnvVariables),
    compile_set_comprehension(Params,Condition,Env,ElementValue,Body,[]),
    term_variables(Body,UsedVariables),
    intersect_variables(UsedVariables,EnvVariables,WaitVariables)},
    emit(set_comprehension(Body,ElementValue,WaitVariables,Value)).

compile_expression2(first(Seq),Env,Value) --> !,
    compile_expression(Seq,Env,SeqValue),
    emit(first_of_sequence(SeqValue,Value)).

compile_expression2(tail(Seq),Env,Value) --> !,
    compile_expression(Seq,Env,SeqValue),
    emit(tail_of_sequence(SeqValue,Value)).

compile_expression2(overwrite(Rel,New),Env,Value) --> !,
    compile_expression(Rel,Env,RelValue),
    compile_expression(New,Env,NewValue),
    emit(override_relation(RelValue,NewValue,Value)).

compile_expression2(insert_front(Front,Seq),Env,Value) --> !,
    compile_expression(Front,Env,FrontValue),
    compile_expression(Seq,Env,SeqValue),
    emit(insert_at_front_of_sequence(SeqValue,FrontValue,Value)).

compile_expression2(couple(A,B),Env,Value) --> !,
    {Value = (AV,BV)},
    compile_expression(A,Env,AV), compile_expression(B,Env,BV).

compile_expression_l([],_,[]) --> !.

compile_expression_l([Expr|Erest],Env,[Value|Vrest]) -->
    compile_expression(Expr,Env,Value),
    compile_expression_l(Erest,Env,Vrest).

compile_if(If,Rest,Env) -->
    {get_texpr_expr(If,if_elsif(P,S))},
    compile_if2(Rest,P,S,Env).

compile_if2([],P,S,Env) -->
    compile_predicate(P,Env),
    compile_substitution(S,Env).

compile_if2([Elif|Rest],P,S,Env) -->
    compile_check(P,Env,CheckVar),
    emit(if_pred(CheckVar,Yes,No)),
    { compile_substitution(S,Env,Yes,[]),
    compile_if(Elif,Rest,Env,No,[]) }.

compile_membership(interval(Lower,Upper),ElemValue,Env) -->
    compile_expression(Lower,Env,LValue),
    compile_expression(Upper,Env,UValue),
    emit(check_less_equal(LValue,ElemValue,pred_true)),
    emit(check_less_equal(ElemValue,UValue,pred_true)).

compile_membership(SetExpression,ElemValue,Env) -->
    {SetExpression =.. [BOP,BArg1,BArg2],
    probvm_binary_in_boolean_type(BOP,VMOP,_),
    !,Command =.. [VMOP,ElemValue,Arg1,Arg2]},
    compile_expression(BArg1,Env,Arg1),
    compile_expression(BArg2,Env,Arg2),
    emit(Command).

compile_predicate(TExpr,Env) -->
    {get_texpr_expr(TExpr,Expr), get_texpr_info(TExpr,Info)},
    compile_predicate2(Expr,Info,Env).

compile_predicate2(truth,_,_Env) --> !.

compile_predicate2(falsity,_,_Env) --> !,emit(fail).

compile_predicate2(conjunct(A,B),_,Env) --> !,
    compile_predicate(A,Env), compile_predicate(B,Env).

compile_predicate2(member(El,TSet),_,Env) -->
    {get_texpr_expr(TSet,Set)},
    compile_expression(El,Env,ElValue),
    compile_membership(Set,ElValue,Env).

compile_predicate2(implication(A,B),_,Env) -->
    compile_check(A,Env,CheckVar),!,
    { compile_predicate(B,Env,Then,[]) },
    emit(if_pred(CheckVar,Then,[])).

compile_predicate2(Expr,_,Env) -->
    compile_check2(Expr,Env,pred_true),!.

compile_predicate2(exists(Parameters,BCondition),Infos,Env) -->
    { ( memberchk(used_ids(Used),Infos) -> true
    ; otherwise ->
    Used = [], add_error(probvm_interpreter,
    'Expected information of used identifiers in exists operation information',
    Infos, unknown)),
    add_enumerated_identifier(Parameters,_Values,Env,Subenv,Enum,[]),
    compile_predicate(BCondition,Subenv,Condition,[]),
    get_values_if_vars(Used,Env,WaitVars)},
    emit(exists(Condition,WaitVars,Enum)).

compile_set_comprehension(TParams,Condition,Env,ElementValue) -->
    add_enumerated_identifier(TParams,Values,Env,SubEnv),
    {convert_list_into_pairs(Values,ElementValue)},
    compile_predicate(Condition,SubEnv).

compile_substitution(TExpr,Env) -->
    {get_texpr_expr(TExpr,Expr)},
    compile_substitution2(Expr,Env).

compile_substitution2(assign([LHS],[RHS]),Env) -->
    compile_expression(RHS,Env,Value),
    {get_texpr_id(LHS,Id),
    lookup_post_identifier(Id,Env,Var)},
    emit(Var=Value).

compile_substitution2(becomes_element_of([LHS],Set),Env) -->
    compile_expression(Set,Env,SetValue),
    {get_texpr_id(LHS,Id),
    lookup_post_identifier(Id,Env,Value)},
    emit(element_of(Value,SetValue)).

compile_substitution2(becomes_such([TId],Predicate),Env) -->
    add_enumerated_identifier([TId],[Value],Env,SubEnv),
    compile_predicate(Predicate,SubEnv),
    {get_texpr_id(TId,Id), lookup_post_identifier(Id,Env,Var)},
    emit(Var=Value).

compile_substitution2(parallel(Substs),Env) -->
    compile_substitution_l(Substs,Env).

compile_substitution2(any(Ids,P,Subst),Env) -->
    add_enumerated_identifier(Ids,_,Env,SubEnv),
    compile_predicate(P,SubEnv),
    compile_substitution(Subst,SubEnv).

compile_substitution2(precondition(Cond,Subst),Env) -->
    compile_predicate(Cond,Env),
    compile_substitution(Subst,Env).

compile_substitution2(select([When]),Env) -->
    {get_texpr_expr(When,select_when(P,S))},!,
    compile_predicate(P,Env),
    compile_substitution(S,Env).

compile_substitution2(if([If|Elifs]),Env) -->
    compile_if(If,Elifs,Env).

compile_substitution2(skip,_) --> !.

compile_substitution_l([],_) --> !.

compile_substitution_l([Subst|Srest],Env) -->
    compile_substitution(Subst,Env),
    compile_substitution_l(Srest,Env).

create_cmp_env(Pre,Post,cmp(Pre,Post)).

emit(Inst) --> [Inst].

get_values_if_vars([],_,[]).

get_values_if_vars([Id|Rest],Env,Result) :-
    ( lookup_pre_identifier(Id,Env,Value) -> Result = [Value|RRest]
    ; otherwise -> Result = RRest),
    get_values_if_vars(Rest,Env,RRest).

integer_bounds('INTEGER',none,none).

integer_bounds('NATURAL',0,none).

integer_bounds('NATURAL1',1,none).

integer_bounds('NAT',0,MAXINT) :- get_preference(maxint,MAXINT).

integer_bounds('NAT1',1,MAXINT) :- get_preference(maxint,MAXINT).

integer_bounds('INT',MININT,MAXINT) :-
    get_preference(minint,MININT),
    get_preference(maxint,MAXINT).

intersect_variables([],_,[]).

intersect_variables([V|Vrest],List,Result) :-
    ( exact_member(V,List) -> Result=[V|Rrest]
    ; otherwise -> Result=Rrest),
    intersect_variables(Vrest,List,Rrest).

lookup_post_identifier(Id,cmp(_,Post),Value) :- memberchk(Id=Value,Post).

lookup_pre_identifier(Id,cmp(Pre,_),Value) :- memberchk(Id=Value,Pre).

pass --> [].