package org.simantics.scl.compiler.compilation;

import java.util.ArrayList;
import java.util.Iterator;
import java.util.List;

import org.cojen.classfile.TypeDesc;
import org.simantics.scl.compiler.common.datatypes.Constructor;
import org.simantics.scl.compiler.common.names.Name;
import org.simantics.scl.compiler.constants.JavaTypeInstanceConstructor;
import org.simantics.scl.compiler.constants.SCLConstructor;
import org.simantics.scl.compiler.constants.StringConstant;
import org.simantics.scl.compiler.constants.generic.CallJava;
import org.simantics.scl.compiler.constants.generic.ClassRef;
import org.simantics.scl.compiler.constants.generic.ConvertToListFilter;
import org.simantics.scl.compiler.constants.generic.MethodRef;
import org.simantics.scl.compiler.constants.generic.OutputFilter;
import org.simantics.scl.compiler.constants.generic.ParameterStackItem;
import org.simantics.scl.compiler.constants.generic.PopOutputFilter;
import org.simantics.scl.compiler.constants.generic.StackItem;
import org.simantics.scl.compiler.constants.generic.ThreadLocalStackItem;
import org.simantics.scl.compiler.elaboration.contexts.TranslationContext;
import org.simantics.scl.compiler.elaboration.contexts.TypeTranslationContext;
import org.simantics.scl.compiler.elaboration.errors.NotPatternException;
import org.simantics.scl.compiler.elaboration.expressions.EApply;
import org.simantics.scl.compiler.elaboration.expressions.EGetConstraint;
import org.simantics.scl.compiler.elaboration.expressions.EIntegerLiteral;
import org.simantics.scl.compiler.elaboration.expressions.EListLiteral;
import org.simantics.scl.compiler.elaboration.expressions.ELiteral;
import org.simantics.scl.compiler.elaboration.expressions.EVar;
import org.simantics.scl.compiler.elaboration.expressions.Expression;
import org.simantics.scl.compiler.elaboration.expressions.Variable;
import org.simantics.scl.compiler.elaboration.fundeps.Fundep;
import org.simantics.scl.compiler.elaboration.java.JavaMethodDeclaration;
import org.simantics.scl.compiler.elaboration.macros.StandardMacroRule;
import org.simantics.scl.compiler.elaboration.modules.InlineProperty;
import org.simantics.scl.compiler.elaboration.modules.MethodImplementation;
import org.simantics.scl.compiler.elaboration.modules.PrivateProperty;
import org.simantics.scl.compiler.elaboration.modules.SCLValue;
import org.simantics.scl.compiler.elaboration.modules.TypeAlias;
import org.simantics.scl.compiler.elaboration.modules.TypeClass;
import org.simantics.scl.compiler.elaboration.modules.TypeClassInstance;
import org.simantics.scl.compiler.elaboration.modules.TypeClassMethod;
import org.simantics.scl.compiler.elaboration.query.Query;
import org.simantics.scl.compiler.elaboration.query.pre.QPreGuard;
import org.simantics.scl.compiler.elaboration.relations.ConcreteRelation;
import org.simantics.scl.compiler.elaboration.rules.MappingRelation;
import org.simantics.scl.compiler.elaboration.rules.SectionName;
import org.simantics.scl.compiler.elaboration.rules.TransformationRule;
import org.simantics.scl.compiler.environment.AmbiguousNameException;
import org.simantics.scl.compiler.environment.Environment;
import org.simantics.scl.compiler.environment.EnvironmentFactory;
import org.simantics.scl.compiler.environment.Environments;
import org.simantics.scl.compiler.errors.ErrorLog;
import org.simantics.scl.compiler.errors.Locations;
import org.simantics.scl.compiler.internal.codegen.effects.EffectConstructor;
import org.simantics.scl.compiler.internal.codegen.effects.ThreadLocalVariable;
import org.simantics.scl.compiler.internal.codegen.types.JavaReferenceValidator;
import org.simantics.scl.compiler.internal.codegen.types.JavaTypeTranslator;
import org.simantics.scl.compiler.internal.codegen.types.StandardTypeConstructor;
import org.simantics.scl.compiler.internal.codegen.utils.Constants;
import org.simantics.scl.compiler.internal.codegen.utils.JavaNamingPolicy;
import org.simantics.scl.compiler.internal.codegen.utils.MethodBuilderBase;
import org.simantics.scl.compiler.internal.deriving.InstanceDeriver;
import org.simantics.scl.compiler.internal.deriving.InstanceDerivers;
import org.simantics.scl.compiler.internal.elaboration.profiling.BranchPointInjector;
import org.simantics.scl.compiler.internal.elaboration.utils.StronglyConnectedComponents;
import org.simantics.scl.compiler.internal.parsing.declarations.ConstructorAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DAnnotationAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DClassAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DDataAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DDerivingInstanceAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DEffectAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DFixityAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DInstanceAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DMappingRelationAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DRelationAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DRuleAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DTypeAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DValueAst;
import org.simantics.scl.compiler.internal.parsing.declarations.DValueTypeAst;
import org.simantics.scl.compiler.internal.parsing.exceptions.SCLSyntaxErrorException;
import org.simantics.scl.compiler.internal.parsing.translation.ProcessedDClassAst;
import org.simantics.scl.compiler.internal.parsing.translation.ProcessedDInstanceAst;
import org.simantics.scl.compiler.internal.parsing.translation.RelationRepository;
import org.simantics.scl.compiler.internal.parsing.translation.ValueRepository;
import org.simantics.scl.compiler.internal.parsing.types.TypeAst;
import org.simantics.scl.compiler.module.ConcreteModule;
import org.simantics.scl.compiler.module.ImportDeclaration;
import org.simantics.scl.compiler.module.repository.ImportFailure;
import org.simantics.scl.compiler.module.repository.ImportFailureException;
import org.simantics.scl.compiler.types.TCon;
import org.simantics.scl.compiler.types.TForAll;
import org.simantics.scl.compiler.types.TFun;
import org.simantics.scl.compiler.types.TPred;
import org.simantics.scl.compiler.types.TVar;
import org.simantics.scl.compiler.types.Type;
import org.simantics.scl.compiler.types.Types;
import org.simantics.scl.compiler.types.kinds.Kind;
import org.simantics.scl.compiler.types.kinds.Kinds;
import org.simantics.scl.compiler.types.util.MultiFunction;
import org.simantics.scl.runtime.profiling.BranchPoint;

import gnu.trove.list.array.TIntArrayList;
import gnu.trove.map.hash.THashMap;
import gnu.trove.map.hash.TObjectIntHashMap;
import gnu.trove.procedure.TObjectObjectProcedure;
import gnu.trove.set.hash.THashSet;
import gnu.trove.set.hash.TIntHashSet;

