|
walther@59633
|
1 |
(* Title: ProgLang/prog_tac.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@59718
|
10 |
"-------- fun eval_leaf -------------------------------------------------------------------";
|
|
walther@59633
|
11 |
"-------- xxx ------";
|
|
walther@59633
|
12 |
"-------- xxx ------";
|
|
walther@59633
|
13 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59633
|
14 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59633
|
15 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59633
|
16 |
|
|
walther@59633
|
17 |
|
|
walther@59718
|
18 |
"-------- fun eval_leaf -------------------------------------------------------------------";
|
|
walther@59718
|
19 |
"-------- fun eval_leaf -------------------------------------------------------------------";
|
|
walther@59718
|
20 |
"-------- fun eval_leaf -------------------------------------------------------------------";
|
|
Walther@60558
|
21 |
val {scr = Prog sc, ...} = MethodC.from_store_PIDE ctxt ["Test", "sqrt-equ-test"];
|
|
walther@59861
|
22 |
case eval_leaf [] NONE TermC.empty sc of
|
|
wenzelm@60309
|
23 |
(Expr (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
|
|
walther@60336
|
24 |
(Const (\<^const_name>\<open>Test.solve_root_equ\<close>, _) $ Free ("e_e", _) $ Free ("v_v", _)) $
|
|
wenzelm@60309
|
25 |
(Const (\<^const_name>\<open>Let\<close>, _) $
|
|
walther@60336
|
26 |
(Const (\<^const_name>\<open>Chain\<close>, _) $
|
|
walther@60336
|
27 |
(Const (\<^const_name>\<open>While\<close>, _) $ _ $
|
|
walther@59633
|
28 |
_ ) $
|
|
walther@59633
|
29 |
(_) $
|
|
walther@59633
|
30 |
Free ("e_e", _)) $
|
|
wenzelm@60309
|
31 |
Abs ("e_e", _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e_e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)) )
|
|
walther@59729
|
32 |
), NONE) => ()
|
|
walther@59861
|
33 |
| _ => error "eval_leaf [] NONE TermC.empty";
|