import java.io.IOException;
import java.util.*;

import Dep.Absyn.*;

public class Interactive {
/*
        private static void checkTypeJudgement(Type j) {
                try {
                        Exp e = ToExp.toExp(j.eexp_1);
                        Exp t = ToExp.toExp(j.eexp_2);
                        if (!new CheckType().typecheck(e, t)) 
                                throw new TypeException(e + " does not have the type " + t);
                        System.out.println(e + " : " + t + " => OK");
                } catch (TypeException ex) {
                        System.out.println("Error: " + ex.getMessage());
                }
        }
*/
        private static Map<String,Set<String>> findDeps(Map<String,Module> ms) {
                Map<String,Set<String>> deps = new HashMap<String,Set<String>>();
                for (Map.Entry<String,Module> e : ms.entrySet()) {
                        Set<String> s = new HashSet<String>();
                        deps.put(e.getKey(), s);
                        for (Import i : e.getValue().listimport_)
                                s.add(i.ident_);
                }
                return deps;
        }
        
        private static List<String> topologicalSort(Map<String,Set<String>> deps) {
                List<String> sorted = new LinkedList<String>();

                while (!deps.isEmpty()) {
                        // FIXME: use priority queue to get lower complexity
                        String key = null;
                        for (Map.Entry<String,Set<String>> e : deps.entrySet()) {
                                if (e.getValue().isEmpty()) {
                                        key = e.getKey();
                                        break;
                                }
                        }
                        if (key == null)
                                throw new TypeException("Circular module dependency");
                        sorted.add(key);
                        Set<String> ds = deps.remove(key);
                        for (Set<String> s : deps.values())
                                s.remove(key);
                }

                return sorted;
        }

        private static Map<String,Exp> getTypeDecls(List<Decl> decls) {
                Map<String,Exp> r = new HashMap<String,Exp>();
                for (Decl d : decls) {
                        if (d instanceof TypeDecl) {
                                TypeDecl td = (TypeDecl)d;
                                r.put(td.ident_, ToExp.toExp(td.eexp_));
                        }
                }
                return r;
        }

        private static Context checkTypeDecls(Context c, Map<String,Exp> decls) {
                CheckType tc = new CheckType();

                // build value enviroment where constants are mapped to VConsts
                Env rho = c.rho;
                for (String n : decls.keySet()) {
                        if (rho.contains(n))
                                throw new TypeException("Duplicate constant type declaration: " + n);
                        rho = rho.update(n, new VConst(n));
                }
                
                // build type enviroment where constants are mapped to the
                // values of their type expressions
                Env gamma = c.gamma;
                for (Map.Entry<String,Exp> d : decls.entrySet()) {
                        assert !gamma.contains(d.getKey());
                        gamma = gamma.update(d.getKey(), tc.eval(rho, d.getValue()));
                }

                c = new Context(rho, gamma);

                for (Map.Entry<String,Exp> d : decls.entrySet()) {
                        if (!tc.checkTypeType(c, d.getValue()))
                                throw new TypeException("When checking " + d.getKey() + ": " 
                                        + d.getValue() + " is not a type.");
                }

                return c;
        }

        private static Map<String,List<FunCase>> getPattDecls(List<Decl> decls) {
                Map<String,List<FunCase>> ps = new HashMap<String,List<FunCase>>();
                for (Decl d : decls) {
                        if (d instanceof PattDecl) {
                                PattDecl pd = (PattDecl)d;
                                List<FunCase> cs = ps.get(pd.ident_);
                                if (cs == null) {
                                        cs = new LinkedList<FunCase>();
                                        ps.put(pd.ident_, cs);
                                }
                                cs.add(new FunCase(pd.ident_,
                                                   pd.listpattern_, 
                                                   ToExp.toExp(pd.eexp_)));
                        }
                }
                return ps;
        }

        private static void checkPattDecls(Context c, Map<String,List<FunCase>> ps) {
                for (Map.Entry<String,List<FunCase>> e : ps.entrySet()) {
                        Val funType = c.gamma.lookup(e.getKey());
                        for (FunCase fc : e.getValue())
                                checkFunCase(c, fc, funType);
                }
        }

