Context.generic is canonical state of parsers;
removed obsolete global/local parsers;
tuned interfaces;
--- a/src/Pure/Isar/args.ML Fri Feb 10 02:22:39 2006 +0100
+++ b/src/Pure/Isar/args.ML Fri Feb 10 02:22:41 2006 +0100
@@ -69,31 +69,21 @@
val named_typ: (string -> typ) -> T list -> typ * T list
val named_term: (string -> term) -> T list -> term * T list
val named_fact: (string -> thm list) -> T list -> thm list * T list
- val global_typ_abbrev: theory * T list -> typ * (theory * T list)
- val global_typ: theory * T list -> typ * (theory * T list)
- val global_term: theory * T list -> term * (theory * T list)
- val global_prop: theory * T list -> term * (theory * T list)
- val local_typ_abbrev: ProofContext.context * T list -> typ * (ProofContext.context * T list)
- val local_typ: ProofContext.context * T list -> typ * (ProofContext.context * T list)
- val local_term: ProofContext.context * T list -> term * (ProofContext.context * T list)
- val local_prop: ProofContext.context * T list -> term * (ProofContext.context * T list)
val typ_abbrev: Context.generic * T list -> typ * (Context.generic * T list)
val typ: Context.generic * T list -> typ * (Context.generic * T list)
val term: Context.generic * T list -> term * (Context.generic * T list)
val prop: Context.generic * T list -> term * (Context.generic * T list)
- val global_tyname: theory * T list -> string * (theory * T list)
- val global_const: theory * T list -> string * (theory * T list)
- val local_tyname: ProofContext.context * T list -> string * (ProofContext.context * T list)
- val local_const: ProofContext.context * T list -> string * (ProofContext.context * T list)
val tyname: Context.generic * T list -> string * (Context.generic * T list)
val const: Context.generic * T list -> string * (Context.generic * T list)
val thm_sel: T list -> PureThy.interval list * T list
- val bang_facts: ProofContext.context * T list -> thm list * (ProofContext.context * T list)
+ val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
-> ((int -> tactic) -> tactic) * ('a * T list)
val attribs: (string -> string) -> T list -> src list * T list
val opt_attribs: (string -> string) -> T list -> src list * T list
- val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> src -> 'a -> 'a * 'b
+ val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'b * 'a
+ val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
+ src -> ProofContext.context -> ProofContext.context * 'a
val pretty_src: ProofContext.context -> src -> Pretty.T
val pretty_attribs: ProofContext.context -> src list -> Pretty.T list
end;
@@ -307,16 +297,6 @@
(* terms and types *)
-val global_typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o ProofContext.init);
-val global_typ = Scan.peek (named_typ o ProofContext.read_typ o ProofContext.init);
-val global_term = Scan.peek (named_term o ProofContext.read_term o ProofContext.init);
-val global_prop = Scan.peek (named_term o ProofContext.read_prop o ProofContext.init);
-
-val local_typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev);
-val local_typ = Scan.peek (named_typ o ProofContext.read_typ);
-val local_term = Scan.peek (named_term o ProofContext.read_term);
-val local_prop = Scan.peek (named_term o ProofContext.read_prop);
-
val typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o Context.proof_of);
val typ = Scan.peek (named_typ o ProofContext.read_typ o Context.proof_of);
val term = Scan.peek (named_term o ProofContext.read_term o Context.proof_of);
@@ -325,17 +305,11 @@
(* type and constant names *)
-val dest_tyname = fn Type (c, _) => c | TFree (a, _) => a | _ => "";
-val dest_const = fn Const (c, _) => c | Free (x, _) => x | _ => "";
+val tyname = Scan.peek (named_typ o Context.cases Sign.read_tyname ProofContext.read_tyname)
+ >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
-val global_tyname = Scan.peek (named_typ o Sign.read_tyname) >> dest_tyname;
-val global_const = Scan.peek (named_term o Sign.read_const) >> dest_const;
-val local_tyname = Scan.peek (named_typ o ProofContext.read_tyname) >> dest_tyname;
-val local_const = Scan.peek (named_term o ProofContext.read_const) >> dest_const;
-val tyname =
- Scan.peek (named_typ o Context.cases Sign.read_tyname ProofContext.read_tyname) >> dest_tyname;
-val const =
- Scan.peek (named_term o Context.cases Sign.read_const ProofContext.read_const) >> dest_const;
+val const = Scan.peek (named_term o Context.cases Sign.read_const ProofContext.read_const)
+ >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
(* misc *)
@@ -345,8 +319,8 @@
nat --| $$$ "-" >> PureThy.From ||
nat >> PureThy.Single));
-val bang_facts = Scan.peek (fn ctxt =>
- $$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []);
+val bang_facts = Scan.peek (fn context =>
+ $$$ "!" >> K (ProofContext.prems_of (Context.proof_of context)) || Scan.succeed []);
(* goal specification *)
@@ -404,6 +378,8 @@
error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n " ^
space_implode " " (map string_of args')));
+fun context_syntax kind scan src = apfst Context.the_proof o syntax kind scan src o Context.Proof;
+
(** pretty printing **)
--- a/src/Pure/Isar/attrib.ML Fri Feb 10 02:22:39 2006 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Feb 10 02:22:41 2006 +0100
@@ -27,15 +27,9 @@
(('c * 'att list) * ('d * 'att list) list) list
val crude_closure: Context.proof -> src -> src
val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
- val global_thm: theory * Args.T list -> thm * (theory * Args.T list)
- val global_thms: theory * Args.T list -> thm list * (theory * Args.T list)
- val global_thmss: theory * Args.T list -> thm list * (theory * Args.T list)
- val local_thm: Context.proof * Args.T list -> thm * (Context.proof * Args.T list)
- val local_thms: Context.proof * Args.T list -> thm list * (Context.proof * Args.T list)
- val local_thmss: Context.proof * Args.T list -> thm list * (Context.proof * Args.T list)
val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
- val thmss: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
+ val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
val syntax: (Context.generic * Args.T list ->
attribute * (Context.generic * Args.T list)) -> src -> attribute
val no_args: attribute -> src -> attribute
@@ -149,37 +143,28 @@
local
-fun gen_thm theory_of apply get pick = Scan.depend (fn st =>
- (Scan.ahead Args.alt_name -- Args.named_fact (get st o Fact)
+val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
+
+fun gen_thm pick = Scan.depend (fn st =>
+ (Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact)
>> (fn (s, fact) => ("", Fact s, fact)) ||
- Scan.ahead Args.name -- Args.named_fact (get st o Name) -- Args.thm_sel
+ Scan.ahead Args.name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel
>> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||
- Scan.ahead Args.name -- Args.named_fact (get st o Name)
+ Scan.ahead Args.name -- Args.named_fact (get_thms st o Name)
>> (fn (name, fact) => (name, Name name, fact))) --
- Args.opt_attribs (intern (theory_of st))
+ Args.opt_attribs (intern (Context.theory_of st))
>> (fn ((name, thmref, fact), srcs) =>
let
val ths = PureThy.select_thm thmref fact;
- val atts = map (attribute_i (theory_of st)) srcs;
- val (st', ths') = foldl_map (apply atts) (st, ths);
+ val atts = map (attribute_i (Context.theory_of st)) srcs;
+ val (st', ths') = foldl_map (Library.apply atts) (st, ths);
in (st', pick name ths') end));
-val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
-
in
-val global_thm = gen_thm I Thm.theory_attributes PureThy.get_thms PureThy.single_thm;
-val global_thms = gen_thm I Thm.theory_attributes PureThy.get_thms (K I);
-val global_thmss = Scan.repeat global_thms >> List.concat;
-
-val local_thm =
- gen_thm ProofContext.theory_of Thm.proof_attributes ProofContext.get_thms PureThy.single_thm;
-val local_thms = gen_thm ProofContext.theory_of Thm.proof_attributes ProofContext.get_thms (K I);
-val local_thmss = Scan.repeat local_thms >> List.concat;
-
-val thm = gen_thm Context.theory_of Library.apply get_thms PureThy.single_thm;
-val thms = gen_thm Context.theory_of Library.apply get_thms (K I);
-val thmss = Scan.repeat thms >> List.concat;
+val thm = gen_thm PureThy.single_thm;
+val multi_thm = gen_thm (K I);
+val thms = Scan.repeat multi_thm >> List.concat;
end;
@@ -217,7 +202,7 @@
>> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B))));
val OF_att =
- syntax (thmss >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)));
+ syntax (thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)));
(* read_instantiate: named instantiation of type and term variables *)
@@ -397,7 +382,7 @@
(* unfold / fold definitions *)
fun unfolded_syntax rule =
- syntax (thmss >>
+ syntax (thms >>
(fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths)));
val unfolded = unfolded_syntax LocalDefs.unfold;