equal
deleted
inserted
replaced
1381 in |
1381 in |
1382 make_constants_intr i |
1382 make_constants_intr i |
1383 end; |
1383 end; |
1384 |
1384 |
1385 (* ------------------------------------------------------------------------- *) |
1385 (* ------------------------------------------------------------------------- *) |
1386 (* power: 'power (a, b)' computes a^b, for a>=0, b>=0 *) |
|
1387 (* ------------------------------------------------------------------------- *) |
|
1388 |
|
1389 (* int * int -> int *) |
|
1390 |
|
1391 fun power (a, 0) = 1 |
|
1392 | power (a, 1) = a |
|
1393 | power (a, b) = |
|
1394 let val ab = power(a, b div 2) in |
|
1395 ab * ab * power(a, b mod 2) |
|
1396 end; |
|
1397 |
|
1398 (* ------------------------------------------------------------------------- *) |
|
1399 (* size_of_type: returns the number of elements in a type 'T' (i.e. 'length *) |
1386 (* size_of_type: returns the number of elements in a type 'T' (i.e. 'length *) |
1400 (* (make_constants T)', but implemented more efficiently) *) |
1387 (* (make_constants T)', but implemented more efficiently) *) |
1401 (* ------------------------------------------------------------------------- *) |
1388 (* ------------------------------------------------------------------------- *) |
1402 |
1389 |
1403 (* theory -> model -> Term.typ -> int *) |
1390 (* theory -> model -> Term.typ -> int *) |
1413 fun size_of_type thy model T = |
1400 fun size_of_type thy model T = |
1414 let |
1401 let |
1415 (* returns the number of elements that have the same tree structure as a *) |
1402 (* returns the number of elements that have the same tree structure as a *) |
1416 (* given interpretation *) |
1403 (* given interpretation *) |
1417 fun size_of_intr (Leaf xs) = length xs |
1404 fun size_of_intr (Leaf xs) = length xs |
1418 | size_of_intr (Node xs) = power (size_of_intr (hd xs), length xs) |
1405 | size_of_intr (Node xs) = Integer.pow (length xs) (size_of_intr (hd xs)) |
1419 (* obtain the interpretation for a variable of type 'T' *) |
1406 (* obtain the interpretation for a variable of type 'T' *) |
1420 val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, |
1407 val (i, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, |
1421 bounds=[], wellformed=True} (Free ("dummy", T)) |
1408 bounds=[], wellformed=True} (Free ("dummy", T)) |
1422 in |
1409 in |
1423 size_of_intr i |
1410 size_of_intr i |
2894 fun append m n = |
2881 fun append m n = |
2895 let |
2882 let |
2896 val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m) |
2883 val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m) |
2897 val (len_n, off_n) = the (AList.lookup (op =) lenoff_lists n) |
2884 val (len_n, off_n) = the (AList.lookup (op =) lenoff_lists n) |
2898 val len_elem = len_m + len_n |
2885 val len_elem = len_m + len_n |
2899 val off_elem = off_m * power (size_elem, len_n) + off_n |
2886 val off_elem = off_m * Integer.pow len_n size_elem + off_n |
2900 in |
2887 in |
2901 case AList.lookup op= lenoff'_lists (len_elem, off_elem) of |
2888 case AList.lookup op= lenoff'_lists (len_elem, off_elem) of |
2902 NONE => |
2889 NONE => |
2903 (* undefined *) |
2890 (* undefined *) |
2904 Leaf (replicate size_list False) |
2891 Leaf (replicate size_list False) |