Allow ":" in addition to "returns" in function definitions. Make the pretty-printer use ":" not "returns".

Allow foo(x,y,z:int,p,q:ptr) kind of syntax in function definitions.
Consequently foo(int,y:bool) is no longer allowed.
Update the testsuite to match that.

1 files changed, 158 insertions, 108 deletions

diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc
index 8ae741ab..a7453d09 100644
--- a/Source/Core/Parser.ssc
+++ b/Source/Core/Parser.ssc
@@ -118,6 +118,10 @@ private class BvBounds : Expr {
 		errDist = 0;

 	}

 

+	public static void SemErr(IToken! tok, string! msg) {

+		Errors.SemErr(tok.filename, tok.line, tok.col, msg);

+	}

+

 	static void Get() {

 		for (;;) {

 			token = t;

@@ -260,6 +264,8 @@ private class BvBounds : Expr {
 		TypeVariableSeq! typeParams = new TypeVariableSeq();

 		VariableSeq arguments = new VariableSeq();

 		TypedIdent! tyd;

+		TypedIdent retTyd = null;

+		Type! retTy;

 		QKeyValue kv = null;

 		Expr definition = null;

 		Expr! tmp;

@@ -283,10 +289,17 @@ private class BvBounds : Expr {
 			}

 		}

 		Expect(9);

-		Expect(24);

-		Expect(8);

-		VarOrType(out tyd);

-		Expect(9);

+		if (t.kind == 24) {

+			Get();

+			Expect(8);

+			VarOrType(out tyd);

+			Expect(9);

+			retTyd = tyd; 

+		} else if (t.kind == 10) {

+			Get();

+			Type(out retTy);

+			retTyd = new TypedIdent(retTy.tok, "", retTy); 

+		} else Error(86);

 		if (t.kind == 25) {

 			Get();

 			Expression(out tmp);

@@ -294,42 +307,78 @@ private class BvBounds : Expr {
 			Expect(26);

 		} else if (t.kind == 7) {

 			Get();

-		} else Error(86);

+		} else Error(87);

+		if (retTyd == null) {

+		 // construct a dummy type for the case of syntax error

+		 tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int));

+		} else {

+		  tyd = retTyd;

+		}

 		Function! func = new Function(z, z.val, typeParams, arguments,

-		                      new Formal(tyd.tok, tyd, false), null, kv);

+		                       new Formal(tyd.tok, tyd, false), null, kv);

 		ds.Add(func);

-		if (definition != null) {

-		  // generate either an axiom or a function body

-		  if (QKeyValue.FindBoolAttribute(kv, "inline")) {

-		    func.Body = definition;

+		bool allUnnamed = true;

+		foreach (Formal! f in arguments) {

+		  if (f.TypedIdent.Name != "") {

+		    allUnnamed = false;

+		break;

+		     }

+		   }

+		   if (!allUnnamed) {

+		     Type prevType = null;

+		     for (int i = arguments.Length - 1; i >= 0; i--) {

+		       TypedIdent! curr = ((!)arguments[i]).TypedIdent;

+		       if (curr.Name == "") {

+		  if (prevType == null) {

+		    SemErr(curr.tok, "the type of the last parameter is unspecified");

+		    break;

+		  }

+		  Type ty = curr.Type;

+		         if (ty is UnresolvedTypeIdentifier &&

+		             ((!)(ty as UnresolvedTypeIdentifier)).Arguments.Length == 0) {

+		    curr.Name = ((!)(ty as UnresolvedTypeIdentifier)).Name;

+		    curr.Type = prevType;

 		  } else {

-		    VariableSeq dummies = new VariableSeq();

-		    ExprSeq callArgs = new ExprSeq();

-		    int i = 0;

-		    foreach (Formal! f in arguments) {

-		      string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;

-		      dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));

-		      callArgs.Add(new IdentifierExpr(f.tok, nm));

-		      i++;

-		    }

-		    TypeVariableSeq! quantifiedTypeVars = new TypeVariableSeq ();

-		    foreach (TypeVariable! t in typeParams)

-		      quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));

-		      Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);

-		    // specify the type of the function, because it might be that

-		    // type parameters only occur in the output type

-		    call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone());

-		    Expr def = Expr.Eq(call, definition);

-		    if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

-		      def = new ForallExpr(z, quantifiedTypeVars, dummies, 

-		                           kv, 

-		                           new Trigger(z, true, new ExprSeq(call), null),

-		                           def);

-		    }

-		    ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));

+		    SemErr(curr.tok, "expecting an identifier as parameter name");

 		  }

-		}

+		} else {

+		  prevType = curr.Type;

+		}

+		     }

+		   }

