src/Pure/Isar/code.ML
changeset 27557 151731493264
parent 26970 bc28e7bcb765
child 27582 367aff8d7ffd
     1.1 --- a/src/Pure/Isar/code.ML	Mon Jul 14 11:04:42 2008 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Jul 14 11:04:46 2008 +0200
     1.3 @@ -15,14 +15,14 @@
     1.4    val del_func: thm -> theory -> theory
     1.5    val del_funcs: string -> theory -> theory
     1.6    val add_funcl: string * thm list Susp.T -> theory -> theory
     1.7 +  val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
     1.8 +  val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
     1.9    val add_inline: thm -> theory -> theory
    1.10    val del_inline: thm -> theory -> theory
    1.11 -  val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory
    1.12 -  val del_inline_proc: string -> theory -> theory
    1.13 -  val add_preproc: string * (theory -> thm list -> thm list) -> theory -> theory
    1.14 -  val del_preproc: string -> theory -> theory
    1.15    val add_post: thm -> theory -> theory
    1.16    val del_post: thm -> theory -> theory
    1.17 +  val add_functrans: string * (theory -> thm list -> thm list) -> theory -> theory
    1.18 +  val del_functrans: string -> theory -> theory
    1.19    val add_datatype: (string * typ) list -> theory -> theory
    1.20    val add_datatype_cmd: string list -> theory -> theory
    1.21    val type_interpretation:
    1.22 @@ -173,6 +173,7 @@
    1.23  
    1.24  
    1.25  (* fundamental melting operations *)
    1.26 +(*FIXME delete*)
    1.27  
    1.28  fun melt _ ([], []) = (false, [])
    1.29    | melt _ ([], ys) = (true, ys)
    1.30 @@ -258,42 +259,34 @@
    1.31    Spec { funcs = funcs, dtyps = dtyps, cases = cases };
    1.32  fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) =
    1.33    mk_spec (f (funcs, (dtyps, cases)));
    1.34 -fun melt_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
    1.35 +fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
    1.36    Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) =
    1.37    let
    1.38 -    val (touched_funcs, funcs) = melt_funcs (funcs1, funcs2);
    1.39 -    val (touched_dtyps, dtyps) = melt_dtyps (dtyps1, dtyps2);
    1.40 -    val (touched_cases, cases) = melt_cases (cases1, cases2);
    1.41 -    val touched = if touched_dtyps then NONE else
    1.42 -      SOME (fold (insert (op =)) touched_cases touched_funcs);
    1.43 -  in (touched, mk_spec (funcs, (dtyps, cases))) end;
    1.44 +    val (_, funcs) = melt_funcs (funcs1, funcs2);
    1.45 +    val (_, dtyps) = melt_dtyps (dtyps1, dtyps2);
    1.46 +    val (_, cases) = melt_cases (cases1, cases2);
    1.47 +  in mk_spec (funcs, (dtyps, cases)) end;
    1.48  
    1.49  
    1.50  (* pre- and postprocessor *)
    1.51  
    1.52  datatype thmproc = Thmproc of {
    1.53 -  inlines: thm list,
    1.54 -  inline_procs: (string * (serial * (theory -> cterm list -> thm list))) list,
    1.55 -  preprocs: (string * (serial * (theory -> thm list -> thm list))) list,
    1.56 -  posts: thm list
    1.57 +  pre: MetaSimplifier.simpset,
    1.58 +  post: MetaSimplifier.simpset,
    1.59 +  functrans: (string * (serial * (theory -> thm list -> thm list))) list
    1.60  };
    1.61  
    1.62 -fun mk_thmproc (((inlines, inline_procs), preprocs), posts) =
    1.63 -  Thmproc { inlines = inlines, inline_procs = inline_procs, preprocs = preprocs,
    1.64 -    posts = posts };
    1.65 -fun map_thmproc f (Thmproc { inlines, inline_procs, preprocs, posts }) =
    1.66 -  mk_thmproc (f (((inlines, inline_procs), preprocs), posts));
    1.67 -fun melt_thmproc (Thmproc { inlines = inlines1, inline_procs = inline_procs1,
    1.68 -    preprocs = preprocs1, posts = posts1 },
    1.69 -  Thmproc { inlines = inlines2, inline_procs = inline_procs2,
    1.70 -      preprocs = preprocs2, posts= posts2 }) =
    1.71 +fun mk_thmproc ((pre, post), functrans) =
    1.72 +  Thmproc { pre = pre, post = post, functrans = functrans };
    1.73 +fun map_thmproc f (Thmproc { pre, post, functrans }) =
    1.74 +  mk_thmproc (f ((pre, post), functrans));
    1.75 +fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 },
    1.76 +  Thmproc { pre = pre2, post = post2, functrans = functrans2 }) =
    1.77      let
    1.78 -      val (touched1, inlines) = melt_thms (inlines1, inlines2);
    1.79 -      val (touched2, inline_procs) = melt_alist (op =) (eq_fst (op =)) (inline_procs1, inline_procs2);
    1.80 -      val (touched3, preprocs) = melt_alist (op =) (eq_fst (op =)) (preprocs1, preprocs2);
    1.81 -      val (_, posts) = melt_thms (posts1, posts2);
    1.82 -    in (touched1 orelse touched2 orelse touched3,
    1.83 -      mk_thmproc (((inlines, inline_procs), preprocs), posts)) end;
    1.84 +      val pre = MetaSimplifier.merge_ss (pre1, pre2);
    1.85 +      val post = MetaSimplifier.merge_ss (post1, post2);
    1.86 +      val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
    1.87 +    in mk_thmproc ((pre, post), functrans) end;
    1.88  
    1.89  datatype exec = Exec of {
    1.90    thmproc: thmproc,
    1.91 @@ -304,14 +297,13 @@
    1.92    Exec { thmproc = thmproc, spec = spec };
    1.93  fun map_exec f (Exec { thmproc = thmproc, spec = spec }) =
    1.94    mk_exec (f (thmproc, spec));
    1.95 -fun melt_exec (Exec { thmproc = thmproc1, spec = spec1 },
    1.96 +fun merge_exec (Exec { thmproc = thmproc1, spec = spec1 },
    1.97    Exec { thmproc = thmproc2, spec = spec2 }) =
    1.98    let
    1.99 -    val (touched', thmproc) = melt_thmproc (thmproc1, thmproc2);
   1.100 -    val (touched_cs, spec) = melt_spec (spec1, spec2);
   1.101 -    val touched = if touched' then NONE else touched_cs;
   1.102 -  in (touched, mk_exec (thmproc, spec)) end;
   1.103 -val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
   1.104 +    val thmproc = merge_thmproc (thmproc1, thmproc2);
   1.105 +    val spec = merge_spec (spec1, spec2);
   1.106 +  in mk_exec (thmproc, spec) end;
   1.107 +val empty_exec = mk_exec (mk_thmproc ((MetaSimplifier.empty_ss, MetaSimplifier.empty_ss), []),
   1.108    mk_spec (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty))));
   1.109  
   1.110  fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x;
   1.111 @@ -381,9 +373,9 @@
   1.112    val extend = copy;
   1.113    fun merge pp ((exec1, data1), (exec2, data2)) =
   1.114      let
   1.115 -      val (touched, exec) = melt_exec (exec1, exec2);
   1.116 -      val data1' = invoke_purge_all NONE touched (! data1);
   1.117 -      val data2' = invoke_purge_all NONE touched (! data2);
   1.118 +      val exec = merge_exec (exec1, exec2);
   1.119 +      val data1' = invoke_purge_all NONE NONE (! data1);
   1.120 +      val data2' = invoke_purge_all NONE NONE (! data2);
   1.121        val data = invoke_merge_all pp (data1', data2');
   1.122      in (exec, ref data) end;
   1.123  );
   1.124 @@ -457,10 +449,9 @@
   1.125                            :: Pretty.str "of"
   1.126                            :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
   1.127            );
   1.128 -    val inlines = (#inlines o the_thmproc) exec;
   1.129 -    val posts = (#posts o the_thmproc) exec;
   1.130 -    val inline_procs = (map fst o #inline_procs o the_thmproc) exec;
   1.131 -    val preprocs = (map fst o #preprocs o the_thmproc) exec;
   1.132 +    val pre = (#pre o the_thmproc) exec;
   1.133 +    val post = (#post o the_thmproc) exec;
   1.134 +    val functrans = (map fst o #functrans o the_thmproc) exec;
   1.135      val funs = the_funcs exec
   1.136        |> Symtab.dest
   1.137        |> (map o apsnd) snd
   1.138 @@ -478,25 +469,20 @@
   1.139          :: Pretty.fbrk
   1.140          :: (Pretty.fbreaks o map pretty_func) funs
   1.141        ),
   1.142 +      Pretty.block [
   1.143 +        Pretty.str "preprocessing simpset:",
   1.144 +        Pretty.fbrk,
   1.145 +        MetaSimplifier.pretty_ss pre
   1.146 +      ],
   1.147 +      Pretty.block [
   1.148 +        Pretty.str "postprocessing simpset:",
   1.149 +        Pretty.fbrk,
   1.150 +        MetaSimplifier.pretty_ss post
   1.151 +      ],
   1.152        Pretty.block (
   1.153 -        Pretty.str "inlining theorems:"
   1.154 -        :: Pretty.fbrk
   1.155 -        :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
   1.156 -      ),
   1.157 -      Pretty.block (
   1.158 -        Pretty.str "inlining procedures:"
   1.159 +        Pretty.str "function transformators:"
   1.160          :: Pretty.fbrk
   1.161 -        :: (Pretty.fbreaks o map Pretty.str) inline_procs
   1.162 -      ),
   1.163 -      Pretty.block (
   1.164 -        Pretty.str "preprocessors:"
   1.165 -        :: Pretty.fbrk
   1.166 -        :: (Pretty.fbreaks o map Pretty.str) preprocs
   1.167 -      ),
   1.168 -      Pretty.block (
   1.169 -        Pretty.str "postprocessor theorems:"
   1.170 -        :: Pretty.fbrk
   1.171 -        :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) posts
   1.172 +        :: (Pretty.fbreaks o map Pretty.str) functrans
   1.173        ),
   1.174        Pretty.block (
   1.175          Pretty.str "datatypes:"
   1.176 @@ -834,41 +820,32 @@
   1.177  fun add_undefined c thy =
   1.178    (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy;
   1.179  
   1.180 -fun add_inline thm thy =
   1.181 -  (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
   1.182 -    (insert Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
   1.183 -        (*fully applied in order to get right context for mk_rew!*)
   1.184 +val map_pre = map_exec_purge NONE o map_thmproc o apfst o apfst;
   1.185 +val map_post = map_exec_purge NONE o map_thmproc o apfst o apsnd;
   1.186 +
   1.187 +fun add_inline thm thy = (map_pre o MetaSimplifier.add_simp)
   1.188 +  (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
   1.189 +    (*fully applied in order to get right context for mk_rew!*)
   1.190 +
   1.191 +fun del_inline thm thy = (map_pre o MetaSimplifier.del_simp)
   1.192 +  (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
   1.193 +    (*fully applied in order to get right context for mk_rew!*)
   1.194  
   1.195 -fun del_inline thm thy =
   1.196 -  (map_exec_purge NONE o map_thmproc o apfst o apfst o apfst)
   1.197 -    (remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
   1.198 -        (*fully applied in order to get right context for mk_rew!*)
   1.199 +fun add_post thm thy = (map_post o MetaSimplifier.add_simp)
   1.200 +  (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
   1.201 +    (*fully applied in order to get right context for mk_rew!*)
   1.202  
   1.203 -fun add_inline_proc (name, f) =
   1.204 -  (map_exec_purge NONE o map_thmproc o apfst o apfst o apsnd)
   1.205 +fun del_post thm thy = (map_post o MetaSimplifier.del_simp)
   1.206 +  (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
   1.207 +    (*fully applied in order to get right context for mk_rew!*)
   1.208 +  
   1.209 +fun add_functrans (name, f) =
   1.210 +  (map_exec_purge NONE o map_thmproc o apsnd)
   1.211      (AList.update (op =) (name, (serial (), f)));
   1.212  
   1.213 -fun del_inline_proc name =
   1.214 -  (map_exec_purge NONE o map_thmproc o apfst o apfst o apsnd)
   1.215 -    (delete_force "inline procedure" name);
   1.216 -
   1.217 -fun add_preproc (name, f) =
   1.218 -  (map_exec_purge NONE o map_thmproc o apfst o apsnd)
   1.219 -    (AList.update (op =) (name, (serial (), f)));
   1.220 -
   1.221 -fun del_preproc name =
   1.222 -  (map_exec_purge NONE o map_thmproc o apfst o apsnd)
   1.223 -    (delete_force "preprocessor" name);
   1.224 -
   1.225 -fun add_post thm thy =
   1.226 +fun del_functrans name =
   1.227    (map_exec_purge NONE o map_thmproc o apsnd)
   1.228 -    (insert Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
   1.229 -        (*fully applied in order to get right context for mk_rew!*)
   1.230 -
   1.231 -fun del_post thm thy =
   1.232 -  (map_exec_purge NONE o map_thmproc o apsnd)
   1.233 -    (remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
   1.234 -        (*fully applied in order to get right context for mk_rew!*)
   1.235 +    (delete_force "function transformator" name);
   1.236  
   1.237  val _ = Context.>> (Context.map_theory
   1.238    (let
   1.239 @@ -890,20 +867,8 @@
   1.240  
   1.241  local
   1.242  
   1.243 -fun gen_apply_inline_proc prep post thy f x =
   1.244 -  let
   1.245 -    val cts = prep x;
   1.246 -    val rews = map CodeUnit.assert_rew (f thy cts);
   1.247 -  in post rews x end;
   1.248 -
   1.249 -val apply_inline_proc = gen_apply_inline_proc (maps
   1.250 -  ((fn [args, rhs] => rhs :: (snd o Drule.strip_comb) args) o snd o Drule.strip_comb o Thm.cprop_of))
   1.251 -  (fn rews => map (CodeUnit.rewrite_func rews));
   1.252 -val apply_inline_proc_cterm = gen_apply_inline_proc single
   1.253 -  (MetaSimplifier.rewrite false);
   1.254 -
   1.255 -fun apply_preproc thy f [] = []
   1.256 -  | apply_preproc thy f (thms as (thm :: _)) =
   1.257 +fun apply_functrans thy f [] = []
   1.258 +  | apply_functrans thy f (thms as (thm :: _)) =
   1.259        let
   1.260          val const = const_of_func thy thm;
   1.261          val thms' = f thy thms;
   1.262 @@ -925,10 +890,9 @@
   1.263  
   1.264  fun preprocess thy thms =
   1.265    thms
   1.266 -  |> fold (fn (_, (_, f)) => apply_preproc thy f) ((#preprocs o the_thmproc o the_exec) thy)
   1.267 -  |> map (CodeUnit.rewrite_func ((#inlines o the_thmproc o the_exec) thy))
   1.268 -  |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o the_exec) thy)
   1.269 -(*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
   1.270 +  |> fold (fn (_, (_, f)) => apply_functrans thy f) ((#functrans o the_thmproc o the_exec) thy)
   1.271 +  |> map (CodeUnit.rewrite_func ((#pre o the_thmproc o the_exec) thy))
   1.272 +  (*FIXME - must check gere: rewrite rule, defining equation, proper constant *)
   1.273    |> map (AxClass.unoverload thy)
   1.274    |> common_typ_funcs;
   1.275  
   1.276 @@ -938,9 +902,7 @@
   1.277      val thy = Thm.theory_of_cterm ct;
   1.278    in
   1.279      ct
   1.280 -    |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o the_exec) thy)
   1.281 -    |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
   1.282 -        ((#inline_procs o the_thmproc o the_exec) thy)
   1.283 +    |> MetaSimplifier.rewrite' (ProofContext.init thy) false ((#pre o the_thmproc o the_exec) thy)
   1.284      |> rhs_conv (AxClass.unoverload_conv thy)
   1.285    end;
   1.286  
   1.287 @@ -952,7 +914,8 @@
   1.288    in
   1.289      ct
   1.290      |> AxClass.overload_conv thy
   1.291 -    |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o the_exec) thy))
   1.292 +    |> rhs_conv (MetaSimplifier.rewrite' (ProofContext.init thy) false 
   1.293 +          ((#post o the_thmproc o the_exec) thy))
   1.294    end;
   1.295  
   1.296  fun postprocess_term thy = term_of_conv thy postprocess_conv;