src/Pure/codegen.ML
changeset 16769 7f188f2127f7
parent 16649 d88271eb5b26
child 17057 0934ac31985f
equal deleted inserted replaced
16768:37636be4cbd1 16769:7f188f2127f7
    13   val margin : int ref
    13   val margin : int ref
    14 
    14 
    15   datatype 'a mixfix =
    15   datatype 'a mixfix =
    16       Arg
    16       Arg
    17     | Ignore
    17     | Ignore
       
    18     | Module
    18     | Pretty of Pretty.T
    19     | Pretty of Pretty.T
    19     | Quote of 'a;
    20     | Quote of 'a;
    20 
    21 
    21   type deftab
    22   type deftab
    22   type codegr
    23   type codegr
    28   val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
    29   val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
    29   val preprocess: theory -> thm list -> thm list
    30   val preprocess: theory -> thm list -> thm list
    30   val print_codegens: theory -> unit
    31   val print_codegens: theory -> unit
    31   val generate_code: theory -> (string * string) list -> (string * string) list
    32   val generate_code: theory -> (string * string) list -> (string * string) list
    32   val generate_code_i: theory -> (string * term) list -> (string * string) list
    33   val generate_code_i: theory -> (string * term) list -> (string * string) list
    33   val assoc_consts: (xstring * string option * term mixfix list) list -> theory -> theory
    34   val assoc_consts: (xstring * string option * (term mixfix list *
    34   val assoc_consts_i: (xstring * typ option * term mixfix list) list -> theory -> theory
    35     (string * string) list)) list -> theory -> theory
    35   val assoc_types: (xstring * typ mixfix list) list -> theory -> theory
    36   val assoc_consts_i: (xstring * typ option * (term mixfix list *
    36   val get_assoc_code: theory -> string -> typ -> term mixfix list option
    37     (string * string) list)) list -> theory -> theory
    37   val get_assoc_type: theory -> string -> typ mixfix list option
    38   val assoc_types: (xstring * (typ mixfix list *
       
    39     (string * string) list)) list -> theory -> theory
       
    40   val get_assoc_code: theory -> string -> typ ->
       
    41     (term mixfix list * (string * string) list) option
       
    42   val get_assoc_type: theory -> string ->
       
    43     (typ mixfix list * (string * string) list) option
    38   val invoke_codegen: theory -> deftab -> string -> string -> bool ->
    44   val invoke_codegen: theory -> deftab -> string -> string -> bool ->
    39     codegr * term -> codegr * Pretty.T
    45     codegr * term -> codegr * Pretty.T
    40   val invoke_tycodegen: theory -> deftab -> string -> string -> bool ->
    46   val invoke_tycodegen: theory -> deftab -> string -> string -> bool ->
    41     codegr * typ -> codegr * Pretty.T
    47     codegr * typ -> codegr * Pretty.T
    42   val mk_id: string -> string
    48   val mk_id: string -> string
    77 (**** Mixfix syntax ****)
    83 (**** Mixfix syntax ****)
    78 
    84 
    79 datatype 'a mixfix =
    85 datatype 'a mixfix =
    80     Arg
    86     Arg
    81   | Ignore
    87   | Ignore
       
    88   | Module
    82   | Pretty of Pretty.T
    89   | Pretty of Pretty.T
    83   | Quote of 'a;
    90   | Quote of 'a;
    84 
    91 
    85 fun is_arg Arg = true
    92 fun is_arg Arg = true
    86   | is_arg Ignore = true
    93   | is_arg Ignore = true
   162 (struct
   169 (struct
   163   val name = "Pure/codegen";
   170   val name = "Pure/codegen";
   164   type T =
   171   type T =
   165     {codegens : (string * term codegen) list,
   172     {codegens : (string * term codegen) list,
   166      tycodegens : (string * typ codegen) list,
   173      tycodegens : (string * typ codegen) list,
   167      consts : ((string * typ) * term mixfix list) list,
   174      consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
   168      types : (string * typ mixfix list) list,
   175      types : (string * (typ mixfix list * (string * string) list)) list,
   169      attrs: (string * (Args.T list -> theory attribute * Args.T list)) list,
   176      attrs: (string * (Args.T list -> theory attribute * Args.T list)) list,
   170      preprocs: (stamp * (theory -> thm list -> thm list)) list,
   177      preprocs: (stamp * (theory -> thm list -> thm list)) list,
   171      test_params: test_params};
   178      test_params: test_params};
   172 
   179 
   173   val empty =
   180   val empty =
   453   Sign.typ_instance thy (T1, Type.varifyT T2);
   460   Sign.typ_instance thy (T1, Type.varifyT T2);
   454 
   461 
   455 fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) =>
   462 fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) =>
   456   s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
   463   s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
   457 
   464 
       
   465 fun get_aux_code xs = List.mapPartial (fn (m, code) =>
       
   466   if m = "" orelse m mem !mode then SOME code else NONE) xs;
       
   467 
   458 fun mk_deftab thy =
   468 fun mk_deftab thy =
   459   let
   469   let
   460     val axmss = map (fn thy' =>
   470     val axmss = map (fn thy' =>
   461       (Context.theory_name thy', snd (#axioms (Theory.rep_theory thy'))))
   471       (Context.theory_name thy', snd (#axioms (Theory.rep_theory thy'))))
   462       (thy :: Theory.ancestors_of thy);
   472       (thy :: Theory.ancestors_of thy);
   514 
   524 
   515 fun pretty_fn [] p = [p]
   525 fun pretty_fn [] p = [p]
   516   | pretty_fn (x::xs) p = Pretty.str ("fn " ^ x ^ " =>") ::
   526   | pretty_fn (x::xs) p = Pretty.str ("fn " ^ x ^ " =>") ::
   517       Pretty.brk 1 :: pretty_fn xs p;
   527       Pretty.brk 1 :: pretty_fn xs p;
   518 
   528 
   519 fun pretty_mixfix [] [] _ = []
   529 fun pretty_mixfix _ _ [] [] _ = []
   520   | pretty_mixfix (Arg :: ms) (p :: ps) qs = p :: pretty_mixfix ms ps qs
   530   | pretty_mixfix module module' (Arg :: ms) (p :: ps) qs =
   521   | pretty_mixfix (Ignore :: ms) ps qs = pretty_mixfix ms ps qs
   531       p :: pretty_mixfix module module' ms ps qs
   522   | pretty_mixfix (Pretty p :: ms) ps qs = p :: pretty_mixfix ms ps qs
   532   | pretty_mixfix module module' (Ignore :: ms) ps qs =
   523   | pretty_mixfix (Quote _ :: ms) ps (q :: qs) = q :: pretty_mixfix ms ps qs;
   533       pretty_mixfix module module' ms ps qs
       
   534   | pretty_mixfix module module' (Module :: ms) ps qs =
       
   535       (if "modular" mem !mode andalso module <> module'
       
   536        then cons (Pretty.str (module' ^ ".")) else I)
       
   537       (pretty_mixfix module module' ms ps qs)
       
   538   | pretty_mixfix module module' (Pretty p :: ms) ps qs =
       
   539       p :: pretty_mixfix module module' ms ps qs
       
   540   | pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) =
       
   541       q :: pretty_mixfix module module' ms ps qs;
   524 
   542 
   525 
   543 
   526 (**** default code generators ****)
   544 (**** default code generators ****)
   527 
   545 
   528 fun eta_expand t ts i =
   546 fun eta_expand t ts i =
   565           val (gr'', _) = invoke_tycodegen thy defs dep thyname false (gr', T)
   583           val (gr'', _) = invoke_tycodegen thy defs dep thyname false (gr', T)
   566         in SOME (gr'', mk_app brack (Pretty.str s) ps) end
   584         in SOME (gr'', mk_app brack (Pretty.str s) ps) end
   567 
   585 
   568     | Const (s, T) =>
   586     | Const (s, T) =>
   569       (case get_assoc_code thy s T of
   587       (case get_assoc_code thy s T of
   570          SOME ms =>
   588          SOME (ms, aux) =>
   571            let val i = num_args ms
   589            let val i = num_args ms
   572            in if length ts < i then
   590            in if length ts < i then
   573                default_codegen thy defs gr dep thyname brack (eta_expand u ts i)
   591                default_codegen thy defs gr dep thyname brack (eta_expand u ts i)
   574              else
   592              else
   575                let
   593                let
   576                  val (ts1, ts2) = args_of ms ts;
   594                  val (ts1, ts2) = args_of ms ts;
   577                  val (gr1, ps1) = codegens false (gr, ts1);
   595                  val (gr1, ps1) = codegens false (gr, ts1);
   578                  val (gr2, ps2) = codegens true (gr1, ts2);
   596                  val (gr2, ps2) = codegens true (gr1, ts2);
   579                  val (gr3, ps3) = codegens false (gr2, quotes_of ms);
   597                  val (gr3, ps3) = codegens false (gr2, quotes_of ms);
   580                in
   598                  val (thyname', suffix) = (case get_defn thy defs s T of
   581                  SOME (gr3, mk_app brack (Pretty.block (pretty_mixfix ms ps1 ps3)) ps2)
   599                      NONE => (thyname_of_const s thy, "")
       
   600                    | SOME ((U, (thyname', _)), NONE) => (thyname', "")
       
   601                    | SOME ((U, (thyname', _)), SOME i) =>
       
   602                        (thyname', "_def" ^ string_of_int i));
       
   603                  val node_id = s ^ suffix;
       
   604                  val p = mk_app brack (Pretty.block
       
   605                    (pretty_mixfix thyname thyname' ms ps1 ps3)) ps2
       
   606                in SOME (case try (Graph.get_node gr3) node_id of
       
   607                    NONE => (case get_aux_code aux of
       
   608                        [] => (gr3, p)
       
   609                      | xs => (Graph.add_edge (node_id, dep) (Graph.new_node
       
   610                          (node_id, (NONE, thyname', space_implode "\n" xs ^ "\n")) gr3), p))
       
   611                  | SOME _ => (Graph.add_edge (node_id, dep) gr3, p))
   582                end
   612                end
   583            end
   613            end
   584        | NONE => (case get_defn thy defs s T of
   614        | NONE => (case get_defn thy defs s T of
   585            NONE => NONE
   615            NONE => NONE
   586          | SOME ((U, (thyname', (args, rhs))), k) =>
   616          | SOME ((U, (thyname', (args, rhs))), k) =>
   635   | default_tycodegen thy defs gr dep thyname brack (TFree (s, _)) =
   665   | default_tycodegen thy defs gr dep thyname brack (TFree (s, _)) =
   636       SOME (gr, Pretty.str s)
   666       SOME (gr, Pretty.str s)
   637   | default_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
   667   | default_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
   638       (case assoc (#types (CodegenData.get thy), s) of
   668       (case assoc (#types (CodegenData.get thy), s) of
   639          NONE => NONE
   669          NONE => NONE
   640        | SOME ms =>
   670        | SOME (ms, aux) =>
   641            let
   671            let
   642              val (gr', ps) = foldl_map
   672              val (gr', ps) = foldl_map
   643                (invoke_tycodegen thy defs dep thyname false)
   673                (invoke_tycodegen thy defs dep thyname false)
   644                (gr, fst (args_of ms Ts));
   674                (gr, fst (args_of ms Ts));
   645              val (gr'', qs) = foldl_map
   675              val (gr'', qs) = foldl_map
   646                (invoke_tycodegen thy defs dep thyname false)
   676                (invoke_tycodegen thy defs dep thyname false)
   647                (gr', quotes_of ms)
   677                (gr', quotes_of ms);
   648            in SOME (gr'', Pretty.block (pretty_mixfix ms ps qs)) end);
   678              val thyname' = thyname_of_type s thy;
       
   679              val node_id = s ^ " (type)";
       
   680              val p = Pretty.block (pretty_mixfix thyname thyname' ms ps qs)
       
   681            in SOME (case try (Graph.get_node gr'') node_id of
       
   682                NONE => (case get_aux_code aux of
       
   683                    [] => (gr'', p)
       
   684                  | xs => (Graph.add_edge (node_id, dep) (Graph.new_node
       
   685                      (node_id, (NONE, thyname', space_implode "\n" xs ^ "\n")) gr''), p))
       
   686              | SOME _ => (Graph.add_edge (node_id, dep) gr'', p))
       
   687            end);
   649 
   688 
   650 val _ = Context.add_setup
   689 val _ = Context.add_setup
   651  [add_codegen "default" default_codegen,
   690  [add_codegen "default" default_codegen,
   652   add_tycodegen "default" default_tycodegen];
   691   add_tycodegen "default" default_tycodegen];
   653 
   692 
   825 
   864 
   826 fun parse_mixfix rd s =
   865 fun parse_mixfix rd s =
   827   (case Scan.finite Symbol.stopper (Scan.repeat
   866   (case Scan.finite Symbol.stopper (Scan.repeat
   828      (   $$ "_" >> K Arg
   867      (   $$ "_" >> K Arg
   829       || $$ "?" >> K Ignore
   868       || $$ "?" >> K Ignore
       
   869       || $$ "\\<module>" >> K Module
   830       || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
   870       || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
   831       || $$ "{" |-- $$ "*" |-- Scan.repeat1
   871       || $$ "{" |-- $$ "*" |-- Scan.repeat1
   832            (   $$ "'" |-- Scan.one Symbol.not_eof
   872            (   $$ "'" |-- Scan.one Symbol.not_eof
   833             || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
   873             || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
   834          $$ "*" --| $$ "}" >> (Quote o rd o implode)
   874          $$ "*" --| $$ "}" >> (Quote o rd o implode)
   835       || Scan.repeat1
   875       || Scan.repeat1
   836            (   $$ "'" |-- Scan.one Symbol.not_eof
   876            (   $$ "'" |-- Scan.one Symbol.not_eof
   837             || Scan.unless ($$ "_" || $$ "?" || $$ "/" || $$ "{" |-- $$ "*")
   877             || Scan.unless ($$ "_" || $$ "?" || $$ "\\<module>" || $$ "/" || $$ "{" |-- $$ "*")
   838                  (Scan.one Symbol.not_eof)) >> (Pretty o str o implode)))
   878                  (Scan.one Symbol.not_eof)) >> (Pretty o str o implode)))
   839        (Symbol.explode s) of
   879        (Symbol.explode s) of
   840      (p, []) => p
   880      (p, []) => p
   841    | _ => error ("Malformed annotation: " ^ quote s));
   881    | _ => error ("Malformed annotation: " ^ quote s));
   842 
   882 
   843 val _ = Context.add_setup
   883 val _ = Context.add_setup
   844   [assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")]];
   884   [assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
       
   885      [("term_of",
       
   886        "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
       
   887       ("test",
       
   888        "fun gen_fun_type _ G i =\n\
       
   889        \  let\n\
       
   890        \    val f = ref (fn x => raise ERROR);\n\
       
   891        \    val _ = (f := (fn x =>\n\
       
   892        \      let\n\
       
   893        \        val y = G i;\n\
       
   894        \        val f' = !f\n\
       
   895        \      in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\
       
   896        \  in (fn x => !f x) end;\n")]))]];
   845 
   897 
   846 
   898 
   847 structure P = OuterParse and K = OuterSyntax.Keyword;
   899 structure P = OuterParse and K = OuterSyntax.Keyword;
       
   900 
       
   901 fun strip_newlines s = implode (fst (take_suffix (equal "\n")
       
   902   (snd (take_prefix (equal "\n") (explode s))))) ^ "\n";
       
   903 
       
   904 val parse_attach = Scan.repeat (P.$$$ "attach" |--
       
   905   Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
       
   906     (P.verbatim >> strip_newlines));
   848 
   907 
   849 val assoc_typeP =
   908 val assoc_typeP =
   850   OuterSyntax.command "types_code"
   909   OuterSyntax.command "types_code"
   851   "associate types with target language types" K.thy_decl
   910   "associate types with target language types" K.thy_decl
   852     (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")") >>
   911     (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
   853      (fn xs => Toplevel.theory (fn thy => assoc_types
   912      (fn xs => Toplevel.theory (fn thy => assoc_types
   854        (map (fn (name, mfx) => (name, parse_mixfix
   913        (map (fn ((name, mfx), aux) => (name, (parse_mixfix
   855          (typ_of o read_ctyp thy) mfx)) xs) thy)));
   914          (typ_of o read_ctyp thy) mfx, aux))) xs) thy)));
   856 
   915 
   857 val assoc_constP =
   916 val assoc_constP =
   858   OuterSyntax.command "consts_code"
   917   OuterSyntax.command "consts_code"
   859   "associate constants with target language code" K.thy_decl
   918   "associate constants with target language code" K.thy_decl
   860     (Scan.repeat1
   919     (Scan.repeat1
   861        (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --|
   920        (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --|
   862         P.$$$ "(" -- P.string --| P.$$$ ")") >>
   921         P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
   863      (fn xs => Toplevel.theory (fn thy => assoc_consts
   922      (fn xs => Toplevel.theory (fn thy => assoc_consts
   864        (map (fn ((name, optype), mfx) => (name, optype, parse_mixfix
   923        (map (fn (((name, optype), mfx), aux) => (name, optype, (parse_mixfix
   865          (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx))
   924          (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx, aux)))
   866            xs) thy)));
   925            xs) thy)));
   867 
   926 
   868 val generate_codeP =
   927 val generate_codeP =
   869   OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl
   928   OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl
   870     (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
   929     (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
   913     (fn (ps, g) => Toplevel.keep (fn st =>
   972     (fn (ps, g) => Toplevel.keep (fn st =>
   914       test_goal (app (getOpt (Option.map
   973       test_goal (app (getOpt (Option.map
   915           (map (fn f => f (Toplevel.sign_of st))) ps, []))
   974           (map (fn f => f (Toplevel.sign_of st))) ps, []))
   916         (get_test_params (Toplevel.theory_of st), [])) g st)));
   975         (get_test_params (Toplevel.theory_of st), [])) g st)));
   917 
   976 
       
   977 val _ = OuterSyntax.add_keywords ["attach"];
       
   978 
   918 val _ = OuterSyntax.add_parsers
   979 val _ = OuterSyntax.add_parsers
   919   [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP];
   980   [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP];
   920 
   981 
   921 end;
   982 end;