code: private Context translateSwitch(WyilFile.Stmt.Switch stmt, Context context) {
  		Tuple<WyilFile.Stmt.Case> cases = stmt.getCases();
  		//
  		Pair<Expr, Context> p = translateExpressionWithChecks(stmt.getCondition(), null, context);
  		Expr value = p.first();
  		context = p.second();
  		//
  		WyalFile.Stmt defaultValue = null;
  		Context[] descendants = new Context[cases.size() + 1];
  		Context defaultContext = null;
  		boolean hasDefault = false;
  		//
  		for (int i = 0; i != cases.size(); ++i) {
  			WyilFile.Stmt.Case caSe = cases.get(i);
  			Context caseContext;
  			// Setup knowledge from case values
  			if (!caSe.isDefault()) {
  				WyalFile.Stmt e = null;
  				for (WyilFile.Expr constant : caSe.getConditions()) {
  					// Expr v = convert(constant, stmt, context.getEnvironment());
  					Expr v = translateExpression(constant, null, context.getEnvironment());
  					e = or(e, new Expr.Equal(value, v));
  					defaultValue = and(defaultValue, new Expr.NotEqual(value, v));
  				}
  				caseContext = context.assume(e);
  				descendants[i] = translateStatementBlock(caSe.getBlock(), caseContext);
  			} else {
  				defaultContext = context.assume(defaultValue);
  				defaultContext = translateStatementBlock(caSe.getBlock(), defaultContext);
  				hasDefault = true;
  			}
  		}
  		// Sort out default context
  		if (!hasDefault) {
  			// indicates no default block was present, so we just assume what we
  			// know and treat it as a fall through.
  			defaultContext = context.assume(defaultValue);
  		}
  		descendants[descendants.length - 1] = defaultContext;
  		//
  		return joinDescendants(context, descendants);
  	}
docs: Translate a switch statement.
  
  @param stmt
  @param wyalFile