def parse_time(value):
    """Convert a time string to "HH:MM:SS.S"

    - leading zeros are added where necessary
    - trailing zeros after "." are stripped
    - trailing "." is stripped

    e.g.

    - "6:15:22 PM" -> "18:15:22"
    - "6:15:22.00 AM" -> "06:15:22"
    - "6:02:22.010 AM" -> "06:02:22.01"
    """
    if value.count(' '):
        time, ap = value.split()
        if ap == 'PM':
            timetup = time.split(':')
            timetup[0] = str(int(timetup[0]) + 12)
            time = ':'.join(timetup)
    else:
        time = value
    hh, mm, ss = time.split(':')
    if ss.count('.'):
        ss0, ss1 = ss.split('.')
        ss1 = ('.' + ss1).rstrip('.0')
    else:
        ss0 = ss
        ss1 = ''
    newvalue = ':'.join(['{:02d}'.format(int(hh)), '{:02d}'.format(int(mm)),
        '{:02d}'.format(int(ss0)) + ss1])
    return newvalue
