let rec term s =
    Trace.func "canon" "Term" Term.pp Term.pp
      (can s)
      
  and can s a =
    match a with
      | Var _ -> v s a 
      | App(Sym.Arith(op), al) -> arith s op al
      | App(Sym.Bvarith(Sym.Unsigned), [x]) -> unsigned s x
      | App(Sym.Pp(op), xl) -> pprod s op xl
      | App(f, al) ->
          let th = Th.of_sym f in
          let interp x = fnd th s (can s x) in
          let al' = mapl interp al in
          let a' = if al == al' then a else sigma s f al' in
            lookup s a'

  and pprod s op al =   
    match op, al with
      | Expt(n), [x] ->
          lookup s (Sig.mk_expt n (fnd Th.la s (can s x)))
      | Mult, xl ->
          lookup s (Sig.mk_multl (Term.mapl (fun x -> fnd Th.la s (can s x)) xl))
      | _ ->
          assert false
          
  and unsigned s x =
    lookup s (Bvarith.mk_unsigned (fnd Th.bv s (can s x)))
      
  and arith s op l =       (* special treatment for arithmetic *)
    match op, l with       (* for optimizing memory usage. *)
      | Sym.Num(q), [] -> 
          lookup s (Arith.mk_num q)
      | Sym.Multq(q), [x] -> 
          let y = can s x in
            lookup s (Arith.mk_multq q (fnd Th.la s y))
      | Sym.Add, [x; y] -> 
          let a' = fnd Th.la s (can s x) 
          and b' = fnd Th.la s (can s y) in
            lookup s (Arith.mk_add a' b')
      | Sym.Add, _ :: _ :: _ -> 
          let f a = fnd Th.la s (can s a) in
          let l' =  mapl f l in
            lookup s (Arith.mk_addl l')
      | _ ->  
          let str = "Ill-formed term " ^ 
                    (Pretty.to_string Sym.pp (Sym.Arith(op))) ^
                    (Pretty.to_string (Pretty.list Term.pp) l)
          in
            failwith str