public class Elaboration {
    // inputs
    ErrorLog errorLog;
    String moduleName;
    ArrayList<ImportDeclaration> importsAst;
    JavaReferenceValidator<Object, Object, Object, Object> javaReferenceValidator;
    ValueRepository valueDefinitionsAst;
    RelationRepository relationDefinitionsAst;

    // creates
    ConcreteModule module;
    Environment importedEnvironment;
    Environment environment;
    JavaNamingPolicy namingPolicy;
    ArrayList<SupplementedValueType> supplementedTypeAnnotations = new ArrayList<SupplementedValueType>();
    
    JavaTypeTranslator javaTypeTranslator;
    ArrayList<StandardTypeConstructor> dataTypes = new ArrayList<StandardTypeConstructor>();
    THashMap<String, ClassRef> classRefs = new THashMap<String, ClassRef>();
    THashMap<String, BranchPoint[]> branchPoints; 
    
    @SuppressWarnings("unchecked")
    public Elaboration(ErrorLog errorLog, CompilationTimer timer, EnvironmentFactory localEnvironmentFactory,
            String moduleName, ArrayList<ImportDeclaration> importsAst,
            JavaReferenceValidator<?, ?, ?, ?> javaReferenceValidator,
            ValueRepository valueDefinitionsAst,
            RelationRepository relationDefinitionsAst) {
        this.errorLog = errorLog;
        this.moduleName = moduleName;
        importsAst = processRelativeImports(importsAst);
        this.importsAst = importsAst;
        this.javaReferenceValidator = (JavaReferenceValidator<Object, Object, Object, Object>)javaReferenceValidator;
        this.valueDefinitionsAst = valueDefinitionsAst;
        this.relationDefinitionsAst = relationDefinitionsAst;

        module = new ConcreteModule(moduleName);
        try {
            if(timer != null)
                timer.suspendTimer();
            importedEnvironment = localEnvironmentFactory.createEnvironment(
                    importsAst.toArray(new ImportDeclaration[importsAst.size()]));
            if(timer != null)
                timer.continueTimer();
            this.environment = new EnvironmentOfModule(importedEnvironment, module);
        } catch (ImportFailureException e) {
            for(ImportFailure failure : e.failures)
                errorLog.log(failure.location, failure.toString());
            return;
        }
        for(ImportDeclaration importAst : importsAst)
            this.module.addDependency(new ImportDeclaration(
                    importAst.moduleName,
                    importAst.reexport ? importAst.localName : null,
                    false,
                    importAst.spec));
        localEnvironmentFactory.addBuiltinDependencies(module);
        namingPolicy = new JavaNamingPolicy(moduleName);
    }
    
    private ArrayList<ImportDeclaration> processRelativeImports(ArrayList<ImportDeclaration> relativeImports) {
        ArrayList<ImportDeclaration> absoluteImports = new ArrayList<ImportDeclaration>(relativeImports.size());
        for(ImportDeclaration relativeImport : relativeImports) {
            if(relativeImport.moduleName.startsWith(".")) {
                String absoluteModuleName = convertRelativeModulePath(relativeImport.location, relativeImport.moduleName);
                if(absoluteModuleName != null) {
                    ImportDeclaration absoluteImport = new ImportDeclaration(
                            absoluteModuleName, relativeImport.localName,
                            relativeImport.reexport, relativeImport.spec);
                    absoluteImport.location = relativeImport.location;
                    absoluteImports.add(absoluteImport);
                }
            }
            else
                absoluteImports.add(relativeImport);
        }
        return absoluteImports;
    }

    private String convertRelativeModulePath(long location, String relativeModuleName) {
        String originalRelativeModuleName = relativeModuleName;
        int p = moduleName.lastIndexOf('/');
        String parentPackage = p < 0 ? "" : moduleName.substring(0, p);
        while(relativeModuleName.startsWith(".")) {
            if(relativeModuleName.startsWith("./")) {
                relativeModuleName = relativeModuleName.substring(2);
            }
            else if(relativeModuleName.startsWith("../")) {
                relativeModuleName = relativeModuleName.substring(3);
                if(parentPackage.isEmpty()) {
                    errorLog.log(location, "Couldn't resolve the relative module name " + originalRelativeModuleName + " when the current module name is " + moduleName + ".");
                    return null;
                }
                p = parentPackage.lastIndexOf('/');
                parentPackage = p < 0 ? "" : parentPackage.substring(0, p);
            }
            else {
                errorLog.log(location, "Couldn't resolve the relative module name " + originalRelativeModuleName + ". It has an invalid syntax.");
                return null;
            }
        }
        return parentPackage + "/" + relativeModuleName;
    }

    public void addTypesToEnvironment(
            ArrayList<DDataAst> dataTypesAst,
            ArrayList<DTypeAst> typeAliasesAst,
            ArrayList<DEffectAst> effectsAst) {
        for(DDataAst dataType : dataTypesAst) {
            dataType.parameterKinds = new Kind[dataType.parameters.length];
            Kind constructorKind = Kinds.STAR;
            for(int i=dataType.parameters.length-1;i>=0;--i) {
                Kind kind = Kinds.metaVar();
                dataType.parameterKinds[i] = kind;
                constructorKind = Kinds.arrow(kind, constructorKind);
            }
            
            StandardTypeConstructor typeConstructor = new StandardTypeConstructor(
                    Types.con(moduleName, dataType.name), constructorKind);

            NameExistenceChecks.checkIfTypeExists(errorLog,
                    dataType.location, importedEnvironment, dataType.name);
            if(module.addTypeConstructor(dataType.name, typeConstructor))
                errorLog.log(dataType.location, "Type "+dataType.name+" has already been defined in this module.");
            dataType.typeConstructor = typeConstructor;
        }
        
        for(DTypeAst typeAlias : typeAliasesAst) {
            TypeAlias alias = new TypeAlias(Types.con(moduleName, typeAlias.name), typeAlias.parameters.length);
            NameExistenceChecks.checkIfTypeExists(errorLog,
                    typeAlias.location, importedEnvironment, typeAlias.name);
            if(module.addTypeAlias(typeAlias.name, alias)) {
                errorLog.log(typeAlias.location, "Type alias "+typeAlias.name+" has already been defined in this module.");
            }
        }
        
        for(DEffectAst effect : effectsAst) {
            EffectConstructor effectConstructor = new EffectConstructor(Types.con(moduleName, effect.name));
            effectConstructor.addThreadLocalVariable(
                    new ThreadLocalVariable(
                            effect.variableName,
                            TypeDesc.forClass(effect.threadLocalType)
                            ));
            if(module.addEffectConstructor(effect.name, effectConstructor))
                errorLog.log(effect.location, "Type "+effect.name+" has already been defined in this module.");
        }     
        javaTypeTranslator = new JavaTypeTranslator(environment);
    }
    
