From 0f517bdf5bcb5707d92396fffb360dc3966b89aa Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 18 Aug 2016 22:01:26 +0200
Subject: [PATCH] SimpleSymbols for default symbol implementations
---
src/main/scala/inox/ast/SimpleSymbols.scala | 36 +++++++++++++++++++++
src/main/scala/inox/package.scala | 33 +------------------
2 files changed, 37 insertions(+), 32 deletions(-)
create mode 100644 src/main/scala/inox/ast/SimpleSymbols.scala
diff --git a/src/main/scala/inox/ast/SimpleSymbols.scala b/src/main/scala/inox/ast/SimpleSymbols.scala
new file mode 100644
index 000000000..e02d0f379
--- /dev/null
+++ b/src/main/scala/inox/ast/SimpleSymbols.scala
@@ -0,0 +1,36 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package ast
+
+trait SimpleSymbols { self: Trees =>
+
+ class Symbols(
+ val functions: Map[Identifier, FunDef],
+ val adts: Map[Identifier, ADTDefinition]
+ ) extends AbstractSymbols {
+
+ def transform(t: TreeTransformer) = new Symbols(
+ functions.mapValues(fd => new FunDef(
+ fd.id,
+ fd.tparams, // type parameters can't be transformed!
+ fd.params.map(vd => t.transform(vd)),
+ t.transform(fd.returnType),
+ t.transform(fd.fullBody),
+ fd.flags)),
+ adts.mapValues {
+ case sort: ADTSort => sort
+ case cons: ADTConstructor => new ADTConstructor(
+ cons.id,
+ cons.tparams,
+ cons.sort,
+ cons.fields.map(t.transform),
+ cons.flags)
+ })
+
+ def extend(functions: Seq[FunDef] = Seq.empty, adts: Seq[ADTDefinition] = Seq.empty) = new Symbols(
+ this.functions ++ functions.map(fd => fd.id -> fd),
+ this.adts ++ adts.map(cd => cd.id -> cd)
+ )
+ }
+}
diff --git a/src/main/scala/inox/package.scala b/src/main/scala/inox/package.scala
index 9ae8863f5..755de6a11 100644
--- a/src/main/scala/inox/package.scala
+++ b/src/main/scala/inox/package.scala
@@ -41,41 +41,10 @@ package object inox {
}
}
- object trees extends ast.Trees {
-
+ object trees extends ast.Trees with ast.SimpleSymbols {
object deconstructor extends {
protected val s: trees.type = trees
protected val t: trees.type = trees
} with ast.TreeDeconstructor
-
- class Symbols(
- val functions: Map[Identifier, FunDef],
- val adts: Map[Identifier, ADTDefinition]
- ) extends AbstractSymbols {
-
- def transform(t: TreeTransformer) = new Symbols(
- functions.mapValues(fd => new FunDef(
- fd.id,
- fd.tparams, // type parameters can't be transformed!
- fd.params.map(vd => t.transform(vd)),
- t.transform(fd.returnType),
- t.transform(fd.fullBody),
- fd.flags)),
- adts.mapValues {
- case sort: ADTSort => sort
- case cons: ADTConstructor => new ADTConstructor(
- cons.id,
- cons.tparams,
- cons.sort,
- cons.fields.map(t.transform),
- cons.flags)
- })
-
- def extend(functions: Seq[FunDef] = Seq.empty, adts: Seq[ADTDefinition] = Seq.empty) = new Symbols(
- this.functions ++ functions.map(fd => fd.id -> fd),
- this.adts ++ adts.map(cd => cd.id -> cd)
- )
- }
-
}
}
--
GitLab