# HG changeset patch # User wenzelm # Date 1266788102 -3600 # Node ID 9ea4445d2ccf30a8f615ffbece5a26c407fd94ce # Parent 40c37da7af546e58d33041e6666b4fd32b56d0d6 slightly more abstract syntax mark/unmark operations; diff -r 40c37da7af54 -r 9ea4445d2ccf src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Sun Feb 21 22:35:02 2010 +0100 @@ -422,8 +422,7 @@ | _ => NONE; val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of; -val dest_case' = gen_dest_case - (try (dest_Const #> fst #> unprefix Syntax.constN)) (K dummyT); +val dest_case' = gen_dest_case (try (dest_Const #> fst #> Syntax.unmark_const)) (K dummyT); (* destruct nested patterns *) @@ -461,7 +460,7 @@ Syntax.const @{syntax_const "_case1"} $ map_aterms (fn Free p => Syntax.mark_boundT p - | Const (s, _) => Syntax.const (Syntax.constN ^ s) + | Const (s, _) => Syntax.const (Syntax.mark_const s) | t => t) pat $ map_aterms (fn x as Free (s, T) => diff -r 40c37da7af54 -r 9ea4445d2ccf src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Sun Feb 21 22:35:02 2010 +0100 @@ -223,7 +223,7 @@ fun add_case_tr' case_names thy = Sign.add_advanced_trfuns ([], [], map (fn case_name => - let val case_name' = Syntax.constN ^ case_name + let val case_name' = Syntax.mark_const case_name in (case_name', Datatype_Case.case_tr' info_of_case case_name') end) case_names, []) thy; diff -r 40c37da7af54 -r 9ea4445d2ccf src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/HOL/Tools/record.ML Sun Feb 21 22:35:02 2010 +0100 @@ -799,7 +799,7 @@ let val (args, rest) = split_args (map fst (but_last fields)) fargs; val more' = mk_ext rest; - in list_comb (Syntax.const (Syntax.constN ^ ext ^ extN), args @ [more']) end + in list_comb (Syntax.const (Syntax.mark_const (ext ^ extN)), args @ [more']) end | NONE => err ("no fields defined for " ^ ext)) | NONE => err (name ^ " is no proper field")) | mk_ext [] = more; @@ -977,7 +977,7 @@ fun strip_fields t = (case strip_comb t of (Const (ext, _), args as (_ :: _)) => - (case try (unprefix Syntax.constN o unsuffix extN) ext of + (case try (Syntax.unmark_const o unsuffix extN) ext of SOME ext' => (case get_extfields thy ext' of SOME fields => @@ -1004,7 +1004,7 @@ fun record_ext_tr' name = let - val ext_name = Syntax.constN ^ name ^ extN; + val ext_name = Syntax.mark_const (name ^ extN); fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts)); in (ext_name, tr') end; @@ -1024,7 +1024,7 @@ if null (loose_bnos t) then t else raise Match | _ => raise Match); in - (case try (unprefix Syntax.constN) c |> Option.map extern of + (case Option.map extern (try Syntax.unmark_const c) of SOME update_name => (case try (unsuffix updateN) update_name of SOME name => @@ -1046,7 +1046,7 @@ fun field_update_tr' name = let - val update_name = Syntax.constN ^ name ^ updateN; + val update_name = Syntax.mark_const (name ^ updateN); fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u) | tr' _ _ = raise Match; in (update_name, tr') end; diff -r 40c37da7af54 -r 9ea4445d2ccf src/HOL/Tools/string_syntax.ML --- a/src/HOL/Tools/string_syntax.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/HOL/Tools/string_syntax.ML Sun Feb 21 22:35:02 2010 +0100 @@ -16,11 +16,11 @@ (* nibble *) val mk_nib = - Syntax.Constant o prefix Syntax.constN o + Syntax.Constant o Syntax.mark_const o fst o Term.dest_Const o HOLogic.mk_nibble; fun dest_nib (Syntax.Constant s) = - (case try (unprefix Syntax.constN) s of + (case try Syntax.unmark_const s of NONE => raise Match | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match)); diff -r 40c37da7af54 -r 9ea4445d2ccf src/HOL/ex/Binary.thy --- a/src/HOL/ex/Binary.thy Sun Feb 21 21:41:29 2010 +0100 +++ b/src/HOL/ex/Binary.thy Sun Feb 21 22:35:02 2010 +0100 @@ -191,7 +191,7 @@ parse_translation {* let val syntax_consts = - map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a); + map_aterms (fn Const (c, T) => Const (Syntax.mark_const c, T) | a => a); fun binary_tr [Const (num, _)] = let diff -r 40c37da7af54 -r 9ea4445d2ccf src/HOLCF/Tools/Domain/domain_syntax.ML --- a/src/HOLCF/Tools/Domain/domain_syntax.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Sun Feb 21 22:35:02 2010 +0100 @@ -114,7 +114,7 @@ (* ----- case translation --------------------------------------------------- *) - fun syntax b = Syntax.constN ^ Sign.full_bname thy b; + fun syntax b = Syntax.mark_const (Sign.full_bname thy b); local open Syntax in local diff -r 40c37da7af54 -r 9ea4445d2ccf src/HOLCF/Tools/cont_consts.ML --- a/src/HOLCF/Tools/cont_consts.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/HOLCF/Tools/cont_consts.ML Sun Feb 21 22:35:02 2010 +0100 @@ -46,7 +46,7 @@ *) fun transform thy (c, T, mx) = let - fun syntax b = Syntax.constN ^ Sign.full_bname thy b; + fun syntax b = Syntax.mark_const (Sign.full_bname thy b); val c1 = Binding.name_of c; val c2 = c1 ^ "_cont_syntax"; val n = Syntax.mixfix_args mx; diff -r 40c37da7af54 -r 9ea4445d2ccf src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/Pure/Isar/expression.ML Sun Feb 21 22:35:02 2010 +0100 @@ -604,7 +604,7 @@ (* achieve plain syntax for locale predicates (without "PROP") *) -fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args => +fun aprop_tr' n c = (Syntax.mark_const c, fn ctxt => fn args => if length args = n then Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *) Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) diff -r 40c37da7af54 -r 9ea4445d2ccf src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/Pure/Isar/proof_context.ML Sun Feb 21 22:35:02 2010 +0100 @@ -988,7 +988,7 @@ fun const_ast_tr intern ctxt [Syntax.Variable c] = let val Const (c', _) = read_const_proper ctxt c; - val d = if intern then Syntax.constN ^ c' else c; + val d = if intern then Syntax.mark_const c' else c; in Syntax.Constant d end | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts); @@ -1017,7 +1017,7 @@ fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx)) | const_syntax ctxt (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of ctxt)) c of - SOME T => SOME (false, (Syntax.constN ^ c, T, mx)) + SOME T => SOME (false, (Syntax.mark_const c, T, mx)) | NONE => NONE) | const_syntax _ _ = NONE; diff -r 40c37da7af54 -r 9ea4445d2ccf src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/Pure/ML/ml_antiquote.ML Sun Feb 21 22:35:02 2010 +0100 @@ -114,7 +114,7 @@ fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) => #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c)) - |> syn ? prefix Syntax.constN + |> syn ? Syntax.mark_const |> ML_Syntax.print_string); val _ = inline "const_name" (const false); diff -r 40c37da7af54 -r 9ea4445d2ccf src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Sun Feb 21 22:35:02 2010 +0100 @@ -67,8 +67,8 @@ ("", paramT --> paramsT, Delimfix "_")] |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\_./ _)", [0, 3], 3)), - (Syntax.constN ^ "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4)), - (Syntax.constN ^ "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] + (Syntax.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4)), + (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] |> Sign.add_modesyntax_i ("latex", false) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\_./ _)", [0, 3], 3))] |> Sign.add_trrules_i (map Syntax.ParsePrintRule @@ -78,10 +78,10 @@ [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]), (Syntax.mk_appl (Constant "_Lam") [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"], - Syntax.mk_appl (Constant (Syntax.constN ^ "AbsP")) [Variable "A", + Syntax.mk_appl (Constant (Syntax.mark_const "AbsP")) [Variable "A", (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]), (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"], - Syntax.mk_appl (Constant (Syntax.constN ^ "Abst")) + Syntax.mk_appl (Constant (Syntax.mark_const "Abst")) [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]); diff -r 40c37da7af54 -r 9ea4445d2ccf src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/Pure/Syntax/lexicon.ML Sun Feb 21 22:35:02 2010 +0100 @@ -31,7 +31,11 @@ val read_xnum: string -> {radix: int, leading_zeros: int, value: int} val read_float: string -> {mant: int, exp: int} val fixedN: string + val mark_fixed: string -> string + val unmark_fixed: string -> string val constN: string + val mark_const: string -> string + val unmark_const: string -> string end; signature LEXICON = @@ -331,8 +335,13 @@ (* specific identifiers *) +val fixedN = "\\<^fixed>"; +val mark_fixed = prefix fixedN; +val unmark_fixed = unprefix fixedN; + val constN = "\\<^const>"; -val fixedN = "\\<^fixed>"; +val mark_const = prefix constN; +val unmark_const = unprefix constN; (* read numbers *) diff -r 40c37da7af54 -r 9ea4445d2ccf src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/Pure/Syntax/printer.ML Sun Feb 21 22:35:02 2010 +0100 @@ -321,10 +321,10 @@ else pr, args)) and atomT a = - (case try (unprefix Lexicon.constN) a of + (case try Lexicon.unmark_const a of SOME c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c)) | NONE => - (case try (unprefix Lexicon.fixedN) a of + (case try Lexicon.unmark_fixed a of SOME x => the (token_trans "_free" x) | NONE => Pretty.str a)) @@ -340,8 +340,8 @@ let val nargs = length args; val markup = Pretty.mark - (Markup.const (unprefix Lexicon.constN a) handle Fail _ => - (Markup.fixed (unprefix Lexicon.fixedN a))) + (Markup.const (Lexicon.unmark_const a) handle Fail _ => + (Markup.fixed (Lexicon.unmark_fixed a))) handle Fail _ => I; (*find matching table entry, or print as prefix / postfix*) diff -r 40c37da7af54 -r 9ea4445d2ccf src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/Pure/Syntax/type_ext.ML Sun Feb 21 22:35:02 2010 +0100 @@ -123,7 +123,9 @@ | decode (t $ u) = decode t $ decode u | decode (Const (a, T)) = let val c = - (case try (unprefix Lexicon.constN) a of SOME c => c | NONE => snd (map_const a)) + (case try Lexicon.unmark_const a of + SOME c => c + | NONE => snd (map_const a)) in Const (c, map_type T) end | decode (Free (a, T)) = (case (map_free a, map_const a) of diff -r 40c37da7af54 -r 9ea4445d2ccf src/Pure/consts.ML --- a/src/Pure/consts.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/Pure/consts.ML Sun Feb 21 22:35:02 2010 +0100 @@ -127,7 +127,7 @@ val extern = Name_Space.extern o space_of; fun intern_syntax consts name = - (case try (unprefix Syntax.constN) name of + (case try Syntax.unmark_const name of SOME c => c | NONE => intern consts name); diff -r 40c37da7af54 -r 9ea4445d2ccf src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/Pure/pure_thy.ML Sun Feb 21 22:35:02 2010 +0100 @@ -225,7 +225,7 @@ val typ = Simple_Syntax.read_typ; val prop = Simple_Syntax.read_prop; -val const = prefix Syntax.constN; +val const = Syntax.mark_const; val typeT = Syntax.typeT; val spropT = Syntax.spropT; diff -r 40c37da7af54 -r 9ea4445d2ccf src/Pure/sign.ML --- a/src/Pure/sign.ML Sun Feb 21 21:41:29 2010 +0100 +++ b/src/Pure/sign.ML Sun Feb 21 22:35:02 2010 +0100 @@ -297,7 +297,7 @@ val intern_typ = typ_mapping intern_class intern_type; val extern_typ = typ_mapping extern_class extern_type; val intern_term = term_mapping intern_class intern_type intern_const; -val extern_term = term_mapping extern_class extern_type (fn _ => fn c => Syntax.constN ^ c); +val extern_term = term_mapping extern_class extern_type (K Syntax.mark_const); val intern_tycons = typ_mapping (K I) intern_type; end; @@ -486,7 +486,7 @@ val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram; fun const_syntax (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of thy)) c of - SOME T => SOME (Syntax.constN ^ c, T, mx) + SOME T => SOME (Syntax.mark_const c, T, mx) | NONE => NONE) | const_syntax _ = NONE; in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end; @@ -503,11 +503,10 @@ fun prep (b, raw_T, mx) = let val c = full_name thy b; - val c_syn = Syntax.constN ^ c; val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg => cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b)); val T' = Logic.varifyT T; - in ((b, T'), (c_syn, T', mx), Const (c, T)) end; + in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end; val args = map prep raw_args; in thy