# HG changeset patch # User wenzelm # Date 1266782905 -3600 # Node ID 2cb27605301f122526f2043163ab59aa098fb382 # Parent 0f17eda72e602059495703c3c6b02574fed05153 authentic syntax for *all* term constants; diff -r 0f17eda72e60 -r 2cb27605301f src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Feb 21 21:04:17 2010 +0100 +++ b/src/Pure/Isar/proof_context.ML Sun Feb 21 21:08:25 2010 +0100 @@ -28,7 +28,6 @@ val full_name: Proof.context -> binding -> string val syn_of: Proof.context -> Syntax.syntax val consts_of: Proof.context -> Consts.T - val const_syntax_name: Proof.context -> string -> string val the_const_constraint: Proof.context -> string -> typ val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context @@ -235,7 +234,6 @@ val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of; val consts_of = #1 o #consts o rep_context; -val const_syntax_name = Consts.syntax_name o consts_of; val the_const_constraint = Consts.the_constraint o consts_of; val facts_of = #facts o rep_context; @@ -707,10 +705,10 @@ val consts = consts_of ctxt; in t - |> Sign.extern_term (Consts.extern_early consts) thy + |> Sign.extern_term thy |> Local_Syntax.extern_term syntax - |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (Local_Syntax.syn_of syntax) - (not (PureThy.old_appl_syntax thy)) + |> Syntax.standard_unparse_term (Consts.extern consts) ctxt + (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy)) end; in @@ -990,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 const_syntax_name ctxt c' else c; + val d = if intern then Syntax.constN ^ c' else c; in Syntax.Constant d end | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts); @@ -1018,7 +1016,9 @@ fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx)) | const_syntax ctxt (Const (c, _), mx) = - Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx)) + (case try (Consts.type_scheme (consts_of ctxt)) c of + SOME T => SOME (false, (Syntax.constN ^ c, T, mx)) + | NONE => NONE) | const_syntax _ _ = NONE; in diff -r 0f17eda72e60 -r 2cb27605301f src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Sun Feb 21 21:04:17 2010 +0100 +++ b/src/Pure/ML/ml_antiquote.ML Sun Feb 21 21:08:25 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 ? ProofContext.const_syntax_name ctxt + |> syn ? prefix Syntax.constN |> ML_Syntax.print_string); val _ = inline "const_name" (const false); diff -r 0f17eda72e60 -r 2cb27605301f src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Sun Feb 21 21:04:17 2010 +0100 +++ b/src/Pure/Syntax/syn_trans.ML Sun Feb 21 21:08:25 2010 +0100 @@ -129,13 +129,15 @@ (* type propositions *) -fun mk_type ty = Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty); +fun mk_type ty = + Lexicon.const "_constrain" $ + Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "itself" $ ty); fun ofclass_tr (*"_ofclass"*) [ty, cls] = cls $ mk_type ty | ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts); fun sort_constraint_tr (*"_sort_constraint"*) [ty] = - Lexicon.const "Pure.sort_constraint" $ mk_type ty + Lexicon.const "\\<^const>Pure.sort_constraint" $ mk_type ty | sort_constraint_tr (*"_sort_constraint"*) ts = raise TERM ("sort_constraint_tr", ts); @@ -152,7 +154,7 @@ (case Ast.unfold_ast_p "_asms" asms of (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm'] | _ => raise Ast.AST ("bigimpl_ast_tr", asts)) - in Ast.fold_ast_p "==>" (prems, concl) end + in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts); @@ -350,7 +352,7 @@ (* type propositions *) -fun type_prop_tr' _ (*"_type_prop"*) T [Const ("Pure.sort_constraint", _)] = +fun type_prop_tr' _ (*"_type_prop"*) T [Const ("\\<^const>Pure.sort_constraint", _)] = Lexicon.const "_sort_constraint" $ TypeExt.term_of_typ true T | type_prop_tr' show_sorts (*"_type_prop"*) T [t] = Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t @@ -366,7 +368,7 @@ fun is_prop Ts t = fastype_of1 (Ts, t) = propT handle TERM _ => false; - fun is_term (Const ("Pure.term", _) $ _) = true + fun is_term (Const ("\\<^const>Pure.term", _) $ _) = true | is_term _ = false; fun tr' _ (t as Const _) = t @@ -379,7 +381,7 @@ | tr' Ts (t as Bound _) = if is_prop Ts t then aprop t else t | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t) - | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) = + | tr' Ts (t as t1 $ (t2 as Const ("\\<^const>TYPE", Type ("itself", [T])))) = if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1 else tr' Ts t1 $ tr' Ts t2 | tr' Ts (t as t1 $ t2) = @@ -393,7 +395,7 @@ fun impl_ast_tr' (*"==>"*) asts = if TypeExt.no_brackets () then raise Match else - (case Ast.unfold_ast_p "==>" (Ast.Appl (Ast.Constant "==>" :: asts)) of + (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of (prems as _ :: _ :: _, concl) => let val (asms, asm) = split_last prems; @@ -514,11 +516,13 @@ [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"), ("_pttrns", idtyp_ast_tr' "_pttrns"), - ("==>", impl_ast_tr'), + ("\\<^const>==>", impl_ast_tr'), ("_index", index_ast_tr')]); val pure_trfunsT = - [("_type_prop", type_prop_tr'), ("TYPE", type_tr'), ("_type_constraint_", type_constraint_tr')]; + [("_type_prop", type_prop_tr'), + ("\\<^const>TYPE", type_tr'), + ("_type_constraint_", type_constraint_tr')]; fun struct_trfuns structs = ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]); diff -r 0f17eda72e60 -r 2cb27605301f src/Pure/consts.ML --- a/src/Pure/consts.ML Sun Feb 21 21:04:17 2010 +0100 +++ b/src/Pure/consts.ML Sun Feb 21 21:08:25 2010 +0100 @@ -21,15 +21,13 @@ val space_of: T -> Name_Space.T val is_concealed: T -> string -> bool val intern: T -> xstring -> string + val intern_syntax: T -> xstring -> string val extern: T -> string -> xstring - val extern_early: T -> string -> xstring - val syntax: T -> string * mixfix -> string * typ * mixfix - val syntax_name: T -> string -> string val read_const: T -> string -> term val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*) val typargs: T -> string * typ -> typ list val instance: T -> string * typ list -> typ - val declare: bool -> Name_Space.naming -> binding * typ -> T -> T + val declare: Name_Space.naming -> binding * typ -> T -> T val constrain: string * typ option -> T -> T val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> binding * term -> T -> (term * term) * T @@ -46,7 +44,7 @@ (* datatype T *) -type decl = {T: typ, typargs: int list list, authentic: bool}; +type decl = {T: typ, typargs: int list list}; type abbrev = {rhs: term, normal_rhs: term, force_expand: bool}; datatype T = Consts of @@ -128,18 +126,10 @@ val intern = Name_Space.intern o space_of; val extern = Name_Space.extern o space_of; -fun extern_early consts c = - (case try (the_const consts) c of - SOME ({authentic = true, ...}, _) => Syntax.constN ^ c - | _ => extern consts c); - -fun syntax consts (c, mx) = - let - val ({T, authentic, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg; - val c' = if authentic then Syntax.constN ^ c else Long_Name.base_name c; - in (c', T, mx) end; - -fun syntax_name consts c = #1 (syntax consts (c, NoSyn)); +fun intern_syntax consts name = + (case try (unprefix Syntax.constN) name of + SOME c => c + | NONE => intern consts name); (* read_const *) @@ -231,10 +221,10 @@ (* declarations *) -fun declare authentic naming (b, declT) = +fun declare naming (b, declT) = map_consts (fn (decls, constraints, rev_abbrevs) => let - val decl = {T = declT, typargs = typargs_of declT, authentic = authentic}; + val decl = {T = declT, typargs = typargs_of declT}; val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE)); in (decls', constraints, rev_abbrevs) end); @@ -285,7 +275,7 @@ in consts |> map_consts (fn (decls, constraints, rev_abbrevs) => let - val decl = {T = T, typargs = typargs_of T, authentic = true}; + val decl = {T = T, typargs = typargs_of T}; val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand}; val (_, decls') = decls |> Name_Space.define true naming (b, (decl, SOME abbr)); diff -r 0f17eda72e60 -r 2cb27605301f src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Sun Feb 21 21:04:17 2010 +0100 +++ b/src/Pure/pure_thy.ML Sun Feb 21 21:08:25 2010 +0100 @@ -225,6 +225,7 @@ val typ = Simple_Syntax.read_typ; val prop = Simple_Syntax.read_prop; +val const = prefix Syntax.constN; val typeT = Syntax.typeT; val spropT = Syntax.spropT; @@ -310,11 +311,11 @@ ("_indexvar", typ "index", Delimfix "'\\"), ("_struct", typ "index => logic", Mixfix ("\\_", [1000], 1000)), ("_update_name", typ "idt", NoSyn), - ("==>", typ "prop => prop => prop", Delimfix "op ==>"), - (Term.dummy_patternN, typ "aprop", Delimfix "'_"), + (const "==>", typ "prop => prop => prop", Delimfix "op ==>"), + (const Term.dummy_patternN, typ "aprop", Delimfix "'_"), ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"), - ("Pure.term", typ "logic => prop", Delimfix "TERM _"), - ("Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))] + (const "Pure.term", typ "logic => prop", Delimfix "TERM _"), + (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))] #> Sign.add_syntax_i applC_syntax #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) [("fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), @@ -326,14 +327,14 @@ ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), ("_type_constraint_", typ "'a", NoSyn), ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), - ("==", typ "'a => 'a => prop", Infixr ("\\", 2)), - ("all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), - ("==>", typ "prop => prop => prop", Infixr ("\\", 1)), + (const "==", typ "'a => 'a => prop", Infixr ("\\", 2)), + (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), + (const "==>", typ "prop => prop => prop", Infixr ("\\", 1)), ("_DDDOT", typ "aprop", Delimfix "\\"), ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), ("_DDDOT", typ "logic", Delimfix "\\")] #> Sign.add_modesyntax_i ("", false) - [("prop", typ "prop => prop", Mixfix ("_", [0], 0))] + [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))] #> Sign.add_modesyntax_i ("HTML", false) [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3))] #> Sign.add_consts_i diff -r 0f17eda72e60 -r 2cb27605301f src/Pure/sign.ML --- a/src/Pure/sign.ML Sun Feb 21 21:04:17 2010 +0100 +++ b/src/Pure/sign.ML Sun Feb 21 21:08:25 2010 +0100 @@ -41,7 +41,6 @@ val declared_tyname: theory -> string -> bool val declared_const: theory -> string -> bool val const_monomorphic: theory -> string -> bool - val const_syntax_name: theory -> string -> string val const_typargs: theory -> string * typ -> typ list val const_instance: theory -> string * typ list -> typ val mk_const: theory -> string * typ list -> term @@ -59,7 +58,7 @@ val intern_typ: theory -> typ -> typ val extern_typ: theory -> typ -> typ val intern_term: theory -> term -> term - val extern_term: (string -> xstring) -> theory -> term -> term + val extern_term: theory -> term -> term val intern_tycons: theory -> typ -> typ val arity_number: theory -> string -> int val arity_sorts: theory -> string -> sort -> sort list @@ -226,7 +225,6 @@ val the_const_type = Consts.the_type o consts_of; val const_type = try o the_const_type; val const_monomorphic = Consts.is_monomorphic o consts_of; -val const_syntax_name = Consts.syntax_name o consts_of; val const_typargs = Consts.typargs o consts_of; val const_instance = Consts.instance o consts_of; @@ -299,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; -fun extern_term h = term_mapping extern_class extern_type (K h); +val extern_term = term_mapping extern_class extern_type (fn _ => fn c => Syntax.constN ^ c); val intern_tycons = typ_mapping (K I) intern_type; end; @@ -486,7 +484,10 @@ fun notation add mode args thy = let val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram; - fun const_syntax (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx) + fun const_syntax (Const (c, _), mx) = + (case try (Consts.type_scheme (consts_of thy)) c of + SOME T => SOME (Syntax.constN ^ c, T, mx) + | NONE => NONE) | const_syntax _ = NONE; in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end; @@ -495,14 +496,14 @@ local -fun gen_add_consts parse_typ authentic raw_args thy = +fun gen_add_consts parse_typ raw_args thy = let val ctxt = ProofContext.init thy; val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt; fun prep (b, raw_T, mx) = let val c = full_name thy b; - val c_syn = if authentic then Syntax.constN ^ c else Name.of_binding 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; @@ -510,20 +511,20 @@ val args = map prep raw_args; in thy - |> map_consts (fold (Consts.declare authentic (naming_of thy) o #1) args) + |> map_consts (fold (Consts.declare (naming_of thy) o #1) args) |> add_syntax_i (map #2 args) |> pair (map #3 args) end; in -fun add_consts args = snd o gen_add_consts Syntax.parse_typ false args; -fun add_consts_i args = snd o gen_add_consts (K I) false args; +fun add_consts args = snd o gen_add_consts Syntax.parse_typ args; +fun add_consts_i args = snd o gen_add_consts (K I) args; fun declare_const ((b, T), mx) thy = let val pos = Binding.pos_of b; - val ([const as Const (c, _)], thy') = gen_add_consts (K I) true [(b, T, mx)] thy; + val ([const as Const (c, _)], thy') = gen_add_consts (K I) [(b, T, mx)] thy; val _ = Position.report (Markup.const_decl c) pos; in (const, thy') end;