]> gerrit.simantics Code Review - simantics/platform.git/blob
850f077db32d3ec9c8b81a2ebe5b4f6b32b30aa6
[simantics/platform.git] /
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 }