diff --git a/src/main/scala/inox/transformers/CollectorWithPC.scala b/src/main/scala/inox/transformers/CollectorWithPC.scala new file mode 100644 index 0000000000000000000000000000000000000000..771fab6f8e197ec450d7bb06b76d9f70f2bd4dba --- /dev/null +++ b/src/main/scala/inox/transformers/CollectorWithPC.scala @@ -0,0 +1,26 @@ +/* Copyright 2009-2016 EPFL, Lausanne */ + +package inox +package transformers + +/** A [[Collector]] that collects path conditions */ +trait CollectorWithPC extends TransformerWithPC with Collector + +object CollectorWithPC { + def apply[T](p: Program)(f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]) = { + new CollectorWithPC { + + type R = T + val trees: p.trees.type = p.trees + val symbols: p.symbols.type = p.symbols + import trees.Expr + import symbols.Path + val initEnv: Path = Path.empty + + protected def step(e: Expr, env: Path): List[(T, Path)] = { + f.lift((e, env)).map((_, env)).toList + } + + } + } +} diff --git a/src/main/scala/inox/transformers/TransformerWithPC.scala b/src/main/scala/inox/transformers/TransformerWithPC.scala index fd0709898fca22d7a5d4e30c0f97186180c3d4e0..ecda40920e7e754d9d4cc058d5184fdc4fcdcafe 100644 --- a/src/main/scala/inox/transformers/TransformerWithPC.scala +++ b/src/main/scala/inox/transformers/TransformerWithPC.scala @@ -95,6 +95,3 @@ trait TransformerWithPC extends Transformer { } } - -/** A [[Collector]] that collects path conditions */ -trait CollectorWithPC extends TransformerWithPC with Collector