From 786bb2197cc7a3db97bdf86d21cdba0706841647 Mon Sep 17 00:00:00 2001
From: Mario Bucev <mario.bucev@epfl.ch>
Date: Mon, 26 Sep 2022 14:14:53 +0200
Subject: [PATCH] Adding a case for type instantiation
---
src/main/scala/inox/ast/TypeOps.scala | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/src/main/scala/inox/ast/TypeOps.scala b/src/main/scala/inox/ast/TypeOps.scala
index f745b7674..3b081c5fe 100644
--- a/src/main/scala/inox/ast/TypeOps.scala
+++ b/src/main/scala/inox/ast/TypeOps.scala
@@ -72,6 +72,15 @@ trait TypeOps {
(ts1 zip ts2).foldLeft[Instantiation](Map.empty) {
case (inst, (tp1, tp2)) => unify(inst, rec(tp1, tp2))
}
+ case (adt1: ADTType, refn: RefinementType) =>
+ refn.getType match {
+ case adt2: ADTType =>
+ // ADT(X1, ..., Xn) -> { vd: ADT(A1, ..., An) | prop }
+ // ~>
+ // X1 -> A1, ..., Xn -> An
+ rec(adt1, adt2)
+ case _ => throw new Failure
+ }
case _ => throw new Failure
}
--
GitLab