diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala index be2a14fa5f6a44a84f53cfa63705438babfc0a7f..db86711715825840bc02ab8e1fba5c6470135f67 100644 --- a/src/main/scala/leon/purescala/Extractors.scala +++ b/src/main/scala/leon/purescala/Extractors.scala @@ -19,8 +19,6 @@ object Extractors { case SetCardinality(t) => Some((t,SetCardinality)) case MultisetCardinality(t) => Some((t,MultisetCardinality)) case MultisetToSet(t) => Some((t,MultisetToSet)) - case Car(t) => Some((t,Car)) - case Cdr(t) => Some((t,Cdr)) case SetMin(s) => Some((s,SetMin)) case SetMax(s) => Some((s,SetMax)) case CaseClassSelector(cd, e, sel) => Some((e, CaseClassSelector(cd, _, sel))) @@ -69,8 +67,6 @@ object Extractors { case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt)) case ArrayFill(t1, t2) => Some((t1, t2, ArrayFill)) case ArraySelect(t1, t2) => Some((t1, t2, ArraySelect)) - case Concat(t1,t2) => Some((t1,t2,Concat)) - case ListAt(t1,t2) => Some((t1,t2,ListAt)) case Let(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => Let(binders, e, b))) case LetTuple(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => LetTuple(binders, e, b))) case Require(pre, body) => Some((pre, body, Require)) diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala index 663cf5e396036b7de5852c3e65980607b64f3404..8cb92d293b920d20bf61735451c35f5054824bd3 100644 --- a/src/main/scala/leon/purescala/Trees.scala +++ b/src/main/scala/leon/purescala/Trees.scala @@ -631,14 +631,6 @@ object Trees { setType(array.getType) } - /* List operations */ - case class NilList(baseType: TypeTree) extends Expr with Terminal - case class Cons(head: Expr, tail: Expr) extends Expr - case class Car(list: Expr) extends Expr - case class Cdr(list: Expr) extends Expr - case class Concat(list1: Expr, list2: Expr) extends Expr - case class ListAt(list: Expr, index: Expr) extends Expr - /* Constraint programming */ case class Distinct(exprs: Seq[Expr]) extends Expr with FixedType { val fixedType = BooleanType