intermed. context integration appl_add does not work
1.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon Mar 21 00:32:53 2011 +0100
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Apr 04 11:05:07 2011 +0200
1.3 @@ -15,7 +15,7 @@
1.4 val all_modspec : ptree * pos' -> ptree * pos'
1.5 datatype appl = Appl of tac_ | Notappl of string
1.6 val appl_add :
1.7 - theory ->
1.8 + Proof.context ->
1.9 string ->
1.10 SpecifyTools.ori list ->
1.11 SpecifyTools.itm list ->
1.12 @@ -90,13 +90,13 @@
1.13 val is_error : SpecifyTools.itm_ -> bool
1.14 val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
1.15 val is_known :
1.16 - theory ->
1.17 + Proof.context ->
1.18 string ->
1.19 SpecifyTools.ori list ->
1.20 Term.term -> string * SpecifyTools.ori * Term.term list
1.21 val is_list_type : Term.typ -> bool
1.22 val is_notyet_input :
1.23 - theory ->
1.24 + Proof.context ->
1.25 SpecifyTools.itm list ->
1.26 Term.term list ->
1.27 SpecifyTools.ori ->
1.28 @@ -142,7 +142,6 @@
1.29 val ori2Coritm :
1.30 pat list -> ori -> itm
1.31 val ori_2itm :
1.32 - 'a ->
1.33 SpecifyTools.itm_ ->
1.34 Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
1.35 val overwrite_ppc :
1.36 @@ -169,7 +168,7 @@
1.37 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
1.38 -> string * SpecifyTools.ori * Term.term list
1.39 val seek_orits :
1.40 - theory ->
1.41 + Proof.context ->
1.42 string ->
1.43 Term.term list ->
1.44 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
1.45 @@ -193,7 +192,7 @@
1.46 ptree ->
1.47 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
1.48 val tag_form : theory -> term * term -> term
1.49 - val test_types : theory -> Term.term * Term.term list -> string
1.50 + val test_types : Proof.context -> Term.term * Term.term list -> string
1.51 val typeless : Term.term -> Term.term
1.52 val unbound_ppc : term SpecifyTools.ppc -> Term.term list
1.53 val vals_of_oris : SpecifyTools.ori list -> Term.term list
1.54 @@ -277,40 +276,35 @@
1.55
1.56 (*.to an input (d,ts) find the according ori and insert the ts.*)
1.57 (*WN.11.03: + dont take first inter<>[]*)
1.58 -fun seek_oridts thy sel (d,ts) [] =
1.59 - ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
1.60 - (comp_dts thy (d,ts))) ^
1.61 +fun seek_oridts ctxt sel (d,ts) [] =
1.62 + ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
1.63 + (comp_dts (d,ts))) ^
1.64 "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
1.65 [])
1.66 - | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
1.67 - if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
1.68 - then if sel = sel'
1.69 + | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
1.70 + if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
1.71 then ("",
1.72 (id,vat,sel,d, inter op = ts ts'):ori,
1.73 ts')
1.74 - else ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
1.75 - (comp_dts thy (d,ts))) ^ " not for " ^ sel,
1.76 - e_ori_,
1.77 - [])
1.78 - else seek_oridts thy sel (d,ts) oris;
1.79 + else seek_oridts ctxt sel (d,ts) oris;
1.80
1.81 (*.to an input (_,ts) find the according ori and insert the ts.*)
1.82 -fun seek_orits thy sel ts [] =
1.83 +fun seek_orits ctxt sel ts [] =
1.84 ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
1.85 - (thy2ctxt thy))) ts) ^
1.86 + ctxt)) ts) ^
1.87 "') not found in oris (typed)", e_ori_, [])
1.88 - | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
1.89 + | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
1.90 if sel = sel' andalso (inter op = ts ts') <> []
1.91 then if sel = sel'
1.92 then ("",
1.93 (id,vat,sel,d, inter op = ts ts'):ori,
1.94 ts')
1.95 else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
1.96 - (thy2ctxt thy)))) ts)
1.97 + ctxt))) ts)
1.98 ^ " not for " ^ sel,
1.99 e_ori_,
1.100 [])
1.101 - else seek_orits thy sel ts oris;
1.102 + else seek_orits ctxt sel ts oris;
1.103 (* false
1.104 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
1.105 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
1.106 @@ -479,21 +473,19 @@
1.107 (* val (_,_,fd,d,ts) = hd miss;
1.108 *)
1.109 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
1.110 - (fd, (Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy))) o
1.111 - (comp_dts thy)) (d,[hd ts]) : cterm');
1.112 -(* val t = comp_dts thy (d,[hd ts]);
1.113 + (fd, (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) o
1.114 + comp_dts) (d,[hd ts]) : cterm');
1.115 +(* val t = comp_dts (d,[hd ts]);
1.116 *)
1.117
1.118 (* get a term from ori, notyet input in itm.
1.119 the term from ori is thrown back to a string in order to reuse
1.120 machinery for immediate input by the user. *)
1.121 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.122 - (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
1.123 - (comp_dts thy))
1.124 + (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
1.125 (d, subtract op = (ts_in itm_) ts) : cterm');
1.126 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.127 - (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
1.128 - (comp_dts thy))
1.129 + (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
1.130 (d, subtract op = (ts_in itm_) ts) : cterm');
1.131
1.132 (* in FE dsc, not dat: this is in itms ...*)
1.133 @@ -519,7 +511,7 @@
1.134 (f,(d,_))::itms =>
1.135 SOME (f : string,
1.136 ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1.137 - comp_dts thy) (d, []) : cterm')
1.138 + comp_dts) (d, []) : cterm')
1.139 | _ => NONE end
1.140
1.141 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
1.142 @@ -642,10 +634,10 @@
1.143 (*. update the itm_ already input, all..from ori .*)
1.144 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
1.145 *)
1.146 -fun ori_2itm thy itm_ pid all ((id,vt,fd,d,ts):ori) =
1.147 +fun ori_2itm itm_ pid all ((id,vt,fd,d,ts):ori) =
1.148 let
1.149 val ts' = union op = (ts_in itm_) ts;
1.150 - val pval = pbl_ids' thy d ts'
1.151 + val pval = pbl_ids' d ts'
1.152 (*WN.9.5.03: FIXXXME [#0, epsilon]
1.153 here would upd_penv be called for [#0, epsilon] etc. *)
1.154 val complete = if eq_set op = (ts', all) then true else false;
1.155 @@ -685,7 +677,7 @@
1.156 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
1.157 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
1.158 *)
1.159 -fun is_notyet_input thy (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
1.160 +fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
1.161 case find_first (eq1 d) pbt of
1.162 SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
1.163 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
1.164 @@ -696,29 +688,28 @@
1.165 val ts' = inter op = (ts_in itm_) ts;
1.166 in if subset op = (ts, ts')
1.167 then (((strs2str' o
1.168 - map (Print_Mode.setmp [] (Syntax.string_of_term
1.169 - (thy2ctxt thy)))) ts') ^
1.170 + map (Print_Mode.setmp [] (Syntax.string_of_term ctxt))) ts') ^
1.171 " already input", e_itm) (*2*)
1.172 else ("",
1.173 - ori_2itm thy itm_ pid all (i,v,f,d,
1.174 + ori_2itm itm_ pid all (i,v,f,d,
1.175 subtract op = ts' ts)) (*3,4*)
1.176 end
1.177 - | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
1.178 + | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[])))
1.179 pid all (i,v,f,d,ts)) (*1*)
1.180 )
1.181 - | NONE => ("", ori_2itm thy (Sup (d,ts))
1.182 + | NONE => ("", ori_2itm (Sup (d,ts))
1.183 e_term all (i,v,f,d,ts));
1.184
1.185 -fun test_types thy (d,ts) =
1.186 +fun test_types ctxt (d,ts) =
1.187 let
1.188 (*val s = !show_types; val _ = show_types:= true;*)
1.189 - val opt = (try (comp_dts thy)) (d,ts);
1.190 + val opt = (try comp_dts) (d,ts);
1.191 val msg = case opt of
1.192 SOME _ => ""
1.193 - | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) d) ^
1.194 + | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
1.195 " " ^
1.196 ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
1.197 - (thy2ctxt thy)))) ts)
1.198 + ctxt))) ts)
1.199 ^ " is illtyped");
1.200 (*val _ = show_types:= s*)
1.201 in msg end;
1.202 @@ -736,7 +727,7 @@
1.203 give feedback on all(?) strange input;
1.204 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
1.205 (*WN.11.03: from lists*)
1.206 -fun is_known thy sel ori t =
1.207 +fun is_known ctxt sel ori t =
1.208 (* val (ori,t)=(oris,term_of ct);
1.209 *)
1.210 let
1.211 @@ -744,7 +735,7 @@
1.212 val ots = (distinct o flat o (map #5)) (ori:ori list);
1.213 val oids = ((map (fst o dest_Free)) o distinct o
1.214 flat o (map vars)) ots;
1.215 - val (d,ts(*,pval*)) = split_dts thy t;
1.216 + val (d,ts(*,pval*)) = split_dts t;
1.217 val ids = map (fst o dest_Free)
1.218 ((distinct o (flat o (map vars))) ts);
1.219 in if (subtract op = oids ids) <> []
1.220 @@ -757,19 +748,18 @@
1.221 then (("terms '"^
1.222 ((strs2str' o
1.223 (map (Print_Mode.setmp [] (Syntax.string_of_term
1.224 - (thy2ctxt thy))))) ts)^
1.225 + ctxt)))) ts)^
1.226 "' not in example (typeless)"), e_ori_, [])
1.227 - else (case seek_orits thy sel ts ori of
1.228 + else (case seek_orits ctxt sel ts ori of
1.229 ("", ori_ as (_,_,_,d,ts), all) =>
1.230 - (case test_types thy (d,ts) of
1.231 + (case test_types ctxt (d,ts) of
1.232 "" => ("", ori_, all)
1.233 | msg => (msg, e_ori_, []))
1.234 | (msg,_,_) => (msg, e_ori_, []))
1.235 else
1.236 if member op = (map #4 ori) d
1.237 - then seek_oridts thy sel (d,ts) ori
1.238 - else ((Print_Mode.setmp [] (Syntax.string_of_term
1.239 - (thy2ctxt thy)) d) ^
1.240 + then seek_oridts ctxt sel (d,ts) ori
1.241 + else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
1.242 " not in example", (0, [], sel, d, ts), [])
1.243 end;
1.244
1.245 @@ -783,61 +773,45 @@
1.246 (** add an item to the model; check wrt. oris and pbt **)
1.247 (* in contrary to oris<>[] below, this part handles user-input
1.248 extremely acceptive, i.e. accept input instead error-msg *)
1.249 -fun appl_add thy sel ([]:ori list) ppc pbt ct' =
1.250 -(* val (ppc,pbt,ct',env) = (pbl, (#ppc o get_pbt) cpI, ct, []:envv);
1.251 - !!!! 28.8.01: env tested _minimally_ !!!
1.252 - *)
1.253 - let
1.254 - val i = 1 + (if ppc=[] then 0 else maxl (map #1 ppc));
1.255 - in case parse thy ct' of (*should be done in applicable_in 4.00.FIXME*)
1.256 - NONE => Add (i,[],false,sel,Syn ct')
1.257 -(* val (SOME ct) = parse thy ct';
1.258 - *)
1.259 - | SOME ct =>
1.260 +fun appl_add ctxt sel [] ppc pbt t =
1.261 let
1.262 - val (d,ts(*,pval*)) = split_dts thy (term_of ct);
1.263 - in if d = e_term
1.264 - then Add (i,[],false,sel,Mis (dsc_unknown,hd ts(*24.3.02*)))
1.265 -
1.266 - else
1.267 - (case find_first (eq1 d) pbt of
1.268 - NONE => Add (i,[],true,sel,Sup ((d,ts)))
1.269 - | SOME (f,(_,id)) =>
1.270 -(* val SOME (f,(_,id)) = find_first (eq1 d) pbt;
1.271 - *)
1.272 - let
1.273 - fun eq2 d ((i,_,_,_,itm_):itm) =
1.274 - (d = (d_in itm_)) andalso i<>0;
1.275 - in case find_first (eq2 d) ppc of
1.276 - NONE => Add (i,[],true,f, Cor ((d,ts), (id, (*pval*)
1.277 - pbl_ids' thy d ts)))
1.278 - | SOME (i',_,_,_,itm_) =>
1.279 -(* val SOME (i',_,_,_,itm_) = find_first (eq2 d) ppc;
1.280 - val NONE = find_first (eq2 d) ppc;
1.281 - *)
1.282 - if is_list_dsc d
1.283 - then let val ts = union op = ts (ts_in itm_)
1.284 - in Add (if ts_in itm_ = [] then i else i',
1.285 - [],true,f,Cor ((d, ts), (id, (*pval*)
1.286 - pbl_ids' thy d ts)))
1.287 - end
1.288 - else Add (i',[],true,f,Cor ((d,ts),(id, (*pval*)
1.289 - pbl_ids' thy d ts)))
1.290 - end
1.291 - )
1.292 + val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
1.293 + in case parseNEW ctxt t of
1.294 + NONE => Add (i, [], false, sel, Syn t)
1.295 + | SOME t' =>
1.296 + let val (d, ts) = split_dts t';
1.297 + in if d = e_term then
1.298 + Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
1.299 + (case find_first (eq1 d) pbt of
1.300 + NONE => Add (i, [], true, sel, Sup (d,ts))
1.301 + | SOME (f, (_, id)) =>
1.302 + let fun eq2 d (i, _, _, _, itm_) =
1.303 + d = (d_in itm_) andalso i <> 0;
1.304 + in case find_first (eq2 d) ppc of
1.305 + NONE => Add (i, [], true, f,
1.306 + Cor ((d, ts), (id, pbl_ids' d ts))
1.307 + )
1.308 + | SOME (i', _, _, _, itm_) => if is_list_dsc d then
1.309 + let
1.310 + val in_itm = ts_in itm_;
1.311 + val ts' = union op = ts in_itm;
1.312 + val i'' = if in_itm = [] then i else i';
1.313 + in Add (i'', [], true, f,
1.314 + Cor ((d, ts'), (id, pbl_ids' d ts'))
1.315 + )
1.316 + end else
1.317 + Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
1.318 + end)
1.319 + end
1.320 end
1.321 - end
1.322 -(* add ct to ppc *)
1.323 -(*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*)
1.324 - | appl_add thy sel oris ppc pbt (*only for upd_envv*) str =
1.325 - case parse thy str of
1.326 - NONE => Err ("syntax error in " ^ str)
1.327 - | SOME t => case is_known thy sel oris (term_of t) of
1.328 - ("", ori', all) =>
1.329 - (case is_notyet_input thy ppc all ori' pbt of
1.330 - ("", itm) => Add itm
1.331 - | (msg, _) => Err msg)
1.332 - | (msg, _, _) => Err msg;
1.333 + | appl_add ctxt sel oris ppc pbt str =
1.334 + case parseNEW ctxt str of
1.335 + NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
1.336 + | SOME t => case is_known ctxt sel oris t of
1.337 + ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
1.338 + ("", itm) => Add itm
1.339 + | (msg, _) => Err msg)
1.340 + | (msg, _, _) => Err msg;
1.341 (*
1.342 > val (msg,itm) = is_notyet_input thy ppc all ori';
1.343 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
1.344 @@ -1043,8 +1017,8 @@
1.345 (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1.346 val cpI = if pI = e_pblID then pI' else pI;
1.347 val cmI = if mI = e_metID then mI' else mI;
1.348 - val {ppc,pre,prls,...} = get_met cmI
1.349 - in case appl_add thy sel oris met ppc ct of
1.350 + val {ppc,pre,prls,...} = get_met cmI;
1.351 + in case appl_add (thy2ctxt thy) sel oris met ppc ct of
1.352 Add itm (*..union old input *) =>
1.353 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1.354 *)
1.355 @@ -1077,7 +1051,7 @@
1.356 end
1.357 (* val (p,_) = p;
1.358 *)
1.359 -| specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
1.360 +| specify_additem sel (ct,_) (p,p_(*Frm, Pbl*)) c pt =
1.361 let
1.362 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.363 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.364 @@ -1085,7 +1059,7 @@
1.365 val cpI = if pI = e_pblID then pI' else pI;
1.366 val cmI = if mI = e_metID then mI' else mI;
1.367 val {ppc,where_,prls,...} = get_pbt cpI;
1.368 - in case appl_add thy sel oris pbl ppc ct of
1.369 + in case appl_add (thy2ctxt thy) sel oris pbl ppc ct of
1.370 Add itm (*..union old input *) =>
1.371 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1.372 *)
1.373 @@ -1138,9 +1112,10 @@
1.374 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1.375 let (* either """"""""""""""" all empty or complete *)
1.376 val thy = assoc_thy dI';
1.377 + val (istate_, ctxt) = (#ppc o get_pbt) pI' |> prep_ori fmz thy;
1.378 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1.379 - else prep_ori fmz thy ((#ppc o get_pbt) pI');
1.380 - val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
1.381 + else istate_;
1.382 + val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1.383 (oris,(dI',pI',mI'),e_term);
1.384 val {ppc,prls,where_,...} = get_pbt pI'
1.385 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1.386 @@ -1317,7 +1292,7 @@
1.387 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1.388 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.389 val cpI = if pI = e_pblID then pI' else pI;
1.390 - in case appl_add thy sel oris pbl ((#ppc o get_pbt) cpI) ct of
1.391 + in case appl_add (thy2ctxt thy) sel oris pbl ((#ppc o get_pbt) cpI) ct of
1.392 Add itm (*..union old input *) =>
1.393 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1.394 *)
1.395 @@ -1350,7 +1325,7 @@
1.396 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.397 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.398 val cmI = if mI = e_metID then mI' else mI;
1.399 - in case appl_add thy sel oris met ((#ppc o get_met) cmI) ct of
1.400 + in case appl_add (thy2ctxt thy) sel oris met ((#ppc o get_met) cmI) ct of
1.401 Add itm (*..union old input *) =>
1.402 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1.403 *)
1.404 @@ -1579,7 +1554,7 @@
1.405 val thy = assoc_thy dI
1.406 val mI = if mI = [] then hd met else mI
1.407 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1.408 - val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1.409 + val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1.410 ([], (dI,pI,mI), hdl)
1.411 val pt = update_spec pt [] (dI,pI,mI)
1.412 val pits = init_pbl' ppc
1.413 @@ -1588,12 +1563,12 @@
1.414 else if mI <> [] then (* from met-browser *)
1.415 let val {ppc,...} = get_met mI
1.416 val dI = if dI = "" then "Isac" else dI
1.417 - val thy = assoc_thy dI
1.418 - val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1.419 - ([], (dI,pI,mI), e_term(*FIXME met*))
1.420 - val pt = update_spec pt [] (dI,pI,mI)
1.421 - val mits = init_pbl' ppc
1.422 - val pt = update_met pt [] mits
1.423 + val thy = assoc_thy dI;
1.424 + val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1.425 + ([], (dI,pI,mI), e_term(*FIXME met*));
1.426 + val pt = update_spec pt [] (dI,pI,mI);
1.427 + val mits = init_pbl' ppc;
1.428 + val pt = update_met pt [] mits;
1.429 in ((pt, ([], Met)), []) : calcstate end
1.430 else (* new example, pepare for interactive modeling *)
1.431 let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1.432 @@ -1604,18 +1579,19 @@
1.433 val thy = assoc_thy dI
1.434 val (pI, pors, mI) =
1.435 if mI = ["no_met"]
1.436 - then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI)
1.437 + then let val pors = get_pbt pI |> #ppc |> prep_ori fmz thy |> #1;
1.438 val pI' = refine_ori' pors pI;
1.439 in (pI', pors(*refinement over models with diff.precond only*),
1.440 (hd o #met o get_pbt) pI') end
1.441 - else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI)
1.442 + else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy |> #1, mI)
1.443 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1.444 val dI = theory2theory' (maxthy thy thy');
1.445 + val ctxt = prep_ori fmz thy ppc |> #2;
1.446 val hdl = case cas of
1.447 NONE => pblterm dI pI
1.448 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1.449 - ~~~ vals_of_oris pors) t
1.450 - val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
1.451 + ~~~ vals_of_oris pors) t;
1.452 + val (pt, _) = cappend_problem e_ptree [] (Uistate, ctxt) (fmz, (dI, pI, mI))
1.453 (pors, (dI, pI, mI), hdl)
1.454 in ((pt, ([], Pbl)),
1.455 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1.456 @@ -1814,7 +1790,7 @@
1.457 ...}) = get_obj I pt p;
1.458 val thy = assoc_thy dI;
1.459 val {ppc,...} = get_met mI;
1.460 - val mors = prep_ori fmz_ thy ppc;
1.461 + val mors = prep_ori fmz_ thy ppc |> #1;
1.462 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1.463 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1.464 val pt = update_spec pt p (dI,pI,mI);
2.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Mar 21 00:32:53 2011 +0100
2.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Apr 04 11:05:07 2011 +0200
2.3 @@ -226,7 +226,7 @@
2.4 fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) =
2.5 (* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl;
2.6 *)
2.7 - (let val t = (comp_dts (Isac "delay")) (d,ts);
2.8 + (let val t = comp_dts (d,ts);
2.9 val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
2.10 (*this ^ should raise the exn on unability of re-parsing dts*)
2.11 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
2.12 @@ -237,12 +237,12 @@
2.13 (let val t = (term_of o the o (parse dI)) str
2.14 in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
2.15 | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
2.16 - (let val t = (comp_dts (Isac "delay")) (d,ts);
2.17 + (let val t = comp_dts (d,ts);
2.18 val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
2.19 (*this ^ should raise the exn on unability of re-parsing dts*)
2.20 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
2.21 | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
2.22 - (let val t = (comp_dts (Isac"delay" )) (d,ts);
2.23 + (let val t = comp_dts (d,ts);
2.24 val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t;
2.25 (*this ^ should raise the exn on unability of re-parsing dts*)
2.26 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
2.27 @@ -279,27 +279,17 @@
2.28 *)
2.29 fun appl_add' dI oris ppc pbt (sel, ct) =
2.30 let
2.31 - val thy = assoc_thy dI;
2.32 - in case parse thy ct of
2.33 + val ctxt = assoc_thy dI |> thy2ctxt;
2.34 + in case parseNEW ctxt ct of
2.35 NONE => (0,[],false,sel, Syn ct):itm
2.36 - | SOME ct => (* val SOME ct = parse thy ct;
2.37 - *)
2.38 - (case is_known thy sel oris (term_of ct) of
2.39 - (* val ("",ori'(*ts='ct'*), all) = is_known thy sel oris (term_of ct);
2.40 - *)
2.41 - ("",ori'(*ts='ct'*), all) =>
2.42 - (case is_notyet_input thy ppc all ori' pbt of
2.43 - (* val ("",itm) = is_notyet_input thy ppc all ori' pbt;
2.44 - *)
2.45 - ("",itm) => itm
2.46 - (* val (msg,xx) = is_notyet_input thy ppc all ori' pbt;
2.47 - *)
2.48 - | (msg,_) => error ("appl_add': "^msg))
2.49 - (* val (msg,(_,_,_,d,ts),all) = is_known thy sel oris (term_of ct);
2.50 - *)
2.51 - | (msg,(i,v,_,d,ts),_) =>
2.52 - if is_e_ts ts then (i,v,false, sel, Inc ((d,ts),(e_term,[])))
2.53 - else (i,v,false,sel, Sup (d,ts)))
2.54 + | SOME t => (case is_known ctxt sel oris t of
2.55 + ("", ori', all) =>
2.56 + (case is_notyet_input ctxt ppc all ori' pbt of
2.57 + ("",itm) => itm
2.58 + | (msg,_) => error ("appl_add': " ^ msg))
2.59 + | (_, (i, v, _, d, ts), _) => if is_e_ts ts then
2.60 + (i, v, false, sel, Inc ((d, ts), (e_term, []))) else
2.61 + (i, v, false, sel, Sup (d, ts)))
2.62 end;
2.63
2.64 (*.generate preliminary itm_ from a strin (with field "#Given" etc.).*)
2.65 @@ -313,7 +303,7 @@
2.66 | SOME ct =>
2.67 (* val SOME ct = parse thy str;
2.68 *)
2.69 - let val (d,ts) = ((split_dts thy) o term_of) ct
2.70 + let val (d,ts) = (split_dts o term_of) ct
2.71 val popt = find_first (eq7 (f,d)) pbt
2.72 in case popt of
2.73 NONE => ([1](*??*), true(*??*), f, Sup (d,ts))
2.74 @@ -453,7 +443,7 @@
2.75 let val pbt = (#ppc o get_pbt) pI
2.76 val dI' = #1 (some_spec ospec spec)
2.77 val oris = if pI = #2 ospec then oris
2.78 - else prep_ori fmz_(assoc_thy"Isac") pbt;
2.79 + else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
2.80 in (Pbl, appl_adds dI' oris probl pbt
2.81 (map itms2fstr probl), meth) end else
2.82 if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
3.1 --- a/src/Tools/isac/Interpret/mstools.sml Mon Mar 21 00:32:53 2011 +0100
3.2 +++ b/src/Tools/isac/Interpret/mstools.sml Mon Apr 04 11:05:07 2011 +0200
3.3 @@ -75,7 +75,7 @@
3.4 val pres2str : (bool * term) list -> string
3.5 (* val evalprecond : rls -> term -> bool * term *)
3.6 (* val cnt : itm list -> int -> int * int *)
3.7 - val comp_dts : theory -> term * term list -> term
3.8 + val comp_dts : term * term list -> term
3.9 val comp_dts' : term * term list -> term
3.10 val comp_dts'' : term * term list -> string
3.11 val comp_ts : term * term list -> term
3.12 @@ -116,7 +116,7 @@
3.13 val mkval' : term list -> term
3.14 (* val pblID_of_match : match -> pblID *)
3.15 val pbl_ids : Proof.context -> term -> term -> term list
3.16 - val pbl_ids' : 'a -> term -> term list -> term list
3.17 + val pbl_ids' : term -> term list -> term list
3.18 (* val pen2str : theory -> term * term list -> string *)
3.19 val penvval_in : itm_ -> term list
3.20 val refined : match list -> pblID
3.21 @@ -124,7 +124,7 @@
3.22 match_ list -> match_ option
3.23 (* val refined_IDitms :
3.24 match list -> match option *)
3.25 - val split_dts : 'a -> term -> term * term list
3.26 + val split_dts : term -> term * term list
3.27 val split_dts' : term * term -> term list
3.28 (* val take_apart : term -> term list *)
3.29 (* val take_apart_inv : term list -> term *)
3.30 @@ -206,18 +206,18 @@
3.31 (if is_reall_dsc d then (d $ e_listReal)
3.32 else if is_booll_dsc d then (d $ e_listBool)
3.33 else d)
3.34 - | comp_dts thy (d,ts) =
3.35 + | comp_dts (d,ts) =
3.36 (cterm_of (*(sign_of o assoc_thy) "Isac"*)
3.37 (Thy_Info.get_theory "Isac")
3.38 (*comp_dts:FIXXME stay with term for efficiency !!*)
3.39 (d $ (comp_ts (d, ts)))
3.40 handle _ => error ("comp_dts: "^(term2str d)^
3.41 " $ "^(term2str (hd ts))));*)
3.42 -fun comp_dts thy (d,[]) =
3.43 +fun comp_dts (d,[]) =
3.44 (if is_reall_dsc d then (d $ e_listReal)
3.45 else if is_booll_dsc d then (d $ e_listBool)
3.46 else d)
3.47 - | comp_dts thy (d,ts) =
3.48 + | comp_dts (d,ts) =
3.49 (d $ (comp_ts (d, ts)))
3.50 handle _ => error ("comp_dts: "^(term2str d)^
3.51 " $ "^(term2str (hd ts)));
3.52 @@ -323,7 +323,7 @@
3.53 term * description
3.54 term list * lists decomposed for elementwise input
3.55 term list pbl_ids not _HERE_: dont know which list-elems input*)
3.56 -fun split_dts thy (t as d $ arg) =
3.57 +fun split_dts (t as d $ arg) =
3.58 if is_dsc d
3.59 then if is_list_dsc d
3.60 then if is_list arg
3.61 @@ -333,11 +333,23 @@
3.62 else (d, [arg]) (*a variable or metavariable for a list*)
3.63 else (d, [arg])
3.64 else (e_term, dest_list' t(*9.01 ???*))
3.65 - | split_dts thy t = (*either dsc or term*)
3.66 + | split_dts t = (*either dsc or term*)
3.67 let val (h,argl) = strip_comb t
3.68 in if (not o is_dsc) h then (e_term, dest_list' t)
3.69 else (h, dest_list (h,argl))
3.70 end;
3.71 +(*fun split_dts (t as d $ arg) =
3.72 + if is_dsc d then
3.73 + if is_list_dsc d andalso is_list arg andalso is_unl d |> not then
3.74 + (d, take_apart arg) else
3.75 + (d, [arg]) else
3.76 + (e_term, dest_list' t)
3.77 + | split_dts t =
3.78 + let val t' as (h, _) = strip_comb t;
3.79 + in if is_dsc h then
3.80 + (h, dest_list t') else
3.81 + (e_term, dest_list' t)
3.82 + end;*)
3.83 (* tests see fun comp_dts
3.84
3.85 > val t = str2term "someList []";
3.86 @@ -654,7 +666,7 @@
3.87 | pbl_ids' _ vs =
3.88 error ("pbl_ids': not implemented for " ^ terms2str vs);
3.89 (*9.5.03 penv postponed: pbl_ids'*)
3.90 -fun pbl_ids' thy d vs = [comp_ts (d, vs)];
3.91 +fun pbl_ids' d vs = [comp_ts (d, vs)];
3.92
3.93
3.94 (*14.9.01: not used after putting values for penv into itm_
3.95 @@ -796,17 +808,17 @@
3.96 (*make string for error-msgs*)
3.97 fun itm_2str_ ctxt (Cor ((d,ts), penv)) =
3.98 "Cor " ^
3.99 - Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts ctxt (d,ts)) ^
3.100 + Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)) ^
3.101 " ," ^ pen2str ctxt penv
3.102 | itm_2str_ ctxt (Syn c) = "Syn " ^ c
3.103 | itm_2str_ ctxt (Typ c) = "Typ " ^ c
3.104 | itm_2str_ ctxt (Inc ((d,ts), penv)) =
3.105 "Inc " ^
3.106 - Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts ctxt (d,ts)) ^
3.107 + Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)) ^
3.108 " ," ^ pen2str ctxt penv
3.109 | itm_2str_ ctxt (Sup (d,ts)) =
3.110 "Sup " ^
3.111 - Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts ctxt (d,ts))
3.112 + Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts))
3.113 | itm_2str_ ctxt (Mis (d,pid))=
3.114 "Mis "^ Print_Mode.setmp [] (Syntax.string_of_term ctxt) d ^
3.115 " " ^ Print_Mode.setmp [] (Syntax.string_of_term ctxt) pid
4.1 --- a/src/Tools/isac/Interpret/ptyps.sml Mon Mar 21 00:32:53 2011 +0100
4.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Mon Apr 04 11:05:07 2011 +0200
4.3 @@ -15,13 +15,13 @@
4.4 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
4.5
4.6 fun itm_2item thy (Cor ((d,ts),_)) =
4.7 - Correct (term2str (comp_dts thy (d,ts)))
4.8 + Correct (term2str (comp_dts (d,ts)))
4.9 | itm_2item _ (Syn c) = SyntaxE c
4.10 | itm_2item _ (Typ c) = TypeE c
4.11 | itm_2item thy (Inc ((d,ts),_)) =
4.12 - Incompl (term2str (comp_dts thy (d,ts)))
4.13 + Incompl (term2str (comp_dts (d,ts)))
4.14 | itm_2item thy (Sup (d,ts)) =
4.15 - Superfl (term2str (comp_dts thy (d,ts)))
4.16 + Superfl (term2str (comp_dts (d,ts)))
4.17 | itm_2item _ (Mis (d,pid)) =
4.18 Missing (term2str d ^ " " ^ term2str pid);
4.19
4.20 @@ -132,11 +132,11 @@
4.21
4.22
4.23 (*create output-string for itm_*)
4.24 -fun itm_out thy (Cor ((d,ts),_)) = term2str (comp_dts thy(d,ts))
4.25 +fun itm_out thy (Cor ((d,ts),_)) = term2str (comp_dts (d,ts))
4.26 | itm_out thy (Syn c) = c
4.27 | itm_out thy (Typ c) = c
4.28 - | itm_out thy (Inc ((d,ts),_)) = term2str (comp_dts thy(d,ts))
4.29 - | itm_out thy (Sup (d,ts)) = term2str (comp_dts thy(d,ts))
4.30 + | itm_out thy (Inc ((d,ts),_)) = term2str (comp_dts (d,ts))
4.31 + | itm_out thy (Sup (d,ts)) = term2str (comp_dts (d,ts))
4.32 | itm_out thy (Mis (d,pid)) = term2str d ^ " " ^ term2str pid;
4.33
4.34 fun boolterm2item (true, term) = Correct (term2str term)
4.35 @@ -274,23 +274,23 @@
4.36 val (thy,pbt) = (assoc_thy dI',(#ppc o get_pbt) pI');
4.37 val (fmz, thy, pbt) = (fmz, thy, ((#ppc o get_pbt) pI));
4.38 *)
4.39 -fun prep_ori [] _ _ = []
4.40 +fun prep_ori [] _ _ = ([], e_ctxt)
4.41 | prep_ori fmz thy pbt =
4.42 - let
4.43 - val ctopts = map (parse thy) fmz
4.44 - val _= (*FIXME.WN060916 improve error report*)
4.45 - if null (filter is_none ctopts) then ()
4.46 - else error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz)
4.47 - val dts = map ((split_dts thy) o term_of o the) ctopts
4.48 - val ori = map (add_field thy pbt) dts;
4.49 -(* val ori = map (flat3 o (pair "#undef")) dts; *)
4.50 - val ori' = add_variants ori;
4.51 - val maxv = max (map fst ori');
4.52 - val maxv = if maxv = 0 then 1(*only 1 variant*) else maxv;
4.53 - val ori'' = coll_variants ori';
4.54 - val ori''' = map (apfst (replace_0 maxv)) ori'';
4.55 - val ori'''' = add_id ori'''
4.56 - in (map flattup ori''''):ori list end;
4.57 + let
4.58 + val ctxt = ProofContext.init_global thy
4.59 + |> fold declare_constraints fmz;
4.60 + fun checked_parseNEW t = case parseNEW ctxt t of
4.61 + NONE => error ("prep_ori: SYNTAX ERROR in " ^ t)
4.62 + | SOME t' => t';
4.63 + val ori = map (add_field thy pbt o split_dts o checked_parseNEW) fmz
4.64 + |> add_variants;
4.65 + val maxv = map fst ori |> max;
4.66 + val maxv = if maxv = 0 then 1 else maxv;
4.67 + val oris = coll_variants ori
4.68 + |> map (replace_0 maxv |> apfst)
4.69 + |> add_id
4.70 + |> map flattup;
4.71 + in (oris, ctxt) end;
4.72
4.73
4.74 (*-----------------------------------------^^^-(4) aus modspec.sml 23.3.02*)
4.75 @@ -827,12 +827,12 @@
4.76 fun chk_ thy pbt ((i,vats,b,f,Cor ((d,vs),_)):itm) =
4.77 (case find_first (eq1 d) pbt of
4.78 SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
4.79 - (id, pbl_ids' thy d vs))):itm)
4.80 + (id, pbl_ids' d vs))):itm)
4.81 | NONE => (i,vats,false,f,Sup (d,vs)))
4.82 | chk_ thy pbt ((i,vats,b,f,Inc ((d,vs),_)):itm) =
4.83 (case find_first (eq1 d) pbt of
4.84 SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
4.85 - (id, pbl_ids' thy d vs))):itm)
4.86 + (id, pbl_ids' d vs))):itm)
4.87 | NONE => (i,vats,false,f,Sup (d,vs)))
4.88
4.89 | chk_ thy pbt (itm as (i,vats,b,f,Syn ct):itm) = itm
4.90 @@ -841,7 +841,7 @@
4.91 | chk_ thy pbt ((i,vats,b,f,Sup (d,vs)):itm) =
4.92 (case find_first (eq1 d) pbt of
4.93 SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
4.94 - (id, pbl_ids' thy d vs))):itm)
4.95 + (id, pbl_ids' d vs))):itm)
4.96 | NONE => (i,vats,false,f,Sup (d,vs)))
4.97 (* val (i,vats,b,f,Mis (d,vs)) = i4;
4.98 *)
4.99 @@ -948,7 +948,7 @@
4.100 fun chk1_ thy pbt ((i,vats,f,d,vs):ori) =
4.101 case find_first (eq1 d) pbt of
4.102 SOME (_,(_,id)) => [(i,vats,true,f,
4.103 - Cor ((d,vs), (id, pbl_ids' thy d vs))):itm]
4.104 + Cor ((d,vs), (id, pbl_ids' d vs))):itm]
4.105 | NONE => [];
4.106
4.107 (* elem 'p' of pbt contained in itms ? *)
4.108 @@ -1034,7 +1034,7 @@
4.109
4.110 (*. match a formalization with a problem type .*)
4.111 fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) =
4.112 - let val oris = prep_ori fmz thy ppc;
4.113 + let val oris = prep_ori fmz thy ppc |> #1;
4.114 val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er);
4.115 in if bool then Matches' (itms2itemppc thy itms pre')
4.116 else NoMatch' (itms2itemppc thy itms pre') end;
4.117 @@ -1081,7 +1081,7 @@
4.118 *)
4.119 let val _ = (tracing o ((curry op^)"*** pass ") o strs2str)(pblRD @ [pI])
4.120 val {thy,ppc,where_,prls,...} = py
4.121 - val oris = prep_ori fmz thy ppc
4.122 + val oris = prep_ori fmz thy ppc |> #1;
4.123 (*8.3.02: itms!: oris ev. are _not_ complete here*)
4.124 val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls)
4.125 in if b then pbls @ [Matches (rev (pblRD @ [pI]),
4.126 @@ -1096,7 +1096,7 @@
4.127 | refin' pblRD fmz pbls (Ptyp (pI,[py],pys)) =
4.128 let val _ = (tracing o ((curry op^)"*** pass ") o strs2str) (pblRD @ [pI])
4.129 val {thy,ppc,where_,prls,...} = py
4.130 - val oris = prep_ori fmz thy ppc;
4.131 + val oris = prep_ori fmz thy ppc |> #1;
4.132 (*8.3.02: itms!: oris ev. are _not_ complete here*)
4.133 val(b, (itms, pre')) = match_oris' thy oris (ppc,where_,prls);
4.134 in if b
5.1 --- a/src/Tools/isac/ProgLang/termC.sml Mon Mar 21 00:32:53 2011 +0100
5.2 +++ b/src/Tools/isac/ProgLang/termC.sml Mon Apr 04 11:05:07 2011 +0200
5.3 @@ -1062,7 +1062,8 @@
5.4 *** Free ( R, RealDef.real) *)
5.5
5.6 (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
5.7 -fun parseNEW ctxt str = Syntax.read_term ctxt str |> numbers_to_string;
5.8 +fun parseNEW ctxt str = SOME (Syntax.read_term ctxt str |> numbers_to_string)
5.9 + handle _ => NONE;
5.10
5.11 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation*)
5.12 fun parse_patt thy str = (thy, str) |>> thy2ctxt
6.1 --- a/src/Tools/isac/Test_Isac.thy Mon Mar 21 00:32:53 2011 +0100
6.2 +++ b/src/Tools/isac/Test_Isac.thy Mon Apr 04 11:05:07 2011 +0200
6.3 @@ -15,7 +15,12 @@
6.4 representation of terms and thus break some tests.
6.5 *)
6.6
6.7 -theory Test_Isac imports "Knowledge/Isac" begin
6.8 +theory Test_Isac imports
6.9 + "Knowledge/Isac"
6.10 + "../../../test/Pure/General/Basics"
6.11 + "../../../test/Pure/Isar/Test_Parse_Term" (*part.*)
6.12 + "../../../test/Pure/Isar/Test_Parsers"
6.13 +begin
6.14
6.15 ML{* writeln "**** run the tests **************************************" *}
6.16 ML {* Toplevel.debug := true; *}
6.17 @@ -42,7 +47,7 @@
6.18 cd"smltest/Scripts";
6.19 *)
6.20 use"../../../test/Tools/isac/ProgLang/termC.sml" (*part.*)
6.21 -ML {*print_depth 9*}
6.22 +ML {*print_depth 90*}
6.23 use"../../../test/Tools/isac/ProgLang/calculate.sml" (*part.*)
6.24
6.25 ML {*store_met*}
6.26 @@ -55,6 +60,7 @@
6.27 cd "../..";
6.28 cd"smltest/ME";
6.29 *)
6.30 +
6.31 use "../../../test/Tools/isac/Interpret/mstools.sml" (*empty*)
6.32 use "../../../test/Tools/isac/Interpret/ctree.sml" (*part.*)
6.33 use "../../../test/Tools/isac/Interpret/ptyps.sml" (*TODO*)
6.34 @@ -64,7 +70,7 @@
6.35 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
6.36 use"inform.sml";
6.37 *)
6.38 -ML {*print_depth 5*}
6.39 +ML {*print_depth 300*}
6.40 use "../../../test/Tools/isac/Interpret/mathengine.sml" (*part.+110310*)
6.41 ML {**}
6.42 (*
6.43 @@ -159,10 +165,6 @@
6.44 use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
6.45 *)
6.46 use "../../../test/Pure/library.sml" (**)
6.47 -use_thy "../../../test/Pure/General/Basics"
6.48 -
6.49 -use_thy "../../../test/Pure/Isar/Test_Parse_Term" (*part.*)
6.50 -use_thy "../../../test/Pure/Isar/Test_Parsers"
6.51
6.52 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *}
6.53 (*
7.1 --- a/test/Pure/Isar/Test_Parse_Term.thy Mon Mar 21 00:32:53 2011 +0100
7.2 +++ b/test/Pure/Isar/Test_Parse_Term.thy Mon Apr 04 11:05:07 2011 +0200
7.3 @@ -42,8 +42,8 @@
7.4
7.5
7.6 section {* decompose term *}
7.7 +ML {*
7.8 (*========== inhibit exn 110314 ================================================
7.9 -ML {*
7.10 "---from src/Pure/Isar/token.ML ----------------------------------------------";
7.11 datatype value =
7.12 Text of string | Typ of typ | Term of term | Fact of thm list | Attribute of morphism -> attribute;
7.13 @@ -89,7 +89,7 @@
7.14 (*fn : Token.T list -> string * Token.T list*)
7.15 val term = inner_syntax term_group;
7.16 (*fn : Token.T list -> string * Token.T list*)
7.17 +============ inhibit exn 110314 ==============================================*)
7.18 *}
7.19 -============ inhibit exn 110314 ==============================================*)
7.20
7.21 end
7.22 \ No newline at end of file
8.1 --- a/test/Tools/isac/Frontend/interface.sml Mon Mar 21 00:32:53 2011 +0100
8.2 +++ b/test/Tools/isac/Frontend/interface.sml Mon Apr 04 11:05:07 2011 +0200
8.3 @@ -88,7 +88,7 @@
8.4 "--------- solve_linear as rootpbl FE -------------------";
8.5 states := [];
8.6 CalcTree (*start of calculation, return No.1*)
8.7 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
8.8 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
8.9 ("Test",
8.10 ["linear","univariate","equation","test"],
8.11 ["Test","solve_linear"]))];
9.1 --- a/test/Tools/isac/Interpret/ctree.sml Mon Mar 21 00:32:53 2011 +0100
9.2 +++ b/test/Tools/isac/Interpret/ctree.sml Mon Apr 04 11:05:07 2011 +0200
9.3 @@ -64,17 +64,17 @@
9.4 "this build should be detailed each time a test fails later \
9.5 \i.e. all the tests should be caught here first \
9.6 \and linked with a reference to the respective test environment";
9.7 -val fmz = ["equality (x+1=2)",
9.8 - "solveFor x","solutions L"];
9.9 +val fmz = ["equality (x+1=(2::int))",
9.10 + "solveFor (x::int)","solutions L"];
9.11 val (dI',pI',mI') =
9.12 ("Test",["sqroot-test","univariate","equation","test"],
9.13 ["Test","squ-equ-test-subpbl1"]);
9.14 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.15 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.16 +val (p,_,f,(nxt,tacx),_,pt) = me nxt p [1] pt;
9.17 (* nxt = Add_Given "equality (x + 1 = 2)"
9.18 (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
9.19 *)
9.20 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.21 +val (p,_,f,nxt,_,pt) = me (nxt,tacx) p [1] pt;
9.22 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
9.23 *)
9.24 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.25 @@ -92,7 +92,7 @@
9.26 "ctree.sml-------------- cut_tree new (from ptree above)----------";
9.27 val (pt', cuts) = cut_tree pt ([1],Frm);
9.28 "ctree.sml-------------- cappend on complete ctree from above ----";
9.29 -val (pt', cuts) = cappend_form pt [1] e_istate (str2term "Inform[1]");
9.30 +val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]");
9.31 "----------------------------------------------------------------/";
9.32 (*========== inhibit exn WN110319 ==============================================
9.33 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
10.1 --- a/test/Tools/isac/Interpret/mathengine.sml Mon Mar 21 00:32:53 2011 +0100
10.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Mon Apr 04 11:05:07 2011 +0200
10.3 @@ -36,7 +36,7 @@
10.4 val ctxt = ProofContext.init_global thy;
10.5
10.6 val ctopts = map (parse thy) fmz;
10.7 - val dts = map ((split_dts thy) o term_of o the) ctopts;
10.8 + val dts = map (split_dts o term_of o the) ctopts;
10.9 (*split_dts:
10.10 (term * term list) list
10.11 formulas: e.g. ((1+2)*4/3)^^^2
10.12 @@ -114,13 +114,13 @@
10.13 loc_solve_ (mI,m) ptp;
10.14 val (m, (pt, pos)) = ((mI,m), ptp);
10.15 solve m (pt, pos);
10.16 - val ((_, m as Apply_Method' (mI, _, _)), (pt, (pos as (p,_)))) =
10.17 + val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
10.18 (m, (pt, pos));
10.19 val {srls,...} = get_met mI;
10.20 val PblObj{meth=itms,...} = get_obj I pt p;
10.21 val thy' = get_obj g_domID pt p;
10.22 val thy = assoc_thy thy';
10.23 - val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI;
10.24 + val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
10.25
10.26 "----- go on in the calculation";
10.27 val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;
11.1 --- a/test/Tools/isac/Interpret/mstools.sml Mon Mar 21 00:32:53 2011 +0100
11.2 +++ b/test/Tools/isac/Interpret/mstools.sml Mon Apr 04 11:05:07 2011 +0200
11.3 @@ -20,7 +20,9 @@
11.4 "----------- fun declare_constraints --------------------";
11.5 val ctxt = ProofContext.init_global @{theory}
11.6 |> declare_constraints "xxx + yyy = (111::int)";
11.7 -val t = parseNEW ctxt "xxx = 123";
11.8 +val t = case parseNEW ctxt "xxx = 123" of
11.9 + NONE => error "mstools: syntax error"
11.10 + | SOME t' => t';
11.11 if ((lhs t) |> type_of) = @{typ int} then ()
11.12 else error "mstools: incorrect type inference from parseNEW ctxt";
11.13
12.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Mon Mar 21 00:32:53 2011 +0100
12.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Mon Apr 04 11:05:07 2011 +0200
12.3 @@ -26,8 +26,15 @@
12.4 "----------- rewriting for usecase1 ---------------------";
12.5 "----------- rewriting for usecase1 ---------------------";
12.6 "----------- rewriting for usecase1 ---------------------";
12.7 -val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int")];
12.8 -val t = parseNEW ctxt "xxx + 111 = abc + (123::int)";
12.9 +val subst = let
12.10 + val pair = (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int");
12.11 + in case pair of
12.12 + (SOME r, SOME s) => [(r,s)]
12.13 + | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
12.14 + end;
12.15 +val t = case parseNEW ctxt "xxx + 111 = abc + (123::int)" of
12.16 + SOME t' => t'
12.17 + | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
12.18
12.19 val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst
12.20 (num_str @{thm "int_isolate_add"}) t; term2str t;
12.21 @@ -63,7 +70,9 @@
12.22 val thy = @{theory "Test"};
12.23 "----------- rewriting for usecase2 ---------------------";
12.24
12.25 -val t = parseNEW ctxt "xxx + abc + -1 * 111 + (123::int)";
12.26 +val t = case parseNEW ctxt "xxx + abc + -1 * 111 + (123::int)" of
12.27 + SOME t' => t'
12.28 + | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
12.29
12.30 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
12.31 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
13.1 --- a/test/Tools/isac/Knowledge/integrate.sml Mon Mar 21 00:32:53 2011 +0100
13.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Mon Apr 04 11:05:07 2011 +0200
13.3 @@ -7,6 +7,7 @@
13.4 use"integrate.sml";
13.5 *)
13.6 val thy = @{theory "Integrate"};
13.7 +val ctxt = thy2ctxt thy;
13.8
13.9 "--------------------------------------------------------";
13.10 "table of contents --------------------------------------";
13.11 @@ -35,9 +36,10 @@
13.12 "----------- parsing ------------------------------------";
13.13 "----------- parsing ------------------------------------";
13.14 "----------- parsing ------------------------------------";
13.15 -fun str2term str = (term_of o the o (parse thy)) str;
13.16 +fun str2term str = parseNEW ctxt str |> the;
13.17 +
13.18 fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term
13.19 - (ProofContext.init_global thy)) t;
13.20 + ctxt) t;
13.21
13.22 val t = str2term "Integral x D x";
13.23 val t = str2term "Integral x^^^2 D x";
14.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Mar 21 00:32:53 2011 +0100
14.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Apr 04 11:05:07 2011 +0200
14.3 @@ -366,7 +366,7 @@
14.4 "----------- pbl polynom probe -----------------------------------";
14.5 "----------- pbl polynom probe -----------------------------------";
14.6 states:=[];
14.7 -CalcTree [(["Pruefe (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\
14.8 +CalcTree [(["Pruefe ((5::int)*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\
14.9 \3 - 2 * e + 2 * f + 2 * g)",
14.10 "mitWert [e = 1, f = 2, g = 3]",
14.11 "Geprueft b"],