--- a/src/Pure/Isar/class.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/class.ML Sat Mar 07 22:16:50 2009 +0100
@@ -10,9 +10,9 @@
(*FIXME the split into class_target.ML, theory_target.ML and
class.ML is artificial*)
- val class: bstring -> class list -> Element.context_i list
+ val class: binding -> class list -> Element.context_i list
-> theory -> string * local_theory
- val class_cmd: bstring -> xstring list -> Element.context list
+ val class_cmd: binding -> xstring list -> Element.context list
-> theory -> string * local_theory
val prove_subclass: tactic -> class -> local_theory -> local_theory
val subclass: class -> local_theory -> Proof.state
@@ -73,7 +73,7 @@
val morph = base_morph $> eq_morph;
(* assm_intro *)
- fun prove_assm_intro thm =
+ fun prove_assm_intro thm =
let
val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
@@ -169,7 +169,7 @@
val _ = case filter_out (is_class thy) sups
of [] => ()
| no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
- val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
+ val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
val supparam_names = map fst supparams;
val _ = if has_duplicates (op =) supparam_names
then error ("Duplicate parameter(s) in superclasses: "
@@ -200,7 +200,7 @@
| check_element e = [()];
val _ = map check_element syntax_elems;
fun fork_syn (Element.Fixes xs) =
- fold_map (fn (c, ty, syn) => cons (Binding.name_of c, syn) #> pair (c, ty, NoSyn)) xs
+ fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
#>> Element.Fixes
| fork_syn x = pair x;
val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
@@ -217,7 +217,7 @@
(* class establishment *)
-fun add_consts bname class base_sort sups supparams global_syntax thy =
+fun add_consts class base_sort sups supparams global_syntax thy =
let
(*FIXME simplify*)
val supconsts = supparams
@@ -227,17 +227,16 @@
val raw_params = (snd o chop (length supparams)) all_params;
fun add_const (b, SOME raw_ty, _) thy =
let
- val v = Binding.name_of b;
- val c = Sign.full_bname thy v;
+ val c = Sign.full_name thy b;
val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
val ty0 = Type.strip_sorts ty;
val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
- val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v;
+ val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
in
thy
- |> Sign.declare_const [] ((Binding.name v, ty0), syn)
+ |> Sign.declare_const [] ((b, ty0), syn)
|> snd
- |> pair ((v, ty), (c, ty'))
+ |> pair ((Binding.name_of b, ty), (c, ty'))
end;
in
thy
@@ -261,7 +260,7 @@
| [thm] => SOME thm;
in
thy
- |> add_consts bname class base_sort sups supparams global_syntax
+ |> add_consts class base_sort sups supparams global_syntax
|-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
(map (fst o snd) params)
[(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
@@ -273,12 +272,12 @@
fun gen_class prep_spec bname raw_supclasses raw_elems thy =
let
- val class = Sign.full_bname thy bname;
+ val class = Sign.full_name thy bname;
val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
prep_spec thy raw_supclasses raw_elems;
in
thy
- |> Expression.add_locale bname "" supexpr elems
+ |> Expression.add_locale bname Binding.empty supexpr elems
|> snd |> LocalTheory.exit_global
|> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
|-> (fn (param_map, params, assm_axiom) =>
--- a/src/Pure/Isar/class_target.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Sat Mar 07 22:16:50 2009 +0100
@@ -24,9 +24,9 @@
val begin: class list -> sort -> Proof.context -> Proof.context
val init: class -> theory -> Proof.context
val declare: class -> Properties.T
- -> (string * mixfix) * term -> theory -> theory
+ -> (binding * mixfix) * term -> theory -> theory
val abbrev: class -> Syntax.mode -> Properties.T
- -> (string * mixfix) * term -> theory -> theory
+ -> (binding * mixfix) * term -> theory -> theory
val class_prefix: string -> string
val refresh_syntax: class -> Proof.context -> Proof.context
val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
@@ -52,12 +52,12 @@
val default_intro_tac: Proof.context -> thm list -> tactic
(*old axclass layer*)
- val axclass_cmd: bstring * xstring list
+ val axclass_cmd: binding * xstring list
-> (Attrib.binding * string list) list
-> theory -> class * theory
val classrel_cmd: xstring * xstring -> theory -> Proof.state
val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
- val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
+ val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
end;
structure Class_Target : CLASS_TARGET =
@@ -363,8 +363,8 @@
fun declare class pos ((c, mx), dict) thy =
let
val morph = morphism thy class;
- val b = Morphism.binding morph (Binding.name c);
- val b_def = Morphism.binding morph (Binding.name (c ^ "_dict"));
+ val b = Morphism.binding morph c;
+ val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b);
val c' = Sign.full_name thy b;
val dict' = Morphism.term morph dict;
val ty' = Term.fastype_of dict';
@@ -386,7 +386,7 @@
let
val morph = morphism thy class;
val unchecks = these_unchecks thy [class];
- val b = Morphism.binding morph (Binding.name c);
+ val b = Morphism.binding morph c;
val c' = Sign.full_name thy b;
val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
val ty' = Term.fastype_of rhs';
--- a/src/Pure/Isar/constdefs.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML Sat Mar 07 22:16:50 2009 +0100
@@ -44,13 +44,13 @@
else ());
val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
- val name = Thm.def_name_optional c (Binding.name_of raw_name);
+ val name = Binding.map_name (Thm.def_name_optional c) raw_name;
val atts = map (prep_att thy) raw_atts;
val thy' =
thy
- |> Sign.add_consts_i [(c, T, mx)]
- |> PureThy.add_defs false [((Binding.name name, def), atts)]
+ |> Sign.add_consts_i [(Binding.name c, T, mx)]
+ |> PureThy.add_defs false [((name, def), atts)]
|-> (fn [thm] => Code.add_default_eqn thm);
in ((c, T), thy') end;
--- a/src/Pure/Isar/expression.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/expression.ML Sat Mar 07 22:16:50 2009 +0100
@@ -29,9 +29,9 @@
val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
- val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
+ val add_locale: binding -> binding -> expression_i -> Element.context_i list ->
theory -> string * local_theory
- val add_locale_cmd: bstring -> bstring -> expression -> Element.context list ->
+ val add_locale_cmd: binding -> binding -> expression -> Element.context list ->
theory -> string * local_theory
(* Interpretation *)
@@ -41,15 +41,12 @@
(term list list * (string * morphism) list * morphism) * Proof.context
val sublocale: string -> expression_i -> theory -> Proof.state
val sublocale_cmd: string -> expression -> theory -> Proof.state
- val interpretation: expression_i -> (Attrib.binding * term) list ->
- theory -> Proof.state
- val interpretation_cmd: expression -> (Attrib.binding * string) list ->
- theory -> Proof.state
+ val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
+ val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
val interpret: expression_i -> bool -> Proof.state -> Proof.state
val interpret_cmd: expression -> bool -> Proof.state -> Proof.state
end;
-
structure Expression : EXPRESSION =
struct
@@ -90,11 +87,10 @@
fun match_bind (n, b) = (n = Binding.name_of b);
fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
- (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *)
- Binding.name_of b1 = Binding.name_of b2 andalso
+ Binding.eq_name (b1, b2) andalso
(mx1 = mx2 orelse
error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
-
+
fun params_loc loc =
(Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
fun params_inst (expr as (loc, (prfx, Positional insts))) =
@@ -132,8 +128,10 @@
val implicit' = map (#1 #> Binding.name_of) implicit;
val fixed' = map (#1 #> Binding.name_of) fixed;
val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
- val implicit'' = if strict then []
- else let val _ = reject_dups
+ val implicit'' =
+ if strict then []
+ else
+ let val _ = reject_dups
"Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed')
in map (fn (b, mx) => (b, NONE, mx)) implicit end;
@@ -176,7 +174,7 @@
val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
val res = Syntax.check_terms ctxt arg;
val ctxt' = ctxt |> fold Variable.auto_fixes res;
-
+
(* instantiation *)
val (type_parms'', res') = chop (length type_parms) res;
val insts'' = (parm_names ~~ res') |> map_filter
@@ -330,7 +328,7 @@
let
val elem' = finish_primitive parms (closeup ctxt parms do_close) elem;
in elem' end
-
+
fun finish ctxt parms do_close insts elems =
let
val deps = map (finish_inst ctxt parms do_close) insts;
@@ -366,7 +364,7 @@
val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt;
in (i+1, insts', ctxt'') end;
-
+
fun prep_elem insts raw_elem (elems, ctxt) =
let
val ctxt' = declare_elem prep_vars_elem raw_elem ctxt;
@@ -390,7 +388,7 @@
(* Retrieve parameter types *)
val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.name_of o #1) fixes)
| _ => fn ps => ps) (Fixes fors :: elems') [];
- val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6;
+ val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6;
val parms = xs ~~ Ts; (* params from expression and elements *)
val Fixes fors' = finish_primitive parms I (Fixes fors);
@@ -490,7 +488,7 @@
val exp_typ = Logic.type_map exp_term;
val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
in ((propss, deps, export'), goal_ctxt) end;
-
+
in
fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x;
@@ -617,7 +615,7 @@
fun def_pred bname parms defs ts norm_ts thy =
let
- val name = Sign.full_bname thy bname;
+ val name = Sign.full_name thy bname;
val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
val env = Term.add_free_names body [];
@@ -635,9 +633,9 @@
val ([pred_def], defs_thy) =
thy
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
- |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
+ |> Sign.declare_const [] ((bname, predT), NoSyn) |> snd
|> PureThy.add_defs false
- [((Binding.name (Thm.def_name bname), Logic.mk_equals (head, body)), [Thm.kind_internal])];
+ [((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
val cert = Thm.cterm_of defs_thy;
@@ -660,7 +658,7 @@
in
-(* CB: main predicate definition function *)
+(* main predicate definition function *)
fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy =
let
@@ -670,13 +668,13 @@
if null exts then (NONE, NONE, [], thy)
else
let
- val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
+ val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname
val ((statement, intro, axioms), thy') =
thy
|> def_pred aname parms defs' exts exts';
val (_, thy'') =
thy'
- |> Sign.add_path aname
+ |> Sign.add_path (Binding.name_of aname)
|> Sign.no_base_names
|> PureThy.note_thmss Thm.internalK
[((Binding.name introN, []), [([intro], [Locale.unfold_attrib])])]
@@ -691,7 +689,7 @@
|> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
val (_, thy'''') =
thy'''
- |> Sign.add_path pname
+ |> Sign.add_path (Binding.name_of pname)
|> Sign.no_base_names
|> PureThy.note_thmss Thm.internalK
[((Binding.name introN, []), [([intro], [Locale.intro_attrib])]),
@@ -722,7 +720,7 @@
fun gen_add_locale prep_decl
bname raw_predicate_bname raw_import raw_body thy =
let
- val name = Sign.full_bname thy bname;
+ val name = Sign.full_name thy bname;
val _ = Locale.defined thy name andalso
error ("Duplicate definition of locale " ^ quote name);
@@ -730,14 +728,16 @@
prep_decl raw_import I raw_body (ProofContext.init thy);
val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
- val predicate_bname = if raw_predicate_bname = "" then bname
+ val predicate_bname =
+ if Binding.is_empty raw_predicate_bname then bname
else raw_predicate_bname;
val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
define_preds predicate_bname parms text thy;
val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
- val _ = if null extraTs then ()
- else warning ("Additional type variable(s) in locale specification " ^ quote bname);
+ val _ =
+ if null extraTs then ()
+ else warning ("Additional type variable(s) in locale specification " ^ quote (Binding.str_of bname));
val a_satisfy = Element.satisfy_morphism a_axioms;
val b_satisfy = Element.satisfy_morphism b_axioms;
@@ -748,7 +748,7 @@
val notes =
if is_some asm
- then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
+ then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []),
[([Assumption.assume (cterm_of thy' (the asm))],
[(Attrib.internal o K) Locale.witness_attrib])])])]
else [];
@@ -766,7 +766,7 @@
val loc_ctxt = thy'
|> Locale.register_locale bname (extraTs, params)
- (asm, rev defs) (a_intro, b_intro) axioms ([], [])
+ (asm, rev defs) (a_intro, b_intro) axioms ([], [])
(map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev)
|> TheoryTarget.init (SOME name)
|> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
@@ -793,7 +793,7 @@
val target_ctxt = Locale.init target thy;
val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
-
+
fun after_qed witss = ProofContext.theory (
fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
(name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
@@ -879,7 +879,7 @@
val ctxt = Proof.context_of state;
val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
-
+
fun store_reg (name, morph) thms =
let
val morph' = morph $> Element.satisfy_morphism thms $> export;
--- a/src/Pure/Isar/isar_syn.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Mar 07 22:16:50 2009 +0100
@@ -86,7 +86,7 @@
val _ =
OuterSyntax.command "classes" "declare type classes" K.thy_decl
- (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
+ (Scan.repeat1 (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
val _ =
@@ -100,7 +100,7 @@
val _ =
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
- (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
+ (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
P.!!! (P.list1 P.xname)) []
-- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
>> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y)));
@@ -110,19 +110,19 @@
val _ =
OuterSyntax.command "typedecl" "type declaration" K.thy_decl
- (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
+ (P.type_args -- P.binding -- P.opt_infix >> (fn ((args, a), mx) =>
Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd)));
val _ =
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
(Scan.repeat1
- (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
+ (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
>> (Toplevel.theory o Sign.add_tyabbrs o
map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
val _ =
OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
- K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Sign.add_nonterminals));
+ K.thy_decl (Scan.repeat1 P.binding >> (Toplevel.theory o Sign.add_nonterminals));
val _ =
OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
@@ -133,11 +133,11 @@
val _ =
OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
- (P.const >> (Toplevel.theory o ObjectLogic.add_judgment));
+ (P.const_binding >> (Toplevel.theory o ObjectLogic.add_judgment_cmd));
val _ =
OuterSyntax.command "consts" "declare constants" K.thy_decl
- (Scan.repeat1 P.const >> (Toplevel.theory o Sign.add_consts));
+ (Scan.repeat1 P.const_binding >> (Toplevel.theory o Sign.add_consts));
val opt_overloaded = P.opt_keyword "overloaded";
@@ -392,10 +392,10 @@
val _ =
OuterSyntax.command "locale" "define named proof context" K.thy_decl
- (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
+ (P.binding -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
- (Expression.add_locale_cmd name "" expr elems #> snd)));
+ (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
val _ =
OuterSyntax.command "sublocale"
@@ -430,7 +430,7 @@
val _ =
OuterSyntax.command "class" "define type class" K.thy_decl
- (P.name -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin
+ (P.binding -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin
>> (fn ((name, (supclasses, elems)), begin) =>
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
(Class.class_cmd name supclasses elems #> snd)));
--- a/src/Pure/Isar/locale.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/locale.ML Sat Mar 07 22:16:50 2009 +0100
@@ -30,7 +30,7 @@
signature LOCALE =
sig
(* Locale specification *)
- val register_locale: bstring ->
+ val register_locale: binding ->
(string * sort) list * (binding * typ option * mixfix) list ->
term option * term list ->
thm option * thm option -> thm list ->
@@ -78,7 +78,7 @@
(* Diagnostic *)
val print_locales: theory -> unit
- val print_locale: theory -> bool -> bstring -> unit
+ val print_locale: theory -> bool -> xstring -> unit
end;
@@ -173,8 +173,8 @@
of SOME (Loc loc) => loc
| NONE => error ("Unknown locale " ^ quote name);
-fun register_locale bname parameters spec intros axioms decls notes dependencies thy =
- thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
+fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
+ thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (binding,
mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
fun change_locale name =
--- a/src/Pure/Isar/object_logic.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/object_logic.ML Sat Mar 07 22:16:50 2009 +0100
@@ -8,9 +8,9 @@
sig
val get_base_sort: theory -> sort option
val add_base_sort: sort -> theory -> theory
- val typedecl: bstring * string list * mixfix -> theory -> typ * theory
- val add_judgment: bstring * string * mixfix -> theory -> theory
- val add_judgment_i: bstring * typ * mixfix -> theory -> theory
+ val typedecl: binding * string list * mixfix -> theory -> typ * theory
+ val add_judgment: binding * typ * mixfix -> theory -> theory
+ val add_judgment_cmd: binding * string * mixfix -> theory -> theory
val judgment_name: theory -> string
val is_judgment: theory -> term -> bool
val drop_judgment: theory -> term -> term
@@ -85,17 +85,18 @@
(* typedecl *)
-fun typedecl (raw_name, vs, mx) thy =
+fun typedecl (a, vs, mx) thy =
let
val base_sort = get_base_sort thy;
- val name = Sign.full_bname thy (Syntax.type_name raw_name mx);
+ val b = Binding.map_name (Syntax.type_name mx) a;
val _ = has_duplicates (op =) vs andalso
- error ("Duplicate parameters in type declaration: " ^ quote name);
+ error ("Duplicate parameters in type declaration: " ^ quote (Binding.str_of b));
+ val name = Sign.full_name thy b;
val n = length vs;
val T = Type (name, map (fn v => TFree (v, [])) vs);
in
thy
- |> Sign.add_types [(raw_name, n, mx)]
+ |> Sign.add_types [(a, n, mx)]
|> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
|> pair T
end;
@@ -105,10 +106,10 @@
local
-fun gen_add_judgment add_consts (bname, T, mx) thy =
- let val c = Sign.full_bname thy (Syntax.const_name bname mx) in
+fun gen_add_judgment add_consts (b, T, mx) thy =
+ let val c = Sign.full_name thy (Binding.map_name (Syntax.const_name mx) b) in
thy
- |> add_consts [(bname, T, mx)]
+ |> add_consts [(b, T, mx)]
|> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')
|> map_data (fn (base_sort, judgment, atomize_rulify) =>
if is_some judgment then error "Attempt to redeclare object-logic judgment"
@@ -117,8 +118,8 @@
in
-val add_judgment = gen_add_judgment Sign.add_consts;
-val add_judgment_i = gen_add_judgment Sign.add_consts_i;
+val add_judgment = gen_add_judgment Sign.add_consts_i;
+val add_judgment_cmd = gen_add_judgment Sign.add_consts;
end;
--- a/src/Pure/Isar/specification.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/specification.ML Sat Mar 07 22:16:50 2009 +0100
@@ -181,7 +181,7 @@
Position.str_of (Binding.pos_of b));
in (b, mx) end);
val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
- (var, ((Binding.map_name (suffix "_raw") name, []), rhs));
+ (var, ((Binding.suffix_name "_raw" name, []), rhs));
val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
--- a/src/Pure/Isar/theory_target.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Sat Mar 07 22:16:50 2009 +0100
@@ -189,7 +189,7 @@
val similar_body = Type.similar_types (rhs, rhs');
(* FIXME workaround based on educated guess *)
val prefix' = Binding.prefix_of b';
- val class_global = Binding.name_of b = Binding.name_of b'
+ val class_global = Binding.eq_name (b, b')
andalso not (null prefix')
andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
in
@@ -210,7 +210,7 @@
fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
let
- val c = Binding.name_of b;
+ val c = Binding.name_of b; (* FIXME Binding.qualified_name_of *)
val tags = LocalTheory.group_position_of lthy;
val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
val U = map #2 xs ---> T;
@@ -233,7 +233,7 @@
in
lthy'
|> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((b, mx2), t))
- |> is_class ? class_target ta (Class_Target.declare target tags ((c, mx1), t))
+ |> is_class ? class_target ta (Class_Target.declare target tags ((b, mx1), t))
|> LocalDefs.add_def ((b, NoSyn), t)
end;
@@ -242,7 +242,6 @@
fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
let
- val c = Binding.name_of b;
val tags = LocalTheory.group_position_of lthy;
val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
val target_ctxt = LocalTheory.target_of lthy;
@@ -260,7 +259,7 @@
#-> (fn (lhs, _) =>
let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
term_syntax ta (locale_const ta prmode tags ((b, mx2), lhs')) #>
- is_class ? class_target ta (Class_Target.abbrev target prmode tags ((c, mx1), t'))
+ is_class ? class_target ta (Class_Target.abbrev target prmode tags ((b, mx1), t'))
end)
else
LocalTheory.theory
@@ -279,8 +278,8 @@
val thy = ProofContext.theory_of lthy;
val thy_ctxt = ProofContext.init thy;
- val c = Binding.name_of b;
- val name' = Binding.map_name (Thm.def_name_optional c) name;
+ val c = Binding.name_of b; (* FIXME Binding.qualified_name_of (!?) *)
+ val name' = Binding.map_name (Thm.def_name_optional (Binding.name_of b)) name;
val (rhs', rhs_conv) =
LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
--- a/src/Pure/Proof/extraction.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Sat Mar 07 22:16:50 2009 +0100
@@ -37,12 +37,12 @@
thy
|> Theory.copy
|> Sign.root_path
- |> Sign.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
+ |> Sign.add_types [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
|> Sign.add_consts
- [("typeof", "'b::{} => Type", NoSyn),
- ("Type", "'a::{} itself => Type", NoSyn),
- ("Null", "Null", NoSyn),
- ("realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
+ [(Binding.name "typeof", "'b::{} => Type", NoSyn),
+ (Binding.name "Type", "'a::{} itself => Type", NoSyn),
+ (Binding.name "Null", "Null", NoSyn),
+ (Binding.name "realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
val nullT = Type ("Null", []);
val nullt = Const ("Null", nullT);
@@ -732,7 +732,7 @@
val fu = Type.freeze u;
val (def_thms, thy') = if t = nullt then ([], thy) else
thy
- |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
+ |> Sign.add_consts_i [(Binding.name (extr_name s vs), fastype_of ft, NoSyn)]
|> PureThy.add_defs false [((Binding.name (extr_name s vs ^ "_def"),
Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
in
--- a/src/Pure/Proof/proof_syntax.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Sat Mar 07 22:16:50 2009 +0100
@@ -37,7 +37,7 @@
fun add_proof_atom_consts names thy =
thy
|> Sign.absolute_path
- |> Sign.add_consts_i (map (fn name => (name, proofT, NoSyn)) names);
+ |> Sign.add_consts_i (map (fn name => (Binding.name name, proofT, NoSyn)) names);
(** constants for application and abstraction **)
@@ -46,16 +46,16 @@
|> Theory.copy
|> Sign.root_path
|> Sign.add_defsort_i []
- |> Sign.add_types [("proof", 0, NoSyn)]
+ |> Sign.add_types [(Binding.name "proof", 0, NoSyn)]
|> Sign.add_consts_i
- [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
- ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
- ("Abst", (aT --> proofT) --> proofT, NoSyn),
- ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
- ("Hyp", propT --> proofT, NoSyn),
- ("Oracle", propT --> proofT, NoSyn),
- ("MinProof", proofT, Delimfix "?")]
- |> Sign.add_nonterminals ["param", "params"]
+ [(Binding.name "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
+ (Binding.name "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
+ (Binding.name "Abst", (aT --> proofT) --> proofT, NoSyn),
+ (Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
+ (Binding.name "Hyp", propT --> proofT, NoSyn),
+ (Binding.name "Oracle", propT --> proofT, NoSyn),
+ (Binding.name "MinProof", proofT, Delimfix "?")]
+ |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
|> Sign.add_syntax_i
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
--- a/src/Pure/axclass.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/axclass.ML Sat Mar 07 22:16:50 2009 +0100
@@ -7,7 +7,7 @@
signature AX_CLASS =
sig
- val define_class: bstring * class list -> string list ->
+ val define_class: binding * class list -> string list ->
(Thm.binding * term list) list -> theory -> class * theory
val add_classrel: thm -> theory -> theory
val add_arity: thm -> theory -> theory
@@ -19,8 +19,8 @@
val class_of_param: theory -> string -> class option
val cert_classrel: theory -> class * class -> class * class
val read_classrel: theory -> xstring * xstring -> class * class
- val axiomatize_class: bstring * class list -> theory -> theory
- val axiomatize_class_cmd: bstring * xstring list -> theory -> theory
+ val axiomatize_class: binding * class list -> theory -> theory
+ val axiomatize_class_cmd: binding * xstring list -> theory -> theory
val axiomatize_classrel: (class * class) list -> theory -> theory
val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
val axiomatize_arity: arity -> theory -> theory
@@ -325,8 +325,7 @@
let
val ctxt = ProofContext.init thy;
val (c1, c2) = cert_classrel thy raw_rel;
- val th = Goal.prove ctxt [] []
- (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg =>
+ val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
quote (Syntax.string_of_classrel ctxt [c1, c2]));
in
@@ -374,14 +373,15 @@
|> Sign.sticky_prefix name_inst
|> Sign.no_base_names
|> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
- |-> (fn const' as Const (c'', _) => Thm.add_def false true
- (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
- #>> Thm.varifyT
- #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
- #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
- #> snd
- #> Sign.restore_naming thy
- #> pair (Const (c, T))))
+ |-> (fn const' as Const (c'', _) =>
+ Thm.add_def false true
+ (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
+ #>> Thm.varifyT
+ #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
+ #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
+ #> snd
+ #> Sign.restore_naming thy
+ #> pair (Const (c, T))))
end;
fun define_overloaded name (c, t) thy =
@@ -390,8 +390,7 @@
val SOME tyco = inst_tyco_of thy (c, T);
val (c', eq) = get_inst_param thy (c, tyco);
val prop = Logic.mk_equals (Const (c', T), t);
- val name' = Thm.def_name_optional
- (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name;
+ val name' = Thm.def_name_optional (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name;
in
thy
|> Thm.add_def false false (Binding.name name', prop)
@@ -424,8 +423,8 @@
(* class *)
- val bconst = Logic.const_of_class bclass;
- val class = Sign.full_bname thy bclass;
+ val bconst = Binding.map_name Logic.const_of_class bclass;
+ val class = Sign.full_name thy bclass;
val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super);
fun check_constraint (a, S) =
@@ -472,7 +471,7 @@
val ([def], def_thy) =
thy
|> Sign.primitive_class (bclass, super)
- |> PureThy.add_defs false [((Binding.name (Thm.def_name bconst), class_eq), [])];
+ |> PureThy.add_defs false [((Binding.map_name Thm.def_name bconst, class_eq), [])];
val (raw_intro, (raw_classrel, raw_axioms)) =
split_defined (length conjs) def ||> chop (length super);
@@ -482,7 +481,7 @@
val class_triv = Thm.class_triv def_thy class;
val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
def_thy
- |> Sign.add_path bconst
+ |> Sign.add_path (Binding.name_of bconst)
|> Sign.no_base_names
|> PureThy.note_thmss ""
[((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
@@ -498,7 +497,7 @@
val result_thy =
facts_thy
|> fold put_classrel (map (pair class) super ~~ classrel)
- |> Sign.add_path bconst
+ |> Sign.add_path (Binding.name_of bconst)
|> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
|> Sign.restore_naming facts_thy
|> map_axclasses (fn (axclasses, parameters) =>
@@ -537,7 +536,7 @@
fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
let
- val class = Sign.full_bname thy bclass;
+ val class = Sign.full_name thy bclass;
val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy;
in
thy
--- a/src/Pure/pure_thy.ML Sat Mar 07 22:12:07 2009 +0100
+++ b/src/Pure/pure_thy.ML Sat Mar 07 22:16:50 2009 +0100
@@ -290,11 +290,11 @@
val _ = Context.>> (Context.map_theory
(OldApplSyntax.init #>
Sign.add_types
- [("fun", 2, NoSyn),
- ("prop", 0, NoSyn),
- ("itself", 1, NoSyn),
- ("dummy", 0, NoSyn)]
- #> Sign.add_nonterminals Syntax.basic_nonterms
+ [(Binding.name "fun", 2, NoSyn),
+ (Binding.name "prop", 0, NoSyn),
+ (Binding.name "itself", 1, NoSyn),
+ (Binding.name "dummy", 0, NoSyn)]
+ #> Sign.add_nonterminals (map Binding.name Syntax.basic_nonterms)
#> Sign.add_syntax_i
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)),
("_abs", typ "'a", NoSyn),
@@ -360,12 +360,12 @@
#> Sign.add_modesyntax_i ("HTML", false)
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
#> Sign.add_consts_i
- [("==", typ "'a => 'a => prop", InfixrName ("==", 2)),
- ("==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
- ("all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
- ("prop", typ "prop => prop", NoSyn),
- ("TYPE", typ "'a itself", NoSyn),
- (Term.dummy_patternN, typ "'a", Delimfix "'_")]
+ [(Binding.name "==", typ "'a => 'a => prop", InfixrName ("==", 2)),
+ (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
+ (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
+ (Binding.name "prop", typ "prop => prop", NoSyn),
+ (Binding.name "TYPE", typ "'a itself", NoSyn),
+ (Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")]
#> Theory.add_deps "==" ("==", typ "'a => 'a => prop") []
#> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") []
#> Theory.add_deps "all" ("all", typ "('a => prop) => prop") []
@@ -375,9 +375,9 @@
#> Sign.add_trfunsT Syntax.pure_trfunsT
#> Sign.local_path
#> Sign.add_consts_i
- [("term", typ "'a => prop", NoSyn),
- ("sort_constraint", typ "'a itself => prop", NoSyn),
- ("conjunction", typ "prop => prop => prop", NoSyn)]
+ [(Binding.name "term", typ "'a => prop", NoSyn),
+ (Binding.name "sort_constraint", typ "'a itself => prop", NoSyn),
+ (Binding.name "conjunction", typ "prop => prop => prop", NoSyn)]
#> (add_defs false o map Thm.no_attributes)
[(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
(Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),