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