1.1 --- a/src/Tools/isac/Interpret/calchead.sml Sun May 15 11:32:41 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Sun May 15 12:36:29 2011 +0200
1.3 @@ -997,90 +997,82 @@
1.4 | pos => error ("header called with "^ pos_2str pos);
1.5
1.6
1.7 -fun specify_additem sel (ct,_) (p,Met) c pt =
1.8 - let
1.9 - val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.10 - probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1.11 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.12 - (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1.13 - val cpI = if pI = e_pblID then pI' else pI;
1.14 - val cmI = if mI = e_metID then mI' else mI;
1.15 - val {ppc,pre,prls,...} = get_met cmI;
1.16 - in case appl_add ctxt sel oris met ppc ct of
1.17 - Add itm (*..union old input *) =>
1.18 - let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1.19 - *)
1.20 - val met' = insert_ppc thy itm met;
1.21 - (*val pt' = update_met pt p met';*)
1.22 - val ((p,Met),_,_,pt') =
1.23 - generate1 thy (case sel of
1.24 - "#Given" => Add_Given' (ct, met')
1.25 - | "#Find" => Add_Find' (ct, met')
1.26 - | "#Relate"=> Add_Relation'(ct, met'))
1.27 - (Uistate, e_ctxt) (p,Met) pt
1.28 - val pre' = check_preconds thy prls pre met'
1.29 - val pb = foldl and_ (true, map fst pre')
1.30 - (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
1.31 - val (p_,nxt) =
1.32 - nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1.33 - ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1.34 - in ((p,p_), ((p,p_),Uistate),
1.35 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.36 - (Method cmI, itms2itemppc thy met' pre'))),
1.37 - nxt,Safe,pt') end
1.38 - | Err msg =>
1.39 - let val pre' = check_preconds thy prls pre met
1.40 - val pb = foldl and_ (true, map fst pre')
1.41 - (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
1.42 - val (p_,nxt) =
1.43 - nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1.44 - ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1.45 - in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.46 - end
1.47 -(* val (p,_) = p;
1.48 - *)
1.49 -| specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt =
1.50 - let
1.51 - val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.52 - probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1.53 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.54 - val cpI = if pI = e_pblID then pI' else pI;
1.55 - val cmI = if mI = e_metID then mI' else mI;
1.56 - val {ppc,where_,prls,...} = get_pbt cpI;
1.57 - in case appl_add ctxt sel oris pbl ppc ct of
1.58 - Add itm (*..union old input *) =>
1.59 - (* val Add itm = appl_add thy sel oris pbl ppc ct;
1.60 - *)
1.61 - let
1.62 - (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
1.63 - val pbl' = insert_ppc thy itm pbl
1.64 - val ((p,Pbl),_,_,pt') =
1.65 - generate1 thy (case sel of
1.66 - "#Given" => Add_Given' (ct, pbl')
1.67 - | "#Find" => Add_Find' (ct, pbl')
1.68 - | "#Relate"=> Add_Relation'(ct, pbl'))
1.69 - (Uistate, e_ctxt) (p,Pbl) pt
1.70 - val pre = check_preconds thy prls where_ pbl'
1.71 - val pb = foldl and_ (true, map fst pre)
1.72 - (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
1.73 - val (p_,nxt) =
1.74 - nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1.75 - (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1.76 - val ppc = if p_= Pbl then pbl' else met;
1.77 - in ((p,p_), ((p,p_),Uistate),
1.78 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.79 - (header p_ pI cmI,
1.80 - itms2itemppc thy ppc pre))), nxt,Safe,pt') end
1.81 +fun specify_additem sel (ct,_) (p, Met) c pt =
1.82 + let
1.83 + val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.84 + probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1.85 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.86 + val cpI = if pI = e_pblID then pI' else pI;
1.87 + val cmI = if mI = e_metID then mI' else mI;
1.88 + val {ppc,pre,prls,...} = get_met cmI;
1.89 + in
1.90 + case appl_add ctxt sel oris met ppc ct of
1.91 + Add itm (*..union old input *) =>
1.92 + let
1.93 + val met' = insert_ppc thy itm met;
1.94 + val ((p, Met), _, _, pt') =
1.95 + generate1 thy (case sel of
1.96 + "#Given" => Add_Given' (ct, met')
1.97 + | "#Find" => Add_Find' (ct, met')
1.98 + | "#Relate"=> Add_Relation'(ct, met'))
1.99 + (Uistate, e_ctxt) (p, Met) pt
1.100 + val pre' = check_preconds thy prls pre met'
1.101 + val pb = foldl and_ (true, map fst pre')
1.102 + val (p_, nxt) =
1.103 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1.104 + ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1.105 + in ((p, p_), ((p, p_), Uistate),
1.106 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.107 + (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
1.108 + end
1.109 + | Err msg =>
1.110 + let
1.111 + val pre' = check_preconds thy prls pre met
1.112 + val pb = foldl and_ (true, map fst pre')
1.113 + val (p_, nxt) =
1.114 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1.115 + ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1.116 + in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.117 + end
1.118
1.119 - | Err msg =>
1.120 - let val pre = check_preconds thy prls where_ pbl
1.121 - val pb = foldl and_ (true, map fst pre)
1.122 - (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
1.123 - val (p_,nxt) =
1.124 - nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1.125 - (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1.126 - in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.127 - end;
1.128 + | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt =
1.129 + let
1.130 + val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.131 + probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1.132 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.133 + val cpI = if pI = e_pblID then pI' else pI;
1.134 + val cmI = if mI = e_metID then mI' else mI;
1.135 + val {ppc,where_,prls,...} = get_pbt cpI;
1.136 + in
1.137 + case appl_add ctxt sel oris pbl ppc ct of
1.138 + Add itm (*..union old input *) =>
1.139 + let
1.140 + val pbl' = insert_ppc thy itm pbl
1.141 + val ((p, Pbl), _, _, pt') =
1.142 + generate1 thy (case sel of
1.143 + "#Given" => Add_Given' (ct, pbl')
1.144 + | "#Find" => Add_Find' (ct, pbl')
1.145 + | "#Relate"=> Add_Relation'(ct, pbl'))
1.146 + (Uistate, e_ctxt) (p,Pbl) pt
1.147 + val pre = check_preconds thy prls where_ pbl'
1.148 + val pb = foldl and_ (true, map fst pre)
1.149 + val (p_, nxt) =
1.150 + nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1.151 + (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1.152 + val ppc = if p_= Pbl then pbl' else met;
1.153 + in ((p,p_), ((p,p_),Uistate),
1.154 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.155 + (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt,Safe,pt')
1.156 + end
1.157 + | Err msg =>
1.158 + let
1.159 + val pre = check_preconds thy prls where_ pbl
1.160 + val pb = foldl and_ (true, map fst pre)
1.161 + val (p_, nxt) =
1.162 + nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1.163 + (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1.164 + in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.165 + end;
1.166
1.167 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1.168 let (* either """"""""""""""" all empty or complete *)