# HG changeset patch # User wenzelm # Date 1236465429 -3600 # Node ID 46aa785d1e296f6a685c60a38635e37550818e44 # Parent d9ecd70b111298ad81b54a18074c865a8d5465c1# Parent 90efbb8a8cb2a60343500edc3217a7c48fb597fc merged diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Import/proof_kernel.ML Sat Mar 07 23:37:09 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) diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Import/replay.ML --- a/src/HOL/Import/replay.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Import/replay.ML Sat Mar 07 23:37:09 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 = diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Sat Mar 07 23:37:09 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_-type together with -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; diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Sat Mar 07 23:37:09 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, diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Statespace/state_space.ML Sat Mar 07 23:37:09 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; diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Sat Mar 07 23:37:09 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, diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Tools/datatype_package.ML Sat Mar 07 23:37:09 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; diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Sat Mar 07 23:37:09 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 *) diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Tools/function_package/size.ML --- a/src/HOL/Tools/function_package/size.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Tools/function_package/size.ML Sat Mar 07 23:37:09 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))) diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Sat Mar 07 23:37:09 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)); diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Tools/inductive_set_package.ML --- a/src/HOL/Tools/inductive_set_package.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Tools/inductive_set_package.ML Sat Mar 07 23:37:09 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 diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Tools/record_package.ML Sat Mar 07 23:37:09 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) diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Tools/typecopy_package.ML --- a/src/HOL/Tools/typecopy_package.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Tools/typecopy_package.ML Sat Mar 07 23:37:09 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 diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOL/Tools/typedef_package.ML Sat Mar 07 23:37:09 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)" diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOLCF/IOA/meta_theory/ioa_package.ML --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Sat Mar 07 23:37:09 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) diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOLCF/Tools/cont_consts.ML --- a/src/HOLCF/Tools/cont_consts.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOLCF/Tools/cont_consts.ML Sat Mar 07 23:37:09 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; diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOLCF/Tools/domain/domain_extender.ML --- a/src/HOLCF/Tools/domain/domain_extender.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Sat Mar 07 23:37:09 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), diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOLCF/Tools/domain/domain_syntax.ML --- a/src/HOLCF/Tools/domain/domain_syntax.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML Sat Mar 07 23:37:09 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)); diff -r d9ecd70b1112 -r 46aa785d1e29 src/HOLCF/Tools/pcpodef_package.ML --- a/src/HOLCF/Tools/pcpodef_package.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/HOLCF/Tools/pcpodef_package.ML Sat Mar 07 23:37:09 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 diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/General/binding.ML Sat Mar 07 23:37:09 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; diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Isar/class.ML Sat Mar 07 23:37:09 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) => diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Isar/class_target.ML Sat Mar 07 23:37:09 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'; diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Isar/constdefs.ML Sat Mar 07 23:37:09 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; diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Isar/expression.ML Sat Mar 07 23:37:09 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; diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sat Mar 07 23:37:09 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); diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Isar/isar_syn.ML Sat Mar 07 23:37:09 2009 +0100 @@ -86,7 +86,7 @@ val _ = OuterSyntax.command "classes" "declare type classes" K.thy_decl - (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\" || P.$$$ "<") |-- + (Scan.repeat1 (P.binding -- Scan.optional ((P.$$$ "\\" || 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.$$$ "\\" || P.$$$ "<") |-- + (P.binding -- Scan.optional ((P.$$$ "\\" || 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))); diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Isar/locale.ML Sat Mar 07 23:37:09 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 = diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Isar/object_logic.ML Sat Mar 07 23:37:09 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; diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Isar/outer_parse.ML Sat Mar 07 23:37:09 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); diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Isar/specification.ML Sat Mar 07 23:37:09 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]); diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Isar/theory_target.ML Sat Mar 07 23:37:09 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' []; diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Proof/extraction.ML Sat Mar 07 23:37:09 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 diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Sat Mar 07 23:37:09 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)), diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/Syntax/mixfix.ML Sat Mar 07 23:37:09 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), diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/axclass.ML Sat Mar 07 23:37:09 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 diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/drule.ML --- a/src/Pure/drule.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/drule.ML Sat Mar 07 23:37:09 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))); diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/meta_simplifier.ML Sat Mar 07 23:37:09 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)); diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/more_thm.ML Sat Mar 07 23:37:09 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); diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/pure_thy.ML Sat Mar 07 23:37:09 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\\_./ _)", [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; diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/sign.ML --- a/src/Pure/sign.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/sign.ML Sat Mar 07 23:37:09 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); diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/simplifier.ML Sat Mar 07 23:37:09 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; diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/theory.ML --- a/src/Pure/theory.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/theory.ML Sat Mar 07 23:37:09 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) *) diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/thm.ML --- a/src/Pure/thm.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/thm.ML Sat Mar 07 23:37:09 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)); diff -r d9ecd70b1112 -r 46aa785d1e29 src/Pure/type.ML --- a/src/Pure/type.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/Pure/type.ML Sat Mar 07 23:37:09 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 diff -r d9ecd70b1112 -r 46aa785d1e29 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/ZF/Tools/datatype_package.ML Sat Mar 07 23:37:09 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 => diff -r d9ecd70b1112 -r 46aa785d1e29 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/ZF/Tools/inductive_package.ML Sat Mar 07 23:37:09 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); diff -r d9ecd70b1112 -r 46aa785d1e29 src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Sat Mar 07 17:05:40 2009 +0100 +++ b/src/ZF/ind_syntax.ML Sat Mar 07 23:37:09 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;