gerrit.simantics Code Review - simantics/platform.git/blob

   1 package org.simantics.scl.compiler.elaboration.contexts;
   2
   3 import gnu.trove.map.hash.THashMap;
   4 import gnu.trove.set.hash.THashSet;
   5
   6 import java.util.ArrayList;
   7
   8 import org.simantics.scl.compiler.common.exceptions.InternalCompilerError;
   9 import org.simantics.scl.compiler.common.names.Name;
  10 import org.simantics.scl.compiler.constants.NoRepConstant;
  11 import org.simantics.scl.compiler.elaboration.expressions.EApply;
  12 import org.simantics.scl.compiler.elaboration.expressions.EConstant;
  13 import org.simantics.scl.compiler.elaboration.expressions.EError;
  14 import org.simantics.scl.compiler.elaboration.expressions.ELiteral;
  15 import org.simantics.scl.compiler.elaboration.expressions.EPlaceholder;
  16 import org.simantics.scl.compiler.elaboration.expressions.EVariable;
  17 import org.simantics.scl.compiler.elaboration.expressions.Expression;
  18 import org.simantics.scl.compiler.elaboration.expressions.Variable;
  19 import org.simantics.scl.compiler.elaboration.modules.SCLValue;
  20 import org.simantics.scl.compiler.environment.Environment;
  21 import org.simantics.scl.compiler.errors.ErrorLog;
  22 import org.simantics.scl.compiler.errors.Locations;
  23 import org.simantics.scl.compiler.internal.elaboration.constraints.Constraint;
  24 import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintEnvironment;
  25 import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintSolver;
  26 import org.simantics.scl.compiler.internal.elaboration.constraints.ExpressionAugmentation;
  27 import org.simantics.scl.compiler.internal.elaboration.constraints.ReducedConstraints;
  28 import org.simantics.scl.compiler.internal.elaboration.subsumption.SubSolver;
  29 import org.simantics.scl.compiler.internal.elaboration.subsumption.Subsumption;
  30 import org.simantics.scl.compiler.types.TApply;
  31 import org.simantics.scl.compiler.types.TCon;
  32 import org.simantics.scl.compiler.types.TForAll;
  33 import org.simantics.scl.compiler.types.TFun;
  34 import org.simantics.scl.compiler.types.TMetaVar;
  35 import org.simantics.scl.compiler.types.TPred;
  36 import org.simantics.scl.compiler.types.TUnion;
  37 import org.simantics.scl.compiler.types.TVar;
  38 import org.simantics.scl.compiler.types.Type;
  39 import org.simantics.scl.compiler.types.Types;
  40 import org.simantics.scl.compiler.types.exceptions.UnificationException;
  41 import org.simantics.scl.compiler.types.kinds.Kinds;
  42 import org.simantics.scl.compiler.types.util.TypeUnparsingContext;
  43
  44 public class TypingContext implements EnvironmentalContext {
  45
  46     private ErrorLog errorLog;
  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     //TypeUnparsingContext tuc = new TypeUnparsingContext();
  68
  69     Environment environment;
  70     THashMap<Name, SCLValue> constants = new THashMap<Name, SCLValue>();
  71
  72     public TypingContext(ErrorLog errorLog, Environment environment) {
  73         this.errorLog = errorLog;
  74         this.environment = environment;
  75     }
  76
  77     /**
  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}
  80      * are allowed.
  81      */
  82     public void subsumeEffect(long loc, Type a, Type b) {
  83         a = Types.canonical(a);
  84         if(a == Types.NO_EFFECTS)
  85             return;
  86         b = Types.canonical(b);
  87         if(a == b)
  88             return;
  89         if(b == Types.NO_EFFECTS) {
  90             try {
  91                 Types.unify(a, Types.NO_EFFECTS);
  92             } catch(UnificationException e) {
  93                 errorLog.log(loc, "No side-effects allowed here.");
  94                 return;
  95             }
  96         }
  97
  98         //System.out.println("subsumeEffect(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
  99
 100         /*if(a instanceof TUnion) {
 101             TUnion union = (TUnion)a;
 102             for(Type e : union.effects)
 103                 subsumeEffect(loc, e, b);
 104         }
 105         else*/
 106         effectSubsumptions.add(new Subsumption(loc, a, b));
 107     }
 108
 109     public void subsume(long loc, Type a, Type b) throws UnificationException {
 110         a = Types.canonical(a);
 111         b = Types.canonical(b);
 112         if(a == b)
 113             return;
 114
 115         //System.out.println("subsume(" + a.toString(tuc) + ", " + b.toString(tuc) + ")");
 116
 117         if(a instanceof TMetaVar) {
 118             TMetaVar aVar = (TMetaVar)a;
 119             if(b instanceof TMetaVar)
 120                 subsumptions.add(new Subsumption(loc, a, b));
 121             else {
 122                 if(b.contains(aVar))
 123                     throw new UnificationException(a, b);
 124                 aVar.setRef(createSubtypeTemplate(loc, b));
 125             }
 126             return;
 127         }
 128         else if(b instanceof TMetaVar) {
 129             TMetaVar bVar = (TMetaVar)b;
 130             if(a.contains(bVar))
 131                 throw new UnificationException(a, b);
 132             bVar.setRef(createSupertypeTemplate(loc, a));
 133             return;
 134         }
 135         if(a instanceof TFun) {
 136             if(!(b instanceof TFun))
 137                 throw new UnificationException(a, b);
 138             TFun aFun = (TFun)a;
 139             TFun bFun = (TFun)b;
 140             subsume(loc, bFun.domain, aFun.domain);
 141             subsumeEffect(loc, aFun.effect, bFun.effect);
 142             subsume(loc, aFun.range, bFun.range);
 143         }
 144         else if(a instanceof TApply) {
 145             Types.unify(a, b);
 146         }
 147         else if(a instanceof TPred) {
 148             Types.unify(a, b);
 149         }
 150         else // a instanceof TUnion
 151             throw new UnificationException(a, b);
 152     }
 153
 154     /**
 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.
 158      */
 159     private Type createSubtypeTemplate(long loc, Type type) {
 160         type = Types.canonical(type);
 161         if(type instanceof TCon)
 162             return type;
 163         else if(type instanceof TApply)
 164             return type;
 165         else if(type instanceof TPred)
 166             return type;
 167         else if(type instanceof TFun) {
 168             TFun fun = (TFun)type;
 169             Type funEffect = Types.canonical(fun.effect);
 170             Type effect;
 171             if(funEffect == Types.NO_EFFECTS)
 172                 effect = Types.NO_EFFECTS;
 173             else {
 174                 effect = Types.metaVar(Kinds.EFFECT);
 175                 effectSubsumptions.add(new Subsumption(loc, effect, funEffect));
 176             }
 177             return Types.functionE(
 178                     createSupertypeTemplate(loc, fun.domain),
 179                     effect,
 180                     createSubtypeTemplate(loc, fun.range));
 181         }
 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));
 186             return newVar;
 187         }
 188         else if(type instanceof TVar)
 189             return type;
 190         else if(type instanceof TUnion) {
 191             TUnion union = (TUnion)type;
 192             if(union.isMinimal())
 193                 return type;
 194             TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
 195             subsumptions.add(new Subsumption(loc, newVar, type));
 196             return newVar;
 197         }
 198         else if(type instanceof TForAll) {
 199             TForAll forAll = (TForAll)type;
 200             Type t = createSubtypeTemplate(loc, forAll.type);
 201             if(t == forAll.type)
 202                 return type;
 203             else
 204                 return Types.forAll(forAll.var, t);
 205         }
 206         else
 207             throw new InternalCompilerError("Unsupported type " + type + ".");
 208     }
 209
 210     /**
 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.
 214      */
 215     private Type createSupertypeTemplate(long loc, Type type) {
 216         type = Types.canonical(type);
 217         if(type instanceof TCon)
 218             return type;
 219         else if(type instanceof TApply)
 220             return type;
 221         else if(type instanceof TPred)
 222             return type;
 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),
 229                     effect,
 230                     createSupertypeTemplate(loc, fun.range));
 231         }
 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));
 236             return newVar;
 237         }
 238         else if(type instanceof TVar)
 239             return type;
 240         else if(type instanceof TUnion) {
 241             TMetaVar newVar = Types.metaVar(Kinds.EFFECT);
 242             subsumptions.add(new Subsumption(loc, type, newVar));
 243             return newVar;
 244         }
 245         else if(type instanceof TForAll) {
 246             TForAll forAll = (TForAll)type;
 247             Type t = createSupertypeTemplate(loc, forAll.type);
 248             if(t == forAll.type)
 249                 return type;
 250             else
 251                 return Types.forAll(forAll.var, t);
 252         }
 253         else
 254             throw new InternalCompilerError("Unsupported type " + type + ".");
 255     }
 256
 257     /**
 258      * Instantiates type abstractions and constraints from the value.
 259      */
 260     public Expression instantiate(Expression expr) {
 261         Type type = Types.weakCanonical(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);
 268         }
 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;
 273                 type = fun.range;
 274
 275                 long loc = expr.getLocation();
 276                 EVariable var = new EVariable(loc, null);
 277                 var.setType(pred);
 278                 expr = new EApply(loc, expr, var);
 279                 addConstraintDemand(var);
 280             }
 281             else if(fun.domain == Types.PUNIT) {
 282                 type = fun.range;
 283
 284                 long loc = expr.getLocation();
 285                 declareEffect(expr.location, fun.effect);
 286                 expr = new EApply(loc, fun.effect, expr, new ELiteral(loc, NoRepConstant.PUNIT));
 287             }
 288             else
 289                 break;
 290         }
 291         expr.setType(type);
 292         return expr;
 293     }
 294
 295     /**
 296      * Enforces {@code expr} to have type {@code b} by adding
 297      * type applications, lambdas and effect subsumptions.
 298      */
 299     public Expression subsume(Expression expr, Type b) {
 300         b = Types.weakCanonical(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));
 307         }*/
 308         expr = instantiate(expr);
 309
 310         try {
 311             subsume(expr.getLocation(), expr.getType(), b);
 312         } catch(UnificationException e) {
 313             typeError(expr.getLocation(), b, expr.getType());
 314         }
 315         return expr;
 316     }
 317
 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);
 330                 }
 331                 else {
 332                     try {
 333                         subsume(sub.loc, a, b);
 334                     } catch (UnificationException e) {
 335                         errorLog.log(sub.loc, "Type " + a + " is not a subtype of " + b + ".");
 336                     }
 337                     nontrivialSubs = true;
 338                 }
 339             }
 340             ++iterationCount;
 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)
 347                     if(!isEffect(sub.a))
 348                         subCopies.add(new Subsumption(sub.loc,
 349                                 sub.a.copySkeleton(metaVarMap), sub.b.copySkeleton(metaVarMap)));
 350
 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));*/
 355
 356                 for(Subsumption sub : subCopies)
 357                     try {
 358                         Types.unify(sub.a, sub.b);
 359                     } catch (UnificationException e) {
 360                         errorLog.log(sub.loc, "Unification of types failed.");
 361                         return false;
 362                     }
 363
 364                 /*System.out.println("----");
 365                 for(Subsumption sub : subCopies)
 366                     System.out.println(sub.a.toString(tuc) + " === " + sub.b.toString(tuc));*/
 367             }
 368         }
 369         for(Subsumption sub : subsumptions)
 370             try {
 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();
 376             }
 377         subsumptions.clear();
 378         return true;
 379     }
 380
 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.getTypeConstructor((TCon)type).kind == Kinds.EFFECT;
 386         else if(type instanceof TVar)
 387             return ((TVar)type).getKind() == Kinds.EFFECT;
 388         else if(type instanceof TUnion)
 389             return true;
 390         else
 391             return false;
 392
 393     }
 394
 395     public void solveSubsumptions(long globalLoc) {
 396         if(expandSubsumptions())
 397             new SubSolver(errorLog, effectSubsumptions, potentialSingletonEffects, globalLoc).solve();
 398     }
 399
 400     public void declareEffect(long loc, Type effect) {
 401         subsumeEffect(loc, effect, effectUpperBounds.get(effectUpperBounds.size()-1));
 402     }
 403
 404     public void pushEffectUpperBound(long loc, Type effect) {
 405         effectUpperBounds.add(effect);
 406         potentialSingletonEffects.add(effect);
 407     }
 408
 409     public Type popEffectUpperBound() {
 410         return effectUpperBounds.remove(effectUpperBounds.size()-1);
 411     }
 412
 413     public ErrorLog getErrorLog() {
 414         return errorLog;
 415     }
 416
 417     public boolean isInPattern() {
 418         return isInPattern;
 419     }
 420
 421     public void setInPattern(boolean isInPattern) {
 422         this.isInPattern = isInPattern;
 423     }
 424
 425     public void pushConstraintFrame(Variable[] array) {
 426         constraintFrames.add(array);
 427     }
 428
 429     public void popConstraintFrame() {
 430         constraintFrames.remove(constraintFrames.size()-1);
 431     }
 432
 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);
 438                     return;
 439                 }
 440         constraintDemand.add(var);
 441     }
 442
 443     public Expression addConstraint(TPred pred) {
 444         EVariable evidence = new EVariable(null);
 445         evidence.setType(pred);
 446         addConstraintDemand(evidence);
 447         return evidence;
 448     }
 449
 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]);
 456         return evidences;
 457     }
 458
 459     public ArrayList<EVariable> getConstraintDemand() {
 460         return constraintDemand;
 461     }
 462
 463     public void resetConstraintDemand() {
 464         constraintDemand = new ArrayList<EVariable>();
 465     }
 466
 467     public void typeError(long loc, Type requiredType, Type givenType) {
 468         TypeUnparsingContext tuc = new TypeUnparsingContext();
 469         errorLog.log(loc, "Expected <" + requiredType.toString(tuc) + "> got <" + givenType.toString(tuc) + ">.");
 470     }
 471
 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,
 478                     true);
 479
 480             expression = ExpressionAugmentation.augmentSolved(
 481                     red.solvedConstraints,
 482                     expression);
 483
 484             for(Constraint c : red.unsolvedConstraints)
 485                 errorLog.log(c.getDemandLocation(), "There is no instance for <"+c.constraint+">.");
 486         }
 487         else
 488             expression = expression.decomposeMatching();
 489
 490         return expression;
 491     }
 492
 493     public SCLValue getValue(Name name) {
 494         if(constants.containsKey(name))
 495             return constants.get(name);
 496         SCLValue value = environment.getValue(name);
 497         if(value == null)
 498             errorLog.log(Locations.NO_LOCATION, "Couldn't find " + name + ".");
 499         constants.put(name, value);
 500         return value;
 501     }
 502
 503     public Expression getConstant(Name name, Type ... typeParameters) {
 504         SCLValue value = getValue(name);
 505         if(value == null)
 506             return new EError(Locations.NO_LOCATION);
 507         return new EConstant(value, typeParameters);
 508     }
 509
 510     public Environment getEnvironment() {
 511         return environment;
 512     }
 513
 514 }