accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
--- a/src/HOL/Tools/recdef_package.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML Fri Jun 17 18:35:27 2005 +0200
@@ -103,28 +103,27 @@
type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
-structure GlobalRecdefArgs =
-struct
+structure GlobalRecdefData = TheoryDataFun
+(struct
val name = "HOL/recdef";
type T = recdef_info Symtab.table * hints;
val empty = (Symtab.empty, mk_hints ([], [], [])): T;
val copy = I;
- val prep_ext = I;
- fun merge
+ val extend = I;
+ fun merge _
((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
- (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) =
+ (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
(Symtab.merge (K true) (tab1, tab2),
mk_hints (Drule.merge_rules (simps1, simps2),
Library.merge_alists congs1 congs2,
Drule.merge_rules (wfs1, wfs2)));
- fun print sg (tab, hints) =
- (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space sg, tab))) ::
+ fun print thy (tab, hints) =
+ (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space thy, tab))) ::
pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
-end;
+end);
-structure GlobalRecdefData = TheoryDataFun(GlobalRecdefArgs);
val print_recdefs = GlobalRecdefData.print;
@@ -143,15 +142,14 @@
(* proof data kind 'HOL/recdef' *)
-structure LocalRecdefArgs =
-struct
+structure LocalRecdefData = ProofDataFun
+(struct
val name = "HOL/recdef";
type T = hints;
val init = get_global_hints;
fun print _ hints = pretty_hints hints |> Pretty.chunks |> Pretty.writeln;
-end;
+end);
-structure LocalRecdefData = ProofDataFun(LocalRecdefArgs);
val get_local_hints = LocalRecdefData.get;
val map_local_hints = LocalRecdefData.map;
@@ -234,7 +232,7 @@
let
val _ = requires_recdef thy;
- val name = Sign.intern_const (Theory.sign_of thy) raw_name;
+ val name = Sign.intern_const thy raw_name;
val bname = Sign.base_name name;
val _ = message ("Defining recursive function " ^ quote name ^ " ...");
@@ -282,7 +280,7 @@
fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
let
- val name = Sign.intern_const (Theory.sign_of thy) raw_name;
+ val name = Sign.intern_const thy raw_name;
val bname = Sign.base_name name;
val _ = requires_recdef thy;
@@ -306,7 +304,7 @@
fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i int thy =
let
- val name = prep_name (Theory.sign_of thy) raw_name;
+ val name = prep_name thy raw_name;
val atts = map (prep_att thy) raw_atts;
val tcs =
(case get_recdef thy name of
@@ -380,6 +378,4 @@
end;
-
end;
-
--- a/src/HOL/Tools/record_package.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/HOL/Tools/record_package.ML Fri Jun 17 18:35:27 2005 +0200
@@ -29,16 +29,16 @@
val ext_typeN: string
val last_extT: typ -> (string * typ list) option
val dest_recTs : typ -> (string * typ list) list
- val get_extT_fields: Sign.sg -> typ -> ((string * typ) list * (string * typ))
- val get_recT_fields: Sign.sg -> typ -> ((string * typ) list * (string * typ))
- val get_extension: Sign.sg -> Symtab.key -> (string * typ list) option
- val get_extinjects: Sign.sg -> thm list
- val get_simpset: Sign.sg -> simpset
+ val get_extT_fields: theory -> typ -> ((string * typ) list * (string * typ))
+ val get_recT_fields: theory -> typ -> ((string * typ) list * (string * typ))
+ val get_extension: theory -> Symtab.key -> (string * typ list) option
+ val get_extinjects: theory -> thm list
+ val get_simpset: theory -> simpset
val print_records: theory -> unit
- val add_record: string list * string -> string option -> (string * string * mixfix) list
- -> theory -> theory
- val add_record_i: string list * string -> (typ list * string) option
- -> (string * typ * mixfix) list -> theory -> theory
+ val add_record: string list * string -> string option -> (string * string * mixfix) list
+ -> theory -> theory
+ val add_record_i: string list * string -> (typ list * string) option
+ -> (string * typ * mixfix) list -> theory -> theory
val setup: (theory -> theory) list
end;
@@ -235,8 +235,8 @@
equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
extfields = extfields, fieldext = fieldext }: record_data;
-structure RecordsArgs =
-struct
+structure RecordsData = TheoryDataFun
+(struct
val name = "HOL/records";
type T = record_data;
@@ -246,8 +246,8 @@
Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
val copy = I;
- val prep_ext = I;
- fun merge
+ val extend = I;
+ fun merge _
({records = recs1,
sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
equalities = equalities1,
@@ -296,11 +296,11 @@
[prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
pretty_parent parent @ map pretty_field fields));
in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
-end;
+end);
-structure RecordsData = TheoryDataFun(RecordsArgs);
val print_records = RecordsData.print;
+
(* access 'records' *)
fun get_record thy name = Symtab.lookup (#records (RecordsData.get thy), name);
@@ -315,7 +315,7 @@
(* access 'sel_upd' *)
-fun get_sel_upd sg = #sel_upd (RecordsData.get_sg sg);
+val get_sel_upd = #sel_upd o RecordsData.get;
fun get_selectors sg name = Symtab.lookup (#selectors (get_sel_upd sg), name);
fun is_selector sg name =
@@ -353,7 +353,7 @@
in RecordsData.put data thy end;
fun get_equalities sg name =
- Symtab.lookup (#equalities (RecordsData.get_sg sg), name);
+ Symtab.lookup (#equalities (RecordsData.get sg), name);
(* access 'extinjects' *)
@@ -365,7 +365,7 @@
splits extfields fieldext;
in RecordsData.put data thy end;
-fun get_extinjects sg = #extinjects (RecordsData.get_sg sg);
+fun get_extinjects sg = #extinjects (RecordsData.get sg);
(* access 'extsplit' *)
@@ -379,7 +379,7 @@
in RecordsData.put data thy end;
fun get_extsplit sg name =
- Symtab.lookup (#extsplit (RecordsData.get_sg sg), name);
+ Symtab.lookup (#extsplit (RecordsData.get sg), name);
(* access 'splits' *)
@@ -393,13 +393,13 @@
in RecordsData.put data thy end;
fun get_splits sg name =
- Symtab.lookup (#splits (RecordsData.get_sg sg), name);
+ Symtab.lookup (#splits (RecordsData.get sg), name);
(* extension of a record name *)
fun get_extension sg name =
- case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
+ case Symtab.lookup (#records (RecordsData.get sg),name) of
SOME s => SOME (#extension s)
| NONE => NONE;
@@ -415,7 +415,7 @@
in RecordsData.put data thy end;
fun get_extfields sg name =
- Symtab.lookup (#extfields (RecordsData.get_sg sg), name);
+ Symtab.lookup (#extfields (RecordsData.get sg), name);
fun get_extT_fields sg T =
let
@@ -425,7 +425,7 @@
val midx = maxidx_of_typs (moreT::Ts);
fun varify (a, S) = TVar ((a, midx), S);
val varifyT = map_type_tfree varify;
- val {records,extfields,...} = RecordsData.get_sg sg;
+ val {records,extfields,...} = RecordsData.get sg;
val (flds,(more,_)) = split_last (Symtab.lookup_multi (extfields,name));
val args = map varifyT (snd (#extension (valOf (Symtab.lookup (records,recname)))));
@@ -458,7 +458,7 @@
fun get_fieldext sg name =
- Symtab.lookup (#fieldext (RecordsData.get_sg sg), name);
+ Symtab.lookup (#fieldext (RecordsData.get sg), name);
(* parent records *)
@@ -841,7 +841,7 @@
fun prove_split_simp sg T prop =
let
- val {sel_upd={simpset,...},extsplit,...} = RecordsData.get_sg sg;
+ val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg;
val extsplits =
Library.foldl (fn (thms,(n,_)) => (list (Symtab.lookup (extsplit,n)))@thms)
([],dest_recTs T);
@@ -880,7 +880,7 @@
(case get_updates sg u of SOME u_name =>
let
fun mk_abs_var x t = (x, fastype_of t);
- val {sel_upd={updates,...},extfields,...} = RecordsData.get_sg sg;
+ val {sel_upd={updates,...},extfields,...} = RecordsData.get sg;
fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
(case (Symtab.lookup (updates,u)) of
@@ -938,7 +938,7 @@
(fn sg => fn _ => fn t =>
(case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) =>
let datatype ('a,'b) calc = Init of 'b | Inter of 'a
- val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get_sg sg;
+ val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg;
fun mk_abs_var x t = (x, fastype_of t);
fun sel_name u = NameSpace.base (unsuffix updateN u);
@@ -1142,7 +1142,7 @@
let
val sg = Thm.sign_of_thm st;
val {sel_upd={simpset,...},...}
- = RecordsData.get_sg sg;
+ = RecordsData.get sg;
val has_rec = exists_Const
(fn (s, Type (_, [Type (_, [T, _]), _])) =>
--- a/src/HOL/Tools/typedef_package.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/HOL/Tools/typedef_package.ML Fri Jun 17 18:35:27 2005 +0200
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/typedef_package.ML
ID: $Id$
- Author: Markus Wenzel, TU Muenchen
+ Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Gordon/HOL-style type definitions.
*)
@@ -50,18 +50,16 @@
(** theory data **)
-structure TypedefArgs =
-struct
+structure TypedefData = TheoryDataFun
+(struct
val name = "HOL/typedef";
type T = (typ * typ * string * string) Symtab.table;
val empty = Symtab.empty;
val copy = I;
- val prep_ext = I;
- val merge : T * T -> T = Symtab.merge op =;
- fun print sg _ = ();
-end;
-
-structure TypedefData = TheoryDataFun(TypedefArgs);
+ val extend = I;
+ fun merge _ (tabs: T * T) = Symtab.merge (op =) tabs;
+ fun print _ _ = ();
+end);
fun put_typedef newT oldT Abs_name Rep_name thy =
TypedefData.put (Symtab.update_new
@@ -74,16 +72,14 @@
fun add_typedecls decls thy =
let
- val full = Sign.full_name (Theory.sign_of thy);
-
fun arity_of (raw_name, args, mx) =
- (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.typeS, HOLogic.typeS);
+ (Sign.full_name thy (Syntax.type_name raw_name mx),
+ replicate (length args) HOLogic.typeS, HOLogic.typeS);
in
if can (Theory.assert_super HOL.thy) thy then
- thy
- |> PureThy.add_typedecls decls
+ thy |> Theory.add_typedecls decls
|> Theory.add_arities_i (map arity_of decls)
- else thy |> PureThy.add_typedecls decls
+ else thy |> Theory.add_typedecls decls
end;
@@ -109,16 +105,17 @@
getOpt (witn2_tac, TRY (ALLGOALS (CLASET' blast_tac)));
in
message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
- Tactic.prove (Theory.sign_of thy) [] [] goal (K tac)
- end handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
+ Tactic.prove thy [] [] goal (K tac)
+ end
+ handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
(* prepare_typedef *)
-fun read_term sg used s =
- #1 (Thm.read_def_cterm (sg, K NONE, K NONE) used true (s, HOLogic.typeT));
+fun read_term thy used s =
+ #1 (Thm.read_def_cterm (thy, K NONE, K NONE) used true (s, HOLogic.typeT));
-fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
+fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg;
fun err_in_typedef name =
error ("The error(s) above occurred in typedef " ^ quote name);
@@ -126,16 +123,15 @@
fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
let
val _ = Theory.requires thy "Typedef" "typedefs";
- val sign = Theory.sign_of thy;
- val full = Sign.full_name sign;
+ val full = Sign.full_name thy;
(*rhs*)
val full_name = full name;
- val cset = prep_term sign vs raw_set;
+ val cset = prep_term thy vs raw_set;
val {T = setT, t = set, ...} = Thm.rep_cterm cset;
val rhs_tfrees = term_tfrees set;
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
- error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT));
+ error ("Not a set type: " ^ quote (Sign.string_of_typ thy setT));
fun mk_nonempty A =
HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
val goal = mk_nonempty set;
@@ -283,7 +279,7 @@
val (gr', _) = Codegen.invoke_tycodegen thy dep false (gr, T);
val (gr'', ps) =
foldl_map (Codegen.invoke_codegen thy dep true) (gr', ts);
- val id = Codegen.mk_const_id (sign_of thy) s
+ val id = Codegen.mk_const_id thy s
in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
fun get_name (Type (tname, _)) = tname
| get_name _ = "";
@@ -312,10 +308,9 @@
| SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
if isSome (Codegen.get_assoc_type thy tname) then NONE else
let
- val sg = sign_of thy;
- val Abs_id = Codegen.mk_const_id sg Abs_name;
- val Rep_id = Codegen.mk_const_id sg Rep_name;
- val ty_id = Codegen.mk_type_id sg s;
+ val Abs_id = Codegen.mk_const_id thy Abs_name;
+ val Rep_id = Codegen.mk_const_id thy Rep_name;
+ val ty_id = Codegen.mk_type_id thy s;
val (gr', qs) = foldl_map
(Codegen.invoke_tycodegen thy dep (length Ts = 1)) (gr, Ts);
val gr'' = Graph.add_edge (Abs_id, dep) gr' handle Graph.UNDEF _ =>
@@ -334,21 +329,21 @@
Pretty.str "x) = x;"]) ^ "\n\n" ^
(if "term_of" mem !Codegen.mode then
Pretty.string_of (Pretty.block [Pretty.str "fun ",
- Codegen.mk_term_of sg false newT, Pretty.brk 1,
+ Codegen.mk_term_of thy false newT, Pretty.brk 1,
Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
Pretty.str "x) =", Pretty.brk 1,
Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
- Codegen.mk_term_of sg false oldT, Pretty.brk 1,
+ Codegen.mk_term_of thy false oldT, Pretty.brk 1,
Pretty.str "x;"]) ^ "\n\n"
else "") ^
(if "test" mem !Codegen.mode then
Pretty.string_of (Pretty.block [Pretty.str "fun ",
- Codegen.mk_gen sg false [] "" newT, Pretty.brk 1,
+ Codegen.mk_gen thy false [] "" newT, Pretty.brk 1,
Pretty.str "i =", Pretty.brk 1,
Pretty.block [Pretty.str (Abs_id ^ " ("),
- Codegen.mk_gen sg false [] "" oldT, Pretty.brk 1,
+ Codegen.mk_gen thy false [] "" oldT, Pretty.brk 1,
Pretty.str "i);"]]) ^ "\n\n"
else "")
in Graph.map_node Abs_id (K (NONE, s)) gr'' end
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Jun 17 18:35:27 2005 +0200
@@ -11,7 +11,7 @@
and a simplification procedure
- lin_arith_prover: Sign.sg -> simpset -> term -> thm option
+ lin_arith_prover: theory -> simpset -> term -> thm option
Only take premises and conclusions into account that are already (negated)
(in)equations. lin_arith_prover tries to prove or disprove the term.
@@ -34,7 +34,7 @@
val neg_prop: term -> term
val is_False: thm -> bool
val is_nat: typ list * term -> bool
- val mk_nat_thm: Sign.sg -> term -> thm
+ val mk_nat_thm: theory -> term -> thm
end;
(*
mk_Eq(~in) = `in == False'
@@ -52,7 +52,7 @@
signature LIN_ARITH_DATA =
sig
val decomp:
- Sign.sg -> term -> ((term*rat)list * rat * string * (term*rat)list * rat * bool)option
+ theory -> term -> ((term*rat)list * rat * string * (term*rat)list * rat * bool)option
val number_of: IntInf.int * typ -> term
end;
(*
@@ -77,7 +77,7 @@
-> theory -> theory
val trace : bool ref
val fast_arith_neq_limit: int ref
- val lin_arith_prover: Sign.sg -> simpset -> term -> thm option
+ val lin_arith_prover: theory -> simpset -> term -> thm option
val lin_arith_tac: bool -> int -> tactic
val cut_lin_arith_tac: thm list -> int -> tactic
end;
@@ -91,8 +91,8 @@
(* data kind 'Provers/fast_lin_arith' *)
-structure DataArgs =
-struct
+structure Data = TheoryDataFun
+(struct
val name = "Provers/fast_lin_arith";
type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset};
@@ -100,12 +100,13 @@
val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
lessD = [], neqE = [], simpset = Simplifier.empty_ss};
val copy = I;
- val prep_ext = I;
+ val extend = I;
- fun merge ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
- lessD = lessD1, neqE=neqE1, simpset = simpset1},
- {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
- lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
+ fun merge _
+ ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
+ lessD = lessD1, neqE=neqE1, simpset = simpset1},
+ {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
+ lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
{add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2),
inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
@@ -114,9 +115,8 @@
simpset = Simplifier.merge_ss (simpset1, simpset2)};
fun print _ _ = ();
-end;
+end);
-structure Data = TheoryDataFun(DataArgs);
val map_data = Data.map;
val setup = [Data.init];
@@ -420,7 +420,7 @@
in
fun mkthm sg asms just =
let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
- Data.get_sg sg;
+ Data.get sg;
val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
map fst lhs union (map fst rhs union ats))
([], List.mapPartial (fn thm => if Thm.no_prems thm
@@ -625,7 +625,7 @@
fun refute_tac(i,justs) =
fn state =>
let val sg = #sign(rep_thm state)
- val {neqE, ...} = Data.get_sg sg;
+ val {neqE, ...} = Data.get sg;
fun just1 j = REPEAT_DETERM(eresolve_tac neqE i) THEN
METAHYPS (fn asms => rtac (mkthm sg asms j) 1) i
in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN
@@ -691,7 +691,7 @@
in (ct1,ct2) end;
fun splitasms sg asms =
-let val {neqE, ...} = Data.get_sg sg;
+let val {neqE, ...} = Data.get sg;
fun split(asms',[]) = Tip(rev asms')
| split(asms',asm::asms) =
(case get_first (fn th => SOME(asm COMP th) handle THM _ => NONE) neqE
--- a/src/Pure/Isar/attrib.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Jun 17 18:35:27 2005 +0200
@@ -8,8 +8,9 @@
signature BASIC_ATTRIB =
sig
val print_attributes: theory -> unit
- val Attribute: bstring -> (Args.src -> theory attribute) * (Args.src -> ProofContext.context attribute)
- -> string -> unit
+ val Attribute: bstring ->
+ (Args.src -> theory attribute) * (Args.src -> ProofContext.context attribute) ->
+ string -> unit
end;
signature ATTRIB =
@@ -17,8 +18,8 @@
include BASIC_ATTRIB
type src
exception ATTRIB_FAIL of (string * Position.T) * exn
- val intern: Sign.sg -> xstring -> string
- val intern_src: Sign.sg -> src -> src
+ val intern: theory -> xstring -> string
+ val intern_src: theory -> src -> src
val global_attribute_i: theory -> src -> theory attribute
val global_attribute: theory -> src -> theory attribute
val local_attribute_i: theory -> src -> ProofContext.context attribute
@@ -33,9 +34,12 @@
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: ProofContext.context * Args.T list -> thm * (ProofContext.context * Args.T list)
- val local_thms: ProofContext.context * Args.T list -> thm list * (ProofContext.context * Args.T list)
- val local_thmss: ProofContext.context * Args.T list -> thm list * (ProofContext.context * Args.T list)
+ val local_thm: ProofContext.context * Args.T list ->
+ thm * (ProofContext.context * Args.T list)
+ val local_thms: ProofContext.context * Args.T list ->
+ thm list * (ProofContext.context * Args.T list)
+ val local_thmss: ProofContext.context * Args.T list ->
+ thm list * (ProofContext.context * Args.T list)
val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> src -> 'a attribute
val no_args: 'a attribute -> src -> 'a attribute
val add_del_args: 'a attribute -> 'a attribute -> src -> 'a attribute
@@ -50,10 +54,10 @@
(** attributes theory data **)
-(* data kind 'Isar/attributes' *)
+(* datatype attributes *)
-structure AttributesDataArgs =
-struct
+structure AttributesData = TheoryDataFun
+(struct
val name = "Isar/attributes";
type T =
((((src -> theory attribute) * (src -> ProofContext.context attribute))
@@ -61,9 +65,9 @@
val empty = NameSpace.empty_table;
val copy = I;
- val prep_ext = I;
+ val extend = I;
- fun merge tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
+ fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
fun print _ attribs =
@@ -74,16 +78,15 @@
[Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
|> Pretty.chunks |> Pretty.writeln
end;
-end;
+end);
-structure AttributesData = TheoryDataFun(AttributesDataArgs);
val _ = Context.add_setup [AttributesData.init];
val print_attributes = AttributesData.print;
(* interning *)
-val intern = NameSpace.intern o #1 o AttributesData.get_sg;
+val intern = NameSpace.intern o #1 o AttributesData.get;
val intern_src = Args.map_name o intern;
@@ -103,10 +106,10 @@
in attr end;
val global_attribute_i = gen_attribute fst;
-fun global_attribute thy = global_attribute_i thy o intern_src (Theory.sign_of thy);
+fun global_attribute thy = global_attribute_i thy o intern_src thy;
val local_attribute_i = gen_attribute snd;
-fun local_attribute thy = local_attribute_i thy o intern_src (Theory.sign_of thy);
+fun local_attribute thy = local_attribute_i thy o intern_src thy;
val context_attribute_i = local_attribute_i o ProofContext.theory_of;
val context_attribute = local_attribute o ProofContext.theory_of;
@@ -133,10 +136,9 @@
fun add_attributes raw_attrs thy =
let
- val sg = Theory.sign_of thy;
val new_attrs = raw_attrs |> map (fn (name, (f, g), comment) =>
(name, (((f, g), comment), stamp ())));
- fun add attrs = NameSpace.extend_table (Sign.naming_of sg) (attrs, new_attrs)
+ fun add attrs = NameSpace.extend_table (Sign.naming_of thy) (attrs, new_attrs)
handle Symtab.DUPS dups =>
error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
in AttributesData.map add thy end;
@@ -157,7 +159,7 @@
fun gen_thm theory_of attrib get pick = Scan.depend (fn st =>
Scan.ahead Args.name -- Args.named_fact (fn name => get st (name, NONE)) --
- Scan.option Args.thm_sel -- Args.opt_attribs (intern (Theory.sign_of (theory_of st)))
+ Scan.option Args.thm_sel -- Args.opt_attribs (intern (theory_of st))
>> (fn (((name, fact), sel), srcs) =>
let
val ths = PureThy.select_thm (name, sel) fact;
@@ -238,24 +240,24 @@
fun the_type types xi = the (types xi)
handle Option.Option => error_var "No such variable in theorem: " xi;
-fun unify_types sign types ((unifier, maxidx), (xi, u)) =
+fun unify_types thy types ((unifier, maxidx), (xi, u)) =
let
val T = the_type types xi;
val U = Term.fastype_of u;
val maxidx' = Int.max (maxidx, Int.max (#2 xi, Term.maxidx_of_term u));
in
- Type.unify (Sign.tsig_of sign) (unifier, maxidx') (T, U)
+ Type.unify (Sign.tsig_of thy) (unifier, maxidx') (T, U)
handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
end;
fun typ_subst env = apsnd (Term.typ_subst_TVars env);
fun subst env = apsnd (Term.subst_TVars env);
-fun instantiate sign envT env thm =
+fun instantiate thy envT env thm =
let
val (_, sorts) = Drule.types_sorts thm;
- fun prepT (a, T) = (Thm.ctyp_of sign (TVar (a, the_sort sorts a)), Thm.ctyp_of sign T);
- fun prep (xi, t) = pairself (Thm.cterm_of sign) (Var (xi, Term.fastype_of t), t);
+ fun prepT (a, T) = (Thm.ctyp_of thy (TVar (a, the_sort sorts a)), Thm.ctyp_of thy T);
+ fun prep (xi, t) = pairself (Thm.cterm_of thy) (Var (xi, Term.fastype_of t), t);
in
Drule.instantiate (map prepT (distinct envT),
map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
@@ -266,7 +268,7 @@
fun read_instantiate init mixed_insts (context, thm) =
let
val ctxt = init context;
- val sign = ProofContext.sign_of ctxt;
+ val thy = ProofContext.theory_of ctxt;
val (type_insts, term_insts) = List.partition (is_tvar o #1) (map #2 mixed_insts);
val internal_insts = term_insts |> List.mapPartial
@@ -290,23 +292,23 @@
| Args.Typ T => T
| _ => error_var "Type argument expected for " xi);
in
- if Sign.of_sort sign (T, S) then (xi, T)
+ if Sign.of_sort thy (T, S) then (xi, T)
else error_var "Incompatible sort for typ instantiation of " xi
end;
val type_insts' = map readT type_insts;
- val thm' = instantiate sign type_insts' [] thm;
+ val thm' = instantiate thy type_insts' [] thm;
(* internal term instantiations *)
val types' = #1 (Drule.types_sorts thm');
val unifier = map (apsnd snd) (Vartab.dest (#1
- (Library.foldl (unify_types sign types') ((Vartab.empty, 0), internal_insts))));
+ (Library.foldl (unify_types thy types') ((Vartab.empty, 0), internal_insts))));
val type_insts'' = map (typ_subst unifier) type_insts';
val internal_insts'' = map (subst unifier) internal_insts;
- val thm'' = instantiate sign unifier internal_insts'' thm';
+ val thm'' = instantiate thy unifier internal_insts'' thm';
(* external term instantiations *)
@@ -323,7 +325,7 @@
val external_insts''' = xs ~~ ts;
val term_insts''' = internal_insts''' @ external_insts''';
- val thm''' = instantiate sign inferred external_insts''' thm'';
+ val thm''' = instantiate thy inferred external_insts''' thm'';
in
(* assign internalized values *)
--- a/src/Pure/Isar/locale.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Pure/Isar/locale.ML Fri Jun 17 18:35:27 2005 +0200
@@ -44,8 +44,8 @@
type element
type element_i
type locale
- val intern: Sign.sg -> xstring -> string
- val extern: Sign.sg -> string -> xstring
+ val intern: theory -> xstring -> string
+ val extern: theory -> string -> xstring
val the_locale: theory -> string -> locale
val intern_attrib_elem: theory ->
('typ, 'term, 'fact) elem -> ('typ, 'term, 'fact) elem
@@ -161,11 +161,11 @@
then t
else Term.map_term_types (tinst_tab_type tinst) t;
-fun tinst_tab_thm sg tinst thm = if Symtab.is_empty tinst
+fun tinst_tab_thm thy tinst thm = if Symtab.is_empty tinst
then thm
else let
- val cert = Thm.cterm_of sg;
- val certT = Thm.ctyp_of sg;
+ val cert = Thm.cterm_of thy;
+ val certT = Thm.ctyp_of thy;
val {hyps, prop, ...} = Thm.rep_thm thm;
val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
val tinst' = Symtab.dest tinst |>
@@ -198,11 +198,11 @@
| instf (s $ t) = instf s $ instf t
in instf end;
-fun inst_tab_thm sg (inst, tinst) thm = if Symtab.is_empty inst
- then tinst_tab_thm sg tinst thm
+fun inst_tab_thm thy (inst, tinst) thm = if Symtab.is_empty inst
+ then tinst_tab_thm thy tinst thm
else let
- val cert = Thm.cterm_of sg;
- val certT = Thm.ctyp_of sg;
+ val cert = Thm.cterm_of thy;
+ val certT = Thm.ctyp_of thy;
val {hyps, prop, ...} = Thm.rep_thm thm;
(* type instantiations *)
val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
@@ -218,7 +218,7 @@
if a = x then SOME (Free (x, tinst_tab_type tinst T), t)
else NONE) frees);
in
- if null tinst' andalso null inst' then tinst_tab_thm sg tinst thm
+ if null tinst' andalso null inst' then tinst_tab_thm thy tinst thm
else thm |> Drule.implies_intr_list (map cert hyps)
|> Drule.tvars_intr_list (map #1 tinst')
|> (fn (th, al) => th |> Thm.instantiate
@@ -239,9 +239,9 @@
val empty: T
val join: T * T -> T
val dest: T -> (term list * ((string * Attrib.src list) * thm list)) list
- val lookup: Sign.sg -> T * term list ->
+ val lookup: theory -> T * term list ->
((string * Attrib.src list) * thm list) option
- val insert: Sign.sg -> term list * (string * Attrib.src list) -> T ->
+ val insert: theory -> term list * (string * Attrib.src list) -> T ->
T * (term list * ((string * Attrib.src list) * thm list)) list
val add_witness: term list -> thm -> T -> T
end =
@@ -262,7 +262,7 @@
(* joining of registrations: prefix and attributs of left theory,
thms are equal, no attempt to subsumption testing *)
- fun join (r1, r2) = Termtab.join (fn (reg, _) => SOME reg) (r1, r2);
+ fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => SOME reg) (r1, r2);
fun dest regs = map (apfst untermify) (Termtab.dest regs);
@@ -321,8 +321,8 @@
(** theory data **)
-structure GlobalLocalesArgs =
-struct
+structure GlobalLocalesData = TheoryDataFun
+(struct
val name = "Isar/locales";
type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
(* 1st entry: locale namespace,
@@ -331,39 +331,37 @@
val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
val copy = I;
- val prep_ext = I;
+ val extend = I;
- fun join_locs ({predicate, import, elems, params}: locale,
+ fun join_locs _ ({predicate, import, elems, params}: locale,
{elems = elems', ...}: locale) =
SOME {predicate = predicate, import = import,
elems = gen_merge_lists eq_snd elems elems',
params = params};
- fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) =
+ fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
(NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
- Symtab.join (SOME o Registrations.join) (regs1, regs2));
+ Symtab.join (K (SOME o Registrations.join)) (regs1, regs2));
fun print _ (space, locs, _) =
Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
|> Pretty.writeln;
-end;
+end);
-structure GlobalLocalesData = TheoryDataFun(GlobalLocalesArgs);
val _ = Context.add_setup [GlobalLocalesData.init];
(** context data **)
-structure LocalLocalesArgs =
-struct
+structure LocalLocalesData = ProofDataFun
+(struct
val name = "Isar/locales";
type T = Registrations.T Symtab.table;
(* registrations, indexed by locale name *)
fun init _ = Symtab.empty;
fun print _ _ = ();
-end;
+end);
-structure LocalLocalesData = ProofDataFun(LocalLocalesArgs);
val _ = Context.add_setup [LocalLocalesData.init];
@@ -371,12 +369,12 @@
val print_locales = GlobalLocalesData.print;
-val intern = NameSpace.intern o #1 o GlobalLocalesData.get_sg;
-val extern = NameSpace.extern o #1 o GlobalLocalesData.get_sg;
+val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
+val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
fun declare_locale name thy =
thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
- (Sign.declare_name (Theory.sign_of thy) name space, locs, regs));
+ (Sign.declare_name thy name space, locs, regs));
fun put_locale name loc =
GlobalLocalesData.map (fn (space, locs, regs) =>
@@ -408,15 +406,15 @@
val get_local_registrations =
gen_get_registrations LocalLocalesData.get;
-fun gen_get_registration get get_sg thy_ctxt (name, ps) =
+fun gen_get_registration get thy_of thy_ctxt (name, ps) =
case Symtab.lookup (get thy_ctxt, name) of
NONE => NONE
- | SOME reg => Registrations.lookup (get_sg thy_ctxt) (reg, ps);
+ | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
val get_global_registration =
- gen_get_registration (#3 o GlobalLocalesData.get) Theory.sign_of;
+ gen_get_registration (#3 o GlobalLocalesData.get) I;
val get_local_registration =
- gen_get_registration LocalLocalesData.get ProofContext.sign_of;
+ gen_get_registration LocalLocalesData.get ProofContext.theory_of;
val test_global_registration = isSome oo get_global_registration;
val test_local_registration = isSome oo get_local_registration;
@@ -430,15 +428,15 @@
(* add registration to theory or context, ignored if subsumed *)
-fun gen_put_registration map_data get_sg (name, ps) attn thy_ctxt =
+fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
map_data (fn regs =>
let
- val sg = get_sg thy_ctxt;
+ val thy = thy_of thy_ctxt;
val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty);
- val (reg', sups) = Registrations.insert sg (ps, attn) reg;
+ val (reg', sups) = Registrations.insert thy (ps, attn) reg;
val _ = if not (null sups) then warning
("Subsumed interpretation(s) of locale " ^
- quote (extern sg name) ^
+ quote (extern thy name) ^
"\nby interpretation(s) with the following prefix(es):\n" ^
commas_quote (map (fn (_, ((s, _), _)) => s) sups))
else ();
@@ -446,10 +444,9 @@
val put_global_registration =
gen_put_registration (fn f =>
- GlobalLocalesData.map (fn (space, locs, regs) =>
- (space, locs, f regs))) Theory.sign_of;
+ GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
val put_local_registration =
- gen_put_registration LocalLocalesData.map ProofContext.sign_of;
+ gen_put_registration LocalLocalesData.map ProofContext.theory_of;
(* TODO: needed? *)
(*
@@ -487,7 +484,6 @@
fun imports thy (upper, lower) =
let
- val sign = sign_of thy;
fun imps (Locale name) low = (name = low) orelse
(case get_locale thy name of
NONE => false
@@ -495,7 +491,7 @@
| imps (Rename (expr, _)) low = imps expr low
| imps (Merge es) low = exists (fn e => imps e low) es;
in
- imps (Locale (intern sign upper)) (intern sign lower)
+ imps (Locale (intern thy upper)) (intern thy lower)
end;
@@ -505,7 +501,6 @@
let
val ctxt = mk_ctxt thy_ctxt;
val thy = ProofContext.theory_of ctxt;
- val sg = Theory.sign_of thy;
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
val prt_atts = Args.pretty_attribs ctxt;
@@ -517,7 +512,7 @@
[Pretty.str ":", Pretty.brk 1,
Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts))]));
- val loc_int = intern sg loc;
+ val loc_int = intern thy loc;
val regs = get_regs thy_ctxt;
val loc_regs = Symtab.lookup (regs, loc_int);
in
@@ -547,9 +542,9 @@
fun err_in_locale ctxt msg ids =
let
- val sign = ProofContext.sign_of ctxt;
+ val thy = ProofContext.theory_of ctxt;
fun prt_id (name, parms) =
- [Pretty.block (Pretty.breaks (map Pretty.str (extern sign name :: parms)))];
+ [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
val err_msg =
if forall (equal "" o #1) ids then msg
@@ -591,7 +586,7 @@
fun map_attrib_elem f = map_elem {name = I, var = I, typ = I, term = I, fact = I, attrib = f};
-fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src (Theory.sign_of thy));
+fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src thy);
fun intern_attrib_elem_expr thy (Elem elem) = Elem (intern_attrib_elem thy elem)
| intern_attrib_elem_expr _ (Expr expr) = Expr expr;
@@ -623,8 +618,8 @@
fun rename_thm ren th =
let
- val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th;
- val cert = Thm.cterm_of sign;
+ val {thy, hyps, prop, maxidx, ...} = Thm.rep_thm th;
+ val cert = Thm.cterm_of thy;
val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps));
val xs' = map (rename ren) xs;
fun cert_frees names = map (cert o Free) (names ~~ Ts);
@@ -659,9 +654,9 @@
fun inst_thm _ [] th = th
| inst_thm ctxt env th =
let
- val sign = ProofContext.sign_of ctxt;
- val cert = Thm.cterm_of sign;
- val certT = Thm.ctyp_of sign;
+ val thy = ProofContext.theory_of ctxt;
+ val cert = Thm.cterm_of thy;
+ val certT = Thm.ctyp_of thy;
val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env;
@@ -686,16 +681,16 @@
(* instantiate TFrees *)
-fun tinst_tab_elem sg tinst =
- map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm sg tinst);
+fun tinst_tab_elem thy tinst =
+ map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm thy tinst);
(* instantiate TFrees and Frees *)
-fun inst_tab_elem sg (inst as (_, tinst)) =
- map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm sg inst);
+fun inst_tab_elem thy (inst as (_, tinst)) =
+ map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm thy inst);
-fun inst_tab_elems sign inst ((n, ps), elems) =
- ((n, map (inst_tab_term inst) ps), map (inst_tab_elem sign inst) elems);
+fun inst_tab_elems thy inst ((n, ps), elems) =
+ ((n, map (inst_tab_term inst) ps), map (inst_tab_elem thy inst) elems);
(** structured contexts: rename + merge + implicit type instantiation **)
@@ -719,7 +714,7 @@
val (maxidx', Ts') = foldl_map paramify (maxidx, Ts);
val (maxidx'', Us') = foldl_map paramify (maxidx', Us);
- val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
+ val tsig = Sign.tsig_of (ProofContext.theory_of ctxt);
fun unify (env, (SOME T, SOME U)) = (Type.unify tsig env (U, T)
handle Type.TUNIFY =>
@@ -771,8 +766,8 @@
fun unify_parms ctxt (fixed_parms : (string * typ) list)
(raw_parmss : (string * typ option) list list) =
let
- val sign = ProofContext.sign_of ctxt;
- val tsig = Sign.tsig_of sign;
+ val thy = ProofContext.theory_of ctxt;
+ val tsig = Sign.tsig_of thy;
val maxidx = length raw_parmss;
val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
@@ -783,7 +778,7 @@
fun unify T ((env, maxidx), U) =
Type.unify tsig (env, maxidx) (U, T)
handle Type.TUNIFY =>
- let val prt = Sign.string_of_typ sign
+ let val prt = Sign.string_of_typ thy
in raise TYPE ("unify_parms: failed to unify types " ^
prt U ^ " and " ^ prt T, [U, T], [])
end
@@ -1065,9 +1060,9 @@
(* expressions *)
-fun intern_expr sg (Locale xname) = Locale (intern sg xname)
- | intern_expr sg (Merge exprs) = Merge (map (intern_expr sg) exprs)
- | intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs);
+fun intern_expr thy (Locale xname) = Locale (intern thy xname)
+ | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
+ | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
(* parameters *)
@@ -1196,14 +1191,14 @@
val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs);
in (Term.dest_Free f, eq') end;
-fun abstract_thm sign eq =
- Thm.assume (Thm.cterm_of sign eq) |> Drule.gen_all |> Drule.abs_def;
+fun abstract_thm thy eq =
+ Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
fun bind_def ctxt (name, ps) ((xs, env, ths), eq) =
let
val ((y, T), b) = abstract_term eq;
val b' = norm_term env b;
- val th = abstract_thm (ProofContext.sign_of ctxt) eq;
+ val th = abstract_thm (ProofContext.theory_of ctxt) eq;
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
in
conditional (exists (equal y o #1) xs) (fn () =>
@@ -1382,7 +1377,7 @@
{var = I, typ = I, term = I,
name = prep_name ctxt,
fact = get ctxt,
- attrib = Args.assignable o intern (ProofContext.sign_of ctxt)};
+ attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
in
@@ -1399,11 +1394,12 @@
fun prep_context_statement prep_expr prep_elemss prep_facts
do_close fixed_params import elements raw_concl context =
let
- val sign = ProofContext.sign_of context;
+ val thy = ProofContext.theory_of context;
- val ((import_ids, import_syn), raw_import_elemss) = flatten (context, prep_expr sign) (([], Symtab.empty), Expr import);
+ val ((import_ids, import_syn), raw_import_elemss) =
+ flatten (context, prep_expr thy) (([], Symtab.empty), Expr import);
(* CB: normalise "includes" among elements *)
- val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr sign))
+ val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
((import_ids, import_syn), elements);
val raw_elemss = List.concat raw_elemsss;
@@ -1426,7 +1422,7 @@
val stmt = gen_distinct Term.aconv
(List.concat (map (fn ((_, axs), _) =>
List.concat (map (#hyps o Thm.rep_thm) axs)) qs));
- val cstmt = map (cterm_of sign) stmt;
+ val cstmt = map (cterm_of thy) stmt;
in
((((import_ctxt, import_elemss), (ctxt, elemss, syn)), (parms, spec, defs)), (cstmt, concl))
end;
@@ -1437,7 +1433,7 @@
fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt =
let
val thy = ProofContext.theory_of ctxt;
- val locale = Option.map (prep_locale (Theory.sign_of thy)) raw_locale;
+ val locale = Option.map (prep_locale thy) raw_locale;
val (target_stmt, fixed_params, import) =
(case locale of NONE => ([], [], empty)
| SOME name =>
@@ -1577,7 +1573,7 @@
val (parms, parmTs_o) =
the_locale thy target |> #params |> fst |> map fst |> split_list;
val parmvTs = map (Type.varifyT o valOf) parmTs_o;
- val ids = flatten (ProofContext.init thy, intern_expr (Theory.sign_of thy))
+ val ids = flatten (ProofContext.init thy, intern_expr thy)
(([], Symtab.empty), Expr (Locale target)) |> fst |> fst |> map fst;
val regs = get_global_registrations thy target;
@@ -1586,10 +1582,9 @@
fun activate (thy, (vts, ((prfx, atts2), _))) =
let
- val sg = Theory.sign_of thy;
val ts = map Logic.unvarify vts;
(* type instantiation *)
- val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of sg))
+ val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of thy))
(Vartab.empty, (parmvTs ~~ map Term.fastype_of ts));
val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
|> Symtab.make;
@@ -1602,7 +1597,7 @@
val args' = map (fn ((n, atts), [(ths, [])]) =>
((if prfx = "" orelse n = "" then "" else NameSpace.pack [prfx, n], (* FIXME *)
map (Attrib.global_attribute_i thy) (atts @ atts2)),
- [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm sg (inst, tinst)) ths, [])]))
+ [(map (Drule.standard o Drule.satisfy_hyps prems o inst_tab_thm thy (inst, tinst)) ths, [])]))
args;
in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end;
in Library.foldl activate (thy, regs) end;
@@ -1632,7 +1627,7 @@
fun gen_note_thmss prep_locale prep_facts kind raw_loc args thy =
let
val thy_ctxt = ProofContext.init thy;
- val loc = prep_locale (Theory.sign_of thy) raw_loc;
+ val loc = prep_locale thy raw_loc;
val (_, (stmt, _), loc_ctxt, _, _) = cert_context_statement (SOME loc) [] [] thy_ctxt;
val export = ProofContext.export_standard stmt loc_ctxt thy_ctxt;
@@ -1678,14 +1673,14 @@
val introN = "intro";
val axiomsN = "axioms";
-fun atomize_spec sign ts =
+fun atomize_spec thy ts =
let
val t = foldr1 Logic.mk_conjunction ts;
- val body = ObjectLogic.atomize_term sign t;
+ val body = ObjectLogic.atomize_term thy t;
val bodyT = Term.fastype_of body;
in
- if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of sign t))
- else (body, bodyT, ObjectLogic.atomize_rule sign (Thm.cterm_of sign t))
+ if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
+ else (body, bodyT, ObjectLogic.atomize_rule thy (Thm.cterm_of thy t))
end;
fun aprop_tr' n c = (c, fn args =>
@@ -1703,10 +1698,9 @@
fun def_pred bname parms defs ts norm_ts thy =
let
- val sign = Theory.sign_of thy;
- val name = Sign.full_name sign bname;
+ val name = Sign.full_name thy bname;
- val (body, bodyT, body_eq) = atomize_spec sign norm_ts;
+ val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
val env = Term.add_term_free_names (body, []);
val xs = List.filter (fn (x, _) => x mem_string env) parms;
val Ts = map #2 xs;
@@ -1716,7 +1710,7 @@
val args = map Logic.mk_type extraTs @ map Free xs;
val head = Term.list_comb (Const (name, predT), args);
- val statement = ObjectLogic.assert_propT sign head;
+ val statement = ObjectLogic.assert_propT thy head;
val (defs_thy, [pred_def]) =
thy
@@ -1725,10 +1719,9 @@
|> Theory.add_consts_i [(bname, predT, Syntax.NoSyn)]
|> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
- val defs_sign = Theory.sign_of defs_thy;
- val cert = Thm.cterm_of defs_sign;
+ val cert = Thm.cterm_of defs_thy;
- val intro = Tactic.prove_standard defs_sign [] norm_ts statement (fn _ =>
+ val intro = Tactic.prove_standard defs_thy [] norm_ts statement (fn _ =>
Tactic.rewrite_goals_tac [pred_def] THEN
Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
@@ -1738,7 +1731,7 @@
Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]
|> Drule.conj_elim_precise (length ts);
val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) =>
- Tactic.prove_plain defs_sign [] [] t (fn _ =>
+ Tactic.prove_plain defs_thy [] [] t (fn _ =>
Tactic.rewrite_goals_tac defs THEN
Tactic.compose_tac (false, ax, 0) 1));
in (defs_thy, (statement, intro, axioms)) end;
@@ -1788,7 +1781,7 @@
let
val (def_thy, (statement, intro, axioms)) =
thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
- val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement;
+ val cstatement = Thm.cterm_of def_thy statement;
in
def_thy |> note_thmss_qualified "" bname
[((introN, []), [([intro], [])]),
@@ -1808,8 +1801,7 @@
(* CB: do_pred controls generation of predicates.
true -> with, false -> without predicates. *)
let
- val sign = Theory.sign_of thy;
- val name = Sign.full_name sign bname;
+ val name = Sign.full_name thy bname;
val _ = conditional (isSome (get_locale thy name)) (fn () =>
error ("Duplicate definition of locale " ^ quote name));
@@ -1817,6 +1809,7 @@
val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), text) =
prep_ctxt raw_import raw_body thy_ctxt;
val elemss = import_elemss @ body_elemss;
+ val import = prep_expr thy raw_import;
val (pred_thy, (elemss', predicate as (predicate_statement, predicate_axioms))) =
if do_pred then thy |> define_preds bname text elemss
@@ -1838,7 +1831,7 @@
pred_thy
|> note_thmss_qualified "" name facts' |> #1
|> declare_locale name
- |> put_locale name {predicate = predicate, import = prep_expr sign raw_import,
+ |> put_locale name {predicate = predicate, import = import,
elems = map (fn e => (e, stamp ())) (List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))),
params = (params_of elemss' |>
map (fn (x, T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss))}
@@ -1935,10 +1928,10 @@
attn expr insts thy_ctxt =
let
val ctxt = mk_ctxt thy_ctxt;
- val sign = ProofContext.sign_of ctxt;
+ val thy = ProofContext.theory_of ctxt;
val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init;
- val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr sign)
+ val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy)
(([], Symtab.empty), Expr expr);
val do_close = false; (* effect unknown *)
val ((parms, all_elemss, _), (spec, (xs, defs, _))) =
@@ -2004,7 +1997,7 @@
(* instantiate ids and elements *)
val inst_elemss = map
- (fn (id, (_, elems)) => inst_tab_elems sign (inst, tinst) (id,
+ (fn (id, (_, elems)) => inst_tab_elems thy (inst, tinst) (id,
map (fn Int e => e) elems))
(ids' ~~ all_elemss);
@@ -2016,7 +2009,7 @@
val propss = extract_asms_elemss new_inst_elemss;
val bind_attrib = Attrib.crude_closure ctxt o Args.assignable;
- val attn' = apsnd (map (bind_attrib o Attrib.intern_src sign)) attn;
+ val attn' = apsnd (map (bind_attrib o Attrib.intern_src thy)) attn;
(** add registrations to theory or context,
without theorems, these are added after the proof **)
@@ -2034,7 +2027,7 @@
val prep_global_registration = gen_prep_registration
ProofContext.init false
(fn thy => fn sorts => fn used =>
- Sign.read_def_terms (Theory.sign_of thy, K NONE, sorts) used true)
+ Sign.read_def_terms (thy, K NONE, sorts) used true)
(fn thy => fn (name, ps) =>
test_global_registration thy (name, map Logic.varify ps))
(fn (name, ps) => put_global_registration (name, map Logic.varify ps))
--- a/src/Pure/Isar/proof_context.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Jun 17 18:35:27 2005 +0200
@@ -13,7 +13,7 @@
type exporter
exception CONTEXT of string * context
val theory_of: context -> theory
- val sign_of: context -> Sign.sg
+ val sign_of: context -> theory (*obsolete*)
val is_fixed: context -> string -> bool
val is_known: context -> string -> bool
val fixed_names_of: context -> string list
@@ -198,7 +198,7 @@
make_context (f (thy, syntax, data, asms, binds, thms, cases, defs));
fun theory_of (Context {thy, ...}) = thy;
-val sign_of = Theory.sign_of o theory_of;
+val sign_of = theory_of;
fun syntax_of (Context {syntax, ...}) = syntax;
fun fixes_of (Context {asms = (_, fixes), ...}) = fixes;
@@ -218,7 +218,7 @@
(* errors *)
-fun of_theory thy = "\nof theory " ^ Sign.str_of_sg (Theory.sign_of thy);
+fun of_theory thy = "\nof theory " ^ Context.str_of_thy thy;
fun err_inconsistent kinds =
error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " proof data");
@@ -240,20 +240,19 @@
(* data kind 'Isar/proof_data' *)
-structure ProofDataDataArgs =
-struct
+structure ProofDataData = TheoryDataFun
+(struct
val name = "Isar/proof_data";
type T = (Object.kind * ((theory -> Object.T) * (context -> Object.T -> unit))) Symtab.table;
val empty = Symtab.empty;
val copy = I;
- val prep_ext = I;
- fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
+ val extend = I;
+ fun merge _ tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
handle Symtab.DUPS kinds => err_inconsistent kinds;
fun print _ tab = Pretty.writeln (Pretty.strs (map #1 (Symtab.dest tab)));
-end;
+end);
-structure ProofDataData = TheoryDataFun(ProofDataDataArgs);
val _ = Context.add_setup [ProofDataData.init];
val print_proof_data = ProofDataData.print;
@@ -304,7 +303,7 @@
fun init thy =
let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
- make_context (thy, (Theory.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
+ make_context (thy, (Sign.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
(NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [],
(Vartab.empty, Vartab.empty, [], Symtab.empty))
end;
@@ -364,7 +363,7 @@
fun add_syntax decls =
map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs) =>
let
- val is_logtype = Sign.is_logtype (Theory.sign_of thy);
+ val is_logtype = Sign.is_logtype thy;
val structs' = structs @ List.mapPartial prep_struct decls;
val mxs = List.mapPartial prep_mixfix decls;
val (fixed, mxs_output) = Library.split_list (List.mapPartial prep_mixfix' decls);
@@ -385,11 +384,11 @@
(** pretty printing **)
-fun pretty_term ctxt t = Sign.pretty_term' (syn_of ctxt) (sign_of ctxt) (context_tr' ctxt t);
-fun pretty_typ ctxt T = Sign.pretty_typ (sign_of ctxt) T;
-fun pretty_sort ctxt S = Sign.pretty_sort (sign_of ctxt) S;
-fun pretty_classrel ctxt cs = Sign.pretty_classrel (sign_of ctxt) cs;
-fun pretty_arity ctxt ar = Sign.pretty_arity (sign_of ctxt) ar;
+fun pretty_term ctxt t = Sign.pretty_term' (syn_of ctxt) (theory_of ctxt) (context_tr' ctxt t);
+fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T;
+fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S;
+fun pretty_classrel ctxt cs = Sign.pretty_classrel (theory_of ctxt) cs;
+fun pretty_arity ctxt ar = Sign.pretty_arity (theory_of ctxt) ar;
fun pp ctxt = Pretty.pp (pretty_term ctxt, pretty_typ ctxt, pretty_sort ctxt,
pretty_classrel ctxt, pretty_arity ctxt);
@@ -433,11 +432,11 @@
local
fun read_typ_aux read ctxt s =
- transform_error (read (syn_of ctxt) (sign_of ctxt, def_sort ctxt)) s
+ transform_error (read (syn_of ctxt) (theory_of ctxt, def_sort ctxt)) s
handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt);
fun cert_typ_aux cert ctxt raw_T =
- cert (sign_of ctxt) raw_T
+ cert (theory_of ctxt) raw_T
handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
in
@@ -505,29 +504,29 @@
(* read / certify wrt. signature *) (*exception ERROR*) (*exception TERM*)
-fun read_def_termTs freeze pp syn sg (types, sorts, used) sTs =
- Sign.read_def_terms' pp (Sign.is_logtype sg) syn (sg, types, sorts) used freeze sTs;
+fun read_def_termTs freeze pp syn thy (types, sorts, used) sTs =
+ Sign.read_def_terms' pp (Sign.is_logtype thy) syn (thy, types, sorts) used freeze sTs;
-fun read_def_termT freeze pp syn sg defs sT =
- apfst hd (read_def_termTs freeze pp syn sg defs [sT]);
+fun read_def_termT freeze pp syn thy defs sT =
+ apfst hd (read_def_termTs freeze pp syn thy defs [sT]);
-fun read_term_sg freeze pp syn sg defs s =
- #1 (read_def_termT freeze pp syn sg defs (s, TypeInfer.logicT));
+fun read_term_thy freeze pp syn thy defs s =
+ #1 (read_def_termT freeze pp syn thy defs (s, TypeInfer.logicT));
-fun read_prop_sg freeze pp syn sg defs s =
- #1 (read_def_termT freeze pp syn sg defs (s, propT));
+fun read_prop_thy freeze pp syn thy defs s =
+ #1 (read_def_termT freeze pp syn thy defs (s, propT));
-fun read_terms_sg freeze pp syn sg defs =
- #1 o read_def_termTs freeze pp syn sg defs o map (rpair TypeInfer.logicT);
+fun read_terms_thy freeze pp syn thy defs =
+ #1 o read_def_termTs freeze pp syn thy defs o map (rpair TypeInfer.logicT);
-fun read_props_sg freeze pp syn sg defs =
- #1 o read_def_termTs freeze pp syn sg defs o map (rpair propT);
+fun read_props_thy freeze pp syn thy defs =
+ #1 o read_def_termTs freeze pp syn thy defs o map (rpair propT);
-fun cert_term_sg pp sg t = #1 (Sign.certify_term pp sg t);
+fun cert_term_thy pp thy t = #1 (Sign.certify_term pp thy t);
-fun cert_prop_sg pp sg tm =
- let val (t, T, _) = Sign.certify_term pp sg tm
+fun cert_prop_thy pp thy tm =
+ let val (t, T, _) = Sign.certify_term pp thy tm
in if T = propT then t else raise TERM ("Term not of type prop", [t]) end;
@@ -538,7 +537,7 @@
fun unifyT ctxt (T, U) =
let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U)
- in #1 (Type.unify (Sign.tsig_of (sign_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
+ in #1 (Type.unify (Sign.tsig_of (theory_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
fun norm_term (ctxt as Context {binds, ...}) schematic =
let
@@ -588,7 +587,7 @@
val sorts = append_env (def_sort ctxt) more_sorts;
val used = used_types ctxt @ more_used;
in
- (transform_error (read (pp ctxt) (syn_of ctxt) (sign_of ctxt) (types, sorts, used)) s
+ (transform_error (read (pp ctxt) (syn_of ctxt) (theory_of ctxt) (types, sorts, used)) s
handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
| ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
|> app (intern_skolem ctxt internal)
@@ -609,13 +608,13 @@
val read_prop_pats = read_term_pats propT;
fun read_term_liberal ctxt =
- gen_read' (read_term_sg true) I false false ctxt (K true) (K NONE) (K NONE) [];
+ gen_read' (read_term_thy true) I false false ctxt (K true) (K NONE) (K NONE) [];
-val read_term = gen_read (read_term_sg true) I false false;
-val read_prop = gen_read (read_prop_sg true) I false false;
-val read_prop_schematic = gen_read (read_prop_sg true) I false true;
-val read_terms = gen_read (read_terms_sg true) map false false;
-fun read_props schematic = gen_read (read_props_sg true) map false schematic;
+val read_term = gen_read (read_term_thy true) I false false;
+val read_prop = gen_read (read_prop_thy true) I false false;
+val read_prop_schematic = gen_read (read_prop_thy true) I false true;
+val read_terms = gen_read (read_terms_thy true) map false false;
+fun read_props schematic = gen_read (read_props_thy true) map false schematic;
end;
@@ -626,17 +625,17 @@
fun gen_cert cert pattern schematic ctxt t = t
|> (if pattern then I else norm_term ctxt schematic)
- |> (fn t' => cert (pp ctxt) (sign_of ctxt) t'
+ |> (fn t' => cert (pp ctxt) (theory_of ctxt) t'
handle TERM (msg, _) => raise CONTEXT (msg, ctxt));
in
-val cert_term = gen_cert cert_term_sg false false;
-val cert_prop = gen_cert cert_prop_sg false false;
-val cert_props = map oo gen_cert cert_prop_sg false;
+val cert_term = gen_cert cert_term_thy false false;
+val cert_prop = gen_cert cert_prop_thy false false;
+val cert_props = map oo gen_cert cert_prop_thy false;
-fun cert_term_pats _ = map o gen_cert cert_term_sg true false;
-val cert_prop_pats = map o gen_cert cert_prop_sg true false;
+fun cert_term_pats _ = map o gen_cert cert_term_thy true false;
+val cert_prop_pats = map o gen_cert cert_prop_thy true false;
end;
@@ -693,13 +692,13 @@
fun read_tyname ctxt c =
if c mem_string used_types ctxt then
- TFree (c, if_none (def_sort ctxt (c, ~1)) (Sign.defaultS (sign_of ctxt)))
- else Sign.read_tyname (sign_of ctxt) c;
+ TFree (c, if_none (def_sort ctxt (c, ~1)) (Sign.defaultS (theory_of ctxt)))
+ else Sign.read_tyname (theory_of ctxt) c;
fun read_const ctxt c =
(case lookup_skolem ctxt c of
SOME c' => Free (c', dummyT)
- | NONE => Sign.read_const (sign_of ctxt) c);
+ | NONE => Sign.read_const (theory_of ctxt) c);
@@ -774,8 +773,8 @@
|> Seq.map (Drule.implies_intr_list view)
|> Seq.map (fn rule =>
let
- val {sign, prop, ...} = Thm.rep_thm rule;
- val frees = map (Thm.cterm_of sign) (List.mapPartial (find_free prop) fixes);
+ val {thy, prop, ...} = Thm.rep_thm rule;
+ val frees = map (Thm.cterm_of thy) (List.mapPartial (find_free prop) fixes);
val tfrees = gen (Term.add_term_tfree_names (prop, []));
in
rule
@@ -852,7 +851,7 @@
val maxidx = fold (fn (t1, t2) => fn i =>
Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1;
- val envs = Unify.smash_unifiers (sign_of ctxt, Envir.empty maxidx,
+ val envs = Unify.smash_unifiers (theory_of ctxt, Envir.empty maxidx,
map swap pairs); (*prefer assignment of variables from patterns*)
val env =
(case Seq.pull envs of
@@ -882,7 +881,7 @@
val add_binds = fold (gen_bind read_term);
val add_binds_i = fold (gen_bind cert_term);
-fun auto_bind f ts ctxt = ctxt |> add_binds_i (map drop_schematic (f (sign_of ctxt) ts));
+fun auto_bind f ts ctxt = ctxt |> add_binds_i (map drop_schematic (f (theory_of ctxt) ts));
val auto_bind_goal = auto_bind AutoBind.goal;
val auto_bind_facts = auto_bind AutoBind.facts;
@@ -977,12 +976,12 @@
(*beware of proper order of evaluation!*)
fun retrieve_thms f g (ctxt as Context {thy, thms = (_, (space, tab), _), ...}) =
let
- val sg_ref = Sign.self_ref (Theory.sign_of thy);
+ val thy_ref = Theory.self_ref thy;
val get_from_thy = f thy;
in
fn xnamei as (xname, _) =>
(case Symtab.lookup (tab, NameSpace.intern space xname) of
- SOME ths => map (Thm.transfer_sg (Sign.deref sg_ref)) (PureThy.select_thm xnamei ths)
+ SOME ths => map (Thm.transfer (Theory.deref thy_ref)) (PureThy.select_thm xnamei ths)
| _ => get_from_thy xnamei) |> g xname
end;
@@ -1116,7 +1115,7 @@
fun head_of_def cprop =
#1 (Term.strip_comb (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop)))))
- |> Thm.cterm_of (Thm.sign_of_cterm cprop);
+ |> Thm.cterm_of (Thm.theory_of_cterm cprop);
fun export_def _ cprops thm =
thm
@@ -1132,7 +1131,7 @@
fun add_assm (ctxt, ((name, attrs), props)) =
let
- val cprops = map (Thm.cterm_of (sign_of ctxt)) props;
+ val cprops = map (Thm.cterm_of (theory_of ctxt)) props;
val asms = map (Tactic.norm_hhf_rule o Thm.assume) cprops;
val ths = map (fn th => ([th], [])) asms;
@@ -1438,7 +1437,7 @@
(*theory*)
val pretty_thy = Pretty.block
- [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg (sign_of ctxt)];
+ [Pretty.str "Theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)];
(*defaults*)
fun prt_atom prt prtT (x, X) = Pretty.block
--- a/src/Pure/Proof/extraction.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Jun 17 18:35:27 2005 +0200
@@ -7,7 +7,7 @@
signature EXTRACTION =
sig
- val set_preprocessor : (Sign.sg -> Proofterm.proof -> Proofterm.proof) -> theory -> theory
+ val set_preprocessor : (theory -> Proofterm.proof -> Proofterm.proof) -> theory -> theory
val add_realizes_eqns_i : ((term * term) list * (term * term)) list -> theory -> theory
val add_realizes_eqns : string list -> theory -> theory
val add_typeof_eqns_i : ((term * term) list * (term * term)) list -> theory -> theory
@@ -86,9 +86,9 @@
({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
foldr add_rule {next = next, rs = rs1, net = net} (rs2 \\ rs1);
-fun condrew sign rules procs =
+fun condrew thy rules procs =
let
- val tsig = Sign.tsig_of sign;
+ val tsig = Sign.tsig_of thy;
fun rew tm =
Pattern.rewrite_term tsig [] (condrew' :: procs) tm
@@ -112,7 +112,7 @@
(~1, map (Int.max o pairself maxidx_of_term) prems'),
iTs = Tenv, asol = tenv};
val env'' = Library.foldl (fn (env, p) =>
- Pattern.unify (sign, env, [pairself (lookup rew) p])) (env', prems')
+ Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems')
in SOME (Envir.norm_term env'' (inc (ren tm2)))
end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
(sort (Int.compare o pairself fst)
@@ -178,8 +178,8 @@
(* data kind 'Pure/extraction' *)
-structure ExtractionArgs =
-struct
+structure ExtractionData = TheoryDataFun
+(struct
val name = "Pure/extraction";
type T =
{realizes_eqns : rules,
@@ -189,7 +189,7 @@
realizers : (string list * (term * proof)) list Symtab.table,
defs : thm list,
expand : (string * term) list,
- prep : (Sign.sg -> proof -> proof) option}
+ prep : (theory -> proof -> proof) option}
val empty =
{realizes_eqns = empty_rules,
@@ -200,9 +200,9 @@
expand = [],
prep = NONE};
val copy = I;
- val prep_ext = I;
+ val extend = I;
- fun merge
+ fun merge _
(({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
realizers = realizers1, defs = defs1, expand = expand1, prep = prep1},
{realizes_eqns = realizes_eqns2, typeof_eqns = typeof_eqns2, types = types2,
@@ -216,16 +216,15 @@
expand = merge_lists expand1 expand2,
prep = (case prep1 of NONE => prep2 | _ => prep1)};
- fun print sg (x : T) = ();
-end;
+ fun print _ _ = ();
+end);
-structure ExtractionData = TheoryDataFun(ExtractionArgs);
val _ = Context.add_setup [ExtractionData.init];
fun read_condeq thy =
- let val sg = sign_of (add_syntax thy)
+ let val thy' = add_syntax thy
in fn s =>
- let val t = Logic.varify (term_of (read_cterm sg (s, propT)))
+ let val t = Logic.varify (term_of (read_cterm thy' (s, propT)))
in (map Logic.dest_equals (Logic.strip_imp_prems t),
Logic.dest_equals (Logic.strip_imp_concl t))
end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
@@ -286,13 +285,13 @@
fun freeze_thaw f x =
map_term_types thaw (f (map_term_types freeze x));
-fun etype_of sg vs Ts t =
+fun etype_of thy vs Ts t =
let
- val {typeof_eqns, ...} = ExtractionData.get_sg sg;
+ val {typeof_eqns, ...} = ExtractionData.get thy;
fun err () = error ("Unable to determine type of extracted program for\n" ^
- Sign.string_of_term sg t)
- in case strip_abs_body (freeze_thaw (condrew sg (#net typeof_eqns)
- [typeof_proc (Sign.defaultS sg) vs]) (list_abs (map (pair "x") (rev Ts),
+ Sign.string_of_term thy t)
+ in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
+ [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts),
Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
| _ => err ()
@@ -319,28 +318,26 @@
val rtypes = map fst types;
val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
val thy' = add_syntax thy;
- val sign = sign_of thy';
- val tsg = Sign.tsig_of sign;
val rd = ProofSyntax.read_proof thy' false
in fn (thm, (vs, s1, s2)) =>
let
val name = Thm.name_of_thm thm;
val _ = assert (name <> "") "add_realizers: unnamed theorem";
- val prop = Pattern.rewrite_term tsg
+ val prop = Pattern.rewrite_term (Sign.tsig_of thy')
(map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
val vars = vars_of prop;
val vars' = filter_out (fn v =>
tname_of (body_type (fastype_of v)) mem rtypes) vars;
- val T = etype_of sign vs [] prop;
+ val T = etype_of thy' vs [] prop;
val (T', thw) = Type.freeze_thaw_type
(if T = nullT then nullT else map fastype_of vars' ---> T);
- val t = map_term_types thw (term_of (read_cterm sign (s1, T')));
- val r' = freeze_thaw (condrew sign eqns
- (procs @ [typeof_proc (Sign.defaultS sign) vs, rlz_proc]))
+ val t = map_term_types thw (term_of (read_cterm thy' (s1, T')));
+ val r' = freeze_thaw (condrew thy' eqns
+ (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
(Const ("realizes", T --> propT --> propT) $
(if T = nullT then t else list_comb (t, vars')) $ prop);
val r = foldr forall_intr r' (map (get_var_type r') vars);
- val prf = Reconstruct.reconstruct_proof sign r (rd s2);
+ val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
in (name, (vs, (t, prf))) end
end;
@@ -351,15 +348,14 @@
fun realizes_of thy vs t prop =
let
val thy' = add_syntax thy;
- val sign = sign_of thy';
val {realizes_eqns, typeof_eqns, defs, types, ...} =
ExtractionData.get thy';
val procs = List.concat (map (fst o snd) types);
val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
- val prop' = Pattern.rewrite_term (Sign.tsig_of sign)
+ val prop' = Pattern.rewrite_term (Sign.tsig_of thy')
(map (Logic.dest_equals o prop_of) defs) [] prop;
- in freeze_thaw (condrew sign eqns
- (procs @ [typeof_proc (Sign.defaultS sign) vs, rlz_proc]))
+ in freeze_thaw (condrew thy' eqns
+ (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
(Const ("realizes", fastype_of t --> propT --> propT) $ t $ prop')
end;
@@ -403,7 +399,7 @@
in
ExtractionData.put
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns,
- types = map (apfst (Sign.intern_type (sign_of thy))) tys @ types,
+ types = map (apfst (Sign.intern_type thy)) tys @ types,
realizers = realizers, defs = defs, expand = expand, prep = prep} thy
end;
@@ -466,15 +462,14 @@
fun extract thms thy =
let
- val sg = sign_of (add_syntax thy);
- val tsg = Sign.tsig_of sg;
+ val thy' = add_syntax thy;
val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
ExtractionData.get thy;
val procs = List.concat (map (fst o snd) types);
val rtypes = map fst types;
- val typroc = typeof_proc (Sign.defaultS sg);
- val prep = getOpt (prep, K I) sg o ProofRewriteRules.elim_defs sg false defs o
- Reconstruct.expand_proof sg (("", NONE) :: map (apsnd SOME) expand);
+ val typroc = typeof_proc (Sign.defaultS thy');
+ val prep = getOpt (prep, K I) thy' o ProofRewriteRules.elim_defs thy' false defs o
+ Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand);
val rrews = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
fun find_inst prop Ts ts vs =
@@ -485,7 +480,7 @@
fun add_args ((Var ((a, i), _), t), (vs', tye)) =
if a mem rvs then
- let val T = etype_of sg vs Ts t
+ let val T = etype_of thy' vs Ts t
in if T = nullT then (vs', tye)
else (a :: vs', (("'" ^ a, i), T) :: tye)
end
@@ -497,7 +492,7 @@
fun find' s = map snd o List.filter (equal s o fst)
fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
- (condrew sg rrews (procs @ [typroc vs, rlz_proc])) (list_abs
+ (condrew thy' rrews (procs @ [typroc vs, rlz_proc])) (list_abs
(map (pair "x") (rev Ts), t)));
fun realizes_null vs prop = app_rlz_rews [] vs
@@ -513,7 +508,7 @@
| corr d defs vs ts Ts hs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
let
- val T = etype_of sg vs Ts prop;
+ val T = etype_of thy' vs Ts prop;
val u = if T = nullT then
(case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
@@ -537,7 +532,7 @@
else (case t' of SOME (u $ _) => SOME u | _ => NONE));
val u = if not (tname_of T mem rtypes) then t else
let
- val eT = etype_of sg vs Ts t;
+ val eT = etype_of thy' vs Ts t;
val (r, Us') = if eT = nullT then (nullt, Us) else
(Bound (length Us), eT :: Us);
val u = list_comb (incr_boundvars (length Us') t,
@@ -551,7 +546,7 @@
| corr d defs vs ts Ts hs (prf1 %% prf2) (prf1' %% prf2') t =
let
val prop = Reconstruct.prop_of' hs prf2';
- val T = etype_of sg vs Ts prop;
+ val T = etype_of thy' vs Ts prop;
val (defs1, f, u) = if T = nullT then (defs, t, NONE) else
(case t of
SOME (f $ u) => (defs, SOME f, SOME u)
@@ -569,7 +564,7 @@
let
val (vs', tye) = find_inst prop Ts ts vs;
val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye;
- val T = etype_of sg vs' [] prop;
+ val T = etype_of thy' vs' [] prop;
val defs' = if T = nullT then defs
else fst (extr d defs vs ts Ts hs prf0)
in
@@ -582,7 +577,7 @@
val _ = msg d ("Building correctness proof for " ^ quote name ^
(if null vs' then ""
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
- val prf' = prep (Reconstruct.reconstruct_proof sg prop prf);
+ val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
val (defs'', corr_prf) =
corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
val corr_prop = Reconstruct.prop_of corr_prf;
@@ -599,7 +594,7 @@
| SOME rs => (case find vs' rs of
SOME (_, prf') => (defs', prf_subst_TVars tye' prf')
| NONE => error ("corr: no realizer for instance of theorem " ^
- quote name ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
+ quote name ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
(Reconstruct.prop_of (proof_combt (prf0, ts))))))
end
@@ -608,12 +603,12 @@
val (vs', tye) = find_inst prop Ts ts vs;
val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
in
- if etype_of sg vs' [] prop = nullT andalso
+ if etype_of thy' vs' [] prop = nullT andalso
realizes_null vs' prop aconv prop then (defs, prf0)
else case find vs' (Symtab.lookup_multi (realizers, s)) of
SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
| NONE => error ("corr: no realizer for instance of axiom " ^
- quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
+ quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
(Reconstruct.prop_of (proof_combt (prf0, ts)))))
end
@@ -628,7 +623,7 @@
| extr d defs vs ts Ts hs (AbsP (s, SOME t, prf)) =
let
- val T = etype_of sg vs Ts t;
+ val T = etype_of thy' vs Ts t;
val (defs', t) = extr d defs vs [] (T :: Ts) (t :: hs)
(incr_pboundvars 0 1 prf)
in (defs',
@@ -646,7 +641,7 @@
let
val (defs', f) = extr d defs vs [] Ts hs prf1;
val prop = Reconstruct.prop_of' hs prf2;
- val T = etype_of sg vs Ts prop
+ val T = etype_of thy' vs Ts prop
in
if T = nullT then (defs', f) else
let val (defs'', t) = extr d defs' vs [] Ts hs prf2
@@ -665,7 +660,7 @@
val _ = msg d ("Extracting " ^ quote s ^
(if null vs' then ""
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
- val prf' = prep (Reconstruct.reconstruct_proof sg prop prf);
+ val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
val (defs', t) = extr (d + 1) defs vs' [] [] [] prf';
val (defs'', corr_prf) =
corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
@@ -708,7 +703,7 @@
| SOME rs => (case find vs' rs of
SOME (t, _) => (defs, subst_TVars tye' t)
| NONE => error ("extr: no realizer for instance of theorem " ^
- quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
+ quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
(Reconstruct.prop_of (proof_combt (prf0, ts))))))
end
@@ -720,7 +715,7 @@
case find vs' (Symtab.lookup_multi (realizers, s)) of
SOME (t, _) => (defs, subst_TVars tye' t)
| NONE => error ("extr: no realizer for instance of axiom " ^
- quote s ^ ":\n" ^ Sign.string_of_term sg (Envir.beta_norm
+ quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
(Reconstruct.prop_of (proof_combt (prf0, ts)))))
end
@@ -731,7 +726,7 @@
val {prop, der = (_, prf), sign, ...} = rep_thm thm;
val name = Thm.name_of_thm thm;
val _ = assert (name <> "") "extraction: unnamed theorem";
- val _ = assert (etype_of sg vs [] prop <> nullT) ("theorem " ^
+ val _ = assert (etype_of thy' vs [] prop <> nullT) ("theorem " ^
quote name ^ " has no computational content")
in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
@@ -739,7 +734,7 @@
fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms);
fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
- (case Sign.const_type (sign_of thy) (extr_name s vs) of
+ (case Sign.const_type thy (extr_name s vs) of
NONE =>
let
val corr_prop = Reconstruct.prop_of prf;
@@ -798,6 +793,6 @@
val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP];
-val etype_of = etype_of o sign_of o add_syntax;
+val etype_of = etype_of o add_syntax;
end;
--- a/src/Pure/axclass.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Pure/axclass.ML Fri Jun 17 18:35:27 2005 +0200
@@ -119,41 +119,40 @@
intro: thm,
axioms: thm list};
-structure AxclassesArgs =
-struct
+structure AxclassesData = TheoryDataFun
+(struct
val name = "Pure/axclasses";
type T = axclass_info Symtab.table;
val empty = Symtab.empty;
val copy = I;
- val prep_ext = I;
- fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2);
+ val extend = I;
+ fun merge _ = Symtab.merge (K true);
- fun print sg tab =
+ fun print thy tab =
let
fun pretty_class c cs = Pretty.block
- (Pretty.str (Sign.extern_class sg c) :: Pretty.str " <" :: Pretty.brk 1 ::
- Pretty.breaks (map (Pretty.str o Sign.extern_class sg) cs));
+ (Pretty.str (Sign.extern_class thy c) :: Pretty.str " <" :: Pretty.brk 1 ::
+ Pretty.breaks (map (Pretty.str o Sign.extern_class thy) cs));
fun pretty_thms name thms = Pretty.big_list (name ^ ":")
- (map (Display.pretty_thm_sg sg) thms);
+ (map (Display.pretty_thm_sg thy) thms);
fun pretty_axclass (name, {super_classes, intro, axioms}) = Pretty.block (Pretty.fbreaks
[pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]);
in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end;
-end;
+end);
-structure AxclassesData = TheoryDataFun(AxclassesArgs);
val _ = Context.add_setup [AxclassesData.init];
val print_axclasses = AxclassesData.print;
(* get and put data *)
-fun lookup_axclass_info_sg sg c = Symtab.lookup (AxclassesData.get_sg sg, c);
+fun lookup_axclass_info thy c = Symtab.lookup (AxclassesData.get thy, c);
fun get_axclass_info thy c =
- (case lookup_axclass_info_sg (Theory.sign_of thy) c of
+ (case lookup_axclass_info thy c of
NONE => error ("Unknown axclass " ^ quote c)
| SOME info => info);
@@ -163,10 +162,10 @@
(* class_axms *)
-fun class_axms sign =
- let val classes = Sign.classes sign in
- map (Thm.class_triv sign) classes @
- List.mapPartial (Option.map #intro o lookup_axclass_info_sg sign) classes
+fun class_axms thy =
+ let val classes = Sign.classes thy in
+ map (Thm.class_triv thy) classes @
+ List.mapPartial (Option.map #intro o lookup_axclass_info thy) classes
end;
@@ -183,17 +182,14 @@
fun ext_axclass prep_class prep_axm prep_att (bclass, raw_super_classes) raw_axioms_atts thy =
let
- val sign = Theory.sign_of thy;
-
- val class = Sign.full_name sign bclass;
- val super_classes = map (prep_class sign) raw_super_classes;
- val axms = map (prep_axm sign o fst) raw_axioms_atts;
+ val class = Sign.full_name thy bclass;
+ val super_classes = map (prep_class thy) raw_super_classes;
+ val axms = map (prep_axm thy o fst) raw_axioms_atts;
val atts = map (map (prep_att thy) o snd) raw_axioms_atts;
(*declare class*)
val class_thy =
thy |> Theory.add_classes_i [(bclass, super_classes)];
- val class_sign = Theory.sign_of class_thy;
(*prepare abstract axioms*)
fun abs_axm ax =
@@ -205,9 +201,9 @@
fun axm_sort (name, ax) =
(case term_tfrees ax of
[] => []
- | [(_, S)] => if Sign.subsort class_sign ([class], S) then S else err_bad_axsort name class
+ | [(_, S)] => if Sign.subsort class_thy ([class], S) then S else err_bad_axsort name class
| _ => err_bad_tfrees name);
- val axS = Sign.certify_sort class_sign (List.concat (map axm_sort axms));
+ val axS = Sign.certify_sort class_thy (List.concat (map axm_sort axms));
val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
fun inclass c = Logic.mk_inclass (aT axS, c);
@@ -268,16 +264,16 @@
(* prepare classes and arities *)
-fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
+fun read_class thy c = Sign.certify_class thy (Sign.intern_class thy c);
-fun test_classrel sg cc = (Type.add_classrel (Sign.pp sg) [cc] (Sign.tsig_of sg); cc);
-fun cert_classrel sg = test_classrel sg o Library.pairself (Sign.certify_class sg);
-fun read_classrel sg = test_classrel sg o Library.pairself (read_class sg);
+fun test_classrel thy cc = (Type.add_classrel (Sign.pp thy) [cc] (Sign.tsig_of thy); cc);
+fun cert_classrel thy = test_classrel thy o Library.pairself (Sign.certify_class thy);
+fun read_classrel thy = test_classrel thy o Library.pairself (read_class thy);
-fun test_arity sg ar = (Type.add_arities (Sign.pp sg) [ar] (Sign.tsig_of sg); ar);
+fun test_arity thy ar = (Type.add_arities (Sign.pp thy) [ar] (Sign.tsig_of thy); ar);
-fun prep_arity prep_tycon prep_sort prep sg (t, Ss, x) =
- test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep sg x);
+fun prep_arity prep_tycon prep_sort prep thy (t, Ss, x) =
+ test_arity thy (prep_tycon thy t, map (prep_sort thy) Ss, prep thy x);
val read_arity = prep_arity Sign.intern_type Sign.read_sort Sign.read_sort;
val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
@@ -289,22 +285,20 @@
fun ext_inst_subclass prep_classrel raw_cc tac thy =
let
- val sign = Theory.sign_of thy;
- val (c1, c2) = prep_classrel sign raw_cc;
- val txt = quote (Sign.string_of_classrel sign [c1, c2]);
+ val (c1, c2) = prep_classrel thy raw_cc;
+ val txt = quote (Sign.string_of_classrel thy [c1, c2]);
val _ = message ("Proving class inclusion " ^ txt ^ " ...");
- val th = Tactic.prove sign [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR =>
+ val th = Tactic.prove thy [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR =>
error ("The error(s) above occurred while trying to prove " ^ txt);
in add_classrel_thms [th] thy end;
fun ext_inst_arity prep_arity raw_arity tac thy =
let
- val sign = Theory.sign_of thy;
- val arity = prep_arity sign raw_arity;
- val txt = quote (Sign.string_of_arity sign arity);
+ val arity = prep_arity thy raw_arity;
+ val txt = quote (Sign.string_of_arity thy arity);
val _ = message ("Proving type arity " ^ txt ^ " ...");
val props = (mk_arities arity);
- val ths = Tactic.prove_multi sign [] [] props
+ val ths = Tactic.prove_multi thy [] [] props
(fn _ => Tactic.smart_conjunction_tac (length props) THEN tac)
handle ERROR => error ("The error(s) above occurred while trying to prove " ^ txt);
in add_arity_thms ths thy end;
@@ -327,7 +321,7 @@
theory
|> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
("", [fn (thy, th) => (add_thms [th] thy, th)]) []
- (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
+ (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int;
in
@@ -345,7 +339,7 @@
fun intro_classes_tac facts st =
(ALLGOALS (Method.insert_tac facts THEN'
- REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st))))
+ REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.theory_of_thm st))))
THEN Tactic.distinct_subgoals_tac) st;
fun default_intro_classes_tac [] = intro_classes_tac []
@@ -410,41 +404,39 @@
local
-fun prove mk_prop str_of sign prop thms usr_tac =
- (Tactic.prove sign [] [] (mk_prop prop)
+fun prove mk_prop str_of thy prop thms usr_tac =
+ (Tactic.prove thy [] [] (mk_prop prop)
(K (axclass_tac thms THEN (if_none usr_tac all_tac)))
handle ERROR => error ("The error(s) above occurred while trying to prove " ^
- quote (str_of sign prop))) |> Drule.standard;
+ quote (str_of thy prop))) |> Drule.standard;
-val prove_subclass = prove mk_classrel (fn sg => fn (c1, c2) =>
- Pretty.string_of_classrel (Sign.pp sg) [c1, c2]);
+val prove_subclass = prove mk_classrel (fn thy => fn (c1, c2) =>
+ Pretty.string_of_classrel (Sign.pp thy) [c1, c2]);
-val prove_arity = prove mk_arity (fn sg => fn (t, Ss, c) =>
- Pretty.string_of_arity (Sign.pp sg) (t, Ss, [c]));
+val prove_arity = prove mk_arity (fn thy => fn (t, Ss, c) =>
+ Pretty.string_of_arity (Sign.pp thy) (t, Ss, [c]));
fun witnesses thy names thms =
- PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ List.filter is_def (map snd (axioms_of thy));
+ PureThy.get_thmss thy (map (rpair NONE) names) @
+ thms @
+ List.filter is_def (map snd (axioms_of thy));
in
fun add_inst_subclass_x raw_c1_c2 names thms usr_tac thy =
- let
- val sign = Theory.sign_of thy;
- val (c1, c2) = read_classrel sign raw_c1_c2;
- in
- message ("Proving class inclusion " ^ quote (Sign.string_of_classrel sign [c1, c2]) ^ " ...");
- thy |> add_classrel_thms [prove_subclass sign (c1, c2) (witnesses thy names thms) usr_tac]
+ let val (c1, c2) = read_classrel thy raw_c1_c2 in
+ message ("Proving class inclusion " ^ quote (Sign.string_of_classrel thy [c1, c2]) ^ " ...");
+ thy |> add_classrel_thms [prove_subclass thy (c1, c2) (witnesses thy names thms) usr_tac]
end;
fun add_inst_arity_x raw_arity names thms usr_tac thy =
let
- val sign = Theory.sign_of thy;
- val (t, Ss, cs) = read_arity sign raw_arity;
+ val (t, Ss, cs) = read_arity thy raw_arity;
val wthms = witnesses thy names thms;
fun prove c =
(message ("Proving type arity " ^
- quote (Sign.string_of_arity sign (t, Ss, [c])) ^ " ...");
- prove_arity sign (t, Ss, c) wthms usr_tac);
+ quote (Sign.string_of_arity thy (t, Ss, [c])) ^ " ...");
+ prove_arity thy (t, Ss, c) wthms usr_tac);
in add_arity_thms (map prove cs) thy end;
end;
--- a/src/Pure/codegen.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Pure/codegen.ML Fri Jun 17 18:35:27 2005 +0200
@@ -38,8 +38,8 @@
val invoke_tycodegen: theory -> string -> bool ->
(exn option * string) Graph.T * typ -> (exn option * string) Graph.T * Pretty.T
val mk_id: string -> string
- val mk_const_id: Sign.sg -> string -> string
- val mk_type_id: Sign.sg -> string -> string
+ val mk_const_id: theory -> string -> string
+ val mk_type_id: theory -> string -> string
val rename_term: term -> term
val new_names: term -> string list -> string list
val new_name: term -> string -> string
@@ -50,8 +50,8 @@
val eta_expand: term -> term list -> int -> term
val strip_tname: string -> string
val mk_type: bool -> typ -> Pretty.T
- val mk_term_of: Sign.sg -> bool -> typ -> Pretty.T
- val mk_gen: Sign.sg -> bool -> string list -> string -> typ -> Pretty.T
+ val mk_term_of: theory -> bool -> typ -> Pretty.T
+ val mk_gen: theory -> bool -> string list -> string -> typ -> Pretty.T
val test_fn: (int -> (string * term) list option) ref
val test_term: theory -> int -> int -> term -> (string * term) list option
val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
@@ -121,14 +121,14 @@
fun set_iterations iterations ({size, default_type, ...} : test_params) =
{size = size, iterations = iterations, default_type = default_type};
-fun set_default_type s sg ({size, iterations, ...} : test_params) =
+fun set_default_type s thy ({size, iterations, ...} : test_params) =
{size = size, iterations = iterations,
- default_type = SOME (typ_of (read_ctyp sg s))};
+ default_type = SOME (typ_of (read_ctyp thy s))};
(* data kind 'Pure/codegen' *)
-
-structure CodegenArgs =
-struct
+
+structure CodegenData = TheoryDataFun
+(struct
val name = "Pure/codegen";
type T =
{codegens : (string * term codegen) list,
@@ -143,9 +143,9 @@
{codegens = [], tycodegens = [], consts = [], types = [], attrs = [],
preprocs = [], test_params = default_test_params};
val copy = I;
- val prep_ext = I;
+ val extend = I;
- fun merge
+ fun merge _
({codegens = codegens1, tycodegens = tycodegens1,
consts = consts1, types = types1, attrs = attrs1,
preprocs = preprocs1, test_params = test_params1},
@@ -160,13 +160,12 @@
preprocs = merge_alists' preprocs1 preprocs2,
test_params = merge_test_params test_params1 test_params2};
- fun print sg ({codegens, tycodegens, ...} : T) =
+ fun print _ ({codegens, tycodegens, ...} : T) =
Pretty.writeln (Pretty.chunks
[Pretty.strs ("term code generators:" :: map fst codegens),
Pretty.strs ("type code generators:" :: map fst tycodegens)]);
-end;
+end);
-structure CodegenData = TheoryDataFun(CodegenArgs);
val _ = Context.add_setup [CodegenData.init];
val print_codegens = CodegenData.print;
@@ -265,18 +264,17 @@
fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) =>
let
- val sg = sign_of thy;
val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
CodegenData.get thy;
- val cname = Sign.intern_const sg s;
+ val cname = Sign.intern_const thy s;
in
- (case Sign.const_type sg cname of
+ (case Sign.const_type thy cname of
SOME T =>
let val T' = (case tyopt of
NONE => T
| SOME ty =>
- let val U = prep_type sg ty
- in if Sign.typ_instance sg (U, T) then U
+ let val U = prep_type thy ty
+ in if Sign.typ_instance thy (U, T) then U
else error ("Illegal type constraint for constant " ^ cname)
end)
in (case assoc (consts, (cname, T')) of
@@ -291,7 +289,7 @@
end) (thy, xs);
val assoc_consts_i = gen_assoc_consts (K I);
-val assoc_consts = gen_assoc_consts (fn sg => typ_of o read_ctyp sg);
+val assoc_consts = gen_assoc_consts (typ_of oo read_ctyp);
(**** associate types with target language types ****)
@@ -322,7 +320,7 @@
("<" :: "^" :: xs, ">") => (true, implode xs)
| ("<" :: xs, ">") => (false, implode xs)
| _ => sys_error "dest_sym");
-
+
fun mk_id s = if s = "" then "" else
let
fun check_str [] = []
@@ -341,12 +339,12 @@
if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
end;
-fun mk_const_id sg s =
- let val s' = mk_id (Sign.extern_const sg s)
+fun mk_const_id thy s =
+ let val s' = mk_id (Sign.extern_const thy s)
in if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' end;
-fun mk_type_id sg s =
- let val s' = mk_id (Sign.extern_type sg s)
+fun mk_type_id thy s =
+ let val s' = mk_id (Sign.extern_type thy s)
in if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' end;
fun rename_terms ts =
@@ -570,11 +568,10 @@
fun gen_generate_code prep_term thy =
setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
let
- val sg = sign_of thy;
val gr = Graph.new_node ("<Top>", (NONE, "")) Graph.empty;
val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
(invoke_codegen thy "<Top>" false (gr, t)))
- (gr, map (apsnd (prep_term sg)) xs)
+ (gr, map (apsnd (prep_term thy)) xs)
val code =
"structure Generated =\nstruct\n\n" ^
output_code gr' ["<Top>"] ^
@@ -585,7 +582,7 @@
val generate_code_i = gen_generate_code (K I);
val generate_code = gen_generate_code
- (fn sg => term_of o read_cterm sg o rpair TypeInfer.logicT);
+ (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT);
(**** Reflection ****)
@@ -603,22 +600,22 @@
[Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","),
Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]);
-fun mk_term_of sg p (TVar ((s, i), _)) = Pretty.str
+fun mk_term_of _ p (TVar ((s, i), _)) = Pretty.str
(strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
- | mk_term_of sg p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
- | mk_term_of sg p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
- (separate (Pretty.brk 1) (Pretty.str ("term_of_" ^ mk_type_id sg s) ::
- List.concat (map (fn T => [mk_term_of sg true T, mk_type true T]) Ts))));
+ | mk_term_of _ p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
+ | mk_term_of thy p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
+ (separate (Pretty.brk 1) (Pretty.str ("term_of_" ^ mk_type_id thy s) ::
+ List.concat (map (fn T => [mk_term_of thy true T, mk_type true T]) Ts))));
(**** Test data generators ****)
-fun mk_gen sg p xs a (TVar ((s, i), _)) = Pretty.str
+fun mk_gen _ p xs a (TVar ((s, i), _)) = Pretty.str
(strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
- | mk_gen sg p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
- | mk_gen sg p xs a (Type (s, Ts)) = (if p then parens else I) (Pretty.block
- (separate (Pretty.brk 1) (Pretty.str ("gen_" ^ mk_type_id sg s ^
- (if s mem xs then "'" else "")) :: map (mk_gen sg true xs a) Ts @
+ | mk_gen _ p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
+ | mk_gen thy p xs a (Type (s, Ts)) = (if p then parens else I) (Pretty.block
+ (separate (Pretty.brk 1) (Pretty.str ("gen_" ^ mk_type_id thy s ^
+ (if s mem xs then "'" else "")) :: map (mk_gen thy true xs a) Ts @
(if s mem xs then [Pretty.str a] else []))));
val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
@@ -629,7 +626,6 @@
"Term to be tested contains type variables";
val _ = assert (null (term_vars t))
"Term to be tested contains schematic variables";
- val sg = sign_of thy;
val frees = map dest_Free (term_frees t);
val szname = variant (map fst frees) "i";
val s = "structure TestTerm =\nstruct\n\n" ^
@@ -641,7 +637,7 @@
Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) =>
Pretty.block [Pretty.str ("val " ^ mk_id s ^ " ="), Pretty.brk 1,
- mk_gen sg false [] "" T, Pretty.brk 1,
+ mk_gen thy false [] "" T, Pretty.brk 1,
Pretty.str (szname ^ ";")]) frees)),
Pretty.brk 1, Pretty.str "in", Pretty.brk 1,
Pretty.block [Pretty.str "if ",
@@ -652,7 +648,7 @@
List.concat (separate [Pretty.str ",", Pretty.brk 1]
(map (fn (s, T) => [Pretty.block
[Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1,
- mk_app false (mk_term_of sg false T)
+ mk_app false (mk_term_of thy false T)
[Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @
[Pretty.str "]"])]],
Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
@@ -670,12 +666,12 @@
fun test_goal ({size, iterations, default_type}, tvinsts) i st =
let
- val sg = Toplevel.sign_of st;
+ val thy = Toplevel.theory_of st;
fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
| strip t = t;
val (gi, frees) = Logic.goal_params
(prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
- val gi' = ObjectLogic.atomize_term sg (map_term_types
+ val gi' = ObjectLogic.atomize_term thy (map_term_types
(map_type_tfree (fn p as (s, _) => getOpt (assoc (tvinsts, s),
getOpt (default_type,TFree p)))) (subst_bounds (frees, strip gi)));
in case test_term (Toplevel.theory_of st) size iterations gi' of
@@ -683,7 +679,7 @@
| SOME cex => writeln ("Counterexample found:\n" ^
Pretty.string_of (Pretty.chunks (map (fn (s, t) =>
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,
- Sign.pretty_term sg t]) cex)))
+ Sign.pretty_term thy t]) cex)))
end;
@@ -753,8 +749,8 @@
P.$$$ "=" |-- getOpt (assoc (params, s), Scan.fail)) >> snd;
fun parse_tyinst xs =
- (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn sg =>
- fn (x, ys) => (x, (v, typ_of (read_ctyp sg s)) :: ys))) xs;
+ (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
+ fn (x, ys) => (x, (v, typ_of (read_ctyp thy s)) :: ys))) xs;
fun app [] x = x
| app (f :: fs) x = app fs (f x);
@@ -768,7 +764,7 @@
val testP =
OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
(Scan.option (P.$$$ "[" |-- P.list1
- ( parse_test_params >> (fn f => fn sg => apfst (f sg))
+ ( parse_test_params >> (fn f => fn thy => apfst (f thy))
|| parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
(fn (ps, g) => Toplevel.keep (fn st =>
test_goal (app (getOpt (Option.map
--- a/src/Pure/goals.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Pure/goals.ML Fri Jun 17 18:35:27 2005 +0200
@@ -1,6 +1,6 @@
-(* Title: Pure/goals.ML
+(* Title: Pure/goals.ML
ID: $Id$
- Author: Lawrence C Paulson and Florian Kammueller, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson and Florian Kammueller, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Old-style locales and goal stack package. The goal stack initially
@@ -19,71 +19,71 @@
val thms: xstring -> thm list
type proof
val reset_goals : unit -> unit
- val atomic_goal : theory -> string -> thm list
- val atomic_goalw : theory -> thm list -> string -> thm list
- val Goal : string -> thm list
- val Goalw : thm list -> string -> thm list
- val ba : int -> unit
- val back : unit -> unit
- val bd : thm -> int -> unit
- val bds : thm list -> int -> unit
- val be : thm -> int -> unit
- val bes : thm list -> int -> unit
- val br : thm -> int -> unit
- val brs : thm list -> int -> unit
- val bw : thm -> unit
- val bws : thm list -> unit
- val by : tactic -> unit
- val byev : tactic list -> unit
- val chop : unit -> unit
- val choplev : int -> unit
+ val atomic_goal : theory -> string -> thm list
+ val atomic_goalw : theory -> thm list -> string -> thm list
+ val Goal : string -> thm list
+ val Goalw : thm list -> string -> thm list
+ val ba : int -> unit
+ val back : unit -> unit
+ val bd : thm -> int -> unit
+ val bds : thm list -> int -> unit
+ val be : thm -> int -> unit
+ val bes : thm list -> int -> unit
+ val br : thm -> int -> unit
+ val brs : thm list -> int -> unit
+ val bw : thm -> unit
+ val bws : thm list -> unit
+ val by : tactic -> unit
+ val byev : tactic list -> unit
+ val chop : unit -> unit
+ val choplev : int -> unit
val export_thy : theory -> thm -> thm
val export : thm -> thm
- val Export : thm -> thm
- val fa : unit -> unit
- val fd : thm -> unit
- val fds : thm list -> unit
- val fe : thm -> unit
- val fes : thm list -> unit
- val filter_goal : (term*term->bool) -> thm list -> int -> thm list
- val fr : thm -> unit
- val frs : thm list -> unit
- val getgoal : int -> term
- val gethyps : int -> thm list
- val goal : theory -> string -> thm list
- val goalw : theory -> thm list -> string -> thm list
- val goalw_cterm : thm list -> cterm -> thm list
- val pop_proof : unit -> thm list
- val pr : unit -> unit
+ val Export : thm -> thm
+ val fa : unit -> unit
+ val fd : thm -> unit
+ val fds : thm list -> unit
+ val fe : thm -> unit
+ val fes : thm list -> unit
+ val filter_goal : (term*term->bool) -> thm list -> int -> thm list
+ val fr : thm -> unit
+ val frs : thm list -> unit
+ val getgoal : int -> term
+ val gethyps : int -> thm list
+ val goal : theory -> string -> thm list
+ val goalw : theory -> thm list -> string -> thm list
+ val goalw_cterm : thm list -> cterm -> thm list
+ val pop_proof : unit -> thm list
+ val pr : unit -> unit
val disable_pr : unit -> unit
val enable_pr : unit -> unit
- val prlev : int -> unit
- val prlim : int -> unit
- val premises : unit -> thm list
- val prin : term -> unit
- val printyp : typ -> unit
- val pprint_term : term -> pprint_args -> unit
- val pprint_typ : typ -> pprint_args -> unit
- val print_exn : exn -> 'a
- val print_sign_exn : Sign.sg -> exn -> 'a
- val prove_goal : theory -> string -> (thm list -> tactic list) -> thm
+ val prlev : int -> unit
+ val prlim : int -> unit
+ val premises : unit -> thm list
+ val prin : term -> unit
+ val printyp : typ -> unit
+ val pprint_term : term -> pprint_args -> unit
+ val pprint_typ : typ -> pprint_args -> unit
+ val print_exn : exn -> 'a
+ val print_sign_exn : theory -> exn -> 'a
+ val prove_goal : theory -> string -> (thm list -> tactic list) -> thm
val prove_goalw : theory->thm list->string->(thm list->tactic list)->thm
- val prove_goalw_cterm : thm list->cterm->(thm list->tactic list)->thm
- val prove_goalw_cterm_nocheck : thm list->cterm->(thm list->tactic list)->thm
+ val prove_goalw_cterm : thm list->cterm->(thm list->tactic list)->thm
+ val prove_goalw_cterm_nocheck : thm list->cterm->(thm list->tactic list)->thm
val quick_and_dirty_prove_goalw_cterm: theory -> thm list -> cterm
-> (thm list -> tactic list) -> thm
val simple_prove_goal_cterm : cterm->(thm list->tactic list)->thm
- val push_proof : unit -> unit
- val read : string -> term
- val ren : string -> int -> unit
- val restore_proof : proof -> thm list
- val result : unit -> thm
+ val push_proof : unit -> unit
+ val read : string -> term
+ val ren : string -> int -> unit
+ val restore_proof : proof -> thm list
+ val result : unit -> thm
val result_error_fn : (thm -> string -> thm) ref
- val rotate_proof : unit -> thm list
- val uresult : unit -> thm
- val save_proof : unit -> proof
- val topthm : unit -> thm
- val undo : unit -> unit
+ val rotate_proof : unit -> thm list
+ val uresult : unit -> thm
+ val save_proof : unit -> proof
+ val topthm : unit -> thm
+ val undo : unit -> unit
val bind_thm : string * thm -> unit
val bind_thms : string * thm list -> unit
val qed : string -> unit
@@ -112,7 +112,7 @@
val open_locale: xstring -> theory -> theory
val close_locale: xstring -> theory -> theory
val print_scope: theory -> unit
- val read_cterm: Sign.sg -> string * typ -> cterm
+ val read_cterm: theory -> string * typ -> cterm
end;
structure Goals: GOALS =
@@ -125,11 +125,11 @@
locale Locale_name =
fixes (*variables that are fixed in the locale's scope*)
- v :: T
+ v :: T
assumes (*meta-hypothesis that hold in the locale*)
- Asm_name "meta-formula"
+ Asm_name "meta-formula"
defines (*local definitions of fixed variables in terms of others*)
- v_def "v x == ...x..."
+ v_def "v x == ...x..."
*)
(** type locale **)
@@ -144,13 +144,13 @@
defaults: (string * sort) list * (string * typ) list * string list};
fun make_locale ancestor consts nosyn rules defs thms defaults =
- {ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules,
+ {ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules,
defs = defs, thms = thms, defaults = defaults}: locale;
-fun pretty_locale sg (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
+fun pretty_locale thy (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
let
- val prt_typ = Pretty.quote o Sign.pretty_typ sg;
- val prt_term = Pretty.quote o Sign.pretty_term sg;
+ val prt_typ = Pretty.quote o Sign.pretty_typ thy;
+ val prt_term = Pretty.quote o Sign.pretty_term thy;
fun pretty_const (c, T) = Pretty.block
[Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ T];
@@ -182,48 +182,43 @@
fun make_locale_data space locales scope =
{space = space, locales = locales, scope = scope}: locale_data;
-structure LocalesArgs =
-struct
+structure LocalesData = TheoryDataFun
+(struct
val name = "Pure/old-locales";
type T = locale_data;
val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
- fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
- fun merge ({space = space1, locales = locales1, scope = _},
+ fun extend {space, locales, scope = _} = make_locale_data space locales (ref []);
+ fun merge _ ({space = space1, locales = locales1, scope = _},
{space = space2, locales = locales2, scope = _}) =
make_locale_data (NameSpace.merge (space1, space2))
(Symtab.merge (K true) (locales1, locales2))
(ref []);
- fun print sg {space, locales, scope} =
+ fun print thy {space, locales, scope} =
let
val locs = NameSpace.extern_table (space, locales);
val scope_names = rev (map (NameSpace.extern space o fst) (! scope));
in
- [Display.pretty_name_space ("locale name space", space),
- Pretty.big_list "locales:" (map (pretty_locale sg) locs),
+ [Pretty.big_list "locales:" (map (pretty_locale thy) locs),
Pretty.strs ("current scope:" :: scope_names)]
|> Pretty.chunks |> Pretty.writeln
end;
-end;
+end);
-
-structure LocalesData = TheoryDataFun(LocalesArgs);
val _ = Context.add_setup [LocalesData.init];
val print_locales = LocalesData.print;
(* access locales *)
-fun get_locale_sg sg name = Symtab.lookup (#locales (LocalesData.get_sg sg), name);
-
-val get_locale = get_locale_sg o Theory.sign_of;
+fun get_locale thy name = Symtab.lookup (#locales (LocalesData.get thy), name);
fun put_locale (name, locale) thy =
let
val {space, locales, scope} = LocalesData.get thy;
- val space' = Sign.declare_name (Theory.sign_of thy) name space;
+ val space' = Sign.declare_name thy name space;
val locales' = Symtab.update ((name, locale), locales);
in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
@@ -236,11 +231,9 @@
(* access scope *)
-fun get_scope_sg sg =
- if Sign.eq_sg (sg, Theory.sign_of ProtoPure.thy) then []
- else ! (#scope (LocalesData.get_sg sg));
-
-val get_scope = get_scope_sg o Theory.sign_of;
+fun get_scope thy =
+ if eq_thy (thy, ProtoPure.thy) then []
+ else ! (#scope (LocalesData.get thy));
fun change_scope f thy =
let val {scope, ...} = LocalesData.get thy
@@ -264,26 +257,26 @@
fun opn lc th = (change_scope (cons lc) th; th)
in case anc of
NONE => opn loc thy
- | SOME(loc') =>
- if loc' mem (map fst cur_sc)
+ | SOME(loc') =>
+ if loc' mem (map fst cur_sc)
then opn loc thy
- else (warning ("Opening locale " ^ quote loc' ^ ", required by " ^
- quote xname);
+ else (warning ("Opening locale " ^ quote loc' ^ ", required by " ^
+ quote xname);
opn loc (open_locale (Sign.base_name loc') thy))
end;
fun pop_locale [] = error "Currently no open locales"
| pop_locale (_ :: locs) = locs;
-fun close_locale name thy =
+fun close_locale name thy =
let val lname = (case get_scope thy of (ln,_)::_ => ln
| _ => error "No locales are open!")
- val ok = (name = Sign.base_name lname) handle _ => false
+ val ok = name = Sign.base_name lname
in if ok then (change_scope pop_locale thy; thy)
else error ("locale " ^ name ^ " is not top of scope; top is " ^ lname)
end;
-fun print_scope thy =
+fun print_scope thy =
Pretty.writeln (Pretty.strs ("current scope:" :: rev(map (Sign.base_name o fst) (get_scope thy))));
(*implicit context versions*)
@@ -295,11 +288,10 @@
(** functions for goals.ML **)
(* in_locale: check if hyps (: term list) of a proof are contained in the
- (current) scope. This function is needed in prepare_proof. It needs to
- refer to the signature, because theory is not available in prepare_proof. *)
+ (current) scope. This function is needed in prepare_proof. *)
-fun in_locale hyps sg =
- let val cur_sc = get_scope_sg sg;
+fun in_locale hyps thy =
+ let val cur_sc = get_scope thy;
val rule_lists = map (#rules o snd) cur_sc;
val def_lists = map (#defs o snd) cur_sc;
val rules = map snd (foldr (op union) [] rule_lists);
@@ -311,12 +303,10 @@
(* is_open_loc: check if any locale is open, i.e. in the scope of the current thy *)
-fun is_open_loc_sg sign =
- let val cur_sc = get_scope_sg sign
+fun is_open_loc thy =
+ let val cur_sc = get_scope thy
in not(null(cur_sc)) end;
-val is_open_loc = is_open_loc_sg o Theory.sign_of;
-
(* get theorems *)
@@ -336,7 +326,7 @@
(* get the defaults of a locale, for extension *)
-fun get_defaults thy name =
+fun get_defaults thy name =
let val (lname, loc) = the_locale thy name;
in #defaults(loc)
end;
@@ -346,15 +336,15 @@
(* prepare types *)
-fun read_typ sg (envT, s) =
+fun read_typ thy (envT, s) =
let
fun def_sort (x, ~1) = assoc (envT, x)
| def_sort _ = NONE;
- val T = Type.no_tvars (Sign.read_typ (sg, def_sort) s) handle TYPE (msg, _, _) => error msg;
+ val T = Type.no_tvars (Sign.read_typ (thy, def_sort) s) handle TYPE (msg, _, _) => error msg;
in (Term.add_typ_tfrees (T, envT), T) end;
-fun cert_typ sg (envT, raw_T) =
- let val T = Type.no_tvars (Sign.certify_typ sg raw_T) handle TYPE (msg, _, _) => error msg
+fun cert_typ thy (envT, raw_T) =
+ let val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg
in (Term.add_typ_tfrees (T, envT), T) end;
@@ -365,20 +355,20 @@
fun enter_term t (envS, envT, used) =
(Term.add_term_tfrees (t, envS), add_frees (envT, t), Term.add_term_tfree_names (t, used));
-fun read_axm sg ((envS, envT, used), (name, s)) =
+fun read_axm thy ((envS, envT, used), (name, s)) =
let
fun def_sort (x, ~1) = assoc (envS, x)
| def_sort _ = NONE;
fun def_type (x, ~1) = assoc (envT, x)
| def_type _ = NONE;
- val (_, t) = Theory.read_def_axm (sg, def_type, def_sort) used (name, s);
+ val (_, t) = Theory.read_def_axm (thy, def_type, def_sort) used (name, s);
in
(enter_term t (envS, envT, used), t)
end;
-fun cert_axm sg ((envS, envT, used), (name, raw_t)) =
- let val (_, t) = Theory.cert_axm sg (name, raw_t)
+fun cert_axm thy ((envS, envT, used), (name, raw_t)) =
+ let val (_, t) = Theory.cert_axm thy (name, raw_t)
in (enter_term t (envS, envT, used), t) end;
@@ -386,8 +376,8 @@
that already exist for subterms. If no locale is open, this function is equal to
Thm.read_cterm *)
-fun read_cterm sign =
- let val cur_sc = get_scope_sg sign;
+fun read_cterm thy =
+ let val cur_sc = get_scope thy;
val defaults = map (#defaults o snd) cur_sc;
val envS = List.concat (map #1 defaults);
val envT = List.concat (map #2 defaults);
@@ -396,15 +386,15 @@
| def_sort _ = NONE;
fun def_type (x, ~1) = assoc (envT, x)
| def_type _ = NONE;
- in (if (is_open_loc_sg sign)
- then (#1 o read_def_cterm (sign, def_type, def_sort) used true)
- else Thm.read_cterm sign)
+ in (if (is_open_loc thy)
+ then (#1 o read_def_cterm (thy, def_type, def_sort) used true)
+ else Thm.read_cterm thy)
end;
(* basic functions needed for definitions and display *)
(* collect all locale constants of a scope, i.e. a list of locales *)
-fun collect_consts sg =
- let val cur_sc = get_scope_sg sg;
+fun collect_consts thy =
+ let val cur_sc = get_scope thy;
val locale_list = map snd cur_sc;
val const_list = List.concat (map #consts locale_list)
in map fst const_list end;
@@ -447,7 +437,7 @@
(* assume a definition, i.e assume the cterm of a definiton term and then eliminate
the binding !!, so that the def can be applied as rewrite. The meta hyp will still contain !! *)
-fun prep_hyps clist sg = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of sg);
+fun prep_hyps clist thy = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of thy);
(* concrete syntax *)
@@ -460,21 +450,20 @@
(* add_locale *)
fun gen_add_locale prep_typ prep_term bname bancestor raw_consts raw_rules raw_defs thy =
- let val sign = Theory.sign_of thy;
+ let
+ val name = Sign.full_name thy bname;
- val name = Sign.full_name sign bname;
-
- val (envSb, old_loc_consts, _) =
+ val (envSb, old_loc_consts, _) =
case bancestor of
SOME(loc) => (get_defaults thy loc)
| NONE => ([],[],[]);
- val old_nosyn = case bancestor of
+ val old_nosyn = case bancestor of
SOME(loc) => #nosyn(#2(the_locale thy loc))
| NONE => [];
(* Get the full name of the ancestor *)
- val ancestor = case bancestor of
+ val ancestor = case bancestor of
SOME(loc) => SOME(#1(the_locale thy loc))
| NONE => NONE;
@@ -485,7 +474,7 @@
val c = Syntax.const_name raw_c raw_mx;
val c_syn = mark_syn c;
val mx = Syntax.fix_mixfix raw_c raw_mx;
- val (envS', T) = prep_typ sign (envS, raw_T) handle ERROR =>
+ val (envS', T) = prep_typ thy (envS, raw_T) handle ERROR =>
error ("The error(s) above occured in locale constant " ^ quote c);
val trfun = if mx = Syntax.NoSyn then NONE else SOME (c_syn, mk_loc_tr c);
in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
@@ -505,38 +494,36 @@
|> Theory.add_modesyntax_i Syntax.default_mode loc_syn
|> Theory.add_trfuns ([], loc_trfuns, [], []);
- val syntax_sign = Theory.sign_of syntax_thy;
-
(* prepare rules and defs *)
fun prep_axiom (env, (a, raw_t)) =
let
- val (env', t) = prep_term syntax_sign (env, (a, raw_t)) handle ERROR =>
+ val (env', t) = prep_term syntax_thy (env, (a, raw_t)) handle ERROR =>
error ("The error(s) above occured in locale rule / definition " ^ quote a);
in (env', (a, t)) end;
val ((envS1, envT1, used1), loc_rules) =
foldl_map prep_axiom ((envS0, loc_consts, map fst envS0), raw_rules);
- val (defaults, loc_defs) =
- foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
+ val (defaults, loc_defs) =
+ foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
- val old_loc_consts = collect_consts syntax_sign;
+ val old_loc_consts = collect_consts syntax_thy;
val new_loc_consts = (map #1 loc_consts);
val all_loc_consts = old_loc_consts @ new_loc_consts;
- val (defaults, loc_defs_terms) =
- foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
- val loc_defs_thms =
- map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) loc_defs_terms;
- val (defaults, loc_thms_terms) =
- foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
- val loc_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign))
- (loc_thms_terms)
+ val (defaults, loc_defs_terms) =
+ foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
+ val loc_defs_thms =
+ map (apsnd (prep_hyps (map #1 loc_consts) syntax_thy)) loc_defs_terms;
+ val (defaults, loc_thms_terms) =
+ foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
+ val loc_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_thy))
+ (loc_thms_terms)
@ loc_defs_thms;
- (* error messages *)
+ (* error messages *)
fun locale_error msg = error (msg ^ "\nFor locale " ^ quote name);
@@ -544,31 +531,31 @@
if is_none (get_locale thy name) then []
else ["Duplicate definition of locale " ^ quote name];
- (* check if definientes are locale constants
+ (* check if definientes are locale constants
(in the same locale, so no redefining!) *)
val err_def_head =
- let fun peal_appl t =
- case t of
+ let fun peal_appl t =
+ case t of
t1 $ t2 => peal_appl t1
| Free(t) => t
| _ => locale_error ("Bad form of LHS in locale definition");
- fun lhs (_, Const ("==" , _) $ d1 $ d2) = peal_appl d1
- | lhs _ = locale_error ("Definitions must use the == relation");
+ fun lhs (_, Const ("==" , _) $ d1 $ d2) = peal_appl d1
+ | lhs _ = locale_error ("Definitions must use the == relation");
val defs = map lhs loc_defs;
val check = defs subset loc_consts
- in if check then []
+ in if check then []
else ["defined item not declared fixed in locale " ^ quote name]
- end;
+ end;
(* check that variables on rhs of definitions are either fixed or on lhs *)
- val err_var_rhs =
- let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) =
- let val varl1 = difflist d1 all_loc_consts;
- val varl2 = difflist d2 all_loc_consts
- in t andalso (varl2 subset varl1)
- end
- | compare_var_sides (_,_) =
- locale_error ("Definitions must use the == relation")
+ val err_var_rhs =
+ let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) =
+ let val varl1 = difflist d1 all_loc_consts;
+ val varl2 = difflist d2 all_loc_consts
+ in t andalso (varl2 subset varl1)
+ end
+ | compare_var_sides (_,_) =
+ locale_error ("Definitions must use the == relation")
val check = Library.foldl compare_var_sides (true, loc_defs)
in if check then []
else ["nonfixed variable on right hand side of a locale definition in locale " ^ quote name]
@@ -580,8 +567,8 @@
else error (cat_lines errs);
syntax_thy
- |> put_locale (name,
- make_locale ancestor loc_consts nosyn loc_thms_terms
+ |> put_locale (name,
+ make_locale ancestor loc_consts nosyn loc_thms_terms
loc_defs_terms loc_thms defaults)
end;
@@ -612,14 +599,14 @@
| const_ssubst_list (s :: l) t = const_ssubst_list l (const_ssubst t s);
(* pretty_term *)
-fun pretty_term sign =
- if (is_open_loc_sg sign) then
- let val locale_list = map snd(get_scope_sg sign);
+fun pretty_term thy =
+ if (is_open_loc thy) then
+ let val locale_list = map snd(get_scope thy);
val nosyn = List.concat (map #nosyn locale_list);
- val str_list = (collect_consts sign) \\ nosyn
- in Sign.pretty_term sign o (const_ssubst_list str_list)
+ val str_list = (collect_consts thy) \\ nosyn
+ in Sign.pretty_term thy o (const_ssubst_list str_list)
end
- else Sign.pretty_term sign;
+ else Sign.pretty_term thy;
@@ -644,10 +631,9 @@
fun init_mkresult _ = error "No goal has been supplied in subgoal module";
val curr_mkresult = ref (init_mkresult: bool*thm->thm);
-val dummy = trivial(read_cterm (Theory.sign_of ProtoPure.thy)
- ("PROP No_goal_has_been_supplied",propT));
+val dummy = Thm.trivial (read_cterm ProtoPure.thy ("PROP No_goal_has_been_supplied", propT));
-(*List of previous goal stacks, for the undo operation. Set by setstate.
+(*List of previous goal stacks, for the undo operation. Set by setstate.
A list of lists!*)
val undo_list = ref([[(dummy, Seq.empty)]] : gstack list);
@@ -662,9 +648,9 @@
(*** Setting up goal-directed proof ***)
-(*Generates the list of new theories when the proof state's signature changes*)
-fun sign_error (sign,sign') =
- let val names = Sign.stamp_names_of sign' \\ Sign.stamp_names_of sign
+(*Generates the list of new theories when the proof state's theory changes*)
+fun thy_error (thy,thy') =
+ let val names = Context.names_of thy' \\ Context.names_of thy
in case names of
[name] => "\nNew theory: " ^ name
| _ => "\nNew theories: " ^ space_implode ", " names
@@ -689,23 +675,22 @@
end;
(** exporting a theorem out of a locale means turning all meta-hyps into assumptions
- and expand and cancel the locale definitions.
+ and expand and cancel the locale definitions.
export goes through all levels in case of nested locales, whereas
export_thy just goes one up. **)
-fun get_top_scope_thms thy =
- let val sc = (get_scope_sg (Theory.sign_of thy))
- in if (null sc) then (warning "No locale in theory"; [])
+fun get_top_scope_thms thy =
+ let val sc = get_scope thy
+ in if null sc then (warning "No locale in theory"; [])
else map Thm.prop_of (map #2 (#thms(snd(hd sc))))
end;
-fun implies_intr_some_hyps thy A_set th =
- let
- val sign = Theory.sign_of thy;
+fun implies_intr_some_hyps thy A_set th =
+ let
val used_As = A_set inter #hyps(rep_thm(th));
- val ctl = map (cterm_of sign) used_As
+ val ctl = map (cterm_of thy) used_As
in Library.foldl (fn (x, y) => Thm.implies_intr y x) (th, ctl)
- end;
+ end;
fun standard_some thy A_set th =
let val {maxidx,...} = rep_thm th
@@ -716,7 +701,7 @@
|> zero_var_indexes |> Thm.varifyT |> Thm.compress
end;
-fun export_thy thy th =
+fun export_thy thy th =
let val A_set = get_top_scope_thms thy
in
standard_some thy [] (Seq.hd ((REPEAT (FIRSTGOAL (rtac reflexive_thm))) (standard_some thy A_set th)))
@@ -733,107 +718,106 @@
"Goal::prop=>prop" to avoid assumptions being returned separately.
*)
fun prepare_proof atomic rths chorn =
- let val {sign, t=horn,...} = rep_cterm chorn;
+ let val {thy, t=horn,...} = rep_cterm chorn;
val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
val (As, B) = Logic.strip_horn horn;
val atoms = atomic andalso
forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
val (As,B) = if atoms then ([],horn) else (As,B);
- val cAs = map (cterm_of sign) As;
+ val cAs = map (cterm_of thy) As;
val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs;
- val cB = cterm_of sign B;
+ val cB = cterm_of thy B;
val st0 = let val st = Drule.impose_hyps cAs (Drule.mk_triv_goal cB)
in rewrite_goals_rule rths st end
(*discharges assumptions from state in the order they appear in goal;
- checks (if requested) that resulting theorem is equivalent to goal. *)
+ checks (if requested) that resulting theorem is equivalent to goal. *)
fun mkresult (check,state) =
let val state = Seq.hd (flexflex_rule state)
- handle THM _ => state (*smash flexflex pairs*)
- val ngoals = nprems_of state
+ handle THM _ => state (*smash flexflex pairs*)
+ val ngoals = nprems_of state
val ath = implies_intr_list cAs state
val th = ath RS Drule.rev_triv_goal
- val {hyps,prop,sign=sign',...} = rep_thm th
+ val {hyps,prop,thy=thy',...} = rep_thm th
val final_th = if (null(hyps)) then standard th else varify th
in if not check then final_th
- else if not (Sign.eq_sg(sign,sign')) then !result_error_fn state
- ("Signature of proof state has changed!" ^
- sign_error (sign,sign'))
+ else if not (eq_thy(thy,thy')) then !result_error_fn state
+ ("Theory of proof state has changed!" ^
+ thy_error (thy,thy'))
else if ngoals>0 then !result_error_fn state
- (string_of_int ngoals ^ " unsolved goals!")
- else if (not (null hyps) andalso (not (in_locale hyps sign)))
- then !result_error_fn state
- ("Additional hypotheses:\n" ^
- cat_lines
- (map (Sign.string_of_term sign)
- (List.filter (fn x => (not (in_locale [x] sign)))
- hyps)))
- else if Pattern.matches (Sign.tsig_of sign)
- (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
- then final_th
- else !result_error_fn state "proved a different theorem"
+ (string_of_int ngoals ^ " unsolved goals!")
+ else if (not (null hyps) andalso (not (in_locale hyps thy)))
+ then !result_error_fn state
+ ("Additional hypotheses:\n" ^
+ cat_lines
+ (map (Sign.string_of_term thy)
+ (List.filter (fn x => (not (in_locale [x] thy)))
+ hyps)))
+ else if Pattern.matches (Sign.tsig_of thy)
+ (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
+ then final_th
+ else !result_error_fn state "proved a different theorem"
end
in
- if Sign.eq_sg(sign, Thm.sign_of_thm st0)
+ if eq_thy(thy, Thm.theory_of_thm st0)
then (prems, st0, mkresult)
- else error ("Definitions would change the proof state's signature" ^
- sign_error (sign, Thm.sign_of_thm st0))
+ else error ("Definitions would change the proof state's theory" ^
+ thy_error (thy, Thm.theory_of_thm st0))
end
handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s);
(*Prints exceptions readably to users*)
-fun print_sign_exn_unit sign e =
+fun print_sign_exn_unit thy e =
case e of
THM (msg,i,thms) =>
- (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
- List.app print_thm thms)
+ (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
+ List.app print_thm thms)
| THEORY (msg,thys) =>
- (writeln ("Exception THEORY raised:\n" ^ msg);
- List.app (Pretty.writeln o Display.pretty_theory) thys)
+ (writeln ("Exception THEORY raised:\n" ^ msg);
+ List.app (writeln o Context.str_of_thy) thys)
| TERM (msg,ts) =>
- (writeln ("Exception TERM raised:\n" ^ msg);
- List.app (writeln o Sign.string_of_term sign) ts)
+ (writeln ("Exception TERM raised:\n" ^ msg);
+ List.app (writeln o Sign.string_of_term thy) ts)
| TYPE (msg,Ts,ts) =>
- (writeln ("Exception TYPE raised:\n" ^ msg);
- List.app (writeln o Sign.string_of_typ sign) Ts;
- List.app (writeln o Sign.string_of_term sign) ts)
+ (writeln ("Exception TYPE raised:\n" ^ msg);
+ List.app (writeln o Sign.string_of_typ thy) Ts;
+ List.app (writeln o Sign.string_of_term thy) ts)
| e => raise e;
(*Prints an exception, then fails*)
-fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise ERROR);
+fun print_sign_exn thy e = (print_sign_exn_unit thy e; raise ERROR);
(** the prove_goal.... commands
Prove theorem using the listed tactics; check it has the specified form.
- Augment signature with all type assignments of goal.
+ Augment theory with all type assignments of goal.
Syntax is similar to "goal" command for easy keyboard use. **)
(*Version taking the goal as a cterm*)
fun prove_goalw_cterm_general check rths chorn tacsf =
let val (prems, st0, mkresult) = prepare_proof false rths chorn
val tac = EVERY (tacsf prems)
- fun statef() =
- (case Seq.pull (tac st0) of
- SOME(st,_) => st
- | _ => error ("prove_goal: tactic failed"))
+ fun statef() =
+ (case Seq.pull (tac st0) of
+ SOME(st,_) => st
+ | _ => error ("prove_goal: tactic failed"))
in mkresult (check, cond_timeit (!Output.timing) statef) end
- handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
- writeln ("The exception above was raised for\n" ^
- Display.string_of_cterm chorn); raise e);
+ handle e => (print_sign_exn_unit (#thy (rep_cterm chorn)) e;
+ writeln ("The exception above was raised for\n" ^
+ Display.string_of_cterm chorn); raise e);
-(*Two variants: one checking the result, one not.
+(*Two variants: one checking the result, one not.
Neither prints runtime messages: they are for internal packages.*)
-fun prove_goalw_cterm rths chorn =
- setmp Output.timing false (prove_goalw_cterm_general true rths chorn)
-and prove_goalw_cterm_nocheck rths chorn =
- setmp Output.timing false (prove_goalw_cterm_general false rths chorn);
+fun prove_goalw_cterm rths chorn =
+ setmp Output.timing false (prove_goalw_cterm_general true rths chorn)
+and prove_goalw_cterm_nocheck rths chorn =
+ setmp Output.timing false (prove_goalw_cterm_general false rths chorn);
(*Version taking the goal as a string*)
fun prove_goalw thy rths agoal tacsf =
- let val sign = Theory.sign_of thy
- val chorn = read_cterm sign (agoal,propT)
- in prove_goalw_cterm_general true rths chorn tacsf end
+ let val chorn = read_cterm thy (agoal, propT)
+ in prove_goalw_cterm_general true rths chorn tacsf end
handle ERROR => error (*from read_cterm?*)
- ("The error(s) above occurred for " ^ quote agoal);
+ ("The error(s) above occurred for " ^ quote agoal);
(*String version with no meta-rewrite-rules*)
fun prove_goal thy = prove_goalw thy [];
@@ -847,7 +831,7 @@
(*** Commands etc ***)
(*Return the current goal stack, if any, from undo_list*)
-fun getstate() : gstack = case !undo_list of
+fun getstate() : gstack = case !undo_list of
[] => error"No current state in subgoal module"
| x::_ => x;
@@ -868,7 +852,7 @@
(*Printing can raise exceptions, so the assignment occurs last.
Can do setstate[(st,Seq.empty)] to set st as the state. *)
-fun setstate newgoals =
+fun setstate newgoals =
(print_top (pop newgoals); undo_list := newgoals :: !undo_list);
(*Given a proof state transformation, return a command that updates
@@ -895,7 +879,7 @@
For debugging uses of METAHYPS*)
local exception GETHYPS of thm list
in
-fun gethyps i =
+fun gethyps i =
(METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm()); [])
handle GETHYPS hyps => hyps
end;
@@ -904,14 +888,14 @@
fun filter_goal could ths i = filter_thms could (999, getgoal i, ths);
(*For inspecting earlier levels of the backward proof*)
-fun chop_level n (pair,pairs) =
+fun chop_level n (pair,pairs) =
let val level = length pairs
in if n<0 andalso ~n <= level
- then List.drop (pair::pairs, ~n)
+ then List.drop (pair::pairs, ~n)
else if 0<=n andalso n<= level
- then List.drop (pair::pairs, level - n)
- else error ("Level number must lie between 0 and " ^
- string_of_int level)
+ then List.drop (pair::pairs, level - n)
+ else error ("Level number must lie between 0 and " ^
+ string_of_int level)
end;
(*Print the given level of the proof; prlev ~1 prints previous level*)
@@ -922,15 +906,15 @@
fun prlim n = (goals_limit:=n; pr());
(** the goal.... commands
- Read main goal. Set global variables curr_prems, curr_mkresult.
+ Read main goal. Set global variables curr_prems, curr_mkresult.
Initial subgoal and premises are rewritten using rths. **)
(*Version taking the goal as a cterm; if you have a term t and theory thy, use
- goalw_cterm rths (cterm_of (Theory.sign_of thy) t); *)
-fun agoalw_cterm atomic rths chorn =
+ goalw_cterm rths (cterm_of thy t); *)
+fun agoalw_cterm atomic rths chorn =
let val (prems, st0, mkresult) = prepare_proof atomic rths chorn
in undo_list := [];
- setstate [ (st0, Seq.empty) ];
+ setstate [ (st0, Seq.empty) ];
curr_prems := prems;
curr_mkresult := mkresult;
prems
@@ -939,10 +923,10 @@
val goalw_cterm = agoalw_cterm false;
(*Version taking the goal as a string*)
-fun agoalw atomic thy rths agoal =
- agoalw_cterm atomic rths (read_cterm(Theory.sign_of thy)(agoal,propT))
+fun agoalw atomic thy rths agoal =
+ agoalw_cterm atomic rths (read_cterm thy (agoal, propT))
handle ERROR => error (*from type_assign, etc via prepare_proof*)
- ("The error(s) above occurred for " ^ quote agoal);
+ ("The error(s) above occurred for " ^ quote agoal);
val goalw = agoalw false;
@@ -978,15 +962,15 @@
fun by_com tac ((th,ths), pairs) : gstack =
(case Seq.pull(tac th) of
NONE => error"by: tactic failed"
- | SOME(th2,ths2) =>
- (if eq_thm(th,th2)
- then warning "Warning: same as previous level"
- else if eq_thm_sg(th,th2) then ()
- else warning ("Warning: signature of proof state has changed" ^
- sign_error (Thm.sign_of_thm th, Thm.sign_of_thm th2));
+ | SOME(th2,ths2) =>
+ (if eq_thm(th,th2)
+ then warning "Warning: same as previous level"
+ else if eq_thm_thy(th,th2) then ()
+ else warning ("Warning: theory of proof state has changed" ^
+ thy_error (Thm.theory_of_thm th, Thm.theory_of_thm th2));
((th2,ths2)::(th,ths)::pairs)));
-fun by tac = cond_timeit (!Output.timing)
+fun by tac = cond_timeit (!Output.timing)
(fn() => make_command (by_com tac));
(* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.
@@ -999,13 +983,13 @@
fun backtrack [] = error"back: no alternatives"
| backtrack ((th,thstr) :: pairs) =
(case Seq.pull thstr of
- NONE => (writeln"Going back a level..."; backtrack pairs)
- | SOME(th2,thstr2) =>
- (if eq_thm(th,th2)
- then warning "Warning: same as previous choice at this level"
- else if eq_thm_sg(th,th2) then ()
- else warning "Warning: signature of proof state has changed";
- (th2,thstr2)::pairs));
+ NONE => (writeln"Going back a level..."; backtrack pairs)
+ | SOME(th2,thstr2) =>
+ (if eq_thm(th,th2)
+ then warning "Warning: same as previous choice at this level"
+ else if eq_thm_thy(th,th2) then ()
+ else warning "Warning: theory of proof state has changed";
+ (th2,thstr2)::pairs));
fun back() = setstate (backtrack (getstate()));
@@ -1031,25 +1015,25 @@
fun top_proof() = case !proofstack of
- [] => error("Stack of proof attempts is empty!")
+ [] => error("Stack of proof attempts is empty!")
| p::ps => (p,ps);
(* push a copy of the current proof state on to the stack *)
fun push_proof() = (proofstack := (save_proof() :: !proofstack));
(* discard the top proof state of the stack *)
-fun pop_proof() =
+fun pop_proof() =
let val (p,ps) = top_proof()
val prems = restore_proof p
in proofstack := ps; pr(); prems end;
(* rotate the stack so that the top element goes to the bottom *)
fun rotate_proof() = let val (p,ps) = top_proof()
- in proofstack := ps@[save_proof()];
- restore_proof p;
- pr();
- !curr_prems
- end;
+ in proofstack := ps@[save_proof()];
+ restore_proof p;
+ pr();
+ !curr_prems
+ end;
(** Shortcuts for commonly-used tactics **)
@@ -1085,11 +1069,11 @@
(** Reading and printing terms wrt the current theory **)
-fun top_sg() = Thm.sign_of_thm (topthm());
+fun top_sg() = Thm.theory_of_thm (topthm());
fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT));
-(*Print a term under the current signature of the proof state*)
+(*Print a term under the current theory of the proof state*)
fun prin t = writeln (Sign.string_of_term (top_sg()) t);
fun printyp T = writeln (Sign.string_of_typ (top_sg()) T);
@@ -1099,7 +1083,7 @@
fun pprint_typ T = Sign.pprint_typ (top_sg()) T;
-(*Prints exceptions nicely at top level;
+(*Prints exceptions nicely at top level;
raises the exception in order to have a polymorphic type!*)
fun print_exn e = (print_sign_exn_unit (top_sg()) e; raise e);
@@ -1128,15 +1112,15 @@
(* retrieval *)
-fun theory_of_goal () = ThyInfo.theory_of_sign (Thm.sign_of_thm (topthm ()));
+fun theory_of_goal () = Thm.theory_of_thm (topthm ());
val context_of_goal = ProofContext.init o theory_of_goal;
fun thms_containing raw_consts =
let
val thy = theory_of_goal ();
- val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
+ val consts = map (Sign.intern_const thy) raw_consts;
in
- (case List.filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of
+ (case List.filter (is_none o Sign.const_type thy) consts of
[] => ()
| cs => error ("thms_containing: undeclared consts " ^ commas_quote cs));
PureThy.thms_containing_consts thy consts
--- a/src/Pure/meta_simplifier.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Pure/meta_simplifier.ML Fri Jun 17 18:35:27 2005 +0200
@@ -42,7 +42,7 @@
val merge_ss: simpset * simpset -> simpset
type simproc
val mk_simproc: string -> cterm list ->
- (Sign.sg -> simpset -> term -> thm option) -> simproc
+ (theory -> simpset -> term -> thm option) -> simproc
val add_prems: thm list -> simpset -> simpset
val prems_of_ss: simpset -> thm list
val addsimps: simpset * thm list -> simpset
@@ -75,15 +75,15 @@
exception SIMPLIFIER of string * thm
val clear_ss: simpset -> simpset
exception SIMPROC_FAIL of string * exn
- val simproc_i: Sign.sg -> string -> term list
- -> (Sign.sg -> simpset -> term -> thm option) -> simproc
- val simproc: Sign.sg -> string -> string list
- -> (Sign.sg -> simpset -> term -> thm option) -> simproc
+ val simproc_i: theory -> string -> term list
+ -> (theory -> simpset -> term -> thm option) -> simproc
+ val simproc: theory -> string -> string list
+ -> (theory -> simpset -> term -> thm option) -> simproc
val rewrite_cterm: bool * bool * bool ->
(simpset -> thm -> thm option) -> simpset -> cterm -> thm
val rewrite_aux: (simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
val simplify_aux: (simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
- val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term
+ val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
val rewrite_thm: bool * bool * bool ->
(simpset -> thm -> thm option) -> simpset -> thm -> thm
val rewrite_goals_rule_aux: (simpset -> thm -> thm option) -> thm list -> thm -> thm
@@ -116,7 +116,7 @@
else tracing (enclose "[" "]" (string_of_int(!simp_depth)) ^ a);
fun prnt warn a = if warn then warning a else println a;
-fun prtm warn a sg t = prnt warn (a ^ "\n" ^ Sign.string_of_term sg t);
+fun prtm warn a thy t = prnt warn (a ^ "\n" ^ Sign.string_of_term thy t);
fun prctm warn a t = prnt warn (a ^ "\n" ^ Display.string_of_cterm t);
in
@@ -124,8 +124,8 @@
fun debug warn a = if ! debug_simp then prnt warn a else ();
fun trace warn a = if ! trace_simp then prnt warn a else ();
-fun debug_term warn a sign t = if ! debug_simp then prtm warn a sign t else ();
-fun trace_term warn a sign t = if ! trace_simp then prtm warn a sign t else ();
+fun debug_term warn a thy t = if ! debug_simp then prtm warn a thy t else ();
+fun trace_term warn a thy t = if ! trace_simp then prtm warn a thy t else ();
fun trace_cterm warn a ct = if ! trace_simp then prctm warn a ct else ();
fun trace_thm a th = if ! trace_simp then prctm false a (Thm.cprop_of th) else ();
@@ -231,7 +231,7 @@
Proc of
{name: string,
lhs: cterm,
- proc: Sign.sg -> simpset -> term -> thm option,
+ proc: theory -> simpset -> term -> thm option,
id: stamp};
fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = (id1 = id2);
@@ -354,8 +354,8 @@
Proc {name = name, lhs = lhs, proc = proc, id = id}))
end;
-fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg o Logic.varify);
-fun simproc sg name = simproc_i sg name o map (Sign.simple_read_term sg TypeInfer.logicT);
+fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
+fun simproc thy name = simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT);
@@ -407,7 +407,7 @@
not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems)));
(*simple test for looping rewrite rules and stupid orientations*)
-fun reorient sign prems lhs rhs =
+fun reorient thy prems lhs rhs =
rewrite_rule_extra_vars prems lhs rhs
orelse
is_Var (head_of lhs)
@@ -420,7 +420,7 @@
*)
exists (apl (lhs, Logic.occs)) (rhs :: prems)
orelse
- null prems andalso Pattern.matches (Sign.tsig_of sign) (lhs, rhs)
+ null prems andalso Pattern.matches (Sign.tsig_of thy) (lhs, rhs)
(*the condition "null prems" is necessary because conditional rewrites
with extra variables in the conditions may terminate although
the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
@@ -429,7 +429,7 @@
fun decomp_simp thm =
let
- val {sign, prop, ...} = Thm.rep_thm thm;
+ val {thy, prop, ...} = Thm.rep_thm thm;
val prems = Logic.strip_imp_prems prop;
val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
@@ -441,7 +441,7 @@
var_perm (term_of elhs, erhs) andalso
not (term_of elhs aconv erhs) andalso
not (is_Var (term_of elhs));
- in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end;
+ in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
fun decomp_simp' thm =
let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
@@ -476,10 +476,10 @@
end;
fun orient_rrule ss (thm, name) =
- let val (sign, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
+ let val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
- else if reorient sign prems lhs rhs then
- if reorient sign prems rhs lhs
+ else if reorient thy prems lhs rhs then
+ if reorient thy prems rhs lhs
then mk_eq_True ss (thm, name)
else
let val Simpset (_, {mk_rews = {mk_sym, ...}, ...}) = ss in
@@ -718,9 +718,9 @@
(symmetric (Drule.beta_eta_conversion (lhs_of thm'))) thm')
in if msg then trace_thm "SUCCEEDED" thm' else (); SOME thm'' end
handle THM _ =>
- let val {sign, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
+ let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
trace_thm "Proved wrong thm (Check subgoaler?)" thm';
- trace_term false "Should have proved:" sign prop0;
+ trace_term false "Should have proved:" thy prop0;
NONE
end;
@@ -773,16 +773,16 @@
IMPORTANT: rewrite rules must not introduce new Vars or TVars!
*)
-fun rewritec (prover, signt, maxt) ss t =
+fun rewritec (prover, thyt, maxt) ss t =
let
val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
val eta_thm = Thm.eta_conversion t;
val eta_t' = rhs_of eta_thm;
val eta_t = term_of eta_t';
- val tsigt = Sign.tsig_of signt;
+ val tsigt = Sign.tsig_of thyt;
fun rew {thm, name, lhs, elhs, fo, perm} =
let
- val {sign, prop, maxidx, ...} = rep_thm thm;
+ val {thy, prop, maxidx, ...} = rep_thm thm;
val (rthm, elhs') = if maxt = ~1 then (thm, elhs)
else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
@@ -837,9 +837,9 @@
fun proc_rews [] = NONE
| proc_rews (Proc {name, proc, lhs, ...} :: ps) =
if Pattern.matches tsigt (Thm.term_of lhs, Thm.term_of t) then
- (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
+ (debug_term false ("Trying procedure " ^ quote name ^ " on:") thyt eta_t;
case transform_failure (curry SIMPROC_FAIL name)
- (fn () => proc signt ss eta_t) () of
+ (fn () => proc thyt ss eta_t) () of
NONE => (debug false "FAILED"; proc_rews ps)
| SOME raw_thm =>
(trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
@@ -859,8 +859,8 @@
(* conversion to apply a congruence rule to a term *)
-fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
- let val sign = Thm.sign_of_thm cong
+fun congc (prover,thyt,maxt) {thm=cong,lhs=lhs} t =
+ let val thy = Thm.theory_of_thm cong
val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
val insts = Thm.cterm_match (rlhs, t)
@@ -889,20 +889,20 @@
fun transitive2 thm = transitive1 (SOME thm);
fun transitive3 thm = transitive1 thm o SOME;
-fun bottomc ((simprem, useprem, mutsimp), prover, sign, maxidx) =
+fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
let
fun botc skel ss t =
if is_Var skel then NONE
else
(case subc skel ss t of
some as SOME thm1 =>
- (case rewritec (prover, sign, maxidx) ss (rhs_of thm1) of
+ (case rewritec (prover, thy, maxidx) ss (rhs_of thm1) of
SOME (thm2, skel2) =>
transitive2 (transitive thm1 thm2)
(botc skel2 ss (rhs_of thm2))
| NONE => some)
| NONE =>
- (case rewritec (prover, sign, maxidx) ss t of
+ (case rewritec (prover, thy, maxidx) ss t of
SOME (thm2, skel2) => transitive2 thm2
(botc skel2 ss (rhs_of thm2))
| NONE => NONE))
@@ -957,7 +957,7 @@
(*post processing: some partial applications h t1 ... tj, j <= length ts,
may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
(let
- val thm = congc (prover ss, sign, maxidx) cong t0;
+ val thm = congc (prover ss, thy, maxidx) cong t0;
val t = getOpt (Option.map rhs_of thm, t0);
val (cl, cr) = Thm.dest_comb t
val dVar = Var(("", 0), dummyT)
@@ -1012,7 +1012,7 @@
val concl' =
Drule.mk_implies (prem, getOpt (Option.map rhs_of eq, concl));
val dprem = Option.map (curry (disch false) prem)
- in case rewritec (prover, sign, maxidx) ss' concl' of
+ in case rewritec (prover, thy, maxidx) ss' concl' of
NONE => rebuild prems concl' rrss asms ss (dprem eq)
| SOME (eq', _) => transitive2 (Library.foldl (disch false o swap)
(valOf (transitive3 (dprem eq) eq'), prems))
@@ -1096,8 +1096,8 @@
then warning ("Simplification depth " ^ string_of_int (!simp_depth))
else ();
trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
- let val {sign, t, maxidx, ...} = Thm.rep_cterm ct
- val res = bottomc (mode, prover, sign, maxidx) ss ct
+ let val {thy, t, maxidx, ...} = Thm.rep_cterm ct
+ val res = bottomc (mode, prover, thy, maxidx) ss ct
handle THM (s, _, thms) =>
error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
Pretty.string_of (Display.pretty_thms thms))
@@ -1115,8 +1115,8 @@
Drule.fconv_rule (rewrite_cterm (full, false, false) prover (empty_ss addsimps thms));
(*simple term rewriting -- no proof*)
-fun rewrite_term sg rules procs =
- Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs;
+fun rewrite_term thy rules procs =
+ Pattern.rewrite_term (Sign.tsig_of thy) (map decomp_simp' rules) procs;
fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss);
--- a/src/Pure/proofterm.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Pure/proofterm.ML Fri Jun 17 18:35:27 2005 +0200
@@ -95,7 +95,7 @@
val equal_elim : term -> term -> proof -> proof -> proof
val axm_proof : string -> term -> proof
val oracle_proof : string -> term -> proof
- val thm_proof : Sign.sg -> string * (string * string list) list ->
+ val thm_proof : theory -> string * (string * string list) list ->
term list -> term -> proof -> proof
val get_name_tags : term list -> term -> proof -> string * (string * string list) list
@@ -1093,21 +1093,19 @@
(* data kind 'Pure/proof' *)
-structure ProofArgs =
-struct
+structure ProofData = TheoryDataFun
+(struct
val name = "Pure/proof";
type T = ((proof * proof) list *
(string * (typ list -> proof -> proof option)) list);
val empty = ([], []);
val copy = I;
- val prep_ext = I;
- fun merge ((rules1, procs1), (rules2, procs2)) =
+ val extend = I;
+ fun merge _ ((rules1, procs1), (rules2, procs2)) =
(merge_lists rules1 rules2, merge_alists procs1 procs2);
fun print _ _ = ();
-end;
-
-structure ProofData = TheoryDataFun(ProofArgs);
+end);
val init = ProofData.init;
@@ -1119,7 +1117,7 @@
let val r = ProofData.get thy
in ProofData.put (fst r, ps @ snd r) thy end;
-fun thm_proof sign (name, tags) hyps prop prf =
+fun thm_proof thy (name, tags) hyps prop prf =
let
val prop = Logic.list_implies (hyps, prop);
val nvs = needed_vars prop;
@@ -1127,7 +1125,7 @@
if ixn mem nvs then SOME v else NONE) (vars_of prop) @
map SOME (sort (make_ord atless) (term_frees prop));
val opt_prf = if ! proofs = 2 then
- #4 (shrink [] 0 (rewrite_prf fst (ProofData.get_sg sign)
+ #4 (shrink [] 0 (rewrite_prf fst (ProofData.get thy)
(foldr (uncurry implies_intr_proof) prf hyps)))
else MinProof (mk_min_proof ([], prf));
val head = (case strip_combt (fst (strip_combP prf)) of
--- a/src/Pure/simplifier.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Pure/simplifier.ML Fri Jun 17 18:35:27 2005 +0200
@@ -22,9 +22,9 @@
val mk_context_simproc: string -> cterm list ->
(Proof.context -> simpset -> term -> thm option) -> context_simproc
val print_simpset: theory -> unit
- val simpset_ref_of_sg: Sign.sg -> simpset ref
+ val simpset_ref_of_sg: theory -> simpset ref (*obsolete*)
val simpset_ref_of: theory -> simpset ref
- val simpset_of_sg: Sign.sg -> simpset
+ val simpset_of_sg: theory -> simpset (*obsolete*)
val simpset_of: theory -> simpset
val SIMPSET: (simpset -> tactic) -> tactic
val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
@@ -58,13 +58,13 @@
signature SIMPLIFIER =
sig
include BASIC_SIMPLIFIER
- val simproc_i: Sign.sg -> string -> term list
- -> (Sign.sg -> simpset -> term -> thm option) -> simproc
- val simproc: Sign.sg -> string -> string list
- -> (Sign.sg -> simpset -> term -> thm option) -> simproc
- val context_simproc_i: Sign.sg -> string -> term list
+ val simproc_i: theory -> string -> term list
+ -> (theory -> simpset -> term -> thm option) -> simproc
+ val simproc: theory -> string -> string list
+ -> (theory -> simpset -> term -> thm option) -> simproc
+ val context_simproc_i: theory -> string -> term list
-> (Proof.context -> simpset -> term -> thm option) -> context_simproc
- val context_simproc: Sign.sg -> string -> string list
+ val context_simproc: theory -> string -> string list
-> (Proof.context -> simpset -> term -> thm option) -> context_simproc
val rewrite: simpset -> cterm -> thm
val asm_rewrite: simpset -> cterm -> thm
@@ -130,11 +130,11 @@
fun eq_context_simproc (ContextSimproc (_, id1), ContextSimproc (_, id2)) = (id1 = id2);
val merge_context_simprocs = gen_merge_lists eq_context_simproc;
-fun context_simproc_i sg name =
- mk_context_simproc name o map (Thm.cterm_of sg o Logic.varify);
+fun context_simproc_i thy name =
+ mk_context_simproc name o map (Thm.cterm_of thy o Logic.varify);
-fun context_simproc sg name =
- context_simproc_i sg name o map (Sign.simple_read_term sg TypeInfer.logicT);
+fun context_simproc thy name =
+ context_simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT);
(* datatype context_ss *)
@@ -188,25 +188,24 @@
(* theory data kind 'Pure/simpset' *)
-structure GlobalSimpsetArgs =
-struct
+structure GlobalSimpset = TheoryDataFun
+(struct
val name = "Pure/simpset";
type T = simpset ref * context_ss;
val empty = (ref empty_ss, empty_context_ss);
fun copy (ref ss, ctxt_ss) = (ref ss, ctxt_ss): T; (*create new reference!*)
- val prep_ext = copy;
- fun merge ((ref ss1, ctxt_ss1), (ref ss2, ctxt_ss2)) =
+ val extend = copy;
+ fun merge _ ((ref ss1, ctxt_ss1), (ref ss2, ctxt_ss2)) =
(ref (merge_ss (ss1, ss2)), merge_context_ss (ctxt_ss1, ctxt_ss2));
fun print _ (ref ss, _) = print_ss ss;
-end;
+end);
-structure GlobalSimpset = TheoryDataFun(GlobalSimpsetArgs);
val _ = Context.add_setup [GlobalSimpset.init];
val print_simpset = GlobalSimpset.print;
-val simpset_ref_of_sg = #1 o GlobalSimpset.get_sg;
val simpset_ref_of = #1 o GlobalSimpset.get;
+val simpset_ref_of_sg = simpset_ref_of;
val get_context_ss = #2 o GlobalSimpset.get o ProofContext.theory_of;
fun map_context_ss f = GlobalSimpset.map (apsnd
@@ -216,14 +215,14 @@
(* access global simpset *)
-val simpset_of_sg = ! o simpset_ref_of_sg;
-val simpset_of = simpset_of_sg o Theory.sign_of;
+val simpset_of = ! o simpset_ref_of;
+val simpset_of_sg = simpset_of;
-fun SIMPSET tacf state = tacf (simpset_of_sg (Thm.sign_of_thm state)) state;
-fun SIMPSET' tacf i state = tacf (simpset_of_sg (Thm.sign_of_thm state)) i state;
+fun SIMPSET tacf state = tacf (simpset_of (Thm.theory_of_thm state)) state;
+fun SIMPSET' tacf i state = tacf (simpset_of (Thm.theory_of_thm state)) i state;
val simpset = simpset_of o Context.the_context;
-val simpset_ref = simpset_ref_of_sg o Theory.sign_of o Context.the_context;
+val simpset_ref = simpset_ref_of o Context.the_context;
(* change global simpset *)
@@ -285,15 +284,14 @@
(* proof data kind 'Pure/simpset' *)
-structure LocalSimpsetArgs =
-struct
+structure LocalSimpset = ProofDataFun
+(struct
val name = "Pure/simpset";
type T = simpset;
val init = simpset_of;
fun print ctxt ss = print_ss (context_ss ctxt ss (get_context_ss ctxt));
-end;
+end);
-structure LocalSimpset = ProofDataFun(LocalSimpsetArgs);
val _ = Context.add_setup [LocalSimpset.init];
val print_local_simpset = LocalSimpset.print;
--- a/src/Sequents/prover.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/Sequents/prover.ML Fri Jun 17 18:35:27 2005 +0200
@@ -168,32 +168,27 @@
-structure ProverArgs =
- struct
+structure ProverData = TheoryDataFun
+(struct
val name = "Sequents/prover";
type T = pack ref;
val empty = ref empty_pack
fun copy (ref pack) = ref pack;
- val prep_ext = copy;
- fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
+ val extend = copy;
+ fun merge _ (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
fun print _ (ref pack) = print_pack pack;
- end;
-
-structure ProverData = TheoryDataFun(ProverArgs);
+end);
val prover_setup = [ProverData.init];
val print_pack = ProverData.print;
-val pack_ref_of_sg = ProverData.get_sg;
val pack_ref_of = ProverData.get;
(* access global pack *)
-val pack_of_sg = ! o pack_ref_of_sg;
-val pack_of = pack_of_sg o sign_of;
-
+val pack_of = ! o pack_ref_of;
val pack = pack_of o Context.the_context;
-val pack_ref = pack_ref_of_sg o sign_of o Context.the_context;
+val pack_ref = pack_ref_of o Context.the_context;
(* change global pack *)
--- a/src/ZF/Tools/induct_tacs.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Fri Jun 17 18:35:27 2005 +0200
@@ -30,22 +30,20 @@
mutual_induct : thm,
exhaustion : thm};
-structure DatatypesArgs =
- struct
+structure DatatypesData = TheoryDataFun
+(struct
val name = "ZF/datatypes";
type T = datatype_info Symtab.table;
val empty = Symtab.empty;
val copy = I;
- val prep_ext = I;
- val merge: T * T -> T = Symtab.merge (K true);
+ val extend = I;
+ fun merge _ tabs : T = Symtab.merge (K true) tabs;
- fun print sg tab =
+ fun print thy tab =
Pretty.writeln (Pretty.strs ("datatypes:" ::
- map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
- end;
-
-structure DatatypesData = TheoryDataFun(DatatypesArgs);
+ map #1 (NameSpace.extern_table (Sign.type_space thy, tab))));
+end);
(** Constructor information: needed to map constructors to datatypes **)
@@ -57,27 +55,22 @@
rec_rewrites : thm list}; (*recursor equations*)
-structure ConstructorsArgs =
-struct
+structure ConstructorsData = TheoryDataFun
+(struct
val name = "ZF/constructors"
type T = constructor_info Symtab.table
-
val empty = Symtab.empty
val copy = I;
- val prep_ext = I
- val merge: T * T -> T = Symtab.merge (K true)
-
- fun print sg tab = () (*nothing extra to print*)
-end;
-
-structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
-
+ val extend = I
+ fun merge _ tabs: T = Symtab.merge (K true) tabs;
+ fun print _ _= ();
+end);
structure DatatypeTactics : DATATYPE_TACTICS =
struct
-fun datatype_info_sg sign name =
- (case Symtab.lookup (DatatypesData.get_sg sign, name) of
+fun datatype_info thy name =
+ (case Symtab.lookup (DatatypesData.get thy, name) of
SOME info => info
| NONE => error ("Unknown datatype " ^ quote name));
@@ -106,11 +99,11 @@
fun exhaust_induct_tac exh var i state =
let
val (_, _, Bi, _) = dest_state (state, i)
- val {sign, ...} = rep_thm state
+ val thy = Thm.theory_of_thm state
val tn = find_tname var Bi
val rule =
- if exh then #exhaustion (datatype_info_sg sign tn)
- else #induct (datatype_info_sg sign tn)
+ if exh then #exhaustion (datatype_info thy tn)
+ else #induct (datatype_info thy tn)
val (Const("op :",_) $ Var(ixn,_) $ _) =
(case prems_of rule of
[] => error "induction is not available for this datatype"
@@ -120,7 +113,7 @@
end
handle Find_tname msg =>
if exh then (*try boolean case analysis instead*)
- case_tac var i state
+ case_tac var i state
else error msg;
val exhaust_tac = exhaust_induct_tac true;
@@ -131,12 +124,10 @@
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
let
- val sign = sign_of thy;
-
(*analyze the LHS of a case equation to get a constructor*)
fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
| const_of eqn = error ("Ill-formed case equation: " ^
- Sign.string_of_term sign eqn);
+ Sign.string_of_term thy eqn);
val constructors =
map (head_of o const_of o FOLogic.dest_Trueprop o
@@ -232,4 +223,3 @@
val exhaust_tac = DatatypeTactics.exhaust_tac;
val induct_tac = DatatypeTactics.induct_tac;
-
--- a/src/ZF/Tools/typechk.ML Fri Jun 17 18:33:42 2005 +0200
+++ b/src/ZF/Tools/typechk.ML Fri Jun 17 18:35:27 2005 +0200
@@ -124,33 +124,26 @@
(** global tcset **)
structure TypecheckingArgs =
- struct
+struct
val name = "ZF/type-checker";
type T = tcset ref;
val empty = ref (TC{rules=[], net=Net.empty});
fun copy (ref tc) = ref tc;
- val prep_ext = copy;
- fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
+ val extend = copy;
+ fun merge _ (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
fun print _ (ref tc) = print_tc tc;
- end;
+end;
structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
val print_tcset = TypecheckingData.print;
-val tcset_ref_of_sg = TypecheckingData.get_sg;
val tcset_ref_of = TypecheckingData.get;
-
-
-(* access global tcset *)
+val tcset_of = ! o tcset_ref_of;
+val tcset = tcset_of o Context.the_context;
+val tcset_ref = tcset_ref_of o Context.the_context;
-val tcset_of_sg = ! o tcset_ref_of_sg;
-val tcset_of = tcset_of_sg o sign_of;
-
-val tcset = tcset_of o Context.the_context;
-val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
-
-fun TCSET tacf st = tacf (tcset_of_sg (Thm.sign_of_thm st)) st;
-fun TCSET' tacf i st = tacf (tcset_of_sg (Thm.sign_of_thm st)) i st;
+fun TCSET tacf st = tacf (tcset_of (Thm.theory_of_thm st)) st;
+fun TCSET' tacf i st = tacf (tcset_of (Thm.theory_of_thm st)) i st;
(* change global tcset *)
@@ -168,15 +161,14 @@
(** local tcset **)
-structure LocalTypecheckingArgs =
-struct
+structure LocalTypecheckingData = ProofDataFun
+(struct
val name = TypecheckingArgs.name;
type T = tcset;
val init = tcset_of;
fun print _ tcset = print_tc tcset;
-end;
+end);
-structure LocalTypecheckingData = ProofDataFun(LocalTypecheckingArgs);
val local_tcset_of = LocalTypecheckingData.get;