% Copyright (C) 2013, 2017 Peter Schueller <schueller.p@gmail.com>

#script (lua)
  function args(t)
    return t:args()
  end

  function name(t)
    return t:name()
  end

  function contains(term,item)
    for k,v in pairs(term:args()) do
      if tostring(v)==tostring(item) then
        return 1
      end
    end
    return 0
  end
  
  function concat(t)
    local res = ""
    for k,v in pairs(t:args()) do
      res = res .. tostring(v)
    end
    if res ~= "" then
      return res
    else
      return {}
    end
  end

  function argumentsAsSet(t)
    local res = ""
    for k,v in pairs(t:args()) do
      res = res .. "," .. tostring(v)
    end
    if res ~= "" then
      return "\\{" .. string.sub(res,2) .. "\\}"
    else
      return "\\{\\}"
    end
  end
#end.

% set library
% construct empty set: @set()
% construct one-element set: @set(elem1)
% construct multi-element set: @set((elem1,elem2,elem3))
% set union: @setunion(S1,S2)
% set union: @setintersection(S1,S2)
% set member: @setintersection(S1,S2)
% set to string conversion: @settostring(S)
% set comparison: S1 == S2, S1 != S2, S1 < S2, ...
#script (lua)
  -- transforms a lua table
  --    { [string_of_setmember] = Val_of_setmember, ... }
  -- that represents a set into a sorted lua table
  --    { [0] = Val_of_setmember, [1] = ... }
  function sethelperAssocToSortedIArray(assoctable)
    -- first sort the strings we use as indices
    a = {}
    for k, n in pairs(assoctable) do
      table.insert(a, k)
    end
    table.sort(a)
    -- now put the Val s corresponding to indices into b
    b = {}
    for k, n in ipairs(a) do
    	table.insert(b,assoctable[n])
    end
    return b
  end

  function set(elem)
    if elem == nil then
      return gringo.Fun("set")
    else
      local elements = {}
      if #elem:args() == 0 then
        elements[1] = elem
      else
        for k,v in pairs(elem:args()) do
          elements[tostring(v)] = v
        end
        elements = sethelperAssocToSortedIArray(elements)
      end
      return gringo.Fun("set", elements)
    end
  end

  function setunion(s1,s2)
    local elements = {}
    if Val.type(s1) == Val.FUNC then
      -- TODO error if s1:name() is not 'set'
      for k,v in pairs(s1:args()) do
        elements[tostring(v)] = v
      end
    end
    if Val.type(s2) == Val.FUNC then
      -- TODO error if s2:name() is not 'set'
      for k,v in pairs(s2:args()) do
        elements[tostring(v)] = v
      end
    end
    elements = sethelperAssocToSortedIArray(elements)
    return Val.new(Val.FUNC, "set", elements)
  end

  function setintersection(s1,s2)
    local elements1 = {}
    if Val.type(s1) == Val.FUNC then
      -- TODO error if s1:name() is not 'set'
      for k,v in pairs(s1:args()) do
        elements1[tostring(v)] = v
      end
    end
    local elements2 = {}
    if Val.type(s2) == Val.FUNC then
      -- TODO error if s2:name() is not 'set'
      for k,v in pairs(s2:args()) do
        if elements1[tostring(v)] ~= nil then
          elements2[tostring(v)] = v
	end
      end
    end
    elements2 = sethelperAssocToSortedIArray(elements2)
    return Val.new(Val.FUNC, "set", elements2)
  end

  function setmember(elem,set)
    for k,v in pairs(set:args()) do
      if tostring(elem) == tostring(v) then
        return 1
      end
    end
    return 0
  end

  function settostring(t)
    -- TODO error if t:name() is not 'set'
    local res = ""
    for k,v in pairs(t:args()) do
      res = res .. "," .. tostring(v)
    end
    if res ~= "" then
      return "{" .. string.sub(res,2) .. "}"
    else
      return "{}"
    end
  end

  function setelement(set)
    local res = {}
    for k,v in pairs(set:args()) do
      table.insert(res,v)
    end
    return res
  end
  -- foo(G,ID,E) :- dep(G,ID,_,_,S), E = @setelement(S).
  -- foo(G,ID,@setelement(S)) :- dep(G,ID,_,_,S).
#end.

