# HG changeset patch # User haftmann # Date 1159196661 -7200 # Node ID a56f0743b3eeac57e598e33905c44aba629846d8 # Parent f3f2b1091ea0173fb3c50b83e0ad2f4a820b1a75 cleaned up diff -r f3f2b1091ea0 -r a56f0743b3ee src/Pure/Tools/codegen_consts.ML --- a/src/Pure/Tools/codegen_consts.ML Mon Sep 25 17:04:20 2006 +0200 +++ b/src/Pure/Tools/codegen_consts.ML Mon Sep 25 17:04:21 2006 +0200 @@ -18,10 +18,9 @@ val norm_of_typ: theory -> string * typ -> const val find_def: theory -> const -> ((string (*theory name*) * thm) * typ list) option - val sortinsts: theory -> typ * typ -> (typ * sort) list - val class_of_classop: theory -> const -> class option - val insts_of_classop: theory -> const -> const list - val typ_of_classop: theory -> const -> typ + val disc_typ_of_classop: theory -> const -> typ + val disc_typ_of_const: theory -> (const -> typ) -> const -> typ + val consts_of: theory -> term -> const list * (string * typ) list val read_const: theory -> string -> const val string_of_const: theory -> const -> string val raw_string_of_const: const -> string @@ -73,12 +72,6 @@ get_first get_def specs end; -fun sortinsts thy (ty, ty_decl) = - Vartab.empty - |> Sign.typ_match thy (ty_decl, ty) - |> Vartab.dest - |> map (fn (_, (sort, ty)) => (ty, sort)); - fun mk_classop_typinst thy (c, tyco) = (c, [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy (*for monotonicity*))) (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]); @@ -101,28 +94,15 @@ fun norm_of_typ thy (c, ty) = norm thy (c, Consts.typargs (Sign.consts_of thy) (c, ty)); -fun class_of_classop thy (c, [TVar _]) = - AxClass.class_of_param thy c - | class_of_classop thy (c, [TFree _]) = - AxClass.class_of_param thy c - | class_of_classop thy (c, _) = NONE; - -fun insts_of_classop thy (c_tys as (c, tys)) = - (*get rid of this finally*) - case AxClass.class_of_param thy c - of NONE => [c_tys] - | SOME class => let - val cs = maps (AxClass.params_of thy) - (Graph.all_succs ((#classes o Sorts.rep_algebra o Sign.classes_of) thy) [class]) - fun add_tyco (tyco, classes) = - if member (op = o apsnd fst) classes class - then cons tyco else I; - val tycos = - Symtab.fold add_tyco - ((#arities o Sorts.rep_algebra o Sign.classes_of) thy) []; - in maps (fn c => map (fn tyco => mk_classop_typinst thy (c, tyco)) tycos) cs end; - -fun typ_of_classop thy (c, [TVar _]) = +fun disc_typ_of_classop thy (c, [TVar _]) = + let + val class = (the o AxClass.class_of_param thy) c; + val (v, cs) = ClassPackage.the_consts_sign thy class + in + (Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u)) + ((the o AList.lookup (op =) cs) c) + end + | disc_typ_of_classop thy (c, [TFree _]) = let val class = (the o AxClass.class_of_param thy) c; val (v, cs) = ClassPackage.the_consts_sign thy class @@ -130,15 +110,7 @@ (Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u)) ((the o AList.lookup (op =) cs) c) end - | typ_of_classop thy (c, [TFree _]) = - let - val class = (the o AxClass.class_of_param thy) c; - val (v, cs) = ClassPackage.the_consts_sign thy class - in - (Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u)) - ((the o AList.lookup (op =) cs) c) - end - | typ_of_classop thy (c, [Type (tyco, _)]) = + | disc_typ_of_classop thy (c, [Type (tyco, _)]) = let val class = (the o AxClass.class_of_param thy) c; val (_, cs) = ClassPackage.the_inst_sign thy (class, tyco); @@ -146,6 +118,16 @@ Logic.varifyT ((the o AList.lookup (op =) cs) c) end; +fun disc_typ_of_const thy f (const as (c, [ty])) = + if (is_some o AxClass.class_of_param thy) c + then disc_typ_of_classop thy const + else f const + | disc_typ_of_const thy f const = f const; + +fun consts_of thy t = + fold_aterms (fn Const c => cons (norm_of_typ thy c, c) | _ => I) t [] + |> split_list; + (* reading constants as terms *) diff -r f3f2b1091ea0 -r a56f0743b3ee src/Pure/Tools/codegen_data.ML --- a/src/Pure/Tools/codegen_data.ML Mon Sep 25 17:04:20 2006 +0200 +++ b/src/Pure/Tools/codegen_data.ML Mon Sep 25 17:04:21 2006 +0200 @@ -26,7 +26,6 @@ val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) option val get_datatype_of_constr: theory -> CodegenConsts.const -> string option - val the_datatype_constrs: theory -> CodegenConsts.const list val print_thms: theory -> unit @@ -130,9 +129,8 @@ let val is_classop = (is_some o AxClass.class_of_param thy) c; val const = CodegenConsts.norm_of_typ thy c_ty; - val ty_decl = if is_classop - then CodegenConsts.typ_of_classop thy const - else snd (CodegenConsts.typ_of_inst thy const); + val ty_decl = CodegenConsts.disc_typ_of_const thy + (snd o CodegenConsts.typ_of_inst thy) const; val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy); in if Sign.typ_equiv thy (ty_decl, ty) then (const, thm) @@ -154,7 +152,7 @@ fun constrain thm0 thm = case AxClass.class_of_param thy (fst c) of SOME _ => let - val ty_decl = CodegenConsts.typ_of_classop thy c; + val ty_decl = CodegenConsts.disc_typ_of_classop thy c; val max = maxidx_of_typ ty_decl + 1; val thm = Thm.incr_indexes max thm; val ty = typ_func thy thm; @@ -676,9 +674,6 @@ Consttab.lookup ((the_dcontrs o get_exec) thy) c |> (Option.map o tap) (fn dtco => get_datatype thy dtco); -fun the_datatype_constrs thy = - Consttab.keys ((the_dcontrs o get_exec) thy); - (** code attributes **)