lib.py 4.35 KB
Newer Older
1 2 3 4 5 6 7 8
#!/usr/bin/env python
#-*- coding: UTF-8 -*-

# utilitaires pour manipuler la BDD

import sys


9
# différences de résultats entre les 2 prouveurs
10 11 12 13
def diff(cursor, prover1, prover2):
  "trouve les (file,goal) dont le résultat est différent\
  pour prover1 et prover2"

14
  query = """SELECT r1.file, r1.goal, r1.prover, r1.result, r2.prover, r2.result
15 16
    FROM runs r1
    INNER JOIN runs r2
17 18 19
    WHERE r1.prover = "%s" AND r2.prover = "%s"
      AND r1.file = r2.file AND r1.goal = r2.goal
      AND r1.result <> r2.result""" % \
20 21 22 23 24 25 26 27 28
      (prover1, prover2)
  try:
    result = cursor.execute(query)
    return result.fetchall()
  except Exception, e:
    print >> sys.stderr, "exception :", repr(e)
    return []


29
# (file,goal) sur lesquels le premier prouveur est meilleur que le second
30 31 32 33
def superior(cursor, prover1, prover2):
  "trouve les (file,goal) pour lesquels prover1 > prover2"

  query = """SELECT distinct r1.file, r1.goal
34 35
    FROM runs r1
    INNER JOIN runs r2
36
    WHERE r1.prover = "%s" AND r2.prover = "%s"
37
      AND r1.file = r2.file AND r1.goal = r2.goal
38
      AND r1.result = "Valid"
39
      AND r2.result <> "Valid"
40 41 42 43 44 45 46 47 48
    """ % (prover1, prover2)

  try:
    result = cursor.execute(query)
    return result.fetchall()
  except Exception, e:
    print >> sys.stderr, "exception :", repr(e)
    return None

49

50
# affichage aligné en colonnes
51
def print_columns(lines, sep = u"."):
52
  "affiche les colonnes bien alignées"
53
  sep = unicode(sep)
54 55 56 57
  if len(lines) == 0:
    return
  column_width = len(lines[0])
  widths = [0 for x in xrange(column_width)]
58
  # calculer la largeur de chaque colonne (max des largeurs de ses éléments)
59 60
  for line in lines:
    for i in xrange(column_width-1):
61
      widths[i] = max(widths[i], len(unicode(line[i])))
62 63 64

  for line in lines:
    for i in xrange(column_width-1):
65
      assert(len(unicode(line[i])) <= widths[i])
66 67 68
      item = unicode(line[i])
      item = item.ljust(widths[i]+2, sep)
      print item,
69
    print line[-1]
70 71


72
# petite facilité
73
def print_sep():
74 75
  "affiche une ligne de '-' pour séparer clairement des\
  sections de l'affichage"
76
  print "---------------------------------------------------------------"
77 78


79
# effacer la ligne courante du terminal
80 81 82 83
def erase_line(stream = sys.stdout):
  "efface la ligne et revient au début"
  stream.write("\033[2K\r")
  stream.flush()
84 85


86
# récupéré sur le net, pour obtenir largeur et hauteur du terminal
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
def getTerminalSize():
  "récupère la largeur et la hauteur du terminal"
# {{{
  def ioctl_GWINSZ(fd):
    try:
      import fcntl, termios, struct, os
      cr = struct.unpack('hh', fcntl.ioctl(fd, termios.TIOCGWINSZ, '1234'))
    except:
      return None
    return cr
  cr = ioctl_GWINSZ(0) or ioctl_GWINSZ(1) or ioctl_GWINSZ(2)
  if not cr:
    try:
      fd = os.open(os.ctermid(), os.O_RDONLY)
      cr = ioctl_GWINSZ(fd)
      os.close(fd)
    except:
        pass
  if not cr:
    try:
      cr = (env['LINES'], env['COLUMNS'])
    except:
      cr = (25, 80)
  return int(cr[1]), int(cr[0])
# }}}

113 114 115 116 117 118


# tente d'affichier un tableau donné en entrée. Ce tableau
# est un dictionnaire (colonne,ligne) -> item qui doit vérifier
# la propriété suivante :
# pour tout (i,j) dans tab, (j,i) est aussi dans tab
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
def printTab(tab):
  "affiche le tableau carré donné en entrée"

  items = list(set( [unicode(x) for (x,y) in tab.keys()] )) # enlever doublons
  for i in items:
    tab[ (None,i) ] = i # pour la première ligne

  max_width = 0
  normal_sum = 0
  for i in items:
    max_width = max(max_width, len(i)+1)
    normal_sum += len(i) + 1

  width,height = getTerminalSize()
  if max_width * (len(items)+1)  >= width: # ça ne rentre pas
    print >> sys.stderr, "terminal trop étroit"
    max_width = width / (len(items) + 1)

  def print_line(item):
    if item != None:
      sys.stdout.write(item[:max_width-1].ljust(max_width-1, " ")+"|")
    else:
      sys.stdout.write("x\y : x>y".ljust(max_width-1, " ")+"|")
    for i in xrange(len(items)):
      i = items[i]
      if i == item:
        sys.stdout.write("x".ljust(max_width, " "))
      else:
        num = unicode(tab[ (item,i) ])
        sys.stdout.write(num[:max_width-1].ljust(max_width, " "))
    sys.stdout.write("\n")

  print "légende : [colonne] est meilleur que [ligne] sur [case] buts\n"
  print_line(None)
  for i in items:
    print("-"*(len(items)+1)*max_width)
    print_line(i)

  for i in items:
    try:
      del tab[ (None,i) ]
    except:
      pass