    private static final int[] EMPTY_INT_ARRAY = new int[0];
    
    public void processTypeAliases(ArrayList<DTypeAst> typeAliasesAst) {
        TObjectIntHashMap<String> typeAliasMap = new TObjectIntHashMap<String>();
        for(int i=0;i<typeAliasesAst.size();++i)
            typeAliasMap.put(typeAliasesAst.get(i).name, i); 
        TIntHashSet tempIntSet = new TIntHashSet();
        ArrayList<DTypeAst> orderedTypeAliases = new ArrayList<DTypeAst>(typeAliasesAst.size()); 
        //for(int i=0;i<typeAliasesAst.size();++i)
        //    System.out.println(i + "# " + typeAliasesAst.get(i).name);
        new StronglyConnectedComponents(typeAliasesAst.size()) {
            @Override
            protected int[] findDependencies(int u) {
                typeAliasesAst.get(u).type.collectReferences(typeAliasMap, tempIntSet);
                if(tempIntSet.isEmpty())
                    return EMPTY_INT_ARRAY;
                if(tempIntSet.contains(u)) {
                    errorLog.log(typeAliasesAst.get(u).location, "Type alias has a self reference.");
                    tempIntSet.remove(u);
                }
                int[] result = tempIntSet.toArray();
                tempIntSet.clear();
                //System.out.println(u + " -> " + Arrays.toString(result));
                return result; 
            }
            @Override
            protected void reportComponent(int[] component) {
                //System.out.println("component: " + Arrays.toString(component));
                if(component.length > 1) {
                    StringBuilder b = new StringBuilder();
                    b.append("Recursively defined type alias (");
                    long minLocation = typeAliasesAst.get(component[0]).location;
                    boolean first = true;
                    for(int u : component) {
                        DTypeAst typeAlias = typeAliasesAst.get(u);
                        if(first)
                            first = false;
                        else
                            b.append(", ");
                        b.append(typeAlias.name);
                        if(Locations.beginOf(typeAlias.location) < Locations.beginOf(minLocation))
                            minLocation = typeAlias.location;
                    }
                    b.append(").");
                    errorLog.log(minLocation, b.toString());
                }
                else
                    orderedTypeAliases.add(typeAliasesAst.get(component[0]));
            }
        }.findComponents();
        
        if(errorLog.isEmpty()) {
            for(DTypeAst typeAlias : orderedTypeAliases) {
                TypeAlias alias = module.getTypeAlias(typeAlias.name);
                TypeTranslationContext context = createTypeTranslationContext();
                for(int i=0;i<typeAlias.parameters.length;++i)
                    context.pushTypeVar(typeAlias.parameters[i]);
                alias.body = typeAlias.type.toType(context, Kinds.metaVar());
                for(int i=0;i<typeAlias.parameters.length;++i)
                    alias.parameters[i] = context.popTypeVar(typeAlias.parameters[i], null);
            }
        }
    }
    
    public void processDataTypes(ArrayList<DDataAst> dataTypesAst) {
        for(DDataAst dataTypeAst : dataTypesAst) {
            TypeTranslationContext context = createTypeTranslationContext();
            TVar[] typeParameters = new TVar[dataTypeAst.parameters.length];
            for(int i=0;i<dataTypeAst.parameters.length;++i)
                typeParameters[i] = context.addTypeVar(dataTypeAst.parameters[i]);
            Constructor[] constructors = new Constructor[dataTypeAst.constructors.length];
            String className = null;
            boolean external = false;
            for(DAnnotationAst annotation : dataTypeAst.getAnnotations()) {
                if(annotation.id.text.equals("@JavaType")) {
                    if(annotation.parameters.length != 1 || 
                            !(annotation.parameters[0] instanceof ELiteral) ||
                            !(((ELiteral)annotation.parameters[0]).getValue() instanceof StringConstant))
                        errorLog.log(annotation.location, "Invalid parameters. Expected @JavaType \"className\".");
                    else {
                        className = ((StringConstant)((ELiteral)annotation.parameters[0]).getValue()).getValue().replace('.', '/');
                        external = true;                        
                        break;
                    }
                }
            }
            
            boolean trivialDataType = dataTypeAst.constructors.length == 1 &&
                    dataTypeAst.constructors[0].parameters.length == 1;
            if(className == null && !trivialDataType)
                className = namingPolicy.getDataTypeClassName(dataTypeAst.name);
            
            StandardTypeConstructor dataType = dataTypeAst.typeConstructor;
            
            dataType.setType(Types.con(moduleName, dataTypeAst.name), typeParameters);
            dataType.setConstructors(constructors);
            if(!trivialDataType)
                dataType.setTypeDesc(TypeDesc.forClass(className));            
            if(!external || dataTypeAst.constructors.length > 0) {
                dataType.isOpen = false;
            }
            dataType.external = external;
            dataTypes.add(dataType);
            for(int j=0;j<constructors.length;++j) {
                ConstructorAst constructor = dataTypeAst.constructors[j];
                String name = constructor.name;
                Type[] parameterTypes = new Type[constructor.parameters.length];
                for(int i=constructor.parameters.length-1;i>=0;--i)
                    parameterTypes[i] = context.toType(constructor.parameters[i]);
                String javaName = constructors.length == 1 ? className 
                        : namingPolicy.getConstructorClassName(name);
                String[] fieldNames = null;
                for(DAnnotationAst annotation : constructor.annotations)
                    if(annotation.id.text.equals("@JavaType")) {
                        try {
                            javaName = ((StringConstant)((ELiteral)annotation.parameters[0])
                                    .getValue()).getValue();
                        } catch(Exception e) {
                            errorLog.log(annotation.parameters[0].location, "Invalid annotation parameter.");
                        }
                    }
                    else if(annotation.id.text.equals("@FieldNames")) {
                        try {
                            EListLiteral literal = (EListLiteral)annotation.parameters[0];
                            fieldNames = new String[literal.getComponents().length];
                            for(int i=0;i<fieldNames.length;++i) {
                                Expression component = literal.getComponents()[i];
                                if(component instanceof EVar)
                                    fieldNames[i] = ((EVar)component).name;
                                else if(component instanceof ELiteral)
                                    fieldNames[i] = ((StringConstant)((ELiteral)component).getValue()).getValue();
                            }
                        } catch(Exception e) {
                            errorLog.log(annotation.parameters[0].location, "Invalid annotation parameter.");
                            fieldNames = null;
                        }
                    }   
                
                constructors[j] = new Constructor(constructor.location, dataType,
                        Name.create(moduleName, name), 
                        parameterTypes, javaName);
                constructors[j].fieldNames = fieldNames;
                constructors[j].recordFieldNames = constructor.fieldNames;
            }
        }
    }
    
