7 structure Argo_Real: sig end = |
7 structure Argo_Real: sig end = |
8 struct |
8 struct |
9 |
9 |
10 (* translating input terms *) |
10 (* translating input terms *) |
11 |
11 |
12 fun trans_type _ \<^typ>\<open>Real.real\<close> tcx = SOME (Argo_Expr.Real, tcx) |
12 fun trans_type _ \<^Type>\<open>real\<close> tcx = SOME (Argo_Expr.Real, tcx) |
13 | trans_type _ _ _ = NONE |
13 | trans_type _ _ _ = NONE |
14 |
14 |
15 fun trans_term f (@{const Groups.uminus_class.uminus (real)} $ t) tcx = |
15 fun trans_term f \<^Const_>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx = |
16 tcx |> f t |>> Argo_Expr.mk_neg |> SOME |
16 tcx |> f t |>> Argo_Expr.mk_neg |> SOME |
17 | trans_term f (@{const Groups.plus_class.plus (real)} $ t1 $ t2) tcx = |
17 | trans_term f \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx = |
18 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_add2 |> SOME |
18 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_add2 |> SOME |
19 | trans_term f (@{const Groups.minus_class.minus (real)} $ t1 $ t2) tcx = |
19 | trans_term f \<^Const_>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx = |
20 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_sub |> SOME |
20 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_sub |> SOME |
21 | trans_term f (@{const Groups.times_class.times (real)} $ t1 $ t2) tcx = |
21 | trans_term f \<^Const_>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx = |
22 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_mul |> SOME |
22 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_mul |> SOME |
23 | trans_term f (@{const Rings.divide_class.divide (real)} $ t1 $ t2) tcx = |
23 | trans_term f \<^Const_>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx = |
24 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_div |> SOME |
24 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_div |> SOME |
25 | trans_term f (@{const Orderings.ord_class.min (real)} $ t1 $ t2) tcx = |
25 | trans_term f \<^Const_>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx = |
26 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_min |> SOME |
26 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_min |> SOME |
27 | trans_term f (@{const Orderings.ord_class.max (real)} $ t1 $ t2) tcx = |
27 | trans_term f \<^Const_>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx = |
28 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_max |> SOME |
28 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_max |> SOME |
29 | trans_term f (@{const Groups.abs_class.abs (real)} $ t) tcx = |
29 | trans_term f \<^Const_>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx = |
30 tcx |> f t |>> Argo_Expr.mk_abs |> SOME |
30 tcx |> f t |>> Argo_Expr.mk_abs |> SOME |
31 | trans_term f (@{const Orderings.ord_class.less (real)} $ t1 $ t2) tcx = |
31 | trans_term f \<^Const_>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx = |
32 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_lt |> SOME |
32 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_lt |> SOME |
33 | trans_term f (@{const Orderings.ord_class.less_eq (real)} $ t1 $ t2) tcx = |
33 | trans_term f \<^Const_>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx = |
34 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_le |> SOME |
34 tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_le |> SOME |
35 | trans_term _ t tcx = |
35 | trans_term _ t tcx = |
36 (case try HOLogic.dest_number t of |
36 (case try HOLogic.dest_number t of |
37 SOME (\<^typ>\<open>Real.real\<close>, n) => SOME (Argo_Expr.mk_num (Rat.of_int n), tcx) |
37 SOME (\<^Type>\<open>real\<close>, n) => SOME (Argo_Expr.mk_num (Rat.of_int n), tcx) |
38 | _ => NONE) |
38 | _ => NONE) |
39 |
39 |
40 |
40 |
41 (* reverse translation *) |
41 (* reverse translation *) |
42 |
42 |
43 fun mk_plus t1 t2 = @{const Groups.plus_class.plus (real)} $ t1 $ t2 |
43 fun mk_plus t1 t2 = \<^Const>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> |
44 fun mk_sum ts = uncurry (fold_rev mk_plus) (split_last ts) |
44 fun mk_sum ts = uncurry (fold_rev mk_plus) (split_last ts) |
45 fun mk_times t1 t2 = @{const Groups.times_class.times (real)} $ t1 $ t2 |
45 fun mk_times t1 t2 = \<^Const>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> |
46 fun mk_divide t1 t2 = @{const Rings.divide_class.divide (real)} $ t1 $ t2 |
46 fun mk_divide t1 t2 = \<^Const>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> |
47 fun mk_le t1 t2 = @{const Orderings.ord_class.less_eq (real)} $ t1 $ t2 |
47 fun mk_le t1 t2 = \<^Const>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> |
48 fun mk_lt t1 t2 = @{const Orderings.ord_class.less (real)} $ t1 $ t2 |
48 fun mk_lt t1 t2 = \<^Const>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> |
49 |
49 |
50 fun mk_real_num i = HOLogic.mk_number \<^typ>\<open>Real.real\<close> i |
50 fun mk_real_num i = HOLogic.mk_number \<^Type>\<open>real\<close> i |
51 |
51 |
52 fun mk_number n = |
52 fun mk_number n = |
53 let val (p, q) = Rat.dest n |
53 let val (p, q) = Rat.dest n |
54 in if q = 1 then mk_real_num p else mk_divide (mk_real_num p) (mk_real_num q) end |
54 in if q = 1 then mk_real_num p else mk_divide (mk_real_num p) (mk_real_num q) end |
55 |
55 |
56 fun term_of _ (Argo_Expr.E (Argo_Expr.Num n, _)) = SOME (mk_number n) |
56 fun term_of _ (Argo_Expr.E (Argo_Expr.Num n, _)) = SOME (mk_number n) |
57 | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = |
57 | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = SOME \<^Const>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close> |
58 SOME (@{const Groups.uminus_class.uminus (real)} $ f e) |
|
59 | term_of f (Argo_Expr.E (Argo_Expr.Add, es)) = SOME (mk_sum (map f es)) |
58 | term_of f (Argo_Expr.E (Argo_Expr.Add, es)) = SOME (mk_sum (map f es)) |
60 | term_of f (Argo_Expr.E (Argo_Expr.Sub, [e1, e2])) = |
59 | term_of f (Argo_Expr.E (Argo_Expr.Sub, [e1, e2])) = |
61 SOME (@{const Groups.minus_class.minus (real)} $ f e1 $ f e2) |
60 SOME \<^Const>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close> |
62 | term_of f (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) = SOME (mk_times (f e1) (f e2)) |
61 | term_of f (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) = SOME (mk_times (f e1) (f e2)) |
63 | term_of f (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) = SOME (mk_divide (f e1) (f e2)) |
62 | term_of f (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) = SOME (mk_divide (f e1) (f e2)) |
64 | term_of f (Argo_Expr.E (Argo_Expr.Min, [e1, e2])) = |
63 | term_of f (Argo_Expr.E (Argo_Expr.Min, [e1, e2])) = |
65 SOME (@{const Orderings.ord_class.min (real)} $ f e1 $ f e2) |
64 SOME \<^Const>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close> |
66 | term_of f (Argo_Expr.E (Argo_Expr.Max, [e1, e2])) = |
65 | term_of f (Argo_Expr.E (Argo_Expr.Max, [e1, e2])) = |
67 SOME (@{const Orderings.ord_class.max (real)} $ f e1 $ f e2) |
66 SOME \<^Const>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close> |
68 | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME (@{const Groups.abs_class.abs (real)} $ f e) |
67 | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME \<^Const>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close> |
69 | term_of f (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (mk_le (f e1) (f e2)) |
68 | term_of f (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (mk_le (f e1) (f e2)) |
70 | term_of f (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (mk_lt (f e1) (f e2)) |
69 | term_of f (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (mk_lt (f e1) (f e2)) |
71 | term_of _ _ = NONE |
70 | term_of _ _ = NONE |
72 |
71 |
73 |
72 |