let sign lookup a = 
  let rec term a =
    match a with
      | Var _ -> lookup a
      | Term.App(Arith(op), xl) -> arith op xl
      | Term.App(Pp(op), xl) -> pprod op xl
      | Term.App(Bvarith(op), [x]) -> bvarith op x
      | a -> raise Not_found
  and arith op al = 
    try
      match op, al with
        | Num(q), [] -> Sign.of_q q
        | Multq(q), [x] -> Sign.multq q (term x)
        | Add, [x; y] -> Sign.add (term x) (term y)
        | Add, xl -> Sign.addl (List.map term xl)
        | _ -> assert false
      with
          Not_found -> Sign.T
  and bvarith op a =
    match op with
      | Unsigned -> Sign.Nonneg
  and pprod op al =
    try
      match op, al with
        | Expt(n), [x] -> Sign.expt n (try term x with Not_found -> Sign.T)
        | Mult, [] -> Sign.of_q Q.one
        | Mult, [x] -> term x
        | Mult, [x; y] -> Sign.mult (term x) (term y)
        | Mult, xl -> Sign.multl (List.map term xl)
        | _ -> assert false
      with
          Not_found -> Sign.T
  in
    term a