Adapted to modular code generation.
--- a/src/HOL/Tools/datatype_codegen.ML Fri Jul 01 14:11:06 2005 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Fri Jul 01 14:13:40 2005 +0200
@@ -39,7 +39,7 @@
(max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs)
in case xs of [] => NONE | x :: _ => SOME x end;
-fun add_dt_defs thy dep gr (descr: DatatypeAux.descr) =
+fun add_dt_defs thy defs dep gr (descr: DatatypeAux.descr) =
let
val sg = sign_of thy;
val tab = DatatypePackage.get_datatypes thy;
@@ -48,8 +48,8 @@
val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
exists (exists DatatypeAux.is_rec_type o snd) cs) descr');
- val (_, (_, _, (cname, _) :: _)) :: _ = descr';
- val dname = mk_const_id sg cname;
+ val (_, (tname, _, (dname, _) :: _)) :: _ = descr';
+ val thyname = thyname_of_type tname thy;
fun mk_dtdef gr prfx [] = (gr, [])
| mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) =
@@ -59,17 +59,17 @@
val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
val (gr', ps) = foldl_map (fn (gr, (cname, cargs)) =>
apsnd (pair cname) (foldl_map
- (invoke_tycodegen thy dname false) (gr, cargs))) (gr, cs');
+ (invoke_tycodegen thy defs dname thyname false) (gr, cargs))) (gr, cs');
val (gr'', rest) = mk_dtdef gr' "and " xs
in
(gr'',
Pretty.block (Pretty.str prfx ::
(if null tvs then [] else
[mk_tuple (map Pretty.str tvs), Pretty.str " "]) @
- [Pretty.str (mk_type_id sg tname ^ " ="), Pretty.brk 1] @
+ [Pretty.str (mk_type_id sg thyname thyname tname ^ " ="), Pretty.brk 1] @
List.concat (separate [Pretty.brk 1, Pretty.str "| "]
(map (fn (cname, ps') => [Pretty.block
- (Pretty.str (mk_const_id sg cname) ::
+ (Pretty.str (mk_const_id sg thyname thyname cname) ::
(if null ps' then [] else
List.concat ([Pretty.str " of", Pretty.brk 1] ::
separate [Pretty.str " *", Pretty.brk 1]
@@ -89,15 +89,16 @@
let val args = map (fn i =>
Pretty.str ("x" ^ string_of_int i)) (1 upto length Ts)
in (" | ", Pretty.blk (4,
- [Pretty.str prfx, mk_term_of sg false T, Pretty.brk 1,
- if null Ts then Pretty.str (mk_const_id sg cname)
- else parens (Pretty.block [Pretty.str (mk_const_id sg cname),
+ [Pretty.str prfx, mk_term_of thy thyname false T, Pretty.brk 1,
+ if null Ts then Pretty.str (mk_const_id sg thyname thyname cname)
+ else parens (Pretty.block
+ [Pretty.str (mk_const_id sg thyname thyname cname),
Pretty.brk 1, mk_tuple args]),
Pretty.str " =", Pretty.brk 1] @
List.concat (separate [Pretty.str " $", Pretty.brk 1]
([Pretty.str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
mk_type false (Ts ---> T), Pretty.str ")"] ::
- map (fn (x, U) => [Pretty.block [mk_term_of sg false U,
+ map (fn (x, U) => [Pretty.block [mk_term_of thy thyname false U,
Pretty.brk 1, x]]) (args ~~ Ts)))))
end) (prfx, cs')
in eqs @ rest end;
@@ -116,11 +117,11 @@
fun mk_constr s b (cname, dts) =
let
- val gs = map (fn dt => mk_app false (mk_gen sg false rtnames s
+ val gs = map (fn dt => mk_app false (mk_gen thy thyname false rtnames s
(DatatypeAux.typ_of_dtyp descr sorts dt))
[Pretty.str (if b andalso DatatypeAux.is_rec_type dt then "0"
else "j")]) dts;
- val id = mk_const_id sg cname
+ val id = mk_const_id sg thyname thyname cname
in case gs of
_ :: _ :: _ => Pretty.block
[Pretty.str id, Pretty.brk 1, mk_tuple gs]
@@ -135,7 +136,7 @@
[Pretty.str "]"]), Pretty.brk 1, Pretty.str "()"];
val gs = map (Pretty.str o suffix "G" o strip_tname) tvs;
- val gen_name = "gen_" ^ mk_type_id sg tname
+ val gen_name = "gen_" ^ mk_type_id sg thyname thyname tname
in
Pretty.blk (4, separate (Pretty.brk 1)
@@ -173,10 +174,10 @@
handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ =>
let
val gr1 = Graph.add_edge (dname, dep)
- (Graph.new_node (dname, (NONE, "")) gr);
+ (Graph.new_node (dname, (NONE, "", "")) gr);
val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr';
in
- Graph.map_node dname (K (NONE,
+ Graph.map_node dname (K (NONE, thyname,
Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
[Pretty.str ";"])) ^ "\n\n" ^
(if "term_of" mem !mode then
@@ -187,16 +188,16 @@
Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk
(mk_gen_of_def "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
else ""))) gr2
- end)
+ end, thyname)
end;
(**** case expressions ****)
-fun pretty_case thy gr dep brack constrs (c as Const (_, T)) ts =
+fun pretty_case thy defs gr dep thyname brack constrs (c as Const (_, T)) ts =
let val i = length constrs
in if length ts <= i then
- invoke_codegen thy dep brack (gr, eta_expand c ts (i+1))
+ invoke_codegen thy defs dep thyname brack (gr, eta_expand c ts (i+1))
else
let
val ts1 = Library.take (i, ts);
@@ -212,10 +213,10 @@
val xs = variantlist (replicate j "x", names);
val Us' = Library.take (j, fst (strip_type U));
val frees = map Free (xs ~~ Us');
- val (gr0, cp) = invoke_codegen thy dep false
+ val (gr0, cp) = invoke_codegen thy defs dep thyname false
(gr, list_comb (Const (cname, Us' ---> dT), frees));
val t' = Envir.beta_norm (list_comb (t, frees));
- val (gr1, p) = invoke_codegen thy dep false (gr0, t');
+ val (gr1, p) = invoke_codegen thy defs dep thyname false (gr0, t');
val (ps, gr2) = pcase gr1 cs ts Us;
in
([Pretty.block [cp, Pretty.str " =>", Pretty.brk 1, p]] :: ps, gr2)
@@ -223,8 +224,8 @@
val (ps1, gr1) = pcase gr constrs ts1 Ts;
val ps = List.concat (separate [Pretty.brk 1, Pretty.str "| "] ps1);
- val (gr2, p) = invoke_codegen thy dep false (gr1, t);
- val (gr3, ps2) = foldl_map (invoke_codegen thy dep true) (gr2, ts2)
+ val (gr2, p) = invoke_codegen thy defs dep thyname false (gr1, t);
+ val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep thyname true) (gr2, ts2)
in (gr3, (if not (null ts2) andalso brack then parens else I)
(Pretty.block (separate (Pretty.brk 1)
(Pretty.block ([Pretty.str "(case ", p, Pretty.str " of",
@@ -235,14 +236,16 @@
(**** constructors ****)
-fun pretty_constr thy gr dep brack args (c as Const (s, _)) ts =
+fun pretty_constr thy defs gr dep thyname brack args (c as Const (s, T)) ts =
let val i = length args
in if i > 1 andalso length ts < i then
- invoke_codegen thy dep brack (gr, eta_expand c ts i)
+ invoke_codegen thy defs dep thyname brack (gr, eta_expand c ts i)
else
let
- val id = mk_const_id (sign_of thy) s;
- val (gr', ps) = foldl_map (invoke_codegen thy dep (i = 1)) (gr, ts);
+ val thyname' = thyname_of_type (fst (dest_Type (body_type T))) thy;
+ val id = mk_const_id (sign_of thy) thyname thyname' s;
+ val (gr', ps) = foldl_map
+ (invoke_codegen thy defs dep thyname (i = 1)) (gr, ts);
in (case args of
_ :: _ :: _ => (gr', (if brack then parens else I)
(Pretty.block [Pretty.str id, Pretty.brk 1, mk_tuple ps]))
@@ -253,7 +256,7 @@
(**** code generators for terms and types ****)
-fun datatype_codegen thy gr dep brack t = (case strip_comb t of
+fun datatype_codegen thy defs gr dep thyname brack t = (case strip_comb t of
(c as Const (s, T), ts) =>
(case find_first (fn (_, {index, descr, case_name, ...}) =>
s = case_name orelse
@@ -264,28 +267,31 @@
if isSome (get_assoc_code thy s T) then NONE else
let val SOME (_, _, constrs) = assoc (descr, index)
in (case (assoc (constrs, s), strip_type T) of
- (NONE, _) => SOME (pretty_case thy gr dep brack
+ (NONE, _) => SOME (pretty_case thy defs gr dep thyname brack
(#3 (valOf (assoc (descr, index)))) c ts)
- | (SOME args, (_, Type _)) => SOME (pretty_constr thy
- (fst (invoke_tycodegen thy dep false (gr, snd (strip_type T))))
- dep brack args c ts)
+ | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs
+ (fst (invoke_tycodegen thy defs dep thyname false
+ (gr, snd (strip_type T))))
+ dep thyname brack args c ts)
| _ => NONE)
end)
| _ => NONE);
-fun datatype_tycodegen thy gr dep brack (Type (s, Ts)) =
+fun datatype_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
(case Symtab.lookup (DatatypePackage.get_datatypes thy, s) of
NONE => NONE
| SOME {descr, ...} =>
if isSome (get_assoc_type thy s) then NONE else
- let val (gr', ps) = foldl_map
- (invoke_tycodegen thy dep false) (gr, Ts)
- in SOME (add_dt_defs thy dep gr' descr,
+ let
+ val (gr', ps) = foldl_map
+ (invoke_tycodegen thy defs dep thyname false) (gr, Ts);
+ val (gr'', thyname') = add_dt_defs thy defs dep gr' descr
+ in SOME (gr'',
Pretty.block ((if null Ts then [] else
[mk_tuple ps, Pretty.str " "]) @
- [Pretty.str (mk_type_id (sign_of thy) s)]))
+ [Pretty.str (mk_type_id (sign_of thy) thyname thyname' s)]))
end)
- | datatype_tycodegen _ _ _ _ _ = NONE;
+ | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
val setup =
--- a/src/HOL/Tools/inductive_codegen.ML Fri Jul 01 14:11:06 2005 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Jul 01 14:13:40 2005 +0200
@@ -7,7 +7,7 @@
signature INDUCTIVE_CODEGEN =
sig
- val add : theory attribute
+ val add : string option -> theory attribute
val setup : (theory -> theory) list
end;
@@ -22,18 +22,20 @@
(struct
val name = "HOL/inductive_codegen";
type T =
- {intros : thm list Symtab.table,
+ {intros : (thm * string) list Symtab.table,
graph : unit Graph.T,
- eqns : thm list Symtab.table};
+ eqns : (thm * string) list Symtab.table};
val empty =
{intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
val copy = I;
val extend = I;
fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1},
{intros=intros2, graph=graph2, eqns=eqns2}) =
- {intros = Symtab.merge_multi Drule.eq_thm_prop (intros1, intros2),
+ {intros = Symtab.merge_multi (Drule.eq_thm_prop o pairself fst)
+ (intros1, intros2),
graph = Graph.merge (K true) (graph1, graph2),
- eqns = Symtab.merge_multi Drule.eq_thm_prop (eqns1, eqns2)};
+ eqns = Symtab.merge_multi (Drule.eq_thm_prop o pairself fst)
+ (eqns1, eqns2)};
fun print _ _ = ();
end);
@@ -43,15 +45,19 @@
fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
-fun add (p as (thy, thm)) =
- let val {intros, graph, eqns} = CodegenData.get thy;
+fun add optmod (p as (thy, thm)) =
+ let
+ val {intros, graph, eqns} = CodegenData.get thy;
+ fun thyname_of s = (case optmod of
+ NONE => thyname_of_const s thy | SOME s => s);
in (case concl_of thm of
_ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
Const (s, _) =>
let val cs = foldr add_term_consts [] (prems_of thm)
in (CodegenData.put
{intros = Symtab.update ((s,
- getOpt (Symtab.lookup (intros, s), []) @ [thm]), intros),
+ getOpt (Symtab.lookup (intros, s), []) @
+ [(thm, thyname_of s)]), intros),
graph = foldr (uncurry (Graph.add_edge o pair s))
(Library.foldl add_node (graph, s :: cs)) cs,
eqns = eqns} thy, thm)
@@ -61,7 +67,8 @@
Const (s, _) =>
(CodegenData.put {intros = intros, graph = graph,
eqns = Symtab.update ((s,
- getOpt (Symtab.lookup (eqns, s), []) @ [thm]), eqns)} thy, thm)
+ getOpt (Symtab.lookup (eqns, s), []) @
+ [(thm, thyname_of s)]), eqns)} thy, thm)
| _ => (warn thm; p))
| _ => (warn thm; p))
end;
@@ -71,13 +78,17 @@
in case Symtab.lookup (intros, s) of
NONE => (case InductivePackage.get_inductive thy s of
NONE => NONE
- | SOME ({names, ...}, {intrs, ...}) => SOME (names, preprocess thy intrs))
+ | SOME ({names, ...}, {intrs, ...}) =>
+ SOME (names, thyname_of_const s thy,
+ preprocess thy intrs))
| SOME _ =>
- let val SOME names = find_first
- (fn xs => s mem xs) (Graph.strong_conn graph)
- in SOME (names, preprocess thy
- (List.concat (map (fn s => valOf (Symtab.lookup (intros, s))) names)))
- end
+ let
+ val SOME names = find_first
+ (fn xs => s mem xs) (Graph.strong_conn graph);
+ val intrs = List.concat (map
+ (fn s => valOf (Symtab.lookup (intros, s))) names);
+ val (_, (_, thyname)) = split_last intrs
+ in SOME (names, thyname, preprocess thy (map fst intrs)) end
end;
@@ -364,26 +375,30 @@
else [Pretty.str ")"])))
end;
-fun modename thy s (iss, is) = space_implode "__"
- (mk_const_id (sign_of thy) s ::
+fun strip_spaces s = implode (fst (take_suffix (equal " ") (explode s)));
+
+fun modename thy thyname thyname' s (iss, is) = space_implode "__"
+ (mk_const_id (sign_of thy) thyname thyname' (strip_spaces s) ::
map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is]));
-fun compile_expr thy dep brack (gr, (NONE, t)) =
- apsnd single (invoke_codegen thy dep brack (gr, t))
- | compile_expr _ _ _ (gr, (SOME _, Var ((name, _), _))) =
+fun compile_expr thy defs dep thyname brack thynames (gr, (NONE, t)) =
+ apsnd single (invoke_codegen thy defs dep thyname brack (gr, t))
+ | compile_expr _ _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
(gr, [Pretty.str name])
- | compile_expr thy dep brack (gr, (SOME (Mode (mode, ms)), t)) =
+ | compile_expr thy defs dep thyname brack thynames (gr, (SOME (Mode (mode, ms)), t)) =
let
val (Const (name, _), args) = strip_comb t;
val (gr', ps) = foldl_map
- (compile_expr thy dep true) (gr, ms ~~ args);
+ (compile_expr thy defs dep thyname true thynames) (gr, ms ~~ args);
in (gr', (if brack andalso not (null ps) then
single o parens o Pretty.block else I)
(List.concat (separate [Pretty.brk 1]
- ([Pretty.str (modename thy name mode)] :: ps))))
+ ([Pretty.str (modename thy thyname
+ (if name = "op =" then ""
+ else the (assoc (thynames, name))) name mode)] :: ps))))
end;
-fun compile_clause thy gr dep all_vs arg_vs modes (iss, is) (ts, ps) =
+fun compile_clause thy defs gr dep thyname all_vs arg_vs modes thynames (iss, is) (ts, ps) =
let
val modes' = modes @ List.mapPartial
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
@@ -396,7 +411,7 @@
fun compile_eq (gr, (s, t)) =
apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single)
- (invoke_codegen thy dep false (gr, t));
+ (invoke_codegen thy defs dep thyname false (gr, t));
val (in_ts, out_ts) = get_args is 1 ts;
val ((all_vs', eqs), in_ts') =
@@ -409,14 +424,14 @@
fun compile_prems out_ts' vs names gr [] =
let
val (gr2, out_ps) = foldl_map
- (invoke_codegen thy dep false) (gr, out_ts);
+ (invoke_codegen thy defs dep thyname false) (gr, out_ts);
val (gr3, eq_ps) = foldl_map compile_eq (gr2, eqs);
val ((names', eqs'), out_ts'') =
foldl_map check_constrt ((names, []), out_ts');
val (nvs, out_ts''') = foldl_map distinct_v
((names', map (fn x => (x, [x])) vs), out_ts'');
val (gr4, out_ps') = foldl_map
- (invoke_codegen thy dep false) (gr3, out_ts''');
+ (invoke_codegen thy defs dep thyname false) (gr3, out_ts''');
val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs')
in
(gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
@@ -434,7 +449,7 @@
val (nvs, out_ts'') = foldl_map distinct_v
((names', map (fn x => (x, [x])) vs), out_ts');
val (gr0, out_ps) = foldl_map
- (invoke_codegen thy dep false) (gr, out_ts'');
+ (invoke_codegen thy defs dep thyname false) (gr, out_ts'');
val (gr1, eq_ps) = foldl_map compile_eq (gr0, eqs)
in
(case p of
@@ -442,14 +457,15 @@
let
val (in_ts, out_ts''') = get_args js 1 us;
val (gr2, in_ps) = foldl_map
- (invoke_codegen thy dep false) (gr1, in_ts);
+ (invoke_codegen thy defs dep thyname false) (gr1, in_ts);
val (gr3, ps) = if is_ind t then
apsnd (fn ps => ps @ [Pretty.brk 1, mk_tuple in_ps])
- (compile_expr thy dep false (gr2, (mode, t)))
+ (compile_expr thy defs dep thyname false thynames
+ (gr2, (mode, t)))
else
apsnd (fn p => conv_ntuple us t
[Pretty.str "Seq.of_list", Pretty.brk 1, p])
- (invoke_codegen thy dep true (gr2, t));
+ (invoke_codegen thy defs dep thyname true (gr2, t));
val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
in
(gr4, compile_match (snd nvs) eq_ps out_ps
@@ -459,7 +475,7 @@
end
| Sidecond t =>
let
- val (gr2, side_p) = invoke_codegen thy dep true (gr1, t);
+ val (gr2, side_p) = invoke_codegen thy defs dep thyname true (gr1, t);
val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
in
(gr3, compile_match (snd nvs) eq_ps out_ps
@@ -474,22 +490,23 @@
(gr', Pretty.block [Pretty.str "Seq.single inp :->", Pretty.brk 1, prem_p])
end;
-fun compile_pred thy gr dep prfx all_vs arg_vs modes s cls mode =
- let val (gr', cl_ps) = foldl_map (fn (gr, cl) =>
- compile_clause thy gr dep all_vs arg_vs modes mode cl) (gr, cls)
+fun compile_pred thy defs gr dep thyname prfx all_vs arg_vs modes thynames s cls mode =
+ let val (gr', cl_ps) = foldl_map (fn (gr, cl) => compile_clause thy defs
+ gr dep thyname all_vs arg_vs modes thynames mode cl) (gr, cls)
in
((gr', "and "), Pretty.block
([Pretty.block (separate (Pretty.brk 1)
- (Pretty.str (prfx ^ modename thy s mode) :: map Pretty.str arg_vs) @
+ (Pretty.str (prfx ^ modename thy thyname thyname s mode) ::
+ map Pretty.str arg_vs) @
[Pretty.str " inp ="]),
Pretty.brk 1] @
List.concat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps))))
end;
-fun compile_preds thy gr dep all_vs arg_vs modes preds =
+fun compile_preds thy defs gr dep thyname all_vs arg_vs modes thynames preds =
let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) =>
- foldl_map (fn ((gr', prfx'), mode) =>
- compile_pred thy gr' dep prfx' all_vs arg_vs modes s cls mode)
+ foldl_map (fn ((gr', prfx'), mode) => compile_pred thy defs gr'
+ dep thyname prfx' all_vs arg_vs modes thynames s cls mode)
((gr, prfx), valOf (assoc (modes, s)))) ((gr, "fun "), preds)
in
(gr', space_implode "\n\n" (map Pretty.string_of (List.concat prs)) ^ ";\n\n")
@@ -499,11 +516,13 @@
exception Modes of
(string * (int list option list * int list) list) list *
- (string * (int list list option list * int list list)) list;
+ (string * (int list list option list * int list list)) list *
+ string;
-fun lookup_modes gr dep = apfst List.concat (apsnd List.concat (ListPair.unzip
- (map ((fn (SOME (Modes x), _) => x | _ => ([], [])) o Graph.get_node gr)
- (Graph.all_preds gr [dep]))));
+fun lookup_modes gr dep = foldl (fn ((xs, ys, z), (xss, yss, zss)) =>
+ (xss @ xs, yss @ ys, zss @ map (rpair z o fst) ys)) ([], [], [])
+ (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [], "")) o Graph.get_node gr)
+ (Graph.all_preds gr [dep]));
fun print_factors factors = message ("Factors:\n" ^
space_implode "\n" (map (fn (s, (fs, f)) => s ^ ": " ^
@@ -518,18 +537,17 @@
NONE => xs
| SOME xs' => xs inter xs') :: constrain cs ys;
-fun mk_extra_defs thy gr dep names ts =
+fun mk_extra_defs thy defs gr dep names ts =
Library.foldl (fn (gr, name) =>
if name mem names then gr
else (case get_clauses thy name of
NONE => gr
- | SOME (names, intrs) =>
- mk_ind_def thy gr dep names [] [] (prep_intrs intrs)))
+ | SOME (names, thyname, intrs) =>
+ mk_ind_def thy defs gr dep names thyname [] [] (prep_intrs intrs)))
(gr, foldr add_term_consts [] ts)
-and mk_ind_def thy gr dep names modecs factorcs intrs =
- let val ids = map (mk_const_id (sign_of thy)) names
- in Graph.add_edge (hd ids, dep) gr handle Graph.UNDEF _ =>
+and mk_ind_def thy defs gr dep names thyname modecs factorcs intrs =
+ Graph.add_edge (hd names, dep) gr handle Graph.UNDEF _ =>
let
val _ $ (_ $ _ $ u) = Logic.strip_imp_concl (hd intrs);
val (_, args) = strip_comb u;
@@ -565,10 +583,10 @@
else fs
| add_prod_factors _ (fs, _) = fs;
- val gr' = mk_extra_defs thy
- (Graph.add_edge (hd ids, dep)
- (Graph.new_node (hd ids, (NONE, "")) gr)) (hd ids) names intrs;
- val (extra_modes, extra_factors) = lookup_modes gr' (hd ids);
+ val gr' = mk_extra_defs thy defs
+ (Graph.add_edge (hd names, dep)
+ (Graph.new_node (hd names, (NONE, "", "")) gr)) (hd names) names intrs;
+ val (extra_modes, extra_factors, extra_thynames) = lookup_modes gr' (hd names);
val fs = constrain factorcs (map (apsnd dest_factors)
(Library.foldl (add_prod_factors extra_factors) ([], List.concat (map (fn t =>
Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs))));
@@ -581,38 +599,40 @@
(infer_modes thy extra_modes factors arg_vs clauses);
val _ = print_factors factors;
val _ = print_modes modes;
- val (gr'', s) = compile_preds thy gr' (hd ids) (terms_vs intrs) arg_vs
- (modes @ extra_modes) clauses;
+ val (gr'', s) = compile_preds thy defs gr' (hd names) thyname (terms_vs intrs)
+ arg_vs (modes @ extra_modes)
+ (map (rpair thyname o fst) factors @ extra_thynames) clauses;
in
- (Graph.map_node (hd ids) (K (SOME (Modes (modes, factors)), s)) gr'')
- end
- end;
+ (Graph.map_node (hd names)
+ (K (SOME (Modes (modes, factors, thyname)), thyname, s)) gr'')
+ end;
fun find_mode s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
(modes_of modes u handle Option => []) of
NONE => error ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
| mode => mode);
-fun mk_ind_call thy gr dep t u is_query = (case head_of u of
+fun mk_ind_call thy defs gr dep thyname t u is_query = (case head_of u of
Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
(NONE, _) => NONE
- | (SOME (names, intrs), NONE) =>
+ | (SOME (names, thyname', intrs), NONE) =>
let
fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
((ts, mode), i+1)
| mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
- val gr1 = mk_extra_defs thy
- (mk_ind_def thy gr dep names [] [] (prep_intrs intrs)) dep names [u];
- val (modes, factors) = lookup_modes gr1 dep;
+ val gr1 = mk_extra_defs thy defs
+ (mk_ind_def thy defs gr dep names thyname' [] [] (prep_intrs intrs)) dep names [u];
+ val (modes, factors, thynames) = lookup_modes gr1 dep;
val ts = split_prod [] (snd (valOf (assoc (factors, s)))) t;
val (ts', is) = if is_query then
fst (Library.foldl mk_mode ((([], []), 1), ts))
else (ts, 1 upto length ts);
val mode = find_mode s u modes is;
val (gr2, in_ps) = foldl_map
- (invoke_codegen thy dep false) (gr1, ts');
- val (gr3, ps) = compile_expr thy dep false (gr2, (mode, u))
+ (invoke_codegen thy defs dep thyname false) (gr1, ts');
+ val (gr3, ps) =
+ compile_expr thy defs dep thyname false thynames (gr2, (mode, u))
in
SOME (gr3, Pretty.block
(ps @ [Pretty.brk 1, mk_tuple in_ps]))
@@ -620,16 +640,17 @@
| _ => NONE)
| _ => NONE);
-fun list_of_indset thy gr dep brack u = (case head_of u of
+fun list_of_indset thy defs gr dep thyname brack u = (case head_of u of
Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
(NONE, _) => NONE
- | (SOME (names, intrs), NONE) =>
+ | (SOME (names, thyname', intrs), NONE) =>
let
- val gr1 = mk_extra_defs thy
- (mk_ind_def thy gr dep names [] [] (prep_intrs intrs)) dep names [u];
- val (modes, factors) = lookup_modes gr1 dep;
+ val gr1 = mk_extra_defs thy defs
+ (mk_ind_def thy defs gr dep names thyname' [] [] (prep_intrs intrs)) dep names [u];
+ val (modes, factors, thynames) = lookup_modes gr1 dep;
val mode = find_mode s u modes [];
- val (gr2, ps) = compile_expr thy dep false (gr1, (mode, u))
+ val (gr2, ps) =
+ compile_expr thy defs dep thyname false thynames (gr1, (mode, u))
in
SOME (gr2, (if brack then parens else I)
(Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
@@ -650,58 +671,63 @@
in
rename_term
(Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop (HOLogic.mk_mem
- (foldr1 HOLogic.mk_prod (ts @ [u]), Const (Sign.base_name s ^ "_aux",
+ (foldr1 HOLogic.mk_prod (ts @ [u]), Const (s ^ " ",
HOLogic.mk_setT (foldr1 HOLogic.mk_prodT (Ts @ [U])))))))
end;
-fun mk_fun thy name eqns dep gr =
- let val id = mk_const_id (sign_of thy) name
- in Graph.add_edge (id, dep) gr handle Graph.UNDEF _ =>
+fun mk_fun thy defs name eqns dep thyname thyname' gr =
+ let
+ val fun_id = mk_const_id (sign_of thy) thyname' thyname' name;
+ val call_id = mk_const_id (sign_of thy) thyname thyname' name
+ in (Graph.add_edge (name, dep) gr handle Graph.UNDEF _ =>
let
val clauses = map clause_of_eqn eqns;
- val pname = mk_const_id (sign_of thy) (Sign.base_name name ^ "_aux");
+ val pname = name ^ " ";
val arity = length (snd (strip_comb (fst (HOLogic.dest_eq
(HOLogic.dest_Trueprop (concl_of (hd eqns)))))));
val mode = 1 upto arity;
val vars = map (fn i => Pretty.str ("x" ^ string_of_int i)) mode;
val s = Pretty.string_of (Pretty.block
- [mk_app false (Pretty.str ("fun " ^ id)) vars, Pretty.str " =",
+ [mk_app false (Pretty.str ("fun " ^ fun_id)) vars, Pretty.str " =",
Pretty.brk 1, Pretty.str "Seq.hd", Pretty.brk 1,
- parens (Pretty.block [Pretty.str (modename thy pname ([], mode)),
+ parens (Pretty.block [Pretty.str (modename thy thyname' thyname' pname ([], mode)),
Pretty.brk 1, mk_tuple vars])]) ^ ";\n\n";
- val gr' = mk_ind_def thy (Graph.add_edge (id, dep)
- (Graph.new_node (id, (NONE, s)) gr)) id [pname]
+ val gr' = mk_ind_def thy defs (Graph.add_edge (name, dep)
+ (Graph.new_node (name, (NONE, thyname', s)) gr)) name [pname] thyname'
[(pname, [([], mode)])]
[(pname, map (fn i => replicate i 2) (0 upto arity-1))]
clauses;
- val (modes, _) = lookup_modes gr' dep;
+ val (modes, _, _) = lookup_modes gr' dep;
val _ = find_mode pname (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
(Logic.strip_imp_concl (hd clauses))))) modes mode
- in gr' end
+ in gr' end, call_id)
end;
-fun inductive_codegen thy gr dep brack (Const ("op :", _) $ t $ u) =
- ((case mk_ind_call thy gr dep (Term.no_dummy_patterns t) u false of
+fun inductive_codegen thy defs gr dep thyname brack (Const ("op :", _) $ t $ u) =
+ ((case mk_ind_call thy defs gr dep thyname (Term.no_dummy_patterns t) u false of
NONE => NONE
| SOME (gr', call_p) => SOME (gr', (if brack then parens else I)
(Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
- handle TERM _ => mk_ind_call thy gr dep t u true)
- | inductive_codegen thy gr dep brack t = (case strip_comb t of
+ handle TERM _ => mk_ind_call thy defs gr dep thyname t u true)
+ | inductive_codegen thy defs gr dep thyname brack t = (case strip_comb t of
(Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy), s) of
- NONE => list_of_indset thy gr dep brack t
+ NONE => list_of_indset thy defs gr dep thyname brack t
| SOME eqns =>
let
- val gr' = mk_fun thy s (preprocess thy eqns) dep gr
- val (gr'', ps) = foldl_map (invoke_codegen thy dep true) (gr', ts);
- in SOME (gr'', mk_app brack (Pretty.str (mk_const_id
- (sign_of thy) s)) ps)
+ val (_, (_, thyname')) = split_last eqns;
+ val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns))
+ dep thyname thyname' gr;
+ val (gr'', ps) = foldl_map
+ (invoke_codegen thy defs dep thyname true) (gr', ts);
+ in SOME (gr'', mk_app brack (Pretty.str id) ps)
end)
| _ => NONE);
val setup =
[add_codegen "inductive" inductive_codegen,
CodegenData.init,
- add_attribute "ind" (Scan.succeed add)];
+ add_attribute "ind"
+ (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
end;
--- a/src/HOL/Tools/recfun_codegen.ML Fri Jul 01 14:11:06 2005 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Fri Jul 01 14:13:40 2005 +0200
@@ -7,7 +7,8 @@
signature RECFUN_CODEGEN =
sig
- val add: theory attribute
+ val add: string option -> theory attribute
+ val del: theory attribute
val setup: (theory -> theory) list
end;
@@ -19,11 +20,11 @@
structure CodegenData = TheoryDataFun
(struct
val name = "HOL/recfun_codegen";
- type T = thm list Symtab.table;
+ type T = (thm * string option) list Symtab.table;
val empty = Symtab.empty;
val copy = I;
val extend = I;
- fun merge _ = Symtab.merge_multi' Drule.eq_thm_prop;
+ fun merge _ = Symtab.merge_multi' (Drule.eq_thm_prop o pairself fst);
fun print _ _ = ();
end);
@@ -35,14 +36,14 @@
fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
string_of_thm thm);
-fun add (p as (thy, thm)) =
+fun add optmod (p as (thy, thm)) =
let
val tab = CodegenData.get thy;
val (s, _) = const_of (prop_of thm);
in
if Pattern.pattern (lhs_of thm) then
(CodegenData.put (Symtab.update ((s,
- thm :: getOpt (Symtab.lookup (tab, s), [])), tab)) thy, thm)
+ (thm, optmod) :: getOpt (Symtab.lookup (tab, s), [])), tab)) thy, thm)
else (warn thm; p)
end handle TERM _ => (warn thm; p);
@@ -53,7 +54,7 @@
in case Symtab.lookup (tab, s) of
NONE => p
| SOME thms => (CodegenData.put (Symtab.update ((s,
- gen_rem eq_thm (thms, thm)), tab)) thy, thm)
+ gen_rem (eq_thm o apfst fst) (thms, thm)), tab)) thy, thm)
end handle TERM _ => (warn thm; p);
fun del_redundant thy eqs [] = eqs
@@ -61,20 +62,27 @@
let
val tsig = Sign.tsig_of (sign_of thy);
val matches = curry
- (Pattern.matches tsig o pairself lhs_of)
+ (Pattern.matches tsig o pairself (lhs_of o fst))
in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
-fun get_equations thy (s, T) =
+fun get_equations thy defs (s, T) =
(case Symtab.lookup (CodegenData.get thy, s) of
- NONE => []
- | SOME thms => preprocess thy (del_redundant thy []
- (List.filter (fn thm => is_instance thy T
- (snd (const_of (prop_of thm)))) thms)));
+ NONE => ([], "")
+ | SOME thms =>
+ let val thms' = del_redundant thy []
+ (List.filter (fn (thm, _) => is_instance thy T
+ (snd (const_of (prop_of thm)))) thms)
+ in if null thms' then ([], "")
+ else (preprocess thy (map fst thms'),
+ case snd (snd (split_last thms')) of
+ NONE => (case get_defn thy defs s T of
+ NONE => thyname_of_const s thy
+ | SOME ((_, (thyname, _)), _) => thyname)
+ | SOME thyname => thyname)
+ end);
-fun mk_poly_id thy (s, T) = mk_const_id (sign_of thy) s ^
- (case get_defn thy s T of
- SOME (_, SOME i) => "_def" ^ string_of_int i
- | _ => "");
+fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
+ SOME (_, SOME i) => "_def" ^ string_of_int i | _ => "");
exception EQN of string * typ * string;
@@ -82,27 +90,27 @@
if x mem xs then xs
else Library.foldl (cycle g) (x :: xs, List.concat (Graph.find_paths g (x, x)));
-fun add_rec_funs thy gr dep eqs =
+fun add_rec_funs thy defs gr dep eqs thyname =
let
- fun dest_eq t =
- (mk_poly_id thy (const_of t), dest_eqn (rename_term t));
+ fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
+ dest_eqn (rename_term t));
val eqs' = map dest_eq eqs;
val (dname, _) :: _ = eqs';
val (s, T) = const_of (hd eqs);
- fun mk_fundef fname prfx gr [] = (gr, [])
- | mk_fundef fname prfx gr ((fname', (lhs, rhs)) :: xs) =
+ fun mk_fundef thyname fname prfx gr [] = (gr, [])
+ | mk_fundef thyname fname prfx gr ((fname', (lhs, rhs)) :: xs) =
let
- val (gr1, pl) = invoke_codegen thy dname false (gr, lhs);
- val (gr2, pr) = invoke_codegen thy dname false (gr1, rhs);
- val (gr3, rest) = mk_fundef fname' "and " gr2 xs
+ val (gr1, pl) = invoke_codegen thy defs dname thyname false (gr, lhs);
+ val (gr2, pr) = invoke_codegen thy defs dname thyname false (gr1, rhs);
+ val (gr3, rest) = mk_fundef thyname fname' "and " gr2 xs
in
(gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then " | " else prfx),
pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest)
end;
- fun put_code fundef = Graph.map_node dname
- (K (SOME (EQN ("", dummyT, dname)), Pretty.string_of (Pretty.blk (0,
+ fun put_code thyname fundef = Graph.map_node dname
+ (K (SOME (EQN ("", dummyT, dname)), thyname, Pretty.string_of (Pretty.blk (0,
separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n"));
in
@@ -110,43 +118,47 @@
NONE =>
let
val gr1 = Graph.add_edge (dname, dep)
- (Graph.new_node (dname, (SOME (EQN (s, T, "")), "")) gr);
- val (gr2, fundef) = mk_fundef "" "fun " gr1 eqs';
+ (Graph.new_node (dname, (SOME (EQN (s, T, "")), "", "")) gr);
+ val (gr2, fundef) = mk_fundef thyname "" "fun " gr1 eqs';
val xs = cycle gr2 ([], dname);
val cs = map (fn x => case Graph.get_node gr2 x of
- (SOME (EQN (s, T, _)), _) => (s, T)
+ (SOME (EQN (s, T, _)), _, _) => (s, T)
| _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
implode (separate ", " xs))) xs
in (case xs of
- [_] => put_code fundef gr2
+ [_] => put_code thyname fundef gr2
| _ =>
if not (dep mem xs) then
let
- val eqs'' = map (dest_eq o prop_of)
- (List.concat (map (get_equations thy) cs));
- val (gr3, fundef') = mk_fundef "" "fun "
+ val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
+ val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
+ val (gr3, fundef') = mk_fundef thyname "" "fun "
(Graph.add_edge (dname, dep)
(foldr (uncurry Graph.new_node) (Graph.del_nodes xs gr2)
(map (fn k =>
- (k, (SOME (EQN ("", dummyT, dname)), ""))) xs))) eqs''
- in put_code fundef' gr3 end
+ (k, (SOME (EQN ("", dummyT, dname)), thyname, ""))) xs))) eqs''
+ in put_code thyname fundef' gr3 end
else gr2)
end
- | SOME (SOME (EQN (_, _, s)), _) =>
+ | SOME (SOME (EQN (_, _, s)), _, _) =>
if s = "" then
if dname = dep then gr else Graph.add_edge (dname, dep) gr
else if s = dep then gr else Graph.add_edge (s, dep) gr)
end;
-fun recfun_codegen thy gr dep brack t = (case strip_comb t of
- (Const (p as (s, T)), ts) => (case (get_equations thy p, get_assoc_code thy s T) of
- ([], _) => NONE
+fun recfun_codegen thy defs gr dep thyname brack t = (case strip_comb t of
+ (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy s T) of
+ (([], _), _) => NONE
| (_, SOME _) => NONE
- | (eqns, NONE) =>
- let val (gr', ps) = foldl_map (invoke_codegen thy dep true) (gr, ts)
+ | ((eqns, thyname'), NONE) =>
+ let
+ val (gr', ps) = foldl_map
+ (invoke_codegen thy defs dep thyname true) (gr, ts);
+ val suffix = mk_suffix thy defs p
in
- SOME (add_rec_funs thy gr' dep (map prop_of eqns),
- mk_app brack (Pretty.str (mk_poly_id thy p)) ps)
+ SOME (add_rec_funs thy defs gr' dep (map prop_of eqns) thyname',
+ mk_app brack (Pretty.str
+ (mk_const_id (sign_of thy) thyname thyname' s ^ suffix)) ps)
end)
| _ => NONE);
@@ -154,6 +166,8 @@
val setup =
[CodegenData.init,
add_codegen "recfun" recfun_codegen,
- add_attribute "" (Args.del |-- Scan.succeed del || Scan.succeed add)];
+ add_attribute ""
+ ( Args.del |-- Scan.succeed del
+ || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
end;
--- a/src/HOL/Tools/typedef_package.ML Fri Jul 01 14:11:06 2005 +0200
+++ b/src/HOL/Tools/typedef_package.ML Fri Jul 01 14:13:40 2005 +0200
@@ -272,17 +272,18 @@
(** trivial code generator **)
-fun typedef_codegen thy gr dep brack t =
+fun typedef_codegen thy defs gr dep thyname brack t =
let
+ fun get_name (Type (tname, _)) = tname
+ | get_name _ = "";
fun mk_fun s T ts =
let
- val (gr', _) = Codegen.invoke_tycodegen thy dep false (gr, T);
+ val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr, T);
val (gr'', ps) =
- foldl_map (Codegen.invoke_codegen thy dep true) (gr', ts);
- val id = Codegen.mk_const_id thy s
+ foldl_map (Codegen.invoke_codegen thy defs dep thyname true) (gr', ts);
+ val id = Codegen.mk_const_id thy
+ thyname (Codegen.thyname_of_type (get_name T) thy) s
in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
- fun get_name (Type (tname, _)) = tname
- | get_name _ = "";
fun lookup f T = getOpt (Option.map f (Symtab.lookup
(TypedefData.get thy, get_name T)), "")
in
@@ -302,23 +303,25 @@
| mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
| mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
-fun typedef_tycodegen thy gr dep brack (Type (s, Ts)) =
+fun typedef_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
(case Symtab.lookup (TypedefData.get thy, s) of
NONE => NONE
| SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
if isSome (Codegen.get_assoc_type thy tname) then NONE else
let
- val Abs_id = Codegen.mk_const_id thy Abs_name;
- val Rep_id = Codegen.mk_const_id thy Rep_name;
- val ty_id = Codegen.mk_type_id thy s;
+ val thyname' = Codegen.thyname_of_type tname thy;
+ val Abs_id = Codegen.mk_const_id thy thyname' thyname' Abs_name;
+ val Rep_id = Codegen.mk_const_id thy thyname' thyname' Rep_name;
+ val ty_id = Codegen.mk_type_id thy thyname' thyname' s;
+ val ty_call_id = Codegen.mk_type_id thy thyname thyname' s;
val (gr', qs) = foldl_map
- (Codegen.invoke_tycodegen thy dep (length Ts = 1)) (gr, Ts);
- val gr'' = Graph.add_edge (Abs_id, dep) gr' handle Graph.UNDEF _ =>
+ (Codegen.invoke_tycodegen thy defs dep thyname (length Ts = 1)) (gr, Ts);
+ val gr'' = Graph.add_edge (Abs_name, dep) gr' handle Graph.UNDEF _ =>
let
val (gr'', p :: ps) = foldl_map
- (Codegen.invoke_tycodegen thy Abs_id false)
- (Graph.add_edge (Abs_id, dep)
- (Graph.new_node (Abs_id, (NONE, "")) gr'), oldT :: Us);
+ (Codegen.invoke_tycodegen thy defs Abs_name thyname' false)
+ (Graph.add_edge (Abs_name, dep)
+ (Graph.new_node (Abs_name, (NONE, "", "")) gr'), oldT :: Us);
val s =
Pretty.string_of (Pretty.block [Pretty.str "datatype ",
mk_tyexpr ps ty_id,
@@ -329,28 +332,28 @@
Pretty.str "x) = x;"]) ^ "\n\n" ^
(if "term_of" mem !Codegen.mode then
Pretty.string_of (Pretty.block [Pretty.str "fun ",
- Codegen.mk_term_of thy false newT, Pretty.brk 1,
+ Codegen.mk_term_of thy thyname' false newT, Pretty.brk 1,
Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
Pretty.str "x) =", Pretty.brk 1,
Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
- Codegen.mk_term_of thy false oldT, Pretty.brk 1,
+ Codegen.mk_term_of thy thyname' false oldT, Pretty.brk 1,
Pretty.str "x;"]) ^ "\n\n"
else "") ^
(if "test" mem !Codegen.mode then
Pretty.string_of (Pretty.block [Pretty.str "fun ",
- Codegen.mk_gen thy false [] "" newT, Pretty.brk 1,
+ Codegen.mk_gen thy thyname' false [] "" newT, Pretty.brk 1,
Pretty.str "i =", Pretty.brk 1,
Pretty.block [Pretty.str (Abs_id ^ " ("),
- Codegen.mk_gen thy false [] "" oldT, Pretty.brk 1,
+ Codegen.mk_gen thy thyname' false [] "" oldT, Pretty.brk 1,
Pretty.str "i);"]]) ^ "\n\n"
else "")
- in Graph.map_node Abs_id (K (NONE, s)) gr'' end
+ in Graph.map_node Abs_name (K (NONE, thyname', s)) gr'' end
in
- SOME (gr'', mk_tyexpr qs ty_id)
+ SOME (gr'', mk_tyexpr qs ty_call_id)
end)
- | typedef_tycodegen thy gr dep brack _ = NONE;
+ | typedef_tycodegen thy defs gr dep thyname brack _ = NONE;
val setup =
[TypedefData.init,