5 10 20 30 40 50 60 70 80 |
5 10 20 30 40 50 60 70 80 |
6 *) |
6 *) |
7 |
7 |
8 theory Test_Some imports Isac begin |
8 theory Test_Some imports Isac begin |
9 |
9 |
10 use"../../../test/Tools/isac/Interpret/mathengine.sml" |
10 use"../../../test/Tools/isac/Interpret/script.sml" |
11 |
11 |
12 ML {* |
12 ML {* |
|
13 "----------- Apply_Method: exception PTREE get_obj: pos = [0] does"; |
|
14 (*WN110922 exception PTREE "get_obj: pos = [0] does not exist"*) |
|
15 val fmz = ["Traegerlaenge L", |
|
16 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)", |
|
17 "Biegelinie y", |
|
18 "RandbedingungenBiegung [y 0 = 0, y L = 0]", |
|
19 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]", |
|
20 "FunktionsVariable x"]; |
|
21 val (dI',pI',mI') = |
|
22 ("Biegelinie",["MomentBestimmte","Biegelinien"], |
|
23 ["IntegrierenUndKonstanteBestimmen"]); |
|
24 val p = e_pos'; val c = []; |
|
25 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
26 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
27 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
28 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
29 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
30 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
31 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
32 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
33 |
|
34 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () |
|
35 | _ => error "script.sml, doesnt find Substitute #2"; |
13 |
36 |
14 *} |
37 *} |
15 ML {* |
38 ML {* |
16 |
39 (* |
|
40 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
41 exception PTREE "get_obj: pos = [0] does not exist" raised (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml") |
|
42 *) |
17 *} |
43 *} |
18 ML {* |
44 ML {* |
|
45 "----------- me method [diff,integration] ---------------"; |
|
46 "----------- me method [diff,integration] ---------------"; |
|
47 "----------- me method [diff,integration] ---------------"; |
|
48 (*exp_CalcInt_No-1.xml*) |
|
49 val p = e_pos'; val c = []; |
|
50 "----- step 0: returns nxt = Model_Problem ---"; |
|
51 val (p,_,f,nxt,_,pt) = |
|
52 CalcTreeTEST |
|
53 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"], |
|
54 ("Integrate", ["integrate","function"], ["diff","integration"]))]; |
|
55 "----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---"; |
|
56 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*) |
|
57 "----- step 2: returns nxt = Add_Given \"integrateBy x\" ---"; |
|
58 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
59 "----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---"; |
|
60 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
61 "----- step 4: returns nxt = Specify_Theory \"Integrate\" ---"; |
|
62 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
63 "----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---"; |
|
64 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
65 "----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---"; |
|
66 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
67 "----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---"; |
|
68 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
69 case nxt of (_, Apply_Method ["diff", "integration"]) => () |
|
70 | _ => error "integrate.sml -- me method [diff,integration] -- spec"; |
|
71 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")"; |
19 |
72 |
|
73 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); |
|
74 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); |
|
75 val (mI,m) = mk_tac'_ tac; |
|
76 val Appl m = applicable_in p pt m; |
|
77 member op = specsteps mI (*false*); |
|
78 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp); |
|
79 "~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) = |
|
80 (m, (pt, pos)); |
|
81 val {srls, ...} = get_met mI; |
|
82 val PblObj {meth=itms, ...} = get_obj I pt p; |
|
83 val thy' = get_obj g_domID pt p; |
|
84 val thy = assoc_thy thy'; |
|
85 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI; |
|
86 val ini = init_form thy sc env; |
|
87 val p = lev_dn p; |
|
88 ini = NONE; (*true*) |
|
89 val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt); |
|
90 val d = e_rls (*FIXME: get simplifier from domID*); |
|
91 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), |
|
92 (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = |
|
93 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt')); |
20 *} |
94 *} |
21 ML {* |
95 ML {* |
22 |
|
23 *} |
96 *} |
24 ML {* |
97 ML {* |
25 |
98 val thy = assoc_thy thy'; |
|
99 l = [] orelse ((*init.in solve..Apply_Method...*) |
|
100 (last_elem o fst) p = 0 andalso snd p = Res); (*true*) |
|
101 "~~~~~ fun assy, args:"; val (ya, (is as (E,l,a,v,S,b),ss), |
|
102 (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) = |
|
103 (((ts,d),Aundef), ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]), body); |
26 *} |
104 *} |
27 ML {* |
105 ML {* |
28 |
106 "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) = |
|
107 (ya, ((E , l@[L,R], a,v,S,b),ss), e); |
29 *} |
108 *} |
30 ML {* |
109 ML {* |
31 |
110 val (a', STac stac) = handle_leaf "locate" thy' sr E a v t |
32 *} |
111 *} |
33 ML {* |
112 ML {* |
34 |
113 assod pt d m stac; |
|
114 print_depth 999; |
35 *} |
115 *} |
36 ML {* |
116 ML {* |
|
117 (* |
|
118 val ctxt = get_ctxt pt (p,p_) |
|
119 exception PTREE "get_obj: pos = [0] does not exist" raised (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml") |
|
120 *) |
|
121 *} |
|
122 ML {* |
|
123 lev_back (p,p_) |
|
124 *} |
|
125 ML {* |
|
126 *} |
|
127 ML {* |
|
128 (* |
|
129 assy ya ((E , l@[L,R], a,v,S,b),ss) e |
|
130 (assy ((ts,d),Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body) |
|
131 locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') |
|
132 solve m (pt, pos); |
|
133 loc_solve_ (mI,m) ptp |
|
134 locatetac tac (pt,p) |
|
135 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
|
136 WAS exception PTREE "get_obj: pos = [0] does not exist" |
|
137 raised (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml") |
|
138 *) |
|
139 |
37 |
140 |
38 *} |
141 *} |
39 ML {* |
142 ML {* |
40 |
143 |
41 *} |
144 *} |