drop a redundant argument from "bad arity" exceptions

src/core/pretty.ml

@@ -500,20 +500,20 @@ let () = Exn_printer.register
   | Ty.TypeMismatch (t1,t2) ->
       fprintf fmt "Type mismatch between %a and %a"
         print_ty t1 print_ty t2
-  | Ty.BadTypeArity (ts, ts_arg, app_arg) ->
+  | Ty.BadTypeArity (ts, app_arg) ->
       fprintf fmt "Bad type arity: type symbol %a must be applied \
                    to %i arguments, but is applied to %i"
-        print_ts ts ts_arg app_arg
+        print_ts ts (List.length ts.ts_args) app_arg
   | Ty.DuplicateTypeVar tv ->
       fprintf fmt "Type variable %a is used twice" print_tv tv
   | Ty.UnboundTypeVar tv ->
       fprintf fmt "Unbound type variable: %a" print_tv tv
   | Ty.UnexpectedProp ->
       fprintf fmt "Unexpected propositional type"
-  | Term.BadArity (ls, ls_arg, app_arg) ->
+  | Term.BadArity (ls, app_arg) ->
       fprintf fmt "Bad arity: symbol %a must be applied \
                    to %i arguments, but is applied to %i"
-        print_ls ls ls_arg app_arg
+        print_ls ls (List.length ls.ls_args) app_arg
   | Term.EmptyCase ->
       fprintf fmt "Empty match expression"
   | Term.DuplicateVar vs ->

src/core/term.ml

@@ -202,7 +202,7 @@ let pat_any pr pat =
 
 (* smart constructors for patterns *)
 
-exception BadArity of lsymbol * int * int
+exception BadArity of lsymbol * int
 exception FunctionSymbolExpected of lsymbol
 exception PredicateSymbolExpected of lsymbol
 exception ConstructorExpected of lsymbol
@@ -213,9 +213,8 @@ let pat_app fs pl ty =
     | None -> raise (FunctionSymbolExpected fs)
   in
   let mtch s ty p = ty_match s ty p.pat_ty in
-  ignore (try List.fold_left2 mtch s fs.ls_args pl
-    with Invalid_argument _ -> raise (BadArity
-      (fs, List.length fs.ls_args, List.length pl)));
+  ignore (try List.fold_left2 mtch s fs.ls_args pl with
+    | Invalid_argument _ -> raise (BadArity (fs, List.length pl)));
   if fs.ls_constr = 0 then raise (ConstructorExpected fs);
   pat_app fs pl ty
 
@@ -707,9 +706,8 @@ let t_open_quant_cb fq =
 
 let ls_arg_inst ls tl =
   let mtch s ty t = ty_match s ty (t_type t) in
-  try List.fold_left2 mtch Mtv.empty ls.ls_args tl
-  with Invalid_argument _ -> raise (BadArity
-    (ls, List.length ls.ls_args, List.length tl))
+  try List.fold_left2 mtch Mtv.empty ls.ls_args tl with
+    | Invalid_argument _ -> raise (BadArity (ls, List.length tl))
 
 let ls_app_inst ls tl ty =
   let s = ls_arg_inst ls tl in

src/core/term.mli

@@ -66,7 +66,7 @@ val ls_ty_freevars : lsymbol -> Stv.t
 exception EmptyCase
 exception DuplicateVar of vsymbol
 exception UncoveredVar of vsymbol
-exception BadArity of lsymbol * int * int
+exception BadArity of lsymbol * int
 exception FunctionSymbolExpected of lsymbol
 exception PredicateSymbolExpected of lsymbol
 exception ConstructorExpected of lsymbol

src/core/theory.ml

@@ -115,7 +115,7 @@ let meta_hash m = m.meta_tag
 
 exception KnownMeta of meta
 exception UnknownMeta of string
-exception BadMetaArity of meta * int * int
+exception BadMetaArity of meta * int
 exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
 
 let meta_table = Hstr.create 17
@@ -767,9 +767,8 @@ let create_meta m al =
     let mt = get_meta_arg_type a in
     if at = mt then a else raise (MetaTypeMismatch (m,at,mt))
   in
-  let al = try List.map2 get_meta_arg m.meta_type al
-    with Invalid_argument _ ->
-      raise (BadMetaArity (m, List.length m.meta_type, List.length al))
+  let al = try List.map2 get_meta_arg m.meta_type al with
+    | Invalid_argument _ -> raise (BadMetaArity (m, List.length al))
   in
   mk_tdecl (Meta (m,al))
 