#script (lua)
  function valuesAsList(tbl)
    local ret = ""
    for k,v in pairs(tbl) do
      ret = ret .. "," .. tostring(v)
    end
    ret = string.sub(ret,2)
    return ret
  end

  function keysAsList(tbl)
    local ret = ""
    for k,v in pairs(tbl) do
      ret = ret .. "," .. tostring(k)
    end
    ret = string.sub(ret,2)
    return ret
  end

  function cident(s)
    local res = tostring(s)
    res = string.gsub(res,"%(","")
    res = string.gsub(res,"%)","")
    res = string.gsub(res,",","_")
    res = string.gsub(res," ","_")
    return res
  end

  function logtable(t)
  	for k,v in pairs(t) do
		print(k,v)
	end
  end

  function map(func, array)
      local new_array = {}
      for i,v in ipairs(array) do
          new_array[i] = func(v)
      end
      return new_array
  end

  function filterPred(pred,model)
    local result = {}
    for i,v in pairs(model:atoms()) do
      if v:name() == pred then
        table.insert(result, v:args())
      end
    end
    return result
  end

  function printGraph(m,graph)
    local gid = graph
    print("digraph witness {")
    print("layout=dot;")
    -- get nodes
    local nodes = {}
    for i,node in pairs(filterPred("gn",m)) do
      if gid == node[1] then
        local n = node[2]
        local nid = cident(n)
        nodes[nid] = { ["aspnid"] = n, ["type"] = {}, ["attr"] = {} }
      end
    end
    -- get properties
    for i,prop in pairs(filterPred("gp",m)) do
      if gid == prop[1] then
        local nid = cident(prop[2])
        local name = tostring(prop[3])
        local setelement = tostring(prop[4])
	if nodes[nid][name] == nil then
          nodes[nid][name] = { [setelement] = 1 }
	else
	  nodes[nid][name][setelement] = 1
	end
      end
    end
    -- print error messages
    local msg = ""
    for i,err in pairs(filterPred("error",m)) do
      msg = msg .. "\\n" .. tostring(err[1]) .. " " .. tostring(err[2])
    end
    if msg ~= "" then
      print("{ rank=min; error [shape=rectangle,style=filled,color=red,label=\"" .. string.sub(msg,3) .. "\"]; }")
    end
    -- print nodes
    for nid,data in pairs(nodes) do
      local nstr = nid .. "[shape=rectangle"
      local label = ""
      -- label = label .. tostring(data["aspnid"]) .. " "
      nstr = nstr .. ",tooltip=\"" .. tostring(data["aspnid"]) .. "\""
      if data["type"]["dep"] == 1 then
        nstr = nstr .. ",color=white"
      elseif data["type"]["nom"] == 1 then
        nstr = nstr .. ",style=filled,color=lightblue"
        label = label .. keysAsList(data["name"]) .. "(E)"
      elseif data["type"]["act"] == 1 then
        nstr = nstr .. ",style=filled,color=orange"
        label = label .. keysAsList(data["name"]) .. "(A)"
      elseif data["type"]["mod"] == 1 then
        nstr = nstr .. ",style=filled,color=green"
        label = label .. keysAsList(data["name"]) .. "(M)"
      end
      -- attr
      local attrstr = keysAsList(data["attr"])
      if #attrstr > 0 or data["type"]["dep"] == 1 then
        label = label .. " \\{" .. attrstr .. "\\}"
      end
      label = ",label=\"" .. label .. "\""
      -- print
      print(nstr .. label .. "];")
    end
    -- print edges
    for i,edge in pairs(filterPred("ge",m)) do
      if gid == edge[1] then
        local fromid = cident(edge[2])
        local toid = cident(edge[3])
	if nodes[fromid]["attr"]["meta"] == 1 then
	  print(fromid .. " -> " .. toid .. " [style=dashed];")
	elseif nodes[toid]["attr"]["meta"] == 1 then
	  print(fromid .. " -> " .. toid .. " [style=dashed,arrowhead=none];")
	elseif nodes[toid]["type"]["dep"] == 1 then
          print(fromid .. " -> " .. toid .. " [arrowhead=none];")
	else
          print(fromid .. " -> " .. toid .. ";")
	end
      end
    end
    -- print extra messages
    local msg = ""
    for i,message in pairs(filterPred("print",m)) do
      msg = msg .. "\\n" .. tostring(message[1])
    end
    if msg ~= "" then
      print("{ rank=source; msg [shape=rectangle,label=\"" .. string.sub(msg,3) .. "\"]; }")
    end
    -- finish graph
    print("}")
  end

  function onModel(m)
    -- normal model printing
    -- print(table.concat(map(tostring, m:atoms()), ","))
    for i,graph in pairs(filterPred("gprint",m)) do
      printGraph(m,graph[1])
    end
  end

  function main(prg)
    prg:ground({{"base", {}}})
    return prg:solve(nil,onModel)
  end
