- "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^
- List.fold_right
- (fun (x,y) i -> "\n " ^ x ^ " => " ^
- (match y with None -> "" | Some y -> pp y l) ^ i)
- connames_and_patterns "" ^
- "\nend"
+ "\nmatch " ^ pp te l ^ " return " ^ pp ty l ^ " with \n [ " ^
+ (String.concat "\n | "
+ (List.map
+ (fun (x,argsno,y) ->
+ let rec aux argsno l =
+ function
+ Cic.Lambda (name,ty,bo) when argsno > 0 ->
+ let args,res = aux (argsno - 1) (Some name::l) bo in
+ ("(" ^ (match name with C.Anonymous -> "_" | C.Name s -> s)^
+ ":" ^ pp ty l ^ ")")::args, res
+ | t when argsno = 0 -> [],pp t l
+ | t -> ["{" ^ string_of_int argsno ^ " args missing}"],pp t l
+ in
+ let pattern,body =
+ match y with
+ None -> x,""
+ | Some y when argsno = 0 -> x,pp y l
+ | Some y ->
+ let args,body = aux argsno l y in
+ "(" ^ x ^ " " ^ String.concat " " args ^ ")",body
+ in
+ pattern ^ " => " ^ body
+ ) connames_and_argsno_and_patterns)) ^
+ "\n]"