82 (*use "ProgLang/scrtools.sml" 2002*) |
80 (*use "ProgLang/scrtools.sml" 2002*) |
83 (*use "ProgLang/tools.sml" 2002*) |
81 (*use "ProgLang/tools.sml" 2002*) |
84 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*} |
82 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*} |
85 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} |
83 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} |
86 use "Interpret/mstools.sml" (*empty*) |
84 use "Interpret/mstools.sml" (*empty*) |
87 |
|
88 ML {*print_depth 5; |
|
89 val fmz = ["equality (x+1=(2::real))", (*FIRST OF ALL TESTS*) "solveFor x", "solutions L"]; |
|
90 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"], |
|
91 ["Test","squ-equ-test-subpbl1"]); |
|
92 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
93 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
94 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
95 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
96 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
97 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
98 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
99 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
100 "----- fun me, args:"; val (_,tac) = nxt; |
|
101 "----- fun locatetac, args:"; val ptp as (pt, p) = (pt, p); |
|
102 val (mI,m) = mk_tac'_ tac; |
|
103 val Appl m = applicable_in p pt m; |
|
104 member op = specsteps mI; (*false*) |
|
105 "----- fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp); |
|
106 "----- fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos); |
|
107 val {srls, ...} = get_met mI; |
|
108 val PblObj {meth=itms, ...} = get_obj I pt p; |
|
109 val thy' = get_obj g_domID pt p; |
|
110 val thy = assoc_thy thy'; |
|
111 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI; |
|
112 val ini = init_form thy sc env; (*NONE*) |
|
113 *} |
|
114 ML {* |
|
115 "----- fun init_form, args:"; val (Script sc) = sc; |
|
116 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc); |
|
117 *} |
|
118 ML {* |
|
119 fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a = |
|
120 (writeln "Script.Seq"; |
|
121 case get_t y e1 a of NONE => get_t y e2 a | la => la) |
|
122 | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ = |
|
123 (case get_t y e1 a of NONE => get_t y e2 a | la => la) |
|
124 | get_t y (Const ("Script.Try",_) $ e) a = (writeln "Script.Try 1"; |
|
125 get_t y e a) |
|
126 | get_t y (Const ("Script.Try",_) $ e $ a) _ = (writeln "Script.Try 2"; |
|
127 get_t y e a) |
|
128 | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a |
|
129 | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a |
|
130 | get_t y (Const ("Script.Or",_) $e1 $ e2) a = |
|
131 (case get_t y e1 a of NONE => get_t y e2 a | la => la) |
|
132 | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ = |
|
133 (case get_t y e1 a of NONE => get_t y e2 a | la => la) |
|
134 | get_t y (Const ("Script.While",_) $ c $ e) a = get_t y e a |
|
135 | get_t y (Const ("Script.While",_) $ c $ e $ a) _ = get_t y e a |
|
136 | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a = |
|
137 (case get_t y e1 a of NONE => get_t y e2 a | la => la) |
|
138 (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a = |
|
139 (tracing("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2)); |
|
140 case get_t y e1 a of NONE => get_t y e2 a | la => la) |
|
141 | get_t y (Abs (_,_,e)) a = get_t y e a*) |
|
142 | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a = |
|
143 (writeln "HOL.Let"; |
|
144 get_t y e1 a (*don't go deeper without evaluation !*)) |
|
145 | get_t y (Const ("If",_) $ c $ e1 $ e2) a = NONE |
|
146 (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*) |
|
147 |
|
148 | get_t y (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a |
|
149 | get_t y (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a |
|
150 | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a |
|
151 | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a |
|
152 | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = |
|
153 (writeln "Script.Rewrite'_Set 1"; |
|
154 SOME a) |
|
155 | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a = |
|
156 (writeln "Script.Rewrite'_Set 2"; |
|
157 SOME a) |
|
158 | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a |
|
159 | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a |
|
160 | get_t y (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a |
|
161 | get_t y (Const ("Script.Calculate",_) $ _ ) a = SOME a |
|
162 |
|
163 | get_t y (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a |
|
164 | get_t y (Const ("Script.Substitute",_) $ _ ) a = SOME a |
|
165 |
|
166 | get_t y (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE |
|
167 |
|
168 | get_t y x _ = |
|
169 ((*tracing ("### get_t yac: list-expr "^(term2str x));*) |
|
170 NONE); |
|
171 *} |
|
172 ML {* |
|
173 case get_t thy body e_term of SOME (Free ("e_e", _)) => () |
|
174 | _ => error "script: Const in script (as term) changed"; |
|
175 get_stac thy sc; |
|
176 (*========== inhibit exn 110323 ================================================ |
|
177 print_depth 999; sc; |
|
178 val p = lev_dn p; |
|
179 val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt); |
|
180 val Check_Postcond' (_, (ttt,_)) = m'; |
|
181 term2str ttt; (*is the whole script*) |
|
182 solve m (pt, pos); |
|
183 loc_solve_ (mI,m) ptp; |
|
184 locatetac tac (pt,p); |
|
185 ============ inhibit exn 110loc_solve_ (mI,m) ptp323 ==============================================*) |
|
186 *} |
|
187 use "Interpret/ctree.sml" |
85 use "Interpret/ctree.sml" |
188 use "Interpret/ptyps.sml" (* *) |
86 use "Interpret/ptyps.sml" (* *) |
189 (*use "Interpret/generate.sml" new 2011*) |
87 (*use "Interpret/generate.sml" new 2011*) |
190 use "Interpret/calchead.sml" (* *) |
88 use "Interpret/calchead.sml" (* *) |
191 (*use "Interpret/appl.sml" new 2011*) |
89 (*use "Interpret/appl.sml" new 2011*) |
192 use "Interpret/rewtools.sml" (* *) |
90 use "Interpret/rewtools.sml" (* *) |
193 (*use "Interpret/script.sml" TODO*) |
91 use "Interpret/script.sml" (*TODO*) |
194 (*use "Interpret/solve.sml" TODO*) |
92 (*use "Interpret/solve.sml" TODO*) |
195 (*use "Interpret/inform.sml" TODO*) |
93 (*use "Interpret/inform.sml" TODO*) |
196 use "Interpret/mathengine.sml"(*part.*) |
94 use "Interpret/mathengine.sml"(*part.*) |
197 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*} |
95 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*} |
198 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*} |
96 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*} |