475 |
475 |
476 fun mk_const_id module cname (gr, (tab1, tab2)) = |
476 fun mk_const_id module cname (gr, (tab1, tab2)) = |
477 let |
477 let |
478 val ((module, s), tab1') = mk_long_id tab1 module cname |
478 val ((module, s), tab1') = mk_long_id tab1 module cname |
479 val s' = mk_id s; |
479 val s' = mk_id s; |
480 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' |
480 val s'' = if ThmDatabase.is_ml_reserved s' then s' ^ "_const" else s' |
481 in ((gr, (tab1', tab2)), (module, s'')) end; |
481 in ((gr, (tab1', tab2)), (module, s'')) end; |
482 |
482 |
483 fun get_const_id cname (gr, (tab1, tab2)) = |
483 fun get_const_id cname (gr, (tab1, tab2)) = |
484 case Symtab.lookup (fst tab1) cname of |
484 case Symtab.lookup (fst tab1) cname of |
485 NONE => error ("get_const_id: no such constant: " ^ quote cname) |
485 NONE => error ("get_const_id: no such constant: " ^ quote cname) |
486 | SOME (module, s) => |
486 | SOME (module, s) => |
487 let |
487 let |
488 val s' = mk_id s; |
488 val s' = mk_id s; |
489 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' |
489 val s'' = if ThmDatabase.is_ml_reserved s' then s' ^ "_const" else s' |
490 in (module, s'') end; |
490 in (module, s'') end; |
491 |
491 |
492 fun mk_type_id module tyname (gr, (tab1, tab2)) = |
492 fun mk_type_id module tyname (gr, (tab1, tab2)) = |
493 let |
493 let |
494 val ((module, s), tab2') = mk_long_id tab2 module tyname |
494 val ((module, s), tab2') = mk_long_id tab2 module tyname |
495 val s' = mk_id s; |
495 val s' = mk_id s; |
496 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' |
496 val s'' = if ThmDatabase.is_ml_reserved s' then s' ^ "_type" else s' |
497 in ((gr, (tab1, tab2')), (module, s'')) end; |
497 in ((gr, (tab1, tab2')), (module, s'')) end; |
498 |
498 |
499 fun get_type_id tyname (gr, (tab1, tab2)) = |
499 fun get_type_id tyname (gr, (tab1, tab2)) = |
500 case Symtab.lookup (fst tab2) tyname of |
500 case Symtab.lookup (fst tab2) tyname of |
501 NONE => error ("get_type_id: no such type: " ^ quote tyname) |
501 NONE => error ("get_type_id: no such type: " ^ quote tyname) |
502 | SOME (module, s) => |
502 | SOME (module, s) => |
503 let |
503 let |
504 val s' = mk_id s; |
504 val s' = mk_id s; |
505 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' |
505 val s'' = if ThmDatabase.is_ml_reserved s' then s' ^ "_type" else s' |
506 in (module, s'') end; |
506 in (module, s'') end; |
507 |
507 |
508 fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab); |
508 fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab); |
509 |
509 |
510 fun get_node (gr, x) k = Graph.get_node gr k; |
510 fun get_node (gr, x) k = Graph.get_node gr k; |
563 |
563 |
564 fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) => |
564 fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) => |
565 s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy))); |
565 s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy))); |
566 |
566 |
567 fun get_aux_code xs = map_filter (fn (m, code) => |
567 fun get_aux_code xs = map_filter (fn (m, code) => |
568 if m = "" orelse m mem !mode then SOME code else NONE) xs; |
568 if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs; |
569 |
569 |
570 fun mk_deftab thy = |
570 fun mk_deftab thy = |
571 let |
571 let |
572 val axmss = map (fn thy' => |
572 val axmss = map (fn thy' => |
573 (Context.theory_name thy', snd (#axioms (Theory.rep_theory thy')))) |
573 (Context.theory_name thy', snd (#axioms (Theory.rep_theory thy')))) |
693 (map (fst o fst o dest_Var) (term_vars t) union |
693 (map (fst o fst o dest_Var) (term_vars t) union |
694 add_term_names (t, ThmDatabase.ml_reserved)) (map mk_id xs); |
694 add_term_names (t, ThmDatabase.ml_reserved)) (map mk_id xs); |
695 |
695 |
696 fun new_name t x = hd (new_names t [x]); |
696 fun new_name t x = hd (new_names t [x]); |
697 |
697 |
698 fun if_library x y = if "library" mem !mode then x else y; |
698 fun if_library x y = if member (op =) (!mode) "library" then x else y; |
699 |
699 |
700 fun default_codegen thy defs gr dep module brack t = |
700 fun default_codegen thy defs gr dep module brack t = |
701 let |
701 let |
702 val (u, ts) = strip_comb t; |
702 val (u, ts) = strip_comb t; |
703 fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack) |
703 fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack) |
875 |
875 |
876 fun gen_generate_code prep_term thy modules module = |
876 fun gen_generate_code prep_term thy modules module = |
877 setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs => |
877 setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs => |
878 let |
878 let |
879 val _ = assert (module <> "" orelse |
879 val _ = assert (module <> "" orelse |
880 "library" mem !mode andalso forall (equal "" o fst) xs) |
880 member (op =) (!mode) "library" andalso forall (equal "" o fst) xs) |
881 "missing module name"; |
881 "missing module name"; |
882 val graphs = get_modules thy; |
882 val graphs = get_modules thy; |
883 val defs = mk_deftab thy; |
883 val defs = mk_deftab thy; |
884 val gr = new_node ("<Top>", (NONE, module, "")) |
884 val gr = new_node ("<Top>", (NONE, module, "")) |
885 (foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) => |
885 (foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) => |
901 | (s', p) => SOME (Pretty.string_of (Pretty.block |
901 | (s', p) => SOME (Pretty.string_of (Pretty.block |
902 [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"]))) ps; |
902 [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"]))) ps; |
903 val code' = space_implode "\n\n" code ^ "\n\n"; |
903 val code' = space_implode "\n\n" code ^ "\n\n"; |
904 val code'' = |
904 val code'' = |
905 map_filter (fn (name, s) => |
905 map_filter (fn (name, s) => |
906 if "library" mem !mode andalso name = module andalso null code |
906 if member (op =) (!mode) "library" andalso name = module andalso null code |
907 then NONE |
907 then NONE |
908 else SOME (name, mk_struct name s)) |
908 else SOME (name, mk_struct name s)) |
909 ((if null code then I |
909 ((if null code then I |
910 else add_to_module module code') |
910 else add_to_module module code') |
911 (output_code (fst gr') (if_library "" module) ["<Top>"])) |
911 (output_code (fst gr') (if_library "" module) ["<Top>"])) |
950 (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G") |
950 (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G") |
951 | mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G") |
951 | mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G") |
952 | mk_gen gr module p xs a (Type (s, Ts)) = (if p then parens else I) |
952 | mk_gen gr module p xs a (Type (s, Ts)) = (if p then parens else I) |
953 (Pretty.block (separate (Pretty.brk 1) |
953 (Pretty.block (separate (Pretty.brk 1) |
954 (Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^ |
954 (Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^ |
955 (if s mem xs then "'" else "")) :: |
955 (if member (op =) xs s then "'" else "")) :: |
956 map (mk_gen gr module true xs a) Ts @ |
956 map (mk_gen gr module true xs a) Ts @ |
957 (if s mem xs then [Pretty.str a] else [])))); |
957 (if member (op =) xs s then [Pretty.str a] else [])))); |
958 |
958 |
959 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE); |
959 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE); |
960 |
960 |
961 fun test_term thy sz i t = |
961 fun test_term thy sz i t = |
962 let |
962 let |
1065 fun evaluation_oracle (thy, Evaluation t) = |
1065 fun evaluation_oracle (thy, Evaluation t) = |
1066 Logic.mk_equals (t, eval_term thy t); |
1066 Logic.mk_equals (t, eval_term thy t); |
1067 |
1067 |
1068 fun evaluation_conv ct = |
1068 fun evaluation_conv ct = |
1069 let val {sign, t, ...} = rep_cterm ct |
1069 let val {sign, t, ...} = rep_cterm ct |
1070 in Thm.invoke_oracle_i sign "Pure.Evaluation" (sign, Evaluation t) end; |
1070 in Thm.invoke_oracle_i sign "Pure.evaluation" (sign, Evaluation t) end; |
1071 |
1071 |
1072 val _ = Context.add_setup |
1072 val _ = Context.add_setup |
1073 (Theory.add_oracle ("Evaluation", evaluation_oracle)); |
1073 (Theory.add_oracle ("evaluation", evaluation_oracle)); |
1074 |
1074 |
1075 (**** Interface ****) |
1075 (**** Interface ****) |
1076 |
1076 |
1077 val str = setmp print_mode [] Pretty.str; |
1077 val str = setmp print_mode [] Pretty.str; |
1078 |
1078 |