--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu May 01 09:30:35 2014 +0200
@@ -422,7 +422,7 @@
#> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix
("prob_" ^ str0 (Position.line_of pos) ^ "__")
#> Config.put SMT_Config.debug_files
- (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
+ (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_"
^ serial_string ())
| set_file_name NONE = I
val st' =
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu May 01 09:30:35 2014 +0200
@@ -721,7 +721,7 @@
| is_line_cnf_ueq _ = false
fun open_conjecture_term (ATerm (((s, s'), tys), tms)) =
- ATerm ((if is_tptp_variable s then (s |> Name.desymbolize false, s')
+ ATerm ((if is_tptp_variable s then (s |> Name.desymbolize (SOME false), s')
else (s, s'), tys), tms |> map open_conjecture_term)
| open_conjecture_term _ = raise Fail "unexpected higher-order term"
fun open_formula conj =
@@ -843,7 +843,7 @@
else
s |> no_qualifiers
|> unquote_tvar
- |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
+ |> Name.desymbolize (SOME (Char.isUpper (String.sub (full_name, 0))))
|> (fn s =>
if size s > max_readable_name_size then
String.substring (s, 0, max_readable_name_size div 2 - 4) ^
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu May 01 09:30:35 2014 +0200
@@ -229,7 +229,7 @@
fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s =
(if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
"_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^
- string_of_int index_no ^ "_" ^ Name.desymbolize false s
+ string_of_int index_no ^ "_" ^ Name.desymbolize (SOME false) s
fun cluster_of_zapped_var_name s =
let val get_int = the o Int.fromString o nth (space_explode "_" s) in
--- a/src/HOL/Tools/SMT2/smt2_translate.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML Thu May 01 09:30:35 2014 +0200
@@ -98,7 +98,7 @@
SOME (name, _) => (name, cx)
| NONE =>
let
- val sugg = Name.desymbolize true (suggested_name_of_typ T) ^ safe_suffix
+ val sugg = Name.desymbolize (SOME true) (suggested_name_of_typ T) ^ safe_suffix
val (name, names') = Name.variant sugg names
val typs' = Typtab.update (T, (name, proper)) typs
in (name, (names', typs', terms)) end)
@@ -108,7 +108,7 @@
SOME (name, _) => (name, cx)
| NONE =>
let
- val sugg = Name.desymbolize false (suggested_name_of_term t) ^ safe_suffix
+ val sugg = Name.desymbolize (SOME false) (suggested_name_of_term t) ^ safe_suffix
val (name, names') = Name.variant sugg names
val terms' = Termtab.update (t, (name, sort)) terms
in (name, (names', typs, terms')) end)
--- a/src/HOL/Tools/SMT2/z3_new_proof.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_proof.ML Thu May 01 09:30:35 2014 +0200
@@ -313,7 +313,7 @@
exception Z3_PARSE of string * SMTLIB2.tree
-val desymbolize = Name.desymbolize false o perhaps (try (unprefix "?"))
+val desymbolize = Name.desymbolize (SOME false) o perhaps (try (unprefix "?"))
fun parse_type cx ty Ts =
(case apply_parsers (get_type_parsers (ctxt_of cx)) (ty, Ts) of
--- a/src/Pure/Isar/code.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/Pure/Isar/code.ML Thu May 01 09:30:35 2014 +0200
@@ -621,7 +621,7 @@
fun mk_desymbolization pre post mk vs =
let
val names = map (pre o fst o fst) vs
- |> map (Name.desymbolize false)
+ |> map (Name.desymbolize (SOME false))
|> Name.variant_list []
|> map post;
in map_filter (fn (((v, i), x), v') =>
--- a/src/Pure/ML/ml_antiquotation.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML Thu May 01 09:30:35 2014 +0200
@@ -30,7 +30,7 @@
fun variant a ctxt =
let
val names = Names.get ctxt;
- val (b, names') = Name.variant (Name.desymbolize false a) names;
+ val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names;
val ctxt' = Names.put names' ctxt;
in (b, ctxt') end;
--- a/src/Pure/name.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/Pure/name.ML Thu May 01 09:30:35 2014 +0200
@@ -31,7 +31,7 @@
val invent_list: string list -> string -> int -> string list
val variant: string -> context -> string * context
val variant_list: string list -> string list -> string list
- val desymbolize: bool -> string -> string
+ val desymbolize: bool option -> string -> string
end;
structure Name: NAME =
@@ -150,8 +150,9 @@
(* names conforming to typical requirements of identifiers in the world outside *)
-fun desymbolize upper "" = if upper then "X" else "x"
- | desymbolize upper s =
+fun desymbolize perhaps_upper "" =
+ if the_default false perhaps_upper then "X" else "x"
+ | desymbolize perhaps_upper s =
let
val xs as (x :: _) = Symbol.explode s;
val ys =
@@ -171,10 +172,12 @@
Symbol.Sym name => "_" :: raw_explode name @ sep xs
| _ => sep xs);
fun upper_lower cs =
- if upper then nth_map 0 Symbol.to_ascii_upper cs
- else
- (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
- Symbol.to_ascii_lower cs;
+ case perhaps_upper of
+ NONE => cs
+ | SOME true => nth_map 0 Symbol.to_ascii_upper cs
+ | SOME false =>
+ (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
+ Symbol.to_ascii_lower cs;
in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
end;
--- a/src/Tools/Code/code_symbol.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/Tools/Code/code_symbol.ML Thu May 01 09:30:35 2014 +0200
@@ -83,7 +83,7 @@
structure Graph = Graph(type key = T val ord = symbol_ord);
local
- val base = Name.desymbolize false o Long_Name.base_name;
+ val base = Name.desymbolize (SOME false) o Long_Name.base_name;
fun base_rel (x, y) = base y ^ "_" ^ base x;
in
--- a/src/Tools/Code/code_target.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/Tools/Code/code_target.ML Thu May 01 09:30:35 2014 +0200
@@ -128,14 +128,14 @@
val _ = if s = "" then error "Bad empty code name" else ();
val xs = Long_Name.explode s;
val xs' = if is_module
- then map (Name.desymbolize true) xs
+ then map (Name.desymbolize (SOME true)) xs
else if length xs < 2
then error ("Bad code name without module component: " ^ quote s)
else
let
val (ys, y) = split_last xs;
- val ys' = map (Name.desymbolize true) ys;
- val y' = Name.desymbolize false y;
+ val ys' = map (Name.desymbolize (SOME true)) ys;
+ val y' = Name.desymbolize (SOME false) y;
in ys' @ [y'] end;
in if xs' = xs
then if is_module then (xs, "") else split_last xs
--- a/src/Tools/Code/code_thingol.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu May 01 09:30:35 2014 +0200
@@ -603,7 +603,7 @@
pair (IVar (SOME v))
| translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
let
- val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t);
+ val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize (SOME false) v, ty, t);
val v'' = if member (op =) (Term.add_free_names t' []) v'
then SOME v' else NONE
in