108 (* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *) |
108 (* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *) |
109 fun tuple_list_for_name rel_table bounds name = |
109 fun tuple_list_for_name rel_table bounds name = |
110 the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]] |
110 the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]] |
111 |
111 |
112 (* term -> term *) |
112 (* term -> term *) |
113 fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) = |
113 fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) = |
114 unarize_and_unbox_term t1 |
114 unarize_unbox_etc_term t1 |
115 | unarize_and_unbox_term (Const (@{const_name PairBox}, |
115 | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) = |
116 Type ("fun", [T1, Type ("fun", [T2, _])])) |
116 unarize_unbox_etc_term t1 |
117 $ t1 $ t2) = |
117 | unarize_unbox_etc_term |
118 let val Ts = map unarize_unbox_and_uniterize_type [T1, T2] in |
118 (Const (@{const_name PairBox}, |
119 Const (@{const_name Pair}, Ts ---> Type ("*", Ts)) |
119 Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])])) |
120 $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2 |
120 $ t1 $ t2) = |
|
121 let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in |
|
122 Const (@{const_name Pair}, Ts ---> Type (@{type_name "*"}, Ts)) |
|
123 $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2 |
121 end |
124 end |
122 | unarize_and_unbox_term (Const (s, T)) = |
125 | unarize_unbox_etc_term (Const (s, T)) = |
123 Const (s, unarize_unbox_and_uniterize_type T) |
126 Const (s, uniterize_unarize_unbox_etc_type T) |
124 | unarize_and_unbox_term (t1 $ t2) = |
127 | unarize_unbox_etc_term (t1 $ t2) = |
125 unarize_and_unbox_term t1 $ unarize_and_unbox_term t2 |
128 unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2 |
126 | unarize_and_unbox_term (Free (s, T)) = |
129 | unarize_unbox_etc_term (Free (s, T)) = |
127 Free (s, unarize_unbox_and_uniterize_type T) |
130 Free (s, uniterize_unarize_unbox_etc_type T) |
128 | unarize_and_unbox_term (Var (x, T)) = |
131 | unarize_unbox_etc_term (Var (x, T)) = |
129 Var (x, unarize_unbox_and_uniterize_type T) |
132 Var (x, uniterize_unarize_unbox_etc_type T) |
130 | unarize_and_unbox_term (Bound j) = Bound j |
133 | unarize_unbox_etc_term (Bound j) = Bound j |
131 | unarize_and_unbox_term (Abs (s, T, t')) = |
134 | unarize_unbox_etc_term (Abs (s, T, t')) = |
132 Abs (s, unarize_unbox_and_uniterize_type T, unarize_and_unbox_term t') |
135 Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t') |
133 |
136 |
134 (* typ -> typ -> (typ * typ) * (typ * typ) *) |
137 (* typ -> typ -> (typ * typ) * (typ * typ) *) |
135 fun factor_out_types (T1 as Type ("*", [T11, T12])) |
138 fun factor_out_types (T1 as Type (@{type_name "*"}, [T11, T12])) |
136 (T2 as Type ("*", [T21, T22])) = |
139 (T2 as Type (@{type_name "*"}, [T21, T22])) = |
137 let val (n1, n2) = pairself num_factors_in_type (T11, T21) in |
140 let val (n1, n2) = pairself num_factors_in_type (T11, T21) in |
138 if n1 = n2 then |
141 if n1 = n2 then |
139 let |
142 let |
140 val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22 |
143 val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22 |
141 in |
144 in |
142 ((Type ("*", [T11, T11']), opt_T12'), |
145 ((Type (@{type_name "*"}, [T11, T11']), opt_T12'), |
143 (Type ("*", [T21, T21']), opt_T22')) |
146 (Type (@{type_name "*"}, [T21, T21']), opt_T22')) |
144 end |
147 end |
145 else if n1 < n2 then |
148 else if n1 < n2 then |
146 case factor_out_types T1 T21 of |
149 case factor_out_types T1 T21 of |
147 (p1, (T21', NONE)) => (p1, (T21', SOME T22)) |
150 (p1, (T21', NONE)) => (p1, (T21', SOME T22)) |
148 | (p1, (T21', SOME T22')) => |
151 | (p1, (T21', SOME T22')) => |
149 (p1, (T21', SOME (Type ("*", [T22', T22])))) |
152 (p1, (T21', SOME (Type (@{type_name "*"}, [T22', T22])))) |
150 else |
153 else |
151 swap (factor_out_types T2 T1) |
154 swap (factor_out_types T2 T1) |
152 end |
155 end |
153 | factor_out_types (Type ("*", [T11, T12])) T2 = ((T11, SOME T12), (T2, NONE)) |
156 | factor_out_types (Type (@{type_name "*"}, [T11, T12])) T2 = |
154 | factor_out_types T1 (Type ("*", [T21, T22])) = ((T1, NONE), (T21, SOME T22)) |
157 ((T11, SOME T12), (T2, NONE)) |
|
158 | factor_out_types T1 (Type (@{type_name "*"}, [T21, T22])) = |
|
159 ((T1, NONE), (T21, SOME T22)) |
155 | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE)) |
160 | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE)) |
156 |
161 |
157 (* bool -> typ -> typ -> (term * term) list -> term *) |
162 (* bool -> typ -> typ -> (term * term) list -> term *) |
158 fun make_plain_fun maybe_opt T1 T2 = |
163 fun make_plain_fun maybe_opt T1 T2 = |
159 let |
164 let |
186 val cut = length (HOLogic.strip_tupleT T1) |
191 val cut = length (HOLogic.strip_tupleT T1) |
187 val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2) |
192 val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2) |
188 val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut |
193 val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut |
189 in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end |
194 in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end |
190 (* typ -> term -> term -> term *) |
195 (* typ -> term -> term -> term *) |
191 fun pair_up (Type ("*", [T1', T2'])) |
196 fun pair_up (Type (@{type_name "*"}, [T1', T2'])) |
192 (t1 as Const (@{const_name Pair}, |
197 (t1 as Const (@{const_name Pair}, |
193 Type ("fun", [_, Type ("fun", [_, T1])])) $ t11 $ t12) |
198 Type (@{type_name fun}, |
194 t2 = |
199 [_, Type (@{type_name fun}, [_, T1])])) |
|
200 $ t11 $ t12) t2 = |
195 if T1 = T1' then HOLogic.mk_prod (t1, t2) |
201 if T1 = T1' then HOLogic.mk_prod (t1, t2) |
196 else HOLogic.mk_prod (t11, pair_up T2' t12 t2) |
202 else HOLogic.mk_prod (t11, pair_up T2' t12 t2) |
197 | pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2) |
203 | pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2) |
198 (* typ -> term -> term list * term list -> (term * term) list*) |
204 (* typ -> term -> term list * term list -> (term * term) list*) |
199 fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3 |
205 fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3 |
200 |
206 |
201 (* typ -> typ -> typ -> term -> term *) |
207 (* typ -> typ -> typ -> term -> term *) |
202 fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t = |
208 fun typecast_fun (Type (@{type_name fun}, [T1', T2'])) T1 T2 t = |
203 let |
209 let |
204 (* typ -> typ -> typ -> typ -> term -> term *) |
210 (* typ -> typ -> typ -> typ -> term -> term *) |
205 fun do_curry T1 T1a T1b T2 t = |
211 fun do_curry T1 T1a T1b T2 t = |
206 let |
212 let |
207 val (maybe_opt, ps) = dest_plain_fun t |
213 val (maybe_opt, ps) = dest_plain_fun t |
236 t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2) |
242 t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2) |
237 | ((T1a', SOME T1b'), (_, NONE)) => |
243 | ((T1a', SOME T1b'), (_, NONE)) => |
238 t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2' |
244 t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2' |
239 | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], []) |
245 | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], []) |
240 (* typ -> typ -> term -> term *) |
246 (* typ -> typ -> term -> term *) |
241 and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t = |
247 and do_term (Type (@{type_name fun}, [T1', T2'])) |
|
248 (Type (@{type_name fun}, [T1, T2])) t = |
242 do_fun T1' T2' T1 T2 t |
249 do_fun T1' T2' T1 T2 t |
243 | do_term (T' as Type ("*", Ts' as [T1', T2'])) (Type ("*", [T1, T2])) |
250 | do_term (T' as Type (@{type_name "*"}, Ts' as [T1', T2'])) |
|
251 (Type (@{type_name "*"}, [T1, T2])) |
244 (Const (@{const_name Pair}, _) $ t1 $ t2) = |
252 (Const (@{const_name Pair}, _) $ t1 $ t2) = |
245 Const (@{const_name Pair}, Ts' ---> T') |
253 Const (@{const_name Pair}, Ts' ---> T') |
246 $ do_term T1' T1 t1 $ do_term T2' T2 t2 |
254 $ do_term T1' T1 t1 $ do_term T2' T2 t2 |
247 | do_term T' T t = |
255 | do_term T' T t = |
248 if T = T' then t |
256 if T = T' then t |
305 tps then |
313 tps then |
306 Const (unknown, T1 --> T2) |
314 Const (unknown, T1 --> T2) |
307 else |
315 else |
308 aux tps |
316 aux tps |
309 end |
317 end |
310 (* typ -> typ -> typ -> (term * term) list -> term *) |
318 (* bool -> typ -> typ -> typ -> (term * term) list -> term *) |
311 fun make_map T1 T2 T2' = |
319 fun make_map maybe_opt T1 T2 T2' = |
312 let |
320 let |
313 val update_const = Const (@{const_name fun_upd}, |
321 val update_const = Const (@{const_name fun_upd}, |
314 (T1 --> T2) --> T1 --> T2 --> T1 --> T2) |
322 (T1 --> T2) --> T1 --> T2 --> T1 --> T2) |
315 (* (term * term) list -> term *) |
323 (* (term * term) list -> term *) |
316 fun aux' [] = Const (@{const_abbrev Map.empty}, T1 --> T2) |
324 fun aux' [] = Const (@{const_abbrev Map.empty}, T1 --> T2) |
317 | aux' ((t1, t2) :: ps) = |
325 | aux' ((t1, t2) :: ps) = |
318 (case t2 of |
326 (case t2 of |
319 Const (@{const_name None}, _) => aux' ps |
327 Const (@{const_name None}, _) => aux' ps |
320 | _ => update_const $ aux' ps $ t1 $ t2) |
328 | _ => update_const $ aux' ps $ t1 $ t2) |
321 fun aux ps = |
329 fun aux ps = |
322 if not (is_complete_type datatypes false T1) then |
330 if maybe_opt andalso not (is_complete_type datatypes false T1) then |
323 update_const $ aux' ps $ Const (unrep, T1) |
331 update_const $ aux' ps $ Const (unrep, T1) |
324 $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2')) |
332 $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2')) |
325 else |
333 else |
326 aux' ps |
334 aux' ps |
327 in aux end |
335 in aux end |
328 (* typ list -> term -> term *) |
336 (* typ list -> term -> term *) |
329 fun polish_funs Ts t = |
337 fun polish_funs Ts t = |
330 (case fastype_of1 (Ts, t) of |
338 (case fastype_of1 (Ts, t) of |
331 Type ("fun", [T1, T2]) => |
339 Type (@{type_name fun}, [T1, T2]) => |
332 if is_plain_fun t then |
340 if is_plain_fun t then |
333 case T2 of |
341 case T2 of |
334 @{typ bool} => |
342 @{typ bool} => |
335 let |
343 let |
336 val (maybe_opt, ts_pair) = |
344 val (maybe_opt, ts_pair) = |
354 $ (t2 as Const (s, _)) => |
362 $ (t2 as Const (s, _)) => |
355 if s = unknown then polish_funs Ts t11 |
363 if s = unknown then polish_funs Ts t11 |
356 else polish_funs Ts t1 $ polish_funs Ts t2 |
364 else polish_funs Ts t1 $ polish_funs Ts t2 |
357 | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2 |
365 | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2 |
358 | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t') |
366 | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t') |
359 | Const (s, Type ("fun", [T1, T2])) => |
367 | Const (s, Type (@{type_name fun}, [T1, T2])) => |
360 if s = opt_flag orelse s = non_opt_flag then |
368 if s = opt_flag orelse s = non_opt_flag then |
361 Abs ("x", T1, Const (unknown, T2)) |
369 Abs ("x", T1, Const (unknown, T2)) |
362 else |
370 else |
363 t |
371 t |
364 | t => t |
372 | t => t |
365 (* bool -> typ -> typ -> typ -> term list -> term list -> term *) |
373 (* bool -> typ -> typ -> typ -> term list -> term list -> term *) |
366 fun make_fun maybe_opt T1 T2 T' ts1 ts2 = |
374 fun make_fun maybe_opt T1 T2 T' ts1 ts2 = |
367 ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst) |
375 ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst) |
368 |> make_plain_fun maybe_opt T1 T2 |
376 |> make_plain_fun maybe_opt T1 T2 |
369 |> unarize_and_unbox_term |
377 |> unarize_unbox_etc_term |
370 |> typecast_fun (unarize_unbox_and_uniterize_type T') |
378 |> typecast_fun (uniterize_unarize_unbox_etc_type T') |
371 (unarize_unbox_and_uniterize_type T1) |
379 (uniterize_unarize_unbox_etc_type T1) |
372 (unarize_unbox_and_uniterize_type T2) |
380 (uniterize_unarize_unbox_etc_type T2) |
373 (* (typ * int) list -> typ -> typ -> int -> term *) |
381 (* (typ * int) list -> typ -> typ -> int -> term *) |
374 fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j _ = |
382 fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ = |
375 let |
383 let |
376 val k1 = card_of_type card_assigns T1 |
384 val k1 = card_of_type card_assigns T1 |
377 val k2 = card_of_type card_assigns T2 |
385 val k2 = card_of_type card_assigns T2 |
378 in |
386 in |
379 term_for_rep seen T T' (Vect (k1, Atom (k2, 0))) |
387 term_for_rep true seen T T' (Vect (k1, Atom (k2, 0))) |
380 [nth_combination (replicate k1 (k2, 0)) j] |
388 [nth_combination (replicate k1 (k2, 0)) j] |
381 handle General.Subscript => |
389 handle General.Subscript => |
382 raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom", |
390 raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom", |
383 signed_string_of_int j ^ " for " ^ |
391 signed_string_of_int j ^ " for " ^ |
384 string_for_rep (Vect (k1, Atom (k2, 0)))) |
392 string_for_rep (Vect (k1, Atom (k2, 0)))) |
385 end |
393 end |
386 | term_for_atom seen (Type ("*", [T1, T2])) _ j k = |
394 | term_for_atom seen (Type (@{type_name "*"}, [T1, T2])) _ j k = |
387 let |
395 let |
388 val k1 = card_of_type card_assigns T1 |
396 val k1 = card_of_type card_assigns T1 |
389 val k2 = k div k1 |
397 val k2 = k div k1 |
390 in |
398 in |
391 list_comb (HOLogic.pair_const T1 T2, |
399 list_comb (HOLogic.pair_const T1 T2, |
517 (* (typ * int) list -> int -> rep -> typ -> typ -> typ -> int list |
526 (* (typ * int) list -> int -> rep -> typ -> typ -> typ -> int list |
518 -> term *) |
527 -> term *) |
519 and term_for_vect seen k R T1 T2 T' js = |
528 and term_for_vect seen k R T1 T2 T' js = |
520 make_fun true T1 T2 T' |
529 make_fun true T1 T2 T' |
521 (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k)) |
530 (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k)) |
522 (map (term_for_rep seen T2 T2 R o single) |
531 (map (term_for_rep true seen T2 T2 R o single) |
523 (batch_list (arity_of_rep R) js)) |
532 (batch_list (arity_of_rep R) js)) |
524 (* (typ * int) list -> typ -> typ -> rep -> int list list -> term *) |
533 (* bool -> (typ * int) list -> typ -> typ -> rep -> int list list -> term *) |
525 and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1 |
534 and term_for_rep _ seen T T' Unit [[]] = term_for_atom seen T T' 0 1 |
526 | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] = |
535 | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] = |
527 if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k |
536 if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k |
528 else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R]) |
537 else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R]) |
529 | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] = |
538 | term_for_rep _ seen (Type (@{type_name "*"}, [T1, T2])) _ |
|
539 (Struct [R1, R2]) [js] = |
530 let |
540 let |
531 val arity1 = arity_of_rep R1 |
541 val arity1 = arity_of_rep R1 |
532 val (js1, js2) = chop arity1 js |
542 val (js1, js2) = chop arity1 js |
533 in |
543 in |
534 list_comb (HOLogic.pair_const T1 T2, |
544 list_comb (HOLogic.pair_const T1 T2, |
535 map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2] |
545 map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2] |
536 [[js1], [js2]]) |
546 [[js1], [js2]]) |
537 end |
547 end |
538 | term_for_rep seen (Type ("fun", [T1, T2])) T' (Vect (k, R')) [js] = |
548 | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T' |
|
549 (Vect (k, R')) [js] = |
539 term_for_vect seen k R' T1 T2 T' js |
550 term_for_vect seen k R' T1 T2 T' js |
540 | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut)) |
551 | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T' |
541 jss = |
552 (Func (R1, Formula Neut)) jss = |
542 let |
553 let |
543 val jss1 = all_combinations_for_rep R1 |
554 val jss1 = all_combinations_for_rep R1 |
544 val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1 |
555 val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1 |
545 val ts2 = |
556 val ts2 = |
546 map (fn js => term_for_rep seen T2 T2 (Atom (2, 0)) |
557 map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0)) |
547 [[int_from_bool (member (op =) jss js)]]) |
558 [[int_from_bool (member (op =) jss js)]]) |
548 jss1 |
559 jss1 |
549 in make_fun false T1 T2 T' ts1 ts2 end |
560 in make_fun false T1 T2 T' ts1 ts2 end |
550 | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss = |
561 | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T' |
|
562 (Func (R1, R2)) jss = |
551 let |
563 let |
552 val arity1 = arity_of_rep R1 |
564 val arity1 = arity_of_rep R1 |
553 val jss1 = all_combinations_for_rep R1 |
565 val jss1 = all_combinations_for_rep R1 |
554 val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1 |
566 val ts1 = map (term_for_rep false seen T1 T1 R1 o single) jss1 |
555 val grouped_jss2 = AList.group (op =) (map (chop arity1) jss) |
567 val grouped_jss2 = AList.group (op =) (map (chop arity1) jss) |
556 val ts2 = map (term_for_rep seen T2 T2 R2 o the_default [] |
568 val ts2 = map (term_for_rep false seen T2 T2 R2 o the_default [] |
557 o AList.lookup (op =) grouped_jss2) jss1 |
569 o AList.lookup (op =) grouped_jss2) jss1 |
558 in make_fun true T1 T2 T' ts1 ts2 end |
570 in make_fun maybe_opt T1 T2 T' ts1 ts2 end |
559 | term_for_rep seen T T' (Opt R) jss = |
571 | term_for_rep _ seen T T' (Opt R) jss = |
560 if null jss then Const (unknown, T) else term_for_rep seen T T' R jss |
572 if null jss then Const (unknown, T) |
561 | term_for_rep _ T _ R jss = |
573 else term_for_rep true seen T T' R jss |
|
574 | term_for_rep _ _ T _ R jss = |
562 raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep", |
575 raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep", |
563 Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^ |
576 Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^ |
564 string_of_int (length jss)) |
577 string_of_int (length jss)) |
565 in polish_funs [] o unarize_and_unbox_term oooo term_for_rep [] end |
578 in polish_funs [] o unarize_unbox_etc_term oooo term_for_rep true [] end |
566 |
579 |
567 (* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list |
580 (* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list |
568 -> nut -> term *) |
581 -> nut -> term *) |
569 fun term_for_name pool scope sel_names rel_table bounds name = |
582 fun term_for_name pool scope sel_names rel_table bounds name = |
570 let val T = type_of name in |
583 let val T = type_of name in |
687 fun pretty_for_assign name = |
700 fun pretty_for_assign name = |
688 let |
701 let |
689 val (oper, (t1, T'), T) = |
702 val (oper, (t1, T'), T) = |
690 case name of |
703 case name of |
691 FreeName (s, T, _) => |
704 FreeName (s, T, _) => |
692 let val t = Free (s, unarize_unbox_and_uniterize_type T) in |
705 let val t = Free (s, uniterize_unarize_unbox_etc_type T) in |
693 ("=", (t, format_term_type thy def_table formats t), T) |
706 ("=", (t, format_term_type thy def_table formats t), T) |
694 end |
707 end |
695 | ConstName (s, T, _) => |
708 | ConstName (s, T, _) => |
696 (assign_operator_for_const (s, T), |
709 (assign_operator_for_const (s, T), |
697 user_friendly_const hol_ctxt base_step_names formats (s, T), T) |
710 user_friendly_const hol_ctxt base_step_names formats (s, T), T) |
708 Pretty.str oper, Syntax.pretty_term ctxt t2]) |
721 Pretty.str oper, Syntax.pretty_term ctxt t2]) |
709 end |
722 end |
710 (* dtype_spec -> Pretty.T *) |
723 (* dtype_spec -> Pretty.T *) |
711 fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) = |
724 fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) = |
712 Pretty.block (Pretty.breaks |
725 Pretty.block (Pretty.breaks |
713 [Syntax.pretty_typ ctxt (unarize_unbox_and_uniterize_type typ), |
726 (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) :: |
714 Pretty.str "=", |
727 (case typ of |
715 Pretty.enum "," "{" "}" |
728 Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"] |
716 (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @ |
729 | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"] |
717 (if fun_from_pair complete false then [] |
730 | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"] |
718 else [Pretty.str unrep]))]) |
731 | _ => []) @ |
|
732 [Pretty.str "=", |
|
733 Pretty.enum "," "{" "}" |
|
734 (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @ |
|
735 (if fun_from_pair complete false then [] |
|
736 else [Pretty.str unrep]))])) |
719 (* typ -> dtype_spec list *) |
737 (* typ -> dtype_spec list *) |
720 fun integer_datatype T = |
738 fun integer_datatype T = |
721 [{typ = T, card = card_of_type card_assigns T, co = false, |
739 [{typ = T, card = card_of_type card_assigns T, co = false, |
722 standard = true, complete = (false, false), concrete = (true, true), |
740 standard = true, complete = (false, false), concrete = (true, true), |
723 deep = true, constrs = []}] |
741 deep = true, constrs = []}] |
750 val (skolem_names, nonskolem_nonsel_names) = |
768 val (skolem_names, nonskolem_nonsel_names) = |
751 List.partition is_skolem_name nonsel_names |
769 List.partition is_skolem_name nonsel_names |
752 val (eval_names, noneval_nonskolem_nonsel_names) = |
770 val (eval_names, noneval_nonskolem_nonsel_names) = |
753 List.partition (String.isPrefix eval_prefix o nickname_of) |
771 List.partition (String.isPrefix eval_prefix o nickname_of) |
754 nonskolem_nonsel_names |
772 nonskolem_nonsel_names |
755 ||> filter_out (curry (op =) @{const_name bisim_iterator_max} |
773 ||> filter_out (member (op =) [@{const_name bisim}, |
|
774 @{const_name bisim_iterator_max}] |
756 o nickname_of) |
775 o nickname_of) |
757 val free_names = |
776 val free_names = |
758 map (fn x as (s, T) => |
777 map (fn x as (s, T) => |
759 case filter (curry (op =) x |
778 case filter (curry (op =) x |
760 o pairf nickname_of |
779 o pairf nickname_of |
761 (unarize_unbox_and_uniterize_type o type_of)) |
780 (uniterize_unarize_unbox_etc_type o type_of)) |
762 free_names of |
781 free_names of |
763 [name] => name |
782 [name] => name |
764 | [] => FreeName (s, T, Any) |
783 | [] => FreeName (s, T, Any) |
765 | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model", |
784 | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model", |
766 [Const x])) all_frees |
785 [Const x])) all_frees |