Refactored code that generates an axiom for a function, and changed the pretty printing to always reflect when a function body is inlined

1 files changed, 1 insertions, 28 deletions

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 80ab7d9f..5810fe49 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -418,34 +418,7 @@ private class BvBounds : Expr {
 		 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){

-		     Contract.Assert(f != null);

-		     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){

-		     Contract.Assert(t != null);

-		     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)retTyd.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));

+		   ds.Add(func.CreateDefinitionAxiom(definition, kv));

 		 }

 		}