79 fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) = |
79 fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) = |
80 let val rec_names = map (scan_to_id o trim o fst) rec_pairs |
80 let val rec_names = map (scan_to_id o trim o fst) rec_pairs |
81 val big_rec_name = space_implode "_" rec_names |
81 val big_rec_name = space_implode "_" rec_names |
82 and srec_tms = mk_list (map fst rec_pairs) |
82 and srec_tms = mk_list (map fst rec_pairs) |
83 and scons = mk_scons rec_pairs |
83 and scons = mk_scons rec_pairs |
84 and sdom = (*default domain?*) |
84 and sdom_sum = |
85 if dom = "" then co ^ "data_domain rec_tms" |
85 if dom = "" then co ^ "data_domain rec_tms" (*default*) |
86 else "replicate " ^ string_of_int (length rec_names) ^ |
86 else "readtm (sign_of thy) iT " ^ dom |
87 " (readtm (sign_of thy) iT " ^ dom ^ ")" |
|
88 val stri_name = big_rec_name ^ "_Intrnl" |
87 val stri_name = big_rec_name ^ "_Intrnl" |
89 val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs) |
88 val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs) |
90 in |
89 in |
91 (";\n\n\ |
90 (";\n\n\ |
92 \structure " ^ stri_name ^ " =\n\ |
91 \structure " ^ stri_name ^ " =\n\ |
93 \ let open Ind_Syntax in\n\ |
92 \ let open Ind_Syntax in\n\ |
94 \ struct\n\ |
93 \ struct\n\ |
|
94 \ val _ = writeln \"" ^ co ^ |
|
95 "Datatype definition " ^ big_rec_name ^ "\"\n\ |
95 \ val rec_tms\t= map (readtm (sign_of thy) iT) " ^ srec_tms ^ "\n\ |
96 \ val rec_tms\t= map (readtm (sign_of thy) iT) " ^ srec_tms ^ "\n\ |
96 \ val domts\t= " ^ sdom ^ "\n\ |
97 \ val dom_sum\t= " ^ sdom_sum ^ "\n\ |
97 \ and con_ty_lists\t= read_constructs (sign_of thy)\n" |
98 \ and con_ty_lists\t= read_constructs (sign_of thy)\n" |
98 ^ scons ^ "\n\ |
99 ^ scons ^ "\n\ |
99 \ val intr_tms\t= mk_all_intr_tms (rec_tms, con_ty_lists)\n\ |
100 \ val intr_tms\t= mk_all_intr_tms (rec_tms, con_ty_lists)\n\ |
100 \ end\n\ |
101 \ end\n\ |
101 \ end;\n\n\ |
102 \ end;\n\n\ |
102 \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ |
103 \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ |
103 mk_list (map quote rec_names) ^ ", " ^ |
104 mk_list (map quote rec_names) ^ ", " ^ |
104 stri_name ^ ".con_ty_lists) \n\ |
105 stri_name ^ ".con_ty_lists) \n\ |
105 \ |> " ^ co ^ "Ind.add_fp_def_i \n (" ^ |
106 \ |> " ^ co ^ "Ind.add_fp_def_i \n (" ^ |
106 stri_name ^ ".rec_tms, " ^ |
107 stri_name ^ ".rec_tms, " ^ |
107 stri_name ^ ".domts, " ^ |
108 stri_name ^ ".dom_sum, " ^ |
108 stri_name ^ ".intr_tms)" |
109 stri_name ^ ".intr_tms)" |
109 , |
110 , |
110 "structure " ^ big_rec_name ^ " =\n\ |
111 "structure " ^ big_rec_name ^ " =\n\ |
111 \ struct\n\ |
112 \ struct\n\ |
112 \ val _ = writeln \"" ^ co ^ |
113 \ val _ = writeln \"Proofs for " ^ co ^ |
113 "Datatype definition " ^ big_rec_name ^ "\"\n\ |
114 "Datatype definition " ^ big_rec_name ^ "\"\n\ |
114 \ structure Result = " ^ co ^ "Data_section_Fun\n\ |
115 \ structure Result = " ^ co ^ "Data_section_Fun\n\ |
115 \ (open " ^ stri_name ^ "\n\ |
116 \ (open " ^ stri_name ^ "\n\ |
116 \ val thy\t\t= thy\n\ |
117 \ val thy\t\t= thy\n\ |
117 \ val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\ |
118 \ val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\ |