10 val target_OCaml: string |
10 val target_OCaml: string |
11 val evaluation_code_of: theory -> string -> string |
11 val evaluation_code_of: theory -> string -> string |
12 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list |
12 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list |
13 val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T) |
13 val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T) |
14 -> Code_Printer.fixity -> 'a list -> Pretty.T option |
14 -> Code_Printer.fixity -> 'a list -> Pretty.T option |
15 val check_SML: theory -> unit |
|
16 val check_OCaml: theory -> unit |
|
17 val setup: theory -> theory |
15 val setup: theory -> theory |
18 end; |
16 end; |
19 |
17 |
20 structure Code_ML : CODE_ML = |
18 structure Code_ML : CODE_ML = |
21 struct |
19 struct |
950 fun evaluation_code_of thy target struct_name = |
948 fun evaluation_code_of thy target struct_name = |
951 Code_Target.serialize_custom thy (target, fn _ => fn [] => |
949 Code_Target.serialize_custom thy (target, fn _ => fn [] => |
952 serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true); |
950 serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true); |
953 |
951 |
954 |
952 |
955 (** formal checking of compiled code **) |
|
956 |
|
957 fun check_SML thy = Code_Target.external_check thy target_SML |
|
958 "ISABELLE_PROCESS" (fn p => Path.append p (Path.explode "ROOT.ML")) |
|
959 (fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure"); |
|
960 |
|
961 fun check_OCaml thy = Code_Target.external_check thy target_OCaml |
|
962 "EXEC_OCAML" (fn p => Path.append p (Path.explode "ROOT.ocaml")) |
|
963 (fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p); |
|
964 |
|
965 |
|
966 (** Isar setup **) |
953 (** Isar setup **) |
967 |
954 |
968 fun isar_serializer_sml module_name = |
955 fun isar_serializer_sml module_name = |
969 Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true |
956 Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true |
970 >> (fn with_signatures => serialize_ml target_SML |
957 >> (fn with_signatures => serialize_ml target_SML |
975 >> (fn with_signatures => serialize_ml target_OCaml |
962 >> (fn with_signatures => serialize_ml target_OCaml |
976 print_ocaml_module print_ocaml_stmt module_name with_signatures)); |
963 print_ocaml_module print_ocaml_stmt module_name with_signatures)); |
977 |
964 |
978 val setup = |
965 val setup = |
979 Code_Target.add_target |
966 Code_Target.add_target |
980 (target_SML, { serializer = isar_serializer_sml, literals = literals_sml, check = () }) |
967 (target_SML, { serializer = isar_serializer_sml, literals = literals_sml, |
|
968 check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), |
|
969 make_command = fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure" } }) |
981 #> Code_Target.add_target |
970 #> Code_Target.add_target |
982 (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml, check = () }) |
971 (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml, |
|
972 check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"), |
|
973 make_command = fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p } }) |
983 #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
974 #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
984 brackify_infix (1, R) fxy ( |
975 brackify_infix (1, R) fxy ( |
985 print_typ (INFX (1, X)) ty1, |
976 print_typ (INFX (1, X)) ty1, |
986 str "->", |
977 str "->", |
987 print_typ (INFX (1, R)) ty2 |
978 print_typ (INFX (1, R)) ty2 |