equal
deleted
inserted
replaced
33 |
33 |
34 fun is_linear [t] = U.is_number t |
34 fun is_linear [t] = U.is_number t |
35 | is_linear [t, u] = U.is_number t orelse U.is_number u |
35 | is_linear [t, u] = U.is_number t orelse U.is_number u |
36 | is_linear _ = false |
36 | is_linear _ = false |
37 |
37 |
38 fun times _ T ts = if is_linear ts then SOME ((("*", 2), T), ts, T) else NONE |
38 fun mk_times ts = Term.list_comb (@{const times (real)}, ts) |
|
39 |
|
40 fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE |
39 | times _ _ _ = NONE |
41 | times _ _ _ = NONE |
40 |
42 |
|
43 fun mk_divide ts = Term.list_comb (@{const divide (real)}, ts) |
|
44 |
41 fun divide _ T (ts as [_, t]) = |
45 fun divide _ T (ts as [_, t]) = |
42 if U.is_number t then SOME ((("/", 2), T), ts, T) else NONE |
46 if U.is_number t then SOME ("/", 2, ts, mk_divide) else NONE |
43 | divide _ _ _ = NONE |
47 | divide _ _ _ = NONE |
44 in |
48 in |
45 |
49 |
46 val setup_builtins = |
50 val setup_builtins = |
47 B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #> |
51 B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #> |