From 99ecf1d7222d7167f533f63ee469cfbb4df36963 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 22 Sep 2015 18:24:12 +0200
Subject: [PATCH] Treat Forall in instantiateType
---
src/main/scala/leon/purescala/TypeOps.scala | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 0e7493018..f64c05219 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -300,6 +300,14 @@ object TypeOps {
val mapping = args.map(_.id) zip newArgs.map(_.id)
Lambda(newArgs, rec(idsMap ++ mapping)(body)).copiedFrom(l)
+ case f @ Forall(args, body) =>
+ val newArgs = args.map { arg =>
+ val tpe = tpeSub(arg.getType)
+ ValDef(freshId(arg.id, tpe))
+ }
+ val mapping = args.map(_.id) zip newArgs.map(_.id)
+ Forall(newArgs, rec(idsMap ++ mapping)(body)).copiedFrom(f)
+
case p @ Passes(in, out, cases) =>
val (newIn, newCases) = onMatchLike(in, cases)
passes(newIn, srec(out), newCases).copiedFrom(p)
--
GitLab