:- module(skip_pattern_compiler, [
     compile_query_pure/3,
     assert_regular/2
]).

:- use_module(library(clpfd)).
:- use_module(library(ordsets)).
:- use_module(library(varnumbers)).
:- use_module(library(pairs)).
:- use_module('skip_pattern_syntax.pl').

/*
  States a(N, M, Vars, Id, IterVar, WinWar), where:
     N - number used to create states,
     M - number used to create variables,
     Vars - set of current variables,
     Id - identifier of the currently compiled pattern
     IterVar - variable storing iteration stack,
     WinVar - variable storing window stack
*/

state(S), [S] --> [S].
state(S0, S), [S] --> [S0].

fresh_state(S, Vs)
   --> state(a(N0, M0, Vars, Id, IterVar, WinVar), 
             a(N, M0, Vars, Id, IterVar, WinVar)),
       {
          N #= N0 + 1,
          term_to_atom(s(Id, N0), Sid),
          S =.. [Sid, IterVar, WinVar | Vs]
       }.

fresh_states([], []) --> [].
fresh_states([S|States], [Vs|Vss])
   --> fresh_state(S, Vs),
       fresh_states(States, Vss).

fresh_var('$VAR'(M0))
   --> state(a(N0, M0, Vars, Id, IterVar, WinVar), 
             a(N0, M, Vars, Id, IterVar, WinVar)),
       {M #= M0 + 1}.

fresh_vars([]) --> [].
fresh_vars([V|Vs])
   --> fresh_var(V),
       fresh_vars(Vs).

args_fresh_vars([], []) --> [].
args_fresh_vars([_|As], [V|Vs])
   --> fresh_var(V),
       args_fresh_vars(As, Vs).

event_fresh(Event0, Event)
   --> {
      Event0 =.. [Type | Args]
   }, args_fresh_vars(Args, Vs),
   {
      Event =.. [Type | Vs]
   }.

current_vars(Vars)
      --> state(a(_,_, Vars, _, _, _)).

replace_vars(Vars0, Vars)
   --> state(a(N, M, Vars0, Id, IterVar, WinVar), 
             a(N,M, Vars, Id, IterVar, WinVar)).

merge_states(S1, S2, S)
   --> state(a(_, _, _, _, IterVar, WinWar)),
       {
         S1 =.. [Sid1|_],
         S2 =.. [Sid2|_],
         term_to_atom(a(Sid1, Sid2), Sid),
         S =.. [Sid, IterVar, WinWar, S1, S2]
       }.
      

frame_state_push(Frame, S0, S)
   :- S0 =.. [Sid, IterVar | Vs],
      S  =.. [Sid, [Frame | IterVar] | Vs].

win_state_push(StartWindow, S0, S)
   :- S0 =.. [Sid, IterVar, WinVar | Vs],
      S  =.. [Sid, IterVar, [StartWindow|WinVar] | Vs].

reinit_state(S0, S)
   :- S0 =.. [Sid, _, _ | Vs],
      S =.. [Sid, [], []|Vs].


/*
   Translate conditions. Extract references ref(var, field, value)
*/

cond_trans_goals_(
      ref(Var, Field),
      V,
      [ref(Var, Field, V)]
   ) --> fresh_var(V), !.

cond_trans_goals_(Cond, Trans, Goals)
     --> {
            Cond =.. [F|L], 
            dif(F, ref)
         },
         conds_trans_goals_(L, L1, Goals),
         {Trans =.. [F|L1]}.

conds_trans_goals_([],[],[]) --> [].
conds_trans_goals_([C|L],[T|L1], Gs)
  --> cond_trans_goals_(C, T, G),
      conds_trans_goals_(L, L1, Gs0),
      {append(G, Gs0, Gs)}.

glist_goals([], true).
glist_goals([G], G).
glist_goals([G1, G2|Gs], (G1, Goals))
   :- glist_goals([G2|Gs], Goals).

cond_trans(Cond, Goals)
   --> cond_trans_goals_(Cond, T, Gs),
       {
         append(Gs, [T], Gs1),
         glist_goals(Gs1, Goals)
       }.

/*
    Automatons are represented (during compilation) by dicts of the form
    auto{
         transitions: [trans(V, Type, S0, S1):-G, ...],
         epses: [eps(S0, S1), ...],
         skips: [skip(S, V1, event_specs)],
         initial: S,
         final: [S, ...],
         states: [S, ...]
    }
    where event_specs is a list of pairs type-condition.
    An event E is skippable in state S0 iff its type either is not on the list skips or it is 
    and then the condition is satisfied. The variable V1 is used
    to refer to the event under consideration in all the conditions.
*/


compile_query_pure(Id, Pattern, Automaton)
    :- numbervars(Pattern, 0, M0),
       M1 #= M0 + 1,
       M #= M1 +1,
       phrase(comp_aut(Pattern, Automaton), [a(0, M, [], Id, '$VAR'(M0), '$VAR'(M1))], [_]).

comp_aut(empty, auto{
        transitions: [],
        epses: [],
        skips: [],
        initial: S,
        final: [S],
        states: [S]
    })
    --> current_vars(Vs),
        fresh_state(S, Vs).

comp_aut(
   event(Type, V), auto{
        transitions: [(trans(V, Type, S0, S1) :- true)],
        epses: [],
        initial: S0,
        skips: [skip(S0, V1, [])],
        final: [S1],
        states: [S0, S1]
   }) 
   --> fresh_var(V1),
       replace_vars(Vs0, Vs),
       {ord_add_element(Vs0, V, Vs)},
       fresh_states([S0, S1], [Vs0, Vs]).

comp_aut(P1 then P2, auto{
   transitions: Ts,
   epses: Es,
   initial: I,
   skips: Skips,
   final: F,
   states: States
})
--> 
    comp_aut(P1, Auto1),
    comp_aut(P2, Auto2),
    {
      I = Auto1.initial,
      F = Auto2.final,
      append(Auto1.transitions, Auto2.transitions, Ts),
      append(Auto1.epses, Auto2.epses, Es0),
      append(Auto1.skips, Auto2.skips, Skips),
      append(Auto1.states, Auto2.states, States),
      sources_target_acc_epses(Auto1.final, Auto2.initial, Es0, Es)
    }.

comp_aut(P1 or P2, auto{
   transitions: Ts,
   epses: [(eps(S0, I1) :- true), (eps(S0, I2) :- true)|Es],
   skips: Skips,
   initial: S0,
   final: Fs,
   states: [S0|States]
})
   --> current_vars(Vs0),
       comp_aut(P1, Auto1),
       replace_vars(Vs1, Vs0),
       comp_aut(P2, Auto2),
       replace_vars(Vs2, Vs),
       {
          I1 = Auto1.initial,
          I2 = Auto2.initial,
          ord_intersection(Vs1, Vs2, Vs),
          append(Auto1.transitions, Auto2.transitions, Ts),
          append(Auto1.epses, Auto2.epses, Es),
          append(Auto1.skips, Auto2.skips, Skips),
          append(Auto1.final, Auto2.final, Fs),
          append(Auto1.states, Auto2.states, States)
       },
       fresh_state(S0, Vs0).

comp_aut(P1 and P2, auto{
   transitions: Trans,
   epses: [(eps(NewInit, I) :- true), (eps(F, NewFinal) :- true)|Es],
   skips: Skips,
   initial: NewInit,
   final: [NewFinal],
   states: States
})
   --> current_vars(Vs0),
       comp_aut(P1, Auto10),
       replace_vars(Vs1, Vs0),
       comp_aut(P2, Auto20),
       replace_vars(Vs2, Vs),
       {
          ord_union(Vs1, Vs2, Vs)
       },
       fresh_states([NewInit, NewFinal], [Vs0, Vs]),
       localize_auto(Auto10, Auto1, F1, Vs1),
       localize_auto(Auto20, Auto2, F2, Vs2),
       merge_states(F1, F2, F),
       merge_states(Auto1.initial, Auto2.initial, I),
       collect_lists(Auto1.states, Auto2.states, cartesian_, [], States),
       collect_lists(Auto1.epses, Auto2.states, merge_eps_(left), [], Es1),
       collect_lists(Auto2.epses, Auto1.states, merge_eps_(right), Es1, Es),
       collect_lists(Auto1.skips, Auto2.skips, merge_skips_(F1, F2), [], Skips),
       collect_lists(Auto1.transitions, Auto2.skips, 
                     merge_trans_skip_(left), [], Trans1),
       collect_lists(Auto2.transitions, Auto1.skips, 
                     merge_trans_skip_(right), Trans1, Trans2),
       collect_lists(Auto1.transitions, Auto2.transitions, 
                        merge_trans_, Trans2, Trans).

comp_aut(iter(P), Auto)
   --> current_vars(Vs),
       comp_aut(P, Auto0),
       replace_vars(_,Vs),
       {
         sources_target_acc_epses(Auto0.final, Auto0.initial, Auto0.epses, Es),
         Auto = Auto0.put([epses=Es])
       }.

comp_aut(iter(P, Event, V), Auto)
--> 
    current_vars(Vs0),
    comp_aut(P, Auto0),
    {ord_add_element(Vs0, V, Vs)},
    fresh_states([IterInit, IterFinal], [Vs0, Vs]),
    event_fresh(Event, EventFresh0),
    event_fresh(Event, EventFresh),
    cond_trans_goals_(Event, EventT, GoalList0),
    {
       EventT =.. [Type|ExprList],
       maplist(init_expr, ExprList, InitList),
       InitEvent =.. [Type|InitList],
       frame_state_push(InitEvent, Auto0.initial, I),
       maplist(frame_state_push(EventFresh0), Auto0.final, FinalN),
       frame_state_push(EventFresh, Auto0.initial, NextIter),
       EventFresh0 =.. [_|Xs0],
       EventFresh =.. [_|Xs],
       maplist(update_goal, ExprList, Xs0, Xs, UpdGoalList),
       append(GoalList0, UpdGoalList, GoalList),
       glist_goals(GoalList, Goals),
       glist_goals([V=EventFresh|GoalList], GoalsFinal),
       sources_target_cond_acc_epses(FinalN, NextIter, Goals, 
                                     [(eps(IterInit, I) :- true)|Auto0.epses], 
                                     Epses0),
       sources_target_cond_acc_epses(FinalN, IterFinal, 
                                     GoalsFinal, Epses0, Epses),
       Auto = Auto0.put([epses=Epses, initial=IterInit, final=[IterFinal], 
                         states=[IterInit, IterFinal|Auto0.states]])
    },
    replace_vars(_, Vs).      


comp_aut(filter(P, Cond), Auto)
   --> 
       comp_aut(P, Auto0),
       current_vars(Vs),
       fresh_state(S, Vs),
       cond_trans(Cond, C),
       {
         sources_target_cond_acc_epses(Auto0.final, S, C, Auto0.epses, Es),
         Auto = Auto0.put([epses=Es, final=[S], states=[S|Auto0.states]])
       }.


comp_aut(unless(P, event(Type, V), Cond), Auto1)
   -->
       comp_aut(P, Auto),
       cond_trans(#\ Cond, C),
       {
          maplist(mod_skip(Type, V, C), Auto.skips, Skips),
          Auto1 = Auto.put([skips=Skips])
       }. 

comp_aut(P within DT,  auto{
   transitions: Trans,
   epses: [(eps(NewInit, I) :- true)|Epses],
   skips: Auto0Skips,
   initial: NewInit,
   final: [NewFinal],
   states: [NewInit, NewFinal| Auto0States]
}) --> 
       current_vars(Vs0),
       comp_aut(P, Auto0),
       current_vars(Vs1),
       fresh_states([NewInit, NewFinal], [Vs0, Vs1]),
       fresh_vars([T0, T1, X]),
       {
         Auto0Skips = Auto0.skips,
         Auto0States = Auto0.states,
         win_state_push(w(T0, a), Auto0.initial, I),
         maplist(win_state_push(w(T0, X)), Auto0.final, FinalN),
         sources_target_acc_epses(FinalN, NewFinal, Auto0.epses, Epses),
         maplist(window_trans(T0, T1, X, DT), Auto0.transitions, Trans)
       }.

window_trans(T0, T1, X, DT, 
   (trans(V, Type, S0, S1) :- G), 
   (trans(V, Type, ST0, ST1) :- G, event_time(V, T1), update_time(X, T0, T1, DT))
) :- win_state_push(w(T0, X), S0, ST0),
     win_state_push(w(T0, b), S1, ST1).

init_expr(sum(_), 0).
update_goal(sum(E), X0, X, X #= X0 + E).

mod_skip(Type, V0, C0, skip(S, V, L0), skip(S,  V, L))
    :- renumber_var(V0, V, C0, C),
       mod_or_add_skip_rules(Type, C, L0, L).

mod_or_add_skip_rules(Type, C, [], [Type-C]).
mod_or_add_skip_rules(Type, C, [Type-C0 | L0], [Type-(C, C0) |L0]).
mod_or_add_skip_rules(Type, C, [Type0-C0 | L0], [Type0-C0 | L])
    :- dif(Type, Type0),
       mod_or_add_skip_rules(Type, C, L0, L).

renumber_var('$VAR'(N0), '$VAR'(N), '$VAR'(N0), '$VAR'(N)).
renumber_var('$VAR'(N0), _, '$VAR'(N), '$VAR'(N))
     :- N0 #\= N.
renumber_var('$VAR'(N0), '$VAR'(N), C0, C)
      :- C0 =.. [F|Args0],
         dif(F, '$VAR'),
         maplist(renumber_var('$VAR'(N0), '$VAR'(N)), Args0, Args),
         C =.. [F|Args].

sources_target_acc_epses([], _, L, L).
sources_target_acc_epses([S|Ss], T, Acc, L)
    :- sources_target_acc_epses(Ss, T, [(eps(S, T) :- true)|Acc], L).

sources_target_cond_acc_epses([], _, _, L, L).
sources_target_cond_acc_epses([S|Ss], T, C, Acc, L)
    :- sources_target_cond_acc_epses(Ss, T, C, [(eps(S, T) :- C)|Acc], L).

localize_auto(Auto0, Auto, F, Vs)
--> state(a(_, _, _, _, IterVar, WinWar)),
    fresh_state(F, Vs),
    fresh_vars([NewIter, NewWin, V]),
    {
      States = [F|Auto0.states],
      sources_target_acc_epses(Auto0.final, F, Auto0.epses, Epses),
      Skips = [skip(F, V, [])|Auto0.skips],
      reinit_state(Auto0.initial, NewInitial),
      Auto1 = Auto0.put([initial=NewInitial, 
                        states=States, 
                        final=[F],
                        epses=Epses,
                        skips=Skips]),
      renumber_var(IterVar, NewIter, Auto1, Auto2),
      renumber_var(WinWar, NewWin, Auto2, Auto)
    }. 

collect_lists([], _, _, Out, Out) --> [].
collect_lists([L0|Ls0], Ls1, F, Buf0, Out)
   --> collect_list(Ls1, L0, F, Buf0, Buf1),
       collect_lists(Ls0, Ls1, F, Buf1, Out).
collect_list([], _, _, Out, Out) --> [].
collect_list([L1|Ls1], L0, F, Buf0, Out)
   --> call(F, L0, L1, Buf0, Buf1),
       collect_list(Ls1, L0, F, Buf1, Out).

cartesian_(S1, S2, Ls, [S|Ls])
   --> merge_states(S1, S2, S).

merge_eps_(Dir, (eps(S0, S1) :- G), S, Buf, [(eps(Sm0, Sm1) :- G)|Buf])
   --> merge_states(Dir, S0, S, Sm0),
       merge_states(Dir, S1, S, Sm1).

merge_states(left, S1, S2, S)
   --> merge_states(S1, S2, S).
merge_states(right, S1, S2, S)
   --> merge_states(S2, S1, S).

merge_skips_(F1, F2, skip(S1, V1, L1), skip(S2, V2, L2),  Buf, Buf1)
   --> {S1=F1, S2=F2} -> {Buf1 = Buf} ; (
         merge_states(S1, S2, S),
         {
            renumber_var(V1, V2, L1, L11),
            merge_specs(L11, L2, L),
            Buf1 = [skip(S, V2, L)|Buf]
         }
   ). 

merge_specs([], Spec, Spec).
merge_specs([Pair|Spec0], Spec1, Spec)
   :- merge_spec(Spec1, Pair, Spec2),
      merge_specs(Spec0, Spec2, Spec).

merge_spec([], Pair, [Pair]).
merge_spec([Type-Cond0|Spec0], Type-Cond, [Type-(Cond0, Cond)|Spec0]) 
   :- !.
merge_spec([Type0-Cond0|Spec0], Type-Cond, [Type0-Cond0|Spec])
   :- dif(Type0, Type),
      merge_spec(Spec0, Type-Cond, Spec).

merge_trans_skip_(
   Dir,
   (trans(V, Type, S0, S1):-G), 
   skip(S2, V1, L), 
   Buf,
   [(trans(V, Type, Sm0, Sm1):-C, G)|Buf]
) --> merge_states(Dir, S0, S2, Sm0),
      merge_states(Dir, S1, S2, Sm1),
      {
         type_spec_cond(Type, L, C0),
         renumber_var(V1, V, C0, C)
      }.

type_spec_cond(_, [],  true).
type_spec_cond(Type, [Type-C|_], C) :- !.
type_spec_cond(Type, [Type1-_|L], C)
   :- dif(Type, Type1),
      type_spec_cond(Type, L, C).

merge_trans_(
      (trans(V1, Type1, S10, S11) :- G1),
      (trans(V2, Type2, S20, S21) :- G2),
      Buf, Buf1
   ) --> {Type1 = Type2} -> (
            merge_states(S10, S20, S0),
            merge_states(S11, S21, S1),
            {Buf1 = [(trans(V2, Type2, S0, S1) :- V1=V2, G1, G2)|Buf]}
        ) ; {Buf1 = Buf}. 

/*
   Asserting compiled automaton.
*/

assert_auto(Id, Auto)
:- maplist(assert_trans, Auto.transitions),
   maplist(assert_trans, Auto.epses),
   maplist(assert_skip, Auto.skips),
   Auto.initial =.. [Sid, _, _|Xs], 
   Init =.. [Sid, [], []|Xs],
   assertz(so_automaton:initial(Id, Init)),
   maplist(assert_final, Auto.final).

assert_trans((trans(V, Type, S0, S1) :- G))
   :- assertz((so_automaton:trans(S0, V, S1) :- event_type(V, Type), G)).

assert_trans((eps(S0, S1) :- G))
   :- assertz(so_automaton:eps(S0, S1):-G).

assert_final(S)
   :- assertz(so_automaton:final(S)).

dif_(A, B, dif(A, B)).

assert_skip(skip(S, V, L))
   :- pairs_keys(L, Types),
      maplist(assert_exceptional_skip(S, V), L),
      maplist(dif_(Type__), Types, DifList),
      glist_goals([event_type(V, Type__)|DifList], DifGoals),
      assertz(so_automaton:skip(S, V) :- DifGoals).

assert_exceptional_skip(S, V, Type-Cond)
    :- assertz((so_automaton:skip(S, V) :- event_type(V, Type), Cond)).

assert_regular(Id, Pattern)
    :-  compile_query_pure(Id, Pattern, Auto0),
        varnumbers(Auto0, Auto),
        writeln(Auto),
        assert_auto(Id, Auto).