more explicit notion of canonized code equations
authorhaftmann
Wed Oct 14 12:20:01 2009 +0200 (2009-10-14)
changeset 329286bcc35f7ff6d
parent 32927 7a20fd22ba01
child 32929 0e9e13ac06d7
more explicit notion of canonized code equations
src/Pure/Isar/code.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/Isar/code.ML	Wed Oct 14 12:19:17 2009 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Oct 14 12:20:01 2009 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4    val const_typ_eqn: theory -> thm -> string * typ
     1.5    val typscheme_eqn: theory -> thm -> (string * sort) list * typ
     1.6    val typscheme_eqns: theory -> string -> thm list -> (string * sort) list * typ
     1.7 +  val same_typscheme: theory -> thm list -> thm list
     1.8  
     1.9    (*executable code*)
    1.10    val add_datatype: (string * typ) list -> theory -> theory
     2.1 --- a/src/Tools/Code/code_thingol.ML	Wed Oct 14 12:19:17 2009 +0200
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Oct 14 12:20:01 2009 +0200
     2.3 @@ -86,7 +86,7 @@
     2.4        * ((string * stmt) list * (string * stmt) list)) list
     2.5  
     2.6    val expand_eta: theory -> int -> thm -> thm
     2.7 -  val clean_thms: theory -> thm list -> thm list
     2.8 +  val canonize_thms: theory -> thm list -> thm list
     2.9    val read_const_exprs: theory -> string list -> string list * string list
    2.10    val consts_program: theory -> string list -> string list * (naming * program)
    2.11    val cached_program: theory -> naming * program
    2.12 @@ -446,9 +446,9 @@
    2.13      val var_subst = mk_desymbolization I I Var vs;
    2.14    in Thm.certify_instantiate ([], var_subst) thm end;
    2.15  
    2.16 -fun desymbolize_all_vars thy = desymbolize_tvars thy #> map (desymbolize_vars thy);
    2.17 -
    2.18 -fun clean_thms thy = map (Thm.transfer thy) #> same_arity thy #> desymbolize_all_vars thy;
    2.19 +fun canonize_thms thy = map (Thm.transfer thy)
    2.20 +  #> Code.same_typscheme thy #> desymbolize_tvars thy
    2.21 +  #> same_arity thy #> map (desymbolize_vars thy);
    2.22  
    2.23  
    2.24  (** statements, abstract programs **)
    2.25 @@ -614,7 +614,7 @@
    2.26        #>> (fn class => Classparam (c, class));
    2.27      fun stmt_fun raw_eqns =
    2.28        let
    2.29 -        val eqns = burrow_fst (clean_thms thy) raw_eqns;
    2.30 +        val eqns = burrow_fst (canonize_thms thy) raw_eqns;
    2.31          val (vs, ty) = Code.typscheme_eqns thy c (map fst eqns);
    2.32        in
    2.33          fold_map (translate_tyvar_sort thy algbr eqngr) vs