let rec mk_apply op a =
  if is_i op then a else 
    match d_apply op with
      | k', [b] 
          when is_k k' -> 
          b
      | s', [c; b] 
          when is_s s' ->
          mk_apply (mk_apply c a) (mk_apply b a)
      | c', [d; c; b] 
          when is_c c' ->
          if Term.eq a b then a
          else (match Term.is_equal c d with
            | Three.Yes -> b
            | Three.No -> a
            | Three.X -> 
                if Term.eq d a && Term.eq c b then a
                else 
                  (match d_apply b, d_apply a with
                     | (z, [a']), (z', [b'])
                         when Term.eq z z'
                           && Term.eq d a'
                           && Term.eq c b' -> mk_apply z a'
                     | _ ->
                         Term.App.mk_app Sym.Cl.apply [c'; d; c; b; a]))    
      | f', bl ->
          (try
             if not(!reflection_enabled) then
               raise Not_found;
             let (op', n') = d_reify f' in
               if n' = List.length bl + 1 then
                 reflect op' (bl @ [a])
               else
                 raise Not_found
           with
               Not_found -> 
                 Term.App.mk_app Sym.Cl.apply ([f'] @ bl @ [a]))
        

and mk_apply2 op a1 a2 =
  mk_apply (mk_apply op a1) a2

and mk_apply3 op a1 a2 a3 =
  mk_apply (mk_apply (mk_apply op a1) a2) a3 


and mk_apply_star op = function
  | [] -> op
  | a :: al -> 
      let op' = mk_apply op a in
        mk_apply_star op' al

and mk_cases a b c d =
  mk_apply (mk_apply (mk_apply (mk_apply (mk_c()) a) b) c) d


and sigma op al =
  Trace.msg "foo32" "Cl.sigma" (op, al) (Sym.Cl.pp Term.pp);
  match op, al with
    | Sym.Apply, [x; y] -> mk_apply x y
    | Sym.S, [] -> mk_s ()
    | Sym.K, [] -> mk_k ()
    | Sym.I, [] -> mk_i ()
    | Sym.C, [] -> mk_c ()
    | Sym.Reify(f, n), [] -> mk_reify (f, n)
    | Sym.C, [a; b; c; d] -> mk_cases a b c d
    | Sym.S, [a; b; c] -> mk_apply3 (mk_s()) a b c
    | Sym.K, [a; b] -> mk_apply2 (mk_k()) a b
    | Sym.I, [a] -> mk_apply (mk_i()) a
    | Sym.Apply, [c; a1; a2; a3; a4] when is_c(c) -> mk_cases a1 a2 a3 a4
    | Sym.Apply, [s; a1; a2; a3] when is_s(s) -> mk_apply3 (mk_s()) a1 a2 a3
    | Sym.Apply, [k; a1; a2] when is_k(k) -> mk_apply2 (mk_k()) a1 a2
    | _ ->
        assert false



(** Build a first-order application of function symbol f. *)


and reflect f al =  
  match Sym.get f with
    | Sym.Arith(op) -> Arith.sigma op al
    | Sym.Product(op) -> Product.sigma op al
    | Sym.Bv(op) -> Bitvector.sigma op al
    | Sym.Coproduct(op) -> Coproduct.sigma op al
    | Sym.Propset(op) -> Propset.sigma op al
    | Sym.Cl(op) -> sigma op al
    | Sym.Pp(op) -> Pprod.sigma op al
    | Sym.Uninterp _ -> Term.App.mk_app f al
    | Sym.Arrays(op) -> Funarr.sigma Term.is_equal op al




(** Build a higher-order application of function symbol f. Thus reflection must be disabled here. *)


and reify f al = 
  let n = List.length al in
  let op = mk_reify (f, n) in
    try
      reflection_enabled := false;
      let b = mk_apply_star op al in
        reflection_enabled := true;
        b
    with
        exc -> 
          reflection_enabled := true;
          raise exc