let rec width f =
  match f with
    | Bv(b) -> Some(width_bv b)
    | _ -> None

and width_bv b =
  match b with
    | Const(c) ->
        Bitv.length c
    | Sub(n,i,j) ->
        assert(0 <= i && i <= j && j < n);
        j-i+1
    | Conc(n,m) -> 
        assert(0 <= n && 0 <= m);
        n + m
    | Bitwise(n) ->
        assert(n >= 0);
        n