walther@59911
|
1 |
(* Title: BaseDefinitions/substitution.sml
|
walther@59911
|
2 |
Author: Walther Neuper
|
walther@59911
|
3 |
(c) due to copyright terms
|
walther@59911
|
4 |
*)
|
walther@59911
|
5 |
|
walther@59911
|
6 |
"-----------------------------------------------------------------------------";
|
walther@59911
|
7 |
"-----------------------------------------------------------------------------";
|
walther@59911
|
8 |
"table of contents -----------------------------------------------------------";
|
walther@59911
|
9 |
"-----------------------------------------------------------------------------";
|
walther@59912
|
10 |
"-------- fun program_to_input -----------------------------------------------";
|
walther@59911
|
11 |
"-------- fun T_from_input ---------------------------------------------------";
|
walther@59911
|
12 |
"-------- fun T_from_program -------------------------------------------------";
|
walther@59912
|
13 |
"-------- fun T_to_input -----------------------------------------------------";
|
walther@59912
|
14 |
"-------- fun T_to_string_eqs ------------------------------------------------";
|
walther@59912
|
15 |
"-------- fun T_from_string_eqs ----------------------------------------------";
|
walther@59912
|
16 |
"-------- fun input_to_terms -------------------------------------------------";
|
walther@59911
|
17 |
"-------- build fun for_bdv --------------------------------------------------";
|
walther@59911
|
18 |
"-----------------------------------------------------------------------------";
|
walther@59911
|
19 |
"-----------------------------------------------------------------------------";
|
walther@59911
|
20 |
|
walther@59912
|
21 |
"-------- fun program_to_input -----------------------------------------------";
|
walther@59912
|
22 |
"-------- fun program_to_input -----------------------------------------------";
|
walther@59912
|
23 |
"-------- fun program_to_input -----------------------------------------------";
|
Walther@60500
|
24 |
val ctxt = Proof_Context.init_global @{theory}
|
walther@59911
|
25 |
val subst_prog = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"};
|
walther@59912
|
26 |
if Subst.program_to_input subst_prog = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then ()
|
walther@59912
|
27 |
else error "program_to_input changed";
|
walther@59911
|
28 |
|
walther@59911
|
29 |
"-------- fun T_from_input -----------------------------------------------------";
|
walther@59911
|
30 |
"-------- fun T_from_input -----------------------------------------------------";
|
walther@59911
|
31 |
"-------- fun T_from_input -----------------------------------------------------";
|
Walther@60500
|
32 |
case Subst.T_from_input ctxt ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] of
|
walther@59911
|
33 |
[(Free ("bdv_1", _), Free ("x", _)),
|
walther@59911
|
34 |
(Free ("bdv_2", _), Free ("y", _)),
|
walther@59911
|
35 |
(Free ("bdv_3", _), Free ("z", _))] => ()
|
walther@59911
|
36 |
| _ => error "T_from_input changed";
|
walther@59911
|
37 |
|
walther@59911
|
38 |
"-------- fun T_from_program ------------------------------------------------";
|
walther@59911
|
39 |
"-------- fun T_from_program ------------------------------------------------";
|
walther@59911
|
40 |
"-------- fun T_from_program ------------------------------------------------";
|
walther@59911
|
41 |
val t = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"};
|
walther@59911
|
42 |
case Subst.T_from_program t of
|
walther@59911
|
43 |
[(Free ("bdv_1", _), Free ("x", _)),
|
walther@59911
|
44 |
(Free ("bdv_2", _), Free ("y", _)),
|
walther@59911
|
45 |
(Free ("bdv_3", _), Free ("z", _))] => ()
|
walther@59911
|
46 |
| _ => error "Subst.T_from_program changed";
|
walther@59911
|
47 |
|
walther@59912
|
48 |
"-------- fun T_to_input -----------------------------------------------------";
|
walther@59912
|
49 |
"-------- fun T_to_input -----------------------------------------------------";
|
walther@59912
|
50 |
"-------- fun T_to_input -----------------------------------------------------";
|
walther@59911
|
51 |
val subst_rew =
|
walther@59911
|
52 |
[(@{term "bdv_1 :: real"}, @{term "x :: real"}),
|
walther@59911
|
53 |
(@{term "bdv_2 :: real"}, @{term "y :: real"}),
|
walther@59911
|
54 |
(@{term "bdv_3 :: real"}, @{term "z :: real"})];
|
walther@59912
|
55 |
if Subst.T_to_input subst_rew = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then ()
|
walther@59911
|
56 |
else error "T_to_strings changed";
|
walther@59911
|
57 |
|
walther@59912
|
58 |
"-------- fun T_to_string_eqs ------------------------------------------------";
|
walther@59912
|
59 |
"-------- fun T_to_string_eqs ------------------------------------------------";
|
walther@59912
|
60 |
"-------- fun T_to_string_eqs ------------------------------------------------";
|
walther@59912
|
61 |
val subst =
|
walther@59912
|
62 |
[(@{term "bdv_1 :: real"}, @{term "x :: real"}),
|
walther@59912
|
63 |
(@{term "bdv_2 :: real"}, @{term "y :: real"}),
|
walther@59912
|
64 |
(@{term "xxx :: real"}, @{term "aaa + (111 :: real)"})];
|
walther@59912
|
65 |
|
walther@59912
|
66 |
if Subst.T_to_string_eqs subst = ["bdv_1 = x", "bdv_2 = y", "xxx = aaa + 111"] then ()
|
walther@59912
|
67 |
else error "T_to_tyty changed";
|
walther@59912
|
68 |
|
walther@59912
|
69 |
"-------- fun T_from_string_eqs ----------------------------------------------";
|
walther@59912
|
70 |
"-------- fun T_from_string_eqs ----------------------------------------------";
|
walther@59912
|
71 |
"-------- fun T_from_string_eqs ----------------------------------------------";
|
walther@59912
|
72 |
val string_eqs = ["bdv_1 = x", "bdv_2 = y", "xxx = aaa + 111"];
|
walther@59912
|
73 |
|
walther@59912
|
74 |
case Subst.T_from_string_eqs @{theory} string_eqs of
|
walther@59912
|
75 |
[(Free ("bdv_1", _), Free ("x", _)),
|
walther@59912
|
76 |
(Free ("bdv_2", _), Free ("y", _)),
|
walther@60317
|
77 |
(Free ("xxx", _),
|
walther@60336
|
78 |
Const (\<^const_name>\<open>plus_class.plus\<close>, _) $ Free ("aaa", _) $
|
walther@60336
|
79 |
(Const (\<^const_name>\<open>numeral\<close>, _) $
|
walther@60336
|
80 |
(Const (\<^const_name>\<open>num.Bit1\<close>, _) $ _ )))] => ()
|
walther@60317
|
81 |
| _ => error "fun T_from_string_eqs";
|
walther@59912
|
82 |
|
walther@59912
|
83 |
"-------- fun input_to_terms -------------------------------------------------";
|
walther@59912
|
84 |
"-------- fun input_to_terms -------------------------------------------------";
|
walther@59912
|
85 |
"-------- fun input_to_terms -------------------------------------------------";
|
walther@59912
|
86 |
Subst.input_to_terms: Subst.input -> term list;
|
walther@59912
|
87 |
val input = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(aaa, bbb + 2)"];
|
walther@59912
|
88 |
|
walther@59912
|
89 |
case Subst.input_to_terms input of
|
wenzelm@60309
|
90 |
[Const (\<^const_name>\<open>Pair\<close>, _) $
|
walther@60336
|
91 |
(Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Char\<close>, _) $
|
wenzelm@60309
|
92 |
Const (\<^const_name>\<open>False\<close>, _) $ _ $ _ $ _ $ _ $ _ $ _ $ _) $ _) $
|
walther@59912
|
93 |
Free ("x", _),
|
walther@59912
|
94 |
_,
|
wenzelm@60309
|
95 |
Const (\<^const_name>\<open>Pair\<close>, _) $ Free ("aaa", _) $ _] => ()
|
walther@59912
|
96 |
| _ => error "input_to_eqs CHANGED";
|
walther@59912
|
97 |
|
walther@59911
|
98 |
"-------- build fun for_bdv --------------------------------------------------";
|
walther@59911
|
99 |
"-------- build fun for_bdv --------------------------------------------------";
|
walther@59911
|
100 |
"-------- build fun for_bdv --------------------------------------------------";
|
walther@59912
|
101 |
Subst.program_to_input: Subst.program -> string list;
|
walther@59911
|
102 |
|
Walther@60559
|
103 |
val {scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"];
|
Walther@60565
|
104 |
val env = [(TermC.parse_test @{context} "v_v", TermC.parse_test @{context} "x")] : Subst.T;
|
walther@59911
|
105 |
|
walther@59911
|
106 |
"~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env);
|
walther@59911
|
107 |
fun scan (Const _) = NONE
|
walther@59911
|
108 |
| scan (Free _) = NONE
|
walther@59911
|
109 |
| scan (Var _) = NONE
|
walther@59911
|
110 |
| scan (Bound _) = NONE
|
wenzelm@60309
|
111 |
| scan (t as Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ _ $ _) $ _) =
|
walther@59911
|
112 |
if TermC.is_bdv_subst t then SOME t else NONE
|
walther@59911
|
113 |
| scan (Abs (_, _, body)) = scan body
|
walther@59911
|
114 |
| scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst
|
walther@59911
|
115 |
|
walther@59911
|
116 |
val SOME tm = scan prog;
|
walther@59911
|
117 |
val subst = tm |> subst_atomic env;
|
walther@59911
|
118 |
if UnparseC.term tm = "[(''bdv'', v_v)]" then () else error "for_bdv changed 1";
|
walther@59911
|
119 |
|
walther@59912
|
120 |
if Subst.program_to_input subst = (["(''bdv'', x)"] : Subst.input) then ()
|
walther@59911
|
121 |
else error "for_bdv changed 2";
|