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