From 30daf75f78b331e971ba08cf794ec006441a722b Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 17 Jan 2013 19:06:42 -0800 Subject: Refactored code that generates an axiom for a function, and changed the pretty printing to always reflect when a function body is inlined --- Source/Core/Parser.cs | 29 +---------------------------- 1 file changed, 1 insertion(+), 28 deletions(-) (limited to 'Source/Core/Parser.cs') 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)); } } -- cgit v1.2.3