    public void processTypeClasses(ArrayList<ProcessedDClassAst> typeClassesAst) {
        for(ProcessedDClassAst pClassAst : typeClassesAst) {
            DClassAst classAst = pClassAst.orig;
            
            if(module.getTypeClass(classAst.name) != null) {
                errorLog.log(classAst.location, "Class "+classAst.name+" has already been defined in this module.");
                continue;
            }
            
            TypeTranslationContext context = createTypeTranslationContext();            
            
            TPred[] classContext = new TPred[classAst.context.length];
            for(int i=0;i<classContext.length;++i)
                classContext[i] = context.toTFuncApply(classAst.context[i]);
            
            TVar[] parameters = new TVar[classAst.parameters.length];
            
            if(classAst.name.equals("Functor") || classAst.name.equals("Monad")) {
                // FIXME hack
                parameters[0] = context.resolveTypeVariable(pClassAst.orig.location, classAst.parameters[0], Kinds.STAR_TO_STAR);
            }
            else {
                for(int i=0;i<parameters.length;++i)
                    parameters[i] = context.resolveTypeVariable(pClassAst.orig.location, classAst.parameters[i], Kinds.metaVar());
            }
                        
            TCon con = Types.con(moduleName, classAst.name);
            TypeClass typeClass = new TypeClass(classAst.location, 
                    classContext, 
                    con, 
                    namingPolicy.getTypeClassInterfaceName(con),
                    parameters,
                    Fundep.mapFundeps(classAst.parameters, classAst.fundeps));
            
            THashMap<String, TypeClassMethod> methods = typeClass.methods;
            for(DValueTypeAst methodDecl : pClassAst.typeDeclarations) {
                try {
                    Type type;
                    try {
                        type = context.toType(methodDecl.type);
                    } catch(SCLSyntaxErrorException e) {
                        errorLog.log(e.location, e.getMessage());
                        continue;
                    }
                    for(EVar name : methodDecl.names) {
                        typeClass.methodNames.add(name.name);
                        methods.put(name.name,
                                new TypeClassMethod(typeClass, name.name, 
                                        namingPolicy.getMethodName(name.name),
                                        type, Types.getArity(type),
                                        name.location)
                                );
                    }
                } catch(RuntimeException e) {
                    errorLog.setExceptionPosition(methodDecl.location);
                    throw e;
                }
            }
            
            for(String methodName : pClassAst.defaultImplementations.getValueNames()) {
                String fullName = "_" + classAst.name + "_default_" + methodName;                
                ArrayList<DValueAst> defs = pClassAst.defaultImplementations.getDefinition(methodName);
                
                TypeClassMethod method = typeClass.methods.get(methodName);
                if(method == null) {
                    errorLog.log(defs.get(0).location, "Method " + methodName + " is not defined in this class.");
                    continue;
                }
                method.setDefaultImplementation(Name.create(moduleName, fullName));
                
                valueDefinitionsAst.addDefinitions(fullName, defs);
                /*valueDefinitionsAst.addAnnotation(fullName, new DAnnotationAst(new EVar("@private"), 
                        Collections.<Expression>emptyList()));*/
                supplementedTypeAnnotations.add(new SupplementedValueType(defs.get(0).location, fullName, method.getType()));                
            }
            
            module.addTypeClass(classAst.name, typeClass);
        }
    }

    private TypeTranslationContext createTypeTranslationContext() {
        return new TypeTranslationContext(errorLog, environment);
    }
    
    public void processDerivingInstances(ArrayList<DDerivingInstanceAst> derivingInstancesAst,
            ArrayList<ProcessedDInstanceAst> instancesAst) {
        for(DDerivingInstanceAst derivingInstance : derivingInstancesAst) {
            String name = derivingInstance.name.name;
            TCon con;
            try {
                con = Environments.getTypeClassName(environment, name);
            } catch (AmbiguousNameException e) {
                errorLog.log(derivingInstance.name.location, e.getMessage());
                continue;
            }
            if(con == null) {
                errorLog.log(derivingInstance.name.location, "Couldn't resolve class " + name + ".");
                continue;
            }
            InstanceDeriver deriver = InstanceDerivers.get(con);
            if(deriver == null)
                errorLog.log(derivingInstance.location, "Doesn't know how to derive " + name + ".");
            else
                deriver.derive(errorLog, environment, instancesAst, derivingInstance);
        }
    }
    
    public void processInstances(ArrayList<ProcessedDInstanceAst> instancesAst) {
        THashSet<TPred> instanceClashCheckSet = new THashSet<TPred>(); 
        for(ProcessedDInstanceAst pInstanceAst : instancesAst) {
            DInstanceAst instanceAst = pInstanceAst.orig;
            try {
                TypeTranslationContext context = createTypeTranslationContext();
                
                String name = instanceAst.name.name;
                TCon typeClassCon;
                try {
                    typeClassCon = Environments.getTypeClassName(environment, name);
                } catch (AmbiguousNameException e) {
                    errorLog.log(instanceAst.name.location, e.getMessage());
                    continue;
                }
                if(typeClassCon == null) {
                    errorLog.log(instanceAst.name.location, "Couldn't resolve class " + name + ".");
                    continue;
                }
                TypeClass typeClass = environment.getTypeClass(typeClassCon);
                pInstanceAst.typeClass = typeClass;
                
                if(instanceAst.types.length != typeClass.parameters.length) {
                    errorLog.log(instanceAst.location, "Wrong number of parameters to type class " + typeClassCon.name + ".");
                    continue;
                }
                Type[] parameters = new Type[instanceAst.types.length];
                for(int i=0;i<parameters.length;++i)
                    parameters[i] = context.toType(instanceAst.types[i], typeClass.parameters[i].getKind() /* FIXME */);
                TPred instance = Types.pred(typeClassCon, parameters);
                
                if(!instanceClashCheckSet.add(instance)) {
                    errorLog.log(instanceAst.location, "Duplicate definition of the instance " + instance + ".");
                    continue;
                }
                
                TPred[] instanceContext = new TPred[instanceAst.context.length];
                for(int i=0;i<instanceContext.length;++i)
                    instanceContext[i] = context.toTFuncApply(instanceAst.context[i]);
                
                String javaName = namingPolicy.getInstanceClassName(instance);
                String instancePrefix = instance.toName() + "$";
    
                ValueRepository valueDefs = pInstanceAst.valueDefs;
    
                THashMap<String, MethodImplementation> methodImplementations =
                        new THashMap<String, MethodImplementation>();
                for(String valueName : valueDefs.getValueNames()) {
                    String fullName = instancePrefix + valueName;
                    long loc = valueDefs.getDefinition(valueName).get(0).location;
                    valueDefinitionsAst.addFrom(valueDefs, valueName, fullName);
                    /*valueDefinitionsAst.addAnnotation(fullName, new DAnnotationAst(new EVar("@private"), 
                            Collections.<Expression>emptyList()));*/
                    TypeClassMethod method = typeClass.methods.get(valueName);
                    if(method == null) {
                        errorLog.log(loc, "Method " + valueName + " is not defined in the type class " + typeClass.name.name + ".");
                        continue;
                    }
                    Type type = method.getBaseType().replace(typeClass.parameters, parameters);
                    for(int i=instanceContext.length-1;i>=0;--i)
                        type = Types.constrained(instanceContext[i], type);
                    //System.out.println(valueName + " :: " + type);
                    supplementedTypeAnnotations.add(
                            new SupplementedValueType(loc, fullName, type));
                    methodImplementations.put(valueName,
                            new MethodImplementation(Name.create(moduleName, fullName), false));
                }
                
                // Are all necessary methods defined
                for(String methodName : typeClass.methods.keySet())
                    if(!methodImplementations.containsKey(methodName)) {
                        Name defaultImplementation = typeClass.methods.get(methodName).getDefaultImplementation();
                        if(defaultImplementation == null)
                            errorLog.log(instanceAst.location, "Method " + methodName + " is not defined.");
                        else
                            methodImplementations.put(methodName, 
                                    new MethodImplementation(defaultImplementation, true));
                    }
                
                JavaTypeInstanceConstructor generator = new JavaTypeInstanceConstructor(javaName, instance, instanceContext);
                if(instanceContext.length == 0)
                    generator.setHasStaticInstance(true);
                
                TypeClassInstance typeClassInstance = 
                        new TypeClassInstance(instanceAst.location, typeClass, generator,
                                generator.getTypeParameters(),
                                instanceContext, instance, methodImplementations,
                                javaName);
                
                generator.setInstance(typeClassInstance);
                
                module.addTypeClassInstance(typeClassCon, typeClassInstance);
            } catch(RuntimeException e) {
                errorLog.setExceptionPosition(instanceAst.location);
                throw e;
            }
        }
        
        // Generate superclass functions
        for(ArrayList<TypeClassInstance> instanceArray : module.getTypeInstances().values())
            for(TypeClassInstance instance : instanceArray) {
                try {
                    TypeClass typeClass = instance.typeClass;
                    int superCount = typeClass.context.length;
                    
                    instance.superExpressions = new SCLValue[superCount];
                    for(int i=0;i<superCount;++i) {
                        TPred type = (TPred)typeClass.context[i]
                                .replace(typeClass.parameters, instance.instance.parameters);
                        SCLValue value = new SCLValue(Name.create(moduleName, 
                                instance.javaName.substring(instance.javaName.indexOf('$')+1) + "_super" + i));
                        //value.addProperty(PrivateProperty.INSTANCE);
                        module.addValue(value);
                        Expression expression = new EGetConstraint(instance.location, type);
                        value.setExpression(expression);
                        value.setType(Types.forAll(instance.generatorParameters, Types.constrained(instance.context, type)));
                        //TypeUnparsingContext tuc = new TypeUnparsingContext();
                        // TODO error handling
                        instance.superExpressions[i] = value;
                    }
                } catch(RuntimeException e) {
                    errorLog.setExceptionPosition(instance.getLocation());
                    throw e;
                }
            }
    }
    
    public void processJavaMethods(ArrayList<JavaMethodDeclaration> javaMethodDeclarations) {
        for(JavaMethodDeclaration javaMethod : javaMethodDeclarations) {
            String name = javaMethod.methodName.name;
            String javaName = name;
            ArrayList<DAnnotationAst> annotations = 
                    valueDefinitionsAst.getAnnotations(name);
            boolean isPrivate = false;
            if(annotations != null) {
                for(DAnnotationAst annotation : annotations)
                    if(annotation.id.text.equals("@JavaName")) {
                        Expression p0 = annotation.parameters[0];
                        if(p0 instanceof EVar)
                            javaName = ((EVar)p0).name;
                        else if(p0 instanceof ELiteral) {
                            ELiteral lit = (ELiteral)p0;
                            javaName = ((StringConstant)lit.getValue()).getValue();
                        }
                    }
                    else if(annotation.id.text.equals("@private")) {
                        isPrivate = true;
                    }
            }
            
            Type type = createTypeTranslationContext().toType(javaMethod.type);

            CallJava callJava = resolveMethod(
                    javaMethod.location,
                    javaMethod.className,
                    javaName,
                    type);
            if(callJava != null) {
                NameExistenceChecks.checkIfValueExists(errorLog, javaMethod.location,
                        importedEnvironment, name);
                SCLValue value = module.addValue(name, callJava);
                value.definitionLocation = javaMethod.methodName.location;
                if(isPrivate)
                    value.addProperty(PrivateProperty.INSTANCE);
            }
        }
    }
    
    /**
     * Convert a java class method into a {@link CallJava} instance.
     * Compilation errors are logged for failures in finding the named class or in accessing the method.
     * The return value for errors is {@code null}.
     * 
     * @param loc  SCL source location
     * @param className  Name of the class
     * @param methodName  Name of the method
     * @param type  The expected SCL type of the method 
     * @return  A new JavaCall instance, or null if the given method can not be instantiated.
     */
    private CallJava resolveMethod(long loc,
            String className, String methodName, Type type) {
        // Resolve class
        ClassRef classRef = classRefs.get(className);
        if(classRef == null) {
            if(classRefs.containsKey(className))
                return null;
            classRef = javaReferenceValidator.getClassRef(className);
            classRefs.put(className, classRef);
            if(classRef == null) {
                errorLog.log(loc, "Didn't find class " + className + ".");
                return null;
            }
            if(!javaReferenceValidator.isPublic(classRef.getClass())) {
                errorLog.log(loc, "Class " + className + " is not public.");
                return null;
            }
            
        }
        
        // Resolve method
        List<MethodRef> methodRefs = classRef.getMethodRefs(methodName);
        if(methodRefs.isEmpty()) {
            errorLog.log(loc, "Didn't find any public method or field with name '" + methodName + "' from class " + className + ".");
            return null;
        }
        
        ArrayList<CallJava> candidates = new ArrayList<CallJava>(2); 
        for(MethodRef methodRef : methodRefs) {
            CallJava candidate = matchType(methodRef, type);
            if(candidate != null)
                candidates.add(candidate);
        }

        if(candidates.isEmpty()) {
            StringBuilder b = new StringBuilder();
            b.append("Didn't find any public method or field matching the type " + type + ". The following methods and fields were tried:");
            for(MethodRef methodRef : methodRefs) {
                b.append("\n    ");
                b.append(methodRef);
            }
            b.append("\nbut expected something like:");
            {
                MultiFunction mFun = Types.matchFunction(type);
                b.append("\n    public static ");
                b.append(javaTypeTranslator.toTypeDesc(mFun.returnType).getFullName()).append(' ').append(methodName).append('(');
                boolean first = true;
                for(Type parameter : mFun.parameterTypes) {
                    if(first)
                        first = false;
                    else
                        b.append(", ");
                    b.append(javaTypeTranslator.toTypeDesc(parameter).getFullName());
                }
                b.append(')');
            }
            errorLog.log(loc, b.toString());
            return null;
        }
        else if(candidates.size() == 1)
            return candidates.get(0);
        else {
            // Try to find the best match
            ArrayList<CallJava> bestCandidates = new ArrayList<CallJava>(candidates.size());
            loop: for(CallJava candidate : candidates) {
                Iterator<CallJava> it = bestCandidates.iterator();
                while(it.hasNext()) {
                    CallJava b = it.next();
                    switch(candidate.compareTo(javaReferenceValidator, b)) {
                    case CallJava.LESS:
                    case CallJava.EQUAL:
                        continue loop;
                    case CallJava.GREATER:
                        it.remove();
                        break;
                    case CallJava.INCOMPARABLE:
                        break;
                    }
                }
                bestCandidates.add(candidate);
            }
            
            if(bestCandidates.size() == 1) {
                // System.out.println("Choose: " + bestCandidates.get(0).getMethodRef());
                return bestCandidates.get(0);
            }
            else { 
                StringBuilder b = new StringBuilder();
                b.append("Found more than one incomparable public methods the type " + type + ":");
                for(CallJava callJava : bestCandidates) {
                    b.append("\n    ");
                    b.append(callJava.getMethodRef());
                }
                errorLog.log(loc, b.toString());
                return null;
            }
        }
    }

    private CallJava matchType(MethodRef methodRef, Type type) {
        //System.out.println("-----------------------------------------------------");
        //System.out.println("method: " + methodRef);
        //System.out.println("type: " + type);

        type = Types.canonical(type);
        while(type instanceof TForAll)
            type = Types.canonical(((TForAll)type).type);
            
        TypeDesc[] expectedParameterTypes = methodRef.getParameterTypes();
        
        ArrayList<Type> parameterTypes = new ArrayList<Type>();
        Type effect = Types.NO_EFFECTS;
        Type returnType = type;
        
        StackItem[] stackItems = new StackItem[expectedParameterTypes.length];
        TIntArrayList unresolvedItems = new TIntArrayList();
        
        loop:
        for(int i=0;i<expectedParameterTypes.length;++i) {
            Type parameterType;
            TypeDesc providedParameterType;
            do {
                if(effect != Types.NO_EFFECTS || !(returnType instanceof TFun)) {
                    while(i < expectedParameterTypes.length)
                        unresolvedItems.add(i++);
                    break loop;
                }
                TFun fun = (TFun)returnType;
                parameterType = Types.canonical(fun.domain);
                parameterTypes.add(parameterType);
                effect = Types.canonical(fun.effect);
                returnType = Types.canonical(fun.range);
                providedParameterType = javaTypeTranslator.toTypeDesc(parameterType);
            } while(providedParameterType.equals(TypeDesc.VOID));
            
            while(true) {
                TypeDesc expectedParameterType = expectedParameterTypes[i];
                if(javaReferenceValidator.isAssignableFrom(expectedParameterType,
                        providedParameterType)) {
                    stackItems[i] = new ParameterStackItem(
                            parameterTypes.size()-1, 
                            parameterType);
                    break;
                }
                else
                    unresolvedItems.add(i++);
                if(i == expectedParameterTypes.length) {
                    parameterTypes.remove(parameterTypes.size()-1);
                    returnType = Types.functionE(parameterType, effect, returnType);
                    break;
                }
            } 
        }
        //System.out.println("returnType: " + returnType);
        if(!unresolvedItems.isEmpty()) {
            ArrayList<TCon> concreteEffects = new ArrayList<TCon>();
            effect.collectConcreteEffects(concreteEffects);
            
            for(TCon eff : concreteEffects) {
                EffectConstructor effC = environment.getEffectConstructor(eff);
                for(ThreadLocalVariable var : effC.getThreadLocalVariables()) {
                    for(int i=0;i<unresolvedItems.size();++i) {
                        int id = unresolvedItems.get(i);
                        if(!expectedParameterTypes[id].equals(TypeDesc.OBJECT) &&
                                javaReferenceValidator.isAssignableFrom(expectedParameterTypes[id], var.type)) {
                            stackItems[id] = new ThreadLocalStackItem(var.variableName, var.type);
                            unresolvedItems.removeAt(i);
                            --i;
                        }
                    }
                }
            }
            
            if(!unresolvedItems.isEmpty())
                return null;
            /*System.out.print("Unresolved: ");
            boolean first = true;
            for(int i=0;i<unresolvedItems.size();++i) {
                if(first)
                    first = false;
                else
                    System.out.print(", ");
                System.out.print(expectedParameterTypes[unresolvedItems.get(i)]);
            }
            System.out.println();*/            
        }   
        OutputFilter filter = null;
        {
            TypeDesc providedReturnType = methodRef.getReturnType();
            if(!providedReturnType.equals(Constants.FUNCTION)) {
                while(returnType instanceof TFun && effect == Types.NO_EFFECTS) {
                    TFun fun = (TFun)returnType;
                    Type parameterType = Types.canonical(fun.domain);
                    if(!javaTypeTranslator.toTypeDesc(parameterType).equals(TypeDesc.VOID))
                        return null;                    
                    parameterTypes.add(parameterType);
                    effect = Types.canonical(fun.effect);
                    returnType = Types.canonical(fun.range);
                }
            }
            TypeDesc expectedReturnType = 
                    javaTypeTranslator.toTypeDesc(returnType);
            if(!javaReferenceValidator.isAssignableFrom(expectedReturnType,
                    providedReturnType)) {
                if(expectedReturnType.equals(TypeDesc.VOID))
                    filter = PopOutputFilter.INSTANCE;
                else if(expectedReturnType.equals(Constants.LIST)
                        && providedReturnType.equals(Constants.COLLECTION))
                    filter = ConvertToListFilter.INSTANCE;
                else
                    return null;
            }
        }
        
        CallJava result = new CallJava(
                Types.freeVarsArray(type),
                effect,
                returnType,
                parameterTypes.toArray(new Type[parameterTypes.size()]),
                stackItems, 
                methodRef,
                filter);
        //System.out.println(result.getType());
        return result;
    }

    public void processMappingRelations(ArrayList<DMappingRelationAst> mappingRelationsAst) {
        for(DMappingRelationAst mappingRelation : mappingRelationsAst) {
            TypeAst[] parameterTypesAst = mappingRelation.parameterTypes;
            Type[] parameterTypes = new Type[parameterTypesAst.length];
            TypeTranslationContext typeTranslationContext = createTypeTranslationContext();
            for(int i=0;i<parameterTypes.length;++i)
                parameterTypes[i] = parameterTypesAst[i].toType(typeTranslationContext, Kinds.STAR);
            MappingRelation mRel = 
                    new MappingRelation(Name.create(moduleName, mappingRelation.name), parameterTypes);
            mRel.location = mappingRelation.location;
            if(module.addMappingRelation(mRel))
                errorLog.log(mappingRelation.location, "Mapping relation " + mappingRelation.name + 
                        " has already been defined.");
        }
    }

    THashMap<String, DRuleAst> ruleAstMap = new THashMap<String, DRuleAst>();
    
    public void processRules(ArrayList<DRuleAst> rulesAst) {
        // Find implied mapping relations
        for(DRuleAst ruleA : rulesAst) {
            ArrayList<Query> whereSection = ruleA.getSections().get("where");
            if(whereSection != null)
                for(Query query : whereSection) {
                    if(!(query instanceof QPreGuard))
                        continue;
                    QPreGuard guard = (QPreGuard)query;
                    if(!(guard.guard instanceof EApply))
                        continue;
                    EApply apply = (EApply)guard.guard;
                    if(!(apply.getFunction() instanceof EVar))
                        continue;

                    String name = ((EVar)apply.getFunction()).name;
                    if(module.getMappingRelation(name) != null)
                        continue;

                    int arity = apply.getParameters().length;
                    Type[] parameterTypes = new Type[arity];
                    for(int i=0;i<arity;++i)
                        parameterTypes[i] = Types.metaVar(Kinds.STAR);
                    MappingRelation mRel = 
                            new MappingRelation(Name.create(moduleName, name), parameterTypes);
                    mRel.location = query.location;
                    module.addMappingRelation(mRel);
                }
            if(ruleAstMap.put(ruleA.name, ruleA) != null)
                errorLog.log(ruleA.location, "Rule " + ruleA.name + 
                        " has already been defined.");
        }
        
        // 
        for(String ruleName : ruleAstMap.keySet())
            processRule(ruleName);
    }
    
    private TransformationRule processRule(String ruleName) {
        TransformationRule rule = module.getRule(ruleName);
        if(rule != null)
            return rule;
        
        DRuleAst ruleAst = ruleAstMap.get(ruleName);
        if(ruleAst.alreadyProcessing) {
            errorLog.log(ruleAst.location, "Cyclic chain of rule extensions.");
            return null;
        }
        
        TransformationRule[] extendsRules;
        int length = ruleAst.extendsNames.length;
        if(length == 0)
            extendsRules = TransformationRule.EMPTY_ARRAY;
        else {
            extendsRules = new TransformationRule[length];
            for(int i=0;i<length;++i) {
                try {
                    String extendsName = ruleAst.extendsNames[i];
                    TransformationRule extendsRule;
                    if(ruleAstMap.containsKey(extendsName))
                        extendsRule = processRule(extendsName);
                    else {
                        extendsRule = Environments.getRule(environment, extendsName);
                        if(extendsRule == null)
                            errorLog.log(ruleAst.location,
                                    "Couldn't resolve rule name " + extendsName + ".");
                    }
                    extendsRules[i] = extendsRule;
                } catch(AmbiguousNameException e) {
                    errorLog.log(ruleAst.location, e.getMessage());
                }
            }
        }
        
        final THashMap<SectionName, Query[]> sections = new THashMap<SectionName, Query[]>();

        final TranslationContext context = createTranslationContext();
        if(length > 0) {
            THashMap<String, Variable> variables = context.getVariables();
            for(TransformationRule extendsRule : extendsRules) {
                if(extendsRule == null)
                    continue;
                for(Variable var : extendsRule.variables)
                    if(variables.put(var.getName(), var) != null) {
                        errorLog.log(ruleAst.location, 
                                "Variable " + var.getName() + " is defined in more than one base rule, which is not currently allowed.");
                    }
            }
        }
        context.pushExistentialFrame();
        ruleAst.getSections().forEachEntry(new TObjectObjectProcedure<String, ArrayList<Query>>() {
            @Override
            public boolean execute(String sectionNameString, ArrayList<Query> queries) {
                Query[] resolvedQueries = new Query[queries.size()];
                for(int i=0;i<resolvedQueries.length;++i)
                    resolvedQueries[i] = queries.get(i).resolve(context);

                SectionName sectionName = SectionName.getSectionName(sectionNameString);
                if(sectionName == null)
                    context.getErrorLog().log(queries.get(0).location,
                            "Invalid section name " + sectionNameString + ".");
                else
                    sections.put(sectionName, resolvedQueries);
                return true;
            }
        });
        
        Variable[] variables = context.getVariables().values().toArray(new Variable[context.getVariables().size()]);

        rule = new TransformationRule(ruleAst.isAbstract,
                Name.create(moduleName, ruleAst.name),
                extendsRules,
                sections, variables);
        rule.location = ruleAst.location;
        module.addRule(rule);
        return rule;
    }

    public void addDataTypesToEnvironment() {
        for(StandardTypeConstructor dataType : dataTypes) {
            int constructorTag = 0;
            for(Constructor constructor : dataType.constructors) {
                SCLValue value = new SCLValue(constructor.name);
                SCLConstructor sclConstructor = 
                        new SCLConstructor(
                                constructor.name.name,
                                constructor.javaName, 
                                constructor.getTypeVariables(),
                                constructorTag++,
                                constructor.getReturnType(),
                                constructor.fieldNames == null 
                                        ? SCLConstructor.DEFAULT_FIELD_NAMES[constructor.getParameterTypes().length] 
                                        : constructor.fieldNames,
                                constructor.recordFieldNames,
                                constructor.getParameterTypes());
                if(dataType.constructors.length == 1 && (
                        dataType.getTypeDesc() == null ||
                        dataType.constructors[0].javaName.equals(MethodBuilderBase.getClassName(dataType.getTypeDesc()))))
                    sclConstructor.setOnlyConstructor(true);
                value.setValue(sclConstructor);
                value.setType(constructor.getType());
                
                NameExistenceChecks.checkIfValueExists(errorLog, constructor.loc,
                        importedEnvironment, constructor.name.name);
                if(module.addValue(value)) {
                    errorLog.log(constructor.loc,
                            "Value " + constructor.name.name + " is already defined.");
                }
            }
        }
    }
    
