1.1 --- a/src/Tools/isac/Interpret/inform.sml Thu May 05 09:23:32 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu May 05 14:21:54 2011 +0200
1.3 @@ -395,79 +395,57 @@
1.4 "): Par should be internal");
1.5
1.6 fun imodel2fstr iitems =
1.7 - let fun xxx is [] = is
1.8 - | xxx is ((Given strs)::iis) =
1.9 - xxx (is @ (map (pair "#Given") strs)) iis
1.10 - | xxx is ((Find strs)::iis) =
1.11 - xxx (is @ (map (pair "#Find") strs)) iis
1.12 - | xxx is ((Relate strs)::iis) =
1.13 - xxx (is @ (map (pair "#Relate") strs)) iis
1.14 - in xxx [] iitems end;
1.15 + let
1.16 + fun xxx is [] = is
1.17 + | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
1.18 + | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
1.19 + | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
1.20 + in xxx [] iitems end;
1.21
1.22 -(*.input a CAS-command via a whole calchead;
1.23 - dWN0602 ropped due to change of design in the front-end.*)
1.24 -(*since previous calc-head _only_ has changed:
1.25 - EITHER _1_ part of the specification OR some items in the model;
1.26 - the hdform is left as is except in cas_input .*)
1.27 -(*FIXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX___Met___XXXXXXXXXXXME.TODO.WN:11.03*)
1.28 -(* val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
1.29 - (p, "xxx", empty_model, Pbl, e_spec);
1.30 - val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
1.31 - (p,"", [Given ["fixedValues [r=Arbfix]"],
1.32 - Find ["maximum A", "valuesFor [a,b]"],
1.33 - Relate ["relations [A=a*b, a/2=r*sin alpha, \
1.34 - \b/2=r*cos alpha]"]], Pbl, e_spec);
1.35 - val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
1.36 - (([],Pbl), "not used here",
1.37 - [Given ["fixedValues [r=Arbfix]"],
1.38 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.39 - Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl,
1.40 - ("DiffApp", ["e_pblID"], ["e_metID"]));
1.41 - val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = ichd;
1.42 - *)
1.43 +(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
1.44 fun input_icalhd pt (((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)):icalhd) =
1.45 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1.46 - spec = sspec as (sdI,spI,smI), probl, meth,...} =
1.47 - get_obj I pt p;
1.48 + spec = sspec as (sdI,spI,smI), probl, meth,...} = get_obj I pt p;
1.49 in if is_casinput hdf fmz then the (cas_input (str2term hdf))
1.50 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
1.51 - let val (pos_, pits, mits) =
1.52 - if dI <> sdI
1.53 - then let val its = map (parsitm (assoc_thy dI)) probl;
1.54 - val (its, trms) = filter_sep is_Par its;
1.55 - val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec));
1.56 - in (Pbl, appl_adds dI oris its pbt
1.57 - (map par2fstr trms), meth) end else
1.58 - if pI <> spI
1.59 - then if pI = snd3 ospec then (Pbl, probl, meth) else
1.60 - let val pbt = (#ppc o get_pbt) pI
1.61 - val dI' = #1 (some_spec ospec spec)
1.62 - val oris = if pI = #2 ospec then oris
1.63 - else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
1.64 - in (Pbl, appl_adds dI' oris probl pbt
1.65 - (map itms2fstr probl), meth) end else
1.66 - if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
1.67 - then let val met = (#ppc o get_met) mI
1.68 - val mits = complete_metitms oris probl meth met
1.69 - in if foldl and_ (true, map #3 mits)
1.70 - then (Pbl, probl, mits) else (Met, probl, mits)
1.71 - end else
1.72 - (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)]
1.73 - ((#ppc o get_pbt) (#2 (some_spec ospec spec)))
1.74 - (imodel2fstr imodel), meth);
1.75 - val pt = update_spec pt p spec;
1.76 - in if pos_ = Pbl
1.77 - then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
1.78 - val pre =check_preconds(assoc_thy"Isac")prls where_ pits
1.79 - in (update_pbl pt p pits,
1.80 - (ocalhd_complete pits pre spec,
1.81 - Pbl, hdf', pits, pre, spec):ocalhd) end
1.82 - else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
1.83 - val pre = check_preconds (assoc_thy"Isac") prls pre mits
1.84 - in (update_met pt p mits,
1.85 - (ocalhd_complete mits pre spec,
1.86 - Met, hdf', mits, pre, spec):ocalhd) end
1.87 - end end
1.88 + let val (pos_, pits, mits) =
1.89 + if dI <> sdI
1.90 + then let val its = map (parsitm (assoc_thy dI)) probl;
1.91 + val (its, trms) = filter_sep is_Par its;
1.92 + val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec));
1.93 + in (Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
1.94 + else if pI <> spI
1.95 + then if pI = snd3 ospec then (Pbl, probl, meth)
1.96 + else
1.97 + let val pbt = (#ppc o get_pbt) pI
1.98 + val dI' = #1 (some_spec ospec spec)
1.99 + val oris = if pI = #2 ospec then oris
1.100 + else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
1.101 + in (Pbl, appl_adds dI' oris probl pbt
1.102 + (map itms2fstr probl), meth) end
1.103 + else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
1.104 + then let val met = (#ppc o get_met) mI
1.105 + val mits = complete_metitms oris probl meth met
1.106 + in if foldl and_ (true, map #3 mits)
1.107 + then (Pbl, probl, mits) else (Met, probl, mits)
1.108 + end
1.109 + else (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)]
1.110 + ((#ppc o get_pbt) (#2 (some_spec ospec spec)))
1.111 + (imodel2fstr imodel), meth);
1.112 + val pt = update_spec pt p spec;
1.113 + in if pos_ = Pbl
1.114 + then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
1.115 + val pre =check_preconds(assoc_thy"Isac")prls where_ pits
1.116 + in (update_pbl pt p pits,
1.117 + (ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec):ocalhd)
1.118 + end
1.119 + else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
1.120 + val pre = check_preconds (assoc_thy"Isac") prls pre mits
1.121 + in (update_met pt p mits,
1.122 + (ocalhd_complete mits pre spec, Met, hdf', mits, pre, spec):ocalhd)
1.123 + end
1.124 + end
1.125 + end
1.126 | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) =
1.127 error "input_icalhd Met not impl.";
1.128