#!/usr/bin/python

"""
Various routines for studying dependencies in agda files
"""


import os
import re
import subprocess
import sys
import tempfile



class BadDag(Exception):
    pass



class Dag():

    def __init__(self,edges=[]):
        self.by_source = {}
        self.by_target = {}
        self.add_edges(edges)

    def edges(self):
        for (v,E) in self.by_source.iteritems():
            for e in E:
                yield (v,e)

    def copy(self):
        G = Dag()
        G.add_edges_unsafe(self.edges())
        return G

    def can_reach(self,x,y):
        if x==y:
            return True
        for x2 in self.by_source[x]:
            if self.can_reach(x2,y):
                return True
        return False

    def add_edge_unsafe(self,x,y):
        if x not in self.by_source:
            self.by_source[x] = set()
        if y not in self.by_source:
            self.by_source[y] = set()
        if x not in self.by_target:
            self.by_target[x] = set()
        if y not in self.by_target:
            self.by_target[y] = set()
        self.by_source[x].add(y)
        self.by_target[y].add(x)

    def add_edges_unsafe(self,edges):
        for (x,y) in edges:
            self.add_edge_unsafe(x,y)

    def add_edge(self,x,y):
        if self.can_reach(y,x):
            raise BadDag
        self.add_edge_unsafe(x,y)

    def add_edges(self,edges):
        edges = list(edges)
        if len(edges) > 0:
            self.add_edges_unsafe(edges)
            self.check()

    def delete_vertex(self,v):
        del(self.by_source[v])
        del(self.by_target[v])
        for (_,E) in self.by_source.iteritems():
            E.discard(v)
        for (_,E) in self.by_target.iteritems():
            E.discard(v)

    def check(self):
        self.copy().destructive_check()

    def destructive_check(self):
        while len(self.by_source) > 0:
            l = list(self.minima())
            if len(l) == 0:
                raise BadDag
            for v in l:
                self.delete_vertex(v)

    def vertices(self):
        "An iter over vertices"
        return self.by_source.iterkeys()

    def minima(self):
        "An iter over minima, or sources: elements with no arrows in"
        for (v,E) in self.by_target.iteritems():
            if len(E) == 0:
                yield v

    def maxima(self):
        "An iter over maxima, or sinks: elements with no arrows out"
        for (v,E) in self.by_source.iteritems():
            if len(E) == 0:
                yield v

    def neighbours(self,v):
        a = set()
        a.update(self.by_source[a],self.by_target[a])
        
    def connected_components(self):
        unused = set(self.vertices())
        components = []
        while len(unused) > 0:
            v = unused.pop()
            new = set([v])
            old = set()
            while len(new) > 0:
                u = new.pop()
                old.add(u)
                for v in self.neighbours(u):
                    if v not in old:
                        new.add(v)
            components.append(old)
                


def test_Dag():

    # K2,2
    a = Dag([(1,3),(1,4),(2,3),(2,4)]) 

    # a branched path
    b = Dag([(1,2),(2,3),(2,30),(3,4),(4,5)])
    assert b.can_reach(1,5)
    assert not(b.can_reach(30,5))

    # a cycle with extra details ; should fail
    try:
        c = Dag([(0,1),(1,2),(2,3),(3,4),(4,5),(5,1)])
        assert False
    except BadDag:
        pass



class BadFile(Exception):
    pass



def create_dependency_dot(name,lookups,dotfile):
    args = ["agda","--dependency-graph=%s"%dotfile] + ["--include-path=%s"%d for d in lookups] + [name]
    subprocess.check_call(args)


def parse_dependency_dot(dotfile):
    names = {}
    r = re.compile('   (.*)\\[label="(.*)"\\];')
    s = re.compile("   (.*) -> (.*);")
    for l in open(dotfile,'r'):
        m = r.match(l)
        if m:
            (x,y) = m.groups()
            names[x] = y
        m = s.match(l)
        if m:
            (x,y) = m.groups()
            yield (names[x],names[y])


def dependency_edges(name,lookups):
    a = tempfile.mkstemp()[1]
    try:
        create_dependency_dot(name,lookups,a)
        for edge in parse_dependency_dot(a):
            yield edge
    finally:
        os.remove(a)


def dependency_graph(name,lookups):
    return Dag(dependency_edges(name,lookups))


def multidependency_edges(names,lookups):
    for name in names:
        for edge in dependency_edges(name,lookups):
            yield edge


def multidependency_graph(names,lookups):
    return Dag(multidependency_edges(names,lookups))



def recursively_find_files(dirname):
    for (d,_,files) in os.walk(dirname):
        for f in files:
            if f[-5:] == ".agda":
                yield (False, os.path.join(d,f))
            elif f[-6:] == ".lagda":
                yield (True, os.path.join(d,f))



if __name__=="__main__":
    # a very small interface at the moment
    # just shows "entry points": files which are not imported by other files

    # sample use:
    #  agda-depends Sheffield/CategoryTheory-Set ./ /home/james/.local/agda-lib
    #  (the first argument is the directory to check, the second and
    #  subsequent are the libraries to use)

    dirname = sys.argv[1]
    lookups = sys.argv[2:]
    files = (x for (t,x) in recursively_find_files(dirname))
    G = multidependency_graph(files, lookups)
    for x in G.minima():
        print x


