walther@59957
|
1 |
(* Title: "Specify/i-model.sml"
|
walther@59957
|
2 |
Author: Walther Neuper
|
walther@59957
|
3 |
(c) due to copyright terms
|
walther@59957
|
4 |
*)
|
walther@59957
|
5 |
|
walther@59957
|
6 |
"-----------------------------------------------------------------------------------------------";
|
walther@59957
|
7 |
"table of contents -----------------------------------------------------------------------------";
|
walther@59957
|
8 |
"-----------------------------------------------------------------------------------------------";
|
walther@59957
|
9 |
"----------- investigate fun add_single in I_Model ---------------------------------------------";
|
walther@59957
|
10 |
"-----------------------------------------------------------------------------------------------";
|
walther@59957
|
11 |
"-----------------------------------------------------------------------------------------------";
|
walther@59957
|
12 |
"-----------------------------------------------------------------------------------------------";
|
walther@59957
|
13 |
|
walther@59957
|
14 |
open I_Model;
|
walther@59957
|
15 |
"----------- investigate fun add_single in I_Model -------------------------------------------";
|
walther@59957
|
16 |
"----------- investigate fun add_single in I_Model -------------------------------------------";
|
walther@59957
|
17 |
"----------- investigate fun add_single in I_Model -------------------------------------------";
|
walther@59997
|
18 |
val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
|
walther@59957
|
19 |
"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
|
walther@59957
|
20 |
"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
|
walther@59957
|
21 |
"AbleitungBiegelinie dy"];
|
walther@59957
|
22 |
val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
|
walther@59957
|
23 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)
|
walther@59957
|
24 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)
|
walther@59957
|
25 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "Streckenlast q_0"*)
|
walther@59957
|
26 |
(*[], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
|
walther@59957
|
27 |
|
walther@59957
|
28 |
(*/------------------- begin step into -----------------------------------------------------\*)
|
walther@59957
|
29 |
(*+*)val Add_Given "Streckenlast q_0" = nxt;
|
walther@59957
|
30 |
|
walther@59957
|
31 |
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
|
walther@59957
|
32 |
|
walther@59957
|
33 |
val ("ok", ([], [], _)) = (*case*)
|
walther@59957
|
34 |
Step.by_tactic tac (pt, p) (*of*);
|
walther@59957
|
35 |
"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
|
walther@59957
|
36 |
val Applicable.Yes tac' = (*case*)
|
walther@59957
|
37 |
Step.check tac (pt, p) (*of*);
|
walther@59957
|
38 |
(*if*) Tactic.for_specify' tac' (*then*);
|
walther@59957
|
39 |
|
walther@59957
|
40 |
val ("ok", ([], [], _)) =
|
walther@59957
|
41 |
Step_Specify.by_tactic tac' ptp;
|
walther@59957
|
42 |
"~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
|
walther@59957
|
43 |
|
walther@59957
|
44 |
val ("ok", ([], [], _)) =
|
walther@59990
|
45 |
Specify.by_tactic' "#Given" ct (pt, p);
|
walther@59957
|
46 |
"~~~~~ fun specify_additem , args:"; val (sel, ct, (pt, pos as (p,_(*Frm, Pbl*)))) =
|
walther@59957
|
47 |
("#Given", ct, (pt, p));
|
walther@59992
|
48 |
val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)
|
walther@59957
|
49 |
val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
|
walther@59957
|
50 |
val cpI = if pI = Problem.id_empty then pI' else pI
|
walther@59957
|
51 |
val cmI = if mI = Method.id_empty then mI' else mI
|
walther@59970
|
52 |
val {ppc, where_, prls, ...} = Problem.from_store cpI;
|
walther@59957
|
53 |
|
walther@59957
|
54 |
(*+*)if Model_Pattern.to_string ppc = "[\"" ^
|
walther@59997
|
55 |
"(#Given, (Traegerlaenge, l_l))\", \"" ^
|
walther@59997
|
56 |
"(#Given, (Streckenlast, q_q))\", \"" ^
|
walther@59997
|
57 |
"(#Find, (Biegelinie, b_b))\", \"" ^
|
walther@59957
|
58 |
"(#Relate, (Randbedingungen, r_b))\"]"
|
walther@59957
|
59 |
(*+*)then () else error "INITIAL Model_Pattern CHANGED";
|
walther@59957
|
60 |
(*+*)if O_Model.to_string oris = "[\n" ^
|
walther@59997
|
61 |
"(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
|
walther@59997
|
62 |
"(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
|
walther@59997
|
63 |
"(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
|
walther@59997
|
64 |
"(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
|
walther@59997
|
65 |
"(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
|
walther@59997
|
66 |
"(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
|
walther@59997
|
67 |
"(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
|
walther@59957
|
68 |
(*+*)then () else error "INITIAL O_Model CHANGED";
|
walther@59957
|
69 |
(*+*)if I_Model.to_string ctxt pbl = "[\n" ^
|
walther@59997
|
70 |
"(0 ,[] ,false ,#Given ,Inc Streckenlast ,(??.empty, [])), \n" ^
|
walther@59997
|
71 |
"(0 ,[] ,false ,#Find ,Inc Biegelinie ,(??.empty, [])), \n" ^
|
walther@59997
|
72 |
"(0 ,[] ,false ,#Relate ,Inc Randbedingungen [] ,(??.empty, [])), \n" ^
|
walther@59957
|
73 |
"(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L]))]"
|
walther@59957
|
74 |
(*+*)then () else error "INITIAL I_Model CHANGED";
|
walther@59957
|
75 |
|
walther@59957
|
76 |
val Add (2, [1], true, "#Given", Cor ((Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]),
|
walther@59957
|
77 |
(Free ("q_q", _), [Free ("q_0", _)]))) = (*case*)
|
walther@59958
|
78 |
I_Model.check_single ctxt sel oris pbl ppc ct (*of*);
|
walther@59957
|
79 |
"~~~~~ fun add_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) = (ctxt, sel, oris, pbl, ppc, ct);
|
walther@59957
|
80 |
val SOME t =(*case*) TermC.parseNEW ctxt str (*of*);
|
walther@59957
|
81 |
(** )val ("", (2, [1], "#Given", Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]), [Free ("q_0", _)]) =( **)
|
walther@59957
|
82 |
(**)val ("", ori', all) =(**)
|
walther@59957
|
83 |
(*case*) is_known ctxt m_field o_model t (*of*);
|
walther@59957
|
84 |
|
walther@59957
|
85 |
(*+*)O_Model.single_to_string ori';
|
walther@59957
|
86 |
(*+*)val [Free ("q_0", _)] = all;
|
walther@59957
|
87 |
|
walther@59957
|
88 |
(** )val ("", (2, [1], true, "#Given", Cor ((Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)])))) =( **)
|
walther@59957
|
89 |
(**)val ("", itm) =(**)
|
walther@59957
|
90 |
(*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
|
walther@59957
|
91 |
|
walther@59957
|
92 |
Add itm (*return from add_single*);
|
walther@59957
|
93 |
"~~~~~ from fun add_single \<longrightarrow>fun specify_additem , return:"; val (I_Model.Add itm) = (Add itm);
|
walther@59958
|
94 |
val pbl' = I_Model.add_single thy itm pbl;
|
walther@59957
|
95 |
|
walther@59957
|
96 |
(*+*)if I_Model.to_string ctxt pbl' = "[\n" ^
|
walther@59997
|
97 |
"(0 ,[] ,false ,#Find ,Inc Biegelinie ,(??.empty, [])), \n" ^
|
walther@59997
|
98 |
"(0 ,[] ,false ,#Relate ,Inc Randbedingungen [] ,(??.empty, [])), \n" ^
|
walther@59997
|
99 |
"(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
|
walther@59957
|
100 |
"(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0]))]"
|
walther@59957
|
101 |
(*+*)then () else error "FINAL I_Model CHANGED";
|
walther@59957
|
102 |
|
walther@59957
|
103 |
val (p, pt') =
|
walther@59992
|
104 |
case Specify_Step.add (I_Model.get_tac sel (ct, pbl')) (Istate.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
|
walther@59957
|
105 |
((p, Pbl), _, _, pt') => (p, pt')
|
walther@59965
|
106 |
val pre = Pre_Conds.check' thy prls where_ pbl'
|
walther@59957
|
107 |
val pb = foldl and_ (true, map fst pre)
|
walther@59957
|
108 |
val (p_, _) =
|
walther@59990
|
109 |
Specify.find_next_step' Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
|
walther@59957
|
110 |
|
walther@59965
|
111 |
(*+*)if pre = [] then () else error "FINAL Pre_Conds.check' CHANGED 1";
|
walther@59965
|
112 |
(*+*)if pb = true then () else error "FINAL Pre_Conds.check' CHANGED 1";
|
walther@59957
|
113 |
(*-------------------- stop step into -------------------------------------------------------*)
|
walther@59957
|
114 |
(*\------------------- end step into -------------------------------------------------------/*)
|
walther@59957
|
115 |
|
walther@59957
|
116 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt'''''; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)
|
walther@59957
|
117 |
|
walther@59957
|
118 |
(* final test ...*)
|
walther@59957
|
119 |
if p = ([], Pbl) then
|
walther@59957
|
120 |
case nxt of Add_Relation "Randbedingungen [y 0 = 0]" => () | _ => error "investigate fun add_single CHANGED 1"
|
walther@59957
|
121 |
else error "investigate fun add_single CHANGED 2"
|