@@ -907,9 +906,9 @@ let () = Exn_printer.register
   | KnownMeta m ->
       Format.fprintf fmt "Metaproperty %s is already registered with \
         a conflicting signature" m.meta_name
-  | BadMetaArity (m,i1,i2) ->
+  | BadMetaArity (m,n) ->
       Format.fprintf fmt "Metaproperty %s requires %d arguments but \
-        is applied to %d" m.meta_name i1 i2
+        is applied to %d" m.meta_name (List.length m.meta_type) n
   | MetaTypeMismatch (m,t1,t2) ->
       Format.fprintf fmt "Metaproperty %s expects %a argument but \
         is applied to %a"

src/core/theory.mli

@@ -220,6 +220,6 @@ exception ClashSymbol of string
 
 exception KnownMeta of meta
 exception UnknownMeta of string
-exception BadMetaArity of meta * int * int
+exception BadMetaArity of meta * int
 exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
 

src/core/ty.ml

@@ -144,7 +144,7 @@ let ty_closed ty = ty_v_all Util.ffalse ty
 
 (* smart constructors *)
 
-exception BadTypeArity of tysymbol * int * int
+exception BadTypeArity of tysymbol * int
 exception DuplicateTypeVar of tvsymbol
 exception UnboundTypeVar of tvsymbol
 
@@ -155,17 +155,15 @@ let create_tysymbol name args def =
   ignore (Opt.map (ty_v_all check) def);
   mk_ts name args def
 
-let ty_app s tl =
-  let tll = List.length tl in
-  let stl = List.length s.ts_args in
-  if tll <> stl then raise (BadTypeArity (s,stl,tll));
-  match s.ts_def with
-    | Some ty ->
-        let add m v t = Mtv.add v t m in
-        let m = List.fold_left2 add Mtv.empty s.ts_args tl in
-        ty_full_inst m ty
-    | _ ->
-        ty_app s tl
+let ty_app s tl = match s.ts_def with
+  | Some ty ->
+      let mv = try List.fold_right2 Mtv.add s.ts_args tl Mtv.empty with
+        | Invalid_argument _ -> raise (BadTypeArity (s, List.length tl)) in
+      ty_full_inst mv ty
+  | None ->
+      if List.length s.ts_args <> List.length tl then
+        raise (BadTypeArity (s, List.length tl));
+      ty_app s tl
 
 (* symbol-wise map/fold *)
 

src/core/ty.mli

@@ -61,7 +61,7 @@ val ty_equal : ty -> ty -> bool
 val ts_hash : tysymbol -> int
 val ty_hash : ty -> int
 
-exception BadTypeArity of tysymbol * int * int
+exception BadTypeArity of tysymbol * int
 exception DuplicateTypeVar of tvsymbol
 exception UnboundTypeVar of tvsymbol
 

src/parser/typing.ml

@@ -326,7 +326,7 @@ and dpat_node loc uc env = function
 
 and dpat_args ls loc uc env el pl =
   let n = List.length el and m = List.length pl in
-  if n <> m then error ~loc (BadArity (ls,n,m));
+  if n <> m then error ~loc (BadArity (ls,m));
   let rec check_arg env = function
     | [], [] ->
         env, []
@@ -402,8 +402,7 @@ and dterm_node ~localize loc uc env = function
   | PPvar x ->
       (* 0-arity symbol (constant) *)
       let s, tyl, ty = specialize_fsymbol x uc in
-      let n = List.length tyl in
-      if n > 0 then error ~loc (BadArity (s,n,0));
+      if tyl <> [] then error ~loc (BadArity (s,0));
       Tapp (s, []), ty
   | PPapp (x, tl) when check_highord uc env x tl ->
       let tl = apply_highord loc x tl in
@@ -666,7 +665,7 @@ and dpat_list uc env ty p =
 
 and dtype_args ~localize ls loc uc env el tl =
   let n = List.length el and m = List.length tl in
-  if n <> m then error ~loc (BadArity (ls,n,m));
+  if n <> m then error ~loc (BadArity (ls,m));
   let rec check_arg = function
     | [], [] ->
         []

src/whyml/mlw_dty.ml

@@ -69,28 +69,24 @@ and reg_refresh mv mr r = match Mreg.find_opt r mr with
       let reg = create_dreg ity in
       Mreg.add r reg mr, reg
 
