# HG changeset patch # User berghofe # Date 1121161284 -7200 # Node ID 7f188f2127f7ba402ca3ca19a077a81b79d104cc # Parent 37636be4cbd150f0f2f33766adc515e5575c588c Implemented mechanism for attaching auxiliary code to consts_code and types_code declarations. diff -r 37636be4cbd1 -r 7f188f2127f7 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Mon Jul 11 19:59:11 2005 +0200 +++ b/src/Pure/codegen.ML Tue Jul 12 11:41:24 2005 +0200 @@ -15,6 +15,7 @@ datatype 'a mixfix = Arg | Ignore + | Module | Pretty of Pretty.T | Quote of 'a; @@ -30,11 +31,16 @@ 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 assoc_consts: (xstring * string option * term mixfix list) list -> theory -> theory - val assoc_consts_i: (xstring * typ option * term mixfix list) list -> theory -> theory - val assoc_types: (xstring * typ mixfix list) list -> theory -> theory - val get_assoc_code: theory -> string -> typ -> term mixfix list option - val get_assoc_type: theory -> string -> typ mixfix list option + 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 * + (string * string) list)) list -> theory -> theory + val assoc_types: (xstring * (typ mixfix list * + (string * string) list)) list -> theory -> theory + val get_assoc_code: theory -> string -> typ -> + (term mixfix list * (string * string) list) option + val get_assoc_type: theory -> string -> + (typ mixfix list * (string * string) list) option val invoke_codegen: theory -> deftab -> string -> string -> bool -> codegr * term -> codegr * Pretty.T val invoke_tycodegen: theory -> deftab -> string -> string -> bool -> @@ -79,6 +85,7 @@ datatype 'a mixfix = Arg | Ignore + | Module | Pretty of Pretty.T | Quote of 'a; @@ -164,8 +171,8 @@ type T = {codegens : (string * term codegen) list, tycodegens : (string * typ codegen) list, - consts : ((string * typ) * term mixfix list) list, - types : (string * typ mixfix list) list, + consts : ((string * typ) * (term mixfix list * (string * string) list)) list, + 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, test_params: test_params}; @@ -455,6 +462,9 @@ fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) => s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy))); +fun get_aux_code xs = List.mapPartial (fn (m, code) => + if m = "" orelse m mem !mode then SOME code else NONE) xs; + fun mk_deftab thy = let val axmss = map (fn thy' => @@ -516,11 +526,19 @@ | pretty_fn (x::xs) p = Pretty.str ("fn " ^ x ^ " =>") :: Pretty.brk 1 :: pretty_fn xs p; -fun pretty_mixfix [] [] _ = [] - | pretty_mixfix (Arg :: ms) (p :: ps) qs = p :: pretty_mixfix ms ps qs - | pretty_mixfix (Ignore :: ms) ps qs = pretty_mixfix ms ps qs - | pretty_mixfix (Pretty p :: ms) ps qs = p :: pretty_mixfix ms ps qs - | pretty_mixfix (Quote _ :: ms) ps (q :: qs) = q :: pretty_mixfix ms ps qs; +fun pretty_mixfix _ _ [] [] _ = [] + | pretty_mixfix module module' (Arg :: ms) (p :: ps) qs = + p :: pretty_mixfix module module' ms ps qs + | 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' + then cons (Pretty.str (module' ^ ".")) else I) + (pretty_mixfix module module' ms ps qs) + | pretty_mixfix module module' (Pretty p :: ms) ps qs = + p :: pretty_mixfix module module' ms ps qs + | pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) = + q :: pretty_mixfix module module' ms ps qs; (**** default code generators ****) @@ -567,7 +585,7 @@ | Const (s, T) => (case get_assoc_code thy s T of - SOME ms => + 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) @@ -577,8 +595,20 @@ val (gr1, ps1) = codegens false (gr, ts1); val (gr2, ps2) = codegens true (gr1, ts2); val (gr3, ps3) = codegens false (gr2, quotes_of ms); - in - SOME (gr3, mk_app brack (Pretty.block (pretty_mixfix ms ps1 ps3)) ps2) + 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 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 + 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)) end end | NONE => (case get_defn thy defs s T of @@ -637,15 +667,24 @@ | default_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) = (case assoc (#types (CodegenData.get thy), s) of NONE => NONE - | SOME ms => + | SOME (ms, aux) => let val (gr', ps) = foldl_map (invoke_tycodegen thy defs dep thyname false) (gr, fst (args_of ms Ts)); val (gr'', qs) = foldl_map (invoke_tycodegen thy defs dep thyname false) - (gr', quotes_of ms) - in SOME (gr'', Pretty.block (pretty_mixfix ms ps qs)) end); + (gr', quotes_of ms); + val thyname' = thyname_of_type s thy; + 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 + 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)) + end); val _ = Context.add_setup [add_codegen "default" default_codegen, @@ -827,6 +866,7 @@ (case Scan.finite Symbol.stopper (Scan.repeat ( $$ "_" >> K Arg || $$ "?" >> K Ignore + || $$ "\\" >> K Module || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length) || $$ "{" |-- $$ "*" |-- Scan.repeat1 ( $$ "'" |-- Scan.one Symbol.not_eof @@ -834,35 +874,54 @@ $$ "*" --| $$ "}" >> (Quote o rd o implode) || Scan.repeat1 ( $$ "'" |-- Scan.one Symbol.not_eof - || Scan.unless ($$ "_" || $$ "?" || $$ "/" || $$ "{" |-- $$ "*") + || Scan.unless ($$ "_" || $$ "?" || $$ "\\" || $$ "/" || $$ "{" |-- $$ "*") (Scan.one Symbol.not_eof)) >> (Pretty o str o implode))) (Symbol.explode s) of (p, []) => p | _ => error ("Malformed annotation: " ^ quote s)); val _ = Context.add_setup - [assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")]]; + [assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)", + [("term_of", + "fun term_of_fun_type _ T _ U _ = Free (\"\", T --> U);\n"), + ("test", + "fun gen_fun_type _ G i =\n\ + \ let\n\ + \ val f = ref (fn x => raise ERROR);\n\ + \ val _ = (f := (fn x =>\n\ + \ let\n\ + \ val y = G i;\n\ + \ val f' = !f\n\ + \ in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\ + \ in (fn x => !f x) end;\n")]))]]; structure P = OuterParse and K = OuterSyntax.Keyword; +fun strip_newlines s = implode (fst (take_suffix (equal "\n") + (snd (take_prefix (equal "\n") (explode s))))) ^ "\n"; + +val parse_attach = Scan.repeat (P.$$$ "attach" |-- + Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" -- + (P.verbatim >> strip_newlines)); + val assoc_typeP = OuterSyntax.command "types_code" "associate types with target language types" K.thy_decl - (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")") >> + (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >> (fn xs => Toplevel.theory (fn thy => assoc_types - (map (fn (name, mfx) => (name, parse_mixfix - (typ_of o read_ctyp thy) mfx)) xs) thy))); + (map (fn ((name, mfx), aux) => (name, (parse_mixfix + (typ_of o read_ctyp thy) mfx, aux))) xs) thy))); val assoc_constP = OuterSyntax.command "consts_code" "associate constants with target language code" K.thy_decl (Scan.repeat1 (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --| - P.$$$ "(" -- P.string --| P.$$$ ")") >> + P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >> (fn xs => Toplevel.theory (fn thy => assoc_consts - (map (fn ((name, optype), mfx) => (name, optype, parse_mixfix - (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx)) + (map (fn (((name, optype), mfx), aux) => (name, optype, (parse_mixfix + (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx, aux))) xs) thy))); val generate_codeP = @@ -915,6 +974,8 @@ (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_parsers [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP];