--- 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;
--- 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,
--- 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 };
--- 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)
--- 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 *)
--- 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), []),
--- 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 *)
--- 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;
--- 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
--- 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) =>
--- 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;
--- 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);