#end.

% translating graph input into graph processor concepts

concept(G,ID,nom,Name) :- nom(G,ID,Name).
concept(G,ID,act,Name) :- act(G,ID,Name).
concept(G,ID,mod,Name) :- mod(G,ID,Name).
gn(G,ID) :- concept(G,ID,_,_).
gp(G,ID,name,Name) :- concept(G,ID,_,Name).
gp(G,ID,type,Type) :- concept(G,ID,Type,_).

gn(G,ID) :- dep(G,ID,_,_,_).
gp(G,ID,type,dep) :- dep(G,ID,_,_,_).
gp(G,ID,attr,@setelement(Attrib)) :- dep(G,ID,_,_,Attrib).

ge(G,FromID,ID) :- dep(G,ID,FromID,_,_).
ge(G,ID,ToID) :- dep(G,ID,_,ToID,_).

graph(G) :- gn(G,_).

% graph library:
%
% gn(GraphID,NodeID):
% define graph node
%
% gp(GraphID,NodeID,PropertyName,PropertyValue):
% define node property, properties can have multiple values (set semantics)
%
% ge(GraphID,NodeFromID,NodeToID):
% define graph edge
%
% gcontract(Mod,Graph,Node1,Node2):
% add "unify nodes Node1 and Node 2" to graph modification set (modset) Mod
%
% gremove(Mod,Graph,Node):
% add "remove node Node" from graph modification set (modset) Mod
%
% gmodimport(IntoMod,FromMod):
% add modifications in modset FromMod to modset IntoMod
%
% gimport(IntoGraphID,FromGraphID,NodeAdorn,Mod):
% import one graph into another one, applying modset
% * adorning node identifiers to create new node identifiers
% * NodeAdorn allows to import graphs multiply
% * imported node id becomes i(FromGID,FromNID,NodeAdorn)
%

gmod(Mod,Graph) :- gcontract(Mod,Graph,_,_).

% assertion: modset is about just one graph
error("invalid modset with multiple graphs (mod,g1,g2)",
	@concat((Mod," ",G1," ",G2))) :-
	gmod(Mod,G1), gmod(Mod,G2), G1<G2.
% assertion: we only contract nodes that are in the graph (1)
error("invalid contraction of n1 (mod,graph,n1,n2)",
	@concat((Mod," ",G," ",N1," ",N2))) :-
	gcontract(Mod,G,N1,N2), not gn(G,N1).
% assertion: we only contract nodes that are in the graph (2)
error("invalid contraction of n2 (mod,graph,n1,n2)",
	@concat((Mod," ",G," ",N1," ",N2))) :-
	gcontract(Mod,G,N1,N2), not gn(G,N2).
% assertion: we cannot contract nodes that are eliminated (1)
error("invalid contraction of eliminated n1 (mod,graph,n1,n2)",
	@concat((Mod," ",G," ",N1," ",N2))) :-
	gcontract(Mod,G,N1,N2), gremove(Mod,G,N1).
% assertion: we cannot contract nodes that are eliminated (2)
error("invalid contraction of eliminated n2 (mod,graph,n1,n2)",
	@concat((Mod," ",G," ",N1," ",N2))) :-
	gcontract(Mod,G,N1,N2), gremove(Mod,G,N2).

% modset importing
gcontract(IntoMod,G,N1,N2) :-
	gmodimport(IntoMod,FromMod), gcontract(FromMod,G,N1,N2).
gremove(IntoMod,G,N) :-
	gmodimport(IntoMod,FromMod), gremove(FromMod,G,N).

%
% define equivalence clusters of nodes in contraction of graph
%

% reflexivity
gnequiv(Mod,G,N,N) :- gn(G,N), gmod(Mod,G), not gremove(Mod,G,N).
% symmetry
gnequiv(Mod,G,N1,N2) :- gnequiv(Mod,G,N2,N1).
% transitivity
gnequiv(Mod,G,N1,N3) :- gnequiv(Mod,G,N1,N2), gnequiv(Mod,G,N2,N3), N1<N2, N2<N3.
% equivalence due to contraction
gnequiv(Mod,G,N1,N2) :- gmod(Mod,G), gn(G,N1), gn(G,N2), gcontract(Mod,G,N1,N2), N1 < N2.

