# HG changeset patch # User wenzelm # Date 1681938266 -7200 # Node ID f11bfc1516729bbe283a02ffa09c0dd3d1219f52 # Parent 2cd00c4054abca45dab94bf891f421ab547f913e clarified theory_id: plain value without state; diff -r 2cd00c4054ab -r f11bfc151672 src/Pure/context.ML --- a/src/Pure/context.ML Wed Apr 19 14:48:43 2023 +0200 +++ b/src/Pure/context.ML Wed Apr 19 23:04:26 2023 +0200 @@ -119,18 +119,12 @@ (** datatype theory **) -type stage = int * int Synchronized.var; -fun init_stage () : stage = (0, Synchronized.var "Context.stage" 1); -fun next_stage ((_, state): stage) = (Synchronized.change_result state (fn n => (n, n + 1)), state); - abstype theory_id = Theory_Id of - (*identity*) {id: serial, (*identifier*) - ids: Intset.T} * (*cumulative identifiers -- symbolic body content*) - (*history*) - {name: string, (*official theory name*) - stage: stage option} (*index and counter for anonymous updates*) + ids: Intset.T, (*cumulative identifiers -- symbolic body content*) + name: string, (*official theory name*) + stage: int} (*index for anonymous updates*) with fun rep_theory_id (Theory_Id args) = args; @@ -143,6 +137,8 @@ (*identity*) {theory_id: theory_id, token: Position.T Unsynchronized.ref} * + (*allocation state*) + {next_stage: unit -> int} * (*ancestry*) {parents: theory list, (*immediate predecessors*) ancestors: theory list} * (*all predecessors -- canonical reverse order*) @@ -155,24 +151,28 @@ val theory_identity = #1 o rep_theory; val theory_id = #theory_id o theory_identity; -val identity_of_id = #1 o rep_theory_id; -val identity_of = identity_of_id o theory_id; -val history_of_id = #2 o rep_theory_id; -val history_of = history_of_id o theory_id; -val ancestry_of = #2 o rep_theory; -val data_of = #3 o rep_theory; +val identity_of = rep_theory_id o theory_id; +val state_of = #2 o rep_theory; +val ancestry_of = #3 o rep_theory; +val data_of = #4 o rep_theory; -fun make_identity id ids = {id = id, ids = ids}; -fun make_history name = {name = name, stage = SOME (init_stage ())}; +fun make_state () = {next_stage = Counter.make ()}; +fun next_stage {next_stage: unit -> int} = next_stage (); + fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors}; -val theory_id_ord = int_ord o apply2 (#id o identity_of_id); -val theory_id_long_name = #name o history_of_id; +fun stage_final stage = stage = 0; + +val theory_id_stage = #stage o rep_theory_id; +val theory_id_final = stage_final o theory_id_stage; +val theory_id_ord = int_ord o apply2 (#id o rep_theory_id); +val theory_id_long_name = #name o rep_theory_id; val theory_id_name = Long_Name.base_name o theory_id_long_name; -val theory_long_name = #name o history_of; + +val theory_long_name = #name o identity_of; val theory_name = Long_Name.base_name o theory_long_name; fun theory_name' {long} = if long then theory_long_name else theory_name; -val theory_identifier = #id o identity_of_id o theory_id; +val theory_identifier = #id o identity_of; val parents_of = #parents o ancestry_of; val ancestors_of = #ancestors o ancestry_of; @@ -183,9 +183,8 @@ val PureN = "Pure"; fun display_name thy_id = - (case history_of_id thy_id of - {name, stage = NONE} => name - | {name, stage = SOME (i, _)} => name ^ ":" ^ string_of_int i); + if theory_id_final thy_id then theory_id_name thy_id + else theory_id_name thy_id ^ ":" ^ string_of_int (theory_id_stage thy_id); fun display_names thy = let @@ -209,14 +208,14 @@ (case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of SOME thy' => thy' | NONE => error ("Unknown ancestor theory " ^ quote name)) - else if is_none (#stage (history_of thy)) then thy + else if theory_id_final (theory_id thy) then thy else error ("Unfinished theory " ^ quote name); (* build ids *) val merge_ids = - apply2 (theory_id #> rep_theory_id #> #1) #> + apply2 identity_of #> (fn ({id = id1, ids = ids1, ...}, {id = id2, ids = ids2, ...}) => Intset.merge (ids1, ids2) |> Intset.insert id1 @@ -225,11 +224,10 @@ (* equality and inclusion *) -val eq_thy_id = op = o apply2 (#id o identity_of_id); +val eq_thy_id = op = o apply2 (#id o rep_theory_id); val eq_thy = op = o apply2 (#id o identity_of); -val proper_subthy_id = - apply2 (rep_theory_id #> #1) #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id); +val proper_subthy_id = apply2 rep_theory_id #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id); val proper_subthy = proper_subthy_id o apply2 theory_id; fun subthy_id p = eq_thy_id p orelse proper_subthy_id p; @@ -331,11 +329,11 @@ total = length trace} end; -fun create_thy ids history ancestry data = +fun create_thy ids name stage state ancestry data = let - val theory_id = make_theory_id (make_identity (serial ()) ids, history); + val theory_id = make_theory_id {id = serial (), ids = ids, name = name, stage = stage}; val token = make_token (); - in Theory ({theory_id = theory_id, token = token}, ancestry, data) end; + in Theory ({theory_id = theory_id, token = token}, state, ancestry, data) end; end; @@ -343,22 +341,25 @@ (* primitives *) val pre_pure_thy = - create_thy Intset.empty (make_history PureN) (make_ancestry [] []) Datatab.empty; + let + val state = make_state (); + val stage = next_stage state; + in create_thy Intset.empty PureN stage state (make_ancestry [] []) Datatab.empty end; local fun change_thy finish f thy = let - val ({id, ids}, {name, stage}) = rep_theory_id (theory_id thy); - val Theory (_, ancestry, data) = thy; + val {id, ids, name, stage} = identity_of thy; + val Theory (_, state, ancestry, data) = thy; val ancestry' = - if is_none stage + if stage_final stage then make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)) else ancestry; - val history' = {name = name, stage = if finish then NONE else Option.map next_stage stage}; val ids' = Intset.insert id ids; + val stage' = if finish then 0 else next_stage state; val data' = f data; - in create_thy ids' history' ancestry' data' end; + in create_thy ids' name stage' state ancestry' data' end; in @@ -375,12 +376,14 @@ fun bad_join (thy1, thy2) = raise THEORY ("Cannot join theories", [thy1, thy2]); -fun join_history thys = - apply2 history_of thys |> - (fn ({name, stage}, {name = name', stage = stage'}) => - if name = name' andalso is_some stage andalso is_some stage' then - {name = name, stage = Option.map next_stage stage} - else bad_join thys); +fun join_stage (thy1, thy2) = + apply2 identity_of (thy1, thy2) |> + (fn ({name, stage, ...}, {name = name', stage = stage', ...}) => + if name <> name' orelse stage_final stage orelse stage_final stage' + then bad_join (thy1, thy2) + else + let val state = state_of thy1 + in {name = name, stage = next_stage state, state = state} end) fun join_ancestry thys = apply2 ancestry_of thys |> @@ -393,10 +396,10 @@ fun join_thys thys = let val ids = merge_ids thys; - val history = join_history thys; + val {name, stage, state} = join_stage thys; val ancestry = join_ancestry thys; val data = merge_data thys (apply2 data_of thys); - in create_thy ids history ancestry data end; + in create_thy ids name stage state ancestry data end; end; @@ -408,10 +411,10 @@ fun merge_thys thys = let val ids = merge_ids thys; - val history = make_history ""; + val state = state_of (#1 thys); val ancestry = make_ancestry [] []; val data = merge_data thys (apply2 data_of thys); - in create_thy ids history ancestry data end; + in create_thy ids "" 0 state ancestry data end; fun maximal_thys thys = thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys); @@ -432,11 +435,12 @@ [] => error "Missing theory imports" | [thy] => extend_thy thy | thy :: thys => Library.foldl merge_thys (thy, thys)); - val ({ids, ...}, _) = rep_theory_id (theory_id thy0); + val ids = #ids (identity_of thy0); - val history = make_history name; + val state = make_state (); + val stage = next_stage state; val ancestry = make_ancestry parents ancestors; - in create_thy ids history ancestry (data_of thy0) |> tap finish_thy end; + in create_thy ids name stage state ancestry (data_of thy0) |> tap finish_thy end; end;