src/Pure/Isar/code.ML
changeset 27609 b23c9ad0fe7d
parent 27582 367aff8d7ffd
child 27675 cb0021d56e11
     1.1 --- a/src/Pure/Isar/code.ML	Tue Jul 15 15:59:49 2008 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Jul 15 16:02:07 2008 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    val del_inline: thm -> theory -> theory
     1.5    val add_post: thm -> theory -> theory
     1.6    val del_post: thm -> theory -> theory
     1.7 -  val add_functrans: string * (theory -> thm list -> thm list) -> theory -> theory
     1.8 +  val add_functrans: string * (theory -> thm list -> thm list option) -> theory -> theory
     1.9    val del_functrans: string -> theory -> theory
    1.10    val add_datatype: (string * typ) list -> theory -> theory
    1.11    val add_datatype_cmd: string list -> theory -> theory
    1.12 @@ -54,8 +54,7 @@
    1.13  sig
    1.14    type T
    1.15    val empty: T
    1.16 -  val merge: Pretty.pp -> T * T -> T
    1.17 -  val purge: theory option -> string list option -> T -> T
    1.18 +  val purge: theory -> string list -> T -> T
    1.19  end;
    1.20  
    1.21  signature CODE_DATA =
    1.22 @@ -69,8 +68,8 @@
    1.23  signature PRIVATE_CODE =
    1.24  sig
    1.25    include CODE
    1.26 -  val declare_data: Object.T -> (Pretty.pp -> Object.T * Object.T -> Object.T)
    1.27 -    -> (theory option -> string list option -> Object.T -> Object.T) -> serial
    1.28 +  val declare_data: Object.T -> (theory -> string list -> Object.T -> Object.T)
    1.29 +    -> serial
    1.30    val get_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.31      -> theory -> 'a
    1.32    val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.33 @@ -171,10 +170,6 @@
    1.34  
    1.35  fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
    1.36  
    1.37 -
    1.38 -(* fundamental melting operations *)
    1.39 -(*FIXME delete*)
    1.40 -
    1.41  fun melt _ ([], []) = (false, [])
    1.42    | melt _ ([], ys) = (true, ys)
    1.43    | melt eq (xs, ys) = fold_rev
    1.44 @@ -200,17 +195,15 @@
    1.45          (subtract Thm.eq_thm_prop dels2 (Susp.force sels1), Susp.force sels2);
    1.46        val (_, dels) = melt_thms
    1.47          (subtract Thm.eq_thm_prop (Susp.force sels2) dels1, dels2);
    1.48 -    in (true, ((Susp.delay o K) sels, dels)) end
    1.49 +    in ((Susp.delay o K) sels, dels) end
    1.50      else let
    1.51 -      val (sels_t, sels) = melt_lthms (sels1, sels2);
    1.52 -    in (sels_t, (sels, dels)) end
    1.53 +      val (_, sels) = melt_lthms (sels1, sels2);
    1.54 +    in (sels, dels) end
    1.55    end;
    1.56  
    1.57  
    1.58  (* specification data *)
    1.59  
    1.60 -val merge_funcs = Symtab.join (fn _ => fn ((_, a), (_, b)) => melt_sdthms (a, b));
    1.61 -
    1.62  val eq_string = op = : string * string -> bool;
    1.63  fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
    1.64    gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
    1.65 @@ -220,11 +213,8 @@
    1.66      fun join _ (cos as (_, cos2)) = if eq_dtyp cos then raise Symtab.SAME else cos2;
    1.67    in Symtab.join join tabs end;
    1.68  
    1.69 -fun merge_cases ((cases1, undefs1), (cases2, undefs2)) =
    1.70 -  (Symtab.merge (K true) (cases1, cases2), Symtab.merge (K true) (undefs1, undefs2));
    1.71 -
    1.72  datatype spec = Spec of {
    1.73 -  funcs: (bool * sdthms) Symtab.table,
    1.74 +  funcs: sdthms Symtab.table,
    1.75    dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
    1.76    cases: (int * string list) Symtab.table * unit Symtab.table
    1.77  };
    1.78 @@ -233,12 +223,13 @@
    1.79    Spec { funcs = funcs, dtyps = dtyps, cases = cases };
    1.80  fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) =
    1.81    mk_spec (f (funcs, (dtyps, cases)));
    1.82 -fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
    1.83 -  Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) =
    1.84 +fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = (cases1, undefs1) },
    1.85 +  Spec { funcs = funcs2, dtyps = dtyps2, cases = (cases2, undefs2) }) =
    1.86    let
    1.87 -    val funcs = merge_funcs (funcs1, funcs2);
    1.88 +    val funcs = Symtab.join (K melt_sdthms) (funcs1, funcs2);
    1.89      val dtyps = merge_dtyps (dtyps1, dtyps2);
    1.90 -    val cases = merge_cases (cases1, cases2);
    1.91 +    val cases = (Symtab.merge (K true) (cases1, cases2),
    1.92 +      Symtab.merge (K true) (undefs1, undefs2));
    1.93    in mk_spec (funcs, (dtyps, cases)) end;
    1.94  
    1.95  
    1.96 @@ -247,7 +238,7 @@
    1.97  datatype thmproc = Thmproc of {
    1.98    pre: MetaSimplifier.simpset,
    1.99    post: MetaSimplifier.simpset,
   1.100 -  functrans: (string * (serial * (theory -> thm list -> thm list))) list
   1.101 +  functrans: (string * (serial * (theory -> thm list -> thm list option))) list
   1.102  };
   1.103  
   1.104  fun mk_thmproc ((pre, post), functrans) =
   1.105 @@ -300,8 +291,7 @@
   1.106  
   1.107  type kind = {
   1.108    empty: Object.T,
   1.109 -  merge: Pretty.pp -> Object.T * Object.T -> Object.T,
   1.110 -  purge: theory option -> string list option -> Object.T -> Object.T
   1.111 +  purge: theory -> string list -> Object.T -> Object.T
   1.112  };
   1.113  
   1.114  val kinds = ref (Datatab.empty: kind Datatab.table);
   1.115 @@ -313,22 +303,19 @@
   1.116  
   1.117  in
   1.118  
   1.119 -fun declare_data empty merge purge =
   1.120 +fun declare_data empty purge =
   1.121    let
   1.122      val k = serial ();
   1.123 -    val kind = {empty = empty, merge = merge, purge = purge};
   1.124 +    val kind = {empty = empty, purge = purge};
   1.125      val _ = change kinds (Datatab.update (k, kind));
   1.126      val _ = change kind_keys (cons k);
   1.127    in k end;
   1.128  
   1.129 -fun invoke_empty k = invoke (fn kind => #empty kind) k;
   1.130 +fun invoke_init k = invoke (fn kind => #empty kind) k;
   1.131  
   1.132 -fun invoke_merge_all pp = Datatab.join
   1.133 -  (invoke (fn kind => #merge kind pp));
   1.134 -
   1.135 -fun invoke_purge_all thy_opt cs =
   1.136 +fun invoke_purge_all thy cs =
   1.137    fold (fn k => Datatab.map_entry k
   1.138 -    (invoke (fn kind => #purge kind thy_opt cs) k)) (! kind_keys);
   1.139 +    (invoke (fn kind => #purge kind thy cs) k)) (! kind_keys);
   1.140  
   1.141  end; (*local*)
   1.142  
   1.143 @@ -338,20 +325,16 @@
   1.144  local
   1.145  
   1.146  type data = Object.T Datatab.table;
   1.147 +val empty_data = Datatab.empty : data;
   1.148  
   1.149  structure CodeData = TheoryDataFun
   1.150  (
   1.151    type T = exec * data ref;
   1.152 -  val empty = (empty_exec, ref Datatab.empty : data ref);
   1.153 +  val empty = (empty_exec, ref empty_data);
   1.154    fun copy (exec, data) = (exec, ref (! data));
   1.155    val extend = copy;
   1.156    fun merge pp ((exec1, data1), (exec2, data2)) =
   1.157 -    let
   1.158 -      val exec = merge_exec (exec1, exec2);
   1.159 -      val data1' = invoke_purge_all NONE NONE (! data1);
   1.160 -      val data2' = invoke_purge_all NONE NONE (! data2);
   1.161 -      val data = invoke_merge_all pp (data1', data2');
   1.162 -    in (exec, ref data) end;
   1.163 +    (merge_exec (exec1, exec2), ref empty_data);
   1.164  );
   1.165  
   1.166  val _ = Context.>> (Context.map_theory CodeData.init);
   1.167 @@ -361,7 +344,7 @@
   1.168  fun get_ensure_init kind data_ref =
   1.169    case Datatab.lookup (! data_ref) kind
   1.170     of SOME x => x
   1.171 -    | NONE => let val y = invoke_empty kind
   1.172 +    | NONE => let val y = invoke_init kind
   1.173          in (change data_ref (Datatab.update (kind, y)); y) end;
   1.174  
   1.175  in
   1.176 @@ -371,8 +354,9 @@
   1.177  val the_exec = fst o CodeData.get;
   1.178  
   1.179  fun map_exec_purge touched f thy =
   1.180 -  CodeData.map (fn (exec, data) => 
   1.181 -    (f exec, ref (invoke_purge_all (SOME thy) touched (! data)))) thy;
   1.182 +  CodeData.map (fn (exec, data) => (f exec, ref (case touched
   1.183 +   of SOME cs => invoke_purge_all thy cs (! data)
   1.184 +    | NONE => empty_data))) thy;
   1.185  
   1.186  
   1.187  (* access to data dependent on abstract executable content *)
   1.188 @@ -426,9 +410,8 @@
   1.189      val pre = (#pre o the_thmproc) exec;
   1.190      val post = (#post o the_thmproc) exec;
   1.191      val functrans = (map fst o #functrans o the_thmproc) exec;
   1.192 -    val funs = the_funcs exec
   1.193 +    val funcs = the_funcs exec
   1.194        |> Symtab.dest
   1.195 -      |> (map o apsnd) snd
   1.196        |> (map o apfst) (CodeUnit.string_of_const thy)
   1.197        |> sort (string_ord o pairself fst);
   1.198      val dtyps = the_dtyps exec
   1.199 @@ -441,7 +424,7 @@
   1.200        Pretty.block (
   1.201          Pretty.str "defining equations:"
   1.202          :: Pretty.fbrk
   1.203 -        :: (Pretty.fbreaks o map pretty_func) funs
   1.204 +        :: (Pretty.fbreaks o map pretty_func) funcs
   1.205        ),
   1.206        Pretty.block [
   1.207          Pretty.str "preprocessing simpset:",
   1.208 @@ -454,7 +437,7 @@
   1.209          MetaSimplifier.pretty_ss post
   1.210        ],
   1.211        Pretty.block (
   1.212 -        Pretty.str "function transformators:"
   1.213 +        Pretty.str "function transformers:"
   1.214          :: Pretty.fbrk
   1.215          :: (Pretty.fbreaks o map Pretty.str) functrans
   1.216        ),
   1.217 @@ -527,7 +510,7 @@
   1.218      val funcs = classparams
   1.219        |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
   1.220        |> map (Symtab.lookup ((the_funcs o the_exec) thy))
   1.221 -      |> (map o Option.map) (Susp.force o fst o snd)
   1.222 +      |> (map o Option.map) (Susp.force o fst)
   1.223        |> maps these
   1.224        |> map (Thm.transfer thy)
   1.225      fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys
   1.226 @@ -704,7 +687,7 @@
   1.227        else ();
   1.228    in
   1.229      (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
   1.230 -      (c, (false, (Susp.value [], []))) (apsnd (add_thm func))) thy
   1.231 +      (c, (Susp.value [], [])) (add_thm func)) thy
   1.232    end;
   1.233  
   1.234  fun add_liberal_func thm thy =
   1.235 @@ -716,7 +699,7 @@
   1.236            then thy
   1.237            else map_exec_purge (SOME [c]) (map_funcs
   1.238              (Symtab.map_default
   1.239 -              (c, (false, (Susp.value [], []))) (apsnd (add_thm func)))) thy
   1.240 +              (c, (Susp.value [], [])) (add_thm func))) thy
   1.241          end
   1.242      | NONE => thy;
   1.243  
   1.244 @@ -729,7 +712,7 @@
   1.245            then thy
   1.246            else map_exec_purge (SOME [c]) (map_funcs
   1.247            (Symtab.map_default
   1.248 -            (c, (false, (Susp.value [], []))) (apsnd (add_thm func)))) thy
   1.249 +            (c, (Susp.value [], [])) (add_thm func))) thy
   1.250          end
   1.251      | NONE => thy;
   1.252  
   1.253 @@ -738,12 +721,12 @@
   1.254     of SOME func => let
   1.255            val c = const_of_func thy func;
   1.256          in map_exec_purge (SOME [c]) (map_funcs
   1.257 -          (Symtab.map_entry c (apsnd (del_thm func)))) thy
   1.258 +          (Symtab.map_entry c (del_thm func))) thy
   1.259          end
   1.260      | NONE => thy;
   1.261  
   1.262  fun del_funcs const = map_exec_purge (SOME [const])
   1.263 -  (map_funcs (Symtab.map_entry const (apsnd del_thms)));
   1.264 +  (map_funcs (Symtab.map_entry const del_thms));
   1.265  
   1.266  fun add_funcl (const, lthms) thy =
   1.267    let
   1.268 @@ -752,8 +735,8 @@
   1.269          alas, naive checking results in non-termination!*)
   1.270    in
   1.271      map_exec_purge (SOME [const])
   1.272 -      (map_funcs (Symtab.map_default (const, (false, (Susp.value [], [])))
   1.273 -      (apsnd (add_lthms lthms')))) thy
   1.274 +      (map_funcs (Symtab.map_default (const, (Susp.value [], []))
   1.275 +      (add_lthms lthms'))) thy
   1.276    end;
   1.277  
   1.278  val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute
   1.279 @@ -819,7 +802,7 @@
   1.280  
   1.281  fun del_functrans name =
   1.282    (map_exec_purge NONE o map_thmproc o apsnd)
   1.283 -    (delete_force "function transformator" name);
   1.284 +    (delete_force "function transformer" name);
   1.285  
   1.286  val _ = Context.>> (Context.map_theory
   1.287    (let
   1.288 @@ -841,11 +824,13 @@
   1.289  
   1.290  local
   1.291  
   1.292 -fun apply_functrans thy f [] = []
   1.293 -  | apply_functrans thy f (thms as (thm :: _)) =
   1.294 +fun apply_functrans thy [] = []
   1.295 +  | apply_functrans thy (thms as thm :: _) =
   1.296        let
   1.297          val const = const_of_func thy thm;
   1.298 -        val thms' = f thy thms;
   1.299 +        val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
   1.300 +          o the_thmproc o the_exec) thy;
   1.301 +        val thms' = perhaps (perhaps_loop (perhaps_apply functrans)) thms;
   1.302        in certify_const thy const thms' end;
   1.303  
   1.304  fun rhs_conv conv thm =
   1.305 @@ -867,7 +852,7 @@
   1.306      val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy;
   1.307    in
   1.308      thms
   1.309 -    |> fold (fn (_, (_, f)) => apply_functrans thy f) ((#functrans o the_thmproc o the_exec) thy)
   1.310 +    |> apply_functrans thy
   1.311      |> map (CodeUnit.rewrite_func pre)
   1.312      (*FIXME - must check gere: rewrite rule, defining equation, proper constant *)
   1.313      |> map (AxClass.unoverload thy)
   1.314 @@ -913,7 +898,7 @@
   1.315  
   1.316  fun get_funcs thy const =
   1.317    Symtab.lookup ((the_funcs o the_exec) thy) const
   1.318 -  |> Option.map (Susp.force o fst o snd)
   1.319 +  |> Option.map (Susp.force o fst)
   1.320    |> these
   1.321    |> map (Thm.transfer thy);
   1.322  
   1.323 @@ -950,8 +935,7 @@
   1.324  fun dest (Data x) = x
   1.325  
   1.326  val kind = Code.declare_data (Data Data.empty)
   1.327 -  (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)))
   1.328 -  (fn thy_opt => fn cs => fn Data x => Data (Data.purge thy_opt cs x));
   1.329 +  (fn thy => fn cs => fn Data x => Data (Data.purge thy cs x));
   1.330  
   1.331  val data_op = (kind, Data, dest);
   1.332