wneuper@59540
|
1 |
(* biegelinie-3.sml
|
wneuper@59540
|
2 |
author: Walther Neuper 190515
|
wneuper@59540
|
3 |
(c) due to copyright terms
|
wneuper@59540
|
4 |
*)
|
wneuper@59540
|
5 |
"table of contents -----------------------------------------------";
|
wneuper@59540
|
6 |
"-----------------------------------------------------------------";
|
wneuper@59540
|
7 |
"----------- see biegelinie-1.sml---------------------------------";
|
wneuper@59540
|
8 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
|
wneuper@59540
|
9 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
|
wneuper@59540
|
10 |
"-----------------------------------------------------------------";
|
wneuper@59540
|
11 |
"-----------------------------------------------------------------";
|
wneuper@59540
|
12 |
"-----------------------------------------------------------------";
|
wneuper@59540
|
13 |
|
wneuper@59540
|
14 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
|
wneuper@59540
|
15 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
|
wneuper@59540
|
16 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
|
wneuper@59540
|
17 |
"----- Bsp 7.70 with me";
|
wneuper@59540
|
18 |
val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
|
wneuper@59540
|
19 |
"Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
|
wneuper@59540
|
20 |
"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
|
wneuper@59540
|
21 |
"AbleitungBiegelinie dy"];
|
wneuper@59540
|
22 |
val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
|
wneuper@59540
|
23 |
["IntegrierenUndKonstanteBestimmen2"]);
|
wneuper@59540
|
24 |
val p = e_pos'; val c = [];
|
wneuper@59540
|
25 |
(*//----------------------------------vvv CalcTreeTEST ----------------------------------------\\*)
|
wneuper@59540
|
26 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
|
wneuper@59540
|
27 |
|
wneuper@59540
|
28 |
(*+*)val PblObj {probl, meth, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt (fst p);
|
wneuper@59540
|
29 |
(*+*)writeln (oris2str oris); (*[
|
wneuper@59540
|
30 |
(1, ["1"], #Given,Traegerlaenge, ["L"]),
|
wneuper@59540
|
31 |
(2, ["1"], #Given,Streckenlast, ["q_0"]),
|
wneuper@59540
|
32 |
(3, ["1"], #Find,Biegelinie, ["y"]),
|
wneuper@59540
|
33 |
(4, ["1"], #Relate,Randbedingungen, ["[y 0 = 0]","[y L = 0]","[M_b 0 = 0]","[M_b L = 0]"]),
|
wneuper@59540
|
34 |
(5, ["1"], #undef,FunktionsVariable, ["x"]),
|
wneuper@59540
|
35 |
(6, ["1"], #undef,GleichungsVariablen, ["[c]","[c_2]","[c_3]","[c_4]"]),
|
wneuper@59540
|
36 |
(7, ["1"], #undef,AbleitungBiegelinie, ["dy"])]*)
|
wneuper@59540
|
37 |
(*+*)itms2str_ @{context} probl = "[]";
|
wneuper@59540
|
38 |
(*+*)itms2str_ @{context} meth = "[]";
|
wneuper@59540
|
39 |
(*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*)
|
wneuper@59540
|
40 |
|
wneuper@59540
|
41 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
|
wneuper@59540
|
42 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)
|
wneuper@59540
|
43 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)
|
wneuper@59540
|
44 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
|
wneuper@59540
|
45 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
|
wneuper@59540
|
46 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
|
wneuper@59540
|
47 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)
|
wneuper@59540
|
48 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
|
wneuper@59540
|
49 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
|
wneuper@59540
|
50 |
(*----------- 10 -----------*)
|
wneuper@59540
|
51 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
|
wneuper@59540
|
52 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy*)
|
wneuper@59540
|
53 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
|
wneuper@59540
|
54 |
|
wneuper@59540
|
55 |
(*//----------------------------------vvv Apply_Method ["IntegrierenUndKonstanteBestimmen2"----\\*)
|
wneuper@59540
|
56 |
(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Model_Problem*)
|
wneuper@59540
|
57 |
(*AMBIGUITY in creating the environment from formal args. of partial_function "Biegelinie.Biegelinie2Script"
|
wneuper@59540
|
58 |
and the actual args., ie. items of the guard of "["IntegrierenUndKonstanteBestimmen2"]" by "assoc_by_type":
|
wneuper@59540
|
59 |
formal arg. "b" type-matches with several...actual args. "["dy","y"]"
|
wneuper@59540
|
60 |
selected "dy"
|
wneuper@59540
|
61 |
with
|
wneuper@59540
|
62 |
formals: ["l","q","v","b","s","vs","id_abl"]
|
wneuper@59540
|
63 |
actuals: ["L","q_0","x","[c, c_2, c_3, c_4]","dy","y","[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]"]*)
|
wneuper@59540
|
64 |
|
wneuper@59540
|
65 |
"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);
|
wneuper@59540
|
66 |
val (pt''', p''') =
|
wneuper@59540
|
67 |
(*locatetac is here for testing by me; step would suffice in me*)
|
wneuper@59540
|
68 |
case locatetac tac (pt,p) of
|
wneuper@59540
|
69 |
("ok", (_, _, ptp)) => ptp
|
wneuper@59540
|
70 |
;
|
wneuper@59540
|
71 |
(*+*)p = ([], Met);
|
wneuper@59540
|
72 |
(*+*)p''' = ([1], Pbl);
|
wneuper@59540
|
73 |
(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p''');
|
wneuper@59540
|
74 |
(*+*)(*MISSING after locatetac:*)
|
wneuper@59540
|
75 |
(*+*)writeln (oris2str oris); (*[
|
wneuper@59540
|
76 |
(1, ["1"], #Given,Streckenlast, ["q_0"]),
|
wneuper@59540
|
77 |
(2, ["1"], #Given,FunktionsVariable, ["x"]),
|
wneuper@59540
|
78 |
(3, ["1"], #Find,Funktionen, ["funs'''"])]
|
wneuper@59540
|
79 |
MISSING:
|
wneuper@59540
|
80 |
Biegelinie
|
wneuper@59540
|
81 |
AbleitungBiegelinie
|
wneuper@59540
|
82 |
*)
|
wneuper@59540
|
83 |
"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
|
wneuper@59540
|
84 |
val (mI, m) = Solve.mk_tac'_ tac;
|
wneuper@59540
|
85 |
val Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
|
wneuper@59540
|
86 |
(*if*) member op = Solve.specsteps mI = false; (*else*)
|
wneuper@59540
|
87 |
|
wneuper@59540
|
88 |
loc_solve_ (mI,m) ptp;
|
wneuper@59540
|
89 |
"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
|
wneuper@59540
|
90 |
|
wneuper@59540
|
91 |
Solve.solve m (pt, pos);
|
wneuper@59540
|
92 |
"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tac.Apply_Method' (mI, _, _, _)), (pt, (pos as (p, _)))) =
|
wneuper@59540
|
93 |
(m, (pt, pos));
|
wneuper@59540
|
94 |
val {srls, ...} = Specify.get_met mI;
|
wneuper@59540
|
95 |
val itms = case get_obj I pt p of
|
wneuper@59540
|
96 |
PblObj {meth=itms, ...} => itms
|
wneuper@59540
|
97 |
| _ => error "solve Apply_Method: uncovered case get_obj"
|
wneuper@59540
|
98 |
val thy' = get_obj g_domID pt p;
|
wneuper@59540
|
99 |
val thy = Celem.assoc_thy thy';
|
wneuper@59540
|
100 |
val (is, env, ctxt, sc) = case Lucin.init_scrstate thy itms mI of
|
wneuper@59540
|
101 |
(is as Selem.ScrState (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
|
wneuper@59540
|
102 |
| _ => error "solve Apply_Method: uncovered case init_scrstate"
|
wneuper@59540
|
103 |
val ini = Lucin.init_form thy sc env;
|
wneuper@59540
|
104 |
val p = lev_dn p;
|
wneuper@59540
|
105 |
val NONE = (*case*) ini (*of*);
|
wneuper@59540
|
106 |
val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
|
wneuper@59540
|
107 |
val d = Rule.e_rls (*FIXME: get simplifier from domID*);
|
wneuper@59540
|
108 |
val Steps (_, ss as (_, _, pt', p', c') :: _) =
|
wneuper@59540
|
109 |
(*case*) Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*);
|
wneuper@59540
|
110 |
|
wneuper@59540
|
111 |
(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');
|
wneuper@59540
|
112 |
(*+*)(*MISSING after locate_gen:*)
|
wneuper@59540
|
113 |
(*+*)writeln (oris2str oris); (*[
|
wneuper@59540
|
114 |
(1, ["1"], #Given,Streckenlast, ["q_0"]),
|
wneuper@59540
|
115 |
(2, ["1"], #Given,FunktionsVariable, ["x"]),
|
wneuper@59540
|
116 |
(3, ["1"], #Find,Funktionen, ["funs'''"])]
|
wneuper@59540
|
117 |
MISSING:
|
wneuper@59540
|
118 |
Biegelinie
|
wneuper@59540
|
119 |
AbleitungBiegelinie
|
wneuper@59540
|
120 |
*)
|
wneuper@59540
|
121 |
"~~~~~ fun locate_gen , args:"; val ((thy', srls), m, (pt, p),
|
wneuper@59540
|
122 |
(scr as Rule.Prog sc, d), (Selem.ScrState (E,l,a,v,S,b), ctxt)) =
|
wneuper@59540
|
123 |
((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
|
wneuper@59540
|
124 |
val thy = Celem.assoc_thy thy';
|
wneuper@59540
|
125 |
(*if*) l = [] orelse (
|
wneuper@59540
|
126 |
(*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res) = true;(*then*)
|
wneuper@59540
|
127 |
(assy (thy',ctxt,srls,d,Aundef) ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) (body_of sc));
|
wneuper@59540
|
128 |
|
wneuper@59540
|
129 |
"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss:step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
|
wneuper@59540
|
130 |
((thy',ctxt,srls,d,Aundef), ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]), (body_of sc));
|
wneuper@59540
|
131 |
(*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*);
|
wneuper@59540
|
132 |
|
wneuper@59540
|
133 |
"~~~~~ fun assy , args:"; val ((thy',ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss), t) =
|
wneuper@59540
|
134 |
(ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
|
wneuper@59540
|
135 |
val (a', LTool.STac stac) = (*case*) handle_leaf "locate" thy' sr E a v t (*of*);
|
wneuper@59540
|
136 |
(*+*)writeln (term2str stac); (*SubProblem
|
wneuper@59540
|
137 |
(''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
|
wneuper@59540
|
138 |
[''Biegelinien'', ''ausBelastung''])
|
wneuper@59540
|
139 |
[REAL q_0, REAL x, REAL_REAL y, REAL_REAL dy] *)
|
wneuper@59540
|
140 |
val p' =
|
wneuper@59540
|
141 |
case p_ of Frm => p
|
wneuper@59540
|
142 |
| Res => lev_on p
|
wneuper@59540
|
143 |
| _ => error ("assy: call by " ^ pos'2str (p,p_));
|
wneuper@59540
|
144 |
val Ass (m,v') = (*case*) assod pt d m stac (*of*);
|
wneuper@59540
|
145 |
|
wneuper@59540
|
146 |
"~~~~~ fun assod , args:"; val (pt, _, (Tac.Subproblem' ((domID, pblID, _), _, _, _, _, _)),
|
wneuper@59540
|
147 |
(stac as Const ("Script.SubProblem", _) $ (Const ("Product_Type.Pair", _) $
|
wneuper@59540
|
148 |
dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags')) =
|
wneuper@59540
|
149 |
(pt, d, m, stac);
|
wneuper@59540
|
150 |
val dI = HOLogic.dest_string dI';
|
wneuper@59540
|
151 |
val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
|
wneuper@59540
|
152 |
val pI = pI' |> HOLogic.dest_list |> map HOLogic.dest_string;
|
wneuper@59540
|
153 |
val mI = mI' |> HOLogic.dest_list |> map HOLogic.dest_string;
|
wneuper@59540
|
154 |
val ags = TermC.isalist2list ags';
|
wneuper@59540
|
155 |
(*if*) mI = ["no_met"] = false; (*else*)
|
wneuper@59540
|
156 |
(* val (pI, pors, mI) = *)
|
wneuper@59540
|
157 |
(pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
|
wneuper@59540
|
158 |
handle ERROR "actual args do not match formal args"
|
wneuper@59540
|
159 |
=> (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
|
wneuper@59540
|
160 |
"~~~~~ fun match_ags , args:"; val (thy, pbt, ags) = (thy, ((#ppc o Specify.get_pbt) pI), ags);
|
wneuper@59540
|
161 |
(*+*)pbt;
|
wneuper@59540
|
162 |
fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
|
wneuper@59540
|
163 |
val pbt' = filter_out is_copy_named pbt
|
wneuper@59540
|
164 |
val cy = filter is_copy_named pbt
|
wneuper@59540
|
165 |
val oris' = matc thy pbt' ags []
|
wneuper@59540
|
166 |
val cy' = map (cpy_nam pbt' oris') cy
|
wneuper@59540
|
167 |
val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
|
wneuper@59540
|
168 |
|
wneuper@59540
|
169 |
(*+*)val c = [];
|
wneuper@59540
|
170 |
(*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)
|
wneuper@59540
|
171 |
|
wneuper@59540
|
172 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Add_Given "Streckenlast q_0"*)
|
wneuper@59540
|
173 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
|
wneuper@59540
|
174 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Funktionen funs'''"*)
|
wneuper@59540
|
175 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
|
wneuper@59540
|
176 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
|
wneuper@59540
|
177 |
(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Specify_Method ["Biegelinien", "ausBelastung"]*)
|
wneuper@59540
|
178 |
(*----------- 20 -----------*)
|
wneuper@59540
|
179 |
(*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
|
wneuper@59540
|
180 |
(*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*)
|
wneuper@59540
|
181 |
ERROR itms2args: 'Biegelinie' not in itms*)
|
wneuper@59540
|
182 |
|
wneuper@59540
|
183 |
(*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _)
|
wneuper@59540
|
184 |
[REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]
|
wneuper@59540
|
185 |
^^^^^^^^^^^ ..ERROR itms2args: 'Biegelinie' not in itms*)
|
wneuper@59540
|
186 |
(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p''''');
|
wneuper@59540
|
187 |
(*+*)if oris2str oris =
|
wneuper@59540
|
188 |
(*+*) "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]"
|
wneuper@59540
|
189 |
(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed oris";
|
wneuper@59540
|
190 |
writeln (oris2str oris); (*[
|
wneuper@59540
|
191 |
(1, ["1"], #Given,Streckenlast, ["q_0"]),
|
wneuper@59540
|
192 |
(2, ["1"], #Given,FunktionsVariable, ["x"]),
|
wneuper@59540
|
193 |
(3, ["1"], #Find,Funktionen, ["funs'''"])]*)
|
wneuper@59540
|
194 |
(*+*)if itms2str_ @{context} probl = "[\n(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),\n(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),\n(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]"
|
wneuper@59540
|
195 |
(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl";
|
wneuper@59540
|
196 |
writeln (itms2str_ @{context} probl); (*[
|
wneuper@59540
|
197 |
(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
|
wneuper@59540
|
198 |
(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
|
wneuper@59540
|
199 |
(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*)
|
wneuper@59540
|
200 |
(*+*)if itms2str_ @{context} meth = "[]"
|
wneuper@59540
|
201 |
(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth";
|
wneuper@59540
|
202 |
writeln (itms2str_ @{context} meth); (*[]*)
|
wneuper@59540
|
203 |
|
wneuper@59540
|
204 |
"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
|
wneuper@59540
|
205 |
(* val (pt, p) = *)
|
wneuper@59540
|
206 |
(*locatetac is here for testing by me; step would suffice in me*)
|
wneuper@59540
|
207 |
case locatetac tac (pt,p) of
|
wneuper@59540
|
208 |
("ok", (_, _, ptp)) => ptp
|
wneuper@59540
|
209 |
;
|
wneuper@59540
|
210 |
"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
|
wneuper@59540
|
211 |
val (mI, m) = Solve.mk_tac'_ tac;
|
wneuper@59540
|
212 |
val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
|
wneuper@59540
|
213 |
(*if*) member op = Solve.specsteps mI = true; (*then*)
|
wneuper@59540
|
214 |
|
wneuper@59540
|
215 |
(*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)
|
wneuper@59540
|
216 |
"~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp);
|
wneuper@59540
|
217 |
(* val (p, _, f, _, _, pt) =*) Chead.specify m pos [] pt;
|
wneuper@59540
|
218 |
|
wneuper@59540
|
219 |
"~~~~~ fun specify , args:"; val ((Tac.Specify_Method' (mID, _, _)), (pos as (p, _)), _, pt) = (m, pos, [], pt);
|
wneuper@59540
|
220 |
val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
|
wneuper@59540
|
221 |
PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
|
wneuper@59540
|
222 |
(oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
|
wneuper@59540
|
223 |
val {ppc, pre, prls,...} = Specify.get_met mID
|
wneuper@59540
|
224 |
val thy = Celem.assoc_thy dI
|
wneuper@59540
|
225 |
val dI'' = if dI = Rule.e_domID then dI' else dI
|
wneuper@59540
|
226 |
val pI'' = if pI = Celem.e_pblID then pI' else pI
|
wneuper@59540
|
227 |
;
|
wneuper@59540
|
228 |
(*+*)writeln (oris2str oris); (*[
|
wneuper@59540
|
229 |
(1, ["1"], #Given,Streckenlast, ["q_0"]),
|
wneuper@59540
|
230 |
(2, ["1"], #Given,FunktionsVariable, ["x"]),
|
wneuper@59540
|
231 |
(3, ["1"], #Find,Funktionen, ["funs'''"])]*)
|
wneuper@59540
|
232 |
(*+*)writeln (pats2str' ppc);
|
wneuper@59540
|
233 |
(*["(#Given, (Streckenlast, q__q))
|
wneuper@59540
|
234 |
","(#Given, (FunktionsVariable, v_v))
|
wneuper@59540
|
235 |
","(#Given, (Biegelinie, id_fun))
|
wneuper@59540
|
236 |
","(#Given, (AbleitungBiegelinie, id_abl))
|
wneuper@59540
|
237 |
","(#Find, (Funktionen, fun_s))"]*)
|
wneuper@59540
|
238 |
(*+*)writeln (pats2str' ((#ppc o Specify.get_pbt) pI));
|
wneuper@59540
|
239 |
(*["(#Given, (Streckenlast, q_q))
|
wneuper@59540
|
240 |
","(#Given, (FunktionsVariable, v_v))
|
wneuper@59540
|
241 |
","(#Find, (Funktionen, funs'''))"]*)
|
wneuper@59540
|
242 |
val oris = Specify.add_field' thy ppc oris
|
wneuper@59540
|
243 |
val met = if met = [] then pbl else met
|
wneuper@59540
|
244 |
val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
|
wneuper@59540
|
245 |
;
|
wneuper@59540
|
246 |
(*+*)writeln (itms2str_ @{context} itms); (*[
|
wneuper@59540
|
247 |
(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
|
wneuper@59540
|
248 |
(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
|
wneuper@59540
|
249 |
(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *)
|
wneuper@59540
|
250 |
|
wneuper@59540
|
251 |
(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
|
wneuper@59540
|
252 |
val itms =
|
wneuper@59540
|
253 |
if mI' = ["Biegelinien", "ausBelastung"]
|
wneuper@59540
|
254 |
then itms @
|
wneuper@59540
|
255 |
[(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
|
wneuper@59540
|
256 |
[Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
|
wneuper@59540
|
257 |
(Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
|
wneuper@59540
|
258 |
[Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
|
wneuper@59540
|
259 |
(5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
|
wneuper@59540
|
260 |
[Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
|
wneuper@59540
|
261 |
(Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
|
wneuper@59540
|
262 |
[Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
|
wneuper@59540
|
263 |
else itms
|
wneuper@59540
|
264 |
(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
|
wneuper@59540
|
265 |
|
wneuper@59540
|
266 |
val itms' = itms @
|
wneuper@59540
|
267 |
[(4, [1], true, "#Given", Cor ((@{term "Biegelinie"},
|
wneuper@59540
|
268 |
[@{term "y::real \<Rightarrow> real"}]),
|
wneuper@59540
|
269 |
(@{term "id_fun::real \<Rightarrow> real"},
|
wneuper@59540
|
270 |
[@{term "y::real \<Rightarrow> real"}] ))),
|
wneuper@59540
|
271 |
(5, [1], true, "#Given", Cor ((@{term "AbleitungBiegelinie"},
|
wneuper@59540
|
272 |
[@{term "dy::real \<Rightarrow> real"}]),
|
wneuper@59540
|
273 |
(@{term "id_abl::real \<Rightarrow> real"},
|
wneuper@59540
|
274 |
[@{term "dy::real \<Rightarrow> real"}] )))]
|
wneuper@59540
|
275 |
val itms'' = itms @
|
wneuper@59540
|
276 |
[(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
|
wneuper@59540
|
277 |
[Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
|
wneuper@59540
|
278 |
(Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
|
wneuper@59540
|
279 |
[Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
|
wneuper@59540
|
280 |
(5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
|
wneuper@59540
|
281 |
[Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
|
wneuper@59540
|
282 |
(Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
|
wneuper@59540
|
283 |
[Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
|
wneuper@59540
|
284 |
;
|
wneuper@59540
|
285 |
if itms' = itms'' then () else error "itms BUIT BY HAND ARE BROKEN";
|
wneuper@59540
|
286 |
(*//-----------------------------------------^^^ Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
|
wneuper@59540
|
287 |
|
wneuper@59540
|
288 |
val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
|
wneuper@59540
|
289 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
290 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
291 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
292 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
293 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
294 |
(*----------- 30 -----------*)
|
wneuper@59540
|
295 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
296 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
297 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
298 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
299 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
300 |
(*----------- 40 -----------*)
|
wneuper@59540
|
301 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
302 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
303 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
304 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
305 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
306 |
(*----------- 50 -----------*)
|
wneuper@59540
|
307 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
308 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
309 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
310 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
311 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
312 |
(*----------- 60 -----------*)
|
wneuper@59540
|
313 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
314 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
315 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
316 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
317 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
318 |
(*----------- 70 -----------*)
|
wneuper@59540
|
319 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
320 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
321 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
322 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
323 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
324 |
(*----------- 80 -----------*)
|
wneuper@59540
|
325 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
326 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
327 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
328 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
329 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
330 |
(*----------- 90 -----------*)
|
wneuper@59540
|
331 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
332 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
333 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
334 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
335 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
336 |
(*---------- 100 -----------*)
|
wneuper@59540
|
337 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
338 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
339 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
340 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
341 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
342 |
(*---------- 110 -----------*)
|
wneuper@59540
|
343 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
344 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
345 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
346 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
347 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
348 |
(* > ML < changing this to " \ <close> ML \ <open>" line causes:
|
wneuper@59540
|
349 |
exception Size raised (line 169 of "./basis/LibrarySupport.sml")
|
wneuper@59540
|
350 |
|
wneuper@59540
|
351 |
so, until exn can be spotted, the test is commited here and
|
wneuper@59540
|
352 |
not coopied to ~~test/../biegelinie-3.sml*)
|
wneuper@59540
|
353 |
(*---------- 120 -----------*)
|
wneuper@59540
|
354 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
355 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
356 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
357 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
358 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
359 |
(*---------- 130 -----------*)
|
wneuper@59540
|
360 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
361 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
362 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
363 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
364 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
wneuper@59540
|
365 |
|
wneuper@59540
|
366 |
if p = ([3], Pbl)
|
wneuper@59540
|
367 |
then
|
wneuper@59540
|
368 |
case nxt of
|
wneuper@59540
|
369 |
("Add_Given", Add_Given "solveForVars [c_2, c_3, c_4]") =>
|
wneuper@59540
|
370 |
(case f of
|
wneuper@59540
|
371 |
PpcKF
|
wneuper@59540
|
372 |
(Problem [],
|
wneuper@59540
|
373 |
{Find = [Incompl "solution []"], Given =
|
wneuper@59540
|
374 |
[Correct
|
wneuper@59540
|
375 |
"equalities\n [0 = -1 * c_4 / -1,\n 0 =\n (-24 * c_4 * EI + -24 * L * c_3 * EI + 12 * L ^^^ 2 * c_2 +\n 4 * L ^^^ 3 * c +\n -1 * L ^^^ 4 * q_0) /\n (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",
|
wneuper@59540
|
376 |
Incompl "solveForVars [c]"],
|
wneuper@59540
|
377 |
Relate = [], Where = [], With = []}) => ()
|
wneuper@59540
|
378 |
| _ => error "Bsp.7.70 me changed 1")
|
wneuper@59540
|
379 |
| _ => error "Bsp.7.70 me changed 2"
|
wneuper@59540
|
380 |
else error "Bsp.7.70 me changed 3";
|
wneuper@59540
|
381 |
|
wneuper@59540
|
382 |
|
wneuper@59540
|
383 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
|
wneuper@59540
|
384 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
|
wneuper@59540
|
385 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
|
wneuper@59540
|
386 |
(* the error in this test might be independent from introduction of y, dy
|
wneuper@59540
|
387 |
as arguments in IntegrierenUndKonstanteBestimmen2,
|
wneuper@59540
|
388 |
rather due to so far untested use of "auto" *)
|
wneuper@59540
|
389 |
val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
|
wneuper@59540
|
390 |
"Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
|
wneuper@59540
|
391 |
"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
|
wneuper@59540
|
392 |
"AbleitungBiegelinie dy"];
|
wneuper@59540
|
393 |
val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
|
wneuper@59540
|
394 |
["IntegrierenUndKonstanteBestimmen2"]);
|
wneuper@59540
|
395 |
|
wneuper@59540
|
396 |
reset_states ();
|
wneuper@59540
|
397 |
CalcTree [(fmz, (dI',pI',mI'))];
|
wneuper@59540
|
398 |
Iterator 1;
|
wneuper@59540
|
399 |
moveActiveRoot 1;
|
wneuper@59540
|
400 |
|
wneuper@59540
|
401 |
(*[], Met*)autoCalculate 1 CompleteCalcHead;
|
wneuper@59540
|
402 |
(*[1], Pbl*)autoCalculate 1 (Step 1); (* into SubProblem *)
|
wneuper@59540
|
403 |
(*[1], Res*)autoCalculate 1 CompleteSubpbl; (**)
|
wneuper@59540
|
404 |
(*[2], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)
|
wneuper@59540
|
405 |
(*[2], Res*)autoCalculate 1 CompleteSubpbl;
|
wneuper@59540
|
406 |
(*[3], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)
|
wneuper@59540
|
407 |
(*[3], Met*)autoCalculate 1 CompleteCalcHead;
|
wneuper@59540
|
408 |
(*[3, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)
|
wneuper@59540
|
409 |
(*(**)autoCalculate 1 CompleteSubpbl; error in kernel 4: generate1: not impl.for Empty_Tac_*)
|
wneuper@59540
|
410 |
(*[3, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
|
wneuper@59540
|
411 |
(*[3, 2], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
|
wneuper@59540
|
412 |
(*[3, 3], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
|
wneuper@59540
|
413 |
(*[3, 4], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
|
wneuper@59540
|
414 |
(*[3, 5], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
|
wneuper@59540
|
415 |
(*[3, 6], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
|
wneuper@59540
|
416 |
(*[3, 7], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
|
wneuper@59540
|
417 |
(*[3, 8], Pbl*)autoCalculate 1 (Step 1); (* solve SubProblem *)
|
wneuper@59540
|
418 |
(*[3, 8], Met*)autoCalculate 1 CompleteCalcHead;
|
wneuper@59540
|
419 |
(*[3, 8, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)
|
wneuper@59540
|
420 |
(*[3, 8, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
|
wneuper@59540
|
421 |
(*(**)autoCalculate 1 (Step 1);
|
wneuper@59540
|
422 |
*** generate1: not impl.for Empty_Tac_
|
wneuper@59540
|
423 |
val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)
|
wneuper@59540
|
424 |
|
wneuper@59540
|
425 |
val ((pt,_),_) = get_calc 1;
|
wneuper@59540
|
426 |
val ip = get_pos 1 1;
|
wneuper@59540
|
427 |
val (Form f, tac, asms) = pt_extract (pt, ip);
|
wneuper@59540
|
428 |
|
wneuper@59540
|
429 |
if ip = ([3, 8, 1], Res) andalso
|
wneuper@59540
|
430 |
term2str f = "[-1 * c_4 / -1 = 0,\n (6 * c_4 * EI + 6 * L * c_3 * EI + -3 * L ^^^ 2 * c_2 + -1 * L ^^^ 3 * c) /\n (6 * EI) =\n L ^^^ 4 * q_0 / (-24 * EI),\n c_2 = 0, c_2 + L * c = L ^^^ 2 * q_0 / 2]"
|
wneuper@59540
|
431 |
then
|
wneuper@59540
|
432 |
case tac of
|
wneuper@59540
|
433 |
SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()
|
wneuper@59540
|
434 |
| _ => error "ERROR biegel.7.70 changed 1"
|
wneuper@59540
|
435 |
else error "ERROR biegel.7.70 changed 2";
|