# HG changeset patch # User krauss # Date 1240300404 -7200 # Node ID 3c7a76e79898668855d22d8d39e444b7bd0bcade # Parent e3bbc2c4c58147226bf6360423b0b3cd60179cae simplify computation and consistency checks of argument counts in the input diff -r e3bbc2c4c581 -r 3c7a76e79898 src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Apr 20 12:27:23 2009 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Apr 21 09:53:24 2009 +0200 @@ -215,21 +215,6 @@ (fname, qs, gs, args, rhs) end -exception ArgumentCount of string - -fun mk_arities fqgars = - let fun f (fname, _, _, args, _) arities = - let val k = length args - in - case Symtab.lookup arities fname of - NONE => Symtab.update (fname, k) arities - | SOME i => (if i = k then arities else raise ArgumentCount fname) - end - in - fold f fqgars Symtab.empty - end - - (* Check for all sorts of errors in the input *) fun check_defs ctxt fixes eqs = let @@ -269,13 +254,14 @@ " occur" ^ plural "s" "" funvars ^ " in function position.", "Misspelled constructor???"]); true) in - fqgar + (fname, length args) end - - val _ = mk_arities (map check eqs) - handle ArgumentCount fname => - error ("Function " ^ quote fname ^ - " has different numbers of arguments in different equations") + + val _ = AList.group (op =) (map check eqs) + |> map (fn (fname, ars) => + length (distinct (op =) ars) = 1 + orelse error ("Function " ^ quote fname ^ + " has different numbers of arguments in different equations")) fun check_sorts ((fname, fT), _) = Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) diff -r e3bbc2c4c581 -r 3c7a76e79898 src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Apr 20 12:27:23 2009 +0200 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Tue Apr 21 09:53:24 2009 +0200 @@ -215,11 +215,11 @@ #> Proof.global_future_terminal_proof (Method.Basic (method, Position.none), NONE) int -fun mk_catchall fixes arities = +fun mk_catchall fixes arity_of = let fun mk_eqn ((fname, fT), _) = let - val n = the (Symtab.lookup arities fname) + val n = arity_of fname val (argTs, rT) = chop n (binder_types fT) |> apsnd (fn Ts => Ts ---> body_type fT) @@ -235,7 +235,12 @@ end fun add_catchall ctxt fixes spec = - spec @ mk_catchall fixes (mk_arities (map (split_def ctxt) spec)) + let val fqgars = map (split_def ctxt) spec + val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars + |> AList.lookup (op =) #> the + in + spec @ mk_catchall fixes arity_of + end fun warn_if_redundant ctxt origs tss = let diff -r e3bbc2c4c581 -r 3c7a76e79898 src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Mon Apr 20 12:27:23 2009 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Tue Apr 21 09:53:24 2009 +0200 @@ -87,12 +87,12 @@ val num = length fs val fnames = map fst fs val fqgars = map (split_def ctxt) eqs - val arities = mk_arities fqgars + val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars + |> AList.lookup (op =) #> the fun curried_types (fname, fT) = let - val k = the_default 1 (Symtab.lookup arities fname) - val (caTs, uaTs) = chop k (binder_types fT) + val (caTs, uaTs) = chop (arity_of fname) (binder_types fT) in (caTs, uaTs ---> body_type fT) end