src/Pure/context.ML
changeset 29069 c7ba485581ae
parent 29001 b97a3f808133
child 29093 1cc36c0ec9eb
     1.1 --- a/src/Pure/context.ML	Thu Dec 11 20:17:57 2008 +0100
     1.2 +++ b/src/Pure/context.ML	Thu Dec 11 20:31:45 2008 +0100
     1.3 @@ -17,9 +17,9 @@
     1.4  sig
     1.5    include BASIC_CONTEXT
     1.6    (*theory context*)
     1.7 -  val theory_name: theory -> string
     1.8    val parents_of: theory -> theory list
     1.9    val ancestors_of: theory -> theory list
    1.10 +  val theory_name: theory -> string
    1.11    val is_stale: theory -> bool
    1.12    val PureN: string
    1.13    val is_draft: theory -> bool
    1.14 @@ -145,9 +145,8 @@
    1.15    Theory of
    1.16     (*identity*)
    1.17     {self: theory ref option,            (*dynamic self reference -- follows theory changes*)
    1.18 -    id: serial * string,                (*identifier of this theory*)
    1.19 -    ids: string Inttab.table,           (*identifiers of ancestors*)
    1.20 -    iids: string Inttab.table} *        (*identifiers of intermediate checkpoints*)
    1.21 +    id: serial * (string * int),        (*identifier/name of this theory node*)
    1.22 +    ids: (string * int) Inttab.table} * (*ancestors and checkpoints*)
    1.23     (*data*)
    1.24     Object.T Datatab.table *
    1.25     (*ancestry*)
    1.26 @@ -155,8 +154,7 @@
    1.27      ancestors: theory list} *           (*all predecessors*)
    1.28     (*history*)
    1.29     {name: string,                       (*prospective name of finished theory*)
    1.30 -    version: int,                       (*checkpoint counter*)
    1.31 -    intermediates: theory list};        (*intermediate checkpoints*)
    1.32 +    version: int};                      (*checkpoint counter*)
    1.33  
    1.34  exception THEORY of string * theory list;
    1.35  
    1.36 @@ -167,9 +165,9 @@
    1.37  val ancestry_of = #3 o rep_theory;
    1.38  val history_of  = #4 o rep_theory;
    1.39  
    1.40 -fun make_identity self id ids iids = {self = self, id = id, ids = ids, iids = iids};
    1.41 +fun make_identity self id ids = {self = self, id = id, ids = ids};
    1.42  fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
    1.43 -fun make_history name vers ints = {name = name, version = vers, intermediates = ints};
    1.44 +fun make_history name version = {name = name, version = version};
    1.45  
    1.46  val the_self = the o #self o identity_of;
    1.47  val parents_of = #parents o ancestry_of;
    1.48 @@ -187,10 +185,10 @@
    1.49    | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
    1.50  
    1.51  fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
    1.52 -  | vitalize (thy as Theory ({self = NONE, id, ids, iids}, data, ancestry, history)) =
    1.53 +  | vitalize (thy as Theory ({self = NONE, id, ids}, data, ancestry, history)) =
    1.54        let
    1.55          val r = ref thy;
    1.56 -        val thy' = Theory (make_identity (SOME r) id ids iids, data, ancestry, history);
    1.57 +        val thy' = Theory (make_identity (SOME r) id ids, data, ancestry, history);
    1.58        in r := thy'; thy' end;
    1.59  
    1.60  
    1.61 @@ -199,21 +197,25 @@
    1.62  val PureN = "Pure";
    1.63  
    1.64  val draftN = "#";
    1.65 -fun draft_id (_, name) = (name = draftN);
    1.66 +val draft_name = (draftN, ~1);
    1.67 +
    1.68 +fun draft_id (_, (name, _)) = (name = draftN);
    1.69  val is_draft = draft_id o #id o identity_of;
    1.70  
    1.71  fun reject_draft thy =
    1.72    if is_draft thy then raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy])
    1.73    else thy;
    1.74  
    1.75 -fun exists_name name (thy as Theory ({id, ids, iids, ...}, _, _, _)) =
    1.76 +fun exists_name name (thy as Theory ({id = (_, (a, _)), ids, ...}, _, _, _)) =
    1.77    name = theory_name thy orelse
    1.78 -  name = #2 id orelse
    1.79 -  Inttab.exists (fn (_, a) => a = name) ids orelse
    1.80 -  Inttab.exists (fn (_, a) => a = name) iids;
    1.81 +  name = a orelse
    1.82 +  Inttab.exists (fn (_, (b, _)) => b = name) ids;
    1.83  
    1.84 -fun names_of (Theory ({id, ids, ...}, _, _, _)) =
    1.85 -  rev (#2 id :: Inttab.fold (cons o #2) ids []);
    1.86 +fun name_of (a, ~1) = a
    1.87 +  | name_of (a, i) = a ^ ":" ^ string_of_int i;
    1.88 +
    1.89 +fun names_of (Theory ({id = (_, a), ids, ...}, _, _, _)) =
    1.90 +  rev (name_of a :: Inttab.fold (fn (_, (b, ~1)) => cons b | _ => I) ids []);
    1.91  
    1.92  fun pretty_thy thy =
    1.93    Pretty.str_list "{" "}" (names_of thy @ (if is_stale thy then ["!"] else []));
    1.94 @@ -252,30 +254,26 @@
    1.95  
    1.96  (* consistency *)
    1.97  
    1.98 -fun check_ins id ids =
    1.99 +fun check_insert id ids =
   1.100    if draft_id id orelse Inttab.defined ids (#1 id) then ids
   1.101    else if Inttab.exists (fn (_, a) => a = #2 id) ids then
   1.102 -    error ("Different versions of theory component " ^ quote (#2 id))
   1.103 +    error ("Different versions of theory component " ^ quote (name_of (#2 id)))
   1.104    else Inttab.update id ids;
   1.105  
   1.106 -fun check_insert intermediate id (ids, iids) =
   1.107 -  let val ids' = check_ins id ids and iids' = check_ins id iids
   1.108 -  in if intermediate then (ids, iids') else (ids', iids) end;
   1.109 -
   1.110  fun check_merge
   1.111 -    (Theory ({id = id1, ids = ids1, iids = iids1, ...}, _, _, history1))
   1.112 -    (Theory ({id = id2, ids = ids2, iids = iids2, ...}, _, _, history2)) =
   1.113 -  (Inttab.fold check_ins ids2 ids1, Inttab.fold check_ins iids2 iids1)
   1.114 -  |> check_insert (#version history1 > 0) id1
   1.115 -  |> check_insert (#version history2 > 0) id2;
   1.116 +    (Theory ({id = id1, ids = ids1, ...}, _, _, _))
   1.117 +    (Theory ({id = id2, ids = ids2, ...}, _, _, _)) =
   1.118 +  Inttab.fold check_insert ids2 ids1
   1.119 +  |> check_insert id1
   1.120 +  |> check_insert id2;
   1.121  
   1.122  
   1.123  (* equality and inclusion *)
   1.124  
   1.125  val eq_thy = eq_id o pairself (#id o identity_of);
   1.126  
   1.127 -fun proper_subthy (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =
   1.128 -  Inttab.defined ids i orelse Inttab.defined iids i;
   1.129 +fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) =
   1.130 +  Inttab.defined ids (#1 id);
   1.131  
   1.132  fun subthy thys = eq_thy thys orelse proper_subthy thys;
   1.133  
   1.134 @@ -302,19 +300,18 @@
   1.135  
   1.136  (* primitives *)
   1.137  
   1.138 -fun create_thy name self id ids iids data ancestry history =
   1.139 +fun create_thy name self id ids data ancestry history =
   1.140    let
   1.141 -    val {version, name = _, intermediates = _} = history;
   1.142 -    val intermediate = version > 0;
   1.143 -    val (ids', iids') = check_insert intermediate id (ids, iids);
   1.144 +    val {version, ...} = history;
   1.145 +    val ids' = check_insert id ids;
   1.146      val id' = (serial (), name);
   1.147 -    val _ = check_insert intermediate id' (ids', iids');
   1.148 -    val identity' = make_identity self id' ids' iids';
   1.149 +    val _ = check_insert id' ids';
   1.150 +    val identity' = make_identity self id' ids';
   1.151    in vitalize (Theory (identity', data, ancestry, history)) end;
   1.152  
   1.153  fun change_thy name f thy =
   1.154    let
   1.155 -    val Theory ({self, id, ids, iids}, data, ancestry, history) = thy;
   1.156 +    val Theory ({self, id, ids}, data, ancestry, history) = thy;
   1.157      val (self', data', ancestry') =
   1.158        if is_draft thy then (self, data, ancestry)    (*destructive change!*)
   1.159        else if #version history > 0
   1.160 @@ -322,36 +319,36 @@
   1.161        else (NONE, extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry));
   1.162      val data'' = f data';
   1.163      val thy' = NAMED_CRITICAL "theory" (fn () =>
   1.164 -      (check_thy thy; create_thy name self' id ids iids data'' ancestry' history));
   1.165 +      (check_thy thy; create_thy name self' id ids data'' ancestry' history));
   1.166    in thy' end;
   1.167  
   1.168  fun name_thy name = change_thy name I;
   1.169 -val modify_thy = change_thy draftN;
   1.170 +val modify_thy = change_thy draft_name;
   1.171  val extend_thy = modify_thy I;
   1.172  
   1.173  fun copy_thy thy =
   1.174    let
   1.175 -    val Theory ({id, ids, iids, ...}, data, ancestry, history) = thy;
   1.176 +    val Theory ({id, ids, ...}, data, ancestry, history) = thy;
   1.177      val data' = copy_data data;
   1.178      val thy' = NAMED_CRITICAL "theory" (fn () =>
   1.179 -      (check_thy thy; create_thy draftN NONE id ids iids data' ancestry history));
   1.180 +      (check_thy thy; create_thy draft_name NONE id ids data' ancestry history));
   1.181    in thy' end;
   1.182  
   1.183 -val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
   1.184 -  Datatab.empty (make_ancestry [] []) (make_history PureN 0 []);
   1.185 +val pre_pure_thy = create_thy draft_name NONE (serial (), draft_name) Inttab.empty
   1.186 +  Datatab.empty (make_ancestry [] []) (make_history PureN 0);
   1.187  
   1.188  
   1.189  (* named theory nodes *)
   1.190  
   1.191  fun merge_thys pp (thy1, thy2) =
   1.192    let
   1.193 -    val (ids, iids) = check_merge thy1 thy2;
   1.194 +    val ids = check_merge thy1 thy2;
   1.195      val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   1.196      val ancestry = make_ancestry [] [];
   1.197 -    val history = make_history "" 0 [];
   1.198 +    val history = make_history "" 0;
   1.199      val thy' = NAMED_CRITICAL "theory" (fn () =>
   1.200       (check_thy thy1; check_thy thy2;
   1.201 -      create_thy draftN NONE (serial (), draftN) ids iids data ancestry history))
   1.202 +      create_thy draft_name NONE (serial (), draft_name) ids data ancestry history));
   1.203    in thy' end;
   1.204  
   1.205  fun maximal_thys thys =
   1.206 @@ -363,37 +360,36 @@
   1.207      let
   1.208        val parents = maximal_thys (distinct eq_thy imports);
   1.209        val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
   1.210 -      val Theory ({id, ids, iids, ...}, data, _, _) =
   1.211 +      val Theory ({id, ids, ...}, data, _, _) =
   1.212          (case parents of
   1.213            [] => error "No parent theories"
   1.214          | [thy] => extend_thy thy
   1.215          | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
   1.216        val ancestry = make_ancestry parents ancestors;
   1.217 -      val history = make_history name 0 [];
   1.218 +      val history = make_history name 0;
   1.219        val thy' = NAMED_CRITICAL "theory" (fn () =>
   1.220 -        (map check_thy imports; create_thy draftN NONE id ids iids data ancestry history));
   1.221 +        (map check_thy imports; create_thy draft_name NONE id ids data ancestry history));
   1.222      in thy' end;
   1.223  
   1.224  
   1.225 -(* undoable checkpoints *)
   1.226 +(* persistent checkpoints *)
   1.227  
   1.228  fun checkpoint_thy thy =
   1.229    if not (is_draft thy) then thy
   1.230    else
   1.231      let
   1.232 -      val {name, version, intermediates} = history_of thy;
   1.233 -      val thy' as Theory (identity', data', ancestry', _) =
   1.234 -        name_thy (name ^ ":" ^ string_of_int version) thy;
   1.235 -      val history' = make_history name (version + 1) (thy' :: intermediates);
   1.236 +      val {name, version} = history_of thy;
   1.237 +      val thy' as Theory (identity', data', ancestry', _) = name_thy (name, version) thy;
   1.238 +      val history' = make_history name (version + 1);
   1.239        val thy'' = NAMED_CRITICAL "theory" (fn () =>
   1.240          (check_thy thy'; vitalize (Theory (identity', data', ancestry', history'))));
   1.241      in thy'' end;
   1.242  
   1.243  fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
   1.244    let
   1.245 -    val {name, ...} = history_of thy;
   1.246 -    val Theory (identity', data', ancestry', _) = name_thy name thy;
   1.247 -    val history' = make_history name 0 [];
   1.248 +    val name = theory_name thy;
   1.249 +    val Theory (identity', data', ancestry', _) = name_thy (name, ~1) thy;
   1.250 +    val history' = make_history name 0;
   1.251      val thy' = vitalize (Theory (identity', data', ancestry', history'));
   1.252    in thy' end);
   1.253