# HG changeset patch # User wenzelm # Date 1229178929 -3600 # Node ID 1b8e021e8c1f324038666d4dd2ab4cea2563aafd # Parent 8cffa980bd93d9a59db5d979b6dc6c90b8c44bfa# Parent a75f3ed534a09ab865f24b97e0e8b6fdf65269ea merged diff -r 8cffa980bd93 -r 1b8e021e8c1f Admin/isatest/settings/at-mac-poly-5.1-para --- a/Admin/isatest/settings/at-mac-poly-5.1-para Sat Dec 13 15:33:13 2008 +0100 +++ b/Admin/isatest/settings/at-mac-poly-5.1-para Sat Dec 13 15:35:29 2008 +0100 @@ -4,7 +4,7 @@ ML_SYSTEM="polyml-5.2.1" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="-H 2000" + ML_OPTIONS="--immutable 800 --mutable 1200" ISABELLE_HOME_USER=~/isabelle-at-mac-poly-e diff -r 8cffa980bd93 -r 1b8e021e8c1f src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sat Dec 13 15:33:13 2008 +0100 +++ b/src/Pure/Isar/proof.ML Sat Dec 13 15:35:29 2008 +0100 @@ -1,5 +1,4 @@ (* Title: Pure/Isar/proof.ML - ID: $Id$ Author: Markus Wenzel, TU Muenchen The Isar/VM proof language interpreter: maintains a structured flow of @@ -826,7 +825,7 @@ |> null props ? (refine (Method.Basic (Method.assumption, Position.none)) #> Seq.hd) end; -fun generic_qed state = +fun generic_qed after_ctxt state = let val (goal_ctxt, {statement, goal, after_qed, ...}) = current_goal state; val outer_state = state |> close_block; @@ -845,7 +844,7 @@ fun after_global' x y = Position.setmp_thread_data pos (fn () => after_global x y) (); in outer_state - |> map_context (ProofContext.auto_bind_facts props) + |> map_context (after_ctxt props) |> pair ((after_local', after_global'), results) end; @@ -872,7 +871,8 @@ fun local_qed txt = end_proof false txt #> - Seq.maps (generic_qed #-> (fn ((after_qed, _), results) => after_qed results)); + Seq.maps (generic_qed ProofContext.auto_bind_facts #-> + (fn ((after_qed, _), results) => after_qed results)); (* global goals *) @@ -892,7 +892,7 @@ fun global_qeds txt = end_proof true txt - #> Seq.map (generic_qed #> (fn (((_, after_qed), results), state) => + #> Seq.map (generic_qed (K I) #> (fn (((_, after_qed), results), state) => after_qed results (context_of state))) |> Seq.DETERM; (*backtracking may destroy theory!*) diff -r 8cffa980bd93 -r 1b8e021e8c1f src/Pure/context.ML --- a/src/Pure/context.ML Sat Dec 13 15:33:13 2008 +0100 +++ b/src/Pure/context.ML Sat Dec 13 15:35:29 2008 +0100 @@ -21,11 +21,10 @@ val ancestors_of: theory -> theory list val theory_name: theory -> string val is_stale: theory -> bool - val PureN: string val is_draft: theory -> bool val reject_draft: theory -> theory - val exists_name: string -> theory -> bool - val names_of: theory -> string list + val PureN: string + val display_names: theory -> string list val pretty_thy: theory -> Pretty.T val string_of_thy: theory -> string val pprint_thy: theory -> pprint_args -> unit @@ -144,17 +143,18 @@ datatype theory = Theory of (*identity*) - {self: theory ref option, (*dynamic self reference -- follows theory changes*) - id: serial * (string * int), (*identifier/name of this theory node*) - ids: (string * int) Inttab.table} * (*ancestors and checkpoints*) + {self: theory ref option, (*dynamic self reference -- follows theory changes*) + draft: bool, (*draft mode -- linear destructive changes*) + id: serial, (*identifier*) + ids: unit Inttab.table} * (*cumulative identifiers of non-drafts -- symbolic body content*) (*data*) - Object.T Datatab.table * + Object.T Datatab.table * (*body content*) (*ancestry*) - {parents: theory list, (*immediate predecessors*) - ancestors: theory list} * (*all predecessors*) + {parents: theory list, (*immediate predecessors*) + ancestors: theory list} * (*all predecessors -- canonical reverse order*) (*history*) - {name: string, (*prospective name of finished theory*) - version: int}; (*checkpoint counter*) + {name: string, (*official theory name*) + stage: int}; (*checkpoint counter*) exception THEORY of string * theory list; @@ -165,9 +165,9 @@ val ancestry_of = #3 o rep_theory; val history_of = #4 o rep_theory; -fun make_identity self id ids = {self = self, id = id, ids = ids}; +fun make_identity self draft id ids = {self = self, draft = draft, id = id, ids = ids}; fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors}; -fun make_history name version = {name = name, version = version}; +fun make_history name stage = {name = name, stage = stage}; val the_self = the o #self o identity_of; val parents_of = #parents o ancestry_of; @@ -177,7 +177,7 @@ (* staleness *) -fun eq_id ((i: int, _), (j, _)) = (i = j); +fun eq_id (i: int, j) = i = j; fun is_stale (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) = @@ -185,47 +185,46 @@ | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true; fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy) - | vitalize (thy as Theory ({self = NONE, id, ids}, data, ancestry, history)) = + | vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) = let val r = ref thy; - val thy' = Theory (make_identity (SOME r) id ids, data, ancestry, history); + val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history); in r := thy'; thy' end; -(* names *) - -val PureN = "Pure"; +(* draft mode *) -val draftN = "#"; -val draft_name = (draftN, ~1); - -fun draft_id (_, (name, _)) = (name = draftN); -val is_draft = draft_id o #id o identity_of; +val is_draft = #draft o identity_of; fun reject_draft thy = if is_draft thy then raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy]) else thy; -fun exists_name name (thy as Theory ({id = (_, (a, _)), ids, ...}, _, _, _)) = - name = theory_name thy orelse - name = a orelse - Inttab.exists (fn (_, (b, _)) => b = name) ids; + +(* names *) + +val PureN = "Pure"; +val draftN = "#"; +val finished = ~1; -fun name_of (a, ~1) = a - | name_of (a, i) = a ^ ":" ^ string_of_int i; +fun display_names thy = + let + val draft = if is_draft thy then [draftN] else []; + val {stage, ...} = history_of thy; + val name = + if stage = finished then theory_name thy + else theory_name thy ^ ":" ^ string_of_int stage; + val ancestor_names = map theory_name (ancestors_of thy); + val stale = if is_stale thy then ["!"] else []; + in rev (stale @ draft @ [name] @ ancestor_names) end; -fun names_of (Theory ({id = (_, a), ids, ...}, _, _, _)) = - rev (name_of a :: Inttab.fold (fn (_, (b, ~1)) => cons b | _ => I) ids []); - -fun pretty_thy thy = - Pretty.str_list "{" "}" (names_of thy @ (if is_stale thy then ["!"] else [])); - +val pretty_thy = Pretty.str_list "{" "}" o display_names; val string_of_thy = Pretty.string_of o pretty_thy; val pprint_thy = Pretty.pprint o pretty_thy; fun pretty_abbrev_thy thy = let - val names = names_of thy; + val names = display_names thy; val n = length names; val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names; in Pretty.str_list "{" "}" abbrev end; @@ -252,20 +251,18 @@ val pprint_thy_ref = Pretty.pprint o pretty_thy o deref; -(* consistency *) +(* build ids *) + +fun insert_id draft id ids = + if draft then ids + else Inttab.update (id, ()) ids; -fun check_insert id ids = - if draft_id id orelse Inttab.defined ids (#1 id) then ids - else if Inttab.exists (fn (_, a) => a = #2 id) ids then - error ("Different versions of theory component " ^ quote (name_of (#2 id))) - else Inttab.update id ids; - -fun check_merge - (Theory ({id = id1, ids = ids1, ...}, _, _, _)) - (Theory ({id = id2, ids = ids2, ...}, _, _, _)) = - Inttab.fold check_insert ids2 ids1 - |> check_insert id1 - |> check_insert id2; +fun merge_ids + (Theory ({draft = draft1, id = id1, ids = ids1, ...}, _, _, _)) + (Theory ({draft = draft2, id = id2, ids = ids2, ...}, _, _, _)) = + Inttab.merge (K true) (ids1, ids2) + |> insert_id draft1 id1 + |> insert_id draft2 id2; (* equality and inclusion *) @@ -273,22 +270,35 @@ val eq_thy = eq_id o pairself (#id o identity_of); fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) = - Inttab.defined ids (#1 id); + Inttab.defined ids id; fun subthy thys = eq_thy thys orelse proper_subthy thys; fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1); +(* consistent ancestors *) + +fun extend_ancestors thy thys = + if member eq_thy thys thy then raise THEORY ("Duplicate theory node", thy :: thys) + else thy :: thys; + +fun extend_ancestors_of thy = extend_ancestors thy (ancestors_of thy); + +val merge_ancestors = merge (fn (thy1, thy2) => + eq_thy (thy1, thy2) orelse + theory_name thy1 = theory_name thy2 andalso + raise THEORY ("Inconsistent theory versions", [thy1, thy2])); + + (* trivial merge *) fun merge (thy1, thy2) = if eq_thy (thy1, thy2) then thy1 else if proper_subthy (thy2, thy1) then thy1 else if proper_subthy (thy1, thy2) then thy2 - else (check_merge thy1 thy2; - error (cat_lines ["Attempt to perform non-trivial merge of theories:", - str_of_thy thy1, str_of_thy thy2])); + else error (cat_lines ["Attempt to perform non-trivial merge of theories:", + str_of_thy thy1, str_of_thy thy2]); fun merge_refs (ref1, ref2) = if ref1 = ref2 then ref1 @@ -300,41 +310,38 @@ (* primitives *) -fun create_thy name self id ids data ancestry history = - let - val {version, ...} = history; - val ids' = check_insert id ids; - val id' = (serial (), name); - val _ = check_insert id' ids'; - val identity' = make_identity self id' ids'; - in vitalize (Theory (identity', data, ancestry, history)) end; +fun create_thy self draft ids data ancestry history = + let val identity = make_identity self draft (serial ()) ids; + in vitalize (Theory (identity, data, ancestry, history)) end; -fun change_thy name f thy = +fun change_thy draft' f thy = let - val Theory ({self, id, ids}, data, ancestry, history) = thy; + val Theory ({self, draft, id, ids}, data, ancestry, history) = thy; val (self', data', ancestry') = - if is_draft thy then (self, data, ancestry) (*destructive change!*) - else if #version history > 0 + if draft then (self, data, ancestry) (*destructive change!*) + else if #stage history > 0 then (NONE, copy_data data, ancestry) - else (NONE, extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry)); + else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy)); + val ids' = insert_id draft id ids; val data'' = f data'; val thy' = NAMED_CRITICAL "theory" (fn () => - (check_thy thy; create_thy name self' id ids data'' ancestry' history)); + (check_thy thy; create_thy self' draft' ids' data'' ancestry' history)); in thy' end; -fun name_thy name = change_thy name I; -val modify_thy = change_thy draft_name; -val extend_thy = modify_thy I; +val name_thy = change_thy false I; +val extend_thy = change_thy true I; +val modify_thy = change_thy true; fun copy_thy thy = let - val Theory ({id, ids, ...}, data, ancestry, history) = thy; + val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy; + val ids' = insert_id draft id ids; val data' = copy_data data; val thy' = NAMED_CRITICAL "theory" (fn () => - (check_thy thy; create_thy draft_name NONE id ids data' ancestry history)); + (check_thy thy; create_thy NONE true ids' data' ancestry history)); in thy' end; -val pre_pure_thy = create_thy draft_name NONE (serial (), draft_name) Inttab.empty +val pre_pure_thy = create_thy NONE true Inttab.empty Datatab.empty (make_ancestry [] []) (make_history PureN 0); @@ -342,56 +349,56 @@ fun merge_thys pp (thy1, thy2) = let - val ids = check_merge thy1 thy2; + val ids = merge_ids thy1 thy2; val data = merge_data (pp thy1) (data_of thy1, data_of thy2); val ancestry = make_ancestry [] []; val history = make_history "" 0; val thy' = NAMED_CRITICAL "theory" (fn () => - (check_thy thy1; check_thy thy2; - create_thy draft_name NONE (serial (), draft_name) ids data ancestry history)); + (check_thy thy1; check_thy thy2; create_thy NONE true ids data ancestry history)); in thy' end; fun maximal_thys thys = thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys); fun begin_thy pp name imports = - if name = draftN then error ("Illegal theory name: " ^ quote draftN) + if name = "" orelse name = draftN then error ("Bad theory name: " ^ quote name) else let val parents = maximal_thys (distinct eq_thy imports); - val ancestors = distinct eq_thy (parents @ maps ancestors_of parents); - val Theory ({id, ids, ...}, data, _, _) = + val ancestors = + Library.foldl merge_ancestors ([], map ancestors_of parents) + |> fold extend_ancestors parents; + + val Theory ({ids, ...}, data, _, _) = (case parents of [] => error "No parent theories" | [thy] => extend_thy thy | thy :: thys => Library.foldl (merge_thys pp) (thy, thys)); + val ancestry = make_ancestry parents ancestors; val history = make_history name 0; val thy' = NAMED_CRITICAL "theory" (fn () => - (map check_thy imports; create_thy draft_name NONE id ids data ancestry history)); + (map check_thy imports; create_thy NONE true ids data ancestry history)); in thy' end; -(* persistent checkpoints *) +(* history stages *) + +fun history_stage f thy = + let + val {name, stage} = history_of thy; + val _ = stage = finished andalso raise THEORY ("Theory already finished", [thy]); + val history' = make_history name (f stage); + val thy' as Theory (identity', data', ancestry', _) = name_thy thy; + val thy'' = NAMED_CRITICAL "theory" (fn () => + (check_thy thy'; vitalize (Theory (identity', data', ancestry', history')))); + in thy'' end; fun checkpoint_thy thy = - if not (is_draft thy) then thy - else - let - val {name, version} = history_of thy; - val thy' as Theory (identity', data', ancestry', _) = name_thy (name, version) thy; - val history' = make_history name (version + 1); - val thy'' = NAMED_CRITICAL "theory" (fn () => - (check_thy thy'; vitalize (Theory (identity', data', ancestry', history')))); - in thy'' end; + if is_draft thy then history_stage (fn stage => stage + 1) thy + else thy; -fun finish_thy thy = NAMED_CRITICAL "theory" (fn () => - let - val name = theory_name thy; - val Theory (identity', data', ancestry', _) = name_thy (name, ~1) thy; - val history' = make_history name 0; - val thy' = vitalize (Theory (identity', data', ancestry', history')); - in thy' end); +val finish_thy = history_stage (fn _ => finished); (* theory data *) diff -r 8cffa980bd93 -r 1b8e021e8c1f src/Pure/display.ML --- a/src/Pure/display.ML Sat Dec 13 15:33:13 2008 +0100 +++ b/src/Pure/display.ML Sat Dec 13 15:35:29 2008 +0100 @@ -213,7 +213,7 @@ ||> List.partition (Defs.plain_args o #2 o #1); val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1); in - [Pretty.strs ("names:" :: Context.names_of thy)] @ + [Pretty.strs ("names:" :: Context.display_names thy)] @ [Pretty.strs ["name prefix:", NameSpace.path_of naming], Pretty.big_list "classes:" (map pretty_classrel clsses), pretty_default default, diff -r 8cffa980bd93 -r 1b8e021e8c1f src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Sat Dec 13 15:33:13 2008 +0100 +++ b/src/Pure/old_goals.ML Sat Dec 13 15:35:29 2008 +0100 @@ -127,7 +127,7 @@ (*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 + let val names = Context.display_names thy' \\ Context.display_names thy in case names of [name] => "\nNew theory: " ^ name | _ => "\nNew theories: " ^ space_implode ", " names diff -r 8cffa980bd93 -r 1b8e021e8c1f src/Pure/theory.ML --- a/src/Pure/theory.ML Sat Dec 13 15:33:13 2008 +0100 +++ b/src/Pure/theory.ML Sat Dec 13 15:35:29 2008 +0100 @@ -68,7 +68,7 @@ val copy = Context.copy_thy; fun requires thy name what = - if Context.exists_name name thy then () + if exists (fn thy' => Context.theory_name thy' = name) (thy :: ancestors_of thy) then () else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);