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.common.names.Name;
   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.EConstant;
  11 import org.simantics.scl.compiler.elaboration.expressions.EError;
  12 import org.simantics.scl.compiler.elaboration.expressions.ELiteral;
  13 import org.simantics.scl.compiler.elaboration.expressions.EPlaceholder;
  14 import org.simantics.scl.compiler.elaboration.expressions.EVariable;
  15 import org.simantics.scl.compiler.elaboration.expressions.Expression;
  16 import org.simantics.scl.compiler.elaboration.expressions.Variable;
  17 import org.simantics.scl.compiler.elaboration.modules.SCLValue;
  18 import org.simantics.scl.compiler.environment.Environment;
  19 import org.simantics.scl.compiler.errors.ErrorLog;
  20 import org.simantics.scl.compiler.errors.Locations;
  21 import org.simantics.scl.compiler.internal.elaboration.constraints.Constraint;
  22 import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintEnvironment;
  23 import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintSolver;
  24 import org.simantics.scl.compiler.internal.elaboration.constraints.ExpressionAugmentation;
  25 import org.simantics.scl.compiler.internal.elaboration.constraints.ReducedConstraints;
  26 import org.simantics.scl.compiler.internal.elaboration.subsumption.SubSolver;
  27 import org.simantics.scl.compiler.internal.elaboration.subsumption.Subsumption;
  28 import org.simantics.scl.compiler.types.TApply;
  29 import org.simantics.scl.compiler.types.TCon;
  30 import org.simantics.scl.compiler.types.TForAll;
  31 import org.simantics.scl.compiler.types.TFun;
  32 import org.simantics.scl.compiler.types.TMetaVar;
  33 import org.simantics.scl.compiler.types.TPred;
  34 import org.simantics.scl.compiler.types.TUnion;
  35 import org.simantics.scl.compiler.types.TVar;
  36 import org.simantics.scl.compiler.types.Type;
  37 import org.simantics.scl.compiler.types.Types;
  38 import org.simantics.scl.compiler.types.exceptions.UnificationException;
  39 import org.simantics.scl.compiler.types.kinds.Kinds;
  40 import org.simantics.scl.compiler.types.util.TypeUnparsingContext;
  41
  42 import gnu.trove.map.hash.THashMap;
  43 import gnu.trove.set.hash.THashSet;
  44
  45 public class TypingContext implements EnvironmentalContext {
  46
  47     private ErrorLog errorLog;
  48
  49     // Subsumption
  50     private ArrayList<Subsumption> effectSubsumptions = new ArrayList<Subsumption>();
  51     private ArrayList<Subsumption> subsumptions = new ArrayList<Subsumption>();
  52     private ArrayList<Type> potentialSingletonEffects = new ArrayList<Type>();
  53
  54     // Effects
  55     private ArrayList<Type> effectUpperBounds = new ArrayList<Type>();
  56
  57     // Constraints
  58     private ArrayList<EVariable> constraintDemand = new ArrayList<EVariable>();
  59     private ArrayList<Variable[]> constraintFrames = new ArrayList<Variable[]>();
  60
  61     // Patterns
  62     private boolean isInPattern;
  63
  64     // Recursion
  65     public THashSet<SCLValue> recursiveValues;
  66     public ArrayList<EPlaceholder> recursiveReferences;
  67
  68     // Overloading
  69     public ArrayList<EAmbiguous> overloadedExpressions = new ArrayList<EAmbiguous>();
  70
  71     //TypeUnparsingContext tuc = new TypeUnparsingContext();
  72
  73     Environment environment;
  74     THashMap<Name, SCLValue> constants = new THashMap<Name, SCLValue>();
  75
  76     public TypingContext(ErrorLog errorLog, Environment environment) {
  77         this.errorLog = errorLog;
  78         this.environment = environment;
  79     }
  80
  81     /**
  82      * Records the fact that {@code a} should be a subeffect
  83      * of {@code b}. Only types {@code TMetaVar}, {@code TVar}, {@code TCon}, {@code TUnion}
  84      * are allowed.
  85      */
  86     public void subsumeEffect(long loc, Type a, Type b) {
  87         a = Types.canonical(a);
  88         if(a == Types.NO_EFFECTS)
  89             return;
  90         b = Types.canonical(b);
  91         if(a == b)
  92             return;
  93         if(b == Types.NO_EFFECTS) {
  94             try {
  95                 Types.unify(a, Types.NO_EFFECTS);
  96             } catch(UnificationException e) {
  97                 errorLog.log(loc, "No side-effects allowed here.");
  98                 return;
  99             }
 100         }
 101
 102         //System.out.println("subsumeEffect(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
 103
 104         /*if(a instanceof TUnion) {
 105             TUnion union = (TUnion)a;
 106             for(Type e : union.effects)
 107                 subsumeEffect(loc, e, b);
 108         }
 109         else*/
 110         effectSubsumptions.add(new Subsumption(loc, a, b));
 111     }
 112
 113     public void subsume(long loc, Type a, Type b) throws UnificationException {
 114         a = Types.canonical(a);
 115         b = Types.canonical(b);
 116         if(a == b)
 117             return;
 118
 119         //System.out.println("subsume(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
 120
 121         if(a instanceof TMetaVar) {
 122             TMetaVar aVar = (TMetaVar)a;
 123             if(b instanceof TMetaVar)
 124                 subsumptions.add(new Subsumption(loc, a, b));
 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             subsumptions.add(new Subsumption(loc, newVar, var));
 190             return newVar;
 191         }
 192         else if(type instanceof TVar)
 193             return type;
 194         else if(type instanceof TUnion) {
 195             TUnion union = (TUnion)type;
 196             if(union.isMinimal())
 197                 return type;
 198             TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
 199             subsumptions.add(new Subsumption(loc, newVar, type));
 200             return newVar;
 201         }
 202         else if(type instanceof TForAll) {
 203             TForAll forAll = (TForAll)type;
 204             Type t = createSubtypeTemplate(loc, forAll.type);
 205             if(t == forAll.type)
 206                 return type;
 207             else
 208                 return Types.forAll(forAll.var, t);
 209         }
 210         else
 211             throw new InternalCompilerError("Unsupported type " + type + ".");
 212     }
 213
 214     /**
 215      * Creates a template for all supertypes of the given type
 216      * where all possible varying types are replaced by metavars
 217      * with properly set inequalities.
 218      */
 219     private Type createSupertypeTemplate(long loc, Type type) {
 220         type = Types.canonical(type);
 221         if(type instanceof TCon)
 222             return type;
 223         else if(type instanceof TApply)
 224             return type;
 225         else if(type instanceof TPred)
 226             return type;
 227         else if(type instanceof TFun) {
 228             TFun fun = (TFun)type;
 229             TMetaVar effect = Types.metaVar(Kinds.EFFECT);
 230             effectSubsumptions.add(new Subsumption(loc, fun.effect, effect));
 231             return Types.functionE(
 232                     createSubtypeTemplate(loc, fun.domain),
 233                     effect,
 234                     createSupertypeTemplate(loc, fun.range));
 235         }
 236         else if(type instanceof TMetaVar) {
 237             TMetaVar var = (TMetaVar)type;
 238             TMetaVar newVar = Types.metaVar(var.getKind());
 239             subsumptions.add(new Subsumption(loc, var, newVar));
 240             return newVar;
 241         }
 242         else if(type instanceof TVar)
 243             return type;
 244         else if(type instanceof TUnion) {
 245             TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
 246             subsumptions.add(new Subsumption(loc, type, newVar));
 247             return newVar;
 248         }
 249         else if(type instanceof TForAll) {
 250             TForAll forAll = (TForAll)type;
 251             Type t = createSupertypeTemplate(loc, forAll.type);
 252             if(t == forAll.type)
 253                 return type;
 254             else
 255                 return Types.forAll(forAll.var, t);
 256         }
 257         else
 258             throw new InternalCompilerError("Unsupported type " + type + ".");
 259     }
 260
 261     /**
 262      * Instantiates type abstractions and constraints from the value.
 263      */
 264     public Expression instantiate(Expression expr) {
 265         Type type = Types.canonical(expr.getType());
 266         while(type instanceof TForAll) {
 267             TForAll forAll = (TForAll)type;
 268             TVar var = forAll.var;
 269             TMetaVar mVar = Types.metaVar(var.getKind());
 270             type = Types.canonical(forAll.type).replace(var, mVar);
 271             expr = expr.applyType(mVar);
 272         }
 273         while(type instanceof TFun) {
 274             TFun fun = (TFun)type;
 275             if(fun.domain instanceof TPred) { // No need to canonicalize
 276                 TPred pred = (TPred)fun.domain;
 277                 type = fun.range;
 278
 279                 long loc = expr.getLocation();
 280                 EVariable var = new EVariable(loc, null);
 281                 var.setType(pred);
 282                 expr = new EApply(loc, expr, var);
 283                 addConstraintDemand(var);
 284             }
 285             else if(fun.domain == Types.PUNIT) {
 286                 type = fun.range;
 287
 288                 long loc = expr.getLocation();
 289                 declareEffect(expr.location, fun.effect);
 290                 expr = new EApply(loc, fun.effect, expr, new ELiteral(loc, NoRepConstant.PUNIT));
 291             }
 292             else
 293                 break;
 294         }
 295         expr.setType(type);
 296         return expr;
 297     }
 298
 299     /**
 300      * Enforces {@code expr} to have type {@code b} by adding
 301      * type applications, lambdas and effect subsumptions.
 302      */
 303     public Expression subsume(Expression expr, Type b) {
 304         b = Types.canonical(b);
 305         /*if(b instanceof TForAll) {
 306             TForAll forAll = (TForAll)b;
 307             TVar var = forAll.var;
 308             TVar newVar = Types.var(var.getKind());
 309             b = Types.canonical(forAll.type).replace(var, newVar);
 310             return new ELambdaType(new TVar[] {newVar}, subsume(expr, b));
 311         }*/
 312         expr = instantiate(expr);
 313
 314         try {
 315             subsume(expr.getLocation(), expr.getType(), b);
 316         } catch(UnificationException e) {
 317             typeError(expr.getLocation(), b, expr.getType());
 318         }
 319         return expr;
 320     }
 321
 322     private boolean expandSubsumptions() {
 323         boolean nontrivialSubs = true;
 324         int iterationCount = 0;
 325         while(!subsumptions.isEmpty() && nontrivialSubs) {
 326             ArrayList<Subsumption> oldSubsumptions = subsumptions;
 327             subsumptions = new ArrayList<Subsumption>();
 328             nontrivialSubs = false;
 329             for(Subsumption sub : oldSubsumptions) {
 330                 Type a = sub.a = Types.canonical(sub.a);
 331                 Type b = sub.b = Types.canonical(sub.b);
 332                 if(b instanceof TMetaVar && a instanceof TMetaVar) {
 333                     subsumptions.add(sub);
 334                 }
 335                 else {
 336                     try {
 337                         subsume(sub.loc, a, b);
 338                     } catch (UnificationException e) {
 339                         errorLog.log(sub.loc, "Type " + a + " is not a subtype of " + b + ".");
 340                     }
 341                     nontrivialSubs = true;
 342                 }
 343             }
 344             ++iterationCount;
 345             if(iterationCount == 5) {
 346                 // Test that the skeletons are unifiable
 347                 THashMap<TMetaVar,TMetaVar> metaVarMap =
 348                         new THashMap<TMetaVar,TMetaVar>();
 349                 ArrayList<Subsumption> subCopies = new ArrayList<Subsumption>(subsumptions.size());
 350                 for(Subsumption sub : subsumptions)
 351                     if(!isEffect(sub.a))
 352                         subCopies.add(new Subsumption(sub.loc,
 353                                 sub.a.copySkeleton(metaVarMap), sub.b.copySkeleton(metaVarMap)));
 354
 355                 /*System.out.println("----");
 356                 TypeUnparsingContext tuc = new TypeUnparsingContext();
 357                 for(Subsumption sub : subCopies)
 358                     System.out.println(sub.a.toString(tuc) + " == " + sub.b.toString(tuc));*/
 359
 360                 for(Subsumption sub : subCopies)
 361                     try {
 362                         Types.unify(sub.a, sub.b);
 363                     } catch (UnificationException e) {
 364                         errorLog.log(sub.loc, "Unification of types failed.");
 365                         return false;
 366                     }
 367
 368                 /*System.out.println("----");
 369                 for(Subsumption sub : subCopies)
 370                     System.out.println(sub.a.toString(tuc) + " === " + sub.b.toString(tuc));*/
 371             }
 372         }
 373         for(Subsumption sub : subsumptions)
 374             try {
 375                 // FIXME This is not correct in all cases, should emit unsolved subsumptions to the type of the value
 376                 Types.unify(sub.a, sub.b);
 377             } catch (UnificationException e) {
 378                 // Should not happen. Both types should be metavars.
 379                 throw new InternalCompilerError();
 380             }
 381         subsumptions.clear();
 382         return true;
 383     }
 384
 385     private boolean isEffect(Type type) {
 386         if(type instanceof TMetaVar)
 387             return ((TMetaVar)type).getKind() == Kinds.EFFECT;
 388         else if(type instanceof TCon)
 389             return environment.getTypeConstructor((TCon)type).kind == Kinds.EFFECT;
 390         else if(type instanceof TVar)
 391             return ((TVar)type).getKind() == Kinds.EFFECT;
 392         else if(type instanceof TUnion)
 393             return true;
 394         else
 395             return false;
 396
 397     }
 398
 399     public void solveSubsumptions(long globalLoc) {
 400         if(expandSubsumptions())
 401             new SubSolver(errorLog, effectSubsumptions, potentialSingletonEffects, globalLoc).solve();
 402     }
 403
 404     public void declareEffect(long loc, Type effect) {
 405         subsumeEffect(loc, effect, effectUpperBounds.get(effectUpperBounds.size()-1));
 406     }
 407
 408     public void pushEffectUpperBound(long loc, Type effect) {
 409         effectUpperBounds.add(effect);
 410         potentialSingletonEffects.add(effect);
 411     }
 412
 413     public Type popEffectUpperBound() {
 414         return effectUpperBounds.remove(effectUpperBounds.size()-1);
 415     }
 416
 417     public ErrorLog getErrorLog() {
 418         return errorLog;
 419     }
 420
 421     public boolean isInPattern() {
 422         return isInPattern;
 423     }
 424
 425     public void setInPattern(boolean isInPattern) {
 426         this.isInPattern = isInPattern;
 427     }
 428
 429     public void pushConstraintFrame(Variable[] array) {
 430         constraintFrames.add(array);
 431     }
 432
 433     public void popConstraintFrame() {
 434         constraintFrames.remove(constraintFrames.size()-1);
 435     }
 436
 437     public void addConstraintDemand(EVariable var) {
 438         for(int i=constraintFrames.size()-1;i>=0;--i)
 439             for(Variable con : constraintFrames.get(i))
 440                 if(Types.equals(var.getType(), con.getType())) {
 441                     var.setVariable(con);
 442                     return;
 443                 }
 444         constraintDemand.add(var);
 445     }
 446
 447     public Expression addConstraint(TPred pred) {
 448         EVariable evidence = new EVariable(null);
 449         evidence.setType(pred);
 450         addConstraintDemand(evidence);
 451         return evidence;
 452     }
 453
 454     public Expression[] addConstraints(TPred[] preds) {
 455         if(preds.length == 0)
 456             return Expression.EMPTY_ARRAY;
 457         Expression[] evidences = new Expression[preds.length];
 458         for(int i=0;i<preds.length;++i)
 459             evidences[i] = addConstraint(preds[i]);
 460         return evidences;
 461     }
 462
 463     public ArrayList<EVariable> getConstraintDemand() {
 464         return constraintDemand;
 465     }
 466
 467     public void resetConstraintDemand() {
 468         constraintDemand = new ArrayList<EVariable>();
 469     }
 470
 471     public void typeError(long loc, Type requiredType, Type givenType) {
 472         TypeUnparsingContext tuc = new TypeUnparsingContext();
 473         errorLog.log(loc, "Expected <" + requiredType.toString(tuc) + "> got <" + givenType.toString(tuc) + ">.");
 474     }
 475
 476     public Expression solveConstraints(Environment environment, Expression expression) {
 477         ArrayList<EVariable> constraintDemand = getConstraintDemand();
 478         if(!constraintDemand.isEmpty()) {
 479             ConstraintEnvironment ce = new ConstraintEnvironment(environment);
 480             ReducedConstraints red = ConstraintSolver.solve(
 481                     ce, new ArrayList<TPred>(0), constraintDemand,
 482                     true);
 483
 484             expression = ExpressionAugmentation.augmentSolved(
 485                     red.solvedConstraints,
 486                     expression);
 487
 488             for(Constraint c : red.unsolvedConstraints)
 489                 errorLog.log(c.getDemandLocation(), "There is no instance for <"+c.constraint+">.");
 490         }
 491         else
 492             expression = expression.decomposeMatching();
 493
 494         return expression;
 495     }
 496
 497     public SCLValue getValue(Name name) {
 498         if(constants.containsKey(name))
 499             return constants.get(name);
 500         SCLValue value = environment.getValue(name);
 501         if(value == null)
 502             errorLog.log(Locations.NO_LOCATION, "Couldn't find " + name + ".");
 503         constants.put(name, value);
 504         return value;
 505     }
 506
 507     public Expression getConstant(Name name, Type ... typeParameters) {
 508         SCLValue value = getValue(name);
 509         if(value == null)
 510             return new EError(Locations.NO_LOCATION);
 511         return new EConstant(value, typeParameters);
 512     }
 513
 514     public Environment getEnvironment() {
 515         return environment;
 516     }
 517
 518 }