%
% define nodes representing clusters
% gnrepresentative(Mod,G,N1,N2) means that N1 represents N2
%
% lexicographically smallest representative of clusters with more than 1 node
gneq_lt(Mod,G,N1,N2) :- gnequiv(Mod,G,N1,N2), N1 < N2.
gneq_notsmallest(Mod,G,N1,N2) :- gneq_lt(Mod,G,N1,N2), gneq_lt(Mod,G,N0,N1).
gnrepresentative(Mod,G,N1,N2) :- gneq_lt(Mod,G,N1,N2), not gneq_notsmallest(Mod,G,N1,N2). 
gnrepresented(Mod,G,N2) :- gnrepresentative(Mod,G,N1,N2), N1 != N2.

%
% define node targets in graph
%
% nonrepresented node is its own target
gntarget(IntoG,i(G,N,Adorn),G,N,Adorn) :- 
	gimport(IntoG,G,Adorn,Mod), gn(G,N),
	not gnrepresented(Mod,G,N),
	not gremove(Mod,G,N).
% represented node has representative as target 
gntarget(IntoG,i(G,N,Adorn),G,NFrom,Adorn) :- 
	gimport(IntoG,G,Adorn,Mod), gn(G,NFrom),
	gnrepresentative(Mod,G,N,NFrom).

% new nodes
gn(IntoG,N) :- gntarget(IntoG,N,_,_,_).
% new properties
gp(IntoG,i(G,N,Adorn),Attr,Value) :-
	gntarget(IntoG,i(G,N,Adorn),G,NFrom,Adorn), gp(G,NFrom,Attr,Value).
% new edges
ge(IntoG,From,To) :-
	gimport(IntoG,G,Adorn,_), ge(G,GFrom,GTo),
	gntarget(IntoG,From,G,GFrom,Adorn), gntarget(IntoG,To,G,GTo,Adorn).

% gguesscontractions(G,M):
% guess contrations from graph G into modset M
%
% gguesscontractions_intergraph(G,MS,G1,Adorn1,G2,Adorn2):
% guess contractions into modset MS on graph G
% between graph G1 imported (into G) with Adornment1
% and graph G2 imported (into G) with Adornment2
% (but not within graph G1 and not within graph G2)
%
% gprint(G):
% print graph G (only one)
%
% print(Msg):
% print message (multiple possible)
%
% gprintrepresentatives(G,M):
% print representatives of nodes including names in modset M of graph G

% gguesscontractions/2
{ gcontract(MS,G,N1,N2) } :-
	gguesscontractions(G,MS),
	gn(G,N1), gn(G,N2), N1 < N2,
	not gremove(MS,G,N1), not gremove(MS,G,N2),
	gp(G,N1,type,Type), gp(G,N2,type,Type).


% gguesscontractions_intergraph/6 (G,MS,G1,Adorn1,G2,Adorn2)
{ gcontract(MS,G,i(G1,N1,Adorn1),i(G2,N2,Adorn2)) } :-
	gguesscontractions_intergraph(G,MS,G1,Adorn1,G2,Adorn2),
	gn(G,i(G1,N1,Adorn1)), gn(G,i(G2,N2,Adorn2)),
	gp(G,i(G1,N1,Adorn1),type,Type), gp(G,i(G2,N2,Adorn2),type,Type).
% requires that there is gimport(_,G,_,MS) and gimport(G,G1,Adorn1,_) and gimport(G,G2,Adorn2,_)
cangguesscontractions_intergraph(G,MS,G1,Adorn1,G2,Adorn2) :-
	gimport(_,G,_,MS), gimport(G,G1,Adorn1,_), gimport(G,G2,Adorn2,_).
error(@concat(("malformed gguesscontractions_intergraph(",G,",",MS,",",G1,",",Adorn1,",",G2,",",Adorn2))) :-
	gguesscontractions_intergraph(G,MS,G1,Adorn1,G2,Adorn2),
	not cangguesscontractions_intergraph(G,MS,G1,Adorn1,G2,Adorn2).


% gprintrepresentatives/2
print(@concat((N1," (",Name1,") <= ",N2," (",Name2,")"))) :-
	gprintrepresentatives(G,Mod),
	gnrepresentative(Mod,G,N1,N2),
	gp(G,N1,name,Name1), gp(G,N2,name,Name2).

