support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
authorwenzelm
Thu Jul 04 12:31:24 2019 +0200 (2 weeks ago)
changeset 7036134b271c4f400
parent 70360 03430649a7d2
child 70362 421727c19b23
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
src/Pure/context.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/context.ML	Thu Jul 04 11:26:00 2019 +0200
     1.2 +++ b/src/Pure/context.ML	Thu Jul 04 12:31:24 2019 +0200
     1.3 @@ -50,6 +50,7 @@
     1.4    val subthy: theory * theory -> bool
     1.5    val trace_theories: bool Unsynchronized.ref
     1.6    val theories_trace: unit -> {active_positions: Position.T list, active: int, total: int}
     1.7 +  val join_thys: theory * theory -> theory
     1.8    val begin_thy: string -> theory list -> theory
     1.9    val finish_thy: theory -> theory
    1.10    val theory_data_size: theory -> (Position.T * int) list
    1.11 @@ -365,7 +366,39 @@
    1.12  end;
    1.13  
    1.14  
    1.15 -(* named theory nodes *)
    1.16 +(* join: anonymous theory nodes *)
    1.17 +
    1.18 +local
    1.19 +
    1.20 +fun bad_join (thy1, thy2) = raise THEORY ("Cannot join theories", [thy1, thy2]);
    1.21 +
    1.22 +fun join_history thys =
    1.23 +  apply2 history_of thys |>
    1.24 +  (fn ({name, stage}, {name = name', stage = stage'}) =>
    1.25 +    if name = name' andalso is_some stage andalso is_some stage' then
    1.26 +      {name = name, stage = Option.map next_stage stage}
    1.27 +    else bad_join thys);
    1.28 +
    1.29 +fun join_ancestry thys =
    1.30 +  apply2 ancestry_of thys |>
    1.31 +  (fn (ancestry as {parents, ancestors}, {parents = parents', ancestors = ancestors'}) =>
    1.32 +    if eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors')
    1.33 +    then ancestry else bad_join thys);
    1.34 +
    1.35 +in
    1.36 +
    1.37 +fun join_thys thys =
    1.38 +  let
    1.39 +    val ids = merge_ids thys;
    1.40 +    val history = join_history thys;
    1.41 +    val ancestry = join_ancestry thys;
    1.42 +    val data = merge_data thys (apply2 data_of thys);
    1.43 +  in create_thy ids history ancestry data end;
    1.44 +
    1.45 +end;
    1.46 +
    1.47 +
    1.48 +(* merge: named theory nodes *)
    1.49  
    1.50  local
    1.51  
     2.1 --- a/src/Pure/theory.ML	Thu Jul 04 11:26:00 2019 +0200
     2.2 +++ b/src/Pure/theory.ML	Thu Jul 04 12:31:24 2019 +0200
     2.3 @@ -23,6 +23,7 @@
     2.4    val defs_of: theory -> Defs.T
     2.5    val at_begin: (theory -> theory option) -> theory -> theory
     2.6    val at_end: (theory -> theory option) -> theory -> theory
     2.7 +  val join_theory: theory list -> theory
     2.8    val begin_theory: string * Position.T -> theory list -> theory
     2.9    val end_theory: theory -> theory
    2.10    val add_axiom: Proof.context -> binding * term -> theory -> theory
    2.11 @@ -168,6 +169,11 @@
    2.12  val defs_of = #defs o rep_theory;
    2.13  
    2.14  
    2.15 +(* join theory *)
    2.16 +
    2.17 +val join_theory = foldl1 Context.join_thys;
    2.18 +
    2.19 +
    2.20  (* begin/end theory *)
    2.21  
    2.22  val begin_wrappers = rev o #1 o #wrappers o rep_theory;