--- a/src/HOL/Import/proof_kernel.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Import/proof_kernel.ML Sun Mar 08 00:16:34 2009 +0100
@@ -1926,7 +1926,8 @@
val csyn = mk_syn thy constname
val thy1 = case HOL4DefThy.get thy of
Replaying _ => thy
- | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
+ | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)];
+ Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy)
val eq = mk_defeq constname rhs' thy1
val (thms, thy2) = PureThy.add_defs false [((Binding.name thmname,eq),[])] thy1
val _ = ImportRecorder.add_defs thmname eq
@@ -2017,7 +2018,7 @@
val thy' = add_dump str thy
val _ = ImportRecorder.add_consts consts
in
- Sign.add_consts_i consts thy'
+ Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy'
end
val thy1 = List.foldr (fn(name,thy)=>
@@ -2093,7 +2094,9 @@
val tnames = map fst tfrees
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
- val ((_, typedef_info), thy') = TypedefPackage.add_typedef false (SOME thmname) typ c NONE (rtac th2 1) thy
+ val ((_, typedef_info), thy') =
+ TypedefPackage.add_typedef false (SOME (Binding.name thmname))
+ (Binding.name tycname, tnames, tsyn) c NONE (rtac th2 1) thy
val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
@@ -2179,7 +2182,9 @@
val tnames = sort string_ord (map fst tfrees)
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
- val ((_, typedef_info), thy') = TypedefPackage.add_typedef false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
+ val ((_, typedef_info), thy') =
+ TypedefPackage.add_typedef false NONE (Binding.name tycname,tnames,tsyn) c
+ (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
val fulltyname = Sign.intern_type thy' tycname
val aty = Type (fulltyname, map mk_vartype tnames)
--- a/src/HOL/Import/replay.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Import/replay.ML Sun Mar 08 00:16:34 2009 +0100
@@ -334,7 +334,7 @@
add_hol4_mapping thyname thmname isaname thy
| delta (Hol_pending (thyname, thmname, th)) thy =
add_hol4_pending thyname thmname ([], th_of thy th) thy
- | delta (Consts cs) thy = Sign.add_consts_i cs thy
+ | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy
| delta (Hol_const_mapping (thyname, constname, fullcname)) thy =
add_hol4_const_mapping thyname constname true fullcname thy
| delta (Hol_move (fullname, moved_thmname)) thy =
@@ -343,8 +343,9 @@
snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
| delta (Hol_theorem (thyname, thmname, th)) thy =
add_hol4_theorem thyname thmname ([], th_of thy th) thy
- | delta (Typedef (thmname, typ, c, repabs, th)) thy =
- snd (TypedefPackage.add_typedef false thmname typ c repabs (rtac (th_of thy th) 1) thy)
+ | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy =
+ snd (TypedefPackage.add_typedef false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
+ (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
| delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =
add_hol4_type_mapping thyname tycname true fulltyname thy
| delta (Indexed_theorem (i, th)) thy =
--- a/src/HOL/Nominal/nominal_atoms.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Sun Mar 08 00:16:34 2009 +0100
@@ -100,7 +100,7 @@
val (_,thy1) =
fold_map (fn ak => fn thy =>
- let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)])
+ let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
val inject_flat = Library.flat inject
val ak_type = Type (Sign.intern_type thy1 ak,[])
@@ -187,7 +187,7 @@
cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
in
- thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)]
+ thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)]
|> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])]
|> snd
|> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
@@ -217,7 +217,7 @@
(Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
in
- thy |> Sign.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)]
+ thy |> Sign.add_consts_i [(Binding.name prm_name, mk_permT T --> T --> T, NoSyn)]
|> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
end) ak_names_types thy3;
@@ -300,7 +300,7 @@
(HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
in
- AxClass.define_class (cl_name, ["HOL.type"]) []
+ AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
[((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
((Binding.name (cl_name ^ "2"), []), [axiom2]),
((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
@@ -349,7 +349,8 @@
val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
in
- AxClass.define_class (cl_name, [pt_name]) [] [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
+ AxClass.define_class (Binding.name cl_name, [pt_name]) []
+ [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
end) ak_names_types thy8;
(* proves that every fs_<ak>-type together with <ak>-type *)
@@ -398,7 +399,7 @@
(HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x),
cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
in
- AxClass.define_class (cl_name, ["HOL.type"]) []
+ AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
[((Binding.name (cl_name ^ "1"), []), [ax1])] thy'
end) ak_names_types thy) ak_names_types thy12;
--- a/src/HOL/Nominal/nominal_package.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Sun Mar 08 00:16:34 2009 +0100
@@ -197,7 +197,7 @@
val tmp_thy = thy |>
Theory.copy |>
Sign.add_types (map (fn (tvs, tname, mx, _) =>
- (tname, length tvs, mx)) dts);
+ (Binding.name tname, length tvs, mx)) dts);
val atoms = atoms_of thy;
@@ -235,8 +235,8 @@
Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
| replace_types T = T;
- val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn,
- map (fn (cname, cargs, mx) => (cname ^ "_Rep",
+ val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,
+ map (fn (cname, cargs, mx) => (Binding.name (cname ^ "_Rep"),
map replace_types cargs, NoSyn)) constrs)) dts';
val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
@@ -615,7 +615,8 @@
val (typedefs, thy6) =
thy4
|> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
- TypedefPackage.add_typedef false (SOME name') (name, map fst tvs, mx)
+ TypedefPackage.add_typedef false (SOME (Binding.name name'))
+ (Binding.name name, map fst tvs, mx)
(Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
Const (cname, U --> HOLogic.boolT)) NONE
(rtac exI 1 THEN rtac CollectI 1 THEN
@@ -800,7 +801,7 @@
(Const (rep_name, T --> T') $ lhs, rhs));
val def_name = (NameSpace.base_name cname) ^ "_def";
val ([def_thm], thy') = thy |>
- Sign.add_consts_i [(cname', constrT, mx)] |>
+ Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
(PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
in (thy', defs @ [def_thm], eqns @ [eqn]) end;
@@ -2012,7 +2013,7 @@
val (reccomb_defs, thy12) =
thy11
|> Sign.add_consts_i (map (fn ((name, T), T') =>
- (NameSpace.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
+ (Binding.name (NameSpace.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
(Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
--- a/src/HOL/Statespace/state_space.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML Sun Mar 08 00:16:34 2009 +0100
@@ -154,13 +154,13 @@
fun add_locale name expr elems thy =
thy
- |> Expression.add_locale name name expr elems
+ |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
|> snd
|> LocalTheory.exit;
fun add_locale_cmd name expr elems thy =
thy
- |> Expression.add_locale_cmd name "" expr elems
+ |> Expression.add_locale_cmd (Binding.name name) Binding.empty expr elems
|> snd
|> LocalTheory.exit;
--- a/src/HOL/Tools/datatype_abs_proofs.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Sun Mar 08 00:16:34 2009 +0100
@@ -235,7 +235,7 @@
val (reccomb_defs, thy2) =
thy1
|> Sign.add_consts_i (map (fn ((name, T), T') =>
- (NameSpace.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
+ (Binding.name (NameSpace.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
(Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
--- a/src/HOL/Tools/datatype_package.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML Sun Mar 08 00:16:34 2009 +0100
@@ -36,8 +36,8 @@
simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
-> theory -> Proof.state;
val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
- val add_datatype : bool -> bool -> string list -> (string list * bstring * mixfix *
- (bstring * typ list * mixfix) list) list -> theory ->
+ val add_datatype : bool -> bool -> string list -> (string list * binding * mixfix *
+ (binding * typ list * mixfix) list) list -> theory ->
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -46,8 +46,8 @@
split_thms : (thm * thm) list,
induction : thm,
simps : thm list} * theory
- val add_datatype_cmd : bool -> string list -> (string list * bstring * mixfix *
- (bstring * string list * mixfix) list) list -> theory ->
+ val add_datatype_cmd : bool -> string list -> (string list * binding * mixfix *
+ (binding * string list * mixfix) list) list -> theory ->
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -566,11 +566,11 @@
val (tyvars, _, _, _)::_ = dts;
val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
- let val full_tname = Sign.full_bname tmp_thy (Syntax.type_name tname mx)
+ let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
in (case duplicates (op =) tvs of
[] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
else error ("Mutually recursive datatypes must have same type parameters")
- | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
+ | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
" : " ^ commas dups))
end) dts);
@@ -585,13 +585,14 @@
val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs))
- in (constrs @ [((if flat_names then Sign.full_bname tmp_thy else
- Sign.full_bname_path tmp_thy tname) (Syntax.const_name cname mx'),
+ in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
+ Sign.full_name_path tmp_thy (Binding.name_of tname))
+ (Binding.map_name (Syntax.const_name mx') cname),
map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
- end handle ERROR msg =>
- cat_error msg ("The error above occured in constructor " ^ cname ^
- " of datatype " ^ tname);
+ end handle ERROR msg => cat_error msg
+ ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
+ " of datatype " ^ quote (Binding.str_of tname));
val (constrs', constr_syntax', sorts') =
fold prep_constr constrs ([], [], sorts)
@@ -599,11 +600,11 @@
in
case duplicates (op =) (map fst constrs') of
[] =>
- (dts' @ [(i, (Sign.full_bname tmp_thy (Syntax.type_name tname mx),
+ (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname),
map DtTFree tvs, constrs'))],
constr_syntax @ [constr_syntax'], sorts', i + 1)
| dups => error ("Duplicate constructors " ^ commas dups ^
- " in datatype " ^ tname)
+ " in datatype " ^ quote (Binding.str_of tname))
end;
val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
@@ -676,12 +677,13 @@
local structure P = OuterParse and K = OuterKeyword in
val datatype_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
- (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
+ Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
+ (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix));
fun mk_datatype args =
let
- val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
+ val names = map
+ (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
val specs = map (fn ((((_, vs), t), mx), cons) =>
(vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
in snd o add_datatype_cmd false names specs end;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Sun Mar 08 00:16:34 2009 +0100
@@ -15,7 +15,7 @@
val distinctness_limit_setup : theory -> theory
val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
string list -> DatatypeAux.descr list -> (string * sort) list ->
- (string * mixfix) list -> (string * mixfix) list list -> attribute
+ (binding * mixfix) list -> (binding * mixfix) list list -> attribute
-> theory -> (thm list list * thm list list * thm list list *
DatatypeAux.simproc_dist list * thm) * theory
end;
@@ -192,7 +192,7 @@
val (typedefs, thy3) = thy2 |>
parent_path flat_names |>
fold_map (fn ((((name, mx), tvs), c), name') =>
- TypedefPackage.add_typedef false (SOME name') (name, tvs, mx)
+ TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
(rtac exI 1 THEN rtac CollectI 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
@@ -212,7 +212,7 @@
(* isomorphism declarations *)
- val iso_decls = map (fn (T, s) => (s, T --> Univ_elT, NoSyn))
+ val iso_decls = map (fn (T, s) => (Binding.name s, T --> Univ_elT, NoSyn))
(oldTs ~~ rep_names');
(* constructor definitions *)
--- a/src/HOL/Tools/function_package/size.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML Sun Mar 08 00:16:34 2009 +0100
@@ -140,7 +140,7 @@
val ((size_def_thms, size_def_thms'), thy') =
thy
|> Sign.add_consts_i (map (fn (s, T) =>
- (NameSpace.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
+ (Binding.name (NameSpace.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
(size_names ~~ recTs1))
|> PureThy.add_defs false
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
--- a/src/HOL/Tools/inductive_realizer.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Mar 08 00:16:34 2009 +0100
@@ -68,8 +68,8 @@
val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
(Logic.strip_imp_concl (prop_of (hd intrs))));
val params = map dest_Var (Library.take (nparms, ts));
- val tname = space_implode "_" (NameSpace.base_name s ^ "T" :: vs);
- fun constr_of_intr intr = (NameSpace.base_name (name_of_thm intr),
+ val tname = Binding.name (space_implode "_" (NameSpace.base_name s ^ "T" :: vs));
+ fun constr_of_intr intr = (Binding.name (NameSpace.base_name (name_of_thm intr)),
map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
filter_out (equal Extraction.nullT) (map
(Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
@@ -234,7 +234,7 @@
end;
fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
- if (name: string) = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
+ if Binding.eq_name (name, s) then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
else x;
fun add_dummies f [] _ thy =
@@ -242,14 +242,14 @@
| add_dummies f dts used thy =
thy
|> f (map snd dts)
- |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
+ |-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
handle DatatypeAux.Datatype_Empty name' =>
let
val name = NameSpace.base_name name';
- val dname = Name.variant used "Dummy"
+ val dname = Name.variant used "Dummy";
in
thy
- |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
+ |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
end;
fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
@@ -296,7 +296,7 @@
val thy1' = thy1 |>
Theory.copy |>
- Sign.add_types (map (fn s => (NameSpace.base_name s, ar, NoSyn)) tnames) |>
+ Sign.add_types (map (fn s => (Binding.name (NameSpace.base_name s), ar, NoSyn)) tnames) |>
fold (fn s => AxClass.axiomatize_arity
(s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
Extraction.add_typeof_eqns_i ty_eqs;
@@ -308,7 +308,7 @@
val ((dummies, dt_info), thy2) =
thy1
|> add_dummies
- (DatatypePackage.add_datatype false false (map #2 dts))
+ (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
(map (pair false) dts) []
||> Extraction.add_typeof_eqns_i ty_eqs
||> Extraction.add_realizes_eqns_i rlz_eqs;
@@ -330,14 +330,17 @@
(if c = Extraction.nullt then c else list_comb (c, map Var (rev
(Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
(maps snd rss ~~ List.concat constrss);
- val (rlzpreds, rlzpreds') = split_list
- (distinct (op = o pairself (#1 o #1)) (map (fn rintr =>
+ val (rlzpreds, rlzpreds') =
+ rintrs |> map (fn rintr =>
let
- val Const (s, T) = head_of (HOLogic.dest_Trueprop
- (Logic.strip_assums_concl rintr));
+ val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
val s' = NameSpace.base_name s;
- val T' = Logic.unvarifyT T
- in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
+ val T' = Logic.unvarifyT T;
+ in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
+ |> distinct (op = o pairself (#1 o #1))
+ |> map (apfst (apfst (apfst Binding.name)))
+ |> split_list;
+
val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
(List.take (snd (strip_comb
(HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
--- a/src/HOL/Tools/inductive_set_package.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Sun Mar 08 00:16:34 2009 +0100
@@ -464,7 +464,7 @@
| NONE => u)) |>
Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
eta_contract (member op = cs' orf is_pred pred_arities))) intros;
- val cnames_syn' = map (fn (b, _) => (Binding.map_name (suffix "p") b, NoSyn)) cnames_syn;
+ val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
InductivePackage.add_ind_def
--- a/src/HOL/Tools/record_package.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Tools/record_package.ML Sun Mar 08 00:16:34 2009 +0100
@@ -1461,9 +1461,10 @@
Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name;
val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
+ val tname = Binding.name (NameSpace.base_name name);
in
thy
- |> TypecopyPackage.add_typecopy (suffix ext_typeN (NameSpace.base_name name), alphas) repT NONE
+ |> TypecopyPackage.add_typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
|-> (fn (name, _) => `(fn thy => get_thms thy name))
end;
@@ -1531,9 +1532,9 @@
(* 1st stage: defs_thy *)
fun mk_defs () =
thy
- |> extension_typedef name repT (alphas@[zeta])
+ |> extension_typedef name repT (alphas @ [zeta])
||> Sign.add_consts_i
- (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
+ (map (Syntax.no_syn o apfst Binding.name) (apfst base ext_decl :: dest_decls @ upd_decls))
||>> PureThy.add_defs false
(map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs))
||>> PureThy.add_defs false
@@ -1895,8 +1896,8 @@
(*record (scheme) type abbreviation*)
val recordT_specs =
- [(suffix schemeN bname, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
- (bname, alphas, recT0, Syntax.NoSyn)];
+ [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
+ (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
(*selectors*)
fun mk_sel_spec (c,T) =
@@ -1937,8 +1938,9 @@
|> Sign.add_tyabbrs_i recordT_specs
|> Sign.add_path bname
|> Sign.add_consts_i
- (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
- |> (Sign.add_consts_i o map Syntax.no_syn)
+ (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx))
+ sel_decls (field_syntax @ [Syntax.NoSyn]))
+ |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, Syntax.NoSyn)))
(upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
|> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs)
||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
--- a/src/HOL/Tools/typecopy_package.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Tools/typecopy_package.ML Sun Mar 08 00:16:34 2009 +0100
@@ -14,7 +14,7 @@
proj: string * typ,
proj_def: thm
}
- val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
+ val add_typecopy: binding * string list -> typ -> (binding * binding) option
-> theory -> (string * info) * theory
val get_typecopies: theory -> string list
val get_info: theory -> string -> info option
--- a/src/HOL/Tools/typedef_package.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOL/Tools/typedef_package.ML Sun Mar 08 00:16:34 2009 +0100
@@ -13,12 +13,12 @@
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
Rep_induct: thm, Abs_induct: thm}
val get_info: theory -> string -> info option
- val add_typedef: bool -> string option -> bstring * string list * mixfix ->
- term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
- val typedef: (bool * string) * (bstring * string list * mixfix) * term
- * (string * string) option -> theory -> Proof.state
- val typedef_cmd: (bool * string) * (bstring * string list * mixfix) * string
- * (string * string) option -> theory -> Proof.state
+ 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 interpretation: (string -> theory -> theory) -> theory -> theory
val setup: theory -> theory
end;
@@ -51,9 +51,6 @@
(* prepare_typedef *)
-fun err_in_typedef msg name =
- cat_error msg ("The error(s) above occurred in typedef " ^ quote name);
-
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
@@ -63,10 +60,12 @@
let
val _ = Theory.requires thy "Typedef" "typedefs";
val ctxt = ProofContext.init thy;
- val full = Sign.full_bname thy;
+
+ val full = Sign.full_name thy;
+ val full_name = full name;
+ val bname = Binding.name_of name;
(*rhs*)
- val full_name = full name;
val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
val setT = Term.fastype_of set;
val rhs_tfrees = Term.add_tfrees set [];
@@ -81,11 +80,14 @@
|> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
|> map TFree;
- val tname = Syntax.type_name t mx;
+ val tname = Binding.map_name (Syntax.type_name mx) t;
val full_tname = full tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
- val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
+ val (Rep_name, Abs_name) =
+ (case opt_morphs of
+ NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
+ | SOME morphs => morphs);
val setT' = map Term.itselfT args_setT ---> setT;
val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
val RepC = Const (full Rep_name, newT --> oldT);
@@ -97,15 +99,15 @@
val set' = if def then setC else set;
val goal' = mk_inhabited set';
val goal = mk_inhabited set;
- val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT));
+ val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT));
(*axiomatization*)
- val typedef_name = "type_definition_" ^ name;
+ val typedef_name = Binding.prefix_name "type_definition_" name;
val typedefC =
Const (@{const_name type_definition},
(newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
- val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' [];
+ val typedef_deps = Term.add_consts set' [];
(*set definition*)
fun add_def theory =
@@ -131,7 +133,7 @@
(Abs_name, oldT --> newT, NoSyn)]
#> add_def
#-> (fn set_def =>
- PureThy.add_axioms [((Binding.name typedef_name, typedef_prop),
+ PureThy.add_axioms [((typedef_name, typedef_prop),
[Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
##>> pair set_def)
##> Theory.add_deps "" (dest_Const RepC) typedef_deps
@@ -142,21 +144,21 @@
val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
thy1
- |> Sign.add_path name
+ |> Sign.add_path (Binding.name_of name)
|> PureThy.add_thms
- ((map o apfst o apfst) Binding.name [((Rep_name, make @{thm type_definition.Rep}), []),
- ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []),
- ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []),
- ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []),
- ((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []),
- ((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}),
- [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]),
- ((Abs_name ^ "_cases", make @{thm type_definition.Abs_cases}),
- [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
- ((Rep_name ^ "_induct", make @{thm type_definition.Rep_induct}),
- [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]),
- ((Abs_name ^ "_induct", make @{thm type_definition.Abs_induct}),
- [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
+ [((Rep_name, make @{thm type_definition.Rep}), []),
+ ((Binding.suffix_name "_inverse" Rep_name, make @{thm type_definition.Rep_inverse}), []),
+ ((Binding.suffix_name "_inverse" Abs_name, make @{thm type_definition.Abs_inverse}), []),
+ ((Binding.suffix_name "_inject" Rep_name, make @{thm type_definition.Rep_inject}), []),
+ ((Binding.suffix_name "_inject" Abs_name, make @{thm type_definition.Abs_inject}), []),
+ ((Binding.suffix_name "_cases" Rep_name, make @{thm type_definition.Rep_cases}),
+ [RuleCases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
+ ((Binding.suffix_name "_cases" Abs_name, make @{thm type_definition.Abs_cases}),
+ [RuleCases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
+ ((Binding.suffix_name "_induct" Rep_name, make @{thm type_definition.Rep_induct}),
+ [RuleCases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
+ ((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}),
+ [RuleCases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
||> Sign.parent_path;
val info = {rep_type = oldT, abs_type = newT,
Rep_name = full Rep_name, Abs_name = full Abs_name,
@@ -201,7 +203,8 @@
|> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal);
in (set, goal, goal_pat, typedef_result) end
- handle ERROR msg => err_in_typedef msg name;
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name));
(* add_typedef: tactic interface *)
@@ -245,13 +248,14 @@
val typedef_decl =
Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
+ ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
--| P.$$$ ")") (true, NONE) --
- (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
+ (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 (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
+ typedef_cmd ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name),
+ (t, vs, mx), A, morphs);
val _ =
OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Mar 08 00:16:34 2009 +0100
@@ -324,6 +324,8 @@
clist [a] = a |
clist (a::r) = a ^ " || " ^ (clist r);
+val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
+
(* add_ioa *)
@@ -351,7 +353,7 @@
(automaton_name ^ "_trans",
"(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
(automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
-|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
+|> add_defs
[(automaton_name ^ "_initial_def",
automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
(automaton_name ^ "_asig_def",
@@ -392,7 +394,7 @@
Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
-|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
+|> add_defs
[(automaton_name ^ "_def",
automaton_name ^ " == " ^ comp_list)]
end)
@@ -407,7 +409,7 @@
thy
|> ContConsts.add_consts_i
[(automaton_name, auttyp,NoSyn)]
-|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
+|> add_defs
[(automaton_name ^ "_def",
automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)]
end)
@@ -421,7 +423,7 @@
thy
|> ContConsts.add_consts_i
[(automaton_name, auttyp,NoSyn)]
-|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
+|> add_defs
[(automaton_name ^ "_def",
automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)]
end)
@@ -447,7 +449,7 @@
Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
-|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
+|> add_defs
[(automaton_name ^ "_def",
automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
end)
--- a/src/HOLCF/Tools/cont_consts.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML Sun Mar 08 00:16:34 2009 +0100
@@ -52,11 +52,11 @@
is generated and connected to the other declaration via some translation.
*)
fun fix_mixfix (syn , T, mx as Infix p ) =
- (Syntax.const_name syn mx, T, InfixName (syn, p))
+ (Syntax.const_name mx syn, T, InfixName (syn, p))
| fix_mixfix (syn , T, mx as Infixl p ) =
- (Syntax.const_name syn mx, T, InfixlName (syn, p))
+ (Syntax.const_name mx syn, T, InfixlName (syn, p))
| fix_mixfix (syn , T, mx as Infixr p ) =
- (Syntax.const_name syn mx, T, InfixrName (syn, p))
+ (Syntax.const_name mx syn, T, InfixrName (syn, p))
| fix_mixfix decl = decl;
fun transform decl = let
val (c, T, mx) = fix_mixfix decl;
@@ -73,7 +73,7 @@
| is_contconst (_,_,Binder _) = false
| is_contconst (c,T,mx ) = cfun_arity T >= Syntax.mixfix_args mx
handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
- quote (Syntax.const_name c mx));
+ quote (Syntax.const_name mx c));
(* add_consts(_i) *)
@@ -85,10 +85,9 @@
val transformed_decls = map transform contconst_decls;
in
thy
- |> Sign.add_consts_i normal_decls
- |> Sign.add_consts_i (map first transformed_decls)
- |> Sign.add_syntax_i (map second transformed_decls)
- |> Sign.add_trrules_i (List.concat (map third transformed_decls))
+ |> (Sign.add_consts_i o map (upd_first Binding.name))
+ (normal_decls @ map first transformed_decls @ map second transformed_decls)
+ |> Sign.add_trrules_i (maps third transformed_decls)
end;
val add_consts = gen_add_consts Syntax.read_typ_global;
--- a/src/HOLCF/Tools/domain/domain_extender.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Sun Mar 08 00:16:34 2009 +0100
@@ -103,7 +103,7 @@
(Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
o fst) eqs''';
val cons''' = map snd eqs''';
- fun thy_type (dname,tvars) = (NameSpace.base_name dname, length tvars, NoSyn);
+ fun thy_type (dname,tvars) = (Binding.name (NameSpace.base_name dname), length tvars, NoSyn);
fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS);
val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
@@ -119,7 +119,7 @@
| typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
| typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
fun one_con (con,mx,args) =
- ((Syntax.const_name con mx),
+ ((Syntax.const_name mx con),
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
find_index_eq tp dts,
DatatypeAux.dtyp_of_typ new_dts tp),
--- a/src/HOLCF/Tools/domain/domain_syntax.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML Sun Mar 08 00:16:34 2009 +0100
@@ -75,7 +75,7 @@
local open Syntax in
local
- fun c_ast con mx = Constant (const_name con mx);
+ fun c_ast con mx = Constant (Syntax.const_name mx con);
fun expvar n = Variable ("e"^(string_of_int n));
fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
(string_of_int m));
--- a/src/HOLCF/Tools/pcpodef_package.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML Sun Mar 08 00:16:34 2009 +0100
@@ -7,14 +7,14 @@
signature PCPODEF_PACKAGE =
sig
- val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
- * (string * string) option -> theory -> Proof.state
- val pcpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
- * (string * string) option -> theory -> Proof.state
- val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
- * (string * string) option -> theory -> Proof.state
- val cpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
- * (string * string) option -> theory -> Proof.state
+ val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
+ * (binding * binding) option -> theory -> Proof.state
+ val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
+ * (binding * binding) option -> theory -> Proof.state
+ val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
+ * (binding * binding) option -> theory -> Proof.state
+ val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
+ * (binding * binding) option -> theory -> Proof.state
end;
structure PcpodefPackage: PCPODEF_PACKAGE =
@@ -24,9 +24,6 @@
(* prepare_cpodef *)
-fun err_in_cpodef msg name =
- cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
-
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
@@ -36,10 +33,12 @@
let
val _ = Theory.requires thy "Pcpodef" "pcpodefs";
val ctxt = ProofContext.init thy;
- val full = Sign.full_bname thy;
+
+ val full = Sign.full_name thy;
+ val full_name = full name;
+ val bname = Binding.name_of name;
(*rhs*)
- val full_name = full name;
val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
val setT = Term.fastype_of set;
val rhs_tfrees = Term.add_tfrees set [];
@@ -58,11 +57,14 @@
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
val lhs_sorts = map snd lhs_tfrees;
- val tname = Syntax.type_name t mx;
+ val tname = Binding.map_name (Syntax.type_name mx) t;
val full_tname = full tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
- val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
+ val (Rep_name, Abs_name) =
+ (case opt_morphs of
+ NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
+ | SOME morphs => morphs);
val RepC = Const (full Rep_name, newT --> oldT);
fun lessC T = Const (@{const_name sq_le}, T --> T --> HOLogic.boolT);
val less_def = Logic.mk_equals (lessC newT,
@@ -76,7 +78,8 @@
|> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
val less_def' = Syntax.check_term lthy3 less_def;
val ((_, (_, less_definition')), lthy4) = lthy3
- |> Specification.definition (NONE, ((Binding.name ("less_" ^ name ^ "_def"), []), less_def'));
+ |> Specification.definition (NONE,
+ ((Binding.prefix_name "less_" (Binding.suffix_name "_def" name), []), less_def'));
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
val thy5 = lthy4
@@ -95,14 +98,14 @@
val cpo_thms' = map (Thm.transfer theory') cpo_thms;
in
theory'
- |> Sign.add_path name
+ |> Sign.add_path (Binding.name_of name)
|> PureThy.add_thms
- ([((Binding.name ("adm_" ^ name), admissible'), []),
- ((Binding.name ("cont_" ^ Rep_name), @{thm typedef_cont_Rep} OF cpo_thms'), []),
- ((Binding.name ("cont_" ^ Abs_name), @{thm typedef_cont_Abs} OF cpo_thms'), []),
- ((Binding.name ("lub_" ^ name), @{thm typedef_lub} OF cpo_thms'), []),
- ((Binding.name ("thelub_" ^ name), @{thm typedef_thelub} OF cpo_thms'), []),
- ((Binding.name ("compact_" ^ name), @{thm typedef_compact} OF cpo_thms'), [])])
+ ([((Binding.prefix_name "adm_" name, admissible'), []),
+ ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
+ ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
+ ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
+ ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
+ ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
|> snd
|> Sign.parent_path
end;
@@ -117,15 +120,14 @@
val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
in
theory'
- |> Sign.add_path name
+ |> Sign.add_path (Binding.name_of name)
|> PureThy.add_thms
- ([((Binding.name (Rep_name ^ "_strict"), @{thm typedef_Rep_strict} OF pcpo_thms'), []),
- ((Binding.name (Abs_name ^ "_strict"), @{thm typedef_Abs_strict} OF pcpo_thms'), []),
- ((Binding.name (Rep_name ^ "_strict_iff"), @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
- ((Binding.name (Abs_name ^ "_strict_iff"), @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
- ((Binding.name (Rep_name ^ "_defined"), @{thm typedef_Rep_defined} OF pcpo_thms'), []),
- ((Binding.name (Abs_name ^ "_defined"), @{thm typedef_Abs_defined} OF pcpo_thms'), [])
- ])
+ ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
|> snd
|> Sign.parent_path
end;
@@ -142,7 +144,8 @@
then (goal_UU_mem, goal_admissible, pcpodef_result)
else (goal_nonempty, goal_admissible, cpodef_result)
end
- handle ERROR msg => err_in_cpodef msg name;
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
(* proof interface *)
@@ -174,14 +177,14 @@
val typedef_proof_decl =
Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
+ ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
--| P.$$$ ")") (true, NONE) --
- (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
+ (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+ Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
(if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
- ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
+ ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
val _ =
OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
--- a/src/Pure/General/binding.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/General/binding.ML Sun Mar 08 00:16:34 2009 +0100
@@ -11,22 +11,24 @@
sig
type binding
val dest: binding -> (string * bool) list * bstring
- val verbose: bool ref
val str_of: binding -> string
val make: bstring * Position.T -> binding
val pos_of: binding -> Position.T
val name: bstring -> binding
val name_of: binding -> string
val map_name: (bstring -> bstring) -> binding -> binding
+ val prefix_name: string -> binding -> binding
+ val suffix_name: string -> binding -> binding
+ val eq_name: binding * binding -> bool
val empty: binding
val is_empty: binding -> bool
val qualify: bool -> string -> binding -> binding
val prefix_of: binding -> (string * bool) list
val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
- val add_prefix: bool -> string -> binding -> binding
+ val prefix: bool -> string -> binding -> binding
end;
-structure Binding: BINDING =
+structure Binding:> BINDING =
struct
(** representation **)
@@ -47,20 +49,9 @@
fun dest (Binding {prefix, qualifier, name, ...}) = (prefix @ qualifier, name);
-
-(* diagnostic output *)
-
-val verbose = ref false;
-
-val str_of_components = implode o map (fn (s, true) => s ^ "!" | (s, false) => s ^ "?");
-
fun str_of (Binding {prefix, qualifier, name, pos}) =
let
- val text =
- if ! verbose then
- (if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^
- str_of_components qualifier ^ name
- else name;
+ val text = space_implode "." (map #1 qualifier @ [name]);
val props = Position.properties_of pos;
in Markup.markup (Markup.properties props (Markup.binding name)) text end;
@@ -76,7 +67,11 @@
fun pos_of (Binding {pos, ...}) = pos;
fun name_of (Binding {name, ...}) = name;
+fun eq_name (b, b') = name_of b = name_of b';
+
fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos));
+val prefix_name = map_name o prefix;
+val suffix_name = map_name o suffix;
val empty = name "";
fun is_empty b = name_of b = "";
@@ -85,8 +80,8 @@
(* user qualifier *)
fun qualify _ "" = I
- | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
- (prefix, (qual, mandatory) :: qualifier, name, pos));
+ | qualify strict qual = map_binding (fn (prefix, qualifier, name, pos) =>
+ (prefix, (qual, strict) :: qualifier, name, pos));
(* system prefix *)
@@ -96,8 +91,8 @@
fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
(f prefix, qualifier, name, pos));
-fun add_prefix _ "" = I
- | add_prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
+fun prefix _ "" = I
+ | prefix strict prfx = map_prefix (cons (prfx, strict));
end;
--- a/src/Pure/Isar/class.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/Isar/class.ML Sun Mar 08 00:16:34 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
@@ -66,15 +66,14 @@
(* canonical interpretation *)
val base_morph = inst_morph
- $> Morphism.binding_morphism
- (Binding.add_prefix false (class_prefix class))
+ $> Morphism.binding_morphism (Binding.prefix false (class_prefix class))
$> Element.satisfy_morphism (the_list wit);
val defs = these_defs thy sups;
val eq_morph = Element.eq_morphism thy defs;
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';
@@ -170,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: "
@@ -201,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 [];
@@ -218,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
@@ -228,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
@@ -262,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)]
@@ -274,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 23:41:04 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Sun Mar 08 00:16:34 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 23:41:04 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML Sun Mar 08 00:16:34 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 23:41:04 2009 +0100
+++ b/src/Pure/Isar/expression.ML Sun Mar 08 00:16:34 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
@@ -186,7 +184,7 @@
val inst = Symtab.make insts'';
in
(Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
- Morphism.binding_morphism (Binding.add_prefix strict prfx), ctxt')
+ Morphism.binding_morphism (Binding.prefix strict prfx), ctxt')
end;
@@ -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_cmd.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sun Mar 08 00:16:34 2009 +0100
@@ -12,7 +12,7 @@
val print_translation: bool * (string * Position.T) -> theory -> theory
val typed_print_translation: bool * (string * Position.T) -> theory -> theory
val print_ast_translation: bool * (string * Position.T) -> theory -> theory
- val oracle: bstring -> SymbolPos.text * Position.T -> theory -> theory
+ val oracle: bstring * Position.T -> SymbolPos.text * Position.T -> theory -> theory
val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
val declaration: string * Position.T -> local_theory -> local_theory
@@ -145,25 +145,25 @@
(* oracles *)
-fun oracle name (oracle_txt, pos) =
+fun oracle (name, pos) (body_txt, body_pos) =
let
- val oracle = SymbolPos.content (SymbolPos.explode (oracle_txt, pos));
+ val body = SymbolPos.content (SymbolPos.explode (body_txt, body_pos));
val txt =
"local\n\
\ val name = " ^ ML_Syntax.print_string name ^ ";\n\
\ val pos = " ^ ML_Syntax.print_position pos ^ ";\n\
\ val binding = Binding.make (name, pos);\n\
- \ val oracle = " ^ oracle ^ ";\n\
+ \ val body = " ^ body ^ ";\n\
\in\n\
- \ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
+ \ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
\end;\n";
- in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;
+ in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos txt)) end;
(* axioms *)
fun add_axms f args thy =
- f (map (fn ((b, ax), srcs) => ((Binding.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
+ f (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args) thy;
val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
--- a/src/Pure/Isar/isar_syn.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sun Mar 08 00:16:34 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";
@@ -371,7 +371,8 @@
val _ =
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
- (P.name -- (P.$$$ "=" |-- P.ML_source) >> (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
+ (P.position P.name -- (P.$$$ "=" |-- P.ML_source) >>
+ (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
(* local theories *)
@@ -391,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"
@@ -429,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 23:41:04 2009 +0100
+++ b/src/Pure/Isar/locale.ML Sun Mar 08 00:16:34 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 23:41:04 2009 +0100
+++ b/src/Pure/Isar/object_logic.ML Sun Mar 08 00:16:34 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/outer_parse.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML Sun Mar 08 00:16:34 2009 +0100
@@ -81,6 +81,7 @@
val opt_mixfix': mixfix parser
val where_: string parser
val const: (string * string * mixfix) parser
+ val const_binding: (binding * string * mixfix) parser
val params: (binding * string option) list parser
val simple_fixes: (binding * string option) list parser
val fixes: (binding * string option * mixfix) list parser
@@ -291,6 +292,7 @@
val where_ = $$$ "where";
val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
+val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
>> (fn (xs, T) => map (rpair T) xs);
--- a/src/Pure/Isar/specification.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/Isar/specification.ML Sun Mar 08 00:16:34 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 23:41:04 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Sun Mar 08 00:16:34 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 23:41:04 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Sun Mar 08 00:16:34 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 23:41:04 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Sun Mar 08 00:16:34 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/Syntax/mixfix.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/Syntax/mixfix.ML Sun Mar 08 00:16:34 2009 +0100
@@ -27,8 +27,8 @@
val literal: string -> mixfix
val no_syn: 'a * 'b -> 'a * 'b * mixfix
val pretty_mixfix: mixfix -> Pretty.T
- val type_name: string -> mixfix -> string
- val const_name: string -> mixfix -> string
+ val type_name: mixfix -> string -> string
+ val const_name: mixfix -> string -> string
val const_mixfix: string -> mixfix -> string * mixfix
val mixfix_args: mixfix -> int
val mixfixT: mixfix -> typ
@@ -105,28 +105,28 @@
fun deprecated c = (legacy_feature ("Unnamed infix operator " ^ quote c); c);
-fun type_name t (InfixName _) = t
- | type_name t (InfixlName _) = t
- | type_name t (InfixrName _) = t
- | type_name t (Infix _) = deprecated (strip_esc t)
- | type_name t (Infixl _) = deprecated (strip_esc t)
- | type_name t (Infixr _) = deprecated (strip_esc t)
- | type_name t _ = t;
+fun type_name (InfixName _) = I
+ | type_name (InfixlName _) = I
+ | type_name (InfixrName _) = I
+ | type_name (Infix _) = deprecated o strip_esc
+ | type_name (Infixl _) = deprecated o strip_esc
+ | type_name (Infixr _) = deprecated o strip_esc
+ | type_name _ = I;
-fun const_name c (InfixName _) = c
- | const_name c (InfixlName _) = c
- | const_name c (InfixrName _) = c
- | const_name c (Infix _) = "op " ^ deprecated (strip_esc c)
- | const_name c (Infixl _) = "op " ^ deprecated (strip_esc c)
- | const_name c (Infixr _) = "op " ^ deprecated (strip_esc c)
- | const_name c _ = c;
+fun const_name (InfixName _) = I
+ | const_name (InfixlName _) = I
+ | const_name (InfixrName _) = I
+ | const_name (Infix _) = prefix "op " o deprecated o strip_esc
+ | const_name (Infixl _) = prefix "op " o deprecated o strip_esc
+ | const_name (Infixr _) = prefix "op " o deprecated o strip_esc
+ | const_name _ = I;
fun fix_mixfix c (Infix p) = InfixName (c, p)
| fix_mixfix c (Infixl p) = InfixlName (c, p)
| fix_mixfix c (Infixr p) = InfixrName (c, p)
| fix_mixfix _ mx = mx;
-fun const_mixfix c mx = (const_name c mx, fix_mixfix c mx);
+fun const_mixfix c mx = (const_name mx c, fix_mixfix c mx);
fun map_mixfix _ NoSyn = NoSyn
| map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p)
@@ -158,7 +158,7 @@
fun syn_ext_types type_decls =
let
- fun name_of (t, _, mx) = type_name t mx;
+ fun name_of (t, _, mx) = type_name mx t;
fun mk_infix sy t p1 p2 p3 =
SynExt.Mfix ("(_ " ^ sy ^ "/ _)",
@@ -189,7 +189,7 @@
fun syn_ext_consts is_logtype const_decls =
let
- fun name_of (c, _, mx) = const_name c mx;
+ fun name_of (c, _, mx) = const_name mx c;
fun mk_infix sy ty c p1 p2 p3 =
[SynExt.Mfix ("op " ^ sy, ty, c, [], SynExt.max_pri),
--- a/src/Pure/axclass.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/axclass.ML Sun Mar 08 00:16:34 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/drule.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/drule.ML Sun Mar 08 00:16:34 2009 +0100
@@ -77,6 +77,7 @@
val beta_conv: cterm -> cterm -> cterm
val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
val flexflex_unique: thm -> thm
+ val get_def: theory -> xstring -> thm
val store_thm: bstring -> thm -> thm
val store_standard_thm: bstring -> thm -> thm
val store_thm_open: bstring -> thm -> thm
@@ -459,6 +460,8 @@
val read_prop = certify o SimpleSyntax.read_prop;
+fun get_def thy = Thm.axiom thy o NameSpace.intern (Theory.axiom_space thy) o Thm.def_name;
+
fun store_thm name th =
Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
--- a/src/Pure/meta_simplifier.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/meta_simplifier.ML Sun Mar 08 00:16:34 2009 +0100
@@ -22,24 +22,6 @@
type solver
val mk_solver': string -> (simpset -> int -> tactic) -> solver
val mk_solver: string -> (thm list -> int -> tactic) -> solver
- val rep_ss: simpset ->
- {rules: rrule Net.net,
- prems: thm list,
- bounds: int * ((string * typ) * string) list,
- depth: int * bool ref,
- context: Proof.context option} *
- {congs: (string * cong) list * string list,
- procs: proc Net.net,
- mk_rews:
- {mk: thm -> thm list,
- mk_cong: thm -> thm,
- mk_sym: thm -> thm option,
- mk_eq_True: thm -> thm option,
- reorient: theory -> term list -> term -> term -> bool},
- termless: term * term -> bool,
- subgoal_tac: simpset -> int -> tactic,
- loop_tacs: (string * (simpset -> int -> tactic)) list,
- solvers: solver list * solver list}
val empty_ss: simpset
val merge_ss: simpset * simpset -> simpset
val pretty_ss: simpset -> Pretty.T
@@ -90,6 +72,24 @@
sig
include BASIC_META_SIMPLIFIER
exception SIMPLIFIER of string * thm
+ val internal_ss: simpset ->
+ {rules: rrule Net.net,
+ prems: thm list,
+ bounds: int * ((string * typ) * string) list,
+ depth: int * bool ref,
+ context: Proof.context option} *
+ {congs: (string * cong) list * string list,
+ procs: proc Net.net,
+ mk_rews:
+ {mk: thm -> thm list,
+ mk_cong: thm -> thm,
+ mk_sym: thm -> thm option,
+ mk_eq_True: thm -> thm option,
+ reorient: theory -> term list -> term -> term -> bool},
+ termless: term * term -> bool,
+ subgoal_tac: simpset -> int -> tactic,
+ loop_tacs: (string * (simpset -> int -> tactic)) list,
+ solvers: solver list * solver list}
val add_simp: thm -> simpset -> simpset
val del_simp: thm -> simpset -> simpset
val solver: simpset -> solver -> int -> tactic
@@ -214,7 +214,7 @@
id: stamp};
-fun rep_ss (Simpset args) = args;
+fun internal_ss (Simpset args) = args;
fun make_ss1 (rules, prems, bounds, depth, context) =
{rules = rules, prems = prems, bounds = bounds, depth = depth, context = context};
@@ -696,7 +696,7 @@
in
-val mksimps = #mk o #mk_rews o #2 o rep_ss;
+fun mksimps (Simpset (_, {mk_rews = {mk, ...}, ...})) = mk;
fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
--- a/src/Pure/more_thm.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/more_thm.ML Sun Mar 08 00:16:34 2009 +0100
@@ -55,6 +55,8 @@
val position_of: thm -> Position.T
val default_position: Position.T -> thm -> thm
val default_position_of: thm -> thm -> thm
+ val def_name: string -> string
+ val def_name_optional: string -> string -> string
val has_name_hint: thm -> bool
val get_name_hint: thm -> string
val put_name_hint: string -> thm -> thm
@@ -278,6 +280,8 @@
(** specification primitives **)
+(* rules *)
+
fun add_axiom (b, prop) thy =
let
val b' = if Binding.is_empty b
@@ -342,6 +346,14 @@
val default_position_of = default_position o position_of;
+(* def_name *)
+
+fun def_name c = c ^ "_def";
+
+fun def_name_optional c "" = def_name c
+ | def_name_optional _ name = name;
+
+
(* unofficial theorem names *)
fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN);
--- a/src/Pure/pure_thy.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/pure_thy.ML Sun Mar 08 00:16:34 2009 +0100
@@ -36,14 +36,14 @@
val note_thmss_grouped: string -> string -> (Thm.binding *
(thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
- val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
+ val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
val add_defs: bool -> ((binding * term) * attribute list) list ->
theory -> thm list * theory
val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
theory -> thm list * theory
- val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
+ val add_defs_cmd: bool -> ((binding * string) * attribute list) list ->
theory -> thm list * theory
- val add_defs_unchecked_cmd: bool -> ((bstring * string) * attribute list) list ->
+ val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list ->
theory -> thm list * theory
val old_appl_syntax: theory -> bool
val old_appl_syntax_setup: theory -> theory
@@ -227,19 +227,19 @@
local
fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b);
fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
- fun add_axm prep_b add = fold_map (fn ((b, ax), atts) => fn thy =>
+ fun add_axm add = fold_map (fn ((b, ax), atts) => fn thy =>
let
val named_ax = [(b, ax)];
val thy' = add named_ax thy;
- val thm = hd (get_axs thy' ((map o apfst) prep_b named_ax));
- in apfst hd (gen_add_thms (K I) [((prep_b b, thm), atts)] thy') end);
+ val thm = hd (get_axs thy' named_ax);
+ in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end);
in
- val add_defs = add_axm I o Theory.add_defs_i false;
- val add_defs_unchecked = add_axm I o Theory.add_defs_i true;
- val add_axioms = add_axm I Theory.add_axioms_i;
- val add_defs_cmd = add_axm Binding.name o Theory.add_defs false;
- val add_defs_unchecked_cmd = add_axm Binding.name o Theory.add_defs true;
- val add_axioms_cmd = add_axm Binding.name Theory.add_axioms;
+ val add_defs = add_axm o Theory.add_defs_i false;
+ val add_defs_unchecked = add_axm o Theory.add_defs_i true;
+ val add_axioms = add_axm Theory.add_axioms_i;
+ val add_defs_cmd = add_axm o Theory.add_defs false;
+ val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
+ val add_axioms_cmd = add_axm Theory.add_axioms;
end;
@@ -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)"),
@@ -389,6 +389,6 @@
#> Sign.hide_const false "Pure.sort_constraint"
#> Sign.hide_const false "Pure.conjunction"
#> add_thmss [((Binding.name "nothing", []), [])] #> snd
- #> Theory.add_axioms_i ((map o apfst) Binding.name Proofterm.equality_axms)));
+ #> Theory.add_axioms_i (map (apfst Binding.name) Proofterm.equality_axms)));
end;
--- a/src/Pure/sign.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/sign.ML Sun Mar 08 00:16:34 2009 +0100
@@ -14,6 +14,7 @@
consts: Consts.T}
val naming_of: theory -> NameSpace.naming
val full_name: theory -> binding -> string
+ val full_name_path: theory -> string -> binding -> string
val full_bname: theory -> bstring -> string
val full_bname_path: theory -> string -> bstring -> string
val syn_of: theory -> Syntax.syntax
@@ -78,24 +79,24 @@
val cert_arity: theory -> arity -> arity
val add_defsort: string -> theory -> theory
val add_defsort_i: sort -> theory -> theory
- val add_types: (bstring * int * mixfix) list -> theory -> theory
- val add_nonterminals: bstring list -> theory -> theory
- val add_tyabbrs: (bstring * string list * string * mixfix) list -> theory -> theory
- val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> theory -> theory
- val add_syntax: (bstring * string * mixfix) list -> theory -> theory
- val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
- val add_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
- val add_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
- val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
- val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
+ val add_types: (binding * int * mixfix) list -> theory -> theory
+ val add_nonterminals: binding list -> theory -> theory
+ val add_tyabbrs: (binding * string list * string * mixfix) list -> theory -> theory
+ val add_tyabbrs_i: (binding * string list * typ * mixfix) list -> theory -> theory
+ val add_syntax: (string * string * mixfix) list -> theory -> theory
+ val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
+ val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
+ val add_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
+ val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
+ val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
val declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
- val add_consts: (bstring * string * mixfix) list -> theory -> theory
- val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
+ val add_consts: (binding * string * mixfix) list -> theory -> theory
+ val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
val add_abbrev: string -> Properties.T -> binding * term -> theory -> (term * term) * theory
val revert_abbrev: string -> string -> theory -> theory
val add_const_constraint: string * typ option -> theory -> theory
- val primitive_class: string * class list -> theory -> theory
+ val primitive_class: binding * class list -> theory -> theory
val primitive_classrel: class * class -> theory -> theory
val primitive_arity: arity -> theory -> theory
val add_trfuns:
@@ -186,9 +187,10 @@
val naming_of = #naming o rep_sg;
val full_name = NameSpace.full_name o naming_of;
+fun full_name_path thy path = NameSpace.full_name (NameSpace.add_path path (naming_of thy));
+
fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
-fun full_bname_path thy elems =
- NameSpace.full_name (NameSpace.add_path elems (naming_of thy)) o Binding.name;
+fun full_bname_path thy path = full_name_path thy path o Binding.name;
(* syntax *)
@@ -435,8 +437,8 @@
fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_type_gram types syn;
- val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
+ val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Binding.name_of a, n, mx)) types) syn;
+ val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
val tags = [(Markup.theory_nameN, Context.theory_name thy)];
val tsig' = fold (Type.add_type naming tags) decls tsig;
in (naming, syn', tsig', consts) end);
@@ -446,7 +448,7 @@
fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_consts ns syn;
+ val syn' = Syntax.update_consts (map Binding.name_of ns) syn;
val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
in (naming, syn', tsig', consts) end);
@@ -457,10 +459,10 @@
thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
val ctxt = ProofContext.init thy;
- val syn' = Syntax.update_type_gram [(a, length vs, mx)] syn;
- val a' = Syntax.type_name a mx;
- val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
- handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
+ val syn' = Syntax.update_type_gram [(Binding.name_of a, length vs, mx)] syn;
+ val b = Binding.map_name (Syntax.type_name mx) a;
+ val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
+ handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
val tsig' = Type.add_abbrev naming [] abbr tsig;
in (naming, syn', tsig', consts) end);
@@ -475,7 +477,7 @@
val ctxt = ProofContext.init thy;
fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
handle ERROR msg =>
- cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
+ cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name mx c));
in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
fun gen_add_syntax x = gen_syntax Syntax.update_const_gram x;
@@ -522,12 +524,10 @@
|> pair (map #3 args)
end;
-fun bindify (name, T, mx) = (Binding.name name, T, mx);
-
in
-fun add_consts args = snd o gen_add_consts Syntax.parse_typ false [] (map bindify args);
-fun add_consts_i args = snd o gen_add_consts (K I) false [] (map bindify args);
+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 declare_const tags ((b, T), mx) thy =
let
@@ -571,10 +571,10 @@
fun primitive_class (bclass, classes) thy =
thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_consts [bclass] syn;
+ val syn' = Syntax.update_consts [Binding.name_of bclass] syn;
val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
in (naming, syn', tsig', consts) end)
- |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
+ |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Syntax.pp_global thy) arg);
--- a/src/Pure/simplifier.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/simplifier.ML Sun Mar 08 00:16:34 2009 +0100
@@ -217,14 +217,14 @@
fun solve_all_tac solvers ss =
let
- val (_, {subgoal_tac, ...}) = MetaSimplifier.rep_ss ss;
+ val (_, {subgoal_tac, ...}) = MetaSimplifier.internal_ss ss;
val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
in DEPTH_SOLVE (solve_tac 1) end;
(*NOTE: may instantiate unknowns that appear also in other subgoals*)
fun generic_simp_tac safe mode ss =
let
- val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.rep_ss ss;
+ val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.internal_ss ss;
val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
(rev (if safe then solvers else unsafe_solvers)));
@@ -238,7 +238,7 @@
fun simp rew mode ss thm =
let
- val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.rep_ss ss;
+ val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.internal_ss ss;
val tacf = solve_all_tac (rev unsafe_solvers);
fun prover s th = Option.map #1 (Seq.pull (tacf s th));
in rew mode prover ss thm end;
--- a/src/Pure/theory.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/theory.ML Sun Mar 08 00:16:34 2009 +0100
@@ -29,10 +29,10 @@
val begin_theory: string -> theory list -> theory
val end_theory: theory -> theory
val add_axioms_i: (binding * term) list -> theory -> theory
- val add_axioms: (bstring * string) list -> theory -> theory
+ val add_axioms: (binding * string) list -> theory -> theory
val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
- val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
+ val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
val add_finals_i: bool -> term list -> theory -> theory
val add_finals: bool -> string list -> theory -> theory
val specify_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
@@ -153,9 +153,6 @@
(* prepare axioms *)
-fun err_in_axm msg name =
- cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
-
fun cert_axm thy (b, raw_tm) =
let
val (t, T, _) = Sign.certify_prop thy raw_tm
@@ -166,9 +163,9 @@
(b, Sign.no_vars (Syntax.pp_global thy) t)
end;
-fun read_axm thy (bname, str) =
- cert_axm thy (Binding.name bname, Syntax.read_prop_global thy str)
- handle ERROR msg => err_in_axm msg bname;
+fun read_axm thy (b, str) =
+ cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in axiom: " ^ quote (Binding.str_of b));
(* add_axioms(_i) *)
--- a/src/Pure/thm.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/thm.ML Sun Mar 08 00:16:34 2009 +0100
@@ -128,9 +128,6 @@
val hyps_of: thm -> term list
val full_prop_of: thm -> term
val axiom: theory -> string -> thm
- val def_name: string -> string
- val def_name_optional: string -> string -> string
- val get_def: theory -> xstring -> thm
val axioms_of: theory -> (string * thm) list
val get_name: thm -> string
val put_name: string -> thm -> thm
@@ -558,14 +555,6 @@
| NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
end;
-fun def_name c = c ^ "_def";
-
-fun def_name_optional c "" = def_name c
- | def_name_optional _ name = name;
-
-fun get_def thy = axiom thy o NameSpace.intern (Theory.axiom_space thy) o def_name;
-
-
(*return additional axioms of this theory node*)
fun axioms_of thy =
map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy));
--- a/src/Pure/type.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/Pure/type.ML Sun Mar 08 00:16:34 2009 +0100
@@ -69,12 +69,12 @@
val eq_type: tyenv -> typ * typ -> bool
(*extend and merge type signatures*)
- val add_class: Pretty.pp -> NameSpace.naming -> bstring * class list -> tsig -> tsig
+ val add_class: Pretty.pp -> NameSpace.naming -> binding * class list -> tsig -> tsig
val hide_class: bool -> string -> tsig -> tsig
val set_defsort: sort -> tsig -> tsig
- val add_type: NameSpace.naming -> Properties.T -> bstring * int -> tsig -> tsig
- val add_abbrev: NameSpace.naming -> Properties.T -> string * string list * typ -> tsig -> tsig
- val add_nonterminal: NameSpace.naming -> Properties.T -> string -> tsig -> tsig
+ val add_type: NameSpace.naming -> Properties.T -> binding * int -> tsig -> tsig
+ val add_abbrev: NameSpace.naming -> Properties.T -> binding * string list * typ -> tsig -> tsig
+ val add_nonterminal: NameSpace.naming -> Properties.T -> binding -> tsig -> tsig
val hide_type: bool -> string -> tsig -> tsig
val add_arity: Pretty.pp -> arity -> tsig -> tsig
val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
@@ -511,7 +511,7 @@
let
val cs' = map (cert_class tsig) cs
handle TYPE (msg, _, _) => error msg;
- val (c', space') = space |> NameSpace.declare naming (Binding.name c);
+ val (c', space') = space |> NameSpace.declare naming c;
val classes' = classes |> Sorts.add_class pp (c', cs');
in ((space', classes'), default, types) end);
@@ -555,9 +555,6 @@
local
-fun err_neg_args c =
- error ("Negative number of arguments in type constructor declaration: " ^ quote c);
-
fun err_in_decls c decl decl' =
let val s = str_of_decl decl and s' = str_of_decl decl' in
if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
@@ -567,7 +564,7 @@
fun new_decl naming tags (c, decl) (space, types) =
let
val tags' = tags |> Position.default_properties (Position.thread_data ());
- val (c', space') = NameSpace.declare naming (Binding.name c) space;
+ val (c', space') = NameSpace.declare naming c space;
val types' =
(case Symtab.lookup types c' of
SOME ((decl', _), _) => err_in_decls c' decl decl'
@@ -590,12 +587,14 @@
in
-fun add_type naming tags (c, n) = if n < 0 then err_neg_args c else
- map_types (new_decl naming tags (c, LogicalType n));
+fun add_type naming tags (c, n) =
+ if n < 0 then error ("Bad type constructor declaration: " ^ quote (Binding.str_of c))
+ else map_types (new_decl naming tags (c, LogicalType n));
fun add_abbrev naming tags (a, vs, rhs) tsig = tsig |> map_types (fn types =>
let
- fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote a);
+ fun err msg =
+ cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote (Binding.str_of a));
val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
handle TYPE (msg, _, _) => err msg;
in
--- a/src/ZF/Tools/datatype_package.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sun Mar 08 00:16:34 2009 +0100
@@ -245,14 +245,14 @@
fun add_recursor thy =
if need_recursor then
thy |> Sign.add_consts_i
- [(recursor_base_name, recursor_typ, NoSyn)]
+ [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
|> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
else thy;
val (con_defs, thy0) = thy_path
|> Sign.add_consts_i
- ((case_base_name, case_typ, NoSyn) ::
- map #1 (List.concat con_ty_lists))
+ (map (fn (c, T, mx) => (Binding.name c, T, mx))
+ ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists)))
|> PureThy.add_defs false
(map (Thm.no_attributes o apfst Binding.name)
(case_def ::
@@ -302,7 +302,7 @@
(*** Prove the recursor theorems ***)
- val recursor_eqns = case try (Thm.get_def thy1) recursor_base_name of
+ val recursor_eqns = case try (Drule.get_def thy1) recursor_base_name of
NONE => (writeln " [ No recursion operator ]";
[])
| SOME recursor_def =>
--- a/src/ZF/Tools/inductive_package.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sun Mar 08 00:16:34 2009 +0100
@@ -180,7 +180,7 @@
(*fetch fp definitions from the theory*)
val big_rec_def::part_rec_defs =
- map (Thm.get_def thy1)
+ map (Drule.get_def thy1)
(case rec_names of [_] => rec_names
| _ => big_rec_base_name::rec_names);
--- a/src/ZF/ind_syntax.ML Sat Mar 07 23:41:04 2009 +0100
+++ b/src/ZF/ind_syntax.ML Sun Mar 08 00:16:34 2009 +0100
@@ -73,7 +73,7 @@
val T = (map (#2 o dest_Free) args) ---> iT
handle TERM _ => error
"Bad variable in constructor specification"
- val name = Syntax.const_name id syn (*handle infix constructors*)
+ val name = Syntax.const_name syn id
in ((id,T,syn), name, args, prems) end;
val read_constructs = map o map o read_construct;