From 4d637c251a4dcc275f0ee19bcbb44c9988d1dc9c Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 4 May 2015 14:25:50 +0200
Subject: [PATCH] Fixed generic type subst for free variables in termination
chains
---
src/main/scala/leon/termination/ChainBuilder.scala | 13 +++++++++----
1 file changed, 9 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index ce0488068..f5bd3b78e 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -50,14 +50,19 @@ final case class Chain(relations: List[Relation]) {
def loop(initialArgs: Seq[Identifier] = Seq.empty, finalArgs: Seq[Identifier] = Seq.empty): Seq[Expr] = {
def rec(relations: List[Relation], funDef: TypedFunDef, subst: Map[Identifier, Identifier]): Seq[Expr] = {
+ val Relation(_, path, FunctionInvocation(fitfd, args), _) = relations.head
+ val tfd = TypedFunDef(fitfd.fd, fitfd.tps.map(funDef.translated))
+
val translate : Expr => Expr = {
- val map : Map[Expr, Expr] = subst.map(p => p._1.toVariable -> p._2.toVariable)
+ val free : Set[Identifier] = path.flatMap(variablesOf).toSet -- funDef.fd.params.map(_.id)
+ val freeMapping : Map[Identifier,Identifier] = free.map(id => id -> {
+ FreshIdentifier(id.name, funDef.translated(id.getType), true).copiedFrom(id)
+ }).toMap
+
+ val map : Map[Expr, Expr] = (subst ++ freeMapping).map(p => p._1.toVariable -> p._2.toVariable)
(e: Expr) => replace(map, funDef.translated(e))
}
- val Relation(_, path, FunctionInvocation(fitfd, args), _) = relations.head
- val tfd = TypedFunDef(fitfd.fd, fitfd.tps.map(funDef.translated))
-
lazy val newArgs = args.map(translate)
path.map(translate) ++ (relations.tail match {
--
GitLab