From 4f975ded7e7b2c8f6e5faa120a9df9a436c70120 Mon Sep 17 00:00:00 2001
From: Lars Hupel <lars.hupel@mytum.de>
Date: Mon, 25 Jan 2016 10:35:25 +0100
Subject: [PATCH] dummy support for strings
---
src/main/isabelle/Leon_Library.thy | 2 ++
src/main/scala/leon/solvers/isabelle/Types.scala | 3 +++
2 files changed, 5 insertions(+)
diff --git a/src/main/isabelle/Leon_Library.thy b/src/main/isabelle/Leon_Library.thy
index 62d7108d4..4327381f8 100644
--- a/src/main/isabelle/Leon_Library.thy
+++ b/src/main/isabelle/Leon_Library.thy
@@ -5,6 +5,8 @@ begin
axiomatization
error :: "nat \<Rightarrow> 'a"
+typedecl string
+
declare [[code abort: error]]
declare null_rec[simp]
diff --git a/src/main/scala/leon/solvers/isabelle/Types.scala b/src/main/scala/leon/solvers/isabelle/Types.scala
index 0e6091551..7d2b4d1d8 100644
--- a/src/main/scala/leon/solvers/isabelle/Types.scala
+++ b/src/main/scala/leon/solvers/isabelle/Types.scala
@@ -127,6 +127,9 @@ final class Types(context: LeonContext, program: Program, system: System)(implic
case Some(datatype) => datatype.typ
}}.map { Type(_, args) }
}
+ case StringType =>
+ context.reporter.warning("Strings are not yet supported, translating to unspecified type")
+ Future.successful { Type("Leon_Library.string", Nil) }
case _ if strict =>
context.reporter.fatalError(s"Unsupported type $tree, can't be inferred")
case _ =>
--
GitLab