[CN-Exec] Error names which function is uninterpreted (#772)

backend/cn/lib/cn_internal_to_ail.ml

@@ -2949,9 +2949,20 @@ let cn_to_ail_function_internal
       in
       (bs, Some (List.map mk_stmt ss))
     | Uninterp ->
-      failwith
-        "Uninterpreted CN functions not supported at runtime. Please provide a concrete \
-         function definition"
+      Cerb_colour.with_colour
+        (fun () ->
+          print_endline
+            Pp.(
+              plain
+                (Pp.item
+                   "Uninterpreted CN functions not supported at runtime. Please provide \
+                    a concrete function definition for"
+                   (space
+                    ^^^ squotes (Definition.Function.pp_sig (Sym.pp fn_sym) lf_def)
+                    ^^^ !^"at"
+                    ^^^ Locations.pp lf_def.loc))))
+        ();
+      exit 2
   in
   let ail_record_opt = generate_record_opt fn_sym lf_def.return_bt in
   let params = List.map (fun (sym, bt) -> (sym, bt_to_ail_ctype bt)) lf_def.args in

backend/cn/lib/definition.ml

@@ -33,18 +33,27 @@ module Function = struct
 
 
   let pp_args xs =
-    Pp.flow_map
-      (Pp.break 1)
-      (fun (sym, typ) -> Pp.parens (Pp.typ (Sym.pp sym) (BaseTypes.pp typ)))
-      xs
+    let doc =
+      Pp.flow_map
+        (Pp.break 1)
+        (fun (sym, typ) -> Pp.parens (Pp.typ (Sym.pp sym) (BaseTypes.pp typ)))
+        xs
+    in
+    if PPrint.requirement doc = 0 then
+      Pp.parens Pp.empty
+    else
+      doc
+
+
+  let pp_sig nm def =
+    let open Pp in
+    nm ^^ pp_args def.args ^^^ colon ^^^ BaseTypes.pp def.return_bt
 
 
   let pp nm def =
     let open Pp in
-    nm
-    ^^ colon
-    ^^^ pp_args def.args
-    ^^ colon
+    pp_sig nm def
+    ^^^ equals
     ^/^
     match def.body with
     | Uninterp -> !^"uninterpreted"

backend/cn/lib/definition.mli

@@ -20,6 +20,8 @@ module Function : sig
 
   val pp_args : (Cerb_frontend.Symbol.sym * unit BaseTypes.t_gen) list -> Pp.document
 
+  val pp_sig : Pp.document -> t -> Pp.document
+
   val pp : Pp.document -> t -> Pp.document
 
   val open_ : (Sym.t * 'a) list -> IndexTerms.t -> IndexTerms.t list -> IndexTerms.t

util/cerb_colour.ml

@@ -34,6 +34,13 @@ let int_fg = function
 let do_colour =
   ref (Unix.isatty Unix.stdout)
 
+let with_colour f x =
+  let col = ! do_colour in
+  do_colour := true;
+  let r = f x in
+  do_colour := col;
+  r
+
 let without_colour f x =
   let col = ! do_colour in
   do_colour := false;

util/cerb_colour.mli

@@ -16,6 +16,7 @@ type ansi_style =
 type ansi_format = ansi_style list
 
 val do_colour: bool ref
+val with_colour: ('a -> 'b) -> 'a -> 'b
 val without_colour: ('a -> 'b) -> 'a -> 'b
 val ansi_format: ?err:bool -> ansi_format -> string -> string
 val pp_ansi_format: ?err:bool -> ansi_format -> (unit -> PPrint.document) -> PPrint.document