# HG changeset patch # User wenzelm # Date 1307634709 -7200 # Node ID 47cf4bc789aa9a2464d5b235cafc99ec6f0af0d1 # Parent 4384f4ae0574a9ed6ca962786dff6adcb3dc4c5b simplified Name.variant -- discontinued builtin fold_map; diff -r 4384f4ae0574 -r 47cf4bc789aa doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Thu Jun 09 17:46:25 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Thu Jun 09 17:51:49 2011 +0200 @@ -855,7 +855,7 @@ @{index_ML Name.context: Name.context} \\ @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\ @{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\ - @{index_ML Name.variants: "string list -> Name.context -> string list * Name.context"} \\ + @{index_ML Name.variant: "string -> Name.context -> string * Name.context"} \\ \end{mldecls} \begin{mldecls} @{index_ML Variable.names_of: "Proof.context -> Name.context"} \\ @@ -878,8 +878,8 @@ \item @{ML Name.invents}~@{text "context name n"} produces @{text "n"} fresh names derived from @{text "name"}. - \item @{ML Name.variants}~@{text "names context"} produces fresh - variants of @{text "names"}; the result is entered into the context. + \item @{ML Name.variant}~@{text "name context"} produces a fresh + variant of @{text "name"}; the result is declared to the context. \item @{ML Variable.names_of}~@{text "ctxt"} retrieves the context of declared type and term variable names. Projecting a proof @@ -901,7 +901,7 @@ @{assert} (list1 = ["a", "b", "c", "d", "e"]); val list2 = - #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] Name.context); + #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] Name.context); @{assert} (list2 = ["x", "xa", "a", "aa", "'a", "'aa"]); *} @@ -918,7 +918,7 @@ @{assert} (list1 = ["d", "e", "f", "g", "h"]); val list2 = - #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] names); + #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] names); @{assert} (list2 = ["x", "xa", "aa", "ab", "'aa", "'ab"]); *} diff -r 4384f4ae0574 -r 47cf4bc789aa doc-src/IsarImplementation/Thy/document/Prelim.tex --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Thu Jun 09 17:46:25 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Thu Jun 09 17:51:49 2011 +0200 @@ -1255,7 +1255,7 @@ \indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\ \indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\ \indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\ - \indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\ + \indexdef{}{ML}{Name.variant}\verb|Name.variant: string -> Name.context -> string * Name.context| \\ \end{mldecls} \begin{mldecls} \indexdef{}{ML}{Variable.names\_of}\verb|Variable.names_of: Proof.context -> Name.context| \\ @@ -1277,8 +1277,8 @@ \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}. - \item \verb|Name.variants|~\isa{names\ context} produces fresh - variants of \isa{names}; the result is entered into the context. + \item \verb|Name.variant|~\isa{name\ context} produces a fresh + variant of \isa{name}; the result is declared to the context. \item \verb|Variable.names_of|~\isa{ctxt} retrieves the context of declared type and term variable names. Projecting a proof @@ -1333,7 +1333,7 @@ \ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}b{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline \isanewline \ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline -\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}Name{\isaliteral{2E}{\isachardot}}variants\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ Name{\isaliteral{2E}{\isachardot}}context{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}fold{\isaliteral{5F}{\isacharunderscore}}map\ Name{\isaliteral{2E}{\isachardot}}variant\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ Name{\isaliteral{2E}{\isachardot}}context{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline \ \ % \isaantiq assert{}% @@ -1378,7 +1378,7 @@ \ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}g{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}h{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline \isanewline \ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline -\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}Name{\isaliteral{2E}{\isachardot}}variants\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ names{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}fold{\isaliteral{5F}{\isacharunderscore}}map\ Name{\isaliteral{2E}{\isachardot}}variant\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ names{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline \ \ % \isaantiq assert{}% diff -r 4384f4ae0574 -r 47cf4bc789aa src/HOL/Boogie/Tools/boogie_loader.ML --- a/src/HOL/Boogie/Tools/boogie_loader.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Thu Jun 09 17:51:49 2011 +0200 @@ -446,8 +446,7 @@ val nctxt = Name.make_context (duplicates (op =) (names_of t [])) fun fresh (i, nctxt) = (position_prefix ^ string_of_int i, (i+1, nctxt)) - fun renamed n (i, nctxt) = - yield_singleton Name.variants n nctxt ||> pair i + fun renamed n (i, nctxt) = Name.variant n nctxt ||> pair i fun mk_label (name, t) = @{term assert_at} $ Free (name, @{typ bool}) $ t fun unique t = @@ -472,11 +471,11 @@ all_names |> map_filter (try (fn n => (n, short_var_name n))) |> split_list - ||>> (fn names => Name.variants names (Name.make_context all_names)) + ||>> (fn names => fold_map Name.variant names (Name.make_context all_names)) |>> Symtab.make o (op ~~) fun rename_free n = the_default n (Symtab.lookup names n) - fun rename_abs n = yield_singleton Name.variants (short_var_name n) + fun rename_abs n = Name.variant (short_var_name n) fun rename _ (Free (n, T)) = Free (rename_free n, T) | rename nctxt (Abs (n, T, t)) = diff -r 4384f4ae0574 -r 47cf4bc789aa src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Thu Jun 09 17:51:49 2011 +0200 @@ -200,7 +200,7 @@ val ind_sort = if null atomTs then HOLogic.typeS else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs)); - val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt'); + val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt'); val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt'; val fsT = TFree (fs_ctxt_tyname, ind_sort); diff -r 4384f4ae0574 -r 47cf4bc789aa src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Jun 09 17:51:49 2011 +0200 @@ -226,7 +226,7 @@ val ind_sort = if null atomTs then HOLogic.typeS else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy ("fs_" ^ Long_Name.base_name a)) atoms)); - val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt'); + val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt'); val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt'; val fsT = TFree (fs_ctxt_tyname, ind_sort); diff -r 4384f4ae0574 -r 47cf4bc789aa src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Thu Jun 09 17:51:49 2011 +0200 @@ -36,7 +36,7 @@ let val (vs, Ts) = split_list (strip_qnt_vars "all" t); val body = strip_qnt_body "all" t; - val (vs', _) = Name.variants vs (Name.make_context (fold_aterms + val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) body [])) in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end; diff -r 4384f4ae0574 -r 47cf4bc789aa src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Thu Jun 09 17:51:49 2011 +0200 @@ -136,7 +136,7 @@ fun mk_variables thy prfx xs ty (tab, ctxt) = let val T = mk_type thy prfx ty; - val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt; + val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt; val zs = map (Free o rpair T) ys; in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end; @@ -779,7 +779,7 @@ map_filter (fn s => lookup funs s |> Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |> split_list ||> split_list; - val (fs', ctxt') = Name.variants fs ctxt + val (fs', ctxt') = fold_map Name.variant fs ctxt in (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns, Element.Fixes (map2 (fn s => fn T => diff -r 4384f4ae0574 -r 47cf4bc789aa src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Jun 09 17:51:49 2011 +0200 @@ -134,7 +134,7 @@ val names = map Long_Name.base_name (the_default tycos (#alt_names info)); val (auxnames, _) = Name.make_context names - |> fold_map (yield_singleton Name.variants o Datatype_Aux.name_of_typ) Us; + |> fold_map (Name.variant o Datatype_Aux.name_of_typ) Us; val prefix = space_implode "_" names; in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end; diff -r 4384f4ae0574 -r 47cf4bc789aa src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 09 17:51:49 2011 +0200 @@ -542,7 +542,7 @@ fun focus_ex t nctxt = let val ((xs, Ts), t') = apfst split_list (strip_ex t) - val (xs', nctxt') = Name.variants xs nctxt; + val (xs', nctxt') = fold_map Name.variant xs nctxt; val ps' = xs' ~~ Ts; val vs = map Free ps'; val t'' = Term.subst_bounds (rev vs, t'); diff -r 4384f4ae0574 -r 47cf4bc789aa src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Jun 09 17:51:49 2011 +0200 @@ -84,8 +84,8 @@ val (argTs, resT) = strip_type (fastype_of func) val nctxt = Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) []) - val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt - val ([resname], nctxt'') = Name.variants ["r"] nctxt' + val (argnames, nctxt') = fold_map Name.variant (replicate (length argTs) "a") nctxt + val (resname, nctxt'') = Name.variant "r" nctxt' val args = map Free (argnames ~~ argTs) val res = Free (resname, resT) in Logic.mk_equals diff -r 4384f4ae0574 -r 47cf4bc789aa src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/HOL/Tools/primrec.ML Thu Jun 09 17:51:49 2011 +0200 @@ -38,7 +38,7 @@ let val (vs, Ts) = split_list (strip_qnt_vars "all" spec); val body = strip_qnt_body "all" spec; - val (vs', _) = Name.variants vs (Name.make_context (fold_aterms + val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) body [])); val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body; val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn) diff -r 4384f4ae0574 -r 47cf4bc789aa src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Pure/Isar/code.ML Thu Jun 09 17:51:49 2011 +0200 @@ -1145,8 +1145,8 @@ fun case_cong thy case_const (num_args, (pos, _)) = let - val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context; - val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt; + val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context; + val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt; val (ws, vs) = chop pos zs; val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const); val Ts = binder_types T; diff -r 4384f4ae0574 -r 47cf4bc789aa src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Pure/ML/ml_antiquote.ML Thu Jun 09 17:51:49 2011 +0200 @@ -29,7 +29,7 @@ fun variant a ctxt = let val names = Names.get ctxt; - val ([b], names') = Name.variants [a] names; + val (b, names') = Name.variant a names; val ctxt' = Names.put names' ctxt; in (b, ctxt') end; diff -r 4384f4ae0574 -r 47cf4bc789aa src/Pure/Proof/proofchecker.ML --- a/src/Pure/Proof/proofchecker.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Pure/Proof/proofchecker.ML Thu Jun 09 17:51:49 2011 +0200 @@ -100,7 +100,7 @@ | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) = let - val ([x], names') = Name.variants [s] names; + val (x, names') = Name.variant s names; val thm = thm_of ((x, T) :: vs, names') Hs prf in Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm diff -r 4384f4ae0574 -r 47cf4bc789aa src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Pure/Syntax/syntax_trans.ML Thu Jun 09 17:51:49 2011 +0200 @@ -439,7 +439,7 @@ (* dependent / nondependent quantifiers *) fun var_abs mark (x, T, b) = - let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context) + let val (x', _) = Name.variant x (Term.declare_term_names b Name.context) in (x', subst_bound (mark (x', T), b)) end; val variant_abs = var_abs Free; diff -r 4384f4ae0574 -r 47cf4bc789aa src/Pure/name.ML --- a/src/Pure/name.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Pure/name.ML Thu Jun 09 17:51:49 2011 +0200 @@ -24,7 +24,7 @@ val invents: context -> string -> int -> string list val names: context -> string -> 'a list -> (string * 'a) list val invent_list: string list -> string -> int -> string list - val variants: string list -> context -> string list * context + val variant: string -> context -> string * context val variant_list: string list -> string list -> string list val desymbolize: bool -> string -> string end; @@ -115,7 +115,7 @@ (*makes a variant of a name distinct from already used names in a context; preserves a suffix of underscores "_"*) -val variants = fold_map (fn name => fn ctxt => +fun variant name ctxt = let fun vary x = (case declared ctxt x of @@ -133,9 +133,9 @@ |> x0 <> x' ? declare_renaming (x0, x') |> declare x'; in (x', ctxt') end; - in (x' ^ replicate_string n "_", ctxt') end); + in (x' ^ replicate_string n "_", ctxt') end; -fun variant_list used names = #1 (make_context used |> variants names); +fun variant_list used names = #1 (make_context used |> fold_map variant names); (* names conforming to typical requirements of identifiers in the world outside *) diff -r 4384f4ae0574 -r 47cf4bc789aa src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Pure/proofterm.ML Thu Jun 09 17:51:49 2011 +0200 @@ -657,7 +657,7 @@ (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t []; val used = Name.context |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t; - val fmap = fs ~~ #1 (Name.variants (map fst fs) used); + val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used); fun thaw (f as (a, S)) = (case AList.lookup (op =) fmap f of NONE => TFree f diff -r 4384f4ae0574 -r 47cf4bc789aa src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Pure/raw_simplifier.ML Thu Jun 09 17:51:49 2011 +0200 @@ -305,7 +305,7 @@ fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t = let val names = Term.declare_term_names t Name.context; - val xs = rev (#1 (Name.variants (rev (map #2 bs)) names)); + val xs = rev (#1 (fold_map Name.variant (rev (map #2 bs)) names)); fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T)); in Term.subst_atomic (ListPair.map subst (bs, xs)) t end; diff -r 4384f4ae0574 -r 47cf4bc789aa src/Pure/term.ML --- a/src/Pure/term.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Pure/term.ML Thu Jun 09 17:51:49 2011 +0200 @@ -514,7 +514,8 @@ val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I); fun variant_frees t frees = - fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees; + fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~ + map snd frees; fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*) @@ -705,7 +706,7 @@ fun strip_abs t (0, used) = (([], t), (0, used)) | strip_abs (Abs (v, T, t)) (k, used) = let - val ([v'], used') = Name.variants [v] used; + val (v', used') = Name.variant v used; val t' = subst_bound (Free (v', T), t); val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used'); in (((v', T) :: vs, t''), (k', used'')) end @@ -713,7 +714,7 @@ fun expand_eta [] t _ = ([], t) | expand_eta (T::Ts) t used = let - val ([v], used') = Name.variants [""] used; + val (v, used') = Name.variant "" used; val (vs, t') = expand_eta Ts (t $ Free (v, T)) used'; in ((v, T) :: vs, t') end; val ((vs1, t'), (k', used')) = strip_abs t (k, used); diff -r 4384f4ae0574 -r 47cf4bc789aa src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Pure/term_subst.ML Thu Jun 09 17:51:49 2011 +0200 @@ -163,7 +163,7 @@ fun zero_var_inst vars = fold (fn v as ((x, i), X) => fn (inst, used) => let - val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used; + val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used; in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end) vars ([], Name.context) |> #1; diff -r 4384f4ae0574 -r 47cf4bc789aa src/Pure/type.ML --- a/src/Pure/type.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Pure/type.ML Thu Jun 09 17:51:49 2011 +0200 @@ -345,7 +345,7 @@ (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t []; val used = Name.context |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t; - val fmap = fs ~~ map (rpair 0) (#1 (Name.variants (map fst fs) used)); + val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used)); fun thaw (f as (_, S)) = (case AList.lookup (op =) fmap f of NONE => TFree f diff -r 4384f4ae0574 -r 47cf4bc789aa src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Pure/variable.ML Thu Jun 09 17:51:49 2011 +0200 @@ -255,7 +255,7 @@ fun variant_frees ctxt ts frees = let val names = names_of (fold declare_names ts ctxt); - val xs = fst (Name.variants (map #1 frees) names); + val xs = fst (fold_map Name.variant (map #1 frees) names); in xs ~~ map snd frees end; @@ -365,7 +365,7 @@ val xs = map check_name bs; val names = names_of ctxt; val (xs', names') = - if is_body ctxt then Name.variants xs names |>> map Name.skolem + if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem else (xs, fold Name.declare xs names); in ctxt |> new_fixes names' xs xs' (map Binding.pos_of bs) end; @@ -373,7 +373,7 @@ let val names = names_of ctxt; val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs; - val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem); + val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem); in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end; end; diff -r 4384f4ae0574 -r 47cf4bc789aa src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Tools/Code/code_haskell.ML Thu Jun 09 17:51:49 2011 +0200 @@ -264,13 +264,12 @@ let fun namify_fun upper base (nsp_fun, nsp_typ) = let - val (base', nsp_fun') = yield_singleton Name.variants - (if upper then first_upper base else base) nsp_fun; + val (base', nsp_fun') = + Name.variant (if upper then first_upper base else base) nsp_fun; in (base', (nsp_fun', nsp_typ)) end; fun namify_typ base (nsp_fun, nsp_typ) = let - val (base', nsp_typ') = yield_singleton Name.variants - (first_upper base) nsp_typ + val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ; in (base', (nsp_fun, nsp_typ')) end; fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair | namify_stmt (Code_Thingol.Fun _) = namify_fun false diff -r 4384f4ae0574 -r 47cf4bc789aa src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Tools/Code/code_ml.ML Thu Jun 09 17:51:49 2011 +0200 @@ -715,12 +715,12 @@ let fun namify_const upper base (nsp_const, nsp_type) = let - val (base', nsp_const') = yield_singleton Name.variants - (if upper then first_upper base else base) nsp_const + val (base', nsp_const') = + Name.variant (if upper then first_upper base else base) nsp_const in (base', (nsp_const', nsp_type)) end; fun namify_type base (nsp_const, nsp_type) = let - val (base', nsp_type') = yield_singleton Name.variants base nsp_type + val (base', nsp_type') = Name.variant base nsp_type in (base', (nsp_const, nsp_type')) end; fun namify_stmt (Code_Thingol.Fun _) = namify_const false | namify_stmt (Code_Thingol.Datatype _) = namify_type diff -r 4384f4ae0574 -r 47cf4bc789aa src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Tools/Code/code_namespace.ML Thu Jun 09 17:51:49 2011 +0200 @@ -46,8 +46,7 @@ let fun alias_fragments name = case module_alias name of SOME name' => Long_Name.explode name' - | NONE => map (fn name => fst (yield_singleton Name.variants name reserved)) - (Long_Name.explode name); + | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name); val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program []; in fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name)) diff -r 4384f4ae0574 -r 47cf4bc789aa src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Tools/Code/code_printer.ML Thu Jun 09 17:51:49 2011 +0200 @@ -165,7 +165,7 @@ fun intro_vars names (namemap, namectxt) = let - val (names', namectxt') = Name.variants names namectxt; + val (names', namectxt') = fold_map Name.variant names namectxt; val namemap' = fold2 (curry Symtab.update) names names' namemap; in (namemap', namectxt') end; @@ -186,7 +186,7 @@ val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE); val x = singleton (Name.variant_list (map_filter I fished1)) "x"; val fished2 = map_index (fillup_param x) fished1; - val (fished3, _) = Name.variants fished2 Name.context; + val (fished3, _) = fold_map Name.variant fished2 Name.context; val vars' = intro_vars fished3 vars; in map (lookup_var vars') fished3 end; diff -r 4384f4ae0574 -r 47cf4bc789aa src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Tools/Code/code_scala.ML Thu Jun 09 17:51:49 2011 +0200 @@ -294,16 +294,16 @@ in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end; fun namify_class base ((nsp_class, nsp_object), nsp_common) = let - val (base', nsp_class') = yield_singleton Name.variants base nsp_class + val (base', nsp_class') = Name.variant base nsp_class in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end; fun namify_object base ((nsp_class, nsp_object), nsp_common) = let - val (base', nsp_object') = yield_singleton Name.variants base nsp_object + val (base', nsp_object') = Name.variant base nsp_object in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end; fun namify_common upper base ((nsp_class, nsp_object), nsp_common) = let val (base', nsp_common') = - yield_singleton Name.variants (if upper then first_upper base else base) nsp_common + Name.variant (if upper then first_upper base else base) nsp_common in (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) diff -r 4384f4ae0574 -r 47cf4bc789aa src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Tools/Code/code_thingol.ML Thu Jun 09 17:51:49 2011 +0200 @@ -354,7 +354,7 @@ fun add_variant update (thing, name) (tab, used) = let - val (name', used') = yield_singleton Name.variants name used; + val (name', used') = Name.variant name used; val tab' = update (thing, name') tab; in (tab', used') end; diff -r 4384f4ae0574 -r 47cf4bc789aa src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Jun 09 17:46:25 2011 +0200 +++ b/src/Tools/induct.ML Thu Jun 09 17:51:49 2011 +0200 @@ -692,7 +692,7 @@ | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt) | add (SOME (NONE, (t, _))) ctxt = let - val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt); + val (s, _) = Name.variant "x" (Variable.names_of ctxt); val ([(lhs, (_, th))], ctxt') = Local_Defs.add_defs [((Binding.name s, NoSyn), (Thm.empty_binding, t))] ctxt