# HG changeset patch # User haftmann # Date 1254724593 -7200 # Node ID 019201eb7e071b0242fa551988f42455b5408990 # Parent 159309603edcf6ceda21813a50eb61b828f8d3b8 variables in type schemes must be renamed simultaneously with variables in equations diff -r 159309603edc -r 019201eb7e07 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Sun Oct 04 12:59:22 2009 +0200 +++ b/src/Pure/Isar/code.ML Mon Oct 05 08:36:33 2009 +0200 @@ -28,6 +28,8 @@ -> (thm * bool) list -> (thm * bool) list val const_typ_eqn: theory -> thm -> string * typ val typscheme_eqn: theory -> thm -> (string * sort) list * typ + val typscheme_rhss_eqns: theory -> string -> thm list + -> ((string * sort) list * typ) * (string * typ list) list (*executable code*) val add_datatype: (string * typ) list -> theory -> theory @@ -117,6 +119,15 @@ val ty' = Logic.unvarifyT ty; in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end; +fun default_typscheme thy c = + let + val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c + o Type.strip_sorts o Sign.the_const_type thy) c; + in case AxClass.class_of_param thy c + of SOME class => ([(Name.aT, [class])], ty) + | NONE => typscheme thy (c, ty) + end; + (** data store **) @@ -515,6 +526,15 @@ fun typscheme_eqn thy = typscheme thy o const_typ_eqn thy; fun const_eqn thy = fst o const_typ_eqn thy; +fun consts_of thy thms = [] |> (fold o fold o fold_aterms) + (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I) + (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of) thms); + +fun typscheme_rhss_eqns thy c [] = + (default_typscheme thy c, []) + | typscheme_rhss_eqns thy c (thms as thm :: _) = + (typscheme_eqn thy thm, consts_of thy thms); + fun assert_eqns_const thy c eqns = let fun cert (eqn as (thm, _)) = if c = const_eqn thy thm @@ -529,7 +549,7 @@ fun inter_sorts vs = fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs []; val sorts = map_transpose inter_sorts vss; - val vts = Name.names Name.context Name.aT sorts + val vts = Name.names Name.context "'X" sorts |> map (fn (v, sort) => TVar ((v, 0), sort)); in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end; diff -r 159309603edc -r 019201eb7e07 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Sun Oct 04 12:59:22 2009 +0200 +++ b/src/Tools/Code/code_preproc.ML Mon Oct 05 08:36:33 2009 +0200 @@ -227,27 +227,6 @@ map (fn (c, _) => AxClass.param_of_inst thy (c, tyco)) o maps (#params o AxClass.get_info thy); -fun consts_of thy eqns = [] |> (fold o fold o fold_aterms) - (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I) - (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns); - -fun default_typscheme_of thy c = - let - val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c - o Type.strip_sorts o Sign.the_const_type thy) c; - in case AxClass.class_of_param thy c - of SOME class => ([(Name.aT, [class])], ty) - | NONE => Code.typscheme thy (c, ty) - end; - -fun tyscm_rhss_of thy c eqns = - let - val tyscm = case eqns - of [] => default_typscheme_of thy c - | ((thm, _) :: _) => Code.typscheme_eqn thy thm; - val rhss = consts_of thy eqns; - in (tyscm, rhss) end; - (* data structures *) @@ -287,7 +266,7 @@ | NONE => let val eqns = Code.these_eqns thy c |> preprocess thy c; - val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns; + val ((lhs, _), rhss) = Code.typscheme_rhss_eqns thy c (map fst eqns); in ((lhs, rhss), eqns) end; fun obtain_instance thy arities (inst as (class, tyco)) = @@ -434,7 +413,7 @@ Vartab.update ((v, 0), sort)) lhs; val eqns = proto_eqns |> (map o apfst) (inst_thm thy inst_tab); - val (tyscm, rhss') = tyscm_rhss_of thy c eqns; + val (tyscm, rhss') = Code.typscheme_rhss_eqns thy c (map fst eqns); val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr; in (map (pair c) rhss' @ rhss, eqngr') end; diff -r 159309603edc -r 019201eb7e07 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Sun Oct 04 12:59:22 2009 +0200 +++ b/src/Tools/Code/code_thingol.ML Mon Oct 05 08:36:33 2009 +0200 @@ -554,16 +554,21 @@ fun stmt_classparam class = ensure_class thy algbr funcgr class #>> (fn class => Classparam (c, class)); - fun stmt_fun ((vs, ty), eqns) = - fold_map (translate_tyvar_sort thy algbr funcgr) vs - ##>> translate_typ thy algbr funcgr ty - ##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy) eqns) - #>> (fn info => Fun (c, info)); + fun stmt_fun raw_eqns = + let + val eqns = burrow_fst (clean_thms thy) raw_eqns; + val ((vs, ty), _) = Code.typscheme_rhss_eqns thy c (map fst eqns); + in + fold_map (translate_tyvar_sort thy algbr funcgr) vs + ##>> translate_typ thy algbr funcgr ty + ##>> fold_map (translate_eqn thy algbr funcgr) eqns + #>> (fn info => Fun (c, info)) + end; val stmt_const = case Code.get_datatype_of_constr thy c of SOME tyco => stmt_datatypecons tyco | NONE => (case AxClass.class_of_param thy c of SOME class => stmt_classparam class - | NONE => stmt_fun (Code_Preproc.typ funcgr c, Code_Preproc.eqns funcgr c)) + | NONE => stmt_fun (Code_Preproc.eqns funcgr c)) in ensure_stmt lookup_const (declare_const thy) stmt_const c end and ensure_class thy (algbr as (_, algebra)) funcgr class = let