equal
deleted
inserted
replaced
120 if length descr' = 1 then ["P"] |
120 if length descr' = 1 then ["P"] |
121 else map (fn i => "P" ^ string_of_int i) (1 upto length descr'); |
121 else map (fn i => "P" ^ string_of_int i) (1 upto length descr'); |
122 |
122 |
123 fun make_pred i T = |
123 fun make_pred i T = |
124 let val T' = T --> HOLogic.boolT |
124 let val T' = T --> HOLogic.boolT |
125 in Free (List.nth (pnames, i), T') end; |
125 in Free (nth pnames i, T') end; |
126 |
126 |
127 fun make_ind_prem k T (cname, cargs) = |
127 fun make_ind_prem k T (cname, cargs) = |
128 let |
128 let |
129 fun mk_prem ((dt, s), T) = |
129 fun mk_prem ((dt, s), T) = |
130 let val (Us, U) = strip_type T |
130 let val (Us, U) = strip_type T |
197 let |
197 let |
198 val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs; |
198 val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs; |
199 val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts); |
199 val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts); |
200 |
200 |
201 fun mk_argT (dt, T) = |
201 fun mk_argT (dt, T) = |
202 binder_types T ---> List.nth (rec_result_Ts, Datatype_Aux.body_index dt); |
202 binder_types T ---> nth rec_result_Ts (Datatype_Aux.body_index dt); |
203 |
203 |
204 val argTs = Ts @ map mk_argT recs |
204 val argTs = Ts @ map mk_argT recs |
205 in argTs ---> List.nth (rec_result_Ts, i) |
205 in argTs ---> nth rec_result_Ts i end) constrs) descr'; |
206 end) constrs) descr'; |
|
207 |
206 |
208 in (rec_result_Ts, reccomb_fn_Ts) end; |
207 in (rec_result_Ts, reccomb_fn_Ts) end; |
209 |
208 |
210 fun make_primrecs new_type_names descr sorts thy = |
209 fun make_primrecs new_type_names descr sorts thy = |
211 let |
210 let |
236 val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs)); |
235 val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs)); |
237 val frees = map Free (tnames ~~ Ts); |
236 val frees = map Free (tnames ~~ Ts); |
238 val frees' = map Free (rec_tnames ~~ recTs'); |
237 val frees' = map Free (rec_tnames ~~ recTs'); |
239 |
238 |
240 fun mk_reccomb ((dt, T), t) = |
239 fun mk_reccomb ((dt, T), t) = |
241 let val (Us, U) = strip_type T |
240 let val (Us, U) = strip_type T in |
242 in list_abs (map (pair "x") Us, |
241 list_abs (map (pair "x") Us, |
243 List.nth (reccombs, Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us)) |
242 nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us)) |
244 end; |
243 end; |
245 |
244 |
246 val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees') |
245 val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees') |
247 |
246 |
248 in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq |
247 in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq |