X-Git-Url: https://gerrit.simantics.org/r/gitweb?a=blobdiff_plain;f=bundles%2Forg.simantics.scl.compiler%2Fsrc%2Forg%2Fsimantics%2Fscl%2Fcompiler%2Fcompilation%2FTypeChecking.java;fp=bundles%2Forg.simantics.scl.compiler%2Fsrc%2Forg%2Fsimantics%2Fscl%2Fcompiler%2Fcompilation%2FTypeChecking.java;h=97266d6e9781e16d2c5d77ba4d0107b80f8ee251;hb=969bd23cab98a79ca9101af33334000879fb60c5;hp=0000000000000000000000000000000000000000;hpb=866dba5cd5a3929bbeae85991796acb212338a08;p=simantics%2Fplatform.git diff --git a/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/compilation/TypeChecking.java b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/compilation/TypeChecking.java new file mode 100644 index 000000000..97266d6e9 --- /dev/null +++ b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/compilation/TypeChecking.java @@ -0,0 +1,426 @@ +package org.simantics.scl.compiler.compilation; + +import static org.simantics.scl.compiler.elaboration.expressions.Expressions.apply; +import static org.simantics.scl.compiler.elaboration.expressions.Expressions.applyTypes; +import static org.simantics.scl.compiler.elaboration.expressions.Expressions.lambda; +import static org.simantics.scl.compiler.elaboration.expressions.Expressions.loc; +import static org.simantics.scl.compiler.elaboration.expressions.Expressions.vars; +import gnu.trove.map.hash.THashMap; +import gnu.trove.map.hash.TObjectIntHashMap; +import gnu.trove.set.hash.THashSet; +import gnu.trove.set.hash.TIntHashSet; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; + +import org.simantics.scl.compiler.elaboration.contexts.TypingContext; +import org.simantics.scl.compiler.elaboration.expressions.EPlaceholder; +import org.simantics.scl.compiler.elaboration.expressions.ETransformation; +import org.simantics.scl.compiler.elaboration.expressions.EVariable; +import org.simantics.scl.compiler.elaboration.expressions.Expression; +import org.simantics.scl.compiler.elaboration.expressions.Variable; +import org.simantics.scl.compiler.elaboration.modules.SCLValue; +import org.simantics.scl.compiler.elaboration.query.Query; +import org.simantics.scl.compiler.elaboration.relations.ConcreteRelation; +import org.simantics.scl.compiler.elaboration.relations.ConcreteRelation.QuerySection; +import org.simantics.scl.compiler.elaboration.relations.SCLRelation; +import org.simantics.scl.compiler.elaboration.rules.MappingRelation; +import org.simantics.scl.compiler.elaboration.rules.TransformationRule; +import org.simantics.scl.compiler.environment.Environment; +import org.simantics.scl.compiler.errors.ErrorLog; +import org.simantics.scl.compiler.internal.elaboration.constraints.Constraint; +import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintEnvironment; +import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintSolver; +import org.simantics.scl.compiler.internal.elaboration.constraints.ExpressionAugmentation; +import org.simantics.scl.compiler.internal.elaboration.constraints.ReducedConstraints; +import org.simantics.scl.compiler.module.ConcreteModule; +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.Kinds; +import org.simantics.scl.compiler.types.util.Polarity; + +public class TypeChecking { + final ErrorLog errorLog; + final Environment environment; + final ConcreteModule module; + + ConstraintEnvironment ce; + TypeCheckingScheduler scheduler; + + public TypeChecking(ErrorLog errorLog, Environment environment, + ConcreteModule module) { + this.errorLog = errorLog; + this.environment = environment; + this.module = module; + } + + private void typeCheckValues() { + for(final SCLValue value : module.getValues()) { + if(value.getExpression() != null) { + if(value.getType() == null) + scheduler.addTypeInferableDefinition(new TypeInferableDefinition() { + ArrayList recursiveReferences; + ArrayList constraintDemand; + ArrayList freeEvidence; + ArrayList unsolvedConstraints; + + @Override + public long getLocation() { + return value.getExpression().getLocation(); + } + + @Override + public Collection getDefinedObjects() { + return Collections.singleton(value); + } + + @Override + public void collectRefs(TObjectIntHashMap allRefs, TIntHashSet refs) { + value.getExpression().collectRefs(allRefs, refs); + } + + @Override + public void initializeTypeChecking(TypingContext context) { + value.setType(Types.metaVar(Kinds.STAR)); + context.recursiveValues.add(value); + } + + @Override + public void checkType(TypingContext context) { + context.recursiveReferences = + this.recursiveReferences = new ArrayList(); + + Expression expression = value.getExpression(); + context.pushEffectUpperBound(expression.location, Types.PROC); + expression = expression.checkType(context, value.getType()); + context.popEffectUpperBound(); + value.setExpression(expression); + + ArrayList constraintDemand = context.getConstraintDemand(); + if(!constraintDemand.isEmpty()) { + this.constraintDemand = constraintDemand; + context.resetConstraintDemand(); + } + + expression.getType().addPolarity(Polarity.POSITIVE); + } + + @Override + public void solveConstraints() { + if(constraintDemand != null) { + Expression expression = value.getExpression(); + + ReducedConstraints red = ConstraintSolver.solve( + ce, new ArrayList(0), constraintDemand, + true); + + expression = ExpressionAugmentation.augmentSolved( + red.solvedConstraints, + expression); + value.setExpression(expression); + value.setType(expression.getType()); + + for(Constraint c : red.unsolvedConstraints) + if(c.constraint.isGround()) + errorLog.log(c.getDemandLocation(), "There is no instance for <"+c.constraint+">."); + + ArrayList fe = new ArrayList(red.unsolvedConstraints.size()); + for(Constraint c : red.unsolvedConstraints) + fe.add(c.evidence); + unsolvedConstraints = red.unsolvedConstraints; + freeEvidence = fe; + } + else { + value.setExpression(value.getExpression().decomposeMatching()); + freeEvidence = new ArrayList(0); + } + } + + @Override + public void collectFreeTypeVariables( + THashSet varSet) { + Type type = value.getType(); + type = type.convertMetaVarsToVars(); + value.setType(type); + varSet.addAll(Types.freeVars(type)); + } + + @Override + public ArrayList getFreeEvidence() { + return freeEvidence; + } + + @Override + public ArrayList getUnsolvedConstraints() { + return unsolvedConstraints; + } + + @Override + public void injectEvidence(TVar[] vars, TPred[] constraints) { + // Create evidence array of every value in the group that has the variables + // in the same array as in the shared array + THashMap indexedEvidence = new THashMap(freeEvidence.size()); + for(Variable v : freeEvidence) + indexedEvidence.put((TPred)v.getType(), v); + freeEvidence.clear(); + for(TPred c : constraints) { + Variable var = indexedEvidence.get(c); + if(var == null) { + // These are variables that are not directly needed in + // this definition but in the definitions that are + // recursively called + var = new Variable("evX"); + var.setType(c); + freeEvidence.add(var); + } + freeEvidence.add(var); + } + + // Add evidence parameters to the functions + value.setExpression(lambda(Types.NO_EFFECTS, freeEvidence, value.getExpression()) + .closure(vars)); + value.setType(Types.forAll(vars, + Types.constrained(constraints, value.getType()))); + + // Add evidence parameters to recursive calls + for(EPlaceholder ref : recursiveReferences) { + ref.expression = loc(ref.expression.location, apply( + Types.NO_EFFECTS, + applyTypes(ref.expression, vars), + vars(freeEvidence))); + } + } + }); + else + scheduler.addPostTypeCheckingRunnable(new Runnable() { + @Override + public void run() { + Type type = value.getType(); + Expression expression = value.getExpression(); + + try { + ArrayList vars = new ArrayList(); + type = Types.removeForAll(type, vars); + ArrayList givenConstraints = new ArrayList(); + type = Types.removePred(type, givenConstraints); + + TypingContext context = new TypingContext(errorLog, environment); + context.pushEffectUpperBound(expression.location, Types.PROC); + expression = expression.checkType(context, type); + context.popEffectUpperBound(); + expression.getType().addPolarity(Polarity.POSITIVE); + context.solveSubsumptions(expression.getLocation()); + ArrayList demands = context.getConstraintDemand(); + if(!demands.isEmpty() || !givenConstraints.isEmpty()) { + ReducedConstraints red = + ConstraintSolver.solve(ce, givenConstraints, demands, true); + givenConstraints.clear(); + for(Constraint c : red.unsolvedConstraints) { + errorLog.log(c.getDemandLocation(), + "Constraint <"+c.constraint+"> is not given and cannot be derived."); + } + if(errorLog.isEmpty()) { // To prevent exceptions + expression = ExpressionAugmentation.augmentSolved( + red.solvedConstraints, + expression); + expression = ExpressionAugmentation.augmentUnsolved( + red.givenConstraints, + expression); + } + } + else { + if(errorLog.isEmpty()) // To prevent exceptions + expression = expression.decomposeMatching(); + } + expression = expression.closure(vars.toArray(new TVar[vars.size()])); + value.setExpression(expression); + } catch(Exception e) { + errorLog.log(expression.location, e); + } + } + }); + } + } + } + + private void typeCheckRelations() { + for(SCLRelation relation_ : module.getRelations()) { + if(!(relation_ instanceof ConcreteRelation)) + continue; + final ConcreteRelation relation = (ConcreteRelation)relation_; + scheduler.addTypeInferableDefinition(new TypeInferableDefinition() { + + @Override + public void initializeTypeChecking(TypingContext context) { + for(Variable parameter : relation.parameters) { + Type type = Types.metaVar(Kinds.STAR); + type.addPolarity(Polarity.BIPOLAR); + parameter.setType(type); + } + } + + @Override + public void solveConstraints() { + } + + @Override + public void injectEvidence(TVar[] vars, TPred[] constraints) { + relation.typeVariables = vars; + } + + @Override + public ArrayList getUnsolvedConstraints() { + return new ArrayList(0); // TODO + } + + @Override + public long getLocation() { + return relation.location; + } + + @Override + public ArrayList getFreeEvidence() { + return new ArrayList(0); // TODO + } + + @Override + public Collection getDefinedObjects() { + return Collections.singleton(relation); + } + + @Override + public void collectRefs(TObjectIntHashMap allRefs, TIntHashSet refs) { + for(QuerySection section : relation.getSections()) + section.query.collectRefs(allRefs, refs); + } + + @Override + public void collectFreeTypeVariables(THashSet varSet) { + for(Variable parameter : relation.parameters) { + Type parameterType = parameter.getType().convertMetaVarsToVars(); + varSet.addAll(Types.freeVars(parameterType)); + } + } + + @Override + public void checkType(TypingContext context) { + for(QuerySection section : relation.getSections()) { + section.effect = Types.metaVar(Kinds.EFFECT); + context.pushEffectUpperBound(relation.location, section.effect); + for(Variable variable : section.existentials) + variable.setType(Types.metaVar(Kinds.STAR)); + section.query.checkType(context); + context.popEffectUpperBound(); + } + + if(relation.enforceSection != null) { + relation.writingEffect = Types.metaVar(Kinds.EFFECT); + context.pushEffectUpperBound(relation.location, relation.writingEffect); + relation.enforceSection.checkType(context); + context.popEffectUpperBound(); + } + } + }); + } + } + + public void typeCheck() { + ce = new ConstraintEnvironment(environment); + scheduler = new TypeCheckingScheduler(errorLog, environment); + + typeCheckValues(); + typeCheckRelations(); + typeCheckRules(); + + scheduler.schedule(); + } + + private void typeCheckRules() { + scheduler.addTypeInferableDefinition(new TypeInferableDefinition() { + @Override + public void solveConstraints() { + // TODO Auto-generated method stub + } + + @Override + public void injectEvidence(TVar[] vars, TPred[] constraints) { + // TODO Auto-generated method stub + + } + + @Override + public void initializeTypeChecking(TypingContext context) { + // TODO Auto-generated method stub + + } + + @Override + public ArrayList getUnsolvedConstraints() { + return new ArrayList(0); + /* + ArrayList demands = context.getConstraintDemand(); + if(!demands.isEmpty()) { + ReducedConstraints red = + ConstraintSolver.solve(ce, new ArrayList(), demands, true); + for(Constraint c : red.unsolvedConstraints) { + errorLog.log(c.getDemandLocation(), + "Constraint <"+c.constraint+"> is not given and cannot be derived."); + } + }*/ + } + + @Override + public long getLocation() { + // TODO Auto-generated method stub + return 0; + } + + @Override + public ArrayList getFreeEvidence() { + return new ArrayList(0); + } + + @Override + public Collection getDefinedObjects() { + return Collections.singleton(ETransformation.TRANSFORMATION_RULES_TYPECHECKED); + } + + @Override + public void collectRefs(TObjectIntHashMap allRefs, TIntHashSet refs) { + for(TransformationRule rule : module.getRules()) + for(Query[] queries : rule.sections.values()) + for(Query query : queries) + query.collectRefs(allRefs, refs); + } + + @Override + public void collectFreeTypeVariables(THashSet varSet) { + } + + @Override + public void checkType(TypingContext context) { + for(TransformationRule rule : module.getRules()) { + context.pushEffectUpperBound(rule.location, Types.metaVar(Kinds.EFFECT)); + rule.checkType(context); + rule.setEffect(Types.canonical(context.popEffectUpperBound())); + } + } + }); + + if(!module.getMappingRelations().isEmpty()) + scheduler.addPostTypeCheckingRunnable(new Runnable() { + @Override + public void run() { + for(MappingRelation mappingRelation : module.getMappingRelations()) + for(Type parameterType : mappingRelation.parameterTypes) + if(!parameterType.isGround()) { + errorLog.log(mappingRelation.location, "Parameter types of the mapping relation are not completely determined."); + break; + } + } + }); + } +}