tuned construction of typerep instances
authorhaftmann
Wed May 13 18:41:39 2009 +0200 (2009-05-13)
changeset 31137cd3aafc1c631
parent 31136 85d04515abb3
child 31138 a51ce445d498
tuned construction of typerep instances
src/HOL/Typerep.thy
     1.1 --- a/src/HOL/Typerep.thy	Wed May 13 18:41:39 2009 +0200
     1.2 +++ b/src/HOL/Typerep.thy	Wed May 13 18:41:39 2009 +0200
     1.3 @@ -35,28 +35,18 @@
     1.4  end
     1.5  *}
     1.6  
     1.7 -ML {*
     1.8 -structure Typerep =
     1.9 -struct
    1.10 +setup {*
    1.11 +let
    1.12  
    1.13 -fun mk f (Type (tyco, tys)) =
    1.14 -      @{term Typerep} $ HOLogic.mk_message_string tyco
    1.15 -        $ HOLogic.mk_list @{typ typerep} (map (mk f) tys)
    1.16 -  | mk f (TFree v) =
    1.17 -      f v;
    1.18 -
    1.19 -fun typerep ty =
    1.20 -  Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
    1.21 -    $ Logic.mk_type ty;
    1.22 -
    1.23 -fun add_def tyco thy =
    1.24 +fun add_typerep tyco thy =
    1.25    let
    1.26      val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep};
    1.27      val vs = Name.names Name.context "'a" sorts;
    1.28      val ty = Type (tyco, map TFree vs);
    1.29      val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
    1.30        $ Free ("T", Term.itselfT ty);
    1.31 -    val rhs = mk (typerep o TFree) ty;
    1.32 +    val rhs = @{term Typerep} $ HOLogic.mk_message_string tyco
    1.33 +      $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
    1.34      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    1.35    in
    1.36      thy
    1.37 @@ -64,23 +54,20 @@
    1.38      |> `(fn lthy => Syntax.check_term lthy eq)
    1.39      |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    1.40      |> snd
    1.41 -    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.42 -    |> LocalTheory.exit_global
    1.43 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.44    end;
    1.45  
    1.46 -fun perhaps_add_def tyco thy =
    1.47 -  let
    1.48 -    val inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}
    1.49 -  in if inst then thy else add_def tyco thy end;
    1.50 +fun ensure_typerep tyco thy = if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
    1.51 +  andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
    1.52 +  then add_typerep tyco thy else thy;
    1.53 +
    1.54 +in
    1.55  
    1.56 -end;
    1.57 -*}
    1.58 +add_typerep @{type_name fun}
    1.59 +#> TypedefPackage.interpretation ensure_typerep
    1.60 +#> Code.type_interpretation (ensure_typerep o fst)
    1.61  
    1.62 -setup {*
    1.63 -  Typerep.add_def @{type_name fun}
    1.64 -  #> Typerep.add_def @{type_name itself}
    1.65 -  #> Typerep.add_def @{type_name bool}
    1.66 -  #> TypedefPackage.interpretation Typerep.perhaps_add_def
    1.67 +end
    1.68  *}
    1.69  
    1.70  lemma [code]: