# HG changeset patch # User wenzelm # Date 1254435008 -7200 # Node ID c58fdaef7a050edbfab179540b43aff5faeb6271 # Parent 484863ae9b98e1cfc63d99b9680507adf13e77f5# Parent 044711ee3f217891626c53cfa4c489f053be053d merged diff -r 484863ae9b98 -r c58fdaef7a05 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Thu Oct 01 23:03:59 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Fri Oct 02 00:10:08 2009 +0200 @@ -538,7 +538,7 @@ val nnf_norm_conv' = nnf_conv then_conv literals_conv [@{term "op &"}, @{term "op |"}] [] - (More_Conv.cache_conv + (Conv.cache_conv (first_conv [real_lt_conv, real_le_conv, real_eq_conv, real_not_lt_conv, real_not_le_conv, real_not_eq_conv, all_conv])) diff -r 484863ae9b98 -r c58fdaef7a05 src/Pure/Concurrent/cache.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Concurrent/cache.ML Fri Oct 02 00:10:08 2009 +0200 @@ -0,0 +1,32 @@ +(* Title: Pure/Concurrent/cache.ML + Author: Makarius + +Concurrently cached values, with minimal locking time and singleton +evaluation due to lazy storage. +*) + +signature CACHE = +sig + val create: 'table -> ('table -> 'key -> 'value lazy option) -> + ('key * 'value lazy -> 'table -> 'table) -> ('key -> 'value) -> 'key -> 'value +end; + +structure Cache: CACHE = +struct + +fun create empty lookup update f = + let + val cache = Synchronized.var "cache" empty; + fun apply x = + Synchronized.change_result cache + (fn tab => + (case lookup tab x of + SOME y => (y, tab) + | NONE => + let val y = Lazy.lazy (fn () => f x) + in (y, update (x, y) tab) end)) + |> Lazy.force; + in apply end; + +end; + diff -r 484863ae9b98 -r c58fdaef7a05 src/Pure/Concurrent/lazy_sequential.ML --- a/src/Pure/Concurrent/lazy_sequential.ML Thu Oct 01 23:03:59 2009 +0200 +++ b/src/Pure/Concurrent/lazy_sequential.ML Fri Oct 02 00:10:08 2009 +0200 @@ -19,7 +19,7 @@ fun peek (Lazy r) = (case ! r of Expr _ => NONE - | Result x => SOME x); + | Result res => SOME res); fun lazy e = Lazy (Unsynchronized.ref (Expr e)); fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a))); diff -r 484863ae9b98 -r c58fdaef7a05 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Oct 01 23:03:59 2009 +0200 +++ b/src/Pure/IsaMakefile Fri Oct 02 00:10:08 2009 +0200 @@ -42,37 +42,37 @@ Pure: $(OUT)/Pure -$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/future.ML \ - Concurrent/lazy.ML Concurrent/lazy_sequential.ML \ - Concurrent/mailbox.ML Concurrent/par_list.ML \ - Concurrent/par_list_sequential.ML Concurrent/simple_thread.ML \ - Concurrent/synchronized.ML Concurrent/synchronized_sequential.ML \ - Concurrent/task_queue.ML General/alist.ML General/antiquote.ML \ - General/balanced_tree.ML General/basics.ML General/binding.ML \ - General/buffer.ML General/file.ML General/graph.ML General/heap.ML \ - General/integer.ML General/long_name.ML General/markup.ML \ - General/name_space.ML General/ord_list.ML General/output.ML \ - General/path.ML General/position.ML General/pretty.ML \ - General/print_mode.ML General/properties.ML General/queue.ML \ - General/same.ML General/scan.ML General/secure.ML General/seq.ML \ - General/source.ML General/stack.ML General/symbol.ML \ - General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \ - General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \ - Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \ - Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \ - Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \ - Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \ - Isar/local_theory.ML Isar/locale.ML Isar/method.ML \ - Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \ - Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \ - Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \ - Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \ - Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML \ - Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \ - Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \ - ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \ - ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \ - ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \ +$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/cache.ML \ + Concurrent/future.ML Concurrent/lazy.ML \ + Concurrent/lazy_sequential.ML Concurrent/mailbox.ML \ + Concurrent/par_list.ML Concurrent/par_list_sequential.ML \ + Concurrent/simple_thread.ML Concurrent/synchronized.ML \ + Concurrent/synchronized_sequential.ML Concurrent/task_queue.ML \ + General/alist.ML General/antiquote.ML General/balanced_tree.ML \ + General/basics.ML General/binding.ML General/buffer.ML \ + General/file.ML General/graph.ML General/heap.ML General/integer.ML \ + General/long_name.ML General/markup.ML General/name_space.ML \ + General/ord_list.ML General/output.ML General/path.ML \ + General/position.ML General/pretty.ML General/print_mode.ML \ + General/properties.ML General/queue.ML General/same.ML \ + General/scan.ML General/secure.ML General/seq.ML General/source.ML \ + General/stack.ML General/symbol.ML General/symbol_pos.ML \ + General/table.ML General/url.ML General/xml.ML General/yxml.ML \ + Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML \ + Isar/class.ML Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \ + Isar/context_rules.ML Isar/element.ML Isar/expression.ML \ + Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML \ + Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \ + Isar/locale.ML Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \ + Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \ + Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \ + Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \ + Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \ + Isar/skip_proof.ML Isar/spec_parse.ML Isar/specification.ML \ + Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML \ + ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML \ + ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML \ + ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \ ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \ Proof/extraction.ML Proof/proof_rewrite_rules.ML \ Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \ diff -r 484863ae9b98 -r c58fdaef7a05 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Oct 01 23:03:59 2009 +0200 +++ b/src/Pure/ROOT.ML Fri Oct 02 00:10:08 2009 +0200 @@ -56,19 +56,25 @@ (* concurrency within the ML runtime *) use "Concurrent/simple_thread.ML"; + use "Concurrent/synchronized.ML"; if Multithreading.available then () else use "Concurrent/synchronized_sequential.ML"; + use "Concurrent/mailbox.ML"; use "Concurrent/task_queue.ML"; use "Concurrent/future.ML"; + use "Concurrent/lazy.ML"; if Multithreading.available then () else use "Concurrent/lazy_sequential.ML"; + use "Concurrent/par_list.ML"; if Multithreading.available then () else use "Concurrent/par_list_sequential.ML"; +use "Concurrent/cache.ML"; + (* fundamental structures *) diff -r 484863ae9b98 -r c58fdaef7a05 src/Pure/conv.ML --- a/src/Pure/conv.ML Thu Oct 01 23:03:59 2009 +0200 +++ b/src/Pure/conv.ML Fri Oct 02 00:10:08 2009 +0200 @@ -1,5 +1,6 @@ (* Title: Pure/conv.ML - Author: Amine Chaieb and Makarius + Author: Amine Chaieb, TU Muenchen + Author: Makarius Conversions: primitive equality reasoning. *) @@ -22,6 +23,7 @@ val every_conv: conv list -> conv val try_conv: conv -> conv val repeat_conv: conv -> conv + val cache_conv: conv -> conv val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv val combination_conv: conv -> conv -> conv val comb_conv: conv -> conv @@ -44,7 +46,7 @@ structure Conv: CONV = struct -(* conversionals *) +(* basic conversionals *) fun no_conv _ = raise CTERM ("no conversion", []); val all_conv = Thm.reflexive; @@ -72,6 +74,8 @@ fun try_conv cv = cv else_conv all_conv; fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; +fun cache_conv (cv: conv) = Thm.cterm_cache cv; + (** Pure conversions **) @@ -177,5 +181,5 @@ end; -structure BasicConv: BASIC_CONV = Conv; -open BasicConv; +structure Basic_Conv: BASIC_CONV = Conv; +open Basic_Conv; diff -r 484863ae9b98 -r c58fdaef7a05 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Oct 01 23:03:59 2009 +0200 +++ b/src/Pure/more_thm.ML Fri Oct 02 00:10:08 2009 +0200 @@ -6,9 +6,19 @@ infix aconvc; +signature BASIC_THM = +sig + include BASIC_THM + structure Ctermtab: TABLE + structure Thmtab: TABLE + val aconvc: cterm * cterm -> bool +end; + signature THM = sig include THM + structure Ctermtab: TABLE + structure Thmtab: TABLE val aconvc: cterm * cterm -> bool val add_cterm_frees: cterm -> cterm list -> cterm list val all_name: string * cterm -> cterm -> cterm @@ -22,6 +32,8 @@ val lhs_of: thm -> cterm val rhs_of: thm -> cterm val thm_ord: thm * thm -> order + val cterm_cache: (cterm -> 'a) -> cterm -> 'a + val thm_cache: (thm -> 'a) -> thm -> 'a val is_reflexive: thm -> bool val eq_thm: thm * thm -> bool val eq_thms: thm list * thm list -> bool @@ -163,6 +175,15 @@ end; +(* tables and caches *) + +structure Ctermtab = Table(type key = cterm val ord = TermOrd.fast_term_ord o pairself Thm.term_of); +structure Thmtab = Table(type key = thm val ord = thm_ord); + +fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f; +fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f; + + (* equality *) fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) @@ -432,6 +453,6 @@ end; -val op aconvc = Thm.aconvc; +structure Basic_Thm: BASIC_THM = Thm; +open Basic_Thm; -structure Thmtab = Table(type key = thm val ord = Thm.thm_ord); diff -r 484863ae9b98 -r c58fdaef7a05 src/Pure/term_ord.ML --- a/src/Pure/term_ord.ML Thu Oct 01 23:03:59 2009 +0200 +++ b/src/Pure/term_ord.ML Fri Oct 02 00:10:08 2009 +0200 @@ -4,8 +4,17 @@ Term orderings. *) +signature BASIC_TERM_ORD = +sig + structure Vartab: TABLE + structure Sorttab: TABLE + structure Typtab: TABLE + structure Termtab: TABLE +end; + signature TERM_ORD = sig + include BASIC_TERM_ORD val fast_indexname_ord: indexname * indexname -> order val sort_ord: sort * sort -> order val typ_ord: typ * typ -> order @@ -17,6 +26,7 @@ val hd_ord: term * term -> order val termless: term * term -> bool val term_lpo: (term -> int) -> term * term -> order + val term_cache: (term -> 'a) -> term -> 'a end; structure TermOrd: TERM_ORD = @@ -202,9 +212,17 @@ end; +(* tables and caches *) + +structure Vartab = Table(type key = indexname val ord = fast_indexname_ord); +structure Sorttab = Table(type key = sort val ord = sort_ord); +structure Typtab = Table(type key = typ val ord = typ_ord); +structure Termtab = Table(type key = term val ord = fast_term_ord); + +fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f; + end; -structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_ord); -structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord); -structure Typtab = Table(type key = typ val ord = TermOrd.typ_ord); -structure Termtab = Table(type key = term val ord = TermOrd.fast_term_ord); +structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd; +open Basic_Term_Ord; + diff -r 484863ae9b98 -r c58fdaef7a05 src/Tools/more_conv.ML --- a/src/Tools/more_conv.ML Thu Oct 01 23:03:59 2009 +0200 +++ b/src/Tools/more_conv.ML Fri Oct 02 00:10:08 2009 +0200 @@ -1,5 +1,5 @@ -(* Title: Tools/more_conv.ML - Author: Sascha Boehme +(* Title: Tools/more_conv.ML + Author: Sascha Boehme, TU Muenchen Further conversions and conversionals. *) @@ -14,16 +14,11 @@ val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv val binder_conv: (Proof.context -> conv) -> Proof.context -> conv - - val cache_conv: conv -> conv end - - structure More_Conv : MORE_CONV = struct - fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs) @@ -45,19 +40,4 @@ fun binder_conv cv ctxt = Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt) - -fun cache_conv conv = - let - val cache = Synchronized.var "cache_conv" Termtab.empty - fun lookup t = - Synchronized.change_result cache (fn tab => (Termtab.lookup tab t, tab)) - val keep = Synchronized.change cache o Termtab.insert Thm.eq_thm - fun keep_result t thm = (keep (t, thm); thm) - - fun cconv ct = - (case lookup (Thm.term_of ct) of - SOME thm => thm - | NONE => keep_result (Thm.term_of ct) (conv ct)) - in cconv end - end