|
walther@59633
|
1 |
(* Title: ProgLang/program.sml
|
|
walther@59633
|
2 |
Author: Walther Neuper 190922
|
|
walther@59633
|
3 |
(c) due to copyright terms
|
|
walther@59633
|
4 |
*)
|
|
walther@59633
|
5 |
|
|
walther@59633
|
6 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59633
|
7 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59633
|
8 |
"table of contents -----------------------------------------------------------------------------";
|
|
walther@59633
|
9 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59633
|
10 |
"-------- fun get_fun_id -----------------------------------------------------------------------";
|
|
walther@59633
|
11 |
"-------- xxx ------";
|
|
walther@59633
|
12 |
"-------- xxx ------";
|
|
walther@59633
|
13 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59633
|
14 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59633
|
15 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59633
|
16 |
|
|
walther@59633
|
17 |
|
|
walther@59633
|
18 |
"-------- fun get_fun_id -----------------------------------------------------------------------";
|
|
walther@59633
|
19 |
"-------- fun get_fun_id -----------------------------------------------------------------------";
|
|
walther@59633
|
20 |
"-------- fun get_fun_id -----------------------------------------------------------------------";
|
|
walther@59633
|
21 |
(* fun_id is nested into arguments, compare ... *)
|
|
wenzelm@60309
|
22 |
val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
|
|
walther@59633
|
23 |
(((((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) $ _) $ _) =
|
|
walther@59633
|
24 |
Thm.prop_of @{thm biegelinie.simps};
|
|
walther@59633
|
25 |
(* ... to: *)
|
|
wenzelm@60309
|
26 |
val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
|
|
walther@59633
|
27 |
(Const (const_id, const_typ) $ _) $ _) =
|
|
walther@59633
|
28 |
Thm.prop_of @{thm simplify.simps};
|
|
walther@59633
|
29 |
|
|
walther@59633
|
30 |
(* get fun_id out of nesting *)
|
|
wenzelm@60309
|
31 |
val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
|
|
walther@59633
|
32 |
nested $ _) =
|
|
walther@59633
|
33 |
Thm.prop_of @{thm biegelinie.simps};
|
|
walther@60336
|
34 |
val (Const (\<^const_name>\<open>biegelinie\<close>, _) $
|
|
walther@60023
|
35 |
Var (("beam", 0), _) $
|
|
walther@60023
|
36 |
Var (("load", 0), _) $
|
|
walther@60023
|
37 |
Var (("fun_var", 0), _) $
|
|
walther@60023
|
38 |
Var (("id_fun", 0), _) $
|
|
walther@60023
|
39 |
Var (("side_conds", 0), _) $
|
|
walther@59633
|
40 |
Var (("vs", 0), _) $
|
|
walther@60023
|
41 |
Var (("id_der", 0), _)) = nested;
|
|
walther@59633
|
42 |
strip_comb nested;
|
|
walther@59633
|
43 |
(*val it =
|
|
walther@60336
|
44 |
(Const (\<^const_name>\<open>biegelinie\<close>, "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")
|
|
walther@59633
|
45 |
,
|
|
walther@59633
|
46 |
[Var (("l", 0), "real"), Var (("q", 0), "real"), Var (("v", 0), "real"),
|
|
walther@59633
|
47 |
Var (("b", 0), "real \<Rightarrow> real"), Var (("s", 0), "bool list")]):
|
|
walther@59633
|
48 |
term * term list*)
|
|
walther@59633
|
49 |
|
|
walther@59633
|
50 |
case get_fun_id (prep_program @{thm biegelinie.simps}) of
|
|
walther@59633
|
51 |
("Biegelinie.biegelinie", _) => ()
|
|
walther@59633
|
52 |
| _ => error "get_fun_id changed";
|
|
walther@59633
|
53 |
case get_fun_id (prep_program @{thm simplify.simps}) of
|
|
walther@59633
|
54 |
("PolyMinus.simplify", _) => ()
|
|
walther@59633
|
55 |
| _ => error "get_fun_id changed";
|