code certificates as integral part of code generation
authorhaftmann
Tue Jan 12 16:27:42 2010 +0100 (2010-01-12)
changeset 3489199b9a6290446
parent 34877 ded5b770ec1c
child 34892 6144d233b99a
code certificates as integral part of code generation
src/HOL/Tools/recfun_codegen.ML
src/Pure/Isar/code.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Jan 12 09:59:45 2010 +0100
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Jan 12 16:27:42 2010 +0100
     1.3 @@ -43,8 +43,10 @@
     1.4  fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
     1.5    let
     1.6      val c = AxClass.unoverload_const thy (raw_c, T);
     1.7 -    val raw_thms = Code.these_eqns thy c
     1.8 +    val raw_thms = Code.get_cert thy I c
     1.9 +      |> Code.eqns_of_cert thy
    1.10        |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    1.11 +      |> map (AxClass.overload thy)
    1.12        |> filter (is_instance T o snd o const_of o prop_of);
    1.13      val module_name = case Symtab.lookup (ModuleData.get thy) c
    1.14       of SOME module_name => module_name
     2.1 --- a/src/Pure/Isar/code.ML	Tue Jan 12 09:59:45 2010 +0100
     2.2 +++ b/src/Pure/Isar/code.ML	Tue Jan 12 16:27:42 2010 +0100
     2.3 @@ -28,17 +28,13 @@
     2.4    val mk_eqn_warning: theory -> thm -> (thm * bool) option
     2.5    val mk_eqn_liberal: theory -> thm -> (thm * bool) option
     2.6    val assert_eqn: theory -> thm * bool -> thm * bool
     2.7 -  val assert_eqns_const: theory -> string
     2.8 -    -> (thm * bool) list -> (thm * bool) list
     2.9    val const_typ_eqn: theory -> thm -> string * typ
    2.10 -  val typscheme_eqn: theory -> thm -> (string * sort) list * typ
    2.11 -  val typscheme_eqns: theory -> string -> thm list -> (string * sort) list * typ
    2.12 -  val standard_typscheme: theory -> thm list -> thm list
    2.13    type cert = thm * bool list
    2.14 -  val cert_of_eqns: theory -> (thm * bool) list -> cert
    2.15 +  val empty_cert: theory -> string -> cert
    2.16 +  val cert_of_eqns: theory -> string -> (thm * bool) list -> cert
    2.17    val constrain_cert: theory -> sort list -> cert -> cert
    2.18 -  val dest_cert: theory -> cert -> (string * ((string * sort) list * typ)) * ((term list * term) * bool) list
    2.19    val eqns_of_cert: theory -> cert -> (thm * bool) list
    2.20 +  val dest_cert: theory -> cert -> ((string * sort) list * typ) * ((term list * term) * (thm * bool)) list
    2.21  
    2.22    (*executable code*)
    2.23    val add_type: string -> theory -> theory
    2.24 @@ -61,8 +57,7 @@
    2.25    val add_undefined: string -> theory -> theory
    2.26    val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
    2.27    val get_datatype_of_constr: theory -> string -> string option
    2.28 -  val these_eqns: theory -> string -> (thm * bool) list
    2.29 -  val eqn_cert: theory -> string -> cert
    2.30 +  val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
    2.31    val get_case_scheme: theory -> string -> (int * (int * string list)) option
    2.32    val undefineds: theory -> string list
    2.33    val print_codesetup: theory -> unit
    2.34 @@ -531,20 +526,6 @@
    2.35  
    2.36  fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
    2.37  
    2.38 -fun typscheme_eqn thy = typscheme thy o apsnd Logic.unvarifyT o const_typ_eqn thy;
    2.39 -
    2.40 -fun typscheme_eqns thy c [] = 
    2.41 -      let
    2.42 -        val raw_ty = const_typ thy c;
    2.43 -        val tvars = Term.add_tvar_namesT raw_ty [];
    2.44 -        val tvars' = case AxClass.class_of_param thy c
    2.45 -         of SOME class => [TFree (Name.aT, [class])]
    2.46 -          | NONE => Name.invent_list [] Name.aT (length tvars)
    2.47 -              |> map (fn v => TFree (v, []));
    2.48 -        val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
    2.49 -      in logical_typscheme thy (c, ty) end
    2.50 -  | typscheme_eqns thy c (thm :: _) = typscheme_eqn thy thm;
    2.51 -
    2.52  fun assert_eqns_const thy c eqns =
    2.53    let
    2.54      fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
    2.55 @@ -555,93 +536,97 @@
    2.56  
    2.57  (* code equation certificates *)
    2.58  
    2.59 -fun standard_typscheme thy thms =
    2.60 -  let
    2.61 -    fun tvars_of T = rev (Term.add_tvarsT T []);
    2.62 -    val vss = map (tvars_of o snd o head_eqn) thms;
    2.63 -    fun inter_sorts vs =
    2.64 -      fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
    2.65 -    val sorts = map_transpose inter_sorts vss;
    2.66 -    val vts = Name.names Name.context Name.aT sorts
    2.67 -      |> map (fn (v, sort) => TVar ((v, 0), sort));
    2.68 -  in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
    2.69 -
    2.70  type cert = thm * bool list;
    2.71  
    2.72 -fun cert_of_eqns thy [] = (Drule.dummy_thm, [])
    2.73 -  | cert_of_eqns thy eqns = 
    2.74 +fun mk_head_cterm thy (c, ty) =
    2.75 +  Thm.cterm_of thy (Logic.mk_equals (Free ("HEAD", ty), Const (c, ty)));
    2.76 +
    2.77 +fun empty_cert thy c = 
    2.78 +  let
    2.79 +    val raw_ty = const_typ thy c;
    2.80 +    val tvars = Term.add_tvar_namesT raw_ty [];
    2.81 +    val tvars' = case AxClass.class_of_param thy c
    2.82 +     of SOME class => [TFree (Name.aT, [class])]
    2.83 +      | NONE => Name.invent_list [] Name.aT (length tvars)
    2.84 +          |> map (fn v => TFree (v, []));
    2.85 +    val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
    2.86 +    val chead = mk_head_cterm thy (c, ty);
    2.87 +  in (Thm.weaken chead Drule.dummy_thm, []) end;
    2.88 +
    2.89 +fun cert_of_eqns thy c [] = empty_cert thy c
    2.90 +  | cert_of_eqns thy c eqns = 
    2.91        let
    2.92 -        val propers = map snd eqns;
    2.93 -        val thms as thm :: _ = (map Thm.freezeT o standard_typscheme thy o map fst) eqns; (*FIXME*)
    2.94 -        val (c, ty) = head_eqn thm;
    2.95 -        val head_thm = Thm.assume (Thm.cterm_of thy (Logic.mk_equals
    2.96 -          (Free ("HEAD", ty), Const (c, ty)))) |> Thm.symmetric;
    2.97 +        val _ = assert_eqns_const thy c eqns;
    2.98 +        val (thms, propers) = split_list eqns;
    2.99 +        fun tvars_of T = rev (Term.add_tvarsT T []);
   2.100 +        val vss = map (tvars_of o snd o head_eqn) thms;
   2.101 +        fun inter_sorts vs =
   2.102 +          fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
   2.103 +        val sorts = map_transpose inter_sorts vss;
   2.104 +        val vts = Name.names Name.context Name.aT sorts;
   2.105 +        val thms as thm :: _ =
   2.106 +          map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
   2.107 +        val head_thm = Thm.symmetric (Thm.assume (mk_head_cterm thy (head_eqn (hd thms))));
   2.108          fun head_conv ct = if can Thm.dest_comb ct
   2.109            then Conv.fun_conv head_conv ct
   2.110            else Conv.rewr_conv head_thm ct;
   2.111          val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv);
   2.112 -        val cert = Conjunction.intr_balanced (map rewrite_head thms);
   2.113 -      in (cert, propers) end;
   2.114 +        val cert_thm = Conjunction.intr_balanced (map rewrite_head thms);
   2.115 +      in (cert_thm, propers) end;
   2.116  
   2.117 -fun head_cert thy cert =
   2.118 +fun head_cert thy cert_thm =
   2.119 +  let
   2.120 +    val [head] = Thm.hyps_of cert_thm;
   2.121 +    val (Free (h, _), Const (c, ty)) = Logic.dest_equals head;
   2.122 +  in ((c, typscheme thy (c, ty)), (head, h)) end;
   2.123 +
   2.124 +fun constrain_cert thy sorts (cert_thm, propers) =
   2.125    let
   2.126 -    val [head] = Thm.hyps_of cert;
   2.127 -    val (Free (h, _), Const (c, ty)) = (Logic.dest_equals o the_single o Thm.hyps_of) cert;
   2.128 -  in ((c, typscheme thy (AxClass.unoverload_const thy (c, ty), ty)), (head, h)) end;
   2.129 +    val ((c, (vs, _)), (head, _)) = head_cert thy cert_thm;
   2.130 +    val subst = map2 (fn (v, _) => fn sort => (v, sort)) vs sorts;
   2.131 +    val head' = (map_types o map_atyps)
   2.132 +      (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) subst v))) head;
   2.133 +    val inst = (map2 (fn (v, sort) => fn sort' =>
   2.134 +      pairself (Thm.ctyp_of thy) (TVar ((v, 0), sort), TFree (v, sort'))) vs sorts, []);
   2.135 +    val cert_thm' = cert_thm
   2.136 +      |> Thm.implies_intr (Thm.cterm_of thy head)
   2.137 +      |> Thm.varifyT
   2.138 +      |> Thm.instantiate inst
   2.139 +      |> Thm.elim_implies (Thm.assume (Thm.cterm_of thy head'));
   2.140 +  in (cert_thm', propers) end;
   2.141  
   2.142 -fun constrain_cert thy sorts (cert, []) = (cert, [])
   2.143 -  | constrain_cert thy sorts (cert, propers) =
   2.144 +fun eqns_of_cert thy (cert_thm, []) = []
   2.145 +  | eqns_of_cert thy (cert_thm, propers) =
   2.146        let
   2.147 -        val ((c, (vs, _)), (head, _)) = head_cert thy cert;
   2.148 -        val subst = map2 (fn (v, _) => fn sort => (v, sort)) vs sorts;
   2.149 -        val head' = (map_types o map_atyps)
   2.150 -          (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) subst v))) head;
   2.151 -        val inst = (map2 (fn (v, sort) => fn sort' =>
   2.152 -          pairself (Thm.ctyp_of thy) (TVar ((v, 0), sort), TFree (v, sort'))) vs sorts ,[]);
   2.153 -        val cert' = cert
   2.154 -          |> Thm.implies_intr (Thm.cterm_of thy head)
   2.155 -          |> Thm.varifyT
   2.156 -          |> Thm.instantiate inst
   2.157 -          |> Thm.elim_implies (Thm.assume (Thm.cterm_of thy head'))
   2.158 -      in (cert', propers) end;
   2.159 -
   2.160 -fun dest_cert thy (cert, propers) =
   2.161 -  let
   2.162 -    val (c_vs_ty, (head, h)) = head_cert thy cert;
   2.163 -    val equations = cert
   2.164 -      |> Thm.prop_of
   2.165 -      |> Logic.dest_conjunction_balanced (length propers)
   2.166 -      |> map Logic.dest_equals
   2.167 -      |> (map o apfst) strip_comb
   2.168 -      |> (map o apfst) (fn (Free (h', _), ts) => case h = h' of True => ts)
   2.169 -  in (c_vs_ty, equations ~~ propers) end;
   2.170 -
   2.171 -fun eqns_of_cert thy (cert, []) = []
   2.172 -  | eqns_of_cert thy (cert, propers) =
   2.173 -      let
   2.174 -        val (_, (head, _)) = head_cert thy cert;
   2.175 -        val thms = cert
   2.176 +        val (_, (head, _)) = head_cert thy cert_thm;
   2.177 +        val thms = cert_thm
   2.178            |> LocalDefs.expand [Thm.cterm_of thy head]
   2.179            |> Thm.varifyT
   2.180            |> Conjunction.elim_balanced (length propers)
   2.181        in thms ~~ propers end;
   2.182  
   2.183 +fun dest_cert thy (cert as (cert_thm, propers)) =
   2.184 +  let
   2.185 +    val eqns = eqns_of_cert thy cert;
   2.186 +    val ((_, vs_ty), _) = head_cert thy cert_thm;
   2.187 +    val equations = if null propers then [] else cert_thm
   2.188 +      |> Thm.prop_of
   2.189 +      |> Logic.dest_conjunction_balanced (length propers)
   2.190 +      |> map Logic.dest_equals
   2.191 +      |> (map o apfst) (snd o strip_comb)
   2.192 +  in (vs_ty, equations ~~ eqns) end;
   2.193 +
   2.194  
   2.195  (* code equation access *)
   2.196  
   2.197 -fun these_eqns thy c =
   2.198 +fun get_cert thy f c =
   2.199    Symtab.lookup ((the_eqns o the_exec) thy) c
   2.200    |> Option.map (snd o snd o fst)
   2.201    |> these
   2.202    |> (map o apfst) (Thm.transfer thy)
   2.203 -  |> burrow_fst (standard_typscheme thy);
   2.204 -
   2.205 -fun eqn_cert thy c =
   2.206 -  Symtab.lookup ((the_eqns o the_exec) thy) c
   2.207 -  |> Option.map (snd o snd o fst)
   2.208 -  |> these
   2.209 -  |> (map o apfst) (Thm.transfer thy)
   2.210 -  |> cert_of_eqns thy;
   2.211 +  |> f
   2.212 +  |> (map o apfst) (AxClass.unoverload thy)
   2.213 +  |> cert_of_eqns thy c;
   2.214  
   2.215  
   2.216  (* cases *)
     3.1 --- a/src/Tools/Code/code_preproc.ML	Tue Jan 12 09:59:45 2010 +0100
     3.2 +++ b/src/Tools/Code/code_preproc.ML	Tue Jan 12 16:27:42 2010 +0100
     3.3 @@ -18,7 +18,7 @@
     3.4  
     3.5    type code_algebra
     3.6    type code_graph
     3.7 -  val eqns: code_graph -> string -> (thm * bool) list
     3.8 +  val cert: code_graph -> string -> Code.cert
     3.9    val sortargs: code_graph -> string -> sort list
    3.10    val all: code_graph -> string list
    3.11    val pretty: theory -> code_graph -> Pretty.T
    3.12 @@ -53,8 +53,8 @@
    3.13      let
    3.14        val pre = Simplifier.merge_ss (pre1, pre2);
    3.15        val post = Simplifier.merge_ss (post1, post2);
    3.16 -      val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
    3.17 -        (* FIXME handle AList.DUP (!?) *)
    3.18 +      val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2)
    3.19 +        handle AList.DUP => error ("Duplicate function transformer");
    3.20      in make_thmproc ((pre, post), functrans) end;
    3.21  
    3.22  structure Code_Preproc_Data = Theory_Data
    3.23 @@ -102,23 +102,14 @@
    3.24  
    3.25  (* post- and preprocessing *)
    3.26  
    3.27 -fun apply_functrans thy c _ [] = []
    3.28 -  | apply_functrans thy c [] eqns = eqns
    3.29 -  | apply_functrans thy c functrans eqns = eqns
    3.30 -      |> perhaps (perhaps_loop (perhaps_apply functrans))
    3.31 -      |> Code.assert_eqns_const thy c
    3.32 -      (*FIXME in future, the check here should be more accurate wrt. type schemes
    3.33 -      -- perhaps by means of upcoming code certificates with a corresponding
    3.34 -         preprocessor protocol*);
    3.35 -
    3.36  fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
    3.37  
    3.38 -fun eqn_conv conv =
    3.39 +fun eqn_conv conv ct =
    3.40    let
    3.41      fun lhs_conv ct = if can Thm.dest_comb ct
    3.42        then Conv.combination_conv lhs_conv conv ct
    3.43        else Conv.all_conv ct;
    3.44 -  in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end;
    3.45 +  in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end;
    3.46  
    3.47  val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
    3.48  
    3.49 @@ -129,17 +120,15 @@
    3.50    #> Logic.dest_equals
    3.51    #> snd;
    3.52  
    3.53 -fun preprocess thy c eqns =
    3.54 +fun preprocess thy eqns =
    3.55    let
    3.56      val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
    3.57      val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
    3.58        o the_thmproc) thy;
    3.59    in
    3.60      eqns
    3.61 -    |> apply_functrans thy c functrans
    3.62 +    |> perhaps (perhaps_loop (perhaps_apply functrans))
    3.63      |> (map o apfst) (rewrite_eqn pre)
    3.64 -    |> (map o apfst) (AxClass.unoverload thy)
    3.65 -    |> map (Code.assert_eqn thy)
    3.66    end;
    3.67  
    3.68  fun preprocess_conv thy ct =
    3.69 @@ -196,20 +185,20 @@
    3.70  (** sort algebra and code equation graph types **)
    3.71  
    3.72  type code_algebra = (sort -> sort) * Sorts.algebra;
    3.73 -type code_graph = ((string * sort) list * (thm * bool) list) Graph.T;
    3.74 +type code_graph = ((string * sort) list * Code.cert) Graph.T;
    3.75  
    3.76 -fun eqns eqngr = these o Option.map snd o try (Graph.get_node eqngr);
    3.77 -fun sortargs eqngr = map snd o fst o Graph.get_node eqngr
    3.78 +fun cert eqngr = snd o Graph.get_node eqngr;
    3.79 +fun sortargs eqngr = map snd o fst o Graph.get_node eqngr;
    3.80  fun all eqngr = Graph.keys eqngr;
    3.81  
    3.82  fun pretty thy eqngr =
    3.83    AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
    3.84    |> (map o apfst) (Code.string_of_const thy)
    3.85    |> sort (string_ord o pairself fst)
    3.86 -  |> map (fn (s, thms) =>
    3.87 +  |> map (fn (s, cert) =>
    3.88         (Pretty.block o Pretty.fbreaks) (
    3.89           Pretty.str s
    3.90 -         :: map (Display.pretty_thm_global thy o fst) thms
    3.91 +         :: map (Display.pretty_thm_global thy o AxClass.overload thy o fst) (Code.eqns_of_cert thy cert)
    3.92         ))
    3.93    |> Pretty.chunks;
    3.94  
    3.95 @@ -227,12 +216,12 @@
    3.96    map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
    3.97      o maps (#params o AxClass.get_info thy);
    3.98  
    3.99 -fun typscheme_rhss thy c eqns =
   3.100 +fun typscheme_rhss thy c cert =
   3.101    let
   3.102 -    val tyscm = Code.typscheme_eqns thy c (map fst eqns);
   3.103 +    val (tyscm, equations) = Code.dest_cert thy cert;
   3.104      val rhss = [] |> (fold o fold o fold_aterms)
   3.105 -      (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
   3.106 -        (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
   3.107 +      (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, ty)) | _ => I)
   3.108 +        (map (op :: o swap o fst) equations);
   3.109    in (tyscm, rhss) end;
   3.110  
   3.111  
   3.112 @@ -259,7 +248,7 @@
   3.113        | NONE => Free;
   3.114  
   3.115  type vardeps_data = ((string * styp list) list * class list) Vargraph.T
   3.116 -  * (((string * sort) list * (thm * bool) list) Symtab.table
   3.117 +  * (((string * sort) list * Code.cert) Symtab.table
   3.118      * (class * string) list);
   3.119  
   3.120  val empty_vardeps_data : vardeps_data =
   3.121 @@ -270,12 +259,11 @@
   3.122  
   3.123  fun obtain_eqns thy eqngr c =
   3.124    case try (Graph.get_node eqngr) c
   3.125 -   of SOME (lhs, eqns) => ((lhs, []), [])
   3.126 +   of SOME (lhs, cert) => ((lhs, []), cert)
   3.127      | NONE => let
   3.128 -        val eqns = Code.these_eqns thy c
   3.129 -          |> preprocess thy c;
   3.130 -        val ((lhs, _), rhss) = typscheme_rhss thy c eqns;
   3.131 -      in ((lhs, rhss), eqns) end;
   3.132 +        val cert = Code.get_cert thy (preprocess thy) c;
   3.133 +        val ((lhs, _), rhss) = typscheme_rhss thy c cert;
   3.134 +      in ((lhs, rhss), cert) end;
   3.135  
   3.136  fun obtain_instance thy arities (inst as (class, tyco)) =
   3.137    case AList.lookup (op =) arities inst
   3.138 @@ -396,32 +384,27 @@
   3.139         handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
   3.140    end;
   3.141  
   3.142 -fun inst_thm thy tvars' thm =
   3.143 +fun inst_cert thy lhs cert =
   3.144    let
   3.145 -    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
   3.146 -    val inter_sort = Sorts.inter_sort (Sign.classes_of thy);
   3.147 -    fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v
   3.148 -     of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar)
   3.149 -          (tvar, (v, inter_sort (sort, sort'))))
   3.150 -      | NONE => NONE;
   3.151 -    val insts = map_filter mk_inst tvars;
   3.152 -  in Thm.instantiate (insts, []) thm end;
   3.153 +    val ((vs, _), _) = Code.dest_cert thy cert;
   3.154 +    val sorts = map (fn (v, sort) => case AList.lookup (op =) lhs v
   3.155 +     of SOME sort' => Sorts.inter_sort (Sign.classes_of thy) (sort, sort')
   3.156 +      | NONE => sort) vs;
   3.157 +  in Code.constrain_cert thy sorts cert end;
   3.158  
   3.159  fun add_arity thy vardeps (class, tyco) =
   3.160    AList.default (op =) ((class, tyco),
   3.161 -    map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) (Sign.arity_number thy tyco));
   3.162 +    map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
   3.163 +      (Sign.arity_number thy tyco));
   3.164  
   3.165 -fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
   3.166 +fun add_cert thy vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) =
   3.167    if can (Graph.get_node eqngr) c then (rhss, eqngr)
   3.168    else let
   3.169      val lhs = map_index (fn (k, (v, _)) =>
   3.170        (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
   3.171 -    val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
   3.172 -      Vartab.update ((v, 0), sort)) lhs;
   3.173 -    val eqns = proto_eqns
   3.174 -      |> (map o apfst) (inst_thm thy inst_tab);
   3.175 -    val ((vs, _), rhss') = typscheme_rhss thy c eqns;
   3.176 -    val eqngr' = Graph.new_node (c, (vs, eqns)) eqngr;
   3.177 +    val cert = inst_cert thy lhs proto_cert;
   3.178 +    val ((vs, _), rhss') = typscheme_rhss thy c cert;
   3.179 +    val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
   3.180    in (map (pair c) rhss' @ rhss, eqngr') end;
   3.181  
   3.182  fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
   3.183 @@ -435,7 +418,7 @@
   3.184      val pp = Syntax.pp_global thy;
   3.185      val algebra = Sorts.subalgebra pp (is_proper_class thy)
   3.186        (AList.lookup (op =) arities') (Sign.classes_of thy);
   3.187 -    val (rhss, eqngr') = Symtab.fold (add_eqs thy vardeps) eqntab ([], eqngr);
   3.188 +    val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
   3.189      fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
   3.190        (rhs ~~ sortargs eqngr' c);
   3.191      val eqngr'' = fold (fn (c, rhs) => fold
     4.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jan 12 09:59:45 2010 +0100
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jan 12 16:27:42 2010 +0100
     4.3 @@ -447,7 +447,7 @@
     4.4    in Thm.certify_instantiate ([], var_subst) thm end;
     4.5  
     4.6  fun canonize_thms thy = map (Thm.transfer thy)
     4.7 -  #> Code.standard_typscheme thy #> desymbolize_tvars thy
     4.8 +  #> desymbolize_tvars thy
     4.9    #> same_arity thy #> map (desymbolize_vars thy);
    4.10  
    4.11  
    4.12 @@ -612,10 +612,10 @@
    4.13      fun stmt_classparam class =
    4.14        ensure_class thy algbr eqngr class
    4.15        #>> (fn class => Classparam (c, class));
    4.16 -    fun stmt_fun raw_eqns =
    4.17 +    fun stmt_fun cert =
    4.18        let
    4.19 -        val eqns = burrow_fst (canonize_thms thy) raw_eqns;
    4.20 -        val (vs, ty) = Code.typscheme_eqns thy c (map fst eqns);
    4.21 +        val ((vs, ty), raw_eqns) = Code.dest_cert thy cert;
    4.22 +        val eqns = burrow_fst (canonize_thms thy) (map snd raw_eqns);
    4.23        in
    4.24          fold_map (translate_tyvar_sort thy algbr eqngr) vs
    4.25          ##>> translate_typ thy algbr eqngr ty
    4.26 @@ -626,7 +626,7 @@
    4.27       of SOME tyco => stmt_datatypecons tyco
    4.28        | NONE => (case AxClass.class_of_param thy c
    4.29           of SOME class => stmt_classparam class
    4.30 -          | NONE => stmt_fun (Code_Preproc.eqns eqngr c))
    4.31 +          | NONE => stmt_fun (Code_Preproc.cert eqngr c))
    4.32    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
    4.33  and ensure_class thy (algbr as (_, algebra)) eqngr class =
    4.34    let
    4.35 @@ -933,11 +933,7 @@
    4.36    let
    4.37      val (_, eqngr) = Code_Preproc.obtain thy consts [];
    4.38      val all_consts = Graph.all_succs eqngr consts;
    4.39 -  in
    4.40 -    eqngr
    4.41 -    |> Graph.subgraph (member (op =) all_consts) 
    4.42 -    |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
    4.43 -  end;
    4.44 +  in Graph.subgraph (member (op =) all_consts) eqngr end;
    4.45  
    4.46  fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy;
    4.47