From 9447617aefbe9706b0d74a827181976e4b9e9d26 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Thu, 17 Dec 2009 01:17:59 +0000
Subject: 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.

---
 Source/Core/BoogiePL.atg | 49 ++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 45 insertions(+), 4 deletions(-)

(limited to 'Source/Core/BoogiePL.atg')

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 4fc91b35..eab10ff9 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -380,6 +380,8 @@ Function<out DeclarationSeq! ds>
      TypeVariableSeq! typeParams = new TypeVariableSeq();
      VariableSeq arguments = new VariableSeq();
      TypedIdent! tyd;
+     TypedIdent retTyd = null;
+     Type! retTy;
      QKeyValue kv = null;
      Expr definition = null;
      Expr! tmp;
@@ -390,12 +392,51 @@ Function<out DeclarationSeq! ds>
   [ VarOrType<out tyd>      (. arguments.Add(new Formal(tyd.tok, tyd, true)); .)
   { "," VarOrType<out tyd>  (. arguments.Add(new Formal(tyd.tok, tyd, true)); .)
   } ] ")"
-  "returns" "(" VarOrType<out tyd> ")"
+  ( 
+    "returns" "(" VarOrType<out tyd> ")" (. retTyd = tyd; .)
+    | 
+    ":" Type<out retTy>   (. retTyd = new TypedIdent(retTy.tok, "", retTy); .) 
+  )
   ( "{" Expression<out tmp> (. definition = tmp; .) "}" | ";" )
   (.
+    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);
     ds.Add(func);
+    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 {
+	    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")) {
@@ -1199,9 +1240,9 @@ ArrayExpression<out Expr! e>
     (. if (store)
          e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs);
        else if (bvExtract)
-         e = new ExtractExpr(x, e,
-                             ((BvBounds)index0).Upper.ToIntSafe,
-                             ((BvBounds)index0).Lower.ToIntSafe);
+         e = new BvExtractExpr(x, e,
+                               ((BvBounds)index0).Upper.ToIntSafe,
+                               ((BvBounds)index0).Lower.ToIntSafe);
        else
          e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs); 
     .)
-- 
cgit v1.2.3