+		   if (definition != null) {

+		     // generate either an axiom or a function body

+		     if (QKeyValue.FindBoolAttribute(kv, "inline")) {

+		       func.Body = definition;

+		     } else {

+		       VariableSeq dummies = new VariableSeq();

+		       ExprSeq callArgs = new ExprSeq();

+		       int i = 0;

+		       foreach (Formal! f in arguments) {

+		         string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;

+		         dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));

+		         callArgs.Add(new IdentifierExpr(f.tok, nm));

+		         i++;

+		       }

+		       TypeVariableSeq! quantifiedTypeVars = new TypeVariableSeq ();

+		       foreach (TypeVariable! t in typeParams)

+		         quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));

 		

+		       Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);

+		       // specify the type of the function, because it might be that

+		       // type parameters only occur in the output type

+		       call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone());

+			    Expr def = Expr.Eq(call, definition);

+			    if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

+			      def = new ForallExpr(z, quantifiedTypeVars, dummies, 

+			                           kv, 

+			                           new Trigger(z, true, new ExprSeq(call), null),

+			                           def);

+			    }

+		       ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));

+		     }

+		   }

+		 

 	}

 

 	static void Axiom(out Axiom! m) {

@@ -402,7 +451,7 @@ private class BvBounds : Expr {
 			impl = new Implementation(x, x.val, typeParams,

 			                          Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null); 

 			

-		} else Error(87);

+		} else Error(88);

 		proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); 

 	}

 

@@ -506,7 +555,7 @@ private class BvBounds : Expr {
 			ty = new UnresolvedTypeIdentifier (tok, tok.val, args); 

 		} else if (t.kind == 15 || t.kind == 17) {

 			MapType(out ty);

-		} else Error(88);

+		} else Error(89);

 	}

 

 	static void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {

@@ -553,7 +602,7 @@ private class BvBounds : Expr {
 			Get();

 			Type(out ty);

 			Expect(9);

-		} else Error(89);

+		} else Error(90);

 	}

 

 	static void Ident(out IToken! x) {

@@ -582,7 +631,7 @@ private class BvBounds : Expr {
 		} else if (t.kind == 15 || t.kind == 17) {

 			MapType(out ty);

 			ts.Add(ty); 

-		} else Error(90);

+		} else Error(91);

 	}

 

 	static void MapType(out Bpl.Type! ty) {

@@ -754,7 +803,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			SpecPrePost(true, pre, post);

 		} else if (t.kind == 34 || t.kind == 35) {

 			SpecPrePost(false, pre, post);

-		} else Error(91);

+		} else Error(92);

 	}

 

 	static void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {

@@ -782,7 +831,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				SpecBody(out locals, out blocks);

 				Expect(7);

 				pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv)); 

-			} else Error(92);

+			} else Error(93);

 		} else if (t.kind == 35) {

 			Get();

 			tok = token; 

@@ -797,8 +846,8 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				SpecBody(out locals, out blocks);

 				Expect(7);

 				post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv)); 

-			} else Error(93);

-		} else Error(94);

+			} else Error(94);

+		} else Error(95);

 	}

 

 	static void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {

@@ -849,7 +898,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 			Expression(out e);

 			b = new Block(x,x.val,cs,new ReturnExprCmd(token,e)); 

-		} else Error(95);

+		} else Error(96);

 		Expect(7);

 	}

 

@@ -893,7 +942,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			CallCmd(out cn);

 			Expect(7);

 			c = cn; 

-		} else Error(96);

+		} else Error(97);

 	}

 

 	static void StmtList(out StmtList! stmtList) {

@@ -977,7 +1026,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 45) {

 			BreakCmd(out bcmd);

 			ec = bcmd; 

-		} else Error(97);

+		} else Error(98);

 	}

 

 	static void TransferCmd(out TransferCmd! tc) {

@@ -995,7 +1044,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 39) {

 			Get();

 			tc = new ReturnCmd(token); 

-		} else Error(98);

+		} else Error(99);

 		Expect(7);

 	}

 

@@ -1020,7 +1069,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				Get();

 				StmtList(out els);

 				elseOption = els; 

-			} else Error(99);

+			} else Error(100);

 		}

 		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); 

 	}

@@ -1079,7 +1128,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (StartOf(5)) {

 			Expression(out ee);

 			e = ee; 

-		} else Error(100);

+		} else Error(101);

 		Expect(9);

 	}

 

@@ -1117,7 +1166,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			}

 			Expect(7);

 			c = new AssignCmd(x, lhss, rhss); 

-		} else Error(101);