-let its_app s tl =
-  let add m v t = Mtv.add v t m in
-  let mv = try List.fold_left2 add Mtv.empty s.its_ts.ts_args tl
-    with Invalid_argument _ ->
-      raise (BadItyArity (s, List.length s.its_ts.ts_args, List.length tl)) in
+let its_app s dl =
+  let mv = try List.fold_right2 Mtv.add s.its_ts.ts_args dl Mtv.empty with
+    | Invalid_argument _ -> raise (BadItyArity (s, List.length dl)) in
   match s.its_def with
   | Some ity ->
       snd (ity_inst_fresh mv Mreg.empty ity)
   | None ->
       let _,rl = Lists.map_fold_left (reg_refresh mv) Mreg.empty s.its_regs in
-      its_app_real s tl rl
-
-let ts_app ts dl =
-  let add m v t = Mtv.add v t m in
-  let mv = try List.fold_left2 add Mtv.empty ts.ts_args dl
-    with Invalid_argument _ ->
-      raise (BadTypeArity (ts, List.length ts.ts_args, List.length dl)) in
-  match ts.ts_def with
+      its_app_real s dl rl
+
+let ts_app s dl =
+  let mv = try List.fold_right2 Mtv.add s.ts_args dl Mtv.empty with
+    | Invalid_argument _ -> raise (BadTypeArity (s, List.length dl)) in
+  match s.ts_def with
   | Some ty ->
       snd (ity_inst_fresh mv Mreg.empty (ity_of_ty ty))
   | None ->
-      ts_app_real ts dl
+      ts_app_real s dl
 
 let rec dity_refresh = function
   | Dvar { contents = Dtvs _ } as dity -> dity

src/whyml/mlw_expr.ml

@@ -177,7 +177,7 @@ let make_ppattern pp ?(ghost=false) ity =
         let ppl = try List.map2 mtch pls.pl_args ppl with
           | Not_found -> raise (Term.ConstructorExpected pls.pl_ls)
           | Invalid_argument _ -> raise (Term.BadArity
-              (pls.pl_ls, List.length pls.pl_args, List.length ppl)) in
+              (pls.pl_ls, List.length ppl)) in
         make_app pls.pl_ls ppl ghost ity
     | PPlapp (ls,ppl) ->
         if ls.ls_constr = 0 then
@@ -190,7 +190,7 @@ let make_ppattern pp ?(ghost=false) ity =
         let ppl = try List.map2 mtch ls.ls_args ppl with
           | Not_found -> raise (Term.ConstructorExpected ls)
           | Invalid_argument _ -> raise (Term.BadArity
-              (ls,List.length ls.ls_args,List.length ppl)) in
+              (ls, List.length ppl)) in
         make_app ls ppl ghost ity
     | PPor (pp1,pp2) ->
         let pp1 = make ghost ity pp1 in
@@ -603,8 +603,7 @@ let e_plapp pls el ity =
           | None   -> ps_app pls.pl_ls tl in
         mk_expr (Elogic t) (VTvalue ity) ghost eff syms
     | [],_ | _,[] ->
-        raise (Term.BadArity
-          (pls.pl_ls, List.length pls.pl_args, List.length el))
+        raise (Term.BadArity (pls.pl_ls, List.length el))
     | fd::fdl, ({ e_node = Elogic t } as e)::argl ->
         let t = match t.t_ty with
           | Some _ -> t

src/whyml/mlw_pretty.ml

@@ -426,14 +426,14 @@ let print_pdecl fmt d = match d.pd_node with
 
 let () = Exn_printer.register
   begin fun fmt exn -> match exn with
-  | Mlw_ty.BadItyArity (ts, ts_arg, app_arg) ->
+  | Mlw_ty.BadItyArity (ts, app_arg) ->
       fprintf fmt "Bad type arity: type symbol %a must be applied \
                    to %i arguments, but is applied to %i"
-        print_its ts ts_arg app_arg
-  | Mlw_ty.BadRegArity (ts, ts_arg, app_arg) ->
+        print_its ts (List.length ts.its_ts.ts_args) app_arg
+  | Mlw_ty.BadRegArity (ts, app_arg) ->
       fprintf fmt "Bad region arity: type symbol %a must be applied \
                    to %i regions, but is applied to %i"
-        print_its ts ts_arg app_arg
+        print_its ts (List.length ts.its_regs) app_arg
   | Mlw_ty.DuplicateRegion r ->
       fprintf fmt "Region %a is used twice" print_reg r
   | Mlw_ty.UnboundRegion r ->

src/whyml/mlw_ty.ml

