# HG changeset patch # User wenzelm # Date 1266532994 -3600 # Node ID 298f729f4fac4ab690a6f33ed16cd7aabe2cef93 # Parent 01e9684324676310d9deb10f1cffcc992a31224d# Parent 6f5b716b85000347e50e4939f6e653d059714425 merged diff -r 01e968432467 -r 298f729f4fac src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/HOL/Tools/typedef.ML Thu Feb 18 23:43:14 2010 +0100 @@ -14,10 +14,10 @@ Rep_induct: thm, Abs_induct: thm} val add_typedef: bool -> binding option -> binding * string list * mixfix -> term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory - val typedef: (bool * binding) * (binding * string list * mixfix) * term - * (binding * binding) option -> theory -> Proof.state - val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string - * (binding * binding) option -> theory -> Proof.state + val typedef: (bool * binding) * (binding * string list * mixfix) * term * + (binding * binding) option -> theory -> Proof.state + val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string * + (binding * binding) option -> theory -> Proof.state val get_info: theory -> string -> info option val the_info: theory -> string -> info val interpretation: (string -> theory -> theory) -> theory -> theory @@ -118,9 +118,9 @@ fun add_def theory = if def then theory - |> Sign.add_consts_i [(name, setT', NoSyn)] - |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name) - (Primitive_Defs.mk_defpair (setC, set)))] + |> Sign.add_consts_i [(name, setT', NoSyn)] (* FIXME authentic syntax *) + |> PureThy.add_defs false + [((Binding.map_name Thm.def_name name, Logic.mk_equals (setC, set)), [])] |-> (fn [th] => pair (SOME th)) else (NONE, theory); fun contract_def NONE th = th @@ -164,7 +164,7 @@ [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]), ((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}), [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])] - ||> Sign.parent_path; + ||> Sign.restore_naming thy1; val info = {rep_type = oldT, abs_type = newT, Rep_name = full Rep_name, Abs_name = full Abs_name, inhabited = inhabited, type_definition = type_definition, set_def = set_def, @@ -250,24 +250,20 @@ val _ = OuterKeyword.keyword "morphisms"; -val typedef_decl = - Scan.optional (P.$$$ "(" |-- - ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) - --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- - Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); - -fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = - typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs); - val _ = OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" OuterKeyword.thy_goal - (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef))); + (Scan.optional (P.$$$ "(" |-- + ((P.$$$ "open" >> K false) -- Scan.option P.binding || + P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- + (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- + Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)) + >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) => + Toplevel.print o Toplevel.theory_to_proof + (typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs)))); end; - val setup = Typedef_Interpretation.init; end; diff -r 01e968432467 -r 298f729f4fac src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/HOLCF/Tools/pcpodef.ML Thu Feb 18 23:43:14 2010 +0100 @@ -100,7 +100,7 @@ ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []), ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []), ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])]) - ||> Sign.parent_path; + ||> Sign.restore_naming thy2; val cpo_info : cpo_info = { below_def = below_def, adm = admissible', cont_Rep = cont_Rep, cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact }; @@ -139,7 +139,7 @@ ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []), ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []), ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])]) - ||> Sign.parent_path; + ||> Sign.restore_naming thy2; val pcpo_info = { Rep_strict = Rep_strict, Abs_strict = Abs_strict, Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff, diff -r 01e968432467 -r 298f729f4fac src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/HOLCF/Tools/repdef.ML Thu Feb 18 23:43:14 2010 +0100 @@ -139,7 +139,7 @@ |> PureThy.add_thms [((Binding.prefix_name "REP_" name, Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])] - ||> Sign.parent_path; + ||> Sign.restore_naming thy4; val rep_info = { emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm }; diff -r 01e968432467 -r 298f729f4fac src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/Pure/General/binding.ML Thu Feb 18 23:43:14 2010 +0100 @@ -22,6 +22,7 @@ val empty: binding val is_empty: binding -> bool val qualify: bool -> string -> binding -> binding + val qualified: bool -> string -> binding -> binding val qualified_name: string -> binding val qualified_name_of: binding -> string val prefix_of: binding -> (string * bool) list @@ -87,6 +88,10 @@ map_binding (fn (conceal, prefix, qualifier, name, pos) => (conceal, prefix, (qual, mandatory) :: qualifier, name, pos)); +fun qualified mandatory name' = map_binding (fn (conceal, prefix, qualifier, name, pos) => + let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)] + in (conceal, prefix, qualifier', name', pos) end); + fun qualified_name "" = empty | qualified_name s = let val (qualifier, name) = split_last (Long_Name.explode s) diff -r 01e968432467 -r 298f729f4fac src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/Pure/General/name_space.ML Thu Feb 18 23:43:14 2010 +0100 @@ -43,6 +43,7 @@ val root_path: naming -> naming val parent_path: naming -> naming val mandatory_path: string -> naming -> naming + val qualified_path: bool -> binding -> naming -> naming val transform_binding: naming -> binding -> binding val full_name: naming -> binding -> string val external_names: naming -> string -> string list @@ -261,6 +262,9 @@ val parent_path = map_path (perhaps (try (#1 o split_last))); fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]); +fun qualified_path mandatory binding = map_path (fn path => + path @ #2 (Binding.dest (Binding.qualified mandatory "" binding))); + (* full name *) diff -r 01e968432467 -r 298f729f4fac src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/Pure/Isar/expression.ML Thu Feb 18 23:43:14 2010 +0100 @@ -681,7 +681,7 @@ |> def_pred abinding parms defs' exts exts'; val (_, thy'') = thy' - |> Sign.mandatory_path (Binding.name_of abinding) + |> Sign.qualified_path true abinding |> PureThy.note_thmss "" [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])] ||> Sign.restore_naming thy'; @@ -695,7 +695,7 @@ |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred); val (_, thy'''') = thy''' - |> Sign.mandatory_path (Binding.name_of binding) + |> Sign.qualified_path true binding |> PureThy.note_thmss "" [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]), ((Binding.conceal (Binding.name axiomsN), []), diff -r 01e968432467 -r 298f729f4fac src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/Pure/Isar/isar_syn.ML Thu Feb 18 23:43:14 2010 +0100 @@ -390,7 +390,7 @@ val _ = OuterSyntax.command "context" "enter local theory context" K.thy_decl (P.name --| P.begin >> (fn name => - Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context name))); + Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name))); (* locales *) diff -r 01e968432467 -r 298f729f4fac src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/Pure/Isar/theory_target.ML Thu Feb 18 23:43:14 2010 +0100 @@ -7,12 +7,14 @@ signature THEORY_TARGET = sig - val peek: local_theory -> {target: string, is_locale: bool, - is_class: bool, instantiation: string list * (string * sort) list * sort, + val peek: local_theory -> + {target: string, + is_locale: bool, + is_class: bool, + instantiation: string list * (string * sort) list * sort, overloading: (string * (string * typ) * bool) list} val init: string option -> theory -> local_theory - val begin: string -> Proof.context -> local_theory - val context: xstring -> theory -> local_theory + val context_cmd: xstring -> theory -> local_theory val instantiation: string list * (string * sort) list * sort -> theory -> local_theory val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory val overloading: (string * (string * typ) * bool) list -> theory -> local_theory @@ -305,13 +307,13 @@ in ((lhs, (res_name, res)), lthy4) end; -(* init *) +(* init various targets *) local fun init_target _ NONE = global_target | init_target thy (SOME target) = - if Locale.defined thy (Locale.intern thy target) + if Locale.defined thy target then make_target target true (Class_Target.is_class thy target) ([], [], []) [] else error ("No such locale: " ^ quote target); @@ -349,17 +351,12 @@ in fun init target thy = init_lthy_ctxt (init_target thy target) thy; -fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt; -fun context "-" thy = init NONE thy - | context target thy = init (SOME (Locale.intern thy target)) thy; - - -(* other targets *) +fun context_cmd "-" thy = init NONE thy + | context_cmd target thy = init (SOME (Locale.intern thy target)) thy; fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []); -fun instantiation_cmd raw_arities thy = - instantiation (Class_Target.read_multi_arity thy raw_arities) thy; +fun instantiation_cmd arities thy = instantiation (Class_Target.read_multi_arity thy arities) thy; val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); val overloading_cmd = gen_overloading Syntax.read_term; diff -r 01e968432467 -r 298f729f4fac src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/Pure/Isar/toplevel.ML Thu Feb 18 23:43:14 2010 +0100 @@ -104,7 +104,7 @@ type generic_theory = Context.generic; (*theory or local_theory*) -val loc_init = Theory_Target.context; +val loc_init = Theory_Target.context_cmd; val loc_exit = Local_Theory.exit_global; fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy diff -r 01e968432467 -r 298f729f4fac src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/Pure/axclass.ML Thu Feb 18 23:43:14 2010 +0100 @@ -286,23 +286,25 @@ (* declaration and definition of instances of overloaded constants *) -fun inst_tyco_of thy (c, T) = case get_inst_tyco (Sign.consts_of thy) (c, T) - of SOME tyco => tyco - | NONE => error ("Illegal type for instantiation of class parameter: " - ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T)); +fun inst_tyco_of thy (c, T) = + (case get_inst_tyco (Sign.consts_of thy) (c, T) of + SOME tyco => tyco + | NONE => error ("Illegal type for instantiation of class parameter: " ^ + quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T))); fun declare_overloaded (c, T) thy = let - val class = case class_of_param thy c - of SOME class => class - | NONE => error ("Not a class parameter: " ^ quote c); + val class = + (case class_of_param thy c of + SOME class => class + | NONE => error ("Not a class parameter: " ^ quote c)); val tyco = inst_tyco_of thy (c, T); val name_inst = instance_name (tyco, class) ^ "_inst"; val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco; val T' = Type.strip_sorts T; in thy - |> Sign.mandatory_path name_inst + |> Sign.qualified_path true (Binding.name name_inst) |> Sign.declare_const ((Binding.name c', T'), NoSyn) |-> (fn const' as Const (c'', _) => Thm.add_def false true @@ -311,8 +313,8 @@ #-> (fn thm => add_inst_param (c, tyco) (c'', thm) #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), []) #> snd - #> Sign.restore_naming thy #> pair (Const (c, T)))) + ||> Sign.restore_naming thy end; fun define_overloaded b (c, t) thy = @@ -482,7 +484,7 @@ val class_triv = Thm.class_triv def_thy class; val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) = def_thy - |> Sign.mandatory_path (Binding.name_of bconst) + |> Sign.qualified_path true bconst |> PureThy.note_thmss "" [((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]), ((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]), @@ -497,7 +499,7 @@ val result_thy = facts_thy |> fold put_classrel (map (pair class) super ~~ classrel) - |> Sign.add_path (Binding.name_of bconst) + |> Sign.qualified_path false bconst |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd |> Sign.restore_naming facts_thy |> map_axclasses (fn (axclasses, parameters) => diff -r 01e968432467 -r 298f729f4fac src/Pure/display.ML --- a/src/Pure/display.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/Pure/display.ML Thu Feb 18 23:43:14 2010 +0100 @@ -125,7 +125,7 @@ fun pretty_full_theory verbose thy = let - val ctxt = ProofContext.init thy; + val ctxt = Syntax.init_pretty_global thy; fun prt_cls c = Syntax.pretty_sort ctxt [c]; fun prt_sort S = Syntax.pretty_sort ctxt S; diff -r 01e968432467 -r 298f729f4fac src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Feb 18 14:28:26 2010 -0800 +++ b/src/Pure/sign.ML Thu Feb 18 23:43:14 2010 +0100 @@ -127,6 +127,7 @@ val root_path: theory -> theory val parent_path: theory -> theory val mandatory_path: string -> theory -> theory + val qualified_path: bool -> binding -> theory -> theory val local_path: theory -> theory val restore_naming: theory -> theory -> theory val hide_class: bool -> string -> theory -> theory @@ -614,6 +615,7 @@ val root_path = map_naming Name_Space.root_path; val parent_path = map_naming Name_Space.parent_path; val mandatory_path = map_naming o Name_Space.mandatory_path; +val qualified_path = map_naming oo Name_Space.qualified_path; fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);