1 package org.simantics.scl.compiler.elaboration.contexts;
3 import java.util.ArrayList;
5 import org.simantics.scl.compiler.common.exceptions.InternalCompilerError;
6 import org.simantics.scl.compiler.compilation.CompilationContext;
7 import org.simantics.scl.compiler.constants.NoRepConstant;
8 import org.simantics.scl.compiler.elaboration.expressions.EAmbiguous;
9 import org.simantics.scl.compiler.elaboration.expressions.EApply;
10 import org.simantics.scl.compiler.elaboration.expressions.ELiteral;
11 import org.simantics.scl.compiler.elaboration.expressions.EPlaceholder;
12 import org.simantics.scl.compiler.elaboration.expressions.EVariable;
13 import org.simantics.scl.compiler.elaboration.expressions.Expression;
14 import org.simantics.scl.compiler.elaboration.expressions.Variable;
15 import org.simantics.scl.compiler.elaboration.modules.SCLValue;
16 import org.simantics.scl.compiler.environment.Environment;
17 import org.simantics.scl.compiler.errors.ErrorLog;
18 import org.simantics.scl.compiler.internal.elaboration.constraints.Constraint;
19 import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintEnvironment;
20 import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintSolver;
21 import org.simantics.scl.compiler.internal.elaboration.constraints.ExpressionAugmentation;
22 import org.simantics.scl.compiler.internal.elaboration.constraints.ReducedConstraints;
23 import org.simantics.scl.compiler.internal.elaboration.subsumption.Subsumption;
24 import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubSolver2;
25 import org.simantics.scl.compiler.types.Skeletons;
26 import org.simantics.scl.compiler.types.TApply;
27 import org.simantics.scl.compiler.types.TCon;
28 import org.simantics.scl.compiler.types.TForAll;
29 import org.simantics.scl.compiler.types.TFun;
30 import org.simantics.scl.compiler.types.TMetaVar;
31 import org.simantics.scl.compiler.types.TPred;
32 import org.simantics.scl.compiler.types.TUnion;
33 import org.simantics.scl.compiler.types.TVar;
34 import org.simantics.scl.compiler.types.Type;
35 import org.simantics.scl.compiler.types.Types;
36 import org.simantics.scl.compiler.types.exceptions.UnificationException;
37 import org.simantics.scl.compiler.types.kinds.Kinds;
38 import org.simantics.scl.compiler.types.util.Polarity;
39 import org.simantics.scl.compiler.types.util.TypeUnparsingContext;
41 import gnu.trove.map.hash.THashMap;
42 import gnu.trove.set.hash.THashSet;
44 public class TypingContext {
46 private CompilationContext compilationContext;
49 private ArrayList<Subsumption> effectSubsumptions = new ArrayList<Subsumption>();
50 private ArrayList<Subsumption> subsumptions = new ArrayList<Subsumption>();
51 private ArrayList<Type> potentialSingletonEffects = new ArrayList<Type>();
54 private ArrayList<Type> effectUpperBounds = new ArrayList<Type>();
57 private ArrayList<EVariable> constraintDemand = new ArrayList<EVariable>();
58 private ArrayList<Variable[]> constraintFrames = new ArrayList<Variable[]>();
61 private boolean isInPattern;
64 public THashSet<SCLValue> recursiveValues;
65 public ArrayList<EPlaceholder> recursiveReferences;
68 public ArrayList<EAmbiguous> overloadedExpressions = new ArrayList<EAmbiguous>();
70 //TypeUnparsingContext tuc = new TypeUnparsingContext();
72 Environment environment;
74 public TypingContext(CompilationContext compilationContext) {
75 this.compilationContext = compilationContext;
76 this.environment = compilationContext.environment;
80 * Records the fact that {@code a} should be a subeffect
81 * of {@code b}. Only types {@code TMetaVar}, {@code TVar}, {@code TCon}, {@code TUnion}
84 public void subsumeEffect(long loc, Type a, Type b) {
85 a = Types.canonical(a);
86 if(a == Types.NO_EFFECTS)
88 b = Types.canonical(b);
91 if(b == Types.NO_EFFECTS) {
93 Types.unify(a, Types.NO_EFFECTS);
94 } catch(UnificationException e) {
95 compilationContext.errorLog.log(loc, "No side-effects allowed here.");
100 //System.out.println("subsumeEffect(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
102 /*if(a instanceof TUnion) {
103 TUnion union = (TUnion)a;
104 for(Type e : union.effects)
105 subsumeEffect(loc, e, b);
108 effectSubsumptions.add(new Subsumption(loc, a, b));
111 public void subsume(long loc, Type a, Type b) throws UnificationException {
112 a = Types.canonical(a);
113 b = Types.canonical(b);
117 //System.out.println("subsume(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
119 if(a instanceof TMetaVar) {
120 TMetaVar aVar = (TMetaVar)a;
121 if(b instanceof TMetaVar) {
122 Skeletons.unifySkeletons(a, b);
123 subsumptions.add(new Subsumption(loc, a, b));
127 throw new UnificationException(a, b);
128 aVar.setRef(createSubtypeTemplate(loc, b));
132 else if(b instanceof TMetaVar) {
133 TMetaVar bVar = (TMetaVar)b;
135 throw new UnificationException(a, b);
136 bVar.setRef(createSupertypeTemplate(loc, a));
139 if(a instanceof TFun) {
140 if(!(b instanceof TFun))
141 throw new UnificationException(a, b);
144 subsume(loc, bFun.domain, aFun.domain);
145 subsumeEffect(loc, aFun.effect, bFun.effect);
146 subsume(loc, aFun.range, bFun.range);
148 else if(a instanceof TApply) {
151 else if(a instanceof TPred) {
154 else // a instanceof TUnion
155 throw new UnificationException(a, b);
159 * Creates a template for all subtypes of the given type
160 * where all possible varying types are replaced by metavars
161 * with properly set inequalities.
163 private Type createSubtypeTemplate(long loc, Type type) {
164 type = Types.canonical(type);
165 if(type instanceof TCon)
167 else if(type instanceof TApply)
169 else if(type instanceof TPred)
171 else if(type instanceof TFun) {
172 TFun fun = (TFun)type;
173 Type funEffect = Types.canonical(fun.effect);
175 if(funEffect == Types.NO_EFFECTS)
176 effect = Types.NO_EFFECTS;
178 effect = Types.metaVar(Kinds.EFFECT);
179 effectSubsumptions.add(new Subsumption(loc, effect, funEffect));
181 return Types.functionE(
182 createSupertypeTemplate(loc, fun.domain),
184 createSubtypeTemplate(loc, fun.range));
186 else if(type instanceof TMetaVar) {
187 TMetaVar var = (TMetaVar)type;
188 TMetaVar newVar = Types.metaVar(var.getKind());
190 newVar.setSkeletonRef(var);
191 } catch (UnificationException e) {
192 throw new InternalCompilerError(loc, e);
194 subsumptions.add(new Subsumption(loc, newVar, var));
197 else if(type instanceof TVar)
199 else if(type instanceof TUnion) {
200 TUnion union = (TUnion)type;
201 if(union.isMinimal())
203 TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
204 subsumptions.add(new Subsumption(loc, newVar, type));
207 else if(type instanceof TForAll) {
208 TForAll forAll = (TForAll)type;
209 Type t = createSubtypeTemplate(loc, forAll.type);
213 return Types.forAll(forAll.var, t);
216 throw new InternalCompilerError("Unsupported type " + type + ".");
220 * Creates a template for all supertypes of the given type
221 * where all possible varying types are replaced by metavars
222 * with properly set inequalities.
224 private Type createSupertypeTemplate(long loc, Type type) {
225 type = Types.canonical(type);
226 if(type instanceof TCon)
228 else if(type instanceof TApply)
230 else if(type instanceof TPred)
232 else if(type instanceof TFun) {
233 TFun fun = (TFun)type;
234 TMetaVar effect = Types.metaVar(Kinds.EFFECT);
235 effectSubsumptions.add(new Subsumption(loc, fun.effect, effect));
236 return Types.functionE(
237 createSubtypeTemplate(loc, fun.domain),
239 createSupertypeTemplate(loc, fun.range));
241 else if(type instanceof TMetaVar) {
242 TMetaVar var = (TMetaVar)type;
243 TMetaVar newVar = Types.metaVar(var.getKind());
245 newVar.setSkeletonRef(var);
246 } catch (UnificationException e) {
247 throw new InternalCompilerError(loc, e);
249 subsumptions.add(new Subsumption(loc, var, newVar));
252 else if(type instanceof TVar)
254 else if(type instanceof TUnion) {
255 TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
256 subsumptions.add(new Subsumption(loc, type, newVar));
259 else if(type instanceof TForAll) {
260 TForAll forAll = (TForAll)type;
261 Type t = createSupertypeTemplate(loc, forAll.type);
265 return Types.forAll(forAll.var, t);
268 throw new InternalCompilerError("Unsupported type " + type + ".");
272 * Instantiates type abstractions and constraints from the value.
274 public Expression instantiate(Expression expr) {
275 Type type = Types.canonical(expr.getType());
276 while(type instanceof TForAll) {
277 TForAll forAll = (TForAll)type;
278 TVar var = forAll.var;
279 TMetaVar mVar = Types.metaVar(var.getKind());
280 type = Types.canonical(forAll.type).replace(var, mVar);
281 expr = expr.applyType(mVar);
283 while(type instanceof TFun) {
284 TFun fun = (TFun)type;
285 if(fun.domain instanceof TPred) { // No need to canonicalize
286 TPred pred = (TPred)fun.domain;
289 long loc = expr.getLocation();
290 EVariable var = new EVariable(loc, null);
292 expr = new EApply(loc, expr, var);
293 addConstraintDemand(var);
295 else if(fun.domain == Types.PUNIT) {
298 long loc = expr.getLocation();
299 declareEffect(expr.location, fun.effect);
300 expr = new EApply(loc, fun.effect, expr, new ELiteral(loc, NoRepConstant.PUNIT));
310 * Enforces {@code expr} to have type {@code b} by adding
311 * type applications, lambdas and effect subsumptions.
313 public Expression subsume(Expression expr, Type b) {
314 b = Types.canonical(b);
315 /*if(b instanceof TForAll) {
316 TForAll forAll = (TForAll)b;
317 TVar var = forAll.var;
318 TVar newVar = Types.var(var.getKind());
319 b = Types.canonical(forAll.type).replace(var, newVar);
320 return new ELambdaType(new TVar[] {newVar}, subsume(expr, b));
322 expr = instantiate(expr);
325 subsume(expr.getLocation(), expr.getType(), b);
326 } catch(UnificationException e) {
327 typeError(expr.getLocation(), b, expr.getType());
332 private boolean expandSubsumptions() {
333 boolean nontrivialSubs = true;
334 int iterationCount = 0;
335 while(!subsumptions.isEmpty() && nontrivialSubs) {
336 ArrayList<Subsumption> oldSubsumptions = subsumptions;
337 subsumptions = new ArrayList<Subsumption>();
338 nontrivialSubs = false;
339 for(Subsumption sub : oldSubsumptions) {
340 Type a = sub.a = Types.canonical(sub.a);
341 Type b = sub.b = Types.canonical(sub.b);
342 if(b instanceof TMetaVar && a instanceof TMetaVar) {
343 subsumptions.add(sub);
347 subsume(sub.loc, a, b);
348 } catch (UnificationException e) {
349 compilationContext.errorLog.log(sub.loc, "Type " + a + " is not a subtype of " + b + ".");
351 nontrivialSubs = true;
355 if(iterationCount == 5) {
356 // Test that the skeletons are unifiable
357 THashMap<TMetaVar,TMetaVar> metaVarMap =
358 new THashMap<TMetaVar,TMetaVar>();
359 ArrayList<Subsumption> subCopies = new ArrayList<Subsumption>(subsumptions.size());
360 for(Subsumption sub : subsumptions)
362 subCopies.add(new Subsumption(sub.loc,
363 sub.a.copySkeleton(metaVarMap), sub.b.copySkeleton(metaVarMap)));
365 /*System.out.println("----");
366 TypeUnparsingContext tuc = new TypeUnparsingContext();
367 for(Subsumption sub : subCopies)
368 System.out.println(sub.a.toString(tuc) + " == " + sub.b.toString(tuc));*/
370 for(Subsumption sub : subCopies)
372 Types.unify(sub.a, sub.b);
373 } catch (UnificationException e) {
374 compilationContext.errorLog.log(sub.loc, "Unification of types failed.");
378 /*System.out.println("----");
379 for(Subsumption sub : subCopies)
380 System.out.println(sub.a.toString(tuc) + " === " + sub.b.toString(tuc));*/
383 for(Subsumption sub : subsumptions)
385 // FIXME This is not correct in all cases, should emit unsolved subsumptions to the type of the value
386 Types.unify(sub.a, sub.b);
387 } catch (UnificationException e) {
388 // Should not happen. Both types should be metavars.
389 throw new InternalCompilerError(e);
391 subsumptions.clear();
395 private boolean isEffect(Type type) {
396 if(type instanceof TMetaVar)
397 return ((TMetaVar)type).getKind() == Kinds.EFFECT;
398 else if(type instanceof TCon)
399 return environment.getTypeDescriptor((TCon)type).getKind() == Kinds.EFFECT;
400 else if(type instanceof TVar)
401 return ((TVar)type).getKind() == Kinds.EFFECT;
402 else if(type instanceof TUnion)
409 public void solveSubsumptions(long globalLoc) {
410 if(expandSubsumptions()) {
411 if(!effectSubsumptions.isEmpty())
412 SubSolver2.solve(compilationContext.errorLog, effectSubsumptions);
414 if(!potentialSingletonEffects.isEmpty())
416 THashSet<TMetaVar> vars = new THashSet<TMetaVar>(4);
417 for(Type type : potentialSingletonEffects)
418 type.collectMetaVars(vars);
419 for(TMetaVar var : vars) {
420 if(var.getRef() == null) {
421 Polarity polarity = var.getPolarity();
422 if(!polarity.isNegative())
424 var.setRef(Types.NO_EFFECTS);
427 } catch(UnificationException e) {
428 throw new InternalCompilerError(e);
430 //new SubSolver(compilationContext.errorLog, effectSubsumptions, potentialSingletonEffects, globalLoc).solve();
434 public void declareEffect(long loc, Type effect) {
435 subsumeEffect(loc, effect, effectUpperBounds.get(effectUpperBounds.size()-1));
438 public void pushEffectUpperBound(long loc, Type effect) {
439 effectUpperBounds.add(effect);
440 potentialSingletonEffects.add(effect);
443 public Type popEffectUpperBound() {
444 return effectUpperBounds.remove(effectUpperBounds.size()-1);
447 public ErrorLog getErrorLog() {
448 return compilationContext.errorLog;
451 public boolean isInPattern() {
455 public void setInPattern(boolean isInPattern) {
456 this.isInPattern = isInPattern;
459 public void pushConstraintFrame(Variable[] array) {
460 constraintFrames.add(array);
463 public void popConstraintFrame() {
464 constraintFrames.remove(constraintFrames.size()-1);
467 public void addConstraintDemand(EVariable var) {
468 for(int i=constraintFrames.size()-1;i>=0;--i)
469 for(Variable con : constraintFrames.get(i))
470 if(Types.equals(var.getType(), con.getType())) {
471 var.setVariable(con);
474 constraintDemand.add(var);
477 public Expression addConstraint(TPred pred) {
478 EVariable evidence = new EVariable(null);
479 evidence.setType(pred);
480 addConstraintDemand(evidence);
484 public Expression[] addConstraints(TPred[] preds) {
485 if(preds.length == 0)
486 return Expression.EMPTY_ARRAY;
487 Expression[] evidences = new Expression[preds.length];
488 for(int i=0;i<preds.length;++i)
489 evidences[i] = addConstraint(preds[i]);
493 public ArrayList<EVariable> getConstraintDemand() {
494 return constraintDemand;
497 public void resetConstraintDemand() {
498 constraintDemand = new ArrayList<EVariable>();
501 public void typeError(long loc, Type requiredType, Type givenType) {
502 TypeUnparsingContext tuc = new TypeUnparsingContext();
503 compilationContext.errorLog.log(loc, "Expected <" + requiredType.toString(tuc) + "> got <" + givenType.toString(tuc) + ">.");
506 public Expression solveConstraints(Environment environment, Expression expression) {
507 ArrayList<EVariable> constraintDemand = getConstraintDemand();
508 if(!constraintDemand.isEmpty()) {
509 ConstraintEnvironment ce = new ConstraintEnvironment(compilationContext);
510 ReducedConstraints red = ConstraintSolver.solve(
511 ce, new ArrayList<TPred>(0), constraintDemand,
514 expression = ExpressionAugmentation.augmentSolved(
515 red.solvedConstraints,
518 for(Constraint c : red.unsolvedConstraints)
519 compilationContext.errorLog.log(c.getDemandLocation(), "There is no instance for <"+c.constraint+">.");
522 expression = expression.decomposeMatching();
527 public Environment getEnvironment() {
528 return compilationContext.environment;
531 public CompilationContext getCompilationContext() {
532 return compilationContext;