% make transitivity/commutativity explicit
% (this eliminates solutions that are equal except for gcontract/4
gcontract(M,G,N1,N3) :- gcontract(M,G,N1,N2), gcontract(M,G,N2,N3), N1 != N2.
gcontract(M,G,N1,N2) :- gcontract(M,G,N2,N1).

% forbid nodes to obtain two types
constr :- gn(G,N), 2 { gp(G,N,type,V) }.

% forbid nodes to obtain two incoming object arrows
constr :- ge(G,FN1,TN), ge(G,FN2,TN), FN1 < FN2, gp(G,FN1,attr,Obj), gp(G,FN2,attr,Obj), Obj = obj.
constr :- ge(G,FN1,TN), ge(G,FN2,TN), FN1 < FN2, gp(G,FN1,attr,Obj), gp(G,FN2,attr,Obj), Obj = obj2.

% forbid to create nodes with incompatible names (isa makes compatible)
constr :- gp(G,N,name,Name1), gp(G,N,name,Name2), Name1 < Name2, not compatible(Name1,Name2).

% forbid to create nodes with incompatible attr (acompat)
constr :- gp(G,N,attr,Attr1), gp(G,N,attr,Attr2), Attr1 < Attr2, not acompat(Attr1,Attr2).

% forbid dependency nodes with two or more non-meta incoming arrows
constr :- gp(G,N,type,dep), ge(G,From1,N), ge(G,From2,N), From1 < From2, not gp(G,From1,attr,meta), not gp(G,From2,attr,meta).

% forbid dependency nodes with two or more non-meta outgoing arrows
constr :- gp(G,N,type,dep), ge(G,N,To1), ge(G,N,To2), To1 < To2, not gp(G,To1,attr,meta), not gp(G,To2,attr,meta).

% forbid multiple dependencies between two nodes (in the same direction)
constr :- ge(G,N1,Ndep1), gp(G,Ndep1,type,dep), ge(G,Ndep1,N2), Ndep1 < Ndep2,
   ge(G,N1,Ndep2), gp(G,Ndep2,type,dep), ge(G,Ndep2,N2).

%
% forbidden_equivalence/3(G,N1,N2):
% nodes N1 and N2 from graph G must not be contracted into one node
% (mixed graphs inherit this property)
%
% assertion: forbidden equivalence must concern two nodes in a graph
error("invalid forbidden equivalence N1 (G,N1,N2)",
	@concat((G," ",N1," ",N2))) :-
	forbidden_equivalence(G,N1,N2), not gn(G,N1).
error("invalid forbidden equivalence N2 (G,N1,N2)",
	@concat((G," ",N1," ",N2))) :-
	forbidden_equivalence(G,N1,N2), not gn(G,N2).
error("invalid forbidden equivalence N1=N2 (G,N1,N2)",
	@concat((G," ",N," ",N))) :-
	forbidden_equivalence(G,N,N).
%
% inheritance in imported/collapsed graphs
forbidden_equivalence(IntoG,IntoN1,IntoN2) :-
	forbidden_equivalence(G,N1,N2),
	gimport(IntoG,G,Adorn,Mod),
	gntarget(IntoG,IntoN1,G,N1,Adorn),
	gntarget(IntoG,IntoN2,G,N2,Adorn).
%
%print(@concat(("forbidden_equivalence: ",G," ",N1," ",N2))) :-
%	forbidden_equivalence(G,N1,N2).

constr :- gnequiv(MS,G,N1,N2), forbidden_equivalence(G,N1,N2).

relation(G,Rel,N1,N2) :-
	ge(G,N1,N12a), gp(G,N12a,type,dep), gp(G,N12a,attr,Rel), ge(G,N12a,N2).

% make sure nothing depends on itself
constr :- relation(G,Rel,N,N).

% object can only be at single location
constr :- relation(G,at,N1,N2), relation(G,at,N1,N3), N2 < N3.


:- constr.

%
% ontology
%

isA(N1,N3) :- isA(N1,N2), isA(N2,N3).
compatible(Name,Name) :- gp(_,_,name,Name).
compatible(N1,N2) :- isA(N1,N2).
compatible(N1,N2) :- compatible(N2,N1).

acompat(Attr,Attr) :- gp(_,_,attr,Attr).
acompat(N1,N2) :- acompat(N2,N1).
acompat(N1,N3) :- acompat(N1,N2), N1 < N2, acompat(N2,N3).