src/Pure/codegen.ML

   val margin : int ref
 
   datatype 'a mixfix =
       Arg
     | Ignore
+    | Module
     | Pretty of Pretty.T
     | Quote of 'a;
 
   type deftab
   type codegr

   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 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 ->
     codegr * typ -> codegr * Pretty.T
   val mk_id: string -> string

 (**** Mixfix syntax ****)
 
 datatype 'a mixfix =
     Arg
   | Ignore
+  | Module
   | Pretty of Pretty.T
   | Quote of 'a;
 
 fun is_arg Arg = true
   | is_arg Ignore = true

 (struct
   val name = "Pure/codegen";
   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};
 
   val empty =

   Sign.typ_instance thy (T1, Type.varifyT T2);
 
 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' =>
       (Context.theory_name thy', snd (#axioms (Theory.rep_theory thy'))))
       (thy :: Theory.ancestors_of thy);

 
 fun pretty_fn [] p = [p]
   | 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 ****)
 
 fun eta_expand t ts i =

           val (gr'', _) = invoke_tycodegen thy defs dep thyname false (gr', T)
         in SOME (gr'', mk_app brack (Pretty.str s) ps) end
 
     | 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)
              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);
-               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
            NONE => NONE
          | SOME ((U, (thyname', (args, rhs))), k) =>

   | default_tycodegen thy defs gr dep thyname brack (TFree (s, _)) =
       SOME (gr, Pretty.str s)
   | 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,
   add_tycodegen "default" default_tycodegen];
 

 
 fun parse_mixfix rd s =
   (case Scan.finite Symbol.stopper (Scan.repeat
      (   $$ "_" >> K Arg
       || $$ "?" >> K Ignore
+      || $$ "\\<module>" >> K Module
       || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
       || $$ "{" |-- $$ "*" |-- Scan.repeat1
            (   $$ "'" |-- Scan.one Symbol.not_eof
             || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
          $$ "*" --| $$ "}" >> (Quote o rd o implode)
       || Scan.repeat1
            (   $$ "'" |-- Scan.one Symbol.not_eof
-            || Scan.unless ($$ "_" || $$ "?" || $$ "/" || $$ "{" |-- $$ "*")
+            || Scan.unless ($$ "_" || $$ "?" || $$ "\\<module>" || $$ "/" || $$ "{" |-- $$ "*")
                  (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 (\"<function>\", 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 =
   OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl
     (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --

     (fn (ps, g) => Toplevel.keep (fn st =>
       test_goal (app (getOpt (Option.map
           (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];
 
 end;