+		} else Error(102);

 	}

 

 	static void CallCmd(out Cmd! c) {

@@ -1180,7 +1229,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				}

 				Expect(9);

 				c = new CallCmd(x, first.val, es, ids); 

-			} else Error(102);

+			} else Error(103);

 		} else if (t.kind == 51) {

 			Get();

 			Ident(out first);

@@ -1234,7 +1283,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			}

 			Expect(9);

 			c = new CallCmd(x, first.val, es, ids); 

-		} else Error(103);

+		} else Error(104);

 	}

 

 	static void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) {

@@ -1274,7 +1323,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (StartOf(5)) {

 			Expression(out e);

 			exprOptional = e; 

-		} else Error(104);

+		} else Error(105);

 	}

 

 	static void CallOutIdent(out IToken id) {

@@ -1286,7 +1335,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 1) {

 			Ident(out p);

 			id = p; 

-		} else Error(105);

+		} else Error(106);

 	}

 

 	static void Expressions(out ExprSeq! es) {

@@ -1331,7 +1380,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 53) {

 			Get();

-		} else Error(106);

+		} else Error(107);

 	}

 

 	static void LogicalExpression(out Expr! e0) {

@@ -1369,7 +1418,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 55) {

 			Get();

-		} else Error(107);

+		} else Error(108);

 	}

 

 	static void ExpliesOp() {

@@ -1377,7 +1426,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 57) {

 			Get();

-		} else Error(108);

+		} else Error(109);

 	}

 

 	static void RelationalExpression(out Expr! e0) {

@@ -1395,7 +1444,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 59) {

 			Get();

-		} else Error(109);

+		} else Error(110);

 	}

 

 	static void OrOp() {

@@ -1403,7 +1452,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 61) {

 			Get();

-		} else Error(110);

+		} else Error(111);

 	}

 

 	static void BvTerm(out Expr! e0) {

@@ -1470,7 +1519,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			x = token; op=BinaryOperator.Opcode.Ge; 

 			break;

 		}

-		default: Error(111); break;

+		default: Error(112); break;

 		}

 	}

 

@@ -1502,7 +1551,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 72) {

 			Get();

 			x = token; op=BinaryOperator.Opcode.Sub; 

-		} else Error(112);

+		} else Error(113);

 	}

 

 	static void UnaryExpression(out Expr! e) {

@@ -1521,7 +1570,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); 

 		} else if (StartOf(12)) {

 			CoercionExpression(out e);

-		} else Error(113);

+		} else Error(114);

 	}

 

 	static void MulOp(out IToken! x, out BinaryOperator.Opcode op) {

@@ -1535,7 +1584,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 74) {

 			Get();

 			x = token; op=BinaryOperator.Opcode.Mod; 

-		} else Error(114);

+		} else Error(115);

 	}

 

 	static void NegOp() {

@@ -1543,7 +1592,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 76) {

 			Get();

-		} else Error(115);

+		} else Error(116);

 	}

 

 	static void CoercionExpression(out Expr! e) {

@@ -1567,7 +1616,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				  e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);

 				}

 				

-			} else Error(116);

+			} else Error(117);

 		}

 	}

 

@@ -1677,7 +1726,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 					e = new NAryExpr(x, new FunctionCall(id), es); 

 				} else if (t.kind == 9) {

 					e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); 

-				} else Error(117);

+				} else Error(118);

 				Expect(9);

 			}

 			break;

@@ -1710,11 +1759,11 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

 				if (typeParams.Length + ds.Length > 0)

 				 e = new ExistsExpr(x, typeParams, ds, kv, trig, e); 

-			} else Error(118);

+			} else Error(119);

 			Expect(9);

 			break;

 		}

-		default: Error(119); break;

+		default: Error(120); break;

 		}

 	}

 

@@ -1739,7 +1788,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 80) {

 			Get();

-		} else Error(120);

+		} else Error(121);

 	}

 

 	static void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,

@@ -1756,7 +1805,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			}

 		} else if (t.kind == 1) {

 			BoundVars(q, out ds);

-		} else Error(121);

+		} else Error(122);

 		QSep();

 		while (t.kind == 25) {

 			AttributeOrTrigger(ref kv, ref trig);

@@ -1769,7 +1818,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			Get();

 		} else if (t.kind == 82) {

 			Get();

-		} else Error(122);

+		} else Error(123);

 	}

 

 	static void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {

@@ -1825,7 +1874,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			  trig.AddLast(new Trigger(tok, true, es, null));

 			}

 			

-		} else Error(123);

+		} else Error(124);

 		Expect(26);

 	}

 

@@ -1839,7 +1888,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 		} else if (StartOf(5)) {

 			Expression(out e);

 			o = e; 

-		} else Error(124);

