tuned structure Code internally
authorhaftmann
Wed Jul 08 08:18:07 2009 +0200 (2009-07-08)
changeset 31962baa8dce5bc45
parent 31961 683b5e3b31fc
child 31967 81dbc693143b
tuned structure Code internally
src/HOL/Tools/recfun_codegen.ML
src/Pure/Isar/code.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Wed Jul 08 06:43:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Wed Jul 08 08:18:07 2009 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  fun add_thm NONE thm thy = Code.add_eqn thm thy
     1.5    | add_thm (SOME module_name) thm thy =
     1.6        let
     1.7 -        val (thm', _) = Code.mk_eqn thy (K false) (thm, true)
     1.8 +        val (thm', _) = Code.mk_eqn thy (thm, true)
     1.9        in
    1.10          thy
    1.11          |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
     2.1 --- a/src/Pure/Isar/code.ML	Wed Jul 08 06:43:30 2009 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Wed Jul 08 08:18:07 2009 +0200
     2.3 @@ -1,18 +1,18 @@
     2.4  (*  Title:      Pure/Isar/code.ML
     2.5      Author:     Florian Haftmann, TU Muenchen
     2.6  
     2.7 -Abstract executable content of theory.  Management of data dependent on
     2.8 -executable content.  Cache assumes non-concurrent processing of a single theory.
     2.9 +Abstract executable code of theory.  Management of data dependent on
    2.10 +executable code.  Cache assumes non-concurrent processing of a single theory.
    2.11  *)
    2.12  
    2.13  signature CODE =
    2.14  sig
    2.15    (*constants*)
    2.16 -  val string_of_const: theory -> string -> string
    2.17 -  val args_number: theory -> string -> int
    2.18    val check_const: theory -> term -> string
    2.19    val read_bare_const: theory -> string -> string * typ
    2.20    val read_const: theory -> string -> string
    2.21 +  val string_of_const: theory -> string -> string
    2.22 +  val args_number: theory -> string -> int
    2.23    val typscheme: theory -> string * typ -> (string * sort) list * typ
    2.24  
    2.25    (*constructor sets*)
    2.26 @@ -25,9 +25,9 @@
    2.27    val resubst_alias: theory -> string -> string
    2.28  
    2.29    (*code equations*)
    2.30 -  val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
    2.31 -  val mk_eqn_warning: theory -> (string -> bool) -> thm -> (thm * bool) option
    2.32 -  val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option
    2.33 +  val mk_eqn: theory -> thm * bool -> thm * bool
    2.34 +  val mk_eqn_warning: theory -> thm -> (thm * bool) option
    2.35 +  val mk_eqn_liberal: theory -> thm -> (thm * bool) option
    2.36    val assert_eqn: theory -> thm * bool -> thm * bool
    2.37    val assert_eqns_const: theory -> string
    2.38      -> (thm * bool) list -> (thm * bool) list
    2.39 @@ -37,7 +37,7 @@
    2.40    val norm_args: theory -> thm list -> thm list 
    2.41    val norm_varnames: theory -> thm list -> thm list
    2.42  
    2.43 -  (*executable content*)
    2.44 +  (*executable code*)
    2.45    val add_datatype: (string * typ) list -> theory -> theory
    2.46    val add_datatype_cmd: string list -> theory -> theory
    2.47    val type_interpretation:
    2.48 @@ -97,23 +97,37 @@
    2.49  structure Code : PRIVATE_CODE =
    2.50  struct
    2.51  
    2.52 -(* auxiliary *)
    2.53 +(** auxiliary **)
    2.54 +
    2.55 +(* printing *)
    2.56  
    2.57  fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy);
    2.58 +
    2.59  fun string_of_const thy c = case AxClass.inst_of_param thy c
    2.60   of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
    2.61    | NONE => Sign.extern_const thy c;
    2.62  
    2.63 -fun args_number thy = length o fst o strip_type o Sign.the_const_type thy;
    2.64 +
    2.65 +(* constants *)
    2.66  
    2.67 +fun check_bare_const thy t = case try dest_Const t
    2.68 + of SOME c_ty => c_ty
    2.69 +  | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
    2.70  
    2.71 -(* utilities *)
    2.72 +fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
    2.73 +
    2.74 +fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
    2.75 +
    2.76 +fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
    2.77  
    2.78  fun typscheme thy (c, ty) =
    2.79    let
    2.80      val ty' = Logic.unvarifyT ty;
    2.81    in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end;
    2.82  
    2.83 +
    2.84 +(* code equation transformations *)
    2.85 +
    2.86  fun expand_eta thy k thm =
    2.87    let
    2.88      val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
    2.89 @@ -221,62 +235,272 @@
    2.90    end;
    2.91  
    2.92  
    2.93 -(* reading constants as terms *)
    2.94 -
    2.95 -fun check_bare_const thy t = case try dest_Const t
    2.96 - of SOME c_ty => c_ty
    2.97 -  | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
    2.98 -
    2.99 -fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
   2.100 -
   2.101 -fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
   2.102 +(** code attributes **)
   2.103  
   2.104 -fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
   2.105 -
   2.106 -
   2.107 -(* const aliasses *)
   2.108 -
   2.109 -structure ConstAlias = TheoryDataFun
   2.110 -(
   2.111 -  type T = ((string * string) * thm) list * class list;
   2.112 -  val empty = ([], []);
   2.113 +structure Code_Attr = TheoryDataFun (
   2.114 +  type T = (string * attribute parser) list;
   2.115 +  val empty = [];
   2.116    val copy = I;
   2.117    val extend = I;
   2.118 -  fun merge _ ((alias1, classes1), (alias2, classes2)) : T =
   2.119 -    (Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2),
   2.120 -      Library.merge (op =) (classes1, classes2));
   2.121 +  fun merge _ = AList.merge (op = : string * string -> bool) (K true);
   2.122  );
   2.123  
   2.124 -fun add_const_alias thm thy =
   2.125 +fun add_attribute (attr as (name, _)) =
   2.126 +  let
   2.127 +    fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
   2.128 +      | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
   2.129 +  in Code_Attr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name
   2.130 +    then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
   2.131 +  end;
   2.132 +
   2.133 +val _ = Context.>> (Context.map_theory
   2.134 +  (Attrib.setup (Binding.name "code")
   2.135 +    (Scan.peek (fn context =>
   2.136 +      List.foldr op || Scan.fail (map snd (Code_Attr.get (Context.theory_of context)))))
   2.137 +    "declare theorems for code generation"));
   2.138 +
   2.139 +
   2.140 +(** data store **)
   2.141 +
   2.142 +(* code equations *)
   2.143 +
   2.144 +type eqns = bool * (thm * bool) list lazy;
   2.145 +  (*default flag, theorems with proper flag (perhaps lazy)*)
   2.146 +
   2.147 +fun pretty_lthms ctxt r = case Lazy.peek r
   2.148 + of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
   2.149 +  | NONE => [Pretty.str "[...]"];
   2.150 +
   2.151 +fun certificate thy f r =
   2.152 +  case Lazy.peek r
   2.153 +   of SOME thms => (Lazy.value o f thy) (Exn.release thms)
   2.154 +    | NONE => let
   2.155 +        val thy_ref = Theory.check_thy thy;
   2.156 +      in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end;
   2.157 +
   2.158 +fun add_drop_redundant thy (thm, proper) thms =
   2.159 +  let
   2.160 +    val args_of = snd o strip_comb o map_types Type.strip_sorts
   2.161 +      o fst o Logic.dest_equals o Thm.plain_prop_of;
   2.162 +    val args = args_of thm;
   2.163 +    val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
   2.164 +    fun matches_args args' = length args <= length args' andalso
   2.165 +      Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
   2.166 +    fun drop (thm', proper') = if (proper orelse not proper')
   2.167 +      andalso matches_args (args_of thm') then 
   2.168 +        (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true)
   2.169 +      else false;
   2.170 +  in (thm, proper) :: filter_out drop thms end;
   2.171 +
   2.172 +fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms)
   2.173 +  | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms)
   2.174 +  | add_thm thy false thm (true, thms) = (false, Lazy.value [thm]);
   2.175 +
   2.176 +fun add_lthms lthms _ = (false, lthms);
   2.177 +
   2.178 +fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
   2.179 +
   2.180 +
   2.181 +(* executable code data *)
   2.182 +
   2.183 +datatype spec = Spec of {
   2.184 +  history_concluded: bool,
   2.185 +  aliasses: ((string * string) * thm) list * class list,
   2.186 +  eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table
   2.187 +    (*with explicit history*),
   2.188 +  dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table
   2.189 +    (*with explicit history*),
   2.190 +  cases: (int * (int * string list)) Symtab.table * unit Symtab.table
   2.191 +};
   2.192 +
   2.193 +fun make_spec ((history_concluded, aliasses), (eqns, (dtyps, cases))) =
   2.194 +  Spec { history_concluded = history_concluded, aliasses = aliasses,
   2.195 +    eqns = eqns, dtyps = dtyps, cases = cases };
   2.196 +fun map_spec f (Spec { history_concluded = history_concluded, aliasses = aliasses, eqns = eqns,
   2.197 +  dtyps = dtyps, cases = cases }) =
   2.198 +  make_spec (f ((history_concluded, aliasses), (eqns, (dtyps, cases))));
   2.199 +fun merge_spec (Spec { history_concluded = _, aliasses = aliasses1, eqns = eqns1,
   2.200 +    dtyps = dtyps1, cases = (cases1, undefs1) },
   2.201 +  Spec { history_concluded = _, aliasses = aliasses2, eqns = eqns2,
   2.202 +    dtyps = dtyps2, cases = (cases2, undefs2) }) =
   2.203    let
   2.204 -    val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm)
   2.205 -     of SOME ofclass_eq => ofclass_eq
   2.206 -      | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
   2.207 -    val (T, class) = case try Logic.dest_of_class ofclass
   2.208 -     of SOME T_class => T_class
   2.209 -      | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
   2.210 -    val tvar = case try Term.dest_TVar T
   2.211 -     of SOME tvar => tvar
   2.212 -      | _ => error ("Bad type: " ^ Display.string_of_thm thm);
   2.213 -    val _ = if Term.add_tvars eqn [] = [tvar] then ()
   2.214 -      else error ("Inconsistent type: " ^ Display.string_of_thm thm);
   2.215 -    val lhs_rhs = case try Logic.dest_equals eqn
   2.216 -     of SOME lhs_rhs => lhs_rhs
   2.217 -      | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
   2.218 -    val c_c' = case try (pairself (check_const thy)) lhs_rhs
   2.219 -     of SOME c_c' => c_c'
   2.220 -      | _ => error ("Not an equation with two constants: "
   2.221 -          ^ Syntax.string_of_term_global thy eqn);
   2.222 -    val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
   2.223 -      else error ("Inconsistent class: " ^ Display.string_of_thm thm);
   2.224 -  in thy |>
   2.225 -    ConstAlias.map (fn (alias, classes) =>
   2.226 -      ((c_c', thm) :: alias, insert (op =) class classes))
   2.227 -  end;
   2.228 +    val aliasses = (Library.merge (eq_snd Thm.eq_thm_prop) (pairself fst (aliasses1, aliasses2)),
   2.229 +      Library.merge (op =) (pairself snd (aliasses1, aliasses2)));
   2.230 +    fun merge_eqns ((_, history1), (_, history2)) =
   2.231 +      let
   2.232 +        val raw_history = AList.merge (op = : serial * serial -> bool)
   2.233 +          (K true) (history1, history2)
   2.234 +        val filtered_history = filter_out (fst o snd) raw_history
   2.235 +        val history = if null filtered_history
   2.236 +          then raw_history else filtered_history;
   2.237 +      in ((false, (snd o hd) history), history) end;
   2.238 +    val eqns = Symtab.join (K merge_eqns) (eqns1, eqns2);
   2.239 +    val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2);
   2.240 +    val cases = (Symtab.merge (K true) (cases1, cases2),
   2.241 +      Symtab.merge (K true) (undefs1, undefs2));
   2.242 +  in make_spec ((false, aliasses), (eqns, (dtyps, cases))) end;
   2.243 +
   2.244 +fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
   2.245 +fun the_aliasses (Spec { aliasses, ... }) = aliasses;
   2.246 +fun the_eqns (Spec { eqns, ... }) = eqns;
   2.247 +fun the_dtyps (Spec { dtyps, ... }) = dtyps;
   2.248 +fun the_cases (Spec { cases, ... }) = cases;
   2.249 +val map_history_concluded = map_spec o apfst o apfst;
   2.250 +val map_aliasses = map_spec o apfst o apsnd;
   2.251 +val map_eqns = map_spec o apsnd o apfst;
   2.252 +val map_dtyps = map_spec o apsnd o apsnd o apfst;
   2.253 +val map_cases = map_spec o apsnd o apsnd o apsnd;
   2.254 +
   2.255 +
   2.256 +(* data slots dependent on executable code *)
   2.257 +
   2.258 +(*private copy avoids potential conflict of table exceptions*)
   2.259 +structure Datatab = TableFun(type key = int val ord = int_ord);
   2.260 +
   2.261 +local
   2.262 +
   2.263 +type kind = {
   2.264 +  empty: Object.T,
   2.265 +  purge: theory -> string list -> Object.T -> Object.T
   2.266 +};
   2.267 +
   2.268 +val kinds = ref (Datatab.empty: kind Datatab.table);
   2.269 +val kind_keys = ref ([]: serial list);
   2.270 +
   2.271 +fun invoke f k = case Datatab.lookup (! kinds) k
   2.272 + of SOME kind => f kind
   2.273 +  | NONE => sys_error "Invalid code data identifier";
   2.274 +
   2.275 +in
   2.276 +
   2.277 +fun declare_data empty purge =
   2.278 +  let
   2.279 +    val k = serial ();
   2.280 +    val kind = {empty = empty, purge = purge};
   2.281 +    val _ = change kinds (Datatab.update (k, kind));
   2.282 +    val _ = change kind_keys (cons k);
   2.283 +  in k end;
   2.284 +
   2.285 +fun invoke_init k = invoke (fn kind => #empty kind) k;
   2.286 +
   2.287 +fun invoke_purge_all thy cs =
   2.288 +  fold (fn k => Datatab.map_entry k
   2.289 +    (invoke (fn kind => #purge kind thy cs) k)) (! kind_keys);
   2.290 +
   2.291 +end; (*local*)
   2.292 +
   2.293 +
   2.294 +(* theory store *)
   2.295 +
   2.296 +local
   2.297 +
   2.298 +type data = Object.T Datatab.table;
   2.299 +val empty_data = Datatab.empty : data;
   2.300 +
   2.301 +structure Code_Data = TheoryDataFun
   2.302 +(
   2.303 +  type T = spec * data ref;
   2.304 +  val empty = (make_spec ((false, ([], [])),
   2.305 +    (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), ref empty_data);
   2.306 +  fun copy (spec, data) = (spec, ref (! data));
   2.307 +  val extend = copy;
   2.308 +  fun merge pp ((spec1, data1), (spec2, data2)) =
   2.309 +    (merge_spec (spec1, spec2), ref empty_data);
   2.310 +);
   2.311 +
   2.312 +fun thy_data f thy = f ((snd o Code_Data.get) thy);
   2.313 +
   2.314 +fun get_ensure_init kind data_ref =
   2.315 +  case Datatab.lookup (! data_ref) kind
   2.316 +   of SOME x => x
   2.317 +    | NONE => let val y = invoke_init kind
   2.318 +        in (change data_ref (Datatab.update (kind, y)); y) end;
   2.319 +
   2.320 +in
   2.321 +
   2.322 +(* access to executable code *)
   2.323 +
   2.324 +val the_exec = fst o Code_Data.get;
   2.325 +
   2.326 +fun complete_class_params thy cs =
   2.327 +  fold (fn c => case AxClass.inst_of_param thy c
   2.328 +   of NONE => insert (op =) c
   2.329 +    | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
   2.330 +
   2.331 +fun map_exec_purge touched f thy =
   2.332 +  Code_Data.map (fn (exec, data) => (f exec, ref (case touched
   2.333 +   of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
   2.334 +    | NONE => empty_data))) thy;
   2.335 +
   2.336 +val purge_data = (Code_Data.map o apsnd) (K (ref empty_data));
   2.337 +
   2.338 +fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
   2.339 +  o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
   2.340 +    o apfst) (fn (_, eqns) => (true, f eqns));
   2.341 +
   2.342 +fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
   2.343 +
   2.344 +
   2.345 +(* tackling equation history *)
   2.346 +
   2.347 +fun get_eqns thy c =
   2.348 +  Symtab.lookup ((the_eqns o the_exec) thy) c
   2.349 +  |> Option.map (Lazy.force o snd o snd o fst)
   2.350 +  |> these;
   2.351 +
   2.352 +fun continue_history thy = if (history_concluded o the_exec) thy
   2.353 +  then thy
   2.354 +    |> (Code_Data.map o apfst o map_history_concluded) (K false)
   2.355 +    |> SOME
   2.356 +  else NONE;
   2.357 +
   2.358 +fun conclude_history thy = if (history_concluded o the_exec) thy
   2.359 +  then NONE
   2.360 +  else thy
   2.361 +    |> (Code_Data.map o apfst)
   2.362 +        ((map_eqns o Symtab.map) (fn ((changed, current), history) =>
   2.363 +          ((false, current),
   2.364 +            if changed then (serial (), current) :: history else history))
   2.365 +        #> map_history_concluded (K true))
   2.366 +    |> SOME;
   2.367 +
   2.368 +val _ = Context.>> (Context.map_theory (Code_Data.init
   2.369 +  #> Theory.at_begin continue_history
   2.370 +  #> Theory.at_end conclude_history));
   2.371 +
   2.372 +
   2.373 +(* access to data dependent on abstract executable code *)
   2.374 +
   2.375 +fun get_data (kind, _, dest) = thy_data (get_ensure_init kind #> dest);
   2.376 +
   2.377 +fun change_data (kind, mk, dest) =
   2.378 +  let
   2.379 +    fun chnge data_ref f =
   2.380 +      let
   2.381 +        val data = get_ensure_init kind data_ref;
   2.382 +        val data' = f (dest data);
   2.383 +      in (change data_ref (Datatab.update (kind, mk data')); data') end;
   2.384 +  in thy_data chnge end;
   2.385 +
   2.386 +fun change_yield_data (kind, mk, dest) =
   2.387 +  let
   2.388 +    fun chnge data_ref f =
   2.389 +      let
   2.390 +        val data = get_ensure_init kind data_ref;
   2.391 +        val (x, data') = f (dest data);
   2.392 +      in (x, (change data_ref (Datatab.update (kind, mk data')); data')) end;
   2.393 +  in thy_data chnge end;
   2.394 +
   2.395 +end; (*local*)
   2.396 +
   2.397 +
   2.398 +(** retrieval interfaces **)
   2.399 +
   2.400 +(* constant aliasses *)
   2.401  
   2.402  fun resubst_alias thy =
   2.403    let
   2.404 -    val alias = fst (ConstAlias.get thy);
   2.405 +    val alias = (fst o the_aliasses o the_exec) thy;
   2.406      val subst_inst_param = Option.map fst o AxClass.inst_of_param thy;
   2.407      fun subst_alias c =
   2.408        get_first (fn ((c', c''), _) => if c = c'' then SOME c' else NONE) alias;
   2.409 @@ -285,10 +509,17 @@
   2.410      #> perhaps subst_alias
   2.411    end;
   2.412  
   2.413 -val triv_classes = snd o ConstAlias.get;
   2.414 +val triv_classes = snd o the_aliasses o the_exec;
   2.415  
   2.416  
   2.417 -(* constructor sets *)
   2.418 +(** foundation **)
   2.419 +
   2.420 +(* constants *)
   2.421 +
   2.422 +fun args_number thy = length o fst o strip_type o Sign.the_const_type thy;
   2.423 +
   2.424 +
   2.425 +(* datatypes *)
   2.426  
   2.427  fun constrset_of_consts thy cs =
   2.428    let
   2.429 @@ -328,6 +559,22 @@
   2.430      val cs''' = map (inst vs) cs'';
   2.431    in (tyco, (vs, rev cs''')) end;
   2.432  
   2.433 +fun get_datatype thy tyco =
   2.434 +  case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco)
   2.435 +   of (_, spec) :: _ => spec
   2.436 +    | [] => Sign.arity_number thy tyco
   2.437 +        |> Name.invents Name.context Name.aT
   2.438 +        |> map (rpair [])
   2.439 +        |> rpair [];
   2.440 +
   2.441 +fun get_datatype_of_constr thy c =
   2.442 +  case (snd o strip_type o Sign.the_const_type thy) c
   2.443 +   of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c
   2.444 +       then SOME tyco else NONE
   2.445 +    | _ => NONE;
   2.446 +
   2.447 +fun is_constr thy = is_some o get_datatype_of_constr thy;
   2.448 +
   2.449  
   2.450  (* code equations *)
   2.451  
   2.452 @@ -342,7 +589,7 @@
   2.453    in not (has_duplicates (op =) ((fold o fold_aterms)
   2.454      (fn Var (v, _) => cons v | _ => I) args [])) end;
   2.455  
   2.456 -fun gen_assert_eqn thy is_constr_head is_constr_pat (thm, proper) =
   2.457 +fun gen_assert_eqn thy is_constr_pat (thm, proper) =
   2.458    let
   2.459      val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
   2.460        handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
   2.461 @@ -394,7 +641,7 @@
   2.462        then ()
   2.463        else bad_thm ("Polymorphic constant as head in equation\n"
   2.464          ^ Display.string_of_thm thm)
   2.465 -    val _ = if not (is_constr_head c)
   2.466 +    val _ = if not (is_constr thy c)
   2.467        then ()
   2.468        else bad_thm ("Constructor as head in equation\n"
   2.469          ^ Display.string_of_thm thm)
   2.470 @@ -407,22 +654,21 @@
   2.471             ^ string_of_typ thy ty_decl)
   2.472    in (thm, proper) end;
   2.473  
   2.474 -fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr);
   2.475 +fun assert_eqn thy = error_thm (gen_assert_eqn thy (is_constr thy));
   2.476 +
   2.477 +fun meta_rewrite thy = LocalDefs.meta_rewrite_rule (ProofContext.init thy);
   2.478  
   2.479 +fun mk_eqn thy = error_thm (gen_assert_eqn thy (K true)) o
   2.480 +  apfst (meta_rewrite thy);
   2.481 +
   2.482 +fun mk_eqn_warning thy = Option.map (fn (thm, _) => (thm, is_linear thm))
   2.483 +  o warning_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy;
   2.484 +
   2.485 +fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm))
   2.486 +  o try_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy;
   2.487  
   2.488  (*those following are permissive wrt. to overloaded constants!*)
   2.489  
   2.490 -fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o
   2.491 -  apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy));
   2.492 -
   2.493 -fun mk_eqn_warning thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm))
   2.494 -  o warning_thm (gen_assert_eqn thy is_constr_head (K true))
   2.495 -  o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
   2.496 -
   2.497 -fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm))
   2.498 -  o try_thm (gen_assert_eqn thy is_constr_head (K true))
   2.499 -  o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
   2.500 -
   2.501  fun const_typ_eqn thy thm =
   2.502    let
   2.503      val (c, ty) = (dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   2.504 @@ -432,8 +678,46 @@
   2.505  fun typscheme_eqn thy = typscheme thy o const_typ_eqn thy;
   2.506  fun const_eqn thy = fst o const_typ_eqn thy;
   2.507  
   2.508 +fun assert_eqns_const thy c eqns =
   2.509 +  let
   2.510 +    fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
   2.511 +      then eqn else error ("Wrong head of code equation,\nexpected constant "
   2.512 +        ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
   2.513 +  in map (cert o assert_eqn thy) eqns end;
   2.514  
   2.515 -(* case cerificates *)
   2.516 +fun common_typ_eqns thy [] = []
   2.517 +  | common_typ_eqns thy [thm] = [thm]
   2.518 +  | common_typ_eqns thy (thms as thm :: _) = (*FIXME is too general*)
   2.519 +      let
   2.520 +        fun incr_thm thm max =
   2.521 +          let
   2.522 +            val thm' = incr_indexes max thm;
   2.523 +            val max' = Thm.maxidx_of thm' + 1;
   2.524 +          in (thm', max') end;
   2.525 +        val (thms', maxidx) = fold_map incr_thm thms 0;
   2.526 +        val ty1 :: tys = map (snd o const_typ_eqn thy) thms';
   2.527 +        fun unify ty env = Sign.typ_unify thy (ty1, ty) env
   2.528 +          handle Type.TUNIFY =>
   2.529 +            error ("Type unificaton failed, while unifying code equations\n"
   2.530 +            ^ (cat_lines o map Display.string_of_thm) thms
   2.531 +            ^ "\nwith types\n"
   2.532 +            ^ (cat_lines o map (string_of_typ thy)) (ty1 :: tys));
   2.533 +        val (env, _) = fold unify tys (Vartab.empty, maxidx)
   2.534 +        val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
   2.535 +          cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
   2.536 +      in map (Thm.instantiate (instT, [])) thms' end;
   2.537 +
   2.538 +fun these_eqns thy c =
   2.539 +  get_eqns thy c
   2.540 +  |> (map o apfst) (Thm.transfer thy)
   2.541 +  |> burrow_fst (common_typ_eqns thy);
   2.542 +
   2.543 +fun all_eqns thy =
   2.544 +  Symtab.dest ((the_eqns o the_exec) thy)
   2.545 +  |> maps (Lazy.force o snd o snd o fst o snd);
   2.546 +
   2.547 +
   2.548 +(* cases *)
   2.549  
   2.550  fun case_certificate thm =
   2.551    let
   2.552 @@ -475,255 +759,12 @@
   2.553    handle Bind => error "bad case certificate"
   2.554         | TERM _ => error "bad case certificate";
   2.555  
   2.556 -
   2.557 -(** code attributes **)
   2.558 -
   2.559 -structure CodeAttr = TheoryDataFun (
   2.560 -  type T = (string * attribute parser) list;
   2.561 -  val empty = [];
   2.562 -  val copy = I;
   2.563 -  val extend = I;
   2.564 -  fun merge _ = AList.merge (op = : string * string -> bool) (K true);
   2.565 -);
   2.566 -
   2.567 -fun add_attribute (attr as (name, _)) =
   2.568 -  let
   2.569 -    fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
   2.570 -      | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
   2.571 -  in CodeAttr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name
   2.572 -    then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
   2.573 -  end;
   2.574 -
   2.575 -val _ = Context.>> (Context.map_theory
   2.576 -  (Attrib.setup (Binding.name "code")
   2.577 -    (Scan.peek (fn context =>
   2.578 -      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))))
   2.579 -    "declare theorems for code generation"));
   2.580 -
   2.581 -
   2.582 -
   2.583 -(** logical and syntactical specification of executable code **)
   2.584 -
   2.585 -(* code equations *)
   2.586 -
   2.587 -type eqns = bool * (thm * bool) list lazy;
   2.588 -  (*default flag, theorems with proper flag (perhaps lazy)*)
   2.589 -
   2.590 -fun pretty_lthms ctxt r = case Lazy.peek r
   2.591 - of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
   2.592 -  | NONE => [Pretty.str "[...]"];
   2.593 -
   2.594 -fun certificate thy f r =
   2.595 -  case Lazy.peek r
   2.596 -   of SOME thms => (Lazy.value o f thy) (Exn.release thms)
   2.597 -    | NONE => let
   2.598 -        val thy_ref = Theory.check_thy thy;
   2.599 -      in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end;
   2.600 +fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
   2.601  
   2.602 -fun add_drop_redundant thy (thm, proper) thms =
   2.603 -  let
   2.604 -    val args_of = snd o strip_comb o map_types Type.strip_sorts
   2.605 -      o fst o Logic.dest_equals o Thm.plain_prop_of;
   2.606 -    val args = args_of thm;
   2.607 -    val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
   2.608 -    fun matches_args args' = length args <= length args' andalso
   2.609 -      Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
   2.610 -    fun drop (thm', proper') = if (proper orelse not proper')
   2.611 -      andalso matches_args (args_of thm') then 
   2.612 -        (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true)
   2.613 -      else false;
   2.614 -  in (thm, proper) :: filter_out drop thms end;
   2.615 -
   2.616 -fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms)
   2.617 -  | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms)
   2.618 -  | add_thm thy false thm (true, thms) = (false, Lazy.value [thm]);
   2.619 -
   2.620 -fun add_lthms lthms _ = (false, lthms);
   2.621 -
   2.622 -fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
   2.623 -
   2.624 -
   2.625 -(* specification data *)
   2.626 -
   2.627 -datatype spec = Spec of {
   2.628 -  concluded_history: bool,
   2.629 -  eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table
   2.630 -    (*with explicit history*),
   2.631 -  dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table
   2.632 -    (*with explicit history*),
   2.633 -  cases: (int * (int * string list)) Symtab.table * unit Symtab.table
   2.634 -};
   2.635 -
   2.636 -fun make_spec ((concluded_history, eqns), (dtyps, cases)) =
   2.637 -  Spec { concluded_history = concluded_history, eqns = eqns, dtyps = dtyps, cases = cases };
   2.638 -fun map_spec f (Spec { concluded_history = concluded_history, eqns = eqns,
   2.639 -  dtyps = dtyps, cases = cases }) =
   2.640 -  make_spec (f ((concluded_history, eqns), (dtyps, cases)));
   2.641 -fun merge_spec (Spec { concluded_history = _, eqns = eqns1, dtyps = dtyps1, cases = (cases1, undefs1) },
   2.642 -  Spec { concluded_history = _, eqns = eqns2, dtyps = dtyps2, cases = (cases2, undefs2) }) =
   2.643 -  let
   2.644 -    fun merge_eqns ((_, history1), (_, history2)) =
   2.645 -      let
   2.646 -        val raw_history = AList.merge (op = : serial * serial -> bool)
   2.647 -          (K true) (history1, history2)
   2.648 -        val filtered_history = filter_out (fst o snd) raw_history
   2.649 -        val history = if null filtered_history
   2.650 -          then raw_history else filtered_history;
   2.651 -      in ((false, (snd o hd) history), history) end;
   2.652 -    val eqns = Symtab.join (K merge_eqns) (eqns1, eqns2);
   2.653 -    val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2);
   2.654 -    val cases = (Symtab.merge (K true) (cases1, cases2),
   2.655 -      Symtab.merge (K true) (undefs1, undefs2));
   2.656 -  in make_spec ((false, eqns), (dtyps, cases)) end;
   2.657 -
   2.658 -
   2.659 -(* code setup data *)
   2.660 -
   2.661 -fun the_spec (Spec x) = x;
   2.662 -fun the_eqns (Spec { eqns, ... }) = eqns;
   2.663 -fun the_dtyps (Spec { dtyps, ... }) = dtyps;
   2.664 -fun the_cases (Spec { cases, ... }) = cases;
   2.665 -fun history_concluded (Spec { concluded_history, ... }) = concluded_history;
   2.666 -val map_concluded_history = map_spec o apfst o apfst;
   2.667 -val map_eqns = map_spec o apfst o apsnd;
   2.668 -val map_dtyps = map_spec o apsnd o apfst;
   2.669 -val map_cases = map_spec o apsnd o apsnd;
   2.670 +val undefineds = Symtab.keys o snd o the_cases o the_exec;
   2.671  
   2.672  
   2.673 -(* data slots dependent on executable content *)
   2.674 -
   2.675 -(*private copy avoids potential conflict of table exceptions*)
   2.676 -structure Datatab = TableFun(type key = int val ord = int_ord);
   2.677 -
   2.678 -local
   2.679 -
   2.680 -type kind = {
   2.681 -  empty: Object.T,
   2.682 -  purge: theory -> string list -> Object.T -> Object.T
   2.683 -};
   2.684 -
   2.685 -val kinds = ref (Datatab.empty: kind Datatab.table);
   2.686 -val kind_keys = ref ([]: serial list);
   2.687 -
   2.688 -fun invoke f k = case Datatab.lookup (! kinds) k
   2.689 - of SOME kind => f kind
   2.690 -  | NONE => sys_error "Invalid code data identifier";
   2.691 -
   2.692 -in
   2.693 -
   2.694 -fun declare_data empty purge =
   2.695 -  let
   2.696 -    val k = serial ();
   2.697 -    val kind = {empty = empty, purge = purge};
   2.698 -    val _ = change kinds (Datatab.update (k, kind));
   2.699 -    val _ = change kind_keys (cons k);
   2.700 -  in k end;
   2.701 -
   2.702 -fun invoke_init k = invoke (fn kind => #empty kind) k;
   2.703 -
   2.704 -fun invoke_purge_all thy cs =
   2.705 -  fold (fn k => Datatab.map_entry k
   2.706 -    (invoke (fn kind => #purge kind thy cs) k)) (! kind_keys);
   2.707 -
   2.708 -end; (*local*)
   2.709 -
   2.710 -
   2.711 -(** theory store **)
   2.712 -
   2.713 -local
   2.714 -
   2.715 -type data = Object.T Datatab.table;
   2.716 -val empty_data = Datatab.empty : data;
   2.717 -
   2.718 -structure Code_Data = TheoryDataFun
   2.719 -(
   2.720 -  type T = spec * data ref;
   2.721 -  val empty = (make_spec ((false, Symtab.empty),
   2.722 -    (Symtab.empty, (Symtab.empty, Symtab.empty))), ref empty_data);
   2.723 -  fun copy (spec, data) = (spec, ref (! data));
   2.724 -  val extend = copy;
   2.725 -  fun merge pp ((spec1, data1), (spec2, data2)) =
   2.726 -    (merge_spec (spec1, spec2), ref empty_data);
   2.727 -);
   2.728 -
   2.729 -fun thy_data f thy = f ((snd o Code_Data.get) thy);
   2.730 -
   2.731 -fun get_ensure_init kind data_ref =
   2.732 -  case Datatab.lookup (! data_ref) kind
   2.733 -   of SOME x => x
   2.734 -    | NONE => let val y = invoke_init kind
   2.735 -        in (change data_ref (Datatab.update (kind, y)); y) end;
   2.736 -
   2.737 -in
   2.738 -
   2.739 -(* access to executable content *)
   2.740 -
   2.741 -val the_exec = fst o Code_Data.get;
   2.742 -
   2.743 -fun complete_class_params thy cs =
   2.744 -  fold (fn c => case AxClass.inst_of_param thy c
   2.745 -   of NONE => insert (op =) c
   2.746 -    | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
   2.747 -
   2.748 -fun map_exec_purge touched f thy =
   2.749 -  Code_Data.map (fn (exec, data) => (f exec, ref (case touched
   2.750 -   of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
   2.751 -    | NONE => empty_data))) thy;
   2.752 -
   2.753 -val purge_data = (Code_Data.map o apsnd) (K (ref empty_data));
   2.754 -
   2.755 -
   2.756 -(* tackling equation history *)
   2.757 -
   2.758 -fun get_eqns thy c =
   2.759 -  Symtab.lookup ((the_eqns o the_exec) thy) c
   2.760 -  |> Option.map (Lazy.force o snd o snd o fst)
   2.761 -  |> these;
   2.762 -
   2.763 -fun continue_history thy = if (history_concluded o the_exec) thy
   2.764 -  then thy
   2.765 -    |> (Code_Data.map o apfst o map_concluded_history) (K false)
   2.766 -    |> SOME
   2.767 -  else NONE;
   2.768 -
   2.769 -fun conclude_history thy = if (history_concluded o the_exec) thy
   2.770 -  then NONE
   2.771 -  else thy
   2.772 -    |> (Code_Data.map o apfst)
   2.773 -        ((map_eqns o Symtab.map) (fn ((changed, current), history) =>
   2.774 -          ((false, current),
   2.775 -            if changed then (serial (), current) :: history else history))
   2.776 -        #> map_concluded_history (K true))
   2.777 -    |> SOME;
   2.778 -
   2.779 -val _ = Context.>> (Context.map_theory (Code_Data.init
   2.780 -  #> Theory.at_begin continue_history
   2.781 -  #> Theory.at_end conclude_history));
   2.782 -
   2.783 -
   2.784 -(* access to data dependent on abstract executable content *)
   2.785 -
   2.786 -fun get_data (kind, _, dest) = thy_data (get_ensure_init kind #> dest);
   2.787 -
   2.788 -fun change_data (kind, mk, dest) =
   2.789 -  let
   2.790 -    fun chnge data_ref f =
   2.791 -      let
   2.792 -        val data = get_ensure_init kind data_ref;
   2.793 -        val data' = f (dest data);
   2.794 -      in (change data_ref (Datatab.update (kind, mk data')); data') end;
   2.795 -  in thy_data chnge end;
   2.796 -
   2.797 -fun change_yield_data (kind, mk, dest) =
   2.798 -  let
   2.799 -    fun chnge data_ref f =
   2.800 -      let
   2.801 -        val data = get_ensure_init kind data_ref;
   2.802 -        val (x, data') = f (dest data);
   2.803 -      in (x, (change data_ref (Datatab.update (kind, mk data')); data')) end;
   2.804 -  in thy_data chnge end;
   2.805 -
   2.806 -end; (*local*)
   2.807 +(* diagnostic *)
   2.808  
   2.809  fun print_codesetup thy =
   2.810    let
   2.811 @@ -772,102 +813,41 @@
   2.812    end;
   2.813  
   2.814  
   2.815 -(** theorem transformation and certification **)
   2.816 +(** declaring executable ingredients **)
   2.817 +
   2.818 +(* constant aliasses *)
   2.819  
   2.820 -fun common_typ_eqns thy [] = []
   2.821 -  | common_typ_eqns thy [thm] = [thm]
   2.822 -  | common_typ_eqns thy (thms as thm :: _) = (*FIXME is too general*)
   2.823 -      let
   2.824 -        fun incr_thm thm max =
   2.825 -          let
   2.826 -            val thm' = incr_indexes max thm;
   2.827 -            val max' = Thm.maxidx_of thm' + 1;
   2.828 -          in (thm', max') end;
   2.829 -        val (thms', maxidx) = fold_map incr_thm thms 0;
   2.830 -        val ty1 :: tys = map (snd o const_typ_eqn thy) thms';
   2.831 -        fun unify ty env = Sign.typ_unify thy (ty1, ty) env
   2.832 -          handle Type.TUNIFY =>
   2.833 -            error ("Type unificaton failed, while unifying code equations\n"
   2.834 -            ^ (cat_lines o map Display.string_of_thm) thms
   2.835 -            ^ "\nwith types\n"
   2.836 -            ^ (cat_lines o map (string_of_typ thy)) (ty1 :: tys));
   2.837 -        val (env, _) = fold unify tys (Vartab.empty, maxidx)
   2.838 -        val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
   2.839 -          cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
   2.840 -      in map (Thm.instantiate (instT, [])) thms' end;
   2.841 +fun add_const_alias thm thy =
   2.842 +  let
   2.843 +    val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm)
   2.844 +     of SOME ofclass_eq => ofclass_eq
   2.845 +      | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
   2.846 +    val (T, class) = case try Logic.dest_of_class ofclass
   2.847 +     of SOME T_class => T_class
   2.848 +      | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
   2.849 +    val tvar = case try Term.dest_TVar T
   2.850 +     of SOME tvar => tvar
   2.851 +      | _ => error ("Bad type: " ^ Display.string_of_thm thm);
   2.852 +    val _ = if Term.add_tvars eqn [] = [tvar] then ()
   2.853 +      else error ("Inconsistent type: " ^ Display.string_of_thm thm);
   2.854 +    val lhs_rhs = case try Logic.dest_equals eqn
   2.855 +     of SOME lhs_rhs => lhs_rhs
   2.856 +      | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
   2.857 +    val c_c' = case try (pairself (check_const thy)) lhs_rhs
   2.858 +     of SOME c_c' => c_c'
   2.859 +      | _ => error ("Not an equation with two constants: "
   2.860 +          ^ Syntax.string_of_term_global thy eqn);
   2.861 +    val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
   2.862 +      else error ("Inconsistent class: " ^ Display.string_of_thm thm);
   2.863 +  in thy |>
   2.864 +    (map_exec_purge NONE o map_aliasses) (fn (alias, classes) =>
   2.865 +      ((c_c', thm) :: alias, insert (op =) class classes))
   2.866 +  end;
   2.867  
   2.868  
   2.869 -(** interfaces and attributes **)
   2.870 -
   2.871 -fun get_datatype thy tyco =
   2.872 -  case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco)
   2.873 -   of (_, spec) :: _ => spec
   2.874 -    | [] => Sign.arity_number thy tyco
   2.875 -        |> Name.invents Name.context Name.aT
   2.876 -        |> map (rpair [])
   2.877 -        |> rpair [];
   2.878 -
   2.879 -fun get_datatype_of_constr thy c =
   2.880 -  case (snd o strip_type o Sign.the_const_type thy) c
   2.881 -   of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c
   2.882 -       then SOME tyco else NONE
   2.883 -    | _ => NONE;
   2.884 -
   2.885 -fun is_constr thy = is_some o get_datatype_of_constr thy;
   2.886 -
   2.887 -val assert_eqn = fn thy => assert_eqn thy (is_constr thy);
   2.888 -
   2.889 -fun assert_eqns_const thy c eqns =
   2.890 -  let
   2.891 -    fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
   2.892 -      then eqn else error ("Wrong head of code equation,\nexpected constant "
   2.893 -        ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
   2.894 -  in map (cert o assert_eqn thy) eqns end;
   2.895 -
   2.896 -fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
   2.897 -  o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
   2.898 -    o apfst) (fn (_, eqns) => (true, f eqns));
   2.899 -
   2.900 -fun gen_add_eqn default (eqn as (thm, _)) thy =
   2.901 -  let val c = const_eqn thy thm
   2.902 -  in change_eqns false c (add_thm thy default eqn) thy end;
   2.903 +(* datatypes *)
   2.904  
   2.905 -fun add_eqn thm thy =
   2.906 -  gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, true)) thy;
   2.907 -
   2.908 -fun add_warning_eqn thm thy =
   2.909 -  case mk_eqn_warning thy (is_constr thy) thm
   2.910 -   of SOME eqn => gen_add_eqn false eqn thy
   2.911 -    | NONE => thy;
   2.912 -
   2.913 -fun add_default_eqn thm thy =
   2.914 -  case mk_eqn_liberal thy (is_constr thy) thm
   2.915 -   of SOME eqn => gen_add_eqn true eqn thy
   2.916 -    | NONE => thy;
   2.917 -
   2.918 -fun add_nbe_eqn thm thy =
   2.919 -  gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, false)) thy;
   2.920 -
   2.921 -fun add_eqnl (c, lthms) thy =
   2.922 -  let
   2.923 -    val lthms' = certificate thy (fn thy => assert_eqns_const thy c) lthms;
   2.924 -  in change_eqns false c (add_lthms lthms') thy end;
   2.925 -
   2.926 -val add_default_eqn_attribute = Thm.declaration_attribute
   2.927 -  (fn thm => Context.mapping (add_default_eqn thm) I);
   2.928 -val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
   2.929 -
   2.930 -fun del_eqn thm thy = case mk_eqn_liberal thy (is_constr thy) thm
   2.931 - of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
   2.932 -  | NONE => thy;
   2.933 -
   2.934 -fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
   2.935 -
   2.936 -fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
   2.937 -
   2.938 -val undefineds = Symtab.keys o snd o the_cases o the_exec;
   2.939 -
   2.940 -structure TypeInterpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
   2.941 +structure Type_Interpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
   2.942  
   2.943  fun add_datatype raw_cs thy =
   2.944    let
   2.945 @@ -884,10 +864,10 @@
   2.946      |> map_exec_purge NONE
   2.947          ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
   2.948          #> (map_cases o apfst) drop_outdated_cases)
   2.949 -    |> TypeInterpretation.data (tyco, serial ())
   2.950 +    |> Type_Interpretation.data (tyco, serial ())
   2.951    end;
   2.952  
   2.953 -fun type_interpretation f =  TypeInterpretation.interpretation
   2.954 +fun type_interpretation f =  Type_Interpretation.interpretation
   2.955    (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
   2.956  
   2.957  fun add_datatype_cmd raw_cs thy =
   2.958 @@ -895,6 +875,59 @@
   2.959      val cs = map (read_bare_const thy) raw_cs;
   2.960    in add_datatype cs thy end;
   2.961  
   2.962 +
   2.963 +(* code equations *)
   2.964 +
   2.965 +fun gen_add_eqn default (eqn as (thm, _)) thy =
   2.966 +  let val c = const_eqn thy thm
   2.967 +  in change_eqns false c (add_thm thy default eqn) thy end;
   2.968 +
   2.969 +fun add_eqn thm thy =
   2.970 +  gen_add_eqn false (mk_eqn thy (thm, true)) thy;
   2.971 +
   2.972 +fun add_warning_eqn thm thy =
   2.973 +  case mk_eqn_warning thy thm
   2.974 +   of SOME eqn => gen_add_eqn false eqn thy
   2.975 +    | NONE => thy;
   2.976 +
   2.977 +fun add_default_eqn thm thy =
   2.978 +  case mk_eqn_liberal thy thm
   2.979 +   of SOME eqn => gen_add_eqn true eqn thy
   2.980 +    | NONE => thy;
   2.981 +
   2.982 +fun add_nbe_eqn thm thy =
   2.983 +  gen_add_eqn false (mk_eqn thy (thm, false)) thy;
   2.984 +
   2.985 +fun add_eqnl (c, lthms) thy =
   2.986 +  let
   2.987 +    val lthms' = certificate thy (fn thy => assert_eqns_const thy c) lthms;
   2.988 +  in change_eqns false c (add_lthms lthms') thy end;
   2.989 +
   2.990 +val add_default_eqn_attribute = Thm.declaration_attribute
   2.991 +  (fn thm => Context.mapping (add_default_eqn thm) I);
   2.992 +val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
   2.993 +
   2.994 +fun del_eqn thm thy = case mk_eqn_liberal thy thm
   2.995 + of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
   2.996 +  | NONE => thy;
   2.997 +
   2.998 +val _ = Context.>> (Context.map_theory
   2.999 +  (let
  2.1000 +    fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
  2.1001 +    fun add_simple_attribute (name, f) =
  2.1002 +      add_attribute (name, Scan.succeed (mk_attribute f));
  2.1003 +    fun add_del_attribute (name, (add, del)) =
  2.1004 +      add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
  2.1005 +        || Scan.succeed (mk_attribute add))
  2.1006 +  in
  2.1007 +    Type_Interpretation.init
  2.1008 +    #> add_del_attribute ("", (add_warning_eqn, del_eqn))
  2.1009 +    #> add_simple_attribute ("nbe", add_nbe_eqn)
  2.1010 +  end));
  2.1011 +
  2.1012 +
  2.1013 +(* cases *)
  2.1014 +
  2.1015  fun add_case thm thy =
  2.1016    let
  2.1017      val (c, (k, case_pats)) = case_cert thm;
  2.1018 @@ -907,35 +940,12 @@
  2.1019  fun add_undefined c thy =
  2.1020    (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy;
  2.1021  
  2.1022 -val _ = Context.>> (Context.map_theory
  2.1023 -  (let
  2.1024 -    fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
  2.1025 -    fun add_simple_attribute (name, f) =
  2.1026 -      add_attribute (name, Scan.succeed (mk_attribute f));
  2.1027 -    fun add_del_attribute (name, (add, del)) =
  2.1028 -      add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
  2.1029 -        || Scan.succeed (mk_attribute add))
  2.1030 -  in
  2.1031 -    TypeInterpretation.init
  2.1032 -    #> add_del_attribute ("", (add_warning_eqn, del_eqn))
  2.1033 -    #> add_simple_attribute ("nbe", add_nbe_eqn)
  2.1034 -  end));
  2.1035 -
  2.1036 -fun these_eqns thy c =
  2.1037 -  get_eqns thy c
  2.1038 -  |> (map o apfst) (Thm.transfer thy)
  2.1039 -  |> burrow_fst (common_typ_eqns thy);
  2.1040 -
  2.1041 -fun all_eqns thy =
  2.1042 -  Symtab.dest ((the_eqns o the_exec) thy)
  2.1043 -  |> maps (Lazy.force o snd o snd o fst o snd);
  2.1044 -
  2.1045  end; (*struct*)
  2.1046  
  2.1047  
  2.1048 -(** type-safe interfaces for data depedent on executable content **)
  2.1049 +(** type-safe interfaces for data depedent on executable code **)
  2.1050  
  2.1051 -functor CodeDataFun(Data: CODE_DATA_ARGS): CODE_DATA =
  2.1052 +functor Code_Data_Fun(Data: CODE_DATA_ARGS): CODE_DATA =
  2.1053  struct
  2.1054  
  2.1055  type T = Data.T;
     3.1 --- a/src/Tools/Code/code_preproc.ML	Wed Jul 08 06:43:30 2009 +0200
     3.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Jul 08 08:18:07 2009 +0200
     3.3 @@ -450,7 +450,7 @@
     3.4  
     3.5  (** store for preprocessed arities and code equations **)
     3.6  
     3.7 -structure Wellsorted = CodeDataFun
     3.8 +structure Wellsorted = Code_Data_Fun
     3.9  (
    3.10    type T = ((string * class) * sort list) list * code_graph;
    3.11    val empty = ([], Graph.empty);
     4.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jul 08 06:43:30 2009 +0200
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Jul 08 08:18:07 2009 +0200
     4.3 @@ -722,15 +722,15 @@
     4.4            ensure_inst thy algbr funcgr inst
     4.5            ##>> (fold_map o fold_map) mk_dict yss
     4.6            #>> (fn (inst, dss) => DictConst (inst, dss))
     4.7 -      | mk_dict (Local (classrels, (v, (k, sort)))) =
     4.8 +      | mk_dict (Local (classrels, (v, (n, sort)))) =
     4.9            fold_map (ensure_classrel thy algbr funcgr) classrels
    4.10 -          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
    4.11 +          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort))))
    4.12    in fold_map mk_dict typargs end;
    4.13  
    4.14  
    4.15  (* store *)
    4.16  
    4.17 -structure Program = CodeDataFun
    4.18 +structure Program = Code_Data_Fun
    4.19  (
    4.20    type T = naming * program;
    4.21    val empty = (empty_naming, Graph.empty);
     5.1 --- a/src/Tools/nbe.ML	Wed Jul 08 06:43:30 2009 +0200
     5.2 +++ b/src/Tools/nbe.ML	Wed Jul 08 08:18:07 2009 +0200
     5.3 @@ -408,7 +408,7 @@
     5.4  
     5.5  (* function store *)
     5.6  
     5.7 -structure Nbe_Functions = CodeDataFun
     5.8 +structure Nbe_Functions = Code_Data_Fun
     5.9  (
    5.10    type T = Code_Thingol.naming * ((Univ option * int) Graph.T * (int * string Inttab.table));
    5.11    val empty = (Code_Thingol.empty_naming, (Graph.empty, (0, Inttab.empty)));