bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/elaboration/contexts/TypingContext.java

   1 package org.simantics.scl.compiler.elaboration.contexts;
   2
   3 import java.util.ArrayList;
   4
   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;
  39
  40 import gnu.trove.map.hash.THashMap;
  41 import gnu.trove.set.hash.THashSet;
  42
  43 public class TypingContext {
  44
  45     private CompilationContext compilationContext;
  46
  47     // Subsumption
  48     private ArrayList<Subsumption> effectSubsumptions = new ArrayList<Subsumption>();
  49     private ArrayList<Subsumption> subsumptions = new ArrayList<Subsumption>();
  50     private ArrayList<Type> potentialSingletonEffects = new ArrayList<Type>();
  51
  52     // Effects
  53     private ArrayList<Type> effectUpperBounds = new ArrayList<Type>();
  54
  55     // Constraints
  56     private ArrayList<EVariable> constraintDemand = new ArrayList<EVariable>();
  57     private ArrayList<Variable[]> constraintFrames = new ArrayList<Variable[]>();
  58
  59     // Patterns
  60     private boolean isInPattern;
  61
  62     // Recursion
  63     public THashSet<SCLValue> recursiveValues;
  64     public ArrayList<EPlaceholder> recursiveReferences;
  65
  66     // Overloading
  67     public ArrayList<EAmbiguous> overloadedExpressions = new ArrayList<EAmbiguous>();
  68
  69     //TypeUnparsingContext tuc = new TypeUnparsingContext();
  70
  71     Environment environment;
  72
  73     public TypingContext(CompilationContext compilationContext) {
  74         this.compilationContext = compilationContext;
  75         this.environment = compilationContext.environment;
  76     }
  77
  78     /**
  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}
  81      * are allowed.
  82      */
  83     public void subsumeEffect(long loc, Type a, Type b) {
  84         a = Types.canonical(a);
  85         if(a == Types.NO_EFFECTS)
  86             return;
  87         b = Types.canonical(b);
  88         if(a == b)
  89             return;
  90         if(b == Types.NO_EFFECTS) {
  91             try {
  92                 Types.unify(a, Types.NO_EFFECTS);
  93             } catch(UnificationException e) {
  94                 compilationContext.errorLog.log(loc, "No side-effects allowed here.");
  95                 return;
  96             }
  97         }
  98
  99         //System.out.println("subsumeEffect(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
 100
 101         /*if(a instanceof TUnion) {
 102             TUnion union = (TUnion)a;
 103             for(Type e : union.effects)
 104                 subsumeEffect(loc, e, b);
 105         }
 106         else*/
 107         effectSubsumptions.add(new Subsumption(loc, a, b));
 108     }
 109
 110     public void subsume(long loc, Type a, Type b) throws UnificationException {
 111         a = Types.canonical(a);
 112         b = Types.canonical(b);
 113         if(a == b)
 114             return;
 115
 116         //System.out.println("subsume(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
 117
 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));
 123             }
 124             else {
 125                 if(b.contains(aVar))
 126                     throw new UnificationException(a, b);
 127                 aVar.setRef(createSubtypeTemplate(loc, b));
 128             }
 129             return;
 130         }
 131         else if(b instanceof TMetaVar) {
 132             TMetaVar bVar = (TMetaVar)b;
 133             if(a.contains(bVar))
 134                 throw new UnificationException(a, b);
 135             bVar.setRef(createSupertypeTemplate(loc, a));
 136             return;
 137         }
 138         if(a instanceof TFun) {
 139             if(!(b instanceof TFun))
 140                 throw new UnificationException(a, b);
 141             TFun aFun = (TFun)a;
 142             TFun bFun = (TFun)b;
 143             subsume(loc, bFun.domain, aFun.domain);
 144             subsumeEffect(loc, aFun.effect, bFun.effect);
 145             subsume(loc, aFun.range, bFun.range);
 146         }
 147         else if(a instanceof TApply) {
 148             Types.unify(a, b);
 149         }
 150         else if(a instanceof TPred) {
 151             Types.unify(a, b);
 152         }
 153         else // a instanceof TUnion
 154             throw new UnificationException(a, b);
 155     }
 156
 157     /**
 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.
 161      */
 162     private Type createSubtypeTemplate(long loc, Type type) {
 163         type = Types.canonical(type);
 164         if(type instanceof TCon)
 165             return type;
 166         else if(type instanceof TApply)
 167             return type;
 168         else if(type instanceof TPred)
 169             return type;
 170         else if(type instanceof TFun) {
 171             TFun fun = (TFun)type;
 172             Type funEffect = Types.canonical(fun.effect);
 173             Type effect;
 174             if(funEffect == Types.NO_EFFECTS)
 175                 effect = Types.NO_EFFECTS;
 176             else {
 177                 effect = Types.metaVar(Kinds.EFFECT);
 178                 effectSubsumptions.add(new Subsumption(loc, effect, funEffect));
 179             }
 180             return Types.functionE(
 181                     createSupertypeTemplate(loc, fun.domain),
 182                     effect,
 183                     createSubtypeTemplate(loc, fun.range));
 184         }
 185         else if(type instanceof TMetaVar) {
 186             TMetaVar var = (TMetaVar)type;
 187             TMetaVar newVar = Types.metaVar(var.getKind());
 188             try {
 189                 newVar.setSkeletonRef(var);
 190             } catch (UnificationException e) {
 191                 throw new InternalCompilerError(loc, e);
 192             }
 193             subsumptions.add(new Subsumption(loc, newVar, var));
 194             return newVar;
 195         }
 196         else if(type instanceof TVar)
 197             return type;
 198         else if(type instanceof TUnion) {
 199             TUnion union = (TUnion)type;
 200             if(union.isMinimal())
 201                 return type;
 202             TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
 203             subsumptions.add(new Subsumption(loc, newVar, type));
 204             return newVar;
 205         }
 206         else if(type instanceof TForAll) {
 207             TForAll forAll = (TForAll)type;
 208             Type t = createSubtypeTemplate(loc, forAll.type);
 209             if(t == forAll.type)
 210                 return type;
 211             else
 212                 return Types.forAll(forAll.var, t);
 213         }
 214         else
 215             throw new InternalCompilerError("Unsupported type " + type + ".");
 216     }
 217
 218     /**
 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.
 222      */
 223     private Type createSupertypeTemplate(long loc, Type type) {
 224         type = Types.canonical(type);
 225         if(type instanceof TCon)
 226             return type;
 227         else if(type instanceof TApply)
 228             return type;
 229         else if(type instanceof TPred)
 230             return type;
 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),
 237                     effect,
 238                     createSupertypeTemplate(loc, fun.range));
 239         }
 240         else if(type instanceof TMetaVar) {
 241             TMetaVar var = (TMetaVar)type;
 242             TMetaVar newVar = Types.metaVar(var.getKind());
 243             try {
 244                 newVar.setSkeletonRef(var);
 245             } catch (UnificationException e) {
 246                 throw new InternalCompilerError(loc, e);
 247             }
 248             subsumptions.add(new Subsumption(loc, var, newVar));
 249             return newVar;
 250         }
 251         else if(type instanceof TVar)
 252             return type;
 253         else if(type instanceof TUnion) {
 254             TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
 255             subsumptions.add(new Subsumption(loc, type, newVar));
 256             return newVar;
 257         }
 258         else if(type instanceof TForAll) {
 259             TForAll forAll = (TForAll)type;
 260             Type t = createSupertypeTemplate(loc, forAll.type);
 261             if(t == forAll.type)
 262                 return type;
 263             else
 264                 return Types.forAll(forAll.var, t);
 265         }
 266         else
 267             throw new InternalCompilerError("Unsupported type " + type + ".");
 268     }
 269
 270     /**
 271      * Instantiates type abstractions and constraints from the value.
 272      */
 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);
 281         }
 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;
 286                 type = fun.range;
 287
 288                 long loc = expr.getLocation();
 289                 EVariable var = new EVariable(loc, null);
 290                 var.setType(pred);
 291                 expr = new EApply(loc, expr, var);
 292                 addConstraintDemand(var);
 293             }
 294             else if(fun.domain == Types.PUNIT) {
 295                 type = fun.range;
 296
 297                 long loc = expr.getLocation();
 298                 declareEffect(expr.location, fun.effect);
 299                 expr = new EApply(loc, fun.effect, expr, new ELiteral(loc, NoRepConstant.PUNIT));
 300             }
 301             else
 302                 break;
 303         }
 304         expr.setType(type);
 305         return expr;
 306     }
 307
 308     /**
 309      * Enforces {@code expr} to have type {@code b} by adding
 310      * type applications, lambdas and effect subsumptions.
 311      */
 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));
 320         }*/
 321         expr = instantiate(expr);
 322
 323         try {
 324             subsume(expr.getLocation(), expr.getType(), b);
 325         } catch(UnificationException e) {
 326             typeError(expr.getLocation(), b, expr.getType());
 327         }
 328         return expr;
 329     }
 330
 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);
 343                 }
 344                 else {
 345                     try {
 346                         subsume(sub.loc, a, b);
 347                     } catch (UnificationException e) {
 348                         compilationContext.errorLog.log(sub.loc, "Type " + a + " is not a subtype of " + b + ".");
 349                     }
 350                     nontrivialSubs = true;
 351                 }
 352             }
 353             ++iterationCount;
 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)
 360                     if(!isEffect(sub.a))
 361                         subCopies.add(new Subsumption(sub.loc,
 362                                 sub.a.copySkeleton(metaVarMap), sub.b.copySkeleton(metaVarMap)));
 363
 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));*/
 368
 369                 for(Subsumption sub : subCopies)
 370                     try {
 371                         Types.unify(sub.a, sub.b);
 372                     } catch (UnificationException e) {
 373                         compilationContext.errorLog.log(sub.loc, "Unification of types failed.");
 374                         return false;
 375                     }
 376
 377                 /*System.out.println("----");
 378                 for(Subsumption sub : subCopies)
 379                     System.out.println(sub.a.toString(tuc) + " === " + sub.b.toString(tuc));*/
 380             }
 381         }
 382         for(Subsumption sub : subsumptions)
 383             try {
 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);
 389             }
 390         subsumptions.clear();
 391         return true;
 392     }
 393
 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)
 402             return true;
 403         else
 404             return false;
 405
 406     }
 407
 408     public void solveSubsumptions(long globalLoc) {
 409         if(expandSubsumptions())
 410             new SubSolver(compilationContext.errorLog, effectSubsumptions, potentialSingletonEffects, globalLoc).solve();
 411     }
 412
 413     public void declareEffect(long loc, Type effect) {
 414         subsumeEffect(loc, effect, effectUpperBounds.get(effectUpperBounds.size()-1));
 415     }
 416
 417     public void pushEffectUpperBound(long loc, Type effect) {
 418         effectUpperBounds.add(effect);
 419         potentialSingletonEffects.add(effect);
 420     }
 421
 422     public Type popEffectUpperBound() {
 423         return effectUpperBounds.remove(effectUpperBounds.size()-1);
 424     }
 425
 426     public ErrorLog getErrorLog() {
 427         return compilationContext.errorLog;
 428     }
 429
 430     public boolean isInPattern() {
 431         return isInPattern;
 432     }
 433
 434     public void setInPattern(boolean isInPattern) {
 435         this.isInPattern = isInPattern;
 436     }
 437
 438     public void pushConstraintFrame(Variable[] array) {
 439         constraintFrames.add(array);
 440     }
 441
 442     public void popConstraintFrame() {
 443         constraintFrames.remove(constraintFrames.size()-1);
 444     }
 445
 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);
 451                     return;
 452                 }
 453         constraintDemand.add(var);
 454     }
 455
 456     public Expression addConstraint(TPred pred) {
 457         EVariable evidence = new EVariable(null);
 458         evidence.setType(pred);
 459         addConstraintDemand(evidence);
 460         return evidence;
 461     }
 462
 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]);
 469         return evidences;
 470     }
 471
 472     public ArrayList<EVariable> getConstraintDemand() {
 473         return constraintDemand;
 474     }
 475
 476     public void resetConstraintDemand() {
 477         constraintDemand = new ArrayList<EVariable>();
 478     }
 479
 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) + ">.");
 483     }
 484
 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,
 491                     true);
 492
 493             expression = ExpressionAugmentation.augmentSolved(
 494                     red.solvedConstraints,
 495                     expression);
 496
 497             for(Constraint c : red.unsolvedConstraints)
 498                 compilationContext.errorLog.log(c.getDemandLocation(), "There is no instance for <"+c.constraint+">.");
 499         }
 500         else
 501             expression = expression.decomposeMatching();
 502
 503         return expression;
 504     }
 505
 506     public Environment getEnvironment() {
 507         return compilationContext.environment;
 508     }
 509
 510     public CompilationContext getCompilationContext() {
 511         return compilationContext;
 512     }
 513
 514 }