57 -> codegen_expr; |
57 -> codegen_expr; |
58 val codegen_split: (int -> term -> term list * term) |
58 val codegen_split: (int -> term -> term list * term) |
59 -> codegen_expr; |
59 -> codegen_expr; |
60 val codegen_number_of: (term -> IntInf.int) -> (term -> term) |
60 val codegen_number_of: (term -> IntInf.int) -> (term -> term) |
61 -> codegen_expr; |
61 -> codegen_expr; |
|
62 val codegen_case: (theory -> string -> (string * int) list option) |
|
63 -> codegen_expr; |
62 val defgen_datatype: (theory -> string -> (string list * string list) option) |
64 val defgen_datatype: (theory -> string -> (string list * string list) option) |
63 -> defgen; |
65 -> defgen; |
64 val defgen_datacons: (theory -> string * string -> typ list option) |
66 val defgen_datacons: (theory -> string * string -> typ list option) |
65 -> defgen; |
67 -> defgen; |
66 val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ) |
68 val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ) |
67 -> defgen; |
69 -> defgen; |
68 |
70 |
69 val print_codegen_modl: theory -> unit; |
71 val print_codegen_generated: theory -> unit; |
70 val mk_deftab: theory -> deftab; |
72 val mk_deftab: theory -> deftab; |
71 structure CodegenData: THEORY_DATA; |
73 structure CodegenData: THEORY_DATA; |
72 structure Insttab: TABLE; |
74 structure Insttab: TABLE; |
73 end; |
75 end; |
74 |
76 |
281 let val (modl, gens, lookups, serialize_data, logic_data) = |
283 let val (modl, gens, lookups, serialize_data, logic_data) = |
282 f (modl, gens, lookups, serialize_data, logic_data) |
284 f (modl, gens, lookups, serialize_data, logic_data) |
283 in CodegenData.put { modl = modl, gens = gens, lookups = lookups, |
285 in CodegenData.put { modl = modl, gens = gens, lookups = lookups, |
284 serialize_data = serialize_data, logic_data = logic_data } thy end; |
286 serialize_data = serialize_data, logic_data = logic_data } thy end; |
285 |
287 |
286 val print_codegen_modl = writeln o Pretty.output o pretty_module o #modl o CodegenData.get; |
288 val print_codegen_generated = writeln o Pretty.output o pretty_module o #modl o CodegenData.get; |
287 |
289 |
288 fun add_codegen_sort (name, cg) = |
290 fun add_codegen_sort (name, cg) = |
289 map_codegen_data |
291 map_codegen_data |
290 (fn (modl, gens, lookups, serialize_data, logic_data) => |
292 (fn (modl, gens, lookups, serialize_data, logic_data) => |
291 (modl, |
293 (modl, |
525 ||>> invoke_cg_type thy defs ty |
527 ||>> invoke_cg_type thy defs ty |
526 ||>> fold_map mk_sortvar sortctxt |
528 ||>> fold_map mk_sortvar sortctxt |
527 |-> (fn ((eqs, ty), sortctxt) => pair (Fun (eqs, (sortctxt, ty)))) |
529 |-> (fn ((eqs, ty), sortctxt) => pair (Fun (eqs, (sortctxt, ty)))) |
528 end; |
530 end; |
529 |
531 |
530 fun mk_app thy defs f ty_use args trns = |
532 fun fix_nargs thy defs gen i (t, ts) trns = |
531 let |
533 if length ts < i |
532 val _ = debug 5 (fn _ => "making application of " ^ quote f) (); |
534 then |
533 val ty_def = Sign.the_const_constraint thy f; |
|
534 val _ = debug 10 (fn _ => "making application (2)") (); |
|
535 fun mk_lookup (ClassPackage.Instance (i, ls)) trns = |
|
536 trns |
|
537 |> ensure_def_class thy defs ((idf_of_name thy nsp_class o fst) i) |
|
538 ||>> ensure_def_class thy defs (idf_of_inst thy defs i) |
|
539 ||>> (fold_map o fold_map) mk_lookup ls |
|
540 |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls))) |
|
541 | mk_lookup (ClassPackage.Lookup (clss, (v, i))) trns = |
|
542 trns |
|
543 |> fold_map (ensure_def_class thy defs) (map (idf_of_name thy nsp_class) clss) |
|
544 |-> (fn clss => pair (ClassPackage.Lookup (clss, (name_of_tvar (TFree (v, [])), i)))); |
|
545 val _ = debug 10 (fn _ => "making application (3)") (); |
|
546 fun mk_itapp e [] = e |
|
547 | mk_itapp e lookup = IInst (e, lookup); |
|
548 in |
|
549 trns |
535 trns |
550 |> debug 10 (fn _ => "making application (4): " ^ f ^ "::" ^ Sign.string_of_typ thy ty_use) |
536 |> debug 10 (fn _ => "eta-expanding") |
551 |> ensure_def_const thy defs (idf_of_cname thy defs (f, ty_use)) |
537 |> gen (strip_comb (Codegen.eta_expand t ts i)) |
552 |> debug 10 (fn _ => "making application (5)") |
538 else |
553 ||>> fold_map (invoke_cg_expr thy defs) args |
539 trns |
554 |> debug 10 (fn _ => "making application (6)") |
540 |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int i ^ ", " ^ string_of_int (length ts) ^ ")") |
555 ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty_use)) |
541 |> gen (t, Library.take (i, ts)) |
556 |> debug 10 (fn _ => "making application (7)") |
542 ||>> fold_map (invoke_cg_expr thy defs) (Library.drop (i, ts)) |
557 ||>> invoke_cg_type thy defs ty_use |
543 |-> pair o mk_apps; |
558 |> debug 10 (fn _ => "making application (8)") |
|
559 |-> (fn (((f, args), lookup), ty_use) => |
|
560 pair (mk_apps (mk_itapp (IConst (f, ty_use)) lookup, args))) |
|
561 end; |
|
562 |
|
563 |
544 |
564 local |
545 local |
565 open CodegenThingolOp; |
546 open CodegenThingolOp; |
566 infix 8 `%%; |
547 infix 8 `%%; |
567 infixr 6 `->; |
548 infixr 6 `->; |
568 infixr 6 `-->; |
549 infixr 6 `-->; |
569 infix 4 `$; |
550 infix 4 `$; |
570 infix 4 `$$; |
551 infix 4 `$$; |
|
552 infixr 5 `|->; |
|
553 infixr 5 `|-->; |
571 in |
554 in |
572 |
555 |
573 (* code generators *) |
556 (* code generators *) |
574 |
557 |
575 fun codegen_sort_default thy defs sort trns = |
558 fun codegen_sort_default thy defs sort trns = |
595 trns |
578 trns |
596 |> ensure_def_tyco thy defs (idf_of_tname thy tyco) |
579 |> ensure_def_tyco thy defs (idf_of_tname thy tyco) |
597 ||>> fold_map (invoke_cg_type thy defs) tys |
580 ||>> fold_map (invoke_cg_type thy defs) tys |
598 |-> (fn (tyco, tys) => succeed (tyco `%% tys)) |
581 |-> (fn (tyco, tys) => succeed (tyco `%% tys)) |
599 |
582 |
600 fun codegen_expr_default thy defs t trns = |
583 fun codegen_expr_default thy defs (Const (f, ty)) trns = |
601 let |
584 let |
602 val (u, ts) = strip_comb t; |
585 val _ = debug 5 (fn _ => "making application of " ^ quote f) (); |
603 fun name_of_var (Free (v, _)) = v |
586 val ty_def = Sign.the_const_constraint thy f; |
604 | name_of_var (Var ((v, i), _)) = if i=0 then v else v ^ string_of_int i |
587 val _ = debug 10 (fn _ => "making application (2)") (); |
605 fun cg_default (Var (_, ty)) = |
588 fun mk_lookup (ClassPackage.Instance (i, ls)) trns = |
606 trns |
589 trns |
607 |> fold_map (invoke_cg_expr thy defs) ts |
590 |> ensure_def_class thy defs ((idf_of_name thy nsp_class o fst) i) |
608 ||>> invoke_cg_type thy defs ty |
591 ||>> ensure_def_class thy defs (idf_of_inst thy defs i) |
609 |-> (fn (args, ty) => succeed (IVarE (name_of_var u, ty) `$$ args)) |
592 ||>> (fold_map o fold_map) mk_lookup ls |
610 | cg_default (Free (_, ty)) = |
593 |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls))) |
611 trns |
594 | mk_lookup (ClassPackage.Lookup (clss, (v, i))) trns = |
612 |> fold_map (invoke_cg_expr thy defs) ts |
595 trns |
613 ||>> invoke_cg_type thy defs ty |
596 |> fold_map (ensure_def_class thy defs) (map (idf_of_name thy nsp_class) clss) |
614 |-> (fn (args, ty) => succeed (IVarE (name_of_var u, ty) `$$ args)) |
597 |-> (fn clss => pair (ClassPackage.Lookup (clss, (name_of_tvar (TFree (v, [])), i)))); |
615 | cg_default (Const (f, ty)) = |
598 val _ = debug 10 (fn _ => "making application (3)") (); |
616 trns |
599 fun mk_itapp e [] = e |
617 |> mk_app thy defs f ty ts |
600 | mk_itapp e lookup = IInst (e, lookup); |
618 |-> (fn e => succeed e) |
601 in |
619 | cg_default (Abs _) = |
602 trns |
620 let |
603 |> debug 10 (fn _ => "making application (4): " ^ f ^ "::" ^ Sign.string_of_typ thy ty ^ " <~> " ^ Sign.string_of_typ thy ty_def) |
621 val (bs, tys) = ListPair.unzip (strip_abs_vars u); |
604 |> ensure_def_const thy defs (idf_of_cname thy defs (f, ty)) |
622 val t = strip_abs_body u; |
605 |> debug 10 (fn _ => "making application (5)") |
623 val bs' = Codegen.new_names t bs; |
606 ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty)) |
624 val t' = subst_bounds (map Free (rev (bs' ~~ tys)), t) |
607 |> debug 10 (fn _ => "making application (6)") |
625 in |
608 ||>> invoke_cg_type thy defs ty |
626 trns |
609 |> debug 10 (fn _ => "making application (7)") |
627 |> fold_map (invoke_cg_expr thy defs) ts |
610 |-> (fn ((f, lookup), ty) => |
628 ||>> invoke_cg_expr thy defs t' |
611 succeed (mk_itapp (IConst (f, ty)) lookup)) |
629 |-> (fn (es, e) => succeed (e `$$ es)) |
612 end |
630 end; |
613 | codegen_expr_default thy defs (Free (v, ty)) trns = |
631 in cg_default u end; |
614 trns |
|
615 |> invoke_cg_type thy defs ty |
|
616 |-> (fn ty => succeed (IVarE (v, ty))) |
|
617 | codegen_expr_default thy defs (Var ((v, i), ty)) trns = |
|
618 trns |
|
619 |> invoke_cg_type thy defs ty |
|
620 |-> (fn ty => succeed (IVarE (if i=0 then v else v ^ string_of_int i, ty))) |
|
621 | codegen_expr_default thy defs (Abs (v, ty, t)) trns = |
|
622 trns |
|
623 |> invoke_cg_type thy defs ty |
|
624 ||>> invoke_cg_expr thy defs (subst_bound (Free (v, ty), t)) |
|
625 |-> (fn (ty, e) => succeed ((v, ty) `|-> e)) |
|
626 | codegen_expr_default thy defs (t1 $ t2) trns = |
|
627 trns |
|
628 |> invoke_cg_expr thy defs t1 |
|
629 ||>> invoke_cg_expr thy defs t2 |
|
630 |-> (fn (e1, e2) => succeed (e1 `$ e2)); |
632 |
631 |
633 (*fun codegen_eq thy defs t trns = |
632 (*fun codegen_eq thy defs t trns = |
634 let |
633 let |
635 fun cg_eq (Const ("op =", _), [t, u]) = |
634 fun cg_eq (Const ("op =", _), [t, u]) = |
636 trns |
635 trns |
807 |> invoke_cg_expr thy defs (mk_int_to_nat bin) |
806 |> invoke_cg_expr thy defs (mk_int_to_nat bin) |
808 |-> (fn expr => succeed expr) |
807 |-> (fn expr => succeed expr) |
809 | codegen_number_of dest_binum mk_int_to_nat thy defs t trns = |
808 | codegen_number_of dest_binum mk_int_to_nat thy defs t trns = |
810 trns |
809 trns |
811 |> fail ("not a number: " ^ Sign.string_of_term thy t); |
810 |> fail ("not a number: " ^ Sign.string_of_term thy t); |
|
811 |
|
812 fun codegen_case get_case_const_data thy defs t trns = |
|
813 let |
|
814 fun cg_case_d gen_names dty (((cname, i), ty), t) trns = |
|
815 let |
|
816 val vs = gen_names i; |
|
817 val tys = Library.take (i, (fst o strip_type) ty); |
|
818 val frees = map2 Free (vs, tys); |
|
819 val t' = Envir.beta_norm (list_comb (t, frees)); |
|
820 in |
|
821 trns |
|
822 |> invoke_cg_expr thy defs (list_comb (Const (cname, tys ---> dty), frees)) |
|
823 ||>> invoke_cg_expr thy defs t' |
|
824 |-> (fn (ep, e) => pair (ipat_of_iexpr ep, e)) |
|
825 end; |
|
826 fun cg_case dty cs (_, ts) trns = |
|
827 let |
|
828 val (ts', t) = split_last ts |
|
829 val _ = debug 10 (fn _ => " in " ^ Sign.string_of_typ thy dty ^ ", pairing " |
|
830 ^ (commas o map (fst o fst)) cs ^ " with " ^ (commas o map (Sign.string_of_term thy)) ts') (); |
|
831 fun gen_names i = |
|
832 variantlist (replicate i "x", foldr add_term_names |
|
833 (map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts) |
|
834 in |
|
835 trns |
|
836 |> invoke_cg_expr thy defs t |
|
837 ||>> fold_map (cg_case_d gen_names dty) (cs ~~ ts') |
|
838 |-> (fn (t, ds) => pair (ICase (t, ds))) |
|
839 end; |
|
840 in case strip_comb t |
|
841 of (t as Const (f, ty), ts) => |
|
842 (case get_case_const_data thy f |
|
843 of NONE => |
|
844 trns |
|
845 |> fail ("not a case constant: " ^ quote f) |
|
846 | SOME cs => |
|
847 let |
|
848 val (tys, dty) = (split_last o fst o strip_type) ty; |
|
849 in |
|
850 trns |
|
851 |> debug 9 (fn _ => "for case const " ^ f ^ "::" |
|
852 ^ Sign.string_of_typ thy ty ^ ",\n with " ^ AList.string_of_alist I string_of_int cs |
|
853 ^ ",\n given as args " ^ (commas o map (Sign.string_of_term thy)) ts |
|
854 ^ ",\n with significant length " ^ string_of_int (length cs + 1)) |
|
855 |> fix_nargs thy defs (cg_case dty (cs ~~ tys)) |
|
856 (length cs + 1) (t, ts) |
|
857 |-> succeed |
|
858 end |
|
859 ) |
|
860 | _ => |
|
861 trns |
|
862 |> fail ("not a case constant expression: " ^ Sign.string_of_term thy t) |
|
863 end; |
812 |
864 |
813 fun defgen_datatype get_datatype thy defs tyco trns = |
865 fun defgen_datatype get_datatype thy defs tyco trns = |
814 case tname_of_idf thy tyco |
866 case tname_of_idf thy tyco |
815 of SOME dtname => |
867 of SOME dtname => |
816 (case get_datatype thy tyco |
868 (case get_datatype thy tyco |
910 fun mk_idf ("0", Type ("nat", [])) = "const.Zero" |
962 fun mk_idf ("0", Type ("nat", [])) = "const.Zero" |
911 | mk_idf ("1", Type ("nat", [])) = "." |
963 | mk_idf ("1", Type ("nat", [])) = "." |
912 | mk_idf (nm, ty) = |
964 | mk_idf (nm, ty) = |
913 if is_number nm |
965 if is_number nm |
914 then nm |
966 then nm |
915 else idf_of_name thy nsp_const |
967 else idf_of_name thy nsp_const nm |
916 (((perhaps o Symtab.lookup) ((fst o #alias o #logic_data o CodegenData.get) thy) nm) |
968 ^ "_" ^ mangle_tyname (ty_decl, ty) |
917 ^ "_" ^ mangle_tyname (ty_decl, ty)) |
|
918 val overl_lookups = map |
969 val overl_lookups = map |
919 (fn (ty, (_, (args, rhs))) => (ty, mk_idf (name, ty), args, rhs)) ds; |
970 (fn (ty, (_, (args, rhs))) => (ty, mk_idf (name, ty), args, rhs)) ds; |
920 in |
971 in |
921 ((overl |> Symtab.update_new (name, map (fn (ty, idf, _, _) => (ty, idf)) overl_lookups), |
972 ((overl |> Symtab.update_new (name, map (fn (ty, idf, _, _) => (ty, idf)) overl_lookups), |
922 overl_rev |> fold Symtab.update_new (map (fn (ty, idf, _, _) => (idf, (name, ty))) overl_lookups)), |
973 overl_rev |> fold Symtab.update_new (map (fn (ty, idf, _, _) => (idf, (name, ty))) overl_lookups)), |
962 (fn (class, (clsmems, _)) => fold |
1013 (fn (class, (clsmems, _)) => fold |
963 (fn clsmem => Symtab.update (clsmem, class)) clsmems) |
1014 (fn clsmem => Symtab.update (clsmem, class)) clsmems) |
964 classtab)) |
1015 classtab)) |
965 in |
1016 in |
966 ((Symtab.empty, Symtab.empty), Symtab.empty, (Insttab.empty, Symtab.empty, Symtab.empty)) |
1017 ((Symtab.empty, Symtab.empty), Symtab.empty, (Insttab.empty, Symtab.empty, Symtab.empty)) |
|
1018 |> add_clsmems (ClassPackage.get_classtab thy) |
967 |> fold add_def (Codegen.mk_deftab thy |> Symtab.dest) |
1019 |> fold add_def (Codegen.mk_deftab thy |> Symtab.dest) |
968 |> add_clsmems (ClassPackage.get_classtab thy) |
|
969 end; |
1020 end; |
970 |
1021 |
971 fun expand_module defs gen thy = |
1022 fun expand_module defs gen thy = |
972 let |
1023 let |
973 fun put_module modl = |
1024 fun put_module modl = |
1100 |
1151 |
1101 fun get_serializer thy serial_name = |
1152 fun get_serializer thy serial_name = |
1102 (#serializer o (fn data => (the oo Symtab.lookup) data serial_name) |
1153 (#serializer o (fn data => (the oo Symtab.lookup) data serial_name) |
1103 o #serialize_data o CodegenData.get) thy; |
1154 o #serialize_data o CodegenData.get) thy; |
1104 |
1155 |
1105 fun mk_const thy f = |
1156 fun mk_const thy (f, s_ty) = |
1106 let |
1157 let |
1107 val f' = Sign.intern_const thy f; |
1158 val f' = Sign.intern_const thy f; |
1108 in (f', Sign.the_const_constraint thy f') end; |
1159 val ty = case s_ty |
1109 |
1160 of NONE => Sign.the_const_constraint thy f' |
1110 fun gen_generate_code consts thy = |
1161 | SOME s => Sign.read_typ (thy, K NONE) s; |
|
1162 in (f', ty) end; |
|
1163 |
|
1164 fun generate_code consts thy = |
1111 let |
1165 let |
1112 val defs = mk_deftab thy; |
1166 val defs = mk_deftab thy; |
1113 val consts' = map (idf_of_cname thy defs) consts; |
1167 val consts' = map (idf_of_cname thy defs o mk_const thy) consts; |
1114 fun generate thy defs = fold_map (ensure_def_const thy defs) consts' |
1168 fun generate thy defs = fold_map (ensure_def_const thy defs) consts' |
1115 in |
1169 in |
1116 thy |
1170 thy |
1117 |> expand_module defs generate |
1171 |> expand_module defs generate |
1118 |-> (fn _ => pair consts') |
1172 |-> (fn _ => pair consts') |
1119 end; |
1173 end; |
1120 |
|
1121 fun generate_code consts thy = |
|
1122 gen_generate_code (map (mk_const thy) consts) thy; |
|
1123 |
1174 |
1124 fun serialize_code serial_name filename consts thy = |
1175 fun serialize_code serial_name filename consts thy = |
1125 let |
1176 let |
1126 fun mk_sfun tab name args f = |
1177 fun mk_sfun tab name args f = |
1127 Symtab.lookup tab name |
1178 Symtab.lookup tab name |
1163 val (generateK, serializeK, extractingK, aliasK, definedK, dependingK, syntax_tycoK, syntax_constK) = |
1213 val (generateK, serializeK, extractingK, aliasK, definedK, dependingK, syntax_tycoK, syntax_constK) = |
1164 ("code_generate", "code_serialize", "extracting", "defined_by", "depending_on", "code_alias", "code_syntax_tyco", "code_syntax_const"); |
1214 ("code_generate", "code_serialize", "extracting", "defined_by", "depending_on", "code_alias", "code_syntax_tyco", "code_syntax_const"); |
1165 |
1215 |
1166 val generateP = |
1216 val generateP = |
1167 OuterSyntax.command generateK "generate executable code for constants" K.thy_decl ( |
1217 OuterSyntax.command generateK "generate executable code for constants" K.thy_decl ( |
1168 Scan.repeat1 P.name |
1218 Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) |
1169 >> (fn consts => |
1219 >> (fn consts => |
1170 Toplevel.theory (generate_code consts #> snd)) |
1220 Toplevel.theory (generate_code consts #> snd)) |
1171 ); |
1221 ); |
1172 |
1222 |
1173 val serializeP = |
1223 val serializeP = |
1174 OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl ( |
1224 OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl ( |
1175 P.name |
1225 P.name |
1176 -- P.name |
1226 -- P.name |
1177 -- Scan.option ( |
1227 -- Scan.option ( |
1178 P.$$$ extractingK |
1228 P.$$$ extractingK |
1179 |-- Scan.repeat1 P.name |
1229 |-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) |
1180 ) |
1230 ) |
1181 >> (fn ((serial_name, filename), consts) => |
1231 >> (fn ((serial_name, filename), consts) => |
1182 Toplevel.theory (serialize_code serial_name filename consts)) |
1232 Toplevel.theory (serialize_code serial_name filename consts)) |
1183 ); |
1233 ); |
1184 |
1234 |
1251 add_defgen ("clsmem", defgen_clsmem), |
1301 add_defgen ("clsmem", defgen_clsmem), |
1252 add_defgen ("clsinst", defgen_clsinst), |
1302 add_defgen ("clsinst", defgen_clsinst), |
1253 add_alias ("op <>", "neq"), |
1303 add_alias ("op <>", "neq"), |
1254 add_alias ("op >=", "ge"), |
1304 add_alias ("op >=", "ge"), |
1255 add_alias ("op >", "gt"), |
1305 add_alias ("op >", "gt"), |
|
1306 add_alias ("op <=", "le"), |
|
1307 add_alias ("op <", "lt"), |
|
1308 add_alias ("op +", "add"), |
1256 add_alias ("op -", "minus"), |
1309 add_alias ("op -", "minus"), |
|
1310 add_alias ("op *", "times"), |
1257 add_alias ("op @", "append"), |
1311 add_alias ("op @", "append"), |
1258 add_lookup_tyco ("bool", type_bool), |
1312 add_lookup_tyco ("bool", type_bool), |
1259 add_lookup_tyco ("IntDef.int", type_integer), |
1313 add_lookup_tyco ("IntDef.int", type_integer), |
1260 add_lookup_tyco ("List.list", type_list), |
1314 add_lookup_tyco ("List.list", type_list), |
1261 add_lookup_tyco ("*", type_pair), |
1315 add_lookup_tyco ("*", type_pair), |