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.TApply;
26 import org.simantics.scl.compiler.types.TCon;
27 import org.simantics.scl.compiler.types.TForAll;
28 import org.simantics.scl.compiler.types.TFun;
29 import org.simantics.scl.compiler.types.TMetaVar;
30 import org.simantics.scl.compiler.types.TPred;
31 import org.simantics.scl.compiler.types.TUnion;
32 import org.simantics.scl.compiler.types.TVar;
33 import org.simantics.scl.compiler.types.Type;
34 import org.simantics.scl.compiler.types.Types;
35 import org.simantics.scl.compiler.types.exceptions.UnificationException;
36 import org.simantics.scl.compiler.types.kinds.Kinds;
37 import org.simantics.scl.compiler.types.util.TypeUnparsingContext;
39 import gnu.trove.map.hash.THashMap;
40 import gnu.trove.set.hash.THashSet;
42 public class TypingContext {
44 private CompilationContext compilationContext;
47 private ArrayList<Subsumption> effectSubsumptions = new ArrayList<Subsumption>();
48 private ArrayList<Subsumption> subsumptions = new ArrayList<Subsumption>();
49 private ArrayList<Type> potentialSingletonEffects = new ArrayList<Type>();
52 private ArrayList<Type> effectUpperBounds = new ArrayList<Type>();
55 private ArrayList<EVariable> constraintDemand = new ArrayList<EVariable>();
56 private ArrayList<Variable[]> constraintFrames = new ArrayList<Variable[]>();
59 private boolean isInPattern;
62 public THashSet<SCLValue> recursiveValues;
63 public ArrayList<EPlaceholder> recursiveReferences;
66 public ArrayList<EAmbiguous> overloadedExpressions = new ArrayList<EAmbiguous>();
68 //TypeUnparsingContext tuc = new TypeUnparsingContext();
70 Environment environment;
72 public TypingContext(CompilationContext compilationContext) {
73 this.compilationContext = compilationContext;
74 this.environment = compilationContext.environment;
78 * Records the fact that {@code a} should be a subeffect
79 * of {@code b}. Only types {@code TMetaVar}, {@code TVar}, {@code TCon}, {@code TUnion}
82 public void subsumeEffect(long loc, Type a, Type b) {
83 a = Types.canonical(a);
84 if(a == Types.NO_EFFECTS)
86 b = Types.canonical(b);
89 if(b == Types.NO_EFFECTS) {
91 Types.unify(a, Types.NO_EFFECTS);
92 } catch(UnificationException e) {
93 compilationContext.errorLog.log(loc, "No side-effects allowed here.");
98 //System.out.println("subsumeEffect(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
100 /*if(a instanceof TUnion) {
101 TUnion union = (TUnion)a;
102 for(Type e : union.effects)
103 subsumeEffect(loc, e, b);
106 effectSubsumptions.add(new Subsumption(loc, a, b));
109 public void subsume(long loc, Type a, Type b) throws UnificationException {
110 a = Types.canonical(a);
111 b = Types.canonical(b);
115 //System.out.println("subsume(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
117 if(a instanceof TMetaVar) {
118 TMetaVar aVar = (TMetaVar)a;
119 if(b instanceof TMetaVar)
120 subsumptions.add(new Subsumption(loc, a, b));
123 throw new UnificationException(a, b);
124 aVar.setRef(createSubtypeTemplate(loc, b));
128 else if(b instanceof TMetaVar) {
129 TMetaVar bVar = (TMetaVar)b;
131 throw new UnificationException(a, b);
132 bVar.setRef(createSupertypeTemplate(loc, a));
135 if(a instanceof TFun) {
136 if(!(b instanceof TFun))
137 throw new UnificationException(a, b);
140 subsume(loc, bFun.domain, aFun.domain);
141 subsumeEffect(loc, aFun.effect, bFun.effect);
142 subsume(loc, aFun.range, bFun.range);
144 else if(a instanceof TApply) {
147 else if(a instanceof TPred) {
150 else // a instanceof TUnion
151 throw new UnificationException(a, b);
155 * Creates a template for all subtypes of the given type
156 * where all possible varying types are replaced by metavars
157 * with properly set inequalities.
159 private Type createSubtypeTemplate(long loc, Type type) {
160 type = Types.canonical(type);
161 if(type instanceof TCon)
163 else if(type instanceof TApply)
165 else if(type instanceof TPred)
167 else if(type instanceof TFun) {
168 TFun fun = (TFun)type;
169 Type funEffect = Types.canonical(fun.effect);
171 if(funEffect == Types.NO_EFFECTS)
172 effect = Types.NO_EFFECTS;
174 effect = Types.metaVar(Kinds.EFFECT);
175 effectSubsumptions.add(new Subsumption(loc, effect, funEffect));
177 return Types.functionE(
178 createSupertypeTemplate(loc, fun.domain),
180 createSubtypeTemplate(loc, fun.range));
182 else if(type instanceof TMetaVar) {
183 TMetaVar var = (TMetaVar)type;
184 TMetaVar newVar = Types.metaVar(var.getKind());
185 subsumptions.add(new Subsumption(loc, newVar, var));
188 else if(type instanceof TVar)
190 else if(type instanceof TUnion) {
191 TUnion union = (TUnion)type;
192 if(union.isMinimal())
194 TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
195 subsumptions.add(new Subsumption(loc, newVar, type));
198 else if(type instanceof TForAll) {
199 TForAll forAll = (TForAll)type;
200 Type t = createSubtypeTemplate(loc, forAll.type);
204 return Types.forAll(forAll.var, t);
207 throw new InternalCompilerError("Unsupported type " + type + ".");
211 * Creates a template for all supertypes of the given type
212 * where all possible varying types are replaced by metavars
213 * with properly set inequalities.
215 private Type createSupertypeTemplate(long loc, Type type) {
216 type = Types.canonical(type);
217 if(type instanceof TCon)
219 else if(type instanceof TApply)
221 else if(type instanceof TPred)
223 else if(type instanceof TFun) {
224 TFun fun = (TFun)type;
225 TMetaVar effect = Types.metaVar(Kinds.EFFECT);
226 effectSubsumptions.add(new Subsumption(loc, fun.effect, effect));
227 return Types.functionE(
228 createSubtypeTemplate(loc, fun.domain),
230 createSupertypeTemplate(loc, fun.range));
232 else if(type instanceof TMetaVar) {
233 TMetaVar var = (TMetaVar)type;
234 TMetaVar newVar = Types.metaVar(var.getKind());
235 subsumptions.add(new Subsumption(loc, var, newVar));
238 else if(type instanceof TVar)
240 else if(type instanceof TUnion) {
241 TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
242 subsumptions.add(new Subsumption(loc, type, newVar));
245 else if(type instanceof TForAll) {
246 TForAll forAll = (TForAll)type;
247 Type t = createSupertypeTemplate(loc, forAll.type);
251 return Types.forAll(forAll.var, t);
254 throw new InternalCompilerError("Unsupported type " + type + ".");
258 * Instantiates type abstractions and constraints from the value.
260 public Expression instantiate(Expression expr) {
261 Type type = Types.canonical(expr.getType());
262 while(type instanceof TForAll) {
263 TForAll forAll = (TForAll)type;
264 TVar var = forAll.var;
265 TMetaVar mVar = Types.metaVar(var.getKind());
266 type = Types.canonical(forAll.type).replace(var, mVar);
267 expr = expr.applyType(mVar);
269 while(type instanceof TFun) {
270 TFun fun = (TFun)type;
271 if(fun.domain instanceof TPred) { // No need to canonicalize
272 TPred pred = (TPred)fun.domain;
275 long loc = expr.getLocation();
276 EVariable var = new EVariable(loc, null);
278 expr = new EApply(loc, expr, var);
279 addConstraintDemand(var);
281 else if(fun.domain == Types.PUNIT) {
284 long loc = expr.getLocation();
285 declareEffect(expr.location, fun.effect);
286 expr = new EApply(loc, fun.effect, expr, new ELiteral(loc, NoRepConstant.PUNIT));
296 * Enforces {@code expr} to have type {@code b} by adding
297 * type applications, lambdas and effect subsumptions.
299 public Expression subsume(Expression expr, Type b) {
300 b = Types.canonical(b);
301 /*if(b instanceof TForAll) {
302 TForAll forAll = (TForAll)b;
303 TVar var = forAll.var;
304 TVar newVar = Types.var(var.getKind());
305 b = Types.canonical(forAll.type).replace(var, newVar);
306 return new ELambdaType(new TVar[] {newVar}, subsume(expr, b));
308 expr = instantiate(expr);
311 subsume(expr.getLocation(), expr.getType(), b);
312 } catch(UnificationException e) {
313 typeError(expr.getLocation(), b, expr.getType());
318 private boolean expandSubsumptions() {
319 boolean nontrivialSubs = true;
320 int iterationCount = 0;
321 while(!subsumptions.isEmpty() && nontrivialSubs) {
322 ArrayList<Subsumption> oldSubsumptions = subsumptions;
323 subsumptions = new ArrayList<Subsumption>();
324 nontrivialSubs = false;
325 for(Subsumption sub : oldSubsumptions) {
326 Type a = sub.a = Types.canonical(sub.a);
327 Type b = sub.b = Types.canonical(sub.b);
328 if(b instanceof TMetaVar && a instanceof TMetaVar) {
329 subsumptions.add(sub);
333 subsume(sub.loc, a, b);
334 } catch (UnificationException e) {
335 compilationContext.errorLog.log(sub.loc, "Type " + a + " is not a subtype of " + b + ".");
337 nontrivialSubs = true;
341 if(iterationCount == 5) {
342 // Test that the skeletons are unifiable
343 THashMap<TMetaVar,TMetaVar> metaVarMap =
344 new THashMap<TMetaVar,TMetaVar>();
345 ArrayList<Subsumption> subCopies = new ArrayList<Subsumption>(subsumptions.size());
346 for(Subsumption sub : subsumptions)
348 subCopies.add(new Subsumption(sub.loc,
349 sub.a.copySkeleton(metaVarMap), sub.b.copySkeleton(metaVarMap)));
351 /*System.out.println("----");
352 TypeUnparsingContext tuc = new TypeUnparsingContext();
353 for(Subsumption sub : subCopies)
354 System.out.println(sub.a.toString(tuc) + " == " + sub.b.toString(tuc));*/
356 for(Subsumption sub : subCopies)
358 Types.unify(sub.a, sub.b);
359 } catch (UnificationException e) {
360 compilationContext.errorLog.log(sub.loc, "Unification of types failed.");
364 /*System.out.println("----");
365 for(Subsumption sub : subCopies)
366 System.out.println(sub.a.toString(tuc) + " === " + sub.b.toString(tuc));*/
369 for(Subsumption sub : subsumptions)
371 // FIXME This is not correct in all cases, should emit unsolved subsumptions to the type of the value
372 Types.unify(sub.a, sub.b);
373 } catch (UnificationException e) {
374 // Should not happen. Both types should be metavars.
375 throw new InternalCompilerError();
377 subsumptions.clear();
381 private boolean isEffect(Type type) {
382 if(type instanceof TMetaVar)
383 return ((TMetaVar)type).getKind() == Kinds.EFFECT;
384 else if(type instanceof TCon)
385 return environment.getTypeDescriptor((TCon)type).getKind() == Kinds.EFFECT;
386 else if(type instanceof TVar)
387 return ((TVar)type).getKind() == Kinds.EFFECT;
388 else if(type instanceof TUnion)
395 public void solveSubsumptions(long globalLoc) {
396 if(expandSubsumptions())
397 new SubSolver(compilationContext.errorLog, effectSubsumptions, potentialSingletonEffects, globalLoc).solve();
400 public void declareEffect(long loc, Type effect) {
401 subsumeEffect(loc, effect, effectUpperBounds.get(effectUpperBounds.size()-1));
404 public void pushEffectUpperBound(long loc, Type effect) {
405 effectUpperBounds.add(effect);
406 potentialSingletonEffects.add(effect);
409 public Type popEffectUpperBound() {
410 return effectUpperBounds.remove(effectUpperBounds.size()-1);
413 public ErrorLog getErrorLog() {
414 return compilationContext.errorLog;
417 public boolean isInPattern() {
421 public void setInPattern(boolean isInPattern) {
422 this.isInPattern = isInPattern;
425 public void pushConstraintFrame(Variable[] array) {
426 constraintFrames.add(array);
429 public void popConstraintFrame() {
430 constraintFrames.remove(constraintFrames.size()-1);
433 public void addConstraintDemand(EVariable var) {
434 for(int i=constraintFrames.size()-1;i>=0;--i)
435 for(Variable con : constraintFrames.get(i))
436 if(Types.equals(var.getType(), con.getType())) {
437 var.setVariable(con);
440 constraintDemand.add(var);
443 public Expression addConstraint(TPred pred) {
444 EVariable evidence = new EVariable(null);
445 evidence.setType(pred);
446 addConstraintDemand(evidence);
450 public Expression[] addConstraints(TPred[] preds) {
451 if(preds.length == 0)
452 return Expression.EMPTY_ARRAY;
453 Expression[] evidences = new Expression[preds.length];
454 for(int i=0;i<preds.length;++i)
455 evidences[i] = addConstraint(preds[i]);
459 public ArrayList<EVariable> getConstraintDemand() {
460 return constraintDemand;
463 public void resetConstraintDemand() {
464 constraintDemand = new ArrayList<EVariable>();
467 public void typeError(long loc, Type requiredType, Type givenType) {
468 TypeUnparsingContext tuc = new TypeUnparsingContext();
469 compilationContext.errorLog.log(loc, "Expected <" + requiredType.toString(tuc) + "> got <" + givenType.toString(tuc) + ">.");
472 public Expression solveConstraints(Environment environment, Expression expression) {
473 ArrayList<EVariable> constraintDemand = getConstraintDemand();
474 if(!constraintDemand.isEmpty()) {
475 ConstraintEnvironment ce = new ConstraintEnvironment(environment);
476 ReducedConstraints red = ConstraintSolver.solve(
477 ce, new ArrayList<TPred>(0), constraintDemand,
480 expression = ExpressionAugmentation.augmentSolved(
481 red.solvedConstraints,
484 for(Constraint c : red.unsolvedConstraints)
485 compilationContext.errorLog.log(c.getDemandLocation(), "There is no instance for <"+c.constraint+">.");
488 expression = expression.decomposeMatching();
493 public Environment getEnvironment() {
494 return compilationContext.environment;
497 public CompilationContext getCompilationContext() {
498 return compilationContext;