let rec split_clock_type ct = match ct with | CT_var alpha -> alpha, Pbw one | CT_on (CT_var alpha, p) -> alpha, Pbw p | CT_on (ct', p) -> let alpha, w = split_clock_type ct' in alpha, On (w, Pbw p)