|
1 (* Title: BaseDefinitions/substitution.sml |
|
2 Author: Walther Neuper |
|
3 (c) due to copyright terms |
|
4 *) |
|
5 |
|
6 "-----------------------------------------------------------------------------"; |
|
7 "-----------------------------------------------------------------------------"; |
|
8 "table of contents -----------------------------------------------------------"; |
|
9 "-----------------------------------------------------------------------------"; |
|
10 "-------- fun program_to_tyty ------------------------------------------------"; |
|
11 "-------- fun T_from_input ---------------------------------------------------"; |
|
12 "-------- fun T_from_program -------------------------------------------------"; |
|
13 "-------- fun T_to_strings ---------------------------------------------------"; |
|
14 "-------- build fun for_bdv --------------------------------------------------"; |
|
15 "-----------------------------------------------------------------------------"; |
|
16 "-----------------------------------------------------------------------------"; |
|
17 |
|
18 "-------- fun program_to_tyty ------------------------------------------------"; |
|
19 "-------- fun program_to_tyty ------------------------------------------------"; |
|
20 "-------- fun program_to_tyty ------------------------------------------------"; |
|
21 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 () |
|
23 else error "subst'_to_sube changed"; |
|
24 |
|
25 "-------- fun T_from_input -----------------------------------------------------"; |
|
26 "-------- fun T_from_input -----------------------------------------------------"; |
|
27 "-------- fun T_from_input -----------------------------------------------------"; |
|
28 case Subst.T_from_input @{theory} ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] of |
|
29 [(Free ("bdv_1", _), Free ("x", _)), |
|
30 (Free ("bdv_2", _), Free ("y", _)), |
|
31 (Free ("bdv_3", _), Free ("z", _))] => () |
|
32 | _ => error "T_from_input changed"; |
|
33 |
|
34 "-------- fun T_from_program ------------------------------------------------"; |
|
35 "-------- fun T_from_program ------------------------------------------------"; |
|
36 "-------- fun T_from_program ------------------------------------------------"; |
|
37 val t = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"}; |
|
38 case Subst.T_from_program t of |
|
39 [(Free ("bdv_1", _), Free ("x", _)), |
|
40 (Free ("bdv_2", _), Free ("y", _)), |
|
41 (Free ("bdv_3", _), Free ("z", _))] => () |
|
42 | _ => error "Subst.T_from_program changed"; |
|
43 |
|
44 "-------- fun T_to_strings -----------------------------------------------------"; |
|
45 "-------- fun T_to_strings -----------------------------------------------------"; |
|
46 "-------- fun T_to_strings -----------------------------------------------------"; |
|
47 val subst_rew = |
|
48 [(@{term "bdv_1 :: real"}, @{term "x :: real"}), |
|
49 (@{term "bdv_2 :: real"}, @{term "y :: real"}), |
|
50 (@{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 () |
|
52 else error "T_to_strings changed"; |
|
53 |
|
54 "-------- build fun for_bdv --------------------------------------------------"; |
|
55 "-------- build fun for_bdv --------------------------------------------------"; |
|
56 "-------- build fun for_bdv --------------------------------------------------"; |
|
57 Subst.program_to_tyty: Subst.program -> string list; |
|
58 |
|
59 val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]; |
|
60 val env = [(str2term "v_v", str2term "x")] : Subst.T; |
|
61 |
|
62 "~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env); |
|
63 fun scan (Const _) = NONE |
|
64 | scan (Free _) = NONE |
|
65 | scan (Var _) = NONE |
|
66 | scan (Bound _) = NONE |
|
67 | scan (t as Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ _ $ _) $ _) = |
|
68 if TermC.is_bdv_subst t then SOME t else NONE |
|
69 | scan (Abs (_, _, body)) = scan body |
|
70 | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst |
|
71 |
|
72 val SOME tm = scan prog; |
|
73 val subst = tm |> subst_atomic env; |
|
74 if UnparseC.term tm = "[(''bdv'', v_v)]" then () else error "for_bdv changed 1"; |
|
75 |
|
76 if Subst.program_to_tyty subst = (["(''bdv'', x)"] : Subst.input) then () |
|
77 else error "for_bdv changed 2"; |