@@ -291,8 +291,8 @@ let lookup_nonghost_reg regs ity =
 
 (* smart constructors *)
 
-exception BadItyArity of itysymbol * int * int
-exception BadRegArity of itysymbol * int * int
+exception BadItyArity of itysymbol * int
+exception BadRegArity of itysymbol * int
 
 exception DuplicateRegion of region
 exception UnboundRegion of region
@@ -389,10 +389,8 @@ and reg_refresh mv mr r = match Mreg.find_opt r mr with
 
 let ity_app_fresh s tl =
   (* type variable map *)
-  let add m v t = Mtv.add v t m in
-  let mv = try List.fold_left2 add Mtv.empty s.its_ts.ts_args tl
-    with Invalid_argument _ ->
-      raise (BadItyArity (s, List.length s.its_ts.ts_args, List.length tl)) in
+  let mv = try List.fold_right2 Mtv.add s.its_ts.ts_args tl Mtv.empty with
+    | Invalid_argument _ -> raise (BadItyArity (s, List.length tl)) in
   (* refresh regions *)
   let mr,rl = Lists.map_fold_left (reg_refresh mv) Mreg.empty s.its_regs in
   let sub = { ity_subst_tv = mv; ity_subst_reg = mr } in
@@ -403,15 +401,12 @@ let ity_app_fresh s tl =
 
 let ity_app s tl rl =
   (* type variable map *)
-  let add m v t = Mtv.add v t m in
-  let mv = try List.fold_left2 add Mtv.empty s.its_ts.ts_args tl
-    with Invalid_argument _ ->
-      raise (BadItyArity (s, List.length s.its_ts.ts_args, List.length tl)) in
+  let mv = try List.fold_right2 Mtv.add s.its_ts.ts_args tl Mtv.empty with
+    | Invalid_argument _ -> raise (BadItyArity (s, List.length tl)) in
   (* region map *)
   let sub = { ity_subst_tv = mv; ity_subst_reg = Mreg.empty } in
-  let sub = try List.fold_left2 reg_match sub s.its_regs rl
-    with Invalid_argument _ ->
-      raise (BadRegArity (s, List.length s.its_regs, List.length rl)) in
+  let sub = try List.fold_left2 reg_match sub s.its_regs rl with
+    | Invalid_argument _ -> raise (BadRegArity (s, List.length rl)) in
   (* every type var and top region in def are in its_ts.ts_args and its_regs *)
   match s.its_def with
   | Some ity -> ity_full_inst sub ity
@@ -419,10 +414,8 @@ let ity_app s tl rl =
 
 let ity_pur s tl =
   (* type variable map *)
-  let add m v t = Mtv.add v t m in
-  let mv = try List.fold_left2 add Mtv.empty s.ts_args tl
-    with Invalid_argument _ ->
-      raise (Ty.BadTypeArity (s, List.length s.ts_args, List.length tl)) in
+  let mv = try List.fold_right2 Mtv.add s.ts_args tl Mtv.empty with
+    | Invalid_argument _ -> raise (Ty.BadTypeArity (s, List.length tl)) in
   let sub = { ity_subst_tv = mv; ity_subst_reg = Mreg.empty } in
   (* every top region in def is guaranteed to be in mr *)
   match s.ts_def with

src/whyml/mlw_ty.mli

@@ -78,8 +78,8 @@ val ity_hash : ity -> int
 val reg_equal : region -> region -> bool
 val reg_hash : region -> int
 
-exception BadItyArity of itysymbol * int * int
-exception BadRegArity of itysymbol * int * int
+exception BadItyArity of itysymbol * int
+exception BadRegArity of itysymbol * int
 exception DuplicateRegion of region
 exception UnboundRegion of region
 

src/whyml/mlw_typing.ml

@@ -368,8 +368,8 @@ and dpat_app denv gloc ({ de_loc = loc } as de) ppl dity =
     | DEglobal_ps ps -> errorm ~loc "%a is not a constructor" print_ps ps
     | _ -> assert false in
   let argl, res = de.de_type in
-  if List.length argl <> List.length ppl then error ~loc:gloc
-    (Term.BadArity (ls, List.length argl, List.length ppl));
+  if List.length argl <> List.length ppl then
+    error ~loc:gloc (Term.BadArity (ls, List.length ppl));
   unify_loc unify gloc res dity;
   let add_pp lp ty (ppl, denv) =
     let pp, denv = dpattern denv lp ty in pp::ppl, denv in