- "[match("^print_name l v ^ ":" ^ string_of_int ar^") " ^ string_of_term_no_pars l (t :> nf) ^
- " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift t)) !bs) ^ "] " ^
- String.concat " " (List.map (string_of_term l) args) ^ ")"
- and string_of_term_no_pars_app l = function
- | `I((n,ar), args) -> print_name l n ^ ":" ^ string_of_int ar ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args))
- | #nf as t -> string_of_term_w_pars l t
- and string_of_term_no_pars_lam l = function
- | `Lam(_,t) -> let name = string_of_var (List.length l) in
- "λ" ^ name ^ ". " ^ (string_of_term_no_pars_lam (name::l) t)
- | _ as t -> string_of_term_no_pars l t
- and string_of_term_no_pars l : nf -> string = function
- | `Lam _ as t -> string_of_term_no_pars_lam l t
- | #nf as t -> string_of_term_no_pars_app l t
- in string_of_term_no_pars l
+ (* assert (bs_lift = lev); *)
+ "(["^ varname 0 l v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars lev l (t :> nf) ^
+ " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (t :> nf)) !bs) ^ "] " ^
+ String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
+ and string_of_term_no_pars_app lev l = function
+ | `I((n,ar), args) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "") ^ " " ^ String.concat " " (List.map (string_of_term_w_pars lev l) (Listx.to_list args :> nf list))
+ | #nf as t -> string_of_term_w_pars lev l t
+ and string_of_term_no_pars_lam lev l = function
+ | `Lam(_,t,g) -> "λ" ^ boundvar lev ^ ". " ^ (string_of_term_no_pars_lam (lev+1) l t)
+ ^ (if g = [] then "" else String.concat ", " ("" :: List.map (string_of_term_no_pars (lev+1) l) g))
+ | _ as t -> string_of_term_no_pars lev l t
+ and string_of_term_no_pars lev l = function
+ | `Lam _ as t -> string_of_term_no_pars_lam lev l t
+ | #nf as t -> string_of_term_no_pars_app lev l t
+ and string_of_term t = string_of_term_no_pars 0 t in
+ string_of_term