transferred code generator preprocessor into separate module
authorhaftmann
Tue May 12 19:30:33 2009 +0200 (2009-05-12)
changeset 3112580218ee73167
parent 31124 58bc773c60e2
child 31126 d8a6122affd7
transferred code generator preprocessor into separate module
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Tools/recfun_codegen.ML
src/Pure/Isar/code.ML
src/Pure/Isar/isar_syn.ML
src/Pure/codegen.ML
src/Tools/Code_Generator.thy
src/Tools/code/code_preproc.ML
src/Tools/code/code_thingol.ML
src/Tools/code/code_wellsorted.ML
     1.1 --- a/src/HOL/HOL.thy	Tue May 12 17:09:36 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue May 12 19:30:33 2009 +0200
     1.3 @@ -1870,8 +1870,8 @@
     1.4  subsubsection {* Generic code generator preprocessor *}
     1.5  
     1.6  setup {*
     1.7 -  Code.map_pre (K HOL_basic_ss)
     1.8 -  #> Code.map_post (K HOL_basic_ss)
     1.9 +  Code_Preproc.map_pre (K HOL_basic_ss)
    1.10 +  #> Code_Preproc.map_post (K HOL_basic_ss)
    1.11  *}
    1.12  
    1.13  subsubsection {* Generic code generator target languages *}
     2.1 --- a/src/HOL/IsaMakefile	Tue May 12 17:09:36 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue May 12 19:30:33 2009 +0200
     2.3 @@ -92,10 +92,10 @@
     2.4    $(SRC)/Tools/auto_solve.ML \
     2.5    $(SRC)/Tools/code/code_haskell.ML \
     2.6    $(SRC)/Tools/code/code_ml.ML \
     2.7 +  $(SRC)/Tools/code/code_preproc.ML \
     2.8    $(SRC)/Tools/code/code_printer.ML \
     2.9    $(SRC)/Tools/code/code_target.ML \
    2.10    $(SRC)/Tools/code/code_thingol.ML \
    2.11 -  $(SRC)/Tools/code/code_wellsorted.ML \
    2.12    $(SRC)/Tools/coherent.ML \
    2.13    $(SRC)/Tools/eqsubst.ML \
    2.14    $(SRC)/Tools/induct.ML \
     3.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue May 12 17:09:36 2009 +0200
     3.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue May 12 19:30:33 2009 +0200
     3.3 @@ -54,7 +54,7 @@
     3.4    let
     3.5      val c' = AxClass.unoverload_const thy (c, T);
     3.6      val opt_name = Symtab.lookup (ModuleData.get thy) c';
     3.7 -    val thms = Code.these_raw_eqns thy c'
     3.8 +    val thms = Code.these_eqns thy c'
     3.9        |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    3.10        |> expand_eta thy
    3.11        |> map_filter (meta_eq_to_obj_eq thy)
     4.1 --- a/src/Pure/Isar/code.ML	Tue May 12 17:09:36 2009 +0200
     4.2 +++ b/src/Pure/Isar/code.ML	Tue May 12 19:30:33 2009 +0200
     4.3 @@ -15,13 +15,6 @@
     4.4    val del_eqn: thm -> theory -> theory
     4.5    val del_eqns: string -> theory -> theory
     4.6    val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
     4.7 -  val map_pre: (simpset -> simpset) -> theory -> theory
     4.8 -  val map_post: (simpset -> simpset) -> theory -> theory
     4.9 -  val add_inline: thm -> theory -> theory
    4.10 -  val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
    4.11 -  val del_functrans: string -> theory -> theory
    4.12 -  val simple_functrans: (theory -> thm list -> thm list option)
    4.13 -    -> theory -> (thm * bool) list -> (thm * bool) list option
    4.14    val add_datatype: (string * typ) list -> theory -> theory
    4.15    val add_datatype_cmd: string list -> theory -> theory
    4.16    val type_interpretation:
    4.17 @@ -32,17 +25,14 @@
    4.18    val purge_data: theory -> theory
    4.19  
    4.20    val these_eqns: theory -> string -> (thm * bool) list
    4.21 -  val these_raw_eqns: theory -> string -> (thm * bool) list
    4.22    val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
    4.23    val get_datatype_of_constr: theory -> string -> string option
    4.24    val get_case_scheme: theory -> string -> (int * (int * string list)) option
    4.25    val is_undefined: theory -> string -> bool
    4.26    val default_typscheme: theory -> string -> (string * sort) list * typ
    4.27 -
    4.28 -  val preprocess_conv: theory -> cterm -> thm
    4.29 -  val preprocess_term: theory -> term -> term
    4.30 -  val postprocess_conv: theory -> cterm -> thm
    4.31 -  val postprocess_term: theory -> term -> term
    4.32 +  val assert_eqn: theory -> thm * bool -> thm * bool
    4.33 +  val assert_eqns_const: theory -> string
    4.34 +    -> (thm * bool) list -> (thm * bool) list
    4.35  
    4.36    val add_attribute: string * attribute parser -> theory -> theory
    4.37  
    4.38 @@ -159,6 +149,8 @@
    4.39  
    4.40  fun mk_spec ((concluded_history, eqns), (dtyps, cases)) =
    4.41    Spec { concluded_history = concluded_history, eqns = eqns, dtyps = dtyps, cases = cases };
    4.42 +val empty_spec =
    4.43 +  mk_spec ((false, Symtab.empty), (Symtab.empty, (Symtab.empty, Symtab.empty)));
    4.44  fun map_spec f (Spec { concluded_history = concluded_history, eqns = eqns,
    4.45    dtyps = dtyps, cases = cases }) =
    4.46    mk_spec (f ((concluded_history, eqns), (dtyps, cases)));
    4.47 @@ -167,7 +159,8 @@
    4.48    let
    4.49      fun merge_eqns ((_, history1), (_, history2)) =
    4.50        let
    4.51 -        val raw_history = AList.merge (op =) (K true) (history1, history2)
    4.52 +        val raw_history = AList.merge (op = : serial * serial -> bool)
    4.53 +          (K true) (history1, history2)
    4.54          val filtered_history = filter_out (fst o snd) raw_history
    4.55          val history = if null filtered_history
    4.56            then raw_history else filtered_history;
    4.57 @@ -179,57 +172,16 @@
    4.58    in mk_spec ((false, eqns), (dtyps, cases)) end;
    4.59  
    4.60  
    4.61 -(* pre- and postprocessor *)
    4.62 -
    4.63 -datatype thmproc = Thmproc of {
    4.64 -  pre: simpset,
    4.65 -  post: simpset,
    4.66 -  functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
    4.67 -};
    4.68 -
    4.69 -fun mk_thmproc ((pre, post), functrans) =
    4.70 -  Thmproc { pre = pre, post = post, functrans = functrans };
    4.71 -fun map_thmproc f (Thmproc { pre, post, functrans }) =
    4.72 -  mk_thmproc (f ((pre, post), functrans));
    4.73 -fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 },
    4.74 -  Thmproc { pre = pre2, post = post2, functrans = functrans2 }) =
    4.75 -    let
    4.76 -      val pre = Simplifier.merge_ss (pre1, pre2);
    4.77 -      val post = Simplifier.merge_ss (post1, post2);
    4.78 -      val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
    4.79 -    in mk_thmproc ((pre, post), functrans) end;
    4.80 -
    4.81 -datatype exec = Exec of {
    4.82 -  thmproc: thmproc,
    4.83 -  spec: spec
    4.84 -};
    4.85 -
    4.86 -
    4.87  (* code setup data *)
    4.88  
    4.89 -fun mk_exec (thmproc, spec) =
    4.90 -  Exec { thmproc = thmproc, spec = spec };
    4.91 -fun map_exec f (Exec { thmproc = thmproc, spec = spec }) =
    4.92 -  mk_exec (f (thmproc, spec));
    4.93 -fun merge_exec (Exec { thmproc = thmproc1, spec = spec1 },
    4.94 -  Exec { thmproc = thmproc2, spec = spec2 }) =
    4.95 -  let
    4.96 -    val thmproc = merge_thmproc (thmproc1, thmproc2);
    4.97 -    val spec = merge_spec (spec1, spec2);
    4.98 -  in mk_exec (thmproc, spec) end;
    4.99 -val empty_exec = mk_exec (mk_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []),
   4.100 -  mk_spec ((false, Symtab.empty), (Symtab.empty, (Symtab.empty, Symtab.empty))));
   4.101 -
   4.102 -fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x;
   4.103 -fun the_spec (Exec { spec = Spec x, ...}) = x;
   4.104 +fun the_spec (Spec x) = x;
   4.105  val the_eqns = #eqns o the_spec;
   4.106  val the_dtyps = #dtyps o the_spec;
   4.107  val the_cases = #cases o the_spec;
   4.108 -val map_thmproc = map_exec o apfst o map_thmproc;
   4.109 -val map_concluded_history = map_exec o apsnd o map_spec o apfst o apfst;
   4.110 -val map_eqns = map_exec o apsnd o map_spec o apfst o apsnd;
   4.111 -val map_dtyps = map_exec o apsnd o map_spec o apsnd o apfst;
   4.112 -val map_cases = map_exec o apsnd o map_spec o apsnd o apsnd;
   4.113 +val map_concluded_history = map_spec o apfst o apfst;
   4.114 +val map_eqns = map_spec o apfst o apsnd;
   4.115 +val map_dtyps = map_spec o apsnd o apfst;
   4.116 +val map_cases = map_spec o apsnd o apsnd;
   4.117  
   4.118  
   4.119  (* data slots dependent on executable content *)
   4.120 @@ -277,17 +229,17 @@
   4.121  type data = Object.T Datatab.table;
   4.122  val empty_data = Datatab.empty : data;
   4.123  
   4.124 -structure CodeData = TheoryDataFun
   4.125 +structure Code_Data = TheoryDataFun
   4.126  (
   4.127 -  type T = exec * data ref;
   4.128 -  val empty = (empty_exec, ref empty_data);
   4.129 -  fun copy (exec, data) = (exec, ref (! data));
   4.130 +  type T = spec * data ref;
   4.131 +  val empty = (empty_spec, ref empty_data);
   4.132 +  fun copy (spec, data) = (spec, ref (! data));
   4.133    val extend = copy;
   4.134 -  fun merge pp ((exec1, data1), (exec2, data2)) =
   4.135 -    (merge_exec (exec1, exec2), ref empty_data);
   4.136 +  fun merge pp ((spec1, data1), (spec2, data2)) =
   4.137 +    (merge_spec (spec1, spec2), ref empty_data);
   4.138  );
   4.139  
   4.140 -fun thy_data f thy = f ((snd o CodeData.get) thy);
   4.141 +fun thy_data f thy = f ((snd o Code_Data.get) thy);
   4.142  
   4.143  fun get_ensure_init kind data_ref =
   4.144    case Datatab.lookup (! data_ref) kind
   4.145 @@ -299,7 +251,7 @@
   4.146  
   4.147  (* access to executable content *)
   4.148  
   4.149 -val the_exec = fst o CodeData.get;
   4.150 +val the_exec = fst o Code_Data.get;
   4.151  
   4.152  fun complete_class_params thy cs =
   4.153    fold (fn c => case AxClass.inst_of_param thy c
   4.154 @@ -307,11 +259,11 @@
   4.155      | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
   4.156  
   4.157  fun map_exec_purge touched f thy =
   4.158 -  CodeData.map (fn (exec, data) => (f exec, ref (case touched
   4.159 +  Code_Data.map (fn (exec, data) => (f exec, ref (case touched
   4.160     of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
   4.161      | NONE => empty_data))) thy;
   4.162  
   4.163 -val purge_data = (CodeData.map o apsnd) (K (ref empty_data));
   4.164 +val purge_data = (Code_Data.map o apsnd) (K (ref empty_data));
   4.165  
   4.166  
   4.167  (* tackling equation history *)
   4.168 @@ -323,21 +275,21 @@
   4.169  
   4.170  fun continue_history thy = if (#concluded_history o the_spec o the_exec) thy
   4.171    then thy
   4.172 -    |> (CodeData.map o apfst o map_concluded_history) (K false)
   4.173 +    |> (Code_Data.map o apfst o map_concluded_history) (K false)
   4.174      |> SOME
   4.175    else NONE;
   4.176  
   4.177  fun conclude_history thy = if (#concluded_history o the_spec o the_exec) thy
   4.178    then NONE
   4.179    else thy
   4.180 -    |> (CodeData.map o apfst)
   4.181 +    |> (Code_Data.map o apfst)
   4.182          ((map_eqns o Symtab.map) (fn ((changed, current), history) =>
   4.183            ((false, current),
   4.184              if changed then (serial (), current) :: history else history))
   4.185          #> map_concluded_history (K true))
   4.186      |> SOME;
   4.187  
   4.188 -val _ = Context.>> (Context.map_theory (CodeData.init
   4.189 +val _ = Context.>> (Context.map_theory (Code_Data.init
   4.190    #> Theory.at_begin continue_history
   4.191    #> Theory.at_end conclude_history));
   4.192  
   4.193 @@ -366,9 +318,6 @@
   4.194  
   4.195  end; (*local*)
   4.196  
   4.197 -
   4.198 -(* print executable content *)
   4.199 -
   4.200  fun print_codesetup thy =
   4.201    let
   4.202      val ctxt = ProofContext.init thy;
   4.203 @@ -390,9 +339,6 @@
   4.204                            :: Pretty.str "of"
   4.205                            :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
   4.206            );
   4.207 -    val pre = (#pre o the_thmproc) exec;
   4.208 -    val post = (#post o the_thmproc) exec;
   4.209 -    val functrans = (map fst o #functrans o the_thmproc) exec;
   4.210      val eqns = the_eqns exec
   4.211        |> Symtab.dest
   4.212        |> (map o apfst) (Code_Unit.string_of_const thy)
   4.213 @@ -410,21 +356,6 @@
   4.214          :: Pretty.fbrk
   4.215          :: (Pretty.fbreaks o map pretty_eqn) eqns
   4.216        ),
   4.217 -      Pretty.block [
   4.218 -        Pretty.str "preprocessing simpset:",
   4.219 -        Pretty.fbrk,
   4.220 -        Simplifier.pretty_ss ctxt pre
   4.221 -      ],
   4.222 -      Pretty.block [
   4.223 -        Pretty.str "postprocessing simpset:",
   4.224 -        Pretty.fbrk,
   4.225 -        Simplifier.pretty_ss ctxt post
   4.226 -      ],
   4.227 -      Pretty.block (
   4.228 -        Pretty.str "function transformers:"
   4.229 -        :: Pretty.fbrk
   4.230 -        :: (Pretty.fbreaks o map Pretty.str) functrans
   4.231 -      ),
   4.232        Pretty.block (
   4.233          Pretty.str "datatypes:"
   4.234          :: Pretty.fbrk
   4.235 @@ -461,10 +392,6 @@
   4.236  
   4.237  (** interfaces and attributes **)
   4.238  
   4.239 -fun delete_force msg key xs =
   4.240 -  if AList.defined (op =) xs key then AList.delete (op =) key xs
   4.241 -  else error ("No such " ^ msg ^ ": " ^ quote key);
   4.242 -
   4.243  fun get_datatype thy tyco =
   4.244    case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco)
   4.245     of (_, spec) :: _ => spec
   4.246 @@ -568,26 +495,6 @@
   4.247  fun add_undefined c thy =
   4.248    (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy;
   4.249  
   4.250 -val map_pre = map_exec_purge NONE o map_thmproc o apfst o apfst;
   4.251 -val map_post = map_exec_purge NONE o map_thmproc o apfst o apsnd;
   4.252 -
   4.253 -val add_inline = map_pre o MetaSimplifier.add_simp;
   4.254 -val del_inline = map_pre o MetaSimplifier.del_simp;
   4.255 -val add_post = map_post o MetaSimplifier.add_simp;
   4.256 -val del_post = map_post o MetaSimplifier.del_simp;
   4.257 -  
   4.258 -fun add_functrans (name, f) =
   4.259 -  (map_exec_purge NONE o map_thmproc o apsnd)
   4.260 -    (AList.update (op =) (name, (serial (), f)));
   4.261 -
   4.262 -fun del_functrans name =
   4.263 -  (map_exec_purge NONE o map_thmproc o apsnd)
   4.264 -    (delete_force "function transformer" name);
   4.265 -
   4.266 -fun simple_functrans f thy eqns = case f thy (map fst eqns)
   4.267 - of SOME thms' => SOME (map (rpair (forall snd eqns)) thms')
   4.268 -  | NONE => NONE;
   4.269 -
   4.270  val _ = Context.>> (Context.map_theory
   4.271    (let
   4.272      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   4.273 @@ -600,77 +507,12 @@
   4.274      TypeInterpretation.init
   4.275      #> add_del_attribute ("", (add_eqn, del_eqn))
   4.276      #> add_simple_attribute ("nbe", add_nbe_eqn)
   4.277 -    #> add_del_attribute ("inline", (add_inline, del_inline))
   4.278 -    #> add_del_attribute ("post", (add_post, del_post))
   4.279    end));
   4.280  
   4.281 -
   4.282 -(** post- and preprocessing **)
   4.283 -
   4.284 -local
   4.285 -
   4.286 -fun apply_functrans thy c _ [] = []
   4.287 -  | apply_functrans thy c [] eqns = eqns
   4.288 -  | apply_functrans thy c functrans eqns = eqns
   4.289 -      |> perhaps (perhaps_loop (perhaps_apply functrans))
   4.290 -      |> assert_eqns_const thy c;
   4.291 -
   4.292 -fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
   4.293 -
   4.294 -fun term_of_conv thy f =
   4.295 -  Thm.cterm_of thy
   4.296 -  #> f
   4.297 -  #> Thm.prop_of
   4.298 -  #> Logic.dest_equals
   4.299 -  #> snd;
   4.300 -
   4.301 -fun preprocess thy c eqns =
   4.302 -  let
   4.303 -    val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy;
   4.304 -    val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
   4.305 -      o the_thmproc o the_exec) thy;
   4.306 -  in
   4.307 -    eqns
   4.308 -    |> apply_functrans thy c functrans
   4.309 -    |> (map o apfst) (Code_Unit.rewrite_eqn pre)
   4.310 -    |> (map o apfst) (AxClass.unoverload thy)
   4.311 -    |> map (assert_eqn thy)
   4.312 -    |> burrow_fst (common_typ_eqns thy)
   4.313 -  end;
   4.314 -
   4.315 -in
   4.316 -
   4.317 -fun preprocess_conv thy ct =
   4.318 -  let
   4.319 -    val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy;
   4.320 -  in
   4.321 -    ct
   4.322 -    |> Simplifier.rewrite pre
   4.323 -    |> rhs_conv (AxClass.unoverload_conv thy)
   4.324 -  end;
   4.325 -
   4.326 -fun preprocess_term thy = term_of_conv thy (preprocess_conv thy);
   4.327 -
   4.328 -fun postprocess_conv thy ct =
   4.329 -  let
   4.330 -    val post = (Simplifier.theory_context thy o #post o the_thmproc o the_exec) thy;
   4.331 -  in
   4.332 -    ct
   4.333 -    |> AxClass.overload_conv thy
   4.334 -    |> rhs_conv (Simplifier.rewrite post)
   4.335 -  end;
   4.336 -
   4.337 -fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
   4.338 -
   4.339 -fun these_raw_eqns thy c =
   4.340 -  get_eqns thy c
   4.341 -  |> (map o apfst) (Thm.transfer thy)
   4.342 -  |> burrow_fst (common_typ_eqns thy);
   4.343 -
   4.344  fun these_eqns thy c =
   4.345    get_eqns thy c
   4.346    |> (map o apfst) (Thm.transfer thy)
   4.347 -  |> preprocess thy c;
   4.348 +  |> burrow_fst (common_typ_eqns thy);
   4.349  
   4.350  fun default_typscheme thy c =
   4.351    let
   4.352 @@ -685,8 +527,6 @@
   4.353           of (thm, _) :: _ => (Code_Unit.typscheme_eqn thy o Drule.zero_var_indexes) thm
   4.354            | [] => strip_sorts (the_const_typscheme c) end;
   4.355  
   4.356 -end; (*local*)
   4.357 -
   4.358  end; (*struct*)
   4.359  
   4.360  
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Tue May 12 17:09:36 2009 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue May 12 19:30:33 2009 +0200
     5.3 @@ -881,7 +881,7 @@
     5.4      (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
     5.5  
     5.6  val _ =
     5.7 -  OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag
     5.8 +  OuterSyntax.improper_command "print_codesetup" "print code generator setup" K.diag
     5.9      (Scan.succeed
    5.10        (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
    5.11          (Code.print_codesetup o Toplevel.theory_of)));
     6.1 --- a/src/Pure/codegen.ML	Tue May 12 17:09:36 2009 +0200
     6.2 +++ b/src/Pure/codegen.ML	Tue May 12 19:30:33 2009 +0200
     6.3 @@ -1024,8 +1024,6 @@
     6.4  
     6.5  val setup = add_codegen "default" default_codegen
     6.6    #> add_tycodegen "default" default_tycodegen
     6.7 -  #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
     6.8 -       (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)))
     6.9    #> add_preprocessor unfold_preprocessor;
    6.10  
    6.11  val _ =
     7.1 --- a/src/Tools/Code_Generator.thy	Tue May 12 17:09:36 2009 +0200
     7.2 +++ b/src/Tools/Code_Generator.thy	Tue May 12 19:30:33 2009 +0200
     7.3 @@ -9,7 +9,7 @@
     7.4  uses
     7.5    "~~/src/Tools/value.ML"
     7.6    "~~/src/Tools/quickcheck.ML"
     7.7 -  "~~/src/Tools/code/code_wellsorted.ML" 
     7.8 +  "~~/src/Tools/code/code_preproc.ML" 
     7.9    "~~/src/Tools/code/code_thingol.ML"
    7.10    "~~/src/Tools/code/code_printer.ML"
    7.11    "~~/src/Tools/code/code_target.ML"
    7.12 @@ -19,7 +19,8 @@
    7.13  begin
    7.14  
    7.15  setup {*
    7.16 -  Code_ML.setup
    7.17 +  Code_Preproc.setup
    7.18 +  #> Code_ML.setup
    7.19    #> Code_Haskell.setup
    7.20    #> Nbe.setup
    7.21  *}
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/code/code_preproc.ML	Tue May 12 19:30:33 2009 +0200
     8.3 @@ -0,0 +1,515 @@
     8.4 +(*  Title:      Tools/code/code_preproc.ML
     8.5 +    Author:     Florian Haftmann, TU Muenchen
     8.6 +
     8.7 +Preprocessing code equations into a well-sorted system
     8.8 +in a graph with explicit dependencies.
     8.9 +*)
    8.10 +
    8.11 +signature CODE_PREPROC =
    8.12 +sig
    8.13 +  val map_pre: (simpset -> simpset) -> theory -> theory
    8.14 +  val map_post: (simpset -> simpset) -> theory -> theory
    8.15 +  val add_inline: thm -> theory -> theory
    8.16 +  val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
    8.17 +  val del_functrans: string -> theory -> theory
    8.18 +  val simple_functrans: (theory -> thm list -> thm list option)
    8.19 +    -> theory -> (thm * bool) list -> (thm * bool) list option
    8.20 +  val print_codeproc: theory -> unit
    8.21 +
    8.22 +  type code_algebra
    8.23 +  type code_graph
    8.24 +  val eqns: code_graph -> string -> (thm * bool) list
    8.25 +  val typ: code_graph -> string -> (string * sort) list * typ
    8.26 +  val all: code_graph -> string list
    8.27 +  val pretty: theory -> code_graph -> Pretty.T
    8.28 +  val obtain: theory -> string list -> term list -> code_algebra * code_graph
    8.29 +  val eval_conv: theory -> (sort -> sort)
    8.30 +    -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
    8.31 +  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
    8.32 +    -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
    8.33 +
    8.34 +  val setup: theory -> theory
    8.35 +end
    8.36 +
    8.37 +structure Code_Preproc : CODE_PREPROC =
    8.38 +struct
    8.39 +
    8.40 +(** preprocessor administration **)
    8.41 +
    8.42 +(* theory data *)
    8.43 +
    8.44 +datatype thmproc = Thmproc of {
    8.45 +  pre: simpset,
    8.46 +  post: simpset,
    8.47 +  functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
    8.48 +};
    8.49 +
    8.50 +fun mk_thmproc ((pre, post), functrans) =
    8.51 +  Thmproc { pre = pre, post = post, functrans = functrans };
    8.52 +fun map_thmproc f (Thmproc { pre, post, functrans }) =
    8.53 +  mk_thmproc (f ((pre, post), functrans));
    8.54 +fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 },
    8.55 +  Thmproc { pre = pre2, post = post2, functrans = functrans2 }) =
    8.56 +    let
    8.57 +      val pre = Simplifier.merge_ss (pre1, pre2);
    8.58 +      val post = Simplifier.merge_ss (post1, post2);
    8.59 +      val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
    8.60 +    in mk_thmproc ((pre, post), functrans) end;
    8.61 +
    8.62 +structure Code_Preproc_Data = TheoryDataFun
    8.63 +(
    8.64 +  type T = thmproc;
    8.65 +  val empty = mk_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
    8.66 +  fun copy spec = spec;
    8.67 +  val extend = copy;
    8.68 +  fun merge pp = merge_thmproc;
    8.69 +);
    8.70 +
    8.71 +fun the_thmproc thy = case Code_Preproc_Data.get thy
    8.72 + of Thmproc x => x;
    8.73 +
    8.74 +fun delete_force msg key xs =
    8.75 +  if AList.defined (op =) xs key then AList.delete (op =) key xs
    8.76 +  else error ("No such " ^ msg ^ ": " ^ quote key);
    8.77 +
    8.78 +fun map_data f thy =
    8.79 +  thy
    8.80 +  |> Code.purge_data
    8.81 +  |> (Code_Preproc_Data.map o map_thmproc) f;
    8.82 +
    8.83 +val map_pre = map_data o apfst o apfst;
    8.84 +val map_post = map_data o apfst o apsnd;
    8.85 +
    8.86 +val add_inline = map_pre o MetaSimplifier.add_simp;
    8.87 +val del_inline = map_pre o MetaSimplifier.del_simp;
    8.88 +val add_post = map_post o MetaSimplifier.add_simp;
    8.89 +val del_post = map_post o MetaSimplifier.del_simp;
    8.90 +  
    8.91 +fun add_functrans (name, f) = (map_data o apsnd)
    8.92 +  (AList.update (op =) (name, (serial (), f)));
    8.93 +
    8.94 +fun del_functrans name = (map_data o apsnd)
    8.95 +  (delete_force "function transformer" name);
    8.96 +
    8.97 +
    8.98 +(* post- and preprocessing *)
    8.99 +
   8.100 +fun apply_functrans thy c _ [] = []
   8.101 +  | apply_functrans thy c [] eqns = eqns
   8.102 +  | apply_functrans thy c functrans eqns = eqns
   8.103 +      |> perhaps (perhaps_loop (perhaps_apply functrans))
   8.104 +      |> Code.assert_eqns_const thy c;
   8.105 +
   8.106 +fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
   8.107 +
   8.108 +fun term_of_conv thy f =
   8.109 +  Thm.cterm_of thy
   8.110 +  #> f
   8.111 +  #> Thm.prop_of
   8.112 +  #> Logic.dest_equals
   8.113 +  #> snd;
   8.114 +
   8.115 +fun preprocess thy c eqns =
   8.116 +  let
   8.117 +    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
   8.118 +    val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
   8.119 +      o the_thmproc) thy;
   8.120 +  in
   8.121 +    eqns
   8.122 +    |> apply_functrans thy c functrans
   8.123 +    |> (map o apfst) (Code_Unit.rewrite_eqn pre)
   8.124 +    |> (map o apfst) (AxClass.unoverload thy)
   8.125 +    |> map (Code.assert_eqn thy)
   8.126 +    |> burrow_fst (Code_Unit.norm_args thy)
   8.127 +    |> burrow_fst (Code_Unit.norm_varnames thy)
   8.128 +  end;
   8.129 +
   8.130 +fun preprocess_conv thy ct =
   8.131 +  let
   8.132 +    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
   8.133 +  in
   8.134 +    ct
   8.135 +    |> Simplifier.rewrite pre
   8.136 +    |> rhs_conv (AxClass.unoverload_conv thy)
   8.137 +  end;
   8.138 +
   8.139 +fun postprocess_conv thy ct =
   8.140 +  let
   8.141 +    val post = (Simplifier.theory_context thy o #post o the_thmproc) thy;
   8.142 +  in
   8.143 +    ct
   8.144 +    |> AxClass.overload_conv thy
   8.145 +    |> rhs_conv (Simplifier.rewrite post)
   8.146 +  end;
   8.147 +
   8.148 +fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
   8.149 +
   8.150 +fun print_codeproc thy =
   8.151 +  let
   8.152 +    val ctxt = ProofContext.init thy;
   8.153 +    val pre = (#pre o the_thmproc) thy;
   8.154 +    val post = (#post o the_thmproc) thy;
   8.155 +    val functrans = (map fst o #functrans o the_thmproc) thy;
   8.156 +  in
   8.157 +    (Pretty.writeln o Pretty.chunks) [
   8.158 +      Pretty.block [
   8.159 +        Pretty.str "preprocessing simpset:",
   8.160 +        Pretty.fbrk,
   8.161 +        Simplifier.pretty_ss ctxt pre
   8.162 +      ],
   8.163 +      Pretty.block [
   8.164 +        Pretty.str "postprocessing simpset:",
   8.165 +        Pretty.fbrk,
   8.166 +        Simplifier.pretty_ss ctxt post
   8.167 +      ],
   8.168 +      Pretty.block (
   8.169 +        Pretty.str "function transformers:"
   8.170 +        :: Pretty.fbrk
   8.171 +        :: (Pretty.fbreaks o map Pretty.str) functrans
   8.172 +      )
   8.173 +    ]
   8.174 +  end;
   8.175 +
   8.176 +fun simple_functrans f thy eqns = case f thy (map fst eqns)
   8.177 + of SOME thms' => SOME (map (rpair (forall snd eqns)) thms')
   8.178 +  | NONE => NONE;
   8.179 +
   8.180 +
   8.181 +(** sort algebra and code equation graph types **)
   8.182 +
   8.183 +type code_algebra = (sort -> sort) * Sorts.algebra;
   8.184 +type code_graph = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
   8.185 +
   8.186 +fun eqns eqngr = these o Option.map snd o try (Graph.get_node eqngr);
   8.187 +fun typ eqngr = fst o Graph.get_node eqngr;
   8.188 +fun all eqngr = Graph.keys eqngr;
   8.189 +
   8.190 +fun pretty thy eqngr =
   8.191 +  AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
   8.192 +  |> (map o apfst) (Code_Unit.string_of_const thy)
   8.193 +  |> sort (string_ord o pairself fst)
   8.194 +  |> map (fn (s, thms) =>
   8.195 +       (Pretty.block o Pretty.fbreaks) (
   8.196 +         Pretty.str s
   8.197 +         :: map (Display.pretty_thm o fst) thms
   8.198 +       ))
   8.199 +  |> Pretty.chunks;
   8.200 +
   8.201 +
   8.202 +(** the Waisenhaus algorithm **)
   8.203 +
   8.204 +(* auxiliary *)
   8.205 +
   8.206 +fun is_proper_class thy = can (AxClass.get_info thy);
   8.207 +
   8.208 +fun complete_proper_sort thy =
   8.209 +  Sign.complete_sort thy #> filter (is_proper_class thy);
   8.210 +
   8.211 +fun inst_params thy tyco =
   8.212 +  map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
   8.213 +    o maps (#params o AxClass.get_info thy);
   8.214 +
   8.215 +fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
   8.216 +  (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
   8.217 +    (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
   8.218 +
   8.219 +fun tyscm_rhss_of thy c eqns =
   8.220 +  let
   8.221 +    val tyscm = case eqns of [] => Code.default_typscheme thy c
   8.222 +      | ((thm, _) :: _) => Code_Unit.typscheme_eqn thy thm;
   8.223 +    val rhss = consts_of thy eqns;
   8.224 +  in (tyscm, rhss) end;
   8.225 +
   8.226 +
   8.227 +(* data structures *)
   8.228 +
   8.229 +datatype const = Fun of string | Inst of class * string;
   8.230 +
   8.231 +fun const_ord (Fun c1, Fun c2) = fast_string_ord (c1, c2)
   8.232 +  | const_ord (Inst class_tyco1, Inst class_tyco2) =
   8.233 +      prod_ord fast_string_ord fast_string_ord (class_tyco1, class_tyco2)
   8.234 +  | const_ord (Fun _, Inst _) = LESS
   8.235 +  | const_ord (Inst _, Fun _) = GREATER;
   8.236 +
   8.237 +type var = const * int;
   8.238 +
   8.239 +structure Vargraph =
   8.240 +  GraphFun(type key = var val ord = prod_ord const_ord int_ord);
   8.241 +
   8.242 +datatype styp = Tyco of string * styp list | Var of var | Free;
   8.243 +
   8.244 +fun styp_of c_lhs (Type (tyco, tys)) = Tyco (tyco, map (styp_of c_lhs) tys)
   8.245 +  | styp_of c_lhs (TFree (v, _)) = case c_lhs
   8.246 +     of SOME (c, lhs) => Var (Fun c, find_index (fn (v', _) => v = v') lhs)
   8.247 +      | NONE => Free;
   8.248 +
   8.249 +type vardeps_data = ((string * styp list) list * class list) Vargraph.T
   8.250 +  * (((string * sort) list * (thm * bool) list) Symtab.table
   8.251 +    * (class * string) list);
   8.252 +
   8.253 +val empty_vardeps_data : vardeps_data =
   8.254 +  (Vargraph.empty, (Symtab.empty, []));
   8.255 +
   8.256 +
   8.257 +(* retrieving equations and instances from the background context *)
   8.258 +
   8.259 +fun obtain_eqns thy eqngr c =
   8.260 +  case try (Graph.get_node eqngr) c
   8.261 +   of SOME ((lhs, _), eqns) => ((lhs, []), [])
   8.262 +    | NONE => let
   8.263 +        val eqns = Code.these_eqns thy c
   8.264 +          |> preprocess thy c;
   8.265 +        val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns;
   8.266 +      in ((lhs, rhss), eqns) end;
   8.267 +
   8.268 +fun obtain_instance thy arities (inst as (class, tyco)) =
   8.269 +  case AList.lookup (op =) arities inst
   8.270 +   of SOME classess => (classess, ([], []))
   8.271 +    | NONE => let
   8.272 +        val all_classes = complete_proper_sort thy [class];
   8.273 +        val superclasses = remove (op =) class all_classes
   8.274 +        val classess = map (complete_proper_sort thy)
   8.275 +          (Sign.arity_sorts thy tyco [class]);
   8.276 +        val inst_params = inst_params thy tyco all_classes;
   8.277 +      in (classess, (superclasses, inst_params)) end;
   8.278 +
   8.279 +
   8.280 +(* computing instantiations *)
   8.281 +
   8.282 +fun add_classes thy arities eqngr c_k new_classes vardeps_data =
   8.283 +  let
   8.284 +    val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
   8.285 +    val diff_classes = new_classes |> subtract (op =) old_classes;
   8.286 +  in if null diff_classes then vardeps_data
   8.287 +  else let
   8.288 +    val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k;
   8.289 +  in
   8.290 +    vardeps_data
   8.291 +    |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
   8.292 +    |> fold (fn styp => fold (ensure_typmatch_inst thy arities eqngr styp) new_classes) styps
   8.293 +    |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
   8.294 +  end end
   8.295 +and add_styp thy arities eqngr c_k tyco_styps vardeps_data =
   8.296 +  let
   8.297 +    val (old_styps, classes) = Vargraph.get_node (fst vardeps_data) c_k;
   8.298 +  in if member (op =) old_styps tyco_styps then vardeps_data
   8.299 +  else
   8.300 +    vardeps_data
   8.301 +    |> (apfst o Vargraph.map_node c_k o apfst) (cons tyco_styps)
   8.302 +    |> fold (ensure_typmatch_inst thy arities eqngr tyco_styps) classes
   8.303 +  end
   8.304 +and add_dep thy arities eqngr c_k c_k' vardeps_data =
   8.305 +  let
   8.306 +    val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k;
   8.307 +  in
   8.308 +    vardeps_data
   8.309 +    |> add_classes thy arities eqngr c_k' classes
   8.310 +    |> apfst (Vargraph.add_edge (c_k, c_k'))
   8.311 +  end
   8.312 +and ensure_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
   8.313 +  if can (Sign.arity_sorts thy tyco) [class]
   8.314 +  then vardeps_data
   8.315 +    |> ensure_inst thy arities eqngr (class, tyco)
   8.316 +    |> fold_index (fn (k, styp) =>
   8.317 +         ensure_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
   8.318 +  else vardeps_data (*permissive!*)
   8.319 +and ensure_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
   8.320 +  if member (op =) insts inst then vardeps_data
   8.321 +  else let
   8.322 +    val (classess, (superclasses, inst_params)) =
   8.323 +      obtain_instance thy arities inst;
   8.324 +  in
   8.325 +    vardeps_data
   8.326 +    |> (apsnd o apsnd) (insert (op =) inst)
   8.327 +    |> fold_index (fn (k, _) =>
   8.328 +         apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess
   8.329 +    |> fold (fn superclass => ensure_inst thy arities eqngr (superclass, tyco)) superclasses
   8.330 +    |> fold (ensure_fun thy arities eqngr) inst_params
   8.331 +    |> fold_index (fn (k, classes) =>
   8.332 +         add_classes thy arities eqngr (Inst (class, tyco), k) classes
   8.333 +         #> fold (fn superclass =>
   8.334 +             add_dep thy arities eqngr (Inst (superclass, tyco), k)
   8.335 +             (Inst (class, tyco), k)) superclasses
   8.336 +         #> fold (fn inst_param =>
   8.337 +             add_dep thy arities eqngr (Fun inst_param, k)
   8.338 +             (Inst (class, tyco), k)
   8.339 +             ) inst_params
   8.340 +         ) classess
   8.341 +  end
   8.342 +and ensure_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
   8.343 +      vardeps_data
   8.344 +      |> add_styp thy arities eqngr c_k tyco_styps
   8.345 +  | ensure_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
   8.346 +      vardeps_data
   8.347 +      |> add_dep thy arities eqngr c_k c_k'
   8.348 +  | ensure_typmatch thy arities eqngr Free c_k vardeps_data =
   8.349 +      vardeps_data
   8.350 +and ensure_rhs thy arities eqngr (c', styps) vardeps_data =
   8.351 +  vardeps_data
   8.352 +  |> ensure_fun thy arities eqngr c'
   8.353 +  |> fold_index (fn (k, styp) =>
   8.354 +       ensure_typmatch thy arities eqngr styp (Fun c', k)) styps
   8.355 +and ensure_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) =
   8.356 +  if Symtab.defined eqntab c then vardeps_data
   8.357 +  else let
   8.358 +    val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
   8.359 +    val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
   8.360 +  in
   8.361 +    vardeps_data
   8.362 +    |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
   8.363 +    |> fold_index (fn (k, _) =>
   8.364 +         apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs
   8.365 +    |> fold_index (fn (k, (_, sort)) =>
   8.366 +         add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
   8.367 +    |> fold (ensure_rhs thy arities eqngr) rhss'
   8.368 +  end;
   8.369 +
   8.370 +
   8.371 +(* applying instantiations *)
   8.372 +
   8.373 +fun dicts_of thy (proj_sort, algebra) (T, sort) =
   8.374 +  let
   8.375 +    fun class_relation (x, _) _ = x;
   8.376 +    fun type_constructor tyco xs class =
   8.377 +      inst_params thy tyco (Sorts.complete_sort algebra [class])
   8.378 +        @ (maps o maps) fst xs;
   8.379 +    fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
   8.380 +  in
   8.381 +    flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
   8.382 +      { class_relation = class_relation, type_constructor = type_constructor,
   8.383 +        type_variable = type_variable } (T, proj_sort sort)
   8.384 +       handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
   8.385 +  end;
   8.386 +
   8.387 +fun add_arity thy vardeps (class, tyco) =
   8.388 +  AList.default (op =)
   8.389 +    ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
   8.390 +      (0 upto Sign.arity_number thy tyco - 1));
   8.391 +
   8.392 +fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
   8.393 +  if can (Graph.get_node eqngr) c then (rhss, eqngr)
   8.394 +  else let
   8.395 +    val lhs = map_index (fn (k, (v, _)) =>
   8.396 +      (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
   8.397 +    val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
   8.398 +      Vartab.update ((v, 0), sort)) lhs;
   8.399 +    val eqns = proto_eqns
   8.400 +      |> (map o apfst) (Code_Unit.inst_thm thy inst_tab);
   8.401 +    val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
   8.402 +    val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
   8.403 +  in (map (pair c) rhss' @ rhss, eqngr') end;
   8.404 +
   8.405 +fun extend_arities_eqngr thy cs ts (arities, eqngr) =
   8.406 +  let
   8.407 +    val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
   8.408 +      insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
   8.409 +    val (vardeps, (eqntab, insts)) = empty_vardeps_data
   8.410 +      |> fold (ensure_fun thy arities eqngr) cs
   8.411 +      |> fold (ensure_rhs thy arities eqngr) cs_rhss;
   8.412 +    val arities' = fold (add_arity thy vardeps) insts arities;
   8.413 +    val pp = Syntax.pp_global thy;
   8.414 +    val algebra = Sorts.subalgebra pp (is_proper_class thy)
   8.415 +      (AList.lookup (op =) arities') (Sign.classes_of thy);
   8.416 +    val (rhss, eqngr') = Symtab.fold (add_eqs thy vardeps) eqntab ([], eqngr);
   8.417 +    fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
   8.418 +      (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
   8.419 +    val eqngr'' = fold (fn (c, rhs) => fold
   8.420 +      (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
   8.421 +  in (algebra, (arities', eqngr'')) end;
   8.422 +
   8.423 +
   8.424 +(** store for preprocessed arities and code equations **)
   8.425 +
   8.426 +structure Wellsorted = CodeDataFun
   8.427 +(
   8.428 +  type T = ((string * class) * sort list) list * code_graph;
   8.429 +  val empty = ([], Graph.empty);
   8.430 +  fun purge thy cs (arities, eqngr) =
   8.431 +    let
   8.432 +      val del_cs = ((Graph.all_preds eqngr
   8.433 +        o filter (can (Graph.get_node eqngr))) cs);
   8.434 +      val del_arities = del_cs
   8.435 +        |> map_filter (AxClass.inst_of_param thy)
   8.436 +        |> maps (fn (c, tyco) =>
   8.437 +             (map (rpair tyco) o Sign.complete_sort thy o the_list
   8.438 +               o AxClass.class_of_param thy) c);
   8.439 +      val arities' = fold (AList.delete (op =)) del_arities arities;
   8.440 +      val eqngr' = Graph.del_nodes del_cs eqngr;
   8.441 +    in (arities', eqngr') end;
   8.442 +);
   8.443 +
   8.444 +
   8.445 +(** retrieval and evaluation interfaces **)
   8.446 +
   8.447 +fun obtain thy cs ts = apsnd snd
   8.448 +  (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
   8.449 +
   8.450 +fun prepare_sorts_typ prep_sort
   8.451 +  = map_type_tfree (fn (v, sort) => TFree (v, prep_sort sort));
   8.452 +
   8.453 +fun prepare_sorts prep_sort (Const (c, ty)) =
   8.454 +      Const (c, prepare_sorts_typ prep_sort ty)
   8.455 +  | prepare_sorts prep_sort (t1 $ t2) =
   8.456 +      prepare_sorts prep_sort t1 $ prepare_sorts prep_sort t2
   8.457 +  | prepare_sorts prep_sort (Abs (v, ty, t)) =
   8.458 +      Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t)
   8.459 +  | prepare_sorts _ (t as Bound _) = t;
   8.460 +
   8.461 +fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct =
   8.462 +  let
   8.463 +    val pp = Syntax.pp_global thy;
   8.464 +    val ct = cterm_of proto_ct;
   8.465 +    val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp)
   8.466 +      (Thm.term_of ct);
   8.467 +    val thm = preprocess_conv thy ct;
   8.468 +    val ct' = Thm.rhs_of thm;
   8.469 +    val t' = Thm.term_of ct';
   8.470 +    val vs = Term.add_tfrees t' [];
   8.471 +    val consts = fold_aterms
   8.472 +      (fn Const (c, _) => insert (op =) c | _ => I) t' [];
   8.473 + 
   8.474 +    val t'' = prepare_sorts prep_sort t';
   8.475 +    val (algebra', eqngr') = obtain thy consts [t''];
   8.476 +  in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end;
   8.477 +
   8.478 +fun simple_evaluator evaluator algebra eqngr vs t ct =
   8.479 +  evaluator algebra eqngr vs t;
   8.480 +
   8.481 +fun eval_conv thy =
   8.482 +  let
   8.483 +    fun conclude_evaluation thm2 thm1 =
   8.484 +      let
   8.485 +        val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
   8.486 +      in
   8.487 +        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
   8.488 +          error ("could not construct evaluation proof:\n"
   8.489 +          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
   8.490 +      end;
   8.491 +  in gen_eval thy I conclude_evaluation end;
   8.492 +
   8.493 +fun eval thy prep_sort postproc evaluator = gen_eval thy (Thm.cterm_of thy)
   8.494 +  (K o postproc (postprocess_term thy)) prep_sort (simple_evaluator evaluator);
   8.495 +
   8.496 +
   8.497 +(** setup **)
   8.498 +
   8.499 +val setup = 
   8.500 +  let
   8.501 +    fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   8.502 +    fun add_del_attribute (name, (add, del)) =
   8.503 +      Code.add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
   8.504 +        || Scan.succeed (mk_attribute add))
   8.505 +  in
   8.506 +    add_del_attribute ("inline", (add_inline, del_inline))
   8.507 +    #> add_del_attribute ("post", (add_post, del_post))
   8.508 +    #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
   8.509 +       (fn thm => Context.mapping (Codegen.add_unfold thm #> add_inline thm) I)))
   8.510 +  end;
   8.511 +
   8.512 +val _ =
   8.513 +  OuterSyntax.improper_command "print_codeproc" "print code preprocessor setup"
   8.514 +  OuterKeyword.diag (Scan.succeed
   8.515 +      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
   8.516 +        (print_codeproc o Toplevel.theory_of)));
   8.517 +
   8.518 +end; (*struct*)
     9.1 --- a/src/Tools/code/code_thingol.ML	Tue May 12 17:09:36 2009 +0200
     9.2 +++ b/src/Tools/code/code_thingol.ML	Tue May 12 19:30:33 2009 +0200
     9.3 @@ -509,7 +509,7 @@
     9.4       of SOME tyco => stmt_datatypecons tyco
     9.5        | NONE => (case AxClass.class_of_param thy c
     9.6           of SOME class => stmt_classparam class
     9.7 -          | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
     9.8 +          | NONE => stmt_fun (Code_Preproc.typ funcgr c, Code_Preproc.eqns funcgr c))
     9.9    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
    9.10  and ensure_class thy (algbr as (_, algebra)) funcgr class =
    9.11    let
    9.12 @@ -603,7 +603,7 @@
    9.13  and translate_const thy algbr funcgr thm (c, ty) =
    9.14    let
    9.15      val tys = Sign.const_typargs thy (c, ty);
    9.16 -    val sorts = (map snd o fst o Code_Wellsorted.typ funcgr) c;
    9.17 +    val sorts = (map snd o fst o Code_Preproc.typ funcgr) c;
    9.18      val tys_args = (fst o Term.strip_type) ty;
    9.19    in
    9.20      ensure_const thy algbr funcgr c
    9.21 @@ -748,7 +748,7 @@
    9.22      fun generate_consts thy algebra funcgr =
    9.23        fold_map (ensure_const thy algebra funcgr);
    9.24    in
    9.25 -    invoke_generation thy (Code_Wellsorted.obtain thy cs []) generate_consts cs
    9.26 +    invoke_generation thy (Code_Preproc.obtain thy cs []) generate_consts cs
    9.27      |-> project_consts
    9.28    end;
    9.29  
    9.30 @@ -788,8 +788,8 @@
    9.31      val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
    9.32    in evaluator naming program ((vs'', (vs', ty')), t') deps end;
    9.33  
    9.34 -fun eval_conv thy prep_sort = Code_Wellsorted.eval_conv thy prep_sort o base_evaluator thy;
    9.35 -fun eval thy prep_sort postproc = Code_Wellsorted.eval thy prep_sort postproc o base_evaluator thy;
    9.36 +fun eval_conv thy prep_sort = Code_Preproc.eval_conv thy prep_sort o base_evaluator thy;
    9.37 +fun eval thy prep_sort postproc = Code_Preproc.eval thy prep_sort postproc o base_evaluator thy;
    9.38  
    9.39  
    9.40  (** diagnostic commands **)
    9.41 @@ -817,7 +817,7 @@
    9.42  
    9.43  fun code_depgr thy consts =
    9.44    let
    9.45 -    val (_, eqngr) = Code_Wellsorted.obtain thy consts [];
    9.46 +    val (_, eqngr) = Code_Preproc.obtain thy consts [];
    9.47      val select = Graph.all_succs eqngr consts;
    9.48    in
    9.49      eqngr
    9.50 @@ -825,7 +825,7 @@
    9.51      |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
    9.52    end;
    9.53  
    9.54 -fun code_thms thy = Pretty.writeln o Code_Wellsorted.pretty thy o code_depgr thy;
    9.55 +fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy;
    9.56  
    9.57  fun code_deps thy consts =
    9.58    let
    10.1 --- a/src/Tools/code/code_wellsorted.ML	Tue May 12 17:09:36 2009 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,342 +0,0 @@
    10.4 -(*  Title:      Tools/code/code_wellsorted.ML
    10.5 -    Author:     Florian Haftmann, TU Muenchen
    10.6 -
    10.7 -Producing well-sorted systems of code equations in a graph
    10.8 -with explicit dependencies -- the Waisenhaus algorithm.
    10.9 -*)
   10.10 -
   10.11 -signature CODE_WELLSORTED =
   10.12 -sig
   10.13 -  type code_algebra
   10.14 -  type code_graph
   10.15 -  val eqns: code_graph -> string -> (thm * bool) list
   10.16 -  val typ: code_graph -> string -> (string * sort) list * typ
   10.17 -  val all: code_graph -> string list
   10.18 -  val pretty: theory -> code_graph -> Pretty.T
   10.19 -  val obtain: theory -> string list -> term list -> code_algebra * code_graph
   10.20 -  val eval_conv: theory -> (sort -> sort)
   10.21 -    -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
   10.22 -  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
   10.23 -    -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
   10.24 -end
   10.25 -
   10.26 -structure Code_Wellsorted : CODE_WELLSORTED =
   10.27 -struct
   10.28 -
   10.29 -(** the algebra and code equation graph types **)
   10.30 -
   10.31 -type code_algebra = (sort -> sort) * Sorts.algebra;
   10.32 -type code_graph = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
   10.33 -
   10.34 -fun eqns eqngr = these o Option.map snd o try (Graph.get_node eqngr);
   10.35 -fun typ eqngr = fst o Graph.get_node eqngr;
   10.36 -fun all eqngr = Graph.keys eqngr;
   10.37 -
   10.38 -fun pretty thy eqngr =
   10.39 -  AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
   10.40 -  |> (map o apfst) (Code_Unit.string_of_const thy)
   10.41 -  |> sort (string_ord o pairself fst)
   10.42 -  |> map (fn (s, thms) =>
   10.43 -       (Pretty.block o Pretty.fbreaks) (
   10.44 -         Pretty.str s
   10.45 -         :: map (Display.pretty_thm o fst) thms
   10.46 -       ))
   10.47 -  |> Pretty.chunks;
   10.48 -
   10.49 -
   10.50 -(** the Waisenhaus algorithm **)
   10.51 -
   10.52 -(* auxiliary *)
   10.53 -
   10.54 -fun is_proper_class thy = can (AxClass.get_info thy);
   10.55 -
   10.56 -fun complete_proper_sort thy =
   10.57 -  Sign.complete_sort thy #> filter (is_proper_class thy);
   10.58 -
   10.59 -fun inst_params thy tyco =
   10.60 -  map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
   10.61 -    o maps (#params o AxClass.get_info thy);
   10.62 -
   10.63 -fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
   10.64 -  (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
   10.65 -    (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
   10.66 -
   10.67 -fun tyscm_rhss_of thy c eqns =
   10.68 -  let
   10.69 -    val tyscm = case eqns of [] => Code.default_typscheme thy c
   10.70 -      | ((thm, _) :: _) => Code_Unit.typscheme_eqn thy thm;
   10.71 -    val rhss = consts_of thy eqns;
   10.72 -  in (tyscm, rhss) end;
   10.73 -
   10.74 -
   10.75 -(* data structures *)
   10.76 -
   10.77 -datatype const = Fun of string | Inst of class * string;
   10.78 -
   10.79 -fun const_ord (Fun c1, Fun c2) = fast_string_ord (c1, c2)
   10.80 -  | const_ord (Inst class_tyco1, Inst class_tyco2) =
   10.81 -      prod_ord fast_string_ord fast_string_ord (class_tyco1, class_tyco2)
   10.82 -  | const_ord (Fun _, Inst _) = LESS
   10.83 -  | const_ord (Inst _, Fun _) = GREATER;
   10.84 -
   10.85 -type var = const * int;
   10.86 -
   10.87 -structure Vargraph =
   10.88 -  GraphFun(type key = var val ord = prod_ord const_ord int_ord);
   10.89 -
   10.90 -datatype styp = Tyco of string * styp list | Var of var | Free;
   10.91 -
   10.92 -fun styp_of c_lhs (Type (tyco, tys)) = Tyco (tyco, map (styp_of c_lhs) tys)
   10.93 -  | styp_of c_lhs (TFree (v, _)) = case c_lhs
   10.94 -     of SOME (c, lhs) => Var (Fun c, find_index (fn (v', _) => v = v') lhs)
   10.95 -      | NONE => Free;
   10.96 -
   10.97 -type vardeps_data = ((string * styp list) list * class list) Vargraph.T
   10.98 -  * (((string * sort) list * (thm * bool) list) Symtab.table
   10.99 -    * (class * string) list);
  10.100 -
  10.101 -val empty_vardeps_data : vardeps_data =
  10.102 -  (Vargraph.empty, (Symtab.empty, []));
  10.103 -
  10.104 -
  10.105 -(* retrieving equations and instances from the background context *)
  10.106 -
  10.107 -fun obtain_eqns thy eqngr c =
  10.108 -  case try (Graph.get_node eqngr) c
  10.109 -   of SOME ((lhs, _), eqns) => ((lhs, []), [])
  10.110 -    | NONE => let
  10.111 -        val eqns = Code.these_eqns thy c
  10.112 -          |> burrow_fst (Code_Unit.norm_args thy)
  10.113 -          |> burrow_fst (Code_Unit.norm_varnames thy);
  10.114 -        val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns;
  10.115 -      in ((lhs, rhss), eqns) end;
  10.116 -
  10.117 -fun obtain_instance thy arities (inst as (class, tyco)) =
  10.118 -  case AList.lookup (op =) arities inst
  10.119 -   of SOME classess => (classess, ([], []))
  10.120 -    | NONE => let
  10.121 -        val all_classes = complete_proper_sort thy [class];
  10.122 -        val superclasses = remove (op =) class all_classes
  10.123 -        val classess = map (complete_proper_sort thy)
  10.124 -          (Sign.arity_sorts thy tyco [class]);
  10.125 -        val inst_params = inst_params thy tyco all_classes;
  10.126 -      in (classess, (superclasses, inst_params)) end;
  10.127 -
  10.128 -
  10.129 -(* computing instantiations *)
  10.130 -
  10.131 -fun add_classes thy arities eqngr c_k new_classes vardeps_data =
  10.132 -  let
  10.133 -    val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
  10.134 -    val diff_classes = new_classes |> subtract (op =) old_classes;
  10.135 -  in if null diff_classes then vardeps_data
  10.136 -  else let
  10.137 -    val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k;
  10.138 -  in
  10.139 -    vardeps_data
  10.140 -    |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
  10.141 -    |> fold (fn styp => fold (assert_typmatch_inst thy arities eqngr styp) new_classes) styps
  10.142 -    |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
  10.143 -  end end
  10.144 -and add_styp thy arities eqngr c_k tyco_styps vardeps_data =
  10.145 -  let
  10.146 -    val (old_styps, classes) = Vargraph.get_node (fst vardeps_data) c_k;
  10.147 -  in if member (op =) old_styps tyco_styps then vardeps_data
  10.148 -  else
  10.149 -    vardeps_data
  10.150 -    |> (apfst o Vargraph.map_node c_k o apfst) (cons tyco_styps)
  10.151 -    |> fold (assert_typmatch_inst thy arities eqngr tyco_styps) classes
  10.152 -  end
  10.153 -and add_dep thy arities eqngr c_k c_k' vardeps_data =
  10.154 -  let
  10.155 -    val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k;
  10.156 -  in
  10.157 -    vardeps_data
  10.158 -    |> add_classes thy arities eqngr c_k' classes
  10.159 -    |> apfst (Vargraph.add_edge (c_k, c_k'))
  10.160 -  end
  10.161 -and assert_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
  10.162 -  if can (Sign.arity_sorts thy tyco) [class]
  10.163 -  then vardeps_data
  10.164 -    |> assert_inst thy arities eqngr (class, tyco)
  10.165 -    |> fold_index (fn (k, styp) =>
  10.166 -         assert_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
  10.167 -  else vardeps_data (*permissive!*)
  10.168 -and assert_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
  10.169 -  if member (op =) insts inst then vardeps_data
  10.170 -  else let
  10.171 -    val (classess, (superclasses, inst_params)) =
  10.172 -      obtain_instance thy arities inst;
  10.173 -  in
  10.174 -    vardeps_data
  10.175 -    |> (apsnd o apsnd) (insert (op =) inst)
  10.176 -    |> fold_index (fn (k, _) =>
  10.177 -         apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess
  10.178 -    |> fold (fn superclass => assert_inst thy arities eqngr (superclass, tyco)) superclasses
  10.179 -    |> fold (assert_fun thy arities eqngr) inst_params
  10.180 -    |> fold_index (fn (k, classes) =>
  10.181 -         add_classes thy arities eqngr (Inst (class, tyco), k) classes
  10.182 -         #> fold (fn superclass =>
  10.183 -             add_dep thy arities eqngr (Inst (superclass, tyco), k)
  10.184 -             (Inst (class, tyco), k)) superclasses
  10.185 -         #> fold (fn inst_param =>
  10.186 -             add_dep thy arities eqngr (Fun inst_param, k)
  10.187 -             (Inst (class, tyco), k)
  10.188 -             ) inst_params
  10.189 -         ) classess
  10.190 -  end
  10.191 -and assert_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
  10.192 -      vardeps_data
  10.193 -      |> add_styp thy arities eqngr c_k tyco_styps
  10.194 -  | assert_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
  10.195 -      vardeps_data
  10.196 -      |> add_dep thy arities eqngr c_k c_k'
  10.197 -  | assert_typmatch thy arities eqngr Free c_k vardeps_data =
  10.198 -      vardeps_data
  10.199 -and assert_rhs thy arities eqngr (c', styps) vardeps_data =
  10.200 -  vardeps_data
  10.201 -  |> assert_fun thy arities eqngr c'
  10.202 -  |> fold_index (fn (k, styp) =>
  10.203 -       assert_typmatch thy arities eqngr styp (Fun c', k)) styps
  10.204 -and assert_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) =
  10.205 -  if Symtab.defined eqntab c then vardeps_data
  10.206 -  else let
  10.207 -    val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
  10.208 -    val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
  10.209 -  in
  10.210 -    vardeps_data
  10.211 -    |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
  10.212 -    |> fold_index (fn (k, _) =>
  10.213 -         apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs
  10.214 -    |> fold_index (fn (k, (_, sort)) =>
  10.215 -         add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
  10.216 -    |> fold (assert_rhs thy arities eqngr) rhss'
  10.217 -  end;
  10.218 -
  10.219 -
  10.220 -(* applying instantiations *)
  10.221 -
  10.222 -fun dicts_of thy (proj_sort, algebra) (T, sort) =
  10.223 -  let
  10.224 -    fun class_relation (x, _) _ = x;
  10.225 -    fun type_constructor tyco xs class =
  10.226 -      inst_params thy tyco (Sorts.complete_sort algebra [class])
  10.227 -        @ (maps o maps) fst xs;
  10.228 -    fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
  10.229 -  in
  10.230 -    flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
  10.231 -      { class_relation = class_relation, type_constructor = type_constructor,
  10.232 -        type_variable = type_variable } (T, proj_sort sort)
  10.233 -       handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
  10.234 -  end;
  10.235 -
  10.236 -fun add_arity thy vardeps (class, tyco) =
  10.237 -  AList.default (op =)
  10.238 -    ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
  10.239 -      (0 upto Sign.arity_number thy tyco - 1));
  10.240 -
  10.241 -fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
  10.242 -  if can (Graph.get_node eqngr) c then (rhss, eqngr)
  10.243 -  else let
  10.244 -    val lhs = map_index (fn (k, (v, _)) =>
  10.245 -      (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
  10.246 -    val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
  10.247 -      Vartab.update ((v, 0), sort)) lhs;
  10.248 -    val eqns = proto_eqns
  10.249 -      |> (map o apfst) (Code_Unit.inst_thm thy inst_tab);
  10.250 -    val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
  10.251 -    val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
  10.252 -  in (map (pair c) rhss' @ rhss, eqngr') end;
  10.253 -
  10.254 -fun extend_arities_eqngr thy cs ts (arities, eqngr) =
  10.255 -  let
  10.256 -    val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
  10.257 -      insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
  10.258 -    val (vardeps, (eqntab, insts)) = empty_vardeps_data
  10.259 -      |> fold (assert_fun thy arities eqngr) cs
  10.260 -      |> fold (assert_rhs thy arities eqngr) cs_rhss;
  10.261 -    val arities' = fold (add_arity thy vardeps) insts arities;
  10.262 -    val pp = Syntax.pp_global thy;
  10.263 -    val algebra = Sorts.subalgebra pp (is_proper_class thy)
  10.264 -      (AList.lookup (op =) arities') (Sign.classes_of thy);
  10.265 -    val (rhss, eqngr') = Symtab.fold (add_eqs thy vardeps) eqntab ([], eqngr);
  10.266 -    fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
  10.267 -      (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
  10.268 -    val eqngr'' = fold (fn (c, rhs) => fold
  10.269 -      (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
  10.270 -  in (algebra, (arities', eqngr'')) end;
  10.271 -
  10.272 -
  10.273 -(** store **)
  10.274 -
  10.275 -structure Wellsorted = CodeDataFun
  10.276 -(
  10.277 -  type T = ((string * class) * sort list) list * code_graph;
  10.278 -  val empty = ([], Graph.empty);
  10.279 -  fun purge thy cs (arities, eqngr) =
  10.280 -    let
  10.281 -      val del_cs = ((Graph.all_preds eqngr
  10.282 -        o filter (can (Graph.get_node eqngr))) cs);
  10.283 -      val del_arities = del_cs
  10.284 -        |> map_filter (AxClass.inst_of_param thy)
  10.285 -        |> maps (fn (c, tyco) =>
  10.286 -             (map (rpair tyco) o Sign.complete_sort thy o the_list
  10.287 -               o AxClass.class_of_param thy) c);
  10.288 -      val arities' = fold (AList.delete (op =)) del_arities arities;
  10.289 -      val eqngr' = Graph.del_nodes del_cs eqngr;
  10.290 -    in (arities', eqngr') end;
  10.291 -);
  10.292 -
  10.293 -
  10.294 -(** retrieval interfaces **)
  10.295 -
  10.296 -fun obtain thy cs ts = apsnd snd
  10.297 -  (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
  10.298 -
  10.299 -fun prepare_sorts_typ prep_sort
  10.300 -  = map_type_tfree (fn (v, sort) => TFree (v, prep_sort sort));
  10.301 -
  10.302 -fun prepare_sorts prep_sort (Const (c, ty)) =
  10.303 -      Const (c, prepare_sorts_typ prep_sort ty)
  10.304 -  | prepare_sorts prep_sort (t1 $ t2) =
  10.305 -      prepare_sorts prep_sort t1 $ prepare_sorts prep_sort t2
  10.306 -  | prepare_sorts prep_sort (Abs (v, ty, t)) =
  10.307 -      Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t)
  10.308 -  | prepare_sorts _ (t as Bound _) = t;
  10.309 -
  10.310 -fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct =
  10.311 -  let
  10.312 -    val pp = Syntax.pp_global thy;
  10.313 -    val ct = cterm_of proto_ct;
  10.314 -    val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp)
  10.315 -      (Thm.term_of ct);
  10.316 -    val thm = Code.preprocess_conv thy ct;
  10.317 -    val ct' = Thm.rhs_of thm;
  10.318 -    val t' = Thm.term_of ct';
  10.319 -    val vs = Term.add_tfrees t' [];
  10.320 -    val consts = fold_aterms
  10.321 -      (fn Const (c, _) => insert (op =) c | _ => I) t' [];
  10.322 - 
  10.323 -    val t'' = prepare_sorts prep_sort t';
  10.324 -    val (algebra', eqngr') = obtain thy consts [t''];
  10.325 -  in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end;
  10.326 -
  10.327 -fun simple_evaluator evaluator algebra eqngr vs t ct =
  10.328 -  evaluator algebra eqngr vs t;
  10.329 -
  10.330 -fun eval_conv thy =
  10.331 -  let
  10.332 -    fun conclude_evaluation thm2 thm1 =
  10.333 -      let
  10.334 -        val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
  10.335 -      in
  10.336 -        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
  10.337 -          error ("could not construct evaluation proof:\n"
  10.338 -          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
  10.339 -      end;
  10.340 -  in gen_eval thy I conclude_evaluation end;
  10.341 -
  10.342 -fun eval thy prep_sort postproc evaluator = gen_eval thy (Thm.cterm_of thy)
  10.343 -  (K o postproc (Code.postprocess_term thy)) prep_sort (simple_evaluator evaluator);
  10.344 -
  10.345 -end; (*struct*)