# HG changeset patch # User haftmann # Date 1216056057 -7200 # Node ID 367aff8d7ffdb25d45df7610c40f8e7d7fe8d29b # Parent db431936de079d055cb4a172596eaf04137c49d3 dropped junk diff -r db431936de07 -r 367aff8d7ffd src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon Jul 14 19:20:29 2008 +0200 +++ b/src/Pure/Isar/code.ML Mon Jul 14 19:20:57 2008 +0200 @@ -180,11 +180,6 @@ | melt eq (xs, ys) = fold_rev (fn y => fn (t, xs) => (t orelse not (member eq xs y), insert eq y xs)) ys (false, xs); -fun melt_alist eq_key eq (xys as (xs, ys)) = - if eq_list (eq_pair eq_key eq) (xs, ys) - then (false, xs) - else (true, AList.merge eq_key eq xys); - val melt_thms = melt Thm.eq_thm_prop; fun melt_lthms (r1, r2) = @@ -214,40 +209,19 @@ (* specification data *) -fun melt_funcs tabs = - let - val tab' = Symtab.join (fn _ => fn ((_, a), (_, b)) => melt_sdthms (a, b)) tabs; - val touched = Symtab.fold (fn (c, (true, _)) => insert (op =) c | _ => I) tab' []; - in (touched, tab') end; +val merge_funcs = Symtab.join (fn _ => fn ((_, a), (_, b)) => melt_sdthms (a, b)); val eq_string = op = : string * string -> bool; fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2) andalso gen_eq_set (eq_fst eq_string) (cs1, cs2); -fun melt_dtyps (tabs as (tab1, tab2)) = +fun merge_dtyps (tabs as (tab1, tab2)) = let - val tycos1 = Symtab.keys tab1; - val tycos2 = Symtab.keys tab2; - val tycos' = filter (member eq_string tycos2) tycos1; - val touched = not (gen_eq_set (op =) (tycos1, tycos2) - andalso gen_eq_set (eq_pair (op =) eq_dtyp) - (AList.make (the o Symtab.lookup tab1) tycos', - AList.make (the o Symtab.lookup tab2) tycos')); - fun join _ (cos as (_, cos2)) = if eq_dtyp cos - then raise Symtab.SAME else cos2; - in (touched, Symtab.join join tabs) end; + fun join _ (cos as (_, cos2)) = if eq_dtyp cos then raise Symtab.SAME else cos2; + in Symtab.join join tabs end; -fun melt_cases ((cases1, undefs1), (cases2, undefs2)) = - let - val touched1 = subtract (op =) (Symtab.keys cases1) (Symtab.keys cases2) - @ subtract (op =) (Symtab.keys cases2) (Symtab.keys cases1); - val touched2 = subtract (op =) (Symtab.keys undefs1) (Symtab.keys undefs2) - @ subtract (op =) (Symtab.keys undefs2) (Symtab.keys undefs1); - val touched = fold (insert (op =)) touched1 touched2; - in - (touched, (Symtab.merge (K true) (cases1, cases2), - Symtab.merge (K true) (undefs1, undefs2))) - end; +fun merge_cases ((cases1, undefs1), (cases2, undefs2)) = + (Symtab.merge (K true) (cases1, cases2), Symtab.merge (K true) (undefs1, undefs2)); datatype spec = Spec of { funcs: (bool * sdthms) Symtab.table, @@ -262,9 +236,9 @@ fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 }, Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) = let - val (_, funcs) = melt_funcs (funcs1, funcs2); - val (_, dtyps) = melt_dtyps (dtyps1, dtyps2); - val (_, cases) = melt_cases (cases1, cases2); + val funcs = merge_funcs (funcs1, funcs2); + val dtyps = merge_dtyps (dtyps1, dtyps2); + val cases = merge_cases (cases1, cases2); in mk_spec (funcs, (dtyps, cases)) end; @@ -889,20 +863,25 @@ in fun preprocess thy thms = - thms - |> fold (fn (_, (_, f)) => apply_functrans thy f) ((#functrans o the_thmproc o the_exec) thy) - |> map (CodeUnit.rewrite_func ((#pre o the_thmproc o the_exec) thy)) - (*FIXME - must check gere: rewrite rule, defining equation, proper constant *) - |> map (AxClass.unoverload thy) - |> common_typ_funcs; + let + val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy; + in + thms + |> fold (fn (_, (_, f)) => apply_functrans thy f) ((#functrans o the_thmproc o the_exec) thy) + |> map (CodeUnit.rewrite_func pre) + (*FIXME - must check gere: rewrite rule, defining equation, proper constant *) + |> map (AxClass.unoverload thy) + |> common_typ_funcs + end; fun preprocess_conv ct = let val thy = Thm.theory_of_cterm ct; + val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy; in ct - |> MetaSimplifier.rewrite' (ProofContext.init thy) false ((#pre o the_thmproc o the_exec) thy) + |> Simplifier.rewrite pre |> rhs_conv (AxClass.unoverload_conv thy) end; @@ -911,11 +890,11 @@ fun postprocess_conv ct = let val thy = Thm.theory_of_cterm ct; + val post = (Simplifier.theory_context thy o #post o the_thmproc o the_exec) thy; in ct |> AxClass.overload_conv thy - |> rhs_conv (MetaSimplifier.rewrite' (ProofContext.init thy) false - ((#post o the_thmproc o the_exec) thy)) + |> rhs_conv (Simplifier.rewrite post) end; fun postprocess_term thy = term_of_conv thy postprocess_conv; diff -r db431936de07 -r 367aff8d7ffd src/Pure/Isar/code_unit.ML --- a/src/Pure/Isar/code_unit.ML Mon Jul 14 19:20:29 2008 +0200 +++ b/src/Pure/Isar/code_unit.ML Mon Jul 14 19:20:57 2008 +0200 @@ -42,7 +42,8 @@ val mk_func: thm -> thm val head_func: thm -> string * ((string * sort) list * typ) val expand_eta: int -> thm -> thm - val rewrite_func: MetaSimplifier.simpset -> thm -> thm + val rewrite_func: simpset -> thm -> thm + val rewrite_head: thm list -> thm -> thm val norm_args: thm list -> thm list val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list @@ -147,8 +148,7 @@ else conv ct; in Conv.fun_conv (Conv.arg_conv lhs_conv) end; -fun rewrite_func ss thm = (Conv.fconv_rule o func_conv o - (MetaSimplifier.rewrite' (ProofContext.init (Thm.theory_of_thm thm)) false)) ss thm; +val rewrite_func = Conv.fconv_rule o func_conv o Simplifier.rewrite; val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false; fun norm_args thms = diff -r db431936de07 -r 367aff8d7ffd src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon Jul 14 19:20:29 2008 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Mon Jul 14 19:20:57 2008 +0200 @@ -412,7 +412,7 @@ Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); val print_simpset = Toplevel.unknown_context o - Toplevel.keep (Simplifier.print_ss o Simplifier.local_simpset_of o Toplevel.context_of); + Toplevel.keep (Pretty.writeln o Simplifier.pretty_ss o Simplifier.local_simpset_of o Toplevel.context_of); val print_rules = Toplevel.unknown_context o Toplevel.keep (ContextRules.print_rules o Toplevel.context_of); diff -r db431936de07 -r 367aff8d7ffd src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Mon Jul 14 19:20:29 2008 +0200 +++ b/src/Pure/meta_simplifier.ML Mon Jul 14 19:20:57 2008 +0200 @@ -44,7 +44,6 @@ val empty_ss: simpset val merge_ss: simpset * simpset -> simpset val pretty_ss: simpset -> Pretty.T - val print_ss: simpset -> unit type simproc val eq_simproc: simproc * simproc -> bool val morph_simproc: morphism -> simproc -> simproc @@ -121,9 +120,7 @@ val norm_hhf: thm -> thm val norm_hhf_protect: thm -> thm val rewrite: bool -> thm list -> conv - val rewrite': Proof.context -> bool -> simpset -> conv; val simplify: bool -> thm list -> thm -> thm - val simplify': Proof.context -> bool -> simpset -> thm -> thm; end; structure MetaSimplifier: META_SIMPLIFIER = @@ -357,8 +354,6 @@ Pretty.strs ("safe solvers:" :: map (quote o solver_name) (#2 solvers))] |> Pretty.chunks end; - -val print_ss = Pretty.writeln o pretty_ss; @@ -1263,12 +1258,9 @@ val simple_prover = SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss))); -fun rewrite' ctxt full ss = rewrite_cterm (full, false, false) simple_prover (context ctxt ss); -fun simplify' ctxt full ss = Conv.fconv_rule (rewrite' ctxt full ss); - fun rewrite _ [] ct = Thm.reflexive ct - | rewrite full thms ct = rewrite' (ProofContext.init (Thm.theory_of_cterm ct)) - full (empty_ss addsimps thms) ct; + | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover + (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct; fun simplify full thms = Conv.fconv_rule (rewrite full thms); val rewrite_rule = simplify true;