scala/lib.scala
author Christian Urban <urbanc@in.tum.de>
Thu, 10 Jan 2019 12:51:24 +0000
changeset 294 6836da75b3ac
parent 221 18905d086cbb
permissions -rw-r--r--
updated to Isabelle 2016-1
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
package object lib {
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
//some list functions
221
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
     4
//slow version
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
     5
//def tl[A](xs: List[A]) : List[A] = xs match {
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
     6
//  case Nil => Nil
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
     7
//  case x::xs => xs
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
     8
//}
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
     9
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    10
def tl[A](xs: List[A]) : List[A] = 
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    11
  try { xs.tail } catch { case _:UnsupportedOperationException => Nil }
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
def hd[A](xs: List[A]) : A = xs.head
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
221
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    15
//slow version
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    16
//def nth_of[A](xs: List[A], n: Int) = 
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    17
//  if (n <= xs.length) Some(xs(n)) else None 
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    18
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
def nth_of[A](xs: List[A], n: Int) = 
221
18905d086cbb some peephole optimisations in the scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 193
diff changeset
    20
  try { Some(xs(n)) } catch { case _:IndexOutOfBoundsException => None }
193
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
//some map functions
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
def dget(m: Map[Int, Int], n: Int) = m.getOrElse(n, 0)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    25
//some string functions
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
def join[A](xs: List[A]) = xs.foldLeft("")(_.toString + _)
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
317a2532c567 split up scala-file into separate components
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
}