1.1 --- a/src/HOL/Code_Evaluation.thy	Wed Feb 24 11:21:37 2010 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Wed Feb 24 14:19:52 2010 +0100
     1.3 @@ -119,6 +119,44 @@
     1.4  end
     1.5  *}
     1.6  
     1.7 +setup {*
     1.8 +let
     1.9 +  fun mk_term_of_eq thy ty vs tyco abs ty_rep proj =
    1.10 +    let
    1.11 +      val arg = Var (("x", 0), ty);
    1.12 +      val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
    1.13 +        (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
    1.14 +        |> Thm.cterm_of thy;
    1.15 +      val cty = Thm.ctyp_of thy ty;
    1.16 +    in
    1.17 +      @{thm term_of_anything}
    1.18 +      |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
    1.19 +      |> Thm.varifyT
    1.20 +    end;
    1.21 +  fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
    1.22 +    let
    1.23 +      val algebra = Sign.classes_of thy;
    1.24 +      val vs = map (fn (v, sort) =>
    1.25 +        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
    1.26 +      val ty = Type (tyco, map TFree vs);
    1.27 +      val ty_rep = map_atyps
    1.28 +        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
    1.29 +      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    1.30 +      val eq = mk_term_of_eq thy ty vs tyco abs ty_rep proj;
    1.31 +   in
    1.32 +      thy
    1.33 +      |> Code.del_eqns const
    1.34 +      |> Code.add_eqn eq
    1.35 +    end;
    1.36 +  fun ensure_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
    1.37 +    let
    1.38 +      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    1.39 +    in if has_inst then add_term_of_code tyco raw_vs abs ty proj thy else thy end;
    1.40 +in
    1.41 +  Code.abstype_interpretation ensure_term_of_code
    1.42 +end
    1.43 +*}
    1.44 +
    1.45  
    1.46  subsubsection {* Code generator setup *}
    1.47