--- a/src/Pure/Tools/codegen_func.ML Thu Jan 25 09:32:50 2007 +0100
+++ b/src/Pure/Tools/codegen_func.ML Thu Jan 25 09:32:51 2007 +0100
@@ -2,22 +2,21 @@
ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Handling defining equations ("func"s) for code generator framework.
+Basic handling of defining equations ("func"s) for code generator framework.
*)
signature CODEGEN_FUNC =
sig
- val check_rew: thm -> thm
+ val assert_rew: thm -> thm
val mk_rew: thm -> thm list
- val check_func: thm -> (CodegenConsts.const * thm) option
+ val assert_func: thm -> thm
val mk_func: thm -> (CodegenConsts.const * thm) list
+ val mk_head: thm -> CodegenConsts.const * thm
val dest_func: thm -> (string * typ) * term list
- val mk_head: thm -> CodegenConsts.const * thm
val typ_func: thm -> typ
- val legacy_mk_func: thm -> (CodegenConsts.const * thm) list
+
val expand_eta: int -> thm -> thm
val rewrite_func: thm list -> thm -> thm
- val get_prim_def_funcs: theory -> string * typ list -> thm list
end;
structure CodegenFunc : CODEGEN_FUNC =
@@ -31,7 +30,7 @@
(* making rewrite theorems *)
-fun check_rew thm =
+fun assert_rew thm =
let
val thy = Thm.theory_of_thm thm;
val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm;
@@ -59,7 +58,7 @@
val thy = Thm.theory_of_thm thm;
val thms = (#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy thm;
in
- map check_rew thms
+ map assert_rew thms
end;
@@ -75,7 +74,7 @@
val mk_head = lift_thm_thy (fn thy => fn thm =>
((CodegenConsts.norm_of_typ thy o fst o dest_func) thm, thm));
-fun gen_check_func strict_functyp thm = case try dest_func thm
+fun assert_func thm = case try dest_func thm
of SOME (c_ty as (c, ty), args) =>
let
val thy = Thm.theory_of_thm thm;
@@ -90,35 +89,10 @@
| no_abs (t1 $ t2) = (no_abs t1; no_abs t2)
| no_abs _ = ();
val _ = map no_abs args;
- val is_classop = (is_some o AxClass.class_of_param thy) c;
- val const = CodegenConsts.norm_of_typ thy c_ty;
- 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);
- val error_warning = if strict_functyp
- then error
- else warning #> K NONE
- in if Sign.typ_equiv thy (ty_decl, ty)
- then SOME (const, thm)
- else (if is_classop
- then error_warning
- else if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
- then warning #> (K o SOME) (const, thm)
- else error_warning)
- ("Type\n" ^ string_of_typ ty
- ^ "\nof function theorem\n"
- ^ string_of_thm thm
- ^ "\nis strictly less general than declared function type\n"
- ^ string_of_typ ty_decl)
- end
+ in thm end
| NONE => bad_thm "Not a function equation" thm;
-val check_func = gen_check_func true;
-val legacy_check_func = gen_check_func false;
-
-fun gen_mk_func check_func = map_filter check_func o mk_rew;
-val mk_func = gen_mk_func check_func;
-val legacy_mk_func = gen_mk_func legacy_check_func;
+val mk_func = map (mk_head o assert_func) o mk_rew;
(* utilities *)
@@ -155,31 +129,6 @@
fold (fn refl => fn thm => Thm.combination thm refl) vs_refl thm
end;
-fun get_prim_def_funcs thy c =
- let
- fun constrain thm0 thm = case AxClass.class_of_param thy (fst c)
- of SOME _ =>
- let
- 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 thm;
- val (env, _) = Sign.typ_unify thy (ty_decl, ty) (Vartab.empty, max);
- val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
- cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
- in Thm.instantiate (instT, []) thm end
- | NONE => thm
- in case CodegenConsts.find_def thy c
- of SOME ((_, thm), _) =>
- thm
- |> Thm.transfer thy
- |> try (map snd o mk_func)
- |> these
- |> map (constrain thm)
- |> map (expand_eta ~1)
- | NONE => []
- end;
-
fun rewrite_func rewrites thm =
let
val rewrite = MetaSimplifier.rewrite false rewrites;
--- a/src/Pure/Tools/codegen_funcgr.ML Thu Jan 25 09:32:50 2007 +0100
+++ b/src/Pure/Tools/codegen_funcgr.ML Thu Jan 25 09:32:51 2007 +0100
@@ -2,7 +2,7 @@
ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Retrieving, normalizing and structuring code function theorems
+Retrieving, normalizing and structuring defining equations
in graph with explicit dependencies.
*)
@@ -10,14 +10,16 @@
sig
type T;
val make: theory -> CodegenConsts.const list -> T
+ val make_consts: theory -> CodegenConsts.const list -> CodegenConsts.const list * T
val make_term: theory -> ((thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T
val funcs: T -> CodegenConsts.const -> thm list
val typ: T -> CodegenConsts.const -> typ
val deps: T -> CodegenConsts.const list -> CodegenConsts.const list list
val all: T -> CodegenConsts.const list
- val norm_varnames: theory -> thm list -> thm list
+ val norm_varnames: thm list -> thm list
val print_codethms: theory -> CodegenConsts.const list -> unit
structure Constgraph : GRAPH
+ val timing: bool ref
end;
structure CodegenFuncgr: CODEGEN_FUNCGR =
@@ -48,6 +50,26 @@
val _ = Context.add_setup Funcgr.init;
+(** retrieval **)
+
+fun funcs funcgr =
+ these o Option.map snd o try (Constgraph.get_node funcgr);
+
+fun typ funcgr =
+ fst o Constgraph.get_node funcgr;
+
+fun deps funcgr cs =
+ let
+ val conn = Constgraph.strong_conn funcgr;
+ val order = rev conn;
+ in
+ (map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order
+ |> filter_out null
+ end;
+
+fun all funcgr = Constgraph.keys funcgr;
+
+
(** theorem purification **)
fun norm_args thms =
@@ -104,7 +126,7 @@
val t' = Term.map_abs_vars CodegenNames.purify_var t;
in Thm.rename_boundvars t t' thm end;
-fun norm_varnames thy thms =
+fun norm_varnames thms =
let
fun burrow_thms f [] = []
| burrow_thms f thms =
@@ -122,52 +144,28 @@
end;
-
-(** retrieval **)
-
-fun funcs funcgr =
- these o Option.map snd o try (Constgraph.get_node funcgr);
-
-fun typ funcgr =
- fst o Constgraph.get_node funcgr;
+(** generic combinators **)
-fun deps funcgr cs =
- let
- val conn = Constgraph.strong_conn funcgr;
- val order = rev conn;
- in
- (map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order
- |> filter_out null
- end;
-
-fun all funcgr = Constgraph.keys funcgr;
-
-local
+fun fold_consts f thms =
+ thms
+ |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Drule.plain_prop_of)
+ |> (fold o fold_aterms) (fn Const c => f c | _ => I);
-fun add_things_of thy f (c, thms) =
- (fold o fold_aterms)
- (fn Const c_ty => let
- val c' = CodegenConsts.norm_of_typ thy c_ty
- in if is_some c andalso CodegenConsts.eq_const (the c, c') then I
- else f (c', c_ty) end
- | _ => I) (maps (op :: o swap o apfst (snd o strip_comb)
- o Logic.dest_equals o Drule.plain_prop_of) thms)
+fun consts_of (const, []) = []
+ | consts_of (const, thms as thm :: _) =
+ 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
+ of SOME const => if is_refl const then I else insert CodegenConsts.eq_const const
+ | NONE => I
+ in fold_consts the_const thms [] end;
-fun rhs_of thy (c, thms) =
- Consttab.empty
- |> add_things_of thy (Consttab.update o rpair () o fst) (c, thms)
- |> Consttab.keys;
-
-fun rhs_of' thy (c, thms) =
- add_things_of thy (cons o snd) (c, thms) [];
-
-fun insts_of thy funcgr (c, ty) =
+fun insts_of thy algebra c ty_decl ty =
let
+ val tys_decl = Sign.const_typargs thy (c, ty_decl);
val tys = Sign.const_typargs thy (c, ty);
- val c' = CodegenConsts.norm thy (c, tys);
- val ty_decl = CodegenConsts.disc_typ_of_const thy
- (fst o Constgraph.get_node funcgr o CodegenConsts.norm thy) (c, tys);
- val tys_decl = Sign.const_typargs thy (c, ty_decl);
+ fun classrel (x, _) _ = x;
fun constructor tyco xs class =
(tyco, class) :: maps (maps fst) xs;
fun variable (TVar (_, sort)) = map (pair []) sort
@@ -177,76 +175,24 @@
| mk_inst (Type (tyco1, tys1)) (Type (tyco2, tys2)) =
if tyco1 <> tyco2 then error "bad instance"
else fold2 mk_inst tys1 tys2;
- val pp = Sign.pp thy;
- val algebra = Sign.classes_of thy;
- fun classrel (x, _) _ = x;
fun of_sort_deriv (ty, sort) =
- Sorts.of_sort_derivation pp algebra
+ Sorts.of_sort_derivation (Sign.pp thy) algebra
{ classrel = classrel, constructor = constructor, variable = variable }
(ty, sort)
in
flat (maps of_sort_deriv (fold2 mk_inst tys tys_decl []))
end;
-exception MISSING_INSTANCE of string * string; (*FIXME provide reasonable error tracking*)
-fun all_classops thy tyco class =
- if can (Sign.arity_sorts thy tyco) [class]
- then
- try (AxClass.params_of_class thy) class
- |> Option.map snd
- |> these
- |> map (fn (c, _) => (c, CodegenConsts.disc_typ_of_classop thy (c, [Type (tyco, [])])))
- |> map (CodegenConsts.norm_of_typ thy)
- else raise MISSING_INSTANCE (tyco, class);
+(** graph algorithm **)
-fun instdefs_of thy insts =
- let
- val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
- in
- Symtab.empty
- |> fold (fn (tyco, class) =>
- Symtab.map_default (tyco, []) (insert (op =) class)) insts
- |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classops thy tyco)
- (Graph.all_succs thy_classes classes))) tab [])
- end;
+val timing = ref false;
-fun insts_of_thms thy funcgr (c, thms) =
- let
- val insts = add_things_of thy (fn (_, c_ty) => fold (insert (op =))
- (insts_of thy funcgr c_ty)) (SOME c, thms) [];
- in
- instdefs_of thy insts handle MISSING_INSTANCE (tyco, class) =>
- error ("No such instance: " ^ quote tyco ^ ", " ^ quote class
- ^ "\nin function theorems\n"
- ^ (cat_lines o map string_of_thm) thms)
- end;
+local
-fun ensure_const thy funcgr c auxgr =
- if can (Constgraph.get_node funcgr) c
- then (NONE, auxgr)
- else if can (Constgraph.get_node auxgr) c
- then (SOME c, auxgr)
- else if is_some (CodegenData.get_datatype_of_constr thy c) then
- auxgr
- |> Constgraph.new_node (c, [])
- |> pair (SOME c)
- else let
- val thms = norm_varnames thy (CodegenData.these_funcs thy c);
- val rhs = rhs_of thy (SOME c, thms);
- in
- auxgr
- |> Constgraph.new_node (c, thms)
- |> fold_map (ensure_const thy funcgr) rhs
- |-> (fn rhs' => fold (fn SOME c' => Constgraph.add_edge (c, c')
- | NONE => I) rhs')
- |> pair (SOME c)
- end;
+exception INVALID of CodegenConsts.const list * string;
-exception INVALID of CodegenConsts.const list * string; (*FIXME provide reasonable error tracking*)
-
-(*FIXME: clarify algorithm*)
-fun specialize_typs' thy funcgr eqss =
+fun specialize_typs' thy funcgr funcss =
let
fun max xs = fold (curry Int.max) xs 0;
fun incr_indices (c, thms) maxidx =
@@ -254,11 +200,14 @@
val thms' = map (Thm.incr_indexes (maxidx + 1)) thms;
val maxidx' = max (maxidx :: map Thm.maxidx_of thms');
in ((c, thms'), maxidx') end;
- val (eqss', maxidx) =
- fold_map incr_indices eqss 0;
+ val (funcss', maxidx) =
+ fold_map incr_indices funcss 0;
+ fun typ_of_const (c, ty) = case try (CodegenConsts.norm_of_typ thy) (c, ty)
+ of SOME const => Option.map fst (try (Constgraph.get_node funcgr) const)
+ | NONE => NONE;
fun unify_const (c, ty) (env, maxidx) =
- case try (Constgraph.get_node funcgr) (CodegenConsts.norm_of_typ thy (c, ty))
- of SOME (ty_decl, _) => let
+ case typ_of_const (c, ty)
+ of SOME ty_decl => let
val ty_decl' = Logic.incr_tvar (maxidx + 1) ty_decl;
val maxidx' = max [maxidx, Term.maxidx_of_typ ty_decl'];
in Type.unify (Sign.tsig_of thy) (ty_decl', ty) (env, maxidx')
@@ -267,7 +216,7 @@
^ (Sign.string_of_typ thy o Envir.norm_type env) ty
^ ",\nfor constant " ^ quote c
^ "\nin function theorems\n"
- ^ (cat_lines o maps (map (Sign.string_of_term thy o map_types (Envir.norm_type env) o Thm.prop_of) o snd)) eqss')))
+ ^ (cat_lines o maps (map (Sign.string_of_term thy o map_types (Envir.norm_type env) o Thm.prop_of) o snd)) funcss')))
end
| NONE => (env, maxidx);
fun apply_unifier unif (c, []) = (c, [])
@@ -296,39 +245,126 @@
^ (cat_lines o map string_of_thm) thms))
in (c, thms') end;
val (unif, _) =
- fold (fn (c, thms) => fold unify_const (rhs_of' thy (c, thms)))
- eqss' (Vartab.empty, maxidx);
- val eqss'' = map (apply_unifier unif) eqss';
- in eqss'' end;
+ fold (fn (_, thms) => fold unify_const (fold_consts (insert (op =)) thms []))
+ funcss' (Vartab.empty, maxidx);
+ val funcss'' = map (apply_unifier unif) funcss';
+ in funcss'' end;
fun specialize_typs thy funcgr =
(map o apfst) SOME
#> specialize_typs' thy funcgr
#> (map o apfst) the;
-fun merge_eqsyss thy raw_eqss funcgr =
+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;
+ fun all_classops tyco class =
+ 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)
+ in
+ Symtab.empty
+ |> fold (fn (tyco, class) =>
+ Symtab.map_default (tyco, []) (insert (op =) class)) insts
+ |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classops tyco)
+ (Graph.all_succs thy_classes classes))) tab [])
+ end;
+
+fun instances_of_consts thy algebra funcgr consts =
let
- val eqss = specialize_typs thy funcgr raw_eqss;
- val tys = map (CodegenData.typ_funcs thy) eqss;
- val rhss = map (rhs_of thy o apfst SOME) eqss;
+ 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 => [];
+ in
+ []
+ |> fold (fold (insert (op =)) o inst) consts
+ |> instances_of thy algebra
+ end;
+
+fun ensure_const' thy algebra funcgr const auxgr =
+ if can (Constgraph.get_node funcgr) const
+ then (NONE, auxgr)
+ else if can (Constgraph.get_node auxgr) const
+ then (SOME const, auxgr)
+ else if is_some (CodegenData.get_datatype_of_constr thy const) then
+ auxgr
+ |> Constgraph.new_node (const, [])
+ |> pair (SOME const)
+ else let
+ val thms = norm_varnames (CodegenData.these_funcs thy const);
+ val rhs = consts_of (const, thms);
+ in
+ auxgr
+ |> Constgraph.new_node (const, thms)
+ |> fold_map (ensure_const thy algebra funcgr) rhs
+ |-> (fn rhs' => fold (fn SOME const' => Constgraph.add_edge (const, const')
+ | NONE => I) rhs')
+ |> pair (SOME const)
+ end
+and ensure_const thy algebra funcgr const =
+ let
+ val timeap = if !timing
+ then Output.timeap_msg ("time for " ^ CodegenConsts.string_of_const thy const)
+ else I;
+ in timeap (ensure_const' thy algebra funcgr const) end;
+
+fun merge_funcss thy algebra raw_funcss funcgr =
+ let
+ val funcss = specialize_typs thy funcgr raw_funcss;
+ fun default_typ (const as (c, tys)) = case CodegenData.tap_typ thy const
+ of SOME ty => ty
+ | NONE => let
+ val ty = Sign.the_const_type thy c
+ in case AxClass.class_of_param thy c
+ of SOME class => let
+ val inst = case tys
+ 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
+ | NONE => ty
+ end;
+ fun add_funcs (const, thms as thm :: _) =
+ Constgraph.new_node (const, (CodegenFunc.typ_func thm, thms))
+ | add_funcs (const, []) =
+ Constgraph.new_node (const, (default_typ const, []));
+ val _ = writeln ("constants " ^ (commas o map (CodegenConsts.string_of_const thy o fst)) funcss);
+ val _ = writeln ("funcs " ^ (cat_lines o maps (map string_of_thm o snd)) funcss);
+ fun add_deps (funcs as (const, thms)) funcgr =
+ let
+ val deps = consts_of funcs;
+ val _ = writeln ("constant " ^ CodegenConsts.string_of_const thy const);
+ val insts = instances_of_consts thy algebra funcgr
+ (fold_consts (insert (op =)) thms []);
+ in
+ funcgr
+ |> ensure_consts' thy algebra insts
+ |> fold (curry Constgraph.add_edge const) deps
+ |> fold (curry Constgraph.add_edge const) insts
+ end;
in
funcgr
- |> fold2 (fn (c, thms) => fn ty => Constgraph.new_node (c, (ty, thms))) eqss tys
- |> `(fn funcgr => map (insts_of_thms thy funcgr) eqss)
- |-> (fn rhs_insts => fold2 (fn (c, _) => fn rhs_inst =>
- ensure_consts thy rhs_inst #> fold (curry Constgraph.add_edge c) rhs_inst) eqss rhs_insts)
- |> fold2 (fn (c, _) => fn rhs => fold (curry Constgraph.add_edge c) rhs) eqss rhss
+ |> fold add_funcs funcss
+ |> fold add_deps funcss
end
-and merge_new_eqsyss thy raw_eqss funcgr =
- if exists (member CodegenConsts.eq_const (Constgraph.keys funcgr)) (map fst raw_eqss)
- then funcgr
- else merge_eqsyss thy raw_eqss funcgr
-and ensure_consts thy cs funcgr =
- fold (snd oo ensure_const thy funcgr) cs Constgraph.empty
- |> (fn auxgr => fold (merge_new_eqsyss thy)
+and ensure_consts' thy algebra cs funcgr =
+ fold (snd oo ensure_const thy algebra funcgr) cs Constgraph.empty
+ |> (fn auxgr => fold (merge_funcss thy algebra)
(map (AList.make (Constgraph.get_node auxgr))
(rev (Constgraph.strong_conn auxgr))) funcgr)
- handle INVALID (cs', msg) => raise INVALID (cs @ cs', msg);
+ handle INVALID (cs', msg) => raise INVALID (fold (insert CodegenConsts.eq_const) cs' cs, msg);
fun drop_classes thy tfrees thm =
let
@@ -344,15 +380,31 @@
|> Tactic.rule_by_tactic ((REPEAT o CHANGED o ALLGOALS o Tactic.resolve_tac) (AxClass.class_intros thy))
end;
+fun ensure_consts thy consts funcgr =
+ let
+ val algebra = CodegenData.coregular_algebra thy
+ in ensure_consts' thy algebra consts funcgr
+ handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "
+ ^ commas (map (CodegenConsts.string_of_const thy) cs'))
+ end;
+
in
-val ensure_consts = (fn thy => fn cs => fn funcgr => ensure_consts thy
- cs funcgr handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "
- ^ commas (map (CodegenConsts.string_of_const thy) cs')));
+
+(** graph retrieval **)
fun make thy consts =
Funcgr.change thy (ensure_consts thy consts);
+fun make_consts thy consts =
+ let
+ val algebra = CodegenData.coregular_algebra thy;
+ fun try_const const funcgr =
+ (SOME const, ensure_consts' thy algebra [const] funcgr)
+ handle INVALID (cs', msg) => (NONE, funcgr);
+ val (consts', funcgr) = Funcgr.change_yield thy (fold_map try_const consts);
+ in (map_filter I consts', funcgr) end;
+
fun make_term thy f ct =
let
val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
@@ -376,16 +428,16 @@
val ct'' = Drule.dest_equals_rhs (Thm.cprop_of thm6);
val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') [];
val drop = drop_classes thy tfrees;
- val instdefs = instdefs_of thy (fold (fold (insert (op =)) o insts_of thy funcgr) cs [])
- handle MISSING_INSTANCE (tyco, class) =>
- error ("No such instance: " ^ quote tyco ^ ", " ^ quote class
- ^ "\nwhile prcoessing term\n"
- ^ string_of_cterm ct)
+ val algebra = CodegenData.coregular_algebra thy;
+ val instdefs = instances_of_consts thy algebra funcgr cs;
val funcgr' = ensure_consts thy instdefs funcgr;
in (f drop ct'' thm5, Funcgr.change thy (K funcgr')) end;
end; (*local*)
+
+(** diagnostics **)
+
fun print_funcgr thy funcgr =
AList.make (snd o Constgraph.get_node funcgr) (Constgraph.keys funcgr)
|> (map o apfst) (CodegenConsts.string_of_const thy)
@@ -405,7 +457,7 @@
print_codethms thy (map (CodegenConsts.read_const thy) cs);
-(** Isar **)
+(** Isar setup **)
structure P = OuterParse;
--- a/src/Pure/Tools/codegen_names.ML Thu Jan 25 09:32:50 2007 +0100
+++ b/src/Pure/Tools/codegen_names.ML Thu Jan 25 09:32:51 2007 +0100
@@ -261,7 +261,7 @@
| 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
+ of SOME (thyname, _) => SOME thyname
| NONE => NONE));
fun const_policy thy (c, tys) =
--- a/src/Pure/Tools/codegen_package.ML Thu Jan 25 09:32:50 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML Thu Jan 25 09:32:51 2007 +0100
@@ -112,9 +112,9 @@
fun ensure_def thy = CodegenThingol.ensure_def (CodegenNames.labelled_name thy);
-fun ensure_def_class thy (algbr as ((proj_sort, _), _)) funcgr strct class trns =
+fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr strct class trns =
let
- val superclasses = (proj_sort o Sign.super_classes thy) class;
+ val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
val (v, cs) = AxClass.params_of_class thy class;
val class' = CodegenNames.class thy class;
val classrels' = map (curry (CodegenNames.classrel thy) class) superclasses;
@@ -135,7 +135,7 @@
and ensure_def_classrel thy algbr funcgr strct (subclass, superclass) trns =
trns
|> ensure_def_class thy algbr funcgr strct subclass
- |-> (fn _ => pair (CodegenNames.classrel thy (subclass, superclass)))
+ |>> (fn _ => CodegenNames.classrel thy (subclass, superclass))
and ensure_def_tyco thy algbr funcgr strct tyco trns =
let
fun defgen_datatype trns =
@@ -164,18 +164,18 @@
and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr strct (v, sort) trns =
trns
|> fold_map (ensure_def_class thy algbr funcgr strct) (proj_sort sort)
- |-> (fn sort => pair (unprefix "'" v, sort))
+ |>> (fn sort => (unprefix "'" v, sort))
and exprgen_type thy algbr funcgr strct (TVar _) trns =
error "TVar encountered in typ during code generation"
| exprgen_type thy algbr funcgr strct (TFree vs) trns =
trns
|> exprgen_tyvar_sort thy algbr funcgr strct vs
- |-> (fn (v, sort) => pair (ITyVar v))
+ |>> (fn (v, sort) => ITyVar v)
| exprgen_type thy algbr funcgr strct (Type ("fun", [t1, t2])) trns =
trns
|> exprgen_type thy algbr funcgr strct t1
||>> exprgen_type thy algbr funcgr strct t2
- |-> (fn (t1', t2') => pair (t1' `-> t2'))
+ |>> (fn (t1', t2') => t1' `-> t2')
| exprgen_type thy algbr funcgr strct (Type (tyco, tys)) trns =
case get_abstype thy (tyco, tys)
of SOME ty =>
@@ -185,7 +185,7 @@
trns
|> ensure_def_tyco thy algbr funcgr strct tyco
||>> fold_map (exprgen_type thy algbr funcgr strct) tys
- |-> (fn (tyco, tys) => pair (tyco `%% tys));
+ |>> (fn (tyco, tys) => tyco `%% tys);
exception CONSTRAIN of (string * typ) * typ;
val timing = ref false;
@@ -213,11 +213,11 @@
trns
|> ensure_def_inst thy algbr funcgr strct inst
||>> (fold_map o fold_map) mk_dict yss
- |-> (fn (inst, dss) => pair (DictConst (inst, dss)))
+ |>> (fn (inst, dss) => DictConst (inst, dss))
| mk_dict (Local (classrels, (v, (k, sort)))) trns =
trns
|> fold_map (ensure_def_classrel thy algbr funcgr strct) classrels
- |-> (fn classrels => pair (DictVar (classrels, (unprefix "'" v, (k, length sort)))))
+ |>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
in
trns
|> fold_map mk_dict typargs
@@ -235,40 +235,37 @@
trns
|> fold_map (exprgen_dicts thy algbr funcgr strct) insts
end
-and ensure_def_inst thy (algbr as ((proj_sort, _), _)) funcgr strct (class, tyco) trns =
+and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr strct (class, tyco) trns =
let
- val (vs, classop_defs) = ((apsnd o map) Const o CodegenConsts.instance_dict thy)
- (class, tyco);
- val classops = (map (CodegenConsts.norm_of_typ thy) o snd
- o AxClass.params_of_class thy) class;
- val arity_typ = Type (tyco, (map TFree vs));
- val superclasses = (proj_sort o Sign.super_classes thy) class
+ val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
+ val (var, classops) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
+ val vs = Name.names (Name.declare var Name.context) "'a" (Sorts.mg_domain algebra tyco [class]);
+ val arity_typ = Type (tyco, map TFree vs);
fun gen_superarity superclass trns =
trns
|> ensure_def_class thy algbr funcgr strct superclass
||>> ensure_def_classrel thy algbr funcgr strct (class, superclass)
||>> exprgen_dicts thy algbr funcgr strct (arity_typ, [superclass])
- |-> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
- pair (superclass, (classrel, (inst, dss))));
- fun gen_classop_def (classop, t) trns =
+ |>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
+ (superclass, (classrel, (inst, dss))));
+ fun gen_classop_def (classop as (c, ty)) trns =
trns
- |> ensure_def_const thy algbr funcgr strct classop
- ||>> exprgen_term thy algbr funcgr strct t;
+ |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy classop)
+ ||>> exprgen_term thy algbr funcgr strct (Const (c, map_type_tfree (K arity_typ) ty));
fun defgen_inst trns =
trns
|> ensure_def_class thy algbr funcgr strct class
||>> ensure_def_tyco thy algbr funcgr strct tyco
||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
||>> fold_map gen_superarity superclasses
- ||>> fold_map gen_classop_def (classops ~~ classop_defs)
+ ||>> fold_map gen_classop_def classops
|-> (fn ((((class, tyco), arity), superarities), classops) =>
succeed (CodegenThingol.Classinst ((class, (tyco, arity)), (superarities, classops))));
val inst = CodegenNames.instance thy (class, tyco);
in
trns
|> tracing (fn _ => "generating instance " ^ quote class ^ " / " ^ quote tyco)
- |> ensure_def thy defgen_inst true
- ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
+ |> 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 =
@@ -334,7 +331,7 @@
| exprgen_term thy algbr funcgr strct (Free (v, ty)) trns =
trns
|> exprgen_type thy algbr funcgr strct ty
- |-> (fn _ => pair (IVar v))
+ |>> (fn _ => IVar v)
| exprgen_term thy algbr funcgr strct (Abs (raw_v, ty, raw_t)) trns =
let
val (v, t) = Syntax.variant_abs (raw_v, ty, raw_t);
@@ -342,27 +339,25 @@
trns
|> exprgen_type thy algbr funcgr strct ty
||>> exprgen_term thy algbr funcgr strct t
- |-> (fn (ty, t) => pair ((v, ty) `|-> t))
+ |>> (fn (ty, t) => (v, ty) `|-> t)
end
| exprgen_term thy algbr funcgr strct (t as _ $ _) trns =
case strip_comb t
of (Const (c, ty), ts) =>
trns
|> select_appgen thy algbr funcgr strct ((c, ty), ts)
- |-> (fn t => pair t)
| (t', ts) =>
trns
|> exprgen_term thy algbr funcgr strct t'
||>> fold_map (exprgen_term thy algbr funcgr strct) ts
- |-> (fn (t, ts) => pair (t `$$ ts))
+ |>> (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))
||>> exprgen_type thy algbr funcgr strct ty
||>> exprgen_dict_parms thy algbr funcgr strct (c, ty)
||>> fold_map (exprgen_term thy algbr funcgr strct) ts
- |-> (fn (((c, ty), iss), ts) =>
- pair (IConst (c, (iss, ty)) `$$ ts))
+ |>> (fn (((c, ty), iss), ts) => IConst (c, (iss, ty)) `$$ ts)
and select_appgen thy algbr funcgr strct ((c, ty), ts) trns =
case Symtab.lookup (fst (CodegenPackageData.get thy)) c
of SOME (i, (appgen, _)) =>
@@ -377,13 +372,13 @@
trns
|> fold_map (exprgen_type thy algbr funcgr strct) tys
||>> appgen thy algbr funcgr strct ((c, ty), ts @ map Free vs)
- |-> (fn (tys, t) => pair (map2 (fn (v, _) => pair v) vs tys `|--> t))
+ |>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
end
else if length ts > i then
trns
|> appgen thy algbr funcgr strct ((c, ty), Library.take (i, ts))
||>> fold_map (exprgen_term thy algbr funcgr strct) (Library.drop (i, ts))
- |-> (fn (t, ts) => pair (t `$$ ts))
+ |>> (fn (t, ts) => t `$$ ts)
else
trns
|> appgen thy algbr funcgr strct ((c, ty), ts)
@@ -401,6 +396,12 @@
^ Sign.string_of_typ thy ty
^ "\noccurs with type\n"
^ Sign.string_of_typ thy ty_decl);
+
+fun perhaps_def_const thy algbr funcgr strct c trns =
+ case try (ensure_def_const thy algbr funcgr strct c) trns
+ of SOME (c, trns) => (SOME c, trns)
+ | NONE => (NONE, trns);
+
fun exprgen_term' thy algbr funcgr strct t trns =
exprgen_term thy algbr funcgr strct t trns
handle CONSTRAIN ((c, ty), ty_decl) => error ("In term " ^ (quote o Sign.string_of_term thy) t
@@ -427,7 +428,7 @@
of SOME i =>
trns
|> exprgen_type thy algbr funcgr strct ty
- |-> (fn _ => pair (IChar (chr i)))
+ |>> (fn _ => IChar (chr i))
| NONE =>
trns
|> appgen_default thy algbr funcgr strct app;
@@ -446,7 +447,7 @@
|> exprgen_term thy algbr funcgr strct st
||>> exprgen_type thy algbr funcgr strct sty
||>> fold_map clausegen ds
- |-> (fn ((se, sty), ds) => pair (ICase ((se, sty), ds)))
+ |>> (fn ((se, sty), ds) => ICase ((se, sty), ds))
end;
fun appgen_let thy algbr funcgr strct (app as (_, [st, ct])) trns =
@@ -554,20 +555,7 @@
(* generic generation combinators *)
-fun operational_algebra thy =
- let
- fun add_iff_operational class classes =
- if (not o null o these o Option.map #params o try (AxClass.get_definition thy)) class
- orelse (length o gen_inter (op =))
- ((Sign.certify_sort thy o Sign.super_classes thy) class, classes) >= 2
- then class :: classes
- else classes;
- val operational_classes = fold add_iff_operational (Sign.all_classes thy) [];
- in
- Sorts.subalgebra (Sign.pp thy) (member (op =) operational_classes) (Sign.classes_of thy)
- end;
-
-fun generate thy funcgr targets init gen it =
+fun generate thy funcgr targets gen it =
let
val cs = map_filter (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy))
(CodegenFuncgr.all funcgr);
@@ -577,9 +565,9 @@
|> fold (fn c => Consts.declare qnaming
((CodegenNames.const thy c, CodegenFuncgr.typ funcgr' c), true))
(CodegenFuncgr.all funcgr');
- val algbr = (operational_algebra thy, consttab);
+ val algbr = (CodegenData.operational_algebra thy, consttab);
in
- Code.change_yield thy (CodegenThingol.start_transact init (gen thy algbr funcgr'
+ Code.change_yield thy (CodegenThingol.start_transact (gen thy algbr funcgr'
(true, targets) it))
|> fst
end;
@@ -589,7 +577,7 @@
val ct = Thm.cterm_of thy t;
val (ct', funcgr) = CodegenFuncgr.make_term thy (K K) ct;
val t' = Thm.term_of ct';
- in generate thy funcgr (SOME []) NONE exprgen_term' t' end;
+ in generate thy funcgr (SOME []) exprgen_term' t' end;
fun eval_term thy (ref_spec, t) =
let
@@ -617,18 +605,17 @@
| SOME thyname => filter (is_const thyname) consts
end;
-fun filter_generatable thy consts =
+fun filter_generatable thy targets consts =
let
- fun generatable const =
- case try (CodegenFuncgr.make thy) [const]
- of SOME funcgr => can
- (generate thy funcgr NONE NONE (fold_map oooo ensure_def_const')) [const]
- | NONE => false;
- in filter generatable consts end;
+ val (consts', funcgr) = CodegenFuncgr.make_consts thy consts;
+ val consts'' = generate thy funcgr targets (fold_map oooo perhaps_def_const) consts';
+ val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE)
+ (consts' ~~ consts'');
+ in consts''' end;
-fun read_constspec thy "*" = filter_generatable thy (consts_of thy NONE)
- | read_constspec thy s = if String.isSuffix ".*" s
- then filter_generatable thy (consts_of thy (SOME (unsuffix ".*" s)))
+fun read_constspec thy targets "*" = filter_generatable thy targets (consts_of thy NONE)
+ | read_constspec thy targets s = if String.isSuffix ".*" s
+ then filter_generatable thy targets (consts_of thy (SOME (unsuffix ".*" s)))
else [CodegenConsts.read_const thy s];
@@ -641,16 +628,16 @@
fun code raw_cs seris thy =
let
- val cs = maps (read_constspec thy) raw_cs;
- (*FIXME: assert serializer*)
val seris' = map (fn (target, args as _ :: _) =>
(target, SOME (CodegenSerializer.get_serializer thy target args))
| (target, []) => (CodegenSerializer.assert_serializer thy target, NONE)) seris;
+ val targets = case map fst seris' of [] => NONE | xs => SOME xs;
+ val cs = maps (read_constspec thy targets) raw_cs;
fun generate' thy = case cs
of [] => []
| _ =>
- generate thy (CodegenFuncgr.make thy cs) (case map fst seris' of [] => NONE | xs => SOME xs)
- NONE (fold_map oooo ensure_def_const') cs;
+ generate thy (CodegenFuncgr.make thy cs) targets
+ (fold_map oooo ensure_def_const') cs;
fun serialize' [] code seri =
seri NONE code
| serialize' cs code seri =
--- a/src/Pure/Tools/codegen_thingol.ML Thu Jan 25 09:32:50 2007 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Thu Jan 25 09:32:51 2007 +0100
@@ -82,7 +82,7 @@
val succeed: 'a -> transact -> 'a * code;
val fail: string -> transact -> 'a * code;
val message: string -> (transact -> 'a) -> transact -> 'a;
- val start_transact: string option -> (transact -> 'a * transact) -> code -> 'a * code;
+ val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
val trace: bool ref;
val tracing: ('a -> string) -> 'a -> 'a;
@@ -344,7 +344,7 @@
| check_prep_def code (d as Datatype _) =
d
| check_prep_def code (Datatypecons dtco) =
- error "Attempted to add bare datatype constructor"
+ error "Attempted to add bare term constructor"
| check_prep_def code (d as Class _) =
d
| check_prep_def code (Classop _) =
@@ -438,16 +438,14 @@
f trns handle FAIL msgs =>
raise FAIL (msg :: msgs);
-fun start_transact init f code =
+fun start_transact f code =
let
fun handle_fail f x =
(f x
handle FAIL msgs =>
(error o cat_lines) ("Code generation failed, while:" :: msgs))
in
- code
- |> (if is_some init then ensure_bot (the init) else I)
- |> pair init
+ (NONE, code)
|> handle_fail f
|-> (fn x => fn (_, code) => (x, code))
end;