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.SubSolver;
24 import org.simantics.scl.compiler.internal.elaboration.subsumption.Subsumption;
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.TypeUnparsingContext;
40 import gnu.trove.map.hash.THashMap;
41 import gnu.trove.set.hash.THashSet;
43 public class TypingContext {
45 private CompilationContext compilationContext;
48 private ArrayList<Subsumption> effectSubsumptions = new ArrayList<Subsumption>();
49 private ArrayList<Subsumption> subsumptions = new ArrayList<Subsumption>();
50 private ArrayList<Type> potentialSingletonEffects = new ArrayList<Type>();
53 private ArrayList<Type> effectUpperBounds = new ArrayList<Type>();
56 private ArrayList<EVariable> constraintDemand = new ArrayList<EVariable>();
57 private ArrayList<Variable[]> constraintFrames = new ArrayList<Variable[]>();
60 private boolean isInPattern;
63 public THashSet<SCLValue> recursiveValues;
64 public ArrayList<EPlaceholder> recursiveReferences;
67 public ArrayList<EAmbiguous> overloadedExpressions = new ArrayList<EAmbiguous>();
69 //TypeUnparsingContext tuc = new TypeUnparsingContext();
71 Environment environment;
73 public TypingContext(CompilationContext compilationContext) {
74 this.compilationContext = compilationContext;
75 this.environment = compilationContext.environment;
79 * Records the fact that {@code a} should be a subeffect
80 * of {@code b}. Only types {@code TMetaVar}, {@code TVar}, {@code TCon}, {@code TUnion}
83 public void subsumeEffect(long loc, Type a, Type b) {
84 a = Types.canonical(a);
85 if(a == Types.NO_EFFECTS)
87 b = Types.canonical(b);
90 if(b == Types.NO_EFFECTS) {
92 Types.unify(a, Types.NO_EFFECTS);
93 } catch(UnificationException e) {
94 compilationContext.errorLog.log(loc, "No side-effects allowed here.");
99 //System.out.println("subsumeEffect(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
101 /*if(a instanceof TUnion) {
102 TUnion union = (TUnion)a;
103 for(Type e : union.effects)
104 subsumeEffect(loc, e, b);
107 effectSubsumptions.add(new Subsumption(loc, a, b));
110 public void subsume(long loc, Type a, Type b) throws UnificationException {
111 a = Types.canonical(a);
112 b = Types.canonical(b);
116 //System.out.println("subsume(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
118 if(a instanceof TMetaVar) {
119 TMetaVar aVar = (TMetaVar)a;
120 if(b instanceof TMetaVar) {
121 Skeletons.unifySkeletons(a, b);
122 subsumptions.add(new Subsumption(loc, a, b));
126 throw new UnificationException(a, b);
127 aVar.setRef(createSubtypeTemplate(loc, b));
131 else if(b instanceof TMetaVar) {
132 TMetaVar bVar = (TMetaVar)b;
134 throw new UnificationException(a, b);
135 bVar.setRef(createSupertypeTemplate(loc, a));
138 if(a instanceof TFun) {
139 if(!(b instanceof TFun))
140 throw new UnificationException(a, b);
143 subsume(loc, bFun.domain, aFun.domain);
144 subsumeEffect(loc, aFun.effect, bFun.effect);
145 subsume(loc, aFun.range, bFun.range);
147 else if(a instanceof TApply) {
150 else if(a instanceof TPred) {
153 else // a instanceof TUnion
154 throw new UnificationException(a, b);
158 * Creates a template for all subtypes of the given type
159 * where all possible varying types are replaced by metavars
160 * with properly set inequalities.
162 private Type createSubtypeTemplate(long loc, Type type) {
163 type = Types.canonical(type);
164 if(type instanceof TCon)
166 else if(type instanceof TApply)
168 else if(type instanceof TPred)
170 else if(type instanceof TFun) {
171 TFun fun = (TFun)type;
172 Type funEffect = Types.canonical(fun.effect);
174 if(funEffect == Types.NO_EFFECTS)
175 effect = Types.NO_EFFECTS;
177 effect = Types.metaVar(Kinds.EFFECT);
178 effectSubsumptions.add(new Subsumption(loc, effect, funEffect));
180 return Types.functionE(
181 createSupertypeTemplate(loc, fun.domain),
183 createSubtypeTemplate(loc, fun.range));
185 else if(type instanceof TMetaVar) {
186 TMetaVar var = (TMetaVar)type;
187 TMetaVar newVar = Types.metaVar(var.getKind());
189 newVar.setSkeletonRef(var);
190 } catch (UnificationException e) {
191 throw new InternalCompilerError(loc, e);
193 subsumptions.add(new Subsumption(loc, newVar, var));
196 else if(type instanceof TVar)
198 else if(type instanceof TUnion) {
199 TUnion union = (TUnion)type;
200 if(union.isMinimal())
202 TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
203 subsumptions.add(new Subsumption(loc, newVar, type));
206 else if(type instanceof TForAll) {
207 TForAll forAll = (TForAll)type;
208 Type t = createSubtypeTemplate(loc, forAll.type);
212 return Types.forAll(forAll.var, t);
215 throw new InternalCompilerError("Unsupported type " + type + ".");
219 * Creates a template for all supertypes of the given type
220 * where all possible varying types are replaced by metavars
221 * with properly set inequalities.
223 private Type createSupertypeTemplate(long loc, Type type) {
224 type = Types.canonical(type);
225 if(type instanceof TCon)
227 else if(type instanceof TApply)
229 else if(type instanceof TPred)
231 else if(type instanceof TFun) {
232 TFun fun = (TFun)type;
233 TMetaVar effect = Types.metaVar(Kinds.EFFECT);
234 effectSubsumptions.add(new Subsumption(loc, fun.effect, effect));
235 return Types.functionE(
236 createSubtypeTemplate(loc, fun.domain),
238 createSupertypeTemplate(loc, fun.range));
240 else if(type instanceof TMetaVar) {
241 TMetaVar var = (TMetaVar)type;
242 TMetaVar newVar = Types.metaVar(var.getKind());
244 newVar.setSkeletonRef(var);
245 } catch (UnificationException e) {
246 throw new InternalCompilerError(loc, e);
248 subsumptions.add(new Subsumption(loc, var, newVar));
251 else if(type instanceof TVar)
253 else if(type instanceof TUnion) {
254 TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
255 subsumptions.add(new Subsumption(loc, type, newVar));
258 else if(type instanceof TForAll) {
259 TForAll forAll = (TForAll)type;
260 Type t = createSupertypeTemplate(loc, forAll.type);
264 return Types.forAll(forAll.var, t);
267 throw new InternalCompilerError("Unsupported type " + type + ".");
271 * Instantiates type abstractions and constraints from the value.
273 public Expression instantiate(Expression expr) {
274 Type type = Types.canonical(expr.getType());
275 while(type instanceof TForAll) {
276 TForAll forAll = (TForAll)type;
277 TVar var = forAll.var;
278 TMetaVar mVar = Types.metaVar(var.getKind());
279 type = Types.canonical(forAll.type).replace(var, mVar);
280 expr = expr.applyType(mVar);
282 while(type instanceof TFun) {
283 TFun fun = (TFun)type;
284 if(fun.domain instanceof TPred) { // No need to canonicalize
285 TPred pred = (TPred)fun.domain;
288 long loc = expr.getLocation();
289 EVariable var = new EVariable(loc, null);
291 expr = new EApply(loc, expr, var);
292 addConstraintDemand(var);
294 else if(fun.domain == Types.PUNIT) {
297 long loc = expr.getLocation();
298 declareEffect(expr.location, fun.effect);
299 expr = new EApply(loc, fun.effect, expr, new ELiteral(loc, NoRepConstant.PUNIT));
309 * Enforces {@code expr} to have type {@code b} by adding
310 * type applications, lambdas and effect subsumptions.
312 public Expression subsume(Expression expr, Type b) {
313 b = Types.canonical(b);
314 /*if(b instanceof TForAll) {
315 TForAll forAll = (TForAll)b;
316 TVar var = forAll.var;
317 TVar newVar = Types.var(var.getKind());
318 b = Types.canonical(forAll.type).replace(var, newVar);
319 return new ELambdaType(new TVar[] {newVar}, subsume(expr, b));
321 expr = instantiate(expr);
324 subsume(expr.getLocation(), expr.getType(), b);
325 } catch(UnificationException e) {
326 typeError(expr.getLocation(), b, expr.getType());
331 private boolean expandSubsumptions() {
332 boolean nontrivialSubs = true;
333 int iterationCount = 0;
334 while(!subsumptions.isEmpty() && nontrivialSubs) {
335 ArrayList<Subsumption> oldSubsumptions = subsumptions;
336 subsumptions = new ArrayList<Subsumption>();
337 nontrivialSubs = false;
338 for(Subsumption sub : oldSubsumptions) {
339 Type a = sub.a = Types.canonical(sub.a);
340 Type b = sub.b = Types.canonical(sub.b);
341 if(b instanceof TMetaVar && a instanceof TMetaVar) {
342 subsumptions.add(sub);
346 subsume(sub.loc, a, b);
347 } catch (UnificationException e) {
348 compilationContext.errorLog.log(sub.loc, "Type " + a + " is not a subtype of " + b + ".");
350 nontrivialSubs = true;
354 if(iterationCount == 5) {
355 // Test that the skeletons are unifiable
356 THashMap<TMetaVar,TMetaVar> metaVarMap =
357 new THashMap<TMetaVar,TMetaVar>();
358 ArrayList<Subsumption> subCopies = new ArrayList<Subsumption>(subsumptions.size());
359 for(Subsumption sub : subsumptions)
361 subCopies.add(new Subsumption(sub.loc,
362 sub.a.copySkeleton(metaVarMap), sub.b.copySkeleton(metaVarMap)));
364 /*System.out.println("----");
365 TypeUnparsingContext tuc = new TypeUnparsingContext();
366 for(Subsumption sub : subCopies)
367 System.out.println(sub.a.toString(tuc) + " == " + sub.b.toString(tuc));*/
369 for(Subsumption sub : subCopies)
371 Types.unify(sub.a, sub.b);
372 } catch (UnificationException e) {
373 compilationContext.errorLog.log(sub.loc, "Unification of types failed.");
377 /*System.out.println("----");
378 for(Subsumption sub : subCopies)
379 System.out.println(sub.a.toString(tuc) + " === " + sub.b.toString(tuc));*/
382 for(Subsumption sub : subsumptions)
384 // FIXME This is not correct in all cases, should emit unsolved subsumptions to the type of the value
385 Types.unify(sub.a, sub.b);
386 } catch (UnificationException e) {
387 // Should not happen. Both types should be metavars.
388 throw new InternalCompilerError(e);
390 subsumptions.clear();
394 private boolean isEffect(Type type) {
395 if(type instanceof TMetaVar)
396 return ((TMetaVar)type).getKind() == Kinds.EFFECT;
397 else if(type instanceof TCon)
398 return environment.getTypeDescriptor((TCon)type).getKind() == Kinds.EFFECT;
399 else if(type instanceof TVar)
400 return ((TVar)type).getKind() == Kinds.EFFECT;
401 else if(type instanceof TUnion)
408 public void solveSubsumptions(long globalLoc) {
409 if(expandSubsumptions())
410 new SubSolver(compilationContext.errorLog, effectSubsumptions, potentialSingletonEffects, globalLoc).solve();
413 public void declareEffect(long loc, Type effect) {
414 subsumeEffect(loc, effect, effectUpperBounds.get(effectUpperBounds.size()-1));
417 public void pushEffectUpperBound(long loc, Type effect) {
418 effectUpperBounds.add(effect);
419 potentialSingletonEffects.add(effect);
422 public Type popEffectUpperBound() {
423 return effectUpperBounds.remove(effectUpperBounds.size()-1);
426 public ErrorLog getErrorLog() {
427 return compilationContext.errorLog;
430 public boolean isInPattern() {
434 public void setInPattern(boolean isInPattern) {
435 this.isInPattern = isInPattern;
438 public void pushConstraintFrame(Variable[] array) {
439 constraintFrames.add(array);
442 public void popConstraintFrame() {
443 constraintFrames.remove(constraintFrames.size()-1);
446 public void addConstraintDemand(EVariable var) {
447 for(int i=constraintFrames.size()-1;i>=0;--i)
448 for(Variable con : constraintFrames.get(i))
449 if(Types.equals(var.getType(), con.getType())) {
450 var.setVariable(con);
453 constraintDemand.add(var);
456 public Expression addConstraint(TPred pred) {
457 EVariable evidence = new EVariable(null);
458 evidence.setType(pred);
459 addConstraintDemand(evidence);
463 public Expression[] addConstraints(TPred[] preds) {
464 if(preds.length == 0)
465 return Expression.EMPTY_ARRAY;
466 Expression[] evidences = new Expression[preds.length];
467 for(int i=0;i<preds.length;++i)
468 evidences[i] = addConstraint(preds[i]);
472 public ArrayList<EVariable> getConstraintDemand() {
473 return constraintDemand;
476 public void resetConstraintDemand() {
477 constraintDemand = new ArrayList<EVariable>();
480 public void typeError(long loc, Type requiredType, Type givenType) {
481 TypeUnparsingContext tuc = new TypeUnparsingContext();
482 compilationContext.errorLog.log(loc, "Expected <" + requiredType.toString(tuc) + "> got <" + givenType.toString(tuc) + ">.");
485 public Expression solveConstraints(Environment environment, Expression expression) {
486 ArrayList<EVariable> constraintDemand = getConstraintDemand();
487 if(!constraintDemand.isEmpty()) {
488 ConstraintEnvironment ce = new ConstraintEnvironment(compilationContext);
489 ReducedConstraints red = ConstraintSolver.solve(
490 ce, new ArrayList<TPred>(0), constraintDemand,
493 expression = ExpressionAugmentation.augmentSolved(
494 red.solvedConstraints,
497 for(Constraint c : red.unsolvedConstraints)
498 compilationContext.errorLog.log(c.getDemandLocation(), "There is no instance for <"+c.constraint+">.");
501 expression = expression.decomposeMatching();
506 public Environment getEnvironment() {
507 return compilationContext.environment;
510 public CompilationContext getCompilationContext() {
511 return compilationContext;