    public void addTypeClassesToEnvironment() {
        for(TypeClass typeClass : module.getTypeClasses()) {
            for(TypeClassMethod method : typeClass.methods.values()) {
                SCLValue value = method.createValue();
                value.definitionLocation = method.location;
                NameExistenceChecks.checkIfValueExists(errorLog, Locations.NO_LOCATION,
                        importedEnvironment, value.getName().name);

                if(module.addValue(value)) {
                    String name = method.getName();
                    long location = Locations.NO_LOCATION;
                    ArrayList<DValueAst> definitions = valueDefinitionsAst.getDefinition(name);
                    if(definitions != null && !definitions.isEmpty())
                        location = definitions.get(0).location;
                    errorLog.log(location, "Value " + name + " is already defined.");
                }
            }
        }
    }
    
    public void preprocessValueDefinitions(ArrayList<DValueTypeAst> typeAnnotationsAst) {
        for(String name : valueDefinitionsAst.getValueNames()) {
            SCLValue value = new SCLValue(Name.create(moduleName, name));
            
            long location = valueDefinitionsAst.getLocation(name);
            NameExistenceChecks.checkIfValueExists(errorLog, location,
                    importedEnvironment, value.getName().name);
            value.definitionLocation = location;
            if(module.addValue(value))
                errorLog.log(location, "Value " + name + " is already defined.");
        }
        for(DValueTypeAst valueTypeAst : typeAnnotationsAst)
            for(EVar name : valueTypeAst.names) {
                SCLValue value = module.getValue(name.name); 
                if(value == null) {
                    errorLog.log(valueTypeAst.location, name.name + " is not defined.");
                    value = new SCLValue(Name.create(moduleName, name.name));
                    module.addValue(value);
                }
                value.definitionLocation = name.location;
            }
        for(String name : relationDefinitionsAst.getRelationNames()) {
            ConcreteRelation relation = new ConcreteRelation(name);
            module.addRelation(name, relation);
        }
    }
    
    public void addValueDefinitionsToEnvironment(ArrayList<DValueTypeAst> typeAnnotationsAst) {
        THashMap<String, DValueTypeAst> typeMap = new THashMap<String, DValueTypeAst>();
        for(DValueTypeAst valueTypeAst : typeAnnotationsAst)
            for(EVar name : valueTypeAst.names) {
                if(typeMap.containsKey(name.name))
                    errorLog.log(valueTypeAst.location, "Type of "+name.name+" has already been declared in this module.");
                else
                    typeMap.put(name.name, valueTypeAst);
            }
        
        for(String name : valueDefinitionsAst.getValueNames()) {
            ArrayList<DValueAst> defs = valueDefinitionsAst.getDefinition(name);
            try {
                SCLValue value = module.getValue(name);
                TranslationContext context = createTranslationContext();
                Expression expression = context.translateCases2(defs);
                value.setExpression(expression);
                
                DValueTypeAst valueTypeAst = typeMap.remove(name);
                if(valueTypeAst != null)
                    value.setType(Types.closure(context.toType(valueTypeAst.type)));
                
                ArrayList<DAnnotationAst> annotations = valueDefinitionsAst.getAnnotations(name);
                if(annotations != null)
                    for(DAnnotationAst annotation : annotations) {
                        handleAnnotation(value, defs, annotation);
                    }
            } catch(RuntimeException e) {
                errorLog.setExceptionPosition(defs.get(0).location);
                throw e;
            }
        }
        for(String name : relationDefinitionsAst.getRelationNames()) {
            ArrayList<DRelationAst> definitions = relationDefinitionsAst.getDefinition(name);
            if(definitions.size() > 1) {
                errorLog.log(definitions.get(1).location,
                        "Does not yet support definition of relations by more than one rule.");
                continue;
            }
            
            DRelationAst definition = definitions.get(0);
            ConcreteRelation relation = (ConcreteRelation)module.getRelation(name);
            relation.location = definition.location;
            TranslationContext context = createTranslationContext();
            definition.translateTo(context, relation);
        }
    }
    
    private TranslationContext createTranslationContext() {
        return new TranslationContext(errorLog, environment, null);
    }
    
    private void handleAnnotation(SCLValue value, ArrayList<DValueAst> defs, DAnnotationAst annotation) {
        if(annotation.id.text.equals("@macro")) {
            value.setMacroRule(new StandardMacroRule());
        }
        else if(annotation.id.text.equals("@inline")) {
            try {
                int arity = defs.get(0).lhs.getFunctionDefinitionArity();
                int phaseMask = 0xffffffff;
                if(annotation.parameters.length > 0) {
                    phaseMask = Integer.parseInt(((EIntegerLiteral)annotation.parameters[0]).getValue());
                }
                value.addProperty(new InlineProperty(arity, phaseMask));
            } catch(NotPatternException e) {
                errorLog.log(annotation.location, "Inline annotation is invalid: this is not a function.");
            }
        }
        else if(annotation.id.text.equals("@private")) {
            value.addProperty(PrivateProperty.INSTANCE);
        }
        else if(annotation.id.text.equals("@deprecated")) {
            // TODO
        }
        else
            errorLog.log(annotation.location, "Unknown annotation.");
    }

    public void addSupplementedTypeAnnotationsToEnvironment() {
        for(SupplementedValueType valueType : supplementedTypeAnnotations) {
            Type type = Types.closure(valueType.type);
            String name = valueType.name;
            SCLValue value = module.getValue(name);
            if(value == null)
                errorLog.log(valueType.position,
                        name + " is not defined.");
            else if(value.getType()==null)
                value.setType(type);
            else
                errorLog.log(valueType.position, 
                        "Type of "+name+" has already been declared in this module.");
        }
    }
    
    public void addFixityToEnvironment(ArrayList<DFixityAst> fixityAst) {
        for(DFixityAst fixity : fixityAst) {
            for(EVar symbol : fixity.symbols) {
                String name = symbol.name;
                SCLValue value = module.getValue(name);
                if(value == null)
                    errorLog.log(symbol.location,
                            name + " is not defined.");
                else
                    value.setPrecedence(fixity.precedence);
            }
        }
    }

    public void addCoverageBranchPoints() {
        branchPoints = new THashMap<String, BranchPoint[]>();
        BranchPointInjector injector = new BranchPointInjector(); 
        for(String valueName : valueDefinitionsAst.getValueNames()) {
            for(DValueAst valueAst : valueDefinitionsAst.getDefinition(valueName))
                valueAst.value = injector.injectBranchPoint(valueAst.value);
            branchPoints.put(valueName, injector.getAndClearBranchPoints());
        }
    }
}