        private static void checkFunCase(Context c, FunCase fc, Val type) {
                // FIXME: we only check declarations without patterns
                if (fc.patterns.isEmpty()) {
                        new CheckType().checkExpType(c, fc.rhs, type);
                }

//                 Map<String,Val> bs = new HashMap<String,Val>();
//                 Val rhsType = checkPatterns(c, fc.patterns, type, bs);
//                 Context c_ = c.extend(bs);
//                 if (!new CheckType().checkExpType(c_, fc.rhs, rhsType))
//                         throw new TypeException("Checking " + fc.name + ": rhs does not have type " 
//                                                 + rhsType);
        }

//         /**
//          *  Check a list of patterns against a function type.
//          *  @param c The external context
//          *  @param ps The patterns
//          *  @param type The function type to check the pattern list against
//          *  @param bs A map of bindings to which all bindings created
//          *  by the patterns will be added.
//          *  @return The type left over
//          */
//         private static Val checkPatterns(Context c, List<Pattern> ps, 
//                                          Val type, Map<String,Val> bs) {

//                 int k = 0;
//                 Val rt = type;
//                 for (Pattern p : ps) {
//                         if (!(rt instanceof VPi))
//                                 throw new TypeException("Trying to match pattern list " + ps 
//                                                         + " against type " + type + ":" 
//                                                         + rt + " is not a product.");
//                         VPi tp = (VPi)rt;
//                         rt = new CheckType().fapp(tp.f, new VGen(k++));
//                         checkPattern(c, p, tp.t, bs);
//                 }               
                
//                 return rt;
//         }

//         /**
//          *  Check the type of a pattern.
//          *  @param p The pattern
//          *  @param type The expected type of the pattern
//          *  @param bs Map to which the bindings created by the pattern will be added.
//          *  @return The type of the pattern
//          */
//        private static Val checkPattern(final Context c, Pattern p, 
//                                        Val type, final Map<String,Val> bs) {

//                 return p.accept(new Pattern.Visitor<Val,Val>() {
//                         public Val visit(PCons p, Val t) {
//                                 Val consType = c.gamma.lookup(p.ident_);
//                                 Val rt = checkPatterns(c, p.listpattern_, consType, bs);

//                                 if (!new CheckType().eqVal(rt, t)) 
//                                         throw new TypeException("Constructor expression " + p 
//                                                                 + " has type " + rt + ", wanted " + t);
                                
//                                 return t;
//                         }
//                         public Val visit(PVar p, Val t) {
//                                 if (bs.containsKey(p.ident_))
//                                         throw new TypeException("Variable " + p.ident_ 
//                                                                 + " already bound in the pattern");
//                                 bs.put(p.ident_, t);
//                                 return t;
//                         }
//                         public Val visit(PType p, Val t) {
//                                 if (!(t instanceof VType))
//                                         throw new TypeException("Pattern " + p + " does not have type " + t);
//                                 return t;
//                         }
//                         public Val visit(PWild p, Val t) {
//                                 return t;
//                         }
//                 }, type);
//         }

        public static void main(String[] args) {    

                try {

                        Map<String,Module> modules = Modules.loadModules(args);
                        Map<String,Set<String>> deps = findDeps(modules);
                        List<String> sorted = topologicalSort(deps);

                        Context c = new Context();
                        Map<String,List<FunCase>> funs = new HashMap<String,List<FunCase>>();
                        for (String s : sorted) {                        
                                Module m = modules.get(s);

                                System.err.println("Checking type declarations in module " + s);
                                Map<String,Exp> types = getTypeDecls(m.listdecl_);
                                c = checkTypeDecls(c, types);

                                System.err.println("Checking function declarations in module " + s);
                                Map<String,List<FunCase>> patts = getPattDecls(m.listdecl_);
                                checkPattDecls(c, patts);
                                funs.putAll(patts);
                        }

                        List<FunCase> mains = funs.get("main");
                        if (mains == null)
                                System.err.println("No main");
                        if (mains.size() > 1)
                                System.err.println("Multiple main cases");
                        Exp main = mains.get(0).rhs;
                        Val v = new CheckType().eval(c.rho, main);
                        System.out.println("main => " + v);

                } catch (TypeException ex) {
                        System.err.println(ex.toString());
                } catch (IOException ex) {
                        System.err.println(ex.toString());
                }

//                 BufferedReader in = new BufferedReader(new InputStreamReader(System.in));
//                 String line;
//                 while ((line = in.readLine()) != null) {
//                         Judge j = ParseJudge.parseJudge(line);
//                         checkJudgement(j);
//                 }

        }

}