# HG changeset patch # User berghofe # Date 1124979016 -7200 # Node ID 6642e0f96f44b6ed1d11b7fdab1706cf247c3ce1 # Parent 2a8111863b16b15249e7ee5cdb78c2e585952feb Implemented incremental code generation. diff -r 2a8111863b16 -r 6642e0f96f44 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Thu Aug 25 09:29:05 2005 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Thu Aug 25 16:10:16 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 defs dep gr (descr: DatatypeAux.descr) = +fun add_dt_defs thy defs dep module gr (descr: DatatypeAux.descr) = let val sg = sign_of thy; val tab = DatatypePackage.get_datatypes thy; @@ -48,8 +48,9 @@ val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => exists (exists DatatypeAux.is_rec_type o snd) cs) descr'); - val (_, (tname, _, (dname, _) :: _)) :: _ = descr'; - val thyname = thyname_of_type tname thy; + val (_, (tname, _, _)) :: _ = descr'; + val node_id = tname ^ " (type)"; + val module' = if_library (thyname_of_type tname thy) module; fun mk_dtdef gr prfx [] = (gr, []) | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) = @@ -57,54 +58,57 @@ val tvs = map DatatypeAux.dest_DtTFree dts; val sorts = map (rpair []) tvs; 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 defs dname thyname false) (gr, cargs))) (gr, cs'); - val (gr'', rest) = mk_dtdef gr' "and " xs + val (gr', (_, type_id)) = mk_type_id module' tname gr; + val (gr'', ps) = + foldl_map (fn (gr, (cname, cargs)) => + foldl_map (invoke_tycodegen thy defs node_id module' false) + (gr, cargs) |>>> + mk_const_id module' cname) (gr', cs'); + val (gr''', rest) = mk_dtdef gr'' "and " xs in - (gr'', + (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 thyname thyname tname ^ " ="), Pretty.brk 1] @ + [Pretty.str (type_id ^ " ="), Pretty.brk 1] @ List.concat (separate [Pretty.brk 1, Pretty.str "| "] - (map (fn (cname, ps') => [Pretty.block - (Pretty.str (mk_const_id sg thyname thyname cname) :: + (map (fn (ps', (_, cname)) => [Pretty.block + (Pretty.str cname :: (if null ps' then [] else List.concat ([Pretty.str " of", Pretty.brk 1] :: separate [Pretty.str " *", Pretty.brk 1] (map single ps'))))]) ps))) :: rest) end; - fun mk_term_of_def prfx [] = [] - | mk_term_of_def prfx ((_, (tname, dts, cs)) :: xs) = + fun mk_term_of_def gr prfx [] = [] + | mk_term_of_def gr prfx ((_, (tname, dts, cs)) :: xs) = let val tvs = map DatatypeAux.dest_DtTFree dts; val sorts = map (rpair []) tvs; val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs; val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts; val T = Type (tname, dts'); - val rest = mk_term_of_def "and " xs; + val rest = mk_term_of_def gr "and " xs; val (_, eqs) = foldl_map (fn (prfx, (cname, Ts)) => 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 thy thyname false T, Pretty.brk 1, - if null Ts then Pretty.str (mk_const_id sg thyname thyname cname) + [Pretty.str prfx, mk_term_of gr module' false T, Pretty.brk 1, + if null Ts then Pretty.str (snd (get_const_id cname gr)) else parens (Pretty.block - [Pretty.str (mk_const_id sg thyname thyname cname), + [Pretty.str (snd (get_const_id cname gr)), 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 thy thyname false U, + map (fn (x, U) => [Pretty.block [mk_term_of gr module' false U, Pretty.brk 1, x]]) (args ~~ Ts))))) end) (prfx, cs') in eqs @ rest end; - fun mk_gen_of_def prfx [] = [] - | mk_gen_of_def prfx ((i, (tname, dts, cs)) :: xs) = + fun mk_gen_of_def gr prfx [] = [] + | mk_gen_of_def gr prfx ((i, (tname, dts, cs)) :: xs) = let val tvs = map DatatypeAux.dest_DtTFree dts; val sorts = map (rpair []) tvs; @@ -117,11 +121,11 @@ fun mk_constr s b (cname, dts) = let - val gs = map (fn dt => mk_app false (mk_gen thy thyname false rtnames s + val gs = map (fn dt => mk_app false (mk_gen gr module' 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 thyname thyname cname + val (_, id) = get_const_id cname gr in case gs of _ :: _ :: _ => Pretty.block [Pretty.str id, Pretty.brk 1, mk_tuple gs] @@ -136,7 +140,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 thyname thyname tname + val gen_name = "gen_" ^ snd (get_type_id tname gr) in Pretty.blk (4, separate (Pretty.brk 1) @@ -166,38 +170,38 @@ [Pretty.str " =", Pretty.brk 1] @ separate (Pretty.brk 1) (Pretty.str (gen_name ^ "'") :: gs @ [Pretty.str "i", Pretty.str "i"]))]) @ - mk_gen_of_def "and " xs + mk_gen_of_def gr "and " xs end in - ((Graph.add_edge_acyclic (dname, dep) gr + (add_edge_acyclic (node_id, dep) gr handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ => let - val gr1 = Graph.add_edge (dname, dep) - (Graph.new_node (dname, (NONE, "", "")) gr); + val gr1 = add_edge (node_id, dep) + (new_node (node_id, (NONE, "", "")) gr); val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr'; in - Graph.map_node dname (K (NONE, thyname, + map_node node_id (K (NONE, module', Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @ [Pretty.str ";"])) ^ "\n\n" ^ (if "term_of" mem !mode then Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk - (mk_term_of_def "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" + (mk_term_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" else "") ^ (if "test" mem !mode then Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk - (mk_gen_of_def "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" + (mk_gen_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" else ""))) gr2 - end, thyname) + end end; (**** case expressions ****) -fun pretty_case thy defs gr dep thyname brack constrs (c as Const (_, T)) ts = +fun pretty_case thy defs gr dep module brack constrs (c as Const (_, T)) ts = let val i = length constrs in if length ts <= i then - invoke_codegen thy defs dep thyname brack (gr, eta_expand c ts (i+1)) + invoke_codegen thy defs dep module brack (gr, eta_expand c ts (i+1)) else let val ts1 = Library.take (i, ts); @@ -213,10 +217,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 defs dep thyname false + val (gr0, cp) = invoke_codegen thy defs dep module false (gr, list_comb (Const (cname, Us' ---> dT), frees)); val t' = Envir.beta_norm (list_comb (t, frees)); - val (gr1, p) = invoke_codegen thy defs dep thyname false (gr0, t'); + val (gr1, p) = invoke_codegen thy defs dep module false (gr0, t'); val (ps, gr2) = pcase gr1 cs ts Us; in ([Pretty.block [cp, Pretty.str " =>", Pretty.brk 1, p]] :: ps, gr2) @@ -224,8 +228,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 defs dep thyname false (gr1, t); - val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep thyname true) (gr2, ts2) + val (gr2, p) = invoke_codegen thy defs dep module false (gr1, t); + val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep module 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", @@ -236,16 +240,15 @@ (**** constructors ****) -fun pretty_constr thy defs gr dep thyname brack args (c as Const (s, T)) ts = +fun pretty_constr thy defs gr dep module 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 defs dep thyname brack (gr, eta_expand c ts i) + invoke_codegen thy defs dep module brack (gr, eta_expand c ts i) else let - val thyname' = thyname_of_type (fst (dest_Type (body_type T))) thy; - val id = mk_const_id (sign_of thy) thyname thyname' s; + val id = mk_qual_id module (get_const_id s gr); val (gr', ps) = foldl_map - (invoke_codegen thy defs dep thyname (i = 1)) (gr, ts); + (invoke_codegen thy defs dep module (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])) @@ -256,7 +259,7 @@ (**** code generators for terms and types ****) -fun datatype_codegen thy defs gr dep thyname brack t = (case strip_comb t of +fun datatype_codegen thy defs gr dep module 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 @@ -267,29 +270,29 @@ 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 defs gr dep thyname brack + (NONE, _) => SOME (pretty_case thy defs gr dep module brack (#3 (valOf (assoc (descr, index)))) c ts) | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs - (fst (invoke_tycodegen thy defs dep thyname false + (fst (invoke_tycodegen thy defs dep module false (gr, snd (strip_type T)))) - dep thyname brack args c ts) + dep module brack args c ts) | _ => NONE) end) | _ => NONE); -fun datatype_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) = +fun datatype_tycodegen thy defs gr dep module 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 defs dep thyname false) (gr, Ts); - val (gr'', thyname') = add_dt_defs thy defs dep gr' descr + (invoke_tycodegen thy defs dep module false) (gr, Ts); + val gr'' = add_dt_defs thy defs dep module 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) thyname thyname' s)])) + [Pretty.str (mk_qual_id module (get_type_id s gr''))])) end) | datatype_tycodegen _ _ _ _ _ _ _ = NONE; diff -r 2a8111863b16 -r 6642e0f96f44 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Thu Aug 25 09:29:05 2005 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Thu Aug 25 16:10:16 2005 +0200 @@ -375,30 +375,31 @@ else [Pretty.str ")"]))) end; -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 modename module s (iss, is) gr = + let val (gr', id) = if s = "op =" then (gr, ("", "equal")) + else mk_const_id module s gr + in (gr', space_implode "__" + (mk_qual_id module id :: + map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is]))) + end; -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, _), _))) = +fun compile_expr thy defs dep module brack (gr, (NONE, t)) = + apsnd single (invoke_codegen thy defs dep module brack (gr, t)) + | compile_expr _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) = (gr, [Pretty.str name]) - | compile_expr thy defs dep thyname brack thynames (gr, (SOME (Mode (mode, ms)), t)) = + | compile_expr thy defs dep module brack (gr, (SOME (Mode (mode, ms)), t)) = let val (Const (name, _), args) = strip_comb t; - val (gr', ps) = foldl_map - (compile_expr thy defs dep thyname true thynames) (gr, ms ~~ args); + val (gr', (ps, mode_id)) = foldl_map + (compile_expr thy defs dep module true) (gr, ms ~~ args) |>>> + modename module name mode; 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 thyname - (if name = "op =" then "" - else the (assoc (thynames, name))) name mode)] :: ps)))) + ([Pretty.str mode_id] :: ps)))) end; -fun compile_clause thy defs gr dep thyname all_vs arg_vs modes thynames (iss, is) (ts, ps) = +fun compile_clause thy defs gr dep module all_vs arg_vs modes (iss, is) (ts, ps) = let val modes' = modes @ List.mapPartial (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)])) @@ -411,7 +412,7 @@ fun compile_eq (gr, (s, t)) = apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single) - (invoke_codegen thy defs dep thyname false (gr, t)); + (invoke_codegen thy defs dep module false (gr, t)); val (in_ts, out_ts) = get_args is 1 ts; val ((all_vs', eqs), in_ts') = @@ -424,14 +425,14 @@ fun compile_prems out_ts' vs names gr [] = let val (gr2, out_ps) = foldl_map - (invoke_codegen thy defs dep thyname false) (gr, out_ts); + (invoke_codegen thy defs dep module 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 defs dep thyname false) (gr3, out_ts'''); + (invoke_codegen thy defs dep module 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' @@ -449,7 +450,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 defs dep thyname false) (gr, out_ts''); + (invoke_codegen thy defs dep module false) (gr, out_ts''); val (gr1, eq_ps) = foldl_map compile_eq (gr0, eqs) in (case p of @@ -457,15 +458,15 @@ let val (in_ts, out_ts''') = get_args js 1 us; val (gr2, in_ps) = foldl_map - (invoke_codegen thy defs dep thyname false) (gr1, in_ts); + (invoke_codegen thy defs dep module 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 defs dep thyname false thynames + (compile_expr thy defs dep module false (gr2, (mode, t))) else apsnd (fn p => conv_ntuple us t [Pretty.str "Seq.of_list", Pretty.brk 1, p]) - (invoke_codegen thy defs dep thyname true (gr2, t)); + (invoke_codegen thy defs dep module 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 @@ -475,7 +476,7 @@ end | Sidecond t => let - val (gr2, side_p) = invoke_codegen thy defs dep thyname true (gr1, t); + val (gr2, side_p) = invoke_codegen thy defs dep module true (gr1, t); val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps'; in (gr3, compile_match (snd nvs) eq_ps out_ps @@ -490,23 +491,25 @@ (gr', Pretty.block [Pretty.str "Seq.single inp :->", Pretty.brk 1, prem_p]) end; -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) +fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode = + let val (gr', (cl_ps, mode_id)) = + foldl_map (fn (gr, cl) => compile_clause thy defs + gr dep module all_vs arg_vs modes mode cl) (gr, cls) |>>> + modename module s mode in ((gr', "and "), Pretty.block ([Pretty.block (separate (Pretty.brk 1) - (Pretty.str (prfx ^ modename thy thyname thyname s mode) :: + (Pretty.str (prfx ^ mode_id) :: 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 defs gr dep thyname all_vs arg_vs modes thynames preds = +fun compile_preds thy defs gr dep module all_vs arg_vs modes preds = let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) => foldl_map (fn ((gr', prfx'), mode) => compile_pred thy defs gr' - dep thyname prfx' all_vs arg_vs modes thynames s cls mode) + dep module prfx' all_vs arg_vs modes 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") @@ -516,13 +519,11 @@ exception Modes of (string * (int list option list * int list) list) list * - (string * (int list list option list * int list list)) list * - string; + (string * (int list list option list * int list list)) list; -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 lookup_modes gr dep = apfst List.concat (apsnd List.concat (ListPair.unzip + (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o get_node gr) + (Graph.all_preds (fst gr) [dep])))); fun print_factors factors = message ("Factors:\n" ^ space_implode "\n" (map (fn (s, (fs, f)) => s ^ ": " ^ @@ -537,17 +538,18 @@ NONE => xs | SOME xs' => xs inter xs') :: constrain cs ys; -fun mk_extra_defs thy defs gr dep names ts = +fun mk_extra_defs thy defs gr dep names module ts = Library.foldl (fn (gr, name) => if name mem names then gr else (case get_clauses thy name of NONE => gr | SOME (names, thyname, intrs) => - mk_ind_def thy defs gr dep names thyname [] [] (prep_intrs intrs))) + mk_ind_def thy defs gr dep names (if_library thyname module) + [] [] (prep_intrs intrs))) (gr, foldr add_term_consts [] ts) -and mk_ind_def thy defs gr dep names thyname modecs factorcs intrs = - Graph.add_edge (hd names, dep) gr handle Graph.UNDEF _ => +and mk_ind_def thy defs gr dep names module modecs factorcs intrs = + add_edge (hd names, dep) gr handle Graph.UNDEF _ => let val _ $ (_ $ _ $ u) = Logic.strip_imp_concl (hd intrs); val (_, args) = strip_comb u; @@ -584,9 +586,9 @@ | add_prod_factors _ (fs, _) = fs; 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); + (add_edge (hd names, dep) + (new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs; + val (extra_modes, extra_factors) = 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)))); @@ -599,40 +601,42 @@ (infer_modes thy extra_modes factors arg_vs clauses); val _ = print_factors factors; val _ = print_modes modes; - 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; + val (gr'', s) = compile_preds thy defs gr' (hd names) module (terms_vs intrs) + arg_vs (modes @ extra_modes) clauses; in - (Graph.map_node (hd names) - (K (SOME (Modes (modes, factors, thyname)), thyname, s)) gr'') + (map_node (hd names) + (K (SOME (Modes (modes, factors)), module, s)) gr'') end; -fun find_mode s u modes is = (case find_first (fn Mode ((_, js), _) => is=js) +fun find_mode gr dep 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)) + NONE => codegen_error gr dep + ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is)) | mode => mode); -fun mk_ind_call thy defs gr dep thyname t u is_query = (case head_of u of +fun mk_ind_call thy defs gr dep module 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, thyname', 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 module' = if_library thyname module; 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; + (mk_ind_def thy defs gr dep names module' + [] [] (prep_intrs intrs)) dep names module' [u]; + val (modes, factors) = 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 mode = find_mode gr1 dep s u modes is; val (gr2, in_ps) = foldl_map - (invoke_codegen thy defs dep thyname false) (gr1, ts'); + (invoke_codegen thy defs dep module false) (gr1, ts'); val (gr3, ps) = - compile_expr thy defs dep thyname false thynames (gr2, (mode, u)) + compile_expr thy defs dep module false (gr2, (mode, u)) in SOME (gr3, Pretty.block (ps @ [Pretty.brk 1, mk_tuple in_ps])) @@ -640,17 +644,19 @@ | _ => NONE) | _ => NONE); -fun list_of_indset thy defs gr dep thyname brack u = (case head_of u of +fun list_of_indset thy defs gr dep module 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, thyname', intrs), NONE) => + | (SOME (names, thyname, intrs), NONE) => let + val module' = if_library thyname module; 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 []; + (mk_ind_def thy defs gr dep names module' + [] [] (prep_intrs intrs)) dep names module' [u]; + val (modes, factors) = lookup_modes gr1 dep; + val mode = find_mode gr1 dep s u modes []; val (gr2, ps) = - compile_expr thy defs dep thyname false thynames (gr1, (mode, u)) + compile_expr thy defs dep module false (gr1, (mode, u)) in SOME (gr2, (if brack then parens else I) (Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1, @@ -671,54 +677,56 @@ in rename_term (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop (HOLogic.mk_mem - (foldr1 HOLogic.mk_prod (ts @ [u]), Const (s ^ " ", + (foldr1 HOLogic.mk_prod (ts @ [u]), Const (s ^ "_aux", HOLogic.mk_setT (foldr1 HOLogic.mk_prodT (Ts @ [U]))))))) end; -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 _ => +fun mk_fun thy defs name eqns dep module module' gr = + case try (get_node gr) name of + NONE => let val clauses = map clause_of_eqn eqns; - val pname = name ^ " "; + val pname = name ^ "_aux"; val arity = length (snd (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of (hd eqns))))))); val mode = 1 upto arity; + val (gr', (fun_id, mode_id)) = gr |> + mk_const_id module' name |>>> + modename module' pname ([], mode); 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 " ^ fun_id)) vars, Pretty.str " =", + [mk_app false (Pretty.str ("fun " ^ snd fun_id)) vars, Pretty.str " =", Pretty.brk 1, Pretty.str "Seq.hd", Pretty.brk 1, - parens (Pretty.block [Pretty.str (modename thy thyname' thyname' pname ([], mode)), + parens (Pretty.block [Pretty.str mode_id, Pretty.brk 1, mk_tuple vars])]) ^ ";\n\n"; - val gr' = mk_ind_def thy defs (Graph.add_edge (name, dep) - (Graph.new_node (name, (NONE, thyname', s)) gr)) name [pname] thyname' + val gr'' = mk_ind_def thy defs (add_edge (name, dep) + (new_node (name, (NONE, module', s)) gr')) name [pname] module' [(pname, [([], mode)])] [(pname, map (fn i => replicate i 2) (0 upto arity-1))] clauses; - val (modes, _, _) = lookup_modes gr' dep; - val _ = find_mode pname (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop + val (modes, _) = lookup_modes gr'' dep; + val _ = find_mode gr'' dep pname (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop (Logic.strip_imp_concl (hd clauses))))) modes mode - in gr' end, call_id) - end; + in (gr'', mk_qual_id module fun_id) end + | SOME _ => + (add_edge (name, dep) gr, mk_qual_id module (get_const_id name gr)); -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 +fun inductive_codegen thy defs gr dep module brack (Const ("op :", _) $ t $ u) = + ((case mk_ind_call thy defs gr dep module (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 defs gr dep thyname t u true) - | inductive_codegen thy defs gr dep thyname brack t = (case strip_comb t of + handle TERM _ => mk_ind_call thy defs gr dep module t u true) + | inductive_codegen thy defs gr dep module brack t = (case strip_comb t of (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy), s) of - NONE => list_of_indset thy defs gr dep thyname brack t + NONE => list_of_indset thy defs gr dep module brack t | SOME eqns => let - val (_, (_, thyname')) = split_last eqns; + val (_, (_, thyname)) = split_last eqns; val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns)) - dep thyname thyname' gr; + dep module (if_library thyname module) gr; val (gr'', ps) = foldl_map - (invoke_codegen thy defs dep thyname true) (gr', ts); + (invoke_codegen thy defs dep module true) (gr', ts); in SOME (gr'', mk_app brack (Pretty.str id) ps) end) | _ => NONE); @@ -745,8 +753,8 @@ fun ?! s = isSome (Seq.pull s); -fun op_61__1 x = Seq.single x; +fun equal__1 x = Seq.single x; -val op_61__2 = op_61__1; +val equal__2 = equal__1; -fun op_61__1_2 (x, y) = ?? (x = y); +fun equal__1_2 (x, y) = ?? (x = y); diff -r 2a8111863b16 -r 6642e0f96f44 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Thu Aug 25 09:29:05 2005 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Thu Aug 25 16:10:16 2005 +0200 @@ -82,15 +82,15 @@ end); fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of - SOME (_, SOME i) => "_def" ^ string_of_int i | _ => ""); + SOME (_, SOME i) => " def" ^ string_of_int i | _ => ""); exception EQN of string * typ * string; fun cycle g (xs, x) = if x mem xs then xs - else Library.foldl (cycle g) (x :: xs, List.concat (Graph.find_paths g (x, x))); + else Library.foldl (cycle g) (x :: xs, List.concat (Graph.find_paths (fst g) (x, x))); -fun add_rec_funs thy defs gr dep eqs thyname = +fun add_rec_funs thy defs gr dep eqs module = let fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t), dest_eqn (rename_term t)); @@ -98,67 +98,71 @@ val (dname, _) :: _ = eqs'; val (s, T) = const_of (hd eqs); - fun mk_fundef thyname fname prfx gr [] = (gr, []) - | mk_fundef thyname fname prfx gr ((fname', (lhs, rhs)) :: xs) = + fun mk_fundef module fname prfx gr [] = (gr, []) + | mk_fundef module fname prfx gr ((fname', (lhs, rhs)) :: xs) = let - 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 + val (gr1, pl) = invoke_codegen thy defs dname module false (gr, lhs); + val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs); + val (gr3, rest) = mk_fundef module 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 thyname fundef = Graph.map_node dname - (K (SOME (EQN ("", dummyT, dname)), thyname, Pretty.string_of (Pretty.blk (0, + fun put_code module fundef = map_node dname + (K (SOME (EQN ("", dummyT, dname)), module, Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n")); in - (case try (Graph.get_node gr) dname of + (case try (get_node gr) dname of NONE => let - val gr1 = Graph.add_edge (dname, dep) - (Graph.new_node (dname, (SOME (EQN (s, T, "")), "", "")) gr); - val (gr2, fundef) = mk_fundef thyname "" "fun " gr1 eqs'; + val gr1 = add_edge (dname, dep) + (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr); + val (gr2, fundef) = mk_fundef module "" "fun " gr1 eqs'; val xs = cycle gr2 ([], dname); - val cs = map (fn x => case Graph.get_node gr2 x of + val cs = map (fn x => case get_node gr2 x of (SOME (EQN (s, T, _)), _, _) => (s, T) | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^ implode (separate ", " xs))) xs in (case xs of - [_] => put_code thyname fundef gr2 + [_] => (put_code module fundef gr2, module) | _ => if not (dep mem xs) then let val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs; + val module' = if_library thyname module; 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) + val (gr3, fundef') = mk_fundef module' "" "fun " + (add_edge (dname, dep) + (foldr (uncurry new_node) (del_nodes xs gr2) (map (fn k => - (k, (SOME (EQN ("", dummyT, dname)), thyname, ""))) xs))) eqs'' - in put_code thyname fundef' gr3 end - else gr2) + (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs))) eqs'' + in (put_code module' fundef' gr3, module') end + else (gr2, module)) end - | 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) + | SOME (SOME (EQN (_, _, s)), module', _) => + (if s = "" then + if dname = dep then gr else add_edge (dname, dep) gr + else if s = dep then gr else add_edge (s, dep) gr, + module')) end; -fun recfun_codegen thy defs gr dep thyname brack t = (case strip_comb t of +fun recfun_codegen thy defs gr dep module 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, thyname'), NONE) => + | ((eqns, thyname), NONE) => let + val module' = if_library thyname module; val (gr', ps) = foldl_map - (invoke_codegen thy defs dep thyname true) (gr, ts); - val suffix = mk_suffix thy defs p + (invoke_codegen thy defs dep module true) (gr, ts); + val suffix = mk_suffix thy defs p; + val (gr'', module'') = + add_rec_funs thy defs gr' dep (map prop_of eqns) module'; + val (gr''', fname) = mk_const_id module'' (s ^ suffix) gr'' in - 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) + SOME (gr''', mk_app brack (Pretty.str (mk_qual_id module fname)) ps) end) | _ => NONE); diff -r 2a8111863b16 -r 6642e0f96f44 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Thu Aug 25 09:29:05 2005 +0200 +++ b/src/HOL/Tools/typedef_package.ML Thu Aug 25 16:10:16 2005 +0200 @@ -272,17 +272,16 @@ (** trivial code generator **) -fun typedef_codegen thy defs gr dep thyname brack t = +fun typedef_codegen thy defs gr dep module brack t = let fun get_name (Type (tname, _)) = tname | get_name _ = ""; fun mk_fun s T ts = let - val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr, T); + val (gr', _) = Codegen.invoke_tycodegen thy defs dep module false (gr, T); val (gr'', ps) = - 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 + foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts); + val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'') in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end; fun lookup f T = getOpt (Option.map f (Symtab.lookup (TypedefData.get thy, get_name T)), "") @@ -303,28 +302,32 @@ | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)] | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; -fun typedef_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) = +fun typedef_tycodegen thy defs gr dep module 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 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 defs dep thyname (length Ts = 1)) (gr, Ts); - val gr'' = Graph.add_edge (Abs_name, dep) gr' handle Graph.UNDEF _ => + val module' = Codegen.if_library + (Codegen.thyname_of_type tname thy) module; + val node_id = tname ^ " (type)"; + val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map + (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1)) + (gr, Ts) |>>> + Codegen.mk_const_id module' Abs_name |>>> + Codegen.mk_const_id module' Rep_name |>>> + Codegen.mk_type_id module' s; + val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id) + in SOME (case try (Codegen.get_node gr') node_id of + NONE => let val (gr'', p :: ps) = foldl_map - (Codegen.invoke_tycodegen thy defs Abs_name thyname' false) - (Graph.add_edge (Abs_name, dep) - (Graph.new_node (Abs_name, (NONE, "", "")) gr'), oldT :: Us); + (Codegen.invoke_tycodegen thy defs node_id module' false) + (Codegen.add_edge (node_id, dep) + (Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us); val s = Pretty.string_of (Pretty.block [Pretty.str "datatype ", - mk_tyexpr ps ty_id, + mk_tyexpr ps (snd ty_id), Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"), Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^ Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id), @@ -332,28 +335,27 @@ 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 thyname' false newT, Pretty.brk 1, + Codegen.mk_term_of gr'' module' 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 thyname' false oldT, Pretty.brk 1, + Codegen.mk_term_of gr'' module' 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 thyname' false [] "" newT, Pretty.brk 1, + Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1, Pretty.str "i =", Pretty.brk 1, Pretty.block [Pretty.str (Abs_id ^ " ("), - Codegen.mk_gen thy thyname' false [] "" oldT, Pretty.brk 1, + Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1, Pretty.str "i);"]]) ^ "\n\n" else "") - in Graph.map_node Abs_name (K (NONE, thyname', s)) gr'' end - in - SOME (gr'', mk_tyexpr qs ty_call_id) + in Codegen.map_node node_id (K (NONE, module', s)) gr'' end + | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr) end) - | typedef_tycodegen thy defs gr dep thyname brack _ = NONE; + | typedef_tycodegen thy defs gr dep module brack _ = NONE; val setup = [TypedefData.init, diff -r 2a8111863b16 -r 6642e0f96f44 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Thu Aug 25 09:29:05 2005 +0200 +++ b/src/Pure/codegen.ML Thu Aug 25 16:10:16 2005 +0200 @@ -20,6 +20,7 @@ | Quote of 'a; type deftab + type node type codegr type 'a codegen @@ -29,8 +30,10 @@ val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory val preprocess: theory -> thm list -> thm list val print_codegens: theory -> unit - val generate_code: theory -> (string * string) list -> (string * string) list - val generate_code_i: theory -> (string * term) list -> (string * string) list + val generate_code: theory -> string list -> string -> (string * string) list -> + (string * string) list * codegr + val generate_code_i: theory -> string list -> string -> (string * term) list -> + (string * string) list * codegr val assoc_consts: (xstring * string option * (term mixfix list * (string * string) list)) list -> theory -> theory val assoc_consts_i: (xstring * typ option * (term mixfix list * @@ -41,19 +44,24 @@ (term mixfix list * (string * string) list) option val get_assoc_type: theory -> string -> (typ mixfix list * (string * string) list) option + val codegen_error: codegr -> string -> string -> 'a val invoke_codegen: theory -> deftab -> string -> string -> bool -> codegr * term -> codegr * Pretty.T val invoke_tycodegen: theory -> deftab -> string -> string -> bool -> codegr * typ -> codegr * Pretty.T val mk_id: string -> string - val mk_const_id: theory -> string -> string -> string -> string - val mk_type_id: theory -> string -> string -> string -> string + val mk_qual_id: string -> string * string -> string + val mk_const_id: string -> string -> codegr -> codegr * (string * string) + val get_const_id: string -> codegr -> string * string + val mk_type_id: string -> string -> codegr -> codegr * (string * string) + val get_type_id: string -> codegr -> string * string val thyname_of_type: string -> theory -> string val thyname_of_const: string -> theory -> string val rename_terms: term list -> term list val rename_term: term -> term val new_names: term -> string list -> string list val new_name: term -> string -> string + val if_library: 'a -> 'a -> 'a val get_defn: theory -> deftab -> string -> typ -> ((typ * (string * (term list * term))) * int option) option val is_instance: theory -> typ -> typ -> bool @@ -62,12 +70,18 @@ val eta_expand: term -> term list -> int -> term val strip_tname: string -> string val mk_type: bool -> typ -> Pretty.T - val mk_term_of: theory -> string -> bool -> typ -> Pretty.T - val mk_gen: theory -> string -> bool -> string list -> string -> typ -> Pretty.T + val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T + val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T val test_fn: (int -> (string * term) list option) ref val test_term: theory -> int -> int -> term -> (string * term) list option val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list val mk_deftab: theory -> deftab + val get_node: codegr -> string -> node + val add_edge: string * string -> codegr -> codegr + val add_edge_acyclic: string * string -> codegr -> codegr + val del_nodes: string list -> codegr -> codegr + val map_node: string -> (node -> node) -> codegr -> codegr + val new_node: string * node -> codegr -> codegr end; structure Codegen : CODEGEN = @@ -118,11 +132,23 @@ (* code dependency graph *) -type codegr = +type nametab = (string * string) Symtab.table * unit Symtab.table; + +fun merge_nametabs ((tab, used), (tab', used')) = + (Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used')); + +type node = (exn option * (* slot for arbitrary data *) string * (* name of structure containing piece of code *) - string) (* piece of code *) - Graph.T; + string); (* piece of code *) + +type codegr = + node Graph.T * + (nametab * (* table for assigned constant names *) + nametab); (* table for assigned type names *) + +val emptygr : codegr = (Graph.empty, + ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty))); (* type of code generators *) @@ -131,7 +157,7 @@ deftab -> (* definition table (for efficiency) *) codegr -> (* code dependency graph *) string -> (* node name of caller (for recording dependencies) *) - string -> (* theory name of caller (for modular code generation) *) + string -> (* module name of caller (for modular code generation) *) bool -> (* whether to parenthesize generated expression *) 'a -> (* item to generate code from *) (codegr * Pretty.T) option; @@ -175,27 +201,29 @@ types : (string * (typ mixfix list * (string * string) list)) list, attrs: (string * (Args.T list -> theory attribute * Args.T list)) list, preprocs: (stamp * (theory -> thm list -> thm list)) list, + modules: codegr Symtab.table, test_params: test_params}; val empty = {codegens = [], tycodegens = [], consts = [], types = [], attrs = [], - preprocs = [], test_params = default_test_params}; + preprocs = [], modules = Symtab.empty, test_params = default_test_params}; val copy = I; val extend = I; fun merge _ ({codegens = codegens1, tycodegens = tycodegens1, consts = consts1, types = types1, attrs = attrs1, - preprocs = preprocs1, test_params = test_params1}, + preprocs = preprocs1, modules = modules1, test_params = test_params1}, {codegens = codegens2, tycodegens = tycodegens2, consts = consts2, types = types2, attrs = attrs2, - preprocs = preprocs2, test_params = test_params2}) = + preprocs = preprocs2, modules = modules2, test_params = test_params2}) = {codegens = merge_alists' codegens1 codegens2, tycodegens = merge_alists' tycodegens1 tycodegens2, consts = merge_alists consts1 consts2, types = merge_alists types1 types2, attrs = merge_alists attrs1 attrs2, preprocs = merge_alists' preprocs1 preprocs2, + modules = Symtab.merge (K true) (modules1, modules2), test_params = merge_test_params test_params1 test_params2}; fun print _ ({codegens, tycodegens, ...} : T) = @@ -213,33 +241,48 @@ fun get_test_params thy = #test_params (CodegenData.get thy); fun map_test_params f thy = - let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = + let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = CodegenData.get thy; in CodegenData.put {codegens = codegens, tycodegens = tycodegens, consts = consts, types = types, attrs = attrs, preprocs = preprocs, - test_params = f test_params} thy + modules = modules, test_params = f test_params} thy + end; + + +(**** access modules ****) + +fun get_modules thy = #modules (CodegenData.get thy); + +fun map_modules f thy = + let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = + CodegenData.get thy; + in CodegenData.put {codegens = codegens, tycodegens = tycodegens, + consts = consts, types = types, attrs = attrs, preprocs = preprocs, + modules = f modules, test_params = test_params} thy end; (**** add new code generators to theory ****) fun add_codegen name f thy = - let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = + let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = CodegenData.get thy in (case assoc (codegens, name) of NONE => CodegenData.put {codegens = (name, f) :: codegens, tycodegens = tycodegens, consts = consts, types = types, - attrs = attrs, preprocs = preprocs, test_params = test_params} thy + attrs = attrs, preprocs = preprocs, modules = modules, + test_params = test_params} thy | SOME _ => error ("Code generator " ^ name ^ " already declared")) end; fun add_tycodegen name f thy = - let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = + let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = CodegenData.get thy in (case assoc (tycodegens, name) of NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens, codegens = codegens, consts = consts, types = types, - attrs = attrs, preprocs = preprocs, test_params = test_params} thy + attrs = attrs, preprocs = preprocs, modules = modules, + test_params = test_params} thy | SOME _ => error ("Code generator " ^ name ^ " already declared")) end; @@ -247,13 +290,13 @@ (**** code attribute ****) fun add_attribute name att thy = - let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = + let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = CodegenData.get thy in (case assoc (attrs, name) of NONE => CodegenData.put {tycodegens = tycodegens, codegens = codegens, consts = consts, types = types, attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs, - preprocs = preprocs, + preprocs = preprocs, modules = modules, test_params = test_params} thy | SOME _ => error ("Code attribute " ^ name ^ " already declared")) end; @@ -273,12 +316,12 @@ (**** preprocessors ****) fun add_preprocessor p thy = - let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = + let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = CodegenData.get thy in CodegenData.put {tycodegens = tycodegens, codegens = codegens, consts = consts, types = types, attrs = attrs, preprocs = (stamp (), p) :: preprocs, - test_params = test_params} thy + modules = modules, test_params = test_params} thy end; fun preprocess thy ths = @@ -302,7 +345,7 @@ fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) => let - val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = + val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = CodegenData.get thy; val cname = Sign.intern_const thy s; in @@ -320,7 +363,7 @@ tycodegens = tycodegens, consts = ((cname, T'), syn) :: consts, types = types, attrs = attrs, preprocs = preprocs, - test_params = test_params} thy + modules = modules, test_params = test_params} thy | SOME _ => error ("Constant " ^ cname ^ " already associated with code")) end | _ => error ("Not a constant: " ^ s)) @@ -334,7 +377,7 @@ fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) => let - val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = + val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = CodegenData.get thy; val tc = Sign.intern_type thy s in @@ -342,7 +385,7 @@ NONE => CodegenData.put {codegens = codegens, tycodegens = tycodegens, consts = consts, types = (tc, syn) :: types, attrs = attrs, - preprocs = preprocs, test_params = test_params} thy + preprocs = preprocs, modules = modules, test_params = test_params} thy | SOME _ => error ("Type " ^ tc ^ " already associated with code")) end) (thy, xs); @@ -377,40 +420,70 @@ if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s' end; -fun extrn thy f thyname s = +fun mk_long_id (p as (tab, used)) module s = let - val xs = NameSpace.unpack s; - val s' = setmp NameSpace.long_names false (setmp NameSpace.short_names false - (setmp NameSpace.unique_names true (f thy))) s; - val xs' = NameSpace.unpack s' - in - if "modular" mem !mode andalso length xs = length xs' andalso hd xs' = thyname - then NameSpace.pack (tl xs') else s' + fun find_name [] = sys_error "mk_long_id" + | find_name (ys :: yss) = + let + val s' = NameSpace.pack ys + val s'' = NameSpace.append module s' + in case Symtab.lookup (used, s'') of + NONE => ((module, s'), (Symtab.update_new ((s, (module, s')), tab), + Symtab.update_new ((s'', ()), used))) + | SOME _ => find_name yss + end + in case Symtab.lookup (tab, s) of + NONE => find_name (Library.suffixes1 (NameSpace.unpack s)) + | SOME name => (name, p) end; -(* thyname: theory name for caller *) -(* thyname': theory name for callee *) -(* if caller and callee reside in different theories, use qualified access *) +(* module: module name for caller *) +(* module': module name for callee *) +(* if caller and callee reside in different modules, use qualified access *) -fun mk_const_id thy thyname thyname' s = +fun mk_qual_id module (module', s) = + if module = module' orelse module' = "" then s else module' ^ "." ^ s; + +fun mk_const_id module cname (gr, (tab1, tab2)) = let - val s' = mk_id (extrn thy Sign.extern_const thyname' s); + val ((module, s), tab1') = mk_long_id tab1 module cname + val s' = mk_id s; val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' - in - if "modular" mem !mode andalso thyname <> thyname' andalso thyname' <> "" - then thyname' ^ "." ^ s'' else s'' - end; + in ((gr, (tab1', tab2)), (module, s'')) end; -fun mk_type_id' f thy thyname thyname' s = +fun get_const_id cname (gr, (tab1, tab2)) = + case Symtab.lookup (fst tab1, cname) of + NONE => error ("get_const_id: no such constant: " ^ quote cname) + | SOME (module, s) => + let + val s' = mk_id s; + val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' + in (module, s'') end; + +fun mk_type_id module tyname (gr, (tab1, tab2)) = let - val s' = mk_id (extrn thy Sign.extern_type thyname' s); - val s'' = f (if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s') - in - if "modular" mem !mode andalso thyname <> thyname' andalso thyname' <> "" - then thyname' ^ "." ^ s'' else s'' - end; + val ((module, s), tab2') = mk_long_id tab2 module tyname + val s' = mk_id s; + val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' + in ((gr, (tab1, tab2')), (module, s'')) end; -val mk_type_id = mk_type_id' I; +fun get_type_id tyname (gr, (tab1, tab2)) = + case Symtab.lookup (fst tab2, tyname) of + NONE => error ("get_type_id: no such type: " ^ quote tyname) + | SOME (module, s) => + let + val s' = mk_id s; + val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' + in (module, s'') end; + +fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab); + +fun get_node (gr, x) k = Graph.get_node gr k; +fun add_edge e (gr, x) = (Graph.add_edge e gr, x); +fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x); +fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x); +fun map_node k f (gr, x) = (Graph.map_node k f gr, x); +fun new_node p (gr, x) = (Graph.new_node p gr, x); fun theory_of_type s thy = if Sign.declared_tyname thy s @@ -503,18 +576,19 @@ (**** invoke suitable code generator for term / type ****) -fun invoke_codegen thy defs dep thyname brack (gr, t) = (case get_first - (fn (_, f) => f thy defs gr dep thyname brack t) (#codegens (CodegenData.get thy)) of - NONE => error ("Unable to generate code for term:\n" ^ - Sign.string_of_term thy t ^ "\nrequired by:\n" ^ - commas (Graph.all_succs gr [dep])) +fun codegen_error (gr, _) dep s = + error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep])); + +fun invoke_codegen thy defs dep module brack (gr, t) = (case get_first + (fn (_, f) => f thy defs gr dep module brack t) (#codegens (CodegenData.get thy)) of + NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^ + Sign.string_of_term thy t) | SOME x => x); -fun invoke_tycodegen thy defs dep thyname brack (gr, T) = (case get_first - (fn (_, f) => f thy defs gr dep thyname brack T) (#tycodegens (CodegenData.get thy)) of - NONE => error ("Unable to generate code for type:\n" ^ - Sign.string_of_typ thy T ^ "\nrequired by:\n" ^ - commas (Graph.all_succs gr [dep])) +fun invoke_tycodegen thy defs dep module brack (gr, T) = (case get_first + (fn (_, f) => f thy defs gr dep module brack T) (#tycodegens (CodegenData.get thy)) of + NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^ + Sign.string_of_typ thy T) | SOME x => x); @@ -532,7 +606,7 @@ | pretty_mixfix module module' (Ignore :: ms) ps qs = pretty_mixfix module module' ms ps qs | pretty_mixfix module module' (Module :: ms) ps qs = - (if "modular" mem !mode andalso module <> module' + (if module <> module' then cons (Pretty.str (module' ^ ".")) else I) (pretty_mixfix module module' ms ps qs) | pretty_mixfix module module' (Pretty p :: ms) ps qs = @@ -564,15 +638,17 @@ fun new_name t x = hd (new_names t [x]); -fun default_codegen thy defs gr dep thyname brack t = +fun if_library x y = if "library" mem !mode then x else y; + +fun default_codegen thy defs gr dep module brack t = let val (u, ts) = strip_comb t; - fun codegens brack = foldl_map (invoke_codegen thy defs dep thyname brack) + fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack) in (case u of Var ((s, i), T) => let val (gr', ps) = codegens true (gr, ts); - val (gr'', _) = invoke_tycodegen thy defs dep thyname false (gr', T) + val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T) in SOME (gr'', mk_app brack (Pretty.str (s ^ (if i=0 then "" else string_of_int i))) ps) end @@ -580,7 +656,7 @@ | Free (s, T) => let val (gr', ps) = codegens true (gr, ts); - val (gr'', _) = invoke_tycodegen thy defs dep thyname false (gr', T) + val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T) in SOME (gr'', mk_app brack (Pretty.str s) ps) end | Const (s, T) => @@ -588,60 +664,66 @@ SOME (ms, aux) => let val i = num_args ms in if length ts < i then - default_codegen thy defs gr dep thyname brack (eta_expand u ts i) + default_codegen thy defs gr dep module brack (eta_expand u ts i) else let val (ts1, ts2) = args_of ms ts; val (gr1, ps1) = codegens false (gr, ts1); val (gr2, ps2) = codegens true (gr1, ts2); val (gr3, ps3) = codegens false (gr2, quotes_of ms); - val (thyname', suffix) = (case get_defn thy defs s T of - NONE => (thyname_of_const s thy, "") - | SOME ((U, (thyname', _)), NONE) => (thyname', "") - | SOME ((U, (thyname', _)), SOME i) => - (thyname', "_def" ^ string_of_int i)); + val (module', suffix) = (case get_defn thy defs s T of + NONE => (if_library (thyname_of_const s thy) module, "") + | SOME ((U, (module', _)), NONE) => + (if_library module' module, "") + | SOME ((U, (module', _)), SOME i) => + (if_library module' module, " def" ^ string_of_int i)); val node_id = s ^ suffix; - val p = mk_app brack (Pretty.block - (pretty_mixfix thyname thyname' ms ps1 ps3)) ps2 - in SOME (case try (Graph.get_node gr3) node_id of + fun p module' = mk_app brack (Pretty.block + (pretty_mixfix module module' ms ps1 ps3)) ps2 + in SOME (case try (get_node gr3) node_id of NONE => (case get_aux_code aux of - [] => (gr3, p) - | xs => (Graph.add_edge (node_id, dep) (Graph.new_node - (node_id, (NONE, thyname', space_implode "\n" xs ^ "\n")) gr3), p)) - | SOME _ => (Graph.add_edge (node_id, dep) gr3, p)) + [] => (gr3, p module) + | xs => (add_edge (node_id, dep) (new_node + (node_id, (NONE, module', space_implode "\n" xs ^ "\n")) gr3), + p module')) + | SOME (_, module'', _) => + (add_edge (node_id, dep) gr3, p module'')) end end | NONE => (case get_defn thy defs s T of NONE => NONE - | SOME ((U, (thyname', (args, rhs))), k) => + | SOME ((U, (thyname, (args, rhs))), k) => let - val suffix = (case k of NONE => "" | SOME i => "_def" ^ string_of_int i); + val module' = if_library thyname module; + val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i); val node_id = s ^ suffix; - val def_id = mk_const_id thy thyname' thyname' s ^ suffix; - val call_id = mk_const_id thy thyname thyname' s ^ suffix; - val (gr', ps) = codegens true (gr, ts); - in - SOME (Graph.add_edge (node_id, dep) gr' handle Graph.UNDEF _ => - let - val _ = message ("expanding definition of " ^ s); - val (Ts, _) = strip_type T; - val (args', rhs') = - if not (null args) orelse null Ts then (args, rhs) else - let val v = Free (new_name rhs "x", hd Ts) - in ([v], betapply (rhs, v)) end; - val (gr1, p) = invoke_codegen thy defs node_id thyname' false - (Graph.add_edge (node_id, dep) - (Graph.new_node (node_id, (NONE, "", "")) gr'), rhs'); - val (gr2, xs) = codegens false (gr1, args'); - val (gr3, _) = invoke_tycodegen thy defs dep thyname false (gr2, T); - val (gr4, ty) = invoke_tycodegen thy defs node_id thyname' false (gr3, U); - in Graph.map_node node_id (K (NONE, thyname', Pretty.string_of - (Pretty.block (separate (Pretty.brk 1) - (if null args' then - [Pretty.str ("val " ^ def_id ^ " :"), ty] - else Pretty.str ("fun " ^ def_id) :: xs) @ - [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr4 - end, mk_app brack (Pretty.str call_id) ps) + val (gr', (ps, def_id)) = codegens true (gr, ts) |>>> + mk_const_id module' (s ^ suffix); + val p = mk_app brack (Pretty.str (mk_qual_id module def_id)) ps + in SOME (case try (get_node gr') node_id of + NONE => + let + val _ = message ("expanding definition of " ^ s); + val (Ts, _) = strip_type T; + val (args', rhs') = + if not (null args) orelse null Ts then (args, rhs) else + let val v = Free (new_name rhs "x", hd Ts) + in ([v], betapply (rhs, v)) end; + val (gr1, p') = invoke_codegen thy defs node_id module' false + (add_edge (node_id, dep) + (new_node (node_id, (NONE, "", "")) gr'), rhs'); + val (gr2, xs) = codegens false (gr1, args'); + val (gr3, _) = invoke_tycodegen thy defs dep module false (gr2, T); + val (gr4, ty) = invoke_tycodegen thy defs node_id module' false (gr3, U); + in (map_node node_id (K (NONE, module', Pretty.string_of + (Pretty.block (separate (Pretty.brk 1) + (if null args' then + [Pretty.str ("val " ^ snd def_id ^ " :"), ty] + else Pretty.str ("fun " ^ snd def_id) :: xs) @ + [Pretty.str " =", Pretty.brk 1, p', Pretty.str ";"])) ^ "\n\n")) gr4, + p) + end + | SOME _ => (add_edge (node_id, dep) gr', p)) end)) | Abs _ => @@ -650,7 +732,7 @@ val t = strip_abs_body u val bs' = new_names t bs; val (gr1, ps) = codegens true (gr, ts); - val (gr2, p) = invoke_codegen thy defs dep thyname false + val (gr2, p) = invoke_codegen thy defs dep module false (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t)); in SOME (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @ @@ -660,30 +742,33 @@ | _ => NONE) end; -fun default_tycodegen thy defs gr dep thyname brack (TVar ((s, i), _)) = +fun default_tycodegen thy defs gr dep module brack (TVar ((s, i), _)) = SOME (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i))) - | default_tycodegen thy defs gr dep thyname brack (TFree (s, _)) = + | default_tycodegen thy defs gr dep module brack (TFree (s, _)) = SOME (gr, Pretty.str s) - | default_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) = + | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) = (case assoc (#types (CodegenData.get thy), s) of NONE => NONE | SOME (ms, aux) => let val (gr', ps) = foldl_map - (invoke_tycodegen thy defs dep thyname false) + (invoke_tycodegen thy defs dep module false) (gr, fst (args_of ms Ts)); val (gr'', qs) = foldl_map - (invoke_tycodegen thy defs dep thyname false) + (invoke_tycodegen thy defs dep module false) (gr', quotes_of ms); - val thyname' = thyname_of_type s thy; + val module' = if_library (thyname_of_type s thy) module; val node_id = s ^ " (type)"; - val p = Pretty.block (pretty_mixfix thyname thyname' ms ps qs) - in SOME (case try (Graph.get_node gr'') node_id of + fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs) + in SOME (case try (get_node gr'') node_id of NONE => (case get_aux_code aux of - [] => (gr'', p) - | xs => (Graph.add_edge (node_id, dep) (Graph.new_node - (node_id, (NONE, thyname', space_implode "\n" xs ^ "\n")) gr''), p)) - | SOME _ => (Graph.add_edge (node_id, dep) gr'', p)) + [] => (gr'', p module') + | xs => (fst (mk_type_id module' s + (add_edge (node_id, dep) (new_node (node_id, + (NONE, module', space_implode "\n" xs ^ "\n")) gr''))), + p module')) + | SOME (_, module'', _) => + (add_edge (node_id, dep) gr'', p module'')) end); val _ = Context.add_setup @@ -696,10 +781,12 @@ fun add_to_module name s ms = overwrite (ms, (name, the (assoc (ms, name)) ^ s)); -fun output_code gr xs = +fun output_code gr module xs = let - val code = - map (fn s => (s, Graph.get_node gr s)) (rev (Graph.all_preds gr xs)) + val code = List.mapPartial (fn s => + let val c as (_, module', _) = Graph.get_node gr s + in if module = "" orelse module = module' then SOME (s, c) else NONE end) + (rev (Graph.all_preds gr xs)); fun string_of_cycle (a :: b :: cs) = let val SOME (x, y) = get_first (fn (x, (_, a', _)) => if a = a' then Option.map (pair x) @@ -709,43 +796,63 @@ in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end | string_of_cycle _ = "" in - if "modular" mem !mode then + if module = "" then let val modules = distinct (map (#2 o snd) code); val mod_gr = foldr (uncurry Graph.add_edge_acyclic) (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules) - (List.concat (map (fn (s, (_, thyname, _)) => map (pair thyname) - (filter_out (equal thyname) (map (#2 o Graph.get_node gr) + (List.concat (map (fn (s, (_, module, _)) => map (pair module) + (filter_out (equal module) (map (#2 o Graph.get_node gr) (Graph.imm_succs gr s)))) code)); val modules' = rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs)) in - foldl (fn ((_, (_, thyname, s)), ms) => add_to_module thyname s ms) + foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms) (map (rpair "") modules') code end handle Graph.CYCLES (cs :: _) => error ("Cyclic dependency of modules:\n" ^ commas cs ^ "\n" ^ string_of_cycle cs) - else [("Generated", implode (map (#3 o snd) code))] + else [(module, implode (map (#3 o snd) code))] end; -fun gen_generate_code prep_term thy = +fun gen_generate_code prep_term thy modules module = setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs => let + val _ = assert (module <> "" orelse + "library" mem !mode andalso forall (equal "" o fst) xs) + "missing module name"; + val graphs = get_modules thy; val defs = mk_deftab thy; - val gr = Graph.new_node ("", (NONE, "Generated", "")) Graph.empty; + val gr = new_node ("", (NONE, module, "")) + (foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) => + (Graph.merge (fn ((_, module, _), (_, module', _)) => + module = module') (gr, gr'), + (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr + (map (fn s => case Symtab.lookup (graphs, s) of + NONE => error ("Undefined code module: " ^ s) + | SOME gr => gr) modules)) + handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks); fun expand (t as Abs _) = t | expand t = (case fastype_of t of Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t); val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s) - (invoke_codegen thy defs "" "Generated" false (gr, t))) + (invoke_codegen thy defs "" module false (gr, t))) (gr, map (apsnd (expand o prep_term thy)) xs); - val code = - space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block - [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^ - "\n\n" + val code = List.mapPartial + (fn ("", _) => NONE + | (s', p) => SOME (Pretty.string_of (Pretty.block + [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"]))) ps; + val code' = space_implode "\n\n" code ^ "\n\n"; + val code'' = + List.mapPartial (fn (name, s) => + if "library" mem !mode andalso name = module andalso null code + then NONE + else SOME (name, mk_struct name s)) + ((if null code then I + else add_to_module module code') + (output_code (fst gr') (if_library "" module) [""])) in - map (fn (name, s) => (name, mk_struct name s)) - (add_to_module "Generated" code (output_code gr' [""])) + (code'', del_nodes [""] gr') end)); val generate_code_i = gen_generate_code (K I); @@ -768,28 +875,27 @@ [Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","), Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]); -fun mk_term_of thy thyname p (TVar ((s, i), _)) = Pretty.str +fun mk_term_of gr module p (TVar ((s, i), _)) = Pretty.str (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F") - | mk_term_of thy thyname p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F") - | mk_term_of thy thyname p (Type (s, Ts)) = (if p then parens else I) + | mk_term_of gr module p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F") + | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I) (Pretty.block (separate (Pretty.brk 1) - (Pretty.str (mk_type_id' (fn s' => "term_of_" ^ s') - thy thyname (thyname_of_type s thy) s) :: + (Pretty.str (mk_qual_id module + (get_type_id' (fn s' => "term_of_" ^ s') s gr)) :: List.concat (map (fn T => - [mk_term_of thy thyname true T, mk_type true T]) Ts)))); + [mk_term_of gr module true T, mk_type true T]) Ts)))); (**** Test data generators ****) -fun mk_gen thy thyname p xs a (TVar ((s, i), _)) = Pretty.str +fun mk_gen gr module p xs a (TVar ((s, i), _)) = Pretty.str (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G") - | mk_gen thy thyname p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G") - | mk_gen thy thyname p xs a (Type (s, Ts)) = (if p then parens else I) + | mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G") + | mk_gen gr module p xs a (Type (s, Ts)) = (if p then parens else I) (Pretty.block (separate (Pretty.brk 1) - (Pretty.str (mk_type_id' (fn s' => "gen_" ^ s') - thy thyname (thyname_of_type s thy) s ^ + (Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^ (if s mem xs then "'" else "")) :: - map (mk_gen thy thyname true xs a) Ts @ + map (mk_gen gr module true xs a) Ts @ (if s mem xs then [Pretty.str a] else [])))); val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE); @@ -802,17 +908,17 @@ "Term to be tested contains schematic variables"; val frees = map dest_Free (term_frees t); val szname = variant (map fst frees) "i"; - val code = space_implode "\n" (map snd - (setmp mode ["term_of", "test"] (generate_code_i thy) - [("testf", list_abs_free (frees, t))])); - val s = "structure TestTerm =\nstruct\n\n" ^ code ^ + val (code, gr) = setmp mode ["term_of", "test"] + (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))]; + val s = "structure TestTerm =\nstruct\n\n" ^ + space_implode "\n" (map snd code) ^ "\nopen Generated;\n\n" ^ Pretty.string_of (Pretty.block [Pretty.str "val () = Codegen.test_fn :=", Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1, Pretty.blk (0, [Pretty.str "let", Pretty.brk 1, Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) => Pretty.block [Pretty.str ("val " ^ mk_id s ^ " ="), Pretty.brk 1, - mk_gen thy "" false [] "" T, Pretty.brk 1, + mk_gen gr "Generated" false [] "" T, Pretty.brk 1, Pretty.str (szname ^ ";")]) frees)), Pretty.brk 1, Pretty.str "in", Pretty.brk 1, Pretty.block [Pretty.str "if ", @@ -823,7 +929,7 @@ List.concat (separate [Pretty.str ",", Pretty.brk 1] (map (fn (s, T) => [Pretty.block [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1, - mk_app false (mk_term_of thy "" false T) + mk_app false (mk_term_of gr "Generated" false T) [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @ [Pretty.str "]"])]], Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^ @@ -898,12 +1004,12 @@ structure P = OuterParse and K = OuterKeyword; -fun strip_newlines s = implode (fst (take_suffix (equal "\n") - (snd (take_prefix (equal "\n") (explode s))))) ^ "\n"; +fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ") + (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n"; val parse_attach = Scan.repeat (P.$$$ "attach" |-- Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" -- - (P.verbatim >> strip_newlines)); + (P.verbatim >> strip_whitespace)); val assoc_typeP = OuterSyntax.command "types_code" @@ -924,24 +1030,44 @@ (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx, aux))) xs) thy))); -val generate_codeP = - OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl - (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- - Scan.optional (P.$$$ "[" |-- P.enum "," P.xname --| P.$$$ "]") (!mode) -- - Scan.repeat1 (P.name --| P.$$$ "=" -- P.term) >> - (fn ((opt_fname, mode'), xs) => Toplevel.theory (fn thy => - let val code = setmp mode mode' (generate_code thy) xs - in ((case opt_fname of - NONE => use_text Context.ml_output false - (space_implode "\n" (map snd code) ^ "\nopen Generated;\n") - | SOME fname => - if "modular" mem mode' then - app (fn (name, s) => File.write - (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s) - (("ROOT", implode (map (fn (name, _) => - "use \"" ^ name ^ ".ML\";\n") code)) :: code) - else File.write (Path.unpack fname) (snd (hd code))); thy) - end))); +fun parse_code lib = + Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) -- + (if lib then Scan.optional P.name "" else P.name) -- + Scan.option (P.$$$ "file" |-- P.name) -- + (if lib then Scan.succeed [] + else Scan.optional (P.$$$ "imports" |-- Scan.repeat1 P.name) []) --| + P.$$$ "contains" -- + ( Scan.repeat1 (P.name --| P.$$$ "=" -- P.term) + || Scan.repeat1 (P.term >> pair "")) >> + (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy => + let + val mode'' = if lib then "library" ins (mode' \ "library") + else mode' \ "library"; + val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs + in ((case opt_fname of + NONE => use_text Context.ml_output false + (space_implode "\n" (map snd code)) + | SOME fname => + if lib then + app (fn (name, s) => File.write + (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s) + (("ROOT", implode (map (fn (name, _) => + "use \"" ^ name ^ ".ML\";\n") code)) :: code) + else File.write (Path.unpack fname) (snd (hd code))); + if lib then thy + else map_modules (fn graphs => + Symtab.update ((module, gr), graphs)) thy) + end)); + +val code_libraryP = + OuterSyntax.command "code_library" + "generates code for terms (one structure for each theory)" K.thy_decl + (parse_code true); + +val code_moduleP = + OuterSyntax.command "code_module" + "generates code for terms (single structure, incremental)" K.thy_decl + (parse_code false); val params = [("size", P.nat >> (K o set_size)), @@ -974,9 +1100,9 @@ (map (fn f => f (Toplevel.sign_of st))) ps, [])) (get_test_params (Toplevel.theory_of st), [])) g st))); -val _ = OuterSyntax.add_keywords ["attach"]; +val _ = OuterSyntax.add_keywords ["attach", "file", "contains"]; val _ = OuterSyntax.add_parsers - [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP]; + [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP]; end;