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