# HG changeset patch # User wenzelm # Date 1119025985 -7200 # Node ID 18a07ad8fea81ecc72d2370ebbe485b4ac14d81f # Parent 24abe4c0e4b498e581ea25606a69c9975726d094 accomodate change of TheoryDataFun; diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/HOL/Import/hol4rews.ML Fri Jun 17 18:33:05 2005 +0200 @@ -18,9 +18,9 @@ type T = ImportStatus val empty = NoImport val copy = I -val prep_ext = I -fun merge (NoImport,NoImport) = NoImport - | merge _ = (warning "Import status set during merge"; NoImport) +val extend = I +fun merge _ (NoImport,NoImport) = NoImport + | merge _ _ = (warning "Import status set during merge"; NoImport) fun print sg import_status = Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname))) end; @@ -33,10 +33,10 @@ type T = string val empty = "" val copy = I -val prep_ext = I -fun merge ("",arg) = arg - | merge (arg,"") = arg - | merge (s1,s2) = +val extend = I +fun merge _ ("",arg) = arg + | merge _ (arg,"") = arg + | merge _ (s1,s2) = if s1 = s2 then s1 else error "Trying to merge two different import segments" @@ -55,9 +55,9 @@ type T = string list val empty = [] val copy = I -val prep_ext = I -fun merge ([],[]) = [] - | merge _ = error "Used names not empty during merge" +val extend = I +fun merge _ ([],[]) = [] + | merge _ _ = error "Used names not empty during merge" fun print sg used_names = Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented") end; @@ -70,9 +70,9 @@ type T = string * string * string list val empty = ("","",[]) val copy = I -val prep_ext = I -fun merge (("","",[]),("","",[])) = ("","",[]) - | merge _ = error "Dump data not empty during merge" +val extend = I +fun merge _ (("","",[]),("","",[])) = ("","",[]) + | merge _ _ = error "Dump data not empty during merge" fun print sg dump_data = Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented") end; @@ -85,8 +85,8 @@ type T = string 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 _ : T * T -> T = Symtab.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 moves:" (Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab))) @@ -100,8 +100,8 @@ type T = string 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 _ : T * T -> T = Symtab.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 imports:" (Symtab.foldl (fn (xl,(thyname,segname)) => (Pretty.str (thyname ^ " imported from segment " ^ segname)::xl)) ([],tab))) @@ -130,8 +130,8 @@ type T = string 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 _ : T * T -> T = Symtab.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 constant moves:" (Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab))) @@ -145,8 +145,8 @@ type T = (string option) StringPair.table val empty = StringPair.empty val copy = I -val prep_ext = I -val merge : T * T -> T = StringPair.merge (K true) +val extend = I +fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 mappings:" (StringPair.foldl (fn (xl,((bthy,bthm),isathm)) => (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED"))::xl)) ([],tab))) @@ -160,8 +160,8 @@ type T = holthm StringPair.table val empty = StringPair.empty val copy = I -val prep_ext = I -val merge : T * T -> T = StringPair.merge (K true) +val extend = I +fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 mappings:" (StringPair.foldl (fn (xl,((bthy,bthm),(_,thm))) => (Pretty.str (bthy ^ "." ^ bthm ^ ":")::(Display.pretty_thm thm)::xl)) ([],tab))) @@ -175,8 +175,8 @@ type T = (bool * string * typ option) StringPair.table val empty = StringPair.empty val copy = I -val prep_ext = I -val merge : T * T -> T = StringPair.merge (K true) +val extend = I +fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 constant mappings:" (StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst,_))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab))) @@ -190,8 +190,8 @@ type T = string StringPair.table val empty = StringPair.empty val copy = I -val prep_ext = I -val merge : T * T -> T = StringPair.merge (K true) +val extend = I +fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 constant renamings:" (StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) ([],tab))) @@ -205,8 +205,8 @@ type T = string StringPair.table val empty = StringPair.empty val copy = I -val prep_ext = I -val merge : T * T -> T = StringPair.merge (K true) +val extend = I +fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 constant definitions:" (StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) ([],tab))) @@ -220,8 +220,8 @@ type T = (bool * string) StringPair.table val empty = StringPair.empty val copy = I -val prep_ext = I -val merge : T * T -> T = StringPair.merge (K true) +val extend = I +fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 type mappings:" (StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab))) @@ -235,8 +235,8 @@ type T = ((term * term) list * thm) StringPair.table val empty = StringPair.empty val copy = I -val prep_ext = I -val merge : T * T -> T = StringPair.merge (K true) +val extend = I +fun merge _ : T * T -> T = StringPair.merge (K true) fun print sg tab = Pretty.writeln (Pretty.big_list "HOL4 pending theorems:" (StringPair.foldl (fn (xl,((bthy,bthm),(_,th))) => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) ([],tab))) @@ -250,8 +250,8 @@ type T = thm list val empty = [] val copy = I -val prep_ext = I -val merge = Library.gen_union Thm.eq_thm +val extend = I +fun merge _ = Library.gen_union Thm.eq_thm fun print sg thms = Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:" (map Display.pretty_thm thms)) @@ -480,7 +480,7 @@ fun process (thy,((bthy,bthm),hth as (_,thm))) = let val sg = sign_of thy - val thm1 = rewrite_rule (map (transfer_sg sg) rews) (transfer_sg sg thm) + val thm1 = rewrite_rule (map (Thm.transfer sg) rews) (Thm.transfer sg thm) val thm2 = standard thm1 val (thy2,_) = PureThy.store_thm((bthm,thm2),[]) thy val thy5 = add_hol4_theorem bthy bthm hth thy2 diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/HOL/Import/import_package.ML --- a/src/HOL/Import/import_package.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/HOL/Import/import_package.ML Fri Jun 17 18:33:05 2005 +0200 @@ -16,10 +16,9 @@ type T = ProofKernel.thm option array option val empty = NONE val copy = I -val prep_ext = I -fun merge _ = NONE -fun print sg import_segment = - Pretty.writeln (Pretty.str ("Pretty printing of importer data not implemented")) +val extend = I +fun merge _ _ = NONE +fun print _ _ = () end structure ImportData = TheoryDataFun(ImportDataArgs) diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Fri Jun 17 18:33:05 2005 +0200 @@ -18,8 +18,8 @@ (**** theory data ****) -structure CodegenArgs = -struct +structure CodegenData = TheoryDataFun +(struct val name = "HOL/inductive_codegen"; type T = {intros : thm list Symtab.table, @@ -28,16 +28,15 @@ val empty = {intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty}; val copy = I; - val prep_ext = I; - fun merge ({intros=intros1, graph=graph1, eqns=eqns1}, + val extend = I; + fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1}, {intros=intros2, graph=graph2, eqns=eqns2}) = {intros = Symtab.merge_multi Drule.eq_thm_prop (intros1, intros2), graph = Graph.merge (K true) (graph1, graph2), eqns = Symtab.merge_multi Drule.eq_thm_prop (eqns1, eqns2)}; fun print _ _ = (); -end; +end); -structure CodegenData = TheoryDataFun(CodegenArgs); fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^ string_of_thm thm); diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Fri Jun 17 18:33:05 2005 +0200 @@ -16,18 +16,17 @@ open Codegen; -structure CodegenArgs = -struct +structure CodegenData = TheoryDataFun +(struct val name = "HOL/recfun_codegen"; type T = thm list Symtab.table; val empty = Symtab.empty; val copy = I; - val prep_ext = I; - val merge = Symtab.merge_multi' Drule.eq_thm_prop; + val extend = I; + fun merge _ = Symtab.merge_multi' Drule.eq_thm_prop; fun print _ _ = (); -end; +end); -structure CodegenData = TheoryDataFun(CodegenArgs); val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; val lhs_of = fst o dest_eqn o prop_of; diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/HOL/Tools/refute.ML Fri Jun 17 18:33:05 2005 +0200 @@ -183,8 +183,8 @@ parameters: string Symtab.table}; val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; val copy = I; - val prep_ext = I; - fun merge + val extend = I; + fun merge _ ({interpreters = in1, printers = pr1, parameters = pa1}, {interpreters = in2, printers = pr2, parameters = pa2}) = {interpreters = rev (merge_alists (rev in1) (rev in2)), diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/HOL/arith_data.ML Fri Jun 17 18:33:05 2005 +0200 @@ -201,24 +201,22 @@ (* arith theory data *) -structure ArithTheoryDataArgs = -struct +structure ArithTheoryData = TheoryDataFun +(struct val name = "HOL/arith"; type T = {splits: thm list, inj_consts: (string * typ)list, discrete: string list, presburger: (int -> tactic) option}; val empty = {splits = [], inj_consts = [], discrete = [], presburger = NONE}; val copy = I; - val prep_ext = I; - fun merge ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1}, + val extend = I; + fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1}, {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, presburger= presburger2}) = {splits = Drule.merge_rules (splits1, splits2), inj_consts = merge_lists inj_consts1 inj_consts2, discrete = merge_lists discrete1 discrete2, presburger = (case presburger1 of NONE => presburger2 | p => p)}; fun print _ _ = (); -end; - -structure ArithTheoryData = TheoryDataFun(ArithTheoryDataArgs); +end); fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} => {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger}) thy, thm); @@ -360,7 +358,7 @@ | decomp2 data _ = NONE fun decomp sg = - let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg + let val {discrete, inj_consts, ...} = ArithTheoryData.get sg in decomp2 (sg,discrete,inj_consts) end fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n) @@ -458,12 +456,12 @@ fun raw_arith_tac ex i st = refute_tac (K true) - (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st)))) + (REPEAT o split_tac (#splits (ArithTheoryData.get (Thm.sign_of_thm st)))) ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex) i st; fun presburger_tac i st = - (case ArithTheoryData.get_sg (sign_of_thm st) of + (case ArithTheoryData.get (sign_of_thm st) of {presburger = SOME tac, ...} => (tracing "Simple arithmetic decision procedure failed.\nNow trying full Presburger arithmetic..."; tac i st) | _ => no_tac st); diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/Provers/classical.ML Fri Jun 17 18:33:05 2005 +0200 @@ -79,10 +79,10 @@ val appSWrappers : claset -> wrapper val appWrappers : claset -> wrapper - val claset_ref_of_sg: Sign.sg -> claset ref val claset_ref_of: theory -> claset ref - val claset_of_sg: Sign.sg -> claset + val claset_ref_of_sg: theory -> claset ref (*obsolete*) val claset_of: theory -> claset + val claset_of_sg: theory -> claset (*obsolete*) val CLASET: (claset -> tactic) -> tactic val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic val claset: unit -> claset @@ -826,23 +826,22 @@ (* theory data kind 'Provers/claset' *) -structure GlobalClasetArgs = -struct +structure GlobalClaset = TheoryDataFun +(struct val name = "Provers/claset"; type T = claset ref * context_cs; val empty = (ref empty_cs, empty_context_cs); - fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T; (*create new reference!*) - val prep_ext = copy; - fun merge ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) = + fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T; + val extend = copy; + fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) = (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2)); fun print _ (ref cs, _) = print_cs cs; -end; +end); -structure GlobalClaset = TheoryDataFun(GlobalClasetArgs); val print_claset = GlobalClaset.print; -val claset_ref_of_sg = #1 o GlobalClaset.get_sg; val claset_ref_of = #1 o GlobalClaset.get; +val claset_ref_of_sg = claset_ref_of; val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of; fun map_context_cs f = GlobalClaset.map (apsnd @@ -851,14 +850,14 @@ (* access claset *) -val claset_of_sg = ! o claset_ref_of_sg; -val claset_of = claset_of_sg o Theory.sign_of; +val claset_of = ! o claset_ref_of; +val claset_of_sg = claset_of; -fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state; -fun CLASET' tacf i state = tacf (claset_of_sg (Thm.sign_of_thm state)) i state; +fun CLASET tacf state = tacf (claset_of (Thm.theory_of_thm state)) state; +fun CLASET' tacf i state = tacf (claset_of (Thm.theory_of_thm state)) i state; val claset = claset_of o Context.the_context; -val claset_ref = claset_ref_of_sg o Theory.sign_of o Context.the_context; +val claset_ref = claset_ref_of o Context.the_context; (* change claset *) @@ -885,15 +884,14 @@ (* proof data kind 'Provers/claset' *) -structure LocalClasetArgs = -struct +structure LocalClaset = ProofDataFun +(struct val name = "Provers/claset"; type T = claset; val init = claset_of; fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt)); -end; +end); -structure LocalClaset = ProofDataFun(LocalClasetArgs); val print_local_claset = LocalClaset.print; val get_local_claset = LocalClaset.get; val put_local_claset = LocalClaset.put; @@ -921,7 +919,7 @@ in (ctxt', #2 (DeltaClasetData.get ctxt')) end; -local +local fun rename_thm' (ctxt,thm) = let val (new_ctxt, new_id) = delta_increment ctxt val new_name = "anon_cla_" ^ (string_of_int new_id) @@ -935,7 +933,7 @@ fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm); end - + (* attributes *) @@ -961,60 +959,60 @@ let val thm_name = Thm.name_of_thm th val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) val delta_cs = get_delta_claset ctxt' - val new_dcs = delta_cs addSDs [th'] - val ctxt'' = put_delta_claset new_dcs ctxt' + val new_dcs = delta_cs addSDs [th'] + val ctxt'' = put_delta_claset new_dcs ctxt' in - change_local_cs (op addSDs) (ctxt'',th) + change_local_cs (op addSDs) (ctxt'',th) end; -fun safe_elim_local (ctxt, th)= +fun safe_elim_local (ctxt, th)= let val thm_name = Thm.name_of_thm th val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) val delta_cs = get_delta_claset ctxt' - val new_dcs = delta_cs addSEs [th'] - val ctxt'' = put_delta_claset new_dcs ctxt' + val new_dcs = delta_cs addSEs [th'] + val ctxt'' = put_delta_claset new_dcs ctxt' in - change_local_cs (op addSEs) (ctxt'',th) + change_local_cs (op addSEs) (ctxt'',th) end; -fun safe_intro_local (ctxt, th) = +fun safe_intro_local (ctxt, th) = let val thm_name = Thm.name_of_thm th val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) val delta_cs = get_delta_claset ctxt' - val new_dcs = delta_cs addSIs [th'] - val ctxt'' = put_delta_claset new_dcs ctxt' + val new_dcs = delta_cs addSIs [th'] + val ctxt'' = put_delta_claset new_dcs ctxt' in - change_local_cs (op addSIs) (ctxt'',th) + change_local_cs (op addSIs) (ctxt'',th) end; -fun haz_dest_local (ctxt, th)= +fun haz_dest_local (ctxt, th)= let val thm_name = Thm.name_of_thm th val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)else (ctxt, th) val delta_cs = get_delta_claset ctxt' - val new_dcs = delta_cs addDs [th'] - val ctxt'' = put_delta_claset new_dcs ctxt' + val new_dcs = delta_cs addDs [th'] + val ctxt'' = put_delta_claset new_dcs ctxt' in - change_local_cs (op addDs) (ctxt'',th) + change_local_cs (op addDs) (ctxt'',th) end; fun haz_elim_local (ctxt,th) = let val thm_name = Thm.name_of_thm th val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) val delta_cs = get_delta_claset ctxt' - val new_dcs = delta_cs addEs [th'] - val ctxt'' = put_delta_claset new_dcs ctxt' - in - change_local_cs (op addEs) (ctxt'',th) + val new_dcs = delta_cs addEs [th'] + val ctxt'' = put_delta_claset new_dcs ctxt' + in + change_local_cs (op addEs) (ctxt'',th) end; -fun haz_intro_local (ctxt,th) = +fun haz_intro_local (ctxt,th) = let val thm_name = Thm.name_of_thm th val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th) val delta_cs = get_delta_claset ctxt' - val new_dcs = delta_cs addIs [th'] - val ctxt'' = put_delta_claset new_dcs ctxt' - in - change_local_cs (op addIs) (ctxt'',th) + val new_dcs = delta_cs addIs [th'] + val ctxt'' = put_delta_claset new_dcs ctxt' + in + change_local_cs (op addIs) (ctxt'',th) end; diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/Pure/Isar/calculation.ML Fri Jun 17 18:33:05 2005 +0200 @@ -32,43 +32,41 @@ (** global and local calculation data **) -(* theory data kind 'Isar/calculation' *) +(* global calculation *) fun print_rules prt x (trans, sym) = [Pretty.big_list "transitivity rules:" (map (prt x) (NetRules.rules trans)), Pretty.big_list "symmetry rules:" (map (prt x) sym)] |> Pretty.chunks |> Pretty.writeln; -structure GlobalCalculationArgs = -struct +structure GlobalCalculation = TheoryDataFun +(struct val name = "Isar/calculation"; type T = thm NetRules.T * thm list val empty = (NetRules.elim, []); val copy = I; - val prep_ext = I; - fun merge ((trans1, sym1), (trans2, sym2)) = + val extend = I; + fun merge _ ((trans1, sym1), (trans2, sym2)) = (NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)); val print = print_rules Display.pretty_thm_sg; -end; +end); -structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs); val _ = Context.add_setup [GlobalCalculation.init]; val print_global_rules = GlobalCalculation.print; -(* proof data kind 'Isar/calculation' *) +(* local calculation *) -structure LocalCalculationArgs = -struct +structure LocalCalculation = ProofDataFun +(struct val name = "Isar/calculation"; type T = (thm NetRules.T * thm list) * (thm list * int) option; fun init thy = (GlobalCalculation.get thy, NONE); fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs; -end; +end); -structure LocalCalculation = ProofDataFun(LocalCalculationArgs); val _ = Context.add_setup [LocalCalculation.init]; val get_local_rules = #1 o LocalCalculation.get o Proof.context_of; val print_local_rules = LocalCalculation.print; diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/Pure/Isar/context_rules.ML Fri Jun 17 18:33:05 2005 +0200 @@ -126,9 +126,9 @@ val empty = make_rules ~1 [] empty_netpairs ([], []); val copy = I; - val prep_ext = I; + val extend = I; - fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...}, + fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...}, Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) = let val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2'); @@ -147,15 +147,14 @@ val _ = Context.add_setup [GlobalRules.init]; val print_global_rules = GlobalRules.print; -structure LocalRulesArgs = -struct +structure LocalRules = ProofDataFun +(struct val name = GlobalRulesArgs.name; type T = GlobalRulesArgs.T; val init = GlobalRules.get; val print = print_rules ProofContext.pretty_thm; -end; +end); -structure LocalRules = ProofDataFun(LocalRulesArgs); val _ = Context.add_setup [LocalRules.init]; val print_local_rules = LocalRules.print; @@ -175,22 +174,25 @@ if k = k' then untaglist rest else x :: untaglist rest; -fun orderlist brls = - untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls); -fun orderlist_no_weight brls = - untaglist (sort (Int.compare o pairself (snd o fst)) brls); +fun orderlist brls = + untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls); + +fun orderlist_no_weight brls = + untaglist (sort (Int.compare o pairself (snd o fst)) brls); fun may_unify weighted t net = map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t)); fun find_erules _ [] = K [] | find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (Thm.prop_of fact)); + fun find_irules w goal = may_unify w (Logic.strip_assums_concl goal); fun find_rules_netpair weighted facts goal (inet, enet) = find_erules weighted facts enet @ find_irules weighted goal inet; -fun find_rules weighted facts goals = map (find_rules_netpair weighted facts goals) o netpairs; +fun find_rules weighted facts goals = + map (find_rules_netpair weighted facts goals) o netpairs; (* wrappers *) @@ -268,5 +270,4 @@ val addXDs_local = modifier (dest_query_local NONE); val delrules_local = modifier rule_del_local; - end; diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/Pure/Isar/induct_attrib.ML --- a/src/Pure/Isar/induct_attrib.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/Pure/Isar/induct_attrib.ML Fri Jun 17 18:33:05 2005 +0200 @@ -85,7 +85,7 @@ NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso Drule.eq_thm_prop (th1, th2)); -fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name); +fun lookup_rule (rs: rules) name = assoc_string (NetRules.rules rs, name); fun print_rules prt kind x rs = let val thms = map snd (NetRules.rules rs) @@ -109,8 +109,8 @@ ((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)), (init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2))); val copy = I; - val prep_ext = I; - fun merge (((casesT1, casesS1), (inductT1, inductS1)), + val extend = I; + fun merge _ (((casesT1, casesS1), (inductT1, inductS1)), ((casesT2, casesS2), (inductT2, inductS2))) = ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)), (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2))); @@ -132,16 +132,15 @@ (* proof data kind 'Isar/induction' *) -structure LocalInductArgs = -struct +structure LocalInduct = ProofDataFun +(struct val name = "Isar/induction"; type T = GlobalInductArgs.T; fun init thy = GlobalInduct.get thy; fun print x = print_all_rules ProofContext.pretty_thm x; -end; +end); -structure LocalInduct = ProofDataFun(LocalInductArgs); val _ = Context.add_setup [LocalInduct.init]; val print_local_rules = LocalInduct.print; val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get; @@ -229,5 +228,4 @@ [(casesN, cases_attr, "declaration of cases rule for type or set"), (inductN, induct_attr, "declaration of induction rule for type or set")]]; - end; diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/Pure/Isar/term_style.ML --- a/src/Pure/Isar/term_style.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/Pure/Isar/term_style.ML Fri Jun 17 18:33:05 2005 +0200 @@ -20,19 +20,18 @@ fun err_dup_styles names = error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names); -structure StyleArgs = -struct +structure StyleData = TheoryDataFun +(struct val name = "Isar/style"; type T = ((Proof.context -> term -> term) * stamp) Symtab.table; val empty = Symtab.empty; val copy = I; - val prep_ext = I; - fun merge tabs = Symtab.merge eq_snd tabs + val extend = I; + fun merge _ tabs = Symtab.merge eq_snd tabs handle Symtab.DUPS dups => err_dup_styles dups; fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab)); -end; +end); -structure StyleData = TheoryDataFun(StyleArgs); val _ = Context.add_setup [StyleData.init]; val print_styles = StyleData.print; @@ -52,16 +51,19 @@ (* predefined styles *) fun style_binargs ctxt t = - let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in + let + val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt) + (Logic.strip_imp_concl t) + in case concl of (_ $ l $ r) => (l, r) | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl) end; fun style_parm_premise i ctxt t = - let val prems = Logic.strip_imp_prems t - in if i <= length prems then List.nth(prems, i-1) - else error ("Not enough premises for prem" ^ string_of_int i ^ - " in propositon: " ^ ProofContext.string_of_term ctxt t) + let val prems = Logic.strip_imp_prems t in + if i <= length prems then List.nth (prems, i - 1) + else error ("Not enough premises for prem" ^ string_of_int i ^ + " in propositon: " ^ ProofContext.string_of_term ctxt t) end; val _ = Context.add_setup diff -r 24abe4c0e4b4 -r 18a07ad8fea8 src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Fri Jun 17 18:33:03 2005 +0200 +++ b/src/ZF/Tools/ind_cases.ML Fri Jun 17 18:33:05 2005 +0200 @@ -18,19 +18,18 @@ (* theory data *) -structure IndCasesArgs = -struct +structure IndCasesData = TheoryDataFun +(struct val name = "ZF/ind_cases"; type T = (simpset -> cterm -> thm) 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 _ tabs : T = Symtab.merge (K true) tabs; fun print _ _ = (); -end; +end); -structure IndCasesData = TheoryDataFun(IndCasesArgs); fun declare name f = IndCasesData.map (fn tab => Symtab.update ((name, f), tab));