5 |
5 |
6 "-----------------------------------------------------------------------------"; |
6 "-----------------------------------------------------------------------------"; |
7 "-----------------------------------------------------------------------------"; |
7 "-----------------------------------------------------------------------------"; |
8 "table of contents -----------------------------------------------------------"; |
8 "table of contents -----------------------------------------------------------"; |
9 "-----------------------------------------------------------------------------"; |
9 "-----------------------------------------------------------------------------"; |
10 "-------- fun program_to_tyty ------------------------------------------------"; |
10 "-------- fun program_to_input -----------------------------------------------"; |
11 "-------- fun T_from_input ---------------------------------------------------"; |
11 "-------- fun T_from_input ---------------------------------------------------"; |
12 "-------- fun T_from_program -------------------------------------------------"; |
12 "-------- fun T_from_program -------------------------------------------------"; |
13 "-------- fun T_to_strings ---------------------------------------------------"; |
13 "-------- fun T_to_input -----------------------------------------------------"; |
|
14 "-------- fun T_to_string_eqs ------------------------------------------------"; |
|
15 "-------- fun T_from_string_eqs ----------------------------------------------"; |
|
16 "-------- fun input_to_terms -------------------------------------------------"; |
14 "-------- build fun for_bdv --------------------------------------------------"; |
17 "-------- build fun for_bdv --------------------------------------------------"; |
15 "-----------------------------------------------------------------------------"; |
18 "-----------------------------------------------------------------------------"; |
16 "-----------------------------------------------------------------------------"; |
19 "-----------------------------------------------------------------------------"; |
17 |
20 |
18 "-------- fun program_to_tyty ------------------------------------------------"; |
21 "-------- fun program_to_input -----------------------------------------------"; |
19 "-------- fun program_to_tyty ------------------------------------------------"; |
22 "-------- fun program_to_input -----------------------------------------------"; |
20 "-------- fun program_to_tyty ------------------------------------------------"; |
23 "-------- fun program_to_input -----------------------------------------------"; |
21 val subst_prog = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"}; |
24 val subst_prog = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"}; |
22 if Subst.program_to_tyty subst_prog = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then () |
25 if Subst.program_to_input subst_prog = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then () |
23 else error "subst'_to_sube changed"; |
26 else error "program_to_input changed"; |
24 |
27 |
25 "-------- fun T_from_input -----------------------------------------------------"; |
28 "-------- fun T_from_input -----------------------------------------------------"; |
26 "-------- fun T_from_input -----------------------------------------------------"; |
29 "-------- fun T_from_input -----------------------------------------------------"; |
27 "-------- fun T_from_input -----------------------------------------------------"; |
30 "-------- fun T_from_input -----------------------------------------------------"; |
28 case Subst.T_from_input @{theory} ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] of |
31 case Subst.T_from_input @{theory} ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] of |
39 [(Free ("bdv_1", _), Free ("x", _)), |
42 [(Free ("bdv_1", _), Free ("x", _)), |
40 (Free ("bdv_2", _), Free ("y", _)), |
43 (Free ("bdv_2", _), Free ("y", _)), |
41 (Free ("bdv_3", _), Free ("z", _))] => () |
44 (Free ("bdv_3", _), Free ("z", _))] => () |
42 | _ => error "Subst.T_from_program changed"; |
45 | _ => error "Subst.T_from_program changed"; |
43 |
46 |
44 "-------- fun T_to_strings -----------------------------------------------------"; |
47 "-------- fun T_to_input -----------------------------------------------------"; |
45 "-------- fun T_to_strings -----------------------------------------------------"; |
48 "-------- fun T_to_input -----------------------------------------------------"; |
46 "-------- fun T_to_strings -----------------------------------------------------"; |
49 "-------- fun T_to_input -----------------------------------------------------"; |
47 val subst_rew = |
50 val subst_rew = |
48 [(@{term "bdv_1 :: real"}, @{term "x :: real"}), |
51 [(@{term "bdv_1 :: real"}, @{term "x :: real"}), |
49 (@{term "bdv_2 :: real"}, @{term "y :: real"}), |
52 (@{term "bdv_2 :: real"}, @{term "y :: real"}), |
50 (@{term "bdv_3 :: real"}, @{term "z :: real"})]; |
53 (@{term "bdv_3 :: real"}, @{term "z :: real"})]; |
51 if Subst.T_to_strings subst_rew = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"]then () |
54 if Subst.T_to_input subst_rew = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then () |
52 else error "T_to_strings changed"; |
55 else error "T_to_strings changed"; |
|
56 |
|
57 "-------- fun T_to_string_eqs ------------------------------------------------"; |
|
58 "-------- fun T_to_string_eqs ------------------------------------------------"; |
|
59 "-------- fun T_to_string_eqs ------------------------------------------------"; |
|
60 val subst = |
|
61 [(@{term "bdv_1 :: real"}, @{term "x :: real"}), |
|
62 (@{term "bdv_2 :: real"}, @{term "y :: real"}), |
|
63 (@{term "xxx :: real"}, @{term "aaa + (111 :: real)"})]; |
|
64 |
|
65 if Subst.T_to_string_eqs subst = ["bdv_1 = x", "bdv_2 = y", "xxx = aaa + 111"] then () |
|
66 else error "T_to_tyty changed"; |
|
67 |
|
68 "-------- fun T_from_string_eqs ----------------------------------------------"; |
|
69 "-------- fun T_from_string_eqs ----------------------------------------------"; |
|
70 "-------- fun T_from_string_eqs ----------------------------------------------"; |
|
71 val string_eqs = ["bdv_1 = x", "bdv_2 = y", "xxx = aaa + 111"]; |
|
72 |
|
73 case Subst.T_from_string_eqs @{theory} string_eqs of |
|
74 [(Free ("bdv_1", _), Free ("x", _)), |
|
75 (Free ("bdv_2", _), Free ("y", _)), |
|
76 (Free ("xxx", _), Const ("Groups.plus_class.plus", _) $ Free ("aaa", _) $ Free ("111", _))] => () |
|
77 | _ => error ""; |
|
78 |
|
79 "-------- fun input_to_terms -------------------------------------------------"; |
|
80 "-------- fun input_to_terms -------------------------------------------------"; |
|
81 "-------- fun input_to_terms -------------------------------------------------"; |
|
82 Subst.input_to_terms: Subst.input -> term list; |
|
83 val input = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(aaa, bbb + 2)"]; |
|
84 |
|
85 case Subst.input_to_terms input of |
|
86 [Const ("Product_Type.Pair", _) $ |
|
87 (Const ("List.list.Cons", _) $ (Const ("String.char.Char", _) $ |
|
88 Const ("HOL.False", _) $ _ $ _ $ _ $ _ $ _ $ _ $ _) $ _) $ |
|
89 Free ("x", _), |
|
90 _, |
|
91 Const ("Product_Type.Pair", _) $ Free ("aaa", _) $ _] => () |
|
92 | _ => error "input_to_eqs CHANGED"; |
53 |
93 |
54 "-------- build fun for_bdv --------------------------------------------------"; |
94 "-------- build fun for_bdv --------------------------------------------------"; |
55 "-------- build fun for_bdv --------------------------------------------------"; |
95 "-------- build fun for_bdv --------------------------------------------------"; |
56 "-------- build fun for_bdv --------------------------------------------------"; |
96 "-------- build fun for_bdv --------------------------------------------------"; |
57 Subst.program_to_tyty: Subst.program -> string list; |
97 Subst.program_to_input: Subst.program -> string list; |
58 |
98 |
59 val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]; |
99 val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]; |
60 val env = [(str2term "v_v", str2term "x")] : Subst.T; |
100 val env = [(str2term "v_v", str2term "x")] : Subst.T; |
61 |
101 |
62 "~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env); |
102 "~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env); |