removed
authorhaftmann
Tue Sep 19 15:22:29 2006 +0200 (2006-09-19)
changeset 2060337dfd7af2746
parent 20602 96fa2cf465f5
child 20604 9dba9c7872c9
removed
src/HOL/ex/CodeOperationalEquality.thy
src/Pure/Tools/codegen_theorems.ML
     1.1 --- a/src/HOL/ex/CodeOperationalEquality.thy	Tue Sep 19 15:22:29 2006 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,167 +0,0 @@
     1.4 -(*  ID:         $Id$
     1.5 -    Author:     Florian Haftmann, TU Muenchen
     1.6 -*)
     1.7 -
     1.8 -header {* Operational equality for code generation *}
     1.9 -
    1.10 -theory CodeOperationalEquality
    1.11 -imports Main
    1.12 -begin
    1.13 -
    1.14 -section {* Operational equality for code generation *}
    1.15 -
    1.16 -subsection {* eq class *}
    1.17 -
    1.18 -class eq =
    1.19 -  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.20 -
    1.21 -defs
    1.22 -  eq_def: "eq x y == (x = y)"
    1.23 -
    1.24 -ML {*
    1.25 -local
    1.26 -  val thy = the_context ();
    1.27 -  val const_eq = Sign.intern_const thy "eq";
    1.28 -  val type_bool = Type (Sign.intern_type thy "bool", []);
    1.29 -in
    1.30 -  val eq_def_sym = Thm.symmetric (thm "eq_def");
    1.31 -  val class_eq = Sign.intern_class thy "eq";
    1.32 -end
    1.33 -*}
    1.34 -
    1.35 -
    1.36 -subsection {* preprocessor *}
    1.37 -
    1.38 -ML {*
    1.39 -fun constrain_op_eq thy thms =
    1.40 -  let
    1.41 -    fun add_eq (Const ("op =", ty)) =
    1.42 -          fold (insert (eq_fst (op = : indexname * indexname -> bool)))
    1.43 -            (Term.add_tvarsT ty [])
    1.44 -      | add_eq _ =
    1.45 -          I
    1.46 -    val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
    1.47 -    val instT = map (fn (v_i, sort) =>
    1.48 -      (Thm.ctyp_of thy (TVar (v_i, sort)),
    1.49 -         Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
    1.50 -  in
    1.51 -    thms
    1.52 -    |> map (Thm.instantiate (instT, []))
    1.53 -  end;
    1.54 -*}
    1.55 -
    1.56 -
    1.57 -subsection {* codetypes hook *}
    1.58 -
    1.59 -setup {*
    1.60 -let
    1.61 -  fun add_eq_instance specs =
    1.62 -    DatatypeCodegen.prove_codetypes_arities
    1.63 -      (K (ClassPackage.intro_classes_tac []))
    1.64 -      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    1.65 -      [class_eq] ((K o K o K) []);
    1.66 -  (* fun add_eq_thms dtco thy =
    1.67 -    let
    1.68 -      val thms =
    1.69 -        DatatypeCodegen.get_eq thy dtco
    1.70 -        |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
    1.71 -        |> constrain_op_eq thy
    1.72 -        |> map (Tactic.rewrite_rule [eq_def_sym])
    1.73 -    in fold CodegenTheorems.add_fun thms thy end; *)
    1.74 -  fun hook dtcos =
    1.75 -    add_eq_instance dtcos (* #> fold add_eq_thms dtcos *);
    1.76 -in
    1.77 -  DatatypeCodegen.add_codetypes_hook_bootstrap hook
    1.78 -end
    1.79 -*}
    1.80 -
    1.81 -
    1.82 -subsection {* extractor *}
    1.83 -
    1.84 -setup {*
    1.85 -let
    1.86 -  val lift_not_thm = thm "HOL.Eq_FalseI";
    1.87 -  val lift_thm = thm "HOL.eq_reflection";
    1.88 -  val eq_def_thm = Thm.symmetric (thm "eq_def");
    1.89 -  fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    1.90 -   of SOME _ => DatatypeCodegen.get_eq thy tyco
    1.91 -    | NONE => case TypedefCodegen.get_triv_typedef thy tyco
    1.92 -       of SOME (_ ,(_, thm)) => [thm]
    1.93 -        | NONE => [];
    1.94 -  fun get_eq_thms_eq thy ("CodeOperationalEquality.eq", ty) = (case strip_type ty
    1.95 -       of (Type (tyco, _) :: _, _) =>
    1.96 -             get_eq_thms thy tyco
    1.97 -             |> map (perhaps (try (fn thm => lift_not_thm OF [thm])))
    1.98 -             |> map (perhaps (try (fn thm => lift_thm OF [thm])))
    1.99 -             (*|> tap (writeln o cat_lines o map string_of_thm)*)
   1.100 -             |> constrain_op_eq thy
   1.101 -             (*|> tap (writeln o cat_lines o map string_of_thm)*)
   1.102 -             |> map (Tactic.rewrite_rule [eq_def_thm])
   1.103 -             (*|> tap (writeln o cat_lines o map string_of_thm)*)
   1.104 -        | _ => [])
   1.105 -    | get_eq_thms_eq _ _ = [];
   1.106 -in
   1.107 -  CodegenTheorems.add_fun_extr get_eq_thms_eq
   1.108 -end
   1.109 -*}
   1.110 -
   1.111 -
   1.112 -subsection {* integers *}
   1.113 -
   1.114 -definition
   1.115 -  "eq_integer (k\<Colon>int) l = (k = l)"
   1.116 -
   1.117 -instance int :: eq ..
   1.118 -
   1.119 -lemma [code func]:
   1.120 -  "eq k l = eq_integer k l"
   1.121 -unfolding eq_integer_def eq_def ..
   1.122 -
   1.123 -code_const eq_integer
   1.124 -  (SML infixl 6 "=")
   1.125 -  (Haskell infixl 4 "==")
   1.126 -
   1.127 -
   1.128 -subsection {* codegenerator setup *}
   1.129 -
   1.130 -setup {*
   1.131 -  CodegenTheorems.add_preproc constrain_op_eq
   1.132 -*}
   1.133 -
   1.134 -declare eq_def [symmetric, code inline]
   1.135 -
   1.136 -
   1.137 -subsection {* haskell setup *}
   1.138 -
   1.139 -code_class eq
   1.140 -  (Haskell "Eq" where eq \<equiv> "(==)")
   1.141 -
   1.142 -code_instance eq :: bool and eq :: unit and eq :: *
   1.143 -  and eq :: option and eq :: list and eq :: char and eq :: int
   1.144 -  (Haskell - and - and - and - and - and - and -)
   1.145 -
   1.146 -code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   1.147 -  (Haskell infixl 4 "==")
   1.148 -
   1.149 -code_const "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   1.150 -  (Haskell infixl 4 "==")
   1.151 -
   1.152 -code_const "eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   1.153 -  (Haskell infixl 4 "==")
   1.154 -
   1.155 -code_const "eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   1.156 -  (Haskell infixl 4 "==")
   1.157 -
   1.158 -code_const "eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
   1.159 -  (Haskell infixl 4 "==")
   1.160 -
   1.161 -code_const "eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   1.162 -  (Haskell infixl 4 "==")
   1.163 -
   1.164 -code_const "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   1.165 -  (Haskell infixl 4 "==")
   1.166 -
   1.167 -code_const "eq"
   1.168 -  (Haskell infixl 4 "==")
   1.169 -
   1.170 -end
   1.171 \ No newline at end of file
     2.1 --- a/src/Pure/Tools/codegen_theorems.ML	Tue Sep 19 15:22:29 2006 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,931 +0,0 @@
     2.4 -(*  Title:      Pure/Tools/codegen_theorems.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Florian Haftmann, TU Muenchen
     2.7 -
     2.8 -Theorems used for code generation.
     2.9 -*)
    2.10 -
    2.11 -signature CODEGEN_THEOREMS =
    2.12 -sig
    2.13 -  val add_notify: ((string * typ) list option -> theory -> theory) -> theory -> theory;
    2.14 -  val add_preproc: (theory -> thm list -> thm list) -> theory -> theory;
    2.15 -  val add_fun_extr: (theory -> string * typ -> thm list) -> theory -> theory;
    2.16 -  val add_datatype_extr: (theory -> string
    2.17 -    -> (((string * sort) list * (string * typ list) list) * tactic) option)
    2.18 -    -> theory -> theory;
    2.19 -  val add_fun: thm -> theory -> theory;
    2.20 -  val del_fun: thm -> theory -> theory;
    2.21 -  val add_unfold: thm -> theory -> theory;
    2.22 -  val del_unfold: thm -> theory -> theory;
    2.23 -  val purge_defs: string * typ -> theory -> theory;
    2.24 -  val notify_dirty: theory -> theory;
    2.25 -
    2.26 -  val extr_typ: theory -> thm -> typ;
    2.27 -  val rewrite_fun: thm list -> thm -> thm;
    2.28 -  val common_typ: theory -> (thm -> typ) -> thm list -> thm list;
    2.29 -  val preprocess: theory -> thm list -> thm list;
    2.30 -
    2.31 -  val prove_freeness: theory -> tactic -> string
    2.32 -    -> (string * sort) list * (string * typ list) list -> thm list;
    2.33 -
    2.34 -  type thmtab;
    2.35 -  val mk_thmtab: theory -> (string * typ) list -> thmtab;
    2.36 -  val get_dtyp_of_cons: thmtab -> string * typ -> string option;
    2.37 -  val get_dtyp_spec: thmtab -> string
    2.38 -    -> ((string * sort) list * (string * typ list) list) option;
    2.39 -  val get_fun_typs: thmtab -> ((string * typ list) * typ) list;
    2.40 -  val get_fun_thms: thmtab -> string * typ -> thm list;
    2.41 -
    2.42 -  val pretty_funtab: theory -> thm list CodegenConsts.Consttab.table -> Pretty.T;
    2.43 -  val print_thms: theory -> unit;
    2.44 -
    2.45 -  val init_obj: (thm * thm) * (thm * thm) -> theory -> theory;
    2.46 -  val debug: bool ref;
    2.47 -  val debug_msg: ('a -> string) -> 'a -> 'a;
    2.48 -end;
    2.49 -
    2.50 -structure CodegenTheorems: CODEGEN_THEOREMS =
    2.51 -struct
    2.52 -
    2.53 -(** preliminaries **)
    2.54 -
    2.55 -(* diagnostics *)
    2.56 -
    2.57 -val debug = ref false;
    2.58 -fun debug_msg f x = (if !debug then Output.tracing (f x) else (); x);
    2.59 -
    2.60 -
    2.61 -(* auxiliary *)
    2.62 -
    2.63 -fun getf_first [] _ = NONE
    2.64 -  | getf_first (f::fs) x = case f x
    2.65 -     of NONE => getf_first fs x
    2.66 -      | y as SOME x => y;
    2.67 -
    2.68 -fun getf_first_list [] x = []
    2.69 -  | getf_first_list (f::fs) x = case f x
    2.70 -     of [] => getf_first_list fs x
    2.71 -      | xs => xs;
    2.72 -
    2.73 -
    2.74 -(* object logic setup *)
    2.75 -
    2.76 -structure CodegenTheoremsSetup = TheoryDataFun
    2.77 -(struct
    2.78 -  val name = "Pure/codegen_theorems_setup";
    2.79 -  type T = ((string * thm) * ((string * string) * (string * string))) option;
    2.80 -  val empty = NONE;
    2.81 -  val copy = I;
    2.82 -  val extend = I;
    2.83 -  fun merge pp = merge_opt (eq_pair (eq_pair (op =) eq_thm)
    2.84 -    (eq_pair (eq_pair (op =) (op =)) (eq_pair (op =) (op =)))) : T * T -> T;
    2.85 -  fun print thy data = ();
    2.86 -end);
    2.87 -
    2.88 -val _ = Context.add_setup CodegenTheoremsSetup.init;
    2.89 -
    2.90 -fun init_obj ((TrueI, FalseE), (conjI, atomize_eq)) thy =
    2.91 -  case CodegenTheoremsSetup.get thy
    2.92 -   of SOME _ => error "Code generator already set up for object logic"
    2.93 -    | NONE =>
    2.94 -        let
    2.95 -          fun strip_implies t = (Logic.strip_imp_prems t, Logic.strip_imp_concl t);
    2.96 -          fun dest_TrueI thm =
    2.97 -            Drule.plain_prop_of thm
    2.98 -            |> ObjectLogic.drop_judgment thy
    2.99 -            |> Term.dest_Const
   2.100 -            |> apsnd (
   2.101 -                  Term.dest_Type
   2.102 -                  #> fst
   2.103 -              );
   2.104 -          fun dest_FalseE thm =
   2.105 -            Drule.plain_prop_of thm
   2.106 -            |> Logic.dest_implies
   2.107 -            |> apsnd (
   2.108 -                 ObjectLogic.drop_judgment thy
   2.109 -                 #> Term.dest_Var
   2.110 -               )
   2.111 -            |> fst
   2.112 -            |> ObjectLogic.drop_judgment thy
   2.113 -            |> Term.dest_Const
   2.114 -            |> fst;
   2.115 -          fun dest_conjI thm =
   2.116 -            Drule.plain_prop_of thm
   2.117 -            |> strip_implies
   2.118 -            |> apfst (map (ObjectLogic.drop_judgment thy #> Term.dest_Var))
   2.119 -            |> apsnd (
   2.120 -                 ObjectLogic.drop_judgment thy
   2.121 -                 #> Term.strip_comb
   2.122 -                 #> apsnd (map Term.dest_Var)
   2.123 -                 #> apfst Term.dest_Const
   2.124 -               )
   2.125 -            |> (fn (v1, ((conj, _), v2)) => if v1 = v2 then conj else error "Wrong premise")
   2.126 -          fun dest_atomize_eq thm=
   2.127 -            Drule.plain_prop_of thm
   2.128 -            |> Logic.dest_equals
   2.129 -            |> apfst (
   2.130 -                 ObjectLogic.drop_judgment thy
   2.131 -                 #> Term.strip_comb
   2.132 -                 #> apsnd (map Term.dest_Var)
   2.133 -                 #> apfst Term.dest_Const
   2.134 -               )
   2.135 -            |> apsnd (
   2.136 -                 Logic.dest_equals
   2.137 -                 #> apfst Term.dest_Var
   2.138 -                 #> apsnd Term.dest_Var
   2.139 -               )
   2.140 -            |> (fn (((eq, _), v2), (v1a as (_, TVar (_, sort)), v1b)) =>
   2.141 -                 if [v1a, v1b] = v2 andalso sort = Sign.defaultS thy then eq else error "Wrong premise")
   2.142 -        in
   2.143 -          ((dest_TrueI TrueI, [dest_FalseE FalseE, dest_conjI conjI, dest_atomize_eq atomize_eq])
   2.144 -          handle _ => error "Bad code generator setup")
   2.145 -          |> (fn ((tr, b), [fl, con, eq]) => CodegenTheoremsSetup.put
   2.146 -               (SOME ((b, atomize_eq), ((tr, fl), (con, eq)))) thy)
   2.147 -        end;
   2.148 -
   2.149 -fun get_obj thy =
   2.150 -  case CodegenTheoremsSetup.get thy
   2.151 -   of SOME ((b, atomize), x) => ((Type (b, []), atomize) ,x)
   2.152 -    | NONE => error "No object logic setup for code theorems";
   2.153 -
   2.154 -fun mk_true thy =
   2.155 -  let
   2.156 -    val ((b, _), ((tr, fl), (con, eq))) = get_obj thy;
   2.157 -  in Const (tr, b) end;
   2.158 -
   2.159 -fun mk_false thy =
   2.160 -  let
   2.161 -    val ((b, _), ((tr, fl), (con, eq))) = get_obj thy;
   2.162 -  in Const (fl, b) end;
   2.163 -
   2.164 -fun mk_obj_conj thy (x, y) =
   2.165 -  let
   2.166 -    val ((b, _), ((tr, fl), (con, eq))) = get_obj thy;
   2.167 -  in Const (con, b --> b --> b) $ x $ y end;
   2.168 -
   2.169 -fun mk_obj_eq thy (x, y) =
   2.170 -  let
   2.171 -    val ((b, _), ((tr, fl), (con, eq))) = get_obj thy;
   2.172 -  in Const (eq, fastype_of x --> fastype_of y --> b) $ x $ y end;
   2.173 -
   2.174 -fun is_obj_eq thy c =
   2.175 -  let
   2.176 -    val ((b, _), ((tr, fl), (con, eq))) = get_obj thy;
   2.177 -  in c = eq end;
   2.178 -
   2.179 -fun mk_func thy ((x, y), rhs) =
   2.180 -  Logic.mk_equals (
   2.181 -    (mk_obj_eq thy (x, y)),
   2.182 -    rhs
   2.183 -  );
   2.184 -
   2.185 -
   2.186 -(* theorem purification *)
   2.187 -
   2.188 -fun err_thm msg thm =
   2.189 -  error (msg ^ ": " ^ string_of_thm thm);
   2.190 -
   2.191 -val mk_rule =
   2.192 -  #mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of;
   2.193 -
   2.194 -fun abs_norm thy thm =
   2.195 -  let
   2.196 -    fun expvars t =
   2.197 -      let
   2.198 -        val lhs = (fst o Logic.dest_equals) t;
   2.199 -        val tys = (fst o strip_type o fastype_of) lhs;
   2.200 -        val used = fold_aterms (fn Var ((v, _), _) => insert (op =) v | _ => I) lhs [];
   2.201 -        val vs = Name.invent_list used "x" (length tys);
   2.202 -      in
   2.203 -        map2 (fn v => fn ty => Var ((v, 0), ty)) vs tys
   2.204 -      end;
   2.205 -    fun expand ct thm =
   2.206 -      Thm.combination thm (Thm.reflexive ct);
   2.207 -    fun beta_norm thm =
   2.208 -      thm
   2.209 -      |> prop_of
   2.210 -      |> Logic.dest_equals
   2.211 -      |> fst
   2.212 -      |> cterm_of thy
   2.213 -      |> Thm.beta_conversion true
   2.214 -      |> Thm.symmetric
   2.215 -      |> (fn thm' => Thm.transitive thm' thm);
   2.216 -  in
   2.217 -    thm
   2.218 -    |> fold (expand o cterm_of thy) ((expvars o prop_of) thm)
   2.219 -    |> beta_norm
   2.220 -  end;
   2.221 -
   2.222 -fun canonical_tvars thy thm =
   2.223 -  let
   2.224 -    fun mk_inst (v_i as (v, i), (v', sort)) (s as (maxidx, set, acc)) =
   2.225 -      if v = v' orelse member (op =) set v then s
   2.226 -        else let
   2.227 -          val ty = TVar (v_i, sort)
   2.228 -        in
   2.229 -          (maxidx + 1, v :: set,
   2.230 -            (ctyp_of thy ty, ctyp_of thy (TVar ((v', maxidx), sort))) :: acc)
   2.231 -        end;
   2.232 -    fun tvars_of thm = (fold_types o fold_atyps)
   2.233 -      (fn TVar (v_i as (v, i), sort) => cons (v_i, (CodegenNames.purify_var v, sort))
   2.234 -        | _ => I) (prop_of thm) [];
   2.235 -    val maxidx = Thm.maxidx_of thm + 1;
   2.236 -    val (_, _, inst) = fold mk_inst (tvars_of thm) (maxidx + 1, [], []);
   2.237 -  in Thm.instantiate (inst, []) thm end;
   2.238 -
   2.239 -fun canonical_vars thy thm =
   2.240 -  let
   2.241 -    fun mk_inst (v_i as (v, i), (v', ty)) (s as (maxidx, set, acc)) =
   2.242 -      if v = v' orelse member (op =) set v then s
   2.243 -        else let
   2.244 -          val t = if i = ~1 then Free (v, ty) else Var (v_i, ty)
   2.245 -        in
   2.246 -          (maxidx + 1,  v :: set,
   2.247 -            (cterm_of thy t, cterm_of thy (Var ((v', maxidx), ty))) :: acc)
   2.248 -        end;
   2.249 -    fun vars_of thm = fold_aterms
   2.250 -      (fn Var (v_i as (v, i), ty) => cons (v_i, (CodegenNames.purify_var v, ty))
   2.251 -        | _ => I) (prop_of thm) [];
   2.252 -    val maxidx = Thm.maxidx_of thm + 1;
   2.253 -    val (_, _, inst) = fold mk_inst (vars_of thm) (maxidx + 1, [], []);
   2.254 -  in Thm.instantiate ([], inst) thm end;
   2.255 -
   2.256 -fun drop_redundant thy eqs =
   2.257 -  let
   2.258 -    val matches = curry (Pattern.matches thy o
   2.259 -      pairself (fst o Logic.dest_equals o prop_of))
   2.260 -    fun drop eqs [] = eqs
   2.261 -      | drop eqs (eq::eqs') =
   2.262 -          drop (eq::eqs) (filter_out (matches eq) eqs')
   2.263 -  in drop [] eqs end;
   2.264 -
   2.265 -fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
   2.266 -  o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
   2.267 -
   2.268 -fun make_eq thy =
   2.269 -  let
   2.270 -    val ((_, atomize), _) = get_obj thy;
   2.271 -  in rewrite_rule [atomize] end;
   2.272 -
   2.273 -fun dest_eq thy thm =
   2.274 -  case try (make_eq thy #> Drule.plain_prop_of
   2.275 -   #> ObjectLogic.drop_judgment thy #> Logic.dest_equals) thm
   2.276 -   of SOME eq => (eq, thm)
   2.277 -    | NONE => err_thm "Not an equation" thm;
   2.278 -
   2.279 -fun dest_fun thy thm =
   2.280 -  let
   2.281 -    fun dest_fun' ((lhs, _), thm) =
   2.282 -      case try (dest_Const o fst o strip_comb) lhs
   2.283 -       of SOME (c, ty) => (c, (ty, thm))
   2.284 -        | NONE => err_thm "Not a function equation" thm;
   2.285 -  in
   2.286 -    thm
   2.287 -    |> dest_eq thy
   2.288 -    |> dest_fun'
   2.289 -  end;
   2.290 -
   2.291 -
   2.292 -
   2.293 -(** theory data **)
   2.294 -
   2.295 -(* data structures *)
   2.296 -
   2.297 -structure Consttab = CodegenConsts.Consttab;
   2.298 -
   2.299 -fun merge' eq (xys as (xs, ys)) =
   2.300 -  if eq_list eq (xs, ys) then (false, xs) else (true, merge eq xys);
   2.301 -
   2.302 -fun alist_merge' eq_key eq (xys as (xs, ys)) =
   2.303 -  if eq_list (eq_pair eq_key eq) (xs, ys) then (false, xs) else (true, AList.merge eq_key eq xys);
   2.304 -
   2.305 -fun list_consttab_join' eq (xyt as (xt, yt)) =
   2.306 -  let
   2.307 -    val xc = Consttab.keys xt;
   2.308 -    val yc = Consttab.keys yt;
   2.309 -    val zc = filter (member CodegenConsts.eq_const yc) xc;
   2.310 -    val wc = subtract (op =) zc xc @ subtract (op =) zc yc;
   2.311 -    fun same_thms c = if eq_list eq_thm ((the o Consttab.lookup xt) c, (the o Consttab.lookup yt) c)
   2.312 -      then NONE else SOME c;
   2.313 -  in (wc @ map_filter same_thms zc, Consttab.join (K (merge eq)) xyt) end;
   2.314 -
   2.315 -datatype notify = Notify of (serial * ((string * typ) list option -> theory -> theory)) list;
   2.316 -
   2.317 -val mk_notify = Notify;
   2.318 -fun map_notify f (Notify notify) = mk_notify (f notify);
   2.319 -fun merge_notify pp (Notify notify1, Notify notify2) =
   2.320 -  mk_notify (AList.merge (op =) (K true) (notify1, notify2));
   2.321 -
   2.322 -datatype preproc = Preproc of {
   2.323 -  preprocs: (serial * (theory -> thm list -> thm list)) list,
   2.324 -  unfolds: thm list
   2.325 -};
   2.326 -
   2.327 -fun mk_preproc (preprocs, unfolds) =
   2.328 -  Preproc { preprocs = preprocs, unfolds = unfolds };
   2.329 -fun map_preproc f (Preproc { preprocs, unfolds }) =
   2.330 -  mk_preproc (f (preprocs, unfolds));
   2.331 -fun merge_preproc _ (Preproc { preprocs = preprocs1, unfolds = unfolds1 },
   2.332 -  Preproc { preprocs = preprocs2, unfolds = unfolds2 }) =
   2.333 -    let
   2.334 -      val (dirty1, preprocs) = alist_merge' (op =) (K true) (preprocs1, preprocs2);
   2.335 -      val (dirty2, unfolds) = merge' eq_thm (unfolds1, unfolds2);
   2.336 -    in (dirty1 orelse dirty2, mk_preproc (preprocs, unfolds)) end;
   2.337 -
   2.338 -datatype extrs = Extrs of {
   2.339 -  funs: (serial * (theory -> string * typ -> thm list)) list,
   2.340 -  datatypes: (serial * (theory -> string -> (((string * sort) list * (string * typ list) list) * tactic) option)) list
   2.341 -};
   2.342 -
   2.343 -fun mk_extrs (funs, datatypes) =
   2.344 -  Extrs { funs = funs, datatypes = datatypes };
   2.345 -fun map_extrs f (Extrs { funs, datatypes }) =
   2.346 -  mk_extrs (f (funs, datatypes));
   2.347 -fun merge_extrs _ (Extrs { funs = funs1, datatypes = datatypes1 },
   2.348 -  Extrs { funs = funs2, datatypes = datatypes2 }) =
   2.349 -    let
   2.350 -      val (dirty1, funs) = alist_merge' (op =) (K true) (funs1, funs2);
   2.351 -      val (dirty2, datatypes) = alist_merge' (op =) (K true) (datatypes1, datatypes2);
   2.352 -    in (dirty1 orelse dirty2, mk_extrs (funs, datatypes)) end;
   2.353 -
   2.354 -datatype funthms = Funthms of {
   2.355 -  dirty: string list,
   2.356 -  funs: thm list Consttab.table
   2.357 -};
   2.358 -
   2.359 -fun mk_funthms (dirty, funs) =
   2.360 -  Funthms { dirty = dirty, funs = funs };
   2.361 -fun map_funthms f (Funthms { dirty, funs }) =
   2.362 -  mk_funthms (f (dirty, funs));
   2.363 -fun merge_funthms _ (Funthms { dirty = dirty1, funs = funs1 },
   2.364 -  Funthms { dirty = dirty2, funs = funs2 }) =
   2.365 -    let
   2.366 -      val (dirty3, funs) = list_consttab_join' eq_thm (funs1, funs2);
   2.367 -    in mk_funthms (merge (op =) (merge (op =) (dirty1, dirty2), map fst dirty3), funs) end;
   2.368 -
   2.369 -datatype T = T of {
   2.370 -  dirty: bool,
   2.371 -  notify: notify,
   2.372 -  preproc: preproc,
   2.373 -  extrs: extrs,
   2.374 -  funthms: funthms
   2.375 -};
   2.376 -
   2.377 -fun mk_T ((dirty, notify), (preproc, (extrs, funthms))) =
   2.378 -  T { dirty = dirty, notify = notify, preproc= preproc, extrs = extrs, funthms = funthms };
   2.379 -fun map_T f (T { dirty, notify, preproc, extrs, funthms }) =
   2.380 -  mk_T (f ((dirty, notify), (preproc, (extrs, funthms))));
   2.381 -fun merge_T pp (T { dirty = dirty1, notify = notify1, preproc = preproc1, extrs = extrs1, funthms = funthms1 },
   2.382 -  T { dirty = dirty2, notify = notify2, preproc = preproc2, extrs = extrs2, funthms = funthms2 }) =
   2.383 -    let
   2.384 -      val (dirty3, preproc) = merge_preproc pp (preproc1, preproc2);
   2.385 -      val (dirty4, extrs) = merge_extrs pp (extrs1, extrs2);
   2.386 -    in
   2.387 -      mk_T ((dirty1 orelse dirty2 orelse dirty3 orelse dirty4, merge_notify pp (notify1, notify2)),
   2.388 -        (preproc, (extrs, merge_funthms pp (funthms1, funthms2))))
   2.389 -    end;
   2.390 -
   2.391 -
   2.392 -(* setup *)
   2.393 -
   2.394 -structure CodegenTheoremsData = TheoryDataFun
   2.395 -(struct
   2.396 -  val name = "Pure/codegen_theorems_data";
   2.397 -  type T = T;
   2.398 -  val empty = mk_T ((false, mk_notify []), (mk_preproc ([], []),
   2.399 -    (mk_extrs ([], []), mk_funthms ([], Consttab.empty))));
   2.400 -  val copy = I;
   2.401 -  val extend = I;
   2.402 -  val merge = merge_T;
   2.403 -  fun print (thy : theory) (data : T) =
   2.404 -    let
   2.405 -      val pretty_thm = ProofContext.pretty_thm (ProofContext.init thy);
   2.406 -      val funthms = (fn T { funthms, ... } => funthms) data;
   2.407 -      val funs = (Consttab.dest o (fn Funthms { funs, ... } => funs)) funthms;
   2.408 -      val preproc = (fn T { preproc, ... } => preproc) data;
   2.409 -      val unfolds = (fn Preproc { unfolds, ... } => unfolds) preproc;
   2.410 -    in
   2.411 -      (Pretty.writeln o Pretty.block o Pretty.fbreaks) ([
   2.412 -        Pretty.str "code generation theorems:",
   2.413 -        Pretty.str "function theorems:" ] @
   2.414 -          map (fn (c, thms) =>
   2.415 -            (Pretty.block o Pretty.fbreaks) (
   2.416 -              (Pretty.str o CodegenConsts.string_of_const thy) c  :: map pretty_thm (rev thms)
   2.417 -            )
   2.418 -          ) funs @ [
   2.419 -        Pretty.block (
   2.420 -          Pretty.str "inlined theorems:"
   2.421 -          :: Pretty.fbrk
   2.422 -          :: (Pretty.fbreaks o map pretty_thm) unfolds
   2.423 -      )])
   2.424 -    end;
   2.425 -end);
   2.426 -
   2.427 -val _ = Context.add_setup CodegenTheoremsData.init;
   2.428 -val print_thms = CodegenTheoremsData.print;
   2.429 -
   2.430 -
   2.431 -(* accessors *)
   2.432 -
   2.433 -local
   2.434 -  val the_preproc = (fn T { preproc = Preproc preproc, ... } => preproc) o CodegenTheoremsData.get;
   2.435 -  val the_extrs = (fn T { extrs = Extrs extrs, ... } => extrs) o CodegenTheoremsData.get;
   2.436 -  val the_funthms = (fn T { funthms = Funthms funthms, ... } => funthms) o CodegenTheoremsData.get;
   2.437 -in
   2.438 -  val is_dirty = (fn T { dirty = dirty, ... } => dirty) o CodegenTheoremsData.get;
   2.439 -  val the_dirty_consts = (fn { dirty = dirty, ... } => dirty) o the_funthms;
   2.440 -  val the_notify = (fn T { notify = Notify notify, ... } => map snd notify) o CodegenTheoremsData.get;
   2.441 -  val the_preprocs = (fn { preprocs, ... } => map snd preprocs) o the_preproc;
   2.442 -  val the_unfolds = (fn { unfolds, ... } => unfolds) o the_preproc;
   2.443 -  val the_funs_extrs = (fn { funs, ... } => map snd funs) o the_extrs;
   2.444 -  val the_datatypes_extrs = (fn { datatypes, ... } => map snd datatypes) o the_extrs;
   2.445 -  val the_funs = (fn { funs, ... } => funs) o the_funthms;
   2.446 -end (*local*);
   2.447 -
   2.448 -val map_data = CodegenTheoremsData.map o map_T;
   2.449 -
   2.450 -(* notifiers *)
   2.451 -
   2.452 -fun all_typs thy c =
   2.453 -  let
   2.454 -    val c_tys = (map (pair c o #lhs o snd) o Defs.specifications_of (Theory.defs_of thy)) c;
   2.455 -  in (c, Sign.the_const_type thy c) :: map (CodegenConsts.typ_of_typinst thy) c_tys end;
   2.456 -
   2.457 -fun add_notify f =
   2.458 -  map_data (fn ((dirty, notify), x) =>
   2.459 -    ((dirty, notify |> map_notify (cons (serial (), f))), x));
   2.460 -
   2.461 -fun get_reset_dirty thy =
   2.462 -  let
   2.463 -    val dirty = is_dirty thy;
   2.464 -    val dirty_const = if dirty then [] else the_dirty_consts thy;
   2.465 -  in
   2.466 -    thy
   2.467 -    |> map_data (fn ((_, notify), (procs, (extrs, funthms))) =>
   2.468 -         ((false, notify), (procs, (extrs, funthms |> map_funthms (fn (_, funs) => ([], funs))))))
   2.469 -    |> pair (dirty, dirty_const)
   2.470 -  end;
   2.471 -
   2.472 -fun notify_all c thy =
   2.473 -  thy
   2.474 -  |> get_reset_dirty
   2.475 -  |-> (fn (true, _) => fold (fn f => f NONE) (the_notify thy)
   2.476 -        | (false, cs) => let val cs' = case c of NONE => cs | SOME c => insert (op =) c cs
   2.477 -            in fold (fn f => f (SOME (maps (all_typs thy) cs'))) (the_notify thy) end);
   2.478 -
   2.479 -fun notify_dirty thy =
   2.480 -  thy
   2.481 -  |> get_reset_dirty
   2.482 -  |-> (fn (true, _) => fold (fn f => f NONE) (the_notify thy)
   2.483 -        | (false, cs) => fold (fn f => f (SOME (maps (all_typs thy) cs))) (the_notify thy));
   2.484 -
   2.485 -
   2.486 -(* modifiers *)
   2.487 -
   2.488 -fun add_preproc f =
   2.489 -  map_data (fn (x, (preproc, y)) =>
   2.490 -    (x, (preproc |> map_preproc (fn (preprocs, unfolds) => ((serial (), f) :: preprocs, unfolds)), y)))
   2.491 -  #> notify_all NONE;
   2.492 -
   2.493 -fun add_fun_extr f =
   2.494 -  map_data (fn (x, (preproc, (extrs, funthms))) =>
   2.495 -    (x, (preproc, (extrs |> map_extrs (fn (funs, datatypes) =>
   2.496 -      ((serial (), f) :: funs, datatypes)), funthms))))
   2.497 -  #> notify_all NONE;
   2.498 -
   2.499 -fun add_datatype_extr f =
   2.500 -  map_data (fn (x, (preproc, (extrs, funthms))) =>
   2.501 -    (x, (preproc, (extrs |> map_extrs (fn (funs, datatypes) =>
   2.502 -      (funs, (serial (), f) :: datatypes)), funthms))))
   2.503 -  #> notify_all NONE;
   2.504 -
   2.505 -fun add_fun thm thy =
   2.506 -  case dest_fun thy thm
   2.507 -   of (c, (ty, _)) =>
   2.508 -    thy
   2.509 -    |> map_data (fn (x, (preproc, (extrs, funthms))) =>
   2.510 -        (x, (preproc, (extrs, funthms |> map_funthms (fn (dirty, funs) =>
   2.511 -          (dirty, funs |> Consttab.map_default (CodegenConsts.norminst_of_typ thy (c, ty), []) (cons thm)))))))
   2.512 -    |> notify_all (SOME c);
   2.513 -
   2.514 -fun del_fun thm thy =
   2.515 -  case dest_fun thy thm
   2.516 -   of (c, (ty, _)) =>
   2.517 -    thy
   2.518 -    |> map_data (fn (x, (preproc, (extrs, funthms))) =>
   2.519 -        (x, (preproc, (extrs, funthms |> map_funthms (fn (dirty, funs) =>
   2.520 -          (dirty, funs |> Consttab.map_entry (CodegenConsts.norminst_of_typ thy (c, ty)) (remove eq_thm thm)))))))
   2.521 -    |> notify_all (SOME c);
   2.522 -
   2.523 -fun add_unfold thm thy =
   2.524 -  thy
   2.525 -  |> tap (fn thy => dest_eq thy thm)
   2.526 -  |> map_data (fn (x, (preproc, y)) =>
   2.527 -       (x, (preproc |> map_preproc (fn (preprocs, unfolds) =>
   2.528 -         (preprocs, thm :: unfolds)), y)))
   2.529 -  |> notify_all NONE;
   2.530 -
   2.531 -fun del_unfold thm =
   2.532 -  map_data (fn (x, (preproc, y)) =>
   2.533 -       (x, (preproc |> map_preproc (fn (preprocs, unfolds) =>
   2.534 -         (preprocs, remove eq_thm thm unfolds)), y)))
   2.535 -  #> notify_all NONE;
   2.536 -
   2.537 -fun purge_defs (c, ty) thy =
   2.538 -  thy
   2.539 -  |> map_data (fn (x, (preproc, (extrs, funthms))) =>
   2.540 -      (x, (preproc, (extrs, funthms |> map_funthms (fn (dirty, funs) =>
   2.541 -        (dirty, funs |> Consttab.update (CodegenConsts.norminst_of_typ thy (c, ty), [])))))))
   2.542 -  |> notify_all (SOME c);
   2.543 -
   2.544 -
   2.545 -
   2.546 -(** theorem handling **)
   2.547 -
   2.548 -(* preprocessing *)
   2.549 -
   2.550 -fun extr_typ thy thm = case dest_fun thy thm
   2.551 - of (_, (ty, _)) => ty;
   2.552 -
   2.553 -fun rewrite_fun rewrites thm =
   2.554 -  let
   2.555 -    val rewrite = Tactic.rewrite true rewrites;
   2.556 -    val (ct_eq, [ct_lhs, ct_rhs]) = (Drule.strip_comb o cprop_of) thm;
   2.557 -    val Const ("==", _) = term_of ct_eq;
   2.558 -    val (ct_f, ct_args) = Drule.strip_comb ct_lhs;
   2.559 -    val rhs' = rewrite ct_rhs;
   2.560 -    val args' = map rewrite ct_args;
   2.561 -    val lhs' = Thm.symmetric (fold (fn th1 => fn th2 => Thm.combination th2 th1)
   2.562 -      args' (Thm.reflexive ct_f));
   2.563 -  in
   2.564 -    Thm.transitive (Thm.transitive lhs' thm) rhs'
   2.565 -  end handle Bind => raise ERROR "rewrite_fun"
   2.566 -
   2.567 -fun common_typ thy _ [] = []
   2.568 -  | common_typ thy _ [thm] = [thm]
   2.569 -  | common_typ thy extract_typ thms =
   2.570 -      let
   2.571 -        fun incr_thm thm max =
   2.572 -          let
   2.573 -            val thm' = incr_indexes max thm;
   2.574 -            val max' = (maxidx_of_typ o fastype_of o Drule.plain_prop_of) thm' + 1;
   2.575 -          in (thm', max') end;
   2.576 -        val (thms', maxidx) = fold_map incr_thm thms 0;
   2.577 -        val (ty1::tys) = map extract_typ thms;
   2.578 -        fun unify ty env = Sign.typ_unify thy (ty1, ty) env
   2.579 -          handle Type.TUNIFY =>
   2.580 -            error ("Type unificaton failed, while unifying function equations\n"
   2.581 -            ^ (cat_lines o map Display.string_of_thm) thms
   2.582 -            ^ "\nwith types\n"
   2.583 -            ^ (cat_lines o map (Sign.string_of_typ thy)) (ty1 :: tys));
   2.584 -        val (env, _) = fold unify tys (Vartab.empty, maxidx)
   2.585 -        val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
   2.586 -          cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
   2.587 -      in map (Thm.instantiate (instT, [])) thms end;
   2.588 -
   2.589 -fun preprocess thy thms =
   2.590 -  let
   2.591 -    fun burrow_thms f [] = []
   2.592 -      | burrow_thms f thms =
   2.593 -          thms
   2.594 -          |> Conjunction.intr_list
   2.595 -          |> f
   2.596 -          |> Conjunction.elim_list;
   2.597 -    fun cmp_thms (thm1, thm2) =
   2.598 -      not (Sign.typ_instance thy (extr_typ thy thm1, extr_typ thy thm2));
   2.599 -    fun unvarify thms =
   2.600 -      #2 (#1 (Variable.import true thms (ProofContext.init thy)));
   2.601 -    val unfold_thms = map (make_eq thy) (the_unfolds thy);
   2.602 -  in
   2.603 -    thms
   2.604 -    |> map (make_eq thy)
   2.605 -    |> map (Thm.transfer thy)
   2.606 -    |> fold (fn f => f thy) (the_preprocs thy)
   2.607 -    |> map (rewrite_fun unfold_thms)
   2.608 -    |> debug_msg (fn _ => "[cg_thm] sorting")
   2.609 -    |> debug_msg (commas o map string_of_thm)
   2.610 -    |> sort (make_ord cmp_thms)
   2.611 -    |> debug_msg (fn _ => "[cg_thm] common_typ")
   2.612 -    |> debug_msg (commas o map string_of_thm)
   2.613 -    |> common_typ thy (extr_typ thy)
   2.614 -    |> debug_msg (fn _ => "[cg_thm] abs_norm")
   2.615 -    |> debug_msg (commas o map string_of_thm)
   2.616 -    |> map (abs_norm thy)
   2.617 -    |> drop_refl thy
   2.618 -    |> burrow_thms (
   2.619 -        debug_msg (fn _ => "[cg_thm] canonical tvars")
   2.620 -        #> debug_msg (string_of_thm)
   2.621 -        #> canonical_tvars thy
   2.622 -        #> debug_msg (fn _ => "[cg_thm] canonical vars")
   2.623 -        #> debug_msg (string_of_thm)
   2.624 -        #> canonical_vars thy
   2.625 -        #> debug_msg (fn _ => "[cg_thm] zero indices")
   2.626 -        #> debug_msg (string_of_thm)
   2.627 -        #> Drule.zero_var_indexes
   2.628 -       )
   2.629 -    |> drop_redundant thy
   2.630 -    |> debug_msg (fn _ => "[cg_thm] preprocessing done")
   2.631 -  end;
   2.632 -
   2.633 -
   2.634 -(* retrieval *)
   2.635 -
   2.636 -fun get_funs thy (c, ty) =
   2.637 -  let
   2.638 -    val _ = debug_msg (fn _ => "[cg_thm] const (1) " ^ c ^ " :: " ^ Sign.string_of_typ thy ty) ()
   2.639 -    val postprocess_typ = case AxClass.class_of_param thy c
   2.640 -     of NONE => map_filter (fn (_, (ty', thm)) =>
   2.641 -          if Sign.typ_instance thy (ty, ty')
   2.642 -          then SOME thm else debug_msg (fn _ => "[cg_thm] dropping " ^ string_of_thm thm) NONE)
   2.643 -      | SOME _ => let
   2.644 -          (*FIXME make this more elegant*)
   2.645 -          val ty' = CodegenConsts.typ_of_classop thy (CodegenConsts.norminst_of_typ thy (c, ty));
   2.646 -          val ct = Thm.cterm_of thy (Const (c, ty'));
   2.647 -          val thm' = Thm.reflexive ct;
   2.648 -        in map (snd o snd) #> cons thm' #> common_typ thy (extr_typ thy) #> tl end;
   2.649 -    fun get_funs (c, ty) =
   2.650 -      (these o Consttab.lookup (the_funs thy) o CodegenConsts.norminst_of_typ thy) (c, ty)
   2.651 -      |> debug_msg (fn _ => "[cg_thm] trying funs")
   2.652 -      |> map (dest_fun thy)
   2.653 -      |> postprocess_typ;
   2.654 -    fun get_extr (c, ty) =
   2.655 -      getf_first_list (map (fn f => f thy) (the_funs_extrs thy)) (c, ty)
   2.656 -      |> debug_msg (fn _ => "[cg_thm] trying extr")
   2.657 -      |> map (dest_fun thy)
   2.658 -      |> postprocess_typ;
   2.659 -    fun get_spec (c, ty) =
   2.660 -      (CodegenConsts.find_def thy o CodegenConsts.norminst_of_typ thy) (c, ty)
   2.661 -      |> debug_msg (fn _ => "[cg_thm] trying spec")
   2.662 -      |> Option.mapPartial (fn ((_, name), _) => try (Thm.get_axiom_i thy) name)
   2.663 -      |> the_list
   2.664 -      |> map_filter (try (dest_fun thy))
   2.665 -      |> postprocess_typ;
   2.666 -  in
   2.667 -    getf_first_list [get_funs, get_extr, get_spec] (c, ty)
   2.668 -    |> debug_msg (fn _ => "[cg_thm] const (2) " ^ c ^ " :: " ^ Sign.string_of_typ thy ty)
   2.669 -    |> preprocess thy
   2.670 -  end;
   2.671 -
   2.672 -fun prove_freeness thy tac dtco vs_cos =
   2.673 -  let
   2.674 -    val truh = mk_true thy;
   2.675 -    val fals = mk_false thy;
   2.676 -    fun mk_lhs vs ((co1, tys1), (co2, tys2)) =
   2.677 -      let
   2.678 -        val dty = Type (dtco, map TFree vs);
   2.679 -        val (xs1, xs2) = chop (length tys1) (Name.invent_list [] "a" (length tys1 + length tys2));
   2.680 -        val frees1 = map2 (fn x => fn ty => Free (x, ty)) xs1 tys1;
   2.681 -        val frees2 = map2 (fn x => fn ty => Free (x, ty)) xs2 tys2;
   2.682 -        fun zip_co co xs tys = list_comb (Const (co,
   2.683 -          tys ---> dty), map2 (fn x => fn ty => Free (x, ty)) xs tys);
   2.684 -      in
   2.685 -        ((frees1, frees2), (zip_co co1 xs1 tys1, zip_co co2 xs2 tys2))
   2.686 -      end;
   2.687 -    fun mk_rhs [] [] = truh
   2.688 -      | mk_rhs xs ys = foldr1 (mk_obj_conj thy) (map2 (curry (mk_obj_eq thy)) xs ys);
   2.689 -    fun mk_eq vs (args as ((co1, _), (co2, _))) (inj, dist) =
   2.690 -      if co1 = co2
   2.691 -        then let
   2.692 -          val ((fs1, fs2), lhs) = mk_lhs vs args;
   2.693 -          val rhs = mk_rhs fs1 fs2;
   2.694 -        in (mk_func thy (lhs, rhs) :: inj, dist) end
   2.695 -        else let
   2.696 -          val (_, lhs) = mk_lhs vs args;
   2.697 -        in (inj, mk_func thy (lhs, fals) :: dist) end;
   2.698 -    fun mk_eqs (vs, cos) =
   2.699 -      let val cos' = rev cos
   2.700 -      in (op @) (fold (mk_eq vs) (product cos' cos') ([], [])) end;
   2.701 -    val ts = (map (ObjectLogic.ensure_propT thy) o mk_eqs) vs_cos;
   2.702 -    fun prove t = if !quick_and_dirty then SkipProof.make_thm thy (Logic.varify t)
   2.703 -      else Goal.prove_global thy [] [] t (K tac);
   2.704 -  in map prove ts end;
   2.705 -
   2.706 -fun get_datatypes thy dtco =
   2.707 -  let
   2.708 -    val _ = debug_msg (fn _ => "[cg_thm] datatype " ^ dtco) ()
   2.709 -  in
   2.710 -    case getf_first (map (fn f => f thy) (the_datatypes_extrs thy)) dtco
   2.711 -     of NONE => NONE
   2.712 -      | SOME (vs_cos, tac) => SOME (vs_cos, prove_freeness thy tac dtco vs_cos)
   2.713 -  end;
   2.714 -
   2.715 -fun get_eq thy (c, ty) =
   2.716 -  if is_obj_eq thy c
   2.717 -  then case strip_type ty
   2.718 -   of (Type (tyco, _) :: _, _) =>
   2.719 -     (case get_datatypes thy tyco
   2.720 -       of SOME (_, thms) => thms
   2.721 -        | _ => [])
   2.722 -    | _ => []
   2.723 -  else [];
   2.724 -
   2.725 -fun check_thms c thms =
   2.726 -  let
   2.727 -    fun check_head_lhs thm (lhs, rhs) =
   2.728 -      case strip_comb lhs
   2.729 -       of (Const (c', _), _) => if c' = c then ()
   2.730 -           else error ("Illegal function equation for " ^ quote c
   2.731 -             ^ ", actually defining " ^ quote c' ^ ": " ^ Display.string_of_thm thm)
   2.732 -        | _ => error ("Illegal function equation: " ^ Display.string_of_thm thm);
   2.733 -    fun check_vars_lhs thm (lhs, rhs) =
   2.734 -      if has_duplicates (op =)
   2.735 -          (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs [])
   2.736 -      then error ("Repeated variables on left hand side of function equation:"
   2.737 -        ^ Display.string_of_thm thm)
   2.738 -      else ();
   2.739 -    fun check_vars_rhs thm (lhs, rhs) =
   2.740 -      if null (subtract (op =)
   2.741 -        (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs [])
   2.742 -        (fold_aterms (fn Free (v, _) => cons v | _ => I) rhs []))
   2.743 -      then ()
   2.744 -      else error ("Free variables on right hand side of function equation:"
   2.745 -        ^ Display.string_of_thm thm)
   2.746 -    val tts = map (Logic.dest_equals o Logic.unvarify o Thm.prop_of) thms;
   2.747 -  in
   2.748 -    (map2 check_head_lhs thms tts; map2 check_vars_lhs thms tts;
   2.749 -      map2 check_vars_rhs thms tts; thms)
   2.750 -  end;
   2.751 -
   2.752 -structure Consttab = CodegenConsts.Consttab;
   2.753 -type thmtab = (theory * (thm list Consttab.table
   2.754 -  * string Consttab.table)
   2.755 -  * ((string * sort) list * (string * typ list) list) Symtab.table);
   2.756 -
   2.757 -fun thmtab_empty thy = (thy, (Consttab.empty, Consttab.empty),
   2.758 -  Symtab.empty);
   2.759 -
   2.760 -fun get_dtyp_of_cons (thy, (_, dtcotab), _) =
   2.761 -  Consttab.lookup dtcotab o CodegenConsts.norminst_of_typ thy;
   2.762 -
   2.763 -fun get_dtyp_spec (_, _, dttab) =
   2.764 -  Symtab.lookup dttab;
   2.765 -
   2.766 -fun has_fun_thms (thy, (funtab, _), _) =
   2.767 -  is_some o Consttab.lookup funtab o CodegenConsts.norminst_of_typ thy;
   2.768 -
   2.769 -fun get_fun_thms (thy, (funtab, _), _) (c_ty as (c, _)) =
   2.770 -  (check_thms c o these o Consttab.lookup funtab
   2.771 -    o CodegenConsts.norminst_of_typ thy) c_ty;
   2.772 -
   2.773 -fun get_fun_typs (thy, (funtab, dtcotab), _) =
   2.774 -  (Consttab.dest funtab
   2.775 -  |> map (fn (c, thm :: _) => (c, extr_typ thy thm)
   2.776 -           | (c as (name, _), []) => (c, case AxClass.class_of_param thy name
   2.777 -         of SOME class => (case ClassPackage.the_consts_sign thy class of (v, cs) =>
   2.778 -              (Logic.varifyT o map_type_tfree (fn u as (w, _) =>
   2.779 -                if w = v then TFree (v, [class]) else TFree u))
   2.780 -              ((the o AList.lookup (op =) cs) name))
   2.781 -          | NONE => Sign.the_const_type thy name)))
   2.782 -  @ (Consttab.keys dtcotab
   2.783 -  |> AList.make (Sign.const_instance thy));
   2.784 -
   2.785 -fun pretty_funtab thy funtab =
   2.786 -  funtab
   2.787 -  |> CodegenConsts.Consttab.dest
   2.788 -  |> map (fn (c, thms) =>
   2.789 -       (Pretty.block o Pretty.fbreaks) (
   2.790 -         (Pretty.str o CodegenConsts.string_of_const thy) c
   2.791 -         :: map Display.pretty_thm thms
   2.792 -       ))
   2.793 -  |> Pretty.chunks;
   2.794 -
   2.795 -fun constrain_funtab thy funtab =
   2.796 -  let
   2.797 -    fun max k [] = k
   2.798 -      | max k (l::ls) = max (if k < l then l else k) ls;
   2.799 -    fun mk_consttyps funtab =
   2.800 -      CodegenConsts.Consttab.empty
   2.801 -      |> CodegenConsts.Consttab.fold (fn (c, thm :: _) =>
   2.802 -           CodegenConsts.Consttab.update_new (c, extr_typ thy thm) | (_, []) => I) funtab
   2.803 -    fun mk_typescheme_of typtab (c, ty) =
   2.804 -      CodegenConsts.Consttab.lookup typtab (CodegenConsts.norminst_of_typ thy (c, ty));
   2.805 -    fun incr_indices (c, thms) maxidx =
   2.806 -      let
   2.807 -        val thms' = map (Thm.incr_indexes maxidx) thms;
   2.808 -        val maxidx' = Int.max
   2.809 -          (maxidx, max ~1 (map Thm.maxidx_of thms') + 1);
   2.810 -      in (thms', maxidx') end;
   2.811 -    fun consts_of_eqs thms =
   2.812 -      let
   2.813 -        fun terms_of_eq thm =
   2.814 -          let
   2.815 -            val (lhs, rhs) = (Logic.dest_equals o Drule.plain_prop_of) thm
   2.816 -          in rhs :: (snd o strip_comb) lhs end;
   2.817 -      in (fold o fold_aterms) (fn Const c => insert (eq_pair (op =) (Type.eq_type Vartab.empty)) c | _ => I)
   2.818 -        (maps terms_of_eq thms) []
   2.819 -      end;
   2.820 -    val typscheme_of =
   2.821 -      mk_typescheme_of (mk_consttyps funtab);
   2.822 -    val tsig = Sign.tsig_of thy;
   2.823 -    fun unify_const (c, ty) (env, maxidx) =
   2.824 -      case typscheme_of (c, ty)
   2.825 -       of SOME ty_decl => let
   2.826 -            (*val _ = writeln "UNIFY";
   2.827 -            val _ = writeln (CodegenConsts.string_of_const_typ thy (c, ty))*)
   2.828 -            val ty_decl' = Logic.incr_tvar maxidx ty_decl;
   2.829 -            (*val _ = writeln "WITH";
   2.830 -            val _ = writeln (CodegenConsts.string_of_const_typ thy (c, ty_decl'))*)
   2.831 -            val maxidx' = Int.max (Term.maxidx_of_typ ty_decl' + 1, maxidx);
   2.832 -            (*val _ = writeln ("  " ^ string_of_int maxidx ^ " +> " ^ string_of_int maxidx');*)
   2.833 -          in Type.unify tsig (ty_decl', ty) (env, maxidx') end
   2.834 -        | NONE => (env, maxidx);
   2.835 -    fun apply_unifier unif [] = []
   2.836 -      | apply_unifier unif (thms as thm :: _) =
   2.837 -          let
   2.838 -            val ty = extr_typ thy thm;
   2.839 -            val ty' = Envir.norm_type unif ty;
   2.840 -            val env = Type.typ_match (Sign.tsig_of thy) (ty, ty') Vartab.empty;
   2.841 -            val inst = Thm.instantiate (Vartab.fold (fn (x_i, (sort, ty)) =>
   2.842 -              cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [], []);
   2.843 -          in map (Drule.zero_var_indexes o inst) thms end;
   2.844 -(*     val _ = writeln "(1)";  *)
   2.845 -(*     val _ = (Pretty.writeln o pretty_funtab thy) funtab;  *)
   2.846 -    val (funtab', maxidx) =
   2.847 -      CodegenConsts.Consttab.fold_map incr_indices funtab 0;
   2.848 -(*     val _ = writeln "(2)";
   2.849 - *     val _ = (Pretty.writeln o pretty_funtab thy) funtab';
   2.850 - *)
   2.851 -    val (unif, _) =
   2.852 -      CodegenConsts.Consttab.fold (fold unify_const o consts_of_eqs o snd)
   2.853 -        funtab' (Vartab.empty, maxidx);
   2.854 -(*     val _ = writeln "(3)";  *)
   2.855 -    val funtab'' =
   2.856 -      CodegenConsts.Consttab.map (apply_unifier unif) funtab';
   2.857 -(*     val _ = writeln "(4)";
   2.858 - *     val _ = (Pretty.writeln o pretty_funtab thy) funtab'';
   2.859 - *)
   2.860 -  in funtab'' end;
   2.861 -
   2.862 -fun mk_thmtab thy cs =
   2.863 -  let
   2.864 -    fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys
   2.865 -      | add_tycos _ = I;
   2.866 -    fun consts_of ts =
   2.867 -      Consttab.empty
   2.868 -      |> (fold o fold_aterms)
   2.869 -           (fn Const c_ty => Consttab.update (CodegenConsts.norminst_of_typ thy c_ty, ())
   2.870 -             | _ => I) ts
   2.871 -      |> Consttab.keys;
   2.872 -    fun add_dtyps_of_type ty thmtab =
   2.873 -      let
   2.874 -        val tycos = add_tycos ty [];
   2.875 -        val tycos_new = filter (is_none o get_dtyp_spec thmtab) tycos;
   2.876 -        fun add_dtyp_spec dtco (dtyp_spec as (vs, cs)) ((thy, (funtab, dtcotab), dttab)) =
   2.877 -          let
   2.878 -            fun mk_co (c, tys) =
   2.879 -              CodegenConsts.norminst_of_typ thy (c, Logic.varifyT (tys ---> Type (dtco, map TFree vs)));
   2.880 -          in
   2.881 -            (thy, (funtab, dtcotab |> fold (fn c_tys =>
   2.882 -              Consttab.update_new (mk_co c_tys, dtco)) cs),
   2.883 -              dttab |> Symtab.update_new (dtco, dtyp_spec))
   2.884 -          end;
   2.885 -      in
   2.886 -        thmtab
   2.887 -        |> fold (fn tyco => case get_datatypes thy tyco
   2.888 -             of SOME (dtyp_spec, _) => add_dtyp_spec tyco dtyp_spec
   2.889 -              | NONE => I) tycos_new
   2.890 -      end;
   2.891 -    fun known thmtab (c, ty) =
   2.892 -      is_some (get_dtyp_of_cons thmtab (c, ty)) orelse has_fun_thms thmtab (c, ty);
   2.893 -    fun add_funthms (c, ty) (thmtab as (thy, (funtab, dtcotab), algebra_dttab))=
   2.894 -      if known thmtab (c, ty) then thmtab
   2.895 -      else let
   2.896 -        val thms = get_funs thy (c, ty)
   2.897 -        val cs_dep = (consts_of o map Thm.prop_of) thms;
   2.898 -      in
   2.899 -        (thy, (funtab |> Consttab.update_new (CodegenConsts.norminst_of_typ thy (c, ty), thms)
   2.900 -        , dtcotab), algebra_dttab)
   2.901 -        |> fold add_c cs_dep
   2.902 -      end
   2.903 -    and add_c (c_tys as (c, tys)) thmtab =
   2.904 -      thmtab
   2.905 -      |> add_dtyps_of_type (snd (CodegenConsts.typ_of_typinst thy c_tys))
   2.906 -      |> fold (add_funthms o CodegenConsts.typ_of_typinst thy)
   2.907 -           (CodegenConsts.insts_of_classop thy c_tys);
   2.908 -  in
   2.909 -    thmtab_empty thy
   2.910 -    |> fold (add_c o CodegenConsts.norminst_of_typ thy) cs
   2.911 -    |> (fn (a, (funtab, b), c) => (a, (funtab |> constrain_funtab thy, b), c))
   2.912 -  end;
   2.913 -
   2.914 -
   2.915 -
   2.916 -(** code attributes and setup **)
   2.917 -
   2.918 -local
   2.919 -  fun add_simple_attribute (name, f) =
   2.920 -    (Codegen.add_attribute name o (Scan.succeed o Thm.declaration_attribute))
   2.921 -      (Context.map_theory o f);
   2.922 -in
   2.923 -  val _ = map (Context.add_setup o add_simple_attribute) [
   2.924 -    ("func", add_fun),
   2.925 -    ("nofun", del_fun),
   2.926 -    ("unfold", (fn thm => Codegen.add_unfold thm #> add_unfold thm)),
   2.927 -    ("inline", add_unfold),
   2.928 -    ("noinline", del_unfold)
   2.929 -  ]
   2.930 -end; (*local*)
   2.931 -
   2.932 -val _ = Context.add_setup (add_fun_extr get_eq);
   2.933 -
   2.934 -end; (*struct*)