1.1 --- a/src/sml/IsacKnowledge/DiffApp.ML Fri May 09 23:16:32 2003 +0200
1.2 +++ b/src/sml/IsacKnowledge/DiffApp.ML Thu May 15 16:22:52 2003 +0200
1.3 @@ -1,7 +1,7 @@
1.4 (* tools for applications of differetiation
1.5 use"DiffApp.ML";
1.6 use"IsacKnowledge/DiffApp.ML";
1.7 - use"../knowledge/DiffApp.ML";
1.8 + use"../IsacKnowledge/DiffApp.ML";
1.9
1.10
1.11 WN.6.5.03: old decisions in this file partially are being changed
1.12 @@ -73,11 +73,27 @@
1.13 ("#Find" ,["functionEq f_1_"])
1.14 ],
1.15 e_rls, None, []));
1.16 +store_pbt
1.17 + (prep_pbt DiffApp.thy
1.18 + (["by_explicit","make","function"]:pblID,
1.19 + [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
1.20 + ("#Find" ,["functionEq f_1_"])
1.21 + ],
1.22 + e_rls, None, [["DiffApp","make_fun_by_explicit"]]));
1.23 +store_pbt
1.24 + (prep_pbt DiffApp.thy
1.25 + (["by_new_variable","make","function"]:pblID,
1.26 + [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
1.27 + (*WN.12.5.03: precond for distinction still missing*)
1.28 + ("#Find" ,["functionEq f_1_"])
1.29 + ],
1.30 + e_rls, None, [["DiffApp","make_fun_by_new_variable"]]));
1.31
1.32 store_pbt
1.33 (prep_pbt DiffApp.thy
1.34 (["on_interval","maximum_of","function"]:pblID,
1.35 [("#Given" ,["functionEq t_","boundVariable v_","interval itv_"]),
1.36 + (*WN.12.5.03: precond for distinction still missing*)
1.37 ("#Find" ,["maxArgument v_0_"])
1.38 ],
1.39 e_rls, None, []));
1.40 @@ -114,19 +130,19 @@
1.41 ("#Find" ,["valuesFor vs_"]),
1.42 ("#Relate",[])
1.43 ],
1.44 - {rew_ord'="tless_true",rls'=eval_rls,calc=[], srls = e_rls,prls=e_rls,
1.45 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
1.46 asm_rls=[],asm_thm=[]},
1.47 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
1.48 \ (v_::real) (itv_::real set) (err_::bool) = \
1.49 \ (let e_ = (hd o (filterVar m_)) rs_; \
1.50 \ t_ = (if 1 < length_ rs_ \
1.51 - \ then (SubProblem (Reals_,[make,function],[no_met])\
1.52 + \ then (SubProblem (DiffApp_,[make,function],[no_met])\
1.53 \ [real_ m_, real_ v_, bool_list_ rs_])\
1.54 \ else (hd rs_)); \
1.55 - \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
1.56 + \ (mx_::real) = SubProblem (DiffApp_,[on_interval,max_of,function], \
1.57 \ [Isac,maximum_on_interval])\
1.58 \ [bool_ t_, real_ v_, real_set_ itv_]\
1.59 - \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values]) \
1.60 + \ in ((SubProblem (DiffApp_,[find_values,tool],[Isac,find_values]) \
1.61 \ [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_, \
1.62 \ bool_list_ (dropWhile (ident e_) rs_)])::bool list))"
1.63 ));
1.64 @@ -136,7 +152,7 @@
1.65 [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
1.66 ("#Find" ,["functionEq f_1_"])
1.67 ],
1.68 - {rew_ord'="tless_true",rls'=eval_rls,srls = list_rls,prls=e_rls,
1.69 + {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,
1.70 calc=[],asm_rls=[],asm_thm=[]},
1.71 "Script Make_fun_by_new_variable (f_::real) (v_::real) \
1.72 \ (eqs_::bool list) = \
1.73 @@ -147,9 +163,9 @@
1.74 \ v_2 = nth_ 2 vs_; \
1.75 \ e_1 = (hd o (filterVar v_1)) es_; \
1.76 \ e_2 = (hd o (filterVar v_2)) es_; \
1.77 - \ (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
1.78 + \ (s_1::bool list) = (SubProblem (DiffApp_,[univariate,equation],[no_met])\
1.79 \ [bool_ e_1, real_ v_1]);\
1.80 - \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
1.81 + \ (s_2::bool list) = (SubProblem (DiffApp_,[univariate,equation],[no_met])\
1.82 \ [bool_ e_2, real_ v_2])\
1.83 \in Substitute [(v_1, (rhs o hd) s_1),(v_2, (rhs o hd) s_2)] h_)"
1.84 ));
1.85 @@ -167,7 +183,7 @@
1.86 \ e_1 = hd (dropWhile (ident h_) eqs_); \
1.87 \ vs_ = dropWhile (ident f_) (Vars h_); \
1.88 \ v_1 = hd (dropWhile (ident v_) vs_); \
1.89 - \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
1.90 + \ (s_1::bool list)=(SubProblem(DiffApp_,[univariate,equation],[no_met])\
1.91 \ [bool_ e_1, real_ v_1])\
1.92 \ in Substitute [(v_1, (rhs o hd) s_1)] h_)"
1.93 ));
2.1 --- a/src/sml/ME/modspec.sml Fri May 09 23:16:32 2003 +0200
2.2 +++ b/src/sml/ME/modspec.sml Thu May 15 16:22:52 2003 +0200
2.3 @@ -165,16 +165,18 @@
2.4
2.5
2.6
2.7 -(* to an input (d,ts) find the according ori
2.8 - and insert the ts *)
2.9 +(*.to an input (d,ts) find the according ori and insert the ts.*)
2.10 fun seek_oridts thy sel (d,ts) [] =
2.11 - ("'"^(string_of_cterm (compos thy (d,ts)))^
2.12 + ("'"^(string_of_cterm (comp_dts thy (d,ts)))^
2.13 "' not found (typed)", e_ori_:ori, [])
2.14 + (* val (id,vat,sel',d',ts')::oris = ori;
2.15 + val (id,vat,sel',d',ts') = ori;
2.16 + *)
2.17 | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
2.18 if sel = sel' andalso d=d' andalso (ts inter ts') <> []
2.19 then if sel = sel'
2.20 then ("",(id,vat,sel,d, ts inter(*!overlap!*) ts'):ori, ts')
2.21 - else ((string_of_cterm (compos thy(d,ts)))^
2.22 + else ((string_of_cterm (comp_dts thy(d,ts)))^
2.23 " not for "^sel, e_ori_, [])
2.24 else seek_oridts thy sel (d,ts) oris;
2.25
2.26 @@ -386,13 +388,13 @@
2.27 (* val (_,_,fd,d,ts) = hd miss;
2.28 *)
2.29 fun getr_ct thy ((_,_,fd,d,ts):ori) =
2.30 - (fd, (string_of_cterm o (compos thy)) (d,[hd ts]):cterm');
2.31 -(* val t = compos thy (d,[hd ts]);
2.32 + (fd, (string_of_cterm o (comp_dts thy)) (d,[hd ts]):cterm');
2.33 +(* val t = comp_dts thy (d,[hd ts]);
2.34 *)
2.35
2.36 (* get a term from ori, notyet input in itm *)
2.37 fun geti_ct thy ((_,_,_,d,ts):ori) ((_,_,_,fd,itm_):itm) =
2.38 - (fd, (string_of_cterm o (compos thy)) (d,ts \\ (ts_in itm_)):cterm');
2.39 + (fd, (string_of_cterm o (comp_dts thy)) (d,ts \\ (ts_in itm_)):cterm');
2.40 (* test-maximum.sml fmy <> [], Init_Proof ...
2.41 val (_,_,_,d,ts) = ori; val (_,_,_,fd,itm_) = hd icl;
2.42 val d' $ ts' = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
2.43 @@ -403,7 +405,7 @@
2.44 cterm_of (sign_of thy) (d $ (hd ts));
2.45 cterm_of (sign_of thy) (d' $ ts');
2.46
2.47 - compos thy (d,ts);
2.48 + comp_dts thy (d,ts);
2.49 *)
2.50
2.51
2.52 @@ -414,10 +416,6 @@
2.53
2.54 (* select an item in oris, notyet input in itms
2.55 (precondition: in itms are only Cor, Sup, Inc) *)
2.56 -(*
2.57 -> val thy = assoc_thy dI;val itms = pbl;
2.58 - nxt_add thy oris pbt itms;
2.59 - *)
2.60 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
2.61 let
2.62 fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
2.63 @@ -428,12 +426,10 @@
2.64 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
2.65 *)
2.66 (f,(d,_))::itms =>
2.67 - Some (f:string, (string_of_cterm o compos thy) (d,[]):cterm')
2.68 + Some (f:string, (string_of_cterm o comp_dts thy) (d,[]):cterm')
2.69 | _ => None end
2.70
2.71 -(* val thy = assoc_thy dI; val pbt = mpc; val itms = met;
2.72 -
2.73 - val (thy,itms)=(assoc_thy (if dI=e_domID then dI' else dI), pbl);
2.74 +(* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
2.75 *)
2.76 | nxt_add thy oris pbt itms =
2.77 let
2.78 @@ -605,10 +601,10 @@
2.79 fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) =
2.80 (id,vt,cl,sl,Cor (d,ts)):itm
2.81 | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =
2.82 - raise error ("update_itm "^(string_of_cterm (compos thy (d,ts)))^
2.83 + raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
2.84 " not not for Syn (s:cterm')")
2.85 | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) =
2.86 - raise error ("update_itm "^(string_of_cterm (compos thy (d,ts)))^
2.87 + raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
2.88 " not not for Typ (s:cterm')")
2.89 | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =
2.90 (id,vt,cl,sl,Fal (d,ts))
2.91 @@ -683,11 +679,10 @@
2.92 then (((strs2str' o
2.93 map (Sign.string_of_term (sign_of thy))) ts')^
2.94 " already input", e_itm) (*2*)
2.95 - else ("", ori_2itm thy itm_ pid all
2.96 - (i,v,f,d,ts\\ts')) (*3,4*)
2.97 + else ("", ori_2itm thy itm_ pid all (i,v,f,d,ts\\ts')) (*3,4*)
2.98 end
2.99 | None => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
2.100 - pid all (i,v,f,d,ts)) (*1*)
2.101 + pid all (i,v,f,d,ts)) (*1*)
2.102 )
2.103 | None => ("", ori_2itm thy (Sup (d,ts))
2.104 e_term all (i,v,f,d,ts));
2.105 @@ -719,7 +714,7 @@
2.106 fun test_types thy (d,ts) =
2.107 let
2.108 val s = !show_types; val _ = show_types:= true;
2.109 - val opt = (try (compos thy)) (d,ts);
2.110 + val opt = (try (comp_dts thy)) (d,ts);
2.111 val msg = case opt of
2.112 Some _ => ""
2.113 | None => ((Sign.string_of_term (sign_of thy) d)^" "^
2.114 @@ -747,7 +742,7 @@
2.115 val ots = (distinct o flat o (map #5)) (ori:ori list);
2.116 val oids = ((map (fst o dest_Free)) o distinct o
2.117 flat o (map vars)) ots;
2.118 - val (d,ts,pval) = split_dts thy t;
2.119 + val (d,ts(*,pval*)) = split_dts thy t;
2.120 val ids = map (fst o dest_Free)
2.121 ((distinct o (flat o (map vars))) ts);
2.122 in if (ids \\ oids) <> []
2.123 @@ -797,7 +792,7 @@
2.124 *)
2.125 | Some ct =>
2.126 let
2.127 - val (d,ts,pval) = split_dts thy (term_of ct);
2.128 + val (d,ts(*,pval*)) = split_dts thy (term_of ct);
2.129 in if d = e_term
2.130 then Add (i,[],false,sel,Mis (dsc_unknown,hd ts(*24.3.02*)))
2.131
2.132 @@ -811,7 +806,8 @@
2.133 fun eq2 d ((i,_,_,_,itm_):itm) =
2.134 (d = (d_in itm_)) andalso i<>0;
2.135 in case find_first (eq2 d) ppc of
2.136 - None => Add (i,[],true,f, Cor ((d,ts), (id, pval)))
2.137 + None => Add (i,[],true,f, Cor ((d,ts), (id, (*pval*)
2.138 + pbl_ids' thy d ts)))
2.139 | Some (i',_,_,_,itm_) =>
2.140 (* val Some (i',_,_,_,itm_) = find_first (eq2 d) ppc;
2.141 val None = find_first (eq2 d) ppc;
2.142 @@ -819,9 +815,11 @@
2.143 if is_list_dsc d
2.144 then let val ts = ts union (ts_in itm_)
2.145 in Add (if ts_in itm_ = [] then i else i',
2.146 - [],true,f,Cor ((d, ts), (id, pval)))
2.147 + [],true,f,Cor ((d, ts), (id, (*pval*)
2.148 + pbl_ids' thy d ts)))
2.149 end
2.150 - else Add (i',[],true,f,Cor ((d,ts),(id, pval)))
2.151 + else Add (i',[],true,f,Cor ((d,ts),(id, (*pval*)
2.152 + pbl_ids' thy d ts)))
2.153 end
2.154 )
2.155 end
2.156 @@ -874,34 +872,26 @@
2.157 val it = false : bool *)
2.158 fun is_cp (_,(_,t)) = (is_cpy o free2str) t;
2.159
2.160 +(*.split type-wrapper from scr-arg and build part of ori.*)
2.161 fun mtc thy (str, (dsc, _)) (ty $ va) =
2.162 - (cterm_of (sign_of thy) (dsc $ va);
2.163 - Some (([1], str, dsc, [va])(*:ori without leading #*)))
2.164 - handle _ => None;
2.165 + (cterm_of (sign_of thy) (dsc $ va);(*type check*)
2.166 + Some (([1], str, dsc, (*[va]*)
2.167 + split_dts' (dsc, va)))(*:ori without leading #*))
2.168 + handle _ => (writeln("### match_ags: type error d="^(term2str dsc)
2.169 + ^" $ ts="^(term2str va));None);
2.170 (*> val pbt = (#ppc o get_pbt) ["univariate","equation"];
2.171 > val Const ("Script.SubProblem",_) $
2.172 (Const ("Pair",_) $ Free (thy',_) $
2.173 (Const ("Pair",_) $ pblID' $
2.174 (Const ("Pair",_) $ Free (mI1',_) $ Free (mI2',_)))) $
2.175 - ags = (term_of o the o (parse thy))
2.176 - "(SubProblem (SqRoot_,[univariate,equation],\
2.177 - \ (SqRoot_,solve_linear)) [bool_ (x+#1-#2=#0), real_ x])::bool list";
2.178 + ags =
2.179 +str2term"(SubProblem (SqRoot_,[univariate,equation],\
2.180 + \ (SqRoot_,solve_linear)) [bool_ (x+#1-#2=#0), real_ x])::bool list";
2.181 > val ags = isalist2list ags;
2.182 > mtc thy (hd pbt) (hd ags);
2.183 val it = Some ([1],"#Given",Const (#,#),[# $ #]) *)
2.184
2.185 (*copy-named vars must be filtered out*)
2.186 -fun matc thy [] _ oris = oris (*type oris, but without leading # *)
2.187 - | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
2.188 - if (is_cpy o free2str) t then oris
2.189 - else let val opt = mtc thy p a;
2.190 - in case opt of
2.191 - Some ori => matc thy pbt ags (oris @ [ori])
2.192 - | None => raise error ("match "^
2.193 - (Sign.string_of_term (sign_of thy) (d$t))^
2.194 - " doesn't match "^
2.195 - (Sign.string_of_term (sign_of thy) a))
2.196 - end;
2.197 fun matc thy [] _ oris = oris (*type oris, but without leading #1 *)
2.198 | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
2.199 if (is_cpy o free2str) t then oris
2.200 @@ -909,10 +899,8 @@
2.201 in case opt of
2.202 Some ori => ((*writeln("### matc: ori0= "^(ori02str ori));*)
2.203 matc thy pbt ags (oris @ [ori]))
2.204 - | None => raise error ("match: "^
2.205 - (Sign.string_of_term (sign_of thy) (d$t))^
2.206 - " doesn't match "^
2.207 - (Sign.string_of_term (sign_of thy) a))
2.208 + | None => raise error ("match: "^(term2str (d$t))^
2.209 + " doesn't match "^(term2str a))
2.210 end;
2.211 (* run subp-rooteq.sml until Init_Proof before ...
2.212 > val Nd (PblObj {origin=(oris,_),...},_) = pt;(*from test/subp-rooteq.sml*)
2.213 @@ -923,23 +911,32 @@
2.214 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
2.215
2.216
2.217 -(*copy name from an appropriate in problem-type,
2.218 - pbt and oris are 1:1 until cpy-nam at the end*)
2.219 +(*copy name from an appropriate name in problem-type,
2.220 + pbt and oris are 1:1 until cpy-nam at the end WN.13.5.03 ?????????*)
2.221 +(* val (pbt,oris) = (pbt',oris');
2.222 + val (gfr,(dsc,t)) = nth 1 cy;
2.223 + cpy_nam pbt oris (gfr,(dsc,t));
2.224 + *)
2.225 fun cpy_nam pbt oris (gfr,(dsc,t)) =
2.226 - let fun sel (_,_,_,[vl]) = vl;
2.227 - val cy = (implode o drop_last o drop_last o explode o free2str) t;
2.228 + (let fun sel (_,_,d,ts) = comp_ts (d, ts);
2.229 + val cy' = (implode o drop_last o drop_last o explode o free2str) t;
2.230 val ext = (last_elem o drop_last o explode o free2str) t;
2.231 val vars' = map (free2str o snd o snd) pbt;(*cpy-nam filtered_out*)
2.232 val vals = map sel oris;
2.233 - val cy_ext = (free2str o the) (assoc (vars'~~vals, cy))^"_"^ext;
2.234 - in ([1], gfr, dsc, [mk_free (type_of t) cy_ext]) end;
2.235 + val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
2.236 + in ([1], gfr, dsc, [mk_free (type_of t) cy_ext]) end)
2.237 + handle _ => raise error ("cpy_nam: for "^(term2str t));
2.238 (*> val (gfr,(dsc,t)) = last_elem pbt;
2.239 > cpy_nam pbt (drop_last oris) (gfr,(dsc,t));
2.240 val it = ([1],"#Find",
2.241 Const ("Descript.solutions","bool List.list => Tools.toreall"),
2.242 [Free ("x_i","bool List.list")]) *)
2.243
2.244 -(*expects beginning of pbt:ags = 1:1, until cpy-nam in pbt*)
2.245 +
2.246 +(*expects beginning of pbt:ags = 1:1, until cpy-nam in oris appended*)
2.247 +(* val (thy,pbt,ags) = (assoc_thy domID,(#ppc o get_pbt) pblID,
2.248 + isalist2list ags');
2.249 + *)
2.250 fun match_ags thy pbt ags =
2.251 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
2.252 val pbt' = filter_out is_cp pbt;(*cpy-nam are never args of script*)
2.253 @@ -959,10 +956,12 @@
2.254 Const ("Descript.solutions","bool List.list => Tools.toreall"),
2.255 [Free ("x_i","bool List.list")])] : ori list*)
2.256
2.257 -(*@@@
2.258 -> val Nd (PblObj {origin=(oris,_),...},_) = pt;(*from test/subp-rooteq.sml*)
2.259 +(*
2.260 +> val Nd (PblObj {origin=(oris,_),...},_) = pt;
2.261
2.262 *)
2.263 +(* split_
2.264 +make oris from args of SubProblem and pbt -----end------*)
2.265
2.266
2.267
2.268 @@ -1012,7 +1011,7 @@
2.269
2.270
2.271 (* test-printouts ---
2.272 -val _=writeln("### insert_ppc: (d,ts)= "^(string_of_cterm(compos thy(d,ts))));
2.273 +val _=writeln("### insert_ppc: (d,ts)="^(string_of_cterm(comp_dts thy(d,ts))));
2.274 val _=writeln("### insert_ppc: pts= "^
2.275 (strs2str' o map (Sign.string_of_term (sign_of thy))) pts);
2.276
3.1 --- a/src/sml/ME/mstools.sml Fri May 09 23:16:32 2003 +0200
3.2 +++ b/src/sml/ME/mstools.sml Thu May 15 16:22:52 2003 +0200
3.3 @@ -3,6 +3,7 @@
3.4 use"mstools.sml";
3.5 *)
3.6
3.7 +
3.8 val e_listReal = (term_of o the o (parse Script.thy)) "[]::(real list)";
3.9 val e_listBool = (term_of o the o (parse Script.thy)) "[]::(bool list)";
3.10
3.11 @@ -29,81 +30,66 @@
3.12
3.13
3.14
3.15 -
3.16 +(*.revert split_dts only for ts; compare comp_dts.*)
3.17 +fun comp_ts (d, ts) =
3.18 + if is_list_dsc d
3.19 + then if is_list (hd ts)
3.20 + then if is_unl d
3.21 + then (hd ts) (*e.g. someList [1,3,2]*)
3.22 + else (take_apart_inv ts)
3.23 + (* SML[ [a], [b] ]SML --> [a,b] *)
3.24 + else (hd ts) (*a variable or metavariable for a list*)
3.25 + else (hd ts);
3.26 (*.revert split_.*)
3.27 -(*
3.28 -fun compos thy (d,[]) =
3.29 - cterm_of (sign_of thy) (*compos: FIXXME stay with term for efficiency !!!*)
3.30 +fun comp_dts thy (d,[]) =
3.31 + cterm_of (sign_of thy)(*comp_dts:FIXXME stay with term for efficiency !!!*)
3.32 (if is_reall_dsc d then (d $ e_listReal)
3.33 else if is_booll_dsc d then (d $ e_listBool)
3.34 else d)
3.35 - (* val (d,ts) = (d,[hd ts]);
3.36 - *)
3.37 - | compos thy (d,ts) =
3.38 - let val t = if is_list_dsc d andalso not (is_unl d)
3.39 - andalso not (is_metavar (hd ts)) (*..for pbt*)
3.40 - then (list2isalist (type_of (hd ts)) ts)
3.41 - else hd ts;
3.42 - in (cterm_of (sign_of thy) (d $ t))
3.43 - handle _ => raise error ("compos: "^(term2str d)^
3.44 - " $ "^(term2str (hd ts)))
3.45 - end;*)
3.46 -fun compos thy (d,[]) =
3.47 - cterm_of (sign_of thy) (*compos: FIXXME stay with term for efficiency !!!*)
3.48 - (if is_reall_dsc d then (d $ e_listReal)
3.49 - else if is_booll_dsc d then (d $ e_listBool)
3.50 - else d)
3.51 - | compos thy (d,ts) =
3.52 - (cterm_of (sign_of thy) (*compos: FIXXME stay with term for efficiency !!*)
3.53 - (if is_list_dsc d
3.54 - then if is_list (hd ts)
3.55 - then if is_unl d
3.56 - then d $ (hd ts) (*e.g. someList [1,3,2]*)
3.57 - else d $ (take_apart_inv ts)
3.58 - (* SML[ [a], [b] ]SML --> [a,b] *)
3.59 - else d $ (hd ts) (*a variable or metavariable for a list*)
3.60 - else d $ (hd ts)))
3.61 - handle _ => raise error ("compos: "^(term2str d)^
3.62 - " $ "^(term2str (hd ts)));
3.63 + | comp_dts thy (d,ts) =
3.64 + (cterm_of (sign_of thy)(*comp_dts:FIXXME stay with term for efficiency !!*)
3.65 + (d $ (comp_ts (d, ts)))
3.66 + handle _ => raise error ("comp_dts: "^(term2str d)^
3.67 + " $ "^(term2str (hd ts))));
3.68 (*val t = str2term "maximum A";
3.69 -> val (d,ts,_) = split_dts thy t; compos thy (d,ts);
3.70 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
3.71 val it = "maximum A" : cterm
3.72 > val t = str2term "fixedValues [r=Arbfix]";
3.73 -> val (d,ts,_) = split_dts thy t; compos thy (d,ts);
3.74 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
3.75 "fixedValues [r = Arbfix]"
3.76 > val t = str2term "valuesFor [a]";
3.77 -> val (d,ts,_) = split_dts thy t; compos thy (d,ts);
3.78 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
3.79 "valuesFor [a]"
3.80 > val t = str2term "valuesFor [a,b]";
3.81 -> val (d,ts,_) = split_dts thy t; compos thy (d,ts);
3.82 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
3.83 "valuesFor [a, b]"
3.84 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]";
3.85 -> val (d,ts,_) = split_dts thy t; compos thy (d,ts);
3.86 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
3.87 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"
3.88 > val t = str2term "boundVariable a";
3.89 -> val (d,ts,_) = split_dts thy t; compos thy (d,ts);
3.90 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
3.91 "boundVariable a"
3.92 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}";
3.93 -> val (d,ts,_) = split_dts thy t; compos thy (d,ts);
3.94 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
3.95 "interval {x. 0 <= x & x <= 2 * r}"
3.96
3.97 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))";
3.98 -> val (d,ts,_) = split_dts thy t; compos thy (d,ts);
3.99 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
3.100 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
3.101 > val t = str2term "solveFor x";
3.102 -> val (d,ts,_) = split_dts thy t; compos thy (d,ts);
3.103 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
3.104 "solveFor x"
3.105 > val t = str2term "errorBound (eps=0)";
3.106 -> val (d,ts,_) = split_dts thy t; compos thy (d,ts);
3.107 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
3.108 "errorBound (eps = 0)"
3.109 > val t = str2term "solutions L";
3.110 -> val (d,ts,_) = split_dts thy t; compos thy (d,ts);
3.111 +> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
3.112 "solutions L"
3.113
3.114 before 6.5.03:
3.115 > val t = (term_of o the o (parse thy)) "testdscforlist [#1]";
3.116 > val (d,ts) = split_dts t;
3.117 -> compos thy (d,ts);
3.118 +> comp_dts thy (d,ts);
3.119 val it = "testdscforlist [#1]" : cterm
3.120
3.121 > val t = (term_of o the o (parse thy)) "(A::real)";
3.122 @@ -119,16 +105,74 @@
3.123 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
3.124 *)
3.125
3.126 -(*.revert split_dts only for ts; compare compos.*)
3.127 -fun composts (d, ts) =
3.128 - if is_list_dsc d
3.129 - then if is_list (hd ts)
3.130 - then if is_unl d
3.131 - then (hd ts) (*e.g. someList [1,3,2]*)
3.132 - else (take_apart_inv ts)
3.133 - (* SML[ [a], [b] ]SML --> [a,b] *)
3.134 - else (hd ts) (*a variable or metavariable for a list*)
3.135 - else (hd ts);
3.136 +(* this may decompose an object-language isa-list;
3.137 + use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)
3.138 +fun dest_list' t = if is_list t then isalist2list t else [t];
3.139 +
3.140 +(*fun is_metavar (Free (str, _)) =
3.141 + if (last_elem o explode) str = "_" then true else false
3.142 + | is_metavar _ = false;*)
3.143 +fun is_var (Free _) = true
3.144 + | is_var _ = false;
3.145 +
3.146 +(*.special handling for lists. ?WN:14.5.03 ??!?*)
3.147 +fun dest_list (d,ts) =
3.148 + let fun dest t =
3.149 + if is_list_dsc d andalso not (is_unl d)
3.150 + andalso not (is_var t) (*..for pbt*)
3.151 + then isalist2list t else [t]
3.152 + in (flat o (map dest)) ts end;
3.153 +
3.154 +
3.155 +(*.decompose an input into description, terms (ev. elems of lists),
3.156 + and the value for the problem-environment; inv to comp_dts .*)
3.157 +(*WN.8.6.03: corrected with minimal effort,
3.158 +fn : theory -> term ->
3.159 + term * description
3.160 + term list * lists decomposed for elementwise input
3.161 + term list pbl_ids not _HERE_: dont know which list-elems input*)
3.162 +fun split_dts thy (t as d $ arg) =
3.163 + if is_dsc d
3.164 + then if is_list_dsc d
3.165 + then if is_list arg
3.166 + then if is_unl d
3.167 + then (d, [arg]) (*e.g. someList [1,3,2]*)
3.168 + else (d, take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*)
3.169 + else (d, [arg]) (*a variable or metavariable for a list*)
3.170 + else (d, [arg])
3.171 + else (e_term, dest_list' t(*9.01 ???*))
3.172 + | split_dts thy t = (*either dsc or term*)
3.173 + let val (h,argl) = strip_comb t
3.174 + in if (not o is_dsc) h then (e_term, dest_list' t)
3.175 + else (h, dest_list (h,argl))
3.176 + end;
3.177 +(* tests see fun comp_dts
3.178 +
3.179 +> val t = str2term "someList []";
3.180 +> val (_,ts) = split_dts thy t; writeln (terms2str ts);
3.181 +["[]"]
3.182 +> val t = str2term "valuesFor []";
3.183 +> val (_,ts) = split_dts thy t; writeln (terms2str ts);
3.184 +["[]"]*)
3.185 +
3.186 +(*.version returning ts only.*)
3.187 +fun split_dts' (d, arg) =
3.188 + if is_dsc d
3.189 + then if is_list_dsc d
3.190 + then if is_list arg
3.191 + then if is_unl d
3.192 + then ([arg]) (*e.g. someList [1,3,2]*)
3.193 + else (take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*)
3.194 + else ([arg]) (*a variable or metavariable for a list*)
3.195 + else ([arg])
3.196 + else (dest_list' arg(*9.01 ???*))
3.197 + | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
3.198 + let val (h,argl) = strip_comb t
3.199 + in if (not o is_dsc) h then (dest_list' t)
3.200 + else (dest_list (h,argl))
3.201 + end;
3.202 +
3.203 +
3.204
3.205
3.206
3.207 @@ -319,7 +363,7 @@
3.208 fun ori02str (vs,fi,t,ts) =
3.209 "("^((strs2str o (map string_of_int)) vs)^", "^fi^", "^
3.210 (term2str t)^", "^((strs2str o (map term2str)) ts)^")";
3.211 -
3.212 +val oris2str = (strs2str' o (map (linefeed o ori2str)));
3.213
3.214
3.215
3.216 @@ -353,7 +397,7 @@
3.217 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
3.218 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
3.219
3.220 - val (dsc,vl,_) = (split_dts o term_of o the o (parse thy)) "solveFor x";
3.221 + val (dsc,vl) = (split_dts o term_of o the o (parse thy)) "solveFor x";
3.222 val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term
3.223 val vl = Free ("x","RealDef.real") : term
3.224
3.225 @@ -361,7 +405,7 @@
3.226 pbl_ids thy dsc vl;
3.227 val it = [Free ("x","RealDef.real")] : term list
3.228
3.229 - val (dsc,vl,_) = (split_dts o term_of o the o(parse thy))
3.230 + val (dsc,vl) = (split_dts o term_of o the o(parse thy))
3.231 "errorBound (eps=#0)";
3.232 val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_";
3.233 pbl_ids thy dsc vl;
3.234 @@ -388,7 +432,7 @@
3.235 raise error ("pbl_ids': not implemented for "
3.236 ^(terms2str vs));
3.237 (*9.5.03 penv postponed: pbl_ids'*)
3.238 -fun pbl_ids' thy d vs = [composts (d, vs)];
3.239 +fun pbl_ids' thy d vs = [comp_ts (d, vs)];
3.240
3.241
3.242 (*14.9.01: not used after putting values for penv into itm_
4.1 --- a/src/sml/ME/ptyps.sml Fri May 09 23:16:32 2003 +0200
4.2 +++ b/src/sml/ME/ptyps.sml Thu May 15 16:22:52 2003 +0200
4.3 @@ -13,20 +13,14 @@
4.4
4.5 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
4.6
4.7 -(*fun is_metavar (Free (str, _)) =
4.8 - if (last_elem o explode) str = "_" then true else false
4.9 - | is_metavar _ = false;*)
4.10 -fun is_var (Free _) = true
4.11 - | is_var _ = false;
4.12
4.13
4.14
4.15 -
4.16 -fun itm_2item thy (Cor ((d,ts),_))= Correct(string_of_cterm (compos thy(d,ts)))
4.17 +fun itm_2item thy (Cor ((d,ts),_))= Correct(string_of_cterm (comp_dts thy(d,ts)))
4.18 | itm_2item thy (Syn c) = SyntaxE c
4.19 | itm_2item thy (Typ c) = TypeE c
4.20 - | itm_2item thy (Inc ((d,ts),_))= Incompl(string_of_cterm (compos thy(d,ts)))
4.21 - | itm_2item thy (Sup (d,ts)) = Superfl(string_of_cterm (compos thy(d,ts)))
4.22 + | itm_2item thy (Inc ((d,ts),_))= Incompl(string_of_cterm (comp_dts thy(d,ts)))
4.23 + | itm_2item thy (Sup (d,ts)) = Superfl(string_of_cterm (comp_dts thy(d,ts)))
4.24 | itm_2item thy (Mis (d,pid)) =
4.25 Missing (Sign.string_of_term (sign_of thy) d ^" "^
4.26 Sign.string_of_term (sign_of thy) pid);
4.27 @@ -96,17 +90,6 @@
4.28
4.29 (*-----------------------------------------vvv-(3) aus modspec.sml 23.3.02*)
4.30
4.31 -(* this may decompose an object-language isa-list;
4.32 - use only, if description is not available, eg. not input *)
4.33 -fun dest_list' t = if is_list t then isalist2list t else [t];
4.34 -
4.35 -(*.special handling for lists.*)
4.36 -fun dest_list (d,ts) =
4.37 - let fun dest t =
4.38 - if is_list_dsc d andalso not (is_unl d)
4.39 - andalso not (is_var t) (*..for pbt*)
4.40 - then isalist2list t else [t]
4.41 - in (flat o (map dest)) ts end;
4.42
4.43
4.44 (*decompose a problem-type into description and identifier
4.45 @@ -130,64 +113,11 @@
4.46 Free ("vs_","bool List.list")) : term * term*)
4.47
4.48
4.49 -(*
4.50 - val t = (term_of o the o (parse thy)) "x::real";
4.51 - val (hd,argl) = strip_comb t;
4.52 -
4.53 - ((split_dts' thy) o term_of o the o (parse thy)) (hd (tl fmz));
4.54 - split_dts' thy t;
4.55 - *)
4.56 -
4.57 -
4.58 -
4.59 -(*fun split_dts thy (t as (_ $ arg)) =
4.60 - let val (h,argl) = strip_comb t
4.61 - in if (not o is_dsc) h then (e_term, dest_list' t, [t(*9.01 ???*)])
4.62 - else (h, dest_list (h,argl), pbl_ids thy h arg)
4.63 - end
4.64 - | split_dts thy t = (*either dsc or term*)
4.65 - let val (h,argl) = strip_comb t
4.66 - in if (not o is_dsc) h then (e_term, dest_list' t, [t(*9.01 ???*)])
4.67 - else (h, dest_list (h,argl), [t(*9.01 ???*)])
4.68 - end;*)
4.69 -
4.70 -(*. decompose an input into description, terms (ev. elems of lists),
4.71 - and the value for the problem-environment .*)
4.72 -(*WN.8.6.03: corrected with minimal effort,
4.73 -fn : theory -> term ->
4.74 - term * description
4.75 - term list * lists decomposed for elementwise input
4.76 - term list pbl_ids not _HERE_: dont know which list-elems input*)
4.77 -fun split_dts thy (t as d $ arg) =
4.78 - if is_dsc d
4.79 - then if is_list_dsc d
4.80 - then if is_list arg
4.81 - then if is_unl d
4.82 - then (d, [arg],[]) (*e.g. someList [1,3,2]*)
4.83 - else (d, take_apart arg, [])(*[a,b] --> SML[ [a], [b] ]SML*)
4.84 - else (d, [arg],[]) (*a variable or metavariable for a list*)
4.85 - else (d, [arg],[])
4.86 - else (e_term, dest_list' t(*9.01 ???*), [])
4.87 - | split_dts thy t = (*either dsc or term*)
4.88 - let val (h,argl) = strip_comb t
4.89 - in if (not o is_dsc) h then (e_term, dest_list' t, [t(*9.01 ???*)])
4.90 - else (h, dest_list (h,argl), [t(*9.01 ???*)])
4.91 - end;
4.92 -(* tests see fun compos
4.93 -
4.94 -> val t = str2term "someList []";
4.95 -> val (_,ts,_) = split_dts thy t; writeln (terms2str ts);
4.96 -["[]"]
4.97 -> val t = str2term "valuesFor []";
4.98 -> val (_,ts,_) = split_dts thy t; writeln (terms2str ts);
4.99 -["[]"]*)
4.100 -
4.101 -
4.102
4.103 (*. take the first two return-values; for prep_ori .*)
4.104 -fun split_dts' thy t =
4.105 +(*WN.13.5.03fun split_dts' thy t =
4.106 let val (d, ts, _) = split_dts thy t
4.107 - in (d, ts) end;
4.108 + in (d, ts) end;*)
4.109
4.110 (*9.3.00*)
4.111 (* split a term into description and (id | structured variable)
4.112 @@ -201,22 +131,22 @@
4.113
4.114
4.115 (*create output-string for itm_*)
4.116 -fun itm_out thy (Cor ((d,ts),_)) = (string_of_cterm (compos thy(d,ts)))
4.117 +fun itm_out thy (Cor ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts)))
4.118 | itm_out thy (Syn c) = c
4.119 | itm_out thy (Typ c) = c
4.120 - | itm_out thy (Inc ((d,ts),_)) = (string_of_cterm (compos thy(d,ts)))
4.121 - | itm_out thy (Sup (d,ts)) = (string_of_cterm (compos thy(d,ts)))
4.122 + | itm_out thy (Inc ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts)))
4.123 + | itm_out thy (Sup (d,ts)) = (string_of_cterm (comp_dts thy(d,ts)))
4.124 | itm_out thy (Mis (d,pid)) =
4.125 Sign.string_of_term (sign_of thy) d ^" "^
4.126 Sign.string_of_term (sign_of thy) pid;
4.127 (*make string for error-msgs*)
4.128 fun itm__2str thy (Cor ((d,ts), penv)) =
4.129 - "Cor " ^ string_of_cterm (compos thy(d,ts)) ^" ,"^ pen2str thy penv
4.130 + "Cor " ^ string_of_cterm (comp_dts thy(d,ts)) ^" ,"^ pen2str thy penv
4.131 | itm__2str thy (Syn c) = "Syn "^c
4.132 | itm__2str thy (Typ c) = "Typ "^c
4.133 | itm__2str thy (Inc ((d,ts), penv)) =
4.134 - "Inc " ^ string_of_cterm (compos thy(d,ts)) ^" ,"^ pen2str thy penv
4.135 - | itm__2str thy (Sup (d,ts)) = "Sup "^(string_of_cterm (compos thy(d,ts)))
4.136 + "Inc " ^ string_of_cterm (comp_dts thy(d,ts)) ^" ,"^ pen2str thy penv
4.137 + | itm__2str thy (Sup (d,ts)) = "Sup "^(string_of_cterm (comp_dts thy(d,ts)))
4.138 | itm__2str thy (Mis (d,pid))=
4.139 "Mis "^ Sign.string_of_term (sign_of thy) d ^
4.140 " "^ Sign.string_of_term (sign_of thy) pid;
4.141 @@ -248,15 +178,15 @@
4.142 *)
4.143 (*--3.3.00
4.144 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) =
4.145 - Correct (string_of_cterm (compos thy(d,ts)))
4.146 + Correct (string_of_cterm (comp_dts thy(d,ts)))
4.147 | itm2item (_,_,_,_,Syn (c)) = SyntaxE c
4.148 | itm2item (_,_,_,_,Typ (c)) = TypeE c
4.149 | itm2item (_,_,_,_,Fal (d,ts)) =
4.150 - False (string_of_cterm (compos thy(d,ts)))
4.151 + False (string_of_cterm (comp_dts thy(d,ts)))
4.152 | itm2item (_,_,_,_,Inc (d,ts)) =
4.153 - Incompl (string_of_cterm (compos thy(d,ts)))
4.154 + Incompl (string_of_cterm (comp_dts thy(d,ts)))
4.155 | itm2item (_,_,_,_,Sup (d,ts)) =
4.156 - Superfl (string_of_cterm (compos thy(d,ts)));
4.157 + Superfl (string_of_cterm (comp_dts thy(d,ts)));
4.158 *)
4.159
4.160 (* use"ME/modspec.sml";
4.161 @@ -409,7 +339,7 @@
4.162 fun prep_ori [] _ _ = []
4.163 | prep_ori fmz thy pbt =
4.164 let
4.165 - val dts = map ((split_dts' thy) o term_of o the o (parse thy)) fmz;
4.166 + val dts = map ((split_dts thy) o term_of o the o (parse thy)) fmz;
4.167 val ori = map (add_field thy pbt) dts;
4.168 (* val ori = map (flat3 o (pair "#undef")) dts; *)
4.169 val ori' = add_variants ori;
5.1 --- a/src/sml/ME/script.sml Fri May 09 23:16:32 2003 +0200
5.2 +++ b/src/sml/ME/script.sml Thu May 15 16:22:52 2003 +0200
5.3 @@ -104,9 +104,12 @@
5.4 > val des = de_esc_underscore esc;
5.5 val des = de_esc_underscore esc;*)
5.6
5.7 +
5.8 +(*WN.12.5.03 not used any more,
5.9 + tacs are more stable than listepxr: subst_tacexpr
5.10 fun is_listexpr t =
5.11 (((ids_of o head_of) t) inter (!listexpr)) <> [];
5.12 -
5.13 +----*)
5.14
5.15 (*go at a location in a script and fetch the contents*)
5.16 fun go [] t = t
5.17 @@ -203,7 +206,7 @@
5.18 val it = "x + #1 = #2" : string *)
5.19
5.20
5.21 -(*get argument of first tactic in a script for init_form*)
5.22 +(*.get argument of first tactic in a script for init_form.*)
5.23 fun get_tac thy (h $ body) =
5.24 let
5.25 fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a =
5.26 @@ -222,11 +225,14 @@
5.27 | get_t y (Const ("Script.While",_) $ c $ e $ a) _ = get_t y e a
5.28 | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a =
5.29 (case get_t y e1 a of None => get_t y e2 a | la => la)
5.30 + (*| get_t y (Const ("Let",_) $ e1 $ Abs (_,_,e2)) a =
5.31 + (writeln("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2));
5.32 + case get_t y e1 a of None => get_t y e2 a | la => la)
5.33 + | get_t y (Abs (_,_,e)) a = get_t y e a*)
5.34 | get_t y (Const ("Let",_) $ e1 $ Abs (_,_,e2)) a =
5.35 - (case get_t y e1 a of None => get_t y e2 a | la => la)
5.36 - | get_t y (Const ("If",_) $ c $ e1 $ e2) a =
5.37 - (case get_t y e1 a of None => get_t y e2 a | la => la)
5.38 - | get_t y (Abs (_,_,e)) a = get_t y e a
5.39 + get_t y e1 a (*don't go deeper without evaluation !*)
5.40 + | get_t y (Const ("If",_) $ c $ e1 $ e2) a = None
5.41 + (*(case get_t y e1 a of None => get_t y e2 a | la => la)*)
5.42
5.43 | get_t y (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = Some a
5.44 | get_t y (Const ("Script.Rewrite",_) $ _ $ _ ) a = Some a
5.45 @@ -244,12 +250,13 @@
5.46
5.47 | get_t y (Const ("Script.SubProblem",_) $ _ $ _) _ = None
5.48
5.49 - | get_t y x _ = raise error ("get_t yac: not defined for "^
5.50 - (Sign.string_of_term (sign_of y) x))
5.51 + | get_t y x _ =
5.52 + ((*writeln ("### get_t yac: list-expr "^(term2str x));*)
5.53 + None)
5.54 in get_t thy body e_term end;
5.55
5.56 (*FIXME: get 1st tac by next_tac [] instead of ... ?? 29.7.02*)
5.57 -(* val (Script sc,((_,(_,_,env,_,_,_))::_)) = (scr,ets);
5.58 +(* val Script sc = scr;
5.59 *)
5.60 fun init_form thy (Script sc) env =
5.61 (case get_tac thy sc of
5.62 @@ -474,7 +481,7 @@
5.63 handle _ => false;
5.64
5.65
5.66 -(* instantiate a tactic, and ev. attach (curried) argument
5.67 +(*.instantiate a tactic or scriptexpr, and ev. attach (curried) argument
5.68 args:
5.69 E environment
5.70 v current value, is attached to curried tactics
5.71 @@ -485,71 +492,75 @@
5.72 but the 1st tac is
5.73 (a) curried: then (a = Some _), or
5.74 (b) not curried: then the values of the initialization are not used
5.75 -*)
5.76 -fun subst_tac E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))=
5.77 - subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t
5.78 +.*)
5.79 +datatype tacexpr = Tac of term | Expr of term
5.80 +fun rep_tacexpr (Tac t ) = t
5.81 + | rep_tacexpr (Expr t) =
5.82 + raise error ("rep_tacexpr called with t= "^(term2str t));
5.83 +fun subst_tacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))=
5.84 + Tac (subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t)
5.85
5.86 - | subst_tac E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ ))=
5.87 - (case a of Some a' => (subst_atomic E (t $ a'))
5.88 + | subst_tacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ ))=
5.89 + Tac (case a of Some a' => (subst_atomic E (t $ a'))
5.90 | None => ((subst_atomic E t) $ v))
5.91
5.92 - | subst_tac E a v
5.93 + | subst_tacexpr E a v
5.94 (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ _ )) =
5.95 - subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t
5.96 + Tac (subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t)
5.97
5.98 - | subst_tac E a v (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ )) =
5.99 - (case a of Some a' => subst_atomic E (t $ a')
5.100 + | subst_tacexpr E a v (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ))=
5.101 + Tac (case a of Some a' => subst_atomic E (t $ a')
5.102 | None => ((subst_atomic E t) $ v))
5.103
5.104 - | subst_tac E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ _ )) =
5.105 - subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t
5.106 + | subst_tacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ _ )) =
5.107 + Tac (subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t)
5.108
5.109 - | subst_tac E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ )) =
5.110 - (case a of Some a' => subst_atomic E (t $ a')
5.111 + | subst_tacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ )) =
5.112 + Tac (case a of Some a' => subst_atomic E (t $ a')
5.113 | None => ((subst_atomic E t) $ v))
5.114
5.115 - | subst_tac E a v
5.116 + | subst_tacexpr E a v
5.117 (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ _ )) =
5.118 - subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t
5.119 + Tac (subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t)
5.120
5.121 - | subst_tac E a v
5.122 + | subst_tacexpr E a v
5.123 (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )) =
5.124 - (case a of Some a' => subst_atomic E (t $ a')
5.125 + Tac (case a of Some a' => subst_atomic E (t $ a')
5.126 | None => ((subst_atomic E t) $ v))
5.127
5.128 - | subst_tac E a v (t as (Const ("Script.Calculate",_) $ _ $ _ )) =
5.129 - subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t
5.130 + | subst_tacexpr E a v (t as (Const ("Script.Calculate",_) $ _ $ _ )) =
5.131 + Tac (subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t)
5.132
5.133 - | subst_tac E a v (t as (Const ("Script.Calculate",_) $ _ )) =
5.134 - (case a of Some a' => subst_atomic E (t $ a')
5.135 + | subst_tacexpr E a v (t as (Const ("Script.Calculate",_) $ _ )) =
5.136 + Tac (case a of Some a' => subst_atomic E (t $ a')
5.137 | None => ((subst_atomic E t) $ v))
5.138
5.139 - | subst_tac E a v
5.140 + | subst_tacexpr E a v
5.141 (t as (Const("Script.Check'_elementwise",_) $ _ $ _ )) =
5.142 - subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t
5.143 + Tac (subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t)
5.144 (* val t = (term_of o the o (parseold Isac.thy))
5.145 "Check_elementwise L_ {v_. Assumptions}";
5.146 val tactac = subst_atomic E t;
5.147 atomt tactac;
5.148 *)
5.149
5.150 - | subst_tac E a v (t as (Const("Script.Check'_elementwise",_) $ _ )) =
5.151 - (case a of Some a' => subst_atomic E (t $ a')
5.152 - | None => ((subst_atomic E t) $ v))
5.153 + | subst_tacexpr E a v (t as (Const("Script.Check'_elementwise",_) $ _ )) =
5.154 + Tac (case a of Some a' => subst_atomic E (t $ a')
5.155 + | None => ((subst_atomic E t) $ v))
5.156
5.157 - | subst_tac E a v (t as (Const("Script.Or'_to'_List",_) $ _ )) = t
5.158 + | subst_tacexpr E a v (t as (Const("Script.Or'_to'_List",_) $ _ )) = Tac t
5.159
5.160 - | subst_tac E a v (t as (Const("Script.Or'_to'_List",_))) = (*t $ v*)
5.161 - (case a of Some a' => subst_atomic E (t $ a')
5.162 - | None => ((subst_atomic E t) $ v))
5.163 + | subst_tacexpr E a v (t as (Const("Script.Or'_to'_List",_))) = (*t $ v*)
5.164 + Tac (case a of Some a' => subst_atomic E (t $ a')
5.165 + | None => ((subst_atomic E t) $ v))
5.166
5.167 - | subst_tac E a v (t as (Const ("Script.SubProblem",_) $ _ $ _)) =
5.168 - subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t
5.169 + | subst_tacexpr E a v (t as (Const ("Script.SubProblem",_) $ _ $ _)) =
5.170 + Tac (subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t)
5.171
5.172 - | subst_tac _ _ _ t = raise error
5.173 - ("subst_tac TODO: no match for "^(term2str t));
5.174 + | subst_tacexpr E a v t =
5.175 + Expr (subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t);
5.176 (*> val t = str2term "SubProblem(Test_, [linear, univariate, equation, test], [Test, solve_linear]) [bool_ e_, real_ v_]";
5.177 -> subst_tac [] None e_term t;*)
5.178 +> subst_tacexpr [] None e_term t;*)
5.179
5.180
5.181 (*start_at: go to the end of executed tactics; this is
5.182 @@ -601,7 +612,8 @@
5.183 (scan ts e1) @ (scan ts e2)
5.184 | scan ts (Const ("Script.Seq",_) $e1 $ e2) =
5.185 (scan ts e1) @ (scan ts e2)
5.186 - | scan ts t = if is_listexpr t then [] else [t];
5.187 + | scan ts t = case subst_tacexpr [] None e_term t of
5.188 + Tac _ => [t] | Expr _ => []
5.189 in (distinct o (scan [])) body end;
5.190 (*sc = Solve_root_equation ...
5.191 > val ts = tacpbls sc;
5.192 @@ -615,9 +627,10 @@
5.193 *)
5.194
5.195
5.196 -(*get the tactics and problems of a script as msteps
5.197 +(*.get the tactics and problems of a script as msteps
5.198 instantiated with the current environment;
5.199 - l is the location which generated the given formula *)
5.200 + l is the location which generated the given formula.*)
5.201 +(*WN.12.5.03: quick-and-dirty repair for listexpressions*)
5.202 fun is_spec_pos Pbl = true
5.203 | is_spec_pos Met = true
5.204 | is_spec_pos _ = false;
5.205 @@ -633,12 +646,13 @@
5.206 else metID;
5.207 val Script sc = (#scr o get_met) metID';
5.208 val ScrState (env,_,_,_,_,_) = get_istate pt (p,p_);
5.209 - in map ((tac2mstep thy) o (subst_tac env None e_term)) (tacpbls sc) end;
5.210 + in map ((tac2mstep thy) o rep_tacexpr o
5.211 + (subst_tacexpr env None e_term)) (tacpbls sc) end;
5.212 (*
5.213 > val Script sc = (#scr o get_met) ("SqRoot.thy","sqrt-equ-test");
5.214 > val env = [((term_of o the o (parse Isac.thy)) "bdv",
5.215 (term_of o the o (parse Isac.thy)) "x")];
5.216 -> map ((tac2mstep thy) o (subst_tac env None e_term)) (tacpbls sc);
5.217 +> map ((tac2mstep thy) o (subst_tacexpr env None e_term)) (tacpbls sc);
5.218 *)
5.219
5.220
5.221 @@ -719,7 +733,7 @@
5.222 term (*for itr_arg,result in ets*)
5.223 | NotAss;
5.224
5.225 -(*assod: mstep' associated with tac w.r.t. d
5.226 +(*.assod: mstep' associated with tac w.r.t. d
5.227 returns
5.228 Ass : associated: e.g. thmID in tac = thmID in m
5.229 +++ arg in tac = arg in m
5.230 @@ -727,7 +741,7 @@
5.231 NotAss : e.g. thmID in tac/=/thmID in m (not =)
5.232 8.01:
5.233 mstep' SubProblem with args completed from script
5.234 -*)
5.235 +.*)
5.236 fun assod d (m as Rewrite_Inst' (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))
5.237 (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $ b $ f_) =
5.238 if thmID = thmID_ then
5.239 @@ -796,30 +810,24 @@
5.240 if id = id' then Ass (m, ((term_of o the o (parse thy)) f'))
5.241 else NotAss
5.242
5.243 -(*
5.244 -val str2term = (term_of o the o (parse Script.thy));
5.245 -val t = str2term
5.246 - "SubProblem (Reals_,[univar,equation],[no_met]) [bool_ e_, real_ v_]";
5.247 -val Const
5.248 - ("Script.SubProblem",_) $
5.249 - (Const
5.250 - ("Pair",_) $
5.251 - Free (dI',_) $
5.252 - (Const
5.253 - ("Pair",_) $ pI' $ mI')) $ ags' = t;*)
5.254
5.255 -(*| assod _ (Subproblem' ((domID,pblID,metID),_,f))
5.256 - (Const ("Script.SubProblem",_) $
5.257 - (Const ("Pair",_) $ Free (dI',_) $
5.258 - (Const ("Pair",_) $ pI' $
5.259 - (Const ("Pair",_) $ Free (mI1',_) $
5.260 - Free (mI2',_)))) $ ags') =*)
5.261 +(* val t = str2term
5.262 + "SubProblem (DiffApp_,[make,function],[no_met]) \
5.263 + \[real_ m_, real_ v_, bool_list_ rs_]";
5.264 +
5.265 + val (Subproblem' ((domID,pblID,metID),_,f)) = m;
5.266 + val (Const ("Script.SubProblem",_) $
5.267 + (Const ("Pair",_) $
5.268 + Free (dI',_) $
5.269 + (Const ("Pair",_) $ pI' $ mI')) $ ags') = tac;
5.270 + *)
5.271 | assod _ (Subproblem' ((domID,pblID,metID),_,f))
5.272 (Const ("Script.SubProblem",_) $
5.273 (Const ("Pair",_) $
5.274 - Free (dI',_) $
5.275 + Free (dI',_) $
5.276 (Const ("Pair",_) $ pI' $ mI')) $ ags') =
5.277 - let val domID' = ((implode o drop_last o explode) dI')^".thy";
5.278 + let val _= writeln "### assod Subproblem";
5.279 + val domID' = ((implode o drop_last o explode) dI')^".thy";
5.280 val pblID' = ((map (de_esc_underscore o free2str))
5.281 o isalist2list) pI';
5.282 val metID' = ((map (de_esc_underscore o free2str))
5.283 @@ -827,8 +835,10 @@
5.284 (*val metID' as (dI',_) = (((implode o drop_last o explode) mI1')^".thy",
5.285 de_esc_underscore mI2');*)
5.286 (*5.8.02: really take domID for metID ?*)
5.287 + val _= writeln "### assod: vor match_ags";
5.288 val oris = match_ags (assoc_thy domID) ((#ppc o get_pbt) pblID)
5.289 (isalist2list ags');
5.290 + val _= writeln "### assod: nach match_ags";
5.291 in
5.292 (*writeln("##### assoc: metID' = "^(metID2str metID'));*)
5.293 if domID = domID' andalso pblID = pblID'
5.294 @@ -1164,15 +1174,28 @@
5.295 | ay => (ay))
5.296 (* val ((m,_,pt,(p,p_),c)::ss) = [(m,EmptyMout,pt,p,[])];
5.297 val t = (term_of o the o (parse Isac.thy)) "Rewrite rmult_1 False";
5.298 +
5.299 + val (ap,(p,p_),c,ss) = (Aundef,p,[],[]);
5.300 + assy (((thy',srls),d),ap) ((E,l,a,v,S,b), (m,EmptyMout,pt,(p,p_),c)::ss) t;
5.301 *)
5.302
5.303 - | assy (((thy',srls),d),ap) ((E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
5.304 - if is_listexpr t
5.305 - then (writeln"### assy: code listexpr missing"; NasNap (v, E))
5.306 - else let val p' = case p_ of Frm => p | Res => lev_on p
5.307 - | _ => raise error ("assy: call by "^(pos'2str (p,p_)));
5.308 - val tac = subst_tac E a v t;
5.309 - in case assod d m tac of
5.310 + | assy (((thy',sr),d),ap) ((E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
5.311 + case subst_tacexpr E a v t of
5.312 + Expr s =>
5.313 + (writeln("### assy: listexpr t= "^(term2str t));
5.314 + writeln("### assy, E= "^(env2str E));
5.315 + writeln("### assy, eval(..)= "^(term2str
5.316 + (eval_listexpr_ (assoc_thy thy') sr
5.317 + (subst_atomic (upd_env_opt E (a,v)) t))));
5.318 + NasNap (eval_listexpr_ (assoc_thy thy') sr
5.319 + (subst_atomic (upd_env_opt E (a,v)) t), E))
5.320 + (* val Tac tac = subst_tacexpr E a v t;
5.321 + *)
5.322 + | Tac tac =>
5.323 + let val p' = case p_ of Frm => p | Res => lev_on p
5.324 + | _ => raise error ("assy: call by "^
5.325 + (pos'2str (p,p_)));
5.326 + in case assod d m tac of
5.327 Ass (m,v') =>
5.328 let val (p'',c',f',pt') = generate1 (assoc_thy thy') m
5.329 (ScrState (E,l,a,v',S,true)) (p',p_) pt;
5.330 @@ -1361,10 +1384,11 @@
5.331 locate_gen (thy':theory') (m:mstep') ((pt,p):ptree * pos')
5.332 (scr,d) (E,l,a,v,S,bb);
5.333
5.334 - val (p) = (p,p_);
5.335 + val ts = (thy',srls);
5.336 + val p = (p,p_);
5.337 val (scr as Script (h $ body)) = (sc);
5.338 val ScrState (E,l,a,v,S,b) = (is);
5.339 - locate_gen thy' m (pt,p) (Script (h $ body),d) (ScrState(E,l,a,v,S,b));
5.340 + locate_gen (thy',srls) m (pt,p) (Script(h $ body),d)(ScrState(E,l,a,v,S,b));
5.341 *)
5.342 | locate_gen (ts as (thy',srls)) (m:mstep') ((pt,p):ptree * pos')
5.343 (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b)) =
5.344 @@ -1381,7 +1405,8 @@
5.345 then let (*val _=writeln("### locate_gen, bef g1: p="^(pos'2str p));*)
5.346 val (po,p_) = p;
5.347 val po' = case p_ of Frm => po | Res => lev_on po
5.348 - val (p'',c'',f'',pt'') = generate1 thy m (ScrState is) (po',p_) pt;
5.349 + val (p'',c'',f'',pt'') =
5.350 + generate1 thy m (ScrState is) (po',p_) pt;
5.351 (*val _=writeln("### locate_gen, aft g1: p''="^(pos'2str p''));*)
5.352 (*drop the intermediate steps !*)
5.353 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
5.354 @@ -1448,10 +1473,10 @@
5.355 Skip (res, E) =>
5.356 let (*val _= writeln("### appy Let "^(term2str t));
5.357 val _= writeln("### appy Let: Skip res ="^(term2str res));*)
5.358 - val (i',b') = variant_abs (i,T,b); (*term.ML FIXXXXXME streichen?*)
5.359 - val i = mk_Free(i',T);
5.360 - val E' = upd_env E (i,res);
5.361 - in appy thy ptp E' (*eno,[](*env'*),iar,res,s*) (l@[R,D]) b(*ody'*) a v end
5.362 + (*val (i',b') = variant_abs (i,T,b); WN.15.5.03
5.363 + val i = mk_Free(i',T); WN.15.5.03 *)
5.364 + val E' = upd_env E (Free (i,T), res);
5.365 + in appy thy ptp E' (l@[R,D]) b a v end
5.366 | ay => ay)
5.367
5.368 | appy (thy as (th,sr)) ptp E l
5.369 @@ -1471,12 +1496,12 @@
5.370 else Skip (v, E))
5.371
5.372 | appy (thy as (th,sr)) ptp E l (t as Const ("If",_) $ c $ e1 $ e2) a v =
5.373 - ((*writeln("### appy If: t= "^(term2str t));
5.374 - writeln("### appy If: c= "^(term2str (subst_atomic (upd_env_opt E (a,v))c)));
5.375 - writeln("### appy If: thy= "^thy);*)
5.376 + (writeln("### appy If: t= "^(term2str t));
5.377 + writeln("### appy If: c= "^(term2str(subst_atomic(upd_env_opt E(a,v))c)));
5.378 + writeln("### appy If: thy= "^(fst thy));
5.379 if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
5.380 - then ((*writeln("### appy If: true") ;*)appy thy ptp E (l@[L,R]) e1 a v)
5.381 - else ((*writeln("### appy If: false");*)appy thy ptp E (l@[ R]) e2 a v))
5.382 + then (writeln("### appy If: true") ;appy thy ptp E (l@[L,R]) e1 a v)
5.383 + else (writeln("### appy If: false");appy thy ptp E (l@[ R]) e2 a v))
5.384
5.385 | appy thy ptp E (*env*) l
5.386 (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v =
5.387 @@ -1559,14 +1584,16 @@
5.388 appy (th,sr) (pt, p) E l t a v;
5.389 *)
5.390 | appy (thy as (th,sr)) (pt, p) E l t a v =
5.391 - if is_listexpr t
5.392 - then ((*writeln("### appy, listexpr= "^(term2str t));
5.393 + case subst_tacexpr E a v t of
5.394 + Expr s => (writeln("### appy, listexpr= "^(term2str t));
5.395 + writeln("### appy, E= "^(env2str E));
5.396 writeln("### appy, eval(..)= "^(term2str
5.397 - (eval_listexpr_ (assoc_thy thy)
5.398 - (subst_atomic (upd_env_opt E (a,v)) t))));*)
5.399 + (eval_listexpr_ (assoc_thy th) sr
5.400 + (subst_atomic (upd_env_opt E (a,v)) t))));
5.401 Skip (eval_listexpr_ (assoc_thy th) sr
5.402 (subst_atomic (upd_env_opt E (a,v)) t), E))
5.403 - else let val tac = subst_tac E a v t;
5.404 + | Tac tac =>
5.405 + let
5.406 (*val _= writeln("### appy t, E= "^(subst2str E));
5.407 val t =(term_of o the o (parse Isac.thy))"Rewrite_Set make_polyomial False g_";
5.408 val v =(term_of o the o (parse Isac.thy))"x+1=0";
5.409 @@ -1752,6 +1779,10 @@
5.410 ((thy',srls),(pt',p'), sc);
5.411 val ScrState (E,l,a,v,s,b) = is';
5.412 next_tac thy ptp (Script (h $ body)) (ScrState (E,l,a,v,s,b));
5.413 +
5.414 + val (thy, ptp as (pt,(p,_)),sc as Script(h $ body),ScrState (E,l,a,v,s,b)) =
5.415 + ((thy',srls),(pt,(lev_on p,Frm)), scr, is);
5.416 + next_tac thy ptp (Script (h $ body)) (ScrState (E,l,a,v,s,b));
5.417 *)
5.418 | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body))
5.419 (ScrState (E,l,a,v,s,b)) =
6.1 --- a/src/sml/ME/sequent.sml Fri May 09 23:16:32 2003 +0200
6.2 +++ b/src/sml/ME/sequent.sml Thu May 15 16:22:52 2003 +0200
6.3 @@ -432,7 +432,9 @@
6.4
6.5 | Take' of term | Take_Inst' of term
6.6 | Group' of (con * int list * term)
6.7 -| Subproblem' of (spec * (ori list) * term) (*term: Subproblem(dom,pbl)*)
6.8 +| Subproblem' of (spec *
6.9 + (ori list) * (*filled in ......*)
6.10 + term) (*Subproblem(dom,pbl)*)
6.11 | CAScmd' of term
6.12 | End_Subproblem' of term (*???*)
6.13 | Split_And' of term | Conclude_And' of term
7.1 --- a/src/sml/ME/solve.sml Fri May 09 23:16:32 2003 +0200
7.2 +++ b/src/sml/ME/solve.sml Thu May 15 16:22:52 2003 +0200
7.3 @@ -143,13 +143,13 @@
7.4 in ((p,p_), [], Form' (FormKF (~1,EdUndef,(length p), Nundef, f)),
7.5 fst (next_tac (thy',srls) (pt,(p,p_)) scr is), Safe, pt) end
7.6 | None =>
7.7 - let val (m,_) = next_tac (thy',srls) (pt,(lev_on p,Frm)) scr is
7.8 + let val (m,_) = next_tac (thy',srls) (pt,(lev_on p,Frm)) scr is;
7.9 val f = case m of
7.10 Subproblem (domID, pblID) =>
7.11 Form' (FormKF (~1,EdUndef,(length p), Nundef,
7.12 (Sign.string_of_term (sign_of (assoc_thy thy'))
7.13 (subpbl domID pblID))))
7.14 - | _ => EmptyMout
7.15 + | _ => EmptyMout;
7.16 (*nothing written to pt !!!*)
7.17 in ((p,p_), [], f, m, Safe, pt) end
7.18 end
7.19 @@ -249,7 +249,8 @@
7.20 m e_istate (p,p_) pt;
7.21 in ((p,p_),ps,f, Empty_Mstep, Unsafe, pt) end
7.22 else
7.23 - let val thy' = get_obj g_domID pt (par_pblobj pt p);
7.24 + let
7.25 + val thy' = get_obj g_domID pt (par_pblobj pt p);
7.26 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
7.27 (*val _= writeln("### solve, before locate_gen p="^(pos'2str(p,p_)));*)
7.28 val d = e_rls; (*FIXME: canon.simplifier for domain is missing
7.29 @@ -258,6 +259,12 @@
7.30 Steps (is', (m',f',pt',p',c')::ss) =>
7.31 (* val Steps (is', (m',f',pt',p',c')::ss) =
7.32 locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
7.33 +
7.34 +val oris = fst (get_obj g_origin pt' [1,1]);writeln(oris2str oris);
7.35 +
7.36 +val Subproblem' (_,oris,_) = m';
7.37 +writeln(oris2str oris);
7.38 +
7.39 *)
7.40 let val nxt =
7.41 case p' of (*change from solve to model subprobl*)
8.1 --- a/src/sml/ROOT.ML Fri May 09 23:16:32 2003 +0200
8.2 +++ b/src/sml/ROOT.ML Thu May 15 16:22:52 2003 +0200
8.3 @@ -38,8 +38,7 @@
8.4 *)
8.5
8.6
8.7 -Compiler.Control.Print.printDepth:=6; (*4 default*)
8.8 -Compiler.Control.Print.printDepth:=5; (*4 default*)
8.9 +Compiler.Control.Print.printDepth:=7; (*4 default*)
8.10 Compiler.Control.Print.printDepth:=4; (*4 default*)
8.11 Compiler.Control.Print.printLength:=999; (*8 default*)
8.12 Compiler.Control.Print.stringDepth:=25000; (*250 default*)
8.13 @@ -98,7 +97,7 @@
8.14 cd"kbtest";
8.15 use"complex.sml";
8.16 use"diff.sml";
8.17 - use"diffapp.sml";
8.18 + (*use"diffapp.sml"; just in work###########################*)
8.19 use"float.sml";
8.20 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
8.21 use"logexp.sml";
8.22 @@ -133,7 +132,7 @@
8.23 "******* systests complete *******";
8.24 cd "../";
8.25
8.26 -Compiler.Control.Print.printDepth:=9; (*4 default*)
8.27 +Compiler.Control.Print.printDepth:=7; (*4 default*)
8.28 Compiler.Control.Print.printDepth:=4; (*4 default*)
8.29 Compiler.Control.Print.printLength:=8; (*8 default*)
8.30 Compiler.Control.Print.printLength:=9999; (*8 default*)
9.1 --- a/src/sml/Scripts/term_G.sml Fri May 09 23:16:32 2003 +0200
9.2 +++ b/src/sml/Scripts/term_G.sml Thu May 15 16:22:52 2003 +0200
9.3 @@ -715,19 +715,18 @@
9.4 fun mk_Free (s,T) = Free(s,T);
9.5 fun mk_free T s = Free(s,T);
9.6
9.7 -
9.8 (*instantiate let; necessary for ass_up*)
9.9 fun inst_abs thy (Const sT) = Const sT
9.10 | inst_abs thy (Free sT) = Free sT
9.11 | inst_abs thy (Bound n) = Bound n
9.12 | inst_abs thy (Var iT) = Var iT
9.13 | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) =
9.14 - let val (v',b') = variant_abs (v,T2,b); (*term.ML*)
9.15 + let val (v',b') = variant_abs (v,T2,b); (*fun variant_abs: term.ML*)
9.16 in Const ("Let",T1) $ inst_abs thy e $ (Abs (v',T2,inst_abs thy b')) end
9.17 | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
9.18 | inst_abs thy t =
9.19 - (writeln("inst_abs: unchanged t= "
9.20 - ^(Sign.string_of_term (sign_of thy) t));t);
9.21 + (writeln("inst_abs: unchanged t= "^(Sign.string_of_term (sign_of thy) t));
9.22 + t);
9.23 (*val scr as (Script sc) = Script ((term_of o the o (parse thy))
9.24 "Script Testeq (e_::bool) = \
9.25 \While (contains_root e_) Do \
9.26 @@ -790,11 +789,187 @@
9.27 *** . . . . . . . . Const ( Script.Rewrite)
9.28 *** . . . . . . . . . Free ( radd_0, )
9.29 *** . . . . . . . . . Const ( False)
9.30 -*** . . . . . . . . . Free ( e_, ) <-- !!!
9.31 +*** . . . . . . . . . Free ( e_, ) <-- ZUFALL vor 5.03!!!
9.32 val it = () : unit*)
9.33
9.34
9.35
9.36 +
9.37 +fun inst_abs thy (Const sT) = Const sT
9.38 + | inst_abs thy (Free sT) = Free sT
9.39 + | inst_abs thy (Bound n) = Bound n
9.40 + | inst_abs thy (Var iT) = Var iT
9.41 + | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) =
9.42 + let val b' = subst_bound (Free(v,T2),b);
9.43 + (*fun variant_abs: term.ML*)
9.44 + in Const ("Let",T1) $ inst_abs thy e $ (Abs (v,T2,inst_abs thy b')) end
9.45 + | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
9.46 + | inst_abs thy t =
9.47 + (writeln("inst_abs: unchanged t= "^(Sign.string_of_term (sign_of thy) t));
9.48 + t);
9.49 +(*val scr =
9.50 + "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \
9.51 + \ (let h_ = (hd o (filterVar f_)) eqs_; \
9.52 + \ e_1 = hd (dropWhile (ident h_) eqs_); \
9.53 + \ vs_ = dropWhile (ident f_) (Vars h_); \
9.54 + \ v_1 = hd (dropWhile (ident v_) vs_); \
9.55 + \ (s_1::bool list)=(SubProblem(DiffApp_,[univar,equation],[no_met])\
9.56 + \ [bool_ e_1, real_ v_1])\
9.57 + \ in Substitute [(v_1, (rhs o hd) s_1)] h_)";
9.58 +> val ttt = (term_of o the o (parse thy)) scr;
9.59 +> writeln(term2str ttt);
9.60 +> atomt ttt;
9.61 +*** -------------
9.62 +*** Const ( DiffApp.Make'_fun'_by'_explicit)
9.63 +*** . Free ( f_, )
9.64 +*** . Free ( v_, )
9.65 +*** . Free ( eqs_, )
9.66 +*** . Const ( Let)
9.67 +*** . . Const ( Fun.op o)
9.68 +*** . . . Const ( List.hd)
9.69 +*** . . . Const ( DiffApp.filterVar)
9.70 +*** . . . . Free ( f_, )
9.71 +*** . . . Free ( eqs_, )
9.72 +*** . . Abs( h_,..
9.73 +*** . . . Const ( Let)
9.74 +*** . . . . Const ( List.hd)
9.75 +*** . . . . . Const ( List.dropWhile)
9.76 +*** . . . . . . Const ( Atools.ident)
9.77 +*** . . . . . . . Bound 0 <---- Free ( h_, )
9.78 +*** . . . . . . Free ( eqs_, )
9.79 +*** . . . . Abs( e_1,..
9.80 +*** . . . . . Const ( Let)
9.81 +*** . . . . . . Const ( List.dropWhile)
9.82 +*** . . . . . . . Const ( Atools.ident)
9.83 +*** . . . . . . . . Free ( f_, )
9.84 +*** . . . . . . . Const ( Tools.Vars)
9.85 +*** . . . . . . . . Bound 1 <---- Free ( h_, )
9.86 +*** . . . . . . Abs( vs_,..
9.87 +*** . . . . . . . Const ( Let)
9.88 +*** . . . . . . . . Const ( List.hd)
9.89 +*** . . . . . . . . . Const ( List.dropWhile)
9.90 +*** . . . . . . . . . . Const ( Atools.ident)
9.91 +*** . . . . . . . . . . . Free ( v_, )
9.92 +*** . . . . . . . . . . Bound 0 <---- Free ( vs_, )
9.93 +*** . . . . . . . . Abs( v_1,..
9.94 +*** . . . . . . . . . Const ( Let)
9.95 +*** . . . . . . . . . . Const ( Script.SubProblem)
9.96 +*** . . . . . . . . . . . Const ( Pair)
9.97 +*** . . . . . . . . . . . . Free ( DiffApp_, )
9.98 +*** . . . . . . . . . . . . Const ( Pair)
9.99 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
9.100 +*** . . . . . . . . . . . . . . Free ( univar, )
9.101 +*** . . . . . . . . . . . . . . Const ( List.list.Cons)
9.102 +*** . . . . . . . . . . . . . . . Free ( equation, )
9.103 +*** . . . . . . . . . . . . . . . Const ( List.list.Nil)
9.104 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
9.105 +*** . . . . . . . . . . . . . . Free ( no_met, )
9.106 +*** . . . . . . . . . . . . . . Const ( List.list.Nil)
9.107 +*** . . . . . . . . . . . Const ( List.list.Cons)
9.108 +*** . . . . . . . . . . . . Const ( Script.bool_)
9.109 +*** . . . . . . . . . . . . . Bound 2 <----- Free ( e_1, )
9.110 +*** . . . . . . . . . . . . Const ( List.list.Cons)
9.111 +*** . . . . . . . . . . . . . Const ( Script.real_)
9.112 +*** . . . . . . . . . . . . . . Bound 0 <----- Free ( v_1, )
9.113 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
9.114 +*** . . . . . . . . . . Abs( s_1,..
9.115 +*** . . . . . . . . . . . Const ( Script.Substitute)
9.116 +*** . . . . . . . . . . . . Const ( List.list.Cons)
9.117 +*** . . . . . . . . . . . . . Const ( Pair)
9.118 +*** . . . . . . . . . . . . . . Bound 1 <----- Free ( v_1, )
9.119 +*** . . . . . . . . . . . . . . Const ( Fun.op o)
9.120 +*** . . . . . . . . . . . . . . . Const ( Tools.rhs)
9.121 +*** . . . . . . . . . . . . . . . Const ( List.hd)
9.122 +*** . . . . . . . . . . . . . . . Bound 0 <----- Free ( s_1, )
9.123 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
9.124 +*** . . . . . . . . . . . . Bound 4 <----- Free ( h_, )
9.125 +
9.126 +> val ttt' = inst_abs thy ttt;
9.127 +> writeln(term2str ttt');
9.128 +Script Make_fun_by_explicit f_ v_ eqs_ =
9.129 + ... as above ...
9.130 +> atomt ttt';
9.131 +*** -------------
9.132 +*** Const ( DiffApp.Make'_fun'_by'_explicit)
9.133 +*** . Free ( f_, )
9.134 +*** . Free ( v_, )
9.135 +*** . Free ( eqs_, )
9.136 +*** . Const ( Let)
9.137 +*** . . Const ( Fun.op o)
9.138 +*** . . . Const ( List.hd)
9.139 +*** . . . Const ( DiffApp.filterVar)
9.140 +*** . . . . Free ( f_, )
9.141 +*** . . . Free ( eqs_, )
9.142 +*** . . Abs( h_,..
9.143 +*** . . . Const ( Let)
9.144 +*** . . . . Const ( List.hd)
9.145 +*** . . . . . Const ( List.dropWhile)
9.146 +*** . . . . . . Const ( Atools.ident)
9.147 +*** . . . . . . . Free ( h_, ) <---- Bound 0
9.148 +*** . . . . . . Free ( eqs_, )
9.149 +*** . . . . Abs( e_1,..
9.150 +*** . . . . . Const ( Let)
9.151 +*** . . . . . . Const ( List.dropWhile)
9.152 +*** . . . . . . . Const ( Atools.ident)
9.153 +*** . . . . . . . . Free ( f_, )
9.154 +*** . . . . . . . Const ( Tools.Vars)
9.155 +*** . . . . . . . . Free ( h_, ) <---- Bound 1
9.156 +*** . . . . . . Abs( vs_,..
9.157 +*** . . . . . . . Const ( Let)
9.158 +*** . . . . . . . . Const ( List.hd)
9.159 +*** . . . . . . . . . Const ( List.dropWhile)
9.160 +*** . . . . . . . . . . Const ( Atools.ident)
9.161 +*** . . . . . . . . . . . Free ( v_, )
9.162 +*** . . . . . . . . . . Free ( vs_, ) <---- Bound 0
9.163 +*** . . . . . . . . Abs( v_1,..
9.164 +*** . . . . . . . . . Const ( Let)
9.165 +*** . . . . . . . . . . Const ( Script.SubProblem)
9.166 +*** . . . . . . . . . . . Const ( Pair)
9.167 +*** . . . . . . . . . . . . Free ( DiffApp_, )
9.168 +*** . . . . . . . . . . . . Const ( Pair)
9.169 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
9.170 +*** . . . . . . . . . . . . . . Free ( univar, )
9.171 +*** . . . . . . . . . . . . . . Const ( List.list.Cons)
9.172 +*** . . . . . . . . . . . . . . . Free ( equation, )
9.173 +*** . . . . . . . . . . . . . . . Const ( List.list.Nil)
9.174 +*** . . . . . . . . . . . . . Const ( List.list.Cons)
9.175 +*** . . . . . . . . . . . . . . Free ( no_met, )
9.176 +*** . . . . . . . . . . . . . . Const ( List.list.Nil)
9.177 +*** . . . . . . . . . . . Const ( List.list.Cons)
9.178 +*** . . . . . . . . . . . . Const ( Script.bool_)
9.179 +*** . . . . . . . . . . . . . Free ( e_1, ) <----- Bound 2
9.180 +*** . . . . . . . . . . . . Const ( List.list.Cons)
9.181 +*** . . . . . . . . . . . . . Const ( Script.real_)
9.182 +*** . . . . . . . . . . . . . . Free ( v_1, ) <----- Bound 0
9.183 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
9.184 +*** . . . . . . . . . . Abs( s_1,..
9.185 +*** . . . . . . . . . . . Const ( Script.Substitute)
9.186 +*** . . . . . . . . . . . . Const ( List.list.Cons)
9.187 +*** . . . . . . . . . . . . . Const ( Pair)
9.188 +*** . . . . . . . . . . . . . . Free ( v_1, ) <----- Bound 1
9.189 +*** . . . . . . . . . . . . . . Const ( Fun.op o)
9.190 +*** . . . . . . . . . . . . . . . Const ( Tools.rhs)
9.191 +*** . . . . . . . . . . . . . . . Const ( List.hd)
9.192 +*** . . . . . . . . . . . . . . . Free ( s_1, ) <----- Bound 0
9.193 +*** . . . . . . . . . . . . . Const ( List.list.Nil)
9.194 +*** . . . . . . . . . . . . Free ( h_, ) <----- Bound 4
9.195 +
9.196 +Note numbering of de Bruijn indexes !
9.197 +
9.198 +Script Make_fun_by_explicit f_ v_ eqs_ =
9.199 + let h_ = (hd o filterVar f_) eqs_;
9.200 + e_1 = hd (dropWhile (ident h_ BOUND_0) eqs_);
9.201 + vs_ = dropWhile (ident f_) (Vars h_ BOUND_1);
9.202 + v_1 = hd (dropWhile (ident v_) vs_ BOUND_0);
9.203 + s_1 =
9.204 + SubProblem (DiffApp_, [univar, equation], [no_met])
9.205 + [bool_ e_1 BOUND_2, real_ v_1 BOUND_0]
9.206 + in Substitute [(v_1 BOUND_1, (rhs o hd) s_1 BOUND_0)] h_ BOUND_4
9.207 +*)
9.208 +
9.209 +
9.210 +
9.211 +
9.212 fun T_a2real (Type (s, [])) =
9.213 if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, [])
9.214 | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts)
10.1 --- a/src/sml/definitions.sml Fri May 09 23:16:32 2003 +0200
10.2 +++ b/src/sml/definitions.sml Thu May 15 16:22:52 2003 +0200
10.3 @@ -2,6 +2,8 @@
10.4 use"definitions.sml";
10.5 *)
10.6
10.7 +val linefeed = (curry op^) "\n";
10.8 +
10.9 type cterm' = string;
10.10 val empty_cterm' = "empty_cterm'";
10.11 type thmID = string;
10.12 @@ -18,12 +20,6 @@
10.13
10.14 type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*)
10.15 type subst = (term * term) list; (*here for ets2str*)
10.16 -fun subst2str (s:subst) =
10.17 - (strs2str o
10.18 - (map (pair2str o
10.19 - (apsnd (Sign.string_of_term (sign_of thy))) o
10.20 - (apfst (Sign.string_of_term (sign_of thy)))))) s;
10.21 -
10.22
10.23
10.24 datatype rule =
10.25 @@ -309,6 +305,14 @@
10.26 fun terms2str ts= (strs2str o (map (Sign.string_of_term
10.27 (sign_of (assoc_thy "Isac.thy"))))) ts;
10.28
10.29 +fun subst2str (s:subst) =
10.30 + (strs2str o
10.31 + (map (linefeed o pair2str o
10.32 + (apsnd term2str) o
10.33 + (apfst term2str)))) s;
10.34 +val env2str = subst2str;
10.35 +
10.36 +
10.37 (*recursive defs:*)
10.38 fun scr2str (Script s) = "Script "^(term2str s)
10.39 | scr2str (Rfuns _) = "Rfuns";
11.1 --- a/src/sml/globals.sml Fri May 09 23:16:32 2003 +0200
11.2 +++ b/src/sml/globals.sml Thu May 15 16:22:52 2003 +0200
11.3 @@ -53,6 +53,10 @@
11.4 met : metID list}; (* methods solving the pbt*)
11.5 val e_pbt = {thy=ProtoPure.thy,cas=None,prls=Erls,
11.6 where_=[],ppc=[],met=[]}:pbt;
11.7 +fun pbt2 (str, (t1, t2)) =
11.8 + pair2str (str, pair2str (term2str t1, term2str t2));
11.9 +fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt;
11.10 +
11.11
11.12 (*.'a is for pbt | met.*)
11.13 (*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*)
12.1 --- a/src/sml/kbtest/diffapp.sml Fri May 09 23:16:32 2003 +0200
12.2 +++ b/src/sml/kbtest/diffapp.sml Thu May 15 16:22:52 2003 +0200
12.3 @@ -511,28 +511,88 @@
12.4 val (dI',pI',mI') =
12.5 ("DiffApp.thy",["maximum_of","function"],
12.6 ["DiffApp","max_by_calculus"]);
12.7 +
12.8 val p = e_pos'; val c = []; val pt = EmptyPtree;
12.9 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
12.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.12 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.14 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.15 +val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
12.16 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.17 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.18 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.20 (*val nxt = ("Specify_Method",Specify_Method ["DiffApp","max_by_calculus"])*)
12.21 +
12.22 +val oris = fst (get_obj g_origin pt (fst p));writeln(oris2str oris);
12.23 +val itms = get_obj g_pbl pt (fst p);writeln(itms2str thy itms);
12.24 +
12.25 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.26 val (p,_,f,nxt,_,pt) = me nxt p c pt;(*FIXXXXXXXXME: hide met-args !!!*)
12.27 val (p,_,f,nxt,_,pt) = me nxt p c pt;(*FIXXXXXXXXME: hide met-args !!!*)
12.28 val (p,_,f,nxt,_,pt) = me nxt p c pt;(*FIXXXXXXXXME: hide met-args !!!*)
12.29 (*val nxt = ("Apply_Method",Apply_Method ["DiffApp","max_by_calculus"])*)
12.30 -
12.31 -(*----GOON
12.32 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.33 +(*val nxt = ("Subproblem",Subproblem ("DiffApp.thy",["make","function"]))*)
12.34 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.35 +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make","function"])*)
12.36 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.37 +(*val nxt = ("Model_Problem",Model_Problem ["by_explicit","make","function"])*)
12.38 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.39 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.40 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.41 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.42 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.43
12.44 +val oris = fst (get_obj g_origin pt (fst p));writeln(oris2str oris);
12.45 +val itms = get_obj g_pbl pt (fst p);writeln(itms2str thy itms);
12.46 +
12.47 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.48 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.49 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.50 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.51 +(*val nxt = ("Apply_Method",Apply_Method ["DiffApp","make_fun_by_explicit"])*)
12.52 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.53 +(*val nxt = Subproblem ("DiffApp.thy",["univariate","equation"])) *)
12.54 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.55 +(*val nxt = Refine_Tacitly ["univariate","equation"])*)
12.56 +
12.57 +val oris = fst (get_obj g_origin pt (fst p));writeln(oris2str oris);
12.58 +val itms = get_obj g_pbl pt (fst p);writeln(itms2str thy itms);
12.59 +
12.60 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.61 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.62 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.63 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.64 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.65 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.66 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.67 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.68 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.69 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.70 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.71 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.72 +(*val f = "1 / 4 * b ^^^ 2 = -1 * (a ^^^ 2 / 4 + -4 * r ^^^ 2 / 4)")) : mout
12.73 + val nxt = ("Or_to_List",Or_to_List) : string * mstep ~~~~~~~~~~~ ?!?!?!?!*)
12.74 +
12.75 +
12.76 +
12.77 +(*val f =
12.78 +Error' (Error_ "Refine_Tacitly [\"univariate\",\"equation\"] not applicable")*)
12.79 +
12.80 +
12.81 +(*----GOON.15.5.03 run scripts for maximum-example: univariate equation ?!?
12.82 +
12.83 +val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
12.84 +
12.85 +val oris = fst (get_obj g_origin pt (fst p));writeln(oris2str oris);
12.86 +
12.87 +val itms = get_obj g_pbl pt (fst p);writeln(itms2str thy itms);
12.88 +val itms = get_obj g_pbl pt [];writeln(itms2str thy itms);
12.89 +
12.90 val itms = get_obj g_met pt (fst p);writeln(itms2str thy itms);
12.91 +val itms = get_obj g_met pt [];writeln(itms2str thy itms);
12.92
12.93 itms2args thy ["DiffApp","max_by_calculus"] itms;
12.94
13.1 --- a/src/sml/kbtest/polyeq.sml Fri May 09 23:16:32 2003 +0200
13.2 +++ b/src/sml/kbtest/polyeq.sml Thu May 15 16:22:52 2003 +0200
13.3 @@ -12,7 +12,7 @@
13.4 "-------------------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
13.5 "-------------------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b--------*)";
13.6
13.7 -"---- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk I s.86 Bsp 5-------------*)";
13.8 +"---- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk I s.86 Bsp 5-------------";
13.9 "((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1)),(*Schal II s.68 Bsp 37*)";
13.10
13.11
14.1 --- a/src/sml/kbtest/rlang.sml Fri May 09 23:16:32 2003 +0200
14.2 +++ b/src/sml/kbtest/rlang.sml Thu May 15 16:22:52 2003 +0200
14.3 @@ -1409,3 +1409,47 @@
14.4 else raise error "rlang.sml: 7";
14.5 *)
14.6
14.7 +
14.8 +"-------------------- WN.15.5.03: Pythagoras -------------------------------";
14.9 +"-------------------- WN.15.5.03: Pythagoras -------------------------------";
14.10 +"-------------------- WN.15.5.03: Pythagoras -------------------------------";
14.11 +val fmz = ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)",
14.12 + "solveFor x","solutions L"];
14.13 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
14.14 +
14.15 +val p = e_pos'; val c = [];
14.16 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
14.17 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
14.18 +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
14.19 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.20 +(* Model_Problem ["normalize","polynomial","univariate","equation"])*)
14.21 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.22 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.23 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.24 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.25 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.26 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.27 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.28 +(*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
14.29 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.30 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.31 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.32 +(*val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])*)
14.33 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.34 +(*val nxt = Refine_Tacitly ["polynomial","univariate","equation"]) *)
14.35 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.36 +(*val nxt =Model_Problem ["degree_0","polynomial","univariate","equation"])*)
14.37 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.38 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.39 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.40 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.41 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.42 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.43 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.44 +(*val nxt = ("Apply_Method",Apply_Method ["PolyEq","solve_d0_poly_equation"])*)
14.45 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.46 +(*val f = "a ^^^ 2 / 4 + b ^^^ 2 / 4 + -4 * r ^^^ 2 / 4 = 0"))
14.47 +val nxt = Rewrite_Set_Inst (["(bdv, x)"],"d0_poly_simplify")) *)
14.48 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.49 +(*val f = Form' (FormKF (~1,EdUndef,2,Nundef,"False")) ???????????????
14.50 +val nxt = ("Or_to_List",Or_to_List) *)
15.1 --- a/src/sml/systest/calculate.sml Fri May 09 23:16:32 2003 +0200
15.2 +++ b/src/sml/systest/calculate.sml Thu May 15 16:22:52 2003 +0200
15.3 @@ -450,4 +450,4 @@
15.4
15.5 val t = str2term "Float ((1,2),(0,0)) * Float ((3,4),(0,0))";
15.6 atomty thy t;
15.7 -(*GOON.10.4.03*)
15.8 \ No newline at end of file
15.9 +(*GOON.10.4.03 eval_binop Float *)
16.1 --- a/src/sml/systest/list_rls.sml Fri May 09 23:16:32 2003 +0200
16.2 +++ b/src/sml/systest/list_rls.sml Thu May 15 16:22:52 2003 +0200
16.3 @@ -133,6 +133,15 @@
16.4 if s''="A = a * b" then () else raise error "new behaviour with list_rls 1.1.";
16.5 val env = env @ [(str2term "e_::bool",str2term "A = a * b")];
16.6
16.7 +(*--- 2.line: condition alone ---*)
16.8 +val t = str2term "1 < length_ (rs_::bool list)";
16.9 +val s = subst_atomic env t;
16.10 +term2str s;
16.11 +"1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
16.12 +val Some (s',_) = rewrite_set_ thy false list_rls s;
16.13 +val s'' = term2str s';
16.14 +if s''="True" then () else raise error "new behaviour with list_rls 1.2.";
16.15 +
16.16 (*--- 2.line in script ---*)
16.17 val t = str2term
16.18 "(if 1 < length_ rs_ \
16.19 @@ -152,13 +161,12 @@
16.20 "SubProblem (Reals_, [make, function], [no_met])\n\
16.21 \ [real_ A, real_ b,\n\
16.22 \ bool_list_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]" then ()
16.23 -else raise error "new behaviour with list_rls 1.2.";
16.24 +else raise error "new behaviour with list_rls 1.3.";
16.25 val env = env @ [(str2term "t_::bool",
16.26 str2term "A = (2*sqrt(r^^^2-(b/2)^^^2)) * b")];
16.27
16.28
16.29
16.30 -
16.31 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
16.32 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
16.33 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
17.1 --- a/src/sml/systest/refine.sml Fri May 09 23:16:32 2003 +0200
17.2 +++ b/src/sml/systest/refine.sml Thu May 15 16:22:52 2003 +0200
17.3 @@ -55,30 +55,30 @@
17.4
17.5 (*case 1: no refinement *)
17.6 val thy = Isac.thy;
17.7 -val (d1,ts1,vs1) = split_dts thy ((term_of o the o (parse thy))
17.8 +val (d1,ts1) = split_dts thy ((term_of o the o (parse thy))
17.9 "fixedValues [aaa=0]");
17.10 -val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy))
17.11 +val (d2,ts2) = split_dts thy ((term_of o the o (parse thy))
17.12 "errorBound (ddd=0)");
17.13 val ori1 = [(1,[1],"#Given",d1,ts1),
17.14 (2,[1],"#Given",d2,ts2)]:ori list;
17.15
17.16
17.17 (*case 2: refined to pbt without children *)
17.18 -val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy))
17.19 +val (d2,ts2) = split_dts thy ((term_of o the o (parse thy))
17.20 "relations [aaa333]");
17.21 val ori2 = [(1,[1],"#Given",d1,ts1),
17.22 (2,[1],"#Given",d2,ts2)]:ori list;
17.23
17.24
17.25 (*case 3: refined to pbt with children *)
17.26 -val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy))
17.27 +val (d2,ts2) = split_dts thy ((term_of o the o (parse thy))
17.28 "valuesFor [aaa222]");
17.29 val ori3 = [(1,[1],"#Given",d1,ts1),
17.30 (2,[1],"#Given",d2,ts2)]:ori list;
17.31
17.32
17.33 (*case 4: refined to children (without child)*)
17.34 -val (d3,ts3,vs3) = split_dts thy ((term_of o the o (parse thy))
17.35 +val (d3,ts3) = split_dts thy ((term_of o the o (parse thy))
17.36 "boundVariable aaa222yyy");
17.37 val ori4 = [(1,[1],"#Given",d1,ts1),
17.38 (2,[1],"#Given",d2,ts2),
18.1 --- a/src/sml/systest/scriptnew.sml Fri May 09 23:16:32 2003 +0200
18.2 +++ b/src/sml/systest/scriptnew.sml Thu May 15 16:22:52 2003 +0200
18.3 @@ -416,12 +416,13 @@
18.4
18.5
18.6
18.7 +
18.8 "------------------ script with Map, Subst (biquadr.equ.)---------";
18.9 "------------------ script with Map, Subst (biquadr.equ.)---------";
18.10 "------------------ script with Map, Subst (biquadr.equ.)---------";
18.11
18.12
18.13 -(*GOON
18.14 +(*GOON.5.03. script with Map, Subst (biquadr.equ.)
18.15 val scr = Script (((inst_abs thy) o term_of o the o (parse thy))
18.16 "Script Biquadrat_poly (e_::bool) (v_::real) = \
18.17 \(let e_ = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_; \
18.18 @@ -431,7 +432,8 @@
18.19 \ ((Rewrite real_root_positive False) Or \
18.20 \ (Rewrite real_root_negative False)) @@ \
18.21 \ OrToList) L_0_ \
18.22 - \ in (flat))"
18.23 + \ in (flat ....))"
18.24 );
18.25
18.26 *)
18.27 +