# HG changeset patch # User berghofe # Date 1120220020 -7200 # Node ID a152d6b21c3174a967c7dcfd5229210ce94b9e35 # Parent 701218c1301cc9156d7a4c851e5eec53baf7199b Adapted to modular code generation. diff -r 701218c1301c -r a152d6b21c31 src/HOL/Tools/datatype_codegen.ML --- 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 = diff -r 701218c1301c -r a152d6b21c31 src/HOL/Tools/inductive_codegen.ML --- 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; diff -r 701218c1301c -r a152d6b21c31 src/HOL/Tools/recfun_codegen.ML --- 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; diff -r 701218c1301c -r a152d6b21c31 src/HOL/Tools/typedef_package.ML --- 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,