CN: Factor out WellTyped error messages

This commit also removes some duplication for ensure_base_type; but this
raises another question - why are there _any_ base type checks in
check.ml? Surely they are all redundant and signal an error in
WellTyped.ml?

backend/cn/lib/builtins.ml

@@ -2,40 +2,43 @@ module SBT = BaseTypes.Surface
 open Or_TypeError
 open IndexTerms
 
+let fail_number_args loc ~has ~expect =
+  fail { loc; msg = WellTyped (Number_arguments { type_ = `Other; has; expect }) }
+
+
 (* builtin function symbols *)
 let mk_arg0 mk args loc =
   match args with
   | [] -> return (mk loc)
-  | _ :: _ as xs ->
-    fail { loc; msg = Number_arguments { has = List.length xs; expect = 0 } }
+  | _ :: _ as xs -> fail_number_args loc ~has:(List.length xs) ~expect:0
 
 
 let mk_arg1 mk args loc =
   match args with
   | [ x ] -> return (mk x loc)
-  | xs -> fail { loc; msg = Number_arguments { has = List.length xs; expect = 1 } }
+  | xs -> fail_number_args loc ~has:(List.length xs) ~expect:1
 
 
 let mk_arg2_err mk args loc =
   match args with
   | [ x; y ] -> mk (x, y) loc
-  | xs -> fail { loc; msg = Number_arguments { has = List.length xs; expect = 2 } }
+  | xs -> fail_number_args loc ~has:(List.length xs) ~expect:2
 
 
 let mk_arg2 mk = mk_arg2_err (fun tup loc -> return (mk tup loc))
 
 let mk_arg3_err mk args loc =
   match args with
   | [ x; y; z ] -> mk (x, y, z) loc
-  | xs -> fail { loc; msg = Number_arguments { has = List.length xs; expect = 3 } }
+  | xs -> fail_number_args loc ~has:(List.length xs) ~expect:3
 
 
 let mk_arg3 mk = mk_arg3_err (fun tup loc -> return (mk tup loc))
 
 let mk_arg5 mk args loc =
   match args with
   | [ a; b; c; d; e ] -> return (mk (a, b, c, d, e) loc)
-  | xs -> fail { loc; msg = Number_arguments { has = List.length xs; expect = 5 } }
+  | xs -> fail_number_args loc ~has:(List.length xs) ~expect:5
 
 
 let min_bits_def (sign, n) =
@@ -124,7 +127,9 @@ let array_to_list_def =
         let expected = "map/array" in
         fail
           { loc;
-            msg = Illtyped_it { it = pp arr; has = SBT.pp (get_bt arr); expected; reason }
+            msg =
+              WellTyped
+                (Illtyped_it { it = pp arr; has = SBT.pp (get_bt arr); expected; reason })
           }
       | Some (_, bt) -> return (array_to_list_ (arr, i, len) bt loc)) )
 

backend/cn/lib/cLogicalFuns.ml

@@ -1,15 +1,14 @@
-open TypeErrors
-open Typing
-
-open Effectful.Make (Typing)
-
 module StringMap = Map.Make (String)
 module IntMap = Map.Make (Int)
 module CF = Cerb_frontend
 module BT = BaseTypes
-open Cerb_pp_prelude
 module Mu = Mucore
 module IT = IndexTerms
+open Cerb_pp_prelude
+open TypeErrors
+open Typing
+
+open Effectful.Make (Typing)
 
 let fail_n m = fail (fun _ctxt -> m)
 
@@ -245,7 +244,7 @@ let rec symb_exec_pexpr ctxt var_map pexpr =
   | PEsym sym ->
     (match Sym.Map.find_opt sym var_map with
      | Some r -> return r
-     | _ -> fail_n { loc; msg = Unknown_variable sym })
+     | _ -> fail_n { loc; msg = WellTyped (Unknown_variable sym) })
   | PEval v ->
     (match val_to_it loc v with
      | Some r -> return r