+		} else Error(125);

 	}

 

 	static void QSep() {

@@ -1847,7 +1896,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			Get();

 		} else if (t.kind == 84) {

 			Get();

-		} else Error(125);

+		} else Error(126);

 	}

 

 

@@ -1953,45 +2002,46 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			case 84: s = "\\u2022 expected"; break;

 			case 85: s = "??? expected"; break;

 			case 86: s = "invalid Function"; break;

-			case 87: s = "invalid Procedure"; break;

-			case 88: s = "invalid Type"; break;

-			case 89: s = "invalid TypeAtom"; break;

-			case 90: s = "invalid TypeArgs"; break;

-			case 91: s = "invalid Spec"; break;

-			case 92: s = "invalid SpecPrePost"; break;

+			case 87: s = "invalid Function"; break;

+			case 88: s = "invalid Procedure"; break;

+			case 89: s = "invalid Type"; break;

+			case 90: s = "invalid TypeAtom"; break;

+			case 91: s = "invalid TypeArgs"; break;

+			case 92: s = "invalid Spec"; break;

 			case 93: s = "invalid SpecPrePost"; break;

 			case 94: s = "invalid SpecPrePost"; break;

-			case 95: s = "invalid SpecBlock"; break;

-			case 96: s = "invalid LabelOrCmd"; break;

-			case 97: s = "invalid StructuredCmd"; break;

-			case 98: s = "invalid TransferCmd"; break;

-			case 99: s = "invalid IfCmd"; break;

-			case 100: s = "invalid Guard"; break;

-			case 101: s = "invalid LabelOrAssign"; break;

-			case 102: s = "invalid CallCmd"; break;

+			case 95: s = "invalid SpecPrePost"; break;

+			case 96: s = "invalid SpecBlock"; break;

+			case 97: s = "invalid LabelOrCmd"; break;

+			case 98: s = "invalid StructuredCmd"; break;

+			case 99: s = "invalid TransferCmd"; break;

+			case 100: s = "invalid IfCmd"; break;

+			case 101: s = "invalid Guard"; break;

+			case 102: s = "invalid LabelOrAssign"; break;

 			case 103: s = "invalid CallCmd"; break;

-			case 104: s = "invalid CallForallArg"; break;

-			case 105: s = "invalid CallOutIdent"; break;

-			case 106: s = "invalid EquivOp"; break;

-			case 107: s = "invalid ImpliesOp"; break;

-			case 108: s = "invalid ExpliesOp"; break;

-			case 109: s = "invalid AndOp"; break;

-			case 110: s = "invalid OrOp"; break;

-			case 111: s = "invalid RelOp"; break;

-			case 112: s = "invalid AddOp"; break;

-			case 113: s = "invalid UnaryExpression"; break;

-			case 114: s = "invalid MulOp"; break;

-			case 115: s = "invalid NegOp"; break;

-			case 116: s = "invalid CoercionExpression"; break;

-			case 117: s = "invalid AtomExpression"; break;

+			case 104: s = "invalid CallCmd"; break;

+			case 105: s = "invalid CallForallArg"; break;

+			case 106: s = "invalid CallOutIdent"; break;

+			case 107: s = "invalid EquivOp"; break;

+			case 108: s = "invalid ImpliesOp"; break;

+			case 109: s = "invalid ExpliesOp"; break;

+			case 110: s = "invalid AndOp"; break;

+			case 111: s = "invalid OrOp"; break;

+			case 112: s = "invalid RelOp"; break;

+			case 113: s = "invalid AddOp"; break;

+			case 114: s = "invalid UnaryExpression"; break;

+			case 115: s = "invalid MulOp"; break;

+			case 116: s = "invalid NegOp"; break;

+			case 117: s = "invalid CoercionExpression"; break;

 			case 118: s = "invalid AtomExpression"; break;

 			case 119: s = "invalid AtomExpression"; break;

-			case 120: s = "invalid Forall"; break;

-			case 121: s = "invalid QuantifierBody"; break;

-			case 122: s = "invalid Exists"; break;

-			case 123: s = "invalid AttributeOrTrigger"; break;

-			case 124: s = "invalid AttributeParameter"; break;

-			case 125: s = "invalid QSep"; break;

+			case 120: s = "invalid AtomExpression"; break;

+			case 121: s = "invalid Forall"; break;

+			case 122: s = "invalid QuantifierBody"; break;

+			case 123: s = "invalid Exists"; break;

+			case 124: s = "invalid AttributeOrTrigger"; break;

+			case 125: s = "invalid AttributeParameter"; break;

+			case 126: s = "invalid QSep"; break;

 

 			default: s = "error " + n; break;

 		}