--- a/src/HOL/Tools/datatype_codegen.ML Fri Mar 30 16:19:02 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Fri Mar 30 16:19:03 2007 +0200
@@ -620,11 +620,10 @@
fun add_eq_thms (dtco, (_, (vs, cs))) thy =
let
val thy_ref = Theory.self_ref thy;
- val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
- val c = CodegenConsts.norm thy ("op =", [ty]);
+ val const = ("op =", SOME dtco);
val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
in
- CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
+ CodegenData.add_funcl (const, CodegenData.lazy get_thms) thy
end;
in
prove_codetypes_arities (ClassPackage.intro_classes_tac [])
--- a/src/Pure/Tools/codegen_consts.ML Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_consts.ML Fri Mar 30 16:19:03 2007 +0200
@@ -8,17 +8,15 @@
signature CODEGEN_CONSTS =
sig
- type const = string * typ list (*type instantiations*)
+ type const = string * string option (* constant name, possibly instance *)
val const_ord: const * const -> order
val eq_const: const * const -> bool
structure Consttab: TABLE
- val inst_of_typ: theory -> string * typ -> const
- val typ_of_inst: theory -> const -> string * typ
- val norm: theory -> const -> const
- val norm_of_typ: theory -> string * typ -> const
- val typ_sort_inst: Sorts.algebra -> typ * sort
- -> sort Vartab.table -> sort Vartab.table
- val typargs: theory -> string * typ -> typ list
+ val const_of_cexpr: theory -> string * typ -> const
+ val string_of_typ: theory -> typ -> string
+ val string_of_const: theory -> const -> string
+ val read_const: theory -> string -> const
+
val co_of_const: theory -> const
-> string * ((string * sort) list * (string * typ list))
val co_of_const': theory -> const
@@ -29,13 +27,10 @@
-> string * typ list -> const
val consts_of_cos: theory -> string -> (string * sort) list
-> (string * typ list) list -> const list
- val find_def: theory -> const -> (string (*theory name*) * thm) option
- val consts_of: theory -> term -> const list
- val read_const: theory -> string -> const
- val string_of_const: theory -> const -> string
- val raw_string_of_const: const -> string
- val string_of_const_typ: theory -> string * typ -> string
- val string_of_typ: theory -> typ -> string
+
+ val typargs: theory -> string * typ -> typ list
+ val typ_sort_inst: Sorts.algebra -> typ * sort
+ -> sort Vartab.table -> sort Vartab.table
end;
structure CodegenConsts: CODEGEN_CONSTS =
@@ -44,124 +39,79 @@
(* basic data structures *)
-type const = string * typ list (*type instantiations*);
-val const_ord = prod_ord fast_string_ord (list_ord Term.typ_ord);
+type const = string * string option;
+val const_ord = prod_ord fast_string_ord (option_ord string_ord);
val eq_const = is_equal o const_ord;
structure Consttab =
TableFun(
- type key = string * typ list;
+ type key = const;
val ord = const_ord;
);
-
-(* type instantiations, overloading, dictionary values *)
-
fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
-fun inst_of_typ thy (c_ty as (c, ty)) =
- (c, Sign.const_typargs thy c_ty);
-fun typ_of_inst thy (c_tys as (c, tys)) =
- (c, Sign.const_instance thy c_tys);
+(* conversion between constant expressions and constants *)
-fun find_def thy (c, tys) =
- let
- val specs = Defs.specifications_of (Theory.defs_of thy) c;
- val typ_instance = case AxClass.class_of_param thy c
- of SOME _ => let
- fun instance_tycos (Type (tyco1, _), Type (tyco2, _)) = tyco1 = tyco2
- | instance_tycos (_ , TVar _) = true
- | instance_tycos ty_ty = Sign.typ_instance thy ty_ty;
- in instance_tycos end
- | NONE => Sign.typ_instance thy;
- fun get_def (_, { is_def, thyname, name, lhs, rhs }) =
- if is_def andalso forall typ_instance (tys ~~ lhs) then
- case try (Thm.get_axiom_i thy) name
- of SOME thm => SOME (thyname, thm)
- | NONE => NONE
- else NONE
- in
- get_first get_def specs
- end;
+fun const_of_cexpr thy (c_ty as (c, _)) =
+ case AxClass.class_of_param thy c
+ of SOME class => (case Sign.const_typargs thy c_ty
+ of [Type (tyco, _)] => if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
+ then (c, SOME tyco)
+ else (c, NONE)
+ | [_] => (c, NONE))
+ | NONE => (c, NONE);
-fun norm thy (c, insts) =
+fun string_of_const thy (c, NONE) = Sign.extern_const thy c
+ | string_of_const thy (c, SOME tyco) = Sign.extern_const thy c
+ ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco);
+
+
+(* reading constants as terms *)
+
+fun read_const thy raw_t =
let
- fun disciplined class [ty as Type (tyco, _)] =
- let
- val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]
- handle CLASS_ERROR => error ("No such instance: " ^ tyco ^ " :: " ^ class
- ^ ",\nrequired for overloaded constant " ^ c);
- val vs = Name.invents Name.context "'a" (length sorts);
- in
- (c, [Type (tyco, map (fn v => TVar ((v, 0), [])) vs)])
- end
- | disciplined class _ =
- (c, [TVar (("'a", 0), [class])]);
- in case AxClass.class_of_param thy c
- of SOME class => disciplined class insts
- | NONE => inst_of_typ thy (c, Sign.the_const_type thy c)
- end;
-
-fun norm_of_typ thy (c, ty) =
- norm thy (c, Sign.const_typargs thy (c, ty));
-
-fun consts_of thy t =
- fold_aterms (fn Const c => cons (norm_of_typ thy c) | _ => I) t []
-
-fun typ_sort_inst algebra =
- let
- val inters = Sorts.inter_sort algebra;
- fun match _ [] = I
- | match (TVar (v, S)) S' = Vartab.map_default (v, []) (fn S'' => inters (S, inters (S', S'')))
- | match (Type (a, Ts)) S =
- fold2 match Ts (Sorts.mg_domain algebra a S)
- in uncurry match end;
-
-fun typargs thy (c_ty as (c, ty)) =
- let
- val opt_class = AxClass.class_of_param thy c;
- val tys = Sign.const_typargs thy (c, ty);
- in case (opt_class, tys)
- of (SOME _, [Type (_, tys')]) => tys'
- | _ => tys
+ val t = Sign.read_term thy raw_t;
+ in case try dest_Const t
+ of SOME c_ty => const_of_cexpr thy c_ty
+ | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
end;
-(* printing *)
-
-fun string_of_const thy (c, tys) =
- space_implode " " (Sign.extern_const thy c
- :: map (enclose "[" "]" o Sign.string_of_typ thy) tys);
-
-fun raw_string_of_const (c, tys) =
- space_implode " " (c
- :: map (enclose "[" "]" o Display.raw_string_of_typ) tys);
-
-fun string_of_const_typ thy (c, ty) =
- string_of_const thy (c, Consts.typargs (Sign.consts_of thy) (c, ty));
-
-
-(* conversion between constants and datatype constructors *)
+(* conversion between constants, constant expressions and datatype constructors *)
fun const_of_co thy tyco vs (co, tys) =
- norm_of_typ thy (co, tys ---> Type (tyco, map TFree vs));
+ const_of_cexpr thy (co, tys ---> Type (tyco, map TFree vs));
fun consts_of_cos thy tyco vs cos =
let
val dty = Type (tyco, map TFree vs);
- fun mk_co (co, tys) = norm_of_typ thy (co, tys ---> dty);
+ fun mk_co (co, tys) = const_of_cexpr thy (co, tys ---> dty);
in map mk_co cos end;
local
exception BAD of string;
+fun mg_typ_of_const thy (c, NONE) = Sign.the_const_type thy c
+ | mg_typ_of_const thy (c, SOME tyco) =
+ let
+ val SOME class = AxClass.class_of_param thy c;
+ val ty = Sign.the_const_type thy c;
+ (*an approximation*)
+ val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]
+ handle CLASS_ERROR => raise BAD ("No such instance: " ^ tyco ^ " :: " ^ class
+ ^ ",\nrequired for overloaded constant " ^ c);
+ val vs = Name.invents Name.context "'a" (length sorts);
+ in map_atyps (K (Type (tyco, map (fn v => TVar ((v, 0), [])) vs))) ty end;
+
fun gen_co_of_const thy const =
let
- val (c, ty) = (apsnd Logic.unvarifyT o typ_of_inst thy) const;
+ val (c, _) = const;
+ val ty = (Logic.unvarifyT o mg_typ_of_const thy) const;
fun err () = raise BAD
- ("Illegal type for datatype constructor: " ^ Sign.string_of_typ thy ty);
+ ("Illegal type for datatype constructor: " ^ string_of_typ thy ty);
val (tys, ty') = strip_type ty;
val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
handle TYPE _ => err ();
@@ -197,18 +147,26 @@
in (tyco, (vs, cos)) end;
-(* reading constants as terms *)
+(* dictionary values *)
-fun read_const_typ thy raw_t =
+fun typargs thy (c_ty as (c, ty)) =
let
- val t = Sign.read_term thy raw_t
- in case try dest_Const t
- of SOME c_ty => (typ_of_inst thy o norm_of_typ thy) c_ty
- | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
+ val opt_class = AxClass.class_of_param thy c;
+ val tys = Sign.const_typargs thy (c, ty);
+ in case (opt_class, tys)
+ of (SOME class, ty as [Type (tyco, tys')]) =>
+ if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
+ then tys' else ty
+ | _ => tys
end;
-fun read_const thy =
- norm_of_typ thy o read_const_typ thy;
-
+fun typ_sort_inst algebra =
+ let
+ val inters = Sorts.inter_sort algebra;
+ fun match _ [] = I
+ | match (TVar (v, S)) S' = Vartab.map_default (v, []) (fn S'' => inters (S, inters (S', S'')))
+ | match (Type (a, Ts)) S =
+ fold2 match Ts (Sorts.mg_domain algebra a S)
+ in uncurry match end;
end;
--- a/src/Pure/Tools/codegen_data.ML Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML Fri Mar 30 16:19:03 2007 +0200
@@ -27,10 +27,9 @@
val coregular_algebra: theory -> Sorts.algebra
val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
val these_funcs: theory -> CodegenConsts.const -> thm list
- val tap_typ: theory -> CodegenConsts.const -> typ option
val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
val get_datatype_of_constr: theory -> CodegenConsts.const -> string option
- val get_constr_typ: theory -> CodegenConsts.const -> typ option
+ val default_typ: theory -> CodegenConsts.const -> typ
val preprocess_cterm: cterm -> thm
@@ -454,7 +453,7 @@
val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
val clsops = (these o Option.map snd o try (AxClass.params_of_class thy)) class;
val funcs = clsops
- |> map (fn (clsop, _) => CodegenConsts.norm thy (clsop, [Type (tyco, map (TFree o rpair []) vs)]))
+ |> map (fn (clsop, _) => (clsop, SOME tyco))
|> map (Consttab.lookup ((the_funcs o get_exec) thy))
|> (map o Option.map) (Susp.force o fst)
|> maps these
@@ -518,7 +517,7 @@
val thy = Thm.theory_of_thm thm;
val raw_funcs = CodegenFunc.mk_func strict thm;
val error_warning = if strict then error else warning #> K NONE;
- fun check_typ_classop class (const as (c, [Type (tyco, _)]), thm) =
+ fun check_typ_classop class (const as (c, SOME tyco), thm) =
let
val ((_, ty), _) = CodegenFunc.dest_func thm;
val ty_decl = classop_weakest_typ thy class (c, tyco);
@@ -547,7 +546,7 @@
^ "\nis incompatible with permitted least general type\n"
^ CodegenConsts.string_of_typ thy ty_strongest)
end
- | check_typ_classop class ((c, [_]), thm) =
+ | check_typ_classop class ((c, NONE), thm) =
error_warning ("Illegal type for class operation " ^ quote c
^ "\nin defining equation\n"
^ string_of_thm thm);
@@ -563,7 +562,7 @@
^ "\nis incompatible declared function type\n"
^ CodegenConsts.string_of_typ thy ty_decl)
end;
- fun check_typ (const as (c, tys), thm) =
+ fun check_typ (const as (c, _), thm) =
case AxClass.class_of_param thy c
of SOME class => check_typ_classop class (const, thm)
| NONE => check_typ_fun (const, thm);
@@ -599,12 +598,12 @@
(del_thm thm)) funcs)) thy
end;
-fun add_funcl (c, lthms) thy =
+fun add_funcl (const, lthms) thy =
let
- val c' = CodegenConsts.norm thy c;
- val lthms' = certificate thy (fn thy => certify_const thy c' o maps (CodegenFunc.mk_func true)) lthms;
+ val lthms' = certificate thy (fn thy => certify_const thy const
+ o maps (CodegenFunc.mk_func true)) lthms;
in
- map_exec_purge (SOME [c]) (map_funcs (Consttab.map_default (c', (Susp.value [], []))
+ map_exec_purge (SOME [const]) (map_funcs (Consttab.map_default (const, (Susp.value [], []))
(add_lthms lthms'))) thy
end;
@@ -682,8 +681,8 @@
| apply_preproc thy f (thms as (thm :: _)) =
let
val thms' = f thy thms;
- val c = (CodegenConsts.norm_of_typ thy o fst o CodegenFunc.dest_func) thm;
- in (certify_const thy c o map CodegenFunc.mk_head) thms' end;
+ val thms'' as ((const, _) :: _) = map CodegenFunc.mk_head thms'
+ in (certify_const thy const o map CodegenFunc.mk_head) thms' end;
fun cmp_thms thy =
make_ord (fn (thm1, thm2) => not (Sign.typ_instance thy (CodegenFunc.typ_func thm1, CodegenFunc.typ_func thm2)));
@@ -716,44 +715,6 @@
end; (*local*)
-local
-
-fun get_funcs thy const =
- Consttab.lookup ((the_funcs o get_exec) thy) const
- |> Option.map (Susp.force o fst)
- |> these
- |> map (Thm.transfer thy);
-
-in
-
-fun these_funcs thy const =
- let
- fun get_prim_def_funcs (const as (c, tys)) =
- case CodegenConsts.find_def thy const
- of SOME (_, thm) =>
- thm
- |> Thm.transfer thy
- |> gen_mk_func_typ false
- |> map (CodegenFunc.expand_eta ~1 o snd)
- | NONE => []
- fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
- o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
- val funcs = case get_funcs thy const
- of [] => get_prim_def_funcs const
- | funcs => funcs
- in
- funcs
- |> preprocess thy
- |> drop_refl thy
- end;
-
-fun tap_typ thy const =
- case get_funcs thy const
- of thm :: _ => SOME (CodegenFunc.typ_func thm)
- | [] => NONE;
-
-end; (*local*)
-
fun get_datatype thy tyco =
case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
of SOME spec => spec
@@ -781,6 +742,65 @@
|> SOME end
| NONE => NONE;
+fun default_typ_proto thy (const as (c, SOME tyco)) = classop_weakest_typ thy
+ ((the o AxClass.class_of_param thy) c) (c, tyco) |> SOME
+ | default_typ_proto thy (const as (c, NONE)) = case AxClass.class_of_param thy c
+ of SOME class => SOME (Term.map_type_tvar
+ (K (TVar (("'a", 0), [class]))) (Sign.the_const_type thy c))
+ | NONE => get_constr_typ thy const;
+
+local
+
+fun get_funcs thy const =
+ Consttab.lookup ((the_funcs o get_exec) thy) const
+ |> Option.map (Susp.force o fst)
+ |> these
+ |> map (Thm.transfer thy);
+
+fun find_def thy (const as (c, _)) =
+ let
+ val specs = Defs.specifications_of (Theory.defs_of thy) c;
+ val ty = case try (default_typ_proto thy) const
+ of NONE => NONE
+ | SOME ty => ty;
+ val tys = Sign.const_typargs thy (c, ty |> the_default (Sign.the_const_type thy c));
+ fun get_def (_, { is_def, name, lhs, rhs, thyname }) =
+ if is_def andalso forall (Sign.typ_instance thy) (tys ~~ lhs) then
+ try (Thm.get_axiom_i thy) name
+ else NONE
+ in get_first get_def specs end;
+
+in
+
+fun these_funcs thy const =
+ let
+ fun get_prim_def_funcs (const as (c, tys)) =
+ case find_def thy const
+ of SOME thm =>
+ thm
+ |> Thm.transfer thy
+ |> gen_mk_func_typ false
+ |> map (CodegenFunc.expand_eta ~1 o snd)
+ | NONE => []
+ fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
+ o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
+ val funcs = case get_funcs thy const
+ of [] => get_prim_def_funcs const
+ | funcs => funcs
+ in
+ funcs
+ |> preprocess thy
+ |> drop_refl thy
+ end;
+
+fun default_typ thy (const as (c, _)) = case default_typ_proto thy const
+ of SOME ty => ty
+ | NONE => (case get_funcs thy const
+ of thm :: _ => CodegenFunc.typ_func thm
+ | [] => Sign.the_const_type thy c);
+
+end; (*local*)
+
(** code attributes **)
--- a/src/Pure/Tools/codegen_func.ML Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML Fri Mar 30 16:19:03 2007 +0200
@@ -75,7 +75,7 @@
o Drule.fconv_rule Drule.beta_eta_conversion);
val mk_head = lift_thm_thy (fn thy => fn thm =>
- ((CodegenConsts.norm_of_typ thy o fst o dest_func) thm, thm));
+ ((CodegenConsts.const_of_cexpr thy o fst o dest_func) thm, thm));
local
--- a/src/Pure/Tools/codegen_funcgr.ML Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML Fri Mar 30 16:19:03 2007 +0200
@@ -80,7 +80,7 @@
let
val thy = Thm.theory_of_thm thm;
val is_refl = curry CodegenConsts.eq_const const;
- fun the_const c = case try (CodegenConsts.norm_of_typ thy) c
+ fun the_const c = case try (CodegenConsts.const_of_cexpr thy) c
of SOME const => if is_refl const then I else insert CodegenConsts.eq_const const
| NONE => I
in fold_consts the_const thms [] end;
@@ -147,7 +147,7 @@
fun resort_funcss thy algebra funcgr =
let
- val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodegenConsts.norm_of_typ thy);
+ val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodegenConsts.const_of_cexpr thy);
fun resort_dep (const, thms) = (const, resort_thms algebra typ_funcgr thms)
handle Sorts.CLASS_ERROR e => raise INVALID ([const], Sorts.msg_class_error (Sign.pp thy) e
^ ",\nfor constant " ^ CodegenConsts.string_of_const thy const
@@ -162,7 +162,7 @@
in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end;
fun resort_recs funcss =
let
- fun tap_typ c_ty = case try (CodegenConsts.norm_of_typ thy) c_ty
+ fun tap_typ c_ty = case try (CodegenConsts.const_of_cexpr thy) c_ty
of SOME const => AList.lookup (CodegenConsts.eq_const) funcss const
|> these
|> try hd
@@ -177,14 +177,6 @@
in if unchanged then funcss' else resort_rec_until funcss' end;
in map resort_dep #> resort_rec_until end;
-fun classop_const thy algebra class classop tyco =
- let
- val sorts = Sorts.mg_domain algebra tyco [class]
- val (var, _) = try (AxClass.params_of_class thy) class |> the_default ("'a", []);
- val vs = Name.names (Name.declare var Name.context) "'a" sorts;
- val arity_typ = Type (tyco, map TFree vs);
- in (classop, [arity_typ]) end;
-
fun instances_of thy algebra insts =
let
val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
@@ -192,8 +184,7 @@
try (AxClass.params_of_class thy) class
|> Option.map snd
|> these
- |> map (fn (c, _) => classop_const thy algebra class c tyco)
- |> map (CodegenConsts.norm thy)
+ |> map (fn (c, _) => (c, SOME tyco))
in
Symtab.empty
|> fold (fn (tyco, class) =>
@@ -204,9 +195,9 @@
fun instances_of_consts thy algebra funcgr consts =
let
- fun inst (const as (c, ty)) = case try (CodegenConsts.norm_of_typ thy) const
- of SOME const => insts_of thy algebra c (fst (Constgraph.get_node funcgr const)) ty
- | NONE => [];
+ fun inst (cexpr as (c, ty)) = insts_of thy algebra c
+ ((fst o Constgraph.get_node funcgr o CodegenConsts.const_of_cexpr thy) cexpr)
+ ty handle CLASS_ERROR => [];
in
[]
|> fold (fold (insert (op =)) o inst) consts
@@ -248,44 +239,23 @@
val funcss = raw_funcss
|> resort_funcss thy algebra funcgr
|> filter_out (can (Constgraph.get_node funcgr) o fst);
- fun classop_typ (c, [typarg]) class =
- let
- val ty = Sign.the_const_type thy c;
- val inst = case typarg
- of Type (tyco, _) => classop_const thy algebra class c tyco
- |> snd
- |> the_single
- |> Logic.varifyT
- | _ => TVar (("'a", 0), [class]);
- in Term.map_type_tvar (K inst) ty end;
- fun default_typ (const as (c, tys)) = case AxClass.class_of_param thy c
- of SOME class => classop_typ const class
- | NONE => (case CodegenData.tap_typ thy const
- of SOME ty => ty
- | NONE => (case CodegenData.get_constr_typ thy const
- of SOME ty => ty
- | NONE => Sign.the_const_type thy c))
- fun typ_func (const as (c, tys)) thms thm =
- let
- val ty = CodegenFunc.typ_func thm;
- in case AxClass.class_of_param thy c
- of SOME class => (case tys
- of [Type _] => let val ty_decl = classop_typ const class
- in if Sign.typ_equiv thy (ty, ty_decl) then ty
- else raise raise INVALID ([const], "Illegal instantation for class operation "
- ^ CodegenConsts.string_of_const thy const
- ^ ":\n" ^ CodegenConsts.string_of_typ thy ty_decl
- ^ "\nto " ^ CodegenConsts.string_of_typ thy ty
- ^ "\nin defining equations\n"
- ^ (cat_lines o map string_of_thm) thms)
- end
- | _ => ty)
- | NONE => ty
- end;
- fun add_funcs (const, thms as thm :: _) =
- Constgraph.new_node (const, (typ_func const thms thm, thms))
- | add_funcs (const, []) =
- Constgraph.new_node (const, (default_typ const, []));
+ fun typ_func const [] = CodegenData.default_typ thy const
+ | typ_func (_, NONE) (thm :: _) = CodegenFunc.typ_func thm
+ | typ_func (const as (c, SOME tyco)) (thms as (thm :: _)) =
+ let
+ val ty = CodegenFunc.typ_func thm;
+ val SOME class = AxClass.class_of_param thy c;
+ val sorts_decl = Sorts.mg_domain algebra tyco [class];
+ val tys = CodegenConsts.typargs thy (c, ty);
+ val sorts = map (snd o dest_TVar) tys;
+ in if sorts = sorts_decl then ty
+ else raise INVALID ([const], "Illegal instantation for class operation "
+ ^ CodegenConsts.string_of_const thy const
+ ^ "\nin defining equations\n"
+ ^ (cat_lines o map string_of_thm) thms)
+ end;
+ fun add_funcs (const, thms) =
+ Constgraph.new_node (const, (typ_func const thms, thms));
fun add_deps (funcs as (const, thms)) funcgr =
let
val deps = consts_of funcs;
@@ -339,6 +309,8 @@
fun ensure_consts_term rewrites thy f ct funcgr =
let
+ fun consts_of thy t =
+ fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t []
fun rhs_conv conv thm =
let
val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm;
@@ -348,12 +320,12 @@
val thm1 = CodegenData.preprocess_cterm ct
|> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy);
val ct' = Drule.dest_equals_rhs (Thm.cprop_of thm1);
- val consts = CodegenConsts.consts_of thy (Thm.term_of ct');
+ val consts = consts_of thy (Thm.term_of ct');
val funcgr' = ensure_consts rewrites thy consts funcgr;
val algebra = CodegenData.coregular_algebra thy;
val (_, thm2) = Thm.varifyT' [] thm1;
val thm3 = Thm.reflexive (Drule.dest_equals_rhs (Thm.cprop_of thm2));
- val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodegenConsts.norm_of_typ thy);
+ val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodegenConsts.const_of_cexpr thy);
val [thm4] = resort_thms algebra typ_funcgr [thm3];
val tfrees = Term.add_tfrees (Thm.prop_of thm1) [];
fun inst thm =
--- a/src/Pure/Tools/codegen_names.ML Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_names.ML Fri Mar 30 16:19:03 2007 +0200
@@ -216,23 +216,21 @@
fun instance_policy thy = policy thy (fn (class, tyco) =>
NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
-fun force_thyname thy (const as (c, tys)) =
+fun force_thyname thy (const as (c, opt_tyco)) =
case AxClass.class_of_param thy c
- of SOME class => (case tys
- of [Type (tyco, _)] => SOME (thyname_of_instance thy (class, tyco))
- | _ => SOME (thyname_of_class thy class))
+ of SOME class => (case opt_tyco
+ of SOME tyco => SOME (thyname_of_instance thy (class, tyco))
+ | NONE => SOME (thyname_of_class thy class))
| NONE => (case CodegenData.get_datatype_of_constr thy const
of SOME dtco => SOME (thyname_of_tyco thy dtco)
- | NONE => (case CodegenConsts.find_def thy const
- of SOME (thyname, _) => SOME thyname
- | NONE => NONE));
+ | NONE => NONE);
-fun const_policy thy (c, tys) =
- case force_thyname thy (c, tys)
+fun const_policy thy (const as (c, opt_tyco)) =
+ case force_thyname thy const
of NONE => policy thy NameSpace.base thyname_of_const c
| SOME thyname => let
val prefix = (purify_prefix o NameSpace.explode o dotify) thyname;
- val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys;
+ val tycos = the_list opt_tyco;
val base = map (purify_base o NameSpace.base) (c :: tycos);
in NameSpace.implode (prefix @ [space_implode "_" base]) end;
@@ -307,7 +305,7 @@
structure ConstName = CodeDataFun
(struct
val name = "Pure/codegen_names";
- type T = const Consttab.table * (string * typ list) Symtab.table;
+ type T = const Consttab.table * (string * string option) Symtab.table;
val empty = (Consttab.empty, Symtab.empty);
fun merge _ ((const1, constrev1), (const2, constrev2)) =
(Consttab.merge eq_string (const1, const2),
@@ -395,8 +393,7 @@
get thy #instance StringPairTab.lookup map_instance StringPairTab.update instance_policy
#> add_idf idf_instance;
fun const thy =
- CodegenConsts.norm thy
- #> get_const thy
+ get_const thy
#> add_idf idf_const;
fun class_rev thy =
--- a/src/Pure/Tools/codegen_package.ML Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML Fri Mar 30 16:19:03 2007 +0200
@@ -141,7 +141,7 @@
val (v, cs) = AxClass.params_of_class thy class;
val class' = CodegenNames.class thy class;
val classrels' = map (curry (CodegenNames.classrel thy) class) superclasses;
- val classops' = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs;
+ val classops' = map (CodegenNames.const thy o CodegenConsts.const_of_cexpr thy) cs;
val defgen_class =
fold_map (ensure_def_class thy algbr funcgr strct) superclasses
##>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs
@@ -170,7 +170,7 @@
||>> fold_map (fn (c, tys) =>
fold_map (exprgen_type thy algbr funcgr strct) tys
#-> (fn tys' =>
- pair ((CodegenNames.const thy o CodegenConsts.norm_of_typ thy)
+ pair ((CodegenNames.const thy o CodegenConsts.const_of_cexpr thy)
(c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
|-> (fn (vs, cos) => succeed (CodegenThingol.Datatype (vs, cos)))
end;
@@ -235,7 +235,7 @@
end
and exprgen_dict_parms thy (algbr as (_, consts)) funcgr strct (c, ty_ctxt) =
let
- val c' = CodegenConsts.norm_of_typ thy (c, ty_ctxt)
+ val c' = CodegenConsts.const_of_cexpr thy (c, ty_ctxt)
val idf = CodegenNames.const thy c';
val ty_decl = Consts.the_declaration consts idf;
val (tys, tys_decl) = pairself (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
@@ -258,7 +258,7 @@
(superclass, (classrel, (inst, dss))));
fun gen_classop_def (classop as (c, ty)) trns =
trns
- |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy classop)
+ |> ensure_def_const thy algbr funcgr strct (CodegenConsts.const_of_cexpr thy classop)
||>> exprgen_term thy algbr funcgr strct (Const (c, map_type_tfree (K arity_typ) ty));
fun defgen_inst trns =
trns
@@ -276,13 +276,13 @@
|> ensure_def thy defgen_inst true ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
|> pair inst
end
-and ensure_def_const thy (algbr as (_, consts)) funcgr strct (c_tys as (c, tys)) trns =
+and ensure_def_const thy (algbr as (_, consts)) funcgr strct (const as (c, opt_tyco)) trns =
let
- val c' = CodegenNames.const thy c_tys;
+ val c' = CodegenNames.const thy const;
fun defgen_datatypecons trns =
trns
|> ensure_def_tyco thy algbr funcgr strct
- ((the o CodegenData.get_datatype_of_constr thy) c_tys)
+ ((the o CodegenData.get_datatype_of_constr thy) const)
|-> (fn _ => succeed CodegenThingol.Bot);
fun defgen_classop trns =
trns
@@ -290,7 +290,7 @@
|-> (fn _ => succeed CodegenThingol.Bot);
fun defgen_fun trns =
case CodegenFuncgr.funcs funcgr
- (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) c_tys)
+ (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) const)
of thms as _ :: _ =>
let
val (ty, eq_thms) = prep_eqs thy thms;
@@ -315,20 +315,20 @@
| [] =>
trns
|> fail ("No defining equations found for "
- ^ (quote o CodegenConsts.string_of_const thy) c_tys);
- val defgen = if (is_some o CodegenData.get_datatype_of_constr thy) c_tys
+ ^ (quote o CodegenConsts.string_of_const thy) const);
+ val defgen = if (is_some o CodegenData.get_datatype_of_constr thy) const
then defgen_datatypecons
- else if (is_some o AxClass.class_of_param thy) c andalso
- case tys of [TFree _] => true | [TVar _] => true | _ => false
- then defgen_classop
- else defgen_fun
+ else if is_some opt_tyco
+ orelse (not o is_some o AxClass.class_of_param thy) c
+ then defgen_fun
+ else defgen_classop
val strict = check_strict strct (CodegenSerializer.const_has_serialization thy) c';
in
trns
|> tracing (fn _ => "generating constant "
- ^ (quote o CodegenConsts.string_of_const thy) c_tys)
+ ^ (quote o CodegenConsts.string_of_const thy) const)
|> ensure_def thy defgen strict ("generating constant "
- ^ CodegenConsts.string_of_const thy c_tys) c'
+ ^ CodegenConsts.string_of_const thy const) c'
|> pair c'
end
and exprgen_term thy algbr funcgr strct (Const (c, ty)) trns =
@@ -359,7 +359,7 @@
|>> (fn (t, ts) => t `$$ ts)
and appgen_default thy algbr funcgr strct ((c, ty), ts) trns =
trns
- |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy (c, ty))
+ |> ensure_def_const thy algbr funcgr strct (CodegenConsts.const_of_cexpr thy (c, ty))
||>> fold_map (exprgen_type thy algbr funcgr strct) ((fst o Term.strip_type) ty)
||>> exprgen_type thy algbr funcgr strct ((snd o Term.strip_type) ty)
||>> exprgen_dict_parms thy algbr funcgr strct (c, ty)
@@ -483,14 +483,11 @@
local
-fun add_consts thy f (c1, c2 as (c, tys)) =
+fun add_consts thy f (c1, c2 as (c, opt_tyco)) =
let
- val _ = case tys
- of [TVar _] => if is_some (AxClass.class_of_param thy c)
- then error ("Not a function: " ^ CodegenConsts.string_of_const thy c2)
- else ()
- | _ => ();
- val _ = if is_some (CodegenData.get_datatype_of_constr thy c2)
+ val _ = if
+ is_some (AxClass.class_of_param thy c) andalso is_none opt_tyco
+ orelse is_some (CodegenData.get_datatype_of_constr thy c2)
then error ("Not a function: " ^ CodegenConsts.string_of_const thy c2)
else ();
val funcgr = Funcgr.make thy [c1, c2];
@@ -548,10 +545,10 @@
in
-val abstyp = gen_abstyp CodegenConsts.norm Sign.certify_typ;
+val abstyp = gen_abstyp (K I) Sign.certify_typ;
val abstyp_e = gen_abstyp CodegenConsts.read_const (fn thy => Sign.read_typ (thy, K NONE));
-val constsubst = gen_constsubst CodegenConsts.norm;
+val constsubst = gen_constsubst (K I);
val constsubst_e = gen_constsubst CodegenConsts.read_const;
end; (*local*)
@@ -608,16 +605,27 @@
fun consts_of thy thyname =
let
val this_thy = Option.map theory thyname |> the_default thy;
- val defs = (#defs o rep_theory) this_thy;
- val cs_names = (Symtab.keys o snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy;
- val consts = maps (fn c => (map (fn tys => CodegenConsts.norm thy (c, tys))
- o map #lhs o filter #is_def o map snd o Defs.specifications_of defs) c) cs_names;
- fun is_const thyname (c, _) =
- (*this is an approximation*)
- not (exists (fn thy => Sign.declared_const thy c) (Theory.parents_of this_thy))
+ val defs = (#defs o rep_theory) thy;
+ val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
+ ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
+ fun classop c = case AxClass.class_of_param thy c
+ of NONE => [(c, NONE)]
+ | SOME class => Symtab.fold
+ (fn (tyco, classes) => if AList.defined (op =) classes class
+ then cons (c, SOME tyco) else I)
+ ((#arities o Sorts.rep_algebra o Sign.classes_of) this_thy)
+ [(c, NONE)];
+ val consts = maps classop cs;
+ fun test_instance thy (class, tyco) =
+ can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
+ fun belongs_here thyname (c, NONE) =
+ not (exists (fn thy => Sign.declared_const thy c) (Theory.parents_of this_thy))
+ | belongs_here thyname (c, SOME tyco) =
+ not (exists (fn thy => test_instance thy ((the o AxClass.class_of_param thy) c, tyco))
+ (Theory.parents_of this_thy))
in case thyname
of NONE => consts
- | SOME thyname => filter (is_const thyname) consts
+ | SOME thyname => filter (belongs_here thyname) consts
end;
fun filter_generatable thy targets consts =
--- a/src/Pure/Tools/codegen_serializer.ML Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Fri Mar 30 16:19:03 2007 +0200
@@ -11,7 +11,7 @@
include BASIC_CODEGEN_THINGOL;
val add_syntax_class: string -> class
- -> (string * ((string * typ list) * string) list) option -> theory -> theory;
+ -> (string * (CodegenConsts.const * string) list) option -> theory -> theory;
val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
val add_syntax_tycoP: string -> string -> OuterParse.token list
-> (theory -> theory) * OuterParse.token list;
@@ -422,7 +422,7 @@
and pr_bind' ((NONE, NONE), _) = str "_"
| pr_bind' ((SOME v, NONE), _) = str v
| pr_bind' ((NONE, SOME p), _) = p
- | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
+ | pr_bind' ((SOME v, SOME p), _) =
and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy;
fun pr_def (MLFuns (funns as (funn :: funns'))) =
let
@@ -889,7 +889,7 @@
val code_width = ref 80;
fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
-fun seri_ml pr_def pr_modl output labelled_name reserved_user module_alias module_prolog
+fun seri_ml pr_def pr_modl reserved_ml output labelled_name reserved_user module_alias module_prolog
(_ : string -> class_syntax option) tyco_syntax const_syntax code =
let
val is_cons = fn node => case CodegenThingol.get_def code node
@@ -898,7 +898,7 @@
datatype node =
Def of string * ml_def option
| Module of string * ((Name.context * Name.context) * node Graph.T);
- val empty_names = ML_Syntax.reserved |> fold Name.declare reserved_user;
+ val empty_names = reserved_ml |> fold Name.declare reserved_user;
val empty_module = ((empty_names, empty_names), Graph.empty);
fun map_node [] f = f
| map_node (m::ms) f =
@@ -1064,9 +1064,17 @@
parse_args ((Args.$$$ "-" >> K output_diag
|| Args.$$$ "#" >> K output_internal
|| Args.name >> output_file)
- >> (fn output => seri_ml pr_sml pr_sml_modl output))
+ >> (fn output => seri_ml pr_sml pr_sml_modl ML_Syntax.reserved output))
end;
+val reserved_ocaml = Name.make_context ["and", "as", "assert", "begin", "class",
+ "constraint", "do", "done", "downto", "else", "end", "exception",
+ "external", "false", "for", "fun", "function", "functor", "if",
+ "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
+ "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
+ "sig", "struct", "then", "to", "true", "try", "type", "val",
+ "virtual", "when", "while", "with", "mod"];
+
val isar_seri_ocaml =
let
fun output_file file = File.write (Path.explode file) o code_output;
@@ -1074,7 +1082,7 @@
in
parse_args ((Args.$$$ "-" >> K output_diag
|| Args.name >> output_file)
- >> (fn output => seri_ml pr_ocaml pr_ocaml_modl output))
+ >> (fn output => seri_ml pr_ocaml pr_ocaml_modl reserved_ocaml output))
end;
@@ -1662,7 +1670,8 @@
|> CodegenThingol.project_code
(Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const)
(SOME [val_name])
- |> seri_ml pr_sml pr_sml_modl I (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
+ |> seri_ml pr_sml pr_sml_modl ML_Syntax.reserved I (labelled_name thy) reserved
+ (Symtab.lookup alias) (Symtab.lookup prolog)
(fun_of class) (fun_of tyco) (fun_of const)
|> eval
end;
@@ -1790,7 +1799,7 @@
fun idfs_of_const thy c =
let
val c' = (c, Sign.the_const_type thy c);
- val c'' = CodegenConsts.norm_of_typ thy c';
+ val c'' = CodegenConsts.const_of_cexpr thy c';
in (c'', CodegenNames.const thy c'') end;
fun no_bindings x = (Option.map o apsnd)
@@ -1798,16 +1807,11 @@
fun gen_add_haskell_monad prep_const c_run c_mbind c_kbind thy =
let
- val c_run' =
- (CodegenConsts.norm thy o prep_const thy) c_run;
- val c_mbind' =
- (CodegenConsts.norm thy o prep_const thy) c_mbind;
- val c_mbind'' =
- CodegenNames.const thy c_mbind';
- val c_kbind' =
- (CodegenConsts.norm thy o prep_const thy) c_kbind;
- val c_kbind'' =
- CodegenNames.const thy c_kbind';
+ val c_run' = prep_const thy c_run;
+ val c_mbind' = prep_const thy c_mbind;
+ val c_mbind'' = CodegenNames.const thy c_mbind';
+ val c_kbind' = prep_const thy c_kbind;
+ val c_kbind'' = CodegenNames.const thy c_kbind';
val pr = pretty_haskell_monad c_mbind'' c_kbind''
in
thy
--- a/src/Pure/Tools/nbe.ML Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/nbe.ML Fri Mar 30 16:19:03 2007 +0200
@@ -121,7 +121,9 @@
fun ensure_funs thy funcgr t =
let
- val consts = CodegenConsts.consts_of thy t;
+ fun consts_of thy t =
+ fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t []
+ val consts = consts_of thy t;
val nbe_tab = NBE_Data.get thy;
in
CodegenFuncgr.deps funcgr consts
--- a/src/Pure/Tools/nbe_codegen.ML Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/nbe_codegen.ML Fri Mar 30 16:19:03 2007 +0200
@@ -150,7 +150,8 @@
let
fun to_term bounds (C s) tcount =
let
- val (c, ty) = (CodegenConsts.typ_of_inst thy o the o CodegenNames.const_rev thy) s;
+ val SOME (const as (c, _)) = CodegenNames.const_rev thy s;
+ val ty = CodegenData.default_typ thy const;
val ty' = map_type_tvar (fn ((s,i),S) => TypeInfer.param (tcount + i) (s,S)) ty;
val tcount' = tcount + maxidx_of_typ ty + 1;
in (Const (c, ty'), tcount') end
--- a/src/Pure/Tools/nbe_eval.ML Fri Mar 30 16:19:02 2007 +0200
+++ b/src/Pure/Tools/nbe_eval.ML Fri Mar 30 16:19:03 2007 +0200
@@ -112,7 +112,8 @@
(* ------------------ evaluation with greetings to Tarski ------------------ *)
-fun prep_term thy (Const c) = Const (CodegenNames.const thy (CodegenConsts.norm_of_typ thy c), dummyT)
+fun prep_term thy (Const c) = Const (CodegenNames.const thy
+ (CodegenConsts.const_of_cexpr thy c), dummyT)
| prep_term thy (Free v_ty) = Free v_ty
| prep_term thy (s $ t) = prep_term thy s $ prep_term thy t
| prep_term thy (Abs (raw_v, ty, raw_t)) =