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 |
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; |