1 package org.simantics.scl.compiler.internal.elaboration.subsumption;
3 import java.util.ArrayList;
5 import org.simantics.scl.compiler.common.exceptions.InternalCompilerError;
6 import org.simantics.scl.compiler.internal.types.effects.EffectIdMap;
7 import org.simantics.scl.compiler.top.SCLCompilerConfiguration;
8 import org.simantics.scl.compiler.types.TMetaVar;
9 import org.simantics.scl.compiler.types.Type;
10 import org.simantics.scl.compiler.types.exceptions.UnificationException;
15 int constLowerBound = EffectIdMap.MIN;
16 int constUpperBound = EffectIdMap.MAX;
17 int upperApprox = EffectIdMap.MAX;
20 ArrayList<Var> simpleLowerBounds = new ArrayList<Var>();
21 ArrayList<Var> simpleUpperBounds = new ArrayList<Var>();
22 ArrayList<VUnion> complexLowerBounds = new ArrayList<VUnion>();
23 ArrayList<VUnion> complexUpperBounds = new ArrayList<VUnion>();
28 public Var(TMetaVar original, String name, SubSolver solver) {
29 this.original = original;
38 solver.dirtyQueue.add(this);
43 * Adds a constant constraint
45 public void addUpperBound(int c) {
47 if(c != constUpperBound) {
48 if((c & constLowerBound) != constLowerBound) {
49 solver.errorLog.log(solver.globalLoc, "Subsumption failed: " +
50 solver.effectIds.toType(constLowerBound) + " is not a subtype of " +
51 solver.effectIds.toType(c)
56 for(int i=0;i<complexUpperBounds.size();++i) {
57 VUnion u = complexUpperBounds.get(i);
59 if(u.con == 0 && u.vars.size() == 1) {
60 removeComplexUpperBound(i);
62 addUpperBound(u.vars.get(0));
69 public void addLowerBound(int c) {
70 if((c | constUpperBound) != constUpperBound) {
71 solver.errorLog.log(solver.globalLoc, "Subsumption failed: " +
72 solver.effectIds.toType(c) + " is not a subtype of " +
73 solver.effectIds.toType(constUpperBound)
81 private void removeComplexUpperBound(int i) {
82 VUnion u = complexUpperBounds.get(i);
83 int lastId = complexUpperBounds.size()-1;
84 VUnion last = complexUpperBounds.remove(lastId);
86 complexUpperBounds.set(i, last);
88 v.complexLowerBounds.remove(u);
94 * Adds a simple variable constraint
96 public void addUpperBound(Var var) {
99 if(simpleUpperBounds.size() < var.simpleLowerBounds.size()) {
100 if(simpleUpperBounds.contains(var))
104 if(var.simpleLowerBounds.contains(this))
108 for(int i=0;i<complexUpperBounds.size();++i)
109 if(complexUpperBounds.get(i).vars.contains(var)) {
110 removeComplexUpperBound(i);
114 simpleUpperBounds.add(var);
115 var.simpleLowerBounds.add(this);
122 * Adds a complex constraint
124 public void addUpperBound(VUnion u) {
125 if(u.vars.isEmpty()) {
126 addUpperBound(u.con);
129 if(u.vars.contains(this))
132 if(simpleUpperBounds.contains(v))
134 u.con &= constUpperBound;
135 if(u.con == constUpperBound)
137 if(u.con == 0 && u.vars.size() == 1)
138 addUpperBound(u.vars.get(0));
141 complexUpperBounds.add(u);
144 v.complexLowerBounds.add(u);
146 // TODO compare complex upper bounds together
149 public void replaceWith(int con) {
150 // Check that replacement is sound
151 if(SCLCompilerConfiguration.DEBUG) {
152 if((con&constLowerBound) != constLowerBound)
153 throw new InternalCompilerError();
154 if((con|constUpperBound) != constUpperBound)
155 throw new InternalCompilerError();
158 // Remove the variable and unify original TMetaVar
159 solver.vars.remove(original);
161 Type type = solver.effectIds.toType(con);
163 System.out.println(original.toString(solver.tuc) + " := " + type.toString(solver.tuc));
164 original.setRef(type);
165 } catch (UnificationException e) {
166 throw new InternalCompilerError();
169 // Propagate change to lower and upper bounds
170 for(Var v : simpleUpperBounds) {
171 v.simpleLowerBounds.remove(this);
172 v.addLowerBound(con);
175 for(Var v : simpleLowerBounds) {
176 v.simpleUpperBounds.remove(this);
177 v.addUpperBound(con);
180 for(VUnion u : complexUpperBounds) {
183 if(u.vars.size() == 1) {
184 Var uv = u.vars.get(0);
185 uv.constLowerBound |= ~u.con;
186 uv.complexLowerBounds.remove(u);
194 for(VUnion u : complexLowerBounds) {
198 u.con &= u.low.constUpperBound;
199 if(u.vars.isEmpty()) {
200 u.low.complexUpperBounds.remove(u);
201 u.low.addUpperBound(u.con);
203 else if(u.vars.size() == 1 && u.con == 0) {
204 u.low.complexUpperBounds.remove(u);
205 u.low.addUpperBound(u.vars.get(0));
210 public void replaceDownwards(Var var) {
211 // Remove the variable and unify original TMetaVar
212 solver.vars.remove(original);
215 System.out.println(original.toString(solver.tuc) + " := " + var.original.toString(solver.tuc));
216 original.setRef(var.original);
217 } catch (UnificationException e) {
218 throw new InternalCompilerError();
221 // Remove downwards dependencies
222 if(constLowerBound != 0)
223 throw new InternalCompilerError();
224 for(Var v : simpleLowerBounds)
225 v.simpleUpperBounds.remove(this);
226 if(!complexLowerBounds.isEmpty())
227 throw new InternalCompilerError();
230 // Propagate change to upper bounds
231 var.addUpperBound(constUpperBound);
232 for(Var v : simpleUpperBounds) {
233 v.simpleLowerBounds.remove(this);
234 var.addUpperBound(v);
236 for(VUnion u : complexUpperBounds) {
237 var.addUpperBound(u);
241 public void replaceUpwards(Var var) {
242 // Remove the variable and unify original TMetaVar
243 solver.vars.remove(original);
246 System.out.println(original.toString(solver.tuc) + " := " + var.original.toString(solver.tuc));
247 original.setRef(var.original);
248 } catch (UnificationException e) {
249 throw new InternalCompilerError();
252 // Remove upwards dependencies
253 if(constUpperBound != EffectIdMap.MAX)
254 throw new InternalCompilerError();
255 for(Var v : simpleUpperBounds)
256 v.simpleLowerBounds.remove(this);
257 if(!complexUpperBounds.isEmpty())
258 throw new InternalCompilerError();
261 // Propagate change to lower bounds
262 var.addLowerBound(constLowerBound);
263 for(Var v : simpleLowerBounds) {
264 v.simpleUpperBounds.remove(this);
266 v.addUpperBound(var);
268 for(VUnion u : complexLowerBounds) {
272 if(u.vars.isEmpty() && u.con == 0) {
273 u.low.complexUpperBounds.remove(u);
274 u.low.addUpperBound(var);
282 public boolean isFree() {
283 return constLowerBound == EffectIdMap.MIN &&
284 constUpperBound == EffectIdMap.MAX &&
285 simpleLowerBounds.isEmpty() &&
286 simpleUpperBounds.isEmpty() &&
287 complexLowerBounds.isEmpty() &&
288 complexUpperBounds.isEmpty();