simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
authorhaftmann
Wed Aug 02 20:33:39 2017 +0200 (21 months ago)
changeset 66310e8d2862ec203
parent 66309 ca985e87c123
child 66312 9a4c049f8997
child 66316 2a1739aad711
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
sufficient to keep history stamps rather than complete historized data;
semantically conflicting specifications are temoprary blacklisted after theory merge but remain historized;
clarified signature;
NEWS
src/HOL/Tools/code_evaluation.ML
src/Pure/Isar/code.ML
     1.1 --- a/NEWS	Thu Aug 03 07:31:25 2017 +0200
     1.2 +++ b/NEWS	Wed Aug 02 20:33:39 2017 +0200
     1.3 @@ -99,9 +99,20 @@
     1.4  
     1.5  * Deleting the last code equations for a particular function using
     1.6  [code del] results in function with no equations (runtime abort) rather
     1.7 -than an unimplemented function (generate time abort).  Use explicit
     1.8 +than an unimplemented function (generation time abort).  Use explicit
     1.9  [[code drop:]] to enforce the latter.  Minor INCOMPATIBILTIY.
    1.10  
    1.11 +* Proper concept of code declarations in code.ML:
    1.12 +  - Regular code declarations act only on the global theory level,
    1.13 +    being ignored with warnings if syntactically malformed.
    1.14 +  - Explicitly global code declarations yield errors if syntactically malformed.
    1.15 +  - Default code declarations are silently ignored if syntactically malformed.
    1.16 +Minor INCOMPATIBILITY.
    1.17 +
    1.18 +* Clarified and standardized internal data bookkeeping of code declarations:
    1.19 +history of serials allows to track potentially non-monotonous declarations
    1.20 +appropriately.  Minor INCOMPATIBILITY.
    1.21 +
    1.22  
    1.23  *** HOL ***
    1.24  
     2.1 --- a/src/HOL/Tools/code_evaluation.ML	Thu Aug 03 07:31:25 2017 +0200
     2.2 +++ b/src/HOL/Tools/code_evaluation.ML	Wed Aug 02 20:33:39 2017 +0200
     2.3 @@ -117,9 +117,10 @@
     2.4      |> Code.declare_default_eqns_global [(eq, true)]
     2.5    end;
     2.6  
     2.7 -fun ensure_abs_term_of_code (tyco, (vs, ((abs, (_, ty)), (proj, _)))) =
     2.8 +fun ensure_abs_term_of_code (tyco, (vs, {abstractor = (abs, (_, ty)),
     2.9 +    projection, ...})) =
    2.10    for_term_of_instance tyco vs
    2.11 -    (fn tyco => fn vs => add_abs_term_of_code tyco vs abs ty proj);
    2.12 +    (fn tyco => fn vs => add_abs_term_of_code tyco vs abs ty projection);
    2.13  
    2.14  
    2.15  (* setup *)
     3.1 --- a/src/Pure/Isar/code.ML	Thu Aug 03 07:31:25 2017 +0200
     3.2 +++ b/src/Pure/Isar/code.ML	Wed Aug 02 20:33:39 2017 +0200
     3.3 @@ -20,7 +20,7 @@
     3.4  
     3.5    (*code equations and certificates*)
     3.6    val assert_eqn: theory -> thm * bool -> thm * bool
     3.7 -  val assert_abs_eqn: theory -> string option -> thm -> thm * string
     3.8 +  val assert_abs_eqn: theory -> string option -> thm -> thm * (string * string)
     3.9    type cert
    3.10    val constrain_cert: theory -> sort list -> cert -> cert
    3.11    val conclude_cert: cert -> cert
    3.12 @@ -38,8 +38,8 @@
    3.13    val declare_abstype: thm -> local_theory -> local_theory
    3.14    val declare_abstype_global: thm -> theory -> theory
    3.15    val abstype_interpretation:
    3.16 -    (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm)))
    3.17 -      -> theory -> theory) -> theory -> theory
    3.18 +    (string * ((string * sort) list * {abs_rep: thm, abstractor: string * ((string * sort) list * typ),
    3.19 +      projection: string}) -> theory -> theory) -> theory -> theory
    3.20    val declare_default_eqns: (thm * bool) list -> local_theory -> local_theory
    3.21    val declare_default_eqns_global: (thm * bool) list -> theory -> theory
    3.22    val declare_eqns: (thm * bool) list -> local_theory -> local_theory
    3.23 @@ -48,7 +48,7 @@
    3.24    val del_eqn_global: thm -> theory -> theory
    3.25    val declare_abstract_eqn: thm -> local_theory -> local_theory
    3.26    val declare_abstract_eqn_global: thm -> theory -> theory
    3.27 -  val declare_empty_global: string -> theory -> theory
    3.28 +  val declare_aborting_global: string -> theory -> theory
    3.29    val declare_unimplemented_global: string -> theory -> theory
    3.30    val declare_case_global: thm -> theory -> theory
    3.31    val declare_undefined_global: string -> theory -> theory
    3.32 @@ -59,7 +59,8 @@
    3.33    val is_abstr: theory -> string -> bool
    3.34    val get_cert: Proof.context -> ((thm * bool) list -> (thm * bool) list option) list
    3.35      -> string -> cert
    3.36 -  val get_case_schema: theory -> string -> (int * (int * string option list)) option
    3.37 +  type case_schema
    3.38 +  val get_case_schema: theory -> string -> case_schema option
    3.39    val get_case_cong: theory -> string -> thm option
    3.40    val is_undefined: theory -> string -> bool
    3.41    val print_codesetup: theory -> unit
    3.42 @@ -150,96 +151,218 @@
    3.43  fun read_const thy = check_unoverload thy o read_bare_const thy;
    3.44  
    3.45  
    3.46 -(** data store **)
    3.47 +(** executable specifications **)
    3.48 +
    3.49 +(* types *)
    3.50 +
    3.51 +datatype type_spec = Constructors of {
    3.52 +      constructors: (string * ((string * sort) list * typ list)) list,
    3.53 +      case_combinators: string list}
    3.54 +  | Abstractor of {
    3.55 +      abs_rep: thm,
    3.56 +      abstractor: string * ((string * sort) list * typ),
    3.57 +      projection: string,
    3.58 +      more_abstract_functions: string list};
    3.59  
    3.60 -(* datatypes *)
    3.61 +fun concrete_constructors_of (Constructors {constructors, ...}) =
    3.62 +      constructors
    3.63 +  | concrete_constructors_of _ =
    3.64 +      [];
    3.65 +
    3.66 +fun constructors_of (Constructors {constructors, ...}) =
    3.67 +      (constructors, false)
    3.68 +  | constructors_of (Abstractor {abstractor = (co, (vs, ty)), ...}) =
    3.69 +      ([(co, (vs, [ty]))], true);
    3.70 +
    3.71 +fun case_combinators_of (Constructors {case_combinators, ...}) =
    3.72 +      case_combinators
    3.73 +  | case_combinators_of (Abstractor _) =
    3.74 +      [];
    3.75  
    3.76 -datatype typ_spec = Constructors of (string * ((string * sort) list * typ list)) list *
    3.77 -      string list (*references to associated case constructors*)
    3.78 -  | Abstractor of (string * ((string * sort) list * typ)) * (string * thm);
    3.79 +fun add_case_combinator c (vs, Constructors {constructors, case_combinators}) =
    3.80 +  (vs, Constructors {constructors = constructors,
    3.81 +    case_combinators = insert (op =) c case_combinators});
    3.82 +
    3.83 +fun projection_of (Constructors _) =
    3.84 +      NONE
    3.85 +  | projection_of (Abstractor {projection, ...}) =
    3.86 +      SOME projection;
    3.87 +
    3.88 +fun abstract_functions_of (Constructors _) =
    3.89 +      []
    3.90 +  | abstract_functions_of (Abstractor {more_abstract_functions, projection, ...}) =
    3.91 +      projection :: more_abstract_functions;
    3.92  
    3.93 -fun constructors_of (Constructors (cos, _)) = (cos, false)
    3.94 -  | constructors_of (Abstractor ((co, (vs, ty)), _)) = ([(co, (vs, [ty]))], true);
    3.95 +fun add_abstract_function c (vs, Abstractor {abs_rep, abstractor, projection, more_abstract_functions}) =
    3.96 +  (vs, Abstractor {abs_rep = abs_rep, abstractor = abstractor, projection = projection,
    3.97 +    more_abstract_functions = insert (op =) c more_abstract_functions});
    3.98  
    3.99 -fun case_consts_of (Constructors (_, case_consts)) = case_consts
   3.100 -  | case_consts_of (Abstractor _) = [];
   3.101 +fun join_same_types' (Constructors {constructors, case_combinators = case_combinators1},
   3.102 +    Constructors {case_combinators = case_combinators2, ...}) =
   3.103 +      Constructors {constructors = constructors,
   3.104 +        case_combinators = merge (op =) (case_combinators1, case_combinators2)}
   3.105 +  | join_same_types' (Abstractor {abs_rep, abstractor, projection, more_abstract_functions = more_abstract_functions1},
   3.106 +      Abstractor {more_abstract_functions = more_abstract_functions2, ...}) =
   3.107 +      Abstractor {abs_rep = abs_rep, abstractor = abstractor, projection = projection,
   3.108 +        more_abstract_functions = merge (op =) (more_abstract_functions1, more_abstract_functions2)};
   3.109 +
   3.110 +fun join_same_types ((vs, spec1), (_, spec2)) = (vs, join_same_types' (spec1, spec2));
   3.111  
   3.112  
   3.113  (* functions *)
   3.114  
   3.115 -datatype fun_spec = Unimplemented
   3.116 -  | Eqns_Default of (thm * bool) list
   3.117 -  | Eqns of (thm * bool) list
   3.118 -  | Proj of term * string
   3.119 -  | Abstr of thm * string;
   3.120 +datatype fun_spec =
   3.121 +    Eqns of bool * (thm * bool) list
   3.122 +  | Proj of term * (string * string)
   3.123 +  | Abstr of thm * (string * string);
   3.124  
   3.125 -val default_fun_spec = Eqns_Default [];
   3.126 +val unimplemented = Eqns (true, []);
   3.127  
   3.128 -fun is_default (Eqns_Default _) = true
   3.129 +fun is_unimplemented (Eqns (true, [])) = true
   3.130 +  | is_unimplemented _ = false;
   3.131 +
   3.132 +fun is_default (Eqns (true, _)) = true
   3.133    | is_default _ = false;
   3.134  
   3.135 -fun associated_abstype (Abstr (_, tyco)) = SOME tyco
   3.136 +val aborting = Eqns (false, []);
   3.137 +
   3.138 +fun associated_abstype (Proj (_, tyco_abs)) = SOME tyco_abs
   3.139 +  | associated_abstype (Abstr (_, tyco_abs)) = SOME tyco_abs
   3.140    | associated_abstype _ = NONE;
   3.141  
   3.142  
   3.143  (* cases *)
   3.144  
   3.145 -datatype case_spec = Case of ((int * (int * string option list)) * thm)
   3.146 +type case_schema = int * (int * string option list);
   3.147 +
   3.148 +datatype case_spec =
   3.149 +    No_Case
   3.150 +  | Case of {schema: case_schema, tycos: string list, cong: thm}
   3.151    | Undefined;
   3.152  
   3.153 +fun associated_datatypes (Case {tycos, schema = (_, (_, raw_cos)), ...}) = (tycos, map_filter I raw_cos)
   3.154 +  | associated_datatypes _ = ([], []);
   3.155 +
   3.156  
   3.157 -(* executable code data *)
   3.158 +(** background theory data store **)
   3.159 +
   3.160 +(* historized declaration data *)
   3.161 +
   3.162 +structure History =
   3.163 +struct
   3.164 +
   3.165 +type 'a T = {
   3.166 +  entry: 'a,
   3.167 +  suppressed: bool,     (*incompatible entries are merely suppressed after theory merge but sustain*)
   3.168 +  history: serial list  (*explicit trace of declaration history supports non-monotonic declarations*)
   3.169 +} Symtab.table;
   3.170 +
   3.171 +fun some_entry (SOME {suppressed = false, entry, ...}) = SOME entry
   3.172 +  | some_entry _ = NONE;
   3.173 +
   3.174 +fun lookup table =
   3.175 +  Symtab.lookup table #> some_entry;
   3.176 +
   3.177 +fun register key entry table =
   3.178 +  if is_some (Symtab.lookup table key)
   3.179 +  then Symtab.map_entry key
   3.180 +    (fn {history, ...} => {entry = entry, suppressed = false, history = serial () :: history}) table
   3.181 +  else Symtab.update (key, {entry = entry, suppressed = false, history = [serial ()]}) table;
   3.182 +
   3.183 +fun modify_entry key f = Symtab.map_entry key
   3.184 +  (fn {entry, suppressed, history} => {entry = f entry, suppressed = suppressed, history = history});
   3.185 +
   3.186 +fun all table = Symtab.dest table
   3.187 +  |> map_filter (fn (key, {entry, suppressed = false, ...}) => SOME (key, entry) | _ => NONE);
   3.188  
   3.189 -datatype spec = Spec of {
   3.190 -  history_concluded: bool,
   3.191 -  types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
   3.192 -    (*with explicit history*),
   3.193 -  functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
   3.194 -    (*with explicit history*),
   3.195 -  cases: case_spec Symtab.table
   3.196 +local
   3.197 +
   3.198 +fun tap_serial (table : 'a T) key =
   3.199 +  Option.map (hd o #history) (Symtab.lookup table key);
   3.200 +
   3.201 +fun merge_history join_same
   3.202 +    ({entry = entry1, history = history1, ...}, {entry = entry2, history = history2, ...}) =
   3.203 +  let
   3.204 +    val history = merge (op =) (history1, history2);
   3.205 +    val entry = if hd history1 = hd history2 then join_same (entry1, entry2)
   3.206 +      else if hd history = hd history1 then entry1 else entry2;
   3.207 +  in {entry = entry, suppressed = false, history = history} end;
   3.208 +
   3.209 +in
   3.210 +
   3.211 +fun join join_same tables = Symtab.join (K (merge_history join_same)) tables;
   3.212 +
   3.213 +fun suppress key = Symtab.map_entry key
   3.214 +  (fn {entry, history, ...} => {entry = entry, suppressed = true, history = history});
   3.215 +
   3.216 +fun suppress_except f = Symtab.map (fn key => fn {entry, suppressed, history} =>
   3.217 +  {entry = entry, suppressed = suppressed orelse (not o f) (key, entry), history = history});
   3.218 +
   3.219 +end;
   3.220 +
   3.221 +end;
   3.222 +
   3.223 +datatype specs = Specs of {
   3.224 +  types: ((string * sort) list * type_spec) History.T,
   3.225 +  pending_eqns: (thm * bool) list Symtab.table,
   3.226 +  functions: fun_spec History.T,
   3.227 +  cases: case_spec History.T
   3.228  };
   3.229  
   3.230 -fun make_spec (history_concluded, (types, (functions, cases))) =
   3.231 -  Spec { history_concluded = history_concluded, types = types,
   3.232 -    functions = functions,  cases = cases };
   3.233 -val empty_spec =
   3.234 -  make_spec (false, (Symtab.empty, (Symtab.empty, Symtab.empty)));
   3.235 -fun map_spec f (Spec { history_concluded = history_concluded,
   3.236 -  types = types, functions = functions, cases = cases }) =
   3.237 -  make_spec (f (history_concluded, (types, (functions, cases))));
   3.238 -fun merge_spec (Spec { history_concluded = _, types = types1,
   3.239 -    functions = functions1, cases = cases1 },
   3.240 -  Spec { history_concluded = _, types = types2,
   3.241 -    functions = functions2, cases = cases2 }) =
   3.242 +fun types_of (Specs {types, ...}) = types;
   3.243 +fun pending_eqns_of (Specs {pending_eqns, ...}) = pending_eqns;
   3.244 +fun functions_of (Specs {functions, ...}) = functions;
   3.245 +fun cases_of (Specs {cases, ...}) = cases;
   3.246 +
   3.247 +fun make_specs (types, ((pending_eqns, functions), cases)) =
   3.248 +  Specs {types = types, pending_eqns = pending_eqns,
   3.249 +    functions = functions, cases = cases};
   3.250 +
   3.251 +val empty_specs =
   3.252 +  make_specs (Symtab.empty, ((Symtab.empty, Symtab.empty), Symtab.empty));
   3.253 +
   3.254 +fun map_specs f (Specs {types = types, pending_eqns = pending_eqns,
   3.255 +    functions = functions, cases = cases}) =
   3.256 +  make_specs (f (types, ((pending_eqns, functions), cases)));
   3.257 +
   3.258 +fun merge_specs (Specs {types = types1, pending_eqns = _,
   3.259 +    functions = functions1, cases = cases1},
   3.260 +  Specs {types = types2, pending_eqns = _,
   3.261 +    functions = functions2, cases = cases2}) =
   3.262    let
   3.263 -    val types = Symtab.join (K (AList.merge (op =) (K true))) (types1, types2);
   3.264 -    val case_consts_of' = (maps case_consts_of o map (snd o snd o hd o snd) o Symtab.dest);
   3.265 -    fun merge_functions ((_, history1), (_, history2)) =
   3.266 +    val types = History.join join_same_types (types1, types2);
   3.267 +    val all_types = map (snd o snd) (History.all types);
   3.268 +    fun check_abstype (c, fun_spec) = case associated_abstype fun_spec of
   3.269 +        NONE => true
   3.270 +      | SOME (tyco, abs) => (case History.lookup types tyco of
   3.271 +          NONE => false
   3.272 +        | SOME (_, Abstractor {abstractor = (abs', _), projection, more_abstract_functions, ...}) =>
   3.273 +            abs = abs' andalso (c = projection orelse member (op =) more_abstract_functions c));
   3.274 +    fun check_datatypes (c, case_spec) =
   3.275        let
   3.276 -        val raw_history = AList.merge (op = : serial * serial -> bool)
   3.277 -          (K true) (history1, history2);
   3.278 -        val filtered_history = filter_out (is_default o snd) raw_history;
   3.279 -        val history = if null filtered_history
   3.280 -          then raw_history else filtered_history;
   3.281 -      in ((false, (snd o hd) history), history) end;
   3.282 -    val all_datatype_specs = map (snd o snd o hd o snd) (Symtab.dest types);
   3.283 -    val all_constructors = maps (map fst o fst o constructors_of) all_datatype_specs;
   3.284 -    val invalidated_case_consts = union (op =) (case_consts_of' types1) (case_consts_of' types2)
   3.285 -      |> subtract (op =) (maps case_consts_of all_datatype_specs)
   3.286 -    val functions = Symtab.join (K merge_functions) (functions1, functions2)
   3.287 -      |> fold (fn c => Symtab.map_entry c (apfst (K (true, default_fun_spec)))) all_constructors;
   3.288 -    val cases = Symtab.merge (K true) (cases1, cases2)
   3.289 -      |> fold Symtab.delete invalidated_case_consts;
   3.290 -  in make_spec (false, (types, (functions, cases))) end;
   3.291 +        val (tycos, required_constructors) = associated_datatypes case_spec;
   3.292 +        val allowed_constructors =
   3.293 +          tycos
   3.294 +          |> maps (these o Option.map (concrete_constructors_of o snd) o History.lookup types)
   3.295 +          |> map fst;
   3.296 +      in subset (op =) (required_constructors, allowed_constructors) end;
   3.297 +    val all_constructors =
   3.298 +      maps (fst o constructors_of) all_types;
   3.299 +    val all_abstract_functions =
   3.300 +      maps abstract_functions_of all_types;
   3.301 +    val case_combinators =
   3.302 +      maps case_combinators_of all_types;
   3.303 +    val functions = History.join fst (functions1, functions2)
   3.304 +      |> fold (History.suppress o fst) all_constructors
   3.305 +      |> History.suppress_except check_abstype;
   3.306 +    val cases = History.join fst (cases1, cases2)
   3.307 +      |> History.suppress_except check_datatypes;
   3.308 +  in make_specs (types, ((Symtab.empty, functions), cases)) end;
   3.309  
   3.310 -fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
   3.311 -fun types_of (Spec { types, ... }) = types;
   3.312 -fun functions_of (Spec { functions, ... }) = functions;
   3.313 -fun cases_of (Spec { cases, ... }) = cases;
   3.314 -val map_history_concluded = map_spec o apfst;
   3.315 -val map_types = map_spec o apsnd o apfst;
   3.316 -val map_functions = map_spec o apsnd o apsnd o apfst;
   3.317 -val map_cases = map_spec o apsnd o apsnd o apsnd;
   3.318 +val map_types = map_specs o apfst;
   3.319 +val map_pending_eqns = map_specs o apsnd o apfst o apfst;
   3.320 +val map_functions = map_specs o apsnd o apfst o apsnd;
   3.321 +val map_cases = map_specs o apsnd o apsnd;
   3.322  
   3.323  
   3.324  (* data slots dependent on executable code *)
   3.325 @@ -249,7 +372,7 @@
   3.326  
   3.327  local
   3.328  
   3.329 -type kind = { empty: Any.T };
   3.330 +type kind = {empty: Any.T};
   3.331  
   3.332  val kinds = Synchronized.var "Code_Data" (Datatab.empty: kind Datatab.table);
   3.333  
   3.334 @@ -263,7 +386,7 @@
   3.335  fun declare_data empty =
   3.336    let
   3.337      val k = serial ();
   3.338 -    val kind = { empty = empty };
   3.339 +    val kind = {empty = empty};
   3.340      val _ = Synchronized.change kinds (Datatab.update (k, kind));
   3.341    in k end;
   3.342  
   3.343 @@ -272,7 +395,7 @@
   3.344  end; (*local*)
   3.345  
   3.346  
   3.347 -(* theory store *)
   3.348 +(* global theory store *)
   3.349  
   3.350  local
   3.351  
   3.352 @@ -281,50 +404,24 @@
   3.353  
   3.354  structure Code_Data = Theory_Data
   3.355  (
   3.356 -  type T = spec * (data * theory) option Synchronized.var;
   3.357 -  val empty = (empty_spec, empty_dataref ());
   3.358 +  type T = specs * (data * theory) option Synchronized.var;
   3.359 +  val empty = (empty_specs, empty_dataref ());
   3.360    val extend : T -> T = apsnd (K (empty_dataref ()));
   3.361 -  fun merge ((spec1, _), (spec2, _)) =
   3.362 -    (merge_spec (spec1, spec2), empty_dataref ());
   3.363 +  fun merge ((specs1, _), (specs2, _)) =
   3.364 +    (merge_specs (specs1, specs2), empty_dataref ());
   3.365  );
   3.366  
   3.367  in
   3.368  
   3.369  
   3.370 -(* access to executable code *)
   3.371 -
   3.372 -val spec_of : theory -> spec = fst o Code_Data.get;
   3.373 +(* access to executable specifications *)
   3.374  
   3.375 -fun map_spec_purge f = Code_Data.map (fn (spec, _) => (f spec, empty_dataref ()));
   3.376 +val specs_of : theory -> specs = fst o Code_Data.get;
   3.377  
   3.378 -fun change_fun_spec c f = (map_spec_purge o map_functions
   3.379 -  o (Symtab.map_default (c, ((false, default_fun_spec), [])))
   3.380 -    o apfst) (fn (_, spec) => (true, f spec));
   3.381 +fun modify_specs f = Code_Data.map (fn (specs, _) => (f specs, empty_dataref ()));
   3.382  
   3.383  
   3.384 -(* tackling equation history *)
   3.385 -
   3.386 -fun continue_history thy = if (history_concluded o spec_of) thy
   3.387 -  then thy
   3.388 -    |> (Code_Data.map o apfst o map_history_concluded) (K false)
   3.389 -    |> SOME
   3.390 -  else NONE;
   3.391 -
   3.392 -fun conclude_history thy = if (history_concluded o spec_of) thy
   3.393 -  then NONE
   3.394 -  else thy
   3.395 -    |> (Code_Data.map o apfst)
   3.396 -        ((map_functions o Symtab.map) (fn _ => fn ((changed, current), history) =>
   3.397 -          ((false, current),
   3.398 -            if changed then (serial (), current) :: history else history))
   3.399 -        #> map_history_concluded (K true))
   3.400 -    |> SOME;
   3.401 -
   3.402 -val _ = Theory.setup
   3.403 -  (Theory.at_begin continue_history #> Theory.at_end conclude_history);
   3.404 -
   3.405 -
   3.406 -(* access to data dependent on abstract executable code *)
   3.407 +(* access to data dependent on executable specifications *)
   3.408  
   3.409  fun change_yield_data (kind, mk, dest) theory f =
   3.410    let
   3.411 @@ -346,6 +443,66 @@
   3.412  end; (*local*)
   3.413  
   3.414  
   3.415 +(* pending function equations *)
   3.416 +
   3.417 +(* Ideally, *all* equations implementing a functions would be treated as
   3.418 +   *one* atomic declaration;  unfortunately, we cannot implement this:
   3.419 +   the too-well-established declaration interface are Isar attributes
   3.420 +   which operate on *one* single theorem.  Hence we treat such Isar
   3.421 +   declarations as "pending" and historize them as proper declarations
   3.422 +   at the end of each theory. *)
   3.423 +
   3.424 +fun modify_pending_eqns c f specs =
   3.425 +  let
   3.426 +    val existing_eqns = case History.lookup (functions_of specs) c of
   3.427 +        SOME (Eqns (false, eqns)) => eqns
   3.428 +      | _ => [];
   3.429 +  in
   3.430 +    specs
   3.431 +    |> map_pending_eqns (Symtab.map_default (c, existing_eqns) f)
   3.432 +  end;
   3.433 +
   3.434 +fun register_fun_spec c spec =
   3.435 +  map_pending_eqns (Symtab.delete_safe c)
   3.436 +  #> map_functions (History.register c spec);
   3.437 +
   3.438 +fun lookup_fun_spec specs c =
   3.439 +  case Symtab.lookup (pending_eqns_of specs) c of
   3.440 +    SOME eqns => Eqns (false, eqns)
   3.441 +  | NONE => (case History.lookup (functions_of specs) c of
   3.442 +      SOME spec => spec
   3.443 +    | NONE => unimplemented);
   3.444 +
   3.445 +fun lookup_proper_fun_spec specs c =
   3.446 +  let
   3.447 +    val spec = lookup_fun_spec specs c
   3.448 +  in
   3.449 +    if is_unimplemented spec then NONE else SOME spec
   3.450 +  end;
   3.451 +
   3.452 +fun all_fun_specs specs =
   3.453 +  map_filter (fn c => Option.map (pair c) (lookup_proper_fun_spec specs c))
   3.454 +    (union (op =)
   3.455 +      ((Symtab.keys o pending_eqns_of) specs)
   3.456 +      ((Symtab.keys o functions_of) specs));
   3.457 +
   3.458 +fun historize_pending_fun_specs thy =
   3.459 +  let
   3.460 +    val pending_eqns = (pending_eqns_of o specs_of) thy;
   3.461 +  in if Symtab.is_empty pending_eqns
   3.462 +    then
   3.463 +      NONE
   3.464 +    else
   3.465 +      thy
   3.466 +      |> modify_specs (map_functions
   3.467 +          (Symtab.fold (fn (c, eqs) => History.register c (Eqns (false, eqs))) pending_eqns)
   3.468 +          #> map_pending_eqns (K Symtab.empty))
   3.469 +      |> SOME
   3.470 +  end;
   3.471 +
   3.472 +val _ = Theory.setup (Theory.at_end historize_pending_fun_specs);
   3.473 +
   3.474 +
   3.475  (** foundation **)
   3.476  
   3.477  (* types *)
   3.478 @@ -393,20 +550,19 @@
   3.479      val constructors = map (inst vs o snd) raw_constructors;
   3.480    in (tyco, (map (rpair []) vs, constructors)) end;
   3.481  
   3.482 -fun get_type_entry thy tyco = case these (Symtab.lookup ((types_of o spec_of) thy) tyco)
   3.483 - of (_, entry) :: _ => SOME entry
   3.484 -  | _ => NONE;
   3.485 +fun lookup_vs_type_spec thy = History.lookup ((types_of o specs_of) thy);
   3.486  
   3.487 -fun get_type thy tyco = case get_type_entry thy tyco
   3.488 - of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
   3.489 +fun get_type thy tyco = case lookup_vs_type_spec thy tyco
   3.490 + of SOME (vs, type_spec) => apfst (pair vs) (constructors_of type_spec)
   3.491    | NONE => Sign.arity_number thy tyco
   3.492        |> Name.invent Name.context Name.aT
   3.493        |> map (rpair [])
   3.494        |> rpair []
   3.495        |> rpair false;
   3.496  
   3.497 -fun get_abstype_spec thy tyco = case get_type_entry thy tyco
   3.498 - of SOME (vs, Abstractor spec) => (vs, spec)
   3.499 +fun get_abstype_spec thy tyco = case lookup_vs_type_spec thy tyco of
   3.500 +    SOME (vs, Abstractor {abs_rep, abstractor, projection, ...}) =>
   3.501 +      (vs, {abs_rep = abs_rep, abstractor = abstractor, projection = projection})
   3.502    | _ => error ("Not an abstract type: " ^ tyco);
   3.503  
   3.504  fun get_type_of_constr_or_abstr thy c =
   3.505 @@ -462,7 +618,7 @@
   3.506        ^ string_of_typ thy ty_decl)
   3.507    end;
   3.508  
   3.509 -fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) =
   3.510 +fun check_eqn thy {allow_nonlinear, allow_consts, allow_pats} thm (lhs, rhs) =
   3.511    let
   3.512      fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
   3.513        | Free _ => bad_thm "Illegal free variable"
   3.514 @@ -507,11 +663,14 @@
   3.515      val _ = if not (is_abstr thy c) then ()
   3.516        else bad_thm "Abstractor as head in equation";
   3.517      val _ = check_decl_ty thy (c, ty);
   3.518 -    val _ = case strip_type ty
   3.519 -     of (Type (tyco, _) :: _, _) => (case get_type_entry thy tyco
   3.520 -       of SOME (_, Abstractor (_, (proj, _))) => if c = proj
   3.521 -            then bad_thm "Projection as head in equation"
   3.522 -            else ()
   3.523 +    val _ = case strip_type ty of
   3.524 +        (Type (tyco, _) :: _, _) => (case lookup_vs_type_spec thy tyco of
   3.525 +          SOME (_, type_spec) => (case projection_of type_spec of
   3.526 +            SOME proj =>
   3.527 +              if c = proj
   3.528 +              then bad_thm "Projection as head in equation"
   3.529 +              else ()
   3.530 +          | _ => ())
   3.531          | _ => ())
   3.532        | _ => ();
   3.533    in () end;
   3.534 @@ -523,8 +682,8 @@
   3.535      val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
   3.536        handle TERM _ => bad_thm "Not an equation"
   3.537             | THM _ => bad_thm "Not a proper equation";
   3.538 -    val _ = check_eqn thy { allow_nonlinear = not proper,
   3.539 -      allow_consts = not (proper andalso check_patterns), allow_pats = true } thm (lhs, rhs);
   3.540 +    val _ = check_eqn thy {allow_nonlinear = not proper,
   3.541 +      allow_consts = not (proper andalso check_patterns), allow_pats = true} thm (lhs, rhs);
   3.542    in (thm, proper) end;
   3.543  
   3.544  fun raw_assert_abs_eqn thy some_tyco thm =
   3.545 @@ -532,9 +691,9 @@
   3.546      val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
   3.547        handle TERM _ => bad_thm "Not an equation"
   3.548             | THM _ => bad_thm "Not a proper equation";
   3.549 -    val (rep, lhs) = dest_comb full_lhs
   3.550 +    val (proj_t, lhs) = dest_comb full_lhs
   3.551        handle TERM _ => bad_thm "Not an abstract equation";
   3.552 -    val (rep_const, ty) = dest_Const rep
   3.553 +    val (proj, ty) = dest_Const proj_t
   3.554        handle TERM _ => bad_thm "Not an abstract equation";
   3.555      val (tyco, Ts) = (dest_Type o domain_type) ty
   3.556        handle TERM _ => bad_thm "Not an abstract equation"
   3.557 @@ -542,16 +701,16 @@
   3.558      val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
   3.559            else bad_thm ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
   3.560        | NONE => ();
   3.561 -    val (vs', (_, (rep', _))) = case try (get_abstype_spec thy) tyco
   3.562 -     of SOME data => data
   3.563 -      | NONE => bad_thm ("Not an abstract type: " ^ tyco);
   3.564 -    val _ = if rep_const = rep' then ()
   3.565 -      else bad_thm ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
   3.566 -    val _ = check_eqn thy { allow_nonlinear = false,
   3.567 -      allow_consts = false, allow_pats = false } thm (lhs, rhs);
   3.568 -    val _ = if ListPair.all (fn (T, (_, sort)) => Sign.of_sort thy (T, sort)) (Ts, vs') then ()
   3.569 +    val (vs, proj', (abs', _)) = case lookup_vs_type_spec thy tyco
   3.570 +     of SOME (vs, Abstractor spec) => (vs, #projection spec, #abstractor spec)
   3.571 +      | _ => bad_thm ("Not an abstract type: " ^ tyco);
   3.572 +    val _ = if proj = proj' then ()
   3.573 +      else bad_thm ("Projection mismatch: " ^ quote proj ^ " vs. " ^ quote proj');
   3.574 +    val _ = check_eqn thy {allow_nonlinear = false,
   3.575 +      allow_consts = false, allow_pats = false} thm (lhs, rhs);
   3.576 +    val _ = if ListPair.all (fn (T, (_, sort)) => Sign.of_sort thy (T, sort)) (Ts, vs) then ()
   3.577        else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   3.578 -  in (thm, tyco) end;
   3.579 +  in (thm, (tyco, abs')) end;
   3.580  
   3.581  in
   3.582  
   3.583 @@ -741,13 +900,13 @@
   3.584  
   3.585  fun concretify_abs thy tyco abs_thm =
   3.586    let
   3.587 -    val (_, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
   3.588 +    val (_, {abstractor = (c_abs, _), abs_rep, ...}) = get_abstype_spec thy tyco;
   3.589      val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm
   3.590      val ty = fastype_of lhs;
   3.591      val ty_abs = (fastype_of o snd o dest_comb) lhs;
   3.592 -    val abs = Thm.global_cterm_of thy (Const (c, ty --> ty_abs));
   3.593 -    val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric cert, Thm.combination (Thm.reflexive abs) abs_thm];
   3.594 -  in (c, (Thm.varifyT_global o zero_var_indexes) raw_concrete_thm) end;
   3.595 +    val abs = Thm.global_cterm_of thy (Const (c_abs, ty --> ty_abs));
   3.596 +    val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric abs_rep, Thm.combination (Thm.reflexive abs) abs_thm];
   3.597 +  in (c_abs, (Thm.varifyT_global o zero_var_indexes) raw_concrete_thm) end;
   3.598  
   3.599  fun add_rhss_of_eqn thy t =
   3.600    let
   3.601 @@ -809,13 +968,13 @@
   3.602          val cert_thm = Conjunction.intr_balanced (map rewrite_head thms');
   3.603        in Equations (cert_thm, propers) end;
   3.604  
   3.605 -fun cert_of_proj ctxt c tyco =
   3.606 +fun cert_of_proj ctxt proj tyco =
   3.607    let
   3.608      val thy = Proof_Context.theory_of ctxt
   3.609 -    val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco;
   3.610 -    val _ = if c = rep then () else
   3.611 -      error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
   3.612 -  in Projection (mk_proj tyco vs ty abs rep, tyco) end;
   3.613 +    val (vs, {abstractor = (abs, (_, ty)), projection = proj', ...}) = get_abstype_spec thy tyco;
   3.614 +    val _ = if proj = proj' then () else
   3.615 +      error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy proj);
   3.616 +  in Projection (mk_proj tyco vs ty abs proj, tyco) end;
   3.617  
   3.618  fun cert_of_abs ctxt tyco c raw_abs_thm =
   3.619    let
   3.620 @@ -900,7 +1059,7 @@
   3.621        in (tyscm, SOME (map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers))) end
   3.622    | equations_of_cert thy (Projection (t, tyco)) =
   3.623        let
   3.624 -        val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
   3.625 +        val (_, {abstractor = (abs, _), ...}) = get_abstype_spec thy tyco;
   3.626          val tyscm = typscheme_projection thy t;
   3.627          val t' = Logic.varify_types_global t;
   3.628          fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE));
   3.629 @@ -916,7 +1075,7 @@
   3.630        end;
   3.631  
   3.632  fun pretty_cert thy (cert as Nothing _) =
   3.633 -      [Pretty.str "(no equations)"]
   3.634 +      [Pretty.str "(unimplemented)"]
   3.635    | pretty_cert thy (cert as Equations _) =
   3.636        (map_filter
   3.637          (Option.map (Thm.pretty_thm_global thy o
   3.638 @@ -933,11 +1092,6 @@
   3.639  
   3.640  (* code certificate access with preprocessing *)
   3.641  
   3.642 -fun retrieve_raw thy c =
   3.643 -  Symtab.lookup ((functions_of o spec_of) thy) c
   3.644 -  |> Option.map (snd o fst)
   3.645 -  |> the_default Unimplemented
   3.646 -
   3.647  fun eqn_conv conv ct =
   3.648    let
   3.649      fun lhs_conv ct = if can Thm.dest_comb ct
   3.650 @@ -967,14 +1121,12 @@
   3.651    end;
   3.652  
   3.653  fun get_cert ctxt functrans c =
   3.654 -  case retrieve_raw (Proof_Context.theory_of ctxt) c of
   3.655 -    Unimplemented => nothing_cert ctxt c
   3.656 -  | Eqns_Default eqns => eqns
   3.657 +  case lookup_proper_fun_spec (specs_of (Proof_Context.theory_of ctxt)) c of
   3.658 +    NONE => nothing_cert ctxt c
   3.659 +  | SOME (Eqns (_, eqns)) => eqns
   3.660        |> cert_of_eqns_preprocess ctxt functrans c
   3.661 -  | Eqns eqns => eqns
   3.662 -      |> cert_of_eqns_preprocess ctxt functrans c
   3.663 -  | Proj (_, tyco) => cert_of_proj ctxt c tyco
   3.664 -  | Abstr (abs_thm, tyco) => abs_thm
   3.665 +  | SOME (Proj (_, (tyco, _))) => cert_of_proj ctxt c tyco
   3.666 +  | SOME (Abstr (abs_thm, (tyco, _))) => abs_thm
   3.667       |> preprocess Conv.arg_conv ctxt
   3.668       |> cert_of_abs ctxt tyco c;
   3.669  
   3.670 @@ -1027,15 +1179,17 @@
   3.671  
   3.672  end;
   3.673  
   3.674 -fun get_case_schema thy c = case Symtab.lookup ((cases_of o spec_of) thy) c of
   3.675 -    SOME (Case (schema, _)) => SOME schema
   3.676 +fun lookup_case_spec thy = History.lookup ((cases_of o specs_of) thy);
   3.677 +
   3.678 +fun get_case_schema thy c = case lookup_case_spec thy c of
   3.679 +    SOME (Case {schema, ...}) => SOME schema
   3.680    | _ => NONE;
   3.681  
   3.682 -fun get_case_cong thy c = case Symtab.lookup ((cases_of o spec_of) thy) c of
   3.683 -    SOME (Case (_, cong)) => SOME cong
   3.684 +fun get_case_cong thy c = case lookup_case_spec thy c of
   3.685 +    SOME (Case {cong, ...}) => SOME cong
   3.686    | _ => NONE;
   3.687  
   3.688 -fun is_undefined thy c = case Symtab.lookup ((cases_of o spec_of) thy) c of
   3.689 +fun is_undefined thy c = case lookup_case_spec thy c of
   3.690      SOME Undefined => true
   3.691    | _ => false;
   3.692  
   3.693 @@ -1045,20 +1199,18 @@
   3.694  fun print_codesetup thy =
   3.695    let
   3.696      val ctxt = Proof_Context.init_global thy;
   3.697 -    val spec = spec_of thy;
   3.698 +    val specs = specs_of thy;
   3.699      fun pretty_equations const thms =
   3.700        (Pretty.block o Pretty.fbreaks)
   3.701          (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
   3.702 -    fun pretty_function (const, Eqns_Default eqns) =
   3.703 -          pretty_equations const (map fst eqns)
   3.704 -      | pretty_function (const, Eqns eqns) =
   3.705 +    fun pretty_function (const, Eqns (_, eqns)) =
   3.706            pretty_equations const (map fst eqns)
   3.707        | pretty_function (const, Proj (proj, _)) = Pretty.block
   3.708            [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
   3.709        | pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm];
   3.710      fun pretty_typ (tyco, vs) = Pretty.str
   3.711        (string_of_typ thy (Type (tyco, map TFree vs)));
   3.712 -    fun pretty_typspec (typ, (cos, abstract)) = if null cos
   3.713 +    fun pretty_type_spec (typ, (cos, abstract)) = if null cos
   3.714        then pretty_typ typ
   3.715        else (Pretty.block o Pretty.breaks) (
   3.716          pretty_typ typ
   3.717 @@ -1071,32 +1223,35 @@
   3.718                        :: Pretty.str "of"
   3.719                        :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
   3.720        );
   3.721 -    fun pretty_caseparam NONE = "<ignored>"
   3.722 -      | pretty_caseparam (SOME c) = string_of_const thy c
   3.723 -    fun pretty_case (const, Case ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
   3.724 -          Pretty.str (string_of_const thy const), Pretty.str "with",
   3.725 -          (Pretty.block o Pretty.commas o map (Pretty.str o pretty_caseparam)) cos]
   3.726 -      | pretty_case (const, _) = Pretty.str (string_of_const thy const)
   3.727 -    val functions = functions_of spec
   3.728 -      |> Symtab.dest
   3.729 -      |> (map o apsnd) (snd o fst)
   3.730 -      |> filter (fn (_, Unimplemented) => false | _ => true)
   3.731 +    fun pretty_case_param NONE = "<ignored>"
   3.732 +      | pretty_case_param (SOME c) = string_of_const thy c
   3.733 +    fun pretty_case (const, Case {schema = (_, (_, [])), ...}) =
   3.734 +          Pretty.str (string_of_const thy const)
   3.735 +      | pretty_case (const, Case {schema = (_, (_, cos)), ...}) =
   3.736 +          (Pretty.block o Pretty.breaks) [
   3.737 +            Pretty.str (string_of_const thy const), Pretty.str "with",
   3.738 +            (Pretty.block o Pretty.commas o map (Pretty.str o pretty_case_param)) cos]
   3.739 +      | pretty_case (const, Undefined) =
   3.740 +          (Pretty.block o Pretty.breaks) [
   3.741 +            Pretty.str (string_of_const thy const), Pretty.str "<undefined>"];
   3.742 +    val functions = all_fun_specs specs
   3.743        |> sort (string_ord o apply2 fst);
   3.744 -    val datatypes = types_of spec
   3.745 -      |> Symtab.dest
   3.746 -      |> map (fn (tyco, (_, (vs, spec)) :: _) =>
   3.747 +    val types = History.all (types_of specs)
   3.748 +      |> map (fn (tyco, (vs, spec)) =>
   3.749            ((tyco, vs), constructors_of spec))
   3.750        |> sort (string_ord o apply2 (fst o fst));
   3.751 -    val cases = Symtab.dest ((cases_of o spec_of) thy);
   3.752 +    val cases = History.all (cases_of specs)
   3.753 +      |> filter (fn (_, No_Case) => false | _ => true)
   3.754 +      |> sort (string_ord o apply2 fst);
   3.755    in
   3.756      Pretty.writeln_chunks [
   3.757        Pretty.block (
   3.758 -        Pretty.str "code equations:" :: Pretty.fbrk
   3.759 -        :: (Pretty.fbreaks o map pretty_function) functions
   3.760 +        Pretty.str "types:" :: Pretty.fbrk
   3.761 +        :: (Pretty.fbreaks o map pretty_type_spec) types
   3.762        ),
   3.763        Pretty.block (
   3.764 -        Pretty.str "datatypes:" :: Pretty.fbrk
   3.765 -        :: (Pretty.fbreaks o map pretty_typspec) datatypes
   3.766 +        Pretty.str "functions:" :: Pretty.fbrk
   3.767 +        :: (Pretty.fbreaks o map pretty_function) functions
   3.768        ),
   3.769        Pretty.block (
   3.770          Pretty.str "cases:" :: Pretty.fbrk
   3.771 @@ -1106,9 +1261,103 @@
   3.772    end;
   3.773  
   3.774  
   3.775 -(** declaring executable ingredients **)
   3.776 +(** declaration of executable ingredients **)
   3.777 +
   3.778 +(* abstract code declarations *)
   3.779 +
   3.780 +local
   3.781 +
   3.782 +fun generic_code_declaration strictness lift_phi f x =
   3.783 +  Local_Theory.declaration
   3.784 +    {syntax = false, pervasive = false}
   3.785 +    (fn phi => Context.mapping (f strictness (lift_phi phi x)) I);
   3.786 +
   3.787 +in
   3.788 +
   3.789 +fun silent_code_declaration lift_phi = generic_code_declaration Silent lift_phi;
   3.790 +fun code_declaration lift_phi = generic_code_declaration Liberal lift_phi;
   3.791 +
   3.792 +end;
   3.793 +
   3.794 +
   3.795 +(* types *)
   3.796 +
   3.797 +fun invalidate_constructors_of (_, type_spec) =
   3.798 +  fold (fn (c, _) => History.register c unimplemented) (fst (constructors_of type_spec));
   3.799 +
   3.800 +fun invalidate_abstract_functions_of (_, type_spec) =
   3.801 +  fold (fn c => History.register c unimplemented) (abstract_functions_of type_spec);
   3.802 +
   3.803 +fun invalidate_case_combinators_of (_, type_spec) =
   3.804 +  fold (fn c => History.register c No_Case) (case_combinators_of type_spec);
   3.805 +
   3.806 +fun register_type (tyco, vs_typ_spec) specs =
   3.807 +  let
   3.808 +    val olds = the_list (History.lookup (types_of specs) tyco);
   3.809 +  in
   3.810 +    specs
   3.811 +    |> map_functions (fold invalidate_abstract_functions_of olds
   3.812 +        #> invalidate_constructors_of vs_typ_spec)
   3.813 +    |> map_cases (fold invalidate_case_combinators_of olds)
   3.814 +    |> map_types (History.register tyco vs_typ_spec)
   3.815 +  end;
   3.816 +
   3.817 +structure Datatype_Plugin = Plugin(type T = string);
   3.818 +
   3.819 +val datatype_plugin = Plugin_Name.declare_setup @{binding datatype_code};
   3.820  
   3.821 -(* code equations *)
   3.822 +fun datatype_interpretation f =
   3.823 +  Datatype_Plugin.interpretation datatype_plugin
   3.824 +    (fn tyco => Local_Theory.background_theory (fn thy =>
   3.825 +      thy
   3.826 +      |> Sign.root_path
   3.827 +      |> Sign.add_path (Long_Name.qualifier tyco)
   3.828 +      |> f (tyco, fst (get_type thy tyco))
   3.829 +      |> Sign.restore_naming thy));
   3.830 +
   3.831 +fun declare_datatype_global proto_constrs thy =
   3.832 +  let
   3.833 +    fun unoverload_const_typ (c, ty) =
   3.834 +      (Axclass.unoverload_const thy (c, ty), ty);
   3.835 +    val constrs = map unoverload_const_typ proto_constrs;
   3.836 +    val (tyco, (vs, cos)) = constrset_of_consts thy constrs;
   3.837 +  in
   3.838 +    thy
   3.839 +    |> modify_specs (register_type
   3.840 +        (tyco, (vs, Constructors {constructors = cos, case_combinators = []})))
   3.841 +    |> Named_Target.theory_map (Datatype_Plugin.data_default tyco)
   3.842 +  end;
   3.843 +
   3.844 +fun declare_datatype_cmd raw_constrs thy =
   3.845 +  declare_datatype_global (map (read_bare_const thy) raw_constrs) thy;
   3.846 +
   3.847 +structure Abstype_Plugin = Plugin(type T = string);
   3.848 +
   3.849 +val abstype_plugin = Plugin_Name.declare_setup @{binding abstype_code};
   3.850 +
   3.851 +fun abstype_interpretation f =
   3.852 +  Abstype_Plugin.interpretation abstype_plugin
   3.853 +    (fn tyco =>
   3.854 +      Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy));
   3.855 +
   3.856 +fun generic_declare_abstype strictness proto_thm thy =
   3.857 +  case check_abstype_cert strictness thy proto_thm of
   3.858 +    SOME (tyco, (vs, (abstractor as (abs, (_, ty)), (proj, abs_rep)))) =>
   3.859 +      thy
   3.860 +      |> modify_specs (register_type
   3.861 +            (tyco, (vs, Abstractor {abstractor = abstractor, projection = proj, abs_rep = abs_rep, more_abstract_functions = []}))
   3.862 +          #> register_fun_spec proj
   3.863 +            (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs proj), (tyco, abs))))
   3.864 +      |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
   3.865 +  | NONE => thy;
   3.866 +
   3.867 +val declare_abstype_global = generic_declare_abstype Strict;
   3.868 +
   3.869 +val declare_abstype =
   3.870 +  code_declaration Morphism.thm generic_declare_abstype;
   3.871 +
   3.872 +
   3.873 +(* functions *)
   3.874  
   3.875  (*
   3.876    strictness wrt. shape of theorem propositions:
   3.877 @@ -1118,14 +1367,6 @@
   3.878      * internal processing after storage: strict
   3.879  *)
   3.880  
   3.881 -fun generic_code_declaration strictness lift_phi f x =
   3.882 -  Local_Theory.declaration
   3.883 -    {syntax = false, pervasive = false}
   3.884 -    (fn phi => Context.mapping (f strictness (lift_phi phi x)) I);
   3.885 -
   3.886 -fun silent_code_declaration lift_phi = generic_code_declaration Silent lift_phi;
   3.887 -fun code_declaration lift_phi = generic_code_declaration Liberal lift_phi;
   3.888 -
   3.889  local
   3.890  
   3.891  fun subsumptive_add thy verbose (thm, proper) eqns =
   3.892 @@ -1148,26 +1389,24 @@
   3.893        else false;
   3.894    in (thm, proper) :: filter_out drop eqns end;
   3.895  
   3.896 -fun add_eqn_for (c, proto_eqn) thy =
   3.897 -  let
   3.898 -    val eqn = apfst Thm.close_derivation proto_eqn;
   3.899 -    fun add (Eqns eqns) = Eqns (subsumptive_add thy true eqn eqns)
   3.900 -      | add _ = Eqns [eqn];
   3.901 -  in change_fun_spec c add thy end;
   3.902 +fun add_eqn_for (c, eqn) thy =
   3.903 +  thy |> modify_specs (modify_pending_eqns c
   3.904 +    (subsumptive_add thy true (apfst Thm.close_derivation eqn)));
   3.905  
   3.906  fun add_eqns_for default (c, proto_eqns) thy =
   3.907 -  let
   3.908 -    val eqns = []
   3.909 -      |> fold_rev (subsumptive_add thy (not default)) proto_eqns
   3.910 -      |> (map o apfst) Thm.close_derivation;
   3.911 -    fun add (Eqns_Default _) = Eqns_Default eqns
   3.912 -      | add data = data;
   3.913 -  in change_fun_spec c (if default then add else K (Eqns eqns)) thy end;
   3.914 +  thy |> modify_specs (fn specs =>
   3.915 +    if is_default (lookup_fun_spec specs c) orelse not default
   3.916 +    then
   3.917 +      let
   3.918 +        val eqns = []
   3.919 +          |> fold_rev (subsumptive_add thy (not default)) proto_eqns
   3.920 +          |> (map o apfst) Thm.close_derivation;
   3.921 +      in specs |> register_fun_spec c (Eqns (default, eqns)) end
   3.922 +    else specs);
   3.923  
   3.924 -fun add_abstract_for (c, proto_abs_eqn) =
   3.925 -  let
   3.926 -    val abs_eqn = apfst Thm.close_derivation proto_abs_eqn;
   3.927 -  in change_fun_spec c (K (Abstr abs_eqn)) end;
   3.928 +fun add_abstract_for (c, (thm, tyco_abs as (tyco, _))) =
   3.929 +  modify_specs (register_fun_spec c (Abstr (Thm.close_derivation thm, tyco_abs))
   3.930 +    #> map_types (History.modify_entry tyco (add_abstract_function c)))
   3.931  
   3.932  in
   3.933  
   3.934 @@ -1203,12 +1442,7 @@
   3.935  fun del_eqn_global thm thy =
   3.936    case prep_eqn Liberal thy (thm, false) of
   3.937      SOME (c, (thm, _)) =>
   3.938 -      let
   3.939 -        fun del (Eqns_Default _) = Eqns []
   3.940 -          | del (Eqns eqns) =
   3.941 -              Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
   3.942 -          | del spec = spec
   3.943 -      in change_fun_spec c del thy end
   3.944 +      modify_specs (modify_pending_eqns c (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')))) thy
   3.945    | NONE => thy;
   3.946  
   3.947  val declare_abstract_eqn_global = generic_declare_abstract_eqn Strict;
   3.948 @@ -1216,9 +1450,11 @@
   3.949  val declare_abstract_eqn =
   3.950    code_declaration Morphism.thm generic_declare_abstract_eqn;
   3.951  
   3.952 -fun declare_empty_global c = change_fun_spec c (K (Eqns []));
   3.953 +fun declare_aborting_global c = 
   3.954 +  modify_specs (register_fun_spec c aborting);
   3.955  
   3.956 -fun declare_unimplemented_global c = change_fun_spec c (K Unimplemented);
   3.957 +fun declare_unimplemented_global c =
   3.958 +  modify_specs (register_fun_spec c unimplemented);
   3.959  
   3.960  
   3.961  (* cases *)
   3.962 @@ -1244,113 +1480,30 @@
   3.963  fun declare_case_global thm thy =
   3.964    let
   3.965      val (case_const, (k, cos)) = case_cert thm;
   3.966 -    val _ = case (filter_out (is_constr thy) o map_filter I) cos
   3.967 -     of [] => ()
   3.968 +    fun get_type_of_constr c = case get_type_of_constr_or_abstr thy c of
   3.969 +        SOME (c, false) => SOME c
   3.970 +      | _ => NONE;
   3.971 +    val cos_with_tycos =
   3.972 +      (map_filter o Option.map) (fn c => (c, get_type_of_constr c)) cos;
   3.973 +    val _ = case map_filter (fn (c, NONE) => SOME c | _ => NONE) cos_with_tycos of
   3.974 +        [] => ()
   3.975        | cs => error ("Non-constructor(s) in case certificate: " ^ commas_quote cs);
   3.976 -    val entry = (1 + Int.max (1, length cos), (k, cos));
   3.977 -    fun register_case cong = map_cases
   3.978 -      (Symtab.update (case_const, Case (entry, cong)));
   3.979 -    fun register_for_constructors (Constructors (cos', cases)) =
   3.980 -         Constructors (cos',
   3.981 -           if exists (fn (co, _) => member (op =) cos (SOME co)) cos'
   3.982 -           then insert (op =) case_const cases
   3.983 -           else cases)
   3.984 -      | register_for_constructors (x as Abstractor _) = x;
   3.985 -    val register_type = (map_types o Symtab.map)
   3.986 -      (K ((map o apsnd o apsnd) register_for_constructors));
   3.987 +    val tycos = distinct (op =) (map_filter snd cos_with_tycos);
   3.988 +    val schema = (1 + Int.max (1, length cos), (k, cos));
   3.989 +    val cong = case_cong thy case_const schema;
   3.990    in
   3.991      thy
   3.992 -    |> `(fn thy => case_cong thy case_const entry)
   3.993 -    |-> (fn cong => map_spec_purge (register_case cong #> register_type))
   3.994 +    |> modify_specs (map_cases (History.register case_const
   3.995 +         (Case {schema = schema, tycos = tycos, cong = cong}))
   3.996 +      #> map_types (fold (fn tyco => History.modify_entry tyco
   3.997 +        (add_case_combinator case_const)) tycos))
   3.998    end;
   3.999  
  3.1000  fun declare_undefined_global c =
  3.1001 -  (map_spec_purge o map_cases) (Symtab.update (c, Undefined));
  3.1002 +  (modify_specs o map_cases) (History.register c Undefined);
  3.1003  
  3.1004  
  3.1005 -(* types *)
  3.1006 -
  3.1007 -fun register_type (tyco, vs_spec) thy =
  3.1008 -  let
  3.1009 -    val (old_constrs, some_old_proj) =
  3.1010 -      case these (Symtab.lookup ((types_of o spec_of) thy) tyco)
  3.1011 -       of (_, (_, Constructors (cos, _))) :: _ => (map fst cos, NONE)
  3.1012 -        | (_, (_, Abstractor ((co, _), (proj, _)))) :: _ => ([co], SOME proj)
  3.1013 -        | [] => ([], NONE);
  3.1014 -    val outdated_funs1 = (map fst o fst o constructors_of o snd) vs_spec;
  3.1015 -    val outdated_funs2 = case some_old_proj
  3.1016 -     of NONE => []
  3.1017 -      | SOME old_proj => Symtab.fold
  3.1018 -          (fn (c, ((_, spec), _)) =>
  3.1019 -            if member (op =) (the_list (associated_abstype spec)) tyco
  3.1020 -            then insert (op =) c else I)
  3.1021 -            ((functions_of o spec_of) thy) [old_proj];
  3.1022 -    fun drop_outdated_cases cases = fold Symtab.delete_safe
  3.1023 -      (Symtab.fold (fn (c, Case ((_, (_, cos)), _)) =>
  3.1024 -        if exists (member (op =) old_constrs) (map_filter I cos)
  3.1025 -          then insert (op =) c else I | _ => I) cases []) cases;
  3.1026 -  in
  3.1027 -    thy
  3.1028 -    |> fold declare_unimplemented_global (outdated_funs1 @ outdated_funs2)
  3.1029 -    |> map_spec_purge
  3.1030 -        ((map_types o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
  3.1031 -        #> map_cases drop_outdated_cases)
  3.1032 -  end;
  3.1033 -
  3.1034 -structure Datatype_Plugin = Plugin(type T = string);
  3.1035 -
  3.1036 -val datatype_plugin = Plugin_Name.declare_setup @{binding datatype_code};
  3.1037 -
  3.1038 -fun datatype_interpretation f =
  3.1039 -  Datatype_Plugin.interpretation datatype_plugin
  3.1040 -    (fn tyco => Local_Theory.background_theory (fn thy =>
  3.1041 -      thy
  3.1042 -      |> Sign.root_path
  3.1043 -      |> Sign.add_path (Long_Name.qualifier tyco)
  3.1044 -      |> f (tyco, fst (get_type thy tyco))
  3.1045 -      |> Sign.restore_naming thy));
  3.1046 -
  3.1047 -fun declare_datatype_global proto_constrs thy =
  3.1048 -  let
  3.1049 -    fun unoverload_const_typ (c, ty) =
  3.1050 -      (Axclass.unoverload_const thy (c, ty), ty);
  3.1051 -    val constrs = map unoverload_const_typ proto_constrs;
  3.1052 -    val (tyco, (vs, cos)) = constrset_of_consts thy constrs;
  3.1053 -  in
  3.1054 -    thy
  3.1055 -    |> register_type (tyco, (vs, Constructors (cos, [])))
  3.1056 -    |> Named_Target.theory_map (Datatype_Plugin.data_default tyco)
  3.1057 -  end;
  3.1058 -
  3.1059 -fun declare_datatype_cmd raw_constrs thy =
  3.1060 -  declare_datatype_global (map (read_bare_const thy) raw_constrs) thy;
  3.1061 -
  3.1062 -structure Abstype_Plugin = Plugin(type T = string);
  3.1063 -
  3.1064 -val abstype_plugin = Plugin_Name.declare_setup @{binding abstype_code};
  3.1065 -
  3.1066 -fun abstype_interpretation f =
  3.1067 -  Abstype_Plugin.interpretation abstype_plugin
  3.1068 -    (fn tyco =>
  3.1069 -      Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy));
  3.1070 -
  3.1071 -fun generic_declare_abstype strictness proto_thm thy =
  3.1072 -  case check_abstype_cert strictness thy proto_thm of
  3.1073 -    SOME (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =>
  3.1074 -      thy
  3.1075 -      |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
  3.1076 -      |> change_fun_spec rep
  3.1077 -        (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
  3.1078 -      |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
  3.1079 -  | NONE => thy;
  3.1080 -
  3.1081 -val declare_abstype_global = generic_declare_abstype Strict;
  3.1082 -
  3.1083 -val declare_abstype =
  3.1084 -  code_declaration Morphism.thm generic_declare_abstype;
  3.1085 -
  3.1086 -
  3.1087 -(* setup *)
  3.1088 +(* attributes *)
  3.1089  
  3.1090  fun code_attribute f = Thm.declaration_attribute
  3.1091    (fn thm => Context.mapping (f thm) I);
  3.1092 @@ -1371,7 +1524,7 @@
  3.1093            (generic_declare_abstype Liberal))
  3.1094        || Args.del |-- Scan.succeed (code_attribute del_eqn_global)
  3.1095        || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term
  3.1096 -          >> code_const_attribute declare_empty_global)
  3.1097 +          >> code_const_attribute declare_aborting_global)
  3.1098        || Args.$$$ "drop" -- Args.colon |-- (Scan.repeat1 Parse.term
  3.1099            >> code_const_attribute declare_unimplemented_global)
  3.1100        || Scan.succeed (code_attribute