23 val add_pretty_list_string: string -> string -> string |
23 val add_pretty_list_string: string -> string -> string |
24 -> string -> string list -> theory -> theory; |
24 -> string -> string list -> theory -> theory; |
25 val add_pretty_char: string -> string -> string list -> theory -> theory |
25 val add_pretty_char: string -> string -> string list -> theory -> theory |
26 val add_pretty_numeral: string -> bool -> string -> string -> string -> string |
26 val add_pretty_numeral: string -> bool -> string -> string -> string -> string |
27 -> string -> string -> theory -> theory; |
27 -> string -> string -> theory -> theory; |
28 val add_pretty_ml_string: string -> string -> string list -> string |
28 val add_pretty_message: string -> string -> string list -> string |
29 -> string -> string -> theory -> theory; |
29 -> string -> string -> theory -> theory; |
30 val add_pretty_imperative_monad_bind: string -> string -> theory -> theory; |
|
31 |
30 |
32 val allow_exception: string -> theory -> theory; |
31 val allow_exception: string -> theory -> theory; |
33 |
32 |
34 type serializer; |
33 type serializer; |
35 val add_serializer: string * serializer -> theory -> theory; |
34 val add_serializer: string * serializer -> theory -> theory; |
36 val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list |
35 val get_serializer: theory -> string -> bool -> string option |
|
36 -> string option -> Args.T list |
37 -> string list option -> CodeThingol.code -> unit; |
37 -> string list option -> CodeThingol.code -> unit; |
38 val assert_serializer: theory -> string -> string; |
38 val assert_serializer: theory -> string -> string; |
39 |
39 |
40 val eval_verbose: bool ref; |
40 val eval_verbose: bool ref; |
41 val eval_invoke: theory -> (string * (unit -> 'a) option ref) |
41 val eval_invoke: theory -> (string * (unit -> 'a) option ref) |
245 | _ => NONE |
247 | _ => NONE |
246 else NONE |
248 else NONE |
247 | dest_numeral _ = NONE; |
249 | dest_numeral _ = NONE; |
248 in dest_numeral end; |
250 in dest_numeral end; |
249 |
251 |
250 fun implode_monad c_mbind c_kbind t = |
252 fun implode_monad c_bind t = |
251 let |
253 let |
252 fun dest_monad (IConst (c, _) `$ t1 `$ t2) = |
254 fun dest_monad (IConst (c, _) `$ t1 `$ t2) = |
253 if c = c_mbind |
255 if c = c_bind |
254 then case CodeThingol.split_abs t2 |
256 then case CodeThingol.split_abs t2 |
255 of SOME (((v, pat), ty), t') => SOME ((SOME (((SOME v, pat), ty), true), t1), t') |
257 of SOME (((v, pat), ty), t') => |
|
258 SOME ((SOME (((SOME v, pat), ty), true), t1), t') |
256 | NONE => NONE |
259 | NONE => NONE |
257 else if c = c_kbind |
|
258 then SOME ((NONE, t1), t2) |
|
259 else NONE |
260 else NONE |
260 | dest_monad t = case CodeThingol.split_let t |
261 | dest_monad t = case CodeThingol.split_let t |
261 of SOME (((pat, ty), tbind), t') => SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t') |
262 of SOME (((pat, ty), tbind), t') => |
|
263 SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t') |
262 | NONE => NONE; |
264 | NONE => NONE; |
263 in CodeThingol.unfoldr dest_monad t end; |
265 in CodeThingol.unfoldr dest_monad t end; |
264 |
266 |
265 |
267 |
266 (** name auxiliary **) |
268 (** name auxiliary **) |
363 fun pr ((v, pat), ty) = |
367 fun pr ((v, pat), ty) = |
364 pr_bind NOBR ((SOME v, pat), ty) |
368 pr_bind NOBR ((SOME v, pat), ty) |
365 #>> (fn p => concat [str "fn", p, str "=>"]); |
369 #>> (fn p => concat [str "fn", p, str "=>"]); |
366 val (ps, vars') = fold_map pr binds vars; |
370 val (ps, vars') = fold_map pr binds vars; |
367 in brackets (ps @ [pr_term lhs vars' NOBR t']) end |
371 in brackets (ps @ [pr_term lhs vars' NOBR t']) end |
368 | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0 |
372 | pr_term lhs vars fxy (ICase (cases as (_, t0))) = |
|
373 (case CodeThingol.unfold_const_app t0 |
369 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) |
374 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) |
370 then pr_case vars fxy cases |
375 then pr_case vars fxy cases |
371 else pr_app lhs vars fxy c_ts |
376 else pr_app lhs vars fxy c_ts |
372 | NONE => pr_case vars fxy cases) |
377 | NONE => pr_case vars fxy cases) |
373 and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) = |
378 and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) = |
378 else if k = length ts then |
383 else if k = length ts then |
379 [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)] |
384 [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)] |
380 else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else |
385 else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else |
381 (str o deresolv) c |
386 (str o deresolv) c |
382 :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts |
387 :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts |
383 and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars |
388 and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax |
|
389 labelled_name is_cons lhs vars |
384 and pr_bind' ((NONE, NONE), _) = str "_" |
390 and pr_bind' ((NONE, NONE), _) = str "_" |
385 | pr_bind' ((SOME v, NONE), _) = str v |
391 | pr_bind' ((SOME v, NONE), _) = str v |
386 | pr_bind' ((NONE, SOME p), _) = p |
392 | pr_bind' ((NONE, SOME p), _) = p |
387 | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p] |
393 | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p] |
388 and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy |
394 and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy |
654 if is_cons c then |
666 if is_cons c then |
655 if length tys = length ts |
667 if length tys = length ts |
656 then case ts |
668 then case ts |
657 of [] => [(str o deresolv) c] |
669 of [] => [(str o deresolv) c] |
658 | [t] => [(str o deresolv) c, pr_term lhs vars BR t] |
670 | [t] => [(str o deresolv) c, pr_term lhs vars BR t] |
659 | _ => [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)] |
671 | _ => [(str o deresolv) c, Pretty.enum "," "(" ")" |
|
672 (map (pr_term lhs vars NOBR) ts)] |
660 else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))] |
673 else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))] |
661 else (str o deresolv) c |
674 else (str o deresolv) c |
662 :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts) |
675 :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts) |
663 and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars |
676 and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax |
|
677 labelled_name is_cons lhs vars |
664 and pr_bind' ((NONE, NONE), _) = str "_" |
678 and pr_bind' ((NONE, NONE), _) = str "_" |
665 | pr_bind' ((SOME v, NONE), _) = str v |
679 | pr_bind' ((SOME v, NONE), _) = str v |
666 | pr_bind' ((NONE, SOME p), _) = p |
680 | pr_bind' ((NONE, SOME p), _) = p |
667 | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v] |
681 | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v] |
668 and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy |
682 and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy |
900 val init_names = Name.make_context reserved_syms; |
924 val init_names = Name.make_context reserved_syms; |
901 val init_module = ((init_names, init_names), Graph.empty); |
925 val init_module = ((init_names, init_names), Graph.empty); |
902 fun map_node [] f = f |
926 fun map_node [] f = f |
903 | map_node (m::ms) f = |
927 | map_node (m::ms) f = |
904 Graph.default_node (m, Module (m, init_module)) |
928 Graph.default_node (m, Module (m, init_module)) |
905 #> Graph.map_node m (fn (Module (dmodlname, (nsp, nodes))) => Module (dmodlname, (nsp, map_node ms f nodes))); |
929 #> Graph.map_node m (fn (Module (dmodlname, (nsp, nodes))) => |
|
930 Module (dmodlname, (nsp, map_node ms f nodes))); |
906 fun map_nsp_yield [] f (nsp, nodes) = |
931 fun map_nsp_yield [] f (nsp, nodes) = |
907 let |
932 let |
908 val (x, nsp') = f nsp |
933 val (x, nsp') = f nsp |
909 in (x, (nsp', nodes)) end |
934 in (x, (nsp', nodes)) end |
910 | map_nsp_yield (m::ms) f (nsp, nodes) = |
935 | map_nsp_yield (m::ms) f (nsp, nodes) = |
934 val (x, nsp_typ') = f nsp_typ |
959 val (x, nsp_typ') = f nsp_typ |
935 in (x, (nsp_fun, nsp_typ')) end; |
960 in (x, (nsp_fun, nsp_typ')) end; |
936 fun mk_funs defs = |
961 fun mk_funs defs = |
937 fold_map |
962 fold_map |
938 (fn (name, CodeThingol.Fun info) => |
963 (fn (name, CodeThingol.Fun info) => |
939 map_nsp_fun (name_def false name) >> (fn base => (base, (name, (apsnd o map) fst info))) |
964 map_nsp_fun (name_def false name) >> |
940 | (name, def) => error ("Function block containing illegal definition: " ^ labelled_name name) |
965 (fn base => (base, (name, (apsnd o map) fst info))) |
|
966 | (name, def) => |
|
967 error ("Function block containing illegal definition: " ^ labelled_name name) |
941 ) defs |
968 ) defs |
942 >> (split_list #> apsnd MLFuns); |
969 >> (split_list #> apsnd MLFuns); |
943 fun mk_datatype defs = |
970 fun mk_datatype defs = |
944 fold_map |
971 fold_map |
945 (fn (name, CodeThingol.Datatype info) => |
972 (fn (name, CodeThingol.Datatype info) => |
946 map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info))) |
973 map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info))) |
947 | (name, CodeThingol.Datatypecons _) => |
974 | (name, CodeThingol.Datatypecons _) => |
948 map_nsp_fun (name_def true name) >> (fn base => (base, NONE)) |
975 map_nsp_fun (name_def true name) >> (fn base => (base, NONE)) |
949 | (name, def) => error ("Datatype block containing illegal definition: " ^ labelled_name name) |
976 | (name, def) => |
|
977 error ("Datatype block containing illegal definition: " ^ labelled_name name) |
950 ) defs |
978 ) defs |
951 >> (split_list #> apsnd (map_filter I |
979 >> (split_list #> apsnd (map_filter I |
952 #> (fn [] => error ("Datatype block without data definition: " ^ (commas o map (labelled_name o fst)) defs) |
980 #> (fn [] => error ("Datatype block without data definition: " |
|
981 ^ (commas o map (labelled_name o fst)) defs) |
953 | infos => MLDatas infos))); |
982 | infos => MLDatas infos))); |
954 fun mk_class defs = |
983 fun mk_class defs = |
955 fold_map |
984 fold_map |
956 (fn (name, CodeThingol.Class info) => |
985 (fn (name, CodeThingol.Class info) => |
957 map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info))) |
986 map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info))) |
958 | (name, CodeThingol.Classrel _) => |
987 | (name, CodeThingol.Classrel _) => |
959 map_nsp_fun (name_def false name) >> (fn base => (base, NONE)) |
988 map_nsp_fun (name_def false name) >> (fn base => (base, NONE)) |
960 | (name, CodeThingol.Classparam _) => |
989 | (name, CodeThingol.Classparam _) => |
961 map_nsp_fun (name_def false name) >> (fn base => (base, NONE)) |
990 map_nsp_fun (name_def false name) >> (fn base => (base, NONE)) |
962 | (name, def) => error ("Class block containing illegal definition: " ^ labelled_name name) |
991 | (name, def) => |
|
992 error ("Class block containing illegal definition: " ^ labelled_name name) |
963 ) defs |
993 ) defs |
964 >> (split_list #> apsnd (map_filter I |
994 >> (split_list #> apsnd (map_filter I |
965 #> (fn [] => error ("Class block without class definition: " ^ (commas o map (labelled_name o fst)) defs) |
995 #> (fn [] => error ("Class block without class definition: " |
|
996 ^ (commas o map (labelled_name o fst)) defs) |
966 | [info] => MLClass info))); |
997 | [info] => MLClass info))); |
967 fun mk_inst [(name, CodeThingol.Classinst info)] = |
998 fun mk_inst [(name, CodeThingol.Classinst info)] = |
968 map_nsp_fun (name_def false name) |
999 map_nsp_fun (name_def false name) |
969 >> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst info))); |
1000 >> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst info))); |
970 fun add_group mk defs nsp_nodes = |
1001 fun add_group mk defs nsp_nodes = |
1041 |> (fn g => case Graph.get_node g name of Def (defname, _) => defname); |
1073 |> (fn g => case Graph.get_node g name of Def (defname, _) => defname); |
1042 in |
1074 in |
1043 NameSpace.implode (remainder @ [defname']) |
1075 NameSpace.implode (remainder @ [defname']) |
1044 end handle Graph.UNDEF _ => |
1076 end handle Graph.UNDEF _ => |
1045 error ("Unknown definition name: " ^ labelled_name name); |
1077 error ("Unknown definition name: " ^ labelled_name name); |
1046 fun the_prolog modlname = case module_prolog modlname |
|
1047 of NONE => [] |
|
1048 | SOME p => [p, str ""]; |
|
1049 fun pr_node prefix (Def (_, NONE)) = |
1078 fun pr_node prefix (Def (_, NONE)) = |
1050 NONE |
1079 NONE |
1051 | pr_node prefix (Def (_, SOME def)) = |
1080 | pr_node prefix (Def (_, SOME def)) = |
1052 SOME (pr_def tyco_syntax const_syntax labelled_name init_syms |
1081 SOME (pr_def tyco_syntax const_syntax labelled_name init_syms |
1053 (deresolver prefix) is_cons def) |
1082 (deresolver prefix) is_cons def) |
1054 | pr_node prefix (Module (dmodlname, (_, nodes))) = |
1083 | pr_node prefix (Module (dmodlname, (_, nodes))) = |
1055 SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname])) |
1084 SOME (pr_modl dmodlname ( |
1056 @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes) |
1085 separate (str "") |
|
1086 ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes) |
1057 o rev o flat o Graph.strong_conn) nodes))); |
1087 o rev o flat o Graph.strong_conn) nodes))); |
1058 val p = Pretty.chunks (the_prolog "" @ separate (str "") ((map_filter |
1088 val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter |
1059 (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes)) |
1089 (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes)) |
1060 in output p end; |
1090 in output p end; |
1061 |
1091 |
1062 val eval_verbose = ref false; |
1092 val eval_verbose = ref false; |
1063 |
1093 |
1154 let |
1184 let |
1155 val (binds, t') = CodeThingol.unfold_abs t; |
1185 val (binds, t') = CodeThingol.unfold_abs t; |
1156 fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty); |
1186 fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty); |
1157 val (ps, vars') = fold_map pr binds vars; |
1187 val (ps, vars') = fold_map pr binds vars; |
1158 in brackets (str "\\" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end |
1188 in brackets (str "\\" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end |
1159 | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0 |
1189 | pr_term lhs vars fxy (ICase (cases as (_, t0))) = |
|
1190 (case CodeThingol.unfold_const_app t0 |
1160 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) |
1191 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) |
1161 then pr_case vars fxy cases |
1192 then pr_case vars fxy cases |
1162 else pr_app lhs vars fxy c_ts |
1193 else pr_app lhs vars fxy c_ts |
1163 | NONE => pr_case vars fxy cases) |
1194 | NONE => pr_case vars fxy cases) |
1164 and pr_app' lhs vars ((c, _), ts) = |
1195 and pr_app' lhs vars ((c, _), ts) = |
1165 (str o deresolv) c :: map (pr_term lhs vars BR) ts |
1196 (str o deresolv) c :: map (pr_term lhs vars BR) ts |
1166 and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars |
1197 and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax |
|
1198 labelled_name is_cons lhs vars |
1167 and pr_bind fxy = pr_bind_haskell pr_term fxy |
1199 and pr_bind fxy = pr_bind_haskell pr_term fxy |
1168 and pr_case vars fxy (cases as ((_, [_]), _)) = |
1200 and pr_case vars fxy (cases as ((_, [_]), _)) = |
1169 let |
1201 let |
1170 val (binds, t) = CodeThingol.unfold_let (ICase cases); |
1202 val (binds, t) = CodeThingol.unfold_let (ICase cases); |
1171 fun pr ((pat, ty), t) vars = |
1203 fun pr ((pat, ty), t) vars = |
1326 str "};" |
1359 str "};" |
1327 ) (map pr_instdef classparam_insts) |
1360 ) (map pr_instdef classparam_insts) |
1328 end; |
1361 end; |
1329 in pr_def def end; |
1362 in pr_def def end; |
1330 |
1363 |
1331 fun pretty_haskell_monad c_mbind c_kbind = |
1364 fun pretty_haskell_monad c_bind = |
1332 let |
1365 let |
1333 fun pretty pr vars fxy [(t, _)] = |
1366 fun pretty pr vars fxy [(t, _)] = |
1334 let |
1367 let |
1335 val pr_bind = pr_bind_haskell (K pr); |
1368 val pr_bind = pr_bind_haskell (K pr); |
1336 fun pr_mbind (NONE, t) vars = |
1369 fun pr_monad (NONE, t) vars = |
1337 (semicolon [pr vars NOBR t], vars) |
1370 (semicolon [pr vars NOBR t], vars) |
1338 | pr_mbind (SOME (bind, true), t) vars = vars |
1371 | pr_monad (SOME (bind, true), t) vars = vars |
1339 |> pr_bind NOBR bind |
1372 |> pr_bind NOBR bind |
1340 |>> (fn p => semicolon [p, str "<-", pr vars NOBR t]) |
1373 |>> (fn p => semicolon [p, str "<-", pr vars NOBR t]) |
1341 | pr_mbind (SOME (bind, false), t) vars = vars |
1374 | pr_monad (SOME (bind, false), t) vars = vars |
1342 |> pr_bind NOBR bind |
1375 |> pr_bind NOBR bind |
1343 |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]); |
1376 |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]); |
1344 val (binds, t) = implode_monad c_mbind c_kbind t; |
1377 val (binds, t) = implode_monad c_bind t; |
1345 val (ps, vars') = fold_map pr_mbind binds vars; |
1378 val (ps, vars') = fold_map pr_monad binds vars; |
1346 fun brack p = if eval_fxy BR fxy then Pretty.block [str "(", p, str ")"] else p; |
1379 fun brack p = if eval_fxy BR fxy then Pretty.block [str "(", p, str ")"] else p; |
1347 in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end; |
1380 in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end; |
1348 in (1, pretty) end; |
1381 in (1, pretty) end; |
1349 |
1382 |
1350 end; (*local*) |
1383 end; (*local*) |
1351 |
1384 |
1352 fun seri_haskell module_prefix module destination string_classes labelled_name |
1385 fun seri_haskell module_prefix module destination string_classes labelled_name |
1353 reserved_syms raw_module_alias module_prolog |
1386 reserved_syms includes raw_module_alias |
1354 class_syntax tyco_syntax const_syntax code = |
1387 class_syntax tyco_syntax const_syntax code = |
1355 let |
1388 let |
1356 val _ = Option.map File.check destination; |
1389 val _ = Option.map File.check destination; |
1357 val is_cons = CodeThingol.is_cons code; |
1390 val is_cons = CodeThingol.is_cons code; |
1358 val module_alias = if is_some module then K module else raw_module_alias; |
1391 val module_alias = if is_some module then K module else raw_module_alias; |
1424 in deriv [] tyco end; |
1459 in deriv [] tyco end; |
1425 fun seri_def qualified = pr_haskell class_syntax tyco_syntax |
1460 fun seri_def qualified = pr_haskell class_syntax tyco_syntax |
1426 const_syntax labelled_name init_syms |
1461 const_syntax labelled_name init_syms |
1427 deresolv_here (if qualified then deresolv else deresolv_here) is_cons |
1462 deresolv_here (if qualified then deresolv else deresolv_here) is_cons |
1428 (if string_classes then deriving_show else K false); |
1463 (if string_classes then deriving_show else K false); |
1429 fun write_module (SOME destination) modlname = |
1464 fun write_modulefile (SOME destination) modlname = |
1430 let |
1465 let |
1431 val filename = case modlname |
1466 val filename = case modlname |
1432 of "" => Path.explode "Main.hs" |
1467 of "" => Path.explode "Main.hs" |
1433 | _ => (Path.ext "hs" o Path.explode o implode o separate "/" o NameSpace.explode) modlname; |
1468 | _ => (Path.ext "hs" o Path.explode o implode o separate "/" |
|
1469 o NameSpace.explode) modlname; |
1434 val pathname = Path.append destination filename; |
1470 val pathname = Path.append destination filename; |
1435 val _ = File.mkdir (Path.dir pathname); |
1471 val _ = File.mkdir (Path.dir pathname); |
1436 in File.write pathname end |
1472 in File.write pathname end |
1437 | write_module NONE _ = PrintMode.setmp [] writeln; |
1473 | write_modulefile NONE _ = PrintMode.setmp [] writeln; |
|
1474 fun write_module destination (modulename, content) = |
|
1475 Pretty.chunks [ |
|
1476 str ("module " ^ modulename ^ " where {"), |
|
1477 str "", |
|
1478 content, |
|
1479 str "", |
|
1480 str "}" |
|
1481 ] |
|
1482 |> code_output |
|
1483 |> write_modulefile destination modulename; |
1438 fun seri_module (modlname', (imports, (defs, _))) = |
1484 fun seri_module (modlname', (imports, (defs, _))) = |
1439 let |
1485 let |
1440 val imports' = |
1486 val imports' = |
1441 imports |
1487 imports |
1442 |> map (name_modl o fst o dest_name) |
1488 |> map (name_modl o fst o dest_name) |
1448 |> map NameSpace.base |
1494 |> map NameSpace.base |
1449 |> has_duplicates (op =); |
1495 |> has_duplicates (op =); |
1450 val mk_import = str o (if qualified |
1496 val mk_import = str o (if qualified |
1451 then prefix "import qualified " |
1497 then prefix "import qualified " |
1452 else prefix "import ") o suffix ";"; |
1498 else prefix "import ") o suffix ";"; |
|
1499 fun import_include (name, _) = str ("import " ^ name ^ ";"); |
|
1500 val content = Pretty.chunks ( |
|
1501 map mk_import imports' |
|
1502 @ map import_include includes |
|
1503 @ str "" |
|
1504 :: separate (str "") (map_filter |
|
1505 (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def)) |
|
1506 | (_, (_, NONE)) => NONE) defs) |
|
1507 ) |
1453 in |
1508 in |
1454 Pretty.chunks ( |
1509 write_module destination (modlname', content) |
1455 str ("module " ^ modlname' ^ " where {") |
|
1456 :: str "" |
|
1457 :: map mk_import imports' |
|
1458 @ str "" |
|
1459 :: separate (str "") ((case module_prolog modlname' |
|
1460 of SOME prolog => [prolog] |
|
1461 | NONE => []) |
|
1462 @ map_filter |
|
1463 (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def)) |
|
1464 | (_, (_, NONE)) => NONE) defs) |
|
1465 @ str "" |
|
1466 @@ str "}" |
|
1467 ) |
|
1468 |> code_output |
|
1469 |> write_module destination modlname' |
|
1470 end; |
1510 end; |
1471 in Symtab.fold (fn modl => fn () => seri_module modl) code' () end; |
1511 in ( |
|
1512 map (write_module destination) includes; |
|
1513 Symtab.fold (fn modl => fn () => seri_module modl) code' () |
|
1514 ) end; |
1472 |
1515 |
1473 fun isar_seri_haskell module file = |
1516 fun isar_seri_haskell module file = |
1474 let |
1517 let |
1475 val destination = case file |
1518 val destination = case file |
1476 of NONE => error ("Haskell: no internal compilation") |
1519 of NONE => error ("Haskell: no internal compilation") |
1527 Symtab.join (K snd) (inst1, inst2)), |
1572 Symtab.join (K snd) (inst1, inst2)), |
1528 (Symtab.join (K snd) (tyco1, tyco2), |
1573 (Symtab.join (K snd) (tyco1, tyco2), |
1529 Symtab.join (K snd) (const1, const2)) |
1574 Symtab.join (K snd) (const1, const2)) |
1530 ); |
1575 ); |
1531 |
1576 |
1532 datatype syntax_modl = SyntaxModl of { |
|
1533 alias: string Symtab.table, |
|
1534 prolog: Pretty.T Symtab.table |
|
1535 }; |
|
1536 |
|
1537 fun mk_syntax_modl (alias, prolog) = |
|
1538 SyntaxModl { alias = alias, prolog = prolog }; |
|
1539 fun map_syntax_modl f (SyntaxModl { alias, prolog }) = |
|
1540 mk_syntax_modl (f (alias, prolog)); |
|
1541 fun merge_syntax_modl (SyntaxModl { alias = alias1, prolog = prolog1 }, |
|
1542 SyntaxModl { alias = alias2, prolog = prolog2 }) = |
|
1543 mk_syntax_modl ( |
|
1544 Symtab.join (K snd) (alias1, alias2), |
|
1545 Symtab.join (K snd) (prolog1, prolog2) |
|
1546 ); |
|
1547 |
|
1548 type serializer = |
1577 type serializer = |
1549 string option |
1578 string option |
1550 -> string option |
1579 -> string option |
1551 -> Args.T list |
1580 -> Args.T list |
1552 -> (string -> string) |
1581 -> (string -> string) |
1553 -> string list |
1582 -> string list |
|
1583 -> (string * Pretty.T) list |
1554 -> (string -> string option) |
1584 -> (string -> string option) |
1555 -> (string -> Pretty.T option) |
|
1556 -> (string -> class_syntax option) |
1585 -> (string -> class_syntax option) |
1557 -> (string -> typ_syntax option) |
1586 -> (string -> typ_syntax option) |
1558 -> (string -> term_syntax option) |
1587 -> (string -> term_syntax option) |
1559 -> CodeThingol.code -> unit; |
1588 -> CodeThingol.code -> unit; |
1560 |
1589 |
1561 datatype target = Target of { |
1590 datatype target = Target of { |
1562 serial: serial, |
1591 serial: serial, |
1563 serializer: serializer, |
1592 serializer: serializer, |
1564 reserved: string list, |
1593 reserved: string list, |
|
1594 includes: Pretty.T Symtab.table, |
1565 syntax_expr: syntax_expr, |
1595 syntax_expr: syntax_expr, |
1566 syntax_modl: syntax_modl |
1596 module_alias: string Symtab.table |
1567 }; |
1597 }; |
1568 |
1598 |
1569 fun mk_target (serial, ((serializer, reserved), (syntax_expr, syntax_modl))) = |
1599 fun mk_target ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias))) = |
1570 Target { serial = serial, reserved = reserved, serializer = serializer, syntax_expr = syntax_expr, syntax_modl = syntax_modl }; |
1600 Target { serial = serial, serializer = serializer, reserved = reserved, |
1571 fun map_target f ( Target { serial, serializer, reserved, syntax_expr, syntax_modl } ) = |
1601 includes = includes, syntax_expr = syntax_expr, module_alias = module_alias }; |
1572 mk_target (f (serial, ((serializer, reserved), (syntax_expr, syntax_modl)))); |
1602 fun map_target f ( Target { serial, serializer, reserved, includes, syntax_expr, module_alias } ) = |
1573 fun merge_target target (Target { serial = serial1, serializer = serializer, reserved = reserved1, |
1603 mk_target (f ((serial, serializer), ((reserved, includes), (syntax_expr, module_alias)))); |
1574 syntax_expr = syntax_expr1, syntax_modl = syntax_modl1 }, |
1604 fun merge_target target (Target { serial = serial1, serializer = serializer, |
1575 Target { serial = serial2, serializer = _, reserved = reserved2, |
1605 reserved = reserved1, includes = includes1, |
1576 syntax_expr = syntax_expr2, syntax_modl = syntax_modl2 }) = |
1606 syntax_expr = syntax_expr1, module_alias = module_alias1 }, |
|
1607 Target { serial = serial2, serializer = _, |
|
1608 reserved = reserved2, includes = includes2, |
|
1609 syntax_expr = syntax_expr2, module_alias = module_alias2 }) = |
1577 if serial1 = serial2 then |
1610 if serial1 = serial2 then |
1578 mk_target (serial1, ((serializer, merge (op =) (reserved1, reserved2)), |
1611 mk_target ((serial1, serializer), |
1579 (merge_syntax_expr (syntax_expr1, syntax_expr2), |
1612 ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)), |
1580 merge_syntax_modl (syntax_modl1, syntax_modl2)) |
1613 (merge_syntax_expr (syntax_expr1, syntax_expr2), |
|
1614 Symtab.join (K snd) (module_alias1, module_alias2)) |
1581 )) |
1615 )) |
1582 else |
1616 else |
1583 error ("Incompatible serializers: " ^ quote target); |
1617 error ("Incompatible serializers: " ^ quote target); |
1584 |
1618 |
1585 structure CodeTargetData = TheoryDataFun |
1619 structure CodeTargetData = TheoryDataFun |
1586 ( |
1620 ( |
1587 type T = target Symtab.table * string list; |
1621 type T = target Symtab.table * string list; |
1588 val empty = (Symtab.empty, []); |
1622 val empty = (Symtab.empty, []); |
1589 val copy = I; |
1623 val copy = I; |
1590 val extend = I; |
1624 val extend = I; |
1591 fun merge _ ((target1, exc1), (target2, exc2)) = |
1625 fun merge _ ((target1, exc1) : T, (target2, exc2)) = |
1592 (Symtab.join merge_target (target1, target2), Library.merge (op =) (exc1, exc2)); |
1626 (Symtab.join merge_target (target1, target2), Library.merge (op =) (exc1, exc2)); |
1593 ); |
1627 ); |
1594 |
1628 |
|
1629 val target_SML = "SML"; |
|
1630 val target_OCaml = "OCaml"; |
|
1631 val target_Haskell = "Haskell"; |
|
1632 val target_diag = "diag"; |
|
1633 |
1595 fun the_serializer (Target { serializer, ... }) = serializer; |
1634 fun the_serializer (Target { serializer, ... }) = serializer; |
1596 fun the_reserved (Target { reserved, ... }) = reserved; |
1635 fun the_reserved (Target { reserved, ... }) = reserved; |
|
1636 fun the_includes (Target { includes, ... }) = includes; |
1597 fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x; |
1637 fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x; |
1598 fun the_syntax_modl (Target { syntax_modl = SyntaxModl x, ... }) = x; |
1638 fun the_module_alias (Target { module_alias , ... }) = module_alias; |
1599 |
1639 |
1600 fun assert_serializer thy target = |
1640 fun assert_serializer thy target = |
1601 case Symtab.lookup (fst (CodeTargetData.get thy)) target |
1641 case Symtab.lookup (fst (CodeTargetData.get thy)) target |
1602 of SOME data => target |
1642 of SOME data => target |
1603 | NONE => error ("Unknown code target language: " ^ quote target); |
1643 | NONE => error ("Unknown code target language: " ^ quote target); |
1608 of SOME _ => warning ("overwriting existing serializer " ^ quote target) |
1648 of SOME _ => warning ("overwriting existing serializer " ^ quote target) |
1609 | NONE => (); |
1649 | NONE => (); |
1610 in |
1650 in |
1611 thy |
1651 thy |
1612 |> (CodeTargetData.map o apfst oo Symtab.map_default) |
1652 |> (CodeTargetData.map o apfst oo Symtab.map_default) |
1613 (target, mk_target (serial (), ((seri, []), |
1653 (target, mk_target ((serial (), seri), (([], Symtab.empty), |
1614 (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), |
1654 (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), |
1615 mk_syntax_modl (Symtab.empty, Symtab.empty))))) |
1655 Symtab.empty)))) |
1616 (map_target (fn (serial, ((_, keywords), syntax)) => (serial, ((seri, keywords), syntax)))) |
1656 ((map_target o apfst o apsnd o K) seri) |
1617 end; |
1657 end; |
1618 |
1658 |
1619 fun map_seri_data target f thy = |
1659 fun map_seri_data target f thy = |
1620 let |
1660 let |
1621 val _ = assert_serializer thy target; |
1661 val _ = assert_serializer thy target; |
1622 in |
1662 in |
1623 thy |
1663 thy |
1624 |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f |
1664 |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f |
1625 end; |
1665 end; |
1626 |
1666 |
1627 val target_SML = "SML"; |
1667 fun map_adaptions target = |
1628 val target_OCaml = "OCaml"; |
1668 map_seri_data target o apsnd o apfst; |
1629 val target_Haskell = "Haskell"; |
1669 fun map_syntax_exprs target = |
1630 val target_diag = "diag"; |
1670 map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr; |
|
1671 fun map_module_alias target = |
|
1672 map_seri_data target o apsnd o apsnd o apsnd; |
1631 |
1673 |
1632 fun get_serializer thy target permissive module file args |
1674 fun get_serializer thy target permissive module file args |
1633 = fn cs => |
1675 = fn cs => |
1634 let |
1676 let |
1635 val (seris, exc) = CodeTargetData.get thy; |
1677 val (seris, exc) = CodeTargetData.get thy; |
1636 val data = case Symtab.lookup seris target |
1678 val data = case Symtab.lookup seris target |
1637 of SOME data => data |
1679 of SOME data => data |
1638 | NONE => error ("Unknown code target language: " ^ quote target); |
1680 | NONE => error ("Unknown code target language: " ^ quote target); |
1639 val seri = the_serializer data; |
1681 val seri = the_serializer data; |
1640 val reserved = the_reserved data; |
1682 val reserved = the_reserved data; |
1641 val { alias, prolog } = the_syntax_modl data; |
1683 val includes = Symtab.dest (the_includes data); |
|
1684 val alias = the_module_alias data; |
1642 val { class, inst, tyco, const } = the_syntax_expr data; |
1685 val { class, inst, tyco, const } = the_syntax_expr data; |
1643 val project = if target = target_diag then I |
1686 val project = if target = target_diag then I |
1644 else CodeThingol.project_code permissive |
1687 else CodeThingol.project_code permissive |
1645 (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs; |
1688 (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs; |
1646 fun check_empty_funs code = case (filter_out (member (op =) exc) |
1689 fun check_empty_funs code = case (filter_out (member (op =) exc) |
1647 (CodeThingol.empty_funs code)) |
1690 (CodeThingol.empty_funs code)) |
1648 of [] => code |
1691 of [] => code |
1649 | names => error ("No defining equations for " ^ commas (map (CodeName.labelled_name thy) names)); |
1692 | names => error ("No defining equations for " |
|
1693 ^ commas (map (CodeName.labelled_name thy) names)); |
1650 in |
1694 in |
1651 project |
1695 project |
1652 #> check_empty_funs |
1696 #> check_empty_funs |
1653 #> seri module file args (CodeName.labelled_name thy) reserved (Symtab.lookup alias) |
1697 #> seri module file args (CodeName.labelled_name thy) reserved includes (Symtab.lookup alias) |
1654 (Symtab.lookup prolog) (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const) |
1698 (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const) |
1655 end; |
1699 end; |
1656 |
1700 |
1657 fun eval_invoke thy (ref_name, reff) code (t, ty) args = |
1701 fun eval_invoke thy (ref_name, reff) code (t, ty) args = |
1658 let |
1702 let |
1659 val _ = if CodeThingol.contains_dictvar t then |
1703 val _ = if CodeThingol.contains_dictvar t then |
1781 case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t |
1825 case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t |
1782 of SOME k => (str o mk_numeral unbounded) k |
1826 of SOME k => (str o mk_numeral unbounded) k |
1783 | NONE => error "Illegal numeral expression"; |
1827 | NONE => error "Illegal numeral expression"; |
1784 in (1, pretty) end; |
1828 in (1, pretty) end; |
1785 |
1829 |
1786 fun pretty_ml_string c_char c_nibbles c_nil c_cons target = |
1830 fun pretty_message c_char c_nibbles c_nil c_cons target = |
1787 let |
1831 let |
1788 val pretty_ops = pr_pretty target; |
1832 val pretty_ops = pr_pretty target; |
1789 val mk_char = #pretty_char pretty_ops; |
1833 val mk_char = #pretty_char pretty_ops; |
1790 val mk_string = #pretty_string pretty_ops; |
1834 val mk_string = #pretty_string pretty_ops; |
1791 fun pretty pr vars fxy [(t, _)] = |
1835 fun pretty pr vars fxy [(t, _)] = |
1792 case implode_list c_nil c_cons t |
1836 case implode_list c_nil c_cons t |
1793 of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts |
1837 of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts |
1794 of SOME p => p |
1838 of SOME p => p |
1795 | NONE => error "Illegal ml_string expression") |
1839 | NONE => error "Illegal message expression") |
1796 | NONE => error "Illegal ml_string expression"; |
1840 | NONE => error "Illegal message expression"; |
1797 in (1, pretty) end; |
1841 in (1, pretty) end; |
1798 |
1842 |
1799 fun pretty_imperative_monad_bind bind' = |
1843 fun pretty_imperative_monad_bind bind' = |
1800 let |
1844 let |
1801 fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t) |
1845 fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t) |
1899 thy |
1963 thy |
1900 |> (map_syntax_exprs target o apsnd o apsnd) |
1964 |> (map_syntax_exprs target o apsnd o apsnd) |
1901 (Symtab.delete_safe c') |
1965 (Symtab.delete_safe c') |
1902 end; |
1966 end; |
1903 |
1967 |
1904 fun cert_class thy class = |
|
1905 let |
|
1906 val _ = AxClass.get_info thy class; |
|
1907 in class end; |
|
1908 |
|
1909 fun read_class thy raw_class = |
|
1910 let |
|
1911 val class = Sign.intern_class thy raw_class; |
|
1912 val _ = AxClass.get_info thy class; |
|
1913 in class end; |
|
1914 |
|
1915 fun cert_tyco thy tyco = |
|
1916 let |
|
1917 val _ = if Sign.declared_tyname thy tyco then () |
|
1918 else error ("No such type constructor: " ^ quote tyco); |
|
1919 in tyco end; |
|
1920 |
|
1921 fun read_tyco thy raw_tyco = |
|
1922 let |
|
1923 val tyco = Sign.intern_type thy raw_tyco; |
|
1924 val _ = if Sign.declared_tyname thy tyco then () |
|
1925 else error ("No such type constructor: " ^ quote raw_tyco); |
|
1926 in tyco end; |
|
1927 |
|
1928 fun no_bindings x = (Option.map o apsnd) |
|
1929 (fn pretty => fn pr => fn vars => pretty (pr vars)) x; |
|
1930 |
|
1931 fun gen_add_haskell_monad prep_const c_run c_mbind c_kbind thy = |
|
1932 let |
|
1933 val c_run' = prep_const thy c_run; |
|
1934 val c_mbind' = prep_const thy c_mbind; |
|
1935 val c_mbind'' = CodeName.const thy c_mbind'; |
|
1936 val c_kbind' = prep_const thy c_kbind; |
|
1937 val c_kbind'' = CodeName.const thy c_kbind'; |
|
1938 val pr = pretty_haskell_monad c_mbind'' c_kbind'' |
|
1939 in |
|
1940 thy |
|
1941 |> gen_add_syntax_const (K I) target_Haskell c_run' (SOME pr) |
|
1942 |> gen_add_syntax_const (K I) target_Haskell c_mbind' |
|
1943 (no_bindings (SOME (parse_infix fst (L, 1) ">>="))) |
|
1944 |> gen_add_syntax_const (K I) target_Haskell c_kbind' |
|
1945 (no_bindings (SOME (parse_infix fst (L, 1) ">>"))) |
|
1946 end; |
|
1947 |
|
1948 fun add_reserved target = |
1968 fun add_reserved target = |
1949 let |
1969 let |
1950 fun add sym syms = if member (op =) syms sym |
1970 fun add sym syms = if member (op =) syms sym |
1951 then error ("Reserved symbol " ^ quote sym ^ " already declared") |
1971 then error ("Reserved symbol " ^ quote sym ^ " already declared") |
1952 else insert (op =) sym syms |
1972 else insert (op =) sym syms |
1953 in map_reserveds target o add end; |
1973 in map_adaptions target o apfst o add end; |
|
1974 |
|
1975 fun add_include target = |
|
1976 let |
|
1977 fun add (name, SOME content) incls = |
|
1978 let |
|
1979 val _ = if Symtab.defined incls name |
|
1980 then warning ("Overwriting existing include " ^ name) |
|
1981 else (); |
|
1982 in Symtab.update (name, str content) incls end |
|
1983 | add (name, NONE) incls = |
|
1984 Symtab.delete name incls; |
|
1985 in map_adaptions target o apsnd o add end; |
1954 |
1986 |
1955 fun add_modl_alias target = |
1987 fun add_modl_alias target = |
1956 map_syntax_modls target o apfst o Symtab.update o apsnd CodeName.check_modulename; |
1988 map_module_alias target o Symtab.update o apsnd CodeName.check_modulename; |
1957 |
1989 |
1958 fun add_modl_prolog target = |
1990 fun add_monad target c_run c_bind thy = |
1959 map_syntax_modls target o apsnd o |
1991 let |
1960 (fn (modl, NONE) => Symtab.delete modl | (modl, SOME prolog) => |
1992 val c_run' = CodeUnit.read_const thy c_run; |
1961 Symtab.update (modl, Pretty.str prolog)); |
1993 val c_bind' = CodeUnit.read_const thy c_bind; |
|
1994 val c_bind'' = CodeName.const thy c_bind'; |
|
1995 in if target = target_Haskell then |
|
1996 thy |
|
1997 |> gen_add_syntax_const (K I) target_Haskell c_run' |
|
1998 (SOME (pretty_haskell_monad c_bind'')) |
|
1999 |> gen_add_syntax_const (K I) target_Haskell c_bind' |
|
2000 (no_bindings (SOME (parse_infix fst (L, 1) ">>="))) |
|
2001 else |
|
2002 thy |
|
2003 |> gen_add_syntax_const (K I) target c_bind' |
|
2004 (SOME (pretty_imperative_monad_bind c_bind'')) |
|
2005 end; |
1962 |
2006 |
1963 fun gen_allow_exception prep_cs raw_c thy = |
2007 fun gen_allow_exception prep_cs raw_c thy = |
1964 let |
2008 let |
1965 val c = prep_cs thy raw_c; |
2009 val c = prep_cs thy raw_c; |
1966 val c' = CodeName.const thy c; |
2010 val c' = CodeName.const thy c; |
2067 in |
2106 in |
2068 thy |
2107 thy |
2069 |> add_syntax_const target number_of (SOME pr) |
2108 |> add_syntax_const target number_of (SOME pr) |
2070 end; |
2109 end; |
2071 |
2110 |
2072 fun add_pretty_ml_string target charr nibbles nill cons str thy = |
2111 fun add_pretty_message target charr nibbles nill cons str thy = |
2073 let |
2112 let |
2074 val charr' = CodeName.const thy charr; |
2113 val charr' = CodeName.const thy charr; |
2075 val nibbles' = map (CodeName.const thy) nibbles; |
2114 val nibbles' = map (CodeName.const thy) nibbles; |
2076 val nil' = CodeName.const thy nill; |
2115 val nil' = CodeName.const thy nill; |
2077 val cons' = CodeName.const thy cons; |
2116 val cons' = CodeName.const thy cons; |
2078 val pr = pretty_ml_string charr' nibbles' nil' cons' target; |
2117 val pr = pretty_message charr' nibbles' nil' cons' target; |
2079 in |
2118 in |
2080 thy |
2119 thy |
2081 |> add_syntax_const target str (SOME pr) |
2120 |> add_syntax_const target str (SOME pr) |
2082 end; |
2121 end; |
2083 |
2122 |
2084 fun add_pretty_imperative_monad_bind target bind thy = |
|
2085 add_syntax_const target bind (SOME (pretty_imperative_monad_bind |
|
2086 (CodeName.const thy bind))) thy; |
|
2087 |
|
2088 val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const; |
|
2089 |
|
2090 |
2123 |
2091 val _ = OuterSyntax.keywords [infixK, infixlK, infixrK]; |
2124 val _ = OuterSyntax.keywords [infixK, infixlK, infixrK]; |
2092 |
2125 |
2093 val _ = |
2126 val _ = |
2094 OuterSyntax.command code_classK "define code syntax for class" K.thy_decl ( |
2127 OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl ( |
2095 parse_multi_syntax P.xname |
2128 parse_multi_syntax P.xname |
2096 (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1 |
2129 (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1 |
2097 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) [])) |
2130 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) [])) |
2098 >> (Toplevel.theory oo fold) (fn (target, syns) => |
2131 >> (Toplevel.theory oo fold) (fn (target, syns) => |
2099 fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns) |
2132 fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns) |
2100 ); |
2133 ); |
2101 |
2134 |
2102 val _ = |
2135 val _ = |
2103 OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl ( |
2136 OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl ( |
2104 parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) |
2137 parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) |
2105 ((P.minus >> K true) || Scan.succeed false) |
2138 ((P.minus >> K true) || Scan.succeed false) |
2106 >> (Toplevel.theory oo fold) (fn (target, syns) => |
2139 >> (Toplevel.theory oo fold) (fn (target, syns) => |
2107 fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns) |
2140 fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns) |
2108 ); |
2141 ); |
2109 |
2142 |
2110 val _ = |
2143 val _ = |
2111 OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl ( |
2144 OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl ( |
2112 parse_multi_syntax P.xname (parse_syntax I) |
2145 parse_multi_syntax P.xname (parse_syntax I) |
2113 >> (Toplevel.theory oo fold) (fn (target, syns) => |
2146 >> (Toplevel.theory oo fold) (fn (target, syns) => |
2114 fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns) |
2147 fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns) |
2115 ); |
2148 ); |
2116 |
2149 |
2117 val _ = |
2150 val _ = |
2118 OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl ( |
2151 OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl ( |
2119 parse_multi_syntax P.term (parse_syntax fst) |
2152 parse_multi_syntax P.term (parse_syntax fst) |
2120 >> (Toplevel.theory oo fold) (fn (target, syns) => |
2153 >> (Toplevel.theory oo fold) (fn (target, syns) => |
2121 fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns) |
2154 fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns) |
2122 ); |
2155 ); |
2123 |
2156 |
2124 val _ = |
2157 val _ = |
2125 OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl ( |
2158 OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl ( |
2126 P.term -- P.term -- P.term |
2159 P.term -- P.term -- Scan.repeat1 P.name |
2127 >> (fn ((raw_run, raw_mbind), raw_kbind) => Toplevel.theory |
2160 >> (fn ((raw_run, raw_bind), targets) => Toplevel.theory |
2128 (add_haskell_monad raw_run raw_mbind raw_kbind)) |
2161 (fold (fn target => add_monad target raw_run raw_bind) targets)) |
2129 ); |
2162 ); |
2130 |
2163 |
2131 val _ = |
2164 val _ = |
2132 OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl ( |
2165 OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl ( |
2133 P.name -- Scan.repeat1 P.name |
2166 P.name -- Scan.repeat1 P.name |
2134 >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds) |
2167 >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds) |
2135 ); |
2168 ); |
2136 |
2169 |
2137 val _ = |
2170 val _ = |
2138 OuterSyntax.command code_modulenameK "alias module to other name" K.thy_decl ( |
2171 OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl ( |
|
2172 P.name -- P.name -- (P.text >> (fn "-" => NONE | s => SOME s)) |
|
2173 >> (fn ((target, name), content) => (Toplevel.theory o add_include target) |
|
2174 (name, content)) |
|
2175 ); |
|
2176 |
|
2177 val _ = |
|
2178 OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl ( |
2139 P.name -- Scan.repeat1 (P.name -- P.name) |
2179 P.name -- Scan.repeat1 (P.name -- P.name) |
2140 >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames) |
2180 >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames) |
2141 ); |
2181 ); |
2142 |
2182 |
2143 val _ = |
2183 val _ = |
2144 OuterSyntax.command code_moduleprologK "add prolog to module" K.thy_decl ( |
2184 OuterSyntax.command "code_exception" "permit exceptions for constant" K.thy_decl ( |
2145 P.name -- Scan.repeat1 (P.name -- (P.text >> (fn "-" => NONE | s => SOME s))) |
|
2146 >> (fn (target, prologs) => (Toplevel.theory o fold (add_modl_prolog target)) prologs) |
|
2147 ); |
|
2148 |
|
2149 val _ = |
|
2150 OuterSyntax.command code_exceptionK "permit exceptions for constant" K.thy_decl ( |
|
2151 Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd) |
2185 Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd) |
2152 ); |
2186 ); |
2153 |
2187 |
2154 |
2188 |
2155 (*including serializer defaults*) |
2189 (*including serializer defaults*) |
2156 val setup = |
2190 val setup = |
2157 add_serializer (target_SML, isar_seri_sml) |
2191 add_serializer (target_SML, isar_seri_sml) |
2158 #> add_serializer (target_OCaml, isar_seri_ocaml) |
2192 #> add_serializer (target_OCaml, isar_seri_ocaml) |
2159 #> add_serializer (target_Haskell, isar_seri_haskell) |
2193 #> add_serializer (target_Haskell, isar_seri_haskell) |
2160 #> add_serializer (target_diag, fn _=> fn _ => fn _ => seri_diagnosis) |
2194 #> add_serializer (target_diag, fn _ => fn _=> fn _ => seri_diagnosis) |
2161 #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] => |
2195 #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] => |
2162 (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [ |
2196 (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [ |
2163 pr_typ (INFX (1, X)) ty1, |
2197 pr_typ (INFX (1, X)) ty1, |
2164 str "->", |
2198 str "->", |
2165 pr_typ (INFX (1, R)) ty2 |
2199 pr_typ (INFX (1, R)) ty2 |